#  MIQCP written by GAMS Convert at 02/15/18 15:45:37
#  
#  Equation counts
#      Total        E        G        L        N        X        C        B
#       2467        1       18     2448        0        0        0        0
#  
#  Variable counts
#                   x        b        i      s1s      s2s       sc       si
#      Total     cont   binary  integer     sos1     sos2    scont     sint
#        154        1      153        0        0        0        0        0
#  FX      0        0        0        0        0        0        0        0
#  
#  Nonzero counts
#      Total    const       NL      DLL
#       7803     7497      306        0
# 
#  Reformulation has removed 1 variable and 1 equation


var b2 binary >= 0, <= 1;
var b3 binary >= 0, <= 1;
var b4 binary >= 0, <= 1;
var b5 binary >= 0, <= 1;
var b6 binary >= 0, <= 1;
var b7 binary >= 0, <= 1;
var b8 binary >= 0, <= 1;
var b9 binary >= 0, <= 1;
var b10 binary >= 0, <= 1;
var b11 binary >= 0, <= 1;
var b12 binary >= 0, <= 1;
var b13 binary >= 0, <= 1;
var b14 binary >= 0, <= 1;
var b15 binary >= 0, <= 1;
var b16 binary >= 0, <= 1;
var b17 binary >= 0, <= 1;
var b18 binary >= 0, <= 1;
var b19 binary >= 0, <= 1;
var b20 binary >= 0, <= 1;
var b21 binary >= 0, <= 1;
var b22 binary >= 0, <= 1;
var b23 binary >= 0, <= 1;
var b24 binary >= 0, <= 1;
var b25 binary >= 0, <= 1;
var b26 binary >= 0, <= 1;
var b27 binary >= 0, <= 1;
var b28 binary >= 0, <= 1;
var b29 binary >= 0, <= 1;
var b30 binary >= 0, <= 1;
var b31 binary >= 0, <= 1;
var b32 binary >= 0, <= 1;
var b33 binary >= 0, <= 1;
var b34 binary >= 0, <= 1;
var b35 binary >= 0, <= 1;
var b36 binary >= 0, <= 1;
var b37 binary >= 0, <= 1;
var b38 binary >= 0, <= 1;
var b39 binary >= 0, <= 1;
var b40 binary >= 0, <= 1;
var b41 binary >= 0, <= 1;
var b42 binary >= 0, <= 1;
var b43 binary >= 0, <= 1;
var b44 binary >= 0, <= 1;
var b45 binary >= 0, <= 1;
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 b76 binary >= 0, <= 1;
var b77 binary >= 0, <= 1;
var b78 binary >= 0, <= 1;
var b79 binary >= 0, <= 1;
var b80 binary >= 0, <= 1;
var b81 binary >= 0, <= 1;
var b82 binary >= 0, <= 1;
var b83 binary >= 0, <= 1;
var b84 binary >= 0, <= 1;
var b85 binary >= 0, <= 1;
var b86 binary >= 0, <= 1;
var b87 binary >= 0, <= 1;
var b88 binary >= 0, <= 1;
var b89 binary >= 0, <= 1;
var b90 binary >= 0, <= 1;
var b91 binary >= 0, <= 1;
var b92 binary >= 0, <= 1;
var b93 binary >= 0, <= 1;
var b94 binary >= 0, <= 1;
var b95 binary >= 0, <= 1;
var b96 binary >= 0, <= 1;
var b97 binary >= 0, <= 1;
var b98 binary >= 0, <= 1;
var b99 binary >= 0, <= 1;
var b100 binary >= 0, <= 1;
var b101 binary >= 0, <= 1;
var b102 binary >= 0, <= 1;
var b103 binary >= 0, <= 1;
var b104 binary >= 0, <= 1;
var b105 binary >= 0, <= 1;
var b106 binary >= 0, <= 1;
var b107 binary >= 0, <= 1;
var b108 binary >= 0, <= 1;
var b109 binary >= 0, <= 1;
var b110 binary >= 0, <= 1;
var b111 binary >= 0, <= 1;
var b112 binary >= 0, <= 1;
var b113 binary >= 0, <= 1;
var b114 binary >= 0, <= 1;
var b115 binary >= 0, <= 1;
var b116 binary >= 0, <= 1;
var b117 binary >= 0, <= 1;
var b118 binary >= 0, <= 1;
var b119 binary >= 0, <= 1;
var b120 binary >= 0, <= 1;
var b121 binary >= 0, <= 1;
var b122 binary >= 0, <= 1;
var b123 binary >= 0, <= 1;
var b124 binary >= 0, <= 1;
var b125 binary >= 0, <= 1;
var b126 binary >= 0, <= 1;
var b127 binary >= 0, <= 1;
var b128 binary >= 0, <= 1;
var b129 binary >= 0, <= 1;
var b130 binary >= 0, <= 1;
var b131 binary >= 0, <= 1;
var b132 binary >= 0, <= 1;
var b133 binary >= 0, <= 1;
var b134 binary >= 0, <= 1;
var b135 binary >= 0, <= 1;
var b136 binary >= 0, <= 1;
var b137 binary >= 0, <= 1;
var b138 binary >= 0, <= 1;
var b139 binary >= 0, <= 1;
var b140 binary >= 0, <= 1;
var b141 binary >= 0, <= 1;
var b142 binary >= 0, <= 1;
var b143 binary >= 0, <= 1;
var b144 binary >= 0, <= 1;
var b145 binary >= 0, <= 1;
var b146 binary >= 0, <= 1;
var b147 binary >= 0, <= 1;
var b148 binary >= 0, <= 1;
var b149 binary >= 0, <= 1;
var b150 binary >= 0, <= 1;
var b151 binary >= 0, <= 1;
var b152 binary >= 0, <= 1;
var b153 binary >= 0, <= 1;
var b154 binary >= 0, <= 1;

minimize obj:    940*b2 + 40300*b3 + 7750*b4 + 56550*b5 + 16790*b6 + 29000*b7
     + 54520*b8 + 26790*b9 + 61040*b10 + 13650*b11 + 158950*b12 + 77190*b13
     + 46110*b14 + 100480*b15 + 61250*b16 + 77440*b17 + 95230*b18 + 15210*b19
     + 63180*b20 + 9300*b21 + 400*b22 + 5800*b23 + 37620*b24 + 73260*b25
     + 14440*b26 + 570*b27 + 105300*b28 + 48410*b29 + 68250*b30 + 2490*b31
     + 73990*b32 + 23850*b33 + 92020*b34 + 14700*b35 + 44980*b36 + 60720*b37
     + 47850*b38 + 7540*b39 + 77760*b40 + 71550*b41 + 1650*b42 + 140000*b43
     + 146020*b44 + 20790*b45 + 7950*b46 + 9660*b47 + 126270*b48 + 15960*b49
     + 3780*b50 + 29610*b51 + 42940*b52 + 7860*b53 + 56610*b54 + 95760*b55
     + 42560*b56 + 101910*b57 + 57750*b58 + 12870*b59 + 8580*b60 + 3380*b61
     + 107160*b62 + 66120*b63 + 63800*b64 + 16800*b65 + 78300*b66 + 30260*b67
     + 39000*b68 + 2640*b69 + 71400*b70 + 12750*b71 + 55250*b72 + 94430*b73
     + 148410*b74 + 10790*b75 + 111870*b76 + 69760*b77 + 181390*b78 + 64600*b79
     + 52890*b80 + 73080*b81 + 42210*b82 + 45570*b83 + 9870*b84 + 122830*b85
     + 18480*b86 + 45050*b87 + 3500*b88 + 61110*b89 + 106720*b90 + 41470*b91
     + 30420*b92 + 26660*b93 + 16530*b94 + 63510*b95 + 27900*b96 + 10050*b97
     + 46610*b98 + 58110*b99 + 5190*b100 + 37430*b101 + 10320*b102 + 32560*b103
     + 15050*b104 + 46170*b105 + 35190*b106 + 138180*b107 + 40110*b108
     + 100080*b109 + 20580*b110 + 3220*b111 + 47850*b112 + 2970*b113
     + 33580*b114 + 560*b115 + 3400*b116 + 31620*b117 + 56420*b118 + 50050*b119
     + 46550*b120 + 420*b121 + 11880*b122 + 42210*b123 + 16650*b124
     + 153450*b125 + 49290*b126 + 59850*b127 + 10800*b128 + 69160*b129
     + 24300*b130 + 7040*b131 + 7920*b132 + 24220*b133 + 6040*b134 + 32490*b135
     + 111470*b136 + 29400*b137 + 2990*b138 + 22950*b139 + 22360*b140
     + 133510*b141 + 8250*b142 + 1200*b143 + 9720*b144 + 83790*b145
     + 54240*b146 + 28050*b147 + 62350*b148 + 1860*b149 + 38640*b150
     + 17550*b151 + 23730*b152 + 58200*b153;

subject to

e2:  - b2 + b3 - b19 <= 0;

e3:  - b2 + b4 - b154 <= 0;

e4:  - b2 + b5 - b20 <= 0;

e5:  - b2 + b6 - b21 <= 0;

e6:  - b2 + b7 - b22 <= 0;

e7:  - b2 + b8 - b23 <= 0;

e8:  - b2 + b9 - b24 <= 0;

e9:  - b2 + b10 - b25 <= 0;

e10:  - b2 + b11 - b26 <= 0;

e11:  - b2 + b12 - b27 <= 0;

e12:  - b2 + b13 - b28 <= 0;

e13:  - b2 + b14 - b29 <= 0;

e14:  - b2 + b15 - b30 <= 0;

e15:  - b2 + b16 - b31 <= 0;

e16:  - b2 + b17 - b32 <= 0;

e17:  - b2 + b18 - b33 <= 0;

e18:  - b3 + b4 - b34 <= 0;

e19:  - b3 + b5 - b35 <= 0;

e20:  - b3 + b6 - b36 <= 0;

e21:  - b3 + b7 - b37 <= 0;

e22:  - b3 + b8 - b38 <= 0;

e23:  - b3 + b9 - b39 <= 0;

e24:  - b3 + b10 - b40 <= 0;

e25:  - b3 + b11 - b41 <= 0;

e26:  - b3 + b12 - b42 <= 0;

e27:  - b3 + b13 - b43 <= 0;

e28:  - b3 + b14 - b44 <= 0;

e29:  - b3 + b15 - b45 <= 0;

e30:  - b3 + b16 - b46 <= 0;

e31:  - b3 + b17 - b47 <= 0;

e32:  - b3 + b18 - b48 <= 0;

e33:  - b4 + b5 - b49 <= 0;

e34:  - b4 + b6 - b50 <= 0;

e35:  - b4 + b7 - b51 <= 0;

e36:  - b4 + b8 - b52 <= 0;

e37:  - b4 + b9 - b53 <= 0;

e38:  - b4 + b10 - b54 <= 0;

e39:  - b4 + b11 - b55 <= 0;

e40:  - b4 + b12 - b56 <= 0;

e41:  - b4 + b13 - b57 <= 0;

e42:  - b4 + b14 - b58 <= 0;

e43:  - b4 + b15 - b59 <= 0;

e44:  - b4 + b16 - b60 <= 0;

e45:  - b4 + b17 - b61 <= 0;

e46:  - b4 + b18 - b62 <= 0;

e47:  - b5 + b6 - b63 <= 0;

e48:  - b5 + b7 - b64 <= 0;

e49:  - b5 + b8 - b65 <= 0;

e50:  - b5 + b9 - b66 <= 0;

e51:  - b5 + b10 - b67 <= 0;

e52:  - b5 + b11 - b68 <= 0;

e53:  - b5 + b12 - b69 <= 0;

e54:  - b5 + b13 - b70 <= 0;

e55:  - b5 + b14 - b71 <= 0;

e56:  - b5 + b15 - b72 <= 0;

e57:  - b5 + b16 - b73 <= 0;

e58:  - b5 + b17 - b74 <= 0;

e59:  - b5 + b18 - b75 <= 0;

e60:  - b6 + b7 - b76 <= 0;

e61:  - b6 + b8 - b77 <= 0;

e62:  - b6 + b9 - b78 <= 0;

e63:  - b6 + b10 - b79 <= 0;

e64:  - b6 + b11 - b80 <= 0;

e65:  - b6 + b12 - b81 <= 0;

e66:  - b6 + b13 - b82 <= 0;

e67:  - b6 + b14 - b83 <= 0;

e68:  - b6 + b15 - b84 <= 0;

e69:  - b6 + b16 - b85 <= 0;

e70:  - b6 + b17 - b86 <= 0;

e71:  - b6 + b18 - b87 <= 0;

e72:  - b7 + b8 - b88 <= 0;

e73:  - b7 + b9 - b89 <= 0;

e74:  - b7 + b10 - b90 <= 0;

e75:  - b7 + b11 - b91 <= 0;

e76:  - b7 + b12 - b92 <= 0;

e77:  - b7 + b13 - b93 <= 0;

e78:  - b7 + b14 - b94 <= 0;

e79:  - b7 + b15 - b95 <= 0;

e80:  - b7 + b16 - b96 <= 0;

e81:  - b7 + b17 - b97 <= 0;

e82:  - b7 + b18 - b98 <= 0;

e83:  - b8 + b9 - b99 <= 0;

e84:  - b8 + b10 - b100 <= 0;

e85:  - b8 + b11 - b101 <= 0;

e86:  - b8 + b12 - b102 <= 0;

e87:  - b8 + b13 - b103 <= 0;

e88:  - b8 + b14 - b104 <= 0;

e89:  - b8 + b15 - b105 <= 0;

e90:  - b8 + b16 - b106 <= 0;

e91:  - b8 + b17 - b107 <= 0;

e92:  - b8 + b18 - b108 <= 0;

e93:  - b9 + b10 - b109 <= 0;

e94:  - b9 + b11 - b110 <= 0;

e95:  - b9 + b12 - b111 <= 0;

e96:  - b9 + b13 - b112 <= 0;

e97:  - b9 + b14 - b113 <= 0;

e98:  - b9 + b15 - b114 <= 0;

e99:  - b9 + b16 - b115 <= 0;

e100:  - b9 + b17 - b116 <= 0;

e101:  - b9 + b18 - b117 <= 0;

e102:  - b10 + b11 - b118 <= 0;

e103:  - b10 + b12 - b119 <= 0;

e104:  - b10 + b13 - b120 <= 0;

e105:  - b10 + b14 - b121 <= 0;

e106:  - b10 + b15 - b122 <= 0;

e107:  - b10 + b16 - b123 <= 0;

e108:  - b10 + b17 - b124 <= 0;

e109:  - b10 + b18 - b125 <= 0;

e110:  - b11 + b12 - b126 <= 0;

e111:  - b11 + b13 - b127 <= 0;

e112:  - b11 + b14 - b128 <= 0;

e113:  - b11 + b15 - b129 <= 0;

e114:  - b11 + b16 - b130 <= 0;

e115:  - b11 + b17 - b131 <= 0;

e116:  - b11 + b18 - b132 <= 0;

e117:  - b12 + b13 - b133 <= 0;

e118:  - b12 + b14 - b134 <= 0;

e119:  - b12 + b15 - b135 <= 0;

e120:  - b12 + b16 - b136 <= 0;

e121:  - b12 + b17 - b137 <= 0;

e122:  - b12 + b18 - b138 <= 0;

e123:  - b13 + b14 - b139 <= 0;

e124:  - b13 + b15 - b140 <= 0;

e125:  - b13 + b16 - b141 <= 0;

e126:  - b13 + b17 - b142 <= 0;

e127:  - b13 + b18 - b143 <= 0;

e128:  - b14 + b15 - b144 <= 0;

e129:  - b14 + b16 - b145 <= 0;

e130:  - b14 + b17 - b146 <= 0;

e131:  - b14 + b18 - b147 <= 0;

e132:  - b15 + b16 - b148 <= 0;

e133:  - b15 + b17 - b149 <= 0;

e134:  - b15 + b18 - b150 <= 0;

e135:  - b16 + b17 - b151 <= 0;

e136:  - b16 + b18 - b152 <= 0;

e137:  - b17 + b18 - b153 <= 0;

e138:  - b19 - b34 + b154 <= 0;

e139:  - b19 + b20 - b35 <= 0;

e140:  - b19 + b21 - b36 <= 0;

e141:  - b19 + b22 - b37 <= 0;

e142:  - b19 + b23 - b38 <= 0;

e143:  - b19 + b24 - b39 <= 0;

e144:  - b19 + b25 - b40 <= 0;

e145:  - b19 + b26 - b41 <= 0;

e146:  - b19 + b27 - b42 <= 0;

e147:  - b19 + b28 - b43 <= 0;

e148:  - b19 + b29 - b44 <= 0;

e149:  - b19 + b30 - b45 <= 0;

e150:  - b19 + b31 - b46 <= 0;

e151:  - b19 + b32 - b47 <= 0;

e152:  - b19 + b33 - b48 <= 0;

e153:    b20 - b49 - b154 <= 0;

e154:    b21 - b50 - b154 <= 0;

e155:    b22 - b51 - b154 <= 0;

e156:    b23 - b52 - b154 <= 0;

e157:    b24 - b53 - b154 <= 0;

e158:    b25 - b54 - b154 <= 0;

e159:    b26 - b55 - b154 <= 0;

e160:    b27 - b56 - b154 <= 0;

e161:    b28 - b57 - b154 <= 0;

e162:    b29 - b58 - b154 <= 0;

e163:    b30 - b59 - b154 <= 0;

e164:    b31 - b60 - b154 <= 0;

e165:    b32 - b61 - b154 <= 0;

e166:    b33 - b62 - b154 <= 0;

e167:  - b20 + b21 - b63 <= 0;

e168:  - b20 + b22 - b64 <= 0;

e169:  - b20 + b23 - b65 <= 0;

e170:  - b20 + b24 - b66 <= 0;

e171:  - b20 + b25 - b67 <= 0;

e172:  - b20 + b26 - b68 <= 0;

e173:  - b20 + b27 - b69 <= 0;

e174:  - b20 + b28 - b70 <= 0;

e175:  - b20 + b29 - b71 <= 0;

e176:  - b20 + b30 - b72 <= 0;

e177:  - b20 + b31 - b73 <= 0;

e178:  - b20 + b32 - b74 <= 0;

e179:  - b20 + b33 - b75 <= 0;

e180:  - b21 + b22 - b76 <= 0;

e181:  - b21 + b23 - b77 <= 0;

e182:  - b21 + b24 - b78 <= 0;

e183:  - b21 + b25 - b79 <= 0;

e184:  - b21 + b26 - b80 <= 0;

e185:  - b21 + b27 - b81 <= 0;

e186:  - b21 + b28 - b82 <= 0;

e187:  - b21 + b29 - b83 <= 0;

e188:  - b21 + b30 - b84 <= 0;

e189:  - b21 + b31 - b85 <= 0;

e190:  - b21 + b32 - b86 <= 0;

e191:  - b21 + b33 - b87 <= 0;

e192:  - b22 + b23 - b88 <= 0;

e193:  - b22 + b24 - b89 <= 0;

e194:  - b22 + b25 - b90 <= 0;

e195:  - b22 + b26 - b91 <= 0;

e196:  - b22 + b27 - b92 <= 0;

e197:  - b22 + b28 - b93 <= 0;

e198:  - b22 + b29 - b94 <= 0;

e199:  - b22 + b30 - b95 <= 0;

e200:  - b22 + b31 - b96 <= 0;

e201:  - b22 + b32 - b97 <= 0;

e202:  - b22 + b33 - b98 <= 0;

e203:  - b23 + b24 - b99 <= 0;

e204:  - b23 + b25 - b100 <= 0;

e205:  - b23 + b26 - b101 <= 0;

e206:  - b23 + b27 - b102 <= 0;

e207:  - b23 + b28 - b103 <= 0;

e208:  - b23 + b29 - b104 <= 0;

e209:  - b23 + b30 - b105 <= 0;

e210:  - b23 + b31 - b106 <= 0;

e211:  - b23 + b32 - b107 <= 0;

e212:  - b23 + b33 - b108 <= 0;

e213:  - b24 + b25 - b109 <= 0;

e214:  - b24 + b26 - b110 <= 0;

e215:  - b24 + b27 - b111 <= 0;

e216:  - b24 + b28 - b112 <= 0;

e217:  - b24 + b29 - b113 <= 0;

e218:  - b24 + b30 - b114 <= 0;

e219:  - b24 + b31 - b115 <= 0;

e220:  - b24 + b32 - b116 <= 0;

e221:  - b24 + b33 - b117 <= 0;

e222:  - b25 + b26 - b118 <= 0;

e223:  - b25 + b27 - b119 <= 0;

e224:  - b25 + b28 - b120 <= 0;

e225:  - b25 + b29 - b121 <= 0;

e226:  - b25 + b30 - b122 <= 0;

e227:  - b25 + b31 - b123 <= 0;

e228:  - b25 + b32 - b124 <= 0;

e229:  - b25 + b33 - b125 <= 0;

e230:  - b26 + b27 - b126 <= 0;

e231:  - b26 + b28 - b127 <= 0;

e232:  - b26 + b29 - b128 <= 0;

e233:  - b26 + b30 - b129 <= 0;

e234:  - b26 + b31 - b130 <= 0;

e235:  - b26 + b32 - b131 <= 0;

e236:  - b26 + b33 - b132 <= 0;

e237:  - b27 + b28 - b133 <= 0;

e238:  - b27 + b29 - b134 <= 0;

e239:  - b27 + b30 - b135 <= 0;

e240:  - b27 + b31 - b136 <= 0;

e241:  - b27 + b32 - b137 <= 0;

e242:  - b27 + b33 - b138 <= 0;

e243:  - b28 + b29 - b139 <= 0;

e244:  - b28 + b30 - b140 <= 0;

e245:  - b28 + b31 - b141 <= 0;

e246:  - b28 + b32 - b142 <= 0;

e247:  - b28 + b33 - b143 <= 0;

e248:  - b29 + b30 - b144 <= 0;

e249:  - b29 + b31 - b145 <= 0;

e250:  - b29 + b32 - b146 <= 0;

e251:  - b29 + b33 - b147 <= 0;

e252:  - b30 + b31 - b148 <= 0;

e253:  - b30 + b32 - b149 <= 0;

e254:  - b30 + b33 - b150 <= 0;

e255:  - b31 + b32 - b151 <= 0;

e256:  - b31 + b33 - b152 <= 0;

e257:  - b32 + b33 - b153 <= 0;

e258:  - b34 + b35 - b49 <= 0;

e259:  - b34 + b36 - b50 <= 0;

e260:  - b34 + b37 - b51 <= 0;

e261:  - b34 + b38 - b52 <= 0;

e262:  - b34 + b39 - b53 <= 0;

e263:  - b34 + b40 - b54 <= 0;

e264:  - b34 + b41 - b55 <= 0;

e265:  - b34 + b42 - b56 <= 0;

e266:  - b34 + b43 - b57 <= 0;

e267:  - b34 + b44 - b58 <= 0;

e268:  - b34 + b45 - b59 <= 0;

e269:  - b34 + b46 - b60 <= 0;

e270:  - b34 + b47 - b61 <= 0;

e271:  - b34 + b48 - b62 <= 0;

e272:  - b35 + b36 - b63 <= 0;

e273:  - b35 + b37 - b64 <= 0;

e274:  - b35 + b38 - b65 <= 0;

e275:  - b35 + b39 - b66 <= 0;

e276:  - b35 + b40 - b67 <= 0;

e277:  - b35 + b41 - b68 <= 0;

e278:  - b35 + b42 - b69 <= 0;

e279:  - b35 + b43 - b70 <= 0;

e280:  - b35 + b44 - b71 <= 0;

e281:  - b35 + b45 - b72 <= 0;

e282:  - b35 + b46 - b73 <= 0;

e283:  - b35 + b47 - b74 <= 0;

e284:  - b35 + b48 - b75 <= 0;

e285:  - b36 + b37 - b76 <= 0;

e286:  - b36 + b38 - b77 <= 0;

e287:  - b36 + b39 - b78 <= 0;

e288:  - b36 + b40 - b79 <= 0;

e289:  - b36 + b41 - b80 <= 0;

e290:  - b36 + b42 - b81 <= 0;

e291:  - b36 + b43 - b82 <= 0;

e292:  - b36 + b44 - b83 <= 0;

e293:  - b36 + b45 - b84 <= 0;

e294:  - b36 + b46 - b85 <= 0;

e295:  - b36 + b47 - b86 <= 0;

e296:  - b36 + b48 - b87 <= 0;

e297:  - b37 + b38 - b88 <= 0;

e298:  - b37 + b39 - b89 <= 0;

e299:  - b37 + b40 - b90 <= 0;

e300:  - b37 + b41 - b91 <= 0;

e301:  - b37 + b42 - b92 <= 0;

e302:  - b37 + b43 - b93 <= 0;

e303:  - b37 + b44 - b94 <= 0;

e304:  - b37 + b45 - b95 <= 0;

e305:  - b37 + b46 - b96 <= 0;

e306:  - b37 + b47 - b97 <= 0;

e307:  - b37 + b48 - b98 <= 0;

e308:  - b38 + b39 - b99 <= 0;

e309:  - b38 + b40 - b100 <= 0;

e310:  - b38 + b41 - b101 <= 0;

e311:  - b38 + b42 - b102 <= 0;

e312:  - b38 + b43 - b103 <= 0;

e313:  - b38 + b44 - b104 <= 0;

