# Maple input for Casey Mulligan's 45 Economics Examples.
# Each examples is fully existentially quantified.  Given here as list of lists of polynomials.
# Inner lists entries are connected by AND and outer list entries by OR (i.e. DNF).
Econ0001:=[[v1 > 0], [v7 >= 0], [v4 <= 0], [v8 <= 0], [v5 <> 1], [v6 <> 1], [v1*v5 + v3*v7 <> v4], [v2*v6 + v3*v8 <> v4]]: 
Econ0004:=[[v1 > 0], [v2 > 0], [v7 >= 0], [v4 <= 0], [v8 <= 0], [v5 <> 1], [v6 <> 1], [v1*v5 + v3*v7 <> v4], [v2*v6 + v3*v8 <> v4]]: 
Econ0006:=[[v1 > 0], [v7 >= 0], [v3 <= 0], [v4 <= 0], [v8 <= 0], [v5 <> 1], [v6 <> 1], [v1*v5 + v3*v7 <> v4], [v2*v6 + v3*v8 <> v4]]: 
Econ0009:=[[v4 >= 0], [v7 >= 0], [v1 < 0], [v2 < 0], [v8 <= 0], [v5 <> 1], [v6 <> 1], [v1*v5 + v3*v7 <> v4], [v2*v6 + v3*v8 <> v4]]: 
Econ0012:=[[v5 >= 0], [v7 >= 0], [v11 >= 0], [v7 < v8], [v12 <= 0], [v2 <> 0], [v4 <> v3], [v9 <> 1], [v10 <> 1], [v11*v5 + v1*v9 <> v7], [v11*v6 + v2*v9 <> v8], [v10*v3 + v12*v5 <> v7], [v10*v4 + v12*v6 <> v8]]: 
Econ0013:=[[v7/2 < v8, v8 < 0], [v5 >= 0], [v7 >= 0], [v11 >= 0], [v12 <= 0], [v2 <> 0], [v4 <> v3], [v9 <> 1], [v10 <> 1], [v11*v5 + v1*v9 <> v7], [v11*v6 + v2*v9 <> v8], [v10*v3 + v12*v5 <> v7], [v10*v4 + v12*v6 <> v8]]: 
Econ0015:=[[v11^2*v7 - v11*v12*v7 - v11^2*v8 + 2*v11*v12*v8 - v12^2*v8 = 0, v11^2*v8 - 2*v11*v12*v8 + v12^2*v8 = v11^2*v7 - v11*v12*v7], [v7 >= 0], [v11 >= 0], [v12 <= 0], [v2 <> 0], [v4 <> v3], [v5 <> 0], [v9 <> 1], [v10 <> 1], [v11*v5 + v1*v9 <> v7], [v11*v6 + v2*v9 <> v8], [v10*v3 + v12*v5 <> v7], [v10*v4 + v12*v6 <> v8]]: 
Econ0016:=[[v7/2 > 0, v8 > v7/2, v6 < v5/2], [v11 >= 0], [v12 >= -v11], [v1 <= 0], [v12 <= 0], [v2 <> 0], [v3 <> v1], [v4 <> v3], [v9 <> 1], [v10 <> 1], [v11*v5 + v1*v9 <> v7], [v11*v6 + v2*v9 <> v8], [v10*v3 + v12*v5 <> v7], [v10*v4 + v12*v6 <> v8]]: 
Econ0018:=[[v7 < v8], [v3 <= 0], [v4 <= 0], [v5 <= v6], [v2 <> v1], [v3*v5 + v4*v7 <> v1], [v3*v6 + v4*v8 <> v2]]: 
Econ0021:=[[v8 < 0, v9 < 0, v10 < 0], [v6 >= 1], [v7 >= 1], [v11 >= 0], [v12 >= 0], [v15 >= 0], [v17 >= 0], [v12 + v14*v16 - v14*v16*v7 + v13*v17*(1 - v7) >= 0], [v20 >= 0], [v3 < 0], [v4 < 0], [v19 < 0], [v1 <= 0], [v2 <= 0], [v5 <= 0], [v13 <= 0], [v11*v14 <= v12*v13], [v11*v15 <= v13*v14], [v16 <= 0], [v18 <= 0], [v6 <> 0], [v7 <> 0], [v18 - v4 <> v3], [v18 - v4 - v5 - 2*v18*v6 + v4*v6 + v5*v6 + v18*v6^2 <> 0], [v10*v16 - v8 + v18*v9 - v4*v9 <> 0], [v1*v19*v2 + v17*v2^2 <> 0], [v10*v12*v13 - v13^2*v16 + v10*v13^2*v17 - v10*v13^2*v17*v7 + v13*v14*v8 + v13^2*v19*v9 - v13^2*v19*v7*v9 <> v10*v11*v14 + v11*v15*v8], [v1*v19*v2 + v1^2*v20 <> 0], [v10*v19 + v20*v9 <> 0]]: 
Econ0022:=[[v6 >= 1], [v7 >= 1], [v11 >= 0], [v12 >= 0], [v15 >= 0], [v17 >= 0], [v12 + v14*v16*(1 - v7) + v13*v17*(1 - v7) >= 0], [v20 >= 0], [v3 < 0], [v4 < 0], [v9 < 0], [v19 < 0], [v1 <= 0], [v2 <= 0], [v5 <= 0], [v13 <= 0], [v11*v14 <= v12*v13], [v11*v15 <= v13*v14], [v16 <= 0], [v18 <= 0], [v18 - v4 <> v3], [v18 - v4 - v5 - 2*v18*v6 + v4*v6 + v5*v6 + v18*v6^2 <> 0], [v10*v16 - v8 + v18*v9 - v4*v9 <> 0], [v1*v19*v2 + v17*v2^2 <> 0], [v10*v11*v14 - v10*v13^2*v17 + v10*v13^2*v17*v7 + v11*v15*v8 - v13^2*v19*v9 + v13^2*v19*v7*v9 <> v10*v12*v13 + v13*v14*v8], [v1*v19*v2 + v1^2*v20 <> 0], [v10*v19 - 2*v10*v19*v6 + v10*v19*v6^2 + v20*v9 - 2*v20*v6*v9 + v20*v6^2*v9 <> v4 + v5]]: 
Econ0023:=[[v6 >= 1], [v7 >= 1], [v11 >= 0], [v12 >= 0], [v15 >= 0], [v17 >= 0], [v12 + v14*v16*(1 - v7) + v13*v17*(1 - v7) >= 0], [v20 >= 0], [v3 < 0], [v4 < 0], [v8 < 0], [v19 < 0], [v1 <= 0], [v2 <= 0], [v5 <= 0], [v13 <= 0], [v11*v14 <= v12*v13], [v11*v15 <= v13*v14], [v16 <= 0], [v18 <= 0], [v18 - v4 <> v3], [v18 - v4 - v5 - 2*v18*v6 + v4*v6 + v5*v6 + v18*v6^2 <> 0], [v10*v16 - v8 + v18*v9 - v4*v9 <> 0], [v1*v19*v2 + v17*v2^2 <> 0], [v10*v11*v14 - v10*v13^2*v17 + v10*v13^2*v17*v7 + v11*v15*v8 - v13^2*v19*v9 + v13^2*v19*v7*v9 <> v10*v12*v13 + v13*v14*v8], [v1*v19*v2 + v1^2*v20 <> 0], [v10*v19 - 2*v10*v19*v6 + v10*v19*v6^2 + v20*v9 - 2*v20*v6*v9 + v20*v6^2*v9 <> v4 + v5]]: 
Econ0024:=[[v6 = 0, v7 < 0], [v3 >= 1], [v4 >= 1], [v8 >= 0], [v9 >= 0], [v12 >= 0], [v14 >= 0], [v11*v13*(1 - v4) + v10*v14*(1 - v4) + v9 >= 0], [v17 >= 0], [v1 < 0], [v16 < 0], [v2 <= 0], [v10 <= 0], [v11*v8 <= v10*v9], [v12*v8 <= v10*v11], [v13 <= 0], [v15 <= 0], [-v1 + v15 - v2 + v1*v3 - 2*v15*v3 + v2*v3 + v15*v3^2 <> 0], [-v5 - v1*v6 + v15*v6 + v13*v7 <> 0], [v16 <> 0], [-(v10^2*v13) + v10*v11*v5 + v10^2*v16*v6 - v10^2*v16*v4*v6 + v10^2*v14*v7 - v10^2*v14*v4*v7 + v10*v7*v9 <> v12*v5*v8 + v11*v7*v8], [v17*v6 + v16*v7 <> 0]]: 
Econ0025:=[[v3 >= 1], [v4 >= 1], [v8 >= 0], [v9 >= 0], [v12 >= 0], [v14 >= 0], [v11*v13*(1 - v4) + v10*v14*(1 - v4) + v9 >= 0], [v17 >= 0], [v1 < 0], [v5 < 0], [v16 < 0], [v2 <= 0], [v10 <= 0], [v11*v8 <= v10*v9], [v12*v8 <= v10*v11], [v13 <= 0], [v15 <= 0], [-v1 + v15 - v2 + v1*v3 - 2*v15*v3 + v2*v3 + v15*v3^2 <> 0], [-v5 - v1*v6 + v15*v6 + v13*v7 <> 0], [v16 <> 0], [-(v10^2*v13) + v10*v11*v5 + v10^2*v16*v6 - v10^2*v16*v4*v6 + v10^2*v14*v7 - v10^2*v14*v4*v7 + v10*v7*v9 <> v12*v5*v8 + v11*v7*v8], [v17*v6 + v16*v7 <> 0]]: 
Econ0026:=[[v5 >= 1], [v6 >= 1], [v10 >= 0], [v11 >= 0], [v14 >= 0], [v17 >= 0], [v20 >= 0], [v3 < 0], [v7 < 0], [v19 < 0], [v1 <= 0], [v2 <= 0], [v4 <= 0], [v12 <= 0], [v10*v13 <= v11*v12], [v10*v14 <= v12*v13], [v18 <= 0], [v9 <> 0], [-(v12*v14*v18) + v12*v14*v3 + v12*v14*v4 + v12*v14*v18*v5 <> v14^2*v9], [v1*v19*v2 + v17*v2^2 <> 0], [-(v12^2*v19) + v12^2*v19*v6 + v10*v14*v7 + v10*v13*v8 - v12^2*v17*v8 + v12^2*v17*v6*v8 <> v12*v13*v7 + v11*v12*v8], [v1*v19*v2 + v1^2*v20 <> 0], [-(v12*v14*v20) + v12*v14*v20*v5 - v14^2*v18*v7 + v14^2*v3*v7 + v14^2*v4*v7 + v14^2*v18*v5*v7 - v13*v14*v18*v8 - v12*v14*v19*v8 + v13*v14*v3*v8 + v13*v14*v4*v8 + v13*v14*v18*v5*v8 + v12*v14*v19*v5*v8 <> -(v12*v16*v18*v7) + v12*v16*v3*v7 + v12*v16*v4*v7 + v12*v16*v18*v5*v7 - v12*v15*v18*v8 + v12*v15*v3*v8 + v12*v15*v4*v8 + v12*v15*v18*v5*v8]]: 
Econ0027:=[[v4 > 0, v5 > 0, v2^2*v5*v7 + v2^2*v4*v8 - v1*v2*v5*v8 > 0, -1 < v3, v3 < 0, v2^2*v5*v7 + v2^2*v4*v8 - v1*v2*v5*v8 < v2^2], [v2*v9 >= 0], [v1^2*v2*v9 >= 0], [v1 <= 0], [v2 <= 0], [v2*v7 <= 0], [v2^2*v7 <= v1*v2*v8], [v8 <= 0], [v10*v13 <= v11*v12], [v10*v14 <= v12*v13], [v6 <> 0], [v2^2 + v2^2*v3 - v2^2*v5*v7 - v2^2*v4*v8 + v1*v2*v5*v8 <> 0], [v2^2*v6 + v1*v5*v9 <> v2*v4*v9], [v10*v14*v2^4*v3 + v10*v13*v2^4*v5 <> v12*v13*v2^4*v3 + v11*v12*v2^4*v5 - v1*v12^2*v2^2*v4*v9 + v1^2*v12^2*v2*v5*v9]]: 
Econ0028:=[[v8 > 0, v11*v2^2*v6 - v1*v11*v2*v8 + v10*v2^2*v8 > 0, -1 < v5, v5 < 0, v7 < 0, v11*v2^2*v6 - v1*v11*v2*v8 + v10*v2^2*v8 < v2^2], [0 > v4], [v4 >= 1], [v13*v2 >= 0], [v1^2*v13*v2 >= 0], [v14 >= 0], [v15 >= 0], [v16 >= 0], [v19 >= 0], [v1 <= 0], [v2 <= 0], [v3 <= -1], [v10*v2 <= 0], [v10*v2^2 <= v1*v11*v2], [v11 <= 0], [v12 <= 0], [v17 <= 0], [v15*v18 <= v16*v17], [v15*v19 <= v17*v18], [-v18^2 + v16*v19 <= 0], [v6 <> 0], [v9 <> 0], [v2^2 + v2^2*v5 - v2^2*v6 - v11*v2^2*v6 + v2^2*v7 + v1*v11*v2*v8 - v10*v2^2*v8 <> 0], [v19*v5 + 2*v19*v3*v5 + v19*v3^2*v5 + v18*v8 + 2*v18*v3*v8 + v18*v3^2*v8 + v12*v9 <> v14*v7 + v14*v3*v7], [v15*v19*v2^4*v5 + v15*v18*v2^4*v8 <> v17*v18*v2^4*v5 - v1*v13*v17^2*v2^2*v6 + v1^2*v13*v17^2*v2*v8 + v16*v17*v2^4*v8]]: 
Econ0029:=[[v5 = 0, v12*v16 = v14*v15 + v14^2*v7*v8], [0 > v2], [v10 > 0], [v2 >= 1], [v11 >= 0], [v14*v15*v5 + v14^2*v5*v7*v8 < v12*v16*v5], [v1 <= 0], [v7 <= 0], [v8 <= 0], [v9 <= 0], [v1*v10 + v8 <= 0], [v12*v15 <= v13*v14], [v12*v16 <= v14*v15], [v6 <> 0], [v5*v8 + v4*v9 <> 1 + v3], [v1*v10*v2*v5 + v2*v5*v8 + v1*v7*v8 <> 1], [v11*v4 <> v6], [v12*v16*v3 - v13*v14*v5 - v10*v14^2*v5 + v12*v15*v5 + v10*v14^2*v2*v5 + v14^2*v7*v8 <> v14*v15*v3]]: 
Econ0030:=[[v6 = 0, v14*v15*v2 - v12*v16*v2 + v14^2*v2*v8*v9 = v1*v10*v14^2*v8], [0 > v3], [v3 >= 1], [v11*v2 >= 0], [v1^2*v11*v2 >= 0], [v14*v15*v2^2*v6 - v12*v16*v2^2*v6 - v1*v10*v14^2*v2*v6*v8 + v14^2*v2^2*v6*v8*v9 < 0], [v1 <= 0], [v2 <= 0], [v8 <= 0], [v2*v9 <= 0], [v2^2*v9 <= v1*v10*v2], [v10 <= 0], [v12*v15 <= v13*v14], [v12*v16 <= v14*v15], [v7 <> 0], [v2 + v2*v4 + v1*v10*v6 <> v10*v2*v5 + v2*v6*v9], [v1*v11*v6 + v2^2*v7 <> v11*v2*v5], [v1^2*v11*v3*v6 + v2^2*v3*v6*v9 + v2^3*v8*v9 <> v2^2 + v1*v11*v2*v3*v5 + v1*v10*v2*v3*v6 + v1*v10*v2^2*v8], [-(v14*v15*v2^3*v4) + v12*v16*v2^3*v4 - v1^2*v11*v14^2*v6 - v13*v14*v2^3*v6 + v12*v15*v2^3*v6 + v1^2*v11*v14^2*v3*v6 + v14^2*v2^3*v8*v9 <> -(v1*v11*v14^2*v2*v5) + v1*v11*v14^2*v2*v3*v5 + v1*v10*v14^2*v2^2*v8]]: 
Econ0051:=[[v6 >= 1], [v7 >= 1], [v11 >= 0], [v12 >= 0], [v15 >= 0], [v17 >= 0], [v12 + v14*v16*(1 - v7) + v13*v17*(1 - v7) >= 0], [v20 >= 0], [v3 < 0], [v4 < 0], [v9 < 0], [v19 < 0], [v1 <= 0], [v2 <= 0], [v5 <= 0], [v13 <= 0], [v11*v14 <= v12*v13], [v11*v15 <= v13*v14], [v16 <= 0], [v18 <= 0], [v18 - v4 <> v3], [v18 - v4 - v5 - 2*v18*v6 + v4*v6 + v5*v6 + v18*v6^2 <> 0], [v10*v16 - v8 + v18*v9 - v4*v9 <> 0], [v1*v19*v2 + v17*v2^2 <> 0], [v10*v11*v14 - v10*v13^2*v17 + v10*v13^2*v17*v7 + v11*v15*v8 - v13^2*v19*v9 + v13^2*v19*v7*v9 <> v10*v12*v13 + v13*v14*v8], [v1*v19*v2 + v1^2*v20 <> 0], [v10*v19 - 2*v10*v19*v6 + v10*v19*v6^2 + v20*v9 - 2*v20*v6*v9 + v20*v6^2*v9 <> v4 + v5]]: 
Econ0052:=[[v28 + v29 = 0], [v1 >= 1], [v2 >= 1], [v14 >= 0], [v19 >= 0], [v13 <= 0], [v16 <= 0], [v17 <= 0], [-v17^2 + v14*v19 <= 0], [v2 <> v1], [v3 <> 0], [v6 <> 0], [v7 <> 1], [v8 <> 0], [v9 <> v7], [v9 - 2*v1*v9 + v1^2*v9 <> 1 - v1 - v2 + v1*v2], [v11 <> 0], [v12 <> 0], [(1 - v1)*v16 <> v13*(1 - v2)], [(1 - v1)*(v17*(v3 - v5) + v19*v5) - v16*v7 <> (1 - v2)*(v14*(v3 - v5) + v17*v5) - v13*v9], [-(v11*v16) + (1 - v1)*(-(v10*v17) + v10*v19 + (1 - v4)*(v18*(v3 - v5) + v20*v5) + v4*(v20*(v3 - v5) + v21*v5)) - (v17*(v3 - v5) + v19*v5)*v6 - (v17*(1 - v4) + v19*v4)*v7 <> -(v12*v13) + (1 - v2)*(-(v10*v14) + v10*v17 + (1 - v4)*(v15*(v3 - v5) + v18*v5) + v4*(v18*(v3 - v5) + v20*v5)) - (v14*(v3 - v5) + v17*v5)*v8 - (v14*(1 - v4) + v17*v4)*v9], [v27*v3 + v24*v7 + v22*v9 <> v13*(v3 - v5) + v16*v5], [v12*v22 + v11*v24 + v3*v30 + v29*v7 + v28*v9 + v8*(v28*v3 + v25*v7 + v23*v9) + v6*(v29*v3 + v26*v7 + v25*v9) <> -(v10*v13) + v10*v16 + (1 - v4)*(v14*(v3 - v5) + v17*v5) + v4*(v17*(v3 - v5) + v19*v5)]]: 
Econ0053:=[[v7 > 0, -1 < v4, 0 < v7*v9, v4 < 0, v6 < 0, v7*v9 < 1], [0 > v3], [v12 > 0], [v3 >= 1], [v13 >= 0], [v14 >= 0], [v15 >= 0], [v18 >= 0], [v1 <= 0], [v2 <= -1], [v9 <= 0], [v10 <= 0], [v11 <= 0], [v1*v12 + v9 <= 0], [v16 <= 0], [v14*v17 <= v15*v16], [v14*v18 <= v16*v17], [-v17^2 + v15*v18 <= 0], [v5 <> 0], [v8 <> 0], [v10*v5 + v7*v9 <> 1 + v4 - v5 + v6], [v18*v4 + 2*v18*v2*v4 + v18*v2^2*v4 + v17*v7 + 2*v17*v2*v7 + v17*v2^2*v7 + v11*v8 <> v13*v6 + v13*v2*v6], [v14*v18*v4 + v14*v17*v7 <> v16*v17*v4 + v15*v16*v7 + v12*v16^2*v7]]: 
Econ0054:=[[v8 > 0, v11*v2^2*v6 - v1*v11*v2*v8 + v10*v2^2*v8 > 0, -1 < v5, v5 < 0, v7 < 0, v11*v2^2*v6 - v1*v11*v2*v8 + v10*v2^2*v8 < v2^2], [0 > v4], [v4 >= 1], [v13*v2 >= 0], [v1^2*v13*v2 >= 0], [v14 >= 0], [v15 >= 0], [v16 >= 0], [v19 >= 0], [v1 <= 0], [v2 <= 0], [v3 <= -1], [v10*v2 <= 0], [v10*v2^2 <= v1*v11*v2], [v11 <= 0], [v12 <= 0], [v17 <= 0], [v15*v18 <= v16*v17], [v15*v19 <= v17*v18], [-v18^2 + v16*v19 <= 0], [v6 <> 0], [v9 <> 0], [v2^2 + v2^2*v5 - v2^2*v6 - v11*v2^2*v6 + v2^2*v7 + v1*v11*v2*v8 - v10*v2^2*v8 <> 0], [v19*v5 + 2*v19*v3*v5 + v19*v3^2*v5 + v18*v8 + 2*v18*v3*v8 + v18*v3^2*v8 + v12*v9 <> v14*v7 + v14*v3*v7], [v15*v19*v2^4*v5 + v15*v18*v2^4*v8 <> v17*v18*v2^4*v5 - v1*v13*v17^2*v2^2*v6 + v1^2*v13*v17^2*v2*v8 + v16*v17*v2^4*v8]]: 
Econ0055:=[[0 > v32], [0 > v33], [v7 > 0], [v10 > 0], [v11 > 0], [v16 > 0], [v17 > 0], [v18 >= 0], [v19 >= 0], [v20 >= 0], [v21 >= 0], [v22 >= 0], [v27 >= 0], [v28 >= 0], [v32 >= 1], [v33 >= 1], [v12 <= 0], [v13 <= 0], [v15 <= 0], [v23 <= 0], [v24 <= 0], [v19*v25 <= v21*v23], [v20*v26 <= v22*v24], [v19*v27 <= v23*v25], [-v25^2 + v21*v27 <= 0], [v20*v28 <= v24*v26], [-v26^2 + v22*v28 <= 0], [v29 <= 0], [v12 + v16*v29 <= 0], [v30 <= 0], [v13 + v17*v30 <= 0], [v31 <= -1], [v3 <> 1], [v4 <> 1], [v5 <> 0], [v9 <> 0], [v14*v5 + v12*v7 <> v1 + v3 - v5 + v6], [v15*v6 + v13*v8 <> v2 + v4 - v6], [v1*v27 + 2*v1*v27*v31 + v1*v27*v31^2 + v25*v7 + 2*v25*v31*v7 + v25*v31^2*v7 + v24*v9 + v15*v24*v9 <> v2*v28 + v15*v2*v28 + v2*v28*v31 + v15*v2*v28*v31 + v18*v24*v6 + v18*v24*v31*v6 + v26*v8 + v15*v26*v8 + v26*v31*v8 + v15*v26*v31*v8], [v10*v12*v23^2 + v1*v19*v27 - v16*v23^2*v7 + v19*v25*v7 + v16*v23^2*v32*v7 <> v1*v23*v25 + v21*v23*v7], [v10*v12*v29 + v12*v32*v7 + v16*v29*v32*v7 <> v3], [v11*v13*v24^2 + v2*v20*v28 - v17*v24^2*v8 + v20*v26*v8 + v17*v24^2*v33*v8 <> v2*v24*v26 + v22*v24*v8], [v11*v13*v30 + v13*v33*v8 + v17*v30*v33*v8 <> v4]]: 
Econ0056:=[[v12*v5 >= v10^2, v12*v8 >= v11^2, v5*v8 >= v7^2, v11^2*v5 + v12*v7^2 + (v10^2 - v12*v5)*v8 >= 2*v10*v11*v7, v12 <= 0, v5 <= 0, v8 <= 0], [v1 <= 0], [v2 <= 0], [v3 <= 0], [v4 <= 0], [v6 <= 0], [v9 <= 0], [2*v11*v6*v9 <= v12*v6^2 + v8*v9^2], [v12*(v5*v6^2 - 2*v4*v6*v7 + v4^2*v8) + 2*v10*v6*(v11*v4 + v7*v9) + v9*(-2*v11*v5*v6 + 2*v11*v4*v7 + v5*v8*v9) <= v11^2*v4^2 + v10^2*v6^2 + 2*v10*v4*v8*v9 + v7^2*v9^2], [v1*v12 + v11*v2 + v10*v3 <> 0], [v1*v10 + v3*v5 + v2*v7 <> 0], [v1*v11 + v3*v7 + v2*v8 <> 0]]: 
Econ0057:=[[v6 = v5], [v7 > v8], [0 >= v13], [v13 >= v14], [v14 >= 1], [v1 <= 0], [v2 <= 0], [v5 <= 0], [v6 <= 0], [v7 <= v10], [v8 <= v9], [(-v1 + v3)*(-v7 + v9) <= 0], [(-v2 + v4)*(v10 - v8) <= 0], [v11 <= 0], [v12 <= 0], [v5^2 <> v1^3], [v6^2 <> v2^3], [27*v11^3*v5 <> 8], [27*v12^3*v6 <> 8], [v11*(1 - v13)*(v5 - v6) <> v1 - v4], [v12*(1 - v14)*(-v5 + v6) <> v2 - v3], [v12*v14*v6 <> v11*v13*v5]]: 
Econ0061:=[[v10*v5 + v11*v6 = v9], [v3^2*v5*v8^2 <> v1*v3*v4*v8], [v3^2*v6*v8^2 <> v2*v3*v7*v8], [v13*v3 <> v3^2*v9], [v14*v4 <> v10*v4^2], [v15*v7 <> v11*v7^2], [v16*v8 <> v1], [v2*v7^2 + v16*v4*v7*v8 - v12*v7^2*v8 <> 0], [v15*v16*v4*v7 + v13*v7^2 - v12*v15*v7^2 - v14*v16*v7^2 <> 0], [v1<=0], [v3<=0], [v4<=0], [v7<=0]]: 
Econ0062:=[[v13*v15*v6 = v14], [v3^2*v5*v8^2 <> v1*v3*v4*v8], [v3^2*v6*v8^2 <> v2*v3*v7*v8], [v12 <> 0], [v17 <> v8], [v1*v18 <> v1^2*v9], [v19*v2 <> v10*v2^2], [v20*v3 <> v11*v3^2], [v21*v4 <> v12*v4^2], [v22*v7 <> v13*v7^2], [v23*v8 <> v14*v8^2], [v24*v8 <> v1], [v2*v7^2 + v24*v4*v7*v8 - v16*v7^2*v8 <> 0], [v22*v24*v4*v7 + v20*v7^2 - v16*v22*v7^2 - v21*v24*v7^2 <> 0], [v17*v25*v3 <> v15*v17^2], [v20*v25 <> v23], [v1<=0], [v3<=0], [v4<=0], [v7<=0]]: 
Econ0063:=[[v6 = 1 - v5], [v3^2*v5*v8^2 <> v1*v3*v4*v8], [v3^2*v6*v8^2 <> v2*v3*v7*v8], [v7*v9 <> v3], [v10*v8 <> v1], [v2*v7^2 + v10*v4*v7*v8 - v7^2*v8*v9 <> 0], [v1<=0], [v3<=0], [v4<=0], [v7<=0]]: 
Econ0064:=[[v13 = v5*(v8 - v9) + v9], [v3^2*v5*v7^2 <> v1*v3*v4*v7], [v11 <> 0], [v14*v6 <> v3], [v1*v15 <> v1^2*v8], [v16*v2 <> v2^2*v9], [v17*v3 <> v10*v3^2], [v18*v4 <> v11*v4^2], [v19*v6 <> v12*v6^2], [v20*v7 <> v13*v7^2], [v22*v7 <> v1], [v2*v6^2 + v22*v4*v6*v7 - v14*v6^2*v7 <> 0], [v1^2*v20 - v1^2*v15*v21 - v1^2*v16*v23 + v1*v15*v2*v23 <> 0], [v20*v22*v4*v6^3 + v16*v6^4 - v14*v20*v6^4 + v18*v24*v4*v6^2*v7 <> v19*v24*v4^2*v6*v7], [v15*v6^2 - v20*v22*v6^2 + v19*v24*v4*v7 <> v18*v24*v6*v7], [v1<=0], [v2<=0], [v3<=0], [v4<=0], [v7<=0]]: 
Econ0065:=[[v13*(-(v16*v5) + v15*v6) = v10], [v3^2*v5*v8^2 <> v1*v3*v4*v8], [v3^2*v6*v8^2 <> v2*v3*v7*v8], [v12 <> 0], [-(v10*v12) + v10*v13 + v12^2*v16 - 2*v12*v13*v16 + v13^2*v16 + v12*v9 - v13*v9 <> 0], [v17*v7 <> v3], [v18 <> v8], [v1*v19 <> v1^2*v9], [v2*v20 <> v10*v2^2], [v21*v3 <> v11*v3^2], [v22*v4 <> v12*v4^2], [v23*v7 <> v13*v7^2], [v24*v8 <> v14*v8^2], [v26*v8 <> v1], [v2*v7^2 + v26*v4*v7*v8 - v17*v7^2*v8 <> 0], [v23*v26*v4*v7 + v21*v7^2 - v17*v23*v7^2 - v22*v26*v7^2 <> 0], [v18*v27*v3 <> v15*v18^2], [v21*v27 <> v24], [v1^2*v24 - v1^2*v19*v25 + v1*v19*v2*v28 - v1^2*v20*v28 <> 0], [v24*v26*v4*v7^3 + v20*v7^4 - v17*v24*v7^4 + v22*v29*v4*v7^2*v8 <> v23*v29*v4^2*v7*v8], [v19*v7^2 - v24*v26*v7^2 + v23*v29*v4*v8 <> v22*v29*v7*v8], [v1<=0], [v2<=0], [v3<=0], [v4<=0], [v7<=0]]: 
Econ0066:=[[v4*v7*(v10 + v9) = v5], [0 >= v4], [v4 >= 1], [v1 <= 0], [v2 <= 0], [v1^2*v11 <= v1*v12*v2], [v12 <= 0], [v3 + v4 <> 1], [v8 <> v3*(v5 - v6) + v6], [v4*v7*v9 <> v8], [v7*(-(v10*v3) + v4*v9) <> v6]]: 
Econ0067:=[[v12*(-(v15*v5) + v16*v6) = v13*(v15 + v16)*v6], [0 >= v6], [v6 >= 1], [v1 <= 0], [v2 <= 0], [v3 <= 0], [v4 <= 0], [v7 <= 0], [v8 <= 0], [v1^2*v26 <= v1*v2*v30], [v30 <= 0], [v5 + v6 <> 1], [v3^2*v5*v8^2 <> v1*v3*v4*v8], [v3^2*v6*v8^2 <> v2*v3*v7*v8], [v9 <> 0], [-(v10*v12) + v10*v13 + v12^2*v16 - 2*v12*v13*v16 + v13^2*v16 + v12*v9 - v13*v9 <> 0], [v18 <> v8], [v1*v19 <> v1^2*v9], [v2*v20 <> v10*v2^2], [v21*v3 <> v11*v3^2], [v22*v4 <> v12*v4^2], [v23*v7 <> v13*v7^2], [v24*v8 <> v14*v8^2], [v27*v8 <> v1], [v2*v7^2 + v27*v4*v7*v8 - v17*v7^2*v8 <> 0], [v23*v27*v4*v7 + v21*v7^2 - v17*v23*v7^2 - v22*v27*v7^2 <> 0], [v18*v28*v3 <> v15*v18^2], [v21*v28 <> v24], [v1^2*v24 - v1^2*v19*v25 + v1*v19*v2*v29 - v1^2*v20*v29 <> 0], [v24*v27*v4*v7^3 + v20*v7^4 - v17*v24*v7^4 + v22*v31*v4*v7^2*v8 <> v23*v31*v4^2*v7*v8], [v19*v7^2 - v24*v27*v7^2 + v23*v31*v4*v8 <> v22*v31*v7*v8]]: 
Econ0074:=[[v7 > v8], [v3 >= v4], [(v1 - v3)*(v7 - v8) >= 0], [(v2 - v4)*(v7 - v8) >= 0], [(v5 - v6)*(v7 - v8) <= 0], [v5 <> v2], [v6 <> v3]]: 
Econ0076:=[[2*v5 + v6 + 2*v2*v7 + v1*v9^2 >= v1*v7^2 + 2*(v2 + v3)*v9], [v1 < 1], [v4 < 0], [v1*v4 < v2^2], [v6 < 0], [v1*v6 < v3^2], [v4*v6 < v5^2], [v5 + v1*v7*v8 < v3*v7 + v2*v8], [v9 <> v7 + v8]]: 
Econ0077:=[[2*v1*v5 + v1*v6 + 2*v1*v2*v7 - v1^2*v7^2 - 2*v1*v2*v9 - 2*v1*v3*v9 + v1^2*v9^2 >= 0], [v1 < 1], [v4 < 0], [v1*v4 < v2^2], [v6 < 0], [v1*v6 < v3^2], [v4*v6 < v5^2], [v1*v5 - v1*v3*v7 - v1*v2*v8 + v1^2*v7*v8 < 0], [v9 <> v7 + v8]]: 
Econ0078:=[[v2 > v3], [v9 > v7], [v1 < 0], [v5 < 0], [v1*v5 < v2^2], [v8 < 0], [v1*v8 < v3^2], [v5*v8 < v6^2], [2*v2*v3*v6 + v1*v5*v8 < v3^2*v5 + v1*v6^2 + v2^2*v8], [v10 < 0], [v1*v10 < v4^2], [v10*v5 < v7^2], [v10*v8 < v9^2], [v1*v10*v5 + 2*v2*v4*v7 < v10*v2^2 + v4^2*v5 + v1*v7^2], [v1*v10*v8 + 2*v3*v4*v9 < v10*v3^2 + v4^2*v8 + v1*v9^2], [v3^2*(-(v10*v5) + v7^2) + v1*v10*v5*v8 + v4^2*(v6^2 - v5*v8) + 2*v1*v6*v7*v9 + v2^2*v9^2 + 2*v2*v3*(v10*v6 - v7*v9) < v1*v10*v6^2 + v10*v2^2*v8 + v1*v7^2*v8 + v1*v5*v9^2 + 2*v4*(v3*(v6*v7 - v5*v9) + v2*(-(v7*v8) + v6*v9))], [2*v6*v7*v9 + v5*(v10*v8 - v9^2) < v10*v6^2 + v7^2*v8], [v2 + v9 <= v3 + v7]]: 
Econ0079:=[[2*v1*v3 + v6 >= 2*v5], [v1^2 < 0], [v4 < 0], [v6 < 0], [v2*v6 < v3^2], [v4*v6 < v5^2], [v5 <= v1*v3]]: 
Econ0080:=[[v9 = 0], [v3 < 0], [v7 < 0], [v3*v7 < v4^2], [v10 < 0], [v10*v3 < v5^2], [v10*v7 < v8^2], [v10*v3*v7 + 2*v4*v5*v8 < v10*v4^2 + v5^2*v7 + v3*v8^2], [v12 < 0], [v12*v3 < v6^2], [v12*v7 < v9^2], [v10*v12 < v11^2], [v12*v3*v7 + 2*v4*v6*v9 < v12*v4^2 + v6^2*v7 + v3*v9^2], [v10*v12*v3 + 2*v11*v5*v6 < v11^2*v3 + v12*v5^2 + v10*v6^2], [v10*v12*v7 + 2*v11*v8*v9 < v11^2*v7 + v12*v8^2 + v10*v9^2], [v11^2*v4^2 + v10*v12*v3*v7 + v6^2*(-(v10*v7) + v8^2) + 2*v11*v3*v8*v9 + 2*v4*v5*(v12*v8 - v11*v9) + v5^2*(-(v12*v7) + v9^2) < v10*v12*v4^2 + v11^2*v3*v7 + v12*v3*v8^2 + v10*v3*v9^2 + 2*v6*(v4*(v11*v8 - v10*v9) + v5*(-(v11*v7) + v8*v9))], [v1 <= 0], [v2 <= 0], [v2*v5 <> 0], [v1*v9 <> v5]]: 
Econ0082:=[[v10 = 0], [v4 < 0], [v7 < 0], [v4*v7 < v5^2], [v9 < 0], [v2*v9 < v3^2], [v4*v9 < v6^2], [v7*v9 < v8^2], [2*v5*v6*v8 + v4*(-v8^2 + v7*v9) < v6^2*v7 + v5^2*v9], [v1 <= 0], [v3 + v8 <= 2*v6], [v6 <> v3], [v1*((-1 + v10)*v3 + (1 - 2*v10)*v6 + v10*v8) <> 0]]: 
Econ0083:=[[v10 = 0], [v2 < 1], [v4 < 0], [v7 < 0], [v4*v7 < v5^2], [v9 < 0], [v2*v9 < v3^2], [v4*v9 < v6^2], [v7*v9 < v8^2], [2*v5*v6*v8 + v4*(-v8^2 + v7*v9) < v6^2*v7 + v5^2*v9], [v1 <= 0], [v4 <= 0], [v1*v2*(v3 - 2*v6 + v8) <= 0], [v1^2*v9 <= 0], [v1*v2*v6 <> v1*v2*v3], [-(v2*v3) + v10*v2*v3 + v2*v6 - 2*v10*v2*v6 + v10*v2*v8 <> 0]]: 
Econ0084:=[[v12 = 0], [0 > v2], [v2 > 1], [v3^2*v4*(v10 + v5 - 2*v8) >= 0], [v4 < 1], [v6 < 0], [v9 < 0], [v6*v9 < v7^2], [v11 < 0], [v11*v4 < v5^2], [v11*v6 < v8^2], [v11*v9 < v10^2], [2*v10*v7*v8 + v6*(-v10^2 + v11*v9) < v11*v7^2 + v8^2*v9], [v1 <= 0], [v3 <= 0], [v1*v10*v2*v3*v4 - v1*v3*v4*v5 + v1*v2*v3*v4*v5 + v1*v3*v4*v8 - 2*v1*v2*v3*v4*v8 <> 0], [v1*v10*v2*v3*v4 + v1^2*v10*v2*v3*v4 + v1^2*v10*v12*v3^2*v4 - v1*v3*v4*v5 - v1^2*v3*v4*v5 + v1*v2*v3*v4*v5 + v1^2*v2*v3*v4*v5 + v1^2*v12*v3^2*v4*v5 + v1*v3*v4*v8 + v1^2*v3*v4*v8 - 2*v1*v2*v3*v4*v8 - 2*v1^2*v2*v3*v4*v8 - 2*v1^2*v12*v3^2*v4*v8 <> 0]]: 
Econ0085:=[[v3 < 1], [v6 < 0], [v3*v6 < v4^2], [v1*v2*v3 + v7 < v2*v4 + v1*v5], [v8 < 0], [v3*v8 < v5^2], [v6*v8 < v7^2], [v3*v4 <= v3^2], [v3*v5 <= 0], [v3*v4 <> v1*v3^2], [v3*v5 <> v2*v3^2], [v3*v7 <> v3*v5]]: 
Econ0086:=[[v7 >= v2], [v1*(v12 + v3 - 2*v8) >= 0], [v1 < 1], [v4 < 0], [v9 < 0], [v4*v9 < v5^2], [v13 < 0], [v13*v4 < v6^2], [v13*v9 < v10^2], [2*v10*v5*v6 + v4*(-v10^2 + v13*v9) < v13*v5^2 + v6^2*v9], [v16 < 0], [v1*v16 < v2^2], [v16*v4 < v7^2], [v16*v9 < v11^2], [v13*v16 < v14^2], [2*v11*v5*v7 + v4*(-v11^2 + v16*v9) < v16*v5^2 + v7^2*v9], [2*v10*v11*v14*v4 + v14^2*v5^2 + 2*(-(v11*v14) + v10*v16)*v5*v6 + v13*v16*v4*v9 + v7^2*(v10^2 - v13*v9) + v6^2*(v11^2 - v16*v9) < v11^2*v13*v4 + v10^2*v16*v4 + v13*v16*v5^2 + v14^2*v4*v9 + 2*v7*((-(v11*v13) + v10*v14)*v5 + v6*(v10*v11 - v14*v9))], [(-v14^2 + v13*v16)*v4 + 2*v14*v6*v7 < v16*v6^2 + v13*v7^2], [2*v10*v11*v14 + (-v14^2 + v13*v16)*v9 < v11^2*v13 + v10^2*v16], [v18 < 0], [v1*v18 < v3^2], [v18*v4 < v8^2], [v18*v9 < v12^2], [v13*v18 < v15^2], [v16*v18 < v17^2], [2*v12*v5*v8 + v4*(-v12^2 + v18*v9) < v18*v5^2 + v8^2*v9], [2*v10*v12*v15*v4 + v15^2*v5^2 + 2*(-(v12*v15) + v10*v18)*v5*v6 + v13*v18*v4*v9 + v8^2*(v10^2 - v13*v9) + v6^2*(v12^2 - v18*v9) < v12^2*v13*v4 + v10^2*v18*v4 + v13*v18*v5^2 + v15^2*v4*v9 + 2*v8*((-(v12*v13) + v10*v15)*v5 + v6*(v10*v12 - v15*v9))], [2*v11*v12*v17*v4 + v17^2*v5^2 + 2*(-(v12*v17) + v11*v18)*v5*v7 + v16*v18*v4*v9 + v8^2*(v11^2 - v16*v9) + v7^2*(v12^2 - v18*v9) < v12^2*v16*v4 + v11^2*v18*v4 + v16*v18*v5^2 + v17^2*v4*v9 + 2*v8*((-(v12*v16) + v11*v17)*v5 + v7*(v11*v12 - v17*v9))], [(-v15^2 + v13*v18)*v4 + 2*v15*v6*v8 < v18*v6^2 + v13*v8^2], [2*v10*v12*v15 + (-v15^2 + v13*v18)*v9 < v12^2*v13 + v10^2*v18], [2*v14*v15*v17*v4 + v13*v16*v18*v4 + v17^2*v6^2 + 2*(-(v15*v17) + v14*v18)*v6*v7 + (v15^2 - v13*v18)*v7^2 + (v14^2 - v13*v16)*v8^2 < v15^2*v16*v4 + v13*v17^2*v4 + v14^2*v18*v4 + v16*v18*v6^2 + 2*((-(v15*v16) + v14*v17)*v6 + (v14*v15 - v13*v17)*v7)*v8], [v12^2*(v14^2 - v13*v16) + v10^2*v17^2 + v11^2*(v15^2 - v13*v18) + 2*v10*v11*(-(v15*v17) + v14*v18) + 2*v14*v15*v17*v9 + v13*v16*v18*v9 < 2*v12*(v11*(v14*v15 - v13*v17) + v10*(-(v15*v16) + v14*v17)) + v10^2*v16*v18 + v15^2*v16*v9 + v13*v17^2*v9 + v14^2*v18*v9], [(-v17^2 + v16*v18)*v4 + 2*v17*v7*v8 < v18*v7^2 + v16*v8^2], [2*v11*v12*v17 + (-v17^2 + v16*v18)*v9 < v12^2*v16 + v11^2*v18], [2*v14*v15*v17 + v13*(-v17^2 + v16*v18) < v15^2*v16 + v14^2*v18], [v12^2*v14^2*v4 + v11^2*v15^2*v4 + 2*v10*v12*v15*v16*v4 + 2*v11*v12*v13*v17*v4 + v10^2*v17^2*v4 + 2*v10*v11*v14*v18*v4 + v15^2*v16*v5^2 + v13*v17^2*v5^2 + v14^2*v18*v5^2 + 2*v12*v14*v17*v5*v6 + 2*v11*v15*v17*v5*v6 + 2*v10*v16*v18*v5*v6 + v12^2*v16*v6^2 + v11^2*v18*v6^2 + 2*v14*v15*v17*v4*v9 + v13*v16*v18*v4*v9 + v17^2*v6^2*v9 + v8^2*(v11^2*v13 - 2*v10*v11*v14 + v10^2*v16 + (v14^2 - v13*v16)*v9) + v7^2*(v12^2*v13 - 2*v10*v12*v15 + v10^2*v18 + (v15^2 - v13*v18)*v9) < 2*v11*v12*v14*v15*v4 + v12^2*v13*v16*v4 + 2*v10*v12*v14*v17*v4 + 2*v10*v11*v15*v17*v4 + v11^2*v13*v18*v4 + v10^2*v16*v18*v4 + 2*v14*v15*v17*v5^2 + v13*v16*v18*v5^2 + 2*v12*v15*v16*v5*v6 + 2*v10*v17^2*v5*v6 + 2*v11*v14*v18*v5*v6 + 2*v11*v12*v17*v6^2 + v15^2*v16*v4*v9  + v13*v17^2*v4*v9 + v14^2*v18*v4*v9 + v16*v18*v6^2*v9 + 2*v8*((v12*(v14^2 - v13*v16) + v11*(-(v14*v15) + v13*v17) + v10*(v15*v16 - v14*v17))*v5 + v7*(-(v10*v12*v14) + v11*(v12*v13 - v10*v15) + v10^2*v17 + (v14*v15 - v13*v17)*v9) + v6*(v11^2*v15 + v10*v12*v16 - v11*(v12*v14 + v10*v17) + (-(v15*v16) + v14*v17)*v9)) + 2*v7*((v12*(-(v14*v15) + v13*v17) + v11*(v15^2 - v13*v18) + v10*(-(v15*v17) + v14*v18))*v5 + v6*(v12^2*v14 - v12*(v11*v15 + v10*v17) + v10*v11*v18 + (v15*v17 - v14*v18)*v9))], [v19 < 0], [v13 <= 0], [v1*v12*v19 - v1*v2 + v1*v19*v3 + v1*v7 - 2*v1*v19*v8 <> 0]]: 
Econ1001:=[[v2 = 0], [v3 >= 1], [v100*(-1 + v34)^2 + v101*(-1 + v35)^2 + (-1 + v3)^2*v69 + (-1 + v4)^2*v70 + (-1 + v5)^2*v71 + (-1 + v6)^2*v72 + (-1 + v7)^2*v73 + (-1 + v10)^2*v76 + (-1 + v11)^2*v77 + (-1 + v12)^2*v78 + (-1 + v13)^2*v79 + v74*(-1 + v8)^2 + (-1 + v14)^2*v80 + (-1 + v15)^2*v81 + (-1 + v16)^2*v82 + (-1 + v17)^2*v83 + (-1 + v18)^2*v84 + (-1 + v19)^2*v85 + (-1 + v20)^2*v86 + (-1 + v21)^2*v87 + (-1 + v22)^2*v88 + (-1 + v23)^2*v89 + v75*(-1 + v9)^2 + (-1 + v24)^2*v90 + (-1 + v25)^2*v91 + (-1 + v26)^2*v92 + (-1 + v27)^2*v93 + (-1 + v28)^2*v94 + (-1 + v29)^2*v95 + (-1 + v30)^2*v96 + (-1 + v31)^2*v97 + (-1 + v32)^2*v98 + (-1 + v33)^2*v99 >= 0], [v1 <= 0], [v10 + v11 + v12 + v13 + v14 + v15 + v16 + v17 + v18 + v19 + v20 + v21 + v22 + v23 + v24 + v25 + v26 + v27 + v28 + v29 + v3 + v30 + v31 + v32 + v33 + v34 + v35 + v4 + v5 + v6 + v7 + v8 + v9 <= 33], [(-1 + v3)*v36 + v37*(-1 + v4) + (-1 + v10)*v43 + (-1 + v11)*v44  + (-1 + v12)*v45 + (-1 + v13)*v46 + (-1 + v14)*v47 + (-1 + v15)*v48 + (-1 + v16)*v49 + v38*(-1 + v5) + (-1 + v17)*v50 + (-1 + v18)*v51 + (-1 + v19)*v52 + (-1 + v20)*v53 + (-1 + v21)*v54 + (-1 + v22)*v55 + (-1 + v23)*v56 + (-1 + v24)*v57 + (-1 + v25)*v58 + (-1 + v26)*v59 + v39*(-1 + v6) + (-1 + v27)*v60 + (-1 + v28)*v61 + (-1 + v29)*v62 + (-1 + v30)*v63 + (-1 + v31)*v64 + (-1 + v32)*v65 + (-1 + v33)*v66 + (-1 + v34)*v67 + (-1 + v35)*v68 + v40*(-1 + v7) + v41*(-1 + v8)   + v42*(-1 + v9) <> 0], [v69 <> -(v1*v36)], [v70 <> -(v1*v37)], [v71 <> -(v1*v38)], [v72 <> -(v1*v39)], [v73 <> -(v1*v40)], [v74 <> -(v1*v41)], [v75 <> -(v1*v42)], [v76 <> -(v1*v43)], [v77 <> -(v1*v44)], [v78 <> -(v1*v45)], [v79 <> -(v1*v46)], [v80 <> -(v1*v47)], [v81 <> -(v1*v48)], [v82 <> -(v1*v49)], [v83 <> -(v1*v50)], [v84 <> -(v1*v51)], [v85 <> -(v1*v52)], [v86 <> -(v1*v53)], [v87 <> -(v1*v54)], [v88 <> -(v1*v55)], [v89 <> -(v1*v56)], [v90 <> -(v1*v57)], [v91 <> -(v1*v58)], [v92 <> -(v1*v59)], [v93 <> -(v1*v60)], [v94 <> -(v1*v61)], [v95 <> -(v1*v62)], [v96 <> -(v1*v63)], [v97 <> -(v1*v64)], [v98 <> -(v1*v65)], [v99 <> -(v1*v66)], [v100 <> -(v1*v67)], [v101 <> -(v1*v68)], [v100*(-1 + v34)*(1 - v2 + v2*v34) + v101*(-1 + v35)*(1 - v2 + v2*v35) + (-1 + v3)*(1 - v2 + v2*v3)*v69 + (-1 + v4)*(1 - v2 + v2*v4)*v70 + (-1 + v5)*(1 - v2 + v2*v5)*v71 + (-1 + v6)*(1 - v2 + v2*v6)*v72 + (-1 + v7)*(1 - v2 + v2*v7)*v73     + (-1 + v10)*(1 - v2 + v10*v2)*v76 + (-1 + v11)*(1 - v2 + v11*v2)*v77 + (-1 + v12)*(1 - v2 + v12*v2)*v78 + (-1 + v13)*(1 - v2 + v13*v2)*v79 + v74*(-1 + v8)*(1 - v2 + v2*v8) + (-1 + v14)*(1 - v2 + v14*v2)*v80 + (-1 + v15)*(1 - v2 + v15*v2)*v81 + (-1 + v16)*(1 - v2 + v16*v2)*v82 + (-1 + v17)*(1 - v2 + v17*v2)*v83 + (-1 + v18)*(1 - v2 + v18*v2)*v84 + (-1 + v19)*(1 - v2 + v19*v2)*v85 + (-1 + v20)*(1 - v2 + v2*v20)*v86 + (-1 + v21)*(1 - v2 + v2*v21)*v87      + (-1 + v22)*(1 - v2 + v2*v22)*v88 + (-1 + v23)*(1 - v2 + v2*v23)*v89 + v75*(-1 + v9)*(1 - v2 + v2*v9) + (-1 + v24)*(1 - v2 + v2*v24)*v90 + (-1 + v25)*(1 - v2 + v2*v25)*v91 + (-1 + v26)*(1 - v2 + v2*v26)*v92 + (-1 + v27)*(1 - v2 + v2*v27)*v93 + (-1 + v28)*(1 - v2 + v2*v28)*v94 + (-1 + v29)*(1 - v2 + v2*v29)*v95 + (-1 + v30)*(1 - v2 + v2*v30)*v96 + (-1 + v31)*(1 - v2 + v2*v31)*v97 + (-1 + v32)*(1 - v2 + v2*v32)*v98 + (-1 + v33)*(1 - v2 + v2*v33)*v99 <> 0]]: