----- Otter 3.0.6, Feb 2000 -----
----> UNIT CONFLICT at  92.97 sec ----> 35253 [binary,35252.1,1.1] $F.

Length of proof is 213.  Level of proof is 28.

---------------- PROOF ----------------

1 [] x=x.
2 [] x+y=y+x.
4,3 [] (x+y)+z=x+ (y+z).
5 [] (x+y@ )@ + (x@ +y@ )@ =y.
8 [] ((((X+X@ )@ + ((X+Y)@ + (X@ +Y)@ ))@ + (((((Z+U)@ +V)@ + (V+Z)@ )@ +W@ )@ + (((((Z+U)@ +V)@ + (V+Z)@ )@ +V)@ + (W@ +V)@ ))@ @ )@ + ((((X+X@ )@ + ((X+Y)@ + (X@ +Y)@ ))@ +V)@ + ((((((Z+U)@ +V)@ + (V+Z)@ )@ +W@ )@ + (((((Z+U)@ +V)@ + (V+Z)@ )@ +V)@ + (W@ +V)@ ))@ @ +V)@ ))@ !=Y.
9 [para_into,3.1.1.1,2.1.1,demod,4] x+ (y+z)=y+ (x+z).
10 [para_into,3.1.1,2.1.1] x+ (y+z)=y+ (z+x).
11 [copy,10,flip.1] x+ (y+z)=z+ (x+y).
12 [para_into,9.1.1.2,9.1.1] x+ (y+ (z+u))=z+ (x+ (y+u)).
14 [para_into,9.1.1,2.1.1,demod,4] x+ (y+z)=x+ (z+y).
17 [para_into,10.1.1.2,3.1.1,demod,4] x+ (y+ (z+u))=y+ (z+ (u+x)).
18 [para_into,10.1.1.2,2.1.1] x+ (y+z)=z+ (y+x).
21 [copy,17,flip.1] x+ (y+ (z+u))=u+ (x+ (y+z)).
34 [para_into,5.1.1.1.1,5.1.1] x@ + ((y+x@ )@ @ + (y@ +x@ )@ )@ =y@ +x@ .
38 [para_into,5.1.1.1.1,2.1.1] (x@ +y)@ + (y@ +x@ )@ =x.
40 [para_into,5.1.1.2.1,5.1.1,demod,4] (x+ (y@ + (x@ +y@ )@ ))@ +y@ =x@ +y@ .
42 [para_into,5.1.1.2.1,2.1.1] (x+y@ )@ + (y@ +x@ )@ =y.
44 [para_into,5.1.1,2.1.1] (x@ +y@ )@ + (x+y@ )@ =y.
46 [para_from,5.1.1,11.1.1.2,flip.1] (x@ +y@ )@ + (z+ (x+y@ )@ )=z+y.
50,49 [para_from,5.1.1,9.1.1.2,flip.1] (x+y@ )@ + (z+ (x@ +y@ )@ )=z+y.
51 [para_from,5.1.1,3.1.1.1,flip.1] (x+y@ )@ + ((x@ +y@ )@ +z)=y+z.
57 [para_into,38.1.1.1.1,38.1.1] x@ + ((y@ +x@ )@ @ + (x@ +y)@ )@ =x@ +y.
69 [para_into,38.1.1.2.1,38.1.1] ((x@ +y@ )@ + (y@ +x))@ +y@ =x@ +y@ .
71 [para_into,38.1.1.2.1,5.1.1] ((x@ +y@ )@ + (x+y@ ))@ +y@ =x@ +y@ .
73 [para_into,38.1.1.2.1,2.1.1] (x@ +y)@ + (x@ +y@ )@ =x.
75 [para_into,38.1.1,2.1.1] (x@ +y@ )@ + (y@ +x)@ =y.
82 [para_from,38.1.1,11.1.1.2,flip.1] (x@ +y@ )@ + (z+ (y@ +x)@ )=z+y.
87 [para_from,38.1.1,3.1.1.1,flip.1] (x@ +y)@ + ((y@ +x@ )@ +z)=x+z.
96 [para_into,42.1.1.1.1,3.1.1] (x+ (y+z@ ))@ + (z@ + (x+y)@ )@ =z.
98 [para_into,42.1.1.2.1,42.1.1,demod,4] (x@ + (y@ + (y+x@ )@ ))@ +x@ =y+x@ .
104 [para_into,42.1.1,2.1.1] (x@ +y@ )@ + (y+x@ )@ =x.
119,118 [para_from,42.1.1,9.1.1.2,flip.1] (x+y@ )@ + (z+ (y@ +x@ )@ )=z+y.
142,141 [para_from,44.1.1,38.1.1.2.1] ((x+y@ )@ + (x@ +y@ ))@ +y@ =x+y@ .
167 [para_into,73.1.1,2.1.1] (x@ +y@ )@ + (x@ +y)@ =x.
268 [para_into,8.1.1.1.2.2.1.1.1.1.2.2.1,2.1.1] ((((X+X@ )@ + ((X+Y)@ + (X@ +Y)@ ))@ + (((((Z+U)@ +V)@ + (V+Z)@ )@ +W@ )@ + (((((Z+U)@ +V)@ + (V+Z)@ )@ +V)@ + (W@ +V)@ ))@ @ )@ + ((((X+X@ )@ + ((X+Y)@ + (X@ +Y)@ ))@ +V)@ + ((((((Z+U)@ +V)@ + (V+Z)@ )@ +W@ )@ + (((((Z+U)@ +V)@ + (V+Z)@ )@ +V)@ + (V+W@ )@ ))@ @ +V)@ ))@ !=Y.
1378 [para_into,46.1.1.2,167.1.1] (x@ @ +y@ )@ +x= (x@ +y@ @ )@ +y.
1380 [para_into,46.1.1.2,75.1.1] (x@ @ +y@ )@ +x= (y@ @ +x@ )@ +y.
1382,1381 [para_into,46.1.1.2,73.1.1] (x@ @ +y@ )@ +x= (x@ +y)@ +y.
1383 [para_into,46.1.1.2,42.1.1,demod,1382] (x@ +y)@ +y= (y+x@ )@ +y.
1384 [para_into,46.1.1.2,38.1.1] (x@ @ +y@ )@ +y= (y@ +x)@ +y.
1388,1387 [para_into,46.1.1.2,5.1.1] (x@ @ +y@ )@ +y= (x+y@ )@ +y.
1398 [copy,1378,flip.1,demod,1382] (x@ +y@ @ )@ +y= (x@ +y)@ +y.
1401 [copy,1380,flip.1,demod,1382,1382] (x@ +y)@ +y= (y@ +x)@ +x.
1402 [copy,1383,flip.1] (x+y@ )@ +x= (y@ +x)@ +x.
1403 [copy,1384,flip.1,demod,1388] (x@ +y)@ +x= (y+x@ )@ +x.
1404 [back_demod,1384,demod,1388] (x+y@ )@ +y= (y@ +x)@ +y.
1853 [para_into,1401.1.1.1.1,2.1.1] (x+y@ )@ +x= (x@ +y)@ +y.
1881 [para_into,1401.1.1,2.1.1] x+ (y@ +x)@ = (x@ +y)@ +y.
1909 [copy,1853,flip.1] (x@ +y)@ +y= (x+y@ )@ +x.
1937 [copy,1881,flip.1] (x@ +y)@ +y=x+ (y@ +x)@ .
2116 [para_into,1402.1.1,2.1.1] x+ (x+y@ )@ = (y@ +x)@ +x.
2148 [copy,2116,flip.1] (x@ +y)@ +y=y+ (y+x@ )@ .
2339 [para_into,1403.1.1,2.1.1] x+ (x@ +y)@ = (y+x@ )@ +x.
2390 [copy,2339,flip.1] (x+y@ )@ +y=y+ (y@ +x)@ .
2568 [para_into,1404.1.1,2.1.1] x+ (y+x@ )@ = (x@ +y)@ +x.
2602 [copy,2568,flip.1] (x@ +y)@ +x=x+ (y+x@ )@ .
3053 [para_into,40.1.1.1.1.2.2.1,1404.1.1,demod,4] (x+ (y@ @ + (y@ + ((y@ @ +x)@ +y@ )@ )))@ +y@ = (x+y@ @ )@ +y@ .
3055 [para_into,40.1.1.1.1.2.2.1,1403.1.1,demod,4] (x@ @ + (y+ (x@ + ((y+x@ @ )@ +x@ )@ )))@ +x@ = (x@ @ +y)@ +x@ .
3176,3175 [para_into,1853.1.1.1.1,1404.1.1,flip.1] ((x+y@ @ )@ @ +y)@ +y= ((y@ @ +x)@ +y@ )@ + (x+y@ @ )@ .
3214 [para_into,1853.1.1,2.1.1] x+ (x+y@ )@ = (x@ +y)@ +y.
3245 [copy,3214,flip.1] (x@ +y)@ +y=x+ (x+y@ )@ .
3406,3405 [para_into,1881.1.1.2.1,1404.1.1] x+ ((x@ +y)@ +x)@ = (x@ + (y+x@ ))@ + (y+x@ ).
3408,3407 [para_into,1881.1.1.2.1,1403.1.1] x+ ((y+x@ )@ +x)@ = (x@ + (x@ +y))@ + (x@ +y).
3439 [back_demod,3053,demod,3406] (x+ (y@ @ + ((y@ @ + (x+y@ @ ))@ + (x+y@ @ ))))@ +y@ = (x+y@ @ )@ +y@ .
3441 [back_demod,3055,demod,3408] (x@ @ + (y+ ((x@ @ + (x@ @ +y))@ + (x@ @ +y))))@ +x@ = (x@ @ +y)@ +x@ .
3471 [para_from,1881.1.1,46.1.1.2] (x@ @ +y@ )@ + ((y@ @ +x)@ +x)=y@ +y.
3506,3505 [para_into,1909.1.1.1.1,1881.1.1,flip.1] (x+ (y@ +x@ )@ @ )@ +x= ((x@ @ +y)@ +y)@ + (y@ +x@ )@ .
3559 [para_into,1909.1.1.1.1,2.1.1] (x+y@ )@ +x= (y+x@ )@ +y.
3589 [para_into,1909.1.1,2.1.1] x+ (y@ +x)@ = (y+x@ )@ +y.
3825 [para_into,1937.1.1.1.1,42.1.1,demod,4,flip.1] x+ (y@ + ((y@ +x@ )@ @ + (x+y@ ))@ )=y@ + (y@ +x@ )@ .
4182 [para_into,2148.1.1,1937.1.1] x+ (y@ +x)@ =y+ (y+x@ )@ .
4183 [para_into,2148.1.1,1909.1.1] (x+y@ )@ +x=y+ (y+x@ )@ .
4237 [copy,4182,flip.1] x+ (x+y@ )@ =y+ (x@ +y)@ .
4706 [para_into,2390.1.1,2.1.1] x+ (y+x@ )@ =x+ (x@ +y)@ .
4834,4833 [para_from,2390.1.1,1853.1.1.1.1,demod,3176,flip.1] ((x@ @ +y)@ +x@ )@ + (y+x@ @ )@ = (x@ + (x@ @ +y)@ )@ + (y+x@ @ )@ .
4946 [para_from,2568.1.1,2148.1.1.1.1,demod,4834] (x@ + (x@ @ +y)@ )@ + (y+x@ @ )@ = (y+x@ @ )@ + ((y+x@ @ )@ +x@ )@ .
5181 [para_from,2602.1.1,11.1.1.2] x+ (y+ (z+y@ )@ )=y+ (x+ (y@ +z)@ ).
5245 [copy,5181,flip.1] x+ (y+ (x@ +z)@ )=y+ (x+ (z+x@ )@ ).
5518,5517 [para_into,51.1.1.2,73.1.1,flip.1] x+ (y@ +x@ @ )@ = (y+x@ )@ +y.
5523 [para_into,51.1.1.2,42.1.1] (x+y@ )@ +y=y+ (y@ +x@ @ )@ .
5612 [para_from,3214.1.1,51.1.1.1.1,demod,4] ((x@ +y)@ +y)@ + ((x@ + (x+y@ )@ )@ +z)=x+ (y@ +z).
5643 [para_into,3245.1.1.1.1,2568.1.1,demod,4834,flip.1] x+ (x+ (y+x@ @ )@ @ )@ = (x@ + (x@ @ +y)@ )@ + (y+x@ @ )@ .
5703 [para_into,3245.1.1,2148.1.1] x+ (x+y@ )@ =y+ (y+x@ )@ .
5813 [para_from,3245.1.1,34.1.1.2.1.2.1,demod,4] x@ + ((y@ + (x@ +x@ ))@ @ + (y+ (y+x@ @ )@ )@ )@ = (y@ +x@ )@ +x@ .
5971,5970 [para_into,3559.1.1.1.1,1937.1.1,demod,3506,flip.1] ((x@ @ +y)@ +y)@ + (y@ +x@ )@ = (y+ (x@ @ +y)@ )@ + (y@ +x@ )@ .
6014,6013 [back_demod,3505,demod,5971] (x+ (y@ +x@ )@ @ )@ +x= (y+ (x@ @ +y)@ )@ + (y@ +x@ )@ .
6763 [para_into,57.1.1.2.1.2.1,3589.1.1] x@ + (((y@ +x@ )@ @ +x@ )@ @ + ((y+x@ @ )@ +y)@ )@ =x@ + (y@ +x@ )@ .
6769 [para_into,57.1.1.2.1.2.1,3214.1.1] x@ + (((x@ +y@ )@ @ +x@ )@ @ + ((x@ @ +y)@ +y)@ )@ =x@ + (x@ +y@ )@ .
7055 [para_from,4182.1.1,57.1.1.2.1.2.1] x@ + (((y@ +x@ )@ @ +x@ )@ @ + (y+ (y+x@ @ )@ )@ )@ =x@ + (y@ +x@ )@ .
7255 [para_from,4183.1.1,1404.1.1.1.1] (x+ (x+y@ @ )@ )@ +y= (y@ + (y@ +x@ )@ )@ +y.
7334 [copy,7255,flip.1] (x@ + (x@ +y@ )@ )@ +x= (y+ (y+x@ @ )@ )@ +x.
7349 [para_from,4237.1.1,1403.1.1.1.1] (x+ (y@ @ +x)@ )@ +y= ((y@ +x@ )@ +y@ )@ +y.
7384 [copy,7349,flip.1] ((x@ +y@ )@ +x@ )@ +x= (y+ (x@ @ +y)@ )@ +x.
7945 [para_from,5703.1.1,1403.1.1.1.1] (x+ (x+y@ @ )@ )@ +y= ((y@ +x@ )@ +y@ )@ +y.
7987 [copy,7945,flip.1] ((x@ +y@ )@ +x@ )@ +x= (y+ (y+x@ @ )@ )@ +x.
8077,8076 [para_into,1381.1.1,2.1.1] x+ (x@ @ +y@ )@ = (x@ +y)@ +y.
8812,8811 [para_from,5517.1.1,51.1.1.2,flip.1] x+ (y@ + (z@ +x@ )@ @ @ )@ = (z+x@ )@ + ((y+ (z@ +x@ )@ @ )@ +y).
8821 [para_from,5517.1.1,57.1.1.2.1.2.1,demod,5518] x@ + (((y@ +x@ @ @ )@ @ +x@ )@ @ + ((y+x@ @ )@ +y)@ )@ = (y+x@ @ )@ +y.
9251,9250 [para_into,5523.1.1.1.1,1401.1.1,demod,8812,6014,50] ((x@ @ +y)@ +y)@ +x= (y+ (x@ @ +y)@ )@ +x.
9372 [para_from,8076.1.1,2602.1.1.1.1,demod,9251,1382,flip.1] x+ ((x@ @ +y)@ +y)@ = (y+ (x@ @ +y)@ )@ +x.
9374 [para_from,8076.1.1,57.1.1.2.1.2.1,demod,8077] x@ + (((x@ @ @ +y@ )@ @ +x@ )@ @ + ((x@ @ +y)@ +y)@ )@ = (x@ @ +y)@ +y.
10545 [para_into,82.1.1.2,1909.1.1] (x@ +y@ )@ + ((z+ (y@ +x)@ @ )@ +z)= (z@ + (y@ +x)@ )@ +y.
10546 [para_into,82.1.1.2,1853.1.1] (x@ +y@ )@ + (((y@ +x)@ @ +z)@ +z)= ((y@ +x)@ +z@ )@ +y.
10583 [copy,10545,flip.1] (x@ + (y@ +z)@ )@ +y= (z@ +y@ )@ + ((x+ (y@ +z)@ @ )@ +x).
10584 [copy,10546,flip.1] ((x@ +y)@ +z@ )@ +x= (y@ +x@ )@ + (((x@ +y)@ @ +z)@ +z).
11052,11051 [para_into,87.1.1.2,1398.1.1] (x@ @ +y)@ + ((y@ +x)@ +x)=x@ +x.
11070 [back_demod,3471,demod,11052] x@ +x=y@ +y.
11139 [para_into,11070.1.1,14.1.1] (x+y)@ + (y+x)=z@ +z.
11145 [para_into,11070.1.1,2.1.1] x+x@ =y@ +y.
11173 [copy,11145,flip.1] x@ +x=y+y@ .
11183,11182 [para_from,11070.1.1,87.1.1.2] (x@ +y)@ + (z@ +z)=x+ (y@ +x@ ).
11204,11203 [para_from,11070.1.1,51.1.1.2] (x+y@ )@ + (z@ +z)=y+ (x@ +y@ ).
11230,11229 [para_from,11070.1.1,42.1.1.2.1] (x+x@ @ )@ + (y@ +y)@ =x@ .
11232,11231 [para_from,11070.1.1,104.1.1.2.1,demod,11230] x@ @ =x.
11288,11287 [para_from,11070.1.1,167.1.1.1.1,demod,11232] (x@ +x)@ + (y+y)@ =y@ .
11519,11518 [back_demod,10584,demod,11232,4] ((x@ +y)@ +z@ )@ +x= (y@ +x@ )@ + ((x@ + (y+z))@ +z).
11521,11520 [back_demod,10583,demod,11232] (x@ + (y@ +z)@ )@ +y= (z@ +y@ )@ + ((x+ (y@ +z))@ +x).
11767,11766 [back_demod,9374,demod,11232,11232,4,11232,11232,4,4,11232] x@ + (x@ + (y@ + (x@ + ((x+y)@ +y)@ )))@ = (x+y)@ +y.
11768 [back_demod,9372,demod,11232,11232] x+ ((x+y)@ +y)@ = (y+ (x+y)@ )@ +x.
11879,11878 [back_demod,8821,demod,11232,11232,4,11232,11232,4,4,11232] x@ + (y@ + (x@ + (x@ + ((y+x)@ +y)@ )))@ = (y+x)@ +y.
11962,11961 [back_demod,7987,demod,11519,11232,11232,flip.1] (x+ (x+y)@ )@ +y= (x+y@ )@ + ((y@ + (x@ +y))@ +y).
12155,12154 [back_demod,7384,demod,11519,11232,11232,flip.1] (x+ (y+x)@ )@ +y= (x+y@ )@ + ((y@ + (x@ +y))@ +y).
12183,12182 [back_demod,7334,demod,11521,11232,11232,11962,flip.1] (x+y@ )@ + ((y@ + (x@ +y))@ +y)= (x+y@ )@ + ((y+ (y@ +x@ ))@ +y).
12263,12262 [back_demod,7055,demod,11232,4,11232,11232,4,4] x@ + (y@ + (x@ + (x@ + (y+ (y+x)@ )@ )))@ =x@ + (y@ +x@ )@ .
12434,12433 [back_demod,6769,demod,11232,4,11232,11232,4,4,11767,flip.1] x@ + (x@ +y@ )@ = (x+y)@ +y.
12440,12439 [back_demod,6763,demod,11232,4,11232,11232,4,4,11879,flip.1] x@ + (y@ +x@ )@ = (y+x)@ +y.
12622,12621 [back_demod,5813,demod,11232,11232,4,4,12263,12440,flip.1] (x@ +y@ )@ +y@ = (x+y)@ +x.
12652,12651 [back_demod,5643,demod,11232,11232,11232,11232,flip.1] (x@ + (x+y)@ )@ + (y+x)@ =x+ (x+ (y+x))@ .
12747 [back_demod,4946,demod,11232,11232,12652,11232,11232,12434,4] x+ (x+ (y+x))@ = (y+ (x+x))@ +x.
12845 [back_demod,3825,demod,11232,4,12434] x+ (y@ + (y@ + (x@ + (x+y@ )))@ )= (y+x)@ +x.
12887 [back_demod,3441,demod,11232,11232,11232,11232,11232] (x+ (y+ ((x+ (x+y))@ + (x+y))))@ +x@ = (x+y)@ +x@ .
12889 [back_demod,3439,demod,11232,11232,11232,11232,11232] (x+ (y+ ((y+ (x+y))@ + (x+y))))@ +y@ = (x+y)@ +y@ .
13060 [back_demod,268,demod,11232,11232,4,4] ((((X+X@ )@ + ((X+Y)@ + (X@ +Y)@ ))@ + (((((Z+U)@ +V)@ + (V+Z)@ )@ +W@ )@ + (((((Z+U)@ +V)@ + (V+Z)@ )@ +V)@ + (W@ +V)@ )))@ + ((((X+X@ )@ + ((X+Y)@ + (X@ +Y)@ ))@ +V)@ + (((((Z+U)@ +V)@ + (V+Z)@ )@ +W@ )@ + (((((Z+U)@ +V)@ + (V+Z)@ )@ +V)@ + ((V+W@ )@ +V)))@ ))@ !=Y.
13191 [back_demod,11768,demod,12155,12183] x+ ((x+y)@ +y)@ = (y+x@ )@ + ((x+ (x@ +y@ ))@ +x).
13406,13405 [para_from,11231.1.1,167.1.1.2.1.1,demod,11232] (x+y@ )@ + (x+y)@ =x@ .
13413 [para_from,11231.1.1,38.1.1.1.1.1,demod,11232] (x+y)@ + (y@ +x)@ =x@ .
13417,13416 [para_from,11231.1.1,104.1.1.2.1.2,demod,11232] (x+y@ )@ + (y+x)@ =x@ .
13429,13428 [para_from,11231.1.1,42.1.1.2.1.1,demod,11232] (x+y)@ + (y+x@ )@ =y@ .
13439,13438 [para_from,11231.1.1,5.1.1.2.1.2,demod,11232] (x+y)@ + (x@ +y)@ =y@ .
13480 [back_demod,13060,demod,13439,13439] ((((X+X@ )@ +Y@ )@ + (((((Z+U)@ +V)@ + (V+Z)@ )@ +W@ )@ + (((((Z+U)@ +V)@ + (V+Z)@ )@ +V)@ + (W@ +V)@ )))@ + ((((X+X@ )@ +Y@ )@ +V)@ + (((((Z+U)@ +V)@ + (V+Z)@ )@ +W@ )@ + (((((Z+U)@ +V)@ + (V+Z)@ )@ +V)@ + ((V+W@ )@ +V)))@ ))@ !=Y.
13505 [para_into,69.1.1.1.1.1.1,4706.1.1,demod,11232,11232,11232,11232] ((x@ + (x+y)@ )@ + ((y+x)@ +x))@ + (y+x)@ =x@ + (y+x)@ .
13585 [para_into,69.1.1.1.1.2,1853.1.1] ((x@ + (x+y@ )@ )@ + ((x@ +y)@ +y))@ + (x+y@ )@ =x@ + (x+y@ )@ .
13639 [para_into,11173.1.1.1,11231.1.1] x+x@ =y+y@ .
13694 [para_from,11173.1.1,4182.1.1.2.1] x+ (y+y@ )@ =x+ (x+x@ )@ .
13751 [copy,13694,flip.1] x+ (x+x@ )@ =x+ (y+y@ )@ .
13980 [para_into,11139.1.1.1.1,13639.1.1,demod,11204] x+ (x@ +x@ )=y@ +y.
14150 [para_into,13980.1.1.2.1,11231.1.1,demod,11232] x@ + (x+x)=y@ +y.
14287 [para_into,14150.1.1,18.1.1] x+ (x+x@ )=y@ +y.
14452 [para_into,71.1.1.1.1.1.1,1401.1.1,demod,11232,4,12622] (((x+y)@ +y)@ + (y@ + (x@ +x@ )))@ +x@ = (y+x)@ +y.
14637 [para_into,14287.1.1.2,13639.1.1] x+ (y+y@ )=z@ +z.
14839 [para_into,14637.1.1,18.1.1] x@ + (x+y)=z@ +z.
14840 [para_into,14637.1.1,11.1.1] x@ + (y+x)=z@ +z.
14842 [para_into,14637.1.1,9.1.1] x+ (y+x@ )=z@ +z.
14852 [copy,14839,flip.1] x@ +x=y@ + (y+z).
14853 [copy,14840,flip.1] x@ +x=y@ + (z+y).
14855 [copy,14842,flip.1] x@ +x=y+ (z+y@ ).
15863 [para_into,96.1.1.1.1,14842.1.1] (x@ +x)@ + (y@ + (y+z)@ )@ =y.
16218 [para_into,14853.1.1.1,11231.1.1] x+x@ =y@ + (z+y).
16250 [copy,16218,flip.1] x@ + (y+x)=z+z@ .
16284 [para_from,14853.1.1,1881.1.1.2.1] x+ (y@ + (z+y))@ = (x@ +x)@ +x.
16341 [copy,16284,flip.1] (x@ +x)@ +x=x+ (y@ + (z+y))@ .
16574 [para_into,14855.1.1.1,11231.1.1] x+x@ =y+ (z+y@ ).
16608 [copy,16574,flip.1] x+ (y+x@ )=z+z@ .
16648 [para_from,14855.1.1,1401.1.1.1.1] (x+ (y+x@ ))@ +z= (z@ +z)@ +z.
16705 [copy,16648,flip.1] (x@ +x)@ +x= (y+ (z+y@ ))@ +x.
16898 [para_into,98.1.1.1.1,14839.1.1,demod,11232,11232] (x@ +x)@ +y=y+y.
17190 [para_from,16250.1.1,1881.1.1.2.1,demod,4] x+ (y+ (z+z@ )@ )= ((x+y)@ +y)@ +y.
17218 [copy,17190,flip.1] ((x+y)@ +y)@ +y=x+ (y+ (z+z@ )@ ).
17399 [para_into,16898.1.1.1.1.1,11231.1.1] (x+x@ )@ +y=y+y.
17442,17441 [para_into,16898.1.1,4183.1.1,demod,11232,11232,11232] x+ (x+x@ )@ =x+x.
17532 [back_demod,13751,demod,17442] x+x=x+ (y+y@ )@ .
17621 [para_from,16898.1.1,5703.1.1.2.1,demod,11288,11232,11232,flip.1] x+ (x+ (y@ +y))@ =x.
17951 [para_into,17399.1.1,4182.1.1,demod,11232,flip.1] (x@ + (y+y@ )@ )@ + (x@ + (y+y@ )@ )@ =x+ (x+ (y+y@ ))@ .
18077 [para_from,17399.1.1,5703.1.1.2.1,demod,11232] (x+x@ )@ + (y@ +y@ )@ =y+ (y+ (x+x@ ))@ .
18080 [para_from,17399.1.1,4183.1.1.1.1,demod,11232] (x@ +x@ )@ + (y+y@ )@ =x+ (x+ (y+y@ ))@ .
18143 [copy,18077,flip.1] x+ (x+ (y+y@ ))@ = (y+y@ )@ + (x@ +x@ )@ .
18146 [copy,18080,flip.1] x+ (x+ (y+y@ ))@ = (x@ +x@ )@ + (y+y@ )@ .
18384 [para_into,17532.1.1,9.1.1,demod,4,4] x+ (x+ (y+y))=x+ (y+ (z+z@ )@ ).
18408 [copy,18384,flip.1] x+ (y+ (z+z@ )@ )=x+ (x+ (y+y)).
18430 [para_from,17532.1.1,12.1.1.2,demod,4,4] x+ (y+ (z+ (u+u@ )@ ))=y+ (x+ (y+ (z+z))).
18439 [para_from,17532.1.1,21.1.1.2.2] x+ (y+ (z+ (u+u@ )@ ))=z+ (x+ (y+z)).
18442 [para_from,17532.1.1,11.1.1.2] x+ (y+ (z+z@ )@ )=y+ (x+y).
18465 [copy,18430,flip.1] x+ (y+ (x+ (z+z)))=y+ (x+ (z+ (u+u@ )@ )).
18474 [copy,18439,flip.1] x+ (y+ (z+x))=y+ (z+ (x+ (u+u@ )@ )).
18477 [copy,18442,flip.1] x+ (y+x)=y+ (x+ (z+z@ )@ ).
18706,18705 [para_into,17621.1.1.2.1.2.1,11231.1.1] x+ (x+ (y+y@ ))@ =x.
18718,18717 [para_into,17621.1.1.2.1.2,14852.1.1] x+ (x+ (y@ + (y+z)))@ =x.
18782,18781 [para_into,17621.1.1.2.1,16608.1.1] x+ (y+y@ )@ =x.
18854,18853 [para_into,17621.1.1,17399.1.1,demod,11204,11204] (x+ (x@ +x@ ))@ + (x+ (x@ +x@ ))@ = (x+x@ )@ .
18856,18855 [para_into,17621.1.1,16898.1.1,demod,11183,11183,18854,flip.1] (x@ +x)@ = (x+x@ )@ .
18858,18857 [back_demod,18146,demod,18706,18782,flip.1] (x@ +x@ )@ =x.
18860,18859 [back_demod,18143,demod,18706,18858,flip.1] (x+x@ )@ +y=y.
18864,18863 [back_demod,17951,demod,18782,11232,18782,11232,18706] x+x=x.
18868,18867 [back_demod,12845,demod,18718,flip.1] (x+y)@ +y=y+x@ .
18871,18870 [back_demod,18477,demod,18782] x+ (y+x)=y+x.
18875,18874 [back_demod,18474,demod,18782] x+ (y+ (z+x))=y+ (z+x).
18882,18881 [back_demod,18465,demod,18864,18782] x+ (y+ (x+z))=y+ (x+z).
18895,18894 [back_demod,18408,demod,18782,18864,flip.1] x+ (x+y)=x+y.
18905,18904 [back_demod,17218,demod,18868,18782] (x+y@ )@ +x=y+x.
18964,18963 [back_demod,16705,demod,18856,18860,flip.1] (x+ (y+x@ ))@ +z=z.
18974,18973 [back_demod,16341,demod,18856,18860,flip.1] x+ (y@ + (z+y))@ =x.
18986,18985 [back_demod,15863,demod,18856,18860] (x@ + (x+y)@ )@ =x.
19020 [back_demod,13480,demod,18860,11232,18860,11232,18905] ((Y+ (((((Z+U)@ +V)@ + (V+Z)@ )@ +W@ )@ + (((((Z+U)@ +V)@ + (V+Z)@ )@ +V)@ + (W@ +V)@ )))@ + ((Y+V)@ + (((((Z+U)@ +V)@ + (V+Z)@ )@ +W@ )@ + (((((Z+U)@ +V)@ + (V+Z)@ )@ +V)@ + (W+V)))@ ))@ !=Y.
19156,19155 [back_demod,14452,demod,18868,18864,142,flip.1] (x+y)@ +x=x+y@ .
19176,19175 [back_demod,12747,demod,18871,18864,18868] x+ (y+x)@ =x+y@ .
19374,19373 [back_demod,13585,demod,18986,18868,11232,18871,13429,flip.1] x@ + (x+y@ )@ =x@ .
19378,19377 [back_demod,13505,demod,18986,18868,18895,13417,flip.1] x@ + (y+x)@ =x@ .
19382,19381 [back_demod,13191,demod,18868,19156,119,18864] x+ (y+x@ )@ =x.
19394,19393 [back_demod,12889,demod,18871,18875,18882,18856,4,19176,18964,flip.1] (x+y)@ +y@ =y@ .
19396,19395 [back_demod,12887,demod,18895,18875,18882,18856,4,19176,18964,flip.1] (x+y)@ +x@ =x@ .
19497,19496 [back_demod,5612,demod,18868,11232,19374,11232] (x+y)@ + (y+z)=y+ (x@ +z).
20186 [back_demod,5245,demod,19382] x+ (y+ (x@ +z)@ )=y+x.
21003 [para_into,19395.1.1.1.1,11.1.1] (x+ (y+z))@ +y@ =y@ .
21246,21245 [para_into,18963.1.1,19381.1.1,demod,11232,flip.1] (x+ (y+ (z+y@ )))@ = (y+ (z+y@ ))@ .
22355,22354 [para_into,21003.1.1.1.1.2,21003.1.1,demod,11232,11232] (x+y@ )@ + (z+ (y+u))=z+ (y+u).
22360 [back_demod,19020,demod,22355] ((Y+ (((((Z+U)@ +V)@ + (V+Z)@ )@ +W@ )@ + (((((Z+U)@ +V)@ + (V+Z)@ )@ +V)@ + (W@ +V)@ )))@ + ((Y+V)@ + (((((Z+U)@ +V)@ + (V+Z)@ )@ +V)@ + (W+V))@ ))@ !=Y.
34970,34969 [para_from,20186.1.1,13413.1.1.2.1,demod,11232,4,19156,11232,flip.1] (x+ (y+z)@ )@ = (x+ (y+z@ ))@ + (x+y@ )@ .
35252 [back_demod,22360,demod,34970,19497,11232,4,21246,19394,11232,18964,34970,19497,11232,4,21246,19394,11232,18964,18864,19378,19396,34970,19497,11232,4,21246,19394,11232,18964,18864,18974,13406,11232] Y!=Y.
35253 [binary,35252.1,1.1] $F.

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