e314:  - b38 + b45 - b105 <= 0;

e315:  - b38 + b46 - b106 <= 0;

e316:  - b38 + b47 - b107 <= 0;

e317:  - b38 + b48 - b108 <= 0;

e318:  - b39 + b40 - b109 <= 0;

e319:  - b39 + b41 - b110 <= 0;

e320:  - b39 + b42 - b111 <= 0;

e321:  - b39 + b43 - b112 <= 0;

e322:  - b39 + b44 - b113 <= 0;

e323:  - b39 + b45 - b114 <= 0;

e324:  - b39 + b46 - b115 <= 0;

e325:  - b39 + b47 - b116 <= 0;

e326:  - b39 + b48 - b117 <= 0;

e327:  - b40 + b41 - b118 <= 0;

e328:  - b40 + b42 - b119 <= 0;

e329:  - b40 + b43 - b120 <= 0;

e330:  - b40 + b44 - b121 <= 0;

e331:  - b40 + b45 - b122 <= 0;

e332:  - b40 + b46 - b123 <= 0;

e333:  - b40 + b47 - b124 <= 0;

e334:  - b40 + b48 - b125 <= 0;

e335:  - b41 + b42 - b126 <= 0;

e336:  - b41 + b43 - b127 <= 0;

e337:  - b41 + b44 - b128 <= 0;

e338:  - b41 + b45 - b129 <= 0;

e339:  - b41 + b46 - b130 <= 0;

e340:  - b41 + b47 - b131 <= 0;

e341:  - b41 + b48 - b132 <= 0;

e342:  - b42 + b43 - b133 <= 0;

e343:  - b42 + b44 - b134 <= 0;

e344:  - b42 + b45 - b135 <= 0;

e345:  - b42 + b46 - b136 <= 0;

e346:  - b42 + b47 - b137 <= 0;

e347:  - b42 + b48 - b138 <= 0;

e348:  - b43 + b44 - b139 <= 0;

e349:  - b43 + b45 - b140 <= 0;

e350:  - b43 + b46 - b141 <= 0;

e351:  - b43 + b47 - b142 <= 0;

e352:  - b43 + b48 - b143 <= 0;

e353:  - b44 + b45 - b144 <= 0;

e354:  - b44 + b46 - b145 <= 0;

e355:  - b44 + b47 - b146 <= 0;

e356:  - b44 + b48 - b147 <= 0;

e357:  - b45 + b46 - b148 <= 0;

e358:  - b45 + b47 - b149 <= 0;

e359:  - b45 + b48 - b150 <= 0;

e360:  - b46 + b47 - b151 <= 0;

e361:  - b46 + b48 - b152 <= 0;

e362:  - b47 + b48 - b153 <= 0;

e363:  - b49 + b50 - b63 <= 0;

e364:  - b49 + b51 - b64 <= 0;

e365:  - b49 + b52 - b65 <= 0;

e366:  - b49 + b53 - b66 <= 0;

e367:  - b49 + b54 - b67 <= 0;

e368:  - b49 + b55 - b68 <= 0;

e369:  - b49 + b56 - b69 <= 0;

e370:  - b49 + b57 - b70 <= 0;

e371:  - b49 + b58 - b71 <= 0;

e372:  - b49 + b59 - b72 <= 0;

e373:  - b49 + b60 - b73 <= 0;

e374:  - b49 + b61 - b74 <= 0;

e375:  - b49 + b62 - b75 <= 0;

e376:  - b50 + b51 - b76 <= 0;

e377:  - b50 + b52 - b77 <= 0;

e378:  - b50 + b53 - b78 <= 0;

e379:  - b50 + b54 - b79 <= 0;

e380:  - b50 + b55 - b80 <= 0;

e381:  - b50 + b56 - b81 <= 0;

e382:  - b50 + b57 - b82 <= 0;

e383:  - b50 + b58 - b83 <= 0;

e384:  - b50 + b59 - b84 <= 0;

e385:  - b50 + b60 - b85 <= 0;

e386:  - b50 + b61 - b86 <= 0;

e387:  - b50 + b62 - b87 <= 0;

e388:  - b51 + b52 - b88 <= 0;

e389:  - b51 + b53 - b89 <= 0;

e390:  - b51 + b54 - b90 <= 0;

e391:  - b51 + b55 - b91 <= 0;

e392:  - b51 + b56 - b92 <= 0;

e393:  - b51 + b57 - b93 <= 0;

e394:  - b51 + b58 - b94 <= 0;

e395:  - b51 + b59 - b95 <= 0;

e396:  - b51 + b60 - b96 <= 0;

e397:  - b51 + b61 - b97 <= 0;

e398:  - b51 + b62 - b98 <= 0;

e399:  - b52 + b53 - b99 <= 0;

e400:  - b52 + b54 - b100 <= 0;

e401:  - b52 + b55 - b101 <= 0;

e402:  - b52 + b56 - b102 <= 0;

e403:  - b52 + b57 - b103 <= 0;

e404:  - b52 + b58 - b104 <= 0;

e405:  - b52 + b59 - b105 <= 0;

e406:  - b52 + b60 - b106 <= 0;

e407:  - b52 + b61 - b107 <= 0;

e408:  - b52 + b62 - b108 <= 0;

e409:  - b53 + b54 - b109 <= 0;

e410:  - b53 + b55 - b110 <= 0;

e411:  - b53 + b56 - b111 <= 0;

e412:  - b53 + b57 - b112 <= 0;

e413:  - b53 + b58 - b113 <= 0;

e414:  - b53 + b59 - b114 <= 0;

e415:  - b53 + b60 - b115 <= 0;

e416:  - b53 + b61 - b116 <= 0;

e417:  - b53 + b62 - b117 <= 0;

e418:  - b54 + b55 - b118 <= 0;

e419:  - b54 + b56 - b119 <= 0;

e420:  - b54 + b57 - b120 <= 0;

e421:  - b54 + b58 - b121 <= 0;

e422:  - b54 + b59 - b122 <= 0;

e423:  - b54 + b60 - b123 <= 0;

e424:  - b54 + b61 - b124 <= 0;

e425:  - b54 + b62 - b125 <= 0;

e426:  - b55 + b56 - b126 <= 0;

e427:  - b55 + b57 - b127 <= 0;

e428:  - b55 + b58 - b128 <= 0;

e429:  - b55 + b59 - b129 <= 0;

e430:  - b55 + b60 - b130 <= 0;

e431:  - b55 + b61 - b131 <= 0;

e432:  - b55 + b62 - b132 <= 0;

e433:  - b56 + b57 - b133 <= 0;

e434:  - b56 + b58 - b134 <= 0;

e435:  - b56 + b59 - b135 <= 0;

e436:  - b56 + b60 - b136 <= 0;

e437:  - b56 + b61 - b137 <= 0;

e438:  - b56 + b62 - b138 <= 0;

e439:  - b57 + b58 - b139 <= 0;

e440:  - b57 + b59 - b140 <= 0;

e441:  - b57 + b60 - b141 <= 0;

e442:  - b57 + b61 - b142 <= 0;

e443:  - b57 + b62 - b143 <= 0;

e444:  - b58 + b59 - b144 <= 0;

e445:  - b58 + b60 - b145 <= 0;

e446:  - b58 + b61 - b146 <= 0;

e447:  - b58 + b62 - b147 <= 0;

e448:  - b59 + b60 - b148 <= 0;

e449:  - b59 + b61 - b149 <= 0;

e450:  - b59 + b62 - b150 <= 0;

e451:  - b60 + b61 - b151 <= 0;

e452:  - b60 + b62 - b152 <= 0;

e453:  - b61 + b62 - b153 <= 0;

e454:  - b63 + b64 - b76 <= 0;

e455:  - b63 + b65 - b77 <= 0;

e456:  - b63 + b66 - b78 <= 0;

e457:  - b63 + b67 - b79 <= 0;

e458:  - b63 + b68 - b80 <= 0;

e459:  - b63 + b69 - b81 <= 0;

e460:  - b63 + b70 - b82 <= 0;

e461:  - b63 + b71 - b83 <= 0;

e462:  - b63 + b72 - b84 <= 0;

e463:  - b63 + b73 - b85 <= 0;

e464:  - b63 + b74 - b86 <= 0;

e465:  - b63 + b75 - b87 <= 0;

e466:  - b64 + b65 - b88 <= 0;

e467:  - b64 + b66 - b89 <= 0;

e468:  - b64 + b67 - b90 <= 0;

e469:  - b64 + b68 - b91 <= 0;

e470:  - b64 + b69 - b92 <= 0;

e471:  - b64 + b70 - b93 <= 0;

e472:  - b64 + b71 - b94 <= 0;

e473:  - b64 + b72 - b95 <= 0;

e474:  - b64 + b73 - b96 <= 0;

e475:  - b64 + b74 - b97 <= 0;

e476:  - b64 + b75 - b98 <= 0;

e477:  - b65 + b66 - b99 <= 0;

e478:  - b65 + b67 - b100 <= 0;

e479:  - b65 + b68 - b101 <= 0;

e480:  - b65 + b69 - b102 <= 0;

e481:  - b65 + b70 - b103 <= 0;

e482:  - b65 + b71 - b104 <= 0;

e483:  - b65 + b72 - b105 <= 0;

e484:  - b65 + b73 - b106 <= 0;

e485:  - b65 + b74 - b107 <= 0;

e486:  - b65 + b75 - b108 <= 0;

e487:  - b66 + b67 - b109 <= 0;

e488:  - b66 + b68 - b110 <= 0;

e489:  - b66 + b69 - b111 <= 0;

e490:  - b66 + b70 - b112 <= 0;

e491:  - b66 + b71 - b113 <= 0;

e492:  - b66 + b72 - b114 <= 0;

e493:  - b66 + b73 - b115 <= 0;

e494:  - b66 + b74 - b116 <= 0;

e495:  - b66 + b75 - b117 <= 0;

e496:  - b67 + b68 - b118 <= 0;

e497:  - b67 + b69 - b119 <= 0;

e498:  - b67 + b70 - b120 <= 0;

e499:  - b67 + b71 - b121 <= 0;

e500:  - b67 + b72 - b122 <= 0;

e501:  - b67 + b73 - b123 <= 0;

e502:  - b67 + b74 - b124 <= 0;

e503:  - b67 + b75 - b125 <= 0;

e504:  - b68 + b69 - b126 <= 0;

e505:  - b68 + b70 - b127 <= 0;

e506:  - b68 + b71 - b128 <= 0;

e507:  - b68 + b72 - b129 <= 0;

e508:  - b68 + b73 - b130 <= 0;

e509:  - b68 + b74 - b131 <= 0;

e510:  - b68 + b75 - b132 <= 0;

e511:  - b69 + b70 - b133 <= 0;

e512:  - b69 + b71 - b134 <= 0;

e513:  - b69 + b72 - b135 <= 0;

e514:  - b69 + b73 - b136 <= 0;

e515:  - b69 + b74 - b137 <= 0;

e516:  - b69 + b75 - b138 <= 0;

e517:  - b70 + b71 - b139 <= 0;

e518:  - b70 + b72 - b140 <= 0;

e519:  - b70 + b73 - b141 <= 0;

e520:  - b70 + b74 - b142 <= 0;

e521:  - b70 + b75 - b143 <= 0;

e522:  - b71 + b72 - b144 <= 0;

e523:  - b71 + b73 - b145 <= 0;

e524:  - b71 + b74 - b146 <= 0;

e525:  - b71 + b75 - b147 <= 0;

e526:  - b72 + b73 - b148 <= 0;

e527:  - b72 + b74 - b149 <= 0;

e528:  - b72 + b75 - b150 <= 0;

e529:  - b73 + b74 - b151 <= 0;

e530:  - b73 + b75 - b152 <= 0;

e531:  - b74 + b75 - b153 <= 0;

e532:  - b76 + b77 - b88 <= 0;

e533:  - b76 + b78 - b89 <= 0;

e534:  - b76 + b79 - b90 <= 0;

e535:  - b76 + b80 - b91 <= 0;

e536:  - b76 + b81 - b92 <= 0;

e537:  - b76 + b82 - b93 <= 0;

e538:  - b76 + b83 - b94 <= 0;

e539:  - b76 + b84 - b95 <= 0;

e540:  - b76 + b85 - b96 <= 0;

e541:  - b76 + b86 - b97 <= 0;

e542:  - b76 + b87 - b98 <= 0;

e543:  - b77 + b78 - b99 <= 0;

e544:  - b77 + b79 - b100 <= 0;

e545:  - b77 + b80 - b101 <= 0;

e546:  - b77 + b81 - b102 <= 0;

e547:  - b77 + b82 - b103 <= 0;

e548:  - b77 + b83 - b104 <= 0;

e549:  - b77 + b84 - b105 <= 0;

e550:  - b77 + b85 - b106 <= 0;

e551:  - b77 + b86 - b107 <= 0;

e552:  - b77 + b87 - b108 <= 0;

e553:  - b78 + b79 - b109 <= 0;

e554:  - b78 + b80 - b110 <= 0;

e555:  - b78 + b81 - b111 <= 0;

e556:  - b78 + b82 - b112 <= 0;

e557:  - b78 + b83 - b113 <= 0;

e558:  - b78 + b84 - b114 <= 0;

e559:  - b78 + b85 - b115 <= 0;

e560:  - b78 + b86 - b116 <= 0;

e561:  - b78 + b87 - b117 <= 0;

e562:  - b79 + b80 - b118 <= 0;

e563:  - b79 + b81 - b119 <= 0;

e564:  - b79 + b82 - b120 <= 0;

e565:  - b79 + b83 - b121 <= 0;

e566:  - b79 + b84 - b122 <= 0;

e567:  - b79 + b85 - b123 <= 0;

e568:  - b79 + b86 - b124 <= 0;

e569:  - b79 + b87 - b125 <= 0;

e570:  - b80 + b81 - b126 <= 0;

e571:  - b80 + b82 - b127 <= 0;

e572:  - b80 + b83 - b128 <= 0;

e573:  - b80 + b84 - b129 <= 0;

e574:  - b80 + b85 - b130 <= 0;

e575:  - b80 + b86 - b131 <= 0;

e576:  - b80 + b87 - b132 <= 0;

e577:  - b81 + b82 - b133 <= 0;

e578:  - b81 + b83 - b134 <= 0;

e579:  - b81 + b84 - b135 <= 0;

e580:  - b81 + b85 - b136 <= 0;

e581:  - b81 + b86 - b137 <= 0;

e582:  - b81 + b87 - b138 <= 0;

e583:  - b82 + b83 - b139 <= 0;

e584:  - b82 + b84 - b140 <= 0;

e585:  - b82 + b85 - b141 <= 0;

e586:  - b82 + b86 - b142 <= 0;

e587:  - b82 + b87 - b143 <= 0;

e588:  - b83 + b84 - b144 <= 0;

e589:  - b83 + b85 - b145 <= 0;

e590:  - b83 + b86 - b146 <= 0;

e591:  - b83 + b87 - b147 <= 0;

e592:  - b84 + b85 - b148 <= 0;

e593:  - b84 + b86 - b149 <= 0;

e594:  - b84 + b87 - b150 <= 0;

e595:  - b85 + b86 - b151 <= 0;

e596:  - b85 + b87 - b152 <= 0;

e597:  - b86 + b87 - b153 <= 0;

e598:  - b88 + b89 - b99 <= 0;

e599:  - b88 + b90 - b100 <= 0;

e600:  - b88 + b91 - b101 <= 0;

e601:  - b88 + b92 - b102 <= 0;

e602:  - b88 + b93 - b103 <= 0;

e603:  - b88 + b94 - b104 <= 0;

e604:  - b88 + b95 - b105 <= 0;

e605:  - b88 + b96 - b106 <= 0;

e606:  - b88 + b97 - b107 <= 0;

e607:  - b88 + b98 - b108 <= 0;

e608:  - b89 + b90 - b109 <= 0;

e609:  - b89 + b91 - b110 <= 0;

e610:  - b89 + b92 - b111 <= 0;

e611:  - b89 + b93 - b112 <= 0;

e612:  - b89 + b94 - b113 <= 0;

e613:  - b89 + b95 - b114 <= 0;

e614:  - b89 + b96 - b115 <= 0;

e615:  - b89 + b97 - b116 <= 0;

e616:  - b89 + b98 - b117 <= 0;

e617:  - b90 + b91 - b118 <= 0;

e618:  - b90 + b92 - b119 <= 0;

e619:  - b90 + b93 - b120 <= 0;

e620:  - b90 + b94 - b121 <= 0;

e621:  - b90 + b95 - b122 <= 0;

e622:  - b90 + b96 - b123 <= 0;

e623:  - b90 + b97 - b124 <= 0;

e624:  - b90 + b98 - b125 <= 0;

e625:  - b91 + b92 - b126 <= 0;

e626:  - b91 + b93 - b127 <= 0;

e627:  - b91 + b94 - b128 <= 0;

e628:  - b91 + b95 - b129 <= 0;

e629:  - b91 + b96 - b130 <= 0;

e630:  - b91 + b97 - b131 <= 0;

e631:  - b91 + b98 - b132 <= 0;

e632:  - b92 + b93 - b133 <= 0;

e633:  - b92 + b94 - b134 <= 0;

e634:  - b92 + b95 - b135 <= 0;

e635:  - b92 + b96 - b136 <= 0;

e636:  - b92 + b97 - b137 <= 0;

e637:  - b92 + b98 - b138 <= 0;

e638:  - b93 + b94 - b139 <= 0;

e639:  - b93 + b95 - b140 <= 0;

e640:  - b93 + b96 - b141 <= 0;

e641:  - b93 + b97 - b142 <= 0;

e642:  - b93 + b98 - b143 <= 0;

e643:  - b94 + b95 - b144 <= 0;

e644:  - b94 + b96 - b145 <= 0;

e645:  - b94 + b97 - b146 <= 0;

e646:  - b94 + b98 - b147 <= 0;

e647:  - b95 + b96 - b148 <= 0;

e648:  - b95 + b97 - b149 <= 0;

e649:  - b95 + b98 - b150 <= 0;

e650:  - b96 + b97 - b151 <= 0;

e651:  - b96 + b98 - b152 <= 0;

e652:  - b97 + b98 - b153 <= 0;

e653:  - b99 + b100 - b109 <= 0;

e654:  - b99 + b101 - b110 <= 0;

e655:  - b99 + b102 - b111 <= 0;

e656:  - b99 + b103 - b112 <= 0;

e657:  - b99 + b104 - b113 <= 0;

e658:  - b99 + b105 - b114 <= 0;

e659:  - b99 + b106 - b115 <= 0;

e660:  - b99 + b107 - b116 <= 0;

e661:  - b99 + b108 - b117 <= 0;

e662:  - b100 + b101 - b118 <= 0;

e663:  - b100 + b102 - b119 <= 0;

e664:  - b100 + b103 - b120 <= 0;

e665:  - b100 + b104 - b121 <= 0;

e666:  - b100 + b105 - b122 <= 0;

e667:  - b100 + b106 - b123 <= 0;

e668:  - b100 + b107 - b124 <= 0;

e669:  - b100 + b108 - b125 <= 0;

e670:  - b101 + b102 - b126 <= 0;

e671:  - b101 + b103 - b127 <= 0;

e672:  - b101 + b104 - b128 <= 0;

e673:  - b101 + b105 - b129 <= 0;

e674:  - b101 + b106 - b130 <= 0;

e675:  - b101 + b107 - b131 <= 0;

e676:  - b101 + b108 - b132 <= 0;

e677:  - b102 + b103 - b133 <= 0;

e678:  - b102 + b104 - b134 <= 0;

e679:  - b102 + b105 - b135 <= 0;

e680:  - b102 + b106 - b136 <= 0;

e681:  - b102 + b107 - b137 <= 0;

e682:  - b102 + b108 - b138 <= 0;

e683:  - b103 + b104 - b139 <= 0;

e684:  - b103 + b105 - b140 <= 0;

e685:  - b103 + b106 - b141 <= 0;

e686:  - b103 + b107 - b142 <= 0;

e687:  - b103 + b108 - b143 <= 0;

e688:  - b104 + b105 - b144 <= 0;

e689:  - b104 + b106 - b145 <= 0;

e690:  - b104 + b107 - b146 <= 0;

e691:  - b104 + b108 - b147 <= 0;

e692:  - b105 + b106 - b148 <= 0;

e693:  - b105 + b107 - b149 <= 0;

e694:  - b105 + b108 - b150 <= 0;

e695:  - b106 + b107 - b151 <= 0;

e696:  - b106 + b108 - b152 <= 0;

e697:  - b107 + b108 - b153 <= 0;

e698:  - b109 + b110 - b118 <= 0;

e699:  - b109 + b111 - b119 <= 0;

e700:  - b109 + b112 - b120 <= 0;

e701:  - b109 + b113 - b121 <= 0;

e702:  - b109 + b114 - b122 <= 0;

e703:  - b109 + b115 - b123 <= 0;

e704:  - b109 + b116 - b124 <= 0;

e705:  - b109 + b117 - b125 <= 0;

e706:  - b110 + b111 - b126 <= 0;

e707:  - b110 + b112 - b127 <= 0;

e708:  - b110 + b113 - b128 <= 0;

e709:  - b110 + b114 - b129 <= 0;

e710:  - b110 + b115 - b130 <= 0;

e711:  - b110 + b116 - b131 <= 0;

e712:  - b110 + b117 - b132 <= 0;

e713:  - b111 + b112 - b133 <= 0;

e714:  - b111 + b113 - b134 <= 0;

e715:  - b111 + b114 - b135 <= 0;

e716:  - b111 + b115 - b136 <= 0;

e717:  - b111 + b116 - b137 <= 0;

e718:  - b111 + b117 - b138 <= 0;

e719:  - b112 + b113 - b139 <= 0;

e720:  - b112 + b114 - b140 <= 0;

e721:  - b112 + b115 - b141 <= 0;

e722:  - b112 + b116 - b142 <= 0;

e723:  - b112 + b117 - b143 <= 0;

e724:  - b113 + b114 - b144 <= 0;

e725:  - b113 + b115 - b145 <= 0;

e726:  - b113 + b116 - b146 <= 0;

e727:  - b113 + b117 - b147 <= 0;

e728:  - b114 + b115 - b148 <= 0;

e729:  - b114 + b116 - b149 <= 0;

e730:  - b114 + b117 - b150 <= 0;

e731:  - b115 + b116 - b151 <= 0;

e732:  - b115 + b117 - b152 <= 0;

e733:  - b116 + b117 - b153 <= 0;

e734:  - b118 + b119 - b126 <= 0;

e735:  - b118 + b120 - b127 <= 0;

e736:  - b118 + b121 - b128 <= 0;

e737:  - b118 + b122 - b129 <= 0;

e738:  - b118 + b123 - b130 <= 0;

e739:  - b118 + b124 - b131 <= 0;

e740:  - b118 + b125 - b132 <= 0;

e741:  - b119 + b120 - b133 <= 0;

e742:  - b119 + b121 - b134 <= 0;

e743:  - b119 + b122 - b135 <= 0;

e744:  - b119 + b123 - b136 <= 0;

e745:  - b119 + b124 - b137 <= 0;

e746:  - b119 + b125 - b138 <= 0;

e747:  - b120 + b121 - b139 <= 0;

e748:  - b120 + b122 - b140 <= 0;

e749:  - b120 + b123 - b141 <= 0;

e750:  - b120 + b124 - b142 <= 0;

e751:  - b120 + b125 - b143 <= 0;

e752:  - b121 + b122 - b144 <= 0;

e753:  - b121 + b123 - b145 <= 0;

e754:  - b121 + b124 - b146 <= 0;

e755:  - b121 + b125 - b147 <= 0;

e756:  - b122 + b123 - b148 <= 0;

e757:  - b122 + b124 - b149 <= 0;

e758:  - b122 + b125 - b150 <= 0;

e759:  - b123 + b124 - b151 <= 0;

e760:  - b123 + b125 - b152 <= 0;

e761:  - b124 + b125 - b153 <= 0;

e762:  - b126 + b127 - b133 <= 0;

e763:  - b126 + b128 - b134 <= 0;

e764:  - b126 + b129 - b135 <= 0;

e765:  - b126 + b130 - b136 <= 0;

e766:  - b126 + b131 - b137 <= 0;

e767:  - b126 + b132 - b138 <= 0;

e768:  - b127 + b128 - b139 <= 0;

e769:  - b127 + b129 - b140 <= 0;

e770:  - b127 + b130 - b141 <= 0;

e771:  - b127 + b131 - b142 <= 0;

e772:  - b127 + b132 - b143 <= 0;

e773:  - b128 + b129 - b144 <= 0;

e774:  - b128 + b130 - b145 <= 0;

e775:  - b128 + b131 - b146 <= 0;

e776:  - b128 + b132 - b147 <= 0;

e777:  - b129 + b130 - b148 <= 0;

e778:  - b129 + b131 - b149 <= 0;

e779:  - b129 + b132 - b150 <= 0;

e780:  - b130 + b131 - b151 <= 0;

e781:  - b130 + b132 - b152 <= 0;

e782:  - b131 + b132 - b153 <= 0;

e783:  - b133 + b134 - b139 <= 0;

e784:  - b133 + b135 - b140 <= 0;

e785:  - b133 + b136 - b141 <= 0;

e786:  - b133 + b137 - b142 <= 0;

e787:  - b133 + b138 - b143 <= 0;

