----- Otter 3.2c, December 2001 ----- -----> EMPTY CLAUSE at 1.12 sec ----> 3838 [hyper,3,3472,1213,3700,1885] $F. Length of proof is 50. Level of proof is 31. ---------------- PROOF ---------------- 1 [] (((y v x)^x) v (((z^ (x v x)) v (u^x))^v))^ (w v ((v6 v x)^ (x v v7)))=x. 3 [] 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. 56 [para_into,1,1] (((x v y)^y) v (y v y))^ (z v ((u v y)^ (y v v)))=y. 57 [para_into,56,56] (((x v (y v y))^ (y v y)) v ((y v y) v (y v y)))^ (z v y)=y v y. 68 [para_from,57,1] (((x v y)^y) v (((y v y) v (z^y))^u))^ (v v ((w v y)^ (y v v6)))=y. 84 [para_from,68,56] (((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. 87 [para_from,84,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. 94 [para_into,87,87] (((x v y)^y) v (z^y))^ (u v ((v v y)^ (y v w)))=y. 104 [para_into,94,94] (((x v (y^z))^ (y^z)) v (u^ (y^z)))^ (v v z)=y^z. 126 [para_from,104,1] (((x v y)^y) v (((z^y) v (u^y))^v))^ (w v ((v6 v y)^ (y v v7)))=y. 161 [para_into,126,126] (((x v y)^y) v y)^ (z v ((u v y)^ (y v v)))=y. 187 [para_from,161,126] (((x v y)^y) v (((z^y) v (u^y))^v))^ (w v y)=y. 188 [para_from,161,94] (((x v y)^y) v (z^y))^ (u v y)=y. 191 [para_from,161,56] (((x v y)^y) v (y v y))^ (z v y)=y. 245 [para_from,191,94] (x v (y^ (x v x)))^ (z v ((u v (x v x))^ ((x v x) v v)))=x v x. 252 [para_into,245,191] (x v x)^ (y v ((z v (x v x))^ ((x v x) v u)))=x v x. 337 [para_from,252,187] (((x v y)^y) v ((z^y) v (z^y)))^ (u v y)=y. 419 [para_from,337,252] ((x^y) v (x^y))^ (z v y)= (x^y) v (x^y). 445 [para_into,419,188,flip.1] ((x v y)^y) v ((x v y)^y)=y. 570 [para_from,445,104] (x^y)^ (z v y)=x^y. 572 [para_from,445,188] x^ (y v x)=x. 573 [para_from,445,94] x^ (y v ((z v x)^ (x v u)))=x. 620 [para_from,572,187] (((x v y)^y) v ((z^y) v (u^y)))^ (v v y)=y. 839 [para_from,620,573] ((x^y) v (z^y))^ (u v y)= (x^y) v (z^y). 889 [para_into,839,188,flip.1] ((x v y)^y) v (z^y)=y. 1016 [para_from,889,573] x^ (x v y)=x. 1055 [para_into,1016,620,flip.1] ((x v y)^y) v ((z^y) v (u^y))=y. 1059 [para_into,1016,161,flip.1] ((x v y)^y) v y=y. 1066 [para_from,1016,570] x^ (y v (x v z))=x^ (x v z). 1143 [para_into,1059,1059] (x^x) v x=x. 1153 [para_from,1059,573] x^ (y v (x^ (x v z)))=x. 1154 [para_from,1059,573] x^ ((y v x)^ (x v z))=x. 1155 [para_from,1059,572] x^x=x. 1213 [para_into,1066,1016] x^ (y v (x v z))=x. 1366 [para_from,1155,1143] x v x=x. 1419 [para_into,1366,889,flip.1] (x v y)^y=y. 1454 [para_into,1419,889] x^ (y^x)=y^x. 1484 [para_from,1419,187] (x v (((y^x) v (z^x))^u))^ (v v x)=x. 1516 [para_into,1454,1154] ((x v y)^ (y v z))^y=y^ ((x v y)^ (y v z)). 1758 [para_into,1484,889] (x v (x^y))^ (z v x)=x. 1779 [para_into,1484,1016] x v (((y^x) v (z^x))^u)=x. 1885 [para_into,1516,1154] ((x v y)^ (y v z))^y=y. 1955 [para_into,1758,1055] (((x^y) v (z^y)) v (((x^y) v (z^y))^u))^y= (x^y) v (z^y). 1968 [para_from,1758,1154] (x^y)^x=x^y. 2144 [para_into,1779,1419] x v (((y^x) v x)^z)=x. 2161 [para_into,1779,1779] x v ((y^x)^z)=x. 3122 [para_from,2144,1153] ((x^y) v y)^y= (x^y) v y. 3194 [para_into,2161,1454] x v (y^ (z^x))=x. 3292 [para_into,3122,1419,flip.1] (x^y) v y=y. 3472 [para_into,3194,1968] x v (y^ (x^z))=x. 3540 [para_into,3292,1955] ((x^y) v (z^y)) v y=y. 3700 [para_into,3540,1968] ((x^y) v (y^z)) v y=y. 3838 [hyper,3,3472,1213,3700,1885] $F. ------------ end of proof -------------