========================================================
The given Problem was:
a a -> b
b a c -> c c a a a a
========================================================
A self-embedding rewrite structure for the given SRS is:
b a c a a c c a c c --(17)-> c c c c a c c a a c c a b a c a a c c a c c a a b (#1047918)
OC+OC at 17
OC: b a c a a c c --(13)-> c c c c a c c a a c c a b a c a a b (#66965)
OC+OC at 9
OC: b a c a a c c --(11)-> c c c c a c c a a b a c c a a b (#11959)
OC+OC at 11
OC: b a c a a c --(9)-> c c c c a c c a a b a b a (#3608)
OC+OC at 5
OC: b a c a a c --(7)-> c c c c a b a c a b a (#1068)
OC+OC at 2
OC: b a c a a c --(5)-> c c b a c c a b a (#66)
OC+OC at 4
OC: b a c --(2)-> c c b a a (#4)
OC+OC at 2
OC: b a c --(1)-> c c a a a a (#2)
Rule
OC: a a --(1)-> b (#1)
Rule
OC: a a a c --(3)-> c c a b a (#12)
OC+OC at 3
OC: a a a c --(2)-> c c a a a a (#3)
OC+OC at 0
OC: a a --(1)-> b (#1)
Rule
OC: b a c --(1)-> c c a a a a (#2)
Rule
OC: a a --(1)-> b (#1)
Rule
OC: b a c --(2)-> c c a b a (#5)
OC+OC at 3
OC: b a c --(1)-> c c a a a a (#2)
Rule
OC: a a --(1)-> b (#1)
Rule
OC: b a c --(2)-> c c a a b (#6)
OC+OC at 4
OC: b a c --(1)-> c c a a a a (#2)
Rule
OC: a a --(1)-> b (#1)
Rule
OC: b a c --(2)-> c c a a b (#6)
OC+OC at 4
OC: b a c --(1)-> c c a a a a (#2)
Rule
OC: a a --(1)-> b (#1)
Rule
OC: b a c --(2)-> c c a b a (#5)
OC+OC at 3
OC: b a c --(1)-> c c a a a a (#2)
Rule
OC: a a --(1)-> b (#1)
Rule
OC: b a c c --(4)-> c c a c c a a b (#20)
OC+OC at 3
OC: b a c --(2)-> c c a b a (#5)
OC+OC at 3
OC: b a c --(1)-> c c a a a a (#2)
Rule
OC: a a --(1)-> b (#1)
Rule
OC: b a c --(2)-> c c a a b (#6)
OC+OC at 4
OC: b a c --(1)-> c c a a a a (#2)
Rule
OC: a a --(1)-> b (#1)
Rule
Hence, the SRS is non-terminating.