#  MINLP written by GAMS Convert at 01/12/18 13:42:22
#  
#  Equation counts
#      Total        E        G        L        N        X        C        B
#       2166       46     2088       32        0        0        0        0
#  
#  Variable counts
#                   x        b        i      s1s      s2s       sc       si
#      Total     cont   binary  integer     sos1     sos2    scont     sint
#        247      155       92        0        0        0        0        0
#  FX      0        0        0        0        0        0        0        0
#  
#  Nonzero counts
#      Total    const       NL      DLL
#       7694     7604       90        0
# 
#  Reformulation has removed 1 variable and 1 equation


var x1 >= 0, <= 0.26351883;
var x2 >= 0, <= 0.26351883;
var x3 >= 0, <= 0.22891574;
var x4 >= 0, <= 0.22891574;
var x5 >= 0, <= 0.21464835;
var x6 >= 0, <= 0.21464835;
var x7 >= 0, <= 0.17964414;
var x8 >= 0, <= 0.17964414;
var x9 >= 0, <= 0.17402843;
var x10 >= 0, <= 0.17402843;
var x11 >= 0, <= 0.15355962;
var x12 >= 0, <= 0.15355962;
var x13 >= 0, <= 0.1942283;
var x14 >= 0, <= 0.1942283;
var x15 >= 0, <= 0.25670555;
var x16 >= 0, <= 0.25670555;
var x17 >= 0, <= 0.27088619;
var x18 >= 0, <= 0.27088619;
var x19 >= 0, <= 0.28985675;
var x20 >= 0, <= 0.28985675;
var x21 >= 0, <= 0.25550303;
var x22 >= 0, <= 0.25550303;
var x23 >= 0, <= 0.19001726;
var x24 >= 0, <= 0.19001726;
var x25 >= 0, <= 0.23803143;
var x26 >= 0, <= 0.23803143;
var x27 >= 0, <= 0.23312962;
var x28 >= 0, <= 0.23312962;
var x29 >= 0, <= 0.27705307;
var x30 >= 0, <= 0.27705307;
var x31 := 1.24666666666667, >= 1.24666666666667, <= 2.02;
var x32 := 2.48, >= 2.48, <= 4.01333333333333;
var x33 := 2.94666666666667, >= 2.94666666666667, <= 4.76;
var x34 := 3.69333333333333, >= 3.69333333333333, <= 5.96;
var x35 := 24.8733333333333, >= 24.8733333333333, <= 42.0933333333333;
var x36 := 58.6666666666667, >= 58.6666666666667, <= 99.28;
var x37 := 4.08, >= 4.08, <= 6.59333333333333;
var x38 := 36.56, >= 36.56, <= 61.8666666666667;
var x39 := 33.26, >= 33.26, <= 56.2866666666667;
var x40 := 24.52, >= 24.52, <= 41.5;
var x41 := 36.9266666666667, >= 36.9266666666667, <= 62.4933333333333;
var x42 := 50.0866666666667, >= 50.0866666666667, <= 80.9066666666667;
var x43 := 16.1866666666667, >= 16.1866666666667, <= 26.1466666666667;
var x44 := 23.52, >= 23.52, <= 38;
var x45 := 38.5266666666667, >= 38.5266666666667, <= 62.24;
var b46 binary >= 0, <= 1;
var b47 binary >= 0, <= 1;
var b48 binary >= 0, <= 1;
var b49 binary >= 0, <= 1;
var b50 binary >= 0, <= 1;
var b51 binary >= 0, <= 1;
var b52 binary >= 0, <= 1;
var b53 binary >= 0, <= 1;
var b54 binary >= 0, <= 1;
var b55 binary >= 0, <= 1;
var b56 binary >= 0, <= 1;
var b57 binary >= 0, <= 1;
var b58 binary >= 0, <= 1;
var b59 binary >= 0, <= 1;
var b60 binary >= 0, <= 1;
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 x76 >= 0, <= 0.5323080366;
var x77 >= 0, <= 0.918715169866666;
var x78 >= 0, <= 1.021726146;
var x79 >= 0, <= 1.0706790744;
var x80 >= 0, <= 7.32543671346667;
var x81 >= 0, <= 15.2453990736;
var x82 >= 0, <= 1.28061192466667;
var x83 >= 0, <= 15.8815166933333;
var x84 >= 0, <= 15.2472806811333;
var x85 >= 0, <= 12.029055125;
var x86 >= 0, <= 15.9672360214667;
var x87 >= 0, <= 15.3736631157333;
var x88 >= 0, <= 6.2237284564;
var x89 >= 0, <= 8.85892556;
var x90 >= 0, <= 17.2437830768;
var x91 := 0.25788969, >= 0.25788969, <= 0.35227087;
var x92 := 0.25788969, >= 0.25788969, <= 0.35227087;
var x93 := -0.7794471, >= -0.98493628, <= -0.7794471;
var x94 := -0.7794471, >= -0.98493628, <= -0.7794471;
var x95 >= 0, <= 0.0580296499999999;
var x96 >= 0, <= 0.0580296499999999;
var x97 >= 0, <= 0.0546689399999999;
var x98 >= 0, <= 0.0546689399999999;
var x99 >= 0, <= 0.09360565;
var x100 >= 0, <= 0.09360565;
var x101 >= 0, <= 0.0476880399999999;
var x102 >= 0, <= 0.0476880399999999;
var x103 >= 0, <= 0.05276021;
var x104 >= 0, <= 0.05276021;
var x105 >= 0, <= 0.04905388;
var x106 >= 0, <= 0.04905388;
var x107 >= 0, <= 0.07731692;
var x108 >= 0, <= 0.07731692;
var x109 >= 0, <= 0.08211741;
var x110 >= 0, <= 0.08211741;
var x111 >= 0, <= 0.09438118;
var x112 >= 0, <= 0.09438118;
var x113 >= 0, <= 0.08436757;
var x114 >= 0, <= 0.08436757;
var x115 >= 0, <= 0.06987597;
var x116 >= 0, <= 0.06987597;
var x117 >= 0, <= 0.04788831;
var x118 >= 0, <= 0.04788831;
var x119 >= 0, <= 0.0668875099999999;
var x120 >= 0, <= 0.0668875099999999;
var x121 >= 0, <= 0.07276512;
var x122 >= 0, <= 0.07276512;
var x123 >= 0, <= 0.09438118;
var x124 >= 0, <= 0.09438118;
var x125 >= 0, <= 0.20548918;
var x126 >= 0, <= 0.20548918;
var x127 >= 0, <= 0.1742468;
var x128 >= 0, <= 0.1742468;
var x129 >= 0, <= 0.1210427;
var x130 >= 0, <= 0.1210427;
var x131 >= 0, <= 0.1319561;
var x132 >= 0, <= 0.1319561;
var x133 >= 0, <= 0.12126822;
var x134 >= 0, <= 0.12126822;
var x135 >= 0, <= 0.10450574;
var x136 >= 0, <= 0.10450574;
var x137 >= 0, <= 0.11691138;
var x138 >= 0, <= 0.11691138;
var x139 >= 0, <= 0.17458814;
var x140 >= 0, <= 0.17458814;
var x141 >= 0, <= 0.17650501;
var x142 >= 0, <= 0.17650501;
var x143 >= 0, <= 0.20548918;
var x144 >= 0, <= 0.20548918;
var x145 >= 0, <= 0.18562706;
var x146 >= 0, <= 0.18562706;
var x147 >= 0, <= 0.14212895;
var x148 >= 0, <= 0.14212895;
var x149 >= 0, <= 0.17114392;
var x150 >= 0, <= 0.17114392;
var x151 >= 0, <= 0.1603645;
var x152 >= 0, <= 0.1603645;
var x153 >= 0, <= 0.18267189;
var x154 >= 0, <= 0.18267189;
var x155 >= 0, <= 0.5323080366;
var x156 >= 0, <= 0.5323080366;
var x157 >= 0, <= 0.918715169866666;
var x158 >= 0, <= 0.918715169866666;
var x159 >= 0, <= 1.021726146;
var x160 >= 0, <= 1.021726146;
var x161 >= 0, <= 1.0706790744;
var x162 >= 0, <= 1.0706790744;
var x163 >= 0, <= 7.32543671346667;
var x164 >= 0, <= 7.32543671346667;
var x165 >= 0, <= 15.2453990736;
var x166 >= 0, <= 15.2453990736;
var x167 >= 0, <= 1.28061192466667;
var x168 >= 0, <= 1.28061192466667;
var x169 >= 0, <= 15.8815166933333;
var x170 >= 0, <= 15.8815166933333;
var x171 >= 0, <= 15.2472806811333;
var x172 >= 0, <= 15.2472806811333;
var x173 >= 0, <= 12.029055125;
var x174 >= 0, <= 12.029055125;
var x175 >= 0, <= 15.9672360214667;
var x176 >= 0, <= 15.9672360214667;
var x177 >= 0, <= 15.3736631157333;
var x178 >= 0, <= 15.3736631157333;
var x179 >= 0, <= 6.2237284564;
var x180 >= 0, <= 6.2237284564;
var x181 >= 0, <= 8.85892556;
var x182 >= 0, <= 8.85892556;
var x183 >= 0, <= 17.2437830768;
var x184 >= 0, <= 17.2437830768;
var b185 binary >= 0, <= 1;
var b186 binary >= 0, <= 1;
var b187 binary >= 0, <= 1;
var b188 binary >= 0, <= 1;
var b189 binary >= 0, <= 1;
var b190 binary >= 0, <= 1;
var b191 binary >= 0, <= 1;
var b192 binary >= 0, <= 1;
var b193 binary >= 0, <= 1;
var b194 binary >= 0, <= 1;
var b195 binary >= 0, <= 1;
var b196 binary >= 0, <= 1;
var b197 binary >= 0, <= 1;
var b198 binary >= 0, <= 1;
var b199 binary >= 0, <= 1;
var b200 binary >= 0, <= 1;
var b201 binary >= 0, <= 1;
var b202 binary >= 0, <= 1;
var b203 binary >= 0, <= 1;
var b204 binary >= 0, <= 1;
var b205 binary >= 0, <= 1;
var b206 binary >= 0, <= 1;
var b207 binary >= 0, <= 1;
var b208 binary >= 0, <= 1;
var b209 binary >= 0, <= 1;
var b210 binary >= 0, <= 1;
var b211 binary >= 0, <= 1;
var b212 binary >= 0, <= 1;
var b213 binary >= 0, <= 1;
var b214 binary >= 0, <= 1;
var b215 binary >= 0, <= 1;
var b216 binary >= 0, <= 1;
var b217 binary >= 0, <= 1;
var b218 binary >= 0, <= 1;
var b219 binary >= 0, <= 1;
var b220 binary >= 0, <= 1;
var b221 binary >= 0, <= 1;
var b222 binary >= 0, <= 1;
var b223 binary >= 0, <= 1;
var b224 binary >= 0, <= 1;
var b225 binary >= 0, <= 1;
var b226 binary >= 0, <= 1;
var b227 binary >= 0, <= 1;
var b228 binary >= 0, <= 1;
var b229 binary >= 0, <= 1;
var b230 binary >= 0, <= 1;
var b231 binary >= 0, <= 1;
var b232 binary >= 0, <= 1;
var b233 binary >= 0, <= 1;
var b234 binary >= 0, <= 1;
var b235 binary >= 0, <= 1;
var b236 binary >= 0, <= 1;
var b237 binary >= 0, <= 1;
var b238 binary >= 0, <= 1;
var b239 binary >= 0, <= 1;
var b240 binary >= 0, <= 1;
var b241 binary >= 0, <= 1;
var b242 binary >= 0, <= 1;
var b243 binary >= 0, <= 1;
var b244 binary >= 0, <= 1;
var b245 binary >= 0, <= 1;
var b246 binary >= 0, <= 1;

minimize obj:    x76 + x77 + x78 + x79 + x80 + x81 + x82 + x83 + x84 + x85
     + x86 + x87 + x88 + x89 + x90;

subject to

e2: -x31*x1*b46 + x155 >= 0;

e3: -x31*x2*b47 + x156 >= 0;

e4: -x32*x3*b48 + x157 >= 0;

e5: -x32*x4*b49 + x158 >= 0;

e6: -x33*x5*b50 + x159 >= 0;

e7: -x33*x6*b51 + x160 >= 0;

e8: -x34*x7*b52 + x161 >= 0;

e9: -x34*x8*b53 + x162 >= 0;

e10: -x35*x9*b54 + x163 >= 0;

e11: -x35*x10*b55 + x164 >= 0;

e12: -x36*x11*b56 + x165 >= 0;

e13: -x36*x12*b57 + x166 >= 0;

e14: -x37*x13*b58 + x167 >= 0;

e15: -x37*x14*b59 + x168 >= 0;

e16: -x38*x15*b60 + x169 >= 0;

e17: -x38*x16*b61 + x170 >= 0;

e18: -x39*x17*b62 + x171 >= 0;

e19: -x39*x18*b63 + x172 >= 0;

e20: -x40*x19*b64 + x173 >= 0;

e21: -x40*x20*b65 + x174 >= 0;

e22: -x41*x21*b66 + x175 >= 0;

e23: -x41*x22*b67 + x176 >= 0;

e24: -x42*x23*b68 + x177 >= 0;

e25: -x42*x24*b69 + x178 >= 0;

e26: -x43*x25*b70 + x179 >= 0;

e27: -x43*x26*b71 + x180 >= 0;

e28: -x44*x27*b72 + x181 >= 0;

e29: -x44*x28*b73 + x182 >= 0;

e30: -x45*x29*b74 + x183 >= 0;

e31: -x45*x30*b75 + x184 >= 0;

e32:    b46 + b47 = 1;

e33:    b48 + b49 = 1;

e34:    b50 + b51 = 1;

e35:    b52 + b53 = 1;

e36:    b54 + b55 = 1;

e37:    b56 + b57 = 1;

e38:    b58 + b59 = 1;

e39:    b60 + b61 = 1;

e40:    b62 + b63 = 1;

e41:    b64 + b65 = 1;

e42:    b66 + b67 = 1;

e43:    b68 + b69 = 1;

e44:    b70 + b71 = 1;

e45:    b72 + b73 = 1;

e46:    b74 + b75 = 1;

e47:    2.02*b46 + 4.01333333333333*b48 + 4.76*b50 + 5.96*b52
      + 42.0933333333333*b54 + 99.28*b56 + 6.59333333333333*b58
      + 61.8666666666667*b60 + 56.2866666666667*b62 + 41.5*b64
      + 62.4933333333333*b66 + 80.9066666666667*b68 + 26.1466666666667*b70
      + 38*b72 + 62.24*b74 <= 302.08;

e48:    2.02*b47 + 4.01333333333333*b49 + 4.76*b51 + 5.96*b53
      + 42.0933333333333*b55 + 99.28*b57 + 6.59333333333333*b59
      + 61.8666666666667*b61 + 56.2866666666667*b63 + 41.5*b65
      + 62.4933333333333*b67 + 80.9066666666667*b69 + 26.1466666666667*b71
      + 38*b73 + 62.24*b75 <= 302.08;

e49:    x91 + x95 >= 0.29424122;

e50:    x92 + x96 >= 0.29424122;

e51:    x91 + x97 >= 0.29760193;

e52:    x92 + x98 >= 0.29760193;

e53:    x91 + x99 >= 0.35149534;

e54:    x92 + x100 >= 0.35149534;

e55:    x91 + x101 >= 0.30458283;

e56:    x92 + x102 >= 0.30458283;

e57:    x91 + x103 >= 0.29951066;

e58:    x92 + x104 >= 0.29951066;

e59:    x91 + x105 >= 0.30694357;

e60:    x92 + x106 >= 0.30694357;

e61:    x91 + x107 >= 0.33520661;

e62:    x92 + x108 >= 0.33520661;

e63:    x91 + x109 >= 0.3400071;

e64:    x92 + x110 >= 0.3400071;

e65:    x91 + x111 >= 0.35227087;

e66:    x92 + x112 >= 0.35227087;

e67:    x91 + x113 >= 0.34225726;

e68:    x92 + x114 >= 0.34225726;

e69:    x91 + x115 >= 0.32776566;

e70:    x92 + x116 >= 0.32776566;

e71:    x91 + x117 >= 0.30438256;

e72:    x92 + x118 >= 0.30438256;

e73:    x91 + x119 >= 0.28538336;

e74:    x92 + x120 >= 0.28538336;

e75:    x91 + x121 >= 0.27950575;

e76:    x92 + x122 >= 0.27950575;

e77:  - x91 + x95 >= -0.29424122;

e78:  - x92 + x96 >= -0.29424122;

e79:  - x91 + x97 >= -0.29760193;

e80:  - x92 + x98 >= -0.29760193;

e81:  - x91 + x99 >= -0.35149534;

e82:  - x92 + x100 >= -0.35149534;

e83:  - x91 + x101 >= -0.30458283;

e84:  - x92 + x102 >= -0.30458283;

e85:  - x91 + x103 >= -0.29951066;

e86:  - x92 + x104 >= -0.29951066;

e87:  - x91 + x105 >= -0.30694357;

e88:  - x92 + x106 >= -0.30694357;

e89:  - x91 + x107 >= -0.33520661;

e90:  - x92 + x108 >= -0.33520661;

e91:  - x91 + x109 >= -0.3400071;

e92:  - x92 + x110 >= -0.3400071;

e93:  - x91 + x113 >= -0.34225726;

e94:  - x92 + x114 >= -0.34225726;

e95:  - x91 + x115 >= -0.32776566;

