#  MINLP written by GAMS Convert at 01/12/18 13:42:24
#  
#  Equation counts
#      Total        E        G        L        N        X        C        B
#       2372       76     2232       64        0        0        0        0
#  
#  Variable counts
#                   x        b        i      s1s      s2s       sc       si
#      Total     cont   binary  integer     sos1     sos2    scont     sint
#        401      279      122        0        0        0        0        0
#  FX      0        0        0        0        0        0        0        0
#  
#  Nonzero counts
#      Total    const       NL      DLL
#       8252     8072      180        0
# 
#  Reformulation has removed 1 variable and 1 equation


var x1 >= 0, <= 0.26351883;
var x2 >= 0, <= 0.26351883;
var x3 >= 0, <= 0.26351883;
var x4 >= 0, <= 0.26351883;
var x5 >= 0, <= 0.22891574;
var x6 >= 0, <= 0.22891574;
var x7 >= 0, <= 0.22891574;
var x8 >= 0, <= 0.22891574;
var x9 >= 0, <= 0.21464835;
var x10 >= 0, <= 0.21464835;
var x11 >= 0, <= 0.21464835;
var x12 >= 0, <= 0.21464835;
var x13 >= 0, <= 0.17964414;
var x14 >= 0, <= 0.17964414;
var x15 >= 0, <= 0.17964414;
var x16 >= 0, <= 0.17964414;
var x17 >= 0, <= 0.17402843;
var x18 >= 0, <= 0.17402843;
var x19 >= 0, <= 0.17402843;
var x20 >= 0, <= 0.17402843;
var x21 >= 0, <= 0.15355962;
var x22 >= 0, <= 0.15355962;
var x23 >= 0, <= 0.15355962;
var x24 >= 0, <= 0.15355962;
var x25 >= 0, <= 0.1942283;
var x26 >= 0, <= 0.1942283;
var x27 >= 0, <= 0.1942283;
var x28 >= 0, <= 0.1942283;
var x29 >= 0, <= 0.25670555;
var x30 >= 0, <= 0.25670555;
var x31 >= 0, <= 0.25670555;
var x32 >= 0, <= 0.25670555;
var x33 >= 0, <= 0.27088619;
var x34 >= 0, <= 0.27088619;
var x35 >= 0, <= 0.27088619;
var x36 >= 0, <= 0.27088619;
var x37 >= 0, <= 0.28985675;
var x38 >= 0, <= 0.28985675;
var x39 >= 0, <= 0.28985675;
var x40 >= 0, <= 0.28985675;
var x41 >= 0, <= 0.25550303;
var x42 >= 0, <= 0.25550303;
var x43 >= 0, <= 0.25550303;
var x44 >= 0, <= 0.25550303;
var x45 >= 0, <= 0.19001726;
var x46 >= 0, <= 0.19001726;
var x47 >= 0, <= 0.19001726;
var x48 >= 0, <= 0.19001726;
var x49 >= 0, <= 0.23803143;
var x50 >= 0, <= 0.23803143;
var x51 >= 0, <= 0.23803143;
var x52 >= 0, <= 0.23803143;
var x53 >= 0, <= 0.23312962;
var x54 >= 0, <= 0.23312962;
var x55 >= 0, <= 0.23312962;
var x56 >= 0, <= 0.23312962;
var x57 >= 0, <= 0.27705307;
var x58 >= 0, <= 0.27705307;
var x59 >= 0, <= 0.27705307;
var x60 >= 0, <= 0.27705307;
var x61 := 1.24666666666667, >= 1.24666666666667, <= 2.02;
var x62 := 2.48, >= 2.48, <= 4.01333333333333;
var x63 := 2.94666666666667, >= 2.94666666666667, <= 4.76;
var x64 := 3.69333333333333, >= 3.69333333333333, <= 5.96;
var x65 := 24.8733333333333, >= 24.8733333333333, <= 42.0933333333333;
var x66 := 58.6666666666667, >= 58.6666666666667, <= 99.28;
var x67 := 4.08, >= 4.08, <= 6.59333333333333;
var x68 := 36.56, >= 36.56, <= 61.8666666666667;
var x69 := 33.26, >= 33.26, <= 56.2866666666667;
var x70 := 24.52, >= 24.52, <= 41.5;
var x71 := 36.9266666666667, >= 36.9266666666667, <= 62.4933333333333;
var x72 := 50.0866666666667, >= 50.0866666666667, <= 80.9066666666667;
var x73 := 16.1866666666667, >= 16.1866666666667, <= 26.1466666666667;
var x74 := 23.52, >= 23.52, <= 38;
var x75 := 38.5266666666667, >= 38.5266666666667, <= 62.24;
var b76 binary >= 0, <= 1;
var b77 binary >= 0, <= 1;
var b78 binary >= 0, <= 1;
var b79 binary >= 0, <= 1;
var b80 binary >= 0, <= 1;
var b81 binary >= 0, <= 1;
var b82 binary >= 0, <= 1;
var b83 binary >= 0, <= 1;
var b84 binary >= 0, <= 1;
var b85 binary >= 0, <= 1;
var b86 binary >= 0, <= 1;
var b87 binary >= 0, <= 1;
var b88 binary >= 0, <= 1;
var b89 binary >= 0, <= 1;
var b90 binary >= 0, <= 1;
var b91 binary >= 0, <= 1;
var b92 binary >= 0, <= 1;
var b93 binary >= 0, <= 1;
var b94 binary >= 0, <= 1;
var b95 binary >= 0, <= 1;
var b96 binary >= 0, <= 1;
var b97 binary >= 0, <= 1;
var b98 binary >= 0, <= 1;
var b99 binary >= 0, <= 1;
var b100 binary >= 0, <= 1;
var b101 binary >= 0, <= 1;
var b102 binary >= 0, <= 1;
var b103 binary >= 0, <= 1;
var b104 binary >= 0, <= 1;
var b105 binary >= 0, <= 1;
var b106 binary >= 0, <= 1;
var b107 binary >= 0, <= 1;
var b108 binary >= 0, <= 1;
var b109 binary >= 0, <= 1;
var b110 binary >= 0, <= 1;
var b111 binary >= 0, <= 1;
var b112 binary >= 0, <= 1;
var b113 binary >= 0, <= 1;
var b114 binary >= 0, <= 1;
var b115 binary >= 0, <= 1;
var b116 binary >= 0, <= 1;
var b117 binary >= 0, <= 1;
var b118 binary >= 0, <= 1;
var b119 binary >= 0, <= 1;
var b120 binary >= 0, <= 1;
var b121 binary >= 0, <= 1;
var b122 binary >= 0, <= 1;
var b123 binary >= 0, <= 1;
var b124 binary >= 0, <= 1;
var b125 binary >= 0, <= 1;
var b126 binary >= 0, <= 1;
var b127 binary >= 0, <= 1;
var b128 binary >= 0, <= 1;
var b129 binary >= 0, <= 1;
var b130 binary >= 0, <= 1;
var b131 binary >= 0, <= 1;
var b132 binary >= 0, <= 1;
var b133 binary >= 0, <= 1;
var b134 binary >= 0, <= 1;
var b135 binary >= 0, <= 1;
var x136 >= 0, <= 0.5323080366;
var x137 >= 0, <= 0.918715169866666;
var x138 >= 0, <= 1.021726146;
var x139 >= 0, <= 1.0706790744;
var x140 >= 0, <= 7.32543671346667;
var x141 >= 0, <= 15.2453990736;
var x142 >= 0, <= 1.28061192466667;
var x143 >= 0, <= 15.8815166933333;
var x144 >= 0, <= 15.2472806811333;
var x145 >= 0, <= 12.029055125;
var x146 >= 0, <= 15.9672360214667;
var x147 >= 0, <= 15.3736631157333;
var x148 >= 0, <= 6.2237284564;
var x149 >= 0, <= 8.85892556;
var x150 >= 0, <= 17.2437830768;
var x151 := 0.25788969, >= 0.25788969, <= 0.35227087;
var x152 := 0.25788969, >= 0.25788969, <= 0.35227087;
var x153 := 0.25788969, >= 0.25788969, <= 0.35227087;
var x154 := 0.25788969, >= 0.25788969, <= 0.35227087;
var x155 := -0.7794471, >= -0.98493628, <= -0.7794471;
var x156 := -0.7794471, >= -0.98493628, <= -0.7794471;
var x157 := -0.7794471, >= -0.98493628, <= -0.7794471;
var x158 := -0.7794471, >= -0.98493628, <= -0.7794471;
var x159 >= 0, <= 0.0580296499999999;
var x160 >= 0, <= 0.0580296499999999;
var x161 >= 0, <= 0.0580296499999999;
var x162 >= 0, <= 0.0580296499999999;
var x163 >= 0, <= 0.0546689399999999;
var x164 >= 0, <= 0.0546689399999999;
var x165 >= 0, <= 0.0546689399999999;
var x166 >= 0, <= 0.0546689399999999;
var x167 >= 0, <= 0.09360565;
var x168 >= 0, <= 0.09360565;
var x169 >= 0, <= 0.09360565;
var x170 >= 0, <= 0.09360565;
var x171 >= 0, <= 0.0476880399999999;
var x172 >= 0, <= 0.0476880399999999;
var x173 >= 0, <= 0.0476880399999999;
var x174 >= 0, <= 0.0476880399999999;
var x175 >= 0, <= 0.05276021;
var x176 >= 0, <= 0.05276021;
var x177 >= 0, <= 0.05276021;
var x178 >= 0, <= 0.05276021;
var x179 >= 0, <= 0.04905388;
var x180 >= 0, <= 0.04905388;
var x181 >= 0, <= 0.04905388;
var x182 >= 0, <= 0.04905388;
var x183 >= 0, <= 0.07731692;
var x184 >= 0, <= 0.07731692;
var x185 >= 0, <= 0.07731692;
var x186 >= 0, <= 0.07731692;
var x187 >= 0, <= 0.08211741;
var x188 >= 0, <= 0.08211741;
var x189 >= 0, <= 0.08211741;
var x190 >= 0, <= 0.08211741;
var x191 >= 0, <= 0.09438118;
var x192 >= 0, <= 0.09438118;
var x193 >= 0, <= 0.09438118;
var x194 >= 0, <= 0.09438118;
var x195 >= 0, <= 0.08436757;
var x196 >= 0, <= 0.08436757;
var x197 >= 0, <= 0.08436757;
var x198 >= 0, <= 0.08436757;
var x199 >= 0, <= 0.06987597;
var x200 >= 0, <= 0.06987597;
var x201 >= 0, <= 0.06987597;
var x202 >= 0, <= 0.06987597;
var x203 >= 0, <= 0.04788831;
var x204 >= 0, <= 0.04788831;
var x205 >= 0, <= 0.04788831;
var x206 >= 0, <= 0.04788831;
var x207 >= 0, <= 0.0668875099999999;
var x208 >= 0, <= 0.0668875099999999;
var x209 >= 0, <= 0.0668875099999999;
var x210 >= 0, <= 0.0668875099999999;
var x211 >= 0, <= 0.07276512;
var x212 >= 0, <= 0.07276512;
var x213 >= 0, <= 0.07276512;
var x214 >= 0, <= 0.07276512;
var x215 >= 0, <= 0.09438118;
var x216 >= 0, <= 0.09438118;
var x217 >= 0, <= 0.09438118;
var x218 >= 0, <= 0.09438118;
var x219 >= 0, <= 0.20548918;
var x220 >= 0, <= 0.20548918;
var x221 >= 0, <= 0.20548918;
var x222 >= 0, <= 0.20548918;
var x223 >= 0, <= 0.1742468;
var x224 >= 0, <= 0.1742468;
var x225 >= 0, <= 0.1742468;
var x226 >= 0, <= 0.1742468;
var x227 >= 0, <= 0.1210427;
var x228 >= 0, <= 0.1210427;
var x229 >= 0, <= 0.1210427;
var x230 >= 0, <= 0.1210427;
var x231 >= 0, <= 0.1319561;
var x232 >= 0, <= 0.1319561;
var x233 >= 0, <= 0.1319561;
var x234 >= 0, <= 0.1319561;
var x235 >= 0, <= 0.12126822;
var x236 >= 0, <= 0.12126822;
var x237 >= 0, <= 0.12126822;
var x238 >= 0, <= 0.12126822;
var x239 >= 0, <= 0.10450574;
var x240 >= 0, <= 0.10450574;
var x241 >= 0, <= 0.10450574;
var x242 >= 0, <= 0.10450574;
var x243 >= 0, <= 0.11691138;
var x244 >= 0, <= 0.11691138;
var x245 >= 0, <= 0.11691138;
var x246 >= 0, <= 0.11691138;
var x247 >= 0, <= 0.17458814;
var x248 >= 0, <= 0.17458814;
var x249 >= 0, <= 0.17458814;
var x250 >= 0, <= 0.17458814;
var x251 >= 0, <= 0.17650501;
var x252 >= 0, <= 0.17650501;
var x253 >= 0, <= 0.17650501;
var x254 >= 0, <= 0.17650501;
var x255 >= 0, <= 0.20548918;
var x256 >= 0, <= 0.20548918;
var x257 >= 0, <= 0.20548918;
var x258 >= 0, <= 0.20548918;
var x259 >= 0, <= 0.18562706;
var x260 >= 0, <= 0.18562706;
var x261 >= 0, <= 0.18562706;
var x262 >= 0, <= 0.18562706;
var x263 >= 0, <= 0.14212895;
var x264 >= 0, <= 0.14212895;
var x265 >= 0, <= 0.14212895;
var x266 >= 0, <= 0.14212895;
var x267 >= 0, <= 0.17114392;
var x268 >= 0, <= 0.17114392;
var x269 >= 0, <= 0.17114392;
var x270 >= 0, <= 0.17114392;
var x271 >= 0, <= 0.1603645;
var x272 >= 0, <= 0.1603645;
var x273 >= 0, <= 0.1603645;
var x274 >= 0, <= 0.1603645;
var x275 >= 0, <= 0.18267189;
var x276 >= 0, <= 0.18267189;
var x277 >= 0, <= 0.18267189;
var x278 >= 0, <= 0.18267189;
var x279 >= 0, <= 0.5323080366;
var x280 >= 0, <= 0.5323080366;
var x281 >= 0, <= 0.5323080366;
var x282 >= 0, <= 0.5323080366;
var x283 >= 0, <= 0.918715169866666;
var x284 >= 0, <= 0.918715169866666;
var x285 >= 0, <= 0.918715169866666;
var x286 >= 0, <= 0.918715169866666;
var x287 >= 0, <= 1.021726146;
var x288 >= 0, <= 1.021726146;
var x289 >= 0, <= 1.021726146;
var x290 >= 0, <= 1.021726146;
var x291 >= 0, <= 1.0706790744;
var x292 >= 0, <= 1.0706790744;
var x293 >= 0, <= 1.0706790744;
var x294 >= 0, <= 1.0706790744;
var x295 >= 0, <= 7.32543671346667;
var x296 >= 0, <= 7.32543671346667;
var x297 >= 0, <= 7.32543671346667;
var x298 >= 0, <= 7.32543671346667;
var x299 >= 0, <= 15.2453990736;
var x300 >= 0, <= 15.2453990736;
var x301 >= 0, <= 15.2453990736;
var x302 >= 0, <= 15.2453990736;
var x303 >= 0, <= 1.28061192466667;
var x304 >= 0, <= 1.28061192466667;
var x305 >= 0, <= 1.28061192466667;
var x306 >= 0, <= 1.28061192466667;
var x307 >= 0, <= 15.8815166933333;
var x308 >= 0, <= 15.8815166933333;
var x309 >= 0, <= 15.8815166933333;
var x310 >= 0, <= 15.8815166933333;
var x311 >= 0, <= 15.2472806811333;
var x312 >= 0, <= 15.2472806811333;
var x313 >= 0, <= 15.2472806811333;
var x314 >= 0, <= 15.2472806811333;
var x315 >= 0, <= 12.029055125;
var x316 >= 0, <= 12.029055125;
var x317 >= 0, <= 12.029055125;
var x318 >= 0, <= 12.029055125;
var x319 >= 0, <= 15.9672360214667;
var x320 >= 0, <= 15.9672360214667;
var x321 >= 0, <= 15.9672360214667;
var x322 >= 0, <= 15.9672360214667;
var x323 >= 0, <= 15.3736631157333;
var x324 >= 0, <= 15.3736631157333;
var x325 >= 0, <= 15.3736631157333;
var x326 >= 0, <= 15.3736631157333;
var x327 >= 0, <= 6.2237284564;
var x328 >= 0, <= 6.2237284564;
var x329 >= 0, <= 6.2237284564;
var x330 >= 0, <= 6.2237284564;
var x331 >= 0, <= 8.85892556;
var x332 >= 0, <= 8.85892556;
var x333 >= 0, <= 8.85892556;
var x334 >= 0, <= 8.85892556;
var x335 >= 0, <= 17.2437830768;
var x336 >= 0, <= 17.2437830768;
var x337 >= 0, <= 17.2437830768;
var x338 >= 0, <= 17.2437830768;
var b339 binary >= 0, <= 1;
var b340 binary >= 0, <= 1;
var b341 binary >= 0, <= 1;
var b342 binary >= 0, <= 1;
var b343 binary >= 0, <= 1;
var b344 binary >= 0, <= 1;
var b345 binary >= 0, <= 1;
var b346 binary >= 0, <= 1;
var b347 binary >= 0, <= 1;
var b348 binary >= 0, <= 1;
var b349 binary >= 0, <= 1;
var b350 binary >= 0, <= 1;
var b351 binary >= 0, <= 1;
var b352 binary >= 0, <= 1;
var b353 binary >= 0, <= 1;
var b354 binary >= 0, <= 1;
var b355 binary >= 0, <= 1;
var b356 binary >= 0, <= 1;
var b357 binary >= 0, <= 1;
var b358 binary >= 0, <= 1;
var b359 binary >= 0, <= 1;
var b360 binary >= 0, <= 1;
var b361 binary >= 0, <= 1;
var b362 binary >= 0, <= 1;
var b363 binary >= 0, <= 1;
var b364 binary >= 0, <= 1;
var b365 binary >= 0, <= 1;
var b366 binary >= 0, <= 1;
var b367 binary >= 0, <= 1;
var b368 binary >= 0, <= 1;
var b369 binary >= 0, <= 1;
var b370 binary >= 0, <= 1;
var b371 binary >= 0, <= 1;
var b372 binary >= 0, <= 1;
var b373 binary >= 0, <= 1;
var b374 binary >= 0, <= 1;
var b375 binary >= 0, <= 1;
var b376 binary >= 0, <= 1;
var b377 binary >= 0, <= 1;
var b378 binary >= 0, <= 1;
var b379 binary >= 0, <= 1;
var b380 binary >= 0, <= 1;
var b381 binary >= 0, <= 1;
var b382 binary >= 0, <= 1;
var b383 binary >= 0, <= 1;
var b384 binary >= 0, <= 1;
var b385 binary >= 0, <= 1;
var b386 binary >= 0, <= 1;
var b387 binary >= 0, <= 1;
var b388 binary >= 0, <= 1;
var b389 binary >= 0, <= 1;
var b390 binary >= 0, <= 1;
var b391 binary >= 0, <= 1;
var b392 binary >= 0, <= 1;
var b393 binary >= 0, <= 1;
var b394 binary >= 0, <= 1;
var b395 binary >= 0, <= 1;
var b396 binary >= 0, <= 1;
var b397 binary >= 0, <= 1;
var b398 binary >= 0, <= 1;
var b399 binary >= 0, <= 1;
var b400 binary >= 0, <= 1;

