======================================================== The given Problem was: a -> a b -> b a c b a b -> c c -> ======================================================== A self-embedding rewrite structure for the given SRS is: a b b b c b --(12)-> b a b b b c b a (#16712) OC+OC at 5 OC: a b b b c b --(11)-> b a b b b a c b a (#8889) OC+OC at 4 OC: a b b b c --(10)-> b a b b a (#567) OC+OC at 5 OC: a b b b --(9)-> b a b b a c (#182) OC+OC at 6 OC: a b b b --(8)-> b a b b a c a (#161) OC+OC at 3 OC: a b b --(6)-> b a b a (#135) OC+OC at 2 OC: a b b --(5)-> b a c c b a (#58) OC+OC at 3 OC: a b b --(4)-> b a c a c b a (#17) OC+OC at 3 OC: a b --(2)-> b a c a (#8) OC+OC at 3 OC: a b --(1)-> b a c b a (#2) Rule OC: b --(1)-> (#3) Rule OC: a b --(2)-> a c b a (#7) OC+OC at 0 OC: a b --(1)-> b a c b a (#2) Rule OC: b --(1)-> (#3) Rule OC: a --(1)-> (#1) Rule OC: c c --(1)-> (#4) Rule OC: a b --(2)-> b a c a (#8) OC+OC at 3 OC: a b --(1)-> b a c b a (#2) Rule OC: b --(1)-> (#3) Rule OC: a --(1)-> (#1) Rule OC: c c --(1)-> (#4) Rule OC: a b --(1)-> b a c b a (#2) Rule OC: a --(1)-> (#1) Rule Hence, the SRS is non-terminating.