======================================================== 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.