----- Otter 3.0.4a, November 1995 -----
The job was started by mccune on gyro, Fri May  3 09:39:28 1996
-----> EMPTY CLAUSE at   0.27 sec ----> 61 [back_demod,34,demod,52,unit_del,1,53] $F.

Length of proof is 18.  Level of proof is 12.

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

1 [] x=x.
2 [] $c3@ +$c3!=$c2@ +$c2| ($c3@ +$c3)+$c2!=$c2|$c3+$c2!=$c2+$c3| ($c3+$c2)+$c1!=$c3+ ($c2+$c1).
3 [] x+y!=z+u| (y@ +z)+u=x.
4 [hyper,3,1] (x@ +y)+x=y.
7,6 [hyper,3,4] (x@ +y)+z=x@ + (y+z).
8 [back_demod,4,demod,7] x@ + (y+x)=y.
11 [back_demod,2,demod,7] $c3@ +$c3!=$c2@ +$c2|$c3@ + ($c3+$c2)!=$c2|$c3+$c2!=$c2+$c3| ($c3+$c2)+$c1!=$c3+ ($c2+$c1).
14 [para_into,8.1.1.2,8.1.1] (x+y)@ +x=y@ .
16 [para_into,6.1.1.1,8.1.1,flip.1] x@ + ((y+x)+z)=y+z.
21,20 [para_into,14.1.1.1.1,8.1.1,flip.1] (x+y)@ =x@ +y@ .
22 [para_from,20.1.1,8.1.1.1,demod,7] x@ + (y@ + (z+ (x+y)))=z.
25,24 [para_into,22.1.1.2,16.1.1] x@ + (y+ (x+z))=y+z.
28 [para_into,24.1.1.2,22.1.1,demod,25] x@ @ +y=y+x.
29 [para_into,24.1.1.2,8.1.1] x@ +x=y@ +y.
31,30 [para_into,24.1.1,16.1.1,flip.1] (x+y)+z=x+ (y+z).
33 [copy,28,flip.1] x+y=y@ @ +x.
34 [back_demod,11,demod,31,unit_del,29,1] $c3@ + ($c3+$c2)!=$c2|$c3+$c2!=$c2+$c3.
37 [para_into,28.1.1,8.1.1,demod,31,flip.1] x+ (y@ +y)=x.
46,45 [para_into,33.1.1,28.1.1,flip.1] x@ @ +y@ @ =x+y.
52,51 [para_from,33.1.1,37.1.1,demod,21,21,46,31] x@ + (x+y)=y.
53 [para_from,33.1.1,24.1.1.2,demod,21,21,46,31,52] x+y=y+x.
61 [back_demod,34,demod,52,unit_del,1,53] $F.

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