e788:  - b134 + b135 - b144 <= 0;

e789:  - b134 + b136 - b145 <= 0;

e790:  - b134 + b137 - b146 <= 0;

e791:  - b134 + b138 - b147 <= 0;

e792:  - b135 + b136 - b148 <= 0;

e793:  - b135 + b137 - b149 <= 0;

e794:  - b135 + b138 - b150 <= 0;

e795:  - b136 + b137 - b151 <= 0;

e796:  - b136 + b138 - b152 <= 0;

e797:  - b137 + b138 - b153 <= 0;

e798:  - b139 + b140 - b144 <= 0;

e799:  - b139 + b141 - b145 <= 0;

e800:  - b139 + b142 - b146 <= 0;

e801:  - b139 + b143 - b147 <= 0;

e802:  - b140 + b141 - b148 <= 0;

e803:  - b140 + b142 - b149 <= 0;

e804:  - b140 + b143 - b150 <= 0;

e805:  - b141 + b142 - b151 <= 0;

e806:  - b141 + b143 - b152 <= 0;

e807:  - b142 + b143 - b153 <= 0;

e808:  - b144 + b145 - b148 <= 0;

e809:  - b144 + b146 - b149 <= 0;

e810:  - b144 + b147 - b150 <= 0;

e811:  - b145 + b146 - b151 <= 0;

e812:  - b145 + b147 - b152 <= 0;

e813:  - b146 + b147 - b153 <= 0;

e814:  - b148 + b149 - b151 <= 0;

e815:  - b148 + b150 - b152 <= 0;

e816:  - b149 + b150 - b153 <= 0;

e817:  - b151 + b152 - b153 <= 0;

e818:    b2 - b3 - b19 <= 0;

e819:    b2 - b4 - b154 <= 0;

e820:    b2 - b5 - b20 <= 0;

e821:    b2 - b6 - b21 <= 0;

e822:    b2 - b7 - b22 <= 0;

e823:    b2 - b8 - b23 <= 0;

e824:    b2 - b9 - b24 <= 0;

e825:    b2 - b10 - b25 <= 0;

e826:    b2 - b11 - b26 <= 0;

e827:    b2 - b12 - b27 <= 0;

e828:    b2 - b13 - b28 <= 0;

e829:    b2 - b14 - b29 <= 0;

e830:    b2 - b15 - b30 <= 0;

e831:    b2 - b16 - b31 <= 0;

e832:    b2 - b17 - b32 <= 0;

e833:    b2 - b18 - b33 <= 0;

e834:    b3 - b4 - b34 <= 0;

e835:    b3 - b5 - b35 <= 0;

e836:    b3 - b6 - b36 <= 0;

e837:    b3 - b7 - b37 <= 0;

e838:    b3 - b8 - b38 <= 0;

e839:    b3 - b9 - b39 <= 0;

e840:    b3 - b10 - b40 <= 0;

e841:    b3 - b11 - b41 <= 0;

e842:    b3 - b12 - b42 <= 0;

e843:    b3 - b13 - b43 <= 0;

e844:    b3 - b14 - b44 <= 0;

e845:    b3 - b15 - b45 <= 0;

e846:    b3 - b16 - b46 <= 0;

e847:    b3 - b17 - b47 <= 0;

e848:    b3 - b18 - b48 <= 0;

e849:    b4 - b5 - b49 <= 0;

e850:    b4 - b6 - b50 <= 0;

e851:    b4 - b7 - b51 <= 0;

e852:    b4 - b8 - b52 <= 0;

e853:    b4 - b9 - b53 <= 0;

e854:    b4 - b10 - b54 <= 0;

e855:    b4 - b11 - b55 <= 0;

e856:    b4 - b12 - b56 <= 0;

e857:    b4 - b13 - b57 <= 0;

e858:    b4 - b14 - b58 <= 0;

e859:    b4 - b15 - b59 <= 0;

e860:    b4 - b16 - b60 <= 0;

e861:    b4 - b17 - b61 <= 0;

e862:    b4 - b18 - b62 <= 0;

e863:    b5 - b6 - b63 <= 0;

e864:    b5 - b7 - b64 <= 0;

e865:    b5 - b8 - b65 <= 0;

e866:    b5 - b9 - b66 <= 0;

e867:    b5 - b10 - b67 <= 0;

e868:    b5 - b11 - b68 <= 0;

e869:    b5 - b12 - b69 <= 0;

e870:    b5 - b13 - b70 <= 0;

e871:    b5 - b14 - b71 <= 0;

e872:    b5 - b15 - b72 <= 0;

e873:    b5 - b16 - b73 <= 0;

e874:    b5 - b17 - b74 <= 0;

e875:    b5 - b18 - b75 <= 0;

e876:    b6 - b7 - b76 <= 0;

e877:    b6 - b8 - b77 <= 0;

e878:    b6 - b9 - b78 <= 0;

e879:    b6 - b10 - b79 <= 0;

e880:    b6 - b11 - b80 <= 0;

e881:    b6 - b12 - b81 <= 0;

e882:    b6 - b13 - b82 <= 0;

e883:    b6 - b14 - b83 <= 0;

e884:    b6 - b15 - b84 <= 0;

e885:    b6 - b16 - b85 <= 0;

e886:    b6 - b17 - b86 <= 0;

e887:    b6 - b18 - b87 <= 0;

e888:    b7 - b8 - b88 <= 0;

e889:    b7 - b9 - b89 <= 0;

e890:    b7 - b10 - b90 <= 0;

e891:    b7 - b11 - b91 <= 0;

e892:    b7 - b12 - b92 <= 0;

e893:    b7 - b13 - b93 <= 0;

e894:    b7 - b14 - b94 <= 0;

e895:    b7 - b15 - b95 <= 0;

e896:    b7 - b16 - b96 <= 0;

e897:    b7 - b17 - b97 <= 0;

e898:    b7 - b18 - b98 <= 0;

e899:    b8 - b9 - b99 <= 0;

e900:    b8 - b10 - b100 <= 0;

e901:    b8 - b11 - b101 <= 0;

e902:    b8 - b12 - b102 <= 0;

e903:    b8 - b13 - b103 <= 0;

e904:    b8 - b14 - b104 <= 0;

e905:    b8 - b15 - b105 <= 0;

e906:    b8 - b16 - b106 <= 0;

e907:    b8 - b17 - b107 <= 0;

e908:    b8 - b18 - b108 <= 0;

e909:    b9 - b10 - b109 <= 0;

e910:    b9 - b11 - b110 <= 0;

e911:    b9 - b12 - b111 <= 0;

e912:    b9 - b13 - b112 <= 0;

e913:    b9 - b14 - b113 <= 0;

e914:    b9 - b15 - b114 <= 0;

e915:    b9 - b16 - b115 <= 0;

e916:    b9 - b17 - b116 <= 0;

e917:    b9 - b18 - b117 <= 0;

e918:    b10 - b11 - b118 <= 0;

e919:    b10 - b12 - b119 <= 0;

e920:    b10 - b13 - b120 <= 0;

e921:    b10 - b14 - b121 <= 0;

e922:    b10 - b15 - b122 <= 0;

e923:    b10 - b16 - b123 <= 0;

e924:    b10 - b17 - b124 <= 0;

e925:    b10 - b18 - b125 <= 0;

e926:    b11 - b12 - b126 <= 0;

e927:    b11 - b13 - b127 <= 0;

e928:    b11 - b14 - b128 <= 0;

e929:    b11 - b15 - b129 <= 0;

e930:    b11 - b16 - b130 <= 0;

e931:    b11 - b17 - b131 <= 0;

e932:    b11 - b18 - b132 <= 0;

e933:    b12 - b13 - b133 <= 0;

e934:    b12 - b14 - b134 <= 0;

e935:    b12 - b15 - b135 <= 0;

e936:    b12 - b16 - b136 <= 0;

e937:    b12 - b17 - b137 <= 0;

e938:    b12 - b18 - b138 <= 0;

e939:    b13 - b14 - b139 <= 0;

e940:    b13 - b15 - b140 <= 0;

e941:    b13 - b16 - b141 <= 0;

e942:    b13 - b17 - b142 <= 0;

e943:    b13 - b18 - b143 <= 0;

e944:    b14 - b15 - b144 <= 0;

e945:    b14 - b16 - b145 <= 0;

e946:    b14 - b17 - b146 <= 0;

e947:    b14 - b18 - b147 <= 0;

e948:    b15 - b16 - b148 <= 0;

e949:    b15 - b17 - b149 <= 0;

e950:    b15 - b18 - b150 <= 0;

e951:    b16 - b17 - b151 <= 0;

e952:    b16 - b18 - b152 <= 0;

e953:    b17 - b18 - b153 <= 0;

e954:    b19 - b34 - b154 <= 0;

e955:    b19 - b20 - b35 <= 0;

e956:    b19 - b21 - b36 <= 0;

e957:    b19 - b22 - b37 <= 0;

e958:    b19 - b23 - b38 <= 0;

e959:    b19 - b24 - b39 <= 0;

e960:    b19 - b25 - b40 <= 0;

e961:    b19 - b26 - b41 <= 0;

e962:    b19 - b27 - b42 <= 0;

e963:    b19 - b28 - b43 <= 0;

e964:    b19 - b29 - b44 <= 0;

e965:    b19 - b30 - b45 <= 0;

e966:    b19 - b31 - b46 <= 0;

e967:    b19 - b32 - b47 <= 0;

e968:    b19 - b33 - b48 <= 0;

e969:  - b20 - b49 + b154 <= 0;

e970:  - b21 - b50 + b154 <= 0;

e971:  - b22 - b51 + b154 <= 0;

e972:  - b23 - b52 + b154 <= 0;

e973:  - b24 - b53 + b154 <= 0;

e974:  - b25 - b54 + b154 <= 0;

e975:  - b26 - b55 + b154 <= 0;

e976:  - b27 - b56 + b154 <= 0;

e977:  - b28 - b57 + b154 <= 0;

e978:  - b29 - b58 + b154 <= 0;

e979:  - b30 - b59 + b154 <= 0;

e980:  - b31 - b60 + b154 <= 0;

e981:  - b32 - b61 + b154 <= 0;

e982:  - b33 - b62 + b154 <= 0;

e983:    b20 - b21 - b63 <= 0;

e984:    b20 - b22 - b64 <= 0;

e985:    b20 - b23 - b65 <= 0;

e986:    b20 - b24 - b66 <= 0;

e987:    b20 - b25 - b67 <= 0;

e988:    b20 - b26 - b68 <= 0;

e989:    b20 - b27 - b69 <= 0;

e990:    b20 - b28 - b70 <= 0;

e991:    b20 - b29 - b71 <= 0;

e992:    b20 - b30 - b72 <= 0;

e993:    b20 - b31 - b73 <= 0;

e994:    b20 - b32 - b74 <= 0;

e995:    b20 - b33 - b75 <= 0;

e996:    b21 - b22 - b76 <= 0;

e997:    b21 - b23 - b77 <= 0;

e998:    b21 - b24 - b78 <= 0;

e999:    b21 - b25 - b79 <= 0;

e1000:    b21 - b26 - b80 <= 0;

e1001:    b21 - b27 - b81 <= 0;

e1002:    b21 - b28 - b82 <= 0;

e1003:    b21 - b29 - b83 <= 0;

e1004:    b21 - b30 - b84 <= 0;

e1005:    b21 - b31 - b85 <= 0;

e1006:    b21 - b32 - b86 <= 0;

e1007:    b21 - b33 - b87 <= 0;

e1008:    b22 - b23 - b88 <= 0;

e1009:    b22 - b24 - b89 <= 0;

e1010:    b22 - b25 - b90 <= 0;

e1011:    b22 - b26 - b91 <= 0;

e1012:    b22 - b27 - b92 <= 0;

e1013:    b22 - b28 - b93 <= 0;

e1014:    b22 - b29 - b94 <= 0;

e1015:    b22 - b30 - b95 <= 0;

e1016:    b22 - b31 - b96 <= 0;

e1017:    b22 - b32 - b97 <= 0;

e1018:    b22 - b33 - b98 <= 0;

e1019:    b23 - b24 - b99 <= 0;

e1020:    b23 - b25 - b100 <= 0;

e1021:    b23 - b26 - b101 <= 0;

e1022:    b23 - b27 - b102 <= 0;

e1023:    b23 - b28 - b103 <= 0;

e1024:    b23 - b29 - b104 <= 0;

e1025:    b23 - b30 - b105 <= 0;

e1026:    b23 - b31 - b106 <= 0;

e1027:    b23 - b32 - b107 <= 0;

e1028:    b23 - b33 - b108 <= 0;

e1029:    b24 - b25 - b109 <= 0;

e1030:    b24 - b26 - b110 <= 0;

e1031:    b24 - b27 - b111 <= 0;

e1032:    b24 - b28 - b112 <= 0;

e1033:    b24 - b29 - b113 <= 0;

e1034:    b24 - b30 - b114 <= 0;

e1035:    b24 - b31 - b115 <= 0;

e1036:    b24 - b32 - b116 <= 0;

e1037:    b24 - b33 - b117 <= 0;

e1038:    b25 - b26 - b118 <= 0;

e1039:    b25 - b27 - b119 <= 0;

e1040:    b25 - b28 - b120 <= 0;

e1041:    b25 - b29 - b121 <= 0;

e1042:    b25 - b30 - b122 <= 0;

e1043:    b25 - b31 - b123 <= 0;

e1044:    b25 - b32 - b124 <= 0;

e1045:    b25 - b33 - b125 <= 0;

e1046:    b26 - b27 - b126 <= 0;

e1047:    b26 - b28 - b127 <= 0;

e1048:    b26 - b29 - b128 <= 0;

e1049:    b26 - b30 - b129 <= 0;

e1050:    b26 - b31 - b130 <= 0;

e1051:    b26 - b32 - b131 <= 0;

e1052:    b26 - b33 - b132 <= 0;

e1053:    b27 - b28 - b133 <= 0;

e1054:    b27 - b29 - b134 <= 0;

e1055:    b27 - b30 - b135 <= 0;

e1056:    b27 - b31 - b136 <= 0;

e1057:    b27 - b32 - b137 <= 0;

e1058:    b27 - b33 - b138 <= 0;

e1059:    b28 - b29 - b139 <= 0;

e1060:    b28 - b30 - b140 <= 0;

e1061:    b28 - b31 - b141 <= 0;

e1062:    b28 - b32 - b142 <= 0;

e1063:    b28 - b33 - b143 <= 0;

e1064:    b29 - b30 - b144 <= 0;

e1065:    b29 - b31 - b145 <= 0;

e1066:    b29 - b32 - b146 <= 0;

e1067:    b29 - b33 - b147 <= 0;

e1068:    b30 - b31 - b148 <= 0;

e1069:    b30 - b32 - b149 <= 0;

e1070:    b30 - b33 - b150 <= 0;

e1071:    b31 - b32 - b151 <= 0;

e1072:    b31 - b33 - b152 <= 0;

e1073:    b32 - b33 - b153 <= 0;

e1074:    b34 - b35 - b49 <= 0;

e1075:    b34 - b36 - b50 <= 0;

e1076:    b34 - b37 - b51 <= 0;

e1077:    b34 - b38 - b52 <= 0;

e1078:    b34 - b39 - b53 <= 0;

e1079:    b34 - b40 - b54 <= 0;

e1080:    b34 - b41 - b55 <= 0;

e1081:    b34 - b42 - b56 <= 0;

e1082:    b34 - b43 - b57 <= 0;

e1083:    b34 - b44 - b58 <= 0;

e1084:    b34 - b45 - b59 <= 0;

e1085:    b34 - b46 - b60 <= 0;

e1086:    b34 - b47 - b61 <= 0;

e1087:    b34 - b48 - b62 <= 0;

e1088:    b35 - b36 - b63 <= 0;

e1089:    b35 - b37 - b64 <= 0;

e1090:    b35 - b38 - b65 <= 0;

e1091:    b35 - b39 - b66 <= 0;

e1092:    b35 - b40 - b67 <= 0;

e1093:    b35 - b41 - b68 <= 0;

e1094:    b35 - b42 - b69 <= 0;

e1095:    b35 - b43 - b70 <= 0;

e1096:    b35 - b44 - b71 <= 0;

e1097:    b35 - b45 - b72 <= 0;

e1098:    b35 - b46 - b73 <= 0;

e1099:    b35 - b47 - b74 <= 0;

e1100:    b35 - b48 - b75 <= 0;

e1101:    b36 - b37 - b76 <= 0;

e1102:    b36 - b38 - b77 <= 0;

e1103:    b36 - b39 - b78 <= 0;

e1104:    b36 - b40 - b79 <= 0;

e1105:    b36 - b41 - b80 <= 0;

e1106:    b36 - b42 - b81 <= 0;

e1107:    b36 - b43 - b82 <= 0;

e1108:    b36 - b44 - b83 <= 0;

e1109:    b36 - b45 - b84 <= 0;

e1110:    b36 - b46 - b85 <= 0;

e1111:    b36 - b47 - b86 <= 0;

e1112:    b36 - b48 - b87 <= 0;

e1113:    b37 - b38 - b88 <= 0;

e1114:    b37 - b39 - b89 <= 0;

e1115:    b37 - b40 - b90 <= 0;

e1116:    b37 - b41 - b91 <= 0;

e1117:    b37 - b42 - b92 <= 0;

e1118:    b37 - b43 - b93 <= 0;

e1119:    b37 - b44 - b94 <= 0;

e1120:    b37 - b45 - b95 <= 0;

e1121:    b37 - b46 - b96 <= 0;

e1122:    b37 - b47 - b97 <= 0;

e1123:    b37 - b48 - b98 <= 0;

e1124:    b38 - b39 - b99 <= 0;

e1125:    b38 - b40 - b100 <= 0;

e1126:    b38 - b41 - b101 <= 0;

e1127:    b38 - b42 - b102 <= 0;

e1128:    b38 - b43 - b103 <= 0;

e1129:    b38 - b44 - b104 <= 0;

e1130:    b38 - b45 - b105 <= 0;

e1131:    b38 - b46 - b106 <= 0;

e1132:    b38 - b47 - b107 <= 0;

e1133:    b38 - b48 - b108 <= 0;

e1134:    b39 - b40 - b109 <= 0;

e1135:    b39 - b41 - b110 <= 0;

e1136:    b39 - b42 - b111 <= 0;

e1137:    b39 - b43 - b112 <= 0;

e1138:    b39 - b44 - b113 <= 0;

e1139:    b39 - b45 - b114 <= 0;

e1140:    b39 - b46 - b115 <= 0;

e1141:    b39 - b47 - b116 <= 0;

e1142:    b39 - b48 - b117 <= 0;

e1143:    b40 - b41 - b118 <= 0;

e1144:    b40 - b42 - b119 <= 0;

e1145:    b40 - b43 - b120 <= 0;

e1146:    b40 - b44 - b121 <= 0;

e1147:    b40 - b45 - b122 <= 0;

e1148:    b40 - b46 - b123 <= 0;

e1149:    b40 - b47 - b124 <= 0;

e1150:    b40 - b48 - b125 <= 0;

e1151:    b41 - b42 - b126 <= 0;

e1152:    b41 - b43 - b127 <= 0;

e1153:    b41 - b44 - b128 <= 0;

e1154:    b41 - b45 - b129 <= 0;

e1155:    b41 - b46 - b130 <= 0;

e1156:    b41 - b47 - b131 <= 0;

e1157:    b41 - b48 - b132 <= 0;

e1158:    b42 - b43 - b133 <= 0;

e1159:    b42 - b44 - b134 <= 0;

e1160:    b42 - b45 - b135 <= 0;

e1161:    b42 - b46 - b136 <= 0;

e1162:    b42 - b47 - b137 <= 0;

e1163:    b42 - b48 - b138 <= 0;

e1164:    b43 - b44 - b139 <= 0;

e1165:    b43 - b45 - b140 <= 0;

e1166:    b43 - b46 - b141 <= 0;

e1167:    b43 - b47 - b142 <= 0;

e1168:    b43 - b48 - b143 <= 0;

e1169:    b44 - b45 - b144 <= 0;

e1170:    b44 - b46 - b145 <= 0;

e1171:    b44 - b47 - b146 <= 0;

e1172:    b44 - b48 - b147 <= 0;

e1173:    b45 - b46 - b148 <= 0;

e1174:    b45 - b47 - b149 <= 0;

e1175:    b45 - b48 - b150 <= 0;

e1176:    b46 - b47 - b151 <= 0;

e1177:    b46 - b48 - b152 <= 0;

e1178:    b47 - b48 - b153 <= 0;

e1179:    b49 - b50 - b63 <= 0;

e1180:    b49 - b51 - b64 <= 0;

e1181:    b49 - b52 - b65 <= 0;

e1182:    b49 - b53 - b66 <= 0;

e1183:    b49 - b54 - b67 <= 0;

e1184:    b49 - b55 - b68 <= 0;

e1185:    b49 - b56 - b69 <= 0;

e1186:    b49 - b57 - b70 <= 0;

e1187:    b49 - b58 - b71 <= 0;

e1188:    b49 - b59 - b72 <= 0;

e1189:    b49 - b60 - b73 <= 0;

e1190:    b49 - b61 - b74 <= 0;

e1191:    b49 - b62 - b75 <= 0;

e1192:    b50 - b51 - b76 <= 0;

e1193:    b50 - b52 - b77 <= 0;

e1194:    b50 - b53 - b78 <= 0;

e1195:    b50 - b54 - b79 <= 0;

e1196:    b50 - b55 - b80 <= 0;

e1197:    b50 - b56 - b81 <= 0;

e1198:    b50 - b57 - b82 <= 0;

e1199:    b50 - b58 - b83 <= 0;

e1200:    b50 - b59 - b84 <= 0;

e1201:    b50 - b60 - b85 <= 0;

e1202:    b50 - b61 - b86 <= 0;

e1203:    b50 - b62 - b87 <= 0;

e1204:    b51 - b52 - b88 <= 0;

e1205:    b51 - b53 - b89 <= 0;

e1206:    b51 - b54 - b90 <= 0;

e1207:    b51 - b55 - b91 <= 0;

e1208:    b51 - b56 - b92 <= 0;

e1209:    b51 - b57 - b93 <= 0;

e1210:    b51 - b58 - b94 <= 0;

e1211:    b51 - b59 - b95 <= 0;

e1212:    b51 - b60 - b96 <= 0;

e1213:    b51 - b61 - b97 <= 0;

e1214:    b51 - b62 - b98 <= 0;

e1215:    b52 - b53 - b99 <= 0;

e1216:    b52 - b54 - b100 <= 0;

e1217:    b52 - b55 - b101 <= 0;

e1218:    b52 - b56 - b102 <= 0;

e1219:    b52 - b57 - b103 <= 0;

e1220:    b52 - b58 - b104 <= 0;

e1221:    b52 - b59 - b105 <= 0;

e1222:    b52 - b60 - b106 <= 0;

e1223:    b52 - b61 - b107 <= 0;

e1224:    b52 - b62 - b108 <= 0;

e1225:    b53 - b54 - b109 <= 0;

e1226:    b53 - b55 - b110 <= 0;

e1227:    b53 - b56 - b111 <= 0;

e1228:    b53 - b57 - b112 <= 0;

e1229:    b53 - b58 - b113 <= 0;

e1230:    b53 - b59 - b114 <= 0;

e1231:    b53 - b60 - b115 <= 0;

e1232:    b53 - b61 - b116 <= 0;

e1233:    b53 - b62 - b117 <= 0;

e1234:    b54 - b55 - b118 <= 0;

e1235:    b54 - b56 - b119 <= 0;

e1236:    b54 - b57 - b120 <= 0;

e1237:    b54 - b58 - b121 <= 0;

e1238:    b54 - b59 - b122 <= 0;

e1239:    b54 - b60 - b123 <= 0;

e1240:    b54 - b61 - b124 <= 0;

e1241:    b54 - b62 - b125 <= 0;

e1242:    b55 - b56 - b126 <= 0;

e1243:    b55 - b57 - b127 <= 0;

e1244:    b55 - b58 - b128 <= 0;

e1245:    b55 - b59 - b129 <= 0;

e1246:    b55 - b60 - b130 <= 0;

e1247:    b55 - b61 - b131 <= 0;

e1248:    b55 - b62 - b132 <= 0;

e1249:    b56 - b57 - b133 <= 0;

e1250:    b56 - b58 - b134 <= 0;

e1251:    b56 - b59 - b135 <= 0;

e1252:    b56 - b60 - b136 <= 0;

e1253:    b56 - b61 - b137 <= 0;

e1254:    b56 - b62 - b138 <= 0;

e1255:    b57 - b58 - b139 <= 0;

e1256:    b57 - b59 - b140 <= 0;

e1257:    b57 - b60 - b141 <= 0;

e1258:    b57 - b61 - b142 <= 0;

e1259:    b57 - b62 - b143 <= 0;

e1260:    b58 - b59 - b144 <= 0;

e1261:    b58 - b60 - b145 <= 0;

e1262:    b58 - b61 - b146 <= 0;

e1263:    b58 - b62 - b147 <= 0;

e1264:    b59 - b60 - b148 <= 0;

e1265:    b59 - b61 - b149 <= 0;

e1266:    b59 - b62 - b150 <= 0;

e1267:    b60 - b61 - b151 <= 0;

e1268:    b60 - b62 - b152 <= 0;

e1269:    b61 - b62 - b153 <= 0;

