======================================================== The given Problem was: a -> a b -> b a c a c b -> c c -> b ======================================================== A self-embedding rewrite structure for the given SRS is: a b b c b b c --(17)-> b b a b b c b b c a (#381431) OC+OC at 8 OC: a b b c b b c --(16)-> b b a b b c b b a c a (#296222) OC+OC at 4 OC: a b b c --(10)-> b b a b a (#1281) OC+OC at 3 OC: a b b c --(9)-> b b a c c a (#1239) OC+OC at 1 OC: a b b c --(7)-> b a b c a (#397) OC+OC at 2 OC: a b b c --(5)-> b a a b (#90) OC+OC at 2 OC: a b b c --(4)-> b a c b a b (#55) OC+OC at 3 OC: a b --(1)-> b a c a (#2) Rule OC: a b c --(3)-> b a b (#9) OC+OC at 2 OC: a b --(2)-> b a c (#6) OC+OC at 3 OC: a b --(1)-> b a c a (#2) Rule OC: a --(1)-> (#1) Rule OC: c c --(1)-> b (#4) Rule OC: c b --(1)-> (#3) Rule OC: a b --(2)-> b c a (#5) OC+OC at 1 OC: a b --(1)-> b a c a (#2) Rule OC: a --(1)-> (#1) Rule OC: a b --(2)-> b a c (#6) OC+OC at 3 OC: a b --(1)-> b a c a (#2) Rule OC: a --(1)-> (#1) Rule OC: c c --(1)-> b (#4) Rule OC: a b b c --(6)-> b c b b a c a (#167) OC+OC at 2 OC: a b --(2)-> b c a (#5) OC+OC at 1 OC: a b --(1)-> b a c a (#2) Rule OC: a --(1)-> (#1) Rule OC: a b c --(4)-> b b a c a (#61) OC+OC at 1 OC: a b c --(3)-> b a b (#9) OC+OC at 2 OC: a b --(2)-> b a c (#6) OC+OC at 3 OC: a b --(1)-> b a c a (#2) Rule OC: a --(1)-> (#1) Rule OC: c c --(1)-> b (#4) Rule OC: a b --(1)-> b a c a (#2) Rule OC: a --(1)-> (#1) Rule Hence, the SRS is non-terminating.