#  MINLP written by GAMS Convert at 01/12/18 13:42:52
#  
#  Equation counts
#      Total        E        G        L        N        X        C        B
#          1        0        0        1        0        0        0        0
#  
#  Variable counts
#                   x        b        i      s1s      s2s       sc       si
#      Total     cont   binary  integer     sos1     sos2    scont     sint
#        436        1      435        0        0        0        0        0
#  FX      0        0        0        0        0        0        0        0
#  
#  Nonzero counts
#      Total    const       NL      DLL
#        436        1      435        0


var b1 binary >= 0, <= 1;
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;
var b155 binary >= 0, <= 1;
var b156 binary >= 0, <= 1;
var b157 binary >= 0, <= 1;
var b158 binary >= 0, <= 1;
var b159 binary >= 0, <= 1;
var b160 binary >= 0, <= 1;
var b161 binary >= 0, <= 1;
var b162 binary >= 0, <= 1;
var b163 binary >= 0, <= 1;
var b164 binary >= 0, <= 1;
var b165 binary >= 0, <= 1;
var b166 binary >= 0, <= 1;
var b167 binary >= 0, <= 1;
var b168 binary >= 0, <= 1;
var b169 binary >= 0, <= 1;
var b170 binary >= 0, <= 1;
var b171 binary >= 0, <= 1;
var b172 binary >= 0, <= 1;
var b173 binary >= 0, <= 1;
var b174 binary >= 0, <= 1;
var b175 binary >= 0, <= 1;
var b176 binary >= 0, <= 1;
var b177 binary >= 0, <= 1;
var b178 binary >= 0, <= 1;
var b179 binary >= 0, <= 1;
var b180 binary >= 0, <= 1;
var b181 binary >= 0, <= 1;
var b182 binary >= 0, <= 1;
var b183 binary >= 0, <= 1;
var b184 binary >= 0, <= 1;
var b185 binary >= 0, <= 1;
var b186 binary >= 0, <= 1;
var b187 binary >= 0, <= 1;
var b188 binary >= 0, <= 1;
var b189 binary >= 0, <= 1;
var b190 binary >= 0, <= 1;
var b191 binary >= 0, <= 1;
var b192 binary >= 0, <= 1;
var b193 binary >= 0, <= 1;
var b194 binary >= 0, <= 1;
var b195 binary >= 0, <= 1;
var b196 binary >= 0, <= 1;
var b197 binary >= 0, <= 1;
var b198 binary >= 0, <= 1;
var b199 binary >= 0, <= 1;
var b200 binary >= 0, <= 1;
var b201 binary >= 0, <= 1;
var b202 binary >= 0, <= 1;
var b203 binary >= 0, <= 1;
var b204 binary >= 0, <= 1;
var b205 binary >= 0, <= 1;
var b206 binary >= 0, <= 1;
var b207 binary >= 0, <= 1;
var b208 binary >= 0, <= 1;
var b209 binary >= 0, <= 1;
var b210 binary >= 0, <= 1;
var b211 binary >= 0, <= 1;
var b212 binary >= 0, <= 1;
var b213 binary >= 0, <= 1;
var b214 binary >= 0, <= 1;
var b215 binary >= 0, <= 1;
var b216 binary >= 0, <= 1;
var b217 binary >= 0, <= 1;
var b218 binary >= 0, <= 1;
var b219 binary >= 0, <= 1;
var b220 binary >= 0, <= 1;
var b221 binary >= 0, <= 1;
var b222 binary >= 0, <= 1;
var b223 binary >= 0, <= 1;
var b224 binary >= 0, <= 1;
var b225 binary >= 0, <= 1;
var b226 binary >= 0, <= 1;
var b227 binary >= 0, <= 1;
var b228 binary >= 0, <= 1;
var b229 binary >= 0, <= 1;
var b230 binary >= 0, <= 1;
var b231 binary >= 0, <= 1;
var b232 binary >= 0, <= 1;
var b233 binary >= 0, <= 1;
var b234 binary >= 0, <= 1;
var b235 binary >= 0, <= 1;
var b236 binary >= 0, <= 1;
var b237 binary >= 0, <= 1;
var b238 binary >= 0, <= 1;
var b239 binary >= 0, <= 1;
var b240 binary >= 0, <= 1;
var b241 binary >= 0, <= 1;
var b242 binary >= 0, <= 1;
var b243 binary >= 0, <= 1;
var b244 binary >= 0, <= 1;
var b245 binary >= 0, <= 1;
var b246 binary >= 0, <= 1;
var b247 binary >= 0, <= 1;
var b248 binary >= 0, <= 1;
var b249 binary >= 0, <= 1;
var b250 binary >= 0, <= 1;
var b251 binary >= 0, <= 1;
var b252 binary >= 0, <= 1;
var b253 binary >= 0, <= 1;
var b254 binary >= 0, <= 1;
var b255 binary >= 0, <= 1;
var b256 binary >= 0, <= 1;
var b257 binary >= 0, <= 1;
var b258 binary >= 0, <= 1;
var b259 binary >= 0, <= 1;
var b260 binary >= 0, <= 1;
var b261 binary >= 0, <= 1;
var b262 binary >= 0, <= 1;
var b263 binary >= 0, <= 1;
var b264 binary >= 0, <= 1;
var b265 binary >= 0, <= 1;
var b266 binary >= 0, <= 1;
var b267 binary >= 0, <= 1;
var b268 binary >= 0, <= 1;
var b269 binary >= 0, <= 1;
var b270 binary >= 0, <= 1;
var b271 binary >= 0, <= 1;
var b272 binary >= 0, <= 1;
var b273 binary >= 0, <= 1;
var b274 binary >= 0, <= 1;
var b275 binary >= 0, <= 1;
var b276 binary >= 0, <= 1;
var b277 binary >= 0, <= 1;
var b278 binary >= 0, <= 1;
var b279 binary >= 0, <= 1;
var b280 binary >= 0, <= 1;
var b281 binary >= 0, <= 1;
var b282 binary >= 0, <= 1;
var b283 binary >= 0, <= 1;
var b284 binary >= 0, <= 1;
var b285 binary >= 0, <= 1;
var b286 binary >= 0, <= 1;
var b287 binary >= 0, <= 1;
var b288 binary >= 0, <= 1;
var b289 binary >= 0, <= 1;
var b290 binary >= 0, <= 1;
var b291 binary >= 0, <= 1;
var b292 binary >= 0, <= 1;
var b293 binary >= 0, <= 1;
var b294 binary >= 0, <= 1;
var b295 binary >= 0, <= 1;
var b296 binary >= 0, <= 1;
var b297 binary >= 0, <= 1;
var b298 binary >= 0, <= 1;
var b299 binary >= 0, <= 1;
var b300 binary >= 0, <= 1;
var b301 binary >= 0, <= 1;
var b302 binary >= 0, <= 1;
var b303 binary >= 0, <= 1;
var b304 binary >= 0, <= 1;
var b305 binary >= 0, <= 1;
var b306 binary >= 0, <= 1;
var b307 binary >= 0, <= 1;
var b308 binary >= 0, <= 1;
var b309 binary >= 0, <= 1;
var b310 binary >= 0, <= 1;
var b311 binary >= 0, <= 1;
var b312 binary >= 0, <= 1;
var b313 binary >= 0, <= 1;
var b314 binary >= 0, <= 1;
var b315 binary >= 0, <= 1;
var b316 binary >= 0, <= 1;
var b317 binary >= 0, <= 1;
var b318 binary >= 0, <= 1;
var b319 binary >= 0, <= 1;
var b320 binary >= 0, <= 1;
var b321 binary >= 0, <= 1;
var b322 binary >= 0, <= 1;
var b323 binary >= 0, <= 1;
var b324 binary >= 0, <= 1;
var b325 binary >= 0, <= 1;
var b326 binary >= 0, <= 1;
var b327 binary >= 0, <= 1;
var b328 binary >= 0, <= 1;
var b329 binary >= 0, <= 1;
var b330 binary >= 0, <= 1;
var b331 binary >= 0, <= 1;
var b332 binary >= 0, <= 1;
var b333 binary >= 0, <= 1;
var b334 binary >= 0, <= 1;
var b335 binary >= 0, <= 1;
var b336 binary >= 0, <= 1;
var b337 binary >= 0, <= 1;
var b338 binary >= 0, <= 1;
var b339 binary >= 0, <= 1;
var b340 binary >= 0, <= 1;
var b341 binary >= 0, <= 1;
var b342 binary >= 0, <= 1;
var b343 binary >= 0, <= 1;
var b344 binary >= 0, <= 1;
var b345 binary >= 0, <= 1;
var b346 binary >= 0, <= 1;
var b347 binary >= 0, <= 1;
var b348 binary >= 0, <= 1;
var b349 binary >= 0, <= 1;
var b350 binary >= 0, <= 1;
var b351 binary >= 0, <= 1;
var b352 binary >= 0, <= 1;
var b353 binary >= 0, <= 1;
var b354 binary >= 0, <= 1;
var b355 binary >= 0, <= 1;
var b356 binary >= 0, <= 1;
var b357 binary >= 0, <= 1;
var b358 binary >= 0, <= 1;
var b359 binary >= 0, <= 1;
var b360 binary >= 0, <= 1;
var b361 binary >= 0, <= 1;
var b362 binary >= 0, <= 1;
var b363 binary >= 0, <= 1;
var b364 binary >= 0, <= 1;
var b365 binary >= 0, <= 1;
var b366 binary >= 0, <= 1;
var b367 binary >= 0, <= 1;
var b368 binary >= 0, <= 1;
var b369 binary >= 0, <= 1;
var b370 binary >= 0, <= 1;
var b371 binary >= 0, <= 1;
var b372 binary >= 0, <= 1;
var b373 binary >= 0, <= 1;
var b374 binary >= 0, <= 1;
var b375 binary >= 0, <= 1;
var b376 binary >= 0, <= 1;
var b377 binary >= 0, <= 1;
var b378 binary >= 0, <= 1;
var b379 binary >= 0, <= 1;
var b380 binary >= 0, <= 1;
var b381 binary >= 0, <= 1;
var b382 binary >= 0, <= 1;
var b383 binary >= 0, <= 1;
var b384 binary >= 0, <= 1;
var b385 binary >= 0, <= 1;
var b386 binary >= 0, <= 1;
var b387 binary >= 0, <= 1;
var b388 binary >= 0, <= 1;
var b389 binary >= 0, <= 1;
var b390 binary >= 0, <= 1;
var b391 binary >= 0, <= 1;
var b392 binary >= 0, <= 1;
var b393 binary >= 0, <= 1;
var b394 binary >= 0, <= 1;
var b395 binary >= 0, <= 1;
var b396 binary >= 0, <= 1;
var b397 binary >= 0, <= 1;
var b398 binary >= 0, <= 1;
var b399 binary >= 0, <= 1;
var b400 binary >= 0, <= 1;
var b401 binary >= 0, <= 1;
var b402 binary >= 0, <= 1;
var b403 binary >= 0, <= 1;
var b404 binary >= 0, <= 1;
var b405 binary >= 0, <= 1;
var b406 binary >= 0, <= 1;
var b407 binary >= 0, <= 1;
var b408 binary >= 0, <= 1;
var b409 binary >= 0, <= 1;
var b410 binary >= 0, <= 1;
var b411 binary >= 0, <= 1;
var b412 binary >= 0, <= 1;
var b413 binary >= 0, <= 1;
var b414 binary >= 0, <= 1;
var b415 binary >= 0, <= 1;
var b416 binary >= 0, <= 1;
var b417 binary >= 0, <= 1;
var b418 binary >= 0, <= 1;
var b419 binary >= 0, <= 1;
var b420 binary >= 0, <= 1;
var b421 binary >= 0, <= 1;
var b422 binary >= 0, <= 1;
var b423 binary >= 0, <= 1;
var b424 binary >= 0, <= 1;
var b425 binary >= 0, <= 1;
var b426 binary >= 0, <= 1;
var b427 binary >= 0, <= 1;
var b428 binary >= 0, <= 1;
var b429 binary >= 0, <= 1;
var b430 binary >= 0, <= 1;
var b431 binary >= 0, <= 1;
var b432 binary >= 0, <= 1;
var b433 binary >= 0, <= 1;
var b434 binary >= 0, <= 1;
var b435 binary >= 0, <= 1;
var x436;

