======================================================== The given Problem was: a a -> a b b a c -> c c a a a ======================================================== A self-embedding rewrite structure for the given SRS is: b a c a a c c a c c --(16)-> c c a c c a c c a a c c a b a c a a c c a c c a a a (#508692) OC+OC at 18 OC: b a c a a c c --(13)-> c c a c c a c c a a c c a b a c a a b (#47771) OC+OC at 10 OC: b a c a a c c --(11)-> c c a c c a c c a a b a c c a a b (#8981) OC+OC at 12 OC: b a c a a c --(9)-> c c a c c a c c a a b a b a (#2966) OC+OC at 6 OC: b a c a a c --(7)-> c c a c c a b a c a b a (#916) OC+OC at 3 OC: b a c a a c --(5)-> c c a b a c c a b a (#80) OC+OC at 4 OC: b a c --(2)-> c c a b a (#4) OC+OC at 2 OC: b a c --(1)-> c c a a a (#2) Rule OC: a a --(1)-> a b (#1) Rule OC: a a a c --(3)-> a c c a b a (#7) OC+OC at 1 OC: a a --(1)-> a b (#1) Rule OC: b a c --(2)-> c c a b a (#4) OC+OC at 2 OC: b a c --(1)-> c c a a a (#2) Rule OC: a a --(1)-> a b (#1) Rule OC: b a c --(2)-> c c a b a (#4) OC+OC at 2 OC: b a c --(1)-> c c a a a (#2) Rule OC: a a --(1)-> a b (#1) Rule OC: b a c --(2)-> c c a a b (#5) OC+OC at 3 OC: b a c --(1)-> c c a a a (#2) Rule OC: a a --(1)-> a b (#1) Rule OC: b a c --(2)-> c c a a b (#5) OC+OC at 3 OC: b a c --(1)-> c c a a a (#2) Rule OC: a a --(1)-> a b (#1) Rule OC: b a c --(2)-> c c a b a (#4) OC+OC at 2 OC: b a c --(1)-> c c a a a (#2) Rule OC: a a --(1)-> a b (#1) Rule OC: b a c c --(3)-> c c a c c a a a (#24) OC+OC at 3 OC: b a c --(2)-> c c a b a (#4) OC+OC at 2 OC: b a c --(1)-> c c a a a (#2) Rule OC: a a --(1)-> a b (#1) Rule OC: b a c --(1)-> c c a a a (#2) Rule Hence, the SRS is non-terminating.