----- Otter 3.0.4, August 1995 -----
The job was started by mccune on gyro, Wed Nov  1 22:03:26 1995
----> UNIT CONFLICT at   4.08 sec ----> 818 [binary,816.1,145.1] $F.

Length of proof is 13.  Level of proof is 4.

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

4 [] x^y=y^x.
6,5 [] (x^y)^z=x^ (y^z).
9 [] x v y=y v x.
10 [] (x v y) v z=x v (y v z).
12 [] x^ (x v y)=x.
14 [] x v (x^y)=x.
16 [] x^ (y v z)= (x^y) v (x^z).
17 [copy,16,flip.1] (x^y) v (x^z)=x^ (y v z).
19 [] A v (B^C)!= (A v B)^ (A v C).
20 [para_into,12.1.1.2,9.1.1] x^ (y v x)=x.
22 [para_into,12.1.1,4.1.1] (x v y)^x=x.
35 [para_into,14.1.1.2,4.1.1] x v (y^x)=x.
39 [para_into,20.1.1.2,14.1.1,demod,6] x^ (y^x)=x^y.
53 [para_into,35.1.1,9.1.1] (x^y) v y=y.
55 [para_into,10.1.1.1,35.1.1,flip.1] x v ((y^x) v z)=x v z.
70 [para_from,10.1.1,22.1.1.1] (x v (y v z))^ (x v y)=x v y.
91,90 [para_into,17.1.1.1,22.1.1] x v ((x v y)^z)= (x v y)^ (x v z).
145 [para_into,19.1.1.2,4.1.1] A v (C^B)!= (A v B)^ (A v C).
346,345 [para_into,55.1.1.2,17.1.1] x v (y^ (x v z))=x v (y^z).
502,501 [para_into,70.1.1.1.2,53.1.1] (x v y)^ (x v (z^y))=x v (z^y).
816 [para_into,90.1.1.2,39.1.1,demod,91,346,502,flip.1] x v (y^z)= (x v z)^ (x v y).
818 [binary,816.1,145.1] $F.

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