e96:  - x92 + x116 >= -0.32776566;

e97:  - x91 + x117 >= -0.30438256;

e98:  - x92 + x118 >= -0.30438256;

e99:  - x91 + x119 >= -0.28538336;

e100:  - x92 + x120 >= -0.28538336;

e101:  - x91 + x121 >= -0.27950575;

e102:  - x92 + x122 >= -0.27950575;

e103:  - x91 + x123 >= -0.25788969;

e104:  - x92 + x124 >= -0.25788969;

e105:    x93 + x127 >= -0.9536939;

e106:    x94 + x128 >= -0.9536939;

e107:    x93 + x129 >= -0.9004898;

e108:    x94 + x130 >= -0.9004898;

e109:    x93 + x131 >= -0.9114032;

e110:    x94 + x132 >= -0.9114032;

e111:    x93 + x133 >= -0.90071532;

e112:    x94 + x134 >= -0.90071532;

e113:    x93 + x135 >= -0.88043054;

e114:    x94 + x136 >= -0.88043054;

e115:    x93 + x137 >= -0.8680249;

e116:    x94 + x138 >= -0.8680249;

e117:    x93 + x139 >= -0.81034814;

e118:    x94 + x140 >= -0.81034814;

e119:    x93 + x141 >= -0.80843127;

e120:    x94 + x142 >= -0.80843127;

e121:    x93 + x143 >= -0.7794471;

e122:    x94 + x144 >= -0.7794471;

e123:    x93 + x145 >= -0.79930922;

e124:    x94 + x146 >= -0.79930922;

e125:    x93 + x147 >= -0.84280733;

e126:    x94 + x148 >= -0.84280733;

e127:    x93 + x149 >= -0.81379236;

e128:    x94 + x150 >= -0.81379236;

e129:    x93 + x151 >= -0.82457178;

e130:    x94 + x152 >= -0.82457178;

e131:    x93 + x153 >= -0.80226439;

e132:    x94 + x154 >= -0.80226439;

e133:  - x93 + x125 >= 0.98493628;

e134:  - x94 + x126 >= 0.98493628;

e135:  - x93 + x127 >= 0.9536939;

e136:  - x94 + x128 >= 0.9536939;

e137:  - x93 + x129 >= 0.9004898;

e138:  - x94 + x130 >= 0.9004898;

e139:  - x93 + x131 >= 0.9114032;

e140:  - x94 + x132 >= 0.9114032;

e141:  - x93 + x133 >= 0.90071532;

e142:  - x94 + x134 >= 0.90071532;

e143:  - x93 + x135 >= 0.88043054;

e144:  - x94 + x136 >= 0.88043054;

e145:  - x93 + x137 >= 0.8680249;

e146:  - x94 + x138 >= 0.8680249;

e147:  - x93 + x139 >= 0.81034814;

e148:  - x94 + x140 >= 0.81034814;

e149:  - x93 + x141 >= 0.80843127;

e150:  - x94 + x142 >= 0.80843127;

e151:  - x93 + x145 >= 0.79930922;

e152:  - x94 + x146 >= 0.79930922;

e153:  - x93 + x147 >= 0.84280733;

e154:  - x94 + x148 >= 0.84280733;

e155:  - x93 + x149 >= 0.81379236;

e156:  - x94 + x150 >= 0.81379236;

e157:  - x93 + x151 >= 0.82457178;

e158:  - x94 + x152 >= 0.82457178;

e159:  - x93 + x153 >= 0.80226439;

e160:  - x94 + x154 >= 0.80226439;

e161:    x1 - x95 - x125 = 0;

e162:    x2 - x96 - x126 = 0;

e163:    x3 - x97 - x127 = 0;

e164:    x4 - x98 - x128 = 0;

e165:    x5 - x99 - x129 = 0;

e166:    x6 - x100 - x130 = 0;

e167:    x7 - x101 - x131 = 0;

e168:    x8 - x102 - x132 = 0;

e169:    x9 - x103 - x133 = 0;

e170:    x10 - x104 - x134 = 0;

e171:    x11 - x105 - x135 = 0;

e172:    x12 - x106 - x136 = 0;

e173:    x13 - x107 - x137 = 0;

e174:    x14 - x108 - x138 = 0;

e175:    x15 - x109 - x139 = 0;

e176:    x16 - x110 - x140 = 0;

e177:    x17 - x111 - x141 = 0;

e178:    x18 - x112 - x142 = 0;

e179:    x19 - x113 - x143 = 0;

e180:    x20 - x114 - x144 = 0;

e181:    x21 - x115 - x145 = 0;

e182:    x22 - x116 - x146 = 0;

e183:    x23 - x117 - x147 = 0;

e184:    x24 - x118 - x148 = 0;

e185:    x25 - x119 - x149 = 0;

e186:    x26 - x120 - x150 = 0;

e187:    x27 - x121 - x151 = 0;

e188:    x28 - x122 - x152 = 0;

e189:    x29 - x123 - x153 = 0;

e190:    x30 - x124 - x154 = 0;

e191:    b203 + b204 >= 1;

e192:    b200 + b205 >= 1;

e193:    b199 + b206 >= 1;

e194:    b198 + b209 >= 1;

e195:    b197 + b204 >= 1;

e196:    b197 + b202 + b205 >= 1;

e197:    b197 + b200 + b207 >= 1;

e198:    b197 + b199 + b208 >= 1;

e199:    b197 + b198 >= 1;

e200:    b196 + b204 >= 1;

e201:    b196 + b203 + b205 >= 1;

e202:    b196 + b202 + b206 >= 1;

e203:    b196 + b201 + b207 >= 1;

e204:    b196 + b200 + b208 >= 1;

e205:    b196 + b199 + b209 >= 1;

e206:    b196 + b198 >= 1;

e207:    b195 + b206 >= 1;

e208:    b195 + b203 + b207 >= 1;

e209:    b195 + b202 + b208 >= 1;

e210:    b195 + b201 + b209 >= 1;

e211:    b195 + b200 >= 1;

e212:    b194 + b209 >= 1;

e213:    b194 + b203 >= 1;

e214:    b193 + b204 >= 1;

e215:    b193 + b203 + b205 >= 1;

e216:    b193 + b201 + b206 >= 1;

e217:    b193 + b200 + b207 >= 1;

e218:    b193 + b199 + b209 >= 1;

e219:    b193 + b198 >= 1;

e220:    b193 + b197 + b205 >= 1;

e221:    b193 + b197 + b203 + b206 >= 1;

e222:    b193 + b197 + b202 + b207 >= 1;

e223:    b193 + b197 + b201 + b208 >= 1;

e224:    b193 + b197 + b200 + b209 >= 1;

e225:    b193 + b197 + b199 >= 1;

e226:    b193 + b196 + b207 >= 1;

e227:    b193 + b196 + b203 + b208 >= 1;

e228:    b193 + b196 + b202 + b209 >= 1;

e229:    b193 + b196 + b201 >= 1;

e230:    b193 + b195 + b209 >= 1;

e231:    b193 + b195 + b203 >= 1;

e232:    b193 + b194 >= 1;

e233:    b192 + b206 >= 1;

e234:    b192 + b203 + b207 >= 1;

e235:    b192 + b202 + b208 >= 1;

e236:    b192 + b201 + b209 >= 1;

e237:    b192 + b200 >= 1;

e238:    b192 + b197 + b208 >= 1;

e239:    b192 + b197 + b203 + b209 >= 1;

e240:    b192 + b197 + b202 >= 1;

e241:    b192 + b196 + b209 >= 1;

e242:    b192 + b196 + b203 >= 1;

e243:    b192 + b195 >= 1;

e244:    b191 + b209 >= 1;

e245:    b191 + b203 >= 1;

e246:    b191 + b197 >= 1;

e247:    b190 + b204 >= 1;

e248:    b190 + b203 + b205 >= 1;

e249:    b190 + b202 + b206 >= 1;

e250:    b190 + b201 + b207 >= 1;

e251:    b190 + b200 + b208 >= 1;

e252:    b190 + b199 + b209 >= 1;

e253:    b190 + b198 >= 1;

e254:    b190 + b197 + b205 >= 1;

e255:    b190 + b197 + b203 + b206 >= 1;

e256:    b190 + b197 + b202 + b207 >= 1;

e257:    b190 + b197 + b201 + b208 >= 1;

e258:    b190 + b197 + b200 + b209 >= 1;

e259:    b190 + b197 + b199 >= 1;

e260:    b190 + b196 + b207 >= 1;

e261:    b190 + b196 + b203 + b208 >= 1;

e262:    b190 + b196 + b202 + b209 >= 1;

e263:    b190 + b196 + b201 >= 1;

e264:    b190 + b195 + b209 >= 1;

e265:    b190 + b195 + b203 >= 1;

e266:    b190 + b194 >= 1;

e267:    b190 + b193 + b206 >= 1;

e268:    b190 + b193 + b203 + b207 >= 1;

e269:    b190 + b193 + b202 + b208 >= 1;

e270:    b190 + b193 + b201 + b209 >= 1;

e271:    b190 + b193 + b200 >= 1;

e272:    b190 + b193 + b197 + b207 >= 1;

e273:    b190 + b193 + b197 + b203 + b209 >= 1;

e274:    b190 + b193 + b197 + b201 >= 1;

e275:    b190 + b193 + b196 + b209 >= 1;

e276:    b190 + b193 + b196 + b203 >= 1;

e277:    b190 + b193 + b195 >= 1;

e278:    b190 + b192 + b209 >= 1;

e279:    b190 + b192 + b203 >= 1;

e280:    b190 + b192 + b197 >= 1;

e281:    b190 + b191 >= 1;

e282:    b189 + b206 >= 1;

e283:    b189 + b203 + b207 >= 1;

e284:    b189 + b202 + b208 >= 1;

e285:    b189 + b201 + b209 >= 1;

e286:    b189 + b200 >= 1;

e287:    b189 + b197 + b208 >= 1;

e288:    b189 + b197 + b203 + b209 >= 1;

e289:    b189 + b197 + b201 >= 1;

e290:    b189 + b196 + b209 >= 1;

e291:    b189 + b196 + b203 >= 1;

e292:    b189 + b195 >= 1;

e293:    b189 + b193 + b209 >= 1;

e294:    b189 + b193 + b202 >= 1;

e295:    b189 + b193 + b197 >= 1;

e296:    b189 + b192 >= 1;

e297:    b188 + b209 >= 1;

e298:    b188 + b203 >= 1;

e299:    b188 + b197 >= 1;

e300:    b188 + b193 >= 1;

e301:    b187 + b204 >= 1;

e302:    b187 + b202 + b205 >= 1;

e303:    b187 + b201 + b206 >= 1;

e304:    b187 + b200 + b207 >= 1;

e305:    b187 + b199 + b209 >= 1;

e306:    b187 + b198 >= 1;

e307:    b187 + b197 + b205 >= 1;

e308:    b187 + b197 + b203 + b206 >= 1;

e309:    b187 + b197 + b202 + b207 >= 1;

e310:    b187 + b197 + b201 + b208 >= 1;

e311:    b187 + b197 + b200 + b209 >= 1;

e312:    b187 + b197 + b199 >= 1;

e313:    b187 + b196 + b207 >= 1;

e314:    b187 + b196 + b203 + b208 >= 1;

e315:    b187 + b196 + b202 + b209 >= 1;

e316:    b187 + b196 + b201 >= 1;

e317:    b187 + b195 + b209 >= 1;

e318:    b187 + b195 + b202 >= 1;

e319:    b187 + b194 >= 1;

e320:    b187 + b193 + b206 >= 1;

e321:    b187 + b193 + b203 + b207 >= 1;

e322:    b187 + b193 + b202 + b208 >= 1;

e323:    b187 + b193 + b201 + b209 >= 1;

e324:    b187 + b193 + b200 >= 1;

e325:    b187 + b193 + b197 + b207 >= 1;

e326:    b187 + b193 + b197 + b203 + b208 >= 1;

e327:    b187 + b193 + b197 + b202 + b209 >= 1;

e328:    b187 + b193 + b197 + b201 >= 1;

e329:    b187 + b193 + b196 + b209 >= 1;

e330:    b187 + b193 + b196 + b203 >= 1;

e331:    b187 + b193 + b195 >= 1;

e332:    b187 + b192 + b209 >= 1;

e333:    b187 + b192 + b203 >= 1;

e334:    b187 + b192 + b197 >= 1;

e335:    b187 + b191 >= 1;

e336:    b187 + b190 + b206 >= 1;

e337:    b187 + b190 + b203 + b207 >= 1;

e338:    b187 + b190 + b202 + b208 >= 1;

e339:    b187 + b190 + b201 + b209 >= 1;

e340:    b187 + b190 + b200 >= 1;

e341:    b187 + b190 + b197 + b207 >= 1;

e342:    b187 + b190 + b197 + b203 + b209 >= 1;

e343:    b187 + b190 + b197 + b202 >= 1;

e344:    b187 + b190 + b196 + b209 >= 1;

e345:    b187 + b190 + b196 + b203 >= 1;

e346:    b187 + b190 + b195 >= 1;

e347:    b187 + b190 + b193 + b208 >= 1;

e348:    b187 + b190 + b193 + b203 + b209 >= 1;

e349:    b187 + b190 + b193 + b202 >= 1;

e350:    b187 + b190 + b193 + b197 >= 1;

e351:    b187 + b190 + b192 >= 1;

e352:    b187 + b189 + b209 >= 1;

e353:    b187 + b189 + b203 >= 1;

e354:    b187 + b189 + b197 >= 1;

e355:    b187 + b189 + b193 >= 1;

e356:    b187 + b188 >= 1;

e357:    b186 + b206 >= 1;

e358:    b186 + b203 + b207 >= 1;

e359:    b186 + b202 + b208 >= 1;

e360:    b186 + b201 + b209 >= 1;

e361:    b186 + b200 >= 1;

e362:    b186 + b197 + b208 >= 1;

e363:    b186 + b197 + b203 + b209 >= 1;

e364:    b186 + b197 + b202 >= 1;

e365:    b186 + b196 + b209 >= 1;

e366:    b186 + b196 + b203 >= 1;

e367:    b186 + b195 >= 1;

e368:    b186 + b193 + b209 >= 1;

e369:    b186 + b193 + b203 >= 1;

e370:    b186 + b193 + b197 >= 1;

e371:    b186 + b192 >= 1;

e372:    b186 + b190 + b209 >= 1;

e373:    b186 + b190 + b203 >= 1;

e374:    b186 + b190 + b197 >= 1;

e375:    b186 + b190 + b193 >= 1;

e376:    b186 + b189 >= 1;

e377:    b185 + b209 >= 1;

e378:    b185 + b203 >= 1;

e379:    b185 + b197 >= 1;

e380:    b185 + b193 >= 1;

e381:    b185 + b190 >= 1;

e382:    b209 + b218 >= 1;

e383:    b209 + b216 + b219 >= 1;

e384:    b209 + b215 + b220 >= 1;

e385:    b209 + b214 + b221 >= 1;

e386:    b209 + b213 >= 1;

e387:    b209 + b212 + b219 >= 1;

e388:    b209 + b212 + b217 + b220 >= 1;

e389:    b209 + b212 + b215 + b222 >= 1;

e390:    b209 + b212 + b214 >= 1;

e391:    b209 + b211 + b221 >= 1;

e392:    b209 + b211 + b217 + b222 >= 1;

e393:    b209 + b211 + b216 >= 1;

e394:    b209 + b210 >= 1;

e395:    b208 + b218 >= 1;

e396:    b208 + b216 + b219 >= 1;

e397:    b208 + b215 + b220 >= 1;

e398:    b208 + b214 + b221 >= 1;

e399:    b208 + b213 >= 1;

e400:    b208 + b212 + b219 >= 1;

e401:    b208 + b212 + b217 + b220 >= 1;

e402:    b208 + b212 + b216 + b221 >= 1;

e403:    b208 + b212 + b215 + b222 >= 1;

e404:    b208 + b212 + b214 >= 1;

e405:    b208 + b211 + b221 >= 1;

e406:    b208 + b211 + b217 + b222 >= 1;

e407:    b208 + b211 + b216 >= 1;

e408:    b208 + b210 >= 1;

e409:    b207 + b218 >= 1;

e410:    b207 + b217 + b219 >= 1;

e411:    b207 + b216 + b220 >= 1;

e412:    b207 + b215 + b221 >= 1;

e413:    b207 + b214 + b222 >= 1;

e414:    b207 + b213 >= 1;

e415:    b207 + b212 + b220 >= 1;

e416:    b207 + b212 + b217 + b221 >= 1;

e417:    b207 + b212 + b216 + b222 >= 1;

e418:    b207 + b212 + b215 >= 1;

e419:    b207 + b211 + b222 >= 1;

e420:    b207 + b211 + b217 >= 1;

e421:    b207 + b210 >= 1;

e422:    b206 + b219 >= 1;

e423:    b206 + b217 + b220 >= 1;

e424:    b206 + b216 + b221 >= 1;

e425:    b206 + b215 + b222 >= 1;

e426:    b206 + b214 >= 1;

e427:    b206 + b212 + b221 >= 1;

e428:    b206 + b212 + b217 + b222 >= 1;

e429:    b206 + b212 + b216 >= 1;

e430:    b206 + b211 >= 1;

e431:    b205 + b220 >= 1;

e432:    b205 + b217 + b221 >= 1;

e433:    b205 + b216 + b222 >= 1;

e434:    b205 + b215 >= 1;

e435:    b205 + b212 + b222 >= 1;

e436:    b205 + b212 + b217 >= 1;