e1270:    b63 - b64 - b76 <= 0;

e1271:    b63 - b65 - b77 <= 0;

e1272:    b63 - b66 - b78 <= 0;

e1273:    b63 - b67 - b79 <= 0;

e1274:    b63 - b68 - b80 <= 0;

e1275:    b63 - b69 - b81 <= 0;

e1276:    b63 - b70 - b82 <= 0;

e1277:    b63 - b71 - b83 <= 0;

e1278:    b63 - b72 - b84 <= 0;

e1279:    b63 - b73 - b85 <= 0;

e1280:    b63 - b74 - b86 <= 0;

e1281:    b63 - b75 - b87 <= 0;

e1282:    b64 - b65 - b88 <= 0;

e1283:    b64 - b66 - b89 <= 0;

e1284:    b64 - b67 - b90 <= 0;

e1285:    b64 - b68 - b91 <= 0;

e1286:    b64 - b69 - b92 <= 0;

e1287:    b64 - b70 - b93 <= 0;

e1288:    b64 - b71 - b94 <= 0;

e1289:    b64 - b72 - b95 <= 0;

e1290:    b64 - b73 - b96 <= 0;

e1291:    b64 - b74 - b97 <= 0;

e1292:    b64 - b75 - b98 <= 0;

e1293:    b65 - b66 - b99 <= 0;

e1294:    b65 - b67 - b100 <= 0;

e1295:    b65 - b68 - b101 <= 0;

e1296:    b65 - b69 - b102 <= 0;

e1297:    b65 - b70 - b103 <= 0;

e1298:    b65 - b71 - b104 <= 0;

e1299:    b65 - b72 - b105 <= 0;

e1300:    b65 - b73 - b106 <= 0;

e1301:    b65 - b74 - b107 <= 0;

e1302:    b65 - b75 - b108 <= 0;

e1303:    b66 - b67 - b109 <= 0;

e1304:    b66 - b68 - b110 <= 0;

e1305:    b66 - b69 - b111 <= 0;

e1306:    b66 - b70 - b112 <= 0;

e1307:    b66 - b71 - b113 <= 0;

e1308:    b66 - b72 - b114 <= 0;

e1309:    b66 - b73 - b115 <= 0;

e1310:    b66 - b74 - b116 <= 0;

e1311:    b66 - b75 - b117 <= 0;

e1312:    b67 - b68 - b118 <= 0;

e1313:    b67 - b69 - b119 <= 0;

e1314:    b67 - b70 - b120 <= 0;

e1315:    b67 - b71 - b121 <= 0;

e1316:    b67 - b72 - b122 <= 0;

e1317:    b67 - b73 - b123 <= 0;

e1318:    b67 - b74 - b124 <= 0;

e1319:    b67 - b75 - b125 <= 0;

e1320:    b68 - b69 - b126 <= 0;

e1321:    b68 - b70 - b127 <= 0;

e1322:    b68 - b71 - b128 <= 0;

e1323:    b68 - b72 - b129 <= 0;

e1324:    b68 - b73 - b130 <= 0;

e1325:    b68 - b74 - b131 <= 0;

e1326:    b68 - b75 - b132 <= 0;

e1327:    b69 - b70 - b133 <= 0;

e1328:    b69 - b71 - b134 <= 0;

e1329:    b69 - b72 - b135 <= 0;

e1330:    b69 - b73 - b136 <= 0;

e1331:    b69 - b74 - b137 <= 0;

e1332:    b69 - b75 - b138 <= 0;

e1333:    b70 - b71 - b139 <= 0;

e1334:    b70 - b72 - b140 <= 0;

e1335:    b70 - b73 - b141 <= 0;

e1336:    b70 - b74 - b142 <= 0;

e1337:    b70 - b75 - b143 <= 0;

e1338:    b71 - b72 - b144 <= 0;

e1339:    b71 - b73 - b145 <= 0;

e1340:    b71 - b74 - b146 <= 0;

e1341:    b71 - b75 - b147 <= 0;

e1342:    b72 - b73 - b148 <= 0;

e1343:    b72 - b74 - b149 <= 0;

e1344:    b72 - b75 - b150 <= 0;

e1345:    b73 - b74 - b151 <= 0;

e1346:    b73 - b75 - b152 <= 0;

e1347:    b74 - b75 - b153 <= 0;

e1348:    b76 - b77 - b88 <= 0;

e1349:    b76 - b78 - b89 <= 0;

e1350:    b76 - b79 - b90 <= 0;

e1351:    b76 - b80 - b91 <= 0;

e1352:    b76 - b81 - b92 <= 0;

e1353:    b76 - b82 - b93 <= 0;

e1354:    b76 - b83 - b94 <= 0;

e1355:    b76 - b84 - b95 <= 0;

e1356:    b76 - b85 - b96 <= 0;

e1357:    b76 - b86 - b97 <= 0;

e1358:    b76 - b87 - b98 <= 0;

e1359:    b77 - b78 - b99 <= 0;

e1360:    b77 - b79 - b100 <= 0;

e1361:    b77 - b80 - b101 <= 0;

e1362:    b77 - b81 - b102 <= 0;

e1363:    b77 - b82 - b103 <= 0;

e1364:    b77 - b83 - b104 <= 0;

e1365:    b77 - b84 - b105 <= 0;

e1366:    b77 - b85 - b106 <= 0;

e1367:    b77 - b86 - b107 <= 0;

e1368:    b77 - b87 - b108 <= 0;

e1369:    b78 - b79 - b109 <= 0;

e1370:    b78 - b80 - b110 <= 0;

e1371:    b78 - b81 - b111 <= 0;

e1372:    b78 - b82 - b112 <= 0;

e1373:    b78 - b83 - b113 <= 0;

e1374:    b78 - b84 - b114 <= 0;

e1375:    b78 - b85 - b115 <= 0;

e1376:    b78 - b86 - b116 <= 0;

e1377:    b78 - b87 - b117 <= 0;

e1378:    b79 - b80 - b118 <= 0;

e1379:    b79 - b81 - b119 <= 0;

e1380:    b79 - b82 - b120 <= 0;

e1381:    b79 - b83 - b121 <= 0;

e1382:    b79 - b84 - b122 <= 0;

e1383:    b79 - b85 - b123 <= 0;

e1384:    b79 - b86 - b124 <= 0;

e1385:    b79 - b87 - b125 <= 0;

e1386:    b80 - b81 - b126 <= 0;

e1387:    b80 - b82 - b127 <= 0;

e1388:    b80 - b83 - b128 <= 0;

e1389:    b80 - b84 - b129 <= 0;

e1390:    b80 - b85 - b130 <= 0;

e1391:    b80 - b86 - b131 <= 0;

e1392:    b80 - b87 - b132 <= 0;

e1393:    b81 - b82 - b133 <= 0;

e1394:    b81 - b83 - b134 <= 0;

e1395:    b81 - b84 - b135 <= 0;

e1396:    b81 - b85 - b136 <= 0;

e1397:    b81 - b86 - b137 <= 0;

e1398:    b81 - b87 - b138 <= 0;

e1399:    b82 - b83 - b139 <= 0;

e1400:    b82 - b84 - b140 <= 0;

e1401:    b82 - b85 - b141 <= 0;

e1402:    b82 - b86 - b142 <= 0;

e1403:    b82 - b87 - b143 <= 0;

e1404:    b83 - b84 - b144 <= 0;

e1405:    b83 - b85 - b145 <= 0;

e1406:    b83 - b86 - b146 <= 0;

e1407:    b83 - b87 - b147 <= 0;

e1408:    b84 - b85 - b148 <= 0;

e1409:    b84 - b86 - b149 <= 0;

e1410:    b84 - b87 - b150 <= 0;

e1411:    b85 - b86 - b151 <= 0;

e1412:    b85 - b87 - b152 <= 0;

e1413:    b86 - b87 - b153 <= 0;

e1414:    b88 - b89 - b99 <= 0;

e1415:    b88 - b90 - b100 <= 0;

e1416:    b88 - b91 - b101 <= 0;

e1417:    b88 - b92 - b102 <= 0;

e1418:    b88 - b93 - b103 <= 0;

e1419:    b88 - b94 - b104 <= 0;

e1420:    b88 - b95 - b105 <= 0;

e1421:    b88 - b96 - b106 <= 0;

e1422:    b88 - b97 - b107 <= 0;

e1423:    b88 - b98 - b108 <= 0;

e1424:    b89 - b90 - b109 <= 0;

e1425:    b89 - b91 - b110 <= 0;

e1426:    b89 - b92 - b111 <= 0;

e1427:    b89 - b93 - b112 <= 0;

e1428:    b89 - b94 - b113 <= 0;

e1429:    b89 - b95 - b114 <= 0;

e1430:    b89 - b96 - b115 <= 0;

e1431:    b89 - b97 - b116 <= 0;

e1432:    b89 - b98 - b117 <= 0;

e1433:    b90 - b91 - b118 <= 0;

e1434:    b90 - b92 - b119 <= 0;

e1435:    b90 - b93 - b120 <= 0;

e1436:    b90 - b94 - b121 <= 0;

e1437:    b90 - b95 - b122 <= 0;

e1438:    b90 - b96 - b123 <= 0;

e1439:    b90 - b97 - b124 <= 0;

e1440:    b90 - b98 - b125 <= 0;

e1441:    b91 - b92 - b126 <= 0;

e1442:    b91 - b93 - b127 <= 0;

e1443:    b91 - b94 - b128 <= 0;

e1444:    b91 - b95 - b129 <= 0;

e1445:    b91 - b96 - b130 <= 0;

e1446:    b91 - b97 - b131 <= 0;

e1447:    b91 - b98 - b132 <= 0;

e1448:    b92 - b93 - b133 <= 0;

e1449:    b92 - b94 - b134 <= 0;

e1450:    b92 - b95 - b135 <= 0;

e1451:    b92 - b96 - b136 <= 0;

e1452:    b92 - b97 - b137 <= 0;

e1453:    b92 - b98 - b138 <= 0;

e1454:    b93 - b94 - b139 <= 0;

e1455:    b93 - b95 - b140 <= 0;

e1456:    b93 - b96 - b141 <= 0;

e1457:    b93 - b97 - b142 <= 0;

e1458:    b93 - b98 - b143 <= 0;

e1459:    b94 - b95 - b144 <= 0;

e1460:    b94 - b96 - b145 <= 0;

e1461:    b94 - b97 - b146 <= 0;

e1462:    b94 - b98 - b147 <= 0;

e1463:    b95 - b96 - b148 <= 0;

e1464:    b95 - b97 - b149 <= 0;

e1465:    b95 - b98 - b150 <= 0;

e1466:    b96 - b97 - b151 <= 0;

e1467:    b96 - b98 - b152 <= 0;

e1468:    b97 - b98 - b153 <= 0;

e1469:    b99 - b100 - b109 <= 0;

e1470:    b99 - b101 - b110 <= 0;

e1471:    b99 - b102 - b111 <= 0;

e1472:    b99 - b103 - b112 <= 0;

e1473:    b99 - b104 - b113 <= 0;

e1474:    b99 - b105 - b114 <= 0;

e1475:    b99 - b106 - b115 <= 0;

e1476:    b99 - b107 - b116 <= 0;

e1477:    b99 - b108 - b117 <= 0;

e1478:    b100 - b101 - b118 <= 0;

e1479:    b100 - b102 - b119 <= 0;

e1480:    b100 - b103 - b120 <= 0;

e1481:    b100 - b104 - b121 <= 0;

e1482:    b100 - b105 - b122 <= 0;

e1483:    b100 - b106 - b123 <= 0;

e1484:    b100 - b107 - b124 <= 0;

e1485:    b100 - b108 - b125 <= 0;

e1486:    b101 - b102 - b126 <= 0;

e1487:    b101 - b103 - b127 <= 0;

e1488:    b101 - b104 - b128 <= 0;

e1489:    b101 - b105 - b129 <= 0;

e1490:    b101 - b106 - b130 <= 0;

e1491:    b101 - b107 - b131 <= 0;

e1492:    b101 - b108 - b132 <= 0;

e1493:    b102 - b103 - b133 <= 0;

e1494:    b102 - b104 - b134 <= 0;

e1495:    b102 - b105 - b135 <= 0;

e1496:    b102 - b106 - b136 <= 0;

e1497:    b102 - b107 - b137 <= 0;

e1498:    b102 - b108 - b138 <= 0;

e1499:    b103 - b104 - b139 <= 0;

e1500:    b103 - b105 - b140 <= 0;

e1501:    b103 - b106 - b141 <= 0;

e1502:    b103 - b107 - b142 <= 0;

e1503:    b103 - b108 - b143 <= 0;

e1504:    b104 - b105 - b144 <= 0;

e1505:    b104 - b106 - b145 <= 0;

e1506:    b104 - b107 - b146 <= 0;

e1507:    b104 - b108 - b147 <= 0;

e1508:    b105 - b106 - b148 <= 0;

e1509:    b105 - b107 - b149 <= 0;

e1510:    b105 - b108 - b150 <= 0;

e1511:    b106 - b107 - b151 <= 0;

e1512:    b106 - b108 - b152 <= 0;

e1513:    b107 - b108 - b153 <= 0;

e1514:    b109 - b110 - b118 <= 0;

e1515:    b109 - b111 - b119 <= 0;

e1516:    b109 - b112 - b120 <= 0;

e1517:    b109 - b113 - b121 <= 0;

e1518:    b109 - b114 - b122 <= 0;

e1519:    b109 - b115 - b123 <= 0;

e1520:    b109 - b116 - b124 <= 0;

e1521:    b109 - b117 - b125 <= 0;

e1522:    b110 - b111 - b126 <= 0;

e1523:    b110 - b112 - b127 <= 0;

e1524:    b110 - b113 - b128 <= 0;

e1525:    b110 - b114 - b129 <= 0;

e1526:    b110 - b115 - b130 <= 0;

e1527:    b110 - b116 - b131 <= 0;

e1528:    b110 - b117 - b132 <= 0;

e1529:    b111 - b112 - b133 <= 0;

e1530:    b111 - b113 - b134 <= 0;

e1531:    b111 - b114 - b135 <= 0;

e1532:    b111 - b115 - b136 <= 0;

e1533:    b111 - b116 - b137 <= 0;

e1534:    b111 - b117 - b138 <= 0;

e1535:    b112 - b113 - b139 <= 0;

e1536:    b112 - b114 - b140 <= 0;

e1537:    b112 - b115 - b141 <= 0;

e1538:    b112 - b116 - b142 <= 0;

e1539:    b112 - b117 - b143 <= 0;

e1540:    b113 - b114 - b144 <= 0;

e1541:    b113 - b115 - b145 <= 0;

e1542:    b113 - b116 - b146 <= 0;

e1543:    b113 - b117 - b147 <= 0;

e1544:    b114 - b115 - b148 <= 0;

e1545:    b114 - b116 - b149 <= 0;

e1546:    b114 - b117 - b150 <= 0;

e1547:    b115 - b116 - b151 <= 0;

e1548:    b115 - b117 - b152 <= 0;

e1549:    b116 - b117 - b153 <= 0;

e1550:    b118 - b119 - b126 <= 0;

e1551:    b118 - b120 - b127 <= 0;

e1552:    b118 - b121 - b128 <= 0;

e1553:    b118 - b122 - b129 <= 0;

e1554:    b118 - b123 - b130 <= 0;

e1555:    b118 - b124 - b131 <= 0;

e1556:    b118 - b125 - b132 <= 0;

e1557:    b119 - b120 - b133 <= 0;

e1558:    b119 - b121 - b134 <= 0;

e1559:    b119 - b122 - b135 <= 0;

e1560:    b119 - b123 - b136 <= 0;

e1561:    b119 - b124 - b137 <= 0;

e1562:    b119 - b125 - b138 <= 0;

e1563:    b120 - b121 - b139 <= 0;

e1564:    b120 - b122 - b140 <= 0;

e1565:    b120 - b123 - b141 <= 0;

e1566:    b120 - b124 - b142 <= 0;

e1567:    b120 - b125 - b143 <= 0;

e1568:    b121 - b122 - b144 <= 0;

e1569:    b121 - b123 - b145 <= 0;

e1570:    b121 - b124 - b146 <= 0;

e1571:    b121 - b125 - b147 <= 0;

e1572:    b122 - b123 - b148 <= 0;

e1573:    b122 - b124 - b149 <= 0;

e1574:    b122 - b125 - b150 <= 0;

e1575:    b123 - b124 - b151 <= 0;

e1576:    b123 - b125 - b152 <= 0;

e1577:    b124 - b125 - b153 <= 0;

e1578:    b126 - b127 - b133 <= 0;

e1579:    b126 - b128 - b134 <= 0;

e1580:    b126 - b129 - b135 <= 0;

e1581:    b126 - b130 - b136 <= 0;

e1582:    b126 - b131 - b137 <= 0;

e1583:    b126 - b132 - b138 <= 0;

e1584:    b127 - b128 - b139 <= 0;

e1585:    b127 - b129 - b140 <= 0;

e1586:    b127 - b130 - b141 <= 0;

e1587:    b127 - b131 - b142 <= 0;

e1588:    b127 - b132 - b143 <= 0;

e1589:    b128 - b129 - b144 <= 0;

e1590:    b128 - b130 - b145 <= 0;

e1591:    b128 - b131 - b146 <= 0;

e1592:    b128 - b132 - b147 <= 0;

e1593:    b129 - b130 - b148 <= 0;

e1594:    b129 - b131 - b149 <= 0;

e1595:    b129 - b132 - b150 <= 0;

e1596:    b130 - b131 - b151 <= 0;

e1597:    b130 - b132 - b152 <= 0;

e1598:    b131 - b132 - b153 <= 0;

e1599:    b133 - b134 - b139 <= 0;

e1600:    b133 - b135 - b140 <= 0;

e1601:    b133 - b136 - b141 <= 0;

e1602:    b133 - b137 - b142 <= 0;

e1603:    b133 - b138 - b143 <= 0;

e1604:    b134 - b135 - b144 <= 0;

e1605:    b134 - b136 - b145 <= 0;

e1606:    b134 - b137 - b146 <= 0;

e1607:    b134 - b138 - b147 <= 0;

e1608:    b135 - b136 - b148 <= 0;

e1609:    b135 - b137 - b149 <= 0;

e1610:    b135 - b138 - b150 <= 0;

e1611:    b136 - b137 - b151 <= 0;

e1612:    b136 - b138 - b152 <= 0;

e1613:    b137 - b138 - b153 <= 0;

e1614:    b139 - b140 - b144 <= 0;

e1615:    b139 - b141 - b145 <= 0;

e1616:    b139 - b142 - b146 <= 0;

e1617:    b139 - b143 - b147 <= 0;

e1618:    b140 - b141 - b148 <= 0;

e1619:    b140 - b142 - b149 <= 0;

e1620:    b140 - b143 - b150 <= 0;

e1621:    b141 - b142 - b151 <= 0;

e1622:    b141 - b143 - b152 <= 0;

e1623:    b142 - b143 - b153 <= 0;

e1624:    b144 - b145 - b148 <= 0;

e1625:    b144 - b146 - b149 <= 0;

e1626:    b144 - b147 - b150 <= 0;

e1627:    b145 - b146 - b151 <= 0;

e1628:    b145 - b147 - b152 <= 0;

e1629:    b146 - b147 - b153 <= 0;

e1630:    b148 - b149 - b151 <= 0;

e1631:    b148 - b150 - b152 <= 0;

e1632:    b149 - b150 - b153 <= 0;

e1633:    b151 - b152 - b153 <= 0;

e1634:  - b2 - b3 + b19 <= 0;

e1635:  - b2 - b4 + b154 <= 0;

e1636:  - b2 - b5 + b20 <= 0;

e1637:  - b2 - b6 + b21 <= 0;

e1638:  - b2 - b7 + b22 <= 0;

e1639:  - b2 - b8 + b23 <= 0;

e1640:  - b2 - b9 + b24 <= 0;

e1641:  - b2 - b10 + b25 <= 0;

e1642:  - b2 - b11 + b26 <= 0;

e1643:  - b2 - b12 + b27 <= 0;

e1644:  - b2 - b13 + b28 <= 0;

e1645:  - b2 - b14 + b29 <= 0;

e1646:  - b2 - b15 + b30 <= 0;

e1647:  - b2 - b16 + b31 <= 0;

e1648:  - b2 - b17 + b32 <= 0;

e1649:  - b2 - b18 + b33 <= 0;

e1650:  - b3 - b4 + b34 <= 0;

e1651:  - b3 - b5 + b35 <= 0;

e1652:  - b3 - b6 + b36 <= 0;

e1653:  - b3 - b7 + b37 <= 0;

e1654:  - b3 - b8 + b38 <= 0;

e1655:  - b3 - b9 + b39 <= 0;

e1656:  - b3 - b10 + b40 <= 0;

e1657:  - b3 - b11 + b41 <= 0;

e1658:  - b3 - b12 + b42 <= 0;

e1659:  - b3 - b13 + b43 <= 0;

e1660:  - b3 - b14 + b44 <= 0;

e1661:  - b3 - b15 + b45 <= 0;

e1662:  - b3 - b16 + b46 <= 0;

e1663:  - b3 - b17 + b47 <= 0;

e1664:  - b3 - b18 + b48 <= 0;

e1665:  - b4 - b5 + b49 <= 0;

e1666:  - b4 - b6 + b50 <= 0;

e1667:  - b4 - b7 + b51 <= 0;

e1668:  - b4 - b8 + b52 <= 0;

e1669:  - b4 - b9 + b53 <= 0;

e1670:  - b4 - b10 + b54 <= 0;

e1671:  - b4 - b11 + b55 <= 0;

e1672:  - b4 - b12 + b56 <= 0;

e1673:  - b4 - b13 + b57 <= 0;

e1674:  - b4 - b14 + b58 <= 0;

e1675:  - b4 - b15 + b59 <= 0;

e1676:  - b4 - b16 + b60 <= 0;

e1677:  - b4 - b17 + b61 <= 0;

e1678:  - b4 - b18 + b62 <= 0;

e1679:  - b5 - b6 + b63 <= 0;

e1680:  - b5 - b7 + b64 <= 0;

e1681:  - b5 - b8 + b65 <= 0;

e1682:  - b5 - b9 + b66 <= 0;

e1683:  - b5 - b10 + b67 <= 0;

e1684:  - b5 - b11 + b68 <= 0;

e1685:  - b5 - b12 + b69 <= 0;

e1686:  - b5 - b13 + b70 <= 0;

e1687:  - b5 - b14 + b71 <= 0;

e1688:  - b5 - b15 + b72 <= 0;

e1689:  - b5 - b16 + b73 <= 0;

e1690:  - b5 - b17 + b74 <= 0;

e1691:  - b5 - b18 + b75 <= 0;

e1692:  - b6 - b7 + b76 <= 0;

e1693:  - b6 - b8 + b77 <= 0;

e1694:  - b6 - b9 + b78 <= 0;

e1695:  - b6 - b10 + b79 <= 0;

e1696:  - b6 - b11 + b80 <= 0;

e1697:  - b6 - b12 + b81 <= 0;

e1698:  - b6 - b13 + b82 <= 0;

e1699:  - b6 - b14 + b83 <= 0;

e1700:  - b6 - b15 + b84 <= 0;

e1701:  - b6 - b16 + b85 <= 0;

e1702:  - b6 - b17 + b86 <= 0;

e1703:  - b6 - b18 + b87 <= 0;

e1704:  - b7 - b8 + b88 <= 0;

e1705:  - b7 - b9 + b89 <= 0;

e1706:  - b7 - b10 + b90 <= 0;

e1707:  - b7 - b11 + b91 <= 0;

e1708:  - b7 - b12 + b92 <= 0;

e1709:  - b7 - b13 + b93 <= 0;

e1710:  - b7 - b14 + b94 <= 0;

e1711:  - b7 - b15 + b95 <= 0;

e1712:  - b7 - b16 + b96 <= 0;

e1713:  - b7 - b17 + b97 <= 0;

e1714:  - b7 - b18 + b98 <= 0;

e1715:  - b8 - b9 + b99 <= 0;

e1716:  - b8 - b10 + b100 <= 0;

e1717:  - b8 - b11 + b101 <= 0;

e1718:  - b8 - b12 + b102 <= 0;

e1719:  - b8 - b13 + b103 <= 0;

e1720:  - b8 - b14 + b104 <= 0;

e1721:  - b8 - b15 + b105 <= 0;

e1722:  - b8 - b16 + b106 <= 0;

e1723:  - b8 - b17 + b107 <= 0;

e1724:  - b8 - b18 + b108 <= 0;

e1725:  - b9 - b10 + b109 <= 0;

e1726:  - b9 - b11 + b110 <= 0;

e1727:  - b9 - b12 + b111 <= 0;

e1728:  - b9 - b13 + b112 <= 0;

e1729:  - b9 - b14 + b113 <= 0;

e1730:  - b9 - b15 + b114 <= 0;

e1731:  - b9 - b16 + b115 <= 0;

e1732:  - b9 - b17 + b116 <= 0;

e1733:  - b9 - b18 + b117 <= 0;

e1734:  - b10 - b11 + b118 <= 0;

e1735:  - b10 - b12 + b119 <= 0;

e1736:  - b10 - b13 + b120 <= 0;

e1737:  - b10 - b14 + b121 <= 0;

e1738:  - b10 - b15 + b122 <= 0;

