----- Otter 3.0.4, August 1995 -----
The job was started by mccune on gyro, Wed Nov  1 21:56:33 1995
-----> EMPTY CLAUSE at   2.82 sec ----> 726 [hyper,2,286.1,293.1]  -> .

Length of proof is 17.  Level of proof is 9.

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

2 [] B+B@ =A+A@ , B*B@ =A*A@  -> .
3 []  -> (x*y)+ ((y*z)+ (z*x))= (x+y)* ((y+z)* (z+x)).
5 []  -> x+ (y* (x*z))=x.
7 []  -> ((x*y)+ (y*z))+y=y.
10,9 []  -> (x+x@ )*y=y.
11 []  -> x* (y+ (x+z))=x.
15 []  -> (x*x@ )+y=y.
22,21 [para_from,15.1.1,9.1.1.1]  -> (x*x@ )@ *y=y.
28,27 [para_into,5.1.1.2,9.1.1]  -> x+ (x*y)=x.
37 [para_into,7.1.1.1.1,9.1.1,demod,28]  -> x+x=x.
43 [para_into,7.1.1.1,5.1.1]  -> (x*y)+y=y.
49 [para_into,11.1.1.2.2,37.1.1]  -> x* (y+x)=x.
55 [para_into,11.1.1.2,43.1.1]  -> x* (x+y)=x.
69 [para_into,49.1.1.2,27.1.1]  -> (x*y)*x=x*y.
150,149 [para_into,21.1.1,55.1.1,flip.1]  -> (x*x@ )@ +y= (x*x@ )@ .
152,151 [para_into,21.1.1,49.1.1,flip.1]  -> x+ (y*y@ )@ = (y*y@ )@ .
155 [para_from,21.1.1,3.1.1.2.1,demod,28,152,150,22,22]  -> (x* (y*y@ )@ )+z=z+x.
158 [copy,155,flip.1]  -> x+y= (y* (z*z@ )@ )+x.
160,159 [para_into,69.1.1.1,21.1.1,demod,22]  -> x* (y*y@ )@ =x.
163 [para_into,69.1.1.1,9.1.1,demod,10]  -> x* (y+y@ )=x.
165 [back_demod,158,demod,160]  -> x+y=y+x.
182 [para_into,165.1.1,15.1.1,flip.1]  -> x+ (y*y@ )=x.
286 [para_into,163.1.1,9.1.1]  -> x+x@ =y+y@ .
293 [para_into,182.1.1,15.1.1]  -> x*x@ =y*y@ .
726 [hyper,2,286.1,293.1]  -> .

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