======================================================== The given Problem was: a -> a b -> b a c b c b -> a c c -> ======================================================== A self-embedding rewrite structure for the given SRS is: b b c b --(11)-> b b c b c c (#7493) OC+OC at 1 OC: b b c b --(9)-> b a b c (#3078) OC+OC at 2 OC: b b c b --(8)-> b a c c b c (#1212) OC+OC at 0 OC: b --(1)-> a (#3) Rule OC: a b c b --(7)-> b a c c b c (#705) OC+OC at 3 OC: a b c --(2)-> b a c b (#13) OC+OC at 4 OC: a b --(1)-> b a c b c (#2) Rule OC: c c --(1)-> (#4) Rule OC: b b --(5)-> c b c (#29) OC+OC at 0 OC: b --(1)-> a (#3) Rule OC: a b --(4)-> c b c (#16) OC+OC at 0 OC: a b --(2)-> b c b c (#6) OC+OC at 1 OC: a b --(1)-> b a c b c (#2) Rule OC: a --(1)-> (#1) Rule OC: b --(2)-> (#5) OC+OC at 0 OC: b --(1)-> a (#3) Rule OC: a --(1)-> (#1) Rule OC: c c --(1)-> (#4) Rule OC: a b --(2)-> b c b c (#6) OC+OC at 1 OC: a b --(1)-> b a c b c (#2) Rule OC: a --(1)-> (#1) Rule Hence, the SRS is non-terminating.