======================================================== The given Problem was: a a b -> b c b a a a a c -> b ======================================================== A self-embedding rewrite structure for the given SRS is: a a b a b c b --(12)-> b c b b c b b c b a b c b a b c b b c b a a a b a b c b a a a (#21737) OC+OC at 25 OC: a a b a b c --(11)-> b c b b c b b c b a b c b a b c b b c b a a a b a a a (#8036) OC+OC at 17 OC: a a b a b c --(10)-> b c b b c b b c b a b c b a b c b a a b b a a a (#4867) OC+OC at 14 OC: a a b a b c --(8)-> b c b b c b b c b a b c b a a a b c b a a a (#1218) OC+OC at 16 OC: a a b a b c --(7)-> b c b b c b b c b a b c b a a a a a b (#416) OC+OC at 10 OC: a a b a b c --(6)-> b c b b c b b c b a a a b a a b (#176) OC+OC at 6 OC: a a b a b c --(5)-> b c b b c b a a b b a a b (#78) OC+OC at 3 OC: a a b a b c --(3)-> b c b a a b c b a a b (#8) OC+OC at 5 OC: a a b --(1)-> b c b a a a (#1) Rule OC: a a b c --(2)-> b c b a a b (#3) OC+OC at 5 OC: a a b --(1)-> b c b a a a (#1) Rule OC: a c --(1)-> b (#2) Rule OC: a a b c --(2)-> b c b a a b (#3) OC+OC at 5 OC: a a b --(1)-> b c b a a a (#1) Rule OC: a c --(1)-> b (#2) Rule OC: a a b --(1)-> b c b a a a (#1) Rule OC: a a b --(1)-> b c b a a a (#1) Rule OC: a a b --(1)-> b c b a a a (#1) Rule OC: a a b c --(2)-> b c b a a b (#3) OC+OC at 5 OC: a a b --(1)-> b c b a a a (#1) Rule OC: a c --(1)-> b (#2) Rule OC: a a b --(1)-> b c b a a a (#1) Rule OC: a a b --(1)-> b c b a a a (#1) Rule Hence, the SRS is non-terminating.