# TIMEOUT 7200 MAIN BEGIN : [Sat Jul 8 21:42:32 2006] READ BEGIN : csp/le450_5c.csp [Sat Jul 8 21:42:32 2006] READ END : csp/le450_5c.csp (14 seconds) [Sat Jul 8 21:42:46 2006] READ CPU : 14.62 = 14.45 + 0.17 + 0 + 0 # BOUND : color 2 17 GENERATE_CNF 17 BEGIN : [Sat Jul 8 21:42:46 2006] GENERATE_CNF 17 END : 28173 variables 358873 clauses 6909571 bytes (18 seconds) [Sat Jul 8 21:43:04 2006] GENERATE_CNF 17 CPU : 16.69 = 16.65 + 0.04 + 0 + 0 MODIFY_CNF 9 BEGIN : [Sat Jul 8 21:43:04 2006] MODIFY_CNF 9 END : 6909575 bytes (0 seconds) [Sat Jul 8 21:43:04 2006] MODIFY_CNF 9 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 9 BEGIN : [Sat Jul 8 21:43:04 2006] CMD : minisat /tmp/csp2sat5785.cnf /tmp/csp2sat5785.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 199320 603254 | 66440 0 0 nan | 0.000 % | | 100 | 199320 603254 | 73084 100 7099 71.0 | 17.606 % | ============================================================================== restarts : 2 conflicts : 122 (152 /sec) decisions : 711 (889 /sec) propagations : 291248 (364060 /sec) conflict literals : 8830 (2.71 % deleted) Memory used : 15.41 MB CPU time : 0.8 s SATISFIABLE VERIFY_CNF 9 END : (1 seconds) [Sat Jul 8 21:43:05 2006] VERIFY_CNF 9 CPU : 0.87 = 0 + 0.01 + 0.81 + 0.05 # RESULT : color 9 SATISFIABLE SHOW_RESULT 9 BEGIN : [Sat Jul 8 21:43:05 2006] # ASSIGN : color 9 # ASSIGN : n1 5 # ASSIGN : n2 7 # ASSIGN : n3 8 # ASSIGN : n4 6 # ASSIGN : n5 5 # ASSIGN : n6 5 # ASSIGN : n7 8 # ASSIGN : n8 8 # ASSIGN : n9 6 # ASSIGN : n10 3 # ASSIGN : n11 5 # ASSIGN : n12 2 # ASSIGN : n13 4 # ASSIGN : n14 6 # ASSIGN : n15 3 # ASSIGN : n16 9 # ASSIGN : n17 4 # ASSIGN : n18 8 # ASSIGN : n19 6 # ASSIGN : n20 3 # ASSIGN : n21 5 # ASSIGN : n22 7 # ASSIGN : n23 4 # ASSIGN : n24 6 # ASSIGN : n25 9 # ASSIGN : n26 3 # ASSIGN : n27 8 # ASSIGN : n28 1 # ASSIGN : n29 6 # ASSIGN : n30 9 # ASSIGN : n31 3 # ASSIGN : n32 1 # ASSIGN : n33 8 # ASSIGN : n34 6 # ASSIGN : n35 6 # ASSIGN : n36 2 # ASSIGN : n37 1 # ASSIGN : n38 8 # ASSIGN : n39 6 # ASSIGN : n40 9 # ASSIGN : n41 9 # ASSIGN : n42 9 # ASSIGN : n43 8 # ASSIGN : n44 6 # ASSIGN : n45 3 # ASSIGN : n46 7 # ASSIGN : n47 2 # ASSIGN : n48 1 # ASSIGN : n49 6 # ASSIGN : n50 3 # ASSIGN : n51 3 # ASSIGN : n52 4 # ASSIGN : n53 8 # ASSIGN : n54 6 # ASSIGN : n55 3 # ASSIGN : n56 7 # ASSIGN : n57 7 # ASSIGN : n58 1 # ASSIGN : n59 6 # ASSIGN : n60 6 # ASSIGN : n61 5 # ASSIGN : n62 7 # ASSIGN : n63 8 # ASSIGN : n64 6 # ASSIGN : n65 3 # ASSIGN : n66 3 # ASSIGN : n67 4 # ASSIGN : n68 8 # ASSIGN : n69 6 # ASSIGN : n70 3 # ASSIGN : n71 5 # ASSIGN : n72 7 # ASSIGN : n73 4 # ASSIGN : n74 6 # ASSIGN : n75 9 # ASSIGN : n76 7 # ASSIGN : n77 7 # ASSIGN : n78 8 # ASSIGN : n79 6 # ASSIGN : n80 3 # ASSIGN : n81 7 # ASSIGN : n82 7 # ASSIGN : n83 8 # ASSIGN : n84 6 # ASSIGN : n85 2 # ASSIGN : n86 2 # ASSIGN : n87 7 # ASSIGN : n88 2 # ASSIGN : n89 6 # ASSIGN : n90 1 # ASSIGN : n91 5 # ASSIGN : n92 7 # ASSIGN : n93 7 # ASSIGN : n94 6 # ASSIGN : n95 2 # ASSIGN : n96 1 # ASSIGN : n97 7 # ASSIGN : n98 8 # ASSIGN : n99 6 # ASSIGN : n100 1 # ASSIGN : n101 4 # ASSIGN : n102 8 # ASSIGN : n103 4 # ASSIGN : n104 9 # ASSIGN : n105 3 # ASSIGN : n106 2 # ASSIGN : n107 1 # ASSIGN : n108 8 # ASSIGN : n109 3 # ASSIGN : n110 9 # ASSIGN : n111 5 # ASSIGN : n112 7 # ASSIGN : n113 8 # ASSIGN : n114 9 # ASSIGN : n115 5 # ASSIGN : n116 3 # ASSIGN : n117 2 # ASSIGN : n118 4 # ASSIGN : n119 6 # ASSIGN : n120 5 # ASSIGN : n121 5 # ASSIGN : n122 7 # ASSIGN : n123 8 # ASSIGN : n124 6 # ASSIGN : n125 6 # ASSIGN : n126 5 # ASSIGN : n127 4 # ASSIGN : n128 8 # ASSIGN : n129 6 # ASSIGN : n130 3 # ASSIGN : n131 3 # ASSIGN : n132 4 # ASSIGN : n133 8 # ASSIGN : n134 6 # ASSIGN : n135 9 # ASSIGN : n136 5 # ASSIGN : n137 2 # ASSIGN : n138 4 # ASSIGN : n139 6 # ASSIGN : n140 9 # ASSIGN : n141 3 # ASSIGN : n142 2 # ASSIGN : n143 1 # ASSIGN : n144 6 # ASSIGN : n145 2 # ASSIGN : n146 4 # ASSIGN : n147 2 # ASSIGN : n148 1 # ASSIGN : n149 6 # ASSIGN : n150 6 # ASSIGN : n151 5 # ASSIGN : n152 1 # ASSIGN : n153 8 # ASSIGN : n154 6 # ASSIGN : n155 9 # ASSIGN : n156 1 # ASSIGN : n157 5 # ASSIGN : n158 8 # ASSIGN : n159 6 # ASSIGN : n160 3 # ASSIGN : n161 1 # ASSIGN : n162 7 # ASSIGN : n163 4 # ASSIGN : n164 6 # ASSIGN : n165 9 # ASSIGN : n166 9 # ASSIGN : n167 7 # ASSIGN : n168 5 # ASSIGN : n169 6 # ASSIGN : n170 3 # ASSIGN : n171 7 # ASSIGN : n172 4 # ASSIGN : n173 8 # ASSIGN : n174 6 # ASSIGN : n175 5 # ASSIGN : n176 7 # ASSIGN : n177 8 # ASSIGN : n178 2 # ASSIGN : n179 6 # ASSIGN : n180 9 # ASSIGN : n181 2 # ASSIGN : n182 4 # ASSIGN : n183 8 # ASSIGN : n184 6 # ASSIGN : n185 3 # ASSIGN : n186 2 # ASSIGN : n187 2 # ASSIGN : n188 8 # ASSIGN : n189 6 # ASSIGN : n190 3 # ASSIGN : n191 7 # ASSIGN : n192 2 # ASSIGN : n193 4 # ASSIGN : n194 6 # ASSIGN : n195 3 # ASSIGN : n196 2 # ASSIGN : n197 1 # ASSIGN : n198 1 # ASSIGN : n199 2 # ASSIGN : n200 3 # ASSIGN : n201 7 # ASSIGN : n202 2 # ASSIGN : n203 1 # ASSIGN : n204 6 # ASSIGN : n205 9 # ASSIGN : n206 3 # ASSIGN : n207 2 # ASSIGN : n208 1 # ASSIGN : n209 6 # ASSIGN : n210 9 # ASSIGN : n211 3 # ASSIGN : n212 7 # ASSIGN : n213 8 # ASSIGN : n214 3 # ASSIGN : n215 6 # ASSIGN : n216 5 # ASSIGN : n217 1 # ASSIGN : n218 8 # ASSIGN : n219 3 # ASSIGN : n220 3 # ASSIGN : n221 3 # ASSIGN : n222 1 # ASSIGN : n223 4 # ASSIGN : n224 9 # ASSIGN : n225 5 # ASSIGN : n226 1 # ASSIGN : n227 4 # ASSIGN : n228 1 # ASSIGN : n229 6 # ASSIGN : n230 5 # ASSIGN : n231 3 # ASSIGN : n232 8 # ASSIGN : n233 8 # ASSIGN : n234 6 # ASSIGN : n235 5 # ASSIGN : n236 3 # ASSIGN : n237 7 # ASSIGN : n238 1 # ASSIGN : n239 6 # ASSIGN : n240 6 # ASSIGN : n241 5 # ASSIGN : n242 7 # ASSIGN : n243 4 # ASSIGN : n244 6 # ASSIGN : n245 5 # ASSIGN : n246 8 # ASSIGN : n247 5 # ASSIGN : n248 8 # ASSIGN : n249 6 # ASSIGN : n250 9 # ASSIGN : n251 5 # ASSIGN : n252 7 # ASSIGN : n253 4 # ASSIGN : n254 6 # ASSIGN : n255 4 # ASSIGN : n256 9 # ASSIGN : n257 5 # ASSIGN : n258 8 # ASSIGN : n259 6 # ASSIGN : n260 9 # ASSIGN : n261 2 # ASSIGN : n262 4 # ASSIGN : n263 8 # ASSIGN : n264 6 # ASSIGN : n265 9 # ASSIGN : n266 9 # ASSIGN : n267 2 # ASSIGN : n268 4 # ASSIGN : n269 6 # ASSIGN : n270 9 # ASSIGN : n271 5 # ASSIGN : n272 7 # ASSIGN : n273 8 # ASSIGN : n274 6 # ASSIGN : n275 9 # ASSIGN : n276 2 # ASSIGN : n277 7 # ASSIGN : n278 8 # ASSIGN : n279 6 # ASSIGN : n280 3 # ASSIGN : n281 5 # ASSIGN : n282 4 # ASSIGN : n283 4 # ASSIGN : n284 6 # ASSIGN : n285 3 # ASSIGN : n286 7 # ASSIGN : n287 4 # ASSIGN : n288 8 # ASSIGN : n289 6 # ASSIGN : n290 3 # ASSIGN : n291 5 # ASSIGN : n292 7 # ASSIGN : n293 8 # ASSIGN : n294 6 # ASSIGN : n295 9 # ASSIGN : n296 3 # ASSIGN : n297 4 # ASSIGN : n298 4 # ASSIGN : n299 6 # ASSIGN : n300 9 # ASSIGN : n301 7 # ASSIGN : n302 7 # ASSIGN : n303 1 # ASSIGN : n304 6 # ASSIGN : n305 6 # ASSIGN : n306 5 # ASSIGN : n307 1 # ASSIGN : n308 8 # ASSIGN : n309 6 # ASSIGN : n310 3 # ASSIGN : n311 3 # ASSIGN : n312 8 # ASSIGN : n313 4 # ASSIGN : n314 6 # ASSIGN : n315 5 # ASSIGN : n316 2 # ASSIGN : n317 2 # ASSIGN : n318 1 # ASSIGN : n319 6 # ASSIGN : n320 9 # ASSIGN : n321 3 # ASSIGN : n322 2 # ASSIGN : n323 1 # ASSIGN : n324 6 # ASSIGN : n325 5 # ASSIGN : n326 3 # ASSIGN : n327 8 # ASSIGN : n328 1 # ASSIGN : n329 9 # ASSIGN : n330 6 # ASSIGN : n331 5 # ASSIGN : n332 7 # ASSIGN : n333 8 # ASSIGN : n334 9 # ASSIGN : n335 9 # ASSIGN : n336 3 # ASSIGN : n337 5 # ASSIGN : n338 8 # ASSIGN : n339 9 # ASSIGN : n340 9 # ASSIGN : n341 5 # ASSIGN : n342 7 # ASSIGN : n343 4 # ASSIGN : n344 6 # ASSIGN : n345 5 # ASSIGN : n346 9 # ASSIGN : n347 8 # ASSIGN : n348 8 # ASSIGN : n349 6 # ASSIGN : n350 5 # ASSIGN : n351 7 # ASSIGN : n352 7 # ASSIGN : n353 8 # ASSIGN : n354 6 # ASSIGN : n355 5 # ASSIGN : n356 4 # ASSIGN : n357 7 # ASSIGN : n358 4 # ASSIGN : n359 6 # ASSIGN : n360 5 # ASSIGN : n361 5 # ASSIGN : n362 7 # ASSIGN : n363 7 # ASSIGN : n364 6 # ASSIGN : n365 9 # ASSIGN : n366 5 # ASSIGN : n367 2 # ASSIGN : n368 1 # ASSIGN : n369 6 # ASSIGN : n370 2 # ASSIGN : n371 5 # ASSIGN : n372 4 # ASSIGN : n373 4 # ASSIGN : n374 6 # ASSIGN : n375 9 # ASSIGN : n376 7 # ASSIGN : n377 4 # ASSIGN : n378 8 # ASSIGN : n379 6 # ASSIGN : n380 9 # ASSIGN : n381 7 # ASSIGN : n382 7 # ASSIGN : n383 8 # ASSIGN : n384 6 # ASSIGN : n385 9 # ASSIGN : n386 3 # ASSIGN : n387 2 # ASSIGN : n388 4 # ASSIGN : n389 6 # ASSIGN : n390 9 # ASSIGN : n391 3 # ASSIGN : n392 4 # ASSIGN : n393 8 # ASSIGN : n394 6 # ASSIGN : n395 6 # ASSIGN : n396 7 # ASSIGN : n397 1 # ASSIGN : n398 8 # ASSIGN : n399 9 # ASSIGN : n400 5 # ASSIGN : n401 7 # ASSIGN : n402 8 # ASSIGN : n403 4 # ASSIGN : n404 6 # ASSIGN : n405 3 # ASSIGN : n406 5 # ASSIGN : n407 4 # ASSIGN : n408 4 # ASSIGN : n409 1 # ASSIGN : n410 3 # ASSIGN : n411 3 # ASSIGN : n412 4 # ASSIGN : n413 8 # ASSIGN : n414 6 # ASSIGN : n415 3 # ASSIGN : n416 7 # ASSIGN : n417 7 # ASSIGN : n418 1 # ASSIGN : n419 6 # ASSIGN : n420 6 # ASSIGN : n421 5 # ASSIGN : n422 7 # ASSIGN : n423 8 # ASSIGN : n424 6 # ASSIGN : n425 4 # ASSIGN : n426 7 # ASSIGN : n427 8 # ASSIGN : n428 7 # ASSIGN : n429 6 # ASSIGN : n430 9 # ASSIGN : n431 5 # ASSIGN : n432 7 # ASSIGN : n433 8 # ASSIGN : n434 6 # ASSIGN : n435 9 # ASSIGN : n436 9 # ASSIGN : n437 7 # ASSIGN : n438 8 # ASSIGN : n439 8 # ASSIGN : n440 9 # ASSIGN : n441 9 # ASSIGN : n442 7 # ASSIGN : n443 8 # ASSIGN : n444 9 # ASSIGN : n445 9 # ASSIGN : n446 9 # ASSIGN : n447 7 # ASSIGN : n448 4 # ASSIGN : n449 1 # ASSIGN : n450 9 SHOW_RESULT 9 END : 9 (0 seconds) [Sat Jul 8 21:43:05 2006] SHOW_RESULT 9 CPU : 0.0400000000000027 = 0.0400000000000027 + 0 + 0 + 0 # BOUND : color 2 9 MODIFY_CNF 5 BEGIN : [Sat Jul 8 21:43:05 2006] MODIFY_CNF 5 END : 6909575 bytes (0 seconds) [Sat Jul 8 21:43:05 2006] MODIFY_CNF 5 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 5 BEGIN : [Sat Jul 8 21:43:05 2006] CMD : minisat /tmp/csp2sat5785.cnf /tmp/csp2sat5785.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 120896 367982 | 40298 0 0 nan | 0.000 % | | 100 | 120896 367982 | 44327 100 1255 12.6 | 24.009 % | ============================================================================== restarts : 2 conflicts : 190 (207 /sec) decisions : 257 (279 /sec) propagations : 439470 (477685 /sec) conflict literals : 4356 (4.14 % deleted) Memory used : 15.40 MB CPU time : 0.92 s SATISFIABLE VERIFY_CNF 5 END : (1 seconds) [Sat Jul 8 21:43:06 2006] VERIFY_CNF 5 CPU : 0.99 = 0 + 0 + 0.94 + 0.05 # RESULT : color 5 SATISFIABLE SHOW_RESULT 5 BEGIN : [Sat Jul 8 21:43:06 2006] # ASSIGN : color 5 # ASSIGN : n1 5 # ASSIGN : n2 2 # ASSIGN : n3 1 # ASSIGN : n4 4 # ASSIGN : n5 3 # ASSIGN : n6 5 # ASSIGN : n7 2 # ASSIGN : n8 1 # ASSIGN : n9 4 # ASSIGN : n10 3 # ASSIGN : n11 5 # ASSIGN : n12 2 # ASSIGN : n13 1 # ASSIGN : n14 4 # ASSIGN : n15 3 # ASSIGN : n16 5 # ASSIGN : n17 2 # ASSIGN : n18 1 # ASSIGN : n19 4 # ASSIGN : n20 3 # ASSIGN : n21 5 # ASSIGN : n22 2 # ASSIGN : n23 1 # ASSIGN : n24 4 # ASSIGN : n25 3 # ASSIGN : n26 5 # ASSIGN : n27 2 # ASSIGN : n28 1 # ASSIGN : n29 4 # ASSIGN : n30 3 # ASSIGN : n31 5 # ASSIGN : n32 2 # ASSIGN : n33 1 # ASSIGN : n34 4 # ASSIGN : n35 3 # ASSIGN : n36 5 # ASSIGN : n37 2 # ASSIGN : n38 1 # ASSIGN : n39 4 # ASSIGN : n40 3 # ASSIGN : n41 5 # ASSIGN : n42 2 # ASSIGN : n43 1 # ASSIGN : n44 4 # ASSIGN : n45 3 # ASSIGN : n46 5 # ASSIGN : n47 2 # ASSIGN : n48 1 # ASSIGN : n49 4 # ASSIGN : n50 3 # ASSIGN : n51 5 # ASSIGN : n52 2 # ASSIGN : n53 1 # ASSIGN : n54 4 # ASSIGN : n55 3 # ASSIGN : n56 5 # ASSIGN : n57 2 # ASSIGN : n58 1 # ASSIGN : n59 4 # ASSIGN : n60 3 # ASSIGN : n61 5 # ASSIGN : n62 2 # ASSIGN : n63 1 # ASSIGN : n64 4 # ASSIGN : n65 3 # ASSIGN : n66 5 # ASSIGN : n67 2 # ASSIGN : n68 1 # ASSIGN : n69 4 # ASSIGN : n70 3 # ASSIGN : n71 5 # ASSIGN : n72 2 # ASSIGN : n73 1 # ASSIGN : n74 4 # ASSIGN : n75 3 # ASSIGN : n76 5 # ASSIGN : n77 2 # ASSIGN : n78 1 # ASSIGN : n79 4 # ASSIGN : n80 3 # ASSIGN : n81 5 # ASSIGN : n82 2 # ASSIGN : n83 1 # ASSIGN : n84 4 # ASSIGN : n85 3 # ASSIGN : n86 5 # ASSIGN : n87 2 # ASSIGN : n88 1 # ASSIGN : n89 4 # ASSIGN : n90 3 # ASSIGN : n91 5 # ASSIGN : n92 2 # ASSIGN : n93 1 # ASSIGN : n94 4 # ASSIGN : n95 3 # ASSIGN : n96 5 # ASSIGN : n97 2 # ASSIGN : n98 1 # ASSIGN : n99 4 # ASSIGN : n100 3 # ASSIGN : n101 5 # ASSIGN : n102 2 # ASSIGN : n103 1 # ASSIGN : n104 4 # ASSIGN : n105 3 # ASSIGN : n106 5 # ASSIGN : n107 2 # ASSIGN : n108 1 # ASSIGN : n109 4 # ASSIGN : n110 3 # ASSIGN : n111 5 # ASSIGN : n112 2 # ASSIGN : n113 1 # ASSIGN : n114 4 # ASSIGN : n115 3 # ASSIGN : n116 5 # ASSIGN : n117 2 # ASSIGN : n118 1 # ASSIGN : n119 4 # ASSIGN : n120 3 # ASSIGN : n121 5 # ASSIGN : n122 2 # ASSIGN : n123 1 # ASSIGN : n124 4 # ASSIGN : n125 3 # ASSIGN : n126 5 # ASSIGN : n127 2 # ASSIGN : n128 1 # ASSIGN : n129 4 # ASSIGN : n130 3 # ASSIGN : n131 5 # ASSIGN : n132 2 # ASSIGN : n133 1 # ASSIGN : n134 4 # ASSIGN : n135 3 # ASSIGN : n136 5 # ASSIGN : n137 2 # ASSIGN : n138 1 # ASSIGN : n139 4 # ASSIGN : n140 3 # ASSIGN : n141 5 # ASSIGN : n142 2 # ASSIGN : n143 1 # ASSIGN : n144 4 # ASSIGN : n145 3 # ASSIGN : n146 5 # ASSIGN : n147 2 # ASSIGN : n148 1 # ASSIGN : n149 4 # ASSIGN : n150 3 # ASSIGN : n151 5 # ASSIGN : n152 2 # ASSIGN : n153 1 # ASSIGN : n154 4 # ASSIGN : n155 3 # ASSIGN : n156 5 # ASSIGN : n157 2 # ASSIGN : n158 1 # ASSIGN : n159 4 # ASSIGN : n160 3 # ASSIGN : n161 5 # ASSIGN : n162 2 # ASSIGN : n163 1 # ASSIGN : n164 4 # ASSIGN : n165 3 # ASSIGN : n166 5 # ASSIGN : n167 2 # ASSIGN : n168 1 # ASSIGN : n169 4 # ASSIGN : n170 3 # ASSIGN : n171 5 # ASSIGN : n172 2 # ASSIGN : n173 1 # ASSIGN : n174 4 # ASSIGN : n175 3 # ASSIGN : n176 5 # ASSIGN : n177 2 # ASSIGN : n178 1 # ASSIGN : n179 4 # ASSIGN : n180 3 # ASSIGN : n181 5 # ASSIGN : n182 2 # ASSIGN : n183 1 # ASSIGN : n184 4 # ASSIGN : n185 3 # ASSIGN : n186 5 # ASSIGN : n187 2 # ASSIGN : n188 1 # ASSIGN : n189 4 # ASSIGN : n190 3 # ASSIGN : n191 5 # ASSIGN : n192 2 # ASSIGN : n193 1 # ASSIGN : n194 4 # ASSIGN : n195 3 # ASSIGN : n196 5 # ASSIGN : n197 2 # ASSIGN : n198 1 # ASSIGN : n199 4 # ASSIGN : n200 3 # ASSIGN : n201 5 # ASSIGN : n202 2 # ASSIGN : n203 1 # ASSIGN : n204 4 # ASSIGN : n205 3 # ASSIGN : n206 5 # ASSIGN : n207 2 # ASSIGN : n208 1 # ASSIGN : n209 4 # ASSIGN : n210 3 # ASSIGN : n211 5 # ASSIGN : n212 2 # ASSIGN : n213 1 # ASSIGN : n214 4 # ASSIGN : n215 3 # ASSIGN : n216 5 # ASSIGN : n217 2 # ASSIGN : n218 1 # ASSIGN : n219 4 # ASSIGN : n220 3 # ASSIGN : n221 5 # ASSIGN : n222 2 # ASSIGN : n223 1 # ASSIGN : n224 4 # ASSIGN : n225 3 # ASSIGN : n226 5 # ASSIGN : n227 2 # ASSIGN : n228 1 # ASSIGN : n229 4 # ASSIGN : n230 3 # ASSIGN : n231 5 # ASSIGN : n232 2 # ASSIGN : n233 1 # ASSIGN : n234 4 # ASSIGN : n235 3 # ASSIGN : n236 5 # ASSIGN : n237 2 # ASSIGN : n238 1 # ASSIGN : n239 4 # ASSIGN : n240 3 # ASSIGN : n241 5 # ASSIGN : n242 2 # ASSIGN : n243 1 # ASSIGN : n244 4 # ASSIGN : n245 3 # ASSIGN : n246 5 # ASSIGN : n247 2 # ASSIGN : n248 1 # ASSIGN : n249 4 # ASSIGN : n250 3 # ASSIGN : n251 5 # ASSIGN : n252 2 # ASSIGN : n253 1 # ASSIGN : n254 4 # ASSIGN : n255 3 # ASSIGN : n256 5 # ASSIGN : n257 2 # ASSIGN : n258 1 # ASSIGN : n259 4 # ASSIGN : n260 3 # ASSIGN : n261 5 # ASSIGN : n262 2 # ASSIGN : n263 1 # ASSIGN : n264 4 # ASSIGN : n265 3 # ASSIGN : n266 5 # ASSIGN : n267 2 # ASSIGN : n268 1 # ASSIGN : n269 4 # ASSIGN : n270 3 # ASSIGN : n271 5 # ASSIGN : n272 2 # ASSIGN : n273 1 # ASSIGN : n274 4 # ASSIGN : n275 3 # ASSIGN : n276 5 # ASSIGN : n277 2 # ASSIGN : n278 1 # ASSIGN : n279 4 # ASSIGN : n280 3 # ASSIGN : n281 5 # ASSIGN : n282 2 # ASSIGN : n283 1 # ASSIGN : n284 4 # ASSIGN : n285 3 # ASSIGN : n286 5 # ASSIGN : n287 2 # ASSIGN : n288 1 # ASSIGN : n289 4 # ASSIGN : n290 3 # ASSIGN : n291 5 # ASSIGN : n292 2 # ASSIGN : n293 1 # ASSIGN : n294 4 # ASSIGN : n295 3 # ASSIGN : n296 5 # ASSIGN : n297 2 # ASSIGN : n298 1 # ASSIGN : n299 4 # ASSIGN : n300 3 # ASSIGN : n301 5 # ASSIGN : n302 2 # ASSIGN : n303 1 # ASSIGN : n304 4 # ASSIGN : n305 3 # ASSIGN : n306 5 # ASSIGN : n307 2 # ASSIGN : n308 1 # ASSIGN : n309 4 # ASSIGN : n310 3 # ASSIGN : n311 5 # ASSIGN : n312 2 # ASSIGN : n313 1 # ASSIGN : n314 4 # ASSIGN : n315 3 # ASSIGN : n316 5 # ASSIGN : n317 2 # ASSIGN : n318 1 # ASSIGN : n319 4 # ASSIGN : n320 3 # ASSIGN : n321 5 # ASSIGN : n322 2 # ASSIGN : n323 1 # ASSIGN : n324 4 # ASSIGN : n325 3 # ASSIGN : n326 5 # ASSIGN : n327 2 # ASSIGN : n328 1 # ASSIGN : n329 4 # ASSIGN : n330 3 # ASSIGN : n331 5 # ASSIGN : n332 2 # ASSIGN : n333 1 # ASSIGN : n334 4 # ASSIGN : n335 3 # ASSIGN : n336 5 # ASSIGN : n337 2 # ASSIGN : n338 1 # ASSIGN : n339 4 # ASSIGN : n340 3 # ASSIGN : n341 5 # ASSIGN : n342 2 # ASSIGN : n343 1 # ASSIGN : n344 4 # ASSIGN : n345 3 # ASSIGN : n346 5 # ASSIGN : n347 2 # ASSIGN : n348 1 # ASSIGN : n349 4 # ASSIGN : n350 3 # ASSIGN : n351 5 # ASSIGN : n352 2 # ASSIGN : n353 1 # ASSIGN : n354 4 # ASSIGN : n355 3 # ASSIGN : n356 5 # ASSIGN : n357 2 # ASSIGN : n358 1 # ASSIGN : n359 4 # ASSIGN : n360 3 # ASSIGN : n361 5 # ASSIGN : n362 2 # ASSIGN : n363 1 # ASSIGN : n364 4 # ASSIGN : n365 3 # ASSIGN : n366 5 # ASSIGN : n367 2 # ASSIGN : n368 1 # ASSIGN : n369 4 # ASSIGN : n370 3 # ASSIGN : n371 5 # ASSIGN : n372 2 # ASSIGN : n373 1 # ASSIGN : n374 4 # ASSIGN : n375 3 # ASSIGN : n376 5 # ASSIGN : n377 2 # ASSIGN : n378 1 # ASSIGN : n379 4 # ASSIGN : n380 3 # ASSIGN : n381 5 # ASSIGN : n382 2 # ASSIGN : n383 1 # ASSIGN : n384 4 # ASSIGN : n385 3 # ASSIGN : n386 5 # ASSIGN : n387 2 # ASSIGN : n388 1 # ASSIGN : n389 4 # ASSIGN : n390 3 # ASSIGN : n391 5 # ASSIGN : n392 2 # ASSIGN : n393 1 # ASSIGN : n394 4 # ASSIGN : n395 3 # ASSIGN : n396 5 # ASSIGN : n397 2 # ASSIGN : n398 1 # ASSIGN : n399 4 # ASSIGN : n400 3 # ASSIGN : n401 5 # ASSIGN : n402 2 # ASSIGN : n403 1 # ASSIGN : n404 4 # ASSIGN : n405 3 # ASSIGN : n406 5 # ASSIGN : n407 2 # ASSIGN : n408 1 # ASSIGN : n409 4 # ASSIGN : n410 3 # ASSIGN : n411 5 # ASSIGN : n412 2 # ASSIGN : n413 1 # ASSIGN : n414 4 # ASSIGN : n415 3 # ASSIGN : n416 5 # ASSIGN : n417 2 # ASSIGN : n418 1 # ASSIGN : n419 4 # ASSIGN : n420 3 # ASSIGN : n421 5 # ASSIGN : n422 2 # ASSIGN : n423 1 # ASSIGN : n424 4 # ASSIGN : n425 3 # ASSIGN : n426 5 # ASSIGN : n427 2 # ASSIGN : n428 1 # ASSIGN : n429 4 # ASSIGN : n430 3 # ASSIGN : n431 5 # ASSIGN : n432 2 # ASSIGN : n433 1 # ASSIGN : n434 4 # ASSIGN : n435 3 # ASSIGN : n436 5 # ASSIGN : n437 2 # ASSIGN : n438 1 # ASSIGN : n439 4 # ASSIGN : n440 3 # ASSIGN : n441 5 # ASSIGN : n442 2 # ASSIGN : n443 1 # ASSIGN : n444 4 # ASSIGN : n445 3 # ASSIGN : n446 5 # ASSIGN : n447 2 # ASSIGN : n448 1 # ASSIGN : n449 4 # ASSIGN : n450 3 SHOW_RESULT 5 END : 5 (0 seconds) [Sat Jul 8 21:43:06 2006] SHOW_RESULT 5 CPU : 0.0399999999999991 = 0.0399999999999991 + 0 + 0 + 0 # BOUND : color 2 5 MODIFY_CNF 3 BEGIN : [Sat Jul 8 21:43:06 2006] MODIFY_CNF 3 END : 6909575 bytes (0 seconds) [Sat Jul 8 21:43:06 2006] MODIFY_CNF 3 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 3 BEGIN : [Sat Jul 8 21:43:06 2006] CMD : minisat /tmp/csp2sat5785.cnf /tmp/csp2sat5785.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 81684 250346 | 27228 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 9 (12 /sec) decisions : 12 (17 /sec) propagations : 10374 (14408 /sec) conflict literals : 14 (17.65 % deleted) Memory used : 15.15 MB CPU time : 0.72 s UNSATISFIABLE VERIFY_CNF 3 END : (0 seconds) [Sat Jul 8 21:43:06 2006] VERIFY_CNF 3 CPU : 0.77 = 0 + 0.01 + 0.72 + 0.04 # RESULT : color 3 UNSATISFIABLE # BOUND : color 4 5 MODIFY_CNF 4 BEGIN : [Sat Jul 8 21:43:06 2006] MODIFY_CNF 4 END : 6909575 bytes (0 seconds) [Sat Jul 8 21:43:06 2006] MODIFY_CNF 4 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 4 BEGIN : [Sat Jul 8 21:43:06 2006] CMD : minisat /tmp/csp2sat5785.cnf /tmp/csp2sat5785.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 101290 309164 | 33763 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 82 (164 /sec) decisions : 96 (192 /sec) propagations : 28955 (57910 /sec) conflict literals : 302 (17.49 % deleted) Memory used : 15.15 MB CPU time : 0.5 s UNSATISFIABLE VERIFY_CNF 4 END : (1 seconds) [Sat Jul 8 21:43:07 2006] VERIFY_CNF 4 CPU : 0.55 = 0 + 0 + 0.5 + 0.05 # RESULT : color 4 UNSATISFIABLE # BOUND : color 5 5 MAIN END : (35 seconds) [Sat Jul 8 21:43:07 2006] MAIN CPU : 34.58 = 31.19 + 0.23 + 2.97 + 0.19