off rlabout;



rlset reals;


{}


testseries12 :=
400*q + 9*td - 20050 > 0 and 200*i2 - 10*q - td + 385 = 0 and n - td = 0
 and n >= 0 and q - 40 <= 0 and q >= 0 and 20*n - 2*td - 300*z - 8331 =
0 and 2*p1 - 7 >= 0 and 80*i2 + 250*p1 + 2*q - 1377 = 0 and (td - 400 >=
 0 and td - 700 < 0 and 3*td + 400*z - 6130 = 0 or td - 700 >= 0 and td
- 990 < 0 and 4*td - 600*z + 3245 = 0) or 400*q + 9*td - 20050 > 0 and
200*i2 - 10*q - td + 385 = 0 and n - td = 0 and n >= 0 and q - 40 <= 0
and q >= 0 and 100*n - 10*td - 2500*z - 36519 = 0 and 2*p1 - 7 >= 0 and
80*i2 + 250*p1 + 2*q - 1457 = 0 and (td - 400 >= 0 and td - 700 < 0 and
3*td + 400*z - 6130 = 0 or td - 700 >= 0 and td - 990 < 0 and 4*td - 600
*z + 3245 = 0) or 400*q + 9*td - 20050 > 0 and 200*i2 - 10*q - td + 385
= 0 and n - td = 0 and n >= 0 and q - 40 <= 0 and q >= 0 and (80*i2 +
250*p1 + 2*q - 1057 > 0 and 80*i2 + 250*p1 + 2*q - 1377 <= 0 and 1480*i2
 - 50*n + 4625*p1 + 37*q + 5*td + 750*z - 4647 = 0 or 80*i2 + 250*p1 + 2
*q - 1377 > 0 and 80*i2 + 250*p1 + 2*q - 1457 <= 0 and 76880*i2 - 2000*n
 + 240250*p1 + 1922*q + 200*td + 50000*z - 669797 = 0 or 80*i2 + 250*p1
+ 2*q - 1457 > 0 and 80*i2 + 250*p1 + 2*q - 1697 < 0 and 10750000*i2 +
500000*n + 33593750*p1 + 268750*q - 50000*td - 10000000*z - 402109359 =
0) and (td - 400 >= 0 and td - 700 < 0 and 3*td + 400*z - 6130 = 0 or td
 - 700 >= 0 and td - 990 < 0 and 4*td - 600*z + 3245 = 0) and (2*p1 - 7
< 0 and 80*i2 + 250*p1 + 2*q - 577 = 0 or 2*p1 - 7 >= 0) or 400*q + 9*td
 - 20050 > 0 and i2 = 0 and n - td = 0 and n >= 0 and q - 40 <= 0 and q
>= 0 and 20*n - 2*td - 300*z - 8331 = 0 and 2*p1 - 7 >= 0 and 80*i2 +
250*p1 + 2*q - 1377 = 0 and (td - 400 >= 0 and td - 700 < 0 and 3*td +
400*z - 5320 = 0 or td - 700 >= 0 and td - 990 < 0 and 2*td - 300*z +
1015 = 0 or td = 0 and z = 0) or 400*q + 9*td - 20050 > 0 and i2 = 0 and
 n - td = 0 and n >= 0 and q - 40 <= 0 and q >= 0 and 100*n - 10*td -
2500*z - 36519 = 0 and 2*p1 - 7 >= 0 and 80*i2 + 250*p1 + 2*q - 1457 = 0
 and (td - 400 >= 0 and td - 700 < 0 and 3*td + 400*z - 5320 = 0 or td -
 700 >= 0 and td - 990 < 0 and 2*td - 300*z + 1015 = 0 or td = 0 and z =
 0) or 400*q + 9*td - 20050 > 0 and i2 = 0 and n - td = 0 and n >= 0 and
 q - 40 <= 0 and q >= 0 and (80*i2 + 250*p1 + 2*q - 1057 > 0 and 80*i2 +
 250*p1 + 2*q - 1377 <= 0 and 1480*i2 - 50*n + 4625*p1 + 37*q + 5*td +
750*z - 4647 = 0 or 80*i2 + 250*p1 + 2*q - 1377 > 0 and 80*i2 + 250*p1 +
 2*q - 1457 <= 0 and 76880*i2 - 2000*n + 240250*p1 + 1922*q + 200*td +
50000*z - 669797 = 0 or 80*i2 + 250*p1 + 2*q - 1457 > 0 and 80*i2 + 250*
p1 + 2*q - 1697 < 0 and 10750000*i2 + 500000*n + 33593750*p1 + 268750*q
- 50000*td - 10000000*z - 402109359 = 0) and (td - 400 >= 0 and td - 700
 < 0 and 3*td + 400*z - 5320 = 0 or td - 700 >= 0 and td - 990 < 0 and 2
*td - 300*z + 1015 = 0 or td = 0 and z = 0) and (2*p1 - 7 < 0 and 80*i2
+ 250*p1 + 2*q - 577 = 0 or 2*p1 - 7 >= 0) or 400*q + 9*td - 20050 <= 0
and 200*i2 - 10*q - td + 385 = 0 and n - td = 0 and n >= 0 and q - 40 <=
 0 and q >= 0 and 20*n - 2*td - 300*z - 8331 = 0 and 2*p1 - 7 >= 0 and
80*i2 + 250*p1 + 2*q - 1377 = 0 and (td - 400 >= 0 and td - 700 < 0 and
3*td + 400*z - 6130 = 0 or td - 700 >= 0 and td - 990 < 0 and 4*td - 600
*z + 3245 = 0) or 400*q + 9*td - 20050 <= 0 and 200*i2 - 10*q - td + 385
 = 0 and n - td = 0 and n >= 0 and q - 40 <= 0 and q >= 0 and 100*n - 10
*td - 2500*z - 36519 = 0 and 2*p1 - 7 >= 0 and 80*i2 + 250*p1 + 2*q -
1457 = 0 and (td - 400 >= 0 and td - 700 < 0 and 3*td + 400*z - 6130 = 0
 or td - 700 >= 0 and td - 990 < 0 and 4*td - 600*z + 3245 = 0) or 400*q
 + 9*td - 20050 <= 0 and 200*i2 - 10*q - td + 385 = 0 and n - td = 0 and
 n >= 0 and q - 40 <= 0 and q >= 0 and (80*i2 + 250*p1 + 2*q - 1057 > 0
and 80*i2 + 250*p1 + 2*q - 1377 <= 0 and 1480*i2 - 50*n + 4625*p1 + 37*q
 + 5*td + 750*z - 4647 = 0 or 80*i2 + 250*p1 + 2*q - 1377 > 0 and 80*i2
+ 250*p1 + 2*q - 1457 <= 0 and 76880*i2 - 2000*n + 240250*p1 + 1922*q +
200*td + 50000*z - 669797 = 0 or 80*i2 + 250*p1 + 2*q - 1457 > 0 and 80*
i2 + 250*p1 + 2*q - 1697 < 0 and 10750000*i2 + 500000*n + 33593750*p1 +
268750*q - 50000*td - 10000000*z - 402109359 = 0) and (td - 400 >= 0 and
 td - 700 < 0 and 3*td + 400*z - 6130 = 0 or td - 700 >= 0 and td - 990
< 0 and 4*td - 600*z + 3245 = 0) and (2*p1 - 7 < 0 and 80*i2 + 250*p1 +
2*q - 577 = 0 or 2*p1 - 7 >= 0) or 400*q + 9*td - 20050 <= 0 and i2 = 0
and n - td = 0 and n >= 0 and q - 40 <= 0 and q >= 0 and 20*n - 2*td -
300*z - 8331 = 0 and 2*p1 - 7 >= 0 and 80*i2 + 250*p1 + 2*q - 1377 = 0
and (td - 400 >= 0 and td - 700 < 0 and 3*td + 400*z - 5320 = 0 or td -
700 >= 0 and td - 990 < 0 and 2*td - 300*z + 1015 = 0 or td = 0 and z =
0) or 400*q + 9*td - 20050 <= 0 and i2 = 0 and n - td = 0 and n >= 0 and
 q - 40 <= 0 and q >= 0 and 100*n - 10*td - 2500*z - 36519 = 0 and 2*p1
- 7 >= 0 and 80*i2 + 250*p1 + 2*q - 1457 = 0 and (td - 400 >= 0 and td -
 700 < 0 and 3*td + 400*z - 5320 = 0 or td - 700 >= 0 and td - 990 < 0
and 2*td - 300*z + 1015 = 0 or td = 0 and z = 0) or 400*q + 9*td - 20050
 <= 0 and i2 = 0 and n - td = 0 and n >= 0 and q - 40 <= 0 and q >= 0
and (80*i2 + 250*p1 + 2*q - 1057 > 0 and 80*i2 + 250*p1 + 2*q - 1377 <=
0 and 1480*i2 - 50*n + 4625*p1 + 37*q + 5*td + 750*z - 4647 = 0 or 80*i2
 + 250*p1 + 2*q - 1377 > 0 and 80*i2 + 250*p1 + 2*q - 1457 <= 0 and
76880*i2 - 2000*n + 240250*p1 + 1922*q + 200*td + 50000*z - 669797 = 0
or 80*i2 + 250*p1 + 2*q - 1457 > 0 and 80*i2 + 250*p1 + 2*q - 1697 < 0
and 10750000*i2 + 500000*n + 33593750*p1 + 268750*q - 50000*td -
10000000*z - 402109359 = 0) and (td - 400 >= 0 and td - 700 < 0 and 3*td
 + 400*z - 5320 = 0 or td - 700 >= 0 and td - 990 < 0 and 2*td - 300*z +
 1015 = 0 or td = 0 and z = 0) and (2*p1 - 7 < 0 and 80*i2 + 250*p1 + 2*
q - 577 = 0 or 2*p1 - 7 >= 0) or 400*q + 9*td - 20050 > 0 and 200*i2 -
10*q - td + 385 = 0 and n - td = 0 and 27*n + 57*td + 7600*z - 116470 >=
 0 and 3*td + 400*z - 3730 >= 0 and 3*td + 400*z - 6130 <= 0 and q - 40
<= 0 and q >= 0 and 120*n + 3*td + 200*z - 80636 = 0 and 2*p1 - 7 >= 0
and 80*i2 + 250*p1 + 2*q - 1377 = 0 and (td - 400 >= 0 and td - 700 < 0
or td - 990 < 0 and td - 700 = 0) or 400*q + 9*td - 20050 > 0 and 200*i2
 - 10*q - td + 385 = 0 and n - td = 0 and 27*n + 57*td + 7600*z - 116470
 >= 0 and 3*td + 400*z - 3730 >= 0 and 3*td + 400*z - 6130 <= 0 and q -
40 <= 0 and q >= 0 and 600*n + 15*td - 5000*z - 372364 = 0 and 2*p1 - 7
>= 0 and 80*i2 + 250*p1 + 2*q - 1457 = 0 and (td - 400 >= 0 and td - 700
 < 0 or td - 990 < 0 and td - 700 = 0) or 400*q + 9*td - 20050 > 0 and
200*i2 - 10*q - td + 385 = 0 and n - td = 0 and 27*n + 57*td + 7600*z -
116470 >= 0 and 3*td + 400*z - 3730 >= 0 and 3*td + 400*z - 6130 <= 0
and q - 40 <= 0 and q >= 0 and (80*i2 + 250*p1 + 2*q - 1057 > 0 and 80*
i2 + 250*p1 + 2*q - 1377 <= 0 and 17760*i2 - 600*n + 55500*p1 + 444*q -
15*td - 1000*z + 97486 = 0 or 80*i2 + 250*p1 + 2*q - 1377 > 0 and 80*i2
+ 250*p1 + 2*q - 1457 <= 0 and 230640*i2 - 6000*n + 720750*p1 + 5766*q -
 150*td + 50000*z - 476891 = 0 or 80*i2 + 250*p1 + 2*q - 1457 > 0 and 80
*i2 + 250*p1 + 2*q - 1697 < 0 and 32250000*i2 + 1500000*n + 100781250*p1
 + 806250*q + 37500*td - 5000000*z - 1589453077 = 0) and (td - 400 >= 0
and td - 700 < 0 or td - 990 < 0 and td - 700 = 0) and (2*p1 - 7 < 0 and
 80*i2 + 250*p1 + 2*q - 577 = 0 or 2*p1 - 7 >= 0) or 400*q + 9*td -
20050 > 0 and i2 = 0 and n - td = 0 and 27*n + 57*td + 7600*z - 116470
>= 0 and 3*td + 400*z - 3730 >= 0 and 3*td + 400*z - 6130 <= 0 and q -
40 <= 0 and q >= 0 and 120*n + 3*td + 200*z - 80636 = 0 and 2*p1 - 7 >=
0 and 80*i2 + 250*p1 + 2*q - 1377 = 0 and (td - 400 >= 0 and td - 700 <
0 and 3*td + 400*z - 5320 = 0 or td - 700 >= 0 and td - 990 < 0 and 2*td
 - 300*z + 1015 = 0 or td = 0 and z = 0) or 400*q + 9*td - 20050 > 0 and
 i2 = 0 and n - td = 0 and 27*n + 57*td + 7600*z - 116470 >= 0 and 3*td
+ 400*z - 3730 >= 0 and 3*td + 400*z - 6130 <= 0 and q - 40 <= 0 and q
>= 0 and 600*n + 15*td - 5000*z - 372364 = 0 and 2*p1 - 7 >= 0 and 80*i2
 + 250*p1 + 2*q - 1457 = 0 and (td - 400 >= 0 and td - 700 < 0 and 3*td
+ 400*z - 5320 = 0 or td - 700 >= 0 and td - 990 < 0 and 2*td - 300*z +
1015 = 0 or td = 0 and z = 0) or 400*q + 9*td - 20050 > 0 and i2 = 0 and
 n - td = 0 and 27*n + 57*td + 7600*z - 116470 >= 0 and 3*td + 400*z -
3730 >= 0 and 3*td + 400*z - 6130 <= 0 and q - 40 <= 0 and q >= 0 and (
80*i2 + 250*p1 + 2*q - 1057 > 0 and 80*i2 + 250*p1 + 2*q - 1377 <= 0 and
 17760*i2 - 600*n + 55500*p1 + 444*q - 15*td - 1000*z + 97486 = 0 or 80*
i2 + 250*p1 + 2*q - 1377 > 0 and 80*i2 + 250*p1 + 2*q - 1457 <= 0 and
230640*i2 - 6000*n + 720750*p1 + 5766*q - 150*td + 50000*z - 476891 = 0
or 80*i2 + 250*p1 + 2*q - 1457 > 0 and 80*i2 + 250*p1 + 2*q - 1697 < 0
and 32250000*i2 + 1500000*n + 100781250*p1 + 806250*q + 37500*td -
5000000*z - 1589453077 = 0) and (td - 400 >= 0 and td - 700 < 0 and 3*td
 + 400*z - 5320 = 0 or td - 700 >= 0 and td - 990 < 0 and 2*td - 300*z +
 1015 = 0 or td = 0 and z = 0) and (2*p1 - 7 < 0 and 80*i2 + 250*p1 + 2*
q - 577 = 0 or 2*p1 - 7 >= 0) or 400*q + 9*td - 20050 <= 0 and 200*i2 -
10*q - td + 385 = 0 and n - td = 0 and 27*n + 57*td + 7600*z - 116470 >=
 0 and 3*td + 400*z - 3730 >= 0 and 3*td + 400*z - 6130 <= 0 and q - 40
<= 0 and q >= 0 and 120*n + 3*td + 200*z - 80636 = 0 and 2*p1 - 7 >= 0
and 80*i2 + 250*p1 + 2*q - 1377 = 0 and (td - 400 >= 0 and td - 700 < 0
or td - 990 < 0 and td - 700 = 0) or 400*q + 9*td - 20050 <= 0 and 200*
i2 - 10*q - td + 385 = 0 and n - td = 0 and 27*n + 57*td + 7600*z -
116470 >= 0 and 3*td + 400*z - 3730 >= 0 and 3*td + 400*z - 6130 <= 0
and q - 40 <= 0 and q >= 0 and 600*n + 15*td - 5000*z - 372364 = 0 and 2
*p1 - 7 >= 0 and 80*i2 + 250*p1 + 2*q - 1457 = 0 and (td - 400 >= 0 and
td - 700 < 0 or td - 990 < 0 and td - 700 = 0) or 400*q + 9*td - 20050
<= 0 and 200*i2 - 10*q - td + 385 = 0 and n - td = 0 and 27*n + 57*td +
7600*z - 116470 >= 0 and 3*td + 400*z - 3730 >= 0 and 3*td + 400*z -
6130 <= 0 and q - 40 <= 0 and q >= 0 and (80*i2 + 250*p1 + 2*q - 1057 >
0 and 80*i2 + 250*p1 + 2*q - 1377 <= 0 and 17760*i2 - 600*n + 55500*p1 +
 444*q - 15*td - 1000*z + 97486 = 0 or 80*i2 + 250*p1 + 2*q - 1377 > 0
and 80*i2 + 250*p1 + 2*q - 1457 <= 0 and 230640*i2 - 6000*n + 720750*p1
+ 5766*q - 150*td + 50000*z - 476891 = 0 or 80*i2 + 250*p1 + 2*q - 1457
> 0 and 80*i2 + 250*p1 + 2*q - 1697 < 0 and 32250000*i2 + 1500000*n +
100781250*p1 + 806250*q + 37500*td - 5000000*z - 1589453077 = 0) and (td
 - 400 >= 0 and td - 700 < 0 or td - 990 < 0 and td - 700 = 0) and (2*p1
 - 7 < 0 and 80*i2 + 250*p1 + 2*q - 577 = 0 or 2*p1 - 7 >= 0) or 400*q +
 9*td - 20050 <= 0 and i2 = 0 and n - td = 0 and 27*n + 57*td + 7600*z -
 116470 >= 0 and 3*td + 400*z - 3730 >= 0 and 3*td + 400*z - 6130 <= 0
and q - 40 <= 0 and q >= 0 and 120*n + 3*td + 200*z - 80636 = 0 and 2*p1
 - 7 >= 0 and 80*i2 + 250*p1 + 2*q - 1377 = 0 and (td - 400 >= 0 and td
- 700 < 0 and 3*td + 400*z - 5320 = 0 or td - 700 >= 0 and td - 990 < 0
and 2*td - 300*z + 1015 = 0 or td = 0 and z = 0) or 400*q + 9*td - 20050
 <= 0 and i2 = 0 and n - td = 0 and 27*n + 57*td + 7600*z - 116470 >= 0
