======================================================== The given Problem was: a -> b a a b c -> b c c a a a ======================================================== A self-embedding rewrite structure for the given SRS is: a a b c a b c c b c c --(12)-> b c c b c c b c c a b c c a a b c a b c c b c c a a a (#673815) OC+OC at 18 OC: a a b c a b c c --(9)-> b c c b c c b c c a b c c a a b c a a a (#41656) OC+OC at 10 OC: a a b c a b c c --(7)-> b c c b c c b c c a a a b c c a a a (#6534) OC+OC at 12 OC: a a b c a b c --(6)-> b c c b c c b c c a a a a a b (#2172) OC+OC at 6 OC: a a b c a b c --(5)-> b c c b c c a a b c a a b (#924) OC+OC at 3 OC: a a b c a b c --(3)-> b c c a a b c c a a b (#20) OC+OC at 5 OC: a a b c --(1)-> b c c a a a (#2) Rule OC: a a b c --(2)-> b c c a a b (#5) OC+OC at 5 OC: a a b c --(1)-> b c c a a a (#2) Rule OC: a --(1)-> b (#1) Rule OC: a a b c --(2)-> b c c a a b (#5) OC+OC at 5 OC: a a b c --(1)-> b c c a a a (#2) Rule OC: a --(1)-> b (#1) Rule OC: a a b c --(1)-> b c c a a a (#2) Rule OC: a a b c --(1)-> b c c a a a (#2) Rule OC: a a b c --(2)-> b c c a a b (#5) OC+OC at 5 OC: a a b c --(1)-> b c c a a a (#2) Rule OC: a --(1)-> b (#1) Rule OC: a a b c c --(3)-> b c c b c c a a a (#25) OC+OC at 3 OC: a a b c --(2)-> b c c a a b (#5) OC+OC at 5 OC: a a b c --(1)-> b c c a a a (#2) Rule OC: a --(1)-> b (#1) Rule OC: a a b c --(1)-> b c c a a a (#2) Rule Hence, the SRS is non-terminating.