minimize obj:    x136 + x137 + x138 + x139 + x140 + x141 + x142 + x143 + x144
     + x145 + x146 + x147 + x148 + x149 + x150;

subject to

e2: -x61*x1*b76 + x279 >= 0;

e3: -x61*x2*b77 + x280 >= 0;

e4: -x61*x3*b78 + x281 >= 0;

e5: -x61*x4*b79 + x282 >= 0;

e6: -x62*x5*b80 + x283 >= 0;

e7: -x62*x6*b81 + x284 >= 0;

e8: -x62*x7*b82 + x285 >= 0;

e9: -x62*x8*b83 + x286 >= 0;

e10: -x63*x9*b84 + x287 >= 0;

e11: -x63*x10*b85 + x288 >= 0;

e12: -x63*x11*b86 + x289 >= 0;

e13: -x63*x12*b87 + x290 >= 0;

e14: -x64*x13*b88 + x291 >= 0;

e15: -x64*x14*b89 + x292 >= 0;

e16: -x64*x15*b90 + x293 >= 0;

e17: -x64*x16*b91 + x294 >= 0;

e18: -x65*x17*b92 + x295 >= 0;

e19: -x65*x18*b93 + x296 >= 0;

e20: -x65*x19*b94 + x297 >= 0;

e21: -x65*x20*b95 + x298 >= 0;

