#  MINLP written by GAMS Convert at 01/12/18 13:42:23
#  
#  Equation counts
#      Total        E        G        L        N        X        C        B
#       2269       61     2160       48        0        0        0        0
#  
#  Variable counts
#                   x        b        i      s1s      s2s       sc       si
#      Total     cont   binary  integer     sos1     sos2    scont     sint
#        324      217      107        0        0        0        0        0
#  FX      0        0        0        0        0        0        0        0
#  
#  Nonzero counts
#      Total    const       NL      DLL
#       7973     7838      135        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.22891574;
var x5 >= 0, <= 0.22891574;
var x6 >= 0, <= 0.22891574;
var x7 >= 0, <= 0.21464835;
var x8 >= 0, <= 0.21464835;
var x9 >= 0, <= 0.21464835;
var x10 >= 0, <= 0.17964414;
var x11 >= 0, <= 0.17964414;
var x12 >= 0, <= 0.17964414;
var x13 >= 0, <= 0.17402843;
var x14 >= 0, <= 0.17402843;
var x15 >= 0, <= 0.17402843;
var x16 >= 0, <= 0.15355962;
var x17 >= 0, <= 0.15355962;
var x18 >= 0, <= 0.15355962;
var x19 >= 0, <= 0.1942283;
var x20 >= 0, <= 0.1942283;
var x21 >= 0, <= 0.1942283;
var x22 >= 0, <= 0.25670555;
var x23 >= 0, <= 0.25670555;
var x24 >= 0, <= 0.25670555;
var x25 >= 0, <= 0.27088619;
var x26 >= 0, <= 0.27088619;
var x27 >= 0, <= 0.27088619;
var x28 >= 0, <= 0.28985675;
var x29 >= 0, <= 0.28985675;
var x30 >= 0, <= 0.28985675;
var x31 >= 0, <= 0.25550303;
var x32 >= 0, <= 0.25550303;
var x33 >= 0, <= 0.25550303;
var x34 >= 0, <= 0.19001726;
var x35 >= 0, <= 0.19001726;
var x36 >= 0, <= 0.19001726;
var x37 >= 0, <= 0.23803143;
var x38 >= 0, <= 0.23803143;
var x39 >= 0, <= 0.23803143;
var x40 >= 0, <= 0.23312962;
var x41 >= 0, <= 0.23312962;
var x42 >= 0, <= 0.23312962;
var x43 >= 0, <= 0.27705307;
var x44 >= 0, <= 0.27705307;
var x45 >= 0, <= 0.27705307;
var x46 := 1.24666666666667, >= 1.24666666666667, <= 2.02;
var x47 := 2.48, >= 2.48, <= 4.01333333333333;
var x48 := 2.94666666666667, >= 2.94666666666667, <= 4.76;
var x49 := 3.69333333333333, >= 3.69333333333333, <= 5.96;
var x50 := 24.8733333333333, >= 24.8733333333333, <= 42.0933333333333;
var x51 := 58.6666666666667, >= 58.6666666666667, <= 99.28;
var x52 := 4.08, >= 4.08, <= 6.59333333333333;
var x53 := 36.56, >= 36.56, <= 61.8666666666667;
var x54 := 33.26, >= 33.26, <= 56.2866666666667;
var x55 := 24.52, >= 24.52, <= 41.5;
var x56 := 36.9266666666667, >= 36.9266666666667, <= 62.4933333333333;
var x57 := 50.0866666666667, >= 50.0866666666667, <= 80.9066666666667;
var x58 := 16.1866666666667, >= 16.1866666666667, <= 26.1466666666667;
var x59 := 23.52, >= 23.52, <= 38;
var x60 := 38.5266666666667, >= 38.5266666666667, <= 62.24;
var b61 binary >= 0, <= 1;
var b62 binary >= 0, <= 1;
var b63 binary >= 0, <= 1;
var b64 binary >= 0, <= 1;
var b65 binary >= 0, <= 1;
var b66 binary >= 0, <= 1;
var b67 binary >= 0, <= 1;
var b68 binary >= 0, <= 1;
var b69 binary >= 0, <= 1;
var b70 binary >= 0, <= 1;
var b71 binary >= 0, <= 1;
var b72 binary >= 0, <= 1;
var b73 binary >= 0, <= 1;
var b74 binary >= 0, <= 1;
var b75 binary >= 0, <= 1;
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 x106 >= 0, <= 0.5323080366;
var x107 >= 0, <= 0.918715169866666;
var x108 >= 0, <= 1.021726146;
var x109 >= 0, <= 1.0706790744;
var x110 >= 0, <= 7.32543671346667;
var x111 >= 0, <= 15.2453990736;
var x112 >= 0, <= 1.28061192466667;
var x113 >= 0, <= 15.8815166933333;
var x114 >= 0, <= 15.2472806811333;
var x115 >= 0, <= 12.029055125;
var x116 >= 0, <= 15.9672360214667;
var x117 >= 0, <= 15.3736631157333;
var x118 >= 0, <= 6.2237284564;
var x119 >= 0, <= 8.85892556;
var x120 >= 0, <= 17.2437830768;
var x121 := 0.25788969, >= 0.25788969, <= 0.35227087;
var x122 := 0.25788969, >= 0.25788969, <= 0.35227087;
var x123 := 0.25788969, >= 0.25788969, <= 0.35227087;
var x124 := -0.7794471, >= -0.98493628, <= -0.7794471;
var x125 := -0.7794471, >= -0.98493628, <= -0.7794471;
var x126 := -0.7794471, >= -0.98493628, <= -0.7794471;
var x127 >= 0, <= 0.0580296499999999;
var x128 >= 0, <= 0.0580296499999999;
var x129 >= 0, <= 0.0580296499999999;
var x130 >= 0, <= 0.0546689399999999;
var x131 >= 0, <= 0.0546689399999999;
var x132 >= 0, <= 0.0546689399999999;
var x133 >= 0, <= 0.09360565;
var x134 >= 0, <= 0.09360565;
var x135 >= 0, <= 0.09360565;
var x136 >= 0, <= 0.0476880399999999;
var x137 >= 0, <= 0.0476880399999999;
var x138 >= 0, <= 0.0476880399999999;
var x139 >= 0, <= 0.05276021;
var x140 >= 0, <= 0.05276021;
var x141 >= 0, <= 0.05276021;
var x142 >= 0, <= 0.04905388;
var x143 >= 0, <= 0.04905388;
var x144 >= 0, <= 0.04905388;
var x145 >= 0, <= 0.07731692;
var x146 >= 0, <= 0.07731692;
var x147 >= 0, <= 0.07731692;
var x148 >= 0, <= 0.08211741;
var x149 >= 0, <= 0.08211741;
var x150 >= 0, <= 0.08211741;
var x151 >= 0, <= 0.09438118;
var x152 >= 0, <= 0.09438118;
var x153 >= 0, <= 0.09438118;
var x154 >= 0, <= 0.08436757;
var x155 >= 0, <= 0.08436757;
var x156 >= 0, <= 0.08436757;
var x157 >= 0, <= 0.06987597;
var x158 >= 0, <= 0.06987597;
var x159 >= 0, <= 0.06987597;
var x160 >= 0, <= 0.04788831;
var x161 >= 0, <= 0.04788831;
var x162 >= 0, <= 0.04788831;
var x163 >= 0, <= 0.0668875099999999;
var x164 >= 0, <= 0.0668875099999999;
var x165 >= 0, <= 0.0668875099999999;
var x166 >= 0, <= 0.07276512;
var x167 >= 0, <= 0.07276512;
var x168 >= 0, <= 0.07276512;
var x169 >= 0, <= 0.09438118;
var x170 >= 0, <= 0.09438118;
var x171 >= 0, <= 0.09438118;
var x172 >= 0, <= 0.20548918;
var x173 >= 0, <= 0.20548918;
var x174 >= 0, <= 0.20548918;
var x175 >= 0, <= 0.1742468;
var x176 >= 0, <= 0.1742468;
var x177 >= 0, <= 0.1742468;
var x178 >= 0, <= 0.1210427;
var x179 >= 0, <= 0.1210427;
var x180 >= 0, <= 0.1210427;
var x181 >= 0, <= 0.1319561;
var x182 >= 0, <= 0.1319561;
var x183 >= 0, <= 0.1319561;
var x184 >= 0, <= 0.12126822;
var x185 >= 0, <= 0.12126822;
var x186 >= 0, <= 0.12126822;
var x187 >= 0, <= 0.10450574;
var x188 >= 0, <= 0.10450574;
var x189 >= 0, <= 0.10450574;
var x190 >= 0, <= 0.11691138;
var x191 >= 0, <= 0.11691138;
var x192 >= 0, <= 0.11691138;
var x193 >= 0, <= 0.17458814;
var x194 >= 0, <= 0.17458814;
var x195 >= 0, <= 0.17458814;
var x196 >= 0, <= 0.17650501;
var x197 >= 0, <= 0.17650501;
var x198 >= 0, <= 0.17650501;
var x199 >= 0, <= 0.20548918;
var x200 >= 0, <= 0.20548918;
var x201 >= 0, <= 0.20548918;
var x202 >= 0, <= 0.18562706;
var x203 >= 0, <= 0.18562706;
var x204 >= 0, <= 0.18562706;
var x205 >= 0, <= 0.14212895;
var x206 >= 0, <= 0.14212895;
var x207 >= 0, <= 0.14212895;
var x208 >= 0, <= 0.17114392;
var x209 >= 0, <= 0.17114392;
var x210 >= 0, <= 0.17114392;
var x211 >= 0, <= 0.1603645;
var x212 >= 0, <= 0.1603645;
var x213 >= 0, <= 0.1603645;
var x214 >= 0, <= 0.18267189;
var x215 >= 0, <= 0.18267189;
var x216 >= 0, <= 0.18267189;
var x217 >= 0, <= 0.5323080366;
var x218 >= 0, <= 0.5323080366;
var x219 >= 0, <= 0.5323080366;
var x220 >= 0, <= 0.918715169866666;
var x221 >= 0, <= 0.918715169866666;
var x222 >= 0, <= 0.918715169866666;
var x223 >= 0, <= 1.021726146;
var x224 >= 0, <= 1.021726146;
var x225 >= 0, <= 1.021726146;
var x226 >= 0, <= 1.0706790744;
var x227 >= 0, <= 1.0706790744;
var x228 >= 0, <= 1.0706790744;
var x229 >= 0, <= 7.32543671346667;
var x230 >= 0, <= 7.32543671346667;
var x231 >= 0, <= 7.32543671346667;
var x232 >= 0, <= 15.2453990736;
var x233 >= 0, <= 15.2453990736;
var x234 >= 0, <= 15.2453990736;
var x235 >= 0, <= 1.28061192466667;
var x236 >= 0, <= 1.28061192466667;
var x237 >= 0, <= 1.28061192466667;
var x238 >= 0, <= 15.8815166933333;
var x239 >= 0, <= 15.8815166933333;
var x240 >= 0, <= 15.8815166933333;
var x241 >= 0, <= 15.2472806811333;
var x242 >= 0, <= 15.2472806811333;
var x243 >= 0, <= 15.2472806811333;
var x244 >= 0, <= 12.029055125;
var x245 >= 0, <= 12.029055125;
var x246 >= 0, <= 12.029055125;
var x247 >= 0, <= 15.9672360214667;
var x248 >= 0, <= 15.9672360214667;
var x249 >= 0, <= 15.9672360214667;
var x250 >= 0, <= 15.3736631157333;
var x251 >= 0, <= 15.3736631157333;
var x252 >= 0, <= 15.3736631157333;
var x253 >= 0, <= 6.2237284564;
var x254 >= 0, <= 6.2237284564;
var x255 >= 0, <= 6.2237284564;
var x256 >= 0, <= 8.85892556;
var x257 >= 0, <= 8.85892556;
var x258 >= 0, <= 8.85892556;
var x259 >= 0, <= 17.2437830768;
var x260 >= 0, <= 17.2437830768;
var x261 >= 0, <= 17.2437830768;
var b262 binary >= 0, <= 1;
var b263 binary >= 0, <= 1;
var b264 binary >= 0, <= 1;
var b265 binary >= 0, <= 1;
var b266 binary >= 0, <= 1;
var b267 binary >= 0, <= 1;
var b268 binary >= 0, <= 1;
var b269 binary >= 0, <= 1;
var b270 binary >= 0, <= 1;
var b271 binary >= 0, <= 1;
var b272 binary >= 0, <= 1;
var b273 binary >= 0, <= 1;
var b274 binary >= 0, <= 1;
var b275 binary >= 0, <= 1;
var b276 binary >= 0, <= 1;
var b277 binary >= 0, <= 1;
var b278 binary >= 0, <= 1;
var b279 binary >= 0, <= 1;
var b280 binary >= 0, <= 1;
var b281 binary >= 0, <= 1;
var b282 binary >= 0, <= 1;
var b283 binary >= 0, <= 1;
var b284 binary >= 0, <= 1;
var b285 binary >= 0, <= 1;
var b286 binary >= 0, <= 1;
var b287 binary >= 0, <= 1;
var b288 binary >= 0, <= 1;
var b289 binary >= 0, <= 1;
var b290 binary >= 0, <= 1;
var b291 binary >= 0, <= 1;
var b292 binary >= 0, <= 1;
var b293 binary >= 0, <= 1;
var b294 binary >= 0, <= 1;
var b295 binary >= 0, <= 1;
var b296 binary >= 0, <= 1;
var b297 binary >= 0, <= 1;
var b298 binary >= 0, <= 1;
var b299 binary >= 0, <= 1;
var b300 binary >= 0, <= 1;
var b301 binary >= 0, <= 1;
var b302 binary >= 0, <= 1;
var b303 binary >= 0, <= 1;
var b304 binary >= 0, <= 1;
var b305 binary >= 0, <= 1;
var b306 binary >= 0, <= 1;
var b307 binary >= 0, <= 1;
var b308 binary >= 0, <= 1;
var b309 binary >= 0, <= 1;
var b310 binary >= 0, <= 1;
var b311 binary >= 0, <= 1;
var b312 binary >= 0, <= 1;
var b313 binary >= 0, <= 1;
var b314 binary >= 0, <= 1;
var b315 binary >= 0, <= 1;
var b316 binary >= 0, <= 1;
var b317 binary >= 0, <= 1;
var b318 binary >= 0, <= 1;
var b319 binary >= 0, <= 1;
var b320 binary >= 0, <= 1;
var b321 binary >= 0, <= 1;
var b322 binary >= 0, <= 1;
var b323 binary >= 0, <= 1;

minimize obj:    x106 + x107 + x108 + x109 + x110 + x111 + x112 + x113 + x114
     + x115 + x116 + x117 + x118 + x119 + x120;

subject to

e2: -x46*x1*b61 + x217 >= 0;

e3: -x46*x2*b62 + x218 >= 0;

e4: -x46*x3*b63 + x219 >= 0;

e5: -x47*x4*b64 + x220 >= 0;

e6: -x47*x5*b65 + x221 >= 0;

e7: -x47*x6*b66 + x222 >= 0;

e8: -x48*x7*b67 + x223 >= 0;

e9: -x48*x8*b68 + x224 >= 0;

e10: -x48*x9*b69 + x225 >= 0;

e11: -x49*x10*b70 + x226 >= 0;

e12: -x49*x11*b71 + x227 >= 0;

e13: -x49*x12*b72 + x228 >= 0;

e14: -x50*x13*b73 + x229 >= 0;

e15: -x50*x14*b74 + x230 >= 0;

e16: -x50*x15*b75 + x231 >= 0;

e17: -x51*x16*b76 + x232 >= 0;

e18: -x51*x17*b77 + x233 >= 0;

e19: -x51*x18*b78 + x234 >= 0;

e20: -x52*x19*b79 + x235 >= 0;

e21: -x52*x20*b80 + x236 >= 0;

e22: -x52*x21*b81 + x237 >= 0;

e23: -x53*x22*b82 + x238 >= 0;

e24: -x53*x23*b83 + x239 >= 0;

e25: -x53*x24*b84 + x240 >= 0;

e26: -x54*x25*b85 + x241 >= 0;

e27: -x54*x26*b86 + x242 >= 0;

e28: -x54*x27*b87 + x243 >= 0;

e29: -x55*x28*b88 + x244 >= 0;

e30: -x55*x29*b89 + x245 >= 0;

e31: -x55*x30*b90 + x246 >= 0;

e32: -x56*x31*b91 + x247 >= 0;

e33: -x56*x32*b92 + x248 >= 0;

e34: -x56*x33*b93 + x249 >= 0;

e35: -x57*x34*b94 + x250 >= 0;

e36: -x57*x35*b95 + x251 >= 0;

e37: -x57*x36*b96 + x252 >= 0;

e38: -x58*x37*b97 + x253 >= 0;

e39: -x58*x38*b98 + x254 >= 0;

e40: -x58*x39*b99 + x255 >= 0;

e41: -x59*x40*b100 + x256 >= 0;

e42: -x59*x41*b101 + x257 >= 0;

e43: -x59*x42*b102 + x258 >= 0;

e44: -x60*x43*b103 + x259 >= 0;

e45: -x60*x44*b104 + x260 >= 0;

e46: -x60*x45*b105 + x261 >= 0;

e47:    b61 + b62 + b63 = 1;

e48:    b64 + b65 + b66 = 1;

e49:    b67 + b68 + b69 = 1;

e50:    b70 + b71 + b72 = 1;

e51:    b73 + b74 + b75 = 1;

e52:    b76 + b77 + b78 = 1;

e53:    b79 + b80 + b81 = 1;

e54:    b82 + b83 + b84 = 1;

e55:    b85 + b86 + b87 = 1;

e56:    b88 + b89 + b90 = 1;

e57:    b91 + b92 + b93 = 1;

e58:    b94 + b95 + b96 = 1;

e59:    b97 + b98 + b99 = 1;

e60:    b100 + b101 + b102 = 1;

e61:    b103 + b104 + b105 = 1;

e62:    2.02*b61 + 4.01333333333333*b64 + 4.76*b67 + 5.96*b70
      + 42.0933333333333*b73 + 99.28*b76 + 6.59333333333333*b79
      + 61.8666666666667*b82 + 56.2866666666667*b85 + 41.5*b88
      + 62.4933333333333*b91 + 80.9066666666667*b94 + 26.1466666666667*b97
      + 38*b100 + 62.24*b103 <= 213.053333333333;

e63:    2.02*b62 + 4.01333333333333*b65 + 4.76*b68 + 5.96*b71
      + 42.0933333333333*b74 + 99.28*b77 + 6.59333333333333*b80
      + 61.8666666666667*b83 + 56.2866666666667*b86 + 41.5*b89
      + 62.4933333333333*b92 + 80.9066666666667*b95 + 26.1466666666667*b98
      + 38*b101 + 62.24*b104 <= 213.053333333333;

