pushreference 1 "P0 -> (Real(0) & P2 & P0) & P0" "";
THEOREMS:=("zero",(termtosequent(parseprop("P0 -> (Real(0) & P1 & P0) & P0")),hd(!PROOFSTACK)))::(!THEOREMS);
PROOFSTACK:=nil;
td "zero";
pushreference 1 "P0 -> (Real(1) & P4 & P0) & P0" "";
THEOREMS:=("one",(termtosequent(parseprop("P0 -> (Real(1) & P3 & P0) & P0")),hd(!PROOFSTACK)))::(!THEOREMS);
PROOFSTACK:=nil;
td "one";
pushreference 1 "P0 -> (Real(a1 + a2) & P6 & P0) & P0" "";
THEOREMS:=("rplus",(termtosequent(parseprop("P0 -> (Real(a1 + a2) & P5 & P0) & P0")),hd(!PROOFSTACK)))::(!THEOREMS);
PROOFSTACK:=nil;
td "rplus";
pushreference 1 "P0 -> (Real(a1 * a2) & P8 & P0) & P0" "";
THEOREMS:=("rtimes",(termtosequent(parseprop("P0 ->  (Real(a1 * a2) & P7 & P0) & P0")),hd(!PROOFSTACK)))::(!THEOREMS);
PROOFSTACK:=nil;
td "rtimes";
pushreference 1 "P0 -> (Real(-(a1)) & P10 & P0) & P0" "";
THEOREMS:=("rminus",(termtosequent(parseprop("P0 -> (Real(-(a1)) & P9 & P0) & P0")),hd(!PROOFSTACK)))::(!THEOREMS);
PROOFSTACK:=nil;
td "rminus";
pushreference 1 "P0 ->  (Real(/(a1)) & P12 & P0) & P0" "";
THEOREMS:=("rinv",(termtosequent(parseprop("P0 -> (Real(/(a1)) & P11 & P0) & P0")),hd(!PROOFSTACK)))::(!THEOREMS);
PROOFSTACK:=nil;
td "rinv";
pushreference 1 "P0 -> (a1 + a2 = a2 + a1 & P14 & P0) & P0" "";
THEOREMS:=("acom",(termtosequent(parseprop("P0 -> (a1 + a2 = a2 + a1 & P13 & P0) & P0")),hd(!PROOFSTACK)))::(!THEOREMS);
PROOFSTACK:=nil;
td "acom";
pushreference 1 "P0 -> ([a1 + a2] + a3 = a1 + a2 + a3 & P16 & P0) & P0" "";
THEOREMS:=("aas",(termtosequent(parseprop("P0 -> ([a1 + a2] + a3 = a1 + a2 + a3 & P15 & P0) & P0")),hd(!PROOFSTACK)))::(!THEOREMS);
PROOFSTACK:=nil;
td "aas";
pushreference 1 "(Real(a1) & P19 & P0) & P0 -> (a1 + 0 = a1 & P20 & P0) & P0" "";
THEOREMS:=("aid",(termtosequent(parseprop("(Real(a1) & P17 & P0) & P0 -> (a1 + 0 = a1 & P18 & P0) & P0")),hd(!PROOFSTACK)))::(!THEOREMS);
PROOFSTACK:=nil;
td "aid";
pushreference 1 "P0 -> (a1 + -(a1) = 0 & P22 & P0) & P0" "";
THEOREMS:=("ainv",(termtosequent(parseprop("P0 -> (a1 + -(a1) = 0 & P21 & P0) & P0")),hd(!PROOFSTACK)))::(!THEOREMS);
PROOFSTACK:=nil;
td "ainv";
pushreference 1 "P0 -> ([a1 * a2] * a3 = a1 * a2 * a3 & P24 & P0) & P0" "";
THEOREMS:=("mas",(termtosequent(parseprop("P0 -> ([a1 * a2] * a3 = a1 * a2 * a3 & P23 & P0) & P0")),hd(!PROOFSTACK)))::(!THEOREMS);
PROOFSTACK:=nil;
td "mas";
pushreference 1 "P0 ->  (a1 * a2 = a2 * a1 & P26 & P0) & P0" "";
THEOREMS:=("mcom",(termtosequent(parseprop("P0 -> (a1 * a2 = a2 * a1 & P25 & P0) & P0")),hd(!PROOFSTACK)))::(!THEOREMS);
PROOFSTACK:=nil;
td "mcom";
pushreference 1 "(Real(a1) & P29 & P0) & P0 -> ( a1 * 1 = a1 & P30 & P0) & P0" "";
THEOREMS:=("mid",(termtosequent(parseprop("(Real(a1) & P27 & P0) & P0 -> (a1 * 1 = a1 & P28 & P0) & P0")),hd(!PROOFSTACK)))::(!THEOREMS);
PROOFSTACK:=nil;
td "mid";
pushreference 1 "P0 -> ((~a1 eq 0 -> a1 * /(a1) = 1) & P32 & P0) & P0" "";
THEOREMS:=("minv",(termtosequent(parseprop("P0 -> ((~a1 eq 0 -> a1 * /(a1) = 1) & P31 & P0) & P0")),hd(!PROOFSTACK)))::(!THEOREMS);
PROOFSTACK:=nil;
td "minv";
pushreference 1 "P0 -> (a1 * [a2 + a3] = a1 * a2 + a1 * a3 & P34 & P0) & P0" "";
THEOREMS:=("dist",(termtosequent(parseprop("P0 -> (a1 * [a2 + a3] =  a1 * a2 + a1 * a3 & P33 & P0) & P0")),hd(!PROOFSTACK)))::(!THEOREMS);
PROOFSTACK:=nil;
td "dist";
pushreference 1 "P0 -> ((a1 <= a2 v a2 <= a1) & P36 & P0) & P0" "";
THEOREMS:=("totorder",(termtosequent(parseprop("P0 -> (( a1 <= a2 v a2 <= a1) & P35 & P0) & P0")),hd(!PROOFSTACK)))::(!THEOREMS);
PROOFSTACK:=nil;
td "totorder";
pushreference 1 "P0 -> ((a1 <= a2 & a2 <= a1 -> a1 = a2) & P38 & P0) & P0" "";
THEOREMS:=("eqbyord",(termtosequent(parseprop("P0 -> ((a1 <= a2 & a2 <= a1 -> a1 = a2) & P37 & P0) & P0")),hd(!PROOFSTACK)))::(!THEOREMS);
PROOFSTACK:=nil;
td "eqbyord";
pushreference 1 "P0 -> ( (a1 <= a2 & a2 <= a3 -> a1 <= a3) & P40 & P0) & P0" "";
THEOREMS:=("ordtrans",(termtosequent(parseprop("P0 ->  ((a1 <= a2 & a2 <= a3 -> a1 <= a3) & P39 & P0) & P0")),hd(!PROOFSTACK)))::(!THEOREMS);
PROOFSTACK:=nil;
td "ordtrans";
pushreference 1 "P0 -> ((a1 <= a2 -> a1 + a3 <= a2 + a3) & P42 & P0) & P0" "";
THEOREMS:=("ordadd",(termtosequent(parseprop("P0 -> ((a1 <= a2 -> a1 + a3 <= a2 + a3) & P41 & P0) & P0")),hd(!PROOFSTACK)))::(!THEOREMS);
PROOFSTACK:=nil;
td "ordadd";
pushreference 1 "P0 -> ((a1 <= a2 -> a3 + a1 <= a3 + a2) & P44 & P0) & P0" "";
THEOREMS:=("ordaddl",(termtosequent(parseprop("P0 ->  ((a1 <= a2 -> a3 + a1 <= a3 + a2) & P43 & P0) & P0")),hd(!PROOFSTACK)))::(!THEOREMS);
PROOFSTACK:=nil;
td "ordaddl";
pushreference 1 "P0 -> ((a1 <= a2 & 0 <= a3 -> a1 * a3 <= a2 * a3) & P46 & P0) & P0" "";
THEOREMS:=("ordmult",(termtosequent(parseprop("P0 -> ((a1 <= a2 & 0 <= a3 -> a1 * a3 <= a2 * a3) & P45 & P0) & P0")),hd(!PROOFSTACK)))::(!THEOREMS);
PROOFSTACK:=nil;
td "ordmult";
pushnode 1 "P0 -> (a1 = a1 & P1 & P0) & P0" 0;
THEOREMS:=("reflx",(termtosequent(parseprop("P0 -> (a1 = a1 & P1 & P0) & P0")),hd(!PROOFSTACK)))::(!THEOREMS);
PROOFSTACK:=nil;
td "reflx";
pushnode 5 "P0 -> (a1 = a1 & P5 & P2 & P3 & P1 & P0) & P0" 0;
pushreference 4 "P0 -> (a1 = a1 & P6 & P0) & P0" "reflx";
pushnode 3 "P0 -> (a1 = a1 & P5 & P2 & P3 & P1 & P0) & P0" 2;
pushnode 2 "( a1 = a2 & P2 & P1 & P0) & P0 -> (a2 = a1 & P3 & P1 & P0) & P0" 1;
pushnode 1 "P0 ->  ((a1 = a2 -> a2 = a1) & P1 & P0) & P0" 1;
THEOREMS:=("symm",(termtosequent(parseprop("P0 -> ((a1 = a2 -> a2 = a1) & P1 & P0) & P0")),hd(!PROOFSTACK)))::(!THEOREMS);
PROOFSTACK:=nil;
td "symm";
pushnode 4 "(a1 = a3 & P8 & P4 & P5 & P2 & P1 & P0) & P0 -> (a1 = a3 & P9 & P6 & P3 & P1 & P0) & P0" 0;
pushnode 3 " (a1 = a2 & P4 & P2 & P1 & P0) & (a2 = a3 & P5 & P2 & P1 & P0) & P0 -> (a1 = a3 & P6 & P3 & P1 & P0) & P0" 1;
pushnode 2 " ((a1 = a2 & a2 = a3) & P2 & P1 & P0) & P0 -> (a1 = a3 & P3 & P1 & P0) & P0" 1;
pushnode 1 "P0 ->  ((a1 = a2 & a2 = a3 -> a1 = a3) & P1 & P0) & P0" 1;
THEOREMS:=("trans",(termtosequent(parseprop("P0 -> ((a1 = a2 & a2 = a3 -> a1 = a3) & P1 & P0) & P0")),hd(!PROOFSTACK)))::(!THEOREMS);
PROOFSTACK:=nil;
td "trans";
pushnode 3 "P0 -> (a1 + a3 = a1 + a3 & P5 & P2 & P3 & P1 & P0) & P0" 0;
pushnode 2 " (a1 = a2 & P2 & P1 & P0) & P0 -> (a1 + a3 = a2 + a3 & P3 & P1 & P0) & P0" 1;
pushnode 1 "P0 ->  ((a1 = a2 -> a1 + a3 = a2 + a3) & P1 & P0) & P0" 1;
THEOREMS:=("aeq",(termtosequent(parseprop("P0 -> ((a1 = a2 -> a1 + a3 = a2 + a3) & P1 & P0) & P0")),hd(!PROOFSTACK)))::(!THEOREMS);
PROOFSTACK:=nil;
td "aeq";
pushnode 3 "P0 -> (a3 + a1 = a3 + a1 & P5 & P2 & P3 & P1 & P0) & P0" 0;
pushnode 2 " (a1 = a2 & P2 & P1 & P0) & P0 -> (a3 + a1 = a3 + a2 & P3 & P1 & P0) & P0" 1;
pushnode 1 "P0 ->  ((a1 = a2 -> a3 + a1 = a3 + a2) & P1 & P0) & P0" 1;
THEOREMS:=("aeql",(termtosequent(parseprop("P0 -> ((a1 = a2 -> a3 + a1 = a3 + a2) & P1 & P0) & P0")),hd(!PROOFSTACK)))::(!THEOREMS);
PROOFSTACK:=nil;
td "aeql";
pushnode 3 "P0 -> (a1 * a3 = a1 * a3 & P5 & P2 & P3 & P1 & P0) & P0" 0;
pushnode 2 " (a1 = a2 & P2 & P1 & P0) & P0 -> (a1 * a3 = a2 * a3 & P3 & P1 & P0) & P0" 1;
pushnode 1 "P0 ->  ((a1 = a2 -> a1 * a3 = a2 * a3) & P1 & P0) & P0" 1;
THEOREMS:=("meq",(termtosequent(parseprop("P0 -> ((a1 = a2 -> a1 * a3 = a2 * a3) & P1 & P0) & P0")),hd(!PROOFSTACK)))::(!THEOREMS);
PROOFSTACK:=nil;
td "meq";
pushnode 3 "P0 -> (a3 * a1 = a3 * a1 & P5 & P2 & P3 & P1 & P0) & P0" 0;
pushnode 2 " (a1 = a2 & P2 & P1 & P0) & P0 -> (a3 * a1 = a3 * a2 & P3 & P1 & P0) & P0" 1;
pushnode 1 "P0 ->  ((a1 = a2 -> a3 * a1 = a3 * a2) & P1 & P0) & P0" 1;
THEOREMS:=("meql",(termtosequent(parseprop("P0 -> ((a1 = a2 -> a3 * a1 = a3 * a2) & P1 & P0) & P0")),hd(!PROOFSTACK)))::(!THEOREMS);
PROOFSTACK:=nil;
td "meql";
pushnode 12 "( [a1 + a2] * a3 = a1 * a3 + a2 * a3 & P17 & P15 & P12 & P10 & P7 & P5 & P3 & P0) & P0 -> ([a1 + a2] * a3 = a1 * a3 + a2 * a3 & P18 & P13 & P8 & P1 & P0) & P0" 0;
pushnode 11 "(a3 * a2 = a2 * a3 & P15 & P0) & ([a1 + a2] * a3 = a1 * a3 + a3 * a2 & P12 & P10 & P7 & P5 & P3 & P0) & P0 -> ([a1 + a2] * a3 = a1 * a3 + a2 * a3 & P13 & P8 & P1 & P0) & P0" 1;
pushreference 10 "P0 -> (a3 * a2 = a2 * a3 & P14 & P0) & P0" "mcom";
pushnode 9 "( [a1 + a2] * a3 = a1 * a3 + a3 * a2 & P12 & P10 & P7 & P5 & P3 & P0) & P0 -> ([ a1 + a2] * a3 = a1 * a3 + a2 * a3 & P13 & P8 & P1 & P0) & P0" 2;
pushnode 8 "(a3 * a1 = a1 * a3 & P10 & P0) & ([a1 + a2] * a3 = a3 * a1 + a3 * a2 & P7 & P5 & P3 & P0) & P0 ->  ([a1 + a2] * a3 = a1 * a3 + a2 * a3 & P8 & P1 & P0) & P0" 1;
pushreference 7 "P0 -> (a3 * a1 = a1 * a3 & P9 & P0) & P0" "mcom";
pushnode 6 "( [a1 + a2] * a3 = a3 * a1 + a3 * a2 & P7 & P5 & P3 & P0) & P0 -> ( [a1 + a2] * a3 = a1 * a3 + a2 * a3 & P8 & P1 & P0) & P0" 2;
pushnode 5 " (a3 * [a1 + a2] = [a1 + a2] * a3 & P5 & P0) & (a3 * [a1 + a2] = a3 * a1 + a3 * a2 & P3 & P0) & P0 -> ([ a1 + a2] * a3 = a1 * a3 + a2 * a3 & P1 & P0) & P0" 1;
pushreference 4 "P0 -> (a3 * [a1 + a2] = [a1 + a2] * a3 &  P4 & P0) & P0" "mcom";
pushnode 3 "(a3 * [a1 + a2] = a3 * a1 + a3 * a2 & P3 & P0) & P0 -> ([a1 + a2] * a3 = a1 * a3 +  a2 * a3 & P1 & P0) & P0" 2;
pushreference 2 "P0 -> (a3 * [a1 + a2] = a3 * a1 + a3 * a2 & P2 & P0) & P0" "dist";
pushnode 1 "P0 -> ([a1 + a2] * a3 = a1 * a3 + a2 * a3 & P1 & P0) & P0" 2;
THEOREMS:=("distr",(termtosequent(parseprop("P0 -> ([a1 + a2] * a3 = a1 * a3 + a2 * a3 & P1 & P0) & P0")),hd(!PROOFSTACK)))::(!THEOREMS);
PROOFSTACK:=nil;
td "distr";
pushnode 23 "(a1 = a2 & P64 & P62 & P54 & P52 & P44 & P42 & P36 & P34 & P27 & P25 & P18 & P11 & P0) & P0 -> (a1 = a2 & P68 & P58 & P48 & P40 & P32 & P23 & P9 & P4 & P0) & P0" 0;
pushnode 22 "(a2 + 0 = a2 & P62 & P0) & ( a1 = a2 + 0 & P54 & P52 & P44 & P42 & P36 & P34 & P27 & P25 & P18 & P11 & P0) & (Real(a2) & P56 & P46 & P38 & P30 & P21 & P7 & P2 & P0) & P0 -> (a1 = a2 & P58 & P48 & P40 & P32 & P23 & P9 & P4 & P0) & P0" 1;
pushnode 21 "(Real(a2) & P56 & P46 & P38 & P30 & P21 & P7 & P2 & P0) & (a1 = a2 + 0 & P54 & P52 & P44 & P42 & P36 & P34 & P27 & P25 & P18 & P11 & P0) & P0 -> (Real(a2) & P61 & P0) & (a1 = a2 & P58 & P48 & P40 & P32 & P23 & P9 & P4 & P0) & P0" 0;
pushreference 20 " (Real(a2) & P59 & P0) & P0 -> (a2 + 0 = a2 & P60 & P0) & P0" "aid";
pushnode 19 "(a1 = a2 + 0 & P54 & P52 & P44 & P42 & P36 & P34 & P27 & P25 & P18 & P11 & P0) & (Real(a2) & P56 & P46 & P38 & P30 & P21 &  P7 & P2 & P0) & P0 -> (a1 = a2 & P58 & P48 & P40 & P32 & P23 & P9 & P4 & P0) & P0" 3;
pushnode 18 " (a1 + 0 = a1 & P52 & P0) & (a1 + 0 = a2 + 0 & P44 & P42 & P36 &  P34 & P27 & P25 & P18 & P11 & P0) & (Real(a1) &  P45 & P37 & P29 & P20 & P6 & P1 & P0) & (Real(a2) & P46 & P38 & P30 & P21 & P7 & P2 & P0) & P0 -> (a1 = a2 & P48 & P40 & P32 & P23 & P9 & P4 & P0) & P0" 1;
pushnode 17 " (Real(a1) & P45 & P37 & P29 & P20 & P6 & P1 & P0) & (Real(a2) & P46 & P38 &  P30 & P21 & P7 & P2 & P0) & (a1 + 0 = a2 + 0 & P44 & P42 & P36 & P34 & P27 & P25 & P18 & P11 & P0) & P0 -> (Real(a1) & P51 & P0) &  (a1 = a2 & P48 & P40 & P32 & P23 & P9 & P4 & P0) & P0" 0;
pushreference 16 "(Real(a1) & P49 & P0) & P0 ->  (a1 + 0 = a1 & P50 & P0) & P0" "aid";
pushnode 15 "(a1 + 0 = a2 + 0 & P44 & P42 & P36 & P34 & P27 & P25 & P18 & P11 & P0) & (Real(a1) & P45 & P37 & P29 & P20 & P6 & P1 & P0) &  (Real(a2) & P46 & P38 & P30 & P21 & P7 & P2 & P0) & P0 -> (a1 = a2 & P48 & P40 & P32 & P23 & P9 & P4 & P0) & P0" 3;
pushnode 14 "(a3 + -(a3) = 0 & P42 & P0) & ( a1 + a3 + -(a3) = a2 + a3 + -(a3) & P36 & P34 & P27 & P25 & P18 & P11 & P0) & ( Real(a1) & P37 & P29 & P20 & P6 & P1 & P0) & (Real(a2) & P38 & P30 & P21 & P7 & P2 & P0) & P0 -> (a1 = a2 & P40 & P32 & P23 & P9 & P4 & P0) & P0" 1;
pushreference 13 "P0 -> (a3 + -(a3) = 0 & P41 & P0) & P0" "ainv";
pushnode 12 "( a1 + a3 + -(a3) = a2 + a3 + -(a3) & P36 & P34 & P27 & P25 & P18 & P11 & P0) & ( Real(a1) & P37 & P29 & P20 & P6 & P1 & P0) & (Real(a2) & P38 & P30 & P21 & P7 & P2 & P0) & P0 -> (a1 = a2 & P40 & P32 & P23 & P9 & P4 & P0) & P0" 2;
pushnode 11 "([a2 + a3] + -(a3) = a2 + a3 + -(a3) & P34 & P0) & (a1 + a3 + -(a3) = [a2 + a3] + -(a3) & P27 & P25 & P18 & P11 & P0) & (Real(a1) & P29 & P20 & P6 & P1 & P0) & (Real(a2) & P30 & P21 & P7 & P2 & P0) & P0 -> (a1 = a2 & P32 & P23 & P9 & P4 & P0) & P0" 1;
pushreference 10 "P0 -> ([a2 + a3] + -(a3) = a2 + a3 + -(a3) & P33 & P0) & P0" "aas";
pushnode 9 " (a1 + a3 + -(a3) =  [a2 + a3] + -(a3) & P27 & P25 & P18 & P11 & P0) &  (Real(a1) & P29 & P20 & P6 & P1 & P0) & (Real(a2) & P30 & P21 & P7 & P2 & P0) & P0 -> (a1 = a2 & P32 & P23 & P9 & P4 & P0) & P0" 2;
pushnode 8 "([a1 + a3] + -(a3) = a1 + a3 + -(a3) & P25 & P0) & ([a1 + a3] + -(a3) = [a2 + a3] + -(a3) & P18 & P11 & P0) & (Real(a1) & P20 & P6 & P1 & P0) & (Real(a2) & P21 & P7 & P2 & P0) & P0 -> (a1 = a2 & P23 & P9 & P4 & P0) & P0" 1;
pushreference 7 "P0 -> ([a1 + a3] + -(a3) = a1 + a3 + -(a3) & P24 & P0) & P0" "aas";
pushnode 6 " ([a1 + a3] + -(a3) = [a2 + a3] + -(a3) & P18 & P11 & P0) & (Real(a1) & P20 & P6 & P1 & P0) & (Real(a2) & P21 & P7 & P2 & P0) & P0 -> (a1 = a2 & P23 & P9 & P4 & P0) & P0" 2;
pushnode 5 "(a1 + a3 = a2 + a3 & P12 & P5 & P4 & P0) & P0 -> (a1 + a3 = a2 + a3 & P16 & P11 & P0) & P0" 0;
pushnode 4 " ((a1 + a3 = a2 + a3 -> [a1 + a3] + -(a3) = [a2 + a3] + -(a3)) & P11 & P0) & (a1 + a3 = a2 + a3 & P5 & P4 & P0) & (Real(a1) & P6 & P1 & P0) &  (Real(a2) & P7 & P2 & P0) & P0 -> (a1 = a2 & P9 & P4 & P0) & P0" 2;
pushreference 3 "P0 -> (( a1 + a3 = a2 + a3 -> [a1 + a3] + -(a3) = [a2 + a3] + -(a3)) & P10 & P0) & P0" "aeq";
pushnode 2 "( a1 + a3 = a2 + a3 & P5 & P4 & P0) & (Real(a1) & P6 & P1 & P0) & (Real(a2) & P7 & P2 & P0) & P0 -> (a1 = a2 & P9 & P4 & P0) & P0" 2;
pushnode 1 "(Real(a1) & P1 & P0) & (Real(a2) & P2 & P0) & P0 -> ((a1 + a3 = a2 + a3 -> a1 = a2) & P4 & P0) & P0" 1;
THEOREMS:=("thm 3.1.i",(termtosequent(parseprop(" (Real(a1) & P1 & P0) & (Real(a2) & P2 & P0) & P0 -> ((a1 + a3 = a2 + a3 -> a1 = a2) & P4 & P0) & P0")),hd(!PROOFSTACK)))::(!THEOREMS);
PROOFSTACK:=nil;
td "thm 3.1.i";
pushnode 27 "(a1 * 0 = 0 & P64 & P57 & P0) & P0 -> (a1 * 0 = 0 & P69 & P55 & P43 & P37 & P26 & P14 & P3 & P0) & P0" 0;
pushnode 26 " (0 = a1 * 0 & P58 & P51 & P47 & P39 & P36 & P32 & P28 & P30 & P22 & P16 & P0) & P0 -> (0 = a1 * 0 & P62 & P57 & P0) & P0" 0;
pushnode 25 "((0 = a1 * 0 -> a1 * 0 = 0) & P57 & P0) & (0 = a1 * 0 & P51 &  P47 & P39 & P36 & P32 & P28 & P30 & P22 & P16 & P0) & P0 -> (a1 * 0 = 0 & P55 & P43 & P37 & P26 & P14 & P3 & P0) & P0" 2;
pushreference 24 "P0 -> ((0 = a1 * 0 -> a1 * 0 = 0) & P56 & P0) & P0" "symm";
pushnode 23 "(0 = a1 * 0 & P51 & P47 & P39 & P36 & P32 & P28 & P30 & P22 & P16 & P0) & P0 -> (a1 * 0 = 0 & P55 & P43 & P37 & P26 &  P14 & P3 & P0) & P0" 2;
pushnode 20 "(a1 * 0 + 0 = a1 * 0 & P47 & P0) & (0 = a1 * 0 + 0 & P39 & P36 & P32 & P28 & P30 &  P22 & P16 & P0) & P0 -> (a1 * 0 = 0 & P43 & P37 & P26 & P14 & P3 & P0) & P0" 1;
pushnode 22 "(Real(a1 * 0) & P49 & P0) & (0 = a1 * 0 + 0 & P39 & P36 & P32 & P28 & P30 & P22 & P16 & P0) & P0 ->  (Real(a1 * 0) & P46 & P0) & (a1 * 0 = 0 & P43 & P37 & P26 & P14 & P3 & P0) & P0" 0;
pushreference 21 " P0 -> (Real(a1 * 0) & P48 & P0) & P0" "rtimes";
pushnode 19 "(0 = a1 * 0 + 0 & P39 & P36 & P32 & P28 & P30 & P22 & P16 & P0) & P0 -> (Real(a1 * 0) & P46 & P0) & (a1 * 0 = 0 & P43 & P37 & P26 & P14 & P3 & P0) & P0" 2;
pushreference 18 "(Real(a1 * 0) & P44 & P0) & P0 ->  (a1 * 0 + 0 = a1 * 0 & P45 & P0) & P0" "aid";
pushnode 17 "(0 = a1 * 0 + 0 & P39 & P36 & P32 & P28 & P30 & P22 & P16 & P0) & P0 -> (a1 * 0 = 0 & P43 & P37 & P26 & P14 & P3 & P0) & P0" 3;
pushnode 16 " (a1 * 0 + -(a1 * 0) = 0 & P36 & P28 & P0) & (a1 * 0 + -(a1 * 0) =  a1 * 0 + a1 * 0 + -(a1 * 0) & P32 & P30 & P22 & P16 & P0) & P0 -> (a1 * 0 = 0 & P37 & P26 & P14 & P3 & P0) & P0" 1;
pushnode 15 "( [a1 * 0 + a1 * 0] + -(a1 * 0) = a1 * 0 + a1 * 0 + -(a1 * 0) & P30 & P0) & (a1 * 0 + -(a1 * 0) = [ a1 * 0 + a1 * 0] + -(a1 * 0) & P22 & P16 & P0) & (a1 * 0 + -(a1 * 0) = 0 & P28 & P0) & P0 -> (a1 * 0 = 0 & P26 & P14 & P3 & P0) & P0" 1;
pushreference 14 "P0 ->  ([a1 * 0 + a1 * 0] + -(a1 * 0) = a1 * 0 + a1 * 0 + -(a1 * 0) & P29 & P0) & P0" "aas";
pushnode 13 " (a1 * 0 + -(a1 * 0) = 0 & P28 & P0) & (a1 * 0 + -(a1 * 0) = [ a1 * 0 + a1 * 0] + -(a1 * 0) & P22 & P16 & P0) & P0 -> (a1 * 0 = 0 & P26 & P14 & P3 & P0) & P0" 2;
pushreference 12 "P0 ->  (a1 * 0 + -(a1 * 0) = 0 & P27 & P0) & P0" "ainv";
pushnode 11 " (a1 * 0 + -(a1 * 0) = [a1 * 0 + a1 * 0] + -(a1 * 0) & P22 & P16 & P0) & P0 -> (a1 * 0 = 0 & P26 & P14 & P3 & P0) & P0" 2;
pushnode 10 " (a1 * 0 = a1 * 0 + a1 * 0 & P17 & P11 & P9 & P5 & P0) & P0 -> (a1 * 0 = a1 * 0 + a1 * 0 & P20 & P16 & P0) & P0" 0;
pushnode 9 "(( a1 * 0 = a1 * 0 + a1 * 0 -> a1 * 0 + -(a1 * 0) = [a1 * 0 + a1 * 0] + -(a1 * 0)) & P16 & P0) & ( a1 * 0 = a1 * 0 + a1 * 0 & P11 & P9 & P5 & P0) & P0 -> ( a1 * 0 = 0 & P14 & P3 & P0) & P0" 2;
pushreference 8 "P0 -> ((a1 * 0 = a1 * 0 + a1 * 0 -> a1 * 0 + -(a1 * 0) = [a1 * 0 + a1 * 0] + -(a1 * 0)) & P15 & P0) & P0" "aeq";
pushnode 7 "(a1 * 0 = a1 * 0 + a1 * 0 & P11 & P9 & P5 & P0) & P0 -> (a1 * 0 = 0 & P14 & P3 & P0) & P0" 2;
pushnode 6 "(0 + 0 = 0 & P9 & P0) & (a1 * [0 + 0] = a1 * 0 + a1 * 0 & P5 & P0) & (Real(0) & P2 & P0) & P0 -> (a1 * 0 = 0 & P3 & P0) & P0" 1;
pushnode 5 "(Real(0) & P2 & P0) & ( a1 * [0 + 0] = a1 * 0 + a1 * 0 & P5 & P0) & P0 -> (Real(0) & P8 & P0) &  (a1 * 0 = 0 & P3 & P0) & P0" 0;
pushreference 4 "(Real(0) & P6 & P0) & P0 -> (0 + 0 = 0 & P7 & P0) & P0" "aid";
pushnode 3 "( a1 * [0 + 0] = a1 * 0 + a1 * 0 & P5 & P0) & (Real(0) & P2 & P0) & P0 ->  (a1 * 0 = 0 & P3 & P0) & P0" 3;
pushreference 2 "P0 -> (a1 * [0 + 0] = a1 * 0 + a1 * 0 & P4 & P0) & P0" "dist";
pushnode 1 "(Real(0) & P2 & P0) & P0 -> (a1 * 0 = 0 & P3 & P0) & P0" 2;
THEOREMS:=("thm 3.1.ii",(termtosequent(parseprop("(Real(0) & P2 & P0) & P0 -> (a1 * 0 = 0 & P3 & P0) & P0")),hd(!PROOFSTACK)))::(!THEOREMS);
PROOFSTACK:=nil;
td "thm 3.1.ii";
pushnode 54 "( -(a1) * a2 = -(a1 * a2) & P109 & P105 & P100 & P98 & P95 & P93 & P90 & P86 & P80 & P77 & P75 & P70 & P68 & P45 & P71 & P61 & P41 & P37 & P0) & P0 -> (-(a1) * a2 = -(a1 * a2) & P110 & P101 & P96 & P91 & P82 & P78 & P73 & P43 & P35 & P25 & P19 & P15 & P1 & P0) & P0" 0;
pushnode 51 " (-(a1) * a2 + 0 = -(a1) * a2 & P105 & P0) & (-(a1) * a2 + 0 = -(a1 * a2) & P100 & P98 & P95 & P93 & P90 & P86 & P80 & P77 &  P75 & P70 & P68 & P45 & P71 & P61 & P41 & P37 & P0) & P0 ->  (-(a1) * a2 = -(a1 * a2) & P101 & P96 & P91 & P82 & P78 & P73 & P43 & P35 & P25 & P19 & P15 & P1 & P0) & P0" 1;
pushnode 53 "(Real(-(a1) * a2) & P107 & P0) & (-(a1) * a2 + 0 = -(a1 * a2) & P100 & P98 & P95 & P93 & P90 & P86 & P80 & P77 & P75 & P70 & P68 & P45 & P71 & P61 & P41 & P37 & P0) & P0 -> (Real(-(a1) * a2) & P104 & P0) & (-(a1) * a2 = -(a1 * a2) & P101 & P96 & P91 & P82 & P78 & P73 & P43 & P35 & P25 & P19 & P15 & P1 & P0) & P0" 0;
pushreference 52 "P0 -> (Real(-(a1) * a2) & P106 & P0) & P0" "rtimes";
pushnode 50 " (-(a1) * a2 + 0 = -(a1 * a2) & P100 & P98 & P95 & P93 & P90 & P86 & P80 & P77 & P75 & P70 & P68 & P45 & P71 & P61 & P41 & P37 & P0) & P0 -> (Real(-(a1) * a2) & P104 & P0) & (-(a1) * a2 = -(a1 * a2) & P101 & P96 & P91 & P82 & P78 & P73 & P43 & P35 & P25 & P19 & P15 & P1 & P0) & P0" 2;
pushreference 49 "(Real(-(a1) * a2) & P102 & P0) & P0 -> (-(a1) * a2 + 0 = -(a1) * a2 & P103 & P0) & P0" "aid";
pushnode 48 "(-(a1) * a2 + 0 = -(a1 * a2) & P100 & P98 & P95 & P93 & P90 & P86 & P80 & P77 & P75 & P70 & P68 & P45 & P71 & P61 & P41 & P37 & P0) & P0 -> (-(a1) * a2 = -(a1 * a2) & P101 & P96 & P91 & P82 & P78 & P73 & P43 & P35 & P25 & P19 & P15 & P1 & P0) & P0" 3;
pushnode 47 "(0 + -(a1) * a2 = -(a1) * a2 + 0 & P98 & P0) & ( 0 + -(a1) * a2 = -(a1 * a2) & P95 & P93 & P90 & P86 & P80 & P77 & P75 & P70 & P68 & P45 & P71 & P61 & P41 & P37 & P0) & P0 -> ( -(a1) * a2 = -(a1 * a2) & P96 & P91 & P82 & P78 & P73 & P43 & P35 & P25 & P19 & P15 & P1 & P0) & P0" 1;
pushreference 46 " P0 -> (0 + -(a1) * a2 = -(a1) * a2 + 0 & P97 & P0) & P0" "acom";
pushnode 45 "(0 + -(a1) * a2 = -(a1 * a2) & P95 & P93 & P90 & P86 & P80 & P77 & P75 & P70 & P68 & P45 & P71 &  P61 & P41 & P37 & P0) & P0 ->  (-(a1) * a2 = -(a1 * a2) & P96 & P91 & P82 & P78 & P73 & P43 & P35 & P25 & P19 & P15 & P1 & P0) & P0" 2;
pushnode 44 "(a1 * a2 + -(a1 * a2) = 0 & P93 & P0) & ( [a1 * a2 + -(a1 * a2)] + -(a1) * a2 = -(a1 * a2) & P90 & P86 & P80 & P77 & P75 & P70 & P68 & P45 & P71 & P61 & P41 & P37 & P0) & P0 -> (-(a1) * a2 = -(a1 * a2) & P91 & P82 & P78 & P73 & P43 & P35 & P25 & P19 & P15 & P1 & P0) & P0" 1;
pushreference 43 "P0 -> ( a1 * a2 + -(a1 * a2) = 0 & P92 & P0) & P0" "ainv";
pushnode 42 "( [a1 * a2 + -(a1 * a2)] + -(a1) * a2 = -(a1 * a2) & P90 & P86 & P80 & P77 & P75 & P70 & P68 & P45 & P71 & P61 & P41 & P37 & P0) & P0 -> (-(a1) * a2 = -(a1 * a2) & P91 & P82 & P78 & P73 & P43 & P35 & P25 & P19 & P15 & P1 & P0) & P0" 2;
pushnode 39 "(-(a1 * a2) + 0 = -(a1 * a2) & P86 & P0) & ([a1 * a2 + -(a1 * a2)] + -(a1) * a2 = -(a1 * a2) + 0 & P80 & P77 & P75 & P70 & P68 & P45 & P71 & P61 & P41 &  P37 & P0) & P0 -> (-(a1) * a2 = -(a1 * a2) & P82 & P78 & P73 & P43 & P35 & P25 & P19 & P15 & P1 & P0) & P0" 1;
pushnode 41 " (Real(-(a1 * a2)) & P88 & P0) &  ([a1 * a2 + -(a1 * a2)] + -(a1) * a2 = -(a1 * a2) + 0 & P80 & P77 & P75 & P70 & P68 & P45 & P71 & P61 & P41 & P37 & P0) & P0 -> (Real(-(a1 * a2)) & P85 & P0) & (-(a1) * a2 = -(a1 * a2) & P82 & P78 & P73 & P43 & P35 & P25 & P19 & P15 & P1 & P0) & P0" 0;
pushreference 40 "P0 -> (Real(-(a1 * a2)) & P87 & P0) & P0" "rminus";
pushnode 38 "( [a1 * a2 + -(a1 * a2)] + -(a1) * a2 = -(a1 * a2) + 0 & P80 & P77 & P75 & P70 & P68 & P45 & P71 & P61 & P41 & P37 & P0) & P0 -> (Real(-( a1 * a2)) & P85 & P0) & (-(a1) * a2 = -(a1 * a2) & P82 & P78 & P73 & P43 & P35 & P25 & P19 & P15 & P1 & P0) & P0" 2;
pushreference 37 "(Real(-( a1 * a2)) & P83 & P0) & P0 -> (-(a1 * a2) + 0 = -(a1 * a2) & P84 & P0) & P0" "aid";
pushnode 36 "([a1 * a2 + -(a1 * a2)] + -(a1) * a2 = -(a1 * a2) + 0 & P80 & P77 & P75 & P70 & P68 & P45 & P71 & P61 & P41 & P37 & P0) & P0 -> ( -(a1) * a2 = -(a1 * a2) & P82 & P78 & P73 & P43 & P35 & P25 & P19 & P15 & P1 & P0) & P0" 3;
pushnode 35 "(-(a1 * a2) + a1 * a2 = a1 * a2 + -(a1 * a2) & P77 & P70 & P45 & P0) & ([-(a1 * a2) + a1 * a2] + -(a1) * a2 = -(a1 * a2) + 0 & P75 &  P68 & P71 & P61 & P41 & P37 & P0) & P0 -> ( -(a1) * a2 = -(a1 * a2) & P78 & P73 & P43 & P35 & P25 & P19 & P15 & P1 & P0) & P0" 1;
pushnode 34 " (-(a1 * a2) + a1 * a2 + -(a1) * a2 =  [-(a1 * a2) + a1 * a2] + -(a1) * a2 & P68 & P61 & P0) & ( -(a1 * a2) + a1 * a2 + -(a1) * a2 = -(a1 * a2) + 0 & P71 & P41 & P37 & P0) & ( -(a1 * a2) + a1 * a2 = a1 * a2 + -(a1 * a2) & P70 & P45 & P0) & P0 -> (-(a1) * a2 = -(a1 * a2) & P73 & P43 & P35 & P25 & P19 & P15 & P1 & P0) & P0" 1;
pushnode 33 "([-(a1 * a2) + a1 * a2] + -(a1) * a2 = -(a1 * a2) + a1 * a2 + -(a1) * a2 & P62 & P59 & P0) & P0 -> ([-(a1 * a2) + a1 * a2] + -(a1) * a2 = -(a1 * a2) +  a1 * a2 + -(a1) * a2 & P66 & P61 & P0) & P0" 0;
pushnode 32 "(([-(a1 * a2) + a1 * a2] + -(a1) * a2 = -( a1 * a2) + a1 * a2 + -(a1) * a2 -> -(a1 * a2) + a1 * a2 + -(a1) * a2 = [-(a1 * a2) + a1 * a2] + -(a1) * a2) & P61 & P0) & ([-(a1 * a2) + a1 * a2] + -(a1) * a2 = -(a1 * a2) + a1 * a2 + -(a1) * a2 & P59 & P0) & ( -(a1 * a2) + a1 * a2 = a1 * a2 + -(a1 * a2) & P45 & P0) & ( -(a1 * a2) + a1 * a2 + -(a1) * a2 = -(a1 * a2) + 0 & P41 & P37 & P0) & P0 -> (-(a1) * a2 = -(a1 * a2) & P43 & P35 & P25 & P19 & P15 & P1 & P0) & P0" 2;
pushreference 31 "P0 -> ( ([-(a1 * a2) + a1 * a2] + -(a1) * a2 = -(a1 * a2) + a1 * a2 + -(a1) * a2 -> -(a1 * a2) + a1 * a2 + -(a1) * a2 = [-(a1 * a2) + a1 * a2] + -(a1) * a2) & P60 & P0) & P0" "symm";
pushnode 30 " ([-( a1 * a2) + a1 * a2] + -(a1) * a2 = -(a1 * a2) + a1 * a2 + -(a1) * a2 & P59 & P0) & (-( a1 * a2) + a1 * a2 = a1 * a2 + -(a1 * a2) & P45 & P0) & ( -(a1 * a2) + a1 * a2 + -(a1) * a2 = -(a1 * a2) + 0 & P41 & P37 & P0) & P0 ->  (-(a1) * a2 = -(a1 * a2) & P43 & P35 & P25 & P19 & P15 & P1 & P0) & P0" 2;
pushreference 29 "P0 -> ([-(a1 * a2) + a1 * a2] + -(a1) * a2 = -(a1 * a2) + a1 * a2 + -(a1) * a2 & P58 & P0) & P0" "aas";
pushnode 25 " (-(a1 * a2) + a1 * a2 = a1 * a2 + -(a1 * a2) & P45 & P0) &  (-(a1 * a2) + a1 * a2 + -(a1) * a2 = -(a1 * a2) + 0 & P41 & P37 & P0) & P0 -> (-(a1) * a2 = -(a1 * a2) & P43 & P35 & P25 & P19 & P15 & P1 & P0) & P0" 2;
pushreference 24 "P0 ->  (-(a1 * a2) + a1 * a2 = a1 * a2 + -(a1 * a2) & P44 & P0) & P0" "acom";
pushnode 23 "(-(a1 * a2) + a1 * a2 + -(a1) * a2 = -(a1 * a2) + 0 & P41 & P37 & P0) & P0 ->  (-(a1) * a2 = -(a1 * a2) & P43 & P35 & P25 & P19 & P15 & P1 & P0) & P0" 2;
pushnode 22 " (a1 * a2 + -(a1) * a2 = 0 & P38 & P33 & P29 & P23 & P21 & P17 & P13 & P12 & P5 & P7 & P0) & P0 -> (a1 * a2 + -(a1) * a2 = 0 & P39 & P37 & P0) & P0" 0;
pushnode 21 "((a1 * a2 + -(a1) * a2 = 0 -> -( a1 * a2) + a1 * a2 + -(a1) * a2 = -(a1 * a2) + 0) & P37 & P0) & (a1 * a2 + -(a1) * a2 = 0 & P33 & P29 & P23 & P21 & P17 & P13 & P12 & P5 & P7 & P0) & P0 -> ( -(a1) * a2 = -(a1 * a2) & P35 & P25 & P19 & P15 & P1 & P0) & P0" 2;
pushreference 20 " P0 -> ((a1 * a2 + -(a1) * a2 = 0 -> -(a1 * a2) + a1 * a2 + -(a1) * a2 = -(a1 * a2) + 0) &  P36 & P0) & P0" "aeql";
pushnode 19 "(a1 * a2 + -(a1) * a2 = 0 & P33 & P29 & P23 & P21 & P17 & P13 & P12 & P5 & P7 & P0) & P0 -> ( -(a1) * a2 = -(a1 * a2) & P35 & P25 & P19 & P15 & P1 & P0) & P0" 2;
pushnode 16 "( a2 * 0 = 0 & P29 & P0) & (a1 * a2 + -(a1) * a2 = a2 * 0 & P23 & P21 & P17 & P13 & P12 & P5 & P7 & P0) & P0 -> (-(a1) * a2 = -(a1 * a2) & P25 & P19 & P15 & P1 & P0) & P0" 1;
pushnode 18 "(Real(0) & P31 & P0) & (a1 * a2 + -(a1) * a2 = a2 * 0 & P23 & P21 & P17 & P13 & P12 & P5 & P7 & P0) & P0 -> (Real(0) & P28 & P0) & (-(a1) * a2 = -(a1 * a2) & P25 & P19 & P15 & P1 & P0) & P0" 0;
pushreference 17 "P0 -> (Real(0) & P30 & P0) & P0" "zero";
pushnode 15 "(a1 * a2 + -(a1) * a2 = a2 * 0 & P23 & P21 & P17 & P13 & P12 & P5 & P7 & P0) & P0 -> (Real(0) & P28 & P0) & (-(a1) * a2 = -(a1 * a2) & P25 & P19 & P15 & P1 & P0) & P0" 2;
pushreference 14 "(Real(0) & P26 & P0) & P0 -> (a2 * 0 = 0 & P27 & P0) & P0" "thm 3.1.ii";
pushnode 13 "(a1 * a2 + -(a1) * a2 = a2 * 0 & P23 & P21 & P17 & P13 & P12 & P5 & P7 & P0) & P0 ->  (-(a1) * a2 = -(a1 * a2) & P25 & P19 & P15 & P1 & P0) & P0" 3;
pushnode 12 "(0 * a2 = a2 * 0 & P21 & P0) & (a1 * a2 + -(a1) * a2 = 0 * a2 & P17 & P13 & P12 & P5 & P7 & P0) & P0 ->  (-(a1) * a2 = -(a1 * a2) & P19 & P15 & P1 & P0) & P0" 1;
pushreference 11 "P0 -> (0 * a2 = a2 * 0 & P20 & P0) & P0" "mcom";
pushnode 10 "( a1 * a2 + -(a1) * a2 = 0 * a2 & P17 & P13 & P12 & P5 & P7 & P0) & P0 -> ( -(a1) * a2 = -(a1 * a2) & P19 & P15 & P1 & P0) & P0" 2;
pushnode 9 "( [a1 + -(a1)] * a2 = a1 * a2 + -(a1) * a2 & P13 & P5 & P0) & ([a1 + -(a1)] * a2 = 0 * a2 & P12 & P7 & P0) & P0 -> (-(a1) * a2 = -(a1 * a2) & P15 & P1 & P0) & P0" 1;
pushnode 8 "( a1 + -(a1) = 0 & P9 & P3 & P0) & P0 -> (a1 + -(a1) = 0 & P10 & P7 & P0) & P0" 0;
pushnode 7 "((a1 + -(a1) = 0 -> [a1 + -(a1)] * a2 = 0 * a2) & P7 & P0) &  ([a1 + -(a1)] * a2 = a1 * a2 + -(a1) * a2 & P5 & P0) & (a1 + -(a1) = 0 & P3 & P0) & P0 -> ( -(a1) * a2 = -(a1 * a2) & P1 & P0) & P0" 2;
pushreference 6 "P0 -> ((a1 + -(a1) = 0 -> [a1 + -(a1)] * a2 = 0 * a2) & P6 & P0) & P0" "meq";
pushnode 5 "([a1 + -(a1)] * a2 = a1 * a2 + -(a1) * a2 & P5 & P0) & (a1 + -(a1) = 0 & P3 & P0) & P0 -> (-(a1) * a2 = -(a1 * a2) & P1 & P0) & P0" 2;
pushreference 4 "P0 ->  ([a1 + -(a1)] * a2 = a1 * a2 + -(a1) * a2 & P4 & P0) & P0" "distr";
pushnode 3 "(a1 + -(a1) = 0 & P3 & P0) & P0 ->  (-(a1) * a2 = -(a1 * a2) & P1 & P0) & P0" 2;
pushreference 2 "P0 -> (a1 + -(a1) = 0 & P2 & P0) & P0" "ainv";
pushnode 1 "P0 -> (-(a1) * a2 = -(a1 * a2) & P1 & P0) & P0" 2;
THEOREMS:=("thm 3.1.iii",(termtosequent(parseprop("P0 -> (-(a1) * a2 = -(a1 * a2) & P1 & P0) & P0")),hd(!PROOFSTACK)))::(!THEOREMS);
PROOFSTACK:=nil;
td "thm 3.1.iii";
pushnode 50 "(-(a1) * -(a2) = a1 * a2 & P125 & P121 & P114 & P112 & P107 & P103 & P96 & P92 & P89 & P82 & P81 & P57 & P84 & P66 & P52 & P50 & P44 & P38 & P0) & P0 -> (-(a1) * -(a2) = a1 * a2 & P128 & P117 & P110 & P99 & P94 & P87 & P55 & P48 & P36 & P29 & P17 & P3 & P0) & P0" 0;
pushnode 47 "(-(a1) * -(a2) + 0 = -(a1) * -(a2) & P121 & P0) & (-(a1) * -(a2) + 0 = a1 * a2 & P114 & P112 & P107 & P103 & P96 & P92 & P89 & P82 & P81 & P57 & P84 & P66 & P52 & P50 & P44 & P38 & P0) & P0 ->  (-(a1) * -(a2) = a1 * a2 & P117 & P110 & P99 & P94 & P87 & P55 & P48 & P36 & P29 & P17 & P3 & P0) & P0" 1;
pushnode 49 "(Real(-(a1) * -(a2)) & P123 & P0) & (-(a1) * -(a2) + 0 = a1 * a2 & P114 & P112 & P107 & P103 & P96 & P92 & P89 & P82 & P81 & P57 & P84 & P66 & P52 & P50 & P44 & P38 & P0) & P0 -> (Real(-(a1) * -(a2)) & P120 & P0) &  (-(a1) * -(a2) = a1 * a2 & P117 & P110 & P99 & P94 & P87 & P55 & P48 & P36 & P29 & P17 & P3 & P0) & P0" 0;
pushreference 48 "P0 -> (Real(-(a1) * -(a2)) & P122 & P0) & P0" "rtimes";
pushnode 46 " (-(a1) * -(a2) + 0 = a1 * a2 &  P114 & P112 & P107 & P103 & P96 & P92 & P89 & P82 & P81 & P57 & P84 & P66 & P52 & P50 & P44 & P38 & P0) & P0 -> (Real(-(a1) * -(a2)) & P120 & P0) &  (-(a1) * -(a2) = a1 * a2 & P117 & P110 & P99 & P94 & P87 & P55 & P48 & P36 & P29 & P17 & P3 & P0) & P0" 2;
pushreference 45 "(Real(-(a1) * -(a2)) & P118 & P0) & P0 -> ( -(a1) * -(a2) + 0 = -(a1) * -(a2) & P119 & P0) & P0" "aid";
pushnode 44 "(-(a1) * -(a2) + 0 = a1 * a2 & P114 & P112 & P107 & P103 & P96 & P92 & P89 & P82 & P81 & P57 & P84 & P66 & P52 & P50 & P44 & P38 & P0) & P0 ->  (-(a1) * -(a2) = a1 * a2 & P117 & P110 & P99 & P94 & P87 & P55 & P48 & P36 & P29 & P17 & P3 & P0) & P0" 3;
pushnode 43 "(0 + -(a1) * -(a2) = -(a1) * -(a2) + 0 & P112 & P0) & (0 + -(a1) * -(a2) = a1 * a2 & P107 & P103 & P96 & P92 & P89 & P82 & P81 & P57 & P84 & P66 & P52 & P50 & P44 & P38 & P0) & P0 -> ( -(a1) * -(a2) = a1 * a2 & P110 & P99 & P94 & P87 & P55 & P48 & P36 & P29 & P17 & P3 & P0) & P0" 1;
pushreference 42 "P0 -> (0 +  -(a1) * -(a2) = -(a1) * -(a2) + 0 & P111 & P0) & P0" "acom";
pushnode 41 "( 0 + -(a1) * -(a2) = a1 * a2 & P107 & P103 & P96 & P92 & P89 & P82 & P81 & P57 & P84 & P66 & P52 & P50 & P44 & P38 & P0) & P0 -> (-(a1) * -(a2) = a1 * a2 & P110 & P99 & P94 & P87 &  P55 & P48 & P36 & P29 & P17 & P3 & P0) & P0" 2;
pushnode 38 "(a1 * a2 + 0 = a1 * a2 & P103 & P0) & ( 0 + -(a1) * -(a2) = a1 * a2 + 0 & P96 & P92 & P89 & P82 & P81 & P57 & P84 & P66 & P52 & P50 & P44 & P38 & P0) & P0 -> (-(a1) * -(a2) = a1 * a2 & P99 & P94 & P87 & P55 & P48 & P36 & P29 & P17 & P3 & P0) & P0" 1;
pushnode 40 " (Real(a1 * a2) & P105 & P0) & (0 + -(a1) * -(a2) = a1 * a2 + 0 & P96 & P92 & P89 & P82 & P81 & P57 & P84 & P66 & P52 & P50 & P44 & P38 & P0) & P0 -> (Real(a1 * a2) & P102 & P0) & ( -(a1) * -(a2) = a1 * a2 & P99 & P94 & P87 & P55 & P48 & P36 & P29 & P17 & P3 & P0) & P0" 0;
pushreference 39 " P0 -> (Real(a1 * a2) & P104 & P0) & P0" "rtimes";
pushnode 37 "(0 + -(a1) * -(a2) = a1 * a2 + 0 & P96 & P92 & P89 & P82 & P81 & P57 & P84 & P66 & P52 & P50 & P44 & P38 & P0) & P0 -> (Real(a1 * a2) & P102 & P0) & (-(a1) * -(a2) = a1 * a2 & P99 & P94 & P87 & P55 & P48 & P36 & P29 & P17 & P3 & P0) & P0" 2;
pushreference 36 "(Real(a1 * a2) & P100 & P0) & P0 -> (a1 * a2 + 0 = a1 * a2 & P101 & P0) & P0" "aid";
pushnode 35 " (0 + -(a1) * -(a2) = a1 * a2 + 0 & P96 & P92 & P89 & P82 & P81 & P57 & P84 & P66 & P52 & P50 & P44 & P38 & P0) & P0 -> (-(a1) * -(a2) = a1 * a2 & P99 & P94 & P87 & P55 & P48 & P36 & P29 & P17 & P3 & P0) & P0" 3;
pushnode 34 "(a1 * a2 + -(a1 * a2) = 0 & P92 & P82 & P57 & P0) &  ([a1 * a2 + -(a1 * a2)] + -(a1) * -(a2) = a1 * a2 + 0 & P89 &  P81 & P84 & P66 & P52 & P50 & P44 & P38 & P0) & P0 -> (-(a1) * -(a2) = a1 * a2 & P94 & P87 & P55 & P48 & P36 & P29 & P17 & P3 & P0) & P0" 1;
pushnode 33 " (a1 * a2 + -(a1 * a2) + -(a1) * -(a2) = [a1 * a2 + -(a1 * a2)] + -(a1) * -(a2) & P81 & P66 & P0) & ( a1 * a2 + -(a1 * a2) + -(a1) * -(a2) = a1 * a2 + 0 & P84 & P52 & P50 & P44 & P38 & P0) & (a1 * a2 + -(a1 * a2) = 0 & P82 & P57 & P0) & P0 -> (-(a1) * -(a2) = a1 * a2 & P87 & P55 & P48 & P36 & P29 & P17 & P3 & P0) & P0" 1;
pushnode 32 "([a1 * a2 + -(a1 * a2)] + -(a1) * -(a2) = a1 * a2 +  -(a1 * a2) + -(a1) * -(a2) & P75 & P64 & P0) & P0 -> ( [a1 * a2 + -(a1 * a2)] + -(a1) * -(a2) = a1 * a2 + -(a1 * a2) + -(a1) * -(a2) & P79 & P66 & P0) & P0" 0;
pushnode 30 "( ([a1 * a2 + -(a1 * a2)] + -(a1) * -(a2) = a1 * a2 + -(a1 * a2) + -(a1) * -(a2) -> a1 * a2 +  -(a1 * a2) + -(a1) * -(a2) = [a1 * a2 + -(a1 * a2)] + -(a1) * -(a2)) & P66 & P0) & (a1 * a2 + -(a1 * a2) = 0 & P57 & P0) & ([ a1 * a2 + -(a1 * a2)] + -(a1) * -(a2) = a1 * a2 + -(a1 * a2) + -(a1) * -(a2) & P64 & P0) & ( a1 * a2 + -(a1 * a2) + -(a1) * -(a2) = a1 * a2 + 0 & P52 & P50 & P44 & P38 & P0) & P0 ->  (-(a1) * -(a2) = a1 * a2 & P55 & P48 & P36 & P29 & P17 & P3 & P0) & P0" 2;
pushreference 29 "P0 -> (([a1 * a2 + -(a1 * a2)] + -(a1) * -(a2) = a1 * a2 + -(a1 * a2) + -(a1) * -(a2) -> a1 * a2 + -(a1 * a2) + -(a1) * -(a2) = [a1 * a2 + -(a1 * a2)] + -(a1) * -(a2)) & P65 & P0) & P0" "symm";
pushnode 28 "( [a1 * a2 + -(a1 * a2)] + -(a1) * -(a2) = a1 * a2 + -(a1 * a2) + -(a1) * -(a2) & P64 & P0) &  (a1 * a2 + -(a1 * a2) = 0 & P57 & P0) &  (a1 * a2 + -(a1 * a2) + -(a1) * -(a2) = a1 * a2 + 0 & P52 & P50 & P44 & P38 & P0) & P0 -> ( -(a1) * -(a2) = a1 * a2 & P55 & P48 & P36 & P29 & P17 & P3 & P0) & P0" 2;
pushreference 27 "P0 -> ( [a1 * a2 + -(a1 * a2)] + -(a1) * -(a2) = a1 * a2 + -(a1 * a2) + -(a1) * -(a2) & P63 & P0) & P0" "aas";
pushnode 25 "( a1 * a2 + -(a1 * a2) = 0 & P57 & P0) & (a1 * a2 + -(a1 * a2) + -(a1) * -(a2) = a1 * a2 + 0 & P52 & P50 & P44 &  P38 & P0) & P0 -> (-(a1) * -(a2) = a1 * a2 & P55 & P48 & P36 & P29 & P17 & P3 & P0) & P0" 2;
pushreference 24 "P0 -> (a1 * a2 + -(a1 * a2) = 0 & P56 & P0) & P0" "ainv";
pushnode 23 "(a1 * a2 + -(a1 * a2) + -(a1) * -(a2) = a1 * a2 + 0 & P52 & P50 & P44 & P38 & P0) & P0 -> (-(a1) * -(a2) = a1 * a2 & P55 & P48 & P36 & P29 & P17 & P3 & P0) & P0" 2;
pushnode 22 " (-(a1) * a2 = -(a1 * a2) & P50 & P0) & (a1 * a2 + -(a1) * a2 + -(a1) * -(a2) = a1 * a2 + 0 & P44 & P38 & P0) & P0 -> (-(a1) * -(a2) = a1 * a2 & P48 & P36 & P29 & P17 & P3 & P0) & P0" 1;
pushreference 21 "P0 -> (-(a1) * a2 = -(a1 * a2) & P49 & P0) & P0" "thm 3.1.iii";
pushnode 20 "(a1 * a2 + -(a1) * a2 + -(a1) * -(a2) = a1 * a2 + 0 & P44 & P38 & P0) & P0 -> (-(a1) * -(a2) = a1 * a2 & P48 & P36 & P29 & P17 & P3 & P0) & P0" 2;
pushnode 19 "( -(a1) * a2 + -(a1) * -(a2) = 0 & P39 & P33 & P31 & P25 & P21 & P13 & P7 & P0) & P0 -> (-(a1) * a2 + -(a1) * -(a2) = 0 & P42 & P38 & P0) & P0" 0;
pushnode 18 "(( -(a1) * a2 + -(a1) * -(a2) = 0 -> a1 * a2 + -(a1) * a2 + -(a1) * -(a2) = a1 * a2 + 0) & P38 & P0) &  (-(a1) * a2 + -(a1) * -(a2) = 0 & P33 & P31 & P25 & P21 & P13 & P7 & P0) & P0 -> (-(a1) * -(a2) = a1 * a2 & P36 & P29 & P17 & P3 & P0) & P0" 2;
pushreference 17 "P0 -> ((-(a1) * a2 + -(a1) * -(a2) = 0 -> a1 * a2 + -(a1) * a2 + -(a1) * -(a2) = a1 * a2 + 0) & P37 & P0) & P0" "aeql";
pushnode 16 "(-(a1) * a2 + -(a1) * -(a2) = 0 & P33 & P31 & P25 & P21 & P13 & P7 & P0) & P0 -> (-(a1) * -(a2) = a1 * a2 & P36 & P29 & P17 & P3 & P0) & P0" 2;
pushnode 15 "(-(a1) * [a2 + -(a2)] = -(a1) * a2 + -(a1) * -(a2) & P31 & P0) & (-(a1) * [a2 + -(a2)] = 0 & P25 & P21 & P13 & P7 & P0) & P0 ->  (-(a1) * -(a2) = a1 * a2 & P29 & P17 & P3 & P0) & P0" 1;
pushreference 14 "P0 ->  (-(a1) * [a2 + -(a2)] = -(a1) * a2 + -(a1) * -(a2) & P30 & P0) & P0" "dist";
pushnode 13 " (-(a1) * [a2 + -(a2)] = 0 & P25 & P21 & P13 & P7 & P0) & P0 -> (-(a1) * -(a2) = a1 * a2 & P29 & P17 & P3 & P0) & P0" 2;
pushnode 10 "(-(a1) * 0 = 0 & P21 & P0) & (-(a1) * [a2 + -(a2)] = -(a1) * 0 & P13 & P7 & P0) & P0 -> (-(a1) * -(a2) = a1 * a2 & P17 & P3 & P0) & P0" 1;
pushnode 12 "(Real(0) & P23 & P0) & (-(a1) * [a2 + -(a2)] = -(a1) * 0 & P13 & P7 & P0) & P0 -> (Real(0) & P20 & P0) & (-(a1) * -(a2) = a1 * a2 & P17 & P3 & P0) & P0" 0;
pushreference 11 "P0 -> (Real(0) & P22 & P0) & P0" "zero";
pushnode 9 " (-(a1) * [a2 + -(a2)] = -(a1) * 0 & P13 & P7 & P0) & P0 -> (Real(0) & P20 & P0) & (-(a1) * -(a2) = a1 * a2 & P17 & P3 & P0) & P0" 2;
pushreference 8 "(Real(0) & P18 & P0) & P0 -> (-(a1) * 0 = 0 & P19 & P0) & P0" "thm 3.1.ii";
pushnode 7 "(-(a1) * [a2 + -(a2)] = -(a1) * 0 & P13 & P7 & P0) & P0 ->  (-(a1) * -(a2) = a1 * a2 & P17 & P3 & P0) & P0" 3;
pushnode 6 "(a2 + -(a2) = 0 & P8 & P5 & P0) & P0 ->  (a2 + -(a2) = 0 & P11 & P7 & P0) & P0" 0;
pushnode 5 " ((a2 + -(a2) = 0 -> -(a1) * [a2 + -(a2)] = -(a1) * 0) & P7 & P0) & (a2 + -(a2) = 0 & P5 & P0) & P0 -> ( -(a1) * -(a2) = a1 * a2 & P3 & P0) & P0" 2;
pushreference 4 "P0 -> ((a2 + -(a2) = 0 -> -(a1) * [a2 + -(a2)] = -(a1) * 0) & P6 & P0) & P0" "meql";
pushnode 3 "(a2 + -(a2) = 0 & P5 & P0) & P0 -> (-(a1) * -(a2) = a1 * a2 & P3 & P0) & P0" 2;
pushreference 2 "P0 -> (a2 + -(a2) = 0 & P4 & P0) & P0" "ainv";
pushnode 1 "P0 -> (-(a1) * -(a2) = a1 * a2 & P3 & P0) & P0" 2;
THEOREMS:=("thm 3.1.iv",(termtosequent(parseprop("P0 -> (-(a1) * -(a2) = a1 * a2 & P3 & P0) & P0")),hd(!PROOFSTACK)))::(!THEOREMS);
PROOFSTACK:=nil;
td "thm 3.1.iv";
pushnode 36 "(a1 = a2 & P116 & P114 & P105 & P103 & P94 & P92 & P85 & P83 & P76 & P68 & P69 & P60 & P53 & P51 & P44 & P42 & P35 & P33 & P26 & P24 & P16 & P8 & P0) & P0 -> (a1 = a2 & P121 & P110 & P99 & P90 & P81 & P74 & P58 & P49 & P40 & P31 & P22 & P6 & P0) & P0" 0;
pushnode 35 "(a2 * 1 = a2 & P114 & P0) & ( a1 = a2 * 1 & P105 & P103 & P94 & P92 & P85 & P83 & P76 & P68 & P69 & P60 & P53 & P51 & P44 & P42 & P35 & P33 & P26 & P24 & P16 & P8 & P0) & (Real(a2) & P107 & P96 & P87 & P78 & P71 & P55 & P46 & P37 & P28 & P18 & P2 & P0) & P0 -> (a1 = a2 & P110 & P99 & P90 & P81 & P74 & P58 & P49 & P40 & P31 & P22 & P6 & P0) & P0" 1;
pushnode 34 " (Real(a2) & P107 & P96 & P87 & P78 & P71 & P55 & P46 & P37 & P28 & P18 & P2 & P0) & ( a1 = a2 * 1 & P105 & P103 & P94 & P92 & P85 & P83 & P76 & P68 & P69 & P60 & P53 & P51 & P44 & P42 & P35 & P33 & P26 & P24 & P16 & P8 & P0) & P0 -> (Real(a2) & P113 & P0) &  (a1 = a2 & P110 & P99 & P90 & P81 & P74 & P58 & P49 & P40 & P31 & P22 & P6 & P0) & P0" 0;
pushreference 33 "(Real(a2) & P111 & P0) & P0 -> (a2 * 1 = a2 & P112 & P0) & P0" "mid";
pushnode 32 "(a1 = a2 * 1 & P105 & P103 & P94 & P92 & P85 & P83 & P76 & P68 & P69 & P60 & P53 & P51 & P44 & P42 & P35 & P33 & P26 & P24 & P16 & P8 & P0) & (Real(a2) & P107 & P96 & P87 & P78 & P71 & P55 & P46 & P37 & P28 & P18 & P2 & P0) & P0 -> (a1 = a2 & P110 & P99 & P90 & P81 & P74 & P58 & P49 & P40 & P31 & P22 & P6 & P0) & P0" 3;
pushnode 31 "(a1 * 1 = a1 & P103 & P0) &  (a1 * 1 = a2 * 1 & P94 & P92 & P85 & P83 & P76 & P68 & P69 & P60 & P53 & P51 & P44 & P42 & P35 & P33 & P26 & P24 & P16 & P8 & P0) & (Real(a1) & P95 & P86 & P77 & P70 & P54 & P45 & P36 & P27 & P17 & P1 & P0) & (Real(a2) & P96 & P87 & P78 & P71 & P55 & P46 & P37 & P28 & P18 & P2 & P0) & P0 -> (a1 = a2 & P99 & P90 & P81 & P74 & P58 & P49 & P40 & P31 & P22 & P6 & P0) & P0" 1;
pushnode 30 "(Real(a1) & P95 & P86 & P77 & P70 & P54 & P45 & P36 & P27 & P17 & P1 & P0) & (Real(a2) & P96 & P87 & P78 & P71 & P55 & P46 & P37 & P28 & P18 & P2 & P0) & (a1 * 1 = a2 * 1 & P94 & P92 & P85 & P83 & P76 & P68 & P69 & P60 & P53 &  P51 & P44 & P42 & P35 & P33 & P26 & P24 & P16 & P8 & P0) & P0 -> (Real(a1) & P102 & P0) & (a1 = a2 & P99 & P90 & P81 & P74 & P58 & P49 & P40 & P31 & P22 & P6 & P0) & P0" 0;
pushreference 29 "(Real(a1) & P100 & P0) & P0 -> (a1 * 1 = a1 & P101 & P0) & P0" "mid";
pushnode 28 "(a1 * 1 = a2 * 1 & P94 & P92 & P85 & P83 & P76 & P68 & P69 & P60 & P53 & P51 &  P44 & P42 & P35 & P33 & P26 & P24 & P16 & P8 & P0) & (Real(a1) & P95 & P86 & P77 & P70 & P54 & P45 & P36 & P27 & P17 & P1 & P0) & (Real(a2) & P96 & P87 & P78 & P71 & P55 & P46 & P37 & P28 & P18 & P2 & P0) & P0 -> ( a1 = a2 & P99 & P90 & P81 & P74 & P58 & P49 & P40 & P31 & P22 & P6 & P0) & P0" 3;
pushnode 27 "(1 * a2 = a2 * 1 & P92 & P0) & (a1 * 1 = 1 * a2 & P85 & P83 & P76 & P68 & P69 & P60 & P53 & P51 & P44 & P42 & P35 & P33 & P26 & P24 & P16 & P8 & P0) & (Real(a1) & P86 & P77 & P70 & P54 & P45 & P36 & P27 & P17 & P1 & P0) & (Real(a2) & P87 & P78 & P71 & P55 & P46 & P37 & P28 & P18 & P2 & P0) & P0 -> (a1 = a2 & P90 & P81 & P74 & P58 & P49 & P40 & P31 & P22 & P6 & P0) & P0" 1;
pushreference 26 "P0 -> ( 1 * a2 = a2 * 1 & P91 & P0) & P0" "mcom";
pushnode 25 "(a1 * 1 = 1 * a2 & P85 & P83 & P76 & P68 & P69 & P60 & P53 & P51 & P44 & P42 & P35 & P33 & P26 & P24 & P16 & P8 & P0) & (Real(a1) & P86 & P77 & P70 & P54 & P45 & P36 & P27 & P17 & P1 & P0) & (Real(a2) & P87 & P78 & P71 & P55 & P46 & P37 & P28 & P18 & P2 & P0) & P0 -> (a1 = a2 & P90 & P81 & P74 & P58 & P49 & P40 & P31 & P22 & P6 & P0) & P0" 2;
pushnode 24 " (1 * a1 = a1 * 1 & P83 & P0) & (1 * a1 = 1 * a2 & P76 & P68 & P69 & P60 & P53 & P51 & P44 & P42 & P35 & P33 & P26 & P24 & P16 & P8 & P0) & (Real(a1) & P77 & P70 & P54 & P45 & P36 & P27 & P17 & P1 & P0) & (Real(a2) & P78 & P71 & P55 & P46 & P37 & P28 & P18 & P2 & P0) & P0 -> (a1 = a2 & P81 & P74 & P58 & P49 & P40 & P31 & P22 & P6 & P0) & P0" 1;
pushreference 23 "P0 -> (1 * a1 = a1 * 1 & P82 & P0) & P0" "mcom";
pushnode 22 " (1 * a1 = 1 * a2 & P76 & P68 & P69 & P60 & P53 & P51 & P44 & P42 & P35 & P33 & P26 & P24 & P16 & P8 & P0) & (Real(a1) & P77 & P70 & P54 & P45 & P36 & P27 & P17 & P1 & P0) & (Real(a2) & P78 & P71 & P55 & P46 & P37 & P28 & P18 & P2 & P0) & P0 -> (a1 = a2 & P81 & P74 & P58 & P49 & P40 & P31 & P22 & P6 & P0) & P0" 2;
pushnode 21 "(a3 * /(a3) = 1 & P68 & P60 & P0) & ( [a3 * /(a3)] * a1 = [a3 * /(a3)] * a2 & P69 & P53 & P51 & P44 & P42 & P35 & P33 & P26 & P24 & P16 & P8 & P0) & ( Real(a1) & P70 & P54 & P45 & P36 & P27 & P17 & P1 & P0) & ( Real(a2) & P71 & P55 & P46 & P37 & P28 & P18 & P2 & P0) & P0 -> (a1 = a2 & P74 & P58 & P49 & P40 & P31 & P22 & P6 & P0) & P0" 1;
pushnode 20 "(~a3 eq 0 & P65 & P57 & P48 & P39 & P30 & P21 & P5 & P0) & P0 -> (~a3 eq 0 & P66 & P60 & P0) & P0" 0;
pushnode 19 "((~a3 eq 0 -> a3 * /(a3) = 1) & P60 & P0) & ([a3 * /(a3)] * a1 = [a3 * /(a3)] * a2 & P53 & P51 & P44 & P42 & P35 & P33 & P26 & P24 & P16 & P8 & P0) & (Real(a1) & P54 & P45 & P36 & P27 & P17 & P1 & P0) & (Real(a2) & P55 & P46 & P37 & P28 & P18 & P2 & P0) &  (~a3 eq 0 & P57 & P48 & P39 & P30 & P21 & P5 & P0) & P0 ->  (a1 = a2 & P58 & P49 & P40 & P31 & P22 & P6 & P0) & P0" 2;
pushreference 18 "P0 -> ((~a3 eq 0 -> a3 * /(a3) = 1) & P59 & P0) & P0" "minv";
pushnode 17 "([ a3 * /(a3)] * a1 = [a3 * /(a3)] * a2 & P53 & P51 & P44 & P42 & P35 & P33 & P26 & P24 & P16 & P8 & P0) & (Real(a1) & P54 & P45 & P36 & P27 & P17 & P1 & P0) & (Real(a2) & P55 & P46 & P37 & P28 & P18 & P2 & P0) &  (~a3 eq 0 & P57 & P48 & P39 & P30 & P21 & P5 & P0) & P0 -> ( a1 = a2 & P58 & P49 & P40 & P31 & P22 & P6 & P0) & P0" 2;
pushnode 16 "( a2 * a3 * /(a3) = [a3 * /(a3)] * a2 & P51 & P0) & ([a3 * /(a3)] * a1 = a2 * a3 * /(a3) & P44 & P42 & P35 & P33 & P26 & P24 & P16 & P8 & P0) & (Real(a1) & P45 & P36 & P27 & P17 & P1 & P0) & (Real(a2) & P46 & P37 & P28 & P18 & P2 & P0) & (~a3 eq 0 & P48 & P39 & P30 & P21 & P5 & P0) & P0 -> (a1 = a2 & P49 & P40 & P31 & P22 & P6 & P0) & P0" 1;
pushreference 15 "P0 ->  (a2 * a3 * /(a3) = [a3 * /(a3)] * a2 & P50 & P0) & P0" "mcom";
pushnode 14 "([a3 * /(a3)] * a1 = a2 * a3 * /(a3) & P44 & P42 & P35 & P33 & P26 & P24 & P16 & P8 & P0) & (Real(a1) & P45 & P36 & P27 & P17 & P1 & P0) & (Real(a2) & P46 & P37 & P28 & P18 & P2 & P0) & (~a3 eq 0 & P48 & P39 & P30 &  P21 & P5 & P0) & P0 -> (a1 = a2 & P49 & P40 & P31 & P22 & P6 & P0) & P0" 2;
pushnode 13 "(a1 * a3 * /(a3) = [a3 * /(a3)] * a1 & P42 & P0) & (a1 *  a3 * /(a3) = a2 * a3 * /(a3) & P35 & P33 & P26 & P24 & P16 & P8 & P0) & ( Real(a1) & P36 & P27 & P17 & P1 & P0) & (Real(a2) & P37 & P28 & P18 & P2 & P0) & (~a3 eq 0 & P39 & P30 &  P21 & P5 & P0) & P0 -> (a1 = a2 & P40 & P31 & P22 & P6 & P0) & P0" 1;
pushreference 12 "P0 -> (a1 * a3 * /(a3) = [a3 * /(a3)] * a1 & P41 & P0) & P0" "mcom";
pushnode 11 "(a1 * a3 * /(a3) = a2 * a3 * /(a3) & P35 & P33 & P26 & P24 & P16 & P8 & P0) & (Real(a1) & P36 & P27 & P17 & P1 & P0) & (Real(a2) & P37 & P28 & P18 & P2 & P0) & (~a3 eq 0 & P39 & P30 & P21 & P5 & P0) & P0 -> (a1 = a2 & P40 & P31 & P22 & P6 & P0) & P0" 2;
pushnode 10 "([a2 * a3] * /(a3) = a2 * a3 * /(a3) & P33 & P0) & (a1 * a3 * /(a3) = [a2 * a3] * /(a3) & P26 & P24 & P16 & P8 & P0) & (Real(a1) & P27 & P17 & P1 & P0) & (Real(a2) & P28 & P18 & P2 & P0) & (~a3 eq 0 & P30 & P21 & P5 & P0) & P0 ->  (a1 = a2 & P31 & P22 & P6 & P0) & P0" 1;
pushreference 9 "P0 -> ([a2 * a3] * /(a3) = a2 * a3 * /(a3) & P32 & P0) & P0" "mas";
pushnode 8 "(a1 *  a3 * /(a3) = [a2 * a3] * /(a3) & P26 & P24 & P16 & P8 & P0) & (Real(a1) & P27 & P17 & P1 & P0) & (Real(a2) & P28 & P18 & P2 & P0) & (~a3 eq 0 & P30 & P21 & P5 & P0) & P0 -> (a1 = a2 & P31 & P22 & P6 & P0) & P0" 2;
pushnode 7 "([a1 * a3] * /(a3) = a1 * a3 * /(a3) & P24 & P0) & ([a1 * a3] * /(a3) = [a2 * a3] * /(a3) & P16 & P8 & P0) & (Real(a1) & P17 & P1 & P0) & (Real(a2) & P18 & P2 & P0) & (~a3 eq 0 & P21 & P5 & P0) & P0 -> (a1 = a2 & P22 & P6 & P0) & P0" 1;
pushreference 6 "P0 -> ([a1 * a3] * /(a3) = a1 * a3 * /(a3) & P23 & P0) & P0" "mas";
pushnode 5 "(~a3 eq 0 &  P21 & P5 & P0) & ([a1 * a3] * /(a3) = [a2 * a3] * /(a3) & P16 & P8 & P0) &  (Real(a1) & P17 & P1 & P0) & (Real(a2) & P18 & P2 & P0) & P0 -> ( a1 = a2 & P22 & P6 & P0) & P0" 2;
pushnode 4 "(a1 * a3 = a2 * a3 & P12 & P4 & P0) & P0 -> (a1 * a3 = a2 * a3 & P14 & P8 & P0) & P0" 0;
pushnode 3 " ((a1 * a3 = a2 * a3 -> [a1 * a3] * /(a3) = [a2 * a3] * /(a3)) & P8 & P0) & (Real(a1) & P1 & P0) & (Real(a2) & P2 & P0) & (a1 * a3 = a2 * a3 & P4 & P0) & (~a3 eq 0 & P5 & P0) & P0 -> (a1 = a2 & P6 & P0) & P0" 2;
pushreference 2 "P0 -> ((a1 * a3 = a2 * a3 -> [a1 * a3] * /(a3) = [a2 * a3] * /(a3)) & P7 & P0) & P0" "meq";
pushnode 1 "(Real(a1) & P1 & P0) & (Real(a2) & P2 & P0) &  (a1 * a3 = a2 * a3 & P4 & P0) & (~a3 eq 0 & P5 & P0) & P0 -> ( a1 = a2 & P6 & P0) & P0" 2;
THEOREMS:=("thm 3.1.v",(termtosequent(parseprop("(Real(a1) & P1 & P0) & (Real(a2) & P2 & P0) & (a1 * a3 = a2 * a3 & P4 & P0) & (~a3 eq 0 & P5 & P0) & P0 -> (a1 = a2 & P6 & P0) & P0")),hd(!PROOFSTACK)))::(!THEOREMS);
PROOFSTACK:=nil;
td "thm 3.1.v";
pushnode 33 "(a1 = 0 & P104 & P97 & P95 & P86 & P84 & P77 & P69 & P70 & P61 & P54 & P50 & P41 & P39 & P32 & P30 & P23 & P21 & P14 & P7 & P0) & P0 ->  (a1 = 0 & P109 & P102 & P91 & P82 & P75 & P59 & P46 & P37 & P28 & P19 & P5 & P0) & P0" 0;
pushnode 32 "(a1 = 0 & P97 & P95 & P86 & P84 & P77 & P69 & P70 & P61 & P54 & P50 & P41 & P39 & P32 & P30 & P23 & P21 & P14 & P7 & P0) & P0 -> ((a1 = 0 v a2 = 0) & P102 & P91 & P82 & P75 & P59 & P46 & P37 & P28 & P19 & P5 & P0) & P0" 1;
pushnode 31 " (a1 * 1 = a1 & P95 & P0) & (a1 * 1 = 0 & P86 & P84 & P77 & P69 & P70 & P61 & P54 & P50 & P41 & P39 & P32 & P30 & P23 & P21 & P14 & P7 & P0) & (Real(a1) & P89 & P80 & P73 & P57 & P44 & P35 & P26 &  P17 & P1 & P0) & P0 -> ((a1 = 0 v a2 = 0) & P91 & P82 & P75 & P59 & P46 & P37 & P28 & P19 & P5 & P0) & P0" 1;
pushnode 30 "(Real(a1) & P89 & P80 & P73 & P57 & P44 & P35 & P26 & P17 & P1 & P0) & (a1 * 1 = 0 & P86 & P84 & P77 & P69 & P70 & P61 & P54 & P50 & P41 & P39 & P32 & P30 & P23 & P21 & P14 & P7 & P0) & P0 -> (Real(a1) & P94 & P0) &  ((a1 = 0 v a2 = 0) & P91 & P82 & P75 & P59 &  P46 & P37 & P28 & P19 & P5 & P0) & P0" 0;
pushreference 29 "(Real(a1) & P92 & P0) & P0 -> (a1 * 1 = a1 & P93 & P0) & P0" "mid";
pushnode 28 "(a1 * 1 = 0 & P86 & P84 & P77 & P69 & P70 & P61 & P54 & P50 & P41 & P39 & P32 & P30 & P23 & P21 & P14 & P7 & P0) & (Real(a1) & P89 & P80 & P73 & P57 & P44 & P35 & P26 & P17 & P1 & P0) & P0 -> ((a1 = 0 v a2 = 0) & P91 & P82 & P75 & P59 & P46 & P37 & P28 & P19 & P5 & P0) & P0" 3;
pushnode 27 " (1 * a1 = a1 * 1 & P84 & P0) & (1 * a1 = 0 & P77 & P69 & P70 & P61 & P54 & P50 & P41 & P39 & P32 & P30 & P23 & P21 & P14 & P7 & P0) & (Real(a1) & P80 & P73 & P57 & P44 & P35 & P26 & P17 & P1 & P0) & P0 -> ((a1 = 0 v a2 = 0) & P82 & P75 & P59 & P46 & P37 & P28 & P19 & P5 & P0) & P0" 1;
pushreference 26 "P0 -> (1 * a1 = a1 * 1 & P83 & P0) & P0" "mcom";
pushnode 25 "(1 * a1 = 0 & P77 & P69 & P70 & P61 & P54 & P50 & P41 & P39 & P32 & P30 & P23 & P21 & P14 & P7 & P0) & (Real(a1) & P80 & P73 & P57 & P44 & P35 & P26 & P17 & P1 & P0) & P0 -> ((a1 = 0 v a2 = 0) & P82 & P75 & P59 & P46 & P37 & P28 & P19 & P5 & P0) & P0" 2;
pushnode 24 " (a2 * /(a2) = 1 & P69 & P61 & P0) & ( [a2 * /(a2)] * a1 = 0 & P70 & P54 & P50 & P41 & P39 & P32 & P30 & P23 & P21 & P14 & P7 & P0) & (Real(a1) & P73 & P57 &  P44 & P35 & P26 & P17 & P1 & P0) & P0 ->  ((a1 = 0 v a2 = 0) & P75 & P59 & P46 & P37 & P28 & P19 & P5 & P0) & P0" 1;
pushnode 23 "(~a2 eq 0 & P64 & P56 & P43 & P34 & P25 & P16 & P4 & P0) & P0 -> (~a2 eq 0 & P67 & P61 & P0) & P0" 0;
pushnode 22 " ((~a2 eq 0 -> a2 * /(a2) = 1) & P61 & P0) & ([a2 * /(a2)] * a1 = 0 & P54 & P50 & P41 & P39 & P32 & P30 & P23 & P21 & P14 & P7 & P0) & (~a2 eq 0 & P56 & P43 & P34 & P25 & P16 & P4 & P0) &  (Real(a1) & P57 & P44 & P35 & P26 & P17 & P1 & P0) & P0 ->  ((a1 = 0 v a2 = 0) & P59 & P46 & P37 & P28 & P19 & P5 & P0) & P0" 2;
pushreference 21 "P0 -> ((~a2 eq 0 -> a2 * /(a2) = 1) & P60 & P0) & P0" "minv";
pushnode 20 "([a2 * /(a2)] * a1 = 0 & P54 & P50 & P41 & P39 & P32 & P30 & P23 & P21 & P14 & P7 & P0) & (~a2 eq 0 & P56 & P43 & P34 & P25 & P16 & P4 & P0) & (Real(a1) & P57 & P44 & P35 & P26 & P17 & P1 & P0) & P0 -> ((a1 = 0 v a2 = 0) & P59 & P46 & P37 & P28 & P19 & P5 & P0) & P0" 2;
pushnode 17 "(/(a2) * 0 = 0 & P50 & P0) & ([a2 * /(a2)] * a1 = /(a2) * 0 & P41 & P39 & P32 & P30 & P23 & P21 & P14 & P7 & P0) & (~a2 eq 0 & P43 & P34 & P25 & P16 & P4 & P0) & (Real(a1) & P44 & P35 & P26 & P17 & P1 & P0) & P0 -> ((a1 = 0 v a2 = 0) & P46 & P37 & P28 & P19 & P5 & P0) & P0" 1;
pushnode 19 "(Real(0) & P52 & P0) & ([a2 * /(a2)] * a1 = /(a2) * 0 & P41 & P39 & P32 & P30 & P23 & P21 & P14 & P7 & P0) & (~a2 eq 0 & P43 & P34 & P25 & P16 & P4 & P0) & (Real(a1) & P44 & P35 & P26 & P17 & P1 & P0) & P0 -> (Real(0) & P49 & P0) & ( (a1 = 0 v a2 = 0) & P46 & P37 & P28 & P19 & P5 & P0) & P0" 0;
pushreference 18 "P0 -> (Real(0) & P51 & P0) & P0" "zero";
pushnode 16 "([a2 * /(a2)] * a1 = /(a2) * 0 & P41 & P39 & P32 & P30 & P23 & P21 & P14 & P7 & P0) & (~a2 eq 0 & P43 & P34 & P25 & P16 & P4 & P0) & (Real(a1) & P44 & P35 & P26 & P17 & P1 & P0) & P0 -> (Real(0) & P49 & P0) & ((a1 = 0 v a2 = 0) & P46 & P37 & P28 & P19 & P5 & P0) & P0" 2;
pushreference 15 "(Real(0) & P47 & P0) & P0 ->  (/(a2) * 0 = 0 & P48 & P0) & P0" "thm 3.1.ii";
pushnode 14 "([a2 * /(a2)] * a1 = /(a2) * 0 & P41 & P39 & P32 & P30 & P23 & P21 & P14 & P7 & P0) & (~a2 eq 0 & P43 & P34 & P25 & P16 & P4 & P0) & (Real(a1) & P44 & P35 & P26 & P17 & P1 & P0) & P0 -> ((a1 = 0 v a2 = 0) & P46 & P37 & P28 & P19 & P5 & P0) & P0" 3;
pushnode 13 "(a1 * a2 * /(a2) = [a2 * /(a2)] * a1 & P39 & P0) & (a1 * a2 * /(a2) = /(a2) * 0 & P32 & P30 & P23 & P21 & P14 & P7 & P0) & ( ~a2 eq 0 & P34 & P25 & P16 & P4 & P0) & (Real(a1) & P35 & P26 & P17 & P1 & P0) & P0 -> ((a1 = 0 v a2 = 0) & P37 & P28 & P19 & P5 & P0) & P0" 1;
pushreference 12 "P0 -> (a1 * a2 * /(a2) = [a2 * /(a2)] * a1 & P38 & P0) & P0" "mcom";
pushnode 11 " (a1 * a2 * /(a2) = /(a2) * 0 & P32 & P30 & P23 & P21 & P14 & P7 & P0) & (~a2 eq 0 & P34 & P25 & P16 & P4 & P0) & (Real(a1) & P35 & P26 & P17 & P1 & P0) & P0 -> ((a1 = 0 v a2 = 0) & P37 & P28 & P19 & P5 & P0) & P0" 2;
pushnode 10 "(0 * /(a2) = /(a2) * 0 & P30 & P0) & (a1 * a2 * /(a2) = 0 * /(a2) & P23 & P21 & P14 & P7 & P0) & (~a2 eq 0 & P25 & P16 & P4 & P0) & (Real(a1) & P26 & P17 & P1 & P0) & P0 ->  ((a1 = 0 v a2 = 0) & P28 & P19 & P5 & P0) & P0" 1;
pushreference 9 "P0 -> (0 * /(a2) = /(a2) * 0 & P29 & P0) & P0" "mcom";
pushnode 8 "( a1 * a2 * /(a2) = 0 * /(a2) & P23 & P21 & P14 & P7 & P0) & (~a2 eq 0 & P25 & P16 & P4 & P0) & (Real(a1) & P26 & P17 &  P1 & P0) & P0 -> ((a1 = 0 v a2 = 0) & P28 & P19 & P5 & P0) & P0" 2;
pushnode 7 "([a1 * a2] * /(a2) = a1 * a2 * /(a2) & P21 & P0) & ([a1 * a2] * /(a2) = 0 * /(a2) & P14 & P7 & P0) & (~a2 eq 0 & P16 & P4 & P0) & (Real(a1) & P17 & P1 & P0) & P0 -> ((a1 = 0 v a2 = 0) & P19 & P5 & P0) & P0" 1;
pushreference 6 "P0 -> ([a1 * a2] * /(a2) = a1 * a2 * /(a2) & P20 & P0) & P0" "mas";
pushnode 5 "( [a1 * a2] * /(a2) = 0 * /(a2) & P14 & P7 & P0) & (~a2 eq 0 & P16 & P4 & P0) & (Real(a1) & P17 & P1 & P0) & P0 -> ((a1 = 0 v a2 = 0) & P19 & P5 & P0) & P0" 2;
pushnode 4 "( a1 * a2 = 0 & P8 & P3 & P0) & P0 -> (a1 * a2 = 0 & P12 & P7 & P0) & P0" 0;
pushnode 3 "((a1 * a2 = 0 -> [a1 * a2] * /(a2) = 0 * /(a2)) & P7 & P0) & (a1 * a2 = 0 & P3 & P0) & (~a2 eq 0 & P4 & P0) & (Real(a1) & P1 & P0) & P0 -> ((a1 = 0 v a2 = 0) & P5 & P0) & P0" 2;
pushreference 2 "P0 -> (( a1 * a2 = 0 -> [a1 * a2] * /(a2) = 0 * /(a2)) & P6 & P0) & P0" "meq";
pushnode 1 "(Real(a1) & P1 & P0) & (a1 * a2 = 0 & P3 & P0) & (~a2 eq 0 & P4 & P0) & P0 -> ((a1 = 0 v a2 = 0) & P5 & P0) & P0" 2;
THEOREMS:=("thm 3.1.vi",(termtosequent(parseprop("(Real(a1) & P1 & P0) & (a1 * a2 = 0 & P3 & P0) & (~a2 eq 0 & P4 & P0) & P0 -> ((a1 = 0 v a2 = 0) & P5 & P0) & P0")),hd(!PROOFSTACK)))::(!THEOREMS);
PROOFSTACK:=nil;
td "thm 3.1.vi";
pushnode 36 " (-(a2) <= -(a1) & P95 & P93 & P82 & P80 & P73 & P71 & P64 & P60 & P51 & P49 & P42 & P40 & P33 & P26 & P0) & P0 -> (-(a2) <= -(a1) & P100 & P87 & P78 & P69 & P56 & P47 & P38 & P24 & P16 & P4 & P0) & P0" 0;
pushnode 35 "( -(a1) + 0 = -(a1) & P93 & P0) & (-(a2) <= -(a1) + 0 & P82 & P80 & P73 & P71 & P64 & P60 & P51 & P49 & P42 & P40 & P33 & P26 & P0) & P0 -> (-(a2) <= -(a1) & P87 & P78 & P69 & P56 & P47 & P38 & P24 & P16 & P4 & P0) & P0" 1;
pushnode 34 "(Real(-(a1)) & P89 & P0) &  (-(a2) <= -(a1) + 0 & P82 & P80 & P73 & P71 & P64 & P60 & P51 & P49 & P42 & P40 & P33 & P26 & P0) & P0 -> (Real(-(a1)) & P92 & P0) & (-(a2) <= -(a1) & P87 & P78 & P69 & P56 & P47 & P38 & P24 & P16 & P4 & P0) & P0" 0;
pushreference 33 "(Real(-(a1)) & P90 & P0) & P0 -> (-(a1) + 0 = -(a1) & P91 & P0) & P0" "aid";
pushnode 32 "(Real(-(a1)) & P89 & P0) &  (-(a2) <= -(a1) + 0 & P82 & P80 & P73 & P71 & P64 & P60 & P51 & P49 & P42 & P40 & P33 & P26 & P0) & P0 -> (-(a2) <= -(a1) & P87 & P78 & P69 & P56 & P47 & P38 & P24 & P16 & P4 & P0) & P0" 3;
pushreference 31 "P0 -> (Real(-(a1)) & P88 & P0) & P0" "rminus";
pushnode 30 " (-(a2) <= -(a1) + 0 & P82 & P80 & P73 & P71 & P64 & P60 & P51 & P49 & P42 & P40 & P33 & P26 & P0) & P0 -> (-(a2) <= -(a1) & P87 & P78 & P69 & P56 & P47 & P38 & P24 & P16 & P4 & P0) & P0" 2;
pushnode 29 "( a2 + -(a2) = 0 & P80 & P0) & (-(a2) <= -(a1) + a2 + -(a2) & P73 & P71 & P64 & P60 & P51 & P49 & P42 & P40 & P33 & P26 & P0) & P0 -> (-(a2) <= -(a1) & P78 & P69 & P56 & P47 & P38 & P24 & P16 & P4 & P0) & P0" 1;
pushreference 28 "P0 -> (a2 + -(a2) = 0 & P79 & P0) & P0" "ainv";
pushnode 27 " (-(a2) <= -(a1) + a2 + -(a2) & P73 & P71 & P64 & P60 & P51 & P49 & P42 & P40 & P33 & P26 & P0) & P0 -> (-(a2) <= -(a1) & P78 & P69 & P56 & P47 & P38 & P24 & P16 & P4 & P0) & P0" 2;
pushnode 26 "([-(a1) + a2] + -(a2) = -(a1) + a2 + -(a2) & P71 & P0) & (-(a2) <= [-(a1) + a2] + -(a2) & P64 & P60 & P51 & P49 & P42 & P40 & P33 & P26 & P0) & P0 -> (-(a2) <= -(a1) & P69 & P56 &  P47 & P38 & P24 & P16 & P4 & P0) & P0" 1;
pushreference 25 "P0 -> ([-(a1) + a2] + -(a2) = -(a1) + a2 + -(a2) & P70 & P0) & P0" "aas";
pushnode 24 " (-(a2) <= [-(a1) + a2] + -(a2) & P64 & P60 & P51 &  P49 & P42 & P40 & P33 & P26 & P0) & P0 -> (-(a2) <= -(a1) & P69 & P56 & P47 & P38 & P24 & P16 & P4 & P0) & P0" 2;
pushnode 21 "(-(a2) + 0 = -(a2) & P60 & P0) & ( -(a2) + 0 <= [-(a1) + a2] + -(a2) & P51 & P49 & P42 & P40 & P33 & P26 & P0) & P0 -> (-(a2) <= -(a1) & P56 & P47 & P38 & P24 & P16 & P4 & P0) & P0" 1;
pushnode 23 "(Real(-(a2)) & P62 & P0) & (-(a2) + 0 <= [-(a1) + a2] + -(a2) & P51 & P49 & P42 & P40 & P33 & P26 & P0) & P0 -> (Real(-(a2)) & P59 & P0) & (-(a2) <= -(a1) & P56 & P47 & P38 & P24 &  P16 & P4 & P0) & P0" 0;
pushreference 22 "P0 -> (Real(-(a2)) & P61 & P0) & P0" "rminus";
pushnode 20 "(-(a2) + 0 <=  [-(a1) + a2] + -(a2) & P51 & P49 & P42 & P40 & P33 & P26 & P0) & P0 -> (Real(-(a2)) & P59 & P0) &  (-(a2) <= -(a1) & P56 & P47 & P38 & P24 & P16 & P4 & P0) & P0" 2;
pushreference 19 "(Real(-(a2)) & P57 & P0) & P0 -> ( -(a2) + 0 = -(a2) & P58 & P0) & P0" "aid";
pushnode 18 "(-(a2) + 0 <= [-(a1) + a2] + -(a2) & P51 & P49 & P42 & P40 & P33 & P26 & P0) & P0 -> (-(a2) <= -(a1) & P56 & P47 & P38 & P24 & P16 & P4 & P0) & P0" 3;
pushnode 17 "(a2 + -(a1) = -(a1) + a2 & P49 & P0) & (-(a2) + 0 <= [a2 + -(a1)] + -(a2) & P42 & P40 & P33 & P26 & P0) & P0 -> (-(a2) <= -(a1) & P47 & P38 & P24 & P16 & P4 & P0) & P0" 1;
pushreference 16 "P0 -> (a2 + -(a1) = -(a1) + a2 & P48 & P0) & P0" "acom";
pushnode 15 "(-(a2) + 0 <= [a2 + -(a1)] + -(a2) & P42 & P40 & P33 & P26 & P0) & P0 -> (-(a2) <= -(a1) & P47 & P38 & P24 & P16 & P4 & P0) & P0" 2;
pushnode 14 "(0 + -(a2) = -(a2) + 0 & P40 & P0) & ( 0 + -(a2) <= [a2 + -(a1)] + -(a2) & P33 & P26 & P0) & P0 -> (-(a2) <= -(a1) & P38 & P24 & P16 & P4 & P0) & P0" 1;
pushreference 13 "P0 -> (0 + -(a2) = -(a2) + 0 & P39 & P0) & P0" "acom";
pushnode 12 "( 0 + -(a2) <= [a2 + -(a1)] + -(a2) & P33 & P26 & P0) & P0 -> (-(a2) <= -(a1) & P38 & P24 & P16 & P4 & P0) & P0" 2;
pushnode 11 " (0 <= a2 + -(a1) & P27 & P20 & P18 & P12 & P6 & P0) & P0 -> (0 <= a2 + -(a1) & P31 & P26 & P0) & P0" 0;
pushnode 10 "((0 <= a2 + -(a1) -> 0 + -(a2) <= [a2 + -(a1)] + -(a2)) & P26 & P0) & (0 <= a2 + -(a1) & P20 & P18 & P12 & P6 & P0) & P0 -> (-(a2) <= -(a1) & P24 & P16 & P4 & P0) & P0" 2;
pushreference 9 "P0 -> ((0 <= a2 + -(a1) -> 0 + -(a2) <= [a2 + -(a1)] + -(a2)) & P25 & P0) & P0" "ordadd";
pushnode 8 "(0 <= a2 + -(a1) & P20 & P18 & P12 & P6 & P0) & P0 -> ( -(a2) <= -(a1) & P24 & P16 & P4 & P0) & P0" 2;
pushnode 7 "(a1 + -(a1) = 0 & P18 & P0) & (a1 + -(a1) <= a2 + -(a1) & P12 & P6 & P0) & P0 -> (-(a2) <= -(a1) & P16 & P4 & P0) & P0" 1;
pushreference 6 "P0 -> (a1 + -(a1) = 0 & P17 & P0) & P0" "ainv";
pushnode 5 "(a1 + -(a1) <= a2 + -(a1) & P12 & P6 & P0) & P0 -> (-(a2) <= -(a1) & P16 & P4 & P0) & P0" 2;
pushnode 4 "(a1 <= a2 & P9 & P3 & P0) & P0 -> (a1 <= a2 & P10 & P6 & P0) & P0" 0;
pushnode 3 "( (a1 <= a2 -> a1 + -(a1) <= a2 + -(a1)) & P6 & P0) & (a1 <= a2 & P3 & P0) & P0 -> (-(a2) <= -(a1) & P4 & P0) & P0" 2;
pushreference 2 "P0 -> ((a1 <= a2 -> a1 + -(a1) <= a2 + -(a1)) & P5 & P0) & P0" "ordadd";
pushnode 1 "(a1 <= a2 & P3 & P0) & P0 -> (-(a2) <= -(a1) & P4 & P0) & P0" 2;
THEOREMS:=("thm 3.2.i",(termtosequent(parseprop("(a1 <= a2 & P3 & P0) & P0 -> (-(a2) <= -(a1) & P4 & P0) & P0")),hd(!PROOFSTACK)))::(!THEOREMS);
PROOFSTACK:=nil;
td "thm 3.2.i";
pushnode 12 "(-(0) = 0 & P16 & P14 & P11 & P7 & P3 & P0) & P0 -> (-(0) = 0 & P17 & P12 & P1 & P0) & P0" 0;
pushnode 11 "(0 + -(0) = 0 & P14 & P0) & (-(0) = 0 + -(0) & P11 & P7 & P3 & P0) & P0 -> (-(0) = 0 & P12 & P1 & P0) & P0" 1;
pushreference 10 "P0 -> (0 + -(0) = 0 & P13 & P0) & P0" "ainv";
pushnode 9 "(-(0) = 0 + -(0) & P11 & P7 & P3 & P0) & P0 -> (-(0) = 0 & P12 & P1 & P0) & P0" 2;
pushnode 6 "(-(0) + 0 = -(0) & P7 & P0) & (-(0) + 0 = 0 + -(0) & P3 & P0) & P0 -> ( -(0) = 0 & P1 & P0) & P0" 1;
pushnode 8 " (Real(-(0)) & P9 & P0) & (-(0) + 0 = 0 + -(0) & P3 & P0) & P0 -> (Real(-(0)) & P6 & P0) & (-(0) = 0 & P1 & P0) & P0" 0;
pushreference 7 "P0 -> (Real(-(0)) & P8 & P0) & P0" "rminus";
pushnode 5 "(-(0) + 0 = 0 + -(0) & P3 & P0) & P0 -> (Real(-(0)) & P6 & P0) & (-(0) = 0 & P1 & P0) & P0" 2;
pushreference 4 "(Real(-(0)) & P4 & P0) & P0 -> (-(0) + 0 = -(0) & P5 & P0) & P0" "aid";
pushnode 3 " (-(0) + 0 = 0 + -(0) & P3 & P0) & P0 -> (-(0) = 0 & P1 & P0) & P0" 3;
pushreference 2 "P0 -> (-(0) + 0 = 0 + -(0) & P2 & P0) & P0" "acom";
pushnode 1 "P0 -> ( -(0) = 0 & P1 & P0) & P0" 2;
THEOREMS:=("zeros",(termtosequent(parseprop("P0 -> (-(0) = 0 & P1 & P0) & P0")),hd(!PROOFSTACK)))::(!THEOREMS);
PROOFSTACK:=nil;
td "zeros";
pushnode 22 " (-(-(a1)) = a1 & P38 & P34 & P28 & P26 & P22 & P20 & P14 & P12 & P8 & P6 & P4 & P0) & P0 ->  (-(-(a1)) = a1 & P40 & P30 & P24 & P16 & P10 & P2 & P0) & P0" 0;
pushnode 19 " (-(-(a1)) + 0 = -(-(a1)) & P34 & P0) & (-(-(a1)) + 0 = a1 & P28 & P26 & P22 & P20 & P14 & P12 & P8 & P6 & P4 & P0) & P0 -> (-(-(a1)) = a1 & P30 & P24 & P16 & P10 & P2 & P0) & P0" 1;
pushnode 21 "(Real(-(-(a1))) & P36 & P0) & (-(-(a1)) + 0 = a1 & P28 & P26 & P22 & P20 & P14 & P12 & P8 & P6 & P4 & P0) & P0 -> ( Real(-(-(a1))) & P33 & P0) & (-(-(a1)) = a1 & P30 & P24 & P16 & P10 & P2 & P0) & P0" 0;
pushreference 20 "P0 -> (Real(-(-(a1))) & P35 & P0) & P0" "rminus";
pushnode 18 "(-(-(a1)) + 0 = a1 & P28 & P26 & P22 & P20 & P14 & P12 & P8 & P6 & P4 & P0) & P0 -> (Real(-(-(a1))) & P33 & P0) & (-(-(a1)) = a1 & P30 & P24 & P16 & P10 & P2 & P0) & P0" 2;
pushreference 17 "(Real(-(-(a1))) & P31 & P0) & P0 -> (-(-(a1)) + 0 = -(-(a1)) & P32 & P0) & P0" "aid";
pushnode 16 "(-(-(a1)) + 0 = a1 & P28 & P26 & P22 & P20 & P14 & P12 & P8 & P6 & P4 & P0) & P0 -> (-(-(a1)) = a1 & P30 & P24 & P16 & P10 & P2 & P0) & P0" 3;
pushnode 15 "(0 + -(-(a1)) = -(-(a1)) + 0 & P26 & P0) & (0 + -(-(a1)) = a1 & P22 & P20 & P14 & P12 & P8 &  P6 & P4 & P0) & P0 ->  (-(-(a1)) = a1 & P24 & P16 & P10 & P2 & P0) & P0" 1;
pushreference 14 "P0 -> (0 + -(-(a1)) = -(-(a1)) + 0 & P25 & P0) & P0" "acom";
pushnode 13 "( 0 + -(-(a1)) = a1 & P22 & P20 & P14 & P12 & P8 & P6 & P4 & P0) & P0 -> (-(-(a1)) = a1 & P24 & P16 & P10 & P2 & P0) & P0" 2;
pushnode 12 "(a1 + 0 = a1 & P20 & P0) & (0 + -(-(a1)) = a1 + 0 & P14 & P12 & P8 & P6 & P4 & P0) & (Real(a1) & P15 & P9 & P1 & P0) & P0 -> (-(-(a1)) = a1 & P16 & P10 & P2 & P0) & P0" 1;
pushnode 11 "( Real(a1) & P15 & P9 & P1 & P0) &  (0 + -(-(a1)) = a1 + 0 & P14 & P12 & P8 & P6 & P4 & P0) & P0 -> (Real(a1) & P19 & P0) & (-(-(a1)) = a1 & P16 & P10 & P2 & P0) & P0" 0;
pushreference 10 "(Real(a1) & P17 & P0) & P0 -> (a1 + 0 = a1 & P18 & P0) & P0" "aid";
pushnode 9 "(0 + -(-(a1)) = a1 + 0 & P14 & P12 & P8 & P6 & P4 & P0) & (Real(a1) & P15 & P9 & P1 & P0) & P0 -> (-(-(a1)) = a1 & P16 & P10 & P2 & P0) & P0" 3;
pushnode 8 "( a1 + -(a1) = 0 & P12 & P0) & ([a1 + -(a1)] + -(-(a1)) = a1 + 0 & P8 & P6 & P4 & P0) &  (Real(a1) & P9 & P1 & P0) & P0 -> (-(-(a1)) = a1 & P10 & P2 & P0) & P0" 1;
pushreference 7 "P0 -> (a1 + -(a1) = 0 & P11 & P0) & P0" "ainv";
pushnode 6 "([a1 + -(a1)] + -(-(a1)) = a1 + 0 & P8 & P6 & P4 & P0) &  (Real(a1) & P9 & P1 & P0) & P0 -> (-(-(a1)) = a1 & P10 & P2 & P0) & P0" 2;
pushnode 5 " (-(a1) + -(-(a1)) = 0 & P6 & P0) & ([a1 + -(a1)] + -(-(a1)) = a1 + -(a1) + -(-(a1)) & P4 & P0) & (Real(a1) & P1 & P0) & P0 -> (-(-(a1)) = a1 & P2 & P0) & P0" 1;
pushreference 4 "P0 -> (-(a1) + -(-(a1)) = 0 & P5 & P0) & P0" "ainv";
pushnode 3 "([a1 + -(a1)] + -(-(a1)) = a1 + -(a1) + -(-(a1)) & P4 & P0) & (Real(a1) & P1 & P0) & P0 -> (-(-(a1)) = a1 & P2 & P0) & P0" 2;
pushreference 2 "P0 ->  ([a1 + -(a1)] + -(-(a1)) = a1 + -(a1) + -(-(a1)) & P3 & P0) & P0" "aas";
pushnode 1 "(Real(a1) & P1 & P0) & P0 -> (-(-(a1)) = a1 & P2 & P0) & P0" 2;
THEOREMS:=("2neg",(termtosequent(parseprop("(Real(a1) & P1 & P0) & P0 -> (-(-(a1)) = a1 & P2 & P0) & P0")),hd(!PROOFSTACK)))::(!THEOREMS);
PROOFSTACK:=nil;
td "2neg";
pushnode 47 "(a2 * a3 <= a1 * a3 & P159 & P157 & P147 & P145 & P135 & P131 & P119 & P115 & P111 & P0) & P0 -> (a2 * a3 <= a1 * a3 & P167 & P155 & P143 & P127 &  P107 & P87 & P76 & P65 & P38 & P20 & P6 & P0) & P0" 0;
pushnode 46 "(a3 * a1 = a1 * a3 & P157 & P0) & (a2 * a3 <= a3 * a1 & P147 & P145 & P135 & P131 & P119 & P115 & P111 & P0) & P0 -> (a2 * a3 <= a1 * a3 & P155 & P143 & P127 & P107 & P87 & P76 & P65 & P38 & P20 & P6 & P0) & P0" 1;
pushreference 45 " P0 -> (a3 * a1 = a1 * a3 & P156 & P0) & P0" "mcom";
pushnode 44 "(a2 * a3 <= a3 * a1 & P147 & P145 & P135 & P131 & P119 & P115 & P111 & P0) & P0 -> (a2 * a3 <= a1 * a3 & P155 & P143 & P127 & P107 & P87 & P76 & P65 & P38 & P20 &  P6 & P0) & P0" 2;
pushnode 43 "(a3 * a2 = a2 * a3 & P145 & P0) & (a3 * a2 <= a3 * a1 & P135 & P131 & P119 & P115 &  P111 & P0) & P0 -> (a2 * a3 <= a1 * a3 & P143 & P127 & P107 & P87 & P76 & P65 & P38 & P20 & P6 & P0) & P0" 1;
pushreference 42 "P0 -> (a3 * a2 = a2 * a3 & P144 & P0) & P0" "mcom";
pushnode 41 " (a3 * a2 <= a3 * a1 & P135 & P131 & P119 & P115 & P111 & P0) & P0 -> (a2 * a3 <= a1 * a3 & P143 & P127 & P107 & P87 & P76 & P65 & P38 & P20 & P6 & P0) & P0" 2;
pushnode 38 "( -(-(a3 * a1)) = a3 * a1 & P131 & P0) & (a3 * a2 <= -(-(a3 * a1)) & P119 & P115 & P111 & P0) & P0 -> (a2 * a3 <= a1 * a3 & P127 & P107 & P87 & P76 & P65 & P38 & P20 & P6 & P0) & P0" 1;
pushnode 40 " (Real(a3 * a1) & P133 & P0) & (a3 * a2 <= -(-(a3 * a1)) & P119 & P115 & P111 & P0) & P0 -> (Real( a3 * a1) & P130 & P0) & (a2 * a3 <= a1 * a3 & P127 & P107 & P87 & P76 & P65 & P38 & P20 & P6 & P0) & P0" 0;
pushreference 39 "P0 -> (Real(a3 * a1) &  P132 & P0) & P0" "rtimes";
pushnode 37 "(a3 * a2 <= -(-(a3 * a1)) & P119 & P115 & P111 & P0) & P0 -> (Real(a3 * a1) & P130 & P0) & (a2 * a3 <= a1 * a3 & P127 & P107 & P87 & P76 & P65 & P38 & P20 & P6 & P0) & P0" 2;
pushreference 36 "(Real(a3 * a1) &  P128 & P0) & P0 -> (-(-(a3 * a1)) = a3 * a1 & P129 & P0) & P0" "2neg";
pushnode 35 "(a3 * a2 <= -(-(a3 * a1)) & P119 & P115 & P111 & P0) & P0 -> (a2 * a3 <= a1 * a3 & P127 & P107 & P87 & P76 & P65 & P38 & P20 & P6 & P0) & P0" 3;
pushnode 32 " (-(-(a3 * a2)) = a3 * a2 & P115 & P0) & (-(-(a3 * a2)) <= -(-(a3 * a1)) & P111 & P0) & (-(a3 * a1) <= -(a3 * a2) & P100 & P89 & P80 & P78 & P69 & P67 & P58 & P56 & P31 & P22 & P0) & P0 -> (a2 * a3 <= a1 * a3 & P107 & P87 & P76 & P65 & P38 & P20 & P6 & P0) & P0" 1;
pushnode 34 "(Real(a3 * a2) & P117 & P0) & ( -(-(a3 * a2)) <= -(-(a3 * a1)) & P111 & P0) & (-(a3 * a1) <= -(a3 * a2) & P100 & P89 & P80 & P78 & P69 & P67 & P58 & P56 & P31 & P22 & P0) & P0 -> (Real(a3 * a2) & P114 & P0) & (a2 * a3 <= a1 * a3 & P107 & P87 & P76 & P65 & P38 & P20 & P6 & P0) & P0" 0;
pushreference 33 "P0 -> (Real(a3 * a2) & P116 & P0) & P0" "rtimes";
pushnode 31 "(-(-(a3 * a2)) <= -(-(a3 * a1)) & P111 & P0) & (-(a3 * a1) <= -(a3 * a2) & P100 & P89 & P80 & P78 & P69 & P67 & P58 & P56 & P31 & P22 & P0) & P0 -> (Real(a3 * a2) & P114 & P0) & (a2 * a3 <= a1 * a3 & P107 & P87 & P76 & P65 & P38 & P20 & P6 & P0) & P0" 2;
pushreference 30 " (Real(a3 * a2) & P112 & P0) & P0 -> (-(-(a3 * a2)) = a3 * a2 & P113 & P0) & P0" "2neg";
pushnode 29 " (-(-(a3 * a2)) <= -(-(a3 * a1)) & P111 & P0) & (-(a3 * a1) <= -(a3 * a2) & P100 & P89 & P80 & P78 & P69 & P67 & P58 & P56 & P31 & P22 & P0) & P0 -> (a2 * a3 <= a1 * a3 & P107 & P87 & P76 & P65 & P38 & P20 & P6 & P0) & P0" 3;
pushnode 28 " (-(a3 * a1) <= -(a3 * a2) & P100 & P89 & P80 & P78 & P69 & P67 & P58 & P56 & P31 & P22 & P0) & P0 -> (-(a3 * a1) <= -(a3 * a2) & P110 & P0) & (a2 * a3 <= a1 * a3 & P107 & P87 & P76 & P65 & P38 & P20 & P6 & P0) & P0" 0;
pushreference 27 "(-(a3 * a1) <= -(a3 * a2) & P108 & P0) & P0 -> (-(-(a3 * a2)) <= -(-(a3 * a1)) & P109 & P0) & P0" "thm 3.2.i";
pushnode 26 "(-(a3 * a1) <= -(a3 * a2) & P100 & P89 & P80 & P78 & P69 & P67 & P58 & P56 & P31 & P22 & P0) & P0 -> (a2 * a3 <= a1 * a3 & P107 & P87 & P76 & P65 & P38 & P20 & P6 & P0) & P0" 3;
pushnode 24 " (-(a3) * a2 = -(a3 * a2) & P89 & P0) & (-(a3 * a1) <= -(a3) * a2 & P80 & P78 & P69 & P67 & P58 & P56 & P31 & P22 & P0) & P0 -> ( a2 * a3 <= a1 * a3 & P87 & P76 & P65 & P38 & P20 & P6 & P0) & P0" 1;
pushreference 23 " P0 -> (-(a3) * a2 = -(a3 * a2) & P88 & P0) & P0" "thm 3.1.iii";
pushnode 22 "(-(a3 * a1) <= -(a3) * a2 & P80 & P78 & P69 & P67 & P58 & P56 & P31 & P22 & P0) & P0 -> (a2 * a3 <= a1 * a3 & P87 & P76 & P65 & P38 & P20 & P6 & P0) & P0" 2;
pushnode 21 "(-(a3) * a1 = -(a3 * a1) & P78 & P0) & (-(a3) * a1 <= -(a3) * a2 & P69 & P67 & P58 & P56 & P31 & P22 & P0) & P0 -> (a2 * a3 <= a1 * a3 & P76 & P65 & P38 & P20 & P6 & P0) & P0" 1;
pushreference 20 "P0 -> (-(a3) * a1 = -(a3 * a1) & P77 & P0) & P0" "thm 3.1.iii";
pushnode 19 "(-(a3) * a1 <= -(a3) * a2 & P69 & P67 & P58 & P56 & P31 & P22 & P0) & P0 -> ( a2 * a3 <= a1 * a3 & P76 & P65 & P38 & P20 & P6 & P0) & P0" 2;
pushnode 18 "(a2 * -(a3) = -(a3) * a2 & P67 & P0) &  (-(a3) * a1 <= a2 * -(a3) & P58 & P56 & P31 & P22 & P0) & P0 -> (a2 * a3 <= a1 * a3 & P65 & P38 & P20 & P6 & P0) & P0" 1;
pushreference 17 "P0 -> (a2 * -(a3) = -(a3) * a2 & P66 & P0) & P0" "mcom";
pushnode 16 "( -(a3) * a1 <= a2 * -(a3) & P58 & P56 & P31 & P22 & P0) & P0 -> (a2 * a3 <= a1 * a3 & P65 & P38 & P20 & P6 & P0) & P0" 2;
pushnode 15 "(a1 * -(a3) = -(a3) * a1 & P56 & P0) &  (a1 * -(a3) <= a2 * -(a3) & P31 & P22 & P0) & P0 -> (a2 * a3 <= a1 * a3 & P38 & P20 & P6 & P0) & P0" 1;
pushreference 14 "P0 -> (a1 * -(a3) = -(a3) * a1 & P55 & P0) & P0" "mcom";
pushnode 11 " (a1 * -(a3) <= a2 * -(a3) & P31 & P22 & P0) & P0 -> (a2 * a3 <= a1 * a3 & P38 & P20 & P6 & P0) & P0" 2;
pushnode 13 "( 0 <= -(a3) & P47 & P23 & P14 & P12 & P10 & P0) & P0 -> (0 <= -(a3) & P53 & P29 & P22 & P0) & P0" 0;
pushnode 12 "(a1 <= a2 & P43 & P27 & P18 & P4 & P0) & P0 -> (a1 <= a2 & P45 & P29 &  P22 & P0) & P0" 0;
pushnode 10 "(0 <= -(a3) & P23 & P14 & P12 & P10 & P0) & (a1 <= a2 & P27 & P18 & P4 & P0) & P0 -> ((a1 <= a2 & 0 <= -(a3)) & P29 & P22 & P0) & P0" 2;
pushnode 9 " ((a1 <= a2 & 0 <= -(a3) -> a1 * -(a3) <= a2 * -(a3)) & P22 & P0) & (0 <= -(a3) & P14 & P12 & P10 & P0) & (a1 <= a2 & P18 & P4 & P0) & P0 -> (a2 * a3 <= a1 * a3 & P20 & P6 & P0) & P0" 2;
pushreference 8 "P0 -> ( (a1 <= a2 & 0 <= -(a3) -> a1 * -(a3) <= a2 * -(a3)) & P21 & P0) & P0" "ordmult";
pushnode 7 " (0 <= -(a3) & P14 & P12 & P10 & P0) & (a1 <= a2 & P18 & P4 & P0) & P0 ->  (a2 * a3 <= a1 * a3 & P20 & P6 & P0) & P0" 2;
pushnode 6 "(-(0) = 0 & P12 & P0) & (-(0) <= -(a3) & P10 & P0) & (a1 <= a2 & P4 & P0) & (a3 <= 0 & P5 & P0) & P0 -> (a2 * a3 <= a1 * a3 & P6 & P0) & P0" 1;
pushreference 5 "P0 ->  (-(0) = 0 & P11 & P0) & P0" "zeros";
pushnode 4 " (-(0) <= -(a3) & P10 & P0) & (a1 <= a2 & P4 & P0) & (a3 <= 0 & P5 & P0) & P0 -> (a2 * a3 <= a1 * a3 & P6 & P0) & P0" 2;
pushnode 3 "(a3 <= 0 & P5 & P0) & (a1 <= a2 & P4 & P0) & P0 -> (a3 <= 0 & P9 & P0) & (a2 * a3 <= a1 * a3 & P6 & P0) & P0" 0;
pushreference 2 "(a3 <= 0 &  P7 & P0) & P0 -> (-(0) <= -(a3) & P8 & P0) & P0" "thm 3.2.i";
pushnode 1 " (a1 <= a2 & P4 & P0) & (a3 <= 0 & P5 & P0) & P0 -> (a2 * a3 <= a1 * a3 & P6 & P0) & P0" 3;
THEOREMS:=("thm 3.2.ii",(termtosequent(parseprop(" (a1 <= a2 & P4 & P0) & (a3 <= 0 & P5 & P0) & P0 -> (a2 * a3 <= a1 * a3 & P6 & P0) & P0")),hd(!PROOFSTACK)))::(!THEOREMS);
PROOFSTACK:=nil;
td "thm 3.2.ii";
pushnode 16 "(0 <= a1 * a2 & P48 & P44 & P35 & P33 & P14 & P7 & P0) & P0 ->  (0 <= a1 * a2 & P53 & P40 & P19 & P5 & P0) & P0" 0;
pushnode 13 "(a2 * 0 = 0 & P44 & P0) &  (a2 * 0 <= a1 * a2 & P35 & P33 & P14 & P7 & P0) & P0 -> (0 <= a1 * a2 & P40 & P19 & P5 & P0) & P0" 1;
pushnode 15 "(Real(0) & P46 & P0) & (a2 * 0 <= a1 * a2 & P35 & P33 & P14 & P7 & P0) & P0 -> (Real(0) & P43 & P0) & (0 <= a1 * a2 & P40 & P19 & P5 & P0) & P0" 0;
pushreference 14 "P0 -> (Real(0) & P45 & P0) & P0" "zero";
pushnode 12 "(a2 * 0 <= a1 * a2 & P35 & P33 & P14 & P7 & P0) & P0 -> (Real(0) & P43 & P0) & (0 <= a1 * a2 & P40 & P19 & P5 & P0) & P0" 2;
pushreference 11 "(Real(0) & P41 & P0) & P0 -> (a2 * 0 = 0 & P42 & P0) & P0" "thm 3.1.ii";
pushnode 10 "(a2 * 0 <= a1 * a2 &  P35 & P33 & P14 & P7 & P0) & P0 -> (0 <= a1 * a2 & P40 & P19 & P5 & P0) & P0" 3;
pushnode 9 " (0 * a2 = a2 * 0 & P33 & P0) & (0 * a2 <= a1 * a2 & P14 & P7 & P0) & P0 -> (0 <= a1 * a2 & P19 & P5 & P0) & P0" 1;
pushreference 8 "P0 -> (0 * a2 = a2 * 0 & P32 & P0) & P0" "mcom";
pushnode 5 "(0 * a2 <= a1 * a2 & P14 & P7 & P0) & P0 -> (0 <= a1 * a2 & P19 & P5 & P0) & P0" 2;
pushnode 7 "(0 <= a2 & P29 & P11 & P4 & P0) & P0 -> (0 <= a2 & P30 & P12 & P7 & P0) & P0" 0;
pushnode 6 "(0 <= a1 & P22 & P10 & P3 & P0) & P0 -> (0 <= a1 & P24 & P12 & P7 & P0) & P0" 0;
pushnode 4 "(0 <= a1 & P10 & P3 & P0) & (0 <= a2 & P11 & P4 & P0) & P0 -> ( (0 <= a1 & 0 <= a2) & P12 & P7 & P0) & P0" 2;
pushnode 3 " ((0 <= a1 & 0 <= a2 -> 0 * a2 <= a1 * a2) & P7 & P0) & (0 <= a1 & P3 & P0) & (0 <= a2 & P4 & P0) & P0 -> (0 <=  a1 * a2 & P5 & P0) & P0" 2;
pushreference 2 "P0 -> ((0 <= a1 & 0 <= a2 -> 0 * a2 <= a1 * a2) & P6 & P0) & P0" "ordmult";
pushnode 1 "(0 <= a1 & P3 & P0) & (0 <= a2 & P4 & P0) & P0 -> (0 <= a1 * a2 & P5 & P0) & P0" 2;
THEOREMS:=("thm 3.2.iii",(termtosequent(parseprop("(0 <= a1 & P3 & P0) & (0 <= a2 & P4 & P0) & P0 -> (0 <= a1 * a2 & P5 & P0) & P0")),hd(!PROOFSTACK)))::(!THEOREMS);
PROOFSTACK:=nil;
td "thm 3.2.iii";
pushnode 44 "(0 <=  a1 * a1 & P103 & P101 & P95 & P91 & P83 & P81 & P65 & P59 & P0) & P0 -> (0 <= a1 * a1 & P107 & P99 & P87 & P69 & P57 & P10 & P2 & P0) & P0" 0;
pushnode 43 " (-(a1) * -(a1) = a1 * a1 & P101 & P0) &  (0 <= -(a1) * -(a1) & P95 & P91 & P83 & P81 & P65 & P59 & P0) & P0 -> (0 <= a1 * a1 & P99 & P87 & P69 & P57 & P10 & P2 & P0) & P0" 1;
pushreference 42 "P0 -> (-(a1) * -(a1) = a1 * a1 & P100 & P0) & P0" "thm 3.1.iv";
pushnode 41 " (0 <= -(a1) * -(a1) & P95 & P91 & P83 & P81 & P65 & P59 & P0) & P0 -> (0 <= a1 * a1 & P99 & P87 & P69 & P57 & P10 & P2 & P0) & P0" 2;
pushnode 38 "(-(a1) * 0 = 0 & P91 & P0) & (-(a1) * 0 <= -(a1) * -(a1) & P83 & P81 & P65 & P59 & P0) & P0 ->  (0 <= a1 * a1 & P87 & P69 & P57 & P10 & P2 & P0) & P0" 1;
pushnode 40 "(Real(0) & P93 & P0) & (-(a1) * 0 <= -(a1) * -(a1) & P83 & P81 & P65 & P59 & P0) & P0 -> (Real(0) & P90 & P0) & (0 <= a1 * a1 & P87 & P69 & P57 & P10 & P2 & P0) & P0" 0;
pushreference 39 "P0 -> (Real(0) & P92 & P0) & P0" "zero";
pushnode 37 "( -(a1) * 0 <= -(a1) * -(a1) & P83 & P81 & P65 & P59 & P0) & P0 ->  (Real(0) & P90 & P0) & (0 <= a1 * a1 & P87 & P69 & P57 & P10 & P2 & P0) & P0" 2;
pushreference 36 "( Real(0) & P88 & P0) & P0 -> (-(a1) * 0 = 0 & P89 & P0) & P0" "thm 3.1.ii";
pushnode 35 "(-(a1) * 0 <= -(a1) * -(a1) & P83 & P81 & P65 & P59 & P0) & P0 ->  (0 <= a1 * a1 & P87 & P69 & P57 & P10 & P2 & P0) & P0" 3;
pushnode 34 "(0 * -(a1) = -(a1) * 0 & P81 & P0) &  (0 * -(a1) <= -(a1) * -(a1) & P65 & P59 & P0) & P0 ->  (0 <= a1 * a1 & P69 & P57 & P10 & P2 & P0) & P0" 1;
pushreference 33 "P0 -> (0 * -(a1) = -(a1) * 0 & P80 & P0) & P0" "mcom";
pushnode 30 "(0 * -(a1) <= -(a1) * -(a1) & P65 & P59 & P0) & P0 -> (0 <= a1 * a1 & P69 & P57 & P10 & P2 & P0) & P0" 2;
pushnode 32 "(0 <= -(a1) & P75 & P60 & P54 & P52 & P50 & P0) & P0 -> (0 <= -(a1) & P78 & P63 & P59 & P0) & P0" 0;
pushnode 31 "(0 <= -(a1) & P70 & P60 & P54 & P52 & P50 & P0) & P0 -> (0 <= -(a1) & P73 & P63 & P59 & P0) & P0" 0;
pushnode 29 "(0 <= -(a1) & P60 & P54 & P52 & P50 & P0) & P0 -> ((0 <= -(a1) & 0 <= -(a1)) & P63 &  P59 & P0) & P0" 2;
pushnode 28 " ((0 <= -(a1) & 0 <= -(a1) -> 0 * -(a1) <= -(a1) * -(a1)) & P59 & P0) & (0 <= -(a1) & P54 & P52 & P50 & P0) & P0 -> (0 <=  a1 * a1 & P57 & P10 & P2 & P0) & P0" 2;
pushreference 27 "P0 -> ( (0 <= -(a1) & 0 <= -(a1) -> 0 * -(a1) <= -(a1) * -(a1)) & P58 & P0) & P0" "ordmult";
pushnode 26 "(0 <= -(a1) & P54 & P52 & P50 & P0) & P0 -> (0 <= a1 * a1 & P57 & P10 & P2 & P0) & P0" 2;
pushnode 25 " (-(0) = 0 & P52 & P0) & (-(0) <= -(a1) & P50 & P0) & (a1 <= 0 & P8 & P4 & P0) & P0 -> (0 <=  a1 * a1 & P10 & P2 & P0) & P0" 1;
pushreference 24 "P0 -> (-(0) = 0 & P51 & P0) & P0" "zeros";
pushnode 23 "(-(0) <= -(a1) & P50 & P0) & (a1 <= 0 & P8 & P4 & P0) & P0 -> (0 <= a1 * a1 & P10 & P2 & P0) & P0" 2;
pushnode 22 " (a1 <= 0 & P8 & P4 & P0) & P0 -> (a1 <= 0 & P49 & P0) & (0 <= a1 * a1 & P10 & P2 & P0) & P0" 0;
pushreference 21 " (a1 <= 0 & P47 & P0) & P0 -> (-(0) <= -(a1) & P48 & P0) & P0" "thm 3.2.i";
pushnode 5 "(a1 <= 0 & P8 & P4 & P0) & P0 -> (0 <= a1 * a1 & P10 & P2 & P0) & P0" 3;
pushnode 20 " (0 <= a1 * a1 & P43 & P39 & P32 & P30 & P17 & P12 & P0) & P0 ->  (0 <= a1 * a1 & P46 & P35 & P20 & P7 & P2 & P0) & P0" 0;
pushnode 17 "(a1 * 0 = 0 & P39 & P0) &  (a1 * 0 <= a1 * a1 & P32 & P30 & P17 & P12 & P0) & P0 ->  (0 <= a1 * a1 & P35 & P20 & P7 & P2 & P0) & P0" 1;
pushnode 19 "(Real(0) & P41 & P0) &  (a1 * 0 <= a1 * a1 & P32 & P30 & P17 & P12 & P0) & P0 -> (Real(0) & P38 & P0) & (0 <= a1 * a1 & P35 & P20 & P7 & P2 & P0) & P0" 0;
pushreference 18 "P0 -> (Real(0) & P40 & P0) & P0" "zero";
pushnode 16 "(a1 * 0 <= a1 * a1 & P32 & P30 & P17 & P12 & P0) & P0 -> (Real(0) & P38 & P0) &  (0 <= a1 * a1 & P35 & P20 & P7 & P2 & P0) & P0" 2;
pushreference 15 "(Real(0) & P36 & P0) & P0 -> (a1 * 0 = 0 & P37 & P0) & P0" "thm 3.1.ii";
pushnode 14 "(a1 * 0 <= a1 * a1 & P32 & P30 & P17 & P12 & P0) & P0 -> (0 <= a1 * a1 & P35 & P20 & P7 & P2 & P0) & P0" 3;
pushnode 13 "(0 * a1 = a1 * 0 & P30 & P0) & (0 * a1 <= a1 * a1 & P17 & P12 & P0) & P0 -> (0 <= a1 * a1 & P20 & P7 & P2 & P0) & P0" 1;
pushreference 12 "P0 -> (0 * a1 = a1 * 0 & P29 & P0) & P0" "mcom";
pushnode 9 "(0 * a1 <= a1 * a1 & P17 & P12 & P0) & P0 ->  (0 <= a1 * a1 & P20 & P7 & P2 & P0) & P0" 2;
pushnode 11 "(0 <= a1 & P25 & P13 & P5 & P4 & P0) & P0 -> (0 <= a1 & P27 & P15 & P12 & P0) & P0" 0;
pushnode 10 "(0 <= a1 & P21 & P13 & P5 & P4 & P0) & P0 -> (0 <= a1 & P23 & P15 & P12 & P0) & P0" 0;
pushnode 8 "(0 <= a1 & P13 & P5 & P4 & P0) & P0 -> ((0 <= a1 & 0 <= a1) & P15 & P12 & P0) & P0" 2;
pushnode 7 "((0 <= a1 & 0 <= a1 -> 0 * a1 <= a1 * a1) & P12 & P0) &  (0 <= a1 & P5 & P4 & P0) & P0 -> (0 <= a1 * a1 & P7 & P2 & P0) & P0" 2;
pushreference 6 "P0 -> ( (0 <= a1 & 0 <= a1 -> 0 * a1 <= a1 * a1) & P11 & P0) & P0" "ordmult";
pushnode 4 "(0 <= a1 & P5 & P4 & P0) & P0 -> ( 0 <= a1 * a1 & P7 & P2 & P0) & P0" 2;
pushnode 3 "((0 <= a1 v a1 <= 0) & P4 & P0) & P0 ->  (0 <= a1 * a1 & P2 & P0) & P0" 2;
pushreference 2 "P0 -> ((0 <= a1 v a1 <= 0) & P3 & P0) & P0" "totorder";
pushnode 1 "P0 -> (0 <= a1 * a1 & P2 & P0) & P0" 2;
THEOREMS:=("thm 3.2.iv",(termtosequent(parseprop(" P0 -> (0 <= a1 * a1 & P2 & P0) & P0")),hd(!PROOFSTACK)))::(!THEOREMS);
PROOFSTACK:=nil;
td "thm 3.2.iv";
pushnode 8 "(a2 + 0 = a1 + 0 & P26 & P21 & P16 & P17 & P10 & P5 & P3 & P0) & P0 -> (a2 + 0 = a1 + 0 & P30 & P25 & P20 & P8 & P4 & P0) & P0" 0;
pushnode 7 "(a2 + 0 = a1 + 0 & P21 & P16 & P17 & P10 & P5 & P3 & P0) & P0 -> (a2 eq a1 & P25 & P20 & P8 & P4 & P0) & P0" 1;
pushnode 6 "(a2 + 0 = a1 + 0 & P16 & P10 & P0) & (a1 + 0 = a2 + 0 & P17 & P5 & P3 & P0) & P0 -> (a2 eq a1 & P20 & P8 & P4 & P0) & P0" 1;
pushnode 5 "(a1 + 0 = a2 + 0 & P11 & P5 & P3 & P0) & P0 -> (a1 + 0 = a2 + 0 & P14 & P10 & P0) & P0" 0;
pushnode 4 "( (a1 + 0 = a2 + 0 -> a2 + 0 = a1 + 0) & P10 & P0) & (a1 + 0 = a2 + 0 & P5 & P3 & P0) & P0 -> ( a2 eq a1 & P8 & P4 & P0) & P0" 2;
pushreference 3 "P0 -> ((a1 + 0 = a2 + 0 -> a2 + 0 = a1 + 0) & P9 & P0) & P0" "symm";
pushnode 2 "(a1 + 0 = a2 + 0 & P5 & P3 & P0) & P0 -> (a2 eq a1 & P8 & P4 & P0) & P0" 2;
pushnode 1 "(a1 eq a2 & P3 & P0) & P0 -> (a2 eq a1 & P4 & P0) & P0" 1;
THEOREMS:=("eqsymm",(termtosequent(parseprop("(a1 eq a2 & P3 & P0) & P0 ->  (a2 eq a1 & P4 & P0) & P0")),hd(!PROOFSTACK)))::(!THEOREMS);
PROOFSTACK:=nil;
td "eqsymm";
pushnode 10 " (a1 = a2 & P23 & P21 & P14 & P12 & P5 & P3 & P0) & P0 -> (a1 = a2 & P26 & P17 & P8 & P4 & P0) & P0" 0;
pushnode 9 " (a2 + 0 = a2 & P21 & P0) & (a1 =  a2 + 0 & P14 & P12 & P5 & P3 & P0) & (Real(a2) & P16 & P7 & P2 & P0) & P0 -> (a1 = a2 & P17 & P8 & P4 & P0) & P0" 1;
pushnode 8 " (Real(a2) & P16 & P7 & P2 & P0) & (a1 = a2 + 0 & P14 & P12 & P5 & P3 & P0) & P0 -> ( Real(a2) & P20 & P0) & (a1 = a2 & P17 & P8 & P4 & P0) & P0" 0;
pushreference 7 " (Real(a2) & P18 & P0) & P0 -> (a2 + 0 = a2 & P19 & P0) & P0" "aid";
pushnode 6 " (a1 = a2 + 0 & P14 & P12 & P5 & P3 & P0) & (Real(a2) & P16 & P7 & P2 & P0) & P0 -> (a1 = a2 & P17 & P8 & P4 & P0) & P0" 3;
pushnode 5 " (a1 + 0 = a1 & P12 & P0) & (a1 + 0 = a2 + 0 & P5 & P3 & P0) &  (Real(a1) & P6 & P1 & P0) & (Real(a2) & P7 & P2 & P0) & P0 -> (a1 = a2 & P8 & P4 & P0) & P0" 1;
pushnode 4 "(Real(a1) & P6 & P1 & P0) & (Real(a2) & P7 & P2 & P0) & ( a1 + 0 = a2 + 0 & P5 & P3 & P0) & P0 -> (Real(a1) & P11 & P0) & (a1 = a2 & P8 & P4 & P0) & P0" 0;
pushreference 3 "(Real(a1) & P9 & P0) & P0 -> (a1 + 0 = a1 & P10 & P0) & P0" "aid";
pushnode 2 "(a1 + 0 = a2 + 0 & P5 & P3 & P0) & (Real(a1) & P6 & P1 & P0) & (Real(a2) & P7 & P2 & P0) & P0 -> ( a1 = a2 & P8 & P4 & P0) & P0" 3;
pushnode 1 "(a1 eq a2 & P3 & P0) & (Real(a1) & P1 & P0) & (Real(a2) & P2 & P0) & P0 -> (a1 = a2 & P4 & P0) & P0" 1;
THEOREMS:=("req",(termtosequent(parseprop("(a1 eq a2 & P3 & P0) & (Real(a1) & P1 & P0) & (Real(a2) & P2 & P0) & P0 -> (a1 = a2 & P4 & P0) & P0")),hd(!PROOFSTACK)))::(!THEOREMS);
PROOFSTACK:=nil;
td "req";
pushnode 9 " (a1 + 0 = a2 + 0 & P28 & P22 & P0) & P0 -> (a1 + 0 = a2 + 0 & P32 & P20 & P16 & P12 & P7 & P3 & P0) & P0" 0;
pushnode 8 " (a2 + 0 = a1 + 0 & P23 & P17 & P13 & P9 & P8 & P4 & P0) & P0 -> (a2 + 0 = a1 + 0 & P26 & P22 & P0) & P0" 0;
pushnode 7 "(( a2 + 0 = a1 + 0 -> a1 + 0 = a2 + 0) & P22 & P0) & (a2 + 0 = a1 + 0 & P17 & P13 & P9 & P8 & P4 & P0) & P0 -> (a1 + 0 = a2 + 0 & P20 & P16 & P12 & P7 & P3 & P0) & P0" 2;
pushreference 6 "P0 -> ((a2 + 0 = a1 + 0 -> a1 + 0 = a2 + 0) & P21 & P0) & P0" "symm";
pushnode 5 " (a2 + 0 = a1 + 0 & P17 & P13 & P9 & P8 & P4 & P0) & P0 -> (a1 + 0 = a2 + 0 & P20 & P16 & P12 & P7 & P3 & P0) & P0" 2;
pushnode 4 "(a2 + 0 = a1 + 0 & P13 & P9 & P8 & P4 & P0) & P0 -> (a1 eq a2 & P16 & P12 & P7 & P3 & P0) & P0" 1;
pushnode 3 "(a2 eq a1 & P9 & P8 & P4 & P0) & P0 -> (a1 eq a2 & P12 & P7 & P3 & P0) & P0" 1;
pushnode 2 "P0 -> (~a2 eq a1 & P8 & P4 & P0) & (a1 eq a2 & P7 & P3 & P0) & P0" 1;
pushnode 1 "(~a1 eq a2 & P3 & P0) & P0 -> (~a2 eq a1 & P4 & P0) & P0" 1;
THEOREMS:=("negeqsymm",(termtosequent(parseprop(" (~a1 eq a2 & P3 & P0) & P0 -> (~a2 eq a1 & P4 & P0) & P0")),hd(!PROOFSTACK)))::(!THEOREMS);
PROOFSTACK:=nil;
td "negeqsymm";
pushnode 4 "(~0 eq 1 & P15 & P7 & P3 & P0) & P0 -> (~0 eq 1 & P16 & P8 & P4 & P0) & P0" 0;
pushnode 10 "(0 <= 1 & P24 & P22 & P18 & P0) & P0 -> (0 <= 1 & P28 & P12 & P8 & P4 & P0) & P0" 0;
pushnode 9 "(1 * 1 = 1 & P22 & P0) & (0 <= 1 * 1 & P18 & P0) &  (Real(1) & P10 & P6 & P2 & P0) & P0 -> (0 <= 1 & P12 & P8 & P4 & P0) & P0" 1;
pushnode 8 "( Real(1) & P10 & P6 & P2 & P0) & (0 <= 1 * 1 & P18 & P0) & P0 ->  (Real(1) & P21 & P0) & (0 <= 1 & P12 & P8 & P4 & P0) & P0" 0;
pushreference 7 "(Real(1) & P19 & P0) & P0 -> (1 * 1 = 1 & P20 & P0) & P0" "mid";
pushnode 6 " (0 <= 1 * 1 & P18 & P0) & (Real(1) & P10 & P6 & P2 & P0) & P0 -> (0 <= 1 & P12 & P8 & P4 & P0) & P0" 3;
pushreference 5 "P0 -> (0 <= 1 * 1 & P17 & P0) & P0" "thm 3.2.iv";
pushnode 3 "( Real(1) & P10 & P6 & P2 & P0) & P0 -> (0 <= 1 & P12 & P8 & P4 & P0) & P0" 2;
pushnode 2 "(Real(1) & P6 & P2 & P0) & (~0 eq 1 & P7 & P3 & P0) & P0 -> ((0 <= 1 & ~0 eq 1) & P8 & P4 & P0) & P0" 2;
pushnode 1 "(Real(1) & P2 & P0) & (~0 eq 1 & P3 & P0) & P0 -> (0 < 1 & P4 & P0) & P0" 1;
THEOREMS:=("thm 3.2.v",(termtosequent(parseprop("(Real(1) & P2 & P0) & ( ~0 eq 1 & P3 & P0) & P0 -> (0 < 1 & P4 & P0) & P0")),hd(!PROOFSTACK)))::(!THEOREMS);
PROOFSTACK:=nil;
td "thm 3.2.v";
pushnode 45 " (a1 + 0 = 0 + 0 & P138 & P129 & P0) & P0 -> (a1 + 0 = 0 + 0 & P145 & P127 & P120 & P108 & P92 & P80 & P74 & P60 & P48 & P36 & P31 & P26 & P20 & P14 & P2 & P0) & P0" 0;
pushnode 44 " (a1 = 0 & P131 & P122 & P115 & P114 & P103 & P112 & P87 &  P102 & P84 & P94 & P76 & P71 & P69 & P57 & P62 & P45 & P33 & P29 & P24 & P18 & P12 & P6 & P0) & P0 -> (a1 = 0 & P136 & P129 & P0) & P0" 0;
pushnode 43 "( (a1 = 0 -> a1 + 0 = 0 + 0) & P129 & P0) & (a1 = 0 & P122 & P115 & P114 & P103 & P112 & P87 & P102 & P84 & P94 & P76 & P71 & P69 & P57 & P62 & P45 & P33 & P29 & P24 & P18 & P12 & P6 & P0) & P0 -> ( a1 + 0 = 0 + 0 & P127 & P120 & P108 & P92 & P80 & P74 & P60 & P48 & P36 & P31 & P26 & P20 & P14 & P2 & P0) & P0" 2;
pushreference 42 "P0 -> ( (a1 = 0 -> a1 + 0 = 0 + 0) & P128 & P0) & P0" "aeq";
pushnode 41 "(a1 = 0 & P122 & P115 & P114 & P103 & P112 & P87 & P102 & P84 & P94 & P76 & P71 & P69 & P57 & P62 & P45 & P33 & P29 & P24 & P18 & P12 & P6 & P0) & P0 -> (a1 + 0 = 0 + 0 & P127 & P120 & P108 & P92 & P80 & P74 & P60 & P48 & P36 & P31 & P26 & P20 & P14 & P2 & P0) & P0" 2;
pushnode 40 "(a1 * 0 = 0 & P115 & P103 & P87 & P84 & P76 & P71 & P69 & P57 & P62 & P45 & P33 & P29 & P24 & P18 & P12 & P6 & P0) & (a1 = a1 * 0 & P114 & P112 & P102 & P94 & P0) & P0 -> (a1 + 0 = 0 + 0 & P120 & P108 & P92 & P80 & P74 & P60 & P48 & P36 & P31 & P26 & P20 & P14 & P2 & P0) & P0" 1;
pushnode 39 "(a1 * 1 = a1 & P112 & P0) & (a1 * 1 = a1 * 0 & P102 & P94 & P0) & (a1 * 0 = 0 & P103 & P87 & P84 & P76 & P71 & P69 & P57 & P62 & P45 & P33 & P29 & P24 & P18 & P12 & P6 & P0) &  (Real(a1) & P106 & P90 & P78 & P72 & P58 & P46 & P34 & P30 & P25 & P19 & P13 & P1 & P0) & P0 -> (a1 + 0 = 0 + 0 & P108 & P92 & P80 & P74 & P60 & P48 & P36 & P31 & P26 & P20 & P14 & P2 & P0) & P0" 1;
pushnode 38 "(Real(a1) & P106 & P90 & P78 & P72 & P58 & P46 & P34 & P30 & P25 & P19 & P13 & P1 & P0) & (a1 * 1 = a1 * 0 & P102 & P94 & P0) & (a1 * 0 = 0 & P103 & P87 & P84 & P76 & P71 & P69 & P57 & P62 & P45 & P33 & P29 & P24 & P18 & P12 & P6 & P0) & P0 -> (Real(a1) & P111 & P0) & (a1 + 0 = 0 + 0 & P108 & P92 & P80 &  P74 & P60 & P48 & P36 & P31 & P26 & P20 & P14 & P2 & P0) & P0" 0;
pushreference 37 "(Real(a1) & P109 & P0) & P0 -> (a1 * 1 = a1 & P110 & P0) & P0" "mid";
pushnode 36 "(a1 * 1 = a1 * 0 & P102 & P94 & P0) & (a1 * 0 = 0 & P103 & P87 & P84 & P76 & P71 & P69 & P57 & P62 & P45 & P33 & P29 & P24 & P18 & P12 & P6 & P0) &  (Real(a1) & P106 & P90 & P78 & P72 & P58 & P46 & P34 & P30 & P25 & P19 & P13 & P1 & P0) & P0 -> (a1 + 0 = 0 + 0 & P108 & P92 & P80 & P74 & P60 & P48 & P36 & P31 & P26 & P20 & P14 & P2 & P0) & P0" 3;
pushnode 35 "(1 = 0 & P96 & P88 & P84 & P76 & P71 & P69 & P57 & P62 & P45 & P33 & P29 & P24 & P18 & P12 & P6 & P0) & P0 -> (1 = 0 & P100 & P94 & P0) & P0" 0;
pushnode 34 "((1 = 0 -> a1 * 1 = a1 * 0) & P94 & P0) & (a1 * 0 = 0 & P87 & P84 & P76 & P71 & P69 & P57 & P62 & P45 & P33 & P29 & P24 & P18 & P12 & P6 & P0) & (1 = 0 & P88 & P84 & P76 & P71 & P69 & P57 & P62 & P45 & P33 & P29 & P24 & P18 & P12 & P6 & P0) &  (Real(a1) & P90 & P78 & P72 & P58 & P46 & P34 & P30 & P25 & P19 & P13 & P1 & P0) & P0 -> (a1 + 0 = 0 + 0 & P92 & P80 & P74 & P60 & P48 & P36 & P31 & P26 & P20 & P14 & P2 & P0) & P0" 2;
pushreference 33 "P0 -> ((1 = 0 -> a1 * 1 = a1 * 0) & P93 & P0) & P0" "meql";
pushnode 32 "(a1 * 0 = 0 & P87 & P84 & P76 & P71 & P69 & P57 & P62 & P45 & P33 & P29 & P24 & P18 & P12 & P6 & P0) & (1 = 0 & P88 & P84 & P76 & P71 & P69 & P57 & P62 & P45 & P33 & P29 & P24 & P18 & P12 & P6 & P0) &  (Real(a1) & P90 & P78 & P72 & P58 & P46 & P34 & P30 & P25 & P19 & P13 & P1 & P0) & P0 ->  (a1 + 0 = 0 + 0 & P92 & P80 & P74 & P60 & P48 & P36 & P31 & P26 & P20 & P14 & P2 & P0) & P0" 2;
pushnode 29 "(a1 * 0 = 0 & P84 & P0) & (1 = a1 * 0 & P76 & P71 & P69 & P57 & P62 & P45 & P33 & P29 & P24 & P18 & P12 & P6 & P0) & (Real(a1) & P78 & P72 & P58 & P46 & P34 & P30 & P25 & P19 & P13 & P1 & P0) & P0 -> (a1 + 0 = 0 + 0 & P80 & P74 & P60 & P48 & P36 & P31 & P26 & P20 & P14 & P2 & P0) & P0" 1;
pushnode 31 "(Real(0) & P86 & P0) & (1 = a1 * 0 & P76 & P71 & P69 & P57 & P62 & P45 & P33 & P29 & P24 & P18 & P12 & P6 & P0) & (Real(a1) & P78 & P72 & P58 & P46 & P34 & P30 & P25 & P19 & P13 & P1 & P0) & P0 -> (Real(0) & P83 & P0) & (a1 + 0 = 0 + 0 & P80 & P74 & P60 & P48 & P36 & P31 & P26 & P20 & P14 & P2 & P0) & P0" 0;
pushreference 30 "P0 -> (Real(0) & P85 & P0) & P0" "zero";
pushnode 28 " (1 = a1 * 0 & P76 & P71 & P69 & P57 & P62 & P45 & P33 & P29 & P24 & P18 & P12 & P6 & P0) & (Real(a1) & P78 & P72 & P58 & P46 & P34 & P30 & P25 & P19 & P13 & P1 & P0) & P0 -> (Real(0) & P83 & P0) & (a1 + 0 = 0 + 0 & P80 & P74 & P60 & P48 & P36 & P31 & P26 & P20 & P14 & P2 & P0) & P0" 2;
pushreference 27 "(Real(0) & P81 & P0) & P0 -> (a1 * 0 = 0 & P82 & P0) & P0" "thm 3.1.ii";
pushnode 26 "(1 = a1 * 0 & P76 & P71 & P69 &  P57 & P62 & P45 & P33 & P29 & P24 & P18 & P12 & P6 & P0) & (Real(a1) & P78 & P72 & P58 & P46 & P34 & P30 & P25 & P19 & P13 & P1 & P0) & P0 -> (a1 + 0 = 0 + 0 & P80 &  P74 & P60 & P48 & P36 & P31 & P26 & P20 & P14 & P2 & P0) & P0" 3;
pushnode 25 " (a1 * /(a1) = 1 & P71 & P57 & P45 & P33 & P29 & P24 & P18 & P12 & P6 & P0) & (a1 * /(a1) = a1 * 0 & P69 & P62 & P0) & (Real(a1) & P72 & P58 & P46 & P34 & P30 & P25 & P19 & P13 & P1 & P0) & P0 -> (a1 + 0 = 0 + 0 & P74 & P60 & P48 & P36 & P31 & P26 & P20 & P14 & P2 & P0) & P0" 1;
pushnode 24 " (/(a1) = 0 & P63 & P56 & P52 & P44 & P40 & P32 & P28 & P23 &  P17 & P16 & P4 & P0) & P0 -> (/(a1) = 0 & P67 & P62 & P0) & P0" 0;
pushnode 23 " ((/(a1) = 0 -> a1 * /(a1) = a1 * 0) & P62 & P0) & (/(a1) = 0 & P56 & P52 & P44 & P40 & P32 & P28 & P23 & P17 & P16 & P4 & P0) & (a1 * /(a1) = 1 & P57 & P45 & P33 & P29 & P24 & P18 & P12 & P6 & P0) & (Real(a1) & P58 & P46 & P34 & P30 & P25 & P19 & P13 & P1 & P0) & P0 -> (a1 + 0 = 0 + 0 & P60 & P48 & P36 & P31 & P26 & P20 & P14 & P2 & P0) & P0" 2;
pushreference 22 "P0 -> ((/(a1) = 0 -> a1 * /(a1) = a1 * 0) &  P61 & P0) & P0" "meql";
pushnode 21 "(/(a1) = 0 & P56 & P52 & P44 & P40 & P32 & P28 & P23 & P17 & P16 & P4 & P0) & (a1 * /(a1) = 1 & P57 & P45 & P33 & P29 & P24 & P18 &  P12 & P6 & P0) & (Real(a1) & P58 & P46 & P34 & P30 & P25 & P19 & P13 & P1 & P0) & P0 -> (a1 + 0 = 0 + 0 & P60 & P48 & P36 & P31 & P26 & P20 & P14 & P2 & P0) & P0" 2;
pushnode 18 "(0 + 0 = 0 & P52 & P0) & (/(a1) = 0 + 0 & P44 & P40 & P32 &  P28 & P23 & P17 & P16 & P4 & P0) & ( a1 * /(a1) = 1 & P45 & P33 & P29 & P24 & P18 & P12 & P6 & P0) & ( Real(a1) & P46 & P34 & P30 & P25 & P19 & P13 & P1 & P0) & P0 -> (a1 + 0 = 0 + 0 & P48 & P36 & P31 & P26 & P20 &  P14 & P2 & P0) & P0" 1;
pushnode 20 " (Real(0) & P54 & P0) & (/(a1) = 0 + 0 & P44 & P40 & P32 & P28 & P23 & P17 & P16 & P4 & P0) & (a1 * /(a1) = 1 & P45 & P33 & P29 & P24 & P18 & P12 & P6 & P0) & (Real(a1) & P46 & P34 & P30 & P25 & P19 & P13 & P1 & P0) & P0 -> (Real(0) & P51 & P0) & (a1 + 0 = 0 + 0 & P48 & P36 & P31 & P26 & P20 & P14 & P2 & P0) & P0" 0;
pushreference 19 "P0 -> (Real(0) & P53 & P0) & P0" "zero";
pushnode 17 "(/(a1) = 0 + 0 & P44 & P40 & P32 & P28 & P23 & P17 & P16 & P4 & P0) & (a1 * /(a1) = 1 & P45 & P33 & P29 & P24 & P18 & P12 & P6 & P0) & (Real(a1) & P46 & P34 & P30 & P25 & P19 & P13 & P1 & P0) & P0 -> ( Real(0) & P51 & P0) & (a1 + 0 = 0 + 0 & P48 & P36 & P31 & P26 & P20 & P14 & P2 & P0) & P0" 2;
pushreference 16 "(Real(0) & P49 & P0) & P0 -> (0 + 0 = 0 & P50 & P0) & P0" "aid";
pushnode 15 "(/(a1) = 0 + 0 & P44 & P40 & P32 & P28 & P23 & P17 & P16 & P4 & P0) & (a1 * /(a1) = 1 & P45 & P33 & P29 & P24 & P18 & P12 & P6 & P0) & (Real(a1) & P46 & P34 & P30 & P25 & P19 & P13 & P1 & P0) & P0 -> (a1 + 0 =  0 + 0 & P48 & P36 & P31 & P26 & P20 & P14 & P2 & P0) & P0" 3;
pushnode 12 "(/(a1) + 0 = /(a1) & P40 & P0) &  (/(a1) + 0 = 0 + 0 & P32 & P28 & P23 & P17 & P16 & P4 & P0) &  (a1 * /(a1) = 1 & P33 & P29 & P24 & P18 & P12 & P6 & P0) & (Real(a1) & P34 & P30 & P25 & P19 & P13 & P1 & P0) & P0 -> (a1 + 0 = 0 + 0 & P36 & P31 & P26 & P20 & P14 & P2 & P0) & P0" 1;
pushnode 14 "(Real(/(a1)) & P42 & P0) & (/(a1) + 0 = 0 + 0 & P32 & P28 & P23 & P17 & P16 & P4 & P0) & (a1 * /(a1) = 1 & P33 & P29 & P24 & P18 & P12 & P6 & P0) &  (Real(a1) & P34 & P30 & P25 & P19 & P13 & P1 & P0) & P0 -> ( Real(/(a1)) & P39 & P0) &  (a1 + 0 = 0 + 0 & P36 & P31 & P26 & P20 & P14 & P2 & P0) & P0" 0;
pushreference 13 "P0 -> (Real(/(a1)) & P41 & P0) & P0" "rinv";
pushnode 11 "(/(a1) + 0 = 0 + 0 & P32 & P28 & P23 & P17 & P16 & P4 & P0) & (a1 * /(a1) = 1 & P33 & P29 & P24 & P18 & P12 &  P6 & P0) &  (Real(a1) & P34 & P30 & P25 & P19 & P13 & P1 & P0) & P0 -> (Real(/(a1)) & P39 & P0) & (a1 + 0 =  0 + 0 & P36 & P31 & P26 & P20 & P14 & P2 & P0) & P0" 2;
pushreference 10 "(Real(/(a1)) & P37 & P0) & P0 -> (/(a1) + 0 = /(a1) & P38 & P0) & P0" "aid";
pushnode 9 "(/(a1) + 0 = 0 + 0 & P32 & P28 &  P23 & P17 & P16 & P4 & P0) & (a1 * /(a1) = 1 & P33 & P29 & P24 & P18 & P12 & P6 & P0) & (Real(a1) & P34 & P30 & P25 & P19 & P13 & P1 & P0) & P0 -> (a1 + 0 = 0 + 0 & P36 & P31 & P26 & P20 & P14 & P2 & P0) & P0" 3;
pushnode 8 " (/(a1) eq 0 & P28 & P23 & P17 & P16 & P4 & P0) & (a1 * /(a1) = 1 & P29 & P24 & P18 & P12 & P6 & P0) & (Real(a1) & P30 & P25 & P19 & P13 & P1 & P0) & P0 -> (a1 + 0 = 0 + 0 & P31 & P26 & P20 & P14 & P2 & P0) & P0" 1;
pushnode 7 "(/(a1) eq 0 & P23 & P17 & P16 & P4 & P0) & ( a1 * /(a1) = 1 & P24 & P18 & P12 & P6 & P0) & (Real(a1) & P25 & P19 & P13 & P1 & P0) & P0 -> (a1 eq 0 & P26 & P20 & P14 & P2 & P0) & P0" 1;
pushnode 6 " (~a1 eq 0 & P20 & P14 & P2 & P0) & (/(a1) eq 0 & P17 & P16 & P4 & P0) & (a1 * /(a1) = 1 & P18 & P12 & P6 & P0) & (Real(a1) & P19 & P13 & P1 & P0) & P0 -> P0" 1;
pushnode 5 "(a1 * /(a1) = 1 & P12 & P6 & P0) & (Real(a1) & P13 & P1 & P0) & (~a1 eq 0 & P14 & P2 & P0) & P0 -> (~/(a1) eq 0 & P16 & P4 & P0) & P0" 1;
pushnode 4 "(~a1 eq 0 & P8 & P2 & P0) & P0 -> (~a1 eq 0 & P10 & P6 & P0) & P0" 0;
pushnode 3 "((~a1 eq 0 -> a1 * /(a1) = 1) & P6 & P0) & (Real(a1) & P1 & P0) & (~a1 eq 0 & P2 & P0) & P0 -> ( ~/(a1) eq 0 & P4 & P0) & P0" 2;
pushreference 2 "P0 -> ((~a1 eq 0 -> a1 * /(a1) = 1) & P5 & P0) & P0" "minv";
pushnode 1 " (Real(a1) & P1 & P0) & (~a1 eq 0 & P2 & P0) & P0 -> (~/(a1) eq 0 & P4 & P0) & P0" 2;
THEOREMS:=("lemma 1.1",(termtosequent(parseprop("(Real(a1) & P1 & P0) & (~a1 eq 0 & P2 & P0) & P0 -> (~/(a1) eq 0 & P4 & P0) & P0")),hd(!PROOFSTACK)))::(!THEOREMS);
PROOFSTACK:=nil;
td "lemma 1.1";
pushnode 36 "(/(/(a1)) = a1 & P89 & P87 & P79 & P77 & P71 & P67 & P64 & P55 & P62 & P48 & P57 & P37 & P33 & P26 & P24 & P19 & P13 & P14 & P7 & P5 & P0) & P0 -> (/(/(a1)) = a1 & P93 & P83 & P75 & P69 & P60 & P40 & P29 & P22 & P17 & P3 & P0) & P0" 0;
pushnode 35 " (a1 * 1 = a1 & P87 & P0) &  (/(/(a1)) = a1 * 1 & P79 & P77 & P71 & P67 & P64 & P55 & P62 & P48 & P57 & P37 & P33 & P26 & P24 & P19 & P13 & P14 & P7 & P5 & P0) & (Real(a1) & P80 & P72 & P65 & P58 & P38 & P27 & P20 & P15 & P1 & P0) & P0 -> (/(/(a1)) = a1 & P83 & P75 & P69 & P60 & P40 & P29 & P22 & P17 & P3 & P0) & P0" 1;
pushnode 34 "(Real(a1) & P80 & P72 & P65 & P58 & P38 & P27 & P20 & P15 &  P1 & P0) &  (/(/(a1)) = a1 * 1 & P79 & P77 & P71 & P67 & P64 & P55 & P62 & P48 & P57 & P37 & P33 & P26 & P24 & P19 & P13 & P14 & P7 & P5 & P0) & P0 -> (Real(a1) & P86 & P0) & (/(/(a1)) = a1 & P83 & P75 & P69 & P60 & P40 & P29 & P22 & P17 & P3 & P0) & P0" 0;
pushreference 33 "(Real(a1) & P84 & P0) & P0 -> (a1 * 1 = a1 & P85 & P0) & P0" "mid";
pushnode 32 " (/(/(a1)) = a1 * 1 & P79 & P77 & P71 & P67 & P64 & P55 & P62 & P48 & P57 & P37 & P33 & P26 & P24 & P19 & P13 & P14 & P7 & P5 & P0) & (Real(a1) & P80 & P72 & P65 & P58 & P38 & P27 & P20 & P15 & P1 & P0) & P0 -> (/(/(a1)) = a1 & P83 & P75 & P69 & P60 & P40 &  P29 & P22 & P17 & P3 & P0) & P0" 3;
pushnode 31 " (1 * a1 = a1 * 1 & P77 & P0) & (/(/(a1)) = 1 * a1 & P71 & P67 & P64 & P55 & P62 & P48 & P57 & P37 & P33 & P26 & P24 & P19 & P13 & P14 & P7 & P5 & P0) & (Real(a1) & P72 & P65 & P58 & P38 & P27 & P20 & P15 & P1 & P0) & P0 -> (/(/(a1)) = a1 & P75 & P69 & P60 & P40 & P29 & P22 & P17 & P3 & P0) & P0" 1;
pushreference 30 "P0 -> (1 * a1 = a1 * 1 & P76 & P0) & P0" "mcom";
pushnode 29 "(/(/(a1)) = 1 * a1 & P71 & P67 & P64 & P55 & P62 & P48 & P57 & P37 & P33 & P26 & P24 & P19 & P13 & P14 & P7 & P5 & P0) & (Real(a1) & P72 & P65 & P58 & P38 & P27 & P20 & P15 & P1 & P0) & P0 -> (/(/(a1)) = a1 & P75 & P69 & P60 & P40 & P29 & P22 & P17 & P3 & P0) & P0" 2;
pushnode 28 "(/(a1) * /(/(a1)) = 1 & P67 & P55 & P48 & P0) &  (/(/(a1)) = [/(a1) * /(/(a1))] * a1 & P64 & P62 & P57 & P37 & P33 & P26 & P24 & P19 & P13 & P14 & P7 & P5 & P0) &  (Real(a1) & P65 & P58 & P38 & P27 & P20 & P15 & P1 & P0) & P0 -> (/(/(a1)) = a1 & P69 & P60 & P40 & P29 & P22 & P17 & P3 & P0) & P0" 1;
pushnode 27 " (a1 * /(a1) * /(/(a1)) = [/(a1) * /(/(a1))] * a1 & P62 & P0) & (/(/(a1)) = a1 * /(a1) * /(/(a1)) & P57 & P37 & P33 & P26 & P24 & P19 & P13 & P14 & P7 & P5 & P0) & (Real(a1) & P58 & P38 & P27 & P20 & P15 & P1 & P0) & (/(a1) * /(/(a1)) = 1 & P55 & P48 & P0) & P0 -> (/(/(a1)) = a1 & P60 & P40 & P29 & P22 & P17 & P3 & P0) & P0" 1;
pushreference 26 "P0 -> (a1 * /(a1) * /(/(a1)) = [/(a1) * /(/(a1))] * a1 & P61 & P0) & P0" "mcom";
pushnode 25 " (/(a1) * /(/(a1)) = 1 & P55 & P48 & P0) & (/(/(a1)) = a1 * /(a1) * /(/(a1)) & P57 & P37 & P33 & P26 & P24 & P19 & P13 & P14 & P7 & P5 & P0) & (Real(a1) & P58 & P38 & P27 & P20 & P15 & P1 & P0) & P0 -> (/(/(a1)) = a1 & P60 & P40 & P29 & P22 & P17 & P3 & P0) & P0" 2;
pushnode 24 "(~/(a1) eq 0 & P49 & P46 & P0) & P0 -> (~/(a1) eq 0 & P53 & P48 & P0) & P0" 0;
pushnode 23 " ((~/(a1) eq 0 -> /(a1) * /(/(a1)) = 1) & P48 & P0) & (~/(a1) eq 0 & P46 & P0) & ( /(/(a1)) = a1 * /(a1) * /(/(a1)) & P37 & P33 & P26 & P24 & P19 & P13 & P14 & P7 & P5 & P0) & (Real(a1) & P38 & P27 & P20 & P15 & P1 & P0) & (~a1 eq 0 & P39 & P28 & P21 & P16 & P2 & P0) & P0 -> (/(/(a1)) = a1 & P40 & P29 & P22 & P17 & P3 & P0) & P0" 2;
pushreference 22 "P0 -> ((~/(a1) eq 0 -> /(a1) * /(/(a1)) = 1) & P47 & P0) & P0" "minv";
pushnode 21 "(~/(a1) eq 0 & P46 & P0) & (/(/(a1)) = a1 * /(a1) * /(/(a1)) & P37 & P33 & P26 & P24 & P19 & P13 & P14 & P7 & P5 & P0) & (Real(a1) & P38 & P27 & P20 & P15 & P1 & P0) & (~a1 eq 0 & P39 & P28 & P21 & P16 & P2 & P0) & P0 -> (/(/(a1)) = a1 & P40 & P29 & P22 & P17 & P3 & P0) & P0" 2;
pushnode 20 " (~a1 eq 0 & P39 & P28 & P21 & P16 & P2 & P0) & (/(/(a1)) = a1 * /(a1) * /(/(a1)) & P37 & P33 & P26 & P24 & P19 & P13 & P14 & P7 & P5 & P0) & (Real(a1) & P38 & P27 & P20 & P15 & P1 & P0) & P0 -> (~a1 eq 0 & P45 & P0) & (/(/(a1)) = a1 & P40 & P29 & P22 & P17 & P3 & P0) & P0" 0;
pushnode 19 " (Real(a1) & P38 & P27 & P20 & P15 & P1 & P0) & (~a1 eq 0 & P39 &  P28 & P21 & P16 & P2 & P0) & (/(/(a1)) = a1 * /(a1) * /(/(a1)) & P37 & P33 & P26 & P24 & P19 & P13 & P14 & P7 & P5 & P0) & P0 -> (Real(a1) & P44 & P0) & (/(/(a1)) = a1 & P40 & P29 & P22 & P17 & P3 & P0) & P0" 0;
pushreference 18 " (Real(a1) & P41 & P0) & (~a1 eq 0 & P42 & P0) & P0 -> (~/(a1) eq 0 & P43 & P0) & P0" "lemma 1.1";
pushnode 17 "(/(/(a1)) = a1 * /(a1) * /(/(a1)) & P37 & P33 & P26 & P24 & P19 & P13 & P14 & P7 & P5 & P0) & (Real(a1) & P38 & P27 & P20 & P15 & P1 & P0) & (~a1 eq 0 & P39 & P28 & P21 & P16 & P2 & P0) & P0 -> (/(/(a1)) = a1 & P40 & P29 & P22 & P17 & P3 & P0) & P0" 4;
pushnode 14 "(/(/(a1)) * 1 = /(/(a1)) & P33 & P0) & ( /(/(a1)) * 1 = a1 * /(a1) * /(/(a1)) & P26 & P24 & P19 & P13 & P14 & P7 & P5 & P0) & ( Real(a1) & P27 & P20 & P15 & P1 & P0) & (~a1 eq 0 & P28 & P21 & P16 & P2 & P0) & P0 -> (/(/(a1)) = a1 & P29 & P22 & P17 & P3 & P0) & P0" 1;
pushnode 16 "(Real(/(/(a1))) & P35 & P0) & (/(/(a1)) * 1 = a1 * /(a1) * /(/(a1)) & P26 & P24 & P19 & P13 & P14 & P7 & P5 & P0) & (Real(a1) & P27 & P20 & P15 & P1 & P0) & (~a1 eq 0 & P28 & P21 & P16 & P2 & P0) & P0 -> (Real(/(/(a1))) & P32 & P0) &  (/(/(a1)) = a1 & P29 & P22 & P17 & P3 & P0) & P0" 0;
pushreference 15 "P0 -> (Real(/(/(a1))) & P34 & P0) & P0" "rinv";
pushnode 13 "(/(/(a1)) * 1 = a1 * /(a1) * /(/(a1)) & P26 & P24 & P19 & P13 & P14 & P7 & P5 & P0) & ( Real(a1) & P27 & P20 & P15 & P1 & P0) & (~a1 eq 0 & P28 & P21 & P16 & P2 & P0) & P0 -> (Real(/(/(a1))) & P32 & P0) & (/(/(a1)) = a1 & P29 & P22 & P17 & P3 & P0) & P0" 2;
pushreference 12 "(Real(/(/(a1))) & P30 & P0) & P0 -> (/(/(a1)) * 1 = /(/(a1)) & P31 & P0) & P0" "mid";
pushnode 11 "(/(/(a1)) * 1 = a1 * /(a1) * /(/(a1)) & P26 & P24 & P19 & P13 & P14 & P7 & P5 & P0) & (Real(a1) & P27 & P20 & P15 & P1 & P0) & (~a1 eq 0 & P28 & P21 & P16 & P2 & P0) & P0 -> (/(/(a1)) = a1 & P29 & P22 & P17 & P3 & P0) & P0" 3;
pushnode 10 "(1 * /(/(a1)) = /(/(a1)) * 1 & P24 & P0) & (1 * /(/(a1)) = a1 * /(a1) * /(/(a1)) & P19 & P13 & P14 & P7 & P5 & P0) & (Real(a1) & P20 & P15 & P1 & P0) &  (~a1 eq 0 & P21 & P16 & P2 & P0) & P0 ->  (/(/(a1)) = a1 & P22 & P17 & P3 & P0) & P0" 1;
pushreference 9 "P0 -> (1 * /(/(a1)) = /(/(a1)) * 1 & P23 & P0) & P0" "mcom";
pushnode 8 "(1 * /(/(a1)) = a1 * /(a1) * /(/(a1)) & P19 & P13 & P14 & P7 & P5 & P0) &  (Real(a1) & P20 & P15 & P1 & P0) & (~a1 eq 0 & P21 & P16 & P2 & P0) & P0 -> ( /(/(a1)) = a1 & P22 & P17 & P3 & P0) & P0" 2;
pushnode 7 "(a1 * /(a1) = 1 & P13 & P7 & P0) & ([a1 * /(a1)] * /(/(a1)) = a1 *  /(a1) * /(/(a1)) & P14 & P5 & P0) & (Real(a1) & P15 & P1 & P0) & (~a1 eq 0 & P16 & P2 & P0) & P0 -> (/(/(a1)) = a1 & P17 & P3 & P0) & P0" 1;
pushnode 6 "(~a1 eq 0 & P10 & P2 & P0) & P0 -> (~a1 eq 0 & P11 & P7 & P0) & P0" 0;
pushnode 5 " ((~a1 eq 0 -> a1 * /(a1) = 1) & P7 & P0) & ([a1 * /(a1)] * /(/(a1)) = a1 * /(a1) * /(/(a1)) & P5 & P0) & (Real(a1) & P1 & P0) & (~a1 eq 0 & P2 & P0) & P0 -> (/(/(a1)) = a1 & P3 & P0) & P0" 2;
pushreference 4 "P0 ->  ((~a1 eq 0 -> a1 * /(a1) = 1) & P6 & P0) & P0" "minv";
pushnode 3 "([a1 * /(a1)] * /(/(a1)) = a1 * /(a1) * /(/(a1)) & P5 & P0) & ( Real(a1) & P1 & P0) & (~a1 eq 0 & P2 & P0) & P0 -> (/(/(a1)) = a1 & P3 & P0) & P0" 2;
pushreference 2 "P0 -> ([a1 * /(a1)] * /(/(a1)) = a1 * /(a1) * /(/(a1)) & P4 & P0) & P0" "mas";
pushnode 1 "(Real(a1) & P1 & P0) & (~a1 eq 0 & P2 & P0) & P0 -> (/(/(a1)) = a1 & P3 & P0) & P0" 2;
THEOREMS:=("lemma 1.2",(termtosequent(parseprop("(Real(a1) & P1 & P0) & (~a1 eq 0 & P2 & P0) & P0 -> (/(/(a1)) = a1 & P3 & P0) & P0")),hd(!PROOFSTACK)))::(!THEOREMS);
PROOFSTACK:=nil;
td "lemma 1.2";
pushnode 80 "(~0 eq /(a1) & P398 & P0) & (~/(a1) eq 0 & P390 & P0) & (~0 eq a1 & P35 & P21 & P14 & P7 & P1 & P0) & (Real(a1) & P37 & P23 & P16 & P9 & P3 & P0) & P0 -> (~0 eq /(a1) & P40 & P26 & P19 & P12 & P6 & P0) & P0" 0;
pushnode 79 "(~/(a1) eq 0 & P390 & P0) & (~0 eq a1 & P35 & P21 & P14 & P7 & P1 & P0) & (Real(a1) & P37 & P23 & P16 & P9 & P3 & P0) & P0 -> (~/(a1) eq 0 & P397 & P0) & (~0 eq /(a1) & P40 & P26 & P19 & P12 & P6 & P0) & P0" 0;
pushreference 78 "(~/(a1) eq 0 & P395 & P0) & P0 -> (~0 eq /(a1) & P396 & P0) & P0" "negeqsymm";
pushnode 74 " (~/(a1) eq 0 & P390 & P0) & (~0 eq a1 & P35 & P21 & P14 & P7 & P1 & P0) & ( Real(a1) & P37 & P23 & P16 & P9 & P3 & P0) & P0 -> (~0 eq /(a1) & P40 & P26 & P19 & P12 & P6 & P0) & P0" 3;
pushnode 77 "( ~a1 eq 0 & P394 & P0) & (~0 eq a1 & P35 & P21 & P14 & P7 & P1 & P0) & (Real(a1) & P37 & P23 & P16 & P9 & P3 & P0) & P0 -> (~a1 eq 0 & P389 & P0) & (~0 eq /(a1) & P40 & P26 & P19 & P12 & P6 & P0) & P0" 0;
pushnode 76 " (~0 eq a1 & P35 & P21 & P14 & P7 & P1 & P0) & (Real(a1) & P37 & P23 & P16 & P9 & P3 & P0) & P0 -> ( ~0 eq a1 & P393 & P0) & (~a1 eq 0 & P389 & P0) & (~0 eq /(a1) & P40 & P26 & P19 & P12 & P6 & P0) & P0" 0;
pushreference 75 "(~0 eq a1 & P391 & P0) & P0 -> (~a1 eq 0 & P392 & P0) & P0" "negeqsymm";
pushnode 73 "(~0 eq a1 & P35 & P21 & P14 & P7 & P1 & P0) & (Real(a1) & P37 & P23 & P16 & P9 & P3 & P0) & P0 -> (~a1 eq 0 & P389 & P0) & (~0 eq /(a1) & P40 & P26 & P19 & P12 & P6 & P0) & P0" 3;
pushnode 72 "(Real(a1) & P37 & P23 & P16 & P9 & P3 & P0) & (~0 eq a1 & P35 & P21 & P14 & P7 & P1 & P0) & P0 -> (Real(a1) & P388 & P0) & (~0 eq /(a1) & P40 & P26 & P19 & P12 & P6 & P0) & P0" 0;
pushreference 71 "(Real(a1) & P385 & P0) & (~a1 eq 0 & P386 & P0) & P0 -> (~/(a1) eq 0 & P387 & P0) & P0" "lemma 1.1";
pushnode 6 " (~0 eq a1 & P35 & P21 & P14 & P7 & P1 & P0) & (Real(a1) & P37 & P23 & P16 & P9 & P3 & P0) & P0 -> ( ~0 eq /(a1) & P40 & P26 & P19 & P12 & P6 & P0) & P0" 4;
pushnode 70 "(0 <= /(a1) & P369 & P365 & P346 & P344 & P328 & P326 & P309 & P289 &  P291 & P273 & P259 & P244 & P246 & P229 & P199 & P197 & P184 & P182 & P145 & P132 & P0) & P0 -> ( 0 <= /(a1) & P384 & P361 & P342 & P322 & P303 & P271 & P257 & P210 & P195 & P156 & P128 & P118 & P83 & P63 & P54 & P33 & P26 & P19 & P12 & P6 & P0) & P0" 0;
pushnode 67 "( /(a1) * 1 = /(a1) & P365 & P0) & (0 <= /(a1) * 1 & P346 & P344 & P328 & P326 & P309 & P289 & P291 & P273 & P259 & P244 & P246 & P229 & P199 & P197 & P184 & P182 & P145 & P132 & P0) & P0 -> (0 <= /(a1) & P361 & P342 & P322 & P303 & P271 & P257 & P210 & P195 & P156 & P128 & P118 & P83 &  P63 & P54 & P33 & P26 & P19 & P12 & P6 & P0) & P0" 1;
pushnode 69 "( Real(/(a1)) & P367 & P0) & (0 <= /(a1) * 1 & P346 & P344 & P328 & P326 & P309 & P289 & P291 & P273 & P259 & P244 & P246 & P229 & P199 & P197 & P184 & P182 & P145 & P132 & P0) & P0 -> (Real(/(a1)) & P364 & P0) & (0 <= /(a1) & P361 &  P342 & P322 & P303 & P271 & P257 & P210 & P195 & P156 & P128 & P118 & P83 & P63 & P54 & P33 & P26 & P19 & P12 & P6 & P0) & P0" 0;
pushreference 68 "P0 ->  (Real(/(a1)) & P366 & P0) & P0" "rinv";
pushnode 66 "(0 <= /(a1) * 1 & P346 & P344 & P328 & P326 & P309 & P289 & P291 & P273 & P259 & P244 & P246 & P229 & P199 & P197 & P184 & P182 & P145 & P132 & P0) & P0 -> (Real(/(a1)) & P364 & P0) & (0 <= /(a1) & P361 & P342 & P322 & P303 & P271 & P257 & P210 & P195 & P156 & P128 & P118 & P83 & P63 & P54 & P33 & P26 & P19 & P12 &  P6 & P0) & P0" 2;
pushreference 65 "(Real(/(a1)) & P362 & P0) & P0 -> (/(a1) * 1 = /(a1) & P363 & P0) & P0" "mid";
pushnode 64 "(0 <= /(a1) * 1 & P346 & P344 & P328 & P326 & P309 & P289 & P291 & P273 & P259 & P244 & P246 & P229 & P199 & P197 & P184 & P182 & P145 & P132 & P0) & P0 ->  (0 <= /(a1) & P361 & P342 & P322 & P303 & P271 & P257 & P210 & P195 & P156 & P128 & P118 & P83 & P63 & P54 & P33 & P26 & P19 & P12 & P6 & P0) & P0" 3;
pushnode 63 " (1 * /(a1) = /(a1) * 1 & P344 & P0) & (0 <= 1 * /(a1) & P328 & P326 & P309 & P289 & P291 & P273 & P259 & P244 & P246 & P229 & P199 & P197 & P184 & P182 & P145 & P132 & P0) & P0 ->  (0 <= /(a1) & P342 & P322 & P303 & P271 & P257 & P210 & P195 & P156 & P128 & P118 & P83 & P63 & P54 & P33 & P26 & P19 & P12 & P6 & P0) & P0" 1;
pushreference 62 "P0 -> (1 * /(a1) = /(a1) * 1 & P343 & P0) & P0" "mcom";
pushnode 61 "(0 <= 1 * /(a1) & P328 & P326 & P309 & P289 &  P291 & P273 & P259 & P244 & P246 & P229 & P199 & P197 & P184 & P182 & P145 & P132 & P0) & P0 -> (0 <= /(a1) & P342 & P322 & P303 & P271 & P257 & P210 & P195 & P156 & P128 & P118 & P83 & P63 & P54 & P33 & P26 & P19 & P12 & P6 & P0) & P0" 2;
pushnode 60 " (a1 * 0 = 0 & P326 & P0) & (a1 * 0 <= 1 * /(a1) & P309 & P289 & P291 & P273 & P259 &  P244 & P246 & P229 & P199 & P197 & P184 & P182 & P145 & P132 & P0) & (Real(0) & P316 & P298 & P266 & P253 & P206 & P191 & P152 & P124 & P115 & P80 & P60 & P51 & P32 & P25 & P18 & P11 & P5 & P0) & P0 -> (0 <= /(a1) & P322 & P303 & P271 & P257 & P210 & P195 & P156 & P128 & P118 & P83 & P63 & P54 & P33 & P26 & P19 & P12 & P6 & P0) & P0" 1;
pushnode 59 " (Real(0) & P316 & P298 & P266 & P253 & P206 & P191 & P152 & P124 & P115 & P80 & P60 & P51 & P32 & P25 & P18 & P11 & P5 & P0) & (a1 * 0 <= 1 * /(a1) & P309 & P289 & P291 & P273 & P259 & P244 & P246 & P229 & P199 & P197 & P184 & P182 & P145 & P132 & P0) & P0 -> ( Real(0) & P325 & P0) & (0 <= /(a1) & P322 & P303 & P271 & P257 & P210 & P195 & P156 & P128 & P118 & P83 & P63 & P54 & P33 & P26 & P19 & P12 & P6 & P0) & P0" 0;
pushreference 58 "(Real(0) & P323 & P0) & P0 -> (a1 * 0 = 0 & P324 & P0) & P0" "thm 3.1.ii";
pushnode 57 " (a1 * 0 <= 1 * /(a1) & P309 & P289 & P291 & P273 & P259 & P244 & P246 & P229 & P199 & P197 & P184 & P182 & P145 & P132 & P0) & (Real(0) & P316 & P298 & P266 & P253 & P206 & P191 & P152 & P124 & P115 & P80 & P60 & P51 & P32 & P25 & P18 & P11 & P5 & P0) & P0 -> (0 <= /(a1) & P322 & P303 & P271 & P257 & P210 & P195 & P156 & P128 & P118 & P83 & P63 & P54 & P33 & P26 & P19 & P12 & P6 & P0) & P0" 3;
pushnode 53 "(a1 * /(a1) = 1 & P289 & P273 & P0) & (a1 * 0 <= [a1 * /(a1)] * /(a1) & P291 & P259 & P244 & P246 & P229 & P199 & P197 & P184 & P182 & P145 & P132 & P0) & (Real(0) & P298 & P266 & P253 & P206 & P191 & P152 & P124 & P115 & P80 & P60 & P51 & P32 & P25 & P18 & P11 & P5 & P0) & P0 -> (0 <= /(a1) & P303 & P271 & P257 & P210 & P195 & P156 & P128 & P118 & P83 & P63 & P54 & P33 & P26 & P19 & P12 & P6 & P0) & P0" 1;
pushnode 56 "(~a1 eq 0 & P307 & P0) & (~0 eq a1 & P284 & P268 & P255 & P208 & P193 & P154 & P126 & P117 & P82 & P62 & P53 & P28 & P21 & P14 & P7 & P1 & P0) & P0 -> (~a1 eq 0 & P287 & P273 & P0) & P0" 0;
pushnode 55 "(~0 eq a1 & P284 & P268 & P255 & P208 & P193 & P154 & P126 & P117 & P82 & P62 & P53 & P28 & P21 & P14 & P7 & P1 & P0) & P0 -> (~0 eq a1 & P306 & P0) & (~a1 eq 0 & P287 & P273 & P0) & P0" 0;
pushreference 54 "( ~0 eq a1 & P304 & P0) & P0 -> (~a1 eq 0 & P305 & P0) & P0" "negeqsymm";
pushnode 52 "(~0 eq a1 & P284 & P268 & P255 & P208 & P193 & P154 & P126 & P117 & P82 & P62 & P53 & P28 & P21 & P14 & P7 & P1 & P0) & P0 ->  (~a1 eq 0 & P287 & P273 & P0) & P0" 3;
pushnode 51 "((~a1 eq 0 -> a1 * /(a1) = 1) & P273 & P0) & (a1 * 0 <= [a1 * /(a1)] * /(a1) & P259 & P244 & P246 & P229 & P199 & P197 & P184 &  P182 & P145 & P132 & P0) & (Real(0) & P266 & P253 & P206 & P191 & P152 & P124 & P115 & P80 & P60 & P51 & P32 & P25 & P18 & P11 & P5 & P0) & (~0 eq a1 & P268 & P255 & P208 & P193 & P154 & P126 & P117 & P82 & P62 & P53 & P28 & P21 & P14 & P7 & P1 & P0) & P0 -> (0 <= /(a1) & P271 & P257 & P210 & P195 & P156 & P128 & P118 & P83 & P63 & P54 & P33 & P26 & P19 & P12 & P6 & P0) & P0" 2;
pushreference 50 "P0 ->  ((~a1 eq 0 -> a1 * /(a1) = 1) & P272 & P0) & P0" "minv";
pushnode 49 " (a1 * 0 <= [a1 * /(a1)] * /(a1) & P259 & P244 & P246 & P229 & P199 & P197 & P184 & P182 & P145 & P132 & P0) & (Real(0) & P266 & P253 & P206 & P191 & P152 & P124 & P115 & P80 & P60 & P51 & P32 & P25 & P18 & P11 & P5 & P0) &  (~0 eq a1 & P268 & P255 & P208 & P193 & P154 & P126 & P117 & P82 & P62 & P53 & P28 & P21 & P14 & P7 & P1 & P0) & P0 -> (0 <= /(a1) & P271 & P257 & P210 & P195 & P156 & P128 & P118 & P83 & P63 & P54 & P33 & P26 & P19 & P12 & P6 & P0) & P0" 2;
pushnode 48 "(a1 * /(a1) * /(a1) = [a1 * /(a1)] * /(a1) & P244 & P229 & P0) & (a1 * 0 <= a1 * /(a1) * /(a1) & P246 & P199 & P197 & P184 & P182 & P145 & P132 & P0) & (Real(0) & P253 & P206 & P191 & P152 & P124 & P115 & P80 & P60 & P51 & P32 & P25 & P18 & P11 & P5 & P0) & (~0 eq a1 & P255 & P208 & P193 & P154 & P126 & P117 & P82 & P62 & P53 & P28 & P21 & P14 & P7 & P1 & P0) & P0 -> (0 <= /(a1) & P257 & P210 & P195 & P156 & P128 & P118 & P83 & P63 & P54 & P33 & P26 & P19 & P12 & P6 & P0) & P0" 1;
pushnode 47 "( [a1 * /(a1)] * /(a1) = a1 * /(a1) * /(a1) & P230 & P227 & P0) & P0 -> ( [a1 * /(a1)] * /(a1) = a1 * /(a1) * /(a1) & P242 & P229 & P0) & P0" 0;
pushnode 46 " (( [a1 * /(a1)] * /(a1) = a1 * /(a1) * /(a1) -> a1 * /(a1) * /(a1) = [a1 * /(a1)] * /(a1)) & P229 & P0) & ([ a1 * /(a1)] * /(a1) = a1 * /(a1) * /(a1) & P227 & P0) & (a1 * 0 <= a1 * /(a1) * /(a1) & P199 & P197 & P184 & P182 & P145 & P132 & P0) & (Real(0) & P206 & P191 & P152 & P124 & P115 & P80 & P60 & P51 & P32 & P25 & P18 & P11 & P5 & P0) & (~0 eq a1 & P208 & P193 & P154 & P126 & P117 & P82 & P62 & P53 & P28 & P21 & P14 & P7 & P1 & P0) & P0 -> (0 <= /(a1) & P210 & P195 & P156 & P128 & P118 & P83 & P63 & P54 & P33 & P26 & P19 & P12 & P6 & P0) & P0" 2;
pushreference 45 "P0 -> (([a1 * /(a1)] * /(a1) = a1 * /(a1) * /(a1) -> a1 * /(a1) * /(a1) = [ a1 * /(a1)] * /(a1)) & P228 & P0) & P0" "symm";
pushnode 44 " ([a1 * /(a1)] * /(a1) = a1 * /(a1) * /(a1) &  P227 & P0) & (a1 * 0 <= a1 * /(a1) * /(a1) & P199 & P197 & P184 & P182 & P145 & P132 & P0) & (Real(0) & P206 & P191 & P152 & P124 & P115 & P80 & P60 & P51 & P32 & P25 & P18 & P11 & P5 & P0) & (~0 eq a1 & P208 & P193 & P154 & P126 & P117 & P82 & P62 & P53 & P28 & P21 & P14 & P7 & P1 & P0) & P0 -> (0 <= /(a1) & P210 & P195 & P156 & P128 & P118 & P83 & P63 & P54 & P33 & P26 & P19 & P12 & P6 & P0) & P0" 2;
pushreference 43 "P0 ->  ([a1 * /(a1)] * /(a1) = a1 * /(a1) * /(a1) & P226 & P0) & P0" "mas";
pushnode 41 "(a1 * 0 <= a1 * /(a1) * /(a1) & P199 & P197 & P184 & P182 & P145 & P132 & P0) & (Real(0) & P206 & P191 & P152 & P124 & P115 & P80 & P60 & P51 & P32 & P25 & P18 & P11 & P5 & P0) & (~0 eq a1 & P208 & P193 & P154 & P126 & P117 & P82 & P62 & P53 & P28 & P21 & P14 & P7 & P1 & P0) & P0 ->  (0 <= /(a1) &  P210 & P195 & P156 & P128 & P118 & P83 & P63 & P54 & P33 & P26 & P19 & P12 & P6 & P0) & P0" 2;
pushreference 40 "P0 ->  ([a1 * /(a1)] * /(a1) = /(a1) * a1 * /(a1) & P211 & P0) & P0" "mcom";
pushnode 39 "(a1 * 0 <= a1 * /(a1) * /(a1) & P199 & P197 & P184 & P182 & P145 & P132 & P0) & (Real(0) & P206 & P191 & P152 & P124 & P115 & P80 & P60 & P51 & P32 & P25 & P18 & P11 & P5 & P0) & (~0 eq a1 & P208 & P193 & P154 & P126 & P117 & P82 & P62 & P53 & P28 & P21 & P14 & P7 & P1 & P0) & P0 ->  (0 <= /(a1) &  P210 & P195 & P156 & P128 & P118 & P83 & P63 & P54 & P33 & P26 & P19 & P12 & P6 & P0) & P0" 2;
pushnode 38 " ([/(a1) * /(a1)] * a1 = a1 * /(a1) * /(a1) & P197 & P0) &  (a1 * 0 <= [/(a1) * /(a1)] * a1 & P184 & P182 & P145 & P132 & P0) &  (Real(0) & P191 & P152 & P124 & P115 & P80 & P60 & P51 & P32 & P25 & P18 & P11 & P5 & P0) &  (~0 eq a1 & P193 & P154 & P126 & P117 & P82 & P62 & P53 & P28 & P21 & P14 & P7 & P1 & P0) & P0 -> ( 0 <= /(a1) & P195 & P156 & P128 & P118 & P83 & P63 & P54 & P33 & P26 & P19 & P12 & P6 & P0) & P0" 1;
pushreference 37 "P0 -> ([/(a1) * /(a1)] * a1 = a1 * /(a1) * /(a1) & P196 & P0) & P0" "mcom";
pushnode 36 "(a1 * 0 <=  [/(a1) * /(a1)] * a1 & P184 & P182 & P145 & P132 & P0) & (Real(0) & P191 & P152 & P124 & P115 & P80 & P60 & P51 & P32 & P25 & P18 & P11 & P5 & P0) &  (~0 eq a1 & P193 & P154 & P126 & P117 & P82 & P62 & P53 & P28 & P21 & P14 & P7 & P1 & P0) & P0 -> (0 <= /(a1) & P195 & P156 & P128 & P118 & P83 & P63 & P54 & P33 & P26 & P19 & P12 & P6 & P0) & P0" 2;
pushnode 35 "(0 * a1 = a1 * 0 & P182 & P0) & ( 0 * a1 <= [/(a1) * /(a1)] * a1 & P145 & P132 & P0) &  (Real(0) & P152 & P124 & P115 & P80 & P60 & P51 & P32 & P25 & P18 & P11 & P5 & P0) & (~0 eq a1 & P154 & P126 & P117 & P82 & P62 & P53 & P28 & P21 & P14 & P7 & P1 & P0) & P0 -> (0 <= /(a1) & P156 & P128 & P118 & P83 & P63 & P54 & P33 & P26 & P19 & P12 & P6 & P0) & P0" 1;
pushreference 34 "P0 -> (0 * a1 = a1 * 0 & P181 & P0) & P0" "mcom";
pushnode 31 "(0 * a1 <= [/(a1) * /(a1)] * a1 & P145 & P132 & P0) &  (Real(0) & P152 & P124 & P115 & P80 & P60 & P51 & P32 & P25 & P18 & P11 & P5 & P0) & (~0 eq a1 & P154 & P126 & P117 & P82 & P62 & P53 & P28 & P21 & P14 & P7 & P1 & P0) & P0 ->  (0 <= /(a1) & P156 & P128 & P118 & P83 & P63 & P54 & P33 & P26 & P19 & P12 & P6 & P0) & P0" 2;
pushnode 33 " (0 <= a1 & P176 & P140 & P125 & P116 & P81 & P61 & P52 & P27 & P20 & P13 & P7 & P1 & P0) & P0 -> (0 <= a1 & P179 & P143 & P132 & P0) & P0" 0;
pushnode 32 "( 0 <= /(a1) * /(a1) & P157 & P133 & P130 & P0) & P0 -> (0 <= /(a1) * /(a1) & P167 & P143 & P132 & P0) & P0" 0;
pushnode 30 "(0 <= /(a1) * /(a1) & P133 & P130 & P0) & (0 <= a1 & P140 & P125 & P116 & P81 & P61 & P52 & P27 & P20 & P13 & P7 & P1 & P0) & P0 -> ((0 <= /(a1) * /(a1) & 0 <= a1) & P143 & P132 & P0) & P0" 2;
pushnode 29 "((0 <= /(a1) * /(a1) & 0 <= a1 -> 0 * a1 <= [/(a1) * /(a1)] * a1) & P132 & P0) & ( 0 <= /(a1) * /(a1) & P130 & P0) & (Real(0) & P124 & P115 & P80 & P60 & P51 & P32 & P25 & P18 & P11 & P5 & P0) & (0 <= a1 & P125 & P116 & P81 & P61 & P52 & P27 & P20 & P13 & P7 & P1 & P0) & (~0 eq a1 & P126 & P117 & P82 & P62 & P53 & P28 & P21 & P14 & P7 & P1 & P0) & P0 -> (0 <= /(a1) & P128 & P118 & P83 & P63 & P54 & P33 & P26 & P19 & P12 & P6 & P0) & P0" 2;
pushreference 28 "P0 ->  ((0 <= /(a1) * /(a1) & 0 <= a1 -> 0 * a1 <= [/(a1) * /(a1)] * a1) & P131 & P0) & P0" "ordmult";
pushnode 27 "(0 <= /(a1) * /(a1) & P130 & P0) & (Real(0) & P124 & P115 & P80 & P60 & P51 & P32 & P25 & P18 & P11 & P5 & P0) & (0 <= a1 & P125 & P116 & P81 & P61 & P52 & P27 & P20 & P13 & P7 & P1 & P0) & (~0 eq a1 & P126 & P117 & P82 & P62 & P53 & P28 & P21 & P14 &  P7 & P1 & P0) & P0 -> (0 <= /(a1) & P128 & P118 & P83 & P63 & P54 & P33 & P26 & P19 & P12 & P6 & P0) & P0" 2;
pushreference 26 "P0 -> (0 <=  /(a1) * /(a1) & P129 & P0) & P0" "thm 3.2.iv";
pushnode 25 " (Real(0) & P124 & P115 & P80 & P60 & P51 & P32 & P25 & P18 & P11 & P5 & P0) &  (0 <= a1 & P125 & P116 & P81 & P61 & P52 & P27 &  P20 & P13 & P7 & P1 & P0) & (~0 eq a1 & P126 & P117 & P82 & P62 & P53 & P28 & P21 & P14 & P7 & P1 & P0) & P0 -> (0 <= /(a1) & P128 & P118 & P83 & P63 & P54 & P33 & P26 & P19 & P12 & P6 & P0) & P0" 2;
pushnode 24 "( Real(0) & P115 & P80 & P60 & P51 & P32 & P25 & P18 & P11 & P5 & P0) & (0 <= a1 & P116 & P81 & P61 & P52 & P27 & P20 & P13 & P7 & P1 & P0) & (~0 eq a1 & P117 & P82 & P62 & P53 & P28 & P21 & P14 & P7 & P1 & P0) & P0 -> ( 0 <= /(a1) & P118 & P83 & P63 & P54 & P33 & P26 & P19 & P12 & P6 & P0) & P0" 1;
pushnode 23 " (a1 * /(a1) = 1 & P99 & P75 & P65 & P0) & P0 -> (a1 * /(a1) = 1 & P107 & P98 & P0) & P0" 0;
pushnode 22 "( (a1 * /(a1) = 1 -> 1 = a1 * /(a1)) & P98 & P0) & (a1 * /(a1) = 1 & P75 & P65 & P0) & (Real(0) & P80 & P60 & P51 & P32 & P25 & P18 & P11 & P5 & P0) & (0 <= a1 & P81 & P61 & P52 & P27 & P20 & P13 & P7 & P1 & P0) & (~0 eq a1 & P82 & P62 & P53 & P28 & P21 & P14 & P7 & P1 & P0) & P0 -> (0 <= /(a1) & P83 & P63 & P54 & P33 & P26 & P19 & P12 & P6 & P0) & P0" 2;
pushreference 21 "P0 -> ( (a1 * /(a1) = 1 -> 1 = a1 * /(a1)) & P97 & P0) & P0" "symm";
pushnode 16 "(a1 * /(a1) = 1 & P75 & P65 & P0) & (Real(0) & P80 & P60 & P51 & P32 & P25 & P18 & P11 & P5 & P0) & (0 <= a1 & P81 & P61 & P52 & P27 & P20 & P13 & P7 & P1 & P0) & (~0 eq a1 & P82 & P62 & P53 & P28 & P21 & P14 & P7 & P1 & P0) & P0 -> (0 <= /(a1) & P83 & P63 & P54 & P33 & P26 & P19 & P12 & P6 & P0) & P0" 2;
pushnode 19 "(~a1 eq 0 & P87 & P0) & (~0 eq a1 & P72 & P62 & P53 & P28 & P21 & P14 & P7 & P1 & P0) & P0 -> (~a1 eq 0 & P73 & P65 & P0) & P0" 0;
pushnode 18 "( ~0 eq a1 & P72 & P62 & P53 & P28 & P21 & P14 & P7 & P1 & P0) & P0 -> (~0 eq a1 & P86 & P0) & (~a1 eq 0 & P73 & P65 & P0) & P0" 0;
pushreference 17 " (~0 eq a1 & P84 & P0) & P0 -> (~a1 eq 0 & P85 & P0) & P0" "negeqsymm";
pushnode 15 "(~0 eq a1 & P72 & P62 & P53 & P28 & P21 & P14 & P7 & P1 & P0) & P0 -> (~a1 eq 0 & P73 & P65 & P0) & P0" 3;
pushnode 14 " ((~a1 eq 0 -> a1 * /(a1) = 1) & P65 & P0) & (Real(0) & P60 & P51 & P32 & P25 & P18 & P11 & P5 & P0) & (0 <= a1 & P61 & P52 & P27 & P20 & P13 & P7 & P1 & P0) & (~0 eq a1 & P62 & P53 & P28 & P21 & P14 & P7 & P1 & P0) & P0 ->  (0 <= /(a1) & P63 & P54 & P33 & P26 & P19 & P12 & P6 & P0) & P0" 2;
pushreference 13 "P0 -> ((~a1 eq 0 -> a1 * /(a1) = 1) & P64 & P0) & P0" "minv";
pushnode 12 " (Real(0) & P60 & P51 & P32 & P25 & P18 & P11 & P5 & P0) &  (0 <= a1 & P61 & P52 & P27 & P20 & P13 & P7 & P1 & P0) &  (~0 eq a1 & P62 & P53 & P28 & P21 & P14 & P7 & P1 & P0) & P0 -> (0 <= /(a1) & P63 & P54 & P33 & P26 & P19 & P12 & P6 & P0) & P0" 2;
pushnode 11 "(Real(0) & P51 & P32 & P25 & P18 & P11 & P5 & P0) &  (0 <= a1 & P52 & P27 & P20 & P13 & P7 & P1 & P0) & (~0 eq a1 & P53 & P28 & P21 & P14 & P7 & P1 & P0) & P0 -> (0 <= /(a1) & P54 & P33 & P26 & P19 & P12 & P6 & P0) & P0" 1;
pushnode 10 " (~0 eq 1 & P29 & P22 & P15 & P8 & P2 & P0) & (Real(1) & P31 & P24 & P17 & P10 & P4 & P0) & (Real(0) & P32 & P25 & P18 & P11 & P5 & P0) & (0 <= a1 & P27 & P20 & P13 & P7 & P1 & P0) & (~0 eq a1 & P28 & P21 & P14 & P7 & P1 & P0) & P0 -> (0 <= /(a1) & P33 & P26 & P19 & P12 & P6 & P0) & P0" 1;
pushnode 9 " (~0 eq 1 & P29 & P22 & P15 & P8 & P2 & P0) & (Real(1) & P31 & P24 & P17 & P10 & P4 & P0) & (Real(0) & P32 & P25 & P18 & P11 & P5 & P0) & (0 <= a1 & P27 & P20 & P13 & P7 & P1 & P0) & (~0 eq a1 & P28 & P21 & P14 & P7 & P1 & P0) & P0 -> (~0 eq 1 & P45 & P0) & (0 <= /(a1) & P33 & P26 & P19 & P12 & P6 & P0) & P0" 0;
pushnode 8 "(Real(1) & P31 & P24 & P17 & P10 & P4 & P0) & (Real(0) & P32 & P25 & P18 & P11 & P5 & P0) & (0 <= a1 & P27 & P20 & P13 & P7 & P1 & P0) & (~0 eq a1 & P28 & P21 & P14 & P7 & P1 & P0) & (~0 eq 1 & P29 & P22 & P15 & P8 & P2 & P0) & P0 -> (Real(1) & P44 & P0) & (0 <= /(a1) & P33 & P26 & P19 & P12 & P6 & P0) & P0" 0;
pushreference 7 "(Real(1) & P41 & P0) & (~0 eq 1 & P42 & P0) & P0 -> (0 < 1 & P43 & P0) & P0" "thm 3.2.v";
pushnode 5 " (~0 eq 1 & P29 & P22 & P15 & P8 & P2 & P0) & (Real(1) & P31 & P24 & P17 & P10 & P4 & P0) & (Real(0) & P32 & P25 & P18 & P11 & P5 & P0) & (0 <= a1 & P27 & P20 & P13 & P7 & P1 & P0) & (~0 eq a1 & P28 & P21 & P14 & P7 & P1 & P0) & P0 -> (0 <= /(a1) & P33 & P26 & P19 & P12 & P6 & P0) & P0" 4;
pushnode 4 " (0 <= a1 & P20 & P13 & P7 & P1 & P0) & (~0 eq a1 & P21 & P14 & P7 & P1 & P0) & (~0 eq 1 & P22 & P15 & P8 & P2 & P0) & (Real(a1) & P23 & P16 & P9 & P3 & P0) & (Real(1) & P24 & P17 & P10 & P4 & P0) &  (Real(0) & P25 & P18 & P11 & P5 & P0) & P0 -> ((0 <= /(a1) & ~0 eq /(a1)) & P26 & P19 & P12 & P6 & P0) & P0" 2;
pushnode 3 "(0 <= a1 & P13 & P7 & P1 & P0) & (~0 eq a1 & P14 & P7 & P1 & P0) & (~0 eq 1 & P15 & P8 & P2 & P0) & (Real(a1) & P16 & P9 & P3 & P0) & (Real(1) & P17 & P10 & P4 & P0) & (Real(0) & P18 & P11 & P5 & P0) & P0 -> (0 < /(a1) & P19 & P12 & P6 & P0) & P0" 1;
pushnode 2 "((0 <= a1 & ~0 eq a1) & P7 & P1 & P0) & (~0 eq 1 & P8 & P2 & P0) & (Real(a1) & P9 & P3 & P0) & (Real(1) & P10 & P4 & P0) & (Real(0) & P11 & P5 & P0) & P0 -> (0 < /(a1) & P12 & P6 & P0) & P0" 1;
pushnode 1 " (0 < a1 & P1 & P0) & (~0 eq 1 & P2 & P0) & (Real(a1) & P3 & P0) & (Real(1) & P4 & P0) & (Real(0) & P5 & P0) & P0 -> (0 < /(a1) & P6 & P0) & P0" 1;
THEOREMS:=("3.2.vi",(termtosequent(parseprop("(0 < a1 & P1 & P0) & (~0 eq 1 & P2 & P0) & (Real(a1) & P3 & P0) & (Real(1) & P4 & P0) & (Real(0) & P5 & P0) & P0 -> (0 < /(a1) & P6 & P0) & P0")),hd(!PROOFSTACK)))::(!THEOREMS);
PROOFSTACK:=nil;
td "3.2.vi";
pushreference 1 "( 0 < a1 & P1 & P0) & (~0 eq 1 & P2 & P0) & (Real(a1) & P3 & P0) & (Real(1) & P4 & P0) & (Real(0) & P5 & P0) & P0 -> (0 < /(a1) & P6 & P0) & P0" "3.2.vi";