# TIMEOUT 7200 MAIN BEGIN : [Fri Jul 7 11:16:03 2006] READ BEGIN : csp/DSJR500.1.csp [Fri Jul 7 11:16:03 2006] READ END : csp/DSJR500.1.csp (6 seconds) [Fri Jul 7 11:16:09 2006] READ CPU : 6 = 5.92 + 0.08 + 0 + 0 # BOUND : color 2 15 GENERATE_CNF 15 BEGIN : [Fri Jul 7 11:16:09 2006] GENERATE_CNF 15 END : 15625 variables 125721 clauses 2342650 bytes (6 seconds) [Fri Jul 7 11:16:15 2006] GENERATE_CNF 15 CPU : 5.83 = 5.8 + 0.03 + 0 + 0 MODIFY_CNF 8 BEGIN : [Fri Jul 7 11:16:15 2006] MODIFY_CNF 8 END : 2342654 bytes (0 seconds) [Fri Jul 7 11:16:15 2006] MODIFY_CNF 8 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 8 BEGIN : [Fri Jul 7 11:16:15 2006] CMD : minisat /tmp/csp2sat5989.cnf /tmp/csp2sat5989.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 72946 218386 | 24315 0 0 nan | 0.000 % | | 100 | 72946 218386 | 26746 100 656 6.6 | 32.058 % | | 252 | 72946 218386 | 29421 252 1771 7.0 | 32.058 % | | 477 | 72946 218386 | 32363 477 3795 8.0 | 32.058 % | | 815 | 72946 218386 | 35599 815 7257 8.9 | 32.058 % | | 1321 | 72946 218386 | 39159 1321 12341 9.3 | 32.058 % | | 2080 | 72946 218386 | 43075 2080 18683 9.0 | 32.058 % | | 3219 | 72946 218386 | 47383 3219 27991 8.7 | 32.058 % | | 4927 | 72946 218386 | 52121 4927 43484 8.8 | 32.058 % | | 7489 | 72948 218386 | 57333 7487 64336 8.6 | 32.058 % | ============================================================================== restarts : 10 conflicts : 9743 (9459 /sec) decisions : 11835 (11490 /sec) propagations : 517922 (502837 /sec) conflict literals : 80108 (14.02 % deleted) Memory used : 6.78 MB CPU time : 1.03 s UNSATISFIABLE VERIFY_CNF 8 END : (1 seconds) [Fri Jul 7 11:16:16 2006] VERIFY_CNF 8 CPU : 1.07 = 0 + 0 + 1.03 + 0.04 # RESULT : color 8 UNSATISFIABLE # BOUND : color 9 15 MODIFY_CNF 12 BEGIN : [Fri Jul 7 11:16:16 2006] MODIFY_CNF 12 END : 2342655 bytes (0 seconds) [Fri Jul 7 11:16:16 2006] MODIFY_CNF 12 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 12 BEGIN : [Fri Jul 7 11:16:16 2006] CMD : minisat /tmp/csp2sat5989.cnf /tmp/csp2sat5989.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 101386 303706 | 33795 0 0 nan | 0.000 % | | 100 | 101386 303706 | 37174 100 870 8.7 | 19.232 % | | 251 | 101386 303706 | 40891 251 3009 12.0 | 19.232 % | | 476 | 101386 303706 | 44981 476 4538 9.5 | 19.232 % | | 814 | 101386 303706 | 49479 814 7373 9.1 | 19.232 % | | 1320 | 101386 303706 | 54427 1320 11882 9.0 | 19.232 % | ============================================================================== restarts : 6 conflicts : 1596 (4836 /sec) decisions : 12319 (37330 /sec) propagations : 190351 (576821 /sec) conflict literals : 13695 (8.94 % deleted) Memory used : 6.77 MB CPU time : 0.33 s SATISFIABLE VERIFY_CNF 12 END : (1 seconds) [Fri Jul 7 11:16:17 2006] VERIFY_CNF 12 CPU : 0.35 = 0 + 0 + 0.33 + 0.02 # RESULT : color 12 SATISFIABLE SHOW_RESULT 12 BEGIN : [Fri Jul 7 11:16:17 2006] # ASSIGN : color 12 # ASSIGN : n1 11 # ASSIGN : n2 3 # ASSIGN : n3 6 # ASSIGN : n4 4 # ASSIGN : n5 3 # ASSIGN : n6 3 # ASSIGN : n7 2 # ASSIGN : n8 3 # ASSIGN : n9 2 # ASSIGN : n10 1 # ASSIGN : n11 6 # ASSIGN : n12 3 # ASSIGN : n13 4 # ASSIGN : n14 8 # ASSIGN : n15 1 # ASSIGN : n16 3 # ASSIGN : n17 6 # ASSIGN : n18 2 # ASSIGN : n19 3 # ASSIGN : n20 2 # ASSIGN : n21 5 # ASSIGN : n22 9 # ASSIGN : n23 2 # ASSIGN : n24 7 # ASSIGN : n25 1 # ASSIGN : n26 9 # ASSIGN : n27 12 # ASSIGN : n28 7 # ASSIGN : n29 3 # ASSIGN : n30 4 # ASSIGN : n31 4 # ASSIGN : n32 2 # ASSIGN : n33 4 # ASSIGN : n34 3 # ASSIGN : n35 1 # ASSIGN : n36 3 # ASSIGN : n37 10 # ASSIGN : n38 6 # ASSIGN : n39 10 # ASSIGN : n40 12 # ASSIGN : n41 12 # ASSIGN : n42 2 # ASSIGN : n43 4 # ASSIGN : n44 4 # ASSIGN : n45 6 # ASSIGN : n46 4 # ASSIGN : n47 9 # ASSIGN : n48 6 # ASSIGN : n49 11 # ASSIGN : n50 3 # ASSIGN : n51 6 # ASSIGN : n52 6 # ASSIGN : n53 7 # ASSIGN : n54 5 # ASSIGN : n55 8 # ASSIGN : n56 4 # ASSIGN : n57 2 # ASSIGN : n58 2 # ASSIGN : n59 1 # ASSIGN : n60 3 # ASSIGN : n61 6 # ASSIGN : n62 12 # ASSIGN : n63 3 # ASSIGN : n64 2 # ASSIGN : n65 2 # ASSIGN : n66 4 # ASSIGN : n67 3 # ASSIGN : n68 5 # ASSIGN : n69 2 # ASSIGN : n70 5 # ASSIGN : n71 6 # ASSIGN : n72 3 # ASSIGN : n73 2 # ASSIGN : n74 3 # ASSIGN : n75 6 # ASSIGN : n76 1 # ASSIGN : n77 2 # ASSIGN : n78 5 # ASSIGN : n79 5 # ASSIGN : n80 9 # ASSIGN : n81 5 # ASSIGN : n82 8 # ASSIGN : n83 4 # ASSIGN : n84 8 # ASSIGN : n85 12 # ASSIGN : n86 5 # ASSIGN : n87 10 # ASSIGN : n88 12 # ASSIGN : n89 5 # ASSIGN : n90 11 # ASSIGN : n91 4 # ASSIGN : n92 6 # ASSIGN : n93 11 # ASSIGN : n94 8 # ASSIGN : n95 9 # ASSIGN : n96 10 # ASSIGN : n97 7 # ASSIGN : n98 8 # ASSIGN : n99 11 # ASSIGN : n100 5 # ASSIGN : n101 12 # ASSIGN : n102 9 # ASSIGN : n103 5 # ASSIGN : n104 7 # ASSIGN : n105 1 # ASSIGN : n106 12 # ASSIGN : n107 6 # ASSIGN : n108 6 # ASSIGN : n109 12 # ASSIGN : n110 8 # ASSIGN : n111 11 # ASSIGN : n112 5 # ASSIGN : n113 10 # ASSIGN : n114 4 # ASSIGN : n115 4 # ASSIGN : n116 11 # ASSIGN : n117 5 # ASSIGN : n118 10 # ASSIGN : n119 1 # ASSIGN : n120 7 # ASSIGN : n121 6 # ASSIGN : n122 7 # ASSIGN : n123 3 # ASSIGN : n124 11 # ASSIGN : n125 10 # ASSIGN : n126 7 # ASSIGN : n127 5 # ASSIGN : n128 3 # ASSIGN : n129 11 # ASSIGN : n130 1 # ASSIGN : n131 7 # ASSIGN : n132 10 # ASSIGN : n133 4 # ASSIGN : n134 6 # ASSIGN : n135 4 # ASSIGN : n136 1 # ASSIGN : n137 4 # ASSIGN : n138 11 # ASSIGN : n139 9 # ASSIGN : n140 9 # ASSIGN : n141 8 # ASSIGN : n142 1 # ASSIGN : n143 12 # ASSIGN : n144 4 # ASSIGN : n145 6 # ASSIGN : n146 4 # ASSIGN : n147 11 # ASSIGN : n148 2 # ASSIGN : n149 9 # ASSIGN : n150 6 # ASSIGN : n151 9 # ASSIGN : n152 5 # ASSIGN : n153 4 # ASSIGN : n154 6 # ASSIGN : n155 11 # ASSIGN : n156 5 # ASSIGN : n157 5 # ASSIGN : n158 4 # ASSIGN : n159 8 # ASSIGN : n160 6 # ASSIGN : n161 11 # ASSIGN : n162 4 # ASSIGN : n163 1 # ASSIGN : n164 8 # ASSIGN : n165 6 # ASSIGN : n166 11 # ASSIGN : n167 4 # ASSIGN : n168 8 # ASSIGN : n169 5 # ASSIGN : n170 3 # ASSIGN : n171 11 # ASSIGN : n172 10 # ASSIGN : n173 5 # ASSIGN : n174 8 # ASSIGN : n175 8 # ASSIGN : n176 9 # ASSIGN : n177 9 # ASSIGN : n178 9 # ASSIGN : n179 11 # ASSIGN : n180 7 # ASSIGN : n181 9 # ASSIGN : n182 7 # ASSIGN : n183 10 # ASSIGN : n184 7 # ASSIGN : n185 2 # ASSIGN : n186 9 # ASSIGN : n187 12 # ASSIGN : n188 10 # ASSIGN : n189 6 # ASSIGN : n190 7 # ASSIGN : n191 8 # ASSIGN : n192 11 # ASSIGN : n193 12 # ASSIGN : n194 8 # ASSIGN : n195 7 # ASSIGN : n196 4 # ASSIGN : n197 9 # ASSIGN : n198 6 # ASSIGN : n199 12 # ASSIGN : n200 9 # ASSIGN : n201 3 # ASSIGN : n202 9 # ASSIGN : n203 3 # ASSIGN : n204 3 # ASSIGN : n205 11 # ASSIGN : n206 12 # ASSIGN : n207 7 # ASSIGN : n208 8 # ASSIGN : n209 6 # ASSIGN : n210 2 # ASSIGN : n211 4 # ASSIGN : n212 7 # ASSIGN : n213 8 # ASSIGN : n214 11 # ASSIGN : n215 5 # ASSIGN : n216 12 # ASSIGN : n217 12 # ASSIGN : n218 12 # ASSIGN : n219 8 # ASSIGN : n220 10 # ASSIGN : n221 2 # ASSIGN : n222 10 # ASSIGN : n223 1 # ASSIGN : n224 10 # ASSIGN : n225 3 # ASSIGN : n226 7 # ASSIGN : n227 10 # ASSIGN : n228 9 # ASSIGN : n229 8 # ASSIGN : n230 12 # ASSIGN : n231 11 # ASSIGN : n232 12 # ASSIGN : n233 10 # ASSIGN : n234 11 # ASSIGN : n235 12 # ASSIGN : n236 6 # ASSIGN : n237 10 # ASSIGN : n238 9 # ASSIGN : n239 7 # ASSIGN : n240 11 # ASSIGN : n241 8 # ASSIGN : n242 6 # ASSIGN : n243 10 # ASSIGN : n244 7 # ASSIGN : n245 9 # ASSIGN : n246 11 # ASSIGN : n247 3 # ASSIGN : n248 5 # ASSIGN : n249 11 # ASSIGN : n250 7 # ASSIGN : n251 4 # ASSIGN : n252 6 # ASSIGN : n253 5 # ASSIGN : n254 3 # ASSIGN : n255 8 # ASSIGN : n256 12 # ASSIGN : n257 9 # ASSIGN : n258 9 # ASSIGN : n259 10 # ASSIGN : n260 11 # ASSIGN : n261 6 # ASSIGN : n262 12 # ASSIGN : n263 10 # ASSIGN : n264 5 # ASSIGN : n265 4 # ASSIGN : n266 7 # ASSIGN : n267 4 # ASSIGN : n268 7 # ASSIGN : n269 4 # ASSIGN : n270 10 # ASSIGN : n271 5 # ASSIGN : n272 12 # ASSIGN : n273 5 # ASSIGN : n274 8 # ASSIGN : n275 9 # ASSIGN : n276 10 # ASSIGN : n277 4 # ASSIGN : n278 11 # ASSIGN : n279 7 # ASSIGN : n280 10 # ASSIGN : n281 4 # ASSIGN : n282 2 # ASSIGN : n283 12 # ASSIGN : n284 5 # ASSIGN : n285 5 # ASSIGN : n286 7 # ASSIGN : n287 7 # ASSIGN : n288 10 # ASSIGN : n289 2 # ASSIGN : n290 12 # ASSIGN : n291 10 # ASSIGN : n292 11 # ASSIGN : n293 2 # ASSIGN : n294 11 # ASSIGN : n295 7 # ASSIGN : n296 8 # ASSIGN : n297 8 # ASSIGN : n298 1 # ASSIGN : n299 7 # ASSIGN : n300 1 # ASSIGN : n301 12 # ASSIGN : n302 11 # ASSIGN : n303 9 # ASSIGN : n304 12 # ASSIGN : n305 9 # ASSIGN : n306 9 # ASSIGN : n307 11 # ASSIGN : n308 12 # ASSIGN : n309 2 # ASSIGN : n310 3 # ASSIGN : n311 11 # ASSIGN : n312 11 # ASSIGN : n313 3 # ASSIGN : n314 1 # ASSIGN : n315 12 # ASSIGN : n316 10 # ASSIGN : n317 12 # ASSIGN : n318 12 # ASSIGN : n319 5 # ASSIGN : n320 10 # ASSIGN : n321 8 # ASSIGN : n322 7 # ASSIGN : n323 6 # ASSIGN : n324 7 # ASSIGN : n325 4 # ASSIGN : n326 12 # ASSIGN : n327 4 # ASSIGN : n328 3 # ASSIGN : n329 2 # ASSIGN : n330 12 # ASSIGN : n331 8 # ASSIGN : n332 9 # ASSIGN : n333 12 # ASSIGN : n334 7 # ASSIGN : n335 9 # ASSIGN : n336 1 # ASSIGN : n337 10 # ASSIGN : n338 12 # ASSIGN : n339 12 # ASSIGN : n340 8 # ASSIGN : n341 9 # ASSIGN : n342 8 # ASSIGN : n343 6 # ASSIGN : n344 5 # ASSIGN : n345 8 # ASSIGN : n346 10 # ASSIGN : n347 10 # ASSIGN : n348 12 # ASSIGN : n349 10 # ASSIGN : n350 7 # ASSIGN : n351 7 # ASSIGN : n352 9 # ASSIGN : n353 12 # ASSIGN : n354 6 # ASSIGN : n355 5 # ASSIGN : n356 10 # ASSIGN : n357 8 # ASSIGN : n358 7 # ASSIGN : n359 11 # ASSIGN : n360 11 # ASSIGN : n361 8 # ASSIGN : n362 2 # ASSIGN : n363 6 # ASSIGN : n364 9 # ASSIGN : n365 8 # ASSIGN : n366 10 # ASSIGN : n367 11 # ASSIGN : n368 6 # ASSIGN : n369 8 # ASSIGN : n370 11 # ASSIGN : n371 12 # ASSIGN : n372 12 # ASSIGN : n373 7 # ASSIGN : n374 12 # ASSIGN : n375 11 # ASSIGN : n376 7 # ASSIGN : n377 8 # ASSIGN : n378 12 # ASSIGN : n379 10 # ASSIGN : n380 9 # ASSIGN : n381 2 # ASSIGN : n382 4 # ASSIGN : n383 12 # ASSIGN : n384 8 # ASSIGN : n385 10 # ASSIGN : n386 11 # ASSIGN : n387 9 # ASSIGN : n388 7 # ASSIGN : n389 8 # ASSIGN : n390 5 # ASSIGN : n391 8 # ASSIGN : n392 12 # ASSIGN : n393 5 # ASSIGN : n394 12 # ASSIGN : n395 9 # ASSIGN : n396 8 # ASSIGN : n397 2 # ASSIGN : n398 1 # ASSIGN : n399 3 # ASSIGN : n400 4 # ASSIGN : n401 12 # ASSIGN : n402 8 # ASSIGN : n403 11 # ASSIGN : n404 11 # ASSIGN : n405 10 # ASSIGN : n406 11 # ASSIGN : n407 4 # ASSIGN : n408 12 # ASSIGN : n409 9 # ASSIGN : n410 8 # ASSIGN : n411 10 # ASSIGN : n412 6 # ASSIGN : n413 4 # ASSIGN : n414 9 # ASSIGN : n415 9 # ASSIGN : n416 11 # ASSIGN : n417 12 # ASSIGN : n418 6 # ASSIGN : n419 6 # ASSIGN : n420 8 # ASSIGN : n421 2 # ASSIGN : n422 7 # ASSIGN : n423 11 # ASSIGN : n424 11 # ASSIGN : n425 10 # ASSIGN : n426 7 # ASSIGN : n427 6 # ASSIGN : n428 10 # ASSIGN : n429 11 # ASSIGN : n430 4 # ASSIGN : n431 2 # ASSIGN : n432 10 # ASSIGN : n433 12 # ASSIGN : n434 12 # ASSIGN : n435 11 # ASSIGN : n436 1 # ASSIGN : n437 2 # ASSIGN : n438 7 # ASSIGN : n439 7 # ASSIGN : n440 10 # ASSIGN : n441 11 # ASSIGN : n442 9 # ASSIGN : n443 11 # ASSIGN : n444 12 # ASSIGN : n445 8 # ASSIGN : n446 7 # ASSIGN : n447 8 # ASSIGN : n448 8 # ASSIGN : n449 10 # ASSIGN : n450 8 # ASSIGN : n451 3 # ASSIGN : n452 6 # ASSIGN : n453 6 # ASSIGN : n454 11 # ASSIGN : n455 6 # ASSIGN : n456 11 # ASSIGN : n457 2 # ASSIGN : n458 9 # ASSIGN : n459 5 # ASSIGN : n460 10 # ASSIGN : n461 9 # ASSIGN : n462 8 # ASSIGN : n463 2 # ASSIGN : n464 9 # ASSIGN : n465 8 # ASSIGN : n466 10 # ASSIGN : n467 5 # ASSIGN : n468 3 # ASSIGN : n469 10 # ASSIGN : n470 9 # ASSIGN : n471 5 # ASSIGN : n472 8 # ASSIGN : n473 7 # ASSIGN : n474 2 # ASSIGN : n475 12 # ASSIGN : n476 6 # ASSIGN : n477 9 # ASSIGN : n478 7 # ASSIGN : n479 9 # ASSIGN : n480 2 # ASSIGN : n481 9 # ASSIGN : n482 10 # ASSIGN : n483 3 # ASSIGN : n484 7 # ASSIGN : n485 4 # ASSIGN : n486 6 # ASSIGN : n487 10 # ASSIGN : n488 5 # ASSIGN : n489 11 # ASSIGN : n490 6 # ASSIGN : n491 1 # ASSIGN : n492 7 # ASSIGN : n493 8 # ASSIGN : n494 10 # ASSIGN : n495 10 # ASSIGN : n496 4 # ASSIGN : n497 4 # ASSIGN : n498 9 # ASSIGN : n499 3 # ASSIGN : n500 8 SHOW_RESULT 12 END : 12 (0 seconds) [Fri Jul 7 11:16:17 2006] SHOW_RESULT 12 CPU : 0.0499999999999991 = 0.0399999999999991 + 0.01 + 0 + 0 # BOUND : color 9 12 MODIFY_CNF 10 BEGIN : [Fri Jul 7 11:16:17 2006] MODIFY_CNF 10 END : 2342655 bytes (0 seconds) [Fri Jul 7 11:16:17 2006] MODIFY_CNF 10 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 10 BEGIN : [Fri Jul 7 11:16:17 2006] CMD : minisat /tmp/csp2sat5989.cnf /tmp/csp2sat5989.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 87166 261046 | 29055 0 0 nan | 0.000 % | | 100 | 87166 261046 | 31960 100 730 7.3 | 25.645 % | | 250 | 87166 261046 | 35156 250 1748 7.0 | 25.645 % | | 475 | 87166 261046 | 38672 475 3875 8.2 | 25.645 % | | 813 | 87166 261046 | 42539 813 6609 8.1 | 25.645 % | | 1320 | 87166 261046 | 46793 1320 10869 8.2 | 25.645 % | | 2079 | 87166 261046 | 51472 2079 16283 7.8 | 25.645 % | | 3218 | 87166 261046 | 56619 3218 25130 7.8 | 25.645 % | | 4928 | 87166 261046 | 62281 4928 39648 8.0 | 25.645 % | | 7491 | 87166 261046 | 68510 7491 64015 8.5 | 25.645 % | | 11337 | 87166 261046 | 75361 11337 103757 9.2 | 25.645 % | | 17103 | 87166 261046 | 82897 17103 161150 9.4 | 25.645 % | | 25752 | 87167 261046 | 91187 25751 247923 9.6 | 25.645 % | | 38728 | 87094 260830 | 100305 24179 232647 9.6 | 25.670 % | ============================================================================== restarts : 14 conflicts : 48133 (3054 /sec) decisions : 55562 (3526 /sec) propagations : 1845987 (117131 /sec) conflict literals : 455372 (12.18 % deleted) Memory used : 8.23 MB CPU time : 15.76 s UNSATISFIABLE VERIFY_CNF 10 END : (16 seconds) [Fri Jul 7 11:16:33 2006] VERIFY_CNF 10 CPU : 15.82 = 0 + 0 + 15.76 + 0.06 # RESULT : color 10 UNSATISFIABLE # BOUND : color 11 12 MODIFY_CNF 11 BEGIN : [Fri Jul 7 11:16:33 2006] MODIFY_CNF 11 END : 2342655 bytes (0 seconds) [Fri Jul 7 11:16:33 2006] MODIFY_CNF 11 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 11 BEGIN : [Fri Jul 7 11:16:33 2006] CMD : minisat /tmp/csp2sat5989.cnf /tmp/csp2sat5989.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 94276 282376 | 31425 0 0 nan | 0.000 % | | 100 | 94276 282376 | 34567 100 1721 17.2 | 22.438 % | | 250 | 94276 282376 | 38024 250 3127 12.5 | 22.438 % | | 476 | 94276 282376 | 41826 476 5763 12.1 | 22.438 % | | 813 | 94276 282376 | 46009 813 9015 11.1 | 22.438 % | | 1319 | 94276 282376 | 50610 1319 15931 12.1 | 22.438 % | | 2078 | 94276 282376 | 55671 2078 24170 11.6 | 22.438 % | | 3217 | 94276 282376 | 61238 3217 33576 10.4 | 22.438 % | | 4925 | 94276 282376 | 67362 4925 51961 10.6 | 22.438 % | | 7489 | 94276 282376 | 74098 7489 79256 10.6 | 22.438 % | | 11333 | 94276 282376 | 81508 11333 121673 10.7 | 22.438 % | | 17099 | 94276 282376 | 89659 17099 190281 11.1 | 22.438 % | | 25748 | 94276 282376 | 98625 25748 295927 11.5 | 22.438 % | | 38723 | 94276 282376 | 108487 38723 458459 11.8 | 22.438 % | | 58184 | 94276 282376 | 119336 58184 726240 12.5 | 22.438 % | | 87377 | 94276 282376 | 131270 87377 1092956 12.5 | 22.438 % | | 131166 | 94277 282376 | 144397 131165 1632618 12.4 | 22.438 % | | 196851 | 94277 282376 | 158836 65545 804381 12.3 | 22.438 % | | 295378 | 94232 282244 | 174720 104046 1229137 11.8 | 22.451 % | ============================================================================== restarts : 19 conflicts : 415617 (758 /sec) decisions : 495628 (904 /sec) propagations : 24448435 (44617 /sec) conflict literals : 5048201 (11.36 % deleted) Memory used : 20.58 MB CPU time : 547.96 s UNSATISFIABLE VERIFY_CNF 11 END : (548 seconds) [Fri Jul 7 11:25:41 2006] VERIFY_CNF 11 CPU : 548.59 = 0 + 0.01 + 547.96 + 0.62 # RESULT : color 11 UNSATISFIABLE # BOUND : color 12 12 MAIN END : (578 seconds) [Fri Jul 7 11:25:41 2006] MAIN CPU : 577.71 = 11.76 + 0.13 + 565.08 + 0.74