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