% 2018 submission by Mulligan, Bradford, Davenport, England, and Tonks
% Each example is a tarskiformula describing A(v) => H(v)
% not(tarskiformula) is therefore equivalent to A(v) and not(H(v))
% not(tarskiformula) is satisfiable if and only if a counterexample exists to A(v) => H(v)
% optvlist is an existential quantifier sequence that allows rlqe to finish in reasonable time
%   As of April 20, 2018, we have not found a sequence that allows rlqe to finish model #0078 in reasonable time.

rlset R; % load Redlog and set the domain to real numbers

% Simple example from Marshall 1895
% shown in Section 2.1 for illustration but is not part of the 45-example library
write "Alfred Marshall on the consequences of reduced costs"$
optvlist:={v1, v2, v3, v4}$
tarskiformula:=(v3 > 0 and v4 < 0) or v1 >= 0 or v2 <= 0 or v4 <> v1*v3 or v4 <> -1 + v2*v3;

rlqe ex(optvlist,not (tarskiformula)); % False result here means that tarskiformula is True ForAll

% Mulligan model #0001
write "Supply-Demand: Determinants of quantity"$
optvlist:={v1, v2, v3, v4, v5, v6, v7, v8}$
tarskiformula:=v1 > 0 or v7 >= 0 or v4 <= 0 or v8 <= 0 or v5 <> 1 or v6 <> 1 or v1*v5 + v3*v7 <> v4 or v2*v6 + v3*v8 <> v4;

rlqe ex(optvlist,not (tarskiformula)); % False result here means that tarskiformula is True ForAll

% Mulligan model #0004
write "Supply-Demand: Determinants of quantity"$
optvlist:={v1, v2, v3, v4, v5, v6, v7, v8}$
tarskiformula:=v1 > 0 or v2 > 0 or v7 >= 0 or v4 <= 0 or v8 <= 0 or v5 <> 1 or v6 <> 1 or v1*v5 + v3*v7 <> v4 or v2*v6 + v3*v8 <> v4;

rlqe ex(optvlist,not (tarskiformula)); % False result here means that tarskiformula is True ForAll

% Mulligan model #0006
write "Supply-Demand: Price and quantity impact together reveal quantity determinants"$
optvlist:={v1, v2, v3, v4, v5, v6, v7, v8}$
tarskiformula:=v1 > 0 or v7 >= 0 or v3 <= 0 or v4 <= 0 or v8 <= 0 or v5 <> 1 or v6 <> 1 or v1*v5 + v3*v7 <> v4 or v2*v6 + v3*v8 <> v4;

rlqe ex(optvlist,not (tarskiformula)); % False result here means that tarskiformula is True ForAll

% Mulligan model #0009
write "Supply-Demand: Determinants of quantity"$
optvlist:={v1, v2, v3, v4, v5, v6, v7, v8}$
tarskiformula:=v4 >= 0 or v7 >= 0 or v1 < 0 or v2 < 0 or v8 <= 0 or v5 <> 1 or v6 <> 1 or v1*v5 + v3*v7 <> v4 or v2*v6 + v3*v8 <> v4;

rlqe ex(optvlist,not (tarskiformula)); % False result here means that tarskiformula is True ForAll

% Mulligan model #0012
write "Supply-Demand Scenarios"$
optvlist:={v1, v2, v3, v4, v5, v6, v7, v8, v9, v10, v11, v12}$
tarskiformula:=v5 >= 0 or v7 >= 0 or v11 >= 0 or v7 < v8 or v12 <= 0 or v2 <> 0 or v4 <> v3 or v9 <> 1 or v10 <> 1 or v11*v5 + v1*v9 <> v7 or v11*v6 + v2*v9 <> v8 or v10*v3 + v12*v5 <> v7 or v10*v4 + v12*v6 <> v8;

rlqe ex(optvlist,not (tarskiformula)); % False result here means that tarskiformula is True ForAll

% Mulligan model #0013
write "Supply-Demand: Krugman scenario error"$
optvlist:={v1, v2, v3, v4, v5, v6, v7, v8, v9, v10, v11, v12}$
tarskiformula:=(v7/2 < v8 and v8 < 0) or v5 >= 0 or v7 >= 0 or v11 >= 0 or v12 <= 0 or v2 <> 0 or v4 <> v3 or v9 <> 1 or v10 <> 1 or v11*v5 + v1*v9 <> v7 or v11*v6 + v2*v9 <> v8 or v10*v3 + v12*v5 <> v7 or v10*v4 + v12*v6 <> v8;

rlqe ex(optvlist,not (tarskiformula)); % False result here means that tarskiformula is True ForAll

% Mulligan model #0015
write "Supply-Demand: Incidence parameter for scenario analysis"$
optvlist:={v1, v2, v3, v4, v5, v6, v7, v8, v9, v10, v11, v12}$
tarskiformula:=(v11^2*v7 - v11*v12*v7 - v11^2*v8 + 2*v11*v12*v8 - v12^2*v8 = 0 and v11^2*v8 - 2*v11*v12*v8 + v12^2*v8 = v11^2*v7 - v11*v12*v7) or v7 >= 0 or v11 >= 0 or v12 <= 0 or v2 <> 0 or v4 <> v3 or v5 <> 0 or v9 <> 1 or v10 <> 1 or v11*v5 + v1*v9 <> v7 or v11*v6 + v2*v9 <> v8 or v10*v3 + v12*v5 <> v7 or v10*v4 + v12*v6 <> v8;

rlqe ex(optvlist,not (tarskiformula)); % False result here means that tarskiformula is True ForAll

% Mulligan model #0016
write "Supply-Demand: The missing Krugman condition"$
optvlist:={v1, v2, v3, v4, v5, v6, v7, v8, v9, v10, v11, v12}$
tarskiformula:=(v7/2 > 0 and v8 > v7/2 and v6 < v5/2) or v11 >= 0 or v12 >= -v11 or v1 <= 0 or v12 <= 0 or v2 <> 0 or v3 <> v1 or v4 <> v3 or v9 <> 1 or v10 <> 1 or v11*v5 + v1*v9 <> v7 or v11*v6 + v2*v9 <> v8 or v10*v3 + v12*v5 <> v7 or v10*v4 + v12*v6 <> v8;

rlqe ex(optvlist,not (tarskiformula)); % False result here means that tarskiformula is True ForAll

