======================================================== The given Problem was: a a a a -> a c a c c c c c -> a a a ======================================================== A self-embedding rewrite structure for the given SRS is: a a a a c a a a c a a c a --(7)-> a c a a a a c a a a c a a c a c c (#3574) OC+OC at 5 OC: a a a a c --(2)-> a c a a a a (#6) OC+OC at 3 OC: a a a a --(1)-> a c a c c (#1) Rule OC: c c c --(1)-> a a a (#2) Rule OC: a a a a c a a c a --(5)-> a c a a a c a a c a c c (#241) OC+OC at 3 OC: a a a a --(1)-> a c a c c (#1) Rule OC: c c c a a c a --(4)-> a a c a a c a c c (#31) OC+OC at 1 OC: c c c --(1)-> a a a (#2) Rule OC: a a a a c a --(3)-> a c a a c a c c (#15) OC+OC at 3 OC: a a a a --(1)-> a c a c c (#1) Rule OC: c c c a --(2)-> a c a c c (#3) OC+OC at 0 OC: c c c --(1)-> a a a (#2) Rule OC: a a a a --(1)-> a c a c c (#1) Rule Hence, the SRS is non-terminating.