#  MIQCP written by GAMS Convert at 02/15/18 15:48:25
#  
#  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
#       1226        1     1225        0        0        0        0        0
#  FX      0        0        0        0        0        0        0        0
#  
#  Nonzero counts
#      Total    const       NL      DLL
#       1226        1     1225        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;
var b1130 binary >= 0, <= 1;
var b1131 binary >= 0, <= 1;
var b1132 binary >= 0, <= 1;
var b1133 binary >= 0, <= 1;
var b1134 binary >= 0, <= 1;
var b1135 binary >= 0, <= 1;
var b1136 binary >= 0, <= 1;
var b1137 binary >= 0, <= 1;
var b1138 binary >= 0, <= 1;
var b1139 binary >= 0, <= 1;
var b1140 binary >= 0, <= 1;
var b1141 binary >= 0, <= 1;
var b1142 binary >= 0, <= 1;
var b1143 binary >= 0, <= 1;
var b1144 binary >= 0, <= 1;
var b1145 binary >= 0, <= 1;
var b1146 binary >= 0, <= 1;
var b1147 binary >= 0, <= 1;
var b1148 binary >= 0, <= 1;
var b1149 binary >= 0, <= 1;
var b1150 binary >= 0, <= 1;
var b1151 binary >= 0, <= 1;
var b1152 binary >= 0, <= 1;
var b1153 binary >= 0, <= 1;
var b1154 binary >= 0, <= 1;
var b1155 binary >= 0, <= 1;
var b1156 binary >= 0, <= 1;
var b1157 binary >= 0, <= 1;
var b1158 binary >= 0, <= 1;
var b1159 binary >= 0, <= 1;
var b1160 binary >= 0, <= 1;
var b1161 binary >= 0, <= 1;
var b1162 binary >= 0, <= 1;
var b1163 binary >= 0, <= 1;
var b1164 binary >= 0, <= 1;
var b1165 binary >= 0, <= 1;
var b1166 binary >= 0, <= 1;
var b1167 binary >= 0, <= 1;
var b1168 binary >= 0, <= 1;
var b1169 binary >= 0, <= 1;
var b1170 binary >= 0, <= 1;
var b1171 binary >= 0, <= 1;
var b1172 binary >= 0, <= 1;
var b1173 binary >= 0, <= 1;
var b1174 binary >= 0, <= 1;
var b1175 binary >= 0, <= 1;
var b1176 binary >= 0, <= 1;
var b1177 binary >= 0, <= 1;
var b1178 binary >= 0, <= 1;
var b1179 binary >= 0, <= 1;
var b1180 binary >= 0, <= 1;
var b1181 binary >= 0, <= 1;
var b1182 binary >= 0, <= 1;
var b1183 binary >= 0, <= 1;
var b1184 binary >= 0, <= 1;
var b1185 binary >= 0, <= 1;
var b1186 binary >= 0, <= 1;
var b1187 binary >= 0, <= 1;
var b1188 binary >= 0, <= 1;
var b1189 binary >= 0, <= 1;
var b1190 binary >= 0, <= 1;
var b1191 binary >= 0, <= 1;
var b1192 binary >= 0, <= 1;
var b1193 binary >= 0, <= 1;
var b1194 binary >= 0, <= 1;
var b1195 binary >= 0, <= 1;
var b1196 binary >= 0, <= 1;
var b1197 binary >= 0, <= 1;
var b1198 binary >= 0, <= 1;
var b1199 binary >= 0, <= 1;
var b1200 binary >= 0, <= 1;
var b1201 binary >= 0, <= 1;
var b1202 binary >= 0, <= 1;
var b1203 binary >= 0, <= 1;
var b1204 binary >= 0, <= 1;
var b1205 binary >= 0, <= 1;
var b1206 binary >= 0, <= 1;
var b1207 binary >= 0, <= 1;
var b1208 binary >= 0, <= 1;
var b1209 binary >= 0, <= 1;
var b1210 binary >= 0, <= 1;
var b1211 binary >= 0, <= 1;
var b1212 binary >= 0, <= 1;
var b1213 binary >= 0, <= 1;
var b1214 binary >= 0, <= 1;
var b1215 binary >= 0, <= 1;
var b1216 binary >= 0, <= 1;
var b1217 binary >= 0, <= 1;
var b1218 binary >= 0, <= 1;
var b1219 binary >= 0, <= 1;
var b1220 binary >= 0, <= 1;
var b1221 binary >= 0, <= 1;
var b1222 binary >= 0, <= 1;
var b1223 binary >= 0, <= 1;
var b1224 binary >= 0, <= 1;
var b1225 binary >= 0, <= 1;
var b1226 binary >= 0, <= 1;

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