----- EQP 0.9, June 1996 -----

The job began on eyas08.mcs.anl.gov, Fri Nov 15 09:33:08 1996

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

5 (wt=5) [] -(x+y = x).
7 (wt=13) [] n(n(n(x)+y)+n(x+y)) = y.
10 (wt=18) [para(7,7)] n(n(n(x+y)+n(x)+y)+y) = n(x+y).
11 (wt=19) [para(7,7)] n(n(n(n(x)+y)+x+y)+y) = n(n(x)+y).
29 (wt=21) [para(11,7)] n(n(n(n(x)+y)+x+y+y)+n(n(x)+y)) = y.
54 (wt=29) [para(29,7)] n(n(n(n(n(x)+y)+x+y+y)+n(n(x)+y)+z)+n(y+z)) = z.
217 (wt=34) [para(54,7)] n(n(n(n(n(x)+y)+x+y+y)+n(n(x)+y)+n(y+z)+z)+z) = n(y+z).
674 (wt=42) [para(217,7)] n(n(n(n(n(n(x)+y)+x+y+y)+n(n(x)+y)+n(y+z)+z)+z+u)+n(n(y+z)+u)) = u.
6736 (wt=49) [para(10,674)] n(n(n(n(x+x+x)+x)+n(x+x+x))+n(n(n(x+x+x)+x)+x+x+x+x+x)) = n(n(x+x+x)+x).
8855 (wt=27) [para(6736,7),demod([54]),flip(1)] n(n(n(x+x+x)+x)+x+x+x+x+x) = n(x+x+x).
8865 (wt=43) [para(8855,7)] n(n(n(n(x+x+x)+x)+n(x+x+x)+x+x)+n(x+x+x)) = n(n(x+x+x)+x)+x+x.
8866 (wt=19) [para(8855,7),demod([11])] n(n(n(x+x+x)+x)+n(x+x+x)) = x.
8870 (wt=27) [para(8866,7)] n(n(n(n(x+x+x)+x)+n(x+x+x)+y)+n(x+y)) = y.
8871 (wt=17) [back_demod(8865),demod([8870]),flip(1)] n(n(x+x+x)+x)+x+x = x+x.

UNIT CONFLICT from 8871 and 5 at 867010.30 seconds.

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