----- EQP 0.9, June 1996 -----
The job began on cosmo.mcs.anl.gov, Mon Oct 21 14:53:57 1996
UNIT CONFLICT from 88 and x=x at   5.19 seconds.

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

1 (wt=5) [] C + C = C.
2 (wt=13) [] n(n(n(x) + y) + n(x + y)) = y.
3 (wt=14) [] -(n(B + n(A)) + n(n(B) + n(A)) = A).
4 (wt=11) [para(1,2)] n(n(C) + n(C + n(C))) = C.
5 (wt=17) [para(1',2)] n(n(C + n(C) + x) + n(C + x)) = C + x.
8 (wt=19) [para(4,2)] n(n(C + x) + n(n(C) + n(C + n(C)) + x)) = x.
9 (wt=14) [para(4,2)] n(C + n(C + n(C) + n(C))) = n(C).
13 (wt=17) [para(1,8)] n(n(C) + n(C + n(C) + n(C + n(C)))) = C.
20 (wt=14) [para(9,2),demod([1])] n(n(C) + n(C + n(C) + n(C))) = C.
22 (wt=14) [para(9,2),demod([20]),flip(1)] n(C + n(C) + n(C)) = n(C + n(C)).
24 (wt=11) [back_demod(9),demod([22])] n(C + n(C + n(C))) = n(C).
32 (wt=9) [para(24,5),demod([13]),flip(1)] C + n(C + n(C)) = C.
35 (wt=9) [para(32',2),demod([8]),flip(1)] n(C + n(C)) + x = x.
42 (wt=13) [para(35,2),demod([35])] n(n(n(x)) + n(x)) = n(C + n(C)).
50 (wt=11) [para(42,2),demod([35])] n(n(n(n(x)) + x)) = n(n(x)).
52 (wt=7) [para(42,2),demod([35,50])] n(n(n(x))) = n(x).
58 (wt=5) [para(2,52),demod([2])] n(n(x)) = x.
87 (wt=13) [para(2,58),flip(1)] n(n(x) + y) + n(x + y) = n(y).
88 (wt=3) [back_demod(3),demod([87,58])] -(A = A).

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