======================================================== The given Problem was: a a b -> a c c a a a a c -> b ======================================================== A self-embedding rewrite structure for the given SRS is: a a b a b c b c --(18)-> a c c a c c b c a b c a a b a b c b c a a a (#1370327) OC+OC at 15 OC: a a b a b c b c --(17)-> a c c a c c b c a b c a a b a a c c b c a a a (#942444) OC+OC at 15 OC: a a b a b c --(13)-> a c c a c c b c a b c a a b a a a (#62176) OC+OC at 9 OC: a a b a b c --(10)-> a c c a c c b c a a a b c a a a (#8203) OC+OC at 11 OC: a a b a b c --(8)-> a c c a c c b c a a a a a b (#2586) OC+OC at 6 OC: a a b a b c --(6)-> a c c a c c a a b a a b (#884) OC+OC at 3 OC: a a b a b c --(4)-> a c c a a b c a a b (#23) OC+OC at 5 OC: a a b --(1)-> a c c a a a (#1) Rule OC: a a b c --(3)-> b c a a b (#5) OC+OC at 0 OC: a a b c --(2)-> a c c a a b (#4) OC+OC at 5 OC: a a b --(1)-> a c c a a a (#1) Rule OC: a c --(1)-> b (#2) Rule OC: a c --(1)-> b (#2) Rule OC: a a b c --(2)-> a c c a a b (#4) OC+OC at 5 OC: a a b --(1)-> a c c a a a (#1) Rule OC: a c --(1)-> b (#2) Rule OC: a a b --(2)-> b c a a a (#3) OC+OC at 0 OC: a a b --(1)-> a c c a a a (#1) Rule OC: a c --(1)-> b (#2) Rule OC: a a b --(2)-> b c a a a (#3) OC+OC at 0 OC: a a b --(1)-> a c c a a a (#1) Rule OC: a c --(1)-> b (#2) Rule OC: a a b c --(3)-> b c a a b (#5) OC+OC at 0 OC: a a b c --(2)-> a c c a a b (#4) OC+OC at 5 OC: a a b --(1)-> a c c a a a (#1) Rule OC: a c --(1)-> b (#2) Rule OC: a c --(1)-> b (#2) Rule OC: a a b c --(4)-> a c c b c a a a (#33) OC+OC at 3 OC: a a b c --(2)-> a c c a a b (#4) OC+OC at 5 OC: a a b --(1)-> a c c a a a (#1) Rule OC: a c --(1)-> b (#2) Rule OC: a a b --(2)-> b c a a a (#3) OC+OC at 0 OC: a a b --(1)-> a c c a a a (#1) Rule OC: a c --(1)-> b (#2) Rule OC: a c --(1)-> b (#2) Rule Hence, the SRS is non-terminating.