----- EQP 0.9a, Feb 1997 -----
The job began on gyro.isdn.mcs.anl.gov, Thu Sep 11 10:39:40 1997
UNIT CONFLICT from 22528 and x=x at 80696.70 seconds.

---------------- PROOF ----------------

1 (wt=5) [] c(c(x)) = x.
2 (wt=11) [] c(x) v (x v y) = c(x) v 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.
8 (wt=5) [back_demod(2),demod([7,7])] 1 v x = 1.
13 (wt=25) [] -(B v (c(A) v c((B ^ c(A)) v ((A ^ (B v c(A))) v (c(B) ^ c(A))))) = 1).
14 (wt=10) [para(4,1),flip(1)] c(x) v c(y) = c(x ^ y).
15 (wt=24) [back_demod(13),demod([14])] -(B v c(A ^ ((B ^ c(A)) v ((A ^ (B v c(A))) v (c(B) ^ c(A))))) = 1).
16 (wt=10) [para(1,4)] c(c(x) v y) = c(y) ^ x.
22 (wt=10) [para(16,1)] c(c(x) ^ y) = c(y) v x.
23 (wt=10) [para(1,16),flip(1)] c(x) ^ c(y) = c(x v y).
24 (wt=23) [back_demod(15),demod([23])] -(B v c(A ^ (c(B v A) v ((B ^ c(A)) v (A ^ (B v c(A)))))) = 1).
25 (wt=8) [para(3,16),demod([1,22]),flip(1)] (c(x) v y) ^ y = y.
27 (wt=7) [para(1,25)] (x v y) ^ y = y.
28 (wt=11) [para(16,7)] c(x) v ((c(y) ^ x) v y) = 1.
31 (wt=15) [para(27',3)] ((x v y) ^ z) v (y ^ z) = (x v y) ^ z.
32 (wt=15) [para(3',27)] ((x ^ y) v z) ^ (y v z) = (x ^ y) v z.
33 (wt=15) [para(16,16)] c((c(x) ^ y) v z) = c(z) ^ (c(y) v x).
38 (wt=14) [para(27',22),demod([22]),flip(1)] c((c(x) v y) ^ z) v x = c(z) v x.
146 (wt=20) [para(14,32)] c(x ^ y) ^ (c(y) v (c(x) ^ z)) = c(y) v (c(x) ^ z).
174 (wt=20) [para(22,33),flip(1)] c(x) ^ (c(y) v (c(z) ^ u)) = c(((c(u) v z) ^ y) v x).
175 (wt=15) [back_demod(146),demod([174,31])] c((c(x) v y) ^ z) = c(z) v (c(y) ^ x).
281 (wt=18) [para(38',28'),demod([8])] c(x) v ((c(y) ^ ((c(z) v u) ^ x)) v (y v z)) = 1.
2662 (wt=18) [para(3',281)] c(x) v ((c(y ^ z) ^ ((c(z) v u) ^ x)) v z) = 1.
2663 (wt=17) [para(1,2662),demod([23])] (c((x ^ y) v z) ^ (c(y) v u)) v (y v z) = 1.
2664 (wt=18) [para(1,2663)] c(x) v ((c((c(x) ^ y) v z) ^ (x v u)) v z) = 1.
3141 (wt=23) [para(2664',3'),demod([8]),flip(1)] c(x) v ((c((c(x) ^ y) v ((c(x) v z) ^ u)) ^ (x v v)) v z) = 1.
22528 (wt=3) [para(175,24),demod([3141])] -(1 = 1).

------------ end of proof -------------