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