----- Otter 3.1-b0, May 2000 ----- ----> UNIT CONFLICT at 22.34 sec ----> 14664 [binary,14662.1,701.1] $Ans(Robbins_basis). Length of proof is 126. 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). 4,3 [] ~(~(x+y)+ ~z)+ ~(x+ ~(z+ ~(~z+u)))=z. 5 [para_into,3.1.1.1.1.1.1,3.1.1] ~(~x+ ~y)+ ~(~(~(z+u)+ ~x)+ ~(y+ ~(~y+v)))=y. 7 [para_into,3.1.1.2.1,3.1.1] ~(~(~(~(x+y)+ ~ ~x)+z)+ ~x)+ ~ ~x=x. 10,9 [para_into,7.1.1.1.1.1.1,3.1.1] ~(~ ~x+ ~x)+ ~ ~x=x. 11 [para_from,7.1.1,3.1.1.1.1] ~x+ ~(~(~(~(x+y)+ ~ ~x)+z)+ ~(~x+ ~(~ ~x+u)))= ~x. 13 [para_from,9.1.1,3.1.1.1.1] ~x+ ~(~ ~x+ ~(~x+ ~(~ ~x+y)))= ~x. 19 [para_into,13.1.1.2.1.2.1,13.1.1] ~x+ ~(~ ~x+ ~ ~x)= ~x. 23 [para_from,13.1.1,3.1.1.2.1.2.1] ~(~(x+y)+ ~ ~z)+ ~(x+ ~ ~z)= ~z. 25 [para_from,13.1.1,3.1.1.2.1.2.1.2.1] ~(~(x+y)+ ~z)+ ~(x+ ~(z+ ~ ~z))=z. 27 [para_from,13.1.1,7.1.1.1.1.1.1.1.1.1.1] ~(~(~(~ ~x+ ~ ~ ~x)+y)+ ~ ~x)+ ~ ~ ~x= ~x. 35 [para_into,5.1.1.2.1.1.1,3.1.1] ~(~(x+ ~(y+ ~(~y+z)))+ ~u)+ ~(~y+ ~(u+ ~(~u+v)))=u. 41 [para_into,23.1.1.1.1.1.1,19.1.1] ~(~ ~x+ ~ ~y)+ ~(~x+ ~ ~y)= ~y. 47 [para_into,23.1.1.2.1,9.1.1] ~(~(~(~ ~x+ ~x)+y)+ ~ ~x)+ ~x= ~x. 79 [para_into,25.1.1.1.1.1.1,19.1.1] ~(~ ~x+ ~y)+ ~(~x+ ~(y+ ~ ~y))=y. 85 [para_into,25.1.1.1.1,23.1.1] ~ ~x+ ~(~(y+z)+ ~((y+ ~ ~x)+ ~ ~(y+ ~ ~x)))=y+ ~ ~x. 93 [para_into,47.1.1.1.1.1.1,79.1.1] ~(~x+ ~ ~x)+ ~x= ~x. 104,103 [para_from,93.1.1,23.1.1.1.1] ~ ~ ~x+ ~(~ ~x+ ~ ~x)= ~x. 115 [para_from,27.1.1,7.1.1.1.1] ~ ~x+ ~ ~ ~ ~x= ~ ~x. 119 [para_from,115.1.1,23.1.1.2.1] ~(~(~ ~x+y)+ ~ ~ ~ ~x)+ ~ ~ ~x= ~ ~ ~x. 122,121 [para_from,103.1.1,13.1.1.2.1.2.1.2.1,demod,104] ~ ~x+ ~ ~x= ~ ~x. 130,129 [back_demod,103,demod,122,122] ~ ~ ~x= ~x. 131 [back_demod,19,demod,122,130] ~x+ ~x= ~x. 133 [back_demod,119,demod,130,130,130] ~(~(~ ~x+y)+ ~ ~x)+ ~x= ~x. 150,149 [para_from,129.1.1,93.1.1.1.1.2,demod,10,flip.1] ~ ~x=x. 155 [para_from,129.1.1,41.1.1.1.1.1,demod,150,150,150] ~(~x+y)+ ~(x+y)= ~y. 161 [para_from,129.1.1,13.1.1.2.1.1,demod,150,150,150,150] x+ ~(~x+ ~(x+ ~(~x+y)))=x. 163 [para_from,129.1.1,11.1.1.2.1.2.1.2.1.1,demod,150,150,150,150] x+ ~(~(~(~(~x+y)+ ~x)+z)+ ~(x+ ~(~x+u)))=x. 170,169 [para_from,129.1.1,41.1.1.1.1.2.1,demod,150,150,150,150,150] ~(x+y)+ ~(~x+y)= ~y. 190,189 [para_from,129.1.1,23.1.1.2.1.2.1,demod,150,150,150,150] ~(~(x+y)+z)+ ~(x+z)= ~z. 201 [back_demod,133,demod,150,150] ~(~(x+y)+x)+ ~x= ~x. 219 [back_demod,85,demod,150,150,150,150,150] x+ ~(~(y+z)+ ~((y+x)+ (y+x)))=y+x. 241 [back_demod,2,demod,170,150,unit_del,1] B+A!=A+B| (A+B)+C!=A+ (B+C)|$Ans(Robbins_basis). 251,250 [para_into,131.1.1.1,149.1.1,demod,150,150] x+x=x. 254 [back_demod,219,demod,251] x+ ~(~(y+z)+ ~(y+x))=y+x. 328 [para_into,169.1.1.2.1,169.1.1,demod,150,150] ~((x+y)+ ~(~x+y))+y= ~x+y. 376 [para_from,161.1.1,169.1.1.2.1,demod,150,150,150,150,150,150] ~(x+ ~(x+ ~(~x+ ~(x+y))))+x=x+ ~(~x+ ~(x+y)). 426 [para_into,189.1.1.1.1.1.1,169.1.1,demod,150] ~(x+y)+ ~(~(z+x)+y)= ~y. 444 [para_into,189.1.1.1.1,155.1.1,demod,150,150] x+ ~(~y+ ~(y+x))=y+x. 480 [para_from,189.1.1,201.1.1.1.1,demod,150,150,150] x+ (y+x)=y+x. 502 [para_into,480.1.1.2,189.1.1,demod,190] ~(x+y)+ ~y= ~y. 511,510 [para_into,480.1.1.2,3.1.1,demod,4] ~(x+ ~(y+ ~(~y+z)))+y=y. 512 [back_demod,376,demod,511,flip.1] x+ ~(~x+ ~(x+y))=x. 542 [para_into,502.1.1.2,149.1.1,demod,150] ~(x+ ~y)+y=y. 544 [para_from,502.1.1,189.1.1.1.1,demod,150,150] x+ ~(y+ ~x)=x. 547,546 [para_from,502.1.1,163.1.1.2.1,demod,150] x+ (x+ ~(~x+y))=x. 564 [para_from,542.1.1,189.1.1.1.1] ~x+ ~(y+x)= ~x. 570 [para_into,544.1.1.2.1,189.1.1,demod,150] (x+y)+y=x+y. 576 [para_from,544.1.1,189.1.1.1.1,demod,150,150,150,150] (x+y)+ ~(x+ ~(z+ (x+y)))=z+ (x+y). 578 [para_from,544.1.1,189.1.1.2.1,demod,150] ~(~(x+y)+ ~(z+ ~x))+ ~x=z+ ~x. 600 [para_from,564.1.1,35.1.1.2.1,demod,150,150] ~(~(x+ ~(~(~y+z)+ ~((~y+z)+u)))+ ~y)+ ~(~y+z)=y. 605,604 [para_from,546.1.1,480.1.1.2,demod,547] (x+ ~(~x+y))+x=x. 615,614 [para_from,546.1.1,502.1.1.1.1] ~x+ ~(x+ ~(~x+y))= ~(x+ ~(~x+y)). 651,650 [para_into,512.1.1.2.1.1,149.1.1,demod,615] ~(x+ ~(~x+y))= ~x. 652 [para_into,512.1.1.2.1.2.1,604.1.1,demod,651,251,150,605,flip.1] x+ ~(~x+y)=x. 662,661 [para_into,652.1.1.2.1.1,149.1.1] ~x+ ~(x+y)= ~x. 663 [back_demod,600,demod,662,150] ~(~(x+ (~y+z))+ ~y)+ ~(~y+z)=y. 665 [back_demod,444,demod,662,150] x+y=y+x. 670 [para_from,652.1.1,189.1.1.1.1,demod,150,150,150,150] (x+y)+ ~(x+ ~((x+y)+z))= (x+y)+z. 678 [para_from,652.1.1,155.1.1.1.1,demod,150,150,150,150] x+ ~(x+ ~(x+y))=x+y. 680 [para_into,665.1.1,189.1.1,flip.1] ~(x+y)+ ~(~(x+z)+y)= ~y. 683 [para_from,665.1.1,189.1.1.1.1] ~(x+ ~(y+z))+ ~(y+x)= ~x. 685 [para_from,665.1.1,189.1.1.2.1] ~(~(x+y)+z)+ ~(z+x)= ~z. 687 [para_from,665.1.1,169.1.1.2.1] ~(x+y)+ ~(y+ ~x)= ~y. 689 [para_from,665.1.1,155.1.1.1.1] ~(x+ ~y)+ ~(y+x)= ~x. 691 [para_from,665.1.1,570.1.1.1] (x+y)+x=y+x. 694,693 [para_from,665.1.1,502.1.1.1.1] ~(x+y)+ ~x= ~x. 695 [para_from,665.1.1,169.1.1.1.1] ~(x+y)+ ~(~y+x)= ~x. 701 [para_from,665.1.1,241.1.1,unit_del,1] (A+B)+C!=A+ (B+C)|$Ans(Robbins_basis). 709 [para_into,254.1.1.2.1.1.1,502.1.1,demod,150] x+ ~(y+ ~(~(z+y)+x))= ~(z+y)+x. 711 [para_into,254.1.1.2.1.2.1,665.1.1] x+ ~(~(y+z)+ ~(x+y))=y+x. 721 [para_into,254.1.1.2.1,665.1.1] x+ ~(~(y+x)+ ~(y+z))=y+x. 723 [para_into,254.1.1.2.1,564.1.1,demod,150,251,flip.1] x+ (x+y)=x+y. 795,794 [para_into,661.1.1.2.1,691.1.1] ~(x+y)+ ~(y+x)= ~(x+y). 798 [para_from,661.1.1,189.1.1.2.1,demod,150,150] ~(~(~x+y)+ ~(x+z))+x=x+z. 800 [para_into,693.1.1.1.1,691.1.1,demod,795] ~(x+y)= ~(y+x). 819 [para_from,800.1.1,542.1.1.1.1.2] ~(x+ ~(y+z))+ (z+y)=z+y. 877 [para_into,678.1.1.2.1,665.1.1] x+ ~(~(x+y)+x)=x+y. 985 [para_from,689.1.1,189.1.1.2.1,demod,150,150] ~(~(~(x+ ~y)+z)+ ~(y+x))+x=y+x. 1017 [para_into,426.1.1.1.1,687.1.1,demod,150,150] x+ ~(~(y+ ~(z+x))+ ~(x+ ~z))=x+ ~z. 1790 [para_into,680.1.1.1.1,665.1.1] ~(x+y)+ ~(~(y+z)+x)= ~x. 1944 [para_into,683.1.1.2.1,665.1.1] ~(x+ ~(y+z))+ ~(x+y)= ~x. 2107,2106 [para_from,819.1.1,685.1.1.2.1,demod,150] ~(~((x+y)+z)+ ~(u+ ~(y+x)))+ ~(x+y)=u+ ~(y+x). 2288 [para_into,578.1.1.1.1.2.1.2,800.1.1,demod,2107] x+ ~(y+z)=x+ ~(z+y). 2320 [para_into,2288.1.1.2.1,794.1.1,demod,150,795,150] x+ (y+z)=x+ (z+y). 2331 [para_into,2288.1.1,665.1.1] ~(x+y)+z=z+ ~(y+x). 2345 [copy,2331,flip.1] x+ ~(y+z)= ~(z+y)+x. 2452 [para_into,2320.1.1,665.1.1] (x+y)+z=z+ (y+x). 3058 [para_into,2345.1.1,328.1.1,flip.1] ~(x+y)+ ~((z+ ~(y+x))+ ~(~z+ ~(y+x)))= ~z+ ~(y+x). 3426 [para_into,663.1.1,2331.1.1] ~(~x+y)+ ~(~x+ ~(z+ (~x+y)))=x. 4035,4034 [para_into,1944.1.1.2.1,723.1.1] ~(x+ ~((x+y)+z))+ ~(x+y)= ~x. 4549 [para_into,709.1.1.2.1,1790.1.1,demod,150,251,flip.1] ~(x+ ~(y+x))+y=y. 4553 [para_into,709.1.1.2.1,680.1.1,demod,150,251,flip.1] ~(x+ ~(x+y))+y=y. 4639 [para_into,4549.1.1.1.1.2.1,689.1.1,demod,150] ~(~(x+y)+y)+ ~(y+ ~x)= ~(y+ ~x). 4687 [para_into,4549.1.1.1.1,2345.1.1] ~(~(x+y)+x)+y=y. 4691 [para_into,4549.1.1.1.1,665.1.1] ~(~(x+y)+y)+x=x. 4699 [para_into,4549.1.1,2331.1.1] x+ ~(~(x+y)+y)=x. 4701 [para_into,4549.1.1,665.1.1] x+ ~(y+ ~(x+y))=x. 4767 [para_from,4549.1.1,695.1.1.1.1,demod,150] ~x+ ~(~x+ ~(y+ ~(x+y)))=y+ ~(x+y). 4825 [para_into,4553.1.1,2331.1.1] x+ ~(~(y+x)+y)=x. 4955 [para_into,4687.1.1.1.1.1.1,687.1.1,demod,150] ~(x+ ~(y+x))+ ~(x+ ~y)= ~(x+ ~y). 5195 [para_into,4691.1.1.1.1.1.1,711.1.1] ~(~(x+y)+ ~(~(x+z)+ ~(y+x)))+y=y. 5277 [para_from,4691.1.1,695.1.1.1.1,demod,150] ~x+ ~(~x+ ~(~(x+y)+y))= ~(x+y)+y. 5379 [para_into,4699.1.1.2.1.1.1,328.1.1] ~((x+y)+ ~(~x+y))+ ~(~(~x+y)+y)= ~((x+y)+ ~(~x+y)). 5985 [para_into,4701.1.1.2.1.2.1,1944.1.1,demod,150] ~(x+ ~(y+z))+ ~(~(x+y)+x)= ~(x+ ~(y+z)). 6021 [para_into,4701.1.1.2.1.2.1,685.1.1,demod,150] ~(~(x+y)+z)+ ~(~(z+x)+z)= ~(~(x+y)+z). 6047 [para_into,4701.1.1.2.1.2.1,254.1.1] x+ ~(~(~(y+z)+ ~(y+x))+ ~(y+x))=x. 6120,6119 [para_from,4825.1.1,709.1.1.2.1,flip.1] ~(x+y)+x=x+ ~y. 6122,6121 [back_demod,6021,demod,6120] ~(~(x+y)+z)+ ~(z+ ~x)= ~(~(x+y)+z). 6130,6129 [back_demod,5985,demod,6120] ~(x+ ~(y+z))+ ~(x+ ~y)= ~(x+ ~(y+z)). 6186,6185 [back_demod,877,demod,6120] x+ ~(x+ ~y)=x+y. 6188,6187 [back_demod,4639,demod,6122] ~(~(x+y)+y)= ~(y+ ~x). 6190,6189 [back_demod,4955,demod,6130] ~(x+ ~(y+x))= ~(x+ ~y). 6196,6195 [back_demod,5277,demod,6188,6190,6186,flip.1] ~(x+y)+y= ~x+y. 6200,6199 [back_demod,4767,demod,6190,6190,6186,flip.1] x+ ~(y+x)= ~y+x. 6213 [back_demod,6047,demod,6196,150] x+ ~((y+z)+ ~(y+x))=x. 6252,6251 [back_demod,5379,demod,6196,150,694,flip.1] ~((x+y)+ ~(~x+y))= ~(x+y). 6368,6367 [back_demod,3058,demod,6252] ~(x+y)+ ~(z+ ~(y+x))= ~z+ ~(y+x). 6383 [back_demod,5195,demod,6368,150] ~((x+y)+ ~(z+x))+z=z. 7706,7705 [para_into,798.1.1.1.1,254.1.1,demod,150,4035,150,flip.1] ~(x+y)+ ~(x+ ~((x+y)+z))= ~x. 7802,7801 [para_into,6195.1.1.1.1,670.1.1,demod,6200,7706] ~x+ ~((x+y)+z)= ~x. 7810,7809 [para_into,6195.1.1.1.1,576.1.1,demod,6200,flip.1] ~(x+y)+ ~(x+ ~(z+ (x+y)))= ~x+ ~(z+ (x+y)). 7829 [back_demod,3426,demod,7810,150] x+ ~(y+ (~x+z))=x. 8334 [para_into,7829.1.1.2.1.2,721.1.1] x+ ~(y+ (z+ ~x))=x. 8465,8464 [para_into,8334.1.1.2.1.2.2,149.1.1] ~x+ ~(y+ (z+x))= ~x. 10337 [para_into,6213.1.1.2.1,2452.1.1] x+ ~(~(y+x)+ (z+y))=x. 11348,11347 [para_from,6383.1.1,985.1.1.1.1.1.1,demod,7802,150,flip.1] (x+y)+ (y+z)=x+ (y+z). 14662 [para_from,10337.1.1,1017.1.1.2.1.1.1,demod,150,11348,8465,150,150,11348] (x+y)+z=x+ (y+z). 14664 [binary,14662.1,701.1] $Ans(Robbins_basis). ------------ end of proof -------------