maximize obj: x436;

subject to

e1: 2*b1*b198 - 2*b1 - 2*b198 - 2*b1*b235 + 2*b235 + 2*b1*b280 + 2*b1*b294 + 2*
    b2*b283 - 2*b2 - 2*b2*b316 + 2*b2*b317 + 2*b2*b318 + 2*b3*b51 - 2*b3 - 2*
    b51 - 2*b3*b149 + 2*b149 + 2*b3*b178 + 2*b178 + 2*b3*b284 + 2*b4*b154 - 2*
    b4 - 2*b154 + 2*b4*b253 - 4*b253 + 2*b4*b255 + 2*b255 - 2*b4*b348 + 2*b5*
    b56 - 2*b5 - 2*b56 - 2*b5*b340 + 2*b5*b341 + 2*b5*b342 + 2*b6*b205 + 2*b6
     - 2*b205 - 2*b6*b327 - 2*b6*b354 - 2*b6*b355 + 2*b7*b70 - 2*b7 - 2*b70 - 2
    *b7*b177 + 2*b177 + 2*b7*b289 + 2*b7*b290 + 2*b8*b56 - 2*b8 + 2*b8*b73 - 2*
    b73 - 2*b8*b351 + 2*b8*b352 + 2*b9*b86 - 2*b9 - 2*b86 - 2*b9*b213 + 2*b213
     + 2*b9*b283 + 2*b9*b299 + 2*b10*b73 - 2*b10 + 2*b10*b90 - 2*b90 - 2*b10*
    b359 + 2*b10*b360 + 2*b11*b22 - 2*b11 - 2*b22 + 2*b11*b201 - 4*b201 + 2*b12
    *b18 - 2*b12 - 2*b18 - 2*b12*b149 + 2*b12*b250 - 2*b250 + 2*b12*b286 + 2*
    b13*b90 - 2*b13 + 2*b13*b113 - 4*b113 + 2*b13*b134 - 2*b134 - 2*b13*b369 - 
    2*b14*b177 + 2*b14 - 2*b14*b247 - 2*b247 - 2*b14*b314 + 2*b14*b316 + 2*b15*
    b113 - 2*b15 + 2*b15*b135 - 4*b135 + 2*b15*b159 - 4*b159 - 2*b15*b379 + 2*
    b16*b33 - 2*b16 - 2*b33 + 2*b16*b362 + 2*b17*b244 - 4*b17 - 4*b244 + 2*b17*
    b287 + 2*b17*b323 + 2*b17*b387 + 2*b18*b84 - 2*b84 + 2*b18*b126 - 4*b126 - 
    2*b18*b323 - 2*b19*b210 + 2*b19 - 2*b210 - 2*b19*b213 - 2*b19*b304 + 2*b19*
    b307 + 2*b20*b135 - 4*b20 + 2*b20*b161 - 4*b161 + 2*b20*b188 - 4*b188 + 2*
    b20*b379 - 2*b21*b73 - 2*b21 + 2*b21*b75 - 4*b75 + 2*b21*b161 + 2*b21*b370
     + 2*b22*b23 - 2*b23 - 2*b22*b61 - 2*b61 + 2*b22*b120 - 4*b120 + 2*b23*b45
     - 2*b45 + 2*b24*b161 - 4*b24 + 2*b24*b190 - 4*b190 + 2*b24*b224 - 4*b224
     + 2*b24*b369 + 2*b25*b42 - 2*b25 - 2*b42 - 2*b25*b56 + 2*b25*b92 - 4*b92
     + 2*b25*b190 + 2*b26*b27 - 2*b26 - 2*b27 - 2*b26*b44 - 2*b44 + 2*b26*b272
     - 2*b272 + 2*b26*b380 + 2*b27*b62 - 4*b62 + 2*b28*b29 - 2*b28 - 2*b29 + 2*
    b28*b52 - 2*b52 + 2*b28*b108 - 4*b108 - 2*b28*b319 + 2*b29*b53 - 2*b53 - 2*
    b29*b155 - 2*b155 + 2*b29*b338 + 2*b30*b190 - 4*b30 + 2*b30*b226 - 4*b226
     + 2*b30*b260 - 4*b260 + 2*b30*b359 + 2*b31*b58 - 2*b31 - 4*b58 + 2*b31*
    b115 - 4*b115 + 2*b31*b226 - 2*b31*b342 - 2*b32*b33 - 2*b32 + 2*b32*b60 - 4
    *b60 + 2*b32*b79 - 4*b79 + 2*b32*b390 + 2*b33*b34 - 2*b34 + 2*b33*b238 - 2*
    b238 + 2*b34*b79 + 2*b35*b36 - 2*b35 - 2*b36 - 2*b35*b365 + 2*b35*b374 + 2*
    b35*b402 + 2*b36*b209 - 4*b209 - 2*b36*b296 + 2*b36*b403 + 2*b37*b177 - 2*
    b37 + 2*b37*b296 + 2*b37*b317 - 2*b37*b366 + 2*b38*b39 - 4*b38 - 4*b39 + 2*
    b38*b309 + 2*b38*b325 + 2*b38*b395 + 2*b39*b275 + 2*b39*b338 + 2*b39*b340
     + 2*b40*b226 - 2*b40 + 2*b40*b262 - 2*b262 - 2*b40*b275 + 2*b40*b351 + 2*
    b41*b75 - 4*b41 + 2*b41*b138 - 4*b138 + 2*b41*b262 + 2*b41*b342 + 2*b42*
    b228 - 4*b228 - 2*b42*b267 + 2*b267 + 2*b42*b353 + 2*b43*b44 - 2*b43 + 2*
    b43*b393 - 2*b43*b396 + 2*b43*b397 + 2*b44*b77 - 4*b77 + 2*b44*b100 - 2*
    b100 + 2*b45*b46 - 2*b46 + 2*b45*b199 - 4*b199 - 2*b45*b393 + 2*b46*b100 + 
    2*b47*b48 + 2*b47 - 2*b48 - 2*b47*b205 - 2*b47*b383 - 2*b47*b385 + 2*b48*
    b49 - 2*b49 - 2*b48*b287 + 2*b48*b407 + 2*b49*b246 - 4*b246 - 2*b49*b286 + 
    2*b49*b409 + 2*b50*b51 - 2*b50 + 2*b50*b149 + 2*b50*b304 - 2*b50*b378 - 2*
    b51*b176 + 2*b176 + 2*b51*b410 + 2*b52*b54 - 4*b54 + 2*b52*b87 - 2*b87 - 2*
    b52*b157 + 4*b157 + 2*b53*b300 + 2*b53*b320 - 2*b53*b399 + 2*b54*b55 + 2*
    b55 + 2*b54*b389 + 2*b54*b399 - 2*b55*b221 + 2*b221 - 2*b55*b223 + 2*b223
     - 2*b55*b275 + 2*b56*b57 - 2*b57 + 2*b57*b92 + 2*b57*b164 - 4*b164 - 2*b57
    *b263 - 2*b263 + 2*b58*b93 - 4*b93 + 2*b58*b343 + 2*b58*b371 + 2*b59*b93 - 
    2*b59 + 2*b59*b276 + 2*b59*b280 - 2*b59*b392 + 2*b60*b61 + 2*b60*b96 - 2*
    b96 + 2*b60*b396 + 2*b61*b97 - 4*b97 + 2*b61*b121 - 2*b121 + 2*b62*b63 - 2*
    b63 + 2*b62*b239 - 4*b239 + 2*b62*b393 + 2*b63*b121 + 2*b64*b66 - 2*b64 - 4
    *b66 + 2*b64*b334 + 2*b65*b145 - 2*b65 - 2*b145 + 2*b65*b173 - 2*b173 + 2*
    b65*b344 - 2*b65*b408 + 2*b66*b205 + 2*b66*b401 + 2*b66*b408 + 2*b67*b68 - 
    4*b67 - 2*b68 + 2*b67*b174 - 2*b174 + 2*b67*b365 + 2*b67*b387 + 2*b68*b127
     + 2*b127 - 2*b68*b281 + 2*b68*b296 + 2*b69*b70 - 2*b69 - 2*b69*b105 + 2*
    b105 + 2*b69*b314 + 2*b69*b316 + 2*b70*b128 - 2*b128 - 2*b70*b211 + 2*b211
     + 2*b71*b107 - 4*b71 - 2*b107 + 2*b71*b128 + 2*b71*b152 + 2*b152 + 2*b71*
    b297 - 2*b72*b311 + 2*b72 + 2*b72*b341 - 2*b72*b359 - 2*b72*b414 + 2*b73*
    b74 - 2*b74 + 2*b74*b115 + 2*b74*b192 - 4*b192 - 2*b74*b227 - 2*b227 + 2*
    b75*b267 + 2*b75*b332 + 2*b76*b195 + 2*b76 + 2*b195 - 2*b76*b267 - 2*b76*
    b276 - 2*b76*b397 + 2*b77*b78 - 2*b78 + 2*b77*b118 - 2*b118 + 2*b77*b391 + 
    2*b78*b119 - 4*b119 + 2*b78*b144 - 2*b144 - 2*b78*b362 + 2*b79*b80 - 2*b80
     + 2*b79*b273 - 4*b273 + 2*b80*b144 + 2*b81*b206 + 2*b81 - 4*b206 - 2*b81*
    b335 - 2*b81*b402 - 2*b81*b416 + 2*b82*b83 - 4*b82 - 2*b83 + 2*b82*b206 + 2
    *b82*b376 + 2*b82*b394 + 2*b83*b105 - 2*b83*b279 + 2*b83*b304 + 2*b84*b86
     - 2*b84*b127 + 2*b84*b307 - 2*b85*b150 + 2*b85 - 2*b150 - 2*b85*b249 - 2*
    b249 - 2*b85*b297 + 2*b85*b345 + 2*b86*b150 - 2*b86*b248 + 2*b248 + 2*b87*
    b182 - 2*b182 - 2*b87*b219 + 2*b219 + 2*b87*b349 - 2*b88*b89 + 2*b88 + 2*
    b89 - 2*b88*b291 + 2*b88*b302 - 2*b88*b389 + 2*b89*b352 - 2*b89*b369 - 2*
    b89*b418 + 2*b90*b91 - 2*b91 - 2*b90*b371 + 2*b91*b138 - 2*b91*b191 - 2*
    b191 + 2*b91*b230 - 4*b230 + 2*b92*b94 - 2*b94 + 2*b92*b232 + 2*b232 + 2*
    b93*b95 - 4*b95 + 2*b93*b231 - 4*b231 + 2*b94*b95 + 2*b94*b230 - 2*b94*b326
     + 2*b95*b96 + 2*b95*b278 + 2*b96*b143 - 4*b143 - 2*b96*b293 + 2*b97*b99 - 
    4*b99 + 2*b97*b142 - 2*b142 + 2*b97*b392 - 2*b98*b121 + 2*b98 + 2*b98*b170
     - 4*b170 - 2*b98*b277 - 2*b98*b285 + 2*b99*b143 + 2*b99*b170 + 2*b99*b362
     + 2*b100*b101 - 2*b101 - 2*b100*b294 + 2*b101*b170 + 2*b102*b243 + 2*b102
     - 4*b243 - 2*b102*b328 - 2*b102*b398 - 2*b102*b419 + 2*b103*b104 - 4*b103
     - 4*b104 + 2*b103*b243 + 2*b103*b384 + 2*b103*b398 + 2*b104*b279 + 2*b104*
    b314 + 2*b104*b378 - 2*b105*b248 - 2*b105*b384 - 2*b106*b215 - 2*b106 + 2*
    b215 + 2*b106*b348 + 2*b106*b410 + 2*b106*b420 + 2*b107*b108 - 2*b107*b151
     - 2*b151 + 2*b107*b182 + 2*b108*b110 - 2*b110 + 2*b108*b348 - 2*b109*b185
     - 2*b109 + 2*b185 + 2*b109*b309 + 2*b109*b337 + 2*b109*b368 + 2*b110*b183
     - 2*b183 + 2*b110*b185 - 2*b110*b389 - 2*b111*b112 + 4*b111 + 2*b112 - 2*
    b111*b257 + 2*b257 - 2*b111*b300 - 2*b111*b302 + 2*b112*b360 - 2*b112*b379
     - 2*b112*b422 + 2*b113*b114 - 2*b114 + 2*b113*b228 - 2*b114*b162 - 2*b162
     + 2*b114*b164 + 2*b114*b266 - 4*b266 + 2*b115*b116 - 4*b116 + 2*b115*b361
     + 2*b116*b266 + 2*b116*b326 + 2*b116*b415 - 2*b117*b118 + 2*b117 + 2*b117*
    b233 - 4*b233 - 2*b117*b278 - 2*b117*b361 + 2*b118*b169 - 4*b169 + 2*b118*
    b415 + 2*b119*b120 + 2*b119*b168 - 2*b168 + 2*b119*b397 + 2*b120*b169 + 2*
    b120*b200 - 4*b200 + 2*b121*b122 - 2*b122 + 2*b122*b200 + 2*b123*b124 + 2*
    b123 - 2*b124 - 2*b123*b322 - 2*b123*b394 - 2*b123*b423 + 2*b124*b125 - 4*
    b125 - 2*b124*b281 + 2*b124*b327 + 2*b125*b126 + 2*b125*b323 + 2*b125*b402
     + 2*b126*b281 + 2*b126*b366 - 2*b127*b211 - 2*b127*b323 + 2*b128*b129 - 2*
    b129 - 2*b128*b308 - 2*b129*b252 + 2*b252 + 2*b129*b336 + 2*b129*b424 - 2*
    b130*b290 + 2*b130 - 2*b130*b330 + 2*b130*b411 - 2*b130*b417 - 2*b131*b156
     - 2*b131 + 2*b156 + 2*b131*b300 + 2*b131*b330 + 2*b131*b358 + 2*b132*b156
     - 2*b132 + 2*b132*b217 - 2*b217 - 2*b132*b395 + 2*b132*b417 - 2*b133*b219
     + 4*b133 - 2*b133*b309 - 2*b133*b310 - 2*b133*b386 + 2*b134*b160 - 2*b160
     - 2*b134*b302 + 2*b134*b386 + 2*b135*b137 - 4*b137 + 2*b135*b371 + 2*b136*
    b137 - 4*b136 + 2*b136*b160 + 2*b136*b228 + 2*b136*b331 + 2*b137*b139 - 2*
    b139 + 2*b137*b192 + 2*b138*b140 - 4*b140 + 2*b138*b353 + 2*b139*b140 + 2*
    b139*b229 - 4*b229 - 2*b139*b276 + 2*b140*b194 + 2*b194 + 2*b140*b412 - 2*
    b141*b142 + 2*b141 + 2*b141*b193 - 2*b193 - 2*b141*b235 - 2*b141*b353 + 2*
    b142*b197 - 4*b197 + 2*b142*b412 + 2*b143*b196 - 2*b196 + 2*b143*b272 - 2*
    b144*b198 + 2*b144*b427 + 2*b145*b146 - 4*b146 + 2*b146*b303 + 2*b146*b382
     + 2*b146*b388 + 2*b147*b245 - 2*b147 - 2*b245 - 2*b147*b279 + 2*b147*b333
     + 2*b147*b388 + 2*b148*b176 + 2*b148 - 2*b148*b287 - 2*b148*b356 - 2*b148*
    b429 - 2*b149*b430 + 2*b150*b151 + 2*b150*b411 + 2*b151*b329 + 2*b151*b430
     - 2*b152*b153 - 2*b153 - 2*b152*b299 - 2*b152*b337 + 2*b153*b155 + 2*b153*
    b329 + 2*b153*b413 + 2*b154*b291 + 2*b154*b349 - 2*b154*b350 + 2*b155*b254
     - 2*b254 + 2*b155*b350 - 2*b156*b186 + 2*b186 - 2*b156*b426 - 2*b157*b158
     - 2*b158 - 2*b157*b185 - 2*b157*b320 + 2*b158*b159 + 2*b158*b369 + 2*b158*
    b426 + 2*b159*b189 - 2*b189 + 2*b159*b302 + 2*b160*b162 - 2*b160*b360 + 2*
    b161*b163 - 4*b163 + 2*b162*b163 + 2*b162*b189 + 2*b163*b165 - 4*b165 + 2*
    b163*b230 + 2*b164*b166 - 4*b166 + 2*b164*b343 + 2*b165*b166 + 2*b165*b265
     - 4*b265 + 2*b165*b276 + 2*b166*b167 + 2*b167 + 2*b166*b406 - 2*b167*b168
     - 2*b167*b195 - 2*b167*b343 + 2*b168*b237 - 2*b237 + 2*b168*b406 + 2*b169*
    b236 - 2*b236 + 2*b169*b238 + 2*b170*b432 - 2*b171*b313 + 2*b171 - 2*b171*
    b423 - 2*b172*b303 + 4*b172 - 2*b172*b381 - 2*b172*b382 - 2*b172*b383 + 2*
    b173*b175 - 4*b175 + 2*b173*b334 - 2*b173*b387 + 2*b174*b208 - 2*b208 - 2*
    b174*b303 + 2*b174*b408 + 2*b175*b208 + 2*b175*b279 + 2*b175*b383 - 2*b176*
    b409 - 2*b176*b431 - 2*b177*b367 - 2*b178*b181 - 2*b181 - 2*b178*b297 - 2*
    b178*b298 + 2*b179*b181 - 4*b179 + 2*b179*b252 + 2*b179*b367 + 2*b179*b420
     - 2*b180*b183 + 2*b180 + 2*b180*b251 - 4*b251 - 2*b180*b349 - 2*b180*b411
     + 2*b181*b183 + 2*b181*b324 - 2*b182*b184 - 2*b184 + 2*b182*b298 + 2*b183*
    b184 + 2*b184*b339 + 2*b184*b395 - 2*b185*b422 - 2*b186*b187 - 2*b187 + 2*
    b186*b258 - 2*b258 - 2*b186*b325 + 2*b187*b188 + 2*b187*b359 + 2*b187*b422
     + 2*b188*b225 - 2*b225 + 2*b188*b310 + 2*b189*b191 - 2*b189*b352 + 2*b190*
    b264 - 2*b264 + 2*b191*b225 + 2*b191*b264 + 2*b192*b193 + 2*b192*b332 + 2*
    b193*b400 - 2*b193*b434 - 2*b194*b196 - 2*b194*b280 - 2*b194*b332 - 2*b195*
    b271 - 2*b271 - 2*b195*b277 + 2*b196*b271 + 2*b196*b400 + 2*b197*b199 + 2*
    b197*b270 - 4*b270 + 2*b197*b272 + 2*b198*b201 + 2*b198*b277 + 2*b199*b201
     + 2*b199*b271 + 2*b200*b202 - 2*b202 + 2*b200*b294 + 2*b201*b202 - 2*b203*
    b322 + 2*b203 - 2*b203*b419 - 2*b204*b312 + 4*b204 - 2*b204*b372 - 2*b204*
    b373 - 2*b204*b375 + 2*b205*b207 - 4*b207 + 2*b206*b209 + 2*b206*b312 + 2*
    b207*b209 + 2*b207*b281 + 2*b207*b375 + 2*b208*b305 - 2*b208*b433 + 2*b209*
    b433 + 2*b210*b212 - 2*b212 + 2*b210*b376 + 2*b210*b433 + 2*b211*b366 - 2*
    b211*b425 - 2*b212*b308 + 2*b212*b403 + 2*b212*b425 + 2*b213*b356 - 2*b213*
    b357 + 2*b214*b215 - 4*b214 + 2*b214*b216 - 2*b216 + 2*b214*b357 + 2*b214*
    b424 - 2*b215*b217 - 2*b215*b358 + 2*b216*b217 - 2*b216*b318 + 2*b216*b319
     + 2*b217*b218 - 2*b218 + 2*b218*b220 - 2*b220 - 2*b218*b368 + 2*b218*b389
     + 2*b219*b413 - 2*b219*b418 + 2*b220*b221 - 2*b220*b301 + 2*b220*b418 - 2*
    b221*b222 - 2*b222 - 2*b221*b350 + 2*b222*b224 + 2*b222*b351 + 2*b222*b418
     - 2*b223*b261 - 2*b261 - 2*b223*b331 + 2*b223*b399 + 2*b224*b261 + 2*b224*
    b320 + 2*b225*b227 - 2*b225*b341 + 2*b226*b229 + 2*b227*b229 + 2*b227*b261
     + 2*b228*b231 + 2*b229*b231 + 2*b230*b233 + 2*b231*b233 - 2*b232*b234 - 2*
    b234 - 2*b232*b293 - 2*b232*b370 + 2*b233*b234 + 2*b234*b236 + 2*b234*b396
     + 2*b235*b293 - 2*b235*b295 + 2*b236*b295 - 2*b236*b326 + 2*b237*b238 + 2*
    b237*b239 - 2*b237*b280 - 2*b238*b274 + 2*b274 + 2*b239*b274 + 2*b239*b295
     - 2*b240*b328 + 2*b240 - 2*b240*b416 - 2*b241*b242 + 4*b241 - 2*b242 - 2*
    b241*b321 - 2*b241*b363 - 2*b241*b364 + 2*b242*b244 + 2*b242*b374 + 2*b242*
    b416 + 2*b243*b246 + 2*b243*b321 + 2*b244*b246 + 2*b244*b303 + 2*b245*b315
     + 2*b245*b407 - 2*b245*b429 + 2*b246*b429 + 2*b247*b249 + 2*b247*b384 + 2*
    b247*b429 + 2*b248*b378 - 2*b248*b421 + 2*b249*b409 + 2*b249*b421 + 2*b250*
    b297 + 2*b250*b345 - 2*b250*b347 + 2*b251*b253 + 2*b251*b347 + 2*b251*b430
     - 2*b252*b254 - 2*b252*b368 + 2*b253*b254 + 2*b253*b318 + 2*b254*b256 - 2*
    b256 - 2*b255*b258 - 2*b255*b309 - 2*b255*b324 + 2*b256*b257 + 2*b256*b258
     - 2*b256*b358 - 2*b257*b413 - 2*b257*b414 + 2*b258*b414 + 2*b259*b260 - 2*
    b259 - 2*b259*b338 + 2*b259*b340 + 2*b259*b414 + 2*b260*b325 + 2*b260*b405
     + 2*b261*b263 + 2*b262*b265 - 2*b262*b405 + 2*b263*b265 + 2*b263*b405 + 2*
    b264*b266 - 2*b264*b434 + 2*b265*b434 + 2*b266*b268 - 4*b268 - 2*b267*b269
     - 2*b269 + 2*b268*b269 + 2*b268*b293 + 2*b268*b434 + 2*b269*b270 + 2*b269*
    b391 + 2*b270*b285 + 2*b270*b326 + 2*b271*b273 - 2*b272*b428 + 2*b273*b285
     + 2*b273*b428 - 2*b274*b432 - 2*b274*b435 + 2*b275*b331 + 2*b277*b278 - 2*
    b278*b285 - 2*b282*b283 + 2*b282*b284 - 2*b282*b349 + 2*b282*b358 - 2*b283*
    b336 - 2*b284*b347 - 2*b284*b348 + 2*b286*b287 - 2*b286*b356 - 2*b288*b289
     + 2*b288*b290 - 2*b288*b337 + 2*b288*b368 + 2*b289*b306 - 2*b289*b329 - 2*
    b290*b357 - 2*b291*b292 + 2*b291*b311 + 2*b292*b319 + 2*b292*b337 - 2*b292*
    b339 - 2*b294*b295 - 2*b296*b345 + 2*b298*b299 - 2*b298*b330 - 2*b299*b367
     - 2*b300*b301 + 2*b301*b324 + 2*b301*b330 - 2*b304*b305 + 2*b305*b377 - 2*
    b305*b403 - 2*b306*b307 + 2*b306*b308 - 2*b306*b318 - 2*b307*b420 + 2*b308*
    b356 + 2*b310*b311 - 2*b310*b360 - 2*b311*b395 + 2*b312*b313 - 2*b312*b407
     + 2*b313*b381 - 2*b313*b388 - 2*b314*b315 + 2*b315*b385 - 2*b315*b409 - 2*
    b316*b424 - 2*b317*b404 - 2*b317*b410 - 2*b319*b336 - 2*b320*b352 + 2*b321*
    b322 - 2*b321*b402 + 2*b322*b372 - 2*b324*b329 - 2*b325*b341 + 2*b327*b328
     - 2*b327*b398 + 2*b328*b363 - 2*b331*b342 - 2*b332*b415 - 2*b333*b334 + 2*
    b333*b335 - 2*b333*b394 - 2*b334*b344 + 2*b335*b354 - 2*b335*b401 + 2*b336*
    b417 - 2*b338*b339 + 2*b339*b422 - 2*b340*b405 - 2*b343*b412 - 2*b345*b346
     + 2*b346*b365 + 2*b346*b404 - 2*b346*b433 + 2*b347*b421 + 2*b350*b426 - 2*
    b351*b399 - 2*b353*b406 + 2*b355*b416 + 2*b357*b425 + 2*b361*b370 - 2*b361*
    b400 - 2*b362*b380 + 2*b364*b419 - 2*b365*b366 + 2*b367*b431 - 2*b370*b371
     + 2*b373*b423 - 2*b374*b375 - 2*b374*b377 + 2*b375*b419 - 2*b376*b377 - 2*
    b376*b378 + 2*b377*b398 + 2*b379*b386 + 2*b383*b423 - 2*b384*b385 + 2*b385*
    b394 - 2*b386*b426 - 2*b387*b388 - 2*b390*b391 + 2*b390*b392 - 2*b390*b393
     - 2*b391*b406 - 2*b392*b412 - 2*b396*b400 - 2*b397*b415 - 2*b403*b404 + 2*
    b404*b431 - 2*b407*b408 - 2*b410*b411 - 2*b413*b417 - 2*b420*b421 - 2*b424*
    b425 - 2*b427*b428 + 2*b428*b435 - 2*b430*b431 + x436 <= 0;