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