======================================================== The given Problem was: a -> a b -> b a c b a a c b c -> ======================================================== A self-embedding rewrite structure for the given SRS is: a b b c b --(8)-> b a c b a b b c b a (#527) OC+OC at 7 OC: a b b c b --(7)-> b a c b a b b a c b a (#143) OC+OC at 6 OC: a b b c --(5)-> b a c b a b a (#50) OC+OC at 7 OC: a b b --(4)-> b a c b a b a c b (#41) OC+OC at 9 OC: a b b --(3)-> b a c b a b a c b a (#10) OC+OC at 5 OC: a b --(1)-> b a c b a a (#2) Rule OC: a b --(2)-> b a c b a (#5) OC+OC at 4 OC: a b --(1)-> b a c b a a (#2) Rule OC: a --(1)-> (#1) Rule OC: a --(1)-> (#1) Rule OC: c b c --(1)-> (#3) Rule OC: a b --(2)-> b a c b a (#5) OC+OC at 4 OC: a b --(1)-> b a c b a a (#2) Rule OC: a --(1)-> (#1) Rule OC: a --(1)-> (#1) Rule Hence, the SRS is non-terminating.