----- EQP 0.9a, Feb 1997 ----- The job began on gyro.isdn.mcs.anl.gov, Thu Sep 11 09:08:11 1997 UNIT CONFLICT from 162 and x=x at 4.18 seconds. ---------------- PROOF ---------------- 1 (wt=5) [] c(c(x)) = x. 3 (wt=7) [] (x ^ y) v x = x. 4 (wt=10) [flip(1)] c(c(x) v c(y)) = x ^ y. 7 (wt=6) [] c(x) v x = 1. 13 (wt=29) [] -(A v ((c(A) ^ ((B ^ c(A)) v (c(B) ^ c(A)))) v (c(A) ^ ((B v A) ^ (A v c(B))))) = 1). 15 (wt=10) [para(1,4)] c(c(x) v y) = c(y) ^ x. 19 (wt=10) [para(15,1)] c(c(x) ^ y) = c(y) v x. 20 (wt=10) [para(1,15),flip(1)] c(x) ^ c(y) = c(x v y). 21 (wt=28) [back_demod(13),demod([20])] -(A v ((c(A) ^ (c(B v A) v (B ^ c(A)))) v (c(A) ^ ((B v A) ^ (A v c(B))))) = 1). 24 (wt=8) [para(3,15),demod([1,19]),flip(1)] (c(x) v y) ^ y = y. 26 (wt=7) [para(1,24)] (x v y) ^ y = y. 27 (wt=11) [para(15,7)] c(x) v ((c(y) ^ x) v y) = 1. 30 (wt=15) [para(15,15)] c((c(x) ^ y) v z) = c(z) ^ (c(y) v x). 32 (wt=15) [para(26',3)] ((x v y) ^ z) v (y ^ z) = (x v y) ^ z. 120 (wt=20) [para(19,30),flip(1)] c(x) ^ (c(y) v (c(z) ^ u)) = c(((c(u) v z) ^ y) v x). 121 (wt=27) [back_demod(21),demod([120])] -(A v (c(A v ((B v A) ^ (A v c(B)))) v (c(A) ^ ((B v A) ^ (A v c(B))))) = 1). 161 (wt=17) [para(26,32)] ((x v y) ^ (y v z)) v y = (x v y) ^ (y v z). 162 (wt=3) [back_demod(121),demod([161,27])] -(1 = 1). ------------ end of proof -------------