======================================================== The given Problem was: a -> a b -> b a a c b a b -> c c -> ======================================================== A self-embedding rewrite structure for the given SRS is: a b b b c b b --(17)-> b a a b b b c b b a a c b (#650596) OC+OC at 6 OC: a b b b c b b --(16)-> b a a b b b a c b b a a c b (#217585) OC+OC at 9 OC: a b b b c b --(14)-> b a a b b b a c b a (#21334) OC+OC at 5 OC: a b b b c b --(13)-> b a a b b a b a c b a (#9979) OC+OC at 6 OC: a b b b c --(11)-> b a a b b a a (#4325) OC+OC at 3 OC: a b b b c --(10)-> b a a c c b b a a (#3474) OC+OC at 4 OC: a b b b c --(9)-> b a a c a c b b a a (#3124) OC+OC at 4 OC: a b --(2)-> b a a c a (#9) OC+OC at 4 OC: a b --(1)-> b a a c b a (#2) Rule OC: b --(1)-> (#3) Rule OC: a b b c --(7)-> a c b b a a (#191) OC+OC at 0 OC: a b b c --(6)-> b a c b b a a (#174) OC+OC at 7 OC: a b b --(5)-> b a c b b a a c (#153) OC+OC at 8 OC: a b b --(4)-> b a c b b a a c a (#18) OC+OC at 4 OC: a b --(2)-> b a c b a (#5) OC+OC at 1 OC: a b --(1)-> b a a c b a (#2) Rule OC: a --(1)-> (#1) Rule OC: a b --(2)-> b a a c a (#9) OC+OC at 4 OC: a b --(1)-> b a a c b a (#2) Rule OC: b --(1)-> (#3) Rule OC: a --(1)-> (#1) Rule OC: c c --(1)-> (#4) Rule OC: b --(1)-> (#3) Rule OC: a --(1)-> (#1) Rule OC: c c --(1)-> (#4) Rule OC: a b --(2)-> b a c b a (#5) OC+OC at 1 OC: a b --(1)-> b a a c b a (#2) Rule OC: a --(1)-> (#1) Rule OC: a --(1)-> (#1) Rule OC: a b --(2)-> b a a c b (#7) OC+OC at 5 OC: a b --(1)-> b a a c b a (#2) Rule OC: a --(1)-> (#1) Rule OC: a --(1)-> (#1) Rule Hence, the SRS is non-terminating.