======================================================== The given Problem was: a a b -> b b c a a a c -> a a ======================================================== A self-embedding rewrite structure for the given SRS is: a a b c a b b c b b --(11)-> b b c b b c b b c a b b c a a b c a b b c b b c a a (#352242) OC+OC at 18 OC: a a b c a b b --(8)-> b b c b b c b b c a b b c a a b c a a (#25589) OC+OC at 10 OC: a a b c a b b --(6)-> b b c b b c b b c a a c b b c a a (#4242) OC+OC at 12 OC: a a b c a b --(5)-> b b c b b c b b c a a c a a (#1653) OC+OC at 6 OC: a a b c a b --(4)-> b b c b b c a a b c a a (#651) OC+OC at 3 OC: a a b c a b --(3)-> b b c a a b b c a a (#67) OC+OC at 4 OC: a a b --(1)-> b b c a a (#1) Rule OC: a c a b --(2)-> a b b c a a (#7) OC+OC at 1 OC: a c --(1)-> a a (#2) Rule OC: a a b --(1)-> b b c a a (#1) Rule OC: a a b --(1)-> b b c a a (#1) Rule OC: a a b --(1)-> b b c a a (#1) Rule OC: a a b --(1)-> b b c a a (#1) Rule OC: a c b --(2)-> b b c a a (#6) OC+OC at 0 OC: a c --(1)-> a a (#2) Rule OC: a a b --(1)-> b b c a a (#1) Rule OC: a c b b --(3)-> b b c b b c a a (#31) OC+OC at 0 OC: a c --(1)-> a a (#2) Rule OC: a a b b --(2)-> b b c b b c a a (#25) OC+OC at 3 OC: a a b --(1)-> b b c a a (#1) Rule OC: a a b --(1)-> b b c a a (#1) Rule Hence, the SRS is non-terminating.