======================================================== The given Problem was: a -> a b -> b b -> c c a -> a a b c ======================================================== A self-embedding rewrite structure for the given SRS is: c a a a a a --(15)-> a c a a a a a b c b c (#140963) OC+OC at 2 OC: c a a --(6)-> a c c (#140) OC+OC at 1 OC: c a a --(5)-> a b b c (#65) OC+OC at 2 OC: c a a --(4)-> a b a b c (#45) OC+OC at 2 OC: c a --(2)-> a b c (#5) OC+OC at 0 OC: c a --(1)-> a a b c (#4) Rule OC: a --(1)-> (#1) Rule OC: c a --(2)-> a b c (#5) OC+OC at 0 OC: c a --(1)-> a a b c (#4) Rule OC: a --(1)-> (#1) Rule OC: a --(1)-> (#1) Rule OC: b b --(1)-> c (#3) Rule OC: c a a a --(9)-> a a a a a b c b c (#7952) OC+OC at 3 OC: c a a a --(8)-> a a a c a b c (#2512) OC+OC at 2 OC: c a a a --(6)-> a a c a a b c (#501) OC+OC at 3 OC: c a a --(5)-> a a c c (#141) OC+OC at 2 OC: c a a --(4)-> a a b b c (#63) OC+OC at 3 OC: c a a --(3)-> a a b a b c (#47) OC+OC at 3 OC: c a --(1)-> a a b c (#4) Rule OC: c a --(2)-> a b c (#5) OC+OC at 0 OC: c a --(1)-> a a b c (#4) Rule OC: a --(1)-> (#1) Rule OC: a --(1)-> (#1) Rule OC: b b --(1)-> c (#3) Rule OC: c a --(1)-> a a b c (#4) Rule OC: c a --(2)-> a c (#8) OC+OC at 1 OC: c a --(1)-> a a b c (#4) Rule OC: a b --(1)-> (#2) Rule OC: c a --(1)-> a a b c (#4) Rule Hence, the SRS is non-terminating.