and 3*td + 400*z - 3730 >= 0 and 3*td + 400*z - 6130 <= 0 and q - 40 <=
0 and q >= 0 and 600*n + 15*td - 5000*z - 372364 = 0 and 2*p1 - 7 >= 0
and 80*i2 + 250*p1 + 2*q - 1457 = 0 and (td - 400 >= 0 and td - 700 < 0
and 3*td + 400*z - 5320 = 0 or td - 700 >= 0 and td - 990 < 0 and 2*td -
 300*z + 1015 = 0 or td = 0 and z = 0) or 400*q + 9*td - 20050 <= 0 and
i2 = 0 and n - td = 0 and 27*n + 57*td + 7600*z - 116470 >= 0 and 3*td +
 400*z - 3730 >= 0 and 3*td + 400*z - 6130 <= 0 and q - 40 <= 0 and q >=
 0 and (80*i2 + 250*p1 + 2*q - 1057 > 0 and 80*i2 + 250*p1 + 2*q - 1377
<= 0 and 17760*i2 - 600*n + 55500*p1 + 444*q - 15*td - 1000*z + 97486 =
0 or 80*i2 + 250*p1 + 2*q - 1377 > 0 and 80*i2 + 250*p1 + 2*q - 1457 <=
0 and 230640*i2 - 6000*n + 720750*p1 + 5766*q - 150*td + 50000*z -
476891 = 0 or 80*i2 + 250*p1 + 2*q - 1457 > 0 and 80*i2 + 250*p1 + 2*q -
 1697 < 0 and 32250000*i2 + 1500000*n + 100781250*p1 + 806250*q + 37500*
td - 5000000*z - 1589453077 = 0) and (td - 400 >= 0 and td - 700 < 0 and
 3*td + 400*z - 5320 = 0 or td - 700 >= 0 and td - 990 < 0 and 2*td -
300*z + 1015 = 0 or td = 0 and z = 0) and (2*p1 - 7 < 0 and 80*i2 + 250*
p1 + 2*q - 577 = 0 or 2*p1 - 7 >= 0) or 400*q + 9*td - 20050 > 0 and td
- 700 >= 0 and td - 990 < 0 and 200*i2 - 10*q - td + 385 = 0 and n - td
= 0 and 81*n - 152*td + 22800*z - 123310 >= 0 and 4*td - 600*z - 355 <=
0 and 4*td - 600*z + 3245 >= 0 and q - 40 <= 0 and q >= 0 and 90*n - 19*
td + 150*z - 45602 = 0 and 2*p1 - 7 >= 0 and 80*i2 + 250*p1 + 2*q - 1377
 = 0 or 400*q + 9*td - 20050 > 0 and td - 700 >= 0 and td - 990 < 0 and
200*i2 - 10*q - td + 385 = 0 and n - td = 0 and 81*n - 152*td + 22800*z
- 123310 >= 0 and 4*td - 600*z - 355 <= 0 and 4*td - 600*z + 3245 >= 0
and q - 40 <= 0 and q >= 0 and 450*n - 95*td - 3750*z - 204898 = 0 and 2
*p1 - 7 >= 0 and 80*i2 + 250*p1 + 2*q - 1457 = 0 or 400*q + 9*td - 20050
 > 0 and td - 700 >= 0 and td - 990 < 0 and 200*i2 - 10*q - td + 385 = 0
 and n - td = 0 and 81*n - 152*td + 22800*z - 123310 >= 0 and 4*td - 600
*z - 355 <= 0 and 4*td - 600*z + 3245 >= 0 and q - 40 <= 0 and q >= 0
and (80*i2 + 250*p1 + 2*q - 1057 > 0 and 80*i2 + 250*p1 + 2*q - 1377 <=
0 and 26640*i2 - 900*n + 83250*p1 + 666*q + 190*td - 1500*z - 2521 = 0
or 80*i2 + 250*p1 + 2*q - 1377 > 0 and 80*i2 + 250*p1 + 2*q - 1457 <= 0
and 691920*i2 - 18000*n + 2162250*p1 + 17298*q + 3800*td + 150000*z -
4405673 = 0 or 80*i2 + 250*p1 + 2*q - 1457 > 0 and 80*i2 + 250*p1 + 2*q
- 1697 < 0 and 96750000*i2 + 4500000*n + 302343750*p1 + 2418750*q -
950000*td - 15000000*z - 4024609231 = 0) and (2*p1 - 7 < 0 and 80*i2 +
250*p1 + 2*q - 577 = 0 or 2*p1 - 7 >= 0) or 400*q + 9*td - 20050 > 0 and
 i2 = 0 and n - td = 0 and 81*n - 152*td + 22800*z - 123310 >= 0 and 4*
td - 600*z - 355 <= 0 and 4*td - 600*z + 3245 >= 0 and q - 40 <= 0 and q
 >= 0 and 90*n - 19*td + 150*z - 45602 = 0 and 2*p1 - 7 >= 0 and 80*i2 +
 250*p1 + 2*q - 1377 = 0 and (td - 400 >= 0 and td - 700 < 0 and 3*td +
400*z - 5320 = 0 or td - 700 >= 0 and td - 990 < 0 and 2*td - 300*z +
1015 = 0 or td = 0 and z = 0) or 400*q + 9*td - 20050 > 0 and i2 = 0 and
 n - td = 0 and 81*n - 152*td + 22800*z - 123310 >= 0 and 4*td - 600*z -
 355 <= 0 and 4*td - 600*z + 3245 >= 0 and q - 40 <= 0 and q >= 0 and
450*n - 95*td - 3750*z - 204898 = 0 and 2*p1 - 7 >= 0 and 80*i2 + 250*p1
 + 2*q - 1457 = 0 and (td - 400 >= 0 and td - 700 < 0 and 3*td + 400*z -
 5320 = 0 or td - 700 >= 0 and td - 990 < 0 and 2*td - 300*z + 1015 = 0
or td = 0 and z = 0) or 400*q + 9*td - 20050 > 0 and i2 = 0 and n - td =
 0 and 81*n - 152*td + 22800*z - 123310 >= 0 and 4*td - 600*z - 355 <= 0
 and 4*td - 600*z + 3245 >= 0 and q - 40 <= 0 and q >= 0 and (80*i2 +
250*p1 + 2*q - 1057 > 0 and 80*i2 + 250*p1 + 2*q - 1377 <= 0 and 26640*
i2 - 900*n + 83250*p1 + 666*q + 190*td - 1500*z - 2521 = 0 or 80*i2 +
250*p1 + 2*q - 1377 > 0 and 80*i2 + 250*p1 + 2*q - 1457 <= 0 and 691920*
i2 - 18000*n + 2162250*p1 + 17298*q + 3800*td + 150000*z - 4405673 = 0
or 80*i2 + 250*p1 + 2*q - 1457 > 0 and 80*i2 + 250*p1 + 2*q - 1697 < 0
and 96750000*i2 + 4500000*n + 302343750*p1 + 2418750*q - 950000*td -
15000000*z - 4024609231 = 0) and (td - 400 >= 0 and td - 700 < 0 and 3*
td + 400*z - 5320 = 0 or td - 700 >= 0 and td - 990 < 0 and 2*td - 300*z
 + 1015 = 0 or td = 0 and z = 0) and (2*p1 - 7 < 0 and 80*i2 + 250*p1 +
2*q - 577 = 0 or 2*p1 - 7 >= 0) or 400*q + 9*td - 20050 <= 0 and td -
700 >= 0 and td - 990 < 0 and 200*i2 - 10*q - td + 385 = 0 and n - td =
0 and 81*n - 152*td + 22800*z - 123310 >= 0 and 4*td - 600*z - 355 <= 0
and 4*td - 600*z + 3245 >= 0 and q - 40 <= 0 and q >= 0 and 90*n - 19*td
 + 150*z - 45602 = 0 and 2*p1 - 7 >= 0 and 80*i2 + 250*p1 + 2*q - 1377 =
 0 or 400*q + 9*td - 20050 <= 0 and td - 700 >= 0 and td - 990 < 0 and
200*i2 - 10*q - td + 385 = 0 and n - td = 0 and 81*n - 152*td + 22800*z
- 123310 >= 0 and 4*td - 600*z - 355 <= 0 and 4*td - 600*z + 3245 >= 0
and q - 40 <= 0 and q >= 0 and 450*n - 95*td - 3750*z - 204898 = 0 and 2
*p1 - 7 >= 0 and 80*i2 + 250*p1 + 2*q - 1457 = 0 or 400*q + 9*td - 20050
 <= 0 and td - 700 >= 0 and td - 990 < 0 and 200*i2 - 10*q - td + 385 =
0 and n - td = 0 and 81*n - 152*td + 22800*z - 123310 >= 0 and 4*td -
600*z - 355 <= 0 and 4*td - 600*z + 3245 >= 0 and q - 40 <= 0 and q >= 0
 and (80*i2 + 250*p1 + 2*q - 1057 > 0 and 80*i2 + 250*p1 + 2*q - 1377 <=
 0 and 26640*i2 - 900*n + 83250*p1 + 666*q + 190*td - 1500*z - 2521 = 0
or 80*i2 + 250*p1 + 2*q - 1377 > 0 and 80*i2 + 250*p1 + 2*q - 1457 <= 0
and 691920*i2 - 18000*n + 2162250*p1 + 17298*q + 3800*td + 150000*z -
4405673 = 0 or 80*i2 + 250*p1 + 2*q - 1457 > 0 and 80*i2 + 250*p1 + 2*q
- 1697 < 0 and 96750000*i2 + 4500000*n + 302343750*p1 + 2418750*q -
950000*td - 15000000*z - 4024609231 = 0) and (2*p1 - 7 < 0 and 80*i2 +
250*p1 + 2*q - 577 = 0 or 2*p1 - 7 >= 0) or 400*q + 9*td - 20050 <= 0
and i2 = 0 and n - td = 0 and 81*n - 152*td + 22800*z - 123310 >= 0 and
4*td - 600*z - 355 <= 0 and 4*td - 600*z + 3245 >= 0 and q - 40 <= 0 and
 q >= 0 and 90*n - 19*td + 150*z - 45602 = 0 and 2*p1 - 7 >= 0 and 80*i2
 + 250*p1 + 2*q - 1377 = 0 and (td - 400 >= 0 and td - 700 < 0 and 3*td
+ 400*z - 5320 = 0 or td - 700 >= 0 and td - 990 < 0 and 2*td - 300*z +
1015 = 0 or td = 0 and z = 0) or 400*q + 9*td - 20050 <= 0 and i2 = 0
and n - td = 0 and 81*n - 152*td + 22800*z - 123310 >= 0 and 4*td - 600*
z - 355 <= 0 and 4*td - 600*z + 3245 >= 0 and q - 40 <= 0 and q >= 0 and
 450*n - 95*td - 3750*z - 204898 = 0 and 2*p1 - 7 >= 0 and 80*i2 + 250*
p1 + 2*q - 1457 = 0 and (td - 400 >= 0 and td - 700 < 0 and 3*td + 400*z
 - 5320 = 0 or td - 700 >= 0 and td - 990 < 0 and 2*td - 300*z + 1015 =
0 or td = 0 and z = 0) or 400*q + 9*td - 20050 <= 0 and i2 = 0 and n -
td = 0 and 81*n - 152*td + 22800*z - 123310 >= 0 and 4*td - 600*z - 355
<= 0 and 4*td - 600*z + 3245 >= 0 and q - 40 <= 0 and q >= 0 and (80*i2
+ 250*p1 + 2*q - 1057 > 0 and 80*i2 + 250*p1 + 2*q - 1377 <= 0 and 26640
*i2 - 900*n + 83250*p1 + 666*q + 190*td - 1500*z - 2521 = 0 or 80*i2 +
250*p1 + 2*q - 1377 > 0 and 80*i2 + 250*p1 + 2*q - 1457 <= 0 and 691920*
i2 - 18000*n + 2162250*p1 + 17298*q + 3800*td + 150000*z - 4405673 = 0
or 80*i2 + 250*p1 + 2*q - 1457 > 0 and 80*i2 + 250*p1 + 2*q - 1697 < 0
and 96750000*i2 + 4500000*n + 302343750*p1 + 2418750*q - 950000*td -
15000000*z - 4024609231 = 0) and (td - 400 >= 0 and td - 700 < 0 and 3*
td + 400*z - 5320 = 0 or td - 700 >= 0 and td - 990 < 0 and 2*td - 300*z
 + 1015 = 0 or td = 0 and z = 0) and (2*p1 - 7 < 0 and 80*i2 + 250*p1 +
2*q - 577 = 0 or 2*p1 - 7 >= 0) or 400*q + 9*td - 20050 > 0 and 200*i2 -
 10*q - td + 385 = 0 and n - td = 0 and n >= 0 and q - 40 <= 0 and q >=
0 and (20*n - 2*td - 300*z - 5963 > 0 and 20*n - 2*td - 300*z - 8331 <=
0 or 20*n - 2*td - 300*z - 8331 > 0 and 20*n - 2*td - 300*z - 8923 <= 0
and 4420*n - 442*td + 81700*z - 3170191 = 0 or 20*n - 2*td - 300*z -
8923 > 0 and 20*n - 2*td - 300*z - 10699 < 0 and 31937500*n - 3193750*td
 - 571562500*z - 13629165033 = 0) and (td - 400 >= 0 and td - 700 < 0
and 3*td + 400*z - 6130 = 0 or td - 700 >= 0 and td - 990 < 0 and 4*td -
 600*z + 3245 = 0) and (2*p1 - 7 < 0 and 20*n - 2*td - 300*z - 2411 = 0
or 2*p1 - 7 >= 0 and 1480*i2 - 50*n + 4625*p1 + 37*q + 5*td + 750*z -
4647 = 0) or 400*q + 9*td - 20050 > 0 and 200*i2 - 10*q - td + 385 = 0
and n - td = 0 and 715*n - 76*td - 11400*z - 316578 <= 0 and 20*n - 2*td
 - 300*z - 10331 <= 0 and 20*n - 2*td - 300*z - 8331 >= 0 and q - 40 <=
0 and q >= 0 and 2*p1 - 7 >= 0 and 80*i2 + 250*p1 + 2*q - 1377 = 0 and (
td - 400 >= 0 and td - 700 < 0 and 120*n + 3*td + 200*z - 80636 = 0 or
td - 700 >= 0 and td - 990 < 0 and 90*n - 19*td + 150*z - 45602 = 0) or
400*q + 9*td - 20050 > 0 and 200*i2 - 10*q - td + 385 = 0 and n - td = 0
 and 715*n - 76*td - 11400*z - 339074 <= 0 and 20*n - 2*td - 300*z -
10923 <= 0 and 20*n - 2*td - 300*z - 8923 >= 0 and q - 40 <= 0 and q >=
0 and 125*z - 1012 = 0 and 2*p1 - 7 >= 0 and 80*i2 + 250*p1 + 2*q - 1457
 = 0 and (td - 400 >= 0 and td - 700 < 0 and 120*n + 3*td + 200*z -
84188 = 0 or td - 700 >= 0 and td - 990 < 0 and 90*n - 19*td + 150*z -
48266 = 0) or 400*q + 9*td - 20050 > 0 and 200*i2 - 10*q - td + 385 = 0
and n - td = 0 and 27*n + 57*td + 7600*z - 116470 >= 0 and 3*td + 400*z
- 3730 >= 0 and 3*td + 400*z - 6130 <= 0 and q - 40 <= 0 and q >= 0 and
(120*n + 3*td + 200*z - 66428 > 0 and 120*n + 3*td + 200*z - 80636 <= 0
or 120*n + 3*td + 200*z - 80636 > 0 and 120*n + 3*td + 200*z - 84188 <=
0 and 26520*n + 663*td + 932200*z - 25794796 = 0 or 120*n + 3*td + 200*z
 - 84188 > 0 and 120*n + 3*td + 200*z - 94844 < 0 and 191625000*n +
4790625*td - 235625000*z - 130719208948 = 0) and (td - 400 >= 0 and td -
 700 < 0 or td - 990 < 0 and td - 700 = 0) and (2*p1 - 7 < 0 and 120*n +
 3*td + 200*z - 45116 = 0 or 2*p1 - 7 >= 0 and 17760*i2 - 600*n + 55500*
p1 + 444*q - 15*td - 1000*z + 97486 = 0) or 400*q + 9*td - 20050 > 0 and
 200*i2 - 10*q - td + 385 = 0 and n - td = 0 and 81*n - 152*td + 22800*z
 - 123310 >= 0 and 4*td - 600*z - 355 <= 0 and 4*td - 600*z + 3245 >= 0
and q - 40 <= 0 and q >= 0 and td - 700 >= 0 and td - 990 < 0 and (90*n
- 19*td + 150*z - 34946 > 0 and 90*n - 19*td + 150*z - 45602 <= 0 or 90*
n - 19*td + 150*z - 45602 > 0 and 90*n - 19*td + 150*z - 48266 <= 0 and
19890*n - 4199*td + 699150*z - 16058722 = 0 or 90*n - 19*td + 150*z -
48266 > 0 and 90*n - 19*td + 150*z - 56258 < 0 and 143718750*n -
30340625*td - 176718750*z - 74285891086 = 0) and (2*p1 - 7 < 0 and 90*n
- 19*td + 150*z - 18962 = 0 or 2*p1 - 7 >= 0 and 26640*i2 - 900*n +
83250*p1 + 666*q + 190*td - 1500*z - 2521 = 0) or 400*q + 9*td - 20050 >
 0 and 200*i2 - 10*q - td + 385 = 0 and n - td = 0 and 112480*i2 - 3575*
