# TIMEOUT 7200 MAIN BEGIN : [Sat Jul 8 20:09:56 2006] READ BEGIN : csp/le450_5a.csp [Sat Jul 8 20:09:56 2006] READ END : csp/le450_5a.csp (9 seconds) [Sat Jul 8 20:10:05 2006] READ CPU : 8.92 = 8.81 + 0.11 + 0 + 0 # BOUND : color 2 14 GENERATE_CNF 14 BEGIN : [Sat Jul 8 20:10:05 2006] GENERATE_CNF 14 END : 18642 variables 178771 clauses 3366022 bytes (9 seconds) [Sat Jul 8 20:10:14 2006] GENERATE_CNF 14 CPU : 8.37 = 8.33 + 0.04 + 0 + 0 MODIFY_CNF 8 BEGIN : [Sat Jul 8 20:10:14 2006] MODIFY_CNF 8 END : 3366026 bytes (0 seconds) [Sat Jul 8 20:10:14 2006] MODIFY_CNF 8 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 8 BEGIN : [Sat Jul 8 20:10:14 2006] CMD : minisat /tmp/csp2sat4336.cnf /tmp/csp2sat4336.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 107498 325052 | 35832 0 0 nan | 0.000 % | | 101 | 107498 325052 | 39415 101 7681 76.0 | 21.768 % | | 252 | 107498 325052 | 43356 252 23547 93.4 | 21.768 % | | 478 | 107498 325052 | 47692 478 38878 81.3 | 21.768 % | | 815 | 107498 325052 | 52461 815 61019 74.9 | 21.768 % | | 1321 | 107498 325052 | 57707 1321 105023 79.5 | 21.768 % | | 2081 | 107498 325052 | 63478 2081 186718 89.7 | 21.768 % | | 3223 | 107498 325052 | 69826 3223 301118 93.4 | 21.768 % | | 4931 | 107498 325052 | 76809 4931 474180 96.2 | 21.768 % | | 7493 | 107498 325052 | 84489 7493 794848 106.1 | 21.768 % | | 11339 | 107498 325052 | 92938 11339 1143942 100.9 | 21.768 % | | 17107 | 107498 325052 | 102232 17107 2013480 117.7 | 21.768 % | | 25756 | 107498 325052 | 112456 25756 3035644 117.9 | 21.768 % | | 38732 | 107498 325052 | 123701 38732 4632329 119.6 | 21.768 % | | 58193 | 107498 325052 | 136071 58193 7675121 131.9 | 21.768 % | | 87385 | 107498 325052 | 149679 87385 11626282 133.0 | 21.768 % | | 131176 | 107498 325052 | 164647 131176 17454875 133.1 | 21.768 % | | 196860 | 107498 325052 | 181111 38586 4767736 123.6 | 21.768 % | | 295387 | 107498 325052 | 199222 137113 18783531 137.0 | 21.768 % | | 443177 | 107498 325052 | 219145 94954 15702915 165.4 | 21.768 % | | 664860 | 107498 325052 | 241059 107585 19804987 184.1 | 21.768 % | ============================================================================== restarts : 21 conflicts : 723294 (268 /sec) decisions : 871660 (323 /sec) propagations : 973684980 (360469 /sec) conflict literals : 116238450 (8.25 % deleted) Memory used : 179.09 MB CPU time : 2701.16 s SATISFIABLE VERIFY_CNF 8 END : (2704 seconds) [Sat Jul 8 20:55:18 2006] VERIFY_CNF 8 CPU : 2703.53 = 0 + 0 + 2701.17 + 2.36 # RESULT : color 8 SATISFIABLE SHOW_RESULT 8 BEGIN : [Sat Jul 8 20:55:18 2006] # ASSIGN : color 8 # ASSIGN : n1 1 # ASSIGN : n2 1 # ASSIGN : n3 8 # ASSIGN : n4 4 # ASSIGN : n5 5 # ASSIGN : n6 1 # ASSIGN : n7 5 # ASSIGN : n8 3 # ASSIGN : n9 5 # ASSIGN : n10 7 # ASSIGN : n11 5 # ASSIGN : n12 1 # ASSIGN : n13 8 # ASSIGN : n14 4 # ASSIGN : n15 4 # ASSIGN : n16 5 # ASSIGN : n17 1 # ASSIGN : n18 7 # ASSIGN : n19 4 # ASSIGN : n20 4 # ASSIGN : n21 5 # ASSIGN : n22 8 # ASSIGN : n23 2 # ASSIGN : n24 3 # ASSIGN : n25 7 # ASSIGN : n26 1 # ASSIGN : n27 6 # ASSIGN : n28 8 # ASSIGN : n29 7 # ASSIGN : n30 4 # ASSIGN : n31 1 # ASSIGN : n32 7 # ASSIGN : n33 6 # ASSIGN : n34 2 # ASSIGN : n35 5 # ASSIGN : n36 1 # ASSIGN : n37 4 # ASSIGN : n38 4 # ASSIGN : n39 8 # ASSIGN : n40 4 # ASSIGN : n41 6 # ASSIGN : n42 5 # ASSIGN : n43 6 # ASSIGN : n44 2 # ASSIGN : n45 4 # ASSIGN : n46 7 # ASSIGN : n47 7 # ASSIGN : n48 5 # ASSIGN : n49 5 # ASSIGN : n50 2 # ASSIGN : n51 5 # ASSIGN : n52 8 # ASSIGN : n53 3 # ASSIGN : n54 4 # ASSIGN : n55 7 # ASSIGN : n56 6 # ASSIGN : n57 7 # ASSIGN : n58 6 # ASSIGN : n59 3 # ASSIGN : n60 4 # ASSIGN : n61 7 # ASSIGN : n62 3 # ASSIGN : n63 6 # ASSIGN : n64 8 # ASSIGN : n65 5 # ASSIGN : n66 5 # ASSIGN : n67 8 # ASSIGN : n68 7 # ASSIGN : n69 3 # ASSIGN : n70 2 # ASSIGN : n71 8 # ASSIGN : n72 7 # ASSIGN : n73 3 # ASSIGN : n74 3 # ASSIGN : n75 7 # ASSIGN : n76 1 # ASSIGN : n77 1 # ASSIGN : n78 7 # ASSIGN : n79 5 # ASSIGN : n80 6 # ASSIGN : n81 3 # ASSIGN : n82 8 # ASSIGN : n83 7 # ASSIGN : n84 3 # ASSIGN : n85 2 # ASSIGN : n86 7 # ASSIGN : n87 6 # ASSIGN : n88 2 # ASSIGN : n89 2 # ASSIGN : n90 6 # ASSIGN : n91 6 # ASSIGN : n92 6 # ASSIGN : n93 2 # ASSIGN : n94 3 # ASSIGN : n95 2 # ASSIGN : n96 6 # ASSIGN : n97 8 # ASSIGN : n98 5 # ASSIGN : n99 7 # ASSIGN : n100 2 # ASSIGN : n101 1 # ASSIGN : n102 1 # ASSIGN : n103 8 # ASSIGN : n104 2 # ASSIGN : n105 4 # ASSIGN : n106 1 # ASSIGN : n107 3 # ASSIGN : n108 6 # ASSIGN : n109 4 # ASSIGN : n110 4 # ASSIGN : n111 6 # ASSIGN : n112 1 # ASSIGN : n113 7 # ASSIGN : n114 4 # ASSIGN : n115 4 # ASSIGN : n116 1 # ASSIGN : n117 3 # ASSIGN : n118 1 # ASSIGN : n119 4 # ASSIGN : n120 4 # ASSIGN : n121 1 # ASSIGN : n122 5 # ASSIGN : n123 6 # ASSIGN : n124 2 # ASSIGN : n125 6 # ASSIGN : n126 3 # ASSIGN : n127 8 # ASSIGN : n128 7 # ASSIGN : n129 6 # ASSIGN : n130 4 # ASSIGN : n131 6 # ASSIGN : n132 8 # ASSIGN : n133 2 # ASSIGN : n134 5 # ASSIGN : n135 4 # ASSIGN : n136 5 # ASSIGN : n137 7 # ASSIGN : n138 7 # ASSIGN : n139 1 # ASSIGN : n140 2 # ASSIGN : n141 1 # ASSIGN : n142 7 # ASSIGN : n143 1 # ASSIGN : n144 3 # ASSIGN : n145 4 # ASSIGN : n146 1 # ASSIGN : n147 3 # ASSIGN : n148 4 # ASSIGN : n149 2 # ASSIGN : n150 8 # ASSIGN : n151 6 # ASSIGN : n152 6 # ASSIGN : n153 8 # ASSIGN : n154 2 # ASSIGN : n155 4 # ASSIGN : n156 6 # ASSIGN : n157 7 # ASSIGN : n158 8 # ASSIGN : n159 3 # ASSIGN : n160 2 # ASSIGN : n161 5 # ASSIGN : n162 5 # ASSIGN : n163 6 # ASSIGN : n164 7 # ASSIGN : n165 8 # ASSIGN : n166 5 # ASSIGN : n167 1 # ASSIGN : n168 7 # ASSIGN : n169 4 # ASSIGN : n170 3 # ASSIGN : n171 1 # ASSIGN : n172 1 # ASSIGN : n173 8 # ASSIGN : n174 3 # ASSIGN : n175 6 # ASSIGN : n176 1 # ASSIGN : n177 3 # ASSIGN : n178 3 # ASSIGN : n179 2 # ASSIGN : n180 4 # ASSIGN : n181 5 # ASSIGN : n182 7 # ASSIGN : n183 5 # ASSIGN : n184 4 # ASSIGN : n185 2 # ASSIGN : n186 1 # ASSIGN : n187 7 # ASSIGN : n188 5 # ASSIGN : n189 3 # ASSIGN : n190 7 # ASSIGN : n191 3 # ASSIGN : n192 1 # ASSIGN : n193 7 # ASSIGN : n194 8 # ASSIGN : n195 4 # ASSIGN : n196 1 # ASSIGN : n197 1 # ASSIGN : n198 7 # ASSIGN : n199 6 # ASSIGN : n200 4 # ASSIGN : n201 8 # ASSIGN : n202 1 # ASSIGN : n203 3 # ASSIGN : n204 7 # ASSIGN : n205 4 # ASSIGN : n206 5 # ASSIGN : n207 8 # ASSIGN : n208 8 # ASSIGN : n209 4 # ASSIGN : n210 4 # ASSIGN : n211 1 # ASSIGN : n212 6 # ASSIGN : n213 5 # ASSIGN : n214 2 # ASSIGN : n215 2 # ASSIGN : n216 1 # ASSIGN : n217 3 # ASSIGN : n218 6 # ASSIGN : n219 6 # ASSIGN : n220 4 # ASSIGN : n221 1 # ASSIGN : n222 5 # ASSIGN : n223 6 # ASSIGN : n224 4 # ASSIGN : n225 4 # ASSIGN : n226 1 # ASSIGN : n227 1 # ASSIGN : n228 2 # ASSIGN : n229 4 # ASSIGN : n230 8 # ASSIGN : n231 1 # ASSIGN : n232 5 # ASSIGN : n233 6 # ASSIGN : n234 4 # ASSIGN : n235 4 # ASSIGN : n236 8 # ASSIGN : n237 3 # ASSIGN : n238 7 # ASSIGN : n239 6 # ASSIGN : n240 4 # ASSIGN : n241 8 # ASSIGN : n242 8 # ASSIGN : n243 8 # ASSIGN : n244 4 # ASSIGN : n245 7 # ASSIGN : n246 5 # ASSIGN : n247 7 # ASSIGN : n248 7 # ASSIGN : n249 5 # ASSIGN : n250 5 # ASSIGN : n251 5 # ASSIGN : n252 7 # ASSIGN : n253 4 # ASSIGN : n254 7 # ASSIGN : n255 3 # ASSIGN : n256 1 # ASSIGN : n257 1 # ASSIGN : n258 7 # ASSIGN : n259 8 # ASSIGN : n260 3 # ASSIGN : n261 1 # ASSIGN : n262 1 # ASSIGN : n263 4 # ASSIGN : n264 5 # ASSIGN : n265 3 # ASSIGN : n266 7 # ASSIGN : n267 6 # ASSIGN : n268 8 # ASSIGN : n269 2 # ASSIGN : n270 2 # ASSIGN : n271 6 # ASSIGN : n272 7 # ASSIGN : n273 8 # ASSIGN : n274 2 # ASSIGN : n275 2 # ASSIGN : n276 6 # ASSIGN : n277 8 # ASSIGN : n278 6 # ASSIGN : n279 2 # ASSIGN : n280 5 # ASSIGN : n281 1 # ASSIGN : n282 1 # ASSIGN : n283 8 # ASSIGN : n284 5 # ASSIGN : n285 8 # ASSIGN : n286 5 # ASSIGN : n287 1 # ASSIGN : n288 3 # ASSIGN : n289 2 # ASSIGN : n290 4 # ASSIGN : n291 1 # ASSIGN : n292 1 # ASSIGN : n293 7 # ASSIGN : n294 7 # ASSIGN : n295 2 # ASSIGN : n296 5 # ASSIGN : n297 8 # ASSIGN : n298 3 # ASSIGN : n299 4 # ASSIGN : n300 4 # ASSIGN : n301 1 # ASSIGN : n302 8 # ASSIGN : n303 3 # ASSIGN : n304 8 # ASSIGN : n305 8 # ASSIGN : n306 3 # ASSIGN : n307 8 # ASSIGN : n308 7 # ASSIGN : n309 2 # ASSIGN : n310 4 # ASSIGN : n311 7 # ASSIGN : n312 8 # ASSIGN : n313 6 # ASSIGN : n314 2 # ASSIGN : n315 4 # ASSIGN : n316 5 # ASSIGN : n317 1 # ASSIGN : n318 2 # ASSIGN : n319 2 # ASSIGN : n320 3 # ASSIGN : n321 6 # ASSIGN : n322 8 # ASSIGN : n323 2 # ASSIGN : n324 4 # ASSIGN : n325 6 # ASSIGN : n326 1 # ASSIGN : n327 7 # ASSIGN : n328 8 # ASSIGN : n329 3 # ASSIGN : n330 4 # ASSIGN : n331 1 # ASSIGN : n332 5 # ASSIGN : n333 6 # ASSIGN : n334 4 # ASSIGN : n335 7 # ASSIGN : n336 1 # ASSIGN : n337 8 # ASSIGN : n338 8 # ASSIGN : n339 3 # ASSIGN : n340 4 # ASSIGN : n341 1 # ASSIGN : n342 3 # ASSIGN : n343 2 # ASSIGN : n344 6 # ASSIGN : n345 7 # ASSIGN : n346 1 # ASSIGN : n347 1 # ASSIGN : n348 7 # ASSIGN : n349 5 # ASSIGN : n350 6 # ASSIGN : n351 5 # ASSIGN : n352 3 # ASSIGN : n353 3 # ASSIGN : n354 4 # ASSIGN : n355 6 # ASSIGN : n356 5 # ASSIGN : n357 7 # ASSIGN : n358 8 # ASSIGN : n359 5 # ASSIGN : n360 4 # ASSIGN : n361 8 # ASSIGN : n362 6 # ASSIGN : n363 8 # ASSIGN : n364 3 # ASSIGN : n365 2 # ASSIGN : n366 1 # ASSIGN : n367 5 # ASSIGN : n368 5 # ASSIGN : n369 5 # ASSIGN : n370 2 # ASSIGN : n371 1 # ASSIGN : n372 4 # ASSIGN : n373 7 # ASSIGN : n374 2 # ASSIGN : n375 4 # ASSIGN : n376 1 # ASSIGN : n377 1 # ASSIGN : n378 4 # ASSIGN : n379 2 # ASSIGN : n380 4 # ASSIGN : n381 6 # ASSIGN : n382 1 # ASSIGN : n383 5 # ASSIGN : n384 2 # ASSIGN : n385 2 # ASSIGN : n386 8 # ASSIGN : n387 8 # ASSIGN : n388 8 # ASSIGN : n389 7 # ASSIGN : n390 6 # ASSIGN : n391 6 # ASSIGN : n392 8 # ASSIGN : n393 6 # ASSIGN : n394 2 # ASSIGN : n395 2 # ASSIGN : n396 1 # ASSIGN : n397 5 # ASSIGN : n398 6 # ASSIGN : n399 8 # ASSIGN : n400 4 # ASSIGN : n401 1 # ASSIGN : n402 5 # ASSIGN : n403 8 # ASSIGN : n404 2 # ASSIGN : n405 5 # ASSIGN : n406 3 # ASSIGN : n407 1 # ASSIGN : n408 3 # ASSIGN : n409 4 # ASSIGN : n410 2 # ASSIGN : n411 5 # ASSIGN : n412 8 # ASSIGN : n413 3 # ASSIGN : n414 3 # ASSIGN : n415 6 # ASSIGN : n416 1 # ASSIGN : n417 8 # ASSIGN : n418 4 # ASSIGN : n419 3 # ASSIGN : n420 4 # ASSIGN : n421 7 # ASSIGN : n422 5 # ASSIGN : n423 6 # ASSIGN : n424 2 # ASSIGN : n425 3 # ASSIGN : n426 6 # ASSIGN : n427 7 # ASSIGN : n428 3 # ASSIGN : n429 6 # ASSIGN : n430 2 # ASSIGN : n431 6 # ASSIGN : n432 6 # ASSIGN : n433 2 # ASSIGN : n434 4 # ASSIGN : n435 3 # ASSIGN : n436 1 # ASSIGN : n437 1 # ASSIGN : n438 5 # ASSIGN : n439 8 # ASSIGN : n440 3 # ASSIGN : n441 1 # ASSIGN : n442 7 # ASSIGN : n443 8 # ASSIGN : n444 3 # ASSIGN : n445 3 # ASSIGN : n446 3 # ASSIGN : n447 7 # ASSIGN : n448 8 # ASSIGN : n449 2 # ASSIGN : n450 4 SHOW_RESULT 8 END : 8 (0 seconds) [Sat Jul 8 20:55:18 2006] SHOW_RESULT 8 CPU : 0.0399999999999976 = 0.0299999999999976 + 0.01 + 0 + 0 # BOUND : color 2 8 MODIFY_CNF 5 BEGIN : [Sat Jul 8 20:55:18 2006] MODIFY_CNF 5 END : 3366026 bytes (0 seconds) [Sat Jul 8 20:55:18 2006] MODIFY_CNF 5 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 5 BEGIN : [Sat Jul 8 20:55:18 2006] CMD : minisat /tmp/csp2sat4336.cnf /tmp/csp2sat4336.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 73214 222200 | 24404 0 0 nan | 0.000 % | | 102 | 73214 222200 | 26844 102 2107 20.7 | 29.026 % | | 252 | 73214 222200 | 29528 252 5380 21.3 | 29.026 % | | 481 | 73214 222200 | 32481 481 12364 25.7 | 29.026 % | | 818 | 73214 222200 | 35729 818 20632 25.2 | 29.026 % | | 1324 | 73214 222200 | 39302 1324 31477 23.8 | 29.026 % | ============================================================================== restarts : 6 conflicts : 1494 (1176 /sec) decisions : 2034 (1602 /sec) propagations : 1169118 (920565 /sec) conflict literals : 34840 (4.69 % deleted) Memory used : 8.68 MB CPU time : 1.27 s SATISFIABLE VERIFY_CNF 5 END : (1 seconds) [Sat Jul 8 20:55:19 2006] VERIFY_CNF 5 CPU : 1.30999999999998 = 0 + 0 + 1.26999999999998 + 0.04 # RESULT : color 5 SATISFIABLE SHOW_RESULT 5 BEGIN : [Sat Jul 8 20:55:19 2006] # ASSIGN : color 5 # ASSIGN : n1 5 # ASSIGN : n2 1 # ASSIGN : n3 4 # ASSIGN : n4 2 # ASSIGN : n5 3 # ASSIGN : n6 5 # ASSIGN : n7 1 # ASSIGN : n8 4 # ASSIGN : n9 3 # ASSIGN : n10 3 # ASSIGN : n11 5 # ASSIGN : n12 1 # ASSIGN : n13 4 # ASSIGN : n14 3 # ASSIGN : n15 3 # ASSIGN : n16 5 # ASSIGN : n17 1 # ASSIGN : n18 4 # ASSIGN : n19 3 # ASSIGN : n20 3 # ASSIGN : n21 5 # ASSIGN : n22 1 # ASSIGN : n23 4 # ASSIGN : n24 3 # ASSIGN : n25 2 # ASSIGN : n26 5 # ASSIGN : n27 1 # ASSIGN : n28 4 # ASSIGN : n29 3 # ASSIGN : n30 3 # ASSIGN : n31 5 # ASSIGN : n32 1 # ASSIGN : n33 4 # ASSIGN : n34 3 # ASSIGN : n35 3 # ASSIGN : n36 5 # ASSIGN : n37 1 # ASSIGN : n38 4 # ASSIGN : n39 3 # ASSIGN : n40 2 # ASSIGN : n41 5 # ASSIGN : n42 1 # ASSIGN : n43 4 # ASSIGN : n44 3 # ASSIGN : n45 3 # ASSIGN : n46 5 # ASSIGN : n47 1 # ASSIGN : n48 4 # ASSIGN : n49 2 # ASSIGN : n50 2 # ASSIGN : n51 5 # ASSIGN : n52 1 # ASSIGN : n53 4 # ASSIGN : n54 2 # ASSIGN : n55 3 # ASSIGN : n56 5 # ASSIGN : n57 1 # ASSIGN : n58 4 # ASSIGN : n59 2 # ASSIGN : n60 3 # ASSIGN : n61 5 # ASSIGN : n62 1 # ASSIGN : n63 4 # ASSIGN : n64 2 # ASSIGN : n65 2 # ASSIGN : n66 5 # ASSIGN : n67 1 # ASSIGN : n68 4 # ASSIGN : n69 2 # ASSIGN : n70 3 # ASSIGN : n71 5 # ASSIGN : n72 1 # ASSIGN : n73 4 # ASSIGN : n74 2 # ASSIGN : n75 2 # ASSIGN : n76 5 # ASSIGN : n77 1 # ASSIGN : n78 4 # ASSIGN : n79 2 # ASSIGN : n80 3 # ASSIGN : n81 5 # ASSIGN : n82 1 # ASSIGN : n83 4 # ASSIGN : n84 2 # ASSIGN : n85 3 # ASSIGN : n86 5 # ASSIGN : n87 1 # ASSIGN : n88 4 # ASSIGN : n89 2 # ASSIGN : n90 2 # ASSIGN : n91 5 # ASSIGN : n92 1 # ASSIGN : n93 4 # ASSIGN : n94 2 # ASSIGN : n95 3 # ASSIGN : n96 5 # ASSIGN : n97 1 # ASSIGN : n98 4 # ASSIGN : n99 2 # ASSIGN : n100 3 # ASSIGN : n101 5 # ASSIGN : n102 1 # ASSIGN : n103 4 # ASSIGN : n104 2 # ASSIGN : n105 3 # ASSIGN : n106 5 # ASSIGN : n107 1 # ASSIGN : n108 4 # ASSIGN : n109 2 # ASSIGN : n110 3 # ASSIGN : n111 5 # ASSIGN : n112 1 # ASSIGN : n113 4 # ASSIGN : n114 2 # ASSIGN : n115 2 # ASSIGN : n116 5 # ASSIGN : n117 1 # ASSIGN : n118 4 # ASSIGN : n119 2 # ASSIGN : n120 3 # ASSIGN : n121 5 # ASSIGN : n122 1 # ASSIGN : n123 4 # ASSIGN : n124 3 # ASSIGN : n125 3 # ASSIGN : n126 5 # ASSIGN : n127 1 # ASSIGN : n128 4 # ASSIGN : n129 3 # ASSIGN : n130 2 # ASSIGN : n131 5 # ASSIGN : n132 1 # ASSIGN : n133 4 # ASSIGN : n134 3 # ASSIGN : n135 3 # ASSIGN : n136 5 # ASSIGN : n137 1 # ASSIGN : n138 4 # ASSIGN : n139 3 # ASSIGN : n140 2 # ASSIGN : n141 5 # ASSIGN : n142 1 # ASSIGN : n143 4 # ASSIGN : n144 3 # ASSIGN : n145 3 # ASSIGN : n146 5 # ASSIGN : n147 1 # ASSIGN : n148 4 # ASSIGN : n149 3 # ASSIGN : n150 3 # ASSIGN : n151 5 # ASSIGN : n152 1 # ASSIGN : n153 4 # ASSIGN : n154 3 # ASSIGN : n155 2 # ASSIGN : n156 5 # ASSIGN : n157 1 # ASSIGN : n158 4 # ASSIGN : n159 2 # ASSIGN : n160 3 # ASSIGN : n161 5 # ASSIGN : n162 1 # ASSIGN : n163 4 # ASSIGN : n164 2 # ASSIGN : n165 2 # ASSIGN : n166 5 # ASSIGN : n167 1 # ASSIGN : n168 4 # ASSIGN : n169 2 # ASSIGN : n170 3 # ASSIGN : n171 5 # ASSIGN : n172 1 # ASSIGN : n173 4 # ASSIGN : n174 2 # ASSIGN : n175 3 # ASSIGN : n176 5 # ASSIGN : n177 1 # ASSIGN : n178 4 # ASSIGN : n179 2 # ASSIGN : n180 2 # ASSIGN : n181 5 # ASSIGN : n182 1 # ASSIGN : n183 4 # ASSIGN : n184 2 # ASSIGN : n185 3 # ASSIGN : n186 5 # ASSIGN : n187 1 # ASSIGN : n188 4 # ASSIGN : n189 2 # ASSIGN : n190 3 # ASSIGN : n191 5 # ASSIGN : n192 1 # ASSIGN : n193 4 # ASSIGN : n194 2 # ASSIGN : n195 3 # ASSIGN : n196 5 # ASSIGN : n197 1 # ASSIGN : n198 4 # ASSIGN : n199 2 # ASSIGN : n200 3 # ASSIGN : n201 5 # ASSIGN : n202 1 # ASSIGN : n203 4 # ASSIGN : n204 2 # ASSIGN : n205 2 # ASSIGN : n206 5 # ASSIGN : n207 1 # ASSIGN : n208 4 # ASSIGN : n209 2 # ASSIGN : n210 3 # ASSIGN : n211 5 # ASSIGN : n212 1 # ASSIGN : n213 4 # ASSIGN : n214 2 # ASSIGN : n215 3 # ASSIGN : n216 5 # ASSIGN : n217 1 # ASSIGN : n218 4 # ASSIGN : n219 2 # ASSIGN : n220 2 # ASSIGN : n221 5 # ASSIGN : n222 1 # ASSIGN : n223 4 # ASSIGN : n224 2 # ASSIGN : n225 3 # ASSIGN : n226 5 # ASSIGN : n227 1 # ASSIGN : n228 4 # ASSIGN : n229 2 # ASSIGN : n230 2 # ASSIGN : n231 5 # ASSIGN : n232 1 # ASSIGN : n233 4 # ASSIGN : n234 3 # ASSIGN : n235 3 # ASSIGN : n236 5 # ASSIGN : n237 1 # ASSIGN : n238 4 # ASSIGN : n239 3 # ASSIGN : n240 3 # ASSIGN : n241 5 # ASSIGN : n242 1 # ASSIGN : n243 4 # ASSIGN : n244 3 # ASSIGN : n245 2 # ASSIGN : n246 5 # ASSIGN : n247 1 # ASSIGN : n248 4 # ASSIGN : n249 3 # ASSIGN : n250 3 # ASSIGN : n251 5 # ASSIGN : n252 1 # ASSIGN : n253 4 # ASSIGN : n254 3 # ASSIGN : n255 2 # ASSIGN : n256 5 # ASSIGN : n257 1 # ASSIGN : n258 4 # ASSIGN : n259 3 # ASSIGN : n260 3 # ASSIGN : n261 5 # ASSIGN : n262 1 # ASSIGN : n263 4 # ASSIGN : n264 3 # ASSIGN : n265 3 # ASSIGN : n266 5 # ASSIGN : n267 1 # ASSIGN : n268 4 # ASSIGN : n269 3 # ASSIGN : n270 2 # ASSIGN : n271 5 # ASSIGN : n272 1 # ASSIGN : n273 4 # ASSIGN : n274 2 # ASSIGN : n275 3 # ASSIGN : n276 5 # ASSIGN : n277 1 # ASSIGN : n278 4 # ASSIGN : n279 2 # ASSIGN : n280 3 # ASSIGN : n281 5 # ASSIGN : n282 1 # ASSIGN : n283 4 # ASSIGN : n284 2 # ASSIGN : n285 3 # ASSIGN : n286 5 # ASSIGN : n287 1 # ASSIGN : n288 4 # ASSIGN : n289 2 # ASSIGN : n290 3 # ASSIGN : n291 5 # ASSIGN : n292 1 # ASSIGN : n293 4 # ASSIGN : n294 2 # ASSIGN : n295 2 # ASSIGN : n296 5 # ASSIGN : n297 1 # ASSIGN : n298 4 # ASSIGN : n299 2 # ASSIGN : n300 3 # ASSIGN : n301 5 # ASSIGN : n302 1 # ASSIGN : n303 4 # ASSIGN : n304 2 # ASSIGN : n305 3 # ASSIGN : n306 5 # ASSIGN : n307 1 # ASSIGN : n308 4 # ASSIGN : n309 2 # ASSIGN : n310 2 # ASSIGN : n311 5 # ASSIGN : n312 1 # ASSIGN : n313 4 # ASSIGN : n314 2 # ASSIGN : n315 3 # ASSIGN : n316 5 # ASSIGN : n317 1 # ASSIGN : n318 4 # ASSIGN : n319 2 # ASSIGN : n320 2 # ASSIGN : n321 5 # ASSIGN : n322 1 # ASSIGN : n323 4 # ASSIGN : n324 2 # ASSIGN : n325 3 # ASSIGN : n326 5 # ASSIGN : n327 1 # ASSIGN : n328 4 # ASSIGN : n329 2 # ASSIGN : n330 3 # ASSIGN : n331 5 # ASSIGN : n332 1 # ASSIGN : n333 4 # ASSIGN : n334 2 # ASSIGN : n335 2 # ASSIGN : n336 5 # ASSIGN : n337 1 # ASSIGN : n338 4 # ASSIGN : n339 2 # ASSIGN : n340 3 # ASSIGN : n341 5 # ASSIGN : n342 1 # ASSIGN : n343 4 # ASSIGN : n344 2 # ASSIGN : n345 2 # ASSIGN : n346 5 # ASSIGN : n347 1 # ASSIGN : n348 4 # ASSIGN : n349 3 # ASSIGN : n350 3 # ASSIGN : n351 5 # ASSIGN : n352 1 # ASSIGN : n353 4 # ASSIGN : n354 3 # ASSIGN : n355 3 # ASSIGN : n356 5 # ASSIGN : n357 1 # ASSIGN : n358 4 # ASSIGN : n359 3 # ASSIGN : n360 2 # ASSIGN : n361 5 # ASSIGN : n362 1 # ASSIGN : n363 4 # ASSIGN : n364 3 # ASSIGN : n365 3 # ASSIGN : n366 5 # ASSIGN : n367 1 # ASSIGN : n368 4 # ASSIGN : n369 3 # ASSIGN : n370 3 # ASSIGN : n371 5 # ASSIGN : n372 1 # ASSIGN : n373 4 # ASSIGN : n374 3 # ASSIGN : n375 3 # ASSIGN : n376 5 # ASSIGN : n377 1 # ASSIGN : n378 4 # ASSIGN : n379 3 # ASSIGN : n380 3 # ASSIGN : n381 5 # ASSIGN : n382 1 # ASSIGN : n383 4 # ASSIGN : n384 2 # ASSIGN : n385 2 # ASSIGN : n386 5 # ASSIGN : n387 1 # ASSIGN : n388 4 # ASSIGN : n389 2 # ASSIGN : n390 3 # ASSIGN : n391 5 # ASSIGN : n392 1 # ASSIGN : n393 4 # ASSIGN : n394 2 # ASSIGN : n395 3 # ASSIGN : n396 5 # ASSIGN : n397 1 # ASSIGN : n398 4 # ASSIGN : n399 2 # ASSIGN : n400 2 # ASSIGN : n401 5 # ASSIGN : n402 1 # ASSIGN : n403 4 # ASSIGN : n404 2 # ASSIGN : n405 3 # ASSIGN : n406 5 # ASSIGN : n407 1 # ASSIGN : n408 4 # ASSIGN : n409 2 # ASSIGN : n410 2 # ASSIGN : n411 5 # ASSIGN : n412 1 # ASSIGN : n413 4 # ASSIGN : n414 2 # ASSIGN : n415 3 # ASSIGN : n416 5 # ASSIGN : n417 1 # ASSIGN : n418 4 # ASSIGN : n419 2 # ASSIGN : n420 3 # ASSIGN : n421 5 # ASSIGN : n422 1 # ASSIGN : n423 4 # ASSIGN : n424 2 # ASSIGN : n425 2 # ASSIGN : n426 5 # ASSIGN : n427 1 # ASSIGN : n428 4 # ASSIGN : n429 2 # ASSIGN : n430 3 # ASSIGN : n431 5 # ASSIGN : n432 1 # ASSIGN : n433 4 # ASSIGN : n434 2 # ASSIGN : n435 2 # ASSIGN : n436 5 # ASSIGN : n437 1 # ASSIGN : n438 4 # ASSIGN : n439 2 # ASSIGN : n440 3 # ASSIGN : n441 5 # ASSIGN : n442 1 # ASSIGN : n443 4 # ASSIGN : n444 2 # ASSIGN : n445 3 # ASSIGN : n446 5 # ASSIGN : n447 1 # ASSIGN : n448 4 # ASSIGN : n449 2 # ASSIGN : n450 2 SHOW_RESULT 5 END : 5 (0 seconds) [Sat Jul 8 20:55:19 2006] SHOW_RESULT 5 CPU : 0.0300000000000011 = 0.0300000000000011 + 0 + 0 + 0 # BOUND : color 2 5 MODIFY_CNF 3 BEGIN : [Sat Jul 8 20:55:19 2006] MODIFY_CNF 3 END : 3366026 bytes (0 seconds) [Sat Jul 8 20:55:19 2006] MODIFY_CNF 3 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 3 BEGIN : [Sat Jul 8 20:55:19 2006] CMD : minisat /tmp/csp2sat4336.cnf /tmp/csp2sat4336.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 50358 153632 | 16786 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 8 (32 /sec) decisions : 7 (28 /sec) propagations : 7896 (31584 /sec) conflict literals : 14 (6.67 % deleted) Memory used : 8.50 MB CPU time : 0.25 s UNSATISFIABLE VERIFY_CNF 3 END : (0 seconds) [Sat Jul 8 20:55:19 2006] VERIFY_CNF 3 CPU : 0.270000000000002 = 0.0100000000000016 + 0 + 0.25 + 0.0100000000000002 # RESULT : color 3 UNSATISFIABLE # BOUND : color 4 5 MODIFY_CNF 4 BEGIN : [Sat Jul 8 20:55:19 2006] MODIFY_CNF 4 END : 3366026 bytes (0 seconds) [Sat Jul 8 20:55:19 2006] MODIFY_CNF 4 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 4 BEGIN : [Sat Jul 8 20:55:19 2006] CMD : minisat /tmp/csp2sat4336.cnf /tmp/csp2sat4336.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 61786 187916 | 20595 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 66 (264 /sec) decisions : 84 (336 /sec) propagations : 13039 (52156 /sec) conflict literals : 209 (16.73 % deleted) Memory used : 8.50 MB CPU time : 0.25 s UNSATISFIABLE VERIFY_CNF 4 END : (1 seconds) [Sat Jul 8 20:55:20 2006] VERIFY_CNF 4 CPU : 0.27 = 0 + 0.01 + 0.25 + 0.00999999999999979 # RESULT : color 4 UNSATISFIABLE # BOUND : color 5 5 MAIN END : (2724 seconds) [Sat Jul 8 20:55:20 2006] MAIN CPU : 2722.77 = 17.24 + 0.17 + 2702.94 + 2.42