======================================================== The given Problem was: 0 0 0 0 -> 0 0 1 1 1 0 0 1 -> 0 0 1 0 ======================================================== A self-embedding rewrite structure for the given SRS is: 0 0 0 0 0 0 1 0 1 0 1 0 --(15)-> 0 0 0 0 0 0 1 0 1 0 1 0 (#25177) OC+OC at 4 OC: 0 0 0 0 0 0 1 0 1 0 1 0 --(14)-> 0 0 0 0 1 0 0 1 1 0 1 0 (#18862) OC+OC at 5 OC: 0 0 0 0 0 0 1 0 1 0 1 0 --(13)-> 0 0 0 0 1 0 0 0 0 0 1 0 (#13310) OC+OC at 2 OC: 0 0 0 0 0 0 1 0 1 0 1 0 --(12)-> 0 0 1 0 0 1 0 0 0 0 1 0 (#1012) OC+OC at 3 OC: 0 0 0 0 --(1)-> 0 0 1 1 (#1) Rule OC: 1 0 0 1 0 1 0 1 0 --(11)-> 0 0 1 0 0 0 0 1 0 (#935) OC+OC at 5 OC: 1 0 0 1 0 1 0 1 0 --(10)-> 0 0 1 0 0 1 0 0 1 (#712) OC+OC at 3 OC: 1 0 0 1 0 1 0 1 0 --(9)-> 0 0 1 1 0 0 1 0 1 (#504) OC+OC at 0 OC: 1 0 0 1 0 1 0 1 0 --(8)-> 0 0 0 0 0 0 1 0 1 (#323) OC+OC at 4 OC: 1 0 0 1 0 1 0 1 0 --(7)-> 0 0 0 0 1 0 0 1 1 (#128) OC+OC at 5 OC: 1 0 0 1 0 1 0 1 --(6)-> 0 0 0 0 1 0 0 0 (#98) OC+OC at 2 OC: 1 0 0 1 0 1 0 1 --(5)-> 0 0 1 0 0 1 0 0 (#67) OC+OC at 3 OC: 1 0 0 1 0 1 0 1 --(4)-> 0 0 1 1 0 0 1 0 (#14) OC+OC at 4 OC: 1 0 0 1 0 1 --(3)-> 0 0 1 1 1 0 (#8) OC+OC at 0 OC: 1 0 0 1 0 1 --(2)-> 0 0 0 0 1 0 (#5) OC+OC at 2 OC: 1 0 0 1 --(1)-> 0 0 1 0 (#2) Rule OC: 1 0 0 1 --(1)-> 0 0 1 0 (#2) Rule OC: 0 0 0 0 --(1)-> 0 0 1 1 (#1) Rule OC: 1 0 0 1 --(1)-> 0 0 1 0 (#2) Rule OC: 1 0 0 1 --(1)-> 0 0 1 0 (#2) Rule OC: 1 0 0 1 --(1)-> 0 0 1 0 (#2) Rule OC: 0 0 0 0 --(1)-> 0 0 1 1 (#1) Rule OC: 1 0 0 1 --(1)-> 0 0 1 0 (#2) Rule OC: 0 0 0 0 --(1)-> 0 0 1 1 (#1) Rule OC: 1 0 0 1 --(1)-> 0 0 1 0 (#2) Rule OC: 1 0 0 1 --(1)-> 0 0 1 0 (#2) Rule OC: 1 0 0 1 --(1)-> 0 0 1 0 (#2) Rule OC: 0 0 0 0 --(1)-> 0 0 1 1 (#1) Rule OC: 1 0 0 1 --(1)-> 0 0 1 0 (#2) Rule Hence, the SRS is non-terminating.