======================================================== The given Problem was: a -> a a a -> b b c -> c c a b c -> ======================================================== A self-embedding rewrite structure for the given SRS is: b c c c c c c --(14)-> c c b c c c c c c b (#57010) OC+OC at 5 OC: b c c c c c c --(13)-> c c b c c a c c c c b (#49958) OC+OC at 3 OC: b c c c --(8)-> c c b b (#907) OC+OC at 2 OC: b c c c --(7)-> c c a a a b (#536) OC+OC at 4 OC: b c c c --(6)-> c c a a c a b (#201) OC+OC at 3 OC: b c --(1)-> c c a b (#3) Rule OC: b c c --(5)-> a c a b (#59) OC+OC at 0 OC: b c c --(4)-> c a c a b (#18) OC+OC at 2 OC: b c --(2)-> c a b (#6) OC+OC at 0 OC: b c --(1)-> c c a b (#3) Rule OC: c --(1)-> (#4) Rule OC: b c --(2)-> c a b (#6) OC+OC at 0 OC: b c --(1)-> c c a b (#3) Rule OC: c --(1)-> (#4) Rule OC: c --(1)-> (#4) Rule OC: c --(1)-> (#4) Rule OC: a a a --(1)-> b (#2) Rule OC: b c c c --(5)-> c c a c c c c b (#208) OC+OC at 3 OC: b c --(1)-> c c a b (#3) Rule OC: b c c --(4)-> c c c c b (#26) OC+OC at 2 OC: b c --(2)-> c c b (#5) OC+OC at 2 OC: b c --(1)-> c c a b (#3) Rule OC: a --(1)-> (#1) Rule OC: b c --(2)-> c c b (#5) OC+OC at 2 OC: b c --(1)-> c c a b (#3) Rule OC: a --(1)-> (#1) Rule OC: a --(1)-> (#1) Rule Hence, the SRS is non-terminating.