----- Otter 3.1-b0, May 2000 ----- ----> UNIT CONFLICT at 90.09 sec ----> 30901 [binary,30899.1,1375.1] $Ans(Robbins_basis). Length of proof is 174. Level of proof is 48. ---------------- 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)+ ~(~(x+z)+ ~(y+ ~(~y+u)))=y. 6,5 [para_into,3.1.1.2.1.1.1,3.1.1] ~(~(x+ ~y)+ ~z)+ ~(~y+ ~(z+ ~(~z+u)))=z. 7 [para_into,3.1.1.2.1.2.1.2.1,3.1.1] ~(x+ ~(y+ ~z))+ ~(~(x+u)+ ~((y+ ~z)+ ~z))=y+ ~z. 9 [para_into,3.1.1.2.1,3.1.1] ~(x+ ~ ~(x+y))+ ~ ~ ~(x+y)= ~(x+y). 13 [para_into,9.1.1.1.1.2.1.1,3.1.1,demod,4,4] ~(~(x+ ~y)+ ~ ~y)+ ~ ~ ~y= ~y. 20,19 [para_into,13.1.1.1.1,13.1.1] ~ ~x+ ~ ~ ~ ~x= ~ ~x. 21 [para_from,19.1.1,3.1.1.2.1.2.1.2.1] ~(x+ ~ ~y)+ ~(~(x+z)+ ~(~y+ ~ ~ ~y))= ~y. 23 [para_from,19.1.1,3.1.1.2.1.1.1] ~(~ ~x+ ~y)+ ~(~ ~ ~x+ ~(y+ ~(~y+z)))=y. 25 [para_into,5.1.1.1.1,13.1.1] ~ ~x+ ~(~ ~x+ ~(~ ~x+ ~(~ ~ ~x+y)))= ~ ~x. 27 [para_into,5.1.1.2.1.2.1.2.1,19.1.1] ~(~(x+ ~y)+ ~ ~z)+ ~(~y+ ~(~z+ ~ ~ ~z))= ~z. 31 [para_into,5.1.1.2.1,5.1.1] ~(~(x+ ~(~(y+ ~z)+ ~ ~ ~z))+ ~ ~z)+ ~ ~ ~z= ~z. 39 [para_into,21.1.1.2.1.2.1,19.1.1] ~(x+ ~ ~ ~y)+ ~(~(x+z)+ ~ ~ ~y)= ~ ~y. 45 [para_into,39.1.1.2.1.1.1,19.1.1] ~(~ ~x+ ~ ~ ~y)+ ~(~ ~ ~x+ ~ ~ ~y)= ~ ~y. 49 [para_into,39.1.1.2.1.1.1,3.1.1] ~(~(x+ ~y)+ ~ ~ ~z)+ ~(~y+ ~ ~ ~z)= ~ ~z. 52,51 [para_into,39.1.1.2.1,13.1.1] ~(~(x+ ~y)+ ~ ~ ~y)+ ~ ~y= ~ ~y. 55 [para_into,51.1.1.1.1.1.1,51.1.1] ~(~ ~ ~x+ ~ ~ ~ ~x)+ ~ ~ ~x= ~ ~ ~x. 63 [para_from,51.1.1,13.1.1.1.1.1.1] ~(~ ~ ~x+ ~ ~ ~x)+ ~ ~ ~ ~x= ~ ~x. 65 [para_from,51.1.1,5.1.1.1.1.1.1] ~(~ ~ ~x+ ~y)+ ~(~ ~x+ ~(y+ ~(~y+z)))=y. 67 [para_into,7.1.1.1.1.2.1,51.1.1,demod,52,52] ~(x+ ~ ~ ~y)+ ~(~(x+z)+ ~(~ ~y+ ~ ~y))= ~ ~y. 70,69 [para_into,7.1.1.1.1.2.1,5.1.1,demod,6,6] ~(x+ ~y)+ ~(~(x+z)+ ~(y+ ~(~u+ ~(y+ ~(~y+v)))))=y. 101 [para_into,49.1.1.2.1,63.1.1] ~(~(x+ ~(~ ~ ~y+ ~ ~ ~y))+ ~ ~ ~ ~y)+ ~ ~ ~y= ~ ~ ~y. 117 [para_into,27.1.1.1.1,51.1.1] ~ ~ ~x+ ~(~ ~ ~x+ ~(~x+ ~ ~ ~x))= ~x. 125 [para_from,117.1.1,25.1.1.2.1.2.1.2.1] ~ ~x+ ~(~ ~x+ ~(~ ~x+ ~ ~x))= ~ ~x. 127 [para_from,117.1.1,23.1.1.2.1.2.1.2.1] ~(~ ~x+ ~ ~ ~y)+ ~(~ ~ ~x+ ~(~ ~y+ ~ ~y))= ~ ~y. 131 [para_from,117.1.1,5.1.1.2.1.2.1.2.1] ~(~(x+ ~y)+ ~ ~ ~z)+ ~(~y+ ~(~ ~z+ ~ ~z))= ~ ~z. 135 [para_into,65.1.1.2.1.2.1.2.1,117.1.1] ~(~ ~ ~x+ ~ ~ ~y)+ ~(~ ~x+ ~(~ ~y+ ~ ~y))= ~ ~y. 138,137 [para_into,31.1.1.1.1.1.1,49.1.1] ~(~ ~ ~x+ ~ ~x)+ ~ ~ ~x= ~x. 154,153 [para_into,67.1.1.2.1,45.1.1,demod,20] ~ ~ ~x+ ~ ~ ~x= ~ ~ ~x. 157 [back_demod,101,demod,154] ~(~(x+ ~ ~ ~ ~y)+ ~ ~ ~ ~y)+ ~ ~ ~y= ~ ~ ~y. 162,161 [back_demod,63,demod,154,154] ~ ~ ~ ~x= ~ ~x. 165 [back_demod,157,demod,162,162] ~(~(x+ ~ ~y)+ ~ ~y)+ ~ ~ ~y= ~ ~ ~y. 174,173 [back_demod,55,demod,162,138,flip.1] ~ ~ ~x= ~x. 178,177 [back_demod,153,demod,174,174,174] ~x+ ~x= ~x. 181 [back_demod,135,demod,174,174,178,174] ~(~x+ ~y)+ ~(~ ~x+ ~y)= ~ ~y. 183 [back_demod,131,demod,174,178,174] ~(~(x+ ~y)+ ~z)+ ~(~y+ ~z)= ~ ~z. 185 [back_demod,127,demod,174,174,178,174] ~(~ ~x+ ~y)+ ~(~x+ ~y)= ~ ~y. 187 [back_demod,125,demod,178,174] ~ ~x+ ~(~ ~x+ ~x)= ~ ~x. 189 [back_demod,67,demod,174,178,174] ~(x+ ~y)+ ~(~(x+z)+ ~y)= ~ ~y. 195 [back_demod,165,demod,174,174] ~(~(x+ ~ ~y)+ ~ ~y)+ ~y= ~y. 201 [back_demod,137,demod,174,174] ~(~x+ ~ ~x)+ ~x= ~x. 205 [back_demod,117,demod,174,174,174,178] ~x+ ~(~x+ ~ ~x)= ~x. 265 [para_from,177.1.1,69.1.1.1.1] ~ ~x+ ~(~(~x+y)+ ~(x+ ~(~z+ ~(x+ ~(~x+u)))))=x. 275 [para_from,201.1.1,3.1.1.2.1] ~(~(x+ ~(~x+y))+ ~x)+ ~ ~(x+ ~(~x+y))=x. 287 [para_from,187.1.1,69.1.1.2.1.1.1,demod,174] ~(~ ~x+ ~y)+ ~(~x+ ~(y+ ~(~z+ ~(y+ ~(~y+u)))))=y. 321 [para_into,181.1.1.1.1,187.1.1,demod,174,174] ~x+ ~(~x+ ~(~ ~x+ ~x))= ~ ~(~ ~x+ ~x). 325 [para_into,181.1.1.2.1,205.1.1,demod,174,174,174] ~(~x+ ~(~ ~x+ ~x))+ ~x= ~ ~(~ ~x+ ~x). 329 [para_from,181.1.1,69.1.1.2.1,demod,174,178,174,174] ~ ~x+ ~(~y+ ~(~ ~x+ ~(~x+z)))= ~ ~x. 340,339 [para_from,181.1.1,3.1.1.2.1,demod,174,178,174,174] ~ ~x+ ~(~x+y)= ~ ~x. 345 [back_demod,329,demod,340,174] ~ ~x+ ~(~y+ ~x)= ~ ~x. 356,355 [para_into,339.1.1.1,173.1.1,demod,174] ~x+ ~(~ ~x+y)= ~x. 367 [para_into,339.1.1.2.1,69.1.1] ~ ~(x+ ~y)+ ~y= ~ ~(x+ ~y). 370,369 [back_demod,325,demod,356,flip.1] ~ ~(~ ~x+ ~x)= ~ ~x+ ~x. 371 [back_demod,321,demod,356,370,flip.1] ~ ~x+ ~x= ~x+ ~ ~x. 421 [para_into,183.1.1.2.1,339.1.1,demod,174] ~(~(x+ ~ ~y)+ ~(~y+z))+ ~y= ~ ~(~y+z). 429 [para_from,183.1.1,181.1.1.1.1,demod,174] ~x+ ~(~ ~(~(y+ ~z)+ ~x)+ ~(~z+ ~x))= ~ ~(~z+ ~x). 443 [para_into,345.1.1.1,173.1.1,demod,174] ~x+ ~(~y+ ~ ~x)= ~x. 451 [para_from,345.1.1,183.1.1.2.1,demod,174] ~(~(x+ ~ ~y)+ ~(~z+ ~y))+ ~y= ~ ~(~z+ ~y). 459 [para_from,443.1.1,183.1.1.2.1] ~(~(x+ ~y)+ ~(~z+ ~ ~y))+ ~ ~y= ~ ~(~z+ ~ ~y). 505 [para_from,185.1.1,183.1.1.2.1,demod,174] ~(~(x+ ~(~ ~y+ ~z))+ ~(~y+ ~z))+ ~z= ~ ~(~y+ ~z). 507 [para_from,185.1.1,181.1.1.1.1,demod,174] ~x+ ~(~ ~(~ ~y+ ~x)+ ~(~y+ ~x))= ~ ~(~y+ ~x). 516,515 [para_into,367.1.1.1.1.1,69.1.1,demod,70] ~ ~x+ ~(~(y+z)+ ~(x+ ~(~u+ ~(x+ ~(~x+v)))))= ~ ~x. 522,521 [back_demod,265,demod,516] ~ ~x=x. 553 [back_demod,507,demod,522,522,522] ~x+ ~((y+ ~x)+ ~(~y+ ~x))= ~y+ ~x. 555 [back_demod,505,demod,522,522] ~(~(x+ ~(y+ ~z))+ ~(~y+ ~z))+ ~z= ~y+ ~z. 601 [back_demod,459,demod,522,522,522,522] ~(~(x+ ~y)+ ~(~z+y))+y= ~z+y. 609 [back_demod,451,demod,522,522] ~(~(x+y)+ ~(~z+ ~y))+ ~y= ~z+ ~y. 625 [back_demod,429,demod,522,522] ~x+ ~((~(y+ ~z)+ ~x)+ ~(~z+ ~x))= ~z+ ~x. 631 [back_demod,421,demod,522,522] ~(~(x+y)+ ~(~y+z))+ ~y= ~y+z. 672,671 [back_demod,371,demod,522,522,flip.1] ~x+x=x+ ~x. 676,675 [back_demod,355,demod,522] ~x+ ~(x+y)= ~x. 678,677 [back_demod,345,demod,522,522] x+ ~(~y+ ~x)=x. 680,679 [back_demod,339,demod,522,522] x+ ~(~x+y)=x. 687 [back_demod,287,demod,522,680,678] ~(x+ ~y)+ ~(~x+ ~y)=y. 690,689 [back_demod,275,demod,680,178,522,680,522] x+x=x. 715 [back_demod,195,demod,522,522] ~(~(x+y)+y)+ ~y= ~y. 719 [back_demod,189,demod,522] ~(x+ ~y)+ ~(~(x+z)+ ~y)=y. 763 [para_into,553.1.1.1,521.1.1,demod,522,522,522] x+ ~((y+x)+ ~(~y+x))= ~y+x. 765 [para_into,555.1.1.1.1.1.1.2.1.2,521.1.1,demod,522,522,522] ~(~(x+ ~(y+z))+ ~(~y+z))+z= ~y+z. 780,779 [para_into,677.1.1.2.1.1,521.1.1] x+ ~(y+ ~x)=x. 782,781 [para_into,677.1.1.2.1,679.1.1,demod,522,522,522] (x+y)+x=x+y. 790,789 [para_into,779.1.1.2.1.2,521.1.1] ~x+ ~(y+x)= ~x. 837 [para_into,715.1.1.1.1.1.1,781.1.1] ~(~(x+y)+x)+ ~x= ~x. 848,847 [para_into,687.1.1.1.1.2,521.1.1,demod,522] ~(x+y)+ ~(~x+y)= ~y. 850,849 [para_into,687.1.1.1.1,789.1.1,demod,522,522] x+ ~(x+ ~(y+x))=y+x. 853 [para_into,687.1.1.1.1,675.1.1,demod,522,522] x+ ~(x+ ~(x+y))=x+y. 863 [back_demod,2,demod,848,522,unit_del,1] B+A!=A+B| (A+B)+C!=A+ (B+C)|$Ans(Robbins_basis). 870 [para_into,847.1.1.2.1.1,521.1.1] ~(~x+y)+ ~(x+y)= ~y. 879,878 [para_from,849.1.1,847.1.1.1.1,demod,676,522,522] ~(x+y)+y=y+ ~(x+y). 880 [para_from,849.1.1,837.1.1.1.1.1.1,demod,879] ~(x+ ~(y+x))+ ~x= ~x. 912 [para_into,601.1.1.1.1.2.1.1,521.1.1,demod,522] ~(~(x+ ~y)+ ~(z+y))+y=z+y. 919,918 [para_from,853.1.1,847.1.1.1.1,demod,676,522,522] ~(x+y)+x=x+ ~(x+y). 938 [para_into,880.1.1.1.1.2.1,878.1.1,demod,850] ~(x+y)+ ~y= ~y. 944 [para_into,938.1.1.1.1,870.1.1,demod,522,522,522] x+ (y+x)=y+x. 946 [para_into,938.1.1.1.1,781.1.1] ~(x+y)+ ~x= ~x. 960 [para_into,609.1.1.1.1.2.1.1,521.1.1,demod,522] ~(~(x+y)+ ~(z+ ~y))+ ~y=z+ ~y. 982 [para_into,625.1.1.2.1.2.1,679.1.1,demod,522,522,522,522,676] ~(x+y)+ ~((~(z+ ~x)+ ~(x+y))+x)= ~x. 1016 [para_into,719.1.1.1.1.2,521.1.1,demod,522] ~(x+y)+ ~(~(x+z)+y)= ~y. 1074 [para_into,1016.1.1.2.1.1.1,1016.1.1,demod,522] ~(~(x+y)+z)+ ~(y+z)= ~z. 1078 [para_into,1016.1.1.2.1.1.1,946.1.1,demod,522] ~(~(x+y)+z)+ ~(x+z)= ~z. 1080 [para_into,1016.1.1.2.1.1.1,944.1.1] ~(x+y)+ ~(~(z+x)+y)= ~y. 1100 [para_into,631.1.1.1.1,789.1.1,demod,522] (x+y)+ ~y= ~y+ (x+y). 1118 [para_into,1100.1.1.1,781.1.1,demod,782] (x+y)+ ~x= ~x+ (x+y). 1120,1119 [para_into,1100.1.1.1,779.1.1,demod,522,522,780,flip.1] (x+ ~y)+y=y+ (x+ ~y). 1122,1121 [para_into,1100.1.1.1,679.1.1,demod,522,522,680,flip.1] (~x+y)+x=x+ (~x+y). 1123 [para_into,1100.1.1.1,675.1.1,demod,522,522,676] ~x+ (x+y)= (x+y)+ ~x. 1184 [para_into,1123.1.1.2,1118.1.1] ~(x+y)+ (~x+ (x+y))= ((x+y)+ ~x)+ ~(x+y). 1254 [para_from,1074.1.1,1016.1.1.2.1,demod,522,522] ~(~(x+y)+ ~(y+z))+z=y+z. 1268 [para_into,1078.1.1.1.1,1074.1.1,demod,522,522] x+ ~(~(y+z)+ ~(z+x))=z+x. 1274 [para_into,1078.1.1.1.1,870.1.1,demod,522,676,522,522] x+y=y+x. 1339 [para_from,1274.1.1,1074.1.1.1.1] ~(x+ ~(y+z))+ ~(z+x)= ~x. 1341 [para_from,1274.1.1,1016.1.1.2.1] ~(x+y)+ ~(y+ ~(x+z))= ~y. 1353 [para_from,1274.1.1,1074.1.1.2.1] ~(~(x+y)+z)+ ~(z+y)= ~z. 1357 [para_from,1274.1.1,870.1.1.1.1] ~(x+ ~y)+ ~(y+x)= ~x. 1359 [para_from,1274.1.1,847.1.1.2.1] ~(x+y)+ ~(y+ ~x)= ~y. 1361 [para_from,1274.1.1,1016.1.1.1.1] ~(x+y)+ ~(~(y+z)+x)= ~x. 1369 [para_from,1274.1.1,847.1.1.1.1] ~(x+y)+ ~(~y+x)= ~x. 1371 [para_from,1274.1.1,1078.1.1.2.1] ~(~(x+y)+z)+ ~(z+x)= ~z. 1375 [para_from,1274.1.1,863.1.1,unit_del,1] (A+B)+C!=A+ (B+C)|$Ans(Robbins_basis). 1407 [para_into,765.1.1.1.1.2.1,1274.1.1] ~(~(x+ ~(y+z))+ ~(z+ ~y))+z= ~y+z. 1441 [para_into,1357.1.1.2.1,1357.1.1,demod,522,522,522] ~(~(x+y)+ (y+ ~x))+y=x+y. 1484,1483 [para_into,1359.1.1.1.1,1357.1.1,demod,522,522,522] x+ ~(~(y+x)+ (x+ ~y))=y+x. 1497 [para_into,1359.1.1.1.1,763.1.1,demod,522] ~(~x+y)+ ~(~((x+y)+ ~(~x+y))+ ~y)= (x+y)+ ~(~x+y). 1759 [para_into,1080.1.1.2.1,1274.1.1] ~(x+y)+ ~(y+ ~(z+x))= ~y. 1765 [para_from,1080.1.1,1078.1.1.1.1,demod,522,522] x+ ~(y+ ~(~(z+y)+x))= ~(z+y)+x. 1935 [para_into,1339.1.1.2.1,1274.1.1] ~(x+ ~(y+z))+ ~(x+z)= ~x. 2054,2053 [para_into,1341.1.1.1.1,779.1.1,demod,522] ~x+ ~(~(y+ ~x)+ ~(x+z))=y+ ~x. 2199 [para_into,1361.1.1.2.1,1353.1.1,demod,522,522] ~(~(x+y)+ ~(z+y))+x=x+y. 2220,2219 [para_from,1361.1.1,1341.1.1.2.1,demod,522,522] ~(~(x+y)+ ~(z+x))+z=z+x. 2263 [para_into,1371.1.1.1.1,1371.1.1,demod,522,522] x+ ~(~(x+y)+ ~(y+z))=x+y. 3259 [para_from,1441.1.1,1369.1.1.1.1,demod,522] ~(x+y)+ ~(~y+ ~(~(x+y)+ (y+ ~x)))= ~(x+y)+ (y+ ~x). 3705 [para_from,1483.1.1,1254.1.1.1.1.2.1,demod,1484] ~(~(x+y)+ ~(z+y))+ ~(~(z+y)+ (y+ ~z))=z+y. 5049 [para_from,982.1.1,912.1.1.1.1,demod,522,690,flip.1] (~(x+ ~y)+ ~(y+ ~y))+y=y. 5063 [para_into,5049.1.1.1.1.1,2199.1.1] (~(~x+y)+ ~(x+ ~x))+x=x. 5096,5095 [para_from,5049.1.1,946.1.1.1.1,demod,2054,flip.1] ~(~(x+ ~y)+ ~(y+ ~y))=x+ ~y. 5123 [para_from,5063.1.1,765.1.1.1.1.1.1.2.1,demod,2220,5096,1120,2220] x+ (y+ ~x)=x+ ~x. 5150,5149 [para_into,5123.1.1.2.2,521.1.1,demod,522,672] ~x+ (y+x)=x+ ~x. 5154,5153 [para_into,5123.1.1.2,2199.1.1] x+ (~x+y)=x+ ~x. 5158,5157 [para_into,5123.1.1.2,1935.1.1,flip.1] (x+y)+ ~(x+y)= (x+y)+ ~x. 5170 [para_into,5123.1.1.2,1268.1.1,demod,5158,522,1122,5154,5158] (~(x+y)+ ~(y+z))+ (y+z)= (x+y)+ ~x. 5180 [para_into,5123.1.1.2,779.1.1,demod,5158] (x+ ~y)+y= (x+ ~y)+ ~x. 5186,5185 [para_into,5123.1.1,1274.1.1] (x+ ~y)+y=y+ ~y. 5187 [back_demod,1184,demod,5150,5158,flip.1] ((x+y)+ ~x)+ ~(x+y)= (x+y)+ ~x. 5206,5205 [copy,5180,flip.1,demod,5186] (x+ ~y)+ ~x=y+ ~y. 5213 [back_demod,5170,demod,5186,5158] (x+y)+ ~x= (z+x)+ ~z. 5217,5216 [back_demod,5187,demod,5206,flip.1] (x+y)+ ~x=x+ ~x. 5220 [copy,5213,flip.1,demod,5217,5217] x+ ~x=y+ ~y. 5371 [para_from,5123.1.1,1078.1.1.2.1] ~(~(x+y)+ (z+ ~x))+ ~(x+ ~x)= ~(z+ ~x). 5424,5423 [para_from,5220.1.1,1339.1.1.2.1,demod,790,522,522] x+ ~(y+ ~y)=x. 5453,5452 [back_demod,5371,demod,5424] ~(~(x+y)+ (z+ ~x))= ~(z+ ~x). 5494,5493 [back_demod,3705,demod,5453] ~(~(x+y)+ ~(z+y))+ ~(y+ ~z)=z+y. 5499 [back_demod,3259,demod,5453,676,522,879,flip.1] ~(x+y)+ (y+ ~x)=y+ ~(x+y). 5666,5665 [para_from,5149.1.1,1371.1.1.2.1,demod,5424,522] ~(~((x+y)+z)+ ~y)=y. 5695 [back_demod,1497,demod,5666,879,flip.1] (x+y)+ ~(~x+y)=y+ ~(~x+y). 5993 [para_from,5665.1.1,1268.1.1.2.1.2,demod,790,flip.1] ~((x+y)+z)+ ~y= ~y. 6419 [para_into,5993.1.1.1.1.1,960.1.1,demod,522,522] ~((x+ ~y)+z)+y=y. 6426,6425 [para_into,5993.1.1.1.1.1,779.1.1,demod,522,522] ~(x+y)+ (z+ ~x)=z+ ~x. 6434,6433 [back_demod,5499,demod,6426,flip.1] x+ ~(y+x)=x+ ~y. 6438,6437 [back_demod,5695,demod,6434,522] (x+y)+ ~(~x+y)=y+x. 6459 [para_from,5993.1.1,765.1.1.1.1.1.1,demod,522,6438,919] x+ ~(x+y)= ~y+x. 6564,6563 [para_from,6419.1.1,765.1.1.1.1.1.1,demod,522,6438] ~(x+y)+x= ~y+x. 6634,6633 [para_into,6433.1.1.2.1,1935.1.1,demod,522,6564,522,flip.1] ~(x+y)+ (x+ ~(z+y))= ~y+x. 6637 [para_into,6433.1.1.2.1,1759.1.1,demod,522,6564,522,522,flip.1] ~(x+ ~(y+z))+ (z+x)= (y+z)+x. 6646,6645 [para_into,6433.1.1.2.1,1357.1.1,demod,522,522,6426] ~(x+y)+y=y+ ~x. 6849 [para_into,6459.1.1.2.1,1371.1.1,demod,522,6646,522,522,flip.1] (x+y)+ ~(~(y+z)+x)=x+ (y+z). 6867 [para_into,6459.1.1.2.1,1254.1.1,demod,6646,522,flip.1] ~x+ ~(~(y+z)+ ~(z+x))= ~(z+x)+ (y+z). 27456,27455 [para_from,2263.1.1,6433.1.1.2.1,demod,6564,522,flip.1] ~(~(x+y)+ ~(y+z))+ ~x= (y+z)+ ~(x+y). 27463 [para_from,2263.1.1,1407.1.1.1.1.1.1.2.1,demod,27456,5494,flip.1] ~x+ ~(~(x+y)+ ~(y+z))= (y+z)+ ~(x+y). 29617 [para_from,6633.1.1,1765.1.1.2.1.2.1,demod,680,6634] (x+ ~(y+z))+ ~z= ~z+x. 29962,29961 [para_into,29617.1.1.1,6645.1.1,flip.1] ~x+ ~(y+ ~(z+x))= (~(z+x)+ ~y)+ ~x. 30009,30008 [para_into,29617.1.1.1,1371.1.1,flip.1] ~x+ ~(~(x+y)+z)= ~z+ ~x. 30032,30031 [para_into,29617.1.1.1,1274.1.1] (~(x+y)+z)+ ~y= ~y+z. 30171,30170 [back_demod,6867,demod,29962,522,30032,flip.1] ~(x+y)+ (z+x)= ~y+ (z+x). 30217,30216 [back_demod,27463,demod,30009,522,flip.1] (x+y)+ ~(z+x)= (x+y)+ ~z. 30530,30529 [back_demod,6637,demod,30171,522] (x+y)+ (y+z)= (x+y)+z. 30899 [back_demod,6849,demod,30217,522,30530] (x+y)+z=x+ (y+z). 30901 [binary,30899.1,1375.1] $Ans(Robbins_basis). ------------ end of proof -------------