----- Otter 3.0.6, Feb 2000 -----
----> UNIT CONFLICT at   3.69 sec ----> 3325 [binary,3323.1,2257.1] $Ans(Robbins_plus_and).

Length of proof is 319.  Level of proof is 48.

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

318 [] x=x.
320,319 [] (((x*x@ )+ ((x*y)+ (x@ *y)))* ((((z+ (u+v)@ )@ + (z+v)@ )@ *w@ )+ ((((z+ (u+v)@ )@ + (z+v)@ )@ *z)+ (w@ *z)))@ )+ ((((x*x@ )+ ((x*y)+ (x@ *y)))*z)+ (((((z+ (u+v)@ )@ + (z+v)@ )@ *w@ )+ ((((z+ (u+v)@ )@ + (z+v)@ )@ *z)+ (w@ *z)))@ *z))=y.
321 [] (A+B)+C!=A+ (B+C)|A+B!=B+A| ((A+B)@ + (A+B@ )@ )@ !=A| (A@ +B@ )@ !=A*B|$Ans(Robbins_plus_and).
322 [copy,321,flip.2] (A+B)+C!=A+ (B+C)|B+A!=A+B| ((A+B)@ + (A+B@ )@ )@ !=A| (A@ +B@ )@ !=A*B|$Ans(Robbins_plus_and).
324,323 [para_into,319.1.1.1.1,319.1.1,demod,320] (x* ((((y+ (z+u)@ )@ + (y+u)@ )@ *v@ )+ ((((y+ (z+u)@ )@ + (y+u)@ )@ *y)+ (v@ *y)))@ )+ ((x*y)+ (((((y+ (z+u)@ )@ + (y+u)@ )@ *v@ )+ ((((y+ (z+u)@ )@ + (y+u)@ )@ *y)+ (v@ *y)))@ *y))=x.
326,325 [back_demod,319,demod,324] (x*x@ )+ ((x*y)+ (x@ *y))=y.
327 [para_into,323.1.1.1.2.1,323.1.1,demod,324] (x* ((y+ (z+u)@ )@ + (y+u)@ )@ @ )+ ((x*y)+ (((y+ (z+u)@ )@ + (y+u)@ )@ @ *y))=x.
330,329 [para_into,325.1.1,323.1.1] (((x+ (y+z)@ )@ + (x+z)@ )@ *u@ )+ ((((x+ (y+z)@ )@ + (x+z)@ )@ *x)+ (u@ *x))=x.
331 [back_demod,323,demod,330,330] (x*y@ )+ ((x*y)+ (y@ *y))=x.
340,339 [para_into,327.1.1,325.1.1,flip.1] ((x+ (y+z)@ )@ + (x+z)@ )@ =x.
343 [back_demod,329,demod,340,340] (x*y@ )+ ((x*x)+ (y@ *x))=x.
345 [para_into,339.1.1.1.1.1.2.1,331.1.1] ((x+y@ )@ + (x+ ((y*z)+ (z@ *z)))@ )@ =x.
347 [para_into,339.1.1.1.1.1.2.1,325.1.1] ((x+y@ )@ + (x+ ((z*y)+ (z@ *y)))@ )@ =x.
350,349 [para_into,339.1.1.1.1.1.2,339.1.1] ((x+y)@ + (x+ (y+z)@ )@ )@ =x.
351 [para_into,339.1.1.1.1,339.1.1] (x+ ((x+ (y+z)@ )@ +z)@ )@ = (x+ (y+z)@ )@ .
355 [para_into,339.1.1.1.2.1,325.1.1] (((x*x@ )+ (y+ ((x*z)+ (x@ *z)))@ )@ +z@ )@ =x*x@ .
357 [para_into,339.1.1.1.2,339.1.1] (((x+ (y+z)@ )@ + (u+ (x+z)@ )@ )@ +x)@ = (x+ (y+z)@ )@ .
359 [para_from,339.1.1,331.1.1.2.2.1,demod,340] (x*y)+ ((x* ((y+ (z+u)@ )@ + (y+u)@ ))+ (y* ((y+ (z+u)@ )@ + (y+u)@ )))=x.
361 [para_from,339.1.1,325.1.1.2.2.1,demod,340] (((x+ (y+z)@ )@ + (x+z)@ )*x)+ ((((x+ (y+z)@ )@ + (x+z)@ )*u)+ (x*u))=u.
364,363 [para_into,343.1.1.1.2,339.1.1,demod,340] (x*y)+ ((x*x)+ (y*x))=x.
405 [para_into,347.1.1.1.2.1,325.1.1] (((x*x@ )+y@ )@ +y@ )@ =x*x@ .
423 [para_into,349.1.1.1.2.1.2.1,325.1.1] ((x+ (y*y@ ))@ + (x+z@ )@ )@ =x.
425 [para_into,349.1.1.1.2.1.2,349.1.1] ((x+ (y+z)@ )@ + (x+y)@ )@ =x.
428,427 [para_into,349.1.1.1.2,349.1.1] (((x+y)@ +x)@ +x)@ = (x+y)@ .
430,429 [para_into,359.1.1,325.1.1] (x@ + (y+z)@ )@ + (x@ +z)@ =x.
431 [para_from,359.1.1,349.1.1.1.2.1.2.1] ((x+ (y*z))@ + (x+y@ )@ )@ =x.
433 [para_into,405.1.1.1.1.1.2,349.1.1,demod,350] (((x*x@ )+y)@ +y)@ =x*x@ .
436,435 [para_into,423.1.1.1.2.1.2,423.1.1] ((x+ (y*y@ ))@ + (x+z)@ )@ =x.
438,437 [para_into,425.1.1.1.1.1.2.1,363.1.1] ((x+y@ )@ + (x+ (y*z))@ )@ =x.
442,441 [para_into,425.1.1.1.1,349.1.1] (x+ ((x+y)@ +x)@ )@ = (x+y)@ .
444,443 [para_from,425.1.1,357.1.1.1.1,flip.1] (x+ ((x+y)@ +y)@ )@ = (x+x)@ .
451 [para_into,429.1.1.1.1.1,427.1.1,demod,428,430,flip.1] ((x+y)@ +x)@ +x=x+y.
459 [para_into,429.1.1.1,349.1.1] x+ ((x+y)@ + (y+z)@ )@ =x+y.
463 [para_into,433.1.1.1.1.1,325.1.1] (x@ + ((y*x)+ (y@ *x)))@ =y*y@ .
471 [para_into,441.1.1.1.2.1.1.1,363.1.1,demod,364] ((x*y)+ (x@ + (x*y))@ )@ =x@ .
473 [para_into,441.1.1.1.2.1.1.1,325.1.1,demod,326] ((x*x@ )+ (y@ + (x*x@ ))@ )@ =y@ .
479 [para_from,441.1.1,429.1.1.1] (x@ +y)@ + (x@ +x@ )@ =x.
481 [para_from,441.1.1,339.1.1.1.1] ((x+y)@ + (x+x)@ )@ =x.
484,483 [para_from,441.1.1,429.1.1.2.1.1,demod,442,430,flip.1] x+ ((x+y)@ +x)@ =x+y.
485 [para_from,443.1.1,429.1.1.1] (x@ +x@ )@ + (x@ +y)@ =x.
490,489 [para_from,443.1.1,339.1.1.1.1] ((x+x)@ + (x+y)@ )@ =x.
491 [para_from,443.1.1,429.1.1.2.1.1,demod,444,430,flip.1] x+ ((x+y)@ +y)@ =x+x.
505 [para_from,471.1.1,425.1.1.1.1] (x@ + ((x*y)+x@ )@ )@ =x*y.
509 [para_from,471.1.1,339.1.1.1.1] (x@ + ((x*y)+ (x*y))@ )@ =x*y.
511 [para_into,473.1.1.1.2.1.1,437.1.1,demod,438] ((x*x@ )+ (y+ (x*x@ ))@ )@ =y.
513 [para_into,479.1.1.1,463.1.1] (x*x@ )+ (y@ +y@ )@ =y.
515 [para_into,479.1.1.1,435.1.1,demod,436] x+x=x+ (y*y@ ).
518 [copy,515,flip.1] x+ (y*y@ )=x+x.
519 [para_into,481.1.1.1.1,435.1.1,demod,436] (x+x)@ = (x+ (y*y@ ))@ .
523 [para_from,481.1.1,479.1.1.2] ((x+x)@ +y)@ +x=x+x.
525 [para_from,481.1.1,351.1.1.1.2,flip.1] (x+ (y+ (x+x)@ )@ )@ = (x+x)@ .
532,531 [para_into,485.1.1.1,481.1.1] x+ ((x+x)@ +y)@ =x+x.
540,539 [para_from,505.1.1,485.1.1.2] (x@ +x@ )@ + (x*y)=x.
541 [para_from,505.1.1,479.1.1.1] (x*y)+ (x@ +x@ )@ =x.
546,545 [para_from,511.1.1,433.1.1.1.1] (x+ (x+ (y*y@ ))@ )@ =y*y@ .
550,549 [para_from,511.1.1,425.1.1.1.1.1.2] ((x+y)@ + (x+ (z*z@ ))@ )@ =x.
552 [para_into,513.1.1.2,489.1.1] (x*x@ )+y=y+y.
553 [para_into,513.1.1.2,435.1.1] (x*x@ )+y=y+ (z*z@ ).
555 [copy,552,flip.1] x+x= (y*y@ )+x.
559 [para_into,515.1.1,515.1.1] x+ (y*y@ )=x+ (z*z@ ).
562 [para_from,515.1.1,511.1.1.1.2.1,demod,546] x*x@ =y*y@ .
563 [para_from,515.1.1,509.1.1.1.2.1] (x@ + ((x*y)+ (z*z@ ))@ )@ =x*y.
565 [para_from,515.1.1,489.1.1.1] ((x+x)@ + (y*y@ ))@ =x.
578,577 [para_from,518.1.1,511.1.1.1.2.1] ((x*x@ )+ (y+y)@ )@ =y.
583 [para_from,519.1.1,479.1.1.1.1.1,demod,490] ((x+ (y*y@ ))@ +z)@ +x=x+x.
586 [para_into,523.1.1.1,509.1.1] ((x+x)*y)+x=x+x.
588 [para_from,523.1.1,355.1.1.1.1.1.2.1,demod,578] (((x*y)+ (x@ *y))+y@ )@ =x*x@ .
590 [para_from,523.1.1,351.1.1.1.2.1,demod,490,flip.1] ((x+x)@ + (y+x)@ )@ =x.
592 [para_into,525.1.1.1.2.1.2,435.1.1,demod,550] ((x+ (y*y@ ))@ + (z+x)@ )@ =x.
594 [para_from,525.1.1,459.1.1.2.1.1,demod,532,flip.1] x+ (y+ (x+x)@ )@ =x+x.
597,596 [para_into,531.1.1.2,509.1.1] x+ ((x+x)*y)=x+x.
612 [para_into,545.1.1.1.2.1,518.1.1] (x+ (x+x)@ )@ =y*y@ .
613 [copy,612,flip.1] x*x@ = (y+ (y+y)@ )@ .
624 [para_from,552.1.1,433.1.1.1.1.1] ((x+x)@ +x)@ =y*y@ .
629,628 [para_into,553.1.1,325.1.1,flip.1] ((x*y)+ (x@ *y))+ (z*z@ )=y.
632 [para_into,555.1.1,555.1.1] (x*x@ )+y= (z*z@ )+y.
635 [para_from,555.1.1,509.1.1.1.2.1] (x@ + ((y*y@ )+ (x*z))@ )@ =x*z.
637 [para_from,555.1.1,541.1.1.2.1] (x*y)+ ((z*z@ )+x@ )@ =x.
641 [para_from,555.1.1,485.1.1.1.1] ((x*x@ )+y@ )@ + (y@ +z)@ =y.
646 [para_from,555.1.1,489.1.1.1.1.1] (((x*x@ )+y)@ + (y+z)@ )@ =y.
653,652 [para_from,555.1.1,481.1.1.1.2.1] ((x+y)@ + ((z*z@ )+x)@ )@ =x.
672 [para_from,565.1.1,562.1.1.2] ((x+x)@ + (y*y@ ))*x=z*z@ .
683 [para_from,577.1.1,518.1.1.2.2] x+ (((y*y@ )+ (z+z)@ )*z)=x+x.
685 [para_from,577.1.1,552.1.1.1.2] (((x*x@ )+ (y+y)@ )*y)+z=z+z.
686 [copy,683,flip.1] x+x=x+ (((y*y@ )+ (z+z)@ )*z).
688 [copy,685,flip.1] x+x= (((y*y@ )+ (z+z)@ )*z)+x.
691 [para_into,586.1.1.1.1,555.1.1] (((x*x@ )+y)*z)+y=y+y.
696,695 [para_from,588.1.1,549.1.1.1.1,demod,629] ((x*x@ )+y@ )@ = (x*y)+ (x@ *y).
698,697 [para_from,588.1.1,435.1.1.1.2,demod,629] (x@ + (y*y@ ))@ = (y*x)+ (y@ *x).
703 [back_demod,641,demod,696] ((x*y)+ (x@ *y))+ (y@ +z)@ =y.
707 [back_demod,637,demod,696] (x*y)+ ((z*x)+ (z@ *x))=x.
710,709 [back_demod,577,demod,696] (x* (y+y))+ (x@ * (y+y))=y.
711 [para_into,590.1.1.1.1.1,555.1.1] (((x*x@ )+y)@ + (z+y)@ )@ =y.
716 [para_from,590.1.1,339.1.1.1.1.1.2] ((x+y)@ + (x+ (z+y)@ )@ )@ =x.
724,723 [para_into,592.1.1,563.1.1] ((x*x@ )+ (y*y@ ))*z=x*x@ .
733 [para_from,612.1.1,483.1.1.2.1.1] x+ ((y*y@ )+x)@ =x+ (x+x)@ .
739 [copy,733,flip.1] x+ (x+x)@ =x+ ((y*y@ )+x)@ .
746 [para_from,613.1.1,596.1.1.2] x+ (y+ (y+y)@ )@ =x+x.
747 [para_from,613.1.1,586.1.1.1] (x+ (x+x)@ )@ +y=y+y.
751 [para_from,613.1.1,539.1.1.2] (x@ +x@ )@ + (y+ (y+y)@ )@ =x.
753 [para_from,613.1.1,553.1.1.1] (x+ (x+x)@ )@ +y=y+ (z*z@ ).
754 [copy,746,flip.1] x+x=x+ (y+ (y+y)@ )@ .
755 [copy,747,flip.1] x+x= (y+ (y+y)@ )@ +x.
757 [copy,753,flip.1] x+ (y*y@ )= (z+ (z+z)@ )@ +x.
760 [para_from,624.1.1,437.1.1.1.1,demod,540,696] (x*y)+ (x@ *y)= (y@ +y@ )@ .
762 [para_into,632.1.1.1,613.1.1] (x+ (x+x)@ )@ +y= (z*z@ )+y.
764 [para_into,646.1.1.1.2.1,541.1.1] (((x*x@ )+ (y*z))@ +y@ )@ =y*z.
780 [para_into,691.1.1.1.1.1,613.1.1] (((x+ (x+x)@ )@ +y)*z)+y=y+y.
785 [para_into,703.1.1.1,685.1.1,demod,696,710,696,710] ((x*x)+ (x*x))+ (x@ +y)@ =x.
787 [para_into,707.1.1.2.1,672.1.1,demod,698,710] (x*y)+ ((z*z@ )+ (x*x))=x.
796,795 [para_into,709.1.1.1,672.1.1,demod,698,710] (x*x@ )+ ((y+y)* (y+y))=y.
813 [para_from,716.1.1,429.1.1.1] x+ ((x+y)@ + (z+y)@ )@ =x+y.
849,848 [para_into,760.1.1,685.1.1,demod,696,710,696,710,flip.1] (x@ +x@ )@ = (x*x)+ (x*x).
851 [back_demod,760,demod,849] (x*y)+ (x@ *y)= (y*y)+ (y*y).
852 [back_demod,751,demod,849] ((x*x)+ (x*x))+ (y+ (y+y)@ )@ =x.
863,862 [para_into,764.1.1.1.1.1,596.1.1,demod,849,724,724,724] (x*x@ )+ (x*x@ )=x*x@ .
867,866 [para_into,764.1.1,481.1.1,demod,863,flip.1] (x*x@ )*y=x*x@ .
869,868 [para_from,764.1.1,583.1.1.1,demod,863] (x*x@ )+ (y*y@ )=y*y@ .
882 [para_into,795.1.1.1,613.1.1] (x+ (x+x)@ )@ + ((y+y)* (y+y))=y.
888 [para_into,795.1.1.2.2,555.1.1] (x*x@ )+ ((y+y)* ((z*z@ )+y))=y.
897,896 [para_from,795.1.1,711.1.1.1.2.1,demod,796,849] (x*x)+ (x*x)= (x+x)* (x+x).
898 [para_from,795.1.1,691.1.1,demod,897,flip.1] ((x+x)+ (x+x))* ((x+x)+ (x+x))=x.
905 [para_from,795.1.1,437.1.1.1.2.1,demod,696,710] (x+x@ )@ =y*y@ .
906 [para_from,795.1.1,431.1.1.1.1.1,demod,696,710] (x@ +x)@ =y*y@ .
915 [back_demod,852,demod,897] ((x+x)* (x+x))+ (y+ (y+y)@ )@ =x.
918,917 [back_demod,851,demod,897] (x*y)+ (x@ *y)= (y+y)* (y+y).
920,919 [back_demod,848,demod,897] (x@ +x@ )@ = (x+x)* (x+x).
922,921 [back_demod,785,demod,897] ((x+x)* (x+x))+ (x@ +y)@ =x.
924 [copy,905,flip.1] x*x@ = (y+y@ )@ .
926 [back_demod,697,demod,918] (x@ + (y*y@ ))@ = (x+x)* (x+x).
929,928 [back_demod,695,demod,918] ((x*x@ )+y@ )@ = (y+y)* (y+y).
932 [para_into,866.1.1.1,613.1.1] (x+ (x+x)@ )@ *y=z*z@ .
933 [copy,932,flip.1] x*x@ = (y+ (y+y)@ )@ *z.
934 [para_into,868.1.1.1,613.1.1] (x+ (x+x)@ )@ + (y*y@ )=y*y@ .
952,951 [para_from,898.1.1,596.1.1.2,flip.1] (x+x)+ (x+x)= (x+x)+x.
954,953 [para_from,898.1.1,586.1.1.1,demod,952,flip.1] (x+x)+x=x+ (x+x).
956,955 [para_from,898.1.1,635.1.1.1.2.1.2,demod,952,954,653,952,954,952,954,flip.1] (x+ (x+x))* (x+ (x+x))=x.
959,958 [back_demod,951,demod,954] (x+x)+ (x+x)=x+ (x+x).
976,975 [para_from,905.1.1,483.1.1.2.1.1] x+ ((y*y@ )+x)@ =x+x@ .
978,977 [para_from,905.1.1,451.1.1.1.1.1] ((x*x@ )+y)@ +y=y+y@ .
985,984 [back_demod,739,demod,976] x+ (x+x)@ =x+x@ .
998,997 [back_demod,934,demod,985] (x+x@ )@ + (y*y@ )=y*y@ .
999 [back_demod,933,demod,985] x*x@ = (y+y@ )@ *z.
1001 [back_demod,915,demod,985] ((x+x)* (x+x))+ (y+y@ )@ =x.
1004,1003 [back_demod,882,demod,985] (x+x@ )@ + ((y+y)* (y+y))=y.
1035 [back_demod,780,demod,985] (((x+x@ )@ +y)*z)+y=y+y.
1038 [back_demod,762,demod,985] (x+x@ )@ +y= (z*z@ )+y.
1041 [back_demod,757,demod,985] x+ (y*y@ )= (z+z@ )@ +x.
1043 [back_demod,755,demod,985] x+x= (y+y@ )@ +x.
1044 [back_demod,754,demod,985] x+x=x+ (y+y@ )@ .
1045 [back_demod,753,demod,985] (x+x@ )@ +y=y+ (z*z@ ).
1047 [back_demod,747,demod,985] (x+x@ )@ +y=y+y.
1067 [para_from,906.1.1,451.1.1.1.1.1,demod,929,flip.1] x@ +x= ((x+x)* (x+x))+x@ .
1079 [para_from,924.1.1,652.1.1.1.2.1.1] ((x+y)@ + ((z+z@ )@ +x)@ )@ =x.
1081 [para_from,924.1.1,549.1.1.1.2.1.2] ((x+y)@ + (x+ (z+z@ )@ )@ )@ =x.
1092 [para_from,924.1.1,787.1.1.1] (x+x@ )@ + ((y*y@ )+ (z*z))=z.
1096 [para_from,924.1.1,646.1.1.1.1.1.1] (((x+x@ )@ +y)@ + (y+z)@ )@ =y.
1099 [para_into,926.1.1.1.2,924.1.1] (x@ + (y+y@ )@ )@ = (x+x)* (x+x).
1102,1101 [para_into,928.1.1.1.1,924.1.1] ((x+x@ )@ +y@ )@ = (y+y)* (y+y).
1136,1135 [para_into,975.1.1.2,928.1.1,flip.1] x@ +x@ @ =x@ + ((x+x)* (x+x)).
1139 [para_into,977.1.1.1.1,491.1.1,demod,869,978,978,978,1136,1004] (x*x@ )@ + (y+y@ )@ =y+y@ .
1146 [para_into,999.1.1,999.1.1] (x+x@ )@ *y= (z+z@ )@ *u.
1177,1176 [para_into,1001.1.1,586.1.1] (x+x@ )@ + (x+x@ )@ = (x+x@ )@ .
1181,1180 [para_from,1003.1.1,481.1.1.1.1.1,demod,1177] (x@ + (y+y@ )@ @ )@ = (y+y@ )@ .
1188,1187 [para_from,1038.1.1,491.1.1.2.1.1.1,demod,978,1177] (x+x@ )@ + (y+y@ )@ = (x+x@ )@ .
1191 [para_into,1041.1.1.2,924.1.1] x+ (y+y@ )@ = (z+z@ )@ +x.
1194 [copy,1191,flip.1] (x+x@ )@ +y=y+ (z+z@ )@ .
1196 [para_from,1041.1.1,583.1.1.1.1.1.1] (((x+x@ )@ +y)@ +z)@ +y=y+y.
1209 [para_from,1043.1.1,955.1.1.1.2] (x+ ((y+y@ )@ +x))* (x+ (x+x))=x.
1211 [para_from,1043.1.1,953.1.1.1] ((x+x@ )@ +y)+y=y+ (y+y).
1223,1222 [para_into,1044.1.1,896.1.1,flip.1] (x*x)+ (y+y@ )@ = (x+x)* (x+x).
1251,1250 [para_into,1067.1.1.1,905.1.1,demod,1223,959,959,956] (x*x@ )+ (y+y@ )=y+y@ .
1255,1254 [para_into,1067.1.1,1047.1.1,demod,1223,959,959,956] (x+x@ )+ (x+x@ )=x+x@ .
1257,1256 [para_into,1067.1.1,1038.1.1,demod,1251,1255,1255,1223,1255,1255,flip.1] (x+x@ )* (x+x@ )=x+x@ .
1266,1265 [para_into,1079.1.1.1.2.1,594.1.1,demod,1188,1188,1181,1188,flip.1] (x+ (y+y@ )@ @ )@ = (y+y@ )@ .
1276 [para_from,1081.1.1,357.1.1.1.1,flip.1] (x+ (y+x@ )@ )@ = (x+x)@ .
1278 [para_into,1092.1.1.2.1,924.1.1] (x+x@ )@ + ((y+y@ )@ + (z*z))=z.
1283 [para_into,1099.1.1.1,1045.1.1,demod,998,1255,1255,1257] (x*x@ )@ =y+y@ .
1290,1289 [para_into,1139.1.1.1.1,924.1.1] (x+x@ )@ @ + (y+y@ )@ =y+y@ .
1321,1320 [para_from,1250.1.1,813.1.1.2.1.1.1,demod,1102,796,1251] x+ (y+y@ )=y+y@ .
1325,1324 [para_into,1256.1.1.1,1194.1.1,demod,1290,1136,1321,1321,1257,1321,1136,1321,1321,1257,1321] (x+x@ )* (y+y@ )=y+y@ .
1330,1329 [para_from,1265.1.1,1135.1.1.1,demod,1266,1136,1321,1321,1325,1321,1266,1004,flip.1] x+ (y+y@ )@ @ =y+y@ .
1338,1337 [para_into,1276.1.1.1.2,1096.1.1,flip.1] ((x+y)+ (x+y))@ = ((x+y)+x)@ .
1341 [para_into,1276.1.1.1.2,711.1.1,demod,1338] ((x+y)+y)@ = ((x+y)+x)@ .
1345 [para_from,1276.1.1,813.1.1.2.1.1,demod,532,flip.1] x+ (y+x@ )@ =x+x.
1365 [para_into,1337.1.1.1.1,917.1.1,demod,918,897,959,959,956,918,flip.1] (((x+x)* (x+x))+ (y*x))@ =x@ .
1376,1375 [para_from,1337.1.1,491.1.1.2.1.1,demod,484,flip.1] (x+y)+ (x+y)= (x+y)+x.
1393 [para_from,1341.1.1,483.1.1.2.1.1,demod,484] (x+y)+x= (x+y)+y.
1397 [copy,1393,flip.1] (x+y)+y= (x+y)+x.
1411 [para_from,1345.1.1,459.1.1.2.1,demod,920,1376,1376] x+ (((x+y)+x)* ((x+y)+x))=x+y.
1426,1425 [para_from,1365.1.1,813.1.1.2.1.1,demod,922,flip.1] ((x+x)* (x+x))+ (y*x)=x.
1432 [para_into,1375.1.1,1043.1.1] (x+x@ )@ + (y+z)= (y+z)+y.
1436 [copy,1432,flip.1] (x+y)+x= (z+z@ )@ + (x+y).
1481 [para_into,1411.1.1.2.1.1,917.1.1,demod,1426,918,1426,918] (x*y)+ (y*y)= (y+y)* (y+y).
1485 [para_into,1411.1.1.2.2,1393.1.1] x+ (((x+y)+x)* ((x+y)+y))=x+y.
1494,1493 [para_into,1425.1.1.1.1,559.1.1,demod,869,869,867] (x*x@ )+ (y* (z*z@ ))=z*z@ .
1509 [para_from,1425.1.1,1397.1.1.1,demod,1426,597] x+ (y*x)=x+x.
1511 [para_into,1436.1.1,1393.1.1] (x+y)+y= (z+z@ )@ + (x+y).
1512 [copy,1511,flip.1] (x+x@ )@ + (y+z)= (y+z)+z.
1521 [para_into,1485.1.1.2.1,1393.1.1] x+ (((x+y)+y)* ((x+y)+y))=x+y.
1530,1529 [para_from,1493.1.1,888.1.1.2.2,demod,1494,flip.1] x* (y*y@ )=y*y@ .
1532,1531 [para_from,1509.1.1,1079.1.1.1.2.1,demod,1188,1330,flip.1] x* (y+y@ )@ = (y+y@ )@ .
1553 [para_from,1529.1.1,331.1.1.2.2,demod,1530,869] (x* (y*y@ )@ )+ (y*y@ )=x.
1565 [para_into,1553.1.1.1.2,1283.1.1] (x* (y+y@ ))+ (z*z@ )=x.
1579 [para_into,1565.1.1.2,1146.1.1] (x* (y+y@ ))+ ((z+z@ )@ *u)=x.
1590 [para_from,1579.1.1,345.1.1.1.2.1.2] ((x+y@ )@ + (x+y)@ )@ =x.
1593,1592 [para_from,1579.1.1,331.1.1.2,demod,1532] (x+x@ )@ +y=y.
1609,1608 [back_demod,1512,demod,1593,flip.1] (x+y)+y=x+y.
1621,1620 [back_demod,1278,demod,1593,1593] x*x=x.
1625,1624 [back_demod,1211,demod,1593,flip.1] x+ (x+x)=x+x.
1627,1626 [back_demod,1209,demod,1593,1625,1621] x+x=x.
1629 [back_demod,1196,demod,1593,1627] (x@ +y)@ +x=x.
1633,1632 [back_demod,1194,demod,1593,flip.1] x+ (y+y@ )@ =x.
1635,1634 [back_demod,1101,demod,1593,1627,1627,1621] x@ @ =x.
1636 [back_demod,1096,demod,1593] (x@ + (x+y)@ )@ =x.
1641,1640 [back_demod,1092,demod,1621,1593] (x*x@ )+y=y.
1645,1644 [back_demod,1045,demod,1593,flip.1] x+ (y*y@ )=x.
1647,1646 [back_demod,1035,demod,1593,1627] (x*y)+x=x.
1683,1682 [back_demod,688,demod,1627,1627,1641,flip.1] (x@ *x)+y=y.
1685,1684 [back_demod,686,demod,1627,1627,1641,flip.1] x+ (y@ *y)=x.
1700 [back_demod,509,demod,1627] (x@ + (x*y)@ )@ =x*y.
1705,1704 [back_demod,1521,demod,1609,1609,1621] x+ (x+y)=x+y.
1707,1706 [back_demod,1481,demod,1621,1627,1627,1621] (x*y)+y=y.
1712 [back_demod,917,demod,1627,1627,1621] (x*y)+ (x@ *y)=y.
1721,1720 [back_demod,1345,demod,1627] x+ (y+x@ )@ =x.
1731,1730 [back_demod,331,demod,1685] (x*y@ )+ (x*y)=x.
1736 [para_from,1590.1.1,716.1.1.1.2] (((x+y@ )@ +y)@ +x)@ = (x+y@ )@ .
1750,1749 [para_from,1592.1.1,716.1.1.1.2.1.2.1] ((x+y)@ + (x+y@ )@ )@ =x.
1762 [para_from,1592.1.1,357.1.1.1.1.1.2.1.2.1,demod,1593,1635,1633,1635,1593,1635] (x+y)+ (z+y@ )@ =x+y.
1772 [back_demod,322,demod,1750,unit_del,318] (A+B)+C!=A+ (B+C)|B+A!=A+B| (A@ +B@ )@ !=A*B|$Ans(Robbins_plus_and).
1790,1789 [para_from,1632.1.1,361.1.1.2.1.1,demod,1721,1633,1721,1683] (x@ *y)+ (x*y)=y.
1796,1795 [para_from,1632.1.1,359.1.1.2.2.2,demod,1721,1633,1721,1645] (x*y)+ (x*y@ )=x.
1797 [para_into,1634.1.1.1,1590.1.1,flip.1] (x+y@ )@ + (x+y)@ =x@ .
1800,1799 [para_into,1634.1.1.1,716.1.1,flip.1] (x+y)@ + (x+ (z+y)@ )@ =x@ .
1803 [para_into,1634.1.1.1,437.1.1,flip.1] (x+y@ )@ + (x+ (y*z))@ =x@ .
1816 [para_from,1634.1.1,1629.1.1.1.1.1] (x+y)@ +x@ =x@ .
1823 [para_from,1636.1.1,483.1.1.2.1.1,demod,1633,flip.1] x@ + (x+y)@ =x@ .
1836 [para_into,1700.1.1.1.1,1634.1.1] (x+ (x@ *y)@ )@ =x@ *y.
1852 [para_into,1720.1.1.2.1.2,1634.1.1] x@ + (y+x)@ =x@ .
1858 [para_into,1736.1.1.1.1.1.1.1.2,1634.1.1,demod,1635] (((x+y)@ +y@ )@ +x)@ = (x+y)@ .
1860 [para_from,1736.1.1,483.1.1.2.1.1,demod,1800,1635,flip.1] ((x+y@ )@ +y)@ +x=x+y@ .
1872 [para_into,1749.1.1.1.1.1,1706.1.1] (x@ + ((y*x)+x@ )@ )@ =y*x.
1874 [para_into,1749.1.1.1.2.1,1706.1.1,demod,1635] (((x*y@ )+y)@ +y)@ =x*y@ .
1899,1898 [para_into,1762.1.1,813.1.1] (x+ (y+z))+z=x+ (y+z).
1900 [para_into,1762.1.1,459.1.1] (x+ (y+z))+y=x+ (y+z).
1910 [para_from,1795.1.1,459.1.1.2.1.1.1,demod,1796] (x*y)+ (x@ + ((x*y@ )+z)@ )@ =x.
1912 [para_into,1797.1.1.1.1,1797.1.1,demod,1635,1635] x+ ((x+y@ )@ + (x+y))@ =x+y@ .
1920 [para_into,1797.1.1.2.1,1797.1.1,demod,1635,1635,1635] ((x+y@ )@ + (x+y))@ +x=x+y@ .
1939 [para_into,1799.1.1.2.1,1799.1.1,demod,1635,1635] ((x+y)@ + (z+y)@ )@ +x=x+y.
1958,1957 [para_into,1803.1.1.2.1,1712.1.1,demod,1635,1647,flip.1] (x*y)@ =x@ +y@ .
1964,1963 [back_demod,1836,demod,1958,1635,1705] (x+y@ )@ =x@ *y.
1980,1979 [back_demod,1939,demod,1964,1635] ((x+y)* (z+y))+x=x+y.
1985 [back_demod,1920,demod,1964] ((x@ *y)+ (x+y))@ +x=x+y@ .
1987 [back_demod,1912,demod,1964] x+ ((x@ *y)+ (x+y))@ =x+y@ .
1989 [back_demod,1910,demod,1964,1635] (x*y)+ (x* ((x*y@ )+z))=x.
2001 [back_demod,1872,demod,1964,1958] (x@ + ((y@ +x@ )*x))@ =y*x.
2005 [back_demod,1860,demod,1964,1707] x@ +y=y+x@ .
2006 [back_demod,1858,demod,1964,1635] (((x+y)*y)+x)@ = (x+y)@ .
2035 [back_demod,1772,demod,1964,1635,unit_del,318] (A+B)+C!=A+ (B+C)|B+A!=A+B|$Ans(Robbins_plus_and).
2061,2060 [para_from,1874.1.1,1634.1.1.1,demod,1958,1635,flip.1] ((x*y@ )+y)@ +y=x@ +y.
2076,2075 [back_demod,1874,demod,2061] (x@ +y)@ =x*y@ .
2084 [back_demod,2001,demod,2076,1958,1964,1635] x* ((y*x)+x@ )=y*x.
2110 [para_into,1898.1.1.1.2,1789.1.1,demod,1790] (x+y)+ (z*y)=x+y.
2112 [para_into,1898.1.1.1.2,1730.1.1,demod,1731] (x+y)+ (y*z)=x+y.
2149,2148 [para_into,1963.1.1.1.2,1634.1.1] (x+y)@ =x@ *y@ .
2154 [para_into,1963.1.1.1,1852.1.1,demod,1635,1635,flip.1] x* (y+x)=x.
2157,2156 [para_into,1963.1.1.1,1823.1.1,demod,1635,1635,flip.1] x* (x+y)=x.
2158 [para_into,1963.1.1.1,1816.1.1,demod,1635,2149,1958,1635,1635,flip.1] (x+y)*x=x.
2196 [back_demod,2006,demod,2149,1958,2149,1707,2149] x@ *y@ =y@ *x@ .
2199 [back_demod,1987,demod,2149,1958,1635,2149] x+ ((x+y@ )* (x@ *y@ ))=x+y@ .
2201 [back_demod,1985,demod,2149,1958,1635,2149] ((x+y@ )* (x@ *y@ ))+x=x+y@ .
2256 [para_into,2005.1.1.1,1634.1.1,demod,1635] x+y=y+x.
2257 [back_unit_del,2256.1,2035.2] (A+B)+C!=A+ (B+C)|$Ans(Robbins_plus_and).
2259,2258 [para_into,2084.1.1.2.2,1634.1.1] x@ * ((y*x@ )+x)=y*x@ .
2290 [para_into,2112.1.1.1,1979.1.1,demod,1980] (x+y)+ (x*z)=x+y.
2345,2344 [para_into,2154.1.1.2,2110.1.1] (x*y)* (z+y)=x*y.
2355,2354 [para_into,2154.1.1.2,1730.1.1] (x*y)*x=x*y.
2360 [para_from,2154.1.1,1712.1.1.2] (x* (y+x@ ))+x@ =y+x@ .
2369,2368 [para_from,2156.1.1,2084.1.1.2.1,demod,2149,2157] (x+y)* (x+ (x@ *y@ ))=x.
2377,2376 [para_from,2156.1.1,1712.1.1.1] x+ (x@ * (x+y))=x+y.
2383,2382 [para_into,2158.1.1.1,1712.1.1] x* (y*x)=y*x.
2394 [para_into,2196.1.1.1,1634.1.1,demod,1635] x*y@ =y@ *x.
2398 [para_into,2199.1.1.2.1.2,1634.1.1,demod,1635,1635] x+ ((x+y)* (x@ *y))=x+y.
2401,2400 [para_into,2199.1.1.2.1,1706.1.1,demod,1958,1635,2383,1707] (x*y@ )+ ((x@ +y)*y@ )=y@ .
2404 [para_into,2201.1.1.1.1.2,1634.1.1,demod,1635,1635] ((x+y)* (x@ *y))+x=x+y.
2412 [para_into,2256.1.1,2110.1.1,flip.1] (x*y)+ (z+y)=z+y.
2426 [para_from,2256.1.1,1900.1.1.1.2,demod,1899] x+ (y+z)=x+ (z+y).
2432 [para_from,2258.1.1,2084.1.1.2.1,demod,2149,1958,1635,2401,2259] ((x*y@ )+y)*y@ =x*y@ .
2435,2434 [para_into,2290.1.1,2256.1.1] (x*y)+ (x+z)=x+z.
2470 [para_from,2354.1.1,2084.1.1.2.1,demod,2355] x* ((x*y)+x@ )=x*y.
2482 [para_into,2368.1.1.2,2256.1.1] (x+y)* ((x@ *y@ )+x)=x.
2484 [para_from,2368.1.1,2084.1.1.2.1,demod,2149,1958,1635,1635,2377,2369] (x+ (x@ *y@ ))* (x+y)=x.
2493,2492 [para_into,2382.1.1.2,2344.1.1,demod,2345] (x+y)* (z*y)=z*y.
2495,2494 [back_demod,2404,demod,2493] (x@ *y)+x=x+y.
2497,2496 [back_demod,2398,demod,2493] x+ (x@ *y)=x+y.
2498 [back_demod,2482,demod,2495] (x+y)* (x+y@ )=x.
2503 [back_demod,2484,demod,2497] (x+y@ )* (x+y)=x.
2512 [para_into,2394.1.1.2,1634.1.1,demod,1635] x*y=y*x.
2542 [para_from,2412.1.1,1989.1.1.2.2] (x*y)+ (x* (z+y@ ))=x.
2545 [para_into,2426.1.1,2256.1.1] (x+y)+z=z+ (y+x).
2555 [copy,2545,flip.1] x+ (y+z)= (z+y)+x.
2570 [para_into,2432.1.1.1.1.2,1634.1.1,demod,1635,1635] ((x*y)+y@ )*y=x*y.
2600 [para_into,2470.1.1.2,2256.1.1] x* (x@ + (x*y))=x*y.
2657,2656 [para_into,2496.1.1.2.1,1634.1.1] x@ + (x*y)=x@ +y.
2659,2658 [back_demod,2600,demod,2657] x* (x@ +y)=x*y.
2669,2668 [para_into,2498.1.1.1,1712.1.1,demod,1958,1635,2435] x* (y+x@ )=y*x.
2677,2676 [back_demod,2360,demod,2669] (x*y)+y@ =x+y@ .
2678 [back_demod,2570,demod,2677] (x+y@ )*y=x*y.
2690 [para_into,2503.1.1.1,2256.1.1] (x@ +y)* (y+x)=y.
2712 [para_from,2512.1.1,2432.1.1.1.1,demod,2495] (x+y)*x@ =y*x@ .
2719,2718 [para_from,2512.1.1,2496.1.1.2] x+ (y*x@ )=x+y.
2740 [para_into,2542.1.1.2.2.2,1634.1.1] (x*y@ )+ (x* (z+y))=x.
2893 [para_into,2690.1.1.2,2256.1.1] (x@ +y)* (x+y)=y.
2972 [para_from,2740.1.1,2712.1.1.1,demod,1958,1635,2659,1958,1635,flip.1] (x* (y+z))* (x@ +z)=x*z.
3000,2999 [para_into,2972.1.1.1,2972.1.1,demod,1958,2149,2345,flip.1] (x* (y+z))*z=x*z.
3052 [para_into,2999.1.1.1,2678.1.1,demod,3000,2149,flip.1] (x+ (y@ *z@ ))*z=x*z.
3070 [para_into,3052.1.1.1.2.1,1634.1.1] (x+ (y*z@ ))*z=x*z.
3105 [para_from,3070.1.1,2718.1.1.2,demod,2719,1635,flip.1] x+ (y+ (z*x))=x+y.
3111 [para_into,3105.1.1.2.2,2893.1.1] (x+y)+ (z+y)= (x+y)+z.
3114,3113 [para_into,3105.1.1.2.2,2690.1.1] (x+y)+ (z+x)= (x+y)+z.
3178 [para_into,3111.1.1,2555.1.1,demod,3114] (x+y)+z= (z+x)+y.
3323 [para_into,3178.1.1,2256.1.1,flip.1] (x+y)+z=x+ (y+z).
3325 [binary,3323.1,2257.1] $Ans(Robbins_plus_and).

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