* #variable= 417 #constraint= 1115
* #aggregation= lexico
* Created by OpbBuilder
min: +1 x417 +1 x408 +1 x399 +1 x390 +1 x381 +1 x372 +1 x363 +1 x354 ;
min: +1 x416 +1 x407 +1 x398 +1 x389 +1 x380 +1 x371 +1 x362 +1 x353 ;
min: +1 x414 +1 x405 +1 x396 +1 x387 +1 x378 +1 x369 +1 x360 +1 x351 ;
min: +1 x412 +1 x403 +1 x394 +1 x385 +1 x376 +1 x367 +1 x358 +1 x349 ;
min: +1 x410 +1 x401 +1 x392 +1 x383 +1 x374 +1 x365 +1 x356 +1 x347 ;
min: +1 x170 +1 x67 +1 x179 +1 x130 +1 x60 +1 x109 +1 x163 +1 x46 +1 x74 +1 x145 +1 x81 +1 x88 +1 x137 +1 x188 +1 x95 +1 x102 +1 x53 +1 x123 +1 x155 +1 x116 ;
min: +1 x312 +1 x310 +1 x308 +1 x306 ;
+1 x1 >= 1;
+1 x2 >= 1;
+1 x7 >= 1;
+1 x12 >= 1;
+1 x17 >= 1;
+1 x22 >= 1;
+1 x27 >= 1;
+1 x32 >= 1;
+1 x37 >= 1;
+1 x48 >= 1;
+1 x76 >= 1;
+1 x317 >= 1;
+1 x321 >= 1;
+1 x325 >= 1;
+1 x329 >= 1;
+1 x333 >= 1;
+1 x337 >= 1;
+1 x341 >= 1;
+1 x345 >= 1;
+1 x46 >= 1;
+1 x74 >= 1;
 -1 x4 +1 x3 >= 0;
 -1 x3 +1 x2 >= 0;
 +1 x5 -1 x2 >= 0;
 +1 x6 -1 x5 >= 0;
 -1 x9 +1 x8 >= 0;
 -1 x8 +1 x7 >= 0;
 +1 x10 -1 x7 >= 0;
 -1 x10 +1 x11 >= 0;
 +1 x13 -1 x14 >= 0;
 +1 x12 -1 x13 >= 0;
 -1 x12 +1 x15 >= 0;
 -1 x15 +1 x16 >= 0;
 -1 x19 +1 x18 >= 0;
 -1 x18 +1 x17 >= 0;
 +1 x20 -1 x17 >= 0;
 +1 x21 -1 x20 >= 0;
 +1 x23 -1 x24 >= 0;
 -1 x23 +1 x22 >= 0;
 -1 x22 +1 x25 >= 0;
 -1 x25 +1 x26 >= 0;
 +1 x28 -1 x29 >= 0;
 +1 x27 -1 x28 >= 0;
 -1 x27 +1 x30 >= 0;
 -1 x30 +1 x31 >= 0;
 +1 x33 -1 x34 >= 0;
 +1 x32 -1 x33 >= 0;
 -1 x32 +1 x35 >= 0;
 -1 x35 +1 x36 >= 0;
 -1 x39 +1 x38 >= 0;
 +1 x37 -1 x38 >= 0;
 -1 x37 +1 x40 >= 0;
 -1 x40 +1 x41 >= 0;
 +1 x19 -1 x42 >= 0;
 +1 x24 -1 x42 >= 0;
 +1 x17 -1 x43 >= 0;
 +1 x24 -1 x43 >= 0;
 +1 x19 -1 x44 >= 0;
 +1 x22 -1 x44 >= 0;
 -1 x44 +1 x45 >= 0;
 -1 x43 +1 x45 >= 0;
 -1 x48 +1 x47 >= 0;
 -1 x47 +1 x48 >= 0;
 +1 x34 -1 x49 >= 0;
 +1 x14 -1 x49 >= 0;
 +1 x32 -1 x50 >= 0;
 +1 x14 -1 x50 >= 0;
 +1 x34 -1 x51 >= 0;
 +1 x12 -1 x51 >= 0;
 -1 x51 +1 x52 >= 0;
 -1 x50 +1 x52 >= 0;
 -1 x55 +1 x54 >= 0;
 -1 x54 +1 x55 >= 0;
 +1 x34 -1 x56 >= 0;
 +1 x24 -1 x56 >= 0;
 +1 x32 -1 x57 >= 0;
 +1 x24 -1 x57 >= 0;
 +1 x34 -1 x58 >= 0;
 +1 x22 -1 x58 >= 0;
 -1 x58 +1 x59 >= 0;
 -1 x57 +1 x59 >= 0;
 +1 x61 -1 x62 >= 0;
 -1 x61 +1 x62 >= 0;
 +1 x24 -1 x63 >= 0;
 +1 x14 -1 x63 >= 0;
 +1 x22 -1 x64 >= 0;
 +1 x14 -1 x64 >= 0;
 +1 x24 -1 x65 >= 0;
 +1 x12 -1 x65 >= 0;
 -1 x65 +1 x66 >= 0;
 -1 x64 +1 x66 >= 0;
 -1 x69 +1 x68 >= 0;
 +1 x69 -1 x68 >= 0;
 +1 x4 -1 x70 >= 0;
 +1 x14 -1 x70 >= 0;
 +1 x2 -1 x71 >= 0;
 +1 x14 -1 x71 >= 0;
 +1 x4 -1 x72 >= 0;
 +1 x12 -1 x72 >= 0;
 -1 x72 +1 x73 >= 0;
 -1 x71 +1 x73 >= 0;
 -1 x76 +1 x75 >= 0;
 -1 x75 +1 x76 >= 0;
 +1 x39 -1 x77 >= 0;
 +1 x4 -1 x77 >= 0;
 +1 x37 -1 x78 >= 0;
 +1 x4 -1 x78 >= 0;
 +1 x39 -1 x79 >= 0;
 +1 x2 -1 x79 >= 0;
 -1 x79 +1 x80 >= 0;
 -1 x78 +1 x80 >= 0;
 -1 x83 +1 x82 >= 0;
 -1 x82 +1 x83 >= 0;
 +1 x39 -1 x84 >= 0;
 +1 x19 -1 x84 >= 0;
 +1 x37 -1 x85 >= 0;
 +1 x19 -1 x85 >= 0;
 +1 x39 -1 x86 >= 0;
 +1 x17 -1 x86 >= 0;
 -1 x86 +1 x87 >= 0;
 -1 x85 +1 x87 >= 0;
 +1 x89 -1 x90 >= 0;
 -1 x89 +1 x90 >= 0;
 +1 x19 -1 x91 >= 0;
 +1 x4 -1 x91 >= 0;
 +1 x17 -1 x92 >= 0;
 +1 x4 -1 x92 >= 0;
 +1 x19 -1 x93 >= 0;
 +1 x2 -1 x93 >= 0;
 -1 x93 +1 x94 >= 0;
 -1 x92 +1 x94 >= 0;
 +1 x96 -1 x97 >= 0;
 -1 x96 +1 x97 >= 0;
 +1 x9 -1 x98 >= 0;
 +1 x39 -1 x98 >= 0;
 +1 x7 -1 x99 >= 0;
 +1 x39 -1 x99 >= 0;
 +1 x9 -1 x100 >= 0;
 +1 x37 -1 x100 >= 0;
 -1 x100 +1 x101 >= 0;
 -1 x99 +1 x101 >= 0;
 -1 x104 +1 x103 >= 0;
 -1 x103 +1 x104 >= 0;
 +1 x29 -1 x105 >= 0;
 +1 x39 -1 x105 >= 0;
 +1 x27 -1 x106 >= 0;
 +1 x39 -1 x106 >= 0;
 +1 x29 -1 x107 >= 0;
 +1 x37 -1 x107 >= 0;
 -1 x107 +1 x108 >= 0;
 -1 x106 +1 x108 >= 0;
 +1 x110 -1 x111 >= 0;
 -1 x110 +1 x111 >= 0;
 +1 x34 -1 x112 >= 0;
 +1 x39 -1 x112 >= 0;
 +1 x32 -1 x113 >= 0;
 +1 x39 -1 x113 >= 0;
 +1 x34 -1 x114 >= 0;
 +1 x37 -1 x114 >= 0;
 -1 x114 +1 x115 >= 0;
 -1 x113 +1 x115 >= 0;
 -1 x118 +1 x117 >= 0;
 +1 x118 -1 x117 >= 0;
 +1 x29 -1 x119 >= 0;
 +1 x9 -1 x119 >= 0;
 +1 x27 -1 x120 >= 0;
 +1 x9 -1 x120 >= 0;
 +1 x29 -1 x121 >= 0;
 +1 x7 -1 x121 >= 0;
 -1 x121 +1 x122 >= 0;
 -1 x120 +1 x122 >= 0;
 +1 x124 -1 x125 >= 0;
 +1 x125 -1 x124 >= 0;
 +1 x34 -1 x126 >= 0;
 +1 x9 -1 x126 >= 0;
 +1 x32 -1 x127 >= 0;
 +1 x9 -1 x127 >= 0;
 +1 x34 -1 x128 >= 0;
 +1 x7 -1 x128 >= 0;
 -1 x128 +1 x129 >= 0;
 -1 x127 +1 x129 >= 0;
 -1 x132 +1 x131 >= 0;
 +1 x132 -1 x131 >= 0;
 +1 x34 -1 x133 >= 0;
 +1 x29 -1 x133 >= 0;
 +1 x32 -1 x134 >= 0;
 +1 x29 -1 x134 >= 0;
 +1 x34 -1 x135 >= 0;
 +1 x27 -1 x135 >= 0;
 -1 x135 +1 x136 >= 0;
 -1 x134 +1 x136 >= 0;
 +1 x138 -1 x139 >= 0;
 -1 x138 +1 x139 >= 0;
 -1 x140 +1 x131 >= 0;
 -1 x131 +1 x140 >= 0;
 +1 x9 -1 x141 >= 0;
 +1 x14 -1 x141 >= 0;
 +1 x7 -1 x142 >= 0;
 +1 x14 -1 x142 >= 0;
 +1 x9 -1 x143 >= 0;
 +1 x12 -1 x143 >= 0;
 -1 x143 +1 x144 >= 0;
 -1 x142 +1 x144 >= 0;
 -1 x147 +1 x146 >= 0;
 +1 x147 -1 x146 >= 0;
 +1 x54 -1 x148 >= 0;
 -1 x54 +1 x148 >= 0;
 +1 x110 -1 x149 >= 0;
 +1 x149 -1 x110 >= 0;
 -1 x150 +1 x82 >= 0;
 -1 x82 +1 x150 >= 0;
 +1 x29 -1 x151 >= 0;
 +1 x4 -1 x151 >= 0;
 +1 x27 -1 x152 >= 0;
 +1 x4 -1 x152 >= 0;
 +1 x29 -1 x153 >= 0;
 +1 x2 -1 x153 >= 0;
 -1 x153 +1 x154 >= 0;
 -1 x152 +1 x154 >= 0;
 +1 x156 -1 x157 >= 0;
 +1 x157 -1 x156 >= 0;
 -1 x158 +1 x156 >= 0;
 +1 x158 -1 x156 >= 0;
 +1 x29 -1 x159 >= 0;
 +1 x24 -1 x159 >= 0;
 +1 x27 -1 x160 >= 0;
 +1 x24 -1 x160 >= 0;
 +1 x29 -1 x161 >= 0;
 +1 x22 -1 x161 >= 0;
 -1 x161 +1 x162 >= 0;
 -1 x160 +1 x162 >= 0;
 +1 x164 -1 x165 >= 0;
 +1 x165 -1 x164 >= 0;
 +1 x24 -1 x166 >= 0;
 +1 x4 -1 x166 >= 0;
 +1 x22 -1 x167 >= 0;
 +1 x4 -1 x167 >= 0;
 +1 x24 -1 x168 >= 0;
 +1 x2 -1 x168 >= 0;
 -1 x168 +1 x169 >= 0;
 -1 x167 +1 x169 >= 0;
 -1 x172 +1 x171 >= 0;
 -1 x171 +1 x172 >= 0;
 +1 x103 -1 x173 >= 0;
 -1 x103 +1 x173 >= 0;
 +1 x89 -1 x174 >= 0;
 +1 x174 -1 x89 >= 0;
 +1 x9 -1 x175 >= 0;
 +1 x19 -1 x175 >= 0;
 +1 x7 -1 x176 >= 0;
 +1 x19 -1 x176 >= 0;
 +1 x9 -1 x177 >= 0;
 +1 x17 -1 x177 >= 0;
 -1 x177 +1 x178 >= 0;
 -1 x176 +1 x178 >= 0;
 -1 x181 +1 x180 >= 0;
 +1 x181 -1 x180 >= 0;
 -1 x182 +1 x146 >= 0;
 -1 x146 +1 x182 >= 0;
 -1 x183 +1 x180 >= 0;
 -1 x180 +1 x183 >= 0;
 +1 x19 -1 x184 >= 0;
 +1 x14 -1 x184 >= 0;
 +1 x17 -1 x185 >= 0;
 +1 x14 -1 x185 >= 0;
 +1 x19 -1 x186 >= 0;
 +1 x12 -1 x186 >= 0;
 -1 x186 +1 x187 >= 0;
 -1 x185 +1 x187 >= 0;
 +1 x189 -1 x190 >= 0;
 -1 x189 +1 x190 >= 0;
 +1 x138 -1 x191 >= 0;
 +1 x191 -1 x138 >= 0;
 +1 x164 -1 x192 >= 0;
 +1 x192 -1 x164 >= 0;
 +1 x61 -1 x193 >= 0;
 +1 x193 -1 x61 >= 0;
 +1 x195 -1 x196 >= 0;
 +1 x194 -1 x196 >= 0;
 -1 x196 -1 x137 >= -1;
 +1 x198 -1 x199 >= 0;
 +1 x197 -1 x199 >= 0;
 -1 x199 -1 x137 >= -1;
 +1 x201 -1 x202 >= 0;
 +1 x200 -1 x202 >= 0;
 -1 x202 -1 x137 >= -1;
 +1 x204 -1 x205 >= 0;
 +1 x203 -1 x205 >= 0;
 -1 x137 -1 x205 >= -1;
 +1 x207 -1 x208 >= 0;
 +1 x206 -1 x208 >= 0;
 -1 x95 -1 x208 >= -1;
 +1 x210 -1 x211 >= 0;
 +1 x209 -1 x211 >= 0;
 -1 x95 -1 x211 >= -1;
 +1 x213 -1 x214 >= 0;
 +1 x212 -1 x214 >= 0;
 -1 x95 -1 x214 >= -1;
 +1 x216 -1 x217 >= 0;
 +1 x215 -1 x217 >= 0;
 -1 x95 -1 x217 >= -1;
 +1 x218 -1 x219 >= 0;
 +1 x195 -1 x219 >= 0;
 -1 x219 -1 x109 >= -1;
 +1 x220 -1 x221 >= 0;
 +1 x198 -1 x221 >= 0;
 -1 x221 -1 x109 >= -1;
 +1 x222 -1 x223 >= 0;
 +1 x201 -1 x223 >= 0;
 -1 x223 -1 x109 >= -1;
 +1 x224 -1 x225 >= 0;
 +1 x204 -1 x225 >= 0;
 -1 x109 -1 x225 >= -1;
 +1 x226 -1 x227 >= 0;
 +1 x206 -1 x227 >= 0;
 -1 x227 -1 x188 >= -1;
 +1 x228 -1 x229 >= 0;
 +1 x209 -1 x229 >= 0;
 -1 x229 -1 x188 >= -1;
 +1 x230 -1 x231 >= 0;
 +1 x212 -1 x231 >= 0;
 -1 x231 -1 x188 >= -1;
 +1 x232 -1 x233 >= 0;
 +1 x215 -1 x233 >= 0;
 -1 x233 -1 x188 >= -1;
 +1 x226 -1 x234 >= 0;
 +1 x194 -1 x234 >= 0;
 -1 x234 -1 x53 >= -1;
 +1 x228 -1 x235 >= 0;
 +1 x197 -1 x235 >= 0;
 -1 x235 -1 x53 >= -1;
 +1 x230 -1 x236 >= 0;
 +1 x200 -1 x236 >= 0;
 -1 x236 -1 x53 >= -1;
 +1 x232 -1 x237 >= 0;
 +1 x203 -1 x237 >= 0;
 -1 x53 -1 x237 >= -1;
 +1 x226 -1 x238 >= 0;
 +1 x207 -1 x238 >= 0;
 -1 x74 -1 x238 >= -1;
 +1 x228 -1 x239 >= 0;
 +1 x210 -1 x239 >= 0;
 -1 x239 -1 x74 >= -1;
 +1 x230 -1 x240 >= 0;
 +1 x213 -1 x240 >= 0;
 -1 x74 -1 x240 >= -1;
 +1 x232 -1 x241 >= 0;
 +1 x216 -1 x241 >= 0;
 -1 x241 -1 x74 >= -1;
 +1 x242 -1 x243 >= 0;
 +1 x195 -1 x243 >= 0;
 -1 x163 -1 x243 >= -1;
 +1 x244 -1 x245 >= 0;
 +1 x198 -1 x245 >= 0;
 -1 x245 -1 x163 >= -1;
 +1 x246 -1 x247 >= 0;
 +1 x201 -1 x247 >= 0;
 -1 x163 -1 x247 >= -1;
 +1 x248 -1 x249 >= 0;
 +1 x204 -1 x249 >= 0;
 -1 x163 -1 x249 >= -1;
 +1 x226 -1 x251 >= 0;
 +1 x250 -1 x251 >= 0;
 -1 x251 -1 x145 >= -1;
 +1 x228 -1 x253 >= 0;
 +1 x252 -1 x253 >= 0;
 -1 x145 -1 x253 >= -1;
 +1 x230 -1 x255 >= 0;
 +1 x254 -1 x255 >= 0;
 -1 x145 -1 x255 >= -1;
 +1 x232 -1 x257 >= 0;
 +1 x256 -1 x257 >= 0;
 -1 x145 -1 x257 >= -1;
 +1 x250 -1 x258 >= 0;
 +1 x195 -1 x258 >= 0;
 -1 x123 -1 x258 >= -1;
 +1 x252 -1 x259 >= 0;
 +1 x198 -1 x259 >= 0;
 -1 x259 -1 x123 >= -1;
 +1 x254 -1 x260 >= 0;
 +1 x201 -1 x260 >= 0;
 -1 x123 -1 x260 >= -1;
 +1 x256 -1 x261 >= 0;
 +1 x204 -1 x261 >= 0;
 -1 x123 -1 x261 >= -1;
 +1 x218 -1 x262 >= 0;
 +1 x194 -1 x262 >= 0;
 -1 x262 -1 x116 >= -1;
 +1 x220 -1 x263 >= 0;
 +1 x197 -1 x263 >= 0;
 -1 x263 -1 x116 >= -1;
 +1 x222 -1 x264 >= 0;
 +1 x200 -1 x264 >= 0;
 -1 x264 -1 x116 >= -1;
 +1 x224 -1 x265 >= 0;
 +1 x203 -1 x265 >= 0;
 -1 x116 -1 x265 >= -1;
 +1 x242 -1 x266 >= 0;
 +1 x194 -1 x266 >= 0;
 -1 x266 -1 x60 >= -1;
 +1 x244 -1 x267 >= 0;
 +1 x197 -1 x267 >= 0;
 -1 x267 -1 x60 >= -1;
 +1 x246 -1 x268 >= 0;
 +1 x200 -1 x268 >= 0;
 -1 x268 -1 x60 >= -1;
 +1 x248 -1 x269 >= 0;
 +1 x203 -1 x269 >= 0;
 -1 x269 -1 x60 >= -1;
 +1 x207 -1 x270 >= 0;
 +1 x218 -1 x270 >= 0;
 -1 x81 -1 x270 >= -1;
 +1 x210 -1 x271 >= 0;
 +1 x220 -1 x271 >= 0;
 -1 x271 -1 x81 >= -1;
 +1 x213 -1 x272 >= 0;
 +1 x222 -1 x272 >= 0;
 -1 x81 -1 x272 >= -1;
 +1 x216 -1 x273 >= 0;
 +1 x224 -1 x273 >= 0;
 -1 x81 -1 x273 >= -1;
 +1 x206 -1 x274 >= 0;
 +1 x218 -1 x274 >= 0;
 -1 x274 -1 x88 >= -1;
 +1 x209 -1 x275 >= 0;
 +1 x220 -1 x275 >= 0;
 -1 x275 -1 x88 >= -1;
 +1 x212 -1 x276 >= 0;
 +1 x222 -1 x276 >= 0;
 -1 x276 -1 x88 >= -1;
 +1 x215 -1 x277 >= 0;
 +1 x224 -1 x277 >= 0;
 -1 x277 -1 x88 >= -1;
 +1 x250 -1 x278 >= 0;
 +1 x194 -1 x278 >= 0;
 -1 x278 -1 x130 >= -1;
 +1 x252 -1 x279 >= 0;
 +1 x197 -1 x279 >= 0;
 -1 x130 -1 x279 >= -1;
 +1 x254 -1 x280 >= 0;
 +1 x200 -1 x280 >= 0;
 -1 x130 -1 x280 >= -1;
 +1 x256 -1 x281 >= 0;
 +1 x203 -1 x281 >= 0;
 -1 x281 -1 x130 >= -1;
 +1 x207 -1 x282 >= 0;
 +1 x242 -1 x282 >= 0;
 -1 x282 -1 x170 >= -1;
 +1 x210 -1 x283 >= 0;
 +1 x244 -1 x283 >= 0;
 -1 x283 -1 x170 >= -1;
 +1 x213 -1 x284 >= 0;
 +1 x246 -1 x284 >= 0;
 -1 x284 -1 x170 >= -1;
 +1 x216 -1 x285 >= 0;
 +1 x248 -1 x285 >= 0;
 -1 x170 -1 x285 >= -1;
 +1 x218 -1 x286 >= 0;
 +1 x250 -1 x286 >= 0;
 -1 x286 -1 x102 >= -1;
 +1 x220 -1 x287 >= 0;
 +1 x252 -1 x287 >= 0;
 -1 x287 -1 x102 >= -1;
 +1 x222 -1 x288 >= 0;
 +1 x254 -1 x288 >= 0;
 -1 x288 -1 x102 >= -1;
 +1 x224 -1 x289 >= 0;
 +1 x256 -1 x289 >= 0;
 -1 x289 -1 x102 >= -1;
 +1 x242 -1 x290 >= 0;
 +1 x206 -1 x290 >= 0;
 -1 x290 -1 x46 >= -1;
 +1 x244 -1 x291 >= 0;
 +1 x209 -1 x291 >= 0;
 -1 x291 -1 x46 >= -1;
 +1 x246 -1 x292 >= 0;
 +1 x212 -1 x292 >= 0;
 -1 x46 -1 x292 >= -1;
 +1 x248 -1 x293 >= 0;
 +1 x215 -1 x293 >= 0;
 -1 x46 -1 x293 >= -1;
 +1 x206 -1 x294 >= 0;
 +1 x250 -1 x294 >= 0;
 -1 x294 -1 x179 >= -1;
 +1 x209 -1 x295 >= 0;
 +1 x252 -1 x295 >= 0;
 -1 x295 -1 x179 >= -1;
 +1 x212 -1 x296 >= 0;
 +1 x254 -1 x296 >= 0;
 -1 x296 -1 x179 >= -1;
 +1 x215 -1 x297 >= 0;
 +1 x256 -1 x297 >= 0;
 -1 x179 -1 x297 >= -1;
 +1 x226 -1 x298 >= 0;
 +1 x242 -1 x298 >= 0;
 -1 x67 -1 x298 >= -1;
 +1 x228 -1 x299 >= 0;
 +1 x244 -1 x299 >= 0;
 -1 x299 -1 x67 >= -1;
 +1 x230 -1 x300 >= 0;
 +1 x246 -1 x300 >= 0;
 -1 x67 -1 x300 >= -1;
 +1 x232 -1 x301 >= 0;
 +1 x248 -1 x301 >= 0;
 -1 x67 -1 x301 >= -1;
 +1 x207 -1 x302 >= 0;
 +1 x195 -1 x302 >= 0;
 -1 x155 -1 x302 >= -1;
 +1 x210 -1 x303 >= 0;
 +1 x198 -1 x303 >= 0;
 -1 x155 -1 x303 >= -1;
 +1 x213 -1 x304 >= 0;
 +1 x201 -1 x304 >= 0;
 -1 x155 -1 x304 >= -1;
 +1 x216 -1 x305 >= 0;
 +1 x204 -1 x305 >= 0;
 -1 x155 -1 x305 >= -1;
 -1 x194 +1 x307 >= 0;
 -1 x218 +1 x307 >= 0;
 -1 x195 +1 x307 >= 0;
 -1 x242 +1 x307 >= 0;
 -1 x206 +1 x307 >= 0;
 -1 x226 +1 x307 >= 0;
 -1 x250 +1 x307 >= 0;
 -1 x207 +1 x307 >= 0;
 +1 x306 -1 x307 >= 0;
 -1 x197 +1 x309 >= 0;
 -1 x220 +1 x309 >= 0;
 -1 x198 +1 x309 >= 0;
 -1 x244 +1 x309 >= 0;
 -1 x209 +1 x309 >= 0;
 -1 x228 +1 x309 >= 0;
 -1 x252 +1 x309 >= 0;
 -1 x210 +1 x309 >= 0;
 +1 x308 -1 x309 >= 0;
 -1 x200 +1 x311 >= 0;
 -1 x222 +1 x311 >= 0;
 -1 x201 +1 x311 >= 0;
 -1 x246 +1 x311 >= 0;
 -1 x212 +1 x311 >= 0;
 -1 x230 +1 x311 >= 0;
 -1 x254 +1 x311 >= 0;
 -1 x213 +1 x311 >= 0;
 +1 x310 -1 x311 >= 0;
 -1 x203 +1 x313 >= 0;
 -1 x224 +1 x313 >= 0;
 -1 x204 +1 x313 >= 0;
 -1 x248 +1 x313 >= 0;
 -1 x215 +1 x313 >= 0;
 -1 x232 +1 x313 >= 0;
 -1 x256 +1 x313 >= 0;
 -1 x216 +1 x313 >= 0;
 -1 x313 +1 x312 >= 0;
 +1 x314 -1 x316 >= 0;
 +1 x315 -1 x316 >= 0;
 +1 x314 -1 x317 >= 0;
 +1 x315 -1 x317 >= 0;
 +1 x318 -1 x320 >= 0;
 +1 x319 -1 x320 >= 0;
 +1 x318 -1 x321 >= 0;
 +1 x319 -1 x321 >= 0;
 +1 x322 -1 x324 >= 0;
 +1 x323 -1 x324 >= 0;
 +1 x322 -1 x325 >= 0;
 +1 x323 -1 x325 >= 0;
 +1 x326 -1 x328 >= 0;
 +1 x327 -1 x328 >= 0;
 +1 x326 -1 x329 >= 0;
 +1 x327 -1 x329 >= 0;
 +1 x330 -1 x332 >= 0;
 +1 x331 -1 x332 >= 0;
 +1 x330 -1 x333 >= 0;
 +1 x331 -1 x333 >= 0;
 +1 x334 -1 x336 >= 0;
 +1 x335 -1 x336 >= 0;
 +1 x334 -1 x337 >= 0;
 +1 x335 -1 x337 >= 0;
 +1 x338 -1 x340 >= 0;
 +1 x339 -1 x340 >= 0;
 +1 x338 -1 x341 >= 0;
 +1 x339 -1 x341 >= 0;
 +1 x342 -1 x344 >= 0;
 +1 x343 -1 x344 >= 0;
 +1 x342 -1 x345 >= 0;
 +1 x343 -1 x345 >= 0;
 -1 x5 -1 x346 >= -1;
 +1 x6 -1 x346 >= 0;
 -1 x347 +1 x346 >= 0;
 +1 x347 -1 x346 >= 0;
 -1 x2 -1 x348 >= -1;
 +1 x5 -1 x348 >= 0;
 +1 x348 -1 x349 >= 0;
 +1 x349 -1 x348 >= 0;
 -1 x3 -1 x350 >= -1;
 +1 x2 -1 x350 >= 0;
 -1 x351 +1 x350 >= 0;
 -1 x350 +1 x351 >= 0;
 -1 x4 -1 x352 >= -1;
 +1 x3 -1 x352 >= 0;
 +1 x352 -1 x353 >= 0;
 +1 x353 -1 x352 >= 0;
 -1 x354 +1 x4 >= 0;
 -1 x4 +1 x354 >= 0;
 -1 x10 -1 x355 >= -1;
 +1 x11 -1 x355 >= 0;
 +1 x355 -1 x356 >= 0;
 -1 x355 +1 x356 >= 0;
 -1 x7 -1 x357 >= -1;
 +1 x10 -1 x357 >= 0;
 +1 x357 -1 x358 >= 0;
 -1 x357 +1 x358 >= 0;
 -1 x8 -1 x359 >= -1;
 +1 x7 -1 x359 >= 0;
 -1 x360 +1 x359 >= 0;
 -1 x359 +1 x360 >= 0;
 -1 x9 -1 x361 >= -1;
 +1 x8 -1 x361 >= 0;
 -1 x362 +1 x361 >= 0;
 +1 x362 -1 x361 >= 0;
 -1 x363 +1 x9 >= 0;
 +1 x363 -1 x9 >= 0;
 -1 x15 -1 x364 >= -1;
 +1 x16 -1 x364 >= 0;
 -1 x365 +1 x364 >= 0;
 +1 x365 -1 x364 >= 0;
 -1 x12 -1 x366 >= -1;
 +1 x15 -1 x366 >= 0;
 -1 x367 +1 x366 >= 0;
 +1 x367 -1 x366 >= 0;
 -1 x13 -1 x368 >= -1;
 +1 x12 -1 x368 >= 0;
 -1 x369 +1 x368 >= 0;
 -1 x368 +1 x369 >= 0;
 -1 x14 -1 x370 >= -1;
 +1 x13 -1 x370 >= 0;
 +1 x370 -1 x371 >= 0;
 -1 x370 +1 x371 >= 0;
 +1 x14 -1 x372 >= 0;
 +1 x372 -1 x14 >= 0;
 -1 x20 -1 x373 >= -1;
 +1 x21 -1 x373 >= 0;
 -1 x374 +1 x373 >= 0;
 -1 x373 +1 x374 >= 0;
 -1 x17 -1 x375 >= -1;
 +1 x20 -1 x375 >= 0;
 +1 x375 -1 x376 >= 0;
 +1 x376 -1 x375 >= 0;
 -1 x18 -1 x377 >= -1;
 +1 x17 -1 x377 >= 0;
 -1 x378 +1 x377 >= 0;
 -1 x377 +1 x378 >= 0;
 -1 x19 -1 x379 >= -1;
 +1 x18 -1 x379 >= 0;
 +1 x379 -1 x380 >= 0;
 +1 x380 -1 x379 >= 0;
 -1 x381 +1 x19 >= 0;
 +1 x381 -1 x19 >= 0;
 -1 x25 -1 x382 >= -1;
 +1 x26 -1 x382 >= 0;
 -1 x383 +1 x382 >= 0;
 -1 x382 +1 x383 >= 0;
 -1 x22 -1 x384 >= -1;
 +1 x25 -1 x384 >= 0;
 +1 x384 -1 x385 >= 0;
 +1 x385 -1 x384 >= 0;
 -1 x23 -1 x386 >= -1;
 +1 x22 -1 x386 >= 0;
 -1 x387 +1 x386 >= 0;
 -1 x386 +1 x387 >= 0;
 -1 x24 -1 x388 >= -1;
 +1 x23 -1 x388 >= 0;
 +1 x388 -1 x389 >= 0;
 +1 x389 -1 x388 >= 0;
 +1 x24 -1 x390 >= 0;
 +1 x390 -1 x24 >= 0;
 -1 x30 -1 x391 >= -1;
 +1 x31 -1 x391 >= 0;
 +1 x391 -1 x392 >= 0;
 -1 x391 +1 x392 >= 0;
 -1 x27 -1 x393 >= -1;
 +1 x30 -1 x393 >= 0;
 -1 x394 +1 x393 >= 0;
 +1 x394 -1 x393 >= 0;
 -1 x28 -1 x395 >= -1;
 +1 x27 -1 x395 >= 0;
 -1 x396 +1 x395 >= 0;
 +1 x396 -1 x395 >= 0;
 -1 x29 -1 x397 >= -1;
 +1 x28 -1 x397 >= 0;
 +1 x397 -1 x398 >= 0;
 +1 x398 -1 x397 >= 0;
 -1 x399 +1 x29 >= 0;
 +1 x399 -1 x29 >= 0;
 -1 x35 -1 x400 >= -1;
 +1 x36 -1 x400 >= 0;
 -1 x401 +1 x400 >= 0;
 -1 x400 +1 x401 >= 0;
 -1 x32 -1 x402 >= -1;
 +1 x35 -1 x402 >= 0;
 +1 x402 -1 x403 >= 0;
 -1 x402 +1 x403 >= 0;
 -1 x33 -1 x404 >= -1;
 +1 x32 -1 x404 >= 0;
 +1 x404 -1 x405 >= 0;
 -1 x404 +1 x405 >= 0;
 -1 x34 -1 x406 >= -1;
 +1 x33 -1 x406 >= 0;
 +1 x406 -1 x407 >= 0;
 -1 x406 +1 x407 >= 0;
 +1 x34 -1 x408 >= 0;
 +1 x408 -1 x34 >= 0;
 -1 x40 -1 x409 >= -1;
 +1 x41 -1 x409 >= 0;
 -1 x410 +1 x409 >= 0;
 -1 x409 +1 x410 >= 0;
 -1 x37 -1 x411 >= -1;
 +1 x40 -1 x411 >= 0;
 +1 x411 -1 x412 >= 0;
 +1 x412 -1 x411 >= 0;
 -1 x38 -1 x413 >= -1;
 +1 x37 -1 x413 >= 0;
 -1 x414 +1 x413 >= 0;
 -1 x413 +1 x414 >= 0;
 -1 x39 -1 x415 >= -1;
 +1 x38 -1 x415 >= 0;
 -1 x416 +1 x415 >= 0;
 +1 x416 -1 x415 >= 0;
 -1 x417 +1 x39 >= 0;
 +1 x417 -1 x39 >= 0;
 +1 x42 -1 x19 -1 x24 >= -1;
 +1 x43 -1 x17 -1 x24 >= -1;
 +1 x44 -1 x19 -1 x22 >= -1;
 -1 x45 +1 x44 +1 x43 >= 0;
 -1 x46 -1 x45 +1 x47 >= -1;
 -1 x46 +1 x45 -1 x47 >= -1;
 +1 x46 -1 x42 +1 x47 >= 0;
 +1 x46 +1 x42 -1 x47 >= 0;
 -1 x45 -1 x42 +1 x47 >= -1;
 +1 x45 +1 x42 -1 x47 >= 0;
 +1 x49 -1 x34 -1 x14 >= -1;
 +1 x50 -1 x32 -1 x14 >= -1;
 +1 x51 -1 x34 -1 x12 >= -1;
 -1 x52 +1 x51 +1 x50 >= 0;
 -1 x53 -1 x52 +1 x54 >= -1;
 -1 x53 +1 x52 -1 x54 >= -1;
 +1 x53 -1 x49 +1 x54 >= 0;
 +1 x53 +1 x49 -1 x54 >= 0;
 -1 x52 -1 x49 +1 x54 >= -1;
 +1 x52 +1 x49 -1 x54 >= 0;
 +1 x56 -1 x34 -1 x24 >= -1;
 +1 x57 -1 x32 -1 x24 >= -1;
 +1 x58 -1 x34 -1 x22 >= -1;
 -1 x59 +1 x58 +1 x57 >= 0;
 -1 x60 -1 x59 +1 x61 >= -1;
 -1 x60 +1 x59 -1 x61 >= -1;
 +1 x60 -1 x56 +1 x61 >= 0;
 +1 x60 +1 x56 -1 x61 >= 0;
 -1 x59 -1 x56 +1 x61 >= -1;
 +1 x59 +1 x56 -1 x61 >= 0;
 +1 x63 -1 x24 -1 x14 >= -1;
 +1 x64 -1 x22 -1 x14 >= -1;
 +1 x65 -1 x24 -1 x12 >= -1;
 -1 x66 +1 x65 +1 x64 >= 0;
 -1 x67 -1 x66 +1 x68 >= -1;
 -1 x67 +1 x66 -1 x68 >= -1;
 +1 x67 -1 x63 +1 x68 >= 0;
 +1 x67 +1 x63 -1 x68 >= 0;
 -1 x66 -1 x63 +1 x68 >= -1;
 +1 x66 +1 x63 -1 x68 >= 0;
 +1 x69 +1 x55 +1 x62 >= 1;
 +1 x70 -1 x4 -1 x14 >= -1;
 +1 x71 -1 x2 -1 x14 >= -1;
 +1 x72 -1 x4 -1 x12 >= -1;
 -1 x73 +1 x72 +1 x71 >= 0;
 -1 x74 -1 x73 +1 x75 >= -1;
 -1 x74 +1 x73 -1 x75 >= -1;
 +1 x74 -1 x70 +1 x75 >= 0;
 +1 x74 +1 x70 -1 x75 >= 0;
 -1 x73 -1 x70 +1 x75 >= -1;
 +1 x73 +1 x70 -1 x75 >= 0;
 +1 x77 -1 x39 -1 x4 >= -1;
 +1 x78 -1 x37 -1 x4 >= -1;
 +1 x79 -1 x39 -1 x2 >= -1;
 -1 x80 +1 x79 +1 x78 >= 0;
 -1 x81 -1 x80 +1 x82 >= -1;
 -1 x81 +1 x80 -1 x82 >= -1;
 +1 x81 -1 x77 +1 x82 >= 0;
 +1 x81 +1 x77 -1 x82 >= 0;
 -1 x80 -1 x77 +1 x82 >= -1;
 +1 x80 +1 x77 -1 x82 >= 0;
 +1 x84 -1 x39 -1 x19 >= -1;
 +1 x85 -1 x37 -1 x19 >= -1;
 +1 x86 -1 x39 -1 x17 >= -1;
 -1 x87 +1 x86 +1 x85 >= 0;
 -1 x88 -1 x87 +1 x89 >= -1;
 -1 x88 +1 x87 -1 x89 >= -1;
 +1 x88 -1 x84 +1 x89 >= 0;
 +1 x88 +1 x84 -1 x89 >= 0;
 -1 x87 -1 x84 +1 x89 >= -1;
 +1 x87 +1 x84 -1 x89 >= 0;
 +1 x91 -1 x19 -1 x4 >= -1;
 +1 x92 -1 x17 -1 x4 >= -1;
 +1 x93 -1 x19 -1 x2 >= -1;
 -1 x94 +1 x93 +1 x92 >= 0;
 -1 x95 -1 x94 +1 x96 >= -1;
 -1 x95 +1 x94 -1 x96 >= -1;
 +1 x95 -1 x91 +1 x96 >= 0;
 +1 x95 +1 x91 -1 x96 >= 0;
 -1 x94 -1 x91 +1 x96 >= -1;
 +1 x94 +1 x91 -1 x96 >= 0;
 +1 x97 +1 x90 +1 x83 >= 1;
 +1 x98 -1 x9 -1 x39 >= -1;
 +1 x99 -1 x7 -1 x39 >= -1;
 +1 x100 -1 x9 -1 x37 >= -1;
 -1 x101 +1 x100 +1 x99 >= 0;
 -1 x102 -1 x101 +1 x103 >= -1;
 -1 x102 +1 x101 -1 x103 >= -1;
 +1 x102 -1 x98 +1 x103 >= 0;
 +1 x102 +1 x98 -1 x103 >= 0;
 -1 x101 -1 x98 +1 x103 >= -1;
 +1 x101 +1 x98 -1 x103 >= 0;
 +1 x105 -1 x29 -1 x39 >= -1;
 +1 x106 -1 x27 -1 x39 >= -1;
 +1 x107 -1 x29 -1 x37 >= -1;
 -1 x108 +1 x107 +1 x106 >= 0;
 -1 x109 -1 x108 +1 x110 >= -1;
 -1 x109 +1 x108 -1 x110 >= -1;
 +1 x109 -1 x105 +1 x110 >= 0;
 +1 x109 +1 x105 -1 x110 >= 0;
 -1 x108 -1 x105 +1 x110 >= -1;
 +1 x108 +1 x105 -1 x110 >= 0;
 +1 x112 -1 x34 -1 x39 >= -1;
 +1 x113 -1 x32 -1 x39 >= -1;
 +1 x114 -1 x34 -1 x37 >= -1;
 -1 x115 +1 x114 +1 x113 >= 0;
 -1 x116 -1 x115 +1 x117 >= -1;
 -1 x116 +1 x115 -1 x117 >= -1;
 +1 x116 -1 x112 +1 x117 >= 0;
 +1 x116 +1 x112 -1 x117 >= 0;
 -1 x115 -1 x112 +1 x117 >= -1;
 +1 x115 +1 x112 -1 x117 >= 0;
 +1 x119 -1 x29 -1 x9 >= -1;
 +1 x120 -1 x27 -1 x9 >= -1;
 +1 x121 -1 x29 -1 x7 >= -1;
 -1 x122 +1 x121 +1 x120 >= 0;
 -1 x123 -1 x122 +1 x124 >= -1;
 -1 x123 +1 x122 -1 x124 >= -1;
 +1 x123 -1 x119 +1 x124 >= 0;
 +1 x123 +1 x119 -1 x124 >= 0;
 -1 x122 -1 x119 +1 x124 >= -1;
 +1 x122 +1 x119 -1 x124 >= 0;
 +1 x126 -1 x34 -1 x9 >= -1;
 +1 x127 -1 x32 -1 x9 >= -1;
 +1 x128 -1 x34 -1 x7 >= -1;
 -1 x129 +1 x128 +1 x127 >= 0;
 -1 x130 -1 x129 +1 x131 >= -1;
 -1 x130 +1 x129 -1 x131 >= -1;
 +1 x130 -1 x126 +1 x131 >= 0;
 +1 x130 +1 x126 -1 x131 >= 0;
 -1 x129 -1 x126 +1 x131 >= -1;
 +1 x129 +1 x126 -1 x131 >= 0;
 +1 x133 -1 x34 -1 x29 >= -1;
 +1 x134 -1 x32 -1 x29 >= -1;
 +1 x135 -1 x34 -1 x27 >= -1;
 -1 x136 +1 x135 +1 x134 >= 0;
 -1 x137 -1 x136 +1 x138 >= -1;
 -1 x137 +1 x136 -1 x138 >= -1;
 +1 x137 -1 x133 +1 x138 >= 0;
 +1 x137 +1 x133 -1 x138 >= 0;
 -1 x136 -1 x133 +1 x138 >= -1;
 +1 x136 +1 x133 -1 x138 >= 0;
 +1 x141 -1 x9 -1 x14 >= -1;
 +1 x142 -1 x7 -1 x14 >= -1;
 +1 x143 -1 x9 -1 x12 >= -1;
 -1 x144 +1 x143 +1 x142 >= 0;
 -1 x145 -1 x144 +1 x146 >= -1;
 -1 x145 +1 x144 -1 x146 >= -1;
 +1 x145 -1 x141 +1 x146 >= 0;
 +1 x145 +1 x141 -1 x146 >= 0;
 -1 x144 -1 x141 +1 x146 >= -1;
 +1 x144 +1 x141 -1 x146 >= 0;
 +1 x147 +1 x148 +1 x140 >= 1;
 +1 x151 -1 x29 -1 x4 >= -1;
 +1 x152 -1 x27 -1 x4 >= -1;
 +1 x153 -1 x29 -1 x2 >= -1;
 -1 x154 +1 x153 +1 x152 >= 0;
 -1 x155 -1 x154 +1 x156 >= -1;
 -1 x155 +1 x154 -1 x156 >= -1;
 +1 x155 -1 x151 +1 x156 >= 0;
 +1 x155 +1 x151 -1 x156 >= 0;
 -1 x154 -1 x151 +1 x156 >= -1;
 +1 x154 +1 x151 -1 x156 >= 0;
 +1 x157 +1 x149 +1 x150 >= 1;
 +1 x159 -1 x29 -1 x24 >= -1;
 +1 x160 -1 x27 -1 x24 >= -1;
 +1 x161 -1 x29 -1 x22 >= -1;
 -1 x162 +1 x161 +1 x160 >= 0;
 -1 x163 -1 x162 +1 x164 >= -1;
 -1 x163 +1 x162 -1 x164 >= -1;
 +1 x163 -1 x159 +1 x164 >= 0;
 +1 x163 +1 x159 -1 x164 >= 0;
 -1 x162 -1 x159 +1 x164 >= -1;
 +1 x162 +1 x159 -1 x164 >= 0;
 +1 x166 -1 x24 -1 x4 >= -1;
 +1 x167 -1 x22 -1 x4 >= -1;
 +1 x168 -1 x24 -1 x2 >= -1;
 -1 x169 +1 x168 +1 x167 >= 0;
 -1 x170 -1 x169 +1 x171 >= -1;
 -1 x170 +1 x169 -1 x171 >= -1;
 +1 x170 -1 x166 +1 x171 >= 0;
 +1 x170 +1 x166 -1 x171 >= 0;
 -1 x169 -1 x166 +1 x171 >= -1;
 +1 x169 +1 x166 -1 x171 >= 0;
 +1 x165 +1 x172 +1 x158 >= 1;
 +1 x175 -1 x9 -1 x19 >= -1;
 +1 x176 -1 x7 -1 x19 >= -1;
 +1 x177 -1 x9 -1 x17 >= -1;
 -1 x178 +1 x177 +1 x176 >= 0;
 -1 x179 -1 x178 +1 x180 >= -1;
 -1 x179 +1 x178 -1 x180 >= -1;
 +1 x179 -1 x175 +1 x180 >= 0;
 +1 x179 +1 x175 -1 x180 >= 0;
 -1 x178 -1 x175 +1 x180 >= -1;
 +1 x178 +1 x175 -1 x180 >= 0;
 +1 x174 +1 x173 +1 x181 >= 1;
 +1 x184 -1 x19 -1 x14 >= -1;
 +1 x185 -1 x17 -1 x14 >= -1;
 +1 x186 -1 x19 -1 x12 >= -1;
 -1 x187 +1 x186 +1 x185 >= 0;
 -1 x188 -1 x187 +1 x189 >= -1;
 -1 x188 +1 x187 -1 x189 >= -1;
 +1 x188 -1 x184 +1 x189 >= 0;
 +1 x188 +1 x184 -1 x189 >= 0;
 -1 x187 -1 x184 +1 x189 >= -1;
 +1 x187 +1 x184 -1 x189 >= 0;
 +1 x182 +1 x190 +1 x183 >= 1;
 +1 x192 +1 x193 +1 x191 >= 1;
 +1 x196 -1 x195 -1 x194 >= -1;
 +1 x199 -1 x198 -1 x197 >= -1;
 +1 x202 -1 x201 -1 x200 >= -1;
 +1 x205 -1 x204 -1 x203 >= -1;
 +1 x208 -1 x207 -1 x206 >= -1;
 +1 x211 -1 x210 -1 x209 >= -1;
 +1 x214 -1 x213 -1 x212 >= -1;
 +1 x217 -1 x216 -1 x215 >= -1;
 +1 x219 -1 x218 -1 x195 >= -1;
 +1 x221 -1 x220 -1 x198 >= -1;
 +1 x223 -1 x222 -1 x201 >= -1;
 +1 x225 -1 x224 -1 x204 >= -1;
 +1 x227 -1 x226 -1 x206 >= -1;
 +1 x229 -1 x228 -1 x209 >= -1;
 +1 x231 -1 x230 -1 x212 >= -1;
 +1 x233 -1 x232 -1 x215 >= -1;
 +1 x234 -1 x226 -1 x194 >= -1;
 +1 x235 -1 x228 -1 x197 >= -1;
 +1 x236 -1 x230 -1 x200 >= -1;
 +1 x237 -1 x232 -1 x203 >= -1;
 +1 x238 -1 x226 -1 x207 >= -1;
 +1 x239 -1 x228 -1 x210 >= -1;
 +1 x240 -1 x230 -1 x213 >= -1;
 +1 x241 -1 x232 -1 x216 >= -1;
 +1 x243 -1 x242 -1 x195 >= -1;
 +1 x245 -1 x244 -1 x198 >= -1;
 +1 x247 -1 x246 -1 x201 >= -1;
 +1 x249 -1 x248 -1 x204 >= -1;
 +1 x251 -1 x226 -1 x250 >= -1;
 +1 x253 -1 x228 -1 x252 >= -1;
 +1 x255 -1 x230 -1 x254 >= -1;
 +1 x257 -1 x232 -1 x256 >= -1;
 +1 x258 -1 x250 -1 x195 >= -1;
 +1 x259 -1 x252 -1 x198 >= -1;
 +1 x260 -1 x254 -1 x201 >= -1;
 +1 x261 -1 x256 -1 x204 >= -1;
 +1 x262 -1 x218 -1 x194 >= -1;
 +1 x263 -1 x220 -1 x197 >= -1;
 +1 x264 -1 x222 -1 x200 >= -1;
 +1 x265 -1 x224 -1 x203 >= -1;
 +1 x266 -1 x242 -1 x194 >= -1;
 +1 x267 -1 x244 -1 x197 >= -1;
 +1 x268 -1 x246 -1 x200 >= -1;
 +1 x269 -1 x248 -1 x203 >= -1;
 +1 x270 -1 x207 -1 x218 >= -1;
 +1 x271 -1 x210 -1 x220 >= -1;
 +1 x272 -1 x213 -1 x222 >= -1;
 +1 x273 -1 x216 -1 x224 >= -1;
 +1 x274 -1 x206 -1 x218 >= -1;
 +1 x275 -1 x209 -1 x220 >= -1;
 +1 x276 -1 x212 -1 x222 >= -1;
 +1 x277 -1 x215 -1 x224 >= -1;
 +1 x278 -1 x250 -1 x194 >= -1;
 +1 x279 -1 x252 -1 x197 >= -1;
 +1 x280 -1 x254 -1 x200 >= -1;
 +1 x281 -1 x256 -1 x203 >= -1;
 +1 x282 -1 x207 -1 x242 >= -1;
 +1 x283 -1 x210 -1 x244 >= -1;
 +1 x284 -1 x213 -1 x246 >= -1;
 +1 x285 -1 x216 -1 x248 >= -1;
 +1 x286 -1 x218 -1 x250 >= -1;
 +1 x287 -1 x220 -1 x252 >= -1;
 +1 x288 -1 x222 -1 x254 >= -1;
 +1 x289 -1 x224 -1 x256 >= -1;
 +1 x290 -1 x242 -1 x206 >= -1;
 +1 x291 -1 x244 -1 x209 >= -1;
 +1 x292 -1 x246 -1 x212 >= -1;
 +1 x293 -1 x248 -1 x215 >= -1;
 +1 x294 -1 x206 -1 x250 >= -1;
 +1 x295 -1 x209 -1 x252 >= -1;
 +1 x296 -1 x212 -1 x254 >= -1;
 +1 x297 -1 x215 -1 x256 >= -1;
 +1 x298 -1 x226 -1 x242 >= -1;
 +1 x299 -1 x228 -1 x244 >= -1;
 +1 x300 -1 x230 -1 x246 >= -1;
 +1 x301 -1 x232 -1 x248 >= -1;
 +1 x302 -1 x207 -1 x195 >= -1;
 +1 x303 -1 x210 -1 x198 >= -1;
 +1 x304 -1 x213 -1 x201 >= -1;
 +1 x305 -1 x216 -1 x204 >= -1;
 +1 x316 -1 x314 -1 x315 >= -1;
 +1 x317 -1 x314 -1 x315 >= -1;
 +1 x320 -1 x318 -1 x319 >= -1;
 +1 x321 -1 x318 -1 x319 >= -1;
 +1 x324 -1 x322 -1 x323 >= -1;
 +1 x325 -1 x322 -1 x323 >= -1;
 +1 x328 -1 x326 -1 x327 >= -1;
 +1 x329 -1 x326 -1 x327 >= -1;
 +1 x332 -1 x330 -1 x331 >= -1;
 +1 x333 -1 x330 -1 x331 >= -1;
 +1 x336 -1 x334 -1 x335 >= -1;
 +1 x337 -1 x334 -1 x335 >= -1;
 +1 x340 -1 x338 -1 x339 >= -1;
 +1 x341 -1 x338 -1 x339 >= -1;
 +1 x344 -1 x342 -1 x343 >= -1;
 +1 x345 -1 x342 -1 x343 >= -1;
 +1 x60 +1 x53 +1 x67 >= 1;
 +1 x88 +1 x81 +1 x95 >= 1;
 +1 x53 +1 x130 +1 x145 >= 1;
 +1 x109 +1 x81 +1 x155 >= 1;
 +1 x170 +1 x155 +1 x163 >= 1;
 +1 x88 +1 x179 +1 x102 >= 1;
 +1 x179 +1 x188 +1 x145 >= 1;
 +1 x60 +1 x137 +1 x163 >= 1;
 +1 x346 +1 x5 -1 x6 >= 0;
 +1 x348 +1 x2 -1 x5 >= 0;
 +1 x350 +1 x3 -1 x2 >= 0;
 +1 x352 +1 x4 -1 x3 >= 0;
 +1 x355 +1 x10 -1 x11 >= 0;
 +1 x357 +1 x7 -1 x10 >= 0;
 +1 x359 +1 x8 -1 x7 >= 0;
 +1 x361 +1 x9 -1 x8 >= 0;
 +1 x364 +1 x15 -1 x16 >= 0;
 +1 x366 +1 x12 -1 x15 >= 0;
 +1 x368 +1 x13 -1 x12 >= 0;
 +1 x370 +1 x14 -1 x13 >= 0;
 +1 x373 +1 x20 -1 x21 >= 0;
 +1 x375 +1 x17 -1 x20 >= 0;
 +1 x377 +1 x18 -1 x17 >= 0;
 +1 x379 +1 x19 -1 x18 >= 0;
 +1 x382 +1 x25 -1 x26 >= 0;
 +1 x384 +1 x22 -1 x25 >= 0;
 +1 x386 +1 x23 -1 x22 >= 0;
 +1 x388 +1 x24 -1 x23 >= 0;
 +1 x391 +1 x30 -1 x31 >= 0;
 +1 x393 +1 x27 -1 x30 >= 0;
 +1 x395 +1 x28 -1 x27 >= 0;
 +1 x397 +1 x29 -1 x28 >= 0;
 +1 x400 +1 x35 -1 x36 >= 0;
 +1 x402 +1 x32 -1 x35 >= 0;
 +1 x404 +1 x33 -1 x32 >= 0;
 +1 x406 +1 x34 -1 x33 >= 0;
 +1 x409 +1 x40 -1 x41 >= 0;
 +1 x411 +1 x37 -1 x40 >= 0;
 +1 x413 +1 x38 -1 x37 >= 0;
 +1 x415 +1 x39 -1 x38 >= 0;
 +1 x125 +1 x132 +1 x118 +1 x104 +1 x139 +1 x111 >= 1;
 -1 x306 +1 x206 +1 x226 +1 x194 +1 x250 +1 x218 +1 x207 +1 x242 +1 x195 >= 0;
 +1 x206 +1 x226 +1 x194 +1 x250 +1 x218 -1 x307 +1 x207 +1 x242 +1 x195 >= 0;
 +1 x228 +1 x220 +1 x252 +1 x197 +1 x244 +1 x198 +1 x209 -1 x308 +1 x210 >= 0;
 +1 x228 +1 x220 +1 x252 +1 x197 +1 x244 -1 x309 +1 x198 +1 x209 +1 x210 >= 0;
 -1 x310 +1 x201 +1 x212 +1 x230 +1 x213 +1 x246 +1 x200 +1 x254 +1 x222 >= 0;
 +1 x201 +1 x212 +1 x230 +1 x213 +1 x246 +1 x200 +1 x254 -1 x311 +1 x222 >= 0;
 +1 x216 +1 x248 +1 x224 +1 x256 +1 x204 -1 x312 +1 x203 +1 x215 +1 x232 >= 0;
 -1 x313 +1 x216 +1 x248 +1 x224 +1 x256 +1 x204 +1 x203 +1 x215 +1 x232 >= 0;
 +1 x116 +1 x102 +1 x137 +1 x109 +1 x130 +1 x123 >= 1;
