# TIMEOUT 7200 MAIN BEGIN : [Tue Jul 11 15:15:30 2006] READ BEGIN : csp/will199GPIA.csp [Tue Jul 11 15:15:30 2006] READ END : csp/will199GPIA.csp (11 seconds) [Tue Jul 11 15:15:41 2006] READ CPU : 11.02 = 10.86 + 0.16 + 0 + 0 # BOUND : color 2 11 GENERATE_CNF 11 BEGIN : [Tue Jul 11 15:15:41 2006] GENERATE_CNF 11 END : 22668 variables 171891 clauses 3256295 bytes (8 seconds) [Tue Jul 11 15:15:49 2006] GENERATE_CNF 11 CPU : 8.47 = 8.47 + 0 + 0 + 0 MODIFY_CNF 6 BEGIN : [Tue Jul 11 15:15:49 2006] MODIFY_CNF 6 END : 3256299 bytes (0 seconds) [Tue Jul 11 15:15:49 2006] MODIFY_CNF 6 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 6 BEGIN : [Tue Jul 11 15:15:49 2006] CMD : minisat /tmp/csp2sat13929.cnf /tmp/csp2sat13929.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 99960 303845 | 33320 0 0 nan | 0.000 % | | 101 | 99960 303845 | 36652 101 849 8.4 | 24.771 % | | 252 | 99961 303845 | 40317 251 2233 8.9 | 24.771 % | | 479 | 99961 303845 | 44348 478 3870 8.1 | 24.771 % | | 817 | 99965 303845 | 48783 811 6453 8.0 | 24.779 % | ============================================================================== restarts : 5 conflicts : 1306 (3530 /sec) decisions : 1767 (4776 /sec) propagations : 337661 (912597 /sec) conflict literals : 9517 (15.89 % deleted) Memory used : 8.29 MB CPU time : 0.37 s UNSATISFIABLE VERIFY_CNF 6 END : (1 seconds) [Tue Jul 11 15:15:50 2006] VERIFY_CNF 6 CPU : 0.39 = 0 + 0 + 0.37 + 0.02 # RESULT : color 6 UNSATISFIABLE # BOUND : color 7 11 MODIFY_CNF 9 BEGIN : [Tue Jul 11 15:15:50 2006] MODIFY_CNF 9 END : 3256299 bytes (0 seconds) [Tue Jul 11 15:15:50 2006] MODIFY_CNF 9 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 9 BEGIN : [Tue Jul 11 15:15:50 2006] CMD : minisat /tmp/csp2sat13929.cnf /tmp/csp2sat13929.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 140592 425741 | 46864 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 1 (5 /sec) decisions : 1145 (5452 /sec) propagations : 23325 (111071 /sec) conflict literals : 5 (0.00 % deleted) Memory used : 8.47 MB CPU time : 0.21 s SATISFIABLE VERIFY_CNF 9 END : (0 seconds) [Tue Jul 11 15:15:50 2006] VERIFY_CNF 9 CPU : 0.26 = 0 + 0.01 + 0.22 + 0.03 # RESULT : color 9 SATISFIABLE SHOW_RESULT 9 BEGIN : [Tue Jul 11 15:15:50 2006] # ASSIGN : color 9 # ASSIGN : n1 8 # ASSIGN : n2 1 # ASSIGN : n3 9 # ASSIGN : n4 3 # ASSIGN : n5 1 # ASSIGN : n6 2 # ASSIGN : n7 4 # ASSIGN : n8 1 # ASSIGN : n9 3 # ASSIGN : n10 2 # ASSIGN : n11 1 # ASSIGN : n12 6 # ASSIGN : n13 2 # ASSIGN : n14 5 # ASSIGN : n15 6 # ASSIGN : n16 1 # ASSIGN : n17 2 # ASSIGN : n18 6 # ASSIGN : n19 3 # ASSIGN : n20 7 # ASSIGN : n21 2 # ASSIGN : n22 8 # ASSIGN : n23 2 # ASSIGN : n24 9 # ASSIGN : n25 1 # ASSIGN : n26 2 # ASSIGN : n27 5 # ASSIGN : n28 3 # ASSIGN : n29 7 # ASSIGN : n30 3 # ASSIGN : n31 4 # ASSIGN : n32 5 # ASSIGN : n33 3 # ASSIGN : n34 4 # ASSIGN : n35 1 # ASSIGN : n36 1 # ASSIGN : n37 5 # ASSIGN : n38 4 # ASSIGN : n39 3 # ASSIGN : n40 5 # ASSIGN : n41 4 # ASSIGN : n42 2 # ASSIGN : n43 2 # ASSIGN : n44 3 # ASSIGN : n45 4 # ASSIGN : n46 2 # ASSIGN : n47 3 # ASSIGN : n48 6 # ASSIGN : n49 1 # ASSIGN : n50 2 # ASSIGN : n51 7 # ASSIGN : n52 8 # ASSIGN : n53 2 # ASSIGN : n54 9 # ASSIGN : n55 4 # ASSIGN : n56 5 # ASSIGN : n57 7 # ASSIGN : n58 3 # ASSIGN : n59 6 # ASSIGN : n60 7 # ASSIGN : n61 4 # ASSIGN : n62 2 # ASSIGN : n63 5 # ASSIGN : n64 1 # ASSIGN : n65 3 # ASSIGN : n66 2 # ASSIGN : n67 1 # ASSIGN : n68 3 # ASSIGN : n69 5 # ASSIGN : n70 4 # ASSIGN : n71 3 # ASSIGN : n72 2 # ASSIGN : n73 5 # ASSIGN : n74 3 # ASSIGN : n75 9 # ASSIGN : n76 5 # ASSIGN : n77 6 # ASSIGN : n78 4 # ASSIGN : n79 3 # ASSIGN : n80 2 # ASSIGN : n81 9 # ASSIGN : n82 6 # ASSIGN : n83 2 # ASSIGN : n84 5 # ASSIGN : n85 9 # ASSIGN : n86 1 # ASSIGN : n87 4 # ASSIGN : n88 2 # ASSIGN : n89 5 # ASSIGN : n90 4 # ASSIGN : n91 6 # ASSIGN : n92 2 # ASSIGN : n93 8 # ASSIGN : n94 3 # ASSIGN : n95 4 # ASSIGN : n96 6 # ASSIGN : n97 9 # ASSIGN : n98 3 # ASSIGN : n99 6 # ASSIGN : n100 4 # ASSIGN : n101 7 # ASSIGN : n102 8 # ASSIGN : n103 4 # ASSIGN : n104 3 # ASSIGN : n105 1 # ASSIGN : n106 1 # ASSIGN : n107 2 # ASSIGN : n108 4 # ASSIGN : n109 1 # ASSIGN : n110 7 # ASSIGN : n111 3 # ASSIGN : n112 4 # ASSIGN : n113 4 # ASSIGN : n114 6 # ASSIGN : n115 3 # ASSIGN : n116 4 # ASSIGN : n117 6 # ASSIGN : n118 2 # ASSIGN : n119 3 # ASSIGN : n120 1 # ASSIGN : n121 3 # ASSIGN : n122 5 # ASSIGN : n123 6 # ASSIGN : n124 3 # ASSIGN : n125 7 # ASSIGN : n126 8 # ASSIGN : n127 4 # ASSIGN : n128 2 # ASSIGN : n129 9 # ASSIGN : n130 1 # ASSIGN : n131 2 # ASSIGN : n132 9 # ASSIGN : n133 3 # ASSIGN : n134 3 # ASSIGN : n135 2 # ASSIGN : n136 7 # ASSIGN : n137 3 # ASSIGN : n138 2 # ASSIGN : n139 1 # ASSIGN : n140 4 # ASSIGN : n141 3 # ASSIGN : n142 9 # ASSIGN : n143 5 # ASSIGN : n144 3 # ASSIGN : n145 9 # ASSIGN : n146 4 # ASSIGN : n147 7 # ASSIGN : n148 2 # ASSIGN : n149 9 # ASSIGN : n150 5 # ASSIGN : n151 2 # ASSIGN : n152 4 # ASSIGN : n153 3 # ASSIGN : n154 1 # ASSIGN : n155 1 # ASSIGN : n156 2 # ASSIGN : n157 3 # ASSIGN : n158 1 # ASSIGN : n159 2 # ASSIGN : n160 4 # ASSIGN : n161 3 # ASSIGN : n162 8 # ASSIGN : n163 3 # ASSIGN : n164 4 # ASSIGN : n165 8 # ASSIGN : n166 3 # ASSIGN : n167 5 # ASSIGN : n168 4 # ASSIGN : n169 1 # ASSIGN : n170 4 # ASSIGN : n171 5 # ASSIGN : n172 6 # ASSIGN : n173 4 # ASSIGN : n174 5 # ASSIGN : n175 3 # ASSIGN : n176 8 # ASSIGN : n177 6 # ASSIGN : n178 7 # ASSIGN : n179 8 # ASSIGN : n180 9 # ASSIGN : n181 5 # ASSIGN : n182 2 # ASSIGN : n183 4 # ASSIGN : n184 6 # ASSIGN : n185 3 # ASSIGN : n186 9 # ASSIGN : n187 1 # ASSIGN : n188 2 # ASSIGN : n189 3 # ASSIGN : n190 6 # ASSIGN : n191 5 # ASSIGN : n192 4 # ASSIGN : n193 6 # ASSIGN : n194 7 # ASSIGN : n195 3 # ASSIGN : n196 1 # ASSIGN : n197 4 # ASSIGN : n198 6 # ASSIGN : n199 3 # ASSIGN : n200 4 # ASSIGN : n201 6 # ASSIGN : n202 7 # ASSIGN : n203 3 # ASSIGN : n204 8 # ASSIGN : n205 3 # ASSIGN : n206 9 # ASSIGN : n207 2 # ASSIGN : n208 3 # ASSIGN : n209 4 # ASSIGN : n210 1 # ASSIGN : n211 2 # ASSIGN : n212 5 # ASSIGN : n213 3 # ASSIGN : n214 1 # ASSIGN : n215 2 # ASSIGN : n216 5 # ASSIGN : n217 4 # ASSIGN : n218 1 # ASSIGN : n219 1 # ASSIGN : n220 8 # ASSIGN : n221 5 # ASSIGN : n222 6 # ASSIGN : n223 1 # ASSIGN : n224 9 # ASSIGN : n225 5 # ASSIGN : n226 6 # ASSIGN : n227 1 # ASSIGN : n228 6 # ASSIGN : n229 2 # ASSIGN : n230 3 # ASSIGN : n231 1 # ASSIGN : n232 6 # ASSIGN : n233 2 # ASSIGN : n234 3 # ASSIGN : n235 4 # ASSIGN : n236 3 # ASSIGN : n237 1 # ASSIGN : n238 2 # ASSIGN : n239 4 # ASSIGN : n240 3 # ASSIGN : n241 1 # ASSIGN : n242 2 # ASSIGN : n243 2 # ASSIGN : n244 1 # ASSIGN : n245 5 # ASSIGN : n246 6 # ASSIGN : n247 2 # ASSIGN : n248 1 # ASSIGN : n249 6 # ASSIGN : n250 4 # ASSIGN : n251 2 # ASSIGN : n252 3 # ASSIGN : n253 6 # ASSIGN : n254 1 # ASSIGN : n255 2 # ASSIGN : n256 3 # ASSIGN : n257 1 # ASSIGN : n258 6 # ASSIGN : n259 6 # ASSIGN : n260 8 # ASSIGN : n261 4 # ASSIGN : n262 1 # ASSIGN : n263 6 # ASSIGN : n264 8 # ASSIGN : n265 4 # ASSIGN : n266 7 # ASSIGN : n267 2 # ASSIGN : n268 9 # ASSIGN : n269 4 # ASSIGN : n270 1 # ASSIGN : n271 2 # ASSIGN : n272 9 # ASSIGN : n273 3 # ASSIGN : n274 1 # ASSIGN : n275 2 # ASSIGN : n276 3 # ASSIGN : n277 4 # ASSIGN : n278 1 # ASSIGN : n279 2 # ASSIGN : n280 7 # ASSIGN : n281 4 # ASSIGN : n282 8 # ASSIGN : n283 1 # ASSIGN : n284 7 # ASSIGN : n285 6 # ASSIGN : n286 3 # ASSIGN : n287 1 # ASSIGN : n288 7 # ASSIGN : n289 5 # ASSIGN : n290 6 # ASSIGN : n291 2 # ASSIGN : n292 1 # ASSIGN : n293 5 # ASSIGN : n294 6 # ASSIGN : n295 2 # ASSIGN : n296 1 # ASSIGN : n297 5 # ASSIGN : n298 3 # ASSIGN : n299 1 # ASSIGN : n300 7 # ASSIGN : n301 2 # ASSIGN : n302 4 # ASSIGN : n303 1 # ASSIGN : n304 7 # ASSIGN : n305 3 # ASSIGN : n306 4 # ASSIGN : n307 1 # ASSIGN : n308 6 # ASSIGN : n309 2 # ASSIGN : n310 3 # ASSIGN : n311 1 # ASSIGN : n312 6 # ASSIGN : n313 2 # ASSIGN : n314 3 # ASSIGN : n315 2 # ASSIGN : n316 7 # ASSIGN : n317 3 # ASSIGN : n318 1 # ASSIGN : n319 4 # ASSIGN : n320 7 # ASSIGN : n321 8 # ASSIGN : n322 1 # ASSIGN : n323 1 # ASSIGN : n324 4 # ASSIGN : n325 2 # ASSIGN : n326 3 # ASSIGN : n327 1 # ASSIGN : n328 4 # ASSIGN : n329 2 # ASSIGN : n330 3 # ASSIGN : n331 4 # ASSIGN : n332 5 # ASSIGN : n333 8 # ASSIGN : n334 1 # ASSIGN : n335 2 # ASSIGN : n336 2 # ASSIGN : n337 7 # ASSIGN : n338 4 # ASSIGN : n339 3 # ASSIGN : n340 1 # ASSIGN : n341 5 # ASSIGN : n342 4 # ASSIGN : n343 9 # ASSIGN : n344 1 # ASSIGN : n345 2 # ASSIGN : n346 6 # ASSIGN : n347 3 # ASSIGN : n348 1 # ASSIGN : n349 4 # ASSIGN : n350 5 # ASSIGN : n351 9 # ASSIGN : n352 7 # ASSIGN : n353 4 # ASSIGN : n354 8 # ASSIGN : n355 2 # ASSIGN : n356 6 # ASSIGN : n357 4 # ASSIGN : n358 2 # ASSIGN : n359 5 # ASSIGN : n360 1 # ASSIGN : n361 1 # ASSIGN : n362 2 # ASSIGN : n363 6 # ASSIGN : n364 3 # ASSIGN : n365 4 # ASSIGN : n366 4 # ASSIGN : n367 5 # ASSIGN : n368 3 # ASSIGN : n369 1 # ASSIGN : n370 2 # ASSIGN : n371 1 # ASSIGN : n372 6 # ASSIGN : n373 2 # ASSIGN : n374 8 # ASSIGN : n375 9 # ASSIGN : n376 5 # ASSIGN : n377 2 # ASSIGN : n378 1 # ASSIGN : n379 3 # ASSIGN : n380 4 # ASSIGN : n381 4 # ASSIGN : n382 1 # ASSIGN : n383 5 # ASSIGN : n384 2 # ASSIGN : n385 3 # ASSIGN : n386 2 # ASSIGN : n387 7 # ASSIGN : n388 8 # ASSIGN : n389 3 # ASSIGN : n390 1 # ASSIGN : n391 3 # ASSIGN : n392 4 # ASSIGN : n393 9 # ASSIGN : n394 1 # ASSIGN : n395 2 # ASSIGN : n396 1 # ASSIGN : n397 9 # ASSIGN : n398 4 # ASSIGN : n399 5 # ASSIGN : n400 2 # ASSIGN : n401 1 # ASSIGN : n402 5 # ASSIGN : n403 6 # ASSIGN : n404 2 # ASSIGN : n405 3 # ASSIGN : n406 6 # ASSIGN : n407 1 # ASSIGN : n408 5 # ASSIGN : n409 1 # ASSIGN : n410 8 # ASSIGN : n411 2 # ASSIGN : n412 1 # ASSIGN : n413 8 # ASSIGN : n414 2 # ASSIGN : n415 6 # ASSIGN : n416 1 # ASSIGN : n417 2 # ASSIGN : n418 6 # ASSIGN : n419 3 # ASSIGN : n420 5 # ASSIGN : n421 1 # ASSIGN : n422 2 # ASSIGN : n423 5 # ASSIGN : n424 7 # ASSIGN : n425 2 # ASSIGN : n426 3 # ASSIGN : n427 4 # ASSIGN : n428 2 # ASSIGN : n429 3 # ASSIGN : n430 4 # ASSIGN : n431 1 # ASSIGN : n432 3 # ASSIGN : n433 1 # ASSIGN : n434 9 # ASSIGN : n435 2 # ASSIGN : n436 1 # ASSIGN : n437 9 # ASSIGN : n438 2 # ASSIGN : n439 5 # ASSIGN : n440 1 # ASSIGN : n441 4 # ASSIGN : n442 5 # ASSIGN : n443 1 # ASSIGN : n444 2 # ASSIGN : n445 4 # ASSIGN : n446 3 # ASSIGN : n447 2 # ASSIGN : n448 4 # ASSIGN : n449 3 # ASSIGN : n450 1 # ASSIGN : n451 2 # ASSIGN : n452 9 # ASSIGN : n453 1 # ASSIGN : n454 2 # ASSIGN : n455 9 # ASSIGN : n456 1 # ASSIGN : n457 3 # ASSIGN : n458 2 # ASSIGN : n459 1 # ASSIGN : n460 3 # ASSIGN : n461 2 # ASSIGN : n462 4 # ASSIGN : n463 1 # ASSIGN : n464 2 # ASSIGN : n465 5 # ASSIGN : n466 1 # ASSIGN : n467 2 # ASSIGN : n468 5 # ASSIGN : n469 1 # ASSIGN : n470 2 # ASSIGN : n471 3 # ASSIGN : n472 4 # ASSIGN : n473 1 # ASSIGN : n474 5 # ASSIGN : n475 6 # ASSIGN : n476 1 # ASSIGN : n477 8 # ASSIGN : n478 2 # ASSIGN : n479 1 # ASSIGN : n480 7 # ASSIGN : n481 8 # ASSIGN : n482 1 # ASSIGN : n483 9 # ASSIGN : n484 3 # ASSIGN : n485 1 # ASSIGN : n486 2 # ASSIGN : n487 3 # ASSIGN : n488 1 # ASSIGN : n489 2 # ASSIGN : n490 6 # ASSIGN : n491 4 # ASSIGN : n492 5 # ASSIGN : n493 6 # ASSIGN : n494 1 # ASSIGN : n495 5 # ASSIGN : n496 1 # ASSIGN : n497 8 # ASSIGN : n498 2 # ASSIGN : n499 1 # ASSIGN : n500 8 # ASSIGN : n501 2 # ASSIGN : n502 6 # ASSIGN : n503 1 # ASSIGN : n504 2 # ASSIGN : n505 6 # ASSIGN : n506 3 # ASSIGN : n507 5 # ASSIGN : n508 1 # ASSIGN : n509 2 # ASSIGN : n510 5 # ASSIGN : n511 1 # ASSIGN : n512 2 # ASSIGN : n513 3 # ASSIGN : n514 4 # ASSIGN : n515 1 # ASSIGN : n516 3 # ASSIGN : n517 4 # ASSIGN : n518 1 # ASSIGN : n519 3 # ASSIGN : n520 1 # ASSIGN : n521 9 # ASSIGN : n522 2 # ASSIGN : n523 1 # ASSIGN : n524 9 # ASSIGN : n525 2 # ASSIGN : n526 5 # ASSIGN : n527 1 # ASSIGN : n528 4 # ASSIGN : n529 5 # ASSIGN : n530 1 # ASSIGN : n531 2 # ASSIGN : n532 4 # ASSIGN : n533 3 # ASSIGN : n534 2 # ASSIGN : n535 4 # ASSIGN : n536 3 # ASSIGN : n537 1 # ASSIGN : n538 2 # ASSIGN : n539 9 # ASSIGN : n540 1 # ASSIGN : n541 2 # ASSIGN : n542 9 # ASSIGN : n543 1 # ASSIGN : n544 3 # ASSIGN : n545 2 # ASSIGN : n546 1 # ASSIGN : n547 3 # ASSIGN : n548 2 # ASSIGN : n549 4 # ASSIGN : n550 1 # ASSIGN : n551 2 # ASSIGN : n552 5 # ASSIGN : n553 1 # ASSIGN : n554 2 # ASSIGN : n555 5 # ASSIGN : n556 1 # ASSIGN : n557 2 # ASSIGN : n558 3 # ASSIGN : n559 1 # ASSIGN : n560 2 # ASSIGN : n561 3 # ASSIGN : n562 3 # ASSIGN : n563 1 # ASSIGN : n564 2 # ASSIGN : n565 9 # ASSIGN : n566 2 # ASSIGN : n567 1 # ASSIGN : n568 2 # ASSIGN : n569 3 # ASSIGN : n570 4 # ASSIGN : n571 5 # ASSIGN : n572 6 # ASSIGN : n573 7 # ASSIGN : n574 8 # ASSIGN : n575 3 # ASSIGN : n576 2 # ASSIGN : n577 4 # ASSIGN : n578 8 # ASSIGN : n579 1 # ASSIGN : n580 2 # ASSIGN : n581 3 # ASSIGN : n582 6 # ASSIGN : n583 2 # ASSIGN : n584 4 # ASSIGN : n585 5 # ASSIGN : n586 3 # ASSIGN : n587 6 # ASSIGN : n588 7 # ASSIGN : n589 8 # ASSIGN : n590 7 # ASSIGN : n591 2 # ASSIGN : n592 5 # ASSIGN : n593 3 # ASSIGN : n594 8 # ASSIGN : n595 1 # ASSIGN : n596 9 # ASSIGN : n597 1 # ASSIGN : n598 4 # ASSIGN : n599 5 # ASSIGN : n600 3 # ASSIGN : n601 8 # ASSIGN : n602 1 # ASSIGN : n603 4 # ASSIGN : n604 2 # ASSIGN : n605 4 # ASSIGN : n606 3 # ASSIGN : n607 5 # ASSIGN : n608 6 # ASSIGN : n609 7 # ASSIGN : n610 9 # ASSIGN : n611 1 # ASSIGN : n612 2 # ASSIGN : n613 3 # ASSIGN : n614 5 # ASSIGN : n615 2 # ASSIGN : n616 7 # ASSIGN : n617 8 # ASSIGN : n618 3 # ASSIGN : n619 5 # ASSIGN : n620 4 # ASSIGN : n621 5 # ASSIGN : n622 4 # ASSIGN : n623 2 # ASSIGN : n624 1 # ASSIGN : n625 3 # ASSIGN : n626 5 # ASSIGN : n627 6 # ASSIGN : n628 7 # ASSIGN : n629 8 # ASSIGN : n630 2 # ASSIGN : n631 1 # ASSIGN : n632 3 # ASSIGN : n633 9 # ASSIGN : n634 2 # ASSIGN : n635 1 # ASSIGN : n636 2 # ASSIGN : n637 3 # ASSIGN : n638 1 # ASSIGN : n639 2 # ASSIGN : n640 3 # ASSIGN : n641 4 # ASSIGN : n642 5 # ASSIGN : n643 1 # ASSIGN : n644 2 # ASSIGN : n645 5 # ASSIGN : n646 1 # ASSIGN : n647 2 # ASSIGN : n648 3 # ASSIGN : n649 4 # ASSIGN : n650 5 # ASSIGN : n651 6 # ASSIGN : n652 7 # ASSIGN : n653 8 # ASSIGN : n654 9 # ASSIGN : n655 9 # ASSIGN : n656 9 # ASSIGN : n657 9 # ASSIGN : n658 9 # ASSIGN : n659 9 # ASSIGN : n660 9 # ASSIGN : n661 9 # ASSIGN : n662 1 # ASSIGN : n663 2 # ASSIGN : n664 4 # ASSIGN : n665 5 # ASSIGN : n666 3 # ASSIGN : n667 6 # ASSIGN : n668 1 # ASSIGN : n669 2 # ASSIGN : n670 3 # ASSIGN : n671 4 # ASSIGN : n672 7 # ASSIGN : n673 1 # ASSIGN : n674 2 # ASSIGN : n675 4 # ASSIGN : n676 5 # ASSIGN : n677 1 # ASSIGN : n678 3 # ASSIGN : n679 2 # ASSIGN : n680 9 # ASSIGN : n681 1 # ASSIGN : n682 3 # ASSIGN : n683 2 # ASSIGN : n684 5 # ASSIGN : n685 3 # ASSIGN : n686 4 # ASSIGN : n687 1 # ASSIGN : n688 2 # ASSIGN : n689 5 # ASSIGN : n690 6 # ASSIGN : n691 7 # ASSIGN : n692 1 # ASSIGN : n693 2 # ASSIGN : n694 3 # ASSIGN : n695 8 # ASSIGN : n696 4 # ASSIGN : n697 5 # ASSIGN : n698 6 # ASSIGN : n699 7 # ASSIGN : n700 8 # ASSIGN : n701 9 SHOW_RESULT 9 END : 9 (0 seconds) [Tue Jul 11 15:15:50 2006] SHOW_RESULT 9 CPU : 0.0399999999999991 = 0.0399999999999991 + 0 + 0 + 0 # BOUND : color 7 9 MODIFY_CNF 8 BEGIN : [Tue Jul 11 15:15:50 2006] MODIFY_CNF 8 END : 3256299 bytes (0 seconds) [Tue Jul 11 15:15:50 2006] MODIFY_CNF 8 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 8 BEGIN : [Tue Jul 11 15:15:50 2006] CMD : minisat /tmp/csp2sat13929.cnf /tmp/csp2sat13929.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 127048 385109 | 42349 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 4 (17 /sec) decisions : 1204 (5017 /sec) propagations : 29631 (123462 /sec) conflict literals : 30 (3.23 % deleted) Memory used : 8.46 MB CPU time : 0.24 s SATISFIABLE VERIFY_CNF 8 END : (0 seconds) [Tue Jul 11 15:15:50 2006] VERIFY_CNF 8 CPU : 0.27 = 0 + 0 + 0.25 + 0.02 # RESULT : color 8 SATISFIABLE SHOW_RESULT 8 BEGIN : [Tue Jul 11 15:15:50 2006] # ASSIGN : color 8 # ASSIGN : n1 1 # ASSIGN : n2 2 # ASSIGN : n3 8 # ASSIGN : n4 3 # ASSIGN : n5 5 # ASSIGN : n6 1 # ASSIGN : n7 6 # ASSIGN : n8 5 # ASSIGN : n9 3 # ASSIGN : n10 4 # ASSIGN : n11 1 # ASSIGN : n12 6 # ASSIGN : n13 2 # ASSIGN : n14 7 # ASSIGN : n15 5 # ASSIGN : n16 1 # ASSIGN : n17 2 # ASSIGN : n18 5 # ASSIGN : n19 7 # ASSIGN : n20 6 # ASSIGN : n21 2 # ASSIGN : n22 3 # ASSIGN : n23 4 # ASSIGN : n24 1 # ASSIGN : n25 7 # ASSIGN : n26 4 # ASSIGN : n27 1 # ASSIGN : n28 2 # ASSIGN : n29 8 # ASSIGN : n30 2 # ASSIGN : n31 3 # ASSIGN : n32 6 # ASSIGN : n33 2 # ASSIGN : n34 3 # ASSIGN : n35 5 # ASSIGN : n36 2 # ASSIGN : n37 5 # ASSIGN : n38 3 # ASSIGN : n39 2 # ASSIGN : n40 4 # ASSIGN : n41 3 # ASSIGN : n42 1 # ASSIGN : n43 2 # ASSIGN : n44 4 # ASSIGN : n45 3 # ASSIGN : n46 8 # ASSIGN : n47 6 # ASSIGN : n48 3 # ASSIGN : n49 1 # ASSIGN : n50 5 # ASSIGN : n51 4 # ASSIGN : n52 2 # ASSIGN : n53 3 # ASSIGN : n54 4 # ASSIGN : n55 1 # ASSIGN : n56 2 # ASSIGN : n57 3 # ASSIGN : n58 6 # ASSIGN : n59 7 # ASSIGN : n60 3 # ASSIGN : n61 1 # ASSIGN : n62 2 # ASSIGN : n63 4 # ASSIGN : n64 6 # ASSIGN : n65 7 # ASSIGN : n66 5 # ASSIGN : n67 6 # ASSIGN : n68 2 # ASSIGN : n69 8 # ASSIGN : n70 3 # ASSIGN : n71 5 # ASSIGN : n72 6 # ASSIGN : n73 4 # ASSIGN : n74 5 # ASSIGN : n75 6 # ASSIGN : n76 2 # ASSIGN : n77 7 # ASSIGN : n78 6 # ASSIGN : n79 3 # ASSIGN : n80 2 # ASSIGN : n81 5 # ASSIGN : n82 8 # ASSIGN : n83 7 # ASSIGN : n84 2 # ASSIGN : n85 2 # ASSIGN : n86 1 # ASSIGN : n87 3 # ASSIGN : n88 7 # ASSIGN : n89 1 # ASSIGN : n90 8 # ASSIGN : n91 4 # ASSIGN : n92 1 # ASSIGN : n93 4 # ASSIGN : n94 5 # ASSIGN : n95 1 # ASSIGN : n96 6 # ASSIGN : n97 2 # ASSIGN : n98 3 # ASSIGN : n99 5 # ASSIGN : n100 6 # ASSIGN : n101 2 # ASSIGN : n102 5 # ASSIGN : n103 6 # ASSIGN : n104 3 # ASSIGN : n105 7 # ASSIGN : n106 2 # ASSIGN : n107 6 # ASSIGN : n108 5 # ASSIGN : n109 4 # ASSIGN : n110 6 # ASSIGN : n111 1 # ASSIGN : n112 5 # ASSIGN : n113 7 # ASSIGN : n114 4 # ASSIGN : n115 3 # ASSIGN : n116 5 # ASSIGN : n117 4 # ASSIGN : n118 2 # ASSIGN : n119 3 # ASSIGN : n120 1 # ASSIGN : n121 3 # ASSIGN : n122 6 # ASSIGN : n123 7 # ASSIGN : n124 3 # ASSIGN : n125 8 # ASSIGN : n126 4 # ASSIGN : n127 4 # ASSIGN : n128 2 # ASSIGN : n129 1 # ASSIGN : n130 4 # ASSIGN : n131 2 # ASSIGN : n132 1 # ASSIGN : n133 6 # ASSIGN : n134 3 # ASSIGN : n135 2 # ASSIGN : n136 7 # ASSIGN : n137 8 # ASSIGN : n138 2 # ASSIGN : n139 5 # ASSIGN : n140 4 # ASSIGN : n141 2 # ASSIGN : n142 3 # ASSIGN : n143 1 # ASSIGN : n144 2 # ASSIGN : n145 7 # ASSIGN : n146 5 # ASSIGN : n147 4 # ASSIGN : n148 8 # ASSIGN : n149 4 # ASSIGN : n150 3 # ASSIGN : n151 8 # ASSIGN : n152 4 # ASSIGN : n153 5 # ASSIGN : n154 2 # ASSIGN : n155 6 # ASSIGN : n156 4 # ASSIGN : n157 5 # ASSIGN : n158 8 # ASSIGN : n159 7 # ASSIGN : n160 3 # ASSIGN : n161 5 # ASSIGN : n162 8 # ASSIGN : n163 2 # ASSIGN : n164 6 # ASSIGN : n165 8 # ASSIGN : n166 2 # ASSIGN : n167 1 # ASSIGN : n168 5 # ASSIGN : n169 8 # ASSIGN : n170 2 # ASSIGN : n171 6 # ASSIGN : n172 7 # ASSIGN : n173 2 # ASSIGN : n174 5 # ASSIGN : n175 3 # ASSIGN : n176 3 # ASSIGN : n177 1 # ASSIGN : n178 5 # ASSIGN : n179 8 # ASSIGN : n180 1 # ASSIGN : n181 4 # ASSIGN : n182 2 # ASSIGN : n183 8 # ASSIGN : n184 5 # ASSIGN : n185 3 # ASSIGN : n186 4 # ASSIGN : n187 1 # ASSIGN : n188 3 # ASSIGN : n189 2 # ASSIGN : n190 7 # ASSIGN : n191 6 # ASSIGN : n192 3 # ASSIGN : n193 7 # ASSIGN : n194 6 # ASSIGN : n195 5 # ASSIGN : n196 4 # ASSIGN : n197 3 # ASSIGN : n198 6 # ASSIGN : n199 5 # ASSIGN : n200 7 # ASSIGN : n201 6 # ASSIGN : n202 5 # ASSIGN : n203 2 # ASSIGN : n204 1 # ASSIGN : n205 2 # ASSIGN : n206 5 # ASSIGN : n207 7 # ASSIGN : n208 2 # ASSIGN : n209 3 # ASSIGN : n210 8 # ASSIGN : n211 2 # ASSIGN : n212 4 # ASSIGN : n213 3 # ASSIGN : n214 1 # ASSIGN : n215 2 # ASSIGN : n216 4 # ASSIGN : n217 3 # ASSIGN : n218 1 # ASSIGN : n219 3 # ASSIGN : n220 5 # ASSIGN : n221 1 # ASSIGN : n222 2 # ASSIGN : n223 6 # ASSIGN : n224 7 # ASSIGN : n225 1 # ASSIGN : n226 2 # ASSIGN : n227 1 # ASSIGN : n228 4 # ASSIGN : n229 2 # ASSIGN : n230 3 # ASSIGN : n231 1 # ASSIGN : n232 4 # ASSIGN : n233 2 # ASSIGN : n234 3 # ASSIGN : n235 5 # ASSIGN : n236 3 # ASSIGN : n237 1 # ASSIGN : n238 2 # ASSIGN : n239 5 # ASSIGN : n240 3 # ASSIGN : n241 1 # ASSIGN : n242 2 # ASSIGN : n243 4 # ASSIGN : n244 8 # ASSIGN : n245 1 # ASSIGN : n246 2 # ASSIGN : n247 4 # ASSIGN : n248 8 # ASSIGN : n249 1 # ASSIGN : n250 3 # ASSIGN : n251 6 # ASSIGN : n252 2 # ASSIGN : n253 7 # ASSIGN : n254 1 # ASSIGN : n255 6 # ASSIGN : n256 2 # ASSIGN : n257 1 # ASSIGN : n258 4 # ASSIGN : n259 7 # ASSIGN : n260 2 # ASSIGN : n261 5 # ASSIGN : n262 1 # ASSIGN : n263 7 # ASSIGN : n264 2 # ASSIGN : n265 5 # ASSIGN : n266 8 # ASSIGN : n267 6 # ASSIGN : n268 4 # ASSIGN : n269 3 # ASSIGN : n270 1 # ASSIGN : n271 6 # ASSIGN : n272 4 # ASSIGN : n273 5 # ASSIGN : n274 7 # ASSIGN : n275 3 # ASSIGN : n276 8 # ASSIGN : n277 1 # ASSIGN : n278 2 # ASSIGN : n279 7 # ASSIGN : n280 8 # ASSIGN : n281 6 # ASSIGN : n282 4 # ASSIGN : n283 1 # ASSIGN : n284 3 # ASSIGN : n285 2 # ASSIGN : n286 6 # ASSIGN : n287 8 # ASSIGN : n288 7 # ASSIGN : n289 4 # ASSIGN : n290 5 # ASSIGN : n291 1 # ASSIGN : n292 2 # ASSIGN : n293 4 # ASSIGN : n294 7 # ASSIGN : n295 1 # ASSIGN : n296 2 # ASSIGN : n297 5 # ASSIGN : n298 6 # ASSIGN : n299 1 # ASSIGN : n300 8 # ASSIGN : n301 2 # ASSIGN : n302 4 # ASSIGN : n303 1 # ASSIGN : n304 8 # ASSIGN : n305 4 # ASSIGN : n306 2 # ASSIGN : n307 1 # ASSIGN : n308 4 # ASSIGN : n309 6 # ASSIGN : n310 2 # ASSIGN : n311 1 # ASSIGN : n312 4 # ASSIGN : n313 5 # ASSIGN : n314 2 # ASSIGN : n315 1 # ASSIGN : n316 3 # ASSIGN : n317 8 # ASSIGN : n318 2 # ASSIGN : n319 1 # ASSIGN : n320 3 # ASSIGN : n321 8 # ASSIGN : n322 2 # ASSIGN : n323 1 # ASSIGN : n324 6 # ASSIGN : n325 2 # ASSIGN : n326 3 # ASSIGN : n327 1 # ASSIGN : n328 6 # ASSIGN : n329 3 # ASSIGN : n330 8 # ASSIGN : n331 1 # ASSIGN : n332 4 # ASSIGN : n333 7 # ASSIGN : n334 2 # ASSIGN : n335 3 # ASSIGN : n336 2 # ASSIGN : n337 7 # ASSIGN : n338 8 # ASSIGN : n339 3 # ASSIGN : n340 1 # ASSIGN : n341 5 # ASSIGN : n342 4 # ASSIGN : n343 6 # ASSIGN : n344 1 # ASSIGN : n345 2 # ASSIGN : n346 1 # ASSIGN : n347 3 # ASSIGN : n348 8 # ASSIGN : n349 4 # ASSIGN : n350 5 # ASSIGN : n351 5 # ASSIGN : n352 6 # ASSIGN : n353 3 # ASSIGN : n354 4 # ASSIGN : n355 1 # ASSIGN : n356 1 # ASSIGN : n357 8 # ASSIGN : n358 6 # ASSIGN : n359 5 # ASSIGN : n360 7 # ASSIGN : n361 7 # ASSIGN : n362 3 # ASSIGN : n363 8 # ASSIGN : n364 5 # ASSIGN : n365 1 # ASSIGN : n366 1 # ASSIGN : n367 2 # ASSIGN : n368 5 # ASSIGN : n369 6 # ASSIGN : n370 7 # ASSIGN : n371 4 # ASSIGN : n372 8 # ASSIGN : n373 3 # ASSIGN : n374 1 # ASSIGN : n375 2 # ASSIGN : n376 5 # ASSIGN : n377 3 # ASSIGN : n378 8 # ASSIGN : n379 4 # ASSIGN : n380 1 # ASSIGN : n381 4 # ASSIGN : n382 2 # ASSIGN : n383 5 # ASSIGN : n384 3 # ASSIGN : n385 1 # ASSIGN : n386 2 # ASSIGN : n387 6 # ASSIGN : n388 4 # ASSIGN : n389 3 # ASSIGN : n390 1 # ASSIGN : n391 5 # ASSIGN : n392 7 # ASSIGN : n393 3 # ASSIGN : n394 1 # ASSIGN : n395 2 # ASSIGN : n396 2 # ASSIGN : n397 3 # ASSIGN : n398 7 # ASSIGN : n399 4 # ASSIGN : n400 1 # ASSIGN : n401 3 # ASSIGN : n402 4 # ASSIGN : n403 5 # ASSIGN : n404 1 # ASSIGN : n405 2 # ASSIGN : n406 1 # ASSIGN : n407 3 # ASSIGN : n408 8 # ASSIGN : n409 2 # ASSIGN : n410 1 # ASSIGN : n411 4 # ASSIGN : n412 2 # ASSIGN : n413 1 # ASSIGN : n414 4 # ASSIGN : n415 1 # ASSIGN : n416 2 # ASSIGN : n417 8 # ASSIGN : n418 1 # ASSIGN : n419 2 # ASSIGN : n420 3 # ASSIGN : n421 4 # ASSIGN : n422 2 # ASSIGN : n423 3 # ASSIGN : n424 4 # ASSIGN : n425 2 # ASSIGN : n426 3 # ASSIGN : n427 1 # ASSIGN : n428 6 # ASSIGN : n429 7 # ASSIGN : n430 1 # ASSIGN : n431 8 # ASSIGN : n432 2 # ASSIGN : n433 4 # ASSIGN : n434 3 # ASSIGN : n435 2 # ASSIGN : n436 4 # ASSIGN : n437 3 # ASSIGN : n438 1 # ASSIGN : n439 2 # ASSIGN : n440 4 # ASSIGN : n441 1 # ASSIGN : n442 2 # ASSIGN : n443 4 # ASSIGN : n444 1 # ASSIGN : n445 4 # ASSIGN : n446 3 # ASSIGN : n447 1 # ASSIGN : n448 4 # ASSIGN : n449 3 # ASSIGN : n450 1 # ASSIGN : n451 2 # ASSIGN : n452 4 # ASSIGN : n453 1 # ASSIGN : n454 2 # ASSIGN : n455 4 # ASSIGN : n456 1 # ASSIGN : n457 8 # ASSIGN : n458 2 # ASSIGN : n459 1 # ASSIGN : n460 8 # ASSIGN : n461 2 # ASSIGN : n462 3 # ASSIGN : n463 2 # ASSIGN : n464 1 # ASSIGN : n465 4 # ASSIGN : n466 5 # ASSIGN : n467 1 # ASSIGN : n468 4 # ASSIGN : n469 3 # ASSIGN : n470 1 # ASSIGN : n471 2 # ASSIGN : n472 1 # ASSIGN : n473 7 # ASSIGN : n474 8 # ASSIGN : n475 1 # ASSIGN : n476 2 # ASSIGN : n477 8 # ASSIGN : n478 2 # ASSIGN : n479 1 # ASSIGN : n480 3 # ASSIGN : n481 4 # ASSIGN : n482 1 # ASSIGN : n483 8 # ASSIGN : n484 3 # ASSIGN : n485 1 # ASSIGN : n486 2 # ASSIGN : n487 3 # ASSIGN : n488 1 # ASSIGN : n489 4 # ASSIGN : n490 1 # ASSIGN : n491 7 # ASSIGN : n492 2 # ASSIGN : n493 1 # ASSIGN : n494 3 # ASSIGN : n495 8 # ASSIGN : n496 2 # ASSIGN : n497 1 # ASSIGN : n498 4 # ASSIGN : n499 2 # ASSIGN : n500 1 # ASSIGN : n501 4 # ASSIGN : n502 1 # ASSIGN : n503 2 # ASSIGN : n504 8 # ASSIGN : n505 1 # ASSIGN : n506 2 # ASSIGN : n507 3 # ASSIGN : n508 4 # ASSIGN : n509 1 # ASSIGN : n510 3 # ASSIGN : n511 4 # ASSIGN : n512 1 # ASSIGN : n513 3 # ASSIGN : n514 1 # ASSIGN : n515 6 # ASSIGN : n516 7 # ASSIGN : n517 1 # ASSIGN : n518 8 # ASSIGN : n519 2 # ASSIGN : n520 4 # ASSIGN : n521 3 # ASSIGN : n522 2 # ASSIGN : n523 4 # ASSIGN : n524 3 # ASSIGN : n525 1 # ASSIGN : n526 2 # ASSIGN : n527 4 # ASSIGN : n528 1 # ASSIGN : n529 2 # ASSIGN : n530 4 # ASSIGN : n531 1 # ASSIGN : n532 4 # ASSIGN : n533 3 # ASSIGN : n534 1 # ASSIGN : n535 4 # ASSIGN : n536 3 # ASSIGN : n537 1 # ASSIGN : n538 2 # ASSIGN : n539 4 # ASSIGN : n540 1 # ASSIGN : n541 2 # ASSIGN : n542 4 # ASSIGN : n543 1 # ASSIGN : n544 8 # ASSIGN : n545 2 # ASSIGN : n546 1 # ASSIGN : n547 8 # ASSIGN : n548 2 # ASSIGN : n549 3 # ASSIGN : n550 2 # ASSIGN : n551 1 # ASSIGN : n552 4 # ASSIGN : n553 5 # ASSIGN : n554 1 # ASSIGN : n555 4 # ASSIGN : n556 3 # ASSIGN : n557 1 # ASSIGN : n558 2 # ASSIGN : n559 3 # ASSIGN : n560 1 # ASSIGN : n561 2 # ASSIGN : n562 1 # ASSIGN : n563 3 # ASSIGN : n564 2 # ASSIGN : n565 1 # ASSIGN : n566 2 # ASSIGN : n567 3 # ASSIGN : n568 4 # ASSIGN : n569 5 # ASSIGN : n570 6 # ASSIGN : n571 7 # ASSIGN : n572 1 # ASSIGN : n573 8 # ASSIGN : n574 1 # ASSIGN : n575 5 # ASSIGN : n576 4 # ASSIGN : n577 3 # ASSIGN : n578 1 # ASSIGN : n579 2 # ASSIGN : n580 4 # ASSIGN : n581 5 # ASSIGN : n582 1 # ASSIGN : n583 6 # ASSIGN : n584 3 # ASSIGN : n585 4 # ASSIGN : n586 7 # ASSIGN : n587 1 # ASSIGN : n588 8 # ASSIGN : n589 1 # ASSIGN : n590 6 # ASSIGN : n591 3 # ASSIGN : n592 2 # ASSIGN : n593 5 # ASSIGN : n594 1 # ASSIGN : n595 4 # ASSIGN : n596 3 # ASSIGN : n597 4 # ASSIGN : n598 1 # ASSIGN : n599 2 # ASSIGN : n600 5 # ASSIGN : n601 3 # ASSIGN : n602 7 # ASSIGN : n603 1 # ASSIGN : n604 8 # ASSIGN : n605 1 # ASSIGN : n606 4 # ASSIGN : n607 5 # ASSIGN : n608 8 # ASSIGN : n609 2 # ASSIGN : n610 1 # ASSIGN : n611 4 # ASSIGN : n612 3 # ASSIGN : n613 4 # ASSIGN : n614 5 # ASSIGN : n615 1 # ASSIGN : n616 6 # ASSIGN : n617 7 # ASSIGN : n618 4 # ASSIGN : n619 2 # ASSIGN : n620 1 # ASSIGN : n621 5 # ASSIGN : n622 4 # ASSIGN : n623 1 # ASSIGN : n624 7 # ASSIGN : n625 8 # ASSIGN : n626 2 # ASSIGN : n627 4 # ASSIGN : n628 3 # ASSIGN : n629 4 # ASSIGN : n630 5 # ASSIGN : n631 1 # ASSIGN : n632 8 # ASSIGN : n633 6 # ASSIGN : n634 2 # ASSIGN : n635 1 # ASSIGN : n636 2 # ASSIGN : n637 8 # ASSIGN : n638 1 # ASSIGN : n639 2 # ASSIGN : n640 8 # ASSIGN : n641 3 # ASSIGN : n642 4 # ASSIGN : n643 2 # ASSIGN : n644 1 # ASSIGN : n645 4 # ASSIGN : n646 2 # ASSIGN : n647 1 # ASSIGN : n648 2 # ASSIGN : n649 3 # ASSIGN : n650 4 # ASSIGN : n651 5 # ASSIGN : n652 6 # ASSIGN : n653 7 # ASSIGN : n654 8 # ASSIGN : n655 8 # ASSIGN : n656 8 # ASSIGN : n657 8 # ASSIGN : n658 8 # ASSIGN : n659 8 # ASSIGN : n660 8 # ASSIGN : n661 8 # ASSIGN : n662 1 # ASSIGN : n663 2 # ASSIGN : n664 3 # ASSIGN : n665 5 # ASSIGN : n666 6 # ASSIGN : n667 4 # ASSIGN : n668 2 # ASSIGN : n669 1 # ASSIGN : n670 5 # ASSIGN : n671 3 # ASSIGN : n672 6 # ASSIGN : n673 2 # ASSIGN : n674 1 # ASSIGN : n675 3 # ASSIGN : n676 4 # ASSIGN : n677 2 # ASSIGN : n678 5 # ASSIGN : n679 1 # ASSIGN : n680 1 # ASSIGN : n681 2 # ASSIGN : n682 5 # ASSIGN : n683 3 # ASSIGN : n684 8 # ASSIGN : n685 4 # ASSIGN : n686 3 # ASSIGN : n687 2 # ASSIGN : n688 1 # ASSIGN : n689 4 # ASSIGN : n690 5 # ASSIGN : n691 6 # ASSIGN : n692 2 # ASSIGN : n693 1 # ASSIGN : n694 2 # ASSIGN : n695 7 # ASSIGN : n696 3 # ASSIGN : n697 4 # ASSIGN : n698 5 # ASSIGN : n699 6 # ASSIGN : n700 7 # ASSIGN : n701 8 SHOW_RESULT 8 END : 8 (0 seconds) [Tue Jul 11 15:15:50 2006] SHOW_RESULT 8 CPU : 0.0399999999999991 = 0.0399999999999991 + 0 + 0 + 0 # BOUND : color 7 8 MODIFY_CNF 7 BEGIN : [Tue Jul 11 15:15:50 2006] MODIFY_CNF 7 END : 3256299 bytes (0 seconds) [Tue Jul 11 15:15:50 2006] MODIFY_CNF 7 CPU : 0.00999999999999801 = 0.00999999999999801 + 0 + 0 + 0 VERIFY_CNF 7 BEGIN : [Tue Jul 11 15:15:50 2006] CMD : minisat /tmp/csp2sat13929.cnf /tmp/csp2sat13929.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 113504 344477 | 37834 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 6 (30 /sec) decisions : 706 (3530 /sec) propagations : 23203 (116015 /sec) conflict literals : 30 (0.00 % deleted) Memory used : 8.46 MB CPU time : 0.2 s SATISFIABLE VERIFY_CNF 7 END : (1 seconds) [Tue Jul 11 15:15:51 2006] VERIFY_CNF 7 CPU : 0.27 = 0 + 0 + 0.21 + 0.06 # RESULT : color 7 SATISFIABLE SHOW_RESULT 7 BEGIN : [Tue Jul 11 15:15:51 2006] # ASSIGN : color 7 # ASSIGN : n1 2 # ASSIGN : n2 1 # ASSIGN : n3 3 # ASSIGN : n4 2 # ASSIGN : n5 6 # ASSIGN : n6 5 # ASSIGN : n7 4 # ASSIGN : n8 2 # ASSIGN : n9 4 # ASSIGN : n10 7 # ASSIGN : n11 2 # ASSIGN : n12 4 # ASSIGN : n13 3 # ASSIGN : n14 1 # ASSIGN : n15 4 # ASSIGN : n16 2 # ASSIGN : n17 5 # ASSIGN : n18 4 # ASSIGN : n19 2 # ASSIGN : n20 6 # ASSIGN : n21 1 # ASSIGN : n22 2 # ASSIGN : n23 7 # ASSIGN : n24 5 # ASSIGN : n25 6 # ASSIGN : n26 3 # ASSIGN : n27 1 # ASSIGN : n28 4 # ASSIGN : n29 6 # ASSIGN : n30 2 # ASSIGN : n31 7 # ASSIGN : n32 1 # ASSIGN : n33 4 # ASSIGN : n34 5 # ASSIGN : n35 3 # ASSIGN : n36 7 # ASSIGN : n37 6 # ASSIGN : n38 5 # ASSIGN : n39 2 # ASSIGN : n40 6 # ASSIGN : n41 5 # ASSIGN : n42 1 # ASSIGN : n43 4 # ASSIGN : n44 1 # ASSIGN : n45 3 # ASSIGN : n46 6 # ASSIGN : n47 1 # ASSIGN : n48 3 # ASSIGN : n49 7 # ASSIGN : n50 5 # ASSIGN : n51 6 # ASSIGN : n52 3 # ASSIGN : n53 5 # ASSIGN : n54 4 # ASSIGN : n55 2 # ASSIGN : n56 3 # ASSIGN : n57 4 # ASSIGN : n58 1 # ASSIGN : n59 6 # ASSIGN : n60 4 # ASSIGN : n61 7 # ASSIGN : n62 5 # ASSIGN : n63 3 # ASSIGN : n64 3 # ASSIGN : n65 6 # ASSIGN : n66 2 # ASSIGN : n67 3 # ASSIGN : n68 6 # ASSIGN : n69 4 # ASSIGN : n70 2 # ASSIGN : n71 2 # ASSIGN : n72 3 # ASSIGN : n73 5 # ASSIGN : n74 2 # ASSIGN : n75 3 # ASSIGN : n76 5 # ASSIGN : n77 1 # ASSIGN : n78 2 # ASSIGN : n79 4 # ASSIGN : n80 5 # ASSIGN : n81 6 # ASSIGN : n82 3 # ASSIGN : n83 5 # ASSIGN : n84 7 # ASSIGN : n85 1 # ASSIGN : n86 6 # ASSIGN : n87 4 # ASSIGN : n88 3 # ASSIGN : n89 6 # ASSIGN : n90 7 # ASSIGN : n91 2 # ASSIGN : n92 2 # ASSIGN : n93 5 # ASSIGN : n94 1 # ASSIGN : n95 6 # ASSIGN : n96 5 # ASSIGN : n97 1 # ASSIGN : n98 4 # ASSIGN : n99 5 # ASSIGN : n100 6 # ASSIGN : n101 1 # ASSIGN : n102 5 # ASSIGN : n103 6 # ASSIGN : n104 3 # ASSIGN : n105 2 # ASSIGN : n106 5 # ASSIGN : n107 7 # ASSIGN : n108 3 # ASSIGN : n109 5 # ASSIGN : n110 7 # ASSIGN : n111 4 # ASSIGN : n112 1 # ASSIGN : n113 6 # ASSIGN : n114 5 # ASSIGN : n115 4 # ASSIGN : n116 6 # ASSIGN : n117 5 # ASSIGN : n118 3 # ASSIGN : n119 1 # ASSIGN : n120 5 # ASSIGN : n121 2 # ASSIGN : n122 3 # ASSIGN : n123 4 # ASSIGN : n124 2 # ASSIGN : n125 6 # ASSIGN : n126 3 # ASSIGN : n127 2 # ASSIGN : n128 4 # ASSIGN : n129 1 # ASSIGN : n130 6 # ASSIGN : n131 4 # ASSIGN : n132 7 # ASSIGN : n133 1 # ASSIGN : n134 1 # ASSIGN : n135 4 # ASSIGN : n136 2 # ASSIGN : n137 1 # ASSIGN : n138 3 # ASSIGN : n139 2 # ASSIGN : n140 7 # ASSIGN : n141 3 # ASSIGN : n142 1 # ASSIGN : n143 4 # ASSIGN : n144 5 # ASSIGN : n145 1 # ASSIGN : n146 6 # ASSIGN : n147 7 # ASSIGN : n148 2 # ASSIGN : n149 1 # ASSIGN : n150 3 # ASSIGN : n151 2 # ASSIGN : n152 1 # ASSIGN : n153 6 # ASSIGN : n154 3 # ASSIGN : n155 3 # ASSIGN : n156 1 # ASSIGN : n157 6 # ASSIGN : n158 3 # ASSIGN : n159 1 # ASSIGN : n160 4 # ASSIGN : n161 2 # ASSIGN : n162 5 # ASSIGN : n163 7 # ASSIGN : n164 6 # ASSIGN : n165 4 # ASSIGN : n166 7 # ASSIGN : n167 6 # ASSIGN : n168 3 # ASSIGN : n169 4 # ASSIGN : n170 1 # ASSIGN : n171 5 # ASSIGN : n172 6 # ASSIGN : n173 1 # ASSIGN : n174 5 # ASSIGN : n175 7 # ASSIGN : n176 3 # ASSIGN : n177 1 # ASSIGN : n178 4 # ASSIGN : n179 3 # ASSIGN : n180 5 # ASSIGN : n181 2 # ASSIGN : n182 4 # ASSIGN : n183 5 # ASSIGN : n184 3 # ASSIGN : n185 7 # ASSIGN : n186 5 # ASSIGN : n187 1 # ASSIGN : n188 6 # ASSIGN : n189 7 # ASSIGN : n190 3 # ASSIGN : n191 7 # ASSIGN : n192 4 # ASSIGN : n193 5 # ASSIGN : n194 7 # ASSIGN : n195 6 # ASSIGN : n196 2 # ASSIGN : n197 7 # ASSIGN : n198 5 # ASSIGN : n199 1 # ASSIGN : n200 7 # ASSIGN : n201 5 # ASSIGN : n202 1 # ASSIGN : n203 4 # ASSIGN : n204 5 # ASSIGN : n205 6 # ASSIGN : n206 3 # ASSIGN : n207 7 # ASSIGN : n208 1 # ASSIGN : n209 3 # ASSIGN : n210 2 # ASSIGN : n211 1 # ASSIGN : n212 6 # ASSIGN : n213 3 # ASSIGN : n214 4 # ASSIGN : n215 1 # ASSIGN : n216 7 # ASSIGN : n217 3 # ASSIGN : n218 4 # ASSIGN : n219 2 # ASSIGN : n220 3 # ASSIGN : n221 5 # ASSIGN : n222 1 # ASSIGN : n223 2 # ASSIGN : n224 3 # ASSIGN : n225 4 # ASSIGN : n226 1 # ASSIGN : n227 2 # ASSIGN : n228 6 # ASSIGN : n229 3 # ASSIGN : n230 1 # ASSIGN : n231 2 # ASSIGN : n232 6 # ASSIGN : n233 3 # ASSIGN : n234 4 # ASSIGN : n235 4 # ASSIGN : n236 2 # ASSIGN : n237 3 # ASSIGN : n238 1 # ASSIGN : n239 4 # ASSIGN : n240 2 # ASSIGN : n241 1 # ASSIGN : n242 5 # ASSIGN : n243 3 # ASSIGN : n244 5 # ASSIGN : n245 1 # ASSIGN : n246 2 # ASSIGN : n247 3 # ASSIGN : n248 5 # ASSIGN : n249 2 # ASSIGN : n250 1 # ASSIGN : n251 6 # ASSIGN : n252 1 # ASSIGN : n253 2 # ASSIGN : n254 3 # ASSIGN : n255 5 # ASSIGN : n256 1 # ASSIGN : n257 2 # ASSIGN : n258 7 # ASSIGN : n259 2 # ASSIGN : n260 6 # ASSIGN : n261 3 # ASSIGN : n262 4 # ASSIGN : n263 1 # ASSIGN : n264 5 # ASSIGN : n265 3 # ASSIGN : n266 7 # ASSIGN : n267 1 # ASSIGN : n268 5 # ASSIGN : n269 4 # ASSIGN : n270 2 # ASSIGN : n271 1 # ASSIGN : n272 5 # ASSIGN : n273 6 # ASSIGN : n274 4 # ASSIGN : n275 1 # ASSIGN : n276 5 # ASSIGN : n277 2 # ASSIGN : n278 3 # ASSIGN : n279 1 # ASSIGN : n280 7 # ASSIGN : n281 6 # ASSIGN : n282 2 # ASSIGN : n283 1 # ASSIGN : n284 7 # ASSIGN : n285 2 # ASSIGN : n286 6 # ASSIGN : n287 1 # ASSIGN : n288 7 # ASSIGN : n289 6 # ASSIGN : n290 3 # ASSIGN : n291 1 # ASSIGN : n292 6 # ASSIGN : n293 5 # ASSIGN : n294 2 # ASSIGN : n295 1 # ASSIGN : n296 6 # ASSIGN : n297 5 # ASSIGN : n298 7 # ASSIGN : n299 6 # ASSIGN : n300 3 # ASSIGN : n301 5 # ASSIGN : n302 1 # ASSIGN : n303 6 # ASSIGN : n304 3 # ASSIGN : n305 7 # ASSIGN : n306 1 # ASSIGN : n307 1 # ASSIGN : n308 3 # ASSIGN : n309 5 # ASSIGN : n310 2 # ASSIGN : n311 1 # ASSIGN : n312 3 # ASSIGN : n313 4 # ASSIGN : n314 2 # ASSIGN : n315 3 # ASSIGN : n316 4 # ASSIGN : n317 1 # ASSIGN : n318 2 # ASSIGN : n319 3 # ASSIGN : n320 4 # ASSIGN : n321 1 # ASSIGN : n322 2 # ASSIGN : n323 6 # ASSIGN : n324 5 # ASSIGN : n325 1 # ASSIGN : n326 2 # ASSIGN : n327 6 # ASSIGN : n328 5 # ASSIGN : n329 1 # ASSIGN : n330 2 # ASSIGN : n331 4 # ASSIGN : n332 5 # ASSIGN : n333 3 # ASSIGN : n334 1 # ASSIGN : n335 2 # ASSIGN : n336 1 # ASSIGN : n337 7 # ASSIGN : n338 6 # ASSIGN : n339 4 # ASSIGN : n340 2 # ASSIGN : n341 4 # ASSIGN : n342 5 # ASSIGN : n343 7 # ASSIGN : n344 3 # ASSIGN : n345 1 # ASSIGN : n346 1 # ASSIGN : n347 2 # ASSIGN : n348 5 # ASSIGN : n349 3 # ASSIGN : n350 4 # ASSIGN : n351 6 # ASSIGN : n352 5 # ASSIGN : n353 1 # ASSIGN : n354 2 # ASSIGN : n355 3 # ASSIGN : n356 7 # ASSIGN : n357 4 # ASSIGN : n358 5 # ASSIGN : n359 3 # ASSIGN : n360 2 # ASSIGN : n361 7 # ASSIGN : n362 6 # ASSIGN : n363 3 # ASSIGN : n364 2 # ASSIGN : n365 4 # ASSIGN : n366 2 # ASSIGN : n367 3 # ASSIGN : n368 7 # ASSIGN : n369 4 # ASSIGN : n370 1 # ASSIGN : n371 3 # ASSIGN : n372 5 # ASSIGN : n373 4 # ASSIGN : n374 1 # ASSIGN : n375 2 # ASSIGN : n376 2 # ASSIGN : n377 4 # ASSIGN : n378 3 # ASSIGN : n379 5 # ASSIGN : n380 1 # ASSIGN : n381 4 # ASSIGN : n382 6 # ASSIGN : n383 2 # ASSIGN : n384 7 # ASSIGN : n385 1 # ASSIGN : n386 5 # ASSIGN : n387 2 # ASSIGN : n388 6 # ASSIGN : n389 4 # ASSIGN : n390 1 # ASSIGN : n391 2 # ASSIGN : n392 3 # ASSIGN : n393 4 # ASSIGN : n394 5 # ASSIGN : n395 1 # ASSIGN : n396 1 # ASSIGN : n397 6 # ASSIGN : n398 3 # ASSIGN : n399 7 # ASSIGN : n400 2 # ASSIGN : n401 2 # ASSIGN : n402 7 # ASSIGN : n403 3 # ASSIGN : n404 4 # ASSIGN : n405 1 # ASSIGN : n406 1 # ASSIGN : n407 2 # ASSIGN : n408 3 # ASSIGN : n409 4 # ASSIGN : n410 1 # ASSIGN : n411 3 # ASSIGN : n412 4 # ASSIGN : n413 1 # ASSIGN : n414 2 # ASSIGN : n415 1 # ASSIGN : n416 3 # ASSIGN : n417 5 # ASSIGN : n418 1 # ASSIGN : n419 2 # ASSIGN : n420 4 # ASSIGN : n421 5 # ASSIGN : n422 2 # ASSIGN : n423 3 # ASSIGN : n424 5 # ASSIGN : n425 4 # ASSIGN : n426 1 # ASSIGN : n427 2 # ASSIGN : n428 7 # ASSIGN : n429 1 # ASSIGN : n430 2 # ASSIGN : n431 7 # ASSIGN : n432 1 # ASSIGN : n433 3 # ASSIGN : n434 2 # ASSIGN : n435 1 # ASSIGN : n436 3 # ASSIGN : n437 2 # ASSIGN : n438 1 # ASSIGN : n439 2 # ASSIGN : n440 7 # ASSIGN : n441 1 # ASSIGN : n442 2 # ASSIGN : n443 7 # ASSIGN : n444 1 # ASSIGN : n445 4 # ASSIGN : n446 2 # ASSIGN : n447 1 # ASSIGN : n448 4 # ASSIGN : n449 2 # ASSIGN : n450 1 # ASSIGN : n451 3 # ASSIGN : n452 2 # ASSIGN : n453 1 # ASSIGN : n454 3 # ASSIGN : n455 2 # ASSIGN : n456 4 # ASSIGN : n457 2 # ASSIGN : n458 1 # ASSIGN : n459 7 # ASSIGN : n460 2 # ASSIGN : n461 1 # ASSIGN : n462 7 # ASSIGN : n463 1 # ASSIGN : n464 2 # ASSIGN : n465 3 # ASSIGN : n466 4 # ASSIGN : n467 2 # ASSIGN : n468 3 # ASSIGN : n469 2 # ASSIGN : n470 4 # ASSIGN : n471 1 # ASSIGN : n472 7 # ASSIGN : n473 2 # ASSIGN : n474 1 # ASSIGN : n475 6 # ASSIGN : n476 2 # ASSIGN : n477 3 # ASSIGN : n478 1 # ASSIGN : n479 2 # ASSIGN : n480 7 # ASSIGN : n481 1 # ASSIGN : n482 2 # ASSIGN : n483 7 # ASSIGN : n484 2 # ASSIGN : n485 1 # ASSIGN : n486 3 # ASSIGN : n487 2 # ASSIGN : n488 1 # ASSIGN : n489 3 # ASSIGN : n490 1 # ASSIGN : n491 2 # ASSIGN : n492 7 # ASSIGN : n493 1 # ASSIGN : n494 2 # ASSIGN : n495 3 # ASSIGN : n496 4 # ASSIGN : n497 1 # ASSIGN : n498 3 # ASSIGN : n499 6 # ASSIGN : n500 1 # ASSIGN : n501 2 # ASSIGN : n502 1 # ASSIGN : n503 3 # ASSIGN : n504 4 # ASSIGN : n505 1 # ASSIGN : n506 2 # ASSIGN : n507 4 # ASSIGN : n508 5 # ASSIGN : n509 2 # ASSIGN : n510 3 # ASSIGN : n511 5 # ASSIGN : n512 4 # ASSIGN : n513 1 # ASSIGN : n514 2 # ASSIGN : n515 7 # ASSIGN : n516 1 # ASSIGN : n517 2 # ASSIGN : n518 7 # ASSIGN : n519 1 # ASSIGN : n520 3 # ASSIGN : n521 2 # ASSIGN : n522 1 # ASSIGN : n523 3 # ASSIGN : n524 2 # ASSIGN : n525 1 # ASSIGN : n526 2 # ASSIGN : n527 6 # ASSIGN : n528 1 # ASSIGN : n529 2 # ASSIGN : n530 6 # ASSIGN : n531 1 # ASSIGN : n532 4 # ASSIGN : n533 3 # ASSIGN : n534 1 # ASSIGN : n535 4 # ASSIGN : n536 3 # ASSIGN : n537 1 # ASSIGN : n538 3 # ASSIGN : n539 2 # ASSIGN : n540 1 # ASSIGN : n541 3 # ASSIGN : n542 2 # ASSIGN : n543 4 # ASSIGN : n544 2 # ASSIGN : n545 1 # ASSIGN : n546 7 # ASSIGN : n547 2 # ASSIGN : n548 1 # ASSIGN : n549 7 # ASSIGN : n550 1 # ASSIGN : n551 2 # ASSIGN : n552 3 # ASSIGN : n553 4 # ASSIGN : n554 2 # ASSIGN : n555 3 # ASSIGN : n556 2 # ASSIGN : n557 4 # ASSIGN : n558 1 # ASSIGN : n559 2 # ASSIGN : n560 4 # ASSIGN : n561 1 # ASSIGN : n562 4 # ASSIGN : n563 2 # ASSIGN : n564 1 # ASSIGN : n565 7 # ASSIGN : n566 1 # ASSIGN : n567 2 # ASSIGN : n568 3 # ASSIGN : n569 4 # ASSIGN : n570 5 # ASSIGN : n571 6 # ASSIGN : n572 1 # ASSIGN : n573 7 # ASSIGN : n574 1 # ASSIGN : n575 4 # ASSIGN : n576 3 # ASSIGN : n577 2 # ASSIGN : n578 1 # ASSIGN : n579 4 # ASSIGN : n580 3 # ASSIGN : n581 4 # ASSIGN : n582 7 # ASSIGN : n583 5 # ASSIGN : n584 2 # ASSIGN : n585 3 # ASSIGN : n586 4 # ASSIGN : n587 1 # ASSIGN : n588 5 # ASSIGN : n589 6 # ASSIGN : n590 5 # ASSIGN : n591 2 # ASSIGN : n592 3 # ASSIGN : n593 4 # ASSIGN : n594 6 # ASSIGN : n595 5 # ASSIGN : n596 2 # ASSIGN : n597 5 # ASSIGN : n598 2 # ASSIGN : n599 3 # ASSIGN : n600 4 # ASSIGN : n601 6 # ASSIGN : n602 7 # ASSIGN : n603 2 # ASSIGN : n604 1 # ASSIGN : n605 2 # ASSIGN : n606 3 # ASSIGN : n607 4 # ASSIGN : n608 6 # ASSIGN : n609 5 # ASSIGN : n610 2 # ASSIGN : n611 3 # ASSIGN : n612 1 # ASSIGN : n613 3 # ASSIGN : n614 2 # ASSIGN : n615 4 # ASSIGN : n616 5 # ASSIGN : n617 6 # ASSIGN : n618 7 # ASSIGN : n619 2 # ASSIGN : n620 1 # ASSIGN : n621 2 # ASSIGN : n622 4 # ASSIGN : n623 3 # ASSIGN : n624 6 # ASSIGN : n625 7 # ASSIGN : n626 2 # ASSIGN : n627 4 # ASSIGN : n628 3 # ASSIGN : n629 4 # ASSIGN : n630 3 # ASSIGN : n631 2 # ASSIGN : n632 1 # ASSIGN : n633 4 # ASSIGN : n634 5 # ASSIGN : n635 6 # ASSIGN : n636 7 # ASSIGN : n637 2 # ASSIGN : n638 1 # ASSIGN : n639 7 # ASSIGN : n640 2 # ASSIGN : n641 1 # ASSIGN : n642 2 # ASSIGN : n643 1 # ASSIGN : n644 3 # ASSIGN : n645 2 # ASSIGN : n646 1 # ASSIGN : n647 3 # ASSIGN : n648 1 # ASSIGN : n649 2 # ASSIGN : n650 3 # ASSIGN : n651 4 # ASSIGN : n652 5 # ASSIGN : n653 6 # ASSIGN : n654 7 # ASSIGN : n655 7 # ASSIGN : n656 7 # ASSIGN : n657 7 # ASSIGN : n658 7 # ASSIGN : n659 7 # ASSIGN : n660 6 # ASSIGN : n661 7 # ASSIGN : n662 6 # ASSIGN : n663 7 # ASSIGN : n664 1 # ASSIGN : n665 3 # ASSIGN : n666 1 # ASSIGN : n667 4 # ASSIGN : n668 2 # ASSIGN : n669 5 # ASSIGN : n670 6 # ASSIGN : n671 4 # ASSIGN : n672 2 # ASSIGN : n673 1 # ASSIGN : n674 5 # ASSIGN : n675 6 # ASSIGN : n676 2 # ASSIGN : n677 3 # ASSIGN : n678 1 # ASSIGN : n679 5 # ASSIGN : n680 5 # ASSIGN : n681 7 # ASSIGN : n682 2 # ASSIGN : n683 1 # ASSIGN : n684 4 # ASSIGN : n685 2 # ASSIGN : n686 3 # ASSIGN : n687 1 # ASSIGN : n688 7 # ASSIGN : n689 2 # ASSIGN : n690 3 # ASSIGN : n691 4 # ASSIGN : n692 1 # ASSIGN : n693 5 # ASSIGN : n694 1 # ASSIGN : n695 5 # ASSIGN : n696 2 # ASSIGN : n697 3 # ASSIGN : n698 4 # ASSIGN : n699 5 # ASSIGN : n700 6 # ASSIGN : n701 7 SHOW_RESULT 7 END : 7 (0 seconds) [Tue Jul 11 15:15:51 2006] SHOW_RESULT 7 CPU : 0.0500000000000007 = 0.0500000000000007 + 0 + 0 + 0 # BOUND : color 7 7 MAIN END : (21 seconds) [Tue Jul 11 15:15:51 2006] MAIN CPU : 20.83 = 19.48 + 0.17 + 1.05 + 0.13