e64:    2.02*b63 + 4.01333333333333*b66 + 4.76*b69 + 5.96*b72
      + 42.0933333333333*b75 + 99.28*b78 + 6.59333333333333*b81
      + 61.8666666666667*b84 + 56.2866666666667*b87 + 41.5*b90
      + 62.4933333333333*b93 + 80.9066666666667*b96 + 26.1466666666667*b99
      + 38*b102 + 62.24*b105 <= 213.053333333333;

e65:    x121 + x127 >= 0.29424122;

e66:    x122 + x128 >= 0.29424122;

e67:    x123 + x129 >= 0.29424122;

e68:    x121 + x130 >= 0.29760193;

e69:    x122 + x131 >= 0.29760193;

e70:    x123 + x132 >= 0.29760193;

e71:    x121 + x133 >= 0.35149534;

e72:    x122 + x134 >= 0.35149534;

e73:    x123 + x135 >= 0.35149534;

e74:    x121 + x136 >= 0.30458283;

e75:    x122 + x137 >= 0.30458283;

e76:    x123 + x138 >= 0.30458283;

e77:    x121 + x139 >= 0.29951066;

e78:    x122 + x140 >= 0.29951066;

e79:    x123 + x141 >= 0.29951066;

e80:    x121 + x142 >= 0.30694357;

e81:    x122 + x143 >= 0.30694357;

e82:    x123 + x144 >= 0.30694357;

e83:    x121 + x145 >= 0.33520661;

e84:    x122 + x146 >= 0.33520661;

e85:    x123 + x147 >= 0.33520661;

e86:    x121 + x148 >= 0.3400071;

e87:    x122 + x149 >= 0.3400071;

e88:    x123 + x150 >= 0.3400071;

e89:    x121 + x151 >= 0.35227087;

e90:    x122 + x152 >= 0.35227087;

e91:    x123 + x153 >= 0.35227087;

e92:    x121 + x154 >= 0.34225726;

e93:    x122 + x155 >= 0.34225726;

e94:    x123 + x156 >= 0.34225726;

e95:    x121 + x157 >= 0.32776566;

e96:    x122 + x158 >= 0.32776566;

e97:    x123 + x159 >= 0.32776566;

e98:    x121 + x160 >= 0.30438256;

e99:    x122 + x161 >= 0.30438256;

e100:    x123 + x162 >= 0.30438256;

e101:    x121 + x163 >= 0.28538336;

e102:    x122 + x164 >= 0.28538336;

e103:    x123 + x165 >= 0.28538336;

e104:    x121 + x166 >= 0.27950575;

e105:    x122 + x167 >= 0.27950575;

e106:    x123 + x168 >= 0.27950575;

e107:  - x121 + x127 >= -0.29424122;

e108:  - x122 + x128 >= -0.29424122;

e109:  - x123 + x129 >= -0.29424122;

e110:  - x121 + x130 >= -0.29760193;

e111:  - x122 + x131 >= -0.29760193;

e112:  - x123 + x132 >= -0.29760193;

e113:  - x121 + x133 >= -0.35149534;

e114:  - x122 + x134 >= -0.35149534;

e115:  - x123 + x135 >= -0.35149534;

e116:  - x121 + x136 >= -0.30458283;

e117:  - x122 + x137 >= -0.30458283;

e118:  - x123 + x138 >= -0.30458283;

e119:  - x121 + x139 >= -0.29951066;

e120:  - x122 + x140 >= -0.29951066;

e121:  - x123 + x141 >= -0.29951066;

e122:  - x121 + x142 >= -0.30694357;

e123:  - x122 + x143 >= -0.30694357;

e124:  - x123 + x144 >= -0.30694357;

e125:  - x121 + x145 >= -0.33520661;

e126:  - x122 + x146 >= -0.33520661;

e127:  - x123 + x147 >= -0.33520661;

e128:  - x121 + x148 >= -0.3400071;

e129:  - x122 + x149 >= -0.3400071;

e130:  - x123 + x150 >= -0.3400071;

e131:  - x121 + x154 >= -0.34225726;

e132:  - x122 + x155 >= -0.34225726;

e133:  - x123 + x156 >= -0.34225726;

e134:  - x121 + x157 >= -0.32776566;

e135:  - x122 + x158 >= -0.32776566;

e136:  - x123 + x159 >= -0.32776566;

e137:  - x121 + x160 >= -0.30438256;

e138:  - x122 + x161 >= -0.30438256;

e139:  - x123 + x162 >= -0.30438256;

e140:  - x121 + x163 >= -0.28538336;

e141:  - x122 + x164 >= -0.28538336;

e142:  - x123 + x165 >= -0.28538336;

e143:  - x121 + x166 >= -0.27950575;

e144:  - x122 + x167 >= -0.27950575;

e145:  - x123 + x168 >= -0.27950575;

e146:  - x121 + x169 >= -0.25788969;

e147:  - x122 + x170 >= -0.25788969;

e148:  - x123 + x171 >= -0.25788969;

e149:    x124 + x175 >= -0.9536939;

e150:    x125 + x176 >= -0.9536939;

e151:    x126 + x177 >= -0.9536939;

e152:    x124 + x178 >= -0.9004898;

e153:    x125 + x179 >= -0.9004898;

e154:    x126 + x180 >= -0.9004898;

e155:    x124 + x181 >= -0.9114032;

e156:    x125 + x182 >= -0.9114032;

e157:    x126 + x183 >= -0.9114032;

e158:    x124 + x184 >= -0.90071532;

e159:    x125 + x185 >= -0.90071532;

e160:    x126 + x186 >= -0.90071532;

e161:    x124 + x187 >= -0.88043054;

e162:    x125 + x188 >= -0.88043054;

e163:    x126 + x189 >= -0.88043054;

e164:    x124 + x190 >= -0.8680249;

e165:    x125 + x191 >= -0.8680249;

e166:    x126 + x192 >= -0.8680249;

e167:    x124 + x193 >= -0.81034814;

e168:    x125 + x194 >= -0.81034814;

e169:    x126 + x195 >= -0.81034814;

e170:    x124 + x196 >= -0.80843127;

e171:    x125 + x197 >= -0.80843127;

e172:    x126 + x198 >= -0.80843127;

e173:    x124 + x199 >= -0.7794471;

e174:    x125 + x200 >= -0.7794471;

e175:    x126 + x201 >= -0.7794471;

e176:    x124 + x202 >= -0.79930922;

e177:    x125 + x203 >= -0.79930922;

e178:    x126 + x204 >= -0.79930922;

e179:    x124 + x205 >= -0.84280733;

e180:    x125 + x206 >= -0.84280733;

e181:    x126 + x207 >= -0.84280733;

e182:    x124 + x208 >= -0.81379236;

e183:    x125 + x209 >= -0.81379236;

e184:    x126 + x210 >= -0.81379236;

e185:    x124 + x211 >= -0.82457178;

e186:    x125 + x212 >= -0.82457178;

e187:    x126 + x213 >= -0.82457178;

e188:    x124 + x214 >= -0.80226439;

e189:    x125 + x215 >= -0.80226439;

e190:    x126 + x216 >= -0.80226439;

e191:  - x124 + x172 >= 0.98493628;

e192:  - x125 + x173 >= 0.98493628;

e193:  - x126 + x174 >= 0.98493628;

e194:  - x124 + x175 >= 0.9536939;

e195:  - x125 + x176 >= 0.9536939;

e196:  - x126 + x177 >= 0.9536939;

e197:  - x124 + x178 >= 0.9004898;

e198:  - x125 + x179 >= 0.9004898;

e199:  - x126 + x180 >= 0.9004898;

e200:  - x124 + x181 >= 0.9114032;

e201:  - x125 + x182 >= 0.9114032;

e202:  - x126 + x183 >= 0.9114032;

e203:  - x124 + x184 >= 0.90071532;

e204:  - x125 + x185 >= 0.90071532;

e205:  - x126 + x186 >= 0.90071532;

e206:  - x124 + x187 >= 0.88043054;

e207:  - x125 + x188 >= 0.88043054;

e208:  - x126 + x189 >= 0.88043054;

e209:  - x124 + x190 >= 0.8680249;

e210:  - x125 + x191 >= 0.8680249;

e211:  - x126 + x192 >= 0.8680249;

e212:  - x124 + x193 >= 0.81034814;

e213:  - x125 + x194 >= 0.81034814;

e214:  - x126 + x195 >= 0.81034814;

e215:  - x124 + x196 >= 0.80843127;

e216:  - x125 + x197 >= 0.80843127;

e217:  - x126 + x198 >= 0.80843127;

e218:  - x124 + x202 >= 0.79930922;

e219:  - x125 + x203 >= 0.79930922;

e220:  - x126 + x204 >= 0.79930922;

e221:  - x124 + x205 >= 0.84280733;

e222:  - x125 + x206 >= 0.84280733;

e223:  - x126 + x207 >= 0.84280733;

e224:  - x124 + x208 >= 0.81379236;

e225:  - x125 + x209 >= 0.81379236;

e226:  - x126 + x210 >= 0.81379236;

e227:  - x124 + x211 >= 0.82457178;

e228:  - x125 + x212 >= 0.82457178;

e229:  - x126 + x213 >= 0.82457178;

e230:  - x124 + x214 >= 0.80226439;

e231:  - x125 + x215 >= 0.80226439;

e232:  - x126 + x216 >= 0.80226439;

e233:    x1 - x127 - x172 = 0;

e234:    x2 - x128 - x173 = 0;

e235:    x3 - x129 - x174 = 0;

e236:    x4 - x130 - x175 = 0;

e237:    x5 - x131 - x176 = 0;

e238:    x6 - x132 - x177 = 0;

e239:    x7 - x133 - x178 = 0;

e240:    x8 - x134 - x179 = 0;

e241:    x9 - x135 - x180 = 0;

e242:    x10 - x136 - x181 = 0;

e243:    x11 - x137 - x182 = 0;

e244:    x12 - x138 - x183 = 0;

e245:    x13 - x139 - x184 = 0;

e246:    x14 - x140 - x185 = 0;

e247:    x15 - x141 - x186 = 0;

e248:    x16 - x142 - x187 = 0;

e249:    x17 - x143 - x188 = 0;

e250:    x18 - x144 - x189 = 0;

e251:    x19 - x145 - x190 = 0;

e252:    x20 - x146 - x191 = 0;

e253:    x21 - x147 - x192 = 0;

e254:    x22 - x148 - x193 = 0;

e255:    x23 - x149 - x194 = 0;

e256:    x24 - x150 - x195 = 0;

e257:    x25 - x151 - x196 = 0;

e258:    x26 - x152 - x197 = 0;

e259:    x27 - x153 - x198 = 0;

e260:    x28 - x154 - x199 = 0;

e261:    x29 - x155 - x200 = 0;

e262:    x30 - x156 - x201 = 0;

e263:    x31 - x157 - x202 = 0;

e264:    x32 - x158 - x203 = 0;

e265:    x33 - x159 - x204 = 0;

e266:    x34 - x160 - x205 = 0;

e267:    x35 - x161 - x206 = 0;

e268:    x36 - x162 - x207 = 0;

e269:    x37 - x163 - x208 = 0;

e270:    x38 - x164 - x209 = 0;

e271:    x39 - x165 - x210 = 0;

e272:    x40 - x166 - x211 = 0;

e273:    x41 - x167 - x212 = 0;

e274:    x42 - x168 - x213 = 0;

e275:    x43 - x169 - x214 = 0;

e276:    x44 - x170 - x215 = 0;

e277:    x45 - x171 - x216 = 0;

e278:    b280 + b281 >= 1;

e279:    b277 + b282 >= 1;

e280:    b276 + b283 >= 1;

e281:    b275 + b286 >= 1;

e282:    b274 + b281 >= 1;

e283:    b274 + b279 + b282 >= 1;

e284:    b274 + b277 + b284 >= 1;

e285:    b274 + b276 + b285 >= 1;

e286:    b274 + b275 >= 1;

e287:    b273 + b281 >= 1;

e288:    b273 + b280 + b282 >= 1;

e289:    b273 + b279 + b283 >= 1;

e290:    b273 + b278 + b284 >= 1;

e291:    b273 + b277 + b285 >= 1;

e292:    b273 + b276 + b286 >= 1;

e293:    b273 + b275 >= 1;

e294:    b272 + b283 >= 1;

e295:    b272 + b280 + b284 >= 1;

e296:    b272 + b279 + b285 >= 1;

e297:    b272 + b278 + b286 >= 1;

e298:    b272 + b277 >= 1;

e299:    b271 + b286 >= 1;

e300:    b271 + b280 >= 1;

e301:    b270 + b281 >= 1;

e302:    b270 + b280 + b282 >= 1;

e303:    b270 + b278 + b283 >= 1;

e304:    b270 + b277 + b284 >= 1;

e305:    b270 + b276 + b286 >= 1;

e306:    b270 + b275 >= 1;

e307:    b270 + b274 + b282 >= 1;

e308:    b270 + b274 + b280 + b283 >= 1;

e309:    b270 + b274 + b279 + b284 >= 1;

e310:    b270 + b274 + b278 + b285 >= 1;

e311:    b270 + b274 + b277 + b286 >= 1;

e312:    b270 + b274 + b276 >= 1;

e313:    b270 + b273 + b284 >= 1;

e314:    b270 + b273 + b280 + b285 >= 1;

e315:    b270 + b273 + b279 + b286 >= 1;

e316:    b270 + b273 + b278 >= 1;

e317:    b270 + b272 + b286 >= 1;

e318:    b270 + b272 + b280 >= 1;

e319:    b270 + b271 >= 1;

e320:    b269 + b283 >= 1;

e321:    b269 + b280 + b284 >= 1;

e322:    b269 + b279 + b285 >= 1;

e323:    b269 + b278 + b286 >= 1;

e324:    b269 + b277 >= 1;

e325:    b269 + b274 + b285 >= 1;

e326:    b269 + b274 + b280 + b286 >= 1;

e327:    b269 + b274 + b279 >= 1;

e328:    b269 + b273 + b286 >= 1;

e329:    b269 + b273 + b280 >= 1;

e330:    b269 + b272 >= 1;

e331:    b268 + b286 >= 1;

e332:    b268 + b280 >= 1;

e333:    b268 + b274 >= 1;

e334:    b267 + b281 >= 1;

e335:    b267 + b280 + b282 >= 1;

e336:    b267 + b279 + b283 >= 1;

e337:    b267 + b278 + b284 >= 1;

e338:    b267 + b277 + b285 >= 1;

e339:    b267 + b276 + b286 >= 1;

e340:    b267 + b275 >= 1;

e341:    b267 + b274 + b282 >= 1;

e342:    b267 + b274 + b280 + b283 >= 1;

e343:    b267 + b274 + b279 + b284 >= 1;

e344:    b267 + b274 + b278 + b285 >= 1;

e345:    b267 + b274 + b277 + b286 >= 1;

e346:    b267 + b274 + b276 >= 1;

e347:    b267 + b273 + b284 >= 1;

e348:    b267 + b273 + b280 + b285 >= 1;

e349:    b267 + b273 + b279 + b286 >= 1;

e350:    b267 + b273 + b278 >= 1;

e351:    b267 + b272 + b286 >= 1;

e352:    b267 + b272 + b280 >= 1;

e353:    b267 + b271 >= 1;

e354:    b267 + b270 + b283 >= 1;

e355:    b267 + b270 + b280 + b284 >= 1;

e356:    b267 + b270 + b279 + b285 >= 1;

e357:    b267 + b270 + b278 + b286 >= 1;

e358:    b267 + b270 + b277 >= 1;

e359:    b267 + b270 + b274 + b284 >= 1;

e360:    b267 + b270 + b274 + b280 + b286 >= 1;

e361:    b267 + b270 + b274 + b278 >= 1;

e362:    b267 + b270 + b273 + b286 >= 1;

e363:    b267 + b270 + b273 + b280 >= 1;

e364:    b267 + b270 + b272 >= 1;

e365:    b267 + b269 + b286 >= 1;

e366:    b267 + b269 + b280 >= 1;

e367:    b267 + b269 + b274 >= 1;

e368:    b267 + b268 >= 1;

e369:    b266 + b283 >= 1;

e370:    b266 + b280 + b284 >= 1;

e371:    b266 + b279 + b285 >= 1;

e372:    b266 + b278 + b286 >= 1;

e373:    b266 + b277 >= 1;

e374:    b266 + b274 + b285 >= 1;

e375:    b266 + b274 + b280 + b286 >= 1;

e376:    b266 + b274 + b278 >= 1;

e377:    b266 + b273 + b286 >= 1;

e378:    b266 + b273 + b280 >= 1;

e379:    b266 + b272 >= 1;

e380:    b266 + b270 + b286 >= 1;

e381:    b266 + b270 + b279 >= 1;

e382:    b266 + b270 + b274 >= 1;

e383:    b266 + b269 >= 1;

e384:    b265 + b286 >= 1;

e385:    b265 + b280 >= 1;

e386:    b265 + b274 >= 1;

e387:    b265 + b270 >= 1;

e388:    b264 + b281 >= 1;

e389:    b264 + b279 + b282 >= 1;

e390:    b264 + b278 + b283 >= 1;

e391:    b264 + b277 + b284 >= 1;

e392:    b264 + b276 + b286 >= 1;

e393:    b264 + b275 >= 1;

e394:    b264 + b274 + b282 >= 1;

e395:    b264 + b274 + b280 + b283 >= 1;

e396:    b264 + b274 + b279 + b284 >= 1;

e397:    b264 + b274 + b278 + b285 >= 1;

e398:    b264 + b274 + b277 + b286 >= 1;

e399:    b264 + b274 + b276 >= 1;

e400:    b264 + b273 + b284 >= 1;

e401:    b264 + b273 + b280 + b285 >= 1;

e402:    b264 + b273 + b279 + b286 >= 1;

e403:    b264 + b273 + b278 >= 1;

e404:    b264 + b272 + b286 >= 1;

e405:    b264 + b272 + b279 >= 1;

e406:    b264 + b271 >= 1;

e407:    b264 + b270 + b283 >= 1;

e408:    b264 + b270 + b280 + b284 >= 1;

e409:    b264 + b270 + b279 + b285 >= 1;

e410:    b264 + b270 + b278 + b286 >= 1;

e411:    b264 + b270 + b277 >= 1;

e412:    b264 + b270 + b274 + b284 >= 1;

e413:    b264 + b270 + b274 + b280 + b285 >= 1;

