off rlabout;



rlset reals;


{}


testseries2 :=
td = 0 and i2 = 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) and (400*q + 9*td - 20050 <= 0 and 20*n - 50*q - 2*td - 300*z - 8331
= 0 or 400*q + 9*td - 20050 > 0 and 160*n - 7*td - 2400*z - 86698 = 0)
or td = 0 and i2 = 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) and (400*q + 9*td - 20050 <= 0 and 20*n -
50*q - 2*td - 300*z - 8923 = 0 or 400*q + 9*td - 20050 > 0 and 160*n - 7
*td - 2400*z - 91434 = 0) or td = 0 and i2 = 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) and (400*q + 9*td -
20050 <= 0 and 1480*i2 - 50*n + 4625*p1 + 162*q + 5*td + 750*z - 4647 =
0 or 400*q + 9*td - 20050 > 0 and 23680*i2 - 800*n + 74000*p1 + 592*q +
35*td + 12000*z + 25898 = 0) or td = 0 and i2 = 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) and (400*q + 9*
td - 20050 <= 0 and 20*n - 50*q - 2*td - 500*z - 6535 = 0 or 400*q + 9*
td - 20050 > 0 and 160*n - 7*td - 4000*z - 72330 = 0) or td = 0 and i2 =
 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) and (400*q + 9*td - 20050 <= 0 and 4420*n - 11050*q -
442*td + 81700*z - 3170191 = 0 or 400*q + 9*td - 20050 > 0 and 35360*n -
 1547*td + 653600*z - 29792578 = 0) or td = 0 and i2 = 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) and (400*q + 9*td -
20050 <= 0 and 100*n - 250*q - 10*td - 2500*z - 36519 = 0 or 400*q + 9*
td - 20050 > 0 and 800*n - 35*td - 20000*z - 392402 = 0) or td = 0 and
i2 = 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) and (400*q + 9*
td - 20050 <= 0 and 76880*i2 - 2000*n + 240250*p1 + 6922*q + 200*td +
50000*z - 669797 = 0 or 400*q + 9*td - 20050 > 0 and 153760*i2 - 4000*n
+ 480500*p1 + 3844*q + 175*td + 100000*z - 838344 = 0) or td = 0 and i2
= 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) and (
400*q + 9*td - 20050 <= 0 and 31937500*n - 79843750*q - 3193750*td -
571562500*z - 13629165033 = 0 or 400*q + 9*td - 20050 > 0 and 255500000*
n - 11178125*td - 4572500000*z - 141050664014 = 0) or td = 0 and i2 = 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) and (400*q + 9*
td - 20050 <= 0 and 187312500*n - 468281250*q - 18731250*td - 4082187500
*z - 74105780531 = 0 or 400*q + 9*td - 20050 > 0 and 1498500000*n -
65559375*td - 32657500000*z - 780627025498 = 0) or td = 0 and i2 = 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) and (400*q + 9*td - 20050 <= 0 and 10750000
*i2 + 500000*n + 33593750*p1 - 981250*q - 50000*td - 10000000*z -
402109359 = 0 or 400*q + 9*td - 20050 > 0 and 10750000*i2 + 500000*n +
33593750*p1 + 268750*q - 21875*td - 10000000*z - 464765609 = 0) or td =
0 and 400*q + 9*td - 20050 <= 0 and i2 = 0 and 9*n - 380*q >= 0 and q -
40 <= 0 and q >= 0 and 20*n - 50*q - 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 td = 0 and 400*q + 9
*td - 20050 <= 0 and i2 = 0 and 9*n - 380*q >= 0 and q - 40 <= 0 and q
>= 0 and (20*n - 50*q - 2*td - 300*z - 5963 > 0 and 20*n - 50*q - 2*td -
 300*z - 8331 <= 0 or 20*n - 50*q - 2*td - 300*z - 8331 > 0 and 20*n -
50*q - 2*td - 300*z - 8923 <= 0 and 4420*n - 11050*q - 442*td + 81700*z
- 3170191 = 0 or 20*n - 50*q - 2*td - 300*z - 8923 > 0 and 20*n - 50*q -
 2*td - 300*z - 10699 < 0 and 31937500*n - 79843750*q - 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 - 50*q - 2*
td - 300*z - 2411 = 0 or 2*p1 - 7 >= 0 and 1480*i2 - 50*n + 4625*p1 +
162*q + 5*td + 750*z - 4647 = 0) or td = 0 and 400*q + 9*td - 20050 <= 0
 and i2 = 0 and 9*n - 380*q >= 0 and q - 40 <= 0 and q >= 0 and 100*n -
250*q - 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 td = 0 and 400*q + 9*td - 20050 <= 0 and i2 = 0
and 9*n - 380*q >= 0 and q - 40 <= 0 and q >= 0 and (100*n - 250*q - 10*
td - 2500*z - 17299 > 0 and 20*n - 50*q - 2*td - 500*z - 6535 <= 0 and
4420*n - 11050*q - 442*td + 81700*z - 3170191 = 0 or 20*n - 50*q - 2*td
- 500*z - 6535 > 0 and 100*n - 250*q - 10*td - 2500*z - 36519 <= 0 or
100*n - 250*q - 10*td - 2500*z - 36519 > 0 and 100*n - 250*q - 10*td -
2500*z - 48051 < 0 and 187312500*n - 468281250*q - 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 - 50*q - 2*td - 500*
z + 1153 = 0 or 2*p1 - 7 >= 0 and 76880*i2 - 2000*n + 240250*p1 + 6922*q
 + 200*td + 50000*z - 669797 = 0) or td = 0 and 400*q + 9*td - 20050 <=
0 and i2 = 0 and 9*n - 380*q >= 0 and q - 40 <= 0 and q >= 0 and (62500*
n - 156250*q - 6250*td - 1250000*z - 32509373 < 0 and 62500*n - 156250*q
 - 6250*td - 1250000*z - 27134373 >= 0 and 31937500*n - 79843750*q -
3193750*td - 571562500*z - 13629165033 = 0 or 62500*n - 156250*q - 6250*
td - 1250000*z - 27134373 < 0 and 62500*n - 156250*q - 6250*td - 1250000
*z - 25790623 >= 0 and 187312500*n - 468281250*q - 18731250*td - 4082187500
*z - 74105780531 = 0 or 62500*n - 156250*q - 6250*td - 1250000*z -
25790623 < 0 and 62500*n - 156250*q - 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 - 156250*q - 6250*td - 1250000*z -
40571873 = 0 or 2*p1 - 7 >= 0 and 10750000*i2 + 500000*n + 33593750*p1 -
 981250*q - 50000*td - 10000000*z - 402109359 = 0) or td = 0 and 400*q +
 9*td - 20050 <= 0 and i2 = 0 and 9*n - 380*q >= 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 + 162*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 + 6922*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 - 981250*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 td = 0 and 400*q + 9*td - 20050 >= 0
