TORPAcyc is applied to the string rewriting system a -> b b b b b -> a interpretation of a: 5 interpretation of b: 2 remove rule 2 continue with: a -> b b interpretation of a: 9 interpretation of b: 4 remove rule 1 termination has been proved