e414:    b264 + b270 + b274 + b279 + b286 >= 1;

e415:    b264 + b270 + b274 + b278 >= 1;

e416:    b264 + b270 + b273 + b286 >= 1;

e417:    b264 + b270 + b273 + b280 >= 1;

e418:    b264 + b270 + b272 >= 1;

e419:    b264 + b269 + b286 >= 1;

e420:    b264 + b269 + b280 >= 1;

e421:    b264 + b269 + b274 >= 1;

e422:    b264 + b268 >= 1;

e423:    b264 + b267 + b283 >= 1;

e424:    b264 + b267 + b280 + b284 >= 1;

e425:    b264 + b267 + b279 + b285 >= 1;

e426:    b264 + b267 + b278 + b286 >= 1;

e427:    b264 + b267 + b277 >= 1;

e428:    b264 + b267 + b274 + b284 >= 1;

e429:    b264 + b267 + b274 + b280 + b286 >= 1;

e430:    b264 + b267 + b274 + b279 >= 1;

e431:    b264 + b267 + b273 + b286 >= 1;

e432:    b264 + b267 + b273 + b280 >= 1;

e433:    b264 + b267 + b272 >= 1;

e434:    b264 + b267 + b270 + b285 >= 1;

e435:    b264 + b267 + b270 + b280 + b286 >= 1;

e436:    b264 + b267 + b270 + b279 >= 1;

e437:    b264 + b267 + b270 + b274 >= 1;

e438:    b264 + b267 + b269 >= 1;

e439:    b264 + b266 + b286 >= 1;

e440:    b264 + b266 + b280 >= 1;

e441:    b264 + b266 + b274 >= 1;

e442:    b264 + b266 + b270 >= 1;

e443:    b264 + b265 >= 1;

e444:    b263 + b283 >= 1;

e445:    b263 + b280 + b284 >= 1;

e446:    b263 + b279 + b285 >= 1;

e447:    b263 + b278 + b286 >= 1;

e448:    b263 + b277 >= 1;

e449:    b263 + b274 + b285 >= 1;

e450:    b263 + b274 + b280 + b286 >= 1;

e451:    b263 + b274 + b279 >= 1;

e452:    b263 + b273 + b286 >= 1;

e453:    b263 + b273 + b280 >= 1;

e454:    b263 + b272 >= 1;

e455:    b263 + b270 + b286 >= 1;

e456:    b263 + b270 + b280 >= 1;

e457:    b263 + b270 + b274 >= 1;

e458:    b263 + b269 >= 1;

e459:    b263 + b267 + b286 >= 1;

e460:    b263 + b267 + b280 >= 1;

e461:    b263 + b267 + b274 >= 1;

e462:    b263 + b267 + b270 >= 1;

e463:    b263 + b266 >= 1;

e464:    b262 + b286 >= 1;

e465:    b262 + b280 >= 1;

e466:    b262 + b274 >= 1;

e467:    b262 + b270 >= 1;

e468:    b262 + b267 >= 1;

e469:    b286 + b295 >= 1;

e470:    b286 + b293 + b296 >= 1;

e471:    b286 + b292 + b297 >= 1;

e472:    b286 + b291 + b298 >= 1;

e473:    b286 + b290 >= 1;

e474:    b286 + b289 + b296 >= 1;

e475:    b286 + b289 + b294 + b297 >= 1;

e476:    b286 + b289 + b292 + b299 >= 1;

e477:    b286 + b289 + b291 >= 1;

e478:    b286 + b288 + b298 >= 1;

e479:    b286 + b288 + b294 + b299 >= 1;

e480:    b286 + b288 + b293 >= 1;

e481:    b286 + b287 >= 1;

e482:    b285 + b295 >= 1;

e483:    b285 + b293 + b296 >= 1;

e484:    b285 + b292 + b297 >= 1;

e485:    b285 + b291 + b298 >= 1;

e486:    b285 + b290 >= 1;

e487:    b285 + b289 + b296 >= 1;

e488:    b285 + b289 + b294 + b297 >= 1;

e489:    b285 + b289 + b293 + b298 >= 1;

e490:    b285 + b289 + b292 + b299 >= 1;

e491:    b285 + b289 + b291 >= 1;

e492:    b285 + b288 + b298 >= 1;

e493:    b285 + b288 + b294 + b299 >= 1;

e494:    b285 + b288 + b293 >= 1;

e495:    b285 + b287 >= 1;

e496:    b284 + b295 >= 1;

e497:    b284 + b294 + b296 >= 1;

e498:    b284 + b293 + b297 >= 1;

e499:    b284 + b292 + b298 >= 1;

e500:    b284 + b291 + b299 >= 1;

e501:    b284 + b290 >= 1;

e502:    b284 + b289 + b297 >= 1;

e503:    b284 + b289 + b294 + b298 >= 1;

e504:    b284 + b289 + b293 + b299 >= 1;

e505:    b284 + b289 + b292 >= 1;

e506:    b284 + b288 + b299 >= 1;

e507:    b284 + b288 + b294 >= 1;

e508:    b284 + b287 >= 1;

e509:    b283 + b296 >= 1;

e510:    b283 + b294 + b297 >= 1;

e511:    b283 + b293 + b298 >= 1;

e512:    b283 + b292 + b299 >= 1;

e513:    b283 + b291 >= 1;

e514:    b283 + b289 + b298 >= 1;

e515:    b283 + b289 + b294 + b299 >= 1;

e516:    b283 + b289 + b293 >= 1;

e517:    b283 + b288 >= 1;

e518:    b282 + b297 >= 1;

e519:    b282 + b294 + b298 >= 1;

e520:    b282 + b293 + b299 >= 1;

e521:    b282 + b292 >= 1;

e522:    b282 + b289 + b299 >= 1;

e523:    b282 + b289 + b294 >= 1;

e524:    b282 + b288 >= 1;

e525:    b281 + b299 >= 1;

e526:    b281 + b294 >= 1;

e527:    b281 + b289 >= 1;

e528:    b280 + b295 >= 1;

e529:    b280 + b293 + b296 >= 1;

e530:    b280 + b292 + b297 >= 1;

e531:    b280 + b290 >= 1;

e532:    b280 + b289 + b296 >= 1;

e533:    b280 + b289 + b294 + b297 >= 1;

e534:    b280 + b289 + b292 + b299 >= 1;

e535:    b280 + b289 + b291 >= 1;

e536:    b280 + b288 + b298 >= 1;

e537:    b280 + b288 + b294 + b299 >= 1;

e538:    b280 + b288 + b293 >= 1;

e539:    b280 + b287 >= 1;

e540:    b280 + b286 + b295 >= 1;

e541:    b280 + b286 + b293 + b296 >= 1;

e542:    b280 + b286 + b292 + b297 >= 1;

e543:    b280 + b286 + b291 + b299 >= 1;

e544:    b280 + b286 + b290 >= 1;

e545:    b280 + b286 + b289 + b296 >= 1;

e546:    b280 + b286 + b289 + b294 + b297 >= 1;

e547:    b280 + b286 + b289 + b293 + b298 >= 1;

e548:    b280 + b286 + b289 + b292 + b299 >= 1;

e549:    b280 + b286 + b289 + b291 >= 1;

e550:    b280 + b286 + b288 + b298 >= 1;

e551:    b280 + b286 + b288 + b294 + b299 >= 1;

e552:    b280 + b286 + b288 + b293 >= 1;

e553:    b280 + b286 + b287 >= 1;

e554:    b280 + b285 + b295 >= 1;

e555:    b280 + b285 + b294 + b296 >= 1;

e556:    b280 + b285 + b293 + b297 >= 1;

e557:    b280 + b285 + b292 + b298 >= 1;

e558:    b280 + b285 + b291 + b299 >= 1;

e559:    b280 + b285 + b290 >= 1;

e560:    b280 + b285 + b289 + b297 >= 1;

e561:    b280 + b285 + b289 + b294 + b298 >= 1;

e562:    b280 + b285 + b289 + b293 + b299 >= 1;

e563:    b280 + b285 + b289 + b292 >= 1;

e564:    b280 + b285 + b288 + b299 >= 1;

e565:    b280 + b285 + b288 + b294 >= 1;

e566:    b280 + b285 + b287 >= 1;

e567:    b280 + b284 + b296 >= 1;

e568:    b280 + b284 + b294 + b297 >= 1;

e569:    b280 + b284 + b293 + b298 >= 1;

e570:    b280 + b284 + b292 + b299 >= 1;

e571:    b280 + b284 + b291 >= 1;

e572:    b280 + b284 + b289 + b298 >= 1;

e573:    b280 + b284 + b289 + b294 + b299 >= 1;

e574:    b280 + b284 + b289 + b293 >= 1;

e575:    b280 + b284 + b288 >= 1;

e576:    b280 + b283 + b297 >= 1;

e577:    b280 + b283 + b294 + b298 >= 1;

e578:    b280 + b283 + b293 + b299 >= 1;

e579:    b280 + b283 + b292 >= 1;

e580:    b280 + b283 + b289 + b299 >= 1;

e581:    b280 + b283 + b289 + b294 >= 1;

e582:    b280 + b283 + b288 >= 1;

e583:    b280 + b282 + b298 >= 1;

e584:    b280 + b282 + b294 + b299 >= 1;

e585:    b280 + b282 + b293 >= 1;

e586:    b280 + b282 + b289 >= 1;

e587:    b279 + b295 >= 1;

e588:    b279 + b293 + b296 >= 1;

e589:    b279 + b292 + b297 >= 1;

e590:    b279 + b291 + b298 >= 1;

e591:    b279 + b290 >= 1;

e592:    b279 + b289 + b296 >= 1;

e593:    b279 + b289 + b294 + b297 >= 1;

e594:    b279 + b289 + b293 + b298 >= 1;

e595:    b279 + b289 + b292 + b299 >= 1;

e596:    b279 + b289 + b291 >= 1;

e597:    b279 + b288 + b298 >= 1;

e598:    b279 + b288 + b294 + b299 >= 1;

e599:    b279 + b288 + b293 >= 1;

e600:    b279 + b287 >= 1;

e601:    b279 + b286 + b295 >= 1;

e602:    b279 + b286 + b294 + b296 >= 1;

e603:    b279 + b286 + b293 + b297 >= 1;

e604:    b279 + b286 + b292 + b298 >= 1;

e605:    b279 + b286 + b291 + b299 >= 1;

e606:    b279 + b286 + b290 >= 1;

e607:    b279 + b286 + b289 + b297 >= 1;

e608:    b279 + b286 + b289 + b294 + b298 >= 1;

e609:    b279 + b286 + b289 + b293 + b299 >= 1;

e610:    b279 + b286 + b289 + b292 >= 1;

e611:    b279 + b286 + b288 + b299 >= 1;

e612:    b279 + b286 + b288 + b294 >= 1;

e613:    b279 + b286 + b287 >= 1;

e614:    b279 + b285 + b296 >= 1;

e615:    b279 + b285 + b294 + b297 >= 1;

e616:    b279 + b285 + b293 + b298 >= 1;

e617:    b279 + b285 + b292 + b299 >= 1;

e618:    b279 + b285 + b291 >= 1;

e619:    b279 + b285 + b289 + b298 >= 1;

e620:    b279 + b285 + b289 + b294 + b299 >= 1;

e621:    b279 + b285 + b289 + b293 >= 1;

e622:    b279 + b285 + b288 >= 1;

e623:    b279 + b284 + b297 >= 1;

e624:    b279 + b284 + b294 + b298 >= 1;

e625:    b279 + b284 + b293 + b299 >= 1;

e626:    b279 + b284 + b292 >= 1;

e627:    b279 + b284 + b289 + b299 >= 1;

e628:    b279 + b284 + b289 + b294 >= 1;

e629:    b279 + b284 + b288 >= 1;

e630:    b279 + b283 + b297 >= 1;

e631:    b279 + b283 + b294 + b299 >= 1;

e632:    b279 + b283 + b293 >= 1;

e633:    b279 + b283 + b289 >= 1;

e634:    b279 + b282 + b298 >= 1;

e635:    b279 + b282 + b294 + b299 >= 1;

e636:    b279 + b282 + b293 >= 1;

e637:    b279 + b282 + b289 >= 1;

e638:    b278 + b295 >= 1;

e639:    b278 + b294 + b296 >= 1;

e640:    b278 + b293 + b297 >= 1;

e641:    b278 + b292 + b298 >= 1;

e642:    b278 + b291 + b299 >= 1;

e643:    b278 + b290 >= 1;

e644:    b278 + b289 + b297 >= 1;

e645:    b278 + b289 + b294 + b298 >= 1;

e646:    b278 + b289 + b293 + b299 >= 1;

e647:    b278 + b289 + b292 >= 1;

e648:    b278 + b288 + b299 >= 1;

e649:    b278 + b288 + b294 >= 1;

e650:    b278 + b287 >= 1;

e651:    b278 + b286 + b296 >= 1;

e652:    b278 + b286 + b294 + b297 >= 1;

e653:    b278 + b286 + b293 + b298 >= 1;

e654:    b278 + b286 + b292 + b299 >= 1;

e655:    b278 + b286 + b291 >= 1;

e656:    b278 + b286 + b289 + b298 >= 1;

e657:    b278 + b286 + b289 + b294 + b299 >= 1;

e658:    b278 + b286 + b289 + b293 >= 1;

e659:    b278 + b286 + b288 >= 1;

e660:    b278 + b285 + b297 >= 1;

e661:    b278 + b285 + b294 + b298 >= 1;

e662:    b278 + b285 + b293 + b299 >= 1;

e663:    b278 + b285 + b292 >= 1;

e664:    b278 + b285 + b289 + b299 >= 1;

e665:    b278 + b285 + b289 + b294 >= 1;

e666:    b278 + b285 + b288 >= 1;

e667:    b278 + b284 + b297 >= 1;

e668:    b278 + b284 + b294 + b298 >= 1;

e669:    b278 + b284 + b293 + b299 >= 1;

e670:    b278 + b284 + b292 >= 1;

e671:    b278 + b284 + b289 + b299 >= 1;

e672:    b278 + b284 + b289 + b294 >= 1;

e673:    b278 + b284 + b288 >= 1;

e674:    b278 + b283 + b298 >= 1;

e675:    b278 + b283 + b294 + b299 >= 1;

e676:    b278 + b283 + b293 >= 1;

e677:    b278 + b283 + b289 >= 1;

e678:    b278 + b282 + b299 >= 1;

e679:    b278 + b282 + b294 >= 1;

e680:    b278 + b282 + b289 >= 1;

e681:    b277 + b296 >= 1;

e682:    b277 + b294 + b297 >= 1;

e683:    b277 + b293 + b298 >= 1;

e684:    b277 + b292 + b299 >= 1;

e685:    b277 + b291 >= 1;

e686:    b277 + b289 + b298 >= 1;

e687:    b277 + b289 + b294 + b299 >= 1;

e688:    b277 + b289 + b293 >= 1;

e689:    b277 + b288 >= 1;

e690:    b277 + b286 + b297 >= 1;

e691:    b277 + b286 + b294 + b298 >= 1;

e692:    b277 + b286 + b293 + b299 >= 1;

e693:    b277 + b286 + b292 >= 1;

e694:    b277 + b286 + b289 + b299 >= 1;

e695:    b277 + b286 + b289 + b294 >= 1;

e696:    b277 + b286 + b288 >= 1;

e697:    b277 + b285 + b297 >= 1;

e698:    b277 + b285 + b294 + b298 >= 1;

e699:    b277 + b285 + b293 >= 1;

e700:    b277 + b285 + b289 + b299 >= 1;

e701:    b277 + b285 + b289 + b294 >= 1;

e702:    b277 + b285 + b288 >= 1;

e703:    b277 + b284 + b298 >= 1;

e704:    b277 + b284 + b294 + b299 >= 1;

e705:    b277 + b284 + b293 >= 1;

e706:    b277 + b284 + b289 >= 1;

e707:    b277 + b283 + b299 >= 1;

e708:    b277 + b283 + b294 >= 1;

e709:    b277 + b283 + b289 >= 1;

e710:    b276 + b297 >= 1;

e711:    b276 + b294 + b298 >= 1;

e712:    b276 + b293 + b299 >= 1;

e713:    b276 + b292 >= 1;

e714:    b276 + b289 + b299 >= 1;

e715:    b276 + b289 + b294 >= 1;

e716:    b276 + b288 >= 1;

e717:    b276 + b286 + b297 >= 1;

e718:    b276 + b286 + b294 + b299 >= 1;

e719:    b276 + b286 + b293 >= 1;

e720:    b276 + b286 + b289 >= 1;

e721:    b276 + b285 + b298 >= 1;

e722:    b276 + b285 + b294 + b299 >= 1;

e723:    b276 + b285 + b293 >= 1;

e724:    b276 + b285 + b289 >= 1;

e725:    b276 + b284 + b299 >= 1;

e726:    b276 + b284 + b294 >= 1;

e727:    b276 + b284 + b289 >= 1;

e728:    b275 + b299 >= 1;

e729:    b275 + b294 >= 1;

e730:    b275 + b289 >= 1;

e731:    b274 + b295 >= 1;

e732:    b274 + b293 + b296 >= 1;

e733:    b274 + b292 + b297 >= 1;

e734:    b274 + b291 + b298 >= 1;

e735:    b274 + b290 >= 1;

e736:    b274 + b289 + b296 >= 1;

e737:    b274 + b289 + b294 + b297 >= 1;

e738:    b274 + b289 + b293 + b298 >= 1;

e739:    b274 + b289 + b292 + b299 >= 1;

e740:    b274 + b289 + b291 >= 1;

e741:    b274 + b288 + b298 >= 1;

e742:    b274 + b288 + b294 + b299 >= 1;

e743:    b274 + b288 + b293 >= 1;

e744:    b274 + b287 >= 1;

e745:    b274 + b286 + b295 >= 1;

e746:    b274 + b286 + b294 + b296 >= 1;

e747:    b274 + b286 + b293 + b297 >= 1;

e748:    b274 + b286 + b292 + b298 >= 1;

e749:    b274 + b286 + b291 + b299 >= 1;

e750:    b274 + b286 + b290 >= 1;

e751:    b274 + b286 + b289 + b297 >= 1;

e752:    b274 + b286 + b289 + b294 + b298 >= 1;

e753:    b274 + b286 + b289 + b293 + b299 >= 1;

e754:    b274 + b286 + b289 + b292 >= 1;

e755:    b274 + b286 + b288 + b299 >= 1;

e756:    b274 + b286 + b288 + b294 >= 1;

e757:    b274 + b286 + b287 >= 1;

e758:    b274 + b285 + b296 >= 1;

