print(`QE Example Bank`): print(` ~~~~ `): print(`Maintained by Zak Tonks, University of Bath`): print(` Z.P.Tonks@bath.ac.uk `): print(`Modified from David Wilson's original CAD Example Bank`): print(`D.J.Wilson@bath.ac.uk`): print(`Run Help() for more information`): Help := proc() print(`This file loads a global table full of QE examples`); print(`This is called 'QEExamples'. Meanwhile, two other global tables are`); print(`loaded - one of which is called 'EconomicsAssumptions', and the other`); print(`'EconomicsHypotheses'. From these, 'BuildEconomicsQEExample' is able `); print(`to build an appropriate QE example as per the paper 'Benchmarks for `); print(`'Non-linear Real Arithmetic Benchmarks derived from Automated `); print(`Reasoning in Economics'. Calling 'PrintQEExamplesInfo' will print `); print(`information about all QE Examples in the database. `); print(`'PrintEconomicsQEExamples' will print all assumptions and hypotheses `); print(`stored per Economics QE example. 'BrownDavenportQEExample' accepts an`); print(`integer argument that builds the Brown-Davenport QE example for `); print(`appropriate 'n'. (this will be quantified if n > 0). It also accepts `); print(`two further optional arguments that should be two unevaluated names `); print(`that replace 'x' and 'y' in output (they will be indexed). `); print(`'BuildEconomicsQEExample' first takes an argument of a name, or an `); print(`integer, referring to one of the problems in the QE economics database`); print(`(see 'PrintEconomicsQEExamples'). The second argument is one of `); print(`'theorem', 'example', 'counterexample', or 'assumptions', and will `); print(`build the corresponding QE example as per the relevant paper given `); print(`such a key word. The output is hence a quantified problem for that `); print(`example. Note: the integer corresponds to the integer that is the `); print(`last 4 digits of such an index of the tables.`); end proc: PrintQEExamplesInfo := proc( ) # prints info about the examples in the given database (table) local L :: list := [ indices( :-QEExamples, ':-indexorder' = ( ( x, y ) -> StringTools:-Compare( x[], y[] ) ), ':-nolist' ) ], n :: nonnegint := numelems( L ), i :: name; printf( `Total of %d examples in this table\n`, n ); printf( `List of examples:\n` ); printf( `\n` ); for i in L do printf( i ); printf( `\n` ); print( :-QEExamples[ i ] ); printf( `\n` ); end do; end proc: PrintEconomicsQEExamplesInfo := proc( ) local L :: list := [ indices( :-EconomicsAssumptions, ':-indexorder' = ( ( x, y ) -> StringTools:-Compare( substring( x[], -4..-1 ), substring( y[], -4..-1 ) ) ), ':-nolist' ) ], n :: nonnegint := numelems( L ), i :: name; printf( `Total of %d economics examples\n`, n ); printf( `List of examples:\n` ); printf( `\n` ); for i in L do printf( i ); printf( `\n` ); printf( `\n` ); printf( `Assumptions:\n` ); printf( `\n` ); print( :-EconomicsAssumptions[ i ] ); printf( `\n` ); printf( `Hypothesis:\n` ); printf( `\n` ); print( :-EconomicsHypotheses[ i ] ); printf( `\n` ); end do; end proc: ################################################################################ BrownDavenportQEExample := proc( n :: nonnegint, x1 :: name := ':-x', y1 :: name := ':-y', $ ) :: TarskiFormula; # From BD09 - recursive definition of building a specific quantified formula # Included to build some of the examples local x :: name, y :: name, xn :: procedure, yn :: procedure, z :: name; if n = 0 then ( x, y ) := cat( x1, ':-`__`' , 0 ) , cat( y1, ':-`__`' , 0 ); return ':-Or'( ':-And'( x <= 1/2, y = 2*x ), ':-And'( x > 1/2, y = 2 - 2*x ) ); else ( xn, yn, z ) := i -> cat( x1, ':-`__`' , i ), i -> cat( y1, ':-`__`' , i ), cat( ':-`z__`', n ); return exists( z, forall( [ xn( n-1 ), yn( n-1 ) ], ':-Implies'( ':-Or'( ':-And'( yn(n-1) = yn(n), xn(n-1) = z ), ':-And'( yn(n-1) = z, xn(n-1) = xn(n) ) ), procname( n-1 ) ) ) ); end if; end proc: ################################################################################ # Makes a global table `QEExamples` full of QE examples :-`QEExamples` := table([ ### 2: CMXY09 Examples #1: '`Parametric Parabola`' = ':-exists'(x, a*x^2+b*x+c = 0 ), #2: '`Whitney Umbrella`' = ':-exists'([u,v], ':-And'( x-u*v = 0, y-v = 0, z-u^2 = 0 ) ), #3: '`Quartic`' = ':-forall'(x, x^4+p*x^2+q*x+r >= 0 ), #7: '`A Real Implicitization Problem`' = ':-exists'([u,v], ':-And'(x-u*v = 0, y-u*v^2 = 0, z-u^2 = 0) ), #8: '`Ball and Circular Cylinder`' = ':-exists'([z,x,y], ':-And'(x^2+y^2+z^2-1 < 0, x^2+(y+z-2)^2-1 < 0) ), #9: '`Termination of Term Rewrite System`' = ':-exists'(r, ':-forall'([x,y], ':-Implies'(':-And'(x-r > 0, y-r > 0), x^2*(1+2*y)^2-y^2*(1+2*x^2) > 0 ) ) ), #10: '`Collins and Johnson`' = ':-exists'(r, ':-And'(3*a^2*r+3*b^2-2*a*r-a^2-b^2 < 0, 3*a^2*r+3*b^2*r-4*a*r+r-2*a^2-2*b^2+2*a > 0, a-1/2 >= 0, b > 0, r > 0, r-1 < 0) ), #11: '`Range of Lower Bounds`' = ':-forall'([x,a,b,c],':-exists'(z, ':-Implies'( ':-And'(a > 0, a*z^2+b*z+c <> 0), a*x^2+b*x+c-y > 0 ) ) ), #12: '`X-axis Ellipse Problem`' = ':-And'(a*b <> 0, ':-forall'([x,y], ':-Implies'( b^2*(x-c)^2+a^2*y^2-a^2*b^2 = 0, x^2+y^2-1 <= 0) ) ), #13: '`Davenport-Heintz`' = ':-exists'(c, ':-forall'([b,a], ':-Implies'( ':-Or'(':-And'(a-d = 0, b-c = 0), ':-And'(a-c = 0, b-1 = 0) ), a^2-b = 0 ) ) ), #14: '`Hong-90`' = ':-exists'([a,b], ':-And'(r+s+t = 0, r*s+s*t+t*r-a = 0, r*s*t-b = 0) ), #15: '`Solotareff-3`' = ':-exists'([u,v], ':-And'(r > 0, r-1 > 0, u+1 > 0, u-v < 0, v-1 < 0, 3*u^2+2*r*u-a = 0, 3*v^2+2*r*v-a = 0, u^3+r*u^2-a*u+a-r-1 = 0, v^3+r*v^2-a*v-2*b-a+r+1 = 0 ) ), #16: '`Collision Problem`' = ':-exists'([t,x,y], ':-And'(17*t/16-6 >= 0, 17*t/16-10 <= 0, x-17*t/16+1 >= 0, x-17*t/16-1 <= 0, y-17*t/16+9 >= 0, y-17*t/16+7 <= 0, (x-t)^2+y^2-1 >= 0 ) ), #18: '`Ellipse Problem`' = ':-And'(a*b <> 0, ':-forall'([x,y], ':-Implies'( b^2*(x-c)^2+a^2*(y-d)^2-a^2*b^2 = 0, x^2+y^2-1 <= 0 ) ) ), ### 4: Motion Planning Examples #4.1.1: '`Piano Movers Problem (Davenport)`' = ':-Or'(x > 0, w > 0, y < 0, z < 0, ':-exists'(t, ':-And'(0 < t , t < 1, x + t*(w-x) < -1, y + t*(z-y) > 1) ) ), #4.1.2: '`Piano Movers Problem (Yang, Zheng)`' = ':-forall'(x, 4*x^8 - 4*(L-3)*x^6 - 2*(3*L - 6)*x^4 - 2*(L-3)*x^2 + 1 > 0 ), #4.1.3: '`Piano Movers Problem (Wang)`' = ':-exists'([a,b,c,d], ':-And'(a^2 + b^2 = r^2, a >= 0, b < 0, c >= 1, d < -1, c - (1+b)*(c-a) = 0, d - (1-a)*(d-b) = 0 ) ), ### 5: Examples from Buchberger-Hong [BH91] #5.1: '`Intersection`' = ':-exists'(z, ':-And'(x^2-(1/2)*(y^2)-(1/2)*z^2 = 0, x*z+z*y-2*x = 0, z^2-y = 0) ), #5.2: Intersection B # Identical to above, but suggests z > x > y rather than z > y > x #5.3: '`Random A`' = ':-exists'(z, ':-forall'(y, ':-exists'(x, ':-And'(4*x^2+x*y^2-z+(1/4) = 0, 2*x+y^2*z+(1/2) = 0, x^2*z-(1/2)*x-y^2 = 0) ) ) ), #5.4: '`Random B`' = ':-exists'(x, ':-forall'(y, ':-exists'(z, ':-And'(4*x^2+x*y^2-z+(1/4) = 0, 2*x+y^2*z+(1/2) = 0, x^2*z-(1/2)*x-y^2 = 0) ) ) ), #5.5: '`Ellipse A`' = ':-exists'([y,x], ':-And'(x^2+y^2-1 = 0, b^2*(x-c)^2+a^2*y^2-a^2*b^2 = 0, a > 0, a-1 < 0, b > 0, b-1 < 0, c >= 0, c-1 < 0) ), #5.6: # Identical to above, but suggests x > y rather than y > x # '`Ellipse B`' = # :-exists'([x,y], ':-And'(x^2+y^2-1 = 0, b^2*(x-c)^2+a^2*y^2-a^2*b^2 = 0, # a > 0, a-1 < 0, b > 0, b-1 < 0, c >= 0, c-1 < 0) # ), # just x > y rather than reverse #5.7: '`Solotareff`' = ':-exists'([y,x], ':-And'( 3*x^2-2*x-a = 0, x^3-x^2-a*x-2*b+a-2 = 0, 3*y^2-2*y-a = 0, y^3-y^2-a*y-a+2 = 0, 4*a-1 >= 0, 4*a-7 <= 0, 4*b+3 >= 0, 4*b-3 <= 0, x+1 >= 0, x <= 0, y >= 0, y-1 <= 0 ) ), #5.8: Solotareff B # as above but different ordering of free vars #5.9: '`Collision`' = ':-exists'([y,x,t], ':-And'( (1/4)*(x-t)^2+(y-10)^2-1 = 0, (1/4)*(x-a*t)^2+(y-a*t)^2-1 = 0, t > 0, a > 0 ) ), #5.10: # as above but t > y > x rather than y > x > t # '`Collision B`' = # ':-exists'([t,y,x], ':-And'( (1/4)*(x-t)^2+(y-10)^2-1 = 0, # (1/4)*(x-a*t)^2+(y-a*t)^2-1 = 0, t > 0, a > 0 # ) ), ### 6: Other Examples #6.1: '`Off-Center Ellipse`' = ':-And'(a <> 0, ':-forall'([x,y], ':-Implies'(16*a^2*y^2-8*a^2*y+4*x^2-4*x-3*a^2+1 = 0, y^2+x^2-1 <= 0) ) ), #6.4: '`Edges Square Product`' = ':-exists'([a,b,c], ':-And'(x-a*b+c = 0, y-a*c-x-2 = 0, a >= 0, 2-a <= 0, b-2 >= 0, 4-b <= 0, c+1 >= 0, 1-c <= 0, x+1 >= 0, 9-x <= 0, y+6 >= 0, 6-y <=0 ) ), #6.5: '`Simplified Edges Square Product`' = ':-exists'(a, ':-And'(-a <= 0, a <= 2, 0 <= 1 + x, x <= 9, 0 <= y + 6, y <= 6, 0 <= -(a^2 + 1) * (-y-a*x+2*a^2+2), (-x + a*y)*(a^2 + 1) <= (a^2 + 1)^2, a^2 + 1 <> 0, 0 <= (a^2 + 1) * (a^2 + 1 -x + a*y), (a^2 + 1)*(y+a*x) <= 4*(a^2 + 1)^2 ) ), # rewritten as David's pdf and input doesn't seem to match #6.6: '`Putnum Example`' = ':-exists'([a,b,c,d], ':-And'(a^2+b^2-1 = 0, (c-10)^2+d^2-9 = 0, 2*x-(a+c) = 0, 2+y-(b+d) = 0 ) ), #6.7: '`Simplified Putnum`' = ':-exists'([a,d], ':-And'(a^2+4*y^2-4*y*d+d^2-1 = 0, 4*x^2-4*x*a-40*x+a^2+20*a+91+d^2 = 0 ) ), #6.8: '`YangXia`' = ':-exists'([s,b,c], ':-And'(a^2*h^2-4*s*(s-a)*(s-b)*(s-c) = 0, 2*R*h-b*c = 0, 2*s-a-b-c = 0, b > 0, c > 0, R > 0, h > 0, a+b-c > 0, b+c-a > 0, c+a-b > 0) ), #6.9: '`Simplified YangXia`' = ':-exists'(b, ':-And'(-(1/2)*b <> 0, R > 0, b > 0, h > 0, (1/16)*a^2*h^2*b^4-(1/32)*a^2*b^6- (1/8)*a^2*R^2*h^2*b^2-(1/8)*R^2*h^2*b^4+(1/64)*b^8+ (1/64)*a^4*b^4+(1/4)*R^4*h^4 = 0, 0 < -(1/4)*(-a*b-b^2+2*R*h)*b, 0 < (1/2)*R*h*b, 0 < (1/4)*(2*R*h+a*b-b^2)*b, 0 < (1/4)*(b^2+2*R*h-a*b)*b ) ), #6.10: '`SEIT Model`' = ':-exists'([s,F,J,T], ':-And'(d-d*s-b*J*s = 0, v*F-(d+t)*J = 0, b*J+c*J*T-(d+v+r)*F+(1-q)*t*J = 0, -d*T+r*F+q*t*J-b^2*T*J = 0, F > 0, J > 0, T > 0, s > 0, b > 0, d > 0, v > 0, r > 0, t > 0, q > 0, b-c > 0) ), #6.11: '`Simplified SEIT Model`' = ':-exists'(J, ':-And'(d < 0, r > 0, t > 0, q > 0, b-c > 0, v > 0, J > 0, b > 0, c > 0, d+J*b <> 0, -v <> 0, 0 < (d+t)*J*v, v*c <> 0, d*(d+J*b) > 0, 0 < (d+J*b)*c*v*(-d*v*b+d^2*v+ d^2*t+d*v*t*q+d^3+d^2*r+J*b*v*t*q+d*t*r+J*b*d*v+ J*b*d*t+J*b*t*v+J*b*d^2+J*b*d*r), 0 = -(d+J*b)*c*v^3*d*(-d*v*b-J*b*v*c+d^2*v+d^2*r+ d*v*t*q + d^3 + c*J*d^2+d^2*t+d*t*r+c*J*d*v+c*J*d*t + J*b*d*v+ J*b*d*r + J*b*v*t*q + J*b*d^2+J^2*b*d*c+ J*b*d*t+J*b*t*r+J^2*b*c*v+J^2*b*t*c) ) ), #6.12: '`Cyclic-3`' = ':-exists'([b,a], ':-And'(a+b+c = 0, a*b+b*c+c*a = 0, a*b*c-1 = 0) ), #6.13: '`Cyclic-4`' = ':-exists'([c,b,a], ':-And'(a+b+c+d = 0, a*b+b*c+c*d+d*a = 0, a*b*c+b*c*d+c*d*a+d*a*b = 0, a*b*c*d-1 = 0) ), #ZPT: '`Cyclic-5`' = ':-exists'([d,c,b,a], ':-And'(a+b+c+d+e = 0, a*b+b*c+c*d+d*e+e*a = 0, a*b*c+b*c*d+c*d*e+d*e*a+e*a*b = 0, a*b*c*d+b*c*d*e+c*d*e*a+d*e*a*b+e*a*b*c = 0, a*b*c*d*e - 1 = 0) ), ### 7: Joukowsky Transformation #7.1: '`Joukowsky Original Formulation`' = ':-forall'([a,b,c,d], ':-Implies'(':-And'(a*(c^2+d^2)*(a^2+b^2+1)-c*(a^2+b^2)*(c^2+d^2+1) = 0, b*(c^2+d^2)*(a^2+b^2-1)-d*(a^2+b^2)*(c^2+d^2-1) = 0, b*d > 0, c^2+d^2-1 > 0), ':-And'(a-c = 0, b-d = 0) ) ), #7.2: '`Joukowsky Separate Clauses`' = ':-exists'([a,b,c,d], ':-And'(a*(c^2+d^2)*(a^2+b^2+1)-c*(a^2+b^2)*(c^2+d^2+1) = 0, b*(c^2+d^2)*(a^2+b^2-1)-d*(a^2+b^2)*(c^2+d^2-1) = 0, b*d > 0, c^2+d^2-1 > 0, a-c <> 0) ), #7.3: '`Joukowsky Upper Half Plane`' = ':-forall'([a,b,c,d], ':-Implies'(':-And'(a*(c^2+d^2)*(a^2+b^2+1)-c*(a^2+b^2)*(c^2+d^2+1) = 0, b*(c^2+d^2)*(a^2+b^2-1)-d*(a^2+b^2)*(c^2+d^2-1) = 0, b > 0, d > 0), ':-And'(a-c = 0, b-d = 0) ) ), # All further examples via ZPT instead of DJW # Brown Davenport Examples seq( cat( '`Brown Davenport `', i ) = BrownDavenportQEExample(i) , i in 1..5 ), # Du & Alechina (ZPT), 2D Euclidean Spaces '`2D Euclidean Space Axiomatisation 1`' = ':-exists'([x__1, y__1, x__2, y__2], (x__1-x__2)^2 + (y__1-y__2)^2 <= 1 ), '`2D Euclidean Space Axiomatisation 2`' = ':-exists'([x__1, y__1, x__2, y__2, x__3, y__3], ':-And'( (x__1-x__2)^2 + (y__1-y__2)^2 <= 1, (x__2-x__3)^2 + (y__2-y__3)^2 <= 1, (x__1-x__3)^2 + (y__1-y__3)^2 > 4) ), '`2D Euclidean Space Axiomatisation 3`' = ':-exists'([x__1, y__1, x__2, y__2, x__3, y__3, x__4, y__4], ':-And'( (x__1-x__2)^2 + (y__1-y__2)^2 <= 1 , (x__2-x__3)^2 + (y__2-y__3)^2 <= 4 , (x__3-x__4)^2 + (y__3-y__4)^2 <= 1 , (x__1-x__4)^2 + (y__1-y__4)^2 > 16 ) ), # Quantified Linear Systems paper '`Quantified Linear System`' = ':-forall'([x,z], ':-exists'([y,w], ':-And'(x+y <= z, w <= y, z <= zx-y) ) ), # Algebraic geometry, 3-cube '`Sharir 3-Cube`' = ':-exists'([x__1, x__2, x__3], ':-And'( -2*x__1 - 25*x__2 + 10*x__3 >= -25, 25*x__1 + 2*x__2 + 10*x__3 >= 2, -2*x__1 + 25*x__2 + 10*x__3 >= -25, 25*x__1 - 2*x__2 + 10*x__3 >= 2, -x__2 - x__3 >= 0, -x__2 + x__3 >= -2 ) ), # Economics SC^2 paper '`NLRA Economics 1`' = ':-forall'( [v__1,v__2,v__3,v__4], ':-Implies'( ':-And'( v__1 < 0, v__2 > 0, v__3*v__2 - 1 = v__4, v__4 = v__3*v__1 ), ':-And'( v__3 > 0, v__4 < 0 ) ) ), # First example given in "Non-linear Real Arithmetic Benchmarks ..." '`Positive Invariant Sets 1`' = ':-exists'( q, ':-forall'( [x__1, x__2, x__3], ':-And'( q > 0, l > 0, a > 0, b > 0, c > 0, b*c/2 * ( 2*( x__1^2 - x__1*x__3 - x__1^2*x__2 ) + 2*(x__2 - 2)*(x__1^2 - a*x__2) ) + b*x__3*(c*x__1 - x__3) <= -q*( b*c/2*(x__1^2 + (x__2 - 2)^2 ) + x__3^2/2 - l ) ) ) ), '`Positive Invariant Sets 2`' = ':-exists'( q, ':-forall'( [x__1, x__2, x__3], ':-And'(0 < l, 0 < q, ':-Or'((4*b*k*r__1*x__4 - 2*b*k*x__4^2 + 4*k*q*r__1^2 - 4*k*q*r__1*x__4 + k*q*x__2^2 + k*q*x__3^2 + k*q*x__4^2 - 2*k*r__1*x__1^2 + 4*k*r__1*x__1*x__2 + 2*k*r__2*x__1*x__3 + q*r__1*x__1^2 - k*l*q - 4*k*x__1*x__2 - 2*k*x__3^2)*k < 0, ':-And'(4*b*k*r__1*x__4 - 2*b*k*x__4^2 + 4*k*q*r__1^2 - 4*k*q*r__1*x__4 + k*q*x__2^2 + k*q*x__3^2 + k*q*x__4^2 - 2*k*r__1*x__1^2 + 4*k*r__1*x__1*x__2 + 2*k*r__2*x__1*x__3 + q*r__1*x__1^2 - k*l*q - 4*k*x__1*x__2 - 2*k*x__3^2 = 0, k <> 0 ) ) ) ) ), '`Positive Invariant Sets 3`' = ':-exists'( [q, l, p__1, x__40], ':-forall'( [x__1, x__2, x__3], ':-And'( l > 0, p__1 > 0, q > 0, -2*p__1*x__1^2*k + 2*p__1*x__1*x__2*k + 2*r__1*x__1*x__2 - 2*x__2^2 - 2*x__1*x__2*x__4+2*r__2*x__1*x__3 - 2*x__3^2 + 2*(x__4 - x__40)*(-b*x__4 + x__1*x__2) <= -q*( p__1*x__1^2 + x__2^2 + x__3^2 + (x__4 - x__40)^2 - l ) ) ) ), '`Positive Invariant Sets 4`' = ':-exists'( [q, l, x__40], ':-forall'( [x__1, x__2, x__3], ':-And'( l > 0, p__1 > 0, q > 0, -2*p__1*x__1^2*k + 2*p__1*x__1*x__2*k + 2*r__1*x__1*x__2 - 2*x__2^2 - 2*x__1*x__2*x__4+2*r__2*x__1*x__3 - 2*x__3^2 + 2*(x__4-x__40)*(-b*x__4 + x__1*x__2) <= -q*(p__1*x__1^2 + x__2^2 + x__3^2 + (x__4 - x__40)^2 - l ) ) ) ), '`Positive Invariant Sets 5`' = ':-exists'( [q, l, p__1], ':-forall'( [x__1, x__2, x__3], ':-And'( l > 0, p__1 > 0, q > 0, -2*p__1*x__1^2*k + 2*p__1*x__1*x__2*k + 2*r__1*x__1*x__2 - 2*x__2^2 - 2*x__1*x__2*x__4+2*r__2*x__1*x__3 - 2*x__3^2 + 2*(x__4-x__40)*(-b*x__4 + x__1*x__2) <= -q*(p__1*x__1^2 + x__2^2 + x__3^2 + (x__4 - x__40)^2 - l ) ) ) ), '`Positive Invariant Sets 6`' = ':-exists'( [q, l], ':-forall'( [x__1, x__2, x__3], ':-And'( l > 0, p__1 > 0, q > 0, -2*p__1*x__1^2*k + 2*p__1*x__1*x__2*k + 2*r__1*x__1*x__2 - 2*x__2^2 - 2*x__1*x__2*x__4+2*r__2*x__1*x__3 - 2*x__3^2 + 2*(x__4-x__40)*(-b*x__4 + x__1*x__2) <= -q*(p__1*x__1^2 + x__2^2 + x__3^2 + (x__4 - x__40)^2 - l ) ) ) ), '`Positive Invariant Sets 7`' = ':-exists'( q, ':-forall'( [x__1, x__2, x__3], ':-And'( l > 0, p__1 > 0, q > 0, -2*p__1*x__1^2*k + 2*p__1*x__1*x__2*k + 2*r__1*x__1*x__2 - 2*x__2^2 - 2*x__1*x__2*x__4+2*r__2*x__1*x__3 - 2*x__3^2 + 2*(x__4-x__40)*(-b*x__4 + x__1*x__2) <= -q*(p__1*x__1^2 + x__2^2 + x__3^2 + (x__4 - x__40)^2 - l ) ) ) ), '`Applied Mechanics Problems 1a`' = ':-forall'( [F__1, F__2, F__3], convert( ':-Implies'( ':-And'( 150*(1-0.05) <= F__1, F__1 <= 150*(1+0.05), 700*(1-0.05) <= F__2, F__2 <= 700*(1+0.05), 300*(1-0.05) <= F__3, F__3 <= 300*(1+0.05) ), ':-And'( N__1 <= F__1 - F__2 + F__3, F__1 - F__2 + F__3 <= N__2 ) ), 'rational' ) ), '`Applied Mechanics Problems 2a`' = ':-forall'( p, ':-Implies'( ':-And'( 150*(1-p) <= F__1, F__1 <= 150*(1+p), 700*(1-p) <= F__2, F__2 <= 700*(1+p), 300*(1-p) <= F__3, F__3 <= 300*(1+p) ), ':-And'( N__1 <= F__1 - F__2 + F__3, F__1 - F__2 + F__3 <= N__2 ) ) ), '`Applied Mechanics Problems 1b`' = ':-forall'( [F__1, F__2, F__3], convert( ':-Implies'( ':-And'( 150*(1-0.05) <= F__1, F__1 <= 150*(1+0.05), 700*(1-0.05) <= F__2, F__2 <= 700*(1+0.05), 550*(1-0.05) <= F__3, F__3 <= 550*(1+0.05) ), ':-And'( N__1 <= F__1 - F__2 + F__3, F__1 - F__2 + F__3 <= N__2 ) ), 'rational' ) ), '`Applied Mechanics Problems 2b`' = ':-forall'( p, ':-Implies'( ':-And'( 150*(1-p) <= F__1, F__1 <= 150*(1+p), 700*(1-p) <= F__2, F__2 <= 700*(1+p), 550*(1-p) <= F__3, F__3 <= 550*(1+p) ), ':-And'( N__1 <= F__1 - F__2 + F__3, F__1 - F__2 + F__3 <= N__2 ) ) ), '`Applied Mechanics Problems 1c`' = ':-forall'( [F__1, F__2, F__3], convert( ':-Implies'( ':-And'( 150*(1-0.05) <= F__1, F__1 <= 150*(1+0.05), 700*(1-0.05) <= F__2, F__2 <= 700*(1+0.05), 550*(1-0.05) <= F__3, F__3 <= 550*(1+0.05) ), ':-And'( N__1 <= F__1 - F__2 + F__3, F__1 - F__2 + F__3 <= N__2 ) ), 'rational' ) ), '`Applied Mechanics Problems 2c`' = ':-forall'( p, ':-Implies'( ':-And'( 150*(1-p) <= F__1, F__1 <= 150*(1+p), 700*(1-p) <= F__2, F__2 <= 700*(1+p), 1200*(1-p) <= F__3, F__3 <= 1200*(1+p) ), ':-And'( N__1 <= F__1 - F__2 + F__3, F__1 - F__2 + F__3 <= N__2 ) ) ), '`Applied Mechanics Problems 3x`' = ':-forall'( [F__1, F__2, F__3, F__4], convert( ':-Implies'( ':-And'( 129 <= F__1, F__1 <= 131, 59 <= F__2, F__2 <= 61, 109 <= F__3, F__3 <= 111, 99 <= F__4, F__4 <= 101 ), ':-And'( Nx1 <= 0.866025*F__1 - 0.342020*F__2 + 0.965926*F__4, 0.866025*F__1 - 0.342020*F__2 + 0.965926*F__4 <= Nx2 ) ), 'rational' ) ), '`Applied Mechanics Problems 3y`' = ':-forall'( [F__1, F__2, F__3, F__4], convert( ':-Implies'( ':-And'( 129 <= F__1, F__1 <= 131, 59 <= F__2, F__2 <= 61, 109 <= F__3, F__3 <= 111, 99 <= F__4, F__4 <= 101 ), ':-And'( Ny1 <= 0.5*F__1 - 0.939693*F__2 - F__3 - 0.258819*F__4, 0.5*F__1 - 0.939693*F__2 - F__3 - 0.258819*F__4 <= Ny2 ) ), 'rational' ) ), '`Applied Mechanics Problems 3`' = ':-forall'( Fp, convert( ':-Implies'( ':-And'( N1 > 0, N2 > 0, -1 <= Fp, Fp <= 1 ), ':-And'( N1^2 <= ( 0.866025*(Fp + 130) - 0.342020*(Fp + 60) + 0.965926*(Fp + 100) )^2 + ( 0.5*(Fp + 130) - 0.939693*(Fp + 60) - (Fp + 110) - 0.258819*(Fp + 100) )^2, ( 0.866025*(Fp + 130) - 0.342020*(Fp + 60) + 0.965926*(Fp + 100) )^2 + ( 0.5*(Fp + 130) - 0.939693*(Fp + 60) - (Fp + 110) - 0.258819*(Fp + 100) )^2 <= N2^2 ) ), 'rational' ) ), '`Applied Mechanics Problems 4a`' = ':-exists'( q, ':-Implies'( ':-And'( -1 <= q, q <= 1 ), ':-And'( 525000*(2 + sqrt(2))*u__1 - 525000*sqrt(2)*u__2 - 525000*sqrt(2)*v__2 = 0, -525000*sqrt(2)*u__1 + 52500*sqrt(2)*(q+20)*u__2 - 52500*sqrt(2)*v__2 = 0, -525000*sqrt(2)*u__1 - 52500*sqrt(2)*u__2 + 52500*sqrt(2)*(q+20)*v__2 = -10 ) ) ), '`Applied Mechanics Problems 4b`' = ':-exists'( q, ':-Implies'( ':-And'( -1 <= q, q <= 1 ), ':-And'( (sqrt(2)*q + 10*(2+sqrt(2)))*u__1 - sqrt(2)*(q+10)*(u__2+v__2) = 0, (q+10)*(u__1-2*u__2) = 0, 5250*sqrt(2)*(q+10)*(u__1-2*v__2) = 1 ) ) ), '`RA Triangle Hyp Longer Than Sum of Sides`' = ':-forall'( [ a, b ], ':-Implies'( ':-And'( a > 0, b > 0, a^2 + b^2 = c^2 ), c > a + b ) ) ]): # end QE table ################################################################################ :-`EconomicsAssumptions` := table([ `Supply-Demand: Determinants of quantity 0001` = ':-And'( v__7 < 0, v__8 > 0, v__4 > 0, v__2*v__6 + v__3*v__8 = v__4, v__1*v__5 + v__3*v__7 = v__4, v__6 = 1, v__5 = 1 ), `Supply-Demand: Determinants of quantity 0004` = ':-And'( v__5 = 1, v__6 = 1, v__1*v__5 + v__3*v__7 = v__4, v__2*v__6 + v__3*v__8 = v__4, v__8 > 0, v__7 < 0 ), `Supply-Demand: Price and quantity impact together reveal quantity determinants\ 0006` = ':-And'( v__5 = 1, v__6 = 1, v__1*v__5 + v__3*v__7 = v__4, v__2*v__6 + v__3*v__8 = v__4, v__8 > 0, v__7 < 0 ), `Supply-Demand: Determinants of quantity 0009` = ':-And'( v__5 = 1, v__6 = 1, v__1*v__5 + v__3*v__7 = v__4, v__2*v__6 + v__3*v__8 = v__4, v__8 > 0, v__7 < 0 ), `Supply-Demand Scenarios 0012` = ':-And'( v__2 = 0, v__4 = v__3, v__9 = 1, v__10 = 1, v__11*v__5 + v__1*v__9 = v__7, v__11*v__6 + v__2*v__9 = v__8, v__10*v__3 + v__12*v__5 = v__7, v__10*v__4 + v__12*v__6 = v__8, v__12 < 0, v__7 < 0, v__11 < 0 ), `Supply-Demand: Krugman scenario error 0013` = ':-And'( v__2 = 0, v__4 = v__3, v__9 = 1, v__10 = 1, v__11*v__5 + v__1*v__9 = v__7, v__11*v__6 + v__2*v__9 = v__8, v__10*v__3 + v__12*v__5 = v__7, v__10*v__4 + v__12*v__6 = v__8, v__12 > 0, v__5 < 0, v__7 < 0, v__11 < 0 ), `Supply-Demand: Incidence parameter for scenario analysis 0015` = ':-And'( v__2 = 0, v__4 = v__3, v__5 = 0, v__9 = 1, v__10 = 1, v__11*v__5 + v__1*v__9 = v__7, v__11*v__6 + v__2*v__9 = v__8, v__10*v__3 + v__12*v__5 = v__7, v__10*v__4 + v__12*v__6 = v__8, v__12 > 0, v__7 < 0, v__11 < 0), `Supply-Demand: The missing Krugman condition 0016` = ':-And'( v__2 = 0, v__3 = v__1, v__4 = v__3, v__9 = 1, v__10 = 1, v__11*v__5 + v__1*v__9 = v__7, v__11*v__6 + v__2*v__9 = v__8, v__10*v__3 + v__12*v__5 = v__7, v__10*v__4 + v__12*v__6 = v__8, v__1 > 0, v__12 > 0, v__11 < 0 ), `Supply-Demand: Becker irrational demand 0018` = ':-And'( v__2 = v__1, v__3*v__5 + v__4*v__7 = v__1, v__3*v__6 + v__4*v__7 = v__1, v__3*v__6 + v__4*v__8 = v__2, v__3 > 0, v__4 > 0, v__5 > v__6 ), `NGM (Neoclassical Growth Model): Labor taxes reduce steady-state labor,\ capital, consumption 0021` = ':-And'( v__7 = 0, v__8 = 0, v__21 - v__5 = v__4, v__21*v__7 - v__21 + v__5 + v__6 = 0, v__7 - 1 <> 0, v__19*v__3 + v__2*v__21 = v__12, v__10*v__21 - v__10*v__5 + v__11*v__19 - v__9 = 0, -v__2*v__22 - v__20*v__3 = 0, v__3 <> 0, -v__10*v__15^2*v__22*v__8 - v__11*v__15^2*v__20*v__8 + v__10*v__15^2* v__22 + v__11*v__15^2*v__20 - v__11*v__13*v__16 + v__11*v__14*v__15 - v__13*v__17*v__9 - v__15^2*v__19 + v__15*v__16*v__9 = 0, v__15^2 <> 0, v__2*v__23 - v__22*v__3 = 0, v__2 <> 0, v__10*v__23 + v__11*v__22 = 0, 0 < v__1, 0 < v__2, 0 < v__3, 0 < v__6, 0 < v__15, 0 < -(-v__13*v__16 + v__14*v__15)*v__15^2, 0 < -(-v__13*v__17 + v__15*v__16)*v__15^2, 0 < v__18, 0 < v__19, 0 < v__21, 0 <= v__4, 0 <= v__5, 0 <= v__22, v__7 < 1, v__8 < 1, v__13 < 0, v__14 < 0, v__17 < 0, v__20 < 0, v__14 + v__16*v__19* (1 - v__8) + v__15*v__20*(1 - v__8) < 0, v__23 < 0 ), `NGM: Capital taxes reduce steady-state capital 0022` = ':-And'( v__21 - v__5 = v__4, v__21*v__7 - v__21 + v__5 + v__6 = 0, v__7 - 1 <> 0, v__19*v__3 + v__2*v__21 = v__12, v__10*v__21 - v__10*v__5 + v__11* v__19 - v__9 = 0, -v__2*v__22 - v__20*v__3 = 0, v__3 <> 0, -v__10*v__15^2* v__22*v__8 - v__11*v__15^2*v__20*v__8 + v__10*v__15^2*v__22 + v__11*v__15^2 *v__20 - v__11*v__13*v__16 + v__11*v__14*v__15 - v__13*v__17*v__9 - v__15^2 *v__19 + v__15*v__16*v__9 = 0, v__15^2 <> 0, v__2*v__23 - v__22*v__3 = 0, v__2 <> 0, v__10*v__23 + v__11*v__22 = 0, 0 < v__1, 0 < v__2, 0 < v__3, 0 < v__6, 0 < v__15, 0 < -(-v__13*v__16 + v__14*v__15)*v__15^2, 0 < -(-v__13* v__17 + v__15*v__16)*v__15^2, 0 < v__18, 0 < v__19, 0 < v__21, 0 <= v__4, 0 <= v__5, 0 <= v__22, v__7 < 1, v__8 < 1, v__13 < 0, v__14 < 0, v__17 < 0, v__20 < 0, v__14 + v__16*v__19*(1 - v__8) + v__15*v__20*(1 - v__8) < 0, v__23 < 0 ), `NGM: Capital taxes reduce steady-state consumption 0023` = ':-And'( v__21 - v__5 = v__4, v__21*v__7 - v__21 + v__5 + v__6 = 0, v__7 - 1 <> 0, v__19*v__3 + v__2*v__21 = v__12, v__10*v__21 - v__10*v__5 + v__11* v__19 - v__9 = 0, -v__2*v__22 - v__20*v__3 = 0, v__3 <> 0, -v__10*v__15^2* v__22*v__8 - v__11*v__15^2*v__20*v__8 + v__10*v__15^2*v__22 + v__11*v__15^2 *v__20 - v__11*v__13*v__16 + v__11*v__14*v__15 - v__13*v__17*v__9 - v__15^2 *v__19 + v__15*v__16*v__9 = 0, v__15^2 <> 0, v__2*v__23 - v__22*v__3 = 0, v__2 <> 0, v__10*v__23 + v__11*v__22 = 0, 0 < v__1, 0 < v__2, 0 < v__3, 0 < v__6, 0 < v__15, 0 < -(-v__13*v__16 + v__14*v__15)*v__15^2, 0 < -(-v__13* v__17 + v__15*v__16)*v__15^2, 0 < v__18, 0 < v__19, 0 < v__21, 0 <= v__4, 0 <= v__5, 0 <= v__22, v__7 < 1, v__8 < 1, v__13 < 0, v__14 < 0, v__17 < 0, v__20 < 0, v__14 + v__16*v__19*(1 - v__8) + v__15*v__20*(1 - v__8) < 0, v__23 < 0 ), `NGM: Labor tax impact with separable production 0024` = ':-And'( v__19*v__6 - v__19 + v__4 + v__5 = 0, v__6 - 1 <> 0, 0 < -(-v__11* v__15 + v__13*v__14)*v__13^2, 0 < -(-v__11*v__14 + v__12*v__13)*v__13^2, -v__10*v__13^2*v__18*v__7 - v__13^2*v__20*v__7*v__9 + v__10*v__13^2*v__18 + v__13^2*v__20*v__9 - v_8*v__11*v__15 - v__10*v__11*v__14 - v__10*v__12* v__13 - v__13^2*v__17 - v__13*v__14*v__8 = 0, v__13^2 <> 0, v__10*v_17 - v__8 + v__19*v__9 - v__4*v__9 = 0, v__20 = 0, v__10*v__20 + v__21*v__9 = 0, v__1 > 0, v__2 > 0, v__3 > 0, v__5 > 0, v__13 > 0 , v__16 > 0, v__17 > 0, v__19 > 0, v__4 >= 0, v__20 >= 0, v__6 < 1, v__7 < 1, v__11 < 0, v__12 < 0, v__15 < 0, v__18 < 0, v__12 + v__14*v__17*(1-v__7) + v__13*v__18*(1-v__7) < 0, v__21 < 0 ), `NGM: Labor tax impact with separable production 0025` = ':-And'( v__19*v__6 - v__19 + v__4 + v__5 = 0, v__6 - 1 <> 0, 0 < -(-v__11* v__15 + v__13*v__14)*v__13^2, 0 < -(-v__11*v__14 + v__12*v__13)*v__13^2, -v__10*v__13^2*v__18*v__7 - v__13^2*v__20*v__7*v__9 + v__10*v__13^2*v__18 + v__13^2*v__20*v__9 - v_8*v__11*v__15 - v__10*v__11*v__14 - v__10*v__12* v__13 - v__13^2*v__17 - v__13*v__14*v__8 = 0, v__13^2 <> 0, v__10*v_17 - v__8 + v__19*v__9 - v__4*v__9 = 0, v__20 = 0, v__10*v__20 + v__21*v__9 = 0, v__1 > 0, v__2 > 0, v__3 > 0, v__5 > 0, v__13 > 0 , v__16 > 0, v__17 > 0, v__19 > 0, v__4 >= 0, v__20 >= 0, v__6 < 1, v__7 < 1, v__11 < 0, v__12 < 0, v__15 < 0, v__18 < 0, v__12 + v__14*v__17*(1-v__7) + v__13*v__18*(1-v__7) < 0, v__21 < 0 ), `NGM: Slope of the stable manifold 0026` = ':-And'( v__11 = 0, v__2*v__22 + v__20*v__3 = v__10, v__1 > 0, v__2 > 0, v__3 > 0, v__5 > 0, v__14 > 0, v__19 > 0, v__20 > 0, v__22 > 0, v__4 >= 0, v__23 >= 0, v__6 < 1, v__7 < 1, v__12 < 0, v__13 < 0, v__14 < 0, v__21 < 0, v__24 < 0, v__14*v__22*v__6 - v__11*v__16 - v__14*v__22 + v__14*v__4 + v__14*v__5 = 0, v__16 <> 0, v__2*v__23 - v__21*v__3 = 0, v__3 <> 0, -v__14^2*v__21*v__7*v__9 + v__14^2*v__21*v__9 - v__14^2*v__23*v__7 - v__12* v__15*v__9 - v__12*v__16*v__8 + v__13*v__14*v__9 + v__14^2*v__23 + v__14* v__15*v__8 = 0, v__14^2 <> 0, v__2*v__24 + v__3*v___23 = 0, v__2 <> 0, - v__14*v__17*v__22*v__6*v__9 - v__14*v__18*v__22*v__6*v__8 + v__15*v__16* v__22*v__6*v__9 + v__16^2*v__22*v__6*v__8 - v__14*(1 - v__6)*v__16*v__23* v__9 + v__14*v__17*v__22*v__9 - v__14*v__17*v__4*v__9 - v__14*v__17*v__5* v__9 + v__14*v__18*v__22*v__8 - v__14*v__18*v__4*v__8 - v__14*v__18*v__5* v__8 - v__15*v__16*v__22*v__9 - v__15*v__16*v__4*v__9 + v__15*v__16*v__5* v__9 - v__16^2*v__22*v__8 - v__16^2*v__4*v__8 + v__16^2*v__5*v__8 - v__14* (1 - v__6)*v__16*v__24 = 0, v__16^2 <> 0, 0 < -(-v__12*v__15 + v__13*v__14) *v__14^2, 0 < -(-v__12*v__16 + v__14*v__15)*v__14^2 ), `NGM: The government purchases multiplier 0027` = ':-And'( v__8 = 0, v__1 > 0, v__3 > 0, v__4 > 0, v__4*v__9 > 0, v__10 > 0, v__2 >= 0, -v__10*v__3*v__7 + v__10*v__4*v__6 + v__4*v__7*v__9 - v__4*v__5 - v__4 = 0, v__4 <> 0, -v__11*v__3*v__7 + v__11*v__4*v__6 - v__4^2*v__8 = 0, v__4^2 <> 0, -v__11*v__14^2*v__3^2*v__7 + v__11*v__14^2*v__3*v__4*v__6 + v__12*v__15*v__4^3*v__7 + v__12*v__16*v__4^3*v__5 - v__13*v__14*v__4^3*v__7 - v__14*v__15*v__4^3*v__5 = 0, v__14^2*v__4^3 <> 0, 0 < -(v__10*v__3 - v__4 *v__9)*v__4, 0 < -(-v__12*v__15 + v__13*v__14)*v__14^2, 0 < -(-v__12*v__16 + v__14*v__15)*v__14^2, 0 < -v__11*v__3^2*v__4^3, 0 < -v__11*v__4 ), `NGM: The government purchases multiplier 0028` = ':-And'( v__8 = 0, v__11 = 0, v__10*v__12*v__4 - v__10*v__13*v__3 + v__13* v__4*v__8 - v__4*v__7 + v__4*v__8 - v__4*v__9 - v__4 = 0, v__4 <> 0, v__10* v__20*v__5^2 + v__21*v__5^2*v__7 + 2*v__10*v__20*v__5 - v__16*v__5*v__9 + 2*v__21*v__5*v__7 + v__10*v__20 + v__11*v__14 - v__16*v__9 + v__21*v__7 = 0, (1 + v__5)^2 <> 0, -v__10*v__15*v__19^2*v__3^2 + v__10*v__17*v__20*v__4^3 - v__10*v__18*v__19*v__4^3 + v__15*v__19^2*v__3*v__4*v__8 + v__17*v__21* v__4^3*v__7 - v__19*v__20*v__4^3*v__7 = 0, v__19^2*v__4^3 <> 0, 0 < v__1, 0 < v__3, 0 < v__4, -1 < v__5, 0 < v__12*v__4, 0 < v__13, 0 < -(-v__12* v__4 + v__13*v__3)*v__4, 0 < v__14, 0 < v__19, 0 < -(-v__17*v__20 + v__18* v__19)*v__19^2, 0 < v__18*v__21 - v__20^2, 0 < -(-v__17*v__21 + v__19*v__20) *v__19^2, 0 <= v__2, v__6 < 1, 0 < -v__15*v__3^2*v__4^3, 0 < -v__15* v__4, v__16 < 0, v__17 < 0, v__18 < 0, v__21 < 0, 0 <= v__6 ), `NGM: Signing the impact of purchases on labor, separable case 0029` = ':-And'( v__8 = 0, v__11*v__7 + v__12*v__6 = 1 + v__5, v__13*v__3*v__4* v__7 + v__11*v__3*v__9 + v__11*v__4*v__7 = 1, v__14*v__6 = v__8, v__13* v__17^2*v__4*v__7 + v__11*v__17^2*v__9 - v__13*v__17^2*v__7 + v__15*v__18* v__7 + v__15*v__19*v__5 - v__16*v__17*v__7 - v__17*v__18*v__5 = 0, v__17^2 <> 0, 0 < v__1, 0 < v__3, 0 < v__9, 0 < v__10, 0 < v__11, 0 < v__12, 0 < v__13*v__3 + v__11, 0 < -(-v__15*v__18 + v__16*v__17)*v__17^2, 0 < -(-v__15*v__19 + v__17*v__18)*v__17^2, 0 <= v__2, v__4 < 1, v__14 < 0, 0 <= v__4, v__13 <= 0 ), `NGM: Signing the impact of purchases on labor 0030` = ':-And'( v__9 = 0, v__11*v__4*v__8 - v__12*v__3*v__8 + v__12*v__4*v__7 - v__4*v__6 - v__4 = 0, v__4 <> 0, -v__13*v__3*v__8 + v__13*v__4*v__7 - v__4^2*v__9 = 0, v__4^2 <> 0, v__10*v__11*v__4^3 - v__10*v__12*v__3*v__4^2 + v__11*v__4^2*v__5*v__8 - v__12*v__3*v__4*v__5*v__8 + v__13*v__3^2*v__5* v__8 - v__13*v__3*v__4*v__5*v__7 - v__4^2 = 0, v__4^2 <> 0, v__10*v__11* v__16^2*v__4^3 - v__10*v__12*v__16^2*v__3*v__4^2 + v__13*v__16^2*v__3^2* v__5*v__8 - v__13*v__16^2*v__3*v__4*v__5*v__7 - v__13*v__16^2*v__3^2*v__8 + v__13*v__16^2*v__3*v__4*v__7 + v__14*v__17*v__4^3*v__8 + v__14*v__18* v__4^3*v__6 + v__15*v__16*v__4^3*v__8 - v__16*v__17*v__4^3*v__6 = 0, v__16^2*v__4^3 <> 0, 0 < v__1, 0 < v__3, 0 < v__4, 0 < v__10, 0 < v__11* v__4, 0 < v__12, 0 < -(-v__11*v__4 + v__12*v__3)*v__4, 0 < -(-v__14*v__17 + v__15*v__16)*v__16^2, 0 < -(-v__14*v__18 + v__16*v__17)*v__16^2, 0 <= v__2, v__5 < 1, 0 < -v__13*v__3^2*v__4^3, 0 < -v__13*v__4, 0 <= v__5 ), `Capital taxes in the NGM 0051` = ':-And'( v__21 - v__5 = v__4, v__21*v__7 - v__21 + v__5 + v__6 = 0, -1 + v__7 <> 0, v__19*v__3 + v__2*v__21 = v__12, v__10*v__21 - v__10*v__5 + v__11*v__19 - v__9 = 0, -v__2*v__22 - v__20*v__3 = 0, v__3 <> 0, -v__10* v__15^2*v__22*v__8 - v__11*v__15^2*v__20*v__8 + v__10*v__15^2*v__22 + v__11*v__15^2*v__20 - v__11*v__13*v__16 + v__11*v__14*v__15 - v__13*v__17* v__9 + v__15*v__16*v__9 = 0, v__15^2 <> 0, v__2*v__23 + v__22*v__3 = 0, v__2 <> 0, v__10*v__23*v__7^2 + v__11*v__22*v__7^2 - 2*v__10*v__23*v__7 - 2*v__11*v__22*v__7 + v__10*v__23 + v__11*v__22 - v__5 - v__6 = 0, (-1 + v__7)^2 <> 0, 0 < v__1, 0 < v__2, 0 < v__3, 0 < v__6, 0 < v__15, 0 < -(-v__13*v__16 + v__14*v__15)*v__15^2, 0 < -(-v__13*v__17 + v__15*v__16)* v__15^2, 0 < v__18, 0 < v__19, 0 < v__21, 0 <= v__4, 0 <= v__5, 0 <= v__22, v__7 < 1, v__8 < 1, v__13 < 0, v__14 < 0, v__17 < 0, v__20 < 0, v__14 + v__16*v__19*(1 - v__8) + v__15*v__20*(1 - v__8) < 0, v__23 < 0 ), `NGM: private and public consumption as substitutes 0052` = ':-And'( v__4 = v__3, v__6 = 0, v__9 = 0, v__10 = 1, v__11 = 1, v__12 = 0, v__13 = 0, v__14*v__3 - v__14 - v__4 + 1 = 0, -1 + v__3 <> 0, v__14 = v__10, v__15 = 0, v__16 = 0, v__18 = 0, v__19 = 0, v__20 = 0, v__21 = 0, v__22 = v__5, v__26*(1 - v__3) = v__23*(1 - v__4), -v__10*v__26 + (1 - v__3)*(v__27*(v__6 - v__8) + v__29*v__8) = -v__14*v__23 + (1 - v__4)*(v__24*(v__6 - v__8) + v__27*v__8), -v__18*v__26 - v__10*(v__27*(1 - v__7) + v__29*v__7) + (1 - v__3)*(-v__17*v__27 + v__17*v__29 + (1 - v__7)*(v__28*(v__6 - v__8) + v__30*v__8) + v__7*(v__30*(v__6 - v__8) + v__31*v__8)) - (v__27*(v__6 - v__8) + v__29*v__8)*v__9 = -v__20*v__23 - v__14*(v__24*(1 - v__7) + v__27*v__7) - v__13*(v__24*(v__6 - v__8) + v__27*v__8) + (1 - v__4)*(-v__17*v__24 + v__17*v__27 + (1 - v__7)*(v__25*(v__6 - v__8) + v__28*v__8) + v__7*(v__28*(v__6 - v__8) + v__30*v__8)), v__10*v__34 + v__14*v__32 + v__37*v__6 = v__23*(v__6 - v__8) + v__26*v__8, v__20*v__32 + v__18*v__34 + v__14*v__38 + v__10*v__39 + v__40*v__6 + v__13*(v__10*v__35 + v__14*v__33 + v__38*v__6) + (v__10*v__36 + v__14*v__35 + v__39*v__6)*v__9 = -v__17*v__23 + v__17*v__26 + (1 - v__7)*(v__24*(v__6 - v__8) + v__27*v__8) + v__7*(v__27*(v__6 - v__8) + v__29*v__8), v__2 < v__1, 0 < v__2, 0 < v__22, 0 < v__23, 0 < v__26, 0 < v__27, 0 < v__24*v__29 - v__27^2, v__3 < 1, v__4 < 1, v__24 < 0, v__29 < 0 ), `NGM: Temporary government purchases 0053` = ':-And'( v__7 = 0, v__10 = 0, v__12*v__9 + v__13*v__7 = 1 + v__6 - v__7 + v__8, v__21*v__4^2*v__9 + v__22*v__4^2*v__6 - v__17*v__4*v__8 + 2*v__21* v__4*v__9 + 2*v__22*v__4*v__6 + v__10*v__14 - v__17*v__8 + v__21*v__9 + v__22*v__6 = 0, (1 + v__4)^2 <> 0, -v__15*v__20^2*v__9 + v__18*v__21*v__9 + v__18*v__22*v__6 - v__19*v__20*v__9 - v__20*v__21*v__6 = 0, v__20^2 <> 0, 0 < v__1, 0 < v__3, -1 < v__4, 0 < v__11, 0 < v__12, 0 < v__13, 0 < v__14, 0 < v__15*v__3 + v__12, 0 < v__20, 0 < -(-v__18*v__21 + v__19*v__20)* v__20^2, 0 < v__19*v__22 - v__21^2, 0 < -(-v__18*v__22 + v__20*v__21)* v__20^2, 0 <= v__2, v__5 < 1, v__16 < 0, v__17 < 0, v__18 < 0, v__19 < 0, v__22 < 0, 0 <= v__5, v__15 <= 0 ), `NGM: Temporary government purchases 0054` = ':-And'( v__8 = 0, v__11 = 0, v__10*v__12*v__4 - v__10*v__13*v__3 + v__13*v__4*v__8 - v__4*v__7 + v__4*v__8 - v__4*v__9 - v__4 = 0, v__4 <> 0, v__10*v__20*v__5^2 + v__21*v__5^2*v__7 + 2*v__10*v__20*v__5 - v__16*v__5* v__9 + 2*v__21*v__5*v__7 + v__10*v__20 + v__11*v__14 - v__16*v__9 + v__21* v__7 = 0, (1 + v__5)^2 <> 0, -v__10*v__15*v__19^2*v__3^2 + v__10*v__17* v__20*v__4^3 - v__10*v__18*v__19*v__4^3 + v__15*v__19^2*v__3*v__4*v__8 + v__17*v__21*v__4^3*v__7 - v__19*v__20*v__4^3*v__7 = 0, v__19^2*v__4^3 <> 0, 0 < v__1, 0 < v__3, 0 < v__4, -1 < v__5, 0 < v__12*v__4, 0 < v__13, 0 < -(-v__12*v__4 + v__13*v__3)*v__4, 0 < v__14, 0 < v__19, 0 < -(-v__17*v__20 + v__18*v__19)*v__19^2, 0 < v__18*v__21 - v__20^2, 0 < -(-v__17*v__21 + v__19*v__20)*v__19^2, 0 <= v__2, v__6 < 1, 0 < -v__15*v__3^2*v__4^3, 0 < -v__15*v__4, v__16 < 0, v__17 < 0, v__18 < 0, v__21 < 0, 0 <= v__6 ), `NGM: Permanent government purchases 0055` = ':-And'( v__3 = 1, v__4 = 1, v__5 = 0, v__9 = 0, v__12*v__7 + v__14*v__5 = v__1 + v__3 - v__5 + v__6, v__13*v__8 + v__15*v__6 = v__2 + v__4 - v__6, -v__1*v__27*v__31^2 + v__15*v__2*v__28*v__31 + v__15*v__26*v__31*v__8 + v__18*v__24*v__31*v__6 - v__25*v__31^2*v__7 - 2*v__1*v__27*v__31 + v__15* v__2*v__28 - v__15*v__24*v__9 + v__15*v__26*v__8 + v__18*v__24*v__6 + v__2* v__28*v__31 - 2*v__25*v__31*v__7 + v__26*v__31*v__8 - v__1*v__27 + v__2* v__28 - v__24*v__9 - v__25*v__7 + v__26*v__8 = 0, (1 + v__31)^2 <> 0, -v__16*v__23^2*v__32*v__7 - v__10*v__12*v__23^2 + v__16*v__23^2*v__7 - v__1*v__19*v__27 + v__1*v__23*v__25 - v__19*v__25*v__7 + v__21*v__23*v__7 = 0, v__23^2 <> 0, v__16*v__29*v__32*v__7 + v__10*v__12*v__29 + v__12*v__32* v__7 = v__3, -v__17*v__24^2*v__33*v__8 - v__11*v__13*v__24^2 + v__17* v__24^2*v__8 - v__2*v__20*v__28 + v__2*v__24*v__26 - v__20*v__26*v__8 + v__22*v__24*v__8 = 0, v__24^2 <> 0, v__17*v__30*v__33*v__8 + v__11*v__13* v__30 + v__13*v__33*v__8 = v__4, 0 < v__12, 0 < v__13, 0 < v__15, 0 < v__23, 0 < v__24, 0 < -(-v__19*v__25 + v__21*v__23)*v__23^2, 0 < -(-v__20* v__26 + v__22*v__24)*v__24^2, 0 < v__21*v__27 - v__25^2, 0 < -(-v__19* v__27 + v__23*v__25)*v__23^2, 0 < v__22*v__28 - v__26^2, 0 < -(-v__20* v__28 + v__24*v__26)*v__24^2, 0 < v__29, 0 < v__16*v__29 + v__12, 0 < v__30, 0 < v__17*v__30 + v__13, -1 < v__31, v__18 < 0, v__19 < 0, v__20 < 0, v__21 < 0, v__22 < 0, v__27 < 0, v__28 < 0, v__32 < 1, v__33 < 1, 0 <= v__32, 0 <= v__33, v__10 <= 0, v__11 <= 0, v__16 <= 0, v__17 <= 0 ), `Jehle and Reny Theorem 3.1 with three inputs 0056` = ':-And'( v__1*v__4 + v__2*v__6 + v__3*v__5 = 0, v__1*v__2 + v__10*v__5 + v__6*v__8 = 0, v__1*v__3 + v__10*v__6 + v__11*v__5 = 0, 0 < v__1, 0 < v__5, 0 < v__6, 0 < v__7, 0 < v__9, 0 < v__12, v__11*v__12^2 + v__4*v__9^2 < 2*v__12*v__3*v__9, v__10^2*v__12^2 + 2*v__11*v__12*v__2*v__7 + v__2^2* v__9^2 + v__3^2*v__7^2 < 2*v__2*(v__10*v__12 + v__3*v__7)*v__9 + v__12*(2* v__10*v__3*v__7 + v__11*v__12*v__8 - 2*v__3*v__8*v__9) + v__4*(-2*v__10* v__7*v__9 + v__11*v__7^2 + v__8*v__9^2) ), `A semialgebraic economy's Laffer curve 0057` = ':-And'( v__7^2 = v__1^3, v__8^2 = v__2^3, 27*v__13^3*v__7 = 8, 27*v__14^3* v__8 = 8, v__13*(1 - v__15) = v__5, v__13*(1 - v__15)*(v__7 - v__8) = v__1 - v__4, v__14*(1 - v__16) = v__6, v__14*(1 - v__16)*(-v__7 + v__8) = v__2 - v__3, v__14*v__16*v__8 = v__13*v__15*v__7, 0 < v__1, 0 < v__2, 0 < v__7, 0 < v__8, v__12 < v__9, v__11 < v__10, 0 < (-v__1 + v__3)*(v__11 - v__9), 0 < (-v__10 + v__12)*(-v__2 + v__4), 0 < v__13, 0 < v__14, 0 < v__15, v__15 < v__16, v__16 < 1, v__8 <> v__7 ), `0058` = true, `0059` = ':-And'( v__1 < v__2, v__2 < v__3, v__3 < v__4, v__4 < v__5, v__5 < v__6, v__6 < v__7, v__7 < v__8, v__8 < v__9, v__9 < v__10, v__10 < v__11, v__11 < v__12, v__12 < v__13, v__13 < v__14, v__14 < v__15, v__15 < v__16, v__16 < v__17, v__17 < v__18, v__18 < v__19, v__19 < v__20, v__20 < v__21, v__21 < v__22, v__22 < v__23, v__23 < v__24, v__24 < v__25, v__25 < v__26, v__26 < v__27, v__27 < v__28, v__28 < v__29, v__29 < v__30, v__30 < v__31, v__31 < v__32, v__32 < v__33, v__33 < v__34, v__34 < v__35, v__35 < v__36, v__36 < v__37, v__37 < v__38, v__38 < v__39, v__39 < v__40, v__40 < v__41 ), `Industry Equilibrium: Prices and factor costs 0061` = ':-And'( -v__3*v__5*v__8 + v__1*v__4 = 0, v__3*v__8 <> 0, -v__3*v__6*v__8 + v__2*v__7 = 0, v__3*v__8 <> 0, -v__3*v__9 + v__13 = 0, v__3 <> 0, -v__10*v__4 + v__14 = 0, v__4 <> 0, -v__11*v__7 + v__15 = 0, v__7 <> 0, v__16*v__8 = v__1, v__12*v__7*v__8 - v__16*v__4*v__8 - v__2*v__7 = 0, v__7 <> 0, v__12*v__15*v__7 + v__14*v__16*v__7 - v__15*v__16*v__4 - v__13*v__7 = 0, v__7 <> 0 ), `Industry Equilibrium: Long-run relationship between real output and real wages\ 0062` = ':-And'( -v__3*v__5*v__8 + v__1*v__4 = 0, v__3*v__8 <> 0, -v__3*v__6*v__8 + v__2*v__7 = 0, v__3*v__8 <> 0, v__12 = 0, v__17 = v__8, -v__1*v__9 + v__18 = 0, v__1 <> 0, -v__10*v__2 + v__19 = 0, v__2 <> 0, -v__11*v__3 + v__20 = 0, v__3 <> 0, -v__12*v__4 + v__21 = 0, v__4 <> 0, -v__13*v__7 + v__22 = 0, v__7 <> 0, -v__14*v__8 + v__23 = 0, v__8 <> 0, v__24*v__8 = v__1, v__16*v__7*v__8 - v__24*v__4*v__8 - v__2*v__7 = 0, v__7 <> 0, v__16*v__22*v__7 + v__21*v__24*v__7 - v__22*v__24*v__4 - v__20*v__7 = 0, v__7 <> 0, -v__15*v__17 + v__25*v__3 = 0, v__17 <> 0, v__20*v__25 = v__23 ), `Industry Equilibrium: Adding up for factor shares 0063` = ':-And'( -v__3*v__5*v__8 + v__1*v__4 = 0, v__3*v__8 <> 0, -v__3*v__6*v__8 + v__2*v__7 = 0, v__3*v__8 <> 0, v__7*v__9 = v__3, v__10*v__8 = v__1, -v__10*v__4*v__8 + v__7*v__8*v__9 - v__2*v__7 = 0, v__7 <> 0 ), `Industry Equilibrium: Input and output quantities 0064` = ':-And'( -v__3*v__5*v__7 + v__1*v__4 = 0, v__3*v__7 <> 0, v__11 = 0, v__14*v__6 = v__3, -v__1*v__8 + v__15 = 0, v__1 <> 0, -v__2*v__9 + v__16 = 0, v__2 <> 0, -v__10*v__3 + v__17 = 0, v__3 <> 0, -v__11*v__4 + v__18 = 0, v__4 <> 0, -v__12*v__6 + v__19 = 0, v__6 <> 0, -v__13*v__7 + v__20 = 0, v__7 <> 0, v__22*v__7 = v__1, v__14*v__6*v__7 - v__22*v__4*v__7 - v__2*v__6 = 0, v__6 <> 0, v__1*v__15*v__21 + v__1*v__16*v__23 - v__15*v__2*v__23 - v__1*v__20 = 0, v__1 <> 0, v__18*v__24*v__6*v__7 - v__19*v__24*v__4*v__7 + v__20*v__22*v__6^2 - v__15*v__6^2 = 0, v__6^2 <> 0, v__14*v__20*v__6^3 - v__18*v__24*v__4*v__6*v__7 + v__19*v__24*v__4^2*v__7 - v__20*v__22*v__4*v__6^2 - v__16*v__6^3 = 0, v__6^3 <> 0 ), `Industry Equilibrium: Marshall's Law 0065` = ':-And'( -v__3*v__5*v__8 + v__1*v__4 = 0, v__3*v__8 <> 0, -v__3*v__6*v__8 + v__2*v__7 = 0, v__3*v__8 <> 0, v__12 = 0, v__12*v__16 - v__13*v__16 - v__10 + v__9 = 0, v__12 - v__13 <> 0, v__17*v__7 = v__3, v__18 = v__8, -v__1*v__9 + v__19 = 0, v__1 <> 0, -v__10*v__2 + v__20 = 0, v__2 <> 0, -v__11*v__3 + v__21 = 0, v__3 <> 0, -v__12*v__4 + v__22 = 0, v__4 <> 0, -v__13*v__7 + v__23 = 0, v__7 <> 0, -v__14*v__8 + v__24 = 0, v__8 <> 0, v__26*v__8 = v__1, v__17*v__7*v__8 - v__26*v__4*v__8 - v__2*v__7 = 0, v__7 <> 0, v__17*v__23*v__7 + v__22*v__26*v__7 - v__23*v__26*v__4 - v__21*v__7 = 0, v__7 <> 0, -v__15*v__18 + v__27*v__3 = 0, v__18 <> 0, v__21*v__27 = v__24, v__1*v__19*v__25 + v__1*v__20*v__28 - v__19*v__2*v__28 - v__1*v__24 = 0, v__1 <> 0, v__22*v__29*v__7*v__8 - v__23*v__29*v__4*v__8 + v__24*v__26*v__7^2 - v__19*v__7^2 = 0, v__7^2 <> 0, v__17*v__24*v__7^3 - v__22*v__29*v__4*v__7*v__8 + v__23*v__29*v__4^2*v__8 - v__24*v__26*v__4*v__7^2 - v__20*v__7^3 = 0, v__7^3 <> 0 ), `Industry Equilibrium: Determinants of long-run capital-labor complementarity\ 0066` = ':-And'( 5 + v__6 = 1, v__12 = v__10 + v__5*(-v__10 + v__9), v__11*v__13* v__6 = v__12, v__11*(v__13*v__6 - v__14*v__5) = v__10, 0 < v__1, 0 < v__2, 0 < v__3, 0 < v__4, 0 < v__7, 0 < v__8, 0 < v__16, 0 < -(-v__1*v__15 + v__16*v__2)*v__1, 0 < v__6, v__6 < 1 ), `Industry Equilibrium: Determinants of short-run capital-labor complementarity\ 0067` = ':-And'( v__5 + v__6 = 1, -v__3*v__5*v__8 + v__1*v__4 = 0, v__3*v__8 <> 0, -v__3*v__6*v__8 + v__2*v__7 = 0, v__3*v__8 <> 0, v__9 = 0, v__12*v__16 - v__13*v__16 - v__10 + v__9 = 0, v__12 - v__13 <> 0, v__18 = v__8, -v__1*v__9 + v__19 = 0, v__1 <> 0, -v__10*v__2 + v__20 = 0, v__2 <> 0, -v__11*v__3 + v__21 = 0, v__3 <> 0, -v__12*v__4 + v__22 = 0, v__4 <> 0, -v__13*v__7 + v__23 = 0, v__7 <> 0, -v__14*v__8 + v__24 = 0, v__8 <> 0, v__27*v__8 = v__1, v__17*v__7*v__8 - v__27*v__4*v__8 - v__2*v__7 = 0, v__7 <> 0, v__17*v__23*v__7 + v__22*v__27*v__7 - v__23*v__27*v__4 - v__21*v__7 = 0, v__7 <> 0, -v__15*v__18 + v__28*v__3 = 0, v__18 <> 0, v__21*v__28 = v__24, v__1*v__19*v__25 + v__1*v__20*v__29 - v__19*v__2*v__29 - v__1*v__24 = 0, v__1 <> 0, v__22*v__31*v__7*v__8 - v__23*v__31*v__4*v__8 + v__24*v__27*v__7^2 - v__19*v__7^2 = 0, v__7^2 <> 0, v__17*v__24*v__7^3 - v__22*v__31*v__4*v__7*v__8 + v__23*v__31*v__4^2*v__8 - v__24*v__27*v__4*v__7^2 - v__20*v__7^3 = 0, v__7^3 <> 0, 0 < v__1, 0 < v__2, 0 < v__3, 0 < v__4, 0 < v__7, 0 < v__8, 0 < v__30, 0 < -(-v__1*v__26 + v__2*v__30)*v__1, 0 < v__6, v__6 < 1 ), `Supply-Demand: Global demand analysis 0074` = ':-And'( v__5 = v__2, v__6 = v__3, 0 < (v__5 - v__6)*(v__7 - v__8), v__3 < v__4, (v__1 - v__3)*(v__7 - v__8) < 0, (v__2 - v__4)*(v__7 - v__8) < 0 ), `Vector mode: Variance of a sum 0076` = ':-And'( v__9 = v__7 + v__8, (-v__7 + x)*(-v__8 + y) >= 0 ), # but actually vector product `Vector mode: Variance of a sum 0077` = ':-And'( v__9 = v__7 + v__8, 1 <= v__1, 0 <= v__4, v__2^2 <= v__1*v__4, 0 <= v__6, v__3^2 <= v__1*v__6, v__5^2 <= v__4*v__6, ':-Or'( (-v__1*v__7*v__8 + v__2*v__8 + v__3*v__7 - v__5)*v__1 < 0, ':-And'( -v__1*v__7*v__8 + v__2* v__8 + v__3*v__7 - v__5 = 0, v__1 <> 0 ) ) ), `Vector mode: Hicks' generalized law of demand 0078` = ':-And'( 0 <= v__1, 0 <= v__10, v__4^2 <= v__1*v__10, 0 <= v__5, v__2^2 <= v__1*v__5, v__7^2 <= v__10*v__5, v__1*v__7^2 + v__10*v__2^2 + v__4^2*v__5 <= v__1*v__10*v__5 + 2*v__2*v__4*v__7, 0 <= v__8, v__3^2 <= v__1*v__8, v__9^2 <= v__10*v__8, v__6^2 <= v__5*v__8, v__1*v__6^2 + v__2^2*v__8 + v__3^2*v__5 <= v__1*v__5*v__8 + 2*v__2*v__3*v__6, v__1*v__9^2 + v__10*v__3^2 + v__4^2*v__8 <= v__1*v__10*v__8 + 2*v__3*v__4*v__9, v__1*v__10*v__6^2 + v__10*v__2^2*v__8 + v__1*v__7^2*v__8 + v__1*v__5*v__9^2 + 2*v__4*(v__3*(-v__5*v__9 + v__6*v__7) + v__2*(v__6*v__9 - v__7*v__8)) <= v__3^2*(-v__10*v__5 + v__7^2) + v__1*v__10*v__5*v__8 + v__4^2*(-v__5*v__8 + v__6^2) + 2*v__1*v__6*v__7*v__9 + v__2^2*v__9^2 + 2*v__2*v__3*(v__10*v__6 - v__7*v__9), v__10*v__6^2 + v__7^2*v__8 <= 2*v__6*v__7*v__9 + v__5*(v__10*v__8 - v__9^2), v__2 <= v__3, v__9 <= v__7 ), `Vector mode: Progressive policy and inequality 0079` = ':-And'( v__1*v__3 < v__5, 0 <= v__1^2, 0 <= v__4, 0 <= v__6, v__3^2 <= v__2*v__6, v__5^2 <= v__4*v__6 ), `Vector mode: Consumer Theory Adding Up 0080` = ':-And'( v__2*v__5 = 0, v__1*v__9 = v__5, 0 < v__1, 0 < v__2 ), `Vector mode: Constant absolute risk aversion 0082` = ':-And'( v__6 = v__3, v__1*((-1 + v__10)*v__3 + (1 - 2*v__10)*v__6 + v__10*v__8) = 0, 0 < v__1, 2*v__6 < v__3 + v__8, 0 <= v__4, 0 <= v__7, v__5^2 <= v__4*v__7, 0 <= v__9, v__3^2 <= v__2*v__9, v__6^2 <= v__4*v__9, v__8^2 <= v__7*v__9, v__5^2*v__9 + v__6^2*v__7 <= 2*v__5*v__6*v__8 + v__4*(v__7*v__9 - v__8^2) ), `Vector mode: Constant absolute risk aversion 0083` = ':-And'( v__3 - v__6 = 0, v__1*v__2 <> 0, v__10*v__3 - 2*v__10*v__6 + v__10*v__8 - v__3 + v__6 = 0, v__2 <> 0, 0 < v__1, 0 < v__4, 0 < v__1*v__2*(v__3 - 2*v__6 + v__8), 0 < v__1^2*v__9, 1 <= v__2, 0 <= v__4, 0 <= v__7, v__5^2 <= v__4*v__7, 0 <= v__9, v__3^2 <= v__2*v__9, v__6^2 <= v__4*v__9, v__8^2 <= v__7*v__9, v__5^2*v__9 + v__6^2*v__7 <= 2*v__5*v__6*v__8 + v__4*(v__7*v__9 - v__8^2) ), `Vector mode: Constant relative risk aversion 0084` = ':-And'( v__3*(v__10*v__2 + v__2*v__5 - 2*v__2*v__8 - v__5 + v__8) = 0, v__1*v__4 <> 0, v__3*(v__1*v__10*v__12*v__3 + v__1*v__12*v__3*v__5 - 2*v__1*v__12*v__3*v__8 + v__1*v__10*v__2 + v__1*v__2*v__5 - 2*v__1*v__2*v__8 - v__1*v__5 + v__1*v__8 + v__10*v__2 + v__2*v__5 - 2*v__2*v__8 - v__5 + v__8) = 0, v__1*v__4 <> 0, 0 < v__1, 0 < v__3, 1 <= v__4, 0 <= v__6, 0 <= v__9, v__7^2 <= v__6*v__9, 0 <= v__11, v__5^2 <= v__11*v__4, v__8^2 <= v__11*v__6, v__10^2 <= v__11*v__9, v__11*v__7^2 + v__8^2*v__9 <= 2*v__10*v__7*v__8 + v__6*(-v__10^2 + v__11*v__9), v__3^2*v__4*(v__10 + v__5 - 2*v__8) < 0, 0 <= v__2, v__2 <= 1 ), `Vector mode: Correlation between wealth and marginal utility 0085` = ':-And'( -v__1*v__3 + v__4 = 0, v__3 <> 0, -v__2*v__3 + v__5 = 0, v__3 <> 0, v__5 - v__7 = 0, v__3 <> 0, 0 < -(v__3 - v__4)*v__3, 0 < v__3*v__5, 1 <= v__3, 0 <= v__6, v__4^2 <= v__3*v__6, 0 <= v__8, v__5^2 <= v__3*v__8, v__7^2 <= v__6*v__8 ), `Vector mode: Risk aversion reduces investment 0086` = ':-And'( v__12*v__19 + v__19*v__3 - 2*v__19*v__8 - v__2 + v__7 = 0, v__1 <> 0, 0 < v__13, 1 <= v__1, 0 <= v__4, 0 <= v__9, v__5^2 <= v__4*v__9, 0 <= v__13, v__6^2 <= v__13*v__4, v__10^2 <= v__13*v__9, v__13*v__5^2 + v__6^2*v__9 <= 2*v__10*v__5*v__6 + v__4*(-v__10^2 + v__13*v__9), 0 <= v__16, v__2^2 <= v__1*v__16, v__7^2 <= v__16*v__4, v__11^2 <= v__16*v__9, v__14^2 <= v__13*v__16, v__16*v__5^2 + v__7^2*v__9 <= 2*v__11*v__5*v__7 + v__4*(-v__11^2 + v__16*v__9), v__11^2*v__13*v__4 + v__10^2*v__16*v__4 + v__13*v__16*v__5^2 + v__14^2*v__4*v__9 + 2*v__7*((v__10*v__14 - v__11*v__13)*v__5 + v__6*(v__10*v__11 - v__14*v__9)) <= 2*v__10*v__11*v__14*v__4 + v__14^2*v__5^2 + 2*(v__10*v__16 - v__11*v__14)*v__5*v__6 + v__13*v__16*v__4*v__9 + v__7^2*(v__10^2 - v__13*v__9) + v__6^2*(v__11^2 - v__16*v__9), v__13*v__7^2 + v__16*v__6^2 <= (v__13*v__16 - v__14^2)*v__4 + 2*v__14*v__6*v__7, v__10^2*v__16 + v__11^2*v__13 <= 2*v__10*v__11*v__14 + (v__13*v__16 - v__14^2)*v__9, 0 <= v__18, v__3^2 <= v__1*v__18, v__8^2 <= v__18*v__4, v__12^2 <= v__18*v__9, v__15^2 <= v__13*v__18, v__17^2 <= v__16*v__18, v__18*v__5^2 + v__8^2*v__9 <= 2*v__12*v__5*v__8 + v__4*(-v__12^2 + v__18*v__9), v__12^2*v__13*v__4 + v__10^2*v__18*v__4 + v__13*v__18*v__5^2 + v__15^2*v__4*v__9 + 2*v__8*((v__10*v__15 - v__12*v__13)*v__5 + v__6*(v__10*v__12 - v__15*v__9)) <= 2*v__10*v__12*v__15*v__4 + v__15^2*v__5^2 + 2*(v__10*v__18 - v__12*v__15)*v__5*v__6 + v__13*v__18*v__4*v__9 + v__8^2*(v__10^2 - v__13*v__9) + v__6^2*(v__12^2 - v__18*v__9), v__12^2*v__16*v__4 + v__11^2*v__18*v__4 + v__16*v__18*v__5^2 + v__17^2*v__4*v__9 + 2*v__8*((v__11*v__17 - v__12*v__16)*v__5 + v__7*(v__11*v__12 - v__17*v__9)) <= 2*v__11*v__12*v__17*v__4 + v__17^2*v__5^2 + 2*(v__11*v__18 - v__12*v__17)*v__5*v__7 + v__16*v__18*v__4*v__9 + v__8^2*(v__11^2 - v__16*v__9) + v__7^2*(v__12^2 - v__18*v__9), v__13*v__8^2 + v__18*v__6^2 <= (v__13*v__18 - v__15^2)*v__4 + 2*v__15*v__6*v__8, v__10^2*v__18 + v__12^2*v__13 <= 2*v__10*v__12*v__15 + (v__13*v__18 - v__15^2)*v__9, v__15^2*v__16*v__4 + v__13*v__17^2*v__4 + v__14^2*v__18*v__4 + v__16*v__18*v__6^2 + 2*((v__14*v__17 - v__15*v__16)*v__6 + (-v__13*v__17 + v__14*v__15)*v__7)*v__8 <= 2*v__14*v__15*v__17*v__4 + v__13*v__16*v__18*v__4 + v__17^2*v__6^2 + 2*(v__14*v__18 - v__15*v__17)*v__6*v__7 + (-v__13*v__18 + v__15^2)*v__7^2 + (-v__13*v__16 + v__14^2)*v__8^2, 2*v__12*(v__11*(-v__13*v__17 + v__14*v__15) + v__10*(v__14*v__17 - v__15*v__16)) + v__10^2*v__16*v__18 + v__15^2*v__16*v__9 + v__13*v__17^2*v__9 + v__14^2*v__18*v__9 <= v__12^2*(-v__13*v__16 + v__14^2) + v__10^2*v__17^2 + v__11^2*(-v__13*v__18 + v__15^2) + 2*v__10*v__11*(v__14*v__18 - v__15*v__17) + 2*v__14*v__15*v__17*v__9 + v__13*v__16*v__18*v__9, v__16*v__8^2 + v__18*v__7^2 <= (v__16*v__18 - v__17^2)*v__4 + 2*v__17*v__7*v__8, v__11^2*v__18 + v__12^2*v__16 <= 2*v__11*v__12*v__17 + (v__16*v__18 - v__17^2)*v__9, v__14^2*v__18 + v__15^2*v__16 <= 2*v__14*v__15*v__17 + v__13*(v__16*v__18 - v__17^2), 2*v__11*v__12*v__14*v__15*v__4 + v__12^2*v__13*v__16*v__4 + 2*v__10*v__12*v__14*v__17*v__4 + 2*v__10*v__11*v__15*v__17*v__4 + v__11^2*v__13*v__18*v__4 + v__10^2*v__16*v__18*v__4 + 2*v__14*v__15*v__17*v__5^2 + v__13*v__16*v__18*v__5^2 + 2*v__12*v__15*v__16*v__5*v__6 + 2*v__10*v__17^2*v__5*v__6 + 2*v__11*v__14*v__18*v__5*v__6 + 2*v__11*v__12*v__17*v__6^2 + v__15^2*v__16*v__4*v__9 + v__13*v__17^2*v__4*v__9 + v__14^2*v__18*v__4*v__9 + v__16*v__18*v__6^2*v__9 + 2*v__8*((v__12*(-v__13*v__16 + v__14^2) + v__11*(v__13*v__17 - v__14*v__15) + v__10*(-v__14*v__17 + v__15*v__16))*v__5 + v__7*(-v__10*v__12*v__14 + v__11*(-v__10*v__15 + v__12*v__13) + v__10^2*v__17 + (-v__13*v__17 + v__14*v__15)*v__9) + v__6*(v__11^2*v__15 + v__10*v__12*v__16 - v__11*(v__10*v__17 + v__12*v__14) + (v__14*v__17 - v__15*v__16)*v__9)) + 2*v__7*((v__12*(v__13*v__17 - v__14*v__15) + v__11*(-v__13*v__18 + v__15^2) + v__10*(v__14*v__18 - v__15*v__17))*v__5 + v__6*(v__12^2*v__14 - v__12*(v__10*v__17 + v__11*v__15) + v__10*v__11*v__18 + (-v__14*v__18 + v__15*v__17)*v__9)) <= v__12^2*v__14^2*v__4 + v__11^2*v__15^2*v__4 + 2*v__10*v__12*v__15*v__16*v__4 + 2*v__11*v__12*v__13*v__17*v__4 + v__10^2*v__17^2*v__4 + 2*v__10*v__11*v__14*v__18*v__4 + v__15^2*v__16*v__5^2 + v__13*v__17^2*v__5^2 + v__14^2*v__18*v__5^2 + 2*v__12*v__14*v__17*v__5*v__6 + 2*v__11*v__15*v__17*v__5*v__6 + 2*v__10*v__16*v__18*v__5*v__6 + v__12^2*v__16*v__6^2 + v__11^2*v__18*v__6^2 + 2*v__14*v__15*v__17*v__4*v__9 + v__13*v__16*v__18*v__4*v__9 + v__17^2*v__6^2*v__9 + v__8^2*(v__11^2*v__13 - 2*v__10*v__11*v__14 + v__10^2*v__16 + (-v__13*v__16 + v__14^2)*v__9) + v__7^2*(v__12^2*v__13 - 2*v__10*v__12*v__15 + v__10^2*v__18 + (-v__13*v__18 + v__15^2)*v__9), v__7 < v__2, v__1*(v__12 + v__3 - 2*v__8) < 0 ), `Constant absolute risk aversion with states delineated 1001` = ':-And'( v__3 < 1, (-1 + v__27)^2*v__93 + (-1 + v__28)^2*v__94 + (-1 + v__29)^2*v__95 + (-1 + v__30)^2*v__96 + (-1 + v__31)^2*v__97 + (-1 + v__32)^2*v__98 + (-1 + v__33)^2*v__99 + v__100*(-1 + v__34)^2 + v__101*(-1 + v__35)^2 + (-1 + v__3)^2*v__69 + (-1 + v__4)^2*v__70 + (-1 + v__5)^2*v__71 + (-1 + v__6)^2*v__72 + (-1 + v__7)^2*v__73 + (-1 + v__10)^2*v__76 + (-1 + v__11)^2*v__77 + (-1 + v__12)^2*v__78 + (-1 + v__13)^2*v__79 + v__74*(-1 + v__8)^2 + (-1 + v__14)^2*v__80 + (-1 + v__15)^2*v__81 + (-1 + v__16)^2*v__82 + (-1 + v__17)^2*v__83 + (-1 + v__18)^2*v__84 + (-1 + v__19)^2*v__85 + (-1 + v__20)^2*v__86 + (-1 + v__21)^2*v__87 + (-1 + v__22)^2*v__88 + (-1 + v__23)^2*v__89 + v__75*(-1 + v__9)^2 + (-1 + v__24)^2*v__90 + (-1 + v__25)^2*v__91 + (-1 + v__26)^2*v__92 < 0, 0 < v__1, 33 < v__8 + v__14 + v__15 + v__16 + v__17 + v__18 + v__19 + v__20 + v__21 + v__3 + v__22 + v__23 + v__9 + v__24 + v__25 + v__26 + v__27 + v__28 + v__29 + v__30 + v__31 + v__32 + v__33 + v__34 + v__35 + v__4 + v__5 + v__6 + v__7 + v__10 + v__11 + v__12 + v__13, (-1 + v__26)*v__59 + v__39*(-1 + v__6) + (-1 + v__27)*v__60 + (-1 + v__28)*v__61 + (-1 + v__29)*v__62 + (-1 + v__30)*v__63 + (-1 + v__31)*v__64 + (-1 + v__32)*v__65 + (-1 + v__33)*v__66 + (-1 + v__34)*v__67 + (-1 + v__35)*v__68 + (-1 + v__12)*v__45 + (-1 + v__13)*v__46 + (-1 + v__14)*v__47 + (-1 + v__15)*v__48 + (-1 + v__16)*v__49 + v__38*(-1 + v__5) + (-1 + v__17)*v__50 + (-1 + v__18)*v__51 + (-1 + v__19)*v__52 + (-1 + v__20)*v__53 + (-1 + v__21)*v__54 + (-1 + v__22)*v__55 + (-1 + v__23)*v__56 + (-1 + v__24)*v__57 + (-1 + v__25)*v__58 + v__42*(-1 + v__9) + (-1 + v__3)*v__36 + v__37*(-1 + v__4) + (-1 + v__10)*v__43 + (-1 + v__11)*v__44 + v__40*(-1 + v__7) + v__41*(-1 + v__8) = 0, v__69 = -v__1*v__36, v__70 = -v__1*v__37, v__71 = -v__1*v__38, v__72 = -v__1*v__39, v__73 = -v__1*v__40, v__74 = -v__1*v__41, v__75 = -v__1*v__42, v__76 = -v__1*v__43, v__77 = -v__1*v__44, v__78 = -v__1*v__45, v__79 = -v__1*v__46, v__80 = -v__1*v__47, v__81 = -v__1*v__48, v__82 = -v__1*v__49, v__83 = -v__1*v__50, v__84 = -v__1*v__51, v__85 = -v__1*v__52, v__86 = -v__1*v__53, v__87 = -v__1*v__54, v__88 = -v__1*v__55, v__89 = -v__1*v__56, v__90 = -v__1*v__57, v__91 = -v__1*v__58, v__92 = -v__1*v__59, v__93 = -v__1*v__60, v__94 = -v__1*v__61, v__95 = -v__1*v__62, v__96 = -v__1*v__63, v__97 = -v__1*v__64, v__98 = -v__1*v__65, v__99 = -v__1*v__66, v__100 = -v__1*v__67, v__101 = -v__1*v__68, (-1 + v__15)*(v__15*v__2 - v__2 + 1)*v__81 + (-1 + v__16)*(v__16*v__2 - v__2 + 1)*v__82 + (-1 + v__17)*(v__17*v__2 - v__2 + 1)*v__83 + (-1 + v__18)*(v__18*v__2 - v__2 + 1)*v__84 + (-1 + v__19)*(v__19*v__2 - v__2 + 1)*v__85 + (-1 + v__20)*(v__2*v__20 - v__2 + 1)*v__86 + (-1 + v__21)*(v__2*v__21 - v__2 + 1)*v__87 + (-1 + v__22)*(v__2*v__22 - v__2 + 1)*v__88 + (-1 + v__23)*(v__2*v__23 - v__2 + 1)*v__89 + v__75*(-1 + v__9)*(v__2*v__9 - v__2 + 1) + (-1 + v__24)*(v__2*v__24 - v__2 + 1)*v__90 + v__100*(-1 + v__34)*(v__2*v__34 - v__2 + 1) + v__101*(-1 + v__35)*(v__2*v__35 - v__2 + 1) + (-1 + v__3)*(v__2*v__3 - v__2 + 1)*v__69 + (-1 + v__4)*(v__2*v__4 - v__2 + 1)*v__70 + (-1 + v__5)*(v__2*v__5 - v__2 + 1)*v__71 + (-1 + v__6)*(v__2*v__6 - v__2 + 1)*v__72 + (-1 + v__7)*(v__2*v__7 - v__2 + 1)*v__73 + (-1 + v__10)*(v__10*v__2 - v__2 + 1)*v__76 + (-1 + v__11)*(v__11*v__2 - v__2 + 1)*v__77 + (-1 + v__12)*(v__12*v__2 - v__2 + 1)*v__78 + (-1 + v__13)*(v__13*v__2 - v__2 + 1)*v__79 + v__74*(-1 + v__8)*(v__2*v__8 - v__2 + 1) + (-1 + v__14)*(v__14*v__2 - v__2 + 1)*v__80 + (-1 + v__25)*(v__2*v__25 - v__2 + 1)*v__91 + (-1 + v__26)*(v__2*v__26 - v__2 + 1)*v__92 + (-1 + v__27)*(v__2*v__27 - v__2 + 1)*v__93 + (-1 + v__28)*(v__2*v__28 - v__2 + 1)*v__94 + (-1 + v__29)*(v__2*v__29 - v__2 + 1)*v__95 + (-1 + v__30)*(v__2*v__30 - v__2 + 1)*v__96 + (-1 + v__31)*(v__2*v__31 - v__2 + 1)*v__97 + (-1 + v__32)*(v__2*v__32 - v__2 + 1)*v__98 + (-1 + v__33)*(v__2*v__33 - v__2 + 1)*v__99 = 0 ) ]): :-`EconomicsHypotheses` := table([ `Supply-Demand: Determinants of quantity 0001` = ( v__1 > 0 ), `Supply-Demand: Determinants of quantity 0004` = ':-Or'( v__1 > 0, v__2 > 0, v__4 <= 0 ), `Supply-Demand: Price and quantity impact together reveal quantity determinants\ 0006` = ':-Or'( v__1 > 0, v__3 <= 0, v__4 <= 0 ), `Supply-Demand: Determinants of quantity 0009` = ':-Or'( v__4 >= 0, v__1 < 0, v__2 < 0 ), `Supply-Demand Scenarios 0012` = ':-Or'( v__5 >= 0, v__7 < v__8 ), `Supply-Demand: Krugman scenario error 0013` = ':-And'( v__7 < 2*v__8, v__8 < 0 ), `Supply-Demand: Incidence parameter for scenario analysis 0015` = ':-And'( v__11*v__7 - v__11*v__8 + v__12*v__8 = 0, v__11 - v__12 <> 0, -v__11*v__7 + v__11*v__8 - v__12*v__8 = 0, v__11 - v__12 <> 0 ), `Supply-Demand: The missing Krugman condition 0016` = ':-Or'( ':-And'( v7 > 0 , 2*v8 > v7, 2*v6 < v5 ), v12 >= -v11 ), `Supply-Demand: Becker irrational demand 0018` = ( v7 < v8 ), `NGM (Neoclassical Growth Model): Labor taxes reduce steady-state labor,\ capital, consumption 0021` = ':-And'( v9 < 0 , v10 < 0 , v11 < 0 ), `NGM: Capital taxes reduce steady-state capital 0022` = ( v__10 < 0 ), `NGM: Capital taxes reduce steady-state consumption 0023` = ( v__9 < 0 ), `NGM: Labor tax impact with separable production 0024` = ':-And'( v__9 = 0, v__10 < 0 ), `NGM: Labor tax impact with separable production 0025` = ( v__8 < 0 ), `NGM: Slope of the stable manifold 0026` = ( v__8 < 0 ), `NGM: The government purchases multiplier 0027` = ':-And'( 0 < v__6, 0 < v__7, -1 < v__5, 0 < -(v__10*v__3*v__7 - v__10*v__4*v__6 - v__4*v__7*v__9)*v__4, v__5 < 0, 0 < -(-v__10*v__3*v__7 + v__10*v__4*v__6 + v__4*v__7*v__9 - v__4)*v__4 ), `NGM: The government purchases multiplier 0028` = ':-And'( 0 < v__10, -1 < v__7, 0 < -(-v__10*v__12*v__4 + v__10*v__13*v__3 - v__13*v__4*v__8)*v__4, v__7 < 0, v__9 < 0, 0 < -v__4*(v__10*v__12*v__4 - v__10*v__13*v__3 + v__13*v__4*v__8 - v__4) ), `NGM: Signing the impact of purchases on labor, separable case 0029` = ':-Or'( ':-And'( v__7 = 0, -v__11*v__17^2*v__9 + v__15*v__19 - v__17*v__18 = 0, v__17^2 <> 0), 0 < -v__7*(v__11*v__17^2*v__9 - v__15*v__19 + v__17*v__18) *v__17^2 ), `NGM: Signing the impact of purchases on labor 0030` = ':-Or'( ':-And'( v__8 = 0, -v__10*v__11*v__16^2*v__4 + v__10*v__12*v__16^2* v__3 + v__14*v__18*v__4 - v__16*v__17*v__4 = 0, v__16^2*v__4 <> 0 ), 0 < -(v__10*v__11*v__16^2*v__4 - v__10*v__12*v__16^2*v__3 - v__14*v__18*v__4 + v__16*v__17*v__4)*v__8*v__16^2*v__4 ), `Capital taxes in the NGM 0051` = ( v__10 < 0 ), `NGM: private and public consumption as substitutes 0052` = ( v__38 + v__39 = 0 ), `NGM: Temporary government purchases 0053` = ':-And'( v__9 > 0, -1 < v__6, 0 < v__12*v__9, v__6 < 0, v__8 < 0, v__12*v__9 < 1 ), `NGM: Temporary government purchases 0054` = ':-And'( 0 < v__10, -1 < v__7, 0 < -(-v__10*v__12*v__4 + v__10*v__13*v__3 - v__13*v__4*v__8)*v__4, v__7 < 0, v__9 < 0, 0 < -v__4*(v__10*v__12*v__4 - v__10*v__13*v__3 + v__13*v__4*v__8 - v__4) ), `NGM: Permanent government purchases 0055` = ( v__7 > 0 ), `Jehle and Reny Theorem 3.1 with three inputs 0056` = ':-And'( v__2^2 <= v__4*v__8, v__3^2 <= v__11*v__4, v__10^2 <= v__8*v__11, 2*v__10*v__2*v__3 <= v__10^2*v__4 + v__3^2*v__8 + v__11*(v__2^2 - v__4*v__8), v__4 <= 0, v__8 <= 0, v__11 <= 0 ), `A semialgebraic economy's Laffer curve 0057` = ( v__9 > v__10 ), `0058` = ':-And'( v__2 <= v__1, v__3 <= v__1, v__4 <= v__1, v__5 <= v__1, v__6 <= v__1, v__7 <= v__1, v__8 <= v__1, v__9 <= v__1, v__10 <= v__1, v__11 <= v__1, v__12 <= v__1, v__13 <= v__1, v__14 <= v__1, v__15 <= v__1, v__16 <= v__1, v__17 <= v__1, v__18 <= v__1, v__19 <= v__1, v__20 <= v__1, v__21 <= v__1, 1 <= 2*v__1, v__1 <= v__2, v__3 <= v__2, v__4 <= v__2, v__5 <= v__2, v__6 <= v__2, v__7 <= v__2, v__8 <= v__2, v__9 <= v__2, v__10 <= v__2, v__11 <= v__2, v__12 <= v__2, v__13 <= v__2, v__14 <= v__2, v__15 <= v__2, v__16 <= v__2, v__17 <= v__2, v__18 <= v__2, v__19 <= v__2, v__20 <= v__2, v__21 <= v__2, 1 <= 2*v__2, 2 <= 2*v__1 + v__2, 2 <= v__1 + 2*v__2, v__1 <= v__3, v__2 <= v__3, v__4 <= v__3, v__5 <= v__3, v__6 <= v__3, v__7 <= v__3, v__8 <= v__3, v__9 <= v__3, v__10 <= v__3, v__11 <= v__3, v__12 <= v__3, v__13 <= v__3, v__14 <= v__3, v__15 <= v__3, v__16 <= v__3, v__17 <= v__3, v__18 <= v__3, v__19 <= v__3, v__20 <= v__3, v__21 <= v__3, 1 <= 2*v__3, 2 <= 2*v__1 + v__3, 2 <= 2*v__2 + v__3, 2 <= v__1 + 2*v__3, 2 <= v__2 + 2*v__3, v__1 <= v__4, v__2 <= v__4, v__3 <= v__4, v__5 <= v__4, v__6 <= v__4, v__7 <= v__4, v__8 <= v__4, v__9 <= v__4, v__10 <= v__4, v__11 <= v__4, v__12 <= v__4, v__13 <= v__4, v__14 <= v__4, v__15 <= v__4, v__16 <= v__4, v__17 <= v__4, v__18 <= v__4, v__19 <= v__4, v__20 <= v__4, v__21 <= v__4, 1 <= 2*v__4, 2 <= 2*v__1 + v__4, 2 <= 2*v__2 + v__4, 2 <= 2*v__3 + v__4, 2 <= v__1 + 2*v__4, 2 <= v__2 + 2*v__4, 2 <= v__3 + 2*v__4, v__1 <= v__5, v__2 <= v__5, v__3 <= v__5, v__4 <= v__5, v__6 <= v__5, v__7 <= v__5, v__8 <= v__5, v__9 <= v__5, v__10 <= v__5, v__11 <= v__5, v__12 <= v__5, v__13 <= v__5, v__14 <= v__5, v__15 <= v__5, v__16 <= v__5, v__17 <= v__5, v__18 <= v__5, v__19 <= v__5, v__20 <= v__5, v__21 <= v__5, 1 <= 2*v__5, 2 <= 2*v__1 + v__5, 2 <= 2*v__2 + v__5, 2 <= 2*v__3 + v__5, 2 <= 2*v__4 + v__5, 2 <= v__1 + 2*v__5, 2 <= v__2 + 2*v__5, 2 <= v__3 + 2*v__5, 2 <= v__4 + 2*v__5, v__1 <= v__6, v__2 <= v__6, v__3 <= v__6, v__4 <= v__6, v__5 <= v__6, v__7 <= v__6, v__8 <= v__6, v__9 <= v__6, v__10 <= v__6, v__11 <= v__6, v__12 <= v__6, v__13 <= v__6, v__14 <= v__6, v__15 <= v__6, v__16 <= v__6, v__17 <= v__6, v__18 <= v__6, v__19 <= v__6, v__20 <= v__6, v__21 <= v__6, 1 <= 2*v__6, 2 <= 2*v__1 + v__6, 2 <= 2*v__2 + v__6, 2 <= 2*v__3 + v__6, 2 <= 2*v__4 + v__6, 2 <= 2*v__5 + v__6, 2 <= v__1 + 2*v__6, 2 <= v__2 + 2*v__6, 2 <= v__3 + 2*v__6, 2 <= v__4 + 2*v__6, 2 <= v__5 + 2*v__6, v__1 <= v__7, v__2 <= v__7, v__3 <= v__7, v__4 <= v__7, v__5 <= v__7, v__6 <= v__7, v__8 <= v__7, v__9 <= v__7, v__10 <= v__7, v__11 <= v__7, v__12 <= v__7, v__13 <= v__7, v__14 <= v__7, v__15 <= v__7, v__16 <= v__7, v__17 <= v__7, v__18 <= v__7, v__19 <= v__7, v__20 <= v__7, v__21 <= v__7, 1 <= 2*v__7, 2 <= 2*v__1 + v__7, 2 <= 2*v__2 + v__7, 2 <= 2*v__3 + v__7, 2 <= 2*v__4 + v__7, 2 <= 2*v__5 + v__7, 2 <= 2*v__6 + v__7, 2 <= v__1 + 2*v__7, 2 <= v__2 + 2*v__7, 2 <= v__3 + 2*v__7, 2 <= v__4 + 2*v__7, 2 <= v__5 + 2*v__7, 2 <= v__6 + 2*v__7, v__1 <= v__8, v__2 <= v__8, v__3 <= v__8, v__4 <= v__8, v__5 <= v__8, v__6 <= v__8, v__7 <= v__8, v__9 <= v__8, v__10 <= v__8, v__11 <= v__8, v__12 <= v__8, v__13 <= v__8, v__14 <= v__8, v__15 <= v__8, v__16 <= v__8, v__17 <= v__8, v__18 <= v__8, v__19 <= v__8, v__20 <= v__8, v__21 <= v__8, 1 <= 2*v__8, 2 <= 2*v__1 + v__8, 2 <= 2*v__2 + v__8, 2 <= 2*v__3 + v__8, 2 <= 2*v__4 + v__8, 2 <= 2*v__5 + v__8, 2 <= 2*v__6 + v__8, 2 <= 2*v__7 + v__8, 2 <= v__1 + 2*v__8, 2 <= v__2 + 2*v__8, 2 <= v__3 + 2*v__8, 2 <= v__4 + 2*v__8, 2 <= v__5 + 2*v__8, 2 <= v__6 + 2*v__8, 2 <= v__7 + 2*v__8, v__1 <= v__9, v__2 <= v__9, v__3 <= v__9, v__4 <= v__9, v__5 <= v__9, v__6 <= v__9, v__7 <= v__9, v__8 <= v__9, v__10 <= v__9, v__11 <= v__9, v__12 <= v__9, v__13 <= v__9, v__14 <= v__9, v__15 <= v__9, v__16 <= v__9, v__17 <= v__9, v__18 <= v__9, v__19 <= v__9, v__20 <= v__9, v__21 <= v__9, 1 <= 2*v__9, 2 <= 2*v__1 + v__9, 2 <= 2*v__2 + v__9, 2 <= 2*v__3 + v__9, 2 <= 2*v__4 + v__9, 2 <= 2*v__5 + v__9, 2 <= 2*v__6 + v__9, 2 <= 2*v__7 + v__9, 2 <= 2*v__8 + v__9, 2 <= v__1 + 2*v__9, 2 <= v__2 + 2*v__9, 2 <= v__3 + 2*v__9, 2 <= v__4 + 2*v__9, 2 <= v__5 + 2*v__9, 2 <= v__6 + 2*v__9, 2 <= v__7 + 2*v__9, 2 <= v__8 + 2*v__9, v__1 <= v__10, v__2 <= v__10, v__3 <= v__10, v__4 <= v__10, v__5 <= v__10, v__6 <= v__10, v__7 <= v__10, v__8 <= v__10, v__9 <= v__10, v__11 <= v__10, v__12 <= v__10, v__13 <= v__10, v__14 <= v__10, v__15 <= v__10, v__16 <= v__10, v__17 <= v__10, v__18 <= v__10, v__19 <= v__10, v__20 <= v__10, v__21 <= v__10, 1 <= 2*v__10, 2 <= 2*v__1 + v__10, 2 <= v__10 + 2*v__2, 2 <= v__10 + 2*v__3, 2 <= v__10 + 2*v__4, 2 <= v__10 + 2*v__5, 2 <= v__10 + 2*v__6, 2 <= v__10 + 2*v__7, 2 <= v__10 + 2*v__8, 2 <= v__10 + 2*v__9, 2 <= v__1 + 2*v__10, 2 <= 2*v__10 + v__2, 2 <= 2*v__10 + v__3, 2 <= 2*v__10 + v__4, 2 <= 2*v__10 + v__5, 2 <= 2*v__10 + v__6, 2 <= 2*v__10 + v__7, 2 <= 2*v__10 + v__8, 2 <= 2*v__10 + v__9, v__1 <= v__11, v__2 <= v__11, v__3 <= v__11, v__4 <= v__11, v__5 <= v__11, v__6 <= v__11, v__7 <= v__11, v__8 <= v__11, v__9 <= v__11, v__10 <= v__11, v__12 <= v__11, v__13 <= v__11, v__14 <= v__11, v__15 <= v__11, v__16 <= v__11, v__17 <= v__11, v__18 <= v__11, v__19 <= v__11, v__20 <= v__11, v__21 <= v__11, 1 <= 2*v__11, 2 <= 2*v__1 + v__11, 2 <= v__11 + 2*v__2, 2 <= v__11 + 2*v__3, 2 <= v__11 + 2*v__4, 2 <= v__11 + 2*v__5, 2 <= v__11 + 2*v__6, 2 <= v__11 + 2*v__7, 2 <= v__11 + 2*v__8, 2 <= v__11 + 2*v__9, 2 <= 2*v__10 + v__11, 2 <= v__1 + 2*v__11, 2 <= 2*v__11 + v__2, 2 <= 2*v__11 + v__3, 2 <= 2*v__11 + v__4, 2 <= 2*v__11 + v__5, 2 <= 2*v__11 + v__6, 2 <= 2*v__11 + v__7, 2 <= 2*v__11 + v__8, 2 <= 2*v__11 + v__9, 2 <= v__10 + 2*v__11, v__1 <= v__12, v__2 <= v__12, v__3 <= v__12, v__4 <= v__12, v__5 <= v__12, v__6 <= v__12, v__7 <= v__12, v__8 <= v__12, v__9 <= v__12, v__10 <= v__12, v__11 <= v__12, v__13 <= v__12, v__14 <= v__12, v__15 <= v__12, v__16 <= v__12, v__17 <= v__12, v__18 <= v__12, v__19 <= v__12, v__20 <= v__12, v__21 <= v__12, 1 <= 2*v__12, 2 <= 2*v__1 + v__12, 2 <= v__12 + 2*v__2, 2 <= v__12 + 2*v__3, 2 <= v__12 + 2*v__4, 2 <= v__12 + 2*v__5, 2 <= v__12 + 2*v__6, 2 <= v__12 + 2*v__7, 2 <= v__12 + 2*v__8, 2 <= v__12 + 2*v__9, 2 <= 2*v__10 + v__12, 2 <= 2*v__11 + v__12, 2 <= v__1 + 2*v__12, 2 <= 2*v__12 + v__2, 2 <= 2*v__12 + v__3, 2 <= 2*v__12 + v__4, 2 <= 2*v__12 + v__5, 2 <= 2*v__12 + v__6, 2 <= 2*v__12 + v__7, 2 <= 2*v__12 + v__8, 2 <= 2*v__12 + v__9, 2 <= v__10 + 2*v__12, 2 <= v__11 + 2*v__12, v__1 <= v__13, v__2 <= v__13, v__3 <= v__13, v__4 <= v__13, v__5 <= v__13, v__6 <= v__13, v__7 <= v__13, v__8 <= v__13, v__9 <= v__13, v__10 <= v__13, v__11 <= v__13, v__12 <= v__13, v__14 <= v__13, v__15 <= v__13, v__16 <= v__13, v__17 <= v__13, v__18 <= v__13, v__19 <= v__13, v__20 <= v__13, v__21 <= v__13, 1 <= 2*v__13, 2 <= 2*v__1 + v__13, 2 <= v__13 + 2*v__2, 2 <= v__13 + 2*v__3, 2 <= v__13 + 2*v__4, 2 <= v__13 + 2*v__5, 2 <= v__13 + 2*v__6, 2 <= v__13 + 2*v__7, 2 <= v__13 + 2*v__8, 2 <= v__13 + 2*v__9, 2 <= 2*v__10 + v__13, 2 <= 2*v__11 + v__13, 2 <= 2*v__12 + v__13, 2 <= v__1 + 2*v__13, 2 <= 2*v__13 + v__2, 2 <= 2*v__13 + v__3, 2 <= 2*v__13 + v__4, 2 <= 2*v__13 + v__5, 2 <= 2*v__13 + v__6, 2 <= 2*v__13 + v__7, 2 <= 2*v__13 + v__8, 2 <= 2*v__13 + v__9, 2 <= v__10 + 2*v__13, 2 <= v__11 + 2*v__13, 2 <= v__12 + 2*v__13, v__1 <= v__14, v__2 <= v__14, v__3 <= v__14, v__4 <= v__14, v__5 <= v__14, v__6 <= v__14, v__7 <= v__14, v__8 <= v__14, v__9 <= v__14, v__10 <= v__14, v__11 <= v__14, v__12 <= v__14, v__13 <= v__14, v__15 <= v__14, v__16 <= v__14, v__17 <= v__14, v__18 <= v__14, v__19 <= v__14, v__20 <= v__14, v__21 <= v__14, 1 <= 2*v__14, 2 <= 2*v__1 + v__14, 2 <= v__14 + 2*v__2, 2 <= v__14 + 2*v__3, 2 <= v__14 + 2*v__4, 2 <= v__14 + 2*v__5, 2 <= v__14 + 2*v__6, 2 <= v__14 + 2*v__7, 2 <= v__14 + 2*v__8, 2 <= v__14 + 2*v__9, 2 <= 2*v__10 + v__14, 2 <= 2*v__11 + v__14, 2 <= 2*v__12 + v__14, 2 <= 2*v__13 + v__14, 2 <= v__1 + 2*v__14, 2 <= 2*v__14 + v__2, 2 <= 2*v__14 + v__3, 2 <= 2*v__14 + v__4, 2 <= 2*v__14 + v__5, 2 <= 2*v__14 + v__6, 2 <= 2*v__14 + v__7, 2 <= 2*v__14 + v__8, 2 <= 2*v__14 + v__9, 2 <= v__10 + 2*v__14, 2 <= v__11 + 2*v__14, 2 <= v__12 + 2*v__14, 2 <= v__13 + 2*v__14, v__1 <= v__15, v__2 <= v__15, v__3 <= v__15, v__4 <= v__15, v__5 <= v__15, v__6 <= v__15, v__7 <= v__15, v__8 <= v__15, v__9 <= v__15, v__10 <= v__15, v__11 <= v__15, v__12 <= v__15, v__13 <= v__15, v__14 <= v__15, v__16 <= v__15, v__17 <= v__15, v__18 <= v__15, v__19 <= v__15, v__20 <= v__15, v__21 <= v__15, 1 <= 2*v__15, 2 <= 2*v__1 + v__15, 2 <= v__15 + 2*v__2, 2 <= v__15 + 2*v__3, 2 <= v__15 + 2*v__4, 2 <= v__15 + 2*v__5, 2 <= v__15 + 2*v__6, 2 <= v__15 + 2*v__7, 2 <= v__15 + 2*v__8, 2 <= v__15 + 2*v__9, 2 <= 2*v__10 + v__15, 2 <= 2*v__11 + v__15, 2 <= 2*v__12 + v__15, 2 <= 2*v__13 + v__15, 2 <= 2*v__14 + v__15, 2 <= v__1 + 2*v__15, 2 <= 2*v__15 + v__2, 2 <= 2*v__15 + v__3, 2 <= 2*v__15 + v__4, 2 <= 2*v__15 + v__5, 2 <= 2*v__15 + v__6, 2 <= 2*v__15 + v__7, 2 <= 2*v__15 + v__8, 2 <= 2*v__15 + v__9, 2 <= v__10 + 2*v__15, 2 <= v__11 + 2*v__15, 2 <= v__12 + 2*v__15, 2 <= v__13 + 2*v__15, 2 <= v__14 + 2*v__15, v__1 <= v__16, v__2 <= v__16, v__3 <= v__16, v__4 <= v__16, v__5 <= v__16, v__6 <= v__16, v__7 <= v__16, v__8 <= v__16, v__9 <= v__16, v__10 <= v__16, v__11 <= v__16, v__12 <= v__16, v__13 <= v__16, v__14 <= v__16, v__15 <= v__16, v__17 <= v__16, v__18 <= v__16, v__19 <= v__16, v__20 <= v__16, v__21 <= v__16, 1 <= 2*v__16, 2 <= 2*v__1 + v__16, 2 <= v__16 + 2*v__2, 2 <= v__16 + 2*v__3, 2 <= v__16 + 2*v__4, 2 <= v__16 + 2*v__5, 2 <= v__16 + 2*v__6, 2 <= v__16 + 2*v__7, 2 <= v__16 + 2*v__8, 2 <= v__16 + 2*v__9, 2 <= 2*v__10 + v__16, 2 <= 2*v__11 + v__16, 2 <= 2*v__12 + v__16, 2 <= 2*v__13 + v__16, 2 <= 2*v__14 + v__16, 2 <= 2*v__15 + v__16, 2 <= v__1 + 2*v__16, 2 <= 2*v__16 + v__2, 2 <= 2*v__16 + v__3, 2 <= 2*v__16 + v__4, 2 <= 2*v__16 + v__5, 2 <= 2*v__16 + v__6, 2 <= 2*v__16 + v__7, 2 <= 2*v__16 + v__8, 2 <= 2*v__16 + v__9, 2 <= v__10 + 2*v__16, 2 <= v__11 + 2*v__16, 2 <= v__12 + 2*v__16, 2 <= v__13 + 2*v__16, 2 <= v__14 + 2*v__16, 2 <= v__15 + 2*v__16, v__1 <= v__17, v__2 <= v__17, v__3 <= v__17, v__4 <= v__17, v__5 <= v__17, v__6 <= v__17, v__7 <= v__17, v__8 <= v__17, v__9 <= v__17, v__10 <= v__17, v__11 <= v__17, v__12 <= v__17, v__13 <= v__17, v__14 <= v__17, v__15 <= v__17, v__16 <= v__17, v__18 <= v__17, v__19 <= v__17, v__20 <= v__17, v__21 <= v__17, 1 <= 2*v__17, 2 <= 2*v__1 + v__17, 2 <= v__17 + 2*v__2, 2 <= v__17 + 2*v__3, 2 <= v__17 + 2*v__4, 2 <= v__17 + 2*v__5, 2 <= v__17 + 2*v__6, 2 <= v__17 + 2*v__7, 2 <= v__17 + 2*v__8, 2 <= v__17 + 2*v__9, 2 <= 2*v__10 + v__17, 2 <= 2*v__11 + v__17, 2 <= 2*v__12 + v__17, 2 <= 2*v__13 + v__17, 2 <= 2*v__14 + v__17, 2 <= 2*v__15 + v__17, 2 <= 2*v__16 + v__17, 2 <= v__1 + 2*v__17, 2 <= 2*v__17 + v__2, 2 <= 2*v__17 + v__3, 2 <= 2*v__17 + v__4, 2 <= 2*v__17 + v__5, 2 <= 2*v__17 + v__6, 2 <= 2*v__17 + v__7, 2 <= 2*v__17 + v__8, 2 <= 2*v__17 + v__9, 2 <= v__10 + 2*v__17, 2 <= v__11 + 2*v__17, 2 <= v__12 + 2*v__17, 2 <= v__13 + 2*v__17, 2 <= v__14 + 2*v__17, 2 <= v__15 + 2*v__17, 2 <= v__16 + 2*v__17, v__1 <= v__18, v__2 <= v__18, v__3 <= v__18, v__4 <= v__18, v__5 <= v__18, v__6 <= v__18, v__7 <= v__18, v__8 <= v__18, v__9 <= v__18, v__10 <= v__18, v__11 <= v__18, v__12 <= v__18, v__13 <= v__18, v__14 <= v__18, v__15 <= v__18, v__16 <= v__18, v__17 <= v__18, v__19 <= v__18, v__20 <= v__18, v__21 <= v__18, 1 <= 2*v__18, 2 <= 2*v__1 + v__18, 2 <= v__18 + 2*v__2, 2 <= v__18 + 2*v__3, 2 <= v__18 + 2*v__4, 2 <= v__18 + 2*v__5, 2 <= v__18 + 2*v__6, 2 <= v__18 + 2*v__7, 2 <= v__18 + 2*v__8, 2 <= v__18 + 2*v__9, 2 <= 2*v__10 + v__18, 2 <= 2*v__11 + v__18, 2 <= 2*v__12 + v__18, 2 <= 2*v__13 + v__18, 2 <= 2*v__14 + v__18, 2 <= 2*v__15 + v__18, 2 <= 2*v__16 + v__18, 2 <= 2*v__17 + v__18, 2 <= v__1 + 2*v__18, 2 <= 2*v__18 + v__2, 2 <= 2*v__18 + v__3, 2 <= 2*v__18 + v__4, 2 <= 2*v__18 + v__5, 2 <= 2*v__18 + v__6, 2 <= 2*v__18 + v__7, 2 <= 2*v__18 + v__8, 2 <= 2*v__18 + v__9, 2 <= v__10 + 2*v__18, 2 <= v__11 + 2*v__18, 2 <= v__12 + 2*v__18, 2 <= v__13 + 2*v__18, 2 <= v__14 + 2*v__18, 2 <= v__15 + 2*v__18, 2 <= v__16 + 2*v__18, 2 <= v__17 + 2*v__18, v__1 <= v__19, v__2 <= v__19, v__3 <= v__19, v__4 <= v__19, v__5 <= v__19, v__6 <= v__19, v__7 <= v__19, v__8 <= v__19, v__9 <= v__19, v__10 <= v__19, v__11 <= v__19, v__12 <= v__19, v__13 <= v__19, v__14 <= v__19, v__15 <= v__19, v__16 <= v__19, v__17 <= v__19, v__18 <= v__19, v__20 <= v__19, v__21 <= v__19, 1 <= 2*v__19, 2 <= 2*v__1 + v__19, 2 <= v__19 + 2*v__2, 2 <= v__19 + 2*v__3, 2 <= v__19 + 2*v__4, 2 <= v__19 + 2*v__5, 2 <= v__19 + 2*v__6, 2 <= v__19 + 2*v__7, 2 <= v__19 + 2*v__8, 2 <= v__19 + 2*v__9, 2 <= 2*v__10 + v__19, 2 <= 2*v__11 + v__19, 2 <= 2*v__12 + v__19, 2 <= 2*v__13 + v__19, 2 <= 2*v__14 + v__19, 2 <= 2*v__15 + v__19, 2 <= 2*v__16 + v__19, 2 <= 2*v__17 + v__19, 2 <= 2*v__18 + v__19, 2 <= v__1 + 2*v__19, 2 <= 2*v__19 + v__2, 2 <= 2*v__19 + v__3, 2 <= 2*v__19 + v__4, 2 <= 2*v__19 + v__5, 2 <= 2*v__19 + v__6, 2 <= 2*v__19 + v__7, 2 <= 2*v__19 + v__8, 2 <= 2*v__19 + v__9, 2 <= v__10 + 2*v__19, 2 <= v__11 + 2*v__19, 2 <= v__12 + 2*v__19, 2 <= v__13 + 2*v__19, 2 <= v__14 + 2*v__19, 2 <= v__15 + 2*v__19, 2 <= v__16 + 2*v__19, 2 <= v__17 + 2*v__19, 2 <= v__18 + 2*v__19, v__1 <= v__20, v__2 <= v__20, v__3 <= v__20, v__4 <= v__20, v__5 <= v__20, v__6 <= v__20, v__7 <= v__20, v__8 <= v__20, v__9 <= v__20, v__10 <= v__20, v__11 <= v__20, v__12 <= v__20, v__13 <= v__20, v__14 <= v__20, v__15 <= v__20, v__16 <= v__20, v__17 <= v__20, v__18 <= v__20, v__19 <= v__20, v__21 <= v__20, 1 <= 2*v__20, 2 <= 2*v__1 + v__20, 2 <= 2*v__2 + v__20, 2 <= v__20 + 2*v__3, 2 <= v__20 + 2*v__4, 2 <= v__20 + 2*v__5, 2 <= v__20 + 2*v__6, 2 <= v__20 + 2*v__7, 2 <= v__20 + 2*v__8, 2 <= v__20 + 2*v__9, 2 <= 2*v__10 + v__20, 2 <= 2*v__11 + v__20, 2 <= 2*v__12 + v__20, 2 <= 2*v__13 + v__20, 2 <= 2*v__14 + v__20, 2 <= 2*v__15 + v__20, 2 <= 2*v__16 + v__20, 2 <= 2*v__17 + v__20, 2 <= 2*v__18 + v__20, 2 <= 2*v__19 + v__20, 2 <= v__1 + 2*v__20, 2 <= v__2 + 2*v__20, 2 <= 2*v__20 + v__3, 2 <= 2*v__20 + v__4, 2 <= 2*v__20 + v__5, 2 <= 2*v__20 + v__6, 2 <= 2*v__20 + v__7, 2 <= 2*v__20 + v__8, 2 <= 2*v__20 + v__9, 2 <= v__10 + 2*v__20, 2 <= v__11 + 2*v__20, 2 <= v__12 + 2*v__20, 2 <= v__13 + 2*v__20, 2 <= v__14 + 2*v__20, 2 <= v__15 + 2*v__20, 2 <= v__16 + 2*v__20, 2 <= v__17 + 2*v__20, 2 <= v__18 + 2*v__20, 2 <= v__19 + 2*v__20, v__1 <= v__21, v__2 <= v__21, v__3 <= v__21, v__4 <= v__21, v__5 <= v__21, v__6 <= v__21, v__7 <= v__21, v__8 <= v__21, v__9 <= v__21, v__10 <= v__21, v__11 <= v__21, v__12 <= v__21, v__13 <= v__21, v__14 <= v__21, v__15 <= v__21, v__16 <= v__21, v__17 <= v__21, v__18 <= v__21, v__19 <= v__21, v__20 <= v__21, 1 <= 2*v__21, 2 <= 2*v__1 + v__21, 2 <= 2*v__2 + v__21, 2 <= v__21 + 2*v__3, 2 <= v__21 + 2*v__4, 2 <= v__21 + 2*v__5, 2 <= v__21 + 2*v__6, 2 <= v__21 + 2*v__7, 2 <= v__21 + 2*v__8, 2 <= v__21 + 2*v__9, 2 <= 2*v__10 + v__21, 2 <= 2*v__11 + v__21, 2 <= 2*v__12 + v__21, 2 <= 2*v__13 + v__21, 2 <= 2*v__14 + v__21, 2 <= 2*v__15 + v__21, 2 <= 2*v__16 + v__21, 2 <= 2*v__17 + v__21, 2 <= 2*v__18 + v__21, 2 <= 2*v__19 + v__21, 2 <= 2*v__20 + v__21, 2 <= v__1 + 2*v__21, 2 <= v__2 + 2*v__21, 2 <= 2*v__21 + v__3, 2 <= 2*v__21 + v__4, 2 <= 2*v__21 + v__5, 2 <= 2*v__21 + v__6, 2 <= 2*v__21 + v__7, 2 <= 2*v__21 + v__8, 2 <= 2*v__21 + v__9, 2 <= v__10 + 2*v__21, 2 <= v__11 + 2*v__21, 2 <= v__12 + 2*v__21, 2 <= v__13 + 2*v__21, 2 <= v__14 + 2*v__21, 2 <= v__15 + 2*v__21, 2 <= v__16 + 2*v__21, 2 <= v__17 + 2*v__21, 2 <= v__18 + 2*v__21, 2 <= v__19 + 2*v__21, 2 <= v__20 + 2*v__21, v__1 <= 2*v__2, v__1 <= 2*v__3, v__1 <= 2*v__4, v__1 <= 2*v__5, v__1 <= 2*v__6, v__1 <= 2*v__7, v__1 <= 2*v__8, v__1 <= 2*v__9, v__1 <= 2*v__10, v__1 <= 2*v__11, v__1 <= 2*v__12, v__1 <= 2*v__13, v__1 <= 2*v__14, v__1 <= 2*v__15, v__1 <= 2*v__16, v__1 <= 2*v__17, v__1 <= 2*v__18, v__1 <= 2*v__19, v__1 <= 2*v__20, v__1 <= 2*v__21, v__2 <= 2*v__1, v__2 <= 2*v__3, v__2 <= 2*v__4, v__2 <= 2*v__5, v__2 <= 2*v__6, v__2 <= 2*v__7, v__2 <= 2*v__8, v__2 <= 2*v__9, v__2 <= 2*v__10, v__2 <= 2*v__11, v__2 <= 2*v__12, v__2 <= 2*v__13, v__2 <= 2*v__14, v__2 <= 2*v__15, v__2 <= 2*v__16, v__2 <= 2*v__17, v__2 <= 2*v__18, v__2 <= 2*v__19, v__2 <= 2*v__20, v__2 <= 2*v__21, v__3 <= 2*v__1, v__3 <= 2*v__2, v__3 <= 2*v__4, v__3 <= 2*v__5, v__3 <= 2*v__6, v__3 <= 2*v__7, v__3 <= 2*v__8, v__3 <= 2*v__9, v__3 <= 2*v__10, v__3 <= 2*v__11, v__3 <= 2*v__12, v__3 <= 2*v__13, v__3 <= 2*v__14, v__3 <= 2*v__15, v__3 <= 2*v__16, v__3 <= 2*v__17, v__3 <= 2*v__18, v__3 <= 2*v__19, v__3 <= 2*v__20, v__3 <= 2*v__21, v__4 <= 2*v__1, v__4 <= 2*v__2, v__4 <= 2*v__3, v__4 <= 2*v__5, v__4 <= 2*v__6, v__4 <= 2*v__7, v__4 <= 2*v__8, v__4 <= 2*v__9, v__4 <= 2*v__10, v__4 <= 2*v__11, v__4 <= 2*v__12, v__4 <= 2*v__13, v__4 <= 2*v__14, v__4 <= 2*v__15, v__4 <= 2*v__16, v__4 <= 2*v__17, v__4 <= 2*v__18, v__4 <= 2*v__19, v__4 <= 2*v__20, v__4 <= 2*v__21, v__5 <= 2*v__1, v__5 <= 2*v__2, v__5 <= 2*v__3, v__5 <= 2*v__4, v__5 <= 2*v__6, v__5 <= 2*v__7, v__5 <= 2*v__8, v__5 <= 2*v__9, v__5 <= 2*v__10, v__5 <= 2*v__11, v__5 <= 2*v__12, v__5 <= 2*v__13, v__5 <= 2*v__14, v__5 <= 2*v__15, v__5 <= 2*v__16, v__5 <= 2*v__17, v__5 <= 2*v__18, v__5 <= 2*v__19, v__5 <= 2*v__20, v__5 <= 2*v__21, v__6 <= 2*v__1, v__6 <= 2*v__2, v__6 <= 2*v__3, v__6 <= 2*v__4, v__6 <= 2*v__5, v__6 <= 2*v__7, v__6 <= 2*v__8, v__6 <= 2*v__9, v__6 <= 2*v__10, v__6 <= 2*v__11, v__6 <= 2*v__12, v__6 <= 2*v__13, v__6 <= 2*v__14, v__6 <= 2*v__15, v__6 <= 2*v__16, v__6 <= 2*v__17, v__6 <= 2*v__18, v__6 <= 2*v__19, v__6 <= 2*v__20, v__6 <= 2*v__21, v__7 <= 2*v__1, v__7 <= 2*v__2, v__7 <= 2*v__3, v__7 <= 2*v__4, v__7 <= 2*v__5, v__7 <= 2*v__6, v__7 <= 2*v__8, v__7 <= 2*v__9, v__7 <= 2*v__10, v__7 <= 2*v__11, v__7 <= 2*v__12, v__7 <= 2*v__13, v__7 <= 2*v__14, v__7 <= 2*v__15, v__7 <= 2*v__16, v__7 <= 2*v__17, v__7 <= 2*v__18, v__7 <= 2*v__19, v__7 <= 2*v__20, v__7 <= 2*v__21, v__8 <= 2*v__1, v__8 <= 2*v__2, v__8 <= 2*v__3, v__8 <= 2*v__4, v__8 <= 2*v__5, v__8 <= 2*v__6, v__8 <= 2*v__7, v__8 <= 2*v__9, v__8 <= 2*v__10, v__8 <= 2*v__11, v__8 <= 2*v__12, v__8 <= 2*v__13, v__8 <= 2*v__14, v__8 <= 2*v__15, v__8 <= 2*v__16, v__8 <= 2*v__17, v__8 <= 2*v__18, v__8 <= 2*v__19, v__8 <= 2*v__20, v__8 <= 2*v__21, v__9 <= 2*v__1, v__9 <= 2*v__2, v__9 <= 2*v__3, v__9 <= 2*v__4, v__9 <= 2*v__5, v__9 <= 2*v__6, v__9 <= 2*v__7, v__9 <= 2*v__8, v__9 <= 2*v__10, v__9 <= 2*v__11, v__9 <= 2*v__12, v__9 <= 2*v__13, v__9 <= 2*v__14, v__9 <= 2*v__15, v__9 <= 2*v__16, v__9 <= 2*v__17, v__9 <= 2*v__18, v__9 <= 2*v__19, v__9 <= 2*v__20, v__9 <= 2*v__21, v__10 <= 2*v__1, v__10 <= 2*v__2, v__10 <= 2*v__3, v__10 <= 2*v__4, v__10 <= 2*v__5, v__10 <= 2*v__6, v__10 <= 2*v__7, v__10 <= 2*v__8, v__10 <= 2*v__9, v__10 <= 2*v__11, v__10 <= 2*v__12, v__10 <= 2*v__13, v__10 <= 2*v__14, v__10 <= 2*v__15, v__10 <= 2*v__16, v__10 <= 2*v__17, v__10 <= 2*v__18, v__10 <= 2*v__19, v__10 <= 2*v__20, v__10 <= 2*v__21, v__11 <= 2*v__1, v__11 <= 2*v__2, v__11 <= 2*v__3, v__11 <= 2*v__4, v__11 <= 2*v__5, v__11 <= 2*v__6, v__11 <= 2*v__7, v__11 <= 2*v__8, v__11 <= 2*v__9, v__11 <= 2*v__10, v__11 <= 2*v__12, v__11 <= 2*v__13, v__11 <= 2*v__14, v__11 <= 2*v__15, v__11 <= 2*v__16, v__11 <= 2*v__17, v__11 <= 2*v__18, v__11 <= 2*v__19, v__11 <= 2*v__20, v__11 <= 2*v__21, v__12 <= 2*v__1, v__12 <= 2*v__2, v__12 <= 2*v__3, v__12 <= 2*v__4, v__12 <= 2*v__5, v__12 <= 2*v__6, v__12 <= 2*v__7, v__12 <= 2*v__8, v__12 <= 2*v__9, v__12 <= 2*v__10, v__12 <= 2*v__11, v__12 <= 2*v__13, v__12 <= 2*v__14, v__12 <= 2*v__15, v__12 <= 2*v__16, v__12 <= 2*v__17, v__12 <= 2*v__18, v__12 <= 2*v__19, v__12 <= 2*v__20, v__12 <= 2*v__21, v__13 <= 2*v__1, v__13 <= 2*v__2, v__13 <= 2*v__3, v__13 <= 2*v__4, v__13 <= 2*v__5, v__13 <= 2*v__6, v__13 <= 2*v__7, v__13 <= 2*v__8, v__13 <= 2*v__9, v__13 <= 2*v__10, v__13 <= 2*v__11, v__13 <= 2*v__12, v__13 <= 2*v__14, v__13 <= 2*v__15, v__13 <= 2*v__16, v__13 <= 2*v__17, v__13 <= 2*v__18, v__13 <= 2*v__19, v__13 <= 2*v__20, v__13 <= 2*v__21, v__14 <= 2*v__1, v__14 <= 2*v__2, v__14 <= 2*v__3, v__14 <= 2*v__4, v__14 <= 2*v__5, v__14 <= 2*v__6, v__14 <= 2*v__7, v__14 <= 2*v__8, v__14 <= 2*v__9, v__14 <= 2*v__10, v__14 <= 2*v__11, v__14 <= 2*v__12, v__14 <= 2*v__13, v__14 <= 2*v__15, v__14 <= 2*v__16, v__14 <= 2*v__17, v__14 <= 2*v__18, v__14 <= 2*v__19, v__14 <= 2*v__20, v__14 <= 2*v__21, v__15 <= 2*v__1, v__15 <= 2*v__2, v__15 <= 2*v__3, v__15 <= 2*v__4, v__15 <= 2*v__5, v__15 <= 2*v__6, v__15 <= 2*v__7, v__15 <= 2*v__8, v__15 <= 2*v__9, v__15 <= 2*v__10, v__15 <= 2*v__11, v__15 <= 2*v__12, v__15 <= 2*v__13, v__15 <= 2*v__14, v__15 <= 2*v__16, v__15 <= 2*v__17, v__15 <= 2*v__18, v__15 <= 2*v__19, v__15 <= 2*v__20, v__15 <= 2*v__21, v__16 <= 2*v__1, v__16 <= 2*v__2, v__16 <= 2*v__3, v__16 <= 2*v__4, v__16 <= 2*v__5, v__16 <= 2*v__6, v__16 <= 2*v__7, v__16 <= 2*v__8, v__16 <= 2*v__9, v__16 <= 2*v__10, v__16 <= 2*v__11, v__16 <= 2*v__12, v__16 <= 2*v__13, v__16 <= 2*v__14, v__16 <= 2*v__15, v__16 <= 2*v__17, v__16 <= 2*v__18, v__16 <= 2*v__19, v__16 <= 2*v__20, v__16 <= 2*v__21, v__17 <= 2*v__1, v__17 <= 2*v__2, v__17 <= 2*v__3, v__17 <= 2*v__4, v__17 <= 2*v__5, v__17 <= 2*v__6, v__17 <= 2*v__7, v__17 <= 2*v__8, v__17 <= 2*v__9, v__17 <= 2*v__10, v__17 <= 2*v__11, v__17 <= 2*v__12, v__17 <= 2*v__13, v__17 <= 2*v__14, v__17 <= 2*v__15, v__17 <= 2*v__16, v__17 <= 2*v__18, v__17 <= 2*v__19, v__17 <= 2*v__20, v__17 <= 2*v__21, v__18 <= 2*v__1, v__18 <= 2*v__2, v__18 <= 2*v__3, v__18 <= 2*v__4, v__18 <= 2*v__5, v__18 <= 2*v__6, v__18 <= 2*v__7, v__18 <= 2*v__8, v__18 <= 2*v__9, v__18 <= 2*v__10, v__18 <= 2*v__11, v__18 <= 2*v__12, v__18 <= 2*v__13, v__18 <= 2*v__14, v__18 <= 2*v__15, v__18 <= 2*v__16, v__18 <= 2*v__17, v__18 <= 2*v__19, v__18 <= 2*v__20, v__18 <= 2*v__21, v__19 <= 2*v__1, v__19 <= 2*v__2, v__19 <= 2*v__3, v__19 <= 2*v__4, v__19 <= 2*v__5, v__19 <= 2*v__6, v__19 <= 2*v__7, v__19 <= 2*v__8, v__19 <= 2*v__9, v__19 <= 2*v__10, v__19 <= 2*v__11, v__19 <= 2*v__12, v__19 <= 2*v__13, v__19 <= 2*v__14, v__19 <= 2*v__15, v__19 <= 2*v__16, v__19 <= 2*v__17, v__19 <= 2*v__18, v__19 <= 2*v__20, v__19 <= 2*v__21, v__20 <= 2*v__1, v__20 <= 2*v__2, v__20 <= 2*v__3, v__20 <= 2*v__4, v__20 <= 2*v__5, v__20 <= 2*v__6, v__20 <= 2*v__7, v__20 <= 2*v__8, v__20 <= 2*v__9, v__20 <= 2*v__10, v__20 <= 2*v__11, v__20 <= 2*v__12, v__20 <= 2*v__13, v__20 <= 2*v__14, v__20 <= 2*v__15, v__20 <= 2*v__16, v__20 <= 2*v__17, v__20 <= 2*v__18, v__20 <= 2*v__19, v__20 <= 2*v__21, v__21 <= 2*v__1, v__21 <= 2*v__2, v__21 <= 2*v__3, v__21 <= 2*v__4, v__21 <= 2*v__5, v__21 <= 2*v__6, v__21 <= 2*v__7, v__21 <= 2*v__8, v__21 <= 2*v__9, v__21 <= 2*v__10, v__21 <= 2*v__11, v__21 <= 2*v__12, v__21 <= 2*v__13, v__21 <= 2*v__14, v__21 <= 2*v__15, v__21 <= 2*v__16, v__21 <= 2*v__17, v__21 <= 2*v__18, v__21 <= 2*v__19, v__21 <= 2*v__20 ), `0059` = ( v__41 > v__1 ), `Industry Equilibrium: Prices and factor costs 0061` = ( v__10*v__5 + v__1*v__6 = v__9 ), `Industry Equilibrium: Long-run relationship between real output and real wages\ 0062` = ( v__13*v__15*v__6 = v__14 ), `Industry Equilibrium: Adding up for factor shares 0063` = ( v__6 = 1 - v__5 ), `Industry Equilibrium: Input and output quantities 0064` = ( v__13 = v__5*(v__8 - v__9) + v__9 ), `Industry Equilibrium: Marshall's Law 0065` = ( v__13*(-v__16*v__5 + v__15*v__6) = v__10 ), `Industry Equilibrium: Determinants of long-run capital-labor complementarity\ 0066` = ( v__11*(v__13 + v__14)*v__6 = v__9 ), `Industry Equilibrium: Determinants of short-run capital-labor complementarity\ 0067` = ( v__12*(-v__15*v__5 + v__16*v__6) = v__13*(v__15 + v__16)*v__6 ), `Supply-Demand: Global demand analysis 0074` = ( v__7 > v__8 ), `Vector mode: Variance of a sum 0076` = ( (-v__9 + x + y)^2 >= (-v__7 + x)^2 ), `Vector mode: Variance of a sum 0077` = ':-Or'( (v__1*v__7^2 - v__1*v__9^2 - 2*v__2*v__7 + 2*v__2*v__9 + 2*v__3*v__9 - 2*v__5 - v__6)*v__1 < 0, ':-And'( v__1*v__7^2 - v__1*v__9^2 - 2*v__2*v__7 + 2*v__2*v__9 + 2*v__3*v__9 - 2*v__5 - v__6 = 0, v__1 <> 0 ) ), `Vector mode: Hicks' generalized law of demand 0078` = ( v__2 + v__9 <= v__3 + v__7 ), `Vector mode: Progressive policy and inequality 0079` = ( 2*v__1*v__3 + v__6 >= 2*v__5 ), `Vector mode: Consumer Theory Adding Up 0080` = ( v__9 = 0 ), `Vector mode: Constant absolute risk aversion 0082` = ( v__10 = 0 ), `Vector mode: Constant absolute risk aversion 0083` = ( v__10 = 0 ), `Vector mode: Constant relative risk aversion 0084` = ( v__12 = 0 ), `Vector mode: Correlation between wealth and marginal utility 0085` = ( v__1*v__2*v__3 + v__7 < v__2*v__4 + v__1*v__5 ), `Vector mode: Risk aversion reduces investment 0086` = ( v__19 < 0 ), `Constant absolute risk aversion with states delineated 1001` = ( v__2 = 0 ) ]): ############################################################################### BuildEconomicsQEExample := proc( n :: Or( name, posint ), mode :: identical( :-theorem, :-example, :-counterexample, :-assumptions ) := ':-theorem', $ ) :: TarskiFormula; local A :: TarskiFormula, H :: TarskiFormula, vars,# :: seq(name) varsExpr :: set, expr :: TarskiFormula, ex :: name, i :: name, x :: name, quant :: identical( :-exists, :-forall ); if type( n, 'name' ) then ex := n; else for i in indices( :-EconomicsAssumptions, ':-nolist' ) do if parse( substring( i, -4..-1 ) ) = n then ex := i; break; end if; end do; if not assigned( ex ) then error "Example not found"; end if; end if; if mode = ':-theorem' then ( A, H ) := :-EconomicsAssumptions[ ex ], :-EconomicsHypotheses[ ex ]; ( quant, expr ) := ':-forall' , ':-Implies'( A, H ); elif mode = ':-example' then ( A, H ) := :-EconomicsAssumptions[ ex ], :-EconomicsHypotheses[ ex ]; ( quant, expr ) := ':-exists', ':-And'( `if`( op( 0, A ) = ':-And', op( A ), A ) , `if`( op( 0, H ) = ':-And', op( H ), H ) ); elif mode = ':-counterexample' then ( A, H ) := :-EconomicsAssumptions[ ex ] , :-EconomicsHypotheses[ ex ]; ( quant, expr ) := ':-exists', ':-And'( `if`( op( 0, A ) = ':-And', op( A ), A ), ':-Not'( H ) ); else # mode = assumptions ( quant, expr ) := ':-exists', :-EconomicsAssumptions[ ex ]; end if; ( varsExpr, vars ) := indets( expr, 'name' ), 'NULL'; for x in varsExpr do if substring( x, 1 ) = ':-v' then vars := vars, x; end if; end do; return quant( [ eval( vars ) ], expr ); end proc: