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