e437:    b205 + b211 >= 1;

e438:    b204 + b222 >= 1;

e439:    b204 + b217 >= 1;

e440:    b204 + b212 >= 1;

e441:    b203 + b218 >= 1;

e442:    b203 + b216 + b219 >= 1;

e443:    b203 + b215 + b220 >= 1;

e444:    b203 + b213 >= 1;

e445:    b203 + b212 + b219 >= 1;

e446:    b203 + b212 + b217 + b220 >= 1;

e447:    b203 + b212 + b215 + b222 >= 1;

e448:    b203 + b212 + b214 >= 1;

e449:    b203 + b211 + b221 >= 1;

e450:    b203 + b211 + b217 + b222 >= 1;

e451:    b203 + b211 + b216 >= 1;

e452:    b203 + b210 >= 1;

e453:    b203 + b209 + b218 >= 1;

e454:    b203 + b209 + b216 + b219 >= 1;

e455:    b203 + b209 + b215 + b220 >= 1;

e456:    b203 + b209 + b214 + b222 >= 1;

e457:    b203 + b209 + b213 >= 1;

e458:    b203 + b209 + b212 + b219 >= 1;

e459:    b203 + b209 + b212 + b217 + b220 >= 1;

e460:    b203 + b209 + b212 + b216 + b221 >= 1;

e461:    b203 + b209 + b212 + b215 + b222 >= 1;

e462:    b203 + b209 + b212 + b214 >= 1;

e463:    b203 + b209 + b211 + b221 >= 1;

e464:    b203 + b209 + b211 + b217 + b222 >= 1;

e465:    b203 + b209 + b211 + b216 >= 1;

e466:    b203 + b209 + b210 >= 1;

e467:    b203 + b208 + b218 >= 1;

e468:    b203 + b208 + b217 + b219 >= 1;

e469:    b203 + b208 + b216 + b220 >= 1;

e470:    b203 + b208 + b215 + b221 >= 1;

e471:    b203 + b208 + b214 + b222 >= 1;

e472:    b203 + b208 + b213 >= 1;

e473:    b203 + b208 + b212 + b220 >= 1;

e474:    b203 + b208 + b212 + b217 + b221 >= 1;

e475:    b203 + b208 + b212 + b216 + b222 >= 1;

e476:    b203 + b208 + b212 + b215 >= 1;

e477:    b203 + b208 + b211 + b222 >= 1;

e478:    b203 + b208 + b211 + b217 >= 1;

e479:    b203 + b208 + b210 >= 1;

e480:    b203 + b207 + b219 >= 1;

e481:    b203 + b207 + b217 + b220 >= 1;

e482:    b203 + b207 + b216 + b221 >= 1;

e483:    b203 + b207 + b215 + b222 >= 1;

e484:    b203 + b207 + b214 >= 1;

e485:    b203 + b207 + b212 + b221 >= 1;

e486:    b203 + b207 + b212 + b217 + b222 >= 1;

e487:    b203 + b207 + b212 + b216 >= 1;

e488:    b203 + b207 + b211 >= 1;

e489:    b203 + b206 + b220 >= 1;

e490:    b203 + b206 + b217 + b221 >= 1;

e491:    b203 + b206 + b216 + b222 >= 1;

e492:    b203 + b206 + b215 >= 1;

e493:    b203 + b206 + b212 + b222 >= 1;

e494:    b203 + b206 + b212 + b217 >= 1;

e495:    b203 + b206 + b211 >= 1;

e496:    b203 + b205 + b221 >= 1;

e497:    b203 + b205 + b217 + b222 >= 1;

e498:    b203 + b205 + b216 >= 1;

e499:    b203 + b205 + b212 >= 1;

e500:    b202 + b218 >= 1;

e501:    b202 + b216 + b219 >= 1;

e502:    b202 + b215 + b220 >= 1;

e503:    b202 + b214 + b221 >= 1;

e504:    b202 + b213 >= 1;

e505:    b202 + b212 + b219 >= 1;

e506:    b202 + b212 + b217 + b220 >= 1;

e507:    b202 + b212 + b216 + b221 >= 1;

e508:    b202 + b212 + b215 + b222 >= 1;

e509:    b202 + b212 + b214 >= 1;

e510:    b202 + b211 + b221 >= 1;

e511:    b202 + b211 + b217 + b222 >= 1;

e512:    b202 + b211 + b216 >= 1;

e513:    b202 + b210 >= 1;

e514:    b202 + b209 + b218 >= 1;

e515:    b202 + b209 + b217 + b219 >= 1;

e516:    b202 + b209 + b216 + b220 >= 1;

e517:    b202 + b209 + b215 + b221 >= 1;

e518:    b202 + b209 + b214 + b222 >= 1;

e519:    b202 + b209 + b213 >= 1;

e520:    b202 + b209 + b212 + b220 >= 1;

e521:    b202 + b209 + b212 + b217 + b221 >= 1;

e522:    b202 + b209 + b212 + b216 + b222 >= 1;

e523:    b202 + b209 + b212 + b215 >= 1;

e524:    b202 + b209 + b211 + b222 >= 1;

e525:    b202 + b209 + b211 + b217 >= 1;

e526:    b202 + b209 + b210 >= 1;

e527:    b202 + b208 + b219 >= 1;

e528:    b202 + b208 + b217 + b220 >= 1;

e529:    b202 + b208 + b216 + b221 >= 1;

e530:    b202 + b208 + b215 + b222 >= 1;

e531:    b202 + b208 + b214 >= 1;

e532:    b202 + b208 + b212 + b221 >= 1;

e533:    b202 + b208 + b212 + b217 + b222 >= 1;

e534:    b202 + b208 + b212 + b216 >= 1;

e535:    b202 + b208 + b211 >= 1;

e536:    b202 + b207 + b220 >= 1;

e537:    b202 + b207 + b217 + b221 >= 1;

e538:    b202 + b207 + b216 + b222 >= 1;

e539:    b202 + b207 + b215 >= 1;

e540:    b202 + b207 + b212 + b222 >= 1;

e541:    b202 + b207 + b212 + b217 >= 1;

e542:    b202 + b207 + b211 >= 1;

e543:    b202 + b206 + b220 >= 1;

e544:    b202 + b206 + b217 + b222 >= 1;

e545:    b202 + b206 + b216 >= 1;

e546:    b202 + b206 + b212 >= 1;

e547:    b202 + b205 + b221 >= 1;

e548:    b202 + b205 + b217 + b222 >= 1;

e549:    b202 + b205 + b216 >= 1;

e550:    b202 + b205 + b212 >= 1;

e551:    b201 + b218 >= 1;

e552:    b201 + b217 + b219 >= 1;

e553:    b201 + b216 + b220 >= 1;

e554:    b201 + b215 + b221 >= 1;

e555:    b201 + b214 + b222 >= 1;

e556:    b201 + b213 >= 1;

e557:    b201 + b212 + b220 >= 1;

e558:    b201 + b212 + b217 + b221 >= 1;

e559:    b201 + b212 + b216 + b222 >= 1;

e560:    b201 + b212 + b215 >= 1;

e561:    b201 + b211 + b222 >= 1;

e562:    b201 + b211 + b217 >= 1;

e563:    b201 + b210 >= 1;

e564:    b201 + b209 + b219 >= 1;

e565:    b201 + b209 + b217 + b220 >= 1;

e566:    b201 + b209 + b216 + b221 >= 1;

e567:    b201 + b209 + b215 + b222 >= 1;

e568:    b201 + b209 + b214 >= 1;

e569:    b201 + b209 + b212 + b221 >= 1;

e570:    b201 + b209 + b212 + b217 + b222 >= 1;

e571:    b201 + b209 + b212 + b216 >= 1;

e572:    b201 + b209 + b211 >= 1;

e573:    b201 + b208 + b220 >= 1;

e574:    b201 + b208 + b217 + b221 >= 1;

e575:    b201 + b208 + b216 + b222 >= 1;

e576:    b201 + b208 + b215 >= 1;

e577:    b201 + b208 + b212 + b222 >= 1;

e578:    b201 + b208 + b212 + b217 >= 1;

e579:    b201 + b208 + b211 >= 1;

e580:    b201 + b207 + b220 >= 1;

e581:    b201 + b207 + b217 + b221 >= 1;

e582:    b201 + b207 + b216 + b222 >= 1;

e583:    b201 + b207 + b215 >= 1;

e584:    b201 + b207 + b212 + b222 >= 1;

e585:    b201 + b207 + b212 + b217 >= 1;

e586:    b201 + b207 + b211 >= 1;

e587:    b201 + b206 + b221 >= 1;

e588:    b201 + b206 + b217 + b222 >= 1;

e589:    b201 + b206 + b216 >= 1;

e590:    b201 + b206 + b212 >= 1;

e591:    b201 + b205 + b222 >= 1;

e592:    b201 + b205 + b217 >= 1;

e593:    b201 + b205 + b212 >= 1;

e594:    b200 + b219 >= 1;

e595:    b200 + b217 + b220 >= 1;

e596:    b200 + b216 + b221 >= 1;

e597:    b200 + b215 + b222 >= 1;

e598:    b200 + b214 >= 1;

e599:    b200 + b212 + b221 >= 1;

e600:    b200 + b212 + b217 + b222 >= 1;

e601:    b200 + b212 + b216 >= 1;

e602:    b200 + b211 >= 1;

e603:    b200 + b209 + b220 >= 1;

e604:    b200 + b209 + b217 + b221 >= 1;

e605:    b200 + b209 + b216 + b222 >= 1;

e606:    b200 + b209 + b215 >= 1;

e607:    b200 + b209 + b212 + b222 >= 1;

e608:    b200 + b209 + b212 + b217 >= 1;

e609:    b200 + b209 + b211 >= 1;

e610:    b200 + b208 + b220 >= 1;

e611:    b200 + b208 + b217 + b221 >= 1;

e612:    b200 + b208 + b216 >= 1;

e613:    b200 + b208 + b212 + b222 >= 1;

e614:    b200 + b208 + b212 + b217 >= 1;

e615:    b200 + b208 + b211 >= 1;

e616:    b200 + b207 + b221 >= 1;

e617:    b200 + b207 + b217 + b222 >= 1;

e618:    b200 + b207 + b216 >= 1;

e619:    b200 + b207 + b212 >= 1;

e620:    b200 + b206 + b222 >= 1;

e621:    b200 + b206 + b217 >= 1;

e622:    b200 + b206 + b212 >= 1;

e623:    b199 + b220 >= 1;

e624:    b199 + b217 + b221 >= 1;

e625:    b199 + b216 + b222 >= 1;

e626:    b199 + b215 >= 1;

e627:    b199 + b212 + b222 >= 1;

e628:    b199 + b212 + b217 >= 1;

e629:    b199 + b211 >= 1;

e630:    b199 + b209 + b220 >= 1;

e631:    b199 + b209 + b217 + b222 >= 1;

e632:    b199 + b209 + b216 >= 1;

e633:    b199 + b209 + b212 >= 1;

e634:    b199 + b208 + b221 >= 1;

e635:    b199 + b208 + b217 + b222 >= 1;

e636:    b199 + b208 + b216 >= 1;

e637:    b199 + b208 + b212 >= 1;

e638:    b199 + b207 + b222 >= 1;

e639:    b199 + b207 + b217 >= 1;

e640:    b199 + b207 + b212 >= 1;

e641:    b198 + b222 >= 1;

e642:    b198 + b217 >= 1;

e643:    b198 + b212 >= 1;

e644:    b197 + b218 >= 1;

e645:    b197 + b216 + b219 >= 1;

e646:    b197 + b215 + b220 >= 1;

e647:    b197 + b214 + b221 >= 1;

e648:    b197 + b213 >= 1;

e649:    b197 + b212 + b219 >= 1;

e650:    b197 + b212 + b217 + b220 >= 1;

e651:    b197 + b212 + b216 + b221 >= 1;

e652:    b197 + b212 + b215 + b222 >= 1;

e653:    b197 + b212 + b214 >= 1;

e654:    b197 + b211 + b221 >= 1;

e655:    b197 + b211 + b217 + b222 >= 1;

e656:    b197 + b211 + b216 >= 1;

e657:    b197 + b210 >= 1;

e658:    b197 + b209 + b218 >= 1;

e659:    b197 + b209 + b217 + b219 >= 1;

e660:    b197 + b209 + b216 + b220 >= 1;

e661:    b197 + b209 + b215 + b221 >= 1;

e662:    b197 + b209 + b214 + b222 >= 1;

e663:    b197 + b209 + b213 >= 1;

e664:    b197 + b209 + b212 + b220 >= 1;

e665:    b197 + b209 + b212 + b217 + b221 >= 1;

e666:    b197 + b209 + b212 + b216 + b222 >= 1;

e667:    b197 + b209 + b212 + b215 >= 1;

e668:    b197 + b209 + b211 + b222 >= 1;

e669:    b197 + b209 + b211 + b217 >= 1;

e670:    b197 + b209 + b210 >= 1;

e671:    b197 + b208 + b219 >= 1;

e672:    b197 + b208 + b216 + b220 >= 1;

e673:    b197 + b208 + b215 + b222 >= 1;

e674:    b197 + b208 + b214 >= 1;

e675:    b197 + b208 + b212 + b220 >= 1;

e676:    b197 + b208 + b212 + b217 + b221 >= 1;

e677:    b197 + b208 + b212 + b216 + b222 >= 1;

e678:    b197 + b208 + b212 + b215 >= 1;

e679:    b197 + b208 + b211 + b222 >= 1;

e680:    b197 + b208 + b211 + b217 >= 1;

e681:    b197 + b208 + b210 >= 1;

e682:    b197 + b207 + b219 >= 1;

e683:    b197 + b207 + b217 + b220 >= 1;

e684:    b197 + b207 + b216 + b221 >= 1;

e685:    b197 + b207 + b215 + b222 >= 1;

e686:    b197 + b207 + b214 >= 1;

e687:    b197 + b207 + b212 + b221 >= 1;

e688:    b197 + b207 + b212 + b217 + b222 >= 1;

e689:    b197 + b207 + b212 + b216 >= 1;

e690:    b197 + b207 + b211 >= 1;

e691:    b197 + b206 + b220 >= 1;

e692:    b197 + b206 + b217 + b221 >= 1;

e693:    b197 + b206 + b216 + b222 >= 1;

e694:    b197 + b206 + b215 >= 1;

e695:    b197 + b206 + b212 + b222 >= 1;

e696:    b197 + b206 + b212 + b217 >= 1;

e697:    b197 + b206 + b211 >= 1;

e698:    b197 + b205 + b221 >= 1;

e699:    b197 + b205 + b217 + b222 >= 1;

e700:    b197 + b205 + b216 >= 1;

e701:    b197 + b205 + b212 >= 1;

e702:    b197 + b203 + b218 >= 1;

e703:    b197 + b203 + b217 + b219 >= 1;

e704:    b197 + b203 + b216 + b220 >= 1;

e705:    b197 + b203 + b215 + b221 >= 1;

e706:    b197 + b203 + b214 + b222 >= 1;

e707:    b197 + b203 + b213 >= 1;

e708:    b197 + b203 + b212 + b220 >= 1;

e709:    b197 + b203 + b212 + b217 + b221 >= 1;

e710:    b197 + b203 + b212 + b216 + b222 >= 1;

e711:    b197 + b203 + b212 + b215 >= 1;

e712:    b197 + b203 + b211 + b222 >= 1;

e713:    b197 + b203 + b211 + b217 >= 1;

e714:    b197 + b203 + b210 >= 1;

e715:    b197 + b203 + b209 + b219 >= 1;

e716:    b197 + b203 + b209 + b217 + b220 >= 1;

e717:    b197 + b203 + b209 + b216 + b221 >= 1;

e718:    b197 + b203 + b209 + b215 + b222 >= 1;

e719:    b197 + b203 + b209 + b214 >= 1;

e720:    b197 + b203 + b209 + b212 + b221 >= 1;

e721:    b197 + b203 + b209 + b212 + b217 + b222 >= 1;

e722:    b197 + b203 + b209 + b212 + b216 >= 1;

e723:    b197 + b203 + b209 + b211 >= 1;

e724:    b197 + b203 + b208 + b219 >= 1;

e725:    b197 + b203 + b208 + b217 + b220 >= 1;

e726:    b197 + b203 + b208 + b216 + b221 >= 1;

e727:    b197 + b203 + b208 + b215 + b222 >= 1;

e728:    b197 + b203 + b208 + b214 >= 1;

e729:    b197 + b203 + b208 + b212 + b221 >= 1;

e730:    b197 + b203 + b208 + b212 + b217 + b222 >= 1;

e731:    b197 + b203 + b208 + b212 + b216 >= 1;

e732:    b197 + b203 + b208 + b211 >= 1;

e733:    b197 + b203 + b207 + b220 >= 1;

e734:    b197 + b203 + b207 + b217 + b221 >= 1;

e735:    b197 + b203 + b207 + b216 + b222 >= 1;

e736:    b197 + b203 + b207 + b215 >= 1;

e737:    b197 + b203 + b207 + b212 + b222 >= 1;

e738:    b197 + b203 + b207 + b212 + b217 >= 1;

e739:    b197 + b203 + b207 + b211 >= 1;

e740:    b197 + b203 + b206 + b221 >= 1;

e741:    b197 + b203 + b206 + b217 + b222 >= 1;

e742:    b197 + b203 + b206 + b216 >= 1;

e743:    b197 + b203 + b206 + b212 >= 1;

e744:    b197 + b203 + b205 + b222 >= 1;

