#  MIQCP written by GAMS Convert at 02/15/18 15:47:54
#  
#  Equation counts
#      Total        E        G        L        N        X        C        B
#          1        1        0        0        0        0        0        0
#  
#  Variable counts
#                   x        b        i      s1s      s2s       sc       si
#      Total     cont   binary  integer     sos1     sos2    scont     sint
#       1129        1     1128        0        0        0        0        0
#  FX      0        0        0        0        0        0        0        0
#  
#  Nonzero counts
#      Total    const       NL      DLL
#       1129        1     1128        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;
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 b781 binary >= 0, <= 1;
var b782 binary >= 0, <= 1;
var b783 binary >= 0, <= 1;
var b784 binary >= 0, <= 1;
var b785 binary >= 0, <= 1;
var b786 binary >= 0, <= 1;
var b787 binary >= 0, <= 1;
var b788 binary >= 0, <= 1;
var b789 binary >= 0, <= 1;
var b790 binary >= 0, <= 1;
var b791 binary >= 0, <= 1;
var b792 binary >= 0, <= 1;
var b793 binary >= 0, <= 1;
var b794 binary >= 0, <= 1;
var b795 binary >= 0, <= 1;
var b796 binary >= 0, <= 1;
var b797 binary >= 0, <= 1;
var b798 binary >= 0, <= 1;
var b799 binary >= 0, <= 1;
var b800 binary >= 0, <= 1;
var b801 binary >= 0, <= 1;
var b802 binary >= 0, <= 1;
var b803 binary >= 0, <= 1;
var b804 binary >= 0, <= 1;
var b805 binary >= 0, <= 1;
var b806 binary >= 0, <= 1;
var b807 binary >= 0, <= 1;
var b808 binary >= 0, <= 1;
var b809 binary >= 0, <= 1;
var b810 binary >= 0, <= 1;
var b811 binary >= 0, <= 1;
var b812 binary >= 0, <= 1;
var b813 binary >= 0, <= 1;
var b814 binary >= 0, <= 1;
var b815 binary >= 0, <= 1;
var b816 binary >= 0, <= 1;
var b817 binary >= 0, <= 1;
var b818 binary >= 0, <= 1;
var b819 binary >= 0, <= 1;
var b820 binary >= 0, <= 1;
var b821 binary >= 0, <= 1;
var b822 binary >= 0, <= 1;
var b823 binary >= 0, <= 1;
var b824 binary >= 0, <= 1;
var b825 binary >= 0, <= 1;
var b826 binary >= 0, <= 1;
var b827 binary >= 0, <= 1;
var b828 binary >= 0, <= 1;
var b829 binary >= 0, <= 1;
var b830 binary >= 0, <= 1;
var b831 binary >= 0, <= 1;
var b832 binary >= 0, <= 1;
var b833 binary >= 0, <= 1;
var b834 binary >= 0, <= 1;
var b835 binary >= 0, <= 1;
var b836 binary >= 0, <= 1;
var b837 binary >= 0, <= 1;
var b838 binary >= 0, <= 1;
var b839 binary >= 0, <= 1;
var b840 binary >= 0, <= 1;
var b841 binary >= 0, <= 1;
var b842 binary >= 0, <= 1;
var b843 binary >= 0, <= 1;
var b844 binary >= 0, <= 1;
var b845 binary >= 0, <= 1;
var b846 binary >= 0, <= 1;
var b847 binary >= 0, <= 1;
var b848 binary >= 0, <= 1;
var b849 binary >= 0, <= 1;
var b850 binary >= 0, <= 1;
var b851 binary >= 0, <= 1;
var b852 binary >= 0, <= 1;
var b853 binary >= 0, <= 1;
var b854 binary >= 0, <= 1;
var b855 binary >= 0, <= 1;
var b856 binary >= 0, <= 1;
var b857 binary >= 0, <= 1;
var b858 binary >= 0, <= 1;
var b859 binary >= 0, <= 1;
var b860 binary >= 0, <= 1;
var b861 binary >= 0, <= 1;
var b862 binary >= 0, <= 1;
var b863 binary >= 0, <= 1;
var b864 binary >= 0, <= 1;
var b865 binary >= 0, <= 1;
var b866 binary >= 0, <= 1;
var b867 binary >= 0, <= 1;
var b868 binary >= 0, <= 1;
var b869 binary >= 0, <= 1;
var b870 binary >= 0, <= 1;
var b871 binary >= 0, <= 1;
var b872 binary >= 0, <= 1;
var b873 binary >= 0, <= 1;
var b874 binary >= 0, <= 1;
var b875 binary >= 0, <= 1;
var b876 binary >= 0, <= 1;
var b877 binary >= 0, <= 1;
var b878 binary >= 0, <= 1;
var b879 binary >= 0, <= 1;
var b880 binary >= 0, <= 1;
var b881 binary >= 0, <= 1;
var b882 binary >= 0, <= 1;
var b883 binary >= 0, <= 1;
var b884 binary >= 0, <= 1;
var b885 binary >= 0, <= 1;
var b886 binary >= 0, <= 1;
var b887 binary >= 0, <= 1;
var b888 binary >= 0, <= 1;
var b889 binary >= 0, <= 1;
var b890 binary >= 0, <= 1;
var b891 binary >= 0, <= 1;
var b892 binary >= 0, <= 1;
var b893 binary >= 0, <= 1;
var b894 binary >= 0, <= 1;
var b895 binary >= 0, <= 1;
var b896 binary >= 0, <= 1;
var b897 binary >= 0, <= 1;
var b898 binary >= 0, <= 1;
var b899 binary >= 0, <= 1;
var b900 binary >= 0, <= 1;
var b901 binary >= 0, <= 1;
var b902 binary >= 0, <= 1;
var b903 binary >= 0, <= 1;
var b904 binary >= 0, <= 1;
var b905 binary >= 0, <= 1;
var b906 binary >= 0, <= 1;
var b907 binary >= 0, <= 1;
var b908 binary >= 0, <= 1;
var b909 binary >= 0, <= 1;
var b910 binary >= 0, <= 1;
var b911 binary >= 0, <= 1;
var b912 binary >= 0, <= 1;
var b913 binary >= 0, <= 1;
var b914 binary >= 0, <= 1;
var b915 binary >= 0, <= 1;
var b916 binary >= 0, <= 1;
var b917 binary >= 0, <= 1;
var b918 binary >= 0, <= 1;
var b919 binary >= 0, <= 1;
var b920 binary >= 0, <= 1;
var b921 binary >= 0, <= 1;
var b922 binary >= 0, <= 1;
var b923 binary >= 0, <= 1;
var b924 binary >= 0, <= 1;
var b925 binary >= 0, <= 1;
var b926 binary >= 0, <= 1;
var b927 binary >= 0, <= 1;
var b928 binary >= 0, <= 1;
var b929 binary >= 0, <= 1;
var b930 binary >= 0, <= 1;
var b931 binary >= 0, <= 1;
var b932 binary >= 0, <= 1;
var b933 binary >= 0, <= 1;
var b934 binary >= 0, <= 1;
var b935 binary >= 0, <= 1;
var b936 binary >= 0, <= 1;
var b937 binary >= 0, <= 1;
var b938 binary >= 0, <= 1;
var b939 binary >= 0, <= 1;
var b940 binary >= 0, <= 1;
var b941 binary >= 0, <= 1;
var b942 binary >= 0, <= 1;
var b943 binary >= 0, <= 1;
var b944 binary >= 0, <= 1;
var b945 binary >= 0, <= 1;
var b946 binary >= 0, <= 1;
var b947 binary >= 0, <= 1;
var b948 binary >= 0, <= 1;
var b949 binary >= 0, <= 1;
var b950 binary >= 0, <= 1;
var b951 binary >= 0, <= 1;
var b952 binary >= 0, <= 1;
var b953 binary >= 0, <= 1;
var b954 binary >= 0, <= 1;
var b955 binary >= 0, <= 1;
var b956 binary >= 0, <= 1;
var b957 binary >= 0, <= 1;
var b958 binary >= 0, <= 1;
var b959 binary >= 0, <= 1;
var b960 binary >= 0, <= 1;
var b961 binary >= 0, <= 1;
var b962 binary >= 0, <= 1;
var b963 binary >= 0, <= 1;
var b964 binary >= 0, <= 1;
var b965 binary >= 0, <= 1;
var b966 binary >= 0, <= 1;
var b967 binary >= 0, <= 1;
var b968 binary >= 0, <= 1;
var b969 binary >= 0, <= 1;
var b970 binary >= 0, <= 1;
var b971 binary >= 0, <= 1;
var b972 binary >= 0, <= 1;
var b973 binary >= 0, <= 1;
var b974 binary >= 0, <= 1;
var b975 binary >= 0, <= 1;
var b976 binary >= 0, <= 1;
var b977 binary >= 0, <= 1;
var b978 binary >= 0, <= 1;
var b979 binary >= 0, <= 1;
var b980 binary >= 0, <= 1;
var b981 binary >= 0, <= 1;
var b982 binary >= 0, <= 1;
var b983 binary >= 0, <= 1;
var b984 binary >= 0, <= 1;
var b985 binary >= 0, <= 1;
var b986 binary >= 0, <= 1;
var b987 binary >= 0, <= 1;
var b988 binary >= 0, <= 1;
var b989 binary >= 0, <= 1;
var b990 binary >= 0, <= 1;
var b991 binary >= 0, <= 1;
var b992 binary >= 0, <= 1;
var b993 binary >= 0, <= 1;
var b994 binary >= 0, <= 1;
var b995 binary >= 0, <= 1;
var b996 binary >= 0, <= 1;
var b997 binary >= 0, <= 1;
var b998 binary >= 0, <= 1;
var b999 binary >= 0, <= 1;
var b1000 binary >= 0, <= 1;
var b1001 binary >= 0, <= 1;
var b1002 binary >= 0, <= 1;
var b1003 binary >= 0, <= 1;
var b1004 binary >= 0, <= 1;
var b1005 binary >= 0, <= 1;
var b1006 binary >= 0, <= 1;
var b1007 binary >= 0, <= 1;
var b1008 binary >= 0, <= 1;
var b1009 binary >= 0, <= 1;
var b1010 binary >= 0, <= 1;
var b1011 binary >= 0, <= 1;
var b1012 binary >= 0, <= 1;
var b1013 binary >= 0, <= 1;
var b1014 binary >= 0, <= 1;
var b1015 binary >= 0, <= 1;
var b1016 binary >= 0, <= 1;
var b1017 binary >= 0, <= 1;
var b1018 binary >= 0, <= 1;
var b1019 binary >= 0, <= 1;
var b1020 binary >= 0, <= 1;
var b1021 binary >= 0, <= 1;
var b1022 binary >= 0, <= 1;
var b1023 binary >= 0, <= 1;
var b1024 binary >= 0, <= 1;
var b1025 binary >= 0, <= 1;
var b1026 binary >= 0, <= 1;
var b1027 binary >= 0, <= 1;
var b1028 binary >= 0, <= 1;
var b1029 binary >= 0, <= 1;
var b1030 binary >= 0, <= 1;
var b1031 binary >= 0, <= 1;
var b1032 binary >= 0, <= 1;
var b1033 binary >= 0, <= 1;
var b1034 binary >= 0, <= 1;
var b1035 binary >= 0, <= 1;
var b1036 binary >= 0, <= 1;
var b1037 binary >= 0, <= 1;
var b1038 binary >= 0, <= 1;
var b1039 binary >= 0, <= 1;
var b1040 binary >= 0, <= 1;
var b1041 binary >= 0, <= 1;
var b1042 binary >= 0, <= 1;
var b1043 binary >= 0, <= 1;
var b1044 binary >= 0, <= 1;
var b1045 binary >= 0, <= 1;
var b1046 binary >= 0, <= 1;
var b1047 binary >= 0, <= 1;
var b1048 binary >= 0, <= 1;
var b1049 binary >= 0, <= 1;
var b1050 binary >= 0, <= 1;
var b1051 binary >= 0, <= 1;
var b1052 binary >= 0, <= 1;
var b1053 binary >= 0, <= 1;
var b1054 binary >= 0, <= 1;
var b1055 binary >= 0, <= 1;
var b1056 binary >= 0, <= 1;
var b1057 binary >= 0, <= 1;
var b1058 binary >= 0, <= 1;
var b1059 binary >= 0, <= 1;
var b1060 binary >= 0, <= 1;
var b1061 binary >= 0, <= 1;
var b1062 binary >= 0, <= 1;
var b1063 binary >= 0, <= 1;
var b1064 binary >= 0, <= 1;
var b1065 binary >= 0, <= 1;
var b1066 binary >= 0, <= 1;
var b1067 binary >= 0, <= 1;
var b1068 binary >= 0, <= 1;
var b1069 binary >= 0, <= 1;
var b1070 binary >= 0, <= 1;
var b1071 binary >= 0, <= 1;
var b1072 binary >= 0, <= 1;
var b1073 binary >= 0, <= 1;
var b1074 binary >= 0, <= 1;
var b1075 binary >= 0, <= 1;
var b1076 binary >= 0, <= 1;
var b1077 binary >= 0, <= 1;
var b1078 binary >= 0, <= 1;
var b1079 binary >= 0, <= 1;
var b1080 binary >= 0, <= 1;
var b1081 binary >= 0, <= 1;
var b1082 binary >= 0, <= 1;
var b1083 binary >= 0, <= 1;
var b1084 binary >= 0, <= 1;
var b1085 binary >= 0, <= 1;
var b1086 binary >= 0, <= 1;
var b1087 binary >= 0, <= 1;
var b1088 binary >= 0, <= 1;
var b1089 binary >= 0, <= 1;
var b1090 binary >= 0, <= 1;
var b1091 binary >= 0, <= 1;
var b1092 binary >= 0, <= 1;
var b1093 binary >= 0, <= 1;
var b1094 binary >= 0, <= 1;
var b1095 binary >= 0, <= 1;
var b1096 binary >= 0, <= 1;
var b1097 binary >= 0, <= 1;
var b1098 binary >= 0, <= 1;
var b1099 binary >= 0, <= 1;
var b1100 binary >= 0, <= 1;
var b1101 binary >= 0, <= 1;
var b1102 binary >= 0, <= 1;
var b1103 binary >= 0, <= 1;
var b1104 binary >= 0, <= 1;
var b1105 binary >= 0, <= 1;
var b1106 binary >= 0, <= 1;
var b1107 binary >= 0, <= 1;
var b1108 binary >= 0, <= 1;
var b1109 binary >= 0, <= 1;
var b1110 binary >= 0, <= 1;
var b1111 binary >= 0, <= 1;
var b1112 binary >= 0, <= 1;
var b1113 binary >= 0, <= 1;
var b1114 binary >= 0, <= 1;
var b1115 binary >= 0, <= 1;
var b1116 binary >= 0, <= 1;
var b1117 binary >= 0, <= 1;
var b1118 binary >= 0, <= 1;
var b1119 binary >= 0, <= 1;
var b1120 binary >= 0, <= 1;
var b1121 binary >= 0, <= 1;
var b1122 binary >= 0, <= 1;
var b1123 binary >= 0, <= 1;
var b1124 binary >= 0, <= 1;
var b1125 binary >= 0, <= 1;
var b1126 binary >= 0, <= 1;
var b1127 binary >= 0, <= 1;
var b1128 binary >= 0, <= 1;
var b1129 binary >= 0, <= 1;