% Mulligan model #0018
write "Supply-Demand: Becker irrational demand"$
optvlist:={v1, v2, v3, v4, v5, v6, v7, v8}$
tarskiformula:=v7 < v8 or v3 <= 0 or v4 <= 0 or v5 <= v6 or v2 <> v1 or v3*v5 + v4*v7 <> v1 or v3*v6 + v4*v8 <> v2;

rlqe ex(optvlist,not (tarskiformula)); % False result here means that tarskiformula is True ForAll

% Mulligan model #0021
write "NGM (Neoclassical Growth Model): Labor taxes reduce steady-state labor, capital, consumption"$
optvlist:={v19, v4, v3, v1, v7, v2, v15, v18, v14, v8, v6, v9, v17, v13, v12, v10, v5, v20, v11, v16}$
tarskiformula:=(v8 < 0 and v9 < 0 and v10 < 0) or v6 >= 1 or v7 >= 1 or v11 >= 0 or v12 >= 0 or v15 >= 0 or v17 >= 0 or v12 + v14*v16 - v14*v16*v7 + v13*v17*(1 - v7) >= 0 or v20 >= 0 or v3 < 0 or v4 < 0 or v19 < 0 or v1 <= 0 or v2 <= 0 or v5 <= 0 or v13 <= 0 or v11*v14 <= v12*v13 or v11*v15 <= v13*v14 or v16 <= 0 or v18 <= 0 or v6 <> 0 or v7 <> 0 or v18 - v4 <> v3 or v18 - v4 - v5 - 2*v18*v6 + v4*v6 + v5*v6 + v18*v6^2 <> 0
 or v10*v16 - v8 + v18*v9 - v4*v9 <> 0 or v1*v19*v2 + v17*v2^2 <> 0 or 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 or v1*v19*v2 + v1^2*v20 <> 0 or v10*v19 + v20*v9 <> 0;

rlqe ex(optvlist,not (tarskiformula)); % False result here means that tarskiformula is True ForAll

% Mulligan model #0022
write "NGM: Capital taxes reduce steady-state capital"$
optvlist:={v17, v3, v18, v15, v16, v2, v6, v10, v20, v19, v5, v1, v12, v11, v14, v7, v13, v9, v8, v4}$
optvlist:={v8, v2, v16, v3, v1, v11, v14, v20, v12, v18, v9, v10, v4, v5, v15, v17, v19, v6, v13, v7}$
tarskiformula:=v6 >= 1 or v7 >= 1 or v11 >= 0 or v12 >= 0 or v15 >= 0 or v17 >= 0 or v12 + v14*v16*(1 - v7) + v13*v17*(1 - v7) >= 0 or v20 >= 0 or v3 < 0 or v4 < 0 or v9 < 0 or v19 < 0 or v1 <= 0 or v2 <= 0 or v5 <= 0 or v13 <= 0 or v11*v14 <= v12*v13 or v11*v15 <= v13*v14 or v16 <= 0 or v18 <= 0 or v18 - v4 <> v3 or v18 - v4 - v5 - 2*v18*v6 + v4*v6 + v5*v6 + v18*v6^2 <> 0 or v10*v16 - v8 + v18*v9 - v4*v9 <> 0 or v1*v19*v2 + v17*v2^2 <> 0
 or 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 or v1*v19*v2 + v1^2*v20 <> 0 or v10*v19 - 2*v10*v19*v6 + v10*v19*v6^2 + v20*v9 - 2*v20*v6*v9 + v20*v6^2*v9 <> v4 + v5;

rlqe ex(optvlist,not (tarskiformula)); % False result here means that tarskiformula is True ForAll

% Mulligan model #0023
write "NGM: Capital taxes reduce steady-state consumption"$
optvlist:={v14, v12, v8, v11, v7, v16, v6, v3, v20, v13, v18, v4, v19, v17, v1, v15, v2, v5, v10, v9}$
tarskiformula:=v6 >= 1 or v7 >= 1 or v11 >= 0 or v12 >= 0 or v15 >= 0 or v17 >= 0 or v12 + v14*v16*(1 - v7) + v13*v17*(1 - v7) >= 0 or v20 >= 0 or v3 < 0 or v4 < 0 or v8 < 0 or v19 < 0 or v1 <= 0 or v2 <= 0 or v5 <= 0 or v13 <= 0 or v11*v14 <= v12*v13 or v11*v15 <= v13*v14 or v16 <= 0 or v18 <= 0 or v18 - v4 <> v3 or v18 - v4 - v5 - 2*v18*v6 + v4*v6 + v5*v6 + v18*v6^2 <> 0 or v10*v16 - v8 + v18*v9 - v4*v9 <> 0
 or v1*v19*v2 + v17*v2^2 <> 0 or 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 or v1*v19*v2 + v1^2*v20 <> 0 or v10*v19 - 2*v10*v19*v6 + v10*v19*v6^2 + v20*v9 - 2*v20*v6*v9 + v20*v6^2*v9 <> v4 + v5;

rlqe ex(optvlist,not (tarskiformula)); % False result here means that tarskiformula is True ForAll

