======================================================== The given Problem was: a -> a -> b a b -> b a c a b -> c c -> ======================================================== A self-embedding rewrite structure for the given SRS is: a b b b c b --(11)-> b a b b b c b (#45592) OC+OC at 4 OC: a b b b c b --(10)-> b a b b a c b (#18820) OC+OC at 2 OC: a b b --(5)-> b a a (#173) OC+OC at 2 OC: a b b --(4)-> b a c c a (#67) OC+OC at 3 OC: a b b --(3)-> b a c b c a (#48) OC+OC at 3 OC: a b --(1)-> b a c a (#3) Rule OC: a b --(2)-> b c a (#7) OC+OC at 1 OC: a b --(1)-> b a c a (#3) Rule OC: a --(1)-> (#1) Rule OC: b --(1)-> (#4) Rule OC: c c --(1)-> (#5) Rule OC: a b c b --(5)-> b b a c b (#362) OC+OC at 1 OC: a b c --(3)-> b a (#14) OC+OC at 2 OC: a b --(2)-> b a c (#8) OC+OC at 3 OC: a b --(1)-> b a c a (#3) Rule OC: a --(1)-> (#1) Rule OC: c c --(1)-> (#5) Rule OC: a b --(2)-> b a c b (#11) OC+OC at 3 OC: a b --(1)-> b a c a (#3) Rule OC: a --(1)-> b (#2) Rule OC: a --(1)-> b (#2) Rule Hence, the SRS is non-terminating.