and i2 = 0 and 180*n + 171*td - 380950 >= 0 and td - 450 >= 0 and 9*td -
 20050 <= 0 and q - 40 <= 0 and q >= 0 and 160*n - 7*td - 2400*z - 86698
 = 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 td = 0
and 400*q + 9*td - 20050 >= 0 and i2 = 0 and 180*n + 171*td - 380950 >=
0 and td - 450 >= 0 and 9*td - 20050 <= 0 and q - 40 <= 0 and q >= 0 and
 (160*n - 7*td - 2400*z - 67754 > 0 and 160*n - 7*td - 2400*z - 86698 <=
 0 or 160*n - 7*td - 2400*z - 86698 > 0 and 160*n - 7*td - 2400*z -
91434 <= 0 and 35360*n - 1547*td + 653600*z - 29792578 = 0 or 160*n - 7*
td - 2400*z - 91434 > 0 and 160*n - 7*td - 2400*z - 105642 < 0 and
255500000*n - 11178125*td - 4572500000*z - 141050664014 = 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 160*n - 7*td - 2400*z - 39338 = 0 or 2*p1 - 7 >= 0 and
23680*i2 - 800*n + 74000*p1 + 592*q + 35*td + 12000*z + 25898 = 0) or td
 = 0 and 400*q + 9*td - 20050 >= 0 and i2 = 0 and 180*n + 171*td -
380950 >= 0 and td - 450 >= 0 and 9*td - 20050 <= 0 and q - 40 <= 0 and
q >= 0 and 800*n - 35*td - 20000*z - 392402 = 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 td = 0 and 400*q + 9*td - 20050 >= 0
 and i2 = 0 and 180*n + 171*td - 380950 >= 0 and td - 450 >= 0 and 9*td
- 20050 <= 0 and q - 40 <= 0 and q >= 0 and (800*n - 35*td - 20000*z -
238642 > 0 and 160*n - 7*td - 4000*z - 72330 <= 0 and 35360*n - 1547*td
+ 653600*z - 29792578 = 0 or 160*n - 7*td - 4000*z - 72330 > 0 and 800*n
 - 35*td - 20000*z - 392402 <= 0 or 800*n - 35*td - 20000*z - 392402 > 0
 and 800*n - 35*td - 20000*z - 484658 < 0 and 1498500000*n - 65559375*td
 - 32657500000*z - 780627025498 = 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 160*n - 7*
td - 4000*z - 10826 = 0 or 2*p1 - 7 >= 0 and 153760*i2 - 4000*n + 480500
*p1 + 3844*q + 175*td + 100000*z - 838344 = 0) or td = 0 and 400*q + 9*
td - 20050 >= 0 and i2 = 0 and 180*n + 171*td - 380950 >= 0 and td - 450
 >= 0 and 9*td - 20050 <= 0 and q - 40 <= 0 and q >= 0 and (500000*n -
21875*td - 10000000*z - 322731234 < 0 and 500000*n - 21875*td - 10000000
*z - 279731234 >= 0 and 255500000*n - 11178125*td - 4572500000*z - 141050664014
 = 0 or 500000*n - 21875*td - 10000000*z - 279731234 < 0 and 500000*n -
21875*td - 10000000*z - 268981234 >= 0 and 1498500000*n - 65559375*td - 32657500000
*z - 780627025498 = 0 or 500000*n - 21875*td - 10000000*z - 268981234 <
0 and 500000*n - 21875*td - 10000000*z - 236731234 > 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 500000*n - 21875*td - 10000000*z - 387231234 = 0 or 2*p1 - 7 >=
 0 and 10750000*i2 + 500000*n + 33593750*p1 + 268750*q - 21875*td -
10000000*z - 464765609 = 0) or td = 0 and 400*q + 9*td - 20050 >= 0 and
i2 = 0 and 180*n + 171*td - 380950 >= 0 and td - 450 >= 0 and 9*td -
20050 <= 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 23680*i2 - 800*n + 74000*p1
+ 592*q + 35*td + 12000*z + 25898 = 0 or 80*i2 + 250*p1 + 2*q - 1377 > 0
 and 80*i2 + 250*p1 + 2*q - 1457 <= 0 and 153760*i2 - 4000*n + 480500*p1
 + 3844*q + 175*td + 100000*z - 838344 = 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 - 21875*td - 10000000*z - 464765609 = 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 td = 0 and i2 = 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) and (400*q + 9*td - 20050 <= 0 and q = 0 or 400*q + 9*td - 20050
 > 0 and 9*td - 20050 = 0) or td = 0 and i2 = 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) and (400*q + 9*td - 20050 <= 0
 and q = 0 or 400*q + 9*td - 20050 > 0 and 9*td - 20050 = 0) or td = 0
and i2 = 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) and (400*q + 9*td - 20050 <= 0 and q = 0 or 400*q + 9*td - 20050 > 0
 and 9*td - 20050 = 0) or td = 0 and i2 = 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)
and (400*q + 9*td - 20050 <= 0 and q = 0 or 400*q + 9*td - 20050 > 0 and
 9*td - 20050 = 0) or td = 0 and i2 = 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) and (400*q + 9*td
 - 20050 <= 0 and q = 0 or 400*q + 9*td - 20050 > 0 and 9*td - 20050 = 0
) or td = 0 and i2 = 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) and (400*q + 9*td - 20050 <= 0 and q = 0 or 400*q + 9*td - 20050
> 0 and 9*td - 20050 = 0) or 6*n - 5*td < 0 and i2 = 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) and (400*q + 9*td - 20050 <= 0
and 20*n - 50*q - 2*td - 300*z - 8331 = 0 or 400*q + 9*td - 20050 > 0
and 160*n - 7*td - 2400*z - 86698 = 0) or 6*n - 5*td < 0 and i2 = 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) and (400*q + 9*td - 20050 <= 0 and 20*n - 50*q - 2*td - 300*z - 8923
= 0 or 400*q + 9*td - 20050 > 0 and 160*n - 7*td - 2400*z - 91434 = 0)
or 6*n - 5*td < 0 and i2 = 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) and (400*q + 9*td - 20050 <= 0 and 1480*i2
- 50*n + 4625*p1 + 162*q + 5*td + 750*z - 4647 = 0 or 400*q + 9*td -
20050 > 0 and 23680*i2 - 800*n + 74000*p1 + 592*q + 35*td + 12000*z +
25898 = 0) or 6*n - 5*td < 0 and i2 = 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) and (400*q + 9*td - 20050 <=
 0 and 20*n - 50*q - 2*td - 500*z - 6535 = 0 or 400*q + 9*td - 20050 > 0
 and 160*n - 7*td - 4000*z - 72330 = 0) or 6*n - 5*td < 0 and i2 = 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) and (400*q + 9*td - 20050 <= 0 and 4420*n - 11050*q - 442*td +
81700*z - 3170191 = 0 or 400*q + 9*td - 20050 > 0 and 35360*n - 1547*td
+ 653600*z - 29792578 = 0) or 6*n - 5*td < 0 and i2 = 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) and (400*q + 9*td -
20050 <= 0 and 100*n - 250*q - 10*td - 2500*z - 36519 = 0 or 400*q + 9*
td - 20050 > 0 and 800*n - 35*td - 20000*z - 392402 = 0) or 6*n - 5*td <
 0 and i2 = 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) and (400*q + 9*
td - 20050 <= 0 and 76880*i2 - 2000*n + 240250*p1 + 6922*q + 200*td +
50000*z - 669797 = 0 or 400*q + 9*td - 20050 > 0 and 153760*i2 - 4000*n
+ 480500*p1 + 3844*q + 175*td + 100000*z - 838344 = 0) or 6*n - 5*td < 0
 and i2 = 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) and (
400*q + 9*td - 20050 <= 0 and 31937500*n - 79843750*q - 3193750*td -
571562500*z - 13629165033 = 0 or 400*q + 9*td - 20050 > 0 and 255500000*
n - 11178125*td - 4572500000*z - 141050664014 = 0) or 6*n - 5*td < 0 and
 i2 = 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) and (
400*q + 9*td - 20050 <= 0 and 187312500*n - 468281250*q - 18731250*td - 4082187500
*z - 74105780531 = 0 or 400*q + 9*td - 20050 > 0 and 1498500000*n -
65559375*td - 32657500000*z - 780627025498 = 0) or 6*n - 5*td < 0 and i2
 = 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) and (400*q + 9*td - 20050 <= 0 and
10750000*i2 + 500000*n + 33593750*p1 - 981250*q - 50000*td - 10000000*z
- 402109359 = 0 or 400*q + 9*td - 20050 > 0 and 10750000*i2 + 500000*n +
 33593750*p1 + 268750*q - 21875*td - 10000000*z - 464765609 = 0) or 6*n