e759:    b274 + b285 + b293 + b297 >= 1;

e760:    b274 + b285 + b292 + b299 >= 1;

e761:    b274 + b285 + b291 >= 1;

e762:    b274 + b285 + b289 + b297 >= 1;

e763:    b274 + b285 + b289 + b294 + b298 >= 1;

e764:    b274 + b285 + b289 + b293 + b299 >= 1;

e765:    b274 + b285 + b289 + b292 >= 1;

e766:    b274 + b285 + b288 + b299 >= 1;

e767:    b274 + b285 + b288 + b294 >= 1;

e768:    b274 + b285 + b287 >= 1;

e769:    b274 + b284 + b296 >= 1;

e770:    b274 + b284 + b294 + b297 >= 1;

e771:    b274 + b284 + b293 + b298 >= 1;

e772:    b274 + b284 + b292 + b299 >= 1;

e773:    b274 + b284 + b291 >= 1;

e774:    b274 + b284 + b289 + b298 >= 1;

e775:    b274 + b284 + b289 + b294 + b299 >= 1;

e776:    b274 + b284 + b289 + b293 >= 1;

e777:    b274 + b284 + b288 >= 1;

e778:    b274 + b283 + b297 >= 1;

e779:    b274 + b283 + b294 + b298 >= 1;

e780:    b274 + b283 + b293 + b299 >= 1;

e781:    b274 + b283 + b292 >= 1;

e782:    b274 + b283 + b289 + b299 >= 1;

e783:    b274 + b283 + b289 + b294 >= 1;

e784:    b274 + b283 + b288 >= 1;

e785:    b274 + b282 + b298 >= 1;

e786:    b274 + b282 + b294 + b299 >= 1;

e787:    b274 + b282 + b293 >= 1;

e788:    b274 + b282 + b289 >= 1;

e789:    b274 + b280 + b295 >= 1;

e790:    b274 + b280 + b294 + b296 >= 1;

e791:    b274 + b280 + b293 + b297 >= 1;

e792:    b274 + b280 + b292 + b298 >= 1;

e793:    b274 + b280 + b291 + b299 >= 1;

e794:    b274 + b280 + b290 >= 1;

e795:    b274 + b280 + b289 + b297 >= 1;

e796:    b274 + b280 + b289 + b294 + b298 >= 1;

e797:    b274 + b280 + b289 + b293 + b299 >= 1;

e798:    b274 + b280 + b289 + b292 >= 1;

e799:    b274 + b280 + b288 + b299 >= 1;

e800:    b274 + b280 + b288 + b294 >= 1;

e801:    b274 + b280 + b287 >= 1;

e802:    b274 + b280 + b286 + b296 >= 1;

e803:    b274 + b280 + b286 + b294 + b297 >= 1;

e804:    b274 + b280 + b286 + b293 + b298 >= 1;

e805:    b274 + b280 + b286 + b292 + b299 >= 1;

e806:    b274 + b280 + b286 + b291 >= 1;

e807:    b274 + b280 + b286 + b289 + b298 >= 1;

e808:    b274 + b280 + b286 + b289 + b294 + b299 >= 1;

e809:    b274 + b280 + b286 + b289 + b293 >= 1;

e810:    b274 + b280 + b286 + b288 >= 1;

e811:    b274 + b280 + b285 + b296 >= 1;

e812:    b274 + b280 + b285 + b294 + b297 >= 1;

e813:    b274 + b280 + b285 + b293 + b298 >= 1;

e814:    b274 + b280 + b285 + b292 + b299 >= 1;

e815:    b274 + b280 + b285 + b291 >= 1;

e816:    b274 + b280 + b285 + b289 + b298 >= 1;

e817:    b274 + b280 + b285 + b289 + b294 + b299 >= 1;

e818:    b274 + b280 + b285 + b289 + b293 >= 1;

e819:    b274 + b280 + b285 + b288 >= 1;

e820:    b274 + b280 + b284 + b297 >= 1;

e821:    b274 + b280 + b284 + b294 + b298 >= 1;

e822:    b274 + b280 + b284 + b293 + b299 >= 1;

e823:    b274 + b280 + b284 + b292 >= 1;

e824:    b274 + b280 + b284 + b289 + b299 >= 1;

e825:    b274 + b280 + b284 + b289 + b294 >= 1;

e826:    b274 + b280 + b284 + b288 >= 1;

e827:    b274 + b280 + b283 + b298 >= 1;

e828:    b274 + b280 + b283 + b294 + b299 >= 1;

e829:    b274 + b280 + b283 + b293 >= 1;

e830:    b274 + b280 + b283 + b289 >= 1;

e831:    b274 + b280 + b282 + b299 >= 1;

e832:    b274 + b280 + b282 + b294 >= 1;

e833:    b274 + b280 + b282 + b289 >= 1;

e834:    b274 + b279 + b295 >= 1;

e835:    b274 + b279 + b294 + b296 >= 1;

e836:    b274 + b279 + b293 + b297 >= 1;

e837:    b274 + b279 + b292 + b299 >= 1;

e838:    b274 + b279 + b291 >= 1;

e839:    b274 + b279 + b289 + b297 >= 1;

e840:    b274 + b279 + b289 + b294 + b298 >= 1;

e841:    b274 + b279 + b289 + b293 + b299 >= 1;

e842:    b274 + b279 + b289 + b292 >= 1;

e843:    b274 + b279 + b288 >= 1;

e844:    b274 + b279 + b286 + b296 >= 1;

e845:    b274 + b279 + b286 + b294 + b297 >= 1;

e846:    b274 + b279 + b286 + b293 + b298 >= 1;

e847:    b274 + b279 + b286 + b292 + b299 >= 1;

e848:    b274 + b279 + b286 + b291 >= 1;

e849:    b274 + b279 + b286 + b289 + b298 >= 1;

e850:    b274 + b279 + b286 + b289 + b294 + b299 >= 1;

e851:    b274 + b279 + b286 + b289 + b293 >= 1;

e852:    b274 + b279 + b286 + b288 >= 1;

e853:    b274 + b279 + b285 + b297 >= 1;

e854:    b274 + b279 + b285 + b294 + b298 >= 1;

e855:    b274 + b279 + b285 + b293 + b299 >= 1;

e856:    b274 + b279 + b285 + b292 >= 1;

e857:    b274 + b279 + b285 + b289 + b299 >= 1;

e858:    b274 + b279 + b285 + b289 + b294 >= 1;

e859:    b274 + b279 + b285 + b288 >= 1;

e860:    b274 + b279 + b284 + b298 >= 1;

e861:    b274 + b279 + b284 + b294 + b299 >= 1;

e862:    b274 + b279 + b284 + b293 >= 1;

e863:    b274 + b279 + b284 + b289 >= 1;

e864:    b274 + b279 + b283 + b299 >= 1;

e865:    b274 + b279 + b283 + b294 >= 1;

e866:    b274 + b279 + b283 + b289 >= 1;

e867:    b274 + b278 + b296 >= 1;

e868:    b274 + b278 + b294 + b297 >= 1;

e869:    b274 + b278 + b293 + b298 >= 1;

e870:    b274 + b278 + b292 + b299 >= 1;

e871:    b274 + b278 + b291 >= 1;

e872:    b274 + b278 + b289 + b298 >= 1;

e873:    b274 + b278 + b289 + b294 + b299 >= 1;

e874:    b274 + b278 + b289 + b293 >= 1;

e875:    b274 + b278 + b288 >= 1;

e876:    b274 + b278 + b286 + b297 >= 1;

e877:    b274 + b278 + b286 + b294 + b298 >= 1;

e878:    b274 + b278 + b286 + b293 + b299 >= 1;

e879:    b274 + b278 + b286 + b292 >= 1;

e880:    b274 + b278 + b286 + b289 + b299 >= 1;

e881:    b274 + b278 + b286 + b289 + b294 >= 1;

e882:    b274 + b278 + b286 + b288 >= 1;

e883:    b274 + b278 + b285 + b298 >= 1;

e884:    b274 + b278 + b285 + b294 + b299 >= 1;

e885:    b274 + b278 + b285 + b293 >= 1;

e886:    b274 + b278 + b285 + b289 >= 1;

e887:    b274 + b278 + b284 + b299 >= 1;

e888:    b274 + b278 + b284 + b294 >= 1;

e889:    b274 + b278 + b284 + b289 >= 1;

e890:    b274 + b278 + b283 + b299 >= 1;

e891:    b274 + b278 + b283 + b294 >= 1;

e892:    b274 + b278 + b283 + b289 >= 1;

e893:    b274 + b277 + b297 >= 1;

e894:    b274 + b277 + b294 + b298 >= 1;

e895:    b274 + b277 + b293 + b299 >= 1;

e896:    b274 + b277 + b292 >= 1;

e897:    b274 + b277 + b289 + b299 >= 1;

e898:    b274 + b277 + b289 + b294 >= 1;

e899:    b274 + b277 + b288 >= 1;

e900:    b274 + b277 + b286 + b298 >= 1;

e901:    b274 + b277 + b286 + b294 + b299 >= 1;

e902:    b274 + b277 + b286 + b293 >= 1;

e903:    b274 + b277 + b286 + b289 >= 1;

e904:    b274 + b277 + b285 + b299 >= 1;

e905:    b274 + b277 + b285 + b294 >= 1;

e906:    b274 + b277 + b285 + b289 >= 1;

e907:    b274 + b276 + b298 >= 1;

e908:    b274 + b276 + b294 + b299 >= 1;

e909:    b274 + b276 + b293 >= 1;

e910:    b274 + b276 + b289 >= 1;

e911:    b274 + b276 + b286 + b299 >= 1;

e912:    b274 + b276 + b286 + b294 >= 1;

e913:    b274 + b276 + b286 + b289 >= 1;

e914:    b273 + b295 >= 1;

e915:    b273 + b294 + b296 >= 1;

e916:    b273 + b293 + b297 >= 1;

e917:    b273 + b292 + b298 >= 1;

e918:    b273 + b291 + b299 >= 1;

e919:    b273 + b290 >= 1;

e920:    b273 + b289 + b297 >= 1;

e921:    b273 + b289 + b294 + b298 >= 1;

e922:    b273 + b289 + b293 + b299 >= 1;

e923:    b273 + b289 + b292 >= 1;

e924:    b273 + b288 + b299 >= 1;

e925:    b273 + b288 + b294 >= 1;

e926:    b273 + b287 >= 1;

e927:    b273 + b286 + b296 >= 1;

e928:    b273 + b286 + b294 + b297 >= 1;

e929:    b273 + b286 + b293 + b298 >= 1;

e930:    b273 + b286 + b292 + b299 >= 1;

e931:    b273 + b286 + b291 >= 1;

e932:    b273 + b286 + b289 + b298 >= 1;

e933:    b273 + b286 + b289 + b294 + b299 >= 1;

e934:    b273 + b286 + b289 + b293 >= 1;

e935:    b273 + b286 + b288 >= 1;

e936:    b273 + b285 + b297 >= 1;

e937:    b273 + b285 + b294 + b298 >= 1;

e938:    b273 + b285 + b293 + b299 >= 1;

e939:    b273 + b285 + b292 >= 1;

e940:    b273 + b285 + b289 + b299 >= 1;

e941:    b273 + b285 + b289 + b294 >= 1;

e942:    b273 + b285 + b288 >= 1;

e943:    b273 + b284 + b298 >= 1;

e944:    b273 + b284 + b294 + b299 >= 1;

e945:    b273 + b284 + b293 >= 1;

e946:    b273 + b284 + b289 >= 1;

e947:    b273 + b283 + b299 >= 1;

e948:    b273 + b283 + b294 >= 1;

e949:    b273 + b283 + b289 >= 1;

e950:    b273 + b282 + b299 >= 1;

e951:    b273 + b282 + b294 >= 1;

e952:    b273 + b282 + b289 >= 1;

e953:    b273 + b280 + b296 >= 1;

e954:    b273 + b280 + b294 + b297 >= 1;

e955:    b273 + b280 + b293 + b298 >= 1;

e956:    b273 + b280 + b292 + b299 >= 1;

e957:    b273 + b280 + b291 >= 1;

e958:    b273 + b280 + b289 + b298 >= 1;

e959:    b273 + b280 + b289 + b294 + b299 >= 1;

e960:    b273 + b280 + b289 + b293 >= 1;

e961:    b273 + b280 + b288 >= 1;

e962:    b273 + b280 + b286 + b297 >= 1;

e963:    b273 + b280 + b286 + b294 + b298 >= 1;

e964:    b273 + b280 + b286 + b293 + b299 >= 1;

e965:    b273 + b280 + b286 + b292 >= 1;

e966:    b273 + b280 + b286 + b289 + b299 >= 1;

e967:    b273 + b280 + b286 + b289 + b294 >= 1;

e968:    b273 + b280 + b286 + b288 >= 1;

e969:    b273 + b280 + b285 + b298 >= 1;

e970:    b273 + b280 + b285 + b294 + b299 >= 1;

e971:    b273 + b280 + b285 + b293 >= 1;

e972:    b273 + b280 + b285 + b289 >= 1;

e973:    b273 + b280 + b284 + b299 >= 1;

e974:    b273 + b280 + b284 + b294 >= 1;

e975:    b273 + b280 + b284 + b289 >= 1;

e976:    b273 + b280 + b283 + b299 >= 1;

e977:    b273 + b280 + b283 + b294 >= 1;

e978:    b273 + b280 + b283 + b289 >= 1;

e979:    b273 + b279 + b297 >= 1;

e980:    b273 + b279 + b294 + b298 >= 1;

e981:    b273 + b279 + b293 + b299 >= 1;

e982:    b273 + b279 + b292 >= 1;

e983:    b273 + b279 + b289 + b299 >= 1;

e984:    b273 + b279 + b289 + b294 >= 1;

e985:    b273 + b279 + b288 >= 1;

e986:    b273 + b279 + b286 + b298 >= 1;

e987:    b273 + b279 + b286 + b294 + b299 >= 1;

e988:    b273 + b279 + b286 + b293 >= 1;

e989:    b273 + b279 + b286 + b289 >= 1;

e990:    b273 + b279 + b285 + b299 >= 1;

e991:    b273 + b279 + b285 + b293 >= 1;

e992:    b273 + b279 + b285 + b289 >= 1;

e993:    b273 + b279 + b284 + b299 >= 1;

e994:    b273 + b279 + b284 + b294 >= 1;

e995:    b273 + b279 + b284 + b289 >= 1;

e996:    b273 + b278 + b298 >= 1;

e997:    b273 + b278 + b294 + b299 >= 1;

e998:    b273 + b278 + b293 >= 1;

e999:    b273 + b278 + b289 >= 1;

e1000:    b273 + b278 + b286 + b299 >= 1;

e1001:    b273 + b278 + b286 + b293 >= 1;

e1002:    b273 + b278 + b286 + b289 >= 1;

e1003:    b273 + b278 + b285 + b299 >= 1;

e1004:    b273 + b278 + b285 + b294 >= 1;

e1005:    b273 + b278 + b285 + b289 >= 1;

e1006:    b273 + b277 + b298 >= 1;

e1007:    b273 + b277 + b294 + b299 >= 1;

e1008:    b273 + b277 + b293 >= 1;

e1009:    b273 + b277 + b289 >= 1;

e1010:    b273 + b277 + b286 + b299 >= 1;

e1011:    b273 + b277 + b286 + b294 >= 1;

e1012:    b273 + b277 + b286 + b289 >= 1;

e1013:    b273 + b276 + b299 >= 1;

e1014:    b273 + b276 + b294 >= 1;

e1015:    b273 + b276 + b289 >= 1;

e1016:    b272 + b297 >= 1;

e1017:    b272 + b294 + b298 >= 1;

e1018:    b272 + b293 + b299 >= 1;

e1019:    b272 + b292 >= 1;

e1020:    b272 + b289 + b299 >= 1;

e1021:    b272 + b289 + b294 >= 1;

e1022:    b272 + b288 >= 1;

e1023:    b272 + b286 + b298 >= 1;

e1024:    b272 + b286 + b294 + b299 >= 1;

e1025:    b272 + b286 + b293 >= 1;

e1026:    b272 + b286 + b289 >= 1;

e1027:    b272 + b285 + b298 >= 1;

e1028:    b272 + b285 + b294 + b299 >= 1;

e1029:    b272 + b285 + b293 >= 1;

e1030:    b272 + b285 + b289 >= 1;

e1031:    b272 + b284 + b299 >= 1;

e1032:    b272 + b284 + b294 >= 1;

e1033:    b272 + b284 + b289 >= 1;

e1034:    b272 + b280 + b298 >= 1;

e1035:    b272 + b280 + b294 + b299 >= 1;

e1036:    b272 + b280 + b293 >= 1;

e1037:    b272 + b280 + b289 >= 1;

e1038:    b272 + b280 + b286 + b299 >= 1;

e1039:    b272 + b280 + b286 + b293 >= 1;

e1040:    b272 + b280 + b286 + b289 >= 1;

e1041:    b272 + b280 + b285 + b299 >= 1;

e1042:    b272 + b280 + b285 + b294 >= 1;

e1043:    b272 + b280 + b285 + b289 >= 1;

e1044:    b272 + b279 + b298 >= 1;

e1045:    b272 + b279 + b294 + b299 >= 1;

e1046:    b272 + b279 + b293 >= 1;

e1047:    b272 + b279 + b289 >= 1;

e1048:    b272 + b279 + b286 + b299 >= 1;

e1049:    b272 + b279 + b286 + b294 >= 1;

e1050:    b272 + b279 + b286 + b289 >= 1;

e1051:    b272 + b278 + b299 >= 1;

e1052:    b272 + b278 + b294 >= 1;

e1053:    b272 + b278 + b289 >= 1;

e1054:    b271 + b299 >= 1;

e1055:    b271 + b294 >= 1;

e1056:    b271 + b289 >= 1;

e1057:    b270 + b295 >= 1;

e1058:    b270 + b294 + b296 >= 1;

e1059:    b270 + b293 + b297 >= 1;

e1060:    b270 + b292 + b298 >= 1;

e1061:    b270 + b291 + b299 >= 1;

e1062:    b270 + b290 >= 1;

e1063:    b270 + b289 + b297 >= 1;

e1064:    b270 + b289 + b294 + b298 >= 1;

e1065:    b270 + b289 + b293 + b299 >= 1;

e1066:    b270 + b289 + b292 >= 1;

e1067:    b270 + b288 + b299 >= 1;

e1068:    b270 + b288 + b294 >= 1;

e1069:    b270 + b287 >= 1;

e1070:    b270 + b286 + b296 >= 1;

