----- Otter 3.0.6, Feb 2000 ----- ----> UNIT CONFLICT at 249.12 sec ----> 74148 [binary,74146.1,8532.1] $Ans(Huntington_axioms). Length of proof is 154. Level of proof is 35. ---------------- PROOF ---------------- 1 [] x=x. 3,2 [] ((((x+x@ )@ + ((x+y)@ + (x@ +y)@ ))@ + (((((z+u)@ +v)@ + (v+z)@ )@ +w@ )@ + (((((z+u)@ +v)@ + (v+z)@ )@ +v)@ + (w@ +v)@ ))@ @ )@ + ((((x+x@ )@ + ((x+y)@ + (x@ +y)@ ))@ +v)@ + ((((((z+u)@ +v)@ + (v+z)@ )@ +w@ )@ + (((((z+u)@ +v)@ + (v+z)@ )@ +v)@ + (w@ +v)@ ))@ @ +v)@ ))@ =y. 4 [] A+B!=B+A| (A+B)+C!=A+ (B+C)| (A+B@ )@ + (A@ +B@ )@ !=B|$Ans(Huntington_axioms). 5 [copy,4,flip.1] B+A!=A+B| (A+B)+C!=A+ (B+C)| (A+B@ )@ + (A@ +B@ )@ !=B|$Ans(Huntington_axioms). 7,6 [para_into,2.1.1.1.1.1.1,2.1.1,demod,3] ((x+ (((((y+z)@ +u)@ + (u+y)@ )@ +v@ )@ + (((((y+z)@ +u)@ + (u+y)@ )@ +u)@ + (v@ +u)@ ))@ @ )@ + ((x+u)@ + ((((((y+z)@ +u)@ + (u+y)@ )@ +v@ )@ + (((((y+z)@ +u)@ + (u+y)@ )@ +u)@ + (v@ +u)@ ))@ @ +u)@ ))@ =x. 9,8 [back_demod,2,demod,7] ((x+x@ )@ + ((x+y)@ + (x@ +y)@ ))@ =y. 11,10 [para_into,8.1.1.1.1.1.2,8.1.1,demod,9] ((((x+x@ )@ + ((x+y)@ + (x@ +y)@ ))+y)@ + ((((x+x@ )@ + ((x+y)@ + (x@ +y)@ ))+z)@ + (y+z)@ ))@ =z. 12 [para_into,8.1.1.1.2.1,8.1.1] (((x+x@ )@ + (x+x@ )@ @ )@ + (y+ ((x+x@ )@ @ + ((x+y)@ + (x@ +y)@ ))@ ))@ = (x+y)@ + (x@ +y)@ . 29,28 [para_into,6.1.1.1.1.1.2.1.1.1.1.2,10.1.1,demod,11,11,11] ((x+ (((((y+z)@ +u)@ + (u+y)@ )@ +v)@ + (((((y+z)@ +u)@ + (u+y)@ )@ +u)@ + (v+u)@ ))@ @ )@ + ((x+u)@ + ((((((y+z)@ +u)@ + (u+y)@ )@ +v)@ + (((((y+z)@ +u)@ + (u+y)@ )@ +u)@ + (v+u)@ ))@ @ +u)@ ))@ =x. 31,30 [para_into,6.1.1.1.1.1.2.1,8.1.1,demod,9] ((x+y@ )@ + ((x+y)@ + (y@ +y)@ ))@ =x. 32 [para_into,6.1.1.1.1.1.2.1,6.1.1,demod,29] ((x+ (((y+z)@ +u)@ + (u+y)@ )@ @ )@ + ((x+u)@ + ((((y+z)@ +u)@ + (u+y)@ )@ @ +u)@ ))@ =x. 34 [para_into,6.1.1,10.1.1,flip.1] (x+x@ )@ + ((x+ (((((y+z)@ +u)@ + (u+y)@ )@ +v@ )@ + (((((y+z)@ +u)@ + (u+y)@ )@ +u)@ + (v@ +u)@ ))@ @ )@ + (x@ + (((((y+z)@ +u)@ + (u+y)@ )@ +v@ )@ + (((((y+z)@ +u)@ + (u+y)@ )@ +u)@ + (v@ +u)@ ))@ @ )@ )=u. 37,36 [para_into,6.1.1,8.1.1,flip.1] (((((x+y)@ +z)@ + (z+x)@ )@ +u@ )@ + (((((x+y)@ +z)@ + (z+x)@ )@ +z)@ + (u@ +z)@ ))@ =z. 39,38 [back_demod,34,demod,37,37] (x+x@ )@ + ((x+y@ )@ + (x@ +y@ )@ )=y. 62 [para_from,30.1.1,12.1.1.1.2.2.1.2.1,demod,31] ((((x+y@ )@ + (x+y@ )@ @ )@ + ((x+y@ )@ + (x+y@ )@ @ )@ @ )@ + (((x+y)@ + (y@ +y)@ )+ (((x+y@ )@ + (x+y@ )@ @ )@ @ + (x+ ((x+y@ )@ @ + ((x+y)@ + (y@ +y)@ ))@ ))@ ))@ =x+ ((x+y@ )@ @ + ((x+y)@ + (y@ +y)@ ))@ . 72 [para_into,38.1.1.1.1.2,8.1.1,demod,9] (((x+x@ )@ + ((x+y)@ + (x@ +y)@ ))+y)@ + ((((x+x@ )@ + ((x+y)@ + (x@ +y)@ ))+z@ )@ + (y+z@ )@ )=z. 74 [para_into,38.1.1.2.1.1.2,30.1.1,demod,31] (x+x@ )@ + ((x+y)@ + (x@ +y)@ )= (y+z@ )@ + ((y+z)@ + (z@ +z)@ ). 78 [para_into,38.1.1.2.1.1.2,8.1.1,demod,9] (x+x@ )@ + ((x+y)@ + (x@ +y)@ )= (z+z@ )@ + ((z+y)@ + (z@ +y)@ ). 90 [para_into,74.1.1,74.1.1] (x+y@ )@ + ((x+y)@ + (y@ +y)@ )= (x+z@ )@ + ((x+z)@ + (z@ +z)@ ). 92,91 [para_into,74.1.1,38.1.1,flip.1] (x@ +y@ )@ + ((x@ +y)@ + (y@ +y)@ )=x. 171 [para_into,32.1.1.1,78.1.1,demod,9,flip.1] (((x+y)@ +z)@ + (z+x)@ )@ =z. 179 [para_into,171.1.1.1.1.1.1.1,90.1.1,demod,31] ((x+y)@ + (y+ (x+z@ )@ )@ )@ =y. 181 [para_into,171.1.1.1.1.1.1.1,78.1.1,demod,9] ((x+y)@ + (y+ (z+z@ )@ )@ )@ =y. 264,263 [para_into,179.1.1.1.2.1.2.1.2,179.1.1] ((x+y)@ + (y+ (x+z)@ )@ )@ =y. 266,265 [para_into,179.1.1.1.2.1.2,179.1.1] (((x+y)@ +z)@ + (z+y)@ )@ =z. 268,267 [para_into,179.1.1.1.2,179.1.1] ((x+ (y+x)@ )@ +x)@ = (y+x)@ . 275 [para_into,263.1.1.1.1,263.1.1] (x+ ((x+ (y+z)@ )@ + ((y+x)@ +u)@ )@ )@ = (x+ (y+z)@ )@ . 277 [para_into,263.1.1.1.1,171.1.1] (x+ ((x+y)@ + (((y+z)@ +x)@ +u)@ )@ )@ = (x+y)@ . 283 [para_into,263.1.1.1.2.1.2.1,78.1.1,demod,9] (((x+x@ )@ +y)@ + (y+z)@ )@ =y. 291 [para_from,263.1.1,171.1.1.1.1] (x+ ((x+ (y+z)@ )@ +y)@ )@ = (x+ (y+z)@ )@ . 311,310 [para_from,263.1.1,171.1.1.1.1.1.1] ((x+y)@ + (y+ (z+x)@ )@ )@ =y. 354,353 [para_into,265.1.1.1.1,265.1.1] (x+ ((x+y)@ +x)@ )@ = (x+y)@ . 442,441 [para_from,267.1.1,171.1.1.1.1] ((x+y)@ + (y+y)@ )@ =y. 450,449 [para_from,267.1.1,38.1.1.2.2.1.2,demod,268,39,flip.1] (x+ (y+x)@ )@ +x=y+x. 485 [para_into,441.1.1.1.2,441.1.1] ((x+ (y+y)@ )@ +y)@ = (y+y)@ . 496,495 [para_from,441.1.1,171.1.1.1.1] (x+ ((x+x)@ +y)@ )@ = (x+x)@ . 659 [para_into,353.1.1.1.2.1.1.1,78.1.1,demod,9,9] ((x+x@ )@ + (y+ (x+x@ )@ )@ )@ =y. 663 [para_from,353.1.1,310.1.1.1.2] ((x+x)@ + (x+y)@ )@ =x. 683 [para_from,353.1.1,38.1.1.2.2.1.2,demod,354,39,flip.1] x+ ((x+y)@ +x)@ =x+y. 769,768 [para_into,683.1.1.2.1.1.1,38.1.1,demod,39] (x+x@ )@ + (y@ + (x+x@ )@ )@ =y. 792 [para_from,485.1.1,449.1.1.1.1.2,demod,450,flip.1] (x+ (y+y)@ )@ +y=y+y. 848 [para_from,495.1.1,38.1.1.2.2.1.2,demod,496,39,flip.1] x+ ((x+x)@ +y)@ =x+x. 1028 [para_into,283.1.1.1.2.1,78.1.1,demod,9] (((x+x@ )@ + (y+y@ )@ )@ +z)@ = (y+y@ )@ . 1111,1110 [para_into,659.1.1.1.2,663.1.1] ((x+x@ )@ +x)@ = (x+x)@ . 1112 [para_into,659.1.1.1.2,659.1.1,demod,1111] ((x+x@ )+ (x+x@ ))@ = (x+x@ )@ . 1115,1114 [para_into,659.1.1.1.2,310.1.1,demod,1111] ((x+y)+ (x+y))@ = (y+ (x+y))@ . 1116 [para_into,659.1.1.1.2,283.1.1,demod,1111] (x+x)@ = ((y+y@ )@ +x)@ . 1118,1117 [para_into,659.1.1.1.2,265.1.1,demod,1111,flip.1] ((x+y@ )@ +y)@ = (y+y)@ . 1119 [para_into,659.1.1.1.2,263.1.1,demod,1111,1115] (x+ (y+x))@ = (y+ (y+x))@ . 1120 [para_into,659.1.1.1.2,181.1.1,demod,1111,1115] (x@ + (x+x@ ))@ = (y+ (x+x@ ))@ . 1121 [para_into,659.1.1.1.2,171.1.1,demod,1111,flip.1] ((x@ +y)@ +x)@ = (x+x)@ . 1124,1123 [back_demod,1112,demod,1115] (x@ + (x+x@ ))@ = (x+x@ )@ . 1130,1129 [copy,1120,flip.1,demod,1124] (x+ (y+y@ ))@ = (y+y@ )@ . 1182 [para_into,1116.1.1,663.1.1,flip.1] ((x+x@ )@ + (y+y)@ )@ =y. 1184 [para_from,1116.1.1,659.1.1.1.2,demod,769] (x+x@ )@ = (y+y@ )@ . 1189 [para_from,1116.1.1,449.1.1.1.1.2,demod,450] (x+x@ )@ +y=y+y. 1346,1345 [para_from,1184.1.1,659.1.1.1.2] ((x+x@ )@ + (y+y@ )@ )@ =x+x@ . 1347 [para_from,1184.1.1,848.1.1.2] x+ (y+y@ )@ =x+x. 1359,1358 [para_from,1184.1.1,265.1.1.1.2,demod,1118] ((x+x)@ + (y+y@ )@ )@ =x. 1375,1374 [para_from,1184.1.1,38.1.1.2.1] (x+x@ )@ + ((y+y@ )@ + (x@ +x@ )@ )=x. 1381,1380 [para_from,1184.1.1,38.1.1.2.2.1.2] (x+x@ )@ + ((x+ (y+y@ )@ )@ + (x@ + (z+z@ )@ )@ )=y+y@ . 1396 [para_from,1184.1.1,38.1.1.2.1.1.2,demod,1381] x+x@ =y+y@ . 1470,1469 [para_from,1184.1.1,38.1.1.1] (x+x@ )@ + ((y+z@ )@ + (y@ +z@ )@ )=z. 1518,1517 [para_from,1184.1.1,8.1.1.1.1] ((x+x@ )@ + ((y+z)@ + (y@ +z)@ ))@ =z. 1547 [back_demod,1028,demod,1346] ((x+x@ )+y)@ = (z+z@ )@ . 1548 [copy,1347,flip.1] x+x=x+ (y+y@ )@ . 1563 [copy,1547,flip.1] (x+x@ )@ = ((y+y@ )+z)@ . 1619,1618 [para_from,1189.1.1,683.1.1.2.1] x+ (x+x)@ =x+x@ . 1620 [para_from,1189.1.1,310.1.1.1] ((x@ + (y+x)@ )@ + (x@ + (y+x)@ )@ )@ =x@ . 1625,1624 [para_from,1189.1.1,283.1.1.1] (((x+x@ )@ @ +y)@ + ((x+x@ )@ @ +y)@ )@ = (x+x@ )@ @ . 1755 [para_into,1347.1.1,1396.1.1] x+x@ = (y+y@ )+ (y+y@ ). 1769 [copy,1755,flip.1] (x+x@ )+ (x+x@ )=y+y@ . 1770 [para_from,1347.1.1,310.1.1.1] ((x+ (y+x))@ + (x+ (y+x))@ )@ =y+x. 1808,1807 [para_from,1548.1.1,792.1.1.1.1.2.1] (x+ (y+ (z+z@ )@ )@ )@ +y=y+y. 1836,1835 [para_into,1618.1.1.2.1,1347.1.1,demod,1346,flip.1] (x+x@ )@ + (x+x@ )@ @ = (x+x@ )@ + (x+x@ ). 1919 [back_demod,62,demod,1836,1130] (((x+y@ )@ + (x+y@ )@ @ )@ + (((x+y)@ + (y@ +y)@ )+ (((x+y@ )@ + (x+y@ )@ @ )@ @ + (x+ ((x+y@ )@ @ + ((x+y)@ + (y@ +y)@ ))@ ))@ ))@ =x+ ((x+y@ )@ @ + ((x+y)@ + (y@ +y)@ ))@ . 1971 [para_from,1117.1.1,848.1.1.2] x@ + (x+x)@ =x@ +x@ . 2008,2007 [para_from,1117.1.1,91.1.1.1.1.1,demod,1118,92,flip.1] (x+y@ )@ +y=y+y. 2043,2042 [para_into,2007.1.1.1,663.1.1,flip.1] (x+y)+ (x+y)=x+ (x+y). 2076 [back_demod,1769,demod,2043] x+ (x+x@ )=y+y@ . 2089 [para_into,2076.1.1.2,1396.1.1] x+ (y+y@ )=z+z@ . 2104 [copy,2089,flip.1] x+x@ =y+ (z+z@ ). 2265 [para_from,1119.1.1,449.1.1.1.1.2,demod,450] x+ (x+y)=y+ (x+y). 2319 [copy,2265,flip.1] x+ (y+x)=y+ (y+x). 2433,2432 [para_into,1121.1.1.1,1347.1.1,demod,1625,1346] (x+x@ )@ @ =x+x@ . 2453 [back_demod,1919,demod,2433] (((x+y@ )@ + (x+y@ )@ @ )@ + (((x+y)@ + (y@ +y)@ )+ (((x+y@ )@ + (x+y@ )@ @ )+ (x+ ((x+y@ )@ @ + ((x+y)@ + (y@ +y)@ ))@ ))@ ))@ =x+ ((x+y@ )@ @ + ((x+y)@ + (y@ +y)@ ))@ . 2627 [para_from,1121.1.1,449.1.1.1.1.2,demod,1619,2008,flip.1] (x@ +y)@ +x=x+x. 2700 [para_into,2627.1.1.1.1,2265.1.1] (x+ (y@ +x))@ +y=y+y. 3380 [para_from,1563.1.1,848.1.1.2] x+ ((y+y@ )+z)@ =x+x. 3381 [para_from,1563.1.1,792.1.1.1] ((x+x@ )+y)@ +z=z+z. 3431 [para_from,1563.1.1,2432.1.1.1] ((x+x@ )+y)@ @ =z+z@ . 3439 [copy,3380,flip.1] x+x=x+ ((y+y@ )+z)@ . 3446 [copy,3431,flip.1] x+x@ = ((y+y@ )+z)@ @ . 3855,3854 [para_into,2042.1.1,1548.1.1] (x+y)+ (z+z@ )@ =x+ (x+y). 4630 [para_from,2700.1.1,683.1.1.2.1,demod,1619,flip.1] x+ (x@ +x)=x+x@ . 4785,4784 [para_into,4630.1.1,2319.1.1] x@ + (x@ +x)=x+x@ . 4805,4804 [para_from,4630.1.1,441.1.1.1.1.1,demod,2043,4785,1346,flip.1] x@ +x=x+x@ . 5152 [back_demod,2453,demod,4805,4805,4805] (((x+y@ )@ + (x+y@ )@ @ )@ + (((x+y)@ + (y+y@ )@ )+ (((x+y@ )@ + (x+y@ )@ @ )+ (x+ ((x+y@ )@ @ + ((x+y)@ + (y+y@ )@ ))@ ))@ ))@ =x+ ((x+y@ )@ @ + ((x+y)@ + (y+y@ )@ ))@ . 6493,6492 [para_into,3439.1.1,2042.1.1,flip.1] (x+y)+ ((z+z@ )+u)@ =x+ (x+y). 6504 [back_demod,5152,demod,6493] (((x+y@ )@ + (x+y@ )@ @ )@ + ((x+y)@ + ((x+y)@ + (y+y@ )@ )))@ =x+ ((x+y@ )@ @ + ((x+y)@ + (y+y@ )@ ))@ . 6698 [para_from,3446.1.1,3380.1.1.2.1] x+ ((y+y@ )+z)@ @ @ =x+x. 6701 [para_from,3446.1.1,3381.1.1.1.1] ((x+x@ )+y)@ @ @ +z=z+z. 6754 [copy,6698,flip.1] x+x=x+ ((y+y@ )+z)@ @ @ . 6757 [copy,6701,flip.1] x+x= ((y+y@ )+z)@ @ @ +x. 7094 [para_into,72.1.1.2.1.1.2,1358.1.1,demod,1359] (((x+x@ )@ + ((x+y)@ + (x@ +y)@ ))+y)@ + ((((x+x@ )@ + ((x+y)@ + (x@ +y)@ ))+z)@ + (y+z)@ )= (z+z)@ + (u+u@ )@ . 7105 [para_into,72.1.1.2.1.1.2,441.1.1,demod,442] (((x+x@ )@ + ((x+y)@ + (x@ +y)@ ))+y)@ + ((((x+x@ )@ + ((x+y)@ + (x@ +y)@ ))+z)@ + (y+z)@ )= (u+z)@ + (z+z)@ . 7106 [para_into,72.1.1.2.1.1.2,310.1.1,demod,311] (((x+x@ )@ + ((x+y)@ + (x@ +y)@ ))+y)@ + ((((x+x@ )@ + ((x+y)@ + (x@ +y)@ ))+z)@ + (y+z)@ )= (u+z)@ + (z+ (v+u)@ )@ . 7108 [para_into,72.1.1.2.1.1.2,265.1.1,demod,266] (((x+x@ )@ + ((x+y)@ + (x@ +y)@ ))+y)@ + ((((x+x@ )@ + ((x+y)@ + (x@ +y)@ ))+z)@ + (y+z)@ )= ((u+v)@ +z)@ + (z+v)@ . 7109 [para_into,72.1.1.2.1.1.2,263.1.1,demod,264] (((x+x@ )@ + ((x+y)@ + (x@ +y)@ ))+y)@ + ((((x+x@ )@ + ((x+y)@ + (x@ +y)@ ))+z)@ + (y+z)@ )= (u+z)@ + (z+ (u+v)@ )@ . 7118 [para_into,72.1.1.2.1.1,2104.1.1,demod,1130,1518] (((x+x@ )@ + ((x+y)@ + (x@ +y)@ ))+y)@ + ((z+z@ )@ + (y+y)@ )= (x+x@ )@ + ((x+y)@ + (x@ +y)@ ). 7152,7151 [para_into,72.1.1.2.2.1,1971.1.1,demod,1470,1470,1619,1375,flip.1] x+x=x. 7162 [para_into,72.1.1.2.2.1,683.1.1] (((x+x@ )@ + ((x+y)@ + (x@ +y)@ ))+y)@ + ((((x+x@ )@ + ((x+y)@ + (x@ +y)@ ))+ ((y+z)@ +y)@ )@ + (y+z)@ )= (y+z)@ +y. 7169,7168 [para_into,72.1.1.2.2,1182.1.1,demod,1381,3855,1130,1381,7152,2008,7152,7152] (x+x@ )@ +y=y. 7177,7176 [para_into,72.1.1.2.2,441.1.1,demod,7169,7169,7152,2008,7152,7152] (((x+ (y+z)@ )@ + (x@ + (y+z)@ )@ )+ (y+z)@ )@ +z=z. 7185,7184 [para_into,72.1.1.2.2,181.1.1,demod,7169,7169,1808,7152,7177,flip.1] x+ (y+y@ )@ =x. 7189,7188 [para_into,72.1.1.2,3380.1.1,demod,1130,1130,7152,7185,7169,1130,1130,7152,7185,7169,1130,1130,7152,7185,7169,7152,7169] x@ @ =x. 7201,7200 [copy,7094,flip.1,demod,7152,7185,7169,7169,flip.1] (((x+y)@ + (x@ +y)@ )+y)@ + ((((x+y)@ + (x@ +y)@ )+z)@ + (y+z)@ )=z@ . 7205,7204 [copy,7105,flip.1,demod,7152,7169,7169,7201] (x+y)@ +y@ =y@ . 7206 [copy,7106,flip.1,demod,7169,7169,7201] (x+y)@ + (y+ (z+x)@ )@ =y@ . 7208 [copy,7108,flip.1,demod,7169,7169,7201] ((x+y)@ +z)@ + (z+y)@ =z@ . 7210 [copy,7109,flip.1,demod,7169,7169,7201] (x+y)@ + (y+ (x+z)@ )@ =y@ . 7227,7226 [back_demod,7118,demod,7169,7152,7169,7205,7169,flip.1] (x+y)@ + (x@ +y)@ =y@ . 7267,7266 [back_demod,6757,demod,7152,7189,flip.1] ((x+x@ )+y)@ +z=z. 7269,7268 [back_demod,6754,demod,7152,7189,flip.1] x+ ((y+y@ )+z)@ =x. 7427,7426 [back_demod,2627,demod,7152] (x@ +y)@ +x=x. 7444 [back_demod,2007,demod,7152] (x+y@ )@ +y=y. 7462 [back_demod,1770,demod,7152,7189] x+ (y+x)=y+x. 7467,7466 [back_demod,1620,demod,7152,7189] x@ + (y+x)@ =x@ . 7488 [back_demod,7162,demod,7227,7169,4805,7227,7169,7467,7189,7169,flip.1] (x+y)@ +x=x+ (x+y)@ . 7492 [back_demod,6504,demod,7189,4805,7185,7152,7169,7189,7189,7185,flip.1] x+ ((x+y@ )+ (x+y)@ )@ =x+y. 7570 [back_demod,5,demod,7227,7189,unit_del,1] B+A!=A+B| (A+B)+C!=A+ (B+C)|$Ans(Huntington_axioms). 7729,7728 [para_into,275.1.1.1.2.1.1.1,7266.1.1,demod,7189,7269,7267,7189,7267,7189] (x+y)+ (x@ +z)@ =x+y. 7799,7798 [para_into,7226.1.1.1.1,7226.1.1,demod,7189,7189,7729,7189] x+ (y+x)@ =y@ +x. 7858 [para_into,277.1.1.1.2.1.1.1,7266.1.1,demod,7269,7189,7267,7189,7267] x@ + ((x+y)+z)@ =x@ . 7995,7994 [para_into,7858.1.1.1,7188.1.1,demod,7189] x+ ((x@ +y)+z)@ =x. 8150 [para_into,7994.1.1.2.1,7462.1.1] x+ (y+ (x@ +z))@ =x. 8154 [para_from,7994.1.1,7462.1.1.2,demod,7995] ((x@ +y)+z)@ +x=x. 8199,8198 [para_into,8150.1.1.2.1.2,7444.1.1] (x+y@ )+ (z+y)@ =x+y@ . 8208 [back_demod,7492,demod,8199] x+ (x+y@ )@ =x+y. 8261,8260 [para_into,8154.1.1.1.1.1,7444.1.1] (x+y)@ + (z+x@ )=z+x@ . 8319,8318 [para_into,8208.1.1.2.1.2,7188.1.1] x+ (x+y)@ =x+y@ . 8327,8326 [back_demod,7488,demod,8319] (x+y)@ +x=x+y@ . 8358 [para_into,291.1.1.1.2.1.1.1,7798.1.1,demod,7427,7799] (x+y@ )@ = (y@ +x)@ . 8430 [para_into,8358.1.1.1.2,7188.1.1,demod,7189] (x+y)@ = (y+x)@ . 8479 [para_from,8430.1.1,7188.1.1.1,demod,7189] x+y=y+x. 8532 [back_unit_del,8479.1,7570.1] (A+B)+C!=A+ (B+C)|$Ans(Huntington_axioms). 18412 [para_from,7206.1.1,8326.1.1.1.1,demod,7189,7799,7189,flip.1] (x+y)@ + (y+ (z+x)@ )=x@ +y. 18612 [para_from,7208.1.1,7798.1.1.2.1,demod,7189,8327,7189,flip.1] ((x+y)@ +z)+ (z+y)@ =z+y@ . 18672 [para_into,7210.1.1.1.1,8479.1.1] (x+y)@ + (x+ (y+z)@ )@ =x@ . 18776 [para_into,7210.1.1,8479.1.1] (x+ (y+z)@ )@ + (y+x)@ =x@ . 56075 [para_from,18672.1.1,7798.1.1.2.1,demod,7189,8327,7189,7189,flip.1] (x+y)+ (x+ (y+z)@ )@ =x+ (y+z). 73106 [para_from,18612.1.1,18412.1.1.2,demod,8261] x+y@ =y@ + ((z+y)@ +x). 73437 [para_into,73106.1.1.2,7188.1.1,demod,7189] x+y=y+ ((z+y@ )@ +x). 73651 [para_into,73437.1.1,8479.1.1,flip.1] x+ ((y+x@ )@ +z)=x+z. 73674,73673 [para_into,73651.1.1.2.1.1,18776.1.1,demod,7189] (x+y)+ (y+z)= (x+y)+z. 73830,73829 [para_into,73651.1.1.2,18776.1.1,flip.1] (x+y)+ (x+z)@ = (x+y)+z@ . 74146 [back_demod,56075,demod,73830,7189,73674] (x+y)+z=x+ (y+z). 74148 [binary,74146.1,8532.1] $Ans(Huntington_axioms). ------------ end of proof -------------