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