----- Otter 3.1-b0, May 2000 ----- ----> UNIT CONFLICT at 40.75 sec ----> 14721 [binary,14720.1,1.1] $Ans(Robbins_basis). Length of proof is 122. Level of proof is 37. ---------------- 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.2.1,3.1.1] ~(~(x+y)+ ~y)+ ~(z+ ~y)=y. 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.2.1,5.1.1] ~(~(x+ (y+ ~z))+ ~(y+ ~z))+ ~z=y+ ~z. 12,11 [para_from,5.1.1,3.1.1.2.1.2.1] ~(~(x+ ~y)+ ~z)+ ~(~(z+ ~(u+ ~z))+ ~y)=z. 13 [para_from,5.1.1,3.1.1.2.1.1.1.2.1] ~(x+ ~(y+ ~z))+ ~(~((y+ ~z)+ ~z)+ ~(u+x))=y+ ~z. 18,17 [para_into,11.1.1.1.1,9.1.1] ~(x+ ~y)+ ~(~(y+ ~(z+ ~y))+ ~(x+ ~y))=y. 19 [para_into,11.1.1.1.1,5.1.1] ~x+ ~(~((y+ ~x)+ ~(z+ ~(y+ ~x)))+ ~x)=y+ ~x. 21 [para_into,11.1.1.2.1.1.1.2.1,5.1.1] ~(~(x+ ~y)+ ~(z+ ~u))+ ~(~((z+ ~u)+ ~u)+ ~y)=z+ ~u. 24,23 [para_from,11.1.1,9.1.1.1.1.2.1,demod,12,12] ~(~(x+y)+ ~y)+ ~(~(y+ ~(z+ ~y))+ ~u)=y. 28,27 [para_from,17.1.1,3.1.1.2.1] ~(~(x+ ~(y+ ~x))+ ~x)+ ~(y+ ~x)=x. 29 [para_into,27.1.1.1.1.1.1.2.1,27.1.1,demod,28] ~(~((x+ ~y)+ ~y)+ ~(x+ ~y))+ ~y=x+ ~y. 31 [para_from,23.1.1,3.1.1.2.1.1.1] ~(x+ ~ ~(~(y+z)+ ~z))+ ~(~z+ ~(u+x))= ~(~(y+z)+ ~z). 35 [para_into,13.1.1.1.1,5.1.1] ~x+ ~(~((y+ ~x)+ ~x)+ ~(z+ ~(~(u+x)+ ~x)))=y+ ~x. 39 [para_into,19.1.1.2.1.1.1.2.1,27.1.1] ~x+ ~(~((y+ ~x)+ ~x)+ ~x)=y+ ~x. 42,41 [para_from,19.1.1,23.1.1.2.1] ~(~(x+y)+ ~y)+ ~(z+ ~(y+ ~(u+ ~y)))=y. 43 [para_from,19.1.1,3.1.1.2.1] ~(~(x+ ~(y+ ~x))+ ~x)+ ~(z+ ~(x+ ~(y+ ~x)))=x. 47 [para_from,41.1.1,13.1.1.2.1.1.1.1,demod,42,42] ~(x+ ~y)+ ~(~(y+ ~(z+ ~(y+ ~(u+ ~y))))+ ~(v+x))=y. 49 [para_from,41.1.1,7.1.1.2.1.2.1.1,demod,42,42] ~(~(x+ ~(y+ ~(z+ ~y)))+ ~ ~y)+ ~(u+ ~ ~y)= ~y. 56,55 [para_into,43.1.1.1.1.1.1,23.1.1,demod,24] ~(~x+ ~ ~(~(y+x)+ ~x))+ ~(z+ ~x)= ~(~(y+x)+ ~x). 63 [para_from,55.1.1,41.1.1.2.1] ~(~(x+y)+ ~y)+ ~ ~(~(z+ (u+ ~y))+ ~(u+ ~y))=y. 67 [para_from,55.1.1,39.1.1.2.1.1.1.1,demod,6,56] ~(x+ ~y)+ ~(~y+ ~(x+ ~y))= ~(~(z+y)+ ~y). 72,71 [para_into,67.1.1.1.1,27.1.1,demod,28,flip.1] ~(~(x+ (y+ ~z))+ ~(y+ ~z))= ~z+ ~(~(y+ ~z)+ ~z). 74 [para_into,67.1.1,67.1.1] ~(~(x+y)+ ~y)= ~(~(z+y)+ ~y). 78,77 [back_demod,63,demod,72] ~(~(x+y)+ ~y)+ ~(~y+ ~(~(z+ ~y)+ ~y))=y. 83 [back_demod,9,demod,72] (~x+ ~(~(y+ ~x)+ ~x))+ ~x=y+ ~x. 88 [para_from,31.1.1,49.1.1.1.1.1.1] ~(~ ~(~(x+y)+ ~y)+ ~ ~ ~y)+ ~(z+ ~ ~ ~y)= ~ ~y. 92 [para_from,31.1.1,47.1.1.2.1.1.1.2.1] ~(x+ ~ ~y)+ ~(~(~y+ ~ ~(~(z+y)+ ~y))+ ~(u+x))= ~y. 94 [para_from,31.1.1,41.1.1.2.1] ~(~(x+ ~y)+ ~ ~y)+ ~ ~(~(z+y)+ ~y)= ~y. 105,104 [para_from,74.1.1,41.1.1.2,demod,72,18] ~(~(x+y)+ ~y)+y=y. 110 [para_from,74.1.1,21.1.1.2] ~(~(x+ ~ ~y)+ ~(z+ ~y))+ ~(~(u+ ~y)+ ~ ~y)=z+ ~y. 118 [para_from,74.1.1,55.1.1.2.1.2,demod,72,78,72] ~x+ ~(y+ ~(~(z+x)+ ~x))= ~x+ ~(~(~(u+x)+ ~x)+ ~x). 120 [copy,118,flip.1] ~x+ ~(~(~(y+x)+ ~x)+ ~x)= ~x+ ~(z+ ~(~(u+x)+ ~x)). 123,122 [para_into,104.1.1.1.1.1.1,104.1.1] ~(~x+ ~x)+x=x. 156 [para_from,104.1.1,21.1.1.2.1.1.1.1,demod,105,105] ~(~(x+ ~y)+ ~ ~z)+ ~(~(~z+ ~z)+ ~y)= ~z. 166 [para_from,104.1.1,39.1.1.2.1.1.1.1,demod,105] ~x+ ~(~(~x+ ~x)+ ~x)= ~x. 177,176 [para_from,104.1.1,74.1.1.1.1.1,flip.1] ~(~(x+y)+ ~y)= ~(~y+ ~y). 180 [para_from,104.1.1,23.1.1.1.1.1.1] ~(~x+ ~x)+ ~(~(x+ ~(y+ ~x))+ ~z)=x. 182 [para_from,104.1.1,5.1.1.1.1.1.1] ~(~x+ ~x)+ ~(y+ ~x)=x. 184 [para_from,104.1.1,31.1.1.2.1.2.1,demod,177,177] ~(x+ ~ ~(~y+ ~y))+ ~(~y+ ~x)= ~(~y+ ~y). 191,190 [para_from,104.1.1,5.1.1.2.1,demod,177] ~(~x+ ~x)+ ~ ~x=x. 201,200 [para_from,104.1.1,29.1.1.1.1.1.1.1,demod,177,123,191,177,123] ~x+ ~x= ~x. 228 [back_demod,120,demod,177,201,177,201] ~x+ ~(~ ~x+ ~x)= ~x+ ~(y+ ~ ~x). 230 [back_demod,110,demod,177,201] ~(~(x+ ~ ~y)+ ~(z+ ~y))+ ~ ~ ~y=z+ ~y. 239,238 [back_demod,94,demod,177,201,177,201,201] ~ ~ ~x= ~x. 240 [back_demod,92,demod,177,201,239,201] ~(x+ ~ ~y)+ ~(~ ~y+ ~(z+x))= ~y. 243,242 [back_demod,88,demod,177,201,239,239,201,239] ~ ~x+ ~(y+ ~x)= ~ ~x. 249,248 [back_demod,71,demod,177,201,flip.1] ~x+ ~(~(y+ ~x)+ ~x)= ~ ~(y+ ~x). 256 [back_demod,35,demod,177,201] ~x+ ~(~((y+ ~x)+ ~x)+ ~(z+ ~ ~x))=y+ ~x. 263,262 [back_demod,5,demod,177,201,243] ~ ~x=x. 267,266 [back_demod,190,demod,201,263,263] x+x=x. 268 [back_demod,184,demod,267,263,267,263] ~(x+ ~y)+ ~(~y+ ~x)=y. 271,270 [back_demod,182,demod,267,263] x+ ~(y+ ~x)=x. 272 [back_demod,180,demod,267,263,271] x+ ~(~x+ ~y)=x. 274 [back_demod,176,demod,267,263] ~(~(x+y)+ ~y)=y. 277,276 [back_demod,166,demod,267,263] ~x+ ~(x+ ~x)= ~x. 278 [back_demod,156,demod,263,267,263] ~(~(x+ ~y)+z)+ ~(z+ ~y)= ~z. 282 [copy,228,flip.1,demod,263,263,277] ~x+ ~(y+x)= ~x. 296 [back_demod,230,demod,263,263] ~(~(x+y)+ ~(z+ ~y))+ ~y=z+ ~y. 303,302 [back_demod,83,demod,249,263] (x+ ~y)+ ~y=x+ ~y. 306 [back_demod,240,demod,263,263] ~(x+y)+ ~(y+ ~(z+x))= ~y. 308 [back_demod,256,demod,303,263] ~x+ ~(~(y+ ~x)+ ~(z+x))=y+ ~x. 327,326 [para_into,272.1.1.2.1.2,262.1.1] x+ ~(~x+y)=x. 328 [para_into,268.1.1.1.1.2,262.1.1,demod,263] ~(x+y)+ ~(y+ ~x)= ~y. 341,340 [para_into,326.1.1.2.1.1,262.1.1] ~x+ ~(x+y)= ~x. 359,358 [para_from,274.1.1,262.1.1.1,flip.1] ~(x+y)+ ~y= ~y. 360 [para_into,278.1.1.1.1.1.1.2,262.1.1,demod,263] ~(~(x+y)+z)+ ~(z+y)= ~z. 378 [para_from,340.1.1,282.1.1.2.1,demod,263,263,263] (x+y)+x=x+y. 391,390 [para_into,358.1.1.1.1,282.1.1,demod,263,263,263] x+ (y+x)=y+x. 402 [para_into,296.1.1.1.1.1.1,296.1.1,demod,263,263,263] ~(~(x+ ~y)+ ~(z+y))+y=z+y. 408 [para_into,296.1.1.1.1.2.1,340.1.1,demod,263,341] ~(~(x+ (y+z))+y)+ ~(y+z)= ~y. 412 [para_into,390.1.1.2,326.1.1,demod,327] ~(~x+y)+x=x. 422 [para_into,306.1.1.1.1,306.1.1,demod,263,263] x+ ~(~(x+ ~(y+z))+ ~(u+ ~(z+x)))=x+ ~(y+z). 424 [para_into,306.1.1.1.1,296.1.1,demod,263] ~(x+ ~y)+ ~(~y+ ~(z+ ~(~(u+y)+ ~(x+ ~y))))=y. 428 [para_into,306.1.1.2.1.2.1,378.1.1] ~(x+y)+ ~(y+ ~(x+z))= ~y. 430 [para_into,306.1.1.2.1.2.1,358.1.1,demod,263] ~(~x+y)+ ~(y+x)= ~y. 432 [para_into,306.1.1.2.1.2.1,340.1.1,demod,263] ~(~(x+y)+z)+ ~(z+x)= ~z. 438 [para_into,328.1.1.1.1,378.1.1] ~(x+y)+ ~(x+ ~(x+y))= ~x. 448 [para_into,328.1.1.1.1,282.1.1,demod,263,263,263] x+ ~(~(y+x)+x)=y+x. 450 [para_into,328.1.1.2.1,412.1.1,demod,263,263,263,263] ~(x+ ~(x+y))+x=x+y. 452 [para_into,328.1.1.2.1,328.1.1,demod,263,263] ~((x+ ~y)+ ~(y+x))+x=y+x. 468 [para_into,308.1.1.2.1,412.1.1,demod,263,263] ~x+ (y+x)= (y+x)+ ~x. 472 [para_into,430.1.1.1.1,430.1.1,demod,263,263] x+ ~(~(x+y)+ (~y+x))=x+y. 481,480 [para_into,448.1.1.2.1,412.1.1,flip.1] ~x+x=x+ ~x. 520 [para_into,468.1.1.2,326.1.1,demod,263,327,263] (~x+y)+x=x+ (~x+y). 542 [para_from,360.1.1,306.1.1.2.1,demod,263,263] ~(x+ ~(~(y+x)+z))+z= ~(y+x)+z. 618 [para_from,520.1.1,360.1.1.2.1] ~(~(x+y)+ (~y+z))+ ~(y+ (~y+z))= ~(~y+z). 620 [para_from,520.1.1,306.1.1.1.1] ~(x+ (~x+y))+ ~(x+ ~(z+ (~x+y)))= ~x. 708 [para_into,432.1.1.1.1,432.1.1,demod,263,263] x+ ~(~(x+y)+ ~(y+z))=x+y. 712 [para_into,432.1.1.1.1,360.1.1,demod,263,263] x+ ~(~(x+y)+ ~(z+y))=x+y. 774 [para_from,402.1.1,306.1.1.1.1] ~(x+y)+ ~(y+ ~(z+ ~(~(u+ ~y)+ ~(x+y))))= ~y. 822 [para_into,452.1.1.1.1.1,328.1.1] ~(~x+ ~((x+ ~y)+ ~(y+x)))+ ~(y+x)= (x+ ~y)+ ~(y+x). 870 [para_into,472.1.1.2.1.2,430.1.1] ~(x+y)+ ~(~(~(x+y)+ (~y+x))+ ~x)= ~(x+y)+ (~y+x). 1105,1104 [para_from,408.1.1,308.1.1.2.1,demod,263,267,481,flip.1] ~(x+ (y+ ~y))+ ~y= ~y. 1125,1124 [para_into,1104.1.1.1.1.2.2,262.1.1,demod,481,263,263] ~(x+ (y+ ~y))+y=y. 1164 [para_from,1104.1.1,438.1.1.2.1.2.1,demod,1105,263,263,1125,263,flip.1] x+ (y+ ~y)=y+ ~y. 1179,1178 [para_from,1164.1.1,412.1.1.1.1] ~(x+ ~x)+y=y. 1181,1180 [para_from,1164.1.1,326.1.1.2.1] x+ ~(y+ ~y)=x. 1207 [para_from,1178.1.1,712.1.1.2.1,demod,263] x+ (y+ ~x)=x+ ~x. 1210,1209 [para_from,1178.1.1,708.1.1.2.1,demod,263] x+ (~x+y)=x+ ~x. 1248,1247 [back_demod,620,demod,1210,1179] ~(x+ ~(y+ (~x+z)))= ~x. 1250,1249 [back_demod,618,demod,1210,1181] ~(~(x+y)+ (~y+z))= ~(~y+z). 1251 [back_demod,520,demod,1210] (~x+y)+x=x+ ~x. 1256 [back_demod,870,demod,1250,359,263,flip.1] ~(x+y)+ (~y+x)= ~(x+y)+x. 1417,1416 [para_from,1207.1.1,428.1.1.1.1,demod,1179] ~((x+ ~y)+ ~(y+z))= ~(x+ ~y). 1424 [back_demod,822,demod,1417,341,263,flip.1] (x+ ~y)+ ~(y+x)=x+ ~(y+x). 1565,1564 [para_into,422.1.1.2.1.2.1.2.1,1251.1.1,demod,1248,1181,327,flip.1] x+ ~(y+ (~x+z))=x. 1633 [para_into,1564.1.1.2.1,450.1.1] x+ ~((~x+y)+z)=x. 1659 [para_from,1564.1.1,390.1.1.2,demod,1565] ~(x+ (~y+z))+y=y. 1782,1781 [para_into,1633.1.1.2.1.1,424.1.1] (x+ ~y)+ ~(y+z)=x+ ~y. 1788,1787 [back_demod,1424,demod,1782,flip.1] x+ ~(y+x)=x+ ~y. 1862,1861 [para_into,1659.1.1.1.1.2,412.1.1] ~(x+y)+ (~y+z)= ~y+z. 1864,1863 [back_demod,1256,demod,1862,flip.1] ~(x+y)+x= ~y+x. 1978,1977 [para_into,1787.1.1.2.1,432.1.1,demod,263,1864,263,flip.1] ~(x+y)+ (~(y+z)+x)= ~y+x. 2149 [para_into,1863.1.1.1.1,432.1.1,demod,263,1788,263,263,flip.1] (x+y)+ ~(~(y+z)+x)=x+ (y+z). 12655 [para_from,1977.1.1,542.1.1.1.1.2.1,demod,327,1978] ~x+ (~(x+y)+z)= ~x+z. 12938,12937 [para_into,12655.1.1.2.1.1,774.1.1,demod,263,263,263] (x+y)+ (y+z)= (x+y)+z. 13040,13039 [para_into,12655.1.1.2,432.1.1,demod,263,263,flip.1] (x+y)+ ~(z+x)= (x+y)+ ~z. 13102,13101 [back_demod,2149,demod,13040,263,12938] (x+y)+z=x+ (y+z). 13894 [back_demod,378,demod,13102,391] x+y=y+x. 13895 [back_demod,2,demod,13102,unit_del,13894,1] ~(~(A+B)+ ~(~A+B))!=B|$Ans(Robbins_basis). 14624,14623 [para_from,13894.1.1,430.1.1.2.1] ~(~x+y)+ ~(x+y)= ~y. 14720 [para_from,13894.1.1,13895.1.1.1,demod,14624,263] B!=B|$Ans(Robbins_basis). 14721 [binary,14720.1,1.1] $Ans(Robbins_basis). ------------ end of proof -------------