# TIMEOUT 7200 MAIN BEGIN : [Thu Jul 6 09:58:09 2006] READ BEGIN : csp/4-FullIns_4.csp [Thu Jul 6 09:58:09 2006] READ END : csp/4-FullIns_4.csp (11 seconds) [Thu Jul 6 09:58:20 2006] READ CPU : 10.58 = 10.47 + 0.11 + 0 + 0 # BOUND : color 2 20 GENERATE_CNF 20 BEGIN : [Thu Jul 6 09:58:20 2006] GENERATE_CNF 20 END : 28500 variables 300961 clauses 5964870 bytes (14 seconds) [Thu Jul 6 09:58:34 2006] GENERATE_CNF 20 CPU : 13.29 = 13.24 + 0.05 + 0 + 0 MODIFY_CNF 11 BEGIN : [Thu Jul 6 09:58:34 2006] MODIFY_CNF 11 END : 5964875 bytes (0 seconds) [Thu Jul 6 09:58:34 2006] MODIFY_CNF 11 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 11 BEGIN : [Thu Jul 6 09:58:34 2006] CMD : minisat /tmp/csp2sat13823.cnf /tmp/csp2sat13823.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 177116 529016 | 59038 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 0 (0 /sec) decisions : 3410 (9472 /sec) propagations : 28500 (79167 /sec) conflict literals : 0 ( nan % deleted) Memory used : 13.49 MB CPU time : 0.36 s SATISFIABLE VERIFY_CNF 11 END : (0 seconds) [Thu Jul 6 09:58:34 2006] VERIFY_CNF 11 CPU : 0.45 = 0 + 0.00999999999999998 + 0.38 + 0.06 # RESULT : color 11 SATISFIABLE SHOW_RESULT 11 BEGIN : [Thu Jul 6 09:58:34 2006] # ASSIGN : color 11 # ASSIGN : n1 3 # ASSIGN : n2 4 # ASSIGN : n3 2 # ASSIGN : n4 2 # ASSIGN : n5 3 # ASSIGN : n6 3 # ASSIGN : n7 2 # ASSIGN : n8 2 # ASSIGN : n9 3 # ASSIGN : n10 3 # ASSIGN : n11 2 # ASSIGN : n12 2 # ASSIGN : n13 9 # ASSIGN : n14 10 # ASSIGN : n15 11 # ASSIGN : n16 5 # ASSIGN : n17 2 # ASSIGN : n18 3 # ASSIGN : n19 5 # ASSIGN : n20 5 # ASSIGN : n21 5 # ASSIGN : n22 5 # ASSIGN : n23 4 # ASSIGN : n24 4 # ASSIGN : n25 4 # ASSIGN : n26 4 # ASSIGN : n27 8 # 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 4 # ASSIGN : n37 11 # ASSIGN : n38 11 # ASSIGN : n39 11 # ASSIGN : n40 11 # ASSIGN : n41 11 # ASSIGN : n42 11 # ASSIGN : n43 11 # ASSIGN : n44 9 # ASSIGN : n45 11 # ASSIGN : n46 11 # ASSIGN : n47 5 # ASSIGN : n48 5 # ASSIGN : n49 11 # ASSIGN : n50 11 # ASSIGN : n51 5 # ASSIGN : n52 5 # ASSIGN : n53 5 # ASSIGN : n54 5 # ASSIGN : n55 2 # ASSIGN : n56 2 # ASSIGN : n57 2 # ASSIGN : n58 2 # ASSIGN : n59 2 # ASSIGN : n60 2 # ASSIGN : n61 2 # ASSIGN : n62 2 # ASSIGN : n63 10 # ASSIGN : n64 2 # ASSIGN : n65 2 # ASSIGN : n66 2 # ASSIGN : n67 2 # ASSIGN : n68 2 # ASSIGN : n69 2 # ASSIGN : n70 2 # ASSIGN : n71 2 # ASSIGN : n72 2 # ASSIGN : n73 3 # ASSIGN : n74 3 # ASSIGN : n75 3 # ASSIGN : n76 3 # ASSIGN : n77 3 # ASSIGN : n78 3 # ASSIGN : n79 3 # ASSIGN : n80 3 # ASSIGN : n81 3 # ASSIGN : n82 3 # ASSIGN : n83 3 # ASSIGN : n84 3 # ASSIGN : n85 3 # ASSIGN : n86 3 # ASSIGN : n87 3 # ASSIGN : n88 3 # ASSIGN : n89 3 # ASSIGN : n90 3 # ASSIGN : n91 4 # ASSIGN : n92 4 # ASSIGN : n93 4 # ASSIGN : n94 4 # ASSIGN : n95 4 # ASSIGN : n96 4 # ASSIGN : n97 4 # ASSIGN : n98 4 # ASSIGN : n99 4 # ASSIGN : n100 4 # ASSIGN : n101 4 # ASSIGN : n102 4 # ASSIGN : n103 4 # ASSIGN : n104 4 # ASSIGN : n105 4 # ASSIGN : n106 4 # ASSIGN : n107 4 # ASSIGN : n108 4 # ASSIGN : n109 8 # ASSIGN : n110 9 # ASSIGN : n111 2 # ASSIGN : n112 3 # ASSIGN : n113 4 # ASSIGN : n114 5 # ASSIGN : n115 1 # ASSIGN : n116 1 # ASSIGN : n117 1 # ASSIGN : n118 1 # ASSIGN : n119 1 # ASSIGN : n120 1 # ASSIGN : n121 1 # ASSIGN : n122 6 # ASSIGN : n123 1 # ASSIGN : n124 1 # ASSIGN : n125 6 # ASSIGN : n126 1 # ASSIGN : n127 6 # ASSIGN : n128 1 # ASSIGN : n129 1 # ASSIGN : n130 1 # ASSIGN : n131 1 # ASSIGN : n132 1 # ASSIGN : n133 1 # ASSIGN : n134 1 # ASSIGN : n135 1 # ASSIGN : n136 1 # ASSIGN : n137 1 # ASSIGN : n138 1 # ASSIGN : n139 1 # ASSIGN : n140 1 # ASSIGN : n141 1 # ASSIGN : n142 1 # ASSIGN : n143 1 # ASSIGN : n144 1 # ASSIGN : n145 1 # ASSIGN : n146 1 # ASSIGN : n147 1 # ASSIGN : n148 1 # ASSIGN : n149 1 # ASSIGN : n150 1 # ASSIGN : n151 1 # ASSIGN : n152 1 # ASSIGN : n153 11 # ASSIGN : n154 1 # ASSIGN : n155 1 # ASSIGN : n156 1 # ASSIGN : n157 1 # ASSIGN : n158 1 # ASSIGN : n159 1 # ASSIGN : n160 1 # ASSIGN : n161 1 # ASSIGN : n162 1 # ASSIGN : n163 1 # ASSIGN : n164 1 # ASSIGN : n165 1 # ASSIGN : n166 1 # ASSIGN : n167 11 # ASSIGN : n168 1 # ASSIGN : n169 1 # ASSIGN : n170 1 # ASSIGN : n171 1 # ASSIGN : n172 1 # ASSIGN : n173 1 # ASSIGN : n174 1 # ASSIGN : n175 1 # ASSIGN : n176 1 # ASSIGN : n177 1 # ASSIGN : n178 1 # ASSIGN : n179 1 # ASSIGN : n180 1 # ASSIGN : n181 6 # ASSIGN : n182 1 # ASSIGN : n183 1 # ASSIGN : n184 1 # ASSIGN : n185 1 # ASSIGN : n186 1 # ASSIGN : n187 1 # ASSIGN : n188 1 # ASSIGN : n189 1 # ASSIGN : n190 1 # ASSIGN : n191 1 # ASSIGN : n192 1 # ASSIGN : n193 1 # ASSIGN : n194 1 # ASSIGN : n195 1 # ASSIGN : n196 1 # ASSIGN : n197 1 # ASSIGN : n198 1 # ASSIGN : n199 1 # ASSIGN : n200 6 # ASSIGN : n201 6 # ASSIGN : n202 1 # ASSIGN : n203 1 # ASSIGN : n204 1 # ASSIGN : n205 1 # ASSIGN : n206 1 # ASSIGN : n207 1 # ASSIGN : n208 1 # ASSIGN : n209 1 # ASSIGN : n210 10 # ASSIGN : n211 1 # ASSIGN : n212 1 # ASSIGN : n213 1 # ASSIGN : n214 1 # ASSIGN : n215 1 # ASSIGN : n216 1 # ASSIGN : n217 1 # ASSIGN : n218 1 # ASSIGN : n219 1 # ASSIGN : n220 1 # ASSIGN : n221 1 # ASSIGN : n222 1 # ASSIGN : n223 10 # ASSIGN : n224 6 # ASSIGN : n225 1 # ASSIGN : n226 1 # ASSIGN : n227 1 # ASSIGN : n228 1 # 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 2 # ASSIGN : n246 2 # ASSIGN : n247 2 # ASSIGN : n248 2 # ASSIGN : n249 2 # ASSIGN : n250 2 # ASSIGN : n251 2 # ASSIGN : n252 2 # ASSIGN : n253 2 # ASSIGN : n254 2 # 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 2 # ASSIGN : n273 2 # ASSIGN : n274 2 # ASSIGN : n275 2 # ASSIGN : n276 2 # ASSIGN : n277 2 # ASSIGN : n278 2 # ASSIGN : n279 2 # ASSIGN : n280 2 # ASSIGN : n281 2 # ASSIGN : n282 2 # 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 2 # ASSIGN : n306 2 # ASSIGN : n307 2 # ASSIGN : n308 2 # ASSIGN : n309 2 # ASSIGN : n310 2 # ASSIGN : n311 2 # ASSIGN : n312 2 # ASSIGN : n313 2 # ASSIGN : n314 2 # ASSIGN : n315 2 # ASSIGN : n316 2 # ASSIGN : n317 2 # ASSIGN : n318 2 # ASSIGN : n319 2 # ASSIGN : n320 2 # ASSIGN : n321 2 # ASSIGN : n322 2 # ASSIGN : n323 2 # ASSIGN : n324 2 # ASSIGN : n325 2 # ASSIGN : n326 2 # ASSIGN : n327 2 # ASSIGN : n328 2 # ASSIGN : n329 2 # ASSIGN : n330 2 # ASSIGN : n331 2 # ASSIGN : n332 2 # ASSIGN : n333 7 # ASSIGN : n334 2 # ASSIGN : n335 2 # ASSIGN : n336 2 # ASSIGN : n337 2 # ASSIGN : n338 2 # ASSIGN : n339 2 # ASSIGN : n340 2 # ASSIGN : n341 2 # ASSIGN : n342 11 # ASSIGN : n343 3 # ASSIGN : n344 3 # ASSIGN : n345 3 # ASSIGN : n346 3 # ASSIGN : n347 3 # ASSIGN : n348 3 # ASSIGN : n349 3 # ASSIGN : n350 3 # ASSIGN : n351 3 # ASSIGN : n352 3 # ASSIGN : n353 3 # ASSIGN : n354 3 # ASSIGN : n355 3 # ASSIGN : n356 3 # ASSIGN : n357 3 # ASSIGN : n358 8 # ASSIGN : n359 3 # ASSIGN : n360 3 # ASSIGN : n361 3 # ASSIGN : n362 3 # ASSIGN : n363 3 # ASSIGN : n364 3 # ASSIGN : n365 3 # ASSIGN : n366 3 # ASSIGN : n367 3 # ASSIGN : n368 3 # ASSIGN : n369 3 # ASSIGN : n370 3 # ASSIGN : n371 3 # ASSIGN : n372 1 # ASSIGN : n373 1 # ASSIGN : n374 1 # ASSIGN : n375 1 # ASSIGN : n376 1 # ASSIGN : n377 1 # ASSIGN : n378 3 # ASSIGN : n379 3 # ASSIGN : n380 3 # ASSIGN : n381 3 # ASSIGN : n382 3 # ASSIGN : n383 3 # ASSIGN : n384 3 # ASSIGN : n385 1 # ASSIGN : n386 3 # ASSIGN : n387 3 # ASSIGN : n388 3 # ASSIGN : n389 3 # ASSIGN : n390 3 # ASSIGN : n391 1 # ASSIGN : n392 1 # ASSIGN : n393 1 # ASSIGN : n394 3 # ASSIGN : n395 1 # ASSIGN : n396 1 # ASSIGN : n397 3 # ASSIGN : n398 3 # ASSIGN : n399 3 # ASSIGN : n400 3 # ASSIGN : n401 3 # ASSIGN : n402 3 # ASSIGN : n403 8 # ASSIGN : n404 3 # ASSIGN : n405 3 # ASSIGN : n406 3 # ASSIGN : n407 1 # 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 3 # ASSIGN : n418 3 # ASSIGN : n419 3 # ASSIGN : n420 3 # ASSIGN : n421 1 # ASSIGN : n422 1 # ASSIGN : n423 3 # ASSIGN : n424 3 # ASSIGN : n425 3 # ASSIGN : n426 3 # ASSIGN : n427 1 # ASSIGN : n428 1 # ASSIGN : n429 1 # ASSIGN : n430 3 # ASSIGN : n431 1 # ASSIGN : n432 1 # ASSIGN : n433 3 # ASSIGN : n434 3 # ASSIGN : n435 3 # ASSIGN : n436 3 # ASSIGN : n437 3 # ASSIGN : n438 3 # ASSIGN : n439 3 # ASSIGN : n440 3 # ASSIGN : n441 3 # ASSIGN : n442 3 # ASSIGN : n443 3 # ASSIGN : n444 3 # ASSIGN : n445 3 # ASSIGN : n446 3 # ASSIGN : n447 3 # ASSIGN : n448 3 # ASSIGN : n449 3 # ASSIGN : n450 3 # ASSIGN : n451 3 # ASSIGN : n452 3 # ASSIGN : n453 1 # ASSIGN : n454 1 # ASSIGN : n455 3 # ASSIGN : n456 3 # ASSIGN : n457 4 # ASSIGN : n458 4 # ASSIGN : n459 4 # ASSIGN : n460 4 # ASSIGN : n461 4 # ASSIGN : n462 4 # ASSIGN : n463 4 # ASSIGN : n464 4 # ASSIGN : n465 4 # ASSIGN : n466 4 # ASSIGN : n467 4 # ASSIGN : n468 4 # ASSIGN : n469 4 # ASSIGN : n470 4 # ASSIGN : n471 4 # ASSIGN : n472 4 # ASSIGN : n473 4 # ASSIGN : n474 4 # ASSIGN : n475 4 # ASSIGN : n476 4 # ASSIGN : n477 4 # ASSIGN : n478 4 # ASSIGN : n479 4 # ASSIGN : n480 4 # ASSIGN : n481 4 # ASSIGN : n482 4 # ASSIGN : n483 4 # ASSIGN : n484 4 # ASSIGN : n485 4 # ASSIGN : n486 4 # ASSIGN : n487 4 # ASSIGN : n488 4 # ASSIGN : n489 4 # ASSIGN : n490 4 # ASSIGN : n491 4 # ASSIGN : n492 4 # ASSIGN : n493 4 # ASSIGN : n494 4 # ASSIGN : n495 4 # ASSIGN : n496 4 # ASSIGN : n497 4 # ASSIGN : n498 4 # ASSIGN : n499 4 # ASSIGN : n500 4 # ASSIGN : n501 4 # ASSIGN : n502 4 # ASSIGN : n503 4 # ASSIGN : n504 4 # ASSIGN : n505 4 # ASSIGN : n506 4 # ASSIGN : n507 4 # ASSIGN : n508 4 # ASSIGN : n509 4 # ASSIGN : n510 2 # ASSIGN : n511 4 # ASSIGN : n512 4 # ASSIGN : n513 4 # ASSIGN : n514 4 # ASSIGN : n515 4 # ASSIGN : n516 4 # ASSIGN : n517 4 # ASSIGN : n518 4 # ASSIGN : n519 4 # ASSIGN : n520 4 # ASSIGN : n521 4 # ASSIGN : n522 4 # ASSIGN : n523 4 # ASSIGN : n524 4 # ASSIGN : n525 4 # ASSIGN : n526 2 # ASSIGN : n527 4 # ASSIGN : n528 4 # ASSIGN : n529 4 # ASSIGN : n530 4 # ASSIGN : n531 4 # ASSIGN : n532 4 # ASSIGN : n533 4 # ASSIGN : n534 4 # ASSIGN : n535 4 # ASSIGN : n536 4 # ASSIGN : n537 4 # ASSIGN : n538 4 # ASSIGN : n539 4 # ASSIGN : n540 4 # ASSIGN : n541 4 # ASSIGN : n542 4 # ASSIGN : n543 4 # ASSIGN : n544 4 # ASSIGN : n545 4 # ASSIGN : n546 4 # ASSIGN : n547 4 # ASSIGN : n548 4 # ASSIGN : n549 4 # ASSIGN : n550 4 # ASSIGN : n551 4 # ASSIGN : n552 4 # 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 4 # ASSIGN : n562 4 # ASSIGN : n563 4 # ASSIGN : n564 4 # ASSIGN : n565 4 # ASSIGN : n566 4 # ASSIGN : n567 4 # ASSIGN : n568 4 # ASSIGN : n569 4 # ASSIGN : n570 4 # ASSIGN : n571 5 # ASSIGN : n572 5 # ASSIGN : n573 5 # ASSIGN : n574 5 # ASSIGN : n575 5 # ASSIGN : n576 5 # ASSIGN : n577 5 # ASSIGN : n578 5 # ASSIGN : n579 5 # ASSIGN : n580 5 # ASSIGN : n581 5 # ASSIGN : n582 5 # ASSIGN : n583 5 # ASSIGN : n584 5 # ASSIGN : n585 5 # ASSIGN : n586 5 # ASSIGN : n587 5 # ASSIGN : n588 5 # ASSIGN : n589 5 # ASSIGN : n590 5 # ASSIGN : n591 5 # ASSIGN : n592 5 # ASSIGN : n593 5 # ASSIGN : n594 5 # ASSIGN : n595 5 # ASSIGN : n596 5 # ASSIGN : n597 5 # ASSIGN : n598 5 # ASSIGN : n599 5 # ASSIGN : n600 5 # ASSIGN : n601 5 # ASSIGN : n602 5 # ASSIGN : n603 5 # ASSIGN : n604 5 # ASSIGN : n605 5 # ASSIGN : n606 5 # ASSIGN : n607 5 # ASSIGN : n608 5 # ASSIGN : n609 5 # ASSIGN : n610 5 # ASSIGN : n611 5 # ASSIGN : n612 5 # ASSIGN : n613 5 # ASSIGN : n614 5 # ASSIGN : n615 5 # ASSIGN : n616 5 # ASSIGN : n617 5 # ASSIGN : n618 5 # ASSIGN : n619 5 # ASSIGN : n620 5 # ASSIGN : n621 5 # ASSIGN : n622 5 # ASSIGN : n623 5 # ASSIGN : n624 5 # ASSIGN : n625 5 # ASSIGN : n626 5 # ASSIGN : n627 5 # ASSIGN : n628 5 # ASSIGN : n629 5 # ASSIGN : n630 5 # ASSIGN : n631 5 # ASSIGN : n632 5 # ASSIGN : n633 5 # ASSIGN : n634 5 # ASSIGN : n635 5 # ASSIGN : n636 5 # ASSIGN : n637 5 # ASSIGN : n638 5 # ASSIGN : n639 5 # ASSIGN : n640 5 # ASSIGN : n641 5 # ASSIGN : n642 5 # ASSIGN : n643 5 # ASSIGN : n644 5 # ASSIGN : n645 5 # ASSIGN : n646 5 # ASSIGN : n647 5 # ASSIGN : n648 5 # ASSIGN : n649 5 # ASSIGN : n650 5 # ASSIGN : n651 5 # ASSIGN : n652 5 # ASSIGN : n653 5 # ASSIGN : n654 5 # ASSIGN : n655 5 # ASSIGN : n656 5 # ASSIGN : n657 5 # ASSIGN : n658 5 # ASSIGN : n659 5 # ASSIGN : n660 5 # ASSIGN : n661 5 # ASSIGN : n662 5 # ASSIGN : n663 5 # ASSIGN : n664 5 # ASSIGN : n665 5 # ASSIGN : n666 5 # ASSIGN : n667 5 # ASSIGN : n668 5 # ASSIGN : n669 5 # ASSIGN : n670 5 # ASSIGN : n671 5 # ASSIGN : n672 5 # ASSIGN : n673 5 # ASSIGN : n674 5 # ASSIGN : n675 5 # ASSIGN : n676 5 # ASSIGN : n677 5 # ASSIGN : n678 5 # ASSIGN : n679 5 # ASSIGN : n680 5 # ASSIGN : n681 5 # ASSIGN : n682 5 # ASSIGN : n683 5 # ASSIGN : n684 5 # ASSIGN : n685 6 # ASSIGN : n686 7 # ASSIGN : n687 8 # ASSIGN : n688 9 # ASSIGN : n689 10 # ASSIGN : n690 11 SHOW_RESULT 11 END : 11 (0 seconds) [Thu Jul 6 09:58:34 2006] SHOW_RESULT 11 CPU : 0.0500000000000007 = 0.0500000000000007 + 0 + 0 + 0 # BOUND : color 2 11 MODIFY_CNF 6 BEGIN : [Thu Jul 6 09:58:34 2006] MODIFY_CNF 6 END : 5964874 bytes (0 seconds) [Thu Jul 6 09:58:34 2006] MODIFY_CNF 6 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 6 BEGIN : [Thu Jul 6 09:58:34 2006] CMD : minisat /tmp/csp2sat13823.cnf /tmp/csp2sat13823.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 110616 329516 | 36872 0 0 nan | 0.000 % | | 100 | 110616 329516 | 40559 100 967 9.7 | 41.214 % | | 251 | 110616 329516 | 44615 251 2833 11.3 | 41.214 % | | 477 | 110616 329516 | 49076 477 4910 10.3 | 41.214 % | | 815 | 110618 329516 | 53984 813 7874 9.7 | 41.214 % | | 1322 | 110433 328952 | 59382 688 6273 9.1 | 41.228 % | ============================================================================== restarts : 6 conflicts : 1609 (1986 /sec) decisions : 4813 (5942 /sec) propagations : 448686 (553933 /sec) conflict literals : 13914 (16.22 % deleted) Memory used : 13.40 MB CPU time : 0.81 s UNSATISFIABLE VERIFY_CNF 6 END : (1 seconds) [Thu Jul 6 09:58:35 2006] VERIFY_CNF 6 CPU : 0.84 = 0 + 0 + 0.81 + 0.03 # RESULT : color 6 UNSATISFIABLE # BOUND : color 7 11 MODIFY_CNF 9 BEGIN : [Thu Jul 6 09:58:35 2006] MODIFY_CNF 9 END : 5964874 bytes (0 seconds) [Thu Jul 6 09:58:35 2006] MODIFY_CNF 9 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 9 BEGIN : [Thu Jul 6 09:58:35 2006] CMD : minisat /tmp/csp2sat13823.cnf /tmp/csp2sat13823.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 150516 449216 | 50172 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 0 (0 /sec) decisions : 2596 (6332 /sec) propagations : 28500 (69512 /sec) conflict literals : 0 ( nan % deleted) Memory used : 13.49 MB CPU time : 0.41 s SATISFIABLE VERIFY_CNF 9 END : (0 seconds) [Thu Jul 6 09:58:35 2006] VERIFY_CNF 9 CPU : 0.46 = 0 + 0 + 0.42 + 0.04 # RESULT : color 9 SATISFIABLE SHOW_RESULT 9 BEGIN : [Thu Jul 6 09:58:35 2006] # ASSIGN : color 9 # ASSIGN : n1 2 # ASSIGN : n2 3 # ASSIGN : n3 2 # ASSIGN : n4 3 # ASSIGN : n5 6 # ASSIGN : n6 3 # ASSIGN : n7 2 # ASSIGN : n8 2 # ASSIGN : n9 3 # ASSIGN : n10 3 # ASSIGN : n11 2 # ASSIGN : n12 2 # ASSIGN : n13 3 # ASSIGN : n14 6 # ASSIGN : n15 7 # ASSIGN : n16 8 # ASSIGN : n17 2 # ASSIGN : n18 9 # ASSIGN : n19 1 # ASSIGN : n20 1 # ASSIGN : n21 1 # ASSIGN : n22 3 # ASSIGN : n23 1 # ASSIGN : n24 1 # ASSIGN : n25 1 # ASSIGN : n26 1 # ASSIGN : n27 6 # ASSIGN : n28 1 # ASSIGN : n29 1 # ASSIGN : n30 1 # ASSIGN : n31 3 # ASSIGN : n32 1 # ASSIGN : n33 1 # ASSIGN : n34 1 # ASSIGN : n35 1 # ASSIGN : n36 1 # ASSIGN : n37 2 # ASSIGN : n38 2 # ASSIGN : n39 2 # ASSIGN : n40 2 # ASSIGN : n41 2 # ASSIGN : n42 2 # ASSIGN : n43 2 # ASSIGN : n44 2 # ASSIGN : n45 2 # ASSIGN : n46 2 # ASSIGN : n47 2 # ASSIGN : n48 2 # ASSIGN : n49 2 # ASSIGN : n50 7 # ASSIGN : n51 7 # ASSIGN : n52 2 # ASSIGN : n53 2 # ASSIGN : n54 2 # ASSIGN : n55 3 # ASSIGN : n56 3 # ASSIGN : n57 3 # ASSIGN : n58 3 # ASSIGN : n59 3 # ASSIGN : n60 3 # ASSIGN : n61 3 # ASSIGN : n62 3 # ASSIGN : n63 3 # ASSIGN : n64 3 # ASSIGN : n65 3 # ASSIGN : n66 3 # ASSIGN : n67 3 # ASSIGN : n68 3 # ASSIGN : n69 3 # ASSIGN : n70 3 # ASSIGN : n71 3 # ASSIGN : n72 3 # ASSIGN : n73 1 # ASSIGN : n74 1 # ASSIGN : n75 1 # ASSIGN : n76 9 # ASSIGN : n77 1 # ASSIGN : n78 1 # ASSIGN : n79 1 # ASSIGN : n80 1 # ASSIGN : n81 1 # ASSIGN : n82 1 # ASSIGN : n83 1 # ASSIGN : n84 1 # ASSIGN : n85 1 # ASSIGN : n86 1 # ASSIGN : n87 1 # ASSIGN : n88 1 # ASSIGN : n89 1 # ASSIGN : n90 1 # 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 2 # ASSIGN : n107 2 # ASSIGN : n108 2 # ASSIGN : n109 6 # ASSIGN : n110 7 # ASSIGN : n111 8 # ASSIGN : n112 1 # ASSIGN : n113 2 # ASSIGN : n114 3 # ASSIGN : n115 4 # ASSIGN : n116 4 # ASSIGN : n117 4 # ASSIGN : n118 4 # ASSIGN : n119 4 # ASSIGN : n120 4 # ASSIGN : n121 4 # ASSIGN : n122 4 # ASSIGN : n123 4 # ASSIGN : n124 4 # ASSIGN : n125 4 # ASSIGN : n126 4 # ASSIGN : n127 4 # ASSIGN : n128 4 # ASSIGN : n129 4 # ASSIGN : n130 4 # ASSIGN : n131 4 # ASSIGN : n132 4 # ASSIGN : n133 4 # ASSIGN : n134 4 # ASSIGN : n135 4 # ASSIGN : n136 4 # ASSIGN : n137 4 # ASSIGN : n138 4 # ASSIGN : n139 4 # ASSIGN : n140 4 # ASSIGN : n141 4 # ASSIGN : n142 4 # ASSIGN : n143 4 # ASSIGN : n144 4 # ASSIGN : n145 4 # ASSIGN : n146 4 # ASSIGN : n147 4 # ASSIGN : n148 4 # ASSIGN : n149 4 # ASSIGN : n150 4 # ASSIGN : n151 4 # ASSIGN : n152 4 # ASSIGN : n153 9 # ASSIGN : n154 4 # 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 9 # 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 9 # ASSIGN : n224 4 # ASSIGN : n225 4 # ASSIGN : n226 4 # ASSIGN : n227 4 # ASSIGN : n228 4 # ASSIGN : n229 5 # ASSIGN : n230 5 # ASSIGN : n231 5 # ASSIGN : n232 5 # ASSIGN : n233 5 # ASSIGN : n234 5 # ASSIGN : n235 5 # ASSIGN : n236 5 # ASSIGN : n237 5 # ASSIGN : n238 5 # ASSIGN : n239 5 # ASSIGN : n240 5 # ASSIGN : n241 5 # ASSIGN : n242 5 # ASSIGN : n243 5 # ASSIGN : n244 5 # ASSIGN : n245 5 # ASSIGN : n246 5 # ASSIGN : n247 5 # ASSIGN : n248 5 # ASSIGN : n249 5 # ASSIGN : n250 5 # ASSIGN : n251 5 # ASSIGN : n252 5 # ASSIGN : n253 5 # ASSIGN : n254 5 # ASSIGN : n255 5 # ASSIGN : n256 5 # ASSIGN : n257 5 # ASSIGN : n258 5 # ASSIGN : n259 5 # ASSIGN : n260 5 # ASSIGN : n261 5 # ASSIGN : n262 5 # ASSIGN : n263 5 # ASSIGN : n264 5 # ASSIGN : n265 5 # ASSIGN : n266 5 # ASSIGN : n267 5 # ASSIGN : n268 5 # ASSIGN : n269 5 # ASSIGN : n270 5 # ASSIGN : n271 5 # ASSIGN : n272 5 # ASSIGN : n273 5 # ASSIGN : n274 5 # ASSIGN : n275 5 # ASSIGN : n276 5 # ASSIGN : n277 5 # ASSIGN : n278 5 # ASSIGN : n279 5 # ASSIGN : n280 5 # ASSIGN : n281 5 # ASSIGN : n282 5 # ASSIGN : n283 5 # ASSIGN : n284 5 # ASSIGN : n285 5 # ASSIGN : n286 5 # ASSIGN : n287 5 # ASSIGN : n288 5 # ASSIGN : n289 5 # ASSIGN : n290 5 # ASSIGN : n291 5 # ASSIGN : n292 5 # ASSIGN : n293 5 # ASSIGN : n294 5 # ASSIGN : n295 5 # ASSIGN : n296 5 # ASSIGN : n297 5 # ASSIGN : n298 5 # ASSIGN : n299 5 # ASSIGN : n300 5 # ASSIGN : n301 5 # ASSIGN : n302 5 # ASSIGN : n303 5 # ASSIGN : n304 5 # ASSIGN : n305 5 # ASSIGN : n306 5 # ASSIGN : n307 5 # ASSIGN : n308 5 # 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 5 # ASSIGN : n339 5 # ASSIGN : n340 5 # ASSIGN : n341 5 # ASSIGN : n342 5 # ASSIGN : n343 1 # 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 1 # 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 9 # ASSIGN : n404 1 # ASSIGN : n405 1 # ASSIGN : n406 1 # ASSIGN : n407 1 # 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 2 # ASSIGN : n458 2 # ASSIGN : n459 2 # ASSIGN : n460 2 # ASSIGN : n461 2 # ASSIGN : n462 2 # 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 2 # ASSIGN : n519 2 # ASSIGN : n520 2 # ASSIGN : n521 2 # ASSIGN : n522 2 # 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 2 # 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 3 # ASSIGN : n572 3 # ASSIGN : n573 3 # ASSIGN : n574 3 # ASSIGN : n575 3 # ASSIGN : n576 3 # ASSIGN : n577 3 # ASSIGN : n578 3 # ASSIGN : n579 3 # ASSIGN : n580 3 # ASSIGN : n581 3 # ASSIGN : n582 3 # ASSIGN : n583 3 # ASSIGN : n584 3 # ASSIGN : n585 3 # ASSIGN : n586 3 # ASSIGN : n587 3 # ASSIGN : n588 3 # ASSIGN : n589 3 # ASSIGN : n590 3 # ASSIGN : n591 3 # ASSIGN : n592 3 # ASSIGN : n593 3 # ASSIGN : n594 3 # ASSIGN : n595 3 # ASSIGN : n596 3 # ASSIGN : n597 3 # ASSIGN : n598 3 # ASSIGN : n599 3 # ASSIGN : n600 3 # ASSIGN : n601 3 # ASSIGN : n602 3 # ASSIGN : n603 3 # ASSIGN : n604 3 # ASSIGN : n605 3 # ASSIGN : n606 3 # ASSIGN : n607 3 # ASSIGN : n608 3 # ASSIGN : n609 3 # ASSIGN : n610 3 # ASSIGN : n611 3 # ASSIGN : n612 3 # ASSIGN : n613 3 # ASSIGN : n614 3 # ASSIGN : n615 3 # ASSIGN : n616 3 # ASSIGN : n617 3 # ASSIGN : n618 3 # 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 3 # ASSIGN : n662 3 # 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 3 # ASSIGN : n674 3 # ASSIGN : n675 3 # ASSIGN : n676 3 # ASSIGN : n677 3 # ASSIGN : n678 3 # ASSIGN : n679 3 # ASSIGN : n680 3 # ASSIGN : n681 3 # ASSIGN : n682 3 # ASSIGN : n683 3 # ASSIGN : n684 3 # ASSIGN : n685 4 # ASSIGN : n686 5 # ASSIGN : n687 6 # ASSIGN : n688 7 # ASSIGN : n689 8 # ASSIGN : n690 9 SHOW_RESULT 9 END : 9 (1 seconds) [Thu Jul 6 09:58:36 2006] SHOW_RESULT 9 CPU : 0.0500000000000007 = 0.0500000000000007 + 0 + 0 + 0 # BOUND : color 7 9 MODIFY_CNF 8 BEGIN : [Thu Jul 6 09:58:36 2006] MODIFY_CNF 8 END : 5964874 bytes (0 seconds) [Thu Jul 6 09:58:36 2006] MODIFY_CNF 8 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 8 BEGIN : [Thu Jul 6 09:58:36 2006] CMD : minisat /tmp/csp2sat13823.cnf /tmp/csp2sat13823.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 137216 409316 | 45738 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 0 (0 /sec) decisions : 2540 (5773 /sec) propagations : 28500 (64773 /sec) conflict literals : 0 ( nan % deleted) Memory used : 13.49 MB CPU time : 0.44 s SATISFIABLE VERIFY_CNF 8 END : (0 seconds) [Thu Jul 6 09:58:36 2006] VERIFY_CNF 8 CPU : 0.49 = 0 + 0 + 0.45 + 0.04 # RESULT : color 8 SATISFIABLE SHOW_RESULT 8 BEGIN : [Thu Jul 6 09:58:36 2006] # ASSIGN : color 8 # ASSIGN : n1 7 # ASSIGN : n2 8 # ASSIGN : n3 1 # ASSIGN : n4 1 # ASSIGN : n5 8 # ASSIGN : n6 8 # ASSIGN : n7 1 # ASSIGN : n8 1 # ASSIGN : n9 8 # ASSIGN : n10 8 # ASSIGN : n11 1 # ASSIGN : n12 1 # ASSIGN : n13 7 # ASSIGN : n14 8 # ASSIGN : n15 4 # ASSIGN : n16 5 # ASSIGN : n17 1 # ASSIGN : n18 6 # ASSIGN : n19 2 # ASSIGN : n20 2 # ASSIGN : n21 2 # ASSIGN : n22 2 # ASSIGN : n23 2 # ASSIGN : n24 2 # ASSIGN : n25 2 # ASSIGN : n26 2 # ASSIGN : n27 7 # ASSIGN : n28 2 # ASSIGN : n29 2 # ASSIGN : n30 2 # ASSIGN : n31 7 # ASSIGN : n32 2 # ASSIGN : n33 2 # ASSIGN : n34 2 # ASSIGN : n35 2 # ASSIGN : n36 2 # ASSIGN : n37 4 # ASSIGN : n38 4 # ASSIGN : n39 4 # ASSIGN : n40 4 # ASSIGN : n41 4 # ASSIGN : n42 4 # ASSIGN : n43 4 # ASSIGN : n44 4 # ASSIGN : n45 4 # ASSIGN : n46 4 # ASSIGN : n47 4 # ASSIGN : n48 4 # ASSIGN : n49 4 # ASSIGN : n50 8 # ASSIGN : n51 4 # ASSIGN : n52 4 # ASSIGN : n53 4 # ASSIGN : n54 4 # ASSIGN : n55 2 # ASSIGN : n56 2 # ASSIGN : n57 2 # ASSIGN : n58 2 # ASSIGN : n59 2 # ASSIGN : n60 2 # ASSIGN : n61 5 # ASSIGN : n62 5 # ASSIGN : n63 5 # ASSIGN : n64 2 # ASSIGN : n65 5 # ASSIGN : n66 5 # ASSIGN : n67 2 # ASSIGN : n68 5 # ASSIGN : n69 2 # ASSIGN : n70 2 # ASSIGN : n71 2 # ASSIGN : n72 2 # ASSIGN : n73 1 # ASSIGN : n74 1 # ASSIGN : n75 1 # ASSIGN : n76 6 # ASSIGN : n77 1 # ASSIGN : n78 1 # ASSIGN : n79 1 # ASSIGN : n80 1 # ASSIGN : n81 1 # ASSIGN : n82 1 # ASSIGN : n83 1 # ASSIGN : n84 1 # ASSIGN : n85 1 # ASSIGN : n86 1 # ASSIGN : n87 1 # ASSIGN : n88 1 # ASSIGN : n89 1 # ASSIGN : n90 1 # ASSIGN : n91 7 # ASSIGN : n92 7 # ASSIGN : n93 7 # ASSIGN : n94 7 # ASSIGN : n95 7 # ASSIGN : n96 7 # ASSIGN : n97 7 # ASSIGN : n98 7 # ASSIGN : n99 7 # ASSIGN : n100 7 # ASSIGN : n101 7 # ASSIGN : n102 7 # ASSIGN : n103 7 # ASSIGN : n104 7 # ASSIGN : n105 7 # ASSIGN : n106 7 # ASSIGN : n107 7 # ASSIGN : n108 7 # ASSIGN : n109 8 # ASSIGN : n110 4 # ASSIGN : n111 5 # ASSIGN : n112 6 # ASSIGN : n113 7 # ASSIGN : n114 2 # 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 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 3 # ASSIGN : n146 3 # ASSIGN : n147 3 # ASSIGN : n148 3 # ASSIGN : n149 3 # ASSIGN : n150 3 # ASSIGN : n151 3 # ASSIGN : n152 3 # ASSIGN : n153 8 # ASSIGN : n154 1 # ASSIGN : n155 1 # ASSIGN : n156 1 # ASSIGN : n157 3 # ASSIGN : n158 3 # ASSIGN : n159 1 # ASSIGN : n160 1 # ASSIGN : n161 1 # ASSIGN : n162 1 # ASSIGN : n163 1 # ASSIGN : n164 1 # ASSIGN : n165 1 # ASSIGN : n166 1 # ASSIGN : n167 8 # ASSIGN : n168 1 # ASSIGN : n169 3 # ASSIGN : n170 3 # ASSIGN : n171 3 # ASSIGN : n172 3 # ASSIGN : n173 3 # ASSIGN : n174 3 # ASSIGN : n175 3 # ASSIGN : n176 3 # ASSIGN : n177 3 # ASSIGN : n178 3 # ASSIGN : n179 3 # ASSIGN : n180 3 # ASSIGN : n181 3 # ASSIGN : n182 3 # ASSIGN : n183 3 # ASSIGN : n184 3 # ASSIGN : n185 3 # ASSIGN : n186 3 # ASSIGN : n187 1 # ASSIGN : n188 1 # ASSIGN : n189 1 # ASSIGN : n190 1 # ASSIGN : n191 1 # ASSIGN : n192 1 # ASSIGN : n193 1 # ASSIGN : n194 1 # ASSIGN : n195 1 # ASSIGN : n196 1 # ASSIGN : n197 1 # ASSIGN : n198 1 # ASSIGN : n199 1 # ASSIGN : n200 3 # ASSIGN : n201 8 # ASSIGN : n202 1 # ASSIGN : n203 1 # ASSIGN : n204 1 # ASSIGN : n205 3 # ASSIGN : n206 3 # ASSIGN : n207 3 # ASSIGN : n208 3 # ASSIGN : n209 3 # ASSIGN : n210 7 # ASSIGN : n211 3 # ASSIGN : n212 3 # ASSIGN : n213 3 # ASSIGN : n214 3 # ASSIGN : n215 3 # ASSIGN : n216 3 # ASSIGN : n217 3 # ASSIGN : n218 3 # ASSIGN : n219 3 # ASSIGN : n220 3 # ASSIGN : n221 3 # ASSIGN : n222 3 # ASSIGN : n223 8 # ASSIGN : n224 3 # ASSIGN : n225 1 # ASSIGN : n226 1 # ASSIGN : n227 3 # ASSIGN : n228 1 # 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 4 # ASSIGN : n241 4 # ASSIGN : n242 4 # ASSIGN : n243 4 # ASSIGN : n244 4 # 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 4 # ASSIGN : n278 4 # ASSIGN : n279 4 # ASSIGN : n280 4 # ASSIGN : n281 4 # ASSIGN : n282 4 # ASSIGN : n283 4 # ASSIGN : n284 4 # ASSIGN : n285 4 # ASSIGN : n286 4 # ASSIGN : n287 4 # ASSIGN : n288 4 # ASSIGN : n289 2 # ASSIGN : n290 2 # ASSIGN : n291 4 # ASSIGN : n292 4 # ASSIGN : n293 4 # ASSIGN : n294 4 # ASSIGN : n295 2 # ASSIGN : n296 2 # ASSIGN : n297 2 # ASSIGN : n298 4 # ASSIGN : n299 2 # ASSIGN : n300 2 # ASSIGN : n301 4 # ASSIGN : n302 4 # ASSIGN : n303 4 # ASSIGN : n304 4 # ASSIGN : n305 4 # ASSIGN : n306 4 # ASSIGN : n307 4 # ASSIGN : n308 4 # ASSIGN : n309 4 # ASSIGN : n310 4 # ASSIGN : n311 4 # ASSIGN : n312 4 # ASSIGN : n313 4 # ASSIGN : n314 4 # ASSIGN : n315 4 # ASSIGN : n316 4 # ASSIGN : n317 4 # ASSIGN : n318 4 # ASSIGN : n319 4 # ASSIGN : n320 4 # ASSIGN : n321 4 # ASSIGN : n322 4 # ASSIGN : n323 4 # ASSIGN : n324 4 # ASSIGN : n325 2 # ASSIGN : n326 2 # ASSIGN : n327 4 # ASSIGN : n328 4 # ASSIGN : n329 4 # ASSIGN : n330 4 # ASSIGN : n331 2 # ASSIGN : n332 2 # ASSIGN : n333 4 # ASSIGN : n334 4 # ASSIGN : n335 2 # ASSIGN : n336 2 # ASSIGN : n337 4 # ASSIGN : n338 4 # ASSIGN : n339 4 # ASSIGN : n340 4 # ASSIGN : n341 2 # ASSIGN : n342 4 # 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 5 # 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 3 # 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 1 # ASSIGN : n458 1 # ASSIGN : n459 1 # ASSIGN : n460 1 # ASSIGN : n461 1 # ASSIGN : n462 1 # ASSIGN : n463 1 # ASSIGN : n464 1 # ASSIGN : n465 1 # ASSIGN : n466 1 # ASSIGN : n467 1 # ASSIGN : n468 1 # ASSIGN : n469 1 # ASSIGN : n470 1 # ASSIGN : n471 1 # ASSIGN : n472 1 # ASSIGN : n473 1 # ASSIGN : n474 1 # ASSIGN : n475 1 # ASSIGN : n476 1 # ASSIGN : n477 1 # ASSIGN : n478 1 # ASSIGN : n479 1 # ASSIGN : n480 1 # ASSIGN : n481 1 # ASSIGN : n482 1 # ASSIGN : n483 1 # ASSIGN : n484 1 # ASSIGN : n485 1 # ASSIGN : n486 1 # ASSIGN : n487 1 # ASSIGN : n488 1 # ASSIGN : n489 1 # ASSIGN : n490 1 # ASSIGN : n491 1 # ASSIGN : n492 1 # ASSIGN : n493 1 # ASSIGN : n494 1 # ASSIGN : n495 1 # ASSIGN : n496 1 # ASSIGN : n497 1 # ASSIGN : n498 1 # ASSIGN : n499 1 # ASSIGN : n500 1 # ASSIGN : n501 1 # ASSIGN : n502 1 # ASSIGN : n503 1 # ASSIGN : n504 1 # ASSIGN : n505 1 # ASSIGN : n506 1 # ASSIGN : n507 1 # ASSIGN : n508 1 # ASSIGN : n509 1 # ASSIGN : n510 1 # ASSIGN : n511 1 # ASSIGN : n512 1 # ASSIGN : n513 1 # ASSIGN : n514 1 # ASSIGN : n515 1 # ASSIGN : n516 1 # ASSIGN : n517 1 # ASSIGN : n518 1 # ASSIGN : n519 1 # ASSIGN : n520 1 # ASSIGN : n521 1 # ASSIGN : n522 1 # ASSIGN : n523 1 # ASSIGN : n524 1 # ASSIGN : n525 1 # ASSIGN : n526 1 # ASSIGN : n527 1 # ASSIGN : n528 1 # ASSIGN : n529 1 # ASSIGN : n530 1 # ASSIGN : n531 1 # ASSIGN : n532 1 # ASSIGN : n533 1 # ASSIGN : n534 1 # ASSIGN : n535 1 # ASSIGN : n536 1 # ASSIGN : n537 1 # ASSIGN : n538 1 # ASSIGN : n539 1 # ASSIGN : n540 1 # ASSIGN : n541 1 # ASSIGN : n542 1 # ASSIGN : n543 1 # ASSIGN : n544 1 # ASSIGN : n545 1 # ASSIGN : n546 1 # ASSIGN : n547 1 # ASSIGN : n548 1 # ASSIGN : n549 1 # ASSIGN : n550 1 # ASSIGN : n551 1 # ASSIGN : n552 1 # ASSIGN : n553 1 # ASSIGN : n554 1 # ASSIGN : n555 1 # ASSIGN : n556 1 # ASSIGN : n557 1 # ASSIGN : n558 1 # ASSIGN : n559 1 # ASSIGN : n560 1 # ASSIGN : n561 1 # ASSIGN : n562 1 # ASSIGN : n563 1 # ASSIGN : n564 1 # ASSIGN : n565 1 # ASSIGN : n566 1 # ASSIGN : n567 1 # ASSIGN : n568 1 # ASSIGN : n569 1 # ASSIGN : n570 1 # 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 2 # ASSIGN : n608 2 # ASSIGN : n609 2 # ASSIGN : n610 2 # ASSIGN : n611 2 # ASSIGN : n612 2 # ASSIGN : n613 2 # ASSIGN : n614 2 # ASSIGN : n615 2 # ASSIGN : n616 2 # ASSIGN : n617 2 # ASSIGN : n618 2 # ASSIGN : n619 2 # ASSIGN : n620 2 # ASSIGN : n621 2 # ASSIGN : n622 2 # ASSIGN : n623 2 # ASSIGN : n624 2 # ASSIGN : n625 2 # ASSIGN : n626 2 # ASSIGN : n627 2 # ASSIGN : n628 2 # ASSIGN : n629 2 # ASSIGN : n630 2 # ASSIGN : n631 2 # ASSIGN : n632 2 # ASSIGN : n633 2 # ASSIGN : n634 2 # ASSIGN : n635 2 # ASSIGN : n636 2 # ASSIGN : n637 2 # ASSIGN : n638 2 # ASSIGN : n639 2 # ASSIGN : n640 2 # ASSIGN : n641 2 # ASSIGN : n642 2 # ASSIGN : n643 2 # ASSIGN : n644 2 # ASSIGN : n645 2 # ASSIGN : n646 2 # ASSIGN : n647 2 # ASSIGN : n648 2 # ASSIGN : n649 2 # ASSIGN : n650 2 # ASSIGN : n651 2 # ASSIGN : n652 2 # ASSIGN : n653 2 # ASSIGN : n654 2 # ASSIGN : n655 2 # ASSIGN : n656 2 # ASSIGN : n657 2 # ASSIGN : n658 2 # ASSIGN : n659 2 # ASSIGN : n660 2 # ASSIGN : n661 2 # ASSIGN : n662 2 # ASSIGN : n663 2 # ASSIGN : n664 2 # ASSIGN : n665 2 # ASSIGN : n666 2 # ASSIGN : n667 2 # ASSIGN : n668 2 # ASSIGN : n669 2 # ASSIGN : n670 2 # ASSIGN : n671 2 # ASSIGN : n672 2 # ASSIGN : n673 2 # ASSIGN : n674 2 # ASSIGN : n675 2 # ASSIGN : n676 2 # ASSIGN : n677 2 # ASSIGN : n678 2 # ASSIGN : n679 2 # ASSIGN : n680 2 # ASSIGN : n681 2 # ASSIGN : n682 2 # ASSIGN : n683 2 # ASSIGN : n684 2 # ASSIGN : n685 3 # ASSIGN : n686 4 # ASSIGN : n687 5 # ASSIGN : n688 6 # ASSIGN : n689 7 # ASSIGN : n690 8 SHOW_RESULT 8 END : 8 (0 seconds) [Thu Jul 6 09:58:36 2006] SHOW_RESULT 8 CPU : 0.0499999999999992 = 0.0399999999999991 + 0.01 + 0 + 0 # BOUND : color 7 8 MODIFY_CNF 7 BEGIN : [Thu Jul 6 09:58:36 2006] MODIFY_CNF 7 END : 5964874 bytes (0 seconds) [Thu Jul 6 09:58:36 2006] MODIFY_CNF 7 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 7 BEGIN : [Thu Jul 6 09:58:36 2006] CMD : minisat /tmp/csp2sat13823.cnf /tmp/csp2sat13823.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 123916 369416 | 41305 0 0 nan | 0.000 % | | 100 | 123916 369416 | 45435 100 946 9.5 | 38.789 % | | 250 | 123916 369416 | 49979 250 3898 15.6 | 38.789 % | | 476 | 123916 369416 | 54976 476 7973 16.8 | 38.789 % | | 813 | 123916 369416 | 60474 813 13653 16.8 | 38.789 % | | 1320 | 123916 369416 | 66522 1320 19348 14.7 | 38.789 % | | 2081 | 123916 369416 | 73174 2081 30640 14.7 | 38.789 % | | 3220 | 123916 369416 | 80491 3220 48376 15.0 | 38.789 % | | 4928 | 123916 369416 | 88540 4928 76086 15.4 | 38.789 % | | 7490 | 123916 369416 | 97395 7490 110292 14.7 | 38.789 % | | 11334 | 123916 369416 | 107134 11334 159956 14.1 | 38.789 % | | 17100 | 123916 369416 | 117847 17100 236253 13.8 | 38.789 % | | 25750 | 123857 369242 | 129632 17582 235177 13.4 | 38.796 % | | 38724 | 123741 368894 | 142596 14377 168331 11.7 | 38.811 % | ============================================================================== restarts : 14 conflicts : 43354 (2215 /sec) decisions : 62471 (3192 /sec) propagations : 10648158 (544106 /sec) conflict literals : 529511 (25.05 % deleted) Memory used : 13.94 MB CPU time : 19.57 s UNSATISFIABLE VERIFY_CNF 7 END : (20 seconds) [Thu Jul 6 09:58:56 2006] VERIFY_CNF 7 CPU : 19.62 = 0 + 0 + 19.57 + 0.05 # RESULT : color 7 UNSATISFIABLE # BOUND : color 8 8 MAIN END : (47 seconds) [Thu Jul 6 09:58:56 2006] MAIN CPU : 45.9 = 23.87 + 0.18 + 21.63 + 0.22