n + 351500*p1 + 2812*q + 380*td + 57000*z - 353172 >= 0 and 1480*i2 - 50
*n + 4625*p1 + 37*q + 5*td + 750*z + 353 >= 0 and 1480*i2 - 50*n + 4625*
p1 + 37*q + 5*td + 750*z - 4647 <= 0 and q - 40 <= 0 and q >= 0 and (80*
i2 + 250*p1 + 2*q - 1057 > 0 and 80*i2 + 250*p1 + 2*q - 1377 <= 0 or 80*
i2 + 250*p1 + 2*q - 1377 > 0 and 80*i2 + 250*p1 + 2*q - 1457 <= 0 and
17680*i2 + 55250*p1 + 442*q + 20000*z - 483917 = 0 or 80*i2 + 250*p1 + 2
*q - 1457 > 0 and 80*i2 + 250*p1 + 2*q - 1697 < 0 and 25550000*i2 +
79843750*p1 + 638750*q - 2500000*z - 448579359 = 0) and (td - 400 >= 0
and td - 700 < 0 and 17760*i2 - 600*n + 55500*p1 + 444*q - 15*td - 1000*
z + 97486 = 0 or td - 700 >= 0 and td - 990 < 0 and 26640*i2 - 900*n +
83250*p1 + 666*q + 190*td - 1500*z - 2521 = 0) and (2*p1 - 7 < 0 and 80*
i2 + 250*p1 + 2*q - 577 = 0 or 2*p1 - 7 >= 0) or 400*q + 9*td - 20050 >
0 and i2 = 0 and n - td = 0 and n >= 0 and q - 40 <= 0 and q >= 0 and (
20*n - 2*td - 300*z - 5963 > 0 and 20*n - 2*td - 300*z - 8331 <= 0 or 20
*n - 2*td - 300*z - 8331 > 0 and 20*n - 2*td - 300*z - 8923 <= 0 and
4420*n - 442*td + 81700*z - 3170191 = 0 or 20*n - 2*td - 300*z - 8923 >
0 and 20*n - 2*td - 300*z - 10699 < 0 and 31937500*n - 3193750*td -
571562500*z - 13629165033 = 0) and (td - 400 >= 0 and td - 700 < 0 and 3
*td + 400*z - 5320 = 0 or td - 700 >= 0 and td - 990 < 0 and 2*td - 300*
z + 1015 = 0 or td = 0 and z = 0) and (2*p1 - 7 < 0 and 20*n - 2*td -
300*z - 2411 = 0 or 2*p1 - 7 >= 0 and 1480*i2 - 50*n + 4625*p1 + 37*q +
5*td + 750*z - 4647 = 0) or 400*q + 9*td - 20050 > 0 and i2 = 0 and n -
td = 0 and 715*n - 76*td - 11400*z - 316578 <= 0 and 20*n - 2*td - 300*z
 - 10331 <= 0 and 20*n - 2*td - 300*z - 8331 >= 0 and q - 40 <= 0 and q
>= 0 and 2*p1 - 7 >= 0 and 80*i2 + 250*p1 + 2*q - 1377 = 0 and (td - 400
 >= 0 and td - 700 < 0 and 3*td + 400*z - 5320 = 0 or td - 700 >= 0 and
td - 990 < 0 and 2*td - 300*z + 1015 = 0 or td = 0 and z = 0) or 400*q +
 9*td - 20050 > 0 and i2 = 0 and n - td = 0 and 715*n - 76*td - 11400*z
- 339074 <= 0 and 20*n - 2*td - 300*z - 10923 <= 0 and 20*n - 2*td - 300
*z - 8923 >= 0 and q - 40 <= 0 and q >= 0 and 125*z - 1012 = 0 and 2*p1
- 7 >= 0 and 80*i2 + 250*p1 + 2*q - 1457 = 0 and (td - 400 >= 0 and td -
 700 < 0 and 3*td + 400*z - 5320 = 0 or td - 700 >= 0 and td - 990 < 0
and 2*td - 300*z + 1015 = 0 or td = 0 and z = 0) or 400*q + 9*td - 20050
 > 0 and i2 = 0 and n - td = 0 and 112480*i2 - 3575*n + 351500*p1 + 2812
*q + 380*td + 57000*z - 353172 >= 0 and 1480*i2 - 50*n + 4625*p1 + 37*q
+ 5*td + 750*z + 353 >= 0 and 1480*i2 - 50*n + 4625*p1 + 37*q + 5*td +
750*z - 4647 <= 0 and q - 40 <= 0 and q >= 0 and (80*i2 + 250*p1 + 2*q -
 1057 > 0 and 80*i2 + 250*p1 + 2*q - 1377 <= 0 or 80*i2 + 250*p1 + 2*q -
 1377 > 0 and 80*i2 + 250*p1 + 2*q - 1457 <= 0 and 17680*i2 + 55250*p1 +
 442*q + 20000*z - 483917 = 0 or 80*i2 + 250*p1 + 2*q - 1457 > 0 and 80*
i2 + 250*p1 + 2*q - 1697 < 0 and 25550000*i2 + 79843750*p1 + 638750*q -
2500000*z - 448579359 = 0) and (td - 400 >= 0 and td - 700 < 0 and 3*td
+ 400*z - 5320 = 0 or td - 700 >= 0 and td - 990 < 0 and 2*td - 300*z +
1015 = 0 or td = 0 and z = 0) and (2*p1 - 7 < 0 and 80*i2 + 250*p1 + 2*q
 - 577 = 0 or 2*p1 - 7 >= 0) or 400*q + 9*td - 20050 <= 0 and 200*i2 -
10*q - td + 385 = 0 and n - td = 0 and n >= 0 and q - 40 <= 0 and q >= 0
 and (20*n - 2*td - 300*z - 5963 > 0 and 20*n - 2*td - 300*z - 8331 <= 0
 or 20*n - 2*td - 300*z - 8331 > 0 and 20*n - 2*td - 300*z - 8923 <= 0
and 4420*n - 442*td + 81700*z - 3170191 = 0 or 20*n - 2*td - 300*z -
8923 > 0 and 20*n - 2*td - 300*z - 10699 < 0 and 31937500*n - 3193750*td
 - 571562500*z - 13629165033 = 0) and (td - 400 >= 0 and td - 700 < 0
and 3*td + 400*z - 6130 = 0 or td - 700 >= 0 and td - 990 < 0 and 4*td -
 600*z + 3245 = 0) and (2*p1 - 7 < 0 and 20*n - 2*td - 300*z - 2411 = 0
or 2*p1 - 7 >= 0 and 1480*i2 - 50*n + 4625*p1 + 37*q + 5*td + 750*z -
4647 = 0) or 400*q + 9*td - 20050 <= 0 and 200*i2 - 10*q - td + 385 = 0
and n - td = 0 and 715*n - 76*td - 11400*z - 316578 <= 0 and 20*n - 2*td
 - 300*z - 10331 <= 0 and 20*n - 2*td - 300*z - 8331 >= 0 and q - 40 <=
0 and q >= 0 and 2*p1 - 7 >= 0 and 80*i2 + 250*p1 + 2*q - 1377 = 0 and (
td - 400 >= 0 and td - 700 < 0 and 120*n + 3*td + 200*z - 80636 = 0 or
td - 700 >= 0 and td - 990 < 0 and 90*n - 19*td + 150*z - 45602 = 0) or
400*q + 9*td - 20050 <= 0 and 200*i2 - 10*q - td + 385 = 0 and n - td =
0 and 715*n - 76*td - 11400*z - 339074 <= 0 and 20*n - 2*td - 300*z -
10923 <= 0 and 20*n - 2*td - 300*z - 8923 >= 0 and q - 40 <= 0 and q >=
0 and 125*z - 1012 = 0 and 2*p1 - 7 >= 0 and 80*i2 + 250*p1 + 2*q - 1457
 = 0 and (td - 400 >= 0 and td - 700 < 0 and 120*n + 3*td + 200*z -
84188 = 0 or td - 700 >= 0 and td - 990 < 0 and 90*n - 19*td + 150*z -
48266 = 0) or 400*q + 9*td - 20050 <= 0 and 200*i2 - 10*q - td + 385 = 0
 and n - td = 0 and 27*n + 57*td + 7600*z - 116470 >= 0 and 3*td + 400*z
 - 3730 >= 0 and 3*td + 400*z - 6130 <= 0 and q - 40 <= 0 and q >= 0 and
 (120*n + 3*td + 200*z - 66428 > 0 and 120*n + 3*td + 200*z - 80636 <= 0
 or 120*n + 3*td + 200*z - 80636 > 0 and 120*n + 3*td + 200*z - 84188 <=
 0 and 26520*n + 663*td + 932200*z - 25794796 = 0 or 120*n + 3*td + 200*
z - 84188 > 0 and 120*n + 3*td + 200*z - 94844 < 0 and 191625000*n +
4790625*td - 235625000*z - 130719208948 = 0) and (td - 400 >= 0 and td -
 700 < 0 or td - 990 < 0 and td - 700 = 0) and (2*p1 - 7 < 0 and 120*n +
 3*td + 200*z - 45116 = 0 or 2*p1 - 7 >= 0 and 17760*i2 - 600*n + 55500*
p1 + 444*q - 15*td - 1000*z + 97486 = 0) or 400*q + 9*td - 20050 <= 0
and 200*i2 - 10*q - td + 385 = 0 and n - td = 0 and 81*n - 152*td +
22800*z - 123310 >= 0 and 4*td - 600*z - 355 <= 0 and 4*td - 600*z +
3245 >= 0 and q - 40 <= 0 and q >= 0 and td - 700 >= 0 and td - 990 < 0
and (90*n - 19*td + 150*z - 34946 > 0 and 90*n - 19*td + 150*z - 45602
<= 0 or 90*n - 19*td + 150*z - 45602 > 0 and 90*n - 19*td + 150*z -
48266 <= 0 and 19890*n - 4199*td + 699150*z - 16058722 = 0 or 90*n - 19*
td + 150*z - 48266 > 0 and 90*n - 19*td + 150*z - 56258 < 0 and
143718750*n - 30340625*td - 176718750*z - 74285891086 = 0) and (2*p1 - 7
 < 0 and 90*n - 19*td + 150*z - 18962 = 0 or 2*p1 - 7 >= 0 and 26640*i2
- 900*n + 83250*p1 + 666*q + 190*td - 1500*z - 2521 = 0) or 400*q + 9*td
 - 20050 <= 0 and 200*i2 - 10*q - td + 385 = 0 and n - td = 0 and 112480
*i2 - 3575*n + 351500*p1 + 2812*q + 380*td + 57000*z - 353172 >= 0 and
1480*i2 - 50*n + 4625*p1 + 37*q + 5*td + 750*z + 353 >= 0 and 1480*i2 -
50*n + 4625*p1 + 37*q + 5*td + 750*z - 4647 <= 0 and q - 40 <= 0 and q
>= 0 and (80*i2 + 250*p1 + 2*q - 1057 > 0 and 80*i2 + 250*p1 + 2*q -
1377 <= 0 or 80*i2 + 250*p1 + 2*q - 1377 > 0 and 80*i2 + 250*p1 + 2*q -
1457 <= 0 and 17680*i2 + 55250*p1 + 442*q + 20000*z - 483917 = 0 or 80*
i2 + 250*p1 + 2*q - 1457 > 0 and 80*i2 + 250*p1 + 2*q - 1697 < 0 and
25550000*i2 + 79843750*p1 + 638750*q - 2500000*z - 448579359 = 0) and (
td - 400 >= 0 and td - 700 < 0 and 17760*i2 - 600*n + 55500*p1 + 444*q -
 15*td - 1000*z + 97486 = 0 or td - 700 >= 0 and td - 990 < 0 and 26640*
i2 - 900*n + 83250*p1 + 666*q + 190*td - 1500*z - 2521 = 0) and (2*p1 -
7 < 0 and 80*i2 + 250*p1 + 2*q - 577 = 0 or 2*p1 - 7 >= 0) or 400*q + 9*
td - 20050 <= 0 and i2 = 0 and n - td = 0 and n >= 0 and q - 40 <= 0 and
 q >= 0 and (20*n - 2*td - 300*z - 5963 > 0 and 20*n - 2*td - 300*z -
8331 <= 0 or 20*n - 2*td - 300*z - 8331 > 0 and 20*n - 2*td - 300*z -
8923 <= 0 and 4420*n - 442*td + 81700*z - 3170191 = 0 or 20*n - 2*td -
300*z - 8923 > 0 and 20*n - 2*td - 300*z - 10699 < 0 and 31937500*n -
3193750*td - 571562500*z - 13629165033 = 0) and (td - 400 >= 0 and td -
700 < 0 and 3*td + 400*z - 5320 = 0 or td - 700 >= 0 and td - 990 < 0
and 2*td - 300*z + 1015 = 0 or td = 0 and z = 0) and (2*p1 - 7 < 0 and
20*n - 2*td - 300*z - 2411 = 0 or 2*p1 - 7 >= 0 and 1480*i2 - 50*n +
4625*p1 + 37*q + 5*td + 750*z - 4647 = 0) or 400*q + 9*td - 20050 <= 0
and i2 = 0 and n - td = 0 and 715*n - 76*td - 11400*z - 316578 <= 0 and
20*n - 2*td - 300*z - 10331 <= 0 and 20*n - 2*td - 300*z - 8331 >= 0 and
 q - 40 <= 0 and q >= 0 and 2*p1 - 7 >= 0 and 80*i2 + 250*p1 + 2*q -
1377 = 0 and (td - 400 >= 0 and td - 700 < 0 and 3*td + 400*z - 5320 = 0
 or td - 700 >= 0 and td - 990 < 0 and 2*td - 300*z + 1015 = 0 or td = 0
 and z = 0) or 400*q + 9*td - 20050 <= 0 and i2 = 0 and n - td = 0 and
715*n - 76*td - 11400*z - 339074 <= 0 and 20*n - 2*td - 300*z - 10923 <=
 0 and 20*n - 2*td - 300*z - 8923 >= 0 and q - 40 <= 0 and q >= 0 and
125*z - 1012 = 0 and 2*p1 - 7 >= 0 and 80*i2 + 250*p1 + 2*q - 1457 = 0
and (td - 400 >= 0 and td - 700 < 0 and 3*td + 400*z - 5320 = 0 or td -
700 >= 0 and td - 990 < 0 and 2*td - 300*z + 1015 = 0 or td = 0 and z =
0) or 400*q + 9*td - 20050 <= 0 and i2 = 0 and n - td = 0 and 112480*i2
- 3575*n + 351500*p1 + 2812*q + 380*td + 57000*z - 353172 >= 0 and 1480*
i2 - 50*n + 4625*p1 + 37*q + 5*td + 750*z + 353 >= 0 and 1480*i2 - 50*n
+ 4625*p1 + 37*q + 5*td + 750*z - 4647 <= 0 and q - 40 <= 0 and q >= 0
and (80*i2 + 250*p1 + 2*q - 1057 > 0 and 80*i2 + 250*p1 + 2*q - 1377 <=
0 or 80*i2 + 250*p1 + 2*q - 1377 > 0 and 80*i2 + 250*p1 + 2*q - 1457 <=
0 and 17680*i2 + 55250*p1 + 442*q + 20000*z - 483917 = 0 or 80*i2 + 250*
p1 + 2*q - 1457 > 0 and 80*i2 + 250*p1 + 2*q - 1697 < 0 and 25550000*i2
+ 79843750*p1 + 638750*q - 2500000*z - 448579359 = 0) and (td - 400 >= 0
 and td - 700 < 0 and 3*td + 400*z - 5320 = 0 or td - 700 >= 0 and td -
990 < 0 and 2*td - 300*z + 1015 = 0 or td = 0 and z = 0) and (2*p1 - 7 <
 0 and 80*i2 + 250*p1 + 2*q - 577 = 0 or 2*p1 - 7 >= 0) or 400*q + 9*td
- 20050 > 0 and 200*i2 - 10*q - td + 385 = 0 and n - td = 0 and n >= 0
and q - 40 <= 0 and q >= 0 and (100*n - 10*td - 2500*z - 17299 > 0 and
20*n - 2*td - 500*z - 6535 <= 0 and 4420*n - 442*td + 81700*z - 3170191
= 0 or 20*n - 2*td - 500*z - 6535 > 0 and 100*n - 10*td - 2500*z - 36519
 <= 0 or 100*n - 10*td - 2500*z - 36519 > 0 and 100*n - 10*td - 2500*z -
 48051 < 0 and 187312500*n - 18731250*td - 4082187500*z - 74105780531 =
0) and (td - 400 >= 0 and td - 700 < 0 and 3*td + 400*z - 6130 = 0 or td
 - 700 >= 0 and td - 990 < 0 and 4*td - 600*z + 3245 = 0) and (2*p1 - 7
< 0 and 20*n - 2*td - 500*z + 1153 = 0 or 2*p1 - 7 >= 0 and 76880*i2 -
2000*n + 240250*p1 + 1922*q + 200*td + 50000*z - 669797 = 0) or 400*q +
9*td - 20050 > 0 and 200*i2 - 10*q - td + 385 = 0 and n - td = 0 and 715
*n - 76*td - 19000*z - 248330 <= 0 and 20*n - 2*td - 500*z - 8535 <= 0
and 20*n - 2*td - 500*z - 6535 >= 0 and q - 40 <= 0 and q >= 0 and 50*z
- 449 = 0 and 2*p1 - 7 >= 0 and 80*i2 + 250*p1 + 2*q - 1377 = 0 and (td
- 400 >= 0 and td - 700 < 0 and 120*n + 3*td - 1000*z - 69860 = 0 or td
- 700 >= 0 and td - 990 < 0 and 90*n - 19*td - 750*z - 37520 = 0) or 400
*q + 9*td - 20050 > 0 and 200*i2 - 10*q - td + 385 = 0 and n - td = 0
and 158015*n - 16796*td + 3104600*z - 120467258 <= 0 and 4420*n - 442*td
 + 81700*z - 3612191 <= 0 and 4420*n - 442*td + 81700*z - 3170191 >= 0
and q - 40 <= 0 and q >= 0 and (250*z - 3129 < 0 and 50*z - 449 >= 0 or
50*z - 449 < 0 and 125*z - 1012 >= 0 or 125*z - 1012 < 0 and 250*z -
1361 > 0 and 108437500*z - 865858649 = 0) and (td - 400 >= 0 and td -
700 < 0 and 26520*n + 663*td + 932200*z - 25794796 = 0 or td - 700 >= 0
and td - 990 < 0 and 19890*n - 4199*td + 699150*z - 16058722 = 0) and (2
*p1 - 7 < 0 and 50*z - 891 = 0 or 2*p1 - 7 >= 0 and 17680*i2 + 55250*p1
+ 442*q + 20000*z - 483917 = 0) or 400*q + 9*td - 20050 > 0 and 200*i2 -
 10*q - td + 385 = 0 and n - td = 0 and 3575*n - 380*td - 95000*z -
1387722 <= 0 and 100*n - 10*td - 2500*z - 46519 <= 0 and 100*n - 10*td -
 2500*z - 36519 >= 0 and q - 40 <= 0 and q >= 0 and 2*p1 - 7 >= 0 and 80
*i2 + 250*p1 + 2*q - 1457 = 0 and (td - 400 >= 0 and td - 700 < 0 and
600*n + 15*td - 5000*z - 372364 = 0 or td - 700 >= 0 and td - 990 < 0
and 450*n - 95*td - 3750*z - 204898 = 0) or 400*q + 9*td - 20050 > 0 and
 200*i2 - 10*q - td + 385 = 0 and n - td = 0 and 27*n + 57*td + 7600*z -
 116470 >= 0 and 3*td + 400*z - 3730 >= 0 and 3*td + 400*z - 6130 <= 0
