======================================================== The given Problem was: 0 0 0 0 -> 0 1 1 1 1 1 0 1 -> 0 1 1 0 ======================================================== A self-embedding rewrite structure for the given SRS is: 0 0 0 0 1 0 1 0 0 1 1 0 0 --(20)-> 0 0 0 0 1 0 1 0 0 1 1 0 0 (#292488) OC+OC at 8 OC: 0 0 0 0 1 0 1 0 0 1 1 0 0 --(19)-> 0 0 0 0 1 0 1 0 1 1 0 1 0 (#226694) OC+OC at 7 OC: 0 0 0 0 1 0 1 0 0 1 1 0 0 --(18)-> 0 0 0 0 1 0 1 1 1 0 1 1 0 (#158781) OC+OC at 5 OC: 0 0 0 0 1 0 1 0 0 1 1 0 0 --(17)-> 0 0 0 0 1 0 0 0 0 0 1 1 0 (#120752) OC+OC at 9 OC: 0 0 0 0 1 0 1 0 0 1 1 0 0 --(16)-> 0 0 0 0 1 0 0 0 0 1 1 0 1 (#87764) OC+OC at 8 OC: 0 0 0 0 1 0 1 0 0 1 1 0 0 --(15)-> 0 0 0 0 1 0 0 0 1 1 0 1 1 (#61478) OC+OC at 7 OC: 0 0 0 0 1 0 1 0 0 1 1 0 0 --(14)-> 0 0 0 0 1 0 0 1 1 0 1 1 1 (#12487) OC+OC at 9 OC: 0 0 0 0 1 0 1 0 0 1 1 --(13)-> 0 0 0 0 1 0 0 1 1 0 0 (#9232) OC+OC at 6 OC: 0 0 0 0 1 0 1 0 0 1 1 --(12)-> 0 0 0 0 1 0 1 1 0 1 0 (#6691) OC+OC at 5 OC: 0 0 0 0 1 0 1 0 0 1 1 --(11)-> 0 0 0 0 1 1 1 0 1 1 0 (#2715) OC+OC at 7 OC: 0 0 0 0 1 0 1 0 0 1 --(10)-> 0 0 0 0 1 1 1 1 1 0 (#2002) OC+OC at 3 OC: 0 0 0 0 1 0 1 0 0 1 --(9)-> 0 0 0 0 0 0 0 1 1 0 (#776) OC+OC at 6 OC: 0 0 0 0 1 0 1 0 0 --(8)-> 0 0 0 0 0 0 1 1 0 (#577) OC+OC at 5 OC: 0 0 0 0 1 0 1 0 0 --(7)-> 0 0 0 0 0 1 1 0 1 (#401) OC+OC at 4 OC: 0 0 0 0 1 0 1 0 0 --(6)-> 0 0 0 0 1 1 0 1 1 (#275) OC+OC at 3 OC: 0 0 0 0 1 0 1 0 0 --(5)-> 0 0 0 1 1 0 1 1 1 (#54) OC+OC at 5 OC: 0 0 0 0 1 0 1 --(4)-> 0 0 0 1 1 0 0 (#40) OC+OC at 2 OC: 0 0 0 0 1 0 1 --(3)-> 0 0 1 1 0 1 0 (#28) OC+OC at 1 OC: 0 0 0 0 1 0 1 --(2)-> 0 1 1 0 1 1 0 (#6) OC+OC at 3 OC: 0 0 0 0 --(1)-> 0 1 1 1 (#1) Rule OC: 1 1 0 1 --(1)-> 0 1 1 0 (#2) Rule OC: 1 1 0 1 --(1)-> 0 1 1 0 (#2) Rule OC: 1 1 0 1 --(1)-> 0 1 1 0 (#2) Rule OC: 0 0 0 0 --(1)-> 0 1 1 1 (#1) Rule OC: 1 1 0 1 --(1)-> 0 1 1 0 (#2) Rule OC: 1 1 0 1 --(1)-> 0 1 1 0 (#2) Rule OC: 1 1 0 1 --(1)-> 0 1 1 0 (#2) Rule OC: 1 1 0 1 --(1)-> 0 1 1 0 (#2) Rule OC: 0 0 0 0 --(1)-> 0 1 1 1 (#1) Rule OC: 1 1 0 1 --(1)-> 0 1 1 0 (#2) Rule OC: 1 1 0 1 --(1)-> 0 1 1 0 (#2) Rule OC: 1 1 0 1 --(1)-> 0 1 1 0 (#2) Rule OC: 0 0 0 0 --(1)-> 0 1 1 1 (#1) Rule OC: 1 1 0 1 --(1)-> 0 1 1 0 (#2) Rule OC: 1 1 0 1 --(1)-> 0 1 1 0 (#2) Rule OC: 1 1 0 1 --(1)-> 0 1 1 0 (#2) Rule OC: 0 0 0 0 --(1)-> 0 1 1 1 (#1) Rule OC: 1 1 0 1 --(1)-> 0 1 1 0 (#2) Rule OC: 1 1 0 1 --(1)-> 0 1 1 0 (#2) Rule Hence, the SRS is non-terminating.