======================================================== The given Problem was: a -> b a b c -> c c a a c c -> b ======================================================== A self-embedding rewrite structure for the given SRS is: a b c b c c c c c --(12)-> c c a b c b c c c c c a a (#82706) OC+OC at 3 OC: a b c --(1)-> c c a a (#2) Rule OC: a b c c c c c --(11)-> b c b c c c c c a a (#15810) OC+OC at 1 OC: a b c --(3)-> b a b (#10) OC+OC at 0 OC: a b c --(2)-> c c a b (#5) OC+OC at 3 OC: a b c --(1)-> c c a a (#2) Rule OC: a --(1)-> b (#1) Rule OC: c c --(1)-> b (#3) Rule OC: a b c c c c --(8)-> c b c c c c c a a (#2047) OC+OC at 3 OC: a b c c --(5)-> c b c a b (#81) OC+OC at 1 OC: a b c c --(4)-> c c c c a b (#68) OC+OC at 2 OC: a b c --(2)-> c c a b (#5) OC+OC at 3 OC: a b c --(1)-> c c a a (#2) Rule OC: a --(1)-> b (#1) Rule OC: a b c --(2)-> c c a b (#5) OC+OC at 3 OC: a b c --(1)-> c c a a (#2) Rule OC: a --(1)-> b (#1) Rule OC: c c --(1)-> b (#3) Rule OC: a b c c --(3)-> c c c c a a (#31) OC+OC at 2 OC: a b c --(2)-> c c a b (#5) OC+OC at 3 OC: a b c --(1)-> c c a a (#2) Rule OC: a --(1)-> b (#1) Rule OC: a b c --(1)-> c c a a (#2) Rule Hence, the SRS is non-terminating.