======================================================== The given Problem was: 0 0 0 0 -> 0 1 1 1 1 0 1 1 -> 0 0 1 0 ======================================================== A self-embedding rewrite structure for the given SRS is: 0 0 0 0 0 1 1 1 1 0 1 --(25)-> 0 0 0 0 0 1 1 1 1 0 1 (#121197) OC+OC at 4 OC: 0 0 0 0 0 1 1 1 1 0 1 --(24)-> 0 0 0 0 0 0 0 0 1 0 1 (#91121) OC+OC at 6 OC: 0 0 0 0 0 1 1 1 1 0 1 --(23)-> 0 0 0 0 0 0 1 0 1 1 1 (#65655) OC+OC at 7 OC: 0 0 0 0 0 1 1 1 1 0 1 --(22)-> 0 0 0 0 0 0 1 0 0 0 0 (#47041) OC+OC at 4 OC: 0 0 0 0 0 1 1 1 1 0 1 --(21)-> 0 0 0 0 1 0 1 1 0 0 0 (#35212) OC+OC at 2 OC: 0 0 0 0 0 1 1 1 1 0 1 --(20)-> 0 0 1 0 1 1 1 1 0 0 0 (#27091) OC+OC at 3 OC: 0 0 0 0 0 1 1 1 1 0 1 --(19)-> 0 0 1 0 0 0 0 1 0 0 0 (#19211) OC+OC at 5 OC: 0 0 0 0 0 1 1 1 1 0 1 --(18)-> 0 0 1 0 0 1 0 1 1 0 0 (#15152) OC+OC at 3 OC: 0 0 0 0 0 1 1 1 1 0 1 --(17)-> 0 0 1 1 0 1 1 1 1 0 0 (#10809) OC+OC at 4 OC: 0 0 0 0 0 1 1 1 1 0 1 --(16)-> 0 0 1 1 0 0 0 0 1 0 0 (#8146) OC+OC at 6 OC: 0 0 0 0 0 1 1 1 1 0 1 --(15)-> 0 0 1 1 0 0 1 0 1 1 0 (#6386) OC+OC at 4 OC: 0 0 0 0 0 1 1 1 1 0 1 --(14)-> 0 0 1 1 1 0 1 1 1 1 0 (#4352) OC+OC at 1 OC: 0 0 0 0 0 1 1 1 1 0 1 --(13)-> 0 0 0 0 0 0 1 1 1 1 0 (#3443) OC+OC at 5 OC: 0 0 0 0 0 1 1 1 1 0 1 --(12)-> 0 0 0 0 0 0 0 0 0 1 0 (#1313) OC+OC at 7 OC: 0 0 0 0 0 1 1 1 1 0 --(11)-> 0 0 0 0 0 0 0 1 0 1 (#988) OC+OC at 5 OC: 0 0 0 0 0 1 1 1 1 0 --(10)-> 0 0 0 0 0 1 0 1 1 1 (#472) OC+OC at 6 OC: 0 0 0 0 0 1 1 1 1 --(9)-> 0 0 0 0 0 1 0 0 0 (#308) OC+OC at 3 OC: 0 0 0 0 0 1 1 1 1 --(8)-> 0 0 0 1 0 1 1 0 0 (#241) OC+OC at 1 OC: 0 0 0 0 0 1 1 1 1 --(7)-> 0 1 0 1 1 1 1 0 0 (#161) OC+OC at 2 OC: 0 0 0 0 0 1 1 1 1 --(6)-> 0 1 0 0 0 0 1 0 0 (#140) OC+OC at 4 OC: 0 0 0 0 0 1 1 1 1 --(5)-> 0 1 0 0 1 0 1 1 0 (#105) OC+OC at 2 OC: 0 0 0 0 0 1 1 1 1 --(4)-> 0 1 1 0 1 1 1 1 0 (#12) OC+OC at 3 OC: 0 0 0 0 --(1)-> 0 1 1 1 (#1) Rule OC: 1 0 1 1 1 1 --(3)-> 0 1 1 1 1 0 (#9) OC+OC at 0 OC: 1 0 1 1 1 1 --(2)-> 0 0 0 0 1 0 (#3) OC+OC at 2 OC: 1 0 1 1 --(1)-> 0 0 1 0 (#2) Rule OC: 1 0 1 1 --(1)-> 0 0 1 0 (#2) Rule OC: 0 0 0 0 --(1)-> 0 1 1 1 (#1) Rule OC: 1 0 1 1 --(1)-> 0 0 1 0 (#2) Rule OC: 1 0 1 1 --(1)-> 0 0 1 0 (#2) Rule OC: 0 0 0 0 --(1)-> 0 1 1 1 (#1) Rule OC: 1 0 1 1 --(1)-> 0 0 1 0 (#2) Rule OC: 1 0 1 1 --(1)-> 0 0 1 0 (#2) Rule OC: 0 0 0 0 --(1)-> 0 1 1 1 (#1) Rule OC: 1 0 1 1 --(1)-> 0 0 1 0 (#2) Rule OC: 1 0 1 1 --(1)-> 0 0 1 0 (#2) Rule OC: 0 0 0 0 --(1)-> 0 1 1 1 (#1) Rule OC: 0 0 0 0 --(1)-> 0 1 1 1 (#1) Rule OC: 1 0 1 1 --(1)-> 0 0 1 0 (#2) Rule OC: 1 0 1 1 --(1)-> 0 0 1 0 (#2) Rule OC: 0 0 0 0 --(1)-> 0 1 1 1 (#1) Rule OC: 1 0 1 1 --(1)-> 0 0 1 0 (#2) Rule OC: 1 0 1 1 --(1)-> 0 0 1 0 (#2) Rule OC: 0 0 0 0 --(1)-> 0 1 1 1 (#1) Rule OC: 1 0 1 1 --(1)-> 0 0 1 0 (#2) Rule OC: 1 0 1 1 --(1)-> 0 0 1 0 (#2) Rule OC: 0 0 0 0 --(1)-> 0 1 1 1 (#1) Rule OC: 1 0 1 1 --(1)-> 0 0 1 0 (#2) Rule OC: 0 0 0 0 --(1)-> 0 1 1 1 (#1) Rule Hence, the SRS is non-terminating.