----- Otter 3.0.3+, Oct 1994 ----- The job was started by mccune on altair.mcs.anl.gov, Thu Jan 12 15:01:34 1995 ----> UNIT CONFLICT at 1038.08 sec ----> 7808 [binary,7807.1,1.1] $F. Length of proof is 106. Level of proof is 18. ---------------- PROOF ---------------- 1 [] x=x. 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^ (y v z)) v (x^y)=x^ (y v z). 14 [] (x v (y^z))^ (x v y)=x v (y^z). 16 [] (x^y) v (z^ (x v y))= (x v y)^ (z v (x^y)). 17 [] A^ (B v (A^C))!= (A^B) v (A^C). 18 [copy,17,flip.1] (A^B) v (A^C)!=A^ (B v (A^C)). 20 [para_into,5.1.1.1,4.1.1,demod,6] x^ (y^z)=y^ (x^z). 22,21 [para_into,5.1.1.1,2.1.1,flip.1] x^ (x^y)=x^y. 23 [para_into,5.1.1,4.1.1] x^ (y^z)=y^ (z^x). 26 [copy,23,flip.1] x^ (y^z)=z^ (x^y). 27 [para_into,10.1.1.1,9.1.1,demod,11] x v (y v z)=y v (x v z). 29,28 [para_into,10.1.1.1,7.1.1,flip.1] x v (x v y)=x v y. 30 [para_into,10.1.1,9.1.1] x v (y v z)=y v (z v x). 37,36 [para_into,21.1.1.2,4.1.1] x^ (y^x)=x^y. 40 [para_into,28.1.1.2,9.1.1] x v (y v x)=x v y. 43,42 [para_into,36.1.1.2,5.1.1] x^ (y^ (z^x))=x^ (y^z). 45,44 [para_from,36.1.1,5.1.1.1,demod,6,6,flip.1] x^ (y^ (x^z))=x^ (y^z). 49,48 [para_from,40.1.1,10.1.1.1,demod,11,11,flip.1] x v (y v (x v z))=x v (y v z). 52 [para_into,12.1.1.1.2,9.1.1] (x^ (y v z)) v (x^z)=x^ (z v y). 56 [para_into,12.1.1.1,4.1.1] ((x v y)^z) v (z^x)=z^ (x v y). 64 [para_into,12.1.1.2,4.1.1] (x^ (y v z)) v (y^x)=x^ (y v z). 68 [para_into,12.1.1,9.1.1] (x^y) v (x^ (y v z))=x^ (y v z). 70 [para_from,12.1.1,10.1.1.1,flip.1] (x^ (y v z)) v ((x^y) v u)= (x^ (y v z)) v u. 95 [para_into,27.1.1,9.1.1,demod,11] x v (y v z)=x v (z v y). 100 [para_into,14.1.1.1.2,23.1.1] (x v (y^ (z^u)))^ (x v u)=x v (u^ (y^z)). 102 [para_into,14.1.1.1.2,5.1.1,demod,6] (x v (y^ (z^u)))^ (x v (y^z))=x v (y^ (z^u)). 110 [para_into,14.1.1.1,7.1.1,demod,6,8] x^ (y^ ((x^y) v x))=x^y. 112 [para_into,14.1.1.2,40.1.1] (x v ((y v x)^z))^ (x v y)=x v ((y v x)^z). 118 [para_into,14.1.1.2,9.1.1] (x v (y^z))^ (y v x)=x v (y^z). 123,122 [para_into,14.1.1,4.1.1] (x v y)^ (x v (y^z))=x v (y^z). 139 [para_into,30.1.1.2,9.1.1] x v (y v z)=z v (y v x). 175 [para_into,16.1.1.1,36.1.1,demod,37] (x^y) v (z^ (x v (y^x)))= (x v (y^x))^ (z v (x^y)). 178 [para_into,16.1.1.1,2.1.1,demod,8,8,3] x v (y^x)=x^ (y v x). 189 [copy,175,flip.1] (x v (y^x))^ (z v (x^y))= (x^y) v (z^ (x v (y^x))). 192 [copy,178,flip.1] x^ (y v x)=x v (y^x). 230,229 [para_into,178.1.1.2,36.1.1,demod,6] (x^y) v (y^x)=x^ (y^ (y v (x^y))). 239 [para_into,178.1.1.2,4.1.1] x v (x^y)=x^ (y v x). 242,241 [para_into,178.1.1,9.1.1] (x^y) v y=y^ (x v y). 261,260 [para_from,178.1.1,28.1.1.2] x v (x^ (y v x))=x v (y^x). 266,265 [para_from,178.1.1,10.1.1.1] (x^ (y v x)) v z=x v ((y^x) v z). 275 [para_into,192.1.1.2,178.1.1,demod,6,22,37,230] x^ (y^ (x v y))=x^ (y^ (y v (x^y))). 278 [para_into,192.1.1.2,40.1.1,demod,11,261,flip.1] x v (y v (x^y))= (x v y)^ (y v x). 283 [para_into,192.1.1.2,12.1.1,demod,6,45,6,45,flip.1] (x^y) v (x^ ((y v z)^y))=x^ (y^ (y v z)). 287,286 [para_into,192.1.1.2,9.1.1,flip.1] x v (y^x)=x^ (x v y). 289 [para_into,192.1.1,4.1.1,demod,287] (x v y)^y=y^ (y v x). 303 [back_demod,278,demod,287] x v (y^ (y v x))= (x v y)^ (y v x). 305 [back_demod,275,demod,287,22] x^ (y^ (x v y))=x^ (y^ (y v x)). 311,310 [back_demod,260,demod,287] x v (x^ (y v x))=x^ (x v y). 314 [back_demod,229,demod,287,22] (x^y) v (y^x)=x^ (y^ (y v x)). 317 [back_demod,189,demod,287,6,287] x^ ((x v y)^ (z v (x^y)))= (x^y) v (z^ (x^ (x v y))). 318 [back_demod,178,demod,287] x^ (x v y)=x^ (y v x). 338,337 [para_into,239.1.1,9.1.1] (x^y) v x=x^ (y v x). 347,346 [back_demod,110,demod,338,45] x^ (y^ (y v x))=x^y. 352,351 [back_demod,314,demod,347] (x^y) v (y^x)=x^y. 354,353 [back_demod,305,demod,347] x^ (y^ (x v y))=x^y. 362,361 [para_from,239.1.1,28.1.1.2,demod,311,flip.1] x v (x^y)=x^ (x v y). 410,409 [para_into,286.1.1.2,23.1.1,demod,6] (x^y) v (x^ (y^z))=x^ (y^ ((x^y) v z)). 412,411 [para_into,286.1.1.2,20.1.1,demod,6] (x^y) v (x^ (z^y))=x^ (y^ ((x^y) v z)). 416,415 [back_demod,283,demod,412] x^ (y^ ((x^y) v (y v z)))=x^ (y^ (y v z)). 436,435 [para_into,289.1.1.1,286.1.1,demod,6,43,242,6,22,354] x^ ((x v y)^y)=y^x. 440,439 [para_into,289.1.1.1,40.1.1,demod,11,8,3] (x v y)^ (y v x)=y v x. 452 [back_demod,303,demod,440] x v (y^ (y v x))=y v x. 530 [para_from,318.1.1,241.1.1.1,demod,266,49,338,29,3] x v (y^ (x v y))=x v y. 586,585 [para_from,337.1.1,14.1.1.2] ((x^y) v (x^z))^ (x^ (y v x))= (x^y) v (x^z). 699 [para_from,351.1.1,139.1.1.2] x v (y^z)= (z^y) v ((y^z) v x). 700 [para_from,351.1.1,95.1.1.2,demod,352] x v (y^z)=x v (z^y). 705,704 [para_from,351.1.1,10.1.1.1,flip.1] (x^y) v ((y^x) v z)= (x^y) v z. 707 [back_demod,699,demod,705] x v (y^z)= (z^y) v x. 784 [para_from,435.1.1,14.1.1.1.2,demod,436] (x v (y^z))^ (x v z)=x v (y^z). 814,813 [para_from,439.1.1,42.1.1.2.2,demod,37,flip.1] (x v y)^ (z^ (y v x))= (x v y)^z. 818 [para_from,439.1.1,20.1.1.2,demod,814] x^ (y v z)= (z v y)^x. 903,902 [para_into,452.1.1.2,4.1.1] x v ((y v x)^y)=y v x. 932,931 [para_into,530.1.1.2,4.1.1] x v ((x v y)^y)=x v y. 1003,1002 [para_into,48.1.1.2.2,361.1.1] x v (y v (x^ (x v z)))=x v (y v (x^z)). 1112 [para_from,700.1.1,30.1.1.2] x v (y v (z^u))=y v ((u^z) v x). 1221 [para_from,707.1.1,30.1.1.2] x v ((y^z) v u)=u v ((z^y) v x). 1311 [para_from,818.1.1,707.1.1.2] x v ((y v z)^u)= ((z v y)^u) v x. 1379 [para_into,52.1.1.2,21.1.1] (x^ (y v (x^z))) v (x^z)=x^ ((x^z) v y). 1383 [para_into,52.1.1.2,4.1.1] (x^ (y v z)) v (z^x)=x^ (z v y). 1455,1454 [para_into,902.1.1.2,26.1.1] x v (y^ (((z^y) v x)^z))= (z^y) v x. 1726 [para_into,56.1.1,707.1.1] (x^y) v ((x v z)^y)=y^ (x v z). 1813,1812 [para_into,68.1.1.1,21.1.1] (x^y) v (x^ ((x^y) v z))=x^ ((x^y) v z). 2347,2346 [para_into,70.1.1.1.2,361.1.1,demod,362] (x^ (y^ (y v z))) v ((x^y) v u)= (x^ (y^ (y v z))) v u. 3311 [para_into,118.1.1.1,707.1.1] ((x^y) v z)^ (y v z)=z v (y^x). 3352 [copy,3311,flip.1] x v (y^z)= ((z^y) v x)^ (y v x). 3427,3426 [para_into,122.1.1.1,28.1.1] (x v y)^ (x v ((x v y)^z))=x v ((x v y)^z). 3497 [para_from,122.1.1,68.1.1.2,demod,123] ((x v y)^x) v (x v (y^z))=x v (y^z). 3499 [para_from,122.1.1,64.1.1.1,demod,11,1003,123] x v ((y^z) v (x^y))=x v (y^z). 4860 [para_into,100.1.1.1,902.1.1,demod,1455] ((x^y) v z)^ (z v y)= (x^y) v z. 5497 [para_into,102.1.1.1,931.1.1,demod,3427,932] x v ((x v (y^z))^y)=x v (y^z). 5499 [para_into,102.1.1.1,902.1.1,demod,903] ((x^y) v z)^ (z v (((x^y) v z)^x))= (x^y) v z. 6221,6220 [para_into,112.1.1,818.1.1] (x v y)^ (y v ((x v y)^z))=y v ((x v y)^z). 6224 [back_demod,5499,demod,6221] x v (((y^z) v x)^y)= (y^z) v x. 7101,7100 [para_into,265.1.1.1,818.1.1] ((x v y)^x) v z=x v ((y^x) v z). 7180 [back_demod,3497,demod,7101,49] x v ((y^x) v (y^z))=x v (y^z). 7272 [para_into,784.1.1,818.1.1] (x v y)^ (y v (z^x))=y v (z^x). 7374 [para_into,3352.1.1,707.1.1,flip.1] ((x^y) v z)^ (y v z)= (x^y) v z. 7393,7392 [para_into,3499.1.1,1221.1.1] (x^y) v ((z^y) v x)=x v (y^z). 7411,7410 [para_into,4860.1.1,818.1.1] (x v y)^ ((z^x) v y)= (z^x) v y. 7423,7422 [para_into,5497.1.1,1311.1.1] (((x^y) v z)^x) v z=z v (x^y). 7452,7451 [para_into,7180.1.1,1112.1.1] (x^y) v ((z^x) v y)=y v (x^z). 7458 [para_from,7272.1.1,1383.1.1.1,demod,6,11,410,416,7411] x v (y^ (z^ (z v x)))= (y^z) v x. 7544,7543 [para_from,7374.1.1,1726.1.1.2,demod,6,2347,7411] (x^ (y^ (y v z))) v z= (x^y) v z. 7558,7557 [para_into,7392.1.1.1,346.1.1,demod,7544,7393,6,flip.1] x v (y^ ((y v x)^z))=x v (y^z). 7586 [para_into,7458.1.1,6224.1.1,demod,6,6,7423,7558] (x^ ((x v y)^z)) v y=y v (x^z). 7689 [para_into,7586.1.1.1,317.1.1,demod,11,7544,7452,flip.1] x v (y^ (z v (y^x)))=x v (y^z). 7740 [para_into,7689.1.1.2.2,707.1.1] x v (y^ ((x^y) v z))=x v (y^z). 7759,7758 [para_into,7689.1.1,9.1.1] (x^ (y v (x^z))) v z=z v (x^y). 7797,7796 [para_from,7740.1.1,585.1.1.1,demod,586,6,37,1813] (x^y) v (x^z)=x^ ((x^y) v z). 7802,7801 [back_demod,1379,demod,7797,7759,flip.1] x^ ((x^y) v z)=x^ (y v (x^z)). 7807 [back_demod,18,demod,7797,7802] A^ (B v (A^C))!=A^ (B v (A^C)). 7808 [binary,7807.1,1.1] $F. ------------ end of proof -------------