======================================================== The given Problem was: a a a -> a b b b a b -> a b a ======================================================== A self-embedding rewrite structure for the given SRS is: a a a a b a --(6)-> a a a a b a (#98) OC+OC at 3 OC: a a a a b a --(5)-> a a a b a b (#74) OC+OC at 2 OC: a a a a b a --(4)-> a a b a b b (#27) OC+OC at 3 OC: a a a a b --(3)-> a a b a a (#15) OC+OC at 1 OC: a a a a b --(2)-> a b a b a (#5) OC+OC at 2 OC: a a a --(1)-> a b b (#1) Rule OC: b a b --(1)-> a b a (#2) Rule OC: b a b --(1)-> a b a (#2) Rule OC: a a a --(1)-> a b b (#1) Rule OC: b a b --(1)-> a b a (#2) Rule OC: b a b --(1)-> a b a (#2) Rule Hence, the SRS is non-terminating.