======================================================== The given Problem was: b a a -> a a a a -> b b b b b -> a b a ======================================================== A self-embedding rewrite structure for the given SRS is: b b a a --(8)-> b b a a (#919) OC+OC at 3 OC: b b a a --(7)-> b b a b a a (#511) OC+OC at 2 OC: b b a a --(6)-> b b b b a (#487) OC+OC at 0 OC: b b a a --(5)-> a a a b a (#290) OC+OC at 1 OC: b b a a --(3)-> a b b a b a (#21) OC+OC at 2 OC: b b --(1)-> a b a (#3) Rule OC: a a a --(2)-> b a b a (#9) OC+OC at 1 OC: a a a --(1)-> b b b (#2) Rule OC: b b --(1)-> a b a (#3) Rule OC: b b a --(2)-> a a (#4) OC+OC at 1 OC: b b --(1)-> a b a (#3) Rule OC: b a a --(1)-> a (#1) Rule OC: a a a --(1)-> b b b (#2) Rule OC: b b --(1)-> a b a (#3) Rule OC: b a a --(1)-> a (#1) Rule Hence, the SRS is non-terminating.