maximize obj: 2*b2*b3 - 2*b2*b120 - 2*b2*b504 + 2*b504 + 2*b2*b700 + 2*b700 - 2
    *b3*b132 - 2*b3*b520 + 4*b520 + 2*b3*b871 - 2*b871 - 2*b4*b136 - 2*b4*b525
     + 4*b525 + 2*b4*b526 + 2*b526 + 2*b4*b547 - 2*b547 + 2*b5*b63 - 2*b5*b488
     + 2*b488 + 2*b5*b891 + 2*b891 - 2*b5*b936 + 4*b936 + 2*b6*b7 + 2*b6*b12 - 
    2*b6*b15 - 2*b6*b476 + 2*b476 + 2*b7*b272 - 2*b7*b461 + 2*b461 - 2*b7*b499
     + 2*b499 + 2*b8*b506 + 2*b506 - 2*b8*b524 + 2*b524 - 2*b8*b548 + 4*b548 + 
    2*b8*b574 - 2*b574 - 2*b9*b10 + 2*b9*b18 + 2*b9*b938 - 2*b938 - 2*b9*b941
     + 2*b941 + 2*b10*b26 + 2*b10*b604 - 2*b604 - 2*b10*b674 + 4*b674 + 2*b11*
    b260 + 2*b11*b383 + 2*b383 - 2*b11*b449 + 2*b449 - 2*b11*b477 + 2*b477 - 2*
    b12*b55 - 2*b12*b383 + 2*b12*b734 - 2*b734 - 2*b13*b63 - 2*b13*b384 + 2*
    b384 + 2*b13*b761 - 2*b761 + 2*b13*b995 + 2*b995 - 2*b14*b496 + 2*b496 - 2*
    b14*b586 + 4*b586 + 2*b14*b857 - 2*b857 + 2*b14*b951 - 2*b951 - 2*b15*b66
     + 2*b15*b689 - 2*b689 + 2*b15*b1080 + 2*b1080 - 2*b16*b143 + 2*b16*b500 - 
    2*b500 + 2*b16*b621 + 2*b621 - 2*b16*b656 + 4*b656 - 2*b17*b385 + 2*b385 - 
    2*b17*b488 + 2*b17*b803 - 2*b803 + 2*b17*b940 + 2*b940 - 2*b18*b385 + 2*b18
    *b806 + 2*b806 - 2*b18*b895 + 4*b895 - 2*b19*b20 - 2*b19*b78 + 2*b19*b903
     - 2*b903 + 2*b19*b1006 - 2*b1006 + 2*b20*b93 + 2*b20*b94 - 2*b20*b768 + 2*
    b768 - 2*b21*b79 - 2*b21*b383 + 2*b21*b650 - 2*b650 + 2*b21*b1015 + 2*b1015
     - 2*b22*b154 + 2*b22*b478 - 2*b478 + 2*b22*b592 + 2*b592 - 2*b22*b695 + 4*
    b695 + 2*b23*b24 + 2*b23*b187 - 2*b23*b199 - 2*b23*b748 + 2*b748 + 2*b24*
    b146 - 2*b24*b396 + 2*b396 - 2*b24*b403 + 2*b403 + 2*b25*b26 - 2*b25*b384
     + 2*b25*b765 + 2*b765 - 2*b25*b943 + 4*b943 - 2*b26*b1125 + 4*b1125 - 2*
    b26*b1128 + 4*b1128 - 2*b27*b95 - 2*b27*b855 + 2*b855 + 2*b27*b954 - 2*b954
     + 2*b27*b1069 - 2*b1069 + 2*b28*b464 - 2*b464 + 2*b28*b564 + 2*b564 - 2*
    b28*b565 + 2*b565 - 2*b28*b740 + 4*b740 + 2*b29*b479 - 2*b479 + 2*b29*b597
     + 2*b597 - 2*b29*b825 + 4*b825 - 2*b29*b970 + 4*b970 + 2*b30*b31 + 2*b30*
    b174 - 2*b30*b210 - 2*b30*b703 + 2*b703 + 2*b31*b134 - 2*b31*b394 + 2*b394
     - 2*b31*b400 + 2*b400 + 2*b32*b230 + 2*b32*b268 - 2*b32*b992 + 2*b992 - 2*
    b32*b1058 - 2*b1058 + 2*b33*b34 - 2*b33*b385 + 2*b33*b720 + 2*b720 - 2*b33*
    b998 + 4*b998 + 2*b34*b1058 - 2*b34*b1059 + 4*b1059 - 2*b34*b1062 + 4*b1062
     + 2*b35*b36 - 2*b35*b108 - 2*b35*b810 + 2*b810 + 2*b35*b1009 - 4*b1009 - 2
    *b36*b46 - 2*b36*b421 + 2*b421 + 2*b36*b1004 - 2*b1004 + 2*b37*b54 - 2*b37*
    b586 - 2*b37*b728 + 2*b728 + 2*b37*b1009 + 2*b38*b39 + 2*b38*b451 - 2*b451
     - 2*b38*b594 + 2*b594 - 2*b38*b784 + 4*b784 + 2*b39*b314 - 2*b39*b539 + 2*
    b539 - 2*b39*b1025 + 2*b1025 + 2*b40*b130 - 2*b40*b480 + 2*b480 + 2*b40*
    b501 - 2*b501 - 2*b40*b625 + 4*b625 + 2*b41*b42 - 2*b41*b43 + 2*b41*b159 - 
    2*b41*b219 - 2*b42*b392 + 2*b392 - 2*b42*b398 + 2*b398 + 2*b42*b878 + 2*
    b878 + 2*b43*b186 - 2*b43*b403 + 2*b43*b750 - 2*b750 + 2*b44*b45 - 2*b44*
    b92 + 2*b44*b666 - 2*b666 - 2*b44*b881 + 2*b881 - 2*b45*b104 - 2*b45*b159
     + 2*b45*b160 + 2*b46*b166 - 2*b46*b851 + 2*b851 + 2*b46*b952 + 2*b952 + 2*
    b47*b119 - 2*b47*b502 + 2*b502 + 2*b47*b518 - 2*b518 - 2*b47*b659 + 4*b659
     + 2*b48*b49 - 2*b48*b50 + 2*b48*b147 - 2*b48*b923 + 2*b923 - 2*b49*b71 - 2
    *b49*b396 + 2*b49*b922 + 2*b922 + 2*b50*b198 - 2*b50*b408 + 2*b408 + 2*b50*
    b793 - 2*b793 + 2*b51*b52 - 2*b51*b106 + 2*b51*b709 - 2*b709 - 2*b51*b837
     + 2*b837 - 2*b52*b114 - 2*b52*b147 + 2*b52*b983 + 2*b983 + 2*b53*b116 + 2*
    b53*b387 + 2*b387 - 2*b53*b395 + 4*b395 - 2*b53*b1072 + 2*b1072 - 2*b54*
    b232 - 2*b54*b387 + 2*b54*b815 - 2*b815 + 2*b55*b153 - 2*b55*b779 + 4*b779
     + 2*b55*b909 + 2*b909 + 2*b56*b112 - 2*b56*b519 + 2*b519 + 2*b56*b540 - 2*
    b540 - 2*b56*b698 + 4*b698 - 2*b57*b570 + 4*b570 + 2*b57*b627 - 2*b627 + 2*
    b57*b976 - 2*b976 - 2*b57*b1103 + 2*b1103 - 2*b58*b59 + 2*b58*b135 - 2*b58*
    b879 + 2*b879 + 2*b58*b976 + 2*b59*b209 - 2*b59*b413 + 2*b413 + 2*b59*b835
     - 2*b835 + 2*b60*b61 - 2*b60*b572 + 2*b572 + 2*b60*b753 - 4*b753 - 2*b60*
    b794 + 2*b794 - 2*b61*b121 - 2*b61*b135 + 2*b61*b1045 + 2*b1045 - 2*b62*
    b709 + 2*b62*b753 + 2*b62*b797 + 2*b797 - 2*b62*b842 + 4*b842 - 2*b63*b223
     + 2*b63*b509 - 2*b509 + 2*b64*b416 + 2*b416 - 2*b64*b770 + 2*b770 - 2*b64*
    b1002 + 2*b1002 + 2*b64*b1006 + 2*b65*b107 + 2*b65*b388 + 2*b388 - 2*b65*
    b393 + 4*b393 - 2*b65*b1008 + 2*b1008 + 2*b66*b142 - 2*b66*b820 + 4*b820 + 
    2*b66*b864 + 2*b864 + 2*b67*b68 + 2*b67*b285 - 2*b67*b390 + 2*b390 - 2*b67*
    b563 + 2*b563 + 2*b68*b141 - 2*b68*b142 - 2*b68*b619 + 2*b619 - 2*b69*b540
     + 2*b69*b566 - 4*b566 + 2*b69*b964 + 2*b964 - 2*b69*b1026 + 4*b1026 + 2*
    b70*b101 - 2*b70*b541 + 4*b541 + 2*b70*b566 - 2*b70*b744 + 4*b744 + 2*b71*
    b72 - 2*b71*b73 + 2*b71*b88 - 2*b72*b171 - 2*b72*b700 + 2*b72*b791 + 2*b791
     + 2*b73*b287 - 2*b73*b482 + 2*b482 + 2*b73*b702 + 2*b702 - 2*b74*b545 + 2*
    b545 - 2*b74*b751 + 2*b751 + 2*b74*b796 - 4*b796 + 2*b74*b1109 - 2*b1109 - 
    2*b75*b666 + 2*b75*b755 + 2*b755 + 2*b75*b796 - 2*b75*b886 + 4*b886 + 2*b76
    *b420 + 2*b420 - 2*b76*b810 + 2*b76*b951 - 2*b76*b1065 + 2*b1065 + 2*b77*
    b94 + 2*b77*b389 + 2*b389 - 2*b77*b391 + 4*b391 - 2*b77*b953 + 2*b953 - 2*
    b78*b389 + 2*b78*b585 + 2*b585 + 2*b78*b905 + 2*b905 + 2*b79*b128 + 2*b79*
    b818 + 2*b818 - 2*b79*b866 + 4*b866 + 2*b80*b81 + 2*b80*b273 - 2*b80*b397
     + 2*b397 - 2*b80*b1024 + 2*b1024 - 2*b81*b128 - 2*b81*b590 + 2*b590 + 2*
    b81*b1085 - 2*b1085 + 2*b82*b83 - 2*b82*b518 + 2*b82*b595 - 4*b595 - 2*b82*
    b1091 + 4*b1091 - 2*b83*b273 + 2*b83*b378 - 2*b83*b913 + 2*b913 - 2*b84*
    b567 + 4*b567 + 2*b84*b595 + 2*b84*b743 - 2*b743 - 2*b84*b787 + 4*b787 + 2*
    b85*b207 - 2*b85*b504 + 2*b85*b743 - 2*b85*b970 - 2*b86*b156 + 2*b86*b392
     - 2*b86*b661 + 4*b661 + 2*b86*b833 + 2*b833 + 2*b87*b297 - 2*b87*b392 - 2*
    b87*b505 + 2*b505 + 2*b87*b663 + 2*b663 - 2*b88*b392 + 2*b88*b1041 + 2*
    b1041 - 2*b88*b1107 + 4*b1107 + 2*b89*b90 - 2*b89*b523 + 4*b523 - 2*b89*
    b707 + 2*b707 + 2*b89*b840 - 4*b840 + 2*b90*b114 - 2*b90*b401 + 2*b401 - 2*
    b90*b571 + 2*b571 - 2*b91*b92 + 2*b91*b190 + 2*b91*b840 - 2*b91*b930 + 4*
    b930 + 2*b92*b266 + 2*b92*b631 - 2*b631 + 2*b93*b424 + 2*b424 - 2*b93*b427
     + 4*b427 - 2*b93*b855 - 2*b94*b902 + 2*b902 - 2*b94*b904 + 4*b904 + 2*b95*
    b204 - 2*b95*b391 + 2*b95*b859 + 2*b859 + 2*b96*b97 + 2*b96*b262 - 2*b96*
    b399 + 2*b399 - 2*b96*b1089 + 2*b1089 - 2*b97*b562 + 2*b562 - 2*b97*b910 + 
    2*b910 + 2*b97*b1020 - 2*b1020 - 2*b98*b262 + 2*b98*b371 + 2*b98*b451 - 2*
    b98*b869 + 2*b869 - 2*b99*b596 + 4*b596 + 2*b99*b623 - 4*b623 + 2*b99*b786
     - 4*b786 - 2*b99*b828 + 4*b828 - 2*b100*b101 + 2*b100*b196 - 2*b100*b660
     + 2*b660 + 2*b100*b786 - 2*b101*b264 + 2*b101*b829 - 2*b829 - 2*b102*b144
     + 2*b102*b356 + 2*b102*b394 - 2*b102*b626 + 4*b626 + 2*b103*b308 + 2*b103*
    b315 - 2*b103*b394 - 2*b103*b521 + 2*b521 + 2*b104*b158 + 2*b104*b483 + 2*
    b483 - 2*b104*b979 + 2*b979 - 2*b105*b106 + 2*b105*b176 + 2*b105*b884 - 4*
    b884 - 2*b105*b987 + 4*b987 + 2*b106*b278 + 2*b106*b600 - 2*b600 + 2*b107*
    b855 - 2*b107*b856 + 2*b856 - 2*b107*b858 + 2*b858 + 2*b108*b214 - 2*b108*
    b393 + 2*b108*b813 + 2*b813 + 2*b109*b350 + 2*b109*b390 - 2*b109*b463 + 4*
    b463 - 2*b109*b1019 + 4*b1019 - 2*b110*b252 + 2*b110*b367 + 2*b110*b464 - 2
    *b110*b824 + 2*b824 - 2*b111*b112 + 2*b111*b184 - 2*b111*b226 + 2*b111*b827
     - 2*b827 - 2*b112*b253 + 2*b112*b871 - 2*b113*b131 + 2*b113*b362 + 2*b113*
    b396 - 2*b113*b598 + 4*b598 + 2*b114*b146 - 2*b114*b922 + 2*b115*b161 - 2*
    b115*b572 + 2*b115*b927 - 4*b927 - 2*b115*b1049 + 4*b1049 + 2*b116*b810 - 2
    *b116*b811 + 2*b811 - 2*b116*b812 + 2*b812 + 2*b117*b224 - 2*b117*b395 - 2*
    b117*b421 + 2*b117*b773 + 2*b773 - 2*b118*b119 + 2*b118*b170 - 2*b118*b745
     + 2*b745 + 2*b118*b870 - 2*b870 - 2*b119*b244 + 2*b119*b336 + 2*b120*b832
     - 2*b832 + 2*b120*b874 - 2*b874 - 2*b120*b1103 + 2*b121*b134 - 2*b121*b878
     + 2*b121*b1109 + 2*b122*b149 - 2*b122*b545 + 2*b122*b984 - 2*b984 - 2*b122
    *b1116 + 4*b1116 + 2*b123*b124 - 2*b123*b759 + 2*b759 + 2*b123*b939 + 2*
    b939 - 2*b123*b994 + 4*b994 + 2*b124*b324 - 2*b124*b577 + 4*b577 - 2*b124*
    b758 + 4*b758 + 2*b125*b770 - 2*b125*b771 + 2*b771 - 2*b125*b772 + 2*b772
     + 2*b125*b1073 - 4*b1073 + 2*b126*b127 + 2*b126*b140 - 2*b126*b393 - 2*
    b126*b476 + 2*b127*b1073 - 2*b127*b1074 + 4*b1074 - 2*b127*b1077 + 2*b1077
     - 2*b128*b251 + 2*b128*b868 + 2*b868 - 2*b129*b130 + 2*b129*b155 - 2*b129*
    b789 + 2*b789 + 2*b129*b914 - 2*b914 - 2*b130*b238 + 2*b130*b328 + 2*b131*
    b132 - 2*b131*b133 + 2*b131*b876 - 2*b876 - 2*b132*b155 + 2*b132*b308 - 2*
    b133*b184 + 2*b133*b974 - 2*b974 + 2*b133*b1034 + 2*b1034 - 2*b134*b834 + 4
    *b834 - 2*b134*b836 + 2*b836 + 2*b135*b793 - 2*b135*b794 + 2*b136*b177 - 2*
    b136*b799 + 4*b799 + 2*b136*b929 - 2*b929 + 2*b137*b138 - 2*b137*b714 + 2*
    b714 + 2*b137*b893 + 2*b893 - 2*b137*b1059 + 2*b138*b318 - 2*b138*b551 + 4*
    b551 - 2*b138*b713 + 4*b713 + 2*b139*b497 + 2*b497 + 2*b139*b1009 - 2*b139*
    b1010 + 4*b1010 - 2*b139*b1012 + 2*b1012 + 2*b140*b320 - 2*b140*b497 - 2*
    b140*b648 + 2*b648 + 2*b141*b242 - 2*b141*b821 + 2*b821 - 2*b141*b865 + 4*
    b865 - 2*b142*b242 + 2*b142*b822 + 2*b822 + 2*b143*b182 - 2*b143*b519 + 2*
    b143*b696 + 2*b696 - 2*b144*b145 + 2*b144*b919 - 2*b919 + 2*b144*b972 - 2*
    b972 - 2*b145*b196 + 2*b145*b329 + 2*b145*b1037 - 2*b1037 - 2*b146*b338 - 2
    *b146*b792 + 2*b792 - 2*b147*b751 + 2*b147*b835 - 2*b148*b149 + 2*b148*b162
     - 2*b148*b527 + 2*b527 + 2*b148*b986 - 2*b986 - 2*b149*b600 + 2*b149*b1050
     + 2*b1050 + 2*b150*b151 - 2*b150*b672 + 4*b672 + 2*b150*b847 + 2*b847 - 2*
    b150*b1125 + 2*b151*b310 - 2*b151*b529 + 4*b529 - 2*b151*b670 + 4*b670 + 2*
    b152*b397 + 2*b152*b538 + 2*b538 - 2*b152*b819 + 4*b819 - 2*b152*b867 + 2*
    b867 - 2*b153*b397 - 2*b153*b538 + 2*b153*b780 + 2*b780 + 2*b154*b169 - 2*
    b154*b541 + 2*b154*b657 + 2*b657 - 2*b155*b441 + 2*b441 + 2*b155*b1035 - 2*
    b1035 - 2*b156*b157 + 2*b156*b975 - 2*b975 + 2*b156*b1035 - 2*b157*b207 + 2
    *b157*b337 + 2*b157*b1102 - 2*b1102 - 2*b158*b347 + 2*b158*b748 - 2*b158*
    b749 + 2*b749 + 2*b159*b218 - 2*b159*b707 - 2*b160*b353 + 2*b160*b522 + 2*
    b522 - 2*b160*b925 + 2*b925 - 2*b161*b409 + 2*b409 - 2*b161*b631 + 2*b161*
    b988 + 2*b988 - 2*b162*b409 + 2*b162*b468 + 2*b468 - 2*b162*b486 + 4*b486
     + 2*b163*b300 - 2*b163*b508 + 4*b508 - 2*b163*b634 + 4*b634 + 2*b163*b803
     + 2*b164*b165 + 2*b164*b166 - 2*b164*b852 + 4*b852 - 2*b164*b1063 + 2*
    b1063 - 2*b165*b448 + 4*b448 - 2*b166*b405 + 2*b405 - 2*b166*b900 + 2*b900
     + 2*b167*b399 + 2*b167*b561 + 2*b561 - 2*b167*b778 + 4*b778 - 2*b167*b911
     + 2*b911 + 2*b168*b322 - 2*b168*b399 - 2*b168*b561 + 2*b168*b734 - 2*b169*
    b565 + 2*b169*b826 + 2*b826 - 2*b169*b1095 + 2*b1095 - 2*b170*b452 + 2*b452
     - 2*b170*b874 + 2*b170*b1100 - 2*b1100 - 2*b171*b172 + 2*b171*b1038 - 2*
    b1038 + 2*b171*b1100 + 2*b172*b345 + 2*b172*b346 - 2*b172*b660 + 2*b173*
    b401 + 2*b173*b703 - 2*b173*b704 + 2*b704 - 2*b173*b706 + 4*b706 - 2*b174*
    b665 + 2*b665 - 2*b174*b881 + 2*b174*b921 - 2*b921 - 2*b175*b358 + 2*b175*
    b881 - 2*b175*b882 + 2*b882 + 2*b175*b1113 - 2*b1113 - 2*b176*b414 + 2*b414
     - 2*b176*b667 - 2*b667 + 2*b176*b931 + 2*b931 - 2*b177*b414 + 2*b177*b454
     + 2*b454 - 2*b177*b507 + 4*b507 + 2*b178*b289 - 2*b178*b487 + 4*b487 - 2*
    b178*b603 + 4*b603 + 2*b178*b761 + 2*b179*b405 - 2*b179*b438 + 4*b438 + 2*
    b180*b402 + 2*b402 + 2*b180*b589 + 2*b589 - 2*b180*b735 + 4*b735 - 2*b180*
    b962 + 2*b962 + 2*b181*b327 - 2*b181*b402 - 2*b181*b589 + 2*b181*b689 + 2*
    b182*b216 - 2*b182*b594 - 2*b182*b1030 + 2*b1030 - 2*b183*b216 + 2*b183*
    b465 + 2*b465 - 2*b183*b520 + 2*b183*b658 - 2*b658 + 2*b184*b185 - 2*b184*
    b465 + 2*b185*b466 + 2*b466 - 2*b185*b700 - 2*b185*b916 + 2*b916 - 2*b186*
    b357 + 2*b186*b1103 - 2*b186*b1105 + 4*b1105 - 2*b187*b630 + 2*b630 - 2*
    b187*b837 + 2*b187*b978 - 2*b978 - 2*b188*b364 + 2*b188*b837 - 2*b188*b838
     + 2*b838 + 2*b188*b1046 - 2*b1046 + 2*b189*b288 + 2*b189*b417 + 2*b417 - 2
    *b189*b548 - 2*b189*b1047 + 2*b1047 + 2*b190*b359 - 2*b190*b417 - 2*b190*
    b710 - 2*b710 + 2*b191*b279 - 2*b191*b469 + 4*b469 - 2*b191*b577 + 2*b191*
    b716 - 2*b716 + 2*b192*b410 + 2*b410 - 2*b192*b432 + 4*b432 + 2*b193*b407
     + 2*b407 + 2*b193*b618 + 2*b618 - 2*b193*b690 + 4*b690 - 2*b193*b1021 + 2*
    b1021 + 2*b194*b334 - 2*b194*b407 - 2*b194*b618 + 2*b194*b650 - 2*b195*b206
     + 2*b195*b481 + 2*b481 - 2*b195*b503 + 4*b503 + 2*b195*b697 - 2*b697 + 2*
    b196*b197 - 2*b196*b481 + 2*b197*b482 - 2*b197*b661 - 2*b197*b873 + 2*b873
     - 2*b198*b363 + 2*b198*b1038 - 2*b198*b1039 + 4*b1039 - 2*b199*b794 + 2*
    b199*b1040 - 2*b1040 + 2*b199*b1110 + 2*b1110 + 2*b200*b422 + 2*b422 - 2*
    b200*b526 + 2*b200*b600 - 2*b200*b985 + 2*b985 - 2*b201*b455 + 2*b455 - 2*
    b201*b551 + 2*b201*b673 - 2*b673 + 2*b201*b1124 + 2*b1124 + 2*b202*b236 - 2
    *b202*b431 + 2*b431 + 2*b202*b554 + 2*b554 - 2*b202*b579 + 4*b579 + 2*b203*
    b415 + 2*b415 - 2*b203*b426 + 4*b426 - 2*b204*b259 + 2*b204*b319 - 2*b204*
    b811 - 2*b205*b367 + 2*b205*b591 - 2*b591 + 2*b205*b1086 + 2*b1086 - 2*b205
    *b1087 + 2*b1087 + 2*b206*b354 - 2*b206*b744 + 2*b206*b967 - 2*b967 + 2*
    b207*b208 - 2*b207*b503 + 2*b208*b505 - 2*b208*b626 - 2*b208*b830 + 2*b830
     - 2*b209*b369 + 2*b209*b975 - 2*b209*b977 + 4*b977 - 2*b210*b751 + 2*b210*
    b1043 + 2*b1043 + 2*b210*b1106 - 2*b1106 + 2*b211*b425 + 2*b425 - 2*b211*
    b506 + 2*b211*b631 - 2*b211*b928 + 2*b928 + 2*b212*b231 - 2*b212*b437 + 2*
    b437 + 2*b212*b532 + 2*b532 - 2*b212*b606 + 4*b606 + 2*b213*b419 + 2*b419
     - 2*b213*b423 + 4*b423 - 2*b214*b271 + 2*b214*b311 - 2*b214*b771 - 2*b215*
    b371 + 2*b215*b620 - 2*b620 + 2*b215*b1021 - 2*b215*b1022 + 2*b1022 + 2*
    b216*b361 - 2*b216*b787 + 2*b217*b521 - 2*b217*b598 + 2*b217*b660 - 2*b217*
    b789 - 2*b218*b570 + 2*b218*b880 + 2*b880 - 2*b218*b1105 + 2*b219*b254 - 2*
    b219*b707 + 2*b219*b981 + 2*b981 + 2*b220*b429 + 2*b429 - 2*b220*b485 + 4*
    b485 + 2*b220*b667 - 2*b220*b885 + 2*b885 + 2*b221*b222 + 2*b221*b223 - 2*
    b221*b430 + 2*b430 - 2*b221*b444 + 2*b444 - 2*b222*b469 + 2*b222*b601 + 2*
    b601 - 2*b222*b668 + 4*b668 - 2*b223*b508 + 2*b223*b604 - 2*b224*b283 + 2*
    b224*b302 - 2*b224*b725 + 2*b725 - 2*b225*b350 - 2*b225*b378 + 2*b225*b655
     - 2*b655 + 2*b225*b962 + 2*b226*b227 + 2*b226*b228 - 2*b226*b699 + 2*b699
     - 2*b227*b372 + 2*b227*b1097 - 2*b1097 - 2*b227*b1099 + 2*b1099 + 2*b228*
    b542 + 2*b542 - 2*b228*b568 + 4*b568 - 2*b228*b745 + 2*b229*b435 + 2*b435
     - 2*b229*b467 + 4*b467 + 2*b229*b710 - 2*b229*b841 + 2*b841 + 2*b230*b455
     - 2*b230*b487 - 2*b230*b530 + 2*b530 - 2*b231*b457 + 2*b457 + 2*b232*b450
     + 2*b450 + 2*b232*b729 + 2*b729 - 2*b232*b1014 + 4*b1014 + 2*b233*b595 - 2
    *b233*b596 - 2*b233*b597 + 2*b233*b1032 - 2*b1032 - 2*b234*b379 + 2*b234*
    b745 + 2*b234*b1032 - 2*b234*b1034 - 2*b235*b240 + 2*b235*b442 + 2*b442 - 2
    *b235*b453 + 4*b453 + 2*b235*b754 - 2*b754 - 2*b236*b472 + 2*b472 + 2*b237*
    b349 - 2*b237*b685 + 4*b685 - 2*b237*b773 + 2*b237*b958 + 2*b958 + 2*b238*
    b566 - 2*b238*b567 + 2*b238*b969 - 2*b969 - 2*b239*b329 + 2*b239*b789 + 2*
    b239*b969 - 2*b239*b970 + 2*b240*b364 + 2*b240*b796 - 2*b240*b797 + 2*b241*
    b342 - 2*b241*b646 + 4*b646 - 2*b241*b727 + 4*b727 + 2*b241*b1013 + 2*b1013
     + 2*b242*b517 + 2*b517 - 2*b242*b688 + 4*b688 - 2*b243*b263 + 2*b243*b361
     + 2*b243*b540 - 2*b243*b785 + 2*b785 + 2*b244*b540 - 2*b244*b541 + 2*b244*
    b914 + 2*b245*b323 - 2*b245*b573 + 4*b573 + 2*b245*b709 - 2*b245*b1043 - 2*
    b246*b247 + 2*b246*b248 - 2*b246*b456 + 2*b456 + 2*b246*b509 + 2*b247*b310
     + 2*b247*b530 - 2*b247*b578 + 4*b578 - 2*b248*b470 + 2*b470 + 2*b248*b512
     + 2*b512 - 2*b248*b533 + 4*b533 + 2*b249*b333 - 2*b249*b615 + 2*b615 - 2*
    b249*b685 + 2*b249*b1078 + 2*b1078 + 2*b250*b251 + 2*b250*b440 + 2*b440 - 2
    *b250*b462 + 2*b462 - 2*b250*b538 - 2*b251*b649 + 4*b649 + 2*b251*b1085 + 2
    *b252*b539 - 2*b252*b741 + 2*b741 + 2*b252*b782 + 2*b782 + 2*b253*b518 - 2*
    b253*b519 + 2*b253*b870 + 2*b254*b749 - 2*b254*b834 - 2*b254*b879 - 2*b255*
    b546 + 4*b546 + 2*b255*b666 + 2*b255*b708 + 2*b708 - 2*b255*b981 + 2*b256*
    b318 - 2*b256*b470 + 2*b256*b552 + 2*b552 - 2*b256*b605 + 4*b605 + 2*b257*
    b341 - 2*b257*b460 + 4*b460 + 2*b258*b259 - 2*b258*b584 + 2*b584 + 2*b258*
    b858 - 2*b258*b904 + 2*b259*b682 - 2*b682 - 2*b259*b950 + 2*b950 + 2*b260*
    b326 - 2*b260*b587 + 2*b587 - 2*b260*b646 + 2*b261*b560 + 2*b560 - 2*b261*
    b617 + 4*b617 - 2*b261*b910 + 2*b261*b1020 - 2*b262*b263 + 2*b262*b738 + 2*
    b738 + 2*b263*b783 - 2*b783 + 2*b263*b965 - 2*b965 + 2*b264*b501 - 2*b264*
    b502 + 2*b264*b827 - 2*b265*b352 + 2*b265*b827 - 2*b265*b828 + 2*b265*b916
     - 2*b266*b523 + 2*b266*b752 + 2*b752 - 2*b266*b925 + 2*b267*b279 + 2*b267*
    b490 + 2*b490 - 2*b267*b510 + 4*b510 - 2*b267*b1124 + 2*b268*b324 - 2*b268*
    b490 - 2*b268*b636 + 4*b636 - 2*b269*b475 + 4*b475 + 2*b269*b1064 + 2*b1064
     + 2*b270*b271 - 2*b270*b613 + 4*b613 + 2*b270*b812 - 2*b270*b955 + 4*b955
     + 2*b271*b724 - 2*b724 - 2*b271*b901 + 2*b901 + 2*b272*b321 - 2*b272*b559
     + 2*b559 - 2*b272*b615 - 2*b273*b274 + 2*b273*b693 + 2*b693 + 2*b274*b739
     - 2*b739 - 2*b274*b824 + 2*b274*b1027 - 2*b1027 + 2*b275*b479 - 2*b275*
    b480 - 2*b275*b743 + 2*b275*b786 - 2*b276*b355 + 2*b276*b786 - 2*b276*b787
     + 2*b276*b971 + 2*b971 - 2*b277*b357 + 2*b277*b627 + 2*b277*b1100 - 2*b277
    *b1101 + 4*b1101 - 2*b278*b545 + 2*b278*b795 + 2*b795 - 2*b278*b882 - 2*
    b279*b1057 + 4*b1057 - 2*b279*b1059 + 2*b280*b332 - 2*b280*b510 + 2*b280*
    b604 - 2*b280*b676 + 4*b676 - 2*b281*b495 + 4*b495 + 2*b281*b1001 + 2*b1001
     + 2*b282*b283 - 2*b282*b644 + 2*b644 + 2*b282*b772 - 2*b282*b1010 + 2*b283
    *b769 - 2*b769 - 2*b283*b854 + 2*b854 - 2*b284*b292 + 2*b284*b313 + 2*b284*
    b476 - 2*b284*b587 - 2*b285*b286 + 2*b285*b654 + 2*b654 - 2*b285*b964 + 2*
    b286*b694 - 2*b694 - 2*b286*b869 + 2*b286*b1092 - 2*b1092 - 2*b287*b363 + 2
    *b287*b1035 - 2*b287*b1036 + 4*b1036 + 2*b288*b572 - 2*b288*b573 - 2*b288*
    b929 + 2*b289*b489 - 2*b489 - 2*b289*b992 - 2*b289*b994 + 2*b290*b340 - 2*
    b290*b531 + 4*b531 + 2*b290*b635 - 2*b635 - 2*b290*b718 + 4*b718 - 2*b291*
    b515 + 4*b515 + 2*b291*b947 + 2*b947 + 2*b292*b293 - 2*b292*b772 + 2*b292*
    b1076 - 2*b1076 - 2*b293*b726 + 2*b726 - 2*b293*b813 + 2*b293*b1071 + 2*
    b1071 + 2*b294*b334 - 2*b294*b621 - 2*b294*b868 + 2*b294*b1024 + 2*b295*
    b296 + 2*b295*b655 - 2*b295*b913 - 2*b295*b1024 + 2*b296*b502 - 2*b296*b593
     + 2*b593 - 2*b296*b596 - 2*b297*b369 + 2*b297*b972 - 2*b297*b973 + 4*b973
     + 2*b298*b545 - 2*b298*b546 - 2*b298*b986 + 2*b298*b1115 - 2*b1115 + 2*
    b299*b989 + 2*b989 + 2*b299*b1115 - 2*b299*b1116 - 2*b299*b1119 + 2*b1119
     + 2*b300*b509 - 2*b300*b937 + 4*b937 - 2*b300*b939 - 2*b301*b536 + 4*b536
     + 2*b301*b897 + 2*b897 + 2*b302*b559 - 2*b302*b684 + 2*b684 - 2*b302*b773
     + 2*b303*b304 + 2*b303*b647 - 2*b647 - 2*b303*b688 - 2*b303*b777 + 4*b777
     + 2*b304*b1076 - 2*b304*b1077 - 2*b304*b1080 + 2*b305*b327 - 2*b305*b592
     - 2*b305*b822 + 2*b305*b1089 + 2*b306*b307 + 2*b306*b620 - 2*b306*b966 + 2
    *b966 - 2*b306*b1089 + 2*b307*b519 - 2*b307*b567 - 2*b307*b1090 + 2*b1090
     - 2*b308*b374 - 2*b308*b917 + 4*b917 + 2*b309*b1048 - 2*b1048 - 2*b309*
    b1049 + 2*b309*b1051 + 2*b1051 - 2*b309*b1052 + 2*b1052 - 2*b310*b892 + 4*
    b892 - 2*b310*b893 + 2*b311*b587 - 2*b311*b645 + 2*b645 - 2*b311*b727 + 2*
    b312*b313 + 2*b312*b616 - 2*b616 - 2*b312*b733 + 4*b733 - 2*b312*b817 + 4*
    b817 - 2*b313*b1012 - 2*b313*b1015 + 2*b314*b322 - 2*b314*b564 - 2*b314*
    b780 + 2*b315*b316 - 2*b315*b543 + 2*b543 - 2*b315*b629 + 2*b629 - 2*b316*
    b702 - 2*b316*b835 + 2*b316*b921 + 2*b317*b986 - 2*b317*b987 - 2*b317*b990
     + 2*b990 + 2*b317*b1118 + 2*b1118 - 2*b318*b846 + 4*b846 - 2*b318*b847 - 2
    *b319*b614 + 2*b614 + 2*b319*b615 - 2*b319*b685 + 2*b320*b321 - 2*b320*b777
     - 2*b320*b863 + 4*b863 - 2*b321*b957 + 2*b957 - 2*b321*b1079 + 4*b1079 - 2
    *b322*b736 + 4*b736 - 2*b322*b738 + 2*b323*b347 - 2*b323*b880 - 2*b323*b982
     - 2*b982 - 2*b324*b802 + 4*b802 - 2*b324*b804 + 2*b804 + 2*b325*b584 + 2*
    b325*b641 + 2*b641 - 2*b325*b642 + 2*b642 - 2*b325*b644 + 2*b326*b648 - 2*
    b326*b906 + 2*b906 - 2*b326*b1014 - 2*b327*b691 + 4*b691 - 2*b327*b693 + 2*
    b328*b329 - 2*b328*b597 - 2*b328*b1034 - 2*b329*b973 + 2*b330*b338 - 2*b330
    *b836 - 2*b330*b1044 - 2*b1044 + 2*b330*b1111 - 2*b1111 + 2*b331*b600 + 2*
    b331*b1111 - 2*b331*b1112 + 2*b1112 - 2*b331*b1114 + 2*b1114 + 2*b332*b759
     - 2*b332*b760 + 4*b760 - 2*b332*b762 + 2*b762 + 2*b333*b687 + 2*b687 - 2*
    b333*b860 + 2*b860 - 2*b333*b959 + 4*b959 - 2*b334*b652 + 4*b652 - 2*b334*
    b654 + 2*b335*b624 - 2*b624 + 2*b335*b1092 - 2*b335*b1093 + 2*b1093 - 2*
    b335*b1096 + 4*b1096 + 2*b336*b337 - 2*b336*b625 - 2*b336*b1099 - 2*b337*
    b915 - 2*b915 - 2*b337*b917 + 2*b338*b793 - 2*b338*b795 + 2*b339*b631 + 2*
    b339*b1044 - 2*b339*b1045 - 2*b339*b1047 + 2*b340*b714 - 2*b340*b715 + 4*
    b715 - 2*b340*b717 + 2*b717 + 2*b341*b642 - 2*b341*b1063 - 2*b341*b1066 + 2
    *b1066 + 2*b342*b732 + 2*b732 - 2*b342*b814 + 2*b814 - 2*b342*b907 + 4*b907
     + 2*b343*b377 - 2*b343*b654 + 2*b343*b910 - 2*b343*b963 - 2*b963 + 2*b344*
    b658 + 2*b344*b1027 - 2*b344*b1028 + 2*b1028 - 2*b344*b1031 + 4*b1031 + 2*
    b345*b871 - 2*b345*b872 - 2*b872 - 2*b345*b875 + 4*b875 + 2*b346*b662 + 2*
    b662 - 2*b346*b699 - 2*b346*b701 + 4*b701 + 2*b347*b750 - 2*b347*b752 + 2*
    b348*b667 + 2*b348*b982 - 2*b348*b983 - 2*b348*b985 - 2*b349*b774 + 2*b774
     + 2*b349*b776 + 2*b776 - 2*b349*b862 + 4*b862 + 2*b350*b380 - 2*b350*b693
     + 2*b351*b697 + 2*b351*b965 - 2*b351*b966 - 2*b351*b968 + 4*b968 + 2*b352*
    b699 + 2*b352*b829 - 2*b352*b831 + 4*b831 + 2*b353*b710 + 2*b353*b926 - 2*
    b926 - 2*b353*b928 + 2*b354*b912 - 2*b912 - 2*b354*b913 - 2*b354*b1030 + 2*
    b355*b746 + 2*b746 + 2*b355*b788 - 2*b788 - 2*b355*b790 + 4*b790 + 2*b356*
    b357 - 2*b356*b749 - 2*b356*b877 + 4*b877 + 2*b357*b1102 + 2*b358*b754 + 2*
    b358*b883 - 2*b883 - 2*b358*b885 + 2*b359*b360 - 2*b359*b755 - 2*b359*b888
     + 2*b888 + 2*b360*b757 + 2*b757 - 2*b360*b844 + 4*b844 - 2*b360*b988 - 2*
    b361*b869 - 2*b361*b1095 + 2*b362*b363 - 2*b362*b792 - 2*b362*b920 + 4*b920
     + 2*b363*b1037 + 2*b364*b839 - 2*b839 - 2*b364*b841 + 2*b365*b366 - 2*b365
    *b806 - 2*b366*b382 + 2*b366*b1127 + 2*b1127 - 2*b366*b1128 + 2*b367*b1088
     - 2*b1088 - 2*b367*b1091 + 2*b368*b369 + 2*b368*b832 - 2*b368*b834 - 2*
    b368*b977 + 2*b369*b974 - 2*b370*b849 + 2*b849 + 2*b370*b1129 - 2*b1129 + 2
    *b371*b1023 - 2*b1023 - 2*b371*b1026 + 2*b372*b872 + 2*b372*b1095 - 2*b372*
    b1096 + 2*b373*b374 + 2*b373*b876 - 2*b373*b877 - 2*b373*b1039 + 2*b374*
    b918 - 2*b918 - 2*b374*b1104 + 2*b1104 + 2*b375*b376 - 2*b375*b895 + 2*b376
    *b996 + 2*b996 - 2*b376*b997 + 4*b997 - 2*b376*b999 + 2*b999 + 2*b377*b1083
     + 2*b1083 - 2*b377*b1084 + 4*b1084 - 2*b377*b1087 + 2*b378*b963 - 2*b378*
    b964 + 2*b379*b915 + 2*b379*b1030 - 2*b379*b1031 + 2*b380*b1018 + 2*b1018
     - 2*b380*b1019 - 2*b380*b1022 + 2*b381*b992 + 2*b381*b1120 + 2*b1120 - 2*
    b381*b1121 + 4*b1121 - 2*b381*b1123 + 4*b1123 + 2*b382*b1129 - 2*b383*b498
     + 2*b498 - 2*b384*b941 + 2*b384*b993 - 2*b993 + 2*b385*b1058 - 2*b386*b428
     + 2*b386 + 2*b428 - 2*b386*b728 - 2*b386*b954 + 2*b386*b1073 - 2*b387*b433
     + 2*b433 - 2*b387*b903 - 2*b388*b428 - 2*b388*b439 + 2*b439 - 2*b388*b857
     - 2*b389*b433 - 2*b389*b449 - 2*b390*b412 + 2*b412 - 2*b390*b539 - 2*b391*
    b439 - 2*b391*b461 - 2*b393*b449 - 2*b394*b976 - 2*b395*b461 - 2*b395*b497
     - 2*b396*b543 - 2*b397*b653 + 2*b653 - 2*b398*b569 + 2*b569 - 2*b398*b748
     + 2*b398*b832 - 2*b399*b692 + 2*b692 - 2*b400*b599 + 2*b599 - 2*b400*b703
     + 2*b400*b876 - 2*b401*b881 - 2*b401*b1041 - 2*b402*b539 - 2*b402*b737 + 2
    *b737 - 2*b403*b628 + 2*b628 + 2*b403*b919 + 2*b404*b750 + 2*b404 - 2*b404*
    b837 - 2*b404*b1107 - 2*b404*b1109 - 2*b405*b406 + 2*b406 - 2*b405*b447 + 2
    *b447 - 2*b406*b410 - 2*b406*b853 + 2*b853 + 2*b406*b1004 - 2*b407*b562 - 2
    *b407*b781 + 4*b781 - 2*b408*b662 - 2*b408*b748 + 2*b408*b975 - 2*b409*b549
     + 2*b549 + 2*b409*b1048 - 2*b410*b411 + 2*b411 - 2*b410*b459 + 2*b459 - 2*
    b411*b415 - 2*b411*b808 + 2*b808 + 2*b411*b1067 - 2*b1067 - 2*b412*b463 + 2
    *b412*b651 + 2*b651 - 2*b412*b1086 - 2*b413*b701 - 2*b413*b703 + 2*b413*
    b1038 - 2*b414*b575 + 2*b575 + 2*b414*b1115 - 2*b415*b416 - 2*b415*b474 + 2
    *b474 - 2*b416*b419 - 2*b416*b768 - 2*b417*b527 - 2*b417*b601 - 2*b418*b445
     + 2*b418 + 2*b445 - 2*b418*b944 + 4*b944 - 2*b419*b420 - 2*b419*b494 + 2*
    b494 - 2*b420*b423 - 2*b420*b723 + 2*b723 - 2*b421*b770 + 2*b421*b1073 - 2*
    b422*b549 - 2*b422*b632 + 4*b632 - 2*b422*b755 - 2*b423*b424 - 2*b423*b514
     + 2*b514 - 2*b424*b426 - 2*b424*b681 + 2*b681 - 2*b425*b575 - 2*b425*b668
     - 2*b425*b797 - 2*b426*b427 - 2*b426*b535 + 2*b535 - 2*b427*b432 - 2*b427*
    b643 + 2*b643 + 2*b428*b775 - 2*b775 - 2*b428*b958 - 2*b429*b601 - 2*b429*
    b711 + 4*b711 - 2*b429*b842 - 2*b430*b487 + 2*b430*b575 - 2*b430*b711 - 2*
    b431*b492 + 2*b492 - 2*b432*b557 + 2*b557 - 2*b432*b1065 + 2*b433*b730 - 2*
    b730 - 2*b433*b1013 - 2*b434*b504 + 2*b434 - 2*b434*b597 - 2*b434*b830 + 2*
    b434*b969 - 2*b435*b632 - 2*b435*b756 + 4*b756 - 2*b435*b886 - 2*b436*b455
     + 2*b436 - 2*b436*b508 + 2*b436*b549 - 2*b436*b756 - 2*b437*b512 - 2*b438*
    b582 + 2*b582 - 2*b438*b1002 - 2*b438*b1065 + 2*b439*b686 - 2*b686 - 2*b439
    *b1078 - 2*b440*b517 - 2*b440*b731 + 4*b731 - 2*b440*b958 - 2*b441*b625 - 2
    *b441*b873 + 2*b441*b1032 - 2*b442*b668 - 2*b442*b798 + 4*b798 - 2*b442*
    b930 - 2*b443*b469 + 2*b443 + 2*b443*b527 - 2*b443*b529 - 2*b443*b798 - 2*
    b444*b488 - 2*b444*b529 + 2*b444*b635 - 2*b445*b446 + 2*b446 + 2*b445*b511
     + 2*b511 - 2*b445*b637 + 4*b637 - 2*b446*b533 - 2*b447*b460 - 2*b448*b609
     + 2*b609 - 2*b448*b948 + 2*b948 - 2*b448*b1002 + 2*b449*b647 - 2*b450*b517
     - 2*b450*b560 - 2*b450*b1013 - 2*b451*b501 + 2*b451*b623 - 2*b452*b659 - 2
    *b452*b916 + 2*b452*b1097 - 2*b453*b711 - 2*b453*b843 + 4*b843 - 2*b453*
    b987 - 2*b454*b487 - 2*b454*b551 - 2*b454*b843 - 2*b455*b1053 + 4*b1053 - 2
    *b456*b490 + 2*b456*b492 - 2*b456*b555 + 4*b555 - 2*b457*b458 + 2*b458 + 2*
    b457*b491 + 2*b491 - 2*b457*b677 + 4*b677 - 2*b458*b555 - 2*b459*b475 - 2*
    b460*b898 + 2*b898 - 2*b460*b948 + 2*b461*b616 - 2*b462*b588 + 4*b588 + 2*
    b462*b861 - 2*b861 - 2*b462*b1078 - 2*b463*b517 - 2*b463*b588 - 2*b464*b479
     + 2*b464*b1094 - 2*b1094 - 2*b465*b698 - 2*b465*b971 - 2*b466*b627 - 2*
    b466*b699 - 2*b466*b1103 - 2*b467*b756 - 2*b467*b887 + 4*b887 - 2*b467*
    b1049 - 2*b468*b508 - 2*b468*b577 - 2*b468*b887 - 2*b469*b671 + 4*b671 - 2*
    b470*b471 + 2*b471 + 2*b470*b489 + 2*b471*b472 - 2*b471*b510 - 2*b471*b580
     + 4*b580 - 2*b472*b473 + 2*b473 - 2*b472*b719 + 4*b719 - 2*b473*b580 - 2*
    b474*b495 - 2*b475*b851 - 2*b475*b898 - 2*b476*b516 + 2*b516 - 2*b477*b560
     - 2*b477*b617 + 2*b477*b815 - 2*b478*b480 + 2*b478*b785 + 2*b478*b1029 - 2
    *b1029 + 2*b479*b1027 + 2*b480*b1092 - 2*b481*b744 - 2*b481*b1033 + 2*b1033
     - 2*b482*b746 - 2*b482*b1038 - 2*b483*b484 + 2*b484 - 2*b483*b544 + 2*b544
     - 2*b483*b706 - 2*b484*b522 - 2*b484*b572 + 2*b484*b838 - 2*b485*b798 - 2*
    b485*b932 + 4*b932 - 2*b485*b1116 - 2*b486*b529 - 2*b486*b603 - 2*b486*b932
     + 2*b488*b489 - 2*b489*b531 - 2*b490*b491 - 2*b491*b531 - 2*b491*b607 + 4*
    b607 - 2*b492*b493 + 2*b493 - 2*b492*b764 + 4*b764 - 2*b493*b607 - 2*b494*
    b515 - 2*b495*b807 + 2*b807 - 2*b495*b851 - 2*b496*b612 + 4*b612 + 2*b496*
    b809 - 2*b809 - 2*b496*b1071 - 2*b497*b498 - 2*b498*b537 + 2*b537 + 2*b498*
    b1076 - 2*b499*b588 - 2*b499*b649 + 2*b499*b775 - 2*b500*b502 + 2*b500*b742
     + 2*b742 + 2*b500*b967 + 2*b501*b965 - 2*b503*b787 - 2*b503*b1098 + 2*
    b1098 + 2*b504*b972 - 2*b505*b790 - 2*b505*b975 - 2*b506*b843 - 2*b506*b989
     - 2*b507*b551 - 2*b507*b634 - 2*b507*b989 - 2*b509*b553 + 4*b553 - 2*b510*
    b511 - 2*b511*b553 - 2*b511*b638 + 4*b638 - 2*b512*b513 + 2*b513 - 2*b512*
    b1127 - 2*b513*b638 - 2*b514*b536 - 2*b515*b767 + 2*b767 - 2*b515*b807 - 2*
    b516*b617 - 2*b516*b688 + 2*b516*b730 + 2*b518*b912 - 2*b520*b660 - 2*b520*
    b828 - 2*b521*b831 - 2*b521*b919 - 2*b522*b524 - 2*b522*b525 - 2*b523*b525
     - 2*b523*b574 - 2*b524*b573 + 2*b524*b1048 - 2*b525*b1048 - 2*b526*b887 - 
    2*b526*b1051 - 2*b527*b528 + 4*b528 - 2*b528*b577 - 2*b528*b670 - 2*b528*
    b1051 - 2*b530*b938 - 2*b530*b1123 - 2*b531*b532 - 2*b532*b578 - 2*b532*
    b678 + 4*b678 - 2*b533*b534 + 2*b534 - 2*b533*b1061 + 2*b1061 - 2*b534*b678
     - 2*b535*b558 + 4*b558 - 2*b536*b722 + 2*b722 - 2*b536*b767 - 2*b537*b649
     + 2*b537*b686 - 2*b537*b733 - 2*b538*b733 - 2*b541*b823 + 4*b823 - 2*b542*
    b543 - 2*b542*b875 - 2*b542*b876 + 2*b543*b918 - 2*b544*b546 - 2*b544*b665
     + 2*b544*b884 - 2*b546*b547 + 2*b547*b986 + 2*b547*b1113 - 2*b548*b932 - 2
    *b548*b1118 - 2*b549*b550 + 4*b550 - 2*b550*b603 - 2*b550*b713 - 2*b550*
    b1118 - 2*b552*b671 - 2*b552*b993 - 2*b552*b1057 - 2*b553*b554 - 2*b553*
    b675 + 2*b675 - 2*b554*b605 - 2*b554*b720 - 2*b555*b556 + 2*b556 - 2*b555*
    b996 - 2*b556*b720 - 2*b557*b583 + 4*b583 - 2*b558*b680 + 2*b680 - 2*b558*
    b722 - 2*b558*b850 + 2*b850 - 2*b559*b812 - 2*b559*b1076 - 2*b560*b561 - 2*
    b561*b777 - 2*b562*b564 + 2*b562*b783 - 2*b563*b741 - 2*b563*b781 + 2*b563*
    b1090 - 2*b564*b1090 - 2*b565*b567 + 2*b565*b622 + 2*b622 + 2*b566*b824 - 2
    *b568*b569 - 2*b568*b832 - 2*b568*b917 - 2*b569*b663 + 2*b569*b974 - 2*b570
    *b663 - 2*b570*b705 + 2*b705 - 2*b571*b573 - 2*b571*b630 + 2*b571*b927 + 2*
    b574*b929 + 2*b574*b1046 - 2*b575*b576 + 2*b576 - 2*b576*b634 - 2*b576*b758
     + 2*b576*b1119 - 2*b578*b579 - 2*b578*b717 - 2*b579*b636 - 2*b579*b765 - 2
    *b580*b581 + 2*b581 - 2*b580*b942 + 4*b942 - 2*b581*b765 - 2*b582*b610 + 4*
    b610 - 2*b583*b641 - 2*b583*b680 - 2*b583*b896 + 2*b896 - 2*b584*b585 - 2*
    b584*b1005 + 2*b1005 - 2*b585*b586 - 2*b585*b856 - 2*b586*b646 - 2*b587*
    b858 - 2*b588*b589 - 2*b589*b817 - 2*b590*b592 + 2*b590*b739 - 2*b590*b1086
     - 2*b591*b593 + 2*b591*b737 + 2*b591*b1025 - 2*b592*b593 + 2*b593*b594 - 2
    *b594*b596 + 2*b595*b869 - 2*b598*b599 - 2*b598*b973 - 2*b599*b702 + 2*b599
    *b1037 - 2*b601*b602 + 2*b602 - 2*b602*b670 - 2*b602*b801 + 4*b801 + 2*b602
    *b1052 - 2*b603*b759 - 2*b604*b937 - 2*b605*b606 - 2*b605*b762 - 2*b606*
    b676 - 2*b606*b806 - 2*b607*b608 + 2*b608 - 2*b607*b997 - 2*b608*b806 - 2*
    b609*b640 + 4*b640 - 2*b610*b611 + 4*b611 - 2*b610*b641 - 2*b610*b946 + 2*
    b946 - 2*b611*b612 - 2*b611*b640 - 2*b611*b681 - 2*b612*b613 - 2*b612*b852
     - 2*b613*b614 - 2*b613*b1068 + 2*b1068 + 2*b614*b857 - 2*b614*b902 - 2*
    b615*b904 - 2*b616*b687 + 2*b616*b1077 - 2*b617*b618 - 2*b618*b863 - 2*b619
    *b621 + 2*b619*b694 - 2*b619*b1021 - 2*b620*b622 + 2*b620*b692 - 2*b621*
    b622 - 2*b622*b1092 + 2*b623*b624 + 2*b623*b913 - 2*b624*b625 + 2*b624*
    b1097 - 2*b626*b628 - 2*b626*b1036 + 2*b627*b747 + 2*b747 - 2*b628*b747 + 2
    *b628*b1102 - 2*b629*b747 - 2*b629*b793 + 2*b629*b978 - 2*b630*b879 + 2*
    b630*b1044 - 2*b632*b633 + 2*b633 - 2*b632*b1053 - 2*b633*b713 - 2*b633*
    b845 + 4*b845 + 2*b633*b990 - 2*b634*b714 - 2*b635*b892 + 2*b635*b1058 - 2*
    b636*b637 - 2*b636*b804 - 2*b637*b718 - 2*b637*b849 - 2*b638*b639 + 2*b639
     - 2*b638*b1062 - 2*b639*b849 - 2*b640*b642 - 2*b640*b1000 + 2*b1000 - 2*
    b641*b723 - 2*b642*b643 + 2*b643*b644 - 2*b643*b770 - 2*b644*b645 + 2*b645*
    b903 - 2*b645*b952 - 2*b646*b955 - 2*b647*b732 + 2*b647*b1012 - 2*b648*b817
     - 2*b648*b908 + 4*b908 - 2*b649*b651 - 2*b650*b652 + 2*b650*b1082 + 2*
    b1082 - 2*b651*b652 - 2*b651*b908 - 2*b652*b1086 + 2*b653*b655 - 2*b653*
    b656 - 2*b653*b962 - 2*b654*b656 - 2*b655*b657 - 2*b656*b657 - 2*b657*b1027
     - 2*b658*b659 + 2*b658*b1094 - 2*b659*b871 - 2*b661*b662 - 2*b661*b1101 - 
    2*b662*b791 - 2*b663*b664 + 2*b664 - 2*b664*b750 - 2*b664*b791 + 2*b664*
    b1040 - 2*b665*b923 + 2*b665*b982 + 2*b666*b667 - 2*b668*b669 + 2*b669 - 2*
    b669*b758 - 2*b669*b890 + 4*b890 + 2*b669*b933 + 2*b933 - 2*b670*b672 - 2*
    b671*b674 - 2*b671*b1056 + 4*b1056 - 2*b672*b674 - 2*b672*b890 + 2*b673*
    b675 - 2*b673*b846 + 2*b673*b993 - 2*b674*b675 - 2*b675*b763 + 4*b763 - 2*
    b676*b677 - 2*b676*b847 - 2*b677*b763 - 2*b677*b895 - 2*b678*b679 + 2*b679
     - 2*b678*b1128 - 2*b679*b895 + 2*b680*b682 - 2*b680*b768 + 2*b681*b683 + 2
    *b683 - 2*b681*b810 - 2*b682*b683 + 2*b682*b1066 - 2*b683*b684 - 2*b683*
    b1071 + 2*b684*b954 - 2*b684*b1007 + 2*b1007 - 2*b685*b1010 - 2*b686*b776
     + 2*b686*b957 - 2*b687*b863 - 2*b687*b960 + 4*b960 - 2*b688*b690 - 2*b689*
    b691 + 2*b689*b1017 + 2*b1017 - 2*b690*b691 - 2*b690*b960 - 2*b691*b1021 - 
    2*b692*b695 - 2*b692*b911 - 2*b693*b695 - 2*b694*b696 + 2*b694*b963 - 2*
    b695*b696 - 2*b696*b965 - 2*b697*b698 + 2*b697*b1029 - 2*b698*b829 - 2*b700
    *b701 - 2*b701*b833 - 2*b702*b704 - 2*b704*b833 + 2*b704*b1106 - 2*b705*
    b706 + 2*b705*b792 - 2*b705*b923 - 2*b706*b708 + 2*b707*b926 - 2*b708*b924
     + 2*b924 - 2*b708*b926 + 2*b709*b710 - 2*b711*b712 + 2*b712 - 2*b712*b801
     + 2*b712*b888 - 2*b712*b935 + 4*b935 - 2*b713*b715 - 2*b714*b845 - 2*b715*
    b803 - 2*b715*b935 + 2*b716*b717 - 2*b716*b802 + 2*b716*b938 - 2*b717*b805
     + 4*b805 - 2*b718*b719 - 2*b718*b893 - 2*b719*b805 - 2*b719*b943 - 2*b720*
    b721 + 2*b721 - 2*b721*b943 + 2*b722*b724 - 2*b722*b808 + 2*b723*b725 - 2*
    b723*b855 - 2*b724*b725 + 2*b724*b1003 + 2*b1003 - 2*b725*b726 + 2*b726*
    b1009 - 2*b726*b1070 + 2*b1070 - 2*b727*b729 - 2*b727*b1074 - 2*b728*b731
     + 2*b728*b861 - 2*b729*b731 - 2*b729*b813 - 2*b730*b816 + 4*b816 + 2*b730*
    b906 - 2*b731*b816 - 2*b732*b908 - 2*b732*b1016 + 4*b1016 - 2*b733*b735 - 2
    *b734*b736 + 2*b734*b961 + 2*b961 - 2*b735*b736 - 2*b735*b1016 - 2*b736*
    b962 - 2*b737*b740 - 2*b737*b867 - 2*b738*b740 - 2*b738*b1022 - 2*b739*b742
     + 2*b739*b1023 - 2*b740*b742 - 2*b741*b823 + 2*b741*b912 - 2*b742*b912 + 2
    *b743*b788 - 2*b744*b788 - 2*b745*b746 - 2*b746*b1102 - 2*b747*b749 + 2*
    b751*b883 - 2*b752*b883 - 2*b752*b980 + 2*b980 + 2*b753*b754 + 2*b753*b1111
     - 2*b754*b755 - 2*b756*b757 - 2*b757*b845 - 2*b757*b991 + 4*b991 - 2*b758*
    b760 - 2*b759*b801 - 2*b760*b761 - 2*b760*b991 + 2*b761*b762 - 2*b762*b848
     + 4*b848 - 2*b763*b764 - 2*b763*b939 - 2*b764*b848 - 2*b764*b998 - 2*b765*
    b766 + 2*b766 - 2*b766*b998 + 2*b767*b769 - 2*b767*b853 + 2*b768*b771 - 2*
    b769*b771 + 2*b769*b949 + 2*b949 - 2*b772*b859 - 2*b773*b774 - 2*b774*b859
     + 2*b774*b861 + 2*b775*b860 - 2*b775*b862 - 2*b776*b960 - 2*b776*b1081 + 4
    *b1081 - 2*b777*b778 - 2*b778*b779 - 2*b778*b1081 - 2*b779*b780 - 2*b779*
    b911 - 2*b780*b782 - 2*b781*b784 - 2*b781*b821 - 2*b782*b784 - 2*b782*b1087
     - 2*b783*b785 + 2*b783*b1088 - 2*b784*b785 + 2*b788*b1033 - 2*b789*b790 - 
    2*b790*b1037 - 2*b791*b792 + 2*b794*b839 - 2*b795*b839 - 2*b795*b1042 + 2*
    b1042 + 2*b796*b1044 - 2*b797*b931 - 2*b798*b800 + 4*b800 - 2*b799*b800 - 2
    *b799*b931 - 2*b799*b1053 - 2*b800*b890 - 2*b800*b1055 + 4*b1055 - 2*b801*
    b802 - 2*b802*b1055 + 2*b803*b804 - 2*b804*b894 + 4*b894 - 2*b805*b994 - 2*
    b805*b1127 + 2*b807*b809 - 2*b807*b900 + 2*b808*b811 - 2*b808*b951 - 2*b809
    *b811 + 2*b809*b899 + 2*b899 - 2*b812*b905 - 2*b813*b814 + 2*b814*b815 - 2*
    b814*b905 - 2*b815*b907 - 2*b816*b818 - 2*b816*b1016 - 2*b817*b819 - 2*b818
    *b819 - 2*b818*b907 - 2*b819*b820 - 2*b820*b822 - 2*b820*b867 - 2*b821*b866
     + 2*b821*b1088 - 2*b822*b1088 - 2*b823*b825 - 2*b823*b1025 - 2*b824*b825
     - 2*b825*b826 - 2*b826*b828 - 2*b826*b1097 - 2*b827*b1096 + 2*b829*b1098
     - 2*b830*b831 + 2*b830*b915 - 2*b831*b974 - 2*b833*b834 + 2*b835*b836 - 2*
    b836*b838 - 2*b838*b1108 + 2*b1108 + 2*b839*b984 + 2*b840*b841 + 2*b840*
    b982 - 2*b841*b842 - 2*b842*b988 - 2*b843*b844 - 2*b844*b935 - 2*b844*b1122
     + 4*b1122 - 2*b845*b846 - 2*b846*b1122 - 2*b847*b940 - 2*b848*b1059 - 2*
    b848*b1061 + 2*b849*b941 - 2*b850*b897 + 2*b851*b854 - 2*b852*b854 - 2*b852
    *b897 + 2*b853*b856 - 2*b853*b1006 - 2*b854*b856 + 2*b857*b956 + 2*b956 - 2
    *b858*b956 - 2*b859*b860 - 2*b860*b956 - 2*b861*b959 - 2*b862*b864 - 2*b862
    *b1081 - 2*b863*b865 - 2*b864*b865 - 2*b864*b959 - 2*b865*b866 - 2*b866*
    b868 + 2*b867*b1023 - 2*b868*b1023 + 2*b870*b872 - 2*b870*b1031 + 2*b872*
    b873 - 2*b873*b875 + 2*b874*b918 + 2*b874*b1099 - 2*b875*b918 - 2*b877*b878
     - 2*b877*b1106 - 2*b878*b880 + 2*b879*b882 - 2*b880*b882 + 2*b883*b927 + 2
    *b884*b885 + 2*b884*b926 - 2*b885*b886 - 2*b886*b1050 - 2*b887*b889 + 4*
    b889 - 2*b888*b889 - 2*b888*b1050 - 2*b889*b891 - 2*b889*b991 - 2*b890*b892
     - 2*b891*b892 - 2*b891*b1054 + 4*b1054 - 2*b893*b995 - 2*b894*b996 - 2*
    b894*b1125 - 2*b894*b1127 - 2*b896*b947 - 2*b897*b899 + 2*b898*b901 - 2*
    b898*b1004 - 2*b899*b901 - 2*b899*b947 + 2*b900*b902 - 2*b900*b1069 - 2*
    b901*b902 + 2*b903*b1011 + 2*b1011 - 2*b904*b1011 - 2*b905*b906 - 2*b906*
    b1011 - 2*b907*b909 - 2*b908*b1083 - 2*b909*b1014 - 2*b909*b1083 - 2*b910*
    b1084 + 2*b911*b963 + 2*b914*b915 - 2*b914*b968 - 2*b916*b917 + 2*b919*
    b1104 - 2*b920*b922 - 2*b920*b1040 - 2*b920*b1104 + 2*b921*b924 - 2*b921*
    b1039 - 2*b922*b924 + 2*b923*b925 - 2*b924*b925 + 2*b927*b928 - 2*b928*b930
     + 2*b929*b1117 + 2*b1117 - 2*b930*b1117 - 2*b931*b933 - 2*b932*b934 + 4*
    b934 - 2*b933*b934 - 2*b933*b1117 - 2*b934*b936 - 2*b934*b1055 - 2*b935*
    b937 - 2*b936*b937 - 2*b936*b1121 + 2*b938*b1060 + 2*b1060 - 2*b939*b1060
     - 2*b940*b942 - 2*b940*b1061 - 2*b941*b944 - 2*b942*b944 - 2*b942*b1060 - 
    2*b943*b945 + 2*b945 - 2*b944*b945 - 2*b946*b1001 - 2*b947*b949 + 2*b948*
    b950 - 2*b948*b1067 - 2*b949*b950 - 2*b949*b1001 - 2*b950*b952 + 2*b951*
    b953 - 2*b952*b953 - 2*b953*b955 + 2*b954*b1075 + 2*b1075 - 2*b955*b1075 - 
    2*b956*b957 - 2*b957*b1075 - 2*b958*b1079 - 2*b959*b961 - 2*b960*b1018 - 2*
    b961*b1018 - 2*b961*b1079 - 2*b964*b966 + 2*b966*b1094 - 2*b967*b968 + 2*
    b967*b1093 - 2*b968*b970 - 2*b969*b1030 - 2*b971*b973 - 2*b971*b1100 - 2*
    b972*b1098 + 2*b976*b979 - 2*b977*b978 - 2*b977*b979 + 2*b978*b980 - 2*b979
    *b980 - 2*b980*b981 - 2*b981*b983 - 2*b983*b1113 + 2*b984*b985 - 2*b984*
    b1112 - 2*b985*b987 - 2*b988*b990 - 2*b989*b1120 - 2*b990*b1120 - 2*b991*
    b992 + 2*b993*b1126 + 2*b1126 - 2*b994*b1126 - 2*b995*b996 - 2*b995*b997 - 
    2*b997*b1126 - 2*b998*b999 - 2*b1000*b1064 - 2*b1001*b1003 + 2*b1002*b1005
     - 2*b1003*b1005 - 2*b1003*b1064 + 2*b1004*b1007 - 2*b1005*b1007 + 2*b1006*
    b1008 - 2*b1007*b1008 - 2*b1008*b1010 - 2*b1011*b1012 - 2*b1013*b1015 - 2*
    b1014*b1017 - 2*b1015*b1017 - 2*b1016*b1019 - 2*b1017*b1019 - 2*b1018*b1020
     + 2*b1020*b1022 - 2*b1024*b1026 - 2*b1025*b1028 - 2*b1026*b1028 + 2*b1028*
    b1029 - 2*b1029*b1031 - 2*b1032*b1095 - 2*b1033*b1035 - 2*b1033*b1036 - 2*
    b1034*b1036 - 2*b1039*b1041 + 2*b1040*b1042 - 2*b1041*b1042 - 2*b1042*b1043
     - 2*b1043*b1045 - 2*b1045*b1046 + 2*b1046*b1047 - 2*b1047*b1049 - 2*b1050*
    b1052 - 2*b1051*b1054 - 2*b1052*b1054 - 2*b1053*b1056 - 2*b1054*b1056 - 2*
    b1055*b1057 - 2*b1056*b1057 - 2*b1060*b1062 + 2*b1061*b1129 - 2*b1062*b1129
     - 2*b1064*b1066 + 2*b1065*b1068 - 2*b1066*b1068 + 2*b1067*b1069 + 2*b1067*
    b1070 - 2*b1068*b1070 + 2*b1069*b1072 - 2*b1070*b1072 - 2*b1071*b1074 - 2*
    b1072*b1074 - 2*b1075*b1077 - 2*b1078*b1080 - 2*b1079*b1082 - 2*b1080*b1082
     - 2*b1081*b1084 - 2*b1082*b1084 - 2*b1083*b1085 + 2*b1085*b1087 - 2*b1089*
    b1091 - 2*b1090*b1093 - 2*b1091*b1093 - 2*b1094*b1096 - 2*b1098*b1101 - 2*
    b1099*b1101 - 2*b1104*b1105 - 2*b1105*b1107 + 2*b1106*b1108 - 2*b1107*b1108
     - 2*b1108*b1110 + 2*b1109*b1112 - 2*b1110*b1111 - 2*b1110*b1112 + 2*b1113*
    b1114 - 2*b1114*b1115 - 2*b1114*b1116 - 2*b1117*b1119 - 2*b1118*b1121 - 2*
    b1119*b1121 - 2*b1120*b1122 - 2*b1122*b1123 - 2*b1123*b1124 - 2*b1124*b1125
     - 2*b1126*b1128;