- 5*td < 0 and 400*q + 9*td - 20050 <= 0 and i2 = 0 and 9*n - 380*q >= 0
 and q - 40 <= 0 and q >= 0 and 20*n - 50*q - 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 6*n - 5*td <
 0 and 400*q + 9*td - 20050 <= 0 and i2 = 0 and 9*n - 380*q >= 0 and q -
 40 <= 0 and q >= 0 and (20*n - 50*q - 2*td - 300*z - 5963 > 0 and 20*n
- 50*q - 2*td - 300*z - 8331 <= 0 or 20*n - 50*q - 2*td - 300*z - 8331 >
 0 and 20*n - 50*q - 2*td - 300*z - 8923 <= 0 and 4420*n - 11050*q - 442
*td + 81700*z - 3170191 = 0 or 20*n - 50*q - 2*td - 300*z - 8923 > 0 and
 20*n - 50*q - 2*td - 300*z - 10699 < 0 and 31937500*n - 79843750*q -
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 - 50*q - 2*td - 300*z - 2411 = 0 or 2*p1 - 7 >= 0 and 1480*i2 - 50*
n + 4625*p1 + 162*q + 5*td + 750*z - 4647 = 0) or 6*n - 5*td < 0 and 400
*q + 9*td - 20050 <= 0 and i2 = 0 and 9*n - 380*q >= 0 and q - 40 <= 0
and q >= 0 and 100*n - 250*q - 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 6*n - 5*td < 0 and 400*q
+ 9*td - 20050 <= 0 and i2 = 0 and 9*n - 380*q >= 0 and q - 40 <= 0 and
q >= 0 and (100*n - 250*q - 10*td - 2500*z - 17299 > 0 and 20*n - 50*q -
 2*td - 500*z - 6535 <= 0 and 4420*n - 11050*q - 442*td + 81700*z -
3170191 = 0 or 20*n - 50*q - 2*td - 500*z - 6535 > 0 and 100*n - 250*q -
 10*td - 2500*z - 36519 <= 0 or 100*n - 250*q - 10*td - 2500*z - 36519 >
 0 and 100*n - 250*q - 10*td - 2500*z - 48051 < 0 and 187312500*n -
468281250*q - 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 - 50*q - 2*td - 500*z + 1153 = 0 or 2*p1 - 7 >= 0
and 76880*i2 - 2000*n + 240250*p1 + 6922*q + 200*td + 50000*z - 669797 =
 0) or 6*n - 5*td < 0 and 400*q + 9*td - 20050 <= 0 and i2 = 0 and 9*n -
 380*q >= 0 and q - 40 <= 0 and q >= 0 and (62500*n - 156250*q - 6250*td
 - 1250000*z - 32509373 < 0 and 62500*n - 156250*q - 6250*td - 1250000*z
 - 27134373 >= 0 and 31937500*n - 79843750*q - 3193750*td - 571562500*z
- 13629165033 = 0 or 62500*n - 156250*q - 6250*td - 1250000*z - 27134373
 < 0 and 62500*n - 156250*q - 6250*td - 1250000*z - 25790623 >= 0 and
187312500*n - 468281250*q - 18731250*td - 4082187500*z - 74105780531 = 0
 or 62500*n - 156250*q - 6250*td - 1250000*z - 25790623 < 0 and 62500*n
- 156250*q - 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 - 156250*q - 6250*td - 1250000*z - 40571873 = 0 or 2*p1 - 7
>= 0 and 10750000*i2 + 500000*n + 33593750*p1 - 981250*q - 50000*td -
10000000*z - 402109359 = 0) or 6*n - 5*td < 0 and 400*q + 9*td - 20050
<= 0 and i2 = 0 and 9*n - 380*q >= 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 + 162*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 + 6922*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 - 981250*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 6*n - 5*td < 0 and 400*q + 9*td - 20050 >= 0 and
i2 = 0 and 180*n + 171*td - 380950 >= 0 and td - 450 >= 0 and 9*td -
20050 <= 0 and q - 40 <= 0 and q >= 0 and 160*n - 7*td - 2400*z - 86698
= 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 6*n - 5
*td < 0 and 400*q + 9*td - 20050 >= 0 and i2 = 0 and 180*n + 171*td -
380950 >= 0 and td - 450 >= 0 and 9*td - 20050 <= 0 and q - 40 <= 0 and
q >= 0 and (160*n - 7*td - 2400*z - 67754 > 0 and 160*n - 7*td - 2400*z
- 86698 <= 0 or 160*n - 7*td - 2400*z - 86698 > 0 and 160*n - 7*td -
2400*z - 91434 <= 0 and 35360*n - 1547*td + 653600*z - 29792578 = 0 or
160*n - 7*td - 2400*z - 91434 > 0 and 160*n - 7*td - 2400*z - 105642 < 0
 and 255500000*n - 11178125*td - 4572500000*z - 141050664014 = 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 160*n - 7*td - 2400*z - 39338 = 0 or 2*p1 - 7 >= 0
 and 23680*i2 - 800*n + 74000*p1 + 592*q + 35*td + 12000*z + 25898 = 0)