e1071:    b270 + b286 + b294 + b297 >= 1;

e1072:    b270 + b286 + b292 + b299 >= 1;

e1073:    b270 + b286 + b291 >= 1;

e1074:    b270 + b286 + b289 + b297 >= 1;

e1075:    b270 + b286 + b289 + b294 + b298 >= 1;

e1076:    b270 + b286 + b289 + b293 + b299 >= 1;

e1077:    b270 + b286 + b289 + b292 >= 1;

e1078:    b270 + b286 + b288 >= 1;

e1079:    b270 + b285 + b296 >= 1;

e1080:    b270 + b285 + b294 + b297 >= 1;

e1081:    b270 + b285 + b293 + b298 >= 1;

e1082:    b270 + b285 + b292 + b299 >= 1;

e1083:    b270 + b285 + b291 >= 1;

e1084:    b270 + b285 + b289 + b298 >= 1;

e1085:    b270 + b285 + b289 + b294 + b299 >= 1;

e1086:    b270 + b285 + b289 + b293 >= 1;

e1087:    b270 + b285 + b288 >= 1;

e1088:    b270 + b284 + b297 >= 1;

e1089:    b270 + b284 + b294 + b298 >= 1;

e1090:    b270 + b284 + b293 + b299 >= 1;

e1091:    b270 + b284 + b292 >= 1;

e1092:    b270 + b284 + b289 + b299 >= 1;

e1093:    b270 + b284 + b289 + b294 >= 1;

e1094:    b270 + b284 + b288 >= 1;

e1095:    b270 + b283 + b298 >= 1;

e1096:    b270 + b283 + b294 + b299 >= 1;

e1097:    b270 + b283 + b293 >= 1;

e1098:    b270 + b283 + b289 >= 1;

e1099:    b270 + b282 + b299 >= 1;

e1100:    b270 + b282 + b294 >= 1;

e1101:    b270 + b282 + b289 >= 1;

e1102:    b270 + b280 + b296 >= 1;

e1103:    b270 + b280 + b293 + b297 >= 1;

e1104:    b270 + b280 + b292 + b298 >= 1;

e1105:    b270 + b280 + b291 + b299 >= 1;

e1106:    b270 + b280 + b290 >= 1;

e1107:    b270 + b280 + b289 + b297 >= 1;

e1108:    b270 + b280 + b289 + b294 + b298 >= 1;

e1109:    b270 + b280 + b289 + b293 >= 1;

e1110:    b270 + b280 + b288 >= 1;

e1111:    b270 + b280 + b286 + b296 >= 1;

e1112:    b270 + b280 + b286 + b294 + b297 >= 1;

e1113:    b270 + b280 + b286 + b293 + b298 >= 1;

e1114:    b270 + b280 + b286 + b292 + b299 >= 1;

e1115:    b270 + b280 + b286 + b291 >= 1;

e1116:    b270 + b280 + b286 + b289 + b298 >= 1;

e1117:    b270 + b280 + b286 + b289 + b294 + b299 >= 1;

e1118:    b270 + b280 + b286 + b289 + b293 >= 1;

e1119:    b270 + b280 + b286 + b288 >= 1;

e1120:    b270 + b280 + b285 + b297 >= 1;

e1121:    b270 + b280 + b285 + b294 + b298 >= 1;

e1122:    b270 + b280 + b285 + b293 + b299 >= 1;

e1123:    b270 + b280 + b285 + b292 >= 1;

e1124:    b270 + b280 + b285 + b289 + b299 >= 1;

e1125:    b270 + b280 + b285 + b289 + b294 >= 1;

e1126:    b270 + b280 + b285 + b288 >= 1;

e1127:    b270 + b280 + b284 + b298 >= 1;

e1128:    b270 + b280 + b284 + b294 + b299 >= 1;

e1129:    b270 + b280 + b284 + b293 >= 1;

e1130:    b270 + b280 + b284 + b289 >= 1;

e1131:    b270 + b280 + b283 + b299 >= 1;

e1132:    b270 + b280 + b283 + b294 >= 1;

e1133:    b270 + b280 + b283 + b289 >= 1;

e1134:    b270 + b279 + b296 >= 1;

e1135:    b270 + b279 + b294 + b297 >= 1;

e1136:    b270 + b279 + b293 + b298 >= 1;

e1137:    b270 + b279 + b292 + b299 >= 1;

e1138:    b270 + b279 + b291 >= 1;

e1139:    b270 + b279 + b289 + b298 >= 1;

e1140:    b270 + b279 + b289 + b294 + b299 >= 1;

e1141:    b270 + b279 + b289 + b293 >= 1;

e1142:    b270 + b279 + b288 >= 1;

e1143:    b270 + b279 + b286 + b297 >= 1;

e1144:    b270 + b279 + b286 + b294 + b298 >= 1;

e1145:    b270 + b279 + b286 + b293 + b299 >= 1;

e1146:    b270 + b279 + b286 + b292 >= 1;

e1147:    b270 + b279 + b286 + b289 + b299 >= 1;

e1148:    b270 + b279 + b286 + b289 + b294 >= 1;

e1149:    b270 + b279 + b286 + b288 >= 1;

e1150:    b270 + b279 + b285 + b298 >= 1;

e1151:    b270 + b279 + b285 + b294 + b299 >= 1;

e1152:    b270 + b279 + b285 + b293 >= 1;

e1153:    b270 + b279 + b285 + b289 >= 1;

e1154:    b270 + b279 + b284 + b299 >= 1;

e1155:    b270 + b279 + b284 + b294 >= 1;

e1156:    b270 + b279 + b284 + b289 >= 1;

e1157:    b270 + b279 + b283 + b299 >= 1;

e1158:    b270 + b279 + b283 + b294 >= 1;

e1159:    b270 + b279 + b283 + b289 >= 1;

e1160:    b270 + b278 + b297 >= 1;

e1161:    b270 + b278 + b294 + b298 >= 1;

e1162:    b270 + b278 + b293 + b299 >= 1;

e1163:    b270 + b278 + b292 >= 1;

e1164:    b270 + b278 + b289 + b299 >= 1;

e1165:    b270 + b278 + b289 + b294 >= 1;

e1166:    b270 + b278 + b288 >= 1;

e1167:    b270 + b278 + b286 + b298 >= 1;

e1168:    b270 + b278 + b286 + b294 + b299 >= 1;

e1169:    b270 + b278 + b286 + b293 >= 1;

e1170:    b270 + b278 + b286 + b289 >= 1;

e1171:    b270 + b278 + b285 + b299 >= 1;

e1172:    b270 + b278 + b285 + b294 >= 1;

e1173:    b270 + b278 + b285 + b289 >= 1;

e1174:    b270 + b278 + b284 + b299 >= 1;

e1175:    b270 + b278 + b284 + b294 >= 1;

e1176:    b270 + b278 + b284 + b289 >= 1;

e1177:    b270 + b277 + b298 >= 1;

e1178:    b270 + b277 + b294 + b299 >= 1;

e1179:    b270 + b277 + b293 >= 1;

e1180:    b270 + b277 + b289 >= 1;

e1181:    b270 + b277 + b286 + b299 >= 1;

e1182:    b270 + b277 + b286 + b294 >= 1;

e1183:    b270 + b277 + b286 + b289 >= 1;

e1184:    b270 + b277 + b285 + b299 >= 1;

e1185:    b270 + b277 + b285 + b294 >= 1;

e1186:    b270 + b277 + b285 + b289 >= 1;

e1187:    b270 + b276 + b299 >= 1;

e1188:    b270 + b276 + b294 >= 1;

e1189:    b270 + b276 + b289 >= 1;

e1190:    b270 + b274 + b296 >= 1;

e1191:    b270 + b274 + b294 + b297 >= 1;

e1192:    b270 + b274 + b293 + b298 >= 1;

e1193:    b270 + b274 + b292 + b299 >= 1;

e1194:    b270 + b274 + b291 >= 1;

e1195:    b270 + b274 + b289 + b298 >= 1;

e1196:    b270 + b274 + b289 + b294 + b299 >= 1;

e1197:    b270 + b274 + b289 + b293 >= 1;

e1198:    b270 + b274 + b288 >= 1;

e1199:    b270 + b274 + b286 + b297 >= 1;

e1200:    b270 + b274 + b286 + b294 + b298 >= 1;

e1201:    b270 + b274 + b286 + b293 + b299 >= 1;

e1202:    b270 + b274 + b286 + b292 >= 1;

e1203:    b270 + b274 + b286 + b289 + b299 >= 1;

e1204:    b270 + b274 + b286 + b289 + b294 >= 1;

e1205:    b270 + b274 + b286 + b288 >= 1;

e1206:    b270 + b274 + b285 + b297 >= 1;

e1207:    b270 + b274 + b285 + b294 + b298 >= 1;

e1208:    b270 + b274 + b285 + b293 + b299 >= 1;

e1209:    b270 + b274 + b285 + b292 >= 1;

e1210:    b270 + b274 + b285 + b289 + b299 >= 1;

e1211:    b270 + b274 + b285 + b289 + b294 >= 1;

e1212:    b270 + b274 + b285 + b288 >= 1;

e1213:    b270 + b274 + b284 + b298 >= 1;

e1214:    b270 + b274 + b284 + b294 + b299 >= 1;

e1215:    b270 + b274 + b284 + b293 >= 1;

e1216:    b270 + b274 + b284 + b289 >= 1;

e1217:    b270 + b274 + b283 + b299 >= 1;

e1218:    b270 + b274 + b283 + b294 >= 1;

e1219:    b270 + b274 + b283 + b289 >= 1;

e1220:    b270 + b274 + b280 + b297 >= 1;

e1221:    b270 + b274 + b280 + b294 + b298 >= 1;

e1222:    b270 + b274 + b280 + b293 + b299 >= 1;

e1223:    b270 + b274 + b280 + b292 >= 1;

e1224:    b270 + b274 + b280 + b289 + b299 >= 1;

e1225:    b270 + b274 + b280 + b289 + b294 >= 1;

e1226:    b270 + b274 + b280 + b288 >= 1;

e1227:    b270 + b274 + b280 + b286 + b298 >= 1;

e1228:    b270 + b274 + b280 + b286 + b294 + b299 >= 1;

e1229:    b270 + b274 + b280 + b286 + b293 >= 1;

e1230:    b270 + b274 + b280 + b286 + b289 >= 1;

e1231:    b270 + b274 + b280 + b285 + b298 >= 1;

e1232:    b270 + b274 + b280 + b285 + b294 + b299 >= 1;

e1233:    b270 + b274 + b280 + b285 + b293 >= 1;

e1234:    b270 + b274 + b280 + b285 + b289 >= 1;

e1235:    b270 + b274 + b280 + b284 + b299 >= 1;

e1236:    b270 + b274 + b280 + b284 + b294 >= 1;

e1237:    b270 + b274 + b280 + b284 + b289 >= 1;

e1238:    b270 + b274 + b279 + b297 >= 1;

e1239:    b270 + b274 + b279 + b294 + b298 >= 1;

e1240:    b270 + b274 + b279 + b293 + b299 >= 1;

e1241:    b270 + b274 + b279 + b292 >= 1;

e1242:    b270 + b274 + b279 + b289 + b299 >= 1;

e1243:    b270 + b274 + b279 + b289 + b294 >= 1;

e1244:    b270 + b274 + b279 + b288 >= 1;

e1245:    b270 + b274 + b279 + b286 + b298 >= 1;

e1246:    b270 + b274 + b279 + b286 + b294 + b299 >= 1;

e1247:    b270 + b274 + b279 + b286 + b293 >= 1;

e1248:    b270 + b274 + b279 + b286 + b289 >= 1;

e1249:    b270 + b274 + b279 + b285 + b299 >= 1;

e1250:    b270 + b274 + b279 + b285 + b294 >= 1;

e1251:    b270 + b274 + b279 + b285 + b289 >= 1;

e1252:    b270 + b274 + b278 + b298 >= 1;

e1253:    b270 + b274 + b278 + b294 + b299 >= 1;

e1254:    b270 + b274 + b278 + b293 >= 1;

e1255:    b270 + b274 + b278 + b289 >= 1;

e1256:    b270 + b274 + b278 + b286 + b299 >= 1;

e1257:    b270 + b274 + b278 + b286 + b294 >= 1;

e1258:    b270 + b274 + b278 + b286 + b289 >= 1;

e1259:    b270 + b274 + b277 + b299 >= 1;

e1260:    b270 + b274 + b277 + b294 >= 1;

e1261:    b270 + b274 + b277 + b289 >= 1;

e1262:    b270 + b273 + b297 >= 1;

e1263:    b270 + b273 + b294 + b298 >= 1;

e1264:    b270 + b273 + b293 + b299 >= 1;

e1265:    b270 + b273 + b292 >= 1;

e1266:    b270 + b273 + b289 + b299 >= 1;

e1267:    b270 + b273 + b289 + b294 >= 1;

e1268:    b270 + b273 + b288 >= 1;

e1269:    b270 + b273 + b286 + b298 >= 1;

e1270:    b270 + b273 + b286 + b294 + b299 >= 1;

e1271:    b270 + b273 + b286 + b293 >= 1;

e1272:    b270 + b273 + b286 + b289 >= 1;

e1273:    b270 + b273 + b285 + b299 >= 1;

e1274:    b270 + b273 + b285 + b294 >= 1;

e1275:    b270 + b273 + b285 + b289 >= 1;

e1276:    b270 + b273 + b280 + b298 >= 1;

e1277:    b270 + b273 + b280 + b294 + b299 >= 1;

e1278:    b270 + b273 + b280 + b293 >= 1;

e1279:    b270 + b273 + b280 + b289 >= 1;

e1280:    b270 + b273 + b280 + b286 + b299 >= 1;

e1281:    b270 + b273 + b280 + b286 + b294 >= 1;

e1282:    b270 + b273 + b280 + b286 + b289 >= 1;

e1283:    b270 + b273 + b279 + b299 >= 1;

e1284:    b270 + b273 + b279 + b294 >= 1;

e1285:    b270 + b273 + b279 + b289 >= 1;

e1286:    b270 + b272 + b299 >= 1;

e1287:    b270 + b272 + b294 >= 1;

e1288:    b270 + b272 + b289 >= 1;

e1289:    b269 + b297 >= 1;

e1290:    b269 + b294 + b298 >= 1;

e1291:    b269 + b293 + b299 >= 1;

e1292:    b269 + b292 >= 1;

e1293:    b269 + b289 + b299 >= 1;

e1294:    b269 + b289 + b294 >= 1;

e1295:    b269 + b288 >= 1;

e1296:    b269 + b286 + b298 >= 1;

e1297:    b269 + b286 + b294 + b299 >= 1;

e1298:    b269 + b286 + b293 >= 1;

e1299:    b269 + b286 + b289 >= 1;

e1300:    b269 + b285 + b298 >= 1;

e1301:    b269 + b285 + b294 + b299 >= 1;

e1302:    b269 + b285 + b293 >= 1;

e1303:    b269 + b285 + b289 >= 1;

e1304:    b269 + b284 + b299 >= 1;

e1305:    b269 + b284 + b294 >= 1;

e1306:    b269 + b284 + b289 >= 1;

e1307:    b269 + b280 + b298 >= 1;

e1308:    b269 + b280 + b294 + b299 >= 1;

e1309:    b269 + b280 + b293 >= 1;

e1310:    b269 + b280 + b289 >= 1;

e1311:    b269 + b280 + b286 + b299 >= 1;

e1312:    b269 + b280 + b286 + b293 >= 1;

e1313:    b269 + b280 + b286 + b289 >= 1;

e1314:    b269 + b280 + b285 + b299 >= 1;

e1315:    b269 + b280 + b285 + b294 >= 1;

e1316:    b269 + b280 + b285 + b289 >= 1;

e1317:    b269 + b279 + b298 >= 1;

e1318:    b269 + b279 + b294 + b299 >= 1;

e1319:    b269 + b279 + b293 >= 1;

e1320:    b269 + b279 + b289 >= 1;

e1321:    b269 + b279 + b286 + b299 >= 1;

e1322:    b269 + b279 + b286 + b294 >= 1;

e1323:    b269 + b279 + b286 + b289 >= 1;

e1324:    b269 + b278 + b299 >= 1;

e1325:    b269 + b278 + b294 >= 1;

e1326:    b269 + b278 + b289 >= 1;

e1327:    b269 + b274 + b298 >= 1;

e1328:    b269 + b274 + b294 + b299 >= 1;

e1329:    b269 + b274 + b293 >= 1;

e1330:    b269 + b274 + b289 >= 1;

e1331:    b269 + b274 + b286 + b299 >= 1;

e1332:    b269 + b274 + b286 + b294 >= 1;

e1333:    b269 + b274 + b286 + b289 >= 1;

e1334:    b269 + b274 + b280 + b299 >= 1;

e1335:    b269 + b274 + b280 + b294 >= 1;

e1336:    b269 + b274 + b280 + b289 >= 1;

e1337:    b269 + b273 + b299 >= 1;

e1338:    b269 + b273 + b294 >= 1;

e1339:    b269 + b273 + b289 >= 1;

e1340:    b268 + b299 >= 1;

e1341:    b268 + b294 >= 1;

e1342:    b268 + b289 >= 1;

e1343:    b267 + b295 >= 1;

e1344:    b267 + b294 + b296 >= 1;

e1345:    b267 + b293 + b297 >= 1;

e1346:    b267 + b292 + b298 >= 1;

e1347:    b267 + b291 + b299 >= 1;

e1348:    b267 + b290 >= 1;

e1349:    b267 + b289 + b297 >= 1;

e1350:    b267 + b289 + b294 + b298 >= 1;

e1351:    b267 + b289 + b293 + b299 >= 1;

e1352:    b267 + b289 + b292 >= 1;

e1353:    b267 + b288 + b299 >= 1;

e1354:    b267 + b288 + b294 >= 1;

e1355:    b267 + b287 >= 1;

e1356:    b267 + b286 + b296 >= 1;

e1357:    b267 + b286 + b294 + b297 >= 1;

e1358:    b267 + b286 + b293 + b298 >= 1;

e1359:    b267 + b286 + b292 + b299 >= 1;

e1360:    b267 + b286 + b291 >= 1;

e1361:    b267 + b286 + b289 + b298 >= 1;

e1362:    b267 + b286 + b289 + b294 + b299 >= 1;

e1363:    b267 + b286 + b289 + b293 >= 1;

e1364:    b267 + b286 + b288 >= 1;

e1365:    b267 + b285 + b296 >= 1;

e1366:    b267 + b285 + b294 + b297 >= 1;

e1367:    b267 + b285 + b293 + b298 >= 1;