e22: -x66*x21*b96 + x299 >= 0;

e23: -x66*x22*b97 + x300 >= 0;

e24: -x66*x23*b98 + x301 >= 0;

e25: -x66*x24*b99 + x302 >= 0;

e26: -x67*x25*b100 + x303 >= 0;

e27: -x67*x26*b101 + x304 >= 0;

e28: -x67*x27*b102 + x305 >= 0;

e29: -x67*x28*b103 + x306 >= 0;

e30: -x68*x29*b104 + x307 >= 0;

e31: -x68*x30*b105 + x308 >= 0;

e32: -x68*x31*b106 + x309 >= 0;

e33: -x68*x32*b107 + x310 >= 0;

e34: -x69*x33*b108 + x311 >= 0;

e35: -x69*x34*b109 + x312 >= 0;

e36: -x69*x35*b110 + x313 >= 0;

e37: -x69*x36*b111 + x314 >= 0;

e38: -x70*x37*b112 + x315 >= 0;

e39: -x70*x38*b113 + x316 >= 0;

e40: -x70*x39*b114 + x317 >= 0;

e41: -x70*x40*b115 + x318 >= 0;

e42: -x71*x41*b116 + x319 >= 0;

e43: -x71*x42*b117 + x320 >= 0;

e44: -x71*x43*b118 + x321 >= 0;

