----- EQP 0.9, June 1996 ----- The job began on eyas08.mcs.anl.gov, Fri Nov 15 09:33:08 1996 ---------------- PROOF ---------------- 7 (wt=13) [] n(n(n(x)+y)+n(x+y)) = y. 8 (wt=14) [] -(n(B+n(A))+n(n(B)+n(A)) = A). 10 (wt=18) [para(7,7)] n(n(n(x+y)+n(x)+y)+y) = n(x+y). 11 (wt=19) [para(7,7)] n(n(n(n(x)+y)+x+y)+y) = n(n(x)+y). 22 (wt=20) [para(10,7)] n(n(n(x+y)+n(x)+y+y)+n(x+y)) = y. 29 (wt=21) [para(11,7)] n(n(n(n(x)+y)+x+y+y)+n(n(x)+y)) = y. 42 (wt=28) [para(22,7)] n(n(n(n(x+y)+n(x)+y+y)+n(x+y)+z)+n(y+z)) = z. 54 (wt=29) [para(29,7)] n(n(n(n(n(x)+y)+x+y+y)+n(n(x)+y)+z)+n(y+z)) = z. 55 (wt=27) [para(29,7)] n(n(n(n(x)+y)+n(n(x)+y)+x+y+y)+y) = n(n(x)+y). 137 (wt=35) [para(55,7)] n(n(n(n(n(x)+y)+n(n(x)+y)+x+y+y)+y+z)+n(n(n(x)+y)+z)) = z. 172 (wt=33) [para(42,7)] n(n(n(n(x+y)+n(x)+y+y)+n(x+y)+n(y+z)+z)+z) = n(y+z). 217 (wt=34) [para(54,7)] n(n(n(n(n(x)+y)+x+y+y)+n(n(x)+y)+n(y+z)+z)+z) = n(y+z). 526 (wt=41) [para(172,7)] n(n(n(n(n(x+y)+n(x)+y+y)+n(x+y)+n(y+z)+z)+z+u)+n(n(y+z)+u)) = u. 674 (wt=42) [para(217,7)] n(n(n(n(n(n(x)+y)+x+y+y)+n(n(x)+y)+n(y+z)+z)+z+u)+n(n(y+z)+u)) = u. 3815 (wt=50) [para(29,137)] n(n(n(n(n(x)+y)+n(n(x)+y)+x+y+y)+n(n(n(x)+y)+x+y+y)+y)+y) = n(n(n(x)+y)+x+y+y). 5732 (wt=25) [para(10,526),demod([7])] n(n(n(n(x)+x)+n(x)+n(x)+n(x))+n(x)) = n(n(x)+x). 5736 (wt=30) [para(5732,7)] n(n(n(n(n(n(x)+x)+n(x)+n(x)+n(x)))+n(x))+n(n(x)+x)) = n(x). 5745 (wt=36) [para(5736,7)] n(n(n(n(n(n(x)+x)+n(x)+n(x)+n(x)))+n(n(x)+x)+n(x))+n(x)) = n(n(x)+x). 5771 (wt=41) [para(5745,7)] n(n(n(n(n(n(n(n(x)+x)+n(x)+n(x)+n(x)))+n(n(x)+x)+n(x)))+n(x))+n(n(x)+x)) = n(x). 5850 (wt=47) [para(5771,7)] n(n(n(n(n(n(n(n(x)+x)+n(x)+n(x)+n(x)))+n(n(x)+x)+n(x)))+n(n(x)+x)+n(x))+n(x)) = n(n(x)+x). 6736 (wt=49) [para(10,674)] n(n(n(n(x+x+x)+x)+n(x+x+x))+n(n(n(x+x+x)+x)+x+x+x+x+x)) = n(n(x+x+x)+x). 7924 (wt=50) [para(5850,7)] n(n(n(n(n(n(n(n(x)+x)+n(x)+n(x)+n(x)))+n(n(x)+x)+n(x)))+n(n(x)+x)+n(x)+n(x))+n(n(x)+x)) = n(x). 8855 (wt=27) [para(6736,7),demod([54]),flip(1)] n(n(n(x+x+x)+x)+x+x+x+x+x) = n(x+x+x). 8858 (wt=35) [para(8855,7)] n(n(n(n(x+x+x)+x)+x+x+x+x+x+y)+n(n(x+x+x)+y)) = y. 8859 (wt=37) [para(8855,7)] n(n(n(x+x+x)+x+x+x+x+x+x)+n(x+x+x)) = x+x+x+x+x. 8861 (wt=47) [para(8855,7)] n(n(n(n(x+x+x)+x)+n(x)+x+x+x+x)+n(x+x+x)) = n(n(x+x+x)+x)+x+x+x+x. 8863 (wt=45) [para(8855,7)] n(n(n(n(x+x+x)+x)+n(x+x)+x+x+x)+n(x+x+x)) = n(n(x+x+x)+x)+x+x+x. 8865 (wt=43) [para(8855,7)] n(n(n(n(x+x+x)+x)+n(x+x+x)+x+x)+n(x+x+x)) = n(n(x+x+x)+x)+x+x. 8866 (wt=19) [para(8855,7),demod([11])] n(n(n(x+x+x)+x)+n(x+x+x)) = x. 8867 (wt=41) [para(8855,7)] n(n(n(n(x+x+x)+x)+n(x+x+x+x)+x)+n(x+x+x)) = n(n(x+x+x)+x)+x. 8870 (wt=27) [para(8866,7)] n(n(n(n(x+x+x)+x)+n(x+x+x)+y)+n(x+y)) = y. 8871 (wt=17) [back_demod(8865),demod([8870]),flip(1)] n(n(x+x+x)+x)+x+x = x+x. 8872 (wt=27) [back_demod(8861),demod([8871,8871])] n(n(n(x)+x+x+x+x)+n(x+x+x)) = x+x+x+x. 8873 (wt=25) [back_demod(8863),demod([8871,8871])] n(n(n(x+x)+x+x+x)+n(x+x+x)) = x+x+x. 8874 (wt=25) [back_demod(8858),demod([8871])] n(n(n(x+x+x)+y)+n(x+x+x+x+x+y)) = y. 8876 (wt=17) [back_demod(8855),demod([8871])] n(x+x+x+x+x) = n(x+x+x). 8881 (wt=23) [para(8871,7)] n(n(n(x+x+x)+x+x+x)+n(x+x)) = x+x. 8882 (wt=23) [para(8871,7)] n(n(n(n(n(x+x+x)+x)+x)+x)+n(x+x)) = x. 8884 (wt=25) [para(8871,7)] n(n(n(n(n(x+x+x)+x))+x+x)+n(x+x)) = x+x. 8887 (wt=29) [para(8871',7)] n(n(n(x+x+x)+x+x+x+y)+n(x+x+y)) = x+x+y. 8897 (wt=21) [para(8876,7)] n(n(n(x+x+x+x)+x)+n(x+x+x)) = x. 8902 (wt=15) [para(8897,7),demod([10])] n(x+x+x+x) = n(x+x+x). 8903 (wt=39) [back_demod(8867),demod([8902])] n(n(n(n(x+x+x)+x)+n(x+x+x)+x)+n(x+x+x)) = n(n(x+x+x)+x)+x. 8904 (wt=23) [para(8902,7)] n(n(n(x+x+x)+y)+n(x+x+x+x+y)) = y. 8907 (wt=21) [para(8902,7)] n(n(n(x+x)+x+x)+n(x+x+x)) = x+x. 8910 (wt=28) [para(8907,7)] n(n(n(x+x+x)+n(x+x)+x+x)+x+x) = n(x+x+x). 8911 (wt=31) [para(8907,7)] n(n(n(n(x+x)+x+x)+x+x+x)+x+x) = n(n(x+x)+x+x). 8928 (wt=28) [para(8881,7)] n(n(n(x+x+x)+n(x+x)+x+x+x)+x+x) = n(x+x). 8931 (wt=31) [para(8882,7)] n(n(n(n(n(n(x+x+x)+x)+x)+x)+n(x+x)+y)+n(x+y)) = y. 8941 (wt=29) [para(7,8904)] n(n(n(n(x)+x+x)+x+x+x+x)+x+x) = n(n(x)+x+x). 8950 (wt=31) [para(8871',22)] n(n(n(n(x+x+x)+x+x)+x+x)+n(n(x+x+x)+x+x)) = x. 8975 (wt=32) [para(8873,7)] n(n(n(x+x+x)+n(x+x)+x+x+x)+x+x+x) = n(x+x+x). 9009 (wt=45) [para(8902,8873)] n(n(n(x+x+x)+x+x+x+x+x+x)+n(x+x+x+x+x+x)) = x+x+x+x+x+x. 9019 (wt=34) [para(8872,7)] n(n(n(x+x+x)+n(x)+x+x+x+x)+x+x+x+x) = n(x+x+x). 9053 (wt=49) [para(8910,7)] n(n(n(n(x+x+x)+n(x+x)+x+x)+n(x)+x)+n(x+x+x)) = n(n(x+x+x)+n(x+x)+x+x)+x. 9057 (wt=32) [para(8928,7)] n(n(n(x+x+x)+n(x+x)+x+x+x+x+x)+n(x+x)) = x+x. 9060 (wt=49) [para(8928,7)] n(n(n(n(x+x+x)+n(x+x)+x+x+x)+n(x+x))+n(x+x)) = n(n(x+x+x)+n(x+x)+x+x+x). 9074 (wt=45) [para(8871',8874)] n(n(n(n(x+x+x)+x)+n(x+x+x)+y)+n(x+x+x+x+x+y)) = n(n(x+x+x)+x)+y. 9088 (wt=35) [para(8871',8884),demod([8871,8871,8871,8871,8871,8871,8871,8871])] n(n(n(n(n(n(x+x+x)+x)+n(x+x+x)+x))+x+x)+n(x+x)) = x+x. 9122 (wt=50) [para(8941,7)] n(n(n(n(n(x)+x+x)+x+x+x+x)+n(x)+x)+n(n(x)+x+x)) = n(n(n(x)+x+x)+x+x+x+x)+x. 9153 (wt=30) [para(22,8904),demod([9019]),flip(1)] n(n(x+x+x)+n(x)+x+x+x+x) = n(n(x+x+x)+x+x). 9154 (wt=27) [back_demod(9019),demod([9153])] n(n(n(x+x+x)+x+x)+x+x+x+x) = n(x+x+x). 9157 (wt=17) [para(9154,7),demod([8859])] x+x+x+x+x = x+x+x+x. 9173 (wt=43) [back_demod(9074),demod([9157])] n(n(n(n(x+x+x)+x)+n(x+x+x)+y)+n(x+x+x+x+y)) = n(n(x+x+x)+x)+y. 9174 (wt=13) [back_demod(9009),demod([9157,9157,9157,9157,8902,8887,9157,9157]),flip(1)] x+x+x+x = x+x+x. 9175 (wt=46) [back_demod(9122),demod([9174,9174])] n(n(n(n(n(x)+x+x)+x+x+x)+n(x)+x)+n(n(x)+x+x)) = n(n(n(x)+x+x)+x+x+x)+x. 9256 (wt=41) [back_demod(9173),demod([9174])] n(n(n(n(x+x+x)+x)+n(x+x+x)+y)+n(x+x+x+y)) = n(n(x+x+x)+x)+y. 9276 (wt=28) [back_demod(9057),demod([9174,9174])] n(n(n(x+x+x)+n(x+x)+x+x+x)+n(x+x)) = x+x. 9277 (wt=28) [back_demod(9060),demod([9276]),flip(1)] n(n(x+x+x)+n(x+x)+x+x+x) = n(n(x+x)+x+x). 9281 (wt=23) [back_demod(8975),demod([9277])] n(n(n(x+x)+x+x)+x+x+x) = n(x+x+x). 9282 (wt=21) [back_demod(8911),demod([9281])] n(n(x+x+x)+x+x) = n(n(x+x)+x+x). 9291 (wt=27) [back_demod(8950),demod([9282,9282])] n(n(n(n(x+x)+x+x)+x+x)+n(n(x+x)+x+x)) = x. 9293 (wt=19) [back_demod(9276),demod([9277])] n(n(n(x+x)+x+x)+n(x+x)) = x+x. 9294 (wt=19) [back_demod(8928),demod([9277])] n(n(n(x+x)+x+x)+x+x) = n(x+x). 9295 (wt=5) [back_demod(9291),demod([9294,9293])] x+x = x. 9598 (wt=41) [back_demod(7924),demod([9295,9295,9295])] n(n(n(n(n(n(n(n(x)+x)+n(x)))+n(n(x)+x)+n(x)))+n(n(x)+x)+n(x))+n(n(x)+x)) = n(x). 9942 (wt=19) [back_demod(3815),demod([9295,9295,9295,11,9295]),flip(1)] n(n(n(x)+y)+x+y) = n(n(n(x)+y)+y). 10579 (wt=32) [back_demod(9175),demod([9295,9295,9295,9295,9295,9295,9295])] n(n(n(n(n(x)+x)+x)+n(x)+x)+n(n(x)+x)) = n(n(n(x)+x)+x)+x. 10931 (wt=17) [back_demod(11),demod([9942])] n(n(n(n(x)+y)+y)+y) = n(n(x)+y). 10941 (wt=19) [back_demod(8931),demod([9295,9295,10931,9295])] n(n(n(n(x)+x)+n(x)+y)+n(x+y)) = y. 10943 (wt=11) [back_demod(8882),demod([9295,9295,10931,9295])] n(n(n(x)+x)+n(x)) = x. 10946 (wt=11) [back_demod(9598),demod([10943,9295,10943,9295,10943])] n(n(n(x)+x)+x) = n(x). 10978 (wt=11) [back_demod(10579),demod([10946,9295,9295,10946])] n(n(n(x)+x)) = n(x)+x. 10987 (wt=17) [back_demod(9088),demod([9295,9295,9295,9295,10978,9295,9295,9295,9295])] n(n(n(n(x)+x)+n(x)+x)+n(x)) = x. 11080 (wt=9) [back_demod(9053),demod([9295,9295,9295,9295,9295,9295,10987,9295,9295,9295,9295]),flip(1)] n(n(x)+x)+x = x. 13507 (wt=9) [back_demod(9256),demod([9295,9295,9295,9295,9295,9295,10941,9295,9295]),flip(1)] n(n(x)+x)+y = y. 13516 (wt=5) [back_demod(8903),demod([9295,9295,9295,9295,11080,9295,9295,13507,9295,9295,11080])] n(n(x)) = x. 13546 (wt=13) [para(7,13516),flip(1)] n(n(x)+y)+n(x+y) = n(y). 13555 (wt=3) [back_demod(8),demod([13546,13516])] -(A = A). UNIT CONFLICT from 13555 and x=x at 928808.75 seconds. ------------ end of proof -------------