and q - 40 <= 0 and q >= 0 and (600*n + 15*td - 5000*z - 257044 > 0 and
120*n + 3*td - 1000*z - 69860 <= 0 and 26520*n + 663*td + 932200*z -
25794796 = 0 or 120*n + 3*td - 1000*z - 69860 > 0 and 600*n + 15*td -
5000*z - 372364 <= 0 or 600*n + 15*td - 5000*z - 372364 > 0 and 600*n +
15*td - 5000*z - 441556 < 0 and 374625000*n + 9365625*td - 1920625000*z
- 243897029812 = 0) and (td - 400 >= 0 and td - 700 < 0 or td - 990 < 0
and td - 700 = 0) and (2*p1 - 7 < 0 and 120*n + 3*td - 1000*z - 23732 =
0 or 2*p1 - 7 >= 0 and 230640*i2 - 6000*n + 720750*p1 + 5766*q - 150*td
+ 50000*z - 476891 = 0) or 400*q + 9*td - 20050 > 0 and 200*i2 - 10*q -
td + 385 = 0 and n - td = 0 and 81*n - 152*td + 22800*z - 123310 >= 0
and 4*td - 600*z - 355 <= 0 and 4*td - 600*z + 3245 >= 0 and q - 40 <= 0
 and q >= 0 and td - 700 >= 0 and td - 990 < 0 and (450*n - 95*td - 3750
*z - 118408 > 0 and 90*n - 19*td - 750*z - 37520 <= 0 and 19890*n - 4199
*td + 699150*z - 16058722 = 0 or 90*n - 19*td - 750*z - 37520 > 0 and
450*n - 95*td - 3750*z - 204898 <= 0 or 450*n - 95*td - 3750*z - 204898
> 0 and 450*n - 95*td - 3750*z - 256792 < 0 and 93656250*n - 19771875*td
 - 480156250*z - 45494960578 = 0) and (2*p1 - 7 < 0 and 90*n - 19*td -
750*z - 2924 = 0 or 2*p1 - 7 >= 0 and 691920*i2 - 18000*n + 2162250*p1 +
 17298*q + 3800*td + 150000*z - 4405673 = 0) or 400*q + 9*td - 20050 > 0
 and 200*i2 - 10*q - td + 385 = 0 and n - td = 0 and 1460720*i2 - 35750*
n + 4564750*p1 + 36518*q + 3800*td + 950000*z - 12726143 >= 0 and 76880*
i2 - 2000*n + 240250*p1 + 1922*q + 200*td + 50000*z - 469797 >= 0 and
76880*i2 - 2000*n + 240250*p1 + 1922*q + 200*td + 50000*z - 669797 <= 0
and q - 40 <= 0 and q >= 0 and (80*i2 + 250*p1 + 2*q - 1057 > 0 and 80*
i2 + 250*p1 + 2*q - 1377 <= 0 and 17680*i2 + 55250*p1 + 442*q + 20000*z
- 483917 = 0 or 80*i2 + 250*p1 + 2*q - 1377 > 0 and 80*i2 + 250*p1 + 2*q
 - 1457 <= 0 or 80*i2 + 250*p1 + 2*q - 1457 > 0 and 80*i2 + 250*p1 + 2*q
 - 1697 < 0 and 29970000*i2 + 93656250*p1 + 749250*q + 2500000*z -
569558609 = 0) and (td - 400 >= 0 and td - 700 < 0 and 230640*i2 - 6000*
n + 720750*p1 + 5766*q - 150*td + 50000*z - 476891 = 0 or td - 700 >= 0
and td - 990 < 0 and 691920*i2 - 18000*n + 2162250*p1 + 17298*q + 3800*
td + 150000*z - 4405673 = 0) and (2*p1 - 7 < 0 and 80*i2 + 250*p1 + 2*q
- 577 = 0 or 2*p1 - 7 >= 0) or 400*q + 9*td - 20050 > 0 and i2 = 0 and n
 - td = 0 and n >= 0 and q - 40 <= 0 and q >= 0 and (100*n - 10*td -
2500*z - 17299 > 0 and 20*n - 2*td - 500*z - 6535 <= 0 and 4420*n - 442*
td + 81700*z - 3170191 = 0 or 20*n - 2*td - 500*z - 6535 > 0 and 100*n -
 10*td - 2500*z - 36519 <= 0 or 100*n - 10*td - 2500*z - 36519 > 0 and
100*n - 10*td - 2500*z - 48051 < 0 and 187312500*n - 18731250*td - 4082187500
*z - 74105780531 = 0) and (td - 400 >= 0 and td - 700 < 0 and 3*td + 400
*z - 5320 = 0 or td - 700 >= 0 and td - 990 < 0 and 2*td - 300*z + 1015
= 0 or td = 0 and z = 0) and (2*p1 - 7 < 0 and 20*n - 2*td - 500*z +
1153 = 0 or 2*p1 - 7 >= 0 and 76880*i2 - 2000*n + 240250*p1 + 1922*q +
200*td + 50000*z - 669797 = 0) or 400*q + 9*td - 20050 > 0 and i2 = 0
and n - td = 0 and 715*n - 76*td - 19000*z - 248330 <= 0 and 20*n - 2*td
 - 500*z - 8535 <= 0 and 20*n - 2*td - 500*z - 6535 >= 0 and q - 40 <= 0
 and q >= 0 and 50*z - 449 = 0 and 2*p1 - 7 >= 0 and 80*i2 + 250*p1 + 2*
q - 1377 = 0 and (td - 400 >= 0 and td - 700 < 0 and 3*td + 400*z - 5320
 = 0 or td - 700 >= 0 and td - 990 < 0 and 2*td - 300*z + 1015 = 0 or td
 = 0 and z = 0) or 400*q + 9*td - 20050 > 0 and i2 = 0 and n - td = 0
and 158015*n - 16796*td + 3104600*z - 120467258 <= 0 and 4420*n - 442*td
 + 81700*z - 3612191 <= 0 and 4420*n - 442*td + 81700*z - 3170191 >= 0
and q - 40 <= 0 and q >= 0 and (250*z - 3129 < 0 and 50*z - 449 >= 0 or
50*z - 449 < 0 and 125*z - 1012 >= 0 or 125*z - 1012 < 0 and 250*z -
1361 > 0 and 108437500*z - 865858649 = 0) and (td - 400 >= 0 and td -
700 < 0 and 3*td + 400*z - 5320 = 0 or td - 700 >= 0 and td - 990 < 0
and 2*td - 300*z + 1015 = 0 or td = 0 and z = 0) and (2*p1 - 7 < 0 and
50*z - 891 = 0 or 2*p1 - 7 >= 0 and 17680*i2 + 55250*p1 + 442*q + 20000*
z - 483917 = 0) or 400*q + 9*td - 20050 > 0 and i2 = 0 and n - td = 0
and 3575*n - 380*td - 95000*z - 1387722 <= 0 and 100*n - 10*td - 2500*z
- 46519 <= 0 and 100*n - 10*td - 2500*z - 36519 >= 0 and q - 40 <= 0 and
 q >= 0 and 2*p1 - 7 >= 0 and 80*i2 + 250*p1 + 2*q - 1457 = 0 and (td -
400 >= 0 and td - 700 < 0 and 3*td + 400*z - 5320 = 0 or td - 700 >= 0
and td - 990 < 0 and 2*td - 300*z + 1015 = 0 or td = 0 and z = 0) or 400
*q + 9*td - 20050 > 0 and i2 = 0 and n - td = 0 and 1460720*i2 - 35750*n
 + 4564750*p1 + 36518*q + 3800*td + 950000*z - 12726143 >= 0 and 76880*
i2 - 2000*n + 240250*p1 + 1922*q + 200*td + 50000*z - 469797 >= 0 and
76880*i2 - 2000*n + 240250*p1 + 1922*q + 200*td + 50000*z - 669797 <= 0
and q - 40 <= 0 and q >= 0 and (80*i2 + 250*p1 + 2*q - 1057 > 0 and 80*
i2 + 250*p1 + 2*q - 1377 <= 0 and 17680*i2 + 55250*p1 + 442*q + 20000*z
- 483917 = 0 or 80*i2 + 250*p1 + 2*q - 1377 > 0 and 80*i2 + 250*p1 + 2*q
 - 1457 <= 0 or 80*i2 + 250*p1 + 2*q - 1457 > 0 and 80*i2 + 250*p1 + 2*q
 - 1697 < 0 and 29970000*i2 + 93656250*p1 + 749250*q + 2500000*z -
569558609 = 0) and (td - 400 >= 0 and td - 700 < 0 and 3*td + 400*z -
5320 = 0 or td - 700 >= 0 and td - 990 < 0 and 2*td - 300*z + 1015 = 0
or td = 0 and z = 0) and (2*p1 - 7 < 0 and 80*i2 + 250*p1 + 2*q - 577 =
0 or 2*p1 - 7 >= 0) or 400*q + 9*td - 20050 <= 0 and 200*i2 - 10*q - td
+ 385 = 0 and n - td = 0 and n >= 0 and q - 40 <= 0 and q >= 0 and (100*
n - 10*td - 2500*z - 17299 > 0 and 20*n - 2*td - 500*z - 6535 <= 0 and
4420*n - 442*td + 81700*z - 3170191 = 0 or 20*n - 2*td - 500*z - 6535 >
0 and 100*n - 10*td - 2500*z - 36519 <= 0 or 100*n - 10*td - 2500*z -
36519 > 0 and 100*n - 10*td - 2500*z - 48051 < 0 and 187312500*n -
18731250*td - 4082187500*z - 74105780531 = 0) and (td - 400 >= 0 and td
- 700 < 0 and 3*td + 400*z - 6130 = 0 or td - 700 >= 0 and td - 990 < 0
and 4*td - 600*z + 3245 = 0) and (2*p1 - 7 < 0 and 20*n - 2*td - 500*z +
 1153 = 0 or 2*p1 - 7 >= 0 and 76880*i2 - 2000*n + 240250*p1 + 1922*q +
200*td + 50000*z - 669797 = 0) or 400*q + 9*td - 20050 <= 0 and 200*i2 -
 10*q - td + 385 = 0 and n - td = 0 and 715*n - 76*td - 19000*z - 248330
 <= 0 and 20*n - 2*td - 500*z - 8535 <= 0 and 20*n - 2*td - 500*z - 6535
 >= 0 and q - 40 <= 0 and q >= 0 and 50*z - 449 = 0 and 2*p1 - 7 >= 0
and 80*i2 + 250*p1 + 2*q - 1377 = 0 and (td - 400 >= 0 and td - 700 < 0
and 120*n + 3*td - 1000*z - 69860 = 0 or td - 700 >= 0 and td - 990 < 0
and 90*n - 19*td - 750*z - 37520 = 0) or 400*q + 9*td - 20050 <= 0 and
200*i2 - 10*q - td + 385 = 0 and n - td = 0 and 158015*n - 16796*td +
3104600*z - 120467258 <= 0 and 4420*n - 442*td + 81700*z - 3612191 <= 0
and 4420*n - 442*td + 81700*z - 3170191 >= 0 and q - 40 <= 0 and q >= 0
and (250*z - 3129 < 0 and 50*z - 449 >= 0 or 50*z - 449 < 0 and 125*z -
1012 >= 0 or 125*z - 1012 < 0 and 250*z - 1361 > 0 and 108437500*z -
865858649 = 0) and (td - 400 >= 0 and td - 700 < 0 and 26520*n + 663*td
+ 932200*z - 25794796 = 0 or td - 700 >= 0 and td - 990 < 0 and 19890*n
- 4199*td + 699150*z - 16058722 = 0) and (2*p1 - 7 < 0 and 50*z - 891 =
0 or 2*p1 - 7 >= 0 and 17680*i2 + 55250*p1 + 442*q + 20000*z - 483917 =
0) or 400*q + 9*td - 20050 <= 0 and 200*i2 - 10*q - td + 385 = 0 and n -
 td = 0 and 3575*n - 380*td - 95000*z - 1387722 <= 0 and 100*n - 10*td -
 2500*z - 46519 <= 0 and 100*n - 10*td - 2500*z - 36519 >= 0 and q - 40
<= 0 and q >= 0 and 2*p1 - 7 >= 0 and 80*i2 + 250*p1 + 2*q - 1457 = 0
and (td - 400 >= 0 and td - 700 < 0 and 600*n + 15*td - 5000*z - 372364
= 0 or td - 700 >= 0 and td - 990 < 0 and 450*n - 95*td - 3750*z -
204898 = 0) or 400*q + 9*td - 20050 <= 0 and 200*i2 - 10*q - td + 385 =
0 and n - td = 0 and 27*n + 57*td + 7600*z - 116470 >= 0 and 3*td + 400*
z - 3730 >= 0 and 3*td + 400*z - 6130 <= 0 and q - 40 <= 0 and q >= 0
and (600*n + 15*td - 5000*z - 257044 > 0 and 120*n + 3*td - 1000*z -
69860 <= 0 and 26520*n + 663*td + 932200*z - 25794796 = 0 or 120*n + 3*
td - 1000*z - 69860 > 0 and 600*n + 15*td - 5000*z - 372364 <= 0 or 600*
n + 15*td - 5000*z - 372364 > 0 and 600*n + 15*td - 5000*z - 441556 < 0
and 374625000*n + 9365625*td - 1920625000*z - 243897029812 = 0) and (td
- 400 >= 0 and td - 700 < 0 or td - 990 < 0 and td - 700 = 0) and (2*p1
- 7 < 0 and 120*n + 3*td - 1000*z - 23732 = 0 or 2*p1 - 7 >= 0 and
230640*i2 - 6000*n + 720750*p1 + 5766*q - 150*td + 50000*z - 476891 = 0)
 or 400*q + 9*td - 20050 <= 0 and 200*i2 - 10*q - td + 385 = 0 and n -
td = 0 and 81*n - 152*td + 22800*z - 123310 >= 0 and 4*td - 600*z - 355
<= 0 and 4*td - 600*z + 3245 >= 0 and q - 40 <= 0 and q >= 0 and td -
700 >= 0 and td - 990 < 0 and (450*n - 95*td - 3750*z - 118408 > 0 and
90*n - 19*td - 750*z - 37520 <= 0 and 19890*n - 4199*td + 699150*z -
16058722 = 0 or 90*n - 19*td - 750*z - 37520 > 0 and 450*n - 95*td -
3750*z - 204898 <= 0 or 450*n - 95*td - 3750*z - 204898 > 0 and 450*n -
95*td - 3750*z - 256792 < 0 and 93656250*n - 19771875*td - 480156250*z -
 45494960578 = 0) and (2*p1 - 7 < 0 and 90*n - 19*td - 750*z - 2924 = 0
or 2*p1 - 7 >= 0 and 691920*i2 - 18000*n + 2162250*p1 + 17298*q + 3800*
td + 150000*z - 4405673 = 0) or 400*q + 9*td - 20050 <= 0 and 200*i2 -
10*q - td + 385 = 0 and n - td = 0 and 1460720*i2 - 35750*n + 4564750*p1
 + 36518*q + 3800*td + 950000*z - 12726143 >= 0 and 76880*i2 - 2000*n +
240250*p1 + 1922*q + 200*td + 50000*z - 469797 >= 0 and 76880*i2 - 2000*
n + 240250*p1 + 1922*q + 200*td + 50000*z - 669797 <= 0 and q - 40 <= 0
and q >= 0 and (80*i2 + 250*p1 + 2*q - 1057 > 0 and 80*i2 + 250*p1 + 2*q
 - 1377 <= 0 and 17680*i2 + 55250*p1 + 442*q + 20000*z - 483917 = 0 or
80*i2 + 250*p1 + 2*q - 1377 > 0 and 80*i2 + 250*p1 + 2*q - 1457 <= 0 or
80*i2 + 250*p1 + 2*q - 1457 > 0 and 80*i2 + 250*p1 + 2*q - 1697 < 0 and
29970000*i2 + 93656250*p1 + 749250*q + 2500000*z - 569558609 = 0) and (
td - 400 >= 0 and td - 700 < 0 and 230640*i2 - 6000*n + 720750*p1 + 5766
*q - 150*td + 50000*z - 476891 = 0 or td - 700 >= 0 and td - 990 < 0 and
 691920*i2 - 18000*n + 2162250*p1 + 17298*q + 3800*td + 150000*z -
4405673 = 0) and (2*p1 - 7 < 0 and 80*i2 + 250*p1 + 2*q - 577 = 0 or 2*
p1 - 7 >= 0) or 400*q + 9*td - 20050 <= 0 and i2 = 0 and n - td = 0 and
n >= 0 and q - 40 <= 0 and q >= 0 and (100*n - 10*td - 2500*z - 17299 >
0 and 20*n - 2*td - 500*z - 6535 <= 0 and 4420*n - 442*td + 81700*z -
3170191 = 0 or 20*n - 2*td - 500*z - 6535 > 0 and 100*n - 10*td - 2500*z
 - 36519 <= 0 or 100*n - 10*td - 2500*z - 36519 > 0 and 100*n - 10*td -
2500*z - 48051 < 0 and 187312500*n - 18731250*td - 4082187500*z - 74105780531
 = 0) and (td - 400 >= 0 and td - 700 < 0 and 3*td + 400*z - 5320 = 0 or
 td - 700 >= 0 and td - 990 < 0 and 2*td - 300*z + 1015 = 0 or td = 0
and z = 0) and (2*p1 - 7 < 0 and 20*n - 2*td - 500*z + 1153 = 0 or 2*p1
- 7 >= 0 and 76880*i2 - 2000*n + 240250*p1 + 1922*q + 200*td + 50000*z -
 669797 = 0) or 400*q + 9*td - 20050 <= 0 and i2 = 0 and n - td = 0 and
