======================================================== The given Problem was: a a -> b a b c -> c c a a a a ======================================================== A self-embedding rewrite structure for the given SRS is: a b c b c c a c c --(18)-> c c c c a c c a a c c a a b c b c c a c c b b (#1829797) OC+OC at 15 OC: a b c b c c a c c --(17)-> c c c c a c c a a c c a a b c a a c c a c c b b (#1373623) OC+OC at 17 OC: a b c b c c a --(12)-> c c c c a c c a a c c a a b c a a a b (#70048) OC+OC at 9 OC: a b c b c c a --(10)-> c c c c a c c a a a b c c a a a b (#7400) OC+OC at 16 OC: a b c b c c --(9)-> c c c c a c c a a a b c c a a a a (#5284) OC+OC at 11 OC: a b c b c --(8)-> c c c c a c c a a a b a b (#2303) OC+OC at 5 OC: a b c b c --(6)-> c c c c a a b c a a b (#318) OC+OC at 2 OC: a b c b c --(4)-> c c a b c c a a b (#15) OC+OC at 4 OC: a b c --(2)-> c c a b a (#4) OC+OC at 3 OC: a b c --(1)-> c c a a a a (#2) Rule OC: a a --(1)-> b (#1) Rule OC: a b c --(2)-> c c a a b (#5) OC+OC at 4 OC: a b c --(1)-> c c a a a a (#2) Rule OC: a a --(1)-> b (#1) Rule OC: a b c --(2)-> c c a a b (#5) OC+OC at 4 OC: a b c --(1)-> c c a a a a (#2) Rule OC: a a --(1)-> b (#1) Rule OC: a b c a --(2)-> c c a a a b (#6) OC+OC at 5 OC: a b c --(1)-> c c a a a a (#2) Rule OC: a a --(1)-> b (#1) Rule OC: a b c --(1)-> c c a a a a (#2) Rule OC: a a --(1)-> b (#1) Rule OC: a b c --(2)-> c c a a b (#5) OC+OC at 4 OC: a b c --(1)-> c c a a a a (#2) Rule OC: a a --(1)-> b (#1) Rule OC: a b c c --(5)-> c c a c c b b (#29) OC+OC at 6 OC: a b c c --(4)-> c c a c c b a a (#17) OC+OC at 3 OC: a b c --(2)-> c c a a b (#5) OC+OC at 4 OC: a b c --(1)-> c c a a a a (#2) Rule OC: a a --(1)-> b (#1) Rule OC: a b c --(2)-> c c b a a (#3) OC+OC at 2 OC: a b c --(1)-> c c a a a a (#2) Rule OC: a a --(1)-> b (#1) Rule OC: a a --(1)-> b (#1) Rule OC: a a --(1)-> b (#1) Rule Hence, the SRS is non-terminating.