#  MINLP written by GAMS Convert at 01/12/18 13:42:53
#  
#  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
#        781        1      780        0        0        0        0        0
#  FX      0        0        0        0        0        0        0        0
#  
#  Nonzero counts
#      Total    const       NL      DLL
#        781        1      780        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 b436 binary >= 0, <= 1;
var b437 binary >= 0, <= 1;
var b438 binary >= 0, <= 1;
var b439 binary >= 0, <= 1;
var b440 binary >= 0, <= 1;
var b441 binary >= 0, <= 1;
var b442 binary >= 0, <= 1;
var b443 binary >= 0, <= 1;
var b444 binary >= 0, <= 1;
var b445 binary >= 0, <= 1;
var b446 binary >= 0, <= 1;
var b447 binary >= 0, <= 1;
var b448 binary >= 0, <= 1;
var b449 binary >= 0, <= 1;
var b450 binary >= 0, <= 1;
var b451 binary >= 0, <= 1;
var b452 binary >= 0, <= 1;
var b453 binary >= 0, <= 1;
var b454 binary >= 0, <= 1;
var b455 binary >= 0, <= 1;
var b456 binary >= 0, <= 1;
var b457 binary >= 0, <= 1;
var b458 binary >= 0, <= 1;
var b459 binary >= 0, <= 1;
var b460 binary >= 0, <= 1;
var b461 binary >= 0, <= 1;
var b462 binary >= 0, <= 1;
var b463 binary >= 0, <= 1;
var b464 binary >= 0, <= 1;
var b465 binary >= 0, <= 1;
var b466 binary >= 0, <= 1;
var b467 binary >= 0, <= 1;
var b468 binary >= 0, <= 1;
var b469 binary >= 0, <= 1;
var b470 binary >= 0, <= 1;
var b471 binary >= 0, <= 1;
var b472 binary >= 0, <= 1;
var b473 binary >= 0, <= 1;
var b474 binary >= 0, <= 1;
var b475 binary >= 0, <= 1;
var b476 binary >= 0, <= 1;
var b477 binary >= 0, <= 1;
var b478 binary >= 0, <= 1;
var b479 binary >= 0, <= 1;
var b480 binary >= 0, <= 1;
var b481 binary >= 0, <= 1;
var b482 binary >= 0, <= 1;
var b483 binary >= 0, <= 1;
var b484 binary >= 0, <= 1;
var b485 binary >= 0, <= 1;
var b486 binary >= 0, <= 1;
var b487 binary >= 0, <= 1;
var b488 binary >= 0, <= 1;
var b489 binary >= 0, <= 1;
var b490 binary >= 0, <= 1;
var b491 binary >= 0, <= 1;
var b492 binary >= 0, <= 1;
var b493 binary >= 0, <= 1;
var b494 binary >= 0, <= 1;
var b495 binary >= 0, <= 1;
var b496 binary >= 0, <= 1;
var b497 binary >= 0, <= 1;
var b498 binary >= 0, <= 1;
var b499 binary >= 0, <= 1;
var b500 binary >= 0, <= 1;
var b501 binary >= 0, <= 1;
var b502 binary >= 0, <= 1;
var b503 binary >= 0, <= 1;
var b504 binary >= 0, <= 1;
var b505 binary >= 0, <= 1;
var b506 binary >= 0, <= 1;
var b507 binary >= 0, <= 1;
var b508 binary >= 0, <= 1;
var b509 binary >= 0, <= 1;
var b510 binary >= 0, <= 1;
var b511 binary >= 0, <= 1;
var b512 binary >= 0, <= 1;
var b513 binary >= 0, <= 1;
var b514 binary >= 0, <= 1;
var b515 binary >= 0, <= 1;
var b516 binary >= 0, <= 1;
var b517 binary >= 0, <= 1;
var b518 binary >= 0, <= 1;
var b519 binary >= 0, <= 1;
var b520 binary >= 0, <= 1;
var b521 binary >= 0, <= 1;
var b522 binary >= 0, <= 1;
var b523 binary >= 0, <= 1;
var b524 binary >= 0, <= 1;
var b525 binary >= 0, <= 1;
var b526 binary >= 0, <= 1;
var b527 binary >= 0, <= 1;
var b528 binary >= 0, <= 1;
var b529 binary >= 0, <= 1;
var b530 binary >= 0, <= 1;
var b531 binary >= 0, <= 1;
var b532 binary >= 0, <= 1;
var b533 binary >= 0, <= 1;
var b534 binary >= 0, <= 1;
var b535 binary >= 0, <= 1;
var b536 binary >= 0, <= 1;
var b537 binary >= 0, <= 1;
var b538 binary >= 0, <= 1;
var b539 binary >= 0, <= 1;
var b540 binary >= 0, <= 1;
var b541 binary >= 0, <= 1;
var b542 binary >= 0, <= 1;
var b543 binary >= 0, <= 1;
var b544 binary >= 0, <= 1;
var b545 binary >= 0, <= 1;
var b546 binary >= 0, <= 1;
var b547 binary >= 0, <= 1;
var b548 binary >= 0, <= 1;
var b549 binary >= 0, <= 1;
var b550 binary >= 0, <= 1;
var b551 binary >= 0, <= 1;
var b552 binary >= 0, <= 1;
var b553 binary >= 0, <= 1;
var b554 binary >= 0, <= 1;
var b555 binary >= 0, <= 1;
var b556 binary >= 0, <= 1;
var b557 binary >= 0, <= 1;
var b558 binary >= 0, <= 1;
var b559 binary >= 0, <= 1;
var b560 binary >= 0, <= 1;
var b561 binary >= 0, <= 1;
var b562 binary >= 0, <= 1;
var b563 binary >= 0, <= 1;
var b564 binary >= 0, <= 1;
var b565 binary >= 0, <= 1;
var b566 binary >= 0, <= 1;
var b567 binary >= 0, <= 1;
var b568 binary >= 0, <= 1;
var b569 binary >= 0, <= 1;
var b570 binary >= 0, <= 1;
var b571 binary >= 0, <= 1;
var b572 binary >= 0, <= 1;
var b573 binary >= 0, <= 1;
var b574 binary >= 0, <= 1;
var b575 binary >= 0, <= 1;
var b576 binary >= 0, <= 1;
var b577 binary >= 0, <= 1;
var b578 binary >= 0, <= 1;
var b579 binary >= 0, <= 1;
var b580 binary >= 0, <= 1;
var b581 binary >= 0, <= 1;
var b582 binary >= 0, <= 1;
var b583 binary >= 0, <= 1;
var b584 binary >= 0, <= 1;
var b585 binary >= 0, <= 1;
var b586 binary >= 0, <= 1;
var b587 binary >= 0, <= 1;
var b588 binary >= 0, <= 1;
var b589 binary >= 0, <= 1;
var b590 binary >= 0, <= 1;
var b591 binary >= 0, <= 1;
var b592 binary >= 0, <= 1;
var b593 binary >= 0, <= 1;
var b594 binary >= 0, <= 1;
var b595 binary >= 0, <= 1;
var b596 binary >= 0, <= 1;
var b597 binary >= 0, <= 1;
var b598 binary >= 0, <= 1;
var b599 binary >= 0, <= 1;
var b600 binary >= 0, <= 1;
var b601 binary >= 0, <= 1;
var b602 binary >= 0, <= 1;
var b603 binary >= 0, <= 1;
var b604 binary >= 0, <= 1;
var b605 binary >= 0, <= 1;
var b606 binary >= 0, <= 1;
var b607 binary >= 0, <= 1;
var b608 binary >= 0, <= 1;
var b609 binary >= 0, <= 1;
var b610 binary >= 0, <= 1;
var b611 binary >= 0, <= 1;
var b612 binary >= 0, <= 1;
var b613 binary >= 0, <= 1;
var b614 binary >= 0, <= 1;
var b615 binary >= 0, <= 1;
var b616 binary >= 0, <= 1;
var b617 binary >= 0, <= 1;
var b618 binary >= 0, <= 1;
var b619 binary >= 0, <= 1;
var b620 binary >= 0, <= 1;
var b621 binary >= 0, <= 1;
var b622 binary >= 0, <= 1;
var b623 binary >= 0, <= 1;
var b624 binary >= 0, <= 1;
var b625 binary >= 0, <= 1;
var b626 binary >= 0, <= 1;
var b627 binary >= 0, <= 1;
var b628 binary >= 0, <= 1;
var b629 binary >= 0, <= 1;
var b630 binary >= 0, <= 1;
var b631 binary >= 0, <= 1;
var b632 binary >= 0, <= 1;
var b633 binary >= 0, <= 1;
var b634 binary >= 0, <= 1;
var b635 binary >= 0, <= 1;
var b636 binary >= 0, <= 1;
var b637 binary >= 0, <= 1;
var b638 binary >= 0, <= 1;
var b639 binary >= 0, <= 1;
var b640 binary >= 0, <= 1;
var b641 binary >= 0, <= 1;
var b642 binary >= 0, <= 1;
var b643 binary >= 0, <= 1;
var b644 binary >= 0, <= 1;
var b645 binary >= 0, <= 1;
var b646 binary >= 0, <= 1;
var b647 binary >= 0, <= 1;
var b648 binary >= 0, <= 1;
var b649 binary >= 0, <= 1;
var b650 binary >= 0, <= 1;
var b651 binary >= 0, <= 1;
var b652 binary >= 0, <= 1;
var b653 binary >= 0, <= 1;
var b654 binary >= 0, <= 1;
var b655 binary >= 0, <= 1;
var b656 binary >= 0, <= 1;
var b657 binary >= 0, <= 1;
var b658 binary >= 0, <= 1;
var b659 binary >= 0, <= 1;
var b660 binary >= 0, <= 1;
var b661 binary >= 0, <= 1;
var b662 binary >= 0, <= 1;
var b663 binary >= 0, <= 1;
var b664 binary >= 0, <= 1;
var b665 binary >= 0, <= 1;
var b666 binary >= 0, <= 1;
var b667 binary >= 0, <= 1;
var b668 binary >= 0, <= 1;
var b669 binary >= 0, <= 1;
var b670 binary >= 0, <= 1;
var b671 binary >= 0, <= 1;
var b672 binary >= 0, <= 1;
var b673 binary >= 0, <= 1;
var b674 binary >= 0, <= 1;
var b675 binary >= 0, <= 1;
var b676 binary >= 0, <= 1;
var b677 binary >= 0, <= 1;
var b678 binary >= 0, <= 1;
var b679 binary >= 0, <= 1;
var b680 binary >= 0, <= 1;
var b681 binary >= 0, <= 1;
var b682 binary >= 0, <= 1;
var b683 binary >= 0, <= 1;
var b684 binary >= 0, <= 1;
var b685 binary >= 0, <= 1;
var b686 binary >= 0, <= 1;
var b687 binary >= 0, <= 1;
var b688 binary >= 0, <= 1;
var b689 binary >= 0, <= 1;
var b690 binary >= 0, <= 1;
var b691 binary >= 0, <= 1;
var b692 binary >= 0, <= 1;
var b693 binary >= 0, <= 1;
var b694 binary >= 0, <= 1;
var b695 binary >= 0, <= 1;
var b696 binary >= 0, <= 1;
var b697 binary >= 0, <= 1;
var b698 binary >= 0, <= 1;
var b699 binary >= 0, <= 1;
var b700 binary >= 0, <= 1;
var b701 binary >= 0, <= 1;
var b702 binary >= 0, <= 1;
var b703 binary >= 0, <= 1;
var b704 binary >= 0, <= 1;
var b705 binary >= 0, <= 1;
var b706 binary >= 0, <= 1;
var b707 binary >= 0, <= 1;
var b708 binary >= 0, <= 1;
var b709 binary >= 0, <= 1;
var b710 binary >= 0, <= 1;
var b711 binary >= 0, <= 1;
var b712 binary >= 0, <= 1;
var b713 binary >= 0, <= 1;
var b714 binary >= 0, <= 1;
var b715 binary >= 0, <= 1;
var b716 binary >= 0, <= 1;
var b717 binary >= 0, <= 1;
var b718 binary >= 0, <= 1;
var b719 binary >= 0, <= 1;
var b720 binary >= 0, <= 1;
var b721 binary >= 0, <= 1;
var b722 binary >= 0, <= 1;
var b723 binary >= 0, <= 1;
var b724 binary >= 0, <= 1;
var b725 binary >= 0, <= 1;
var b726 binary >= 0, <= 1;
var b727 binary >= 0, <= 1;
var b728 binary >= 0, <= 1;
var b729 binary >= 0, <= 1;
var b730 binary >= 0, <= 1;
var b731 binary >= 0, <= 1;
var b732 binary >= 0, <= 1;
var b733 binary >= 0, <= 1;
var b734 binary >= 0, <= 1;
var b735 binary >= 0, <= 1;
var b736 binary >= 0, <= 1;
var b737 binary >= 0, <= 1;
var b738 binary >= 0, <= 1;
var b739 binary >= 0, <= 1;
var b740 binary >= 0, <= 1;
var b741 binary >= 0, <= 1;
var b742 binary >= 0, <= 1;
var b743 binary >= 0, <= 1;
var b744 binary >= 0, <= 1;
var b745 binary >= 0, <= 1;
var b746 binary >= 0, <= 1;
var b747 binary >= 0, <= 1;
var b748 binary >= 0, <= 1;
var b749 binary >= 0, <= 1;
var b750 binary >= 0, <= 1;
var b751 binary >= 0, <= 1;
var b752 binary >= 0, <= 1;
var b753 binary >= 0, <= 1;
var b754 binary >= 0, <= 1;
var b755 binary >= 0, <= 1;
var b756 binary >= 0, <= 1;
var b757 binary >= 0, <= 1;
var b758 binary >= 0, <= 1;
var b759 binary >= 0, <= 1;
var b760 binary >= 0, <= 1;
var b761 binary >= 0, <= 1;
var b762 binary >= 0, <= 1;
var b763 binary >= 0, <= 1;
var b764 binary >= 0, <= 1;
var b765 binary >= 0, <= 1;
var b766 binary >= 0, <= 1;
var b767 binary >= 0, <= 1;
var b768 binary >= 0, <= 1;
var b769 binary >= 0, <= 1;
var b770 binary >= 0, <= 1;
var b771 binary >= 0, <= 1;
var b772 binary >= 0, <= 1;
var b773 binary >= 0, <= 1;
var b774 binary >= 0, <= 1;
var b775 binary >= 0, <= 1;
var b776 binary >= 0, <= 1;
var b777 binary >= 0, <= 1;
var b778 binary >= 0, <= 1;
var b779 binary >= 0, <= 1;
var b780 binary >= 0, <= 1;
var x781;