or 6*n - 5*td < 0 and 400*q + 9*td - 20050 >= 0 and i2 = 0 and 180*n +
171*td - 380950 >= 0 and td - 450 >= 0 and 9*td - 20050 <= 0 and q - 40
<= 0 and q >= 0 and 800*n - 35*td - 20000*z - 392402 = 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 6*n - 5*td < 0 and 400*q +
 9*td - 20050 >= 0 and i2 = 0 and 180*n + 171*td - 380950 >= 0 and td -
450 >= 0 and 9*td - 20050 <= 0 and q - 40 <= 0 and q >= 0 and (800*n -
35*td - 20000*z - 238642 > 0 and 160*n - 7*td - 4000*z - 72330 <= 0 and
35360*n - 1547*td + 653600*z - 29792578 = 0 or 160*n - 7*td - 4000*z -
72330 > 0 and 800*n - 35*td - 20000*z - 392402 <= 0 or 800*n - 35*td -
20000*z - 392402 > 0 and 800*n - 35*td - 20000*z - 484658 < 0 and 1498500000
*n - 65559375*td - 32657500000*z - 780627025498 = 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 160*n - 7*td - 4000*z - 10826 = 0 or 2*p1 - 7 >= 0 and 153760*i2
- 4000*n + 480500*p1 + 3844*q + 175*td + 100000*z - 838344 = 0) or 6*n -
 5*td < 0 and 400*q + 9*td - 20050 >= 0 and i2 = 0 and 180*n + 171*td -
380950 >= 0 and td - 450 >= 0 and 9*td - 20050 <= 0 and q - 40 <= 0 and
q >= 0 and (500000*n - 21875*td - 10000000*z - 322731234 < 0 and 500000*
n - 21875*td - 10000000*z - 279731234 >= 0 and 255500000*n - 11178125*td
 - 4572500000*z - 141050664014 = 0 or 500000*n - 21875*td - 10000000*z -
 279731234 < 0 and 500000*n - 21875*td - 10000000*z - 268981234 >= 0 and
 1498500000*n - 65559375*td - 32657500000*z - 780627025498 = 0 or 500000
*n - 21875*td - 10000000*z - 268981234 < 0 and 500000*n - 21875*td -
10000000*z - 236731234 > 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 500000*n - 21875*td
 - 10000000*z - 387231234 = 0 or 2*p1 - 7 >= 0 and 10750000*i2 + 500000*
n + 33593750*p1 + 268750*q - 21875*td - 10000000*z - 464765609 = 0) or 6
*n - 5*td < 0 and 400*q + 9*td - 20050 >= 0 and i2 = 0 and 180*n + 171*
td - 380950 >= 0 and td - 450 >= 0 and 9*td - 20050 <= 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 23680*i2 - 800*n + 74000*p1 + 592*q + 35*td + 12000*z
+ 25898 = 0 or 80*i2 + 250*p1 + 2*q - 1377 > 0 and 80*i2 + 250*p1 + 2*q
- 1457 <= 0 and 153760*i2 - 4000*n + 480500*p1 + 3844*q + 175*td +
100000*z - 838344 = 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
 - 21875*td - 10000000*z - 464765609 = 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 6*n - 5*td < 0 and
i2 = 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) and (
400*q + 9*td - 20050 <= 0 and q = 0 or 400*q + 9*td - 20050 > 0 and 9*td
 - 20050 = 0) or 6*n - 5*td < 0 and i2 = 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) and (400*q + 9*td - 20050 <= 0
 and q = 0 or 400*q + 9*td - 20050 > 0 and 9*td - 20050 = 0) or 6*n - 5*
td < 0 and i2 = 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) and (400*q + 9*td - 20050 <= 0 and q = 0 or 400*q + 9*td -
20050 > 0 and 9*td - 20050 = 0) or 6*n - 5*td < 0 and i2 = 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) and (400*q + 9*td - 20050 <= 0 and q = 0 or 400*q + 9*td -
20050 > 0 and 9*td - 20050 = 0) or 6*n - 5*td < 0 and i2 = 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) and (400
*q + 9*td - 20050 <= 0 and q = 0 or 400*q + 9*td - 20050 > 0 and 9*td -
20050 = 0) or 6*n - 5*td < 0 and i2 = 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) and (400*q + 9*td - 20050 <= 0 and q = 0
or 400*q + 9*td - 20050 > 0 and 9*td - 20050 = 0)$



rlgsn testseries2;


(z = 0 and td = 0 and q = 0 and 250*p1 - 1457 = 0 and 100*n - 36519 = 0

 and i2 = 0) or (z = 0 and td = 0 and q = 0 and 250*p1 - 1377 = 0

 and 20*n - 8331 = 0 and i2 = 0) or (z = 0 and td = 0 and q = 0

 and 93656250*p1 - 569558609 = 0 and 187312500*n - 74105780531 = 0 and i2 = 0) 

