----- Otter 3.0.4, August 1995 -----
The job was started by mccune on gyro, Wed Nov  1 22:03:40 1995
----> UNIT CONFLICT at  11.74 sec ----> 2281 [binary,2280.1,127.1] $F.

Length of proof is 40.  Level of proof is 10.

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

3,2 [] x^x=x.
4 [] x^y=y^x.
6,5 [] (x^y)^z=x^ (y^z).
8,7 [] x v x=x.
9 [] x v y=y v x.
11,10 [] (x v y) v z=x v (y v z).
12 [] x^ (x v y)=x.
15,14 [] x v (x^y)=x.
16 [] (((x^y) v z)^y) v (z^x)= (((x v y)^z) v y)^ (z v x).
20 [] A v (B^C)!= (A v B)^ (A v C).
21 [para_into,5.1.1.1,4.1.1,demod,6] x^ (y^z)=y^ (x^z).
22 [para_into,5.1.1.1,2.1.1,flip.1] x^ (x^y)=x^y.
29,28 [para_into,12.1.1.2,9.1.1] x^ (y v x)=x.
33,32 [para_into,12.1.1,4.1.1] (x v y)^x=x.
36 [para_into,10.1.1.1,9.1.1,demod,11] x v (y v z)=y v (x v z).
38,37 [para_into,10.1.1.1,7.1.1,flip.1] x v (x v y)=x v y.
47 [para_into,14.1.1.2,4.1.1] x v (y^x)=x.
51 [para_into,14.1.1,9.1.1] (x^y) v x=x.
53 [para_from,14.1.1,10.1.1.1,flip.1] x v ((x^y) v z)=x v z.
56,55 [para_into,28.1.1.2,14.1.1,demod,6] x^ (y^x)=x^y.
57 [para_into,28.1.1.2,10.1.1] x^ (y v (z v x))=x.
61 [para_into,28.1.1,4.1.1] (x v y)^y=y.
67 [para_into,16.1.1.1.1.1,4.1.1] (((x^y) v z)^x) v (z^y)= (((y v x)^z) v x)^ (z v y).
76 [para_into,16.1.1.2,12.1.1,demod,11,33,38] ((((x v y)^z) v x)^z) v x= (x v z)^ (x v y).
89 [para_from,32.1.1,16.1.1.1.1.1,demod,33,11,flip.1] (((x v (y v x))^z) v x)^ (z v (x v y))=x v (z^ (x v y)).
92,91 [para_from,32.1.1,14.1.1.2,demod,11] x v (y v x)=x v y.
94,93 [para_from,32.1.1,5.1.1.1,flip.1] (x v y)^ (x^z)=x^z.
95 [back_demod,89,demod,92] (((x v y)^z) v x)^ (z v (x v y))=x v (z^ (x v y)).
110,109 [para_from,47.1.1,10.1.1.1,flip.1] x v ((y^x) v z)=x v z.
118 [para_into,61.1.1.1,16.1.1,demod,6,94] (((x v y)^z) v y)^ (z^x)=z^x.
122 [para_from,61.1.1,16.1.1.1.1.1,demod,33,11,8,flip.1] (((x v y)^z) v y)^ (z v (x v y))=y v (z^ (x v y)).
127 [para_into,20.1.1,9.1.1] (B^C) v A!= (A v B)^ (A v C).
141,140 [para_into,21.1.1.2,61.1.1,flip.1] (x v y)^ (z^y)=z^y.
142 [para_into,21.1.1.2,32.1.1,flip.1] (x v y)^ (z^x)=z^x.
207,206 [para_from,91.1.1,57.1.1.2.2] (x v y)^ (z v (y v x))=x v y.
559,558 [para_from,109.1.1,57.1.1.2.2] ((x^y) v z)^ (u v (y v z))= (x^y) v z.
696,695 [para_into,140.1.1.2,55.1.1,demod,56] (x v (y^z))^ (z^y)=z^y.
747,746 [para_into,142.1.1.2,55.1.1,demod,56] ((x^y) v z)^ (y^x)=y^x.
936 [para_from,67.1.1,53.1.1.2,demod,11,11,15] (x^y) v (z v ((((y v x)^z) v x)^ (z v y)))= (x^y) v z.
1222,1221 [para_into,76.1.1.1.1.1,55.1.1,demod,747] (x^ (y v z)) v y= (y v (x^ (y v z)))^ (y v z).
1224,1223 [para_into,76.1.1.1.1.1,22.1.1,demod,33] ((x v y)^z) v x= (x v ((x v y)^z))^ (x v y).
1226,1225 [para_into,76.1.1.1.1.1,4.1.1,demod,1222,6,696,1224] (x v ((x v y)^z))^ (x v y)= (x v z)^ (x v y).
1234,1233 [para_into,76.1.1,9.1.1,demod,1224,1226,6,141] x v ((x v y)^z)= (x v z)^ (x v y).
1246,1245 [back_demod,95,demod,1224,1234,6,3,6,29,flip.1] x v (y^ (x v z))= (x v y)^ (x v z).
1248,1247 [back_demod,1223,demod,1234,6,3] ((x v y)^z) v x= (x v z)^ (x v y).
1254,1253 [back_demod,936,demod,1246,110] (x^y) v ((z v x)^ (z v y))= (x^y) v z.
2199 [para_from,118.1.1,51.1.1.1] (x^y) v (((y v z)^x) v z)= ((y v z)^x) v z.
2238,2237 [para_into,122.1.1.1.1.1,9.1.1,demod,1248,6,207,flip.1] x v (y^ (z v x))= (x v y)^ (x v z).
2265,2264 [para_into,122.1.1.2,36.1.1,demod,559,2238] ((x v y)^z) v y= (y v z)^ (y v x).
2280 [back_demod,2199,demod,2265,1254,2265] (x^y) v z= (z v x)^ (z v y).
2281 [binary,2280.1,127.1] $F.

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