======================================================== The given Problem was: a -> a b -> b c b a b -> a c c -> ======================================================== A self-embedding rewrite structure for the given SRS is: b b b c b --(14)-> b b b c b (#111291) OC+OC at 1 OC: b b b c b --(13)-> b c c b b c b (#45165) OC+OC at 0 OC: b --(1)-> a (#3) Rule OC: a b b c b --(12)-> b c c b b c b (#34224) OC+OC at 4 OC: a b b c --(10)-> b c c b a (#7665) OC+OC at 2 OC: a b b c --(6)-> b c b b (#185) OC+OC at 3 OC: a b --(1)-> b c b a (#2) Rule OC: a b c --(5)-> b (#54) OC+OC at 1 OC: a b --(4)-> b c (#16) OC+OC at 2 OC: a b --(2)-> b c b (#6) OC+OC at 3 OC: a b --(1)-> b c b a (#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: b b --(4)-> c b a (#26) OC+OC at 0 OC: b --(1)-> a (#3) Rule OC: a b --(3)-> c b a (#11) OC+OC at 0 OC: a b --(1)-> b c b a (#2) Rule OC: b --(2)-> (#5) OC+OC at 0 OC: b --(1)-> a (#3) Rule OC: a --(1)-> (#1) Rule OC: a b --(2)-> b c b (#6) OC+OC at 3 OC: a b --(1)-> b c b a (#2) Rule OC: a --(1)-> (#1) Rule OC: c c --(1)-> (#4) Rule Hence, the SRS is non-terminating.