e1739:  - b10 - b16 + b123 <= 0;

e1740:  - b10 - b17 + b124 <= 0;

e1741:  - b10 - b18 + b125 <= 0;

e1742:  - b11 - b12 + b126 <= 0;

e1743:  - b11 - b13 + b127 <= 0;

e1744:  - b11 - b14 + b128 <= 0;

e1745:  - b11 - b15 + b129 <= 0;

e1746:  - b11 - b16 + b130 <= 0;

e1747:  - b11 - b17 + b131 <= 0;

e1748:  - b11 - b18 + b132 <= 0;

e1749:  - b12 - b13 + b133 <= 0;

e1750:  - b12 - b14 + b134 <= 0;

e1751:  - b12 - b15 + b135 <= 0;

e1752:  - b12 - b16 + b136 <= 0;

e1753:  - b12 - b17 + b137 <= 0;

e1754:  - b12 - b18 + b138 <= 0;

e1755:  - b13 - b14 + b139 <= 0;

e1756:  - b13 - b15 + b140 <= 0;

e1757:  - b13 - b16 + b141 <= 0;

e1758:  - b13 - b17 + b142 <= 0;

e1759:  - b13 - b18 + b143 <= 0;

e1760:  - b14 - b15 + b144 <= 0;

e1761:  - b14 - b16 + b145 <= 0;

e1762:  - b14 - b17 + b146 <= 0;

e1763:  - b14 - b18 + b147 <= 0;

e1764:  - b15 - b16 + b148 <= 0;

e1765:  - b15 - b17 + b149 <= 0;

e1766:  - b15 - b18 + b150 <= 0;

e1767:  - b16 - b17 + b151 <= 0;

e1768:  - b16 - b18 + b152 <= 0;

e1769:  - b17 - b18 + b153 <= 0;

e1770:  - b19 + b34 - b154 <= 0;

e1771:  - b19 - b20 + b35 <= 0;

e1772:  - b19 - b21 + b36 <= 0;

e1773:  - b19 - b22 + b37 <= 0;

e1774:  - b19 - b23 + b38 <= 0;

e1775:  - b19 - b24 + b39 <= 0;

e1776:  - b19 - b25 + b40 <= 0;

e1777:  - b19 - b26 + b41 <= 0;

e1778:  - b19 - b27 + b42 <= 0;

e1779:  - b19 - b28 + b43 <= 0;

e1780:  - b19 - b29 + b44 <= 0;

e1781:  - b19 - b30 + b45 <= 0;

e1782:  - b19 - b31 + b46 <= 0;

e1783:  - b19 - b32 + b47 <= 0;

e1784:  - b19 - b33 + b48 <= 0;

e1785:  - b20 + b49 - b154 <= 0;

e1786:  - b21 + b50 - b154 <= 0;

e1787:  - b22 + b51 - b154 <= 0;

e1788:  - b23 + b52 - b154 <= 0;

e1789:  - b24 + b53 - b154 <= 0;

e1790:  - b25 + b54 - b154 <= 0;

e1791:  - b26 + b55 - b154 <= 0;

e1792:  - b27 + b56 - b154 <= 0;

e1793:  - b28 + b57 - b154 <= 0;

e1794:  - b29 + b58 - b154 <= 0;

e1795:  - b30 + b59 - b154 <= 0;

e1796:  - b31 + b60 - b154 <= 0;

e1797:  - b32 + b61 - b154 <= 0;

e1798:  - b33 + b62 - b154 <= 0;

e1799:  - b20 - b21 + b63 <= 0;

e1800:  - b20 - b22 + b64 <= 0;

e1801:  - b20 - b23 + b65 <= 0;

e1802:  - b20 - b24 + b66 <= 0;

e1803:  - b20 - b25 + b67 <= 0;

e1804:  - b20 - b26 + b68 <= 0;

e1805:  - b20 - b27 + b69 <= 0;

e1806:  - b20 - b28 + b70 <= 0;

e1807:  - b20 - b29 + b71 <= 0;

e1808:  - b20 - b30 + b72 <= 0;

e1809:  - b20 - b31 + b73 <= 0;

e1810:  - b20 - b32 + b74 <= 0;

e1811:  - b20 - b33 + b75 <= 0;

e1812:  - b21 - b22 + b76 <= 0;

e1813:  - b21 - b23 + b77 <= 0;

e1814:  - b21 - b24 + b78 <= 0;

e1815:  - b21 - b25 + b79 <= 0;

e1816:  - b21 - b26 + b80 <= 0;

e1817:  - b21 - b27 + b81 <= 0;

e1818:  - b21 - b28 + b82 <= 0;

e1819:  - b21 - b29 + b83 <= 0;

e1820:  - b21 - b30 + b84 <= 0;

e1821:  - b21 - b31 + b85 <= 0;

e1822:  - b21 - b32 + b86 <= 0;

e1823:  - b21 - b33 + b87 <= 0;

e1824:  - b22 - b23 + b88 <= 0;

e1825:  - b22 - b24 + b89 <= 0;

e1826:  - b22 - b25 + b90 <= 0;

e1827:  - b22 - b26 + b91 <= 0;

e1828:  - b22 - b27 + b92 <= 0;

e1829:  - b22 - b28 + b93 <= 0;

e1830:  - b22 - b29 + b94 <= 0;

e1831:  - b22 - b30 + b95 <= 0;

e1832:  - b22 - b31 + b96 <= 0;

e1833:  - b22 - b32 + b97 <= 0;

e1834:  - b22 - b33 + b98 <= 0;

e1835:  - b23 - b24 + b99 <= 0;

e1836:  - b23 - b25 + b100 <= 0;

e1837:  - b23 - b26 + b101 <= 0;

e1838:  - b23 - b27 + b102 <= 0;

e1839:  - b23 - b28 + b103 <= 0;

e1840:  - b23 - b29 + b104 <= 0;

e1841:  - b23 - b30 + b105 <= 0;

e1842:  - b23 - b31 + b106 <= 0;

e1843:  - b23 - b32 + b107 <= 0;

e1844:  - b23 - b33 + b108 <= 0;

e1845:  - b24 - b25 + b109 <= 0;

e1846:  - b24 - b26 + b110 <= 0;

e1847:  - b24 - b27 + b111 <= 0;

e1848:  - b24 - b28 + b112 <= 0;

e1849:  - b24 - b29 + b113 <= 0;

e1850:  - b24 - b30 + b114 <= 0;

e1851:  - b24 - b31 + b115 <= 0;

e1852:  - b24 - b32 + b116 <= 0;

e1853:  - b24 - b33 + b117 <= 0;

e1854:  - b25 - b26 + b118 <= 0;

e1855:  - b25 - b27 + b119 <= 0;

e1856:  - b25 - b28 + b120 <= 0;

e1857:  - b25 - b29 + b121 <= 0;

e1858:  - b25 - b30 + b122 <= 0;

e1859:  - b25 - b31 + b123 <= 0;

e1860:  - b25 - b32 + b124 <= 0;

e1861:  - b25 - b33 + b125 <= 0;

e1862:  - b26 - b27 + b126 <= 0;

e1863:  - b26 - b28 + b127 <= 0;

e1864:  - b26 - b29 + b128 <= 0;

e1865:  - b26 - b30 + b129 <= 0;

e1866:  - b26 - b31 + b130 <= 0;

e1867:  - b26 - b32 + b131 <= 0;

e1868:  - b26 - b33 + b132 <= 0;

e1869:  - b27 - b28 + b133 <= 0;

e1870:  - b27 - b29 + b134 <= 0;

e1871:  - b27 - b30 + b135 <= 0;

e1872:  - b27 - b31 + b136 <= 0;

e1873:  - b27 - b32 + b137 <= 0;

e1874:  - b27 - b33 + b138 <= 0;

e1875:  - b28 - b29 + b139 <= 0;

e1876:  - b28 - b30 + b140 <= 0;

e1877:  - b28 - b31 + b141 <= 0;

e1878:  - b28 - b32 + b142 <= 0;

e1879:  - b28 - b33 + b143 <= 0;

e1880:  - b29 - b30 + b144 <= 0;

e1881:  - b29 - b31 + b145 <= 0;

e1882:  - b29 - b32 + b146 <= 0;

e1883:  - b29 - b33 + b147 <= 0;

e1884:  - b30 - b31 + b148 <= 0;

e1885:  - b30 - b32 + b149 <= 0;

e1886:  - b30 - b33 + b150 <= 0;

e1887:  - b31 - b32 + b151 <= 0;

e1888:  - b31 - b33 + b152 <= 0;

e1889:  - b32 - b33 + b153 <= 0;

e1890:  - b34 - b35 + b49 <= 0;

e1891:  - b34 - b36 + b50 <= 0;

e1892:  - b34 - b37 + b51 <= 0;

e1893:  - b34 - b38 + b52 <= 0;

e1894:  - b34 - b39 + b53 <= 0;

e1895:  - b34 - b40 + b54 <= 0;

e1896:  - b34 - b41 + b55 <= 0;

e1897:  - b34 - b42 + b56 <= 0;

e1898:  - b34 - b43 + b57 <= 0;

e1899:  - b34 - b44 + b58 <= 0;

e1900:  - b34 - b45 + b59 <= 0;

e1901:  - b34 - b46 + b60 <= 0;

e1902:  - b34 - b47 + b61 <= 0;

e1903:  - b34 - b48 + b62 <= 0;

e1904:  - b35 - b36 + b63 <= 0;

e1905:  - b35 - b37 + b64 <= 0;

e1906:  - b35 - b38 + b65 <= 0;

e1907:  - b35 - b39 + b66 <= 0;

e1908:  - b35 - b40 + b67 <= 0;

e1909:  - b35 - b41 + b68 <= 0;

e1910:  - b35 - b42 + b69 <= 0;

e1911:  - b35 - b43 + b70 <= 0;

e1912:  - b35 - b44 + b71 <= 0;

e1913:  - b35 - b45 + b72 <= 0;

e1914:  - b35 - b46 + b73 <= 0;

e1915:  - b35 - b47 + b74 <= 0;

e1916:  - b35 - b48 + b75 <= 0;

e1917:  - b36 - b37 + b76 <= 0;

e1918:  - b36 - b38 + b77 <= 0;

e1919:  - b36 - b39 + b78 <= 0;

e1920:  - b36 - b40 + b79 <= 0;

e1921:  - b36 - b41 + b80 <= 0;

e1922:  - b36 - b42 + b81 <= 0;

e1923:  - b36 - b43 + b82 <= 0;

e1924:  - b36 - b44 + b83 <= 0;

e1925:  - b36 - b45 + b84 <= 0;

e1926:  - b36 - b46 + b85 <= 0;

e1927:  - b36 - b47 + b86 <= 0;

e1928:  - b36 - b48 + b87 <= 0;

e1929:  - b37 - b38 + b88 <= 0;

e1930:  - b37 - b39 + b89 <= 0;

e1931:  - b37 - b40 + b90 <= 0;

e1932:  - b37 - b41 + b91 <= 0;

e1933:  - b37 - b42 + b92 <= 0;

e1934:  - b37 - b43 + b93 <= 0;

e1935:  - b37 - b44 + b94 <= 0;

e1936:  - b37 - b45 + b95 <= 0;

e1937:  - b37 - b46 + b96 <= 0;

e1938:  - b37 - b47 + b97 <= 0;

e1939:  - b37 - b48 + b98 <= 0;

e1940:  - b38 - b39 + b99 <= 0;

e1941:  - b38 - b40 + b100 <= 0;

e1942:  - b38 - b41 + b101 <= 0;

e1943:  - b38 - b42 + b102 <= 0;

e1944:  - b38 - b43 + b103 <= 0;

e1945:  - b38 - b44 + b104 <= 0;

e1946:  - b38 - b45 + b105 <= 0;

e1947:  - b38 - b46 + b106 <= 0;

e1948:  - b38 - b47 + b107 <= 0;

e1949:  - b38 - b48 + b108 <= 0;

e1950:  - b39 - b40 + b109 <= 0;

e1951:  - b39 - b41 + b110 <= 0;

e1952:  - b39 - b42 + b111 <= 0;

e1953:  - b39 - b43 + b112 <= 0;

e1954:  - b39 - b44 + b113 <= 0;

e1955:  - b39 - b45 + b114 <= 0;

e1956:  - b39 - b46 + b115 <= 0;

e1957:  - b39 - b47 + b116 <= 0;

e1958:  - b39 - b48 + b117 <= 0;

e1959:  - b40 - b41 + b118 <= 0;

e1960:  - b40 - b42 + b119 <= 0;

e1961:  - b40 - b43 + b120 <= 0;

e1962:  - b40 - b44 + b121 <= 0;

e1963:  - b40 - b45 + b122 <= 0;

e1964:  - b40 - b46 + b123 <= 0;

e1965:  - b40 - b47 + b124 <= 0;

e1966:  - b40 - b48 + b125 <= 0;

e1967:  - b41 - b42 + b126 <= 0;

e1968:  - b41 - b43 + b127 <= 0;

e1969:  - b41 - b44 + b128 <= 0;

e1970:  - b41 - b45 + b129 <= 0;

e1971:  - b41 - b46 + b130 <= 0;

e1972:  - b41 - b47 + b131 <= 0;

e1973:  - b41 - b48 + b132 <= 0;

e1974:  - b42 - b43 + b133 <= 0;

e1975:  - b42 - b44 + b134 <= 0;

e1976:  - b42 - b45 + b135 <= 0;

e1977:  - b42 - b46 + b136 <= 0;

e1978:  - b42 - b47 + b137 <= 0;

e1979:  - b42 - b48 + b138 <= 0;

e1980:  - b43 - b44 + b139 <= 0;

e1981:  - b43 - b45 + b140 <= 0;

e1982:  - b43 - b46 + b141 <= 0;

e1983:  - b43 - b47 + b142 <= 0;

e1984:  - b43 - b48 + b143 <= 0;

e1985:  - b44 - b45 + b144 <= 0;

e1986:  - b44 - b46 + b145 <= 0;

e1987:  - b44 - b47 + b146 <= 0;

e1988:  - b44 - b48 + b147 <= 0;

e1989:  - b45 - b46 + b148 <= 0;

e1990:  - b45 - b47 + b149 <= 0;

e1991:  - b45 - b48 + b150 <= 0;

e1992:  - b46 - b47 + b151 <= 0;

e1993:  - b46 - b48 + b152 <= 0;

e1994:  - b47 - b48 + b153 <= 0;

e1995:  - b49 - b50 + b63 <= 0;

e1996:  - b49 - b51 + b64 <= 0;

e1997:  - b49 - b52 + b65 <= 0;

e1998:  - b49 - b53 + b66 <= 0;

e1999:  - b49 - b54 + b67 <= 0;

e2000:  - b49 - b55 + b68 <= 0;

e2001:  - b49 - b56 + b69 <= 0;

e2002:  - b49 - b57 + b70 <= 0;

e2003:  - b49 - b58 + b71 <= 0;

e2004:  - b49 - b59 + b72 <= 0;

e2005:  - b49 - b60 + b73 <= 0;

e2006:  - b49 - b61 + b74 <= 0;

e2007:  - b49 - b62 + b75 <= 0;

e2008:  - b50 - b51 + b76 <= 0;

e2009:  - b50 - b52 + b77 <= 0;

e2010:  - b50 - b53 + b78 <= 0;

e2011:  - b50 - b54 + b79 <= 0;

e2012:  - b50 - b55 + b80 <= 0;

e2013:  - b50 - b56 + b81 <= 0;

e2014:  - b50 - b57 + b82 <= 0;

e2015:  - b50 - b58 + b83 <= 0;

e2016:  - b50 - b59 + b84 <= 0;

e2017:  - b50 - b60 + b85 <= 0;

e2018:  - b50 - b61 + b86 <= 0;

e2019:  - b50 - b62 + b87 <= 0;

e2020:  - b51 - b52 + b88 <= 0;

e2021:  - b51 - b53 + b89 <= 0;

e2022:  - b51 - b54 + b90 <= 0;

e2023:  - b51 - b55 + b91 <= 0;

e2024:  - b51 - b56 + b92 <= 0;

e2025:  - b51 - b57 + b93 <= 0;

e2026:  - b51 - b58 + b94 <= 0;

e2027:  - b51 - b59 + b95 <= 0;

e2028:  - b51 - b60 + b96 <= 0;

e2029:  - b51 - b61 + b97 <= 0;

e2030:  - b51 - b62 + b98 <= 0;

e2031:  - b52 - b53 + b99 <= 0;

e2032:  - b52 - b54 + b100 <= 0;

e2033:  - b52 - b55 + b101 <= 0;

e2034:  - b52 - b56 + b102 <= 0;

e2035:  - b52 - b57 + b103 <= 0;

e2036:  - b52 - b58 + b104 <= 0;

e2037:  - b52 - b59 + b105 <= 0;

e2038:  - b52 - b60 + b106 <= 0;

e2039:  - b52 - b61 + b107 <= 0;

e2040:  - b52 - b62 + b108 <= 0;

e2041:  - b53 - b54 + b109 <= 0;

e2042:  - b53 - b55 + b110 <= 0;

e2043:  - b53 - b56 + b111 <= 0;

e2044:  - b53 - b57 + b112 <= 0;

e2045:  - b53 - b58 + b113 <= 0;

e2046:  - b53 - b59 + b114 <= 0;

e2047:  - b53 - b60 + b115 <= 0;

e2048:  - b53 - b61 + b116 <= 0;

e2049:  - b53 - b62 + b117 <= 0;

e2050:  - b54 - b55 + b118 <= 0;

e2051:  - b54 - b56 + b119 <= 0;

e2052:  - b54 - b57 + b120 <= 0;

e2053:  - b54 - b58 + b121 <= 0;

e2054:  - b54 - b59 + b122 <= 0;

e2055:  - b54 - b60 + b123 <= 0;

e2056:  - b54 - b61 + b124 <= 0;

e2057:  - b54 - b62 + b125 <= 0;

e2058:  - b55 - b56 + b126 <= 0;

e2059:  - b55 - b57 + b127 <= 0;

e2060:  - b55 - b58 + b128 <= 0;

e2061:  - b55 - b59 + b129 <= 0;

e2062:  - b55 - b60 + b130 <= 0;

e2063:  - b55 - b61 + b131 <= 0;

e2064:  - b55 - b62 + b132 <= 0;

e2065:  - b56 - b57 + b133 <= 0;

e2066:  - b56 - b58 + b134 <= 0;

e2067:  - b56 - b59 + b135 <= 0;

e2068:  - b56 - b60 + b136 <= 0;

e2069:  - b56 - b61 + b137 <= 0;

e2070:  - b56 - b62 + b138 <= 0;

e2071:  - b57 - b58 + b139 <= 0;

e2072:  - b57 - b59 + b140 <= 0;

e2073:  - b57 - b60 + b141 <= 0;

e2074:  - b57 - b61 + b142 <= 0;

e2075:  - b57 - b62 + b143 <= 0;

e2076:  - b58 - b59 + b144 <= 0;

e2077:  - b58 - b60 + b145 <= 0;

e2078:  - b58 - b61 + b146 <= 0;

e2079:  - b58 - b62 + b147 <= 0;

e2080:  - b59 - b60 + b148 <= 0;

e2081:  - b59 - b61 + b149 <= 0;

e2082:  - b59 - b62 + b150 <= 0;

e2083:  - b60 - b61 + b151 <= 0;

e2084:  - b60 - b62 + b152 <= 0;

e2085:  - b61 - b62 + b153 <= 0;

e2086:  - b63 - b64 + b76 <= 0;

e2087:  - b63 - b65 + b77 <= 0;

e2088:  - b63 - b66 + b78 <= 0;

e2089:  - b63 - b67 + b79 <= 0;

e2090:  - b63 - b68 + b80 <= 0;

e2091:  - b63 - b69 + b81 <= 0;

e2092:  - b63 - b70 + b82 <= 0;

e2093:  - b63 - b71 + b83 <= 0;

e2094:  - b63 - b72 + b84 <= 0;

e2095:  - b63 - b73 + b85 <= 0;

e2096:  - b63 - b74 + b86 <= 0;

e2097:  - b63 - b75 + b87 <= 0;

e2098:  - b64 - b65 + b88 <= 0;

e2099:  - b64 - b66 + b89 <= 0;

e2100:  - b64 - b67 + b90 <= 0;

e2101:  - b64 - b68 + b91 <= 0;

e2102:  - b64 - b69 + b92 <= 0;

e2103:  - b64 - b70 + b93 <= 0;

e2104:  - b64 - b71 + b94 <= 0;

e2105:  - b64 - b72 + b95 <= 0;

e2106:  - b64 - b73 + b96 <= 0;

e2107:  - b64 - b74 + b97 <= 0;

e2108:  - b64 - b75 + b98 <= 0;

e2109:  - b65 - b66 + b99 <= 0;

e2110:  - b65 - b67 + b100 <= 0;

e2111:  - b65 - b68 + b101 <= 0;

e2112:  - b65 - b69 + b102 <= 0;

e2113:  - b65 - b70 + b103 <= 0;

e2114:  - b65 - b71 + b104 <= 0;

e2115:  - b65 - b72 + b105 <= 0;

e2116:  - b65 - b73 + b106 <= 0;

e2117:  - b65 - b74 + b107 <= 0;

e2118:  - b65 - b75 + b108 <= 0;

e2119:  - b66 - b67 + b109 <= 0;

e2120:  - b66 - b68 + b110 <= 0;

e2121:  - b66 - b69 + b111 <= 0;

e2122:  - b66 - b70 + b112 <= 0;

e2123:  - b66 - b71 + b113 <= 0;

e2124:  - b66 - b72 + b114 <= 0;

e2125:  - b66 - b73 + b115 <= 0;

e2126:  - b66 - b74 + b116 <= 0;

e2127:  - b66 - b75 + b117 <= 0;

e2128:  - b67 - b68 + b118 <= 0;

e2129:  - b67 - b69 + b119 <= 0;

e2130:  - b67 - b70 + b120 <= 0;

e2131:  - b67 - b71 + b121 <= 0;

e2132:  - b67 - b72 + b122 <= 0;

e2133:  - b67 - b73 + b123 <= 0;

e2134:  - b67 - b74 + b124 <= 0;

e2135:  - b67 - b75 + b125 <= 0;

e2136:  - b68 - b69 + b126 <= 0;

e2137:  - b68 - b70 + b127 <= 0;

e2138:  - b68 - b71 + b128 <= 0;

e2139:  - b68 - b72 + b129 <= 0;

e2140:  - b68 - b73 + b130 <= 0;

e2141:  - b68 - b74 + b131 <= 0;

e2142:  - b68 - b75 + b132 <= 0;

e2143:  - b69 - b70 + b133 <= 0;

e2144:  - b69 - b71 + b134 <= 0;

e2145:  - b69 - b72 + b135 <= 0;

e2146:  - b69 - b73 + b136 <= 0;

e2147:  - b69 - b74 + b137 <= 0;

e2148:  - b69 - b75 + b138 <= 0;

e2149:  - b70 - b71 + b139 <= 0;

e2150:  - b70 - b72 + b140 <= 0;

e2151:  - b70 - b73 + b141 <= 0;

e2152:  - b70 - b74 + b142 <= 0;

e2153:  - b70 - b75 + b143 <= 0;

e2154:  - b71 - b72 + b144 <= 0;

e2155:  - b71 - b73 + b145 <= 0;

e2156:  - b71 - b74 + b146 <= 0;

e2157:  - b71 - b75 + b147 <= 0;

e2158:  - b72 - b73 + b148 <= 0;

e2159:  - b72 - b74 + b149 <= 0;

e2160:  - b72 - b75 + b150 <= 0;

e2161:  - b73 - b74 + b151 <= 0;

e2162:  - b73 - b75 + b152 <= 0;

e2163:  - b74 - b75 + b153 <= 0;

e2164:  - b76 - b77 + b88 <= 0;

e2165:  - b76 - b78 + b89 <= 0;

e2166:  - b76 - b79 + b90 <= 0;

e2167:  - b76 - b80 + b91 <= 0;

e2168:  - b76 - b81 + b92 <= 0;

e2169:  - b76 - b82 + b93 <= 0;

e2170:  - b76 - b83 + b94 <= 0;

e2171:  - b76 - b84 + b95 <= 0;

e2172:  - b76 - b85 + b96 <= 0;

e2173:  - b76 - b86 + b97 <= 0;

e2174:  - b76 - b87 + b98 <= 0;

e2175:  - b77 - b78 + b99 <= 0;

e2176:  - b77 - b79 + b100 <= 0;

e2177:  - b77 - b80 + b101 <= 0;

e2178:  - b77 - b81 + b102 <= 0;

e2179:  - b77 - b82 + b103 <= 0;

e2180:  - b77 - b83 + b104 <= 0;

e2181:  - b77 - b84 + b105 <= 0;

e2182:  - b77 - b85 + b106 <= 0;

e2183:  - b77 - b86 + b107 <= 0;

e2184:  - b77 - b87 + b108 <= 0;

e2185:  - b78 - b79 + b109 <= 0;

e2186:  - b78 - b80 + b110 <= 0;

e2187:  - b78 - b81 + b111 <= 0;

e2188:  - b78 - b82 + b112 <= 0;

e2189:  - b78 - b83 + b113 <= 0;

e2190:  - b78 - b84 + b114 <= 0;

e2191:  - b78 - b85 + b115 <= 0;

e2192:  - b78 - b86 + b116 <= 0;

