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