----- Otter 3.0.6, Feb 2000 ----- ----> UNIT CONFLICT at 21.09 sec ----> 18699 [binary,18698.1,1.1] $F. Length of proof is 213. Level of proof is 40. ---------------- 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@ )+ ((X*Y)+ (X@ *Y)))* ((((Z+ (U+V)@ )@ + (Z+V)@ )@ *W@ )+ ((((Z+ (U+V)@ )@ + (Z+V)@ )@ *Z)+ (W@ *Z)))@ )+ ((((X*X@ )+ ((X*Y)+ (X@ *Y)))*Z)+ (((((Z+ (U+V)@ )@ + (Z+V)@ )@ *W@ )+ ((((Z+ (U+V)@ )@ + (Z+V)@ )@ *Z)+ (W@ *Z)))@ *Z))!=Y. 11 [copy,10,demod,9,9,9,9] (((X*X@ )+ ((X*Y)+ (X@ *Y)))* ((((Z+ (U+V)@ )*Z+V)*W@ )+ ((((Z+ (U+V)@ )*Z+V)*Z)+ (W@ *Z)))@ )+ ((((X*X@ )+ ((X*Y)+ (X@ *Y)))*Z)+ (((((Z+ (U+V)@ )*Z+V)*W@ )+ ((((Z+ (U+V)@ )*Z+V)*Z)+ (W@ *Z)))@ *Z))!=Y. 12 [back_demod,5,demod,9] (x+y@ )@ + (x*y)=y. 15,14 [para_into,8.1.1.1.1,8.1.1] ((x*y)+z@ )@ = (x@ +y@ )*z. 16 [para_into,8.1.1.1.2,8.1.1] (x@ + (y*z))@ =x*y@ +z@ . 18 [para_into,8.1.1.1,2.1.1,demod,9] x*y=y*x. 19 [para_into,3.1.1.1,2.1.1,demod,4] x+ (y+z)=y+ (x+z). 20 [para_into,3.1.1,2.1.1] x+ (y+z)=y+ (z+x). 21 [copy,20,flip.1] x+ (y+z)=z+ (x+y). 24 [para_into,12.1.1.1.1,3.1.1] (x+ (y+z@ ))@ + ((x+y)*z)=z. 26 [para_into,12.1.1.1.1,2.1.1] (x@ +y)@ + (y*x)=x. 29,28 [para_into,12.1.1.1,8.1.1] (x*y)+ (x@ *y)=y. 30 [para_into,12.1.1.2,18.1.1] (x+y@ )@ + (y*x)=y. 33,32 [para_into,12.1.1,2.1.1] (x*y)+ (x+y@ )@ =y. 34 [back_demod,11,demod,29,29] (((X*X@ )+Y)* ((((Z+ (U+V)@ )*Z+V)*W@ )+ ((((Z+ (U+V)@ )*Z+V)*Z)+ (W@ *Z)))@ )+ ((((X*X@ )+Y)*Z)+ (((((Z+ (U+V)@ )*Z+V)*W@ )+ ((((Z+ (U+V)@ )*Z+V)*Z)+ (W@ *Z)))@ *Z))!=Y. 35 [para_from,12.1.1,3.1.1.1,flip.1] (x+y@ )@ + ((x*y)+z)=y+z. 37 [para_into,28.1.1.1,18.1.1] (x*y)+ (y@ *x)=x. 41 [para_into,28.1.1.2,18.1.1] (x*y)+ (y*x@ )=y. 45 [para_from,28.1.1,3.1.1.1,flip.1] (x*y)+ ((x@ *y)+z)=y+z. 49 [para_into,37.1.1.2,18.1.1] (x*y)+ (x*y@ )=x. 52,51 [para_into,37.1.1,2.1.1] (x@ *y)+ (y*x)=y. 53 [para_from,37.1.1,3.1.1.1,flip.1] (x*y)+ ((y@ *x)+z)=x+z. 55 [para_into,14.1.1.1.1,18.1.1,demod,15] (x@ +y@ )*z= (y@ +x@ )*z. 68 [para_into,41.1.1.2.2,8.1.1] ((x@ +y@ )*z)+ (z*x*y)=z. 71,70 [para_into,41.1.1,2.1.1] (x*y@ )+ (y*x)=x. 72 [para_from,41.1.1,3.1.1.1,flip.1] (x*y)+ ((y*x@ )+z)=y+z. 84 [para_into,49.1.1,2.1.1] (x*y@ )+ (x*y)=x. 86 [para_from,49.1.1,3.1.1.1,flip.1] (x*y)+ ((x*y@ )+z)=x+z. 92 [para_from,51.1.1,3.1.1.1,flip.1] (x@ *y)+ ((y*x)+z)=y+z. 98 [para_from,70.1.1,3.1.1.1,flip.1] (x*y@ )+ ((y*x)+z)=x+z. 107 [para_into,16.1.1.1,12.1.1,flip.1] (x+y@ )*x@ +y@ =y@ . 140,139 [para_into,19.1.1.2,37.1.1,flip.1] (x*y)+ (z+ (y@ *x))=z+x. 167 [para_into,26.1.1.1.1,26.1.1] x@ + ((y*x)*x@ +y)=x@ +y. 175 [para_into,26.1.1.2,18.1.1] (x@ +y)@ + (x*y)=x. 177 [para_into,26.1.1,2.1.1] (x*y)+ (y@ +x)@ =y. 179 [para_from,26.1.1,16.1.1.1,flip.1] (x@ +y)*y@ +x@ =x@ . 196 [para_into,30.1.1,2.1.1] (x*y)+ (y+x@ )@ =x. 219 [para_from,32.1.1,14.1.1.1,flip.1] (x@ +y@ )*x+y@ =y@ . 309 [para_into,175.1.1,2.1.1] (x*y)+ (x@ +y)@ =x. 315 [para_from,175.1.1,16.1.1.1,flip.1] (x@ +y)*x@ +y@ =x@ . 348 [para_from,177.1.1,14.1.1.1,flip.1] (x@ +y@ )*y@ +x=y@ . 366 [para_from,196.1.1,14.1.1.1,flip.1] (x@ +y@ )*y+x@ =x@ . 388 [para_from,309.1.1,14.1.1.1,flip.1] (x@ +y@ )*x@ +y=x@ . 581 [para_into,219.1.1.2,177.1.1] ((x*y)@ + (y@ +x)@ )*y= (y@ +x)@ . 583 [para_into,219.1.1.2,32.1.1] ((x*y)@ + (x+y@ )@ )*y= (x+y@ )@ . 667 [para_into,34.1.1.1.2.1.1,18.1.1] (((X*X@ )+Y)* ((W@ * (Z+ (U+V)@ )*Z+V)+ ((((Z+ (U+V)@ )*Z+V)*Z)+ (W@ *Z)))@ )+ ((((X*X@ )+Y)*Z)+ (((((Z+ (U+V)@ )*Z+V)*W@ )+ ((((Z+ (U+V)@ )*Z+V)*Z)+ (W@ *Z)))@ *Z))!=Y. 782,781 [para_into,45.1.1.2,177.1.1,demod,9] (x*y)+y=y+ (y*x). 785,784 [para_into,45.1.1.2,84.1.1] (x*y@ )+x@ =y@ + (x@ *y). 819 [para_from,781.1.1,366.1.1.2] (x@ + (y*x@ )@ )*x@ + (x@ *y)=x@ . 920,919 [para_into,35.1.1.2,84.1.1] (x+y@ @ )@ +x=y@ + (x*y). 921 [para_into,35.1.1.2,70.1.1,demod,920] x@ + (y*x)=x@ + (x*y). 923,922 [para_into,35.1.1.2,49.1.1] (x+y@ )@ +x=y+ (x*y@ ). 928 [para_into,35.1.1.2,37.1.1,demod,923] x+ (y*x@ )=x+ (x@ *y). 1054 [para_into,921.1.1,2.1.1] (x*y)+y@ =y@ + (y*x). 1058 [copy,1054,flip.1] x@ + (x*y)= (y*x)+x@ . 1095 [para_into,928.1.1,2.1.1] (x*y@ )+y=y+ (y@ *x). 1273 [para_into,1058.1.1,2.1.1] (x*y)+x@ = (y*x)+x@ . 1274 [copy,1273,flip.1] (x*y)+y@ = (y*x)+y@ . 1440 [para_from,1274.1.1,45.1.1.2,demod,785,140] x@ +x=y+y@ . 1447 [copy,1440,flip.1] x+x@ =y@ +y. 1455 [para_into,1440.1.1,20.1.1] x+ (y+ (x+y)@ )=z+z@ . 1477 [para_from,1440.1.1,175.1.1.1.1] (x+x@ )@ + (y*y)=y. 1481 [para_from,1440.1.1,24.1.1.1.1.2] (x+ (y+y@ ))@ + ((x+z@ @ )*z)=z. 1490 [para_from,1440.1.1,388.1.1.1] (x+x@ )*y@ @ +y=y@ @ . 1495,1494 [para_from,1440.1.1,315.1.1.2] (x@ @ +x)*y+y@ =x@ @ . 1498 [para_from,1440.1.1,8.1.1.1] (x+x@ )@ =y@ *y. 1499 [para_from,1440.1.1,219.1.1.2,demod,1495] x@ @ @ =x@ . 1511 [para_from,1440.1.1,21.1.1.2] x+ (y+y@ )=z+ (x+z@ ). 1512 [para_from,1440.1.1,20.1.1.2] x+ (y+y@ )=z@ + (z+x). 1513 [para_from,1440.1.1,19.1.1.2] x+ (y+y@ )=z@ + (x+z). 1518 [copy,1498,flip.1] x@ *x= (y+y@ )@ . 1528 [copy,1511,flip.1] x+ (y+x@ )=y+ (z+z@ ). 1567,1566 [para_from,1499.1.1,8.1.1.1.2,demod,9,flip.1] x*y@ @ =x*y. 1571,1570 [para_from,1499.1.1,32.1.1.2.1.2,demod,1567,33,flip.1] x@ @ =x. 1590 [back_demod,1494,demod,1571,1571] (x+x)*y+y@ =x. 1592 [back_demod,1490,demod,1571,1571] (x+x@ )*y+y=y. 1608 [back_demod,1481,demod,1571] (x+ (y+y@ ))@ + ((x+z)*z)=z. 1623,1622 [para_into,53.1.1.2,309.1.1,demod,1571,flip.1] x+ (y+x)@ = (x*y)+y@ . 1625,1624 [para_into,53.1.1.2,196.1.1,demod,1571,flip.1] x+ (x+y)@ = (x*y)+y@ . 1628,1627 [para_into,53.1.1.2,84.1.1] (x@ *y)+y@ =x@ + (y@ *x). 1641 [back_demod,1455,demod,1623] x+ ((y*x)+x@ )=z+z@ . 1665,1664 [para_into,1570.1.1.1,8.1.1] (x*y)@ =x@ +y@ . 1708 [back_demod,819,demod,1665,1571] (x@ + (y@ +x))*x@ + (x@ *y)=x@ . 1725,1724 [back_demod,583,demod,1665,4,1623,1628,flip.1] (x+y@ )@ = (x@ + (y@ + (x@ *y)))*y. 1726 [back_demod,581,demod,1665,4,1625,1628,flip.1] (x@ +y)@ = (y@ + (x@ + (y@ *x)))*x. 1812 [back_demod,1518,demod,1725] x@ *x= (y@ + (y@ + (y@ *y)))*y. 1818 [back_demod,1477,demod,1725] ((x@ + (x@ + (x@ *x)))*x)+ (y*y)=y. 1909,1908 [back_demod,8,demod,1725,1571,1571] (x+ (y@ + (x*y)))*y=x*y. 1952 [copy,1812,flip.1,demod,1909] x@ *x=y@ *y. 1982 [back_demod,1818,demod,1909] (x@ *x)+ (y*y)=y. 2022,2021 [back_demod,1726,demod,1909] (x@ +y)@ =y@ *x. 2032 [para_from,1570.1.1,179.1.1.2.2,demod,1571,1571] (x+y)*y@ +x=x. 2034 [para_from,1570.1.1,388.1.1.2.1,demod,1571,1571] (x+y@ )*x+y=x. 2036 [para_from,1570.1.1,315.1.1.1.1,demod,1571,1571] (x+y)*x+y@ =x. 2040 [para_from,1570.1.1,348.1.1.2.1,demod,1571,1571] (x@ +y)*y+x=y. 2046 [para_from,1570.1.1,219.1.1.1.2,demod,1571,1571] (x@ +y)*x+y=y. 2049,2048 [para_from,1570.1.1,107.1.1.2.2,demod,1571,1571] (x+y)*x@ +y=y. 2065 [para_from,1447.1.1,21.1.1.2] x+ (y@ +y)=z@ + (x+z). 2066 [para_from,1447.1.1,20.1.1.2] x+ (y@ +y)=z+ (z@ +x). 2089 [para_into,1952.1.1.1,1570.1.1] x*x@ =y@ *y. 2090 [copy,2089,flip.1] x@ *x=y*y@ . 2091 [para_from,1952.1.1,1095.1.1.1,demod,1571] (x@ *x)+y=y+ (y@ *y). 2128 [para_into,55.1.1.1.1,1570.1.1,demod,1571] (x+y@ )*z= (y@ +x)*z. 2132 [para_into,55.1.1.1,1447.1.1,demod,1571] (x@ +x)*y= (z+z@ )*y. 2138 [para_into,2090.1.1.1,1570.1.1] x*x@ =y*y@ . 2139 [para_from,2090.1.1,1095.1.1.1,demod,1571] (x*x@ )+y=y+ (y@ *y). 2140 [para_from,2090.1.1,84.1.1.1,demod,1571,1571] (x*x@ )+ (y*y)=y. 2157 [copy,2139,flip.1] x+ (x@ *x)= (y*y@ )+x. 2173 [para_into,1590.1.1.1,19.1.1,demod,4] (x+ (x+ (y+y)))*z+z@ =x+y. 2211 [para_into,1592.1.1.1.2,1570.1.1] (x@ +x)*y+y=y. 2326,2325 [para_from,1982.1.1,53.1.1.2] (x*x)+y=x+ (y*y). 2350 [para_into,2021.1.1.1.1,1664.1.1,demod,4,2022,2022] (x@ *y)*z=x@ *z*y. 2352,2351 [para_into,2021.1.1.1.1,1570.1.1] (x+y)@ =y@ *x@ . 2367 [back_demod,667,demod,2352,2352,2352,2352,1665,1571,1665,1665,2352,1665,1571,1571,2352,4,782,1665,1571,1665,2352,1665,1571,1571,2352,2352,2352,2352,2352,1665,1571,1665,1665,2352,1665,1571,1571,2352,4,782,1665,1665,2352,1665,1571,1571,2352,1571,4] (((X*X@ )+Y)* ((W+Z@ )* ((V+U)*Z@ )+ (Z@ + (Z@ *V@ )))*W+ (((V+U)*Z@ )+ (V@ *Z@ )))+ ((((X*X@ )+Y)*Z)+ ((((W+Z@ )* ((V+U)*Z@ )+ (Z@ + (Z@ *V@ )))* ((V+U)*Z@ )+ ((V@ *Z@ )+W))*Z))!=Y. 2439 [back_demod,1608,demod,2352,2352,1571] ((x*x@ )*y@ )+ ((y+z)*z)=z. 2795 [para_into,2032.1.1.1,49.1.1,demod,1665,1571,4] x*x@ + (y+ (x*y))=x*y. 2807 [para_into,2032.1.1.1,28.1.1,demod,1665,1571,4] x*y+ (x@ + (y*x))=y*x. 2831 [para_from,2032.1.1,84.1.1.2,demod,2352,1571] ((x+y)*x@ *y)+x=x+y. 2871 [para_from,2034.1.1,45.1.1.1,demod,2352,1571,4] x+ (((y*x@ )*x+y)+z)=x+ (y+z). 2879 [para_from,2034.1.1,28.1.1.1,demod,2352,1571] x+ ((y*x@ )*x+y)=x+y. 3077 [para_into,2046.1.1.2,1982.1.1,demod,1665,1571,4] (x+ (x@ + (y*y)))*y=y*y. 3454,3453 [para_from,2325.1.1,3.1.1.1,demod,4,2326,2326] x+ (y+ (z*z))=x+ ((y+z)*y+z). 3472 [back_demod,3077,demod,3454] (x+ ((x@ +y)*x@ +y))*y=y*y. 3622 [para_into,68.1.1.1,2138.1.1,demod,2352,1571,1571,2352,1571,1571] (x*x@ )+ ((y*z)*z*y)=y*z. 3669 [para_into,1511.1.1,21.1.1] x@ + (y+x)=z+ (y+z@ ). 3680 [copy,3669,flip.1] x+ (y+x@ )=z@ + (y+z). 3760 [para_from,1512.1.1,2211.1.1.1,demod,2352,1571] (x@ + (x+ (y*y@ )))*z+z=z. 3873 [para_from,1513.1.1,2036.1.1.1,demod,2352,1571] (x@ + (y+x))*y+ (z*z@ )=y. 5580 [para_into,1641.1.1,1528.1.1] (x*y)+ (z+z@ )=u+u@ . 6445 [para_from,2065.1.1,2036.1.1.1,demod,2352,1571] (x@ + (y+x))*y+ (z@ *z)=y. 6549 [para_from,2066.1.1,2036.1.1.1,demod,2352,1571] (x+ (x@ +y))*y+ (z@ *z)=y. 7540 [para_from,2091.1.1,72.1.1.2,demod,1571,2326,1571] x+ ((y+ (y@ *y))*y+ (y@ *y))=x+y. 8072 [para_into,2128.1.1.1.2,1570.1.1,demod,1571] (x+y)*z= (y+x)*z. 8147 [para_into,8072.1.1,18.1.1] x*y+z= (z+y)*x. 8992 [para_into,2132.1.1.1,1512.1.1,demod,2352,1571] (x@ + (x+ (y*y@ )))*z= (u+u@ )*z. 9011 [copy,8992,flip.1] (x+x@ )*y= (z@ + (z+ (u*u@ )))*y. 9205 [para_into,2139.1.1.1.2,1664.1.1] ((x*y)*x@ +y@ )+z=z+ (z@ *z). 9613 [para_into,2157.1.1.2,1952.1.1] x+ (y@ *y)= (z*z@ )+x. 9622 [copy,9613,flip.1] (x*x@ )+y=y+ (z@ *z). 9818 [para_into,2350.1.1.1.1,1570.1.1,demod,1571] (x*y)*z=x*z*y. 9831 [copy,9818,flip.1] x*y*z= (x*z)*y. 9902 [para_from,9818.1.1,2140.1.1.2] (x*x@ )+ (y* (y*z)*z)=y*z. 9933,9932 [para_from,9818.1.1,1095.1.1.1] (x*y@ *z)+y=y+ (y@ *x*z). 10024 [back_demod,2831,demod,9933] x+ (x@ * (x+y)*y)=x+y. 10080,10079 [para_into,9831.1.1.2,18.1.1,flip.1] (x*y)*z=x*y*z. 10162 [back_demod,9902,demod,10080] (x*x@ )+ (y*y*z*z)=y*z. 10181 [back_demod,9831,demod,10080] x*y*z=x*z*y. 10429 [back_demod,9205,demod,10080] (x*y*x@ +y@ )+z=z+ (z@ *z). 11227 [back_demod,3622,demod,10080] (x*x@ )+ (y*z*z*y)=y*z. 11385 [back_demod,2879,demod,10080] x+ (y*x@ *x+y)=x+y. 11389 [back_demod,2871,demod,10080] x+ ((y*x@ *x+y)+z)=x+ (y+z). 11540 [back_demod,2439,demod,10080] (x*x@ *y@ )+ ((y+z)*z)=z. 11567 [back_demod,2367,demod,10080,10080,10080,10080] (((X*X@ )+Y)* (W+Z@ )* (((V+U)*Z@ )+ (Z@ + (Z@ *V@ )))*W+ (((V+U)*Z@ )+ (V@ *Z@ )))+ ((((X*X@ )+Y)*Z)+ ((W+Z@ )* (((V+U)*Z@ )+ (Z@ + (Z@ *V@ )))* (((V+U)*Z@ )+ ((V@ *Z@ )+W))*Z))!=Y. 11867 [back_demod,167,demod,10080] x@ + (y*x*x@ +y)=x@ +y. 13614 [para_from,3680.1.1,2040.1.1.1,demod,1571,4,1571] (x@ + (y+x))*y+ (z+z)=y+z. 13996 [para_into,5580.1.1.1,2211.1.1] x+ (y+y@ )=z+z@ . 14007 [para_into,5580.1.1,86.1.1,demod,1665,1571] x+ (x@ +y)=z+z@ . 14078 [para_from,13996.1.1,2036.1.1.1,demod,2352,1571] (x+x@ )*y+ (z*z@ )=y. 14080 [para_from,13996.1.1,2034.1.1.2,demod,2352,1571] (x+ (y*y@ ))*z+z@ =x. 14142 [para_from,14007.1.1,2032.1.1.2,demod,1571,4,1571] (x+ (y+x))*z+z@ =x+y. 14149 [para_from,14007.1.1,2040.1.1.2,demod,2352,1571,782] (x+ (x*y@ ))*z+z@ =x. 14162,14161 [para_from,14007.1.1,2048.1.1.2,demod,1571,1571] (x+ (x+y))*z+z@ =x+y. 14170 [para_from,14007.1.1,8147.1.1.2,demod,4] x*y+y@ = (z@ + (u+z))*x. 14201,14200 [back_demod,2173,demod,14162] x+ (y+y)=x+y. 14205 [copy,14170,flip.1] (x@ + (y+x))*z=z*u+u@ . 14215,14214 [back_demod,13614,demod,14201] (x@ + (y+x))*y+z=y+z. 14293,14292 [back_demod,6445,demod,14215] x+ (y@ *y)=x. 14295,14294 [back_demod,3873,demod,14215] x+ (y*y@ )=x. 14309,14308 [back_demod,6549,demod,14293] (x+ (x@ +y))*y=y. 14348 [back_demod,10429,demod,14293] (x*y*x@ +y@ )+z=z. 14367,14366 [back_demod,9622,demod,14293] (x*x@ )+y=y. 14405,14404 [back_demod,7540,demod,14293,14293] x+ (y*y)=x+y. 14416,14415 [back_demod,14080,demod,14295] x*y+y@ =x. 14418,14417 [back_demod,14078,demod,14295] (x+x@ )*y=y. 14439,14438 [back_demod,9011,demod,14418,14295,flip.1] (x@ +x)*y=y. 14442 [back_demod,3760,demod,14295,14439] x+x=x. 14455 [back_demod,11567,demod,14367,14367] (Y* (W+Z@ )* (((V+U)*Z@ )+ (Z@ + (Z@ *V@ )))*W+ (((V+U)*Z@ )+ (V@ *Z@ )))+ ((Y*Z)+ ((W+Z@ )* (((V+U)*Z@ )+ (Z@ + (Z@ *V@ )))* (((V+U)*Z@ )+ ((V@ *Z@ )+W))*Z))!=Y. 14490 [back_demod,11227,demod,14367] x*y*y*x=x*y. 14510 [back_demod,10162,demod,14367] x*x*y*y=x*y. 14571,14570 [back_demod,3472,demod,14405,14309,flip.1] x*x=x. 14583,14582 [back_demod,14205,demod,14416] (x@ + (y+x))*z=z. 14591,14590 [back_demod,14149,demod,14416] x+ (x*y@ )=x. 14593,14592 [back_demod,14142,demod,14416] x+ (y+x)=x+y. 14696,14695 [back_demod,14510,demod,14571] x*x*y=x*y. 14727,14726 [back_demod,1708,demod,14583] x@ + (x@ *y)=x@ . 14815 [back_demod,14455,demod,14591,782,14727,14591,782,14727] (Y* (W+Z@ )*Z@ *W+ (((V+U)*Z@ )+ (V@ *Z@ )))+ ((Y*Z)+ ((W+Z@ )*Z@ * (((V+U)*Z@ )+ ((V@ *Z@ )+W))*Z))!=Y. 14943,14942 [back_demod,14490,demod,14696] x*y*x=x*y. 15087,15086 [para_from,14442.1.1,98.1.1.2,demod,71,flip.1] x+ (y*x)=x. 15089,15088 [para_from,14442.1.1,92.1.1.2,demod,52,flip.1] x+ (x*y)=x. 15129,15128 [back_demod,2795,demod,15087] x*x@ +y=x*y. 15201,15200 [back_demod,11867,demod,15129,14943] x@ + (y*x)=x@ +y. 15241,15240 [back_demod,2807,demod,15201,14593] x*y+x@ =y*x. 15246 [back_demod,1908,demod,15201,14593] (x+y@ )*y=x*y. 15312,15311 [back_demod,14348,demod,15241] (x*x@ *y)+z=z. 15406,15405 [back_demod,11540,demod,15312] (x+y)*y=y. 15482,15481 [back_demod,10024,demod,15406] x+ (x@ *y)=x+y. 15739 [para_from,15086.1.1,2048.1.1.2] (x+ (y*x@ ))*x@ =y*x@ . 15751 [para_from,15086.1.1,3.1.1.1,flip.1] x+ ((y*x)+z)=x+z. 15764,15763 [para_from,15088.1.1,2046.1.1.1,demod,15482] x@ *x+y=x@ *y. 15787,15786 [back_demod,11389,demod,15764,14943] x+ ((y*x@ )+z)=x+ (y+z). 15789,15788 [back_demod,11385,demod,15764,14943] x+ (y*x@ )=x+y. 15812,15811 [back_demod,15739,demod,15789] (x+y)*x@ =y*x@ . 15896,15895 [para_into,15405.1.1.1,3.1.1] (x+ (y+z))*z=z. 15910,15909 [para_into,15405.1.1,18.1.1] x*y+x=x. 15954,15953 [para_from,15405.1.1,10079.1.1.1,flip.1] (x+y)*y*z=y*z. 15964 [back_demod,14815,demod,15954,15954] (Y*Z@ *W+ (((V+U)*Z@ )+ (V@ *Z@ )))+ ((Y*Z)+ (Z@ * (((V+U)*Z@ )+ ((V@ *Z@ )+W))*Z))!=Y. 16166 [para_into,14292.1.1.2,10181.1.1,demod,1665] x+ ((y@ +z@ )*z*y)=x. 17566,17565 [para_from,15246.1.1,10079.1.1.1,demod,10080,flip.1] (x+y@ )*y*z=x*y*z. 17568,17567 [back_demod,16166,demod,17566] x+ (y@ *z*y)=x. 17583 [back_demod,15964,demod,17568] (Y*Z@ *W+ (((V+U)*Z@ )+ (V@ *Z@ )))+ (Y*Z)!=Y. 17609,17608 [para_into,15481.1.1.2.1,2351.1.1,demod,10080,4,15482,4] x+ (y+ (x@ *z))=x+ (y+z). 18657,18656 [para_from,15751.1.1,2048.1.1.2,demod,15787,flip.1] (x*y@ )+z= (y+ (x+z))*y@ +z. 18698 [back_demod,17583,demod,18657,4,17609,15087,15812,15896,15910,18657,15089,15201,2049] Y!=Y. 18699 [binary,18698.1,1.1] $F. ------------ end of proof -------------