or (z = 0 and td = 0 and q = 0 and 4*n - 1307 > 0 and 100*n - 36519 <= 0

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

 and 20*n - 8331 <= 0 and 20*n - 5963 > 0 and 50*n - 4625*p1 + 4647 = 0

 and i2 = 0) or (z = 0 and td = 0 and q = 0 and 62500*n - 25790623 < 0

 and 62500*n - 21759373 > 0 and 500000*n + 33593750*p1 - 402109359 = 0

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

 and 50*n + 15625*p1 - 109322 = 0 and 100*n - 36519 >= 0

 and 3575*n - 1387722 <= 0 and i2 = 0) or (z = 0 and td = 0 and 2*p1 - 7 >= 0

 and 250*p1 + 2*q - 1377 = 0 and 10*n + 3125*p1 - 21378 = 0 and 20*n - 8331 >= 0

 and 715*n - 316578 <= 0 and i2 = 0) or (z = 0 and td = 0 and 2*p1 - 7 >= 0

 and 93656250*p1 + 749250*q - 569558609 = 0

 and 93656250*n + 29267578125*p1 - 215039955578 = 0

 and 187312500*n - 74105780531 >= 0 and 6696421875*n - 2816019660178 <= 0

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

 and 2*n + 625*p1 - 4096 > 0 and 50*n + 15625*p1 - 109322 <= 0

 and 2000*n - 240250*p1 + 392917 <= 0 and 2000*n - 240250*p1 + 669797 >= 0

 and 2000*n - 240250*p1 - 6922*q + 669797 = 0

 and 348851*n - 45647500*p1 + 127261430 <= 0 and i2 = 0) or (z = 0 and td = 0

 and 2*p1 - 7 >= 0 and n < 0 and 10*n + 3125*p1 - 21378 <= 0

 and 10*n + 3125*p1 - 16194 > 0 and 50*n - 4625*p1 + 4647 >= 0

 and 50*n - 4625*p1 - 162*q + 4647 = 0 and 8771*n - 878750*p1 + 882930 <= 0

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

 and 31250*n + 9765625*p1 - 77168749 < 0 and 31250*n + 9765625*p1 - 69809374 > 0

 and 500000*n + 33593750*p1 - 441359359 <= 0

 and 500000*n + 33593750*p1 - 402109359 >= 0

 and 500000*n + 33593750*p1 - 981250*q - 402109359 = 0

 and 18116875*n + 1276562500*p1 - 15280155642 <= 0 and i2 = 0) or (z = 0

 and td = 0 and 2*p1 - 7 >= 0 and 2*n + 625*p1 - 4096 > 0

 and 50*n + 15625*p1 - 109322 <= 0 and 2000*n - 240250*p1 + 392917 <= 0

 and 2000*n - 240250*p1 + 669797 >= 0

 and 2000*n - 240250*p1 - 6922*q + 669797 = 0

 and 348851*n - 45647500*p1 + 127261430 <= 0 and i2 = 0) or (z = 0 and td = 0

 and 2*p1 - 7 >= 0 and 10*n + 3125*p1 - 21378 <= 0

 and 10*n + 3125*p1 - 16194 > 0 and 50*n - 4625*p1 - 1833 <= 0

 and 50*n - 4625*p1 + 4647 >= 0 and 50*n - 4625*p1 - 162*q + 4647 = 0

 and 8771*n - 878750*p1 + 882930 <= 0 and i2 = 0) or (z = 0 and td = 0

 and 2*p1 - 7 >= 0 and 31250*n + 9765625*p1 - 77168749 < 0

 and 31250*n + 9765625*p1 - 69809374 > 0

 and 500000*n + 33593750*p1 - 441359359 <= 0

 and 500000*n + 33593750*p1 - 402109359 >= 0

 and 500000*n + 33593750*p1 - 981250*q - 402109359 = 0

 and 18116875*n + 1276562500*p1 - 15280155642 <= 0 and i2 = 0) or (z = 0

 and td = 0 and 2*p1 - 7 >= 0 and 93656250*n + 29267578125*p1 - 215039955578 = 0

 and 187312500*n - 92837030531 <= 0 and 187312500*n - 74105780531 >= 0

 and 187312500*n - 468281250*q - 74105780531 = 0

 and 144136968750*n - 28126142578125*p1 + 90607109146708 <= 0

 and 144136968750*n - 28126142578125*p1 + 114021171646708 >= 0

 and 2475194203125*n - 534396708984375*p1 + 2166402261287452 <= 0 and i2 = 0) or

 (10*z - 103 <= 0 and 20*z - 161 > 0 and q = 0 and n >= 0

 and 9*n + 1000*z - 13300 < 0 and 12*n - 140*z - 6049 > 0

 and 300*n - 3500*z - 162757 <= 0 and 2000*n - 240250*p1 + 175*td + 4797 = 0

 and 6000*n - 720750*p1 - 70000*z + 945391 = 0 and i2 = 0) or (10*z - 103 <= 0

 and 20*z - 161 > 0 and q = 0 and n >= 0 and 9*n + 1000*z - 13300 < 0

 and 60*n - 100*z - 35633 <= 0 and 60*n - 100*z - 28529 > 0

 and 150*n - 13875*p1 - 250*z - 12659 = 0

 and 400*n - 37000*p1 + 5*td - 42624 = 0 and i2 = 0) or (10*z - 103 <= 0

 and 20*z - 161 > 0 and q = 0 and n >= 0 and 9*n + 1000*z - 13300 < 0

 and 187500*n - 1250000*z - 110621869 < 0

 and 187500*n - 1250000*z - 98528119 > 0

 and 500000*n + 33593750*p1 + 25000*td - 535109359 = 0

 and 1500000*n + 100781250*p1 - 10000000*z - 1472328077 = 0 and i2 = 0) or (

10*z - 103 <= 0 and 20*z - 161 > 0 and q >= 0 and q - 40 <= 0

 and 40*q - 120*z - 409 <= 0 and 2*p1 - 7 >= 0 and 250*p1 + 2*q - 1697 < 0

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

 and 302343750*p1 - 8831250*q - 530000000*z + 2233015769 > 0

 and 302343750*p1 + 181168750*q - 30000000*z - 4416984231 <= 0

 and 500000*n + 33593750*p1 - 981250*q + 25000*td - 535109359 = 0

 and 1500000*n + 100781250*p1 - 2943750*q - 10000000*z - 1472328077 = 0

 and i2 = 0) or (10*z - 103 <= 0 and 20*z - 161 > 0 and q >= 0 and q - 40 <= 0

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

 and 250*p1 + 2*q - 1377 > 0 and 2162250*p1 - 697702*q + 210000*z - 2836173 >= 0

 and 2162250*p1 + 62298*q + 2210000*z - 29436173 < 0

 and 2000*n - 240250*p1 - 6922*q + 175*td + 4797 = 0

 and 6000*n - 720750*p1 - 20766*q - 70000*z + 945391 = 0 and i2 = 0) or (

10*z - 103 <= 0 and 20*z - 161 > 0 and q >= 0 and q - 40 <= 0

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

 and 250*p1 + 2*q - 1057 > 0 and 41625*p1 - 17542*q + 750*z + 37977 >= 0

 and 41625*p1 + 1458*q + 50750*z - 627023 < 0

 and 150*n - 13875*p1 - 486*q - 250*z - 12659 = 0

 and 400*n - 37000*p1 - 1296*q + 5*td - 42624 = 0 and i2 = 0) or (

10*z - 103 <= 0 and 20*z - 161 > 0 and 2*p1 - 7 >= 0

 and 79843750*p1 - 2500000*z - 448579359 <= 0

 and 79843750*p1 - 2500000*z - 423029359 >= 0

 and 319375000*p1 - 2335000*z - 1768192561 >= 0

 and 44912109375*p1 - 18030781250*z - 126758882086 > 0

 and 101943359375*p1 - 3098281250*z - 560337236202 >= 0

 and 1500000*n - 218593750*p1 - 5498750*q + 321989359 = 0

 and 47906250*n + 14970703125*p1 - 687343750*z - 113047752362 = 0

 and 127750000*n + 39921875000*p1 + 13746875*td - 325838464632 = 0 and i2 = 0) 

