----- Otter 3.0.6, Feb 2000 ----- ----> UNIT CONFLICT at 2.40 sec ----> 2828 [binary,2827.1,1.1] $F. Length of proof is 110. Level of proof is 28. ---------------- PROOF ---------------- 1 [] x=x. 2 [] x+y=y+x. 4,3 [] (x+y)+z=x+ (y+z). 5 [] (x+y@ )@ + (x@ +y@ )@ =y. 7 [] x*y= (x@ +y@ )@ . 9,8 [copy,7,flip.1] (x@ +y@ )@ =x*y. 10 [] x+x@ =1. 13,12 [] x*x@ =0. 14 [] (((X*X@ )+ ((X*Y)+ (X@ *Y)))* ((((((Z+ (U+V)@ )@ +0)*1)+ (Z+V)@ )@ *W@ )+ ((((((Z+ (U+V)@ )@ +0)*1)+ (Z+V)@ )@ *Z)+ (W@ *Z)))@ )+ ((((X*X@ )+ ((X*Y)+ (X@ *Y)))*Z)+ (((((((Z+ (U+V)@ )@ +0)*1)+ (Z+V)@ )@ *W@ )+ ((((((Z+ (U+V)@ )@ +0)*1)+ (Z+V)@ )@ *Z)+ (W@ *Z)))@ *Z))!=Y. 15 [copy,14,demod,13,13] ((0+ ((X*Y)+ (X@ *Y)))* ((((((Z+ (U+V)@ )@ +0)*1)+ (Z+V)@ )@ *W@ )+ ((((((Z+ (U+V)@ )@ +0)*1)+ (Z+V)@ )@ *Z)+ (W@ *Z)))@ )+ (((0+ ((X*Y)+ (X@ *Y)))*Z)+ (((((((Z+ (U+V)@ )@ +0)*1)+ (Z+V)@ )@ *W@ )+ ((((((Z+ (U+V)@ )@ +0)*1)+ (Z+V)@ )@ *Z)+ (W@ *Z)))@ *Z))!=Y. 16 [back_demod,5,demod,9] (x+y@ )@ + (x*y)=y. 18 [para_into,10.1.1,2.1.1] x@ +x=1. 21,20 [para_into,8.1.1.1.1,8.1.1] ((x*y)+z@ )@ = (x@ +y@ )*z. 22 [para_into,8.1.1.1.2,8.1.1] (x@ + (y*z))@ =x*y@ +z@ . 26,25 [para_into,8.1.1.1,10.1.1,demod,13] 1@ =0. 27 [para_into,8.1.1.1,2.1.1,demod,9] x*y=y*x. 28 [back_demod,15,demod,21,26,21,26,21,26,21,26] ((0+ ((X*Y)+ (X@ *Y)))* ((((((Z+ (U+V)@ )@ +0)@ +0)*Z+V)*W@ )+ ((((((Z+ (U+V)@ )@ +0)@ +0)*Z+V)*Z)+ (W@ *Z)))@ )+ (((0+ ((X*Y)+ (X@ *Y)))*Z)+ (((((((Z+ (U+V)@ )@ +0)@ +0)*Z+V)*W@ )+ ((((((Z+ (U+V)@ )@ +0)@ +0)*Z+V)*Z)+ (W@ *Z)))@ *Z))!=Y. 31 [para_from,8.1.1,18.1.1.1] (x*y)+ (x@ +y@ )=1. 35 [para_from,8.1.1,10.1.1.2,demod,4] x@ + (y@ + (x*y))=1. 39 [para_from,25.1.1,12.1.1.2] 1*0=0. 41 [para_from,25.1.1,10.1.1.2] 1+0=1. 43 [para_from,25.1.1,8.1.1.1.1] (0+x@ )@ =1*x. 46,45 [para_from,25.1.1,8.1.1.1.2] (x@ +0)@ =x*1. 47 [back_demod,28,demod,46,46,46,46] ((0+ ((X*Y)+ (X@ *Y)))* ((((((Z+ (U+V)@ )*1)+0)*Z+V)*W@ )+ ((((((Z+ (U+V)@ )*1)+0)*Z+V)*Z)+ (W@ *Z)))@ )+ (((0+ ((X*Y)+ (X@ *Y)))*Z)+ (((((((Z+ (U+V)@ )*1)+0)*Z+V)*W@ )+ ((((((Z+ (U+V)@ )*1)+0)*Z+V)*Z)+ (W@ *Z)))@ *Z))!=Y. 53,52 [para_into,3.1.1.1,10.1.1,flip.1] x+ (x@ +y)=1+y. 54 [para_into,3.1.1.1,2.1.1,demod,4] x+ (y+z)=y+ (x+z). 57 [para_into,3.1.1,2.1.1] x+ (y+z)=y+ (z+x). 58 [copy,57,flip.1] x+ (y+z)=z+ (x+y). 59 [para_from,41.1.1,3.1.1.1,flip.1] 1+ (0+x)=1+x. 68,67 [para_into,43.1.1.1.2,25.1.1] (0+0)@ =1*1. 69 [para_into,43.1.1.1.2,8.1.1] (0+ (x*y))@ =1*x@ +y@ . 88,87 [para_into,16.1.1.1.1,10.1.1,demod,26] 0+ (x*x)=x. 93 [para_into,16.1.1.1,43.1.1] (1*x)+ (0*x)=x. 96,95 [para_into,16.1.1.1,8.1.1] (x*y)+ (x@ *y)=y. 99 [para_into,16.1.1.2,39.1.1] (1+0@ )@ +0=0. 103 [para_into,16.1.1.2,27.1.1] (x+y@ )@ + (y*x)=y. 105 [para_into,16.1.1.2,12.1.1] (x+x@ @ )@ +0=x@ . 109 [back_demod,47,demod,96,96] ((0+Y)* ((((((Z+ (U+V)@ )*1)+0)*Z+V)*W@ )+ ((((((Z+ (U+V)@ )*1)+0)*Z+V)*Z)+ (W@ *Z)))@ )+ (((0+Y)*Z)+ (((((((Z+ (U+V)@ )*1)+0)*Z+V)*W@ )+ ((((((Z+ (U+V)@ )*1)+0)*Z+V)*Z)+ (W@ *Z)))@ *Z))!=Y. 116 [para_from,67.1.1,43.1.1.1.2,demod,88,26,flip.1] 1*0+0=0. 126 [para_from,116.1.1,16.1.1.2,demod,68] (1+ (1*1))@ +0=0+0. 174,173 [para_into,59.1.1.2,87.1.1,flip.1] 1+ (x*x)=1+x. 176,175 [para_into,59.1.1.2,10.1.1,flip.1] 1+0@ =1+1. 178,177 [back_demod,126,demod,174] (1+1)@ +0=0+0. 180,179 [back_demod,99,demod,176,178] 0+0=0. 189 [back_demod,67,demod,180] 0@ =1*1. 191 [para_from,179.1.1,3.1.1.1,flip.1] 0+ (0+x)=0+x. 196 [para_into,22.1.1.1,16.1.1,flip.1] (x+y@ )*x@ +y@ =y@ . 250 [para_into,93.1.1.1,27.1.1] (x*1)+ (0*x)=x. 254 [para_into,93.1.1,2.1.1] (0*x)+ (1*x)=x. 299,298 [para_into,191.1.1.2,87.1.1,demod,88] 0+x=x. 305,304 [para_into,191.1.1.2,2.1.1,demod,299,299] x+0=x. 328 [back_demod,109,demod,299,305,305,299,305,305] (Y* (((((Z+ (U+V)@ )*1)*Z+V)*W@ )+ (((((Z+ (U+V)@ )*1)*Z+V)*Z)+ (W@ *Z)))@ )+ ((Y*Z)+ ((((((Z+ (U+V)@ )*1)*Z+V)*W@ )+ (((((Z+ (U+V)@ )*1)*Z+V)*Z)+ (W@ *Z)))@ *Z))!=Y. 330,329 [back_demod,87,demod,299] x*x=x. 341 [back_demod,69,demod,299] (x*y)@ =1*x@ +y@ . 344,343 [back_demod,43,demod,299] x@ @ =1*x. 353 [back_demod,189,demod,330] 0@ =1. 369 [back_demod,105,demod,344,305] (x+ (1*x))@ =x@ . 377 [para_from,353.1.1,8.1.1.1.1] (1+x@ )@ =0*x. 407,406 [para_from,329.1.1,31.1.1.1,demod,53] 1+x@ =1. 409,408 [para_from,329.1.1,20.1.1.1.1] (x+y@ )@ = (x@ +x@ )*y. 416 [back_demod,8,demod,409,344,344] ((1*x)+ (1*x))*y=x*y. 421,420 [back_demod,377,demod,407,26,flip.1] 0*x=0. 426 [back_demod,103,demod,409] ((x@ +x@ )*y)+ (y*x)=y. 437,436 [back_demod,254,demod,421,299] 1*x=x. 439,438 [back_demod,250,demod,421,305] x*1=x. 443,442 [back_demod,416,demod,437,437] (x+x)*y=x*y. 450 [back_demod,369,demod,437] (x+x)@ =x@ . 453,452 [back_demod,343,demod,437] x@ @ =x. 455,454 [back_demod,341,demod,437] (x*y)@ =x@ +y@ . 460 [back_demod,328,demod,439,439,439,439] (Y* ((((Z+ (U+V)@ )*Z+V)*W@ )+ ((((Z+ (U+V)@ )*Z+V)*Z)+ (W@ *Z)))@ )+ ((Y*Z)+ (((((Z+ (U+V)@ )*Z+V)*W@ )+ ((((Z+ (U+V)@ )*Z+V)*Z)+ (W@ *Z)))@ *Z))!=Y. 463 [back_demod,426,demod,443] (x@ *y)+ (y*x)=y. 467 [back_demod,408,demod,443] (x+y@ )@ =x@ *y. 489 [para_from,452.1.1,35.1.1.2.1] x@ + (y+ (x*y@ ))=1. 494,493 [para_into,406.1.1.2,452.1.1] 1+x=1. 499 [back_demod,52,demod,494] x+ (x@ +y)=1. 504,503 [para_into,493.1.1,2.1.1] x+1=1. 508,507 [para_from,450.1.1,452.1.1.1,demod,453,flip.1] x+x=x. 522 [para_into,54.1.1.2,10.1.1,demod,504,flip.1] x+ (y+x@ )=1. 528 [para_into,507.1.1,54.1.1,demod,4,508] x+ (x+y)=x+y. 532 [para_from,507.1.1,54.1.1.2,flip.1] x+ (y+x)=y+x. 534 [para_into,499.1.1.2,54.1.1] x+ (y+ (x@ +z))=1. 572 [para_from,95.1.1,528.1.1.2,demod,96] (x*y)+y=y. 579,578 [para_into,572.1.1.1,27.1.1] (x*y)+x=x. 583,582 [para_into,572.1.1,2.1.1] x+ (y*x)=x. 591,590 [para_into,578.1.1,2.1.1] x+ (x*y)=x. 600 [para_from,582.1.1,3.1.1.1,flip.1] x+ ((y*x)+z)=x+z. 605,604 [para_from,590.1.1,54.1.1.2,flip.1] x+ (y+ (x*z))=y+x. 606 [para_from,590.1.1,3.1.1.1,flip.1] x+ ((x*y)+z)=x+z. 637 [para_into,463.1.1.1,27.1.1] (x*y@ )+ (x*y)=x. 651,650 [para_into,467.1.1.1.2,452.1.1] (x+y)@ =x@ *y@ . 652 [para_into,467.1.1.1,578.1.1,demod,453,455,453,flip.1] (x+y@ )*x=x. 680 [back_demod,460,demod,651,651,651,455,455,651,455,453,453,651,453,4,651,455,455,651,455,453,453,651,4,579,579,455,453,651,651,651,455,455,651,455,453,453,651,453,4,651,455,455,651,455,453,453,651,4,579,579,455,453] (Y* ((Z@ *U+V)+ ((Z@ *V@ )+W))*Z@ *W+Z@ )+ ((Y*Z)+ ((((Z@ *U+V)+ ((Z@ *V@ )+W))*Z@ *W+Z@ )*Z))!=Y. 688,687 [para_into,652.1.1.1.2,452.1.1] (x+y)*x=x. 701 [para_into,687.1.1.1,532.1.1] (x+y)*y=y. 709 [para_into,687.1.1,27.1.1] x*x+y=x. 736,735 [para_into,701.1.1,27.1.1] x*y+x=x. 737 [back_demod,680,demod,736,736] (Y* ((Z@ *U+V)+ ((Z@ *V@ )+W))*Z@ )+ ((Y*Z)+ ((((Z@ *U+V)+ ((Z@ *V@ )+W))*Z@ )*Z))!=Y. 756 [para_from,709.1.1,95.1.1.1] x+ (x@ *x+y)=x+y. 888,887 [para_into,534.1.1.2.2,58.1.1] x+ (y+ (z+ (x@ +u)))=1. 992 [para_into,650.1.1.1,522.1.1,demod,26,651,453,flip.1] x@ *y@ *x=0. 1059 [para_into,992.1.1.2.1,452.1.1] x@ *y*x=0. 1073 [para_into,1059.1.1.1,452.1.1] x*y*x@ =0. 1090,1089 [para_into,1073.1.1,27.1.1] (x*y@ )*y=0. 1091 [back_demod,737,demod,1090,305] (Y* ((Z@ *U+V)+ ((Z@ *V@ )+W))*Z@ )+ (Y*Z)!=Y. 1692 [para_into,196.1.1.1.2,452.1.1,demod,453,453] (x+y)*x@ +y=y. 1706 [para_into,1692.1.1.1,637.1.1,demod,455,453,4,583] x*x@ +y=x*y. 1710 [para_into,1692.1.1.1,489.1.1,demod,453,605,437,flip.1] x+ (y*x@ )=x+y. 1729,1728 [para_into,1692.1.1.1,35.1.1,demod,453,605,437,flip.1] x@ + (y*x)=x@ +y. 1737,1736 [para_into,1692.1.1.2.1,452.1.1] (x@ +y)*x+y=y. 1773,1772 [para_into,1706.1.1.2.1,452.1.1] x@ *x+y=x@ *y. 1794 [back_demod,756,demod,1773] x+ (x@ *y)=x+y. 1818,1817 [para_from,1710.1.1,3.1.1.1,demod,4,flip.1] x+ ((y*x@ )+z)=x+ (y+z). 2017,2016 [para_from,1794.1.1,3.1.1.1,demod,4,flip.1] x+ ((x@ *y)+z)=x+ (y+z). 2589,2588 [para_from,600.1.1,1736.1.1.1,demod,1818,flip.1] (x*y@ )+z= (y@ +z)*y+ (x+z). 2670,2669 [back_demod,1817,demod,2589] x+ ((x@ +y)*x+ (z+y))=x+ (z+y). 2703 [back_demod,1091,demod,2589] (Y* ((Z@ *U+V)+ ((V@ +W)*V+ (Z@ +W)))*Z@ )+ (Y*Z)!=Y. 2814,2813 [para_from,606.1.1,1736.1.1.1,demod,2017,flip.1] (x@ *y)+z= (x@ +z)*x+ (y+z). 2827 [back_demod,2703,demod,2814,4,2670,888,439,688,2589,1729,591,1737] Y!=Y. 2828 [binary,2827.1,1.1] $F. ------------ end of proof -------------