TORPAcyc is applied to the string rewriting system a a a -> b b b -> b a b b b -> a a Tropical matrix interpretation interpretation of a: / 3 3 \ \ 0 2 / interpretation of b: / 3 3 \ \ 3 3 / remove rule 3 continue with: a a a -> b b b -> b a b Tropical matrix interpretation interpretation of a: / 3 3 \ \ 0 1 / interpretation of b: / 1 0 \ \ 2 1 / remove rule 2 continue with: a a a -> b interpretation of a: 1 interpretation of b: 0 remove rule 1 termination has been proved