715*n - 76*td - 19000*z - 248330 <= 0 and 20*n - 2*td - 500*z - 8535 <=
0 and 20*n - 2*td - 500*z - 6535 >= 0 and q - 40 <= 0 and q >= 0 and 50*
z - 449 = 0 and 2*p1 - 7 >= 0 and 80*i2 + 250*p1 + 2*q - 1377 = 0 and (
td - 400 >= 0 and td - 700 < 0 and 3*td + 400*z - 5320 = 0 or td - 700
>= 0 and td - 990 < 0 and 2*td - 300*z + 1015 = 0 or td = 0 and z = 0)
or 400*q + 9*td - 20050 <= 0 and i2 = 0 and n - td = 0 and 158015*n -
16796*td + 3104600*z - 120467258 <= 0 and 4420*n - 442*td + 81700*z -
3612191 <= 0 and 4420*n - 442*td + 81700*z - 3170191 >= 0 and q - 40 <=
0 and q >= 0 and (250*z - 3129 < 0 and 50*z - 449 >= 0 or 50*z - 449 < 0
 and 125*z - 1012 >= 0 or 125*z - 1012 < 0 and 250*z - 1361 > 0 and
108437500*z - 865858649 = 0) and (td - 400 >= 0 and td - 700 < 0 and 3*
td + 400*z - 5320 = 0 or td - 700 >= 0 and td - 990 < 0 and 2*td - 300*z
 + 1015 = 0 or td = 0 and z = 0) and (2*p1 - 7 < 0 and 50*z - 891 = 0 or
 2*p1 - 7 >= 0 and 17680*i2 + 55250*p1 + 442*q + 20000*z - 483917 = 0)
or 400*q + 9*td - 20050 <= 0 and i2 = 0 and n - td = 0 and 3575*n - 380*
td - 95000*z - 1387722 <= 0 and 100*n - 10*td - 2500*z - 46519 <= 0 and
100*n - 10*td - 2500*z - 36519 >= 0 and q - 40 <= 0 and q >= 0 and 2*p1
- 7 >= 0 and 80*i2 + 250*p1 + 2*q - 1457 = 0 and (td - 400 >= 0 and td -
 700 < 0 and 3*td + 400*z - 5320 = 0 or td - 700 >= 0 and td - 990 < 0
and 2*td - 300*z + 1015 = 0 or td = 0 and z = 0) or 400*q + 9*td - 20050
 <= 0 and i2 = 0 and n - td = 0 and 1460720*i2 - 35750*n + 4564750*p1 +
36518*q + 3800*td + 950000*z - 12726143 >= 0 and 76880*i2 - 2000*n +
240250*p1 + 1922*q + 200*td + 50000*z - 469797 >= 0 and 76880*i2 - 2000*
n + 240250*p1 + 1922*q + 200*td + 50000*z - 669797 <= 0 and q - 40 <= 0
and q >= 0 and (80*i2 + 250*p1 + 2*q - 1057 > 0 and 80*i2 + 250*p1 + 2*q
 - 1377 <= 0 and 17680*i2 + 55250*p1 + 442*q + 20000*z - 483917 = 0 or
80*i2 + 250*p1 + 2*q - 1377 > 0 and 80*i2 + 250*p1 + 2*q - 1457 <= 0 or
80*i2 + 250*p1 + 2*q - 1457 > 0 and 80*i2 + 250*p1 + 2*q - 1697 < 0 and
29970000*i2 + 93656250*p1 + 749250*q + 2500000*z - 569558609 = 0) and (
td - 400 >= 0 and td - 700 < 0 and 3*td + 400*z - 5320 = 0 or td - 700
>= 0 and td - 990 < 0 and 2*td - 300*z + 1015 = 0 or td = 0 and z = 0)
and (2*p1 - 7 < 0 and 80*i2 + 250*p1 + 2*q - 577 = 0 or 2*p1 - 7 >= 0)
or 400*q + 9*td - 20050 > 0 and 200*i2 - 10*q - td + 385 = 0 and n - td
= 0 and n >= 0 and q - 40 <= 0 and q >= 0 and (62500*n - 6250*td -
1250000*z - 32509373 < 0 and 62500*n - 6250*td - 1250000*z - 27134373 >=
 0 and 31937500*n - 3193750*td - 571562500*z - 13629165033 = 0 or 62500*
n - 6250*td - 1250000*z - 27134373 < 0 and 62500*n - 6250*td - 1250000*z
 - 25790623 >= 0 and 187312500*n - 18731250*td - 4082187500*z - 74105780531
 = 0 or 62500*n - 6250*td - 1250000*z - 25790623 < 0 and 62500*n - 6250*
td - 1250000*z - 21759373 > 0) and (td - 400 >= 0 and td - 700 < 0 and 3
*td + 400*z - 6130 = 0 or td - 700 >= 0 and td - 990 < 0 and 4*td - 600*
z + 3245 = 0) and (2*p1 - 7 < 0 and 62500*n - 6250*td - 1250000*z -
40571873 = 0 or 2*p1 - 7 >= 0 and 10750000*i2 + 500000*n + 33593750*p1 +
 268750*q - 50000*td - 10000000*z - 402109359 = 0) or 400*q + 9*td -
20050 > 0 and 200*i2 - 10*q - td + 385 = 0 and n - td = 0 and 1141765625
*n - 121362500*td - 21719375000*z - 517908271254 <= 0 and 31937500*n -
3193750*td - 571562500*z - 16822915033 <= 0 and 31937500*n - 3193750*td
- 571562500*z - 13629165033 >= 0 and q - 40 <= 0 and q >= 0 and (156250*
z + 6937499 > 0 and 156250*z + 549999 <= 0 or 156250*z + 549999 > 0 and
78125*z - 523438 <= 0 and 108437500*z - 865858649 = 0 or 78125*z -
523438 > 0 and 156250*z - 5837501 < 0) and (td - 400 >= 0 and td - 700 <
 0 and 191625000*n + 4790625*td - 235625000*z - 130719208948 = 0 or td -
 700 >= 0 and td - 990 < 0 and 143718750*n - 30340625*td - 176718750*z -
 74285891086 = 0) and (2*p1 - 7 < 0 and 156250*z + 16518749 = 0 or 2*p1
- 7 >= 0 and 25550000*i2 + 79843750*p1 + 638750*q - 2500000*z -
448579359 = 0) or 400*q + 9*td - 20050 > 0 and 200*i2 - 10*q - td + 385
= 0 and n - td = 0 and 6696421875*n - 711787500*td - 155123125000*z - 2816019660178
 <= 0 and 187312500*n - 18731250*td - 4082187500*z - 92837030531 <= 0
and 187312500*n - 18731250*td - 4082187500*z - 74105780531 >= 0 and q -
40 <= 0 and q >= 0 and (156250*z - 10848749 < 0 and 156250*z - 3356249
>= 0 and 108437500*z - 865858649 = 0 or 156250*z - 3356249 < 0 and 78125
*z - 741562 >= 0 or 78125*z - 741562 < 0 and 156250*z + 4136251 > 0) and
 (td - 400 >= 0 and td - 700 < 0 and 374625000*n + 9365625*td - 1920625000
*z - 243897029812 = 0 or td - 700 >= 0 and td - 990 < 0 and 93656250*n -
 19771875*td - 480156250*z - 45494960578 = 0) and (2*p1 - 7 < 0 and
156250*z - 22087499 = 0 or 2*p1 - 7 >= 0 and 29970000*i2 + 93656250*p1 +
 749250*q + 2500000*z - 569558609 = 0) or 400*q + 9*td - 20050 > 0 and
200*i2 - 10*q - td + 385 = 0 and n - td = 0 and 27*n + 57*td + 7600*z -
116470 >= 0 and 3*td + 400*z - 3730 >= 0 and 3*td + 400*z - 6130 <= 0
and q - 40 <= 0 and q >= 0 and (375000*n + 9375*td - 1250000*z -
290837488 < 0 and 375000*n + 9375*td - 1250000*z - 258587488 >= 0 and
191625000*n + 4790625*td - 235625000*z - 130719208948 = 0 or 375000*n +
9375*td - 1250000*z - 258587488 < 0 and 375000*n + 9375*td - 1250000*z -
 250524988 >= 0 and 374625000*n + 9365625*td - 1920625000*z - 243897029812
 = 0 or 375000*n + 9375*td - 1250000*z - 250524988 < 0 and 375000*n +
9375*td - 1250000*z - 226337488 > 0) and (td - 400 >= 0 and td - 700 < 0
 or td - 990 < 0 and td - 700 = 0) and (2*p1 - 7 < 0 and 375000*n + 9375
*td - 1250000*z - 339212488 = 0 or 2*p1 - 7 >= 0 and 32250000*i2 +
1500000*n + 100781250*p1 + 806250*q + 37500*td - 5000000*z - 1589453077
= 0) or 400*q + 9*td - 20050 > 0 and 200*i2 - 10*q - td + 385 = 0 and n
- td = 0 and 81*n - 152*td + 22800*z - 123310 >= 0 and 4*td - 600*z -
355 <= 0 and 4*td - 600*z + 3245 >= 0 and q - 40 <= 0 and q >= 0 and td
- 700 >= 0 and td - 990 < 0 and (281250*n - 59375*td - 937500*z -
171643741 < 0 and 281250*n - 59375*td - 937500*z - 147456241 >= 0 and
143718750*n - 30340625*td - 176718750*z - 74285891086 = 0 or 281250*n -
59375*td - 937500*z - 147456241 < 0 and 281250*n - 59375*td - 937500*z -
 141409366 >= 0 and 93656250*n - 19771875*td - 480156250*z - 45494960578
 = 0 or 281250*n - 59375*td - 937500*z - 141409366 < 0 and 281250*n -
59375*td - 937500*z - 123268741 > 0) and (2*p1 - 7 < 0 and 281250*n -
59375*td - 937500*z - 207924991 = 0 or 2*p1 - 7 >= 0 and 96750000*i2 +
4500000*n + 302343750*p1 + 2418750*q - 950000*td - 15000000*z - 4024609231
 = 0) or 400*q + 9*td - 20050 > 0 and 200*i2 - 10*q - td + 385 = 0 and n
 - td = 0 and 204250000*i2 + 8937500*n + 638281250*p1 + 5106250*q -
950000*td - 190000000*z - 7640077821 <= 0 and 10750000*i2 + 500000*n +
33593750*p1 + 268750*q - 50000*td - 10000000*z - 452109359 <= 0 and
10750000*i2 + 500000*n + 33593750*p1 + 268750*q - 50000*td - 10000000*z
- 402109359 >= 0 and q - 40 <= 0 and q >= 0 and (80*i2 + 250*p1 + 2*q -
1057 > 0 and 80*i2 + 250*p1 + 2*q - 1377 <= 0 and 25550000*i2 + 79843750
*p1 + 638750*q - 2500000*z - 448579359 = 0 or 80*i2 + 250*p1 + 2*q -
1377 > 0 and 80*i2 + 250*p1 + 2*q - 1457 <= 0 and 29970000*i2 + 93656250
*p1 + 749250*q + 2500000*z - 569558609 = 0 or 80*i2 + 250*p1 + 2*q -
1457 > 0 and 80*i2 + 250*p1 + 2*q - 1697 < 0) and (td - 400 >= 0 and td
- 700 < 0 and 32250000*i2 + 1500000*n + 100781250*p1 + 806250*q + 37500*
td - 5000000*z - 1589453077 = 0 or td - 700 >= 0 and td - 990 < 0 and
96750000*i2 + 4500000*n + 302343750*p1 + 2418750*q - 950000*td -
15000000*z - 4024609231 = 0) and (2*p1 - 7 < 0 and 80*i2 + 250*p1 + 2*q
- 577 = 0 or 2*p1 - 7 >= 0) or 400*q + 9*td - 20050 > 0 and i2 = 0 and n
 - td = 0 and n >= 0 and q - 40 <= 0 and q >= 0 and (62500*n - 6250*td -
 1250000*z - 32509373 < 0 and 62500*n - 6250*td - 1250000*z - 27134373
>= 0 and 31937500*n - 3193750*td - 571562500*z - 13629165033 = 0 or
62500*n - 6250*td - 1250000*z - 27134373 < 0 and 62500*n - 6250*td -
1250000*z - 25790623 >= 0 and 187312500*n - 18731250*td - 4082187500*z -
 74105780531 = 0 or 62500*n - 6250*td - 1250000*z - 25790623 < 0 and
62500*n - 6250*td - 1250000*z - 21759373 > 0) and (td - 400 >= 0 and td
- 700 < 0 and 3*td + 400*z - 5320 = 0 or td - 700 >= 0 and td - 990 < 0
and 2*td - 300*z + 1015 = 0 or td = 0 and z = 0) and (2*p1 - 7 < 0 and
62500*n - 6250*td - 1250000*z - 40571873 = 0 or 2*p1 - 7 >= 0 and
10750000*i2 + 500000*n + 33593750*p1 + 268750*q - 50000*td - 10000000*z
- 402109359 = 0) or 400*q + 9*td - 20050 > 0 and i2 = 0 and n - td = 0
and 1141765625*n - 121362500*td - 21719375000*z - 517908271254 <= 0 and
31937500*n - 3193750*td - 571562500*z - 16822915033 <= 0 and 31937500*n
- 3193750*td - 571562500*z - 13629165033 >= 0 and q - 40 <= 0 and q >= 0
 and (156250*z + 6937499 > 0 and 156250*z + 549999 <= 0 or 156250*z +
549999 > 0 and 78125*z - 523438 <= 0 and 108437500*z - 865858649 = 0 or
78125*z - 523438 > 0 and 156250*z - 5837501 < 0) and (td - 400 >= 0 and
td - 700 < 0 and 3*td + 400*z - 5320 = 0 or td - 700 >= 0 and td - 990 <
 0 and 2*td - 300*z + 1015 = 0 or td = 0 and z = 0) and (2*p1 - 7 < 0
and 156250*z + 16518749 = 0 or 2*p1 - 7 >= 0 and 25550000*i2 + 79843750*
p1 + 638750*q - 2500000*z - 448579359 = 0) or 400*q + 9*td - 20050 > 0
and i2 = 0 and n - td = 0 and 6696421875*n - 711787500*td - 155123125000
*z - 2816019660178 <= 0 and 187312500*n - 18731250*td - 4082187500*z - 92837030531
 <= 0 and 187312500*n - 18731250*td - 4082187500*z - 74105780531 >= 0
and q - 40 <= 0 and q >= 0 and (156250*z - 10848749 < 0 and 156250*z -
3356249 >= 0 and 108437500*z - 865858649 = 0 or 156250*z - 3356249 < 0
and 78125*z - 741562 >= 0 or 78125*z - 741562 < 0 and 156250*z + 4136251
 > 0) and (td - 400 >= 0 and td - 700 < 0 and 3*td + 400*z - 5320 = 0 or
 td - 700 >= 0 and td - 990 < 0 and 2*td - 300*z + 1015 = 0 or td = 0
and z = 0) and (2*p1 - 7 < 0 and 156250*z - 22087499 = 0 or 2*p1 - 7 >=
0 and 29970000*i2 + 93656250*p1 + 749250*q + 2500000*z - 569558609 = 0)
or 400*q + 9*td - 20050 > 0 and i2 = 0 and n - td = 0 and 204250000*i2 +
 8937500*n + 638281250*p1 + 5106250*q - 950000*td - 190000000*z - 7640077821
 <= 0 and 10750000*i2 + 500000*n + 33593750*p1 + 268750*q - 50000*td -
10000000*z - 452109359 <= 0 and 10750000*i2 + 500000*n + 33593750*p1 +
268750*q - 50000*td - 10000000*z - 402109359 >= 0 and q - 40 <= 0 and q
>= 0 and (80*i2 + 250*p1 + 2*q - 1057 > 0 and 80*i2 + 250*p1 + 2*q -
1377 <= 0 and 25550000*i2 + 79843750*p1 + 638750*q - 2500000*z -
448579359 = 0 or 80*i2 + 250*p1 + 2*q - 1377 > 0 and 80*i2 + 250*p1 + 2*
q - 1457 <= 0 and 29970000*i2 + 93656250*p1 + 749250*q + 2500000*z -
569558609 = 0 or 80*i2 + 250*p1 + 2*q - 1457 > 0 and 80*i2 + 250*p1 + 2*
q - 1697 < 0) and (td - 400 >= 0 and td - 700 < 0 and 3*td + 400*z -
5320 = 0 or td - 700 >= 0 and td - 990 < 0 and 2*td - 300*z + 1015 = 0
or td = 0 and z = 0) and (2*p1 - 7 < 0 and 80*i2 + 250*p1 + 2*q - 577 =
0 or 2*p1 - 7 >= 0) or 400*q + 9*td - 20050 <= 0 and 200*i2 - 10*q - td
+ 385 = 0 and n - td = 0 and n >= 0 and q - 40 <= 0 and q >= 0 and (
62500*n - 6250*td - 1250000*z - 32509373 < 0 and 62500*n - 6250*td -
1250000*z - 27134373 >= 0 and 31937500*n - 3193750*td - 571562500*z - 13629165033
 = 0 or 62500*n - 6250*td - 1250000*z - 27134373 < 0 and 62500*n - 6250*
td - 1250000*z - 25790623 >= 0 and 187312500*n - 18731250*td - 4082187500
*z - 74105780531 = 0 or 62500*n - 6250*td - 1250000*z - 25790623 < 0 and
 62500*n - 6250*td - 1250000*z - 21759373 > 0) and (td - 400 >= 0 and td
 - 700 < 0 and 3*td + 400*z - 6130 = 0 or td - 700 >= 0 and td - 990 < 0
 and 4*td - 600*z + 3245 = 0) and (2*p1 - 7 < 0 and 62500*n - 6250*td -
1250000*z - 40571873 = 0 or 2*p1 - 7 >= 0 and 10750000*i2 + 500000*n +
33593750*p1 + 268750*q - 50000*td - 10000000*z - 402109359 = 0) or 400*q
 + 9*td - 20050 <= 0 and 200*i2 - 10*q - td + 385 = 0 and n - td = 0 and
 1141765625*n - 121362500*td - 21719375000*z - 517908271254 <= 0 and
31937500*n - 3193750*td - 571562500*z - 16822915033 <= 0 and 31937500*n
- 3193750*td - 571562500*z - 13629165033 >= 0 and q - 40 <= 0 and q >= 0
 and (156250*z + 6937499 > 0 and 156250*z + 549999 <= 0 or 156250*z +
549999 > 0 and 78125*z - 523438 <= 0 and 108437500*z - 865858649 = 0 or
78125*z - 523438 > 0 and 156250*z - 5837501 < 0) and (td - 400 >= 0 and
td - 700 < 0 and 191625000*n + 4790625*td - 235625000*z - 130719208948 =
 0 or td - 700 >= 0 and td - 990 < 0 and 143718750*n - 30340625*td -
176718750*z - 74285891086 = 0) and (2*p1 - 7 < 0 and 156250*z + 16518749
 = 0 or 2*p1 - 7 >= 0 and 25550000*i2 + 79843750*p1 + 638750*q - 2500000
*z - 448579359 = 0) or 400*q + 9*td - 20050 <= 0 and 200*i2 - 10*q - td
+ 385 = 0 and n - td = 0 and 6696421875*n - 711787500*td - 155123125000*
z - 2816019660178 <= 0 and 187312500*n - 18731250*td - 4082187500*z - 92837030531
 <= 0 and 187312500*n - 18731250*td - 4082187500*z - 74105780531 >= 0
