======================================================== The given Problem was: a a a -> b b c -> c c a a a a ======================================================== A self-embedding rewrite structure for the given SRS is: b c a a c c a c c --(17)-> c c c c a c c a a c c a b c a a c c a c c b a (#160684) OC+OC at 19 OC: b c a a c c a c --(15)-> c c c c a c c a a c c a b c a a c c a b (#36622) OC+OC at 16 OC: b c a a c c a --(13)-> c c c c a c c a a c c a b c a a b (#13320) OC+OC at 9 OC: b c a a c c a --(11)-> c c c c a c c a a b c c a a b (#2825) OC+OC at 10 OC: b c a a c --(9)-> c c c c a c c a a b b (#981) OC+OC at 5 OC: b c a a c --(7)-> c c c c a b c a b (#187) OC+OC at 2 OC: b c a a c --(5)-> c c b c c a b (#24) OC+OC at 3 OC: b c --(2)-> c c b a (#4) OC+OC at 2 OC: b c --(1)-> c c a a a a (#2) Rule OC: a a a --(1)-> b (#1) Rule OC: a a a c --(3)-> c c a b (#14) OC+OC at 3 OC: a a a c --(2)-> c c a a a a (#3) OC+OC at 0 OC: a a a --(1)-> b (#1) Rule OC: b c --(1)-> c c a a a a (#2) Rule OC: a a a --(1)-> b (#1) Rule OC: b c --(2)-> c c a b (#5) OC+OC at 3 OC: b c --(1)-> c c a a a a (#2) Rule OC: a a a --(1)-> b (#1) Rule OC: b c a --(2)-> c c a a b (#6) OC+OC at 4 OC: b c --(1)-> c c a a a a (#2) Rule OC: a a a --(1)-> b (#1) Rule OC: b c a --(2)-> c c a a b (#6) OC+OC at 4 OC: b c --(1)-> c c a a a a (#2) Rule OC: a a a --(1)-> b (#1) Rule OC: b c --(2)-> c c a b (#5) OC+OC at 3 OC: b c --(1)-> c c a a a a (#2) Rule OC: a a a --(1)-> b (#1) Rule OC: b c --(2)-> c c a b (#5) OC+OC at 3 OC: b c --(1)-> c c a a a a (#2) Rule OC: a a a --(1)-> b (#1) Rule OC: b c --(2)-> c c b a (#4) OC+OC at 2 OC: b c --(1)-> c c a a a a (#2) Rule OC: a a a --(1)-> b (#1) Rule Hence, the SRS is non-terminating.