e45: -x71*x44*b119 + x322 >= 0;

e46: -x72*x45*b120 + x323 >= 0;

e47: -x72*x46*b121 + x324 >= 0;

e48: -x72*x47*b122 + x325 >= 0;

e49: -x72*x48*b123 + x326 >= 0;

e50: -x73*x49*b124 + x327 >= 0;

e51: -x73*x50*b125 + x328 >= 0;

e52: -x73*x51*b126 + x329 >= 0;

e53: -x73*x52*b127 + x330 >= 0;

e54: -x74*x53*b128 + x331 >= 0;

e55: -x74*x54*b129 + x332 >= 0;

e56: -x74*x55*b130 + x333 >= 0;

e57: -x74*x56*b131 + x334 >= 0;

e58: -x75*x57*b132 + x335 >= 0;

e59: -x75*x58*b133 + x336 >= 0;

e60: -x75*x59*b134 + x337 >= 0;

e61: -x75*x60*b135 + x338 >= 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 >= 0.29424122;

e82:    x152 + x160 >= 0.29424122;

e83:    x153 + x161 >= 0.29424122;

e84:    x154 + x162 >= 0.29424122;

e85:    x151 + x163 >= 0.29760193;

e86:    x152 + x164 >= 0.29760193;

e87:    x153 + x165 >= 0.29760193;