e1368:    b267 + b285 + b292 >= 1;

e1369:    b267 + b285 + b289 + b298 >= 1;

e1370:    b267 + b285 + b289 + b294 + b299 >= 1;

e1371:    b267 + b285 + b289 + b293 >= 1;

e1372:    b267 + b285 + b288 >= 1;

e1373:    b267 + b284 + b297 >= 1;

e1374:    b267 + b284 + b294 + b298 >= 1;

e1375:    b267 + b284 + b293 + b299 >= 1;

e1376:    b267 + b284 + b292 >= 1;

e1377:    b267 + b284 + b289 + b299 >= 1;

e1378:    b267 + b284 + b289 + b294 >= 1;

e1379:    b267 + b284 + b288 >= 1;

e1380:    b267 + b283 + b298 >= 1;

e1381:    b267 + b283 + b294 + b299 >= 1;

e1382:    b267 + b283 + b293 >= 1;

e1383:    b267 + b283 + b289 >= 1;

e1384:    b267 + b282 + b299 >= 1;

e1385:    b267 + b282 + b294 >= 1;

e1386:    b267 + b282 + b289 >= 1;

e1387:    b267 + b280 + b296 >= 1;

e1388:    b267 + b280 + b294 + b297 >= 1;

e1389:    b267 + b280 + b293 + b298 >= 1;

e1390:    b267 + b280 + b292 + b299 >= 1;

e1391:    b267 + b280 + b291 >= 1;

e1392:    b267 + b280 + b289 + b298 >= 1;

e1393:    b267 + b280 + b289 + b294 + b299 >= 1;

e1394:    b267 + b280 + b289 + b293 >= 1;

e1395:    b267 + b280 + b288 >= 1;

e1396:    b267 + b280 + b286 + b297 >= 1;

e1397:    b267 + b280 + b286 + b293 + b299 >= 1;

e1398:    b267 + b280 + b286 + b292 >= 1;

e1399:    b267 + b280 + b286 + b289 + b299 >= 1;

e1400:    b267 + b280 + b286 + b289 + b293 >= 1;

e1401:    b267 + b280 + b286 + b288 >= 1;

e1402:    b267 + b280 + b285 + b297 >= 1;

e1403:    b267 + b280 + b285 + b294 + b298 >= 1;

e1404:    b267 + b280 + b285 + b293 + b299 >= 1;

e1405:    b267 + b280 + b285 + b292 >= 1;

e1406:    b267 + b280 + b285 + b289 + b299 >= 1;

e1407:    b267 + b280 + b285 + b289 + b294 >= 1;

e1408:    b267 + b280 + b285 + b288 >= 1;

e1409:    b267 + b280 + b284 + b298 >= 1;

e1410:    b267 + b280 + b284 + b294 + b299 >= 1;

e1411:    b267 + b280 + b284 + b293 >= 1;

e1412:    b267 + b280 + b284 + b289 >= 1;

e1413:    b267 + b280 + b283 + b299 >= 1;

e1414:    b267 + b280 + b283 + b294 >= 1;

e1415:    b267 + b280 + b283 + b289 >= 1;

e1416:    b267 + b279 + b296 >= 1;

e1417:    b267 + b279 + b294 + b297 >= 1;

e1418:    b267 + b279 + b293 + b298 >= 1;

e1419:    b267 + b279 + b292 + b299 >= 1;

e1420:    b267 + b279 + b291 >= 1;

e1421:    b267 + b279 + b289 + b298 >= 1;

e1422:    b267 + b279 + b289 + b294 + b299 >= 1;

e1423:    b267 + b279 + b289 + b293 >= 1;

e1424:    b267 + b279 + b288 >= 1;

e1425:    b267 + b279 + b286 + b297 >= 1;

e1426:    b267 + b279 + b286 + b294 + b298 >= 1;

e1427:    b267 + b279 + b286 + b293 + b299 >= 1;

e1428:    b267 + b279 + b286 + b292 >= 1;

e1429:    b267 + b279 + b286 + b289 + b299 >= 1;

e1430:    b267 + b279 + b286 + b289 + b294 >= 1;

e1431:    b267 + b279 + b286 + b288 >= 1;

e1432:    b267 + b279 + b285 + b298 >= 1;

e1433:    b267 + b279 + b285 + b294 + b299 >= 1;

e1434:    b267 + b279 + b285 + b293 >= 1;

e1435:    b267 + b279 + b285 + b289 >= 1;

e1436:    b267 + b279 + b284 + b299 >= 1;

e1437:    b267 + b279 + b284 + b294 >= 1;

e1438:    b267 + b279 + b284 + b289 >= 1;

e1439:    b267 + b278 + b297 >= 1;

e1440:    b267 + b278 + b294 + b298 >= 1;

e1441:    b267 + b278 + b293 + b299 >= 1;

e1442:    b267 + b278 + b292 >= 1;

e1443:    b267 + b278 + b289 + b299 >= 1;

e1444:    b267 + b278 + b289 + b294 >= 1;

e1445:    b267 + b278 + b288 >= 1;

e1446:    b267 + b278 + b286 + b298 >= 1;

e1447:    b267 + b278 + b286 + b294 + b299 >= 1;

e1448:    b267 + b278 + b286 + b293 >= 1;

e1449:    b267 + b278 + b286 + b289 >= 1;

e1450:    b267 + b278 + b285 + b299 >= 1;

e1451:    b267 + b278 + b285 + b294 >= 1;

e1452:    b267 + b278 + b285 + b289 >= 1;

e1453:    b267 + b277 + b298 >= 1;

e1454:    b267 + b277 + b294 + b299 >= 1;

e1455:    b267 + b277 + b293 >= 1;

e1456:    b267 + b277 + b289 >= 1;

e1457:    b267 + b277 + b286 + b299 >= 1;

e1458:    b267 + b277 + b286 + b294 >= 1;

e1459:    b267 + b277 + b286 + b289 >= 1;

e1460:    b267 + b276 + b299 >= 1;

e1461:    b267 + b276 + b294 >= 1;

e1462:    b267 + b276 + b289 >= 1;

e1463:    b267 + b274 + b296 >= 1;

e1464:    b267 + b274 + b294 + b297 >= 1;

e1465:    b267 + b274 + b293 + b298 >= 1;

e1466:    b267 + b274 + b292 + b299 >= 1;

e1467:    b267 + b274 + b291 >= 1;

e1468:    b267 + b274 + b289 + b298 >= 1;

e1469:    b267 + b274 + b289 + b294 + b299 >= 1;

e1470:    b267 + b274 + b289 + b293 >= 1;

e1471:    b267 + b274 + b288 >= 1;

e1472:    b267 + b274 + b286 + b297 >= 1;

e1473:    b267 + b274 + b286 + b294 + b298 >= 1;

e1474:    b267 + b274 + b286 + b293 + b299 >= 1;

e1475:    b267 + b274 + b286 + b292 >= 1;

e1476:    b267 + b274 + b286 + b289 + b299 >= 1;

e1477:    b267 + b274 + b286 + b289 + b294 >= 1;

e1478:    b267 + b274 + b286 + b288 >= 1;

e1479:    b267 + b274 + b285 + b298 >= 1;

e1480:    b267 + b274 + b285 + b294 + b299 >= 1;

e1481:    b267 + b274 + b285 + b293 >= 1;

e1482:    b267 + b274 + b285 + b289 >= 1;

e1483:    b267 + b274 + b284 + b298 >= 1;

e1484:    b267 + b274 + b284 + b294 + b299 >= 1;

e1485:    b267 + b274 + b284 + b293 >= 1;

e1486:    b267 + b274 + b284 + b289 >= 1;

e1487:    b267 + b274 + b283 + b299 >= 1;

e1488:    b267 + b274 + b283 + b294 >= 1;

e1489:    b267 + b274 + b283 + b289 >= 1;

e1490:    b267 + b274 + b280 + b297 >= 1;

e1491:    b267 + b274 + b280 + b294 + b298 >= 1;

e1492:    b267 + b274 + b280 + b293 + b299 >= 1;

e1493:    b267 + b274 + b280 + b292 >= 1;

e1494:    b267 + b274 + b280 + b289 + b299 >= 1;

e1495:    b267 + b274 + b280 + b289 + b294 >= 1;

e1496:    b267 + b274 + b280 + b288 >= 1;

e1497:    b267 + b274 + b280 + b286 + b298 >= 1;

e1498:    b267 + b274 + b280 + b286 + b294 + b299 >= 1;

e1499:    b267 + b274 + b280 + b286 + b293 >= 1;

e1500:    b267 + b274 + b280 + b286 + b289 >= 1;

e1501:    b267 + b274 + b280 + b285 + b298 >= 1;

e1502:    b267 + b274 + b280 + b285 + b294 + b299 >= 1;

e1503:    b267 + b274 + b280 + b285 + b293 >= 1;

e1504:    b267 + b274 + b280 + b285 + b289 >= 1;

e1505:    b267 + b274 + b280 + b284 + b299 >= 1;

e1506:    b267 + b274 + b280 + b284 + b294 >= 1;

e1507:    b267 + b274 + b280 + b284 + b289 >= 1;

e1508:    b267 + b274 + b279 + b298 >= 1;

e1509:    b267 + b274 + b279 + b293 >= 1;

e1510:    b267 + b274 + b279 + b289 >= 1;

e1511:    b267 + b274 + b279 + b286 + b298 >= 1;

e1512:    b267 + b274 + b279 + b286 + b294 + b299 >= 1;

e1513:    b267 + b274 + b279 + b286 + b293 >= 1;

e1514:    b267 + b274 + b279 + b286 + b289 >= 1;

e1515:    b267 + b274 + b279 + b285 + b299 >= 1;

e1516:    b267 + b274 + b279 + b285 + b294 >= 1;

e1517:    b267 + b274 + b279 + b285 + b289 >= 1;

e1518:    b267 + b274 + b278 + b298 >= 1;

e1519:    b267 + b274 + b278 + b294 + b299 >= 1;

e1520:    b267 + b274 + b278 + b293 >= 1;

e1521:    b267 + b274 + b278 + b289 >= 1;

e1522:    b267 + b274 + b278 + b286 + b299 >= 1;

e1523:    b267 + b274 + b278 + b286 + b294 >= 1;

e1524:    b267 + b274 + b278 + b286 + b289 >= 1;

e1525:    b267 + b274 + b277 + b299 >= 1;

e1526:    b267 + b274 + b277 + b294 >= 1;

e1527:    b267 + b274 + b277 + b289 >= 1;

e1528:    b267 + b273 + b297 >= 1;

e1529:    b267 + b273 + b294 + b298 >= 1;

e1530:    b267 + b273 + b293 + b299 >= 1;

e1531:    b267 + b273 + b292 >= 1;

e1532:    b267 + b273 + b289 + b299 >= 1;

e1533:    b267 + b273 + b289 + b294 >= 1;

e1534:    b267 + b273 + b288 >= 1;

e1535:    b267 + b273 + b286 + b298 >= 1;

e1536:    b267 + b273 + b286 + b294 + b299 >= 1;

e1537:    b267 + b273 + b286 + b293 >= 1;

e1538:    b267 + b273 + b286 + b289 >= 1;

e1539:    b267 + b273 + b285 + b299 >= 1;

e1540:    b267 + b273 + b285 + b294 >= 1;

e1541:    b267 + b273 + b285 + b289 >= 1;

e1542:    b267 + b273 + b280 + b298 >= 1;

e1543:    b267 + b273 + b280 + b294 + b299 >= 1;

e1544:    b267 + b273 + b280 + b293 >= 1;

e1545:    b267 + b273 + b280 + b289 >= 1;

e1546:    b267 + b273 + b280 + b286 + b299 >= 1;

e1547:    b267 + b273 + b280 + b286 + b294 >= 1;

e1548:    b267 + b273 + b280 + b286 + b289 >= 1;

e1549:    b267 + b273 + b279 + b299 >= 1;

e1550:    b267 + b273 + b279 + b294 >= 1;

e1551:    b267 + b273 + b279 + b289 >= 1;

e1552:    b267 + b272 + b299 >= 1;

e1553:    b267 + b272 + b294 >= 1;

e1554:    b267 + b272 + b289 >= 1;

e1555:    b267 + b270 + b297 >= 1;

e1556:    b267 + b270 + b294 + b298 >= 1;

e1557:    b267 + b270 + b293 + b299 >= 1;

e1558:    b267 + b270 + b292 >= 1;

e1559:    b267 + b270 + b289 + b299 >= 1;

e1560:    b267 + b270 + b289 + b294 >= 1;

e1561:    b267 + b270 + b288 >= 1;

e1562:    b267 + b270 + b286 + b298 >= 1;

e1563:    b267 + b270 + b286 + b294 + b299 >= 1;

e1564:    b267 + b270 + b286 + b293 >= 1;

e1565:    b267 + b270 + b286 + b289 >= 1;

e1566:    b267 + b270 + b285 + b298 >= 1;

e1567:    b267 + b270 + b285 + b294 + b299 >= 1;

e1568:    b267 + b270 + b285 + b293 >= 1;

e1569:    b267 + b270 + b285 + b289 >= 1;

e1570:    b267 + b270 + b284 + b299 >= 1;

e1571:    b267 + b270 + b284 + b294 >= 1;

e1572:    b267 + b270 + b284 + b289 >= 1;

e1573:    b267 + b270 + b280 + b298 >= 1;

e1574:    b267 + b270 + b280 + b294 + b299 >= 1;

e1575:    b267 + b270 + b280 + b293 >= 1;

e1576:    b267 + b270 + b280 + b289 >= 1;

e1577:    b267 + b270 + b280 + b286 + b298 >= 1;

e1578:    b267 + b270 + b280 + b286 + b294 + b299 >= 1;

e1579:    b267 + b270 + b280 + b286 + b293 >= 1;

e1580:    b267 + b270 + b280 + b286 + b289 >= 1;

e1581:    b267 + b270 + b280 + b285 + b299 >= 1;

e1582:    b267 + b270 + b280 + b285 + b294 >= 1;

e1583:    b267 + b270 + b280 + b285 + b289 >= 1;

e1584:    b267 + b270 + b279 + b298 >= 1;

e1585:    b267 + b270 + b279 + b294 + b299 >= 1;

e1586:    b267 + b270 + b279 + b293 >= 1;

e1587:    b267 + b270 + b279 + b289 >= 1;

e1588:    b267 + b270 + b279 + b286 + b299 >= 1;

e1589:    b267 + b270 + b279 + b286 + b294 >= 1;

e1590:    b267 + b270 + b279 + b286 + b289 >= 1;

e1591:    b267 + b270 + b278 + b299 >= 1;

e1592:    b267 + b270 + b278 + b294 >= 1;

e1593:    b267 + b270 + b278 + b289 >= 1;

e1594:    b267 + b270 + b274 + b298 >= 1;

e1595:    b267 + b270 + b274 + b294 + b299 >= 1;

e1596:    b267 + b270 + b274 + b293 >= 1;

e1597:    b267 + b270 + b274 + b289 >= 1;

e1598:    b267 + b270 + b274 + b286 + b299 >= 1;

e1599:    b267 + b270 + b274 + b286 + b294 >= 1;

e1600:    b267 + b270 + b274 + b286 + b289 >= 1;

e1601:    b267 + b270 + b274 + b285 + b299 >= 1;

e1602:    b267 + b270 + b274 + b285 + b294 >= 1;

e1603:    b267 + b270 + b274 + b285 + b289 >= 1;

e1604:    b267 + b270 + b274 + b280 + b299 >= 1;

e1605:    b267 + b270 + b274 + b280 + b294 >= 1;

e1606:    b267 + b270 + b274 + b280 + b289 >= 1;

e1607:    b267 + b270 + b274 + b279 + b299 >= 1;

e1608:    b267 + b270 + b274 + b279 + b294 >= 1;

e1609:    b267 + b270 + b274 + b279 + b289 >= 1;

e1610:    b267 + b270 + b273 + b299 >= 1;

e1611:    b267 + b270 + b273 + b294 >= 1;

e1612:    b267 + b270 + b273 + b289 >= 1;

e1613:    b267 + b269 + b299 >= 1;

e1614:    b267 + b269 + b294 >= 1;

e1615:    b267 + b269 + b289 >= 1;

e1616:    b266 + b297 >= 1;

e1617:    b266 + b294 + b298 >= 1;

e1618:    b266 + b293 + b299 >= 1;

e1619:    b266 + b292 >= 1;

e1620:    b266 + b289 + b299 >= 1;

e1621:    b266 + b289 + b294 >= 1;

e1622:    b266 + b288 >= 1;

e1623:    b266 + b286 + b298 >= 1;

e1624:    b266 + b286 + b294 + b299 >= 1;

e1625:    b266 + b286 + b293 >= 1;

e1626:    b266 + b286 + b289 >= 1;

e1627:    b266 + b285 + b298 >= 1;

e1628:    b266 + b285 + b294 + b299 >= 1;

e1629:    b266 + b285 + b293 >= 1;

e1630:    b266 + b285 + b289 >= 1;

e1631:    b266 + b284 + b299 >= 1;

e1632:    b266 + b284 + b294 >= 1;

e1633:    b266 + b284 + b289 >= 1;

e1634:    b266 + b280 + b298 >= 1;

e1635:    b266 + b280 + b293 + b299 >= 1;

e1636:    b266 + b280 + b292 >= 1;

e1637:    b266 + b280 + b289 >= 1;

e1638:    b266 + b280 + b286 + b298 >= 1;

e1639:    b266 + b280 + b286 + b294 + b299 >= 1;

e1640:    b266 + b280 + b286 + b293 >= 1;

e1641:    b266 + b280 + b286 + b289 >= 1;

e1642:    b266 + b280 + b285 + b299 >= 1;

e1643:    b266 + b280 + b285 + b294 >= 1;

e1644:    b266 + b280 + b285 + b289 >= 1;

e1645:    b266 + b279 + b298 >= 1;

e1646:    b266 + b279 + b294 + b299 >= 1;

e1647:    b266 + b279 + b293 >= 1;

e1648:    b266 + b279 + b289 >= 1;

e1649:    b266 + b279 + b286 + b299 >= 1;

e1650:    b266 + b279 + b286 + b294 >= 1;

e1651:    b266 + b279 + b286 + b289 >= 1;

e1652:    b266 + b278 + b299 >= 1;

e1653:    b266 + b278 + b294 >= 1;

e1654:    b266 + b278 + b289 >= 1;

e1655:    b266 + b274 + b298 >= 1;

e1656:    b266 + b274 + b294 + b299 >= 1;

e1657:    b266 + b274 + b293 >= 1;

e1658:    b266 + b274 + b289 >= 1;

