----- Otter 3.2c, December 2001 -----
----> UNIT CONFLICT at   8.25 sec ----> 14338 [binary,14337.1,1.1] $F.

Length of proof is 124.  Level of proof is 35.

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

1 [] x=x.
2 [] (((x v y)^y) v (((z^ (y v y)) v (u^y))^v))^ (w v ((v6 v y)^ (y v v7)))=y.
4 [] B v (A^ (B^C))!=B|B^ (A v (B v C))!=B| ((A^B) v (B^C)) v B!=B| ((A v B)^ (B v C))^B!=B.
5 [para_into,2.1.1.1.2,2.1.1] (((x v y)^y) v (y v y))^ (z v ((u v y)^ (y v v)))=y.
7 [para_into,5.1.1.2.2,5.1.1] (((x v (y v y))^ (y v y)) v ((y v y) v (y v y)))^ (z v y)=y v y.
9 [para_from,5.1.1,2.1.1.2.2] (((x v (y v y))^ (y v y)) v (((z^ ((y v y) v (y v y))) v (u^ (y v y)))^v))^ (w v y)=y v y.
13 [para_from,7.1.1,2.1.1.1.2.1.1] (((x v y)^y) v (((y v y) v (z^y))^u))^ (v v ((w v y)^ (y v v6)))=y.
17 [para_into,13.1.1.2.2,5.1.1] (((x v (y v y))^ (y v y)) v ((((y v y) v (y v y)) v (z^ (y v y)))^u))^ (v v y)=y v y.
19 [para_from,13.1.1,5.1.1.2.2] (((x v (((y v y) v (z^y))^u))^ (((y v y) v (z^y))^u)) v ((((y v y) v (z^y))^u) v (((y v y) v (z^y))^u)))^ (v v y)= ((y v y) v (z^y))^u.
21 [para_into,17.1.1.1.2.1.2,17.1.1] (((x v (y v y))^ (y v y)) v ((((y v y) v (y v y)) v (y v y))^z))^ (u v y)=y v y.
24,23 [para_into,9.1.1.1.2.1.2,21.1.1] (((x v (y v y))^ (y v y)) v (((z^ ((y v y) v (y v y))) v (y v y))^u))^ (v v y)=y v y.
39 [para_from,19.1.1,2.1.1.1.2.1.1] (((x v y)^y) v (((((y v y) v (z^y))^u) v (v^y))^w))^ (v6 v ((v7 v y)^ (y v v8)))=y.
48,47 [para_into,39.1.1.1.2,39.1.1] (((x v y)^y) v (z^y))^ (u v ((v v y)^ (y v w)))=y.
49 [para_into,47.1.1.1.2,23.1.1] (((x v (y v z))^ (y v z)) v (z v z))^ (u v ((v v (y v z))^ ((y v z) v w)))=y v z.
53 [para_into,47.1.1.2.2,47.1.1] (((x v (y^z))^ (y^z)) v (u^ (y^z)))^ (v v z)=y^z.
56,55 [para_into,47.1.1.2.2,13.1.1] (((x v (((y v y) v (z^y))^u))^ (((y v y) v (z^y))^u)) v (v^ (((y v y) v (z^y))^u)))^ (w v y)= ((y v y) v (z^y))^u.
59 [para_into,47.1.1.2.2,5.1.1] (((x v (y v y))^ (y v y)) v (z^ (y v y)))^ (u v y)=y v y.
67 [para_from,47.1.1,5.1.1.2.2] (((x v (y^z))^ (y^z)) v ((y^z) v (y^z)))^ (u v z)=y^z.
69 [para_from,47.1.1,2.1.1.2.2] (((x v (y^z))^ (y^z)) v (((u^ ((y^z) v (y^z))) v (v^ (y^z)))^w))^ (v6 v z)=y^z.
74,73 [para_into,53.1.1.1.1.1.2,47.1.1,demod,48,48,48] (((x v y)^y) v (z^y))^ (u v (v v ((w v y)^ (y v v6))))=y.
75 [para_into,53.1.1.1.1.1.2,23.1.1,demod,24,24,24] (((x v (y v y))^ (y v y)) v (z^ (y v y)))^ (u v (v v y))=y v y.
99 [para_from,53.1.1,2.1.1.1.2.1.1] (((x v y)^y) v (((z^y) v (u^y))^v))^ (w v ((v6 v y)^ (y v v7)))=y.
101 [para_into,59.1.1.1.2,59.1.1] (((x v (y v y))^ (y v y)) v (y v y))^ (z v y)=y v y.
103 [para_into,59.1.1.1.2,53.1.1] (((x v (y v y))^ (y v y)) v (z^y))^ (u v y)=y v y.
107 [para_into,101.1.1.1.1,101.1.1] ((x v x) v (x v x))^ (y v x)=x v x.
125 [para_from,101.1.1,59.1.1.1.1] ((x v x) v (y^ (x v x)))^ (z v x)=x v x.
135 [para_from,101.1.1,7.1.1.1.1] ((x v x) v ((x v x) v (x v x)))^ (y v x)=x v x.
141 [para_from,101.1.1,47.1.1.1.1] ((x v x) v (y^ (x v x)))^ (z v ((u v (x v x))^ ((x v x) v v)))=x v x.
161 [para_into,125.1.1.1.2,53.1.1] ((x v x) v (y^x))^ (z v x)=x v x.
165 [para_into,125.1.1.1.2,19.1.1] ((x v x) v (((x v x) v (y^x))^z))^ (u v x)=x v x.
167 [para_into,161.1.1.1.2,161.1.1] (((x v y) v (x v y)) v (y v y))^ (z v (x v y))= (x v y) v (x v y).
215 [para_from,73.1.1,53.1.1.1.2.2,demod,74,74,74] (((x v y)^y) v (z^y))^ (u v (v v (w v ((v6 v y)^ (y v v7)))))=y.
287 [para_into,75.1.1.1.1,107.1.1] ((x v x) v (y^ (x v x)))^ (z v (u v x))=x v x.
295 [para_into,75.1.1.1.2,67.1.1] (((x v (y v y))^ (y v y)) v (z^y))^ (u v (v v y))=y v y.
333 [para_into,287.1.1.1.2,165.1.1] ((x v x) v (x v x))^ (y v (z v x))=x v x.
475 [para_into,99.1.1.1.2,215.1.1] (((x v y)^y) v y)^ (z v ((u v y)^ (y v v)))=y.
497 [para_into,475.1.1.1.1,107.1.1] ((x v x) v (x v x))^ (y v ((z v (x v x))^ ((x v x) v u)))=x v x.
499 [para_into,475.1.1.2.2,475.1.1] (((x v y)^y) v y)^ (z v y)=y.
507 [para_into,475.1.1.2.2,215.1.1] (((x v (y^z))^ (y^z)) v (y^z))^ (u v z)=y^z.
521 [para_from,475.1.1,47.1.1.2.2] (((x v y)^y) v (z^y))^ (u v y)=y.
546,545 [para_from,475.1.1,5.1.1.2.2] (((x v y)^y) v (y v y))^ (z v y)=y.
548,547 [para_from,475.1.1,215.1.1.2.2.2.2] (((x v y)^y) v (z^y))^ (u v (v v (w v y)))=y.
549 [para_from,475.1.1,99.1.1.2.2] (((x v y)^y) v (((z^y) v (u^y))^v))^ (w v y)=y.
554,553 [para_from,499.1.1,287.1.1.1.2] ((x v x) v x)^ (y v (z v x))=x v x.
673 [para_into,545.1.1.1.1,107.1.1] ((x v x) v ((x v x) v (x v x)))^ (y v (x v x))=x v x.
691 [para_from,545.1.1,295.1.1.1.1] (x v (y^x))^ (z v (u v x))=x v x.
693 [para_from,545.1.1,103.1.1.1.1] (x v (y^x))^ (z v x)=x v x.
698,697 [para_from,545.1.1,101.1.1.1.1] (x v (x v x))^ (y v x)=x v x.
711 [para_from,545.1.1,23.1.1.1.1] (x v (((y^ ((x v x) v (x v x))) v (x v x))^z))^ (u v x)=x v x.
713 [para_from,545.1.1,21.1.1.1.1] (x v ((((x v x) v (x v x)) v (x v x))^y))^ (z v x)=x v x.
744,743 [back_demod,673,demod,698] (x v x) v (x v x)=x v x.
757 [back_demod,713,demod,744,744] (x v ((x v x)^y))^ (z v x)=x v x.
759 [back_demod,711,demod,744] (x v (((y^ (x v x)) v (x v x))^z))^ (u v x)=x v x.
799 [back_demod,497,demod,744] (x v x)^ (y v ((z v (x v x))^ ((x v x) v u)))=x v x.
834,833 [back_demod,333,demod,744] (x v x)^ (y v (z v x))=x v x.
880,879 [back_demod,135,demod,744,744] (x v x)^ (y v x)=x v x.
936,935 [para_from,743.1.1,49.1.1.2.2.2] (((x v (y v y))^ (y v y)) v (y v y))^ (z v ((u v (y v y))^ (y v y)))=y v y.
1024 [para_into,693.1.1.1.2,545.1.1] ((x v y) v y)^ (z v (x v y))= (x v y) v (x v y).
1032 [copy,1024,flip.1] (x v y) v (x v y)= ((x v y) v y)^ (z v (x v y)).
1067 [para_into,55.1.1.2,743.1.1,demod,744,744,744,744] (((x v (((y v y) v (z^ (y v y)))^u))^ (((y v y) v (z^ (y v y)))^u)) v (v^ (((y v y) v (z^ (y v y)))^u)))^ (y v y)= ((y v y) v (z^ (y v y)))^u.
1183 [para_into,757.1.1.1.2.1,743.1.1,demod,744] ((x v x) v ((x v x)^y))^ (z v (x v x))=x v x.
1185 [para_into,757.1.1.1.2,521.1.1] (((x v y)^y) v y)^ (z v ((x v y)^y))= ((x v y)^y) v ((x v y)^y).
1186 [para_into,757.1.1.1.2,75.1.1,demod,936,flip.1] ((x v (y v y))^ (y v y)) v ((x v (y v y))^ (y v y))=y v y.
1526,1525 [para_into,1032.1.1.2,1032.1.1,demod,554] ((x v y) v (x v y)) v (((x v y) v y)^ (z v (x v y)))= (x v y) v (x v y).
1994 [para_into,1183.1.1.1.2,547.1.1] ((((x v y)^y) v ((x v y)^y)) v y)^ (z v (((x v y)^y) v ((x v y)^y)))= ((x v y)^y) v ((x v y)^y).
2194 [para_into,507.1.1.1.1.1.2,547.1.1,demod,548,548,548] (((x v y)^y) v y)^ (z v (u v (v v (w v y))))=y.
2197,2196 [para_into,507.1.1.1.1.1.2,545.1.1,demod,546,546,546] (((x v y)^y) v y)^ (z v (u v y))=y.
2250 [para_into,2194.1.1.1.1.1,743.1.1,demod,880,744] (x v x)^ (y v (z v (u v (v v (x v x)))))=x v x.
2396 [para_into,549.1.1.1.2,2250.1.1] (((x v y)^y) v ((z^y) v (z^y)))^ (u v y)=y.
2602 [para_into,759.1.1.1.2.1.1,507.1.1] (x v (((y^x) v (x v x))^z))^ (u v x)=x v x.
2676 [para_into,799.1.1.2.2.1,1032.1.1,demod,554] (x v x)^ (y v ((x v x)^ ((x v x) v z)))=x v x.
2681,2680 [para_into,799.1.1.2.2,2396.1.1] ((x^y) v (x^y))^ (z v y)= (x^y) v (x^y).
2683,2682 [para_into,799.1.1.2.2,167.1.1] (x v x)^ (y v ((z v x) v (z v x)))=x v x.
2692 [para_into,2682.1.1.2.2,1032.1.1] (x v x)^ (y v (((z v x) v x)^ (u v (z v x))))=x v x.
2700 [para_from,2682.1.1,69.1.1.1.2.1.2.2,demod,2683,2683,2683,2683,744,2683] (((x v (y v y))^ (y v y)) v (((z^ (y v y)) v (u^ (y v y)))^v))^ (w v (v6 v ((v7 v y) v (v7 v y))))=y v y.
2744 [para_into,141.1.1.1.2,2396.1.1] ((x v x) v x)^ (y v ((z v (x v x))^ ((x v x) v u)))=x v x.
2768 [para_into,2680.1.1.1.1,2680.1.1,demod,2681,744,2681,2681,744] ((x^y) v (x^y))^ (z v (u v y))= (x^y) v (x^y).
2776 [para_into,2680.1.1.1.1,2196.1.1,demod,2197,2197,2197] (x v x)^ (y v (z v (u v x)))=x v x.
2780 [para_into,2680.1.1.1.1,1024.1.1,demod,1526,834,flip.1] (((x v y) v y)^ (z v (x v y))) v (((x v y) v y)^ (z v (x v y)))= (x v y) v (x v y).
2794 [para_into,2680.1.1.1.1,55.1.1,demod,56,56,56] ((((x v x) v (y^x))^z) v (((x v x) v (y^x))^z))^ (u v (v v x))= (((x v x) v (y^x))^z) v (((x v x) v (y^x))^z).
2801,2800 [para_into,2680.1.1,521.1.1,flip.1] ((x v y)^y) v ((x v y)^y)=y.
2807,2806 [back_demod,1994,demod,2801,2801,880,2801] x v x=x.
2811,2810 [back_demod,1186,demod,2807,2807,2807,2807,2807,2807] (x v y)^y=y.
2812 [back_demod,1185,demod,2811,2807,2811,2811,2811,2807] x^ (y v x)=x.
2822 [back_demod,2794,demod,2807,2807,2807,2807,2807,2807] ((x v (y^x))^z)^ (u v (v v x))= (x v (y^x))^z.
2837,2836 [back_demod,2780,demod,2807,2807] ((x v y) v y)^ (z v (x v y))=x v y.
2840 [back_demod,2776,demod,2807,2807] x^ (y v (z v (u v x)))=x.
2847,2846 [back_demod,2768,demod,2807,2807] (x^y)^ (z v (u v y))=x^y.
2862 [back_demod,2744,demod,2807,2807,2807,2807,2807] x^ (y v ((z v x)^ (x v u)))=x.
2892 [back_demod,2700,demod,2807,2807,2811,2807,2807,2807,2807] (x v (((y^x) v (z^x))^u))^ (v v (w v (v6 v x)))=x.
2896 [back_demod,2692,demod,2807,2837,2807] x^ (y v (z v x))=x.
2904 [back_demod,2680,demod,2807,2807] (x^y)^ (z v y)=x^y.
2906 [back_demod,2676,demod,2807,2807,2807,2807] x^ (y v (x^ (x v z)))=x.
2966 [back_demod,2602,demod,2807,2807] (x v (((y^x) v x)^z))^ (u v x)=x.
3346 [back_demod,1067,demod,2807,2807,2807,2807,2811,2807,2807,2807,2807,2807] (((x v (y^x))^z) v (u^ ((x v (y^x))^z)))^x= (x v (y^x))^z.
3433,3432 [back_demod,691,demod,2807] (x v (y^x))^ (z v (u v x))=x.
3563,3562 [para_into,2810.1.1.1,2806.1.1] x^x=x.
3571,3570 [para_into,2822.1.1.1,3562.1.1,demod,3433,3563,flip.1] x v (y^x)=x.
3572 [para_into,2822.1.1.1,2810.1.1,demod,2847,3571,flip.1] x^ (y^x)=y^x.
3652 [back_demod,3346,demod,3571,3571,3571,3571] (x^y)^x=x^y.
3789,3788 [para_from,3652.1.1,3570.1.1.2] x v (x^y)=x.
3854 [para_from,2904.1.1,3570.1.1.2] (x v y) v (z^y)=x v y.
3873,3872 [para_into,2906.1.1.2,3570.1.1] x^ (x v y)=x.
3875,3874 [para_from,3872.1.1,2904.1.1.1,demod,3873] x^ (y v (x v z))=x.
3880 [para_from,3872.1.1,3570.1.1.2] (x v y) v x=x v y.
3884 [back_demod,4,demod,3875] B v (A^ (B^C))!=B|B!=B| ((A^B) v (B^C)) v B!=B| ((A v B)^ (B v C))^B!=B.
3908,3907 [para_from,3880.1.1,3874.1.1.2] x^ ((x v y) v z)=x.
3926,3925 [para_from,3880.1.1,2896.1.1.2] x^ ((y v x) v z)=x.
3929 [para_from,3880.1.1,2840.1.1.2.2] x^ (y v ((z v x) v u))=x.
3945 [para_from,3880.1.1,2904.1.1.2] (x^y)^ (y v z)=x^y.
4066,4065 [para_into,3854.1.1.1,3788.1.1,demod,3789] x v (y^ (x^z))=x.
4087 [back_demod,3884,demod,4066] B!=B| ((A^B) v (B^C)) v B!=B| ((A v B)^ (B v C))^B!=B.
4283,4282 [para_into,2862.1.1.2,2806.1.1] x^ ((y v x)^ (x v z))=x.
4438 [para_into,3945.1.1.1,3907.1.1,demod,3908] x^ (((x v y) v z) v u)=x.
4558 [para_into,2892.1.1,3929.1.1] x v (((y^x) v (z^x))^u)=x.
5350 [para_into,4282.1.1.2.1,3880.1.1] x^ ((x v y)^ (x v z))=x.
5373,5372 [para_from,4282.1.1,3572.1.1.2,demod,4283] ((x v y)^ (y v z))^y=y.
5378 [back_demod,4087,demod,5373] B!=B| ((A^B) v (B^C)) v B!=B.
6445 [para_into,2966.1.1,4438.1.1] x v (((y^x) v x)^z)=x.
6507 [para_into,6445.1.1.2,5350.1.1] x v ((y^x) v x)=x.
6641 [para_from,6507.1.1,4282.1.1.2.1,demod,3926,2811,flip.1] (x^y) v y=y.
6709 [para_into,6641.1.1.1,2812.1.1] x v (y v x)=y v x.
7165 [para_from,6709.1.1,4282.1.1.2.2] x^ ((y v x)^ (z v x))=x.
13269 [para_into,4558.1.1.2,7165.1.1] x v ((y^x) v (z^x))=x.
13714,13713 [para_into,13269.1.1.2.2,3652.1.1] x v ((y^x) v (x^z))=x.
14262,14261 [para_from,13713.1.1,6709.1.1.2,demod,13714] ((x^y) v (y^z)) v y=y.
14337 [back_demod,5378,demod,14262] B!=B.
14338 [binary,14337.1,1.1] $F.

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