e88:    x154 + x166 >= 0.29760193;

e89:    x151 + x167 >= 0.35149534;

e90:    x152 + x168 >= 0.35149534;

e91:    x153 + x169 >= 0.35149534;

e92:    x154 + x170 >= 0.35149534;

e93:    x151 + x171 >= 0.30458283;

e94:    x152 + x172 >= 0.30458283;

e95:    x153 + x173 >= 0.30458283;

e96:    x154 + x174 >= 0.30458283;

e97:    x151 + x175 >= 0.29951066;

e98:    x152 + x176 >= 0.29951066;

e99:    x153 + x177 >= 0.29951066;

e100:    x154 + x178 >= 0.29951066;

e101:    x151 + x179 >= 0.30694357;

e102:    x152 + x180 >= 0.30694357;

e103:    x153 + x181 >= 0.30694357;

e104:    x154 + x182 >= 0.30694357;

e105:    x151 + x183 >= 0.33520661;

e106:    x152 + x184 >= 0.33520661;

e107:    x153 + x185 >= 0.33520661;

e108:    x154 + x186 >= 0.33520661;

e109:    x151 + x187 >= 0.3400071;

e110:    x152 + x188 >= 0.3400071;

e111:    x153 + x189 >= 0.3400071;

e112:    x154 + x190 >= 0.3400071;