% Mulligan model #0024
write "NGM: Labor tax impact with separable production"$
optvlist:={v1, v2, v3, v4, v5, v6, v7, v8, v9, v10, v11, v12, v13, v14, v15, v16, v17}$
tarskiformula:=(v6 = 0 and v7 < 0) or v3 >= 1 or v4 >= 1 or v8 >= 0 or v9 >= 0 or v12 >= 0 or v14 >= 0 or v11*v13*(1 - v4) + v10*v14*(1 - v4) + v9 >= 0 or v17 >= 0 or v1 < 0 or v16 < 0 or v2 <= 0 or v10 <= 0 or v11*v8 <= v10*v9 or v12*v8 <= v10*v11 or v13 <= 0 or v15 <= 0 or -v1 + v15 - v2 + v1*v3 - 2*v15*v3 + v2*v3 + v15*v3^2 <> 0 or -v5 - v1*v6 + v15*v6 + v13*v7 <> 0 or v16 <> 0
 or -(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 or v17*v6 + v16*v7 <> 0;

rlqe ex(optvlist,not (tarskiformula)); % False result here means that tarskiformula is True ForAll

% Mulligan model #0025
write "NGM: Labor tax impact with separable production"$
optvlist:={v1, v2, v3, v4, v5, v6, v7, v8, v9, v10, v11, v12, v13, v14, v15, v16, v17}$
tarskiformula:=v3 >= 1 or v4 >= 1 or v8 >= 0 or v9 >= 0 or v12 >= 0 or v14 >= 0 or v11*v13*(1 - v4) + v10*v14*(1 - v4) + v9 >= 0 or v17 >= 0 or v1 < 0 or v5 < 0 or v16 < 0 or v2 <= 0 or v10 <= 0 or v11*v8 <= v10*v9 or v12*v8 <= v10*v11 or v13 <= 0 or v15 <= 0 or -v1 + v15 - v2 + v1*v3 - 2*v15*v3 + v2*v3 + v15*v3^2 <> 0 or -v5 - v1*v6 + v15*v6 + v13*v7 <> 0 or v16 <> 0
 or -(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 or v17*v6 + v16*v7 <> 0;

rlqe ex(optvlist,not (tarskiformula)); % False result here means that tarskiformula is True ForAll

% Mulligan model #0026
write "NGM: Slope of the stable manifold"$
optvlist:={v20, v19, v18, v17, v16, v15, v14, v13, v12, v11, v10, v9, v8, v7, v6, v5, v4, v3, v2, v1}$
tarskiformula:=v5 >= 1 or v6 >= 1 or v10 >= 0 or v11 >= 0 or v14 >= 0 or v17 >= 0 or v20 >= 0 or v3 < 0 or v7 < 0 or v19 < 0 or v1 <= 0 or v2 <= 0 or v4 <= 0 or v12 <= 0 or v10*v13 <= v11*v12 or v10*v14 <= v12*v13 or v18 <= 0 or v9 <> 0 or -(v12*v14*v18) + v12*v14*v3 + v12*v14*v4 + v12*v14*v18*v5 <> v14^2*v9 or v1*v19*v2 + v17*v2^2 <> 0 or -(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 or v1*v19*v2 + v1^2*v20 <> 0
 or -(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;

rlqe ex(optvlist,not (tarskiformula)); % False result here means that tarskiformula is True ForAll

% Mulligan model #0027
write "NGM: The government purchases multiplier"$
optvlist:={v5, v14, v10, v2, v13, v1, v6, v8, v3, v9, v12, v11, v4, v7}$
tarskiformula:=(v4 > 0 and v5 > 0 and v2^2*v5*v7 + v2^2*v4*v8 - v1*v2*v5*v8 > 0 and -1 < v3 and v3 < 0 and v2^2*v5*v7 + v2^2*v4*v8 - v1*v2*v5*v8 < v2^2) or v2*v9 >= 0 or v1^2*v2*v9 >= 0 or v1 <= 0 or v2 <= 0 or v2*v7 <= 0 or v2^2*v7 <= v1*v2*v8 or v8 <= 0 or v10*v13 <= v11*v12 or v10*v14 <= v12*v13 or v6 <> 0 or v2^2 + v2^2*v3 - v2^2*v5*v7 - v2^2*v4*v8 + v1*v2*v5*v8 <> 0 or v2^2*v6 + v1*v5*v9 <> v2*v4*v9
 or 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;

rlqe ex(optvlist,not (tarskiformula)); % False result here means that tarskiformula is True ForAll

% Mulligan model #0028
write "NGM: The government purchases multiplier"$
optvlist:={v5, v8, v12, v19, v11, v9, v4, v16, v3, v17, v10, v7, v2, v18, v15, v1, v14, v6, v13}$
optvlist:={v15, v8, v18, v5, v12, v19, v11, v4, v6, v13, v9, v14, v16, v2, v17, v10, v1, v7, v3}$
tarskiformula:=(v8 > 0 and v11*v2^2*v6 - v1*v11*v2*v8 + v10*v2^2*v8 > 0 and -1 < v5 and v5 < 0 and v7 < 0 and v11*v2^2*v6 - v1*v11*v2*v8 + v10*v2^2*v8 < v2^2) or 0 > v4 or v4 >= 1 or v13*v2 >= 0 or v1^2*v13*v2 >= 0 or v14 >= 0 or v15 >= 0 or v16 >= 0 or v19 >= 0 or v1 <= 0 or v2 <= 0 or v3 <= -1 or v10*v2 <= 0 or v10*v2^2 <= v1*v11*v2 or v11 <= 0 or v12 <= 0 or v17 <= 0 or v15*v18 <= v16*v17 or v15*v19 <= v17*v18
 or -v18^2 + v16*v19 <= 0 or v6 <> 0 or v9 <> 0 or v2^2 + v2^2*v5 - v2^2*v6 - v11*v2^2*v6 + v2^2*v7 + v1*v11*v2*v8 - v10*v2^2*v8 <> 0 or 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 or 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;

rlqe ex(optvlist,not (tarskiformula)); % False result here means that tarskiformula is True ForAll

% Mulligan model #0029
write "NGM: Signing the impact of purchases on labor, separable case"$
optvlist:={v1, v2, v3, v4, v5, v6, v7, v8, v9, v10, v11, v12, v13, v14, v15, v16}$
tarskiformula:=(v5 = 0 and v12*v16 = v14*v15 + v14^2*v7*v8) or 0 > v2 or v10 > 0 or v2 >= 1 or v11 >= 0 or v14*v15*v5 + v14^2*v5*v7*v8 < v12*v16*v5 or v1 <= 0 or v7 <= 0 or v8 <= 0 or v9 <= 0 or v1*v10 + v8 <= 0 or v12*v15 <= v13*v14 or v12*v16 <= v14*v15 or v6 <> 0 or v5*v8 + v4*v9 <> 1 + v3 or v1*v10*v2*v5 + v2*v5*v8 + v1*v7*v8 <> 1 or v11*v4 <> v6 or 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;

rlqe ex(optvlist,not (tarskiformula)); % False result here means that tarskiformula is True ForAll

% Mulligan model #0030
write "NGM: Signing the impact of purchases on labor"$
optvlist:={v5, v13, v6, v2, v10, v9, v3, v16, v4, v15, v1, v12, v11, v8, v7, v14}$
tarskiformula:=(v6 = 0 and v14*v15*v2 - v12*v16*v2 + v14^2*v2*v8*v9 = v1*v10*v14^2*v8) or 0 > v3 or v3 >= 1 or v11*v2 >= 0 or v1^2*v11*v2 >= 0 or 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 or v1 <= 0 or v2 <= 0 or v8 <= 0 or v2*v9 <= 0 or v2^2*v9 <= v1*v10*v2 or v10 <= 0 or v12*v15 <= v13*v14 or v12*v16 <= v14*v15 or v7 <> 0 or v2 + v2*v4 + v1*v10*v6 <> v10*v2*v5 + v2*v6*v9 or v1*v11*v6 + v2^2*v7 <> v11*v2*v5 or 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 or -(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;

rlqe ex(optvlist,not (tarskiformula)); % False result here means that tarskiformula is True ForAll

% Mulligan model #0051
write "Capital taxes in the NGM"$
optvlist:={v18, v5, v14, v7, v17, v12, v6, v16, v13, v11, v1, v9, v3, v4, v19, v10, v15, v20, v8, v2}$
optvlist:={v8, v18, v13, v3, v17, v2, v5, v20, v9, v12, v19, v4, v1, v16, v11, v15, v10, v14, v6, v7}$
tarskiformula:=v6 >= 1 or v7 >= 1 or v11 >= 0 or v12 >= 0 or v15 >= 0 or v17 >= 0 or v12 + v14*v16*(1 - v7) + v13*v17*(1 - v7) >= 0 or v20 >= 0 or v3 < 0 or v4 < 0 or v9 < 0 or v19 < 0 or v1 <= 0 or v2 <= 0 or v5 <= 0 or v13 <= 0 or v11*v14 <= v12*v13 or v11*v15 <= v13*v14 or v16 <= 0 or v18 <= 0 or v18 - v4 <> v3 or v18 - v4 - v5 - 2*v18*v6 + v4*v6 + v5*v6 + v18*v6^2 <> 0 or v10*v16 - v8 + v18*v9 - v4*v9 <> 0
 or v1*v19*v2 + v17*v2^2 <> 0 or 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 or v1*v19*v2 + v1^2*v20 <> 0 or v10*v19 - 2*v10*v19*v6 + v10*v19*v6^2 + v20*v9 - 2*v20*v6*v9 + v20*v6^2*v9 <> v4 + v5;

rlqe ex(optvlist,not (tarskiformula)); % False result here means that tarskiformula is True ForAll

% Mulligan model #0052
write "NGM: private and public consumption as substitutes"$
optvlist:={v30, v29, v28, v27, v26, v25, v24, v23, v22, v21, v20, v19, v18, v17, v16, v15, v14, v13, v12, v11, v10, v9, v8, v7, v6, v5, v4, v3, v2, v1}$
tarskiformula:=v28 + v29 = 0 or v1 >= 1 or v2 >= 1 or v14 >= 0 or v19 >= 0 or v13 <= 0 or v16 <= 0 or v17 <= 0 or -v17^2 + v14*v19 <= 0 or v2 <> v1 or v3 <> 0 or v6 <> 0 or v7 <> 1 or v8 <> 0 or v9 <> v7 or v9 - 2*v1*v9 + v1^2*v9 <> 1 - v1 - v2 + v1*v2 or v11 <> 0 or v12 <> 0 or (1 - v1)*v16 <> v13*(1 - v2) or (1 - v1)*(v17*(v3 - v5) + v19*v5) - v16*v7 <> (1 - v2)*(v14*(v3 - v5) + v17*v5) - v13*v9
 or -(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 or v27*v3 + v24*v7 + v22*v9 <> v13*(v3 - v5) + v16*v5
  or 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);

rlqe ex(optvlist,not (tarskiformula)); % False result here means that tarskiformula is True ForAll

% Mulligan model #0053
write "NGM: Temporary government purchases"$
optvlist:={v1, v2, v3, v4, v5, v6, v7, v8, v9, v10, v11, v12, v13, v14, v15, v16, v17, v18}$
optvlist:={v6, v11, v13, v16, v14, v7, v9, v15, v1, v17, v3, v10, v12, v2, v18, v5, v4, v8}$
tarskiformula:=(v7 > 0 and -1 < v4 and 0 < v7*v9 and v4 < 0 and v6 < 0 and v7*v9 < 1) or 0 > v3 or v12 > 0 or v3 >= 1 or v13 >= 0 or v14 >= 0 or v15 >= 0 or v18 >= 0 or v1 <= 0 or v2 <= -1 or v9 <= 0 or v10 <= 0 or v11 <= 0 or v1*v12 + v9 <= 0 or v16 <= 0 or v14*v17 <= v15*v16 or v14*v18 <= v16*v17 or -v17^2 + v15*v18 <= 0 or v5 <> 0 or v8 <> 0 or v10*v5 + v7*v9 <> 1 + v4 - v5 + v6 or 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
 or v14*v18*v4 + v14*v17*v7 <> v16*v17*v4 + v15*v16*v7 + v12*v16^2*v7;

rlqe ex(optvlist,not (tarskiformula)); % False result here means that tarskiformula is True ForAll

% Mulligan model #0054
write "NGM: Temporary government purchases"$
optvlist:={v5, v2, v4, v10, v6, v12, v18, v14, v16, v1, v17, v3, v13, v11, v7, v8, v9, v15, v19}$
optvlist:={v12, v9, v17, v7, v19, v6, v11, v18, v2, v4, v13, v15, v1, v16, v8, v14, v3, v10, v5}$
tarskiformula:=(v8 > 0 and v11*v2^2*v6 - v1*v11*v2*v8 + v10*v2^2*v8 > 0 and -1 < v5 and v5 < 0 and v7 < 0 and v11*v2^2*v6 - v1*v11*v2*v8 + v10*v2^2*v8 < v2^2) or 0 > v4 or v4 >= 1 or v13*v2 >= 0 or v1^2*v13*v2 >= 0 or v14 >= 0 or v15 >= 0 or v16 >= 0 or v19 >= 0 or v1 <= 0 or v2 <= 0 or v3 <= -1 or v10*v2 <= 0 or v10*v2^2 <= v1*v11*v2 or v11 <= 0 or v12 <= 0 or v17 <= 0 or v15*v18 <= v16*v17 or v15*v19 <= v17*v18 or -v18^2 + v16*v19 <= 0 or v6 <> 0 or v9 <> 0
 or v2^2 + v2^2*v5 - v2^2*v6 - v11*v2^2*v6 + v2^2*v7 + v1*v11*v2*v8 - v10*v2^2*v8 <> 0 or 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 or 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;

rlqe ex(optvlist,not (tarskiformula)); % False result here means that tarskiformula is True ForAll

% Mulligan model #0055
write "NGM: Permanent government purchases"$
optvlist:={v1, v8, v27, v15, v26, v7, v9, v28, v12, v30, v3, v22, v5, v29, v14, v13, v10, v25, v18, v6, v16, v19, v20, v23, v11, v32, v4, v24, v2, v21, v17, v31, v33}$
optvlist:={v33, v23, v28, v10, v32, v29, v12, v15, v25, v8, v20, v3, v11, v14, v17, v22, v31, v6, v18, v4, v24, v9, v1, v27, v26, v5, v7, v19, v16, v30, v2, v21, v13}$
tarskiformula:=0 > v32 or 0 > v33 or v7 > 0 or v10 > 0 or v11 > 0 or v16 > 0 or v17 > 0 or v18 >= 0 or v19 >= 0 or v20 >= 0 or v21 >= 0 or v22 >= 0 or v27 >= 0 or v28 >= 0 or v32 >= 1 or v33 >= 1 or v12 <= 0 or v13 <= 0 or v15 <= 0 or v23 <= 0 or v24 <= 0 or v19*v25 <= v21*v23 or v20*v26 <= v22*v24 or v19*v27 <= v23*v25 or -v25^2 + v21*v27 <= 0 or v20*v28 <= v24*v26 or -v26^2 + v22*v28 <= 0 or v29 <= 0 or v12 + v16*v29 <= 0 or v30 <= 0 or v13 + v17*v30 <= 0
 or v31 <= -1 or v3 <> 1 or v4 <> 1 or v5 <> 0 or v9 <> 0 or v14*v5 + v12*v7 <> v1 + v3 - v5 + v6 or v15*v6 + v13*v8 <> v2 + v4 - v6 or 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 or 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
  or v10*v12*v29 + v12*v32*v7 + v16*v29*v32*v7 <> v3 or 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 or v11*v13*v30 + v13*v33*v8 + v17*v30*v33*v8 <> v4;

rlqe ex(optvlist,not (tarskiformula)); % False result here means that tarskiformula is True ForAll

% Mulligan model #0056
write "Jehle and Reny Theorem 3.1 with three inputs"$
optvlist:={v7, v6, v5, v4, v9, v1, v3, v2, v8, v10, v11, v12}$
tarskiformula:=(v12*v5 >= v10^2 and v12*v8 >= v11^2 and v5*v8 >= v7^2 and v11^2*v5 + v12*v7^2 + (v10^2 - v12*v5)*v8 >= 2*v10*v11*v7 and v12 <= 0 and v5 <= 0 and v8 <= 0) or v1 <= 0 or v2 <= 0 or v3 <= 0 or v4 <= 0 or v6 <= 0 or v9 <= 0 or 2*v11*v6*v9 <= v12*v6^2 + v8*v9^2 or 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 or v1*v12 + v11*v2 + v10*v3 <> 0
 or v1*v10 + v3*v5 + v2*v7 <> 0 or v1*v11 + v3*v7 + v2*v8 <> 0;
rlqe ex(optvlist,not (tarskiformula)); % False result here means that tarskiformula is True ForAll

% Mulligan model #0057
write "A semialgebraic economy's Laffer curve"$
optvlist:={v1, v2, v3, v4, v5, v6, v7, v8, v9, v10, v11, v12, v13, v14}$
tarskiformula:=v6 = v5 or v7 > v8 or 0 >= v13 or v13 >= v14 or v14 >= 1 or v1 <= 0 or v2 <= 0 or v5 <= 0 or v6 <= 0 or v7 <= v10 or v8 <= v9 or (-v1 + v3)*(-v7 + v9) <= 0 or (-v2 + v4)*(v10 - v8) <= 0 or v11 <= 0 or v12 <= 0 or v5^2 <> v1^3 or v6^2 <> v2^3 or 27*v11^3*v5 <> 8 or 27*v12^3*v6 <> 8 or v11*(1 - v13)*(v5 - v6) <> v1 - v4 or v12*(1 - v14)*(-v5 + v6) <> v2 - v3 or v12*v14*v6 <> v11*v13*v5;

rlqe ex(optvlist,not (tarskiformula)); % False result here means that tarskiformula is True ForAll

% Mulligan model #0061
write "Industry Equilibrium: Prices and factor costs"$
optvlist:={v11, v5, v15, v4, v12, v6, v10, v2, v1, v9, v7, v14, v3, v16, v8, v13}$
tarskiformula:=v10*v5 + v11*v6 = v9 or v3^2*v5*v8^2 <> v1*v3*v4*v8 or v3^2*v6*v8^2 <> v2*v3*v7*v8 or v13*v3 <> v3^2*v9 or v14*v4 <> v10*v4^2 or v15*v7 <> v11*v7^2 or v16*v8 <> v1 or v2*v7^2 + v16*v4*v7*v8 - v12*v7^2*v8 <> 0 or v15*v16*v4*v7 + v13*v7^2 - v12*v15*v7^2 - v14*v16*v7^2 <> 0 or v1<=0 or v3<=0 or v4<=0 or v7<=0;

rlqe ex(optvlist,not (tarskiformula)); % False result here means that tarskiformula is True ForAll

% Mulligan model #0062
write "Industry Equilibrium: Long-run relationship between real output and real wages"$
optvlist:={v25, v24, v23, v22, v21, v20, v19, v18, v17, v16, v15, v14, v13, v12, v11, v10, v9, v8, v7, v6, v5, v4, v3, v2, v1}$
tarskiformula:=v13*v15*v6 = v14 or v3^2*v5*v8^2 <> v1*v3*v4*v8 or v3^2*v6*v8^2 <> v2*v3*v7*v8 or v12 <> 0 or v17 <> v8 or v1*v18 <> v1^2*v9 or v19*v2 <> v10*v2^2 or v20*v3 <> v11*v3^2 or v21*v4 <> v12*v4^2 or v22*v7 <> v13*v7^2 or v23*v8 <> v14*v8^2 or v24*v8 <> v1 or v2*v7^2 + v24*v4*v7*v8 - v16*v7^2*v8 <> 0 or v22*v24*v4*v7 + v20*v7^2 - v16*v22*v7^2 - v21*v24*v7^2 <> 0 or v17*v25*v3 <> v15*v17^2 or v20*v25 <> v23 or v1<=0 or v3<=0 or v4<=0 or v7<=0;

rlqe ex(optvlist,not (tarskiformula)); % False result here means that tarskiformula is True ForAll

% Mulligan model #0063
write "Industry Equilibrium: Adding up for factor shares"$
optvlist:={v1, v2, v3, v4, v5, v6, v7, v8, v9, v10}$
tarskiformula:=v6 = 1 - v5 or v3^2*v5*v8^2 <> v1*v3*v4*v8 or v3^2*v6*v8^2 <> v2*v3*v7*v8 or v7*v9 <> v3 or v10*v8 <> v1 or v2*v7^2 + v10*v4*v7*v8 - v7^2*v8*v9 <> 0 or v1<=0 or v3<=0 or v4<=0 or v7<=0;

rlqe ex(optvlist,not (tarskiformula)); % False result here means that tarskiformula is True ForAll

% Mulligan model #0064
write "Industry Equilibrium: Input and output quantities"$
optvlist:={v20, v24, v16, v5, v4, v21, v3, v17, v10, v22, v18, v15, v1, v13, v12, v23, v9, v19, v7, v14, v2, v8, v11, v6}$
tarskiformula:=v13 = v5*(v8 - v9) + v9 or v3^2*v5*v7^2 <> v1*v3*v4*v7 or v11 <> 0 or v14*v6 <> v3 or v1*v15 <> v1^2*v8 or v16*v2 <> v2^2*v9 or v17*v3 <> v10*v3^2 or v18*v4 <> v11*v4^2 or v19*v6 <> v12*v6^2 or v20*v7 <> v13*v7^2 or v22*v7 <> v1 or v2*v6^2 + v22*v4*v6*v7 - v14*v6^2*v7 <> 0 or v1^2*v20 - v1^2*v15*v21 - v1^2*v16*v23 + v1*v15*v2*v23 <> 0 or v20*v22*v4*v6^3 + v16*v6^4 - v14*v20*v6^4 + v18*v24*v4*v6^2*v7 <> v19*v24*v4^2*v6*v7
 or v15*v6^2 - v20*v22*v6^2 + v19*v24*v4*v7 <> v18*v24*v6*v7 or v1<=0 or v2<=0 or v3<=0 or v4<=0 or v7<=0;

rlqe ex(optvlist,not (tarskiformula)); % False result here means that tarskiformula is True ForAll

% Mulligan model #0065
write "Industry Equilibrium: Marshall's Law"$
optvlist:={v20, v24, v28, v21, v14, v18, v8, v19, v2, v3, v5, v11, v9, v6, v16, v13, v25, v4, v27, v29, v22, v17, v12, v10, v1, v26, v23, v7, v15}$
tarskiformula:=v13*(-(v16*v5) + v15*v6) = v10 or v3^2*v5*v8^2 <> v1*v3*v4*v8 or v3^2*v6*v8^2 <> v2*v3*v7*v8 or v12 <> 0 or -(v10*v12) + v10*v13 + v12^2*v16 - 2*v12*v13*v16 + v13^2*v16 + v12*v9 - v13*v9 <> 0 or v17*v7 <> v3 or v18 <> v8 or v1*v19 <> v1^2*v9 or v2*v20 <> v10*v2^2 or v21*v3 <> v11*v3^2 or v22*v4 <> v12*v4^2 or v23*v7 <> v13*v7^2 or v24*v8 <> v14*v8^2 or v26*v8 <> v1 or v2*v7^2 + v26*v4*v7*v8 - v17*v7^2*v8 <> 0
 or v23*v26*v4*v7 + v21*v7^2 - v17*v23*v7^2 - v22*v26*v7^2 <> 0 or v18*v27*v3 <> v15*v18^2 or v21*v27 <> v24 or v1^2*v24 - v1^2*v19*v25 + v1*v19*v2*v28 - v1^2*v20*v28 <> 0 or v24*v26*v4*v7^3 + v20*v7^4 - v17*v24*v7^4 + v22*v29*v4*v7^2*v8 <> v23*v29*v4^2*v7*v8 or v19*v7^2 - v24*v26*v7^2 + v23*v29*v4*v8 <> v22*v29*v7*v8 or v1<=0 or v2<=0 or v3<=0 or v4<=0 or v7<=0;

rlqe ex(optvlist,not (tarskiformula)); % False result here means that tarskiformula is True ForAll

% Mulligan model #0066
write "Industry Equilibrium: Determinants of long-run capital-labor complementarity"$
optvlist:={v12, v11, v1, v10, v9, v5, v2, v6, v7, v8, v3, v4}$
tarskiformula:=v4*v7*(v10 + v9) = v5 or 0 >= v4 or v4 >= 1 or v1 <= 0 or v2 <= 0 or v1^2*v11 <= v1*v12*v2 or v12 <= 0 or v3 + v4 <> 1 or v8 <> v3*(v5 - v6) + v6 or v4*v7*v9 <> v8 or v7*(-(v10*v3) + v4*v9) <> v6;

rlqe ex(optvlist,not (tarskiformula)); % False result here means that tarskiformula is True ForAll

% Mulligan model #0067
write "Industry Equilibrium: Determinants of short-run capital-labor complementarity"$
optvlist:={v30, v16, v15, v6, v31, v13, v5, v20, v21, v23, v22, v9, v2, v18, v11, v28, v19, v3, v10, v8, v29, v17, v25, v24, v7, v1, v26, v27, v12, v4, v14}$
tarskiformula:=v12*(-(v15*v5) + v16*v6) = v13*(v15 + v16)*v6 or 0 >= v6 or v6 >= 1 or v1 <= 0 or v2 <= 0 or v3 <= 0 or v4 <= 0 or v7 <= 0 or v8 <= 0 or v1^2*v26 <= v1*v2*v30 or v30 <= 0 or v5 + v6 <> 1 or v3^2*v5*v8^2 <> v1*v3*v4*v8 or v3^2*v6*v8^2 <> v2*v3*v7*v8 or v9 <> 0 or -(v10*v12) + v10*v13 + v12^2*v16 - 2*v12*v13*v16 + v13^2*v16 + v12*v9 - v13*v9 <> 0 or v18 <> v8 or v1*v19 <> v1^2*v9 or v2*v20 <> v10*v2^2 or v21*v3 <> v11*v3^2 or v22*v4 <> v12*v4^2
 or v23*v7 <> v13*v7^2 or v24*v8 <> v14*v8^2 or v27*v8 <> v1 or v2*v7^2 + v27*v4*v7*v8 - v17*v7^2*v8 <> 0 or v23*v27*v4*v7 + v21*v7^2 - v17*v23*v7^2 - v22*v27*v7^2 <> 0 or v18*v28*v3 <> v15*v18^2 or v21*v28 <> v24 or v1^2*v24 - v1^2*v19*v25 + v1*v19*v2*v29 - v1^2*v20*v29 <> 0 or v24*v27*v4*v7^3 + v20*v7^4 - v17*v24*v7^4 + v22*v31*v4*v7^2*v8 <> v23*v31*v4^2*v7*v8 or v19*v7^2 - v24*v27*v7^2 + v23*v31*v4*v8 <> v22*v31*v7*v8;

rlqe ex(optvlist,not (tarskiformula)); % False result here means that tarskiformula is True ForAll

% Mulligan model #0074
write "Supply-Demand: Global demand analysis"$
optvlist:={v1, v2, v3, v4, v5, v6, v7, v8}$
tarskiformula:=v7 > v8 or v3 >= v4 or (v1 - v3)*(v7 - v8) >= 0 or (v2 - v4)*(v7 - v8) >= 0 or (v5 - v6)*(v7 - v8) <= 0 or v5 <> v2 or v6 <> v3;

rlqe ex(optvlist,not (tarskiformula)); % False result here means that tarskiformula is True ForAll

% Mulligan model #0076
write "Vector mode: Variance of a sum"$
optvlist:={v4, v5, v2, v9, v7, v3, v8, v6, v1}$
tarskiformula:=2*v5 + v6 + 2*v2*v7 + v1*v9^2 >= v1*v7^2 + 2*(v2 + v3)*v9 or v1 < 1 or v4 < 0 or v1*v4 < v2^2 or v6 < 0 or v1*v6 < v3^2 or v4*v6 < v5^2 or v5 + v1*v7*v8 < v3*v7 + v2*v8 or v9 <> v7 + v8;

rlqe ex(optvlist,not (tarskiformula)); % False result here means that tarskiformula is True ForAll

% Mulligan model #0077
write "Vector mode: Variance of a sum"$
optvlist:={v4, v9, v5, v6, v7, v3, v1, v2, v8}$
tarskiformula:=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 or v1 < 1 or v4 < 0 or v1*v4 < v2^2 or v6 < 0 or v1*v6 < v3^2 or v4*v6 < v5^2 or v1*v5 - v1*v3*v7 - v1*v2*v8 + v1^2*v7*v8 < 0 or v9 <> v7 + v8;

rlqe ex(optvlist,not (tarskiformula)); % False result here means that tarskiformula is True ForAll

% Mulligan model #0078
write "Vector mode: Hicks' generalized law of demand"$
optvlist:={v1, v10, v2, v3, v4, v5, v6, v7, v8, v9}$
tarskiformula:=v2 > v3 or v9 > v7 or v1 < 0 or v5 < 0 or v1*v5 < v2^2 or v8 < 0 or v1*v8 < v3^2 or v5*v8 < v6^2 or 2*v2*v3*v6 + v1*v5*v8 < v3^2*v5 + v1*v6^2 + v2^2*v8 or v10 < 0 or v1*v10 < v4^2 or v10*v5 < v7^2 or v10*v8 < v9^2 or v1*v10*v5 + 2*v2*v4*v7 < v10*v2^2 + v4^2*v5 + v1*v7^2 or v1*v10*v8 + 2*v3*v4*v9 < v10*v3^2 + v4^2*v8 + v1*v9^2
 or 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)) or 2*v6*v7*v9 + v5*(v10*v8 - v9^2) < v10*v6^2 + v7^2*v8 or v2 + v9 <= v3 + v7;

rlqe ex(optvlist,not (tarskiformula)); % False result here means that tarskiformula is True ForAll

% Mulligan model #0079
write "Vector mode: Progressive policy and inequality"$
optvlist:={v1, v2, v3, v4, v5, v6}$
tarskiformula:=2*v1*v3 + v6 >= 2*v5 or v1^2 < 0 or v4 < 0 or v6 < 0 or v2*v6 < v3^2 or v4*v6 < v5^2 or v5 <= v1*v3;

rlqe ex(optvlist,not (tarskiformula)); % False result here means that tarskiformula is True ForAll

% Mulligan model #0080
write "Vector mode: Consumer Theory Adding Up"$
optvlist:={v1, v2, v3, v4, v5, v6, v7, v8, v9, v10, v11, v12}$
tarskiformula:=v9 = 0 or v3 < 0 or v7 < 0 or v3*v7 < v4^2 or v10 < 0 or v10*v3 < v5^2 or v10*v7 < v8^2 or v10*v3*v7 + 2*v4*v5*v8 < v10*v4^2 + v5^2*v7 + v3*v8^2 or v12 < 0 or v12*v3 < v6^2 or v12*v7 < v9^2 or v10*v12 < v11^2 or v12*v3*v7 + 2*v4*v6*v9 < v12*v4^2 + v6^2*v7 + v3*v9^2 or v10*v12*v3 + 2*v11*v5*v6 < v11^2*v3 + v12*v5^2 + v10*v6^2 or v10*v12*v7 + 2*v11*v8*v9 < v11^2*v7 + v12*v8^2 + v10*v9^2
 or 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)) or v1 <= 0 or v2 <= 0 or v2*v5 <> 0 or v1*v9 <> v5;

rlqe ex(optvlist,not (tarskiformula)); % False result here means that tarskiformula is True ForAll

% Mulligan model #0082
write "Vector mode: Constant absolute risk aversion"$
optvlist:={v1, v2, v3, v4, v5, v6, v7, v8, v9, v10}$
tarskiformula:=v10 = 0 or v4 < 0 or v7 < 0 or v4*v7 < v5^2 or v9 < 0 or v2*v9 < v3^2 or v4*v9 < v6^2 or v7*v9 < v8^2 or 2*v5*v6*v8 + v4*(-v8^2 + v7*v9) < v6^2*v7 + v5^2*v9 or v1 <= 0 or v3 + v8 <= 2*v6 or v6 <> v3 or v1*((-1 + v10)*v3 + (1 - 2*v10)*v6 + v10*v8) <> 0;

rlqe ex(optvlist,not (tarskiformula)); % False result here means that tarskiformula is True ForAll

% Mulligan model #0083
write "Vector mode: Constant absolute risk aversion"$
optvlist:={v1, v2, v3, v4, v5, v6, v7, v8, v9, v10}$
tarskiformula:=v10 = 0 or v2 < 1 or v4 < 0 or v7 < 0 or v4*v7 < v5^2 or v9 < 0 or v2*v9 < v3^2 or v4*v9 < v6^2 or v7*v9 < v8^2 or 2*v5*v6*v8 + v4*(-v8^2 + v7*v9) < v6^2*v7 + v5^2*v9 or v1 <= 0 or v4 <= 0 or v1*v2*(v3 - 2*v6 + v8) <= 0 or v1^2*v9 <= 0 or v1*v2*v6 <> v1*v2*v3 or -(v2*v3) + v10*v2*v3 + v2*v6 - 2*v10*v2*v6 + v10*v2*v8 <> 0;

rlqe ex(optvlist,not (tarskiformula)); % False result here means that tarskiformula is True ForAll

% Mulligan model #0084
write "Vector mode: Constant relative risk aversion"$
optvlist:={v12, v11, v10, v9, v8, v7, v6, v5, v4, v3, v2, v1}$
tarskiformula:=v12 = 0 or 0 > v2 or v2 > 1 or v3^2*v4*(v10 + v5 - 2*v8) >= 0 or v4 < 1 or v6 < 0 or v9 < 0 or v6*v9 < v7^2 or v11 < 0 or v11*v4 < v5^2 or v11*v6 < v8^2 or v11*v9 < v10^2 or 2*v10*v7*v8 + v6*(-v10^2 + v11*v9) < v11*v7^2 + v8^2*v9 or v1 <= 0 or v3 <= 0 or 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
 or 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;

rlqe ex(optvlist,not (tarskiformula)); % False result here means that tarskiformula is True ForAll

% Mulligan model #0085
write "Vector mode: Correlation between wealth and marginal utility"$
optvlist:={v1, v2, v3, v4, v5, v6, v7, v8}$
tarskiformula:=v3 < 1 or v6 < 0 or v3*v6 < v4^2 or v1*v2*v3 + v7 < v2*v4 + v1*v5 or v8 < 0 or v3*v8 < v5^2 or v6*v8 < v7^2 or v3*v4 <= v3^2 or v3*v5 <= 0 or v3*v4 <> v1*v3^2 or v3*v5 <> v2*v3^2 or v3*v7 <> v3*v5;

rlqe ex(optvlist,not (tarskiformula)); % False result here means that tarskiformula is True ForAll

% Mulligan model #0086
write "Vector mode: Risk aversion reduces investment"$
optvlist:={v1, v2, v3, v4, v5, v6, v7, v8, v9, v10, v11, v12, v13, v14, v15, v16, v17, v18, v19}$
optvlist:={v9, v6, v17, v7, v4, v12, v2, v16, v11, v1, v14, v5, v8, v19, v10, v13, v18, v15, v3}$
tarskiformula:=v7 >= v2 or v1*(v12 + v3 - 2*v8) >= 0 or v1 < 1 or v4 < 0 or v9 < 0 or v4*v9 < v5^2 or v13 < 0 or v13*v4 < v6^2 or v13*v9 < v10^2 or 2*v10*v5*v6 + v4*(-v10^2 + v13*v9) < v13*v5^2 + v6^2*v9 or v16 < 0 or v1*v16 < v2^2 or v16*v4 < v7^2 or v16*v9 < v11^2 or v13*v16 < v14^2 or 2*v11*v5*v7 + v4*(-v11^2 + v16*v9) < v16*v5^2 + v7^2*v9
 or 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)) or (-v14^2 + v13*v16)*v4 + 2*v14*v6*v7 < v16*v6^2 + v13*v7^2 or 2*v10*v11*v14 + (-v14^2 + v13*v16)*v9 < v11^2*v13 + v10^2*v16 or v18 < 0 or v1*v18 < v3^2 or v18*v4 < v8^2 or v18*v9 < v12^2 or v13*v18 < v15^2 or v16*v18 < v17^2 or 2*v12*v5*v8 + v4*(-v12^2 + v18*v9) < v18*v5^2 + v8^2*v9
 or 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)) or 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))
 or (-v15^2 + v13*v18)*v4 + 2*v15*v6*v8 < v18*v6^2 + v13*v8^2
 or 2*v10*v12*v15 + (-v15^2 + v13*v18)*v9 < v12^2*v13 + v10^2*v18 or 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
 or 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 or (-v17^2 + v16*v18)*v4 + 2*v17*v7*v8 < v18*v7^2 + v16*v8^2 or 2*v11*v12*v17 + (-v17^2 + v16*v18)*v9 < v12^2*v16 + v11^2*v18 or 2*v14*v15*v17 + v13*(-v17^2 + v16*v18) < v15^2*v16 + v14^2*v18
 or 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)) or v19 < 0 or v13 <= 0
 or v1*v12*v19 - v1*v2 + v1*v19*v3 + v1*v7 - 2*v1*v19*v8 <> 0;

