======================================================== The given Problem was: a -> a a a -> b b c -> a c c b c -> ======================================================== A self-embedding rewrite structure for the given SRS is: b c c c c --(10)-> b c c c c b (#1427) OC+OC at 3 OC: b c c c c --(9)-> b c c a c c b (#1391) OC+OC at 3 OC: b c c c --(8)-> b c c b (#906) OC+OC at 0 OC: b c c c --(7)-> a a a c c b (#335) OC+OC at 2 OC: b c c c --(6)-> a a c a c c b (#241) OC+OC at 3 OC: b c c --(5)-> a a c b (#63) OC+OC at 1 OC: b c c --(4)-> a c a c b (#18) OC+OC at 2 OC: b c --(2)-> a c b (#6) OC+OC at 1 OC: b c --(1)-> a c c b (#3) Rule OC: c --(1)-> (#4) Rule OC: b c --(2)-> a c b (#6) OC+OC at 1 OC: b c --(1)-> a c c b (#3) Rule OC: c --(1)-> (#4) Rule OC: c --(1)-> (#4) Rule OC: b c --(1)-> a c c b (#3) Rule OC: c --(1)-> (#4) Rule OC: a a a --(1)-> b (#2) Rule OC: b c --(1)-> a c c b (#3) Rule OC: a --(1)-> (#1) Rule Hence, the SRS is non-terminating.