e745:    b197 + b203 + b205 + b217 >= 1;

e746:    b197 + b203 + b205 + b212 >= 1;

e747:    b197 + b202 + b218 >= 1;

e748:    b197 + b202 + b217 + b219 >= 1;

e749:    b197 + b202 + b216 + b220 >= 1;

e750:    b197 + b202 + b215 + b222 >= 1;

e751:    b197 + b202 + b214 >= 1;

e752:    b197 + b202 + b212 + b220 >= 1;

e753:    b197 + b202 + b212 + b217 + b221 >= 1;

e754:    b197 + b202 + b212 + b216 + b222 >= 1;

e755:    b197 + b202 + b212 + b215 >= 1;

e756:    b197 + b202 + b211 >= 1;

e757:    b197 + b202 + b209 + b219 >= 1;

e758:    b197 + b202 + b209 + b217 + b220 >= 1;

e759:    b197 + b202 + b209 + b216 + b221 >= 1;

e760:    b197 + b202 + b209 + b215 + b222 >= 1;

e761:    b197 + b202 + b209 + b214 >= 1;

e762:    b197 + b202 + b209 + b212 + b221 >= 1;

e763:    b197 + b202 + b209 + b212 + b217 + b222 >= 1;

e764:    b197 + b202 + b209 + b212 + b216 >= 1;

e765:    b197 + b202 + b209 + b211 >= 1;

e766:    b197 + b202 + b208 + b220 >= 1;

e767:    b197 + b202 + b208 + b217 + b221 >= 1;

e768:    b197 + b202 + b208 + b216 + b222 >= 1;

e769:    b197 + b202 + b208 + b215 >= 1;

e770:    b197 + b202 + b208 + b212 + b222 >= 1;

e771:    b197 + b202 + b208 + b212 + b217 >= 1;

e772:    b197 + b202 + b208 + b211 >= 1;

e773:    b197 + b202 + b207 + b221 >= 1;

e774:    b197 + b202 + b207 + b217 + b222 >= 1;

e775:    b197 + b202 + b207 + b216 >= 1;

e776:    b197 + b202 + b207 + b212 >= 1;

e777:    b197 + b202 + b206 + b222 >= 1;

e778:    b197 + b202 + b206 + b217 >= 1;

e779:    b197 + b202 + b206 + b212 >= 1;

e780:    b197 + b201 + b219 >= 1;

e781:    b197 + b201 + b217 + b220 >= 1;

e782:    b197 + b201 + b216 + b221 >= 1;

e783:    b197 + b201 + b215 + b222 >= 1;

e784:    b197 + b201 + b214 >= 1;

e785:    b197 + b201 + b212 + b221 >= 1;

e786:    b197 + b201 + b212 + b217 + b222 >= 1;

e787:    b197 + b201 + b212 + b216 >= 1;

e788:    b197 + b201 + b211 >= 1;

e789:    b197 + b201 + b209 + b220 >= 1;

e790:    b197 + b201 + b209 + b217 + b221 >= 1;

e791:    b197 + b201 + b209 + b216 + b222 >= 1;

e792:    b197 + b201 + b209 + b215 >= 1;

e793:    b197 + b201 + b209 + b212 + b222 >= 1;

e794:    b197 + b201 + b209 + b212 + b217 >= 1;

e795:    b197 + b201 + b209 + b211 >= 1;

e796:    b197 + b201 + b208 + b221 >= 1;

e797:    b197 + b201 + b208 + b217 + b222 >= 1;

e798:    b197 + b201 + b208 + b216 >= 1;

e799:    b197 + b201 + b208 + b212 >= 1;

e800:    b197 + b201 + b207 + b222 >= 1;

e801:    b197 + b201 + b207 + b217 >= 1;

e802:    b197 + b201 + b207 + b212 >= 1;

e803:    b197 + b201 + b206 + b222 >= 1;

e804:    b197 + b201 + b206 + b217 >= 1;

e805:    b197 + b201 + b206 + b212 >= 1;

e806:    b197 + b200 + b220 >= 1;

e807:    b197 + b200 + b217 + b221 >= 1;

e808:    b197 + b200 + b216 + b222 >= 1;

e809:    b197 + b200 + b215 >= 1;

e810:    b197 + b200 + b212 + b222 >= 1;

e811:    b197 + b200 + b212 + b217 >= 1;

e812:    b197 + b200 + b211 >= 1;

e813:    b197 + b200 + b209 + b221 >= 1;

e814:    b197 + b200 + b209 + b217 + b222 >= 1;

e815:    b197 + b200 + b209 + b216 >= 1;

e816:    b197 + b200 + b209 + b212 >= 1;

e817:    b197 + b200 + b208 + b222 >= 1;

e818:    b197 + b200 + b208 + b217 >= 1;

e819:    b197 + b200 + b208 + b212 >= 1;

e820:    b197 + b199 + b221 >= 1;

e821:    b197 + b199 + b217 + b222 >= 1;

e822:    b197 + b199 + b216 >= 1;

e823:    b197 + b199 + b212 >= 1;

e824:    b197 + b199 + b209 + b222 >= 1;

e825:    b197 + b199 + b209 + b217 >= 1;

e826:    b197 + b199 + b209 + b212 >= 1;

e827:    b196 + b218 >= 1;

e828:    b196 + b217 + b219 >= 1;

e829:    b196 + b216 + b220 >= 1;

e830:    b196 + b215 + b221 >= 1;

e831:    b196 + b214 + b222 >= 1;

e832:    b196 + b213 >= 1;

e833:    b196 + b212 + b220 >= 1;

e834:    b196 + b212 + b217 + b221 >= 1;

e835:    b196 + b212 + b216 + b222 >= 1;

e836:    b196 + b212 + b215 >= 1;

e837:    b196 + b211 + b222 >= 1;

e838:    b196 + b211 + b217 >= 1;

e839:    b196 + b210 >= 1;

e840:    b196 + b209 + b219 >= 1;

e841:    b196 + b209 + b217 + b220 >= 1;

e842:    b196 + b209 + b216 + b221 >= 1;

e843:    b196 + b209 + b215 + b222 >= 1;

e844:    b196 + b209 + b214 >= 1;

e845:    b196 + b209 + b212 + b221 >= 1;

e846:    b196 + b209 + b212 + b217 + b222 >= 1;

e847:    b196 + b209 + b212 + b216 >= 1;

e848:    b196 + b209 + b211 >= 1;

e849:    b196 + b208 + b220 >= 1;

e850:    b196 + b208 + b217 + b221 >= 1;

e851:    b196 + b208 + b216 + b222 >= 1;

e852:    b196 + b208 + b215 >= 1;

e853:    b196 + b208 + b212 + b222 >= 1;

e854:    b196 + b208 + b212 + b217 >= 1;

e855:    b196 + b208 + b211 >= 1;

e856:    b196 + b207 + b221 >= 1;

e857:    b196 + b207 + b217 + b222 >= 1;

e858:    b196 + b207 + b216 >= 1;

e859:    b196 + b207 + b212 >= 1;

e860:    b196 + b206 + b222 >= 1;

e861:    b196 + b206 + b217 >= 1;

e862:    b196 + b206 + b212 >= 1;

e863:    b196 + b205 + b222 >= 1;

e864:    b196 + b205 + b217 >= 1;

e865:    b196 + b205 + b212 >= 1;

e866:    b196 + b203 + b219 >= 1;

e867:    b196 + b203 + b217 + b220 >= 1;

e868:    b196 + b203 + b216 + b221 >= 1;

e869:    b196 + b203 + b215 + b222 >= 1;

e870:    b196 + b203 + b214 >= 1;

e871:    b196 + b203 + b212 + b221 >= 1;

e872:    b196 + b203 + b212 + b217 + b222 >= 1;

e873:    b196 + b203 + b212 + b216 >= 1;

e874:    b196 + b203 + b211 >= 1;

e875:    b196 + b203 + b209 + b220 >= 1;

e876:    b196 + b203 + b209 + b217 + b221 >= 1;

e877:    b196 + b203 + b209 + b216 + b222 >= 1;

e878:    b196 + b203 + b209 + b215 >= 1;

e879:    b196 + b203 + b209 + b212 + b222 >= 1;

e880:    b196 + b203 + b209 + b212 + b217 >= 1;

e881:    b196 + b203 + b209 + b211 >= 1;

e882:    b196 + b203 + b208 + b221 >= 1;

e883:    b196 + b203 + b208 + b217 + b222 >= 1;

e884:    b196 + b203 + b208 + b216 >= 1;

e885:    b196 + b203 + b208 + b212 >= 1;

e886:    b196 + b203 + b207 + b222 >= 1;

e887:    b196 + b203 + b207 + b217 >= 1;

e888:    b196 + b203 + b207 + b212 >= 1;

e889:    b196 + b203 + b206 + b222 >= 1;

e890:    b196 + b203 + b206 + b217 >= 1;

e891:    b196 + b203 + b206 + b212 >= 1;

e892:    b196 + b202 + b220 >= 1;

e893:    b196 + b202 + b217 + b221 >= 1;

e894:    b196 + b202 + b216 + b222 >= 1;

e895:    b196 + b202 + b215 >= 1;

e896:    b196 + b202 + b212 + b222 >= 1;

e897:    b196 + b202 + b212 + b217 >= 1;

e898:    b196 + b202 + b211 >= 1;

e899:    b196 + b202 + b209 + b221 >= 1;

e900:    b196 + b202 + b209 + b217 + b222 >= 1;

e901:    b196 + b202 + b209 + b216 >= 1;

e902:    b196 + b202 + b209 + b212 >= 1;

e903:    b196 + b202 + b208 + b222 >= 1;

e904:    b196 + b202 + b208 + b216 >= 1;

e905:    b196 + b202 + b208 + b212 >= 1;

e906:    b196 + b202 + b207 + b222 >= 1;

e907:    b196 + b202 + b207 + b217 >= 1;

e908:    b196 + b202 + b207 + b212 >= 1;

e909:    b196 + b201 + b221 >= 1;

e910:    b196 + b201 + b217 + b222 >= 1;

e911:    b196 + b201 + b216 >= 1;

e912:    b196 + b201 + b212 >= 1;

e913:    b196 + b201 + b209 + b222 >= 1;

e914:    b196 + b201 + b209 + b216 >= 1;

e915:    b196 + b201 + b209 + b212 >= 1;

e916:    b196 + b201 + b208 + b222 >= 1;

e917:    b196 + b201 + b208 + b217 >= 1;

e918:    b196 + b201 + b208 + b212 >= 1;

e919:    b196 + b200 + b221 >= 1;

e920:    b196 + b200 + b217 + b222 >= 1;

e921:    b196 + b200 + b216 >= 1;

e922:    b196 + b200 + b212 >= 1;

e923:    b196 + b200 + b209 + b222 >= 1;

e924:    b196 + b200 + b209 + b217 >= 1;

e925:    b196 + b200 + b209 + b212 >= 1;

e926:    b196 + b199 + b222 >= 1;

e927:    b196 + b199 + b217 >= 1;

e928:    b196 + b199 + b212 >= 1;

e929:    b195 + b220 >= 1;

e930:    b195 + b217 + b221 >= 1;

e931:    b195 + b216 + b222 >= 1;

e932:    b195 + b215 >= 1;

e933:    b195 + b212 + b222 >= 1;

e934:    b195 + b212 + b217 >= 1;

e935:    b195 + b211 >= 1;

e936:    b195 + b209 + b221 >= 1;

e937:    b195 + b209 + b217 + b222 >= 1;

e938:    b195 + b209 + b216 >= 1;

e939:    b195 + b209 + b212 >= 1;

e940:    b195 + b208 + b221 >= 1;

e941:    b195 + b208 + b217 + b222 >= 1;

e942:    b195 + b208 + b216 >= 1;

e943:    b195 + b208 + b212 >= 1;

e944:    b195 + b207 + b222 >= 1;

e945:    b195 + b207 + b217 >= 1;

e946:    b195 + b207 + b212 >= 1;

e947:    b195 + b203 + b221 >= 1;

e948:    b195 + b203 + b217 + b222 >= 1;

e949:    b195 + b203 + b216 >= 1;

e950:    b195 + b203 + b212 >= 1;

e951:    b195 + b203 + b209 + b222 >= 1;

e952:    b195 + b203 + b209 + b216 >= 1;

e953:    b195 + b203 + b209 + b212 >= 1;

e954:    b195 + b203 + b208 + b222 >= 1;

e955:    b195 + b203 + b208 + b217 >= 1;

e956:    b195 + b203 + b208 + b212 >= 1;

e957:    b195 + b202 + b221 >= 1;

e958:    b195 + b202 + b217 + b222 >= 1;

e959:    b195 + b202 + b216 >= 1;

e960:    b195 + b202 + b212 >= 1;

e961:    b195 + b202 + b209 + b222 >= 1;

e962:    b195 + b202 + b209 + b217 >= 1;

e963:    b195 + b202 + b209 + b212 >= 1;

e964:    b195 + b201 + b222 >= 1;

e965:    b195 + b201 + b217 >= 1;

e966:    b195 + b201 + b212 >= 1;

e967:    b194 + b222 >= 1;

e968:    b194 + b217 >= 1;

e969:    b194 + b212 >= 1;

e970:    b193 + b218 >= 1;

e971:    b193 + b217 + b219 >= 1;

e972:    b193 + b216 + b220 >= 1;

e973:    b193 + b215 + b221 >= 1;

e974:    b193 + b214 + b222 >= 1;

e975:    b193 + b213 >= 1;

e976:    b193 + b212 + b220 >= 1;

e977:    b193 + b212 + b217 + b221 >= 1;

e978:    b193 + b212 + b216 + b222 >= 1;

e979:    b193 + b212 + b215 >= 1;

e980:    b193 + b211 + b222 >= 1;

e981:    b193 + b211 + b217 >= 1;

e982:    b193 + b210 >= 1;

e983:    b193 + b209 + b219 >= 1;

e984:    b193 + b209 + b217 + b220 >= 1;

e985:    b193 + b209 + b215 + b222 >= 1;

e986:    b193 + b209 + b214 >= 1;

e987:    b193 + b209 + b212 + b220 >= 1;

e988:    b193 + b209 + b212 + b217 + b221 >= 1;

e989:    b193 + b209 + b212 + b216 + b222 >= 1;

e990:    b193 + b209 + b212 + b215 >= 1;

e991:    b193 + b209 + b211 >= 1;

e992:    b193 + b208 + b219 >= 1;

e993:    b193 + b208 + b217 + b220 >= 1;

e994:    b193 + b208 + b216 + b221 >= 1;

e995:    b193 + b208 + b215 + b222 >= 1;

e996:    b193 + b208 + b214 >= 1;

e997:    b193 + b208 + b212 + b221 >= 1;

e998:    b193 + b208 + b212 + b217 + b222 >= 1;

e999:    b193 + b208 + b212 + b216 >= 1;

e1000:    b193 + b208 + b211 >= 1;

e1001:    b193 + b207 + b220 >= 1;

e1002:    b193 + b207 + b217 + b221 >= 1;

e1003:    b193 + b207 + b216 + b222 >= 1;

e1004:    b193 + b207 + b215 >= 1;

e1005:    b193 + b207 + b212 + b222 >= 1;

e1006:    b193 + b207 + b212 + b217 >= 1;

e1007:    b193 + b207 + b211 >= 1;

e1008:    b193 + b206 + b221 >= 1;

e1009:    b193 + b206 + b217 + b222 >= 1;

e1010:    b193 + b206 + b216 >= 1;

e1011:    b193 + b206 + b212 >= 1;

e1012:    b193 + b205 + b222 >= 1;

e1013:    b193 + b205 + b217 >= 1;

e1014:    b193 + b205 + b212 >= 1;

e1015:    b193 + b203 + b219 >= 1;

e1016:    b193 + b203 + b216 + b220 >= 1;

e1017:    b193 + b203 + b215 + b221 >= 1;

e1018:    b193 + b203 + b214 + b222 >= 1;

e1019:    b193 + b203 + b213 >= 1;

e1020:    b193 + b203 + b212 + b220 >= 1;

e1021:    b193 + b203 + b212 + b217 + b221 >= 1;

e1022:    b193 + b203 + b212 + b216 >= 1;

e1023:    b193 + b203 + b211 >= 1;

e1024:    b193 + b203 + b209 + b219 >= 1;

e1025:    b193 + b203 + b209 + b217 + b220 >= 1;

e1026:    b193 + b203 + b209 + b216 + b221 >= 1;

e1027:    b193 + b203 + b209 + b215 + b222 >= 1;

e1028:    b193 + b203 + b209 + b214 >= 1;

e1029:    b193 + b203 + b209 + b212 + b221 >= 1;

e1030:    b193 + b203 + b209 + b212 + b217 + b222 >= 1;

e1031:    b193 + b203 + b209 + b212 + b216 >= 1;

e1032:    b193 + b203 + b209 + b211 >= 1;

e1033:    b193 + b203 + b208 + b220 >= 1;

e1034:    b193 + b203 + b208 + b217 + b221 >= 1;

e1035:    b193 + b203 + b208 + b216 + b222 >= 1;

e1036:    b193 + b203 + b208 + b215 >= 1;

e1037:    b193 + b203 + b208 + b212 + b222 >= 1;

e1038:    b193 + b203 + b208 + b212 + b217 >= 1;

e1039:    b193 + b203 + b208 + b211 >= 1;

e1040:    b193 + b203 + b207 + b221 >= 1;

e1041:    b193 + b203 + b207 + b217 + b222 >= 1;

e1042:    b193 + b203 + b207 + b216 >= 1;

