/* PROBLEMA DE RUTAS CON VEH�CULOS CAPACITADOS (CVRP) */ /* Objective function */ min: +503 x_0_1_0 +503 x_0_1_1 +503 x_0_1_2 +503 x_0_1_3 +525 x_0_2_0 +525 x_0_2_1 +525 x_0_2_2 +525 x_0_2_3 +395 x_0_3_0 +395 x_0_3_1 +395 x_0_3_2 +395 x_0_3_3 +6 x_0_4_0 +6 x_0_4_1 +6 x_0_4_2 +6 x_0_4_3 +272 x_0_5_0 +272 x_0_5_1 +272 x_0_5_2 +272 x_0_5_3 +239 x_0_6_0 +239 x_0_6_1 +239 x_0_6_2 +239 x_0_6_3 +234 x_0_7_0 +234 x_0_7_1 +234 x_0_7_2 +234 x_0_7_3 +417 x_0_8_0 +417 x_0_8_1 +417 x_0_8_2 +417 x_0_8_3 +371 x_0_9_0 +371 x_0_9_1 +371 x_0_9_2 +371 x_0_9_3 +239 x_0_10_0 +239 x_0_10_1 +239 x_0_10_2 +239 x_0_10_3 +97 x_0_11_0 +97 x_0_11_1 +97 x_0_11_2 +97 x_0_11_3 +220 x_0_12_0 +220 x_0_12_1 +220 x_0_12_2 +220 x_0_12_3 +504 x_1_0_0 +504 x_1_0_1 +504 x_1_0_2 +504 x_1_0_3 +296 x_1_2_0 +296 x_1_2_1 +296 x_1_2_2 +296 x_1_2_3 +175 x_1_3_0 +175 x_1_3_1 +175 x_1_3_2 +175 x_1_3_3 +153 x_1_4_0 +153 x_1_4_1 +153 x_1_4_2 +153 x_1_4_3 +213 x_1_5_0 +213 x_1_5_1 +213 x_1_5_2 +213 x_1_5_3 +390 x_1_6_0 +390 x_1_6_1 +390 x_1_6_2 +390 x_1_6_3 +368 x_1_7_0 +368 x_1_7_1 +368 x_1_7_2 +368 x_1_7_3 +464 x_1_8_0 +464 x_1_8_1 +464 x_1_8_2 +464 x_1_8_3 +561 x_1_9_0 +561 x_1_9_1 +561 x_1_9_2 +561 x_1_9_3 +475 x_1_10_0 +475 x_1_10_1 +475 x_1_10_2 +475 x_1_10_3 +459 x_1_11_0 +459 x_1_11_1 +459 x_1_11_2 +459 x_1_11_3 +258 x_1_12_0 +258 x_1_12_1 +258 x_1_12_2 +258 x_1_12_3 +527 x_2_0_0 +527 x_2_0_1 +527 x_2_0_2 +527 x_2_0_3 +295 x_2_1_0 +295 x_2_1_1 +295 x_2_1_2 +295 x_2_1_3 +3 x_2_3_0 +3 x_2_3_1 +3 x_2_3_2 +3 x_2_3_3 +381 x_2_4_0 +381 x_2_4_1 +381 x_2_4_2 +381 x_2_4_3 +431 x_2_5_0 +431 x_2_5_1 +431 x_2_5_2 +431 x_2_5_3 +591 x_2_6_0 +591 x_2_6_1 +591 x_2_6_2 +591 x_2_6_3 +428 x_2_7_0 +428 x_2_7_1 +428 x_2_7_2 +428 x_2_7_3 +405 x_2_8_0 +405 x_2_8_1 +405 x_2_8_2 +405 x_2_8_3 +542 x_2_9_0 +542 x_2_9_1 +542 x_2_9_2 +542 x_2_9_3 +535 x_2_10_0 +535 x_2_10_1 +535 x_2_10_2 +535 x_2_10_3 +525 x_2_11_0 +525 x_2_11_1 +525 x_2_11_2 +525 x_2_11_3 +317 x_2_12_0 +317 x_2_12_1 +317 x_2_12_2 +317 x_2_12_3 +396 x_3_0_0 +396 x_3_0_1 +396 x_3_0_2 +396 x_3_0_3 +182 x_3_1_0 +182 x_3_1_1 +182 x_3_1_2 +182 x_3_1_3 +179 x_3_2_0 +179 x_3_2_1 +179 x_3_2_2 +179 x_3_2_3 +224 x_3_4_0 +224 x_3_4_1 +224 x_3_4_2 +224 x_3_4_3 +275 x_3_5_0 +275 x_3_5_1 +275 x_3_5_2 +275 x_3_5_3 +434 x_3_6_0 +434 x_3_6_1 +434 x_3_6_2 +434 x_3_6_3 +298 x_3_7_0 +298 x_3_7_1 +298 x_3_7_2 +298 x_3_7_3 +368 x_3_8_0 +368 x_3_8_1 +368 x_3_8_2 +368 x_3_8_3 +463 x_3_9_0 +463 x_3_9_1 +463 x_3_9_2 +463 x_3_9_3 +406 x_3_10_0 +406 x_3_10_1 +406 x_3_10_2 +406 x_3_10_3 +395 x_3_11_0 +395 x_3_11_1 +395 x_3_11_2 +395 x_3_11_3 +188 x_3_12_0 +188 x_3_12_1 +188 x_3_12_2 +188 x_3_12_3 +362 x_4_0_0 +362 x_4_0_1 +362 x_4_0_2 +362 x_4_0_3 +141 x_4_1_0 +141 x_4_1_1 +141 x_4_1_2 +141 x_4_1_3 +378 x_4_2_0 +378 x_4_2_1 +378 x_4_2_2 +378 x_4_2_3 +220 x_4_3_0 +220 x_4_3_1 +220 x_4_3_2 +220 x_4_3_3 +102 x_4_5_0 +102 x_4_5_1 +102 x_4_5_2 +102 x_4_5_3 +260 x_4_6_0 +260 x_4_6_1 +260 x_4_6_2 +260 x_4_6_3 +361 x_4_7_0 +361 x_4_7_1 +361 x_4_7_2 +361 x_4_7_3 +448 x_4_8_0 +448 x_4_8_1 +448 x_4_8_2 +448 x_4_8_3 +521 x_4_9_0 +521 x_4_9_1 +521 x_4_9_2 +521 x_4_9_3 +459 x_4_10_0 +459 x_4_10_1 +459 x_4_10_2 +459 x_4_10_3 +443 x_4_11_0 +443 x_4_11_1 +443 x_4_11_2 +443 x_4_11_3 +242 x_4_12_0 +242 x_4_12_1 +242 x_4_12_2 +242 x_4_12_3 +271 x_5_0_0 +271 x_5_0_1 +271 x_5_0_2 +271 x_5_0_3 +212 x_5_1_0 +212 x_5_1_1 +212 x_5_1_2 +212 x_5_1_3 +427 x_5_2_0 +427 x_5_2_1 +427 x_5_2_2 +427 x_5_2_3 +272 x_5_3_0 +272 x_5_3_1 +272 x_5_3_2 +272 x_5_3_3 +100 x_5_4_0 +100 x_5_4_1 +100 x_5_4_2 +100 x_5_4_3 +171 x_5_6_0 +171 x_5_6_1 +171 x_5_6_2 +171 x_5_6_3 +291 x_5_7_0 +291 x_5_7_1 +291 x_5_7_2 +291 x_5_7_3 +387 x_5_8_0 +387 x_5_8_1 +387 x_5_8_2 +387 x_5_8_3 +459 x_5_9_0 +459 x_5_9_1 +459 x_5_9_2 +459 x_5_9_3 +398 x_5_10_0 +398 x_5_10_1 +398 x_5_10_2 +398 x_5_10_3 +352 x_5_11_0 +352 x_5_11_1 +352 x_5_11_2 +352 x_5_11_3 +183 x_5_12_0 +183 x_5_12_1 +183 x_5_12_2 +183 x_5_12_3 +4 x_6_0_0 +4 x_6_0_1 +4 x_6_0_2 +4 x_6_0_3 +373 x_6_1_0 +373 x_6_1_1 +373 x_6_1_2 +373 x_6_1_3 +587 x_6_2_0 +587 x_6_2_1 +587 x_6_2_2 +587 x_6_2_3 +431 x_6_3_0 +431 x_6_3_1 +431 x_6_3_2 +431 x_6_3_3 +259 x_6_4_0 +259 x_6_4_1 +259 x_6_4_2 +259 x_6_4_3 +170 x_6_5_0 +170 x_6_5_1 +170 x_6_5_2 +170 x_6_5_3 +409 x_6_7_0 +409 x_6_7_1 +409 x_6_7_2 +409 x_6_7_3 +547 x_6_8_0 +547 x_6_8_1 +547 x_6_8_2 +547 x_6_8_3 +571 x_6_9_0 +571 x_6_9_1 +571 x_6_9_2 +571 x_6_9_3 +464 x_6_10_0 +464 x_6_10_1 +464 x_6_10_2 +464 x_6_10_3 +322 x_6_11_0 +322 x_6_11_1 +322 x_6_11_2 +322 x_6_11_3 +342 x_6_12_0 +342 x_6_12_1 +342 x_6_12_2 +342 x_6_12_3 +229 x_7_0_0 +229 x_7_0_1 +229 x_7_0_2 +229 x_7_0_3 +367 x_7_1_0 +367 x_7_1_1 +367 x_7_1_2 +367 x_7_1_3 +427 x_7_2_0 +427 x_7_2_1 +427 x_7_2_2 +427 x_7_2_3 +296 x_7_3_0 +296 x_7_3_1 +296 x_7_3_2 +296 x_7_3_3 +352 x_7_4_0 +352 x_7_4_1 +352 x_7_4_2 +352 x_7_4_3 +290 x_7_5_0 +290 x_7_5_1 +290 x_7_5_2 +290 x_7_5_3 +404 x_7_6_0 +404 x_7_6_1 +404 x_7_6_2 +404 x_7_6_3 +225 x_7_8_0 +225 x_7_8_1 +225 x_7_8_2 +225 x_7_8_3 +217 x_7_9_0 +217 x_7_9_1 +217 x_7_9_2 +217 x_7_9_3 +162 x_7_10_0 +162 x_7_10_1 +162 x_7_10_2 +162 x_7_10_3 +227 x_7_11_0 +227 x_7_11_1 +227 x_7_11_2 +227 x_7_11_3 +126 x_7_12_0 +126 x_7_12_1 +126 x_7_12_2 +126 x_7_12_3 +421 x_8_0_0 +421 x_8_0_1 +421 x_8_0_2 +421 x_8_0_3 +462 x_8_1_0 +462 x_8_1_1 +462 x_8_1_2 +462 x_8_1_3 +401 x_8_2_0 +401 x_8_2_1 +401 x_8_2_2 +401 x_8_2_3 +362 x_8_3_0 +362 x_8_3_1 +362 x_8_3_2 +362 x_8_3_3 +448 x_8_4_0 +448 x_8_4_1 +448 x_8_4_2 +448 x_8_4_3 +387 x_8_5_0 +387 x_8_5_1 +387 x_8_5_2 +387 x_8_5_3 +545 x_8_6_0 +545 x_8_6_1 +545 x_8_6_2 +545 x_8_6_3 +226 x_8_7_0 +226 x_8_7_1 +226 x_8_7_2 +226 x_8_7_3 +158 x_8_9_0 +158 x_8_9_1 +158 x_8_9_2 +158 x_8_9_3 +289 x_8_10_0 +289 x_8_10_1 +289 x_8_10_2 +289 x_8_10_3 +419 x_8_11_0 +419 x_8_11_1 +419 x_8_11_2 +419 x_8_11_3 +217 x_8_12_0 +217 x_8_12_1 +217 x_8_12_2 +217 x_8_12_3 +370 x_9_0_0 +370 x_9_0_1 +370 x_9_0_2 +370 x_9_0_3 +559 x_9_1_0 +559 x_9_1_1 +559 x_9_1_2 +559 x_9_1_3 +542 x_9_2_0 +542 x_9_2_1 +542 x_9_2_2 +542 x_9_2_3 +460 x_9_3_0 +460 x_9_3_1 +460 x_9_3_2 +460 x_9_3_3 +523 x_9_4_0 +523 x_9_4_1 +523 x_9_4_2 +523 x_9_4_3 +461 x_9_5_0 +461 x_9_5_1 +461 x_9_5_2 +461 x_9_5_3 +567 x_9_6_0 +567 x_9_6_1 +567 x_9_6_2 +567 x_9_6_3 +221 x_9_7_0 +221 x_9_7_1 +221 x_9_7_2 +221 x_9_7_3 +159 x_9_8_0 +159 x_9_8_1 +159 x_9_8_2 +159 x_9_8_3 +150 x_9_10_0 +150 x_9_10_1 +150 x_9_10_2 +150 x_9_10_3 +284 x_9_11_0 +284 x_9_11_1 +284 x_9_11_2 +284 x_9_11_3 +295 x_9_12_0 +295 x_9_12_1 +295 x_9_12_2 +295 x_9_12_3 +236 x_10_0_0 +236 x_10_0_1 +236 x_10_0_2 +236 x_10_0_3 +475 x_10_1_0 +475 x_10_1_1 +475 x_10_1_2 +475 x_10_1_3 +535 x_10_2_0 +535 x_10_2_1 +535 x_10_2_2 +535 x_10_2_3 +405 x_10_3_0 +405 x_10_3_1 +405 x_10_3_2 +405 x_10_3_3 +460 x_10_4_0 +460 x_10_4_1 +460 x_10_4_2 +460 x_10_4_3 +399 x_10_5_0 +399 x_10_5_1 +399 x_10_5_2 +399 x_10_5_3 +460 x_10_6_0 +460 x_10_6_1 +460 x_10_6_2 +460 x_10_6_3 +165 x_10_7_0 +165 x_10_7_1 +165 x_10_7_2 +165 x_10_7_3 +288 x_10_8_0 +288 x_10_8_1 +288 x_10_8_2 +288 x_10_8_3 +144 x_10_9_0 +144 x_10_9_1 +144 x_10_9_2 +144 x_10_9_3 +154 x_10_11_0 +154 x_10_11_1 +154 x_10_11_2 +154 x_10_11_3 +233 x_10_12_0 +233 x_10_12_1 +233 x_10_12_2 +233 x_10_12_3 +93 x_11_0_0 +93 x_11_0_1 +93 x_11_0_2 +93 x_11_0_3 +456 x_11_1_0 +456 x_11_1_1 +456 x_11_1_2 +456 x_11_1_3 +521 x_11_2_0 +521 x_11_2_1 +521 x_11_2_2 +521 x_11_2_3 +391 x_11_3_0 +391 x_11_3_1 +391 x_11_3_2 +391 x_11_3_3 +437 x_11_4_0 +437 x_11_4_1 +437 x_11_4_2 +437 x_11_4_3 +349 x_11_5_0 +349 x_11_5_1 +349 x_11_5_2 +349 x_11_5_3 +318 x_11_6_0 +318 x_11_6_1 +318 x_11_6_2 +318 x_11_6_3 +230 x_11_7_0 +230 x_11_7_1 +230 x_11_7_2 +230 x_11_7_3 +419 x_11_8_0 +419 x_11_8_1 +419 x_11_8_2 +419 x_11_8_3 +283 x_11_9_0 +283 x_11_9_1 +283 x_11_9_2 +283 x_11_9_3 +155 x_11_10_0 +155 x_11_10_1 +155 x_11_10_2 +155 x_11_10_3 +217 x_11_12_0 +217 x_11_12_1 +217 x_11_12_2 +217 x_11_12_3 +218 x_12_0_0 +218 x_12_0_1 +218 x_12_0_2 +218 x_12_0_3 +257 x_12_1_0 +257 x_12_1_1 +257 x_12_1_2 +257 x_12_1_3 +317 x_12_2_0 +317 x_12_2_1 +317 x_12_2_2 +317 x_12_2_3 +187 x_12_3_0 +187 x_12_3_1 +187 x_12_3_2 +187 x_12_3_3 +242 x_12_4_0 +242 x_12_4_1 +242 x_12_4_2 +242 x_12_4_3 +183 x_12_5_0 +183 x_12_5_1 +183 x_12_5_2 +183 x_12_5_3 +341 x_12_6_0 +341 x_12_6_1 +341 x_12_6_2 +341 x_12_6_3 +123 x_12_7_0 +123 x_12_7_1 +123 x_12_7_2 +123 x_12_7_3 +218 x_12_8_0 +218 x_12_8_1 +218 x_12_8_2 +218 x_12_8_3 +292 x_12_9_0 +292 x_12_9_1 +292 x_12_9_2 +292 x_12_9_3 +230 x_12_10_0 +230 x_12_10_1 +230 x_12_10_2 +230 x_12_10_3 +216 x_12_11_0 +216 x_12_11_1 +216 x_12_11_2 +216 x_12_11_3; /* Constraints */ r1: +y_0_0 +y_0_1 +y_0_2 +y_0_3 <= 4; r2: +y_1_0 +y_1_1 +y_1_2 +y_1_3 = 1; r3: +y_2_0 +y_2_1 +y_2_2 +y_2_3 = 1; r4: +y_3_0 +y_3_1 +y_3_2 +y_3_3 = 1; r5: +y_4_0 +y_4_1 +y_4_2 +y_4_3 = 1; r6: +y_5_0 +y_5_1 +y_5_2 +y_5_3 = 1; r7: +y_6_0 +y_6_1 +y_6_2 +y_6_3 = 1; r8: +y_7_0 +y_7_1 +y_7_2 +y_7_3 = 1; r9: +y_8_0 +y_8_1 +y_8_2 +y_8_3 = 1; r10: +y_9_0 +y_9_1 +y_9_2 +y_9_3 = 1; r11: +y_10_0 +y_10_1 +y_10_2 +y_10_3 = 1; r12: +y_11_0 +y_11_1 +y_11_2 +y_11_3 = 1; r13: +y_12_0 +y_12_1 +y_12_2 +y_12_3 = 1; r14: +x_0_1_0 +x_0_2_0 +x_0_3_0 +x_0_4_0 +x_0_5_0 +x_0_6_0 +x_0_7_0 +x_0_8_0 +x_0_9_0 +x_0_10_0 +x_0_11_0 +x_0_12_0 -y_0_0 = 0; r15: +x_0_1_1 +x_0_2_1 +x_0_3_1 +x_0_4_1 +x_0_5_1 +x_0_6_1 +x_0_7_1 +x_0_8_1 +x_0_9_1 +x_0_10_1 +x_0_11_1 +x_0_12_1 -y_0_1 = 0; r16: +x_0_1_2 +x_0_2_2 +x_0_3_2 +x_0_4_2 +x_0_5_2 +x_0_6_2 +x_0_7_2 +x_0_8_2 +x_0_9_2 +x_0_10_2 +x_0_11_2 +x_0_12_2 -y_0_2 = 0; r17: +x_0_1_3 +x_0_2_3 +x_0_3_3 +x_0_4_3 +x_0_5_3 +x_0_6_3 +x_0_7_3 +x_0_8_3 +x_0_9_3 +x_0_10_3 +x_0_11_3 +x_0_12_3 -y_0_3 = 0; r18: +x_1_0_0 +x_1_2_0 +x_1_3_0 +x_1_4_0 +x_1_5_0 +x_1_6_0 +x_1_7_0 +x_1_8_0 +x_1_9_0 +x_1_10_0 +x_1_11_0 +x_1_12_0 -y_1_0 = 0; r19: +x_1_0_1 +x_1_2_1 +x_1_3_1 +x_1_4_1 +x_1_5_1 +x_1_6_1 +x_1_7_1 +x_1_8_1 +x_1_9_1 +x_1_10_1 +x_1_11_1 +x_1_12_1 -y_1_1 = 0; r20: +x_1_0_2 +x_1_2_2 +x_1_3_2 +x_1_4_2 +x_1_5_2 +x_1_6_2 +x_1_7_2 +x_1_8_2 +x_1_9_2 +x_1_10_2 +x_1_11_2 +x_1_12_2 -y_1_2 = 0; r21: +x_1_0_3 +x_1_2_3 +x_1_3_3 +x_1_4_3 +x_1_5_3 +x_1_6_3 +x_1_7_3 +x_1_8_3 +x_1_9_3 +x_1_10_3 +x_1_11_3 +x_1_12_3 -y_1_3 = 0; r22: +x_2_0_0 +x_2_1_0 +x_2_3_0 +x_2_4_0 +x_2_5_0 +x_2_6_0 +x_2_7_0 +x_2_8_0 +x_2_9_0 +x_2_10_0 +x_2_11_0 +x_2_12_0 -y_2_0 = 0; r23: +x_2_0_1 +x_2_1_1 +x_2_3_1 +x_2_4_1 +x_2_5_1 +x_2_6_1 +x_2_7_1 +x_2_8_1 +x_2_9_1 +x_2_10_1 +x_2_11_1 +x_2_12_1 -y_2_1 = 0; r24: +x_2_0_2 +x_2_1_2 +x_2_3_2 +x_2_4_2 +x_2_5_2 +x_2_6_2 +x_2_7_2 +x_2_8_2 +x_2_9_2 +x_2_10_2 +x_2_11_2 +x_2_12_2 -y_2_2 = 0; r25: +x_2_0_3 +x_2_1_3 +x_2_3_3 +x_2_4_3 +x_2_5_3 +x_2_6_3 +x_2_7_3 +x_2_8_3 +x_2_9_3 +x_2_10_3 +x_2_11_3 +x_2_12_3 -y_2_3 = 0; r26: +x_3_0_0 +x_3_1_0 +x_3_2_0 +x_3_4_0 +x_3_5_0 +x_3_6_0 +x_3_7_0 +x_3_8_0 +x_3_9_0 +x_3_10_0 +x_3_11_0 +x_3_12_0 -y_3_0 = 0; r27: +x_3_0_1 +x_3_1_1 +x_3_2_1 +x_3_4_1 +x_3_5_1 +x_3_6_1 +x_3_7_1 +x_3_8_1 +x_3_9_1 +x_3_10_1 +x_3_11_1 +x_3_12_1 -y_3_1 = 0; r28: +x_3_0_2 +x_3_1_2 +x_3_2_2 +x_3_4_2 +x_3_5_2 +x_3_6_2 +x_3_7_2 +x_3_8_2 +x_3_9_2 +x_3_10_2 +x_3_11_2 +x_3_12_2 -y_3_2 = 0; r29: +x_3_0_3 +x_3_1_3 +x_3_2_3 +x_3_4_3 +x_3_5_3 +x_3_6_3 +x_3_7_3 +x_3_8_3 +x_3_9_3 +x_3_10_3 +x_3_11_3 +x_3_12_3 -y_3_3 = 0; r30: +x_4_0_0 +x_4_1_0 +x_4_2_0 +x_4_3_0 +x_4_5_0 +x_4_6_0 +x_4_7_0 +x_4_8_0 +x_4_9_0 +x_4_10_0 +x_4_11_0 +x_4_12_0 -y_4_0 = 0; r31: +x_4_0_1 +x_4_1_1 +x_4_2_1 +x_4_3_1 +x_4_5_1 +x_4_6_1 +x_4_7_1 +x_4_8_1 +x_4_9_1 +x_4_10_1 +x_4_11_1 +x_4_12_1 -y_4_1 = 0; r32: +x_4_0_2 +x_4_1_2 +x_4_2_2 +x_4_3_2 +x_4_5_2 +x_4_6_2 +x_4_7_2 +x_4_8_2 +x_4_9_2 +x_4_10_2 +x_4_11_2 +x_4_12_2 -y_4_2 = 0; r33: +x_4_0_3 +x_4_1_3 +x_4_2_3 +x_4_3_3 +x_4_5_3 +x_4_6_3 +x_4_7_3 +x_4_8_3 +x_4_9_3 +x_4_10_3 +x_4_11_3 +x_4_12_3 -y_4_3 = 0; r34: +x_5_0_0 +x_5_1_0 +x_5_2_0 +x_5_3_0 +x_5_4_0 +x_5_6_0 +x_5_7_0 +x_5_8_0 +x_5_9_0 +x_5_10_0 +x_5_11_0 +x_5_12_0 -y_5_0 = 0; r35: +x_5_0_1 +x_5_1_1 +x_5_2_1 +x_5_3_1 +x_5_4_1 +x_5_6_1 +x_5_7_1 +x_5_8_1 +x_5_9_1 +x_5_10_1 +x_5_11_1 +x_5_12_1 -y_5_1 = 0; r36: +x_5_0_2 +x_5_1_2 +x_5_2_2 +x_5_3_2 +x_5_4_2 +x_5_6_2 +x_5_7_2 +x_5_8_2 +x_5_9_2 +x_5_10_2 +x_5_11_2 +x_5_12_2 -y_5_2 = 0; r37: +x_5_0_3 +x_5_1_3 +x_5_2_3 +x_5_3_3 +x_5_4_3 +x_5_6_3 +x_5_7_3 +x_5_8_3 +x_5_9_3 +x_5_10_3 +x_5_11_3 +x_5_12_3 -y_5_3 = 0; r38: +x_6_0_0 +x_6_1_0 +x_6_2_0 +x_6_3_0 +x_6_4_0 +x_6_5_0 +x_6_7_0 +x_6_8_0 +x_6_9_0 +x_6_10_0 +x_6_11_0 +x_6_12_0 -y_6_0 = 0; r39: +x_6_0_1 +x_6_1_1 +x_6_2_1 +x_6_3_1 +x_6_4_1 +x_6_5_1 +x_6_7_1 +x_6_8_1 +x_6_9_1 +x_6_10_1 +x_6_11_1 +x_6_12_1 -y_6_1 = 0; r40: +x_6_0_2 +x_6_1_2 +x_6_2_2 +x_6_3_2 +x_6_4_2 +x_6_5_2 +x_6_7_2 +x_6_8_2 +x_6_9_2 +x_6_10_2 +x_6_11_2 +x_6_12_2 -y_6_2 = 0; r41: +x_6_0_3 +x_6_1_3 +x_6_2_3 +x_6_3_3 +x_6_4_3 +x_6_5_3 +x_6_7_3 +x_6_8_3 +x_6_9_3 +x_6_10_3 +x_6_11_3 +x_6_12_3 -y_6_3 = 0; r42: +x_7_0_0 +x_7_1_0 +x_7_2_0 +x_7_3_0 +x_7_4_0 +x_7_5_0 +x_7_6_0 +x_7_8_0 +x_7_9_0 +x_7_10_0 +x_7_11_0 +x_7_12_0 -y_7_0 = 0; r43: +x_7_0_1 +x_7_1_1 +x_7_2_1 +x_7_3_1 +x_7_4_1 +x_7_5_1 +x_7_6_1 +x_7_8_1 +x_7_9_1 +x_7_10_1 +x_7_11_1 +x_7_12_1 -y_7_1 = 0; r44: +x_7_0_2 +x_7_1_2 +x_7_2_2 +x_7_3_2 +x_7_4_2 +x_7_5_2 +x_7_6_2 +x_7_8_2 +x_7_9_2 +x_7_10_2 +x_7_11_2 +x_7_12_2 -y_7_2 = 0; r45: +x_7_0_3 +x_7_1_3 +x_7_2_3 +x_7_3_3 +x_7_4_3 +x_7_5_3 +x_7_6_3 +x_7_8_3 +x_7_9_3 +x_7_10_3 +x_7_11_3 +x_7_12_3 -y_7_3 = 0; r46: +x_8_0_0 +x_8_1_0 +x_8_2_0 +x_8_3_0 +x_8_4_0 +x_8_5_0 +x_8_6_0 +x_8_7_0 +x_8_9_0 +x_8_10_0 +x_8_11_0 +x_8_12_0 -y_8_0 = 0; r47: +x_8_0_1 +x_8_1_1 +x_8_2_1 +x_8_3_1 +x_8_4_1 +x_8_5_1 +x_8_6_1 +x_8_7_1 +x_8_9_1 +x_8_10_1 +x_8_11_1 +x_8_12_1 -y_8_1 = 0; r48: +x_8_0_2 +x_8_1_2 +x_8_2_2 +x_8_3_2 +x_8_4_2 +x_8_5_2 +x_8_6_2 +x_8_7_2 +x_8_9_2 +x_8_10_2 +x_8_11_2 +x_8_12_2 -y_8_2 = 0; r49: +x_8_0_3 +x_8_1_3 +x_8_2_3 +x_8_3_3 +x_8_4_3 +x_8_5_3 +x_8_6_3 +x_8_7_3 +x_8_9_3 +x_8_10_3 +x_8_11_3 +x_8_12_3 -y_8_3 = 0; r50: +x_9_0_0 +x_9_1_0 +x_9_2_0 +x_9_3_0 +x_9_4_0 +x_9_5_0 +x_9_6_0 +x_9_7_0 +x_9_8_0 +x_9_10_0 +x_9_11_0 +x_9_12_0 -y_9_0 = 0; r51: +x_9_0_1 +x_9_1_1 +x_9_2_1 +x_9_3_1 +x_9_4_1 +x_9_5_1 +x_9_6_1 +x_9_7_1 +x_9_8_1 +x_9_10_1 +x_9_11_1 +x_9_12_1 -y_9_1 = 0; r52: +x_9_0_2 +x_9_1_2 +x_9_2_2 +x_9_3_2 +x_9_4_2 +x_9_5_2 +x_9_6_2 +x_9_7_2 +x_9_8_2 +x_9_10_2 +x_9_11_2 +x_9_12_2 -y_9_2 = 0; r53: +x_9_0_3 +x_9_1_3 +x_9_2_3 +x_9_3_3 +x_9_4_3 +x_9_5_3 +x_9_6_3 +x_9_7_3 +x_9_8_3 +x_9_10_3 +x_9_11_3 +x_9_12_3 -y_9_3 = 0; r54: +x_10_0_0 +x_10_1_0 +x_10_2_0 +x_10_3_0 +x_10_4_0 +x_10_5_0 +x_10_6_0 +x_10_7_0 +x_10_8_0 +x_10_9_0 +x_10_11_0 +x_10_12_0 -y_10_0 = 0; r55: +x_10_0_1 +x_10_1_1 +x_10_2_1 +x_10_3_1 +x_10_4_1 +x_10_5_1 +x_10_6_1 +x_10_7_1 +x_10_8_1 +x_10_9_1 +x_10_11_1 +x_10_12_1 -y_10_1 = 0; r56: +x_10_0_2 +x_10_1_2 +x_10_2_2 +x_10_3_2 +x_10_4_2 +x_10_5_2 +x_10_6_2 +x_10_7_2 +x_10_8_2 +x_10_9_2 +x_10_11_2 +x_10_12_2 -y_10_2 = 0; r57: +x_10_0_3 +x_10_1_3 +x_10_2_3 +x_10_3_3 +x_10_4_3 +x_10_5_3 +x_10_6_3 +x_10_7_3 +x_10_8_3 +x_10_9_3 +x_10_11_3 +x_10_12_3 -y_10_3 = 0; r58: +x_11_0_0 +x_11_1_0 +x_11_2_0 +x_11_3_0 +x_11_4_0 +x_11_5_0 +x_11_6_0 +x_11_7_0 +x_11_8_0 +x_11_9_0 +x_11_10_0 +x_11_12_0 -y_11_0 = 0; r59: +x_11_0_1 +x_11_1_1 +x_11_2_1 +x_11_3_1 +x_11_4_1 +x_11_5_1 +x_11_6_1 +x_11_7_1 +x_11_8_1 +x_11_9_1 +x_11_10_1 +x_11_12_1 -y_11_1 = 0; r60: +x_11_0_2 +x_11_1_2 +x_11_2_2 +x_11_3_2 +x_11_4_2 +x_11_5_2 +x_11_6_2 +x_11_7_2 +x_11_8_2 +x_11_9_2 +x_11_10_2 +x_11_12_2 -y_11_2 = 0; r61: +x_11_0_3 +x_11_1_3 +x_11_2_3 +x_11_3_3 +x_11_4_3 +x_11_5_3 +x_11_6_3 +x_11_7_3 +x_11_8_3 +x_11_9_3 +x_11_10_3 +x_11_12_3 -y_11_3 = 0; r62: +x_12_0_0 +x_12_1_0 +x_12_2_0 +x_12_3_0 +x_12_4_0 +x_12_5_0 +x_12_6_0 +x_12_7_0 +x_12_8_0 +x_12_9_0 +x_12_10_0 +x_12_11_0 -y_12_0 = 0; r63: +x_12_0_1 +x_12_1_1 +x_12_2_1 +x_12_3_1 +x_12_4_1 +x_12_5_1 +x_12_6_1 +x_12_7_1 +x_12_8_1 +x_12_9_1 +x_12_10_1 +x_12_11_1 -y_12_1 = 0; r64: +x_12_0_2 +x_12_1_2 +x_12_2_2 +x_12_3_2 +x_12_4_2 +x_12_5_2 +x_12_6_2 +x_12_7_2 +x_12_8_2 +x_12_9_2 +x_12_10_2 +x_12_11_2 -y_12_2 = 0; r65: +x_12_0_3 +x_12_1_3 +x_12_2_3 +x_12_3_3 +x_12_4_3 +x_12_5_3 +x_12_6_3 +x_12_7_3 +x_12_8_3 +x_12_9_3 +x_12_10_3 +x_12_11_3 -y_12_3 = 0; r66: +x_1_0_0 +x_2_0_0 +x_3_0_0 +x_4_0_0 +x_5_0_0 +x_6_0_0 +x_7_0_0 +x_8_0_0 +x_9_0_0 +x_10_0_0 +x_11_0_0 +x_12_0_0 -y_0_0 = 0; r67: +x_1_0_1 +x_2_0_1 +x_3_0_1 +x_4_0_1 +x_5_0_1 +x_6_0_1 +x_7_0_1 +x_8_0_1 +x_9_0_1 +x_10_0_1 +x_11_0_1 +x_12_0_1 -y_0_1 = 0; r68: +x_1_0_2 +x_2_0_2 +x_3_0_2 +x_4_0_2 +x_5_0_2 +x_6_0_2 +x_7_0_2 +x_8_0_2 +x_9_0_2 +x_10_0_2 +x_11_0_2 +x_12_0_2 -y_0_2 = 0; r69: +x_1_0_3 +x_2_0_3 +x_3_0_3 +x_4_0_3 +x_5_0_3 +x_6_0_3 +x_7_0_3 +x_8_0_3 +x_9_0_3 +x_10_0_3 +x_11_0_3 +x_12_0_3 -y_0_3 = 0; r70: +x_0_1_0 +x_2_1_0 +x_3_1_0 +x_4_1_0 +x_5_1_0 +x_6_1_0 +x_7_1_0 +x_8_1_0 +x_9_1_0 +x_10_1_0 +x_11_1_0 +x_12_1_0 -y_1_0 = 0; r71: +x_0_1_1 +x_2_1_1 +x_3_1_1 +x_4_1_1 +x_5_1_1 +x_6_1_1 +x_7_1_1 +x_8_1_1 +x_9_1_1 +x_10_1_1 +x_11_1_1 +x_12_1_1 -y_1_1 = 0; r72: +x_0_1_2 +x_2_1_2 +x_3_1_2 +x_4_1_2 +x_5_1_2 +x_6_1_2 +x_7_1_2 +x_8_1_2 +x_9_1_2 +x_10_1_2 +x_11_1_2 +x_12_1_2 -y_1_2 = 0; r73: +x_0_1_3 +x_2_1_3 +x_3_1_3 +x_4_1_3 +x_5_1_3 +x_6_1_3 +x_7_1_3 +x_8_1_3 +x_9_1_3 +x_10_1_3 +x_11_1_3 +x_12_1_3 -y_1_3 = 0; r74: +x_0_2_0 +x_1_2_0 +x_3_2_0 +x_4_2_0 +x_5_2_0 +x_6_2_0 +x_7_2_0 +x_8_2_0 +x_9_2_0 +x_10_2_0 +x_11_2_0 +x_12_2_0 -y_2_0 = 0; r75: +x_0_2_1 +x_1_2_1 +x_3_2_1 +x_4_2_1 +x_5_2_1 +x_6_2_1 +x_7_2_1 +x_8_2_1 +x_9_2_1 +x_10_2_1 +x_11_2_1 +x_12_2_1 -y_2_1 = 0; r76: +x_0_2_2 +x_1_2_2 +x_3_2_2 +x_4_2_2 +x_5_2_2 +x_6_2_2 +x_7_2_2 +x_8_2_2 +x_9_2_2 +x_10_2_2 +x_11_2_2 +x_12_2_2 -y_2_2 = 0; r77: +x_0_2_3 +x_1_2_3 +x_3_2_3 +x_4_2_3 +x_5_2_3 +x_6_2_3 +x_7_2_3 +x_8_2_3 +x_9_2_3 +x_10_2_3 +x_11_2_3 +x_12_2_3 -y_2_3 = 0; r78: +x_0_3_0 +x_1_3_0 +x_2_3_0 +x_4_3_0 +x_5_3_0 +x_6_3_0 +x_7_3_0 +x_8_3_0 +x_9_3_0 +x_10_3_0 +x_11_3_0 +x_12_3_0 -y_3_0 = 0; r79: +x_0_3_1 +x_1_3_1 +x_2_3_1 +x_4_3_1 +x_5_3_1 +x_6_3_1 +x_7_3_1 +x_8_3_1 +x_9_3_1 +x_10_3_1 +x_11_3_1 +x_12_3_1 -y_3_1 = 0; r80: +x_0_3_2 +x_1_3_2 +x_2_3_2 +x_4_3_2 +x_5_3_2 +x_6_3_2 +x_7_3_2 +x_8_3_2 +x_9_3_2 +x_10_3_2 +x_11_3_2 +x_12_3_2 -y_3_2 = 0; r81: +x_0_3_3 +x_1_3_3 +x_2_3_3 +x_4_3_3 +x_5_3_3 +x_6_3_3 +x_7_3_3 +x_8_3_3 +x_9_3_3 +x_10_3_3 +x_11_3_3 +x_12_3_3 -y_3_3 = 0; r82: +x_0_4_0 +x_1_4_0 +x_2_4_0 +x_3_4_0 +x_5_4_0 +x_6_4_0 +x_7_4_0 +x_8_4_0 +x_9_4_0 +x_10_4_0 +x_11_4_0 +x_12_4_0 -y_4_0 = 0; r83: +x_0_4_1 +x_1_4_1 +x_2_4_1 +x_3_4_1 +x_5_4_1 +x_6_4_1 +x_7_4_1 +x_8_4_1 +x_9_4_1 +x_10_4_1 +x_11_4_1 +x_12_4_1 -y_4_1 = 0; r84: +x_0_4_2 +x_1_4_2 +x_2_4_2 +x_3_4_2 +x_5_4_2 +x_6_4_2 +x_7_4_2 +x_8_4_2 +x_9_4_2 +x_10_4_2 +x_11_4_2 +x_12_4_2 -y_4_2 = 0; r85: +x_0_4_3 +x_1_4_3 +x_2_4_3 +x_3_4_3 +x_5_4_3 +x_6_4_3 +x_7_4_3 +x_8_4_3 +x_9_4_3 +x_10_4_3 +x_11_4_3 +x_12_4_3 -y_4_3 = 0; r86: +x_0_5_0 +x_1_5_0 +x_2_5_0 +x_3_5_0 +x_4_5_0 +x_6_5_0 +x_7_5_0 +x_8_5_0 +x_9_5_0 +x_10_5_0 +x_11_5_0 +x_12_5_0 -y_5_0 = 0; r87: +x_0_5_1 +x_1_5_1 +x_2_5_1 +x_3_5_1 +x_4_5_1 +x_6_5_1 +x_7_5_1 +x_8_5_1 +x_9_5_1 +x_10_5_1 +x_11_5_1 +x_12_5_1 -y_5_1 = 0; r88: +x_0_5_2 +x_1_5_2 +x_2_5_2 +x_3_5_2 +x_4_5_2 +x_6_5_2 +x_7_5_2 +x_8_5_2 +x_9_5_2 +x_10_5_2 +x_11_5_2 +x_12_5_2 -y_5_2 = 0; r89: +x_0_5_3 +x_1_5_3 +x_2_5_3 +x_3_5_3 +x_4_5_3 +x_6_5_3 +x_7_5_3 +x_8_5_3 +x_9_5_3 +x_10_5_3 +x_11_5_3 +x_12_5_3 -y_5_3 = 0; r90: +x_0_6_0 +x_1_6_0 +x_2_6_0 +x_3_6_0 +x_4_6_0 +x_5_6_0 +x_7_6_0 +x_8_6_0 +x_9_6_0 +x_10_6_0 +x_11_6_0 +x_12_6_0 -y_6_0 = 0; r91: +x_0_6_1 +x_1_6_1 +x_2_6_1 +x_3_6_1 +x_4_6_1 +x_5_6_1 +x_7_6_1 +x_8_6_1 +x_9_6_1 +x_10_6_1 +x_11_6_1 +x_12_6_1 -y_6_1 = 0; r92: +x_0_6_2 +x_1_6_2 +x_2_6_2 +x_3_6_2 +x_4_6_2 +x_5_6_2 +x_7_6_2 +x_8_6_2 +x_9_6_2 +x_10_6_2 +x_11_6_2 +x_12_6_2 -y_6_2 = 0; r93: +x_0_6_3 +x_1_6_3 +x_2_6_3 +x_3_6_3 +x_4_6_3 +x_5_6_3 +x_7_6_3 +x_8_6_3 +x_9_6_3 +x_10_6_3 +x_11_6_3 +x_12_6_3 -y_6_3 = 0; r94: +x_0_7_0 +x_1_7_0 +x_2_7_0 +x_3_7_0 +x_4_7_0 +x_5_7_0 +x_6_7_0 +x_8_7_0 +x_9_7_0 +x_10_7_0 +x_11_7_0 +x_12_7_0 -y_7_0 = 0; r95: +x_0_7_1 +x_1_7_1 +x_2_7_1 +x_3_7_1 +x_4_7_1 +x_5_7_1 +x_6_7_1 +x_8_7_1 +x_9_7_1 +x_10_7_1 +x_11_7_1 +x_12_7_1 -y_7_1 = 0; r96: +x_0_7_2 +x_1_7_2 +x_2_7_2 +x_3_7_2 +x_4_7_2 +x_5_7_2 +x_6_7_2 +x_8_7_2 +x_9_7_2 +x_10_7_2 +x_11_7_2 +x_12_7_2 -y_7_2 = 0; r97: +x_0_7_3 +x_1_7_3 +x_2_7_3 +x_3_7_3 +x_4_7_3 +x_5_7_3 +x_6_7_3 +x_8_7_3 +x_9_7_3 +x_10_7_3 +x_11_7_3 +x_12_7_3 -y_7_3 = 0; r98: +x_0_8_0 +x_1_8_0 +x_2_8_0 +x_3_8_0 +x_4_8_0 +x_5_8_0 +x_6_8_0 +x_7_8_0 +x_9_8_0 +x_10_8_0 +x_11_8_0 +x_12_8_0 -y_8_0 = 0; r99: +x_0_8_1 +x_1_8_1 +x_2_8_1 +x_3_8_1 +x_4_8_1 +x_5_8_1 +x_6_8_1 +x_7_8_1 +x_9_8_1 +x_10_8_1 +x_11_8_1 +x_12_8_1 -y_8_1 = 0; r100: +x_0_8_2 +x_1_8_2 +x_2_8_2 +x_3_8_2 +x_4_8_2 +x_5_8_2 +x_6_8_2 +x_7_8_2 +x_9_8_2 +x_10_8_2 +x_11_8_2 +x_12_8_2 -y_8_2 = 0; r101: +x_0_8_3 +x_1_8_3 +x_2_8_3 +x_3_8_3 +x_4_8_3 +x_5_8_3 +x_6_8_3 +x_7_8_3 +x_9_8_3 +x_10_8_3 +x_11_8_3 +x_12_8_3 -y_8_3 = 0; r102: +x_0_9_0 +x_1_9_0 +x_2_9_0 +x_3_9_0 +x_4_9_0 +x_5_9_0 +x_6_9_0 +x_7_9_0 +x_8_9_0 +x_10_9_0 +x_11_9_0 +x_12_9_0 -y_9_0 = 0; r103: +x_0_9_1 +x_1_9_1 +x_2_9_1 +x_3_9_1 +x_4_9_1 +x_5_9_1 +x_6_9_1 +x_7_9_1 +x_8_9_1 +x_10_9_1 +x_11_9_1 +x_12_9_1 -y_9_1 = 0; r104: +x_0_9_2 +x_1_9_2 +x_2_9_2 +x_3_9_2 +x_4_9_2 +x_5_9_2 +x_6_9_2 +x_7_9_2 +x_8_9_2 +x_10_9_2 +x_11_9_2 +x_12_9_2 -y_9_2 = 0; r105: +x_0_9_3 +x_1_9_3 +x_2_9_3 +x_3_9_3 +x_4_9_3 +x_5_9_3 +x_6_9_3 +x_7_9_3 +x_8_9_3 +x_10_9_3 +x_11_9_3 +x_12_9_3 -y_9_3 = 0; r106: +x_0_10_0 +x_1_10_0 +x_2_10_0 +x_3_10_0 +x_4_10_0 +x_5_10_0 +x_6_10_0 +x_7_10_0 +x_8_10_0 +x_9_10_0 +x_11_10_0 +x_12_10_0 -y_10_0 = 0; r107: +x_0_10_1 +x_1_10_1 +x_2_10_1 +x_3_10_1 +x_4_10_1 +x_5_10_1 +x_6_10_1 +x_7_10_1 +x_8_10_1 +x_9_10_1 +x_11_10_1 +x_12_10_1 -y_10_1 = 0; r108: +x_0_10_2 +x_1_10_2 +x_2_10_2 +x_3_10_2 +x_4_10_2 +x_5_10_2 +x_6_10_2 +x_7_10_2 +x_8_10_2 +x_9_10_2 +x_11_10_2 +x_12_10_2 -y_10_2 = 0; r109: +x_0_10_3 +x_1_10_3 +x_2_10_3 +x_3_10_3 +x_4_10_3 +x_5_10_3 +x_6_10_3 +x_7_10_3 +x_8_10_3 +x_9_10_3 +x_11_10_3 +x_12_10_3 -y_10_3 = 0; r110: +x_0_11_0 +x_1_11_0 +x_2_11_0 +x_3_11_0 +x_4_11_0 +x_5_11_0 +x_6_11_0 +x_7_11_0 +x_8_11_0 +x_9_11_0 +x_10_11_0 +x_12_11_0 -y_11_0 = 0; r111: +x_0_11_1 +x_1_11_1 +x_2_11_1 +x_3_11_1 +x_4_11_1 +x_5_11_1 +x_6_11_1 +x_7_11_1 +x_8_11_1 +x_9_11_1 +x_10_11_1 +x_12_11_1 -y_11_1 = 0; r112: +x_0_11_2 +x_1_11_2 +x_2_11_2 +x_3_11_2 +x_4_11_2 +x_5_11_2 +x_6_11_2 +x_7_11_2 +x_8_11_2 +x_9_11_2 +x_10_11_2 +x_12_11_2 -y_11_2 = 0; r113: +x_0_11_3 +x_1_11_3 +x_2_11_3 +x_3_11_3 +x_4_11_3 +x_5_11_3 +x_6_11_3 +x_7_11_3 +x_8_11_3 +x_9_11_3 +x_10_11_3 +x_12_11_3 -y_11_3 = 0; r114: +x_0_12_0 +x_1_12_0 +x_2_12_0 +x_3_12_0 +x_4_12_0 +x_5_12_0 +x_6_12_0 +x_7_12_0 +x_8_12_0 +x_9_12_0 +x_10_12_0 +x_11_12_0 -y_12_0 = 0; r115: +x_0_12_1 +x_1_12_1 +x_2_12_1 +x_3_12_1 +x_4_12_1 +x_5_12_1 +x_6_12_1 +x_7_12_1 +x_8_12_1 +x_9_12_1 +x_10_12_1 +x_11_12_1 -y_12_1 = 0; r116: +x_0_12_2 +x_1_12_2 +x_2_12_2 +x_3_12_2 +x_4_12_2 +x_5_12_2 +x_6_12_2 +x_7_12_2 +x_8_12_2 +x_9_12_2 +x_10_12_2 +x_11_12_2 -y_12_2 = 0; r117: +x_0_12_3 +x_1_12_3 +x_2_12_3 +x_3_12_3 +x_4_12_3 +x_5_12_3 +x_6_12_3 +x_7_12_3 +x_8_12_3 +x_9_12_3 +x_10_12_3 +x_11_12_3 -y_12_3 = 0; r118: +2 y_1_0 +5 y_2_0 +y_3_0 +4 y_4_0 +3 y_5_0 +10 y_6_0 +5 y_7_0 +3 y_8_0 +7 y_9_0 +6 y_10_0 +9 y_11_0 +9 y_12_0 <= 20; r119: +2 y_1_1 +5 y_2_1 +y_3_1 +4 y_4_1 +3 y_5_1 +10 y_6_1 +5 y_7_1 +3 y_8_1 +7 y_9_1 +6 y_10_1 +9 y_11_1 +9 y_12_1 <= 20; r120: +2 y_1_2 +5 y_2_2 +y_3_2 +4 y_4_2 +3 y_5_2 +10 y_6_2 +5 y_7_2 +3 y_8_2 +7 y_9_2 +6 y_10_2 +9 y_11_2 +9 y_12_2 <= 20; r121: +2 y_1_3 +5 y_2_3 +y_3_3 +4 y_4_3 +3 y_5_3 +10 y_6_3 +5 y_7_3 +3 y_8_3 +7 y_9_3 +6 y_10_3 +9 y_11_3 +9 y_12_3 <= 20; r122: +20 x_1_2_0 +u_1_0 -u_2_0 <= 15; r123: +u_1_0 <= 20; r124: +u_1_0 >= 2; r125: +u_2_0 <= 20; r126: +u_2_0 >= 5; r127: +20 x_1_2_1 +u_1_1 -u_2_1 <= 15; r128: +u_1_1 <= 20; r129: +u_1_1 >= 2; r130: +u_2_1 <= 20; r131: +u_2_1 >= 5; r132: +20 x_1_2_2 +u_1_2 -u_2_2 <= 15; r133: +u_1_2 <= 20; r134: +u_1_2 >= 2; r135: +u_2_2 <= 20; r136: +u_2_2 >= 5; r137: +20 x_1_2_3 +u_1_3 -u_2_3 <= 15; r138: +u_1_3 <= 20; r139: +u_1_3 >= 2; r140: +u_2_3 <= 20; r141: +u_2_3 >= 5; r142: +20 x_1_3_0 +u_1_0 -u_3_0 <= 19; r143: +u_1_0 <= 20; r144: +u_1_0 >= 2; r145: +u_3_0 <= 20; r146: +u_3_0 >= 1; r147: +20 x_1_3_1 +u_1_1 -u_3_1 <= 19; r148: +u_1_1 <= 20; r149: +u_1_1 >= 2; r150: +u_3_1 <= 20; r151: +u_3_1 >= 1; r152: +20 x_1_3_2 +u_1_2 -u_3_2 <= 19; r153: +u_1_2 <= 20; r154: +u_1_2 >= 2; r155: +u_3_2 <= 20; r156: +u_3_2 >= 1; r157: +20 x_1_3_3 +u_1_3 -u_3_3 <= 19; r158: +u_1_3 <= 20; r159: +u_1_3 >= 2; r160: +u_3_3 <= 20; r161: +u_3_3 >= 1; r162: +20 x_1_4_0 +u_1_0 -u_4_0 <= 16; r163: +u_1_0 <= 20; r164: +u_1_0 >= 2; r165: +u_4_0 <= 20; r166: +u_4_0 >= 4; r167: +20 x_1_4_1 +u_1_1 -u_4_1 <= 16; r168: +u_1_1 <= 20; r169: +u_1_1 >= 2; r170: +u_4_1 <= 20; r171: +u_4_1 >= 4; r172: +20 x_1_4_2 +u_1_2 -u_4_2 <= 16; r173: +u_1_2 <= 20; r174: +u_1_2 >= 2; r175: +u_4_2 <= 20; r176: +u_4_2 >= 4; r177: +20 x_1_4_3 +u_1_3 -u_4_3 <= 16; r178: +u_1_3 <= 20; r179: +u_1_3 >= 2; r180: +u_4_3 <= 20; r181: +u_4_3 >= 4; r182: +20 x_1_5_0 +u_1_0 -u_5_0 <= 17; r183: +u_1_0 <= 20; r184: +u_1_0 >= 2; r185: +u_5_0 <= 20; r186: +u_5_0 >= 3; r187: +20 x_1_5_1 +u_1_1 -u_5_1 <= 17; r188: +u_1_1 <= 20; r189: +u_1_1 >= 2; r190: +u_5_1 <= 20; r191: +u_5_1 >= 3; r192: +20 x_1_5_2 +u_1_2 -u_5_2 <= 17; r193: +u_1_2 <= 20; r194: +u_1_2 >= 2; r195: +u_5_2 <= 20; r196: +u_5_2 >= 3; r197: +20 x_1_5_3 +u_1_3 -u_5_3 <= 17; r198: +u_1_3 <= 20; r199: +u_1_3 >= 2; r200: +u_5_3 <= 20; r201: +u_5_3 >= 3; r202: +20 x_1_6_0 +u_1_0 -u_6_0 <= 10; r203: +u_1_0 <= 20; r204: +u_1_0 >= 2; r205: +u_6_0 <= 20; r206: +u_6_0 >= 10; r207: +20 x_1_6_1 +u_1_1 -u_6_1 <= 10; r208: +u_1_1 <= 20; r209: +u_1_1 >= 2; r210: +u_6_1 <= 20; r211: +u_6_1 >= 10; r212: +20 x_1_6_2 +u_1_2 -u_6_2 <= 10; r213: +u_1_2 <= 20; r214: +u_1_2 >= 2; r215: +u_6_2 <= 20; r216: +u_6_2 >= 10; r217: +20 x_1_6_3 +u_1_3 -u_6_3 <= 10; r218: +u_1_3 <= 20; r219: +u_1_3 >= 2; r220: +u_6_3 <= 20; r221: +u_6_3 >= 10; r222: +20 x_1_7_0 +u_1_0 -u_7_0 <= 15; r223: +u_1_0 <= 20; r224: +u_1_0 >= 2; r225: +u_7_0 <= 20; r226: +u_7_0 >= 5; r227: +20 x_1_7_1 +u_1_1 -u_7_1 <= 15; r228: +u_1_1 <= 20; r229: +u_1_1 >= 2; r230: +u_7_1 <= 20; r231: +u_7_1 >= 5; r232: +20 x_1_7_2 +u_1_2 -u_7_2 <= 15; r233: +u_1_2 <= 20; r234: +u_1_2 >= 2; r235: +u_7_2 <= 20; r236: +u_7_2 >= 5; r237: +20 x_1_7_3 +u_1_3 -u_7_3 <= 15; r238: +u_1_3 <= 20; r239: +u_1_3 >= 2; r240: +u_7_3 <= 20; r241: +u_7_3 >= 5; r242: +20 x_1_8_0 +u_1_0 -u_8_0 <= 17; r243: +u_1_0 <= 20; r244: +u_1_0 >= 2; r245: +u_8_0 <= 20; r246: +u_8_0 >= 3; r247: +20 x_1_8_1 +u_1_1 -u_8_1 <= 17; r248: +u_1_1 <= 20; r249: +u_1_1 >= 2; r250: +u_8_1 <= 20; r251: +u_8_1 >= 3; r252: +20 x_1_8_2 +u_1_2 -u_8_2 <= 17; r253: +u_1_2 <= 20; r254: +u_1_2 >= 2; r255: +u_8_2 <= 20; r256: +u_8_2 >= 3; r257: +20 x_1_8_3 +u_1_3 -u_8_3 <= 17; r258: +u_1_3 <= 20; r259: +u_1_3 >= 2; r260: +u_8_3 <= 20; r261: +u_8_3 >= 3; r262: +20 x_1_9_0 +u_1_0 -u_9_0 <= 13; r263: +u_1_0 <= 20; r264: +u_1_0 >= 2; r265: +u_9_0 <= 20; r266: +u_9_0 >= 7; r267: +20 x_1_9_1 +u_1_1 -u_9_1 <= 13; r268: +u_1_1 <= 20; r269: +u_1_1 >= 2; r270: +u_9_1 <= 20; r271: +u_9_1 >= 7; r272: +20 x_1_9_2 +u_1_2 -u_9_2 <= 13; r273: +u_1_2 <= 20; r274: +u_1_2 >= 2; r275: +u_9_2 <= 20; r276: +u_9_2 >= 7; r277: +20 x_1_9_3 +u_1_3 -u_9_3 <= 13; r278: +u_1_3 <= 20; r279: +u_1_3 >= 2; r280: +u_9_3 <= 20; r281: +u_9_3 >= 7; r282: +20 x_1_10_0 +u_1_0 -u_10_0 <= 14; r283: +u_1_0 <= 20; r284: +u_1_0 >= 2; r285: +u_10_0 <= 20; r286: +u_10_0 >= 6; r287: +20 x_1_10_1 +u_1_1 -u_10_1 <= 14; r288: +u_1_1 <= 20; r289: +u_1_1 >= 2; r290: +u_10_1 <= 20; r291: +u_10_1 >= 6; r292: +20 x_1_10_2 +u_1_2 -u_10_2 <= 14; r293: +u_1_2 <= 20; r294: +u_1_2 >= 2; r295: +u_10_2 <= 20; r296: +u_10_2 >= 6; r297: +20 x_1_10_3 +u_1_3 -u_10_3 <= 14; r298: +u_1_3 <= 20; r299: +u_1_3 >= 2; r300: +u_10_3 <= 20; r301: +u_10_3 >= 6; r302: +20 x_1_11_0 +u_1_0 -u_11_0 <= 11; r303: +u_1_0 <= 20; r304: +u_1_0 >= 2; r305: +u_11_0 <= 20; r306: +u_11_0 >= 9; r307: +20 x_1_11_1 +u_1_1 -u_11_1 <= 11; r308: +u_1_1 <= 20; r309: +u_1_1 >= 2; r310: +u_11_1 <= 20; r311: +u_11_1 >= 9; r312: +20 x_1_11_2 +u_1_2 -u_11_2 <= 11; r313: +u_1_2 <= 20; r314: +u_1_2 >= 2; r315: +u_11_2 <= 20; r316: +u_11_2 >= 9; r317: +20 x_1_11_3 +u_1_3 -u_11_3 <= 11; r318: +u_1_3 <= 20; r319: +u_1_3 >= 2; r320: +u_11_3 <= 20; r321: +u_11_3 >= 9; r322: +20 x_1_12_0 +u_1_0 -u_12_0 <= 11; r323: +u_1_0 <= 20; r324: +u_1_0 >= 2; r325: +u_12_0 <= 20; r326: +u_12_0 >= 9; r327: +20 x_1_12_1 +u_1_1 -u_12_1 <= 11; r328: +u_1_1 <= 20; r329: +u_1_1 >= 2; r330: +u_12_1 <= 20; r331: +u_12_1 >= 9; r332: +20 x_1_12_2 +u_1_2 -u_12_2 <= 11; r333: +u_1_2 <= 20; r334: +u_1_2 >= 2; r335: +u_12_2 <= 20; r336: +u_12_2 >= 9; r337: +20 x_1_12_3 +u_1_3 -u_12_3 <= 11; r338: +u_1_3 <= 20; r339: +u_1_3 >= 2; r340: +u_12_3 <= 20; r341: +u_12_3 >= 9; r342: +20 x_2_1_0 -u_1_0 +u_2_0 <= 18; r343: +u_2_0 <= 20; r344: +u_2_0 >= 5; r345: +u_1_0 <= 20; r346: +u_1_0 >= 2; r347: +20 x_2_1_1 -u_1_1 +u_2_1 <= 18; r348: +u_2_1 <= 20; r349: +u_2_1 >= 5; r350: +u_1_1 <= 20; r351: +u_1_1 >= 2; r352: +20 x_2_1_2 -u_1_2 +u_2_2 <= 18; r353: +u_2_2 <= 20; r354: +u_2_2 >= 5; r355: +u_1_2 <= 20; r356: +u_1_2 >= 2; r357: +20 x_2_1_3 -u_1_3 +u_2_3 <= 18; r358: +u_2_3 <= 20; r359: +u_2_3 >= 5; r360: +u_1_3 <= 20; r361: +u_1_3 >= 2; r362: +20 x_2_3_0 +u_2_0 -u_3_0 <= 19; r363: +u_2_0 <= 20; r364: +u_2_0 >= 5; r365: +u_3_0 <= 20; r366: +u_3_0 >= 1; r367: +20 x_2_3_1 +u_2_1 -u_3_1 <= 19; r368: +u_2_1 <= 20; r369: +u_2_1 >= 5; r370: +u_3_1 <= 20; r371: +u_3_1 >= 1; r372: +20 x_2_3_2 +u_2_2 -u_3_2 <= 19; r373: +u_2_2 <= 20; r374: +u_2_2 >= 5; r375: +u_3_2 <= 20; r376: +u_3_2 >= 1; r377: +20 x_2_3_3 +u_2_3 -u_3_3 <= 19; r378: +u_2_3 <= 20; r379: +u_2_3 >= 5; r380: +u_3_3 <= 20; r381: +u_3_3 >= 1; r382: +20 x_2_4_0 +u_2_0 -u_4_0 <= 16; r383: +u_2_0 <= 20; r384: +u_2_0 >= 5; r385: +u_4_0 <= 20; r386: +u_4_0 >= 4; r387: +20 x_2_4_1 +u_2_1 -u_4_1 <= 16; r388: +u_2_1 <= 20; r389: +u_2_1 >= 5; r390: +u_4_1 <= 20; r391: +u_4_1 >= 4; r392: +20 x_2_4_2 +u_2_2 -u_4_2 <= 16; r393: +u_2_2 <= 20; r394: +u_2_2 >= 5; r395: +u_4_2 <= 20; r396: +u_4_2 >= 4; r397: +20 x_2_4_3 +u_2_3 -u_4_3 <= 16; r398: +u_2_3 <= 20; r399: +u_2_3 >= 5; r400: +u_4_3 <= 20; r401: +u_4_3 >= 4; r402: +20 x_2_5_0 +u_2_0 -u_5_0 <= 17; r403: +u_2_0 <= 20; r404: +u_2_0 >= 5; r405: +u_5_0 <= 20; r406: +u_5_0 >= 3; r407: +20 x_2_5_1 +u_2_1 -u_5_1 <= 17; r408: +u_2_1 <= 20; r409: +u_2_1 >= 5; r410: +u_5_1 <= 20; r411: +u_5_1 >= 3; r412: +20 x_2_5_2 +u_2_2 -u_5_2 <= 17; r413: +u_2_2 <= 20; r414: +u_2_2 >= 5; r415: +u_5_2 <= 20; r416: +u_5_2 >= 3; r417: +20 x_2_5_3 +u_2_3 -u_5_3 <= 17; r418: +u_2_3 <= 20; r419: +u_2_3 >= 5; r420: +u_5_3 <= 20; r421: +u_5_3 >= 3; r422: +20 x_2_6_0 +u_2_0 -u_6_0 <= 10; r423: +u_2_0 <= 20; r424: +u_2_0 >= 5; r425: +u_6_0 <= 20; r426: +u_6_0 >= 10; r427: +20 x_2_6_1 +u_2_1 -u_6_1 <= 10; r428: +u_2_1 <= 20; r429: +u_2_1 >= 5; r430: +u_6_1 <= 20; r431: +u_6_1 >= 10; r432: +20 x_2_6_2 +u_2_2 -u_6_2 <= 10; r433: +u_2_2 <= 20; r434: +u_2_2 >= 5; r435: +u_6_2 <= 20; r436: +u_6_2 >= 10; r437: +20 x_2_6_3 +u_2_3 -u_6_3 <= 10; r438: +u_2_3 <= 20; r439: +u_2_3 >= 5; r440: +u_6_3 <= 20; r441: +u_6_3 >= 10; r442: +20 x_2_7_0 +u_2_0 -u_7_0 <= 15; r443: +u_2_0 <= 20; r444: +u_2_0 >= 5; r445: +u_7_0 <= 20; r446: +u_7_0 >= 5; r447: +20 x_2_7_1 +u_2_1 -u_7_1 <= 15; r448: +u_2_1 <= 20; r449: +u_2_1 >= 5; r450: +u_7_1 <= 20; r451: +u_7_1 >= 5; r452: +20 x_2_7_2 +u_2_2 -u_7_2 <= 15; r453: +u_2_2 <= 20; r454: +u_2_2 >= 5; r455: +u_7_2 <= 20; r456: +u_7_2 >= 5; r457: +20 x_2_7_3 +u_2_3 -u_7_3 <= 15; r458: +u_2_3 <= 20; r459: +u_2_3 >= 5; r460: +u_7_3 <= 20; r461: +u_7_3 >= 5; r462: +20 x_2_8_0 +u_2_0 -u_8_0 <= 17; r463: +u_2_0 <= 20; r464: +u_2_0 >= 5; r465: +u_8_0 <= 20; r466: +u_8_0 >= 3; r467: +20 x_2_8_1 +u_2_1 -u_8_1 <= 17; r468: +u_2_1 <= 20; r469: +u_2_1 >= 5; r470: +u_8_1 <= 20; r471: +u_8_1 >= 3; r472: +20 x_2_8_2 +u_2_2 -u_8_2 <= 17; r473: +u_2_2 <= 20; r474: +u_2_2 >= 5; r475: +u_8_2 <= 20; r476: +u_8_2 >= 3; r477: +20 x_2_8_3 +u_2_3 -u_8_3 <= 17; r478: +u_2_3 <= 20; r479: +u_2_3 >= 5; r480: +u_8_3 <= 20; r481: +u_8_3 >= 3; r482: +20 x_2_9_0 +u_2_0 -u_9_0 <= 13; r483: +u_2_0 <= 20; r484: +u_2_0 >= 5; r485: +u_9_0 <= 20; r486: +u_9_0 >= 7; r487: +20 x_2_9_1 +u_2_1 -u_9_1 <= 13; r488: +u_2_1 <= 20; r489: +u_2_1 >= 5; r490: +u_9_1 <= 20; r491: +u_9_1 >= 7; r492: +20 x_2_9_2 +u_2_2 -u_9_2 <= 13; r493: +u_2_2 <= 20; r494: +u_2_2 >= 5; r495: +u_9_2 <= 20; r496: +u_9_2 >= 7; r497: +20 x_2_9_3 +u_2_3 -u_9_3 <= 13; r498: +u_2_3 <= 20; r499: +u_2_3 >= 5; r500: +u_9_3 <= 20; r501: +u_9_3 >= 7; r502: +20 x_2_10_0 +u_2_0 -u_10_0 <= 14; r503: +u_2_0 <= 20; r504: +u_2_0 >= 5; r505: +u_10_0 <= 20; r506: +u_10_0 >= 6; r507: +20 x_2_10_1 +u_2_1 -u_10_1 <= 14; r508: +u_2_1 <= 20; r509: +u_2_1 >= 5; r510: +u_10_1 <= 20; r511: +u_10_1 >= 6; r512: +20 x_2_10_2 +u_2_2 -u_10_2 <= 14; r513: +u_2_2 <= 20; r514: +u_2_2 >= 5; r515: +u_10_2 <= 20; r516: +u_10_2 >= 6; r517: +20 x_2_10_3 +u_2_3 -u_10_3 <= 14; r518: +u_2_3 <= 20; r519: +u_2_3 >= 5; r520: +u_10_3 <= 20; r521: +u_10_3 >= 6; r522: +20 x_2_11_0 +u_2_0 -u_11_0 <= 11; r523: +u_2_0 <= 20; r524: +u_2_0 >= 5; r525: +u_11_0 <= 20; r526: +u_11_0 >= 9; r527: +20 x_2_11_1 +u_2_1 -u_11_1 <= 11; r528: +u_2_1 <= 20; r529: +u_2_1 >= 5; r530: +u_11_1 <= 20; r531: +u_11_1 >= 9; r532: +20 x_2_11_2 +u_2_2 -u_11_2 <= 11; r533: +u_2_2 <= 20; r534: +u_2_2 >= 5; r535: +u_11_2 <= 20; r536: +u_11_2 >= 9; r537: +20 x_2_11_3 +u_2_3 -u_11_3 <= 11; r538: +u_2_3 <= 20; r539: +u_2_3 >= 5; r540: +u_11_3 <= 20; r541: +u_11_3 >= 9; r542: +20 x_2_12_0 +u_2_0 -u_12_0 <= 11; r543: +u_2_0 <= 20; r544: +u_2_0 >= 5; r545: +u_12_0 <= 20; r546: +u_12_0 >= 9; r547: +20 x_2_12_1 +u_2_1 -u_12_1 <= 11; r548: +u_2_1 <= 20; r549: +u_2_1 >= 5; r550: +u_12_1 <= 20; r551: +u_12_1 >= 9; r552: +20 x_2_12_2 +u_2_2 -u_12_2 <= 11; r553: +u_2_2 <= 20; r554: +u_2_2 >= 5; r555: +u_12_2 <= 20; r556: +u_12_2 >= 9; r557: +20 x_2_12_3 +u_2_3 -u_12_3 <= 11; r558: +u_2_3 <= 20; r559: +u_2_3 >= 5; r560: +u_12_3 <= 20; r561: +u_12_3 >= 9; r562: +20 x_3_1_0 -u_1_0 +u_3_0 <= 18; r563: +u_3_0 <= 20; r564: +u_3_0 >= 1; r565: +u_1_0 <= 20; r566: +u_1_0 >= 2; r567: +20 x_3_1_1 -u_1_1 +u_3_1 <= 18; r568: +u_3_1 <= 20; r569: +u_3_1 >= 1; r570: +u_1_1 <= 20; r571: +u_1_1 >= 2; r572: +20 x_3_1_2 -u_1_2 +u_3_2 <= 18; r573: +u_3_2 <= 20; r574: +u_3_2 >= 1; r575: +u_1_2 <= 20; r576: +u_1_2 >= 2; r577: +20 x_3_1_3 -u_1_3 +u_3_3 <= 18; r578: +u_3_3 <= 20; r579: +u_3_3 >= 1; r580: +u_1_3 <= 20; r581: +u_1_3 >= 2; r582: +20 x_3_2_0 -u_2_0 +u_3_0 <= 15; r583: +u_3_0 <= 20; r584: +u_3_0 >= 1; r585: +u_2_0 <= 20; r586: +u_2_0 >= 5; r587: +20 x_3_2_1 -u_2_1 +u_3_1 <= 15; r588: +u_3_1 <= 20; r589: +u_3_1 >= 1; r590: +u_2_1 <= 20; r591: +u_2_1 >= 5; r592: +20 x_3_2_2 -u_2_2 +u_3_2 <= 15; r593: +u_3_2 <= 20; r594: +u_3_2 >= 1; r595: +u_2_2 <= 20; r596: +u_2_2 >= 5; r597: +20 x_3_2_3 -u_2_3 +u_3_3 <= 15; r598: +u_3_3 <= 20; r599: +u_3_3 >= 1; r600: +u_2_3 <= 20; r601: +u_2_3 >= 5; r602: +20 x_3_4_0 +u_3_0 -u_4_0 <= 16; r603: +u_3_0 <= 20; r604: +u_3_0 >= 1; r605: +u_4_0 <= 20; r606: +u_4_0 >= 4; r607: +20 x_3_4_1 +u_3_1 -u_4_1 <= 16; r608: +u_3_1 <= 20; r609: +u_3_1 >= 1; r610: +u_4_1 <= 20; r611: +u_4_1 >= 4; r612: +20 x_3_4_2 +u_3_2 -u_4_2 <= 16; r613: +u_3_2 <= 20; r614: +u_3_2 >= 1; r615: +u_4_2 <= 20; r616: +u_4_2 >= 4; r617: +20 x_3_4_3 +u_3_3 -u_4_3 <= 16; r618: +u_3_3 <= 20; r619: +u_3_3 >= 1; r620: +u_4_3 <= 20; r621: +u_4_3 >= 4; r622: +20 x_3_5_0 +u_3_0 -u_5_0 <= 17; r623: +u_3_0 <= 20; r624: +u_3_0 >= 1; r625: +u_5_0 <= 20; r626: +u_5_0 >= 3; r627: +20 x_3_5_1 +u_3_1 -u_5_1 <= 17; r628: +u_3_1 <= 20; r629: +u_3_1 >= 1; r630: +u_5_1 <= 20; r631: +u_5_1 >= 3; r632: +20 x_3_5_2 +u_3_2 -u_5_2 <= 17; r633: +u_3_2 <= 20; r634: +u_3_2 >= 1; r635: +u_5_2 <= 20; r636: +u_5_2 >= 3; r637: +20 x_3_5_3 +u_3_3 -u_5_3 <= 17; r638: +u_3_3 <= 20; r639: +u_3_3 >= 1; r640: +u_5_3 <= 20; r641: +u_5_3 >= 3; r642: +20 x_3_6_0 +u_3_0 -u_6_0 <= 10; r643: +u_3_0 <= 20; r644: +u_3_0 >= 1; r645: +u_6_0 <= 20; r646: +u_6_0 >= 10; r647: +20 x_3_6_1 +u_3_1 -u_6_1 <= 10; r648: +u_3_1 <= 20; r649: +u_3_1 >= 1; r650: +u_6_1 <= 20; r651: +u_6_1 >= 10; r652: +20 x_3_6_2 +u_3_2 -u_6_2 <= 10; r653: +u_3_2 <= 20; r654: +u_3_2 >= 1; r655: +u_6_2 <= 20; r656: +u_6_2 >= 10; r657: +20 x_3_6_3 +u_3_3 -u_6_3 <= 10; r658: +u_3_3 <= 20; r659: +u_3_3 >= 1; r660: +u_6_3 <= 20; r661: +u_6_3 >= 10; r662: +20 x_3_7_0 +u_3_0 -u_7_0 <= 15; r663: +u_3_0 <= 20; r664: +u_3_0 >= 1; r665: +u_7_0 <= 20; r666: +u_7_0 >= 5; r667: +20 x_3_7_1 +u_3_1 -u_7_1 <= 15; r668: +u_3_1 <= 20; r669: +u_3_1 >= 1; r670: +u_7_1 <= 20; r671: +u_7_1 >= 5; r672: +20 x_3_7_2 +u_3_2 -u_7_2 <= 15; r673: +u_3_2 <= 20; r674: +u_3_2 >= 1; r675: +u_7_2 <= 20; r676: +u_7_2 >= 5; r677: +20 x_3_7_3 +u_3_3 -u_7_3 <= 15; r678: +u_3_3 <= 20; r679: +u_3_3 >= 1; r680: +u_7_3 <= 20; r681: +u_7_3 >= 5; r682: +20 x_3_8_0 +u_3_0 -u_8_0 <= 17; r683: +u_3_0 <= 20; r684: +u_3_0 >= 1; r685: +u_8_0 <= 20; r686: +u_8_0 >= 3; r687: +20 x_3_8_1 +u_3_1 -u_8_1 <= 17; r688: +u_3_1 <= 20; r689: +u_3_1 >= 1; r690: +u_8_1 <= 20; r691: +u_8_1 >= 3; r692: +20 x_3_8_2 +u_3_2 -u_8_2 <= 17; r693: +u_3_2 <= 20; r694: +u_3_2 >= 1; r695: +u_8_2 <= 20; r696: +u_8_2 >= 3; r697: +20 x_3_8_3 +u_3_3 -u_8_3 <= 17; r698: +u_3_3 <= 20; r699: +u_3_3 >= 1; r700: +u_8_3 <= 20; r701: +u_8_3 >= 3; r702: +20 x_3_9_0 +u_3_0 -u_9_0 <= 13; r703: +u_3_0 <= 20; r704: +u_3_0 >= 1; r705: +u_9_0 <= 20; r706: +u_9_0 >= 7; r707: +20 x_3_9_1 +u_3_1 -u_9_1 <= 13; r708: +u_3_1 <= 20; r709: +u_3_1 >= 1; r710: +u_9_1 <= 20; r711: +u_9_1 >= 7; r712: +20 x_3_9_2 +u_3_2 -u_9_2 <= 13; r713: +u_3_2 <= 20; r714: +u_3_2 >= 1; r715: +u_9_2 <= 20; r716: +u_9_2 >= 7; r717: +20 x_3_9_3 +u_3_3 -u_9_3 <= 13; r718: +u_3_3 <= 20; r719: +u_3_3 >= 1; r720: +u_9_3 <= 20; r721: +u_9_3 >= 7; r722: +20 x_3_10_0 +u_3_0 -u_10_0 <= 14; r723: +u_3_0 <= 20; r724: +u_3_0 >= 1; r725: +u_10_0 <= 20; r726: +u_10_0 >= 6; r727: +20 x_3_10_1 +u_3_1 -u_10_1 <= 14; r728: +u_3_1 <= 20; r729: +u_3_1 >= 1; r730: +u_10_1 <= 20; r731: +u_10_1 >= 6; r732: +20 x_3_10_2 +u_3_2 -u_10_2 <= 14; r733: +u_3_2 <= 20; r734: +u_3_2 >= 1; r735: +u_10_2 <= 20; r736: +u_10_2 >= 6; r737: +20 x_3_10_3 +u_3_3 -u_10_3 <= 14; r738: +u_3_3 <= 20; r739: +u_3_3 >= 1; r740: +u_10_3 <= 20; r741: +u_10_3 >= 6; r742: +20 x_3_11_0 +u_3_0 -u_11_0 <= 11; r743: +u_3_0 <= 20; r744: +u_3_0 >= 1; r745: +u_11_0 <= 20; r746: +u_11_0 >= 9; r747: +20 x_3_11_1 +u_3_1 -u_11_1 <= 11; r748: +u_3_1 <= 20; r749: +u_3_1 >= 1; r750: +u_11_1 <= 20; r751: +u_11_1 >= 9; r752: +20 x_3_11_2 +u_3_2 -u_11_2 <= 11; r753: +u_3_2 <= 20; r754: +u_3_2 >= 1; r755: +u_11_2 <= 20; r756: +u_11_2 >= 9; r757: +20 x_3_11_3 +u_3_3 -u_11_3 <= 11; r758: +u_3_3 <= 20; r759: +u_3_3 >= 1; r760: +u_11_3 <= 20; r761: +u_11_3 >= 9; r762: +20 x_3_12_0 +u_3_0 -u_12_0 <= 11; r763: +u_3_0 <= 20; r764: +u_3_0 >= 1; r765: +u_12_0 <= 20; r766: +u_12_0 >= 9; r767: +20 x_3_12_1 +u_3_1 -u_12_1 <= 11; r768: +u_3_1 <= 20; r769: +u_3_1 >= 1; r770: +u_12_1 <= 20; r771: +u_12_1 >= 9; r772: +20 x_3_12_2 +u_3_2 -u_12_2 <= 11; r773: +u_3_2 <= 20; r774: +u_3_2 >= 1; r775: +u_12_2 <= 20; r776: +u_12_2 >= 9; r777: +20 x_3_12_3 +u_3_3 -u_12_3 <= 11; r778: +u_3_3 <= 20; r779: +u_3_3 >= 1; r780: +u_12_3 <= 20; r781: +u_12_3 >= 9; r782: +20 x_4_1_0 -u_1_0 +u_4_0 <= 18; r783: +u_4_0 <= 20; r784: +u_4_0 >= 4; r785: +u_1_0 <= 20; r786: +u_1_0 >= 2; r787: +20 x_4_1_1 -u_1_1 +u_4_1 <= 18; r788: +u_4_1 <= 20; r789: +u_4_1 >= 4; r790: +u_1_1 <= 20; r791: +u_1_1 >= 2; r792: +20 x_4_1_2 -u_1_2 +u_4_2 <= 18; r793: +u_4_2 <= 20; r794: +u_4_2 >= 4; r795: +u_1_2 <= 20; r796: +u_1_2 >= 2; r797: +20 x_4_1_3 -u_1_3 +u_4_3 <= 18; r798: +u_4_3 <= 20; r799: +u_4_3 >= 4; r800: +u_1_3 <= 20; r801: +u_1_3 >= 2; r802: +20 x_4_2_0 -u_2_0 +u_4_0 <= 15; r803: +u_4_0 <= 20; r804: +u_4_0 >= 4; r805: +u_2_0 <= 20; r806: +u_2_0 >= 5; r807: +20 x_4_2_1 -u_2_1 +u_4_1 <= 15; r808: +u_4_1 <= 20; r809: +u_4_1 >= 4; r810: +u_2_1 <= 20; r811: +u_2_1 >= 5; r812: +20 x_4_2_2 -u_2_2 +u_4_2 <= 15; r813: +u_4_2 <= 20; r814: +u_4_2 >= 4; r815: +u_2_2 <= 20; r816: +u_2_2 >= 5; r817: +20 x_4_2_3 -u_2_3 +u_4_3 <= 15; r818: +u_4_3 <= 20; r819: +u_4_3 >= 4; r820: +u_2_3 <= 20; r821: +u_2_3 >= 5; r822: +20 x_4_3_0 -u_3_0 +u_4_0 <= 19; r823: +u_4_0 <= 20; r824: +u_4_0 >= 4; r825: +u_3_0 <= 20; r826: +u_3_0 >= 1; r827: +20 x_4_3_1 -u_3_1 +u_4_1 <= 19; r828: +u_4_1 <= 20; r829: +u_4_1 >= 4; r830: +u_3_1 <= 20; r831: +u_3_1 >= 1; r832: +20 x_4_3_2 -u_3_2 +u_4_2 <= 19; r833: +u_4_2 <= 20; r834: +u_4_2 >= 4; r835: +u_3_2 <= 20; r836: +u_3_2 >= 1; r837: +20 x_4_3_3 -u_3_3 +u_4_3 <= 19; r838: +u_4_3 <= 20; r839: +u_4_3 >= 4; r840: +u_3_3 <= 20; r841: +u_3_3 >= 1; r842: +20 x_4_5_0 +u_4_0 -u_5_0 <= 17; r843: +u_4_0 <= 20; r844: +u_4_0 >= 4; r845: +u_5_0 <= 20; r846: +u_5_0 >= 3; r847: +20 x_4_5_1 +u_4_1 -u_5_1 <= 17; r848: +u_4_1 <= 20; r849: +u_4_1 >= 4; r850: +u_5_1 <= 20; r851: +u_5_1 >= 3; r852: +20 x_4_5_2 +u_4_2 -u_5_2 <= 17; r853: +u_4_2 <= 20; r854: +u_4_2 >= 4; r855: +u_5_2 <= 20; r856: +u_5_2 >= 3; r857: +20 x_4_5_3 +u_4_3 -u_5_3 <= 17; r858: +u_4_3 <= 20; r859: +u_4_3 >= 4; r860: +u_5_3 <= 20; r861: +u_5_3 >= 3; r862: +20 x_4_6_0 +u_4_0 -u_6_0 <= 10; r863: +u_4_0 <= 20; r864: +u_4_0 >= 4; r865: +u_6_0 <= 20; r866: +u_6_0 >= 10; r867: +20 x_4_6_1 +u_4_1 -u_6_1 <= 10; r868: +u_4_1 <= 20; r869: +u_4_1 >= 4; r870: +u_6_1 <= 20; r871: +u_6_1 >= 10; r872: +20 x_4_6_2 +u_4_2 -u_6_2 <= 10; r873: +u_4_2 <= 20; r874: +u_4_2 >= 4; r875: +u_6_2 <= 20; r876: +u_6_2 >= 10; r877: +20 x_4_6_3 +u_4_3 -u_6_3 <= 10; r878: +u_4_3 <= 20; r879: +u_4_3 >= 4; r880: +u_6_3 <= 20; r881: +u_6_3 >= 10; r882: +20 x_4_7_0 +u_4_0 -u_7_0 <= 15; r883: +u_4_0 <= 20; r884: +u_4_0 >= 4; r885: +u_7_0 <= 20; r886: +u_7_0 >= 5; r887: +20 x_4_7_1 +u_4_1 -u_7_1 <= 15; r888: +u_4_1 <= 20; r889: +u_4_1 >= 4; r890: +u_7_1 <= 20; r891: +u_7_1 >= 5; r892: +20 x_4_7_2 +u_4_2 -u_7_2 <= 15; r893: +u_4_2 <= 20; r894: +u_4_2 >= 4; r895: +u_7_2 <= 20; r896: +u_7_2 >= 5; r897: +20 x_4_7_3 +u_4_3 -u_7_3 <= 15; r898: +u_4_3 <= 20; r899: +u_4_3 >= 4; r900: +u_7_3 <= 20; r901: +u_7_3 >= 5; r902: +20 x_4_8_0 +u_4_0 -u_8_0 <= 17; r903: +u_4_0 <= 20; r904: +u_4_0 >= 4; r905: +u_8_0 <= 20; r906: +u_8_0 >= 3; r907: +20 x_4_8_1 +u_4_1 -u_8_1 <= 17; r908: +u_4_1 <= 20; r909: +u_4_1 >= 4; r910: +u_8_1 <= 20; r911: +u_8_1 >= 3; r912: +20 x_4_8_2 +u_4_2 -u_8_2 <= 17; r913: +u_4_2 <= 20; r914: +u_4_2 >= 4; r915: +u_8_2 <= 20; r916: +u_8_2 >= 3; r917: +20 x_4_8_3 +u_4_3 -u_8_3 <= 17; r918: +u_4_3 <= 20; r919: +u_4_3 >= 4; r920: +u_8_3 <= 20; r921: +u_8_3 >= 3; r922: +20 x_4_9_0 +u_4_0 -u_9_0 <= 13; r923: +u_4_0 <= 20; r924: +u_4_0 >= 4; r925: +u_9_0 <= 20; r926: +u_9_0 >= 7; r927: +20 x_4_9_1 +u_4_1 -u_9_1 <= 13; r928: +u_4_1 <= 20; r929: +u_4_1 >= 4; r930: +u_9_1 <= 20; r931: +u_9_1 >= 7; r932: +20 x_4_9_2 +u_4_2 -u_9_2 <= 13; r933: +u_4_2 <= 20; r934: +u_4_2 >= 4; r935: +u_9_2 <= 20; r936: +u_9_2 >= 7; r937: +20 x_4_9_3 +u_4_3 -u_9_3 <= 13; r938: +u_4_3 <= 20; r939: +u_4_3 >= 4; r940: +u_9_3 <= 20; r941: +u_9_3 >= 7; r942: +20 x_4_10_0 +u_4_0 -u_10_0 <= 14; r943: +u_4_0 <= 20; r944: +u_4_0 >= 4; r945: +u_10_0 <= 20; r946: +u_10_0 >= 6; r947: +20 x_4_10_1 +u_4_1 -u_10_1 <= 14; r948: +u_4_1 <= 20; r949: +u_4_1 >= 4; r950: +u_10_1 <= 20; r951: +u_10_1 >= 6; r952: +20 x_4_10_2 +u_4_2 -u_10_2 <= 14; r953: +u_4_2 <= 20; r954: +u_4_2 >= 4; r955: +u_10_2 <= 20; r956: +u_10_2 >= 6; r957: +20 x_4_10_3 +u_4_3 -u_10_3 <= 14; r958: +u_4_3 <= 20; r959: +u_4_3 >= 4; r960: +u_10_3 <= 20; r961: +u_10_3 >= 6; r962: +20 x_4_11_0 +u_4_0 -u_11_0 <= 11; r963: +u_4_0 <= 20; r964: +u_4_0 >= 4; r965: +u_11_0 <= 20; r966: +u_11_0 >= 9; r967: +20 x_4_11_1 +u_4_1 -u_11_1 <= 11; r968: +u_4_1 <= 20; r969: +u_4_1 >= 4; r970: +u_11_1 <= 20; r971: +u_11_1 >= 9; r972: +20 x_4_11_2 +u_4_2 -u_11_2 <= 11; r973: +u_4_2 <= 20; r974: +u_4_2 >= 4; r975: +u_11_2 <= 20; r976: +u_11_2 >= 9; r977: +20 x_4_11_3 +u_4_3 -u_11_3 <= 11; r978: +u_4_3 <= 20; r979: +u_4_3 >= 4; r980: +u_11_3 <= 20; r981: +u_11_3 >= 9; r982: +20 x_4_12_0 +u_4_0 -u_12_0 <= 11; r983: +u_4_0 <= 20; r984: +u_4_0 >= 4; r985: +u_12_0 <= 20; r986: +u_12_0 >= 9; r987: +20 x_4_12_1 +u_4_1 -u_12_1 <= 11; r988: +u_4_1 <= 20; r989: +u_4_1 >= 4; r990: +u_12_1 <= 20; r991: +u_12_1 >= 9; r992: +20 x_4_12_2 +u_4_2 -u_12_2 <= 11; r993: +u_4_2 <= 20; r994: +u_4_2 >= 4; r995: +u_12_2 <= 20; r996: +u_12_2 >= 9; r997: +20 x_4_12_3 +u_4_3 -u_12_3 <= 11; r998: +u_4_3 <= 20; r999: +u_4_3 >= 4; r1000: +u_12_3 <= 20; r1001: +u_12_3 >= 9; r1002: +20 x_5_1_0 -u_1_0 +u_5_0 <= 18; r1003: +u_5_0 <= 20; r1004: +u_5_0 >= 3; r1005: +u_1_0 <= 20; r1006: +u_1_0 >= 2; r1007: +20 x_5_1_1 -u_1_1 +u_5_1 <= 18; r1008: +u_5_1 <= 20; r1009: +u_5_1 >= 3; r1010: +u_1_1 <= 20; r1011: +u_1_1 >= 2; r1012: +20 x_5_1_2 -u_1_2 +u_5_2 <= 18; r1013: +u_5_2 <= 20; r1014: +u_5_2 >= 3; r1015: +u_1_2 <= 20; r1016: +u_1_2 >= 2; r1017: +20 x_5_1_3 -u_1_3 +u_5_3 <= 18; r1018: +u_5_3 <= 20; r1019: +u_5_3 >= 3; r1020: +u_1_3 <= 20; r1021: +u_1_3 >= 2; r1022: +20 x_5_2_0 -u_2_0 +u_5_0 <= 15; r1023: +u_5_0 <= 20; r1024: +u_5_0 >= 3; r1025: +u_2_0 <= 20; r1026: +u_2_0 >= 5; r1027: +20 x_5_2_1 -u_2_1 +u_5_1 <= 15; r1028: +u_5_1 <= 20; r1029: +u_5_1 >= 3; r1030: +u_2_1 <= 20; r1031: +u_2_1 >= 5; r1032: +20 x_5_2_2 -u_2_2 +u_5_2 <= 15; r1033: +u_5_2 <= 20; r1034: +u_5_2 >= 3; r1035: +u_2_2 <= 20; r1036: +u_2_2 >= 5; r1037: +20 x_5_2_3 -u_2_3 +u_5_3 <= 15; r1038: +u_5_3 <= 20; r1039: +u_5_3 >= 3; r1040: +u_2_3 <= 20; r1041: +u_2_3 >= 5; r1042: +20 x_5_3_0 -u_3_0 +u_5_0 <= 19; r1043: +u_5_0 <= 20; r1044: +u_5_0 >= 3; r1045: +u_3_0 <= 20; r1046: +u_3_0 >= 1; r1047: +20 x_5_3_1 -u_3_1 +u_5_1 <= 19; r1048: +u_5_1 <= 20; r1049: +u_5_1 >= 3; r1050: +u_3_1 <= 20; r1051: +u_3_1 >= 1; r1052: +20 x_5_3_2 -u_3_2 +u_5_2 <= 19; r1053: +u_5_2 <= 20; r1054: +u_5_2 >= 3; r1055: +u_3_2 <= 20; r1056: +u_3_2 >= 1; r1057: +20 x_5_3_3 -u_3_3 +u_5_3 <= 19; r1058: +u_5_3 <= 20; r1059: +u_5_3 >= 3; r1060: +u_3_3 <= 20; r1061: +u_3_3 >= 1; r1062: +20 x_5_4_0 -u_4_0 +u_5_0 <= 16; r1063: +u_5_0 <= 20; r1064: +u_5_0 >= 3; r1065: +u_4_0 <= 20; r1066: +u_4_0 >= 4; r1067: +20 x_5_4_1 -u_4_1 +u_5_1 <= 16; r1068: +u_5_1 <= 20; r1069: +u_5_1 >= 3; r1070: +u_4_1 <= 20; r1071: +u_4_1 >= 4; r1072: +20 x_5_4_2 -u_4_2 +u_5_2 <= 16; r1073: +u_5_2 <= 20; r1074: +u_5_2 >= 3; r1075: +u_4_2 <= 20; r1076: +u_4_2 >= 4; r1077: +20 x_5_4_3 -u_4_3 +u_5_3 <= 16; r1078: +u_5_3 <= 20; r1079: +u_5_3 >= 3; r1080: +u_4_3 <= 20; r1081: +u_4_3 >= 4; r1082: +20 x_5_6_0 +u_5_0 -u_6_0 <= 10; r1083: +u_5_0 <= 20; r1084: +u_5_0 >= 3; r1085: +u_6_0 <= 20; r1086: +u_6_0 >= 10; r1087: +20 x_5_6_1 +u_5_1 -u_6_1 <= 10; r1088: +u_5_1 <= 20; r1089: +u_5_1 >= 3; r1090: +u_6_1 <= 20; r1091: +u_6_1 >= 10; r1092: +20 x_5_6_2 +u_5_2 -u_6_2 <= 10; r1093: +u_5_2 <= 20; r1094: +u_5_2 >= 3; r1095: +u_6_2 <= 20; r1096: +u_6_2 >= 10; r1097: +20 x_5_6_3 +u_5_3 -u_6_3 <= 10; r1098: +u_5_3 <= 20; r1099: +u_5_3 >= 3; r1100: +u_6_3 <= 20; r1101: +u_6_3 >= 10; r1102: +20 x_5_7_0 +u_5_0 -u_7_0 <= 15; r1103: +u_5_0 <= 20; r1104: +u_5_0 >= 3; r1105: +u_7_0 <= 20; r1106: +u_7_0 >= 5; r1107: +20 x_5_7_1 +u_5_1 -u_7_1 <= 15; r1108: +u_5_1 <= 20; r1109: +u_5_1 >= 3; r1110: +u_7_1 <= 20; r1111: +u_7_1 >= 5; r1112: +20 x_5_7_2 +u_5_2 -u_7_2 <= 15; r1113: +u_5_2 <= 20; r1114: +u_5_2 >= 3; r1115: +u_7_2 <= 20; r1116: +u_7_2 >= 5; r1117: +20 x_5_7_3 +u_5_3 -u_7_3 <= 15; r1118: +u_5_3 <= 20; r1119: +u_5_3 >= 3; r1120: +u_7_3 <= 20; r1121: +u_7_3 >= 5; r1122: +20 x_5_8_0 +u_5_0 -u_8_0 <= 17; r1123: +u_5_0 <= 20; r1124: +u_5_0 >= 3; r1125: +u_8_0 <= 20; r1126: +u_8_0 >= 3; r1127: +20 x_5_8_1 +u_5_1 -u_8_1 <= 17; r1128: +u_5_1 <= 20; r1129: +u_5_1 >= 3; r1130: +u_8_1 <= 20; r1131: +u_8_1 >= 3; r1132: +20 x_5_8_2 +u_5_2 -u_8_2 <= 17; r1133: +u_5_2 <= 20; r1134: +u_5_2 >= 3; r1135: +u_8_2 <= 20; r1136: +u_8_2 >= 3; r1137: +20 x_5_8_3 +u_5_3 -u_8_3 <= 17; r1138: +u_5_3 <= 20; r1139: +u_5_3 >= 3; r1140: +u_8_3 <= 20; r1141: +u_8_3 >= 3; r1142: +20 x_5_9_0 +u_5_0 -u_9_0 <= 13; r1143: +u_5_0 <= 20; r1144: +u_5_0 >= 3; r1145: +u_9_0 <= 20; r1146: +u_9_0 >= 7; r1147: +20 x_5_9_1 +u_5_1 -u_9_1 <= 13; r1148: +u_5_1 <= 20; r1149: +u_5_1 >= 3; r1150: +u_9_1 <= 20; r1151: +u_9_1 >= 7; r1152: +20 x_5_9_2 +u_5_2 -u_9_2 <= 13; r1153: +u_5_2 <= 20; r1154: +u_5_2 >= 3; r1155: +u_9_2 <= 20; r1156: +u_9_2 >= 7; r1157: +20 x_5_9_3 +u_5_3 -u_9_3 <= 13; r1158: +u_5_3 <= 20; r1159: +u_5_3 >= 3; r1160: +u_9_3 <= 20; r1161: +u_9_3 >= 7; r1162: +20 x_5_10_0 +u_5_0 -u_10_0 <= 14; r1163: +u_5_0 <= 20; r1164: +u_5_0 >= 3; r1165: +u_10_0 <= 20; r1166: +u_10_0 >= 6; r1167: +20 x_5_10_1 +u_5_1 -u_10_1 <= 14; r1168: +u_5_1 <= 20; r1169: +u_5_1 >= 3; r1170: +u_10_1 <= 20; r1171: +u_10_1 >= 6; r1172: +20 x_5_10_2 +u_5_2 -u_10_2 <= 14; r1173: +u_5_2 <= 20; r1174: +u_5_2 >= 3; r1175: +u_10_2 <= 20; r1176: +u_10_2 >= 6; r1177: +20 x_5_10_3 +u_5_3 -u_10_3 <= 14; r1178: +u_5_3 <= 20; r1179: +u_5_3 >= 3; r1180: +u_10_3 <= 20; r1181: +u_10_3 >= 6; r1182: +20 x_5_11_0 +u_5_0 -u_11_0 <= 11; r1183: +u_5_0 <= 20; r1184: +u_5_0 >= 3; r1185: +u_11_0 <= 20; r1186: +u_11_0 >= 9; r1187: +20 x_5_11_1 +u_5_1 -u_11_1 <= 11; r1188: +u_5_1 <= 20; r1189: +u_5_1 >= 3; r1190: +u_11_1 <= 20; r1191: +u_11_1 >= 9; r1192: +20 x_5_11_2 +u_5_2 -u_11_2 <= 11; r1193: +u_5_2 <= 20; r1194: +u_5_2 >= 3; r1195: +u_11_2 <= 20; r1196: +u_11_2 >= 9; r1197: +20 x_5_11_3 +u_5_3 -u_11_3 <= 11; r1198: +u_5_3 <= 20; r1199: +u_5_3 >= 3; r1200: +u_11_3 <= 20; r1201: +u_11_3 >= 9; r1202: +20 x_5_12_0 +u_5_0 -u_12_0 <= 11; r1203: +u_5_0 <= 20; r1204: +u_5_0 >= 3; r1205: +u_12_0 <= 20; r1206: +u_12_0 >= 9; r1207: +20 x_5_12_1 +u_5_1 -u_12_1 <= 11; r1208: +u_5_1 <= 20; r1209: +u_5_1 >= 3; r1210: +u_12_1 <= 20; r1211: +u_12_1 >= 9; r1212: +20 x_5_12_2 +u_5_2 -u_12_2 <= 11; r1213: +u_5_2 <= 20; r1214: +u_5_2 >= 3; r1215: +u_12_2 <= 20; r1216: +u_12_2 >= 9; r1217: +20 x_5_12_3 +u_5_3 -u_12_3 <= 11; r1218: +u_5_3 <= 20; r1219: +u_5_3 >= 3; r1220: +u_12_3 <= 20; r1221: +u_12_3 >= 9; r1222: +20 x_6_1_0 -u_1_0 +u_6_0 <= 18; r1223: +u_6_0 <= 20; r1224: +u_6_0 >= 10; r1225: +u_1_0 <= 20; r1226: +u_1_0 >= 2; r1227: +20 x_6_1_1 -u_1_1 +u_6_1 <= 18; r1228: +u_6_1 <= 20; r1229: +u_6_1 >= 10; r1230: +u_1_1 <= 20; r1231: +u_1_1 >= 2; r1232: +20 x_6_1_2 -u_1_2 +u_6_2 <= 18; r1233: +u_6_2 <= 20; r1234: +u_6_2 >= 10; r1235: +u_1_2 <= 20; r1236: +u_1_2 >= 2; r1237: +20 x_6_1_3 -u_1_3 +u_6_3 <= 18; r1238: +u_6_3 <= 20; r1239: +u_6_3 >= 10; r1240: +u_1_3 <= 20; r1241: +u_1_3 >= 2; r1242: +20 x_6_2_0 -u_2_0 +u_6_0 <= 15; r1243: +u_6_0 <= 20; r1244: +u_6_0 >= 10; r1245: +u_2_0 <= 20; r1246: +u_2_0 >= 5; r1247: +20 x_6_2_1 -u_2_1 +u_6_1 <= 15; r1248: +u_6_1 <= 20; r1249: +u_6_1 >= 10; r1250: +u_2_1 <= 20; r1251: +u_2_1 >= 5; r1252: +20 x_6_2_2 -u_2_2 +u_6_2 <= 15; r1253: +u_6_2 <= 20; r1254: +u_6_2 >= 10; r1255: +u_2_2 <= 20; r1256: +u_2_2 >= 5; r1257: +20 x_6_2_3 -u_2_3 +u_6_3 <= 15; r1258: +u_6_3 <= 20; r1259: +u_6_3 >= 10; r1260: +u_2_3 <= 20; r1261: +u_2_3 >= 5; r1262: +20 x_6_3_0 -u_3_0 +u_6_0 <= 19; r1263: +u_6_0 <= 20; r1264: +u_6_0 >= 10; r1265: +u_3_0 <= 20; r1266: +u_3_0 >= 1; r1267: +20 x_6_3_1 -u_3_1 +u_6_1 <= 19; r1268: +u_6_1 <= 20; r1269: +u_6_1 >= 10; r1270: +u_3_1 <= 20; r1271: +u_3_1 >= 1; r1272: +20 x_6_3_2 -u_3_2 +u_6_2 <= 19; r1273: +u_6_2 <= 20; r1274: +u_6_2 >= 10; r1275: +u_3_2 <= 20; r1276: +u_3_2 >= 1; r1277: +20 x_6_3_3 -u_3_3 +u_6_3 <= 19; r1278: +u_6_3 <= 20; r1279: +u_6_3 >= 10; r1280: +u_3_3 <= 20; r1281: +u_3_3 >= 1; r1282: +20 x_6_4_0 -u_4_0 +u_6_0 <= 16; r1283: +u_6_0 <= 20; r1284: +u_6_0 >= 10; r1285: +u_4_0 <= 20; r1286: +u_4_0 >= 4; r1287: +20 x_6_4_1 -u_4_1 +u_6_1 <= 16; r1288: +u_6_1 <= 20; r1289: +u_6_1 >= 10; r1290: +u_4_1 <= 20; r1291: +u_4_1 >= 4; r1292: +20 x_6_4_2 -u_4_2 +u_6_2 <= 16; r1293: +u_6_2 <= 20; r1294: +u_6_2 >= 10; r1295: +u_4_2 <= 20; r1296: +u_4_2 >= 4; r1297: +20 x_6_4_3 -u_4_3 +u_6_3 <= 16; r1298: +u_6_3 <= 20; r1299: +u_6_3 >= 10; r1300: +u_4_3 <= 20; r1301: +u_4_3 >= 4; r1302: +20 x_6_5_0 -u_5_0 +u_6_0 <= 17; r1303: +u_6_0 <= 20; r1304: +u_6_0 >= 10; r1305: +u_5_0 <= 20; r1306: +u_5_0 >= 3; r1307: +20 x_6_5_1 -u_5_1 +u_6_1 <= 17; r1308: +u_6_1 <= 20; r1309: +u_6_1 >= 10; r1310: +u_5_1 <= 20; r1311: +u_5_1 >= 3; r1312: +20 x_6_5_2 -u_5_2 +u_6_2 <= 17; r1313: +u_6_2 <= 20; r1314: +u_6_2 >= 10; r1315: +u_5_2 <= 20; r1316: +u_5_2 >= 3; r1317: +20 x_6_5_3 -u_5_3 +u_6_3 <= 17; r1318: +u_6_3 <= 20; r1319: +u_6_3 >= 10; r1320: +u_5_3 <= 20; r1321: +u_5_3 >= 3; r1322: +20 x_6_7_0 +u_6_0 -u_7_0 <= 15; r1323: +u_6_0 <= 20; r1324: +u_6_0 >= 10; r1325: +u_7_0 <= 20; r1326: +u_7_0 >= 5; r1327: +20 x_6_7_1 +u_6_1 -u_7_1 <= 15; r1328: +u_6_1 <= 20; r1329: +u_6_1 >= 10; r1330: +u_7_1 <= 20; r1331: +u_7_1 >= 5; r1332: +20 x_6_7_2 +u_6_2 -u_7_2 <= 15; r1333: +u_6_2 <= 20; r1334: +u_6_2 >= 10; r1335: +u_7_2 <= 20; r1336: +u_7_2 >= 5; r1337: +20 x_6_7_3 +u_6_3 -u_7_3 <= 15; r1338: +u_6_3 <= 20; r1339: +u_6_3 >= 10; r1340: +u_7_3 <= 20; r1341: +u_7_3 >= 5; r1342: +20 x_6_8_0 +u_6_0 -u_8_0 <= 17; r1343: +u_6_0 <= 20; r1344: +u_6_0 >= 10; r1345: +u_8_0 <= 20; r1346: +u_8_0 >= 3; r1347: +20 x_6_8_1 +u_6_1 -u_8_1 <= 17; r1348: +u_6_1 <= 20; r1349: +u_6_1 >= 10; r1350: +u_8_1 <= 20; r1351: +u_8_1 >= 3; r1352: +20 x_6_8_2 +u_6_2 -u_8_2 <= 17; r1353: +u_6_2 <= 20; r1354: +u_6_2 >= 10; r1355: +u_8_2 <= 20; r1356: +u_8_2 >= 3; r1357: +20 x_6_8_3 +u_6_3 -u_8_3 <= 17; r1358: +u_6_3 <= 20; r1359: +u_6_3 >= 10; r1360: +u_8_3 <= 20; r1361: +u_8_3 >= 3; r1362: +20 x_6_9_0 +u_6_0 -u_9_0 <= 13; r1363: +u_6_0 <= 20; r1364: +u_6_0 >= 10; r1365: +u_9_0 <= 20; r1366: +u_9_0 >= 7; r1367: +20 x_6_9_1 +u_6_1 -u_9_1 <= 13; r1368: +u_6_1 <= 20; r1369: +u_6_1 >= 10; r1370: +u_9_1 <= 20; r1371: +u_9_1 >= 7; r1372: +20 x_6_9_2 +u_6_2 -u_9_2 <= 13; r1373: +u_6_2 <= 20; r1374: +u_6_2 >= 10; r1375: +u_9_2 <= 20; r1376: +u_9_2 >= 7; r1377: +20 x_6_9_3 +u_6_3 -u_9_3 <= 13; r1378: +u_6_3 <= 20; r1379: +u_6_3 >= 10; r1380: +u_9_3 <= 20; r1381: +u_9_3 >= 7; r1382: +20 x_6_10_0 +u_6_0 -u_10_0 <= 14; r1383: +u_6_0 <= 20; r1384: +u_6_0 >= 10; r1385: +u_10_0 <= 20; r1386: +u_10_0 >= 6; r1387: +20 x_6_10_1 +u_6_1 -u_10_1 <= 14; r1388: +u_6_1 <= 20; r1389: +u_6_1 >= 10; r1390: +u_10_1 <= 20; r1391: +u_10_1 >= 6; r1392: +20 x_6_10_2 +u_6_2 -u_10_2 <= 14; r1393: +u_6_2 <= 20; r1394: +u_6_2 >= 10; r1395: +u_10_2 <= 20; r1396: +u_10_2 >= 6; r1397: +20 x_6_10_3 +u_6_3 -u_10_3 <= 14; r1398: +u_6_3 <= 20; r1399: +u_6_3 >= 10; r1400: +u_10_3 <= 20; r1401: +u_10_3 >= 6; r1402: +20 x_6_11_0 +u_6_0 -u_11_0 <= 11; r1403: +u_6_0 <= 20; r1404: +u_6_0 >= 10; r1405: +u_11_0 <= 20; r1406: +u_11_0 >= 9; r1407: +20 x_6_11_1 +u_6_1 -u_11_1 <= 11; r1408: +u_6_1 <= 20; r1409: +u_6_1 >= 10; r1410: +u_11_1 <= 20; r1411: +u_11_1 >= 9; r1412: +20 x_6_11_2 +u_6_2 -u_11_2 <= 11; r1413: +u_6_2 <= 20; r1414: +u_6_2 >= 10; r1415: +u_11_2 <= 20; r1416: +u_11_2 >= 9; r1417: +20 x_6_11_3 +u_6_3 -u_11_3 <= 11; r1418: +u_6_3 <= 20; r1419: +u_6_3 >= 10; r1420: +u_11_3 <= 20; r1421: +u_11_3 >= 9; r1422: +20 x_6_12_0 +u_6_0 -u_12_0 <= 11; r1423: +u_6_0 <= 20; r1424: +u_6_0 >= 10; r1425: +u_12_0 <= 20; r1426: +u_12_0 >= 9; r1427: +20 x_6_12_1 +u_6_1 -u_12_1 <= 11; r1428: +u_6_1 <= 20; r1429: +u_6_1 >= 10; r1430: +u_12_1 <= 20; r1431: +u_12_1 >= 9; r1432: +20 x_6_12_2 +u_6_2 -u_12_2 <= 11; r1433: +u_6_2 <= 20; r1434: +u_6_2 >= 10; r1435: +u_12_2 <= 20; r1436: +u_12_2 >= 9; r1437: +20 x_6_12_3 +u_6_3 -u_12_3 <= 11; r1438: +u_6_3 <= 20; r1439: +u_6_3 >= 10; r1440: +u_12_3 <= 20; r1441: +u_12_3 >= 9; r1442: +20 x_7_1_0 -u_1_0 +u_7_0 <= 18; r1443: +u_7_0 <= 20; r1444: +u_7_0 >= 5; r1445: +u_1_0 <= 20; r1446: +u_1_0 >= 2; r1447: +20 x_7_1_1 -u_1_1 +u_7_1 <= 18; r1448: +u_7_1 <= 20; r1449: +u_7_1 >= 5; r1450: +u_1_1 <= 20; r1451: +u_1_1 >= 2; r1452: +20 x_7_1_2 -u_1_2 +u_7_2 <= 18; r1453: +u_7_2 <= 20; r1454: +u_7_2 >= 5; r1455: +u_1_2 <= 20; r1456: +u_1_2 >= 2; r1457: +20 x_7_1_3 -u_1_3 +u_7_3 <= 18; r1458: +u_7_3 <= 20; r1459: +u_7_3 >= 5; r1460: +u_1_3 <= 20; r1461: +u_1_3 >= 2; r1462: +20 x_7_2_0 -u_2_0 +u_7_0 <= 15; r1463: +u_7_0 <= 20; r1464: +u_7_0 >= 5; r1465: +u_2_0 <= 20; r1466: +u_2_0 >= 5; r1467: +20 x_7_2_1 -u_2_1 +u_7_1 <= 15; r1468: +u_7_1 <= 20; r1469: +u_7_1 >= 5; r1470: +u_2_1 <= 20; r1471: +u_2_1 >= 5; r1472: +20 x_7_2_2 -u_2_2 +u_7_2 <= 15; r1473: +u_7_2 <= 20; r1474: +u_7_2 >= 5; r1475: +u_2_2 <= 20; r1476: +u_2_2 >= 5; r1477: +20 x_7_2_3 -u_2_3 +u_7_3 <= 15; r1478: +u_7_3 <= 20; r1479: +u_7_3 >= 5; r1480: +u_2_3 <= 20; r1481: +u_2_3 >= 5; r1482: +20 x_7_3_0 -u_3_0 +u_7_0 <= 19; r1483: +u_7_0 <= 20; r1484: +u_7_0 >= 5; r1485: +u_3_0 <= 20; r1486: +u_3_0 >= 1; r1487: +20 x_7_3_1 -u_3_1 +u_7_1 <= 19; r1488: +u_7_1 <= 20; r1489: +u_7_1 >= 5; r1490: +u_3_1 <= 20; r1491: +u_3_1 >= 1; r1492: +20 x_7_3_2 -u_3_2 +u_7_2 <= 19; r1493: +u_7_2 <= 20; r1494: +u_7_2 >= 5; r1495: +u_3_2 <= 20; r1496: +u_3_2 >= 1; r1497: +20 x_7_3_3 -u_3_3 +u_7_3 <= 19; r1498: +u_7_3 <= 20; r1499: +u_7_3 >= 5; r1500: +u_3_3 <= 20; r1501: +u_3_3 >= 1; r1502: +20 x_7_4_0 -u_4_0 +u_7_0 <= 16; r1503: +u_7_0 <= 20; r1504: +u_7_0 >= 5; r1505: +u_4_0 <= 20; r1506: +u_4_0 >= 4; r1507: +20 x_7_4_1 -u_4_1 +u_7_1 <= 16; r1508: +u_7_1 <= 20; r1509: +u_7_1 >= 5; r1510: +u_4_1 <= 20; r1511: +u_4_1 >= 4; r1512: +20 x_7_4_2 -u_4_2 +u_7_2 <= 16; r1513: +u_7_2 <= 20; r1514: +u_7_2 >= 5; r1515: +u_4_2 <= 20; r1516: +u_4_2 >= 4; r1517: +20 x_7_4_3 -u_4_3 +u_7_3 <= 16; r1518: +u_7_3 <= 20; r1519: +u_7_3 >= 5; r1520: +u_4_3 <= 20; r1521: +u_4_3 >= 4; r1522: +20 x_7_5_0 -u_5_0 +u_7_0 <= 17; r1523: +u_7_0 <= 20; r1524: +u_7_0 >= 5; r1525: +u_5_0 <= 20; r1526: +u_5_0 >= 3; r1527: +20 x_7_5_1 -u_5_1 +u_7_1 <= 17; r1528: +u_7_1 <= 20; r1529: +u_7_1 >= 5; r1530: +u_5_1 <= 20; r1531: +u_5_1 >= 3; r1532: +20 x_7_5_2 -u_5_2 +u_7_2 <= 17; r1533: +u_7_2 <= 20; r1534: +u_7_2 >= 5; r1535: +u_5_2 <= 20; r1536: +u_5_2 >= 3; r1537: +20 x_7_5_3 -u_5_3 +u_7_3 <= 17; r1538: +u_7_3 <= 20; r1539: +u_7_3 >= 5; r1540: +u_5_3 <= 20; r1541: +u_5_3 >= 3; r1542: +20 x_7_6_0 -u_6_0 +u_7_0 <= 10; r1543: +u_7_0 <= 20; r1544: +u_7_0 >= 5; r1545: +u_6_0 <= 20; r1546: +u_6_0 >= 10; r1547: +20 x_7_6_1 -u_6_1 +u_7_1 <= 10; r1548: +u_7_1 <= 20; r1549: +u_7_1 >= 5; r1550: +u_6_1 <= 20; r1551: +u_6_1 >= 10; r1552: +20 x_7_6_2 -u_6_2 +u_7_2 <= 10; r1553: +u_7_2 <= 20; r1554: +u_7_2 >= 5; r1555: +u_6_2 <= 20; r1556: +u_6_2 >= 10; r1557: +20 x_7_6_3 -u_6_3 +u_7_3 <= 10; r1558: +u_7_3 <= 20; r1559: +u_7_3 >= 5; r1560: +u_6_3 <= 20; r1561: +u_6_3 >= 10; r1562: +20 x_7_8_0 +u_7_0 -u_8_0 <= 17; r1563: +u_7_0 <= 20; r1564: +u_7_0 >= 5; r1565: +u_8_0 <= 20; r1566: +u_8_0 >= 3; r1567: +20 x_7_8_1 +u_7_1 -u_8_1 <= 17; r1568: +u_7_1 <= 20; r1569: +u_7_1 >= 5; r1570: +u_8_1 <= 20; r1571: +u_8_1 >= 3; r1572: +20 x_7_8_2 +u_7_2 -u_8_2 <= 17; r1573: +u_7_2 <= 20; r1574: +u_7_2 >= 5; r1575: +u_8_2 <= 20; r1576: +u_8_2 >= 3; r1577: +20 x_7_8_3 +u_7_3 -u_8_3 <= 17; r1578: +u_7_3 <= 20; r1579: +u_7_3 >= 5; r1580: +u_8_3 <= 20; r1581: +u_8_3 >= 3; r1582: +20 x_7_9_0 +u_7_0 -u_9_0 <= 13; r1583: +u_7_0 <= 20; r1584: +u_7_0 >= 5; r1585: +u_9_0 <= 20; r1586: +u_9_0 >= 7; r1587: +20 x_7_9_1 +u_7_1 -u_9_1 <= 13; r1588: +u_7_1 <= 20; r1589: +u_7_1 >= 5; r1590: +u_9_1 <= 20; r1591: +u_9_1 >= 7; r1592: +20 x_7_9_2 +u_7_2 -u_9_2 <= 13; r1593: +u_7_2 <= 20; r1594: +u_7_2 >= 5; r1595: +u_9_2 <= 20; r1596: +u_9_2 >= 7; r1597: +20 x_7_9_3 +u_7_3 -u_9_3 <= 13; r1598: +u_7_3 <= 20; r1599: +u_7_3 >= 5; r1600: +u_9_3 <= 20; r1601: +u_9_3 >= 7; r1602: +20 x_7_10_0 +u_7_0 -u_10_0 <= 14; r1603: +u_7_0 <= 20; r1604: +u_7_0 >= 5; r1605: +u_10_0 <= 20; r1606: +u_10_0 >= 6; r1607: +20 x_7_10_1 +u_7_1 -u_10_1 <= 14; r1608: +u_7_1 <= 20; r1609: +u_7_1 >= 5; r1610: +u_10_1 <= 20; r1611: +u_10_1 >= 6; r1612: +20 x_7_10_2 +u_7_2 -u_10_2 <= 14; r1613: +u_7_2 <= 20; r1614: +u_7_2 >= 5; r1615: +u_10_2 <= 20; r1616: +u_10_2 >= 6; r1617: +20 x_7_10_3 +u_7_3 -u_10_3 <= 14; r1618: +u_7_3 <= 20; r1619: +u_7_3 >= 5; r1620: +u_10_3 <= 20; r1621: +u_10_3 >= 6; r1622: +20 x_7_11_0 +u_7_0 -u_11_0 <= 11; r1623: +u_7_0 <= 20; r1624: +u_7_0 >= 5; r1625: +u_11_0 <= 20; r1626: +u_11_0 >= 9; r1627: +20 x_7_11_1 +u_7_1 -u_11_1 <= 11; r1628: +u_7_1 <= 20; r1629: +u_7_1 >= 5; r1630: +u_11_1 <= 20; r1631: +u_11_1 >= 9; r1632: +20 x_7_11_2 +u_7_2 -u_11_2 <= 11; r1633: +u_7_2 <= 20; r1634: +u_7_2 >= 5; r1635: +u_11_2 <= 20; r1636: +u_11_2 >= 9; r1637: +20 x_7_11_3 +u_7_3 -u_11_3 <= 11; r1638: +u_7_3 <= 20; r1639: +u_7_3 >= 5; r1640: +u_11_3 <= 20; r1641: +u_11_3 >= 9; r1642: +20 x_7_12_0 +u_7_0 -u_12_0 <= 11; r1643: +u_7_0 <= 20; r1644: +u_7_0 >= 5; r1645: +u_12_0 <= 20; r1646: +u_12_0 >= 9; r1647: +20 x_7_12_1 +u_7_1 -u_12_1 <= 11; r1648: +u_7_1 <= 20; r1649: +u_7_1 >= 5; r1650: +u_12_1 <= 20; r1651: +u_12_1 >= 9; r1652: +20 x_7_12_2 +u_7_2 -u_12_2 <= 11; r1653: +u_7_2 <= 20; r1654: +u_7_2 >= 5; r1655: +u_12_2 <= 20; r1656: +u_12_2 >= 9; r1657: +20 x_7_12_3 +u_7_3 -u_12_3 <= 11; r1658: +u_7_3 <= 20; r1659: +u_7_3 >= 5; r1660: +u_12_3 <= 20; r1661: +u_12_3 >= 9; r1662: +20 x_8_1_0 -u_1_0 +u_8_0 <= 18; r1663: +u_8_0 <= 20; r1664: +u_8_0 >= 3; r1665: +u_1_0 <= 20; r1666: +u_1_0 >= 2; r1667: +20 x_8_1_1 -u_1_1 +u_8_1 <= 18; r1668: +u_8_1 <= 20; r1669: +u_8_1 >= 3; r1670: +u_1_1 <= 20; r1671: +u_1_1 >= 2; r1672: +20 x_8_1_2 -u_1_2 +u_8_2 <= 18; r1673: +u_8_2 <= 20; r1674: +u_8_2 >= 3; r1675: +u_1_2 <= 20; r1676: +u_1_2 >= 2; r1677: +20 x_8_1_3 -u_1_3 +u_8_3 <= 18; r1678: +u_8_3 <= 20; r1679: +u_8_3 >= 3; r1680: +u_1_3 <= 20; r1681: +u_1_3 >= 2; r1682: +20 x_8_2_0 -u_2_0 +u_8_0 <= 15; r1683: +u_8_0 <= 20; r1684: +u_8_0 >= 3; r1685: +u_2_0 <= 20; r1686: +u_2_0 >= 5; r1687: +20 x_8_2_1 -u_2_1 +u_8_1 <= 15; r1688: +u_8_1 <= 20; r1689: +u_8_1 >= 3; r1690: +u_2_1 <= 20; r1691: +u_2_1 >= 5; r1692: +20 x_8_2_2 -u_2_2 +u_8_2 <= 15; r1693: +u_8_2 <= 20; r1694: +u_8_2 >= 3; r1695: +u_2_2 <= 20; r1696: +u_2_2 >= 5; r1697: +20 x_8_2_3 -u_2_3 +u_8_3 <= 15; r1698: +u_8_3 <= 20; r1699: +u_8_3 >= 3; r1700: +u_2_3 <= 20; r1701: +u_2_3 >= 5; r1702: +20 x_8_3_0 -u_3_0 +u_8_0 <= 19; r1703: +u_8_0 <= 20; r1704: +u_8_0 >= 3; r1705: +u_3_0 <= 20; r1706: +u_3_0 >= 1; r1707: +20 x_8_3_1 -u_3_1 +u_8_1 <= 19; r1708: +u_8_1 <= 20; r1709: +u_8_1 >= 3; r1710: +u_3_1 <= 20; r1711: +u_3_1 >= 1; r1712: +20 x_8_3_2 -u_3_2 +u_8_2 <= 19; r1713: +u_8_2 <= 20; r1714: +u_8_2 >= 3; r1715: +u_3_2 <= 20; r1716: +u_3_2 >= 1; r1717: +20 x_8_3_3 -u_3_3 +u_8_3 <= 19; r1718: +u_8_3 <= 20; r1719: +u_8_3 >= 3; r1720: +u_3_3 <= 20; r1721: +u_3_3 >= 1; r1722: +20 x_8_4_0 -u_4_0 +u_8_0 <= 16; r1723: +u_8_0 <= 20; r1724: +u_8_0 >= 3; r1725: +u_4_0 <= 20; r1726: +u_4_0 >= 4; r1727: +20 x_8_4_1 -u_4_1 +u_8_1 <= 16; r1728: +u_8_1 <= 20; r1729: +u_8_1 >= 3; r1730: +u_4_1 <= 20; r1731: +u_4_1 >= 4; r1732: +20 x_8_4_2 -u_4_2 +u_8_2 <= 16; r1733: +u_8_2 <= 20; r1734: +u_8_2 >= 3; r1735: +u_4_2 <= 20; r1736: +u_4_2 >= 4; r1737: +20 x_8_4_3 -u_4_3 +u_8_3 <= 16; r1738: +u_8_3 <= 20; r1739: +u_8_3 >= 3; r1740: +u_4_3 <= 20; r1741: +u_4_3 >= 4; r1742: +20 x_8_5_0 -u_5_0 +u_8_0 <= 17; r1743: +u_8_0 <= 20; r1744: +u_8_0 >= 3; r1745: +u_5_0 <= 20; r1746: +u_5_0 >= 3; r1747: +20 x_8_5_1 -u_5_1 +u_8_1 <= 17; r1748: +u_8_1 <= 20; r1749: +u_8_1 >= 3; r1750: +u_5_1 <= 20; r1751: +u_5_1 >= 3; r1752: +20 x_8_5_2 -u_5_2 +u_8_2 <= 17; r1753: +u_8_2 <= 20; r1754: +u_8_2 >= 3; r1755: +u_5_2 <= 20; r1756: +u_5_2 >= 3; r1757: +20 x_8_5_3 -u_5_3 +u_8_3 <= 17; r1758: +u_8_3 <= 20; r1759: +u_8_3 >= 3; r1760: +u_5_3 <= 20; r1761: +u_5_3 >= 3; r1762: +20 x_8_6_0 -u_6_0 +u_8_0 <= 10; r1763: +u_8_0 <= 20; r1764: +u_8_0 >= 3; r1765: +u_6_0 <= 20; r1766: +u_6_0 >= 10; r1767: +20 x_8_6_1 -u_6_1 +u_8_1 <= 10; r1768: +u_8_1 <= 20; r1769: +u_8_1 >= 3; r1770: +u_6_1 <= 20; r1771: +u_6_1 >= 10; r1772: +20 x_8_6_2 -u_6_2 +u_8_2 <= 10; r1773: +u_8_2 <= 20; r1774: +u_8_2 >= 3; r1775: +u_6_2 <= 20; r1776: +u_6_2 >= 10; r1777: +20 x_8_6_3 -u_6_3 +u_8_3 <= 10; r1778: +u_8_3 <= 20; r1779: +u_8_3 >= 3; r1780: +u_6_3 <= 20; r1781: +u_6_3 >= 10; r1782: +20 x_8_7_0 -u_7_0 +u_8_0 <= 15; r1783: +u_8_0 <= 20; r1784: +u_8_0 >= 3; r1785: +u_7_0 <= 20; r1786: +u_7_0 >= 5; r1787: +20 x_8_7_1 -u_7_1 +u_8_1 <= 15; r1788: +u_8_1 <= 20; r1789: +u_8_1 >= 3; r1790: +u_7_1 <= 20; r1791: +u_7_1 >= 5; r1792: +20 x_8_7_2 -u_7_2 +u_8_2 <= 15; r1793: +u_8_2 <= 20; r1794: +u_8_2 >= 3; r1795: +u_7_2 <= 20; r1796: +u_7_2 >= 5; r1797: +20 x_8_7_3 -u_7_3 +u_8_3 <= 15; r1798: +u_8_3 <= 20; r1799: +u_8_3 >= 3; r1800: +u_7_3 <= 20; r1801: +u_7_3 >= 5; r1802: +20 x_8_9_0 +u_8_0 -u_9_0 <= 13; r1803: +u_8_0 <= 20; r1804: +u_8_0 >= 3; r1805: +u_9_0 <= 20; r1806: +u_9_0 >= 7; r1807: +20 x_8_9_1 +u_8_1 -u_9_1 <= 13; r1808: +u_8_1 <= 20; r1809: +u_8_1 >= 3; r1810: +u_9_1 <= 20; r1811: +u_9_1 >= 7; r1812: +20 x_8_9_2 +u_8_2 -u_9_2 <= 13; r1813: +u_8_2 <= 20; r1814: +u_8_2 >= 3; r1815: +u_9_2 <= 20; r1816: +u_9_2 >= 7; r1817: +20 x_8_9_3 +u_8_3 -u_9_3 <= 13; r1818: +u_8_3 <= 20; r1819: +u_8_3 >= 3; r1820: +u_9_3 <= 20; r1821: +u_9_3 >= 7; r1822: +20 x_8_10_0 +u_8_0 -u_10_0 <= 14; r1823: +u_8_0 <= 20; r1824: +u_8_0 >= 3; r1825: +u_10_0 <= 20; r1826: +u_10_0 >= 6; r1827: +20 x_8_10_1 +u_8_1 -u_10_1 <= 14; r1828: +u_8_1 <= 20; r1829: +u_8_1 >= 3; r1830: +u_10_1 <= 20; r1831: +u_10_1 >= 6; r1832: +20 x_8_10_2 +u_8_2 -u_10_2 <= 14; r1833: +u_8_2 <= 20; r1834: +u_8_2 >= 3; r1835: +u_10_2 <= 20; r1836: +u_10_2 >= 6; r1837: +20 x_8_10_3 +u_8_3 -u_10_3 <= 14; r1838: +u_8_3 <= 20; r1839: +u_8_3 >= 3; r1840: +u_10_3 <= 20; r1841: +u_10_3 >= 6; r1842: +20 x_8_11_0 +u_8_0 -u_11_0 <= 11; r1843: +u_8_0 <= 20; r1844: +u_8_0 >= 3; r1845: +u_11_0 <= 20; r1846: +u_11_0 >= 9; r1847: +20 x_8_11_1 +u_8_1 -u_11_1 <= 11; r1848: +u_8_1 <= 20; r1849: +u_8_1 >= 3; r1850: +u_11_1 <= 20; r1851: +u_11_1 >= 9; r1852: +20 x_8_11_2 +u_8_2 -u_11_2 <= 11; r1853: +u_8_2 <= 20; r1854: +u_8_2 >= 3; r1855: +u_11_2 <= 20; r1856: +u_11_2 >= 9; r1857: +20 x_8_11_3 +u_8_3 -u_11_3 <= 11; r1858: +u_8_3 <= 20; r1859: +u_8_3 >= 3; r1860: +u_11_3 <= 20; r1861: +u_11_3 >= 9; r1862: +20 x_8_12_0 +u_8_0 -u_12_0 <= 11; r1863: +u_8_0 <= 20; r1864: +u_8_0 >= 3; r1865: +u_12_0 <= 20; r1866: +u_12_0 >= 9; r1867: +20 x_8_12_1 +u_8_1 -u_12_1 <= 11; r1868: +u_8_1 <= 20; r1869: +u_8_1 >= 3; r1870: +u_12_1 <= 20; r1871: +u_12_1 >= 9; r1872: +20 x_8_12_2 +u_8_2 -u_12_2 <= 11; r1873: +u_8_2 <= 20; r1874: +u_8_2 >= 3; r1875: +u_12_2 <= 20; r1876: +u_12_2 >= 9; r1877: +20 x_8_12_3 +u_8_3 -u_12_3 <= 11; r1878: +u_8_3 <= 20; r1879: +u_8_3 >= 3; r1880: +u_12_3 <= 20; r1881: +u_12_3 >= 9; r1882: +20 x_9_1_0 -u_1_0 +u_9_0 <= 18; r1883: +u_9_0 <= 20; r1884: +u_9_0 >= 7; r1885: +u_1_0 <= 20; r1886: +u_1_0 >= 2; r1887: +20 x_9_1_1 -u_1_1 +u_9_1 <= 18; r1888: +u_9_1 <= 20; r1889: +u_9_1 >= 7; r1890: +u_1_1 <= 20; r1891: +u_1_1 >= 2; r1892: +20 x_9_1_2 -u_1_2 +u_9_2 <= 18; r1893: +u_9_2 <= 20; r1894: +u_9_2 >= 7; r1895: +u_1_2 <= 20; r1896: +u_1_2 >= 2; r1897: +20 x_9_1_3 -u_1_3 +u_9_3 <= 18; r1898: +u_9_3 <= 20; r1899: +u_9_3 >= 7; r1900: +u_1_3 <= 20; r1901: +u_1_3 >= 2; r1902: +20 x_9_2_0 -u_2_0 +u_9_0 <= 15; r1903: +u_9_0 <= 20; r1904: +u_9_0 >= 7; r1905: +u_2_0 <= 20; r1906: +u_2_0 >= 5; r1907: +20 x_9_2_1 -u_2_1 +u_9_1 <= 15; r1908: +u_9_1 <= 20; r1909: +u_9_1 >= 7; r1910: +u_2_1 <= 20; r1911: +u_2_1 >= 5; r1912: +20 x_9_2_2 -u_2_2 +u_9_2 <= 15; r1913: +u_9_2 <= 20; r1914: +u_9_2 >= 7; r1915: +u_2_2 <= 20; r1916: +u_2_2 >= 5; r1917: +20 x_9_2_3 -u_2_3 +u_9_3 <= 15; r1918: +u_9_3 <= 20; r1919: +u_9_3 >= 7; r1920: +u_2_3 <= 20; r1921: +u_2_3 >= 5; r1922: +20 x_9_3_0 -u_3_0 +u_9_0 <= 19; r1923: +u_9_0 <= 20; r1924: +u_9_0 >= 7; r1925: +u_3_0 <= 20; r1926: +u_3_0 >= 1; r1927: +20 x_9_3_1 -u_3_1 +u_9_1 <= 19; r1928: +u_9_1 <= 20; r1929: +u_9_1 >= 7; r1930: +u_3_1 <= 20; r1931: +u_3_1 >= 1; r1932: +20 x_9_3_2 -u_3_2 +u_9_2 <= 19; r1933: +u_9_2 <= 20; r1934: +u_9_2 >= 7; r1935: +u_3_2 <= 20; r1936: +u_3_2 >= 1; r1937: +20 x_9_3_3 -u_3_3 +u_9_3 <= 19; r1938: +u_9_3 <= 20; r1939: +u_9_3 >= 7; r1940: +u_3_3 <= 20; r1941: +u_3_3 >= 1; r1942: +20 x_9_4_0 -u_4_0 +u_9_0 <= 16; r1943: +u_9_0 <= 20; r1944: +u_9_0 >= 7; r1945: +u_4_0 <= 20; r1946: +u_4_0 >= 4; r1947: +20 x_9_4_1 -u_4_1 +u_9_1 <= 16; r1948: +u_9_1 <= 20; r1949: +u_9_1 >= 7; r1950: +u_4_1 <= 20; r1951: +u_4_1 >= 4; r1952: +20 x_9_4_2 -u_4_2 +u_9_2 <= 16; r1953: +u_9_2 <= 20; r1954: +u_9_2 >= 7; r1955: +u_4_2 <= 20; r1956: +u_4_2 >= 4; r1957: +20 x_9_4_3 -u_4_3 +u_9_3 <= 16; r1958: +u_9_3 <= 20; r1959: +u_9_3 >= 7; r1960: +u_4_3 <= 20; r1961: +u_4_3 >= 4; r1962: +20 x_9_5_0 -u_5_0 +u_9_0 <= 17; r1963: +u_9_0 <= 20; r1964: +u_9_0 >= 7; r1965: +u_5_0 <= 20; r1966: +u_5_0 >= 3; r1967: +20 x_9_5_1 -u_5_1 +u_9_1 <= 17; r1968: +u_9_1 <= 20; r1969: +u_9_1 >= 7; r1970: +u_5_1 <= 20; r1971: +u_5_1 >= 3; r1972: +20 x_9_5_2 -u_5_2 +u_9_2 <= 17; r1973: +u_9_2 <= 20; r1974: +u_9_2 >= 7; r1975: +u_5_2 <= 20; r1976: +u_5_2 >= 3; r1977: +20 x_9_5_3 -u_5_3 +u_9_3 <= 17; r1978: +u_9_3 <= 20; r1979: +u_9_3 >= 7; r1980: +u_5_3 <= 20; r1981: +u_5_3 >= 3; r1982: +20 x_9_6_0 -u_6_0 +u_9_0 <= 10; r1983: +u_9_0 <= 20; r1984: +u_9_0 >= 7; r1985: +u_6_0 <= 20; r1986: +u_6_0 >= 10; r1987: +20 x_9_6_1 -u_6_1 +u_9_1 <= 10; r1988: +u_9_1 <= 20; r1989: +u_9_1 >= 7; r1990: +u_6_1 <= 20; r1991: +u_6_1 >= 10; r1992: +20 x_9_6_2 -u_6_2 +u_9_2 <= 10; r1993: +u_9_2 <= 20; r1994: +u_9_2 >= 7; r1995: +u_6_2 <= 20; r1996: +u_6_2 >= 10; r1997: +20 x_9_6_3 -u_6_3 +u_9_3 <= 10; r1998: +u_9_3 <= 20; r1999: +u_9_3 >= 7; r2000: +u_6_3 <= 20; r2001: +u_6_3 >= 10; r2002: +20 x_9_7_0 -u_7_0 +u_9_0 <= 15; r2003: +u_9_0 <= 20; r2004: +u_9_0 >= 7; r2005: +u_7_0 <= 20; r2006: +u_7_0 >= 5; r2007: +20 x_9_7_1 -u_7_1 +u_9_1 <= 15; r2008: +u_9_1 <= 20; r2009: +u_9_1 >= 7; r2010: +u_7_1 <= 20; r2011: +u_7_1 >= 5; r2012: +20 x_9_7_2 -u_7_2 +u_9_2 <= 15; r2013: +u_9_2 <= 20; r2014: +u_9_2 >= 7; r2015: +u_7_2 <= 20; r2016: +u_7_2 >= 5; r2017: +20 x_9_7_3 -u_7_3 +u_9_3 <= 15; r2018: +u_9_3 <= 20; r2019: +u_9_3 >= 7; r2020: +u_7_3 <= 20; r2021: +u_7_3 >= 5; r2022: +20 x_9_8_0 -u_8_0 +u_9_0 <= 17; r2023: +u_9_0 <= 20; r2024: +u_9_0 >= 7; r2025: +u_8_0 <= 20; r2026: +u_8_0 >= 3; r2027: +20 x_9_8_1 -u_8_1 +u_9_1 <= 17; r2028: +u_9_1 <= 20; r2029: +u_9_1 >= 7; r2030: +u_8_1 <= 20; r2031: +u_8_1 >= 3; r2032: +20 x_9_8_2 -u_8_2 +u_9_2 <= 17; r2033: +u_9_2 <= 20; r2034: +u_9_2 >= 7; r2035: +u_8_2 <= 20; r2036: +u_8_2 >= 3; r2037: +20 x_9_8_3 -u_8_3 +u_9_3 <= 17; r2038: +u_9_3 <= 20; r2039: +u_9_3 >= 7; r2040: +u_8_3 <= 20; r2041: +u_8_3 >= 3; r2042: +20 x_9_10_0 +u_9_0 -u_10_0 <= 14; r2043: +u_9_0 <= 20; r2044: +u_9_0 >= 7; r2045: +u_10_0 <= 20; r2046: +u_10_0 >= 6; r2047: +20 x_9_10_1 +u_9_1 -u_10_1 <= 14; r2048: +u_9_1 <= 20; r2049: +u_9_1 >= 7; r2050: +u_10_1 <= 20; r2051: +u_10_1 >= 6; r2052: +20 x_9_10_2 +u_9_2 -u_10_2 <= 14; r2053: +u_9_2 <= 20; r2054: +u_9_2 >= 7; r2055: +u_10_2 <= 20; r2056: +u_10_2 >= 6; r2057: +20 x_9_10_3 +u_9_3 -u_10_3 <= 14; r2058: +u_9_3 <= 20; r2059: +u_9_3 >= 7; r2060: +u_10_3 <= 20; r2061: +u_10_3 >= 6; r2062: +20 x_9_11_0 +u_9_0 -u_11_0 <= 11; r2063: +u_9_0 <= 20; r2064: +u_9_0 >= 7; r2065: +u_11_0 <= 20; r2066: +u_11_0 >= 9; r2067: +20 x_9_11_1 +u_9_1 -u_11_1 <= 11; r2068: +u_9_1 <= 20; r2069: +u_9_1 >= 7; r2070: +u_11_1 <= 20; r2071: +u_11_1 >= 9; r2072: +20 x_9_11_2 +u_9_2 -u_11_2 <= 11; r2073: +u_9_2 <= 20; r2074: +u_9_2 >= 7; r2075: +u_11_2 <= 20; r2076: +u_11_2 >= 9; r2077: +20 x_9_11_3 +u_9_3 -u_11_3 <= 11; r2078: +u_9_3 <= 20; r2079: +u_9_3 >= 7; r2080: +u_11_3 <= 20; r2081: +u_11_3 >= 9; r2082: +20 x_9_12_0 +u_9_0 -u_12_0 <= 11; r2083: +u_9_0 <= 20; r2084: +u_9_0 >= 7; r2085: +u_12_0 <= 20; r2086: +u_12_0 >= 9; r2087: +20 x_9_12_1 +u_9_1 -u_12_1 <= 11; r2088: +u_9_1 <= 20; r2089: +u_9_1 >= 7; r2090: +u_12_1 <= 20; r2091: +u_12_1 >= 9; r2092: +20 x_9_12_2 +u_9_2 -u_12_2 <= 11; r2093: +u_9_2 <= 20; r2094: +u_9_2 >= 7; r2095: +u_12_2 <= 20; r2096: +u_12_2 >= 9; r2097: +20 x_9_12_3 +u_9_3 -u_12_3 <= 11; r2098: +u_9_3 <= 20; r2099: +u_9_3 >= 7; r2100: +u_12_3 <= 20; r2101: +u_12_3 >= 9; r2102: +20 x_10_1_0 -u_1_0 +u_10_0 <= 18; r2103: +u_10_0 <= 20; r2104: +u_10_0 >= 6; r2105: +u_1_0 <= 20; r2106: +u_1_0 >= 2; r2107: +20 x_10_1_1 -u_1_1 +u_10_1 <= 18; r2108: +u_10_1 <= 20; r2109: +u_10_1 >= 6; r2110: +u_1_1 <= 20; r2111: +u_1_1 >= 2; r2112: +20 x_10_1_2 -u_1_2 +u_10_2 <= 18; r2113: +u_10_2 <= 20; r2114: +u_10_2 >= 6; r2115: +u_1_2 <= 20; r2116: +u_1_2 >= 2; r2117: +20 x_10_1_3 -u_1_3 +u_10_3 <= 18; r2118: +u_10_3 <= 20; r2119: +u_10_3 >= 6; r2120: +u_1_3 <= 20; r2121: +u_1_3 >= 2; r2122: +20 x_10_2_0 -u_2_0 +u_10_0 <= 15; r2123: +u_10_0 <= 20; r2124: +u_10_0 >= 6; r2125: +u_2_0 <= 20; r2126: +u_2_0 >= 5; r2127: +20 x_10_2_1 -u_2_1 +u_10_1 <= 15; r2128: +u_10_1 <= 20; r2129: +u_10_1 >= 6; r2130: +u_2_1 <= 20; r2131: +u_2_1 >= 5; r2132: +20 x_10_2_2 -u_2_2 +u_10_2 <= 15; r2133: +u_10_2 <= 20; r2134: +u_10_2 >= 6; r2135: +u_2_2 <= 20; r2136: +u_2_2 >= 5; r2137: +20 x_10_2_3 -u_2_3 +u_10_3 <= 15; r2138: +u_10_3 <= 20; r2139: +u_10_3 >= 6; r2140: +u_2_3 <= 20; r2141: +u_2_3 >= 5; r2142: +20 x_10_3_0 -u_3_0 +u_10_0 <= 19; r2143: +u_10_0 <= 20; r2144: +u_10_0 >= 6; r2145: +u_3_0 <= 20; r2146: +u_3_0 >= 1; r2147: +20 x_10_3_1 -u_3_1 +u_10_1 <= 19; r2148: +u_10_1 <= 20; r2149: +u_10_1 >= 6; r2150: +u_3_1 <= 20; r2151: +u_3_1 >= 1; r2152: +20 x_10_3_2 -u_3_2 +u_10_2 <= 19; r2153: +u_10_2 <= 20; r2154: +u_10_2 >= 6; r2155: +u_3_2 <= 20; r2156: +u_3_2 >= 1; r2157: +20 x_10_3_3 -u_3_3 +u_10_3 <= 19; r2158: +u_10_3 <= 20; r2159: +u_10_3 >= 6; r2160: +u_3_3 <= 20; r2161: +u_3_3 >= 1; r2162: +20 x_10_4_0 -u_4_0 +u_10_0 <= 16; r2163: +u_10_0 <= 20; r2164: +u_10_0 >= 6; r2165: +u_4_0 <= 20; r2166: +u_4_0 >= 4; r2167: +20 x_10_4_1 -u_4_1 +u_10_1 <= 16; r2168: +u_10_1 <= 20; r2169: +u_10_1 >= 6; r2170: +u_4_1 <= 20; r2171: +u_4_1 >= 4; r2172: +20 x_10_4_2 -u_4_2 +u_10_2 <= 16; r2173: +u_10_2 <= 20; r2174: +u_10_2 >= 6; r2175: +u_4_2 <= 20; r2176: +u_4_2 >= 4; r2177: +20 x_10_4_3 -u_4_3 +u_10_3 <= 16; r2178: +u_10_3 <= 20; r2179: +u_10_3 >= 6; r2180: +u_4_3 <= 20; r2181: +u_4_3 >= 4; r2182: +20 x_10_5_0 -u_5_0 +u_10_0 <= 17; r2183: +u_10_0 <= 20; r2184: +u_10_0 >= 6; r2185: +u_5_0 <= 20; r2186: +u_5_0 >= 3; r2187: +20 x_10_5_1 -u_5_1 +u_10_1 <= 17; r2188: +u_10_1 <= 20; r2189: +u_10_1 >= 6; r2190: +u_5_1 <= 20; r2191: +u_5_1 >= 3; r2192: +20 x_10_5_2 -u_5_2 +u_10_2 <= 17; r2193: +u_10_2 <= 20; r2194: +u_10_2 >= 6; r2195: +u_5_2 <= 20; r2196: +u_5_2 >= 3; r2197: +20 x_10_5_3 -u_5_3 +u_10_3 <= 17; r2198: +u_10_3 <= 20; r2199: +u_10_3 >= 6; r2200: +u_5_3 <= 20; r2201: +u_5_3 >= 3; r2202: +20 x_10_6_0 -u_6_0 +u_10_0 <= 10; r2203: +u_10_0 <= 20; r2204: +u_10_0 >= 6; r2205: +u_6_0 <= 20; r2206: +u_6_0 >= 10; r2207: +20 x_10_6_1 -u_6_1 +u_10_1 <= 10; r2208: +u_10_1 <= 20; r2209: +u_10_1 >= 6; r2210: +u_6_1 <= 20; r2211: +u_6_1 >= 10; r2212: +20 x_10_6_2 -u_6_2 +u_10_2 <= 10; r2213: +u_10_2 <= 20; r2214: +u_10_2 >= 6; r2215: +u_6_2 <= 20; r2216: +u_6_2 >= 10; r2217: +20 x_10_6_3 -u_6_3 +u_10_3 <= 10; r2218: +u_10_3 <= 20; r2219: +u_10_3 >= 6; r2220: +u_6_3 <= 20; r2221: +u_6_3 >= 10; r2222: +20 x_10_7_0 -u_7_0 +u_10_0 <= 15; r2223: +u_10_0 <= 20; r2224: +u_10_0 >= 6; r2225: +u_7_0 <= 20; r2226: +u_7_0 >= 5; r2227: +20 x_10_7_1 -u_7_1 +u_10_1 <= 15; r2228: +u_10_1 <= 20; r2229: +u_10_1 >= 6; r2230: +u_7_1 <= 20; r2231: +u_7_1 >= 5; r2232: +20 x_10_7_2 -u_7_2 +u_10_2 <= 15; r2233: +u_10_2 <= 20; r2234: +u_10_2 >= 6; r2235: +u_7_2 <= 20; r2236: +u_7_2 >= 5; r2237: +20 x_10_7_3 -u_7_3 +u_10_3 <= 15; r2238: +u_10_3 <= 20; r2239: +u_10_3 >= 6; r2240: +u_7_3 <= 20; r2241: +u_7_3 >= 5; r2242: +20 x_10_8_0 -u_8_0 +u_10_0 <= 17; r2243: +u_10_0 <= 20; r2244: +u_10_0 >= 6; r2245: +u_8_0 <= 20; r2246: +u_8_0 >= 3; r2247: +20 x_10_8_1 -u_8_1 +u_10_1 <= 17; r2248: +u_10_1 <= 20; r2249: +u_10_1 >= 6; r2250: +u_8_1 <= 20; r2251: +u_8_1 >= 3; r2252: +20 x_10_8_2 -u_8_2 +u_10_2 <= 17; r2253: +u_10_2 <= 20; r2254: +u_10_2 >= 6; r2255: +u_8_2 <= 20; r2256: +u_8_2 >= 3; r2257: +20 x_10_8_3 -u_8_3 +u_10_3 <= 17; r2258: +u_10_3 <= 20; r2259: +u_10_3 >= 6; r2260: +u_8_3 <= 20; r2261: +u_8_3 >= 3; r2262: +20 x_10_9_0 -u_9_0 +u_10_0 <= 13; r2263: +u_10_0 <= 20; r2264: +u_10_0 >= 6; r2265: +u_9_0 <= 20; r2266: +u_9_0 >= 7; r2267: +20 x_10_9_1 -u_9_1 +u_10_1 <= 13; r2268: +u_10_1 <= 20; r2269: +u_10_1 >= 6; r2270: +u_9_1 <= 20; r2271: +u_9_1 >= 7; r2272: +20 x_10_9_2 -u_9_2 +u_10_2 <= 13; r2273: +u_10_2 <= 20; r2274: +u_10_2 >= 6; r2275: +u_9_2 <= 20; r2276: +u_9_2 >= 7; r2277: +20 x_10_9_3 -u_9_3 +u_10_3 <= 13; r2278: +u_10_3 <= 20; r2279: +u_10_3 >= 6; r2280: +u_9_3 <= 20; r2281: +u_9_3 >= 7; r2282: +20 x_10_11_0 +u_10_0 -u_11_0 <= 11; r2283: +u_10_0 <= 20; r2284: +u_10_0 >= 6; r2285: +u_11_0 <= 20; r2286: +u_11_0 >= 9; r2287: +20 x_10_11_1 +u_10_1 -u_11_1 <= 11; r2288: +u_10_1 <= 20; r2289: +u_10_1 >= 6; r2290: +u_11_1 <= 20; r2291: +u_11_1 >= 9; r2292: +20 x_10_11_2 +u_10_2 -u_11_2 <= 11; r2293: +u_10_2 <= 20; r2294: +u_10_2 >= 6; r2295: +u_11_2 <= 20; r2296: +u_11_2 >= 9; r2297: +20 x_10_11_3 +u_10_3 -u_11_3 <= 11; r2298: +u_10_3 <= 20; r2299: +u_10_3 >= 6; r2300: +u_11_3 <= 20; r2301: +u_11_3 >= 9; r2302: +20 x_10_12_0 +u_10_0 -u_12_0 <= 11; r2303: +u_10_0 <= 20; r2304: +u_10_0 >= 6; r2305: +u_12_0 <= 20; r2306: +u_12_0 >= 9; r2307: +20 x_10_12_1 +u_10_1 -u_12_1 <= 11; r2308: +u_10_1 <= 20; r2309: +u_10_1 >= 6; r2310: +u_12_1 <= 20; r2311: +u_12_1 >= 9; r2312: +20 x_10_12_2 +u_10_2 -u_12_2 <= 11; r2313: +u_10_2 <= 20; r2314: +u_10_2 >= 6; r2315: +u_12_2 <= 20; r2316: +u_12_2 >= 9; r2317: +20 x_10_12_3 +u_10_3 -u_12_3 <= 11; r2318: +u_10_3 <= 20; r2319: +u_10_3 >= 6; r2320: +u_12_3 <= 20; r2321: +u_12_3 >= 9; r2322: +20 x_11_1_0 -u_1_0 +u_11_0 <= 18; r2323: +u_11_0 <= 20; r2324: +u_11_0 >= 9; r2325: +u_1_0 <= 20; r2326: +u_1_0 >= 2; r2327: +20 x_11_1_1 -u_1_1 +u_11_1 <= 18; r2328: +u_11_1 <= 20; r2329: +u_11_1 >= 9; r2330: +u_1_1 <= 20; r2331: +u_1_1 >= 2; r2332: +20 x_11_1_2 -u_1_2 +u_11_2 <= 18; r2333: +u_11_2 <= 20; r2334: +u_11_2 >= 9; r2335: +u_1_2 <= 20; r2336: +u_1_2 >= 2; r2337: +20 x_11_1_3 -u_1_3 +u_11_3 <= 18; r2338: +u_11_3 <= 20; r2339: +u_11_3 >= 9; r2340: +u_1_3 <= 20; r2341: +u_1_3 >= 2; r2342: +20 x_11_2_0 -u_2_0 +u_11_0 <= 15; r2343: +u_11_0 <= 20; r2344: +u_11_0 >= 9; r2345: +u_2_0 <= 20; r2346: +u_2_0 >= 5; r2347: +20 x_11_2_1 -u_2_1 +u_11_1 <= 15; r2348: +u_11_1 <= 20; r2349: +u_11_1 >= 9; r2350: +u_2_1 <= 20; r2351: +u_2_1 >= 5; r2352: +20 x_11_2_2 -u_2_2 +u_11_2 <= 15; r2353: +u_11_2 <= 20; r2354: +u_11_2 >= 9; r2355: +u_2_2 <= 20; r2356: +u_2_2 >= 5; r2357: +20 x_11_2_3 -u_2_3 +u_11_3 <= 15; r2358: +u_11_3 <= 20; r2359: +u_11_3 >= 9; r2360: +u_2_3 <= 20; r2361: +u_2_3 >= 5; r2362: +20 x_11_3_0 -u_3_0 +u_11_0 <= 19; r2363: +u_11_0 <= 20; r2364: +u_11_0 >= 9; r2365: +u_3_0 <= 20; r2366: +u_3_0 >= 1; r2367: +20 x_11_3_1 -u_3_1 +u_11_1 <= 19; r2368: +u_11_1 <= 20; r2369: +u_11_1 >= 9; r2370: +u_3_1 <= 20; r2371: +u_3_1 >= 1; r2372: +20 x_11_3_2 -u_3_2 +u_11_2 <= 19; r2373: +u_11_2 <= 20; r2374: +u_11_2 >= 9; r2375: +u_3_2 <= 20; r2376: +u_3_2 >= 1; r2377: +20 x_11_3_3 -u_3_3 +u_11_3 <= 19; r2378: +u_11_3 <= 20; r2379: +u_11_3 >= 9; r2380: +u_3_3 <= 20; r2381: +u_3_3 >= 1; r2382: +20 x_11_4_0 -u_4_0 +u_11_0 <= 16; r2383: +u_11_0 <= 20; r2384: +u_11_0 >= 9; r2385: +u_4_0 <= 20; r2386: +u_4_0 >= 4; r2387: +20 x_11_4_1 -u_4_1 +u_11_1 <= 16; r2388: +u_11_1 <= 20; r2389: +u_11_1 >= 9; r2390: +u_4_1 <= 20; r2391: +u_4_1 >= 4; r2392: +20 x_11_4_2 -u_4_2 +u_11_2 <= 16; r2393: +u_11_2 <= 20; r2394: +u_11_2 >= 9; r2395: +u_4_2 <= 20; r2396: +u_4_2 >= 4; r2397: +20 x_11_4_3 -u_4_3 +u_11_3 <= 16; r2398: +u_11_3 <= 20; r2399: +u_11_3 >= 9; r2400: +u_4_3 <= 20; r2401: +u_4_3 >= 4; r2402: +20 x_11_5_0 -u_5_0 +u_11_0 <= 17; r2403: +u_11_0 <= 20; r2404: +u_11_0 >= 9; r2405: +u_5_0 <= 20; r2406: +u_5_0 >= 3; r2407: +20 x_11_5_1 -u_5_1 +u_11_1 <= 17; r2408: +u_11_1 <= 20; r2409: +u_11_1 >= 9; r2410: +u_5_1 <= 20; r2411: +u_5_1 >= 3; r2412: +20 x_11_5_2 -u_5_2 +u_11_2 <= 17; r2413: +u_11_2 <= 20; r2414: +u_11_2 >= 9; r2415: +u_5_2 <= 20; r2416: +u_5_2 >= 3; r2417: +20 x_11_5_3 -u_5_3 +u_11_3 <= 17; r2418: +u_11_3 <= 20; r2419: +u_11_3 >= 9; r2420: +u_5_3 <= 20; r2421: +u_5_3 >= 3; r2422: +20 x_11_6_0 -u_6_0 +u_11_0 <= 10; r2423: +u_11_0 <= 20; r2424: +u_11_0 >= 9; r2425: +u_6_0 <= 20; r2426: +u_6_0 >= 10; r2427: +20 x_11_6_1 -u_6_1 +u_11_1 <= 10; r2428: +u_11_1 <= 20; r2429: +u_11_1 >= 9; r2430: +u_6_1 <= 20; r2431: +u_6_1 >= 10; r2432: +20 x_11_6_2 -u_6_2 +u_11_2 <= 10; r2433: +u_11_2 <= 20; r2434: +u_11_2 >= 9; r2435: +u_6_2 <= 20; r2436: +u_6_2 >= 10; r2437: +20 x_11_6_3 -u_6_3 +u_11_3 <= 10; r2438: +u_11_3 <= 20; r2439: +u_11_3 >= 9; r2440: +u_6_3 <= 20; r2441: +u_6_3 >= 10; r2442: +20 x_11_7_0 -u_7_0 +u_11_0 <= 15; r2443: +u_11_0 <= 20; r2444: +u_11_0 >= 9; r2445: +u_7_0 <= 20; r2446: +u_7_0 >= 5; r2447: +20 x_11_7_1 -u_7_1 +u_11_1 <= 15; r2448: +u_11_1 <= 20; r2449: +u_11_1 >= 9; r2450: +u_7_1 <= 20; r2451: +u_7_1 >= 5; r2452: +20 x_11_7_2 -u_7_2 +u_11_2 <= 15; r2453: +u_11_2 <= 20; r2454: +u_11_2 >= 9; r2455: +u_7_2 <= 20; r2456: +u_7_2 >= 5; r2457: +20 x_11_7_3 -u_7_3 +u_11_3 <= 15; r2458: +u_11_3 <= 20; r2459: +u_11_3 >= 9; r2460: +u_7_3 <= 20; r2461: +u_7_3 >= 5; r2462: +20 x_11_8_0 -u_8_0 +u_11_0 <= 17; r2463: +u_11_0 <= 20; r2464: +u_11_0 >= 9; r2465: +u_8_0 <= 20; r2466: +u_8_0 >= 3; r2467: +20 x_11_8_1 -u_8_1 +u_11_1 <= 17; r2468: +u_11_1 <= 20; r2469: +u_11_1 >= 9; r2470: +u_8_1 <= 20; r2471: +u_8_1 >= 3; r2472: +20 x_11_8_2 -u_8_2 +u_11_2 <= 17; r2473: +u_11_2 <= 20; r2474: +u_11_2 >= 9; r2475: +u_8_2 <= 20; r2476: +u_8_2 >= 3; r2477: +20 x_11_8_3 -u_8_3 +u_11_3 <= 17; r2478: +u_11_3 <= 20; r2479: +u_11_3 >= 9; r2480: +u_8_3 <= 20; r2481: +u_8_3 >= 3; r2482: +20 x_11_9_0 -u_9_0 +u_11_0 <= 13; r2483: +u_11_0 <= 20; r2484: +u_11_0 >= 9; r2485: +u_9_0 <= 20; r2486: +u_9_0 >= 7; r2487: +20 x_11_9_1 -u_9_1 +u_11_1 <= 13; r2488: +u_11_1 <= 20; r2489: +u_11_1 >= 9; r2490: +u_9_1 <= 20; r2491: +u_9_1 >= 7; r2492: +20 x_11_9_2 -u_9_2 +u_11_2 <= 13; r2493: +u_11_2 <= 20; r2494: +u_11_2 >= 9; r2495: +u_9_2 <= 20; r2496: +u_9_2 >= 7; r2497: +20 x_11_9_3 -u_9_3 +u_11_3 <= 13; r2498: +u_11_3 <= 20; r2499: +u_11_3 >= 9; r2500: +u_9_3 <= 20; r2501: +u_9_3 >= 7; r2502: +20 x_11_10_0 -u_10_0 +u_11_0 <= 14; r2503: +u_11_0 <= 20; r2504: +u_11_0 >= 9; r2505: +u_10_0 <= 20; r2506: +u_10_0 >= 6; r2507: +20 x_11_10_1 -u_10_1 +u_11_1 <= 14; r2508: +u_11_1 <= 20; r2509: +u_11_1 >= 9; r2510: +u_10_1 <= 20; r2511: +u_10_1 >= 6; r2512: +20 x_11_10_2 -u_10_2 +u_11_2 <= 14; r2513: +u_11_2 <= 20; r2514: +u_11_2 >= 9; r2515: +u_10_2 <= 20; r2516: +u_10_2 >= 6; r2517: +20 x_11_10_3 -u_10_3 +u_11_3 <= 14; r2518: +u_11_3 <= 20; r2519: +u_11_3 >= 9; r2520: +u_10_3 <= 20; r2521: +u_10_3 >= 6; r2522: +20 x_11_12_0 +u_11_0 -u_12_0 <= 11; r2523: +u_11_0 <= 20; r2524: +u_11_0 >= 9; r2525: +u_12_0 <= 20; r2526: +u_12_0 >= 9; r2527: +20 x_11_12_1 +u_11_1 -u_12_1 <= 11; r2528: +u_11_1 <= 20; r2529: +u_11_1 >= 9; r2530: +u_12_1 <= 20; r2531: +u_12_1 >= 9; r2532: +20 x_11_12_2 +u_11_2 -u_12_2 <= 11; r2533: +u_11_2 <= 20; r2534: +u_11_2 >= 9; r2535: +u_12_2 <= 20; r2536: +u_12_2 >= 9; r2537: +20 x_11_12_3 +u_11_3 -u_12_3 <= 11; r2538: +u_11_3 <= 20; r2539: +u_11_3 >= 9; r2540: +u_12_3 <= 20; r2541: +u_12_3 >= 9; r2542: +20 x_12_1_0 -u_1_0 +u_12_0 <= 18; r2543: +u_12_0 <= 20; r2544: +u_12_0 >= 9; r2545: +u_1_0 <= 20; r2546: +u_1_0 >= 2; r2547: +20 x_12_1_1 -u_1_1 +u_12_1 <= 18; r2548: +u_12_1 <= 20; r2549: +u_12_1 >= 9; r2550: +u_1_1 <= 20; r2551: +u_1_1 >= 2; r2552: +20 x_12_1_2 -u_1_2 +u_12_2 <= 18; r2553: +u_12_2 <= 20; r2554: +u_12_2 >= 9; r2555: +u_1_2 <= 20; r2556: +u_1_2 >= 2; r2557: +20 x_12_1_3 -u_1_3 +u_12_3 <= 18; r2558: +u_12_3 <= 20; r2559: +u_12_3 >= 9; r2560: +u_1_3 <= 20; r2561: +u_1_3 >= 2; r2562: +20 x_12_2_0 -u_2_0 +u_12_0 <= 15; r2563: +u_12_0 <= 20; r2564: +u_12_0 >= 9; r2565: +u_2_0 <= 20; r2566: +u_2_0 >= 5; r2567: +20 x_12_2_1 -u_2_1 +u_12_1 <= 15; r2568: +u_12_1 <= 20; r2569: +u_12_1 >= 9; r2570: +u_2_1 <= 20; r2571: +u_2_1 >= 5; r2572: +20 x_12_2_2 -u_2_2 +u_12_2 <= 15; r2573: +u_12_2 <= 20; r2574: +u_12_2 >= 9; r2575: +u_2_2 <= 20; r2576: +u_2_2 >= 5; r2577: +20 x_12_2_3 -u_2_3 +u_12_3 <= 15; r2578: +u_12_3 <= 20; r2579: +u_12_3 >= 9; r2580: +u_2_3 <= 20; r2581: +u_2_3 >= 5; r2582: +20 x_12_3_0 -u_3_0 +u_12_0 <= 19; r2583: +u_12_0 <= 20; r2584: +u_12_0 >= 9; r2585: +u_3_0 <= 20; r2586: +u_3_0 >= 1; r2587: +20 x_12_3_1 -u_3_1 +u_12_1 <= 19; r2588: +u_12_1 <= 20; r2589: +u_12_1 >= 9; r2590: +u_3_1 <= 20; r2591: +u_3_1 >= 1; r2592: +20 x_12_3_2 -u_3_2 +u_12_2 <= 19; r2593: +u_12_2 <= 20; r2594: +u_12_2 >= 9; r2595: +u_3_2 <= 20; r2596: +u_3_2 >= 1; r2597: +20 x_12_3_3 -u_3_3 +u_12_3 <= 19; r2598: +u_12_3 <= 20; r2599: +u_12_3 >= 9; r2600: +u_3_3 <= 20; r2601: +u_3_3 >= 1; r2602: +20 x_12_4_0 -u_4_0 +u_12_0 <= 16; r2603: +u_12_0 <= 20; r2604: +u_12_0 >= 9; r2605: +u_4_0 <= 20; r2606: +u_4_0 >= 4; r2607: +20 x_12_4_1 -u_4_1 +u_12_1 <= 16; r2608: +u_12_1 <= 20; r2609: +u_12_1 >= 9; r2610: +u_4_1 <= 20; r2611: +u_4_1 >= 4; r2612: +20 x_12_4_2 -u_4_2 +u_12_2 <= 16; r2613: +u_12_2 <= 20; r2614: +u_12_2 >= 9; r2615: +u_4_2 <= 20; r2616: +u_4_2 >= 4; r2617: +20 x_12_4_3 -u_4_3 +u_12_3 <= 16; r2618: +u_12_3 <= 20; r2619: +u_12_3 >= 9; r2620: +u_4_3 <= 20; r2621: +u_4_3 >= 4; r2622: +20 x_12_5_0 -u_5_0 +u_12_0 <= 17; r2623: +u_12_0 <= 20; r2624: +u_12_0 >= 9; r2625: +u_5_0 <= 20; r2626: +u_5_0 >= 3; r2627: +20 x_12_5_1 -u_5_1 +u_12_1 <= 17; r2628: +u_12_1 <= 20; r2629: +u_12_1 >= 9; r2630: +u_5_1 <= 20; r2631: +u_5_1 >= 3; r2632: +20 x_12_5_2 -u_5_2 +u_12_2 <= 17; r2633: +u_12_2 <= 20; r2634: +u_12_2 >= 9; r2635: +u_5_2 <= 20; r2636: +u_5_2 >= 3; r2637: +20 x_12_5_3 -u_5_3 +u_12_3 <= 17; r2638: +u_12_3 <= 20; r2639: +u_12_3 >= 9; r2640: +u_5_3 <= 20; r2641: +u_5_3 >= 3; r2642: +20 x_12_6_0 -u_6_0 +u_12_0 <= 10; r2643: +u_12_0 <= 20; r2644: +u_12_0 >= 9; r2645: +u_6_0 <= 20; r2646: +u_6_0 >= 10; r2647: +20 x_12_6_1 -u_6_1 +u_12_1 <= 10; r2648: +u_12_1 <= 20; r2649: +u_12_1 >= 9; r2650: +u_6_1 <= 20; r2651: +u_6_1 >= 10; r2652: +20 x_12_6_2 -u_6_2 +u_12_2 <= 10; r2653: +u_12_2 <= 20; r2654: +u_12_2 >= 9; r2655: +u_6_2 <= 20; r2656: +u_6_2 >= 10; r2657: +20 x_12_6_3 -u_6_3 +u_12_3 <= 10; r2658: +u_12_3 <= 20; r2659: +u_12_3 >= 9; r2660: +u_6_3 <= 20; r2661: +u_6_3 >= 10; r2662: +20 x_12_7_0 -u_7_0 +u_12_0 <= 15; r2663: +u_12_0 <= 20; r2664: +u_12_0 >= 9; r2665: +u_7_0 <= 20; r2666: +u_7_0 >= 5; r2667: +20 x_12_7_1 -u_7_1 +u_12_1 <= 15; r2668: +u_12_1 <= 20; r2669: +u_12_1 >= 9; r2670: +u_7_1 <= 20; r2671: +u_7_1 >= 5; r2672: +20 x_12_7_2 -u_7_2 +u_12_2 <= 15; r2673: +u_12_2 <= 20; r2674: +u_12_2 >= 9; r2675: +u_7_2 <= 20; r2676: +u_7_2 >= 5; r2677: +20 x_12_7_3 -u_7_3 +u_12_3 <= 15; r2678: +u_12_3 <= 20; r2679: +u_12_3 >= 9; r2680: +u_7_3 <= 20; r2681: +u_7_3 >= 5; r2682: +20 x_12_8_0 -u_8_0 +u_12_0 <= 17; r2683: +u_12_0 <= 20; r2684: +u_12_0 >= 9; r2685: +u_8_0 <= 20; r2686: +u_8_0 >= 3; r2687: +20 x_12_8_1 -u_8_1 +u_12_1 <= 17; r2688: +u_12_1 <= 20; r2689: +u_12_1 >= 9; r2690: +u_8_1 <= 20; r2691: +u_8_1 >= 3; r2692: +20 x_12_8_2 -u_8_2 +u_12_2 <= 17; r2693: +u_12_2 <= 20; r2694: +u_12_2 >= 9; r2695: +u_8_2 <= 20; r2696: +u_8_2 >= 3; r2697: +20 x_12_8_3 -u_8_3 +u_12_3 <= 17; r2698: +u_12_3 <= 20; r2699: +u_12_3 >= 9; r2700: +u_8_3 <= 20; r2701: +u_8_3 >= 3; r2702: +20 x_12_9_0 -u_9_0 +u_12_0 <= 13; r2703: +u_12_0 <= 20; r2704: +u_12_0 >= 9; r2705: +u_9_0 <= 20; r2706: +u_9_0 >= 7; r2707: +20 x_12_9_1 -u_9_1 +u_12_1 <= 13; r2708: +u_12_1 <= 20; r2709: +u_12_1 >= 9; r2710: +u_9_1 <= 20; r2711: +u_9_1 >= 7; r2712: +20 x_12_9_2 -u_9_2 +u_12_2 <= 13; r2713: +u_12_2 <= 20; r2714: +u_12_2 >= 9; r2715: +u_9_2 <= 20; r2716: +u_9_2 >= 7; r2717: +20 x_12_9_3 -u_9_3 +u_12_3 <= 13; r2718: +u_12_3 <= 20; r2719: +u_12_3 >= 9; r2720: +u_9_3 <= 20; r2721: +u_9_3 >= 7; r2722: +20 x_12_10_0 -u_10_0 +u_12_0 <= 14; r2723: +u_12_0 <= 20; r2724: +u_12_0 >= 9; r2725: +u_10_0 <= 20; r2726: +u_10_0 >= 6; r2727: +20 x_12_10_1 -u_10_1 +u_12_1 <= 14; r2728: +u_12_1 <= 20; r2729: +u_12_1 >= 9; r2730: +u_10_1 <= 20; r2731: +u_10_1 >= 6; r2732: +20 x_12_10_2 -u_10_2 +u_12_2 <= 14; r2733: +u_12_2 <= 20; r2734: +u_12_2 >= 9; r2735: +u_10_2 <= 20; r2736: +u_10_2 >= 6; r2737: +20 x_12_10_3 -u_10_3 +u_12_3 <= 14; r2738: +u_12_3 <= 20; r2739: +u_12_3 >= 9; r2740: +u_10_3 <= 20; r2741: +u_10_3 >= 6; r2742: +20 x_12_11_0 -u_11_0 +u_12_0 <= 11; r2743: +u_12_0 <= 20; r2744: +u_12_0 >= 9; r2745: +u_11_0 <= 20; r2746: +u_11_0 >= 9; r2747: +20 x_12_11_1 -u_11_1 +u_12_1 <= 11; r2748: +u_12_1 <= 20; r2749: +u_12_1 >= 9; r2750: +u_11_1 <= 20; r2751: +u_11_1 >= 9; r2752: +20 x_12_11_2 -u_11_2 +u_12_2 <= 11; r2753: +u_12_2 <= 20; r2754: +u_12_2 >= 9; r2755: +u_11_2 <= 20; r2756: +u_11_2 >= 9; r2757: +20 x_12_11_3 -u_11_3 +u_12_3 <= 11; r2758: +u_12_3 <= 20; r2759: +u_12_3 >= 9; r2760: +u_11_3 <= 20; r2761: +u_11_3 >= 9; r2762: +x_0_0_0 <= 1; r2763: +x_0_1_0 <= 1; r2764: +x_0_2_0 <= 1; r2765: +x_0_3_0 <= 1; r2766: +x_0_4_0 <= 1; r2767: +x_0_5_0 <= 1; r2768: +x_0_6_0 <= 1; r2769: +x_0_7_0 <= 1; r2770: +x_0_8_0 <= 1; r2771: +x_0_9_0 <= 1; r2772: +x_0_10_0 <= 1; r2773: +x_0_11_0 <= 1; r2774: +x_0_12_0 <= 1; r2775: +x_1_0_0 <= 1; r2776: +x_1_1_0 <= 1; r2777: +x_1_2_0 <= 1; r2778: +x_1_3_0 <= 1; r2779: +x_1_4_0 <= 1; r2780: +x_1_5_0 <= 1; r2781: +x_1_6_0 <= 1; r2782: +x_1_7_0 <= 1; r2783: +x_1_8_0 <= 1; r2784: +x_1_9_0 <= 1; r2785: +x_1_10_0 <= 1; r2786: +x_1_11_0 <= 1; r2787: +x_1_12_0 <= 1; r2788: +x_2_0_0 <= 1; r2789: +x_2_1_0 <= 1; r2790: +x_2_2_0 <= 1; r2791: +x_2_3_0 <= 1; r2792: +x_2_4_0 <= 1; r2793: +x_2_5_0 <= 1; r2794: +x_2_6_0 <= 1; r2795: +x_2_7_0 <= 1; r2796: +x_2_8_0 <= 1; r2797: +x_2_9_0 <= 1; r2798: +x_2_10_0 <= 1; r2799: +x_2_11_0 <= 1; r2800: +x_2_12_0 <= 1; r2801: +x_3_0_0 <= 1; r2802: +x_3_1_0 <= 1; r2803: +x_3_2_0 <= 1; r2804: +x_3_3_0 <= 1; r2805: +x_3_4_0 <= 1; r2806: +x_3_5_0 <= 1; r2807: +x_3_6_0 <= 1; r2808: +x_3_7_0 <= 1; r2809: +x_3_8_0 <= 1; r2810: +x_3_9_0 <= 1; r2811: +x_3_10_0 <= 1; r2812: +x_3_11_0 <= 1; r2813: +x_3_12_0 <= 1; r2814: +x_4_0_0 <= 1; r2815: +x_4_1_0 <= 1; r2816: +x_4_2_0 <= 1; r2817: +x_4_3_0 <= 1; r2818: +x_4_4_0 <= 1; r2819: +x_4_5_0 <= 1; r2820: +x_4_6_0 <= 1; r2821: +x_4_7_0 <= 1; r2822: +x_4_8_0 <= 1; r2823: +x_4_9_0 <= 1; r2824: +x_4_10_0 <= 1; r2825: +x_4_11_0 <= 1; r2826: +x_4_12_0 <= 1; r2827: +x_5_0_0 <= 1; r2828: +x_5_1_0 <= 1; r2829: +x_5_2_0 <= 1; r2830: +x_5_3_0 <= 1; r2831: +x_5_4_0 <= 1; r2832: +x_5_5_0 <= 1; r2833: +x_5_6_0 <= 1; r2834: +x_5_7_0 <= 1; r2835: +x_5_8_0 <= 1; r2836: +x_5_9_0 <= 1; r2837: +x_5_10_0 <= 1; r2838: +x_5_11_0 <= 1; r2839: +x_5_12_0 <= 1; r2840: +x_6_0_0 <= 1; r2841: +x_6_1_0 <= 1; r2842: +x_6_2_0 <= 1; r2843: +x_6_3_0 <= 1; r2844: +x_6_4_0 <= 1; r2845: +x_6_5_0 <= 1; r2846: +x_6_6_0 <= 1; r2847: +x_6_7_0 <= 1; r2848: +x_6_8_0 <= 1; r2849: +x_6_9_0 <= 1; r2850: +x_6_10_0 <= 1; r2851: +x_6_11_0 <= 1; r2852: +x_6_12_0 <= 1; r2853: +x_7_0_0 <= 1; r2854: +x_7_1_0 <= 1; r2855: +x_7_2_0 <= 1; r2856: +x_7_3_0 <= 1; r2857: +x_7_4_0 <= 1; r2858: +x_7_5_0 <= 1; r2859: +x_7_6_0 <= 1; r2860: +x_7_7_0 <= 1; r2861: +x_7_8_0 <= 1; r2862: +x_7_9_0 <= 1; r2863: +x_7_10_0 <= 1; r2864: +x_7_11_0 <= 1; r2865: +x_7_12_0 <= 1; r2866: +x_8_0_0 <= 1; r2867: +x_8_1_0 <= 1; r2868: +x_8_2_0 <= 1; r2869: +x_8_3_0 <= 1; r2870: +x_8_4_0 <= 1; r2871: +x_8_5_0 <= 1; r2872: +x_8_6_0 <= 1; r2873: +x_8_7_0 <= 1; r2874: +x_8_8_0 <= 1; r2875: +x_8_9_0 <= 1; r2876: +x_8_10_0 <= 1; r2877: +x_8_11_0 <= 1; r2878: +x_8_12_0 <= 1; r2879: +x_9_0_0 <= 1; r2880: +x_9_1_0 <= 1; r2881: +x_9_2_0 <= 1; r2882: +x_9_3_0 <= 1; r2883: +x_9_4_0 <= 1; r2884: +x_9_5_0 <= 1; r2885: +x_9_6_0 <= 1; r2886: +x_9_7_0 <= 1; r2887: +x_9_8_0 <= 1; r2888: +x_9_9_0 <= 1; r2889: +x_9_10_0 <= 1; r2890: +x_9_11_0 <= 1; r2891: +x_9_12_0 <= 1; r2892: +x_10_0_0 <= 1; r2893: +x_10_1_0 <= 1; r2894: +x_10_2_0 <= 1; r2895: +x_10_3_0 <= 1; r2896: +x_10_4_0 <= 1; r2897: +x_10_5_0 <= 1; r2898: +x_10_6_0 <= 1; r2899: +x_10_7_0 <= 1; r2900: +x_10_8_0 <= 1; r2901: +x_10_9_0 <= 1; r2902: +x_10_10_0 <= 1; r2903: +x_10_11_0 <= 1; r2904: +x_10_12_0 <= 1; r2905: +x_11_0_0 <= 1; r2906: +x_11_1_0 <= 1; r2907: +x_11_2_0 <= 1; r2908: +x_11_3_0 <= 1; r2909: +x_11_4_0 <= 1; r2910: +x_11_5_0 <= 1; r2911: +x_11_6_0 <= 1; r2912: +x_11_7_0 <= 1; r2913: +x_11_8_0 <= 1; r2914: +x_11_9_0 <= 1; r2915: +x_11_10_0 <= 1; r2916: +x_11_11_0 <= 1; r2917: +x_11_12_0 <= 1; r2918: +x_12_0_0 <= 1; r2919: +x_12_1_0 <= 1; r2920: +x_12_2_0 <= 1; r2921: +x_12_3_0 <= 1; r2922: +x_12_4_0 <= 1; r2923: +x_12_5_0 <= 1; r2924: +x_12_6_0 <= 1; r2925: +x_12_7_0 <= 1; r2926: +x_12_8_0 <= 1; r2927: +x_12_9_0 <= 1; r2928: +x_12_10_0 <= 1; r2929: +x_12_11_0 <= 1; r2930: +x_12_12_0 <= 1; r2931: +x_0_0_0 >= 0; r2932: +x_0_1_0 >= 0; r2933: +x_0_2_0 >= 0; r2934: +x_0_3_0 >= 0; r2935: +x_0_4_0 >= 0; r2936: +x_0_5_0 >= 0; r2937: +x_0_6_0 >= 0; r2938: +x_0_7_0 >= 0; r2939: +x_0_8_0 >= 0; r2940: +x_0_9_0 >= 0; r2941: +x_0_10_0 >= 0; r2942: +x_0_11_0 >= 0; r2943: +x_0_12_0 >= 0; r2944: +x_1_0_0 >= 0; r2945: +x_1_1_0 >= 0; r2946: +x_1_2_0 >= 0; r2947: +x_1_3_0 >= 0; r2948: +x_1_4_0 >= 0; r2949: +x_1_5_0 >= 0; r2950: +x_1_6_0 >= 0; r2951: +x_1_7_0 >= 0; r2952: +x_1_8_0 >= 0; r2953: +x_1_9_0 >= 0; r2954: +x_1_10_0 >= 0; r2955: +x_1_11_0 >= 0; r2956: +x_1_12_0 >= 0; r2957: +x_2_0_0 >= 0; r2958: +x_2_1_0 >= 0; r2959: +x_2_2_0 >= 0; r2960: +x_2_3_0 >= 0; r2961: +x_2_4_0 >= 0; r2962: +x_2_5_0 >= 0; r2963: +x_2_6_0 >= 0; r2964: +x_2_7_0 >= 0; r2965: +x_2_8_0 >= 0; r2966: +x_2_9_0 >= 0; r2967: +x_2_10_0 >= 0; r2968: +x_2_11_0 >= 0; r2969: +x_2_12_0 >= 0; r2970: +x_3_0_0 >= 0; r2971: +x_3_1_0 >= 0; r2972: +x_3_2_0 >= 0; r2973: +x_3_3_0 >= 0; r2974: +x_3_4_0 >= 0; r2975: +x_3_5_0 >= 0; r2976: +x_3_6_0 >= 0; r2977: +x_3_7_0 >= 0; r2978: +x_3_8_0 >= 0; r2979: +x_3_9_0 >= 0; r2980: +x_3_10_0 >= 0; r2981: +x_3_11_0 >= 0; r2982: +x_3_12_0 >= 0; r2983: +x_4_0_0 >= 0; r2984: +x_4_1_0 >= 0; r2985: +x_4_2_0 >= 0; r2986: +x_4_3_0 >= 0; r2987: +x_4_4_0 >= 0; r2988: +x_4_5_0 >= 0; r2989: +x_4_6_0 >= 0; r2990: +x_4_7_0 >= 0; r2991: +x_4_8_0 >= 0; r2992: +x_4_9_0 >= 0; r2993: +x_4_10_0 >= 0; r2994: +x_4_11_0 >= 0; r2995: +x_4_12_0 >= 0; r2996: +x_5_0_0 >= 0; r2997: +x_5_1_0 >= 0; r2998: +x_5_2_0 >= 0; r2999: +x_5_3_0 >= 0; r3000: +x_5_4_0 >= 0; r3001: +x_5_5_0 >= 0; r3002: +x_5_6_0 >= 0; r3003: +x_5_7_0 >= 0; r3004: +x_5_8_0 >= 0; r3005: +x_5_9_0 >= 0; r3006: +x_5_10_0 >= 0; r3007: +x_5_11_0 >= 0; r3008: +x_5_12_0 >= 0; r3009: +x_6_0_0 >= 0; r3010: +x_6_1_0 >= 0; r3011: +x_6_2_0 >= 0; r3012: +x_6_3_0 >= 0; r3013: +x_6_4_0 >= 0; r3014: +x_6_5_0 >= 0; r3015: +x_6_6_0 >= 0; r3016: +x_6_7_0 >= 0; r3017: +x_6_8_0 >= 0; r3018: +x_6_9_0 >= 0; r3019: +x_6_10_0 >= 0; r3020: +x_6_11_0 >= 0; r3021: +x_6_12_0 >= 0; r3022: +x_7_0_0 >= 0; r3023: +x_7_1_0 >= 0; r3024: +x_7_2_0 >= 0; r3025: +x_7_3_0 >= 0; r3026: +x_7_4_0 >= 0; r3027: +x_7_5_0 >= 0; r3028: +x_7_6_0 >= 0; r3029: +x_7_7_0 >= 0; r3030: +x_7_8_0 >= 0; r3031: +x_7_9_0 >= 0; r3032: +x_7_10_0 >= 0; r3033: +x_7_11_0 >= 0; r3034: +x_7_12_0 >= 0; r3035: +x_8_0_0 >= 0; r3036: +x_8_1_0 >= 0; r3037: +x_8_2_0 >= 0; r3038: +x_8_3_0 >= 0; r3039: +x_8_4_0 >= 0; r3040: +x_8_5_0 >= 0; r3041: +x_8_6_0 >= 0; r3042: +x_8_7_0 >= 0; r3043: +x_8_8_0 >= 0; r3044: +x_8_9_0 >= 0; r3045: +x_8_10_0 >= 0; r3046: +x_8_11_0 >= 0; r3047: +x_8_12_0 >= 0; r3048: +x_9_0_0 >= 0; r3049: +x_9_1_0 >= 0; r3050: +x_9_2_0 >= 0; r3051: +x_9_3_0 >= 0; r3052: +x_9_4_0 >= 0; r3053: +x_9_5_0 >= 0; r3054: +x_9_6_0 >= 0; r3055: +x_9_7_0 >= 0; r3056: +x_9_8_0 >= 0; r3057: +x_9_9_0 >= 0; r3058: +x_9_10_0 >= 0; r3059: +x_9_11_0 >= 0; r3060: +x_9_12_0 >= 0; r3061: +x_10_0_0 >= 0; r3062: +x_10_1_0 >= 0; r3063: +x_10_2_0 >= 0; r3064: +x_10_3_0 >= 0; r3065: +x_10_4_0 >= 0; r3066: +x_10_5_0 >= 0; r3067: +x_10_6_0 >= 0; r3068: +x_10_7_0 >= 0; r3069: +x_10_8_0 >= 0; r3070: +x_10_9_0 >= 0; r3071: +x_10_10_0 >= 0; r3072: +x_10_11_0 >= 0; r3073: +x_10_12_0 >= 0; r3074: +x_11_0_0 >= 0; r3075: +x_11_1_0 >= 0; r3076: +x_11_2_0 >= 0; r3077: +x_11_3_0 >= 0; r3078: +x_11_4_0 >= 0; r3079: +x_11_5_0 >= 0; r3080: +x_11_6_0 >= 0; r3081: +x_11_7_0 >= 0; r3082: +x_11_8_0 >= 0; r3083: +x_11_9_0 >= 0; r3084: +x_11_10_0 >= 0; r3085: +x_11_11_0 >= 0; r3086: +x_11_12_0 >= 0; r3087: +x_12_0_0 >= 0; r3088: +x_12_1_0 >= 0; r3089: +x_12_2_0 >= 0; r3090: +x_12_3_0 >= 0; r3091: +x_12_4_0 >= 0; r3092: +x_12_5_0 >= 0; r3093: +x_12_6_0 >= 0; r3094: +x_12_7_0 >= 0; r3095: +x_12_8_0 >= 0; r3096: +x_12_9_0 >= 0; r3097: +x_12_10_0 >= 0; r3098: +x_12_11_0 >= 0; r3099: +x_12_12_0 >= 0; r3100: +x_0_0_1 <= 1; r3101: +x_0_1_1 <= 1; r3102: +x_0_2_1 <= 1; r3103: +x_0_3_1 <= 1; r3104: +x_0_4_1 <= 1; r3105: +x_0_5_1 <= 1; r3106: +x_0_6_1 <= 1; r3107: +x_0_7_1 <= 1; r3108: +x_0_8_1 <= 1; r3109: +x_0_9_1 <= 1; r3110: +x_0_10_1 <= 1; r3111: +x_0_11_1 <= 1; r3112: +x_0_12_1 <= 1; r3113: +x_1_0_1 <= 1; r3114: +x_1_1_1 <= 1; r3115: +x_1_2_1 <= 1; r3116: +x_1_3_1 <= 1; r3117: +x_1_4_1 <= 1; r3118: +x_1_5_1 <= 1; r3119: +x_1_6_1 <= 1; r3120: +x_1_7_1 <= 1; r3121: +x_1_8_1 <= 1; r3122: +x_1_9_1 <= 1; r3123: +x_1_10_1 <= 1; r3124: +x_1_11_1 <= 1; r3125: +x_1_12_1 <= 1; r3126: +x_2_0_1 <= 1; r3127: +x_2_1_1 <= 1; r3128: +x_2_2_1 <= 1; r3129: +x_2_3_1 <= 1; r3130: +x_2_4_1 <= 1; r3131: +x_2_5_1 <= 1; r3132: +x_2_6_1 <= 1; r3133: +x_2_7_1 <= 1; r3134: +x_2_8_1 <= 1; r3135: +x_2_9_1 <= 1; r3136: +x_2_10_1 <= 1; r3137: +x_2_11_1 <= 1; r3138: +x_2_12_1 <= 1; r3139: +x_3_0_1 <= 1; r3140: +x_3_1_1 <= 1; r3141: +x_3_2_1 <= 1; r3142: +x_3_3_1 <= 1; r3143: +x_3_4_1 <= 1; r3144: +x_3_5_1 <= 1; r3145: +x_3_6_1 <= 1; r3146: +x_3_7_1 <= 1; r3147: +x_3_8_1 <= 1; r3148: +x_3_9_1 <= 1; r3149: +x_3_10_1 <= 1; r3150: +x_3_11_1 <= 1; r3151: +x_3_12_1 <= 1; r3152: +x_4_0_1 <= 1; r3153: +x_4_1_1 <= 1; r3154: +x_4_2_1 <= 1; r3155: +x_4_3_1 <= 1; r3156: +x_4_4_1 <= 1; r3157: +x_4_5_1 <= 1; r3158: +x_4_6_1 <= 1; r3159: +x_4_7_1 <= 1; r3160: +x_4_8_1 <= 1; r3161: +x_4_9_1 <= 1; r3162: +x_4_10_1 <= 1; r3163: +x_4_11_1 <= 1; r3164: +x_4_12_1 <= 1; r3165: +x_5_0_1 <= 1; r3166: +x_5_1_1 <= 1; r3167: +x_5_2_1 <= 1; r3168: +x_5_3_1 <= 1; r3169: +x_5_4_1 <= 1; r3170: +x_5_5_1 <= 1; r3171: +x_5_6_1 <= 1; r3172: +x_5_7_1 <= 1; r3173: +x_5_8_1 <= 1; r3174: +x_5_9_1 <= 1; r3175: +x_5_10_1 <= 1; r3176: +x_5_11_1 <= 1; r3177: +x_5_12_1 <= 1; r3178: +x_6_0_1 <= 1; r3179: +x_6_1_1 <= 1; r3180: +x_6_2_1 <= 1; r3181: +x_6_3_1 <= 1; r3182: +x_6_4_1 <= 1; r3183: +x_6_5_1 <= 1; r3184: +x_6_6_1 <= 1; r3185: +x_6_7_1 <= 1; r3186: +x_6_8_1 <= 1; r3187: +x_6_9_1 <= 1; r3188: +x_6_10_1 <= 1; r3189: +x_6_11_1 <= 1; r3190: +x_6_12_1 <= 1; r3191: +x_7_0_1 <= 1; r3192: +x_7_1_1 <= 1; r3193: +x_7_2_1 <= 1; r3194: +x_7_3_1 <= 1; r3195: +x_7_4_1 <= 1; r3196: +x_7_5_1 <= 1; r3197: +x_7_6_1 <= 1; r3198: +x_7_7_1 <= 1; r3199: +x_7_8_1 <= 1; r3200: +x_7_9_1 <= 1; r3201: +x_7_10_1 <= 1; r3202: +x_7_11_1 <= 1; r3203: +x_7_12_1 <= 1; r3204: +x_8_0_1 <= 1; r3205: +x_8_1_1 <= 1; r3206: +x_8_2_1 <= 1; r3207: +x_8_3_1 <= 1; r3208: +x_8_4_1 <= 1; r3209: +x_8_5_1 <= 1; r3210: +x_8_6_1 <= 1; r3211: +x_8_7_1 <= 1; r3212: +x_8_8_1 <= 1; r3213: +x_8_9_1 <= 1; r3214: +x_8_10_1 <= 1; r3215: +x_8_11_1 <= 1; r3216: +x_8_12_1 <= 1; r3217: +x_9_0_1 <= 1; r3218: +x_9_1_1 <= 1; r3219: +x_9_2_1 <= 1; r3220: +x_9_3_1 <= 1; r3221: +x_9_4_1 <= 1; r3222: +x_9_5_1 <= 1; r3223: +x_9_6_1 <= 1; r3224: +x_9_7_1 <= 1; r3225: +x_9_8_1 <= 1; r3226: +x_9_9_1 <= 1; r3227: +x_9_10_1 <= 1; r3228: +x_9_11_1 <= 1; r3229: +x_9_12_1 <= 1; r3230: +x_10_0_1 <= 1; r3231: +x_10_1_1 <= 1; r3232: +x_10_2_1 <= 1; r3233: +x_10_3_1 <= 1; r3234: +x_10_4_1 <= 1; r3235: +x_10_5_1 <= 1; r3236: +x_10_6_1 <= 1; r3237: +x_10_7_1 <= 1; r3238: +x_10_8_1 <= 1; r3239: +x_10_9_1 <= 1; r3240: +x_10_10_1 <= 1; r3241: +x_10_11_1 <= 1; r3242: +x_10_12_1 <= 1; r3243: +x_11_0_1 <= 1; r3244: +x_11_1_1 <= 1; r3245: +x_11_2_1 <= 1; r3246: +x_11_3_1 <= 1; r3247: +x_11_4_1 <= 1; r3248: +x_11_5_1 <= 1; r3249: +x_11_6_1 <= 1; r3250: +x_11_7_1 <= 1; r3251: +x_11_8_1 <= 1; r3252: +x_11_9_1 <= 1; r3253: +x_11_10_1 <= 1; r3254: +x_11_11_1 <= 1; r3255: +x_11_12_1 <= 1; r3256: +x_12_0_1 <= 1; r3257: +x_12_1_1 <= 1; r3258: +x_12_2_1 <= 1; r3259: +x_12_3_1 <= 1; r3260: +x_12_4_1 <= 1; r3261: +x_12_5_1 <= 1; r3262: +x_12_6_1 <= 1; r3263: +x_12_7_1 <= 1; r3264: +x_12_8_1 <= 1; r3265: +x_12_9_1 <= 1; r3266: +x_12_10_1 <= 1; r3267: +x_12_11_1 <= 1; r3268: +x_12_12_1 <= 1; r3269: +x_0_0_1 >= 0; r3270: +x_0_1_1 >= 0; r3271: +x_0_2_1 >= 0; r3272: +x_0_3_1 >= 0; r3273: +x_0_4_1 >= 0; r3274: +x_0_5_1 >= 0; r3275: +x_0_6_1 >= 0; r3276: +x_0_7_1 >= 0; r3277: +x_0_8_1 >= 0; r3278: +x_0_9_1 >= 0; r3279: +x_0_10_1 >= 0; r3280: +x_0_11_1 >= 0; r3281: +x_0_12_1 >= 0; r3282: +x_1_0_1 >= 0; r3283: +x_1_1_1 >= 0; r3284: +x_1_2_1 >= 0; r3285: +x_1_3_1 >= 0; r3286: +x_1_4_1 >= 0; r3287: +x_1_5_1 >= 0; r3288: +x_1_6_1 >= 0; r3289: +x_1_7_1 >= 0; r3290: +x_1_8_1 >= 0; r3291: +x_1_9_1 >= 0; r3292: +x_1_10_1 >= 0; r3293: +x_1_11_1 >= 0; r3294: +x_1_12_1 >= 0; r3295: +x_2_0_1 >= 0; r3296: +x_2_1_1 >= 0; r3297: +x_2_2_1 >= 0; r3298: +x_2_3_1 >= 0; r3299: +x_2_4_1 >= 0; r3300: +x_2_5_1 >= 0; r3301: +x_2_6_1 >= 0; r3302: +x_2_7_1 >= 0; r3303: +x_2_8_1 >= 0; r3304: +x_2_9_1 >= 0; r3305: +x_2_10_1 >= 0; r3306: +x_2_11_1 >= 0; r3307: +x_2_12_1 >= 0; r3308: +x_3_0_1 >= 0; r3309: +x_3_1_1 >= 0; r3310: +x_3_2_1 >= 0; r3311: +x_3_3_1 >= 0; r3312: +x_3_4_1 >= 0; r3313: +x_3_5_1 >= 0; r3314: +x_3_6_1 >= 0; r3315: +x_3_7_1 >= 0; r3316: +x_3_8_1 >= 0; r3317: +x_3_9_1 >= 0; r3318: +x_3_10_1 >= 0; r3319: +x_3_11_1 >= 0; r3320: +x_3_12_1 >= 0; r3321: +x_4_0_1 >= 0; r3322: +x_4_1_1 >= 0; r3323: +x_4_2_1 >= 0; r3324: +x_4_3_1 >= 0; r3325: +x_4_4_1 >= 0; r3326: +x_4_5_1 >= 0; r3327: +x_4_6_1 >= 0; r3328: +x_4_7_1 >= 0; r3329: +x_4_8_1 >= 0; r3330: +x_4_9_1 >= 0; r3331: +x_4_10_1 >= 0; r3332: +x_4_11_1 >= 0; r3333: +x_4_12_1 >= 0; r3334: +x_5_0_1 >= 0; r3335: +x_5_1_1 >= 0; r3336: +x_5_2_1 >= 0; r3337: +x_5_3_1 >= 0; r3338: +x_5_4_1 >= 0; r3339: +x_5_5_1 >= 0; r3340: +x_5_6_1 >= 0; r3341: +x_5_7_1 >= 0; r3342: +x_5_8_1 >= 0; r3343: +x_5_9_1 >= 0; r3344: +x_5_10_1 >= 0; r3345: +x_5_11_1 >= 0; r3346: +x_5_12_1 >= 0; r3347: +x_6_0_1 >= 0; r3348: +x_6_1_1 >= 0; r3349: +x_6_2_1 >= 0; r3350: +x_6_3_1 >= 0; r3351: +x_6_4_1 >= 0; r3352: +x_6_5_1 >= 0; r3353: +x_6_6_1 >= 0; r3354: +x_6_7_1 >= 0; r3355: +x_6_8_1 >= 0; r3356: +x_6_9_1 >= 0; r3357: +x_6_10_1 >= 0; r3358: +x_6_11_1 >= 0; r3359: +x_6_12_1 >= 0; r3360: +x_7_0_1 >= 0; r3361: +x_7_1_1 >= 0; r3362: +x_7_2_1 >= 0; r3363: +x_7_3_1 >= 0; r3364: +x_7_4_1 >= 0; r3365: +x_7_5_1 >= 0; r3366: +x_7_6_1 >= 0; r3367: +x_7_7_1 >= 0; r3368: +x_7_8_1 >= 0; r3369: +x_7_9_1 >= 0; r3370: +x_7_10_1 >= 0; r3371: +x_7_11_1 >= 0; r3372: +x_7_12_1 >= 0; r3373: +x_8_0_1 >= 0; r3374: +x_8_1_1 >= 0; r3375: +x_8_2_1 >= 0; r3376: +x_8_3_1 >= 0; r3377: +x_8_4_1 >= 0; r3378: +x_8_5_1 >= 0; r3379: +x_8_6_1 >= 0; r3380: +x_8_7_1 >= 0; r3381: +x_8_8_1 >= 0; r3382: +x_8_9_1 >= 0; r3383: +x_8_10_1 >= 0; r3384: +x_8_11_1 >= 0; r3385: +x_8_12_1 >= 0; r3386: +x_9_0_1 >= 0; r3387: +x_9_1_1 >= 0; r3388: +x_9_2_1 >= 0; r3389: +x_9_3_1 >= 0; r3390: +x_9_4_1 >= 0; r3391: +x_9_5_1 >= 0; r3392: +x_9_6_1 >= 0; r3393: +x_9_7_1 >= 0; r3394: +x_9_8_1 >= 0; r3395: +x_9_9_1 >= 0; r3396: +x_9_10_1 >= 0; r3397: +x_9_11_1 >= 0; r3398: +x_9_12_1 >= 0; r3399: +x_10_0_1 >= 0; r3400: +x_10_1_1 >= 0; r3401: +x_10_2_1 >= 0; r3402: +x_10_3_1 >= 0; r3403: +x_10_4_1 >= 0; r3404: +x_10_5_1 >= 0; r3405: +x_10_6_1 >= 0; r3406: +x_10_7_1 >= 0; r3407: +x_10_8_1 >= 0; r3408: +x_10_9_1 >= 0; r3409: +x_10_10_1 >= 0; r3410: +x_10_11_1 >= 0; r3411: +x_10_12_1 >= 0; r3412: +x_11_0_1 >= 0; r3413: +x_11_1_1 >= 0; r3414: +x_11_2_1 >= 0; r3415: +x_11_3_1 >= 0; r3416: +x_11_4_1 >= 0; r3417: +x_11_5_1 >= 0; r3418: +x_11_6_1 >= 0; r3419: +x_11_7_1 >= 0; r3420: +x_11_8_1 >= 0; r3421: +x_11_9_1 >= 0; r3422: +x_11_10_1 >= 0; r3423: +x_11_11_1 >= 0; r3424: +x_11_12_1 >= 0; r3425: +x_12_0_1 >= 0; r3426: +x_12_1_1 >= 0; r3427: +x_12_2_1 >= 0; r3428: +x_12_3_1 >= 0; r3429: +x_12_4_1 >= 0; r3430: +x_12_5_1 >= 0; r3431: +x_12_6_1 >= 0; r3432: +x_12_7_1 >= 0; r3433: +x_12_8_1 >= 0; r3434: +x_12_9_1 >= 0; r3435: +x_12_10_1 >= 0; r3436: +x_12_11_1 >= 0; r3437: +x_12_12_1 >= 0; r3438: +x_0_0_2 <= 1; r3439: +x_0_1_2 <= 1; r3440: +x_0_2_2 <= 1; r3441: +x_0_3_2 <= 1; r3442: +x_0_4_2 <= 1; r3443: +x_0_5_2 <= 1; r3444: +x_0_6_2 <= 1; r3445: +x_0_7_2 <= 1; r3446: +x_0_8_2 <= 1; r3447: +x_0_9_2 <= 1; r3448: +x_0_10_2 <= 1; r3449: +x_0_11_2 <= 1; r3450: +x_0_12_2 <= 1; r3451: +x_1_0_2 <= 1; r3452: +x_1_1_2 <= 1; r3453: +x_1_2_2 <= 1; r3454: +x_1_3_2 <= 1; r3455: +x_1_4_2 <= 1; r3456: +x_1_5_2 <= 1; r3457: +x_1_6_2 <= 1; r3458: +x_1_7_2 <= 1; r3459: +x_1_8_2 <= 1; r3460: +x_1_9_2 <= 1; r3461: +x_1_10_2 <= 1; r3462: +x_1_11_2 <= 1; r3463: +x_1_12_2 <= 1; r3464: +x_2_0_2 <= 1; r3465: +x_2_1_2 <= 1; r3466: +x_2_2_2 <= 1; r3467: +x_2_3_2 <= 1; r3468: +x_2_4_2 <= 1; r3469: +x_2_5_2 <= 1; r3470: +x_2_6_2 <= 1; r3471: +x_2_7_2 <= 1; r3472: +x_2_8_2 <= 1; r3473: +x_2_9_2 <= 1; r3474: +x_2_10_2 <= 1; r3475: +x_2_11_2 <= 1; r3476: +x_2_12_2 <= 1; r3477: +x_3_0_2 <= 1; r3478: +x_3_1_2 <= 1; r3479: +x_3_2_2 <= 1; r3480: +x_3_3_2 <= 1; r3481: +x_3_4_2 <= 1; r3482: +x_3_5_2 <= 1; r3483: +x_3_6_2 <= 1; r3484: +x_3_7_2 <= 1; r3485: +x_3_8_2 <= 1; r3486: +x_3_9_2 <= 1; r3487: +x_3_10_2 <= 1; r3488: +x_3_11_2 <= 1; r3489: +x_3_12_2 <= 1; r3490: +x_4_0_2 <= 1; r3491: +x_4_1_2 <= 1; r3492: +x_4_2_2 <= 1; r3493: +x_4_3_2 <= 1; r3494: +x_4_4_2 <= 1; r3495: +x_4_5_2 <= 1; r3496: +x_4_6_2 <= 1; r3497: +x_4_7_2 <= 1; r3498: +x_4_8_2 <= 1; r3499: +x_4_9_2 <= 1; r3500: +x_4_10_2 <= 1; r3501: +x_4_11_2 <= 1; r3502: +x_4_12_2 <= 1; r3503: +x_5_0_2 <= 1; r3504: +x_5_1_2 <= 1; r3505: +x_5_2_2 <= 1; r3506: +x_5_3_2 <= 1; r3507: +x_5_4_2 <= 1; r3508: +x_5_5_2 <= 1; r3509: +x_5_6_2 <= 1; r3510: +x_5_7_2 <= 1; r3511: +x_5_8_2 <= 1; r3512: +x_5_9_2 <= 1; r3513: +x_5_10_2 <= 1; r3514: +x_5_11_2 <= 1; r3515: +x_5_12_2 <= 1; r3516: +x_6_0_2 <= 1; r3517: +x_6_1_2 <= 1; r3518: +x_6_2_2 <= 1; r3519: +x_6_3_2 <= 1; r3520: +x_6_4_2 <= 1; r3521: +x_6_5_2 <= 1; r3522: +x_6_6_2 <= 1; r3523: +x_6_7_2 <= 1; r3524: +x_6_8_2 <= 1; r3525: +x_6_9_2 <= 1; r3526: +x_6_10_2 <= 1; r3527: +x_6_11_2 <= 1; r3528: +x_6_12_2 <= 1; r3529: +x_7_0_2 <= 1; r3530: +x_7_1_2 <= 1; r3531: +x_7_2_2 <= 1; r3532: +x_7_3_2 <= 1; r3533: +x_7_4_2 <= 1; r3534: +x_7_5_2 <= 1; r3535: +x_7_6_2 <= 1; r3536: +x_7_7_2 <= 1; r3537: +x_7_8_2 <= 1; r3538: +x_7_9_2 <= 1; r3539: +x_7_10_2 <= 1; r3540: +x_7_11_2 <= 1; r3541: +x_7_12_2 <= 1; r3542: +x_8_0_2 <= 1; r3543: +x_8_1_2 <= 1; r3544: +x_8_2_2 <= 1; r3545: +x_8_3_2 <= 1; r3546: +x_8_4_2 <= 1; r3547: +x_8_5_2 <= 1; r3548: +x_8_6_2 <= 1; r3549: +x_8_7_2 <= 1; r3550: +x_8_8_2 <= 1; r3551: +x_8_9_2 <= 1; r3552: +x_8_10_2 <= 1; r3553: +x_8_11_2 <= 1; r3554: +x_8_12_2 <= 1; r3555: +x_9_0_2 <= 1; r3556: +x_9_1_2 <= 1; r3557: +x_9_2_2 <= 1; r3558: +x_9_3_2 <= 1; r3559: +x_9_4_2 <= 1; r3560: +x_9_5_2 <= 1; r3561: +x_9_6_2 <= 1; r3562: +x_9_7_2 <= 1; r3563: +x_9_8_2 <= 1; r3564: +x_9_9_2 <= 1; r3565: +x_9_10_2 <= 1; r3566: +x_9_11_2 <= 1; r3567: +x_9_12_2 <= 1; r3568: +x_10_0_2 <= 1; r3569: +x_10_1_2 <= 1; r3570: +x_10_2_2 <= 1; r3571: +x_10_3_2 <= 1; r3572: +x_10_4_2 <= 1; r3573: +x_10_5_2 <= 1; r3574: +x_10_6_2 <= 1; r3575: +x_10_7_2 <= 1; r3576: +x_10_8_2 <= 1; r3577: +x_10_9_2 <= 1; r3578: +x_10_10_2 <= 1; r3579: +x_10_11_2 <= 1; r3580: +x_10_12_2 <= 1; r3581: +x_11_0_2 <= 1; r3582: +x_11_1_2 <= 1; r3583: +x_11_2_2 <= 1; r3584: +x_11_3_2 <= 1; r3585: +x_11_4_2 <= 1; r3586: +x_11_5_2 <= 1; r3587: +x_11_6_2 <= 1; r3588: +x_11_7_2 <= 1; r3589: +x_11_8_2 <= 1; r3590: +x_11_9_2 <= 1; r3591: +x_11_10_2 <= 1; r3592: +x_11_11_2 <= 1; r3593: +x_11_12_2 <= 1; r3594: +x_12_0_2 <= 1; r3595: +x_12_1_2 <= 1; r3596: +x_12_2_2 <= 1; r3597: +x_12_3_2 <= 1; r3598: +x_12_4_2 <= 1; r3599: +x_12_5_2 <= 1; r3600: +x_12_6_2 <= 1; r3601: +x_12_7_2 <= 1; r3602: +x_12_8_2 <= 1; r3603: +x_12_9_2 <= 1; r3604: +x_12_10_2 <= 1; r3605: +x_12_11_2 <= 1; r3606: +x_12_12_2 <= 1; r3607: +x_0_0_2 >= 0; r3608: +x_0_1_2 >= 0; r3609: +x_0_2_2 >= 0; r3610: +x_0_3_2 >= 0; r3611: +x_0_4_2 >= 0; r3612: +x_0_5_2 >= 0; r3613: +x_0_6_2 >= 0; r3614: +x_0_7_2 >= 0; r3615: +x_0_8_2 >= 0; r3616: +x_0_9_2 >= 0; r3617: +x_0_10_2 >= 0; r3618: +x_0_11_2 >= 0; r3619: +x_0_12_2 >= 0; r3620: +x_1_0_2 >= 0; r3621: +x_1_1_2 >= 0; r3622: +x_1_2_2 >= 0; r3623: +x_1_3_2 >= 0; r3624: +x_1_4_2 >= 0; r3625: +x_1_5_2 >= 0; r3626: +x_1_6_2 >= 0; r3627: +x_1_7_2 >= 0; r3628: +x_1_8_2 >= 0; r3629: +x_1_9_2 >= 0; r3630: +x_1_10_2 >= 0; r3631: +x_1_11_2 >= 0; r3632: +x_1_12_2 >= 0; r3633: +x_2_0_2 >= 0; r3634: +x_2_1_2 >= 0; r3635: +x_2_2_2 >= 0; r3636: +x_2_3_2 >= 0; r3637: +x_2_4_2 >= 0; r3638: +x_2_5_2 >= 0; r3639: +x_2_6_2 >= 0; r3640: +x_2_7_2 >= 0; r3641: +x_2_8_2 >= 0; r3642: +x_2_9_2 >= 0; r3643: +x_2_10_2 >= 0; r3644: +x_2_11_2 >= 0; r3645: +x_2_12_2 >= 0; r3646: +x_3_0_2 >= 0; r3647: +x_3_1_2 >= 0; r3648: +x_3_2_2 >= 0; r3649: +x_3_3_2 >= 0; r3650: +x_3_4_2 >= 0; r3651: +x_3_5_2 >= 0; r3652: +x_3_6_2 >= 0; r3653: +x_3_7_2 >= 0; r3654: +x_3_8_2 >= 0; r3655: +x_3_9_2 >= 0; r3656: +x_3_10_2 >= 0; r3657: +x_3_11_2 >= 0; r3658: +x_3_12_2 >= 0; r3659: +x_4_0_2 >= 0; r3660: +x_4_1_2 >= 0; r3661: +x_4_2_2 >= 0; r3662: +x_4_3_2 >= 0; r3663: +x_4_4_2 >= 0; r3664: +x_4_5_2 >= 0; r3665: +x_4_6_2 >= 0; r3666: +x_4_7_2 >= 0; r3667: +x_4_8_2 >= 0; r3668: +x_4_9_2 >= 0; r3669: +x_4_10_2 >= 0; r3670: +x_4_11_2 >= 0; r3671: +x_4_12_2 >= 0; r3672: +x_5_0_2 >= 0; r3673: +x_5_1_2 >= 0; r3674: +x_5_2_2 >= 0; r3675: +x_5_3_2 >= 0; r3676: +x_5_4_2 >= 0; r3677: +x_5_5_2 >= 0; r3678: +x_5_6_2 >= 0; r3679: +x_5_7_2 >= 0; r3680: +x_5_8_2 >= 0; r3681: +x_5_9_2 >= 0; r3682: +x_5_10_2 >= 0; r3683: +x_5_11_2 >= 0; r3684: +x_5_12_2 >= 0; r3685: +x_6_0_2 >= 0; r3686: +x_6_1_2 >= 0; r3687: +x_6_2_2 >= 0; r3688: +x_6_3_2 >= 0; r3689: +x_6_4_2 >= 0; r3690: +x_6_5_2 >= 0; r3691: +x_6_6_2 >= 0; r3692: +x_6_7_2 >= 0; r3693: +x_6_8_2 >= 0; r3694: +x_6_9_2 >= 0; r3695: +x_6_10_2 >= 0; r3696: +x_6_11_2 >= 0; r3697: +x_6_12_2 >= 0; r3698: +x_7_0_2 >= 0; r3699: +x_7_1_2 >= 0; r3700: +x_7_2_2 >= 0; r3701: +x_7_3_2 >= 0; r3702: +x_7_4_2 >= 0; r3703: +x_7_5_2 >= 0; r3704: +x_7_6_2 >= 0; r3705: +x_7_7_2 >= 0; r3706: +x_7_8_2 >= 0; r3707: +x_7_9_2 >= 0; r3708: +x_7_10_2 >= 0; r3709: +x_7_11_2 >= 0; r3710: +x_7_12_2 >= 0; r3711: +x_8_0_2 >= 0; r3712: +x_8_1_2 >= 0; r3713: +x_8_2_2 >= 0; r3714: +x_8_3_2 >= 0; r3715: +x_8_4_2 >= 0; r3716: +x_8_5_2 >= 0; r3717: +x_8_6_2 >= 0; r3718: +x_8_7_2 >= 0; r3719: +x_8_8_2 >= 0; r3720: +x_8_9_2 >= 0; r3721: +x_8_10_2 >= 0; r3722: +x_8_11_2 >= 0; r3723: +x_8_12_2 >= 0; r3724: +x_9_0_2 >= 0; r3725: +x_9_1_2 >= 0; r3726: +x_9_2_2 >= 0; r3727: +x_9_3_2 >= 0; r3728: +x_9_4_2 >= 0; r3729: +x_9_5_2 >= 0; r3730: +x_9_6_2 >= 0; r3731: +x_9_7_2 >= 0; r3732: +x_9_8_2 >= 0; r3733: +x_9_9_2 >= 0; r3734: +x_9_10_2 >= 0; r3735: +x_9_11_2 >= 0; r3736: +x_9_12_2 >= 0; r3737: +x_10_0_2 >= 0; r3738: +x_10_1_2 >= 0; r3739: +x_10_2_2 >= 0; r3740: +x_10_3_2 >= 0; r3741: +x_10_4_2 >= 0; r3742: +x_10_5_2 >= 0; r3743: +x_10_6_2 >= 0; r3744: +x_10_7_2 >= 0; r3745: +x_10_8_2 >= 0; r3746: +x_10_9_2 >= 0; r3747: +x_10_10_2 >= 0; r3748: +x_10_11_2 >= 0; r3749: +x_10_12_2 >= 0; r3750: +x_11_0_2 >= 0; r3751: +x_11_1_2 >= 0; r3752: +x_11_2_2 >= 0; r3753: +x_11_3_2 >= 0; r3754: +x_11_4_2 >= 0; r3755: +x_11_5_2 >= 0; r3756: +x_11_6_2 >= 0; r3757: +x_11_7_2 >= 0; r3758: +x_11_8_2 >= 0; r3759: +x_11_9_2 >= 0; r3760: +x_11_10_2 >= 0; r3761: +x_11_11_2 >= 0; r3762: +x_11_12_2 >= 0; r3763: +x_12_0_2 >= 0; r3764: +x_12_1_2 >= 0; r3765: +x_12_2_2 >= 0; r3766: +x_12_3_2 >= 0; r3767: +x_12_4_2 >= 0; r3768: +x_12_5_2 >= 0; r3769: +x_12_6_2 >= 0; r3770: +x_12_7_2 >= 0; r3771: +x_12_8_2 >= 0; r3772: +x_12_9_2 >= 0; r3773: +x_12_10_2 >= 0; r3774: +x_12_11_2 >= 0; r3775: +x_12_12_2 >= 0; r3776: +x_0_0_3 <= 1; r3777: +x_0_1_3 <= 1; r3778: +x_0_2_3 <= 1; r3779: +x_0_3_3 <= 1; r3780: +x_0_4_3 <= 1; r3781: +x_0_5_3 <= 1; r3782: +x_0_6_3 <= 1; r3783: +x_0_7_3 <= 1; r3784: +x_0_8_3 <= 1; r3785: +x_0_9_3 <= 1; r3786: +x_0_10_3 <= 1; r3787: +x_0_11_3 <= 1; r3788: +x_0_12_3 <= 1; r3789: +x_1_0_3 <= 1; r3790: +x_1_1_3 <= 1; r3791: +x_1_2_3 <= 1; r3792: +x_1_3_3 <= 1; r3793: +x_1_4_3 <= 1; r3794: +x_1_5_3 <= 1; r3795: +x_1_6_3 <= 1; r3796: +x_1_7_3 <= 1; r3797: +x_1_8_3 <= 1; r3798: +x_1_9_3 <= 1; r3799: +x_1_10_3 <= 1; r3800: +x_1_11_3 <= 1; r3801: +x_1_12_3 <= 1; r3802: +x_2_0_3 <= 1; r3803: +x_2_1_3 <= 1; r3804: +x_2_2_3 <= 1; r3805: +x_2_3_3 <= 1; r3806: +x_2_4_3 <= 1; r3807: +x_2_5_3 <= 1; r3808: +x_2_6_3 <= 1; r3809: +x_2_7_3 <= 1; r3810: +x_2_8_3 <= 1; r3811: +x_2_9_3 <= 1; r3812: +x_2_10_3 <= 1; r3813: +x_2_11_3 <= 1; r3814: +x_2_12_3 <= 1; r3815: +x_3_0_3 <= 1; r3816: +x_3_1_3 <= 1; r3817: +x_3_2_3 <= 1; r3818: +x_3_3_3 <= 1; r3819: +x_3_4_3 <= 1; r3820: +x_3_5_3 <= 1; r3821: +x_3_6_3 <= 1; r3822: +x_3_7_3 <= 1; r3823: +x_3_8_3 <= 1; r3824: +x_3_9_3 <= 1; r3825: +x_3_10_3 <= 1; r3826: +x_3_11_3 <= 1; r3827: +x_3_12_3 <= 1; r3828: +x_4_0_3 <= 1; r3829: +x_4_1_3 <= 1; r3830: +x_4_2_3 <= 1; r3831: +x_4_3_3 <= 1; r3832: +x_4_4_3 <= 1; r3833: +x_4_5_3 <= 1; r3834: +x_4_6_3 <= 1; r3835: +x_4_7_3 <= 1; r3836: +x_4_8_3 <= 1; r3837: +x_4_9_3 <= 1; r3838: +x_4_10_3 <= 1; r3839: +x_4_11_3 <= 1; r3840: +x_4_12_3 <= 1; r3841: +x_5_0_3 <= 1; r3842: +x_5_1_3 <= 1; r3843: +x_5_2_3 <= 1; r3844: +x_5_3_3 <= 1; r3845: +x_5_4_3 <= 1; r3846: +x_5_5_3 <= 1; r3847: +x_5_6_3 <= 1; r3848: +x_5_7_3 <= 1; r3849: +x_5_8_3 <= 1; r3850: +x_5_9_3 <= 1; r3851: +x_5_10_3 <= 1; r3852: +x_5_11_3 <= 1; r3853: +x_5_12_3 <= 1; r3854: +x_6_0_3 <= 1; r3855: +x_6_1_3 <= 1; r3856: +x_6_2_3 <= 1; r3857: +x_6_3_3 <= 1; r3858: +x_6_4_3 <= 1; r3859: +x_6_5_3 <= 1; r3860: +x_6_6_3 <= 1; r3861: +x_6_7_3 <= 1; r3862: +x_6_8_3 <= 1; r3863: +x_6_9_3 <= 1; r3864: +x_6_10_3 <= 1; r3865: +x_6_11_3 <= 1; r3866: +x_6_12_3 <= 1; r3867: +x_7_0_3 <= 1; r3868: +x_7_1_3 <= 1; r3869: +x_7_2_3 <= 1; r3870: +x_7_3_3 <= 1; r3871: +x_7_4_3 <= 1; r3872: +x_7_5_3 <= 1; r3873: +x_7_6_3 <= 1; r3874: +x_7_7_3 <= 1; r3875: +x_7_8_3 <= 1; r3876: +x_7_9_3 <= 1; r3877: +x_7_10_3 <= 1; r3878: +x_7_11_3 <= 1; r3879: +x_7_12_3 <= 1; r3880: +x_8_0_3 <= 1; r3881: +x_8_1_3 <= 1; r3882: +x_8_2_3 <= 1; r3883: +x_8_3_3 <= 1; r3884: +x_8_4_3 <= 1; r3885: +x_8_5_3 <= 1; r3886: +x_8_6_3 <= 1; r3887: +x_8_7_3 <= 1; r3888: +x_8_8_3 <= 1; r3889: +x_8_9_3 <= 1; r3890: +x_8_10_3 <= 1; r3891: +x_8_11_3 <= 1; r3892: +x_8_12_3 <= 1; r3893: +x_9_0_3 <= 1; r3894: +x_9_1_3 <= 1; r3895: +x_9_2_3 <= 1; r3896: +x_9_3_3 <= 1; r3897: +x_9_4_3 <= 1; r3898: +x_9_5_3 <= 1; r3899: +x_9_6_3 <= 1; r3900: +x_9_7_3 <= 1; r3901: +x_9_8_3 <= 1; r3902: +x_9_9_3 <= 1; r3903: +x_9_10_3 <= 1; r3904: +x_9_11_3 <= 1; r3905: +x_9_12_3 <= 1; r3906: +x_10_0_3 <= 1; r3907: +x_10_1_3 <= 1; r3908: +x_10_2_3 <= 1; r3909: +x_10_3_3 <= 1; r3910: +x_10_4_3 <= 1; r3911: +x_10_5_3 <= 1; r3912: +x_10_6_3 <= 1; r3913: +x_10_7_3 <= 1; r3914: +x_10_8_3 <= 1; r3915: +x_10_9_3 <= 1; r3916: +x_10_10_3 <= 1; r3917: +x_10_11_3 <= 1; r3918: +x_10_12_3 <= 1; r3919: +x_11_0_3 <= 1; r3920: +x_11_1_3 <= 1; r3921: +x_11_2_3 <= 1; r3922: +x_11_3_3 <= 1; r3923: +x_11_4_3 <= 1; r3924: +x_11_5_3 <= 1; r3925: +x_11_6_3 <= 1; r3926: +x_11_7_3 <= 1; r3927: +x_11_8_3 <= 1; r3928: +x_11_9_3 <= 1; r3929: +x_11_10_3 <= 1; r3930: +x_11_11_3 <= 1; r3931: +x_11_12_3 <= 1; r3932: +x_12_0_3 <= 1; r3933: +x_12_1_3 <= 1; r3934: +x_12_2_3 <= 1; r3935: +x_12_3_3 <= 1; r3936: +x_12_4_3 <= 1; r3937: +x_12_5_3 <= 1; r3938: +x_12_6_3 <= 1; r3939: +x_12_7_3 <= 1; r3940: +x_12_8_3 <= 1; r3941: +x_12_9_3 <= 1; r3942: +x_12_10_3 <= 1; r3943: +x_12_11_3 <= 1; r3944: +x_12_12_3 <= 1; r3945: +x_0_0_3 >= 0; r3946: +x_0_1_3 >= 0; r3947: +x_0_2_3 >= 0; r3948: +x_0_3_3 >= 0; r3949: +x_0_4_3 >= 0; r3950: +x_0_5_3 >= 0; r3951: +x_0_6_3 >= 0; r3952: +x_0_7_3 >= 0; r3953: +x_0_8_3 >= 0; r3954: +x_0_9_3 >= 0; r3955: +x_0_10_3 >= 0; r3956: +x_0_11_3 >= 0; r3957: +x_0_12_3 >= 0; r3958: +x_1_0_3 >= 0; r3959: +x_1_1_3 >= 0; r3960: +x_1_2_3 >= 0; r3961: +x_1_3_3 >= 0; r3962: +x_1_4_3 >= 0; r3963: +x_1_5_3 >= 0; r3964: +x_1_6_3 >= 0; r3965: +x_1_7_3 >= 0; r3966: +x_1_8_3 >= 0; r3967: +x_1_9_3 >= 0; r3968: +x_1_10_3 >= 0; r3969: +x_1_11_3 >= 0; r3970: +x_1_12_3 >= 0; r3971: +x_2_0_3 >= 0; r3972: +x_2_1_3 >= 0; r3973: +x_2_2_3 >= 0; r3974: +x_2_3_3 >= 0; r3975: +x_2_4_3 >= 0; r3976: +x_2_5_3 >= 0; r3977: +x_2_6_3 >= 0; r3978: +x_2_7_3 >= 0; r3979: +x_2_8_3 >= 0; r3980: +x_2_9_3 >= 0; r3981: +x_2_10_3 >= 0; r3982: +x_2_11_3 >= 0; r3983: +x_2_12_3 >= 0; r3984: +x_3_0_3 >= 0; r3985: +x_3_1_3 >= 0; r3986: +x_3_2_3 >= 0; r3987: +x_3_3_3 >= 0; r3988: +x_3_4_3 >= 0; r3989: +x_3_5_3 >= 0; r3990: +x_3_6_3 >= 0; r3991: +x_3_7_3 >= 0; r3992: +x_3_8_3 >= 0; r3993: +x_3_9_3 >= 0; r3994: +x_3_10_3 >= 0; r3995: +x_3_11_3 >= 0; r3996: +x_3_12_3 >= 0; r3997: +x_4_0_3 >= 0; r3998: +x_4_1_3 >= 0; r3999: +x_4_2_3 >= 0; r4000: +x_4_3_3 >= 0; r4001: +x_4_4_3 >= 0; r4002: +x_4_5_3 >= 0; r4003: +x_4_6_3 >= 0; r4004: +x_4_7_3 >= 0; r4005: +x_4_8_3 >= 0; r4006: +x_4_9_3 >= 0; r4007: +x_4_10_3 >= 0; r4008: +x_4_11_3 >= 0; r4009: +x_4_12_3 >= 0; r4010: +x_5_0_3 >= 0; r4011: +x_5_1_3 >= 0; r4012: +x_5_2_3 >= 0; r4013: +x_5_3_3 >= 0; r4014: +x_5_4_3 >= 0; r4015: +x_5_5_3 >= 0; r4016: +x_5_6_3 >= 0; r4017: +x_5_7_3 >= 0; r4018: +x_5_8_3 >= 0; r4019: +x_5_9_3 >= 0; r4020: +x_5_10_3 >= 0; r4021: +x_5_11_3 >= 0; r4022: +x_5_12_3 >= 0; r4023: +x_6_0_3 >= 0; r4024: +x_6_1_3 >= 0; r4025: +x_6_2_3 >= 0; r4026: +x_6_3_3 >= 0; r4027: +x_6_4_3 >= 0; r4028: +x_6_5_3 >= 0; r4029: +x_6_6_3 >= 0; r4030: +x_6_7_3 >= 0; r4031: +x_6_8_3 >= 0; r4032: +x_6_9_3 >= 0; r4033: +x_6_10_3 >= 0; r4034: +x_6_11_3 >= 0; r4035: +x_6_12_3 >= 0; r4036: +x_7_0_3 >= 0; r4037: +x_7_1_3 >= 0; r4038: +x_7_2_3 >= 0; r4039: +x_7_3_3 >= 0; r4040: +x_7_4_3 >= 0; r4041: +x_7_5_3 >= 0; r4042: +x_7_6_3 >= 0; r4043: +x_7_7_3 >= 0; r4044: +x_7_8_3 >= 0; r4045: +x_7_9_3 >= 0; r4046: +x_7_10_3 >= 0; r4047: +x_7_11_3 >= 0; r4048: +x_7_12_3 >= 0; r4049: +x_8_0_3 >= 0; r4050: +x_8_1_3 >= 0; r4051: +x_8_2_3 >= 0; r4052: +x_8_3_3 >= 0; r4053: +x_8_4_3 >= 0; r4054: +x_8_5_3 >= 0; r4055: +x_8_6_3 >= 0; r4056: +x_8_7_3 >= 0; r4057: +x_8_8_3 >= 0; r4058: +x_8_9_3 >= 0; r4059: +x_8_10_3 >= 0; r4060: +x_8_11_3 >= 0; r4061: +x_8_12_3 >= 0; r4062: +x_9_0_3 >= 0; r4063: +x_9_1_3 >= 0; r4064: +x_9_2_3 >= 0; r4065: +x_9_3_3 >= 0; r4066: +x_9_4_3 >= 0; r4067: +x_9_5_3 >= 0; r4068: +x_9_6_3 >= 0; r4069: +x_9_7_3 >= 0; r4070: +x_9_8_3 >= 0; r4071: +x_9_9_3 >= 0; r4072: +x_9_10_3 >= 0; r4073: +x_9_11_3 >= 0; r4074: +x_9_12_3 >= 0; r4075: +x_10_0_3 >= 0; r4076: +x_10_1_3 >= 0; r4077: +x_10_2_3 >= 0; r4078: +x_10_3_3 >= 0; r4079: +x_10_4_3 >= 0; r4080: +x_10_5_3 >= 0; r4081: +x_10_6_3 >= 0; r4082: +x_10_7_3 >= 0; r4083: +x_10_8_3 >= 0; r4084: +x_10_9_3 >= 0; r4085: +x_10_10_3 >= 0; r4086: +x_10_11_3 >= 0; r4087: +x_10_12_3 >= 0; r4088: +x_11_0_3 >= 0; r4089: +x_11_1_3 >= 0; r4090: +x_11_2_3 >= 0; r4091: +x_11_3_3 >= 0; r4092: +x_11_4_3 >= 0; r4093: +x_11_5_3 >= 0; r4094: +x_11_6_3 >= 0; r4095: +x_11_7_3 >= 0; r4096: +x_11_8_3 >= 0; r4097: +x_11_9_3 >= 0; r4098: +x_11_10_3 >= 0; r4099: +x_11_11_3 >= 0; r4100: +x_11_12_3 >= 0; r4101: +x_12_0_3 >= 0; r4102: +x_12_1_3 >= 0; r4103: +x_12_2_3 >= 0; r4104: +x_12_3_3 >= 0; r4105: +x_12_4_3 >= 0; r4106: +x_12_5_3 >= 0; r4107: +x_12_6_3 >= 0; r4108: +x_12_7_3 >= 0; r4109: +x_12_8_3 >= 0; r4110: +x_12_9_3 >= 0; r4111: +x_12_10_3 >= 0; r4112: +x_12_11_3 >= 0; r4113: +x_12_12_3 >= 0; r4114: +y_0_0 <= 1; r4115: +y_1_0 <= 1; r4116: +y_2_0 <= 1; r4117: +y_3_0 <= 1; r4118: +y_4_0 <= 1; r4119: +y_5_0 <= 1; r4120: +y_6_0 <= 1; r4121: +y_7_0 <= 1; r4122: +y_8_0 <= 1; r4123: +y_9_0 <= 1; r4124: +y_10_0 <= 1; r4125: +y_11_0 <= 1; r4126: +y_12_0 <= 1; r4127: +y_0_0 >= 0; r4128: +y_1_0 >= 0; r4129: +y_2_0 >= 0; r4130: +y_3_0 >= 0; r4131: +y_4_0 >= 0; r4132: +y_5_0 >= 0; r4133: +y_6_0 >= 0; r4134: +y_7_0 >= 0; r4135: +y_8_0 >= 0; r4136: +y_9_0 >= 0; r4137: +y_10_0 >= 0; r4138: +y_11_0 >= 0; r4139: +y_12_0 >= 0; r4140: +y_0_1 <= 1; r4141: +y_1_1 <= 1; r4142: +y_2_1 <= 1; r4143: +y_3_1 <= 1; r4144: +y_4_1 <= 1; r4145: +y_5_1 <= 1; r4146: +y_6_1 <= 1; r4147: +y_7_1 <= 1; r4148: +y_8_1 <= 1; r4149: +y_9_1 <= 1; r4150: +y_10_1 <= 1; r4151: +y_11_1 <= 1; r4152: +y_12_1 <= 1; r4153: +y_0_1 >= 0; r4154: +y_1_1 >= 0; r4155: +y_2_1 >= 0; r4156: +y_3_1 >= 0; r4157: +y_4_1 >= 0; r4158: +y_5_1 >= 0; r4159: +y_6_1 >= 0; r4160: +y_7_1 >= 0; r4161: +y_8_1 >= 0; r4162: +y_9_1 >= 0; r4163: +y_10_1 >= 0; r4164: +y_11_1 >= 0; r4165: +y_12_1 >= 0; r4166: +y_0_2 <= 1; r4167: +y_1_2 <= 1; r4168: +y_2_2 <= 1; r4169: +y_3_2 <= 1; r4170: +y_4_2 <= 1; r4171: +y_5_2 <= 1; r4172: +y_6_2 <= 1; r4173: +y_7_2 <= 1; r4174: +y_8_2 <= 1; r4175: +y_9_2 <= 1; r4176: +y_10_2 <= 1; r4177: +y_11_2 <= 1; r4178: +y_12_2 <= 1; r4179: +y_0_2 >= 0; r4180: +y_1_2 >= 0; r4181: +y_2_2 >= 0; r4182: +y_3_2 >= 0; r4183: +y_4_2 >= 0; r4184: +y_5_2 >= 0; r4185: +y_6_2 >= 0; r4186: +y_7_2 >= 0; r4187: +y_8_2 >= 0; r4188: +y_9_2 >= 0; r4189: +y_10_2 >= 0; r4190: +y_11_2 >= 0; r4191: +y_12_2 >= 0; r4192: +y_0_3 <= 1; r4193: +y_1_3 <= 1; r4194: +y_2_3 <= 1; r4195: +y_3_3 <= 1; r4196: +y_4_3 <= 1; r4197: +y_5_3 <= 1; r4198: +y_6_3 <= 1; r4199: +y_7_3 <= 1; r4200: +y_8_3 <= 1; r4201: +y_9_3 <= 1; r4202: +y_10_3 <= 1; r4203: +y_11_3 <= 1; r4204: +y_12_3 <= 1; r4205: +y_0_3 >= 0; r4206: +y_1_3 >= 0; r4207: +y_2_3 >= 0; r4208: +y_3_3 >= 0; r4209: +y_4_3 >= 0; r4210: +y_5_3 >= 0; r4211: +y_6_3 >= 0; r4212: +y_7_3 >= 0; r4213: +y_8_3 >= 0; r4214: +y_9_3 >= 0; r4215: +y_10_3 >= 0; r4216: +y_11_3 >= 0; r4217: +y_12_3 >= 0; /* Integer definitions */ int x_0_1_0,x_0_1_1,x_0_1_2,x_0_1_3,x_0_2_0,x_0_2_1,x_0_2_2,x_0_2_3,x_0_3_0,x_0_3_1,x_0_3_2,x_0_3_3,x_0_4_0,x_0_4_1,x_0_4_2,x_0_4_3,x_0_5_0,x_0_5_1,x_0_5_2,x_0_5_3,x_0_6_0,x_0_6_1,x_0_6_2,x_0_6_3,x_0_7_0,x_0_7_1,x_0_7_2,x_0_7_3,x_0_8_0,x_0_8_1,x_0_8_2,x_0_8_3,x_0_9_0,x_0_9_1,x_0_9_2,x_0_9_3,x_0_10_0,x_0_10_1,x_0_10_2,x_0_10_3,x_0_11_0,x_0_11_1,x_0_11_2,x_0_11_3,x_0_12_0,x_0_12_1,x_0_12_2,x_0_12_3,x_1_0_0,x_1_0_1,x_1_0_2,x_1_0_3,x_1_2_0,x_1_2_1,x_1_2_2,x_1_2_3,x_1_3_0,x_1_3_1,x_1_3_2,x_1_3_3,x_1_4_0,x_1_4_1,x_1_4_2,x_1_4_3,x_1_5_0,x_1_5_1,x_1_5_2,x_1_5_3,x_1_6_0,x_1_6_1,x_1_6_2,x_1_6_3,x_1_7_0,x_1_7_1,x_1_7_2,x_1_7_3,x_1_8_0,x_1_8_1,x_1_8_2,x_1_8_3,x_1_9_0,x_1_9_1,x_1_9_2,x_1_9_3,x_1_10_0,x_1_10_1,x_1_10_2,x_1_10_3,x_1_11_0,x_1_11_1,x_1_11_2,x_1_11_3,x_1_12_0,x_1_12_1,x_1_12_2,x_1_12_3,x_2_0_0,x_2_0_1,x_2_0_2,x_2_0_3,x_2_1_0,x_2_1_1,x_2_1_2,x_2_1_3,x_2_3_0,x_2_3_1,x_2_3_2,x_2_3_3,x_2_4_0,x_2_4_1,x_2_4_2,x_2_4_3,x_2_5_0,x_2_5_1,x_2_5_2,x_2_5_3,x_2_6_0,x_2_6_1,x_2_6_2,x_2_6_3,x_2_7_0,x_2_7_1,x_2_7_2,x_2_7_3,x_2_8_0,x_2_8_1,x_2_8_2,x_2_8_3,x_2_9_0,x_2_9_1,x_2_9_2,x_2_9_3,x_2_10_0,x_2_10_1,x_2_10_2,x_2_10_3,x_2_11_0,x_2_11_1,x_2_11_2,x_2_11_3,x_2_12_0,x_2_12_1,x_2_12_2,x_2_12_3,x_3_0_0,x_3_0_1,x_3_0_2,x_3_0_3,x_3_1_0,x_3_1_1,x_3_1_2,x_3_1_3,x_3_2_0,x_3_2_1,x_3_2_2,x_3_2_3,x_3_4_0,x_3_4_1,x_3_4_2,x_3_4_3,x_3_5_0,x_3_5_1,x_3_5_2,x_3_5_3,x_3_6_0,x_3_6_1,x_3_6_2,x_3_6_3,x_3_7_0,x_3_7_1,x_3_7_2,x_3_7_3,x_3_8_0,x_3_8_1,x_3_8_2,x_3_8_3,x_3_9_0,x_3_9_1,x_3_9_2,x_3_9_3,x_3_10_0,x_3_10_1,x_3_10_2,x_3_10_3,x_3_11_0,x_3_11_1,x_3_11_2,x_3_11_3,x_3_12_0,x_3_12_1,x_3_12_2,x_3_12_3,x_4_0_0,x_4_0_1,x_4_0_2,x_4_0_3,x_4_1_0,x_4_1_1,x_4_1_2,x_4_1_3,x_4_2_0,x_4_2_1,x_4_2_2,x_4_2_3,x_4_3_0,x_4_3_1,x_4_3_2,x_4_3_3,x_4_5_0,x_4_5_1,x_4_5_2,x_4_5_3,x_4_6_0,x_4_6_1,x_4_6_2,x_4_6_3,x_4_7_0,x_4_7_1,x_4_7_2,x_4_7_3,x_4_8_0,x_4_8_1,x_4_8_2,x_4_8_3,x_4_9_0,x_4_9_1,x_4_9_2,x_4_9_3,x_4_10_0,x_4_10_1,x_4_10_2,x_4_10_3,x_4_11_0,x_4_11_1,x_4_11_2,x_4_11_3,x_4_12_0,x_4_12_1,x_4_12_2,x_4_12_3,x_5_0_0,x_5_0_1,x_5_0_2,x_5_0_3,x_5_1_0,x_5_1_1,x_5_1_2,x_5_1_3,x_5_2_0,x_5_2_1,x_5_2_2,x_5_2_3,x_5_3_0,x_5_3_1,x_5_3_2,x_5_3_3,x_5_4_0,x_5_4_1,x_5_4_2,x_5_4_3,x_5_6_0,x_5_6_1,x_5_6_2,x_5_6_3,x_5_7_0,x_5_7_1,x_5_7_2,x_5_7_3,x_5_8_0,x_5_8_1,x_5_8_2,x_5_8_3,x_5_9_0,x_5_9_1,x_5_9_2,x_5_9_3,x_5_10_0,x_5_10_1,x_5_10_2,x_5_10_3,x_5_11_0,x_5_11_1,x_5_11_2,x_5_11_3,x_5_12_0,x_5_12_1,x_5_12_2,x_5_12_3,x_6_0_0,x_6_0_1,x_6_0_2,x_6_0_3,x_6_1_0,x_6_1_1,x_6_1_2,x_6_1_3,x_6_2_0,x_6_2_1,x_6_2_2,x_6_2_3,x_6_3_0,x_6_3_1,x_6_3_2,x_6_3_3,x_6_4_0,x_6_4_1,x_6_4_2,x_6_4_3,x_6_5_0,x_6_5_1,x_6_5_2,x_6_5_3,x_6_7_0,x_6_7_1,x_6_7_2,x_6_7_3,x_6_8_0,x_6_8_1,x_6_8_2,x_6_8_3,x_6_9_0,x_6_9_1,x_6_9_2,x_6_9_3,x_6_10_0,x_6_10_1,x_6_10_2,x_6_10_3,x_6_11_0,x_6_11_1,x_6_11_2,x_6_11_3,x_6_12_0,x_6_12_1,x_6_12_2,x_6_12_3,x_7_0_0,x_7_0_1,x_7_0_2,x_7_0_3,x_7_1_0,x_7_1_1,x_7_1_2,x_7_1_3,x_7_2_0,x_7_2_1,x_7_2_2,x_7_2_3,x_7_3_0,x_7_3_1,x_7_3_2,x_7_3_3,x_7_4_0,x_7_4_1,x_7_4_2,x_7_4_3,x_7_5_0,x_7_5_1,x_7_5_2,x_7_5_3,x_7_6_0,x_7_6_1,x_7_6_2,x_7_6_3,x_7_8_0,x_7_8_1,x_7_8_2,x_7_8_3,x_7_9_0,x_7_9_1,x_7_9_2,x_7_9_3,x_7_10_0,x_7_10_1,x_7_10_2,x_7_10_3,x_7_11_0,x_7_11_1,x_7_11_2,x_7_11_3,x_7_12_0,x_7_12_1,x_7_12_2,x_7_12_3,x_8_0_0,x_8_0_1,x_8_0_2,x_8_0_3,x_8_1_0,x_8_1_1,x_8_1_2,x_8_1_3,x_8_2_0,x_8_2_1,x_8_2_2,x_8_2_3,x_8_3_0,x_8_3_1,x_8_3_2,x_8_3_3,x_8_4_0,x_8_4_1,x_8_4_2,x_8_4_3,x_8_5_0,x_8_5_1,x_8_5_2,x_8_5_3,x_8_6_0,x_8_6_1,x_8_6_2,x_8_6_3,x_8_7_0,x_8_7_1,x_8_7_2,x_8_7_3,x_8_9_0,x_8_9_1,x_8_9_2,x_8_9_3,x_8_10_0,x_8_10_1,x_8_10_2,x_8_10_3,x_8_11_0,x_8_11_1,x_8_11_2,x_8_11_3,x_8_12_0,x_8_12_1,x_8_12_2,x_8_12_3,x_9_0_0,x_9_0_1,x_9_0_2,x_9_0_3,x_9_1_0,x_9_1_1,x_9_1_2,x_9_1_3,x_9_2_0,x_9_2_1,x_9_2_2,x_9_2_3,x_9_3_0,x_9_3_1,x_9_3_2,x_9_3_3,x_9_4_0,x_9_4_1,x_9_4_2,x_9_4_3,x_9_5_0,x_9_5_1,x_9_5_2,x_9_5_3,x_9_6_0,x_9_6_1,x_9_6_2,x_9_6_3,x_9_7_0,x_9_7_1,x_9_7_2,x_9_7_3,x_9_8_0,x_9_8_1,x_9_8_2,x_9_8_3,x_9_10_0,x_9_10_1,x_9_10_2,x_9_10_3,x_9_11_0,x_9_11_1,x_9_11_2,x_9_11_3,x_9_12_0,x_9_12_1,x_9_12_2,x_9_12_3,x_10_0_0,x_10_0_1,x_10_0_2,x_10_0_3,x_10_1_0,x_10_1_1,x_10_1_2,x_10_1_3,x_10_2_0,x_10_2_1,x_10_2_2,x_10_2_3,x_10_3_0,x_10_3_1,x_10_3_2,x_10_3_3,x_10_4_0,x_10_4_1,x_10_4_2,x_10_4_3,x_10_5_0,x_10_5_1,x_10_5_2,x_10_5_3,x_10_6_0,x_10_6_1,x_10_6_2,x_10_6_3,x_10_7_0,x_10_7_1,x_10_7_2,x_10_7_3,x_10_8_0,x_10_8_1,x_10_8_2,x_10_8_3,x_10_9_0,x_10_9_1,x_10_9_2,x_10_9_3,x_10_11_0,x_10_11_1,x_10_11_2,x_10_11_3,x_10_12_0,x_10_12_1,x_10_12_2,x_10_12_3,x_11_0_0,x_11_0_1,x_11_0_2,x_11_0_3,x_11_1_0,x_11_1_1,x_11_1_2,x_11_1_3,x_11_2_0,x_11_2_1,x_11_2_2,x_11_2_3,x_11_3_0,x_11_3_1,x_11_3_2,x_11_3_3,x_11_4_0,x_11_4_1,x_11_4_2,x_11_4_3,x_11_5_0,x_11_5_1,x_11_5_2,x_11_5_3,x_11_6_0,x_11_6_1,x_11_6_2,x_11_6_3,x_11_7_0,x_11_7_1,x_11_7_2,x_11_7_3,x_11_8_0,x_11_8_1,x_11_8_2,x_11_8_3,x_11_9_0,x_11_9_1,x_11_9_2,x_11_9_3,x_11_10_0,x_11_10_1,x_11_10_2,x_11_10_3,x_11_12_0,x_11_12_1,x_11_12_2,x_11_12_3,x_12_0_0,x_12_0_1,x_12_0_2,x_12_0_3,x_12_1_0,x_12_1_1,x_12_1_2,x_12_1_3,x_12_2_0,x_12_2_1,x_12_2_2,x_12_2_3,x_12_3_0,x_12_3_1,x_12_3_2,x_12_3_3,x_12_4_0,x_12_4_1,x_12_4_2,x_12_4_3,x_12_5_0,x_12_5_1,x_12_5_2,x_12_5_3,x_12_6_0,x_12_6_1,x_12_6_2,x_12_6_3,x_12_7_0,x_12_7_1,x_12_7_2,x_12_7_3,x_12_8_0,x_12_8_1,x_12_8_2,x_12_8_3,x_12_9_0,x_12_9_1,x_12_9_2,x_12_9_3,x_12_10_0,x_12_10_1,x_12_10_2,x_12_10_3,x_12_11_0,x_12_11_1,x_12_11_2,x_12_11_3,y_0_0,y_0_1,y_0_2,y_0_3,y_1_0,y_1_1,y_1_2,y_1_3,y_2_0,y_2_1,y_2_2,y_2_3,y_3_0,y_3_1,y_3_2,y_3_3,y_4_0,y_4_1,y_4_2,y_4_3,y_5_0,y_5_1,y_5_2,y_5_3,y_6_0,y_6_1,y_6_2,y_6_3,y_7_0,y_7_1,y_7_2,y_7_3,y_8_0,y_8_1,y_8_2,y_8_3,y_9_0,y_9_1,y_9_2,y_9_3,y_10_0,y_10_1,y_10_2,y_10_3,y_11_0,y_11_1,y_11_2,y_11_3,y_12_0,y_12_1,y_12_2,y_12_3;