rlqe ex(optvlist,not (tarskiformula)); % False result here means that tarskiformula is True ForAll

% Mulligan model #1001
write "Constant absolute risk aversion with states delineated"$
optvlist:={v36, v3, v2, v37, v38, v39, v40, v41, v42, v43, v44, v45, v46, v47, v48, v49, v50, v51, v52, v53, v54, v55, v56, v57, v58, v59, v60, v61, v62, v63, v64, v65, v66, v67, v68, v69, v70, v71, v72, v73, v74, v75, v76, v77, v78, v79, v80, v81, v82, v83, v84, v85, v86, v87, v88, v89, v90, v91, v92, v93, v94, v95, v96, v97, v98, v99, v100, v101, v1, v3, v4, v5, v6, v7, v8, v9, v10, v11, v12, v13, v14, v15, v16, v17, v18, v19, v20, v21, v22, v23, v24, v25,
 v26, v27, v28, v29, v30, v31, v32, v33, v34}$
tarskiformula:=v2 = 0 or v3 >= 1 or 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 or v1 <= 0 or 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 or (-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 or v69 <> -(v1*v36) or v70 <> -(v1*v37) or v71 <> -(v1*v38) or v72 <> -(v1*v39) or v73 <> -(v1*v40) or v74 <> -(v1*v41) or v75 <> -(v1*v42) or v76 <> -(v1*v43) or v77 <> -(v1*v44) or v78 <> -(v1*v45) or v79 <> -(v1*v46) or v80 <> -(v1*v47) or v81 <> -(v1*v48) or v82 <> -(v1*v49) or v83 <> -(v1*v50) or v84 <> -(v1*v51) or v85 <> -(v1*v52) or v86 <> -(v1*v53) or v87 <> -(v1*v54) or v88 <> -(v1*v55) or v89 <> -(v1*v56) or v90 <> -(v1*v57)
    or v91 <> -(v1*v58) or v92 <> -(v1*v59) or v93 <> -(v1*v60) or v94 <> -(v1*v61) or v95 <> -(v1*v62) or v96 <> -(v1*v63) or v97 <> -(v1*v64) or v98 <> -(v1*v65) or v99 <> -(v1*v66) or v100 <> -(v1*v67) or v101 <> -(v1*v68) or 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;

rlqe ex(optvlist,not (tarskiformula)); % False result here means that tarskiformula is True ForAll
bye;