e1043:    b193 + b203 + b207 + b212 >= 1;

e1044:    b193 + b203 + b206 + b222 >= 1;

e1045:    b193 + b203 + b206 + b217 >= 1;

e1046:    b193 + b203 + b206 + b212 >= 1;

e1047:    b193 + b202 + b219 >= 1;

e1048:    b193 + b202 + b217 + b220 >= 1;

e1049:    b193 + b202 + b216 + b221 >= 1;

e1050:    b193 + b202 + b215 + b222 >= 1;

e1051:    b193 + b202 + b214 >= 1;

e1052:    b193 + b202 + b212 + b221 >= 1;

e1053:    b193 + b202 + b212 + b217 + b222 >= 1;

e1054:    b193 + b202 + b212 + b216 >= 1;

e1055:    b193 + b202 + b211 >= 1;

e1056:    b193 + b202 + b209 + b220 >= 1;

e1057:    b193 + b202 + b209 + b217 + b221 >= 1;

e1058:    b193 + b202 + b209 + b216 + b222 >= 1;

e1059:    b193 + b202 + b209 + b215 >= 1;

e1060:    b193 + b202 + b209 + b212 + b222 >= 1;

e1061:    b193 + b202 + b209 + b212 + b217 >= 1;

e1062:    b193 + b202 + b209 + b211 >= 1;

e1063:    b193 + b202 + b208 + b221 >= 1;

e1064:    b193 + b202 + b208 + b217 + b222 >= 1;

e1065:    b193 + b202 + b208 + b216 >= 1;

e1066:    b193 + b202 + b208 + b212 >= 1;

e1067:    b193 + b202 + b207 + b222 >= 1;

e1068:    b193 + b202 + b207 + b217 >= 1;

e1069:    b193 + b202 + b207 + b212 >= 1;

e1070:    b193 + b202 + b206 + b222 >= 1;

e1071:    b193 + b202 + b206 + b217 >= 1;

e1072:    b193 + b202 + b206 + b212 >= 1;

e1073:    b193 + b201 + b220 >= 1;

e1074:    b193 + b201 + b217 + b221 >= 1;

e1075:    b193 + b201 + b216 + b222 >= 1;

e1076:    b193 + b201 + b215 >= 1;

e1077:    b193 + b201 + b212 + b222 >= 1;

e1078:    b193 + b201 + b212 + b217 >= 1;

e1079:    b193 + b201 + b211 >= 1;

e1080:    b193 + b201 + b209 + b221 >= 1;

e1081:    b193 + b201 + b209 + b217 + b222 >= 1;

e1082:    b193 + b201 + b209 + b216 >= 1;

e1083:    b193 + b201 + b209 + b212 >= 1;

e1084:    b193 + b201 + b208 + b222 >= 1;

e1085:    b193 + b201 + b208 + b217 >= 1;

e1086:    b193 + b201 + b208 + b212 >= 1;

e1087:    b193 + b201 + b207 + b222 >= 1;

e1088:    b193 + b201 + b207 + b217 >= 1;

e1089:    b193 + b201 + b207 + b212 >= 1;

e1090:    b193 + b200 + b221 >= 1;

e1091:    b193 + b200 + b217 + b222 >= 1;

e1092:    b193 + b200 + b216 >= 1;

e1093:    b193 + b200 + b212 >= 1;

e1094:    b193 + b200 + b209 + b222 >= 1;

e1095:    b193 + b200 + b209 + b217 >= 1;

e1096:    b193 + b200 + b209 + b212 >= 1;

e1097:    b193 + b200 + b208 + b222 >= 1;

e1098:    b193 + b200 + b208 + b217 >= 1;

e1099:    b193 + b200 + b208 + b212 >= 1;

e1100:    b193 + b199 + b222 >= 1;

e1101:    b193 + b199 + b217 >= 1;

e1102:    b193 + b199 + b212 >= 1;

e1103:    b193 + b197 + b219 >= 1;

e1104:    b193 + b197 + b217 + b220 >= 1;

e1105:    b193 + b197 + b216 + b221 >= 1;

e1106:    b193 + b197 + b215 + b222 >= 1;

e1107:    b193 + b197 + b214 >= 1;

e1108:    b193 + b197 + b212 + b221 >= 1;

e1109:    b193 + b197 + b212 + b217 + b222 >= 1;

e1110:    b193 + b197 + b212 + b216 >= 1;

e1111:    b193 + b197 + b211 >= 1;

e1112:    b193 + b197 + b209 + b220 >= 1;

e1113:    b193 + b197 + b209 + b217 + b221 >= 1;

e1114:    b193 + b197 + b209 + b216 + b222 >= 1;

e1115:    b193 + b197 + b209 + b215 >= 1;

e1116:    b193 + b197 + b209 + b212 + b222 >= 1;

e1117:    b193 + b197 + b209 + b212 + b217 >= 1;

e1118:    b193 + b197 + b209 + b211 >= 1;

e1119:    b193 + b197 + b208 + b220 >= 1;

e1120:    b193 + b197 + b208 + b217 + b221 >= 1;

e1121:    b193 + b197 + b208 + b216 + b222 >= 1;

e1122:    b193 + b197 + b208 + b215 >= 1;

e1123:    b193 + b197 + b208 + b212 + b222 >= 1;

e1124:    b193 + b197 + b208 + b212 + b217 >= 1;

e1125:    b193 + b197 + b208 + b211 >= 1;

e1126:    b193 + b197 + b207 + b221 >= 1;

e1127:    b193 + b197 + b207 + b217 + b222 >= 1;

e1128:    b193 + b197 + b207 + b216 >= 1;

e1129:    b193 + b197 + b207 + b212 >= 1;

e1130:    b193 + b197 + b206 + b222 >= 1;

e1131:    b193 + b197 + b206 + b217 >= 1;

e1132:    b193 + b197 + b206 + b212 >= 1;

e1133:    b193 + b197 + b203 + b220 >= 1;

e1134:    b193 + b197 + b203 + b217 + b221 >= 1;

e1135:    b193 + b197 + b203 + b216 + b222 >= 1;

e1136:    b193 + b197 + b203 + b215 >= 1;

e1137:    b193 + b197 + b203 + b212 + b222 >= 1;

e1138:    b193 + b197 + b203 + b212 + b217 >= 1;

e1139:    b193 + b197 + b203 + b211 >= 1;

e1140:    b193 + b197 + b203 + b209 + b221 >= 1;

e1141:    b193 + b197 + b203 + b209 + b217 + b222 >= 1;

e1142:    b193 + b197 + b203 + b209 + b216 >= 1;

e1143:    b193 + b197 + b203 + b209 + b212 >= 1;

e1144:    b193 + b197 + b203 + b208 + b221 >= 1;

e1145:    b193 + b197 + b203 + b208 + b217 + b222 >= 1;

e1146:    b193 + b197 + b203 + b208 + b216 >= 1;

e1147:    b193 + b197 + b203 + b208 + b212 >= 1;

e1148:    b193 + b197 + b203 + b207 + b222 >= 1;

e1149:    b193 + b197 + b203 + b207 + b217 >= 1;

e1150:    b193 + b197 + b203 + b207 + b212 >= 1;

e1151:    b193 + b197 + b202 + b220 >= 1;

e1152:    b193 + b197 + b202 + b217 + b221 >= 1;

e1153:    b193 + b197 + b202 + b216 + b222 >= 1;

e1154:    b193 + b197 + b202 + b215 >= 1;

e1155:    b193 + b197 + b202 + b212 + b222 >= 1;

e1156:    b193 + b197 + b202 + b212 + b217 >= 1;

e1157:    b193 + b197 + b202 + b211 >= 1;

e1158:    b193 + b197 + b202 + b209 + b221 >= 1;

e1159:    b193 + b197 + b202 + b209 + b217 + b222 >= 1;

e1160:    b193 + b197 + b202 + b209 + b216 >= 1;

e1161:    b193 + b197 + b202 + b209 + b212 >= 1;

e1162:    b193 + b197 + b202 + b208 + b222 >= 1;

e1163:    b193 + b197 + b202 + b208 + b217 >= 1;

e1164:    b193 + b197 + b202 + b208 + b212 >= 1;

e1165:    b193 + b197 + b201 + b221 >= 1;

e1166:    b193 + b197 + b201 + b217 + b222 >= 1;

e1167:    b193 + b197 + b201 + b216 >= 1;

e1168:    b193 + b197 + b201 + b212 >= 1;

e1169:    b193 + b197 + b201 + b209 + b222 >= 1;

e1170:    b193 + b197 + b201 + b209 + b217 >= 1;

e1171:    b193 + b197 + b201 + b209 + b212 >= 1;

e1172:    b193 + b197 + b200 + b222 >= 1;

e1173:    b193 + b197 + b200 + b217 >= 1;

e1174:    b193 + b197 + b200 + b212 >= 1;

e1175:    b193 + b196 + b220 >= 1;

e1176:    b193 + b196 + b217 + b221 >= 1;

e1177:    b193 + b196 + b216 + b222 >= 1;

e1178:    b193 + b196 + b215 >= 1;

e1179:    b193 + b196 + b212 + b222 >= 1;

e1180:    b193 + b196 + b212 + b217 >= 1;

e1181:    b193 + b196 + b211 >= 1;

e1182:    b193 + b196 + b209 + b221 >= 1;

e1183:    b193 + b196 + b209 + b217 + b222 >= 1;

e1184:    b193 + b196 + b209 + b216 >= 1;

e1185:    b193 + b196 + b209 + b212 >= 1;

e1186:    b193 + b196 + b208 + b222 >= 1;

e1187:    b193 + b196 + b208 + b217 >= 1;

e1188:    b193 + b196 + b208 + b212 >= 1;

e1189:    b193 + b196 + b203 + b221 >= 1;

e1190:    b193 + b196 + b203 + b217 + b222 >= 1;

e1191:    b193 + b196 + b203 + b216 >= 1;

e1192:    b193 + b196 + b203 + b212 >= 1;

e1193:    b193 + b196 + b203 + b209 + b222 >= 1;

e1194:    b193 + b196 + b203 + b209 + b217 >= 1;

e1195:    b193 + b196 + b203 + b209 + b212 >= 1;

e1196:    b193 + b196 + b202 + b222 >= 1;

e1197:    b193 + b196 + b202 + b217 >= 1;

e1198:    b193 + b196 + b202 + b212 >= 1;

e1199:    b193 + b195 + b222 >= 1;

e1200:    b193 + b195 + b217 >= 1;

e1201:    b193 + b195 + b212 >= 1;

e1202:    b192 + b220 >= 1;

e1203:    b192 + b217 + b221 >= 1;

e1204:    b192 + b216 + b222 >= 1;

e1205:    b192 + b215 >= 1;

e1206:    b192 + b212 + b222 >= 1;

e1207:    b192 + b212 + b217 >= 1;

e1208:    b192 + b211 >= 1;

e1209:    b192 + b209 + b221 >= 1;

e1210:    b192 + b209 + b217 + b222 >= 1;

e1211:    b192 + b209 + b216 >= 1;

e1212:    b192 + b209 + b212 >= 1;

e1213:    b192 + b208 + b221 >= 1;

e1214:    b192 + b208 + b217 + b222 >= 1;

e1215:    b192 + b208 + b216 >= 1;

e1216:    b192 + b208 + b212 >= 1;

e1217:    b192 + b207 + b222 >= 1;

e1218:    b192 + b207 + b217 >= 1;

e1219:    b192 + b207 + b212 >= 1;

e1220:    b192 + b203 + b221 >= 1;

e1221:    b192 + b203 + b217 + b222 >= 1;

e1222:    b192 + b203 + b216 >= 1;

e1223:    b192 + b203 + b212 >= 1;

e1224:    b192 + b203 + b209 + b222 >= 1;

e1225:    b192 + b203 + b209 + b216 >= 1;

e1226:    b192 + b203 + b209 + b212 >= 1;

e1227:    b192 + b203 + b208 + b222 >= 1;

e1228:    b192 + b203 + b208 + b217 >= 1;

e1229:    b192 + b203 + b208 + b212 >= 1;

e1230:    b192 + b202 + b221 >= 1;

e1231:    b192 + b202 + b217 + b222 >= 1;

e1232:    b192 + b202 + b216 >= 1;

e1233:    b192 + b202 + b212 >= 1;

e1234:    b192 + b202 + b209 + b222 >= 1;

e1235:    b192 + b202 + b209 + b217 >= 1;

e1236:    b192 + b202 + b209 + b212 >= 1;

e1237:    b192 + b201 + b222 >= 1;

e1238:    b192 + b201 + b217 >= 1;

e1239:    b192 + b201 + b212 >= 1;

e1240:    b192 + b197 + b221 >= 1;

e1241:    b192 + b197 + b217 + b222 >= 1;

e1242:    b192 + b197 + b216 >= 1;

e1243:    b192 + b197 + b212 >= 1;

e1244:    b192 + b197 + b209 + b222 >= 1;

e1245:    b192 + b197 + b209 + b217 >= 1;

e1246:    b192 + b197 + b209 + b212 >= 1;

e1247:    b192 + b197 + b203 + b222 >= 1;

e1248:    b192 + b197 + b203 + b217 >= 1;

e1249:    b192 + b197 + b203 + b212 >= 1;

e1250:    b192 + b196 + b222 >= 1;

e1251:    b192 + b196 + b217 >= 1;

e1252:    b192 + b196 + b212 >= 1;

e1253:    b191 + b222 >= 1;

e1254:    b191 + b217 >= 1;

e1255:    b191 + b212 >= 1;

e1256:    b190 + b218 >= 1;

e1257:    b190 + b217 + b219 >= 1;

e1258:    b190 + b216 + b220 >= 1;

e1259:    b190 + b215 + b221 >= 1;

e1260:    b190 + b214 + b222 >= 1;

e1261:    b190 + b213 >= 1;

e1262:    b190 + b212 + b220 >= 1;

e1263:    b190 + b212 + b217 + b221 >= 1;

e1264:    b190 + b212 + b216 + b222 >= 1;

e1265:    b190 + b212 + b215 >= 1;

e1266:    b190 + b211 + b222 >= 1;

e1267:    b190 + b211 + b217 >= 1;

e1268:    b190 + b210 >= 1;

e1269:    b190 + b209 + b219 >= 1;

e1270:    b190 + b209 + b217 + b220 >= 1;

e1271:    b190 + b209 + b216 + b221 >= 1;

e1272:    b190 + b209 + b215 + b222 >= 1;

e1273:    b190 + b209 + b214 >= 1;

e1274:    b190 + b209 + b212 + b221 >= 1;

e1275:    b190 + b209 + b212 + b217 + b222 >= 1;

e1276:    b190 + b209 + b212 + b216 >= 1;

e1277:    b190 + b209 + b211 >= 1;

e1278:    b190 + b208 + b219 >= 1;

e1279:    b190 + b208 + b217 + b220 >= 1;

e1280:    b190 + b208 + b216 + b221 >= 1;

e1281:    b190 + b208 + b215 >= 1;

e1282:    b190 + b208 + b212 + b221 >= 1;

e1283:    b190 + b208 + b212 + b217 + b222 >= 1;

e1284:    b190 + b208 + b212 + b216 >= 1;

e1285:    b190 + b208 + b211 >= 1;

e1286:    b190 + b207 + b220 >= 1;

e1287:    b190 + b207 + b217 + b221 >= 1;

e1288:    b190 + b207 + b216 + b222 >= 1;

e1289:    b190 + b207 + b215 >= 1;

e1290:    b190 + b207 + b212 + b222 >= 1;

e1291:    b190 + b207 + b212 + b217 >= 1;

e1292:    b190 + b207 + b211 >= 1;

e1293:    b190 + b206 + b221 >= 1;

e1294:    b190 + b206 + b217 + b222 >= 1;

e1295:    b190 + b206 + b216 >= 1;

e1296:    b190 + b206 + b212 >= 1;

e1297:    b190 + b205 + b222 >= 1;

e1298:    b190 + b205 + b217 >= 1;

e1299:    b190 + b205 + b212 >= 1;

e1300:    b190 + b203 + b219 >= 1;

e1301:    b190 + b203 + b217 + b220 >= 1;

e1302:    b190 + b203 + b216 + b221 >= 1;

e1303:    b190 + b203 + b215 + b222 >= 1;

e1304:    b190 + b203 + b214 >= 1;

e1305:    b190 + b203 + b212 + b221 >= 1;

e1306:    b190 + b203 + b212 + b217 + b222 >= 1;

e1307:    b190 + b203 + b212 + b216 >= 1;

e1308:    b190 + b203 + b211 >= 1;

e1309:    b190 + b203 + b209 + b220 >= 1;

e1310:    b190 + b203 + b209 + b216 + b222 >= 1;

e1311:    b190 + b203 + b209 + b215 >= 1;

e1312:    b190 + b203 + b209 + b212 + b222 >= 1;

e1313:    b190 + b203 + b209 + b212 + b216 >= 1;

e1314:    b190 + b203 + b209 + b211 >= 1;

e1315:    b190 + b203 + b208 + b220 >= 1;

e1316:    b190 + b203 + b208 + b217 + b221 >= 1;

e1317:    b190 + b203 + b208 + b216 + b222 >= 1;

e1318:    b190 + b203 + b208 + b215 >= 1;

e1319:    b190 + b203 + b208 + b212 + b222 >= 1;

e1320:    b190 + b203 + b208 + b212 + b217 >= 1;

e1321:    b190 + b203 + b208 + b211 >= 1;

e1322:    b190 + b203 + b207 + b221 >= 1;

