======================================================== The given Problem was: 0 0 0 0 -> 0 1 0 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 1 0 0 --(21)-> 0 0 0 0 0 0 1 0 1 0 1 1 0 0 (#83125) OC+OC at 7 OC: 0 0 0 0 0 0 1 0 1 0 1 1 0 0 --(20)-> 0 0 0 0 0 0 1 0 0 0 0 1 0 0 (#58697) OC+OC at 9 OC: 0 0 0 0 0 0 1 0 1 0 1 1 0 0 --(19)-> 0 0 0 0 0 0 1 0 0 1 0 0 1 0 (#44730) OC+OC at 4 OC: 0 0 0 0 0 0 1 0 1 0 1 1 0 0 --(18)-> 0 0 0 0 1 0 0 1 0 1 0 0 1 0 (#35476) OC+OC at 10 OC: 0 0 0 0 0 0 1 0 1 0 1 1 0 0 --(17)-> 0 0 0 0 1 0 0 1 0 1 1 0 0 1 (#25100) OC+OC at 6 OC: 0 0 0 0 0 0 1 0 1 0 1 1 0 0 --(16)-> 0 0 0 0 1 0 0 0 0 0 1 0 0 1 (#19515) OC+OC at 8 OC: 0 0 0 0 0 0 1 0 1 0 1 1 0 0 --(15)-> 0 0 0 0 1 0 0 0 1 0 0 1 0 1 (#4718) OC+OC at 10 OC: 0 0 0 0 0 0 1 0 1 0 1 1 --(14)-> 0 0 0 0 1 0 0 0 1 0 0 0 (#3707) OC+OC at 6 OC: 0 0 0 0 0 0 1 0 1 0 1 1 --(13)-> 0 0 0 0 1 0 1 0 0 1 0 0 (#2569) OC+OC at 7 OC: 0 0 0 0 0 0 1 0 1 0 1 1 --(12)-> 0 0 0 0 1 0 1 1 0 0 1 0 (#2010) OC+OC at 3 OC: 0 0 0 0 0 0 1 0 1 0 1 1 --(11)-> 0 0 0 0 0 0 0 1 0 0 1 0 (#1481) OC+OC at 5 OC: 0 0 0 0 0 0 1 0 1 0 1 1 --(10)-> 0 0 0 0 0 1 0 0 1 0 1 0 (#1215) OC+OC at 3 OC: 0 0 0 0 0 0 1 0 1 0 1 1 --(9)-> 0 0 0 1 0 0 1 0 1 0 1 0 (#974) OC+OC at 1 OC: 0 0 0 0 0 0 1 0 1 0 1 1 --(8)-> 0 1 0 0 1 0 1 0 1 0 1 0 (#115) OC+OC at 3 OC: 0 0 0 0 --(1)-> 0 1 0 1 (#1) Rule OC: 1 0 0 1 0 1 0 1 1 --(7)-> 0 1 0 1 0 1 0 1 0 (#97) OC+OC at 2 OC: 1 0 0 1 0 1 0 1 1 --(6)-> 0 1 0 0 0 0 0 1 0 (#60) OC+OC at 5 OC: 1 0 0 1 0 1 0 1 --(5)-> 0 1 0 0 0 1 0 0 (#40) OC+OC at 3 OC: 1 0 0 1 0 1 0 1 --(4)-> 0 1 0 1 0 0 1 0 (#14) OC+OC at 4 OC: 1 0 0 1 0 1 --(3)-> 0 1 0 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 1 0 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 1 0 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 1 0 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: 0 0 0 0 --(1)-> 0 1 0 1 (#1) Rule OC: 1 0 0 1 --(1)-> 0 0 1 0 (#2) Rule OC: 0 0 0 0 --(1)-> 0 1 0 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 1 0 1 (#1) Rule Hence, the SRS is non-terminating.