======================================================== The given Problem was: a a a -> a b b c -> c c 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 a c c a c c a a c c a b c a a c c a c c a b (#88046) OC+OC at 20 OC: b c a a c c a c --(15)-> c c a c c a c c a a c c a b c a a c c a b (#22112) OC+OC at 17 OC: b c a a c c a --(13)-> c c a c c a c c a a c c a b c a a b (#8655) OC+OC at 10 OC: b c a a c c a --(11)-> c c a c c a c c a a b c c a a b (#1955) OC+OC at 11 OC: b c a a c --(9)-> c c a c c a c c a a b b (#719) OC+OC at 6 OC: b c a a c --(7)-> c c a c c a b c a b (#162) OC+OC at 3 OC: b c a a c --(5)-> c c a b c c a b (#32) OC+OC at 4 OC: b c a a --(3)-> c c a b b (#17) OC+OC at 2 OC: b c a a --(2)-> c c a a a b (#6) OC+OC at 4 OC: b c --(1)-> c c a a a (#2) Rule OC: a a a --(1)-> a b (#1) Rule OC: a a a --(1)-> a b (#1) Rule OC: b c --(2)-> c c a b (#4) OC+OC at 2 OC: b c --(1)-> c c a a a (#2) Rule OC: a a a --(1)-> a b (#1) Rule OC: b c --(2)-> c c a b (#4) OC+OC at 2 OC: b c --(1)-> c c a a a (#2) Rule OC: a a a --(1)-> a b (#1) Rule OC: b c a --(2)-> c c a a b (#5) OC+OC at 3 OC: b c --(1)-> c c a a a (#2) Rule OC: a a a --(1)-> a b (#1) Rule OC: b c a --(2)-> c c a a b (#5) OC+OC at 3 OC: b c --(1)-> c c a a a (#2) Rule OC: a a a --(1)-> a b (#1) Rule OC: b c --(2)-> c c a b (#4) OC+OC at 2 OC: b c --(1)-> c c a a a (#2) Rule OC: a a a --(1)-> a b (#1) Rule OC: b c --(2)-> c c a b (#4) OC+OC at 2 OC: b c --(1)-> c c a a a (#2) Rule OC: a a a --(1)-> a b (#1) Rule OC: b c --(2)-> c c a b (#4) OC+OC at 2 OC: b c --(1)-> c c a a a (#2) Rule OC: a a a --(1)-> a b (#1) Rule Hence, the SRS is non-terminating.