e2193:  - b78 - b87 + b117 <= 0;

e2194:  - b79 - b80 + b118 <= 0;

e2195:  - b79 - b81 + b119 <= 0;

e2196:  - b79 - b82 + b120 <= 0;

e2197:  - b79 - b83 + b121 <= 0;

e2198:  - b79 - b84 + b122 <= 0;

e2199:  - b79 - b85 + b123 <= 0;

e2200:  - b79 - b86 + b124 <= 0;

e2201:  - b79 - b87 + b125 <= 0;

e2202:  - b80 - b81 + b126 <= 0;

e2203:  - b80 - b82 + b127 <= 0;

e2204:  - b80 - b83 + b128 <= 0;

e2205:  - b80 - b84 + b129 <= 0;

e2206:  - b80 - b85 + b130 <= 0;

e2207:  - b80 - b86 + b131 <= 0;

e2208:  - b80 - b87 + b132 <= 0;

e2209:  - b81 - b82 + b133 <= 0;

e2210:  - b81 - b83 + b134 <= 0;

e2211:  - b81 - b84 + b135 <= 0;

e2212:  - b81 - b85 + b136 <= 0;

e2213:  - b81 - b86 + b137 <= 0;

e2214:  - b81 - b87 + b138 <= 0;

e2215:  - b82 - b83 + b139 <= 0;

e2216:  - b82 - b84 + b140 <= 0;

e2217:  - b82 - b85 + b141 <= 0;

e2218:  - b82 - b86 + b142 <= 0;

e2219:  - b82 - b87 + b143 <= 0;

e2220:  - b83 - b84 + b144 <= 0;

e2221:  - b83 - b85 + b145 <= 0;

e2222:  - b83 - b86 + b146 <= 0;

e2223:  - b83 - b87 + b147 <= 0;

e2224:  - b84 - b85 + b148 <= 0;

e2225:  - b84 - b86 + b149 <= 0;

e2226:  - b84 - b87 + b150 <= 0;

e2227:  - b85 - b86 + b151 <= 0;

e2228:  - b85 - b87 + b152 <= 0;

e2229:  - b86 - b87 + b153 <= 0;

e2230:  - b88 - b89 + b99 <= 0;

e2231:  - b88 - b90 + b100 <= 0;

e2232:  - b88 - b91 + b101 <= 0;

e2233:  - b88 - b92 + b102 <= 0;

e2234:  - b88 - b93 + b103 <= 0;

e2235:  - b88 - b94 + b104 <= 0;

e2236:  - b88 - b95 + b105 <= 0;

e2237:  - b88 - b96 + b106 <= 0;

e2238:  - b88 - b97 + b107 <= 0;

e2239:  - b88 - b98 + b108 <= 0;

e2240:  - b89 - b90 + b109 <= 0;

e2241:  - b89 - b91 + b110 <= 0;

e2242:  - b89 - b92 + b111 <= 0;

e2243:  - b89 - b93 + b112 <= 0;

e2244:  - b89 - b94 + b113 <= 0;

e2245:  - b89 - b95 + b114 <= 0;

e2246:  - b89 - b96 + b115 <= 0;

e2247:  - b89 - b97 + b116 <= 0;

e2248:  - b89 - b98 + b117 <= 0;

e2249:  - b90 - b91 + b118 <= 0;

e2250:  - b90 - b92 + b119 <= 0;

e2251:  - b90 - b93 + b120 <= 0;

e2252:  - b90 - b94 + b121 <= 0;

e2253:  - b90 - b95 + b122 <= 0;

e2254:  - b90 - b96 + b123 <= 0;

e2255:  - b90 - b97 + b124 <= 0;

e2256:  - b90 - b98 + b125 <= 0;

e2257:  - b91 - b92 + b126 <= 0;

e2258:  - b91 - b93 + b127 <= 0;

e2259:  - b91 - b94 + b128 <= 0;

e2260:  - b91 - b95 + b129 <= 0;

e2261:  - b91 - b96 + b130 <= 0;

e2262:  - b91 - b97 + b131 <= 0;

e2263:  - b91 - b98 + b132 <= 0;

e2264:  - b92 - b93 + b133 <= 0;

e2265:  - b92 - b94 + b134 <= 0;

e2266:  - b92 - b95 + b135 <= 0;

e2267:  - b92 - b96 + b136 <= 0;

e2268:  - b92 - b97 + b137 <= 0;

e2269:  - b92 - b98 + b138 <= 0;

e2270:  - b93 - b94 + b139 <= 0;

e2271:  - b93 - b95 + b140 <= 0;

e2272:  - b93 - b96 + b141 <= 0;

e2273:  - b93 - b97 + b142 <= 0;

e2274:  - b93 - b98 + b143 <= 0;

e2275:  - b94 - b95 + b144 <= 0;

e2276:  - b94 - b96 + b145 <= 0;

e2277:  - b94 - b97 + b146 <= 0;

e2278:  - b94 - b98 + b147 <= 0;

e2279:  - b95 - b96 + b148 <= 0;

e2280:  - b95 - b97 + b149 <= 0;

e2281:  - b95 - b98 + b150 <= 0;

e2282:  - b96 - b97 + b151 <= 0;

e2283:  - b96 - b98 + b152 <= 0;

e2284:  - b97 - b98 + b153 <= 0;

e2285:  - b99 - b100 + b109 <= 0;

e2286:  - b99 - b101 + b110 <= 0;

e2287:  - b99 - b102 + b111 <= 0;

e2288:  - b99 - b103 + b112 <= 0;

e2289:  - b99 - b104 + b113 <= 0;

e2290:  - b99 - b105 + b114 <= 0;

e2291:  - b99 - b106 + b115 <= 0;

e2292:  - b99 - b107 + b116 <= 0;

e2293:  - b99 - b108 + b117 <= 0;

e2294:  - b100 - b101 + b118 <= 0;

e2295:  - b100 - b102 + b119 <= 0;

e2296:  - b100 - b103 + b120 <= 0;

e2297:  - b100 - b104 + b121 <= 0;

e2298:  - b100 - b105 + b122 <= 0;

e2299:  - b100 - b106 + b123 <= 0;

e2300:  - b100 - b107 + b124 <= 0;

e2301:  - b100 - b108 + b125 <= 0;

e2302:  - b101 - b102 + b126 <= 0;

e2303:  - b101 - b103 + b127 <= 0;

e2304:  - b101 - b104 + b128 <= 0;

e2305:  - b101 - b105 + b129 <= 0;

e2306:  - b101 - b106 + b130 <= 0;

e2307:  - b101 - b107 + b131 <= 0;

e2308:  - b101 - b108 + b132 <= 0;

e2309:  - b102 - b103 + b133 <= 0;

e2310:  - b102 - b104 + b134 <= 0;

e2311:  - b102 - b105 + b135 <= 0;

e2312:  - b102 - b106 + b136 <= 0;

e2313:  - b102 - b107 + b137 <= 0;

e2314:  - b102 - b108 + b138 <= 0;

e2315:  - b103 - b104 + b139 <= 0;

e2316:  - b103 - b105 + b140 <= 0;

e2317:  - b103 - b106 + b141 <= 0;

e2318:  - b103 - b107 + b142 <= 0;

e2319:  - b103 - b108 + b143 <= 0;

e2320:  - b104 - b105 + b144 <= 0;

e2321:  - b104 - b106 + b145 <= 0;

e2322:  - b104 - b107 + b146 <= 0;

e2323:  - b104 - b108 + b147 <= 0;

e2324:  - b105 - b106 + b148 <= 0;

e2325:  - b105 - b107 + b149 <= 0;

e2326:  - b105 - b108 + b150 <= 0;

e2327:  - b106 - b107 + b151 <= 0;

e2328:  - b106 - b108 + b152 <= 0;

e2329:  - b107 - b108 + b153 <= 0;

e2330:  - b109 - b110 + b118 <= 0;

e2331:  - b109 - b111 + b119 <= 0;

e2332:  - b109 - b112 + b120 <= 0;

e2333:  - b109 - b113 + b121 <= 0;

e2334:  - b109 - b114 + b122 <= 0;

e2335:  - b109 - b115 + b123 <= 0;

e2336:  - b109 - b116 + b124 <= 0;

e2337:  - b109 - b117 + b125 <= 0;

e2338:  - b110 - b111 + b126 <= 0;

e2339:  - b110 - b112 + b127 <= 0;

e2340:  - b110 - b113 + b128 <= 0;

e2341:  - b110 - b114 + b129 <= 0;

e2342:  - b110 - b115 + b130 <= 0;

e2343:  - b110 - b116 + b131 <= 0;

e2344:  - b110 - b117 + b132 <= 0;

e2345:  - b111 - b112 + b133 <= 0;

e2346:  - b111 - b113 + b134 <= 0;

e2347:  - b111 - b114 + b135 <= 0;

e2348:  - b111 - b115 + b136 <= 0;

e2349:  - b111 - b116 + b137 <= 0;

e2350:  - b111 - b117 + b138 <= 0;

e2351:  - b112 - b113 + b139 <= 0;

e2352:  - b112 - b114 + b140 <= 0;

e2353:  - b112 - b115 + b141 <= 0;

e2354:  - b112 - b116 + b142 <= 0;

e2355:  - b112 - b117 + b143 <= 0;

e2356:  - b113 - b114 + b144 <= 0;

e2357:  - b113 - b115 + b145 <= 0;

e2358:  - b113 - b116 + b146 <= 0;

e2359:  - b113 - b117 + b147 <= 0;

e2360:  - b114 - b115 + b148 <= 0;

e2361:  - b114 - b116 + b149 <= 0;

e2362:  - b114 - b117 + b150 <= 0;

e2363:  - b115 - b116 + b151 <= 0;

e2364:  - b115 - b117 + b152 <= 0;

e2365:  - b116 - b117 + b153 <= 0;

e2366:  - b118 - b119 + b126 <= 0;

e2367:  - b118 - b120 + b127 <= 0;

e2368:  - b118 - b121 + b128 <= 0;

e2369:  - b118 - b122 + b129 <= 0;

e2370:  - b118 - b123 + b130 <= 0;

e2371:  - b118 - b124 + b131 <= 0;

e2372:  - b118 - b125 + b132 <= 0;

e2373:  - b119 - b120 + b133 <= 0;

e2374:  - b119 - b121 + b134 <= 0;

e2375:  - b119 - b122 + b135 <= 0;

e2376:  - b119 - b123 + b136 <= 0;

e2377:  - b119 - b124 + b137 <= 0;

e2378:  - b119 - b125 + b138 <= 0;

e2379:  - b120 - b121 + b139 <= 0;

e2380:  - b120 - b122 + b140 <= 0;

e2381:  - b120 - b123 + b141 <= 0;

e2382:  - b120 - b124 + b142 <= 0;

e2383:  - b120 - b125 + b143 <= 0;

e2384:  - b121 - b122 + b144 <= 0;

e2385:  - b121 - b123 + b145 <= 0;

e2386:  - b121 - b124 + b146 <= 0;

e2387:  - b121 - b125 + b147 <= 0;

e2388:  - b122 - b123 + b148 <= 0;

e2389:  - b122 - b124 + b149 <= 0;

e2390:  - b122 - b125 + b150 <= 0;

e2391:  - b123 - b124 + b151 <= 0;

e2392:  - b123 - b125 + b152 <= 0;

e2393:  - b124 - b125 + b153 <= 0;

e2394:  - b126 - b127 + b133 <= 0;

e2395:  - b126 - b128 + b134 <= 0;

e2396:  - b126 - b129 + b135 <= 0;

e2397:  - b126 - b130 + b136 <= 0;

e2398:  - b126 - b131 + b137 <= 0;

e2399:  - b126 - b132 + b138 <= 0;

e2400:  - b127 - b128 + b139 <= 0;

e2401:  - b127 - b129 + b140 <= 0;

e2402:  - b127 - b130 + b141 <= 0;

e2403:  - b127 - b131 + b142 <= 0;

e2404:  - b127 - b132 + b143 <= 0;

e2405:  - b128 - b129 + b144 <= 0;

e2406:  - b128 - b130 + b145 <= 0;

e2407:  - b128 - b131 + b146 <= 0;

e2408:  - b128 - b132 + b147 <= 0;

e2409:  - b129 - b130 + b148 <= 0;

e2410:  - b129 - b131 + b149 <= 0;

e2411:  - b129 - b132 + b150 <= 0;

e2412:  - b130 - b131 + b151 <= 0;

e2413:  - b130 - b132 + b152 <= 0;

e2414:  - b131 - b132 + b153 <= 0;

e2415:  - b133 - b134 + b139 <= 0;

e2416:  - b133 - b135 + b140 <= 0;

e2417:  - b133 - b136 + b141 <= 0;

e2418:  - b133 - b137 + b142 <= 0;

e2419:  - b133 - b138 + b143 <= 0;

e2420:  - b134 - b135 + b144 <= 0;

e2421:  - b134 - b136 + b145 <= 0;

e2422:  - b134 - b137 + b146 <= 0;

e2423:  - b134 - b138 + b147 <= 0;

e2424:  - b135 - b136 + b148 <= 0;

e2425:  - b135 - b137 + b149 <= 0;

e2426:  - b135 - b138 + b150 <= 0;

e2427:  - b136 - b137 + b151 <= 0;

e2428:  - b136 - b138 + b152 <= 0;

e2429:  - b137 - b138 + b153 <= 0;

e2430:  - b139 - b140 + b144 <= 0;

e2431:  - b139 - b141 + b145 <= 0;

e2432:  - b139 - b142 + b146 <= 0;

e2433:  - b139 - b143 + b147 <= 0;

e2434:  - b140 - b141 + b148 <= 0;

e2435:  - b140 - b142 + b149 <= 0;

e2436:  - b140 - b143 + b150 <= 0;

e2437:  - b141 - b142 + b151 <= 0;

e2438:  - b141 - b143 + b152 <= 0;

e2439:  - b142 - b143 + b153 <= 0;

e2440:  - b144 - b145 + b148 <= 0;

e2441:  - b144 - b146 + b149 <= 0;

e2442:  - b144 - b147 + b150 <= 0;

e2443:  - b145 - b146 + b151 <= 0;

e2444:  - b145 - b147 + b152 <= 0;

e2445:  - b146 - b147 + b153 <= 0;

e2446:  - b148 - b149 + b151 <= 0;

e2447:  - b148 - b150 + b152 <= 0;

e2448:  - b149 - b150 + b153 <= 0;

e2449:  - b151 - b152 + b153 <= 0;

e2450: 90*b3*b2 + 780*b5*b2 + 100*b6*b2 + 400*b7*b2 + 40*b8*b2 + 660*b9*b2 + 
       740*b10*b2 + 760*b11*b2 + 190*b12*b2 + 540*b13*b2 + 470*b14*b2 + 750*b15
       *b2 + 30*b16*b2 + 490*b17*b2 + 530*b18*b2 + 860*b4*b3 + 300*b5*b3 + 260*
       b6*b3 + 880*b7*b3 + 290*b8*b3 + 260*b9*b3 + 960*b10*b3 + 450*b11*b3 + 
       110*b12*b3 + 800*b13*b3 + 980*b14*b3 + 270*b15*b3 + 150*b16*b3 + 140*b17
       *b3 + 690*b18*b3 + 760*b5*b4 + 140*b6*b4 + 470*b7*b4 + 380*b8*b4 + 60*b9
       *b4 + 510*b10*b4 + 560*b11*b4 + 320*b12*b4 + 790*b13*b4 + 750*b14*b4 + 
       390*b15*b4 + 260*b16*b4 + 20*b17*b4 + 940*b18*b4 + 760*b6*b5 + 550*b7*b5
        + 800*b8*b5 + 580*b9*b5 + 340*b10*b5 + 200*b11*b5 + 880*b12*b5 + 600*
       b13*b5 + 170*b14*b5 + 850*b15*b5 + 710*b16*b5 + 970*b17*b5 + 830*b18*b5
        + 990*b7*b6 + 640*b8*b6 + 970*b9*b6 + 680*b10*b6 + 410*b11*b6 + 630*b12
       *b6 + 670*b13*b6 + 310*b14*b6 + 210*b15*b6 + 710*b16*b6 + 880*b17*b6 + 
       530*b18*b6 + 500*b8*b7 + 630*b9*b7 + 920*b10*b7 + 290*b11*b7 + 180*b12*
       b7 + 860*b13*b7 + 570*b14*b7 + 730*b15*b7 + 180*b16*b7 + 150*b17*b7 + 
       590*b18*b7 + 390*b9*b8 + 30*b10*b8 + 190*b11*b8 + 80*b12*b8 + 880*b13*b8
        + 430*b14*b8 + 570*b15*b8 + 230*b16*b8 + 940*b17*b8 + 210*b18*b8 + 720*
       b10*b9 + 140*b11*b9 + 140*b12*b9 + 870*b13*b9 + 330*b14*b9 + 460*b15*b9
        + 80*b16*b9 + 40*b17*b9 + 340*b18*b9 + 620*b11*b10 + 550*b12*b10 + 490*
       b13*b10 + 60*b14*b10 + 360*b15*b10 + 670*b16*b10 + 450*b17*b10 + 930*b18
       *b10 + 930*b12*b11 + 630*b13*b11 + 80*b14*b11 + 520*b15*b11 + 540*b16*
       b11 + 640*b17*b11 + 240*b18*b11 + 140*b13*b12 + 40*b14*b12 + 190*b15*b12
        + 710*b16*b12 + 280*b17*b12 + 130*b18*b12 + 450*b14*b13 + 520*b15*b13
        + 790*b16*b13 + 110*b17*b13 + 400*b18*b13 + 120*b15*b14 + 570*b16*b14
        + 480*b17*b14 + 170*b18*b14 + 430*b16*b15 + 620*b17*b15 + 240*b18*b15
        + 450*b17*b16 + 210*b18*b16 + 600*b18*b17 >= 23348;

e2451: 260*b19*b2 + 290*b20*b2 + 730*b21*b2 + 500*b22*b2 + 470*b23*b2 + 470*b24
       *b2 + 560*b25*b2 + 150*b26*b2 + 850*b27*b2 + 830*b28*b2 + 530*b29*b2 + 
       640*b30*b2 + 350*b31*b2 + 640*b32*b2 + 890*b33*b2 + 310*b154*b2 + 300*
       b20*b19 + 260*b21*b19 + 880*b22*b19 + 290*b23*b19 + 260*b24*b19 + 960*
       b25*b19 + 450*b26*b19 + 110*b27*b19 + 800*b28*b19 + 980*b29*b19 + 270*
       b30*b19 + 150*b31*b19 + 140*b32*b19 + 690*b33*b19 + 860*b154*b19 + 760*
       b21*b20 + 550*b22*b20 + 800*b23*b20 + 580*b24*b20 + 340*b25*b20 + 200*
       b26*b20 + 880*b27*b20 + 600*b28*b20 + 170*b29*b20 + 850*b30*b20 + 710*
       b31*b20 + 970*b32*b20 + 830*b33*b20 + 760*b154*b20 + 990*b22*b21 + 640*
       b23*b21 + 970*b24*b21 + 680*b25*b21 + 410*b26*b21 + 630*b27*b21 + 670*
       b28*b21 + 310*b29*b21 + 210*b30*b21 + 710*b31*b21 + 880*b32*b21 + 530*
       b33*b21 + 140*b154*b21 + 500*b23*b22 + 630*b24*b22 + 920*b25*b22 + 290*
       b26*b22 + 180*b27*b22 + 860*b28*b22 + 570*b29*b22 + 730*b30*b22 + 180*
       b31*b22 + 150*b32*b22 + 590*b33*b22 + 470*b154*b22 + 390*b24*b23 + 30*
       b25*b23 + 190*b26*b23 + 80*b27*b23 + 880*b28*b23 + 430*b29*b23 + 570*b30
       *b23 + 230*b31*b23 + 940*b32*b23 + 210*b33*b23 + 380*b154*b23 + 720*b25*
       b24 + 140*b26*b24 + 140*b27*b24 + 870*b28*b24 + 330*b29*b24 + 460*b30*
       b24 + 80*b31*b24 + 40*b32*b24 + 340*b33*b24 + 60*b154*b24 + 620*b26*b25
        + 550*b27*b25 + 490*b28*b25 + 60*b29*b25 + 360*b30*b25 + 670*b31*b25 + 
       450*b32*b25 + 930*b33*b25 + 510*b154*b25 + 930*b27*b26 + 630*b28*b26 + 
       80*b29*b26 + 520*b30*b26 + 540*b31*b26 + 640*b32*b26 + 240*b33*b26 + 560
       *b154*b26 + 140*b28*b27 + 40*b29*b27 + 190*b30*b27 + 710*b31*b27 + 280*
       b32*b27 + 130*b33*b27 + 320*b154*b27 + 450*b29*b28 + 520*b30*b28 + 790*
       b31*b28 + 110*b32*b28 + 400*b33*b28 + 790*b154*b28 + 120*b30*b29 + 570*
       b31*b29 + 480*b32*b29 + 170*b33*b29 + 750*b154*b29 + 430*b31*b30 + 620*
       b32*b30 + 240*b33*b30 + 390*b154*b30 + 450*b32*b31 + 210*b33*b31 + 260*
       b154*b31 + 600*b33*b32 + 20*b154*b32 + 940*b154*b33 >= 23348;

e2452: 20*b19*b3 + 310*b34*b3 + 290*b35*b3 + 730*b36*b3 + 500*b37*b3 + 470*b38*
       b3 + 470*b39*b3 + 560*b40*b3 + 150*b41*b3 + 850*b42*b3 + 830*b43*b3 + 
       530*b44*b3 + 640*b45*b3 + 350*b46*b3 + 640*b47*b3 + 890*b48*b3 + 780*b35
       *b19 + 100*b36*b19 + 400*b37*b19 + 40*b38*b19 + 660*b39*b19 + 740*b40*
       b19 + 760*b41*b19 + 190*b42*b19 + 540*b43*b19 + 470*b44*b19 + 750*b45*
       b19 + 30*b46*b19 + 490*b47*b19 + 530*b48*b19 + 760*b35*b34 + 140*b36*b34
        + 470*b37*b34 + 380*b38*b34 + 60*b39*b34 + 510*b40*b34 + 560*b41*b34 + 
       320*b42*b34 + 790*b43*b34 + 750*b44*b34 + 390*b45*b34 + 260*b46*b34 + 20
       *b47*b34 + 940*b48*b34 + 760*b36*b35 + 550*b37*b35 + 800*b38*b35 + 580*
       b39*b35 + 340*b40*b35 + 200*b41*b35 + 880*b42*b35 + 600*b43*b35 + 170*
       b44*b35 + 850*b45*b35 + 710*b46*b35 + 970*b47*b35 + 830*b48*b35 + 990*
       b37*b36 + 640*b38*b36 + 970*b39*b36 + 680*b40*b36 + 410*b41*b36 + 630*
       b42*b36 + 670*b43*b36 + 310*b44*b36 + 210*b45*b36 + 710*b46*b36 + 880*
       b47*b36 + 530*b48*b36 + 500*b38*b37 + 630*b39*b37 + 920*b40*b37 + 290*
       b41*b37 + 180*b42*b37 + 860*b43*b37 + 570*b44*b37 + 730*b45*b37 + 180*
       b46*b37 + 150*b47*b37 + 590*b48*b37 + 390*b39*b38 + 30*b40*b38 + 190*b41
       *b38 + 80*b42*b38 + 880*b43*b38 + 430*b44*b38 + 570*b45*b38 + 230*b46*
       b38 + 940*b47*b38 + 210*b48*b38 + 720*b40*b39 + 140*b41*b39 + 140*b42*
       b39 + 870*b43*b39 + 330*b44*b39 + 460*b45*b39 + 80*b46*b39 + 40*b47*b39
        + 340*b48*b39 + 620*b41*b40 + 550*b42*b40 + 490*b43*b40 + 60*b44*b40 + 
       360*b45*b40 + 670*b46*b40 + 450*b47*b40 + 930*b48*b40 + 930*b42*b41 + 
       630*b43*b41 + 80*b44*b41 + 520*b45*b41 + 540*b46*b41 + 640*b47*b41 + 240
       *b48*b41 + 140*b43*b42 + 40*b44*b42 + 190*b45*b42 + 710*b46*b42 + 280*
       b47*b42 + 130*b48*b42 + 450*b44*b43 + 520*b45*b43 + 790*b46*b43 + 110*
       b47*b43 + 400*b48*b43 + 120*b45*b44 + 570*b46*b44 + 480*b47*b44 + 170*
       b48*b44 + 430*b46*b45 + 620*b47*b45 + 240*b48*b45 + 450*b47*b46 + 210*
       b48*b46 + 600*b48*b47 >= 23348;