or (10*z - 103 <= 0 and 20*z - 161 > 0 and 250*p1 - 1457 <= 0

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

 and 5000*p1 + 120*z - 28731 >= 0 and 140625*p1 - 55250*z - 398698 > 0

 and 2234375*p1 + 5250*z - 12777802 >= 0

 and 150*n + 46875*p1 - 1750*z - 354566 = 0

 and 400*n + 125000*p1 + 35*td - 1007576 = 0 and i2 = 0) or (10*z - 103 <= 0

 and 20*z - 161 > 0 and 250*p1 - 1377 <= 0 and 250*p1 - 1297 >= 0

 and 250*p1 + 2*q - 1377 = 0 and 5000*p1 + 120*z - 27131 >= 0

 and 28125*p1 - 10150*z - 75362 > 0 and 446875*p1 + 150*z - 2407938 >= 0

 and 30*n + 9375*p1 - 50*z - 69454 = 0 and 80*n + 25000*p1 + td - 186984 = 0

 and i2 = 0) or (10*z - 103 <= 0 and 50*z - 449 >= 0 and 2*p1 - 7 >= 0

 and 55250*p1 + 20000*z - 483917 <= 0 and 55250*p1 + 20000*z - 466237 >= 0

 and 1105000*p1 + 426520*z - 9587951 >= 0

 and 6215625*p1 + 672850*z - 42840682 > 0

 and 98759375*p1 + 35117150*z - 847208618 >= 0

 and 6630*n + 2071875*p1 + 960950*z - 24077894 = 0

 and 12000*n - 1054750*p1 - 38438*q - 1496637 = 0

 and 17680*n + 5525000*p1 - 19219*td - 30126024 = 0 and i2 = 0) or (

10*z - 103 <= 0 and 78125*z - 741562 >= 0 and 2*p1 - 7 >= 0

 and 93656250*p1 + 2500000*z - 569558609 <= 0

 and 93656250*p1 + 2500000*z - 539588609 >= 0

 and 374625000*p1 + 18991000*z - 2247590111 >= 0

 and 29267578125*p1 - 10417343750*z - 93245205578 > 0

 and 4185263671875*p1 + 118849843750*z - 24969198952298 >= 0

 and 1500000*n + 475406250*p1 + 53250*q - 3750562513 = 0

 and 93656250*n + 29267578125*p1 - 11093750*z - 231648330578 = 0

 and 749250000*n + 234140625000*p1 + 665625*td - 1854367019624 = 0 and i2 = 0) 