e1659:    b266 + b274 + b286 + b299 >= 1;

e1660:    b266 + b274 + b286 + b294 >= 1;

e1661:    b266 + b274 + b286 + b289 >= 1;

e1662:    b266 + b274 + b280 + b299 >= 1;

e1663:    b266 + b274 + b280 + b294 >= 1;

e1664:    b266 + b274 + b280 + b289 >= 1;

e1665:    b266 + b274 + b279 + b299 >= 1;

e1666:    b266 + b274 + b279 + b294 >= 1;

e1667:    b266 + b274 + b279 + b289 >= 1;

e1668:    b266 + b273 + b299 >= 1;

e1669:    b266 + b273 + b294 >= 1;

e1670:    b266 + b273 + b289 >= 1;

e1671:    b266 + b270 + b299 >= 1;

e1672:    b266 + b270 + b294 >= 1;

e1673:    b266 + b270 + b289 >= 1;

e1674:    b266 + b270 + b280 + b299 >= 1;

e1675:    b266 + b270 + b280 + b294 >= 1;

e1676:    b266 + b270 + b280 + b289 >= 1;

e1677:    b265 + b299 >= 1;

e1678:    b265 + b294 >= 1;

e1679:    b265 + b289 >= 1;

e1680:    b264 + b295 >= 1;

e1681:    b264 + b294 + b296 >= 1;

e1682:    b264 + b293 + b297 >= 1;

e1683:    b264 + b292 + b298 >= 1;

e1684:    b264 + b291 + b299 >= 1;

e1685:    b264 + b290 >= 1;

e1686:    b264 + b289 + b297 >= 1;

e1687:    b264 + b289 + b294 + b298 >= 1;

e1688:    b264 + b289 + b292 >= 1;

e1689:    b264 + b288 + b299 >= 1;

e1690:    b264 + b288 + b294 >= 1;

e1691:    b264 + b287 >= 1;

e1692:    b264 + b286 + b296 >= 1;

e1693:    b264 + b286 + b293 + b297 >= 1;

e1694:    b264 + b286 + b292 + b299 >= 1;

e1695:    b264 + b286 + b291 >= 1;

e1696:    b264 + b286 + b289 + b297 >= 1;

e1697:    b264 + b286 + b289 + b294 + b298 >= 1;

e1698:    b264 + b286 + b289 + b293 + b299 >= 1;

e1699:    b264 + b286 + b289 + b292 >= 1;

e1700:    b264 + b286 + b288 >= 1;

e1701:    b264 + b285 + b296 >= 1;

e1702:    b264 + b285 + b294 + b297 >= 1;

e1703:    b264 + b285 + b293 + b298 >= 1;

e1704:    b264 + b285 + b292 + b299 >= 1;

e1705:    b264 + b285 + b291 >= 1;

e1706:    b264 + b285 + b289 + b298 >= 1;

e1707:    b264 + b285 + b289 + b294 + b299 >= 1;

e1708:    b264 + b285 + b289 + b293 >= 1;

e1709:    b264 + b285 + b288 >= 1;

e1710:    b264 + b284 + b297 >= 1;

e1711:    b264 + b284 + b294 + b298 >= 1;

e1712:    b264 + b284 + b293 + b299 >= 1;

e1713:    b264 + b284 + b292 >= 1;

e1714:    b264 + b284 + b289 + b299 >= 1;

e1715:    b264 + b284 + b289 + b294 >= 1;

e1716:    b264 + b284 + b288 >= 1;

e1717:    b264 + b283 + b298 >= 1;

e1718:    b264 + b283 + b294 + b299 >= 1;

e1719:    b264 + b283 + b293 >= 1;

e1720:    b264 + b283 + b289 >= 1;

e1721:    b264 + b282 + b299 >= 1;

e1722:    b264 + b282 + b294 >= 1;

e1723:    b264 + b282 + b289 >= 1;

e1724:    b264 + b280 + b296 >= 1;

e1725:    b264 + b280 + b293 + b297 >= 1;

e1726:    b264 + b280 + b292 + b298 >= 1;

e1727:    b264 + b280 + b291 >= 1;

e1728:    b264 + b280 + b289 + b297 >= 1;

e1729:    b264 + b280 + b289 + b294 + b298 >= 1;

e1730:    b264 + b280 + b289 + b293 + b299 >= 1;

e1731:    b264 + b280 + b289 + b292 >= 1;

e1732:    b264 + b280 + b288 >= 1;

e1733:    b264 + b280 + b286 + b296 >= 1;

e1734:    b264 + b280 + b286 + b294 + b297 >= 1;

e1735:    b264 + b280 + b286 + b293 + b298 >= 1;

e1736:    b264 + b280 + b286 + b292 + b299 >= 1;

e1737:    b264 + b280 + b286 + b291 >= 1;

e1738:    b264 + b280 + b286 + b289 + b298 >= 1;

e1739:    b264 + b280 + b286 + b289 + b294 + b299 >= 1;

e1740:    b264 + b280 + b286 + b289 + b293 >= 1;

e1741:    b264 + b280 + b286 + b288 >= 1;

e1742:    b264 + b280 + b285 + b297 >= 1;

e1743:    b264 + b280 + b285 + b294 + b298 >= 1;

e1744:    b264 + b280 + b285 + b293 + b299 >= 1;

e1745:    b264 + b280 + b285 + b292 >= 1;

e1746:    b264 + b280 + b285 + b289 + b299 >= 1;

e1747:    b264 + b280 + b285 + b289 + b294 >= 1;

e1748:    b264 + b280 + b285 + b288 >= 1;

e1749:    b264 + b280 + b284 + b298 >= 1;

e1750:    b264 + b280 + b284 + b294 + b299 >= 1;

e1751:    b264 + b280 + b284 + b293 >= 1;

e1752:    b264 + b280 + b284 + b289 >= 1;

e1753:    b264 + b280 + b283 + b299 >= 1;

e1754:    b264 + b280 + b283 + b294 >= 1;

e1755:    b264 + b280 + b283 + b289 >= 1;

e1756:    b264 + b280 + b282 + b299 >= 1;

e1757:    b264 + b280 + b282 + b294 >= 1;

e1758:    b264 + b280 + b282 + b289 >= 1;

e1759:    b264 + b279 + b296 >= 1;

e1760:    b264 + b279 + b294 + b297 >= 1;

e1761:    b264 + b279 + b293 + b298 >= 1;

e1762:    b264 + b279 + b292 + b299 >= 1;

e1763:    b264 + b279 + b291 >= 1;

e1764:    b264 + b279 + b289 + b298 >= 1;

e1765:    b264 + b279 + b289 + b294 + b299 >= 1;

e1766:    b264 + b279 + b289 + b293 >= 1;

e1767:    b264 + b279 + b288 >= 1;

e1768:    b264 + b279 + b286 + b297 >= 1;

e1769:    b264 + b279 + b286 + b294 + b298 >= 1;

e1770:    b264 + b279 + b286 + b293 + b299 >= 1;

e1771:    b264 + b279 + b286 + b292 >= 1;

e1772:    b264 + b279 + b286 + b289 + b299 >= 1;

e1773:    b264 + b279 + b286 + b289 + b294 >= 1;

e1774:    b264 + b279 + b286 + b288 >= 1;

e1775:    b264 + b279 + b285 + b298 >= 1;

e1776:    b264 + b279 + b285 + b294 + b299 >= 1;

e1777:    b264 + b279 + b285 + b293 >= 1;

e1778:    b264 + b279 + b285 + b289 >= 1;

e1779:    b264 + b279 + b284 + b299 >= 1;

e1780:    b264 + b279 + b284 + b294 >= 1;

e1781:    b264 + b279 + b284 + b289 >= 1;

e1782:    b264 + b279 + b283 + b299 >= 1;

e1783:    b264 + b279 + b283 + b294 >= 1;

e1784:    b264 + b279 + b283 + b289 >= 1;

e1785:    b264 + b278 + b297 >= 1;

e1786:    b264 + b278 + b294 + b298 >= 1;

e1787:    b264 + b278 + b293 + b299 >= 1;

e1788:    b264 + b278 + b292 >= 1;

e1789:    b264 + b278 + b289 + b299 >= 1;

e1790:    b264 + b278 + b289 + b294 >= 1;

e1791:    b264 + b278 + b288 >= 1;

e1792:    b264 + b278 + b286 + b298 >= 1;

e1793:    b264 + b278 + b286 + b294 + b299 >= 1;

e1794:    b264 + b278 + b286 + b293 >= 1;

e1795:    b264 + b278 + b286 + b289 >= 1;

e1796:    b264 + b278 + b285 + b299 >= 1;

e1797:    b264 + b278 + b285 + b294 >= 1;

e1798:    b264 + b278 + b285 + b289 >= 1;

e1799:    b264 + b278 + b284 + b299 >= 1;

e1800:    b264 + b278 + b284 + b294 >= 1;

e1801:    b264 + b278 + b284 + b289 >= 1;

e1802:    b264 + b277 + b298 >= 1;

e1803:    b264 + b277 + b294 + b299 >= 1;

e1804:    b264 + b277 + b293 >= 1;

e1805:    b264 + b277 + b289 >= 1;

e1806:    b264 + b277 + b286 + b299 >= 1;

e1807:    b264 + b277 + b286 + b294 >= 1;

e1808:    b264 + b277 + b286 + b289 >= 1;

e1809:    b264 + b277 + b285 + b299 >= 1;

e1810:    b264 + b277 + b285 + b294 >= 1;

e1811:    b264 + b277 + b285 + b289 >= 1;

e1812:    b264 + b276 + b299 >= 1;

e1813:    b264 + b276 + b294 >= 1;

e1814:    b264 + b276 + b289 >= 1;

e1815:    b264 + b274 + b296 >= 1;

e1816:    b264 + b274 + b294 + b297 >= 1;

e1817:    b264 + b274 + b293 + b298 >= 1;

e1818:    b264 + b274 + b292 + b299 >= 1;

e1819:    b264 + b274 + b291 >= 1;

e1820:    b264 + b274 + b289 + b298 >= 1;

e1821:    b264 + b274 + b289 + b294 + b299 >= 1;

e1822:    b264 + b274 + b289 + b293 >= 1;

e1823:    b264 + b274 + b288 >= 1;

e1824:    b264 + b274 + b286 + b297 >= 1;

e1825:    b264 + b274 + b286 + b294 + b298 >= 1;

e1826:    b264 + b274 + b286 + b293 + b299 >= 1;

e1827:    b264 + b274 + b286 + b292 >= 1;

e1828:    b264 + b274 + b286 + b289 + b299 >= 1;

e1829:    b264 + b274 + b286 + b289 + b294 >= 1;

e1830:    b264 + b274 + b286 + b288 >= 1;

e1831:    b264 + b274 + b285 + b297 >= 1;

e1832:    b264 + b274 + b285 + b294 + b298 >= 1;

e1833:    b264 + b274 + b285 + b293 + b299 >= 1;

e1834:    b264 + b274 + b285 + b292 >= 1;

e1835:    b264 + b274 + b285 + b289 + b299 >= 1;

e1836:    b264 + b274 + b285 + b289 + b294 >= 1;

e1837:    b264 + b274 + b285 + b288 >= 1;

e1838:    b264 + b274 + b284 + b298 >= 1;

e1839:    b264 + b274 + b284 + b294 + b299 >= 1;

e1840:    b264 + b274 + b284 + b293 >= 1;

e1841:    b264 + b274 + b284 + b289 >= 1;

e1842:    b264 + b274 + b283 + b299 >= 1;

e1843:    b264 + b274 + b283 + b294 >= 1;

e1844:    b264 + b274 + b283 + b289 >= 1;

e1845:    b264 + b274 + b280 + b297 >= 1;

e1846:    b264 + b274 + b280 + b294 + b298 >= 1;

e1847:    b264 + b274 + b280 + b293 + b299 >= 1;

e1848:    b264 + b274 + b280 + b292 >= 1;

e1849:    b264 + b274 + b280 + b289 + b299 >= 1;

e1850:    b264 + b274 + b280 + b289 + b294 >= 1;

e1851:    b264 + b274 + b280 + b288 >= 1;

e1852:    b264 + b274 + b280 + b286 + b297 >= 1;

e1853:    b264 + b274 + b280 + b286 + b294 + b298 >= 1;

e1854:    b264 + b274 + b280 + b286 + b293 >= 1;

e1855:    b264 + b274 + b280 + b286 + b289 >= 1;

e1856:    b264 + b274 + b280 + b285 + b298 >= 1;

e1857:    b264 + b274 + b280 + b285 + b294 + b299 >= 1;

e1858:    b264 + b274 + b280 + b285 + b293 >= 1;

e1859:    b264 + b274 + b280 + b285 + b289 >= 1;

e1860:    b264 + b274 + b280 + b284 + b299 >= 1;

e1861:    b264 + b274 + b280 + b284 + b294 >= 1;

e1862:    b264 + b274 + b280 + b284 + b289 >= 1;

e1863:    b264 + b274 + b279 + b297 >= 1;

e1864:    b264 + b274 + b279 + b294 + b298 >= 1;

e1865:    b264 + b274 + b279 + b293 + b299 >= 1;

e1866:    b264 + b274 + b279 + b292 >= 1;

e1867:    b264 + b274 + b279 + b289 + b299 >= 1;

e1868:    b264 + b274 + b279 + b289 + b294 >= 1;

e1869:    b264 + b274 + b279 + b288 >= 1;

e1870:    b264 + b274 + b279 + b286 + b298 >= 1;

e1871:    b264 + b274 + b279 + b286 + b294 + b299 >= 1;

e1872:    b264 + b274 + b279 + b286 + b293 >= 1;

e1873:    b264 + b274 + b279 + b286 + b289 >= 1;

e1874:    b264 + b274 + b279 + b285 + b299 >= 1;

e1875:    b264 + b274 + b279 + b285 + b294 >= 1;

e1876:    b264 + b274 + b279 + b285 + b289 >= 1;

e1877:    b264 + b274 + b278 + b298 >= 1;

e1878:    b264 + b274 + b278 + b294 + b299 >= 1;

e1879:    b264 + b274 + b278 + b293 >= 1;

e1880:    b264 + b274 + b278 + b289 >= 1;

e1881:    b264 + b274 + b278 + b286 + b299 >= 1;

e1882:    b264 + b274 + b278 + b286 + b294 >= 1;

e1883:    b264 + b274 + b278 + b286 + b289 >= 1;

e1884:    b264 + b274 + b277 + b299 >= 1;

e1885:    b264 + b274 + b277 + b294 >= 1;

e1886:    b264 + b274 + b277 + b289 >= 1;

e1887:    b264 + b273 + b297 >= 1;

e1888:    b264 + b273 + b294 + b298 >= 1;

e1889:    b264 + b273 + b293 + b299 >= 1;

e1890:    b264 + b273 + b292 >= 1;

e1891:    b264 + b273 + b289 + b299 >= 1;

e1892:    b264 + b273 + b289 + b294 >= 1;

e1893:    b264 + b273 + b288 >= 1;

e1894:    b264 + b273 + b286 + b298 >= 1;

e1895:    b264 + b273 + b286 + b294 + b299 >= 1;

e1896:    b264 + b273 + b286 + b293 >= 1;

e1897:    b264 + b273 + b286 + b289 >= 1;

e1898:    b264 + b273 + b285 + b299 >= 1;

e1899:    b264 + b273 + b285 + b294 >= 1;

e1900:    b264 + b273 + b285 + b289 >= 1;

e1901:    b264 + b273 + b280 + b298 >= 1;

e1902:    b264 + b273 + b280 + b294 + b299 >= 1;

e1903:    b264 + b273 + b280 + b293 >= 1;

e1904:    b264 + b273 + b280 + b289 >= 1;

e1905:    b264 + b273 + b280 + b286 + b299 >= 1;

e1906:    b264 + b273 + b280 + b286 + b294 >= 1;

e1907:    b264 + b273 + b280 + b286 + b289 >= 1;

e1908:    b264 + b273 + b279 + b299 >= 1;

e1909:    b264 + b273 + b279 + b294 >= 1;

e1910:    b264 + b273 + b279 + b289 >= 1;

e1911:    b264 + b272 + b299 >= 1;

e1912:    b264 + b272 + b294 >= 1;

e1913:    b264 + b272 + b289 >= 1;

e1914:    b264 + b272 + b280 + b299 >= 1;

e1915:    b264 + b272 + b280 + b294 >= 1;

e1916:    b264 + b272 + b280 + b289 >= 1;

e1917:    b264 + b270 + b297 >= 1;

e1918:    b264 + b270 + b293 + b298 >= 1;

e1919:    b264 + b270 + b292 >= 1;

e1920:    b264 + b270 + b289 + b298 >= 1;

e1921:    b264 + b270 + b289 + b294 + b299 >= 1;

e1922:    b264 + b270 + b289 + b293 >= 1;

e1923:    b264 + b270 + b288 >= 1;

e1924:    b264 + b270 + b286 + b297 >= 1;

e1925:    b264 + b270 + b286 + b294 + b298 >= 1;

e1926:    b264 + b270 + b286 + b293 + b299 >= 1;

e1927:    b264 + b270 + b286 + b292 >= 1;

e1928:    b264 + b270 + b286 + b289 + b299 >= 1;

e1929:    b264 + b270 + b286 + b289 + b294 >= 1;

e1930:    b264 + b270 + b286 + b288 >= 1;

e1931:    b264 + b270 + b285 + b298 >= 1;

e1932:    b264 + b270 + b285 + b294 + b299 >= 1;

e1933:    b264 + b270 + b285 + b293 >= 1;

e1934:    b264 + b270 + b285 + b289 >= 1;

e1935:    b264 + b270 + b284 + b299 >= 1;

e1936:    b264 + b270 + b284 + b294 >= 1;

e1937:    b264 + b270 + b284 + b289 >= 1;

e1938:    b264 + b270 + b280 + b297 >= 1;

e1939:    b264 + b270 + b280 + b294 + b298 >= 1;

e1940:    b264 + b270 + b280 + b293 + b299 >= 1;

e1941:    b264 + b270 + b280 + b292 >= 1;

e1942:    b264 + b270 + b280 + b289 + b299 >= 1;

e1943:    b264 + b270 + b280 + b289 + b294 >= 1;

e1944:    b264 + b270 + b280 + b288 >= 1;

e1945:    b264 + b270 + b280 + b286 + b298 >= 1;

e1946:    b264 + b270 + b280 + b286 + b294 + b299 >= 1;

e1947:    b264 + b270 + b280 + b286 + b293 >= 1;

e1948:    b264 + b270 + b280 + b286 + b289 >= 1;

