----- Otter 3.1-b0, May 2000 ----- ----> UNIT CONFLICT at 32.32 sec ----> 14262 [binary,14261.1,1.1] $Ans(Robbins_basis). Length of proof is 137. Level of proof is 51. ---------------- PROOF ---------------- 1 [] x=x. 2 [] B+A!=A+B| (A+B)+C!=A+ (B+C)| ~(~(A+B)+ ~(~A+B))!=B|$Ans(Robbins_basis). 3 [] ~(~(x+y)+ ~(~(~y+ ~(z+y))+ ~(x+u)))=y. 6,5 [para_into,3.1.1.1.2.1.2,3.1.1] ~(~(~(x+y)+z)+ ~(~(~z+ ~(u+z))+y))=z. 7 [para_into,3.1.1.1.2,3.1.1] ~(~(~(~ ~(x+y)+ ~(z+ ~(x+y)))+y)+ ~(x+y))=y. 9 [para_into,5.1.1.1.1.1.1,5.1.1] ~(~(x+y)+ ~(~(~y+ ~(z+y))+ ~(~(~x+ ~(u+x))+v)))=y. 15 [para_from,7.1.1,5.1.1.1.2.1.1.1.2] ~(~(~(x+y)+ ~(z+u))+ ~(~(~ ~(z+u)+u)+y))= ~(z+u). 21 [para_from,7.1.1,5.1.1.1.1.1.1] ~(~(x+y)+ ~(~(~y+ ~(z+y))+ ~(u+x)))=y. 24,23 [para_into,9.1.1.1.2,9.1.1] ~(~(~(x+y)+y)+ ~(x+y))=y. 25 [para_into,23.1.1.1.1.1.1,23.1.1,demod,24] ~(~(x+ ~(y+x))+x)= ~(y+x). 30,29 [para_into,25.1.1.1.1,3.1.1,flip.1] ~(~(~x+ ~(y+x))+ ~(z+x))= ~(x+ ~(z+x)). 32,31 [para_from,25.1.1,5.1.1.1.1,demod,30] ~(~(x+y)+ ~(y+ ~(x+y)))=y. 36,35 [para_into,31.1.1.1.1,23.1.1,demod,24] ~(x+ ~(~(y+x)+x))= ~(y+x). 37 [para_into,31.1.1.1.1,5.1.1,demod,6] ~(x+ ~(~(~(~x+ ~(y+x))+z)+x))= ~(~(~x+ ~(y+x))+z). 49 [para_into,15.1.1.1.1.1.2,31.1.1,demod,32,32] ~(~(~(x+y)+z)+ ~(~(~z+ ~(z+ ~(u+z)))+y))=z. 56,55 [para_into,15.1.1.1.1,23.1.1,demod,36] ~(~ ~(x+y)+y)= ~(x+y). 68,67 [para_into,55.1.1.1.1.1,31.1.1,demod,32] ~(~x+ ~(x+ ~(y+x)))=x. 70,69 [para_into,55.1.1.1.1.1,23.1.1,demod,24] ~(~x+ ~(y+x))=x. 71 [para_into,55.1.1.1.1.1,9.1.1,demod,70,70,70,70,flip.1] ~(~(x+y)+ ~(y+ ~(x+z)))= ~(~y+ ~(y+ ~(x+z))). 74,73 [para_into,55.1.1.1.1.1,5.1.1,demod,70,70,flip.1] ~(~(~(x+y)+z)+ ~(z+y))= ~(~z+ ~(z+y)). 76,75 [back_demod,49,demod,68,74] ~(~x+ ~(x+y))=x. 80,79 [back_demod,37,demod,70,70] ~(x+ ~(~(x+y)+x))= ~(x+y). 85 [back_demod,21,demod,70] ~(~(x+y)+ ~(y+ ~(z+x)))=y. 87 [back_demod,73,demod,76] ~(~(~(x+y)+z)+ ~(z+y))=z. 89 [back_demod,71,demod,76] ~(~(x+y)+ ~(y+ ~(x+z)))=y. 106,105 [para_into,75.1.1.1.2,75.1.1] ~(~ ~x+x)= ~x. 108,107 [para_from,75.1.1,69.1.1.1.2] ~(~ ~(x+y)+x)= ~(x+y). 132,131 [para_from,105.1.1,35.1.1.1.2.1.1,demod,106] ~(x+ ~(~x+x))= ~x. 134,133 [para_from,105.1.1,25.1.1.1.1.1.2,demod,106] ~(~(x+ ~x)+x)= ~x. 136,135 [para_from,105.1.1,69.1.1.1.2] ~(~x+ ~x)=x. 144,143 [para_into,135.1.1.1.1,135.1.1,demod,136] ~(x+x)= ~x+ ~x. 146,145 [para_into,135.1.1.1.1,105.1.1,demod,106,144] ~ ~x+ ~ ~x= ~ ~x+x. 148,147 [para_into,135.1.1.1.1,75.1.1,demod,76,144,flip.1] ~x+ ~(x+y)= ~x+ ~x. 150,149 [para_into,135.1.1.1.1,69.1.1,demod,70,144,flip.1] ~x+ ~(y+x)= ~x+ ~x. 152,151 [para_into,135.1.1.1.1,55.1.1,demod,56,144,146] ~ ~(x+y)+ (x+y)= ~ ~(x+y)+y. 153 [para_into,135.1.1.1.1,35.1.1,demod,36,144,146,152,flip.1] x+ ~(~(y+x)+x)= ~ ~(y+x)+x. 162,161 [back_demod,135,demod,144,146] ~ ~x+x=x. 170,169 [back_demod,151,demod,162,flip.1] ~ ~(x+y)+y=x+y. 172,171 [back_demod,145,demod,162] ~ ~x+ ~ ~x=x. 175 [back_demod,153,demod,170] x+ ~(~(y+x)+x)=y+x. 200,199 [para_from,131.1.1,171.1.1.2.1,demod,132,172,flip.1] x+ ~(~x+x)=x. 209 [para_from,133.1.1,171.1.1.2.1,demod,134,172,flip.1] ~(x+ ~x)+x=x. 212,211 [para_from,79.1.1,171.1.1.2.1,demod,80,172,flip.1] x+ ~(~(x+y)+x)=x+y. 249 [para_from,107.1.1,171.1.1.2.1,demod,108,172,flip.1] ~ ~(x+y)+x=x+y. 263 [para_into,175.1.1.2.1.1.1,199.1.1,demod,150,144,172,200] ~(~x+x)+x=x. 270,269 [para_into,175.1.1.2.1.1.1,147.1.1,demod,144,172,148] ~(x+y)+ ~(x+ ~(x+y))= ~x+ ~x. 285 [para_into,85.1.1.1.1.1,149.1.1,demod,144,172] ~(x+ ~(~(y+x)+ ~(z+ ~x)))= ~(y+x). 293 [para_into,85.1.1.1.2.1.2.1,209.1.1] ~(~(x+y)+ ~(y+ ~x))=y. 303 [para_into,85.1.1.1.2.1.2.1,147.1.1,demod,144,172] ~(~(~(x+y)+z)+ ~(z+x))=z. 310,309 [para_into,85.1.1.1.2.1,199.1.1,demod,144] ~((~x+ ~x)+ ~x)=x. 315 [para_into,85.1.1.1.2.1,147.1.1,demod,144,172] ~(~(x+ ~y)+y)= ~y. 320,319 [para_from,85.1.1,175.1.1.2.1.1,demod,270,flip.1] ~(x+y)+ ~(y+ ~(z+x))= ~y+ ~y. 321 [para_from,85.1.1,149.1.1.1,demod,320,320,144,172,320,144,172] x+ ~(y+ (~x+ ~x))=x+x. 323 [para_from,85.1.1,147.1.1.1,demod,320,320,144,172,320,144,172] x+ ~((~x+ ~x)+y)=x+x. 328,327 [para_from,263.1.1,175.1.1.2.1,flip.1] ~x+x=x+ ~x. 349 [para_into,87.1.1.1.1.1.1.1,209.1.1] ~(~(~x+y)+ ~(y+x))=y. 371 [para_from,87.1.1,175.1.1.2.1.1,demod,270,flip.1] ~(~(x+y)+z)+ ~(z+y)= ~z+ ~z. 380,379 [para_into,309.1.1.1.1.1,309.1.1,demod,310,310] ~((x+x)+x)= (~x+ ~x)+ ~x. 381 [para_into,309.1.1.1.1.1,143.1.1,demod,144,144,380,144,172,144,172,144,172] (x+x)+x=x+x. 385 [para_into,381.1.1.1,171.1.1,demod,172] x+ ~ ~x=x. 413 [para_from,89.1.1,175.1.1.2.1.1,demod,270,flip.1] ~(x+y)+ ~(y+ ~(x+z))= ~y+ ~y. 420,419 [para_into,315.1.1.1.1.1,385.1.1,demod,144,172,flip.1] ~ ~x=x. 438,437 [back_demod,385,demod,420] x+x=x. 443 [back_demod,249,demod,420] (x+y)+x=x+y. 446,445 [back_demod,169,demod,420] (x+y)+y=x+y. 447 [back_demod,413,demod,438] ~(x+y)+ ~(y+ ~(x+z))= ~y. 449 [back_demod,371,demod,438] ~(~(x+y)+z)+ ~(z+y)= ~z. 456,455 [back_demod,323,demod,438,438] x+ ~(~x+y)=x. 458,457 [back_demod,321,demod,438,438] x+ ~(y+ ~x)=x. 459 [back_demod,319,demod,438] ~(x+y)+ ~(y+ ~(z+x))= ~y. 462,461 [back_demod,269,demod,438] ~(x+y)+ ~(x+ ~(x+y))= ~x. 470,469 [back_demod,149,demod,438] ~x+ ~(y+x)= ~x. 471 [back_demod,147,demod,438] ~x+ ~(x+y)= ~x. 473 [para_from,315.1.1,175.1.1.2.1.1,demod,328,458,flip.1] ~(x+ ~y)+y=y. 493 [para_into,473.1.1.1.1,443.1.1] ~(~x+y)+x=x. 495 [para_into,493.1.1.1.1.1,419.1.1] ~(x+y)+ ~x= ~x. 498,497 [para_from,469.1.1,473.1.1.1.1,demod,420] x+ (y+x)=y+x. 527 [para_from,293.1.1,175.1.1.2.1.1,demod,462,flip.1] ~(x+y)+ ~(y+ ~x)= ~y. 536,535 [para_from,349.1.1,175.1.1.2.1.1,demod,462,flip.1] ~(~x+y)+ ~(y+x)= ~y. 549 [para_into,285.1.1.1.2.1,495.1.1,demod,420,flip.1] ~((x+ ~y)+y)= ~(y+ (x+ ~y)). 551 [para_from,285.1.1,527.1.1.2] ~((~(x+y)+ ~(z+ ~y))+y)+ ~(x+y)= ~y. 555 [para_into,535.1.1.1.1,535.1.1,demod,420,420] x+ ~(~(x+y)+ (~y+x))=x+y. 589 [para_from,303.1.1,535.1.1.1,demod,420] x+ ~(~(x+y)+ (~(y+z)+x))=x+y. 591 [para_from,303.1.1,527.1.1.2,demod,420] ~((x+y)+ ~(~(y+z)+x))+x= ~(y+z)+x. 593 [para_from,303.1.1,175.1.1.2.1.1,demod,462,flip.1] ~(~(x+y)+z)+ ~(z+x)= ~z. 601 [para_into,447.1.1.1.1,469.1.1,demod,420,420] x+ ~(~(y+x)+ ~(~x+z))=y+x. 695 [para_into,459.1.1.2.1,459.1.1,demod,420,420] ~(~(x+y)+ ~(y+z))+z=y+z. 697 [para_into,459.1.1.2.1,449.1.1,demod,420,420] ~(x+ ~(~(y+x)+z))+z= ~(y+x)+z. 738,737 [para_from,549.1.1,175.1.1.2.1.1,demod,212,flip.1] (x+ ~y)+y=y+ (x+ ~y). 745 [para_into,737.1.1.1.2,419.1.1,demod,420] (x+y)+ ~y= ~y+ (x+y). 748 [para_into,737.1.1.1,535.1.1,demod,536] ~x+ (x+y)= (x+y)+ ~x. 749 [para_into,737.1.1.1,469.1.1,demod,470] ~x+ (y+x)= (y+x)+ ~x. 754 [copy,748,flip.1] (x+y)+ ~x= ~x+ (x+y). 793 [para_from,748.1.1,745.1.1.1,flip.1] ~(x+y)+ (~x+ (x+y))= ((x+y)+ ~x)+ ~(x+y). 809 [para_from,749.1.1,449.1.1.2.1,demod,420] ~(~(x+ (y+z))+ ~z)+ ~((y+z)+ ~z)=z. 847 [para_from,754.1.1,447.1.1.1.1,demod,420] ~(~x+ (x+y))+ ~(~x+ ~((x+y)+z))=x. 864,863 [para_into,593.1.1.1.1,449.1.1,demod,420,420] x+ ~(~(x+y)+ ~(z+y))=x+y. 896,895 [para_into,593.1.1.2.1,473.1.1,demod,420] ~(~(x+y)+ ~(z+ ~x))+ ~x=z+ ~x. 1061 [para_into,555.1.1.2.1.2,535.1.1] ~(x+y)+ ~(~(~(x+y)+ (~y+x))+ ~x)= ~(x+y)+ (~y+x). 1129 [para_from,695.1.1,459.1.1.1.1] ~(x+y)+ ~(y+ ~(z+ ~(~(u+x)+ ~(x+y))))= ~y. 1418,1417 [para_from,551.1.1,601.1.1.2.1,demod,420,438,328,flip.1] (~(x+ ~x)+ ~(y+ ~x))+x=x. 1449 [para_from,1417.1.1,754.1.1.1,demod,864,1418,flip.1] ~(~(x+ ~x)+ ~(y+ ~x))+x=x+ ~x. 1458,1457 [para_from,1417.1.1,471.1.1.2.1,demod,896,flip.1] ~(~(x+ ~x)+ ~(y+ ~x))=y+ ~x. 1468,1467 [back_demod,1449,demod,1458,738] x+ (y+ ~x)=x+ ~x. 1494,1493 [back_demod,737,demod,1468] (x+ ~y)+y=y+ ~y. 1496,1495 [para_into,1467.1.1.2.2,419.1.1,demod,420,328] ~x+ (y+x)=x+ ~x. 1500,1499 [para_into,1467.1.1.2,593.1.1,flip.1] (x+y)+ ~(x+y)= (x+y)+ ~x. 1501 [para_into,1467.1.1.2,551.1.1,demod,1500] (x+y)+ ~y= (x+y)+ ~x. 1505,1504 [para_into,1467.1.1.2,457.1.1,demod,1494,1500,flip.1] (x+ ~y)+ ~x=y+ ~y. 1583,1582 [back_demod,793,demod,1496,1500,1505] (x+y)+ ~x=x+ ~x. 1595,1594 [back_demod,749,demod,1496,flip.1] (x+y)+ ~y=y+ ~y. 1606 [copy,1501,flip.1,demod,1583,1595] x+ ~x=y+ ~y. 1708,1707 [back_demod,754,demod,1583,flip.1] ~x+ (x+y)=x+ ~x. 1737 [back_demod,809,demod,1595] ~(~(x+ (y+z))+ ~z)+ ~(z+ ~z)=z. 1761 [back_demod,847,demod,1708] ~(x+ ~x)+ ~(~x+ ~((x+y)+z))=x. 1781 [para_from,1467.1.1,593.1.1.2.1] ~(~((x+ ~y)+z)+y)+ ~(y+ ~y)= ~y. 1790,1789 [para_from,1467.1.1,469.1.1.2.1] ~(x+ ~y)+ ~(y+ ~y)= ~(x+ ~y). 1824,1823 [back_demod,1737,demod,1790] ~(~(x+ (y+z))+ ~z)=z. 1833 [back_demod,1061,demod,1824,flip.1] ~(x+y)+ (~y+x)= ~(x+y)+x. 1850,1849 [para_from,1606.1.1,493.1.1.1.1] ~(x+ ~x)+y=y. 1852,1851 [para_from,1606.1.1,455.1.1.2.1] x+ ~(y+ ~y)=x. 1873,1872 [back_demod,1761,demod,1850] ~(~x+ ~((x+y)+z))=x. 1923,1922 [back_demod,1781,demod,1852] ~(~((x+ ~y)+z)+y)= ~y. 2077 [para_from,589.1.1,527.1.1.1.1,demod,1824,420,flip.1] ~(x+y)+ (~(y+z)+x)= ~(x+y)+x. 2089 [para_into,591.1.1.1.1.1,1467.1.1,demod,1923,446,1850,flip.1] ~((x+ ~y)+z)+y=y. 2105 [para_from,591.1.1,535.1.1.2.1,demod,1873,420,flip.1] (x+y)+ ~(~(y+z)+x)=x+ ~(~(y+z)+x). 2193 [para_into,2089.1.1.1.1,601.1.1] ~(x+ (y+ ~z))+z=z. 2312,2311 [para_into,2193.1.1.1.1.2,455.1.1] ~(x+y)+ (~y+z)= ~y+z. 2316,2315 [back_demod,1833,demod,2312,flip.1] ~(x+y)+x= ~y+x. 2318,2317 [back_demod,2077,demod,2316] ~(x+y)+ (~(y+z)+x)= ~y+x. 2330,2329 [back_demod,211,demod,2316] x+ ~(~y+x)=x+y. 2331 [back_demod,2105,demod,2330] (x+y)+ ~(~(y+z)+x)=x+ (y+z). 12476 [para_from,2317.1.1,697.1.1.1.1.2.1,demod,456,2318] ~x+ (~(x+y)+z)= ~x+z. 12737,12736 [para_into,12476.1.1.2.1.1,1129.1.1,demod,420,420,420] (x+y)+ (y+z)= (x+y)+z. 12823,12822 [para_into,12476.1.1.2,593.1.1,demod,420,420,flip.1] (x+y)+ ~(z+x)= (x+y)+ ~z. 12875,12874 [back_demod,2331,demod,12823,420,12737] (x+y)+z=x+ (y+z). 13587 [back_demod,443,demod,12875,498] x+y=y+x. 13588 [back_demod,2,demod,12875,unit_del,13587,1] ~(~(A+B)+ ~(~A+B))!=B|$Ans(Robbins_basis). 14202,14201 [para_from,13587.1.1,535.1.1.2.1] ~(~x+y)+ ~(x+y)= ~y. 14261 [para_from,13587.1.1,13588.1.1.1,demod,14202,420] B!=B|$Ans(Robbins_basis). 14262 [binary,14261.1,1.1] $Ans(Robbins_basis). ------------ end of proof -------------