----- Otter 3.1-b0, May 2000 -----
----> UNIT CONFLICT at 756.17 sec ----> 63920 [binary,63919.1,1.1] $Ans(Robbins_basis).

Length of proof is 181.  Level of proof is 56.

---------------- 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)+ ~z)+ ~(~(~u+u)+ (~z+x))=z.
5 [para_into,3.1.1.1.1.1.1,3.1.1] ~(~x+ ~y)+ ~(~(~z+z)+ (~y+ ~(~(u+v)+ ~x)))=y.
7 [para_into,3.1.1.1.1,3.1.1] ~x+ ~(~(~y+y)+ (~(~(~z+z)+ (~x+u))+ ~(u+v)))= ~(~z+z)+ (~x+u).
9 [para_into,3.1.1.2.1.2,3.1.1] ~(~(~(~(~x+x)+ (~y+z))+u)+ ~(~(z+v)+ ~y))+ ~(~(~w+w)+y)= ~(z+v)+ ~y.
11 [para_into,5.1.1.2.1.2.2.1.1.1,5.1.1] ~(~x+ ~y)+ ~(~(~z+z)+ (~y+ ~(~u+ ~x)))=y.
15 [para_into,5.1.1.2.1.2.2.1,3.1.1] ~(~(~(~x+x)+ (~y+z))+ ~u)+ ~(~(~v+v)+ (~u+ ~y))=u.
17 [para_from,11.1.1,3.1.1.2.1.2] ~(~(~(~(~x+x)+ (~y+ ~(~z+ ~u)))+v)+ ~(~u+ ~y))+ ~(~(~w+w)+y)= ~u+ ~y.
23 [para_from,7.1.1,15.1.1.1.1.1.1.2] ~(~(~(~x+x)+ (~(~y+y)+ (~z+u)))+ ~v)+ ~(~(~w+w)+ (~v+ ~z))=v.
29 [para_into,23.1.1.1.1.1.1.2.2,11.1.1] ~(~(~(~x+x)+ (~(~y+y)+z))+ ~u)+ ~(~(~v+v)+ (~u+ ~(~w+ ~z)))=u.
33 [para_into,9.1.1.1.1,9.1.1] ~(~(~x+y)+ ~ ~x)+ ~(~(~z+z)+x)= ~(~u+u)+ ~x.
35 [para_into,33.1.1.1.1.1.1,11.1.1] ~(~x+ ~ ~(~y+ ~x))+ ~(~(~z+z)+ (~y+ ~x))= ~(~u+u)+ ~(~y+ ~x).
37 [para_into,33.1.1,33.1.1] ~(~x+x)+ ~y= ~(~z+z)+ ~y.
45,44 [para_into,37.1.1,11.1.1,flip.1] ~(~x+x)+ ~(~(~y+y)+ (~z+ ~(~u+ ~ ~z)))=z.
50 [para_from,37.1.1,23.1.1.1.1] ~(~(~x+x)+ ~y)+ ~(~(~z+z)+ (~y+ ~u))=y.
74 [para_into,50.1.1.2.1.2,11.1.1] ~(~(~x+x)+ ~(~y+ ~z))+ ~(~(~u+u)+z)= ~y+ ~z.
76 [para_into,50.1.1.2.1.2,7.1.1] ~(~(~x+x)+ ~y)+ ~(~(~z+z)+ (~(~u+u)+ (~y+v)))=y.
84 [para_from,44.1.1,50.1.1.2.1.2] ~(~(~x+x)+ ~(~y+y))+ ~(~(~z+z)+u)= ~y+y.
89 [para_from,44.1.1,17.1.1.1.1.1.1] ~(~x+ ~(~y+ ~ ~(~z+ ~y)))+ ~(~(~u+u)+ ~(~z+ ~y))= ~y+ ~ ~(~z+ ~y).
92,91 [para_from,44.1.1,9.1.1.1.1.2.1.1.1,demod,45] ~(~(~(~(~x+x)+ (~y+ ~(~z+z)))+u)+ ~(~v+ ~y))+ ~(~(~w+w)+y)= ~v+ ~y.
100 [para_from,44.1.1,3.1.1.1.1.1.1] ~(~x+ ~y)+ ~(~(~z+z)+ (~y+ ~(~u+u)))=y.
117,116 [para_into,100.1.1,37.1.1] ~(~x+x)+ ~(~(~y+y)+ (~z+ ~(~u+u)))=z.
123 [para_into,116.1.1.2.1.2,37.1.1,demod,117] ~x+x= ~y+y.
125 [para_into,116.1.1.2.1.2,29.1.1] ~(~x+x)+ ~(~(~y+y)+ ~(~z+ ~u))= ~(~(~v+v)+ (~(~w+w)+u))+ ~ ~(~z+ ~u).
129,128 [para_into,116.1.1.2.1.2,17.1.1,demod,117,flip.1] ~(~(~(~x+x)+ (~(~y+y)+ ~(~z+ ~u)))+v)+ ~(~u+ ~(~y+y))=u.
132,131 [para_into,116.1.1.2.1.2,11.1.1] ~(~x+x)+ ~(~(~y+y)+ ~(~z+ ~u))= ~u+ ~ ~(~z+ ~u).
133 [para_into,116.1.1.2.1.2,9.1.1,demod,117,flip.1] ~(~(~(~x+x)+ (~(~y+y)+z))+u)+ ~(~(z+v)+ ~(~y+y))=z+v.
141,140 [copy,125,flip.1,demod,132] ~(~(~x+x)+ (~(~y+y)+z))+ ~ ~(~u+ ~z)= ~z+ ~ ~(~u+ ~z).
153 [para_from,123.1.1,116.1.1.2.1] ~(~x+x)+ ~(~y+y)= ~(~z+z).
164,163 [para_from,123.1.1,29.1.1.2.1,demod,141] ~(~x+ ~ ~(~y+ ~x))+ ~(~z+z)= ~(~y+ ~x).
181 [para_from,123.1.1,17.1.1.2.1,demod,129] ~x+ ~(~y+y)= ~x+ ~(~z+z).
185 [para_from,123.1.1,3.1.1.2.1] ~(~(x+y)+ ~x)+ ~(~z+z)=x.
189 [copy,153,flip.1] ~(~x+x)= ~(~y+y)+ ~(~z+z).
201,200 [para_from,185.1.1,100.1.1.1.1] ~x+ ~(~(~y+y)+ (~(~z+z)+ ~(~u+u)))= ~z+z.
205 [para_into,153.1.1,153.1.1] ~(~x+x)= ~(~y+y).
213 [para_from,153.1.1,9.1.1.1.1.2.1.1.1,demod,92] ~ ~(~x+x)+ ~y= ~(~(~z+z)+ ~(~u+u))+ ~y.
217 [copy,213,flip.1] ~(~(~x+x)+ ~(~y+y))+ ~z= ~ ~(~u+u)+ ~z.
238 [para_from,205.1.1,123.1.1.1] ~(~x+x)+ (~y+y)= ~z+z.
313 [para_from,181.1.1,205.1.1.1] ~(~ ~(~x+x)+ ~(~y+y))= ~(~z+z).
350 [copy,313,flip.1] ~(~x+x)= ~(~ ~(~y+y)+ ~(~z+z)).
461 [para_from,189.1.1,44.1.1.2.1.2.2.1.1] ~(~x+x)+ ~(~(~y+y)+ (~z+ ~((~(~u+u)+ ~(~v+v))+ ~ ~z)))=z.
746 [para_from,35.1.1,116.1.1.2.1.2,demod,201] ~x+x= ~y+ ~ ~(~ ~y+ ~y).
747 [copy,746,flip.1] ~x+ ~ ~(~ ~x+ ~x)= ~y+y.
867 [para_into,747.1.1.2.1.1,123.1.1] ~x+ ~ ~(~y+y)= ~z+z.
868 [para_into,747.1.1.2.1,189.1.1] ~x+ ~(~(~y+y)+ ~(~z+z))= ~u+u.
885 [copy,867,flip.1] ~x+x= ~y+ ~ ~(~z+z).
886 [copy,868,flip.1] ~x+x= ~y+ ~(~(~z+z)+ ~(~u+u)).
939 [para_into,885.1.1,885.1.1] ~x+ ~ ~(~y+y)= ~z+ ~ ~(~u+u).
989 [para_from,885.1.1,17.1.1.2.1,demod,129] ~x+ ~(~y+ ~ ~(~z+z))= ~x+ ~(~u+u).
1017 [para_from,885.1.1,238.1.1.2] ~(~x+x)+ (~y+ ~ ~(~z+z))= ~u+u.
1471 [para_from,350.1.1,3.1.1.2.1.2.1] ~(~(x+y)+ ~(~z+z))+ ~(~(~u+u)+ (~(~ ~(~v+v)+ ~(~w+w))+x))= ~z+z.
2068 [para_from,886.1.1,100.1.1.2.1.1.1] ~(~x+ ~y)+ ~(~(~z+ ~(~(~u+u)+ ~(~v+v)))+ (~y+ ~(~w+w)))=y.
2080 [para_from,886.1.1,3.1.1.2.1.1.1] ~(~(x+y)+ ~z)+ ~(~(~u+ ~(~(~v+v)+ ~(~w+w)))+ (~z+x))=z.
2329 [para_from,1017.1.1,50.1.1.2.1] ~(~(~x+x)+ ~y)+ ~(~z+z)=y.
2383 [para_into,2329.1.1.2.1.1,350.1.1] ~(~(~x+x)+ ~y)+ ~(~(~ ~(~z+z)+ ~(~u+u))+ (~v+v))=y.
3173,3172 [para_from,74.1.1,116.1.1.2.1.2,demod,117,flip.1] ~(~x+x)+ ~(~y+ ~(~z+z))=y.
3196 [para_into,3172.1.1.1.1.1,189.1.1] ~((~(~x+x)+ ~(~y+y))+ (~z+z))+ ~(~u+ ~(~v+v))=u.
3200 [para_into,3172.1.1.1.1,939.1.1] ~(~x+ ~ ~(~y+y))+ ~(~z+ ~(~u+u))=z.
3206 [para_into,3172.1.1.1,189.1.1] (~(~x+x)+ ~(~y+y))+ ~(~z+ ~(~u+u))=z.
3238 [para_into,3172.1.1.2.1,185.1.1] ~(~x+x)+ ~y= ~(y+z)+ ~y.
3270 [para_from,3172.1.1,7.1.1.2.1.2.1.1.2,demod,3173] ~(~x+x)+ ~(~(~y+y)+ (~(~(~z+z)+u)+ ~(~(~u+ ~(~v+v))+w)))= ~(~z+z)+u.
3272 [para_from,3172.1.1,3.1.1.2.1.2] ~(~(~(~x+ ~(~y+y))+z)+ ~(~u+u))+ ~(~(~v+v)+x)= ~u+u.
3300 [para_into,3238.1.1,3238.1.1] ~(x+y)+ ~x= ~(x+z)+ ~x.
3340 [para_from,3238.1.1,116.1.1.2.1.2,demod,117] (~x+x)+y= ~z+z.
3377 [copy,3340,flip.1] ~x+x= (~y+y)+z.
3451 [para_into,76.1.1.1.1,3172.1.1] ~x+ ~(~(~y+y)+ (~(~z+z)+ (~(~x+ ~(~u+u))+v)))= ~x+ ~(~u+u).
3586 [para_from,3377.1.1,313.1.1.1] ~((~x+x)+y)= ~(~z+z).
3669 [para_from,3377.1.1,3172.1.1.1.1] ~((~x+x)+y)+ ~(~z+ ~(~u+u))=z.
3792 [copy,3586,flip.1] ~(~x+x)= ~((~y+y)+z).
4721,4720 [para_into,84.1.1.2.1,3172.1.1] ~(~(~x+x)+ ~(~y+y))+ ~z= ~y+y.
4734 [back_demod,217,demod,4721] ~x+x= ~ ~(~y+y)+ ~z.
4838 [para_from,4734.1.1,3238.1.1.1.1] ~(~ ~(~x+x)+ ~y)+ ~z= ~(z+u)+ ~z.
4839 [para_from,4734.1.1,3172.1.1.1.1] ~(~ ~(~x+x)+ ~y)+ ~(~z+ ~(~u+u))=z.
4925 [para_from,4734.1.1,76.1.1.2.1.2.1.1] ~(~(~x+x)+ ~y)+ ~(~(~z+z)+ (~(~ ~(~u+u)+ ~v)+ (~y+w)))=y.
4953 [copy,4838,flip.1] ~(x+y)+ ~x= ~(~ ~(~z+z)+ ~u)+ ~x.
5070 [para_from,3300.1.1,3.1.1.1.1.1.1] ~(~(~(x+y)+ ~x)+ ~z)+ ~(~(~u+u)+ (~z+ ~(x+v)))=z.
5114,5113 [para_from,89.1.1,2329.1.1.1.1,demod,164,flip.1] ~(~x+x)+ ~(~y+ ~z)= ~(~y+ ~z).
5220,5219 [back_demod,3172,demod,5114] ~(~x+ ~(~y+y))=x.
5322,5321 [back_demod,4839,demod,5220] ~(~ ~(~x+x)+ ~y)+z=z.
5362,5361 [back_demod,3669,demod,5220] ~((~x+x)+y)+z=z.
5375 [back_demod,3451,demod,5220] ~x+ ~(~(~y+y)+ (~(~z+z)+ (x+u)))= ~x+ ~(~v+v).
5386 [back_demod,3272,demod,5220,5220] (x+y)+ ~(~(~z+z)+x)= ~u+u.
5387 [back_demod,3270,demod,5220] ~(~x+x)+ ~(~(~y+y)+ (~(~(~z+z)+u)+ ~(u+v)))= ~(~z+z)+u.
5392,5391 [back_demod,3206,demod,5220] (~(~x+x)+ ~(~y+y))+z=z.
5398,5397 [back_demod,3200,demod,5220] ~(~x+ ~ ~(~y+y))+z=z.
5402,5401 [back_demod,3196,demod,5392,5220] ~(~x+x)+y=y.
5415,5414 [back_demod,2383,demod,5402,5220,5402] ~ ~x+ ~(~y+y)=x.
5416 [back_demod,2080,demod,5402,5398] ~(~(x+y)+ ~z)+ ~(~z+x)=z.
5422 [back_demod,2068,demod,5402,5398,5220] ~(~x+ ~y)+y=y.
5426 [back_demod,1471,demod,5220,5415,5402,5402] (x+y)+ ~x= ~z+z.
5430 [back_demod,133,demod,5402,5402,5220] ~(~x+y)+ (x+z)=x+z.
5446,5445 [back_demod,4953,demod,5322] ~(x+y)+ ~x= ~x.
5448,5447 [back_demod,4925,demod,5402,5322,5402] ~ ~x+ ~(~x+y)=x.
5455 [copy,5386,flip.1,demod,5402] ~x+x= (y+z)+ ~y.
5468 [back_demod,461,demod,5402,5402,5402,5402] ~(~x+ ~ ~ ~x)=x.
5474,5473 [back_demod,5387,demod,5402,5402,5402,5402] ~(~x+ ~(x+y))=x.
5475 [back_demod,5375,demod,5402,5402] ~x+ ~(x+y)= ~x+ ~(~z+z).
5485 [back_demod,5070,demod,5446,5402] ~(~ ~x+ ~y)+ ~(~y+ ~(x+z))=y.
5553 [para_into,5422.1.1.1.1.1,3792.1.1,demod,5362] ~ ~x+x=x.
5566,5565 [para_into,5445.1.1.1.1,989.1.1,demod,5220] x+ ~ ~x= ~ ~x.
5568,5567 [back_demod,5468,demod,5566] ~ ~ ~ ~x=x.
5581,5580 [para_from,5567.1.1,5445.1.1.2,demod,5568] ~(~ ~ ~x+y)+x=x.
5603,5602 [para_from,5567.1.1,5422.1.1.1.1.1] ~(x+ ~y)+y=y.
5667 [para_from,5473.1.1,5567.1.1.1.1.1] ~ ~ ~x= ~x+ ~(x+y).
5681 [copy,5667,flip.1] ~x+ ~(x+y)= ~ ~ ~x.
5694 [para_into,5219.1.1.1.1,5567.1.1] ~(x+ ~(~y+y))= ~ ~ ~x.
5707 [copy,5694,flip.1] ~ ~ ~x= ~(x+ ~(~y+y)).
5780 [para_into,5414.1.1.1,5567.1.1] x+ ~(~y+y)= ~ ~x.
5787 [copy,5780,flip.1] ~ ~x=x+ ~(~y+y).
5789 [para_into,5426.1.1.2,5567.1.1] (~ ~ ~x+y)+x= ~z+z.
5825 [para_into,5455.1.1.1,5567.1.1] x+ ~ ~ ~x= (y+z)+ ~y.
5835,5834 [para_from,5455.1.1,5602.1.1.1.1] ~((x+y)+ ~x)+z=z.
5976,5975 [para_from,5787.1.1,5553.1.1.1] (x+ ~(~y+y))+x=x.
6414 [para_into,5430.1.1.2,5580.1.1,demod,5581] ~(~ ~(~ ~ ~x+y)+z)+x=x.
8282 [para_into,5416.1.1.1.1.1.1,5681.1.1,demod,5568] ~(x+ ~y)+ ~(~y+ ~x)=y.
8297,8296 [para_into,5416.1.1.1.1,5825.1.1,demod,5568,5835,flip.1] ~ ~ ~(x+y)= ~((x+y)+x).
8304,8303 [para_into,5416.1.1.1.1,5565.1.1,demod,8297,8297,5448,flip.1] ~ ~(x+y)= (x+y)+x.
8539 [back_demod,6414,demod,8304] ~(((~ ~ ~x+y)+ ~ ~ ~x)+z)+x=x.
8566 [para_into,8303.1.1.1.1,5602.1.1,demod,5603,flip.1] x+ ~(y+ ~x)= ~ ~x.
8583,8582 [para_from,8303.1.1,5553.1.1.1] ((x+y)+x)+ (x+y)=x+y.
8658,8657 [para_into,8566.1.1.2.1.2,5567.1.1,demod,5568] ~ ~ ~x+ ~(y+x)= ~x.
8684 [para_into,8657.1.1.2.1,8657.1.1,demod,8304,8304,8583,8304] (x+y)+ ~ ~y= (x+y)+x.
8685 [copy,8684,flip.1] (x+y)+x= (x+y)+ ~ ~y.
8686 [para_from,8657.1.1,5602.1.1.1.1] ~ ~x+ (y+x)=y+x.
8699,8698 [para_into,8686.1.1.1.1,5787.1.1] ~(x+ ~(~y+y))+ (z+ ~x)=z+ ~x.
8700 [para_into,8686.1.1.1.1,5707.1.1,demod,8304,5976] x+ (y+ ~ ~x)=y+ ~ ~x.
8712 [para_into,8686.1.1.2,8657.1.1,demod,8304,8658] ~((x+y)+x)+ ~y= ~y.
8714 [para_from,8686.1.1,5789.1.1.1] (x+ ~y)+y= ~z+z.
8753 [para_into,8714.1.1.1,5447.1.1] x+ (~x+y)= ~z+z.
8930 [para_into,8753.1.1,8686.1.1] ~ ~ ~x+x= ~y+y.
8942 [copy,8930,flip.1] ~x+x= ~ ~ ~y+y.
9223 [para_into,8930.1.1.1.1.1,5787.1.1,demod,8304,5976] x+ ~x= ~y+y.
9234 [copy,9223,flip.1] ~x+x=y+ ~y.
9254 [para_into,5485.1.1.1.1.2,5567.1.1,demod,5568] ~(~ ~x+y)+ ~(y+ ~(x+z))= ~ ~ ~y.
9256 [para_into,5485.1.1.1.1,8930.1.1,demod,5402] ~(~x+ ~(~ ~x+y))=x.
9262 [para_into,5485.1.1.2.1.2.1,8686.1.1,demod,5568] ~(x+ ~y)+ ~(~y+ ~(z+x))=y.
9279 [copy,9254,flip.1] ~ ~ ~x= ~(~ ~y+x)+ ~(x+ ~(y+z)).
9359 [para_from,9234.1.1,5447.1.1.2.1] ~ ~x+ ~(y+ ~y)=x.
9572 [para_from,8942.1.1,5447.1.1.2.1] ~ ~x+ ~(~ ~ ~y+y)=x.
9600 [para_from,8942.1.1,5694.1.1.1.2.1] ~(x+ ~(~ ~ ~y+y))= ~ ~ ~x.
9602 [para_from,8942.1.1,5219.1.1.1.2.1] ~(~x+ ~(~ ~ ~y+y))=x.
9630 [copy,9600,flip.1] ~ ~ ~x= ~(x+ ~(~ ~ ~y+y)).
11026 [para_from,8712.1.1,5475.1.1.2.1,demod,8304,8583,8304,8583] (x+y)+ ~ ~y= (x+y)+ ~(~z+z).
11033 [copy,11026,flip.1] (x+y)+ ~(~z+z)= (x+y)+ ~ ~y.
11065,11064 [para_into,9256.1.1.1.2.1,9359.1.1] ~(~x+ ~x)=x.
11069,11068 [para_into,11064.1.1.1.1,11064.1.1,demod,11065] ~(x+x)= ~x+ ~x.
11077 [para_into,11064.1.1.1.1,5707.1.1] ~(~(x+ ~(~y+y))+ ~ ~ ~x)= ~ ~x.
11080 [para_into,11064.1.1.1.1,5667.1.1] ~((~x+ ~(x+y))+ ~ ~ ~x)= ~ ~x.
11083,11082 [para_into,11064.1.1.1.1,5567.1.1,demod,5568,11069,flip.1] ~ ~ ~x= ~x+ ~x.
11085,11084 [para_into,11064.1.1.1.1,5473.1.1,demod,5474,11069,flip.1] ~x+ ~(x+y)= ~x+ ~x.
11104,11103 [back_demod,11064,demod,11069] ~ ~x+ ~ ~x=x.
11108,11107 [back_demod,11080,demod,11085,11083,11069,11069,11104,11069,11104,flip.1] ~ ~x=x+x.
11110,11109 [back_demod,11077,demod,11108,11069,8699,11069,11108,11108,11108] (x+x)+ (x+x)=x+x.
11297,11296 [back_demod,9630,demod,11108,11069,11108,11069,flip.1] ~(x+ ~((~y+ ~y)+y))= ~x+ ~x.
11302,11301 [back_demod,9602,demod,11108,11069,11297,11108,11108,11110] x+x=x.
11310,11309 [back_demod,9572,demod,11108,11302,11108,11302] x+ ~(~y+y)=x.
11323 [back_demod,9279,demod,11108,11302,11108,11302,flip.1] ~(x+y)+ ~(y+ ~(x+z))= ~y.
11375 [back_demod,8539,demod,11108,11302,11108,11302] ~(((~x+y)+ ~x)+z)+x=x.
11517,11516 [back_demod,11033,demod,11310,11108,11302,flip.1] (x+y)+y=x+y.
11561,11560 [back_demod,8700,demod,11108,11302,11108,11302] x+ (y+x)=y+x.
11563,11562 [back_demod,8685,demod,11108,11302,11517] (x+y)+x=x+y.
11595,11594 [back_demod,11107,demod,11302] ~ ~x=x.
11623,11622 [back_demod,11375,demod,11563] ~((~x+y)+z)+x=x.
11726,11725 [para_from,11560.1.1,5430.1.1.1.1] ~(x+ ~y)+ (y+z)=y+z.
12213 [para_from,11622.1.1,11562.1.1.1,demod,11623] x+ ~((~x+y)+z)=x.
12359,12358 [para_into,12213.1.1.2.1.1,5602.1.1] (x+ ~y)+ ~(y+z)=x+ ~y.
14288 [para_into,8282.1.1.1.1.2,11594.1.1,demod,11595] ~(x+y)+ ~(y+ ~x)= ~y.
16982 [para_into,9262.1.1.1.1.2,11594.1.1,demod,11595] ~(x+y)+ ~(y+ ~(z+x))= ~y.
19159,19158 [para_into,14288.1.1.1.1,14288.1.1,demod,11595,11595,11726,11595] x+ ~(y+x)=x+ ~y.
19162 [para_into,14288.1.1.2.1.2,11594.1.1] ~(~x+y)+ ~(y+x)= ~y.
19164 [para_into,14288.1.1.2.1,14288.1.1,demod,12359,11595,11595] ~(x+ ~y)+x=y+x.
19179,19178 [para_into,19164.1.1.1.1.2,11594.1.1] ~(x+y)+x= ~y+x.
20347 [para_from,11323.1.1,19178.1.1.1.1,demod,11595,19159,11595,flip.1] (x+ ~(y+z))+ ~(y+x)=x+ ~y.
54696 [para_from,16982.1.1,19158.1.1.2.1,demod,11595,19179,11595,11595,flip.1] ~(x+ ~(y+z))+ (z+x)= (y+z)+x.
62360 [para_into,20347.1.1.1,20347.1.1,demod,12359,flip.1] (x+ ~(y+z))+ ~y=x+ ~y.
62871,62870 [para_into,62360.1.1.1.2.1,16982.1.1,demod,11595,11595,11595] (x+y)+ (z+y)=x+ (z+y).
63009,63008 [para_into,62360.1.1.1.2.1,5445.1.1,demod,11595,11595,11595] (x+y)+ (y+z)=x+ (y+z).
63099,63098 [para_into,62870.1.1.1,19178.1.1,demod,62871,flip.1] ~(x+y)+ (z+x)= ~y+ (z+x).
63248,63247 [back_demod,54696,demod,63099,11595,63009,flip.1] (x+y)+z=x+ (y+z).
63840 [back_demod,11562,demod,63248,11561] x+y=y+x.
63841 [back_demod,2,demod,63248,unit_del,63840,1] ~(~(A+B)+ ~(~A+B))!=B|$Ans(Robbins_basis).
63896,63895 [para_from,63840.1.1,19162.1.1.2.1] ~(~x+y)+ ~(x+y)= ~y.
63919 [para_from,63840.1.1,63841.1.1.1,demod,63896,11595] B!=B|$Ans(Robbins_basis).
63920 [binary,63919.1,1.1] $Ans(Robbins_basis).

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