======================================================== The given Problem was: a a b -> b b c a c a c -> a a ======================================================== A self-embedding rewrite structure for the given SRS is: a c c a b b c b b --(18)-> b b c b b c a b b c b b c a c c a b b c b b c a c (#1345782) OC+OC at 17 OC: a c c a b b --(14)-> b b c b b c a b b c b b c a c c a a (#83598) OC+OC at 10 OC: a c c a b b --(12)-> b b c b b c a b b c a c b c a a (#26269) OC+OC at 7 OC: a c c a b b --(10)-> b b c b b c a a c b b c a a (#4435) OC+OC at 9 OC: a c c a b --(7)-> b b c b b c a a c a c (#956) OC+OC at 3 OC: a c c a b --(4)-> b b c a c b c a c (#226) OC+OC at 0 OC: a c c a b --(3)-> a a b b c a c (#19) OC+OC at 1 OC: a c --(1)-> a a (#2) Rule OC: a c a b --(2)-> a b b c a c (#7) OC+OC at 1 OC: a c --(1)-> a a (#2) Rule OC: a a b --(1)-> b b c a c (#1) Rule OC: a a b --(1)-> b b c a c (#1) Rule OC: a c b --(3)-> b b c a a (#10) OC+OC at 0 OC: a c --(1)-> a a (#2) Rule OC: a a b --(2)-> b b c a a (#8) OC+OC at 3 OC: a a b --(1)-> b b c a c (#1) Rule OC: a c --(1)-> a a (#2) Rule OC: a c b --(3)-> b b c a a (#10) OC+OC at 0 OC: a c --(1)-> a a (#2) Rule OC: a a b --(2)-> b b c a a (#8) OC+OC at 3 OC: a a b --(1)-> b b c a c (#1) Rule OC: a c --(1)-> a a (#2) Rule OC: a c b --(2)-> b b c a c (#6) OC+OC at 0 OC: a c --(1)-> a a (#2) Rule OC: a a b --(1)-> b b c a c (#1) Rule OC: a c b --(2)-> b b c a c (#6) OC+OC at 0 OC: a c --(1)-> a a (#2) Rule OC: a a b --(1)-> b b c a c (#1) Rule OC: a c b b --(4)-> b b c b b c a c (#50) OC+OC at 0 OC: a c --(1)-> a a (#2) Rule OC: a a b b --(3)-> b b c b b c a c (#41) OC+OC at 3 OC: a a b --(1)-> b b c a c (#1) Rule OC: a c b --(2)-> b b c a c (#6) OC+OC at 0 OC: a c --(1)-> a a (#2) Rule OC: a a b --(1)-> b b c a c (#1) Rule Hence, the SRS is non-terminating.