and q - 40 <= 0 and q >= 0 and (156250*z - 10848749 < 0 and 156250*z -
3356249 >= 0 and 108437500*z - 865858649 = 0 or 156250*z - 3356249 < 0
and 78125*z - 741562 >= 0 or 78125*z - 741562 < 0 and 156250*z + 4136251
 > 0) and (td - 400 >= 0 and td - 700 < 0 and 374625000*n + 9365625*td -
 1920625000*z - 243897029812 = 0 or td - 700 >= 0 and td - 990 < 0 and
93656250*n - 19771875*td - 480156250*z - 45494960578 = 0) and (2*p1 - 7
< 0 and 156250*z - 22087499 = 0 or 2*p1 - 7 >= 0 and 29970000*i2 +
93656250*p1 + 749250*q + 2500000*z - 569558609 = 0) or 400*q + 9*td -
20050 <= 0 and 200*i2 - 10*q - td + 385 = 0 and n - td = 0 and 27*n + 57
*td + 7600*z - 116470 >= 0 and 3*td + 400*z - 3730 >= 0 and 3*td + 400*z
 - 6130 <= 0 and q - 40 <= 0 and q >= 0 and (375000*n + 9375*td -
1250000*z - 290837488 < 0 and 375000*n + 9375*td - 1250000*z - 258587488
 >= 0 and 191625000*n + 4790625*td - 235625000*z - 130719208948 = 0 or
375000*n + 9375*td - 1250000*z - 258587488 < 0 and 375000*n + 9375*td -
1250000*z - 250524988 >= 0 and 374625000*n + 9365625*td - 1920625000*z -
 243897029812 = 0 or 375000*n + 9375*td - 1250000*z - 250524988 < 0 and
375000*n + 9375*td - 1250000*z - 226337488 > 0) and (td - 400 >= 0 and
td - 700 < 0 or td - 990 < 0 and td - 700 = 0) and (2*p1 - 7 < 0 and
375000*n + 9375*td - 1250000*z - 339212488 = 0 or 2*p1 - 7 >= 0 and
32250000*i2 + 1500000*n + 100781250*p1 + 806250*q + 37500*td - 5000000*z
 - 1589453077 = 0) or 400*q + 9*td - 20050 <= 0 and 200*i2 - 10*q - td +
 385 = 0 and n - td = 0 and 81*n - 152*td + 22800*z - 123310 >= 0 and 4*
td - 600*z - 355 <= 0 and 4*td - 600*z + 3245 >= 0 and q - 40 <= 0 and q
 >= 0 and td - 700 >= 0 and td - 990 < 0 and (281250*n - 59375*td -
937500*z - 171643741 < 0 and 281250*n - 59375*td - 937500*z - 147456241
>= 0 and 143718750*n - 30340625*td - 176718750*z - 74285891086 = 0 or
281250*n - 59375*td - 937500*z - 147456241 < 0 and 281250*n - 59375*td -
 937500*z - 141409366 >= 0 and 93656250*n - 19771875*td - 480156250*z - 45494960578
 = 0 or 281250*n - 59375*td - 937500*z - 141409366 < 0 and 281250*n -
59375*td - 937500*z - 123268741 > 0) and (2*p1 - 7 < 0 and 281250*n -
59375*td - 937500*z - 207924991 = 0 or 2*p1 - 7 >= 0 and 96750000*i2 +
4500000*n + 302343750*p1 + 2418750*q - 950000*td - 15000000*z - 4024609231
 = 0) or 400*q + 9*td - 20050 <= 0 and 200*i2 - 10*q - td + 385 = 0 and
n - td = 0 and 204250000*i2 + 8937500*n + 638281250*p1 + 5106250*q -
950000*td - 190000000*z - 7640077821 <= 0 and 10750000*i2 + 500000*n +
33593750*p1 + 268750*q - 50000*td - 10000000*z - 452109359 <= 0 and
10750000*i2 + 500000*n + 33593750*p1 + 268750*q - 50000*td - 10000000*z
- 402109359 >= 0 and q - 40 <= 0 and q >= 0 and (80*i2 + 250*p1 + 2*q -
1057 > 0 and 80*i2 + 250*p1 + 2*q - 1377 <= 0 and 25550000*i2 + 79843750
*p1 + 638750*q - 2500000*z - 448579359 = 0 or 80*i2 + 250*p1 + 2*q -
1377 > 0 and 80*i2 + 250*p1 + 2*q - 1457 <= 0 and 29970000*i2 + 93656250
*p1 + 749250*q + 2500000*z - 569558609 = 0 or 80*i2 + 250*p1 + 2*q -
1457 > 0 and 80*i2 + 250*p1 + 2*q - 1697 < 0) and (td - 400 >= 0 and td
- 700 < 0 and 32250000*i2 + 1500000*n + 100781250*p1 + 806250*q + 37500*
td - 5000000*z - 1589453077 = 0 or td - 700 >= 0 and td - 990 < 0 and
96750000*i2 + 4500000*n + 302343750*p1 + 2418750*q - 950000*td -
15000000*z - 4024609231 = 0) and (2*p1 - 7 < 0 and 80*i2 + 250*p1 + 2*q
- 577 = 0 or 2*p1 - 7 >= 0) or 400*q + 9*td - 20050 <= 0 and i2 = 0 and
n - td = 0 and n >= 0 and q - 40 <= 0 and q >= 0 and (62500*n - 6250*td
- 1250000*z - 32509373 < 0 and 62500*n - 6250*td - 1250000*z - 27134373
>= 0 and 31937500*n - 3193750*td - 571562500*z - 13629165033 = 0 or
62500*n - 6250*td - 1250000*z - 27134373 < 0 and 62500*n - 6250*td -
1250000*z - 25790623 >= 0 and 187312500*n - 18731250*td - 4082187500*z -
 74105780531 = 0 or 62500*n - 6250*td - 1250000*z - 25790623 < 0 and
62500*n - 6250*td - 1250000*z - 21759373 > 0) and (td - 400 >= 0 and td
- 700 < 0 and 3*td + 400*z - 5320 = 0 or td - 700 >= 0 and td - 990 < 0
and 2*td - 300*z + 1015 = 0 or td = 0 and z = 0) and (2*p1 - 7 < 0 and
62500*n - 6250*td - 1250000*z - 40571873 = 0 or 2*p1 - 7 >= 0 and
10750000*i2 + 500000*n + 33593750*p1 + 268750*q - 50000*td - 10000000*z
- 402109359 = 0) or 400*q + 9*td - 20050 <= 0 and i2 = 0 and n - td = 0
and 1141765625*n - 121362500*td - 21719375000*z - 517908271254 <= 0 and
31937500*n - 3193750*td - 571562500*z - 16822915033 <= 0 and 31937500*n
- 3193750*td - 571562500*z - 13629165033 >= 0 and q - 40 <= 0 and q >= 0
 and (156250*z + 6937499 > 0 and 156250*z + 549999 <= 0 or 156250*z +
549999 > 0 and 78125*z - 523438 <= 0 and 108437500*z - 865858649 = 0 or
78125*z - 523438 > 0 and 156250*z - 5837501 < 0) and (td - 400 >= 0 and
td - 700 < 0 and 3*td + 400*z - 5320 = 0 or td - 700 >= 0 and td - 990 <
 0 and 2*td - 300*z + 1015 = 0 or td = 0 and z = 0) and (2*p1 - 7 < 0
and 156250*z + 16518749 = 0 or 2*p1 - 7 >= 0 and 25550000*i2 + 79843750*
p1 + 638750*q - 2500000*z - 448579359 = 0) or 400*q + 9*td - 20050 <= 0
and i2 = 0 and n - td = 0 and 6696421875*n - 711787500*td - 155123125000
*z - 2816019660178 <= 0 and 187312500*n - 18731250*td - 4082187500*z - 92837030531
 <= 0 and 187312500*n - 18731250*td - 4082187500*z - 74105780531 >= 0
and q - 40 <= 0 and q >= 0 and (156250*z - 10848749 < 0 and 156250*z -
3356249 >= 0 and 108437500*z - 865858649 = 0 or 156250*z - 3356249 < 0
and 78125*z - 741562 >= 0 or 78125*z - 741562 < 0 and 156250*z + 4136251
 > 0) and (td - 400 >= 0 and td - 700 < 0 and 3*td + 400*z - 5320 = 0 or
 td - 700 >= 0 and td - 990 < 0 and 2*td - 300*z + 1015 = 0 or td = 0
and z = 0) and (2*p1 - 7 < 0 and 156250*z - 22087499 = 0 or 2*p1 - 7 >=
0 and 29970000*i2 + 93656250*p1 + 749250*q + 2500000*z - 569558609 = 0)
or 400*q + 9*td - 20050 <= 0 and i2 = 0 and n - td = 0 and 204250000*i2
+ 8937500*n + 638281250*p1 + 5106250*q - 950000*td - 190000000*z - 7640077821
 <= 0 and 10750000*i2 + 500000*n + 33593750*p1 + 268750*q - 50000*td -
10000000*z - 452109359 <= 0 and 10750000*i2 + 500000*n + 33593750*p1 +
268750*q - 50000*td - 10000000*z - 402109359 >= 0 and q - 40 <= 0 and q
>= 0 and (80*i2 + 250*p1 + 2*q - 1057 > 0 and 80*i2 + 250*p1 + 2*q -
1377 <= 0 and 25550000*i2 + 79843750*p1 + 638750*q - 2500000*z -
448579359 = 0 or 80*i2 + 250*p1 + 2*q - 1377 > 0 and 80*i2 + 250*p1 + 2*
q - 1457 <= 0 and 29970000*i2 + 93656250*p1 + 749250*q + 2500000*z -
569558609 = 0 or 80*i2 + 250*p1 + 2*q - 1457 > 0 and 80*i2 + 250*p1 + 2*
q - 1697 < 0) and (td - 400 >= 0 and td - 700 < 0 and 3*td + 400*z -
5320 = 0 or td - 700 >= 0 and td - 990 < 0 and 2*td - 300*z + 1015 = 0
or td = 0 and z = 0) and (2*p1 - 7 < 0 and 80*i2 + 250*p1 + 2*q - 577 =
0 or 2*p1 - 7 >= 0)$



rltab testseries12;


