# TIMEOUT 7200 MAIN BEGIN : [Thu Jul 6 14:04:20 2006] READ BEGIN : csp/5-FullIns_4.csp [Thu Jul 6 14:04:20 2006] READ END : csp/5-FullIns_4.csp (18 seconds) [Thu Jul 6 14:04:38 2006] READ CPU : 18.11 = 17.95 + 0.16 + 0 + 0 # BOUND : color 2 23 GENERATE_CNF 23 BEGIN : [Thu Jul 6 14:04:38 2006] GENERATE_CNF 23 END : 49938 variables 586584 clauses 12051736 bytes (26 seconds) [Thu Jul 6 14:05:04 2006] GENERATE_CNF 23 CPU : 25.67 = 25.66 + 0.01 + 0 + 0 MODIFY_CNF 12 BEGIN : [Thu Jul 6 14:05:04 2006] MODIFY_CNF 12 END : 12051741 bytes (0 seconds) [Thu Jul 6 14:05:04 2006] MODIFY_CNF 12 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 12 BEGIN : [Thu Jul 6 14:05:04 2006] CMD : minisat /tmp/csp2sat18628.cnf /tmp/csp2sat18628.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 329379 982157 | 109793 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 0 (0 /sec) decisions : 5680 (7474 /sec) propagations : 49938 (65708 /sec) conflict literals : 0 ( nan % deleted) Memory used : 24.20 MB CPU time : 0.76 s SATISFIABLE VERIFY_CNF 12 END : (1 seconds) [Thu Jul 6 14:05:05 2006] VERIFY_CNF 12 CPU : 0.909999999999998 = 0.00999999999999801 + 0.01 + 0.79 + 0.1 # RESULT : color 12 SATISFIABLE SHOW_RESULT 12 BEGIN : [Thu Jul 6 14:05:05 2006] # ASSIGN : color 12 # ASSIGN : n1 5 # ASSIGN : n2 1 # ASSIGN : n3 2 # ASSIGN : n4 2 # ASSIGN : n5 1 # ASSIGN : n6 1 # ASSIGN : n7 2 # ASSIGN : n8 2 # ASSIGN : n9 1 # ASSIGN : n10 1 # ASSIGN : n11 2 # ASSIGN : n12 2 # ASSIGN : n13 1 # ASSIGN : n14 1 # ASSIGN : n15 4 # ASSIGN : n16 5 # ASSIGN : n17 10 # ASSIGN : n18 11 # ASSIGN : n19 12 # ASSIGN : n20 1 # ASSIGN : n21 2 # ASSIGN : n22 3 # ASSIGN : n23 3 # ASSIGN : n24 3 # ASSIGN : n25 3 # ASSIGN : n26 3 # ASSIGN : n27 3 # ASSIGN : n28 3 # ASSIGN : n29 3 # ASSIGN : n30 3 # ASSIGN : n31 3 # ASSIGN : n32 3 # ASSIGN : n33 3 # ASSIGN : n34 3 # ASSIGN : n35 3 # ASSIGN : n36 3 # ASSIGN : n37 5 # ASSIGN : n38 3 # ASSIGN : n39 3 # ASSIGN : n40 3 # ASSIGN : n41 3 # ASSIGN : n42 3 # ASSIGN : n43 4 # ASSIGN : n44 4 # ASSIGN : n45 4 # ASSIGN : n46 4 # ASSIGN : n47 4 # ASSIGN : n48 4 # ASSIGN : n49 4 # ASSIGN : n50 4 # ASSIGN : n51 4 # ASSIGN : n52 4 # ASSIGN : n53 4 # ASSIGN : n54 4 # ASSIGN : n55 4 # ASSIGN : n56 4 # ASSIGN : n57 4 # ASSIGN : n58 12 # ASSIGN : n59 4 # ASSIGN : n60 4 # ASSIGN : n61 2 # ASSIGN : n62 4 # ASSIGN : n63 4 # ASSIGN : n64 1 # ASSIGN : n65 1 # ASSIGN : n66 1 # ASSIGN : n67 1 # ASSIGN : n68 1 # ASSIGN : n69 1 # ASSIGN : n70 1 # ASSIGN : n71 1 # ASSIGN : n72 1 # ASSIGN : n73 1 # ASSIGN : n74 1 # ASSIGN : n75 1 # ASSIGN : n76 1 # ASSIGN : n77 5 # ASSIGN : n78 1 # ASSIGN : n79 1 # ASSIGN : n80 1 # ASSIGN : n81 1 # ASSIGN : n82 1 # ASSIGN : n83 1 # ASSIGN : n84 1 # ASSIGN : n85 2 # ASSIGN : n86 2 # ASSIGN : n87 2 # ASSIGN : n88 2 # ASSIGN : n89 2 # ASSIGN : n90 2 # ASSIGN : n91 2 # ASSIGN : n92 2 # ASSIGN : n93 2 # ASSIGN : n94 2 # ASSIGN : n95 2 # ASSIGN : n96 2 # ASSIGN : n97 2 # ASSIGN : n98 2 # ASSIGN : n99 2 # ASSIGN : n100 2 # ASSIGN : n101 2 # ASSIGN : n102 2 # ASSIGN : n103 2 # ASSIGN : n104 2 # ASSIGN : n105 2 # ASSIGN : n106 3 # ASSIGN : n107 3 # ASSIGN : n108 3 # ASSIGN : n109 3 # ASSIGN : n110 3 # ASSIGN : n111 3 # ASSIGN : n112 3 # ASSIGN : n113 3 # ASSIGN : n114 3 # ASSIGN : n115 3 # ASSIGN : n116 3 # ASSIGN : n117 3 # ASSIGN : n118 3 # ASSIGN : n119 3 # ASSIGN : n120 3 # ASSIGN : n121 3 # ASSIGN : n122 3 # ASSIGN : n123 3 # ASSIGN : n124 3 # ASSIGN : n125 3 # ASSIGN : n126 3 # ASSIGN : n127 5 # ASSIGN : n128 5 # ASSIGN : n129 5 # ASSIGN : n130 5 # ASSIGN : n131 5 # ASSIGN : n132 5 # ASSIGN : n133 5 # ASSIGN : n134 5 # ASSIGN : n135 5 # ASSIGN : n136 5 # ASSIGN : n137 5 # ASSIGN : n138 5 # ASSIGN : n139 5 # ASSIGN : n140 5 # ASSIGN : n141 5 # ASSIGN : n142 5 # ASSIGN : n143 5 # ASSIGN : n144 5 # ASSIGN : n145 11 # ASSIGN : n146 5 # ASSIGN : n147 5 # ASSIGN : n148 10 # ASSIGN : n149 1 # ASSIGN : n150 5 # ASSIGN : n151 2 # ASSIGN : n152 3 # ASSIGN : n153 4 # ASSIGN : n154 12 # ASSIGN : n155 6 # ASSIGN : n156 6 # ASSIGN : n157 6 # ASSIGN : n158 6 # ASSIGN : n159 6 # ASSIGN : n160 6 # ASSIGN : n161 6 # ASSIGN : n162 6 # ASSIGN : n163 6 # ASSIGN : n164 6 # ASSIGN : n165 6 # ASSIGN : n166 6 # ASSIGN : n167 6 # ASSIGN : n168 6 # ASSIGN : n169 4 # ASSIGN : n170 6 # ASSIGN : n171 6 # ASSIGN : n172 6 # ASSIGN : n173 6 # ASSIGN : n174 6 # ASSIGN : n175 6 # ASSIGN : n176 6 # ASSIGN : n177 6 # ASSIGN : n178 6 # ASSIGN : n179 6 # ASSIGN : n180 6 # ASSIGN : n181 6 # ASSIGN : n182 6 # ASSIGN : n183 6 # ASSIGN : n184 6 # ASSIGN : n185 6 # ASSIGN : n186 6 # ASSIGN : n187 12 # ASSIGN : n188 6 # ASSIGN : n189 6 # ASSIGN : n190 6 # ASSIGN : n191 6 # ASSIGN : n192 6 # ASSIGN : n193 6 # ASSIGN : n194 6 # ASSIGN : n195 6 # ASSIGN : n196 6 # ASSIGN : n197 6 # ASSIGN : n198 6 # ASSIGN : n199 6 # ASSIGN : n200 6 # ASSIGN : n201 6 # ASSIGN : n202 6 # ASSIGN : n203 4 # ASSIGN : n204 6 # ASSIGN : n205 6 # ASSIGN : n206 6 # ASSIGN : n207 6 # ASSIGN : n208 6 # ASSIGN : n209 6 # ASSIGN : n210 6 # ASSIGN : n211 6 # ASSIGN : n212 6 # ASSIGN : n213 6 # ASSIGN : n214 6 # ASSIGN : n215 6 # ASSIGN : n216 6 # ASSIGN : n217 6 # ASSIGN : n218 6 # ASSIGN : n219 6 # ASSIGN : n220 6 # ASSIGN : n221 6 # ASSIGN : n222 6 # ASSIGN : n223 6 # ASSIGN : n224 6 # ASSIGN : n225 6 # ASSIGN : n226 6 # ASSIGN : n227 6 # ASSIGN : n228 6 # ASSIGN : n229 6 # ASSIGN : n230 6 # ASSIGN : n231 6 # ASSIGN : n232 6 # ASSIGN : n233 6 # ASSIGN : n234 6 # ASSIGN : n235 6 # ASSIGN : n236 6 # ASSIGN : n237 6 # ASSIGN : n238 6 # ASSIGN : n239 6 # ASSIGN : n240 6 # ASSIGN : n241 6 # ASSIGN : n242 6 # ASSIGN : n243 6 # ASSIGN : n244 6 # ASSIGN : n245 6 # ASSIGN : n246 6 # ASSIGN : n247 6 # ASSIGN : n248 6 # ASSIGN : n249 6 # ASSIGN : n250 6 # ASSIGN : n251 6 # ASSIGN : n252 6 # ASSIGN : n253 6 # ASSIGN : n254 6 # ASSIGN : n255 6 # ASSIGN : n256 6 # ASSIGN : n257 6 # ASSIGN : n258 6 # ASSIGN : n259 6 # ASSIGN : n260 6 # ASSIGN : n261 6 # ASSIGN : n262 6 # ASSIGN : n263 6 # ASSIGN : n264 6 # ASSIGN : n265 6 # ASSIGN : n266 6 # ASSIGN : n267 6 # ASSIGN : n268 6 # ASSIGN : n269 6 # ASSIGN : n270 6 # ASSIGN : n271 6 # ASSIGN : n272 6 # ASSIGN : n273 6 # ASSIGN : n274 6 # ASSIGN : n275 6 # ASSIGN : n276 6 # ASSIGN : n277 12 # ASSIGN : n278 6 # ASSIGN : n279 6 # ASSIGN : n280 6 # ASSIGN : n281 6 # ASSIGN : n282 6 # ASSIGN : n283 6 # ASSIGN : n284 6 # ASSIGN : n285 6 # ASSIGN : n286 6 # ASSIGN : n287 6 # ASSIGN : n288 6 # ASSIGN : n289 6 # ASSIGN : n290 6 # ASSIGN : n291 6 # ASSIGN : n292 6 # ASSIGN : n293 6 # ASSIGN : n294 6 # ASSIGN : n295 6 # ASSIGN : n296 6 # ASSIGN : n297 6 # ASSIGN : n298 6 # ASSIGN : n299 6 # ASSIGN : n300 6 # ASSIGN : n301 6 # ASSIGN : n302 6 # ASSIGN : n303 6 # ASSIGN : n304 6 # ASSIGN : n305 6 # ASSIGN : n306 6 # ASSIGN : n307 6 # ASSIGN : n308 6 # ASSIGN : n309 1 # ASSIGN : n310 1 # ASSIGN : n311 1 # ASSIGN : n312 1 # ASSIGN : n313 1 # ASSIGN : n314 1 # ASSIGN : n315 1 # ASSIGN : n316 1 # ASSIGN : n317 1 # ASSIGN : n318 1 # ASSIGN : n319 7 # ASSIGN : n320 1 # ASSIGN : n321 1 # ASSIGN : n322 1 # ASSIGN : n323 1 # ASSIGN : n324 1 # ASSIGN : n325 1 # ASSIGN : n326 1 # ASSIGN : n327 1 # ASSIGN : n328 1 # ASSIGN : n329 1 # ASSIGN : n330 1 # ASSIGN : n331 1 # ASSIGN : n332 1 # ASSIGN : n333 1 # ASSIGN : n334 1 # ASSIGN : n335 1 # ASSIGN : n336 1 # ASSIGN : n337 1 # ASSIGN : n338 12 # ASSIGN : n339 1 # ASSIGN : n340 1 # ASSIGN : n341 1 # ASSIGN : n342 12 # ASSIGN : n343 7 # ASSIGN : n344 1 # ASSIGN : n345 1 # ASSIGN : n346 1 # ASSIGN : n347 1 # ASSIGN : n348 1 # ASSIGN : n349 1 # ASSIGN : n350 1 # ASSIGN : n351 1 # ASSIGN : n352 1 # ASSIGN : n353 1 # ASSIGN : n354 1 # ASSIGN : n355 1 # ASSIGN : n356 1 # ASSIGN : n357 1 # ASSIGN : n358 1 # ASSIGN : n359 1 # ASSIGN : n360 1 # ASSIGN : n361 1 # ASSIGN : n362 1 # ASSIGN : n363 1 # ASSIGN : n364 1 # ASSIGN : n365 7 # ASSIGN : n366 1 # ASSIGN : n367 1 # ASSIGN : n368 1 # ASSIGN : n369 1 # ASSIGN : n370 1 # ASSIGN : n371 1 # ASSIGN : n372 1 # ASSIGN : n373 1 # ASSIGN : n374 1 # ASSIGN : n375 1 # ASSIGN : n376 1 # ASSIGN : n377 1 # ASSIGN : n378 1 # ASSIGN : n379 1 # ASSIGN : n380 1 # ASSIGN : n381 1 # ASSIGN : n382 1 # ASSIGN : n383 1 # ASSIGN : n384 1 # ASSIGN : n385 1 # ASSIGN : n386 1 # ASSIGN : n387 1 # ASSIGN : n388 1 # ASSIGN : n389 1 # ASSIGN : n390 1 # ASSIGN : n391 1 # ASSIGN : n392 1 # ASSIGN : n393 1 # ASSIGN : n394 1 # ASSIGN : n395 1 # ASSIGN : n396 1 # ASSIGN : n397 1 # ASSIGN : n398 1 # ASSIGN : n399 1 # ASSIGN : n400 1 # ASSIGN : n401 1 # ASSIGN : n402 1 # ASSIGN : n403 1 # ASSIGN : n404 1 # ASSIGN : n405 1 # ASSIGN : n406 1 # ASSIGN : n407 7 # ASSIGN : n408 1 # ASSIGN : n409 1 # ASSIGN : n410 1 # ASSIGN : n411 1 # ASSIGN : n412 1 # ASSIGN : n413 1 # ASSIGN : n414 1 # ASSIGN : n415 1 # ASSIGN : n416 1 # ASSIGN : n417 1 # ASSIGN : n418 1 # ASSIGN : n419 1 # ASSIGN : n420 1 # ASSIGN : n421 1 # ASSIGN : n422 1 # ASSIGN : n423 1 # ASSIGN : n424 1 # ASSIGN : n425 1 # ASSIGN : n426 1 # ASSIGN : n427 1 # ASSIGN : n428 1 # ASSIGN : n429 1 # ASSIGN : n430 1 # ASSIGN : n431 1 # ASSIGN : n432 1 # ASSIGN : n433 1 # ASSIGN : n434 1 # ASSIGN : n435 1 # ASSIGN : n436 1 # ASSIGN : n437 1 # ASSIGN : n438 1 # ASSIGN : n439 1 # ASSIGN : n440 1 # ASSIGN : n441 1 # ASSIGN : n442 1 # ASSIGN : n443 1 # ASSIGN : n444 1 # ASSIGN : n445 1 # ASSIGN : n446 1 # ASSIGN : n447 1 # ASSIGN : n448 1 # ASSIGN : n449 1 # ASSIGN : n450 1 # ASSIGN : n451 1 # ASSIGN : n452 1 # ASSIGN : n453 1 # ASSIGN : n454 1 # ASSIGN : n455 1 # ASSIGN : n456 1 # ASSIGN : n457 1 # ASSIGN : n458 1 # ASSIGN : n459 1 # ASSIGN : n460 1 # ASSIGN : n461 1 # ASSIGN : n462 1 # ASSIGN : n463 2 # ASSIGN : n464 2 # ASSIGN : n465 2 # ASSIGN : n466 2 # ASSIGN : n467 2 # ASSIGN : n468 2 # ASSIGN : n469 2 # ASSIGN : n470 2 # ASSIGN : n471 2 # ASSIGN : n472 2 # ASSIGN : n473 2 # ASSIGN : n474 2 # ASSIGN : n475 2 # ASSIGN : n476 2 # ASSIGN : n477 2 # ASSIGN : n478 2 # ASSIGN : n479 2 # ASSIGN : n480 2 # ASSIGN : n481 2 # ASSIGN : n482 2 # ASSIGN : n483 2 # ASSIGN : n484 2 # ASSIGN : n485 2 # ASSIGN : n486 2 # ASSIGN : n487 2 # ASSIGN : n488 2 # ASSIGN : n489 2 # ASSIGN : n490 2 # ASSIGN : n491 2 # ASSIGN : n492 2 # ASSIGN : n493 2 # ASSIGN : n494 2 # ASSIGN : n495 2 # ASSIGN : n496 2 # ASSIGN : n497 2 # ASSIGN : n498 2 # ASSIGN : n499 2 # ASSIGN : n500 2 # ASSIGN : n501 2 # ASSIGN : n502 2 # ASSIGN : n503 2 # ASSIGN : n504 2 # ASSIGN : n505 2 # ASSIGN : n506 2 # ASSIGN : n507 2 # ASSIGN : n508 2 # ASSIGN : n509 2 # ASSIGN : n510 2 # ASSIGN : n511 2 # ASSIGN : n512 2 # ASSIGN : n513 2 # ASSIGN : n514 2 # ASSIGN : n515 2 # ASSIGN : n516 2 # ASSIGN : n517 2 # ASSIGN : n518 8 # ASSIGN : n519 2 # ASSIGN : n520 2 # ASSIGN : n521 2 # ASSIGN : n522 8 # ASSIGN : n523 2 # ASSIGN : n524 2 # ASSIGN : n525 2 # ASSIGN : n526 2 # ASSIGN : n527 2 # ASSIGN : n528 2 # ASSIGN : n529 2 # ASSIGN : n530 2 # ASSIGN : n531 2 # ASSIGN : n532 2 # ASSIGN : n533 2 # ASSIGN : n534 2 # ASSIGN : n535 2 # ASSIGN : n536 8 # ASSIGN : n537 2 # ASSIGN : n538 2 # ASSIGN : n539 2 # ASSIGN : n540 2 # ASSIGN : n541 2 # ASSIGN : n542 2 # ASSIGN : n543 2 # ASSIGN : n544 2 # ASSIGN : n545 2 # ASSIGN : n546 2 # ASSIGN : n547 2 # ASSIGN : n548 2 # ASSIGN : n549 2 # ASSIGN : n550 2 # ASSIGN : n551 2 # ASSIGN : n552 2 # ASSIGN : n553 2 # ASSIGN : n554 2 # ASSIGN : n555 2 # ASSIGN : n556 2 # ASSIGN : n557 2 # ASSIGN : n558 2 # ASSIGN : n559 2 # ASSIGN : n560 2 # ASSIGN : n561 2 # ASSIGN : n562 2 # ASSIGN : n563 2 # ASSIGN : n564 2 # ASSIGN : n565 2 # ASSIGN : n566 2 # ASSIGN : n567 2 # ASSIGN : n568 2 # ASSIGN : n569 2 # ASSIGN : n570 2 # ASSIGN : n571 2 # ASSIGN : n572 2 # ASSIGN : n573 2 # ASSIGN : n574 2 # ASSIGN : n575 2 # ASSIGN : n576 2 # ASSIGN : n577 2 # ASSIGN : n578 2 # ASSIGN : n579 2 # ASSIGN : n580 2 # ASSIGN : n581 2 # ASSIGN : n582 2 # ASSIGN : n583 2 # ASSIGN : n584 2 # ASSIGN : n585 2 # ASSIGN : n586 2 # ASSIGN : n587 2 # ASSIGN : n588 2 # ASSIGN : n589 2 # ASSIGN : n590 2 # ASSIGN : n591 2 # ASSIGN : n592 2 # ASSIGN : n593 2 # ASSIGN : n594 2 # ASSIGN : n595 2 # ASSIGN : n596 2 # ASSIGN : n597 2 # ASSIGN : n598 2 # ASSIGN : n599 2 # ASSIGN : n600 2 # ASSIGN : n601 2 # ASSIGN : n602 2 # ASSIGN : n603 2 # ASSIGN : n604 2 # ASSIGN : n605 2 # ASSIGN : n606 2 # ASSIGN : n607 8 # ASSIGN : n608 2 # ASSIGN : n609 12 # ASSIGN : n610 2 # ASSIGN : n611 2 # ASSIGN : n612 2 # ASSIGN : n613 2 # ASSIGN : n614 2 # ASSIGN : n615 2 # ASSIGN : n616 12 # ASSIGN : n617 3 # ASSIGN : n618 12 # ASSIGN : n619 3 # ASSIGN : n620 3 # ASSIGN : n621 3 # ASSIGN : n622 3 # ASSIGN : n623 3 # ASSIGN : n624 3 # ASSIGN : n625 3 # ASSIGN : n626 3 # ASSIGN : n627 3 # ASSIGN : n628 3 # ASSIGN : n629 3 # ASSIGN : n630 3 # ASSIGN : n631 3 # ASSIGN : n632 3 # ASSIGN : n633 3 # ASSIGN : n634 3 # ASSIGN : n635 3 # ASSIGN : n636 3 # ASSIGN : n637 3 # ASSIGN : n638 3 # ASSIGN : n639 3 # ASSIGN : n640 3 # ASSIGN : n641 3 # ASSIGN : n642 3 # ASSIGN : n643 3 # ASSIGN : n644 3 # ASSIGN : n645 3 # ASSIGN : n646 3 # ASSIGN : n647 3 # ASSIGN : n648 3 # ASSIGN : n649 3 # ASSIGN : n650 3 # ASSIGN : n651 3 # ASSIGN : n652 3 # ASSIGN : n653 3 # ASSIGN : n654 3 # ASSIGN : n655 3 # ASSIGN : n656 3 # ASSIGN : n657 3 # ASSIGN : n658 3 # ASSIGN : n659 3 # ASSIGN : n660 3 # ASSIGN : n661 1 # ASSIGN : n662 1 # ASSIGN : n663 3 # ASSIGN : n664 3 # ASSIGN : n665 3 # ASSIGN : n666 3 # ASSIGN : n667 3 # ASSIGN : n668 3 # ASSIGN : n669 3 # ASSIGN : n670 3 # ASSIGN : n671 3 # ASSIGN : n672 3 # ASSIGN : n673 1 # ASSIGN : n674 3 # ASSIGN : n675 1 # ASSIGN : n676 1 # ASSIGN : n677 1 # ASSIGN : n678 1 # ASSIGN : n679 1 # ASSIGN : n680 3 # ASSIGN : n681 3 # ASSIGN : n682 3 # ASSIGN : n683 3 # ASSIGN : n684 3 # ASSIGN : n685 3 # ASSIGN : n686 3 # ASSIGN : n687 3 # ASSIGN : n688 3 # ASSIGN : n689 3 # ASSIGN : n690 3 # ASSIGN : n691 3 # ASSIGN : n692 3 # ASSIGN : n693 3 # ASSIGN : n694 3 # ASSIGN : n695 3 # ASSIGN : n696 3 # ASSIGN : n697 3 # ASSIGN : n698 3 # ASSIGN : n699 3 # ASSIGN : n700 3 # ASSIGN : n701 3 # ASSIGN : n702 3 # ASSIGN : n703 1 # ASSIGN : n704 1 # ASSIGN : n705 3 # ASSIGN : n706 3 # ASSIGN : n707 3 # ASSIGN : n708 3 # ASSIGN : n709 3 # ASSIGN : n710 3 # ASSIGN : n711 12 # ASSIGN : n712 3 # ASSIGN : n713 3 # ASSIGN : n714 3 # ASSIGN : n715 1 # ASSIGN : n716 3 # ASSIGN : n717 1 # ASSIGN : n718 1 # ASSIGN : n719 3 # ASSIGN : n720 1 # ASSIGN : n721 1 # ASSIGN : n722 3 # ASSIGN : n723 3 # ASSIGN : n724 3 # ASSIGN : n725 3 # ASSIGN : n726 3 # ASSIGN : n727 3 # ASSIGN : n728 3 # ASSIGN : n729 3 # ASSIGN : n730 3 # ASSIGN : n731 3 # ASSIGN : n732 3 # ASSIGN : n733 3 # ASSIGN : n734 3 # ASSIGN : n735 3 # ASSIGN : n736 3 # ASSIGN : n737 3 # ASSIGN : n738 3 # ASSIGN : n739 3 # ASSIGN : n740 3 # ASSIGN : n741 3 # ASSIGN : n742 3 # ASSIGN : n743 3 # ASSIGN : n744 3 # ASSIGN : n745 3 # ASSIGN : n746 3 # ASSIGN : n747 3 # ASSIGN : n748 3 # ASSIGN : n749 3 # ASSIGN : n750 3 # ASSIGN : n751 3 # ASSIGN : n752 3 # ASSIGN : n753 3 # ASSIGN : n754 3 # ASSIGN : n755 3 # ASSIGN : n756 3 # ASSIGN : n757 3 # ASSIGN : n758 3 # ASSIGN : n759 3 # ASSIGN : n760 3 # ASSIGN : n761 3 # ASSIGN : n762 3 # ASSIGN : n763 3 # ASSIGN : n764 3 # ASSIGN : n765 3 # ASSIGN : n766 3 # ASSIGN : n767 1 # ASSIGN : n768 3 # ASSIGN : n769 3 # ASSIGN : n770 3 # ASSIGN : n771 4 # ASSIGN : n772 4 # ASSIGN : n773 4 # ASSIGN : n774 4 # ASSIGN : n775 4 # ASSIGN : n776 4 # ASSIGN : n777 4 # ASSIGN : n778 4 # ASSIGN : n779 4 # ASSIGN : n780 4 # ASSIGN : n781 4 # ASSIGN : n782 4 # ASSIGN : n783 4 # ASSIGN : n784 4 # ASSIGN : n785 4 # ASSIGN : n786 4 # ASSIGN : n787 4 # ASSIGN : n788 4 # ASSIGN : n789 4 # ASSIGN : n790 4 # ASSIGN : n791 4 # ASSIGN : n792 10 # ASSIGN : n793 4 # ASSIGN : n794 4 # ASSIGN : n795 4 # ASSIGN : n796 4 # ASSIGN : n797 4 # ASSIGN : n798 4 # ASSIGN : n799 4 # ASSIGN : n800 4 # ASSIGN : n801 4 # ASSIGN : n802 4 # ASSIGN : n803 4 # ASSIGN : n804 4 # ASSIGN : n805 4 # ASSIGN : n806 4 # ASSIGN : n807 4 # ASSIGN : n808 4 # ASSIGN : n809 4 # ASSIGN : n810 4 # ASSIGN : n811 4 # ASSIGN : n812 4 # ASSIGN : n813 4 # ASSIGN : n814 4 # ASSIGN : n815 4 # ASSIGN : n816 4 # ASSIGN : n817 4 # ASSIGN : n818 4 # ASSIGN : n819 4 # ASSIGN : n820 4 # ASSIGN : n821 4 # ASSIGN : n822 4 # ASSIGN : n823 4 # ASSIGN : n824 4 # ASSIGN : n825 4 # ASSIGN : n826 4 # ASSIGN : n827 4 # ASSIGN : n828 4 # ASSIGN : n829 4 # ASSIGN : n830 4 # ASSIGN : n831 4 # ASSIGN : n832 4 # ASSIGN : n833 4 # ASSIGN : n834 4 # ASSIGN : n835 4 # ASSIGN : n836 4 # ASSIGN : n837 4 # ASSIGN : n838 4 # ASSIGN : n839 4 # ASSIGN : n840 4 # ASSIGN : n841 4 # ASSIGN : n842 4 # ASSIGN : n843 4 # ASSIGN : n844 4 # ASSIGN : n845 4 # ASSIGN : n846 4 # ASSIGN : n847 4 # ASSIGN : n848 4 # ASSIGN : n849 2 # ASSIGN : n850 4 # ASSIGN : n851 4 # ASSIGN : n852 4 # ASSIGN : n853 4 # ASSIGN : n854 4 # ASSIGN : n855 4 # ASSIGN : n856 4 # ASSIGN : n857 4 # ASSIGN : n858 4 # ASSIGN : n859 4 # ASSIGN : n860 4 # ASSIGN : n861 4 # ASSIGN : n862 4 # ASSIGN : n863 4 # ASSIGN : n864 4 # ASSIGN : n865 4 # ASSIGN : n866 4 # ASSIGN : n867 4 # ASSIGN : n868 4 # ASSIGN : n869 4 # ASSIGN : n870 4 # ASSIGN : n871 4 # ASSIGN : n872 4 # ASSIGN : n873 4 # ASSIGN : n874 4 # ASSIGN : n875 4 # ASSIGN : n876 4 # ASSIGN : n877 4 # ASSIGN : n878 4 # ASSIGN : n879 4 # ASSIGN : n880 4 # ASSIGN : n881 4 # ASSIGN : n882 4 # ASSIGN : n883 4 # ASSIGN : n884 4 # ASSIGN : n885 4 # ASSIGN : n886 4 # ASSIGN : n887 4 # ASSIGN : n888 4 # ASSIGN : n889 4 # ASSIGN : n890 4 # ASSIGN : n891 4 # ASSIGN : n892 4 # ASSIGN : n893 4 # ASSIGN : n894 4 # ASSIGN : n895 4 # ASSIGN : n896 4 # ASSIGN : n897 4 # ASSIGN : n898 4 # ASSIGN : n899 4 # ASSIGN : n900 4 # ASSIGN : n901 4 # ASSIGN : n902 4 # ASSIGN : n903 4 # ASSIGN : n904 4 # ASSIGN : n905 4 # ASSIGN : n906 4 # ASSIGN : n907 4 # ASSIGN : n908 4 # ASSIGN : n909 4 # ASSIGN : n910 4 # ASSIGN : n911 4 # ASSIGN : n912 4 # ASSIGN : n913 4 # ASSIGN : n914 4 # ASSIGN : n915 4 # ASSIGN : n916 4 # ASSIGN : n917 4 # ASSIGN : n918 4 # ASSIGN : n919 4 # ASSIGN : n920 4 # ASSIGN : n921 4 # ASSIGN : n922 4 # ASSIGN : n923 4 # ASSIGN : n924 4 # ASSIGN : n925 5 # ASSIGN : n926 5 # ASSIGN : n927 5 # ASSIGN : n928 5 # ASSIGN : n929 5 # ASSIGN : n930 5 # ASSIGN : n931 5 # ASSIGN : n932 5 # ASSIGN : n933 5 # ASSIGN : n934 5 # ASSIGN : n935 5 # ASSIGN : n936 5 # ASSIGN : n937 5 # ASSIGN : n938 5 # ASSIGN : n939 5 # ASSIGN : n940 5 # ASSIGN : n941 5 # ASSIGN : n942 5 # ASSIGN : n943 5 # ASSIGN : n944 5 # ASSIGN : n945 5 # ASSIGN : n946 5 # ASSIGN : n947 5 # ASSIGN : n948 5 # ASSIGN : n949 5 # ASSIGN : n950 5 # ASSIGN : n951 5 # ASSIGN : n952 5 # ASSIGN : n953 5 # ASSIGN : n954 5 # ASSIGN : n955 5 # ASSIGN : n956 5 # ASSIGN : n957 5 # ASSIGN : n958 5 # ASSIGN : n959 5 # ASSIGN : n960 5 # ASSIGN : n961 5 # ASSIGN : n962 5 # ASSIGN : n963 5 # ASSIGN : n964 5 # ASSIGN : n965 5 # ASSIGN : n966 5 # ASSIGN : n967 5 # ASSIGN : n968 5 # ASSIGN : n969 5 # ASSIGN : n970 5 # ASSIGN : n971 5 # ASSIGN : n972 5 # ASSIGN : n973 5 # ASSIGN : n974 5 # ASSIGN : n975 5 # ASSIGN : n976 5 # ASSIGN : n977 5 # ASSIGN : n978 5 # ASSIGN : n979 5 # ASSIGN : n980 5 # ASSIGN : n981 5 # ASSIGN : n982 5 # ASSIGN : n983 5 # ASSIGN : n984 5 # ASSIGN : n985 5 # ASSIGN : n986 5 # ASSIGN : n987 5 # ASSIGN : n988 5 # ASSIGN : n989 5 # ASSIGN : n990 5 # ASSIGN : n991 5 # ASSIGN : n992 5 # ASSIGN : n993 5 # ASSIGN : n994 5 # ASSIGN : n995 5 # ASSIGN : n996 5 # ASSIGN : n997 5 # ASSIGN : n998 5 # ASSIGN : n999 5 # ASSIGN : n1000 5 # ASSIGN : n1001 5 # ASSIGN : n1002 5 # ASSIGN : n1003 5 # ASSIGN : n1004 5 # ASSIGN : n1005 5 # ASSIGN : n1006 5 # ASSIGN : n1007 5 # ASSIGN : n1008 5 # ASSIGN : n1009 5 # ASSIGN : n1010 5 # ASSIGN : n1011 5 # ASSIGN : n1012 5 # ASSIGN : n1013 5 # ASSIGN : n1014 5 # ASSIGN : n1015 5 # ASSIGN : n1016 5 # ASSIGN : n1017 5 # ASSIGN : n1018 5 # ASSIGN : n1019 5 # ASSIGN : n1020 5 # ASSIGN : n1021 5 # ASSIGN : n1022 5 # ASSIGN : n1023 5 # ASSIGN : n1024 5 # ASSIGN : n1025 5 # ASSIGN : n1026 5 # ASSIGN : n1027 5 # ASSIGN : n1028 5 # ASSIGN : n1029 5 # ASSIGN : n1030 5 # ASSIGN : n1031 5 # ASSIGN : n1032 5 # ASSIGN : n1033 5 # ASSIGN : n1034 5 # ASSIGN : n1035 5 # ASSIGN : n1036 5 # ASSIGN : n1037 5 # ASSIGN : n1038 5 # ASSIGN : n1039 5 # ASSIGN : n1040 5 # ASSIGN : n1041 5 # ASSIGN : n1042 5 # ASSIGN : n1043 5 # ASSIGN : n1044 5 # ASSIGN : n1045 5 # ASSIGN : n1046 5 # ASSIGN : n1047 5 # ASSIGN : n1048 5 # ASSIGN : n1049 5 # ASSIGN : n1050 5 # ASSIGN : n1051 5 # ASSIGN : n1052 5 # ASSIGN : n1053 5 # ASSIGN : n1054 5 # ASSIGN : n1055 5 # ASSIGN : n1056 5 # ASSIGN : n1057 5 # ASSIGN : n1058 5 # ASSIGN : n1059 5 # ASSIGN : n1060 5 # ASSIGN : n1061 5 # ASSIGN : n1062 5 # ASSIGN : n1063 5 # ASSIGN : n1064 5 # ASSIGN : n1065 5 # ASSIGN : n1066 5 # ASSIGN : n1067 5 # ASSIGN : n1068 5 # ASSIGN : n1069 5 # ASSIGN : n1070 5 # ASSIGN : n1071 5 # ASSIGN : n1072 5 # ASSIGN : n1073 5 # ASSIGN : n1074 5 # ASSIGN : n1075 5 # ASSIGN : n1076 5 # ASSIGN : n1077 5 # ASSIGN : n1078 5 # ASSIGN : n1079 6 # ASSIGN : n1080 7 # ASSIGN : n1081 8 # ASSIGN : n1082 9 # ASSIGN : n1083 10 # ASSIGN : n1084 11 # ASSIGN : n1085 12 SHOW_RESULT 12 END : 12 (0 seconds) [Thu Jul 6 14:05:05 2006] SHOW_RESULT 12 CPU : 0.0899999999999963 = 0.0899999999999963 + 0 + 0 + 0 # BOUND : color 2 12 MODIFY_CNF 7 BEGIN : [Thu Jul 6 14:05:05 2006] MODIFY_CNF 7 END : 12051740 bytes (0 seconds) [Thu Jul 6 14:05:05 2006] MODIFY_CNF 7 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 7 BEGIN : [Thu Jul 6 14:05:05 2006] CMD : minisat /tmp/csp2sat18628.cnf /tmp/csp2sat18628.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 215429 640307 | 71809 0 0 nan | 0.000 % | | 100 | 215429 640307 | 78989 100 821 8.2 | 41.317 % | | 250 | 215429 640307 | 86888 250 2656 10.6 | 41.317 % | | 476 | 215429 640307 | 95577 476 4798 10.1 | 41.317 % | | 814 | 215429 640307 | 105135 814 8269 10.2 | 41.317 % | | 1320 | 215429 640307 | 115649 1320 14151 10.7 | 41.317 % | | 2081 | 215429 640307 | 127214 2081 21930 10.5 | 41.317 % | | 3222 | 215429 640307 | 139935 3222 32664 10.1 | 41.317 % | ============================================================================== restarts : 8 conflicts : 4239 (2255 /sec) decisions : 10146 (5397 /sec) propagations : 1037118 (551659 /sec) conflict literals : 40249 (12.52 % deleted) Memory used : 24.03 MB CPU time : 1.88 s UNSATISFIABLE VERIFY_CNF 7 END : (2 seconds) [Thu Jul 6 14:05:07 2006] VERIFY_CNF 7 CPU : 1.96 = 0 + 0.00999999999999998 + 1.88 + 0.07 # RESULT : color 7 UNSATISFIABLE # BOUND : color 8 12 MODIFY_CNF 10 BEGIN : [Thu Jul 6 14:05:07 2006] MODIFY_CNF 10 END : 12051741 bytes (0 seconds) [Thu Jul 6 14:05:07 2006] MODIFY_CNF 10 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 10 BEGIN : [Thu Jul 6 14:05:07 2006] CMD : minisat /tmp/csp2sat18628.cnf /tmp/csp2sat18628.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 283799 845417 | 94599 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 0 (0 /sec) decisions : 4969 (5778 /sec) propagations : 49938 (58067 /sec) conflict literals : 0 ( nan % deleted) Memory used : 24.20 MB CPU time : 0.86 s SATISFIABLE VERIFY_CNF 10 END : (1 seconds) [Thu Jul 6 14:05:08 2006] VERIFY_CNF 10 CPU : 0.97 = 0 + 0 + 0.88 + 0.09 # RESULT : color 10 SATISFIABLE SHOW_RESULT 10 BEGIN : [Thu Jul 6 14:05:08 2006] # ASSIGN : color 10 # ASSIGN : n1 10 # ASSIGN : n2 1 # ASSIGN : n3 2 # ASSIGN : n4 1 # ASSIGN : n5 3 # ASSIGN : n6 3 # ASSIGN : n7 1 # ASSIGN : n8 1 # ASSIGN : n9 3 # ASSIGN : n10 3 # ASSIGN : n11 1 # ASSIGN : n12 1 # ASSIGN : n13 3 # ASSIGN : n14 3 # ASSIGN : n15 8 # ASSIGN : n16 9 # ASSIGN : n17 10 # ASSIGN : n18 5 # ASSIGN : n19 6 # ASSIGN : n20 3 # ASSIGN : n21 1 # ASSIGN : n22 2 # ASSIGN : n23 3 # ASSIGN : n24 2 # ASSIGN : n25 2 # ASSIGN : n26 2 # ASSIGN : n27 3 # ASSIGN : n28 2 # ASSIGN : n29 2 # ASSIGN : n30 2 # ASSIGN : n31 2 # ASSIGN : n32 2 # ASSIGN : n33 2 # ASSIGN : n34 2 # ASSIGN : n35 2 # ASSIGN : n36 2 # ASSIGN : n37 7 # ASSIGN : n38 2 # ASSIGN : n39 2 # ASSIGN : n40 2 # ASSIGN : n41 2 # ASSIGN : n42 7 # ASSIGN : n43 1 # ASSIGN : n44 3 # ASSIGN : n45 1 # ASSIGN : n46 3 # ASSIGN : n47 3 # ASSIGN : n48 3 # ASSIGN : n49 1 # ASSIGN : n50 1 # ASSIGN : n51 1 # ASSIGN : n52 3 # ASSIGN : n53 1 # ASSIGN : n54 1 # ASSIGN : n55 1 # ASSIGN : n56 1 # ASSIGN : n57 3 # ASSIGN : n58 8 # ASSIGN : n59 1 # ASSIGN : n60 3 # ASSIGN : n61 3 # ASSIGN : n62 3 # ASSIGN : n63 3 # ASSIGN : n64 1 # ASSIGN : n65 2 # ASSIGN : n66 1 # ASSIGN : n67 2 # ASSIGN : n68 2 # ASSIGN : n69 2 # ASSIGN : n70 1 # ASSIGN : n71 2 # ASSIGN : n72 2 # ASSIGN : n73 2 # ASSIGN : n74 2 # ASSIGN : n75 2 # ASSIGN : n76 2 # ASSIGN : n77 10 # ASSIGN : n78 2 # ASSIGN : n79 2 # ASSIGN : n80 1 # ASSIGN : n81 2 # ASSIGN : n82 2 # ASSIGN : n83 2 # ASSIGN : n84 2 # ASSIGN : n85 3 # ASSIGN : n86 3 # ASSIGN : n87 3 # ASSIGN : n88 3 # ASSIGN : n89 3 # ASSIGN : n90 3 # ASSIGN : n91 3 # ASSIGN : n92 3 # ASSIGN : n93 3 # ASSIGN : n94 3 # ASSIGN : n95 3 # ASSIGN : n96 3 # ASSIGN : n97 3 # ASSIGN : n98 3 # ASSIGN : n99 3 # ASSIGN : n100 3 # ASSIGN : n101 3 # ASSIGN : n102 3 # ASSIGN : n103 3 # ASSIGN : n104 3 # ASSIGN : n105 3 # ASSIGN : n106 1 # ASSIGN : n107 1 # ASSIGN : n108 1 # ASSIGN : n109 1 # ASSIGN : n110 1 # ASSIGN : n111 1 # ASSIGN : n112 1 # ASSIGN : n113 1 # ASSIGN : n114 1 # ASSIGN : n115 1 # ASSIGN : n116 1 # ASSIGN : n117 1 # ASSIGN : n118 1 # ASSIGN : n119 1 # ASSIGN : n120 1 # ASSIGN : n121 1 # ASSIGN : n122 1 # ASSIGN : n123 1 # ASSIGN : n124 1 # ASSIGN : n125 1 # ASSIGN : n126 1 # ASSIGN : n127 3 # ASSIGN : n128 3 # ASSIGN : n129 3 # ASSIGN : n130 3 # ASSIGN : n131 3 # ASSIGN : n132 3 # ASSIGN : n133 3 # ASSIGN : n134 3 # ASSIGN : n135 3 # ASSIGN : n136 3 # ASSIGN : n137 3 # ASSIGN : n138 3 # ASSIGN : n139 3 # ASSIGN : n140 3 # ASSIGN : n141 3 # ASSIGN : n142 3 # ASSIGN : n143 3 # ASSIGN : n144 3 # ASSIGN : n145 9 # ASSIGN : n146 3 # ASSIGN : n147 3 # ASSIGN : n148 7 # ASSIGN : n149 8 # ASSIGN : n150 9 # ASSIGN : n151 3 # ASSIGN : n152 1 # ASSIGN : n153 2 # ASSIGN : n154 10 # ASSIGN : n155 4 # ASSIGN : n156 4 # ASSIGN : n157 4 # ASSIGN : n158 4 # ASSIGN : n159 4 # ASSIGN : n160 4 # ASSIGN : n161 4 # ASSIGN : n162 4 # ASSIGN : n163 4 # ASSIGN : n164 4 # ASSIGN : n165 4 # ASSIGN : n166 4 # ASSIGN : n167 4 # ASSIGN : n168 4 # ASSIGN : n169 4 # ASSIGN : n170 4 # ASSIGN : n171 4 # ASSIGN : n172 4 # ASSIGN : n173 4 # ASSIGN : n174 4 # ASSIGN : n175 4 # ASSIGN : n176 4 # ASSIGN : n177 4 # ASSIGN : n178 4 # ASSIGN : n179 4 # ASSIGN : n180 4 # ASSIGN : n181 4 # ASSIGN : n182 4 # ASSIGN : n183 4 # ASSIGN : n184 4 # ASSIGN : n185 4 # ASSIGN : n186 4 # ASSIGN : n187 4 # ASSIGN : n188 4 # ASSIGN : n189 4 # ASSIGN : n190 4 # ASSIGN : n191 4 # ASSIGN : n192 4 # ASSIGN : n193 4 # ASSIGN : n194 4 # ASSIGN : n195 4 # ASSIGN : n196 4 # ASSIGN : n197 4 # ASSIGN : n198 4 # ASSIGN : n199 4 # ASSIGN : n200 4 # ASSIGN : n201 4 # ASSIGN : n202 4 # ASSIGN : n203 4 # ASSIGN : n204 4 # ASSIGN : n205 4 # ASSIGN : n206 4 # ASSIGN : n207 4 # ASSIGN : n208 4 # ASSIGN : n209 4 # ASSIGN : n210 4 # ASSIGN : n211 4 # ASSIGN : n212 4 # ASSIGN : n213 4 # ASSIGN : n214 4 # ASSIGN : n215 4 # ASSIGN : n216 4 # ASSIGN : n217 4 # ASSIGN : n218 4 # ASSIGN : n219 4 # ASSIGN : n220 4 # ASSIGN : n221 4 # ASSIGN : n222 4 # ASSIGN : n223 4 # ASSIGN : n224 4 # ASSIGN : n225 4 # ASSIGN : n226 4 # ASSIGN : n227 4 # ASSIGN : n228 4 # ASSIGN : n229 4 # ASSIGN : n230 4 # ASSIGN : n231 4 # ASSIGN : n232 4 # ASSIGN : n233 4 # ASSIGN : n234 4 # ASSIGN : n235 4 # ASSIGN : n236 4 # ASSIGN : n237 4 # ASSIGN : n238 4 # ASSIGN : n239 4 # ASSIGN : n240 2 # ASSIGN : n241 4 # ASSIGN : n242 4 # ASSIGN : n243 4 # ASSIGN : n244 2 # ASSIGN : n245 4 # ASSIGN : n246 4 # ASSIGN : n247 4 # ASSIGN : n248 4 # ASSIGN : n249 4 # ASSIGN : n250 4 # ASSIGN : n251 4 # ASSIGN : n252 4 # ASSIGN : n253 4 # ASSIGN : n254 4 # ASSIGN : n255 4 # ASSIGN : n256 4 # ASSIGN : n257 4 # ASSIGN : n258 4 # ASSIGN : n259 4 # ASSIGN : n260 4 # ASSIGN : n261 4 # ASSIGN : n262 4 # ASSIGN : n263 4 # ASSIGN : n264 4 # ASSIGN : n265 4 # ASSIGN : n266 4 # ASSIGN : n267 4 # ASSIGN : n268 4 # ASSIGN : n269 4 # ASSIGN : n270 4 # ASSIGN : n271 4 # ASSIGN : n272 4 # ASSIGN : n273 4 # ASSIGN : n274 4 # ASSIGN : n275 4 # ASSIGN : n276 4 # ASSIGN : n277 10 # ASSIGN : n278 4 # ASSIGN : n279 4 # ASSIGN : n280 4 # ASSIGN : n281 4 # ASSIGN : n282 2 # ASSIGN : n283 4 # ASSIGN : n284 4 # ASSIGN : n285 4 # ASSIGN : n286 2 # ASSIGN : n287 4 # ASSIGN : n288 4 # ASSIGN : n289 4 # ASSIGN : n290 4 # ASSIGN : n291 4 # ASSIGN : n292 4 # ASSIGN : n293 4 # ASSIGN : n294 4 # ASSIGN : n295 4 # ASSIGN : n296 2 # ASSIGN : n297 4 # ASSIGN : n298 4 # ASSIGN : n299 4 # ASSIGN : n300 4 # ASSIGN : n301 4 # ASSIGN : n302 4 # ASSIGN : n303 4 # ASSIGN : n304 4 # ASSIGN : n305 4 # ASSIGN : n306 4 # ASSIGN : n307 2 # ASSIGN : n308 4 # ASSIGN : n309 5 # ASSIGN : n310 5 # ASSIGN : n311 5 # ASSIGN : n312 5 # ASSIGN : n313 5 # ASSIGN : n314 5 # ASSIGN : n315 5 # ASSIGN : n316 5 # ASSIGN : n317 5 # ASSIGN : n318 5 # ASSIGN : n319 5 # ASSIGN : n320 5 # ASSIGN : n321 5 # ASSIGN : n322 5 # ASSIGN : n323 5 # ASSIGN : n324 5 # ASSIGN : n325 5 # ASSIGN : n326 5 # ASSIGN : n327 5 # ASSIGN : n328 5 # ASSIGN : n329 5 # ASSIGN : n330 5 # ASSIGN : n331 5 # ASSIGN : n332 5 # ASSIGN : n333 5 # ASSIGN : n334 5 # ASSIGN : n335 5 # ASSIGN : n336 5 # ASSIGN : n337 5 # ASSIGN : n338 10 # ASSIGN : n339 5 # ASSIGN : n340 5 # ASSIGN : n341 5 # ASSIGN : n342 5 # ASSIGN : n343 5 # ASSIGN : n344 5 # ASSIGN : n345 5 # ASSIGN : n346 5 # ASSIGN : n347 5 # ASSIGN : n348 5 # ASSIGN : n349 5 # ASSIGN : n350 5 # ASSIGN : n351 5 # ASSIGN : n352 5 # ASSIGN : n353 5 # ASSIGN : n354 5 # ASSIGN : n355 5 # ASSIGN : n356 5 # ASSIGN : n357 5 # ASSIGN : n358 5 # ASSIGN : n359 5 # ASSIGN : n360 5 # ASSIGN : n361 5 # ASSIGN : n362 5 # ASSIGN : n363 5 # ASSIGN : n364 5 # ASSIGN : n365 5 # ASSIGN : n366 5 # ASSIGN : n367 5 # ASSIGN : n368 5 # ASSIGN : n369 5 # ASSIGN : n370 5 # ASSIGN : n371 5 # ASSIGN : n372 5 # ASSIGN : n373 5 # ASSIGN : n374 5 # ASSIGN : n375 5 # ASSIGN : n376 5 # ASSIGN : n377 5 # ASSIGN : n378 5 # ASSIGN : n379 5 # ASSIGN : n380 5 # ASSIGN : n381 5 # ASSIGN : n382 5 # ASSIGN : n383 5 # ASSIGN : n384 5 # ASSIGN : n385 5 # ASSIGN : n386 5 # ASSIGN : n387 5 # ASSIGN : n388 5 # ASSIGN : n389 5 # ASSIGN : n390 5 # ASSIGN : n391 5 # ASSIGN : n392 5 # ASSIGN : n393 5 # ASSIGN : n394 5 # ASSIGN : n395 5 # ASSIGN : n396 5 # ASSIGN : n397 5 # ASSIGN : n398 5 # ASSIGN : n399 5 # ASSIGN : n400 5 # ASSIGN : n401 5 # ASSIGN : n402 5 # ASSIGN : n403 5 # ASSIGN : n404 5 # ASSIGN : n405 5 # ASSIGN : n406 5 # ASSIGN : n407 5 # ASSIGN : n408 5 # ASSIGN : n409 5 # ASSIGN : n410 5 # ASSIGN : n411 5 # ASSIGN : n412 5 # ASSIGN : n413 5 # ASSIGN : n414 5 # ASSIGN : n415 5 # ASSIGN : n416 3 # ASSIGN : n417 5 # ASSIGN : n418 5 # ASSIGN : n419 5 # ASSIGN : n420 5 # ASSIGN : n421 5 # ASSIGN : n422 5 # ASSIGN : n423 5 # ASSIGN : n424 5 # ASSIGN : n425 5 # ASSIGN : n426 5 # ASSIGN : n427 5 # ASSIGN : n428 5 # ASSIGN : n429 5 # ASSIGN : n430 5 # ASSIGN : n431 5 # ASSIGN : n432 5 # ASSIGN : n433 5 # ASSIGN : n434 5 # ASSIGN : n435 5 # ASSIGN : n436 5 # ASSIGN : n437 5 # ASSIGN : n438 5 # ASSIGN : n439 5 # ASSIGN : n440 5 # ASSIGN : n441 5 # ASSIGN : n442 5 # ASSIGN : n443 5 # ASSIGN : n444 5 # ASSIGN : n445 5 # ASSIGN : n446 5 # ASSIGN : n447 5 # ASSIGN : n448 5 # ASSIGN : n449 5 # ASSIGN : n450 5 # ASSIGN : n451 5 # ASSIGN : n452 5 # ASSIGN : n453 5 # ASSIGN : n454 5 # ASSIGN : n455 5 # ASSIGN : n456 5 # ASSIGN : n457 5 # ASSIGN : n458 5 # ASSIGN : n459 5 # ASSIGN : n460 5 # ASSIGN : n461 5 # ASSIGN : n462 5 # ASSIGN : n463 6 # ASSIGN : n464 6 # ASSIGN : n465 6 # ASSIGN : n466 6 # ASSIGN : n467 6 # ASSIGN : n468 6 # ASSIGN : n469 6 # ASSIGN : n470 6 # ASSIGN : n471 6 # ASSIGN : n472 6 # ASSIGN : n473 6 # ASSIGN : n474 6 # ASSIGN : n475 6 # ASSIGN : n476 6 # ASSIGN : n477 6 # ASSIGN : n478 6 # ASSIGN : n479 6 # ASSIGN : n480 6 # ASSIGN : n481 6 # ASSIGN : n482 6 # ASSIGN : n483 6 # ASSIGN : n484 6 # ASSIGN : n485 6 # ASSIGN : n486 6 # ASSIGN : n487 6 # ASSIGN : n488 6 # ASSIGN : n489 6 # ASSIGN : n490 6 # ASSIGN : n491 6 # ASSIGN : n492 6 # ASSIGN : n493 6 # ASSIGN : n494 6 # ASSIGN : n495 6 # ASSIGN : n496 6 # ASSIGN : n497 6 # ASSIGN : n498 6 # ASSIGN : n499 6 # ASSIGN : n500 6 # ASSIGN : n501 6 # ASSIGN : n502 6 # ASSIGN : n503 6 # ASSIGN : n504 6 # ASSIGN : n505 6 # ASSIGN : n506 6 # ASSIGN : n507 6 # ASSIGN : n508 6 # ASSIGN : n509 6 # ASSIGN : n510 6 # ASSIGN : n511 6 # ASSIGN : n512 6 # ASSIGN : n513 6 # ASSIGN : n514 6 # ASSIGN : n515 6 # ASSIGN : n516 6 # ASSIGN : n517 6 # ASSIGN : n518 10 # ASSIGN : n519 6 # ASSIGN : n520 6 # ASSIGN : n521 6 # ASSIGN : n522 6 # ASSIGN : n523 6 # ASSIGN : n524 6 # ASSIGN : n525 6 # ASSIGN : n526 6 # ASSIGN : n527 6 # ASSIGN : n528 6 # ASSIGN : n529 6 # ASSIGN : n530 6 # ASSIGN : n531 6 # ASSIGN : n532 6 # ASSIGN : n533 6 # ASSIGN : n534 6 # ASSIGN : n535 6 # ASSIGN : n536 6 # ASSIGN : n537 6 # ASSIGN : n538 6 # ASSIGN : n539 6 # ASSIGN : n540 6 # ASSIGN : n541 6 # ASSIGN : n542 6 # ASSIGN : n543 6 # ASSIGN : n544 6 # ASSIGN : n545 6 # ASSIGN : n546 6 # ASSIGN : n547 6 # ASSIGN : n548 6 # ASSIGN : n549 6 # ASSIGN : n550 6 # ASSIGN : n551 6 # ASSIGN : n552 6 # ASSIGN : n553 6 # ASSIGN : n554 6 # ASSIGN : n555 6 # ASSIGN : n556 6 # ASSIGN : n557 6 # ASSIGN : n558 6 # ASSIGN : n559 6 # ASSIGN : n560 6 # ASSIGN : n561 6 # ASSIGN : n562 6 # ASSIGN : n563 6 # ASSIGN : n564 6 # ASSIGN : n565 6 # ASSIGN : n566 6 # ASSIGN : n567 6 # ASSIGN : n568 6 # ASSIGN : n569 6 # ASSIGN : n570 6 # ASSIGN : n571 6 # ASSIGN : n572 6 # ASSIGN : n573 6 # ASSIGN : n574 6 # ASSIGN : n575 6 # ASSIGN : n576 6 # ASSIGN : n577 6 # ASSIGN : n578 6 # ASSIGN : n579 6 # ASSIGN : n580 6 # ASSIGN : n581 6 # ASSIGN : n582 6 # ASSIGN : n583 6 # ASSIGN : n584 6 # ASSIGN : n585 6 # ASSIGN : n586 6 # ASSIGN : n587 6 # ASSIGN : n588 6 # ASSIGN : n589 6 # ASSIGN : n590 6 # ASSIGN : n591 6 # ASSIGN : n592 6 # ASSIGN : n593 6 # ASSIGN : n594 6 # ASSIGN : n595 6 # ASSIGN : n596 6 # ASSIGN : n597 6 # ASSIGN : n598 6 # ASSIGN : n599 6 # ASSIGN : n600 6 # ASSIGN : n601 6 # ASSIGN : n602 6 # ASSIGN : n603 6 # ASSIGN : n604 6 # ASSIGN : n605 6 # ASSIGN : n606 6 # ASSIGN : n607 6 # ASSIGN : n608 6 # ASSIGN : n609 6 # ASSIGN : n610 6 # ASSIGN : n611 6 # ASSIGN : n612 6 # ASSIGN : n613 6 # ASSIGN : n614 6 # ASSIGN : n615 6 # ASSIGN : n616 6 # ASSIGN : n617 1 # ASSIGN : n618 10 # ASSIGN : n619 1 # ASSIGN : n620 1 # ASSIGN : n621 1 # ASSIGN : n622 1 # ASSIGN : n623 1 # ASSIGN : n624 1 # ASSIGN : n625 1 # ASSIGN : n626 1 # ASSIGN : n627 1 # ASSIGN : n628 1 # ASSIGN : n629 1 # ASSIGN : n630 1 # ASSIGN : n631 1 # ASSIGN : n632 1 # ASSIGN : n633 1 # ASSIGN : n634 1 # ASSIGN : n635 1 # ASSIGN : n636 1 # ASSIGN : n637 1 # ASSIGN : n638 1 # ASSIGN : n639 1 # ASSIGN : n640 1 # ASSIGN : n641 1 # ASSIGN : n642 1 # ASSIGN : n643 1 # ASSIGN : n644 1 # ASSIGN : n645 1 # ASSIGN : n646 1 # ASSIGN : n647 1 # ASSIGN : n648 1 # ASSIGN : n649 1 # ASSIGN : n650 1 # ASSIGN : n651 1 # ASSIGN : n652 1 # ASSIGN : n653 1 # ASSIGN : n654 1 # ASSIGN : n655 1 # ASSIGN : n656 1 # ASSIGN : n657 1 # ASSIGN : n658 1 # ASSIGN : n659 1 # ASSIGN : n660 1 # ASSIGN : n661 1 # ASSIGN : n662 1 # ASSIGN : n663 1 # ASSIGN : n664 1 # ASSIGN : n665 1 # ASSIGN : n666 1 # ASSIGN : n667 1 # ASSIGN : n668 1 # ASSIGN : n669 1 # ASSIGN : n670 1 # ASSIGN : n671 1 # ASSIGN : n672 1 # ASSIGN : n673 1 # ASSIGN : n674 1 # ASSIGN : n675 1 # ASSIGN : n676 1 # ASSIGN : n677 1 # ASSIGN : n678 1 # ASSIGN : n679 1 # ASSIGN : n680 1 # ASSIGN : n681 1 # ASSIGN : n682 1 # ASSIGN : n683 1 # ASSIGN : n684 1 # ASSIGN : n685 1 # ASSIGN : n686 1 # ASSIGN : n687 1 # ASSIGN : n688 1 # ASSIGN : n689 1 # ASSIGN : n690 1 # ASSIGN : n691 1 # ASSIGN : n692 1 # ASSIGN : n693 1 # ASSIGN : n694 1 # ASSIGN : n695 1 # ASSIGN : n696 1 # ASSIGN : n697 1 # ASSIGN : n698 1 # ASSIGN : n699 1 # ASSIGN : n700 1 # ASSIGN : n701 1 # ASSIGN : n702 1 # ASSIGN : n703 1 # ASSIGN : n704 1 # ASSIGN : n705 1 # ASSIGN : n706 1 # ASSIGN : n707 1 # ASSIGN : n708 1 # ASSIGN : n709 1 # ASSIGN : n710 1 # ASSIGN : n711 1 # ASSIGN : n712 1 # ASSIGN : n713 1 # ASSIGN : n714 1 # ASSIGN : n715 1 # ASSIGN : n716 1 # ASSIGN : n717 1 # ASSIGN : n718 1 # ASSIGN : n719 1 # ASSIGN : n720 1 # ASSIGN : n721 1 # ASSIGN : n722 1 # ASSIGN : n723 1 # ASSIGN : n724 1 # ASSIGN : n725 1 # ASSIGN : n726 1 # ASSIGN : n727 1 # ASSIGN : n728 1 # ASSIGN : n729 1 # ASSIGN : n730 1 # ASSIGN : n731 1 # ASSIGN : n732 1 # ASSIGN : n733 1 # ASSIGN : n734 1 # ASSIGN : n735 1 # ASSIGN : n736 1 # ASSIGN : n737 1 # ASSIGN : n738 1 # ASSIGN : n739 1 # ASSIGN : n740 1 # ASSIGN : n741 1 # ASSIGN : n742 1 # ASSIGN : n743 1 # ASSIGN : n744 1 # ASSIGN : n745 1 # ASSIGN : n746 1 # ASSIGN : n747 1 # ASSIGN : n748 1 # ASSIGN : n749 1 # ASSIGN : n750 1 # ASSIGN : n751 1 # ASSIGN : n752 1 # ASSIGN : n753 1 # ASSIGN : n754 1 # ASSIGN : n755 1 # ASSIGN : n756 1 # ASSIGN : n757 1 # ASSIGN : n758 1 # ASSIGN : n759 1 # ASSIGN : n760 1 # ASSIGN : n761 1 # ASSIGN : n762 1 # ASSIGN : n763 1 # ASSIGN : n764 1 # ASSIGN : n765 1 # ASSIGN : n766 1 # ASSIGN : n767 1 # ASSIGN : n768 1 # ASSIGN : n769 1 # ASSIGN : n770 1 # ASSIGN : n771 2 # ASSIGN : n772 2 # ASSIGN : n773 2 # ASSIGN : n774 2 # ASSIGN : n775 2 # ASSIGN : n776 2 # ASSIGN : n777 2 # ASSIGN : n778 2 # ASSIGN : n779 2 # ASSIGN : n780 2 # ASSIGN : n781 2 # ASSIGN : n782 2 # ASSIGN : n783 2 # ASSIGN : n784 2 # ASSIGN : n785 2 # ASSIGN : n786 2 # ASSIGN : n787 2 # ASSIGN : n788 2 # ASSIGN : n789 2 # ASSIGN : n790 2 # ASSIGN : n791 2 # ASSIGN : n792 8 # ASSIGN : n793 2 # ASSIGN : n794 2 # ASSIGN : n795 2 # ASSIGN : n796 2 # ASSIGN : n797 2 # ASSIGN : n798 2 # ASSIGN : n799 2 # ASSIGN : n800 2 # ASSIGN : n801 2 # ASSIGN : n802 2 # ASSIGN : n803 2 # ASSIGN : n804 2 # ASSIGN : n805 2 # ASSIGN : n806 2 # ASSIGN : n807 2 # ASSIGN : n808 2 # ASSIGN : n809 2 # ASSIGN : n810 2 # ASSIGN : n811 2 # ASSIGN : n812 2 # ASSIGN : n813 2 # ASSIGN : n814 2 # ASSIGN : n815 2 # ASSIGN : n816 2 # ASSIGN : n817 2 # ASSIGN : n818 2 # ASSIGN : n819 2 # ASSIGN : n820 2 # ASSIGN : n821 2 # ASSIGN : n822 2 # ASSIGN : n823 2 # ASSIGN : n824 2 # ASSIGN : n825 2 # ASSIGN : n826 2 # ASSIGN : n827 2 # ASSIGN : n828 2 # ASSIGN : n829 2 # ASSIGN : n830 2 # ASSIGN : n831 2 # ASSIGN : n832 2 # ASSIGN : n833 2 # ASSIGN : n834 2 # ASSIGN : n835 2 # ASSIGN : n836 2 # ASSIGN : n837 2 # ASSIGN : n838 2 # ASSIGN : n839 2 # ASSIGN : n840 2 # ASSIGN : n841 2 # ASSIGN : n842 2 # ASSIGN : n843 2 # ASSIGN : n844 2 # ASSIGN : n845 2 # ASSIGN : n846 2 # ASSIGN : n847 2 # ASSIGN : n848 2 # ASSIGN : n849 2 # ASSIGN : n850 2 # ASSIGN : n851 2 # ASSIGN : n852 2 # ASSIGN : n853 2 # ASSIGN : n854 2 # ASSIGN : n855 2 # ASSIGN : n856 2 # ASSIGN : n857 2 # ASSIGN : n858 2 # ASSIGN : n859 2 # ASSIGN : n860 2 # ASSIGN : n861 2 # ASSIGN : n862 2 # ASSIGN : n863 2 # ASSIGN : n864 2 # ASSIGN : n865 2 # ASSIGN : n866 2 # ASSIGN : n867 2 # ASSIGN : n868 2 # ASSIGN : n869 2 # ASSIGN : n870 2 # ASSIGN : n871 2 # ASSIGN : n872 2 # ASSIGN : n873 2 # ASSIGN : n874 2 # ASSIGN : n875 2 # ASSIGN : n876 2 # ASSIGN : n877 2 # ASSIGN : n878 2 # ASSIGN : n879 2 # ASSIGN : n880 2 # ASSIGN : n881 2 # ASSIGN : n882 2 # ASSIGN : n883 2 # ASSIGN : n884 2 # ASSIGN : n885 2 # ASSIGN : n886 2 # ASSIGN : n887 2 # ASSIGN : n888 2 # ASSIGN : n889 2 # ASSIGN : n890 2 # ASSIGN : n891 2 # ASSIGN : n892 2 # ASSIGN : n893 2 # ASSIGN : n894 2 # ASSIGN : n895 2 # ASSIGN : n896 2 # ASSIGN : n897 2 # ASSIGN : n898 2 # ASSIGN : n899 2 # ASSIGN : n900 2 # ASSIGN : n901 2 # ASSIGN : n902 2 # ASSIGN : n903 2 # ASSIGN : n904 2 # ASSIGN : n905 2 # ASSIGN : n906 2 # ASSIGN : n907 2 # ASSIGN : n908 2 # ASSIGN : n909 2 # ASSIGN : n910 2 # ASSIGN : n911 2 # ASSIGN : n912 2 # ASSIGN : n913 2 # ASSIGN : n914 2 # ASSIGN : n915 2 # ASSIGN : n916 2 # ASSIGN : n917 2 # ASSIGN : n918 2 # ASSIGN : n919 2 # ASSIGN : n920 2 # ASSIGN : n921 2 # ASSIGN : n922 2 # ASSIGN : n923 2 # ASSIGN : n924 2 # ASSIGN : n925 3 # ASSIGN : n926 3 # ASSIGN : n927 3 # ASSIGN : n928 3 # ASSIGN : n929 3 # ASSIGN : n930 3 # ASSIGN : n931 3 # ASSIGN : n932 3 # ASSIGN : n933 3 # ASSIGN : n934 3 # ASSIGN : n935 3 # ASSIGN : n936 3 # ASSIGN : n937 3 # ASSIGN : n938 3 # ASSIGN : n939 3 # ASSIGN : n940 3 # ASSIGN : n941 3 # ASSIGN : n942 3 # ASSIGN : n943 3 # ASSIGN : n944 3 # ASSIGN : n945 3 # ASSIGN : n946 3 # ASSIGN : n947 3 # ASSIGN : n948 3 # ASSIGN : n949 3 # ASSIGN : n950 3 # ASSIGN : n951 3 # ASSIGN : n952 3 # ASSIGN : n953 3 # ASSIGN : n954 3 # ASSIGN : n955 3 # ASSIGN : n956 3 # ASSIGN : n957 3 # ASSIGN : n958 3 # ASSIGN : n959 3 # ASSIGN : n960 3 # ASSIGN : n961 3 # ASSIGN : n962 3 # ASSIGN : n963 3 # ASSIGN : n964 3 # ASSIGN : n965 3 # ASSIGN : n966 3 # ASSIGN : n967 3 # ASSIGN : n968 3 # ASSIGN : n969 3 # ASSIGN : n970 3 # ASSIGN : n971 3 # ASSIGN : n972 3 # ASSIGN : n973 3 # ASSIGN : n974 3 # ASSIGN : n975 3 # ASSIGN : n976 3 # ASSIGN : n977 3 # ASSIGN : n978 3 # ASSIGN : n979 3 # ASSIGN : n980 3 # ASSIGN : n981 3 # ASSIGN : n982 3 # ASSIGN : n983 3 # ASSIGN : n984 3 # ASSIGN : n985 3 # ASSIGN : n986 3 # ASSIGN : n987 3 # ASSIGN : n988 3 # ASSIGN : n989 3 # ASSIGN : n990 3 # ASSIGN : n991 3 # ASSIGN : n992 3 # ASSIGN : n993 3 # ASSIGN : n994 3 # ASSIGN : n995 3 # ASSIGN : n996 3 # ASSIGN : n997 3 # ASSIGN : n998 3 # ASSIGN : n999 3 # ASSIGN : n1000 3 # ASSIGN : n1001 3 # ASSIGN : n1002 3 # ASSIGN : n1003 3 # ASSIGN : n1004 3 # ASSIGN : n1005 3 # ASSIGN : n1006 3 # ASSIGN : n1007 3 # ASSIGN : n1008 3 # ASSIGN : n1009 3 # ASSIGN : n1010 3 # ASSIGN : n1011 3 # ASSIGN : n1012 3 # ASSIGN : n1013 3 # ASSIGN : n1014 3 # ASSIGN : n1015 3 # ASSIGN : n1016 3 # ASSIGN : n1017 3 # ASSIGN : n1018 3 # ASSIGN : n1019 3 # ASSIGN : n1020 3 # ASSIGN : n1021 3 # ASSIGN : n1022 3 # ASSIGN : n1023 3 # ASSIGN : n1024 3 # ASSIGN : n1025 3 # ASSIGN : n1026 3 # ASSIGN : n1027 3 # ASSIGN : n1028 3 # ASSIGN : n1029 3 # ASSIGN : n1030 3 # ASSIGN : n1031 3 # ASSIGN : n1032 3 # ASSIGN : n1033 3 # ASSIGN : n1034 3 # ASSIGN : n1035 3 # ASSIGN : n1036 3 # ASSIGN : n1037 3 # ASSIGN : n1038 3 # ASSIGN : n1039 3 # ASSIGN : n1040 3 # ASSIGN : n1041 3 # ASSIGN : n1042 3 # ASSIGN : n1043 3 # ASSIGN : n1044 3 # ASSIGN : n1045 3 # ASSIGN : n1046 3 # ASSIGN : n1047 3 # ASSIGN : n1048 3 # ASSIGN : n1049 3 # ASSIGN : n1050 3 # ASSIGN : n1051 3 # ASSIGN : n1052 3 # ASSIGN : n1053 3 # ASSIGN : n1054 3 # ASSIGN : n1055 3 # ASSIGN : n1056 3 # ASSIGN : n1057 3 # ASSIGN : n1058 3 # ASSIGN : n1059 3 # ASSIGN : n1060 3 # ASSIGN : n1061 3 # ASSIGN : n1062 3 # ASSIGN : n1063 3 # ASSIGN : n1064 3 # ASSIGN : n1065 3 # ASSIGN : n1066 3 # ASSIGN : n1067 3 # ASSIGN : n1068 3 # ASSIGN : n1069 3 # ASSIGN : n1070 3 # ASSIGN : n1071 3 # ASSIGN : n1072 3 # ASSIGN : n1073 3 # ASSIGN : n1074 3 # ASSIGN : n1075 3 # ASSIGN : n1076 3 # ASSIGN : n1077 3 # ASSIGN : n1078 3 # ASSIGN : n1079 4 # ASSIGN : n1080 5 # ASSIGN : n1081 6 # ASSIGN : n1082 7 # ASSIGN : n1083 8 # ASSIGN : n1084 9 # ASSIGN : n1085 10 SHOW_RESULT 10 END : 10 (0 seconds) [Thu Jul 6 14:05:08 2006] SHOW_RESULT 10 CPU : 0.0799999999999983 = 0.0799999999999983 + 0 + 0 + 0 # BOUND : color 8 10 MODIFY_CNF 9 BEGIN : [Thu Jul 6 14:05:08 2006] MODIFY_CNF 9 END : 12051740 bytes (0 seconds) [Thu Jul 6 14:05:08 2006] MODIFY_CNF 9 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 9 BEGIN : [Thu Jul 6 14:05:08 2006] CMD : minisat /tmp/csp2sat18628.cnf /tmp/csp2sat18628.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 261009 777047 | 87003 0 0 nan | 0.000 % | | 100 | 261009 777047 | 95703 100 731 7.3 | 36.968 % | ============================================================================== restarts : 2 conflicts : 114 (71 /sec) decisions : 11352 (7051 /sec) propagations : 89634 (55673 /sec) conflict literals : 813 (9.47 % deleted) Memory used : 24.23 MB CPU time : 1.61 s SATISFIABLE VERIFY_CNF 9 END : (2 seconds) [Thu Jul 6 14:05:10 2006] VERIFY_CNF 9 CPU : 1.74 = 0 + 0 + 1.63 + 0.11 # RESULT : color 9 SATISFIABLE SHOW_RESULT 9 BEGIN : [Thu Jul 6 14:05:10 2006] # ASSIGN : color 9 # ASSIGN : n1 1 # ASSIGN : n2 6 # ASSIGN : n3 1 # ASSIGN : n4 3 # ASSIGN : n5 5 # ASSIGN : n6 7 # ASSIGN : n7 1 # ASSIGN : n8 1 # ASSIGN : n9 8 # ASSIGN : n10 8 # ASSIGN : n11 1 # ASSIGN : n12 1 # ASSIGN : n13 3 # ASSIGN : n14 3 # ASSIGN : n15 5 # ASSIGN : n16 4 # ASSIGN : n17 8 # ASSIGN : n18 6 # ASSIGN : n19 3 # ASSIGN : n20 7 # ASSIGN : n21 1 # ASSIGN : n22 7 # ASSIGN : n23 4 # ASSIGN : n24 3 # ASSIGN : n25 3 # ASSIGN : n26 7 # ASSIGN : n27 4 # ASSIGN : n28 4 # ASSIGN : n29 4 # ASSIGN : n30 4 # ASSIGN : n31 4 # ASSIGN : n32 4 # ASSIGN : n33 4 # ASSIGN : n34 4 # ASSIGN : n35 4 # ASSIGN : n36 9 # ASSIGN : n37 9 # ASSIGN : n38 9 # ASSIGN : n39 6 # ASSIGN : n40 9 # ASSIGN : n41 7 # ASSIGN : n42 9 # ASSIGN : n43 8 # ASSIGN : n44 8 # ASSIGN : n45 7 # ASSIGN : n46 6 # ASSIGN : n47 8 # ASSIGN : n48 8 # ASSIGN : n49 5 # ASSIGN : n50 5 # ASSIGN : n51 6 # ASSIGN : n52 6 # ASSIGN : n53 6 # ASSIGN : n54 6 # ASSIGN : n55 6 # ASSIGN : n56 6 # ASSIGN : n57 5 # ASSIGN : n58 8 # ASSIGN : n59 3 # ASSIGN : n60 6 # ASSIGN : n61 5 # ASSIGN : n62 5 # ASSIGN : n63 5 # ASSIGN : n64 5 # ASSIGN : n65 5 # ASSIGN : n66 4 # ASSIGN : n67 4 # ASSIGN : n68 8 # ASSIGN : n69 8 # ASSIGN : n70 4 # ASSIGN : n71 4 # ASSIGN : n72 4 # ASSIGN : n73 4 # ASSIGN : n74 4 # ASSIGN : n75 4 # ASSIGN : n76 4 # ASSIGN : n77 9 # ASSIGN : n78 7 # ASSIGN : n79 8 # ASSIGN : n80 4 # ASSIGN : n81 7 # ASSIGN : n82 7 # ASSIGN : n83 7 # ASSIGN : n84 7 # ASSIGN : n85 8 # ASSIGN : n86 9 # ASSIGN : n87 7 # ASSIGN : n88 9 # ASSIGN : n89 8 # ASSIGN : n90 5 # ASSIGN : n91 6 # ASSIGN : n92 6 # ASSIGN : n93 8 # ASSIGN : n94 8 # ASSIGN : n95 5 # ASSIGN : n96 5 # ASSIGN : n97 8 # ASSIGN : n98 8 # ASSIGN : n99 5 # ASSIGN : n100 5 # ASSIGN : n101 5 # ASSIGN : n102 5 # ASSIGN : n103 5 # ASSIGN : n104 6 # ASSIGN : n105 5 # ASSIGN : n106 8 # ASSIGN : n107 9 # ASSIGN : n108 6 # ASSIGN : n109 9 # ASSIGN : n110 8 # ASSIGN : n111 8 # ASSIGN : n112 9 # ASSIGN : n113 9 # ASSIGN : n114 8 # ASSIGN : n115 8 # ASSIGN : n116 9 # ASSIGN : n117 9 # ASSIGN : n118 9 # ASSIGN : n119 9 # ASSIGN : n120 4 # ASSIGN : n121 8 # ASSIGN : n122 4 # ASSIGN : n123 4 # ASSIGN : n124 9 # ASSIGN : n125 6 # ASSIGN : n126 4 # ASSIGN : n127 3 # ASSIGN : n128 9 # ASSIGN : n129 3 # ASSIGN : n130 9 # ASSIGN : n131 3 # ASSIGN : n132 3 # ASSIGN : n133 3 # ASSIGN : n134 9 # ASSIGN : n135 3 # ASSIGN : n136 3 # ASSIGN : n137 3 # ASSIGN : n138 5 # ASSIGN : n139 3 # ASSIGN : n140 3 # ASSIGN : n141 5 # ASSIGN : n142 3 # ASSIGN : n143 3 # ASSIGN : n144 3 # ASSIGN : n145 9 # ASSIGN : n146 3 # ASSIGN : n147 5 # ASSIGN : n148 8 # ASSIGN : n149 5 # ASSIGN : n150 9 # ASSIGN : n151 6 # ASSIGN : n152 3 # ASSIGN : n153 7 # ASSIGN : n154 4 # ASSIGN : n155 2 # ASSIGN : n156 2 # ASSIGN : n157 2 # ASSIGN : n158 6 # ASSIGN : n159 2 # ASSIGN : n160 2 # ASSIGN : n161 2 # ASSIGN : n162 2 # ASSIGN : n163 2 # ASSIGN : n164 2 # ASSIGN : n165 2 # ASSIGN : n166 2 # ASSIGN : n167 2 # ASSIGN : n168 2 # ASSIGN : n169 2 # ASSIGN : n170 2 # ASSIGN : n171 2 # ASSIGN : n172 2 # ASSIGN : n173 2 # ASSIGN : n174 2 # ASSIGN : n175 2 # ASSIGN : n176 2 # ASSIGN : n177 2 # ASSIGN : n178 2 # ASSIGN : n179 2 # ASSIGN : n180 2 # ASSIGN : n181 2 # ASSIGN : n182 2 # ASSIGN : n183 2 # ASSIGN : n184 2 # ASSIGN : n185 2 # ASSIGN : n186 2 # ASSIGN : n187 2 # ASSIGN : n188 2 # ASSIGN : n189 2 # ASSIGN : n190 2 # ASSIGN : n191 2 # ASSIGN : n192 2 # ASSIGN : n193 2 # ASSIGN : n194 9 # ASSIGN : n195 2 # ASSIGN : n196 2 # ASSIGN : n197 8 # ASSIGN : n198 2 # ASSIGN : n199 2 # ASSIGN : n200 2 # ASSIGN : n201 2 # ASSIGN : n202 2 # ASSIGN : n203 2 # ASSIGN : n204 2 # ASSIGN : n205 2 # ASSIGN : n206 2 # ASSIGN : n207 2 # ASSIGN : n208 2 # ASSIGN : n209 2 # ASSIGN : n210 2 # ASSIGN : n211 2 # ASSIGN : n212 2 # ASSIGN : n213 2 # ASSIGN : n214 2 # ASSIGN : n215 2 # ASSIGN : n216 2 # ASSIGN : n217 2 # ASSIGN : n218 2 # ASSIGN : n219 2 # ASSIGN : n220 2 # ASSIGN : n221 2 # ASSIGN : n222 2 # ASSIGN : n223 2 # ASSIGN : n224 2 # ASSIGN : n225 2 # ASSIGN : n226 2 # ASSIGN : n227 2 # ASSIGN : n228 2 # ASSIGN : n229 2 # ASSIGN : n230 2 # ASSIGN : n231 2 # ASSIGN : n232 2 # ASSIGN : n233 2 # ASSIGN : n234 2 # ASSIGN : n235 2 # ASSIGN : n236 2 # ASSIGN : n237 2 # ASSIGN : n238 2 # ASSIGN : n239 2 # ASSIGN : n240 2 # ASSIGN : n241 2 # ASSIGN : n242 2 # ASSIGN : n243 2 # ASSIGN : n244 2 # ASSIGN : n245 9 # ASSIGN : n246 2 # ASSIGN : n247 2 # ASSIGN : n248 2 # ASSIGN : n249 2 # ASSIGN : n250 2 # ASSIGN : n251 2 # ASSIGN : n252 8 # ASSIGN : n253 2 # ASSIGN : n254 8 # ASSIGN : n255 2 # ASSIGN : n256 2 # ASSIGN : n257 2 # ASSIGN : n258 2 # ASSIGN : n259 2 # ASSIGN : n260 2 # ASSIGN : n261 2 # ASSIGN : n262 2 # ASSIGN : n263 2 # ASSIGN : n264 2 # ASSIGN : n265 2 # ASSIGN : n266 2 # ASSIGN : n267 2 # ASSIGN : n268 2 # ASSIGN : n269 2 # ASSIGN : n270 2 # ASSIGN : n271 2 # ASSIGN : n272 4 # ASSIGN : n273 2 # ASSIGN : n274 2 # ASSIGN : n275 2 # ASSIGN : n276 2 # ASSIGN : n277 8 # ASSIGN : n278 2 # ASSIGN : n279 2 # ASSIGN : n280 2 # ASSIGN : n281 2 # ASSIGN : n282 9 # ASSIGN : n283 2 # ASSIGN : n284 2 # ASSIGN : n285 2 # ASSIGN : n286 2 # ASSIGN : n287 2 # ASSIGN : n288 2 # ASSIGN : n289 2 # ASSIGN : n290 2 # ASSIGN : n291 2 # ASSIGN : n292 2 # ASSIGN : n293 2 # ASSIGN : n294 2 # ASSIGN : n295 2 # ASSIGN : n296 2 # ASSIGN : n297 2 # ASSIGN : n298 2 # ASSIGN : n299 2 # ASSIGN : n300 2 # ASSIGN : n301 2 # ASSIGN : n302 2 # ASSIGN : n303 2 # ASSIGN : n304 2 # ASSIGN : n305 6 # ASSIGN : n306 2 # ASSIGN : n307 7 # ASSIGN : n308 4 # ASSIGN : n309 1 # ASSIGN : n310 3 # ASSIGN : n311 1 # ASSIGN : n312 1 # ASSIGN : n313 1 # ASSIGN : n314 1 # ASSIGN : n315 1 # ASSIGN : n316 1 # ASSIGN : n317 1 # ASSIGN : n318 1 # ASSIGN : n319 9 # ASSIGN : n320 1 # ASSIGN : n321 1 # ASSIGN : n322 1 # ASSIGN : n323 5 # ASSIGN : n324 1 # ASSIGN : n325 1 # ASSIGN : n326 1 # ASSIGN : n327 1 # ASSIGN : n328 1 # ASSIGN : n329 1 # ASSIGN : n330 3 # ASSIGN : n331 3 # ASSIGN : n332 1 # ASSIGN : n333 3 # ASSIGN : n334 3 # ASSIGN : n335 3 # ASSIGN : n336 3 # ASSIGN : n337 3 # ASSIGN : n338 9 # ASSIGN : n339 3 # ASSIGN : n340 3 # ASSIGN : n341 3 # ASSIGN : n342 3 # ASSIGN : n343 3 # ASSIGN : n344 1 # ASSIGN : n345 1 # ASSIGN : n346 1 # ASSIGN : n347 1 # ASSIGN : n348 1 # ASSIGN : n349 1 # ASSIGN : n350 1 # ASSIGN : n351 9 # ASSIGN : n352 1 # ASSIGN : n353 1 # ASSIGN : n354 1 # ASSIGN : n355 1 # ASSIGN : n356 1 # ASSIGN : n357 1 # ASSIGN : n358 1 # ASSIGN : n359 1 # ASSIGN : n360 1 # ASSIGN : n361 1 # ASSIGN : n362 1 # ASSIGN : n363 1 # ASSIGN : n364 1 # ASSIGN : n365 3 # ASSIGN : n366 1 # ASSIGN : n367 3 # ASSIGN : n368 3 # ASSIGN : n369 1 # ASSIGN : n370 1 # ASSIGN : n371 1 # ASSIGN : n372 1 # ASSIGN : n373 1 # ASSIGN : n374 1 # ASSIGN : n375 1 # ASSIGN : n376 1 # ASSIGN : n377 1 # ASSIGN : n378 1 # ASSIGN : n379 1 # ASSIGN : n380 1 # ASSIGN : n381 1 # ASSIGN : n382 1 # ASSIGN : n383 1 # ASSIGN : n384 1 # ASSIGN : n385 1 # ASSIGN : n386 9 # ASSIGN : n387 1 # ASSIGN : n388 1 # ASSIGN : n389 1 # ASSIGN : n390 7 # ASSIGN : n391 5 # ASSIGN : n392 3 # ASSIGN : n393 1 # ASSIGN : n394 1 # ASSIGN : n395 1 # ASSIGN : n396 1 # ASSIGN : n397 1 # ASSIGN : n398 1 # ASSIGN : n399 1 # ASSIGN : n400 1 # ASSIGN : n401 1 # ASSIGN : n402 1 # ASSIGN : n403 1 # ASSIGN : n404 1 # ASSIGN : n405 1 # ASSIGN : n406 1 # ASSIGN : n407 3 # ASSIGN : n408 1 # ASSIGN : n409 1 # ASSIGN : n410 1 # ASSIGN : n411 1 # ASSIGN : n412 1 # ASSIGN : n413 1 # ASSIGN : n414 3 # ASSIGN : n415 3 # ASSIGN : n416 3 # ASSIGN : n417 1 # ASSIGN : n418 3 # ASSIGN : n419 3 # ASSIGN : n420 1 # ASSIGN : n421 1 # ASSIGN : n422 1 # ASSIGN : n423 1 # ASSIGN : n424 1 # ASSIGN : n425 1 # ASSIGN : n426 1 # ASSIGN : n427 1 # ASSIGN : n428 1 # ASSIGN : n429 3 # ASSIGN : n430 1 # ASSIGN : n431 1 # ASSIGN : n432 1 # ASSIGN : n433 1 # ASSIGN : n434 1 # ASSIGN : n435 3 # ASSIGN : n436 3 # ASSIGN : n437 1 # ASSIGN : n438 1 # ASSIGN : n439 1 # ASSIGN : n440 1 # ASSIGN : n441 1 # ASSIGN : n442 1 # ASSIGN : n443 3 # ASSIGN : n444 3 # ASSIGN : n445 1 # ASSIGN : n446 1 # ASSIGN : n447 1 # ASSIGN : n448 1 # ASSIGN : n449 1 # ASSIGN : n450 1 # ASSIGN : n451 1 # ASSIGN : n452 1 # ASSIGN : n453 1 # ASSIGN : n454 1 # ASSIGN : n455 1 # ASSIGN : n456 3 # ASSIGN : n457 1 # ASSIGN : n458 1 # ASSIGN : n459 3 # ASSIGN : n460 1 # ASSIGN : n461 1 # ASSIGN : n462 1 # ASSIGN : n463 4 # ASSIGN : n464 4 # ASSIGN : n465 4 # ASSIGN : n466 2 # ASSIGN : n467 4 # ASSIGN : n468 4 # ASSIGN : n469 2 # ASSIGN : n470 2 # ASSIGN : n471 4 # ASSIGN : n472 4 # ASSIGN : n473 4 # ASSIGN : n474 4 # ASSIGN : n475 4 # ASSIGN : n476 4 # ASSIGN : n477 2 # ASSIGN : n478 2 # ASSIGN : n479 2 # ASSIGN : n480 6 # ASSIGN : n481 2 # ASSIGN : n482 2 # ASSIGN : n483 2 # ASSIGN : n484 4 # ASSIGN : n485 4 # ASSIGN : n486 4 # ASSIGN : n487 4 # ASSIGN : n488 4 # ASSIGN : n489 4 # ASSIGN : n490 2 # ASSIGN : n491 2 # ASSIGN : n492 2 # ASSIGN : n493 4 # ASSIGN : n494 4 # ASSIGN : n495 4 # ASSIGN : n496 4 # ASSIGN : n497 4 # ASSIGN : n498 2 # ASSIGN : n499 2 # ASSIGN : n500 2 # ASSIGN : n501 2 # ASSIGN : n502 2 # ASSIGN : n503 2 # ASSIGN : n504 4 # ASSIGN : n505 4 # ASSIGN : n506 4 # ASSIGN : n507 4 # ASSIGN : n508 2 # ASSIGN : n509 2 # ASSIGN : n510 2 # ASSIGN : n511 4 # ASSIGN : n512 2 # ASSIGN : n513 4 # ASSIGN : n514 4 # ASSIGN : n515 4 # ASSIGN : n516 4 # ASSIGN : n517 4 # ASSIGN : n518 8 # ASSIGN : n519 2 # ASSIGN : n520 2 # ASSIGN : n521 2 # ASSIGN : n522 6 # ASSIGN : n523 4 # ASSIGN : n524 2 # ASSIGN : n525 2 # ASSIGN : n526 4 # ASSIGN : n527 4 # ASSIGN : n528 4 # ASSIGN : n529 4 # ASSIGN : n530 2 # ASSIGN : n531 4 # ASSIGN : n532 4 # ASSIGN : n533 4 # ASSIGN : n534 2 # ASSIGN : n535 2 # ASSIGN : n536 4 # ASSIGN : n537 4 # ASSIGN : n538 4 # ASSIGN : n539 4 # ASSIGN : n540 2 # ASSIGN : n541 2 # ASSIGN : n542 2 # ASSIGN : n543 2 # ASSIGN : n544 4 # ASSIGN : n545 2 # ASSIGN : n546 2 # ASSIGN : n547 4 # ASSIGN : n548 4 # ASSIGN : n549 4 # ASSIGN : n550 4 # ASSIGN : n551 2 # ASSIGN : n552 2 # ASSIGN : n553 4 # ASSIGN : n554 4 # ASSIGN : n555 4 # ASSIGN : n556 4 # ASSIGN : n557 4 # ASSIGN : n558 4 # ASSIGN : n559 4 # ASSIGN : n560 4 # ASSIGN : n561 2 # ASSIGN : n562 2 # ASSIGN : n563 4 # ASSIGN : n564 2 # ASSIGN : n565 2 # ASSIGN : n566 2 # ASSIGN : n567 2 # ASSIGN : n568 4 # ASSIGN : n569 4 # ASSIGN : n570 4 # ASSIGN : n571 4 # ASSIGN : n572 4 # ASSIGN : n573 4 # ASSIGN : n574 4 # ASSIGN : n575 4 # ASSIGN : n576 2 # ASSIGN : n577 2 # ASSIGN : n578 4 # ASSIGN : n579 4 # ASSIGN : n580 4 # ASSIGN : n581 4 # ASSIGN : n582 2 # ASSIGN : n583 2 # ASSIGN : n584 2 # ASSIGN : n585 2 # ASSIGN : n586 4 # ASSIGN : n587 2 # ASSIGN : n588 2 # ASSIGN : n589 4 # ASSIGN : n590 4 # ASSIGN : n591 4 # ASSIGN : n592 4 # ASSIGN : n593 2 # ASSIGN : n594 2 # ASSIGN : n595 4 # ASSIGN : n596 4 # ASSIGN : n597 4 # ASSIGN : n598 2 # ASSIGN : n599 4 # ASSIGN : n600 4 # ASSIGN : n601 4 # ASSIGN : n602 4 # ASSIGN : n603 2 # ASSIGN : n604 2 # ASSIGN : n605 4 # ASSIGN : n606 2 # ASSIGN : n607 2 # ASSIGN : n608 2 # ASSIGN : n609 2 # ASSIGN : n610 4 # ASSIGN : n611 2 # ASSIGN : n612 2 # ASSIGN : n613 2 # ASSIGN : n614 2 # ASSIGN : n615 4 # ASSIGN : n616 9 # ASSIGN : n617 7 # ASSIGN : n618 5 # ASSIGN : n619 7 # ASSIGN : n620 5 # ASSIGN : n621 7 # ASSIGN : n622 7 # ASSIGN : n623 7 # ASSIGN : n624 7 # ASSIGN : n625 7 # ASSIGN : n626 7 # ASSIGN : n627 7 # ASSIGN : n628 7 # ASSIGN : n629 7 # ASSIGN : n630 7 # ASSIGN : n631 5 # ASSIGN : n632 7 # ASSIGN : n633 7 # ASSIGN : n634 3 # ASSIGN : n635 7 # ASSIGN : n636 7 # ASSIGN : n637 7 # ASSIGN : n638 7 # ASSIGN : n639 7 # ASSIGN : n640 7 # ASSIGN : n641 7 # ASSIGN : n642 3 # ASSIGN : n643 9 # ASSIGN : n644 7 # ASSIGN : n645 7 # ASSIGN : n646 7 # ASSIGN : n647 7 # ASSIGN : n648 7 # ASSIGN : n649 7 # ASSIGN : n650 7 # ASSIGN : n651 7 # ASSIGN : n652 5 # ASSIGN : n653 7 # ASSIGN : n654 7 # ASSIGN : n655 7 # ASSIGN : n656 7 # ASSIGN : n657 7 # ASSIGN : n658 7 # ASSIGN : n659 7 # ASSIGN : n660 5 # ASSIGN : n661 7 # ASSIGN : n662 5 # ASSIGN : n663 7 # ASSIGN : n664 7 # ASSIGN : n665 7 # ASSIGN : n666 3 # ASSIGN : n667 7 # ASSIGN : n668 7 # ASSIGN : n669 7 # ASSIGN : n670 7 # ASSIGN : n671 7 # ASSIGN : n672 7 # ASSIGN : n673 7 # ASSIGN : n674 7 # ASSIGN : n675 7 # ASSIGN : n676 7 # ASSIGN : n677 7 # ASSIGN : n678 7 # ASSIGN : n679 7 # ASSIGN : n680 7 # ASSIGN : n681 7 # ASSIGN : n682 7 # ASSIGN : n683 7 # ASSIGN : n684 7 # ASSIGN : n685 7 # ASSIGN : n686 7 # ASSIGN : n687 5 # ASSIGN : n688 7 # ASSIGN : n689 7 # ASSIGN : n690 7 # ASSIGN : n691 7 # ASSIGN : n692 7 # ASSIGN : n693 7 # ASSIGN : n694 7 # ASSIGN : n695 7 # ASSIGN : n696 3 # ASSIGN : n697 7 # ASSIGN : n698 7 # ASSIGN : n699 7 # ASSIGN : n700 7 # ASSIGN : n701 7 # ASSIGN : n702 7 # ASSIGN : n703 7 # ASSIGN : n704 7 # ASSIGN : n705 7 # ASSIGN : n706 7 # ASSIGN : n707 7 # ASSIGN : n708 7 # ASSIGN : n709 7 # ASSIGN : n710 7 # ASSIGN : n711 7 # ASSIGN : n712 7 # ASSIGN : n713 7 # ASSIGN : n714 7 # ASSIGN : n715 7 # ASSIGN : n716 7 # ASSIGN : n717 7 # ASSIGN : n718 7 # ASSIGN : n719 3 # ASSIGN : n720 7 # ASSIGN : n721 7 # ASSIGN : n722 7 # ASSIGN : n723 7 # ASSIGN : n724 7 # ASSIGN : n725 7 # ASSIGN : n726 7 # ASSIGN : n727 7 # ASSIGN : n728 7 # ASSIGN : n729 7 # ASSIGN : n730 7 # ASSIGN : n731 7 # ASSIGN : n732 7 # ASSIGN : n733 7 # ASSIGN : n734 7 # ASSIGN : n735 7 # ASSIGN : n736 7 # ASSIGN : n737 7 # ASSIGN : n738 3 # ASSIGN : n739 7 # ASSIGN : n740 7 # ASSIGN : n741 7 # ASSIGN : n742 7 # ASSIGN : n743 7 # ASSIGN : n744 7 # ASSIGN : n745 7 # ASSIGN : n746 7 # ASSIGN : n747 7 # ASSIGN : n748 7 # ASSIGN : n749 7 # ASSIGN : n750 7 # ASSIGN : n751 7 # ASSIGN : n752 7 # ASSIGN : n753 7 # ASSIGN : n754 7 # ASSIGN : n755 7 # ASSIGN : n756 7 # ASSIGN : n757 7 # ASSIGN : n758 7 # ASSIGN : n759 7 # ASSIGN : n760 7 # ASSIGN : n761 7 # ASSIGN : n762 7 # ASSIGN : n763 7 # ASSIGN : n764 7 # ASSIGN : n765 5 # ASSIGN : n766 7 # ASSIGN : n767 7 # ASSIGN : n768 7 # ASSIGN : n769 7 # ASSIGN : n770 7 # ASSIGN : n771 4 # ASSIGN : n772 4 # ASSIGN : n773 4 # ASSIGN : n774 2 # ASSIGN : n775 4 # ASSIGN : n776 4 # ASSIGN : n777 2 # ASSIGN : n778 2 # ASSIGN : n779 4 # ASSIGN : n780 4 # ASSIGN : n781 4 # ASSIGN : n782 4 # ASSIGN : n783 4 # ASSIGN : n784 4 # ASSIGN : n785 2 # ASSIGN : n786 2 # ASSIGN : n787 2 # ASSIGN : n788 4 # ASSIGN : n789 2 # ASSIGN : n790 2 # ASSIGN : n791 2 # ASSIGN : n792 6 # ASSIGN : n793 4 # ASSIGN : n794 4 # ASSIGN : n795 4 # ASSIGN : n796 2 # ASSIGN : n797 4 # ASSIGN : n798 2 # ASSIGN : n799 2 # ASSIGN : n800 2 # ASSIGN : n801 4 # ASSIGN : n802 2 # ASSIGN : n803 4 # ASSIGN : n804 4 # ASSIGN : n805 4 # ASSIGN : n806 2 # ASSIGN : n807 2 # ASSIGN : n808 2 # ASSIGN : n809 2 # ASSIGN : n810 2 # ASSIGN : n811 2 # ASSIGN : n812 2 # ASSIGN : n813 4 # ASSIGN : n814 4 # ASSIGN : n815 4 # ASSIGN : n816 2 # ASSIGN : n817 2 # ASSIGN : n818 2 # ASSIGN : n819 4 # ASSIGN : n820 2 # ASSIGN : n821 4 # ASSIGN : n822 4 # ASSIGN : n823 4 # ASSIGN : n824 4 # ASSIGN : n825 4 # ASSIGN : n826 4 # ASSIGN : n827 2 # ASSIGN : n828 2 # ASSIGN : n829 4 # ASSIGN : n830 2 # ASSIGN : n831 2 # ASSIGN : n832 2 # ASSIGN : n833 2 # ASSIGN : n834 4 # ASSIGN : n835 4 # ASSIGN : n836 4 # ASSIGN : n837 4 # ASSIGN : n838 2 # ASSIGN : n839 4 # ASSIGN : n840 2 # ASSIGN : n841 2 # ASSIGN : n842 2 # ASSIGN : n843 2 # ASSIGN : n844 4 # ASSIGN : n845 4 # ASSIGN : n846 4 # ASSIGN : n847 4 # ASSIGN : n848 2 # ASSIGN : n849 2 # ASSIGN : n850 2 # ASSIGN : n851 2 # ASSIGN : n852 2 # ASSIGN : n853 2 # ASSIGN : n854 2 # ASSIGN : n855 4 # ASSIGN : n856 4 # ASSIGN : n857 4 # ASSIGN : n858 4 # ASSIGN : n859 2 # ASSIGN : n860 2 # ASSIGN : n861 4 # ASSIGN : n862 4 # ASSIGN : n863 4 # ASSIGN : n864 4 # ASSIGN : n865 4 # ASSIGN : n866 4 # ASSIGN : n867 4 # ASSIGN : n868 4 # ASSIGN : n869 2 # ASSIGN : n870 2 # ASSIGN : n871 4 # ASSIGN : n872 2 # ASSIGN : n873 2 # ASSIGN : n874 2 # ASSIGN : n875 2 # ASSIGN : n876 4 # ASSIGN : n877 4 # ASSIGN : n878 4 # ASSIGN : n879 4 # ASSIGN : n880 4 # ASSIGN : n881 4 # ASSIGN : n882 2 # ASSIGN : n883 2 # ASSIGN : n884 2 # ASSIGN : n885 2 # ASSIGN : n886 4 # ASSIGN : n887 4 # ASSIGN : n888 4 # ASSIGN : n889 4 # ASSIGN : n890 2 # ASSIGN : n891 4 # ASSIGN : n892 2 # ASSIGN : n893 2 # ASSIGN : n894 2 # ASSIGN : n895 2 # ASSIGN : n896 2 # ASSIGN : n897 4 # ASSIGN : n898 4 # ASSIGN : n899 4 # ASSIGN : n900 4 # ASSIGN : n901 2 # ASSIGN : n902 2 # ASSIGN : n903 4 # ASSIGN : n904 4 # ASSIGN : n905 4 # ASSIGN : n906 4 # ASSIGN : n907 4 # ASSIGN : n908 4 # ASSIGN : n909 4 # ASSIGN : n910 4 # ASSIGN : n911 2 # ASSIGN : n912 2 # ASSIGN : n913 4 # ASSIGN : n914 2 # ASSIGN : n915 2 # ASSIGN : n916 2 # ASSIGN : n917 2 # ASSIGN : n918 4 # ASSIGN : n919 2 # ASSIGN : n920 2 # ASSIGN : n921 2 # ASSIGN : n922 2 # ASSIGN : n923 2 # ASSIGN : n924 4 # ASSIGN : n925 5 # ASSIGN : n926 5 # ASSIGN : n927 5 # ASSIGN : n928 5 # ASSIGN : n929 5 # ASSIGN : n930 5 # ASSIGN : n931 5 # ASSIGN : n932 5 # ASSIGN : n933 5 # ASSIGN : n934 3 # ASSIGN : n935 5 # ASSIGN : n936 5 # ASSIGN : n937 5 # ASSIGN : n938 5 # ASSIGN : n939 5 # ASSIGN : n940 5 # ASSIGN : n941 5 # ASSIGN : n942 5 # ASSIGN : n943 5 # ASSIGN : n944 5 # ASSIGN : n945 5 # ASSIGN : n946 5 # ASSIGN : n947 5 # ASSIGN : n948 5 # ASSIGN : n949 5 # ASSIGN : n950 5 # ASSIGN : n951 5 # ASSIGN : n952 5 # ASSIGN : n953 5 # ASSIGN : n954 5 # ASSIGN : n955 5 # ASSIGN : n956 5 # ASSIGN : n957 5 # ASSIGN : n958 5 # ASSIGN : n959 5 # ASSIGN : n960 5 # ASSIGN : n961 5 # ASSIGN : n962 5 # ASSIGN : n963 5 # ASSIGN : n964 5 # ASSIGN : n965 5 # ASSIGN : n966 5 # ASSIGN : n967 5 # ASSIGN : n968 5 # ASSIGN : n969 5 # ASSIGN : n970 5 # ASSIGN : n971 5 # ASSIGN : n972 5 # ASSIGN : n973 5 # ASSIGN : n974 5 # ASSIGN : n975 5 # ASSIGN : n976 5 # ASSIGN : n977 5 # ASSIGN : n978 5 # ASSIGN : n979 5 # ASSIGN : n980 5 # ASSIGN : n981 5 # ASSIGN : n982 5 # ASSIGN : n983 5 # ASSIGN : n984 5 # ASSIGN : n985 5 # ASSIGN : n986 5 # ASSIGN : n987 5 # ASSIGN : n988 5 # ASSIGN : n989 5 # ASSIGN : n990 5 # ASSIGN : n991 5 # ASSIGN : n992 5 # ASSIGN : n993 5 # ASSIGN : n994 5 # ASSIGN : n995 5 # ASSIGN : n996 5 # ASSIGN : n997 5 # ASSIGN : n998 5 # ASSIGN : n999 5 # ASSIGN : n1000 5 # ASSIGN : n1001 5 # ASSIGN : n1002 5 # ASSIGN : n1003 5 # ASSIGN : n1004 5 # ASSIGN : n1005 5 # ASSIGN : n1006 5 # ASSIGN : n1007 5 # ASSIGN : n1008 5 # ASSIGN : n1009 5 # ASSIGN : n1010 5 # ASSIGN : n1011 5 # ASSIGN : n1012 5 # ASSIGN : n1013 5 # ASSIGN : n1014 5 # ASSIGN : n1015 5 # ASSIGN : n1016 5 # ASSIGN : n1017 5 # ASSIGN : n1018 5 # ASSIGN : n1019 5 # ASSIGN : n1020 5 # ASSIGN : n1021 5 # ASSIGN : n1022 5 # ASSIGN : n1023 5 # ASSIGN : n1024 5 # ASSIGN : n1025 5 # ASSIGN : n1026 3 # ASSIGN : n1027 5 # ASSIGN : n1028 5 # ASSIGN : n1029 5 # ASSIGN : n1030 5 # ASSIGN : n1031 5 # ASSIGN : n1032 5 # ASSIGN : n1033 5 # ASSIGN : n1034 5 # ASSIGN : n1035 5 # ASSIGN : n1036 5 # ASSIGN : n1037 5 # ASSIGN : n1038 5 # ASSIGN : n1039 5 # ASSIGN : n1040 5 # ASSIGN : n1041 5 # ASSIGN : n1042 5 # ASSIGN : n1043 5 # ASSIGN : n1044 5 # ASSIGN : n1045 5 # ASSIGN : n1046 5 # ASSIGN : n1047 5 # ASSIGN : n1048 5 # ASSIGN : n1049 5 # ASSIGN : n1050 5 # ASSIGN : n1051 5 # ASSIGN : n1052 5 # ASSIGN : n1053 5 # ASSIGN : n1054 5 # ASSIGN : n1055 5 # ASSIGN : n1056 5 # ASSIGN : n1057 5 # ASSIGN : n1058 5 # ASSIGN : n1059 5 # ASSIGN : n1060 5 # ASSIGN : n1061 5 # ASSIGN : n1062 5 # ASSIGN : n1063 5 # ASSIGN : n1064 5 # ASSIGN : n1065 5 # ASSIGN : n1066 5 # ASSIGN : n1067 5 # ASSIGN : n1068 5 # ASSIGN : n1069 8 # ASSIGN : n1070 8 # ASSIGN : n1071 8 # ASSIGN : n1072 8 # ASSIGN : n1073 5 # ASSIGN : n1074 8 # ASSIGN : n1075 8 # ASSIGN : n1076 8 # ASSIGN : n1077 5 # ASSIGN : n1078 8 # ASSIGN : n1079 9 # ASSIGN : n1080 3 # ASSIGN : n1081 4 # ASSIGN : n1082 5 # ASSIGN : n1083 8 # ASSIGN : n1084 7 # ASSIGN : n1085 6 SHOW_RESULT 9 END : 9 (0 seconds) [Thu Jul 6 14:05:10 2006] SHOW_RESULT 9 CPU : 0.0900000000000034 = 0.0900000000000034 + 0 + 0 + 0 # BOUND : color 8 9 MODIFY_CNF 8 BEGIN : [Thu Jul 6 14:05:10 2006] MODIFY_CNF 8 END : 12051740 bytes (0 seconds) [Thu Jul 6 14:05:10 2006] MODIFY_CNF 8 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 8 BEGIN : [Thu Jul 6 14:05:10 2006] CMD : minisat /tmp/csp2sat18628.cnf /tmp/csp2sat18628.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 238219 708677 | 79406 0 0 nan | 0.000 % | | 100 | 238219 708677 | 87346 100 745 7.5 | 39.143 % | | 252 | 238219 708677 | 96081 252 4285 17.0 | 39.143 % | | 478 | 238219 708677 | 105689 478 7458 15.6 | 39.143 % | | 816 | 238219 708677 | 116258 816 14876 18.2 | 39.143 % | | 1322 | 238219 708677 | 127884 1322 27151 20.5 | 39.143 % | | 2081 | 238219 708677 | 140672 2081 44354 21.3 | 39.143 % | | 3221 | 238219 708677 | 154739 3221 69916 21.7 | 39.143 % | | 4929 | 238219 708677 | 170213 4929 106039 21.5 | 39.143 % | | 7493 | 238219 708677 | 187235 7493 158498 21.2 | 39.143 % | | 11338 | 238219 708677 | 205958 11338 219804 19.4 | 39.143 % | | 17105 | 238219 708677 | 226554 17105 320821 18.8 | 39.143 % | | 25755 | 238219 708677 | 249210 25755 447118 17.4 | 39.143 % | | 38730 | 238219 708677 | 274131 38730 638935 16.5 | 39.143 % | | 58192 | 238219 708677 | 301544 58192 890292 15.3 | 39.143 % | | 87384 | 238219 708677 | 331698 87384 1289017 14.8 | 39.143 % | | 131174 | 238086 708281 | 364868 57790 802586 13.9 | 39.151 % | ============================================================================== restarts : 17 conflicts : 172534 (804 /sec) decisions : 235309 (1096 /sec) propagations : 37163201 (173118 /sec) conflict literals : 2410105 (25.39 % deleted) Memory used : 26.67 MB CPU time : 214.67 s UNSATISFIABLE VERIFY_CNF 8 END : (215 seconds) [Thu Jul 6 14:08:45 2006] VERIFY_CNF 8 CPU : 214.75 = 0 + 0 + 214.67 + 0.08 # RESULT : color 8 UNSATISFIABLE # BOUND : color 9 9 MAIN END : (265 seconds) [Thu Jul 6 14:08:45 2006] MAIN CPU : 264.4 = 43.91 + 0.19 + 219.85 + 0.45