----- Otter 3.1-b0, May 2000 ----- ----> UNIT CONFLICT at 0.29 sec ----> 445 [binary,444.1,5.1] $Ans(One_b). Length of proof is 9. Level of proof is 7. ---------------- PROOF ---------------- 5 [] or(not(X),X)!=or(not(Y),Y)|$Ans(One_b). 15 [] or(not(or(not(or(x,y)),not(z))),not(or(not(or(not(u),u)),or(not(z),x))))=z. 17 [para_into,15.1.1.1.1.1.1,15.1.1] or(not(or(not(x),not(y))),not(or(not(or(not(z),z)),or(not(y),not(or(not(or(u,v)),not(x)))))))=y. 21 [para_into,15.1.1.2.1.2,15.1.1] or(not(or(not(or(not(or(not(or(not(x),x)),or(not(y),z))),u)),not(or(not(or(z,v)),not(y))))),not(or(not(or(not(w),w)),y)))=or(not(or(z,v)),not(y)). 27 [para_into,17.1.1.2.1.2.2.1.1.1,17.1.1] or(not(or(not(x),not(y))),not(or(not(or(not(z),z)),or(not(y),not(or(not(u),not(x)))))))=y. 177 [para_into,21.1.1.1.1,21.1.1] or(not(or(not(or(not(x),y)),not(not(x)))),not(or(not(or(not(z),z)),x)))=or(not(or(not(u),u)),not(x)). 206 [para_into,177.1.1,177.1.1] or(not(or(not(x),x)),not(y))=or(not(or(not(z),z)),not(y)). 240 [para_into,206.1.1,27.1.1,flip.1] or(not(or(not(x),x)),not(or(not(or(not(y),y)),or(not(z),not(or(not(u),not(not(z))))))))=z. 388 [para_from,240.1.1,15.1.1.1.1.1.1] or(not(or(not(x),not(y))),not(or(not(or(not(z),z)),or(not(y),not(or(not(u),u))))))=y. 420,419 [para_into,388.1.1,206.1.1] or(not(or(not(x),x)),not(or(not(or(not(y),y)),or(not(z),not(or(not(u),u))))))=z. 444 [para_into,419.1.1.2.1.2,206.1.1,demod,420] or(not(x),x)=or(not(y),y). 445 [binary,444.1,5.1] $Ans(One_b). ------------ end of proof ------------- ----> UNIT CONFLICT at 7.03 sec ----> 4890 [binary,4888.1,4171.1] $Ans(Meredith_1b). Length of proof is 36. Level of proof is 15. ---------------- PROOF ---------------- 13 [] or(not(or(not(X),X)),Y)!=Y|$Ans(Meredith_1b). 15 [] or(not(or(not(or(x,y)),not(z))),not(or(not(or(not(u),u)),or(not(z),x))))=z. 17 [para_into,15.1.1.1.1.1.1,15.1.1] or(not(or(not(x),not(y))),not(or(not(or(not(z),z)),or(not(y),not(or(not(or(u,v)),not(x)))))))=y. 19 [para_into,15.1.1.1.1,15.1.1] or(not(x),not(or(not(or(not(y),y)),or(not(or(not(or(not(z),z)),or(not(x),u))),not(or(u,v))))))=or(not(or(not(z),z)),or(not(x),u)). 21 [para_into,15.1.1.2.1.2,15.1.1] or(not(or(not(or(not(or(not(or(not(x),x)),or(not(y),z))),u)),not(or(not(or(z,v)),not(y))))),not(or(not(or(not(w),w)),y)))=or(not(or(z,v)),not(y)). 27 [para_into,17.1.1.2.1.2.2.1.1.1,17.1.1] or(not(or(not(x),not(y))),not(or(not(or(not(z),z)),or(not(y),not(or(not(u),not(x)))))))=y. 32,31 [para_into,17.1.1.2.1.2.2.1,15.1.1] or(not(or(not(or(not(or(not(x),x)),or(not(y),z))),not(u))),not(or(not(or(not(v),v)),or(not(u),not(y)))))=u. 37 [para_from,27.1.1,15.1.1.2.1.2] or(not(or(not(or(not(or(not(or(not(x),x)),or(not(y),not(or(not(z),not(u)))))),v)),not(or(not(u),not(y))))),not(or(not(or(not(w),w)),y)))=or(not(u),not(y)). 57 [para_into,19.1.1.2.1.2.1.1.2,31.1.1,demod,32] or(not(or(not(or(not(or(not(x),x)),or(not(y),z))),not(u))),not(or(not(or(not(v),v)),or(not(or(not(or(not(w),w)),u)),not(or(not(or(not(or(not(v6),v6)),or(not(u),not(y)))),v7))))))=or(not(or(not(w),w)),u). 177 [para_into,21.1.1.1.1,21.1.1] or(not(or(not(or(not(x),y)),not(not(x)))),not(or(not(or(not(z),z)),x)))=or(not(or(not(u),u)),not(x)). 206 [para_into,177.1.1,177.1.1] or(not(or(not(x),x)),not(y))=or(not(or(not(z),z)),not(y)). 240 [para_into,206.1.1,27.1.1,flip.1] or(not(or(not(x),x)),not(or(not(or(not(y),y)),or(not(z),not(or(not(u),not(not(z))))))))=z. 388 [para_from,240.1.1,15.1.1.1.1.1.1] or(not(or(not(x),not(y))),not(or(not(or(not(z),z)),or(not(y),not(or(not(u),u))))))=y. 420,419 [para_into,388.1.1,206.1.1] or(not(or(not(x),x)),not(or(not(or(not(y),y)),or(not(z),not(or(not(u),u))))))=z. 444 [para_into,419.1.1.2.1.2,206.1.1,demod,420] or(not(x),x)=or(not(y),y). 446 [para_into,419.1.1.2.1.2,177.1.1,demod,420] or(not(x),x)=or(not(or(not(or(not(y),y)),z)),not(not(or(not(y),y)))). 459 [copy,446,flip.1] or(not(or(not(or(not(x),x)),y)),not(not(or(not(x),x))))=or(not(z),z). 557 [para_from,444.1.1,419.1.1.2.1] or(not(or(not(x),x)),not(or(not(y),y)))=not(or(not(z),z)). 599 [para_from,444.1.1,13.1.1.1.1] or(not(or(not(x),x)),Y)!=Y|$Ans(Meredith_1b). 652 [para_into,37.1.1.2.1,444.1.1] or(not(or(not(or(not(or(not(or(not(x),x)),or(not(or(not(y),y)),not(or(not(z),not(u)))))),v)),not(or(not(u),not(or(not(y),y)))))),not(or(not(w),w)))=or(not(u),not(or(not(y),y))). 660,659 [para_from,37.1.1,419.1.1.2.1.2,demod,420,flip.1] or(not(or(not(or(not(or(not(x),x)),or(not(or(not(y),y)),not(or(not(z),not(u)))))),v)),not(or(not(u),not(or(not(y),y)))))=u. 687 [back_demod,652,demod,660] or(not(x),not(or(not(y),y)))=or(not(x),not(or(not(z),z))). 688 [para_into,557.1.1,557.1.1] not(or(not(x),x))=not(or(not(y),y)). 1384 [para_from,687.1.1,688.1.1.1] not(or(not(not(or(not(x),x))),not(or(not(y),y))))=not(or(not(z),z)). 1387 [para_from,687.1.1,599.1.1.1.1] or(not(or(not(not(or(not(x),x))),not(or(not(y),y)))),Y)!=Y|$Ans(Meredith_1b). 2333 [para_from,1384.1.1,419.1.1.2.1.1.1.1] or(not(or(not(x),x)),not(or(not(or(not(or(not(y),y)),or(not(not(or(not(z),z))),not(or(not(u),u))))),or(not(v),not(or(not(w),w))))))=v. 2427 [para_from,1384.1.1,419.1.1.2.1.2.2.1.1] or(not(or(not(x),x)),not(or(not(or(not(y),y)),or(not(z),not(or(not(or(not(u),u)),or(not(not(or(not(v),v))),not(or(not(w),w)))))))))=z. 3093 [para_into,459.1.1.1.1,419.1.1] or(not(x),not(not(or(not(y),y))))=or(not(z),z). 3122 [copy,3093,flip.1] or(not(x),x)=or(not(y),not(not(or(not(z),z)))). 3330 [para_from,3093.1.1,15.1.1.1.1] or(not(or(not(x),x)),not(or(not(or(not(y),y)),or(not(not(or(not(z),z))),u))))=not(or(not(z),z)). 3354 [para_from,3122.1.1,1384.1.1.1] not(or(not(x),not(not(or(not(y),y)))))=not(or(not(z),z)). 3443,3442 [para_from,3122.1.1,31.1.1.2.1.2] or(not(or(not(or(not(or(not(x),x)),or(not(y),z))),not(not(y)))),not(or(not(or(not(u),u)),or(not(v),not(not(or(not(w),w)))))))=not(y). 3561 [copy,3354,flip.1] not(or(not(x),x))=not(or(not(y),not(not(or(not(z),z))))). 4171 [para_from,3561.1.1,1387.1.1.1.1.1.1.1.1] or(not(or(not(not(or(not(or(not(x),not(not(or(not(y),y))))),or(not(z),z)))),not(or(not(u),u)))),Y)!=Y|$Ans(Meredith_1b). 4585,4584 [para_into,57.1.1.2.1.2.2.1,557.1.1,demod,3443,flip.1] or(not(or(not(x),x)),not(y))=not(y). 4792,4791 [back_demod,3330,demod,4585] not(or(not(or(not(x),x)),or(not(not(or(not(y),y))),z)))=not(or(not(y),y)). 4877,4876 [back_demod,2427,demod,4792,4585] not(or(not(or(not(x),x)),or(not(y),not(or(not(z),z)))))=y. 4888 [back_demod,2333,demod,4877,4877] or(not(or(not(x),x)),y)=y. 4890 [binary,4888.1,4171.1] $Ans(Meredith_1b). ------------ end of proof ------------- ----> UNIT CONFLICT at 7.03 sec ----> 4891 [binary,4888.1,4167.1] $Ans(Meredith_1b). Length of proof is 36. Level of proof is 15. ---------------- PROOF ---------------- 13 [] or(not(or(not(X),X)),Y)!=Y|$Ans(Meredith_1b). 15 [] or(not(or(not(or(x,y)),not(z))),not(or(not(or(not(u),u)),or(not(z),x))))=z. 17 [para_into,15.1.1.1.1.1.1,15.1.1] or(not(or(not(x),not(y))),not(or(not(or(not(z),z)),or(not(y),not(or(not(or(u,v)),not(x)))))))=y. 19 [para_into,15.1.1.1.1,15.1.1] or(not(x),not(or(not(or(not(y),y)),or(not(or(not(or(not(z),z)),or(not(x),u))),not(or(u,v))))))=or(not(or(not(z),z)),or(not(x),u)). 21 [para_into,15.1.1.2.1.2,15.1.1] or(not(or(not(or(not(or(not(or(not(x),x)),or(not(y),z))),u)),not(or(not(or(z,v)),not(y))))),not(or(not(or(not(w),w)),y)))=or(not(or(z,v)),not(y)). 27 [para_into,17.1.1.2.1.2.2.1.1.1,17.1.1] or(not(or(not(x),not(y))),not(or(not(or(not(z),z)),or(not(y),not(or(not(u),not(x)))))))=y. 32,31 [para_into,17.1.1.2.1.2.2.1,15.1.1] or(not(or(not(or(not(or(not(x),x)),or(not(y),z))),not(u))),not(or(not(or(not(v),v)),or(not(u),not(y)))))=u. 37 [para_from,27.1.1,15.1.1.2.1.2] or(not(or(not(or(not(or(not(or(not(x),x)),or(not(y),not(or(not(z),not(u)))))),v)),not(or(not(u),not(y))))),not(or(not(or(not(w),w)),y)))=or(not(u),not(y)). 57 [para_into,19.1.1.2.1.2.1.1.2,31.1.1,demod,32] or(not(or(not(or(not(or(not(x),x)),or(not(y),z))),not(u))),not(or(not(or(not(v),v)),or(not(or(not(or(not(w),w)),u)),not(or(not(or(not(or(not(v6),v6)),or(not(u),not(y)))),v7))))))=or(not(or(not(w),w)),u). 177 [para_into,21.1.1.1.1,21.1.1] or(not(or(not(or(not(x),y)),not(not(x)))),not(or(not(or(not(z),z)),x)))=or(not(or(not(u),u)),not(x)). 206 [para_into,177.1.1,177.1.1] or(not(or(not(x),x)),not(y))=or(not(or(not(z),z)),not(y)). 240 [para_into,206.1.1,27.1.1,flip.1] or(not(or(not(x),x)),not(or(not(or(not(y),y)),or(not(z),not(or(not(u),not(not(z))))))))=z. 388 [para_from,240.1.1,15.1.1.1.1.1.1] or(not(or(not(x),not(y))),not(or(not(or(not(z),z)),or(not(y),not(or(not(u),u))))))=y. 420,419 [para_into,388.1.1,206.1.1] or(not(or(not(x),x)),not(or(not(or(not(y),y)),or(not(z),not(or(not(u),u))))))=z. 444 [para_into,419.1.1.2.1.2,206.1.1,demod,420] or(not(x),x)=or(not(y),y). 446 [para_into,419.1.1.2.1.2,177.1.1,demod,420] or(not(x),x)=or(not(or(not(or(not(y),y)),z)),not(not(or(not(y),y)))). 459 [copy,446,flip.1] or(not(or(not(or(not(x),x)),y)),not(not(or(not(x),x))))=or(not(z),z). 557 [para_from,444.1.1,419.1.1.2.1] or(not(or(not(x),x)),not(or(not(y),y)))=not(or(not(z),z)). 599 [para_from,444.1.1,13.1.1.1.1] or(not(or(not(x),x)),Y)!=Y|$Ans(Meredith_1b). 652 [para_into,37.1.1.2.1,444.1.1] or(not(or(not(or(not(or(not(or(not(x),x)),or(not(or(not(y),y)),not(or(not(z),not(u)))))),v)),not(or(not(u),not(or(not(y),y)))))),not(or(not(w),w)))=or(not(u),not(or(not(y),y))). 660,659 [para_from,37.1.1,419.1.1.2.1.2,demod,420,flip.1] or(not(or(not(or(not(or(not(x),x)),or(not(or(not(y),y)),not(or(not(z),not(u)))))),v)),not(or(not(u),not(or(not(y),y)))))=u. 687 [back_demod,652,demod,660] or(not(x),not(or(not(y),y)))=or(not(x),not(or(not(z),z))). 688 [para_into,557.1.1,557.1.1] not(or(not(x),x))=not(or(not(y),y)). 756 [para_from,688.1.1,599.1.1.1.1.1] or(not(or(not(or(not(x),x)),or(not(y),y))),Y)!=Y|$Ans(Meredith_1b). 1384 [para_from,687.1.1,688.1.1.1] not(or(not(not(or(not(x),x))),not(or(not(y),y))))=not(or(not(z),z)). 2333 [para_from,1384.1.1,419.1.1.2.1.1.1.1] or(not(or(not(x),x)),not(or(not(or(not(or(not(y),y)),or(not(not(or(not(z),z))),not(or(not(u),u))))),or(not(v),not(or(not(w),w))))))=v. 2427 [para_from,1384.1.1,419.1.1.2.1.2.2.1.1] or(not(or(not(x),x)),not(or(not(or(not(y),y)),or(not(z),not(or(not(or(not(u),u)),or(not(not(or(not(v),v))),not(or(not(w),w)))))))))=z. 3093 [para_into,459.1.1.1.1,419.1.1] or(not(x),not(not(or(not(y),y))))=or(not(z),z). 3122 [copy,3093,flip.1] or(not(x),x)=or(not(y),not(not(or(not(z),z)))). 3330 [para_from,3093.1.1,15.1.1.1.1] or(not(or(not(x),x)),not(or(not(or(not(y),y)),or(not(not(or(not(z),z))),u))))=not(or(not(z),z)). 3354 [para_from,3122.1.1,1384.1.1.1] not(or(not(x),not(not(or(not(y),y)))))=not(or(not(z),z)). 3443,3442 [para_from,3122.1.1,31.1.1.2.1.2] or(not(or(not(or(not(or(not(x),x)),or(not(y),z))),not(not(y)))),not(or(not(or(not(u),u)),or(not(v),not(not(or(not(w),w)))))))=not(y). 3561 [copy,3354,flip.1] not(or(not(x),x))=not(or(not(y),not(not(or(not(z),z))))). 4167 [para_from,3561.1.1,756.1.1.1.1.1.1.1] or(not(or(not(or(not(or(not(x),not(not(or(not(y),y))))),or(not(z),z))),or(not(u),u))),Y)!=Y|$Ans(Meredith_1b). 4585,4584 [para_into,57.1.1.2.1.2.2.1,557.1.1,demod,3443,flip.1] or(not(or(not(x),x)),not(y))=not(y). 4792,4791 [back_demod,3330,demod,4585] not(or(not(or(not(x),x)),or(not(not(or(not(y),y))),z)))=not(or(not(y),y)). 4877,4876 [back_demod,2427,demod,4792,4585] not(or(not(or(not(x),x)),or(not(y),not(or(not(z),z)))))=y. 4888 [back_demod,2333,demod,4877,4877] or(not(or(not(x),x)),y)=y. 4891 [binary,4888.1,4167.1] $Ans(Meredith_1b). ------------ end of proof ------------- ----> UNIT CONFLICT at 7.04 sec ----> 4892 [binary,4888.1,4110.1] $Ans(Meredith_1b). Length of proof is 37. Level of proof is 15. ---------------- PROOF ---------------- 13 [] or(not(or(not(X),X)),Y)!=Y|$Ans(Meredith_1b). 15 [] or(not(or(not(or(x,y)),not(z))),not(or(not(or(not(u),u)),or(not(z),x))))=z. 17 [para_into,15.1.1.1.1.1.1,15.1.1] or(not(or(not(x),not(y))),not(or(not(or(not(z),z)),or(not(y),not(or(not(or(u,v)),not(x)))))))=y. 19 [para_into,15.1.1.1.1,15.1.1] or(not(x),not(or(not(or(not(y),y)),or(not(or(not(or(not(z),z)),or(not(x),u))),not(or(u,v))))))=or(not(or(not(z),z)),or(not(x),u)). 21 [para_into,15.1.1.2.1.2,15.1.1] or(not(or(not(or(not(or(not(or(not(x),x)),or(not(y),z))),u)),not(or(not(or(z,v)),not(y))))),not(or(not(or(not(w),w)),y)))=or(not(or(z,v)),not(y)). 27 [para_into,17.1.1.2.1.2.2.1.1.1,17.1.1] or(not(or(not(x),not(y))),not(or(not(or(not(z),z)),or(not(y),not(or(not(u),not(x)))))))=y. 32,31 [para_into,17.1.1.2.1.2.2.1,15.1.1] or(not(or(not(or(not(or(not(x),x)),or(not(y),z))),not(u))),not(or(not(or(not(v),v)),or(not(u),not(y)))))=u. 37 [para_from,27.1.1,15.1.1.2.1.2] or(not(or(not(or(not(or(not(or(not(x),x)),or(not(y),not(or(not(z),not(u)))))),v)),not(or(not(u),not(y))))),not(or(not(or(not(w),w)),y)))=or(not(u),not(y)). 57 [para_into,19.1.1.2.1.2.1.1.2,31.1.1,demod,32] or(not(or(not(or(not(or(not(x),x)),or(not(y),z))),not(u))),not(or(not(or(not(v),v)),or(not(or(not(or(not(w),w)),u)),not(or(not(or(not(or(not(v6),v6)),or(not(u),not(y)))),v7))))))=or(not(or(not(w),w)),u). 177 [para_into,21.1.1.1.1,21.1.1] or(not(or(not(or(not(x),y)),not(not(x)))),not(or(not(or(not(z),z)),x)))=or(not(or(not(u),u)),not(x)). 206 [para_into,177.1.1,177.1.1] or(not(or(not(x),x)),not(y))=or(not(or(not(z),z)),not(y)). 240 [para_into,206.1.1,27.1.1,flip.1] or(not(or(not(x),x)),not(or(not(or(not(y),y)),or(not(z),not(or(not(u),not(not(z))))))))=z. 388 [para_from,240.1.1,15.1.1.1.1.1.1] or(not(or(not(x),not(y))),not(or(not(or(not(z),z)),or(not(y),not(or(not(u),u))))))=y. 420,419 [para_into,388.1.1,206.1.1] or(not(or(not(x),x)),not(or(not(or(not(y),y)),or(not(z),not(or(not(u),u))))))=z. 444 [para_into,419.1.1.2.1.2,206.1.1,demod,420] or(not(x),x)=or(not(y),y). 446 [para_into,419.1.1.2.1.2,177.1.1,demod,420] or(not(x),x)=or(not(or(not(or(not(y),y)),z)),not(not(or(not(y),y)))). 459 [copy,446,flip.1] or(not(or(not(or(not(x),x)),y)),not(not(or(not(x),x))))=or(not(z),z). 557 [para_from,444.1.1,419.1.1.2.1] or(not(or(not(x),x)),not(or(not(y),y)))=not(or(not(z),z)). 599 [para_from,444.1.1,13.1.1.1.1] or(not(or(not(x),x)),Y)!=Y|$Ans(Meredith_1b). 652 [para_into,37.1.1.2.1,444.1.1] or(not(or(not(or(not(or(not(or(not(x),x)),or(not(or(not(y),y)),not(or(not(z),not(u)))))),v)),not(or(not(u),not(or(not(y),y)))))),not(or(not(w),w)))=or(not(u),not(or(not(y),y))). 660,659 [para_from,37.1.1,419.1.1.2.1.2,demod,420,flip.1] or(not(or(not(or(not(or(not(x),x)),or(not(or(not(y),y)),not(or(not(z),not(u)))))),v)),not(or(not(u),not(or(not(y),y)))))=u. 687 [back_demod,652,demod,660] or(not(x),not(or(not(y),y)))=or(not(x),not(or(not(z),z))). 688 [para_into,557.1.1,557.1.1] not(or(not(x),x))=not(or(not(y),y)). 1384 [para_from,687.1.1,688.1.1.1] not(or(not(not(or(not(x),x))),not(or(not(y),y))))=not(or(not(z),z)). 1387 [para_from,687.1.1,599.1.1.1.1] or(not(or(not(not(or(not(x),x))),not(or(not(y),y)))),Y)!=Y|$Ans(Meredith_1b). 2333 [para_from,1384.1.1,419.1.1.2.1.1.1.1] or(not(or(not(x),x)),not(or(not(or(not(or(not(y),y)),or(not(not(or(not(z),z))),not(or(not(u),u))))),or(not(v),not(or(not(w),w))))))=v. 2427 [para_from,1384.1.1,419.1.1.2.1.2.2.1.1] or(not(or(not(x),x)),not(or(not(or(not(y),y)),or(not(z),not(or(not(or(not(u),u)),or(not(not(or(not(v),v))),not(or(not(w),w)))))))))=z. 3093 [para_into,459.1.1.1.1,419.1.1] or(not(x),not(not(or(not(y),y))))=or(not(z),z). 3122 [copy,3093,flip.1] or(not(x),x)=or(not(y),not(not(or(not(z),z)))). 3330 [para_from,3093.1.1,15.1.1.1.1] or(not(or(not(x),x)),not(or(not(or(not(y),y)),or(not(not(or(not(z),z))),u))))=not(or(not(z),z)). 3353 [para_from,3122.1.1,1387.1.1.1.1] or(not(or(not(x),not(not(or(not(y),y))))),Y)!=Y|$Ans(Meredith_1b). 3354 [para_from,3122.1.1,1384.1.1.1] not(or(not(x),not(not(or(not(y),y)))))=not(or(not(z),z)). 3443,3442 [para_from,3122.1.1,31.1.1.2.1.2] or(not(or(not(or(not(or(not(x),x)),or(not(y),z))),not(not(y)))),not(or(not(or(not(u),u)),or(not(v),not(not(or(not(w),w)))))))=not(y). 3561 [copy,3354,flip.1] not(or(not(x),x))=not(or(not(y),not(not(or(not(z),z))))). 4110 [para_from,3561.1.1,3353.1.1.1.1.2.1.1.1] or(not(or(not(x),not(not(or(not(or(not(y),not(not(or(not(z),z))))),or(not(u),u)))))),Y)!=Y|$Ans(Meredith_1b). 4585,4584 [para_into,57.1.1.2.1.2.2.1,557.1.1,demod,3443,flip.1] or(not(or(not(x),x)),not(y))=not(y). 4792,4791 [back_demod,3330,demod,4585] not(or(not(or(not(x),x)),or(not(not(or(not(y),y))),z)))=not(or(not(y),y)). 4877,4876 [back_demod,2427,demod,4792,4585] not(or(not(or(not(x),x)),or(not(y),not(or(not(z),z)))))=y. 4888 [back_demod,2333,demod,4877,4877] or(not(or(not(x),x)),y)=y. 4892 [binary,4888.1,4110.1] $Ans(Meredith_1b). ------------ end of proof ------------- ----> UNIT CONFLICT at 7.05 sec ----> 4893 [binary,4888.1,4100.1] $Ans(Meredith_1b). Length of proof is 36. Level of proof is 15. ---------------- PROOF ---------------- 13 [] or(not(or(not(X),X)),Y)!=Y|$Ans(Meredith_1b). 15 [] or(not(or(not(or(x,y)),not(z))),not(or(not(or(not(u),u)),or(not(z),x))))=z. 17 [para_into,15.1.1.1.1.1.1,15.1.1] or(not(or(not(x),not(y))),not(or(not(or(not(z),z)),or(not(y),not(or(not(or(u,v)),not(x)))))))=y. 19 [para_into,15.1.1.1.1,15.1.1] or(not(x),not(or(not(or(not(y),y)),or(not(or(not(or(not(z),z)),or(not(x),u))),not(or(u,v))))))=or(not(or(not(z),z)),or(not(x),u)). 21 [para_into,15.1.1.2.1.2,15.1.1] or(not(or(not(or(not(or(not(or(not(x),x)),or(not(y),z))),u)),not(or(not(or(z,v)),not(y))))),not(or(not(or(not(w),w)),y)))=or(not(or(z,v)),not(y)). 27 [para_into,17.1.1.2.1.2.2.1.1.1,17.1.1] or(not(or(not(x),not(y))),not(or(not(or(not(z),z)),or(not(y),not(or(not(u),not(x)))))))=y. 32,31 [para_into,17.1.1.2.1.2.2.1,15.1.1] or(not(or(not(or(not(or(not(x),x)),or(not(y),z))),not(u))),not(or(not(or(not(v),v)),or(not(u),not(y)))))=u. 37 [para_from,27.1.1,15.1.1.2.1.2] or(not(or(not(or(not(or(not(or(not(x),x)),or(not(y),not(or(not(z),not(u)))))),v)),not(or(not(u),not(y))))),not(or(not(or(not(w),w)),y)))=or(not(u),not(y)). 57 [para_into,19.1.1.2.1.2.1.1.2,31.1.1,demod,32] or(not(or(not(or(not(or(not(x),x)),or(not(y),z))),not(u))),not(or(not(or(not(v),v)),or(not(or(not(or(not(w),w)),u)),not(or(not(or(not(or(not(v6),v6)),or(not(u),not(y)))),v7))))))=or(not(or(not(w),w)),u). 177 [para_into,21.1.1.1.1,21.1.1] or(not(or(not(or(not(x),y)),not(not(x)))),not(or(not(or(not(z),z)),x)))=or(not(or(not(u),u)),not(x)). 206 [para_into,177.1.1,177.1.1] or(not(or(not(x),x)),not(y))=or(not(or(not(z),z)),not(y)). 240 [para_into,206.1.1,27.1.1,flip.1] or(not(or(not(x),x)),not(or(not(or(not(y),y)),or(not(z),not(or(not(u),not(not(z))))))))=z. 388 [para_from,240.1.1,15.1.1.1.1.1.1] or(not(or(not(x),not(y))),not(or(not(or(not(z),z)),or(not(y),not(or(not(u),u))))))=y. 420,419 [para_into,388.1.1,206.1.1] or(not(or(not(x),x)),not(or(not(or(not(y),y)),or(not(z),not(or(not(u),u))))))=z. 444 [para_into,419.1.1.2.1.2,206.1.1,demod,420] or(not(x),x)=or(not(y),y). 446 [para_into,419.1.1.2.1.2,177.1.1,demod,420] or(not(x),x)=or(not(or(not(or(not(y),y)),z)),not(not(or(not(y),y)))). 459 [copy,446,flip.1] or(not(or(not(or(not(x),x)),y)),not(not(or(not(x),x))))=or(not(z),z). 557 [para_from,444.1.1,419.1.1.2.1] or(not(or(not(x),x)),not(or(not(y),y)))=not(or(not(z),z)). 599 [para_from,444.1.1,13.1.1.1.1] or(not(or(not(x),x)),Y)!=Y|$Ans(Meredith_1b). 652 [para_into,37.1.1.2.1,444.1.1] or(not(or(not(or(not(or(not(or(not(x),x)),or(not(or(not(y),y)),not(or(not(z),not(u)))))),v)),not(or(not(u),not(or(not(y),y)))))),not(or(not(w),w)))=or(not(u),not(or(not(y),y))). 660,659 [para_from,37.1.1,419.1.1.2.1.2,demod,420,flip.1] or(not(or(not(or(not(or(not(x),x)),or(not(or(not(y),y)),not(or(not(z),not(u)))))),v)),not(or(not(u),not(or(not(y),y)))))=u. 687 [back_demod,652,demod,660] or(not(x),not(or(not(y),y)))=or(not(x),not(or(not(z),z))). 688 [para_into,557.1.1,557.1.1] not(or(not(x),x))=not(or(not(y),y)). 1384 [para_from,687.1.1,688.1.1.1] not(or(not(not(or(not(x),x))),not(or(not(y),y))))=not(or(not(z),z)). 1387 [para_from,687.1.1,599.1.1.1.1] or(not(or(not(not(or(not(x),x))),not(or(not(y),y)))),Y)!=Y|$Ans(Meredith_1b). 2333 [para_from,1384.1.1,419.1.1.2.1.1.1.1] or(not(or(not(x),x)),not(or(not(or(not(or(not(y),y)),or(not(not(or(not(z),z))),not(or(not(u),u))))),or(not(v),not(or(not(w),w))))))=v. 2427 [para_from,1384.1.1,419.1.1.2.1.2.2.1.1] or(not(or(not(x),x)),not(or(not(or(not(y),y)),or(not(z),not(or(not(or(not(u),u)),or(not(not(or(not(v),v))),not(or(not(w),w)))))))))=z. 3093 [para_into,459.1.1.1.1,419.1.1] or(not(x),not(not(or(not(y),y))))=or(not(z),z). 3122 [copy,3093,flip.1] or(not(x),x)=or(not(y),not(not(or(not(z),z)))). 3330 [para_from,3093.1.1,15.1.1.1.1] or(not(or(not(x),x)),not(or(not(or(not(y),y)),or(not(not(or(not(z),z))),u))))=not(or(not(z),z)). 3354 [para_from,3122.1.1,1384.1.1.1] not(or(not(x),not(not(or(not(y),y)))))=not(or(not(z),z)). 3443,3442 [para_from,3122.1.1,31.1.1.2.1.2] or(not(or(not(or(not(or(not(x),x)),or(not(y),z))),not(not(y)))),not(or(not(or(not(u),u)),or(not(v),not(not(or(not(w),w)))))))=not(y). 3561 [copy,3354,flip.1] not(or(not(x),x))=not(or(not(y),not(not(or(not(z),z))))). 4100 [para_from,3561.1.1,1387.1.1.1.1.2.1.1] or(not(or(not(not(or(not(x),x))),not(or(not(or(not(y),not(not(or(not(z),z))))),or(not(u),u))))),Y)!=Y|$Ans(Meredith_1b). 4585,4584 [para_into,57.1.1.2.1.2.2.1,557.1.1,demod,3443,flip.1] or(not(or(not(x),x)),not(y))=not(y). 4792,4791 [back_demod,3330,demod,4585] not(or(not(or(not(x),x)),or(not(not(or(not(y),y))),z)))=not(or(not(y),y)). 4877,4876 [back_demod,2427,demod,4792,4585] not(or(not(or(not(x),x)),or(not(y),not(or(not(z),z)))))=y. 4888 [back_demod,2333,demod,4877,4877] or(not(or(not(x),x)),y)=y. 4893 [binary,4888.1,4100.1] $Ans(Meredith_1b). ------------ end of proof ------------- ----> UNIT CONFLICT at 7.05 sec ----> 4894 [binary,4888.1,4099.1] $Ans(Meredith_1b). Length of proof is 36. Level of proof is 15. ---------------- PROOF ---------------- 13 [] or(not(or(not(X),X)),Y)!=Y|$Ans(Meredith_1b). 15 [] or(not(or(not(or(x,y)),not(z))),not(or(not(or(not(u),u)),or(not(z),x))))=z. 17 [para_into,15.1.1.1.1.1.1,15.1.1] or(not(or(not(x),not(y))),not(or(not(or(not(z),z)),or(not(y),not(or(not(or(u,v)),not(x)))))))=y. 19 [para_into,15.1.1.1.1,15.1.1] or(not(x),not(or(not(or(not(y),y)),or(not(or(not(or(not(z),z)),or(not(x),u))),not(or(u,v))))))=or(not(or(not(z),z)),or(not(x),u)). 21 [para_into,15.1.1.2.1.2,15.1.1] or(not(or(not(or(not(or(not(or(not(x),x)),or(not(y),z))),u)),not(or(not(or(z,v)),not(y))))),not(or(not(or(not(w),w)),y)))=or(not(or(z,v)),not(y)). 27 [para_into,17.1.1.2.1.2.2.1.1.1,17.1.1] or(not(or(not(x),not(y))),not(or(not(or(not(z),z)),or(not(y),not(or(not(u),not(x)))))))=y. 32,31 [para_into,17.1.1.2.1.2.2.1,15.1.1] or(not(or(not(or(not(or(not(x),x)),or(not(y),z))),not(u))),not(or(not(or(not(v),v)),or(not(u),not(y)))))=u. 37 [para_from,27.1.1,15.1.1.2.1.2] or(not(or(not(or(not(or(not(or(not(x),x)),or(not(y),not(or(not(z),not(u)))))),v)),not(or(not(u),not(y))))),not(or(not(or(not(w),w)),y)))=or(not(u),not(y)). 57 [para_into,19.1.1.2.1.2.1.1.2,31.1.1,demod,32] or(not(or(not(or(not(or(not(x),x)),or(not(y),z))),not(u))),not(or(not(or(not(v),v)),or(not(or(not(or(not(w),w)),u)),not(or(not(or(not(or(not(v6),v6)),or(not(u),not(y)))),v7))))))=or(not(or(not(w),w)),u). 177 [para_into,21.1.1.1.1,21.1.1] or(not(or(not(or(not(x),y)),not(not(x)))),not(or(not(or(not(z),z)),x)))=or(not(or(not(u),u)),not(x)). 206 [para_into,177.1.1,177.1.1] or(not(or(not(x),x)),not(y))=or(not(or(not(z),z)),not(y)). 240 [para_into,206.1.1,27.1.1,flip.1] or(not(or(not(x),x)),not(or(not(or(not(y),y)),or(not(z),not(or(not(u),not(not(z))))))))=z. 388 [para_from,240.1.1,15.1.1.1.1.1.1] or(not(or(not(x),not(y))),not(or(not(or(not(z),z)),or(not(y),not(or(not(u),u))))))=y. 420,419 [para_into,388.1.1,206.1.1] or(not(or(not(x),x)),not(or(not(or(not(y),y)),or(not(z),not(or(not(u),u))))))=z. 444 [para_into,419.1.1.2.1.2,206.1.1,demod,420] or(not(x),x)=or(not(y),y). 446 [para_into,419.1.1.2.1.2,177.1.1,demod,420] or(not(x),x)=or(not(or(not(or(not(y),y)),z)),not(not(or(not(y),y)))). 459 [copy,446,flip.1] or(not(or(not(or(not(x),x)),y)),not(not(or(not(x),x))))=or(not(z),z). 557 [para_from,444.1.1,419.1.1.2.1] or(not(or(not(x),x)),not(or(not(y),y)))=not(or(not(z),z)). 599 [para_from,444.1.1,13.1.1.1.1] or(not(or(not(x),x)),Y)!=Y|$Ans(Meredith_1b). 652 [para_into,37.1.1.2.1,444.1.1] or(not(or(not(or(not(or(not(or(not(x),x)),or(not(or(not(y),y)),not(or(not(z),not(u)))))),v)),not(or(not(u),not(or(not(y),y)))))),not(or(not(w),w)))=or(not(u),not(or(not(y),y))). 660,659 [para_from,37.1.1,419.1.1.2.1.2,demod,420,flip.1] or(not(or(not(or(not(or(not(x),x)),or(not(or(not(y),y)),not(or(not(z),not(u)))))),v)),not(or(not(u),not(or(not(y),y)))))=u. 687 [back_demod,652,demod,660] or(not(x),not(or(not(y),y)))=or(not(x),not(or(not(z),z))). 688 [para_into,557.1.1,557.1.1] not(or(not(x),x))=not(or(not(y),y)). 756 [para_from,688.1.1,599.1.1.1.1.1] or(not(or(not(or(not(x),x)),or(not(y),y))),Y)!=Y|$Ans(Meredith_1b). 1384 [para_from,687.1.1,688.1.1.1] not(or(not(not(or(not(x),x))),not(or(not(y),y))))=not(or(not(z),z)). 2333 [para_from,1384.1.1,419.1.1.2.1.1.1.1] or(not(or(not(x),x)),not(or(not(or(not(or(not(y),y)),or(not(not(or(not(z),z))),not(or(not(u),u))))),or(not(v),not(or(not(w),w))))))=v. 2427 [para_from,1384.1.1,419.1.1.2.1.2.2.1.1] or(not(or(not(x),x)),not(or(not(or(not(y),y)),or(not(z),not(or(not(or(not(u),u)),or(not(not(or(not(v),v))),not(or(not(w),w)))))))))=z. 3093 [para_into,459.1.1.1.1,419.1.1] or(not(x),not(not(or(not(y),y))))=or(not(z),z). 3122 [copy,3093,flip.1] or(not(x),x)=or(not(y),not(not(or(not(z),z)))). 3330 [para_from,3093.1.1,15.1.1.1.1] or(not(or(not(x),x)),not(or(not(or(not(y),y)),or(not(not(or(not(z),z))),u))))=not(or(not(z),z)). 3354 [para_from,3122.1.1,1384.1.1.1] not(or(not(x),not(not(or(not(y),y)))))=not(or(not(z),z)). 3443,3442 [para_from,3122.1.1,31.1.1.2.1.2] or(not(or(not(or(not(or(not(x),x)),or(not(y),z))),not(not(y)))),not(or(not(or(not(u),u)),or(not(v),not(not(or(not(w),w)))))))=not(y). 3561 [copy,3354,flip.1] not(or(not(x),x))=not(or(not(y),not(not(or(not(z),z))))). 4099 [para_from,3561.1.1,756.1.1.1.1.2.1] or(not(or(not(or(not(x),x)),or(not(or(not(y),not(not(or(not(z),z))))),or(not(u),u)))),Y)!=Y|$Ans(Meredith_1b). 4585,4584 [para_into,57.1.1.2.1.2.2.1,557.1.1,demod,3443,flip.1] or(not(or(not(x),x)),not(y))=not(y). 4792,4791 [back_demod,3330,demod,4585] not(or(not(or(not(x),x)),or(not(not(or(not(y),y))),z)))=not(or(not(y),y)). 4877,4876 [back_demod,2427,demod,4792,4585] not(or(not(or(not(x),x)),or(not(y),not(or(not(z),z)))))=y. 4888 [back_demod,2333,demod,4877,4877] or(not(or(not(x),x)),y)=y. 4894 [binary,4888.1,4099.1] $Ans(Meredith_1b). ------------ end of proof ------------- ----> UNIT CONFLICT at 7.05 sec ----> 4895 [binary,4888.1,3922.1] $Ans(Meredith_1b). Length of proof is 35. Level of proof is 15. ---------------- PROOF ---------------- 13 [] or(not(or(not(X),X)),Y)!=Y|$Ans(Meredith_1b). 15 [] or(not(or(not(or(x,y)),not(z))),not(or(not(or(not(u),u)),or(not(z),x))))=z. 17 [para_into,15.1.1.1.1.1.1,15.1.1] or(not(or(not(x),not(y))),not(or(not(or(not(z),z)),or(not(y),not(or(not(or(u,v)),not(x)))))))=y. 19 [para_into,15.1.1.1.1,15.1.1] or(not(x),not(or(not(or(not(y),y)),or(not(or(not(or(not(z),z)),or(not(x),u))),not(or(u,v))))))=or(not(or(not(z),z)),or(not(x),u)). 21 [para_into,15.1.1.2.1.2,15.1.1] or(not(or(not(or(not(or(not(or(not(x),x)),or(not(y),z))),u)),not(or(not(or(z,v)),not(y))))),not(or(not(or(not(w),w)),y)))=or(not(or(z,v)),not(y)). 27 [para_into,17.1.1.2.1.2.2.1.1.1,17.1.1] or(not(or(not(x),not(y))),not(or(not(or(not(z),z)),or(not(y),not(or(not(u),not(x)))))))=y. 32,31 [para_into,17.1.1.2.1.2.2.1,15.1.1] or(not(or(not(or(not(or(not(x),x)),or(not(y),z))),not(u))),not(or(not(or(not(v),v)),or(not(u),not(y)))))=u. 37 [para_from,27.1.1,15.1.1.2.1.2] or(not(or(not(or(not(or(not(or(not(x),x)),or(not(y),not(or(not(z),not(u)))))),v)),not(or(not(u),not(y))))),not(or(not(or(not(w),w)),y)))=or(not(u),not(y)). 57 [para_into,19.1.1.2.1.2.1.1.2,31.1.1,demod,32] or(not(or(not(or(not(or(not(x),x)),or(not(y),z))),not(u))),not(or(not(or(not(v),v)),or(not(or(not(or(not(w),w)),u)),not(or(not(or(not(or(not(v6),v6)),or(not(u),not(y)))),v7))))))=or(not(or(not(w),w)),u). 177 [para_into,21.1.1.1.1,21.1.1] or(not(or(not(or(not(x),y)),not(not(x)))),not(or(not(or(not(z),z)),x)))=or(not(or(not(u),u)),not(x)). 206 [para_into,177.1.1,177.1.1] or(not(or(not(x),x)),not(y))=or(not(or(not(z),z)),not(y)). 240 [para_into,206.1.1,27.1.1,flip.1] or(not(or(not(x),x)),not(or(not(or(not(y),y)),or(not(z),not(or(not(u),not(not(z))))))))=z. 388 [para_from,240.1.1,15.1.1.1.1.1.1] or(not(or(not(x),not(y))),not(or(not(or(not(z),z)),or(not(y),not(or(not(u),u))))))=y. 420,419 [para_into,388.1.1,206.1.1] or(not(or(not(x),x)),not(or(not(or(not(y),y)),or(not(z),not(or(not(u),u))))))=z. 444 [para_into,419.1.1.2.1.2,206.1.1,demod,420] or(not(x),x)=or(not(y),y). 446 [para_into,419.1.1.2.1.2,177.1.1,demod,420] or(not(x),x)=or(not(or(not(or(not(y),y)),z)),not(not(or(not(y),y)))). 459 [copy,446,flip.1] or(not(or(not(or(not(x),x)),y)),not(not(or(not(x),x))))=or(not(z),z). 557 [para_from,444.1.1,419.1.1.2.1] or(not(or(not(x),x)),not(or(not(y),y)))=not(or(not(z),z)). 599 [para_from,444.1.1,13.1.1.1.1] or(not(or(not(x),x)),Y)!=Y|$Ans(Meredith_1b). 652 [para_into,37.1.1.2.1,444.1.1] or(not(or(not(or(not(or(not(or(not(x),x)),or(not(or(not(y),y)),not(or(not(z),not(u)))))),v)),not(or(not(u),not(or(not(y),y)))))),not(or(not(w),w)))=or(not(u),not(or(not(y),y))). 660,659 [para_from,37.1.1,419.1.1.2.1.2,demod,420,flip.1] or(not(or(not(or(not(or(not(x),x)),or(not(or(not(y),y)),not(or(not(z),not(u)))))),v)),not(or(not(u),not(or(not(y),y)))))=u. 687 [back_demod,652,demod,660] or(not(x),not(or(not(y),y)))=or(not(x),not(or(not(z),z))). 688 [para_into,557.1.1,557.1.1] not(or(not(x),x))=not(or(not(y),y)). 1384 [para_from,687.1.1,688.1.1.1] not(or(not(not(or(not(x),x))),not(or(not(y),y))))=not(or(not(z),z)). 1387 [para_from,687.1.1,599.1.1.1.1] or(not(or(not(not(or(not(x),x))),not(or(not(y),y)))),Y)!=Y|$Ans(Meredith_1b). 2333 [para_from,1384.1.1,419.1.1.2.1.1.1.1] or(not(or(not(x),x)),not(or(not(or(not(or(not(y),y)),or(not(not(or(not(z),z))),not(or(not(u),u))))),or(not(v),not(or(not(w),w))))))=v. 2427 [para_from,1384.1.1,419.1.1.2.1.2.2.1.1] or(not(or(not(x),x)),not(or(not(or(not(y),y)),or(not(z),not(or(not(or(not(u),u)),or(not(not(or(not(v),v))),not(or(not(w),w)))))))))=z. 3093 [para_into,459.1.1.1.1,419.1.1] or(not(x),not(not(or(not(y),y))))=or(not(z),z). 3122 [copy,3093,flip.1] or(not(x),x)=or(not(y),not(not(or(not(z),z)))). 3330 [para_from,3093.1.1,15.1.1.1.1] or(not(or(not(x),x)),not(or(not(or(not(y),y)),or(not(not(or(not(z),z))),u))))=not(or(not(z),z)). 3354 [para_from,3122.1.1,1384.1.1.1] not(or(not(x),not(not(or(not(y),y)))))=not(or(not(z),z)). 3443,3442 [para_from,3122.1.1,31.1.1.2.1.2] or(not(or(not(or(not(or(not(x),x)),or(not(y),z))),not(not(y)))),not(or(not(or(not(u),u)),or(not(v),not(not(or(not(w),w)))))))=not(y). 3922 [para_from,3354.1.1,1387.1.1.1.1.1.1.1.1] or(not(or(not(not(or(not(or(not(x),x)),or(not(y),not(not(or(not(z),z))))))),not(or(not(u),u)))),Y)!=Y|$Ans(Meredith_1b). 4585,4584 [para_into,57.1.1.2.1.2.2.1,557.1.1,demod,3443,flip.1] or(not(or(not(x),x)),not(y))=not(y). 4792,4791 [back_demod,3330,demod,4585] not(or(not(or(not(x),x)),or(not(not(or(not(y),y))),z)))=not(or(not(y),y)). 4877,4876 [back_demod,2427,demod,4792,4585] not(or(not(or(not(x),x)),or(not(y),not(or(not(z),z)))))=y. 4888 [back_demod,2333,demod,4877,4877] or(not(or(not(x),x)),y)=y. 4895 [binary,4888.1,3922.1] $Ans(Meredith_1b). ------------ end of proof ------------- ----> UNIT CONFLICT at 7.05 sec ----> 4896 [binary,4888.1,3918.1] $Ans(Meredith_1b). Length of proof is 35. Level of proof is 15. ---------------- PROOF ---------------- 13 [] or(not(or(not(X),X)),Y)!=Y|$Ans(Meredith_1b). 15 [] or(not(or(not(or(x,y)),not(z))),not(or(not(or(not(u),u)),or(not(z),x))))=z. 17 [para_into,15.1.1.1.1.1.1,15.1.1] or(not(or(not(x),not(y))),not(or(not(or(not(z),z)),or(not(y),not(or(not(or(u,v)),not(x)))))))=y. 19 [para_into,15.1.1.1.1,15.1.1] or(not(x),not(or(not(or(not(y),y)),or(not(or(not(or(not(z),z)),or(not(x),u))),not(or(u,v))))))=or(not(or(not(z),z)),or(not(x),u)). 21 [para_into,15.1.1.2.1.2,15.1.1] or(not(or(not(or(not(or(not(or(not(x),x)),or(not(y),z))),u)),not(or(not(or(z,v)),not(y))))),not(or(not(or(not(w),w)),y)))=or(not(or(z,v)),not(y)). 27 [para_into,17.1.1.2.1.2.2.1.1.1,17.1.1] or(not(or(not(x),not(y))),not(or(not(or(not(z),z)),or(not(y),not(or(not(u),not(x)))))))=y. 32,31 [para_into,17.1.1.2.1.2.2.1,15.1.1] or(not(or(not(or(not(or(not(x),x)),or(not(y),z))),not(u))),not(or(not(or(not(v),v)),or(not(u),not(y)))))=u. 37 [para_from,27.1.1,15.1.1.2.1.2] or(not(or(not(or(not(or(not(or(not(x),x)),or(not(y),not(or(not(z),not(u)))))),v)),not(or(not(u),not(y))))),not(or(not(or(not(w),w)),y)))=or(not(u),not(y)). 57 [para_into,19.1.1.2.1.2.1.1.2,31.1.1,demod,32] or(not(or(not(or(not(or(not(x),x)),or(not(y),z))),not(u))),not(or(not(or(not(v),v)),or(not(or(not(or(not(w),w)),u)),not(or(not(or(not(or(not(v6),v6)),or(not(u),not(y)))),v7))))))=or(not(or(not(w),w)),u). 177 [para_into,21.1.1.1.1,21.1.1] or(not(or(not(or(not(x),y)),not(not(x)))),not(or(not(or(not(z),z)),x)))=or(not(or(not(u),u)),not(x)). 206 [para_into,177.1.1,177.1.1] or(not(or(not(x),x)),not(y))=or(not(or(not(z),z)),not(y)). 240 [para_into,206.1.1,27.1.1,flip.1] or(not(or(not(x),x)),not(or(not(or(not(y),y)),or(not(z),not(or(not(u),not(not(z))))))))=z. 388 [para_from,240.1.1,15.1.1.1.1.1.1] or(not(or(not(x),not(y))),not(or(not(or(not(z),z)),or(not(y),not(or(not(u),u))))))=y. 420,419 [para_into,388.1.1,206.1.1] or(not(or(not(x),x)),not(or(not(or(not(y),y)),or(not(z),not(or(not(u),u))))))=z. 444 [para_into,419.1.1.2.1.2,206.1.1,demod,420] or(not(x),x)=or(not(y),y). 446 [para_into,419.1.1.2.1.2,177.1.1,demod,420] or(not(x),x)=or(not(or(not(or(not(y),y)),z)),not(not(or(not(y),y)))). 459 [copy,446,flip.1] or(not(or(not(or(not(x),x)),y)),not(not(or(not(x),x))))=or(not(z),z). 557 [para_from,444.1.1,419.1.1.2.1] or(not(or(not(x),x)),not(or(not(y),y)))=not(or(not(z),z)). 599 [para_from,444.1.1,13.1.1.1.1] or(not(or(not(x),x)),Y)!=Y|$Ans(Meredith_1b). 652 [para_into,37.1.1.2.1,444.1.1] or(not(or(not(or(not(or(not(or(not(x),x)),or(not(or(not(y),y)),not(or(not(z),not(u)))))),v)),not(or(not(u),not(or(not(y),y)))))),not(or(not(w),w)))=or(not(u),not(or(not(y),y))). 660,659 [para_from,37.1.1,419.1.1.2.1.2,demod,420,flip.1] or(not(or(not(or(not(or(not(x),x)),or(not(or(not(y),y)),not(or(not(z),not(u)))))),v)),not(or(not(u),not(or(not(y),y)))))=u. 687 [back_demod,652,demod,660] or(not(x),not(or(not(y),y)))=or(not(x),not(or(not(z),z))). 688 [para_into,557.1.1,557.1.1] not(or(not(x),x))=not(or(not(y),y)). 756 [para_from,688.1.1,599.1.1.1.1.1] or(not(or(not(or(not(x),x)),or(not(y),y))),Y)!=Y|$Ans(Meredith_1b). 1384 [para_from,687.1.1,688.1.1.1] not(or(not(not(or(not(x),x))),not(or(not(y),y))))=not(or(not(z),z)). 2333 [para_from,1384.1.1,419.1.1.2.1.1.1.1] or(not(or(not(x),x)),not(or(not(or(not(or(not(y),y)),or(not(not(or(not(z),z))),not(or(not(u),u))))),or(not(v),not(or(not(w),w))))))=v. 2427 [para_from,1384.1.1,419.1.1.2.1.2.2.1.1] or(not(or(not(x),x)),not(or(not(or(not(y),y)),or(not(z),not(or(not(or(not(u),u)),or(not(not(or(not(v),v))),not(or(not(w),w)))))))))=z. 3093 [para_into,459.1.1.1.1,419.1.1] or(not(x),not(not(or(not(y),y))))=or(not(z),z). 3122 [copy,3093,flip.1] or(not(x),x)=or(not(y),not(not(or(not(z),z)))). 3330 [para_from,3093.1.1,15.1.1.1.1] or(not(or(not(x),x)),not(or(not(or(not(y),y)),or(not(not(or(not(z),z))),u))))=not(or(not(z),z)). 3354 [para_from,3122.1.1,1384.1.1.1] not(or(not(x),not(not(or(not(y),y)))))=not(or(not(z),z)). 3443,3442 [para_from,3122.1.1,31.1.1.2.1.2] or(not(or(not(or(not(or(not(x),x)),or(not(y),z))),not(not(y)))),not(or(not(or(not(u),u)),or(not(v),not(not(or(not(w),w)))))))=not(y). 3918 [para_from,3354.1.1,756.1.1.1.1.1.1.1] or(not(or(not(or(not(or(not(x),x)),or(not(y),not(not(or(not(z),z)))))),or(not(u),u))),Y)!=Y|$Ans(Meredith_1b). 4585,4584 [para_into,57.1.1.2.1.2.2.1,557.1.1,demod,3443,flip.1] or(not(or(not(x),x)),not(y))=not(y). 4792,4791 [back_demod,3330,demod,4585] not(or(not(or(not(x),x)),or(not(not(or(not(y),y))),z)))=not(or(not(y),y)). 4877,4876 [back_demod,2427,demod,4792,4585] not(or(not(or(not(x),x)),or(not(y),not(or(not(z),z)))))=y. 4888 [back_demod,2333,demod,4877,4877] or(not(or(not(x),x)),y)=y. 4896 [binary,4888.1,3918.1] $Ans(Meredith_1b). ------------ end of proof ------------- ----> UNIT CONFLICT at 7.05 sec ----> 4897 [binary,4888.1,3858.1] $Ans(Meredith_1b). Length of proof is 36. Level of proof is 15. ---------------- PROOF ---------------- 13 [] or(not(or(not(X),X)),Y)!=Y|$Ans(Meredith_1b). 15 [] or(not(or(not(or(x,y)),not(z))),not(or(not(or(not(u),u)),or(not(z),x))))=z. 17 [para_into,15.1.1.1.1.1.1,15.1.1] or(not(or(not(x),not(y))),not(or(not(or(not(z),z)),or(not(y),not(or(not(or(u,v)),not(x)))))))=y. 19 [para_into,15.1.1.1.1,15.1.1] or(not(x),not(or(not(or(not(y),y)),or(not(or(not(or(not(z),z)),or(not(x),u))),not(or(u,v))))))=or(not(or(not(z),z)),or(not(x),u)). 21 [para_into,15.1.1.2.1.2,15.1.1] or(not(or(not(or(not(or(not(or(not(x),x)),or(not(y),z))),u)),not(or(not(or(z,v)),not(y))))),not(or(not(or(not(w),w)),y)))=or(not(or(z,v)),not(y)). 27 [para_into,17.1.1.2.1.2.2.1.1.1,17.1.1] or(not(or(not(x),not(y))),not(or(not(or(not(z),z)),or(not(y),not(or(not(u),not(x)))))))=y. 32,31 [para_into,17.1.1.2.1.2.2.1,15.1.1] or(not(or(not(or(not(or(not(x),x)),or(not(y),z))),not(u))),not(or(not(or(not(v),v)),or(not(u),not(y)))))=u. 37 [para_from,27.1.1,15.1.1.2.1.2] or(not(or(not(or(not(or(not(or(not(x),x)),or(not(y),not(or(not(z),not(u)))))),v)),not(or(not(u),not(y))))),not(or(not(or(not(w),w)),y)))=or(not(u),not(y)). 57 [para_into,19.1.1.2.1.2.1.1.2,31.1.1,demod,32] or(not(or(not(or(not(or(not(x),x)),or(not(y),z))),not(u))),not(or(not(or(not(v),v)),or(not(or(not(or(not(w),w)),u)),not(or(not(or(not(or(not(v6),v6)),or(not(u),not(y)))),v7))))))=or(not(or(not(w),w)),u). 177 [para_into,21.1.1.1.1,21.1.1] or(not(or(not(or(not(x),y)),not(not(x)))),not(or(not(or(not(z),z)),x)))=or(not(or(not(u),u)),not(x)). 206 [para_into,177.1.1,177.1.1] or(not(or(not(x),x)),not(y))=or(not(or(not(z),z)),not(y)). 240 [para_into,206.1.1,27.1.1,flip.1] or(not(or(not(x),x)),not(or(not(or(not(y),y)),or(not(z),not(or(not(u),not(not(z))))))))=z. 388 [para_from,240.1.1,15.1.1.1.1.1.1] or(not(or(not(x),not(y))),not(or(not(or(not(z),z)),or(not(y),not(or(not(u),u))))))=y. 420,419 [para_into,388.1.1,206.1.1] or(not(or(not(x),x)),not(or(not(or(not(y),y)),or(not(z),not(or(not(u),u))))))=z. 444 [para_into,419.1.1.2.1.2,206.1.1,demod,420] or(not(x),x)=or(not(y),y). 446 [para_into,419.1.1.2.1.2,177.1.1,demod,420] or(not(x),x)=or(not(or(not(or(not(y),y)),z)),not(not(or(not(y),y)))). 459 [copy,446,flip.1] or(not(or(not(or(not(x),x)),y)),not(not(or(not(x),x))))=or(not(z),z). 557 [para_from,444.1.1,419.1.1.2.1] or(not(or(not(x),x)),not(or(not(y),y)))=not(or(not(z),z)). 599 [para_from,444.1.1,13.1.1.1.1] or(not(or(not(x),x)),Y)!=Y|$Ans(Meredith_1b). 652 [para_into,37.1.1.2.1,444.1.1] or(not(or(not(or(not(or(not(or(not(x),x)),or(not(or(not(y),y)),not(or(not(z),not(u)))))),v)),not(or(not(u),not(or(not(y),y)))))),not(or(not(w),w)))=or(not(u),not(or(not(y),y))). 660,659 [para_from,37.1.1,419.1.1.2.1.2,demod,420,flip.1] or(not(or(not(or(not(or(not(x),x)),or(not(or(not(y),y)),not(or(not(z),not(u)))))),v)),not(or(not(u),not(or(not(y),y)))))=u. 687 [back_demod,652,demod,660] or(not(x),not(or(not(y),y)))=or(not(x),not(or(not(z),z))). 688 [para_into,557.1.1,557.1.1] not(or(not(x),x))=not(or(not(y),y)). 1384 [para_from,687.1.1,688.1.1.1] not(or(not(not(or(not(x),x))),not(or(not(y),y))))=not(or(not(z),z)). 1387 [para_from,687.1.1,599.1.1.1.1] or(not(or(not(not(or(not(x),x))),not(or(not(y),y)))),Y)!=Y|$Ans(Meredith_1b). 2333 [para_from,1384.1.1,419.1.1.2.1.1.1.1] or(not(or(not(x),x)),not(or(not(or(not(or(not(y),y)),or(not(not(or(not(z),z))),not(or(not(u),u))))),or(not(v),not(or(not(w),w))))))=v. 2427 [para_from,1384.1.1,419.1.1.2.1.2.2.1.1] or(not(or(not(x),x)),not(or(not(or(not(y),y)),or(not(z),not(or(not(or(not(u),u)),or(not(not(or(not(v),v))),not(or(not(w),w)))))))))=z. 3093 [para_into,459.1.1.1.1,419.1.1] or(not(x),not(not(or(not(y),y))))=or(not(z),z). 3122 [copy,3093,flip.1] or(not(x),x)=or(not(y),not(not(or(not(z),z)))). 3330 [para_from,3093.1.1,15.1.1.1.1] or(not(or(not(x),x)),not(or(not(or(not(y),y)),or(not(not(or(not(z),z))),u))))=not(or(not(z),z)). 3353 [para_from,3122.1.1,1387.1.1.1.1] or(not(or(not(x),not(not(or(not(y),y))))),Y)!=Y|$Ans(Meredith_1b). 3354 [para_from,3122.1.1,1384.1.1.1] not(or(not(x),not(not(or(not(y),y)))))=not(or(not(z),z)). 3443,3442 [para_from,3122.1.1,31.1.1.2.1.2] or(not(or(not(or(not(or(not(x),x)),or(not(y),z))),not(not(y)))),not(or(not(or(not(u),u)),or(not(v),not(not(or(not(w),w)))))))=not(y). 3858 [para_from,3354.1.1,3353.1.1.1.1.2.1.1.1] or(not(or(not(x),not(not(or(not(or(not(y),y)),or(not(z),not(not(or(not(u),u))))))))),Y)!=Y|$Ans(Meredith_1b). 4585,4584 [para_into,57.1.1.2.1.2.2.1,557.1.1,demod,3443,flip.1] or(not(or(not(x),x)),not(y))=not(y). 4792,4791 [back_demod,3330,demod,4585] not(or(not(or(not(x),x)),or(not(not(or(not(y),y))),z)))=not(or(not(y),y)). 4877,4876 [back_demod,2427,demod,4792,4585] not(or(not(or(not(x),x)),or(not(y),not(or(not(z),z)))))=y. 4888 [back_demod,2333,demod,4877,4877] or(not(or(not(x),x)),y)=y. 4897 [binary,4888.1,3858.1] $Ans(Meredith_1b). ------------ end of proof ------------- ----> UNIT CONFLICT at 7.06 sec ----> 4898 [binary,4888.1,3850.1] $Ans(Meredith_1b). Length of proof is 35. Level of proof is 15. ---------------- PROOF ---------------- 13 [] or(not(or(not(X),X)),Y)!=Y|$Ans(Meredith_1b). 15 [] or(not(or(not(or(x,y)),not(z))),not(or(not(or(not(u),u)),or(not(z),x))))=z. 17 [para_into,15.1.1.1.1.1.1,15.1.1] or(not(or(not(x),not(y))),not(or(not(or(not(z),z)),or(not(y),not(or(not(or(u,v)),not(x)))))))=y. 19 [para_into,15.1.1.1.1,15.1.1] or(not(x),not(or(not(or(not(y),y)),or(not(or(not(or(not(z),z)),or(not(x),u))),not(or(u,v))))))=or(not(or(not(z),z)),or(not(x),u)). 21 [para_into,15.1.1.2.1.2,15.1.1] or(not(or(not(or(not(or(not(or(not(x),x)),or(not(y),z))),u)),not(or(not(or(z,v)),not(y))))),not(or(not(or(not(w),w)),y)))=or(not(or(z,v)),not(y)). 27 [para_into,17.1.1.2.1.2.2.1.1.1,17.1.1] or(not(or(not(x),not(y))),not(or(not(or(not(z),z)),or(not(y),not(or(not(u),not(x)))))))=y. 32,31 [para_into,17.1.1.2.1.2.2.1,15.1.1] or(not(or(not(or(not(or(not(x),x)),or(not(y),z))),not(u))),not(or(not(or(not(v),v)),or(not(u),not(y)))))=u. 37 [para_from,27.1.1,15.1.1.2.1.2] or(not(or(not(or(not(or(not(or(not(x),x)),or(not(y),not(or(not(z),not(u)))))),v)),not(or(not(u),not(y))))),not(or(not(or(not(w),w)),y)))=or(not(u),not(y)). 57 [para_into,19.1.1.2.1.2.1.1.2,31.1.1,demod,32] or(not(or(not(or(not(or(not(x),x)),or(not(y),z))),not(u))),not(or(not(or(not(v),v)),or(not(or(not(or(not(w),w)),u)),not(or(not(or(not(or(not(v6),v6)),or(not(u),not(y)))),v7))))))=or(not(or(not(w),w)),u). 177 [para_into,21.1.1.1.1,21.1.1] or(not(or(not(or(not(x),y)),not(not(x)))),not(or(not(or(not(z),z)),x)))=or(not(or(not(u),u)),not(x)). 206 [para_into,177.1.1,177.1.1] or(not(or(not(x),x)),not(y))=or(not(or(not(z),z)),not(y)). 240 [para_into,206.1.1,27.1.1,flip.1] or(not(or(not(x),x)),not(or(not(or(not(y),y)),or(not(z),not(or(not(u),not(not(z))))))))=z. 388 [para_from,240.1.1,15.1.1.1.1.1.1] or(not(or(not(x),not(y))),not(or(not(or(not(z),z)),or(not(y),not(or(not(u),u))))))=y. 420,419 [para_into,388.1.1,206.1.1] or(not(or(not(x),x)),not(or(not(or(not(y),y)),or(not(z),not(or(not(u),u))))))=z. 444 [para_into,419.1.1.2.1.2,206.1.1,demod,420] or(not(x),x)=or(not(y),y). 446 [para_into,419.1.1.2.1.2,177.1.1,demod,420] or(not(x),x)=or(not(or(not(or(not(y),y)),z)),not(not(or(not(y),y)))). 459 [copy,446,flip.1] or(not(or(not(or(not(x),x)),y)),not(not(or(not(x),x))))=or(not(z),z). 557 [para_from,444.1.1,419.1.1.2.1] or(not(or(not(x),x)),not(or(not(y),y)))=not(or(not(z),z)). 599 [para_from,444.1.1,13.1.1.1.1] or(not(or(not(x),x)),Y)!=Y|$Ans(Meredith_1b). 652 [para_into,37.1.1.2.1,444.1.1] or(not(or(not(or(not(or(not(or(not(x),x)),or(not(or(not(y),y)),not(or(not(z),not(u)))))),v)),not(or(not(u),not(or(not(y),y)))))),not(or(not(w),w)))=or(not(u),not(or(not(y),y))). 660,659 [para_from,37.1.1,419.1.1.2.1.2,demod,420,flip.1] or(not(or(not(or(not(or(not(x),x)),or(not(or(not(y),y)),not(or(not(z),not(u)))))),v)),not(or(not(u),not(or(not(y),y)))))=u. 687 [back_demod,652,demod,660] or(not(x),not(or(not(y),y)))=or(not(x),not(or(not(z),z))). 688 [para_into,557.1.1,557.1.1] not(or(not(x),x))=not(or(not(y),y)). 1384 [para_from,687.1.1,688.1.1.1] not(or(not(not(or(not(x),x))),not(or(not(y),y))))=not(or(not(z),z)). 1387 [para_from,687.1.1,599.1.1.1.1] or(not(or(not(not(or(not(x),x))),not(or(not(y),y)))),Y)!=Y|$Ans(Meredith_1b). 2333 [para_from,1384.1.1,419.1.1.2.1.1.1.1] or(not(or(not(x),x)),not(or(not(or(not(or(not(y),y)),or(not(not(or(not(z),z))),not(or(not(u),u))))),or(not(v),not(or(not(w),w))))))=v. 2427 [para_from,1384.1.1,419.1.1.2.1.2.2.1.1] or(not(or(not(x),x)),not(or(not(or(not(y),y)),or(not(z),not(or(not(or(not(u),u)),or(not(not(or(not(v),v))),not(or(not(w),w)))))))))=z. 3093 [para_into,459.1.1.1.1,419.1.1] or(not(x),not(not(or(not(y),y))))=or(not(z),z). 3122 [copy,3093,flip.1] or(not(x),x)=or(not(y),not(not(or(not(z),z)))). 3330 [para_from,3093.1.1,15.1.1.1.1] or(not(or(not(x),x)),not(or(not(or(not(y),y)),or(not(not(or(not(z),z))),u))))=not(or(not(z),z)). 3354 [para_from,3122.1.1,1384.1.1.1] not(or(not(x),not(not(or(not(y),y)))))=not(or(not(z),z)). 3443,3442 [para_from,3122.1.1,31.1.1.2.1.2] or(not(or(not(or(not(or(not(x),x)),or(not(y),z))),not(not(y)))),not(or(not(or(not(u),u)),or(not(v),not(not(or(not(w),w)))))))=not(y). 3850 [para_from,3354.1.1,1387.1.1.1.1.2.1.1] or(not(or(not(not(or(not(x),x))),not(or(not(or(not(y),y)),or(not(z),not(not(or(not(u),u)))))))),Y)!=Y|$Ans(Meredith_1b). 4585,4584 [para_into,57.1.1.2.1.2.2.1,557.1.1,demod,3443,flip.1] or(not(or(not(x),x)),not(y))=not(y). 4792,4791 [back_demod,3330,demod,4585] not(or(not(or(not(x),x)),or(not(not(or(not(y),y))),z)))=not(or(not(y),y)). 4877,4876 [back_demod,2427,demod,4792,4585] not(or(not(or(not(x),x)),or(not(y),not(or(not(z),z)))))=y. 4888 [back_demod,2333,demod,4877,4877] or(not(or(not(x),x)),y)=y. 4898 [binary,4888.1,3850.1] $Ans(Meredith_1b). ------------ end of proof -------------