======================================================== The given Problem was: a a b -> b c b a a a a c -> ======================================================== A self-embedding rewrite structure for the given SRS is: a a b a b c b b c b --(12)-> b c b b c b b c b a b c b a a b a b c b b c b a a a (#65546) OC+OC at 20 OC: a a b a b c b b c --(11)-> b c b b c b b c b a b c b a a b a b c b a a (#13007) OC+OC at 17 OC: a a b a b c b --(9)-> b c b b c b b c b a b c b a a b a a a (#5732) OC+OC at 10 OC: a a b a b c b --(7)-> b c b b c b b c b a a a b c b a a a (#850) OC+OC at 12 OC: a a b a b c --(6)-> b c b b c b b c b a a a a a (#275) OC+OC at 6 OC: a a b a b c --(5)-> b c b b c b a a b a a (#155) OC+OC at 3 OC: a a b a b c --(3)-> b c b a a b c b a a (#9) 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 (#3) OC+OC at 5 OC: a a b --(1)-> b c b a a a (#1) Rule OC: a c --(1)-> (#2) Rule OC: a a b c --(2)-> b c b a a (#3) OC+OC at 5 OC: a a b --(1)-> b c b a a a (#1) Rule OC: a c --(1)-> (#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 c --(2)-> b c b a a (#3) OC+OC at 5 OC: a a b --(1)-> b c b a a a (#1) Rule OC: a c --(1)-> (#2) Rule OC: a a b c --(2)-> b c b a a (#3) OC+OC at 5 OC: a a b --(1)-> b c b a a a (#1) Rule OC: a c --(1)-> (#2) Rule OC: a a b --(1)-> b c b a a a (#1) Rule Hence, the SRS is non-terminating.