----- Otter 3.1-b0, May 2000 -----
----> UNIT CONFLICT at  53.48 sec ----> 18023 [binary,18022.1,1.1] $Ans(Robbins_basis).

Length of proof is 146.  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)+ ~(~(y+ ~(z+ ~y))+ ~(x+u))=y.
6,5 [para_into,3.1.1.2.1.2.1,3.1.1] ~(~(x+ ~y)+ ~z)+ ~(~(z+ ~(u+ ~z))+ ~y)=z.
7 [para_into,3.1.1.2.1,3.1.1] ~(~((x+ ~y)+ ~(z+ ~(x+ ~y)))+ ~y)+ ~(x+ ~y)=y.
11 [para_into,7.1.1.1.1.1.1.2.1,7.1.1] ~(~((x+ ~y)+ ~y)+ ~y)+ ~(x+ ~y)=y.
13 [para_from,7.1.1,5.1.1.2.1.1.1.2.1] ~(~(x+ ~y)+ ~(z+ ~u))+ ~(~((z+ ~u)+ ~u)+ ~y)=z+ ~u.
17 [para_from,7.1.1,3.1.1.2.1.1.1.2.1] ~(x+ ~(y+ ~z))+ ~(~((y+ ~z)+ ~z)+ ~(x+u))=y+ ~z.
19 [para_from,7.1.1,5.1.1.1.1.1.1] ~(~x+ ~y)+ ~(~(y+ ~(z+ ~y))+ ~(u+ ~x))=y.
21 [para_into,19.1.1.2.1.1.1.2.1,11.1.1] ~(~x+ ~(y+ ~z))+ ~(~((y+ ~z)+ ~z)+ ~(u+ ~x))=y+ ~z.
27 [para_into,19.1.1.2.1,3.1.1] ~(~(x+y)+ ~x)+ ~(z+ ~x)=x.
29 [para_into,27.1.1.2.1,27.1.1] ~(~((x+ ~y)+z)+ ~(x+ ~y))+ ~y=x+ ~y.
31 [para_into,13.1.1.1.1,27.1.1] ~x+ ~(~((y+ ~x)+ ~x)+ ~x)=y+ ~x.
38,37 [para_into,29.1.1.1.1.1.1.1,5.1.1,demod,6,6] ~(~(x+y)+ ~x)+ ~(~(x+ ~(z+ ~x))+ ~u)=x.
42,41 [para_into,37.1.1.2.1,31.1.1] ~(~(x+y)+ ~x)+ ~(z+ ~(x+ ~(u+ ~x)))=x.
43 [para_from,37.1.1,3.1.1.2.1.1.1] ~(x+ ~ ~(~(y+z)+ ~y))+ ~(~y+ ~(x+u))= ~(~(y+z)+ ~y).
45 [para_into,41.1.1.1.1.1.1,31.1.1] ~(~(x+ ~y)+ ~ ~y)+ ~(z+ ~(~y+ ~(u+ ~ ~y)))= ~y.
49 [para_from,41.1.1,13.1.1.2.1.1.1.1,demod,42,42] ~(~(x+ ~y)+ ~z)+ ~(~(z+ ~(u+ ~(z+ ~(v+ ~z))))+ ~y)=z.
51 [para_from,41.1.1,5.1.1.1.1.1.1] ~(~x+ ~y)+ ~(~(y+ ~(z+ ~y))+ ~(u+ ~(x+ ~(v+ ~x))))=y.
57 [para_into,17.1.1.1.1.2.1,41.1.1,demod,42,42] ~(x+ ~y)+ ~(~(y+ ~(z+ ~(y+ ~(u+ ~y))))+ ~(x+v))=y.
59 [para_into,17.1.1.1.1.2.1,37.1.1,demod,38,38] ~(x+ ~y)+ ~(~(y+ ~(~(y+ ~(z+ ~y))+ ~u))+ ~(x+v))=y.
61 [para_into,17.1.1.1.1,27.1.1] ~x+ ~(~((y+ ~x)+ ~x)+ ~(~(~(x+z)+ ~x)+u))=y+ ~x.
63 [para_from,17.1.1,5.1.1.2.1] ~(~(x+ ~(~((y+ ~z)+ ~z)+ ~(z+u)))+ ~z)+ ~(y+ ~z)=z.
77 [para_from,43.1.1,45.1.1.2.1] ~(~(x+ ~y)+ ~ ~y)+ ~ ~(~(y+z)+ ~y)= ~y.
79 [para_from,43.1.1,41.1.1.2.1] ~(~(~x+y)+ ~ ~x)+ ~ ~(~(x+z)+ ~x)= ~x.
86 [para_from,77.1.1,27.1.1.1.1] ~ ~x+ ~(y+ ~ ~(~(x+z)+ ~x))= ~(~(x+z)+ ~x).
97 [para_from,79.1.1,43.1.1.1.1] ~ ~x+ ~(~x+ ~(~(~(~x+y)+ ~ ~x)+z))= ~(~(x+u)+ ~x).
98 [copy,97,flip.1] ~(~(x+y)+ ~x)= ~ ~x+ ~(~x+ ~(~(~(~x+z)+ ~ ~x)+u)).
104,103 [para_into,86.1.1.2.1,79.1.1,flip.1] ~(~(x+y)+ ~x)= ~ ~x+ ~ ~x.
110,109 [back_demod,98,demod,104,104,flip.1] ~ ~x+ ~(~x+ ~((~ ~ ~x+ ~ ~ ~x)+y))= ~ ~x+ ~ ~x.
125 [back_demod,61,demod,104] ~x+ ~(~((y+ ~x)+ ~x)+ ~((~ ~x+ ~ ~x)+z))=y+ ~x.
135 [back_demod,27,demod,104] (~ ~x+ ~ ~x)+ ~(y+ ~x)=x.
139 [para_from,135.1.1,3.1.1.2.1.2.1] ~((~ ~x+ ~ ~x)+ ~y)+ ~(~(y+ ~(z+ ~y))+ ~x)=y.
144,143 [para_into,103.1.1.1.1.1,31.1.1] ~(~(x+ ~y)+ ~ ~y)= ~ ~ ~y+ ~ ~ ~y.
151 [para_from,103.1.1,57.1.1.2.1.1.1.2.1.2.1.2] ~(x+ ~y)+ ~(~(y+ ~(z+ ~(y+ (~ ~y+ ~ ~y))))+ ~(x+u))=y.
167,166 [para_from,103.1.1,135.1.1.2] (~ ~x+ ~ ~x)+ (~ ~x+ ~ ~x)=x.
176 [para_from,103.1.1,3.1.1.2.1.2] ~(~(x+y)+ ~z)+ ~(~(z+ ~(u+ ~z))+ (~ ~x+ ~ ~x))=z.
180 [para_from,103.1.1,19.1.1.2.1.1.1.2] ~(~x+ ~y)+ ~(~(y+ (~ ~y+ ~ ~y))+ ~(z+ ~x))=y.
183 [para_into,49.1.1.1,103.1.1] (~ ~x+ ~ ~x)+ ~(~(x+ ~(y+ ~(x+ ~(z+ ~x))))+ ~u)=x.
202,201 [para_into,51.1.1.2.1,59.1.1] ~(~x+ ~x)+ ~(y+ ~x)=x.
206 [para_into,201.1.1.1.1.1,103.1.1,demod,104,167,104] ~x+ ~(y+ (~ ~x+ ~ ~x))= ~(x+z)+ ~x.
213 [para_into,201.1.1.2,103.1.1] ~(~x+ ~x)+ (~ ~x+ ~ ~x)=x.
216 [copy,206,flip.1] ~(x+y)+ ~x= ~x+ ~(z+ (~ ~x+ ~ ~x)).
223 [para_into,213.1.1.1.1.1,143.1.1,demod,144,167,144,144,202,flip.1] ~(x+ ~y)+ ~ ~y= ~ ~y+ ~ ~y.
226,225 [para_into,213.1.1.1.1.1,103.1.1,demod,104,167,104,104,202,flip.1] ~(x+y)+ ~x= ~x+ ~x.
237 [back_demod,216,demod,226,flip.1] ~x+ ~(y+ (~ ~x+ ~ ~x))= ~x+ ~x.
242,241 [back_demod,103,demod,226] ~(~x+ ~x)= ~ ~x+ ~ ~x.
247 [para_into,225.1.1.1.1,225.1.1,demod,242,flip.1] ~ ~(x+y)+ ~ ~(x+y)= (~ ~x+ ~ ~x)+ ~ ~(x+y).
264,263 [para_into,63.1.1.1.1.1.1,21.1.1] ~(~(x+ ~y)+ ~y)+ ~(x+ ~y)=y.
269 [para_from,241.1.1,225.1.1.2,demod,242,242,167] ~((~x+ ~x)+y)+ (~ ~x+ ~ ~x)=x.
303 [para_into,263.1.1.1.1.1.1,263.1.1,demod,264] ~(~x+ ~(y+ ~x))+ ~x=y+ ~x.
316,315 [para_into,303.1.1.1.1,31.1.1,flip.1] ~((x+ ~y)+ ~y)+ ~y= ~(x+ ~y)+ ~y.
323 [back_demod,31,demod,316] ~x+ ~(~(y+ ~x)+ ~x)=y+ ~x.
333 [para_into,323.1.1.2.1,225.1.1,demod,242] ~x+ (~ ~x+ ~ ~x)=x+ ~x.
336,335 [para_into,323.1.1,59.1.1,demod,226,242,flip.1] x+ (~ ~x+ ~ ~x)=x.
340,339 [para_into,323.1.1,3.1.1,flip.1] x+ ~(y+ ~x)=x.
341 [back_demod,180,demod,336] ~(~x+ ~y)+ ~(~y+ ~(z+ ~x))=y.
345 [back_demod,151,demod,336,340] ~(x+ ~y)+ ~(~y+ ~(x+z))=y.
362,361 [back_demod,183,demod,340,340] (~ ~x+ ~ ~x)+ ~(~x+ ~y)=x.
363 [back_demod,176,demod,340] ~(~(x+y)+ ~z)+ ~(~z+ (~ ~x+ ~ ~x))=z.
367 [back_demod,139,demod,340] ~((~ ~x+ ~ ~x)+ ~y)+ ~(~y+ ~x)=y.
378,377 [para_into,339.1.1.2.1,339.1.1] (x+ ~y)+ ~y=x+ ~y.
391 [back_demod,125,demod,378] ~x+ ~(~(y+ ~x)+ ~((~ ~x+ ~ ~x)+z))=y+ ~x.
395 [back_demod,63,demod,378] ~(~(x+ ~(~(y+ ~z)+ ~(z+u)))+ ~z)+ ~(y+ ~z)=z.
404,403 [para_into,377.1.1.1,109.1.1,demod,362,110,flip.1] ~ ~x+ ~ ~x=x.
409 [back_demod,391,demod,404] ~x+ ~(~(y+ ~x)+ ~(x+z))=y+ ~x.
417 [back_demod,367,demod,404] ~(x+ ~y)+ ~(~y+ ~x)=y.
421 [back_demod,363,demod,404] ~(~(x+y)+ ~z)+ ~(~z+x)=z.
423 [back_demod,361,demod,404] x+ ~(~x+ ~y)=x.
428,427 [back_demod,335,demod,404] x+x=x.
429 [back_demod,333,demod,428] ~x+ ~ ~x=x+ ~x.
436,435 [back_demod,269,demod,428,428,226,428] ~ ~x=x.
448,447 [back_demod,247,demod,436,436,428,436,436,428,436,flip.1] x+ (x+y)=x+y.
450,449 [back_demod,237,demod,436,436,428,428] ~x+ ~(y+x)= ~x.
451 [back_demod,223,demod,436,436,436,428] ~(x+ ~y)+y=y.
457 [back_demod,225,demod,428] ~(x+y)+ ~x= ~x.
464,463 [back_demod,429,demod,436] ~x+x=x+ ~x.
471 [para_into,341.1.1.1.1,339.1.1,demod,436,436,436] x+ ~(~(y+x)+ ~(z+ ~x))=y+x.
483 [para_from,435.1.1,323.1.1.1,demod,436,436,436] x+ ~(~(y+x)+x)=y+x.
501 [para_into,451.1.1.1.1.2,435.1.1] ~(x+y)+ ~y= ~y.
505 [para_into,345.1.1.1.1.2,435.1.1,demod,436] ~(x+y)+ ~(y+ ~(x+z))= ~y.
511 [para_into,345.1.1.2.1,451.1.1,demod,436,436,436] ~(x+ ~(y+ (x+z)))+ (x+z)=y+ (x+z).
516,515 [para_into,423.1.1.2.1.2,435.1.1] x+ ~(~x+y)=x.
518,517 [para_into,515.1.1.2.1.1,435.1.1] ~x+ ~(x+y)= ~x.
522,521 [para_from,449.1.1,451.1.1.1.1,demod,436] x+ (y+x)=y+x.
529 [para_into,521.1.1.2,515.1.1,demod,516] ~(~x+y)+x=x.
532,531 [para_from,457.1.1,515.1.1.2.1,demod,436] (x+y)+x=x+y.
539 [para_into,395.1.1.1.1.1.1.2.1.1.1.2,435.1.1,demod,436,436] ~(~(x+ ~(~(y+z)+ ~(~z+u)))+z)+ ~(y+z)= ~z.
543 [para_into,395.1.1.1.1.1.1.2.1.1.1,517.1.1,demod,436,518,436] ~(~(x+ ~(y+ ~((y+z)+u)))+ ~(y+z))+y=y+z.
547 [para_into,395.1.1.1.1.1.1.2.1.2.1,521.1.1] ~(~(x+ ~(~(y+ ~z)+ ~(u+z)))+ ~z)+ ~(y+ ~z)=z.
567 [para_into,483.1.1.2.1.1.1,531.1.1,demod,532] x+ ~(~(x+y)+x)=x+y.
569 [para_into,483.1.1.2.1.1.1,517.1.1,demod,436,518] ~(x+y)+ ~(x+ ~(x+y))= ~x.
611 [para_into,409.1.1.1,435.1.1,demod,436,436] x+ ~(~(y+x)+ ~(~x+z))=y+x.
621 [para_into,409.1.1.2.1.1.1,449.1.1,demod,436,450] ~(x+y)+ ~(y+ ~((x+y)+z))= ~y.
635 [para_into,417.1.1.1.1.2,435.1.1,demod,436] ~(x+y)+ ~(y+ ~x)= ~y.
646,645 [para_into,635.1.1.2.1.2,435.1.1] ~(~x+y)+ ~(y+x)= ~y.
649 [para_into,645.1.1.1.1,645.1.1,demod,436,436] x+ ~(~(x+y)+ (~y+x))=x+y.
654,653 [para_into,421.1.1.1.1.2,435.1.1,demod,436] ~(~(x+y)+z)+ ~(z+x)= ~z.
683 [para_into,421.1.1.2.1,457.1.1,demod,436] ~(~(~x+y)+ ~(x+z))+x=x+z.
723 [para_into,505.1.1.2.1.2.1,635.1.1,demod,436] ~(~(x+y)+z)+ ~(z+y)= ~z.
767 [para_into,653.1.1.1.1,653.1.1,demod,436,436] x+ ~(~(x+y)+ ~(y+z))=x+y.
833 [para_into,723.1.1.2.1,569.1.1,demod,436,436] ~(~(x+ ~(y+ ~(y+z)))+ ~(y+z))+y=y+z.
843 [para_into,723.1.1.2.1,457.1.1,demod,436,436] ~(~(x+ ~y)+ ~(y+z))+y=y+z.
845 [para_from,723.1.1,653.1.1.1.1,demod,436,436] x+ ~(~(x+y)+ ~(z+y))=x+y.
913 [para_from,471.1.1,653.1.1.2.1] ~(~(~(~(x+y)+ ~(z+ ~y))+u)+y)+ ~(x+y)= ~y.
959 [para_into,649.1.1.2.1.2,645.1.1] ~(x+y)+ ~(~(~(x+y)+ (~y+x))+ ~x)= ~(x+y)+ (~y+x).
1049 [para_into,845.1.1.2.1.1.1,653.1.1,demod,436,654] ~(~(x+y)+z)+ ~(z+ ~(u+ ~(z+x)))= ~z.
1399 [para_from,539.1.1,611.1.1.2.1,demod,436,428,464,flip.1] ~(x+ ~(~(y+ ~y)+ ~(~y+z)))+y=y.
1547 [para_into,683.1.1.1.1,621.1.1,demod,436,428,464,flip.1] x+ ~((x+ ~x)+y)=x.
1568,1567 [para_into,1547.1.1.2.1.1.2,435.1.1,demod,464] ~x+ ~((x+ ~x)+y)= ~x.
1578,1577 [para_from,1547.1.1,543.1.1.1.1.1.1,demod,1568,436,448,flip.1] (x+ ~x)+y=x+ ~x.
1580,1579 [para_from,1547.1.1,511.1.1.1.1,demod,1578] ~x+ (x+y)=x+ ~x.
1814,1813 [para_from,1577.1.1,449.1.1.2.1] ~x+ ~(y+ ~y)= ~x.
1825,1824 [para_from,1577.1.1,501.1.1.1.1] ~(x+ ~x)+ ~y= ~y.
1827,1826 [para_from,1577.1.1,395.1.1.2.1,demod,1578,1825,436,1814] ~(~(x+ (y+z))+ ~y)=y.
1829,1828 [para_from,1577.1.1,395.1.1.1.1.1.1.2.1.1.1,demod,1825,436,1827,1578] x+ ~(y+ ~y)=x.
1830 [para_from,1577.1.1,409.1.1.2.1.1.1,demod,1825,436,1580,1578] x+ ~x=y+ ~y.
1834,1833 [para_from,1577.1.1,451.1.1.1.1] ~(x+ ~x)+y=y.
1861 [back_demod,1399,demod,1834,436] ~(x+ (~y+z))+y=y.
1889,1888 [para_into,547.1.1.1.1.1.1.2.1.1.1,1830.1.1,demod,1834,436,1829] ~(~(x+ (y+z))+ ~z)=z.
1896 [back_demod,959,demod,1889,flip.1] ~(x+y)+ (~y+x)= ~(x+y)+x.
2252,2251 [para_into,1861.1.1.1.1.2,529.1.1] ~(x+y)+ (~y+z)= ~y+z.
2260,2259 [para_into,1861.1.1.1.1,683.1.1] ~((~x+y)+z)+x=x.
2262,2261 [back_demod,1896,demod,2252,flip.1] ~(x+y)+x= ~y+x.
2264,2263 [back_demod,567,demod,2262] x+ ~(~y+x)=x+y.
2466 [para_from,2259.1.1,531.1.1.1,demod,2260] x+ ~((~x+y)+z)=x.
2476 [para_into,2261.1.1.1.1,845.1.1,demod,2262,436,flip.1] (~(x+y)+ ~(z+y))+x= ~y+x.
2478 [para_into,2261.1.1.1.1,767.1.1,demod,2262,436,flip.1] (~(x+y)+ ~(y+z))+x= ~y+x.
2484 [para_into,2261.1.1.1.1,653.1.1,demod,436,2264,436,flip.1] (x+y)+ ~(~(y+z)+x)=x+ (y+z).
2550 [para_into,2263.1.1.2.1.1,435.1.1] x+ ~(y+x)=x+ ~y.
2562 [para_into,2263.1.1.2.1,723.1.1,demod,436,2262,flip.1] ~(x+y)+ (~(z+y)+x)= ~y+x.
2782 [para_into,2466.1.1.2.1.1,529.1.1] (~x+y)+ ~(x+z)= ~x+y.
2806 [para_into,2550.1.1.2.1,767.1.1,demod,2262,436,flip.1] ~(~(x+y)+ ~(y+z))+ ~x= (y+z)+ ~(x+y).
14397,14396 [para_into,2476.1.1.1.2.1,2782.1.1,demod,436] (~(x+ ~(y+z))+ ~(~y+u))+x= (y+z)+x.
14444 [para_from,2476.1.1,645.1.1.2.1] ~(~x+ (~(x+y)+ ~(z+y)))+ ~(~y+x)= ~(~(x+y)+ ~(z+y)).
14686 [para_from,2478.1.1,645.1.1.2.1] ~(~x+ (~(x+y)+ ~(y+z)))+ ~(~y+x)= ~(~(x+y)+ ~(y+z)).
15718 [para_into,2562.1.1.2,2562.1.1,demod,2252,flip.1] ~x+ (~(y+x)+z)= ~x+z.
16051,16050 [para_into,15718.1.1.2.1.1,913.1.1,demod,436,436,436] (x+y)+ (y+z)= (x+y)+z.
16053,16052 [para_into,15718.1.1.2.1.1,843.1.1] ~x+ (~(x+y)+z)= ~x+z.
16111,16110 [back_demod,14686,demod,16053,flip.1] ~(~(x+y)+ ~(y+z))= ~(~x+ ~(y+z))+ ~(~y+x).
16115,16114 [back_demod,14444,demod,16053,flip.1] ~(~(x+y)+ ~(z+y))= ~(~x+ ~(z+y))+ ~(~y+x).
16239,16238 [back_demod,2806,demod,16111,14397,flip.1] (x+y)+ ~(z+x)= (x+y)+ ~z.
16286 [back_demod,2,demod,16115] B+A!=A+B| (A+B)+C!=A+ (B+C)| ~(~A+ ~(~A+B))+ ~(~B+A)!=B|$Ans(Robbins_basis).
16432,16431 [back_demod,2484,demod,16239,436,16051] (x+y)+z=x+ (y+z).
16590 [back_demod,16286,demod,16432,unit_del,1] B+A!=A+B| ~(~A+ ~(~A+B))+ ~(~B+A)!=B|$Ans(Robbins_basis).
17460 [back_demod,531,demod,16432,522] x+y=y+x.
17592,17591 [para_from,1049.1.1,833.1.1.1.1.1.1,demod,436,2262,436,16432,2262,522,flip.1] x+ ~(x+y)= ~y+x.
17659 [back_demod,16590,demod,17592,unit_del,17460] ~(~B+ ~A)+ ~(~B+A)!=B|$Ans(Robbins_basis).
18022 [para_from,17460.1.1,17659.1.1.1.1,demod,646,436] B!=B|$Ans(Robbins_basis).
18023 [binary,18022.1,1.1] $Ans(Robbins_basis).

------------ end of proof -------------