e1323:    b190 + b203 + b207 + b217 + b222 >= 1;

e1324:    b190 + b203 + b207 + b216 >= 1;

e1325:    b190 + b203 + b207 + b212 >= 1;

e1326:    b190 + b203 + b206 + b222 >= 1;

e1327:    b190 + b203 + b206 + b217 >= 1;

e1328:    b190 + b203 + b206 + b212 >= 1;

e1329:    b190 + b202 + b219 >= 1;

e1330:    b190 + b202 + b217 + b220 >= 1;

e1331:    b190 + b202 + b216 + b221 >= 1;

e1332:    b190 + b202 + b215 + b222 >= 1;

e1333:    b190 + b202 + b214 >= 1;

e1334:    b190 + b202 + b212 + b221 >= 1;

e1335:    b190 + b202 + b212 + b217 + b222 >= 1;

e1336:    b190 + b202 + b212 + b216 >= 1;

e1337:    b190 + b202 + b211 >= 1;

e1338:    b190 + b202 + b209 + b220 >= 1;

e1339:    b190 + b202 + b209 + b217 + b221 >= 1;

e1340:    b190 + b202 + b209 + b216 + b222 >= 1;

e1341:    b190 + b202 + b209 + b215 >= 1;

e1342:    b190 + b202 + b209 + b212 + b222 >= 1;

e1343:    b190 + b202 + b209 + b212 + b217 >= 1;

e1344:    b190 + b202 + b209 + b211 >= 1;

e1345:    b190 + b202 + b208 + b221 >= 1;

e1346:    b190 + b202 + b208 + b217 + b222 >= 1;

e1347:    b190 + b202 + b208 + b216 >= 1;

e1348:    b190 + b202 + b208 + b212 >= 1;

e1349:    b190 + b202 + b207 + b222 >= 1;

e1350:    b190 + b202 + b207 + b217 >= 1;

e1351:    b190 + b202 + b207 + b212 >= 1;

e1352:    b190 + b201 + b220 >= 1;

e1353:    b190 + b201 + b217 + b221 >= 1;

e1354:    b190 + b201 + b216 + b222 >= 1;

e1355:    b190 + b201 + b215 >= 1;

e1356:    b190 + b201 + b212 + b222 >= 1;

e1357:    b190 + b201 + b212 + b217 >= 1;

e1358:    b190 + b201 + b211 >= 1;

e1359:    b190 + b201 + b209 + b221 >= 1;

e1360:    b190 + b201 + b209 + b217 + b222 >= 1;

e1361:    b190 + b201 + b209 + b216 >= 1;

e1362:    b190 + b201 + b209 + b212 >= 1;

e1363:    b190 + b201 + b208 + b222 >= 1;

e1364:    b190 + b201 + b208 + b217 >= 1;

e1365:    b190 + b201 + b208 + b212 >= 1;

e1366:    b190 + b200 + b221 >= 1;

e1367:    b190 + b200 + b217 + b222 >= 1;

e1368:    b190 + b200 + b216 >= 1;

e1369:    b190 + b200 + b212 >= 1;

e1370:    b190 + b200 + b209 + b222 >= 1;

e1371:    b190 + b200 + b209 + b217 >= 1;

e1372:    b190 + b200 + b209 + b212 >= 1;

e1373:    b190 + b199 + b222 >= 1;

e1374:    b190 + b199 + b217 >= 1;

e1375:    b190 + b199 + b212 >= 1;

e1376:    b190 + b197 + b219 >= 1;

e1377:    b190 + b197 + b217 + b220 >= 1;

e1378:    b190 + b197 + b216 + b221 >= 1;

e1379:    b190 + b197 + b215 + b222 >= 1;

e1380:    b190 + b197 + b214 >= 1;

e1381:    b190 + b197 + b212 + b221 >= 1;

e1382:    b190 + b197 + b212 + b217 + b222 >= 1;

e1383:    b190 + b197 + b212 + b216 >= 1;

e1384:    b190 + b197 + b211 >= 1;

e1385:    b190 + b197 + b209 + b220 >= 1;

e1386:    b190 + b197 + b209 + b217 + b221 >= 1;

e1387:    b190 + b197 + b209 + b216 + b222 >= 1;

e1388:    b190 + b197 + b209 + b215 >= 1;

e1389:    b190 + b197 + b209 + b212 + b222 >= 1;

e1390:    b190 + b197 + b209 + b212 + b217 >= 1;

e1391:    b190 + b197 + b209 + b211 >= 1;

e1392:    b190 + b197 + b208 + b221 >= 1;

e1393:    b190 + b197 + b208 + b217 + b222 >= 1;

e1394:    b190 + b197 + b208 + b216 >= 1;

e1395:    b190 + b197 + b208 + b212 >= 1;

e1396:    b190 + b197 + b207 + b221 >= 1;

e1397:    b190 + b197 + b207 + b217 + b222 >= 1;

e1398:    b190 + b197 + b207 + b216 >= 1;

e1399:    b190 + b197 + b207 + b212 >= 1;

e1400:    b190 + b197 + b206 + b222 >= 1;

e1401:    b190 + b197 + b206 + b217 >= 1;

e1402:    b190 + b197 + b206 + b212 >= 1;

e1403:    b190 + b197 + b203 + b220 >= 1;

e1404:    b190 + b197 + b203 + b217 + b221 >= 1;

e1405:    b190 + b197 + b203 + b216 + b222 >= 1;

e1406:    b190 + b197 + b203 + b215 >= 1;

e1407:    b190 + b197 + b203 + b212 + b222 >= 1;

e1408:    b190 + b197 + b203 + b212 + b217 >= 1;

e1409:    b190 + b197 + b203 + b211 >= 1;

e1410:    b190 + b197 + b203 + b209 + b221 >= 1;

e1411:    b190 + b197 + b203 + b209 + b217 + b222 >= 1;

e1412:    b190 + b197 + b203 + b209 + b216 >= 1;

e1413:    b190 + b197 + b203 + b209 + b212 >= 1;

e1414:    b190 + b197 + b203 + b208 + b221 >= 1;

e1415:    b190 + b197 + b203 + b208 + b217 + b222 >= 1;

e1416:    b190 + b197 + b203 + b208 + b216 >= 1;

e1417:    b190 + b197 + b203 + b208 + b212 >= 1;

e1418:    b190 + b197 + b203 + b207 + b222 >= 1;

e1419:    b190 + b197 + b203 + b207 + b217 >= 1;

e1420:    b190 + b197 + b203 + b207 + b212 >= 1;

e1421:    b190 + b197 + b202 + b221 >= 1;

e1422:    b190 + b197 + b202 + b216 >= 1;

e1423:    b190 + b197 + b202 + b212 >= 1;

e1424:    b190 + b197 + b202 + b209 + b221 >= 1;

e1425:    b190 + b197 + b202 + b209 + b217 + b222 >= 1;

e1426:    b190 + b197 + b202 + b209 + b216 >= 1;

e1427:    b190 + b197 + b202 + b209 + b212 >= 1;

e1428:    b190 + b197 + b202 + b208 + b222 >= 1;

e1429:    b190 + b197 + b202 + b208 + b217 >= 1;

e1430:    b190 + b197 + b202 + b208 + b212 >= 1;

e1431:    b190 + b197 + b201 + b221 >= 1;

e1432:    b190 + b197 + b201 + b217 + b222 >= 1;

e1433:    b190 + b197 + b201 + b216 >= 1;

e1434:    b190 + b197 + b201 + b212 >= 1;

e1435:    b190 + b197 + b201 + b209 + b222 >= 1;

e1436:    b190 + b197 + b201 + b209 + b217 >= 1;

e1437:    b190 + b197 + b201 + b209 + b212 >= 1;

e1438:    b190 + b197 + b200 + b222 >= 1;

e1439:    b190 + b197 + b200 + b217 >= 1;

e1440:    b190 + b197 + b200 + b212 >= 1;

e1441:    b190 + b196 + b220 >= 1;

e1442:    b190 + b196 + b217 + b221 >= 1;

e1443:    b190 + b196 + b216 + b222 >= 1;

e1444:    b190 + b196 + b215 >= 1;

e1445:    b190 + b196 + b212 + b222 >= 1;

e1446:    b190 + b196 + b212 + b217 >= 1;

e1447:    b190 + b196 + b211 >= 1;

e1448:    b190 + b196 + b209 + b221 >= 1;

e1449:    b190 + b196 + b209 + b217 + b222 >= 1;

e1450:    b190 + b196 + b209 + b216 >= 1;

e1451:    b190 + b196 + b209 + b212 >= 1;

e1452:    b190 + b196 + b208 + b222 >= 1;

e1453:    b190 + b196 + b208 + b217 >= 1;

e1454:    b190 + b196 + b208 + b212 >= 1;

e1455:    b190 + b196 + b203 + b221 >= 1;

e1456:    b190 + b196 + b203 + b217 + b222 >= 1;

e1457:    b190 + b196 + b203 + b216 >= 1;

e1458:    b190 + b196 + b203 + b212 >= 1;

e1459:    b190 + b196 + b203 + b209 + b222 >= 1;

e1460:    b190 + b196 + b203 + b209 + b217 >= 1;

e1461:    b190 + b196 + b203 + b209 + b212 >= 1;

e1462:    b190 + b196 + b202 + b222 >= 1;

e1463:    b190 + b196 + b202 + b217 >= 1;

e1464:    b190 + b196 + b202 + b212 >= 1;

e1465:    b190 + b195 + b222 >= 1;

e1466:    b190 + b195 + b217 >= 1;

e1467:    b190 + b195 + b212 >= 1;

e1468:    b190 + b193 + b220 >= 1;

e1469:    b190 + b193 + b217 + b221 >= 1;

e1470:    b190 + b193 + b216 + b222 >= 1;

e1471:    b190 + b193 + b215 >= 1;

e1472:    b190 + b193 + b212 + b222 >= 1;

e1473:    b190 + b193 + b212 + b217 >= 1;

e1474:    b190 + b193 + b211 >= 1;

e1475:    b190 + b193 + b209 + b221 >= 1;

e1476:    b190 + b193 + b209 + b217 + b222 >= 1;

e1477:    b190 + b193 + b209 + b216 >= 1;

e1478:    b190 + b193 + b209 + b212 >= 1;

e1479:    b190 + b193 + b208 + b221 >= 1;

e1480:    b190 + b193 + b208 + b217 + b222 >= 1;

e1481:    b190 + b193 + b208 + b216 >= 1;

e1482:    b190 + b193 + b208 + b212 >= 1;

e1483:    b190 + b193 + b207 + b222 >= 1;

e1484:    b190 + b193 + b207 + b217 >= 1;

e1485:    b190 + b193 + b207 + b212 >= 1;

e1486:    b190 + b193 + b203 + b221 >= 1;

e1487:    b190 + b193 + b203 + b217 + b222 >= 1;

e1488:    b190 + b193 + b203 + b216 >= 1;

e1489:    b190 + b193 + b203 + b212 >= 1;

e1490:    b190 + b193 + b203 + b209 + b221 >= 1;

e1491:    b190 + b193 + b203 + b209 + b217 + b222 >= 1;

e1492:    b190 + b193 + b203 + b209 + b216 >= 1;

e1493:    b190 + b193 + b203 + b209 + b212 >= 1;

e1494:    b190 + b193 + b203 + b208 + b222 >= 1;

e1495:    b190 + b193 + b203 + b208 + b217 >= 1;

e1496:    b190 + b193 + b203 + b208 + b212 >= 1;

e1497:    b190 + b193 + b202 + b221 >= 1;

e1498:    b190 + b193 + b202 + b217 + b222 >= 1;

e1499:    b190 + b193 + b202 + b216 >= 1;

e1500:    b190 + b193 + b202 + b212 >= 1;

e1501:    b190 + b193 + b202 + b209 + b222 >= 1;

e1502:    b190 + b193 + b202 + b209 + b217 >= 1;

e1503:    b190 + b193 + b202 + b209 + b212 >= 1;

e1504:    b190 + b193 + b201 + b222 >= 1;

e1505:    b190 + b193 + b201 + b217 >= 1;

e1506:    b190 + b193 + b201 + b212 >= 1;

e1507:    b190 + b193 + b197 + b221 >= 1;

e1508:    b190 + b193 + b197 + b217 + b222 >= 1;

e1509:    b190 + b193 + b197 + b216 >= 1;

e1510:    b190 + b193 + b197 + b212 >= 1;

e1511:    b190 + b193 + b197 + b209 + b222 >= 1;

e1512:    b190 + b193 + b197 + b209 + b217 >= 1;

e1513:    b190 + b193 + b197 + b209 + b212 >= 1;

e1514:    b190 + b193 + b197 + b208 + b222 >= 1;

e1515:    b190 + b193 + b197 + b208 + b217 >= 1;

e1516:    b190 + b193 + b197 + b208 + b212 >= 1;

e1517:    b190 + b193 + b197 + b203 + b222 >= 1;

e1518:    b190 + b193 + b197 + b203 + b217 >= 1;

e1519:    b190 + b193 + b197 + b203 + b212 >= 1;

e1520:    b190 + b193 + b197 + b202 + b222 >= 1;

e1521:    b190 + b193 + b197 + b202 + b217 >= 1;

e1522:    b190 + b193 + b197 + b202 + b212 >= 1;

e1523:    b190 + b193 + b196 + b222 >= 1;

e1524:    b190 + b193 + b196 + b217 >= 1;

e1525:    b190 + b193 + b196 + b212 >= 1;

e1526:    b190 + b192 + b222 >= 1;

e1527:    b190 + b192 + b217 >= 1;

e1528:    b190 + b192 + b212 >= 1;

e1529:    b189 + b220 >= 1;

e1530:    b189 + b217 + b221 >= 1;

e1531:    b189 + b216 + b222 >= 1;

e1532:    b189 + b215 >= 1;

e1533:    b189 + b212 + b222 >= 1;

e1534:    b189 + b212 + b217 >= 1;

e1535:    b189 + b211 >= 1;

e1536:    b189 + b209 + b221 >= 1;

e1537:    b189 + b209 + b217 + b222 >= 1;

e1538:    b189 + b209 + b216 >= 1;

e1539:    b189 + b209 + b212 >= 1;

e1540:    b189 + b208 + b221 >= 1;

e1541:    b189 + b208 + b217 + b222 >= 1;

e1542:    b189 + b208 + b216 >= 1;

e1543:    b189 + b208 + b212 >= 1;

e1544:    b189 + b207 + b222 >= 1;

e1545:    b189 + b207 + b217 >= 1;

e1546:    b189 + b207 + b212 >= 1;

e1547:    b189 + b203 + b221 >= 1;

e1548:    b189 + b203 + b216 + b222 >= 1;

e1549:    b189 + b203 + b215 >= 1;

e1550:    b189 + b203 + b212 >= 1;

e1551:    b189 + b203 + b209 + b221 >= 1;

e1552:    b189 + b203 + b209 + b217 + b222 >= 1;

e1553:    b189 + b203 + b209 + b216 >= 1;

e1554:    b189 + b203 + b209 + b212 >= 1;

e1555:    b189 + b203 + b208 + b222 >= 1;

e1556:    b189 + b203 + b208 + b217 >= 1;

e1557:    b189 + b203 + b208 + b212 >= 1;

e1558:    b189 + b202 + b221 >= 1;

e1559:    b189 + b202 + b217 + b222 >= 1;

e1560:    b189 + b202 + b216 >= 1;

e1561:    b189 + b202 + b212 >= 1;

e1562:    b189 + b202 + b209 + b222 >= 1;

e1563:    b189 + b202 + b209 + b217 >= 1;

e1564:    b189 + b202 + b209 + b212 >= 1;

e1565:    b189 + b201 + b222 >= 1;

e1566:    b189 + b201 + b217 >= 1;

e1567:    b189 + b201 + b212 >= 1;

e1568:    b189 + b197 + b221 >= 1;

e1569:    b189 + b197 + b217 + b222 >= 1;

e1570:    b189 + b197 + b216 >= 1;

e1571:    b189 + b197 + b212 >= 1;

e1572:    b189 + b197 + b209 + b222 >= 1;

e1573:    b189 + b197 + b209 + b217 >= 1;

e1574:    b189 + b197 + b209 + b212 >= 1;

e1575:    b189 + b197 + b203 + b222 >= 1;

e1576:    b189 + b197 + b203 + b217 >= 1;

e1577:    b189 + b197 + b203 + b212 >= 1;

e1578:    b189 + b197 + b202 + b222 >= 1;

e1579:    b189 + b197 + b202 + b217 >= 1;

e1580:    b189 + b197 + b202 + b212 >= 1;

e1581:    b189 + b196 + b222 >= 1;

e1582:    b189 + b196 + b217 >= 1;

e1583:    b189 + b196 + b212 >= 1;

e1584:    b189 + b193 + b222 >= 1;

e1585:    b189 + b193 + b217 >= 1;

e1586:    b189 + b193 + b212 >= 1;

e1587:    b189 + b193 + b203 + b222 >= 1;

e1588:    b189 + b193 + b203 + b217 >= 1;

e1589:    b189 + b193 + b203 + b212 >= 1;

e1590:    b188 + b222 >= 1;

e1591:    b188 + b217 >= 1;

e1592:    b188 + b212 >= 1;

e1593:    b187 + b218 >= 1;

e1594:    b187 + b217 + b219 >= 1;

e1595:    b187 + b216 + b220 >= 1;

e1596:    b187 + b215 + b221 >= 1;

e1597:    b187 + b214 + b222 >= 1;

