The job began on dopey.mcs.anl.gov, Thu Jun 13 14:32:31 1996
UNIT CONFLICT from 3733 and 1 at 608688.73 seconds.

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

1 (wt=5) [] -(x + y = x).
2 (wt=7) [] n(D + C) = n(C).
3 (wt=13) [] n(n(n(x) + y) + n(x + y)) = y.
4 (wt=15) [para(2,3)] n(n(D + C + x) + n(n(C) + x)) = x.
5 (wt=11) [para(2,3)] n(n(C) + n(D + n(C))) = D.
7 (wt=19) [para(5,3)] n(n(D + x) + n(n(C) + n(D + n(C)) + x)) = x.
9 (wt=17) [para(5,3)] n(D + n(C + n(D + n(C)))) = n(D + n(C)).
18 (wt=19) [para(3,3)] n(n(n(n(x) + y) + x + y) + y) = n(n(x) + y).
25 (wt=21) [para(2,18),demod([2])] n(n(D + C + n(n(C) + x) + x) + x) = n(n(C) + x).
35 (wt=23) [para(4,3)] n(n(n(D + C + x) + n(n(C) + x) + y) + n(x + y)) = y.
64 (wt=19) [para(9,3)] n(n(D + n(C)) + n(D + C + n(D + n(C)))) = D.
141 (wt=21) [para(18,3)] n(n(n(n(x) + y) + x + y + y) + n(n(x) + y)) = y.
145 (wt=26) [para(3,18),demod([3])] n(n(n(n(x) + y) + n(x + y) + n(y + z) + z) + z) = n(y + z).
170 (wt=30) [para(64,3)] n(D + n(D + n(C) + n(D + C + n(D + n(C))))) = n(D + C + n(D + n(C))).
287 (wt=29) [para(141,3)] n(n(n(n(n(x) + y) + x + y + y) + n(n(x) + y) + z) + n(y + z)) = z.
298 (wt=13) [para(5,35),demod([5,170])] n(D + C + n(D + n(C))) = n(C).
826 (wt=30) [para(5,145),demod([5])] n(n(D + n(C)) + n(D + n(D + n(C)) + n(n(C) + n(x)) + n(n(C) + x))) = D.
1234 (wt=34) [para(145,3)] n(n(n(n(n(x) + y) + n(x + y) + n(y + z) + z) + z + u) + n(n(y + z) + u)) = u.
1475 (wt=15) [para(25,7),demod([287]),flip(1)] n(D + D + C + n(D + n(C))) = n(C).
1498 (wt=29) [para(1475,18),demod([1475])] n(n(D + D + C + n(D + n(C)) + n(n(C) + x) + x) + x) = n(n(C) + x).
3318 (wt=33) [para(5,1234)] n(D + n(D + n(C) + n(D + n(D + n(C)) + n(n(C) + n(x)) + n(n(C) + x)))) = n(C).
3707 (wt=24) [para(826,35),demod([298,5,3318]),flip(1)] n(D + n(D + n(C)) + n(n(C) + n(x)) + n(n(C) + x)) = n(C).
3708 (wt=26) [para(2,3707)] n(D + n(D + n(C)) + n(D + C + n(C)) + n(n(C) + n(C))) = n(C).
3733 (wt=21) [para(3708,3),demod([1498]),flip(1)] D + n(D + n(C)) + n(n(C) + n(C)) = n(n(C) + n(C)).

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