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