e1598:    b187 + b213 >= 1;

e1599:    b187 + b212 + b220 >= 1;

e1600:    b187 + b212 + b217 + b221 >= 1;

e1601:    b187 + b212 + b215 >= 1;

e1602:    b187 + b211 + b222 >= 1;

e1603:    b187 + b211 + b217 >= 1;

e1604:    b187 + b210 >= 1;

e1605:    b187 + b209 + b219 >= 1;

e1606:    b187 + b209 + b216 + b220 >= 1;

e1607:    b187 + b209 + b215 + b222 >= 1;

e1608:    b187 + b209 + b214 >= 1;

e1609:    b187 + b209 + b212 + b220 >= 1;

e1610:    b187 + b209 + b212 + b217 + b221 >= 1;

e1611:    b187 + b209 + b212 + b216 + b222 >= 1;

e1612:    b187 + b209 + b212 + b215 >= 1;

e1613:    b187 + b209 + b211 >= 1;

e1614:    b187 + b208 + b219 >= 1;

e1615:    b187 + b208 + b217 + b220 >= 1;

e1616:    b187 + b208 + b216 + b221 >= 1;

e1617:    b187 + b208 + b215 + b222 >= 1;

e1618:    b187 + b208 + b214 >= 1;

e1619:    b187 + b208 + b212 + b221 >= 1;

e1620:    b187 + b208 + b212 + b217 + b222 >= 1;

e1621:    b187 + b208 + b212 + b216 >= 1;

e1622:    b187 + b208 + b211 >= 1;

e1623:    b187 + b207 + b220 >= 1;

e1624:    b187 + b207 + b217 + b221 >= 1;

e1625:    b187 + b207 + b216 + b222 >= 1;

e1626:    b187 + b207 + b215 >= 1;

e1627:    b187 + b207 + b212 + b222 >= 1;

e1628:    b187 + b207 + b212 + b217 >= 1;

e1629:    b187 + b207 + b211 >= 1;

e1630:    b187 + b206 + b221 >= 1;

e1631:    b187 + b206 + b217 + b222 >= 1;

e1632:    b187 + b206 + b216 >= 1;

e1633:    b187 + b206 + b212 >= 1;

e1634:    b187 + b205 + b222 >= 1;

e1635:    b187 + b205 + b217 >= 1;

e1636:    b187 + b205 + b212 >= 1;

e1637:    b187 + b203 + b219 >= 1;

e1638:    b187 + b203 + b216 + b220 >= 1;

e1639:    b187 + b203 + b215 + b221 >= 1;

e1640:    b187 + b203 + b214 >= 1;

e1641:    b187 + b203 + b212 + b220 >= 1;

e1642:    b187 + b203 + b212 + b217 + b221 >= 1;

e1643:    b187 + b203 + b212 + b216 + b222 >= 1;

e1644:    b187 + b203 + b212 + b215 >= 1;

e1645:    b187 + b203 + b211 >= 1;

e1646:    b187 + b203 + b209 + b219 >= 1;

e1647:    b187 + b203 + b209 + b217 + b220 >= 1;

e1648:    b187 + b203 + b209 + b216 + b221 >= 1;

e1649:    b187 + b203 + b209 + b215 + b222 >= 1;

e1650:    b187 + b203 + b209 + b214 >= 1;

e1651:    b187 + b203 + b209 + b212 + b221 >= 1;

e1652:    b187 + b203 + b209 + b212 + b217 + b222 >= 1;

e1653:    b187 + b203 + b209 + b212 + b216 >= 1;

e1654:    b187 + b203 + b209 + b211 >= 1;

e1655:    b187 + b203 + b208 + b220 >= 1;

e1656:    b187 + b203 + b208 + b217 + b221 >= 1;

e1657:    b187 + b203 + b208 + b216 + b222 >= 1;

e1658:    b187 + b203 + b208 + b215 >= 1;

e1659:    b187 + b203 + b208 + b212 + b222 >= 1;

e1660:    b187 + b203 + b208 + b212 + b217 >= 1;

e1661:    b187 + b203 + b208 + b211 >= 1;

e1662:    b187 + b203 + b207 + b221 >= 1;

e1663:    b187 + b203 + b207 + b217 + b222 >= 1;

e1664:    b187 + b203 + b207 + b216 >= 1;

e1665:    b187 + b203 + b207 + b212 >= 1;

e1666:    b187 + b203 + b206 + b222 >= 1;

e1667:    b187 + b203 + b206 + b217 >= 1;

e1668:    b187 + b203 + b206 + b212 >= 1;

e1669:    b187 + b203 + b205 + b222 >= 1;

e1670:    b187 + b203 + b205 + b217 >= 1;

e1671:    b187 + b203 + b205 + b212 >= 1;

e1672:    b187 + b202 + b219 >= 1;

e1673:    b187 + b202 + b217 + b220 >= 1;

e1674:    b187 + b202 + b216 + b221 >= 1;

e1675:    b187 + b202 + b215 + b222 >= 1;

e1676:    b187 + b202 + b214 >= 1;

e1677:    b187 + b202 + b212 + b221 >= 1;

e1678:    b187 + b202 + b212 + b217 + b222 >= 1;

e1679:    b187 + b202 + b212 + b216 >= 1;

e1680:    b187 + b202 + b211 >= 1;

e1681:    b187 + b202 + b209 + b220 >= 1;

e1682:    b187 + b202 + b209 + b217 + b221 >= 1;

e1683:    b187 + b202 + b209 + b216 + b222 >= 1;

e1684:    b187 + b202 + b209 + b215 >= 1;

e1685:    b187 + b202 + b209 + b212 + b222 >= 1;

e1686:    b187 + b202 + b209 + b212 + b217 >= 1;

e1687:    b187 + b202 + b209 + b211 >= 1;

e1688:    b187 + b202 + b208 + b221 >= 1;

e1689:    b187 + b202 + b208 + b217 + b222 >= 1;

e1690:    b187 + b202 + b208 + b216 >= 1;

e1691:    b187 + b202 + b208 + b212 >= 1;

e1692:    b187 + b202 + b207 + b222 >= 1;

e1693:    b187 + b202 + b207 + b217 >= 1;

e1694:    b187 + b202 + b207 + b212 >= 1;

e1695:    b187 + b202 + b206 + b222 >= 1;

e1696:    b187 + b202 + b206 + b217 >= 1;

e1697:    b187 + b202 + b206 + b212 >= 1;

e1698:    b187 + b201 + b220 >= 1;

e1699:    b187 + b201 + b217 + b221 >= 1;

e1700:    b187 + b201 + b216 + b222 >= 1;

e1701:    b187 + b201 + b215 >= 1;

e1702:    b187 + b201 + b212 + b222 >= 1;

e1703:    b187 + b201 + b212 + b217 >= 1;

e1704:    b187 + b201 + b211 >= 1;

e1705:    b187 + b201 + b209 + b221 >= 1;

e1706:    b187 + b201 + b209 + b217 + b222 >= 1;

e1707:    b187 + b201 + b209 + b216 >= 1;

e1708:    b187 + b201 + b209 + b212 >= 1;

e1709:    b187 + b201 + b208 + b222 >= 1;

e1710:    b187 + b201 + b208 + b217 >= 1;

e1711:    b187 + b201 + b208 + b212 >= 1;

e1712:    b187 + b201 + b207 + b222 >= 1;

e1713:    b187 + b201 + b207 + b217 >= 1;

e1714:    b187 + b201 + b207 + b212 >= 1;

e1715:    b187 + b200 + b221 >= 1;

e1716:    b187 + b200 + b217 + b222 >= 1;

e1717:    b187 + b200 + b216 >= 1;

e1718:    b187 + b200 + b212 >= 1;

e1719:    b187 + b200 + b209 + b222 >= 1;

e1720:    b187 + b200 + b209 + b217 >= 1;

e1721:    b187 + b200 + b209 + b212 >= 1;

e1722:    b187 + b200 + b208 + b222 >= 1;

e1723:    b187 + b200 + b208 + b217 >= 1;

e1724:    b187 + b200 + b208 + b212 >= 1;

e1725:    b187 + b199 + b222 >= 1;

e1726:    b187 + b199 + b217 >= 1;

e1727:    b187 + b199 + b212 >= 1;

e1728:    b187 + b197 + b219 >= 1;

e1729:    b187 + b197 + b217 + b220 >= 1;

e1730:    b187 + b197 + b216 + b221 >= 1;

e1731:    b187 + b197 + b215 + b222 >= 1;

e1732:    b187 + b197 + b214 >= 1;

e1733:    b187 + b197 + b212 + b221 >= 1;

e1734:    b187 + b197 + b212 + b217 + b222 >= 1;

e1735:    b187 + b197 + b212 + b216 >= 1;

e1736:    b187 + b197 + b211 >= 1;

e1737:    b187 + b197 + b209 + b220 >= 1;

e1738:    b187 + b197 + b209 + b217 + b221 >= 1;

e1739:    b187 + b197 + b209 + b216 + b222 >= 1;

e1740:    b187 + b197 + b209 + b215 >= 1;

e1741:    b187 + b197 + b209 + b212 + b222 >= 1;

e1742:    b187 + b197 + b209 + b212 + b217 >= 1;

e1743:    b187 + b197 + b209 + b211 >= 1;

e1744:    b187 + b197 + b208 + b220 >= 1;

e1745:    b187 + b197 + b208 + b217 + b221 >= 1;

e1746:    b187 + b197 + b208 + b216 + b222 >= 1;

e1747:    b187 + b197 + b208 + b215 >= 1;

e1748:    b187 + b197 + b208 + b212 + b222 >= 1;

e1749:    b187 + b197 + b208 + b212 + b217 >= 1;

e1750:    b187 + b197 + b208 + b211 >= 1;

e1751:    b187 + b197 + b207 + b221 >= 1;

e1752:    b187 + b197 + b207 + b217 + b222 >= 1;

e1753:    b187 + b197 + b207 + b216 >= 1;

e1754:    b187 + b197 + b207 + b212 >= 1;

e1755:    b187 + b197 + b206 + b222 >= 1;

e1756:    b187 + b197 + b206 + b217 >= 1;

e1757:    b187 + b197 + b206 + b212 >= 1;

e1758:    b187 + b197 + b203 + b220 >= 1;

e1759:    b187 + b197 + b203 + b217 + b221 >= 1;

e1760:    b187 + b197 + b203 + b216 + b222 >= 1;

e1761:    b187 + b197 + b203 + b215 >= 1;

e1762:    b187 + b197 + b203 + b212 + b222 >= 1;

e1763:    b187 + b197 + b203 + b212 + b217 >= 1;

e1764:    b187 + b197 + b203 + b211 >= 1;

e1765:    b187 + b197 + b203 + b209 + b220 >= 1;

e1766:    b187 + b197 + b203 + b209 + b217 + b221 >= 1;

e1767:    b187 + b197 + b203 + b209 + b216 >= 1;

e1768:    b187 + b197 + b203 + b209 + b212 >= 1;

e1769:    b187 + b197 + b203 + b208 + b221 >= 1;

e1770:    b187 + b197 + b203 + b208 + b217 + b222 >= 1;

e1771:    b187 + b197 + b203 + b208 + b216 >= 1;

e1772:    b187 + b197 + b203 + b208 + b212 >= 1;

e1773:    b187 + b197 + b203 + b207 + b222 >= 1;

e1774:    b187 + b197 + b203 + b207 + b217 >= 1;

e1775:    b187 + b197 + b203 + b207 + b212 >= 1;

e1776:    b187 + b197 + b202 + b220 >= 1;

e1777:    b187 + b197 + b202 + b217 + b221 >= 1;

e1778:    b187 + b197 + b202 + b216 + b222 >= 1;

e1779:    b187 + b197 + b202 + b215 >= 1;

e1780:    b187 + b197 + b202 + b212 + b222 >= 1;

e1781:    b187 + b197 + b202 + b212 + b217 >= 1;

e1782:    b187 + b197 + b202 + b211 >= 1;

e1783:    b187 + b197 + b202 + b209 + b221 >= 1;

e1784:    b187 + b197 + b202 + b209 + b217 + b222 >= 1;

e1785:    b187 + b197 + b202 + b209 + b216 >= 1;

e1786:    b187 + b197 + b202 + b209 + b212 >= 1;

e1787:    b187 + b197 + b202 + b208 + b222 >= 1;

e1788:    b187 + b197 + b202 + b208 + b217 >= 1;

e1789:    b187 + b197 + b202 + b208 + b212 >= 1;

e1790:    b187 + b197 + b201 + b221 >= 1;

e1791:    b187 + b197 + b201 + b217 + b222 >= 1;

e1792:    b187 + b197 + b201 + b216 >= 1;

e1793:    b187 + b197 + b201 + b212 >= 1;

e1794:    b187 + b197 + b201 + b209 + b222 >= 1;

e1795:    b187 + b197 + b201 + b209 + b217 >= 1;

e1796:    b187 + b197 + b201 + b209 + b212 >= 1;

e1797:    b187 + b197 + b200 + b222 >= 1;

e1798:    b187 + b197 + b200 + b217 >= 1;

e1799:    b187 + b197 + b200 + b212 >= 1;

e1800:    b187 + b196 + b220 >= 1;

e1801:    b187 + b196 + b217 + b221 >= 1;

e1802:    b187 + b196 + b216 + b222 >= 1;

e1803:    b187 + b196 + b215 >= 1;

e1804:    b187 + b196 + b212 + b222 >= 1;

e1805:    b187 + b196 + b212 + b217 >= 1;

e1806:    b187 + b196 + b211 >= 1;

e1807:    b187 + b196 + b209 + b221 >= 1;

e1808:    b187 + b196 + b209 + b217 + b222 >= 1;

e1809:    b187 + b196 + b209 + b216 >= 1;

e1810:    b187 + b196 + b209 + b212 >= 1;

e1811:    b187 + b196 + b208 + b222 >= 1;

e1812:    b187 + b196 + b208 + b217 >= 1;

e1813:    b187 + b196 + b208 + b212 >= 1;

e1814:    b187 + b196 + b203 + b221 >= 1;

e1815:    b187 + b196 + b203 + b217 + b222 >= 1;

e1816:    b187 + b196 + b203 + b216 >= 1;

e1817:    b187 + b196 + b203 + b212 >= 1;

e1818:    b187 + b196 + b203 + b209 + b222 >= 1;

e1819:    b187 + b196 + b203 + b209 + b217 >= 1;

e1820:    b187 + b196 + b203 + b209 + b212 >= 1;

e1821:    b187 + b196 + b202 + b222 >= 1;

e1822:    b187 + b196 + b202 + b217 >= 1;

e1823:    b187 + b196 + b202 + b212 >= 1;

e1824:    b187 + b195 + b222 >= 1;

e1825:    b187 + b195 + b217 >= 1;

e1826:    b187 + b195 + b212 >= 1;

e1827:    b187 + b195 + b203 + b222 >= 1;

e1828:    b187 + b195 + b203 + b217 >= 1;

e1829:    b187 + b195 + b203 + b212 >= 1;

e1830:    b187 + b193 + b220 >= 1;

e1831:    b187 + b193 + b216 + b221 >= 1;

e1832:    b187 + b193 + b215 >= 1;

e1833:    b187 + b193 + b212 + b221 >= 1;

e1834:    b187 + b193 + b212 + b217 + b222 >= 1;

e1835:    b187 + b193 + b212 + b216 >= 1;

e1836:    b187 + b193 + b211 >= 1;

e1837:    b187 + b193 + b209 + b220 >= 1;

e1838:    b187 + b193 + b209 + b217 + b221 >= 1;

e1839:    b187 + b193 + b209 + b216 + b222 >= 1;

e1840:    b187 + b193 + b209 + b215 >= 1;

e1841:    b187 + b193 + b209 + b212 + b222 >= 1;

e1842:    b187 + b193 + b209 + b212 + b217 >= 1;

e1843:    b187 + b193 + b209 + b211 >= 1;

e1844:    b187 + b193 + b208 + b221 >= 1;

e1845:    b187 + b193 + b208 + b217 + b222 >= 1;

e1846:    b187 + b193 + b208 + b216 >= 1;

e1847:    b187 + b193 + b208 + b212 >= 1;

e1848:    b187 + b193 + b207 + b222 >= 1;

e1849:    b187 + b193 + b207 + b217 >= 1;

e1850:    b187 + b193 + b207 + b212 >= 1;

e1851:    b187 + b193 + b203 + b220 >= 1;

e1852:    b187 + b193 + b203 + b217 + b221 >= 1;

e1853:    b187 + b193 + b203 + b216 + b222 >= 1;

e1854:    b187 + b193 + b203 + b215 >= 1;

e1855:    b187 + b193 + b203 + b212 + b222 >= 1;

e1856:    b187 + b193 + b203 + b212 + b217 >= 1;

e1857:    b187 + b193 + b203 + b211 >= 1;

e1858:    b187 + b193 + b203 + b209 + b221 >= 1;

e1859:    b187 + b193 + b203 + b209 + b217 + b222 >= 1;

e1860:    b187 + b193 + b203 + b209 + b216 >= 1;

e1861:    b187 + b193 + b203 + b209 + b212 >= 1;

e1862:    b187 + b193 + b203 + b208 + b222 >= 1;

e1863:    b187 + b193 + b203 + b208 + b217 >= 1;

e1864:    b187 + b193 + b203 + b208 + b212 >= 1;

e1865:    b187 + b193 + b202 + b221 >= 1;

e1866:    b187 + b193 + b202 + b217 + b222 >= 1;

e1867:    b187 + b193 + b202 + b216 >= 1;