or (20*z - 161 >= 0 and 60*z - 599 < 0 and q = 0 and n >= 0

 and n - 40*z - 276 > 0 and 12*n - 1500*z + 5075 < 0

 and 25*n - 1000*z - 7861 <= 0 and 2000*n - 240250*p1 - 80000*z + 771297 = 0

 and 6000*n - 720750*p1 - 1600*td + 1501891 = 0 and i2 = 0) or (20*z - 161 >= 0

 and 60*z - 599 < 0 and q = 0 and n >= 0 and 5*n - 150*z - 1829 <= 0

 and 5*n - 150*z - 1237 > 0 and 12*n - 1500*z + 5075 < 0

 and 100*n - 9250*p1 - 3000*z + 14369 = 0 and 100*n - 9250*p1 - 20*td + 4219 = 0

 and i2 = 0) or (20*z - 161 >= 0 and 60*z - 599 < 0 and q = 0 and n >= 0

 and 12*n - 1500*z + 5075 < 0 and 15625*n - 546875*z - 5654687 < 0

 and 31250*n - 1093750*z - 9293749 > 0

 and 500000*n + 33593750*p1 - 17500000*z - 376734359 = 0

 and 1500000*n + 100781250*p1 - 350000*td - 1307828077 = 0 and i2 = 0) or (

20*z - 161 >= 0 and 60*z - 599 < 0 and q >= 0 and q - 40 <= 0

 and 160*q + 540*z - 9847 <= 0 and 2*p1 - 7 >= 0 and 250*p1 + 2*q - 1697 < 0

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

 and 100781250*p1 - 2943750*q + 135000000*z - 1764578077 > 0

 and 302343750*p1 + 181168750*q - 157500000*z - 3390609231 <= 0

 and 500000*n + 33593750*p1 - 981250*q - 17500000*z - 376734359 = 0

 and 1500000*n + 100781250*p1 - 2943750*q - 350000*td - 1307828077 = 0

 and i2 = 0) or (20*z - 161 >= 0 and 60*z - 599 < 0 and q >= 0 and q - 40 <= 0

 and 160*q + 540*z - 9847 <= 0 and 2*p1 - 7 >= 0 and 250*p1 + 2*q - 1457 <= 0

 and 250*p1 + 2*q - 1377 > 0 and 720750*p1 + 20766*q - 510000*z + 223609 < 0

 and 2162250*p1 - 697702*q + 720000*z - 6941673 >= 0

 and 2000*n - 240250*p1 - 6922*q - 80000*z + 771297 = 0

 and 6000*n - 720750*p1 - 20766*q - 1600*td + 1501891 = 0 and i2 = 0) or (

20*z - 161 >= 0 and 60*z - 599 < 0 and q >= 0 and q - 40 <= 0

 and 160*q + 540*z - 9847 <= 0 and 2*p1 - 7 >= 0 and 250*p1 + 2*q - 1377 <= 0

 and 250*p1 + 2*q - 1057 > 0 and 13875*p1 + 486*q - 14250*z + 41884 < 0

 and 83250*p1 - 35084*q + 27000*z - 129321 >= 0

 and 100*n - 9250*p1 - 324*q - 3000*z + 14369 = 0

 and 100*n - 9250*p1 - 324*q - 20*td + 4219 = 0 and i2 = 0) or (20*z - 161 >= 0

 and 60*z - 599 < 0 and q >= 0 and q - 40 <= 0 and 160*q + 540*z - 9847 >= 0

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

 and 201562500*p1 + 1612500*q + 295312500*z - 3990734279 > 0

 and 604687500*p1 + 4837500*q - 1521562500*z + 15220672163 <= 0

 and 1000000*n + 67187500*p1 + 537500*q - 26562500*z - 907328093 = 0

 and 1500000*n + 100781250*p1 + 806250*q - 265625*td - 1495796827 = 0 and i2 = 0

) or (20*z - 161 >= 0 and 60*z - 599 < 0 and q >= 0 and q - 40 <= 0

 and 160*q + 540*z - 9847 >= 0 and 2*p1 - 7 >= 0 and 250*p1 + 2*q - 1457 <= 0

 and 250*p1 + 2*q - 1377 > 0 and 2883000*p1 + 23064*q - 2242500*z + 4587061 < 0

 and 8649000*p1 + 69192*q + 12532500*z - 203781817 >= 0

 and 8000*n - 961000*p1 - 7688*q - 252500*z + 1854313 = 0

 and 12000*n - 1441500*p1 - 11532*q - 2525*td + 1500032 = 0 and i2 = 0) or (

20*z - 161 >= 0 and 60*z - 599 < 0 and q >= 0 and q - 40 <= 0

 and 160*q + 540*z - 9847 >= 0 and 2*p1 - 7 >= 0 and 250*p1 + 2*q - 1377 <= 0

 and 250*p1 + 2*q - 1057 > 0 and 444000*p1 + 3552*q - 496500*z + 2078813 < 0

 and 1332000*p1 + 10656*q + 2362500*z - 37272161 >= 0

 and 800*n - 74000*p1 - 592*q - 115*td - 66498 = 0

 and 1600*n - 148000*p1 - 1184*q - 34500*z - 16271 = 0 and i2 = 0) or (

20*z - 161 >= 0 and 60*z - 599 < 0 and q >= 0 and q - 40 <= 0

 and 160*q + 540*z - 9847 > 0 and 2*p1 - 7 >= 0 and 250*p1 + 2*q - 1697 < 0

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

 and 201562500*p1 + 1612500*q + 295312500*z - 3990734279 > 0

 and 604687500*p1 + 4837500*q - 1521562500*z + 15220672163 <= 0

 and 1000000*n + 67187500*p1 + 537500*q - 26562500*z - 907328093 = 0

 and 1500000*n + 100781250*p1 + 806250*q - 265625*td - 1495796827 = 0 and i2 = 0

) or (20*z - 161 >= 0 and 60*z - 599 < 0 and q >= 0 and q - 40 <= 0

 and 160*q + 540*z - 9847 > 0 and 2*p1 - 7 >= 0 and 250*p1 + 2*q - 1457 <= 0

 and 250*p1 + 2*q - 1377 > 0 and 2883000*p1 + 23064*q - 2242500*z + 4587061 < 0

 and 8649000*p1 + 69192*q + 12532500*z - 203781817 >= 0

 and 8000*n - 961000*p1 - 7688*q - 252500*z + 1854313 = 0

 and 12000*n - 1441500*p1 - 11532*q - 2525*td + 1500032 = 0 and i2 = 0) or (

20*z - 161 >= 0 and 60*z - 599 < 0 and q >= 0 and q - 40 <= 0

 and 160*q + 540*z - 9847 > 0 and 2*p1 - 7 >= 0 and 250*p1 + 2*q - 1377 <= 0

 and 250*p1 + 2*q - 1057 > 0 and 444000*p1 + 3552*q - 496500*z + 2078813 < 0

 and 1332000*p1 + 10656*q + 2362500*z - 37272161 >= 0

 and 800*n - 74000*p1 - 592*q - 115*td - 66498 = 0

 and 1600*n - 148000*p1 - 1184*q - 34500*z - 16271 = 0 and i2 = 0) or (

20*z - 161 >= 0 and 60*z - 599 < 0 and 2*p1 - 7 >= 0

 and 79843750*p1 - 2500000*z - 448579359 <= 0

 and 79843750*p1 - 2500000*z - 423029359 >= 0

 and 1277500000*p1 - 74492500*z - 6548292619 >= 0

 and 14970703125*p1 + 3943593750*z - 122381486737 > 0

 and 203886718750*p1 - 5033125000*z - 1130040144279 >= 0

 and 250000*n - 262656250*p1 - 2726250*q + 1381660577 = 0

 and 31937500*n + 9980468750*p1 - 1363125000*z - 68080756783 = 0

 and 31937500*n + 9980468750*p1 - 9087500*td - 72692663033 = 0 and i2 = 0) or (

20*z - 161 >= 0 and 60*z - 599 < 0 and 250*p1 - 1457 <= 0 and 250*p1 - 1377 >= 0

 and 250*p1 + 2*q - 1457 = 0 and 20000*p1 - 540*z - 106713 >= 0

 and 46875*p1 + 12750*z - 383791 > 0 and 4468750*p1 + 36000*z - 25760879 >= 0

 and 100*n + 31250*p1 - 4000*z - 213569 = 0

 and 300*n + 93750*p1 - 80*td - 681307 = 0 and i2 = 0) or (20*z - 161 >= 0

 and 60*z - 599 < 0 and 250*p1 - 1377 <= 0 and 250*p1 - 1297 >= 0

 and 250*p1 + 2*q - 1377 = 0 and 9375*p1 + 2850*z - 75299 > 0

 and 20000*p1 - 540*z - 100313 >= 0 and 893750*p1 + 5400*z - 4856931 >= 0

 and 20*n + 6250*p1 - 600*z - 41741 = 0 and 20*n + 6250*p1 - 4*td - 43771 = 0

 and i2 = 0) or (20*z - 161 >= 0 and 78125*z - 741562 < 0 and 2*p1 - 7 >= 0

 and 93656250*p1 + 2500000*z - 569558609 <= 0

 and 93656250*p1 + 2500000*z - 539588609 >= 0

 and 1498500000*p1 - 459500*z - 8375151269 >= 0

 and 29267578125*p1 + 9042343750*z - 249895689953 > 0

 and 8370527343750*p1 + 285464375000*z - 50322903638971 >= 0

 and 250000*n + 344593750*p1 + 2131750*q - 2181822311 = 0

 and 187312500*n + 58535156250*p1 - 5329375000*z - 420573801781 = 0

 and 561937500*n + 175605468750*p1 - 106587500*td - 1315814561593 = 0 and i2 = 0

) or (20*z - 161 > 0 and 40*z - 397 <= 0 and q >= 0 and q - 40 <= 0

 and 40*q - 120*z - 409 >= 0 and 2*p1 - 7 >= 0 and 250*p1 + 2*q - 1697 < 0

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

 and 302343750*p1 + 2418750*q - 563750000*z + 2117984519 > 0

 and 302343750*p1 + 2418750*q + 506250000*z - 2589265481 <= 0

 and 500000*n + 33593750*p1 + 268750*q + 53125*td - 597765609 = 0

 and 1500000*n + 100781250*p1 + 806250*q - 21250000*z - 1510671827 = 0

 and i2 = 0) or (20*z - 161 > 0 and 40*z - 397 <= 0 and q >= 0 and q - 40 <= 0

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

 and 250*p1 + 2*q - 1377 > 0 and 1081125*p1 + 8649*q - 967500*z - 5073524 >= 0

 and 1081125*p1 + 8649*q + 1172500*z - 14488024 < 0

 and 3000*n - 360375*p1 - 2883*q - 57500*z + 396008 = 0

 and 4000*n - 480500*p1 - 3844*q + 575*td - 491656 = 0 and i2 = 0) or (

20*z - 161 > 0 and 40*z - 397 <= 0 and q >= 0 and q - 40 <= 0

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

 and 250*p1 + 2*q - 1057 > 0 and 333000*p1 + 2664*q - 423000*z - 1158359 >= 0

 and 333000*p1 + 2664*q + 433000*z - 4924159 < 0

 and 800*n - 74000*p1 - 592*q + 55*td - 185498 = 0

 and 1200*n - 111000*p1 - 888*q - 11000*z - 131947 = 0 and i2 = 0) or (

20*z - 161 > 0 and 40*z - 397 <= 0 and q >= 0 and q - 40 <= 0

 and 40*q - 120*z - 409 > 0 and 2*p1 - 7 >= 0 and 250*p1 + 2*q - 1697 < 0

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

 and 302343750*p1 + 2418750*q - 563750000*z + 2117984519 > 0

 and 302343750*p1 + 2418750*q + 506250000*z - 2589265481 <= 0

 and 500000*n + 33593750*p1 + 268750*q + 53125*td - 597765609 = 0

 and 1500000*n + 100781250*p1 + 806250*q - 21250000*z - 1510671827 = 0

 and i2 = 0) or (20*z - 161 > 0 and 40*z - 397 <= 0 and q >= 0 and q - 40 <= 0

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

 and 250*p1 + 2*q - 1377 > 0 and 1081125*p1 + 8649*q - 967500*z - 5073524 >= 0

 and 1081125*p1 + 8649*q + 1172500*z - 14488024 < 0

 and 3000*n - 360375*p1 - 2883*q - 57500*z + 396008 = 0

 and 4000*n - 480500*p1 - 3844*q + 575*td - 491656 = 0 and i2 = 0) or (

20*z - 161 > 0 and 40*z - 397 <= 0 and q >= 0 and q - 40 <= 0

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

 and 250*p1 + 2*q - 1057 > 0 and 333000*p1 + 2664*q - 423000*z - 1158359 >= 0

 and 333000*p1 + 2664*q + 433000*z - 4924159 < 0

 and 800*n - 74000*p1 - 592*q + 55*td - 185498 = 0

 and 1200*n - 111000*p1 - 888*q - 11000*z - 131947 = 0 and i2 = 0) or (

20*z - 161 > 0 and 78125*z - 741562 < 0 and 2*p1 - 7 >= 0

 and 93656250*p1 + 2500000*z - 569558609 <= 0

 and 93656250*p1 + 2500000*z - 539588609 >= 0

 and 374625000*p1 + 18991000*z - 2247590111 >= 0

 and 29267578125*p1 - 10417343750*z - 93245205578 > 0

 and 4185263671875*p1 + 118849843750*z - 24969198952298 >= 0

 and 1500000*n + 475406250*p1 + 53250*q - 3750562513 = 0

 and 93656250*n + 29267578125*p1 - 11093750*z - 231648330578 = 0

 and 749250000*n + 234140625000*p1 + 665625*td - 1854367019624 = 0 and i2 = 0) 

