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