\ Equation counts \ Total E G L N X C B \ 2371 75 2232 64 0 0 0 0 \ \ Variable counts \ x b i s1s s2s sc si \ Total cont binary integer sos1 sos2 scont sint \ 400 278 122 0 0 0 0 0 \ \ Nonzero counts \ Total const NL DLL \ 8251 8071 180 0 \ Minimize obj: 0 x1 + 0 x2 + 0 x3 + 0 x4 + 0 x5 + 0 x6 + 0 x7 + 0 x8 + 0 x9 + 0 x10 + 0 x11 + 0 x12 + 0 x13 + 0 x14 + 0 x15 + 0 x16 + 0 x17 + 0 x18 + 0 x19 + 0 x20 + 0 x21 + 0 x22 + 0 x23 + 0 x24 + 0 x25 + 0 x26 + 0 x27 + 0 x28 + 0 x29 + 0 x30 + 0 x31 + 0 x32 + 0 x33 + 0 x34 + 0 x35 + 0 x36 + 0 x37 + 0 x38 + 0 x39 + 0 x40 + 0 x41 + 0 x42 + 0 x43 + 0 x44 + 0 x45 + 0 x46 + 0 x47 + 0 x48 + 0 x49 + 0 x50 + 0 x51 + 0 x52 + 0 x53 + 0 x54 + 0 x55 + 0 x56 + 0 x57 + 0 x58 + 0 x59 + 0 x60 + 0 x61 + 0 x62 + 0 x63 + 0 x64 + 0 x65 + 0 x66 + 0 x67 + 0 x68 + 0 x69 + 0 x70 + 0 x71 + 0 x72 + 0 x73 + 0 x74 + 0 x75 + 0 b76 + 0 b77 + 0 b78 + 0 b79 + 0 b80 + 0 b81 + 0 b82 + 0 b83 + 0 b84 + 0 b85 + 0 b86 + 0 b87 + 0 b88 + 0 b89 + 0 b90 + 0 b91 + 0 b92 + 0 b93 + 0 b94 + 0 b95 + 0 b96 + 0 b97 + 0 b98 + 0 b99 + 0 b100 + 0 b101 + 0 b102 + 0 b103 + 0 b104 + 0 b105 + 0 b106 + 0 b107 + 0 b108 + 0 b109 + 0 b110 + 0 b111 + 0 b112 + 0 b113 + 0 b114 + 0 b115 + 0 b116 + 0 b117 + 0 b118 + 0 b119 + 0 b120 + 0 b121 + 0 b122 + 0 b123 + 0 b124 + 0 b125 + 0 b126 + 0 b127 + 0 b128 + 0 b129 + 0 b130 + 0 b131 + 0 b132 + 0 b133 + 0 b134 + 0 b135 + x136 + x137 + x138 + x139 + x140 + x141 + x142 + x143 + x144 + x145 + x146 + x147 + x148 + x149 + x150 + 0 x151 + 0 x152 + 0 x153 + 0 x154 + 0 x155 + 0 x156 + 0 x157 + 0 x158 + 0 x159 + 0 x160 + 0 x161 + 0 x162 + 0 x163 + 0 x164 + 0 x165 + 0 x166 + 0 x167 + 0 x168 + 0 x169 + 0 x170 + 0 x171 + 0 x172 + 0 x173 + 0 x174 + 0 x175 + 0 x176 + 0 x177 + 0 x178 + 0 x179 + 0 x180 + 0 x181 + 0 x182 + 0 x183 + 0 x184 + 0 x185 + 0 x186 + 0 x187 + 0 x188 + 0 x189 + 0 x190 + 0 x191 + 0 x192 + 0 x193 + 0 x194 + 0 x195 + 0 x196 + 0 x197 + 0 x198 + 0 x199 + 0 x200 + 0 x201 + 0 x202 + 0 x203 + 0 x204 + 0 x205 + 0 x206 + 0 x207 + 0 x208 + 0 x209 + 0 x210 + 0 x211 + 0 x212 + 0 x213 + 0 x214 + 0 x215 + 0 x216 + 0 x217 + 0 x218 + 0 x219 + 0 x220 + 0 x221 + 0 x222 + 0 x223 + 0 x224 + 0 x225 + 0 x226 + 0 x227 + 0 x228 + 0 x229 + 0 x230 + 0 x231 + 0 x232 + 0 x233 + 0 x234 + 0 x235 + 0 x236 + 0 x237 + 0 x238 + 0 x239 + 0 x240 + 0 x241 + 0 x242 + 0 x243 + 0 x244 + 0 x245 + 0 x246 + 0 x247 + 0 x248 + 0 x249 + 0 x250 + 0 x251 + 0 x252 + 0 x253 + 0 x254 + 0 x255 + 0 x256 + 0 x257 + 0 x258 + 0 x259 + 0 x260 + 0 x261 + 0 x262 + 0 x263 + 0 x264 + 0 x265 + 0 x266 + 0 x267 + 0 x268 + 0 x269 + 0 x270 + 0 x271 + 0 x272 + 0 x273 + 0 x274 + 0 x275 + 0 x276 + 0 x277 + 0 x278 + 0 x279 + 0 x280 + 0 x281 + 0 x282 + 0 x283 + 0 x284 + 0 x285 + 0 x286 + 0 x287 + 0 x288 + 0 x289 + 0 x290 + 0 x291 + 0 x292 + 0 x293 + 0 x294 + 0 x295 + 0 x296 + 0 x297 + 0 x298 + 0 x299 + 0 x300 + 0 x301 + 0 x302 + 0 x303 + 0 x304 + 0 x305 + 0 x306 + 0 x307 + 0 x308 + 0 x309 + 0 x310 + 0 x311 + 0 x312 + 0 x313 + 0 x314 + 0 x315 + 0 x316 + 0 x317 + 0 x318 + 0 x319 + 0 x320 + 0 x321 + 0 x322 + 0 x323 + 0 x324 + 0 x325 + 0 x326 + 0 x327 + 0 x328 + 0 x329 + 0 x330 + 0 x331 + 0 x332 + 0 x333 + 0 x334 + 0 x335 + 0 x336 + 0 x337 + 0 x338 + 0 b339 + 0 b340 + 0 b341 + 0 b342 + 0 b343 + 0 b344 + 0 b345 + 0 b346 + 0 b347 + 0 b348 + 0 b349 + 0 b350 + 0 b351 + 0 b352 + 0 b353 + 0 b354 + 0 b355 + 0 b356 + 0 b357 + 0 b358 + 0 b359 + 0 b360 + 0 b361 + 0 b362 + 0 b363 + 0 b364 + 0 b365 + 0 b366 + 0 b367 + 0 b368 + 0 b369 + 0 b370 + 0 b371 + 0 b372 + 0 b373 + 0 b374 + 0 b375 + 0 b376 + 0 b377 + 0 b378 + 0 b379 + 0 b380 + 0 b381 + 0 b382 + 0 b383 + 0 b384 + 0 b385 + 0 b386 + 0 b387 + 0 b388 + 0 b389 + 0 b390 + 0 b391 + 0 b392 + 0 b393 + 0 b394 + 0 b395 + 0 b396 + 0 b397 + 0 b398 + 0 b399 + 0 b400 Subject To e2: x279 - x1 x61 b76 >= 0 e3: x280 - x2 x61 b77 >= 0 e4: x281 - x3 x61 b78 >= 0 e5: x282 - x4 x61 b79 >= 0 e6: x283 - x5 x62 b80 >= 0 e7: x284 - x6 x62 b81 >= 0 e8: x285 - x7 x62 b82 >= 0 e9: x286 - x8 x62 b83 >= 0 e10: x287 - x9 x63 b84 >= 0 e11: x288 - x10 x63 b85 >= 0 e12: x289 - x11 x63 b86 >= 0 e13: x290 - x12 x63 b87 >= 0 e14: x291 - x13 x64 b88 >= 0 e15: x292 - x14 x64 b89 >= 0 e16: x293 - x15 x64 b90 >= 0 e17: x294 - x16 x64 b91 >= 0 e18: x295 - x17 x65 b92 >= 0 e19: x296 - x18 x65 b93 >= 0 e20: x297 - x19 x65 b94 >= 0 e21: x298 - x20 x65 b95 >= 0 e22: x299 - x21 x66 b96 >= 0 e23: x300 - x22 x66 b97 >= 0 e24: x301 - x23 x66 b98 >= 0 e25: x302 - x24 x66 b99 >= 0 e26: x303 - x25 x67 b100 >= 0 e27: x304 - x26 x67 b101 >= 0 e28: x305 - x27 x67 b102 >= 0 e29: x306 - x28 x67 b103 >= 0 e30: x307 - x29 x68 b104 >= 0 e31: x308 - x30 x68 b105 >= 0 e32: x309 - x31 x68 b106 >= 0 e33: x310 - x32 x68 b107 >= 0 e34: x311 - x33 x69 b108 >= 0 e35: x312 - x34 x69 b109 >= 0 e36: x313 - x35 x69 b110 >= 0 e37: x314 - x36 x69 b111 >= 0 e38: x315 - x37 x70 b112 >= 0 e39: x316 - x38 x70 b113 >= 0 e40: x317 - x39 x70 b114 >= 0 e41: x318 - x40 x70 b115 >= 0 e42: x319 - x41 x71 b116 >= 0 e43: x320 - x42 x71 b117 >= 0 e44: x321 - x43 x71 b118 >= 0 e45: x322 - x44 x71 b119 >= 0 e46: x323 - x45 x72 b120 >= 0 e47: x324 - x46 x72 b121 >= 0 e48: x325 - x47 x72 b122 >= 0 e49: x326 - x48 x72 b123 >= 0 e50: x327 - x49 x73 b124 >= 0 e51: x328 - x50 x73 b125 >= 0 e52: x329 - x51 x73 b126 >= 0 e53: x330 - x52 x73 b127 >= 0 e54: x331 - x53 x74 b128 >= 0 e55: x332 - x54 x74 b129 >= 0 e56: x333 - x55 x74 b130 >= 0 e57: x334 - x56 x74 b131 >= 0 e58: x335 - x57 x75 b132 >= 0 e59: x336 - x58 x75 b133 >= 0 e60: x337 - x59 x75 b134 >= 0 e61: x338 - x60 x75 b135 >= 0 e62: b76 + b77 + b78 + b79 = 1 e63: b80 + b81 + b82 + b83 = 1 e64: b84 + b85 + b86 + b87 = 1 e65: b88 + b89 + b90 + b91 = 1 e66: b92 + b93 + b94 + b95 = 1 e67: b96 + b97 + b98 + b99 = 1 e68: b100 + b101 + b102 + b103 = 1 e69: b104 + b105 + b106 + b107 = 1 e70: b108 + b109 + b110 + b111 = 1 e71: b112 + b113 + b114 + b115 = 1 e72: b116 + b117 + b118 + b119 = 1 e73: b120 + b121 + b122 + b123 = 1 e74: b124 + b125 + b126 + b127 = 1 e75: b128 + b129 + b130 + b131 = 1 e76: b132 + b133 + b134 + b135 = 1 e77: 2.02 b76 + 4.01333333333333 b80 + 4.76 b84 + 5.96 b88 + 42.0933333333333 b92 + 99.28 b96 + 6.59333333333333 b100 + 61.8666666666667 b104 + 56.2866666666667 b108 + 41.5 b112 + 62.4933333333333 b116 + 80.9066666666667 b120 + 26.1466666666667 b124 + 38 b128 + 62.24 b132 <= 153.54 e78: 2.02 b77 + 4.01333333333333 b81 + 4.76 b85 + 5.96 b89 + 42.0933333333333 b93 + 99.28 b97 + 6.59333333333333 b101 + 61.8666666666667 b105 + 56.2866666666667 b109 + 41.5 b113 + 62.4933333333333 b117 + 80.9066666666667 b121 + 26.1466666666667 b125 + 38 b129 + 62.24 b133 <= 153.54 e79: 2.02 b78 + 4.01333333333333 b82 + 4.76 b86 + 5.96 b90 + 42.0933333333333 b94 + 99.28 b98 + 6.59333333333333 b102 + 61.8666666666667 b106 + 56.2866666666667 b110 + 41.5 b114 + 62.4933333333333 b118 + 80.9066666666667 b122 + 26.1466666666667 b126 + 38 b130 + 62.24 b134 <= 153.54 e80: 2.02 b79 + 4.01333333333333 b83 + 4.76 b87 + 5.96 b91 + 42.0933333333333 b95 + 99.28 b99 + 6.59333333333333 b103 + 61.8666666666667 b107 + 56.2866666666667 b111 + 41.5 b115 + 62.4933333333333 b119 + 80.9066666666667 b123 + 26.1466666666667 b127 + 38 b131 + 62.24 b135 <= 153.54 e81: x151 + x159 >= .29424122 e82: x152 + x160 >= .29424122 e83: x153 + x161 >= .29424122 e84: x154 + x162 >= .29424122 e85: x151 + x163 >= .29760193 e86: x152 + x164 >= .29760193 e87: x153 + x165 >= .29760193 e88: x154 + x166 >= .29760193 e89: x151 + x167 >= .35149534 e90: x152 + x168 >= .35149534 e91: x153 + x169 >= .35149534 e92: x154 + x170 >= .35149534 e93: x151 + x171 >= .30458283 e94: x152 + x172 >= .30458283 e95: x153 + x173 >= .30458283 e96: x154 + x174 >= .30458283 e97: x151 + x175 >= .29951066 e98: x152 + x176 >= .29951066 e99: x153 + x177 >= .29951066 e100: x154 + x178 >= .29951066 e101: x151 + x179 >= .30694357 e102: x152 + x180 >= .30694357 e103: x153 + x181 >= .30694357 e104: x154 + x182 >= .30694357 e105: x151 + x183 >= .33520661 e106: x152 + x184 >= .33520661 e107: x153 + x185 >= .33520661 e108: x154 + x186 >= .33520661 e109: x151 + x187 >= .3400071 e110: x152 + x188 >= .3400071 e111: x153 + x189 >= .3400071 e112: x154 + x190 >= .3400071 e113: x151 + x191 >= .35227087 e114: x152 + x192 >= .35227087 e115: x153 + x193 >= .35227087 e116: x154 + x194 >= .35227087 e117: x151 + x195 >= .34225726 e118: x152 + x196 >= .34225726 e119: x153 + x197 >= .34225726 e120: x154 + x198 >= .34225726 e121: x151 + x199 >= .32776566 e122: x152 + x200 >= .32776566 e123: x153 + x201 >= .32776566 e124: x154 + x202 >= .32776566 e125: x151 + x203 >= .30438256 e126: x152 + x204 >= .30438256 e127: x153 + x205 >= .30438256 e128: x154 + x206 >= .30438256 e129: x151 + x207 >= .28538336 e130: x152 + x208 >= .28538336 e131: x153 + x209 >= .28538336 e132: x154 + x210 >= .28538336 e133: x151 + x211 >= .27950575 e134: x152 + x212 >= .27950575 e135: x153 + x213 >= .27950575 e136: x154 + x214 >= .27950575 e137: - x151 + x159 >= -.29424122 e138: - x152 + x160 >= -.29424122 e139: - x153 + x161 >= -.29424122 e140: - x154 + x162 >= -.29424122 e141: - x151 + x163 >= -.29760193 e142: - x152 + x164 >= -.29760193 e143: - x153 + x165 >= -.29760193 e144: - x154 + x166 >= -.29760193 e145: - x151 + x167 >= -.35149534 e146: - x152 + x168 >= -.35149534 e147: - x153 + x169 >= -.35149534 e148: - x154 + x170 >= -.35149534 e149: - x151 + x171 >= -.30458283 e150: - x152 + x172 >= -.30458283 e151: - x153 + x173 >= -.30458283 e152: - x154 + x174 >= -.30458283 e153: - x151 + x175 >= -.29951066 e154: - x152 + x176 >= -.29951066 e155: - x153 + x177 >= -.29951066 e156: - x154 + x178 >= -.29951066 e157: - x151 + x179 >= -.30694357 e158: - x152 + x180 >= -.30694357 e159: - x153 + x181 >= -.30694357 e160: - x154 + x182 >= -.30694357 e161: - x151 + x183 >= -.33520661 e162: - x152 + x184 >= -.33520661 e163: - x153 + x185 >= -.33520661 e164: - x154 + x186 >= -.33520661 e165: - x151 + x187 >= -.3400071 e166: - x152 + x188 >= -.3400071 e167: - x153 + x189 >= -.3400071 e168: - x154 + x190 >= -.3400071 e169: - x151 + x195 >= -.34225726 e170: - x152 + x196 >= -.34225726 e171: - x153 + x197 >= -.34225726 e172: - x154 + x198 >= -.34225726 e173: - x151 + x199 >= -.32776566 e174: - x152 + x200 >= -.32776566 e175: - x153 + x201 >= -.32776566 e176: - x154 + x202 >= -.32776566 e177: - x151 + x203 >= -.30438256 e178: - x152 + x204 >= -.30438256 e179: - x153 + x205 >= -.30438256 e180: - x154 + x206 >= -.30438256 e181: - x151 + x207 >= -.28538336 e182: - x152 + x208 >= -.28538336 e183: - x153 + x209 >= -.28538336 e184: - x154 + x210 >= -.28538336 e185: - x151 + x211 >= -.27950575 e186: - x152 + x212 >= -.27950575 e187: - x153 + x213 >= -.27950575 e188: - x154 + x214 >= -.27950575 e189: - x151 + x215 >= -.25788969 e190: - x152 + x216 >= -.25788969 e191: - x153 + x217 >= -.25788969 e192: - x154 + x218 >= -.25788969 e193: x155 + x223 >= -.9536939 e194: x156 + x224 >= -.9536939 e195: x157 + x225 >= -.9536939 e196: x158 + x226 >= -.9536939 e197: x155 + x227 >= -.9004898 e198: x156 + x228 >= -.9004898 e199: x157 + x229 >= -.9004898 e200: x158 + x230 >= -.9004898 e201: x155 + x231 >= -.9114032 e202: x156 + x232 >= -.9114032 e203: x157 + x233 >= -.9114032 e204: x158 + x234 >= -.9114032 e205: x155 + x235 >= -.90071532 e206: x156 + x236 >= -.90071532 e207: x157 + x237 >= -.90071532 e208: x158 + x238 >= -.90071532 e209: x155 + x239 >= -.88043054 e210: x156 + x240 >= -.88043054 e211: x157 + x241 >= -.88043054 e212: x158 + x242 >= -.88043054 e213: x155 + x243 >= -.8680249 e214: x156 + x244 >= -.8680249 e215: x157 + x245 >= -.8680249 e216: x158 + x246 >= -.8680249 e217: x155 + x247 >= -.81034814 e218: x156 + x248 >= -.81034814 e219: x157 + x249 >= -.81034814 e220: x158 + x250 >= -.81034814 e221: x155 + x251 >= -.80843127 e222: x156 + x252 >= -.80843127 e223: x157 + x253 >= -.80843127 e224: x158 + x254 >= -.80843127 e225: x155 + x255 >= -.7794471 e226: x156 + x256 >= -.7794471 e227: x157 + x257 >= -.7794471 e228: x158 + x258 >= -.7794471 e229: x155 + x259 >= -.79930922 e230: x156 + x260 >= -.79930922 e231: x157 + x261 >= -.79930922 e232: x158 + x262 >= -.79930922 e233: x155 + x263 >= -.84280733 e234: x156 + x264 >= -.84280733 e235: x157 + x265 >= -.84280733 e236: x158 + x266 >= -.84280733 e237: x155 + x267 >= -.81379236 e238: x156 + x268 >= -.81379236 e239: x157 + x269 >= -.81379236 e240: x158 + x270 >= -.81379236 e241: x155 + x271 >= -.82457178 e242: x156 + x272 >= -.82457178 e243: x157 + x273 >= -.82457178 e244: x158 + x274 >= -.82457178 e245: x155 + x275 >= -.80226439 e246: x156 + x276 >= -.80226439 e247: x157 + x277 >= -.80226439 e248: x158 + x278 >= -.80226439 e249: - x155 + x219 >= .98493628 e250: - x156 + x220 >= .98493628 e251: - x157 + x221 >= .98493628 e252: - x158 + x222 >= .98493628 e253: - x155 + x223 >= .9536939 e254: - x156 + x224 >= .9536939 e255: - x157 + x225 >= .9536939 e256: - x158 + x226 >= .9536939 e257: - x155 + x227 >= .9004898 e258: - x156 + x228 >= .9004898 e259: - x157 + x229 >= .9004898 e260: - x158 + x230 >= .9004898 e261: - x155 + x231 >= .9114032 e262: - x156 + x232 >= .9114032 e263: - x157 + x233 >= .9114032 e264: - x158 + x234 >= .9114032 e265: - x155 + x235 >= .90071532 e266: - x156 + x236 >= .90071532 e267: - x157 + x237 >= .90071532 e268: - x158 + x238 >= .90071532 e269: - x155 + x239 >= .88043054 e270: - x156 + x240 >= .88043054 e271: - x157 + x241 >= .88043054 e272: - x158 + x242 >= .88043054 e273: - x155 + x243 >= .8680249 e274: - x156 + x244 >= .8680249 e275: - x157 + x245 >= .8680249 e276: - x158 + x246 >= .8680249 e277: - x155 + x247 >= .81034814 e278: - x156 + x248 >= .81034814 e279: - x157 + x249 >= .81034814 e280: - x158 + x250 >= .81034814 e281: - x155 + x251 >= .80843127 e282: - x156 + x252 >= .80843127 e283: - x157 + x253 >= .80843127 e284: - x158 + x254 >= .80843127 e285: - x155 + x259 >= .79930922 e286: - x156 + x260 >= .79930922 e287: - x157 + x261 >= .79930922 e288: - x158 + x262 >= .79930922 e289: - x155 + x263 >= .84280733 e290: - x156 + x264 >= .84280733 e291: - x157 + x265 >= .84280733 e292: - x158 + x266 >= .84280733 e293: - x155 + x267 >= .81379236 e294: - x156 + x268 >= .81379236 e295: - x157 + x269 >= .81379236 e296: - x158 + x270 >= .81379236 e297: - x155 + x271 >= .82457178 e298: - x156 + x272 >= .82457178 e299: - x157 + x273 >= .82457178 e300: - x158 + x274 >= .82457178 e301: - x155 + x275 >= .80226439 e302: - x156 + x276 >= .80226439 e303: - x157 + x277 >= .80226439 e304: - x158 + x278 >= .80226439 e305: x1 - x159 - x219 = 0 e306: x2 - x160 - x220 = 0 e307: x3 - x161 - x221 = 0 e308: x4 - x162 - x222 = 0 e309: x5 - x163 - x223 = 0 e310: x6 - x164 - x224 = 0 e311: x7 - x165 - x225 = 0 e312: x8 - x166 - x226 = 0 e313: x9 - x167 - x227 = 0 e314: x10 - x168 - x228 = 0 e315: x11 - x169 - x229 = 0 e316: x12 - x170 - x230 = 0 e317: x13 - x171 - x231 = 0 e318: x14 - x172 - x232 = 0 e319: x15 - x173 - x233 = 0 e320: x16 - x174 - x234 = 0 e321: x17 - x175 - x235 = 0 e322: x18 - x176 - x236 = 0 e323: x19 - x177 - x237 = 0 e324: x20 - x178 - x238 = 0 e325: x21 - x179 - x239 = 0 e326: x22 - x180 - x240 = 0 e327: x23 - x181 - x241 = 0 e328: x24 - x182 - x242 = 0 e329: x25 - x183 - x243 = 0 e330: x26 - x184 - x244 = 0 e331: x27 - x185 - x245 = 0 e332: x28 - x186 - x246 = 0 e333: x29 - x187 - x247 = 0 e334: x30 - x188 - x248 = 0 e335: x31 - x189 - x249 = 0 e336: x32 - x190 - x250 = 0 e337: x33 - x191 - x251 = 0 e338: x34 - x192 - x252 = 0 e339: x35 - x193 - x253 = 0 e340: x36 - x194 - x254 = 0 e341: x37 - x195 - x255 = 0 e342: x38 - x196 - x256 = 0 e343: x39 - x197 - x257 = 0 e344: x40 - x198 - x258 = 0 e345: x41 - x199 - x259 = 0 e346: x42 - x200 - x260 = 0 e347: x43 - x201 - x261 = 0 e348: x44 - x202 - x262 = 0 e349: x45 - x203 - x263 = 0 e350: x46 - x204 - x264 = 0 e351: x47 - x205 - x265 = 0 e352: x48 - x206 - x266 = 0 e353: x49 - x207 - x267 = 0 e354: x50 - x208 - x268 = 0 e355: x51 - x209 - x269 = 0 e356: x52 - x210 - x270 = 0 e357: x53 - x211 - x271 = 0 e358: x54 - x212 - x272 = 0 e359: x55 - x213 - x273 = 0 e360: x56 - x214 - x274 = 0 e361: x57 - x215 - x275 = 0 e362: x58 - x216 - x276 = 0 e363: x59 - x217 - x277 = 0 e364: x60 - x218 - x278 = 0 e365: b357 + b358 >= 1 e366: b354 + b359 >= 1 e367: b353 + b360 >= 1 e368: b352 + b363 >= 1 e369: b351 + b358 >= 1 e370: b351 + b356 + b359 >= 1 e371: b351 + b354 + b361 >= 1 e372: b351 + b353 + b362 >= 1 e373: b351 + b352 >= 1 e374: b350 + b358 >= 1 e375: b350 + b357 + b359 >= 1 e376: b350 + b356 + b360 >= 1 e377: b350 + b355 + b361 >= 1 e378: b350 + b354 + b362 >= 1 e379: b350 + b353 + b363 >= 1 e380: b350 + b352 >= 1 e381: b349 + b360 >= 1 e382: b349 + b357 + b361 >= 1 e383: b349 + b356 + b362 >= 1 e384: b349 + b355 + b363 >= 1 e385: b349 + b354 >= 1 e386: b348 + b363 >= 1 e387: b348 + b357 >= 1 e388: b347 + b358 >= 1 e389: b347 + b357 + b359 >= 1 e390: b347 + b355 + b360 >= 1 e391: b347 + b354 + b361 >= 1 e392: b347 + b353 + b363 >= 1 e393: b347 + b352 >= 1 e394: b347 + b351 + b359 >= 1 e395: b347 + b351 + b357 + b360 >= 1 e396: b347 + b351 + b356 + b361 >= 1 e397: b347 + b351 + b355 + b362 >= 1 e398: b347 + b351 + b354 + b363 >= 1 e399: b347 + b351 + b353 >= 1 e400: b347 + b350 + b361 >= 1 e401: b347 + b350 + b357 + b362 >= 1 e402: b347 + b350 + b356 + b363 >= 1 e403: b347 + b350 + b355 >= 1 e404: b347 + b349 + b363 >= 1 e405: b347 + b349 + b357 >= 1 e406: b347 + b348 >= 1 e407: b346 + b360 >= 1 e408: b346 + b357 + b361 >= 1 e409: b346 + b356 + b362 >= 1 e410: b346 + b355 + b363 >= 1 e411: b346 + b354 >= 1 e412: b346 + b351 + b362 >= 1 e413: b346 + b351 + b357 + b363 >= 1 e414: b346 + b351 + b356 >= 1 e415: b346 + b350 + b363 >= 1 e416: b346 + b350 + b357 >= 1 e417: b346 + b349 >= 1 e418: b345 + b363 >= 1 e419: b345 + b357 >= 1 e420: b345 + b351 >= 1 e421: b344 + b358 >= 1 e422: b344 + b357 + b359 >= 1 e423: b344 + b356 + b360 >= 1 e424: b344 + b355 + b361 >= 1 e425: b344 + b354 + b362 >= 1 e426: b344 + b353 + b363 >= 1 e427: b344 + b352 >= 1 e428: b344 + b351 + b359 >= 1 e429: b344 + b351 + b357 + b360 >= 1 e430: b344 + b351 + b356 + b361 >= 1 e431: b344 + b351 + b355 + b362 >= 1 e432: b344 + b351 + b354 + b363 >= 1 e433: b344 + b351 + b353 >= 1 e434: b344 + b350 + b361 >= 1 e435: b344 + b350 + b357 + b362 >= 1 e436: b344 + b350 + b356 + b363 >= 1 e437: b344 + b350 + b355 >= 1 e438: b344 + b349 + b363 >= 1 e439: b344 + b349 + b357 >= 1 e440: b344 + b348 >= 1 e441: b344 + b347 + b360 >= 1 e442: b344 + b347 + b357 + b361 >= 1 e443: b344 + b347 + b356 + b362 >= 1 e444: b344 + b347 + b355 + b363 >= 1 e445: b344 + b347 + b354 >= 1 e446: b344 + b347 + b351 + b361 >= 1 e447: b344 + b347 + b351 + b357 + b363 >= 1 e448: b344 + b347 + b351 + b355 >= 1 e449: b344 + b347 + b350 + b363 >= 1 e450: b344 + b347 + b350 + b357 >= 1 e451: b344 + b347 + b349 >= 1 e452: b344 + b346 + b363 >= 1 e453: b344 + b346 + b357 >= 1 e454: b344 + b346 + b351 >= 1 e455: b344 + b345 >= 1 e456: b343 + b360 >= 1 e457: b343 + b357 + b361 >= 1 e458: b343 + b356 + b362 >= 1 e459: b343 + b355 + b363 >= 1 e460: b343 + b354 >= 1 e461: b343 + b351 + b362 >= 1 e462: b343 + b351 + b357 + b363 >= 1 e463: b343 + b351 + b355 >= 1 e464: b343 + b350 + b363 >= 1 e465: b343 + b350 + b357 >= 1 e466: b343 + b349 >= 1 e467: b343 + b347 + b363 >= 1 e468: b343 + b347 + b356 >= 1 e469: b343 + b347 + b351 >= 1 e470: b343 + b346 >= 1 e471: b342 + b363 >= 1 e472: b342 + b357 >= 1 e473: b342 + b351 >= 1 e474: b342 + b347 >= 1 e475: b341 + b358 >= 1 e476: b341 + b356 + b359 >= 1 e477: b341 + b355 + b360 >= 1 e478: b341 + b354 + b361 >= 1 e479: b341 + b353 + b363 >= 1 e480: b341 + b352 >= 1 e481: b341 + b351 + b359 >= 1 e482: b341 + b351 + b357 + b360 >= 1 e483: b341 + b351 + b356 + b361 >= 1 e484: b341 + b351 + b355 + b362 >= 1 e485: b341 + b351 + b354 + b363 >= 1 e486: b341 + b351 + b353 >= 1 e487: b341 + b350 + b361 >= 1 e488: b341 + b350 + b357 + b362 >= 1 e489: b341 + b350 + b356 + b363 >= 1 e490: b341 + b350 + b355 >= 1 e491: b341 + b349 + b363 >= 1 e492: b341 + b349 + b356 >= 1 e493: b341 + b348 >= 1 e494: b341 + b347 + b360 >= 1 e495: b341 + b347 + b357 + b361 >= 1 e496: b341 + b347 + b356 + b362 >= 1 e497: b341 + b347 + b355 + b363 >= 1 e498: b341 + b347 + b354 >= 1 e499: b341 + b347 + b351 + b361 >= 1 e500: b341 + b347 + b351 + b357 + b362 >= 1 e501: b341 + b347 + b351 + b356 + b363 >= 1 e502: b341 + b347 + b351 + b355 >= 1 e503: b341 + b347 + b350 + b363 >= 1 e504: b341 + b347 + b350 + b357 >= 1 e505: b341 + b347 + b349 >= 1 e506: b341 + b346 + b363 >= 1 e507: b341 + b346 + b357 >= 1 e508: b341 + b346 + b351 >= 1 e509: b341 + b345 >= 1 e510: b341 + b344 + b360 >= 1 e511: b341 + b344 + b357 + b361 >= 1 e512: b341 + b344 + b356 + b362 >= 1 e513: b341 + b344 + b355 + b363 >= 1 e514: b341 + b344 + b354 >= 1 e515: b341 + b344 + b351 + b361 >= 1 e516: b341 + b344 + b351 + b357 + b363 >= 1 e517: b341 + b344 + b351 + b356 >= 1 e518: b341 + b344 + b350 + b363 >= 1 e519: b341 + b344 + b350 + b357 >= 1 e520: b341 + b344 + b349 >= 1 e521: b341 + b344 + b347 + b362 >= 1 e522: b341 + b344 + b347 + b357 + b363 >= 1 e523: b341 + b344 + b347 + b356 >= 1 e524: b341 + b344 + b347 + b351 >= 1 e525: b341 + b344 + b346 >= 1 e526: b341 + b343 + b363 >= 1 e527: b341 + b343 + b357 >= 1 e528: b341 + b343 + b351 >= 1 e529: b341 + b343 + b347 >= 1 e530: b341 + b342 >= 1 e531: b340 + b360 >= 1 e532: b340 + b357 + b361 >= 1 e533: b340 + b356 + b362 >= 1 e534: b340 + b355 + b363 >= 1 e535: b340 + b354 >= 1 e536: b340 + b351 + b362 >= 1 e537: b340 + b351 + b357 + b363 >= 1 e538: b340 + b351 + b356 >= 1 e539: b340 + b350 + b363 >= 1 e540: b340 + b350 + b357 >= 1 e541: b340 + b349 >= 1 e542: b340 + b347 + b363 >= 1 e543: b340 + b347 + b357 >= 1 e544: b340 + b347 + b351 >= 1 e545: b340 + b346 >= 1 e546: b340 + b344 + b363 >= 1 e547: b340 + b344 + b357 >= 1 e548: b340 + b344 + b351 >= 1 e549: b340 + b344 + b347 >= 1 e550: b340 + b343 >= 1 e551: b339 + b363 >= 1 e552: b339 + b357 >= 1 e553: b339 + b351 >= 1 e554: b339 + b347 >= 1 e555: b339 + b344 >= 1 e556: b363 + b372 >= 1 e557: b363 + b370 + b373 >= 1 e558: b363 + b369 + b374 >= 1 e559: b363 + b368 + b375 >= 1 e560: b363 + b367 >= 1 e561: b363 + b366 + b373 >= 1 e562: b363 + b366 + b371 + b374 >= 1 e563: b363 + b366 + b369 + b376 >= 1 e564: b363 + b366 + b368 >= 1 e565: b363 + b365 + b375 >= 1 e566: b363 + b365 + b371 + b376 >= 1 e567: b363 + b365 + b370 >= 1 e568: b363 + b364 >= 1 e569: b362 + b372 >= 1 e570: b362 + b370 + b373 >= 1 e571: b362 + b369 + b374 >= 1 e572: b362 + b368 + b375 >= 1 e573: b362 + b367 >= 1 e574: b362 + b366 + b373 >= 1 e575: b362 + b366 + b371 + b374 >= 1 e576: b362 + b366 + b370 + b375 >= 1 e577: b362 + b366 + b369 + b376 >= 1 e578: b362 + b366 + b368 >= 1 e579: b362 + b365 + b375 >= 1 e580: b362 + b365 + b371 + b376 >= 1 e581: b362 + b365 + b370 >= 1 e582: b362 + b364 >= 1 e583: b361 + b372 >= 1 e584: b361 + b371 + b373 >= 1 e585: b361 + b370 + b374 >= 1 e586: b361 + b369 + b375 >= 1 e587: b361 + b368 + b376 >= 1 e588: b361 + b367 >= 1 e589: b361 + b366 + b374 >= 1 e590: b361 + b366 + b371 + b375 >= 1 e591: b361 + b366 + b370 + b376 >= 1 e592: b361 + b366 + b369 >= 1 e593: b361 + b365 + b376 >= 1 e594: b361 + b365 + b371 >= 1 e595: b361 + b364 >= 1 e596: b360 + b373 >= 1 e597: b360 + b371 + b374 >= 1 e598: b360 + b370 + b375 >= 1 e599: b360 + b369 + b376 >= 1 e600: b360 + b368 >= 1 e601: b360 + b366 + b375 >= 1 e602: b360 + b366 + b371 + b376 >= 1 e603: b360 + b366 + b370 >= 1 e604: b360 + b365 >= 1 e605: b359 + b374 >= 1 e606: b359 + b371 + b375 >= 1 e607: b359 + b370 + b376 >= 1 e608: b359 + b369 >= 1 e609: b359 + b366 + b376 >= 1 e610: b359 + b366 + b371 >= 1 e611: b359 + b365 >= 1 e612: b358 + b376 >= 1 e613: b358 + b371 >= 1 e614: b358 + b366 >= 1 e615: b357 + b372 >= 1 e616: b357 + b370 + b373 >= 1 e617: b357 + b369 + b374 >= 1 e618: b357 + b367 >= 1 e619: b357 + b366 + b373 >= 1 e620: b357 + b366 + b371 + b374 >= 1 e621: b357 + b366 + b369 + b376 >= 1 e622: b357 + b366 + b368 >= 1 e623: b357 + b365 + b375 >= 1 e624: b357 + b365 + b371 + b376 >= 1 e625: b357 + b365 + b370 >= 1 e626: b357 + b364 >= 1 e627: b357 + b363 + b372 >= 1 e628: b357 + b363 + b370 + b373 >= 1 e629: b357 + b363 + b369 + b374 >= 1 e630: b357 + b363 + b368 + b376 >= 1 e631: b357 + b363 + b367 >= 1 e632: b357 + b363 + b366 + b373 >= 1 e633: b357 + b363 + b366 + b371 + b374 >= 1 e634: b357 + b363 + b366 + b370 + b375 >= 1 e635: b357 + b363 + b366 + b369 + b376 >= 1 e636: b357 + b363 + b366 + b368 >= 1 e637: b357 + b363 + b365 + b375 >= 1 e638: b357 + b363 + b365 + b371 + b376 >= 1 e639: b357 + b363 + b365 + b370 >= 1 e640: b357 + b363 + b364 >= 1 e641: b357 + b362 + b372 >= 1 e642: b357 + b362 + b371 + b373 >= 1 e643: b357 + b362 + b370 + b374 >= 1 e644: b357 + b362 + b369 + b375 >= 1 e645: b357 + b362 + b368 + b376 >= 1 e646: b357 + b362 + b367 >= 1 e647: b357 + b362 + b366 + b374 >= 1 e648: b357 + b362 + b366 + b371 + b375 >= 1 e649: b357 + b362 + b366 + b370 + b376 >= 1 e650: b357 + b362 + b366 + b369 >= 1 e651: b357 + b362 + b365 + b376 >= 1 e652: b357 + b362 + b365 + b371 >= 1 e653: b357 + b362 + b364 >= 1 e654: b357 + b361 + b373 >= 1 e655: b357 + b361 + b371 + b374 >= 1 e656: b357 + b361 + b370 + b375 >= 1 e657: b357 + b361 + b369 + b376 >= 1 e658: b357 + b361 + b368 >= 1 e659: b357 + b361 + b366 + b375 >= 1 e660: b357 + b361 + b366 + b371 + b376 >= 1 e661: b357 + b361 + b366 + b370 >= 1 e662: b357 + b361 + b365 >= 1 e663: b357 + b360 + b374 >= 1 e664: b357 + b360 + b371 + b375 >= 1 e665: b357 + b360 + b370 + b376 >= 1 e666: b357 + b360 + b369 >= 1 e667: b357 + b360 + b366 + b376 >= 1 e668: b357 + b360 + b366 + b371 >= 1 e669: b357 + b360 + b365 >= 1 e670: b357 + b359 + b375 >= 1 e671: b357 + b359 + b371 + b376 >= 1 e672: b357 + b359 + b370 >= 1 e673: b357 + b359 + b366 >= 1 e674: b356 + b372 >= 1 e675: b356 + b370 + b373 >= 1 e676: b356 + b369 + b374 >= 1 e677: b356 + b368 + b375 >= 1 e678: b356 + b367 >= 1 e679: b356 + b366 + b373 >= 1 e680: b356 + b366 + b371 + b374 >= 1 e681: b356 + b366 + b370 + b375 >= 1 e682: b356 + b366 + b369 + b376 >= 1 e683: b356 + b366 + b368 >= 1 e684: b356 + b365 + b375 >= 1 e685: b356 + b365 + b371 + b376 >= 1 e686: b356 + b365 + b370 >= 1 e687: b356 + b364 >= 1 e688: b356 + b363 + b372 >= 1 e689: b356 + b363 + b371 + b373 >= 1 e690: b356 + b363 + b370 + b374 >= 1 e691: b356 + b363 + b369 + b375 >= 1 e692: b356 + b363 + b368 + b376 >= 1 e693: b356 + b363 + b367 >= 1 e694: b356 + b363 + b366 + b374 >= 1 e695: b356 + b363 + b366 + b371 + b375 >= 1 e696: b356 + b363 + b366 + b370 + b376 >= 1 e697: b356 + b363 + b366 + b369 >= 1 e698: b356 + b363 + b365 + b376 >= 1 e699: b356 + b363 + b365 + b371 >= 1 e700: b356 + b363 + b364 >= 1 e701: b356 + b362 + b373 >= 1 e702: b356 + b362 + b371 + b374 >= 1 e703: b356 + b362 + b370 + b375 >= 1 e704: b356 + b362 + b369 + b376 >= 1 e705: b356 + b362 + b368 >= 1 e706: b356 + b362 + b366 + b375 >= 1 e707: b356 + b362 + b366 + b371 + b376 >= 1 e708: b356 + b362 + b366 + b370 >= 1 e709: b356 + b362 + b365 >= 1 e710: b356 + b361 + b374 >= 1 e711: b356 + b361 + b371 + b375 >= 1 e712: b356 + b361 + b370 + b376 >= 1 e713: b356 + b361 + b369 >= 1 e714: b356 + b361 + b366 + b376 >= 1 e715: b356 + b361 + b366 + b371 >= 1 e716: b356 + b361 + b365 >= 1 e717: b356 + b360 + b374 >= 1 e718: b356 + b360 + b371 + b376 >= 1 e719: b356 + b360 + b370 >= 1 e720: b356 + b360 + b366 >= 1 e721: b356 + b359 + b375 >= 1 e722: b356 + b359 + b371 + b376 >= 1 e723: b356 + b359 + b370 >= 1 e724: b356 + b359 + b366 >= 1 e725: b355 + b372 >= 1 e726: b355 + b371 + b373 >= 1 e727: b355 + b370 + b374 >= 1 e728: b355 + b369 + b375 >= 1 e729: b355 + b368 + b376 >= 1 e730: b355 + b367 >= 1 e731: b355 + b366 + b374 >= 1 e732: b355 + b366 + b371 + b375 >= 1 e733: b355 + b366 + b370 + b376 >= 1 e734: b355 + b366 + b369 >= 1 e735: b355 + b365 + b376 >= 1 e736: b355 + b365 + b371 >= 1 e737: b355 + b364 >= 1 e738: b355 + b363 + b373 >= 1 e739: b355 + b363 + b371 + b374 >= 1 e740: b355 + b363 + b370 + b375 >= 1 e741: b355 + b363 + b369 + b376 >= 1 e742: b355 + b363 + b368 >= 1 e743: b355 + b363 + b366 + b375 >= 1 e744: b355 + b363 + b366 + b371 + b376 >= 1 e745: b355 + b363 + b366 + b370 >= 1 e746: b355 + b363 + b365 >= 1 e747: b355 + b362 + b374 >= 1 e748: b355 + b362 + b371 + b375 >= 1 e749: b355 + b362 + b370 + b376 >= 1 e750: b355 + b362 + b369 >= 1 e751: b355 + b362 + b366 + b376 >= 1 e752: b355 + b362 + b366 + b371 >= 1 e753: b355 + b362 + b365 >= 1 e754: b355 + b361 + b374 >= 1 e755: b355 + b361 + b371 + b375 >= 1 e756: b355 + b361 + b370 + b376 >= 1 e757: b355 + b361 + b369 >= 1 e758: b355 + b361 + b366 + b376 >= 1 e759: b355 + b361 + b366 + b371 >= 1 e760: b355 + b361 + b365 >= 1 e761: b355 + b360 + b375 >= 1 e762: b355 + b360 + b371 + b376 >= 1 e763: b355 + b360 + b370 >= 1 e764: b355 + b360 + b366 >= 1 e765: b355 + b359 + b376 >= 1 e766: b355 + b359 + b371 >= 1 e767: b355 + b359 + b366 >= 1 e768: b354 + b373 >= 1 e769: b354 + b371 + b374 >= 1 e770: b354 + b370 + b375 >= 1 e771: b354 + b369 + b376 >= 1 e772: b354 + b368 >= 1 e773: b354 + b366 + b375 >= 1 e774: b354 + b366 + b371 + b376 >= 1 e775: b354 + b366 + b370 >= 1 e776: b354 + b365 >= 1 e777: b354 + b363 + b374 >= 1 e778: b354 + b363 + b371 + b375 >= 1 e779: b354 + b363 + b370 + b376 >= 1 e780: b354 + b363 + b369 >= 1 e781: b354 + b363 + b366 + b376 >= 1 e782: b354 + b363 + b366 + b371 >= 1 e783: b354 + b363 + b365 >= 1 e784: b354 + b362 + b374 >= 1 e785: b354 + b362 + b371 + b375 >= 1 e786: b354 + b362 + b370 >= 1 e787: b354 + b362 + b366 + b376 >= 1 e788: b354 + b362 + b366 + b371 >= 1 e789: b354 + b362 + b365 >= 1 e790: b354 + b361 + b375 >= 1 e791: b354 + b361 + b371 + b376 >= 1 e792: b354 + b361 + b370 >= 1 e793: b354 + b361 + b366 >= 1 e794: b354 + b360 + b376 >= 1 e795: b354 + b360 + b371 >= 1 e796: b354 + b360 + b366 >= 1 e797: b353 + b374 >= 1 e798: b353 + b371 + b375 >= 1 e799: b353 + b370 + b376 >= 1 e800: b353 + b369 >= 1 e801: b353 + b366 + b376 >= 1 e802: b353 + b366 + b371 >= 1 e803: b353 + b365 >= 1 e804: b353 + b363 + b374 >= 1 e805: b353 + b363 + b371 + b376 >= 1 e806: b353 + b363 + b370 >= 1 e807: b353 + b363 + b366 >= 1 e808: b353 + b362 + b375 >= 1 e809: b353 + b362 + b371 + b376 >= 1 e810: b353 + b362 + b370 >= 1 e811: b353 + b362 + b366 >= 1 e812: b353 + b361 + b376 >= 1 e813: b353 + b361 + b371 >= 1 e814: b353 + b361 + b366 >= 1 e815: b352 + b376 >= 1 e816: b352 + b371 >= 1 e817: b352 + b366 >= 1 e818: b351 + b372 >= 1 e819: b351 + b370 + b373 >= 1 e820: b351 + b369 + b374 >= 1 e821: b351 + b368 + b375 >= 1 e822: b351 + b367 >= 1 e823: b351 + b366 + b373 >= 1 e824: b351 + b366 + b371 + b374 >= 1 e825: b351 + b366 + b370 + b375 >= 1 e826: b351 + b366 + b369 + b376 >= 1 e827: b351 + b366 + b368 >= 1 e828: b351 + b365 + b375 >= 1 e829: b351 + b365 + b371 + b376 >= 1 e830: b351 + b365 + b370 >= 1 e831: b351 + b364 >= 1 e832: b351 + b363 + b372 >= 1 e833: b351 + b363 + b371 + b373 >= 1 e834: b351 + b363 + b370 + b374 >= 1 e835: b351 + b363 + b369 + b375 >= 1 e836: b351 + b363 + b368 + b376 >= 1 e837: b351 + b363 + b367 >= 1 e838: b351 + b363 + b366 + b374 >= 1 e839: b351 + b363 + b366 + b371 + b375 >= 1 e840: b351 + b363 + b366 + b370 + b376 >= 1 e841: b351 + b363 + b366 + b369 >= 1 e842: b351 + b363 + b365 + b376 >= 1 e843: b351 + b363 + b365 + b371 >= 1 e844: b351 + b363 + b364 >= 1 e845: b351 + b362 + b373 >= 1 e846: b351 + b362 + b370 + b374 >= 1 e847: b351 + b362 + b369 + b376 >= 1 e848: b351 + b362 + b368 >= 1 e849: b351 + b362 + b366 + b374 >= 1 e850: b351 + b362 + b366 + b371 + b375 >= 1 e851: b351 + b362 + b366 + b370 + b376 >= 1 e852: b351 + b362 + b366 + b369 >= 1 e853: b351 + b362 + b365 + b376 >= 1 e854: b351 + b362 + b365 + b371 >= 1 e855: b351 + b362 + b364 >= 1 e856: b351 + b361 + b373 >= 1 e857: b351 + b361 + b371 + b374 >= 1 e858: b351 + b361 + b370 + b375 >= 1 e859: b351 + b361 + b369 + b376 >= 1 e860: b351 + b361 + b368 >= 1 e861: b351 + b361 + b366 + b375 >= 1 e862: b351 + b361 + b366 + b371 + b376 >= 1 e863: b351 + b361 + b366 + b370 >= 1 e864: b351 + b361 + b365 >= 1 e865: b351 + b360 + b374 >= 1 e866: b351 + b360 + b371 + b375 >= 1 e867: b351 + b360 + b370 + b376 >= 1 e868: b351 + b360 + b369 >= 1 e869: b351 + b360 + b366 + b376 >= 1 e870: b351 + b360 + b366 + b371 >= 1 e871: b351 + b360 + b365 >= 1 e872: b351 + b359 + b375 >= 1 e873: b351 + b359 + b371 + b376 >= 1 e874: b351 + b359 + b370 >= 1 e875: b351 + b359 + b366 >= 1 e876: b351 + b357 + b372 >= 1 e877: b351 + b357 + b371 + b373 >= 1 e878: b351 + b357 + b370 + b374 >= 1 e879: b351 + b357 + b369 + b375 >= 1 e880: b351 + b357 + b368 + b376 >= 1 e881: b351 + b357 + b367 >= 1 e882: b351 + b357 + b366 + b374 >= 1 e883: b351 + b357 + b366 + b371 + b375 >= 1 e884: b351 + b357 + b366 + b370 + b376 >= 1 e885: b351 + b357 + b366 + b369 >= 1 e886: b351 + b357 + b365 + b376 >= 1 e887: b351 + b357 + b365 + b371 >= 1 e888: b351 + b357 + b364 >= 1 e889: b351 + b357 + b363 + b373 >= 1 e890: b351 + b357 + b363 + b371 + b374 >= 1 e891: b351 + b357 + b363 + b370 + b375 >= 1 e892: b351 + b357 + b363 + b369 + b376 >= 1 e893: b351 + b357 + b363 + b368 >= 1 e894: b351 + b357 + b363 + b366 + b375 >= 1 e895: b351 + b357 + b363 + b366 + b371 + b376 >= 1 e896: b351 + b357 + b363 + b366 + b370 >= 1 e897: b351 + b357 + b363 + b365 >= 1 e898: b351 + b357 + b362 + b373 >= 1 e899: b351 + b357 + b362 + b371 + b374 >= 1 e900: b351 + b357 + b362 + b370 + b375 >= 1 e901: b351 + b357 + b362 + b369 + b376 >= 1 e902: b351 + b357 + b362 + b368 >= 1 e903: b351 + b357 + b362 + b366 + b375 >= 1 e904: b351 + b357 + b362 + b366 + b371 + b376 >= 1 e905: b351 + b357 + b362 + b366 + b370 >= 1 e906: b351 + b357 + b362 + b365 >= 1 e907: b351 + b357 + b361 + b374 >= 1 e908: b351 + b357 + b361 + b371 + b375 >= 1 e909: b351 + b357 + b361 + b370 + b376 >= 1 e910: b351 + b357 + b361 + b369 >= 1 e911: b351 + b357 + b361 + b366 + b376 >= 1 e912: b351 + b357 + b361 + b366 + b371 >= 1 e913: b351 + b357 + b361 + b365 >= 1 e914: b351 + b357 + b360 + b375 >= 1 e915: b351 + b357 + b360 + b371 + b376 >= 1 e916: b351 + b357 + b360 + b370 >= 1 e917: b351 + b357 + b360 + b366 >= 1 e918: b351 + b357 + b359 + b376 >= 1 e919: b351 + b357 + b359 + b371 >= 1 e920: b351 + b357 + b359 + b366 >= 1 e921: b351 + b356 + b372 >= 1 e922: b351 + b356 + b371 + b373 >= 1 e923: b351 + b356 + b370 + b374 >= 1 e924: b351 + b356 + b369 + b376 >= 1 e925: b351 + b356 + b368 >= 1 e926: b351 + b356 + b366 + b374 >= 1 e927: b351 + b356 + b366 + b371 + b375 >= 1 e928: b351 + b356 + b366 + b370 + b376 >= 1 e929: b351 + b356 + b366 + b369 >= 1 e930: b351 + b356 + b365 >= 1 e931: b351 + b356 + b363 + b373 >= 1 e932: b351 + b356 + b363 + b371 + b374 >= 1 e933: b351 + b356 + b363 + b370 + b375 >= 1 e934: b351 + b356 + b363 + b369 + b376 >= 1 e935: b351 + b356 + b363 + b368 >= 1 e936: b351 + b356 + b363 + b366 + b375 >= 1 e937: b351 + b356 + b363 + b366 + b371 + b376 >= 1 e938: b351 + b356 + b363 + b366 + b370 >= 1 e939: b351 + b356 + b363 + b365 >= 1 e940: b351 + b356 + b362 + b374 >= 1 e941: b351 + b356 + b362 + b371 + b375 >= 1 e942: b351 + b356 + b362 + b370 + b376 >= 1 e943: b351 + b356 + b362 + b369 >= 1 e944: b351 + b356 + b362 + b366 + b376 >= 1 e945: b351 + b356 + b362 + b366 + b371 >= 1 e946: b351 + b356 + b362 + b365 >= 1 e947: b351 + b356 + b361 + b375 >= 1 e948: b351 + b356 + b361 + b371 + b376 >= 1 e949: b351 + b356 + b361 + b370 >= 1 e950: b351 + b356 + b361 + b366 >= 1 e951: b351 + b356 + b360 + b376 >= 1 e952: b351 + b356 + b360 + b371 >= 1 e953: b351 + b356 + b360 + b366 >= 1 e954: b351 + b355 + b373 >= 1 e955: b351 + b355 + b371 + b374 >= 1 e956: b351 + b355 + b370 + b375 >= 1 e957: b351 + b355 + b369 + b376 >= 1 e958: b351 + b355 + b368 >= 1 e959: b351 + b355 + b366 + b375 >= 1 e960: b351 + b355 + b366 + b371 + b376 >= 1 e961: b351 + b355 + b366 + b370 >= 1 e962: b351 + b355 + b365 >= 1 e963: b351 + b355 + b363 + b374 >= 1 e964: b351 + b355 + b363 + b371 + b375 >= 1 e965: b351 + b355 + b363 + b370 + b376 >= 1 e966: b351 + b355 + b363 + b369 >= 1 e967: b351 + b355 + b363 + b366 + b376 >= 1 e968: b351 + b355 + b363 + b366 + b371 >= 1 e969: b351 + b355 + b363 + b365 >= 1 e970: b351 + b355 + b362 + b375 >= 1 e971: b351 + b355 + b362 + b371 + b376 >= 1 e972: b351 + b355 + b362 + b370 >= 1 e973: b351 + b355 + b362 + b366 >= 1 e974: b351 + b355 + b361 + b376 >= 1 e975: b351 + b355 + b361 + b371 >= 1 e976: b351 + b355 + b361 + b366 >= 1 e977: b351 + b355 + b360 + b376 >= 1 e978: b351 + b355 + b360 + b371 >= 1 e979: b351 + b355 + b360 + b366 >= 1 e980: b351 + b354 + b374 >= 1 e981: b351 + b354 + b371 + b375 >= 1 e982: b351 + b354 + b370 + b376 >= 1 e983: b351 + b354 + b369 >= 1 e984: b351 + b354 + b366 + b376 >= 1 e985: b351 + b354 + b366 + b371 >= 1 e986: b351 + b354 + b365 >= 1 e987: b351 + b354 + b363 + b375 >= 1 e988: b351 + b354 + b363 + b371 + b376 >= 1 e989: b351 + b354 + b363 + b370 >= 1 e990: b351 + b354 + b363 + b366 >= 1 e991: b351 + b354 + b362 + b376 >= 1 e992: b351 + b354 + b362 + b371 >= 1 e993: b351 + b354 + b362 + b366 >= 1 e994: b351 + b353 + b375 >= 1 e995: b351 + b353 + b371 + b376 >= 1 e996: b351 + b353 + b370 >= 1 e997: b351 + b353 + b366 >= 1 e998: b351 + b353 + b363 + b376 >= 1 e999: b351 + b353 + b363 + b371 >= 1 e1000: b351 + b353 + b363 + b366 >= 1 e1001: b350 + b372 >= 1 e1002: b350 + b371 + b373 >= 1 e1003: b350 + b370 + b374 >= 1 e1004: b350 + b369 + b375 >= 1 e1005: b350 + b368 + b376 >= 1 e1006: b350 + b367 >= 1 e1007: b350 + b366 + b374 >= 1 e1008: b350 + b366 + b371 + b375 >= 1 e1009: b350 + b366 + b370 + b376 >= 1 e1010: b350 + b366 + b369 >= 1 e1011: b350 + b365 + b376 >= 1 e1012: b350 + b365 + b371 >= 1 e1013: b350 + b364 >= 1 e1014: b350 + b363 + b373 >= 1 e1015: b350 + b363 + b371 + b374 >= 1 e1016: b350 + b363 + b370 + b375 >= 1 e1017: b350 + b363 + b369 + b376 >= 1 e1018: b350 + b363 + b368 >= 1 e1019: b350 + b363 + b366 + b375 >= 1 e1020: b350 + b363 + b366 + b371 + b376 >= 1 e1021: b350 + b363 + b366 + b370 >= 1 e1022: b350 + b363 + b365 >= 1 e1023: b350 + b362 + b374 >= 1 e1024: b350 + b362 + b371 + b375 >= 1 e1025: b350 + b362 + b370 + b376 >= 1 e1026: b350 + b362 + b369 >= 1 e1027: b350 + b362 + b366 + b376 >= 1 e1028: b350 + b362 + b366 + b371 >= 1 e1029: b350 + b362 + b365 >= 1 e1030: b350 + b361 + b375 >= 1 e1031: b350 + b361 + b371 + b376 >= 1 e1032: b350 + b361 + b370 >= 1 e1033: b350 + b361 + b366 >= 1 e1034: b350 + b360 + b376 >= 1 e1035: b350 + b360 + b371 >= 1 e1036: b350 + b360 + b366 >= 1 e1037: b350 + b359 + b376 >= 1 e1038: b350 + b359 + b371 >= 1 e1039: b350 + b359 + b366 >= 1 e1040: b350 + b357 + b373 >= 1 e1041: b350 + b357 + b371 + b374 >= 1 e1042: b350 + b357 + b370 + b375 >= 1 e1043: b350 + b357 + b369 + b376 >= 1 e1044: b350 + b357 + b368 >= 1 e1045: b350 + b357 + b366 + b375 >= 1 e1046: b350 + b357 + b366 + b371 + b376 >= 1 e1047: b350 + b357 + b366 + b370 >= 1 e1048: b350 + b357 + b365 >= 1 e1049: b350 + b357 + b363 + b374 >= 1 e1050: b350 + b357 + b363 + b371 + b375 >= 1 e1051: b350 + b357 + b363 + b370 + b376 >= 1 e1052: b350 + b357 + b363 + b369 >= 1 e1053: b350 + b357 + b363 + b366 + b376 >= 1 e1054: b350 + b357 + b363 + b366 + b371 >= 1 e1055: b350 + b357 + b363 + b365 >= 1 e1056: b350 + b357 + b362 + b375 >= 1 e1057: b350 + b357 + b362 + b371 + b376 >= 1 e1058: b350 + b357 + b362 + b370 >= 1 e1059: b350 + b357 + b362 + b366 >= 1 e1060: b350 + b357 + b361 + b376 >= 1 e1061: b350 + b357 + b361 + b371 >= 1 e1062: b350 + b357 + b361 + b366 >= 1 e1063: b350 + b357 + b360 + b376 >= 1 e1064: b350 + b357 + b360 + b371 >= 1 e1065: b350 + b357 + b360 + b366 >= 1 e1066: b350 + b356 + b374 >= 1 e1067: b350 + b356 + b371 + b375 >= 1 e1068: b350 + b356 + b370 + b376 >= 1 e1069: b350 + b356 + b369 >= 1 e1070: b350 + b356 + b366 + b376 >= 1 e1071: b350 + b356 + b366 + b371 >= 1 e1072: b350 + b356 + b365 >= 1 e1073: b350 + b356 + b363 + b375 >= 1 e1074: b350 + b356 + b363 + b371 + b376 >= 1 e1075: b350 + b356 + b363 + b370 >= 1 e1076: b350 + b356 + b363 + b366 >= 1 e1077: b350 + b356 + b362 + b376 >= 1 e1078: b350 + b356 + b362 + b370 >= 1 e1079: b350 + b356 + b362 + b366 >= 1 e1080: b350 + b356 + b361 + b376 >= 1 e1081: b350 + b356 + b361 + b371 >= 1 e1082: b350 + b356 + b361 + b366 >= 1 e1083: b350 + b355 + b375 >= 1 e1084: b350 + b355 + b371 + b376 >= 1 e1085: b350 + b355 + b370 >= 1 e1086: b350 + b355 + b366 >= 1 e1087: b350 + b355 + b363 + b376 >= 1 e1088: b350 + b355 + b363 + b370 >= 1 e1089: b350 + b355 + b363 + b366 >= 1 e1090: b350 + b355 + b362 + b376 >= 1 e1091: b350 + b355 + b362 + b371 >= 1 e1092: b350 + b355 + b362 + b366 >= 1 e1093: b350 + b354 + b375 >= 1 e1094: b350 + b354 + b371 + b376 >= 1 e1095: b350 + b354 + b370 >= 1 e1096: b350 + b354 + b366 >= 1 e1097: b350 + b354 + b363 + b376 >= 1 e1098: b350 + b354 + b363 + b371 >= 1 e1099: b350 + b354 + b363 + b366 >= 1 e1100: b350 + b353 + b376 >= 1 e1101: b350 + b353 + b371 >= 1 e1102: b350 + b353 + b366 >= 1 e1103: b349 + b374 >= 1 e1104: b349 + b371 + b375 >= 1 e1105: b349 + b370 + b376 >= 1 e1106: b349 + b369 >= 1 e1107: b349 + b366 + b376 >= 1 e1108: b349 + b366 + b371 >= 1 e1109: b349 + b365 >= 1 e1110: b349 + b363 + b375 >= 1 e1111: b349 + b363 + b371 + b376 >= 1 e1112: b349 + b363 + b370 >= 1 e1113: b349 + b363 + b366 >= 1 e1114: b349 + b362 + b375 >= 1 e1115: b349 + b362 + b371 + b376 >= 1 e1116: b349 + b362 + b370 >= 1 e1117: b349 + b362 + b366 >= 1 e1118: b349 + b361 + b376 >= 1 e1119: b349 + b361 + b371 >= 1 e1120: b349 + b361 + b366 >= 1 e1121: b349 + b357 + b375 >= 1 e1122: b349 + b357 + b371 + b376 >= 1 e1123: b349 + b357 + b370 >= 1 e1124: b349 + b357 + b366 >= 1 e1125: b349 + b357 + b363 + b376 >= 1 e1126: b349 + b357 + b363 + b370 >= 1 e1127: b349 + b357 + b363 + b366 >= 1 e1128: b349 + b357 + b362 + b376 >= 1 e1129: b349 + b357 + b362 + b371 >= 1 e1130: b349 + b357 + b362 + b366 >= 1 e1131: b349 + b356 + b375 >= 1 e1132: b349 + b356 + b371 + b376 >= 1 e1133: b349 + b356 + b370 >= 1 e1134: b349 + b356 + b366 >= 1 e1135: b349 + b356 + b363 + b376 >= 1 e1136: b349 + b356 + b363 + b371 >= 1 e1137: b349 + b356 + b363 + b366 >= 1 e1138: b349 + b355 + b376 >= 1 e1139: b349 + b355 + b371 >= 1 e1140: b349 + b355 + b366 >= 1 e1141: b348 + b376 >= 1 e1142: b348 + b371 >= 1 e1143: b348 + b366 >= 1 e1144: b347 + b372 >= 1 e1145: b347 + b371 + b373 >= 1 e1146: b347 + b370 + b374 >= 1 e1147: b347 + b369 + b375 >= 1 e1148: b347 + b368 + b376 >= 1 e1149: b347 + b367 >= 1 e1150: b347 + b366 + b374 >= 1 e1151: b347 + b366 + b371 + b375 >= 1 e1152: b347 + b366 + b370 + b376 >= 1 e1153: b347 + b366 + b369 >= 1 e1154: b347 + b365 + b376 >= 1 e1155: b347 + b365 + b371 >= 1 e1156: b347 + b364 >= 1 e1157: b347 + b363 + b373 >= 1 e1158: b347 + b363 + b371 + b374 >= 1 e1159: b347 + b363 + b369 + b376 >= 1 e1160: b347 + b363 + b368 >= 1 e1161: b347 + b363 + b366 + b374 >= 1 e1162: b347 + b363 + b366 + b371 + b375 >= 1 e1163: b347 + b363 + b366 + b370 + b376 >= 1 e1164: b347 + b363 + b366 + b369 >= 1 e1165: b347 + b363 + b365 >= 1 e1166: b347 + b362 + b373 >= 1 e1167: b347 + b362 + b371 + b374 >= 1 e1168: b347 + b362 + b370 + b375 >= 1 e1169: b347 + b362 + b369 + b376 >= 1 e1170: b347 + b362 + b368 >= 1 e1171: b347 + b362 + b366 + b375 >= 1 e1172: b347 + b362 + b366 + b371 + b376 >= 1 e1173: b347 + b362 + b366 + b370 >= 1 e1174: b347 + b362 + b365 >= 1 e1175: b347 + b361 + b374 >= 1 e1176: b347 + b361 + b371 + b375 >= 1 e1177: b347 + b361 + b370 + b376 >= 1 e1178: b347 + b361 + b369 >= 1 e1179: b347 + b361 + b366 + b376 >= 1 e1180: b347 + b361 + b366 + b371 >= 1 e1181: b347 + b361 + b365 >= 1 e1182: b347 + b360 + b375 >= 1 e1183: b347 + b360 + b371 + b376 >= 1 e1184: b347 + b360 + b370 >= 1 e1185: b347 + b360 + b366 >= 1 e1186: b347 + b359 + b376 >= 1 e1187: b347 + b359 + b371 >= 1 e1188: b347 + b359 + b366 >= 1 e1189: b347 + b357 + b373 >= 1 e1190: b347 + b357 + b370 + b374 >= 1 e1191: b347 + b357 + b369 + b375 >= 1 e1192: b347 + b357 + b368 + b376 >= 1 e1193: b347 + b357 + b367 >= 1 e1194: b347 + b357 + b366 + b374 >= 1 e1195: b347 + b357 + b366 + b371 + b375 >= 1 e1196: b347 + b357 + b366 + b370 >= 1 e1197: b347 + b357 + b365 >= 1 e1198: b347 + b357 + b363 + b373 >= 1 e1199: b347 + b357 + b363 + b371 + b374 >= 1 e1200: b347 + b357 + b363 + b370 + b375 >= 1 e1201: b347 + b357 + b363 + b369 + b376 >= 1 e1202: b347 + b357 + b363 + b368 >= 1 e1203: b347 + b357 + b363 + b366 + b375 >= 1 e1204: b347 + b357 + b363 + b366 + b371 + b376 >= 1 e1205: b347 + b357 + b363 + b366 + b370 >= 1 e1206: b347 + b357 + b363 + b365 >= 1 e1207: b347 + b357 + b362 + b374 >= 1 e1208: b347 + b357 + b362 + b371 + b375 >= 1 e1209: b347 + b357 + b362 + b370 + b376 >= 1 e1210: b347 + b357 + b362 + b369 >= 1 e1211: b347 + b357 + b362 + b366 + b376 >= 1 e1212: b347 + b357 + b362 + b366 + b371 >= 1 e1213: b347 + b357 + b362 + b365 >= 1 e1214: b347 + b357 + b361 + b375 >= 1 e1215: b347 + b357 + b361 + b371 + b376 >= 1 e1216: b347 + b357 + b361 + b370 >= 1 e1217: b347 + b357 + b361 + b366 >= 1 e1218: b347 + b357 + b360 + b376 >= 1 e1219: b347 + b357 + b360 + b371 >= 1 e1220: b347 + b357 + b360 + b366 >= 1 e1221: b347 + b356 + b373 >= 1 e1222: b347 + b356 + b371 + b374 >= 1 e1223: b347 + b356 + b370 + b375 >= 1 e1224: b347 + b356 + b369 + b376 >= 1 e1225: b347 + b356 + b368 >= 1 e1226: b347 + b356 + b366 + b375 >= 1 e1227: b347 + b356 + b366 + b371 + b376 >= 1 e1228: b347 + b356 + b366 + b370 >= 1 e1229: b347 + b356 + b365 >= 1 e1230: b347 + b356 + b363 + b374 >= 1 e1231: b347 + b356 + b363 + b371 + b375 >= 1 e1232: b347 + b356 + b363 + b370 + b376 >= 1 e1233: b347 + b356 + b363 + b369 >= 1 e1234: b347 + b356 + b363 + b366 + b376 >= 1 e1235: b347 + b356 + b363 + b366 + b371 >= 1 e1236: b347 + b356 + b363 + b365 >= 1 e1237: b347 + b356 + b362 + b375 >= 1 e1238: b347 + b356 + b362 + b371 + b376 >= 1 e1239: b347 + b356 + b362 + b370 >= 1 e1240: b347 + b356 + b362 + b366 >= 1 e1241: b347 + b356 + b361 + b376 >= 1 e1242: b347 + b356 + b361 + b371 >= 1 e1243: b347 + b356 + b361 + b366 >= 1 e1244: b347 + b356 + b360 + b376 >= 1 e1245: b347 + b356 + b360 + b371 >= 1 e1246: b347 + b356 + b360 + b366 >= 1 e1247: b347 + b355 + b374 >= 1 e1248: b347 + b355 + b371 + b375 >= 1 e1249: b347 + b355 + b370 + b376 >= 1 e1250: b347 + b355 + b369 >= 1 e1251: b347 + b355 + b366 + b376 >= 1 e1252: b347 + b355 + b366 + b371 >= 1 e1253: b347 + b355 + b365 >= 1 e1254: b347 + b355 + b363 + b375 >= 1 e1255: b347 + b355 + b363 + b371 + b376 >= 1 e1256: b347 + b355 + b363 + b370 >= 1 e1257: b347 + b355 + b363 + b366 >= 1 e1258: b347 + b355 + b362 + b376 >= 1 e1259: b347 + b355 + b362 + b371 >= 1 e1260: b347 + b355 + b362 + b366 >= 1 e1261: b347 + b355 + b361 + b376 >= 1 e1262: b347 + b355 + b361 + b371 >= 1 e1263: b347 + b355 + b361 + b366 >= 1 e1264: b347 + b354 + b375 >= 1 e1265: b347 + b354 + b371 + b376 >= 1 e1266: b347 + b354 + b370 >= 1 e1267: b347 + b354 + b366 >= 1 e1268: b347 + b354 + b363 + b376 >= 1 e1269: b347 + b354 + b363 + b371 >= 1 e1270: b347 + b354 + b363 + b366 >= 1 e1271: b347 + b354 + b362 + b376 >= 1 e1272: b347 + b354 + b362 + b371 >= 1 e1273: b347 + b354 + b362 + b366 >= 1 e1274: b347 + b353 + b376 >= 1 e1275: b347 + b353 + b371 >= 1 e1276: b347 + b353 + b366 >= 1 e1277: b347 + b351 + b373 >= 1 e1278: b347 + b351 + b371 + b374 >= 1 e1279: b347 + b351 + b370 + b375 >= 1 e1280: b347 + b351 + b369 + b376 >= 1 e1281: b347 + b351 + b368 >= 1 e1282: b347 + b351 + b366 + b375 >= 1 e1283: b347 + b351 + b366 + b371 + b376 >= 1 e1284: b347 + b351 + b366 + b370 >= 1 e1285: b347 + b351 + b365 >= 1 e1286: b347 + b351 + b363 + b374 >= 1 e1287: b347 + b351 + b363 + b371 + b375 >= 1 e1288: b347 + b351 + b363 + b370 + b376 >= 1 e1289: b347 + b351 + b363 + b369 >= 1 e1290: b347 + b351 + b363 + b366 + b376 >= 1 e1291: b347 + b351 + b363 + b366 + b371 >= 1 e1292: b347 + b351 + b363 + b365 >= 1 e1293: b347 + b351 + b362 + b374 >= 1 e1294: b347 + b351 + b362 + b371 + b375 >= 1 e1295: b347 + b351 + b362 + b370 + b376 >= 1 e1296: b347 + b351 + b362 + b369 >= 1 e1297: b347 + b351 + b362 + b366 + b376 >= 1 e1298: b347 + b351 + b362 + b366 + b371 >= 1 e1299: b347 + b351 + b362 + b365 >= 1 e1300: b347 + b351 + b361 + b375 >= 1 e1301: b347 + b351 + b361 + b371 + b376 >= 1 e1302: b347 + b351 + b361 + b370 >= 1 e1303: b347 + b351 + b361 + b366 >= 1 e1304: b347 + b351 + b360 + b376 >= 1 e1305: b347 + b351 + b360 + b371 >= 1 e1306: b347 + b351 + b360 + b366 >= 1 e1307: b347 + b351 + b357 + b374 >= 1 e1308: b347 + b351 + b357 + b371 + b375 >= 1 e1309: b347 + b351 + b357 + b370 + b376 >= 1 e1310: b347 + b351 + b357 + b369 >= 1 e1311: b347 + b351 + b357 + b366 + b376 >= 1 e1312: b347 + b351 + b357 + b366 + b371 >= 1 e1313: b347 + b351 + b357 + b365 >= 1 e1314: b347 + b351 + b357 + b363 + b375 >= 1 e1315: b347 + b351 + b357 + b363 + b371 + b376 >= 1 e1316: b347 + b351 + b357 + b363 + b370 >= 1 e1317: b347 + b351 + b357 + b363 + b366 >= 1 e1318: b347 + b351 + b357 + b362 + b375 >= 1 e1319: b347 + b351 + b357 + b362 + b371 + b376 >= 1 e1320: b347 + b351 + b357 + b362 + b370 >= 1 e1321: b347 + b351 + b357 + b362 + b366 >= 1 e1322: b347 + b351 + b357 + b361 + b376 >= 1 e1323: b347 + b351 + b357 + b361 + b371 >= 1 e1324: b347 + b351 + b357 + b361 + b366 >= 1 e1325: b347 + b351 + b356 + b374 >= 1 e1326: b347 + b351 + b356 + b371 + b375 >= 1 e1327: b347 + b351 + b356 + b370 + b376 >= 1 e1328: b347 + b351 + b356 + b369 >= 1 e1329: b347 + b351 + b356 + b366 + b376 >= 1 e1330: b347 + b351 + b356 + b366 + b371 >= 1 e1331: b347 + b351 + b356 + b365 >= 1 e1332: b347 + b351 + b356 + b363 + b375 >= 1 e1333: b347 + b351 + b356 + b363 + b371 + b376 >= 1 e1334: b347 + b351 + b356 + b363 + b370 >= 1 e1335: b347 + b351 + b356 + b363 + b366 >= 1 e1336: b347 + b351 + b356 + b362 + b376 >= 1 e1337: b347 + b351 + b356 + b362 + b371 >= 1 e1338: b347 + b351 + b356 + b362 + b366 >= 1 e1339: b347 + b351 + b355 + b375 >= 1 e1340: b347 + b351 + b355 + b371 + b376 >= 1 e1341: b347 + b351 + b355 + b370 >= 1 e1342: b347 + b351 + b355 + b366 >= 1 e1343: b347 + b351 + b355 + b363 + b376 >= 1 e1344: b347 + b351 + b355 + b363 + b371 >= 1 e1345: b347 + b351 + b355 + b363 + b366 >= 1 e1346: b347 + b351 + b354 + b376 >= 1 e1347: b347 + b351 + b354 + b371 >= 1 e1348: b347 + b351 + b354 + b366 >= 1 e1349: b347 + b350 + b374 >= 1 e1350: b347 + b350 + b371 + b375 >= 1 e1351: b347 + b350 + b370 + b376 >= 1 e1352: b347 + b350 + b369 >= 1 e1353: b347 + b350 + b366 + b376 >= 1 e1354: b347 + b350 + b366 + b371 >= 1 e1355: b347 + b350 + b365 >= 1 e1356: b347 + b350 + b363 + b375 >= 1 e1357: b347 + b350 + b363 + b371 + b376 >= 1 e1358: b347 + b350 + b363 + b370 >= 1 e1359: b347 + b350 + b363 + b366 >= 1 e1360: b347 + b350 + b362 + b376 >= 1 e1361: b347 + b350 + b362 + b371 >= 1 e1362: b347 + b350 + b362 + b366 >= 1 e1363: b347 + b350 + b357 + b375 >= 1 e1364: b347 + b350 + b357 + b371 + b376 >= 1 e1365: b347 + b350 + b357 + b370 >= 1 e1366: b347 + b350 + b357 + b366 >= 1 e1367: b347 + b350 + b357 + b363 + b376 >= 1 e1368: b347 + b350 + b357 + b363 + b371 >= 1 e1369: b347 + b350 + b357 + b363 + b366 >= 1 e1370: b347 + b350 + b356 + b376 >= 1 e1371: b347 + b350 + b356 + b371 >= 1 e1372: b347 + b350 + b356 + b366 >= 1 e1373: b347 + b349 + b376 >= 1 e1374: b347 + b349 + b371 >= 1 e1375: b347 + b349 + b366 >= 1 e1376: b346 + b374 >= 1 e1377: b346 + b371 + b375 >= 1 e1378: b346 + b370 + b376 >= 1 e1379: b346 + b369 >= 1 e1380: b346 + b366 + b376 >= 1 e1381: b346 + b366 + b371 >= 1 e1382: b346 + b365 >= 1 e1383: b346 + b363 + b375 >= 1 e1384: b346 + b363 + b371 + b376 >= 1 e1385: b346 + b363 + b370 >= 1 e1386: b346 + b363 + b366 >= 1 e1387: b346 + b362 + b375 >= 1 e1388: b346 + b362 + b371 + b376 >= 1 e1389: b346 + b362 + b370 >= 1 e1390: b346 + b362 + b366 >= 1 e1391: b346 + b361 + b376 >= 1 e1392: b346 + b361 + b371 >= 1 e1393: b346 + b361 + b366 >= 1 e1394: b346 + b357 + b375 >= 1 e1395: b346 + b357 + b371 + b376 >= 1 e1396: b346 + b357 + b370 >= 1 e1397: b346 + b357 + b366 >= 1 e1398: b346 + b357 + b363 + b376 >= 1 e1399: b346 + b357 + b363 + b370 >= 1 e1400: b346 + b357 + b363 + b366 >= 1 e1401: b346 + b357 + b362 + b376 >= 1 e1402: b346 + b357 + b362 + b371 >= 1 e1403: b346 + b357 + b362 + b366 >= 1 e1404: b346 + b356 + b375 >= 1 e1405: b346 + b356 + b371 + b376 >= 1 e1406: b346 + b356 + b370 >= 1 e1407: b346 + b356 + b366 >= 1 e1408: b346 + b356 + b363 + b376 >= 1 e1409: b346 + b356 + b363 + b371 >= 1 e1410: b346 + b356 + b363 + b366 >= 1 e1411: b346 + b355 + b376 >= 1 e1412: b346 + b355 + b371 >= 1 e1413: b346 + b355 + b366 >= 1 e1414: b346 + b351 + b375 >= 1 e1415: b346 + b351 + b371 + b376 >= 1 e1416: b346 + b351 + b370 >= 1 e1417: b346 + b351 + b366 >= 1 e1418: b346 + b351 + b363 + b376 >= 1 e1419: b346 + b351 + b363 + b371 >= 1 e1420: b346 + b351 + b363 + b366 >= 1 e1421: b346 + b351 + b357 + b376 >= 1 e1422: b346 + b351 + b357 + b371 >= 1 e1423: b346 + b351 + b357 + b366 >= 1 e1424: b346 + b350 + b376 >= 1 e1425: b346 + b350 + b371 >= 1 e1426: b346 + b350 + b366 >= 1 e1427: b345 + b376 >= 1 e1428: b345 + b371 >= 1 e1429: b345 + b366 >= 1 e1430: b344 + b372 >= 1 e1431: b344 + b371 + b373 >= 1 e1432: b344 + b370 + b374 >= 1 e1433: b344 + b369 + b375 >= 1 e1434: b344 + b368 + b376 >= 1 e1435: b344 + b367 >= 1 e1436: b344 + b366 + b374 >= 1 e1437: b344 + b366 + b371 + b375 >= 1 e1438: b344 + b366 + b370 + b376 >= 1 e1439: b344 + b366 + b369 >= 1 e1440: b344 + b365 + b376 >= 1 e1441: b344 + b365 + b371 >= 1 e1442: b344 + b364 >= 1 e1443: b344 + b363 + b373 >= 1 e1444: b344 + b363 + b371 + b374 >= 1 e1445: b344 + b363 + b370 + b375 >= 1 e1446: b344 + b363 + b369 + b376 >= 1 e1447: b344 + b363 + b368 >= 1 e1448: b344 + b363 + b366 + b375 >= 1 e1449: b344 + b363 + b366 + b371 + b376 >= 1 e1450: b344 + b363 + b366 + b370 >= 1 e1451: b344 + b363 + b365 >= 1 e1452: b344 + b362 + b373 >= 1 e1453: b344 + b362 + b371 + b374 >= 1 e1454: b344 + b362 + b370 + b375 >= 1 e1455: b344 + b362 + b369 >= 1 e1456: b344 + b362 + b366 + b375 >= 1 e1457: b344 + b362 + b366 + b371 + b376 >= 1 e1458: b344 + b362 + b366 + b370 >= 1 e1459: b344 + b362 + b365 >= 1 e1460: b344 + b361 + b374 >= 1 e1461: b344 + b361 + b371 + b375 >= 1 e1462: b344 + b361 + b370 + b376 >= 1 e1463: b344 + b361 + b369 >= 1 e1464: b344 + b361 + b366 + b376 >= 1 e1465: b344 + b361 + b366 + b371 >= 1 e1466: b344 + b361 + b365 >= 1 e1467: b344 + b360 + b375 >= 1 e1468: b344 + b360 + b371 + b376 >= 1 e1469: b344 + b360 + b370 >= 1 e1470: b344 + b360 + b366 >= 1 e1471: b344 + b359 + b376 >= 1 e1472: b344 + b359 + b371 >= 1 e1473: b344 + b359 + b366 >= 1 e1474: b344 + b357 + b373 >= 1 e1475: b344 + b357 + b371 + b374 >= 1 e1476: b344 + b357 + b370 + b375 >= 1 e1477: b344 + b357 + b369 + b376 >= 1 e1478: b344 + b357 + b368 >= 1 e1479: b344 + b357 + b366 + b375 >= 1 e1480: b344 + b357 + b366 + b371 + b376 >= 1 e1481: b344 + b357 + b366 + b370 >= 1 e1482: b344 + b357 + b365 >= 1 e1483: b344 + b357 + b363 + b374 >= 1 e1484: b344 + b357 + b363 + b370 + b376 >= 1 e1485: b344 + b357 + b363 + b369 >= 1 e1486: b344 + b357 + b363 + b366 + b376 >= 1 e1487: b344 + b357 + b363 + b366 + b370 >= 1 e1488: b344 + b357 + b363 + b365 >= 1 e1489: b344 + b357 + b362 + b374 >= 1 e1490: b344 + b357 + b362 + b371 + b375 >= 1 e1491: b344 + b357 + b362 + b370 + b376 >= 1 e1492: b344 + b357 + b362 + b369 >= 1 e1493: b344 + b357 + b362 + b366 + b376 >= 1 e1494: b344 + b357 + b362 + b366 + b371 >= 1 e1495: b344 + b357 + b362 + b365 >= 1 e1496: b344 + b357 + b361 + b375 >= 1 e1497: b344 + b357 + b361 + b371 + b376 >= 1 e1498: b344 + b357 + b361 + b370 >= 1 e1499: b344 + b357 + b361 + b366 >= 1 e1500: b344 + b357 + b360 + b376 >= 1 e1501: b344 + b357 + b360 + b371 >= 1 e1502: b344 + b357 + b360 + b366 >= 1 e1503: b344 + b356 + b373 >= 1 e1504: b344 + b356 + b371 + b374 >= 1 e1505: b344 + b356 + b370 + b375 >= 1 e1506: b344 + b356 + b369 + b376 >= 1 e1507: b344 + b356 + b368 >= 1 e1508: b344 + b356 + b366 + b375 >= 1 e1509: b344 + b356 + b366 + b371 + b376 >= 1 e1510: b344 + b356 + b366 + b370 >= 1 e1511: b344 + b356 + b365 >= 1 e1512: b344 + b356 + b363 + b374 >= 1 e1513: b344 + b356 + b363 + b371 + b375 >= 1 e1514: b344 + b356 + b363 + b370 + b376 >= 1 e1515: b344 + b356 + b363 + b369 >= 1 e1516: b344 + b356 + b363 + b366 + b376 >= 1 e1517: b344 + b356 + b363 + b366 + b371 >= 1 e1518: b344 + b356 + b363 + b365 >= 1 e1519: b344 + b356 + b362 + b375 >= 1 e1520: b344 + b356 + b362 + b371 + b376 >= 1 e1521: b344 + b356 + b362 + b370 >= 1 e1522: b344 + b356 + b362 + b366 >= 1 e1523: b344 + b356 + b361 + b376 >= 1 e1524: b344 + b356 + b361 + b371 >= 1 e1525: b344 + b356 + b361 + b366 >= 1 e1526: b344 + b355 + b374 >= 1 e1527: b344 + b355 + b371 + b375 >= 1 e1528: b344 + b355 + b370 + b376 >= 1 e1529: b344 + b355 + b369 >= 1 e1530: b344 + b355 + b366 + b376 >= 1 e1531: b344 + b355 + b366 + b371 >= 1 e1532: b344 + b355 + b365 >= 1 e1533: b344 + b355 + b363 + b375 >= 1 e1534: b344 + b355 + b363 + b371 + b376 >= 1 e1535: b344 + b355 + b363 + b370 >= 1 e1536: b344 + b355 + b363 + b366 >= 1 e1537: b344 + b355 + b362 + b376 >= 1 e1538: b344 + b355 + b362 + b371 >= 1 e1539: b344 + b355 + b362 + b366 >= 1 e1540: b344 + b354 + b375 >= 1 e1541: b344 + b354 + b371 + b376 >= 1 e1542: b344 + b354 + b370 >= 1 e1543: b344 + b354 + b366 >= 1 e1544: b344 + b354 + b363 + b376 >= 1 e1545: b344 + b354 + b363 + b371 >= 1 e1546: b344 + b354 + b363 + b366 >= 1 e1547: b344 + b353 + b376 >= 1 e1548: b344 + b353 + b371 >= 1 e1549: b344 + b353 + b366 >= 1 e1550: b344 + b351 + b373 >= 1 e1551: b344 + b351 + b371 + b374 >= 1 e1552: b344 + b351 + b370 + b375 >= 1 e1553: b344 + b351 + b369 + b376 >= 1 e1554: b344 + b351 + b368 >= 1 e1555: b344 + b351 + b366 + b375 >= 1 e1556: b344 + b351 + b366 + b371 + b376 >= 1 e1557: b344 + b351 + b366 + b370 >= 1 e1558: b344 + b351 + b365 >= 1 e1559: b344 + b351 + b363 + b374 >= 1 e1560: b344 + b351 + b363 + b371 + b375 >= 1 e1561: b344 + b351 + b363 + b370 + b376 >= 1 e1562: b344 + b351 + b363 + b369 >= 1 e1563: b344 + b351 + b363 + b366 + b376 >= 1 e1564: b344 + b351 + b363 + b366 + b371 >= 1 e1565: b344 + b351 + b363 + b365 >= 1 e1566: b344 + b351 + b362 + b375 >= 1 e1567: b344 + b351 + b362 + b371 + b376 >= 1 e1568: b344 + b351 + b362 + b370 >= 1 e1569: b344 + b351 + b362 + b366 >= 1 e1570: b344 + b351 + b361 + b375 >= 1 e1571: b344 + b351 + b361 + b371 + b376 >= 1 e1572: b344 + b351 + b361 + b370 >= 1 e1573: b344 + b351 + b361 + b366 >= 1 e1574: b344 + b351 + b360 + b376 >= 1 e1575: b344 + b351 + b360 + b371 >= 1 e1576: b344 + b351 + b360 + b366 >= 1 e1577: b344 + b351 + b357 + b374 >= 1 e1578: b344 + b351 + b357 + b371 + b375 >= 1 e1579: b344 + b351 + b357 + b370 + b376 >= 1 e1580: b344 + b351 + b357 + b369 >= 1 e1581: b344 + b351 + b357 + b366 + b376 >= 1 e1582: b344 + b351 + b357 + b366 + b371 >= 1 e1583: b344 + b351 + b357 + b365 >= 1 e1584: b344 + b351 + b357 + b363 + b375 >= 1 e1585: b344 + b351 + b357 + b363 + b371 + b376 >= 1 e1586: b344 + b351 + b357 + b363 + b370 >= 1 e1587: b344 + b351 + b357 + b363 + b366 >= 1 e1588: b344 + b351 + b357 + b362 + b375 >= 1 e1589: b344 + b351 + b357 + b362 + b371 + b376 >= 1 e1590: b344 + b351 + b357 + b362 + b370 >= 1 e1591: b344 + b351 + b357 + b362 + b366 >= 1 e1592: b344 + b351 + b357 + b361 + b376 >= 1 e1593: b344 + b351 + b357 + b361 + b371 >= 1 e1594: b344 + b351 + b357 + b361 + b366 >= 1 e1595: b344 + b351 + b356 + b375 >= 1 e1596: b344 + b351 + b356 + b370 >= 1 e1597: b344 + b351 + b356 + b366 >= 1 e1598: b344 + b351 + b356 + b363 + b375 >= 1 e1599: b344 + b351 + b356 + b363 + b371 + b376 >= 1 e1600: b344 + b351 + b356 + b363 + b370 >= 1 e1601: b344 + b351 + b356 + b363 + b366 >= 1 e1602: b344 + b351 + b356 + b362 + b376 >= 1 e1603: b344 + b351 + b356 + b362 + b371 >= 1 e1604: b344 + b351 + b356 + b362 + b366 >= 1 e1605: b344 + b351 + b355 + b375 >= 1 e1606: b344 + b351 + b355 + b371 + b376 >= 1 e1607: b344 + b351 + b355 + b370 >= 1 e1608: b344 + b351 + b355 + b366 >= 1 e1609: b344 + b351 + b355 + b363 + b376 >= 1 e1610: b344 + b351 + b355 + b363 + b371 >= 1 e1611: b344 + b351 + b355 + b363 + b366 >= 1 e1612: b344 + b351 + b354 + b376 >= 1 e1613: b344 + b351 + b354 + b371 >= 1 e1614: b344 + b351 + b354 + b366 >= 1 e1615: b344 + b350 + b374 >= 1 e1616: b344 + b350 + b371 + b375 >= 1 e1617: b344 + b350 + b370 + b376 >= 1 e1618: b344 + b350 + b369 >= 1 e1619: b344 + b350 + b366 + b376 >= 1 e1620: b344 + b350 + b366 + b371 >= 1 e1621: b344 + b350 + b365 >= 1 e1622: b344 + b350 + b363 + b375 >= 1 e1623: b344 + b350 + b363 + b371 + b376 >= 1 e1624: b344 + b350 + b363 + b370 >= 1 e1625: b344 + b350 + b363 + b366 >= 1 e1626: b344 + b350 + b362 + b376 >= 1 e1627: b344 + b350 + b362 + b371 >= 1 e1628: b344 + b350 + b362 + b366 >= 1 e1629: b344 + b350 + b357 + b375 >= 1 e1630: b344 + b350 + b357 + b371 + b376 >= 1 e1631: b344 + b350 + b357 + b370 >= 1 e1632: b344 + b350 + b357 + b366 >= 1 e1633: b344 + b350 + b357 + b363 + b376 >= 1 e1634: b344 + b350 + b357 + b363 + b371 >= 1 e1635: b344 + b350 + b357 + b363 + b366 >= 1 e1636: b344 + b350 + b356 + b376 >= 1 e1637: b344 + b350 + b356 + b371 >= 1 e1638: b344 + b350 + b356 + b366 >= 1 e1639: b344 + b349 + b376 >= 1 e1640: b344 + b349 + b371 >= 1 e1641: b344 + b349 + b366 >= 1 e1642: b344 + b347 + b374 >= 1 e1643: b344 + b347 + b371 + b375 >= 1 e1644: b344 + b347 + b370 + b376 >= 1 e1645: b344 + b347 + b369 >= 1 e1646: b344 + b347 + b366 + b376 >= 1 e1647: b344 + b347 + b366 + b371 >= 1 e1648: b344 + b347 + b365 >= 1 e1649: b344 + b347 + b363 + b375 >= 1 e1650: b344 + b347 + b363 + b371 + b376 >= 1 e1651: b344 + b347 + b363 + b370 >= 1 e1652: b344 + b347 + b363 + b366 >= 1 e1653: b344 + b347 + b362 + b375 >= 1 e1654: b344 + b347 + b362 + b371 + b376 >= 1 e1655: b344 + b347 + b362 + b370 >= 1 e1656: b344 + b347 + b362 + b366 >= 1 e1657: b344 + b347 + b361 + b376 >= 1 e1658: b344 + b347 + b361 + b371 >= 1 e1659: b344 + b347 + b361 + b366 >= 1 e1660: b344 + b347 + b357 + b375 >= 1 e1661: b344 + b347 + b357 + b371 + b376 >= 1 e1662: b344 + b347 + b357 + b370 >= 1 e1663: b344 + b347 + b357 + b366 >= 1 e1664: b344 + b347 + b357 + b363 + b375 >= 1 e1665: b344 + b347 + b357 + b363 + b371 + b376 >= 1 e1666: b344 + b347 + b357 + b363 + b370 >= 1 e1667: b344 + b347 + b357 + b363 + b366 >= 1 e1668: b344 + b347 + b357 + b362 + b376 >= 1 e1669: b344 + b347 + b357 + b362 + b371 >= 1 e1670: b344 + b347 + b357 + b362 + b366 >= 1 e1671: b344 + b347 + b356 + b375 >= 1 e1672: b344 + b347 + b356 + b371 + b376 >= 1 e1673: b344 + b347 + b356 + b370 >= 1 e1674: b344 + b347 + b356 + b366 >= 1 e1675: b344 + b347 + b356 + b363 + b376 >= 1 e1676: b344 + b347 + b356 + b363 + b371 >= 1 e1677: b344 + b347 + b356 + b363 + b366 >= 1 e1678: b344 + b347 + b355 + b376 >= 1 e1679: b344 + b347 + b355 + b371 >= 1 e1680: b344 + b347 + b355 + b366 >= 1 e1681: b344 + b347 + b351 + b375 >= 1 e1682: b344 + b347 + b351 + b371 + b376 >= 1 e1683: b344 + b347 + b351 + b370 >= 1 e1684: b344 + b347 + b351 + b366 >= 1 e1685: b344 + b347 + b351 + b363 + b376 >= 1 e1686: b344 + b347 + b351 + b363 + b371 >= 1 e1687: b344 + b347 + b351 + b363 + b366 >= 1 e1688: b344 + b347 + b351 + b362 + b376 >= 1 e1689: b344 + b347 + b351 + b362 + b371 >= 1 e1690: b344 + b347 + b351 + b362 + b366 >= 1 e1691: b344 + b347 + b351 + b357 + b376 >= 1 e1692: b344 + b347 + b351 + b357 + b371 >= 1 e1693: b344 + b347 + b351 + b357 + b366 >= 1 e1694: b344 + b347 + b351 + b356 + b376 >= 1 e1695: b344 + b347 + b351 + b356 + b371 >= 1 e1696: b344 + b347 + b351 + b356 + b366 >= 1 e1697: b344 + b347 + b350 + b376 >= 1 e1698: b344 + b347 + b350 + b371 >= 1 e1699: b344 + b347 + b350 + b366 >= 1 e1700: b344 + b346 + b376 >= 1 e1701: b344 + b346 + b371 >= 1 e1702: b344 + b346 + b366 >= 1 e1703: b343 + b374 >= 1 e1704: b343 + b371 + b375 >= 1 e1705: b343 + b370 + b376 >= 1 e1706: b343 + b369 >= 1 e1707: b343 + b366 + b376 >= 1 e1708: b343 + b366 + b371 >= 1 e1709: b343 + b365 >= 1 e1710: b343 + b363 + b375 >= 1 e1711: b343 + b363 + b371 + b376 >= 1 e1712: b343 + b363 + b370 >= 1 e1713: b343 + b363 + b366 >= 1 e1714: b343 + b362 + b375 >= 1 e1715: b343 + b362 + b371 + b376 >= 1 e1716: b343 + b362 + b370 >= 1 e1717: b343 + b362 + b366 >= 1 e1718: b343 + b361 + b376 >= 1 e1719: b343 + b361 + b371 >= 1 e1720: b343 + b361 + b366 >= 1 e1721: b343 + b357 + b375 >= 1 e1722: b343 + b357 + b370 + b376 >= 1 e1723: b343 + b357 + b369 >= 1 e1724: b343 + b357 + b366 >= 1 e1725: b343 + b357 + b363 + b375 >= 1 e1726: b343 + b357 + b363 + b371 + b376 >= 1 e1727: b343 + b357 + b363 + b370 >= 1 e1728: b343 + b357 + b363 + b366 >= 1 e1729: b343 + b357 + b362 + b376 >= 1 e1730: b343 + b357 + b362 + b371 >= 1 e1731: b343 + b357 + b362 + b366 >= 1 e1732: b343 + b356 + b375 >= 1 e1733: b343 + b356 + b371 + b376 >= 1 e1734: b343 + b356 + b370 >= 1 e1735: b343 + b356 + b366 >= 1 e1736: b343 + b356 + b363 + b376 >= 1 e1737: b343 + b356 + b363 + b371 >= 1 e1738: b343 + b356 + b363 + b366 >= 1 e1739: b343 + b355 + b376 >= 1 e1740: b343 + b355 + b371 >= 1 e1741: b343 + b355 + b366 >= 1 e1742: b343 + b351 + b375 >= 1 e1743: b343 + b351 + b371 + b376 >= 1 e1744: b343 + b351 + b370 >= 1 e1745: b343 + b351 + b366 >= 1 e1746: b343 + b351 + b363 + b376 >= 1 e1747: b343 + b351 + b363 + b371 >= 1 e1748: b343 + b351 + b363 + b366 >= 1 e1749: b343 + b351 + b357 + b376 >= 1 e1750: b343 + b351 + b357 + b371 >= 1 e1751: b343 + b351 + b357 + b366 >= 1 e1752: b343 + b351 + b356 + b376 >= 1 e1753: b343 + b351 + b356 + b371 >= 1 e1754: b343 + b351 + b356 + b366 >= 1 e1755: b343 + b350 + b376 >= 1 e1756: b343 + b350 + b371 >= 1 e1757: b343 + b350 + b366 >= 1 e1758: b343 + b347 + b376 >= 1 e1759: b343 + b347 + b371 >= 1 e1760: b343 + b347 + b366 >= 1 e1761: b343 + b347 + b357 + b376 >= 1 e1762: b343 + b347 + b357 + b371 >= 1 e1763: b343 + b347 + b357 + b366 >= 1 e1764: b342 + b376 >= 1 e1765: b342 + b371 >= 1 e1766: b342 + b366 >= 1 e1767: b341 + b372 >= 1 e1768: b341 + b371 + b373 >= 1 e1769: b341 + b370 + b374 >= 1 e1770: b341 + b369 + b375 >= 1 e1771: b341 + b368 + b376 >= 1 e1772: b341 + b367 >= 1 e1773: b341 + b366 + b374 >= 1 e1774: b341 + b366 + b371 + b375 >= 1 e1775: b341 + b366 + b369 >= 1 e1776: b341 + b365 + b376 >= 1 e1777: b341 + b365 + b371 >= 1 e1778: b341 + b364 >= 1 e1779: b341 + b363 + b373 >= 1 e1780: b341 + b363 + b370 + b374 >= 1 e1781: b341 + b363 + b369 + b376 >= 1 e1782: b341 + b363 + b368 >= 1 e1783: b341 + b363 + b366 + b374 >= 1 e1784: b341 + b363 + b366 + b371 + b375 >= 1 e1785: b341 + b363 + b366 + b370 + b376 >= 1 e1786: b341 + b363 + b366 + b369 >= 1 e1787: b341 + b363 + b365 >= 1 e1788: b341 + b362 + b373 >= 1 e1789: b341 + b362 + b371 + b374 >= 1 e1790: b341 + b362 + b370 + b375 >= 1 e1791: b341 + b362 + b369 + b376 >= 1 e1792: b341 + b362 + b368 >= 1 e1793: b341 + b362 + b366 + b375 >= 1 e1794: b341 + b362 + b366 + b371 + b376 >= 1 e1795: b341 + b362 + b366 + b370 >= 1 e1796: b341 + b362 + b365 >= 1 e1797: b341 + b361 + b374 >= 1 e1798: b341 + b361 + b371 + b375 >= 1 e1799: b341 + b361 + b370 + b376 >= 1 e1800: b341 + b361 + b369 >= 1 e1801: b341 + b361 + b366 + b376 >= 1 e1802: b341 + b361 + b366 + b371 >= 1 e1803: b341 + b361 + b365 >= 1 e1804: b341 + b360 + b375 >= 1 e1805: b341 + b360 + b371 + b376 >= 1 e1806: b341 + b360 + b370 >= 1 e1807: b341 + b360 + b366 >= 1 e1808: b341 + b359 + b376 >= 1 e1809: b341 + b359 + b371 >= 1 e1810: b341 + b359 + b366 >= 1 e1811: b341 + b357 + b373 >= 1 e1812: b341 + b357 + b370 + b374 >= 1 e1813: b341 + b357 + b369 + b375 >= 1 e1814: b341 + b357 + b368 >= 1 e1815: b341 + b357 + b366 + b374 >= 1 e1816: b341 + b357 + b366 + b371 + b375 >= 1 e1817: b341 + b357 + b366 + b370 + b376 >= 1 e1818: b341 + b357 + b366 + b369 >= 1 e1819: b341 + b357 + b365 >= 1 e1820: b341 + b357 + b363 + b373 >= 1 e1821: b341 + b357 + b363 + b371 + b374 >= 1 e1822: b341 + b357 + b363 + b370 + b375 >= 1 e1823: b341 + b357 + b363 + b369 + b376 >= 1 e1824: b341 + b357 + b363 + b368 >= 1 e1825: b341 + b357 + b363 + b366 + b375 >= 1 e1826: b341 + b357 + b363 + b366 + b371 + b376 >= 1 e1827: b341 + b357 + b363 + b366 + b370 >= 1 e1828: b341 + b357 + b363 + b365 >= 1 e1829: b341 + b357 + b362 + b374 >= 1 e1830: b341 + b357 + b362 + b371 + b375 >= 1 e1831: b341 + b357 + b362 + b370 + b376 >= 1 e1832: b341 + b357 + b362 + b369 >= 1 e1833: b341 + b357 + b362 + b366 + b376 >= 1 e1834: b341 + b357 + b362 + b366 + b371 >= 1 e1835: b341 + b357 + b362 + b365 >= 1 e1836: b341 + b357 + b361 + b375 >= 1 e1837: b341 + b357 + b361 + b371 + b376 >= 1 e1838: b341 + b357 + b361 + b370 >= 1 e1839: b341 + b357 + b361 + b366 >= 1 e1840: b341 + b357 + b360 + b376 >= 1 e1841: b341 + b357 + b360 + b371 >= 1 e1842: b341 + b357 + b360 + b366 >= 1 e1843: b341 + b357 + b359 + b376 >= 1 e1844: b341 + b357 + b359 + b371 >= 1 e1845: b341 + b357 + b359 + b366 >= 1 e1846: b341 + b356 + b373 >= 1 e1847: b341 + b356 + b371 + b374 >= 1 e1848: b341 + b356 + b370 + b375 >= 1 e1849: b341 + b356 + b369 + b376 >= 1 e1850: b341 + b356 + b368 >= 1 e1851: b341 + b356 + b366 + b375 >= 1 e1852: b341 + b356 + b366 + b371 + b376 >= 1 e1853: b341 + b356 + b366 + b370 >= 1 e1854: b341 + b356 + b365 >= 1 e1855: b341 + b356 + b363 + b374 >= 1 e1856: b341 + b356 + b363 + b371 + b375 >= 1 e1857: b341 + b356 + b363 + b370 + b376 >= 1 e1858: b341 + b356 + b363 + b369 >= 1 e1859: b341 + b356 + b363 + b366 + b376 >= 1 e1860: b341 + b356 + b363 + b366 + b371 >= 1 e1861: b341 + b356 + b363 + b365 >= 1 e1862: b341 + b356 + b362 + b375 >= 1 e1863: b341 + b356 + b362 + b371 + b376 >= 1 e1864: b341 + b356 + b362 + b370 >= 1 e1865: b341 + b356 + b362 + b366 >= 1 e1866: b341 + b356 + b361 + b376 >= 1 e1867: b341 + b356 + b361 + b371 >= 1 e1868: b341 + b356 + b361 + b366 >= 1 e1869: b341 + b356 + b360 + b376 >= 1 e1870: b341 + b356 + b360 + b371 >= 1 e1871: b341 + b356 + b360 + b366 >= 1 e1872: b341 + b355 + b374 >= 1 e1873: b341 + b355 + b371 + b375 >= 1 e1874: b341 + b355 + b370 + b376 >= 1 e1875: b341 + b355 + b369 >= 1 e1876: b341 + b355 + b366 + b376 >= 1 e1877: b341 + b355 + b366 + b371 >= 1 e1878: b341 + b355 + b365 >= 1 e1879: b341 + b355 + b363 + b375 >= 1 e1880: b341 + b355 + b363 + b371 + b376 >= 1 e1881: b341 + b355 + b363 + b370 >= 1 e1882: b341 + b355 + b363 + b366 >= 1 e1883: b341 + b355 + b362 + b376 >= 1 e1884: b341 + b355 + b362 + b371 >= 1 e1885: b341 + b355 + b362 + b366 >= 1 e1886: b341 + b355 + b361 + b376 >= 1 e1887: b341 + b355 + b361 + b371 >= 1 e1888: b341 + b355 + b361 + b366 >= 1 e1889: b341 + b354 + b375 >= 1 e1890: b341 + b354 + b371 + b376 >= 1 e1891: b341 + b354 + b370 >= 1 e1892: b341 + b354 + b366 >= 1 e1893: b341 + b354 + b363 + b376 >= 1 e1894: b341 + b354 + b363 + b371 >= 1 e1895: b341 + b354 + b363 + b366 >= 1 e1896: b341 + b354 + b362 + b376 >= 1 e1897: b341 + b354 + b362 + b371 >= 1 e1898: b341 + b354 + b362 + b366 >= 1 e1899: b341 + b353 + b376 >= 1 e1900: b341 + b353 + b371 >= 1 e1901: b341 + b353 + b366 >= 1 e1902: b341 + b351 + b373 >= 1 e1903: b341 + b351 + b371 + b374 >= 1 e1904: b341 + b351 + b370 + b375 >= 1 e1905: b341 + b351 + b369 + b376 >= 1 e1906: b341 + b351 + b368 >= 1 e1907: b341 + b351 + b366 + b375 >= 1 e1908: b341 + b351 + b366 + b371 + b376 >= 1 e1909: b341 + b351 + b366 + b370 >= 1 e1910: b341 + b351 + b365 >= 1 e1911: b341 + b351 + b363 + b374 >= 1 e1912: b341 + b351 + b363 + b371 + b375 >= 1 e1913: b341 + b351 + b363 + b370 + b376 >= 1 e1914: b341 + b351 + b363 + b369 >= 1 e1915: b341 + b351 + b363 + b366 + b376 >= 1 e1916: b341 + b351 + b363 + b366 + b371 >= 1 e1917: b341 + b351 + b363 + b365 >= 1 e1918: b341 + b351 + b362 + b374 >= 1 e1919: b341 + b351 + b362 + b371 + b375 >= 1 e1920: b341 + b351 + b362 + b370 + b376 >= 1 e1921: b341 + b351 + b362 + b369 >= 1 e1922: b341 + b351 + b362 + b366 + b376 >= 1 e1923: b341 + b351 + b362 + b366 + b371 >= 1 e1924: b341 + b351 + b362 + b365 >= 1 e1925: b341 + b351 + b361 + b375 >= 1 e1926: b341 + b351 + b361 + b371 + b376 >= 1 e1927: b341 + b351 + b361 + b370 >= 1 e1928: b341 + b351 + b361 + b366 >= 1 e1929: b341 + b351 + b360 + b376 >= 1 e1930: b341 + b351 + b360 + b371 >= 1 e1931: b341 + b351 + b360 + b366 >= 1 e1932: b341 + b351 + b357 + b374 >= 1 e1933: b341 + b351 + b357 + b371 + b375 >= 1 e1934: b341 + b351 + b357 + b370 + b376 >= 1 e1935: b341 + b351 + b357 + b369 >= 1 e1936: b341 + b351 + b357 + b366 + b376 >= 1 e1937: b341 + b351 + b357 + b366 + b371 >= 1 e1938: b341 + b351 + b357 + b365 >= 1 e1939: b341 + b351 + b357 + b363 + b374 >= 1 e1940: b341 + b351 + b357 + b363 + b371 + b375 >= 1 e1941: b341 + b351 + b357 + b363 + b370 >= 1 e1942: b341 + b351 + b357 + b363 + b366 >= 1 e1943: b341 + b351 + b357 + b362 + b375 >= 1 e1944: b341 + b351 + b357 + b362 + b371 + b376 >= 1 e1945: b341 + b351 + b357 + b362 + b370 >= 1 e1946: b341 + b351 + b357 + b362 + b366 >= 1 e1947: b341 + b351 + b357 + b361 + b376 >= 1 e1948: b341 + b351 + b357 + b361 + b371 >= 1 e1949: b341 + b351 + b357 + b361 + b366 >= 1 e1950: b341 + b351 + b356 + b374 >= 1 e1951: b341 + b351 + b356 + b371 + b375 >= 1 e1952: b341 + b351 + b356 + b370 + b376 >= 1 e1953: b341 + b351 + b356 + b369 >= 1 e1954: b341 + b351 + b356 + b366 + b376 >= 1 e1955: b341 + b351 + b356 + b366 + b371 >= 1 e1956: b341 + b351 + b356 + b365 >= 1 e1957: b341 + b351 + b356 + b363 + b375 >= 1 e1958: b341 + b351 + b356 + b363 + b371 + b376 >= 1 e1959: b341 + b351 + b356 + b363 + b370 >= 1 e1960: b341 + b351 + b356 + b363 + b366 >= 1 e1961: b341 + b351 + b356 + b362 + b376 >= 1 e1962: b341 + b351 + b356 + b362 + b371 >= 1 e1963: b341 + b351 + b356 + b362 + b366 >= 1 e1964: b341 + b351 + b355 + b375 >= 1 e1965: b341 + b351 + b355 + b371 + b376 >= 1 e1966: b341 + b351 + b355 + b370 >= 1 e1967: b341 + b351 + b355 + b366 >= 1 e1968: b341 + b351 + b355 + b363 + b376 >= 1 e1969: b341 + b351 + b355 + b363 + b371 >= 1 e1970: b341 + b351 + b355 + b363 + b366 >= 1 e1971: b341 + b351 + b354 + b376 >= 1 e1972: b341 + b351 + b354 + b371 >= 1 e1973: b341 + b351 + b354 + b366 >= 1 e1974: b341 + b350 + b374 >= 1 e1975: b341 + b350 + b371 + b375 >= 1 e1976: b341 + b350 + b370 + b376 >= 1 e1977: b341 + b350 + b369 >= 1 e1978: b341 + b350 + b366 + b376 >= 1 e1979: b341 + b350 + b366 + b371 >= 1 e1980: b341 + b350 + b365 >= 1 e1981: b341 + b350 + b363 + b375 >= 1 e1982: b341 + b350 + b363 + b371 + b376 >= 1 e1983: b341 + b350 + b363 + b370 >= 1 e1984: b341 + b350 + b363 + b366 >= 1 e1985: b341 + b350 + b362 + b376 >= 1 e1986: b341 + b350 + b362 + b371 >= 1 e1987: b341 + b350 + b362 + b366 >= 1 e1988: b341 + b350 + b357 + b375 >= 1 e1989: b341 + b350 + b357 + b371 + b376 >= 1 e1990: b341 + b350 + b357 + b370 >= 1 e1991: b341 + b350 + b357 + b366 >= 1 e1992: b341 + b350 + b357 + b363 + b376 >= 1 e1993: b341 + b350 + b357 + b363 + b371 >= 1 e1994: b341 + b350 + b357 + b363 + b366 >= 1 e1995: b341 + b350 + b356 + b376 >= 1 e1996: b341 + b350 + b356 + b371 >= 1 e1997: b341 + b350 + b356 + b366 >= 1 e1998: b341 + b349 + b376 >= 1 e1999: b341 + b349 + b371 >= 1 e2000: b341 + b349 + b366 >= 1 e2001: b341 + b349 + b357 + b376 >= 1 e2002: b341 + b349 + b357 + b371 >= 1 e2003: b341 + b349 + b357 + b366 >= 1 e2004: b341 + b347 + b374 >= 1 e2005: b341 + b347 + b370 + b375 >= 1 e2006: b341 + b347 + b369 >= 1 e2007: b341 + b347 + b366 + b375 >= 1 e2008: b341 + b347 + b366 + b371 + b376 >= 1 e2009: b341 + b347 + b366 + b370 >= 1 e2010: b341 + b347 + b365 >= 1 e2011: b341 + b347 + b363 + b374 >= 1 e2012: b341 + b347 + b363 + b371 + b375 >= 1 e2013: b341 + b347 + b363 + b370 + b376 >= 1 e2014: b341 + b347 + b363 + b369 >= 1 e2015: b341 + b347 + b363 + b366 + b376 >= 1 e2016: b341 + b347 + b363 + b366 + b371 >= 1 e2017: b341 + b347 + b363 + b365 >= 1 e2018: b341 + b347 + b362 + b375 >= 1 e2019: b341 + b347 + b362 + b371 + b376 >= 1 e2020: b341 + b347 + b362 + b370 >= 1 e2021: b341 + b347 + b362 + b366 >= 1 e2022: b341 + b347 + b361 + b376 >= 1 e2023: b341 + b347 + b361 + b371 >= 1 e2024: b341 + b347 + b361 + b366 >= 1 e2025: b341 + b347 + b357 + b374 >= 1 e2026: b341 + b347 + b357 + b371 + b375 >= 1 e2027: b341 + b347 + b357 + b370 + b376 >= 1 e2028: b341 + b347 + b357 + b369 >= 1 e2029: b341 + b347 + b357 + b366 + b376 >= 1 e2030: b341 + b347 + b357 + b366 + b371 >= 1 e2031: b341 + b347 + b357 + b365 >= 1 e2032: b341 + b347 + b357 + b363 + b375 >= 1 e2033: b341 + b347 + b357 + b363 + b371 + b376 >= 1 e2034: b341 + b347 + b357 + b363 + b370 >= 1 e2035: b341 + b347 + b357 + b363 + b366 >= 1 e2036: b341 + b347 + b357 + b362 + b376 >= 1 e2037: b341 + b347 + b357 + b362 + b371 >= 1 e2038: b341 + b347 + b357 + b362 + b366 >= 1 e2039: b341 + b347 + b356 + b375 >= 1 e2040: b341 + b347 + b356 + b371 + b376 >= 1 e2041: b341 + b347 + b356 + b370 >= 1 e2042: b341 + b347 + b356 + b366 >= 1 e2043: b341 + b347 + b356 + b363 + b376 >= 1 e2044: b341 + b347 + b356 + b363 + b371 >= 1 e2045: b341 + b347 + b356 + b363 + b366 >= 1 e2046: b341 + b347 + b355 + b376 >= 1 e2047: b341 + b347 + b355 + b371 >= 1 e2048: b341 + b347 + b355 + b366 >= 1 e2049: b341 + b347 + b351 + b375 >= 1 e2050: b341 + b347 + b351 + b371 + b376 >= 1 e2051: b341 + b347 + b351 + b370 >= 1 e2052: b341 + b347 + b351 + b366 >= 1 e2053: b341 + b347 + b351 + b363 + b376 >= 1 e2054: b341 + b347 + b351 + b363 + b371 >= 1 e2055: b341 + b347 + b351 + b363 + b366 >= 1 e2056: b341 + b347 + b351 + b362 + b376 >= 1 e2057: b341 + b347 + b351 + b362 + b371 >= 1 e2058: b341 + b347 + b351 + b362 + b366 >= 1 e2059: b341 + b347 + b351 + b357 + b376 >= 1 e2060: b341 + b347 + b351 + b357 + b371 >= 1 e2061: b341 + b347 + b351 + b357 + b366 >= 1 e2062: b341 + b347 + b351 + b357 + b363 + b376 >= 1 e2063: b341 + b347 + b351 + b357 + b363 + b371 >= 1 e2064: b341 + b347 + b351 + b357 + b363 + b366 >= 1 e2065: b341 + b347 + b351 + b356 + b376 >= 1 e2066: b341 + b347 + b351 + b356 + b371 >= 1 e2067: b341 + b347 + b351 + b356 + b366 >= 1 e2068: b341 + b347 + b350 + b376 >= 1 e2069: b341 + b347 + b350 + b371 >= 1 e2070: b341 + b347 + b350 + b366 >= 1 e2071: b341 + b346 + b376 >= 1 e2072: b341 + b346 + b371 >= 1 e2073: b341 + b346 + b366 >= 1 e2074: b341 + b344 + b374 >= 1 e2075: b341 + b344 + b371 + b375 >= 1 e2076: b341 + b344 + b370 + b376 >= 1 e2077: b341 + b344 + b369 >= 1 e2078: b341 + b344 + b366 + b376 >= 1 e2079: b341 + b344 + b366 + b371 >= 1 e2080: b341 + b344 + b365 >= 1 e2081: b341 + b344 + b363 + b375 >= 1 e2082: b341 + b344 + b363 + b371 + b376 >= 1 e2083: b341 + b344 + b363 + b370 >= 1 e2084: b341 + b344 + b363 + b366 >= 1 e2085: b341 + b344 + b362 + b375 >= 1 e2086: b341 + b344 + b362 + b371 + b376 >= 1 e2087: b341 + b344 + b362 + b370 >= 1 e2088: b341 + b344 + b362 + b366 >= 1 e2089: b341 + b344 + b361 + b376 >= 1 e2090: b341 + b344 + b361 + b371 >= 1 e2091: b341 + b344 + b361 + b366 >= 1 e2092: b341 + b344 + b357 + b375 >= 1 e2093: b341 + b344 + b357 + b371 + b376 >= 1 e2094: b341 + b344 + b357 + b370 >= 1 e2095: b341 + b344 + b357 + b366 >= 1 e2096: b341 + b344 + b357 + b363 + b375 >= 1 e2097: b341 + b344 + b357 + b363 + b371 + b376 >= 1 e2098: b341 + b344 + b357 + b363 + b370 >= 1 e2099: b341 + b344 + b357 + b363 + b366 >= 1 e2100: b341 + b344 + b357 + b362 + b376 >= 1 e2101: b341 + b344 + b357 + b362 + b371 >= 1 e2102: b341 + b344 + b357 + b362 + b366 >= 1 e2103: b341 + b344 + b356 + b375 >= 1 e2104: b341 + b344 + b356 + b371 + b376 >= 1 e2105: b341 + b344 + b356 + b370 >= 1 e2106: b341 + b344 + b356 + b366 >= 1 e2107: b341 + b344 + b356 + b363 + b376 >= 1 e2108: b341 + b344 + b356 + b363 + b371 >= 1 e2109: b341 + b344 + b356 + b363 + b366 >= 1 e2110: b341 + b344 + b355 + b376 >= 1 e2111: b341 + b344 + b355 + b371 >= 1 e2112: b341 + b344 + b355 + b366 >= 1 e2113: b341 + b344 + b351 + b375 >= 1 e2114: b341 + b344 + b351 + b371 + b376 >= 1 e2115: b341 + b344 + b351 + b370 >= 1 e2116: b341 + b344 + b351 + b366 >= 1 e2117: b341 + b344 + b351 + b363 + b376 >= 1 e2118: b341 + b344 + b351 + b363 + b371 >= 1 e2119: b341 + b344 + b351 + b363 + b366 >= 1 e2120: b341 + b344 + b351 + b362 + b376 >= 1 e2121: b341 + b344 + b351 + b362 + b371 >= 1 e2122: b341 + b344 + b351 + b362 + b366 >= 1 e2123: b341 + b344 + b351 + b357 + b376 >= 1 e2124: b341 + b344 + b351 + b357 + b371 >= 1 e2125: b341 + b344 + b351 + b357 + b366 >= 1 e2126: b341 + b344 + b350 + b376 >= 1 e2127: b341 + b344 + b350 + b371 >= 1 e2128: b341 + b344 + b350 + b366 >= 1 e2129: b341 + b344 + b347 + b376 >= 1 e2130: b341 + b344 + b347 + b371 >= 1 e2131: b341 + b344 + b347 + b366 >= 1 e2132: b341 + b344 + b347 + b363 + b376 >= 1 e2133: b341 + b344 + b347 + b363 + b371 >= 1 e2134: b341 + b344 + b347 + b363 + b366 >= 1 e2135: b341 + b344 + b347 + b357 + b376 >= 1 e2136: b341 + b344 + b347 + b357 + b371 >= 1 e2137: b341 + b344 + b347 + b357 + b366 >= 1 e2138: b341 + b343 + b376 >= 1 e2139: b341 + b343 + b371 >= 1 e2140: b341 + b343 + b366 >= 1 e2141: b340 + b374 >= 1 e2142: b340 + b371 + b375 >= 1 e2143: b340 + b370 + b376 >= 1 e2144: b340 + b369 >= 1 e2145: b340 + b366 + b376 >= 1 e2146: b340 + b366 + b371 >= 1 e2147: b340 + b365 >= 1 e2148: b340 + b363 + b375 >= 1 e2149: b340 + b363 + b371 + b376 >= 1 e2150: b340 + b363 + b370 >= 1 e2151: b340 + b363 + b366 >= 1 e2152: b340 + b362 + b375 >= 1 e2153: b340 + b362 + b371 + b376 >= 1 e2154: b340 + b362 + b370 >= 1 e2155: b340 + b362 + b366 >= 1 e2156: b340 + b361 + b376 >= 1 e2157: b340 + b361 + b371 >= 1 e2158: b340 + b361 + b366 >= 1 e2159: b340 + b357 + b375 >= 1 e2160: b340 + b357 + b370 >= 1 e2161: b340 + b357 + b366 >= 1 e2162: b340 + b357 + b363 + b375 >= 1 e2163: b340 + b357 + b363 + b371 + b376 >= 1 e2164: b340 + b357 + b363 + b370 >= 1 e2165: b340 + b357 + b363 + b366 >= 1 e2166: b340 + b357 + b362 + b376 >= 1 e2167: b340 + b357 + b362 + b371 >= 1 e2168: b340 + b357 + b362 + b366 >= 1 e2169: b340 + b356 + b375 >= 1 e2170: b340 + b356 + b371 + b376 >= 1 e2171: b340 + b356 + b370 >= 1 e2172: b340 + b356 + b366 >= 1 e2173: b340 + b356 + b363 + b376 >= 1 e2174: b340 + b356 + b363 + b371 >= 1 e2175: b340 + b356 + b363 + b366 >= 1 e2176: b340 + b355 + b376 >= 1 e2177: b340 + b355 + b371 >= 1 e2178: b340 + b355 + b366 >= 1 e2179: b340 + b351 + b375 >= 1 e2180: b340 + b351 + b371 + b376 >= 1 e2181: b340 + b351 + b370 >= 1 e2182: b340 + b351 + b366 >= 1 e2183: b340 + b351 + b363 + b376 >= 1 e2184: b340 + b351 + b363 + b371 >= 1 e2185: b340 + b351 + b363 + b366 >= 1 e2186: b340 + b351 + b357 + b376 >= 1 e2187: b340 + b351 + b357 + b371 >= 1 e2188: b340 + b351 + b357 + b366 >= 1 e2189: b340 + b350 + b376 >= 1 e2190: b340 + b350 + b371 >= 1 e2191: b340 + b350 + b366 >= 1 e2192: b340 + b347 + b376 >= 1 e2193: b340 + b347 + b371 >= 1 e2194: b340 + b347 + b366 >= 1 e2195: b340 + b344 + b376 >= 1 e2196: b340 + b344 + b371 >= 1 e2197: b340 + b344 + b366 >= 1 e2198: b339 + b376 >= 1 e2199: b339 + b371 >= 1 e2200: b339 + b366 >= 1 e2201: x61 - 1.34666666666667 b339 >= 0 e2202: x61 - 1.92 b340 >= 0 e2203: x61 - 2.02 b341 >= 0 e2204: x62 - 2.67333333333333 b342 >= 0 e2205: x62 - 3.82 b343 >= 0 e2206: x62 - 4.01333333333333 b344 >= 0 e2207: x63 - 3.17333333333333 b345 >= 0 e2208: x63 - 4.53333333333333 b346 >= 0 e2209: x63 - 4.76 b347 >= 0 e2210: x64 - 3.97333333333333 b348 >= 0 e2211: x64 - 5.39333333333333 b349 >= 0 e2212: x64 - 5.68 b350 >= 0 e2213: x64 - 5.96 b351 >= 0 e2214: x65 - 26.7866666666667 b352 >= 0 e2215: x65 - 34.44 b353 >= 0 e2216: x65 - 36.3533333333333 b354 >= 0 e2217: x65 - 38.2666666666667 b355 >= 0 e2218: x65 - 40.18 b356 >= 0 e2219: x65 - 42.0933333333333 b357 >= 0 e2220: x66 - 63.18 b358 >= 0 e2221: x66 - 81.2333333333333 b359 >= 0 e2222: x66 - 85.7466666666667 b360 >= 0 e2223: x66 - 90.2533333333333 b361 >= 0 e2224: x66 - 94.7666666666667 b362 >= 0 e2225: x66 - 99.28 b363 >= 0 e2226: x67 - 4.39333333333333 b364 >= 0 e2227: x67 - 6.28 b365 >= 0 e2228: x67 - 6.59333333333333 b366 >= 0 e2229: x68 - 39.3733333333333 b367 >= 0 e2230: x68 - 53.4333333333333 b368 >= 0 e2231: x68 - 56.24 b369 >= 0 e2232: x68 - 59.0533333333333 b370 >= 0 e2233: x68 - 61.8666666666667 b371 >= 0 e2234: x69 - 35.82 b372 >= 0 e2235: x69 - 48.6133333333333 b373 >= 0 e2236: x69 - 51.1733333333333 b374 >= 0 e2237: x69 - 53.7333333333333 b375 >= 0 e2238: x69 - 56.2866666666667 b376 >= 0 e2239: x70 - 26.4066666666667 b377 >= 0 e2240: x70 - 33.9533333333333 b378 >= 0 e2241: x70 - 35.84 b379 >= 0 e2242: x70 - 37.7266666666667 b380 >= 0 e2243: x70 - 39.6133333333333 b381 >= 0 e2244: x70 - 41.5 b382 >= 0 e2245: x71 - 39.7666666666667 b383 >= 0 e2246: x71 - 53.9666666666667 b384 >= 0 e2247: x71 - 56.8066666666667 b385 >= 0 e2248: x71 - 59.6466666666667 b386 >= 0 e2249: x71 - 62.4933333333333 b387 >= 0 e2250: x72 - 53.94 b388 >= 0 e2251: x72 - 77.0533333333333 b389 >= 0 e2252: x72 - 80.9066666666667 b390 >= 0 e2253: x73 - 17.4333333333333 b391 >= 0 e2254: x73 - 24.9066666666667 b392 >= 0 e2255: x73 - 26.1466666666667 b393 >= 0 e2256: x74 - 25.3333333333333 b394 >= 0 e2257: x74 - 36.1866666666667 b395 >= 0 e2258: x74 - 38 b396 >= 0 e2259: x75 - 41.4933333333333 b397 >= 0 e2260: x75 - 56.3133333333333 b398 >= 0 e2261: x75 - 59.2733333333333 b399 >= 0 e2262: x75 - 62.24 b400 >= 0 e2263: - x136 + x279 <= 0 e2264: - x136 + x280 <= 0 e2265: - x136 + x281 <= 0 e2266: - x136 + x282 <= 0 e2267: - x137 + x283 <= 0 e2268: - x137 + x284 <= 0 e2269: - x137 + x285 <= 0 e2270: - x137 + x286 <= 0 e2271: - x138 + x287 <= 0 e2272: - x138 + x288 <= 0 e2273: - x138 + x289 <= 0 e2274: - x138 + x290 <= 0 e2275: - x139 + x291 <= 0 e2276: - x139 + x292 <= 0 e2277: - x139 + x293 <= 0 e2278: - x139 + x294 <= 0 e2279: - x140 + x295 <= 0 e2280: - x140 + x296 <= 0 e2281: - x140 + x297 <= 0 e2282: - x140 + x298 <= 0 e2283: - x141 + x299 <= 0 e2284: - x141 + x300 <= 0 e2285: - x141 + x301 <= 0 e2286: - x141 + x302 <= 0 e2287: - x142 + x303 <= 0 e2288: - x142 + x304 <= 0 e2289: - x142 + x305 <= 0 e2290: - x142 + x306 <= 0 e2291: - x143 + x307 <= 0 e2292: - x143 + x308 <= 0 e2293: - x143 + x309 <= 0 e2294: - x143 + x310 <= 0 e2295: - x144 + x311 <= 0 e2296: - x144 + x312 <= 0 e2297: - x144 + x313 <= 0 e2298: - x144 + x314 <= 0 e2299: - x145 + x315 <= 0 e2300: - x145 + x316 <= 0 e2301: - x145 + x317 <= 0 e2302: - x145 + x318 <= 0 e2303: - x146 + x319 <= 0 e2304: - x146 + x320 <= 0 e2305: - x146 + x321 <= 0 e2306: - x146 + x322 <= 0 e2307: - x147 + x323 <= 0 e2308: - x147 + x324 <= 0 e2309: - x147 + x325 <= 0 e2310: - x147 + x326 <= 0 e2311: - x148 + x327 <= 0 e2312: - x148 + x328 <= 0 e2313: - x148 + x329 <= 0 e2314: - x148 + x330 <= 0 e2315: - x149 + x331 <= 0 e2316: - x149 + x332 <= 0 e2317: - x149 + x333 <= 0 e2318: - x149 + x334 <= 0 e2319: - x150 + x335 <= 0 e2320: - x150 + x336 <= 0 e2321: - x150 + x337 <= 0 e2322: - x150 + x338 <= 0 e2323: b339 - b340 >= 0 e2324: b340 - b341 >= 0 e2325: b342 - b343 >= 0 e2326: b343 - b344 >= 0 e2327: b345 - b346 >= 0 e2328: b346 - b347 >= 0 e2329: b348 - b349 >= 0 e2330: b349 - b350 >= 0 e2331: b350 - b351 >= 0 e2332: b352 - b353 >= 0 e2333: b353 - b354 >= 0 e2334: b354 - b355 >= 0 e2335: b355 - b356 >= 0 e2336: b356 - b357 >= 0 e2337: b358 - b359 >= 0 e2338: b359 - b360 >= 0 e2339: b360 - b361 >= 0 e2340: b361 - b362 >= 0 e2341: b362 - b363 >= 0 e2342: b364 - b365 >= 0 e2343: b365 - b366 >= 0 e2344: b367 - b368 >= 0 e2345: b368 - b369 >= 0 e2346: b369 - b370 >= 0 e2347: b370 - b371 >= 0 e2348: b372 - b373 >= 0 e2349: b373 - b374 >= 0 e2350: b374 - b375 >= 0 e2351: b375 - b376 >= 0 e2352: b377 - b378 >= 0 e2353: b378 - b379 >= 0 e2354: b379 - b380 >= 0 e2355: b380 - b381 >= 0 e2356: b381 - b382 >= 0 e2357: b383 - b384 >= 0 e2358: b384 - b385 >= 0 e2359: b385 - b386 >= 0 e2360: b386 - b387 >= 0 e2361: b388 - b389 >= 0 e2362: b389 - b390 >= 0 e2363: b391 - b392 >= 0 e2364: b392 - b393 >= 0 e2365: b394 - b395 >= 0 e2366: b395 - b396 >= 0 e2367: b397 - b398 >= 0 e2368: b398 - b399 >= 0 e2369: b399 - b400 >= 0 e2370: x155 - x156 >= 0 e2371: x156 - x157 >= 0 e2372: x157 - x158 >= 0 Bounds x1 <= .26351883 x2 <= .26351883 x3 <= .26351883 x4 <= .26351883 x5 <= .22891574 x6 <= .22891574 x7 <= .22891574 x8 <= .22891574 x9 <= .21464835 x10 <= .21464835 x11 <= .21464835 x12 <= .21464835 x13 <= .17964414 x14 <= .17964414 x15 <= .17964414 x16 <= .17964414 x17 <= .17402843 x18 <= .17402843 x19 <= .17402843 x20 <= .17402843 x21 <= .15355962 x22 <= .15355962 x23 <= .15355962 x24 <= .15355962 x25 <= .1942283 x26 <= .1942283 x27 <= .1942283 x28 <= .1942283 x29 <= .25670555 x30 <= .25670555 x31 <= .25670555 x32 <= .25670555 x33 <= .27088619 x34 <= .27088619 x35 <= .27088619 x36 <= .27088619 x37 <= .28985675 x38 <= .28985675 x39 <= .28985675 x40 <= .28985675 x41 <= .25550303 x42 <= .25550303 x43 <= .25550303 x44 <= .25550303 x45 <= .19001726 x46 <= .19001726 x47 <= .19001726 x48 <= .19001726 x49 <= .23803143 x50 <= .23803143 x51 <= .23803143 x52 <= .23803143 x53 <= .23312962 x54 <= .23312962 x55 <= .23312962 x56 <= .23312962 x57 <= .27705307 x58 <= .27705307 x59 <= .27705307 x60 <= .27705307 1.24666666666667 <= x61 <= 2.02 2.48 <= x62 <= 4.01333333333333 2.94666666666667 <= x63 <= 4.76 3.69333333333333 <= x64 <= 5.96 24.8733333333333 <= x65 <= 42.0933333333333 58.6666666666667 <= x66 <= 99.28 4.08 <= x67 <= 6.59333333333333 36.56 <= x68 <= 61.8666666666667 33.26 <= x69 <= 56.2866666666667 24.52 <= x70 <= 41.5 36.9266666666667 <= x71 <= 62.4933333333333 50.0866666666667 <= x72 <= 80.9066666666667 16.1866666666667 <= x73 <= 26.1466666666667 23.52 <= x74 <= 38 38.5266666666667 <= x75 <= 62.24 x136 <= .5323080366 x137 <= .918715169866666 x138 <= 1.021726146 x139 <= 1.0706790744 x140 <= 7.32543671346667 x141 <= 15.2453990736 x142 <= 1.28061192466667 x143 <= 15.8815166933333 x144 <= 15.2472806811333 x145 <= 12.029055125 x146 <= 15.9672360214667 x147 <= 15.3736631157333 x148 <= 6.2237284564 x149 <= 8.85892556 x150 <= 17.2437830768 .25788969 <= x151 <= .35227087 .25788969 <= x152 <= .35227087 .25788969 <= x153 <= .35227087 .25788969 <= x154 <= .35227087 -.98493628 <= x155 <= -.7794471 -.98493628 <= x156 <= -.7794471 -.98493628 <= x157 <= -.7794471 -.98493628 <= x158 <= -.7794471 x159 <= 5.80296499999999e-2 x160 <= 5.80296499999999e-2 x161 <= 5.80296499999999e-2 x162 <= 5.80296499999999e-2 x163 <= 5.46689399999999e-2 x164 <= 5.46689399999999e-2 x165 <= 5.46689399999999e-2 x166 <= 5.46689399999999e-2 x167 <= 9.360565e-2 x168 <= 9.360565e-2 x169 <= 9.360565e-2 x170 <= 9.360565e-2 x171 <= 4.76880399999999e-2 x172 <= 4.76880399999999e-2 x173 <= 4.76880399999999e-2 x174 <= 4.76880399999999e-2 x175 <= 5.276021e-2 x176 <= 5.276021e-2 x177 <= 5.276021e-2 x178 <= 5.276021e-2 x179 <= 4.905388e-2 x180 <= 4.905388e-2 x181 <= 4.905388e-2 x182 <= 4.905388e-2 x183 <= 7.731692e-2 x184 <= 7.731692e-2 x185 <= 7.731692e-2 x186 <= 7.731692e-2 x187 <= 8.211741e-2 x188 <= 8.211741e-2 x189 <= 8.211741e-2 x190 <= 8.211741e-2 x191 <= 9.438118e-2 x192 <= 9.438118e-2 x193 <= 9.438118e-2 x194 <= 9.438118e-2 x195 <= 8.436757e-2 x196 <= 8.436757e-2 x197 <= 8.436757e-2 x198 <= 8.436757e-2 x199 <= 6.987597e-2 x200 <= 6.987597e-2 x201 <= 6.987597e-2 x202 <= 6.987597e-2 x203 <= 4.788831e-2 x204 <= 4.788831e-2 x205 <= 4.788831e-2 x206 <= 4.788831e-2 x207 <= 6.68875099999999e-2 x208 <= 6.68875099999999e-2 x209 <= 6.68875099999999e-2 x210 <= 6.68875099999999e-2 x211 <= 7.276512e-2 x212 <= 7.276512e-2 x213 <= 7.276512e-2 x214 <= 7.276512e-2 x215 <= 9.438118e-2 x216 <= 9.438118e-2 x217 <= 9.438118e-2 x218 <= 9.438118e-2 x219 <= .20548918 x220 <= .20548918 x221 <= .20548918 x222 <= .20548918 x223 <= .1742468 x224 <= .1742468 x225 <= .1742468 x226 <= .1742468 x227 <= .1210427 x228 <= .1210427 x229 <= .1210427 x230 <= .1210427 x231 <= .1319561 x232 <= .1319561 x233 <= .1319561 x234 <= .1319561 x235 <= .12126822 x236 <= .12126822 x237 <= .12126822 x238 <= .12126822 x239 <= .10450574 x240 <= .10450574 x241 <= .10450574 x242 <= .10450574 x243 <= .11691138 x244 <= .11691138 x245 <= .11691138 x246 <= .11691138 x247 <= .17458814 x248 <= .17458814 x249 <= .17458814 x250 <= .17458814 x251 <= .17650501 x252 <= .17650501 x253 <= .17650501 x254 <= .17650501 x255 <= .20548918 x256 <= .20548918 x257 <= .20548918 x258 <= .20548918 x259 <= .18562706 x260 <= .18562706 x261 <= .18562706 x262 <= .18562706 x263 <= .14212895 x264 <= .14212895 x265 <= .14212895 x266 <= .14212895 x267 <= .17114392 x268 <= .17114392 x269 <= .17114392 x270 <= .17114392 x271 <= .1603645 x272 <= .1603645 x273 <= .1603645 x274 <= .1603645 x275 <= .18267189 x276 <= .18267189 x277 <= .18267189 x278 <= .18267189 x279 <= .5323080366 x280 <= .5323080366 x281 <= .5323080366 x282 <= .5323080366 x283 <= .918715169866666 x284 <= .918715169866666 x285 <= .918715169866666 x286 <= .918715169866666 x287 <= 1.021726146 x288 <= 1.021726146 x289 <= 1.021726146 x290 <= 1.021726146 x291 <= 1.0706790744 x292 <= 1.0706790744 x293 <= 1.0706790744 x294 <= 1.0706790744 x295 <= 7.32543671346667 x296 <= 7.32543671346667 x297 <= 7.32543671346667 x298 <= 7.32543671346667 x299 <= 15.2453990736 x300 <= 15.2453990736 x301 <= 15.2453990736 x302 <= 15.2453990736 x303 <= 1.28061192466667 x304 <= 1.28061192466667 x305 <= 1.28061192466667 x306 <= 1.28061192466667 x307 <= 15.8815166933333 x308 <= 15.8815166933333 x309 <= 15.8815166933333 x310 <= 15.8815166933333 x311 <= 15.2472806811333 x312 <= 15.2472806811333 x313 <= 15.2472806811333 x314 <= 15.2472806811333 x315 <= 12.029055125 x316 <= 12.029055125 x317 <= 12.029055125 x318 <= 12.029055125 x319 <= 15.9672360214667 x320 <= 15.9672360214667 x321 <= 15.9672360214667 x322 <= 15.9672360214667 x323 <= 15.3736631157333 x324 <= 15.3736631157333 x325 <= 15.3736631157333 x326 <= 15.3736631157333 x327 <= 6.2237284564 x328 <= 6.2237284564 x329 <= 6.2237284564 x330 <= 6.2237284564 x331 <= 8.85892556 x332 <= 8.85892556 x333 <= 8.85892556 x334 <= 8.85892556 x335 <= 17.2437830768 x336 <= 17.2437830768 x337 <= 17.2437830768 x338 <= 17.2437830768 Binary b76 b77 b78 b79 b80 b81 b82 b83 b84 b85 b86 b87 b88 b89 b90 b91 b92 b93 b94 b95 b96 b97 b98 b99 b100 b101 b102 b103 b104 b105 b106 b107 b108 b109 b110 b111 b112 b113 b114 b115 b116 b117 b118 b119 b120 b121 b122 b123 b124 b125 b126 b127 b128 b129 b130 b131 b132 b133 b134 b135 b339 b340 b341 b342 b343 b344 b345 b346 b347 b348 b349 b350 b351 b352 b353 b354 b355 b356 b357 b358 b359 b360 b361 b362 b363 b364 b365 b366 b367 b368 b369 b370 b371 b372 b373 b374 b375 b376 b377 b378 b379 b380 b381 b382 b383 b384 b385 b386 b387 b388 b389 b390 b391 b392 b393 b394 b395 b396 b397 b398 b399 b400 End