e1868:    b187 + b193 + b202 + b212 >= 1;

e1869:    b187 + b193 + b202 + b209 + b222 >= 1;

e1870:    b187 + b193 + b202 + b209 + b217 >= 1;

e1871:    b187 + b193 + b202 + b209 + b212 >= 1;

e1872:    b187 + b193 + b201 + b222 >= 1;

e1873:    b187 + b193 + b201 + b217 >= 1;

e1874:    b187 + b193 + b201 + b212 >= 1;

e1875:    b187 + b193 + b197 + b221 >= 1;

e1876:    b187 + b193 + b197 + b217 + b222 >= 1;

e1877:    b187 + b193 + b197 + b216 >= 1;

e1878:    b187 + b193 + b197 + b212 >= 1;

e1879:    b187 + b193 + b197 + b209 + b222 >= 1;

e1880:    b187 + b193 + b197 + b209 + b217 >= 1;

e1881:    b187 + b193 + b197 + b209 + b212 >= 1;

e1882:    b187 + b193 + b197 + b208 + b222 >= 1;

e1883:    b187 + b193 + b197 + b208 + b217 >= 1;

e1884:    b187 + b193 + b197 + b208 + b212 >= 1;

e1885:    b187 + b193 + b197 + b203 + b222 >= 1;

e1886:    b187 + b193 + b197 + b203 + b217 >= 1;

e1887:    b187 + b193 + b197 + b203 + b212 >= 1;

e1888:    b187 + b193 + b197 + b203 + b209 + b222 >= 1;

e1889:    b187 + b193 + b197 + b203 + b209 + b217 >= 1;

e1890:    b187 + b193 + b197 + b203 + b209 + b212 >= 1;

e1891:    b187 + b193 + b197 + b202 + b222 >= 1;

e1892:    b187 + b193 + b197 + b202 + b217 >= 1;

e1893:    b187 + b193 + b197 + b202 + b212 >= 1;

e1894:    b187 + b193 + b196 + b222 >= 1;

e1895:    b187 + b193 + b196 + b217 >= 1;

e1896:    b187 + b193 + b196 + b212 >= 1;

e1897:    b187 + b192 + b222 >= 1;

e1898:    b187 + b192 + b217 >= 1;

e1899:    b187 + b192 + b212 >= 1;

e1900:    b187 + b190 + b220 >= 1;

e1901:    b187 + b190 + b217 + b221 >= 1;

e1902:    b187 + b190 + b216 + b222 >= 1;

e1903:    b187 + b190 + b215 >= 1;

e1904:    b187 + b190 + b212 + b222 >= 1;

e1905:    b187 + b190 + b212 + b217 >= 1;

e1906:    b187 + b190 + b211 >= 1;

e1907:    b187 + b190 + b209 + b221 >= 1;

e1908:    b187 + b190 + b209 + b217 + b222 >= 1;

e1909:    b187 + b190 + b209 + b216 >= 1;

e1910:    b187 + b190 + b209 + b212 >= 1;

e1911:    b187 + b190 + b208 + b221 >= 1;

e1912:    b187 + b190 + b208 + b217 + b222 >= 1;

e1913:    b187 + b190 + b208 + b216 >= 1;

e1914:    b187 + b190 + b208 + b212 >= 1;

e1915:    b187 + b190 + b207 + b222 >= 1;

e1916:    b187 + b190 + b207 + b217 >= 1;

e1917:    b187 + b190 + b207 + b212 >= 1;

e1918:    b187 + b190 + b203 + b221 >= 1;

e1919:    b187 + b190 + b203 + b217 + b222 >= 1;

e1920:    b187 + b190 + b203 + b216 >= 1;

e1921:    b187 + b190 + b203 + b212 >= 1;

e1922:    b187 + b190 + b203 + b209 + b221 >= 1;

e1923:    b187 + b190 + b203 + b209 + b217 + b222 >= 1;

e1924:    b187 + b190 + b203 + b209 + b216 >= 1;

e1925:    b187 + b190 + b203 + b209 + b212 >= 1;

e1926:    b187 + b190 + b203 + b208 + b222 >= 1;

e1927:    b187 + b190 + b203 + b208 + b217 >= 1;

e1928:    b187 + b190 + b203 + b208 + b212 >= 1;

e1929:    b187 + b190 + b202 + b221 >= 1;

e1930:    b187 + b190 + b202 + b217 + b222 >= 1;

e1931:    b187 + b190 + b202 + b216 >= 1;

e1932:    b187 + b190 + b202 + b212 >= 1;

e1933:    b187 + b190 + b202 + b209 + b222 >= 1;

e1934:    b187 + b190 + b202 + b209 + b217 >= 1;

e1935:    b187 + b190 + b202 + b209 + b212 >= 1;

e1936:    b187 + b190 + b201 + b222 >= 1;

e1937:    b187 + b190 + b201 + b217 >= 1;

e1938:    b187 + b190 + b201 + b212 >= 1;

e1939:    b187 + b190 + b197 + b221 >= 1;

e1940:    b187 + b190 + b197 + b217 + b222 >= 1;

e1941:    b187 + b190 + b197 + b216 >= 1;

e1942:    b187 + b190 + b197 + b212 >= 1;

e1943:    b187 + b190 + b197 + b209 + b222 >= 1;

e1944:    b187 + b190 + b197 + b209 + b217 >= 1;

e1945:    b187 + b190 + b197 + b209 + b212 >= 1;

e1946:    b187 + b190 + b197 + b208 + b222 >= 1;

e1947:    b187 + b190 + b197 + b208 + b217 >= 1;

e1948:    b187 + b190 + b197 + b208 + b212 >= 1;

e1949:    b187 + b190 + b197 + b203 + b222 >= 1;

e1950:    b187 + b190 + b197 + b203 + b217 >= 1;

e1951:    b187 + b190 + b197 + b203 + b212 >= 1;

e1952:    b187 + b190 + b196 + b222 >= 1;

e1953:    b187 + b190 + b196 + b217 >= 1;

e1954:    b187 + b190 + b196 + b212 >= 1;

e1955:    b187 + b190 + b193 + b222 >= 1;

e1956:    b187 + b190 + b193 + b217 >= 1;

e1957:    b187 + b190 + b193 + b212 >= 1;

e1958:    b187 + b190 + b193 + b209 + b222 >= 1;

e1959:    b187 + b190 + b193 + b209 + b217 >= 1;

e1960:    b187 + b190 + b193 + b209 + b212 >= 1;

e1961:    b187 + b190 + b193 + b203 + b222 >= 1;

e1962:    b187 + b190 + b193 + b203 + b217 >= 1;

e1963:    b187 + b190 + b193 + b203 + b212 >= 1;

e1964:    b187 + b189 + b222 >= 1;

e1965:    b187 + b189 + b217 >= 1;

e1966:    b187 + b189 + b212 >= 1;

e1967:    b186 + b220 >= 1;

e1968:    b186 + b217 + b221 >= 1;

e1969:    b186 + b216 + b222 >= 1;

e1970:    b186 + b215 >= 1;

e1971:    b186 + b212 + b222 >= 1;

e1972:    b186 + b212 + b217 >= 1;

e1973:    b186 + b211 >= 1;

e1974:    b186 + b209 + b221 >= 1;

e1975:    b186 + b209 + b217 + b222 >= 1;

e1976:    b186 + b209 + b216 >= 1;

e1977:    b186 + b209 + b212 >= 1;

e1978:    b186 + b208 + b221 >= 1;

e1979:    b186 + b208 + b217 + b222 >= 1;

e1980:    b186 + b208 + b216 >= 1;

e1981:    b186 + b208 + b212 >= 1;

e1982:    b186 + b207 + b222 >= 1;

e1983:    b186 + b207 + b217 >= 1;

e1984:    b186 + b207 + b212 >= 1;

e1985:    b186 + b203 + b221 >= 1;

e1986:    b186 + b203 + b216 >= 1;

e1987:    b186 + b203 + b212 >= 1;

e1988:    b186 + b203 + b209 + b221 >= 1;

e1989:    b186 + b203 + b209 + b217 + b222 >= 1;

e1990:    b186 + b203 + b209 + b216 >= 1;

e1991:    b186 + b203 + b209 + b212 >= 1;

e1992:    b186 + b203 + b208 + b222 >= 1;

e1993:    b186 + b203 + b208 + b217 >= 1;

e1994:    b186 + b203 + b208 + b212 >= 1;

e1995:    b186 + b202 + b221 >= 1;

e1996:    b186 + b202 + b217 + b222 >= 1;

e1997:    b186 + b202 + b216 >= 1;

e1998:    b186 + b202 + b212 >= 1;

e1999:    b186 + b202 + b209 + b222 >= 1;

e2000:    b186 + b202 + b209 + b217 >= 1;

e2001:    b186 + b202 + b209 + b212 >= 1;

e2002:    b186 + b201 + b222 >= 1;

e2003:    b186 + b201 + b217 >= 1;

e2004:    b186 + b201 + b212 >= 1;

e2005:    b186 + b197 + b221 >= 1;

e2006:    b186 + b197 + b217 + b222 >= 1;

e2007:    b186 + b197 + b216 >= 1;

e2008:    b186 + b197 + b212 >= 1;

e2009:    b186 + b197 + b209 + b222 >= 1;

e2010:    b186 + b197 + b209 + b217 >= 1;

e2011:    b186 + b197 + b209 + b212 >= 1;

e2012:    b186 + b197 + b203 + b222 >= 1;

e2013:    b186 + b197 + b203 + b217 >= 1;

e2014:    b186 + b197 + b203 + b212 >= 1;

e2015:    b186 + b196 + b222 >= 1;

e2016:    b186 + b196 + b217 >= 1;

e2017:    b186 + b196 + b212 >= 1;

e2018:    b186 + b193 + b222 >= 1;

e2019:    b186 + b193 + b217 >= 1;

e2020:    b186 + b193 + b212 >= 1;

e2021:    b186 + b190 + b222 >= 1;

e2022:    b186 + b190 + b217 >= 1;

e2023:    b186 + b190 + b212 >= 1;

e2024:    b185 + b222 >= 1;

e2025:    b185 + b217 >= 1;

e2026:    b185 + b212 >= 1;

e2027:    x31 - 1.34666666666667*b185 >= 0;

e2028:    x31 - 1.92*b186 >= 0;

e2029:    x31 - 2.02*b187 >= 0;

e2030:    x32 - 2.67333333333333*b188 >= 0;

e2031:    x32 - 3.82*b189 >= 0;

e2032:    x32 - 4.01333333333333*b190 >= 0;

e2033:    x33 - 3.17333333333333*b191 >= 0;

e2034:    x33 - 4.53333333333333*b192 >= 0;

e2035:    x33 - 4.76*b193 >= 0;

e2036:    x34 - 3.97333333333333*b194 >= 0;

e2037:    x34 - 5.39333333333333*b195 >= 0;

e2038:    x34 - 5.68*b196 >= 0;

e2039:    x34 - 5.96*b197 >= 0;

e2040:    x35 - 26.7866666666667*b198 >= 0;

e2041:    x35 - 34.44*b199 >= 0;

e2042:    x35 - 36.3533333333333*b200 >= 0;

e2043:    x35 - 38.2666666666667*b201 >= 0;

e2044:    x35 - 40.18*b202 >= 0;

e2045:    x35 - 42.0933333333333*b203 >= 0;

e2046:    x36 - 63.18*b204 >= 0;

e2047:    x36 - 81.2333333333333*b205 >= 0;

e2048:    x36 - 85.7466666666667*b206 >= 0;

e2049:    x36 - 90.2533333333333*b207 >= 0;

e2050:    x36 - 94.7666666666667*b208 >= 0;

e2051:    x36 - 99.28*b209 >= 0;

e2052:    x37 - 4.39333333333333*b210 >= 0;

e2053:    x37 - 6.28*b211 >= 0;

e2054:    x37 - 6.59333333333333*b212 >= 0;

e2055:    x38 - 39.3733333333333*b213 >= 0;

e2056:    x38 - 53.4333333333333*b214 >= 0;

e2057:    x38 - 56.24*b215 >= 0;

e2058:    x38 - 59.0533333333333*b216 >= 0;

e2059:    x38 - 61.8666666666667*b217 >= 0;

e2060:    x39 - 35.82*b218 >= 0;

e2061:    x39 - 48.6133333333333*b219 >= 0;

e2062:    x39 - 51.1733333333333*b220 >= 0;

e2063:    x39 - 53.7333333333333*b221 >= 0;

e2064:    x39 - 56.2866666666667*b222 >= 0;

e2065:    x40 - 26.4066666666667*b223 >= 0;

e2066:    x40 - 33.9533333333333*b224 >= 0;

e2067:    x40 - 35.84*b225 >= 0;

e2068:    x40 - 37.7266666666667*b226 >= 0;

e2069:    x40 - 39.6133333333333*b227 >= 0;

e2070:    x40 - 41.5*b228 >= 0;

e2071:    x41 - 39.7666666666667*b229 >= 0;

e2072:    x41 - 53.9666666666667*b230 >= 0;

e2073:    x41 - 56.8066666666667*b231 >= 0;

e2074:    x41 - 59.6466666666667*b232 >= 0;

e2075:    x41 - 62.4933333333333*b233 >= 0;

e2076:    x42 - 53.94*b234 >= 0;

e2077:    x42 - 77.0533333333333*b235 >= 0;

e2078:    x42 - 80.9066666666667*b236 >= 0;

e2079:    x43 - 17.4333333333333*b237 >= 0;

e2080:    x43 - 24.9066666666667*b238 >= 0;

e2081:    x43 - 26.1466666666667*b239 >= 0;

e2082:    x44 - 25.3333333333333*b240 >= 0;

e2083:    x44 - 36.1866666666667*b241 >= 0;

e2084:    x44 - 38*b242 >= 0;

e2085:    x45 - 41.4933333333333*b243 >= 0;

e2086:    x45 - 56.3133333333333*b244 >= 0;

e2087:    x45 - 59.2733333333333*b245 >= 0;

e2088:    x45 - 62.24*b246 >= 0;

e2089:  - x76 + x155 <= 0;

e2090:  - x76 + x156 <= 0;

e2091:  - x77 + x157 <= 0;

e2092:  - x77 + x158 <= 0;

e2093:  - x78 + x159 <= 0;

e2094:  - x78 + x160 <= 0;

e2095:  - x79 + x161 <= 0;

e2096:  - x79 + x162 <= 0;

e2097:  - x80 + x163 <= 0;

e2098:  - x80 + x164 <= 0;

e2099:  - x81 + x165 <= 0;

e2100:  - x81 + x166 <= 0;

e2101:  - x82 + x167 <= 0;

e2102:  - x82 + x168 <= 0;

e2103:  - x83 + x169 <= 0;

e2104:  - x83 + x170 <= 0;

e2105:  - x84 + x171 <= 0;

e2106:  - x84 + x172 <= 0;

e2107:  - x85 + x173 <= 0;

e2108:  - x85 + x174 <= 0;

e2109:  - x86 + x175 <= 0;

e2110:  - x86 + x176 <= 0;

e2111:  - x87 + x177 <= 0;

e2112:  - x87 + x178 <= 0;

e2113:  - x88 + x179 <= 0;

e2114:  - x88 + x180 <= 0;

e2115:  - x89 + x181 <= 0;

e2116:  - x89 + x182 <= 0;

e2117:  - x90 + x183 <= 0;

e2118:  - x90 + x184 <= 0;

e2119:    b185 - b186 >= 0;

e2120:    b186 - b187 >= 0;

e2121:    b188 - b189 >= 0;

e2122:    b189 - b190 >= 0;

e2123:    b191 - b192 >= 0;

e2124:    b192 - b193 >= 0;

e2125:    b194 - b195 >= 0;

e2126:    b195 - b196 >= 0;

e2127:    b196 - b197 >= 0;

e2128:    b198 - b199 >= 0;

e2129:    b199 - b200 >= 0;

e2130:    b200 - b201 >= 0;

e2131:    b201 - b202 >= 0;

e2132:    b202 - b203 >= 0;

e2133:    b204 - b205 >= 0;

e2134:    b205 - b206 >= 0;

e2135:    b206 - b207 >= 0;

e2136:    b207 - b208 >= 0;

e2137:    b208 - b209 >= 0;

e2138:    b210 - b211 >= 0;

e2139:    b211 - b212 >= 0;

e2140:    b213 - b214 >= 0;

e2141:    b214 - b215 >= 0;

e2142:    b215 - b216 >= 0;

e2143:    b216 - b217 >= 0;

e2144:    b218 - b219 >= 0;

e2145:    b219 - b220 >= 0;

e2146:    b220 - b221 >= 0;

e2147:    b221 - b222 >= 0;

e2148:    b223 - b224 >= 0;

e2149:    b224 - b225 >= 0;

e2150:    b225 - b226 >= 0;

e2151:    b226 - b227 >= 0;

e2152:    b227 - b228 >= 0;

e2153:    b229 - b230 >= 0;

e2154:    b230 - b231 >= 0;

e2155:    b231 - b232 >= 0;

e2156:    b232 - b233 >= 0;

e2157:    b234 - b235 >= 0;

e2158:    b235 - b236 >= 0;

e2159:    b237 - b238 >= 0;

e2160:    b238 - b239 >= 0;

e2161:    b240 - b241 >= 0;

e2162:    b241 - b242 >= 0;

e2163:    b243 - b244 >= 0;

e2164:    b244 - b245 >= 0;

e2165:    b245 - b246 >= 0;

e2166:    x93 - x94 >= 0;