pushreference 1 "(a2 E a1 & P1 & P0) & P0 -> ( An(a1) E a1 & P2 & P0) & P0" "AN";
THEOREMS:=("AN",(termtosequent(parseprop(" (a2 E a1 & P1 & P0) & P0 -> ( An(a1) E a1 & P2 & P0) & P0")),hd(!PROOFSTACK)))::(!THEOREMS);
PROOFSTACK:=nil;
td "AN";
pushreference 2 "P0 -> (Real(a1 + a2) & P3 & P0) & P0" "RPLUS";
THEOREMS:=("RPLUS",(termtosequent(parseprop("P0 -> (Real(a1 + a2) & P3 & P0) & P0")),hd(!PROOFSTACK)))::(!THEOREMS);
PROOFSTACK:=nil;
td "RPLUS";
pushreference 3 "P0 -> (Real(a1 * a2) & P4 & P0) & P0" "RTIMES";
THEOREMS:=("RTIMES",(termtosequent(parseprop("P0 -> (Real(a1 * a2) & P4 & P0) & P0")),hd(!PROOFSTACK)))::(!THEOREMS);
PROOFSTACK:=nil;
td "RTIMES";
pushreference 4 "P0 -> (Real(Minus(a1)) & P5 & P0) & P0" "RMINUS";
THEOREMS:=("RMINUS",(termtosequent(parseprop("P0 -> (Real(Minus(a1)) & P5 & P0) & P0")),hd(!PROOFSTACK)))::(!THEOREMS);
PROOFSTACK:=nil;
td "RMINUS";
pushreference 5 "P0 -> (Real(Inv(a1)) & P6 & P0) & P0" "RINV";
THEOREMS:=("RINV",(termtosequent(parseprop("P0 -> (Real(Inv(a1)) & P6 & P0) & P0")),hd(!PROOFSTACK)))::(!THEOREMS);
PROOFSTACK:=nil;
td "RINV";
pushreference 6 "P0 -> (Real(Sup(a1)) & P7 & P0) & P0" "RSUP";
THEOREMS:=("RSUP",(termtosequent(parseprop("P0 -> (Real(Sup(a1)) & P7 & P0) & P0")),hd(!PROOFSTACK)))::(!THEOREMS);
PROOFSTACK:=nil;
td "RSUP";
pushreference 7 "P0 -> ( a1 + a2 = a2 + a1 & P8 & P0) & P0" "CPLUS";
THEOREMS:=("CPLUS",(termtosequent(parseprop("P0 -> ( a1 + a2 = a2 + a1 & P8 & P0) & P0")),hd(!PROOFSTACK)))::(!THEOREMS);
PROOFSTACK:=nil;
td "CPLUS";
pushreference 8 "P0 -> ( a1 * a2 = a2 * a1 & P9 & P0) & P0" "CTIMES";
THEOREMS:=("CTIMES",(termtosequent(parseprop("P0 -> ( a1 * a2 = a2 * a1 & P9 & P0) & P0")),hd(!PROOFSTACK)))::(!THEOREMS);
PROOFSTACK:=nil;
td "CTIMES";
pushreference 9 "P0 ->  ([a1 + a2] + a3 = a1 + a2 + a3 & P10 & P0) & P0" "APLUS";
THEOREMS:=("APLUS",(termtosequent(parseprop(" P0 -> ( [a1 + a2] + a3 = a1 + a2 + a3 & P10 & P0) & P0")),hd(!PROOFSTACK)))::(!THEOREMS);
PROOFSTACK:=nil;
td "APLUS";
pushreference 10 " P0 -> ( [a1 * a2] * a3 = a1 * a2 * a3 & P11 & P0) & P0" "ATIMES";
THEOREMS:=("ATIMES",(termtosequent(parseprop(" P0 -> ( [a1 * a2] * a3 = a1 * a2 * a3 & P11 & P0) & P0")),hd(!PROOFSTACK)))::(!THEOREMS);
PROOFSTACK:=nil;
td "ATIMES";
pushreference 11 " P0 ->  (a1 * [a2 + a3] = a1 * a2 + a1 * a3 & P12 & P0) & P0" "DIST";
THEOREMS:=("DIST",(termtosequent(parseprop(" P0 ->  (a1 * [a2 + a3] = a1 * a2 + a1 * a3 & P12 & P0) & P0")),hd(!PROOFSTACK)))::(!THEOREMS);
PROOFSTACK:=nil;
td "DIST";
pushreference 12 " P0 -> ( (Real(a1) -> a1 + Zero = a1) & P13 & P0) & P0" "IPLUS";
THEOREMS:=("IPLUS",(termtosequent(parseprop(" P0 -> ( (Real(a1) -> a1 + Zero = a1) & P13 & P0) & P0")),hd(!PROOFSTACK)))::(!THEOREMS);
PROOFSTACK:=nil;
td "IPLUS";
pushreference 13 " P0 -> ( (Real(a1) -> a1 * One = a1) & P14 & P0) & P0" "ITIMES";
THEOREMS:=("ITIMES",(termtosequent(parseprop(" P0 -> ( (Real(a1) -> a1 * One = a1) & P14 & P0) & P0")),hd(!PROOFSTACK)))::(!THEOREMS);
PROOFSTACK:=nil;
td "ITIMES";
pushreference 14 " P0 -> (a1 + Minus(a1) = Zero & P15 & P0) & P0" "MINUS";
THEOREMS:=("MINUS",(termtosequent(parseprop("P0 -> ( a1 + Minus(a1) = Zero & P15 & P0) & P0")),hd(!PROOFSTACK)))::(!THEOREMS);
PROOFSTACK:=nil;
td "MINUS";
pushreference 15 "P0 -> ((a1 Equal Zero v a1 * Inv(a1) = One) &  P16 & P0) & P0" "INV";
THEOREMS:=("INV",(termtosequent(parseprop("P0 -> ((a1 Equal Zero v a1 * Inv(a1) = One) &  P16 & P0) & P0")),hd(!PROOFSTACK)))::(!THEOREMS);
PROOFSTACK:=nil;
td "INV";
pushreference 16 "P0 -> (~Zero Equal One & P17 & P0) & P0" "NONTRIV";
THEOREMS:=("NONTRIV",(termtosequent(parseprop("P0 -> (~Zero Equal One & P17 & P0) & P0")),hd(!PROOFSTACK)))::(!THEOREMS);
PROOFSTACK:=nil;
td "NONTRIV";
pushreference 17 "P0 -> (~a1 < a1 & P18 & P0) & P0" "IRR";
THEOREMS:=("IRR",(termtosequent(parseprop("P0 -> (~a1 < a1 & P18 & P0) & P0")),hd(!PROOFSTACK)))::(!THEOREMS);
PROOFSTACK:=nil;
td "IRR";
pushreference 18 "P0 -> ( (a1 Equal a2 v a1 < a2 v a2 < a1) & P19 & P0) & P0" "TRI";
THEOREMS:=("TRI",(termtosequent(parseprop("P0 -> ((a1 Equal a2 v a1 < a2 v a2 < a1) &  P19 & P0) & P0")),hd(!PROOFSTACK)))::(!THEOREMS);
PROOFSTACK:=nil;
td "TRI";
pushreference 19 "P0 -> (( a1 < a2 & a2 < a3 -> a1 < a3) &  P20 & P0) & P0" "TRANS";
THEOREMS:=("TRANS",(termtosequent(parseprop("P0 -> (( a1 < a2 & a2 < a3 -> a1 < a3) &  P20 & P0) & P0")),hd(!PROOFSTACK)))::(!THEOREMS);
PROOFSTACK:=nil;
td "TRANS";
pushreference 20 "P0 -> ((a1 < a2 == a1 + a3 < a2 + a3) &  P21 & P0) & P0" "MPLUS0";
THEOREMS:=("MPLUS0",(termtosequent(parseprop("P0 -> ((a1 < a2 == a1 + a3 < a2 + a3) &  P21 & P0) & P0")),hd(!PROOFSTACK)))::(!THEOREMS);
PROOFSTACK:=nil;
td "MPLUS0";
pushnode 5 " ((a1 < a2 -> a1 + a3 < a2 + a3) &  P25 & P24 & P23 & P0) & P0 -> (( a1 < a2 -> a1 + a3 < a2 + a3) &  P22 & P0) & P0" 0;
pushnode 4 " (((a1 < a2 -> a1 + a3 < a2 + a3) & ( a1 + a3 < a2 + a3 -> a1 < a2)) &  P24 & P23 & P0) & P0 -> (( a1 < a2 -> a1 + a3 < a2 + a3) &  P22 & P0) & P0" 1;
pushnode 3 " ((a1 < a2 == a1 + a3 < a2 + a3) &  P23 & P0) & P0 -> ((a1 < a2 -> a1 + a3 < a2 + a3) &  P22 & P0) & P0" 1;
pushreference 2 "P0 -> ((a1 < a2 == a1 + a3 < a2 + a3) &  P23 & P0) & P0" "MPLUS0";
pushnode 1 "P0 -> ((a1 < a2 -> a1 + a3 < a2 + a3) &  P22 & P0) & P0" 2;
THEOREMS:=("MPLUS",(termtosequent(parseprop("P0 -> ((a1 < a2 -> a1 + a3 < a2 + a3) &  P22 & P0) & P0")),hd(!PROOFSTACK)))::(!THEOREMS);
PROOFSTACK:=nil;
td "MPLUS";
pushreference 6 "P0 -> (( Zero < a3 & a1 < a2 -> a1 * a3 < a2 * a3) &  P27 & P0) & P0" "MTIMES";
THEOREMS:=("MTIMES",(termtosequent(parseprop("P0 -> (( Zero < a3 & a1 < a2 -> a1 * a3 < a2 * a3) &  P27 & P0) & P0")),hd(!PROOFSTACK)))::(!THEOREMS);
PROOFSTACK:=nil;
td "MTIMES";
pushreference 7 "P0 -> (( (Ex1.x1 E a1) & (Ax1.x1 E a1 -> x1 <= a2) -> Sup(a1) <= a2) &  P28 & P0) & P0" "SUP1";
THEOREMS:=("SUP1",(termtosequent(parseprop("P0 -> (( (Ex1.x1 E a1) & (Ax1.x1 E a1 -> x1 <= a2) -> Sup(a1) <= a2) &  P28 & P0) & P0")),hd(!PROOFSTACK)))::(!THEOREMS);
PROOFSTACK:=nil;
td "SUP1";
pushreference 8 "P0 -> (( (Ax1.x1 E a1 -> x1 <= a2) -> (Ax1.x1 E a1 -> x1 <= Sup(a1))) &  P29 & P0) & P0" "SUP2";
THEOREMS:=("SUP2",(termtosequent(parseprop("P0 -> (( (Ax1.x1 E a1 -> x1 <= a2) -> (Ax1.x1 E a1 -> x1 <= Sup(a1))) &  P29 & P0) & P0")),hd(!PROOFSTACK)))::(!THEOREMS);
PROOFSTACK:=nil;
td "SUP2";
pushnode 36 " (a1 + Zero = a1 & P72 & P68 & P0) & P0 -> ( a1 + Zero = a1 & P67 & P64 & P37 & P35 & P32 & P30 & P65 & P37 & P35 & P32 &  P30 & P0) & P0" 0;
pushnode 35 " (Real(a1) & P33 & P31 & P30 & P0) & P0 -> ( Real(a1) & P71 & P68 & P0) & P0" 0;
pushnode 33 "((Real(a1) -> a1 + Zero = a1) & P68 & P0) &  (Real(a1) & P33 & P31 & P30 & P0) & P0 -> (a1 + Zero = a1 & P67 & P64 & P37 & P35 & P32 & P30 & P65 &  P37 & P35 & P32 & P30 & P0) & P0" 2;
pushreference 32 "P0 -> ((Real(a1) -> a1 + Zero = a1) & P68 & P0) & P0" "IPLUS";
pushnode 31 "( Real(a1) & P33 & P31 & P30 & P0) & P0 ->  (a1 + Zero = a1 & P67 & P64 &  P37 & P35 & P32 & P30 & P65 & P37 & P35 & P32 & P30 & P0) & P0" 2;
pushnode 30 "( a2 = Zero & P64 & P37 & P35 & P32 & P30 & P0) & ( Real(a1) & P33 & P31 & P30 & P0) & P0 ->  (a1 + a2 = a1 &  P65 & P37 & P35 & P32 & P30 & P0) & P0" 1;
pushnode 6 "( Real(a1) & P33 & P31 & P30 & P0) & P0 -> ((a2 = Zero -> a1 + a2 = a1) & P37 & P35 &  P32 & P30 & P0) & P0" 1;
pushnode 29 " ( [a2 + a1] + Minus(a1) = a2 & P60 & P58 & P53 & P52 & P45 & P43 &  P57 & P55 & P0) & P0 -> ([ a2 + a1] + Minus(a1) = a2 &  P63 & P51 & P49 & P59 & P53 & P52 & P45 & P43 & P46 & P0) & P0" 0;
pushnode 28 " ( a1 + a2 = a2 + a1 & P51 & P49 & P0) &  ([a2 + a1] + Minus(a1) = a2 &  P60 & P58 & P53 & P52 & P45 & P43 & P57 & P55 & P0) & P0 -> ([a1 + a2] + Minus(a1) = a2 & P59 & P53 & P52 &  P45 & P43 & P46 & P0) & P0" 1;
pushnode 27 " ([a2 + a1] + Minus(a1) = a2 + Zero & P58 & P53 & P52 & P45 & P43 & P0) &  (a2 + Zero = a2 & P57 & P55 & P0) &  (a1 + a2 = a2 + a1 & P51 & P49 & P0) & P0 ->  ([ a1 + a2] + Minus(a1) = a2 &  P59 & P53 & P52 & P45 & P43 & P46 & P0) & P0" 1;
pushnode 26 " ([ a2 + a1] + Minus(a1) = a2 + Zero &  P53 & P52 & P45 & P43 & P0) & ( a2 + Zero = a2 & P57 & P55 & P0) & (a1 + a2 = a2 + a1 & P51 & P49 & P0) & P0 -> ( [a1 + a2] + Minus(a1) = a2 &  P46 & P0) & P0" 1;
pushnode 25 "( Real(a2) & P34 & P31 & P30 & P0) & P0 -> (Real(a2) & P56 & P55 & P0) & P0" 0;
pushnode 24 "((Real(a2) -> a2 + Zero = a2) & P55 & P0) &  ([a2 + a1] + Minus(a1) = a2 + Zero &  P53 & P52 & P45 & P43 & P0) &  (Real(a2) & P34 & P31 & P30 & P0) &  (a1 + a2 = a2 + a1 & P51 & P49 & P0) & P0 -> ([a1 + a2] + Minus(a1) = a2 & P46 & P0) & P0" 2;
pushreference 23 "P0 -> ((Real(a2) -> a2 + Zero = a2) & P55 & P0) & P0" "IPLUS";
pushnode 22 " ([ a2 + a1] + Minus(a1) = a2 + Zero &  P53 & P52 & P45 & P43 & P0) &  (Real(a2) & P34 & P31 & P30 & P0) &  (a1 + a2 = a2 + a1 & P51 & P49 & P0) & P0 -> ([ a1 + a2] + Minus(a1) = a2 &  P46 & P0) & P0" 2;
pushnode 21 "( [a2 + a1] + Minus(a1) = a2 +  a1 + Minus(a1) & P52 & P0) & ( a1 + Minus(a1) = Zero & P45 &  P43 & P0) & ( Real(a2) & P34 & P31 & P30 & P0) & ( a1 + a2 = a2 + a1 & P51 & P49 & P0) & P0 -> ([a1 + a2] + Minus(a1) = a2 &  P46 & P0) & P0" 1;
pushreference 20 "P0 -> ( [a2 + a1] + Minus(a1) =  a2 + a1 + Minus(a1) & P52 & P0) & P0" "APLUS";
pushnode 19 "( a1 + a2 = a2 + a1 & P51 & P49 & P0) & (a1 + Minus(a1) = Zero & P45 & P43 & P0) &  (Real(a2) &  P34 & P31 & P30 & P0) & P0 -> ([ a1 + a2] + Minus(a1) = a2 &  P46 & P0) & P0" 2;
pushnode 18 " (a1 + a2 = a2 + a1 &  P49 & P0) & (a1 + Minus(a1) = Zero & P45 & P43 & P0) &  (Real(a2) &  P34 & P31 & P30 & P0) & P0 -> ([a1 + a2] + Minus(a1) = a2 & P46 & P0) & P0" 1;
pushreference 17 "P0 -> ( a1 + a2 = a2 + a1 & P49 & P0) & P0" "CPLUS";
pushnode 15 "( a1 + Minus(a1) = Zero & P45 & P43 & P0) & ( Real(a2) & P34 & P31 & P30 & P0) & P0 -> ([a1 + a2] + Minus(a1) = a2 & P46 & P0) & P0" 2;
pushnode 16 " (a2 = Zero & P47 & P44 & P40 & P43 & P46 & P0) & P0 -> (a2 = Zero & P39 & P36 & P35 & P32 & P30 & P0) & P0" 0;
pushnode 14 " ( [a1 + a2] + Minus(a1) = Zero & P44 & P40 & P43 & P0) & ([ a1 + a2] + Minus(a1) = a2 &  P46 & P0) & P0 -> (a2 = Zero & P39 & P36 & P35 & P32 & P30 & P0) & P0" 1;
pushnode 13 "( [a1 + a2] + Minus(a1) = Zero & P44 & P40 & P43 & P0) & ( a1 + Minus(a1) = Zero & P45 &  P43 & P0) & ( Real(a2) & P34 & P31 & P30 & P0) & P0 ->  (a2 = Zero &  P39 & P36 & P35 & P32 & P30 & P0) & P0" 2;
pushnode 12 "([ a1 + a2] + Minus(a1) = a1 + Minus(a1) & P40 & P0) & ( a1 + Minus(a1) = Zero & P43 & P0) & ( Real(a2) & P34 & P31 & P30 & P0) & P0 ->  (a2 = Zero &  P39 & P36 & P35 & P32 & P30 & P0) & P0" 1;
pushreference 11 " P0 -> (a1 + Minus(a1) = Zero & P43 & P0) & P0" "MINUS";
pushnode 9 " ([a1 + a2] + Minus(a1) =  a1 + Minus(a1) & P40 & P0) &  (Real(a2) & P34 & P31 & P30 & P0) & P0 -> (a2 = Zero & P39 & P36 & P35 & P32 & P30 & P0) & P0" 2;
pushnode 10 "P0 ->  ( a1 + Minus(a1) = a1 + Minus(a1) & P42 & P38 & P36 & P35 &  P32 & P30 & P40 & P0) & P0" 0;
pushnode 8 "( a1 + a2 = a1 & P38 & P36 & P35 & P32 & P30 & P0) & P0 -> ([a1 + a2] + Minus(a1) = a1 + Minus(a1) & P40 & P0) & P0" 1;
pushnode 7 " (a1 + a2 = a1 & P38 & P36 & P35 &  P32 & P30 & P0) &  (Real(a2) & P34 & P31 & P30 & P0) & P0 -> ( a2 = Zero & P39 & P36 & P35 & P32 & P30 & P0) & P0" 2;
pushnode 5 " (Real(a2) & P34 & P31 & P30 & P0) & P0 ->  ((a1 + a2 = a1 -> a2 = Zero) &  P36 & P35 & P32 & P30 & P0) & P0" 1;
pushnode 4 "( Real(a1) & P33 & P31 & P30 & P0) & ( Real(a2) & P34 & P31 & P30 & P0) & P0 -> ( ((a1 + a2 = a1 -> a2 = Zero) & (a2 = Zero -> a1 + a2 = a1)) & P35 & P32 & P30 & P0) & P0" 2;
pushnode 3 "  (Real(a1) & P33 & P31 & P30 & P0) &  (Real(a2) & P34 & P31 & P30 & P0) & P0 -> ((a1 + a2 = a1 == a2 = Zero) & P32 & P30 & P0) & P0" 1;
THEOREMS:=("NULLADD",(termtosequent(parseprop("  (Real(a1) & P33 & P31 & P30 & P0) &  (Real(a2) & P34 & P31 & P30 & P0) & P0 -> ((a1 + a2 = a1 == a2 = Zero) & P32 & P30 & P0) & P0")),hd(!PROOFSTACK)))::(!THEOREMS);
PROOFSTACK:=nil;
td "NULLADD";
pushnode 6 " (a1 + Zero = a1 & P78 & P76 & P0) & P0 -> ( a1 + Zero = a1 & P75 & P73 & P0) & P0" 0;
pushnode 5 "(Real(a1) & P74 & P73 & P0) & P0 -> (Real(a1) & P77 & P76 & P0) & P0" 0;
pushnode 4 "((Real(a1) -> a1 + Zero = a1) & P76 & P0) & (Real(a1) & P74 & P73 & P0) & P0 -> ( a1 + Zero = a1 & P75 & P73 & P0) & P0" 2;
pushreference 3 "P0 -> ((Real(a1) -> a1 + Zero = a1) & P76 & P0) & P0" "IPLUS";
pushnode 2 " ( Real(a1) & P74 & P73 & P0) & P0 -> ( a1 + Zero = a1 & P75 & P73 & P0) & P0" 2;
THEOREMS:=("IPLUSa",(termtosequent(parseprop("(Real(a1) & P74 & P73 & P0) & P0 ->  (a1 + Zero = a1 & P75 & P73 & P0) & P0")),hd(!PROOFSTACK)))::(!THEOREMS);
PROOFSTACK:=nil;
td "IPLUSa";
pushnode 1 "P0 -> (a1 = a1 & P79 & P0) & P0" 0;
THEOREMS:=("TRIV",(termtosequent(parseprop(" P0 ->  (a1 = a1 & P79 & P0) & P0")),hd(!PROOFSTACK)))::(!THEOREMS);
PROOFSTACK:=nil;
td "TRIV";
pushnode 3 "( P2 & P111 & P108 & P0) & P0 ->  (P2 & P109 & P0) & P0" 0;
pushnode 2 "( P1 & P107 & P0) & P0 -> (P1 & P110 & P108 & P0) & P0" 0;
pushnode 1 " ((P1 -> P2) & P108 & P0) & (P1 & P107 & P0) & P0 ->  (P2 & P109 & P0) & P0" 2;
THEOREMS:=("MP",(termtosequent(parseprop("(( P1 -> P2) & P108 & P0) & ( P1 & P107 & P0) & P0 -> (P2 & P109 & P0) & P0")),hd(!PROOFSTACK)))::(!THEOREMS);
PROOFSTACK:=nil;
td "MP";
pushreference 4 " P0 -> (Real(U1 + Minus(U1)) & P115 & P113 &  P112 & P0) & P0" "RPLUS";
pushnode 3 "( U1 + Minus(U1) = Zero & P113 & P0) & P0 -> (Real(Zero) & P112 & P0) & P0" 1;
pushreference 2 "P0 -> ( U1 + Minus(U1) = Zero & P113 & P0) & P0" "MINUS";
pushnode 1 "P0 -> (Real(Zero) & P112 & P0) & P0" 2;
THEOREMS:=("RZERO",(termtosequent(parseprop("P0 -> (Real(Zero) & P112 & P0) & P0")),hd(!PROOFSTACK)))::(!THEOREMS);
PROOFSTACK:=nil;
td "RZERO";
pushnode 17 "P0 -> ( a1 * Zero = a1 * Zero & P131 & P129 & P127 & P126 & P124 & P117 & P0) & P0" 0;
pushnode 16 "(Zero + Zero = Zero & P129 & P127 & P0) & P0 ->  (a1 * [Zero + Zero] =  a1 * Zero & P126 & P124 & P117 & P0) & P0" 1;
pushreference 15 "P0 -> ( Real(Zero) & P128 & P127 & P0) & P0" "RZERO";
pushnode 14 " ((Real(Zero) -> Zero + Zero = Zero) &  P127 & P0) & P0 ->  (a1 * [Zero + Zero] =  a1 * Zero & P126 & P124 & P117 & P0) & P0" 2;
pushreference 13 "P0 -> (( Real(Zero) -> Zero + Zero = Zero) &  P127 & P0) & P0" "IPLUS";
pushnode 12 "P0 ->  (a1 * [Zero + Zero] = a1 * Zero &  P126 & P124 & P117 & P0) & P0" 2;
pushnode 11 "( a1 * [Zero + Zero] =  a1 * Zero + a1 * Zero &  P124 & P0) & P0 -> ( a1 * Zero + a1 * Zero =  a1 * Zero & P117 & P0) & P0" 1;
pushreference 10 "P0 -> (a1 * [Zero + Zero] = a1 * Zero + a1 * Zero & P124 & P0) & P0" "DIST";
pushnode 3 " P0 ->  (a1 * Zero + a1 * Zero = a1 * Zero & P117 & P0) & P0" 2;
pushreference 7 " P0 -> (Real(a1 * Zero) & P119 & P0) & P0" "RTIMES";
pushreference 6 "P0 -> (Real(a1 * Zero) &  P118 & P0) & P0" "RTIMES";
pushreference 9 " ((a1 * Zero + a1 * Zero = a1 * Zero ->  a1 * Zero = Zero) &  P122 & P121 & P120 & P0) & (a1 * Zero + a1 * Zero = a1 * Zero &  P117 & P0) & P0 -> ( a1 * Zero = Zero & P116 & P0) & P0" "MP";
pushnode 8 " (((a1 * Zero + a1 * Zero = a1 * Zero ->  a1 * Zero = Zero) & ( a1 * Zero = Zero ->  a1 * Zero + a1 * Zero = a1 * Zero)) &  P121 & P120 & P0) & (a1 * Zero + a1 * Zero = a1 * Zero &  P117 & P0) & P0 -> ( a1 * Zero = Zero & P116 & P0) & P0" 1;
pushnode 5 "((a1 * Zero + a1 * Zero = a1 * Zero ==  a1 * Zero = Zero) &  P120 & P0) & (a1 * Zero + a1 * Zero = a1 * Zero & P117 & P0) & P0 -> ( a1 * Zero = Zero & P116 & P0) & P0" 1;
pushreference 4 "(Real(a1 * Zero) & P118 & P0) & ( Real(a1 * Zero) & P119 & P0) & P0 -> ((a1 * Zero + a1 * Zero = a1 * Zero ==  a1 * Zero = Zero) &  P120 & P0) & P0" "NULLADD";
pushnode 2 " (a1 * Zero + a1 * Zero = a1 * Zero &  P117 & P0) & P0 -> (a1 * Zero = Zero & P116 & P0) & P0" 4;
pushnode 1 "P0 -> (a1 * Zero = Zero & P116 & P0) & P0" 2;
THEOREMS:=("MZERO",(termtosequent(parseprop("P0 -> (a1 * Zero = Zero & P116 & P0) & P0")),hd(!PROOFSTACK)))::(!THEOREMS);
PROOFSTACK:=nil;
td "MZERO";
pushnode 28 " (a2 = Minus(a1) & P155 & P151 & P149 & P147 & P141 &  P140 & P139 & P136 & P135 & P133 & P132 & P146 & P142 & P145 & P143 & P148 &  P150 & P154 & P152 & P0) & ( Minus(a1) + Zero = Minus(a1) & P145 & P143 & P0) & ( a2 + a1 = Zero & P139 & P136 & P135 & P133 &  P132 & P0) & ( Zero + Minus(a1) = Minus(a1) &  P146 & P142 & P145 & P143 & P0) & ([ a2 + a1] + Minus(a1) = a2 + a1 + Minus(a1) &  P148 & P0) & (a1 + Minus(a1) = Zero & P150 & P0) & ( a2 + Zero = a2 & P154 & P152 & P0) & P0 -> (a2 = Minus(a1) & P137 &  P135 & P133 & P132 & P0) & P0" 0;
pushnode 27 " (a2 + Zero = a2 & P154 &  P152 & P0) & (a2 + Zero = Minus(a1) & P151 &  P149 & P147 & P141 & P140 & P139 & P136 & P135 & P133 & P132 & P146 & P142 &  P145 & P143 & P148 & P150 & P0) &  ( Minus(a1) + Zero = Minus(a1) &  P145 & P143 & P0) &  (a2 + a1 = Zero & P139 &  P136 & P135 & P133 & P132 & P0) & ( Zero + Minus(a1) = Minus(a1) & P146 & P142 & P145 & P143 & P0) & ( [a2 + a1] + Minus(a1) = a2 + a1 + Minus(a1) & P148 & P0) & ( a1 + Minus(a1) = Zero & P150 & P0) & P0 -> (a2 = Minus(a1) & P137 &  P135 & P133 & P132 & P0) & P0" 1;
pushnode 26 " (Real(a2) & P138 & P136 & P135 & P133 & P132 & P0) & P0 ->  (Real(a2) & P153 & P152 & P0) & P0" 0;
pushnode 25 "((Real(a2) -> a2 + Zero = a2) &  P152 & P0) & (a1 + Minus(a1) = Zero & P150 & P0) & ( a2 + Zero = Minus(a1) & P151 & P149 & P147 & P141 & P140 & P139 &  P136 & P135 & P133 & P132 & P146 & P142 & P145 & P143 & P148 & P150 & P0) &  (Real(a2) & P138 &  P136 & P135 & P133 & P132 & P0) & ( Minus(a1) + Zero = Minus(a1) & P145 & P143 & P0) & ( a2 + a1 = Zero & P139 & P136 & P135 & P133 &  P132 & P0) & ( Zero + Minus(a1) = Minus(a1) &  P146 & P142 & P145 & P143 & P0) & ([ a2 + a1] + Minus(a1) = a2 + a1 + Minus(a1) &  P148 & P0) & P0 -> ( a2 = Minus(a1) & P137 & P135 & P133 & P132 & P0) & P0" 2;
pushreference 24 " P0 -> ( (Real(a2) -> a2 + Zero = a2) & P152 & P0) & P0" "IPLUS";
pushnode 23 " ( a1 + Minus(a1) = Zero & P150 & P0) & ( a2 + Zero = Minus(a1) & P151 & P149 & P147 & P141 & P140 & P139 &  P136 & P135 & P133 & P132 & P146 & P142 & P145 & P143 & P148 & P150 & P0) &  (Real(a2) & P138 &  P136 & P135 & P133 & P132 & P0) & ( Minus(a1) + Zero = Minus(a1) & P145 & P143 & P0) & ( a2 + a1 = Zero & P139 & P136 & P135 & P133 &  P132 & P0) & ( Zero + Minus(a1) = Minus(a1) &  P146 & P142 & P145 & P143 & P0) & ([ a2 + a1] + Minus(a1) = a2 + a1 + Minus(a1) &  P148 & P0) & P0 -> (a2 = Minus(a1) & P137 & P135 & P133 & P132 & P0) & P0" 2;
pushnode 22 "( a1 + Minus(a1) = Zero & P150 & P0) & ( a2 + a1 + Minus(a1) = Minus(a1) &  P149 & P147 & P141 & P140 & P139 & P136 & P135 & P133 & P132 & P146 & P142 &  P145 & P143 & P148 & P0) & ( Real(a2) & P138 & P136 & P135 & P133 & P132 & P0) &  ( Minus(a1) + Zero = Minus(a1) &  P145 & P143 & P0) &  (a2 + a1 = Zero & P139 &  P136 & P135 & P133 & P132 & P0) & ( Zero + Minus(a1) = Minus(a1) & P146 & P142 & P145 & P143 & P0) & ( [a2 + a1] + Minus(a1) = a2 + a1 + Minus(a1) & P148 & P0) & P0 -> ( a2 = Minus(a1) & P137 & P135 & P133 & P132 & P0) & P0" 1;
pushreference 21 " P0 -> (a1 + Minus(a1) = Zero & P150 & P0) & P0" "MINUS";
pushnode 20 "( [a2 + a1] + Minus(a1) = a2 + a1 + Minus(a1) & P148 & P0) & ( a2 + a1 + Minus(a1) = Minus(a1) &  P149 & P147 & P141 & P140 & P139 & P136 & P135 & P133 & P132 & P146 & P142 &  P145 & P143 & P148 & P0) & ( Real(a2) & P138 & P136 & P135 & P133 & P132 & P0) &  ( Minus(a1) + Zero = Minus(a1) &  P145 & P143 & P0) &  (a2 + a1 = Zero & P139 &  P136 & P135 & P133 & P132 & P0) & ( Zero + Minus(a1) = Minus(a1) & P146 & P142 & P145 & P143 & P0) & P0 -> (a2 = Minus(a1) & P137 &  P135 & P133 & P132 & P0) & P0" 2;
pushnode 19 "( [a2 + a1] + Minus(a1) = a2 +  a1 + Minus(a1) & P148 & P0) &  ([ a2 + a1] + Minus(a1) = Minus(a1) &  P147 & P141 & P140 & P139 & P136 & P135 & P133 & P132 & P146 & P142 & P145 &  P143 & P0) & (Real(a2) & P138 & P136 & P135 & P133 & P132 & P0) &  ( Minus(a1) + Zero = Minus(a1) &  P145 & P143 & P0) &  (a2 + a1 = Zero & P139 &  P136 & P135 & P133 & P132 & P0) & ( Zero + Minus(a1) = Minus(a1) & P146 & P142 & P145 & P143 & P0) & P0 -> ( a2 = Minus(a1) & P137 & P135 & P133 & P132 & P0) & P0" 1;
pushreference 18 " P0 -> ( [a2 + a1] + Minus(a1) = a2 + a1 + Minus(a1) & P148 & P0) & P0" "APLUS";
pushnode 17 "( Zero + Minus(a1) = Minus(a1) & P146 & P142 & P145 & P143 & P0) & ([a2 + a1] + Minus(a1) = Minus(a1) & P147 &  P141 & P140 & P139 & P136 & P135 & P133 & P132 & P146 & P142 & P145 & P143 & P0) & ( Real(a2) & P138 & P136 & P135 & P133 & P132 & P0) &  ( Minus(a1) + Zero = Minus(a1) &  P145 & P143 & P0) &  (a2 + a1 = Zero & P139 &  P136 & P135 & P133 & P132 & P0) & P0 -> ( a2 = Minus(a1) & P137 & P135 & P133 & P132 & P0) & P0" 2;
pushnode 16 "( Zero + Minus(a1) = Minus(a1) &  P146 & P142 & P145 & P143 & P0) & ([ a2 + a1] + Minus(a1) = Zero + Minus(a1) & P141 & P140 & P139 & P136 &  P135 & P133 & P132 & P0) & ( Real(a2) & P138 & P136 & P135 & P133 & P132 & P0) &  ( Minus(a1) + Zero = Minus(a1) &  P145 & P143 & P0) &  (a2 + a1 = Zero & P139 &  P136 & P135 & P133 & P132 & P0) & P0 -> ( a2 = Minus(a1) & P137 & P135 & P133 & P132 & P0) & P0" 1;
pushnode 15 " ( Minus(a1) + Zero = Minus(a1) &  P145 & P143 & P0) &  (Zero + Minus(a1) = Minus(a1) + Zero & P142 & P0) &  (a2 + a1 = Zero & P139 &  P136 & P135 & P133 & P132 & P0) &  ([a2 + a1] + Minus(a1) = Zero + Minus(a1) &  P141 & P140 & P139 & P136 & P135 & P133 & P132 & P0) &  (Real(a2) & P138 & P136 & P135 & P133 &  P132 & P0) & P0 -> ( a2 = Minus(a1) & P137 & P135 & P133 & P132 & P0) & P0" 1;
pushreference 14 " P0 -> (Real(Minus(a1)) & P144 & P143 & P0) & P0" "RMINUS";
pushnode 13 " ( (Real(Minus(a1)) -> Minus(a1) + Zero = Minus(a1)) & P143 & P0) & ( Zero + Minus(a1) = Minus(a1) + Zero &  P142 & P0) & ( a2 + a1 = Zero & P139 & P136 & P135 & P133 & P132 & P0) & ([ a2 + a1] + Minus(a1) = Zero + Minus(a1) & P141 & P140 & P139 & P136 &  P135 & P133 & P132 & P0) & ( Real(a2) & P138 & P136 & P135 & P133 & P132 & P0) & P0 -> (a2 = Minus(a1) & P137 & P135 & P133 & P132 & P0) & P0" 2;
pushreference 12 "P0 -> ( (Real(Minus(a1)) -> Minus(a1) + Zero = Minus(a1)) & P143 & P0) & P0" "IPLUS";
pushnode 11 " (Zero + Minus(a1) = Minus(a1) + Zero & P142 & P0) &  (a2 + a1 = Zero & P139 &  P136 & P135 & P133 & P132 & P0) &  ([a2 + a1] + Minus(a1) = Zero + Minus(a1) &  P141 & P140 & P139 & P136 & P135 & P133 & P132 & P0) &  (Real(a2) & P138 & P136 & P135 & P133 &  P132 & P0) & P0 -> ( a2 = Minus(a1) & P137 & P135 & P133 & P132 & P0) & P0" 2;
pushreference 10 " P0 -> ( Zero + Minus(a1) = Minus(a1) + Zero & P142 & P0) & P0" "CPLUS";
pushnode 9 "( a2 + a1 = Zero & P139 & P136 & P135 & P133 &  P132 & P0) & ([ a2 + a1] + Minus(a1) = Zero + Minus(a1) & P141 & P140 & P139 & P136 &  P135 & P133 & P132 & P0) & ( Real(a2) & P138 & P136 & P135 & P133 & P132 & P0) & P0 -> ( a2 = Minus(a1) & P137 & P135 & P133 & P132 & P0) & P0" 2;
pushnode 8 "( a2 + a1 = Zero & P139 & P136 & P135 & P133 &  P132 & P0) & ([ a2 + a1] + Minus(a1) =  [a2 + a1] + Minus(a1) &  P140 & P0) & ( Real(a2) & P138 & P136 & P135 & P133 & P132 & P0) & P0 -> ( a2 = Minus(a1) & P137 & P135 & P133 & P132 & P0) & P0" 1;
pushreference 7 " P0 ->  ([a2 + a1] + Minus(a1) =  [a2 + a1] + Minus(a1) &  P140 & P0) & P0" "TRIV";
pushnode 6 "  (Real(a2) &  P138 & P136 & P135 & P133 & P132 & P0) &  (a2 + a1 = Zero & P139 &  P136 & P135 & P133 & P132 & P0) & P0 -> (a2 = Minus(a1) & P137 &  P135 & P133 & P132 & P0) & P0" 2;
pushnode 5 "((Real(a2) & a2 + a1 = Zero) & P136 &  P135 & P133 & P132 & P0) & P0 -> (a2 = Minus(a1) & P137 & P135 & P133 & P132 & P0) & P0" 1;
pushnode 4 "P0 -> (( Real(a2) & a2 + a1 = Zero -> a2 = Minus(a1)) &  P135 & P133 & P132 & P0) & P0" 1;
pushnode 3 "( a1 + a2 = a2 + a1 & P133 & P0) & P0 -> ((Real(a2) & a1 + a2 = Zero -> a2 = Minus(a1)) &  P132 & P0) & P0" 1;
pushreference 2 "P0 -> ( a1 + a2 = a2 + a1 & P133 & P0) & P0" "CPLUS";
pushnode 1 "P0 -> ((Real(a2) & a1 + a2 = Zero -> a2 = Minus(a1)) &  P132 & P0) & P0" 2;
THEOREMS:=("UNIQUEINV",(termtosequent(parseprop("P0 -> ((Real(a2) & a1 + a2 = Zero -> a2 = Minus(a1)) &  P132 & P0) & P0")),hd(!PROOFSTACK)))::(!THEOREMS);
PROOFSTACK:=nil;
td "UNIQUEINV";
pushnode 5 " (a2 = Minus(a1) & P161 & P159 & P0) & P0 -> ( a2 = Minus(a1) & P158 & P0) & P0" 0;
pushnode 7 " (a1 + a2 = Zero & P157 & P0) & P0 -> (a1 + a2 = Zero & P163 &  P160 & P159 & P0) & P0" 0;
pushnode 6 "(Real(a2) & P156 & P0) & P0 -> ( Real(a2) & P162 & P160 & P159 & P0) & P0" 0;
pushnode 4 " (Real(a2) & P156 & P0) & (a1 + a2 = Zero &  P157 & P0) & P0 ->  ((Real(a2) & a1 + a2 = Zero) & P160 &  P159 & P0) & P0" 2;
pushnode 3 "((Real(a2) & a1 + a2 = Zero -> a2 = Minus(a1)) &  P159 & P0) & ( Real(a2) & P156 & P0) & ( a1 + a2 = Zero & P157 & P0) & P0 -> ( a2 = Minus(a1) & P158 & P0) & P0" 2;
pushreference 2 "P0 -> ((Real(a2) & a1 + a2 = Zero -> a2 = Minus(a1)) &  P159 & P0) & P0" "UNIQUEINV";
pushnode 1 " (Real(a2) & P156 & P0) & (a1 + a2 = Zero &  P157 & P0) & P0 -> ( a2 = Minus(a1) & P158 & P0) & P0" 2;
THEOREMS:=("UINV",(termtosequent(parseprop(" (Real(a2) & P156 & P0) & (a1 + a2 = Zero &  P157 & P0) & P0 -> ( a2 = Minus(a1) & P158 & P0) & P0")),hd(!PROOFSTACK)))::(!THEOREMS);
PROOFSTACK:=nil;
td "UINV";
pushreference 9 "P0 -> (Real(Zero) & P171 & P0) & P0" "RZERO";
pushnode 8 "(Real(a1) & P165 & P164 & P0) & P0 ->  (Real(a1) & P170 & P0) & P0" 0;
pushreference 13 "(( Zero = Zero -> a1 + Zero = a1) &  P175 & P173 & P172 & P0) & ( Zero = Zero & P176 & P0) & P0 -> ( a1 + Zero = a1 & P169 & P167 & P166 & P164 & P0) & P0" "MP";
pushnode 12 " P0 ->  (Zero = Zero & P176 & P0) & P0" 0;
pushnode 11 "(( Zero = Zero -> a1 + Zero = a1) &  P175 & P173 & P172 & P0) & P0 -> (a1 + Zero = a1 & P169 &  P167 & P166 & P164 & P0) & P0" 2;
pushnode 10 "( ((a1 + Zero = a1 -> Zero = Zero) & ( Zero = Zero -> a1 + Zero = a1)) & P173 & P172 & P0) & P0 -> (a1 + Zero = a1 & P169 &  P167 & P166 & P164 & P0) & P0" 1;
pushnode 7 " ((a1 + Zero = a1 == Zero = Zero) & P172 & P0) & P0 -> (a1 + Zero = a1 & P169 &  P167 & P166 & P164 & P0) & P0" 1;
pushreference 6 " (Real(a1) & P170 & P0) & (Real(Zero) & P171 & P0) & P0 -> ((a1 + Zero = a1 == Zero = Zero) &  P172 & P0) & P0" "NULLADD";
pushnode 5 "(Real(a1) & P165 & P164 & P0) & P0 -> (a1 + Zero = a1 & P169 &  P167 & P166 & P164 & P0) & P0" 4;
pushnode 4 "( Zero + a1 = a1 + Zero & P167 & P0) & ( Real(a1) & P165 & P164 & P0) & P0 -> ( Zero + a1 = a1 & P166 & P164 & P0) & P0" 1;
pushreference 3 "P0 -> ( Zero + a1 = a1 + Zero & P167 & P0) & P0" "CPLUS";
pushnode 2 "(Real(a1) & P165 & P164 & P0) & P0 ->  (Zero + a1 = a1 & P166 &  P164 & P0) & P0" 2;
THEOREMS:=("IPLUSb",(termtosequent(parseprop(" (Real(a1) &  P165 & P164 & P0) & P0 -> ( Zero + a1 = a1 & P166 & P164 & P0) & P0")),hd(!PROOFSTACK)))::(!THEOREMS);
PROOFSTACK:=nil;
td "IPLUSb";
pushreference 4 "P0 ->  ( a1 + Minus(a1) = Zero & P180 & P178 & P177 & P0) & P0" "MINUS";
pushnode 3 "( Minus(a1) + a1 = a1 + Minus(a1) &  P178 & P0) & P0 -> ( Minus(a1) + a1 = Zero & P177 & P0) & P0" 1;
pushreference 2 " P0 -> ( Minus(a1) + a1 = a1 + Minus(a1) & P178 & P0) & P0" "CPLUS";
pushnode 1 " P0 -> (Minus(a1) + a1 = Zero & P177 & P0) & P0" 2;
THEOREMS:=("MINUS2",(termtosequent(parseprop("P0 -> ( Minus(a1) + a1 = Zero & P177 & P0) & P0")),hd(!PROOFSTACK)))::(!THEOREMS);
PROOFSTACK:=nil;
td "MINUS2";
pushnode 62 "P0 -> ( a1 + Zero = a1 + Zero & P235 & P233 & P232 & P230 & P229 & P227 &  P213 & P0) & P0" 0;
pushnode 61 "( a2 + Minus(a2) = Zero & P233 & P0) & P0 ->  (a1 + a2 + Minus(a2) = a1 + Zero &  P232 & P230 & P229 & P227 & P213 & P0) & P0" 1;
pushreference 60 " P0 -> (a2 + Minus(a2) = Zero & P233 & P0) & P0" "MINUS";
pushnode 59 "P0 ->  (a1 + a2 + Minus(a2) = a1 + Zero &  P232 & P230 & P229 & P227 & P213 & P0) & P0" 2;
pushnode 58 "([ a1 + a2] + Minus(a2) = a1 + a2 + Minus(a2) &  P230 & P0) & P0 -> ([ a1 + a2] + Minus(a2) = a1 + Zero &  P229 & P227 & P213 & P0) & P0" 1;
pushreference 57 "P0 -> ( [a1 + a2] + Minus(a2) =  a1 + a2 + Minus(a2) & P230 & P0) & P0" "APLUS";
pushnode 56 "P0 ->  ([a1 + a2] + Minus(a2) =  a1 + Zero & P229 & P227 & P213 & P0) & P0" 2;
pushnode 55 "( Minus(a2) + a1 + a2 = [a1 + a2] + Minus(a2) & P227 & P0) & P0 -> ( Minus(a2) + a1 + a2 = a1 + Zero &  P213 & P0) & P0" 1;
pushreference 54 "P0 -> ( Minus(a2) + a1 + a2 = [a1 + a2] + Minus(a2) & P227 & P0) & P0" "CPLUS";
pushnode 39 "P0 ->  (Minus(a2) + a1 + a2 = a1 + Zero & P213 & P0) & P0" 2;
pushreference 53 " P0 ->  (Zero + a2 = a2 + Zero & P226 &  P224 & P223 & P221 & P215 & P0) & P0" "CPLUS";
pushnode 52 "( Minus(a1) + a1 = Zero & P224 & P0) & P0 ->  ([ Minus(a1) + a1] + a2 = a2 + Zero & P223 & P221 & P215 & P0) & P0" 1;
pushreference 51 "P0 -> ( Minus(a1) + a1 = Zero & P224 & P0) & P0" "MINUS2";
pushnode 50 " P0 ->  ([Minus(a1) + a1] + a2 = a2 + Zero & P223 & P221 & P215 & P0) & P0" 2;
pushnode 49 "([ Minus(a1) + a1] + a2 =  Minus(a1) + a1 + a2 &  P221 & P0) & P0 -> ( Minus(a1) + a1 + a2 = a2 + Zero &  P215 & P0) & P0" 1;
pushreference 48 "P0 -> ( [Minus(a1) + a1] + a2 = Minus(a1) + a1 + a2 & P221 & P0) & P0" "APLUS";
pushnode 42 " P0 -> ( Minus(a1) + a1 + a2 = a2 + Zero & P215 & P0) & P0" 2;
pushreference 47 " (( a1 + Zero < a2 + Zero -> a1 < a2) & P220 & P218 & P217 & P0) & ( a1 + Zero < a2 + Zero & P216 & P214 & P212 & P210 & P213 & P215 & P0) & P0 -> ( a1 < a2 & P209 & P184 & P182 & P181 & P0) & P0" "MP";
pushnode 46 "  (((a1 < a2 -> a1 + Zero < a2 + Zero) & ( a1 + Zero < a2 + Zero -> a1 < a2)) &  P218 & P217 & P0) &  (Minus(a1) + a1 + a2 = a2 + Zero & P215 & P0) & ( a1 + Zero < a2 + Zero & P216 & P214 & P212 & P210 & P213 & P215 & P0) &  (Minus(a2) + a1 + a2 = a1 + Zero & P213 & P0) & P0 -> (a1 < a2 & P209 & P184 & P182 &  P181 & P0) & P0" 1;
pushnode 45 " ((a1 < a2 == a1 + Zero < a2 + Zero) &  P217 & P0) & ( Minus(a1) + a1 + a2 = a2 + Zero &  P215 & P0) & (a1 + Zero < a2 + Zero & P216 &  P214 & P212 & P210 & P213 & P215 & P0) & ( Minus(a2) + a1 + a2 = a1 + Zero &  P213 & P0) & P0 -> (a1 < a2 & P209 & P184 & P182 & P181 & P0) & P0" 1;
pushreference 44 "P0 -> ((a1 < a2 == a1 + Zero < a2 + Zero) &  P217 & P0) & P0" "MPLUS0";
pushnode 43 " (Minus(a1) + a1 + a2 = a2 + Zero & P215 & P0) & ( a1 + Zero < a2 + Zero & P216 & P214 & P212 & P210 & P213 & P215 & P0) &  (Minus(a2) + a1 + a2 = a1 + Zero & P213 & P0) & P0 -> ( a1 < a2 & P209 & P184 & P182 & P181 & P0) & P0" 2;
pushnode 41 " (Minus(a1) + a1 + a2 = a2 + Zero & P215 & P0) & (a1 + Zero < Minus(a1) + a1 + a2 & P214 & P212 & P210 & P213 & P0) & (Minus(a2) + a1 + a2 = a1 + Zero &  P213 & P0) & P0 -> ( a1 < a2 & P209 & P184 & P182 & P181 & P0) & P0" 1;
pushnode 40 "(a1 + Zero < Minus(a1) + a1 + a2 & P214 & P212 & P210 & P213 & P0) & (Minus(a2) + a1 + a2 = a1 + Zero &  P213 & P0) & P0 -> (a1 < a2 &  P209 & P184 & P182 & P181 & P0) & P0" 2;
pushnode 38 "  (Minus(a2) + a1 + a2 = a1 + Zero & P213 & P0) &  (Minus(a2) + a1 + a2 < Minus(a1) + a1 + a2 &  P212 & P210 & P0) & P0 -> (a1 < a2 & P209 & P184 & P182 & P181 & P0) & P0" 1;
pushnode 37 "( Minus(a2) + a1 + a2 <  Minus(a1) + a1 + a2 & P212 & P210 & P0) & P0 -> (a1 < a2 & P209 & P184 & P182 & P181 & P0) & P0" 2;
pushnode 36 "(Minus(a2) < Minus(a1) & P208 &  P184 & P182 & P181 & P0) & P0 ->  (Minus(a2) < Minus(a1) & P211 & P210 & P0) & P0" 0;
pushnode 35 " (( Minus(a2) < Minus(a1) -> Minus(a2) + a1 + a2 < Minus(a1) + a1 + a2) &  P210 & P0) & ( Minus(a2) < Minus(a1) & P208 & P184 & P182 & P181 & P0) & P0 -> (a1 < a2 & P209 & P184 & P182 & P181 & P0) & P0" 2;
pushreference 34 "P0 -> ( (Minus(a2) < Minus(a1) -> Minus(a2) + a1 + a2 < Minus(a1) + a1 + a2) & P210 & P0) & P0" "MPLUS";
pushnode 33 "( Minus(a2) < Minus(a1) & P208 & P184 & P182 & P181 & P0) & P0 -> ( a1 < a2 & P209 & P184 & P182 & P181 & P0) & P0" 2;
pushnode 4 "P0 ->  ((Minus(a2) < Minus(a1) -> a1 < a2) & P184 & P182 & P181 & P0) & P0" 1;
pushreference 18 "P0 -> ( Real(Minus(a2)) & P195 & P0) & P0" "RMINUS";
pushreference 31 "P0 -> (Real(Minus(a1)) & P205 & P0) & P0" "RMINUS";
pushnode 32 "(Minus(a2) < Minus(a1) & P207 &  P204 & P202 & P199 & P197 & P194 & P192 & P189 & P185 & P190 & P193 & P196 &  P198 & P200 & P203 & P206 & P0) & ( a1 + Minus(a1) = Zero & P193 & P0) & ( Zero + Minus(a2) = Minus(a2) & P196 & P0) & (Minus(a1) + Minus(a2) = Minus(a2) + Minus(a1) &  P198 & P0) & (a2 + Minus(a2) = Zero & P203 & P0) & (Zero + Minus(a1) = Minus(a1) & P206 & P0) & P0 -> ( Minus(a2) < Minus(a1) & P187 & P183 & P182 & P181 & P0) & P0" 0;
pushnode 30 "( Zero + Minus(a1) = Minus(a1) &  P206 & P0) &  (Minus(a2) < Zero + Minus(a1) & P204 & P202 & P199 & P197 &  P194 & P192 & P189 & P185 & P190 & P193 & P196 & P198 & P200 & P203 & P0) & ( a1 + Minus(a1) = Zero & P193 & P0) & ( Zero + Minus(a2) = Minus(a2) &  P196 & P0) & ( Minus(a1) + Minus(a2) = Minus(a2) + Minus(a1) &  P198 & P0) & (a2 + Minus(a2) = Zero & P203 & P0) & P0 -> ( Minus(a2) < Minus(a1) & P187 & P183 & P182 & P181 & P0) & P0" 1;
pushreference 29 "( Real(Minus(a1)) & P205 & P0) & P0 -> ( Zero + Minus(a1) = Minus(a1) & P206 & P0) & P0" "IPLUSb";
pushnode 28 "( a2 + Minus(a2) = Zero & P203 & P0) & ( Minus(a2) < Zero + Minus(a1) & P204 & P202 & P199 & P197 &  P194 & P192 & P189 & P185 & P190 & P193 & P196 & P198 & P200 & P203 & P0) & ( a1 + Minus(a1) = Zero & P193 & P0) & ( Zero + Minus(a2) = Minus(a2) & P196 & P0) & (Minus(a1) + Minus(a2) = Minus(a2) + Minus(a1) &  P198 & P0) & P0 -> ( Minus(a2) < Minus(a1) & P187 & P183 & P182 & P181 & P0) & P0" 3;
pushnode 27 "( a2 + Minus(a2) = Zero & P203 & P0) &  (Minus(a2) <  [a2 + Minus(a2)] + Minus(a1) &  P202 & P199 & P197 & P194 & P192 & P189 & P185 & P190 & P193 & P196 & P198 &  P200 & P0) &  (a1 + Minus(a1) = Zero &  P193 & P0) & ( Zero + Minus(a2) = Minus(a2) & P196 & P0) & (Minus(a1) + Minus(a2) = Minus(a2) + Minus(a1) &  P198 & P0) & P0 -> ( Minus(a2) < Minus(a1) & P187 & P183 & P182 & P181 & P0) & P0" 1;
pushreference 26 " P0 -> (a2 + Minus(a2) = Zero & P203 & P0) & P0" "MINUS";
pushnode 25 "  (Minus(a2) < [a2 + Minus(a2)] + Minus(a1) & P202 & P199 & P197 & P194 &  P192 & P189 & P185 & P190 & P193 & P196 & P198 & P200 & P0) & ( a1 + Minus(a1) = Zero & P193 & P0) & ( Zero + Minus(a2) = Minus(a2) &  P196 & P0) & ( Minus(a1) + Minus(a2) = Minus(a2) + Minus(a1) &  P198 & P0) & P0 ->  (Minus(a2) < Minus(a1) & P187 & P183 &  P182 & P181 & P0) & P0" 2;
pushnode 24 "([ a2 + Minus(a2)] + Minus(a1) = a2 + Minus(a2) + Minus(a1) &  P200 & P0) & ( Minus(a2) < a2 +  Minus(a2) + Minus(a1) & P199 & P197 & P194 & P192 & P189 & P185 &  P190 & P193 & P196 & P198 & P0) & ( a1 + Minus(a1) = Zero & P193 & P0) & ( Zero + Minus(a2) = Minus(a2) & P196 & P0) & (Minus(a1) + Minus(a2) = Minus(a2) + Minus(a1) &  P198 & P0) & P0 -> ( Minus(a2) < Minus(a1) & P187 & P183 & P182 & P181 & P0) & P0" 1;
pushreference 23 " P0 ->  ( [a2 + Minus(a2)] + Minus(a1) =  a2 + Minus(a2) + Minus(a1) & P200 & P0) & P0" "APLUS";
pushnode 22 "( Minus(a1) + Minus(a2) = Minus(a2) + Minus(a1) &  P198 & P0) & ( Minus(a2) < a2 +  Minus(a2) + Minus(a1) & P199 & P197 & P194 & P192 & P189 & P185 &  P190 & P193 & P196 & P198 & P0) & ( a1 + Minus(a1) = Zero & P193 & P0) & ( Zero + Minus(a2) = Minus(a2) & P196 & P0) & P0 -> ( Minus(a2) < Minus(a1) & P187 & P183 & P182 & P181 & P0) & P0" 2;
pushnode 21 "( Minus(a1) + Minus(a2) = Minus(a2) + Minus(a1) &  P198 & P0) & ( Minus(a2) < a2 +  Minus(a1) + Minus(a2) & P197 & P194 & P192 & P189 & P185 & P190 &  P193 & P196 & P0) & ( a1 + Minus(a1) = Zero & P193 & P0) & ( Zero + Minus(a2) = Minus(a2) & P196 & P0) & P0 -> ( Minus(a2) < Minus(a1) & P187 & P183 & P182 & P181 & P0) & P0" 1;
pushreference 20 " P0 -> ( Minus(a1) + Minus(a2) = Minus(a2) + Minus(a1) &  P198 & P0) & P0" "CPLUS";
pushnode 19 "(Minus(a2) < a2 + Minus(a1) + Minus(a2) &  P197 & P194 & P192 & P189 & P185 & P190 & P193 & P196 & P0) & ( a1 + Minus(a1) = Zero & P193 & P0) & ( Zero + Minus(a2) = Minus(a2) & P196 & P0) & P0 -> ( Minus(a2) < Minus(a1) & P187 & P183 & P182 & P181 & P0) & P0" 2;
pushnode 17 "( Zero + Minus(a2) = Minus(a2) &  P196 & P0) & (Zero + Minus(a2) < a2 + Minus(a1) + Minus(a2) &  P194 & P192 & P189 & P185 & P190 & P193 & P0) & ( a1 + Minus(a1) = Zero & P193 & P0) & P0 -> ( Minus(a2) < Minus(a1) & P187 & P183 & P182 & P181 & P0) & P0" 1;
pushreference 16 "( Real(Minus(a2)) & P195 & P0) & P0 -> ( Zero + Minus(a2) = Minus(a2) & P196 & P0) & P0" "IPLUSb";
pushnode 15 "( a1 + Minus(a1) = Zero & P193 & P0) & ( Zero + Minus(a2) < a2 +  Minus(a1) + Minus(a2) & P194 & P192 & P189 & P185 & P190 & P193 & P0) & P0 -> ( Minus(a2) < Minus(a1) & P187 & P183 & P182 & P181 & P0) & P0" 3;
pushnode 14 "( a1 + Minus(a1) = Zero & P193 & P0) & ( [a1 + Minus(a1)] + Minus(a2) < a2 + Minus(a1) + Minus(a2) &  P192 & P189 & P185 & P190 & P0) & P0 -> ( Minus(a2) < Minus(a1) & P187 & P183 & P182 & P181 & P0) & P0" 1;
pushreference 13 " P0 -> (a1 + Minus(a1) = Zero & P193 & P0) & P0" "MINUS";
pushnode 12 "([a1 + Minus(a1)] + Minus(a2) < a2 + Minus(a1) + Minus(a2) &  P192 & P189 & P185 & P190 & P0) & P0 ->  (Minus(a2) < Minus(a1) & P187 & P183 &  P182 & P181 & P0) & P0" 2;
pushnode 11 " ([ a1 + Minus(a1)] + Minus(a2) = a1 + Minus(a1) + Minus(a2) &  P190 & P0) &  (a1 +  Minus(a1) + Minus(a2) <  a2 + Minus(a1) + Minus(a2) &  P189 & P185 & P0) & P0 -> (Minus(a2) < Minus(a1) &  P187 & P183 & P182 & P181 & P0) & P0" 1;
pushreference 10 "P0 -> ( [a1 + Minus(a1)] + Minus(a2) = a1 + Minus(a1) + Minus(a2) &  P190 & P0) & P0" "APLUS";
pushnode 9 " (a1 + Minus(a1) + Minus(a2) < a2 + Minus(a1) + Minus(a2) &  P189 & P185 & P0) & P0 -> ( Minus(a2) < Minus(a1) & P187 & P183 & P182 & P181 & P0) & P0" 2;
pushnode 8 "( a1 < a2 & P186 & P183 & P182 & P181 & P0) & P0 -> (a1 < a2 & P188 & P185 & P0) & P0" 0;
pushnode 7 "( (a1 < a2 -> a1 + Minus(a1) + Minus(a2) < a2 + Minus(a1) + Minus(a2)) & P185 & P0) & ( a1 < a2 & P186 & P183 & P182 & P181 & P0) & P0 -> ( Minus(a2) < Minus(a1) & P187 & P183 & P182 & P181 & P0) & P0" 2;
pushnode 6 "( ( a1 < a2 -> a1 + Minus(a1) + Minus(a2) < a2 + Minus(a1) + Minus(a2)) & P185 & P0) & P0 ->  ((a1 < a2 -> Minus(a2) < Minus(a1)) &  P183 & P182 & P181 & P0) & P0" 1;
pushreference 5 " P0 -> ( (a1 < a2 -> a1 + Minus(a1) + Minus(a2) < a2 + Minus(a1) + Minus(a2)) & P185 & P0) & P0" "MPLUS";
pushnode 3 "P0 ->  ((a1 < a2 -> Minus(a2) < Minus(a1)) &  P183 & P182 & P181 & P0) & P0" 2;
pushnode 2 " P0 -> ( ( (a1 < a2 -> Minus(a2) < Minus(a1)) & ( Minus(a2) < Minus(a1) -> a1 < a2)) & P182 & P181 & P0) & P0" 2;
pushnode 1 "P0 -> ( (a1 < a2 == Minus(a2) < Minus(a1)) & P181 & P0) & P0" 1;
THEOREMS:=("MINUSLESS",(termtosequent(parseprop(" P0 -> ( (a1 < a2 == Minus(a2) < Minus(a1)) & P181 & P0) & P0")),hd(!PROOFSTACK)))::(!THEOREMS);
PROOFSTACK:=nil;
td "MINUSLESS";
pushnode 15 "( a1 = a2 & P251 & P247 & P243 & P242 & P240 & P237 & P236 & P246 & P244 &  P250 & P248 & P0) & (a1 + Zero = a1 & P246 & P244 & P0) & ( a2 + Zero = a2 & P250 & P248 & P0) & P0 ->  (a1 = a2 &  P238 & P236 & P0) & P0" 0;
pushnode 14 "( a2 + Zero = a2 & P250 & P248 & P0) & (a1 =  a2 + Zero & P247 & P243 & P242 & P240 & P237 &  P236 & P246 & P244 & P0) & ( a1 + Zero = a1 & P246 & P244 & P0) & P0 ->  (a1 = a2 &  P238 & P236 & P0) & P0" 1;
pushnode 13 "( Real(a2) & P241 & P240 & P237 & P236 & P0) & P0 -> (Real(a2) & P249 & P248 & P0) & P0" 0;
pushnode 12 "((Real(a2) -> a2 + Zero = a2) &  P248 & P0) & (a1 + Zero = a1 & P246 & P244 & P0) & (a1 =  a2 + Zero & P247 & P243 & P242 & P240 & P237 &  P236 & P246 & P244 & P0) & ( Real(a2) & P241 & P240 & P237 & P236 & P0) & P0 -> ( a1 = a2 & P238 & P236 & P0) & P0" 2;
pushreference 11 "P0 -> ((Real(a2) -> a2 + Zero = a2) &  P248 & P0) & P0" "IPLUS";
pushnode 10 " (a1 + Zero = a1 & P246 &  P244 & P0) & (a1 = a2 + Zero & P247 & P243 & P242 &  P240 & P237 & P236 & P246 & P244 & P0) & ( Real(a2) & P241 & P240 & P237 & P236 & P0) & P0 ->  (a1 = a2 &  P238 & P236 & P0) & P0" 2;
pushnode 9 "( a1 + Zero = a1 & P246 & P244 & P0) & ( a1 + Zero = a2 + Zero &  P243 & P242 & P240 & P237 & P236 & P0) & ( Real(a2) & P241 & P240 & P237 & P236 & P0) & P0 ->  (a1 = a2 &  P238 & P236 & P0) & P0" 1;
pushnode 8 "( Real(a1) & P239 & P237 & P236 & P0) & P0 -> (Real(a1) & P245 & P244 & P0) & P0" 0;
pushnode 7 " ((Real(a1) -> a1 + Zero = a1) &  P244 & P0) &  (a1 + Zero = a2 + Zero & P243 &  P242 & P240 & P237 & P236 & P0) &  (Real(a1) & P239 & P237 & P236 & P0) & (Real(a2) & P241 & P240 & P237 & P236 & P0) & P0 -> (a1 = a2 & P238 & P236 & P0) & P0" 2;
pushreference 6 "P0 -> ((Real(a1) -> a1 + Zero = a1) &  P244 & P0) & P0" "IPLUS";
pushnode 5 "( a1 + Zero = a2 + Zero & P243 & P242 & P240 & P237 & P236 & P0) &  (Real(a1) &  P239 & P237 & P236 & P0) & (Real(a2) & P241 & P240 & P237 & P236 & P0) & P0 -> ( a1 = a2 & P238 & P236 & P0) & P0" 2;
pushnode 4 " (a1 Equal a2 & P242 & P240 & P237 & P236 & P0) & (Real(a1) & P239 & P237 &  P236 & P0) & (Real(a2) & P241 & P240 & P237 &  P236 & P0) & P0 -> (a1 = a2 & P238 & P236 & P0) & P0" 1;
THEOREMS:=("EQUALITY",(termtosequent(parseprop(" (a1 Equal a2 & P242 & P240 & P237 & P236 & P0) & (Real(a1) & P239 & P237 &  P236 & P0) & (Real(a2) & P241 & P240 & P237 &  P236 & P0) & P0 -> (a1 = a2 & P238 & P236 & P0) & P0")),hd(!PROOFSTACK)))::(!THEOREMS);
PROOFSTACK:=nil;
td "EQUALITY";
pushnode 19 " (a1 + Minus(a1) <  [a1 + Minus(a1)] + Minus(a1) &  P267 & P265 & P0) & P0 -> ( a1 + Minus(a1) < [a1 + Minus(a1)] + Minus(a1) & P258 & P0) & P0" 0;
pushnode 20 "( a1 < Zero & P256 & P253 & P252 & P0) & P0 -> (a1 < Zero & P269 & P257 & P266 & P265 & P0) & P0" 0;
pushnode 18 "( a1 + Minus(a1) = Zero & P257 & P0) & ( a1 < Zero & P256 & P253 & P252 & P0) & P0 -> ( a1 < a1 + Minus(a1) & P266 & P265 & P0) & P0" 1;
pushnode 17 " (( a1 < a1 + Minus(a1) -> a1 + Minus(a1) < [a1 + Minus(a1)] + Minus(a1)) &  P265 & P0) & (a1 + Minus(a1) = Zero & P257 & P0) & (a1 < Zero & P256 &  P253 & P252 & P0) & P0 -> ( a1 + Minus(a1) < [a1 + Minus(a1)] + Minus(a1) & P258 & P0) & P0" 2;
pushreference 16 " P0 -> ( (a1 < a1 + Minus(a1) -> a1 + Minus(a1) < [a1 + Minus(a1)] + Minus(a1)) & P265 & P0) & P0" "MPLUS";
pushnode 7 "( a1 + Minus(a1) = Zero & P257 & P0) & ( a1 < Zero & P256 & P253 & P252 & P0) & P0 -> ( a1 + Minus(a1) < [a1 + Minus(a1)] + Minus(a1) & P258 & P0) & P0" 2;
pushreference 14 " P0 ->  (Real(Minus(a1)) & P262 & P0) & P0" "RMINUS";
pushnode 15 " ( Zero < Minus(a1) & P264 & P261 & P259 & P258 & P257 & P260 & P263 & P0) & ( a1 + Minus(a1) = Zero & P257 & P0) & ( Zero + Minus(a1) = Minus(a1) + Zero &  P260 & P0) & ( Minus(a1) + Zero = Minus(a1) &  P263 & P0) & P0 ->  (Zero < Minus(a1) & P254 & P252 & P0) & P0" 0;
pushnode 13 " ( Minus(a1) + Zero = Minus(a1) &  P263 & P0) &  (Zero <  Minus(a1) + Zero & P261 & P259 &  P258 & P257 & P260 & P0) & ( a1 + Minus(a1) = Zero & P257 & P0) & ( Zero + Minus(a1) = Minus(a1) + Zero &  P260 & P0) & P0 ->  (Zero < Minus(a1) & P254 & P252 & P0) & P0" 1;
pushreference 12 "( Real(Minus(a1)) & P262 & P0) & P0 -> ( Minus(a1) + Zero = Minus(a1) & P263 & P0) & P0" "IPLUSa";
pushnode 11 "( Zero + Minus(a1) = Minus(a1) + Zero &  P260 & P0) &  (Zero <  Minus(a1) + Zero & P261 & P259 &  P258 & P257 & P260 & P0) & ( a1 + Minus(a1) = Zero & P257 & P0) & P0 -> ( Zero < Minus(a1) & P254 & P252 & P0) & P0" 3;
pushnode 10 " (Zero + Minus(a1) = Minus(a1) + Zero & P260 & P0) &  ( Zero < Zero + Minus(a1) & P259 & P258 & P257 & P0) & ( a1 + Minus(a1) = Zero & P257 & P0) & P0 -> ( Zero < Minus(a1) & P254 & P252 & P0) & P0" 1;
pushreference 9 "P0 ->  (Zero + Minus(a1) = Minus(a1) + Zero & P260 & P0) & P0" "CPLUS";
pushnode 8 "( a1 + Minus(a1) = Zero & P257 & P0) &  ( Zero < Zero + Minus(a1) & P259 & P258 & P257 & P0) & P0 -> ( Zero < Minus(a1) & P254 & P252 & P0) & P0" 2;
pushnode 6 " ( a1 + Minus(a1) = Zero & P257 & P0) & ( a1 + Minus(a1) < [a1 + Minus(a1)] + Minus(a1) & P258 & P0) & P0 ->  (Zero < Minus(a1) & P254 & P252 & P0) & P0" 1;
pushnode 5 "( a1 + Minus(a1) = Zero & P257 & P0) & ( a1 < Zero & P256 & P253 & P252 & P0) & P0 ->  (Zero < Minus(a1) & P254 &  P252 & P0) & P0" 2;
pushreference 4 "P0 -> (a1 + Minus(a1) = Zero & P257 & P0) & P0" "MINUS";
pushnode 3 "( a1 < Zero & P256 & P253 & P252 & P0) & P0 ->  (Zero < Minus(a1) & P254 & P252 & P0) & P0" 2;
THEOREMS:=("NEGINEQ",(termtosequent(parseprop("( a1 < Zero & P256 & P253 & P252 & P0) & P0 ->  (Zero < Minus(a1) & P254 & P252 & P0) & P0")),hd(!PROOFSTACK)))::(!THEOREMS);
PROOFSTACK:=nil;
td "NEGINEQ";
pushnode 28 "(a1 * Zero = Zero & P295 & P0) & P0 -> ( a1 * Zero = Zero & P294 & P292 & P291 &  P289 & P275 & P0) & P0" 0;
pushreference 27 "P0 -> ( a1 * Zero = Zero & P295 & P0) & P0" "MZERO";
pushnode 26 "P0 ->  (a1 * Zero = Zero &  P294 & P292 & P291 & P289 & P275 & P0) & P0" 2;
pushnode 25 "( a2 + Minus(a2) = Zero & P292 & P0) & P0 -> ( a1 * [a2 + Minus(a2)] = Zero &  P291 & P289 & P275 & P0) & P0" 1;
pushreference 24 "P0 -> ( a2 + Minus(a2) = Zero & P292 & P0) & P0" "MINUS";
pushnode 23 "P0 ->  (a1 * [a2 + Minus(a2)] = Zero &  P291 & P289 & P275 & P0) & P0" 2;
pushnode 22 "( a1 * [a2 + Minus(a2)] =  a1 * a2 + a1 * Minus(a2) &  P289 & P0) & P0 -> ( a1 * a2 + a1 * Minus(a2) = Zero &  P275 & P0) & P0" 1;
pushreference 21 "P0 -> (a1 * [a2 + Minus(a2)] = a1 * a2 + a1 * Minus(a2) &  P289 & P0) & P0" "DIST";
pushnode 5 "P0 -> (a1 * a2 + a1 * Minus(a2) = Zero &  P275 & P0) & P0" 2;
pushnode 20 " ( a2 + Minus(a2) = Zero & P280 & P0) & ( a1 * Zero = Zero & P282 & P0) & P0 -> (a1 * a2 + a1 * Minus(a2) = a1 * a2 + a1 * Minus(a2) &  P288 & P283 & P281 & P278 & P276 & P280 & P282 & P285 & P0) & P0" 0;
pushnode 19 "(Zero = a1 * a2 + a1 * Minus(a2) & P283 &  P281 & P278 & P276 & P280 & P282 & P0) & ( a2 + Minus(a2) = Zero & P280 & P0) & ( a1 * Zero = Zero & P282 & P0) & P0 -> ( a1 * a2 + a1 * Minus(a2) = Zero &  P285 & P0) & P0" 1;
pushreference 18 "P0 -> ( Real(a1 * Minus(a2)) & P284 & P0) & P0" "RTIMES";
pushnode 17 "( a1 * Minus(a2) = Minus(a1 * a2) & P286 & P0) & P0 ->  ( a1 * Minus(a2) = Minus(a1 * a2) &  P272 & P270 & P0) & P0" 0;
pushreference 16 "(Real( a1 * Minus(a2)) & P284 & P0) & (a1 * a2 +  a1 * Minus(a2) = Zero &  P285 & P0) & P0 -> (a1 * Minus(a2) = Minus(a1 * a2) &  P286 & P0) & P0" "UINV";
pushnode 15 " (a1 * Zero = Zero & P282 & P0) &  ( Zero = a1 * a2 + a1 * Minus(a2) & P283 & P281 & P278 & P276 & P280 & P282 & P0) & ( a2 + Minus(a2) = Zero & P280 & P0) & P0 -> ( a1 * Minus(a2) = Minus(a1 * a2) & P272 & P270 & P0) & P0" 4;
pushnode 14 " (a1 * Zero = Zero & P282 & P0) & ( a1 * Zero =  a1 * a2 + a1 * Minus(a2) & P281 & P278 & P276 & P280 & P0) & ( a2 + Minus(a2) = Zero & P280 & P0) & P0 -> ( a1 * Minus(a2) = Minus(a1 * a2) & P272 & P270 & P0) & P0" 1;
pushreference 13 "P0 -> (a1 * Zero = Zero &  P282 & P0) & P0" "MZERO";
pushnode 12 "( a2 + Minus(a2) = Zero & P280 & P0) & ( a1 * Zero = a1 * a2 + a1 * Minus(a2) & P281 &  P278 & P276 & P280 & P0) & P0 -> (a1 * Minus(a2) = Minus(a1 * a2) & P272 & P270 & P0) & P0" 2;
pushnode 11 " ( a2 + Minus(a2) = Zero & P280 & P0) &  ( a1 * [a2 + Minus(a2)] =  a1 * a2 + a1 * Minus(a2) &  P278 & P276 & P0) & P0 -> ( a1 * Minus(a2) = Minus(a1 * a2) & P272 & P270 & P0) & P0" 1;
pushreference 10 "P0 -> ( a2 + Minus(a2) = Zero & P280 & P0) & P0" "MINUS";
pushnode 9 " (a1 * [a2 + Minus(a2)] = a1 * a2 + a1 * Minus(a2) &  P278 & P276 & P0) & P0 ->  ( a1 * Minus(a2) = Minus(a1 * a2) &  P272 & P270 & P0) & P0" 2;
pushnode 7 "( a1 * [a2 + Minus(a2)] =  a1 * a2 + a1 * Minus(a2) &  P276 & P0) & P0 ->  ( a1 * Minus(a2) = Minus(a1 * a2) &  P272 & P270 & P0) & P0" 1;
pushreference 6 " P0 ->  ( a1 * [a2 + Minus(a2)] =  a1 * a2 + a1 * Minus(a2) & P276 & P0) & P0" "DIST";
pushnode 4 "P0 ->  ( a1 * Minus(a2) = Minus(a1 * a2) &  P272 & P270 & P0) & P0" 2;
pushnode 3 " P0 -> ( a1 * Minus(a2) = Minus(a1 * a2) & P272 & P270 & P0) & P0" 2;
THEOREMS:=("NEGCOMM",(termtosequent(parseprop("P0 -> ( a1 * Minus(a2) = Minus(a1 * a2) & P272 & P270 & P0) & P0")),hd(!PROOFSTACK)))::(!THEOREMS);
PROOFSTACK:=nil;
td "NEGCOMM";
pushnode 11 "  ( Minus(a1) + a1 = Zero & P301 & P299 & P300 & P0) & ( a1 + Minus(a1) = Minus(a1) + a1 & P300 & P0) & P0 -> ( Minus(a1) + a1 = Zero & P303 & P0) & P0" 0;
pushnode 10 "(Real(a1) & P297 & P296 & P0) & P0 ->  (Real(a1) & P302 & P0) & P0" 0;
pushnode 12 " P0 -> (a1 = a1 & P306 & P304 & P298 & P296 & P0) & P0" 0;
pushnode 9 " (a1 = Minus(Minus(a1)) & P304 & P0) & P0 ->  (Minus(Minus(a1)) = a1 & P298 &  P296 & P0) & P0" 1;
pushreference 8 " (Real(a1) &  P302 & P0) & ( Minus(a1) + a1 = Zero & P303 & P0) & P0 -> (a1 = Minus(Minus(a1)) & P304 & P0) & P0" "UINV";
pushnode 7 " (a1 + Minus(a1) = Minus(a1) + a1 & P300 & P0) &  ( Minus(a1) + a1 = Zero & P301 & P299 & P300 & P0) & (Real(a1) & P297 & P296 & P0) & P0 -> ( Minus(Minus(a1)) = a1 & P298 & P296 & P0) & P0" 4;
pushnode 6 "( a1 + Minus(a1) = Minus(a1) + a1 & P300 & P0) & ( a1 + Minus(a1) = Zero & P299 & P0) & ( Real(a1) & P297 & P296 & P0) & P0 -> ( Minus(Minus(a1)) = a1 & P298 & P296 & P0) & P0" 1;
pushreference 5 "P0 -> ( a1 + Minus(a1) = Minus(a1) + a1 & P300 & P0) & P0" "CPLUS";
pushnode 4 "( a1 + Minus(a1) = Zero & P299 & P0) &  (Real(a1) & P297 & P296 & P0) & P0 -> ( Minus(Minus(a1)) = a1 & P298 & P296 & P0) & P0" 2;
pushreference 3 "P0 -> ( a1 + Minus(a1) = Zero & P299 & P0) & P0" "MINUS";
pushnode 2 "(Real(a1) & P297 & P296 & P0) & P0 ->  (Minus(Minus(a1)) = a1 & P298 & P296 & P0) & P0" 2;
THEOREMS:=("DOUBLENEG",(termtosequent(parseprop(" (Real(a1) & P297 & P296 & P0) & P0 -> ( Minus(Minus(a1)) = a1 & P298 & P296 & P0) & P0")),hd(!PROOFSTACK)))::(!THEOREMS);
PROOFSTACK:=nil;
td "DOUBLENEG";
pushreference 16 "P0 -> (Real(a1 * a2) & P320 & P0) & P0" "RTIMES";
pushnode 15 "( Minus(Minus(a1 * a2)) = a1 * a2 & P321 & P0) & P0 ->  (Minus(Minus( a1 * a2)) = a1 * a2 & P319 &  P317 & P316 & P314 & P313 & P311 & P310 & P308 & P307 & P0) & P0" 0;
pushreference 14 "(Real(a1 * a2) & P320 & P0) & P0 -> ( Minus(Minus(a1 * a2)) = a1 * a2 & P321 & P0) & P0" "DOUBLENEG";
pushnode 13 " P0 -> ( Minus(Minus(a1 * a2)) = a1 * a2 & P319 & P317 & P316 &  P314 & P313 & P311 & P310 & P308 & P307 & P0) & P0" 3;
pushnode 12 "( a2 * a1 = a1 * a2 & P317 & P0) & P0 -> ( Minus(Minus(a2 * a1)) = a1 * a2 & P316 & P314 & P313 &  P311 & P310 & P308 & P307 & P0) & P0" 1;
pushreference 11 "P0 -> ( a2 * a1 = a1 * a2 & P317 & P0) & P0" "CTIMES";
pushnode 10 "P0 -> ( Minus(Minus(a2 * a1)) = a1 * a2 & P316 & P314 & P313 &  P311 & P310 & P308 & P307 & P0) & P0" 2;
pushnode 9 "( a2 * Minus(a1) = Minus(a2 * a1) & P314 & P0) & P0 ->  (Minus( a2 * Minus(a1)) = a1 * a2 &  P313 & P311 & P310 & P308 & P307 & P0) & P0" 1;
pushreference 8 " P0 -> ( a2 * Minus(a1) = Minus(a2 * a1) & P314 & P0) & P0" "NEGCOMM";
pushnode 7 " P0 -> ( Minus(a2 * Minus(a1)) = a1 * a2 & P313 & P311 & P310 &  P308 & P307 & P0) & P0" 2;
pushnode 6 " (Minus(a1) * a2 = a2 * Minus(a1) & P311 & P0) & P0 -> ( Minus(Minus(a1) * a2) = a1 * a2 & P310 & P308 & P307 & P0) & P0" 1;
pushreference 5 "P0 -> ( Minus(a1) * a2 = a2 * Minus(a1) &  P311 & P0) & P0" "CTIMES";
pushnode 4 "P0 -> ( Minus(Minus(a1) * a2) = a1 * a2 & P310 & P308 & P307 & P0) & P0" 2;
pushnode 3 "( Minus(a1) * Minus(a2) = Minus(Minus(a1) * a2) &  P308 & P0) & P0 -> ( Minus(a1) * Minus(a2) = a1 * a2 &  P307 & P0) & P0" 1;
pushreference 2 "P0 -> (Minus(a1) * Minus(a2) = Minus( Minus(a1) * a2) & P308 & P0) & P0" "NEGCOMM";
pushnode 1 "P0 ->  (Minus(a1) * Minus(a2) = a1 * a2 & P307 & P0) & P0" 2;
THEOREMS:=("TIMESDOUBNEG",(termtosequent(parseprop(" P0 -> ( Minus(a1) * Minus(a2) = a1 * a2 & P307 & P0) & P0")),hd(!PROOFSTACK)))::(!THEOREMS);
PROOFSTACK:=nil;
td "TIMESDOUBNEG";
pushnode 6 "( a3 < Zero & P325 & P323 & P322 & P0) & P0 ->  (a3 < Zero & P327 & P0) & P0" 0;
pushnode 28 "( a2 * a3 < a1 * a3 & P347 & P345 &  P341 & P339 & P344 & P346 & P0) & ( Minus(a2) * Minus(a3) = a2 * a3 &  P344 & P0) & ( Minus(a1) * Minus(a3) = a1 * a3 &  P346 & P0) & P0 -> ( a2 * a3 < a1 * a3 & P324 & P322 & P0) & P0" 0;
pushnode 27 "( Minus(a1) * Minus(a3) = a1 * a3 & P346 & P0) & (a2 * a3 <  Minus(a1) * Minus(a3) &  P345 & P341 & P339 & P344 & P0) & ( Minus(a2) * Minus(a3) = a2 * a3 &  P344 & P0) & P0 -> ( a2 * a3 < a1 * a3 & P324 & P322 & P0) & P0" 1;
pushreference 26 "P0 -> ( Minus(a1) * Minus(a3) = a1 * a3 & P346 & P0) & P0" "TIMESDOUBNEG";
pushnode 25 "( Minus(a2) * Minus(a3) = a2 * a3 &  P344 & P0) & (a2 * a3 <  Minus(a1) * Minus(a3) &  P345 & P341 & P339 & P344 & P0) & P0 -> ( a2 * a3 < a1 * a3 & P324 & P322 & P0) & P0" 2;
pushnode 24 " ( Minus(a2) * Minus(a3) = a2 * a3 & P344 & P0) &  (Minus(a2) * Minus(a3) < Minus(a1) * Minus(a3) &  P341 & P339 & P0) & P0 -> ( a2 * a3 < a1 * a3 & P324 & P322 & P0) & P0" 1;
pushreference 23 "P0 -> ( Minus(a2) * Minus(a3) = a2 * a3 & P344 & P0) & P0" "TIMESDOUBNEG";
pushnode 20 " ( Minus(a2) * Minus(a3) < Minus(a1) * Minus(a3) &  P341 & P339 & P0) & P0 -> ( a2 * a3 < a1 * a3 & P324 & P322 & P0) & P0" 2;
pushnode 22 " (Minus(a2) < Minus(a1) & P334 & P331 & P330 &  P329 & P0) & P0 ->  ( Minus(a2) < Minus(a1) & P343 & P340 & P339 & P0) & P0" 0;
pushnode 21 "( Zero < Minus(a3) & P328 & P0) & P0 -> (Zero < Minus(a3) & P342 & P340 & P339 & P0) & P0" 0;
pushnode 19 " ( Zero < Minus(a3) & P328 & P0) & ( Minus(a2) < Minus(a1) & P334 & P331 & P330 & P329 & P0) & P0 ->  ((Zero < Minus(a3) & Minus(a2) < Minus(a1)) &  P340 & P339 & P0) & P0" 2;
pushnode 18 "( ( Zero < Minus(a3) & Minus(a2) < Minus(a1) ->  Minus(a2) * Minus(a3) < Minus(a1) * Minus(a3)) &  P339 & P0) & ( Zero < Minus(a3) & P328 & P0) & ( Minus(a2) < Minus(a1) & P334 & P331 & P330 & P329 & P0) & P0 -> (a2 * a3 < a1 * a3 & P324 & P322 & P0) & P0" 2;
pushreference 17 "P0 -> ( (Zero < Minus(a3) & Minus(a2) < Minus(a1) ->  Minus(a2) * Minus(a3) < Minus(a1) * Minus(a3)) &  P339 & P0) & P0" "MTIMES";
pushnode 16 " (Zero < Minus(a3) & P328 & P0) & ( Minus(a2) < Minus(a1) & P334 & P331 & P330 & P329 & P0) & P0 -> ( a2 * a3 < a1 * a3 & P324 & P322 & P0) & P0" 2;
pushnode 15 " (Minus(a2) < Minus(a1) & P334 & P331 &  P330 & P329 & P0) & P0 -> ( Minus(a2) < Minus(a1) & P337 & P332 & P330 & P329 & P0) & P0" 0;
pushnode 12 "(( Minus(a2) < Minus(a1) -> a1 < a2) &  P332 & P330 & P329 & P0) & ( Zero < Minus(a3) & P328 & P0) & ( Minus(a2) < Minus(a1) & P334 & P331 & P330 & P329 & P0) & P0 -> (a2 * a3 < a1 * a3 & P324 & P322 & P0) & P0" 2;
pushnode 14 "(a1 < a2 & P336 & P332 & P330 & P329 & P0) & P0 -> ( a1 < a2 & P333 & P331 & P330 & P329 & P0) & P0" 0;
pushnode 13 " (a1 < a2 & P326 & P323 & P322 & P0) & P0 -> ( a1 < a2 & P333 & P331 & P330 & P329 & P0) & P0" 0;
pushnode 11 " ((Minus(a2) < Minus(a1) -> a1 < a2) & P332 & P330 & P329 & P0) &  (a1 < a2 & P326 & P323 & P322 & P0) & P0 -> ( a1 < a2 & P333 & P331 & P330 & P329 & P0) & P0" 2;
pushnode 10 " ((a1 < a2 -> Minus(a2) < Minus(a1)) &  P331 & P330 & P329 & P0) &  ((Minus(a2) < Minus(a1) -> a1 < a2) & P332 & P330 & P329 & P0) & (Zero < Minus(a3) & P328 & P0) & (a1 < a2 & P326 & P323 &  P322 & P0) & P0 -> ( a2 * a3 < a1 * a3 & P324 & P322 & P0) & P0" 2;
pushnode 9 "( ( (a1 < a2 -> Minus(a2) < Minus(a1)) & ( Minus(a2) < Minus(a1) -> a1 < a2)) & P330 & P329 & P0) & ( Zero < Minus(a3) & P328 & P0) & ( a1 < a2 & P326 & P323 & P322 & P0) & P0 -> (a2 * a3 < a1 * a3 & P324 & P322 & P0) & P0" 1;
pushnode 8 "((a1 < a2 == Minus(a2) < Minus(a1)) &  P329 & P0) & ( Zero < Minus(a3) & P328 & P0) & ( a1 < a2 & P326 & P323 & P322 & P0) & P0 -> (a2 * a3 < a1 * a3 & P324 & P322 & P0) & P0" 1;
pushreference 7 "P0 -> ((a1 < a2 == Minus(a2) < Minus(a1)) &  P329 & P0) & P0" "MINUSLESS";
pushnode 5 " (Zero < Minus(a3) & P328 & P0) & (a1 < a2 & P326 & P323 &  P322 & P0) & P0 -> ( a2 * a3 < a1 * a3 & P324 & P322 & P0) & P0" 2;
pushreference 4 " (a3 < Zero & P327 & P0) & P0 -> ( Zero < Minus(a3) & P328 & P0) & P0" "NEGINEQ";
pushnode 3 " (a3 < Zero & P325 & P323 & P322 & P0) &  (a1 < a2 & P326 & P323 & P322 & P0) & P0 -> ( a2 * a3 < a1 * a3 & P324 & P322 & P0) & P0" 3;
THEOREMS:=("MTIMESNEG",(termtosequent(parseprop(" (a3 < Zero & P325 & P323 & P322 & P0) &  (a1 < a2 & P326 & P323 & P322 & P0) & P0 -> ( a2 * a3 < a1 * a3 & P324 & P322 & P0) & P0")),hd(!PROOFSTACK)))::(!THEOREMS);
PROOFSTACK:=nil;
td "MTIMESNEG";
pushnode 42 " (Zero < a1 * a1 & P384 & P378 & P376 &  P383 & P381 & P382 & P0) & ( a1 * Zero = Zero * a1 &  P382 & P0) &  (Zero * a1 = Zero & P383 & P381 & P382 & P0) & P0 -> (Zero < a1 * a1 & P353 &  P351 & P350 & P348 & P0) & P0" 0;
pushnode 41 " (Zero * a1 = Zero & P383 &  P381 & P382 & P0) & (Zero * a1 < a1 * a1 & P378 & P376 & P0) & ( a1 * Zero = Zero * a1 &  P382 & P0) & P0 ->  (Zero < a1 * a1 & P353 & P351 &  P350 & P348 & P0) & P0" 1;
pushnode 40 "( a1 * Zero = Zero * a1 &  P382 & P0) & (a1 * Zero = Zero & P381 & P0) & (Zero * a1 < a1 * a1 & P378 & P376 & P0) & P0 -> ( Zero < a1 * a1 & P353 & P351 & P350 & P348 & P0) & P0" 1;
pushreference 39 " P0 -> (a1 * Zero = Zero * a1 & P382 & P0) & P0" "CTIMES";
pushnode 38 "(a1 * Zero = Zero & P381 & P0) & (Zero * a1 < a1 * a1 & P378 & P376 & P0) & P0 -> ( Zero < a1 * a1 & P353 & P351 & P350 & P348 & P0) & P0" 2;
pushreference 37 " P0 -> (a1 * Zero = Zero & P381 & P0) & P0" "MZERO";
pushnode 34 "( Zero * a1 < a1 * a1 & P378 & P376 & P0) & P0 ->  (Zero < a1 * a1 & P353 & P351 &  P350 & P348 & P0) & P0" 2;
pushnode 36 "( Zero < a1 & P368 & P356 & P354 & P0) & P0 ->  (Zero < a1 & P380 & P377 & P376 & P0) & P0" 0;
pushnode 35 "( Zero < a1 & P368 & P356 & P354 & P0) & P0 ->  (Zero < a1 & P379 & P377 & P376 & P0) & P0" 0;
pushnode 33 "( Zero < a1 & P368 & P356 & P354 & P0) & P0 -> ( (Zero < a1 & Zero < a1) & P377 & P376 & P0) & P0" 2;
pushnode 32 "(( Zero < a1 & Zero < a1 -> Zero * a1 < a1 * a1) &  P376 & P0) & ( Zero < a1 & P368 & P356 & P354 & P0) & P0 -> ( Zero < a1 * a1 & P353 & P351 & P350 & P348 & P0) & P0" 2;
pushreference 31 " P0 -> ( (Zero < a1 & Zero < a1 ->  Zero * a1 < a1 * a1) & P376 & P0) & P0" "MTIMES";
pushnode 20 " (Zero < a1 & P368 & P356 & P354 & P0) & P0 -> (Zero < a1 * a1 & P353 & P351 & P350 & P348 & P0) & P0" 2;
pushnode 24 " (a1 < Zero & P367 & P356 & P354 & P0) & P0 -> ( a1 < Zero & P370 & P0) & P0" 0;
pushnode 23 " (a1 < Zero & P367 & P356 & P354 & P0) & P0 -> ( a1 < Zero & P369 & P0) & P0" 0;
pushnode 30 "  (Zero < a1 * a1 & P375 & P371 &  P374 & P372 & P373 & P0) & ( a1 * Zero = Zero * a1 & P373 & P0) & ( Zero * a1 = Zero & P374 & P372 & P373 & P0) & P0 -> (Zero < a1 * a1 & P353 & P351 & P350 &  P348 & P0) & P0" 0;
pushnode 29 "(Zero * a1 = Zero & P374 &  P372 & P373 & P0) & (Zero * a1 < a1 * a1 & P371 & P0) &  (a1 * Zero = Zero * a1 & P373 & P0) & P0 -> (Zero <  a1 * a1 & P353 & P351 & P350 & P348 & P0) & P0" 1;
pushnode 28 "( a1 * Zero = Zero * a1 & P373 & P0) & ( a1 * Zero = Zero & P372 & P0) &  (Zero * a1 < a1 * a1 & P371 & P0) & P0 -> (Zero <  a1 * a1 & P353 & P351 & P350 & P348 & P0) & P0" 1;
pushreference 27 "P0 -> ( a1 * Zero = Zero * a1 & P373 & P0) & P0" "CTIMES";
pushnode 26 "(a1 * Zero = Zero & P372 & P0) & ( Zero * a1 < a1 * a1 & P371 & P0) & P0 -> ( Zero < a1 * a1 & P353 & P351 & P350 & P348 & P0) & P0" 2;
pushreference 25 " P0 -> (a1 * Zero = Zero & P372 & P0) & P0" "MZERO";
pushnode 22 "( Zero * a1 < a1 * a1 & P371 & P0) & P0 ->  (Zero < a1 * a1 & P353 & P351 &  P350 & P348 & P0) & P0" 2;
pushreference 21 "( a1 < Zero & P369 & P0) & ( a1 < Zero & P370 & P0) & P0 -> ( Zero * a1 < a1 * a1 & P371 & P0) & P0" "MTIMESNEG";
pushnode 19 " (a1 < Zero & P367 & P356 & P354 & P0) & P0 -> (Zero < a1 * a1 & P353 & P351 & P350 & P348 & P0) & P0" 4;
pushnode 8 "( (a1 < Zero v Zero < a1) & P356 & P354 & P0) & P0 ->  (Zero < a1 * a1 & P353 & P351 &  P350 & P348 & P0) & P0" 2;
pushreference 13 " P0 ->  (Real(Zero) & P359 & P0) & P0" "RZERO";
pushnode 12 "( Real(a1) & P349 & P348 & P0) & P0 ->  (Real(a1) & P358 & P0) & P0" 0;
pushnode 11 "( a1 Equal Zero & P355 & P354 & P0) & P0 -> (a1 Equal Zero & P357 & P0) & P0" 0;
pushnode 18 "(Zero Equal Zero & P366 & P355 & P354 &  P361 & P360 & P0) & ( a1 = Zero & P361 & P360 & P0) & P0 -> (Zero Equal Zero & P365 &  P363 & P362 & P360 & P352 & P351 & P350 & P348 & P0) & P0" 0;
pushnode 17 " (a1 = Zero & P361 & P360 & P0) &  (a1 Equal Zero & P355 & P354 & P0) & P0 -> ( Zero Equal Zero & P365 & P363 & P362 & P360 & P352 & P351 & P350 &  P348 & P0) & P0" 1;
pushnode 16 " (Zero * Zero = Zero &  P363 & P0) & ( a1 = Zero & P361 & P360 & P0) & ( a1 Equal Zero & P355 & P354 & P0) & P0 -> (Zero Equal Zero * Zero & P362 &  P360 & P352 & P351 & P350 & P348 & P0) & P0" 1;
pushreference 15 "P0 -> ( Zero * Zero = Zero & P363 & P0) & P0" "MZERO";
pushnode 14 " (a1 = Zero & P361 & P360 & P0) &  (a1 Equal Zero & P355 & P354 & P0) & P0 ->  (Zero Equal  Zero * Zero & P362 & P360 & P352 & P351 &  P350 & P348 & P0) & P0" 2;
pushnode 10 "( a1 = Zero & P360 & P0) & ( a1 Equal Zero & P355 & P354 & P0) & P0 -> ( Zero Equal a1 * a1 & P352 & P351 & P350 & P348 & P0) & P0" 1;
pushreference 9 "( a1 Equal Zero & P357 & P0) & ( Real(a1) & P358 & P0) & ( Real(Zero) & P359 & P0) & P0 -> (a1 = Zero &  P360 & P0) & P0" "EQUALITY";
pushnode 7 " (a1 Equal Zero & P355 & P354 & P0) & (Real(a1) & P349 & P348 & P0) & P0 -> ( Zero Equal a1 * a1 & P352 & P351 & P350 & P348 & P0) & P0" 5;
pushnode 6 "(( a1 Equal Zero v a1 < Zero v Zero < a1) &  P354 & P0) & ( Real(a1) & P349 & P348 & P0) & P0 -> ( Zero Equal a1 * a1 & P352 & P351 & P350 & P348 & P0) & ( Zero < a1 * a1 & P353 & P351 & P350 & P348 & P0) & P0" 2;
pushreference 5 "P0 -> ( (a1 Equal Zero v a1 < Zero v Zero < a1) & P354 & P0) & P0" "TRI";
pushnode 4 "(Real(a1) & P349 & P348 & P0) & P0 -> (Zero Equal a1 * a1 & P352 &  P351 & P350 & P348 & P0) & (Zero <  a1 * a1 & P353 & P351 & P350 & P348 & P0) & P0" 2;
pushnode 3 "( Real(a1) & P349 & P348 & P0) & P0 -> ( (Zero Equal a1 * a1 v Zero < a1 * a1) & P351 & P350 & P348 & P0) & P0" 1;
pushnode 2 "(Real(a1) & P349 & P348 & P0) & P0 ->  (Zero <= a1 * a1 & P350 & P348 & P0) & P0" 1;
THEOREMS:=("SQUARENONNEG",(termtosequent(parseprop(" (Real(a1) & P349 & P348 & P0) & P0 -> ( Zero <= a1 * a1 & P350 & P348 & P0) & P0")),hd(!PROOFSTACK)))::(!THEOREMS);
PROOFSTACK:=nil;
td "SQUARENONNEG";
pushreference 4 "P0 ->  (a1 * Zero = Zero &  P388 & P386 & P385 & P0) & P0" "MZERO";
pushnode 3 "( Zero * a1 = a1 * Zero &  P386 & P0) & P0 -> ( Zero * a1 = Zero & P385 & P0) & P0" 1;
pushreference 2 " P0 -> (Zero * a1 = a1 * Zero & P386 & P0) & P0" "CTIMES";
pushnode 1 "P0 -> (Zero * a1 = Zero & P385 & P0) & P0" 2;
THEOREMS:=("MZERO2",(termtosequent(parseprop("P0 -> (Zero * a1 = Zero & P385 & P0) & P0")),hd(!PROOFSTACK)))::(!THEOREMS);
PROOFSTACK:=nil;
td "MZERO2";
pushnode 5 "P0 -> ( a2 + Zero = a2 + Zero & P395 & P393 & P390 & P389 & P392 & P391 &  P389 & P0) & P0" 0;
pushnode 4 " ( a1 + Zero = a2 + Zero & P393 & P390 & P389 & P0) & P0 -> (a2 + Zero = a1 + Zero & P392 &  P391 & P389 & P0) & P0" 1;
pushnode 3 " (a1 Equal a2 & P390 & P389 & P0) & P0 ->  ( a2 + Zero = a1 + Zero & P392 & P391 & P389 & P0) & P0" 1;
pushnode 2 "( a1 Equal a2 & P390 & P389 & P0) & P0 ->  (a2 Equal a1 & P391 & P389 & P0) & P0" 1;
THEOREMS:=("EqualSymm",(termtosequent(parseprop("( a1 Equal a2 & P390 & P389 & P0) & P0 ->  (a2 Equal a1 & P391 & P389 & P0) & P0")),hd(!PROOFSTACK)))::(!THEOREMS);
PROOFSTACK:=nil;
td "EqualSymm";
pushreference 9 "P0 -> (Real( One * Inv(One)) & P403 & P401 &  P397 & P396 & P0) & P0" "RTIMES";
pushnode 8 "( One * Inv(One) = One & P401 & P397 & P0) & P0 ->  (Real(One) & P396 & P0) & P0" 1;
pushreference 7 "( One Equal Zero & P400 & P397 & P0) & P0 ->  (Zero Equal One & P399 & P398 & P0) & P0" "EqualSymm";
pushnode 6 "(( One Equal Zero v One * Inv(One) = One) &  P397 & P0) & P0 -> ( Zero Equal One & P399 & P398 & P0) & ( Real(One) & P396 & P0) & P0" 2;
pushnode 5 "(~Zero Equal One & P398 & P0) & ( (One Equal Zero v One * Inv(One) = One) & P397 & P0) & P0 -> (Real(One) & P396 & P0) & P0" 1;
pushreference 4 "P0 -> (~Zero Equal One & P398 & P0) & P0" "NONTRIV";
pushnode 3 "( (One Equal Zero v One * Inv(One) = One) & P397 & P0) & P0 ->  (Real(One) & P396 & P0) & P0" 2;
pushreference 2 " P0 -> ((One Equal Zero v One * Inv(One) = One) &  P397 & P0) & P0" "INV";
pushnode 1 "P0 -> (Real(One) & P396 & P0) & P0" 2;
THEOREMS:=("REALONE",(termtosequent(parseprop("P0 -> (Real(One) & P396 & P0) & P0")),hd(!PROOFSTACK)))::(!THEOREMS);
PROOFSTACK:=nil;
td "REALONE";
pushnode 12 "(a2 < a2 & P410 & P408 & P0) & P0 -> (a2 < a2 & P414 & P413 & P0) & P0" 0;
pushnode 11 " (~a2 < a2 & P413 & P0) & (a2 < a2 & P410 & P408 & P0) & P0 -> P0" 1;
pushreference 10 "P0 -> (~a2 < a2 & P413 & P0) & P0" "IRR";
pushnode 7 "(a2 < a2 & P410 & P408 & P0) & P0 -> P0" 2;
pushnode 9 "(a1 < a2 & P405 & P404 & P0) & P0 ->  (a1 < a2 & P412 & P409 & P408 & P0) & P0" 0;
pushnode 8 "( a2 < a1 & P407 & P406 & P404 & P0) & P0 ->  (a2 < a1 & P411 & P409 & P408 & P0) & P0" 0;
pushnode 6 "( a2 < a1 & P407 & P406 & P404 & P0) & ( a1 < a2 & P405 & P404 & P0) & P0 -> ( (a2 < a1 & a1 < a2) & P409 & P408 & P0) & P0" 2;
pushnode 5 "(( a2 < a1 & a1 < a2 -> a2 < a2) &  P408 & P0) &  (a2 < a1 &  P407 & P406 & P404 & P0) & (a1 < a2 & P405 & P404 & P0) & P0 -> P0" 2;
pushreference 4 "P0 -> (( a2 < a1 & a1 < a2 -> a2 < a2) & P408 & P0) & P0" "TRANS";
pushnode 3 "( a2 < a1 & P407 & P406 & P404 & P0) & ( a1 < a2 & P405 & P404 & P0) & P0 -> P0" 2;
THEOREMS:=("NOTBOTH",(termtosequent(parseprop(" (a2 < a1 & P407 &  P406 & P404 & P0) &  (a1 < a2 &  P405 & P404 & P0) & P0 -> P0")),hd(!PROOFSTACK)))::(!THEOREMS);
PROOFSTACK:=nil;
td "NOTBOTH";
pushnode 12 " (a2 + Zero < a2 + Zero & P423 & P422 & P420 & P419 & P416 & P415 & P0) &  ( a1 + Zero = a2 + Zero & P419 & P416 & P415 & P0) & P0 -> ( a2 + Zero < a2 + Zero & P425 & P424 & P0) & P0" 0;
pushnode 11 "( ~a2 + Zero < a2 + Zero & P424 & P0) & ( a1 + Zero = a2 + Zero &  P419 & P416 & P415 & P0) & ( a2 + Zero < a2 + Zero &  P423 & P422 & P420 & P419 & P416 & P415 & P0) & P0 -> P0" 1;
pushreference 10 "P0 -> (~a2 + Zero < a2 + Zero & P424 & P0) & P0" "IRR";
pushnode 9 "( a1 + Zero = a2 + Zero &  P419 & P416 & P415 & P0) & ( a2 + Zero < a2 + Zero &  P423 & P422 & P420 & P419 & P416 & P415 & P0) & P0 -> P0" 2;
pushnode 8 " (a1 + Zero = a2 + Zero & P419 & P416 & P415 & P0) & ( a1 + Zero < a2 + Zero & P422 & P420 & P0) & P0 -> P0" 1;
pushnode 7 " (a1 < a2 & P418 &  P417 & P415 & P0) & P0 -> (a1 < a2 & P421 & P420 & P0) & P0" 0;
pushnode 6 "((a1 < a2 -> a1 + Zero < a2 + Zero) &  P420 & P0) & (a1 + Zero = a2 + Zero & P419 &  P416 & P415 & P0) &  (a1 < a2 &  P418 & P417 & P415 & P0) & P0 -> P0" 2;
pushreference 5 "P0 -> ((a1 < a2 -> a1 + Zero < a2 + Zero) &  P420 & P0) & P0" "MPLUS";
pushnode 4 " ( a1 + Zero = a2 + Zero & P419 & P416 & P415 & P0) &  (a1 < a2 & P418 & P417 & P415 & P0) & P0 -> P0" 2;
pushnode 3 "(a1 Equal a2 & P416 & P415 & P0) & ( a1 < a2 & P418 & P417 & P415 & P0) & P0 -> P0" 1;
THEOREMS:=("NOTBOTH2",(termtosequent(parseprop(" (a1 Equal a2 &  P416 & P415 & P0) &  (a1 < a2 & P418 & P417 & P415 & P0) & P0 -> P0")),hd(!PROOFSTACK)))::(!THEOREMS);
PROOFSTACK:=nil;
td "NOTBOTH2";
pushnode 6 "(a1 Equal a2 & P427 & P426 & P0) & P0 -> (a1 Equal a2 & P430 & P0) & P0" 0;
pushreference 5 " (a2 Equal a1 & P431 & P0) & (a2 < a1 & P429 & P428 &  P426 & P0) & P0 -> P0" "NOTBOTH2";
pushreference 4 " (a1 Equal a2 & P430 & P0) & P0 -> (a2 Equal a1 & P431 & P0) & P0" "EqualSymm";
pushnode 3 " (a2 < a1 & P429 & P428 & P426 & P0) &  (a1 Equal a2 & P427 & P426 & P0) & P0 -> P0" 3;
THEOREMS:=("NOTBOTH3",(termtosequent(parseprop(" (a2 < a1 & P429 & P428 & P426 & P0) &  (a1 Equal a2 & P427 & P426 & P0) & P0 -> P0")),hd(!PROOFSTACK)))::(!THEOREMS);
PROOFSTACK:=nil;
td "NOTBOTH3";
pushreference 4 "P0 ->  (Real(One) & P433 & P0) & P0" "REALONE";
pushnode 12 " (Zero <  One * One & P442 & P440 & P434 & P0) & P0 -> (Zero < One * One & P439 & P437 & P435 & P432 & P0) & P0" 0;
pushnode 16 "  (Zero Equal One & P443 & P441 & P440 &  P434 & P438 & P437 & P435 & P0) &  (One * One = One &  P438 & P437 & P435 & P0) & P0 ->  (Zero Equal One & P445 &  P444 & P0) & P0" 0;
pushnode 15 "( ~Zero Equal One & P444 & P0) & ( One * One = One & P438 & P437 & P435 & P0) &  (Zero Equal One & P443 & P441 & P440 &  P434 & P438 & P437 & P435 & P0) & P0 -> P0" 1;
pushreference 14 "P0 ->  (~Zero Equal One & P444 & P0) & P0" "NONTRIV";
pushnode 13 " ( One * One = One & P438 & P437 & P435 & P0) &  (Zero Equal One & P443 & P441 & P440 &  P434 & P438 & P437 & P435 & P0) & P0 -> P0" 2;
pushnode 11 "( One * One = One & P438 & P437 & P435 & P0) &  (Zero Equal  One * One & P441 & P440 & P434 & P0) & P0 -> P0" 1;
pushnode 10 " ((Zero Equal One * One v Zero < One * One) &  P440 & P434 & P0) & (One * One = One & P438 &  P437 & P435 & P0) & P0 -> (Zero <  One * One & P439 & P437 & P435 & P432 & P0) & P0" 2;
pushnode 9 " (Zero <= One * One &  P434 & P0) &  (One * One = One & P438 & P437 & P435 & P0) & P0 -> (Zero < One * One &  P439 & P437 & P435 & P432 & P0) & P0" 1;
pushnode 8 " (One * One = One & P437 &  P435 & P0) & (Zero <= One * One & P434 & P0) & P0 -> ( Zero < One & P432 & P0) & P0" 1;
pushreference 7 "P0 ->  (Real(One) & P436 & P435 & P0) & P0" "REALONE";
pushnode 6 " (( Real(One) -> One * One = One) &  P435 & P0) &  (Zero <= One * One & P434 & P0) & P0 -> (Zero < One & P432 & P0) & P0" 2;
pushreference 5 "P0 -> ((Real(One) -> One * One = One) &  P435 & P0) & P0" "ITIMES";
pushnode 3 " (Zero <= One * One & P434 & P0) & P0 ->  (Zero < One & P432 & P0) & P0" 2;
pushreference 2 "( Real(One) & P433 & P0) & P0 -> (Zero <= One * One & P434 & P0) & P0" "SQUARENONNEG";
pushnode 1 "P0 ->  (Zero < One & P432 & P0) & P0" 3;
THEOREMS:=("ZEROLESSONE",(termtosequent(parseprop(" P0 ->  (Zero < One & P432 & P0) & P0")),hd(!PROOFSTACK)))::(!THEOREMS);
PROOFSTACK:=nil;
td "ZEROLESSONE";
pushreference 17 " P0 -> (a1 * a2 = a2 * a1 & P461 & P459 & P457 &  P456 & P454 & P453 & P451 & P450 & P448 & P446 & P0) & P0" "CTIMES";
pushnode 16 "( a2 * a1 + Zero = a2 * a1 & P459 & P457 & P0) & P0 -> ( a1 * a2 = a2 * a1 + Zero & P456 & P454 & P453 & P451 & P450 &  P448 & P446 & P0) & P0" 1;
pushreference 15 "P0 ->  (Real(a2 * a1) &  P458 & P457 & P0) & P0" "RTIMES";
pushnode 14 "((Real( a2 * a1) -> a2 * a1 + Zero = a2 * a1) & P457 & P0) & P0 -> ( a1 * a2 = a2 * a1 + Zero &  P456 & P454 & P453 & P451 & P450 & P448 & P446 & P0) & P0" 2;
pushreference 13 "P0 -> ( (Real(a2 * a1) ->  a2 * a1 + Zero = a2 * a1) & P457 & P0) & P0" "IPLUS";
pushnode 12 " P0 -> ( a1 * a2 = a2 * a1 + Zero & P456 & P454 & P453 & P451 & P450 &  P448 & P446 & P0) & P0" 2;
pushnode 11 "( a2 * Zero = Zero & P454 & P0) & P0 ->  (a1 * a2 = a2 * a1 + a2 * Zero & P453 & P451 & P450 & P448 &  P446 & P0) & P0" 1;
pushreference 10 "P0 -> (a2 * Zero = Zero & P454 & P0) & P0" "MZERO";
pushnode 9 " P0 -> ( a1 * a2 = a2 * a1 + a2 * Zero & P453 & P451 & P450 & P448 &  P446 & P0) & P0" 2;
pushnode 8 "( a2 * [a1 + Zero] = a2 * a1 + a2 * Zero & P451 & P0) & P0 -> (a1 * a2 = a2 * [a1 + Zero] & P450 & P448 & P446 & P0) & P0" 1;
pushreference 7 "P0 -> (a2 * [a1 + Zero] = a2 * a1 + a2 * Zero & P451 & P0) & P0" "DIST";
pushnode 6 "P0 -> (a1 * a2 = a2 * [a1 + Zero] & P450 & P448 & P446 & P0) & P0" 2;
pushnode 5 "([a1 + Zero] * a2 = a2 * [a1 + Zero] & P448 & P0) & P0 -> ( a1 * a2 = [a1 + Zero] * a2 &  P446 & P0) & P0" 1;
pushreference 4 "P0 -> ( [a1 + Zero] * a2 = a2 * [ a1 + Zero] & P448 & P0) & P0" "CTIMES";
pushnode 1 "P0 ->  (a1 * a2 = [a1 + Zero] * a2 & P446 & P0) & P0" 2;
THEOREMS:=("SubLemma",(termtosequent(parseprop(" P0 -> ( a1 * a2 = [a1 + Zero] * a2 & P446 & P0) & P0")),hd(!PROOFSTACK)))::(!THEOREMS);
PROOFSTACK:=nil;
td "SubLemma";
pushnode 26 "( a1 * a1 < a2 * a2 & P487 & P485 & P0) & P0 -> ( a1 * a1 < a2 * a2 & P472 & P469 &  P466 & P465 & P463 & P0) & P0" 0;
pushnode 28 "( a1 * a2 < a2 * a2 & P475 & P473 & P0) & P0 ->  ( a1 * a2 < a2 * a2 & P489 & P486 & P485 & P0) & P0" 0;
pushnode 27 " (a1 * a1 < a1 * a2 & P484 & P480 & P478 &  P483 & P0) &  (a2 * a1 =  a1 * a2 & P483 & P0) & P0 ->  ( a1 * a1 < a1 * a2 & P488 & P486 & P485 & P0) & P0" 0;
pushnode 25 "(a2 * a1 = a1 * a2 & P483 & P0) & ( a1 * a1 < a1 * a2 & P484 & P480 & P478 & P483 & P0) & ( a1 * a2 < a2 * a2 & P475 & P473 & P0) & P0 ->  ((a1 * a1 < a1 * a2 & a1 * a2 < a2 * a2) &  P486 & P485 & P0) & P0" 2;
pushnode 24 "(( a1 * a1 < a1 * a2 & a1 * a2 < a2 * a2 -> a1 * a1 < a2 * a2) &  P485 & P0) &  (a2 * a1 =  a1 * a2 & P483 & P0) & ( a1 * a1 < a1 * a2 & P484 & P480 & P478 & P483 & P0) & ( a1 * a2 < a2 * a2 & P475 & P473 & P0) & P0 -> ( a1 * a1 < a2 * a2 & P472 & P469 &  P466 & P465 & P463 & P0) & P0" 2;
pushreference 23 "P0 -> (( a1 * a1 < a1 * a2 & a1 * a2 < a2 * a2 ->  a1 * a1 < a2 * a2) &  P485 & P0) & P0" "TRANS";
pushnode 22 "( a2 * a1 = a1 * a2 & P483 & P0) & ( a1 * a1 < a1 * a2 & P484 & P480 &  P478 & P483 & P0) & ( a1 * a2 < a2 * a2 & P475 & P473 & P0) & P0 -> ( a1 * a1 < a2 * a2 & P472 & P469 & P466 & P465 & P463 & P0) & P0" 2;
pushnode 21 "( a2 * a1 = a1 * a2 & P483 & P0) & ( a1 * a1 < a2 * a1 & P480 & P478 & P0) & (a1 * a2 < a2 * a2 & P475 & P473 & P0) & P0 -> (a1 * a1 < a2 * a2 & P472 & P469 & P466 & P465 & P463 & P0) & P0" 1;
pushreference 20 "P0 -> ( a2 * a1 = a1 * a2 & P483 & P0) & P0" "CTIMES";
pushnode 17 " ( a1 * a1 < a2 * a1 & P480 & P478 & P0) & ( a1 * a2 < a2 * a2 & P475 & P473 & P0) & P0 ->  (a1 * a1 < a2 * a2 &  P472 & P469 & P466 & P465 & P463 & P0) & P0" 2;
pushnode 19 "( a1 < a2 & P471 & P469 & P466 & P465 & P463 & P0) & P0 ->  (a1 < a2 & P482 & P479 & P478 & P0) & P0" 0;
pushnode 18 "( Zero < a1 & P467 & P464 & P463 & P0) & P0 ->  (Zero < a1 & P481 & P479 & P478 & P0) & P0" 0;
pushnode 16 "( a1 < a2 & P471 & P469 & P466 & P465 & P463 & P0) & ( Zero < a1 & P467 & P464 & P463 & P0) & P0 -> ( (Zero < a1 & a1 < a2) & P479 & P478 & P0) & P0" 2;
pushnode 15 "(( Zero < a1 & a1 < a2 -> a1 * a1 < a2 * a1) &  P478 & P0) & (a1 * a2 <  a2 * a2 & P475 & P473 & P0) & ( a1 < a2 & P471 & P469 & P466 & P465 & P463 & P0) & ( Zero < a1 & P467 & P464 & P463 & P0) & P0 -> ( a1 * a1 < a2 * a2 & P472 & P469 &  P466 & P465 & P463 & P0) & P0" 2;
pushreference 14 "P0 -> (( Zero < a1 & a1 < a2 -> a1 * a1 < a2 * a1) &  P478 & P0) & P0" "MTIMES";
pushnode 11 "( a1 * a2 < a2 * a2 & P475 & P473 & P0) & ( a1 < a2 & P471 & P469 & P466 & P465 & P463 & P0) & ( Zero < a1 & P467 & P464 & P463 & P0) & P0 -> (a1 * a1 < a2 * a2 & P472 & P469 & P466 & P465 & P463 & P0) & P0" 2;
pushnode 13 " (a1 < a2 & P471 & P469 & P466 & P465 & P463 & P0) & P0 -> (a1 < a2 & P477 & P474 &  P473 & P0) & P0" 0;
pushnode 12 "( Zero < a2 & P468 & P464 & P463 & P0) & P0 ->  (Zero < a2 & P476 & P474 & P473 & P0) & P0" 0;
pushnode 10 "( a1 < a2 & P471 & P469 & P466 & P465 & P463 & P0) & ( Zero < a2 & P468 & P464 & P463 & P0) & P0 -> ( (Zero < a2 & a1 < a2) & P474 & P473 & P0) & P0" 2;
pushnode 9 "(( Zero < a2 & a1 < a2 -> a1 * a2 < a2 * a2) &  P473 & P0) &  (a1 < a2 &  P471 & P469 & P466 & P465 & P463 & P0) & (Zero < a1 & P467 & P464 & P463 & P0) &  (Zero < a2 & P468 & P464 & P463 & P0) & P0 -> ( a1 * a1 < a2 * a2 & P472 & P469 &  P466 & P465 & P463 & P0) & P0" 2;
pushreference 8 "P0 -> (( Zero < a2 & a1 < a2 -> a1 * a2 < a2 * a2) &  P473 & P0) & P0" "MTIMES";
pushnode 7 "  (a1 < a2 & P471 & P469 & P466 & P465 & P463 & P0) &  (Zero < a1 & P467 & P464 & P463 & P0) & (Zero < a2 & P468 & P464 & P463 & P0) & P0 ->  (a1 * a1 < a2 * a2 &  P472 & P469 & P466 & P465 & P463 & P0) & P0" 2;
THEOREMS:=("SquareOrder1",(termtosequent(parseprop("( a1 < a2 & P471 & P469 & P466 & P465 & P463 & P0) & ( Zero < a1 & P467 & P464 & P463 & P0) & ( Zero < a2 & P468 & P464 & P463 & P0) & P0 -> (a1 * a1 < a2 * a2 & P472 & P469 & P466 & P465 & P463 & P0) & P0")),hd(!PROOFSTACK)))::(!THEOREMS);
PROOFSTACK:=nil;
td "SquareOrder1";
pushnode 67 " (Zero < a1 & P467 & P464 & P463 & P0) & P0 -> ( Zero < a1 & P523 & P0) & P0" 0;
pushnode 66 " (Zero < a2 & P468 & P464 & P463 & P0) & P0 -> ( Zero < a2 & P522 & P0) & P0" 0;
pushnode 65 " (a2 < a1 & P520 & P494 & P492 & P0) & P0 -> ( a2 < a1 & P521 & P0) & P0" 0;
pushreference 64 "( a2 * a2 < a1 * a1 & P524 & P0) & ( a1 * a1 < a2 * a2 & P490 & P470 &  P466 & P465 & P463 & P0) & P0 -> P0" "NOTBOTH";
pushreference 63 "(a2 < a1 & P521 & P0) & (Zero < a2 & P522 & P0) & (Zero < a1 & P523 & P0) & P0 -> (a2 * a2 < a1 * a1 & P524 & P0) & P0" "SquareOrder1";
pushnode 62 "( a2 < a1 & P520 & P494 & P492 & P0) & ( a1 * a1 < a2 * a2 & P490 & P470 &  P466 & P465 & P463 & P0) & ( Zero < a1 & P467 & P464 & P463 & P0) & ( Zero < a2 & P468 & P464 & P463 & P0) & P0 -> P0" 5;
pushnode 61 " (a1 < a2 & P519 & P494 & P492 & P0) & P0 -> ( a1 < a2 & P491 & P470 & P466 & P465 & P463 & P0) & P0" 0;
pushnode 33 "( (a1 < a2 v a2 < a1) & P494 & P492 & P0) & ( a1 * a1 < a2 * a2 & P490 & P470 &  P466 & P465 & P463 & P0) & ( Zero < a1 & P467 & P464 & P463 & P0) & ( Zero < a2 & P468 & P464 & P463 & P0) & P0 -> ( a1 < a2 & P491 & P470 & P466 & P465 & P463 & P0) & P0" 2;
pushnode 60 "  ( a2 * a2 < a2 * a2 & P516 & P514 & P510 & P508 & P507 & P505 & P503 &  P501 & P499 & P497 & P490 & P470 & P466 & P465 & P463 & P496 & P498 & P500 &  P502 & P504 & P506 & P495 & P493 & P492 & P506 & P502 & P498 & P0) & ( a1 * a1 = [a1 + Zero] * a1 & P496 & P0) & ( [a1 + Zero] * a1 = a1 * [a1 + Zero] &  P500 & P0) & (a1 * [a1 + Zero] = [a1 + Zero] * [a1 + Zero] & P504 & P0) &  (a1 + Zero = a2 + Zero & P495 & P493 & P492 & P0) & P0 -> ( a2 * a2 < a2 * a2 & P518 & P517 & P0) & P0" 0;
pushnode 59 "( ~a2 * a2 < a2 * a2 & P517 & P0) & ( a2 * a2 < a2 * a2 & P516 & P514 &  P510 & P508 & P507 & P505 & P503 & P501 & P499 & P497 & P490 & P470 & P466 &  P465 & P463 & P496 & P498 & P500 & P502 & P504 & P506 & P495 & P493 & P492 &  P506 & P502 & P498 & P0) & ( a1 * a1 = [a1 + Zero] * a1 &  P496 & P0) & ([a1 + Zero] * a1 = a1 * [a1 + Zero] & P500 & P0) & (a1 * [a1 + Zero] = [a1 + Zero] * [a1 + Zero] & P504 & P0) &  (a1 + Zero = a2 + Zero & P495 & P493 & P492 & P0) & P0 -> P0" 1;
pushreference 58 "P0 -> (~a2 * a2 < a2 * a2 & P517 & P0) & P0" "IRR";
pushnode 57 " (a2 * a2 < a2 * a2 &  P516 & P514 & P510 & P508 & P507 & P505 & P503 & P501 & P499 & P497 & P490 &  P470 & P466 & P465 & P463 & P496 & P498 & P500 & P502 & P504 & P506 & P495 &  P493 & P492 & P506 & P502 & P498 & P0) & (a1 * a1 =  [a1 + Zero] * a1 & P496 & P0) & ( [a1 + Zero] * a1 = a1 * [a1 + Zero] &  P500 & P0) & (a1 * [a1 + Zero] = [a1 + Zero] * [a1 + Zero] & P504 & P0) &  (a1 + Zero = a2 + Zero & P495 & P493 & P492 & P0) & P0 -> P0" 2;
pushnode 56 "( a2 * a2 = [a2 + Zero] * a2 & P498 & P0) & ( [a2 + Zero] * a2 < [a2 + Zero] * a2 &  P514 & P510 & P508 & P507 & P505 & P503 & P501 & P499 & P497 & P490 & P470 &  P466 & P465 & P463 & P496 & P498 & P500 & P502 & P504 & P506 & P495 & P493 &  P492 & P506 & P502 & P0) & ( a1 * a1 = [a1 + Zero] * a1 &  P496 & P0) & ([a1 + Zero] * a1 = a1 * [a1 + Zero] & P500 & P0) & (a1 * [a1 + Zero] = [a1 + Zero] * [a1 + Zero] & P504 & P0) &  (a1 + Zero = a2 + Zero & P495 & P493 & P492 & P0) & P0 -> P0" 1;
pushnode 54 "([a2 + Zero] * a2 = a2 * [a2 + Zero] & P502 & P0) & (a2 * [a2 + Zero] < a2 * [a2 + Zero] &  P510 & P508 & P507 & P505 & P503 & P501 & P499 & P497 & P490 & P470 & P466 &  P465 & P463 & P496 & P498 & P500 & P502 & P504 & P506 & P495 & P493 & P492 &  P506 & P0) & (a1 * a1 = [ a1 + Zero] * a1 &  P496 & P0) & (a2 * a2 = [ a2 + Zero] * a2 &  P498 & P0) & ([a1 + Zero] * a1 = a1 * [a1 + Zero] & P500 & P0) & (a1 * [a1 + Zero] = [a1 + Zero] * [a1 + Zero] & P504 & P0) &  (a1 + Zero = a2 + Zero & P495 & P493 & P492 & P0) & P0 -> P0" 1;
pushnode 53 "( a2 * [a2 + Zero] =  [a2 + Zero] * [a2 + Zero] & P506 & P0) &  ( [a2 + Zero] * [a2 + Zero] <  [a2 + Zero] * [a2 + Zero] &  P508 & P507 & P505 & P503 & P501 & P499 & P497 & P490 & P470 & P466 & P465 &  P463 & P496 & P498 & P500 & P502 & P504 & P506 & P495 & P493 & P492 & P0) & ( a1 * a1 = [a1 + Zero] * a1 & P496 & P0) & (a2 * a2 = [a2 + Zero] * a2 &  P498 & P0) & ([a1 + Zero] * a1 = a1 * [a1 + Zero] & P500 & P0) & ( [a2 + Zero] * a2 = a2 * [a2 + Zero] &  P502 & P0) & (a1 * [a1 + Zero] = [a1 + Zero] * [a1 + Zero] & P504 & P0) &  (a1 + Zero = a2 + Zero & P495 & P493 & P492 & P0) & P0 -> P0" 1;
pushnode 52 "  (a1 + Zero = a2 + Zero &  P495 & P493 & P492 & P0) &  ([a1 + Zero] * [a1 + Zero] < [a2 + Zero] * [a2 + Zero] & P507 & P505 & P503 &  P501 & P499 & P497 & P490 & P470 & P466 & P465 & P463 & P496 & P498 & P500 &  P502 & P504 & P506 & P0) & (a1 * a1 =  [a1 + Zero] * a1 & P496 & P0) & (a2 * a2 =  [a2 + Zero] * a2 & P498 & P0) & ( [a1 + Zero] * a1 = a1 * [a1 + Zero] &  P500 & P0) & ([a2 + Zero] * a2 = a2 * [a2 + Zero] & P502 & P0) & (a1 * [a1 + Zero] = [a1 + Zero] * [a1 + Zero] & P504 & P0) & (a2 * [a2 + Zero] = [a2 + Zero] * [a2 + Zero] & P506 & P0) & P0 -> P0" 1;
pushnode 51 "(a2 * [a2 + Zero] = [a2 + Zero] * [a2 + Zero] & P506 & P0) & ( [a1 + Zero] * [a1 + Zero] < a2 * [a2 + Zero] & P505 & P503 & P501 &  P499 & P497 & P490 & P470 & P466 & P465 & P463 & P496 & P498 & P500 & P502 &  P504 & P0) & ( a1 + Zero = a2 + Zero &  P495 & P493 & P492 & P0) & ( a1 * a1 = [a1 + Zero] * a1 &  P496 & P0) & (a2 * a2 = [ a2 + Zero] * a2 &  P498 & P0) & ([a1 + Zero] * a1 = a1 * [a1 + Zero] & P500 & P0) & ( [a2 + Zero] * a2 = a2 * [a2 + Zero] &  P502 & P0) & (a1 * [a1 + Zero] = [a1 + Zero] * [a1 + Zero] & P504 & P0) & P0 -> P0" 1;
pushreference 50 "P0 -> ( a2 * [a2 + Zero] =  [a2 + Zero] * [a2 + Zero] & P506 & P0) & P0" "SubLemma";
pushnode 49 "( a1 * [a1 + Zero] = [a1 + Zero] * [ a1 + Zero] & P504 & P0) & ( [a1 + Zero] * [a1 + Zero] < a2 * [a2 + Zero] & P505 & P503 & P501 &  P499 & P497 & P490 & P470 & P466 & P465 & P463 & P496 & P498 & P500 & P502 &  P504 & P0) & ( a1 + Zero = a2 + Zero &  P495 & P493 & P492 & P0) & ( a1 * a1 = [a1 + Zero] * a1 &  P496 & P0) & (a2 * a2 = [ a2 + Zero] * a2 &  P498 & P0) & ([a1 + Zero] * a1 = a1 * [a1 + Zero] & P500 & P0) & ( [a2 + Zero] * a2 = a2 * [a2 + Zero] &  P502 & P0) & P0 -> P0" 2;
pushnode 48 "(a1 * [a1 + Zero] = [a1 + Zero] * [a1 + Zero] & P504 & P0) &  (a1 * [a1 + Zero] < a2 * [a2 + Zero] &  P503 & P501 & P499 & P497 & P490 & P470 & P466 & P465 & P463 & P496 & P498 &  P500 & P502 & P0) &  ( a1 + Zero = a2 + Zero & P495 & P493 & P492 & P0) & ( a1 * a1 = [a1 + Zero] * a1 & P496 & P0) & (a2 * a2 = [a2 + Zero] * a2 &  P498 & P0) & ([a1 + Zero] * a1 = a1 * [a1 + Zero] & P500 & P0) & ( [a2 + Zero] * a2 = a2 * [a2 + Zero] &  P502 & P0) & P0 -> P0" 1;
pushreference 47 "P0 -> (a1 * [ a1 + Zero] = [a1 + Zero] * [ a1 + Zero] & P504 & P0) & P0" "SubLemma";
pushnode 46 "([ a2 + Zero] * a2 = a2 * [a2 + Zero] & P502 & P0) &  (a1 * [a1 + Zero] < a2 * [a2 + Zero] &  P503 & P501 & P499 & P497 & P490 & P470 & P466 & P465 & P463 & P496 & P498 &  P500 & P502 & P0) &  ( a1 + Zero = a2 + Zero & P495 & P493 & P492 & P0) & ( a1 * a1 = [a1 + Zero] * a1 & P496 & P0) & (a2 * a2 = [a2 + Zero] * a2 &  P498 & P0) & ([a1 + Zero] * a1 = a1 * [a1 + Zero] & P500 & P0) & P0 -> P0" 2;
pushnode 45 "([a2 + Zero] * a2 = a2 * [a2 + Zero] & P502 & P0) & (a1 * [a1 + Zero] < [a2 + Zero] * a2 &  P501 & P499 & P497 & P490 & P470 & P466 & P465 & P463 & P496 & P498 & P500 & P0) &  (a1 + Zero =  a2 + Zero & P495 & P493 & P492 & P0) & ( a1 * a1 = [a1 + Zero] * a1 & P496 & P0) & (a2 * a2 = [a2 + Zero] * a2 &  P498 & P0) & ([a1 + Zero] * a1 = a1 * [a1 + Zero] & P500 & P0) & P0 -> P0" 1;
pushreference 44 "P0 -> ([a2 + Zero] * a2 = a2 * [a2 + Zero] & P502 & P0) & P0" "CTIMES";
pushnode 43 "( [a1 + Zero] * a1 = a1 * [ a1 + Zero] & P500 & P0) & ( a1 * [a1 + Zero] < [a2 + Zero] * a2 & P501 & P499 & P497 & P490 & P470 & P466 & P465 &  P463 & P496 & P498 & P500 & P0) & ( a1 + Zero = a2 + Zero &  P495 & P493 & P492 & P0) & ( a1 * a1 = [a1 + Zero] * a1 &  P496 & P0) & (a2 * a2 = [ a2 + Zero] * a2 &  P498 & P0) & P0 -> P0" 2;
pushnode 42 "([a1 + Zero] * a1 = a1 * [a1 + Zero] & P500 & P0) &  ( [a1 + Zero] * a1 < [a2 + Zero] * a2 &  P499 & P497 & P490 & P470 & P466 & P465 & P463 & P496 & P498 & P0) &  ( a1 + Zero = a2 + Zero & P495 & P493 & P492 & P0) & ( a1 * a1 = [a1 + Zero] * a1 & P496 & P0) & (a2 * a2 = [a2 + Zero] * a2 &  P498 & P0) & P0 -> P0" 1;
pushreference 41 "P0 -> ([a1 + Zero] * a1 = a1 * [a1 + Zero] & P500 & P0) & P0" "CTIMES";
pushnode 40 " ( a2 * a2 = [a2 + Zero] * a2 &  P498 & P0) & ([a1 + Zero] * a1 < [a2 + Zero] * a2 & P499 & P497 & P490 & P470 & P466 & P465 & P463 &  P496 & P498 & P0) & (a1 + Zero = a2 + Zero & P495 &  P493 & P492 & P0) & (a1 * a1 = [ a1 + Zero] * a1 &  P496 & P0) & P0 -> P0" 2;
pushnode 39 " (a2 * a2 =  [a2 + Zero] * a2 & P498 & P0) & ( [a1 + Zero] * a1 < a2 * a2 &  P497 & P490 & P470 & P466 & P465 & P463 & P496 & P0) & ( a1 + Zero = a2 + Zero &  P495 & P493 & P492 & P0) & ( a1 * a1 = [a1 + Zero] * a1 &  P496 & P0) & P0 -> P0" 1;
pushreference 38 "P0 -> (a2 * a2 =  [a2 + Zero] * a2 & P498 & P0) & P0" "SubLemma";
pushnode 37 "( a1 * a1 = [a1 + Zero] * a1 & P496 & P0) & ( [a1 + Zero] * a1 < a2 * a2 &  P497 & P490 & P470 & P466 & P465 & P463 & P496 & P0) & ( a1 + Zero = a2 + Zero &  P495 & P493 & P492 & P0) & P0 -> P0" 2;
pushnode 36 "(a1 * a1 = [a1 + Zero] * a1 &  P496 & P0) & (a1 * a1 <  a2 * a2 & P490 & P470 & P466 & P465 & P463 & P0) & ( a1 + Zero = a2 + Zero &  P495 & P493 & P492 & P0) & P0 -> P0" 1;
pushreference 35 "P0 -> (a1 * a1 = [a1 + Zero] * a1 &  P496 & P0) & P0" "SubLemma";
pushnode 34 "  ( a1 + Zero = a2 + Zero & P495 & P493 & P492 & P0) &  (a1 * a1 < a2 * a2 &  P490 & P470 & P466 & P465 & P463 & P0) & P0 -> P0" 2;
pushnode 32 " (a1 Equal a2 &  P493 & P492 & P0) & ( a1 * a1 < a2 * a2 & P490 & P470 & P466 & P465 & P463 & P0) & P0 -> P0" 1;
pushnode 31 "( (a1 Equal a2 v  a1 < a2 v a2 < a1) & P492 & P0) & ( a1 * a1 < a2 * a2 & P490 & P470 &  P466 & P465 & P463 & P0) & ( Zero < a1 & P467 & P464 & P463 & P0) & ( Zero < a2 & P468 & P464 & P463 & P0) & P0 -> ( a1 < a2 & P491 & P470 & P466 & P465 & P463 & P0) & P0" 2;
pushreference 30 "P0 -> ((a1 Equal a2 v a1 < a2 v a2 < a1) &  P492 & P0) & P0" "TRI";
pushnode 29 "( a1 * a1 < a2 * a2 & P490 & P470 & P466 & P465 & P463 & P0) & ( Zero < a1 & P467 & P464 & P463 & P0) & ( Zero < a2 & P468 & P464 & P463 & P0) & P0 ->  (a1 < a2 &  P491 & P470 & P466 & P465 & P463 & P0) & P0" 2;
pushnode 6 "( Zero < a1 & P467 & P464 & P463 & P0) & ( Zero < a2 & P468 & P464 & P463 & P0) & P0 -> (( a1 * a1 < a2 * a2 -> a1 < a2) &  P470 & P466 & P465 & P463 & P0) & P0" 1;
pushreference 7 "  (a1 < a2 & P471 & P469 & P466 & P465 & P463 & P0) &  (Zero < a1 & P467 & P464 & P463 & P0) & (Zero < a2 & P468 & P464 & P463 & P0) & P0 ->  (a1 * a1 < a2 * a2 &  P472 & P469 & P466 & P465 & P463 & P0) & P0" "SquareOrder1";
pushnode 5 "( Zero < a1 & P467 & P464 & P463 & P0) & ( Zero < a2 & P468 & P464 & P463 & P0) & P0 -> ((a1 < a2 -> a1 * a1 < a2 * a2) & P469 & P466 & P465 & P463 & P0) & P0" 1;
pushnode 4 " (Zero < a1 & P467 & P464 & P463 & P0) &  (Zero < a2 & P468 & P464 & P463 & P0) & P0 ->  ((( a1 < a2 -> a1 * a1 < a2 * a2) & ( a1 * a1 < a2 * a2 -> a1 < a2)) &  P466 & P465 & P463 & P0) & P0" 2;
pushnode 3 " (( Zero < a1 & Zero < a2) &  P464 & P463 & P0) & P0 ->  ((( a1 < a2 -> a1 * a1 < a2 * a2) & ( a1 * a1 < a2 * a2 -> a1 < a2)) &  P466 & P465 & P463 & P0) & P0" 1;
pushnode 2 " (( Zero < a1 & Zero < a2) &  P464 & P463 & P0) & P0 ->  (( a1 < a2 == a1 * a1 < a2 * a2) &  P465 & P463 & P0) & P0" 1;
pushnode 1 " P0 -> ( (Zero < a1 & Zero < a2 -> ( a1 < a2 == a1 * a1 < a2 * a2)) & P463 & P0) & P0" 1;
THEOREMS:=("SquareOrder",(termtosequent(parseprop(" P0 -> ( (Zero < a1 & Zero < a2 -> ( a1 < a2 == a1 * a1 < a2 * a2)) & P463 & P0) & P0")),hd(!PROOFSTACK)))::(!THEOREMS);
PROOFSTACK:=nil;
td "SquareOrder";
pushnode 5 "( Zero E a1 & P530 & P528 & P527 & P526 & P525 & P0) & P0 -> (Zero E a1 & P529 & P527 & P526 & P525 & P0) & P0" 0;
pushnode 4 "( (Zero E a1 & (Ax20.x20 E a1 -> x20 + One E a1)) & P528 & P527 & P526 & P525 & P0) & P0 -> ( Zero E a1 & P529 & P527 & P526 & P525 & P0) & P0" 1;
pushnode 3 "P0 -> (( Zero E a1 & (Ax20.x20 E a1 -> x20 + One E a1) -> Zero E a1) &  P527 & P526 & P525 & P0) & P0" 1;
pushnode 2 "P0 ->  ((Ax17. Zero E x17 & (Ax19.x19 E x17 -> x19 + One E x17) -> Zero E x17) &  P526 & P525 & P0) & P0" 1;
pushnode 1 " P0 ->  (Zero E Nat & P525 & P0) & P0" 1;
THEOREMS:=("ZeroNat",(termtosequent(parseprop(" P0 ->  (Zero E Nat & P525 & P0) & P0")),hd(!PROOFSTACK)))::(!THEOREMS);
PROOFSTACK:=nil;
td "ZeroNat";
pushnode 13 "( a1 + One E a2 & P549 & P546 & P545 & P540 &  P537 & P536 & P534 & P532 & P0) & P0 ->  (a1 + One E a2 & P541 & P537 &  P536 & P534 & P532 & P0) & P0" 0;
pushnode 12 "( a1 E a2 & P543 & P538 & P535 & P533 & P532 & P0) & P0 -> (a1 E a2 & P548 & P546 & P545 & P540 & P537 &  P536 & P534 & P532 & P0) & P0" 0;
pushnode 11 " ((a1 E a2 -> a1 + One E a2) & P546 &  P545 & P540 & P537 & P536 & P534 & P532 & P0) &  (a1 E a2 & P543 & P538 & P535 & P533 &  P532 & P0) & P0 -> ( a1 + One E a2 & P541 & P537 & P536 & P534 &  P532 & P0) & P0" 2;
pushnode 10 "((Ax20.x20 E a2 -> x20 + One E a2) &  P545 & P540 & P537 & P536 & P534 & P532 & P0) & ( a1 E a2 & P543 & P538 & P535 & P533 & P532 & P0) & P0 -> ( a1 + One E a2 & P541 & P537 & P536 & P534 & P532 & P0) & P0" 1;
pushnode 9 "( (Zero E a2 & (Ax20.x20 E a2 -> x20 + One E a2)) & P540 & P537 & P536 & P534 & P532 & P0) & ( a1 E a2 & P543 & P538 & P535 & P533 & P532 & P0) & P0 -> ( a1 + One E a2 & P541 & P537 & P536 & P534 & P532 & P0) & P0" 1;
pushnode 8 "( (Zero E a2 & (Ax20.x20 E a2 -> x20 + One E a2)) & P540 & P537 & P536 & P534 & P532 & P0) & P0 -> ( (Zero E a2 & (Ax20.x20 E a2 -> x20 + One E a2)) & P542 & P538 & P535 & P533 & P532 & P0) & P0" 0;
pushnode 7 "(( Zero E a2 & (Ax20.x20 E a2 -> x20 + One E a2) -> a1 E a2) &  P538 & P535 & P533 & P532 & P0) & (( Zero E a2 & (Ax20.x20 E a2 -> x20 + One E a2)) &  P540 & P537 & P536 & P534 & P532 & P0) & P0 -> ( a1 + One E a2 & P541 & P537 & P536 & P534 & P532 & P0) & P0" 2;
pushnode 6 "(( Zero E a2 & (Ax20.x20 E a2 -> x20 + One E a2) -> a1 E a2) &  P538 & P535 & P533 & P532 & P0) & P0 -> (( Zero E a2 & (Ax20.x20 E a2 -> x20 + One E a2) -> a1 + One E a2) &  P537 & P536 & P534 & P532 & P0) & P0" 1;
pushnode 5 " ((Ax17. Zero E x17 & (Ax19.x19 E x17 -> x19 + One E x17) -> a1 E x17) &  P535 & P533 & P532 & P0) & P0 -> (( Zero E a2 & (Ax20.x20 E a2 -> x20 + One E a2) ->  a1 + One E a2) &  P537 & P536 & P534 & P532 & P0) & P0" 1;
pushnode 4 " ((Ax17. Zero E x17 & (Ax19.x19 E x17 -> x19 + One E x17) -> a1 E x17) &  P535 & P533 & P532 & P0) & P0 ->  ((Ax17. Zero E x17 & (Ax19.x19 E x17 -> x19 + One E x17) ->  a1 + One E x17) &  P536 & P534 & P532 & P0) & P0" 1;
pushnode 3 "((Ax17. Zero E x17 & (Ax19.x19 E x17 -> x19 + One E x17) -> a1 E x17) & P535 & P533 & P532 & P0) & P0 -> ( a1 + One E Nat & P534 & P532 & P0) & P0" 1;
pushnode 2 "(a1 E Nat & P533 & P532 & P0) & P0 ->  (a1 + One E Nat & P534 & P532 & P0) & P0" 1;
THEOREMS:=("NatClosed",(termtosequent(parseprop(" (a1 E Nat & P533 & P532 & P0) & P0 -> ( a1 + One E Nat & P534 & P532 & P0) & P0")),hd(!PROOFSTACK)))::(!THEOREMS);
PROOFSTACK:=nil;
td "NatClosed";
pushnode 14 "(Real(a1) & P566 & P557 & P554 & P553 & P551 &  P550 & P0) & P0 -> ( Real(a1) & P552 & P550 & P0) & P0" 0;
pushnode 6 " (a1 E {x1|Real(x1)} & P557 & P554 & P553 &  P551 & P550 & P0) & P0 -> (Real(a1) & P552 & P550 & P0) & P0" 1;
pushreference 13 "P0 ->  (Real(a2 + One) & P565 &  P563 & P561 & P559 & P556 & P554 & P553 & P551 & P550 & P0) & P0" "RPLUS";
pushnode 12 "P0 -> (a2 + One E {x22|Real(x22)} & P563 & P561 &  P559 & P556 & P554 & P553 & P551 & P550 & P0) & P0" 1;
pushnode 11 "P0 -> ( a2 + One E {x22|Real(x22)} & P563 & P561 & P559 & P556 &  P554 & P553 & P551 & P550 & P0) & P0" 1;
pushnode 10 "P0 -> ( (a2 E {x21|Real(x21)} -> a2 + One E {x22|Real(x22)}) & P561 & P559 & P556 &  P554 & P553 & P551 & P550 & P0) & P0" 1;
pushnode 8 "P0 -> ( (Ax20.x20 E {x1|Real(x1)} -> x20 + One E {x1|Real(x1)}) & P559 & P556 & P554 &  P553 & P551 & P550 & P0) & P0" 1;
pushreference 9 "P0 ->  (Real(Zero) & P560 & P558 & P556 & P554 &  P553 & P551 & P550 & P0) & P0" "RZERO";
pushnode 7 " P0 -> (Zero E {x1|Real(x1)} & P558 & P556 & P554 & P553 & P551 &  P550 & P0) & P0" 1;
pushnode 5 "P0 -> ( (Zero E {x1|Real(x1)} & (Ax20. x20 E {x1|Real(x1)} -> x20 + One E {x1|Real(x1)})) & P556 & P554 & P553 &  P551 & P550 & P0) & P0" 2;
pushnode 4 "(( Zero E {x1|Real(x1)} & (Ax20. x20 E {x1|Real(x1)} -> x20 + One E {x1|Real(x1)}) -> a1 E {x1|Real(x1)}) &  P554 & P553 & P551 & P550 & P0) & P0 -> (Real(a1) & P552 & P550 & P0) & P0" 2;
pushnode 3 " ((Ax17. Zero E x17 & (Ax19.x19 E x17 -> x19 + One E x17) -> a1 E x17) &  P553 & P551 & P550 & P0) & P0 -> ( Real(a1) & P552 & P550 & P0) & P0" 1;
pushnode 2 "(a1 E Nat & P551 & P550 & P0) & P0 -> (Real(a1) & P552 & P550 & P0) & P0" 1;
THEOREMS:=("NatReal",(termtosequent(parseprop("(a1 E Nat & P551 & P550 & P0) & P0 -> (Real(a1) & P552 & P550 & P0) & P0")),hd(!PROOFSTACK)))::(!THEOREMS);
PROOFSTACK:=nil;
td "NatReal";
pushnode 11 "(a3 E a2 & P637 & P632 & P630 & P629 & P628 &  P627 & P626 & P625 & P0) & P0 -> (a3 E a2 & P634 & P633 & P630 & P629 & P628 &  P627 & P626 & P625 & P0) & P0" 0;
pushnode 10 "(a3 E a1 & P636 & P632 & P630 & P629 & P628 &  P627 & P626 & P625 & P0) & P0 -> (a3 E a1 & P635 & P633 & P630 & P629 & P628 &  P627 & P626 & P625 & P0) & P0" 0;
pushnode 9 "( (a3 E a1 v a3 E a2) & P632 & P630 & P629 & P628 & P627 & P626 &  P625 & P0) & P0 -> ( a3 E a2 & P634 & P633 & P630 & P629 & P628 & P627 & P626 & P625 & P0) & ( a3 E a1 & P635 & P633 & P630 & P629 & P628 & P627 & P626 & P625 & P0) & P0" 2;
pushnode 8 "( (a3 E a1 v a3 E a2) & P632 & P630 & P629 & P628 & P627 & P626 &  P625 & P0) & P0 -> (( a3 E a2 v a3 E a1) & P633 &  P630 & P629 & P628 & P627 & P626 & P625 & P0) & P0" 1;
pushnode 6 "P0 -> (( a3 E a1 v a3 E a2 -> a3 E a2 v a3 E a1) &  P630 & P629 & P628 & P627 & P626 & P625 & P0) & P0" 1;
THEOREMS:=("Symmetric",(termtosequent(parseprop("P0 -> (( a3 E a1 v a3 E a2 -> a3 E a2 v a3 E a1) &  P630 & P629 & P628 & P627 & P626 & P625 & P0) & P0")),hd(!PROOFSTACK)))::(!THEOREMS);
PROOFSTACK:=nil;
td "Symmetric";
pushnode 27 " (a3 = a1 & P756 & P745 & P743 & P742 & P741 &  P740 & P739 & P0) & P0 ->  (a3 = a1 & P772 & P771 & P770 & P768 &  P763 & P761 & P759 & P758 & P757 & P745 & P743 & P742 & P741 & P740 & P739 &  P760 & P758 & P757 & P745 & P743 & P742 & P741 & P740 & P739 & P0) & P0" 0;
pushnode 26 "( a3 = a1 & P756 & P745 & P743 & P742 & P741 & P740 & P739 & P0) & P0 ->  (( a3 = a1 v a3 = a2) & P771 &  P770 & P768 & P763 & P761 & P759 & P758 & P757 & P745 & P743 & P742 & P741 &  P740 & P739 & P760 & P758 & P757 & P745 & P743 & P742 & P741 & P740 & P739 & P0) & P0" 1;
pushnode 25 " (a3 = a1 & P756 & P745 &  P743 & P742 & P741 & P740 & P739 & P0) & P0 -> (a3 E {x4| x4 = a1 v x4 = a2} & P770 &  P768 & P763 & P761 & P759 & P758 & P757 & P745 & P743 & P742 & P741 & P740 &  P739 & P760 & P758 & P757 & P745 & P743 & P742 & P741 & P740 & P739 & P0) & P0" 1;
pushnode 24 " ( a4 = {x4|x4 = a1 v x4 = a2} & P768 & P763 & P761 & P759 &  P758 & P757 & P745 & P743 & P742 & P741 & P740 & P739 & P0) & (a3 = a1 & P756 & P745 & P743 & P742 & P741 & P740 &  P739 & P0) & P0 ->  (a3 E a4 &  P760 & P758 & P757 & P745 & P743 & P742 & P741 & P740 & P739 & P0) & P0" 1;
pushnode 20 "  (a4 = a1 Couple a2 & P763 & P761 & P759 & P758 & P757 &  P745 & P743 & P742 & P741 & P740 & P739 & P0) &  (a3 = a1 & P756 & P745 & P743 & P742 &  P741 & P740 & P739 & P0) & P0 ->  (a3 E a4 & P760 & P758 & P757 &  P745 & P743 & P742 & P741 & P740 & P739 & P0) & P0" 1;
pushnode 22 "( a3 = a1 & P756 & P745 & P743 & P742 & P741 & P740 & P739 & P0) & P0 -> ( a3 = a1 & P766 & P765 & P762 & P761 & P759 & P758 & P757 & P745 & P743 &  P742 & P741 & P740 & P739 & P760 & P758 & P757 & P745 & P743 & P742 & P741 &  P740 & P739 & P0) & P0" 0;
pushnode 21 " (a3 = a1 & P756 & P745 & P743 & P742 &  P741 & P740 & P739 & P0) & P0 -> ( a3 E Sing(a1) & P765 & P762 & P761 & P759 & P758 & P757 & P745 & P743 &  P742 & P741 & P740 & P739 & P760 & P758 & P757 & P745 & P743 & P742 & P741 &  P740 & P739 & P0) & P0" 1;
pushnode 19 "  (a4 = Sing(a1) & P762 & P761 & P759 & P758 &  P757 & P745 & P743 & P742 & P741 & P740 & P739 & P0) &  (a3 = a1 & P756 & P745 & P743 & P742 &  P741 & P740 & P739 & P0) & P0 ->  (a3 E a4 & P760 & P758 & P757 &  P745 & P743 & P742 & P741 & P740 & P739 & P0) & P0" 1;
pushnode 18 " ( ( a4 = Sing(a1) v a4 = a1 Couple a2) & P761 & P759 &  P758 & P757 & P745 & P743 & P742 & P741 & P740 & P739 & P0) &  (a3 = a1 & P756 & P745 &  P743 & P742 & P741 & P740 & P739 & P0) & P0 ->  (a3 E a4 & P760 & P758 & P757 &  P745 & P743 & P742 & P741 & P740 & P739 & P0) & P0" 2;
pushnode 17 "  (a4 E  a1 Kpair a2 & P759 & P758 & P757 & P745 &  P743 & P742 & P741 & P740 & P739 & P0) &  (a3 = a1 & P756 & P745 & P743 & P742 &  P741 & P740 & P739 & P0) & P0 ->  (a3 E a4 & P760 & P758 & P757 &  P745 & P743 & P742 & P741 & P740 & P739 & P0) & P0" 1;
pushnode 16 "( a3 = a1 & P756 & P745 & P743 & P742 & P741 & P740 & P739 & P0) & P0 -> ((a4 E  a1 Kpair a2 -> a3 E a4) &  P758 & P757 & P745 & P743 & P742 & P741 & P740 & P739 & P0) & P0" 1;
pushnode 15 " (a3 = a1 & P756 & P745 & P743 & P742 & P741 &  P740 & P739 & P0) & P0 ->  ((Ax9. x9 E a1 Kpair a2 -> a3 E x9) &  P757 & P745 & P743 & P742 & P741 & P740 & P739 & P0) & P0" 1;
pushnode 7 " P0 ->  ( (a3 = a1 -> (Ax9.x9 E a1 Kpair a2 -> a3 E x9)) & P745 & P743 & P742 & P741 & P740 & P739 & P0) & P0" 1;
pushnode 14 "( a3 = a1 & P755 & P751 & P748 & P746 & P744 & P743 & P742 & P741 & P740 &  P739 & P0) & P0 -> ( a3 = a1 & P747 & P744 & P743 & P742 & P741 & P740 & P739 & P0) & P0" 0;
pushnode 11 "( a3 E Sing(a1) & P751 & P748 & P746 & P744 & P743 & P742 & P741 & P740 &  P739 & P0) & P0 -> ( a3 = a1 & P747 & P744 & P743 & P742 & P741 & P740 & P739 & P0) & P0" 1;
pushnode 13 " P0 ->  (Sing(a1) = Sing(a1) & P753 & P752 & P750 & P748 & P746 & P744 &  P743 & P742 & P741 & P740 & P739 & P0) & P0" 0;
pushnode 12 " P0 -> ( (Sing(a1) = Sing(a1) v Sing(a1) = a1 Couple a2) & P752 & P750 & P748 & P746 &  P744 & P743 & P742 & P741 & P740 & P739 & P0) & P0" 1;
pushnode 10 "P0 -> ( Sing(a1) E a1 Kpair a2 & P750 & P748 & P746 & P744 & P743 &  P742 & P741 & P740 & P739 & P0) & P0" 1;
pushnode 9 "(( Sing(a1) E a1 Kpair a2 -> a3 E Sing(a1)) &  P748 & P746 & P744 & P743 & P742 & P741 & P740 & P739 & P0) & P0 -> (a3 = a1 & P747 & P744 & P743 & P742 & P741 &  P740 & P739 & P0) & P0" 2;
pushnode 8 " ((Ax9. x9 E a1 Kpair a2 -> a3 E x9) &  P746 & P744 & P743 & P742 & P741 & P740 & P739 & P0) & P0 -> ( a3 = a1 & P747 & P744 & P743 & P742 & P741 & P740 & P739 & P0) & P0" 1;
pushnode 6 " P0 -> (( (Ax9.x9 E a1 Kpair a2 -> a3 E x9) -> a3 = a1) &  P744 & P743 & P742 & P741 & P740 & P739 & P0) & P0" 1;
pushnode 5 "P0 -> (( ((Ax9.x9 E a1 Kpair a2 -> a3 E x9) -> a3 = a1) & (a3 = a1 -> (Ax9. x9 E a1 Kpair a2 -> a3 E x9))) &  P743 & P742 & P741 & P740 & P739 & P0) & P0" 2;
pushnode 4 "P0 -> ( ((Ax9.x9 E a1 Kpair a2 -> a3 E x9) == a3 = a1) & P742 & P741 & P740 & P739 & P0) & P0" 1;
pushnode 3 " P0 -> ( (Ax4. (Ax8.x8 E a1 Kpair a2 -> x4 E x8) == x4 = a1) &  P741 & P740 & P739 & P0) & P0" 1;
pushnode 2 "P0 ->  ({x4|(Ax8.x8 E a1 Kpair a2 -> x4 E x8)} = {x3|x3 = a1} &  P740 & P739 & P0) & P0" 1;
pushnode 1 " P0 ->  (Si(a1 Kpair a2) = Sing(a1) & P739 & P0) & P0" 1;
THEOREMS:=("PROJ1",(termtosequent(parseprop("P0 -> ( Si(a1 Kpair a2) = Sing(a1) & P739 & P0) & P0")),hd(!PROOFSTACK)))::(!THEOREMS);
PROOFSTACK:=nil;
td "PROJ1";
pushnode 136 " P0 ->  ( a1 Couple a2 = a1 Couple a2 & P954 & P932 & P930 & P896 &  P894 & P892 & P889 & P888 & P887 & P876 & P874 & P871 & P780 & P778 & P777 &  P776 & P775 & P774 & P872 & P780 & P778 & P777 & P776 & P775 & P774 & P929 &  P899 & P897 & P895 & P894 & P892 & P889 & P888 & P887 & P876 & P874 & P871 &  P780 & P778 & P777 & P776 & P775 & P774 & P872 & P780 & P778 & P777 & P776 &  P775 & P774 & P890 & P888 & P887 & P876 & P874 & P871 & P780 & P778 & P777 &  P776 & P775 & P774 & P872 & P780 & P778 & P777 & P776 & P775 & P774 & P0) & P0" 0;
pushnode 120 " (a6 = a1 Couple a2 & P932 & P930 & P896 & P894 & P892 &  P889 & P888 & P887 & P876 & P874 & P871 & P780 & P778 & P777 & P776 & P775 &  P774 & P872 & P780 & P778 & P777 & P776 & P775 & P774 & P0) & P0 -> (a1 Couple a2 = a6 & P929 & P899 & P897 &  P895 & P894 & P892 & P889 & P888 & P887 & P876 & P874 & P871 & P780 & P778 &  P777 & P776 & P775 & P774 & P872 & P780 & P778 & P777 & P776 & P775 & P774 &  P890 & P888 & P887 & P876 & P874 & P871 & P780 & P778 & P777 & P776 & P775 &  P774 & P872 & P780 & P778 & P777 & P776 & P775 & P774 & P0) & P0" 1;
pushnode 135 " (a8 = a1 & P949 & P944 & P942 & P941 & P934 &  P933 & P893 & P892 & P889 & P888 & P887 & P876 & P874 & P871 & P780 & P778 &  P777 & P776 & P775 & P774 & P872 & P780 & P778 & P777 & P776 & P775 & P774 &  P931 & P930 & P896 & P894 & P892 & P889 & P888 & P887 & P876 & P874 & P871 &  P780 & P778 & P777 & P776 & P775 & P774 & P872 & P780 & P778 & P777 & P776 &  P775 & P774 & P939 & P938 & P937 & P936 & P931 & P930 & P896 & P894 & P892 &  P889 & P888 & P887 & P876 & P874 & P871 & P780 & P778 & P777 & P776 & P775 &  P774 & P872 & P780 & P778 & P777 & P776 & P775 & P774 & P929 & P899 & P897 &  P895 & P894 & P892 & P889 & P888 & P887 & P876 & P874 & P871 & P780 & P778 &  P777 & P776 & P775 & P774 & P872 & P780 & P778 & P777 & P776 & P775 & P774 &  P890 & P888 & P887 & P876 & P874 & P871 & P780 & P778 & P777 & P776 & P775 &  P774 & P872 & P780 & P778 & P777 & P776 & P775 & P774 & P0) & P0 -> ( a8 = a1 & P951 & P950 & P944 & P942 & P941 & P934 & P933 & P893 & P892 &  P889 & P888 & P887 & P876 & P874 & P871 & P780 & P778 & P777 & P776 & P775 &  P774 & P872 & P780 & P778 & P777 & P776 & P775 & P774 & P931 & P930 & P896 &  P894 & P892 & P889 & P888 & P887 & P876 & P874 & P871 & P780 & P778 & P777 &  P776 & P775 & P774 & P872 & P780 & P778 & P777 & P776 & P775 & P774 & P939 &  P938 & P937 & P936 & P931 & P930 & P896 & P894 & P892 & P889 & P888 & P887 &  P876 & P874 & P871 & P780 & P778 & P777 & P776 & P775 & P774 & P872 & P780 &  P778 & P777 & P776 & P775 & P774 & P929 & P899 & P897 & P895 & P894 & P892 &  P889 & P888 & P887 & P876 & P874 & P871 & P780 & P778 & P777 & P776 & P775 &  P774 & P872 & P780 & P778 & P777 & P776 & P775 & P774 & P890 & P888 & P887 &  P876 & P874 & P871 & P780 & P778 & P777 & P776 & P775 & P774 & P872 & P780 &  P778 & P777 & P776 & P775 & P774 & P0) & P0" 0;
pushnode 134 " (a8 = a1 & P949 & P944 & P942 & P941 & P934 &  P933 & P893 & P892 & P889 & P888 & P887 & P876 & P874 & P871 & P780 & P778 &  P777 & P776 & P775 & P774 & P872 & P780 & P778 & P777 & P776 & P775 & P774 &  P931 & P930 & P896 & P894 & P892 & P889 & P888 & P887 & P876 & P874 & P871 &  P780 & P778 & P777 & P776 & P775 & P774 & P872 & P780 & P778 & P777 & P776 &  P775 & P774 & P939 & P938 & P937 & P936 & P931 & P930 & P896 & P894 & P892 &  P889 & P888 & P887 & P876 & P874 & P871 & P780 & P778 & P777 & P776 & P775 &  P774 & P872 & P780 & P778 & P777 & P776 & P775 & P774 & P929 & P899 & P897 &  P895 & P894 & P892 & P889 & P888 & P887 & P876 & P874 & P871 & P780 & P778 &  P777 & P776 & P775 & P774 & P872 & P780 & P778 & P777 & P776 & P775 & P774 &  P890 & P888 & P887 & P876 & P874 & P871 & P780 & P778 & P777 & P776 & P775 &  P774 & P872 & P780 & P778 & P777 & P776 & P775 & P774 & P0) & P0 -> (( a8 = a1 v a8 = a1) & P950 &  P944 & P942 & P941 & P934 & P933 & P893 & P892 & P889 & P888 & P887 & P876 &  P874 & P871 & P780 & P778 & P777 & P776 & P775 & P774 & P872 & P780 & P778 &  P777 & P776 & P775 & P774 & P931 & P930 & P896 & P894 & P892 & P889 & P888 &  P887 & P876 & P874 & P871 & P780 & P778 & P777 & P776 & P775 & P774 & P872 &  P780 & P778 & P777 & P776 & P775 & P774 & P939 & P938 & P937 & P936 & P931 &  P930 & P896 & P894 & P892 & P889 & P888 & P887 & P876 & P874 & P871 & P780 &  P778 & P777 & P776 & P775 & P774 & P872 & P780 & P778 & P777 & P776 & P775 &  P774 & P929 & P899 & P897 & P895 & P894 & P892 & P889 & P888 & P887 & P876 &  P874 & P871 & P780 & P778 & P777 & P776 & P775 & P774 & P872 & P780 & P778 &  P777 & P776 & P775 & P774 & P890 & P888 & P887 & P876 & P874 & P871 & P780 &  P778 & P777 & P776 & P775 & P774 & P872 & P780 & P778 & P777 & P776 & P775 &  P774 & P0) & P0" 1;
pushnode 130 " P0 ->  ((a8 = a1 -> a8 = a1 v a8 = a1) &  P944 & P942 & P941 & P934 & P933 & P893 & P892 & P889 & P888 & P887 & P876 &  P874 & P871 & P780 & P778 & P777 & P776 & P775 & P774 & P872 & P780 & P778 &  P777 & P776 & P775 & P774 & P931 & P930 & P896 & P894 & P892 & P889 & P888 &  P887 & P876 & P874 & P871 & P780 & P778 & P777 & P776 & P775 & P774 & P872 &  P780 & P778 & P777 & P776 & P775 & P774 & P939 & P938 & P937 & P936 & P931 &  P930 & P896 & P894 & P892 & P889 & P888 & P887 & P876 & P874 & P871 & P780 &  P778 & P777 & P776 & P775 & P774 & P872 & P780 & P778 & P777 & P776 & P775 &  P774 & P929 & P899 & P897 & P895 & P894 & P892 & P889 & P888 & P887 & P876 &  P874 & P871 & P780 & P778 & P777 & P776 & P775 & P774 & P872 & P780 & P778 &  P777 & P776 & P775 & P774 & P890 & P888 & P887 & P876 & P874 & P871 & P780 &  P778 & P777 & P776 & P775 & P774 & P872 & P780 & P778 & P777 & P776 & P775 &  P774 & P0) & P0" 1;
pushnode 133 "(a8 = a1 &  P948 & P945 & P943 & P942 & P941 & P934 & P933 & P893 & P892 & P889 & P888 &  P887 & P876 & P874 & P871 & P780 & P778 & P777 & P776 & P775 & P774 & P872 &  P780 & P778 & P777 & P776 & P775 & P774 & P931 & P930 & P896 & P894 & P892 &  P889 & P888 & P887 & P876 & P874 & P871 & P780 & P778 & P777 & P776 & P775 &  P774 & P872 & P780 & P778 & P777 & P776 & P775 & P774 & P939 & P938 & P937 &  P936 & P931 & P930 & P896 & P894 & P892 & P889 & P888 & P887 & P876 & P874 &  P871 & P780 & P778 & P777 & P776 & P775 & P774 & P872 & P780 & P778 & P777 &  P776 & P775 & P774 & P929 & P899 & P897 & P895 & P894 & P892 & P889 & P888 &  P887 & P876 & P874 & P871 & P780 & P778 & P777 & P776 & P775 & P774 & P872 &  P780 & P778 & P777 & P776 & P775 & P774 & P890 & P888 & P887 & P876 & P874 &  P871 & P780 & P778 & P777 & P776 & P775 & P774 & P872 & P780 & P778 & P777 &  P776 & P775 & P774 & P0) & P0 ->  (a8 = a1 & P946 & P943 & P942 & P941 & P934 &  P933 & P893 & P892 & P889 & P888 & P887 & P876 & P874 & P871 & P780 & P778 &  P777 & P776 & P775 & P774 & P872 & P780 & P778 & P777 & P776 & P775 & P774 &  P931 & P930 & P896 & P894 & P892 & P889 & P888 & P887 & P876 & P874 & P871 &  P780 & P778 & P777 & P776 & P775 & P774 & P872 & P780 & P778 & P777 & P776 &  P775 & P774 & P939 & P938 & P937 & P936 & P931 & P930 & P896 & P894 & P892 &  P889 & P888 & P887 & P876 & P874 & P871 & P780 & P778 & P777 & P776 & P775 &  P774 & P872 & P780 & P778 & P777 & P776 & P775 & P774 & P929 & P899 & P897 &  P895 & P894 & P892 & P889 & P888 & P887 & P876 & P874 & P871 & P780 & P778 &  P777 & P776 & P775 & P774 & P872 & P780 & P778 & P777 & P776 & P775 & P774 &  P890 & P888 & P887 & P876 & P874 & P871 & P780 & P778 & P777 & P776 & P775 &  P774 & P872 & P780 & P778 & P777 & P776 & P775 & P774 & P0) & P0" 0;
pushnode 132 "( a8 = a1 & P947 & P945 & P943 & P942 & P941 & P934 & P933 & P893 & P892 &  P889 & P888 & P887 & P876 & P874 & P871 & P780 & P778 & P777 & P776 & P775 &  P774 & P872 & P780 & P778 & P777 & P776 & P775 & P774 & P931 & P930 & P896 &  P894 & P892 & P889 & P888 & P887 & P876 & P874 & P871 & P780 & P778 & P777 &  P776 & P775 & P774 & P872 & P780 & P778 & P777 & P776 & P775 & P774 & P939 &  P938 & P937 & P936 & P931 & P930 & P896 & P894 & P892 & P889 & P888 & P887 &  P876 & P874 & P871 & P780 & P778 & P777 & P776 & P775 & P774 & P872 & P780 &  P778 & P777 & P776 & P775 & P774 & P929 & P899 & P897 & P895 & P894 & P892 &  P889 & P888 & P887 & P876 & P874 & P871 & P780 & P778 & P777 & P776 & P775 &  P774 & P872 & P780 & P778 & P777 & P776 & P775 & P774 & P890 & P888 & P887 &  P876 & P874 & P871 & P780 & P778 & P777 & P776 & P775 & P774 & P872 & P780 &  P778 & P777 & P776 & P775 & P774 & P0) & P0 ->  (a8 = a1 & P946 & P943 & P942 & P941 & P934 &  P933 & P893 & P892 & P889 & P888 & P887 & P876 & P874 & P871 & P780 & P778 &  P777 & P776 & P775 & P774 & P872 & P780 & P778 & P777 & P776 & P775 & P774 &  P931 & P930 & P896 & P894 & P892 & P889 & P888 & P887 & P876 & P874 & P871 &  P780 & P778 & P777 & P776 & P775 & P774 & P872 & P780 & P778 & P777 & P776 &  P775 & P774 & P939 & P938 & P937 & P936 & P931 & P930 & P896 & P894 & P892 &  P889 & P888 & P887 & P876 & P874 & P871 & P780 & P778 & P777 & P776 & P775 &  P774 & P872 & P780 & P778 & P777 & P776 & P775 & P774 & P929 & P899 & P897 &  P895 & P894 & P892 & P889 & P888 & P887 & P876 & P874 & P871 & P780 & P778 &  P777 & P776 & P775 & P774 & P872 & P780 & P778 & P777 & P776 & P775 & P774 &  P890 & P888 & P887 & P876 & P874 & P871 & P780 & P778 & P777 & P776 & P775 &  P774 & P872 & P780 & P778 & P777 & P776 & P775 & P774 & P0) & P0" 0;
pushnode 131 "(( a8 = a1 v a8 = a1) & P945 &  P943 & P942 & P941 & P934 & P933 & P893 & P892 & P889 & P888 & P887 & P876 &  P874 & P871 & P780 & P778 & P777 & P776 & P775 & P774 & P872 & P780 & P778 &  P777 & P776 & P775 & P774 & P931 & P930 & P896 & P894 & P892 & P889 & P888 &  P887 & P876 & P874 & P871 & P780 & P778 & P777 & P776 & P775 & P774 & P872 &  P780 & P778 & P777 & P776 & P775 & P774 & P939 & P938 & P937 & P936 & P931 &  P930 & P896 & P894 & P892 & P889 & P888 & P887 & P876 & P874 & P871 & P780 &  P778 & P777 & P776 & P775 & P774 & P872 & P780 & P778 & P777 & P776 & P775 &  P774 & P929 & P899 & P897 & P895 & P894 & P892 & P889 & P888 & P887 & P876 &  P874 & P871 & P780 & P778 & P777 & P776 & P775 & P774 & P872 & P780 & P778 &  P777 & P776 & P775 & P774 & P890 & P888 & P887 & P876 & P874 & P871 & P780 &  P778 & P777 & P776 & P775 & P774 & P872 & P780 & P778 & P777 & P776 & P775 &  P774 & P0) & P0 -> ( a8 = a1 & P946 & P943 & P942 & P941 & P934 & P933 & P893 & P892 & P889 &  P888 & P887 & P876 & P874 & P871 & P780 & P778 & P777 & P776 & P775 & P774 &  P872 & P780 & P778 & P777 & P776 & P775 & P774 & P931 & P930 & P896 & P894 &  P892 & P889 & P888 & P887 & P876 & P874 & P871 & P780 & P778 & P777 & P776 &  P775 & P774 & P872 & P780 & P778 & P777 & P776 & P775 & P774 & P939 & P938 &  P937 & P936 & P931 & P930 & P896 & P894 & P892 & P889 & P888 & P887 & P876 &  P874 & P871 & P780 & P778 & P777 & P776 & P775 & P774 & P872 & P780 & P778 &  P777 & P776 & P775 & P774 & P929 & P899 & P897 & P895 & P894 & P892 & P889 &  P888 & P887 & P876 & P874 & P871 & P780 & P778 & P777 & P776 & P775 & P774 &  P872 & P780 & P778 & P777 & P776 & P775 & P774 & P890 & P888 & P887 & P876 &  P874 & P871 & P780 & P778 & P777 & P776 & P775 & P774 & P872 & P780 & P778 &  P777 & P776 & P775 & P774 & P0) & P0" 2;
pushnode 129 "P0 ->  (( a8 = a1 v a8 = a1 -> a8 = a1) &  P943 & P942 & P941 & P934 & P933 & P893 & P892 & P889 & P888 & P887 & P876 &  P874 & P871 & P780 & P778 & P777 & P776 & P775 & P774 & P872 & P780 & P778 &  P777 & P776 & P775 & P774 & P931 & P930 & P896 & P894 & P892 & P889 & P888 &  P887 & P876 & P874 & P871 & P780 & P778 & P777 & P776 & P775 & P774 & P872 &  P780 & P778 & P777 & P776 & P775 & P774 & P939 & P938 & P937 & P936 & P931 &  P930 & P896 & P894 & P892 & P889 & P888 & P887 & P876 & P874 & P871 & P780 &  P778 & P777 & P776 & P775 & P774 & P872 & P780 & P778 & P777 & P776 & P775 &  P774 & P929 & P899 & P897 & P895 & P894 & P892 & P889 & P888 & P887 & P876 &  P874 & P871 & P780 & P778 & P777 & P776 & P775 & P774 & P872 & P780 & P778 &  P777 & P776 & P775 & P774 & P890 & P888 & P887 & P876 & P874 & P871 & P780 &  P778 & P777 & P776 & P775 & P774 & P872 & P780 & P778 & P777 & P776 & P775 &  P774 & P0) & P0" 1;
pushnode 128 "P0 -> (((a8 = a1 v a8 = a1 -> a8 = a1) & ( a8 = a1 -> a8 = a1 v a8 = a1)) &  P942 & P941 & P934 & P933 & P893 & P892 & P889 & P888 & P887 & P876 & P874 &  P871 & P780 & P778 & P777 & P776 & P775 & P774 & P872 & P780 & P778 & P777 &  P776 & P775 & P774 & P931 & P930 & P896 & P894 & P892 & P889 & P888 & P887 &  P876 & P874 & P871 & P780 & P778 & P777 & P776 & P775 & P774 & P872 & P780 &  P778 & P777 & P776 & P775 & P774 & P939 & P938 & P937 & P936 & P931 & P930 &  P896 & P894 & P892 & P889 & P888 & P887 & P876 & P874 & P871 & P780 & P778 &  P777 & P776 & P775 & P774 & P872 & P780 & P778 & P777 & P776 & P775 & P774 &  P929 & P899 & P897 & P895 & P894 & P892 & P889 & P888 & P887 & P876 & P874 &  P871 & P780 & P778 & P777 & P776 & P775 & P774 & P872 & P780 & P778 & P777 &  P776 & P775 & P774 & P890 & P888 & P887 & P876 & P874 & P871 & P780 & P778 &  P777 & P776 & P775 & P774 & P872 & P780 & P778 & P777 & P776 & P775 & P774 & P0) & P0" 2;
pushnode 127 "P0 ->  (( a8 = a1 v a8 = a1 == a8 = a1) &  P941 & P934 & P933 & P893 & P892 & P889 & P888 & P887 & P876 & P874 & P871 &  P780 & P778 & P777 & P776 & P775 & P774 & P872 & P780 & P778 & P777 & P776 &  P775 & P774 & P931 & P930 & P896 & P894 & P892 & P889 & P888 & P887 & P876 &  P874 & P871 & P780 & P778 & P777 & P776 & P775 & P774 & P872 & P780 & P778 &  P777 & P776 & P775 & P774 & P939 & P938 & P937 & P936 & P931 & P930 & P896 &  P894 & P892 & P889 & P888 & P887 & P876 & P874 & P871 & P780 & P778 & P777 &  P776 & P775 & P774 & P872 & P780 & P778 & P777 & P776 & P775 & P774 & P929 &  P899 & P897 & P895 & P894 & P892 & P889 & P888 & P887 & P876 & P874 & P871 &  P780 & P778 & P777 & P776 & P775 & P774 & P872 & P780 & P778 & P777 & P776 &  P775 & P774 & P890 & P888 & P887 & P876 & P874 & P871 & P780 & P778 & P777 &  P776 & P775 & P774 & P872 & P780 & P778 & P777 & P776 & P775 & P774 & P0) & P0" 1;
pushnode 126 "( a2 = a1 & P934 & P933 & P893 & P892 & P889 & P888 & P887 & P876 & P874 &  P871 & P780 & P778 & P777 & P776 & P775 & P774 & P872 & P780 & P778 & P777 &  P776 & P775 & P774 & P931 & P930 & P896 & P894 & P892 & P889 & P888 & P887 &  P876 & P874 & P871 & P780 & P778 & P777 & P776 & P775 & P774 & P872 & P780 &  P778 & P777 & P776 & P775 & P774 & P0) & P0 -> (( a8 = a1 v a8 = a2 == a8 = a1) &  P939 & P938 & P937 & P936 & P931 & P930 & P896 & P894 & P892 & P889 & P888 &  P887 & P876 & P874 & P871 & P780 & P778 & P777 & P776 & P775 & P774 & P872 &  P780 & P778 & P777 & P776 & P775 & P774 & P929 & P899 & P897 & P895 & P894 &  P892 & P889 & P888 & P887 & P876 & P874 & P871 & P780 & P778 & P777 & P776 &  P775 & P774 & P872 & P780 & P778 & P777 & P776 & P775 & P774 & P890 & P888 &  P887 & P876 & P874 & P871 & P780 & P778 & P777 & P776 & P775 & P774 & P872 &  P780 & P778 & P777 & P776 & P775 & P774 & P0) & P0" 1;
pushnode 125 "(a2 = a1 & P934 & P933 & P893 & P892 & P889 &  P888 & P887 & P876 & P874 & P871 & P780 & P778 & P777 & P776 & P775 & P774 &  P872 & P780 & P778 & P777 & P776 & P775 & P774 & P931 & P930 & P896 & P894 &  P892 & P889 & P888 & P887 & P876 & P874 & P871 & P780 & P778 & P777 & P776 &  P775 & P774 & P872 & P780 & P778 & P777 & P776 & P775 & P774 & P0) & P0 ->  ((Ax4. x4 = a1 v x4 = a2 == x4 = a1) &  P938 & P937 & P936 & P931 & P930 & P896 & P894 & P892 & P889 & P888 & P887 &  P876 & P874 & P871 & P780 & P778 & P777 & P776 & P775 & P774 & P872 & P780 &  P778 & P777 & P776 & P775 & P774 & P929 & P899 & P897 & P895 & P894 & P892 &  P889 & P888 & P887 & P876 & P874 & P871 & P780 & P778 & P777 & P776 & P775 &  P774 & P872 & P780 & P778 & P777 & P776 & P775 & P774 & P890 & P888 & P887 &  P876 & P874 & P871 & P780 & P778 & P777 & P776 & P775 & P774 & P872 & P780 &  P778 & P777 & P776 & P775 & P774 & P0) & P0" 1;
pushnode 124 "( a2 = a1 & P934 & P933 & P893 & P892 & P889 & P888 & P887 & P876 & P874 &  P871 & P780 & P778 & P777 & P776 & P775 & P774 & P872 & P780 & P778 & P777 &  P776 & P775 & P774 & P931 & P930 & P896 & P894 & P892 & P889 & P888 & P887 &  P876 & P874 & P871 & P780 & P778 & P777 & P776 & P775 & P774 & P872 & P780 &  P778 & P777 & P776 & P775 & P774 & P0) & P0 -> ( {x4|x4 = a1 v x4 = a2} = {x3|x3 = a1} & P937 & P936 &  P931 & P930 & P896 & P894 & P892 & P889 & P888 & P887 & P876 & P874 & P871 &  P780 & P778 & P777 & P776 & P775 & P774 & P872 & P780 & P778 & P777 & P776 &  P775 & P774 & P929 & P899 & P897 & P895 & P894 & P892 & P889 & P888 & P887 &  P876 & P874 & P871 & P780 & P778 & P777 & P776 & P775 & P774 & P872 & P780 &  P778 & P777 & P776 & P775 & P774 & P890 & P888 & P887 & P876 & P874 & P871 &  P780 & P778 & P777 & P776 & P775 & P774 & P872 & P780 & P778 & P777 & P776 &  P775 & P774 & P0) & P0" 1;
pushnode 123 "(a2 = a1 & P934 & P933 & P893 & P892 & P889 &  P888 & P887 & P876 & P874 & P871 & P780 & P778 & P777 & P776 & P775 & P774 &  P872 & P780 & P778 & P777 & P776 & P775 & P774 & P931 & P930 & P896 & P894 &  P892 & P889 & P888 & P887 & P876 & P874 & P871 & P780 & P778 & P777 & P776 &  P775 & P774 & P872 & P780 & P778 & P777 & P776 & P775 & P774 & P0) & P0 ->  ( a1 Couple a2 = Sing(a1) & P936 & P931 & P930 & P896 & P894 &  P892 & P889 & P888 & P887 & P876 & P874 & P871 & P780 & P778 & P777 & P776 &  P775 & P774 & P872 & P780 & P778 & P777 & P776 & P775 & P774 & P929 & P899 &  P897 & P895 & P894 & P892 & P889 & P888 & P887 & P876 & P874 & P871 & P780 &  P778 & P777 & P776 & P775 & P774 & P872 & P780 & P778 & P777 & P776 & P775 &  P774 & P890 & P888 & P887 & P876 & P874 & P871 & P780 & P778 & P777 & P776 &  P775 & P774 & P872 & P780 & P778 & P777 & P776 & P775 & P774 & P0) & P0" 1;
pushnode 122 "( a6 = Sing(a1) & P931 & P930 & P896 & P894 & P892 & P889 & P888 & P887 &  P876 & P874 & P871 & P780 & P778 & P777 & P776 & P775 & P774 & P872 & P780 &  P778 & P777 & P776 & P775 & P774 & P0) & ( a2 = a1 & P934 & P933 & P893 & P892 & P889 & P888 & P887 & P876 & P874 &  P871 & P780 & P778 & P777 & P776 & P775 & P774 & P872 & P780 & P778 & P777 &  P776 & P775 & P774 & P931 & P930 & P896 & P894 & P892 & P889 & P888 & P887 &  P876 & P874 & P871 & P780 & P778 & P777 & P776 & P775 & P774 & P872 & P780 &  P778 & P777 & P776 & P775 & P774 & P0) & P0 -> ( a1 Couple a2 = a6 & P929 & P899 & P897 & P895 & P894 & P892 & P889 &  P888 & P887 & P876 & P874 & P871 & P780 & P778 & P777 & P776 & P775 & P774 &  P872 & P780 & P778 & P777 & P776 & P775 & P774 & P890 & P888 & P887 & P876 &  P874 & P871 & P780 & P778 & P777 & P776 & P775 & P774 & P872 & P780 & P778 &  P777 & P776 & P775 & P774 & P0) & P0" 1;
pushnode 121 " (a2 E Sing(a1) & P933 & P893 & P892 & P889 &  P888 & P887 & P876 & P874 & P871 & P780 & P778 & P777 & P776 & P775 & P774 &  P872 & P780 & P778 & P777 & P776 & P775 & P774 & P931 & P930 & P896 & P894 &  P892 & P889 & P888 & P887 & P876 & P874 & P871 & P780 & P778 & P777 & P776 &  P775 & P774 & P872 & P780 & P778 & P777 & P776 & P775 & P774 & P0) &  (a6 = Sing(a1) &  P931 & P930 & P896 & P894 & P892 & P889 & P888 & P887 & P876 & P874 & P871 &  P780 & P778 & P777 & P776 & P775 & P774 & P872 & P780 & P778 & P777 & P776 &  P775 & P774 & P0) & P0 -> ( a1 Couple a2 = a6 & P929 & P899 & P897 & P895 & P894 & P892 & P889 &  P888 & P887 & P876 & P874 & P871 & P780 & P778 & P777 & P776 & P775 & P774 &  P872 & P780 & P778 & P777 & P776 & P775 & P774 & P890 & P888 & P887 & P876 &  P874 & P871 & P780 & P778 & P777 & P776 & P775 & P774 & P872 & P780 & P778 &  P777 & P776 & P775 & P774 & P0) & P0" 1;
pushnode 119 "  (a6 = Sing(a1) & P931 & P930 & P896 & P894 &  P892 & P889 & P888 & P887 & P876 & P874 & P871 & P780 & P778 & P777 & P776 &  P775 & P774 & P872 & P780 & P778 & P777 & P776 & P775 & P774 & P0) &  (a2 E a6 & P893 & P892 & P889 & P888 & P887 & P876 &  P874 & P871 & P780 & P778 & P777 & P776 & P775 & P774 & P872 & P780 & P778 &  P777 & P776 & P775 & P774 & P0) & P0 -> ( a1 Couple a2 = a6 & P929 & P899 & P897 & P895 & P894 & P892 & P889 &  P888 & P887 & P876 & P874 & P871 & P780 & P778 & P777 & P776 & P775 & P774 &  P872 & P780 & P778 & P777 & P776 & P775 & P774 & P890 & P888 & P887 & P876 &  P874 & P871 & P780 & P778 & P777 & P776 & P775 & P774 & P872 & P780 & P778 &  P777 & P776 & P775 & P774 & P0) & P0" 1;
pushnode 118 " ((a6 = Sing(a1) v a6 = a1 Couple a2) &  P930 & P896 & P894 & P892 & P889 & P888 & P887 & P876 & P874 & P871 & P780 &  P778 & P777 & P776 & P775 & P774 & P872 & P780 & P778 & P777 & P776 & P775 &  P774 & P0) &  (a2 E a6 &  P893 & P892 & P889 & P888 & P887 & P876 & P874 & P871 & P780 & P778 & P777 &  P776 & P775 & P774 & P872 & P780 & P778 & P777 & P776 & P775 & P774 & P0) & P0 -> ( a1 Couple a2 = a6 & P929 & P899 & P897 & P895 & P894 & P892 & P889 &  P888 & P887 & P876 & P874 & P871 & P780 & P778 & P777 & P776 & P775 & P774 &  P872 & P780 & P778 & P777 & P776 & P775 & P774 & P890 & P888 & P887 & P876 &  P874 & P871 & P780 & P778 & P777 & P776 & P775 & P774 & P872 & P780 & P778 &  P777 & P776 & P775 & P774 & P0) & P0" 2;
pushnode 117 "  (a6 E a1 Kpair a2 &  P896 & P894 & P892 & P889 & P888 & P887 & P876 & P874 & P871 & P780 & P778 &  P777 & P776 & P775 & P774 & P872 & P780 & P778 & P777 & P776 & P775 & P774 & P0) &  (a2 E a6 & P893 & P892 & P889 & P888 & P887 & P876 & P874 & P871 &  P780 & P778 & P777 & P776 & P775 & P774 & P872 & P780 & P778 & P777 & P776 &  P775 & P774 & P0) & P0 -> ( a1 Couple a2 = a6 & P929 & P899 & P897 & P895 & P894 & P892 & P889 &  P888 & P887 & P876 & P874 & P871 & P780 & P778 & P777 & P776 & P775 & P774 &  P872 & P780 & P778 & P777 & P776 & P775 & P774 & P890 & P888 & P887 & P876 &  P874 & P871 & P780 & P778 & P777 & P776 & P775 & P774 & P872 & P780 & P778 &  P777 & P776 & P775 & P774 & P0) & P0" 1;
pushnode 95 " (a5 = a1 Couple a2 &  P899 & P897 & P895 & P894 & P892 & P889 & P888 & P887 & P876 & P874 & P871 &  P780 & P778 & P777 & P776 & P775 & P774 & P872 & P780 & P778 & P777 & P776 &  P775 & P774 & P0) &  (a6 E a1 Kpair a2 &  P896 & P894 & P892 & P889 & P888 & P887 & P876 & P874 & P871 & P780 & P778 &  P777 & P776 & P775 & P774 & P872 & P780 & P778 & P777 & P776 & P775 & P774 & P0) &  (a2 E a6 & P893 & P892 & P889 & P888 & P887 & P876 & P874 & P871 &  P780 & P778 & P777 & P776 & P775 & P774 & P872 & P780 & P778 & P777 & P776 &  P775 & P774 & P0) & P0 -> ( a5 = a6 & P890 & P888 & P887 & P876 & P874 & P871 & P780 & P778 & P777 &  P776 & P775 & P774 & P872 & P780 & P778 & P777 & P776 & P775 & P774 & P0) & P0" 1;
pushnode 116 "( a7 = a1 & P927 & P924 & P919 & P917 & P916 & P902 & P901 & P891 & P889 &  P888 & P887 & P876 & P874 & P871 & P780 & P778 & P777 & P776 & P775 & P774 &  P872 & P780 & P778 & P777 & P776 & P775 & P774 & P898 & P897 & P895 & P894 &  P892 & P889 & P888 & P887 & P876 & P874 & P871 & P780 & P778 & P777 & P776 &  P775 & P774 & P872 & P780 & P778 & P777 & P776 & P775 & P774 & P914 & P913 &  P912 & P911 & P907 & P905 & P896 & P894 & P892 & P889 & P888 & P887 & P876 &  P874 & P871 & P780 & P778 & P777 & P776 & P775 & P774 & P872 & P780 & P778 &  P777 & P776 & P775 & P774 & P904 & P898 & P897 & P895 & P894 & P892 & P889 &  P888 & P887 & P876 & P874 & P871 & P780 & P778 & P777 & P776 & P775 & P774 &  P872 & P780 & P778 & P777 & P776 & P775 & P774 & P890 & P888 & P887 & P876 &  P874 & P871 & P780 & P778 & P777 & P776 & P775 & P774 & P872 & P780 & P778 &  P777 & P776 & P775 & P774 & P0) & P0 -> (a7 = a1 & P925 & P919 & P917 & P916 & P902 &  P901 & P891 & P889 & P888 & P887 & P876 & P874 & P871 & P780 & P778 & P777 &  P776 & P775 & P774 & P872 & P780 & P778 & P777 & P776 & P775 & P774 & P898 &  P897 & P895 & P894 & P892 & P889 & P888 & P887 & P876 & P874 & P871 & P780 &  P778 & P777 & P776 & P775 & P774 & P872 & P780 & P778 & P777 & P776 & P775 &  P774 & P914 & P913 & P912 & P911 & P907 & P905 & P896 & P894 & P892 & P889 &  P888 & P887 & P876 & P874 & P871 & P780 & P778 & P777 & P776 & P775 & P774 &  P872 & P780 & P778 & P777 & P776 & P775 & P774 & P904 & P898 & P897 & P895 &  P894 & P892 & P889 & P888 & P887 & P876 & P874 & P871 & P780 & P778 & P777 &  P776 & P775 & P774 & P872 & P780 & P778 & P777 & P776 & P775 & P774 & P890 &  P888 & P887 & P876 & P874 & P871 & P780 & P778 & P777 & P776 & P775 & P774 &  P872 & P780 & P778 & P777 & P776 & P775 & P774 & P0) & P0" 0;
pushnode 115 " (a7 = a1 & P926 & P924 & P919 & P917 & P916 &  P902 & P901 & P891 & P889 & P888 & P887 & P876 & P874 & P871 & P780 & P778 &  P777 & P776 & P775 & P774 & P872 & P780 & P778 & P777 & P776 & P775 & P774 &  P898 & P897 & P895 & P894 & P892 & P889 & P888 & P887 & P876 & P874 & P871 &  P780 & P778 & P777 & P776 & P775 & P774 & P872 & P780 & P778 & P777 & P776 &  P775 & P774 & P914 & P913 & P912 & P911 & P907 & P905 & P896 & P894 & P892 &  P889 & P888 & P887 & P876 & P874 & P871 & P780 & P778 & P777 & P776 & P775 &  P774 & P872 & P780 & P778 & P777 & P776 & P775 & P774 & P904 & P898 & P897 &  P895 & P894 & P892 & P889 & P888 & P887 & P876 & P874 & P871 & P780 & P778 &  P777 & P776 & P775 & P774 & P872 & P780 & P778 & P777 & P776 & P775 & P774 &  P890 & P888 & P887 & P876 & P874 & P871 & P780 & P778 & P777 & P776 & P775 &  P774 & P872 & P780 & P778 & P777 & P776 & P775 & P774 & P0) & P0 -> ( a7 = a1 & P925 & P919 & P917 & P916 & P902 & P901 & P891 & P889 & P888 &  P887 & P876 & P874 & P871 & P780 & P778 & P777 & P776 & P775 & P774 & P872 &  P780 & P778 & P777 & P776 & P775 & P774 & P898 & P897 & P895 & P894 & P892 &  P889 & P888 & P887 & P876 & P874 & P871 & P780 & P778 & P777 & P776 & P775 &  P774 & P872 & P780 & P778 & P777 & P776 & P775 & P774 & P914 & P913 & P912 &  P911 & P907 & P905 & P896 & P894 & P892 & P889 & P888 & P887 & P876 & P874 &  P871 & P780 & P778 & P777 & P776 & P775 & P774 & P872 & P780 & P778 & P777 &  P776 & P775 & P774 & P904 & P898 & P897 & P895 & P894 & P892 & P889 & P888 &  P887 & P876 & P874 & P871 & P780 & P778 & P777 & P776 & P775 & P774 & P872 &  P780 & P778 & P777 & P776 & P775 & P774 & P890 & P888 & P887 & P876 & P874 &  P871 & P780 & P778 & P777 & P776 & P775 & P774 & P872 & P780 & P778 & P777 &  P776 & P775 & P774 & P0) & P0" 0;
pushnode 114 "( (a7 = a1 v a7 = a1) & P924 & P919 & P917 & P916 & P902 & P901 &  P891 & P889 & P888 & P887 & P876 & P874 & P871 & P780 & P778 & P777 & P776 &  P775 & P774 & P872 & P780 & P778 & P777 & P776 & P775 & P774 & P898 & P897 &  P895 & P894 & P892 & P889 & P888 & P887 & P876 & P874 & P871 & P780 & P778 &  P777 & P776 & P775 & P774 & P872 & P780 & P778 & P777 & P776 & P775 & P774 &  P914 & P913 & P912 & P911 & P907 & P905 & P896 & P894 & P892 & P889 & P888 &  P887 & P876 & P874 & P871 & P780 & P778 & P777 & P776 & P775 & P774 & P872 &  P780 & P778 & P777 & P776 & P775 & P774 & P904 & P898 & P897 & P895 & P894 &  P892 & P889 & P888 & P887 & P876 & P874 & P871 & P780 & P778 & P777 & P776 &  P775 & P774 & P872 & P780 & P778 & P777 & P776 & P775 & P774 & P890 & P888 &  P887 & P876 & P874 & P871 & P780 & P778 & P777 & P776 & P775 & P774 & P872 &  P780 & P778 & P777 & P776 & P775 & P774 & P0) & P0 -> (a7 = a1 & P925 & P919 & P917 & P916 & P902 &  P901 & P891 & P889 & P888 & P887 & P876 & P874 & P871 & P780 & P778 & P777 &  P776 & P775 & P774 & P872 & P780 & P778 & P777 & P776 & P775 & P774 & P898 &  P897 & P895 & P894 & P892 & P889 & P888 & P887 & P876 & P874 & P871 & P780 &  P778 & P777 & P776 & P775 & P774 & P872 & P780 & P778 & P777 & P776 & P775 &  P774 & P914 & P913 & P912 & P911 & P907 & P905 & P896 & P894 & P892 & P889 &  P888 & P887 & P876 & P874 & P871 & P780 & P778 & P777 & P776 & P775 & P774 &  P872 & P780 & P778 & P777 & P776 & P775 & P774 & P904 & P898 & P897 & P895 &  P894 & P892 & P889 & P888 & P887 & P876 & P874 & P871 & P780 & P778 & P777 &  P776 & P775 & P774 & P872 & P780 & P778 & P777 & P776 & P775 & P774 & P890 &  P888 & P887 & P876 & P874 & P871 & P780 & P778 & P777 & P776 & P775 & P774 &  P872 & P780 & P778 & P777 & P776 & P775 & P774 & P0) & P0" 2;
pushnode 111 "P0 -> (( a7 = a1 v a7 = a1 -> a7 = a1) &  P919 & P917 & P916 & P902 & P901 & P891 & P889 & P888 & P887 & P876 & P874 &  P871 & P780 & P778 & P777 & P776 & P775 & P774 & P872 & P780 & P778 & P777 &  P776 & P775 & P774 & P898 & P897 & P895 & P894 & P892 & P889 & P888 & P887 &  P876 & P874 & P871 & P780 & P778 & P777 & P776 & P775 & P774 & P872 & P780 &  P778 & P777 & P776 & P775 & P774 & P914 & P913 & P912 & P911 & P907 & P905 &  P896 & P894 & P892 & P889 & P888 & P887 & P876 & P874 & P871 & P780 & P778 &  P777 & P776 & P775 & P774 & P872 & P780 & P778 & P777 & P776 & P775 & P774 &  P904 & P898 & P897 & P895 & P894 & P892 & P889 & P888 & P887 & P876 & P874 &  P871 & P780 & P778 & P777 & P776 & P775 & P774 & P872 & P780 & P778 & P777 &  P776 & P775 & P774 & P890 & P888 & P887 & P876 & P874 & P871 & P780 & P778 &  P777 & P776 & P775 & P774 & P872 & P780 & P778 & P777 & P776 & P775 & P774 & P0) & P0" 1;
pushnode 113 "(a7 = a1 & P920 & P918 & P917 & P916 & P902 &  P901 & P891 & P889 & P888 & P887 & P876 & P874 & P871 & P780 & P778 & P777 &  P776 & P775 & P774 & P872 & P780 & P778 & P777 & P776 & P775 & P774 & P898 &  P897 & P895 & P894 & P892 & P889 & P888 & P887 & P876 & P874 & P871 & P780 &  P778 & P777 & P776 & P775 & P774 & P872 & P780 & P778 & P777 & P776 & P775 &  P774 & P914 & P913 & P912 & P911 & P907 & P905 & P896 & P894 & P892 & P889 &  P888 & P887 & P876 & P874 & P871 & P780 & P778 & P777 & P776 & P775 & P774 &  P872 & P780 & P778 & P777 & P776 & P775 & P774 & P904 & P898 & P897 & P895 &  P894 & P892 & P889 & P888 & P887 & P876 & P874 & P871 & P780 & P778 & P777 &  P776 & P775 & P774 & P872 & P780 & P778 & P777 & P776 & P775 & P774 & P890 &  P888 & P887 & P876 & P874 & P871 & P780 & P778 & P777 & P776 & P775 & P774 &  P872 & P780 & P778 & P777 & P776 & P775 & P774 & P0) & P0 ->  (a7 = a1 & P922 & P921 & P918 & P917 & P916 &  P902 & P901 & P891 & P889 & P888 & P887 & P876 & P874 & P871 & P780 & P778 &  P777 & P776 & P775 & P774 & P872 & P780 & P778 & P777 & P776 & P775 & P774 &  P898 & P897 & P895 & P894 & P892 & P889 & P888 & P887 & P876 & P874 & P871 &  P780 & P778 & P777 & P776 & P775 & P774 & P872 & P780 & P778 & P777 & P776 &  P775 & P774 & P914 & P913 & P912 & P911 & P907 & P905 & P896 & P894 & P892 &  P889 & P888 & P887 & P876 & P874 & P871 & P780 & P778 & P777 & P776 & P775 &  P774 & P872 & P780 & P778 & P777 & P776 & P775 & P774 & P904 & P898 & P897 &  P895 & P894 & P892 & P889 & P888 & P887 & P876 & P874 & P871 & P780 & P778 &  P777 & P776 & P775 & P774 & P872 & P780 & P778 & P777 & P776 & P775 & P774 &  P890 & P888 & P887 & P876 & P874 & P871 & P780 & P778 & P777 & P776 & P775 &  P774 & P872 & P780 & P778 & P777 & P776 & P775 & P774 & P0) & P0" 0;
pushnode 112 "( a7 = a1 & P920 & P918 & P917 & P916 & P902 & P901 & P891 & P889 & P888 &  P887 & P876 & P874 & P871 & P780 & P778 & P777 & P776 & P775 & P774 & P872 &  P780 & P778 & P777 & P776 & P775 & P774 & P898 & P897 & P895 & P894 & P892 &  P889 & P888 & P887 & P876 & P874 & P871 & P780 & P778 & P777 & P776 & P775 &  P774 & P872 & P780 & P778 & P777 & P776 & P775 & P774 & P914 & P913 & P912 &  P911 & P907 & P905 & P896 & P894 & P892 & P889 & P888 & P887 & P876 & P874 &  P871 & P780 & P778 & P777 & P776 & P775 & P774 & P872 & P780 & P778 & P777 &  P776 & P775 & P774 & P904 & P898 & P897 & P895 & P894 & P892 & P889 & P888 &  P887 & P876 & P874 & P871 & P780 & P778 & P777 & P776 & P775 & P774 & P872 &  P780 & P778 & P777 & P776 & P775 & P774 & P890 & P888 & P887 & P876 & P874 &  P871 & P780 & P778 & P777 & P776 & P775 & P774 & P872 & P780 & P778 & P777 &  P776 & P775 & P774 & P0) & P0 -> ( (a7 = a1 v a7 = a1) & P921 & P918 & P917 & P916 & P902 & P901 &  P891 & P889 & P888 & P887 & P876 & P874 & P871 & P780 & P778 & P777 & P776 &  P775 & P774 & P872 & P780 & P778 & P777 & P776 & P775 & P774 & P898 & P897 &  P895 & P894 & P892 & P889 & P888 & P887 & P876 & P874 & P871 & P780 & P778 &  P777 & P776 & P775 & P774 & P872 & P780 & P778 & P777 & P776 & P775 & P774 &  P914 & P913 & P912 & P911 & P907 & P905 & P896 & P894 & P892 & P889 & P888 &  P887 & P876 & P874 & P871 & P780 & P778 & P777 &