======================================================== The given Problem was: a -> a a -> b a b c c -> c b -> a c ======================================================== A self-embedding rewrite structure for the given SRS is: c b b b b b a b --(19)-> b b c b b b b b a b c c (#4339105) OC+OC at 4 OC: c b b b b b a b --(18)-> b b c b a b b b b a b c c (#3139690) OC+OC at 3 OC: c b b --(4)-> b b c c (#123) OC+OC at 0 OC: c b b --(2)-> a a c (#9) OC+OC at 1 OC: c b --(1)-> a c (#4) Rule OC: c b --(1)-> a c (#4) Rule OC: a a --(2)-> b b c (#7) OC+OC at 1 OC: a a --(1)-> b a b c (#2) Rule OC: a --(1)-> (#1) Rule OC: c b b b a b --(14)-> b a b b b b a b c c (#247933) OC+OC at 5 OC: c b b b a --(11)-> b a b b b c b (#18711) OC+OC at 3 OC: c b b b a --(9)-> b a b a a b (#5737) OC+OC at 3 OC: c b b b a --(7)-> b a b c b a b (#1606) OC+OC at 4 OC: c b b --(3)-> b a b c c (#122) OC+OC at 0 OC: c b b --(2)-> a a c (#9) OC+OC at 1 OC: c b --(1)-> a c (#4) Rule OC: c b --(1)-> a c (#4) Rule OC: a a --(1)-> b a b c (#2) Rule OC: c b a --(4)-> b a b (#26) OC+OC at 0 OC: c b --(2)-> a (#6) OC+OC at 1 OC: c b --(1)-> a c (#4) Rule OC: c --(1)-> (#3) Rule OC: a a --(2)-> b a b (#8) OC+OC at 3 OC: a a --(1)-> b a b c (#2) Rule OC: c --(1)-> (#3) Rule OC: c b --(2)-> a (#6) OC+OC at 1 OC: c b --(1)-> a c (#4) Rule OC: c --(1)-> (#3) Rule OC: a a --(2)-> b b c (#7) OC+OC at 1 OC: a a --(1)-> b a b c (#2) Rule OC: a --(1)-> (#1) Rule OC: c b b --(3)-> b a b c c (#122) OC+OC at 0 OC: c b b --(2)-> a a c (#9) OC+OC at 1 OC: c b --(1)-> a c (#4) Rule OC: c b --(1)-> a c (#4) Rule OC: a a --(1)-> b a b c (#2) Rule OC: a --(1)-> (#1) Rule Hence, the SRS is non-terminating.