e113:    x151 + x191 >= 0.35227087;

e114:    x152 + x192 >= 0.35227087;

e115:    x153 + x193 >= 0.35227087;

e116:    x154 + x194 >= 0.35227087;

e117:    x151 + x195 >= 0.34225726;

e118:    x152 + x196 >= 0.34225726;

e119:    x153 + x197 >= 0.34225726;

e120:    x154 + x198 >= 0.34225726;

e121:    x151 + x199 >= 0.32776566;

e122:    x152 + x200 >= 0.32776566;

e123:    x153 + x201 >= 0.32776566;

e124:    x154 + x202 >= 0.32776566;

e125:    x151 + x203 >= 0.30438256;

e126:    x152 + x204 >= 0.30438256;

e127:    x153 + x205 >= 0.30438256;

e128:    x154 + x206 >= 0.30438256;

e129:    x151 + x207 >= 0.28538336;

e130:    x152 + x208 >= 0.28538336;

e131:    x153 + x209 >= 0.28538336;

e132:    x154 + x210 >= 0.28538336;

e133:    x151 + x211 >= 0.27950575;

e134:    x152 + x212 >= 0.27950575;

e135:    x153 + x213 >= 0.27950575;

e136:    x154 + x214 >= 0.27950575;

e137:  - x151 + x159 >= -0.29424122;

e138:  - x152 + x160 >= -0.29424122;

e139:  - x153 + x161 >= -0.29424122;

