----- Otter 3.1-b0, May 2000 ----- ----> UNIT CONFLICT at 47.51 sec ----> 16520 [binary,16519.1,1.1] $Ans(Robbins_basis). Length of proof is 130. Level of proof is 36. ---------------- 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))+ ~(u+x)))=y. 6,5 [para_into,3.1.1.1.2,3.1.1] ~(~(~(x+ ~y)+y)+ ~(z+y))=y. 8,7 [para_into,5.1.1.1.1.1.1,5.1.1] ~(~(x+ (y+x))+ ~(z+ (y+x)))=y+x. 9 [para_into,5.1.1.1.2,5.1.1] ~(~(~(x+ ~ ~(y+z))+ ~(y+z))+z)= ~(y+z). 12,11 [para_from,5.1.1,3.1.1.1.2.1.2] ~(~(~(x+y)+z)+ ~(~(~z+ ~(u+z))+y))=z. 13 [para_from,5.1.1,3.1.1.1.2.1.1.1.2] ~(~(x+ ~(y+z))+ ~(~(~ ~(y+z)+z)+ ~(u+x)))= ~(y+z). 17 [para_into,11.1.1.1.1.1.1,11.1.1] ~(~(x+y)+ ~(~(~y+ ~(z+y))+ ~(~(~x+ ~(u+x))+v)))=y. 19 [para_into,11.1.1.1.1,9.1.1] ~(~(x+y)+ ~(~(~y+ ~(z+y))+ ~(x+y)))=y. 21 [para_into,11.1.1.1.1,5.1.1] ~(x+ ~(~(~ ~(y+x)+ ~(z+ ~(y+x)))+x))= ~(y+x). 23 [para_into,11.1.1.1.2.1.1.1.2,5.1.1] ~(~(~(x+y)+ ~(z+u))+ ~(~(~ ~(z+u)+u)+y))= ~(z+u). 25 [para_from,11.1.1,9.1.1.1.1.1.2,demod,12,12] ~(~(~(x+ ~y)+y)+ ~(~(~y+ ~(z+y))+u))=y. 27 [para_from,11.1.1,3.1.1.1.2.1.2] ~(~(~(~(~x+ ~(y+x))+z)+u)+ ~(~(~u+ ~(v+u))+x))=u. 29 [para_from,19.1.1,3.1.1.1.2] ~(~(~(~x+ ~(y+x))+x)+ ~(y+x))=x. 35 [para_into,13.1.1.1.1,5.1.1] ~(x+ ~(~(~ ~(y+x)+x)+ ~(z+ ~(~(u+ ~x)+x))))= ~(y+x). 37 [para_from,13.1.1,11.1.1.1.2] ~(~(~(x+ ~(~(~ ~(y+z)+z)+ ~(u+ ~z)))+z)+ ~(y+z))=z. 41 [para_from,25.1.1,11.1.1.1.2.1.1] ~(~(~(x+y)+ (~(z+ ~u)+u))+ ~(u+y))= ~(z+ ~u)+u. 45 [para_into,21.1.1.1.2.1.1.1.2,29.1.1] ~(x+ ~(~(~ ~(y+x)+x)+x))= ~(y+x). 58,57 [para_into,17.1.1.1.2,19.1.1] ~(~(~(x+y)+y)+ ~(x+y))=y. 61 [para_into,57.1.1.1.1.1.1,57.1.1,demod,58] ~(~(x+ ~(y+x))+x)= ~(y+x). 68,67 [para_into,61.1.1.1.1,45.1.1,flip.1] ~(~(~ ~(x+y)+y)+y)= ~(~(x+y)+y). 75 [back_demod,45,demod,68] ~(x+ ~(~(y+x)+x))= ~(y+x). 88,87 [para_into,75.1.1,3.1.1,flip.1] ~(~x+ ~(x+x))=x. 103 [para_into,87.1.1.1.1,87.1.1] ~(x+ ~((~x+ ~(x+x))+ (~x+ ~(x+x))))= ~x+ ~(x+x). 109 [para_from,87.1.1,29.1.1.1.1.1.1] ~(~(x+x)+ ~(x+x))=x. 111 [para_from,87.1.1,25.1.1.1.2] ~(~(~(x+ ~y)+y)+ (~y+ ~(z+y)))=y. 114,113 [para_from,87.1.1,23.1.1.1.2.1.1.1.1.1,demod,88,88,88] ~(~(~(x+y)+z)+ ~(z+y))=z. 123 [para_from,87.1.1,13.1.1.1.1.1.2,demod,88,88,88] ~(~(x+y)+ ~(y+ ~(z+x)))=y. 127 [para_from,87.1.1,25.1.1.1.2.1.1] ~(~(~(x+ ~y)+y)+ ~(y+z))=y. 134,133 [para_into,109.1.1.1.1,7.1.1,demod,8] ~((x+y)+ (x+y))= ~(y+ (x+y)). 136,135 [para_into,109.1.1.1.1,5.1.1,demod,6,flip.1] ~(~(x+ ~y)+y)= ~(y+y). 137 [back_demod,103,demod,134] ~(x+ ~(~(x+x)+ (~x+ ~(x+x))))= ~x+ ~(x+x). 139 [back_demod,127,demod,136] ~(~(x+x)+ ~(x+y))=x. 142,141 [back_demod,111,demod,136] ~(~(x+x)+ (~x+ ~(y+x)))=x. 147 [back_demod,35,demod,136] ~(x+ ~(~(~ ~(y+x)+x)+ ~(z+ ~(x+x))))= ~(y+x). 151 [back_demod,9,demod,136] ~(~(~(x+y)+ ~(x+y))+y)= ~(x+y). 153 [back_demod,5,demod,136] ~(~(x+x)+ ~(y+x))=x. 156,155 [back_demod,137,demod,142,flip.1] ~x+ ~(x+x)= ~(x+x). 159 [back_demod,87,demod,156] ~ ~(x+x)=x. 164,163 [para_into,159.1.1.1,7.1.1,flip.1] ~(x+ (y+x))= ~(y+x). 166,165 [back_demod,133,demod,164] ~((x+y)+ (x+y))= ~(x+y). 186,185 [para_from,163.1.1,29.1.1.1.2,demod,164,136,166] ~(~(x+y)+ ~(x+y))=x+y. 200,199 [back_demod,151,demod,186] ~((x+y)+y)= ~(x+y). 208,207 [para_from,139.1.1,159.1.1.1,flip.1] ~(x+x)= ~x. 209 [para_from,139.1.1,139.1.1.1.1,demod,208,208] ~(x+ ~(~x+y))= ~x. 214,213 [para_from,139.1.1,29.1.1.1.1.1.1,demod,164,208,164,208,208] ~ ~x=x+x. 215 [para_from,139.1.1,27.1.1.1.1.1.1.1.1] ~(~(~(x+y)+z)+ ~(~(~z+ ~(u+z))+ (x+x)))=z. 222,221 [para_from,139.1.1,61.1.1.1.1.1.2,demod,114,208,flip.1] ~(~x+ ~(x+y))=x. 239 [para_from,139.1.1,17.1.1.1.2.1.1] ~(~(x+ (y+y))+ ~(y+ ~(~(~x+ ~(z+x))+u)))=y+y. 245 [para_from,139.1.1,57.1.1.1.2,demod,208,222] ~(~(x+ ~(x+y))+x)= ~(x+y). 260,259 [back_demod,159,demod,208,214] x+x=x. 262,261 [back_demod,153,demod,260] ~(~x+ ~(y+x))=x. 263 [back_demod,147,demod,214,260,200,260] ~(x+ ~(~(y+x)+ ~(z+ ~x)))= ~(y+x). 268,267 [back_demod,135,demod,260] ~(~(x+ ~y)+y)= ~y. 281 [back_demod,37,demod,214,260,200] ~(~(~(x+ ~(~(y+z)+ ~(u+ ~z)))+z)+ ~(y+z))=z. 305 [back_demod,239,demod,260,262,260] ~(~(x+y)+ ~(y+ ~(x+z)))=y. 307 [back_demod,215,demod,262,260] ~(~(~(x+y)+z)+ ~(z+x))=z. 310,309 [back_demod,213,demod,260] ~ ~x=x. 343 [para_from,259.1.1,41.1.1.1.1.1.1.1] ~(~(~x+ (~(y+ ~z)+z))+ ~(z+x))= ~(y+ ~z)+z. 348,347 [para_into,309.1.1.1,163.1.1,demod,310,flip.1] x+ (y+x)=y+x. 349 [para_into,309.1.1.1,75.1.1,demod,310,flip.1] x+ ~(~(y+x)+x)=y+x. 356,355 [para_into,309.1.1.1,41.1.1,demod,268,flip.1] ~(~(x+y)+ (~(z+ ~u)+u))+ ~(u+y)= ~u. 358,357 [back_demod,41,demod,356,310,flip.1] ~(x+ ~y)+y=y. 359 [back_demod,355,demod,358] ~(~(x+y)+z)+ ~(z+y)= ~z. 361 [back_demod,343,demod,358,358] ~(~(~x+y)+ ~(y+x))=y. 374,373 [para_into,357.1.1.1.1.2,309.1.1] ~(x+y)+ ~y= ~y. 378,377 [para_from,221.1.1,309.1.1.1,flip.1] ~x+ ~(x+y)= ~x. 379 [para_from,221.1.1,357.1.1.1] x+ (x+y)=x+y. 383 [para_into,123.1.1.1.2.1.2.1,357.1.1] ~(~(x+y)+ ~(y+ ~x))=y. 389 [para_from,123.1.1,309.1.1.1,flip.1] ~(x+y)+ ~(y+ ~(z+x))= ~y. 398,397 [para_from,209.1.1,309.1.1.1,demod,310,flip.1] x+ ~(~x+y)=x. 399 [para_into,397.1.1.2.1,347.1.1] x+ ~(y+ ~x)=x. 401 [para_from,397.1.1,347.1.1.2,demod,398] ~(~x+y)+x=x. 405 [para_into,401.1.1.1.1.1,309.1.1] ~(x+y)+ ~x= ~x. 409 [para_into,245.1.1.1.1.1,399.1.1] ~(~x+x)= ~(x+ ~x). 414,413 [para_from,377.1.1,399.1.1.2.1,demod,310] (x+y)+x=x+y. 431 [para_into,263.1.1.1.2.1,401.1.1,demod,310,310,flip.1] ~((x+ ~y)+y)= ~(y+ (x+ ~y)). 437 [para_from,263.1.1,309.1.1.1,demod,310,flip.1] x+ ~(~(y+x)+ ~(z+ ~x))=y+x. 448,447 [para_from,409.1.1,309.1.1.1,demod,310,flip.1] ~x+x=x+ ~x. 460,459 [para_into,349.1.1.2.1.1.1,413.1.1,demod,414] x+ ~(~(x+y)+x)=x+y. 468,467 [para_into,349.1.1.2.1.1.1,377.1.1,demod,310,378] ~(x+y)+ ~(x+ ~(x+y))= ~x. 475 [para_from,361.1.1,349.1.1.2.1.1,demod,468,flip.1] ~(~x+y)+ ~(y+x)= ~y. 479 [para_into,281.1.1.1.1.1.1.1.2.1.1.1,413.1.1,demod,414] ~(~(~(x+ ~(~(y+z)+ ~(u+ ~y)))+y)+ ~(y+z))=y. 507 [para_from,383.1.1,349.1.1.2.1.1,demod,468,flip.1] ~(x+y)+ ~(y+ ~x)= ~y. 523 [para_into,475.1.1.1.1,475.1.1,demod,310,310] x+ ~(~(x+y)+ (~y+x))=x+y. 529 [para_into,507.1.1.2.1,507.1.1,demod,310,310] ~((x+ ~y)+ ~(y+x))+x=y+x. 555 [para_from,305.1.1,475.1.1.1,demod,310] x+ ~(~(x+ ~(y+z))+ (y+x))=x+ ~(y+z). 559 [para_from,305.1.1,349.1.1.2.1.1,demod,468,flip.1] ~(x+y)+ ~(y+ ~(x+z))= ~y. 589 [para_from,307.1.1,475.1.1.1,demod,310] x+ ~(~(x+y)+ (~(y+z)+x))=x+y. 591 [para_from,307.1.1,507.1.1.2,demod,310] ~((x+y)+ ~(~(y+z)+x))+x= ~(y+z)+x. 593 [para_from,307.1.1,349.1.1.2.1.1,demod,468,flip.1] ~(~(x+y)+z)+ ~(z+x)= ~z. 607 [para_into,359.1.1.2.1,405.1.1,demod,310,310] ~(~(x+ ~y)+ ~(y+z))+y=y+z. 611 [para_into,359.1.1.2.1,379.1.1] ~(~(x+ (y+z))+y)+ ~(y+z)= ~y. 657 [para_into,389.1.1.2.1,389.1.1,demod,310,310] ~(~(x+y)+ ~(y+z))+z=y+z. 661 [para_into,389.1.1.2.1,359.1.1,demod,310,310] ~(x+ ~(~(y+x)+z))+z= ~(y+x)+z. 690,689 [para_from,431.1.1,349.1.1.2.1.1,demod,460,flip.1] (x+ ~y)+y=y+ (x+ ~y). 702 [para_into,689.1.1.1,413.1.1,demod,414] (~x+y)+x=x+ (~x+y). 737 [para_from,702.1.1,359.1.1.2.1] ~(~(x+y)+ (~y+z))+ ~(y+ (~y+z))= ~(~y+z). 839 [para_into,593.1.1.1.1,593.1.1,demod,310,310] x+ ~(~(x+y)+ ~(y+z))=x+y. 1019 [para_into,523.1.1.2.1.2,475.1.1] ~(x+y)+ ~(~(~(x+y)+ (~y+x))+ ~x)= ~(x+y)+ (~y+x). 1043 [para_from,479.1.1,437.1.1.2,demod,260,flip.1] ~(x+ ~(~(y+ ~y)+ ~(z+ ~y)))+y=y. 1051 [para_into,529.1.1.1.1.1,507.1.1] ~(~x+ ~((x+ ~y)+ ~(y+x)))+ ~(y+x)= (x+ ~y)+ ~(y+x). 1111 [para_from,657.1.1,389.1.1.1.1] ~(x+y)+ ~(y+ ~(z+ ~(~(u+x)+ ~(x+y))))= ~y. 1368,1367 [para_from,611.1.1,437.1.1.2.1,demod,310,260,flip.1] ~(x+ (y+ ~y))+y=y. 1388,1387 [para_into,1367.1.1.1.1.2.2,309.1.1,demod,448] ~(x+ (y+ ~y))+ ~y= ~y. 1430,1429 [para_from,1367.1.1,467.1.1.1.1,demod,1368,1388,310,448,310,flip.1] x+ (y+ ~y)=y+ ~y. 1492,1491 [para_from,1429.1.1,401.1.1.1.1] ~(x+ ~x)+y=y. 1494,1493 [para_from,1429.1.1,397.1.1.2.1] x+ ~(y+ ~y)=x. 1495 [para_from,1429.1.1,607.1.1.1.1.2.1,demod,1494,310,690,1430] x+ (y+ ~x)=z+ ~z. 1497 [back_demod,1043,demod,1492,310] ~(x+ (y+ ~z))+z=z. 1509,1508 [para_from,1491.1.1,839.1.1.2.1,demod,310] x+ (~x+y)=x+ ~x. 1513 [para_from,1491.1.1,593.1.1.2.1,demod,1494,310,310] (x+y)+ ~x=z+ ~z. 1534,1533 [back_demod,737,demod,1509,1494] ~(~(x+y)+ (~y+z))= ~(~y+z). 1591 [back_demod,1019,demod,1534,374,310,flip.1] ~(x+y)+ (~y+x)= ~(x+y)+x. 1678,1677 [para_from,1495.1.1,559.1.1.1.1,demod,1492] ~((x+ ~y)+ ~(y+z))= ~(x+ ~y). 1693 [back_demod,1051,demod,1678,378,310,flip.1] (x+ ~y)+ ~(y+x)=x+ ~(y+x). 1706,1705 [para_into,555.1.1.2.1.2,1495.1.1,demod,1678,1430,1494,flip.1] (x+ ~y)+ ~(y+z)=x+ ~y. 1718,1717 [back_demod,1693,demod,1706,flip.1] x+ ~(y+x)=x+ ~y. 1744,1743 [para_into,1497.1.1.1.1.2.2,309.1.1] ~(x+ (y+z))+ ~z= ~z. 1764,1763 [para_into,1497.1.1.1.1.2,397.1.1] ~(x+y)+ (~y+z)= ~y+z. 1770,1769 [back_demod,1591,demod,1764,flip.1] ~(x+y)+x= ~y+x. 1952,1951 [para_from,1513.1.1,559.1.1.1.1,demod,1492,310] ~(~x+ ~((x+y)+z))=x. 2029,2028 [para_from,589.1.1,507.1.1.1.1,demod,1744,310,1770,310,flip.1] ~(x+y)+ (~(y+z)+x)= ~y+x. 2115 [para_from,591.1.1,475.1.1.2.1,demod,1952,1718,310,310,flip.1] (x+y)+ ~(~(y+z)+x)=x+ (y+z). 14611 [para_from,2028.1.1,661.1.1.1.1.2.1,demod,398,2029] ~x+ (~(x+y)+z)= ~x+z. 14890,14889 [para_into,14611.1.1.2.1.1,1111.1.1,demod,310,310,310] (x+y)+ (y+z)= (x+y)+z. 14986,14985 [para_into,14611.1.1.2,593.1.1,demod,310,310,flip.1] (x+y)+ ~(z+x)= (x+y)+ ~z. 15054,15053 [back_demod,2115,demod,14986,310,14890] (x+y)+z=x+ (y+z). 15813 [back_demod,413,demod,15054,348] x+y=y+x. 15814 [back_demod,2,demod,15054,unit_del,15813,1] ~(~(A+B)+ ~(~A+B))!=B|$Ans(Robbins_basis). 16456,16455 [para_from,15813.1.1,475.1.1.2.1] ~(~x+y)+ ~(x+y)= ~y. 16519 [para_from,15813.1.1,15814.1.1.1,demod,16456,310] B!=B|$Ans(Robbins_basis). 16520 [binary,16519.1,1.1] $Ans(Robbins_basis). ------------ end of proof -------------