----- Otter 3.0.6, Feb 2000 -----
----> UNIT CONFLICT at 235.52 sec ----> 119506 [binary,119505.1,10855.1] $Ans(Huntington_axioms_and).

Length of proof is 498.  Level of proof is 84.

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

1 [] x=x.
3,2 [] (((x*x@ )+ ((x*y)+ (x@ *y)))* ((((((z+ (u+v)@ )@ +0)*1)+ (z+v)@ )@ *w@ )+ ((((((z+ (u+v)@ )@ +0)*1)+ (z+v)@ )@ *z)+ (w@ *z)))@ )+ ((((x*x@ )+ ((x*y)+ (x@ *y)))*z)+ (((((((z+ (u+v)@ )@ +0)*1)+ (z+v)@ )@ *w@ )+ ((((((z+ (u+v)@ )@ +0)*1)+ (z+v)@ )@ *z)+ (w@ *z)))@ *z))=y.
6 [] A*B!=B*A| (A*B)*C!=A* (B*C)| (A*B@ )@ * (A@ *B@ )@ !=B| (A@ *B@ )@ !=A+B|$Ans(Huntington_axioms_and).
7 [copy,6,flip.1] B*A!=A*B| (A*B)*C!=A* (B*C)| (A*B@ )@ * (A@ *B@ )@ !=B| (A@ *B@ )@ !=A+B|$Ans(Huntington_axioms_and).
9,8 [para_into,2.1.1.1.1,2.1.1,demod,3] (x* ((((((y+ (z+u)@ )@ +0)*1)+ (y+u)@ )@ *v@ )+ ((((((y+ (z+u)@ )@ +0)*1)+ (y+u)@ )@ *y)+ (v@ *y)))@ )+ ((x*y)+ (((((((y+ (z+u)@ )@ +0)*1)+ (y+u)@ )@ *v@ )+ ((((((y+ (z+u)@ )@ +0)*1)+ (y+u)@ )@ *y)+ (v@ *y)))@ *y))=x.
11,10 [back_demod,2,demod,9] (x*x@ )+ ((x*y)+ (x@ *y))=y.
12 [para_into,8.1.1.1.2.1,10.1.1,demod,11] (x*y@ )+ ((x*y)+ (y@ *y))=x.
14 [para_into,8.1.1.1.2.1,8.1.1,demod,9] (x* ((((y+ (z+u)@ )@ +0)*1)+ (y+u)@ )@ @ )+ ((x*y)+ (((((y+ (z+u)@ )@ +0)*1)+ (y+u)@ )@ @ *y))=x.
16 [para_into,8.1.1,10.1.1,flip.1] (((((x+ (y+z)@ )@ +0)*1)+ (x+z)@ )@ *u@ )+ ((((((x+ (y+z)@ )@ +0)*1)+ (x+z)@ )@ *x)+ (u@ *x))=x.
29,28 [para_into,14.1.1,10.1.1,flip.1] ((((x+ (y+z)@ )@ +0)*1)+ (x+z)@ )@ =x.
30 [back_demod,16,demod,29,29] (x*y@ )+ ((x*x)+ (y@ *x))=x.
32 [para_into,28.1.1.1.1.1.1.1.2.1,30.1.1] ((((x+y@ )@ +0)*1)+ (x+ ((y*y)+ (z@ *y)))@ )@ =x.
34 [para_into,28.1.1.1.1.1.1.1.2.1,12.1.1] ((((x+y@ )@ +0)*1)+ (x+ ((y*z)+ (z@ *z)))@ )@ =x.
36 [para_into,28.1.1.1.1.1.1.1.2.1,10.1.1] ((((x+y@ )@ +0)*1)+ (x+ ((z*y)+ (z@ *y)))@ )@ =x.
38 [para_into,28.1.1.1.1.1.1.1.2,28.1.1] ((((x+y)@ +0)*1)+ (x+ (y+z)@ )@ )@ =x.
46 [para_from,28.1.1,30.1.1.2.2.1,demod,29] (x*y)+ ((x*x)+ (y*x))=x.
48 [para_into,32.1.1.1.2.1.2.2.1,32.1.1] ((((x+y@ )@ +0)*1)+ (x+ ((y*y)+ (z*y)))@ )@ =x.
54 [para_into,38.1.1.1.1.1.1.1,46.1.1] (((x@ +0)*1)+ ((x*y)+ (((x*x)+ (y*x))+z)@ )@ )@ =x*y.
60 [para_into,38.1.1.1.2.1.2.1,46.1.1] ((((x+ (y*z))@ +0)*1)+ (x+y@ )@ )@ =x.
62 [para_into,38.1.1.1.2.1.2.1,10.1.1] ((((x+ (y*y@ ))@ +0)*1)+ (x+z@ )@ )@ =x.
64 [para_into,38.1.1.1.2.1.2,38.1.1] ((((x+ (((y+z)@ +0)*1))@ +0)*1)+ (x+y)@ )@ =x.
66 [para_into,38.1.1.1.2,38.1.1] (((((((x+y)@ +0)*1)+x)@ +0)*1)+x)@ = ((x+y)@ +0)*1.
68 [para_from,38.1.1,28.1.1.1.1.1.1] (((x+0)*1)+ ((((x+y)@ +0)*1)+ (y+z)@ )@ )@ = ((x+y)@ +0)*1.
71,70 [para_into,62.1.1.1.2.1.2,62.1.1] ((((x+ (y*y@ ))@ +0)*1)+ (x+z)@ )@ =x.
76 [para_into,70.1.1.1.2.1,10.1.1] (((((x*x@ )+ (y*y@ ))@ +0)*1)+z@ )@ =x*x@ .
78 [para_into,48.1.1.1.2.1,46.1.1] (((((x*y)+x@ )@ +0)*1)+x@ )@ =x*y.
81,80 [para_into,64.1.1.1.1.1.1.1.2.1.1.1,46.1.1] ((((x+ ((y@ +0)*1))@ +0)*1)+ (x+ (y*z))@ )@ =x.
95,94 [para_into,76.1.1.1.2,70.1.1] (((((x*x@ )+ (y*y@ ))@ +0)*1)+z)@ =x*x@ .
97,96 [para_into,94.1.1.1,46.1.1] (((x*x@ )+ (y*y@ ))@ +0)@ =x*x@ .
102 [para_into,36.1.1.1.2.1,10.1.1] (((((x*x@ )+y@ )@ +0)*1)+y@ )@ =x*x@ .
105,104 [para_into,102.1.1.1.1.1.1.1.2,80.1.1,demod,81] (((((x*x@ )+y)@ +0)*1)+y)@ =x*x@ .
108 [para_into,104.1.1.1.1.1.1.1,10.1.1] (((x@ +0)*1)+ ((y*x)+ (y@ *x)))@ =y*y@ .
110 [para_into,108.1.1,94.1.1] x*x@ =y*y@ .
115 [para_from,108.1.1,70.1.1.1.2] ((((((x@ +0)*1)+ (y*y@ ))@ +0)*1)+ (z*z@ ))@ = (x@ +0)*1.
123 [para_into,110.1.1.2,80.1.1] ((((x+ ((y@ +0)*1))@ +0)*1)+ (x+ (y*z))@ )*x=u*u@ .
126 [para_into,110.1.1.2,70.1.1] ((((x+ (y*y@ ))@ +0)*1)+ (x+z)@ )*x=u*u@ .
128 [para_into,110.1.1.2,60.1.1] ((((x+ (y*z))@ +0)*1)+ (x+y@ )@ )*x=u*u@ .
130 [para_into,110.1.1.2,38.1.1] ((((x+y)@ +0)*1)+ (x+ (y+z)@ )@ )*x=u*u@ .
133 [para_into,110.1.1.2,28.1.1] ((((x+ (y+z)@ )@ +0)*1)+ (x+z)@ )*x=u*u@ .
138 [copy,123,flip.1] x*x@ = ((((y+ ((z@ +0)*1))@ +0)*1)+ (y+ (z*u))@ )*y.
151 [para_from,110.1.1,46.1.1.2.2] (x@ *x)+ ((x@ *x@ )+ (y*y@ ))=x@ .
157 [para_from,110.1.1,36.1.1.1.2.1.2.2] ((((x+y@ @ @ )@ +0)*1)+ (x+ ((y*y@ @ )+ (z*z@ )))@ )@ =x.
173 [para_from,110.1.1,10.1.1.1] (x*x@ )+ ((y*z)+ (y@ *z))=z.
189 [para_into,173.1.1.2.1,110.1.1] (x*x@ )+ ((y*y@ )+ (z@ *z@ ))=z@ .
191 [para_into,173.1.1.2.2.1,104.1.1] (x*x@ )+ (((((((y*y@ )+z)@ +0)*1)+z)*u)+ ((y*y@ )*u))=u.
198,197 [para_into,173.1.1.2.2.1,70.1.1] (x*x@ )+ ((((((y+ (z*z@ ))@ +0)*1)+ (y+u)@ )*v)+ (y*v))=v.
200,199 [para_into,173.1.1.2.2.1,60.1.1] (x*x@ )+ ((((((y+ (z*u))@ +0)*1)+ (y+z@ )@ )*v)+ (y*v))=v.
202,201 [para_into,173.1.1.2.2.1,38.1.1] (x*x@ )+ ((((((y+z)@ +0)*1)+ (y+ (z+u)@ )@ )*v)+ (y*v))=v.
204,203 [para_into,173.1.1.2.2.1,28.1.1] (x*x@ )+ ((((((y+ (z+u)@ )@ +0)*1)+ (y+u)@ )*v)+ (y*v))=v.
205 [para_into,173.1.1.2.2,110.1.1] (x*x@ )+ ((y*y@ @ )+ (z*z@ ))=y@ @ .
221 [para_into,189.1.1.2.2.1,80.1.1,demod,81,81] (x*x@ )+ ((y*y@ )+ (z*z))=z.
303 [para_into,54.1.1,94.1.1,flip.1] ((x*x@ )+ (y*y@ ))*z=x*x@ .
305 [para_from,54.1.1,70.1.1.1.2] ((((((x@ +0)*1)+ (y*y@ ))@ +0)*1)+ (x*z))@ = (x@ +0)*1.
334 [para_from,303.1.1,221.1.1.2.2] (x*x@ )+ ((y*y@ )+ (z*z@ ))= (z*z@ )+ (u*u@ ).
337 [para_from,303.1.1,46.1.1.2.2] (x* ((y*y@ )+ (z*z@ )))+ ((x*x)+ (y*y@ ))=x.
347 [para_into,337.1.1.1.2.1,110.1.1] (x* ((y*y@ )+ (z*z@ )))+ ((x*x)+ (u*u@ ))=x.
351 [para_from,126.1.1,80.1.1.1.2.1.2,demod,71] ((((x+ ((y+0)*1))@ +0)*1)+ (x+ (z*z@ ))@ )@ =x.
355 [para_from,126.1.1,12.1.1.1,demod,198,flip.1] (((x@ + (y*y@ ))@ +0)*1)+ (x@ +z)@ =x.
357 [para_from,128.1.1,12.1.1.1,demod,200,flip.1] (((x@ + (y*z))@ +0)*1)+ (x@ +y@ )@ =x.
361 [para_from,130.1.1,12.1.1.1,demod,202,flip.1] (((x@ +y)@ +0)*1)+ (x@ + (y+z)@ )@ =x.
389 [para_from,133.1.1,12.1.1.1,demod,204,flip.1] (((x@ + (y+z)@ )@ +0)*1)+ (x@ +z)@ =x.
431 [para_into,334.1.1.2.2,110.1.1] (x*x@ )+ ((y*y@ )+ (z*z@ ))= (u*u@ )+ (v*v@ ).
433 [copy,431,flip.1] (x*x@ )+ (y*y@ )= (z*z@ )+ ((u*u@ )+ (v*v@ )).
445,444 [para_into,68.1.1.1.2.1.1.1.1,96.1.1,demod,95,97,flip.1] ((x*x@ )+0)*1=x*x@ .
452,451 [para_into,68.1.1.1.2,70.1.1,demod,445,flip.1] (((x*x@ )+ (x*x@ ))@ +0)*1= ((x*x@ )+ (x*x@ ))@ .
456,455 [para_into,68.1.1.1.2,38.1.1] (((x+0)*1)+x)@ = ((x+x)@ +0)*1.
495 [para_into,455.1.1,70.1.1,flip.1] (((x+ (y*y@ ))@ + (x+ (y*y@ ))@ )@ +0)*1=x.
623,622 [para_into,495.1.1.1.1.1.1.1.2,110.1.1] (((x+ (y*y@ ))@ + (x+ (z*z@ ))@ )@ +0)*1=x.
632 [para_from,622.1.1,351.1.1.1.1.1.1.1.2] ((((x+y)@ +0)*1)+ (x+ (z*z@ ))@ )@ =x.
636 [para_from,622.1.1,48.1.1.1.2.1.2.2] ((((x+1@ )@ +0)*1)+ (x+ ((1*1)+y))@ )@ =x.
645,644 [para_into,632.1.1.1.1.1.1.1,221.1.1] (((x@ +0)*1)+ ((y*y@ )+ (z*z@ ))@ )@ =y*y@ .
650 [para_into,632.1.1.1.1.1.1.1,46.1.1] (((x@ +0)*1)+ ((x*y)+ (z*z@ ))@ )@ =x*y.
658 [para_into,632.1.1.1.1.1.1,54.1.1] ((((x*y)+0)*1)+ (((x@ +0)*1)+ (z*z@ ))@ )@ = (x@ +0)*1.
676 [para_into,636.1.1.1.2.1.2,46.1.1] ((((x+1@ )@ +0)*1)+ (x+1)@ )@ =x.
685,684 [para_from,676.1.1,173.1.1.2.2.1] (x*x@ )+ ((((((y+1@ )@ +0)*1)+ (y+1)@ )*z)+ (y*z))=z.
698 [para_from,676.1.1,110.1.1.2] ((((x+1@ )@ +0)*1)+ (x+1)@ )*x=y*y@ .
712 [para_from,698.1.1,12.1.1.1,demod,685,flip.1] (((x@ +1@ )@ +0)*1)+ (x@ +1)@ =x.
722,721 [para_into,115.1.1.1.1.1.1.1.1,622.1.1,demod,623] ((((x+ (y*y@ ))@ +0)*1)+ (z*z@ ))@ =x.
730 [para_from,721.1.1,622.1.1.1.1.1.2,demod,722] ((x+x)@ +0)*1= ((x+ (y*y@ ))@ +0)*1.
734 [para_from,721.1.1,389.1.1.1.1.1.1.2] (((x@ +y)@ +0)*1)+ (x@ + (z*z@ ))@ =x.
755,754 [para_into,730.1.1,622.1.1,flip.1] (((x+ (y*y@ ))@ + (z*z@ ))@ +0)*1=x.
759,758 [para_from,730.1.1,455.1.1.1.1,demod,71,flip.1] (((x+x)@ + (x+x)@ )@ +0)*1=x.
775,774 [para_into,758.1.1,730.1.1] (((x+x)@ + (y*y@ ))@ +0)*1=x.
869,868 [para_from,774.1.1,355.1.1.1] x+ ((x+x)@ +y)@ =x+x.
870 [para_from,774.1.1,80.1.1.1.1.1.1.1.2] ((((x+y)@ +0)*1)+ (x+ (((y+y)@ + (z*z@ ))*u))@ )@ =x.
872 [para_from,774.1.1,721.1.1.1.1] (x+ (y*y@ ))@ = (x+x)@ .
887 [copy,872,flip.1] (x+x)@ = (x+ (y*y@ ))@ .
888 [para_into,872.1.1.1.2.2,872.1.1] (x+ ((y+ (z*z@ ))* (y+y)@ ))@ = (x+x)@ .
944 [para_from,872.1.1,355.1.1.1.1.1] (((x@ +x@ )@ +0)*1)+ (x@ +y)@ =x.
947,946 [para_from,872.1.1,632.1.1.1.2] ((((x+y)@ +0)*1)+ (x+x)@ )@ =x.
950 [para_from,872.1.1,650.1.1.1.2] (((x@ +0)*1)+ ((x*y)+ (x*y))@ )@ =x*y.
956 [para_from,872.1.1,721.1.1.1.1.1.1] ((((x+x)@ +0)*1)+ (y*y@ ))@ =x.
959 [para_from,872.1.1,70.1.1.1.1.1.1] ((((x+x)@ +0)*1)+ (x+y)@ )@ =x.
984 [para_from,872.1.1,173.1.1.2.2.1] (x*x@ )+ (((y+ (z*z@ ))*u)+ ((y+y)@ *u))=u.
1033 [para_from,872.1.1,355.1.1.2.1.1,demod,755,869] x+x=x+ (y*y@ ).
1034 [para_from,872.1.1,355.1.1.1.1.1.1.1,demod,775] x+ ((x+ (y*y@ ))@ +z)@ =x+ (y*y@ ).
1043 [para_from,872.1.1,110.1.1.2] (x+ (y*y@ ))* (x+x)@ =z*z@ .
1047 [para_from,872.1.1,221.1.1.1.2] ((x+ (y*y@ ))* (x+x)@ )+ ((z*z@ )+ (u*u))=u.
1051 [para_from,872.1.1,173.1.1.1.2] ((x+ (y*y@ ))* (x+x)@ )+ ((z*u)+ (z@ *u))=u.
1075 [copy,1033,flip.1] x+ (y*y@ )=x+x.
1083 [copy,1043,flip.1] x*x@ = (y+ (z*z@ ))* (y+y)@ .
1090 [para_into,1033.1.1,1033.1.1] x+ (y*y@ )=x+ (z*z@ ).
1109 [para_from,1033.1.1,28.1.1.1.1.1.1.1.2.1] ((((x+ (y+ (z*z@ ))@ )@ +0)*1)+ (x+y)@ )@ =x.
1111 [para_from,1033.1.1,12.1.1.2] (x@ *x@ )+ ((x@ *x)+ (y*y@ ))=x@ .
1183 [para_into,887.1.1.1,1033.1.1] (x+ (y*y@ ))@ = (x+ (z*z@ ))@ .
1212 [para_from,887.1.1,1075.1.1.2.2] x+ ((y+y)* (y+ (z*z@ ))@ )=x+x.
1341 [para_into,1090.1.1.2.2,872.1.1] x+ ((y+ (z*z@ ))* (y+y)@ )=x+ (u*u@ ).
1473 [para_from,1183.1.1,1075.1.1.2.2] x+ ((y+ (z*z@ ))* (y+ (u*u@ ))@ )=x+x.
1568 [para_from,946.1.1,110.1.1.2] ((((x+y)@ +0)*1)+ (x+x)@ )*x=z*z@ .
1591 [copy,1568,flip.1] x*x@ = ((((y+z)@ +0)*1)+ (y+y)@ )*y.
1633,1632 [para_into,956.1.1.1,1075.1.1] ((((x+x)@ +0)*1)+ (((x+x)@ +0)*1))@ =x.
1637,1636 [para_from,956.1.1,721.1.1.1.1.1.1] (((x+0)*1)+ (y*y@ ))@ = ((x+x)@ +0)*1.
1676 [para_from,956.1.1,389.1.1.1.1.1.1.1,demod,1637,759] (((x+ (y+z)@ )@ +0)*1)+ (x+z)@ = (((x+x)@ +0)*1)+ (u*u@ ).
1678 [para_from,956.1.1,357.1.1.2.1.1,demod,1637,759] (((x+ (y*z))@ +0)*1)+ (x+y@ )@ = (((x+x)@ +0)*1)+ (u*u@ ).
1682 [para_from,956.1.1,110.1.1.2] ((((x+x)@ +0)*1)+ (y*y@ ))*x=z*z@ .
1693 [back_demod,658,demod,1637] ((((x*y)+0)*1)+ (((x@ +x@ )@ +0)*1))@ = (x@ +0)*1.
1699 [back_demod,305,demod,1637] ((((((x@ +x@ )@ +0)*1)+0)*1)+ (x*y))@ = (x@ +0)*1.
1715 [copy,1682,flip.1] x*x@ = ((((y+y)@ +0)*1)+ (z*z@ ))*y.
1839 [para_from,1083.1.1,650.1.1.1.2.1.1] (((x@ +0)*1)+ (((y+ (z*z@ ))* (y+y)@ )+ (u*u@ ))@ )@ =x*x@ .
1844 [para_from,1083.1.1,444.1.1.1.1] (((x+ (y*y@ ))* (x+x)@ )+0)*1=z*z@ .
1849 [copy,1844,flip.1] x*x@ = (((y+ (z*z@ ))* (y+y)@ )+0)*1.
2034,2033 [para_into,944.1.1.1.1.1.1.1,455.1.1,demod,456,1633,456] ((x+0)*1)+ ((((x+x)@ +0)*1)+y)@ = ((x+0)*1)+x.
2101 [para_into,754.1.1.1.1.1.2.2,946.1.1] (((x+ (y*y@ ))@ + (((((z+u)@ +0)*1)+ (z+z)@ )*z))@ +0)*1=x.
2368,2367 [para_into,734.1.1.1.1.1.1.1,455.1.1,demod,456,1637,759] ((((((x+x)@ +0)*1)+y)@ +0)*1)+x= ((x+0)*1)+x.
2379 [para_into,734.1.1.2.1,1212.1.1] (((x@ +y)@ +0)*1)+ (x@ +x@ )@ =x.
2404 [para_from,950.1.1,28.1.1.1.1.1.1] ((((x*y)+0)*1)+ (((x@ +0)*1)+ (x*y))@ )@ = (x@ +0)*1.
2545 [para_from,1591.1.1,444.1.1.1.1] ((((((x+y)@ +0)*1)+ (x+x)@ )*x)+0)*1=z*z@ .
2549 [copy,2545,flip.1] x*x@ = ((((((y+z)@ +0)*1)+ (y+y)@ )*y)+0)*1.
2556,2555 [para_into,1632.1.1.1.1.1.1.1,1033.1.1] ((((x+ (y*y@ ))@ +0)*1)+ (((x+x)@ +0)*1))@ =x.
2587,2586 [para_from,1636.1.1,650.1.1.1.2] ((((x+0)@ +0)*1)+ (((x+x)@ +0)*1))@ = (x+0)*1.
2592 [para_from,1636.1.1,1034.1.1.2.1.1,demod,2034] ((x+0)*1)+x= ((x+0)*1)+ (y*y@ ).
2615 [copy,2592,flip.1] ((x+0)*1)+ (y*y@ )= ((x+0)*1)+x.
2619 [para_into,2592.1.1,2379.1.1,flip.1] (((x@ +x@ )@ +0)*1)+ (y*y@ )=x.
2621 [para_into,2592.1.1,734.1.1,flip.1] (((x@ + (y*y@ ))@ +0)*1)+ (z*z@ )=x.
2626 [para_into,2619.1.1.1.1.1.1.1,946.1.1,demod,947] (((x+x)@ +0)*1)+ (y*y@ )= (((x+z)@ +0)*1)+ (x+x)@ .
2628 [para_into,2619.1.1.1.1.1.1.1,104.1.1,demod,105,452] ((x*x@ )+ (x*x@ ))@ + (y*y@ )= ((((x*x@ )+z)@ +0)*1)+z.
2641 [para_into,2619.1.1.2.2,946.1.1] (((x@ +x@ )@ +0)*1)+ (((((y+z)@ +0)*1)+ (y+y)@ )*y)=x.
2670,2669 [para_into,2615.1.1.1.1,1033.1.1] ((0+ (x*x@ ))*1)+ (y*y@ )= ((0+0)*1)+0.
2682,2681 [para_into,2615.1.1,1473.1.1] ((x+0)*1)+ ((x+0)*1)= ((x+0)*1)+x.
2851 [para_from,1849.1.1,2621.1.1.1.1.1.1.2] (((x@ + ((((y+ (z*z@ ))* (y+y)@ )+0)*1))@ +0)*1)+ (u*u@ )=x.
3090,3089 [para_from,2669.1.1,622.1.1.1.1.1.2.1,demod,2670,456,456,2682,456,759,flip.1] (0+ (x*x@ ))*1= (0+0)*1.
3092,3091 [para_from,2669.1.1,650.1.1.1.2.1,demod,456,2556,3090,flip.1] (0+0)*1=0.
3094,3093 [para_from,2669.1.1,66.1.1.1.1.1.1.1.1.1.1.1,demod,3092,3090,3092,3090,3092,2368,3092,3090,3092,flip.1] ((0+ (x*x@ ))@ +0)*1= (0+0)@ .
3097,3096 [para_from,2669.1.1,70.1.1.1.2.1,demod,3090,3092,3094,3092,3090,3092] ((0+0)@ + (0+0)@ )@ =0.
3157,3156 [para_from,3091.1.1,455.1.1.1.1,flip.1] ((0+0)@ +0)*1= (0+0)@ .
3158 [para_from,3091.1.1,68.1.1.1.1] (0+ ((((0+x)@ +0)*1)+ (x+y)@ )@ )@ = ((0+x)@ +0)*1.
3183,3182 [para_from,3091.1.1,12.1.1.2.1] ((0+0)*1@ )+ (0+ (1@ *1))=0+0.
3312 [para_into,3096.1.1.1,1033.1.1] ((0+0)@ + (x*x@ ))@ =0.
3327,3326 [para_from,3096.1.1,774.1.1.1.1.1.1] ((0+ (x*x@ ))@ +0)*1= (0+0)@ .
3329,3328 [para_from,3096.1.1,2379.1.1.2] ((((0+0)@ +x)@ +0)*1)+0=0+0.
3461 [para_from,3096.1.1,712.1.1.2.1.1,demod,3097] (((0+1@ )@ +0)*1)+ (0+1)@ = (0+0)@ + (0+0)@ .
3473 [para_from,3096.1.1,389.1.1.1.1.1.1.1,demod,3097] (((0+ (x+y)@ )@ +0)*1)+ (0+y)@ = (0+0)@ + (0+0)@ .
3475 [para_from,3096.1.1,361.1.1.2.1.1,demod,3097] (((0+x)@ +0)*1)+ (0+ (x+y)@ )@ = (0+0)@ + (0+0)@ .
3477 [para_from,3096.1.1,357.1.1.2.1.1,demod,3097] (((0+ (x*y))@ +0)*1)+ (0+x@ )@ = (0+0)@ + (0+0)@ .
3681 [para_from,3312.1.1,1034.1.1.2.1.1] (0+0)@ + (0+x)@ = (0+0)@ + (y*y@ ).
3808 [copy,3681,flip.1] (0+0)@ + (x*x@ )= (0+0)@ + (0+y)@ .
3840,3839 [para_from,3156.1.1,959.1.1.1.1] ((0+0)@ + (0+x)@ )@ =0.
4340 [para_from,3182.1.1,66.1.1.1.1.1.1.1.1.1.1.1,demod,3157,3183,3157] (((((0+0)@ + ((0+0)*1@ ))@ +0)*1)+ ((0+0)*1@ ))@ = (0+0)@ .
4367,4366 [para_from,3328.1.1,2681.1.1.2.1,demod,3329,3092,3092,3329,3092,flip.1] 0+ ((((0+0)@ +x)@ +0)*1)=0+0.
4369,4368 [para_from,3328.1.1,455.1.1.1.1.1,demod,3092,4367,2682,456,flip.1] ((((((0+0)@ +x)@ + ((0+0)@ +x)@ )@ +0)*1)+0)*1= (0+0)@ .
4371,4370 [para_from,3328.1.1,959.1.1.1.2.1,demod,2682,456,4369,3840,flip.1] (((0+0)@ +x)@ +0)*1=0.
4372 [back_demod,4340,demod,4371] (0+ ((0+0)*1@ ))@ = (0+0)@ .
4458 [para_from,4372.1.1,389.1.1.1.1.1.1.2] (((x@ + (0+0)@ )@ +0)*1)+ (x@ + ((0+0)*1@ ))@ =x.
4743 [para_into,3808.1.1.2,1715.1.1] (0+0)@ + (((((x+x)@ +0)*1)+ (y*y@ ))*x)= (0+0)@ + (0+z)@ .
4748 [copy,4743,flip.1] (0+0)@ + (0+x)@ = (0+0)@ + (((((y+y)@ +0)*1)+ (z*z@ ))*y).
4831 [para_into,191.1.1.2.1.1.1.1.1.1.1,110.1.1] (x*x@ )+ (((((((y*y@ )+z)@ +0)*1)+z)*u)+ ((v*v@ )*u))=u.
4866 [para_from,984.1.1,34.1.1.1.2.1] (((((x*x@ )+ (y+ (z*z@ ))@ )@ +0)*1)+ (y+y)@ )@ =x*x@ .
4883 [para_into,1109.1.1.1.2.1,2621.1.1,demod,645,445] ((x*x@ )+y@ )@ = ((y@ + (z*z@ ))@ +0)*1.
4884 [para_into,1109.1.1.1.2.1,2619.1.1,demod,645,445] ((x*x@ )+y@ )@ = ((y@ +y@ )@ +0)*1.
4885 [copy,4883,flip.1] ((x@ + (y*y@ ))@ +0)*1= ((z*z@ )+x@ )@ .
4898 [para_into,4884.1.1.1.1.2,946.1.1] ((((((x+y)@ +0)*1)+ (x+x)@ )*x)+z@ )@ = ((z@ +z@ )@ +0)*1.
4905,4904 [para_into,4884.1.1.1.2,3839.1.1,demod,3840,3840,3157] ((x*x@ )+0)@ = (0+0)@ .
4906 [para_into,4884.1.1.1.2,1636.1.1,demod,1637,1637,2682,456,759] ((x*x@ )+ (((y+y)@ +0)*1))@ = (y+0)*1.
4909,4908 [para_into,4884.1.1.1.2,1183.1.1,demod,623] ((x*x@ )+ (y+ (z*z@ ))@ )@ =y.
4916 [copy,4898,flip.1] ((x@ +x@ )@ +0)*1= ((((((y+z)@ +0)*1)+ (y+y)@ )*y)+x@ )@ .
4932 [back_demod,4866,demod,4909] (((x+0)*1)+ (x+x)@ )@ =y*y@ .
4934 [copy,4932,flip.1] x*x@ = (((y+0)*1)+ (y+y)@ )@ .
4977 [para_from,4904.1.1,104.1.1.1.1.1.1,demod,3157] ((0+0)@ +0)@ =x*x@ .
5012 [para_from,4904.1.1,1341.1.1.2.1.2.2] x+ ((y+ (((z*z@ )+0)* (0+0)@ ))* (y+y)@ )=x+ (u*u@ ).
5016 [para_from,4904.1.1,888.1.1.1.2.1.2.2] (x+ ((y+ (((z*z@ )+0)* (0+0)@ ))* (y+y)@ ))@ = (x+x)@ .
5036 [para_from,4904.1.1,205.1.1.2.1.2.1,demod,4905] (x*x@ )+ ((((y*y@ )+0)* (0+0)@ @ )+ (z*z@ ))= (0+0)@ @ .
5050 [para_from,4904.1.1,1075.1.1.2.2] x+ (((y*y@ )+0)* (0+0)@ )=x+x.
5053 [para_from,4904.1.1,1682.1.1.1.2.2] ((((x+x)@ +0)*1)+ (((y*y@ )+0)* (0+0)@ ))*x=z*z@ .
5060 [para_from,4904.1.1,1111.1.1.2.2.2] (x@ *x@ )+ ((x@ *x)+ (((y*y@ )+0)* (0+0)@ ))=x@ .
5075 [para_from,4904.1.1,151.1.1.2.2.2] (x@ *x)+ ((x@ *x@ )+ (((y*y@ )+0)* (0+0)@ ))=x@ .
5079 [para_from,4904.1.1,347.1.1.1.2.1.2] (x* ((((y*y@ )+0)* (0+0)@ )+ (z*z@ )))+ ((x*x)+ (u*u@ ))=x.
5082 [para_from,4904.1.1,303.1.1.1.2.2] ((x*x@ )+ (((y*y@ )+0)* (0+0)@ ))*z=x*x@ .
5094 [para_from,4904.1.1,1051.1.1.1.1.2.2] ((x+ (((y*y@ )+0)* (0+0)@ ))* (x+x)@ )+ ((z*u)+ (z@ *u))=u.
5096 [para_from,4904.1.1,1047.1.1.1.1.2.2] ((x+ (((y*y@ )+0)* (0+0)@ ))* (x+x)@ )+ ((z*z@ )+ (u*u))=u.
5098 [para_from,4904.1.1,1043.1.1.1.2.2] (x+ (((y*y@ )+0)* (0+0)@ ))* (x+x)@ =z*z@ .
5121,5120 [para_from,4904.1.1,712.1.1.2.1.1,demod,4905,4371,869,flip.1] (x*x@ )+0=0+0.
5127,5126 [para_from,4904.1.1,444.1.1.1.1.2,demod,5121,5121,3092,5121,5121,flip.1] (0+0)* (0+0)@ =0.
5132,5131 [para_from,4904.1.1,94.1.1.1.1.1.1.1.1.2,demod,5121,5127,3327,5121,5121,5127] ((0+0)@ +x)@ =0.
5134,5133 [copy,4977,flip.1,demod,5132] x*x@ =0.
5140,5139 [copy,5012,flip.1,demod,5134,5134,5134,flip.1] x+ ((y+0)* (y+y)@ )=x+0.
5142 [copy,5016,flip.1,demod,5134,5134,5140] (x+x)@ = (x+0)@ .
5147,5146 [copy,5053,flip.1,demod,5134,5134,5134,flip.1] ((((x+x)@ +0)*1)+0)*x=0.
5151,5150 [copy,5098,flip.1,demod,5134,5134,5134,flip.1] (x+0)* (x+x)@ =0.
5171 [back_demod,5096,demod,5134,5134,5151,5134] 0+ (0+ (x*x))=x.
5173 [back_demod,5094,demod,5134,5134,5151] 0+ ((x*y)+ (x@ *y))=y.
5176,5175 [back_demod,5082,demod,5134,5134,5134,5134] (0+0)*x=0.
5177 [back_demod,5079,demod,5134,5134,5134,5134] (x* (0+0))+ ((x*x)+0)=x.
5181 [back_demod,5075,demod,5134,5134] (x@ *x)+ ((x@ *x@ )+0)=x@ .
5191 [back_demod,5060,demod,5134,5134] (x@ *x@ )+ ((x@ *x)+0)=x@ .
5199 [back_demod,5050,demod,5134,5134] x+0=x+x.
5205 [back_demod,5036,demod,5134,5134,5176,5134,flip.1] (0+0)@ @ =0+ (0+0).
5269 [back_demod,4934,demod,5134,flip.1] (((x+0)*1)+ (x+x)@ )@ =0.
5277 [back_demod,4906,demod,5134] (0+ (((x+x)@ +0)*1))@ = (x+0)*1.
5286,5285 [back_demod,4885,demod,5134,5134] ((x@ +0)@ +0)*1= (0+x@ )@ .
5303 [back_demod,4831,demod,5134,5134,5134] 0+ ((((((0+x)@ +0)*1)+x)*y)+ (0*y))=y.
5334,5333 [back_demod,4748,demod,5134,5147] (0+0)@ + (0+x)@ = (0+0)@ +0.
5396,5395 [back_demod,2851,demod,5134,5151,5176,5286,5134] (0+x@ )@ +0=x.
5412 [back_demod,2628,demod,5134,5134,5134,5134] (0+0)@ +0= (((0+x)@ +0)*1)+x.
5414 [back_demod,2626,demod,5134] (((x+x)@ +0)*1)+0= (((x+y)@ +0)*1)+ (x+x)@ .
5431,5430 [back_demod,2555,demod,5134,2587] (x+0)*1=x.
5437,5436 [back_demod,2549,demod,5134,5431,5431,flip.1] ((x+y)@ + (x+x)@ )*x=0.
5512 [back_demod,2101,demod,5134,5431,5437,5431] ((x+0)@ +0)@ =x.
5545,5544 [back_demod,1839,demod,5431,5134,5151,5134,5134] (x@ + (0+0)@ )@ =0.
5574 [back_demod,1678,demod,5431,5431,5134] (x+ (y*z))@ + (x+y@ )@ = (x+x)@ +0.
5576 [back_demod,1676,demod,5431,5431,5134] (x+ (y+z)@ )@ + (x+z)@ = (x+x)@ +0.
5698 [back_demod,870,demod,5431,5134] ((x+y)@ + (x+ (((y+y)@ +0)*z))@ )@ =x.
5739,5738 [back_demod,433,demod,5134,5134,5134,5134,5134,flip.1] 0+ (0+0)=0+0.
5788 [back_demod,197,demod,5134,5134,5431] 0+ ((((x+0)@ + (x+y)@ )*z)+ (x*z))=z.
5794 [back_demod,157,demod,5431,5134] ((x+y@ @ @ )@ + (x+ ((y*y@ @ )+0))@ )@ =x.
5806 [back_demod,138,demod,5134,5431,5431,flip.1] ((x+y@ )@ + (x+ (y*z))@ )*x=0.
5811,5810 [back_demod,4916,demod,5431,5431,5437] (x@ +x@ )@ = (0+x@ )@ .
5813,5812 [back_demod,4898,demod,5431,5437,5811,5396] (0+x@ )@ =x*1.
5815,5814 [back_demod,2641,demod,5811,5813,5431,5431,5437] (x*1)+0=x.
5818 [back_demod,4458,demod,5545,5431,5176] 0+ (x@ +0)@ =x.
5822 [back_demod,1699,demod,5811,5813,5815,5815,5431] ((x*1)+ (x*y))@ =x@ .
5834 [back_demod,3477,demod,5431,5813,5334] (0+ (x*y))@ + (x*1)= (0+0)@ +0.
5836 [back_demod,3475,demod,5431,5813,5334] (0+x)@ + ((x+y)*1)= (0+0)@ +0.
5837 [back_demod,3473,demod,5813,5815,5334] ((x+y)*1)+ (0+y)@ = (0+0)@ +0.
5838 [back_demod,3461,demod,5813,5815,5334] (1*1)+ (0+1)@ = (0+0)@ +0.
5868 [copy,5412,flip.1,demod,5431] (0+x)@ +x= (0+0)@ +0.
5870 [copy,5414,flip.1,demod,5431,5431] (x+y)@ + (x+x)@ = (x+x)@ +0.
5885 [back_demod,5303,demod,5431] 0+ ((((0+x)@ +x)*y)+ (0*y))=y.
5892,5891 [back_demod,5277,demod,5431,5813,5431] (x+x)*1=x.
5893 [back_demod,5269,demod,5431] (x+ (x+x)@ )@ =0.
5923 [back_demod,3158,demod,5431,5813,5431] ((0+x)@ + (x+y)@ )*1= (0+x)@ .
5933 [back_demod,2404,demod,5431,5431,5431] ((x*y)+ (x@ + (x*y))@ )@ =x@ .
5936 [back_demod,2379,demod,5431,5811,5813] (x@ +y)@ + (x*1)=x.
5952 [back_demod,1693,demod,5431,5811,5813,5815,5431] ((x*y)+ (x*1))@ =x@ .
6004 [back_demod,78,demod,5431] (((x*y)+x@ )@ +x@ )@ =x*y.
6006 [back_demod,68,demod,5431,5431,5431] (x+ ((x+y)@ + (y+z)@ )@ )@ = (x+y)@ .
6036 [back_demod,5205,demod,5739] (0+0)@ @ =0+0.
6046 [copy,5836,flip.1] (0+0)@ +0= (0+x)@ + ((x+y)*1).
6047 [copy,5837,flip.1] (0+0)@ +0= ((x+y)*1)+ (0+y)@ .
6052 [para_from,5175.1.1,46.1.1.2.1,demod,5176] 0+ (0+ (x* (0+0)))=0+0.
6058 [para_into,5814.1.1,5199.1.1] (x*1)+ (x*1)=x.
6087,6086 [para_into,5512.1.1.1.1.1,5814.1.1] (x@ +0)@ =x*1.
6088 [back_demod,5818,demod,6087] 0+ (x*1)=x.
6106 [para_into,6088.1.1.2,5891.1.1] 0+x=x+x.
6107 [para_into,6088.1.1.2,5430.1.1] 0+x=x+0.
6108 [copy,6106,flip.1] x+x=0+x.
6111,6110 [para_from,6088.1.1,5171.1.1.2] 0+1=1.
6115,6114 [back_demod,5838,demod,6111,flip.1] (0+0)@ +0= (1*1)+1@ .
6116 [back_demod,6047,demod,6115,flip.1] ((x+y)*1)+ (0+y)@ = (1*1)+1@ .
6118 [back_demod,6046,demod,6115,flip.1] (0+x)@ + ((x+y)*1)= (1*1)+1@ .
6121,6120 [back_demod,5868,demod,6115] (0+x)@ +x= (1*1)+1@ .
6122 [back_demod,5834,demod,6121] (0+ (x*y))@ + (x*1)= (1*1)+1@ .
6128 [back_demod,5885,demod,6121] 0+ ((((1*1)+1@ )*x)+ (0*x))=x.
6134 [para_into,6106.1.1,6110.1.1,flip.1] 1+1=1.
6143,6142 [para_from,6134.1.1,5891.1.1.1] 1*1=1.
6150 [back_demod,6128,demod,6143] 0+ (((1+1@ )*x)+ (0*x))=x.
6156 [back_demod,6122,demod,6143] (0+ (x*y))@ + (x*1)=1+1@ .
6160 [back_demod,6118,demod,6143] (0+x)@ + ((x+y)*1)=1+1@ .
6162 [back_demod,6116,demod,6143] ((x+y)*1)+ (0+y)@ =1+1@ .
6190 [para_from,6107.1.1,5171.1.1.2] 0+ ((x*x)+0)=x.
6194 [para_from,6108.1.1,5891.1.1.1] (0+x)*1=x.
6198 [para_from,6108.1.1,5142.1.1.1] (0+x)@ = (x+0)@ .
6201 [para_from,6108.1.1,868.1.1.2.1.1.1] x+ ((0+x)@ +y)@ =x+x.
6207 [copy,6198,flip.1] (x+0)@ = (0+x)@ .
6212 [para_into,6194.1.1.1,5171.1.1,flip.1] 0+ (x*x)=x*1.
6241,6240 [para_from,5738.1.1,6194.1.1.1,demod,5892,flip.1] 0+0=0.
6258 [back_demod,6052,demod,6241,6241] 0+ (0+ (x*0))=0.
6261,6260 [back_demod,6036,demod,6241,6241] 0@ @ =0.
6288 [back_demod,5177,demod,6241] (x*0)+ ((x*x)+0)=x.
6291,6290 [back_demod,5175,demod,6241] 0*x=0.
6304 [back_demod,6150,demod,6291] 0+ (((1+1@ )*x)+0)=x.
6306 [para_into,5173.1.1.2.1,6194.1.1] 0+ (x+ ((0+x)@ *1))=1.
6312 [para_from,5173.1.1,6194.1.1.1,flip.1] (x*y)+ (x@ *y)=y*1.
6314 [para_from,6260.1.1,12.1.1.2.2.1,demod,6261,5134] (x*0)+ ((x*0@ )+0)=x.
6316 [para_from,6260.1.1,5133.1.1.2] 0@ *0=0.
6320 [para_from,6316.1.1,12.1.1.2.2] (x*0@ )+ ((x*0)+0)=x.
6366 [para_from,5812.1.1,12.1.1.2.2.1,demod,5813] (x* (y*1))+ ((x* (0+y@ ))+ ((y*1)* (0+y@ )))=x.
6370 [para_from,5812.1.1,5133.1.1.2] (0+x@ )* (x*1)=0.
6372 [para_from,5812.1.1,5181.1.1.2.1.2,demod,5813,5813,5813] ((x*1)* (0+x@ ))+ (((x*1)* (x*1))+0)=x*1.
6440 [para_from,6058.1.1,5893.1.1.1.2.1] ((x*1)+x@ )@ =0.
6477,6476 [para_from,6190.1.1,6194.1.1.1,flip.1] (x*x)+0=x*1.
6484 [back_demod,6372,demod,6477] ((x*1)* (0+x@ ))+ ((x*1)*1)=x*1.
6490 [back_demod,6288,demod,6477] (x*0)+ (x*1)=x.
6536 [para_into,5191.1.1.1.1,5812.1.1,demod,5813,5813,5813] ((x*1)* (x*1))+ (((x*1)* (0+x@ ))+0)=x*1.
6562 [para_from,6207.1.1,12.1.1.2.2.1] (x* (y+0)@ )+ ((x* (y+0))+ ((0+y)@ * (y+0)))=x.
6583,6582 [para_from,6212.1.1,6194.1.1.1] (x*1)*1=x*x.
6584 [back_demod,6484,demod,6583] ((x*1)* (0+x@ ))+ (x*x)=x*1.
6612 [para_from,6258.1.1,6194.1.1.1,demod,6291,flip.1] 0+ (x*0)=0.
6615,6614 [para_into,6612.1.1,6107.1.1] (x*0)+0=0.
6619,6618 [back_demod,6320,demod,6615] (x*0@ )+0=x.
6620 [back_demod,6314,demod,6619] (x*0)+x=x.
6623,6622 [para_from,6612.1.1,6194.1.1.1,demod,6291,flip.1] x*0=0.
6625,6624 [back_demod,6620,demod,6623] 0+x=x.
6629,6628 [back_demod,6490,demod,6623,6625] x*1=x.
6649,6648 [back_demod,6584,demod,6629,6625,5134,6625,6629] x*x=x.
6664 [back_demod,6562,demod,6625] (x* (y+0)@ )+ ((x* (y+0))+ (y@ * (y+0)))=x.
6679,6678 [back_demod,6536,demod,6629,6629,6649,6629,6625,5134,6625,6629] x+0=x.
6723,6722 [back_demod,6370,demod,6625,6629] x@ *x=0.
6724 [back_demod,6366,demod,6629,6625,6629,6625,5134,6679] (x*y)+ (x*y@ )=x.
6729,6728 [back_demod,6306,demod,6625,6629,6625] x+x@ =1.
6731,6730 [back_demod,6304,demod,6729,6679,6625] 1*x=x.
6748 [back_demod,6201,demod,6625] x+ (x@ +y)@ =x+x.
6752 [back_demod,6162,demod,6629,6625,6729] (x+y)+y@ =1.
6754 [back_demod,6160,demod,6625,6629,6729] x@ + (x+y)=1.
6758 [back_demod,6156,demod,6625,6629,6729] (x*y)@ +x=1.
6761,6760 [back_demod,6108,demod,6625] x+x=x.
6767,6766 [back_demod,5923,demod,6625,6629,6625] x@ + (x+y)@ =x@ .
6769,6768 [back_demod,5812,demod,6625,6629] x@ @ =x.
6772 [back_demod,5788,demod,6679,6767,6625] (x@ *y)+ (x*y)=y.
6813,6812 [back_demod,6440,demod,6629,6729] 1@ =0.
6821,6820 [back_demod,6312,demod,6629] (x*y)+ (x@ *y)=y.
6826 [back_demod,5952,demod,6629] ((x*y)+x)@ =x@ .
6830 [back_demod,5936,demod,6629] (x@ +y)@ +x=x.
6832 [back_demod,5822,demod,6629] (x+ (x*y))@ =x@ .
6858 [back_demod,6664,demod,6679,6679,6679,6723,6679] (x*y@ )+ (x*y)=x.
6860 [back_demod,5870,demod,6761,6761,6679] (x+y)@ +x@ =x@ .
6864 [back_demod,5794,demod,6769,6769,6649,6679] ((x+y@ )@ + (x+y)@ )@ =x.
6872 [back_demod,5698,demod,6761,6679] ((x+y)@ + (x+ (y@ *z))@ )@ =x.
6878 [back_demod,5576,demod,6761,6679] (x+ (y+z)@ )@ + (x+z)@ =x@ .
6882 [back_demod,5574,demod,6761,6679] (x+ (y*z))@ + (x+y@ )@ =x@ .
6890 [back_demod,6748,demod,6761] x+ (x@ +y)@ =x.
6894 [para_into,6752.1.1.2,6768.1.1] (x+y@ )+y=1.
6902 [para_into,6754.1.1.1,6768.1.1] x+ (x@ +y)=1.
6937,6936 [para_from,6826.1.1,6768.1.1.1,demod,6769,flip.1] (x*y)+x=x.
6940 [para_from,6830.1.1,6902.1.1.2] (x@ +y)+x=1.
6950 [para_into,6940.1.1.1.1,6768.1.1] (x+y)+x@ =1.
6960 [para_into,6950.1.1.1,6936.1.1] x+ (x*y)@ =1.
6968 [para_into,5933.1.1.1.2.1.1,6768.1.1,demod,6769] ((x@ *y)+ (x+ (x@ *y))@ )@ =x.
6994 [para_from,6832.1.1,6768.1.1.1,demod,6769,flip.1] x+ (x*y)=x.
7010 [para_from,6772.1.1,5806.1.1.1.2.1,demod,6937,6769] (x+y@ )* (x@ *y)=0.
7014 [para_from,6772.1.1,6754.1.1.2] (x@ *y)@ +y=1.
7016 [para_from,6772.1.1,6752.1.1.1] x+ (y*x)@ =1.
7028 [para_into,7014.1.1.1.1.1,6768.1.1] (x*y)@ +y=1.
7060 [para_from,6820.1.1,5806.1.1.1.2.1,demod,6769,6937] (x@ +y@ )* (x*y)=0.
7072 [para_into,6860.1.1.1.1,6860.1.1,demod,6769,6769,6769] x+ (x+y)=x+y.
7076 [para_from,6860.1.1,6890.1.1.2.1,demod,6769] (x+y)+x=x+y.
7081,7080 [para_into,7072.1.1.2,6820.1.1,demod,6821] (x*y)+y=y.
7092 [para_into,7076.1.1.1,7080.1.1,demod,7081] x+ (y*x)=x.
7128 [para_into,7010.1.1.1.2,6768.1.1] (x+y)* (x@ *y@ )=0.
7134 [para_into,7010.1.1.1,7028.1.1,demod,6769,6731] (x*y@ )*y=0.
7136 [para_into,7010.1.1.1,7016.1.1,demod,6731] x@ * (y*x)=0.
7138 [para_into,7010.1.1.1,6960.1.1,demod,6731] x@ * (x*y)=0.
7140 [para_into,7010.1.1.1,6950.1.1,demod,6731] (x+y)@ *x=0.
7142 [para_into,7010.1.1.1,6894.1.1,demod,6769,6731] (x+y)@ *y=0.
7146 [para_into,7010.1.1.1,6758.1.1,demod,6769,6731] (x@ *y)*x=0.
7152 [para_into,7134.1.1.1.2,6768.1.1] (x*y)*y@ =0.
7156 [para_from,7134.1.1,6820.1.1.1,demod,6625] (x*y@ )@ *y=y.
7161,7160 [para_from,7136.1.1,6820.1.1.2,demod,6679] x* (y*x)=y*x.
7168 [para_from,7138.1.1,6858.1.1.2,demod,6679] x@ * (x*y)@ =x@ .
7170 [para_into,7140.1.1.1.1,6860.1.1,demod,6769] x* (x+y)@ =0.
7174 [para_from,7140.1.1,6820.1.1.2,demod,6679] (x+y)*x=x.
7182 [para_from,7174.1.1,6858.1.1.1] x@ + ((x@ +y)*x)=x@ +y.
7188 [para_from,7174.1.1,6724.1.1.1] x+ ((x+y)*x@ )=x+y.
7192 [para_from,7142.1.1,6820.1.1.2,demod,6679] (x+y)*y=y.
7203,7202 [para_from,7192.1.1,6936.1.1.1] x+ (y+x)=y+x.
7206 [para_from,7192.1.1,6758.1.1.1.1] x@ + (y+x)=1.
7234 [para_into,7146.1.1.1.1,6768.1.1] (x*y)*x@ =0.
7238 [para_from,7146.1.1,6820.1.1.1,demod,6625] (x@ *y)@ *x=x.
7240 [para_from,7152.1.1,6820.1.1.1,demod,6625] (x*y)@ *y@ =y@ .
7246 [para_from,7170.1.1,6858.1.1.1,demod,6625] x* (x+y)=x.
7250 [para_from,7246.1.1,6772.1.1.1] x@ + (x* (x@ +y))=x@ +y.
7252 [para_from,7246.1.1,6820.1.1.1] x+ (x@ * (x+y))=x+y.
7254 [para_from,7246.1.1,6772.1.1.2] (x@ * (x+y))+x=x+y.
7257,7256 [para_into,7206.1.1.1,6768.1.1] x+ (y+x@ )=1.
7258 [para_into,7234.1.1.1,7192.1.1] x* (y+x)@ =0.
7296 [para_from,7258.1.1,6858.1.1.1,demod,6625] x* (y+x)=x.
7304 [para_from,7296.1.1,6820.1.1.2] (x* (y+x@ ))+x@ =y+x@ .
7318 [para_from,7156.1.1,6724.1.1.2,demod,6769,6769] ((x*y)@ *y)+y@ = (x*y)@ .
7326 [para_from,7156.1.1,6724.1.1.1] x+ ((y*x@ )@ *x@ )= (y*x@ )@ .
7344 [para_into,6004.1.1.1.1.1.1,7160.1.1,demod,7161] (((x*y)+y@ )@ +y@ )@ =x*y.
7386 [para_from,7202.1.1,6830.1.1.1.1] (x+y@ )@ +y=y.
7388 [para_from,7202.1.1,6860.1.1.1.1] (x+y)@ +y@ =y@ .
7390 [para_from,7202.1.1,6766.1.1.2.1] x@ + (y+x)@ =x@ .
7396 [para_from,7238.1.1,6858.1.1.1,demod,6769,6769] x@ + ((x*y)@ *x)= (x*y)@ .
7424 [para_into,6006.1.1.1.2.1.1.1,7256.1.1,demod,6813,6625,6769,7257,6813] (x+ ((y+x@ )+z))@ =0.
7527,7526 [para_from,7424.1.1,6752.1.1.2,demod,6679] x+ (y+ ((z+y@ )+u))=1.
7528 [para_from,7424.1.1,7386.1.1.1.1.2,demod,6679,7527,flip.1] x+ ((y+x@ )+z)=1.
7590 [para_into,7528.1.1.2.1.2,6768.1.1] x@ + ((y+x)+z)=1.
7614 [para_from,7590.1.1,7128.1.1.1,demod,6769,6731] x* ((y+x)+z)@ =0.
7668 [para_into,6864.1.1.1.1.1.2,6768.1.1] ((x+y)@ + (x+y@ )@ )@ =x.
7676 [para_into,6864.1.1.1.1,6864.1.1] (x+ ((x+y@ )@ + (x+y))@ )@ = (x+y@ )@ .
7694 [para_into,6864.1.1.1.2.1,6858.1.1] (((x*y@ )+ (x*y)@ )@ +x@ )@ =x*y@ .
7698 [para_into,6864.1.1.1.2.1,6772.1.1] (((x@ *y)+ (x*y)@ )@ +y@ )@ =x@ *y.
7811,7810 [para_from,7614.1.1,6858.1.1.1,demod,6625] x* ((y+x)+z)=x.
7822 [para_into,7810.1.1.2.1,7076.1.1] x* ((x+y)+z)=x.
7830 [para_into,7810.1.1.2,7202.1.1] x* (y+ (z+x))=x.
7832 [para_from,7810.1.1,7160.1.1.2,demod,7811] ((x+y)+z)*y=y.
7836 [para_from,7810.1.1,7092.1.1.2] ((x+y)+z)+y= (x+y)+z.
7859,7858 [para_from,7822.1.1,7092.1.1.2] ((x+y)+z)+x= (x+y)+z.
7879,7878 [para_into,7830.1.1.2.2,7390.1.1] (x+y)@ * (z+y@ )= (x+y)@ .
7883,7882 [para_into,7830.1.1.2.2,7092.1.1] (x*y)* (z+y)=x*y.
7953,7952 [para_into,6872.1.1.1.1.1,7016.1.1,demod,6813,6769,6625,6769] x+ ((y*x)*z)=x.
7966 [para_into,6872.1.1.1.1.1,6820.1.1] (x@ + ((y*x)+ ((y@ *x)@ *z))@ )@ =y*x.
7982 [para_into,6872.1.1.1.2.1.2,7240.1.1] ((x+ (y*z))@ + (x+z@ )@ )@ =x.
8003,8002 [para_into,6872.1.1.1.2.1,6820.1.1,demod,6937] (x@ +y@ )@ =x*y.
8018 [back_demod,7982,demod,8003] (x+ (y*z))* (x+z@ )=x.
8026 [back_demod,7966,demod,8003] x* ((y*x)+ ((y@ *x)@ *z))=y*x.
8040 [back_demod,7698,demod,8003] ((x@ *y)+ (x*y)@ )*y=x@ *y.
8044 [back_demod,7694,demod,8003] ((x*y@ )+ (x*y)@ )*x=x*y@ .
8046 [back_demod,7668,demod,8003] (x+y)* (x+y@ )=x.
8068 [back_demod,7344,demod,8003] ((x*y)+y@ )*y=x*y.
8115 [para_into,7832.1.1.1.1,7092.1.1] (x+y)* (z*x)=z*x.
8117 [para_into,7832.1.1.1.1,6994.1.1] (x+y)* (x*z)=x*z.
8206,8205 [para_into,7952.1.1.2,7160.1.1] x+ (y* (z*x))=x.
8219 [para_from,7952.1.1,7202.1.1.2,demod,7953] ((x*y)*z)+y=y.
8313 [para_from,8205.1.1,7202.1.1.2,demod,8206] (x* (y*z))+z=z.
8386,8385 [para_into,6878.1.1.2.1,7386.1.1,demod,8003,6769] ((x+y@ )* (z+y))+y@ =x+y@ .
8389 [para_into,6878.1.1.2.1,7080.1.1] ((x*y)+ (z+y)@ )@ +y@ = (x*y)@ .
8436,8435 [para_into,8219.1.1.1.1,7246.1.1] (x*y)+ (x+z)=x+z.
8442,8441 [para_into,8219.1.1.1.1,7168.1.1] (x@ *y)+ (x*z)@ = (x*z)@ .
8448,8447 [back_demod,8040,demod,8442] (x*y)@ *y=x@ *y.
8449 [back_demod,7326,demod,8448,flip.1] (x*y@ )@ =y+ (x@ *y@ ).
8452,8451 [back_demod,7318,demod,8448,flip.1] (x*y)@ = (x@ *y)+y@ .
8470 [back_demod,7,demod,8452,6769,8452,6769,6769,8452,6769,6769] B*A!=A*B| (A*B)*C!=A* (B*C)| ((A@ *B@ )+B)* ((A*B@ )+B)!=B| (A*B@ )+B!=A+B|$Ans(Huntington_axioms_and).
8472,8471 [back_demod,8449,demod,8452,6769] (x@ *y@ )+y=y+ (x@ *y@ ).
8487 [back_demod,8389,demod,8452] ((x*y)+ (z+y)@ )@ +y@ = (x@ *y)+y@ .
8533 [back_demod,8044,demod,8452] ((x*y@ )+ ((x@ *y)+y@ ))*x=x*y@ .
8537 [back_demod,8026,demod,8452,6769] x* ((y*x)+ (((y*x)+x@ )*z))=y*x.
8599 [back_demod,7396,demod,8452,8452] x@ + (((x@ *y)+y@ )*x)= (x@ *y)+y@ .
8634 [back_demod,8470,demod,8472] B*A!=A*B| (A*B)*C!=A* (B*C)| (B+ (A@ *B@ ))* ((A*B@ )+B)!=B| (A*B@ )+B!=A+B|$Ans(Huntington_axioms_and).
8700,8699 [para_into,8313.1.1.1.2,7296.1.1] (x*y)+ (z+y)=z+y.
8704,8703 [back_demod,8533,demod,8700] ((x@ *y)+y@ )*x=x*y@ .
8708,8707 [back_demod,8599,demod,8704,flip.1] (x@ *y)+y@ =x@ + (x*y@ ).
8784 [back_demod,8487,demod,8708] ((x*y)+ (z+y)@ )@ +y@ =x@ + (x*y@ ).
8794,8793 [back_demod,8451,demod,8708] (x*y)@ =x@ + (x*y@ ).
9050 [para_into,6882.1.1.1.1,6772.1.1,demod,6937,6769,8794,6769] x@ +y=y+ (y@ *x@ ).
9080 [copy,9050,flip.1] x+ (x@ *y@ )=y@ +x.
9247 [para_into,8002.1.1.1.1,8002.1.1] ((x*y)+z@ )@ = (x@ +y@ )*z.
9250,9249 [para_into,8002.1.1.1.1,6768.1.1] (x+y@ )@ =x@ *y.
9271 [back_demod,8784,demod,9250,8794] ((x@ + (x*y@ ))* (z+y))+y@ =x@ + (x*y@ ).
9299 [back_demod,6968,demod,9250,8794,6769] (x+ (x@ *y@ ))* (x+ (x@ *y))=x.
9302,9301 [back_demod,9247,demod,9250,8794] (x@ + (x*y@ ))*z= (x@ +y@ )*z.
9406,9405 [back_demod,7676,demod,9250,8700,9250,9250] x@ * (x+y)=x@ *y.
9474,9473 [back_demod,9271,demod,9302,8386,flip.1] x@ + (x*y@ )=x@ +y@ .
9522 [back_demod,7254,demod,9406] (x@ *y)+x=x+y.
9525,9524 [back_demod,7252,demod,9406] x+ (x@ *y)=x+y.
9630,9629 [back_demod,8793,demod,9474] (x*y)@ =x@ +y@ .
9655 [back_demod,9299,demod,9525,9525] (x+y@ )* (x+y)=x.
9679 [back_demod,9080,demod,9525] x+y@ =y@ +x.
9689 [para_into,9679.1.1.2,6768.1.1,demod,6769] x+y=y+x.
9738 [para_into,8046.1.1.1,9689.1.1] (x+y)* (y+x@ )=y.
9760 [para_into,8046.1.1.1,7388.1.1,demod,6769] x@ * ((y+x)@ +x)= (y+x)@ .
9775,9774 [para_into,8046.1.1.1,6820.1.1,demod,9630,6769,8436] x* (y+x@ )=y*x.
9777,9776 [para_into,8046.1.1.1,6724.1.1,demod,9630,6769,8700] x* (x@ +y)=x*y.
9790 [para_into,8046.1.1.2,7080.1.1] ((x*y@ )+y)*y@ =x*y@ .
9792 [para_into,8046.1.1.2,6860.1.1] ((x+y)@ +x)*x@ = (x+y)@ .
9796,9795 [back_demod,7304,demod,9775] (x*y)+y@ =x+y@ .
9797 [back_demod,7250,demod,9777] x@ + (x*y)=x@ +y.
9833 [back_demod,8537,demod,9796] x* ((y*x)+ ((y+x@ )*z))=y*x.
9838,9837 [back_demod,8068,demod,9796] (x+y@ )*y=x*y.
9899,9898 [para_from,8046.1.1,6772.1.1.2,demod,7879] (x+y)@ +x=x+y@ .
9901,9900 [back_demod,9792,demod,9899,flip.1] (x+y)@ = (x+y@ )*x@ .
9920 [back_demod,9760,demod,9901,9901] x@ * (((y+x@ )*y@ )+x)= (y+x@ )*y@ .
10282 [para_into,7182.1.1.2.1,9689.1.1,demod,9838] x@ + (y*x)=x@ +y.
10404 [para_from,9629.1.1,6768.1.1.1,demod,9901,6769,6769] (x@ +y)*x=x*y.
10457,10456 [para_into,9655.1.1.2,9689.1.1] (x+y@ )* (y+x)=x.
10491,10490 [para_from,9738.1.1,6772.1.1.2,demod,9901,7883] ((x+y@ )*x@ )+y=y+x@ .
10495,10494 [back_demod,9920,demod,10491,9406,flip.1] (x+y@ )*x@ =y@ *x@ .
10684,10683 [back_demod,9900,demod,10495] (x+y)@ =y@ *x@ .
10688 [para_into,9774.1.1.2,9689.1.1,demod,9777] x*y=y*x.
10690 [back_unit_del,10688.1,8634.1] (A*B)*C!=A* (B*C)| (B+ (A@ *B@ ))* ((A*B@ )+B)!=B| (A*B@ )+B!=A+B|$Ans(Huntington_axioms_and).
10707,10706 [para_from,9774.1.1,9522.1.1.1,demod,6769,7203] (x*y@ )+y=x+y.
10721 [back_demod,10690,demod,10707,10707,unit_del,1] (A*B)*C!=A* (B*C)| (B+ (A@ *B@ ))* (A+B)!=B|$Ans(Huntington_axioms_and).
10723,10722 [back_demod,9790,demod,10707] (x+y)*y@ =x*y@ .
10725,10724 [para_into,7188.1.1.2.1,9689.1.1,demod,10723] x+ (y*x@ )=x+y.
10754 [back_demod,10721,demod,10725,10457,unit_del,1] (A*B)*C!=A* (B*C)|$Ans(Huntington_axioms_and).
10853 [para_into,10754.1.1.1,10688.1.1] (B*A)*C!=A* (B*C)|$Ans(Huntington_axioms_and).
10855 [para_into,10853.1.1,10688.1.1] C* (B*A)!=A* (B*C)|$Ans(Huntington_axioms_and).
11072,11071 [para_from,10683.1.1,6722.1.1.1] (x@ *y@ )* (y+x)=0.
11288 [para_into,7836.1.1.1.1,9689.1.1,demod,7859] (x+y)+z= (y+x)+z.
12135 [para_into,9405.1.1.2,9689.1.1] x@ * (y+x)=x@ *y.
12196,12195 [para_into,9797.1.1.2,7060.1.1,demod,10684,6769,6769,6679,10684,6769,6769,flip.1] (x*y)+ (y*x)=x*y.
12431 [para_into,11288.1.1,9689.1.1] x+ (y+z)= (z+y)+x.
14061 [para_into,12431.1.1.2,12195.1.1,demod,12196] x+ (y*z)= (z*y)+x.
14075 [para_from,12431.1.1,10404.1.1.1,demod,9838] (x+y)*z=z* (y+x).
14082 [copy,14075,flip.1] x* (y+z)= (z+y)*x.
15440 [para_into,8018.1.1.1,9689.1.1] ((x*y)+z)* (z+y@ )=z.
15505,15504 [para_from,8018.1.1,10282.1.1.2,demod,10684,6769,10707,10684,6769,flip.1] (x*y@ )+ (y+ (z*x))=x+y.
21251 [para_into,15440.1.1.2,9689.1.1] ((x*y)+z)* (y@ +z)=z.
52892 [para_from,15504.1.1,7202.1.1.2,demod,15505] (x+ (y*z))+ (z+x)=z+x.
53705 [para_from,52892.1.1,12135.1.1.2,demod,10684,11072,10684,flip.1] (x@ *y@ )* (x+ (z*y))=0.
63199 [para_into,53705.1.1.1.1,6768.1.1] (x*y@ )* (x@ + (z*y))=0.
74463 [para_into,9833.1.1.2.2,8117.1.1] x* ((y*x)+ (y*z))=y*x.
74465 [para_into,9833.1.1.2.2,8115.1.1] x* ((y*x)+ (z*y))=y*x.
78003 [para_into,63199.1.1.2.2,21251.1.1,demod,10684,6769] (x* (y@ *z))* (x@ +y)=0.
85557 [para_into,74463.1.1.2,14061.1.1] x* ((y*z)+ (z*x))=z*x.
86229 [para_into,74465.1.1,14082.1.1] ((x*y)+ (y*z))*z=y*z.
90409 [para_into,78003.1.1.1.2.1,6768.1.1] (x* (y*z))* (x@ +y@ )=0.
114781 [para_from,90409.1.1,10282.1.1.2,demod,10684,6769,6769,6679,10684,6769,6769,flip.1] (x*y)+ (y* (x*z))=x*y.
119073 [para_from,114781.1.1,85557.1.1.2] (x*y)* (x*z)=z* (x*y).
119082,119081 [para_from,114781.1.1,86229.1.1.1] (x*y)* (x*z)=y* (x*z).
119505 [copy,119073,flip.1,demod,119082] x* (y*z)=z* (y*x).
119506 [binary,119505.1,10855.1] $Ans(Huntington_axioms_and).

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