e140:  - x154 + x162 >= -0.29424122;

e141:  - x151 + x163 >= -0.29760193;

e142:  - x152 + x164 >= -0.29760193;

e143:  - x153 + x165 >= -0.29760193;

e144:  - x154 + x166 >= -0.29760193;

e145:  - x151 + x167 >= -0.35149534;

e146:  - x152 + x168 >= -0.35149534;

e147:  - x153 + x169 >= -0.35149534;

e148:  - x154 + x170 >= -0.35149534;

e149:  - x151 + x171 >= -0.30458283;

e150:  - x152 + x172 >= -0.30458283;

e151:  - x153 + x173 >= -0.30458283;

e152:  - x154 + x174 >= -0.30458283;

e153:  - x151 + x175 >= -0.29951066;

e154:  - x152 + x176 >= -0.29951066;

e155:  - x153 + x177 >= -0.29951066;

e156:  - x154 + x178 >= -0.29951066;

e157:  - x151 + x179 >= -0.30694357;

e158:  - x152 + x180 >= -0.30694357;

e159:  - x153 + x181 >= -0.30694357;

e160:  - x154 + x182 >= -0.30694357;

e161:  - x151 + x183 >= -0.33520661;

e162:  - x152 + x184 >= -0.33520661;

e163:  - x153 + x185 >= -0.33520661;

e164:  - x154 + x186 >= -0.33520661;

e165:  - x151 + x187 >= -0.3400071;

e166:  - x152 + x188 >= -0.3400071;

e167:  - x153 + x189 >= -0.3400071;

e168:  - x154 + x190 >= -0.3400071;

e169:  - x151 + x195 >= -0.34225726;

e170:  - x152 + x196 >= -0.34225726;

e171:  - x153 + x197 >= -0.34225726;

e172:  - x154 + x198 >= -0.34225726;

e173:  - x151 + x199 >= -0.32776566;

e174:  - x152 + x200 >= -0.32776566;

e175:  - x153 + x201 >= -0.32776566;

e176:  - x154 + x202 >= -0.32776566;

e177:  - x151 + x203 >= -0.30438256;

e178:  - x152 + x204 >= -0.30438256;

e179:  - x153 + x205 >= -0.30438256;

e180:  - x154 + x206 >= -0.30438256;

e181:  - x151 + x207 >= -0.28538336;

e182:  - x152 + x208 >= -0.28538336;

e183:  - x153 + x209 >= -0.28538336;

e184:  - x154 + x210 >= -0.28538336;

e185:  - x151 + x211 >= -0.27950575;

e186:  - x152 + x212 >= -0.27950575;

e187:  - x153 + x213 >= -0.27950575;

e188:  - x154 + x214 >= -0.27950575;

e189:  - x151 + x215 >= -0.25788969;

e190:  - x152 + x216 >= -0.25788969;

e191:  - x153 + x217 >= -0.25788969;

e192:  - x154 + x218 >= -0.25788969;

e193:    x155 + x223 >= -0.9536939;

e194:    x156 + x224 >= -0.9536939;

e195:    x157 + x225 >= -0.9536939;

e196:    x158 + x226 >= -0.9536939;

e197:    x155 + x227 >= -0.9004898;

e198:    x156 + x228 >= -0.9004898;

e199:    x157 + x229 >= -0.9004898;

e200:    x158 + x230 >= -0.9004898;

e201:    x155 + x231 >= -0.9114032;

e202:    x156 + x232 >= -0.9114032;

e203:    x157 + x233 >= -0.9114032;

e204:    x158 + x234 >= -0.9114032;

e205:    x155 + x235 >= -0.90071532;

e206:    x156 + x236 >= -0.90071532;

e207:    x157 + x237 >= -0.90071532;

e208:    x158 + x238 >= -0.90071532;

e209:    x155 + x239 >= -0.88043054;

e210:    x156 + x240 >= -0.88043054;

e211:    x157 + x241 >= -0.88043054;

e212:    x158 + x242 >= -0.88043054;

e213:    x155 + x243 >= -0.8680249;

e214:    x156 + x244 >= -0.8680249;

e215:    x157 + x245 >= -0.8680249;

e216:    x158 + x246 >= -0.8680249;

e217:    x155 + x247 >= -0.81034814;

e218:    x156 + x248 >= -0.81034814;

e219:    x157 + x249 >= -0.81034814;

e220:    x158 + x250 >= -0.81034814;

e221:    x155 + x251 >= -0.80843127;

e222:    x156 + x252 >= -0.80843127;

