======================================================== The given Problem was: a -> b a b -> b b a c c a c b -> ======================================================== A self-embedding rewrite structure for the given SRS is: a b b b b b b b --(18)-> b b a b b b b b b b c c a c c a (#171326) OC+OC at 7 OC: a b b b b b b b --(16)-> b b a b b b b a b c c a (#33931) OC+OC at 8 OC: a b b b b b b b --(15)-> b b a b b b b a c b b c c a (#13922) OC+OC at 5 OC: a b b b b b --(11)-> b b a b b a (#417) OC+OC at 3 OC: a b b b b b --(10)-> b b a c b b b a (#211) OC+OC at 8 OC: a b b b b --(9)-> b b a c b b b a c (#84) OC+OC at 5 OC: a b b b --(6)-> b b a c b a (#33) OC+OC at 4 OC: a b b b --(5)-> b b a c c b b a (#22) OC+OC at 8 OC: a b b --(4)-> b b a c c b b a c (#11) OC+OC at 5 OC: a b --(1)-> b b a c c a (#2) Rule OC: a b --(3)-> b b a c (#6) OC+OC at 4 OC: a b --(2)-> b b a c c b (#5) OC+OC at 5 OC: a b --(1)-> b b a c c a (#2) Rule OC: a --(1)-> b (#1) Rule OC: c b --(1)-> (#3) Rule OC: c b --(1)-> (#3) Rule OC: c b --(1)-> (#3) Rule OC: a b --(3)-> b b a c (#6) OC+OC at 4 OC: a b --(2)-> b b a c c b (#5) OC+OC at 5 OC: a b --(1)-> b b a c c a (#2) Rule OC: a --(1)-> b (#1) Rule OC: c b --(1)-> (#3) Rule OC: c b --(1)-> (#3) Rule OC: c b --(1)-> (#3) Rule OC: a b b --(4)-> b b a c b b c c a (#39) OC+OC at 4 OC: a b b --(3)-> b b a c c b b b c c a (#14) OC+OC at 5 OC: a b --(1)-> b b a c c a (#2) Rule OC: a b --(2)-> b b b c c a (#4) OC+OC at 2 OC: a b --(1)-> b b a c c a (#2) Rule OC: a --(1)-> b (#1) Rule OC: c b --(1)-> (#3) Rule OC: c b --(1)-> (#3) Rule OC: a b --(2)-> b b b c c a (#4) OC+OC at 2 OC: a b --(1)-> b b a c c a (#2) Rule OC: a --(1)-> b (#1) Rule Hence, the SRS is non-terminating.