----- EQP 0.9, June 1996 -----
The job began on cosmo.mcs.anl.gov, Mon Oct 21 15:15:20 1996
UNIT CONFLICT from 1802 and 1 at 2319.30 seconds.

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

1 (wt=5) [] -(x + x = x).
2 (wt=5) [] D + C = C.
3 (wt=13) [] n(n(n(x) + y) + n(x + y)) = y.
4 (wt=11) [para(2,3)] n(n(C) + n(D + n(C))) = D.
8 (wt=21) [para(2',3)] n(n(D + n(C + x) + y) + n(C + x + y)) = D + y.
20 (wt=17) [para(4,3)] n(D + n(C + n(D + n(C)))) = n(D + n(C)).
34 (wt=21) [para(3,3)] n(n(n(n(x) + y) + n(x + y) + z) + n(y + z)) = z.
35 (wt=19) [para(3,3)] n(n(n(n(x) + y) + x + y) + y) = n(n(x) + y).
56 (wt=19) [para(2,34)] n(n(C) + n(D + n(C + n(x)) + n(C + x))) = D.
151 (wt=25) [para(20,3)] n(n(D + n(C + n(D + n(C))) + x) + n(n(D + n(C)) + x)) = x.
152 (wt=17) [para(20,3),demod([2])] n(n(D + n(C)) + n(C + n(D + n(C)))) = D.
173 (wt=26) [para(152,3)] n(D + n(D + n(C) + n(C + n(D + n(C))))) = n(C + n(D + n(C))).
197 (wt=23) [para(2',151)] n(n(C + n(D + n(C))) + n(C + n(C + n(D + n(C))))) = C.
280 (wt=27) [para(35,3)] n(n(n(n(n(x) + y) + x + y) + y + z) + n(n(n(x) + y) + z)) = z.
837 (wt=11) [para(4,151),demod([173])] n(C + n(D + n(C))) = n(C).
839 (wt=11) [back_demod(197),demod([837,837])] n(n(C) + n(C + n(C))) = C.
842 (wt=19) [para(839,3)] n(n(C + x) + n(n(C) + n(C + n(C)) + x)) = x.
844 (wt=17) [para(839,3)] n(C + n(C + n(C + n(C)))) = n(C + n(C)).
883 (wt=19) [para(844,3)] n(n(C + n(C)) + n(C + C + n(C + n(C)))) = C.
946 (wt=30) [para(883,3)] n(C + n(C + n(C) + n(C + C + n(C + n(C))))) = n(C + C + n(C + n(C))).
1706 (wt=13) [para(839,280),demod([946])] n(C + C + n(C + n(C))) = n(C).
1734 (wt=9) [para(1706,8),demod([56]),flip(1)] D + n(C + n(C)) = D.
1745 (wt=9) [para(2',1734'),demod([2])] C + n(C + n(C)) = C.
1802 (wt=9) [para(1745',3),demod([842]),flip(1)] n(C + n(C)) + x = x.

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