----- Otter 3.1-b0, May 2000 ----- ----> UNIT CONFLICT at 20.93 sec ----> 16083 [binary,16081.1,1012.1] $Ans(Robbins_basis). Length of proof is 104. Level of proof is 38. ---------------- 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)+ ~(~(x+z)+ ~(~y+ ~(y+u))))=y. 5 [para_into,3.1.1.1.2.1.1,3.1.1] ~(~(~(x+y)+z)+ ~(y+ ~(~z+ ~(z+u))))=z. 7 [para_into,3.1.1.1.2.1.2.1.2,3.1.1] ~(~(x+ ~(y+z))+ ~(~(x+u)+ ~(~ ~(y+z)+z)))= ~(y+z). 9 [para_into,5.1.1.1.1.1.1,5.1.1] ~(~(x+y)+ ~(~(z+ ~(~x+ ~(x+u)))+ ~(~y+ ~(y+v))))=y. 11 [para_into,5.1.1.1.2.1.2.1.2,3.1.1] ~(~(~(x+y)+ ~(z+u))+ ~(y+ ~(~ ~(z+u)+u)))= ~(z+u). 15 [para_from,5.1.1,3.1.1.1.2] ~(~(~(x+ ~ ~y)+ ~y)+y)= ~y. 22,21 [para_into,15.1.1.1.1,15.1.1] ~(~ ~x+x)= ~x. 24,23 [para_from,15.1.1,5.1.1.1.1] ~(~x+ ~(~x+ ~(~x+ ~(x+y))))=x. 83 [para_into,23.1.1.1.2.1.2.1.2,23.1.1,demod,22] ~(~ ~x+ ~(~ ~x+ ~x))= ~x. 95 [para_from,23.1.1,7.1.1.1.2.1.2.1.1.1,demod,24,24,24] ~(~(x+y)+ ~(~(x+z)+y))=y. 105 [para_into,9.1.1.1.2.1.1,21.1.1] ~(~(x+y)+ ~(~ ~(~x+ ~(x+z))+ ~(~y+ ~(y+u))))=y. 112,111 [para_into,83.1.1.1.1.1,23.1.1,demod,24,24,24] ~(~x+ ~(~x+x))=x. 126,125 [para_from,111.1.1,21.1.1.1.1.1,demod,112] ~(~x+ (~x+ ~(~x+x)))=x. 151 [para_into,11.1.1.1.1.1.2,125.1.1,demod,126,126,126] ~(~(~(x+y)+z)+ ~(y+z))=z. 157 [para_into,95.1.1.1.1,111.1.1] ~(x+ ~(~(~x+y)+ ~(~x+x)))= ~(~x+x). 159 [para_into,95.1.1.1.1,95.1.1] ~(x+ ~(~(~(y+x)+z)+ ~(~(y+u)+x)))= ~(~(y+u)+x). 168,167 [para_into,95.1.1.1.2.1.1,125.1.1] ~(~(~x+y)+ ~(x+y))=y. 171 [para_into,95.1.1.1.2,95.1.1] ~(~(x+ ~(~(x+y)+z))+z)= ~(~(x+y)+z). 217 [para_into,167.1.1.1.1,167.1.1] ~(x+ ~((~y+x)+ ~(y+x)))= ~(y+x). 238,237 [para_into,167.1.1.1.2,21.1.1] ~(~(~ ~ ~x+x)+ ~x)=x. 247 [para_from,167.1.1,9.1.1.1.2] ~(~(x+ ~x)+ ~(~x+ ~(x+y)))= ~x. 260,259 [para_from,167.1.1,7.1.1.1.2,demod,22] ~(~ ~(x+y)+y)= ~(x+y). 261 [para_from,167.1.1,7.1.1.1.1,demod,260] ~(x+ ~(~(~(~y+x)+z)+ ~(y+x)))= ~(y+x). 272,271 [para_from,167.1.1,3.1.1.1.2,demod,22] ~(~x+ ~(x+y))=x. 279 [para_from,167.1.1,5.1.1.1.1.1.1,demod,272] ~(~(x+y)+ ~(~(z+x)+y))=y. 285 [back_demod,247,demod,272] ~(~(x+ ~x)+x)= ~x. 290,289 [back_demod,105,demod,272,272] ~(~(x+y)+ ~(~x+y))=y. 295 [back_demod,2,demod,290,unit_del,1] B+A!=A+B| (A+B)+C!=A+ (B+C)|$Ans(Robbins_basis). 364 [para_from,285.1.1,95.1.1.1.2] ~(~(x+x)+ ~x)=x. 392 [para_into,364.1.1.1.2,271.1.1] ~(~((~x+ ~(x+y))+ (~x+ ~(x+y)))+x)= ~x+ ~(x+y). 396 [para_into,364.1.1.1.2,21.1.1] ~(~((~ ~x+x)+ (~ ~x+x))+ ~x)= ~ ~x+x. 400 [para_from,364.1.1,15.1.1.1.1.1.1] ~(~(~x+ ~x)+x)= ~x. 463,462 [para_from,400.1.1,95.1.1.1.2] ~(~(~x+x)+ ~x)=x. 607,606 [para_into,259.1.1.1.1.1,462.1.1,demod,463] ~(~x+ ~x)=x. 609,608 [para_into,259.1.1.1.1.1,400.1.1,demod,22,607,flip.1] ~(x+x)= ~x. 611,610 [para_into,259.1.1.1.1.1,237.1.1,demod,609,238] ~ ~x=x. 612 [para_into,259.1.1.1.1.1,167.1.1,demod,168] ~(~x+ ~(y+x))=x. 671,670 [back_demod,396,demod,611,611,609,609,609,611,611,flip.1] x+x=x. 675,674 [back_demod,392,demod,671,272,671,flip.1] ~x+ ~(x+y)= ~x. 728 [para_into,610.1.1.1,167.1.1,flip.1] ~(~x+y)+ ~(x+y)= ~y. 730 [para_into,610.1.1.1,95.1.1,flip.1] ~(x+y)+ ~(~(x+z)+y)= ~y. 736 [para_from,151.1.1,610.1.1.1,flip.1] ~(~(x+y)+z)+ ~(y+z)= ~z. 743,742 [para_from,612.1.1,610.1.1.1,flip.1] ~x+ ~(y+x)= ~x. 745,744 [para_into,674.1.1.1,610.1.1,demod,611] x+ ~(~x+y)=x. 750 [para_into,157.1.1.1.2.1.1.1,674.1.1,demod,611,745,flip.1] ~(~x+x)= ~(x+ ~x). 759,758 [para_into,742.1.1.1,610.1.1,demod,611] x+ ~(y+ ~x)=x. 762 [para_into,742.1.1.2.1,742.1.1,demod,611,611,611] (x+y)+y=x+y. 764 [para_into,742.1.1.2.1,674.1.1,demod,611,611,611] (x+y)+x=x+y. 780 [para_from,159.1.1,610.1.1.1,demod,611,flip.1] x+ ~(~(~(y+x)+z)+ ~(~(y+u)+x))= ~(y+u)+x. 789,788 [para_from,750.1.1,610.1.1.1,demod,611,flip.1] ~x+x=x+ ~x. 796 [para_into,171.1.1.1.1.1,758.1.1,demod,671,611,flip.1] ~(~(x+y)+ ~x)=x. 800 [para_from,171.1.1,610.1.1.1,demod,611,flip.1] ~(x+ ~(~(x+y)+z))+z= ~(x+y)+z. 814 [para_from,796.1.1,610.1.1.1,flip.1] ~(x+y)+ ~x= ~x. 820 [para_into,814.1.1.2,610.1.1,demod,611] ~(~x+y)+x=x. 843,842 [para_into,217.1.1.1.2.1.1,758.1.1,demod,611,611,675,611,611] ~(~(x+y)+y)= ~(y+ ~(x+y)). 845,844 [para_into,217.1.1.1.2.1.1,744.1.1,demod,611,611,675,611,611] ~(~(x+y)+x)= ~(x+ ~(x+y)). 868 [para_from,217.1.1,820.1.1.1] ~(x+ ~y)+y=y. 876 [para_from,217.1.1,610.1.1.1,demod,611,flip.1] x+ ~((~y+x)+ ~(y+x))=y+x. 914 [para_from,289.1.1,610.1.1.1,flip.1] ~(x+y)+ ~(~x+y)= ~y. 917,916 [para_into,728.1.1.1.1,758.1.1,demod,611,611,611,611] x+ ~(x+ ~(y+x))=y+x. 936 [para_into,914.1.1.1.1,764.1.1,demod,845] ~(x+y)+ ~(x+ ~(x+y))= ~x. 954 [para_into,261.1.1.1.2.1.1.1,820.1.1,demod,675,611] ~(x+y)= ~(y+x). 977 [para_from,261.1.1,610.1.1.1,demod,611,flip.1] x+ ~(~(~(~y+x)+z)+ ~(y+x))=y+x. 990 [para_from,954.1.1,610.1.1.1,demod,611] x+y=y+x. 997 [para_from,954.1.1,744.1.1.2.1.1] (x+y)+ ~(~(y+x)+z)=x+y. 1007 [para_from,954.1.1,728.1.1.2] ~(~x+y)+ ~(y+x)= ~y. 1012 [para_from,990.1.1,295.1.1,unit_del,1] (A+B)+C!=A+ (B+C)|$Ans(Robbins_basis). 1100 [para_from,279.1.1,610.1.1.1,flip.1] ~(x+y)+ ~(~(z+x)+y)= ~y. 1258 [para_into,730.1.1.1.1,1007.1.1,demod,611,611] x+ ~(~(~(~y+x)+z)+ ~(x+y))=x+y. 1411 [para_from,936.1.1,736.1.1.1.1,demod,611,611] x+ ~(y+ ~(x+ ~(x+y)))=x+ ~(x+y). 1550,1549 [para_into,780.1.1.2.1.2.1.1.1,990.1.1] x+ ~(~(~(y+x)+z)+ ~(~(u+y)+x))= ~(y+u)+x. 1551 [para_into,780.1.1.2.1.2.1.1.1,916.1.1,demod,1550,917] ~(x+y)+z= ~(y+x)+z. 1572 [para_into,1551.1.1,990.1.1] x+ ~(y+z)= ~(z+y)+x. 1578 [copy,1572,flip.1] ~(x+y)+z=z+ ~(y+x). 1908 [para_into,1572.1.1,736.1.1,flip.1] ~(x+y)+ ~(~(z+y)+x)= ~x. 2013 [para_into,1578.1.1,736.1.1,flip.1] ~(x+y)+ ~(y+ ~(z+x))= ~y. 2384 [para_from,1100.1.1,800.1.1.1.1,demod,611,671,845,flip.1] ~(x+ ~(x+y))+y=y. 2428 [para_into,2384.1.1.1.1.2.1,800.1.1,demod,843] ~(~(~(x+y)+z)+ ~(x+ ~(~(x+y)+z)))+z=z. 2432 [para_into,2384.1.1.1.1.2.1,762.1.1] ~((x+y)+ ~(x+y))+y=y. 2455,2454 [para_into,2384.1.1,1578.1.1,demod,845] x+ ~(y+ ~(y+x))=x. 2484 [back_demod,1411,demod,2455,flip.1] x+ ~(x+y)=x+ ~y. 2643,2642 [para_into,2484.1.1.2.1,990.1.1] x+ ~(y+x)=x+ ~y. 2653,2652 [para_into,2484.1.1.2.1,764.1.1] (x+y)+ ~(x+y)= (x+y)+ ~x. 2687 [back_demod,2428,demod,2643] ~(~(~(x+y)+z)+ ~x)+z=z. 2701 [back_demod,2432,demod,2653] ~((x+y)+ ~x)+y=y. 2831 [para_into,876.1.1.2.1.1,868.1.1,demod,2643,759,flip.1] (x+ ~y)+y=y+ ~y. 2838,2837 [para_into,876.1.1.2.1.1,814.1.1,demod,2643,675,611,789,flip.1] (x+y)+ ~x=x+ ~x. 2893,2892 [back_demod,2701,demod,2838] ~(x+ ~x)+y=y. 3356 [para_from,2831.1.1,780.1.1.2.1.1.1.1.1,demod,2893] x+ ~(~y+ ~(~((z+ ~x)+u)+x))= ~((z+ ~x)+u)+x. 3361,3360 [para_from,2831.1.1,730.1.1.1.1,demod,2893] ~(~((x+ ~y)+z)+y)= ~y. 3362 [back_demod,3356,demod,3361,759,flip.1] ~((x+ ~y)+z)+y=y. 3388 [para_from,2837.1.1,780.1.1.2.1.1.1.1.1,demod,2893] ~x+ ~(~y+ ~(~((x+z)+u)+ ~x))= ~((x+z)+u)+ ~x. 3393,3392 [para_from,2837.1.1,730.1.1.1.1,demod,2893,611] ~(~((x+y)+z)+ ~x)=x. 3394 [back_demod,3388,demod,3393,743,flip.1] ~((x+y)+z)+ ~x= ~x. 3524 [para_into,3362.1.1,1578.1.1] x+ ~(y+ (z+ ~x))=x. 3528 [para_into,3362.1.1,990.1.1] x+ ~((y+ ~x)+z)=x. 3735,3734 [para_into,3524.1.1.2.1.2.2,610.1.1] ~x+ ~(y+ (z+x))= ~x. 3787,3786 [para_into,3528.1.1.2.1.1.2,610.1.1] ~x+ ~((y+x)+z)= ~x. 4030 [para_from,3394.1.1,997.1.1.2.1,demod,611] (x+ (y+z))+y=x+ (y+z). 14866 [para_into,2687.1.1.1.1.1.1.1.1,2013.1.1,demod,611,611] ~(~(x+y)+ (z+x))+y=y. 14870 [para_into,2687.1.1.1.1.1.1.1.1,1908.1.1,demod,611,611] ~(~(x+y)+ (x+z))+y=y. 15349,15348 [para_from,14866.1.1,1258.1.1.2.1.1.1,demod,3735,611,flip.1] (x+y)+ (y+z)= (x+y)+z. 15727,15726 [para_from,14870.1.1,1258.1.1.2.1.1.1,demod,3735,611,flip.1] (x+y)+ (x+z)= (x+y)+z. 15728 [para_from,14870.1.1,977.1.1.2.1.1.1,demod,15727,3787,611,15727] (x+y)+z= (x+z)+y. 16081 [para_into,15728.1.1,4030.1.1,demod,15349,flip.1] (x+y)+z=x+ (y+z). 16083 [binary,16081.1,1012.1] $Ans(Robbins_basis). ------------ end of proof -------------