-1 x216 -1 x213 -1 x210 -1 x207 +4 x314 >= 0;
+1 x216 +1 x213 +1 x210 +1 x207 -4 x314 >= -3;
+1 x216 +1 x213 +1 x210 +1 x207 +2 x315 >= 2;
-1 x216 -1 x213 -1 x210 -1 x207 -4 x315 >= -5;
-1 x256 -1 x254 -1 x252 -1 x250 +4 x318 >= 0;
+1 x256 +1 x254 +1 x252 +1 x250 -4 x318 >= -3;
+1 x256 +1 x254 +1 x252 +1 x250 +2 x319 >= 2;
-1 x256 -1 x254 -1 x252 -1 x250 -4 x319 >= -5;
-1 x232 -1 x230 -1 x228 -1 x226 +4 x322 >= 0;
+1 x232 +1 x230 +1 x228 +1 x226 -4 x322 >= -3;
+1 x232 +1 x230 +1 x228 +1 x226 +2 x323 >= 2;
-1 x232 -1 x230 -1 x228 -1 x226 -4 x323 >= -5;
-1 x215 -1 x212 -1 x209 -1 x206 +4 x326 >= 0;
+1 x215 +1 x212 +1 x209 +1 x206 -4 x326 >= -3;
+1 x215 +1 x212 +1 x209 +1 x206 +2 x327 >= 2;
-1 x215 -1 x212 -1 x209 -1 x206 -4 x327 >= -5;
-1 x248 -1 x246 -1 x244 -1 x242 +4 x330 >= 0;
+1 x248 +1 x246 +1 x244 +1 x242 -4 x330 >= -3;
+1 x248 +1 x246 +1 x244 +1 x242 +2 x331 >= 2;
-1 x248 -1 x246 -1 x244 -1 x242 -4 x331 >= -5;
-1 x204 -1 x201 -1 x198 -1 x195 +4 x334 >= 0;
+1 x204 +1 x201 +1 x198 +1 x195 -4 x334 >= -3;
+1 x204 +1 x201 +1 x198 +1 x195 +2 x335 >= 2;
-1 x204 -1 x201 -1 x198 -1 x195 -4 x335 >= -5;
-1 x203 -1 x200 -1 x197 -1 x194 +4 x338 >= 0;
+1 x203 +1 x200 +1 x197 +1 x194 -4 x338 >= -3;
+1 x203 +1 x200 +1 x197 +1 x194 +2 x339 >= 2;
-1 x203 -1 x200 -1 x197 -1 x194 -4 x339 >= -5;
-1 x224 -1 x222 -1 x220 -1 x218 +4 x342 >= 0;
+1 x224 +1 x222 +1 x220 +1 x218 -4 x342 >= -3;
+1 x224 +1 x222 +1 x220 +1 x218 +2 x343 >= 2;
-1 x224 -1 x222 -1 x220 -1 x218 -4 x343 >= -5;