or (50*z - 449 = 0 and 2*td - 1679 = 0 and 2*p1 - 7 >= 0

 and 250*p1 + 2*q - 1377 = 0 and 5*n - 3176 >= 0 and 20*n + 6250*p1 - 47129 = 0

 and 715*n - 482752 <= 0 and i2 = 0) or (50*z - 449 < 0 and 125*z - 1012 >= 0

 and 2*p1 - 7 >= 0 and 55250*p1 + 20000*z - 483917 <= 0

 and 55250*p1 + 20000*z - 466237 >= 0 and 1105000*p1 + 426520*z - 9587951 >= 0

 and 6215625*p1 + 672850*z - 42840682 > 0

 and 98759375*p1 + 35117150*z - 847208618 >= 0

 and 6630*n + 2071875*p1 + 960950*z - 24077894 = 0

 and 12000*n - 1054750*p1 - 38438*q - 1496637 = 0

 and 17680*n + 5525000*p1 - 19219*td - 30126024 = 0 and i2 = 0) or (

50*z - 449 < 0 and 125*z - 1012 >= 0 and 2*p1 - 7 >= 0

 and 55250*p1 + 20000*z - 483917 <= 0 and 55250*p1 + 20000*z - 466237 >= 0

 and 2071875*p1 + 1601850*z - 25369639 > 0

 and 4420000*p1 + 1480660*z - 36537173 >= 0

 and 197518750*p1 + 71361400*z - 1703490391 >= 0

 and 2000*n - 19250*p1 - 5154*q - 1164371 = 0

 and 4420*n + 1381250*p1 + 515400*z - 15043801 = 0

 and 4420*n + 1381250*p1 + 3436*td - 13300031 = 0 and i2 = 0) or (50*z - 449 < 0

 and 1703700*z - 14445503 > 0 and q = 0 and 55250*p1 + 20000*z - 483917 = 0

 and 165750*p1 + 400*td - 1248751 = 0 and 2000*n - 19250*p1 - 1164371 = 0

 and i2 = 0) or (50*z - 449 >= 0 and 60*z - 599 < 0 and q = 0

 and 55250*p1 + 20000*z - 483917 = 0 and 165750*p1 + 400*td - 1248751 = 0

 and 2000*n - 19250*p1 - 1164371 = 0 and i2 = 0) or (50*z - 449 >= 0

 and 60*z - 599 < 0 and 2*p1 - 7 >= 0 and 55250*p1 + 20000*z - 483917 <= 0

 and 55250*p1 + 20000*z - 466237 >= 0 and 2071875*p1 + 1601850*z - 25369639 > 0

 and 4420000*p1 + 1480660*z - 36537173 >= 0

 and 197518750*p1 + 71361400*z - 1703490391 >= 0

 and 2000*n - 19250*p1 - 5154*q - 1164371 = 0

 and 4420*n + 1381250*p1 + 515400*z - 15043801 = 0

 and 4420*n + 1381250*p1 + 3436*td - 13300031 = 0 and i2 = 0) or (60*z - 599 < 0

 and 5700*z - 47323 > 0 and q = 0 and 250*p1 - 1377 = 0

 and 5*n - 150*z - 1829 = 0 and 10*n - 2*td - 4673 = 0 and i2 = 0) or (

60*z - 599 < 0 and 25500*z - 221207 > 0 and q = 0 and 250*p1 - 1457 = 0

 and 25*n - 1000*z - 7861 = 0 and 75*n - 20*td - 33733 = 0 and i2 = 0) or (

60*z - 599 < 0 and 78125*z - 741562 >= 0 and q = 0

 and 93656250*p1 + 2500000*z - 569558609 = 0

 and 280968750*p1 + 50000*td - 1683300827 = 0

 and 250000*n + 344593750*p1 - 2181822311 = 0 and i2 = 0) or (60*z - 599 < 0

 and 78125*z - 741562 >= 0 and 2*p1 - 7 >= 0

 and 93656250*p1 + 2500000*z - 569558609 <= 0

 and 93656250*p1 + 2500000*z - 539588609 >= 0

 and 1498500000*p1 - 459500*z - 8375151269 >= 0

 and 29267578125*p1 + 9042343750*z - 249895689953 > 0

 and 8370527343750*p1 + 285464375000*z - 50322903638971 >= 0

 and 250000*n + 344593750*p1 + 2131750*q - 2181822311 = 0

 and 187312500*n + 58535156250*p1 - 5329375000*z - 420573801781 = 0

 and 561937500*n + 175605468750*p1 - 106587500*td - 1315814561593 = 0 and i2 = 0

) or (60*z - 599 < 0 and 8824687500*z - 76545713849 > 0 and q = 0

 and 79843750*p1 - 2500000*z - 448579359 = 0

 and 239531250*p1 - 50000*td - 1371113077 = 0

 and 250000*n - 262656250*p1 + 1381660577 = 0 and i2 = 0) or (

78125*z - 741562 < 0 and 16522187500*z - 143817249281 > 0 and q = 0

 and 93656250*p1 + 2500000*z - 569558609 = 0

 and 280968750*p1 + 50000*td - 1683300827 = 0

 and 250000*n + 344593750*p1 - 2181822311 = 0 and i2 = 0)


end;