e2453: 260*b34*b4 + 290*b49*b4 + 730*b50*b4 + 500*b51*b4 + 470*b52*b4 + 470*b53
       *b4 + 560*b54*b4 + 150*b55*b4 + 850*b56*b4 + 830*b57*b4 + 530*b58*b4 + 
       640*b59*b4 + 350*b60*b4 + 640*b61*b4 + 890*b62*b4 + 20*b154*b4 + 300*b49
       *b34 + 260*b50*b34 + 880*b51*b34 + 290*b52*b34 + 260*b53*b34 + 960*b54*
       b34 + 450*b55*b34 + 110*b56*b34 + 800*b57*b34 + 980*b58*b34 + 270*b59*
       b34 + 150*b60*b34 + 140*b61*b34 + 690*b62*b34 + 90*b154*b34 + 760*b50*
       b49 + 550*b51*b49 + 800*b52*b49 + 580*b53*b49 + 340*b54*b49 + 200*b55*
       b49 + 880*b56*b49 + 600*b57*b49 + 170*b58*b49 + 850*b59*b49 + 710*b60*
       b49 + 970*b61*b49 + 830*b62*b49 + 780*b154*b49 + 990*b51*b50 + 640*b52*
       b50 + 970*b53*b50 + 680*b54*b50 + 410*b55*b50 + 630*b56*b50 + 670*b57*
       b50 + 310*b58*b50 + 210*b59*b50 + 710*b60*b50 + 880*b61*b50 + 530*b62*
       b50 + 100*b154*b50 + 500*b52*b51 + 630*b53*b51 + 920*b54*b51 + 290*b55*
       b51 + 180*b56*b51 + 860*b57*b51 + 570*b58*b51 + 730*b59*b51 + 180*b60*
       b51 + 150*b61*b51 + 590*b62*b51 + 400*b154*b51 + 390*b53*b52 + 30*b54*
       b52 + 190*b55*b52 + 80*b56*b52 + 880*b57*b52 + 430*b58*b52 + 570*b59*b52
        + 230*b60*b52 + 940*b61*b52 + 210*b62*b52 + 40*b154*b52 + 720*b54*b53
        + 140*b55*b53 + 140*b56*b53 + 870*b57*b53 + 330*b58*b53 + 460*b59*b53
        + 80*b60*b53 + 40*b61*b53 + 340*b62*b53 + 660*b154*b53 + 620*b55*b54 + 
       550*b56*b54 + 490*b57*b54 + 60*b58*b54 + 360*b59*b54 + 670*b60*b54 + 450
       *b61*b54 + 930*b62*b54 + 740*b154*b54 + 930*b56*b55 + 630*b57*b55 + 80*
       b58*b55 + 520*b59*b55 + 540*b60*b55 + 640*b61*b55 + 240*b62*b55 + 760*
       b154*b55 + 140*b57*b56 + 40*b58*b56 + 190*b59*b56 + 710*b60*b56 + 280*
       b61*b56 + 130*b62*b56 + 190*b154*b56 + 450*b58*b57 + 520*b59*b57 + 790*
       b60*b57 + 110*b61*b57 + 400*b62*b57 + 540*b154*b57 + 120*b59*b58 + 570*
       b60*b58 + 480*b61*b58 + 170*b62*b58 + 470*b154*b58 + 430*b60*b59 + 620*
       b61*b59 + 240*b62*b59 + 750*b154*b59 + 450*b61*b60 + 210*b62*b60 + 30*
       b154*b60 + 600*b62*b61 + 490*b154*b61 + 530*b154*b62 >= 23348;

e2454: 20*b20*b5 + 260*b35*b5 + 310*b49*b5 + 730*b63*b5 + 500*b64*b5 + 470*b65*
       b5 + 470*b66*b5 + 560*b67*b5 + 150*b68*b5 + 850*b69*b5 + 830*b70*b5 + 
       530*b71*b5 + 640*b72*b5 + 350*b73*b5 + 640*b74*b5 + 890*b75*b5 + 90*b35*
       b20 + 100*b63*b20 + 400*b64*b20 + 40*b65*b20 + 660*b66*b20 + 740*b67*b20
        + 760*b68*b20 + 190*b69*b20 + 540*b70*b20 + 470*b71*b20 + 750*b72*b20
        + 30*b73*b20 + 490*b74*b20 + 530*b75*b20 + 860*b49*b35 + 260*b63*b35 + 
       880*b64*b35 + 290*b65*b35 + 260*b66*b35 + 960*b67*b35 + 450*b68*b35 + 
       110*b69*b35 + 800*b70*b35 + 980*b71*b35 + 270*b72*b35 + 150*b73*b35 + 
       140*b74*b35 + 690*b75*b35 + 140*b63*b49 + 470*b64*b49 + 380*b65*b49 + 60
       *b66*b49 + 510*b67*b49 + 560*b68*b49 + 320*b69*b49 + 790*b70*b49 + 750*
       b71*b49 + 390*b72*b49 + 260*b73*b49 + 20*b74*b49 + 940*b75*b49 + 990*b64
       *b63 + 640*b65*b63 + 970*b66*b63 + 680*b67*b63 + 410*b68*b63 + 630*b69*
       b63 + 670*b70*b63 + 310*b71*b63 + 210*b72*b63 + 710*b73*b63 + 880*b74*
       b63 + 530*b75*b63 + 500*b65*b64 + 630*b66*b64 + 920*b67*b64 + 290*b68*
       b64 + 180*b69*b64 + 860*b70*b64 + 570*b71*b64 + 730*b72*b64 + 180*b73*
       b64 + 150*b74*b64 + 590*b75*b64 + 390*b66*b65 + 30*b67*b65 + 190*b68*b65
        + 80*b69*b65 + 880*b70*b65 + 430*b71*b65 + 570*b72*b65 + 230*b73*b65 + 
       940*b74*b65 + 210*b75*b65 + 720*b67*b66 + 140*b68*b66 + 140*b69*b66 + 
       870*b70*b66 + 330*b71*b66 + 460*b72*b66 + 80*b73*b66 + 40*b74*b66 + 340*
       b75*b66 + 620*b68*b67 + 550*b69*b67 + 490*b70*b67 + 60*b71*b67 + 360*b72
       *b67 + 670*b73*b67 + 450*b74*b67 + 930*b75*b67 + 930*b69*b68 + 630*b70*
       b68 + 80*b71*b68 + 520*b72*b68 + 540*b73*b68 + 640*b74*b68 + 240*b75*b68
        + 140*b70*b69 + 40*b71*b69 + 190*b72*b69 + 710*b73*b69 + 280*b74*b69 + 
       130*b75*b69 + 450*b71*b70 + 520*b72*b70 + 790*b73*b70 + 110*b74*b70 + 
       400*b75*b70 + 120*b72*b71 + 570*b73*b71 + 480*b74*b71 + 170*b75*b71 + 
       430*b73*b72 + 620*b74*b72 + 240*b75*b72 + 450*b74*b73 + 210*b75*b73 + 
       600*b75*b74 >= 23348;

e2455: 20*b21*b6 + 260*b36*b6 + 310*b50*b6 + 290*b63*b6 + 500*b76*b6 + 470*b77*
       b6 + 470*b78*b6 + 560*b79*b6 + 150*b80*b6 + 850*b81*b6 + 830*b82*b6 + 
       530*b83*b6 + 640*b84*b6 + 350*b85*b6 + 640*b86*b6 + 890*b87*b6 + 90*b36*
       b21 + 780*b63*b21 + 400*b76*b21 + 40*b77*b21 + 660*b78*b21 + 740*b79*b21
        + 760*b80*b21 + 190*b81*b21 + 540*b82*b21 + 470*b83*b21 + 750*b84*b21
        + 30*b85*b21 + 490*b86*b21 + 530*b87*b21 + 860*b50*b36 + 300*b63*b36 + 
       880*b76*b36 + 290*b77*b36 + 260*b78*b36 + 960*b79*b36 + 450*b80*b36 + 
       110*b81*b36 + 800*b82*b36 + 980*b83*b36 + 270*b84*b36 + 150*b85*b36 + 
       140*b86*b36 + 690*b87*b36 + 760*b63*b50 + 470*b76*b50 + 380*b77*b50 + 60
       *b78*b50 + 510*b79*b50 + 560*b80*b50 + 320*b81*b50 + 790*b82*b50 + 750*
       b83*b50 + 390*b84*b50 + 260*b85*b50 + 20*b86*b50 + 940*b87*b50 + 550*b76
       *b63 + 800*b77*b63 + 580*b78*b63 + 340*b79*b63 + 200*b80*b63 + 880*b81*
       b63 + 600*b82*b63 + 170*b83*b63 + 850*b84*b63 + 710*b85*b63 + 970*b86*
       b63 + 830*b87*b63 + 500*b77*b76 + 630*b78*b76 + 920*b79*b76 + 290*b80*
       b76 + 180*b81*b76 + 860*b82*b76 + 570*b83*b76 + 730*b84*b76 + 180*b85*
       b76 + 150*b86*b76 + 590*b87*b76 + 390*b78*b77 + 30*b79*b77 + 190*b80*b77
        + 80*b81*b77 + 880*b82*b77 + 430*b83*b77 + 570*b84*b77 + 230*b85*b77 + 
       940*b86*b77 + 210*b87*b77 + 720*b79*b78 + 140*b80*b78 + 140*b81*b78 + 
       870*b82*b78 + 330*b83*b78 + 460*b84*b78 + 80*b85*b78 + 40*b86*b78 + 340*
       b87*b78 + 620*b80*b79 + 550*b81*b79 + 490*b82*b79 + 60*b83*b79 + 360*b84
       *b79 + 670*b85*b79 + 450*b86*b79 + 930*b87*b79 + 930*b81*b80 + 630*b82*
       b80 + 80*b83*b80 + 520*b84*b80 + 540*b85*b80 + 640*b86*b80 + 240*b87*b80
        + 140*b82*b81 + 40*b83*b81 + 190*b84*b81 + 710*b85*b81 + 280*b86*b81 + 
       130*b87*b81 + 450*b83*b82 + 520*b84*b82 + 790*b85*b82 + 110*b86*b82 + 
       400*b87*b82 + 120*b84*b83 + 570*b85*b83 + 480*b86*b83 + 170*b87*b83 + 
       430*b85*b84 + 620*b86*b84 + 240*b87*b84 + 450*b86*b85 + 210*b87*b85 + 
       600*b87*b86 >= 23348;

e2456: 20*b22*b7 + 260*b37*b7 + 310*b51*b7 + 290*b64*b7 + 730*b76*b7 + 470*b88*
       b7 + 470*b89*b7 + 560*b90*b7 + 150*b91*b7 + 850*b92*b7 + 830*b93*b7 + 
       530*b94*b7 + 640*b95*b7 + 350*b96*b7 + 640*b97*b7 + 890*b98*b7 + 90*b37*
       b22 + 780*b64*b22 + 100*b76*b22 + 40*b88*b22 + 660*b89*b22 + 740*b90*b22
        + 760*b91*b22 + 190*b92*b22 + 540*b93*b22 + 470*b94*b22 + 750*b95*b22
        + 30*b96*b22 + 490*b97*b22 + 530*b98*b22 + 860*b51*b37 + 300*b64*b37 + 
       260*b76*b37 + 290*b88*b37 + 260*b89*b37 + 960*b90*b37 + 450*b91*b37 + 
       110*b92*b37 + 800*b93*b37 + 980*b94*b37 + 270*b95*b37 + 150*b96*b37 + 
       140*b97*b37 + 690*b98*b37 + 760*b64*b51 + 140*b76*b51 + 380*b88*b51 + 60
       *b89*b51 + 510*b90*b51 + 560*b91*b51 + 320*b92*b51 + 790*b93*b51 + 750*
       b94*b51 + 390*b95*b51 + 260*b96*b51 + 20*b97*b51 + 940*b98*b51 + 760*b76
       *b64 + 800*b88*b64 + 580*b89*b64 + 340*b90*b64 + 200*b91*b64 + 880*b92*
       b64 + 600*b93*b64 + 170*b94*b64 + 850*b95*b64 + 710*b96*b64 + 970*b97*
       b64 + 830*b98*b64 + 640*b88*b76 + 970*b89*b76 + 680*b90*b76 + 410*b91*
       b76 + 630*b92*b76 + 670*b93*b76 + 310*b94*b76 + 210*b95*b76 + 710*b96*
       b76 + 880*b97*b76 + 530*b98*b76 + 390*b89*b88 + 30*b90*b88 + 190*b91*b88
        + 80*b92*b88 + 880*b93*b88 + 430*b94*b88 + 570*b95*b88 + 230*b96*b88 + 
       940*b97*b88 + 210*b98*b88 + 720*b90*b89 + 140*b91*b89 + 140*b92*b89 + 
       870*b93*b89 + 330*b94*b89 + 460*b95*b89 + 80*b96*b89 + 40*b97*b89 + 340*
       b98*b89 + 620*b91*b90 + 550*b92*b90 + 490*b93*b90 + 60*b94*b90 + 360*b95
       *b90 + 670*b96*b90 + 450*b97*b90 + 930*b98*b90 + 930*b92*b91 + 630*b93*
       b91 + 80*b94*b91 + 520*b95*b91 + 540*b96*b91 + 640*b97*b91 + 240*b98*b91
        + 140*b93*b92 + 40*b94*b92 + 190*b95*b92 + 710*b96*b92 + 280*b97*b92 + 
       130*b98*b92 + 450*b94*b93 + 520*b95*b93 + 790*b96*b93 + 110*b97*b93 + 
       400*b98*b93 + 120*b95*b94 + 570*b96*b94 + 480*b97*b94 + 170*b98*b94 + 
       430*b96*b95 + 620*b97*b95 + 240*b98*b95 + 450*b97*b96 + 210*b98*b96 + 
       600*b98*b97 >= 23348;

e2457: 20*b23*b8 + 260*b38*b8 + 310*b52*b8 + 290*b65*b8 + 730*b77*b8 + 500*b88*
       b8 + 470*b99*b8 + 560*b100*b8 + 150*b101*b8 + 850*b102*b8 + 830*b103*b8
        + 530*b104*b8 + 640*b105*b8 + 350*b106*b8 + 640*b107*b8 + 890*b108*b8
        + 90*b38*b23 + 780*b65*b23 + 100*b77*b23 + 400*b88*b23 + 660*b99*b23 + 
       740*b100*b23 + 760*b101*b23 + 190*b102*b23 + 540*b103*b23 + 470*b104*b23
        + 750*b105*b23 + 30*b106*b23 + 490*b107*b23 + 530*b108*b23 + 860*b52*
       b38 + 300*b65*b38 + 260*b77*b38 + 880*b88*b38 + 260*b99*b38 + 960*b100*
       b38 + 450*b101*b38 + 110*b102*b38 + 800*b103*b38 + 980*b104*b38 + 270*
       b105*b38 + 150*b106*b38 + 140*b107*b38 + 690*b108*b38 + 760*b65*b52 + 
       140*b77*b52 + 470*b88*b52 + 60*b99*b52 + 510*b100*b52 + 560*b101*b52 + 
       320*b102*b52 + 790*b103*b52 + 750*b104*b52 + 390*b105*b52 + 260*b106*b52
        + 20*b107*b52 + 940*b108*b52 + 760*b77*b65 + 550*b88*b65 + 580*b99*b65
        + 340*b100*b65 + 200*b101*b65 + 880*b102*b65 + 600*b103*b65 + 170*b104*
       b65 + 850*b105*b65 + 710*b106*b65 + 970*b107*b65 + 830*b108*b65 + 990*
       b88*b77 + 970*b99*b77 + 680*b100*b77 + 410*b101*b77 + 630*b102*b77 + 670
       *b103*b77 + 310*b104*b77 + 210*b105*b77 + 710*b106*b77 + 880*b107*b77 + 
       530*b108*b77 + 630*b99*b88 + 920*b100*b88 + 290*b101*b88 + 180*b102*b88
        + 860*b103*b88 + 570*b104*b88 + 730*b105*b88 + 180*b106*b88 + 150*b107*
       b88 + 590*b108*b88 + 720*b100*b99 + 140*b101*b99 + 140*b102*b99 + 870*
       b103*b99 + 330*b104*b99 + 460*b105*b99 + 80*b106*b99 + 40*b107*b99 + 340
       *b108*b99 + 620*b101*b100 + 550*b102*b100 + 490*b103*b100 + 60*b104*b100
        + 360*b105*b100 + 670*b106*b100 + 450*b107*b100 + 930*b108*b100 + 930*
       b102*b101 + 630*b103*b101 + 80*b104*b101 + 520*b105*b101 + 540*b106*b101
        + 640*b107*b101 + 240*b108*b101 + 140*b103*b102 + 40*b104*b102 + 190*
       b105*b102 + 710*b106*b102 + 280*b107*b102 + 130*b108*b102 + 450*b104*
       b103 + 520*b105*b103 + 790*b106*b103 + 110*b107*b103 + 400*b108*b103 + 
       120*b105*b104 + 570*b106*b104 + 480*b107*b104 + 170*b108*b104 + 430*b106
       *b105 + 620*b107*b105 + 240*b108*b105 + 450*b107*b106 + 210*b108*b106 + 
       600*b108*b107 >= 23348;

e2458: 20*b24*b9 + 260*b39*b9 + 310*b53*b9 + 290*b66*b9 + 730*b78*b9 + 500*b89*
       b9 + 470*b99*b9 + 560*b109*b9 + 150*b110*b9 + 850*b111*b9 + 830*b112*b9
        + 530*b113*b9 + 640*b114*b9 + 350*b115*b9 + 640*b116*b9 + 890*b117*b9
        + 90*b39*b24 + 780*b66*b24 + 100*b78*b24 + 400*b89*b24 + 40*b99*b24 + 
       740*b109*b24 + 760*b110*b24 + 190*b111*b24 + 540*b112*b24 + 470*b113*b24
        + 750*b114*b24 + 30*b115*b24 + 490*b116*b24 + 530*b117*b24 + 860*b53*
       b39 + 300*b66*b39 + 260*b78*b39 + 880*b89*b39 + 290*b99*b39 + 960*b109*
       b39 + 450*b110*b39 + 110*b111*b39 + 800*b112*b39 + 980*b113*b39 + 270*
       b114*b39 + 150*b115*b39 + 140*b116*b39 + 690*b117*b39 + 760*b66*b53 + 
       140*b78*b53 + 470*b89*b53 + 380*b99*b53 + 510*b109*b53 + 560*b110*b53 + 
       320*b111*b53 + 790*b112*b53 + 750*b113*b53 + 390*b114*b53 + 260*b115*b53
        + 20*b116*b53 + 940*b117*b53 + 760*b78*b66 + 550*b89*b66 + 800*b99*b66
        + 340*b109*b66 + 200*b110*b66 + 880*b111*b66 + 600*b112*b66 + 170*b113*
       b66 + 850*b114*b66 + 710*b115*b66 + 970*b116*b66 + 830*b117*b66 + 990*
       b89*b78 + 640*b99*b78 + 680*b109*b78 + 410*b110*b78 + 630*b111*b78 + 670
       *b112*b78 + 310*b113*b78 + 210*b114*b78 + 710*b115*b78 + 880*b116*b78 + 
       530*b117*b78 + 500*b99*b89 + 920*b109*b89 + 290*b110*b89 + 180*b111*b89
        + 860*b112*b89 + 570*b113*b89 + 730*b114*b89 + 180*b115*b89 + 150*b116*
       b89 + 590*b117*b89 + 30*b109*b99 + 190*b110*b99 + 80*b111*b99 + 880*b112
       *b99 + 430*b113*b99 + 570*b114*b99 + 230*b115*b99 + 940*b116*b99 + 210*
       b117*b99 + 620*b110*b109 + 550*b111*b109 + 490*b112*b109 + 60*b113*b109
        + 360*b114*b109 + 670*b115*b109 + 450*b116*b109 + 930*b117*b109 + 930*
       b111*b110 + 630*b112*b110 + 80*b113*b110 + 520*b114*b110 + 540*b115*b110
        + 640*b116*b110 + 240*b117*b110 + 140*b112*b111 + 40*b113*b111 + 190*
       b114*b111 + 710*b115*b111 + 280*b116*b111 + 130*b117*b111 + 450*b113*
       b112 + 520*b114*b112 + 790*b115*b112 + 110*b116*b112 + 400*b117*b112 + 
       120*b114*b113 + 570*b115*b113 + 480*b116*b113 + 170*b117*b113 + 430*b115
       *b114 + 620*b116*b114 + 240*b117*b114 + 450*b116*b115 + 210*b117*b115 + 
       600*b117*b116 >= 23348;

e2459: 20*b25*b10 + 260*b40*b10 + 310*b54*b10 + 290*b67*b10 + 730*b79*b10 + 500
       *b90*b10 + 470*b100*b10 + 470*b109*b10 + 150*b118*b10 + 850*b119*b10 + 
       830*b120*b10 + 530*b121*b10 + 640*b122*b10 + 350*b123*b10 + 640*b124*b10
        + 890*b125*b10 + 90*b40*b25 + 780*b67*b25 + 100*b79*b25 + 400*b90*b25
        + 40*b100*b25 + 660*b109*b25 + 760*b118*b25 + 190*b119*b25 + 540*b120*
       b25 + 470*b121*b25 + 750*b122*b25 + 30*b123*b25 + 490*b124*b25 + 530*
       b125*b25 + 860*b54*b40 + 300*b67*b40 + 260*b79*b40 + 880*b90*b40 + 290*
       b100*b40 + 260*b109*b40 + 450*b118*b40 + 110*b119*b40 + 800*b120*b40 + 
       980*b121*b40 + 270*b122*b40 + 150*b123*b40 + 140*b124*b40 + 690*b125*b40
        + 760*b67*b54 + 140*b79*b54 + 470*b90*b54 + 380*b100*b54 + 60*b109*b54
        + 560*b118*b54 + 320*b119*b54 + 790*b120*b54 + 750*b121*b54 + 390*b122*
       b54 + 260*b123*b54 + 20*b124*b54 + 940*b125*b54 + 760*b79*b67 + 550*b90*
       b67 + 800*b100*b67 + 580*b109*b67 + 200*b118*b67 + 880*b119*b67 + 600*
       b120*b67 + 170*b121*b67 + 850*b122*b67 + 710*b123*b67 + 970*b124*b67 + 
       830*b125*b67 + 990*b90*b79 + 640*b100*b79 + 970*b109*b79 + 410*b118*b79
        + 630*b119*b79 + 670*b120*b79 + 310*b121*b79 + 210*b122*b79 + 710*b123*
       b79 + 880*b124*b79 + 530*b125*b79 + 500*b100*b90 + 630*b109*b90 + 290*
       b118*b90 + 180*b119*b90 + 860*b120*b90 + 570*b121*b90 + 730*b122*b90 + 
       180*b123*b90 + 150*b124*b90 + 590*b125*b90 + 390*b109*b100 + 190*b118*
       b100 + 80*b119*b100 + 880*b120*b100 + 430*b121*b100 + 570*b122*b100 + 
       230*b123*b100 + 940*b124*b100 + 210*b125*b100 + 140*b118*b109 + 140*b119
       *b109 + 870*b120*b109 + 330*b121*b109 + 460*b122*b109 + 80*b123*b109 + 
       40*b124*b109 + 340*b125*b109 + 930*b119*b118 + 630*b120*b118 + 80*b121*
       b118 + 520*b122*b118 + 540*b123*b118 + 640*b124*b118 + 240*b125*b118 + 
       140*b120*b119 + 40*b121*b119 + 190*b122*b119 + 710*b123*b119 + 280*b124*
       b119 + 130*b125*b119 + 450*b121*b120 + 520*b122*b120 + 790*b123*b120 + 
       110*b124*b120 + 400*b125*b120 + 120*b122*b121 + 570*b123*b121 + 480*b124
       *b121 + 170*b125*b121 + 430*b123*b122 + 620*b124*b122 + 240*b125*b122 + 
       450*b124*b123 + 210*b125*b123 + 600*b125*b124 >= 23348;

e2460: 20*b26*b11 + 260*b41*b11 + 310*b55*b11 + 290*b68*b11 + 730*b80*b11 + 500
       *b91*b11 + 470*b101*b11 + 470*b110*b11 + 560*b118*b11 + 850*b126*b11 + 
       830*b127*b11 + 530*b128*b11 + 640*b129*b11 + 350*b130*b11 + 640*b131*b11
        + 890*b132*b11 + 90*b41*b26 + 780*b68*b26 + 100*b80*b26 + 400*b91*b26
        + 40*b101*b26 + 660*b110*b26 + 740*b118*b26 + 190*b126*b26 + 540*b127*
       b26 + 470*b128*b26 + 750*b129*b26 + 30*b130*b26 + 490*b131*b26 + 530*
       b132*b26 + 860*b55*b41 + 300*b68*b41 + 260*b80*b41 + 880*b91*b41 + 290*
       b101*b41 + 260*b110*b41 + 960*b118*b41 + 110*b126*b41 + 800*b127*b41 + 
       980*b128*b41 + 270*b129*b41 + 150*b130*b41 + 140*b131*b41 + 690*b132*b41
        + 760*b68*b55 + 140*b80*b55 + 470*b91*b55 + 380*b101*b55 + 60*b110*b55
        + 510*b118*b55 + 320*b126*b55 + 790*b127*b55 + 750*b128*b55 + 390*b129*
       b55 + 260*b130*b55 + 20*b131*b55 + 940*b132*b55 + 760*b80*b68 + 550*b91*
       b68 + 800*b101*b68 + 580*b110*b68 + 340*b118*b68 + 880*b126*b68 + 600*
       b127*b68 + 170*b128*b68 + 850*b129*b68 + 710*b130*b68 + 970*b131*b68 + 
       830*b132*b68 + 990*b91*b80 + 640*b101*b80 + 970*b110*b80 + 680*b118*b80
        + 630*b126*b80 + 670*b127*b80 + 310*b128*b80 + 210*b129*b80 + 710*b130*
       b80 + 880*b131*b80 + 530*b132*b80 + 500*b101*b91 + 630*b110*b91 + 920*
       b118*b91 + 180*b126*b91 + 860*b127*b91 + 570*b128*b91 + 730*b129*b91 + 
       180*b130*b91 + 150*b131*b91 + 590*b132*b91 + 390*b110*b101 + 30*b118*
       b101 + 80*b126*b101 + 880*b127*b101 + 430*b128*b101 + 570*b129*b101 + 
       230*b130*b101 + 940*b131*b101 + 210*b132*b101 + 720*b118*b110 + 140*b126
       *b110 + 870*b127*b110 + 330*b128*b110 + 460*b129*b110 + 80*b130*b110 + 
       40*b131*b110 + 340*b132*b110 + 550*b126*b118 + 490*b127*b118 + 60*b128*
       b118 + 360*b129*b118 + 670*b130*b118 + 450*b131*b118 + 930*b132*b118 + 
       140*b127*b126 + 40*b128*b126 + 190*b129*b126 + 710*b130*b126 + 280*b131*
       b126 + 130*b132*b126 + 450*b128*b127 + 520*b129*b127 + 790*b130*b127 + 
       110*b131*b127 + 400*b132*b127 + 120*b129*b128 + 570*b130*b128 + 480*b131
       *b128 + 170*b132*b128 + 430*b130*b129 + 620*b131*b129 + 240*b132*b129 + 
       450*b131*b130 + 210*b132*b130 + 600*b132*b131 >= 23348;