maximize obj: x781;

subject to

e1: 2*b1*b3 - 2*b1 - 4*b3 - 2*b1*b161 + 2*b161 + 2*b1*b162 - 4*b162 + 2*b1*b484
     + 2*b2*b369 - 2*b2 - 2*b369 - 2*b2*b471 + 2*b471 + 2*b2*b488 + 2*b2*b501
     + 2*b3*b492 + 2*b3*b493 + 2*b3*b511 + 2*b4*b23 - 2*b4 - 2*b23 + 2*b4*b119
     - 2*b119 + 2*b4*b524 - 2*b4*b551 + 2*b5*b103 - 2*b5 - 2*b103 + 2*b5*b498
     - 2*b5*b538 + 2*b5*b539 + 2*b6*b83 - 2*b6 - 2*b83 + 2*b6*b351 + 2*b351 + 2
    *b6*b491 - 2*b6*b547 + 2*b7*b84 - 2*b7 - 2*b84 + 2*b7*b207 - 2*b207 + 2*b7*
    b506 - 2*b7*b555 + 2*b8*b233 - 2*b8 - 2*b233 - 2*b8*b263 + 4*b263 + 2*b8*
    b301 - 4*b301 + 2*b8*b533 + 2*b9*b104 - 2*b9 - 2*b104 + 2*b9*b498 + 2*b9*
    b499 - 2*b9*b568 + 2*b10*b267 - 2*b10 - 2*b267 - 2*b10*b300 + 4*b300 + 2*
    b10*b338 - 4*b338 + 2*b10*b543 + 2*b11*b129 - 2*b11 - 2*b129 - 2*b11*b350
     + 2*b350 + 2*b11*b491 + 2*b11*b507 - 2*b12*b279 - 2*b12 + 2*b279 + 2*b12*
    b282 - 2*b282 + 2*b12*b400 - 2*b400 + 2*b12*b541 + 2*b13*b152 - 2*b13 - 2*
    b152 + 2*b13*b207 - 2*b13*b396 + 2*b396 + 2*b13*b519 + 2*b14*b243 - 2*b14
     - 2*b243 - 2*b14*b313 + 2*b313 + 2*b14*b450 - 4*b450 + 2*b14*b453 + 2*b453
     + 2*b15*b109 - 2*b15 - 2*b109 - 2*b15*b460 + 4*b460 + 2*b15*b600 + 2*b15*
    b601 - 2*b16*b41 - 2*b16 + 2*b41 + 2*b16*b132 - 2*b132 + 2*b16*b613 + 2*b16
    *b614 + 2*b17*b27 - 2*b17 - 2*b27 + 2*b17*b372 - 4*b372 - 2*b18*b69 - 2*b18
     - 2*b69 + 2*b18*b310 - 2*b310 + 2*b18*b445 - 2*b445 + 2*b18*b555 + 2*b19*
    b90 - 2*b19 - 2*b90 + 2*b19*b156 - 4*b156 - 2*b19*b623 + 2*b19*b624 + 2*b20
    *b276 - 2*b20 - 2*b276 + 2*b20*b396 + 2*b20*b547 - 2*b20*b620 + 2*b21*b109
     - 2*b21 + 2*b21*b185 - 4*b185 + 2*b21*b215 - 4*b215 - 2*b21*b634 + 2*b22*
    b37 - 2*b22 - 2*b37 + 2*b22*b636 + 2*b23*b118 - 4*b118 + 2*b23*b265 - 2*
    b265 - 2*b23*b380 - 2*b380 + 2*b24*b238 - 2*b24 - 2*b238 + 2*b24*b350 + 2*
    b24*b538 - 2*b24*b631 + 2*b25*b132 - 2*b25 + 2*b25*b216 - 4*b216 + 2*b25*
    b247 - 4*b247 - 2*b25*b642 + 2*b26*b73 - 2*b26 - 4*b73 - 2*b26*b109 + 2*b26
    *b216 + 2*b26*b643 + 2*b27*b28 - 2*b28 - 2*b27*b94 - 2*b94 + 2*b27*b165 - 4
    *b165 + 2*b28*b46 - 2*b46 + 2*b29*b239 - 2*b29 - 2*b239 + 2*b29*b529 + 2*
    b29*b568 - 2*b29*b640 + 2*b30*b156 - 2*b30 + 2*b30*b248 - 4*b248 + 2*b30*
    b285 - 4*b285 - 2*b30*b649 + 2*b31*b44 - 2*b31 - 2*b44 - 2*b31*b90 + 2*b31*
    b92 - 4*b92 + 2*b31*b248 + 2*b32*b33 - 2*b32 - 2*b33 - 2*b32*b76 - 2*b76 + 
    2*b32*b192 - 4*b192 + 2*b32*b651 + 2*b33*b62 - 2*b62 + 2*b34*b277 - 2*b34
     - 2*b277 + 2*b34*b517 + 2*b34*b555 - 2*b34*b648 + 2*b35*b185 - 4*b35 + 2*
    b35*b286 - 4*b286 + 2*b35*b322 - 4*b322 + 2*b35*b649 + 2*b36*b59 - 2*b36 - 
    4*b59 + 2*b36*b111 - 4*b111 + 2*b36*b286 - 2*b36*b614 + 2*b37*b38 - 2*b38
     - 2*b37*b61 - 2*b61 + 2*b37*b223 - 4*b223 + 2*b38*b77 - 4*b77 + 2*b39*b51
     + 2*b39 + 2*b51 - 2*b39*b99 + 4*b99 - 2*b39*b495 - 2*b39*b526 + 2*b40*b128
     - 2*b40 - 2*b128 + 2*b40*b311 - 2*b311 + 2*b40*b547 - 2*b40*b657 + 2*b41*
    b89 - 2*b89 - 2*b41*b155 + 2*b155 - 2*b41*b478 + 2*b42*b216 - 4*b42 + 2*b42
    *b323 - 4*b323 + 2*b42*b361 - 4*b361 + 2*b42*b642 + 2*b43*b73 - 2*b43 + 2*
    b43*b134 - 4*b134 + 2*b43*b323 - 2*b43*b601 + 2*b44*b412 - 4*b412 + 2*b44*
    b625 - 2*b44*b650 - 2*b45*b46 - 2*b45 + 2*b45*b75 - 4*b75 + 2*b45*b95 - 4*
    b95 + 2*b45*b673 + 2*b46*b47 - 2*b47 + 2*b46*b256 - 4*b256 + 2*b47*b95 - 2*
    b48*b297 - 2*b48 + 2*b297 + 2*b48*b376 - 4*b376 + 2*b48*b532 + 2*b48*b590
     - 2*b49*b337 + 2*b49 + 4*b337 - 2*b49*b481 + 2*b49*b513 - 2*b49*b627 + 2*
    b50*b52 + 2*b50 - 2*b52 - 2*b50*b122 + 4*b122 - 2*b50*b489 - 2*b50*b535 - 2
    *b51*b496 - 2*b51*b692 - 2*b51*b693 + 2*b52*b504 + 2*b52*b693 - 2*b52*b704
     + 2*b53*b149 - 2*b53 - 4*b149 + 2*b53*b479 + 2*b53*b537 - 2*b53*b620 + 2*
    b54*b103 - 4*b54 + 2*b54*b349 - 4*b349 + 2*b54*b538 + 2*b54*b657 + 2*b55*
    b56 - 2*b55 - 2*b56 + 2*b55*b85 - 2*b85 + 2*b55*b210 - 4*b210 - 2*b55*b548
     + 2*b56*b86 - 2*b86 + 2*b56*b130 - 2*b130 - 2*b56*b705 + 2*b57*b248 - 4*
    b57 + 2*b57*b363 - 2*b363 + 2*b57*b408 - 4*b408 + 2*b57*b634 + 2*b58*b92 - 
    4*b58 + 2*b58*b158 - 4*b158 + 2*b58*b363 + 2*b58*b601 + 2*b59*b159 - 4*b159
     + 2*b59*b615 + 2*b59*b644 + 2*b60*b61 - 2*b60 + 2*b60*b676 - 2*b60*b684 + 
    2*b60*b685 + 2*b61*b93 - 4*b93 + 2*b61*b114 - 4*b114 + 2*b62*b63 - 2*b63 + 
    2*b62*b474 - 2*b474 - 2*b62*b676 + 2*b63*b114 + 2*b64*b333 - 2*b64 - 4*b333
     - 2*b64*b334 + 2*b334 + 2*b64*b523 + 2*b64*b603 - 2*b65*b300 + 2*b65 - 2*
    b65*b485 + 2*b65*b503 - 2*b65*b618 + 2*b66*b68 + 2*b66 - 4*b68 - 2*b66*b145
     + 4*b145 - 2*b66*b270 - 2*b270 - 2*b66*b487 - 2*b67*b504 + 2*b67 + 2*b67*
    b514 - 2*b67*b680 - 2*b67*b681 + 2*b68*b271 - 4*b271 + 2*b68*b515 + 2*b68*
    b681 + 2*b69*b151 - 4*b151 + 2*b69*b309 - 2*b309 + 2*b69*b630 + 2*b70*b83
     - 4*b70 + 2*b70*b395 - 4*b395 + 2*b70*b529 + 2*b70*b648 + 2*b71*b286 - 4*
    b71 + 2*b71*b410 - 2*b410 + 2*b71*b461 - 4*b461 + 2*b71*b623 + 2*b72*b111
     - 4*b72 + 2*b72*b187 - 4*b187 + 2*b72*b410 + 2*b72*b614 + 2*b73*b602 + 2*
    b73*b650 + 2*b74*b480 - 2*b74 + 2*b74*b492 + 2*b74*b650 - 2*b74*b675 + 2*
    b75*b76 + 2*b75*b684 + 2*b75*b696 + 2*b76*b112 - 4*b112 + 2*b76*b137 - 4*
    b137 + 2*b77*b78 - 2*b78 + 2*b77*b421 - 2*b421 + 2*b77*b676 + 2*b78*b137 + 
    2*b79*b296 - 2*b79 - 4*b296 - 2*b79*b377 + 2*b377 + 2*b79*b513 + 2*b79*b616
     - 2*b80*b436 + 4*b80 + 2*b436 - 2*b80*b514 - 2*b80*b515 - 2*b80*b669 + 2*
    b81*b527 - 4*b81 + 2*b81*b553 + 2*b81*b669 + 2*b81*b704 + 2*b82*b84 - 4*b82
     + 2*b82*b444 - 4*b444 + 2*b82*b517 + 2*b82*b640 + 2*b83*b151 - 2*b83*b724
     - 2*b84*b723 + 2*b84*b724 + 2*b85*b87 - 4*b87 + 2*b85*b183 - 2*b183 - 2*
    b85*b358 + 4*b358 + 2*b86*b88 - 4*b88 + 2*b86*b458 - 2*b458 - 2*b86*b599 + 
    2*b87*b88 + 2*b87*b458 + 2*b87*b683 + 2*b88*b360 + 2*b360 + 2*b88*b477 + 2*
    b89*b323 + 2*b89*b463 - 2*b463 - 2*b89*b477 + 2*b90*b91 - 4*b91 + 2*b90*
    b587 + 2*b91*b134 + 2*b91*b218 - 4*b218 + 2*b91*b463 + 2*b92*b468 + 2*b468
     + 2*b92*b589 + 2*b93*b94 + 2*b93*b674 + 2*b93*b708 + 2*b94*b135 - 4*b135
     + 2*b94*b166 - 2*b166 + 2*b95*b96 - 2*b96 + 2*b95*b370 - 4*b370 + 2*b96*
    b166 + 2*b97*b260 - 2*b97 - 4*b260 - 2*b97*b426 + 2*b426 + 2*b97*b503 + 2*
    b97*b626 - 2*b98*b267 + 2*b98 - 2*b98*b269 - 2*b269 + 2*b98*b341 - 4*b341
     - 2*b98*b638 - 2*b99*b527 - 2*b99*b661 - 2*b99*b662 + 2*b100*b536 - 4*b100
     + 2*b100*b565 + 2*b100*b662 + 2*b100*b692 - 2*b101*b578 + 2*b101 + 2*b101*
    b582 - 2*b101*b647 - 2*b101*b648 + 2*b102*b104 - 2*b102 + 2*b102*b128 - 2*
    b102*b483 + 2*b102*b631 + 2*b103*b127 - 2*b127 - 2*b103*b181 - 2*b181 + 2*
    b104*b181 - 2*b104*b733 + 2*b105*b181 - 4*b105 + 2*b105*b209 - 2*b209 + 2*
    b105*b516 + 2*b105*b641 + 2*b106*b108 - 2*b106 - 4*b108 + 2*b106*b154 - 2*
    b154 - 2*b106*b405 + 4*b405 + 2*b106*b541 + 2*b107*b540 - 2*b107 + 2*b107*
    b585 + 2*b107*b694 - 2*b107*b715 + 2*b108*b478 + 2*b108*b672 + 2*b108*b715
     + 2*b109*b110 - 2*b110 + 2*b110*b158 + 2*b110*b251 - 4*b251 - 2*b110*b464
     - 2*b464 + 2*b111*b573 + 2*b111*b635 + 2*b112*b113 - 2*b113 + 2*b112*b163
     - 2*b163 + 2*b112*b675 + 2*b113*b164 - 4*b164 + 2*b113*b193 - 2*b193 - 2*
    b113*b636 + 2*b114*b115 - 2*b115 + 2*b114*b422 - 4*b422 + 2*b115*b193 - 2*
    b116*b117 - 2*b116 + 2*b117 + 2*b116*b227 - 4*b227 + 2*b116*b494 + 2*b116*
    b637 + 2*b117*b118 - 2*b117*b486 - 2*b117*b737 + 2*b118*b197 + 2*b197 + 2*
    b118*b687 + 2*b119*b121 - 2*b121 + 2*b119*b552 - 2*b119*b678 - 2*b120*b233
     + 2*b120 - 2*b120*b384 + 2*b384 + 2*b120*b386 - 4*b386 - 2*b120*b703 + 2*
    b121*b386 - 2*b121*b495 + 2*b121*b713 - 2*b122*b536 - 2*b122*b654 - 2*b122*
    b655 + 2*b123*b545 - 4*b123 + 2*b123*b577 + 2*b123*b655 + 2*b123*b680 + 2*
    b124*b515 - 2*b124 + 2*b124*b608 + 2*b124*b662 - 2*b124*b732 + 2*b125*b149
     - 4*b125 + 2*b125*b527 + 2*b125*b655 + 2*b125*b732 + 2*b126*b348 + 2*b126
     - 2*b348 - 2*b126*b566 - 2*b126*b656 - 2*b126*b657 + 2*b127*b129 - 2*b127*
    b479 + 2*b127*b620 - 2*b128*b206 - 2*b206 + 2*b128*b528 + 2*b129*b206 - 2*
    b129*b739 - 2*b130*b131 + 2*b131 + 2*b130*b530 + 2*b130*b570 - 2*b131*b460
     + 2*b131*b600 - 2*b131*b741 + 2*b132*b133 - 2*b133 - 2*b132*b644 + 2*b133*
    b187 + 2*b133*b288 - 4*b288 - 2*b133*b411 - 2*b411 + 2*b134*b560 + 2*b134*
    b625 + 2*b135*b136 - 4*b136 + 2*b135*b190 - 2*b190 + 2*b135*b685 + 2*b136*
    b191 - 4*b191 + 2*b136*b224 - 2*b224 + 2*b136*b636 + 2*b137*b138 - 2*b138
     + 2*b137*b475 - 4*b475 + 2*b138*b224 - 2*b139*b140 + 2*b139 + 2*b140 + 2*
    b139*b195 - 4*b195 - 2*b139*b494 - 2*b139*b637 - 2*b140*b482 + 2*b140*b730
     - 2*b140*b744 + 2*b141*b143 - 2*b141 - 2*b143 + 2*b141*b544 + 2*b141*b564
     - 2*b141*b667 - 2*b142*b199 + 2*b142 - 2*b199 - 2*b142*b432 + 2*b432 + 2*
    b142*b434 - 4*b434 - 2*b142*b691 + 2*b143*b434 - 2*b143*b489 + 2*b143*b702
     + 2*b144*b271 - 2*b144 - 2*b144*b436 + 2*b144*b628 + 2*b144*b667 - 2*b145*
    b146 + 2*b146 - 2*b145*b545 - 2*b145*b646 + 2*b146*b148 - 4*b148 - 2*b146*
    b441 + 2*b441 - 2*b146*b746 + 2*b147*b504 - 2*b147 + 2*b147*b593 + 2*b147*
    b669 - 2*b147*b722 + 2*b148*b179 - 4*b179 + 2*b148*b536 + 2*b148*b722 + 2*
    b149*b150 - 2*b150 + 2*b149*b609 + 2*b150*b310 - 2*b150*b483 + 2*b150*b722
     + 2*b151*b152 + 2*b151*b483 + 2*b152*b240 - 2*b240 - 2*b152*b747 + 2*b153*
    b240 - 2*b153 + 2*b153*b279 - 2*b153*b449 + 2*b449 + 2*b153*b724 + 2*b154*
    b281 - 2*b281 - 2*b154*b403 + 2*b403 + 2*b154*b611 - 2*b155*b558 + 2*b155*
    b613 - 2*b155*b749 + 2*b156*b157 - 2*b157 + 2*b156*b412 + 2*b157*b218 + 2*
    b157*b326 - 4*b326 - 2*b157*b364 - 2*b364 + 2*b158*b160 - 4*b160 + 2*b158*
    b615 + 2*b159*b162 + 2*b159*b415 - 4*b415 + 2*b159*b522 + 2*b160*b162 + 2*
    b160*b326 + 2*b160*b559 - 2*b161*b163 + 2*b161*b366 - 2*b366 - 2*b161*b635
     + 2*b162*b163 + 2*b163*b222 - 4*b222 + 2*b164*b165 + 2*b164*b221 - 2*b221
     + 2*b164*b696 + 2*b165*b222 + 2*b165*b257 - 2*b257 + 2*b166*b167 - 2*b167
     - 2*b166*b511 + 2*b167*b257 + 2*b168*b169 - 2*b168 + 2*b169 + 2*b168*b170
     - 4*b170 + 2*b168*b652 - 2*b168*b750 - 2*b169*b503 - 2*b169*b626 - 2*b169*
    b627 + 2*b170*b425 - 4*b425 + 2*b170*b627 + 2*b170*b687 - 2*b171*b298 + 2*
    b171 + 2*b298 - 2*b171*b544 + 2*b171*b730 - 2*b171*b745 - 2*b172*b174 - 2*
    b172 + 2*b174 + 2*b172*b175 - 2*b175 + 2*b172*b339 + 2*b339 + 2*b172*b534
     + 2*b173*b175 - 2*b173 + 2*b173*b383 - 2*b383 - 2*b173*b690 + 2*b173*b745
     + 2*b174*b176 - 2*b176 - 2*b174*b660 - 2*b174*b679 + 2*b175*b176 - 2*b175*
    b487 - 2*b176*b577 + 2*b176*b661 + 2*b177*b178 + 2*b177 - 4*b178 - 2*b177*
    b438 + 2*b438 - 2*b177*b579 - 2*b177*b751 + 2*b178*b203 - 4*b203 + 2*b178*
    b545 + 2*b178*b714 + 2*b179*b180 - 2*b180 + 2*b179*b594 + 2*b179*b630 + 2*
    b180*b276 - 2*b180*b479 + 2*b180*b714 + 2*b181*b182 - 2*b182 + 2*b182*b242
     + 2*b242 - 2*b182*b665 + 2*b182*b752 + 2*b183*b315 - 2*b315 - 2*b183*b357
     + 2*b357 + 2*b183*b598 - 2*b184*b550 + 2*b184 - 2*b184*b623 + 2*b184*b624
     - 2*b184*b754 + 2*b185*b186 - 2*b186 + 2*b185*b644 + 2*b186*b251 - 2*b186*
    b324 - 2*b324 + 2*b186*b365 - 4*b365 + 2*b187*b188 - 4*b188 + 2*b187*b602
     + 2*b188*b365 + 2*b188*b572 + 2*b188*b742 - 2*b189*b190 + 2*b189 + 2*b189*
    b328 - 4*b328 - 2*b189*b471 - 2*b189*b625 + 2*b190*b255 - 4*b255 + 2*b190*
    b742 + 2*b191*b192 + 2*b191*b254 - 2*b254 + 2*b191*b708 + 2*b192*b255 + 2*
    b192*b294 - 4*b294 + 2*b193*b194 - 2*b194 - 2*b193*b501 + 2*b194*b294 + 2*
    b195*b645 + 2*b195*b743 + 2*b195*b744 - 2*b196*b513 + 2*b196 - 2*b196*b616
     + 2*b196*b617 - 2*b196*b618 - 2*b197*b335 + 2*b335 - 2*b197*b534 - 2*b197*
    b738 - 2*b198*b229 - 2*b198 + 2*b229 + 2*b198*b544 + 2*b198*b711 + 2*b198*
    b738 + 2*b199*b201 - 4*b201 + 2*b199*b302 + 2*b302 + 2*b199*b525 + 2*b200*
    b201 - 2*b200 + 2*b200*b431 - 2*b431 - 2*b200*b678 + 2*b200*b738 + 2*b201*
    b202 - 2*b202 + 2*b201*b487 - 2*b202*b565 + 2*b202*b654 + 2*b202*b667 + 2*
    b203*b205 - 4*b205 + 2*b203*b579 + 2*b203*b639 + 2*b204*b205 + 2*b204 - 2*
    b204*b275 - 2*b275 - 2*b204*b567 - 2*b204*b756 + 2*b205*b238 + 2*b205*b483
     + 2*b206*b208 - 2*b208 + 2*b206*b725 + 2*b207*b490 - 2*b207*b597 + 2*b208*
    b597 - 2*b208*b671 + 2*b208*b757 + 2*b209*b210 - 2*b209*b241 - 2*b241 + 2*
    b209*b354 - 2*b354 + 2*b210*b212 - 2*b212 + 2*b210*b597 - 2*b211*b319 - 2*
    b211 + 2*b319 + 2*b211*b354 + 2*b211*b540 + 2*b211*b584 + 2*b212*b319 + 2*
    b212*b401 - 2*b401 - 2*b212*b683 - 2*b213*b214 + 2*b213 + 2*b214 - 2*b213*
    b508 + 2*b213*b542 - 2*b213*b672 + 2*b214*b215 - 2*b214*b634 - 2*b214*b758
     + 2*b215*b531 + 2*b215*b759 + 2*b216*b217 - 2*b217 + 2*b217*b288 + 2*b217*
    b414 - 4*b414 - 2*b217*b760 + 2*b218*b219 - 4*b219 + 2*b218*b589 + 2*b219*
    b291 + 2*b291 + 2*b219*b414 + 2*b219*b735 - 2*b220*b221 + 2*b220 + 2*b220*
    b290 - 4*b290 - 2*b220*b418 + 2*b418 - 2*b220*b615 + 2*b221*b293 - 4*b293
     + 2*b221*b735 + 2*b222*b223 + 2*b222*b292 - 2*b292 + 2*b223*b293 + 2*b223*
    b331 - 4*b331 + 2*b224*b225 - 2*b225 - 2*b224*b493 + 2*b225*b331 + 2*b226*
    b227 - 2*b226 + 2*b226*b637 + 2*b227*b736 + 2*b227*b737 - 2*b228*b523 + 2*
    b228 - 2*b228*b603 + 2*b228*b604 - 2*b228*b606 + 2*b229*b231 - 4*b231 - 2*
    b229*b427 - 2*b427 - 2*b229*b532 - 2*b230*b379 + 4*b230 + 2*b379 - 2*b230*
    b525 - 2*b230*b730 - 2*b230*b731 + 2*b231*b534 + 2*b231*b700 + 2*b231*b731
     + 2*b232*b267 - 2*b232 + 2*b232*b485 + 2*b232*b653 - 2*b232*b668 + 2*b233*
    b234 - 4*b234 + 2*b233*b265 + 2*b234*b235 - 2*b235 + 2*b234*b489 + 2*b234*
    b668 - 2*b235*b553 + 2*b235*b646 + 2*b235*b678 - 2*b236*b442 + 2*b236 + 4*
    b442 - 2*b236*b515 + 2*b236*b554 - 2*b236*b693 + 2*b237*b239 - 2*b237 - 2*
    b237*b442 + 2*b237*b546 + 2*b237*b631 + 2*b238*b682 - 2*b238*b764 - 2*b239*
    b763 + 2*b239*b764 + 2*b240*b241 - 2*b240*b517 + 2*b241*b583 + 2*b241*b765
     - 2*b242*b499 - 2*b242*b548 - 2*b242*b753 - 2*b243*b283 + 2*b283 + 2*b243*
    b530 + 2*b243*b633 + 2*b244*b283 - 2*b244 + 2*b244*b452 - 2*b452 - 2*b244*
    b694 + 2*b244*b753 - 2*b245*b246 + 2*b245 + 2*b246 - 2*b245*b455 + 2*b455
     - 2*b245*b520 + 2*b245*b531 + 2*b246*b247 - 2*b246*b642 - 2*b246*b767 + 2*
    b247*b362 - 2*b362 + 2*b247*b542 + 2*b248*b250 - 4*b250 + 2*b249*b250 - 4*
    b249 + 2*b249*b362 + 2*b249*b412 + 2*b249*b571 + 2*b250*b326 + 2*b250*b467
     - 4*b467 + 2*b251*b252 - 4*b252 + 2*b251*b573 + 2*b252*b253 + 2*b253 + 2*
    b252*b467 + 2*b252*b727 - 2*b253*b254 - 2*b253*b488 - 2*b253*b602 + 2*b254*
    b330 - 4*b330 + 2*b254*b727 + 2*b255*b256 + 2*b255*b329 - 2*b329 + 2*b256*
    b330 + 2*b256*b371 - 4*b371 + 2*b257*b258 - 2*b258 - 2*b257*b369 + 2*b258*
    b371 + 2*b259*b260 - 2*b259 + 2*b259*b626 + 2*b260*b728 + 2*b260*b729 - 2*
    b261*b532 + 2*b261 - 2*b261*b590 + 2*b261*b591 - 2*b261*b592 + 2*b262*b264
     + 2*b262 - 4*b264 - 2*b262*b378 - 2*b378 - 2*b262*b523 - 2*b262*b551 - 2*
    b263*b266 - 2*b266 - 2*b263*b605 - 2*b263*b720 + 2*b264*b266 + 2*b264*b525
     + 2*b264*b689 + 2*b265*b481 - 2*b265*b660 + 2*b266*b660 + 2*b266*b721 + 2*
    b267*b268 - 4*b268 + 2*b268*b270 + 2*b268*b495 + 2*b268*b660 + 2*b269*b271
     + 2*b269*b272 - 2*b272 + 2*b269*b712 + 2*b270*b272 + 2*b270*b690 + 2*b271*
    b273 - 4*b273 + 2*b272*b273 - 2*b272*b438 + 2*b273*b496 + 2*b273*b619 - 2*
    b274*b393 + 2*b274 + 4*b393 - 2*b274*b527 + 2*b274*b546 - 2*b274*b681 + 2*
    b275*b277 + 2*b275*b554 + 2*b275*b620 + 2*b276*b670 - 2*b276*b770 - 2*b277*
    b769 + 2*b277*b770 + 2*b278*b280 - 4*b278 - 2*b280 + 2*b278*b671 + 2*b278*
    b752 + 2*b278*b771 - 2*b279*b507 - 2*b279*b748 - 2*b280*b498 + 2*b280*b569
     + 2*b280*b748 + 2*b281*b518 + 2*b281*b665 - 2*b281*b705 + 2*b282*b451 + 2*
    b451 + 2*b282*b520 - 2*b282*b622 - 2*b283*b405 - 2*b283*b767 - 2*b284*b403
     + 4*b284 - 2*b284*b530 - 2*b284*b531 - 2*b284*b658 + 2*b285*b409 - 2*b409
     + 2*b285*b549 + 2*b285*b658 + 2*b286*b287 - 4*b287 + 2*b287*b289 - 2*b289
     + 2*b287*b365 + 2*b287*b760 + 2*b288*b290 + 2*b288*b560 + 2*b289*b290 + 2*
    b289*b413 - 4*b413 - 2*b289*b480 + 2*b290*b717 - 2*b291*b292 - 2*b291*b492
     - 2*b291*b589 + 2*b292*b368 - 4*b368 + 2*b292*b717 + 2*b293*b367 - 2*b367
     + 2*b293*b474 + 2*b294*b493 + 2*b294*b773 + 2*b295*b296 - 2*b295 + 2*b295*
    b616 + 2*b296*b718 + 2*b296*b719 + 2*b297*b299 - 2*b299 - 2*b297*b699 - 2*
    b297*b700 + 2*b298*b301 - 2*b298*b513 - 2*b298*b563 + 2*b299*b301 - 2*b299*
    b429 + 4*b429 + 2*b299*b576 - 2*b300*b303 - 2*b303 - 2*b300*b711 + 2*b301*
    b303 - 2*b302*b432 - 2*b302*b481 - 2*b302*b653 + 2*b303*b432 + 2*b303*b713
     + 2*b304*b305 - 2*b304 - 2*b305 + 2*b304*b385 - 2*b385 - 2*b304*b628 + 2*
    b304*b704 - 2*b305*b389 + 2*b389 + 2*b305*b535 + 2*b305*b761 + 2*b306*b308
     - 4*b306 - 4*b308 + 2*b306*b594 + 2*b306*b607 + 2*b306*b761 - 2*b307*b346
     + 4*b307 + 2*b346 - 2*b307*b536 - 2*b307*b537 - 2*b307*b669 + 2*b308*b346
     + 2*b308*b496 + 2*b308*b537 + 2*b309*b311 + 2*b309*b566 - 2*b309*b714 + 2*
    b310*b663 - 2*b310*b747 + 2*b311*b747 - 2*b311*b776 + 2*b312*b314 - 4*b312
     - 2*b314 + 2*b312*b447 - 2*b447 + 2*b312*b665 + 2*b312*b757 - 2*b313*b316
     - 2*b316 - 2*b313*b519 + 2*b313*b725 + 2*b314*b316 - 2*b314*b506 + 2*b314*
    b556 - 2*b315*b318 - 2*b318 + 2*b315*b505 + 2*b315*b671 + 2*b316*b318 + 2*
    b316*b740 + 2*b317*b508 - 2*b317 + 2*b317*b548 + 2*b317*b611 - 2*b317*b612
     + 2*b318*b612 + 2*b318*b694 - 2*b319*b358 - 2*b319*b758 - 2*b320*b321 + 4*
    b320 - 2*b321 - 2*b320*b357 - 2*b320*b540 - 2*b320*b542 + 2*b321*b322 + 2*
    b321*b649 + 2*b321*b758 + 2*b322*b462 - 2*b462 + 2*b322*b557 + 2*b323*b325
     - 4*b325 + 2*b324*b325 + 2*b324*b462 + 2*b324*b759 + 2*b325*b327 - 4*b327
     + 2*b325*b414 + 2*b326*b328 + 2*b327*b328 + 2*b327*b466 - 4*b466 + 2*b327*
    b480 + 2*b328*b707 + 2*b329*b420 - 2*b420 - 2*b329*b572 + 2*b329*b707 + 2*
    b330*b419 - 4*b419 + 2*b330*b421 + 2*b331*b501 + 2*b331*b777 + 2*b332*b333
     - 2*b332 + 2*b332*b603 + 2*b333*b709 + 2*b333*b710 + 2*b334*b336 - 2*b336
     - 2*b334*b710 - 2*b334*b711 + 2*b335*b338 - 2*b335*b503 - 2*b335*b576 + 2*
    b336*b338 + 2*b336*b563 - 2*b336*b653 - 2*b337*b340 - 2*b340 - 2*b337*b552
     - 2*b337*b700 + 2*b338*b340 - 2*b339*b384 - 2*b339*b429 - 2*b339*b485 + 2*
    b340*b384 + 2*b340*b702 + 2*b341*b342 - 2*b342 + 2*b341*b433 - 4*b433 + 2*
    b341*b692 - 2*b342*b343 + 2*b343 + 2*b342*b526 + 2*b342*b755 + 2*b343*b344
     - 4*b344 - 2*b343*b390 + 4*b390 - 2*b343*b577 + 2*b344*b579 + 2*b344*b755
     + 2*b344*b768 - 2*b345*b545 + 4*b345 - 2*b345*b546 - 2*b345*b662 - 2*b345*
    b664 - 2*b346*b670 - 2*b346*b776 + 2*b347*b349 - 2*b347 + 2*b347*b578 + 2*
    b347*b596 - 2*b347*b722 + 2*b348*b443 - 4*b443 + 2*b348*b595 - 2*b348*b739
     + 2*b349*b739 + 2*b349*b776 - 2*b350*b581 - 2*b350*b632 - 2*b351*b353 - 2*
    b353 - 2*b351*b516 - 2*b351*b518 + 2*b352*b353 - 4*b352 + 2*b352*b449 + 2*
    b352*b632 + 2*b352*b765 + 2*b353*b355 - 2*b355 + 2*b353*b548 - 2*b354*b356
     - 2*b356 + 2*b354*b497 + 2*b355*b356 - 2*b355*b641 + 2*b355*b734 + 2*b356*
    b599 + 2*b356*b683 + 2*b357*b734 - 2*b357*b754 - 2*b358*b359 - 2*b359 - 2*
    b358*b549 + 2*b359*b361 + 2*b359*b642 + 2*b359*b754 - 2*b360*b570 - 2*b360*
    b571 - 2*b360*b726 + 2*b361*b570 + 2*b361*b726 + 2*b362*b364 - 2*b362*b613
     + 2*b363*b465 - 2*b465 - 2*b363*b706 + 2*b364*b465 + 2*b364*b726 + 2*b365*
    b366 + 2*b366*b695 - 2*b366*b779 + 2*b367*b473 - 2*b473 - 2*b367*b559 + 2*
    b367*b695 + 2*b368*b370 + 2*b368*b472 - 4*b472 + 2*b368*b474 + 2*b369*b372
     + 2*b369*b484 + 2*b370*b372 + 2*b370*b473 + 2*b371*b373 - 2*b373 + 2*b371*
    b511 + 2*b372*b373 + 2*b374*b376 - 2*b374 + 2*b374*b590 - 2*b375*b561 + 4*
    b375 - 2*b375*b697 - 2*b375*b698 - 2*b375*b699 + 2*b376*b697 + 2*b376*b699
     + 2*b377*b380 - 2*b377*b719 - 2*b377*b720 + 2*b378*b380 + 2*b378*b561 + 2*
    b378*b699 + 2*b379*b382 - 4*b382 - 2*b379*b494 - 2*b379*b592 + 2*b380*b382
     - 2*b381*b383 + 4*b381 - 2*b381*b482 - 2*b381*b564 - 2*b381*b689 + 2*b382*
    b383 + 2*b382*b552 + 2*b383*b638 - 2*b384*b778 + 2*b385*b387 - 2*b387 + 2*
    b385*b533 - 2*b385*b721 + 2*b386*b388 - 2*b388 + 2*b386*b680 + 2*b387*b388
     - 2*b387*b514 + 2*b387*b778 - 2*b388*b607 + 2*b388*b751 + 2*b389*b391 - 4*
    b391 - 2*b389*b439 + 4*b439 - 2*b389*b565 - 2*b390*b609 - 2*b390*b761 - 2*
    b390*b762 + 2*b391*b441 + 2*b391*b751 + 2*b391*b762 + 2*b392*b440 + 2*b392
     - 4*b440 - 2*b392*b554 - 2*b392*b655 - 2*b392*b656 - 2*b393*b682 - 2*b393*
    b768 - 2*b393*b769 + 2*b394*b395 - 2*b394 + 2*b394*b582 + 2*b394*b593 - 2*
    b394*b732 + 2*b395*b733 + 2*b395*b769 - 2*b396*b595 - 2*b396*b621 + 2*b397*
    b621 - 2*b397 + 2*b397*b733 - 2*b397*b757 + 2*b397*b764 + 2*b398*b399 - 4*
    b398 + 2*b399 + 2*b398*b400 + 2*b398*b621 + 2*b398*b771 - 2*b399*b401 - 2*
    b399*b598 - 2*b399*b725 + 2*b400*b401 - 2*b400*b539 + 2*b401*b402 - 2*b402
     + 2*b402*b404 - 2*b404 - 2*b402*b633 + 2*b402*b672 + 2*b403*b740 - 2*b403*
    b749 - 2*b404*b521 + 2*b404*b586 + 2*b404*b749 - 2*b405*b406 - 2*b406 - 2*
    b405*b557 + 2*b406*b408 + 2*b406*b634 + 2*b406*b749 - 2*b407*b585 + 4*b407
     - 2*b407*b587 - 2*b407*b715 - 2*b407*b716 + 2*b408*b585 + 2*b408*b716 + 2*
    b409*b411 - 2*b409*b600 + 2*b409*b760 + 2*b410*b413 - 2*b410*b716 + 2*b411*
    b413 + 2*b411*b716 + 2*b412*b415 + 2*b413*b415 + 2*b414*b416 - 4*b416 + 2*
    b415*b416 + 2*b416*b417 - 2*b417 + 2*b416*b500 + 2*b417*b419 - 2*b417*b635
     + 2*b417*b684 - 2*b418*b484 + 2*b418*b510 - 2*b418*b512 + 2*b419*b512 + 2*
    b419*b559 + 2*b420*b421 + 2*b420*b422 - 2*b420*b492 - 2*b421*b476 + 2*b476
     + 2*b422*b476 + 2*b422*b512 + 2*b423*b424 - 2*b423 + 2*b424 + 2*b423*b425
     - 2*b424*b574 - 2*b424*b686 - 2*b424*b688 + 2*b425*b688 + 2*b425*b750 + 2*
    b426*b428 - 4*b428 - 2*b426*b729 - 2*b426*b730 + 2*b427*b428 + 2*b427*b574
     + 2*b427*b688 + 2*b428*b430 - 4*b430 + 2*b428*b653 - 2*b429*b431 - 2*b429*
    b486 + 2*b430*b431 + 2*b430*b564 + 2*b430*b605 + 2*b431*b629 - 2*b432*b775
     + 2*b433*b435 - 4*b435 + 2*b433*b543 + 2*b433*b721 + 2*b434*b436 + 2*b434*
    b437 - 4*b437 + 2*b435*b437 + 2*b435*b514 + 2*b435*b775 - 2*b436*b746 + 2*
    b437*b607 + 2*b437*b746 + 2*b438*b440 - 2*b438*b553 - 2*b439*b594 - 2*b439*
    b755 - 2*b439*b756 + 2*b440*b746 + 2*b440*b756 - 2*b441*b566 - 2*b441*b647
     - 2*b442*b762 - 2*b442*b763 + 2*b443*b444 + 2*b443*b608 + 2*b443*b732 + 2*
    b444*b723 + 2*b444*b763 + 2*b445*b516 + 2*b445*b581 - 2*b445*b610 + 2*b446*
    b610 - 2*b446 + 2*b446*b723 - 2*b446*b752 + 2*b446*b770 + 2*b447*b448 - 4*
    b448 - 2*b447*b568 + 2*b447*b772 + 2*b448*b450 + 2*b448*b610 + 2*b448*b641
     - 2*b449*b452 - 2*b449*b611 + 2*b450*b452 + 2*b450*b539 - 2*b451*b454 - 2*
    b454 - 2*b451*b490 - 2*b451*b665 + 2*b452*b454 - 2*b453*b456 - 2*b456 - 2*
    b453*b530 - 2*b453*b569 + 2*b454*b455 + 2*b454*b456 - 2*b455*b740 - 2*b455*
    b741 + 2*b456*b457 + 2*b457 + 2*b456*b741 - 2*b457*b459 - 2*b459 - 2*b457*
    b570 - 2*b457*b622 - 2*b458*b460 + 2*b458*b461 + 2*b459*b461 + 2*b459*b623
     + 2*b459*b741 - 2*b460*b706 + 2*b461*b706 + 2*b462*b464 - 2*b462*b588 + 2*
    b463*b466 - 2*b463*b726 + 2*b464*b466 + 2*b464*b706 + 2*b465*b467 - 2*b465*
    b779 + 2*b466*b779 + 2*b467*b469 - 4*b469 - 2*b468*b470 - 2*b470 - 2*b468*
    b500 - 2*b468*b643 + 2*b469*b470 + 2*b469*b510 + 2*b469*b779 + 2*b470*b472
     + 2*b470*b674 + 2*b471*b500 - 2*b471*b502 + 2*b472*b502 + 2*b472*b572 + 2*
    b473*b475 - 2*b473*b488 - 2*b474*b774 + 2*b475*b502 + 2*b475*b774 - 2*b476*
    b777 - 2*b476*b780 - 2*b477*b478 + 2*b477*b571 + 2*b478*b586 + 2*b479*b581
     - 2*b480*b522 + 2*b481*b482 + 2*b482*b523 - 2*b484*b493 + 2*b485*b486 + 2*
    b486*b532 + 2*b487*b553 + 2*b488*b522 + 2*b489*b565 - 2*b490*b491 + 2*b490*
    b633 - 2*b491*b583 + 2*b494*b605 + 2*b495*b577 - 2*b496*b580 - 2*b497*b498
     + 2*b497*b499 - 2*b497*b611 - 2*b499*b610 - 2*b500*b708 - 2*b501*b502 - 2*
    b504*b567 - 2*b505*b506 + 2*b505*b507 - 2*b505*b598 + 2*b506*b528 - 2*b507*
    b621 - 2*b508*b509 + 2*b508*b550 + 2*b509*b556 + 2*b509*b598 - 2*b509*b599
     - 2*b510*b650 - 2*b510*b696 - 2*b511*b512 - 2*b516*b517 + 2*b518*b519 - 2*
    b518*b584 - 2*b519*b632 - 2*b520*b521 + 2*b520*b558 + 2*b521*b569 + 2*b521*
    b584 - 2*b522*b685 - 2*b524*b525 + 2*b524*b628 - 2*b524*b712 + 2*b526*b712
     - 2*b526*b778 - 2*b528*b529 - 2*b528*b539 - 2*b529*b752 - 2*b531*b624 - 2*
    b533*b534 - 2*b533*b701 + 2*b535*b701 - 2*b535*b775 - 2*b537*b682 - 2*b538*
    b757 - 2*b540*b541 - 2*b541*b556 - 2*b542*b613 - 2*b543*b544 - 2*b543*b690
     - 2*b546*b670 - 2*b547*b765 + 2*b549*b550 - 2*b549*b600 - 2*b550*b683 + 2*
    b551*b720 + 2*b551*b745 - 2*b552*b629 - 2*b554*b663 - 2*b555*b771 - 2*b556*
    b597 + 2*b557*b558 - 2*b557*b588 - 2*b558*b694 - 2*b559*b560 - 2*b560*b742
     + 2*b561*b562 - 2*b561*b563 + 2*b562*b698 - 2*b562*b709 - 2*b562*b710 + 2*
    b563*b710 - 2*b564*b638 + 2*b566*b567 + 2*b567*b693 + 2*b568*b595 - 2*b569*
    b583 - 2*b571*b614 - 2*b572*b573 - 2*b573*b735 + 2*b574*b575 - 2*b574*b576
     + 2*b575*b686 - 2*b575*b718 - 2*b575*b719 + 2*b576*b719 - 2*b578*b579 + 2*
    b578*b580 + 2*b580*b681 - 2*b580*b714 - 2*b581*b582 - 2*b582*b733 + 2*b583*
    b753 - 2*b584*b641 - 2*b585*b586 - 2*b586*b612 + 2*b587*b588 - 2*b587*b601
     + 2*b588*b715 - 2*b589*b727 - 2*b590*b677 + 2*b591*b677 - 2*b591*b728 - 2*
    b591*b729 + 2*b592*b689 + 2*b592*b729 - 2*b593*b594 - 2*b593*b639 - 2*b595*
    b596 + 2*b596*b639 - 2*b596*b723 + 2*b599*b754 - 2*b602*b717 - 2*b603*b666
     + 2*b604*b666 - 2*b604*b736 - 2*b604*b737 - 2*b605*b606 + 2*b606*b700 + 2*
    b606*b737 - 2*b607*b619 - 2*b608*b609 - 2*b608*b630 + 2*b609*b619 + 2*b612*
    b758 - 2*b615*b707 - 2*b616*b659 + 2*b617*b659 - 2*b617*b743 - 2*b617*b744
     + 2*b618*b711 + 2*b618*b744 - 2*b619*b768 + 2*b622*b705 + 2*b622*b767 - 2*
    b624*b759 - 2*b625*b695 - 2*b626*b652 + 2*b627*b720 - 2*b628*b629 + 2*b629*
    b775 - 2*b630*b631 + 2*b632*b766 - 2*b633*b671 + 2*b635*b643 - 2*b636*b651
     - 2*b637*b645 + 2*b638*b778 - 2*b639*b640 + 2*b640*b682 - 2*b643*b644 + 2*
    b646*b703 - 2*b646*b761 + 2*b647*b756 + 2*b647*b763 + 2*b648*b670 - 2*b649*
    b658 + 2*b654*b691 - 2*b654*b755 + 2*b656*b762 + 2*b656*b769 + 2*b657*b663
     + 2*b658*b767 + 2*b661*b679 - 2*b661*b751 - 2*b663*b664 + 2*b664*b768 + 2*
    b664*b776 - 2*b667*b668 + 2*b668*b731 - 2*b672*b734 - 2*b673*b674 + 2*b673*
    b675 - 2*b673*b676 - 2*b674*b707 - 2*b675*b717 + 2*b678*b679 - 2*b679*b680
     - 2*b684*b695 - 2*b685*b727 - 2*b687*b688 - 2*b687*b689 + 2*b690*b691 - 2*
    b691*b692 - 2*b696*b735 - 2*b701*b702 + 2*b701*b703 - 2*b702*b745 - 2*b703*
    b704 + 2*b705*b748 - 2*b708*b742 - 2*b712*b713 - 2*b713*b738 - 2*b721*b731
     - 2*b724*b725 - 2*b734*b753 + 2*b739*b766 - 2*b740*b748 + 2*b747*b772 - 2*
    b759*b760 - 2*b764*b766 - 2*b765*b766 - 2*b770*b772 - 2*b771*b772 - 2*b773*
    b774 + 2*b774*b780 + x781 <= 0;