TORPAcyc is applied to the string rewriting system b c a -> a b a b c b -> c c c d -> a b c a a a -> a c b a interpretation of b: 0 interpretation of c: 0 interpretation of a: 0 interpretation of d: 10 remove rule 3 continue with: b c a -> a b a b c b -> c c a a -> a c b a Tropical matrix interpretation interpretation of b: / 2 1 \ \ 0 - / interpretation of c: / 1 0 \ \ 0 0 / interpretation of a: / 1 0 \ \ - 1 / interpretation of d: / 0 0 \ \ 0 0 / remove rule 3 continue with: b c a -> a b a b c b -> c c Terminating due to match bound 3, proved by the graph consisting of the following edges: from 1 to 1, label: b0 from 1 to 1, label: c0 from 1 to 1, label: a0 from 1 to 1, label: d0 from 1 to 2, label: a1 from 1 to 5, label: c1 from 2 to 3, label: b1 from 2 to 7, label: c2 from 2 to 12, label: b1 from 3 to 4, label: a1 from 4 to 5, label: b1 from 4 to 6, label: c2 from 4 to 2, label: a1 from 4 to 8, label: a2 from 5 to 1, label: c1 from 6 to 5, label: c2 from 7 to 3, label: c2 from 7 to 12, label: c2 from 8 to 9, label: b2 from 8 to 17, label: c3 from 9 to 10, label: a2 from 10 to 11, label: b2 from 10 to 16, label: c3 from 11 to 2, label: c2 from 12 to 13, label: a1 from 13 to 14, label: b1 from 13 to 15, label: c2 from 14 to 2, label: c1 from 15 to 14, label: c2 from 16 to 11, label: c3 from 17 to 9, label: c3