======================================================== The given Problem was: a -> a -> b c c b b b -> b a b a ======================================================== A self-embedding rewrite structure for the given SRS is: c b b b b b b b b b --(15)-> b b c b b b b b b b b b c c (#17919) OC+OC at 10 OC: c b b b b b b b b b --(14)-> b b c b b b b b b b a b b c c (#15204) OC+OC at 4 OC: c b b b --(2)-> b b c b a (#10) OC+OC at 1 OC: c b b b --(1)-> b a b a (#3) Rule OC: a --(1)-> b c (#2) Rule OC: a b b b b b b --(12)-> b b b b b b a b b c c (#7907) OC+OC at 4 OC: a b b b b b b --(9)-> b b b b a b b b c (#2043) OC+OC at 2 OC: a b b b b b b --(6)-> b b a b b b b b c (#190) OC+OC at 1 OC: a --(1)-> b c (#2) Rule OC: c b b b b b b --(5)-> b a b b b b b c (#89) OC+OC at 3 OC: c b b b --(1)-> b a b a (#3) Rule OC: a b b b --(4)-> b b b b c (#22) OC+OC at 1 OC: a --(1)-> b c (#2) Rule OC: c b b b --(3)-> b b b c (#12) OC+OC at 2 OC: c b b b --(2)-> b b a (#4) OC+OC at 1 OC: c b b b --(1)-> b a b a (#3) Rule OC: a --(1)-> (#1) Rule OC: a --(1)-> b c (#2) Rule OC: a b b b --(3)-> b b a b (#6) OC+OC at 1 OC: a --(1)-> b c (#2) Rule OC: c b b b --(2)-> b a b (#5) OC+OC at 3 OC: c b b b --(1)-> b a b a (#3) Rule OC: a --(1)-> (#1) Rule OC: a b b b --(3)-> b b a b b c (#21) OC+OC at 1 OC: a --(1)-> b c (#2) Rule OC: c b b b --(2)-> b a b b c (#11) OC+OC at 3 OC: c b b b --(1)-> b a b a (#3) Rule OC: a --(1)-> b c (#2) Rule OC: a --(1)-> (#1) Rule Hence, the SRS is non-terminating.