======================================================== The given Problem was: a -> a b -> b c a a b c -> c c -> b ======================================================== A self-embedding rewrite structure for the given SRS is: a b b b b --(14)-> a b b b b a a (#48019) OC+OC at 2 OC: a b b b b --(13)-> a b c c b b a a (#22514) OC+OC at 3 OC: a b b b b --(12)-> a b c a c b b a a (#16671) OC+OC at 1 OC: a b --(2)-> a a (#8) OC+OC at 0 OC: a b --(1)-> b c a a (#2) Rule OC: b c --(1)-> (#3) Rule OC: a b b b --(10)-> b c a c b b a a (#8041) OC+OC at 0 OC: a b b b --(8)-> a b c b b a a (#2260) OC+OC at 4 OC: a b b b --(7)-> a b c b c c a a (#1154) OC+OC at 5 OC: a b b b --(6)-> a b c b c a c a a (#764) OC+OC at 1 OC: a b --(2)-> a a (#8) OC+OC at 0 OC: a b --(1)-> b c a a (#2) Rule OC: b c --(1)-> (#3) Rule OC: a b b --(4)-> b c b c a c a a (#355) OC+OC at 2 OC: a b b --(2)-> b c a b c a a (#39) OC+OC at 3 OC: a b --(1)-> b c a a (#2) Rule OC: a b --(1)-> b c a a (#2) Rule OC: a b --(2)-> b c a (#6) OC+OC at 2 OC: a b --(1)-> b c a a (#2) Rule OC: a --(1)-> (#1) Rule OC: a --(1)-> (#1) Rule OC: c c --(1)-> b (#4) Rule OC: a b --(2)-> b c a (#6) OC+OC at 2 OC: a b --(1)-> b c a a (#2) Rule OC: a --(1)-> (#1) Rule OC: a --(1)-> (#1) Rule OC: c c --(1)-> b (#4) Rule Hence, the SRS is non-terminating.