e1949:    b264 + b270 + b280 + b285 + b299 >= 1;

e1950:    b264 + b270 + b280 + b285 + b294 >= 1;

e1951:    b264 + b270 + b280 + b285 + b289 >= 1;

e1952:    b264 + b270 + b279 + b298 >= 1;

e1953:    b264 + b270 + b279 + b294 + b299 >= 1;

e1954:    b264 + b270 + b279 + b293 >= 1;

e1955:    b264 + b270 + b279 + b289 >= 1;

e1956:    b264 + b270 + b279 + b286 + b299 >= 1;

e1957:    b264 + b270 + b279 + b286 + b294 >= 1;

e1958:    b264 + b270 + b279 + b286 + b289 >= 1;

e1959:    b264 + b270 + b278 + b299 >= 1;

e1960:    b264 + b270 + b278 + b294 >= 1;

e1961:    b264 + b270 + b278 + b289 >= 1;

e1962:    b264 + b270 + b274 + b298 >= 1;

e1963:    b264 + b270 + b274 + b294 + b299 >= 1;

e1964:    b264 + b270 + b274 + b293 >= 1;

e1965:    b264 + b270 + b274 + b289 >= 1;

e1966:    b264 + b270 + b274 + b286 + b299 >= 1;

e1967:    b264 + b270 + b274 + b286 + b294 >= 1;

e1968:    b264 + b270 + b274 + b286 + b289 >= 1;

e1969:    b264 + b270 + b274 + b285 + b299 >= 1;

e1970:    b264 + b270 + b274 + b285 + b294 >= 1;

e1971:    b264 + b270 + b274 + b285 + b289 >= 1;

e1972:    b264 + b270 + b274 + b280 + b299 >= 1;

e1973:    b264 + b270 + b274 + b280 + b294 >= 1;

e1974:    b264 + b270 + b274 + b280 + b289 >= 1;

e1975:    b264 + b270 + b274 + b280 + b286 + b299 >= 1;

e1976:    b264 + b270 + b274 + b280 + b286 + b294 >= 1;

e1977:    b264 + b270 + b274 + b280 + b286 + b289 >= 1;

e1978:    b264 + b270 + b274 + b279 + b299 >= 1;

e1979:    b264 + b270 + b274 + b279 + b294 >= 1;

e1980:    b264 + b270 + b274 + b279 + b289 >= 1;

e1981:    b264 + b270 + b273 + b299 >= 1;

e1982:    b264 + b270 + b273 + b294 >= 1;

e1983:    b264 + b270 + b273 + b289 >= 1;

e1984:    b264 + b269 + b299 >= 1;

e1985:    b264 + b269 + b294 >= 1;

e1986:    b264 + b269 + b289 >= 1;

e1987:    b264 + b267 + b297 >= 1;

e1988:    b264 + b267 + b294 + b298 >= 1;

e1989:    b264 + b267 + b293 + b299 >= 1;

e1990:    b264 + b267 + b292 >= 1;

e1991:    b264 + b267 + b289 + b299 >= 1;

e1992:    b264 + b267 + b289 + b294 >= 1;

e1993:    b264 + b267 + b288 >= 1;

e1994:    b264 + b267 + b286 + b298 >= 1;

e1995:    b264 + b267 + b286 + b294 + b299 >= 1;

e1996:    b264 + b267 + b286 + b293 >= 1;

e1997:    b264 + b267 + b286 + b289 >= 1;

e1998:    b264 + b267 + b285 + b298 >= 1;

e1999:    b264 + b267 + b285 + b294 + b299 >= 1;

e2000:    b264 + b267 + b285 + b293 >= 1;

e2001:    b264 + b267 + b285 + b289 >= 1;

e2002:    b264 + b267 + b284 + b299 >= 1;

e2003:    b264 + b267 + b284 + b294 >= 1;

e2004:    b264 + b267 + b284 + b289 >= 1;

e2005:    b264 + b267 + b280 + b298 >= 1;

e2006:    b264 + b267 + b280 + b294 + b299 >= 1;

e2007:    b264 + b267 + b280 + b293 >= 1;

e2008:    b264 + b267 + b280 + b289 >= 1;

e2009:    b264 + b267 + b280 + b286 + b298 >= 1;

e2010:    b264 + b267 + b280 + b286 + b294 + b299 >= 1;

e2011:    b264 + b267 + b280 + b286 + b293 >= 1;

e2012:    b264 + b267 + b280 + b286 + b289 >= 1;

e2013:    b264 + b267 + b280 + b285 + b299 >= 1;

e2014:    b264 + b267 + b280 + b285 + b294 >= 1;

e2015:    b264 + b267 + b280 + b285 + b289 >= 1;

e2016:    b264 + b267 + b279 + b298 >= 1;

e2017:    b264 + b267 + b279 + b294 + b299 >= 1;

e2018:    b264 + b267 + b279 + b293 >= 1;

e2019:    b264 + b267 + b279 + b289 >= 1;

e2020:    b264 + b267 + b279 + b286 + b299 >= 1;

e2021:    b264 + b267 + b279 + b286 + b294 >= 1;

e2022:    b264 + b267 + b279 + b286 + b289 >= 1;

e2023:    b264 + b267 + b278 + b299 >= 1;

e2024:    b264 + b267 + b278 + b294 >= 1;

e2025:    b264 + b267 + b278 + b289 >= 1;

e2026:    b264 + b267 + b274 + b298 >= 1;

e2027:    b264 + b267 + b274 + b294 + b299 >= 1;

e2028:    b264 + b267 + b274 + b293 >= 1;

e2029:    b264 + b267 + b274 + b289 >= 1;

e2030:    b264 + b267 + b274 + b286 + b299 >= 1;

e2031:    b264 + b267 + b274 + b286 + b294 >= 1;

e2032:    b264 + b267 + b274 + b286 + b289 >= 1;

e2033:    b264 + b267 + b274 + b285 + b299 >= 1;

e2034:    b264 + b267 + b274 + b285 + b294 >= 1;

e2035:    b264 + b267 + b274 + b285 + b289 >= 1;

e2036:    b264 + b267 + b274 + b280 + b299 >= 1;

e2037:    b264 + b267 + b274 + b280 + b294 >= 1;

e2038:    b264 + b267 + b274 + b280 + b289 >= 1;

e2039:    b264 + b267 + b273 + b299 >= 1;

e2040:    b264 + b267 + b273 + b294 >= 1;

e2041:    b264 + b267 + b273 + b289 >= 1;

e2042:    b264 + b267 + b270 + b299 >= 1;

e2043:    b264 + b267 + b270 + b294 >= 1;

e2044:    b264 + b267 + b270 + b289 >= 1;

e2045:    b264 + b267 + b270 + b286 + b299 >= 1;

e2046:    b264 + b267 + b270 + b286 + b294 >= 1;

e2047:    b264 + b267 + b270 + b286 + b289 >= 1;

e2048:    b264 + b267 + b270 + b280 + b299 >= 1;

e2049:    b264 + b267 + b270 + b280 + b294 >= 1;

e2050:    b264 + b267 + b270 + b280 + b289 >= 1;

e2051:    b264 + b266 + b299 >= 1;

e2052:    b264 + b266 + b294 >= 1;

e2053:    b264 + b266 + b289 >= 1;

e2054:    b263 + b297 >= 1;

e2055:    b263 + b294 + b298 >= 1;

e2056:    b263 + b293 + b299 >= 1;

e2057:    b263 + b292 >= 1;

e2058:    b263 + b289 + b299 >= 1;

e2059:    b263 + b289 + b294 >= 1;

e2060:    b263 + b288 >= 1;

e2061:    b263 + b286 + b298 >= 1;

e2062:    b263 + b286 + b294 + b299 >= 1;

e2063:    b263 + b286 + b293 >= 1;

e2064:    b263 + b286 + b289 >= 1;

e2065:    b263 + b285 + b298 >= 1;

e2066:    b263 + b285 + b294 + b299 >= 1;

e2067:    b263 + b285 + b293 >= 1;

e2068:    b263 + b285 + b289 >= 1;

e2069:    b263 + b284 + b299 >= 1;

e2070:    b263 + b284 + b294 >= 1;

e2071:    b263 + b284 + b289 >= 1;

e2072:    b263 + b280 + b298 >= 1;

e2073:    b263 + b280 + b293 >= 1;

e2074:    b263 + b280 + b289 >= 1;

e2075:    b263 + b280 + b286 + b298 >= 1;

e2076:    b263 + b280 + b286 + b294 + b299 >= 1;

e2077:    b263 + b280 + b286 + b293 >= 1;

e2078:    b263 + b280 + b286 + b289 >= 1;

e2079:    b263 + b280 + b285 + b299 >= 1;

e2080:    b263 + b280 + b285 + b294 >= 1;

e2081:    b263 + b280 + b285 + b289 >= 1;

e2082:    b263 + b279 + b298 >= 1;

e2083:    b263 + b279 + b294 + b299 >= 1;

e2084:    b263 + b279 + b293 >= 1;

e2085:    b263 + b279 + b289 >= 1;

e2086:    b263 + b279 + b286 + b299 >= 1;

e2087:    b263 + b279 + b286 + b294 >= 1;

e2088:    b263 + b279 + b286 + b289 >= 1;

e2089:    b263 + b278 + b299 >= 1;

e2090:    b263 + b278 + b294 >= 1;

e2091:    b263 + b278 + b289 >= 1;

e2092:    b263 + b274 + b298 >= 1;

e2093:    b263 + b274 + b294 + b299 >= 1;

e2094:    b263 + b274 + b293 >= 1;

e2095:    b263 + b274 + b289 >= 1;

e2096:    b263 + b274 + b286 + b299 >= 1;

e2097:    b263 + b274 + b286 + b294 >= 1;

e2098:    b263 + b274 + b286 + b289 >= 1;

e2099:    b263 + b274 + b280 + b299 >= 1;

e2100:    b263 + b274 + b280 + b294 >= 1;

e2101:    b263 + b274 + b280 + b289 >= 1;

e2102:    b263 + b273 + b299 >= 1;

e2103:    b263 + b273 + b294 >= 1;

e2104:    b263 + b273 + b289 >= 1;

e2105:    b263 + b270 + b299 >= 1;

e2106:    b263 + b270 + b294 >= 1;

e2107:    b263 + b270 + b289 >= 1;

e2108:    b263 + b267 + b299 >= 1;

e2109:    b263 + b267 + b294 >= 1;

e2110:    b263 + b267 + b289 >= 1;

e2111:    b262 + b299 >= 1;

e2112:    b262 + b294 >= 1;

e2113:    b262 + b289 >= 1;

e2114:    x46 - 1.34666666666667*b262 >= 0;

e2115:    x46 - 1.92*b263 >= 0;

e2116:    x46 - 2.02*b264 >= 0;

e2117:    x47 - 2.67333333333333*b265 >= 0;

e2118:    x47 - 3.82*b266 >= 0;

e2119:    x47 - 4.01333333333333*b267 >= 0;

e2120:    x48 - 3.17333333333333*b268 >= 0;

e2121:    x48 - 4.53333333333333*b269 >= 0;

e2122:    x48 - 4.76*b270 >= 0;

e2123:    x49 - 3.97333333333333*b271 >= 0;

e2124:    x49 - 5.39333333333333*b272 >= 0;

e2125:    x49 - 5.68*b273 >= 0;

e2126:    x49 - 5.96*b274 >= 0;

e2127:    x50 - 26.7866666666667*b275 >= 0;

e2128:    x50 - 34.44*b276 >= 0;

e2129:    x50 - 36.3533333333333*b277 >= 0;

e2130:    x50 - 38.2666666666667*b278 >= 0;

e2131:    x50 - 40.18*b279 >= 0;

e2132:    x50 - 42.0933333333333*b280 >= 0;

e2133:    x51 - 63.18*b281 >= 0;

e2134:    x51 - 81.2333333333333*b282 >= 0;

e2135:    x51 - 85.7466666666667*b283 >= 0;

e2136:    x51 - 90.2533333333333*b284 >= 0;

e2137:    x51 - 94.7666666666667*b285 >= 0;

e2138:    x51 - 99.28*b286 >= 0;

e2139:    x52 - 4.39333333333333*b287 >= 0;

e2140:    x52 - 6.28*b288 >= 0;

e2141:    x52 - 6.59333333333333*b289 >= 0;

e2142:    x53 - 39.3733333333333*b290 >= 0;

e2143:    x53 - 53.4333333333333*b291 >= 0;

e2144:    x53 - 56.24*b292 >= 0;

e2145:    x53 - 59.0533333333333*b293 >= 0;

e2146:    x53 - 61.8666666666667*b294 >= 0;

e2147:    x54 - 35.82*b295 >= 0;

e2148:    x54 - 48.6133333333333*b296 >= 0;

e2149:    x54 - 51.1733333333333*b297 >= 0;

e2150:    x54 - 53.7333333333333*b298 >= 0;

e2151:    x54 - 56.2866666666667*b299 >= 0;

e2152:    x55 - 26.4066666666667*b300 >= 0;

e2153:    x55 - 33.9533333333333*b301 >= 0;

e2154:    x55 - 35.84*b302 >= 0;

e2155:    x55 - 37.7266666666667*b303 >= 0;

e2156:    x55 - 39.6133333333333*b304 >= 0;

e2157:    x55 - 41.5*b305 >= 0;

e2158:    x56 - 39.7666666666667*b306 >= 0;

e2159:    x56 - 53.9666666666667*b307 >= 0;

e2160:    x56 - 56.8066666666667*b308 >= 0;

e2161:    x56 - 59.6466666666667*b309 >= 0;

e2162:    x56 - 62.4933333333333*b310 >= 0;

e2163:    x57 - 53.94*b311 >= 0;

e2164:    x57 - 77.0533333333333*b312 >= 0;

e2165:    x57 - 80.9066666666667*b313 >= 0;

e2166:    x58 - 17.4333333333333*b314 >= 0;

e2167:    x58 - 24.9066666666667*b315 >= 0;

e2168:    x58 - 26.1466666666667*b316 >= 0;

e2169:    x59 - 25.3333333333333*b317 >= 0;

e2170:    x59 - 36.1866666666667*b318 >= 0;

e2171:    x59 - 38*b319 >= 0;

e2172:    x60 - 41.4933333333333*b320 >= 0;

e2173:    x60 - 56.3133333333333*b321 >= 0;

e2174:    x60 - 59.2733333333333*b322 >= 0;

e2175:    x60 - 62.24*b323 >= 0;

e2176:  - x106 + x217 <= 0;

e2177:  - x106 + x218 <= 0;

e2178:  - x106 + x219 <= 0;

e2179:  - x107 + x220 <= 0;

e2180:  - x107 + x221 <= 0;

e2181:  - x107 + x222 <= 0;

e2182:  - x108 + x223 <= 0;

e2183:  - x108 + x224 <= 0;

e2184:  - x108 + x225 <= 0;

e2185:  - x109 + x226 <= 0;

e2186:  - x109 + x227 <= 0;

e2187:  - x109 + x228 <= 0;

e2188:  - x110 + x229 <= 0;

e2189:  - x110 + x230 <= 0;

e2190:  - x110 + x231 <= 0;

e2191:  - x111 + x232 <= 0;

e2192:  - x111 + x233 <= 0;

e2193:  - x111 + x234 <= 0;

e2194:  - x112 + x235 <= 0;

e2195:  - x112 + x236 <= 0;

e2196:  - x112 + x237 <= 0;

e2197:  - x113 + x238 <= 0;

e2198:  - x113 + x239 <= 0;

e2199:  - x113 + x240 <= 0;

e2200:  - x114 + x241 <= 0;

e2201:  - x114 + x242 <= 0;

e2202:  - x114 + x243 <= 0;

e2203:  - x115 + x244 <= 0;

e2204:  - x115 + x245 <= 0;

e2205:  - x115 + x246 <= 0;

e2206:  - x116 + x247 <= 0;

e2207:  - x116 + x248 <= 0;

e2208:  - x116 + x249 <= 0;

e2209:  - x117 + x250 <= 0;

e2210:  - x117 + x251 <= 0;

e2211:  - x117 + x252 <= 0;

e2212:  - x118 + x253 <= 0;

e2213:  - x118 + x254 <= 0;

e2214:  - x118 + x255 <= 0;

e2215:  - x119 + x256 <= 0;

e2216:  - x119 + x257 <= 0;

e2217:  - x119 + x258 <= 0;

e2218:  - x120 + x259 <= 0;

e2219:  - x120 + x260 <= 0;

e2220:  - x120 + x261 <= 0;

e2221:    b262 - b263 >= 0;

e2222:    b263 - b264 >= 0;

e2223:    b265 - b266 >= 0;

e2224:    b266 - b267 >= 0;

e2225:    b268 - b269 >= 0;

e2226:    b269 - b270 >= 0;

e2227:    b271 - b272 >= 0;

e2228:    b272 - b273 >= 0;

e2229:    b273 - b274 >= 0;

e2230:    b275 - b276 >= 0;

e2231:    b276 - b277 >= 0;

e2232:    b277 - b278 >= 0;

e2233:    b278 - b279 >= 0;

e2234:    b279 - b280 >= 0;

e2235:    b281 - b282 >= 0;

e2236:    b282 - b283 >= 0;

e2237:    b283 - b284 >= 0;

e2238:    b284 - b285 >= 0;

e2239:    b285 - b286 >= 0;

e2240:    b287 - b288 >= 0;

e2241:    b288 - b289 >= 0;

e2242:    b290 - b291 >= 0;

e2243:    b291 - b292 >= 0;

e2244:    b292 - b293 >= 0;

e2245:    b293 - b294 >= 0;

e2246:    b295 - b296 >= 0;

e2247:    b296 - b297 >= 0;

e2248:    b297 - b298 >= 0;

e2249:    b298 - b299 >= 0;

e2250:    b300 - b301 >= 0;

e2251:    b301 - b302 >= 0;

e2252:    b302 - b303 >= 0;

e2253:    b303 - b304 >= 0;

e2254:    b304 - b305 >= 0;

e2255:    b306 - b307 >= 0;

e2256:    b307 - b308 >= 0;

e2257:    b308 - b309 >= 0;

e2258:    b309 - b310 >= 0;

e2259:    b311 - b312 >= 0;

e2260:    b312 - b313 >= 0;

e2261:    b314 - b315 >= 0;

e2262:    b315 - b316 >= 0;

e2263:    b317 - b318 >= 0;

e2264:    b318 - b319 >= 0;

e2265:    b320 - b321 >= 0;

e2266:    b321 - b322 >= 0;

e2267:    b322 - b323 >= 0;

e2268:    x124 - x125 >= 0;

e2269:    x125 - x126 >= 0;