true and (n - td = 0 and (td - 990 < 0 and ((50*z - 449 = 0 and q >= 0

 and q - 40 <= 0 and 2*p1 - 7 >= 0 and 250*p1 + 2*q - 1377 = 0

 and 20*n - 2*td - 13025 <= 0 and 20*n - 2*td - 11025 >= 0

 and 715*n - 76*td - 418950 <= 0 and i2 = 0

 and (td - 576 = 0 or 2*td - 1679 = 0)) or (50*z - 449 = 0 and q >= 0

 and q - 40 <= 0 and 2*p1 - 7 >= 0 and 20*n - 2*td - 13025 <= 0

 and 20*n - 2*td - 11025 >= 0 and 715*n - 76*td - 418950 <= 0

 and 80*i2 + 250*p1 + 2*q - 1377 = 0 and 200*i2 - 10*q - td + 385 = 0 and (

(td - 700 < 0 and td - 400 >= 0 and 40*n + td - 26280 = 0)

 or (td - 700 >= 0 and 90*n - 19*td - 44255 = 0))) or (125*z - 1012 = 0

 and q >= 0 and q - 40 <= 0 and 2*p1 - 7 >= 0 and 250*p1 + 2*q - 1457 = 0

 and 100*n - 10*td - 66759 <= 0 and 100*n - 10*td - 56759 >= 0

 and 3575*n - 380*td - 2156842 <= 0 and i2 = 0

 and (10*td - 7069 = 0 or 15*td - 10408 = 0)) or (125*z - 1012 = 0 and q >= 0

 and q - 40 <= 0 and 2*p1 - 7 >= 0 and 100*n - 10*td - 66759 <= 0

 and 100*n - 10*td - 56759 >= 0 and 3575*n - 380*td - 2156842 <= 0

 and 80*i2 + 250*p1 + 2*q - 1457 = 0 and 200*i2 - 10*q - td + 385 = 0 and (

(td - 700 < 0 and td - 400 >= 0 and 600*n + 15*td - 412844 = 0)

 or (td - 700 >= 0 and 450*n - 95*td - 235258 = 0))) or (td - 700 >= 0

 and 4*td - 600*z - 355 <= 0 and 4*td - 600*z + 3245 >= 0 and q >= 0

 and q - 40 <= 0 and 2*p1 - 7 >= 0 and 81*n - 152*td + 22800*z - 123310 >= 0

 and 90*n - 19*td + 150*z - 45602 = 0 and 80*i2 + 250*p1 + 2*q - 1377 = 0

 and 200*i2 - 10*q - td + 385 = 0) or (td - 700 >= 0 and 4*td - 600*z - 355 <= 0

 and 4*td - 600*z + 3245 >= 0 and q >= 0 and q - 40 <= 0 and 2*p1 - 7 >= 0

 and 81*n - 152*td + 22800*z - 123310 >= 0

 and 450*n - 95*td - 3750*z - 204898 = 0 and 80*i2 + 250*p1 + 2*q - 1457 = 0

 and 200*i2 - 10*q - td + 385 = 0) or (td - 700 >= 0 and 4*td - 600*z - 355 <= 0

 and 4*td - 600*z + 3245 >= 0 and q >= 0 and q - 40 <= 0

 and 81*n - 152*td + 22800*z - 123310 >= 0 and 200*i2 - 10*q - td + 385 = 0

 and (2*p1 - 7 >= 0 or 80*i2 + 250*p1 + 2*q - 577 = 0) and ((

80*i2 + 250*p1 + 2*q - 1697 < 0 and 80*i2 + 250*p1 + 2*q - 1457 > 0 and 

96750000*i2 + 4500000*n + 302343750*p1 + 2418750*q - 950000*td - 15000000*z

 - 4024609231 = 0) or (80*i2 + 250*p1 + 2*q - 1457 <= 0

 and 80*i2 + 250*p1 + 2*q - 1377 > 0 and 

691920*i2 - 18000*n + 2162250*p1 + 17298*q + 3800*td + 150000*z - 4405673 = 0) 

or (80*i2 + 250*p1 + 2*q - 1377 <= 0 and 80*i2 + 250*p1 + 2*q - 1057 > 0

 and 26640*i2 - 900*n + 83250*p1 + 666*q + 190*td - 1500*z - 2521 = 0))) or (

td - 700 >= 0 and 4*td - 600*z - 355 <= 0 and 4*td - 600*z + 3245 >= 0

 and q >= 0 and q - 40 <= 0 and 81*n - 152*td + 22800*z - 123310 >= 0

 and 200*i2 - 10*q - td + 385 = 0 and (

(2*p1 - 7 < 0 and 90*n - 19*td - 750*z - 2924 = 0) or (2*p1 - 7 >= 0 and 

691920*i2 - 18000*n + 2162250*p1 + 17298*q + 3800*td + 150000*z - 4405673 = 0)) 

and ((90*n - 19*td - 750*z - 37520 <= 0 and 450*n - 95*td - 3750*z - 118408 > 0

 and 19890*n - 4199*td + 699150*z - 16058722 = 0)

 or (90*n - 19*td - 750*z - 37520 > 0 and 450*n - 95*td - 3750*z - 204898 <= 0) 

or (450*n - 95*td - 3750*z - 256792 < 0 and 450*n - 95*td - 3750*z - 204898 > 0

 and 93656250*n - 19771875*td - 480156250*z - 45494960578 = 0))) or (

td - 700 >= 0 and 4*td - 600*z - 355 <= 0 and 4*td - 600*z + 3245 >= 0

 and q >= 0 and q - 40 <= 0 and 81*n - 152*td + 22800*z - 123310 >= 0

 and 200*i2 - 10*q - td + 385 = 0 and (

(2*p1 - 7 < 0 and 90*n - 19*td + 150*z - 18962 = 0) or (2*p1 - 7 >= 0

 and 26640*i2 - 900*n + 83250*p1 + 666*q + 190*td - 1500*z - 2521 = 0)) and ((

90*n - 19*td + 150*z - 56258 < 0 and 90*n - 19*td + 150*z - 48266 > 0

 and 143718750*n - 30340625*td - 176718750*z - 74285891086 = 0) or (

90*n - 19*td + 150*z - 48266 <= 0 and 90*n - 19*td + 150*z - 45602 > 0

 and 19890*n - 4199*td + 699150*z - 16058722 = 0)

 or (90*n - 19*td + 150*z - 45602 <= 0 and 90*n - 19*td + 150*z - 34946 > 0))) 

or (td - 700 >= 0 and 4*td - 600*z - 355 <= 0 and 4*td - 600*z + 3245 >= 0

 and q >= 0 and q - 40 <= 0 and 81*n - 152*td + 22800*z - 123310 >= 0

 and 200*i2 - 10*q - td + 385 = 0 and (

(2*p1 - 7 < 0 and 281250*n - 59375*td - 937500*z - 207924991 = 0) or (

2*p1 - 7 >= 0 and 96750000*i2 + 4500000*n + 302343750*p1 + 2418750*q - 950000*td

 - 15000000*z - 4024609231 = 0)) and ((

281250*n - 59375*td - 937500*z - 171643741 < 0

 and 281250*n - 59375*td - 937500*z - 147456241 >= 0

 and 143718750*n - 30340625*td - 176718750*z - 74285891086 = 0) or (

281250*n - 59375*td - 937500*z - 147456241 < 0

 and 281250*n - 59375*td - 937500*z - 141409366 >= 0

 and 93656250*n - 19771875*td - 480156250*z - 45494960578 = 0) or (

281250*n - 59375*td - 937500*z - 141409366 < 0

 and 281250*n - 59375*td - 937500*z - 123268741 > 0))) or (

3*td + 400*z - 6130 <= 0 and 3*td + 400*z - 3730 >= 0 and q >= 0 and q - 40 <= 0

 and 2*p1 - 7 >= 0 and 250*p1 + 2*q - 1457 = 0

 and 27*n + 57*td + 7600*z - 116470 >= 0 and 600*n + 15*td - 5000*z - 372364 = 0

 and i2 = 0 and ((z = 0 and td = 0)

 or (td - 700 < 0 and td - 400 >= 0 and 3*td + 400*z - 5320 = 0)

 or (td - 700 >= 0 and 2*td - 300*z + 1015 = 0))) or (3*td + 400*z - 6130 <= 0

 and 3*td + 400*z - 3730 >= 0 and q >= 0 and q - 40 <= 0 and 2*p1 - 7 >= 0

 and 250*p1 + 2*q - 1377 = 0 and 27*n + 57*td + 7600*z - 116470 >= 0

 and 120*n + 3*td + 200*z - 80636 = 0 and i2 = 0 and ((z = 0 and td = 0)

 or (td - 700 < 0 and td - 400 >= 0 and 3*td + 400*z - 5320 = 0)

 or (td - 700 >= 0 and 2*td - 300*z + 1015 = 0))) or (3*td + 400*z - 6130 <= 0

 and 3*td + 400*z - 3730 >= 0 and q >= 0 and q - 40 <= 0 and 2*p1 - 7 >= 0

 and 27*n + 57*td + 7600*z - 116470 >= 0 and 120*n + 3*td + 200*z - 80636 = 0

 and 80*i2 + 250*p1 + 2*q - 1377 = 0 and 200*i2 - 10*q - td + 385 = 0

 and (td - 700 = 0 or (td - 700 < 0 and td - 400 >= 0))) or (

3*td + 400*z - 6130 <= 0 and 3*td + 400*z - 3730 >= 0 and q >= 0 and q - 40 <= 0

 and 2*p1 - 7 >= 0 and 27*n + 57*td + 7600*z - 116470 >= 0

 and 600*n + 15*td - 5000*z - 372364 = 0 and 80*i2 + 250*p1 + 2*q - 1457 = 0

 and 200*i2 - 10*q - td + 385 = 0

 and (td - 700 = 0 or (td - 700 < 0 and td - 400 >= 0))) or (

3*td + 400*z - 6130 <= 0 and 3*td + 400*z - 3730 >= 0 and q >= 0 and q - 40 <= 0

 and 27*n + 57*td + 7600*z - 116470 >= 0 and i2 = 0

 and (2*p1 - 7 >= 0 or 250*p1 + 2*q - 577 = 0) and ((z = 0 and td = 0)

 or (td - 700 < 0 and td - 400 >= 0 and 3*td + 400*z - 5320 = 0)

 or (td - 700 >= 0 and 2*td - 300*z + 1015 = 0)) and ((250*p1 + 2*q - 1697 < 0

 and 250*p1 + 2*q - 1457 > 0

 and 1500000*n + 100781250*p1 + 806250*q + 37500*td - 5000000*z - 1589453077 = 0

) or (250*p1 + 2*q - 1457 <= 0 and 250*p1 + 2*q - 1377 > 0

 and 6000*n - 720750*p1 - 5766*q + 150*td - 50000*z + 476891 = 0) or (

250*p1 + 2*q - 1377 <= 0 and 250*p1 + 2*q - 1057 > 0

 and 600*n - 55500*p1 - 444*q + 15*td + 1000*z - 97486 = 0))) or (

3*td + 400*z - 6130 <= 0 and 3*td + 400*z - 3730 >= 0 and q >= 0 and q - 40 <= 0

 and 27*n + 57*td + 7600*z - 116470 >= 0 and 200*i2 - 10*q - td + 385 = 0

 and (td - 700 = 0 or (td - 700 < 0 and td - 400 >= 0))

 and (2*p1 - 7 >= 0 or 80*i2 + 250*p1 + 2*q - 577 = 0) and ((

80*i2 + 250*p1 + 2*q - 1697 < 0 and 80*i2 + 250*p1 + 2*q - 1457 > 0 and 

32250000*i2 + 1500000*n + 100781250*p1 + 806250*q + 37500*td - 5000000*z

 - 1589453077 = 0) or (80*i2 + 250*p1 + 2*q - 1457 <= 0

 and 80*i2 + 250*p1 + 2*q - 1377 > 0

 and 230640*i2 - 6000*n + 720750*p1 + 5766*q - 150*td + 50000*z - 476891 = 0) or

 (80*i2 + 250*p1 + 2*q - 1377 <= 0 and 80*i2 + 250*p1 + 2*q - 1057 > 0

 and 17760*i2 - 600*n + 55500*p1 + 444*q - 15*td - 1000*z + 97486 = 0))) or (

3*td + 400*z - 6130 <= 0 and 3*td + 400*z - 3730 >= 0 and q >= 0 and q - 40 <= 0

 and 27*n + 57*td + 7600*z - 116470 >= 0 and 200*i2 - 10*q - td + 385 = 0

 and (td - 700 = 0 or (td - 700 < 0 and td - 400 >= 0)) and (

(2*p1 - 7 < 0 and 120*n + 3*td - 1000*z - 23732 = 0) or (2*p1 - 7 >= 0

 and 230640*i2 - 6000*n + 720750*p1 + 5766*q - 150*td + 50000*z - 476891 = 0)) 

and ((120*n + 3*td - 1000*z - 69860 <= 0 and 600*n + 15*td - 5000*z - 257044 > 0

 and 26520*n + 663*td + 932200*z - 25794796 = 0)

 or (120*n + 3*td - 1000*z - 69860 > 0 and 600*n + 15*td - 5000*z - 372364 <= 0)

 or (600*n + 15*td - 5000*z - 441556 < 0 and 600*n + 15*td - 5000*z - 372364 > 0

 and 374625000*n + 9365625*td - 1920625000*z - 243897029812 = 0))) or (

3*td + 400*z - 6130 <= 0 and 3*td + 400*z - 3730 >= 0 and q >= 0 and q - 40 <= 0

 and 27*n + 57*td + 7600*z - 116470 >= 0 and 200*i2 - 10*q - td + 385 = 0

 and (td - 700 = 0 or (td - 700 < 0 and td - 400 >= 0)) and (

(2*p1 - 7 < 0 and 120*n + 3*td + 200*z - 45116 = 0) or (2*p1 - 7 >= 0

 and 17760*i2 - 600*n + 55500*p1 + 444*q - 15*td - 1000*z + 97486 = 0)) and ((

120*n + 3*td + 200*z - 94844 < 0 and 120*n + 3*td + 200*z - 84188 > 0

 and 191625000*n + 4790625*td - 235625000*z - 130719208948 = 0) or (

120*n + 3*td + 200*z - 84188 <= 0 and 120*n + 3*td + 200*z - 80636 > 0

 and 26520*n + 663*td + 932200*z - 25794796 = 0)

 or (120*n + 3*td + 200*z - 80636 <= 0 and 120*n + 3*td + 200*z - 66428 > 0))) 

or (3*td + 400*z - 6130 <= 0 and 3*td + 400*z - 3730 >= 0 and q >= 0

 and q - 40 <= 0 and 27*n + 57*td + 7600*z - 116470 >= 0

 and 200*i2 - 10*q - td + 385 = 0

 and (td - 700 = 0 or (td - 700 < 0 and td - 400 >= 0)) and (

(2*p1 - 7 < 0 and 375000*n + 9375*td - 1250000*z - 339212488 = 0) or (

2*p1 - 7 >= 0 and 32250000*i2 + 1500000*n + 100781250*p1 + 806250*q + 37500*td

 - 5000000*z - 1589453077 = 0)) and ((

375000*n + 9375*td - 1250000*z - 290837488 < 0

 and 375000*n + 9375*td - 1250000*z - 258587488 >= 0

 and 191625000*n + 4790625*td - 235625000*z - 130719208948 = 0) or (

375000*n + 9375*td - 1250000*z - 258587488 < 0

 and 375000*n + 9375*td - 1250000*z - 250524988 >= 0

 and 374625000*n + 9365625*td - 1920625000*z - 243897029812 = 0) or (

375000*n + 9375*td - 1250000*z - 250524988 < 0

 and 375000*n + 9375*td - 1250000*z - 226337488 > 0))) or (

4*td - 600*z - 355 <= 0 and 4*td - 600*z + 3245 >= 0 and q >= 0 and q - 40 <= 0

 and 2*p1 - 7 >= 0 and 250*p1 + 2*q - 1457 = 0

 and 81*n - 152*td + 22800*z - 123310 >= 0

 and 450*n - 95*td - 3750*z - 204898 = 0 and i2 = 0 and ((z = 0 and td = 0)

 or (td - 700 < 0 and td - 400 >= 0 and 3*td + 400*z - 5320 = 0)

 or (td - 700 >= 0 and 2*td - 300*z + 1015 = 0))) or (4*td - 600*z - 355 <= 0

 and 4*td - 600*z + 3245 >= 0 and q >= 0 and q - 40 <= 0 and 2*p1 - 7 >= 0

 and 250*p1 + 2*q - 1377 = 0 and 81*n - 152*td + 22800*z - 123310 >= 0

 and 90*n - 19*td + 150*z - 45602 = 0 and i2 = 0 and ((z = 0 and td = 0)

 or (td - 700 < 0 and td - 400 >= 0 and 3*td + 400*z - 5320 = 0)

 or (td - 700 >= 0 and 2*td - 300*z + 1015 = 0))) or (4*td - 600*z - 355 <= 0

 and 4*td - 600*z + 3245 >= 0 and q >= 0 and q - 40 <= 0

 and 81*n - 152*td + 22800*z - 123310 >= 0 and i2 = 0

 and (2*p1 - 7 >= 0 or 250*p1 + 2*q - 577 = 0) and ((z = 0 and td = 0)

 or (td - 700 < 0 and td - 400 >= 0 and 3*td + 400*z - 5320 = 0)

 or (td - 700 >= 0 and 2*td - 300*z + 1015 = 0)) and ((250*p1 + 2*q - 1697 < 0

 and 250*p1 + 2*q - 1457 > 0 and 

4500000*n + 302343750*p1 + 2418750*q - 950000*td - 15000000*z - 4024609231 = 0) 

or (250*p1 + 2*q - 1457 <= 0 and 250*p1 + 2*q - 1377 > 0

 and 18000*n - 2162250*p1 - 17298*q - 3800*td - 150000*z + 4405673 = 0) or (

250*p1 + 2*q - 1377 <= 0 and 250*p1 + 2*q - 1057 > 0

 and 900*n - 83250*p1 - 666*q - 190*td + 1500*z + 2521 = 0))) or (q >= 0

 and q - 40 <= 0 and 2*p1 - 7 >= 0 and 250*p1 + 2*q - 1457 = 0 and n >= 0

 and 100*n - 10*td - 2500*z - 36519 = 0 and i2 = 0 and ((z = 0 and td = 0)

 or (td - 700 < 0 and td - 400 >= 0 and 3*td + 400*z - 5320 = 0)

 or (td - 700 >= 0 and 2*td - 300*z + 1015 = 0))) or (q >= 0 and q - 40 <= 0

 and 2*p1 - 7 >= 0 and 250*p1 + 2*q - 1457 = 0

 and 100*n - 10*td - 2500*z - 46519 <= 0 and 100*n - 10*td - 2500*z - 36519 >= 0

 and 3575*n - 380*td - 95000*z - 1387722 <= 0 and i2 = 0 and ((z = 0 and td = 0)

 or (td - 700 < 0 and td - 400 >= 0 and 3*td + 400*z - 5320 = 0)

 or (td - 700 >= 0 and 2*td - 300*z + 1015 = 0))) or (q >= 0 and q - 40 <= 0

 and 2*p1 - 7 >= 0 and 250*p1 + 2*q - 1377 = 0 and n >= 0

 and 20*n - 2*td - 300*z - 8331 = 0 and i2 = 0 and ((z = 0 and td = 0)

 or (td - 700 < 0 and td - 400 >= 0 and 3*td + 400*z - 5320 = 0)

 or (td - 700 >= 0 and 2*td - 300*z + 1015 = 0))) or (q >= 0 and q - 40 <= 0

 and 2*p1 - 7 >= 0 and 250*p1 + 2*q - 1377 = 0

 and 20*n - 2*td - 300*z - 10331 <= 0 and 20*n - 2*td - 300*z - 8331 >= 0

 and 715*n - 76*td - 11400*z - 316578 <= 0 and i2 = 0 and ((z = 0 and td = 0)

 or (td - 700 < 0 and td - 400 >= 0 and 3*td + 400*z - 5320 = 0)

 or (td - 700 >= 0 and 2*td - 300*z + 1015 = 0))) or (q >= 0 and q - 40 <= 0

 and 2*p1 - 7 >= 0 and n >= 0 and 20*n - 2*td - 300*z - 8331 = 0

 and 80*i2 + 250*p1 + 2*q - 1377 = 0 and 200*i2 - 10*q - td + 385 = 0 and (

(td - 700 < 0 and td - 400 >= 0 and 3*td + 400*z - 6130 = 0)

 or (td - 700 >= 0 and 4*td - 600*z + 3245 = 0))) or (q >= 0 and q - 40 <= 0

 and 2*p1 - 7 >= 0 and n >= 0 and 100*n - 10*td - 2500*z - 36519 = 0

 and 80*i2 + 250*p1 + 2*q - 1457 = 0 and 200*i2 - 10*q - td + 385 = 0 and (

(td - 700 < 0 and td - 400 >= 0 and 3*td + 400*z - 6130 = 0)

 or (td - 700 >= 0 and 4*td - 600*z + 3245 = 0))) or (q >= 0 and q - 40 <= 0

 and 2*p1 - 7 >= 0 and 20*n - 2*td - 300*z - 10331 <= 0

 and 20*n - 2*td - 300*z - 8331 >= 0 and 715*n - 76*td - 11400*z - 316578 <= 0

 and 80*i2 + 250*p1 + 2*q - 1377 = 0 and 200*i2 - 10*q - td + 385 = 0 and (

(td - 700 < 0 and td - 400 >= 0 and 120*n + 3*td + 200*z - 80636 = 0)

 or (td - 700 >= 0 and 90*n - 19*td + 150*z - 45602 = 0))) or (q >= 0

 and q - 40 <= 0 and 2*p1 - 7 >= 0 and 100*n - 10*td - 2500*z - 46519 <= 0

 and 100*n - 10*td - 2500*z - 36519 >= 0

 and 3575*n - 380*td - 95000*z - 1387722 <= 0

 and 80*i2 + 250*p1 + 2*q - 1457 = 0 and 200*i2 - 10*q - td + 385 = 0 and (

(td - 700 < 0 and td - 400 >= 0 and 600*n + 15*td - 5000*z - 372364 = 0)

 or (td - 700 >= 0 and 450*n - 95*td - 3750*z - 204898 = 0))) or (q >= 0

 and q - 40 <= 0 and n >= 0 and i2 = 0

 and (2*p1 - 7 >= 0 or 250*p1 + 2*q - 577 = 0) and ((z = 0 and td = 0)

 or (td - 700 < 0 and td - 400 >= 0 and 3*td + 400*z - 5320 = 0)

 or (td - 700 >= 0 and 2*td - 300*z + 1015 = 0)) and ((250*p1 + 2*q - 1697 < 0

 and 250*p1 + 2*q - 1457 > 0

 and 500000*n + 33593750*p1 + 268750*q - 50000*td - 10000000*z - 402109359 = 0) 

or (250*p1 + 2*q - 1457 <= 0 and 250*p1 + 2*q - 1377 > 0

 and 2000*n - 240250*p1 - 1922*q - 200*td - 50000*z + 669797 = 0) or (

250*p1 + 2*q - 1377 <= 0 and 250*p1 + 2*q - 1057 > 0

 and 50*n - 4625*p1 - 37*q - 5*td - 750*z + 4647 = 0))) or (q >= 0

 and q - 40 <= 0 and n >= 0 and i2 = 0 and ((z = 0 and td = 0)

 or (td - 700 < 0 and td - 400 >= 0 and 3*td + 400*z - 5320 = 0)

 or (td - 700 >= 0 and 2*td - 300*z + 1015 = 0)) and (

(2*p1 - 7 < 0 and 20*n - 2*td - 500*z + 1153 = 0) or (2*p1 - 7 >= 0

 and 2000*n - 240250*p1 - 1922*q - 200*td - 50000*z + 669797 = 0)) and ((

20*n - 2*td - 500*z - 6535 <= 0 and 100*n - 10*td - 2500*z - 17299 > 0

 and 4420*n - 442*td + 81700*z - 3170191 = 0)

 or (20*n - 2*td - 500*z - 6535 > 0 and 100*n - 10*td - 2500*z - 36519 <= 0) or 

(100*n - 10*td - 2500*z - 48051 < 0 and 100*n - 10*td - 2500*z - 36519 > 0

 and 187312500*n - 18731250*td - 4082187500*z - 74105780531 = 0))) or (q >= 0

 and q - 40 <= 0 and n >= 0 and i2 = 0 and ((z = 0 and td = 0)

 or (td - 700 < 0 and td - 400 >= 0 and 3*td + 400*z - 5320 = 0)

 or (td - 700 >= 0 and 2*td - 300*z + 1015 = 0)) and (

(2*p1 - 7 < 0 and 20*n - 2*td - 300*z - 2411 = 0)

 or (2*p1 - 7 >= 0 and 50*n - 4625*p1 - 37*q - 5*td - 750*z + 4647 = 0)) and ((

20*n - 2*td - 300*z - 10699 < 0 and 20*n - 2*td - 300*z - 8923 > 0

 and 31937500*n - 3193750*td - 571562500*z - 13629165033 = 0) or (

20*n - 2*td - 300*z - 8923 <= 0 and 20*n - 2*td - 300*z - 8331 > 0

 and 4420*n - 442*td + 81700*z - 3170191 = 0)

 or (20*n - 2*td - 300*z - 8331 <= 0 and 20*n - 2*td - 300*z - 5963 > 0))) or (

q >= 0 and q - 40 <= 0 and n >= 0 and i2 = 0 and ((z = 0 and td = 0)

 or (td - 700 < 0 and td - 400 >= 0 and 3*td + 400*z - 5320 = 0)

 or (td - 700 >= 0 and 2*td - 300*z + 1015 = 0)) and (

(2*p1 - 7 < 0 and 62500*n - 6250*td - 1250000*z - 40571873 = 0) or (

2*p1 - 7 >= 0

 and 500000*n + 33593750*p1 + 268750*q - 50000*td - 10000000*z - 402109359 = 0))

 and ((62500*n - 6250*td - 1250000*z - 32509373 < 0

 and 62500*n - 6250*td - 1250000*z - 27134373 >= 0

 and 31937500*n - 3193750*td - 571562500*z - 13629165033 = 0) or (

62500*n - 6250*td - 1250000*z - 27134373 < 0

 and 62500*n - 6250*td - 1250000*z - 25790623 >= 0

 and 187312500*n - 18731250*td - 4082187500*z - 74105780531 = 0) or (

62500*n - 6250*td - 1250000*z - 25790623 < 0

 and 62500*n - 6250*td - 1250000*z - 21759373 > 0))) or (q >= 0 and q - 40 <= 0

 and n >= 0 and 200*i2 - 10*q - td + 385 = 0

 and (2*p1 - 7 >= 0 or 80*i2 + 250*p1 + 2*q - 577 = 0) and (

(td - 700 < 0 and td - 400 >= 0 and 3*td + 400*z - 6130 = 0)

 or (td - 700 >= 0 and 4*td - 600*z + 3245 = 0)) and ((

80*i2 + 250*p1 + 2*q - 1697 < 0 and 80*i2 + 250*p1 + 2*q - 1457 > 0 and 

10750000*i2 + 500000*n + 33593750*p1 + 268750*q - 50000*td - 10000000*z

 - 402109359 = 0) or (80*i2 + 250*p1 + 2*q - 1457 <= 0

 and 80*i2 + 250*p1 + 2*q - 1377 > 0

 and 76880*i2 - 2000*n + 240250*p1 + 1922*q + 200*td + 50000*z - 669797 = 0) or 

(80*i2 + 250*p1 + 2*q - 1377 <= 0 and 80*i2 + 250*p1 + 2*q - 1057 > 0

 and 1480*i2 - 50*n + 4625*p1 + 37*q + 5*td + 750*z - 4647 = 0))) or (q >= 0

 and q - 40 <= 0 and n >= 0 and 200*i2 - 10*q - td + 385 = 0 and (

(td - 700 < 0 and td - 400 >= 0 and 3*td + 400*z - 6130 = 0)

 or (td - 700 >= 0 and 4*td - 600*z + 3245 = 0)) and (

(2*p1 - 7 < 0 and 20*n - 2*td - 500*z + 1153 = 0) or (2*p1 - 7 >= 0

 and 76880*i2 - 2000*n + 240250*p1 + 1922*q + 200*td + 50000*z - 669797 = 0)) 

and ((20*n - 2*td - 500*z - 6535 <= 0 and 100*n - 10*td - 2500*z - 17299 > 0

 and 4420*n - 442*td + 81700*z - 3170191 = 0)

 or (20*n - 2*td - 500*z - 6535 > 0 and 100*n - 10*td - 2500*z - 36519 <= 0) or 

(100*n - 10*td - 2500*z - 48051 < 0 and 100*n - 10*td - 2500*z - 36519 > 0

 and 187312500*n - 18731250*td - 4082187500*z - 74105780531 = 0))) or (q >= 0

 and q - 40 <= 0 and n >= 0 and 200*i2 - 10*q - td + 385 = 0 and (

(td - 700 < 0 and td - 400 >= 0 and 3*td + 400*z - 6130 = 0)

 or (td - 700 >= 0 and 4*td - 600*z + 3245 = 0)) and (

(2*p1 - 7 < 0 and 20*n - 2*td - 300*z - 2411 = 0) or (2*p1 - 7 >= 0

 and 1480*i2 - 50*n + 4625*p1 + 37*q + 5*td + 750*z - 4647 = 0)) and ((

20*n - 2*td - 300*z - 10699 < 0 and 20*n - 2*td - 300*z - 8923 > 0

 and 31937500*n - 3193750*td - 571562500*z - 13629165033 = 0) or (

20*n - 2*td - 300*z - 8923 <= 0 and 20*n - 2*td - 300*z - 8331 > 0

 and 4420*n - 442*td + 81700*z - 3170191 = 0)

 or (20*n - 2*td - 300*z - 8331 <= 0 and 20*n - 2*td - 300*z - 5963 > 0))) or (

q >= 0 and q - 40 <= 0 and n >= 0 and 200*i2 - 10*q - td + 385 = 0 and (

(td - 700 < 0 and td - 400 >= 0 and 3*td + 400*z - 6130 = 0)

 or (td - 700 >= 0 and 4*td - 600*z + 3245 = 0)) and (

(2*p1 - 7 < 0 and 62500*n - 6250*td - 1250000*z - 40571873 = 0) or (

2*p1 - 7 >= 0 and 10750000*i2 + 500000*n + 33593750*p1 + 268750*q - 50000*td

 - 10000000*z - 402109359 = 0)) and ((

62500*n - 6250*td - 1250000*z - 32509373 < 0

 and 62500*n - 6250*td - 1250000*z - 27134373 >= 0

 and 31937500*n - 3193750*td - 571562500*z - 13629165033 = 0) or (

62500*n - 6250*td - 1250000*z - 27134373 < 0

 and 62500*n - 6250*td - 1250000*z - 25790623 >= 0

 and 187312500*n - 18731250*td - 4082187500*z - 74105780531 = 0) or (

62500*n - 6250*td - 1250000*z - 25790623 < 0

 and 62500*n - 6250*td - 1250000*z - 21759373 > 0))) or (q >= 0 and q - 40 <= 0

 and 50*n - 4625*p1 - 37*q - 5*td - 750*z - 353 <= 0

 and 50*n - 4625*p1 - 37*q - 5*td - 750*z + 4647 >= 0

 and 3575*n - 351500*p1 - 2812*q - 380*td - 57000*z + 353172 <= 0 and i2 = 0

 and (2*p1 - 7 >= 0 or 250*p1 + 2*q - 577 = 0) and ((z = 0 and td = 0)

 or (td - 700 < 0 and td - 400 >= 0 and 3*td + 400*z - 5320 = 0)

 or (td - 700 >= 0 and 2*td - 300*z + 1015 = 0)) and ((250*p1 + 2*q - 1697 < 0

 and 250*p1 + 2*q - 1457 > 0

 and 79843750*p1 + 638750*q - 2500000*z - 448579359 = 0) or (

250*p1 + 2*q - 1457 <= 0 and 250*p1 + 2*q - 1377 > 0

 and 55250*p1 + 442*q + 20000*z - 483917 = 0)

 or (250*p1 + 2*q - 1377 <= 0 and 250*p1 + 2*q - 1057 > 0))) or (q >= 0

 and q - 40 <= 0

 and 2000*n - 240250*p1 - 1922*q - 200*td - 50000*z + 469797 <= 0

 and 2000*n - 240250*p1 - 1922*q - 200*td - 50000*z + 669797 >= 0

 and 35750*n - 4564750*p1 - 36518*q - 3800*td - 950000*z + 12726143 <= 0

 and i2 = 0 and (2*p1 - 7 >= 0 or 250*p1 + 2*q - 577 = 0) and (

(z = 0 and td = 0)

 or (td - 700 < 0 and td - 400 >= 0 and 3*td + 400*z - 5320 = 0)

 or (td - 700 >= 0 and 2*td - 300*z + 1015 = 0)) and ((250*p1 + 2*q - 1697 < 0

 and 250*p1 + 2*q - 1457 > 0

 and 93656250*p1 + 749250*q + 2500000*z - 569558609 = 0)

 or (250*p1 + 2*q - 1457 <= 0 and 250*p1 + 2*q - 1377 > 0) or (

250*p1 + 2*q - 1377 <= 0 and 250*p1 + 2*q - 1057 > 0

 and 55250*p1 + 442*q + 20000*z - 483917 = 0))) or (q >= 0 and q - 40 <= 0

 and 4420*n - 442*td + 81700*z - 3612191 <= 0

 and 4420*n - 442*td + 81700*z - 3170191 >= 0

 and 158015*n - 16796*td + 3104600*z - 120467258 <= 0 and i2 = 0 and (

108437500*z - 865858649 = 0 or (50*z - 449 < 0 and 125*z - 1012 >= 0)

 or (50*z - 449 >= 0 and 250*z - 3129 < 0)) and ((z = 0 and td = 0)

 or (td - 700 < 0 and td - 400 >= 0 and 3*td + 400*z - 5320 = 0)

 or (td - 700 >= 0 and 2*td - 300*z + 1015 = 0)) and (

(50*z - 891 = 0 and 2*p1 - 7 < 0)

 or (2*p1 - 7 >= 0 and 55250*p1 + 442*q + 20000*z - 483917 = 0))) or (q >= 0

 and q - 40 <= 0 and 4420*n - 442*td + 81700*z - 3612191 <= 0

 and 4420*n - 442*td + 81700*z - 3170191 >= 0

 and 158015*n - 16796*td + 3104600*z - 120467258 <= 0

 and 200*i2 - 10*q - td + 385 = 0 and (108437500*z - 865858649 = 0

 or (50*z - 449 < 0 and 125*z - 1012 >= 0)

 or (50*z - 449 >= 0 and 250*z - 3129 < 0)) and (

(50*z - 891 = 0 and 2*p1 - 7 < 0)

 or (2*p1 - 7 >= 0 and 17680*i2 + 55250*p1 + 442*q + 20000*z - 483917 = 0)) and 

((td - 700 < 0 and td - 400 >= 0 and 26520*n + 663*td + 932200*z - 25794796 = 0)

 or (td - 700 >= 0 and 19890*n - 4199*td + 699150*z - 16058722 = 0))) or (q >= 0

 and q - 40 <= 0

 and 500000*n + 33593750*p1 + 268750*q - 50000*td - 10000000*z - 452109359 <= 0

 and 500000*n + 33593750*p1 + 268750*q - 50000*td - 10000000*z - 402109359 >= 0 

and 8937500*n + 638281250*p1 + 5106250*q - 950000*td - 190000000*z - 7640077821

 <= 0 and i2 = 0 and (2*p1 - 7 >= 0 or 250*p1 + 2*q - 577 = 0) and (

(z = 0 and td = 0)

 or (td - 700 < 0 and td - 400 >= 0 and 3*td + 400*z - 5320 = 0)

 or (td - 700 >= 0 and 2*td - 300*z + 1015 = 0)) and (

(250*p1 + 2*q - 1697 < 0 and 250*p1 + 2*q - 1457 > 0) or (

250*p1 + 2*q - 1457 <= 0 and 250*p1 + 2*q - 1377 > 0

 and 93656250*p1 + 749250*q + 2500000*z - 569558609 = 0) or (

250*p1 + 2*q - 1377 <= 0 and 250*p1 + 2*q - 1057 > 0

 and 79843750*p1 + 638750*q - 2500000*z - 448579359 = 0))) or (q >= 0

 and q - 40 <= 0 and 31937500*n - 3193750*td - 571562500*z - 16822915033 <= 0

 and 31937500*n - 3193750*td - 571562500*z - 13629165033 >= 0

 and 1141765625*n - 121362500*td - 21719375000*z - 517908271254 <= 0 and i2 = 0 

and ((z = 0 and td = 0)

 or (td - 700 < 0 and td - 400 >= 0 and 3*td + 400*z - 5320 = 0)

 or (td - 700 >= 0 and 2*td - 300*z + 1015 = 0)) and (

(78125*z - 523438 > 0 and 156250*z - 5837501 < 0)

 or (156250*z + 549999 <= 0 and 156250*z + 6937499 > 0)) and (

(156250*z + 16518749 = 0 and 2*p1 - 7 < 0)

 or (2*p1 - 7 >= 0 and 79843750*p1 + 638750*q - 2500000*z - 448579359 = 0))) or 

(q >= 0 and q - 40 <= 0

 and 31937500*n - 3193750*td - 571562500*z - 16822915033 <= 0

 and 31937500*n - 3193750*td - 571562500*z - 13629165033 >= 0

 and 1141765625*n - 121362500*td - 21719375000*z - 517908271254 <= 0

 and 200*i2 - 10*q - td + 385 = 0 and (

(78125*z - 523438 > 0 and 156250*z - 5837501 < 0)

 or (156250*z + 549999 <= 0 and 156250*z + 6937499 > 0)) and (

(156250*z + 16518749 = 0 and 2*p1 - 7 < 0) or (2*p1 - 7 >= 0

 and 25550000*i2 + 79843750*p1 + 638750*q - 2500000*z - 448579359 = 0)) and ((

td - 700 < 0 and td - 400 >= 0

 and 191625000*n + 4790625*td - 235625000*z - 130719208948 = 0) or (

td - 700 >= 0 and 143718750*n - 30340625*td - 176718750*z - 74285891086 = 0))) 

or (q >= 0 and q - 40 <= 0

 and 187312500*n - 18731250*td - 4082187500*z - 92837030531 <= 0

 and 187312500*n - 18731250*td - 4082187500*z - 74105780531 >= 0

 and 6696421875*n - 711787500*td - 155123125000*z - 2816019660178 <= 0

 and i2 = 0 and ((z = 0 and td = 0)

 or (td - 700 < 0 and td - 400 >= 0 and 3*td + 400*z - 5320 = 0)

 or (td - 700 >= 0 and 2*td - 300*z + 1015 = 0)) and (

(78125*z - 741562 < 0 and 156250*z + 4136251 > 0)

 or (78125*z - 741562 >= 0 and 156250*z - 3356249 < 0)) and (

(156250*z - 22087499 = 0 and 2*p1 - 7 < 0)

 or (2*p1 - 7 >= 0 and 93656250*p1 + 749250*q + 2500000*z - 569558609 = 0))) or 

(q >= 0 and q - 40 <= 0

 and 187312500*n - 18731250*td - 4082187500*z - 92837030531 <= 0

 and 187312500*n - 18731250*td - 4082187500*z - 74105780531 >= 0

 and 6696421875*n - 711787500*td - 155123125000*z - 2816019660178 <= 0

 and 200*i2 - 10*q - td + 385 = 0 and (

(78125*z - 741562 < 0 and 156250*z + 4136251 > 0)

 or (78125*z - 741562 >= 0 and 156250*z - 3356249 < 0)) and (

(156250*z - 22087499 = 0 and 2*p1 - 7 < 0) or (2*p1 - 7 >= 0

 and 29970000*i2 + 93656250*p1 + 749250*q + 2500000*z - 569558609 = 0)) and ((

td - 700 < 0 and td - 400 >= 0

 and 374625000*n + 9365625*td - 1920625000*z - 243897029812 = 0)

 or (td - 700 >= 0 and 93656250*n - 19771875*td - 480156250*z - 45494960578 = 0)

)) or (q >= 0 and q - 40 <= 0 and 200*i2 - 10*q - td + 385 = 0

 and 1480*i2 - 50*n + 4625*p1 + 37*q + 5*td + 750*z - 4647 <= 0

 and 1480*i2 - 50*n + 4625*p1 + 37*q + 5*td + 750*z + 353 >= 0

 and 112480*i2 - 3575*n + 351500*p1 + 2812*q + 380*td + 57000*z - 353172 >= 0

 and (2*p1 - 7 >= 0 or 80*i2 + 250*p1 + 2*q - 577 = 0) and ((td - 700 < 0

 and td - 400 >= 0

 and 17760*i2 - 600*n + 55500*p1 + 444*q - 15*td - 1000*z + 97486 = 0) or (

td - 700 >= 0

 and 26640*i2 - 900*n + 83250*p1 + 666*q + 190*td - 1500*z - 2521 = 0)) and ((

80*i2 + 250*p1 + 2*q - 1697 < 0 and 80*i2 + 250*p1 + 2*q - 1457 > 0

 and 25550000*i2 + 79843750*p1 + 638750*q - 2500000*z - 448579359 = 0) or (

80*i2 + 250*p1 + 2*q - 1457 <= 0 and 80*i2 + 250*p1 + 2*q - 1377 > 0

 and 17680*i2 + 55250*p1 + 442*q + 20000*z - 483917 = 0)

 or (80*i2 + 250*p1 + 2*q - 1377 <= 0 and 80*i2 + 250*p1 + 2*q - 1057 > 0))) or 

(q >= 0 and q - 40 <= 0 and 200*i2 - 10*q - td + 385 = 0

 and 76880*i2 - 2000*n + 240250*p1 + 1922*q + 200*td + 50000*z - 669797 <= 0

 and 76880*i2 - 2000*n + 240250*p1 + 1922*q + 200*td + 50000*z - 469797 >= 0 and

 1460720*i2 - 35750*n + 4564750*p1 + 36518*q + 3800*td + 950000*z - 12726143

 >= 0 and (2*p1 - 7 >= 0 or 80*i2 + 250*p1 + 2*q - 577 = 0) and ((td - 700 < 0

 and td - 400 >= 0

 and 230640*i2 - 6000*n + 720750*p1 + 5766*q - 150*td + 50000*z - 476891 = 0) or

 (td - 700 >= 0 and 

691920*i2 - 18000*n + 2162250*p1 + 17298*q + 3800*td + 150000*z - 4405673 = 0)) 

and ((80*i2 + 250*p1 + 2*q - 1697 < 0 and 80*i2 + 250*p1 + 2*q - 1457 > 0

 and 29970000*i2 + 93656250*p1 + 749250*q + 2500000*z - 569558609 = 0)

 or (80*i2 + 250*p1 + 2*q - 1457 <= 0 and 80*i2 + 250*p1 + 2*q - 1377 > 0) or (

80*i2 + 250*p1 + 2*q - 1377 <= 0 and 80*i2 + 250*p1 + 2*q - 1057 > 0

 and 17680*i2 + 55250*p1 + 442*q + 20000*z - 483917 = 0))) or (q >= 0

 and q - 40 <= 0 and 200*i2 - 10*q - td + 385 = 0 and 10750000*i2 + 500000*n

 + 33593750*p1 + 268750*q - 50000*td - 10000000*z - 452109359 <= 0 and 

10750000*i2 + 500000*n + 33593750*p1 + 268750*q - 50000*td - 10000000*z

 - 402109359 >= 0 and 204250000*i2 + 8937500*n + 638281250*p1 + 5106250*q

 - 950000*td - 190000000*z - 7640077821 <= 0

 and (2*p1 - 7 >= 0 or 80*i2 + 250*p1 + 2*q - 577 = 0) and ((td - 700 < 0

 and td - 400 >= 0 and 32250000*i2 + 1500000*n + 100781250*p1 + 806250*q

 + 37500*td - 5000000*z - 1589453077 = 0) or (td - 700 >= 0 and 96750000*i2

 + 4500000*n + 302343750*p1 + 2418750*q - 950000*td - 15000000*z - 4024609231

 = 0)) and (

(80*i2 + 250*p1 + 2*q - 1697 < 0 and 80*i2 + 250*p1 + 2*q - 1457 > 0) or (

80*i2 + 250*p1 + 2*q - 1457 <= 0 and 80*i2 + 250*p1 + 2*q - 1377 > 0

 and 29970000*i2 + 93656250*p1 + 749250*q + 2500000*z - 569558609 = 0) or (

80*i2 + 250*p1 + 2*q - 1377 <= 0 and 80*i2 + 250*p1 + 2*q - 1057 > 0

 and 25550000*i2 + 79843750*p1 + 638750*q - 2500000*z - 448579359 = 0))))))


end;

