TORPAcyc is applied to the string rewriting system a a a -> b b b b b -> c d c -> a a d -> c interpretation of a: 2 interpretation of b: 3 interpretation of c: 4 interpretation of d: 4 remove rule 2 continue with: a a a -> b b c -> a a d -> c interpretation of a: 1 interpretation of b: 1 interpretation of c: 9 interpretation of d: 10 remove rule 3 continue with: a a a -> b b c -> a a interpretation of a: 1 interpretation of b: 1 interpretation of c: 3 interpretation of d: 10 remove rule 2 continue with: a a a -> b b interpretation of a: 1 interpretation of b: 0 interpretation of c: 8 interpretation of d: 10 remove rule 1 termination has been proved