======================================================== The given Problem was: a -> a b b -> b b b a c a c b -> ======================================================== A self-embedding rewrite structure for the given SRS is: a b b b b b b b b --(15)-> b b b a b b b b b b b b a c a a c c (#55517) OC+OC at 4 OC: a b b b b b b b b --(14)-> b b b a c b b b b b b b b b a c a a c c (#32200) OC+OC at 5 OC: a b b --(1)-> b b b a c a (#2) Rule OC: a b b b b b b --(13)-> b b b b b b b b b a c a a c c (#10272) OC+OC at 6 OC: a b b b b b b --(12)-> b b b b b b a b b a c c (#6323) OC+OC at 3 OC: a b b b b b b --(9)-> b b b a b b b b b a c c (#786) OC+OC at 4 OC: a b b b b b b --(8)-> b b b a c b b b b b b a c c (#592) OC+OC at 5 OC: a b b --(1)-> b b b a c a (#2) Rule OC: a b b b b --(7)-> b b b b b b a c c (#91) OC+OC at 3 OC: a b b b b --(5)-> b b b a b b c (#37) OC+OC at 4 OC: a b b b b --(4)-> b b b a c b b b c (#15) OC+OC at 8 OC: a b b b b --(3)-> b b b a c b b b a c (#13) OC+OC at 5 OC: a b b --(1)-> b b b a c a (#2) Rule OC: a b b --(2)-> b b b a c (#5) OC+OC at 5 OC: a b b --(1)-> b b b a c a (#2) Rule OC: a --(1)-> (#1) Rule OC: a --(1)-> (#1) Rule OC: c b --(1)-> (#3) Rule OC: a b b --(2)-> b b b a c (#5) OC+OC at 5 OC: a b b --(1)-> b b b a c a (#2) Rule OC: a --(1)-> (#1) Rule OC: c b --(1)-> (#3) Rule OC: a b b b --(3)-> b b b a (#6) OC+OC at 4 OC: a b b --(2)-> b b b a c (#5) OC+OC at 5 OC: a b b --(1)-> b b b a c a (#2) Rule OC: a --(1)-> (#1) Rule OC: c b --(1)-> (#3) Rule OC: a b b --(1)-> b b b a c a (#2) Rule OC: c b --(1)-> (#3) Rule Hence, the SRS is non-terminating.