e2461: 20*b27*b12 + 260*b42*b12 + 310*b56*b12 + 290*b69*b12 + 730*b81*b12 + 500
       *b92*b12 + 470*b102*b12 + 470*b111*b12 + 560*b119*b12 + 150*b126*b12 + 
       830*b133*b12 + 530*b134*b12 + 640*b135*b12 + 350*b136*b12 + 640*b137*b12
        + 890*b138*b12 + 90*b42*b27 + 780*b69*b27 + 100*b81*b27 + 400*b92*b27
        + 40*b102*b27 + 660*b111*b27 + 740*b119*b27 + 760*b126*b27 + 540*b133*
       b27 + 470*b134*b27 + 750*b135*b27 + 30*b136*b27 + 490*b137*b27 + 530*
       b138*b27 + 860*b56*b42 + 300*b69*b42 + 260*b81*b42 + 880*b92*b42 + 290*
       b102*b42 + 260*b111*b42 + 960*b119*b42 + 450*b126*b42 + 800*b133*b42 + 
       980*b134*b42 + 270*b135*b42 + 150*b136*b42 + 140*b137*b42 + 690*b138*b42
        + 760*b69*b56 + 140*b81*b56 + 470*b92*b56 + 380*b102*b56 + 60*b111*b56
        + 510*b119*b56 + 560*b126*b56 + 790*b133*b56 + 750*b134*b56 + 390*b135*
       b56 + 260*b136*b56 + 20*b137*b56 + 940*b138*b56 + 760*b81*b69 + 550*b92*
       b69 + 800*b102*b69 + 580*b111*b69 + 340*b119*b69 + 200*b126*b69 + 600*
       b133*b69 + 170*b134*b69 + 850*b135*b69 + 710*b136*b69 + 970*b137*b69 + 
       830*b138*b69 + 990*b92*b81 + 640*b102*b81 + 970*b111*b81 + 680*b119*b81
        + 410*b126*b81 + 670*b133*b81 + 310*b134*b81 + 210*b135*b81 + 710*b136*
       b81 + 880*b137*b81 + 530*b138*b81 + 500*b102*b92 + 630*b111*b92 + 920*
       b119*b92 + 290*b126*b92 + 860*b133*b92 + 570*b134*b92 + 730*b135*b92 + 
       180*b136*b92 + 150*b137*b92 + 590*b138*b92 + 390*b111*b102 + 30*b119*
       b102 + 190*b126*b102 + 880*b133*b102 + 430*b134*b102 + 570*b135*b102 + 
       230*b136*b102 + 940*b137*b102 + 210*b138*b102 + 720*b119*b111 + 140*b126
       *b111 + 870*b133*b111 + 330*b134*b111 + 460*b135*b111 + 80*b136*b111 + 
       40*b137*b111 + 340*b138*b111 + 620*b126*b119 + 490*b133*b119 + 60*b134*
       b119 + 360*b135*b119 + 670*b136*b119 + 450*b137*b119 + 930*b138*b119 + 
       630*b133*b126 + 80*b134*b126 + 520*b135*b126 + 540*b136*b126 + 640*b137*
       b126 + 240*b138*b126 + 450*b134*b133 + 520*b135*b133 + 790*b136*b133 + 
       110*b137*b133 + 400*b138*b133 + 120*b135*b134 + 570*b136*b134 + 480*b137
       *b134 + 170*b138*b134 + 430*b136*b135 + 620*b137*b135 + 240*b138*b135 + 
       450*b137*b136 + 210*b138*b136 + 600*b138*b137 >= 23348;

e2462: 20*b28*b13 + 260*b43*b13 + 310*b57*b13 + 290*b70*b13 + 730*b82*b13 + 500
       *b93*b13 + 470*b103*b13 + 470*b112*b13 + 560*b120*b13 + 150*b127*b13 + 
       850*b133*b13 + 530*b139*b13 + 640*b140*b13 + 350*b141*b13 + 640*b142*b13
        + 890*b143*b13 + 90*b43*b28 + 780*b70*b28 + 100*b82*b28 + 400*b93*b28
        + 40*b103*b28 + 660*b112*b28 + 740*b120*b28 + 760*b127*b28 + 190*b133*
       b28 + 470*b139*b28 + 750*b140*b28 + 30*b141*b28 + 490*b142*b28 + 530*
       b143*b28 + 860*b57*b43 + 300*b70*b43 + 260*b82*b43 + 880*b93*b43 + 290*
       b103*b43 + 260*b112*b43 + 960*b120*b43 + 450*b127*b43 + 110*b133*b43 + 
       980*b139*b43 + 270*b140*b43 + 150*b141*b43 + 140*b142*b43 + 690*b143*b43
        + 760*b70*b57 + 140*b82*b57 + 470*b93*b57 + 380*b103*b57 + 60*b112*b57
        + 510*b120*b57 + 560*b127*b57 + 320*b133*b57 + 750*b139*b57 + 390*b140*
       b57 + 260*b141*b57 + 20*b142*b57 + 940*b143*b57 + 760*b82*b70 + 550*b93*
       b70 + 800*b103*b70 + 580*b112*b70 + 340*b120*b70 + 200*b127*b70 + 880*
       b133*b70 + 170*b139*b70 + 850*b140*b70 + 710*b141*b70 + 970*b142*b70 + 
       830*b143*b70 + 990*b93*b82 + 640*b103*b82 + 970*b112*b82 + 680*b120*b82
        + 410*b127*b82 + 630*b133*b82 + 310*b139*b82 + 210*b140*b82 + 710*b141*
       b82 + 880*b142*b82 + 530*b143*b82 + 500*b103*b93 + 630*b112*b93 + 920*
       b120*b93 + 290*b127*b93 + 180*b133*b93 + 570*b139*b93 + 730*b140*b93 + 
       180*b141*b93 + 150*b142*b93 + 590*b143*b93 + 390*b112*b103 + 30*b120*
       b103 + 190*b127*b103 + 80*b133*b103 + 430*b139*b103 + 570*b140*b103 + 
       230*b141*b103 + 940*b142*b103 + 210*b143*b103 + 720*b120*b112 + 140*b127
       *b112 + 140*b133*b112 + 330*b139*b112 + 460*b140*b112 + 80*b141*b112 + 
       40*b142*b112 + 340*b143*b112 + 620*b127*b120 + 550*b133*b120 + 60*b139*
       b120 + 360*b140*b120 + 670*b141*b120 + 450*b142*b120 + 930*b143*b120 + 
       930*b133*b127 + 80*b139*b127 + 520*b140*b127 + 540*b141*b127 + 640*b142*
       b127 + 240*b143*b127 + 40*b139*b133 + 190*b140*b133 + 710*b141*b133 + 
       280*b142*b133 + 130*b143*b133 + 120*b140*b139 + 570*b141*b139 + 480*b142
       *b139 + 170*b143*b139 + 430*b141*b140 + 620*b142*b140 + 240*b143*b140 + 
       450*b142*b141 + 210*b143*b141 + 600*b143*b142 >= 23348;

e2463: 20*b29*b14 + 260*b44*b14 + 310*b58*b14 + 290*b71*b14 + 730*b83*b14 + 500
       *b94*b14 + 470*b104*b14 + 470*b113*b14 + 560*b121*b14 + 150*b128*b14 + 
       850*b134*b14 + 830*b139*b14 + 640*b144*b14 + 350*b145*b14 + 640*b146*b14
        + 890*b147*b14 + 90*b44*b29 + 780*b71*b29 + 100*b83*b29 + 400*b94*b29
        + 40*b104*b29 + 660*b113*b29 + 740*b121*b29 + 760*b128*b29 + 190*b134*
       b29 + 540*b139*b29 + 750*b144*b29 + 30*b145*b29 + 490*b146*b29 + 530*
       b147*b29 + 860*b58*b44 + 300*b71*b44 + 260*b83*b44 + 880*b94*b44 + 290*
       b104*b44 + 260*b113*b44 + 960*b121*b44 + 450*b128*b44 + 110*b134*b44 + 
       800*b139*b44 + 270*b144*b44 + 150*b145*b44 + 140*b146*b44 + 690*b147*b44
        + 760*b71*b58 + 140*b83*b58 + 470*b94*b58 + 380*b104*b58 + 60*b113*b58
        + 510*b121*b58 + 560*b128*b58 + 320*b134*b58 + 790*b139*b58 + 390*b144*
       b58 + 260*b145*b58 + 20*b146*b58 + 940*b147*b58 + 760*b83*b71 + 550*b94*
       b71 + 800*b104*b71 + 580*b113*b71 + 340*b121*b71 + 200*b128*b71 + 880*
       b134*b71 + 600*b139*b71 + 850*b144*b71 + 710*b145*b71 + 970*b146*b71 + 
       830*b147*b71 + 990*b94*b83 + 640*b104*b83 + 970*b113*b83 + 680*b121*b83
        + 410*b128*b83 + 630*b134*b83 + 670*b139*b83 + 210*b144*b83 + 710*b145*
       b83 + 880*b146*b83 + 530*b147*b83 + 500*b104*b94 + 630*b113*b94 + 920*
       b121*b94 + 290*b128*b94 + 180*b134*b94 + 860*b139*b94 + 730*b144*b94 + 
       180*b145*b94 + 150*b146*b94 + 590*b147*b94 + 390*b113*b104 + 30*b121*
       b104 + 190*b128*b104 + 80*b134*b104 + 880*b139*b104 + 570*b144*b104 + 
       230*b145*b104 + 940*b146*b104 + 210*b147*b104 + 720*b121*b113 + 140*b128
       *b113 + 140*b134*b113 + 870*b139*b113 + 460*b144*b113 + 80*b145*b113 + 
       40*b146*b113 + 340*b147*b113 + 620*b128*b121 + 550*b134*b121 + 490*b139*
       b121 + 360*b144*b121 + 670*b145*b121 + 450*b146*b121 + 930*b147*b121 + 
       930*b134*b128 + 630*b139*b128 + 520*b144*b128 + 540*b145*b128 + 640*b146
       *b128 + 240*b147*b128 + 140*b139*b134 + 190*b144*b134 + 710*b145*b134 + 
       280*b146*b134 + 130*b147*b134 + 520*b144*b139 + 790*b145*b139 + 110*b146
       *b139 + 400*b147*b139 + 430*b145*b144 + 620*b146*b144 + 240*b147*b144 + 
       450*b146*b145 + 210*b147*b145 + 600*b147*b146 >= 23348;

e2464: 20*b30*b15 + 260*b45*b15 + 310*b59*b15 + 290*b72*b15 + 730*b84*b15 + 500
       *b95*b15 + 470*b105*b15 + 470*b114*b15 + 560*b122*b15 + 150*b129*b15 + 
       850*b135*b15 + 830*b140*b15 + 530*b144*b15 + 350*b148*b15 + 640*b149*b15
        + 890*b150*b15 + 90*b45*b30 + 780*b72*b30 + 100*b84*b30 + 400*b95*b30
        + 40*b105*b30 + 660*b114*b30 + 740*b122*b30 + 760*b129*b30 + 190*b135*
       b30 + 540*b140*b30 + 470*b144*b30 + 30*b148*b30 + 490*b149*b30 + 530*
       b150*b30 + 860*b59*b45 + 300*b72*b45 + 260*b84*b45 + 880*b95*b45 + 290*
       b105*b45 + 260*b114*b45 + 960*b122*b45 + 450*b129*b45 + 110*b135*b45 + 
       800*b140*b45 + 980*b144*b45 + 150*b148*b45 + 140*b149*b45 + 690*b150*b45
        + 760*b72*b59 + 140*b84*b59 + 470*b95*b59 + 380*b105*b59 + 60*b114*b59
        + 510*b122*b59 + 560*b129*b59 + 320*b135*b59 + 790*b140*b59 + 750*b144*
       b59 + 260*b148*b59 + 20*b149*b59 + 940*b150*b59 + 760*b84*b72 + 550*b95*
       b72 + 800*b105*b72 + 580*b114*b72 + 340*b122*b72 + 200*b129*b72 + 880*
       b135*b72 + 600*b140*b72 + 170*b144*b72 + 710*b148*b72 + 970*b149*b72 + 
       830*b150*b72 + 990*b95*b84 + 640*b105*b84 + 970*b114*b84 + 680*b122*b84
        + 410*b129*b84 + 630*b135*b84 + 670*b140*b84 + 310*b144*b84 + 710*b148*
       b84 + 880*b149*b84 + 530*b150*b84 + 500*b105*b95 + 630*b114*b95 + 920*
       b122*b95 + 290*b129*b95 + 180*b135*b95 + 860*b140*b95 + 570*b144*b95 + 
       180*b148*b95 + 150*b149*b95 + 590*b150*b95 + 390*b114*b105 + 30*b122*
       b105 + 190*b129*b105 + 80*b135*b105 + 880*b140*b105 + 430*b144*b105 + 
       230*b148*b105 + 940*b149*b105 + 210*b150*b105 + 720*b122*b114 + 140*b129
       *b114 + 140*b135*b114 + 870*b140*b114 + 330*b144*b114 + 80*b148*b114 + 
       40*b149*b114 + 340*b150*b114 + 620*b129*b122 + 550*b135*b122 + 490*b140*
       b122 + 60*b144*b122 + 670*b148*b122 + 450*b149*b122 + 930*b150*b122 + 
       930*b135*b129 + 630*b140*b129 + 80*b144*b129 + 540*b148*b129 + 640*b149*
       b129 + 240*b150*b129 + 140*b140*b135 + 40*b144*b135 + 710*b148*b135 + 
       280*b149*b135 + 130*b150*b135 + 450*b144*b140 + 790*b148*b140 + 110*b149
       *b140 + 400*b150*b140 + 570*b148*b144 + 480*b149*b144 + 170*b150*b144 + 
       450*b149*b148 + 210*b150*b148 + 600*b150*b149 >= 23348;

e2465: 20*b31*b16 + 260*b46*b16 + 310*b60*b16 + 290*b73*b16 + 730*b85*b16 + 500
       *b96*b16 + 470*b106*b16 + 470*b115*b16 + 560*b123*b16 + 150*b130*b16 + 
       850*b136*b16 + 830*b141*b16 + 530*b145*b16 + 640*b148*b16 + 640*b151*b16
        + 890*b152*b16 + 90*b46*b31 + 780*b73*b31 + 100*b85*b31 + 400*b96*b31
        + 40*b106*b31 + 660*b115*b31 + 740*b123*b31 + 760*b130*b31 + 190*b136*
       b31 + 540*b141*b31 + 470*b145*b31 + 750*b148*b31 + 490*b151*b31 + 530*
       b152*b31 + 860*b60*b46 + 300*b73*b46 + 260*b85*b46 + 880*b96*b46 + 290*
       b106*b46 + 260*b115*b46 + 960*b123*b46 + 450*b130*b46 + 110*b136*b46 + 
       800*b141*b46 + 980*b145*b46 + 270*b148*b46 + 140*b151*b46 + 690*b152*b46
        + 760*b73*b60 + 140*b85*b60 + 470*b96*b60 + 380*b106*b60 + 60*b115*b60
        + 510*b123*b60 + 560*b130*b60 + 320*b136*b60 + 790*b141*b60 + 750*b145*
       b60 + 390*b148*b60 + 20*b151*b60 + 940*b152*b60 + 760*b85*b73 + 550*b96*
       b73 + 800*b106*b73 + 580*b115*b73 + 340*b123*b73 + 200*b130*b73 + 880*
       b136*b73 + 600*b141*b73 + 170*b145*b73 + 850*b148*b73 + 970*b151*b73 + 
       830*b152*b73 + 990*b96*b85 + 640*b106*b85 + 970*b115*b85 + 680*b123*b85
        + 410*b130*b85 + 630*b136*b85 + 670*b141*b85 + 310*b145*b85 + 210*b148*
       b85 + 880*b151*b85 + 530*b152*b85 + 500*b106*b96 + 630*b115*b96 + 920*
       b123*b96 + 290*b130*b96 + 180*b136*b96 + 860*b141*b96 + 570*b145*b96 + 
       730*b148*b96 + 150*b151*b96 + 590*b152*b96 + 390*b115*b106 + 30*b123*
       b106 + 190*b130*b106 + 80*b136*b106 + 880*b141*b106 + 430*b145*b106 + 
       570*b148*b106 + 940*b151*b106 + 210*b152*b106 + 720*b123*b115 + 140*b130
       *b115 + 140*b136*b115 + 870*b141*b115 + 330*b145*b115 + 460*b148*b115 + 
       40*b151*b115 + 340*b152*b115 + 620*b130*b123 + 550*b136*b123 + 490*b141*
       b123 + 60*b145*b123 + 360*b148*b123 + 450*b151*b123 + 930*b152*b123 + 
       930*b136*b130 + 630*b141*b130 + 80*b145*b130 + 520*b148*b130 + 640*b151*
       b130 + 240*b152*b130 + 140*b141*b136 + 40*b145*b136 + 190*b148*b136 + 
       280*b151*b136 + 130*b152*b136 + 450*b145*b141 + 520*b148*b141 + 110*b151
       *b141 + 400*b152*b141 + 120*b148*b145 + 480*b151*b145 + 170*b152*b145 + 
       620*b151*b148 + 240*b152*b148 + 600*b152*b151 >= 23348;

e2466: 20*b32*b17 + 260*b47*b17 + 310*b61*b17 + 290*b74*b17 + 730*b86*b17 + 500
       *b97*b17 + 470*b107*b17 + 470*b116*b17 + 560*b124*b17 + 150*b131*b17 + 
       850*b137*b17 + 830*b142*b17 + 530*b146*b17 + 640*b149*b17 + 350*b151*b17
        + 890*b153*b17 + 90*b47*b32 + 780*b74*b32 + 100*b86*b32 + 400*b97*b32
        + 40*b107*b32 + 660*b116*b32 + 740*b124*b32 + 760*b131*b32 + 190*b137*
       b32 + 540*b142*b32 + 470*b146*b32 + 750*b149*b32 + 30*b151*b32 + 530*
       b153*b32 + 860*b61*b47 + 300*b74*b47 + 260*b86*b47 + 880*b97*b47 + 290*
       b107*b47 + 260*b116*b47 + 960*b124*b47 + 450*b131*b47 + 110*b137*b47 + 
       800*b142*b47 + 980*b146*b47 + 270*b149*b47 + 150*b151*b47 + 690*b153*b47
        + 760*b74*b61 + 140*b86*b61 + 470*b97*b61 + 380*b107*b61 + 60*b116*b61
        + 510*b124*b61 + 560*b131*b61 + 320*b137*b61 + 790*b142*b61 + 750*b146*
       b61 + 390*b149*b61 + 260*b151*b61 + 940*b153*b61 + 760*b86*b74 + 550*b97
       *b74 + 800*b107*b74 + 580*b116*b74 + 340*b124*b74 + 200*b131*b74 + 880*
       b137*b74 + 600*b142*b74 + 170*b146*b74 + 850*b149*b74 + 710*b151*b74 + 
       830*b153*b74 + 990*b97*b86 + 640*b107*b86 + 970*b116*b86 + 680*b124*b86
        + 410*b131*b86 + 630*b137*b86 + 670*b142*b86 + 310*b146*b86 + 210*b149*
       b86 + 710*b151*b86 + 530*b153*b86 + 500*b107*b97 + 630*b116*b97 + 920*
       b124*b97 + 290*b131*b97 + 180*b137*b97 + 860*b142*b97 + 570*b146*b97 + 
       730*b149*b97 + 180*b151*b97 + 590*b153*b97 + 390*b116*b107 + 30*b124*
       b107 + 190*b131*b107 + 80*b137*b107 + 880*b142*b107 + 430*b146*b107 + 
       570*b149*b107 + 230*b151*b107 + 210*b153*b107 + 720*b124*b116 + 140*b131
       *b116 + 140*b137*b116 + 870*b142*b116 + 330*b146*b116 + 460*b149*b116 + 
       80*b151*b116 + 340*b153*b116 + 620*b131*b124 + 550*b137*b124 + 490*b142*
       b124 + 60*b146*b124 + 360*b149*b124 + 670*b151*b124 + 930*b153*b124 + 
       930*b137*b131 + 630*b142*b131 + 80*b146*b131 + 520*b149*b131 + 540*b151*
       b131 + 240*b153*b131 + 140*b142*b137 + 40*b146*b137 + 190*b149*b137 + 
       710*b151*b137 + 130*b153*b137 + 450*b146*b142 + 520*b149*b142 + 790*b151
       *b142 + 400*b153*b142 + 120*b149*b146 + 570*b151*b146 + 170*b153*b146 + 
       430*b151*b149 + 240*b153*b149 + 210*b153*b151 >= 23348;

e2467: 20*b33*b18 + 260*b48*b18 + 310*b62*b18 + 290*b75*b18 + 730*b87*b18 + 500
       *b98*b18 + 470*b108*b18 + 470*b117*b18 + 560*b125*b18 + 150*b132*b18 + 
       850*b138*b18 + 830*b143*b18 + 530*b147*b18 + 640*b150*b18 + 350*b152*b18
        + 640*b153*b18 + 90*b48*b33 + 780*b75*b33 + 100*b87*b33 + 400*b98*b33
        + 40*b108*b33 + 660*b117*b33 + 740*b125*b33 + 760*b132*b33 + 190*b138*
       b33 + 540*b143*b33 + 470*b147*b33 + 750*b150*b33 + 30*b152*b33 + 490*
       b153*b33 + 860*b62*b48 + 300*b75*b48 + 260*b87*b48 + 880*b98*b48 + 290*
       b108*b48 + 260*b117*b48 + 960*b125*b48 + 450*b132*b48 + 110*b138*b48 + 
       800*b143*b48 + 980*b147*b48 + 270*b150*b48 + 150*b152*b48 + 140*b153*b48
        + 760*b75*b62 + 140*b87*b62 + 470*b98*b62 + 380*b108*b62 + 60*b117*b62
        + 510*b125*b62 + 560*b132*b62 + 320*b138*b62 + 790*b143*b62 + 750*b147*
       b62 + 390*b150*b62 + 260*b152*b62 + 20*b153*b62 + 760*b87*b75 + 550*b98*
       b75 + 800*b108*b75 + 580*b117*b75 + 340*b125*b75 + 200*b132*b75 + 880*
       b138*b75 + 600*b143*b75 + 170*b147*b75 + 850*b150*b75 + 710*b152*b75 + 
       970*b153*b75 + 990*b98*b87 + 640*b108*b87 + 970*b117*b87 + 680*b125*b87
        + 410*b132*b87 + 630*b138*b87 + 670*b143*b87 + 310*b147*b87 + 210*b150*
       b87 + 710*b152*b87 + 880*b153*b87 + 500*b108*b98 + 630*b117*b98 + 920*
       b125*b98 + 290*b132*b98 + 180*b138*b98 + 860*b143*b98 + 570*b147*b98 + 
       730*b150*b98 + 180*b152*b98 + 150*b153*b98 + 390*b117*b108 + 30*b125*
       b108 + 190*b132*b108 + 80*b138*b108 + 880*b143*b108 + 430*b147*b108 + 
       570*b150*b108 + 230*b152*b108 + 940*b153*b108 + 720*b125*b117 + 140*b132
       *b117 + 140*b138*b117 + 870*b143*b117 + 330*b147*b117 + 460*b150*b117 + 
       80*b152*b117 + 40*b153*b117 + 620*b132*b125 + 550*b138*b125 + 490*b143*
       b125 + 60*b147*b125 + 360*b150*b125 + 670*b152*b125 + 450*b153*b125 + 
       930*b138*b132 + 630*b143*b132 + 80*b147*b132 + 520*b150*b132 + 540*b152*
       b132 + 640*b153*b132 + 140*b143*b138 + 40*b147*b138 + 190*b150*b138 + 
       710*b152*b138 + 280*b153*b138 + 450*b147*b143 + 520*b150*b143 + 790*b152
       *b143 + 110*b153*b143 + 120*b150*b147 + 570*b152*b147 + 480*b153*b147 + 
       430*b152*b150 + 620*b153*b150 + 450*b153*b152 >= 23348;
