TORPAcyc is applied to the string rewriting system b c a -> a b a b b -> c c a a -> a c b a 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 2, label: a1 from 1 to 7, label: c1 from 2 to 3, label: b1 from 2 to 6, label: c2 from 2 to 8, label: c1 from 2 to 10, label: c1 from 2 to 12, label: b1 from 3 to 4, label: a1 from 3 to 17, label: a2 from 4 to 1, label: b1 from 4 to 5, label: c2 from 4 to 2, label: a1 from 5 to 1, label: c2 from 6 to 3, label: c2 from 6 to 12, label: c2 from 7 to 1, label: c1 from 8 to 9, label: b1 from 8 to 16, label: c2 from 9 to 1, label: a1 from 9 to 2, label: a1 from 9 to 17, label: a2 from 10 to 11, label: b1 from 10 to 15, label: c2 from 11 to 2, label: a1 from 12 to 13, label: a1 from 13 to 2, label: b1 from 13 to 14, label: c2 from 14 to 2, label: c2 from 15 to 11, label: c2 from 16 to 9, label: c2 from 17 to 18, label: c2 from 18 to 19, label: b2 from 18 to 20, label: c3 from 19 to 2, label: a2 from 20 to 19, label: c3