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