======================================================== The given Problem was: b c -> a b b b a -> a c b ======================================================== A self-embedding rewrite structure for the given SRS is: b c a a c a --(10)-> a a c a b a c b c a a c a b b b (#6541) OC+OC at 9 OC: b c a a --(6)-> a a c a b a c b c b (#302) OC+OC at 5 OC: b c a a --(5)-> a a c a b b a c b (#86) OC+OC at 6 OC: b c a --(4)-> a a c a b b b (#30) OC+OC at 3 OC: b c a --(3)-> a a c b c b (#17) OC+OC at 1 OC: b c a --(2)-> a b a c b (#5) OC+OC at 2 OC: b c --(1)-> a b b (#1) Rule OC: b a --(1)-> a c b (#2) Rule OC: b a --(1)-> a c b (#2) Rule OC: b c --(1)-> a b b (#1) Rule OC: b a --(1)-> a c b (#2) Rule OC: b a --(1)-> a c b (#2) Rule OC: b c a --(4)-> a a c a b b b (#30) OC+OC at 3 OC: b c a --(3)-> a a c b c b (#17) OC+OC at 1 OC: b c a --(2)-> a b a c b (#5) OC+OC at 2 OC: b c --(1)-> a b b (#1) Rule OC: b a --(1)-> a c b (#2) Rule OC: b a --(1)-> a c b (#2) Rule OC: b c --(1)-> a b b (#1) Rule Hence, the SRS is non-terminating.