e223:    x157 + x253 >= -0.80843127;

e224:    x158 + x254 >= -0.80843127;

e225:    x155 + x255 >= -0.7794471;

e226:    x156 + x256 >= -0.7794471;

e227:    x157 + x257 >= -0.7794471;

e228:    x158 + x258 >= -0.7794471;

e229:    x155 + x259 >= -0.79930922;

e230:    x156 + x260 >= -0.79930922;

e231:    x157 + x261 >= -0.79930922;

e232:    x158 + x262 >= -0.79930922;

e233:    x155 + x263 >= -0.84280733;

e234:    x156 + x264 >= -0.84280733;

e235:    x157 + x265 >= -0.84280733;

e236:    x158 + x266 >= -0.84280733;

e237:    x155 + x267 >= -0.81379236;

e238:    x156 + x268 >= -0.81379236;

e239:    x157 + x269 >= -0.81379236;

e240:    x158 + x270 >= -0.81379236;

e241:    x155 + x271 >= -0.82457178;

e242:    x156 + x272 >= -0.82457178;

e243:    x157 + x273 >= -0.82457178;

e244:    x158 + x274 >= -0.82457178;

e245:    x155 + x275 >= -0.80226439;

e246:    x156 + x276 >= -0.80226439;

e247:    x157 + x277 >= -0.80226439;

e248:    x158 + x278 >= -0.80226439;

e249:  - x155 + x219 >= 0.98493628;

e250:  - x156 + x220 >= 0.98493628;

e251:  - x157 + x221 >= 0.98493628;

e252:  - x158 + x222 >= 0.98493628;

e253:  - x155 + x223 >= 0.9536939;

e254:  - x156 + x224 >= 0.9536939;

e255:  - x157 + x225 >= 0.9536939;

e256:  - x158 + x226 >= 0.9536939;

e257:  - x155 + x227 >= 0.9004898;

e258:  - x156 + x228 >= 0.9004898;

e259:  - x157 + x229 >= 0.9004898;

e260:  - x158 + x230 >= 0.9004898;

e261:  - x155 + x231 >= 0.9114032;

e262:  - x156 + x232 >= 0.9114032;

e263:  - x157 + x233 >= 0.9114032;

e264:  - x158 + x234 >= 0.9114032;

e265:  - x155 + x235 >= 0.90071532;

e266:  - x156 + x236 >= 0.90071532;

e267:  - x157 + x237 >= 0.90071532;

e268:  - x158 + x238 >= 0.90071532;

e269:  - x155 + x239 >= 0.88043054;

e270:  - x156 + x240 >= 0.88043054;

e271:  - x157 + x241 >= 0.88043054;

e272:  - x158 + x242 >= 0.88043054;

e273:  - x155 + x243 >= 0.8680249;

e274:  - x156 + x244 >= 0.8680249;

e275:  - x157 + x245 >= 0.8680249;

e276:  - x158 + x246 >= 0.8680249;

e277:  - x155 + x247 >= 0.81034814;

e278:  - x156 + x248 >= 0.81034814;

e279:  - x157 + x249 >= 0.81034814;

e280:  - x158 + x250 >= 0.81034814;

e281:  - x155 + x251 >= 0.80843127;

e282:  - x156 + x252 >= 0.80843127;

e283:  - x157 + x253 >= 0.80843127;

e284:  - x158 + x254 >= 0.80843127;

e285:  - x155 + x259 >= 0.79930922;

e286:  - x156 + x260 >= 0.79930922;

e287:  - x157 + x261 >= 0.79930922;

e288:  - x158 + x262 >= 0.79930922;

e289:  - x155 + x263 >= 0.84280733;

e290:  - x156 + x264 >= 0.84280733;

e291:  - x157 + x265 >= 0.84280733;

e292:  - x158 + x266 >= 0.84280733;

e293:  - x155 + x267 >= 0.81379236;

e294:  - x156 + x268 >= 0.81379236;

e295:  - x157 + x269 >= 0.81379236;

e296:  - x158 + x270 >= 0.81379236;

e297:  - x155 + x271 >= 0.82457178;

e298:  - x156 + x272 >= 0.82457178;

e299:  - x157 + x273 >= 0.82457178;

e300:  - x158 + x274 >= 0.82457178;

e301:  - x155 + x275 >= 0.80226439;

e302:  - x156 + x276 >= 0.80226439;

e303:  - x157 + x277 >= 0.80226439;

e304:  - x158 + x278 >= 0.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;