# TIMEOUT 7200 MAIN BEGIN : [Mon Jul 10 21:34:02 2006] READ BEGIN : csp/school1_nsh.csp [Mon Jul 10 21:34:02 2006] READ END : csp/school1_nsh.csp (21 seconds) [Mon Jul 10 21:34:23 2006] READ CPU : 21.53 = 21.25 + 0.28 + 0 + 0 # BOUND : color 2 39 GENERATE_CNF 39 BEGIN : [Mon Jul 10 21:34:23 2006] GENERATE_CNF 39 END : 43695 variables 1182196 clauses 23970992 bytes (51 seconds) [Mon Jul 10 21:35:14 2006] GENERATE_CNF 39 CPU : 49.87 = 49.59 + 0.28 + 0 + 0 MODIFY_CNF 20 BEGIN : [Mon Jul 10 21:35:14 2006] MODIFY_CNF 20 END : 23970997 bytes (0 seconds) [Mon Jul 10 21:35:14 2006] MODIFY_CNF 20 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 20 BEGIN : [Mon Jul 10 21:35:14 2006] CMD : minisat /tmp/csp2sat29227.cnf /tmp/csp2sat29227.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 624823 1877786 | 208274 0 0 nan | 0.000 % | | 100 | 624823 1877786 | 229101 100 3165 31.6 | 17.771 % | | 251 | 624823 1877786 | 252011 251 4449 17.7 | 17.771 % | | 476 | 624823 1877786 | 277212 476 6484 13.6 | 17.771 % | | 813 | 624823 1877786 | 304933 813 11364 14.0 | 17.771 % | | 1319 | 624823 1877786 | 335427 1319 18888 14.3 | 17.771 % | ============================================================================== restarts : 6 conflicts : 1365 (119 /sec) decisions : 3493 (304 /sec) propagations : 546401 (47596 /sec) conflict literals : 19965 (4.83 % deleted) Memory used : 45.45 MB CPU time : 11.48 s SATISFIABLE VERIFY_CNF 20 END : (12 seconds) [Mon Jul 10 21:35:26 2006] VERIFY_CNF 20 CPU : 11.66 = 0 + 0.01 + 11.5 + 0.15 # RESULT : color 20 SATISFIABLE SHOW_RESULT 20 BEGIN : [Mon Jul 10 21:35:26 2006] # ASSIGN : color 20 # ASSIGN : n1 17 # ASSIGN : n2 19 # ASSIGN : n3 4 # ASSIGN : n4 5 # ASSIGN : n5 6 # ASSIGN : n6 13 # ASSIGN : n7 18 # ASSIGN : n8 17 # ASSIGN : n9 12 # ASSIGN : n10 10 # ASSIGN : n11 11 # ASSIGN : n12 16 # ASSIGN : n13 15 # ASSIGN : n14 19 # ASSIGN : n15 17 # ASSIGN : n16 3 # ASSIGN : n17 12 # ASSIGN : n18 4 # ASSIGN : n19 10 # ASSIGN : n20 18 # ASSIGN : n21 14 # ASSIGN : n22 1 # ASSIGN : n23 9 # ASSIGN : n24 5 # ASSIGN : n25 6 # ASSIGN : n26 2 # ASSIGN : n27 7 # ASSIGN : n28 4 # ASSIGN : n29 15 # ASSIGN : n30 8 # ASSIGN : n31 12 # ASSIGN : n32 17 # ASSIGN : n33 9 # ASSIGN : n34 16 # ASSIGN : n35 1 # ASSIGN : n36 10 # ASSIGN : n37 5 # ASSIGN : n38 3 # ASSIGN : n39 8 # ASSIGN : n40 19 # ASSIGN : n41 6 # ASSIGN : n42 11 # ASSIGN : n43 16 # ASSIGN : n44 2 # ASSIGN : n45 6 # ASSIGN : n46 20 # ASSIGN : n47 19 # ASSIGN : n48 12 # ASSIGN : n49 18 # ASSIGN : n50 4 # ASSIGN : n51 8 # ASSIGN : n52 18 # ASSIGN : n53 3 # ASSIGN : n54 14 # ASSIGN : n55 11 # ASSIGN : n56 15 # ASSIGN : n57 7 # ASSIGN : n58 10 # ASSIGN : n59 11 # ASSIGN : n60 7 # ASSIGN : n61 5 # ASSIGN : n62 3 # ASSIGN : n63 8 # ASSIGN : n64 9 # ASSIGN : n65 14 # ASSIGN : n66 13 # ASSIGN : n67 16 # ASSIGN : n68 15 # ASSIGN : n69 17 # ASSIGN : n70 16 # ASSIGN : n71 14 # ASSIGN : n72 9 # ASSIGN : n73 19 # ASSIGN : n74 13 # ASSIGN : n75 10 # ASSIGN : n76 11 # ASSIGN : n77 7 # ASSIGN : n78 5 # ASSIGN : n79 20 # ASSIGN : n80 10 # ASSIGN : n81 11 # ASSIGN : n82 7 # ASSIGN : n83 5 # ASSIGN : n84 3 # ASSIGN : n85 10 # ASSIGN : n86 20 # ASSIGN : n87 16 # ASSIGN : n88 19 # ASSIGN : n89 9 # ASSIGN : n90 2 # ASSIGN : n91 13 # ASSIGN : n92 16 # ASSIGN : n93 19 # ASSIGN : n94 9 # ASSIGN : n95 20 # ASSIGN : n96 13 # ASSIGN : n97 5 # ASSIGN : n98 3 # ASSIGN : n99 1 # ASSIGN : n100 8 # ASSIGN : n101 10 # ASSIGN : n102 11 # ASSIGN : n103 7 # ASSIGN : n104 19 # ASSIGN : n105 2 # ASSIGN : n106 6 # ASSIGN : n107 4 # ASSIGN : n108 11 # ASSIGN : n109 7 # ASSIGN : n110 14 # ASSIGN : n111 13 # ASSIGN : n112 9 # ASSIGN : n113 10 # ASSIGN : n114 5 # ASSIGN : n115 16 # ASSIGN : n116 5 # ASSIGN : n117 20 # ASSIGN : n118 1 # ASSIGN : n119 2 # ASSIGN : n120 4 # ASSIGN : n121 10 # ASSIGN : n122 11 # ASSIGN : n123 5 # ASSIGN : n124 13 # ASSIGN : n125 1 # ASSIGN : n126 16 # ASSIGN : n127 2 # ASSIGN : n128 6 # ASSIGN : n129 14 # ASSIGN : n130 18 # ASSIGN : n131 3 # ASSIGN : n132 9 # ASSIGN : n133 3 # ASSIGN : n134 8 # ASSIGN : n135 3 # ASSIGN : n136 20 # ASSIGN : n137 19 # ASSIGN : n138 19 # ASSIGN : n139 1 # ASSIGN : n140 1 # ASSIGN : n141 2 # ASSIGN : n142 2 # ASSIGN : n143 6 # ASSIGN : n144 9 # ASSIGN : n145 20 # ASSIGN : n146 4 # ASSIGN : n147 10 # ASSIGN : n148 14 # ASSIGN : n149 12 # ASSIGN : n150 16 # ASSIGN : n151 3 # ASSIGN : n152 13 # ASSIGN : n153 15 # ASSIGN : n154 3 # ASSIGN : n155 8 # ASSIGN : n156 2 # ASSIGN : n157 16 # ASSIGN : n158 1 # ASSIGN : n159 17 # ASSIGN : n160 1 # ASSIGN : n161 6 # ASSIGN : n162 3 # ASSIGN : n163 15 # ASSIGN : n164 7 # ASSIGN : n165 8 # ASSIGN : n166 10 # ASSIGN : n167 4 # ASSIGN : n168 6 # ASSIGN : n169 5 # ASSIGN : n170 3 # ASSIGN : n171 14 # ASSIGN : n172 19 # ASSIGN : n173 17 # ASSIGN : n174 2 # ASSIGN : n175 9 # ASSIGN : n176 3 # ASSIGN : n177 4 # ASSIGN : n178 9 # ASSIGN : n179 12 # ASSIGN : n180 5 # ASSIGN : n181 11 # ASSIGN : n182 16 # ASSIGN : n183 13 # ASSIGN : n184 1 # ASSIGN : n185 1 # ASSIGN : n186 8 # ASSIGN : n187 1 # ASSIGN : n188 2 # ASSIGN : n189 19 # ASSIGN : n190 16 # ASSIGN : n191 9 # ASSIGN : n192 12 # ASSIGN : n193 1 # ASSIGN : n194 2 # ASSIGN : n195 3 # ASSIGN : n196 4 # ASSIGN : n197 17 # ASSIGN : n198 4 # ASSIGN : n199 4 # ASSIGN : n200 18 # ASSIGN : n201 9 # ASSIGN : n202 6 # ASSIGN : n203 3 # ASSIGN : n204 10 # ASSIGN : n205 20 # ASSIGN : n206 1 # ASSIGN : n207 2 # ASSIGN : n208 12 # ASSIGN : n209 6 # ASSIGN : n210 18 # ASSIGN : n211 2 # ASSIGN : n212 11 # ASSIGN : n213 7 # ASSIGN : n214 17 # ASSIGN : n215 2 # ASSIGN : n216 20 # ASSIGN : n217 5 # ASSIGN : n218 11 # ASSIGN : n219 7 # ASSIGN : n220 5 # ASSIGN : n221 13 # ASSIGN : n222 16 # ASSIGN : n223 19 # ASSIGN : n224 5 # ASSIGN : n225 3 # ASSIGN : n226 7 # ASSIGN : n227 20 # ASSIGN : n228 10 # ASSIGN : n229 18 # ASSIGN : n230 13 # ASSIGN : n231 10 # ASSIGN : n232 9 # ASSIGN : n233 7 # ASSIGN : n234 13 # ASSIGN : n235 14 # ASSIGN : n236 20 # ASSIGN : n237 8 # ASSIGN : n238 17 # ASSIGN : n239 8 # ASSIGN : n240 12 # ASSIGN : n241 20 # ASSIGN : n242 11 # ASSIGN : n243 14 # ASSIGN : n244 4 # ASSIGN : n245 10 # ASSIGN : n246 7 # ASSIGN : n247 16 # ASSIGN : n248 18 # ASSIGN : n249 17 # ASSIGN : n250 13 # ASSIGN : n251 5 # ASSIGN : n252 3 # ASSIGN : n253 12 # ASSIGN : n254 6 # ASSIGN : n255 2 # ASSIGN : n256 4 # ASSIGN : n257 11 # ASSIGN : n258 7 # ASSIGN : n259 6 # ASSIGN : n260 15 # ASSIGN : n261 13 # ASSIGN : n262 19 # ASSIGN : n263 17 # ASSIGN : n264 3 # ASSIGN : n265 14 # ASSIGN : n266 4 # ASSIGN : n267 16 # ASSIGN : n268 7 # ASSIGN : n269 15 # ASSIGN : n270 17 # ASSIGN : n271 16 # ASSIGN : n272 18 # ASSIGN : n273 20 # ASSIGN : n274 13 # ASSIGN : n275 5 # ASSIGN : n276 3 # ASSIGN : n277 5 # ASSIGN : n278 18 # ASSIGN : n279 14 # ASSIGN : n280 13 # ASSIGN : n281 5 # ASSIGN : n282 3 # ASSIGN : n283 2 # ASSIGN : n284 20 # ASSIGN : n285 19 # ASSIGN : n286 4 # ASSIGN : n287 11 # ASSIGN : n288 7 # ASSIGN : n289 16 # ASSIGN : n290 19 # ASSIGN : n291 10 # ASSIGN : n292 20 # ASSIGN : n293 3 # ASSIGN : n294 4 # ASSIGN : n295 7 # ASSIGN : n296 11 # ASSIGN : n297 17 # ASSIGN : n298 6 # ASSIGN : n299 1 # ASSIGN : n300 5 # ASSIGN : n301 12 # ASSIGN : n302 4 # ASSIGN : n303 10 # ASSIGN : n304 17 # ASSIGN : n305 13 # ASSIGN : n306 14 # ASSIGN : n307 7 # ASSIGN : n308 8 # ASSIGN : n309 20 # ASSIGN : n310 6 # ASSIGN : n311 9 # ASSIGN : n312 15 # ASSIGN : n313 20 # ASSIGN : n314 18 # ASSIGN : n315 20 # ASSIGN : n316 20 # ASSIGN : n317 8 # ASSIGN : n318 16 # ASSIGN : n319 17 # ASSIGN : n320 6 # ASSIGN : n321 9 # ASSIGN : n322 11 # ASSIGN : n323 4 # ASSIGN : n324 10 # ASSIGN : n325 5 # ASSIGN : n326 13 # ASSIGN : n327 15 # ASSIGN : n328 8 # ASSIGN : n329 13 # ASSIGN : n330 16 # ASSIGN : n331 4 # ASSIGN : n332 6 # ASSIGN : n333 9 # ASSIGN : n334 19 # ASSIGN : n335 6 # ASSIGN : n336 9 # ASSIGN : n337 19 # ASSIGN : n338 20 # ASSIGN : n339 15 # ASSIGN : n340 18 # ASSIGN : n341 10 # ASSIGN : n342 11 # ASSIGN : n343 7 # ASSIGN : n344 10 # ASSIGN : n345 11 # ASSIGN : n346 7 # ASSIGN : n347 4 # ASSIGN : n348 10 # ASSIGN : n349 11 # ASSIGN : n350 6 # ASSIGN : n351 13 # ASSIGN : n352 9 SHOW_RESULT 20 END : 20 (0 seconds) [Mon Jul 10 21:35:26 2006] SHOW_RESULT 20 CPU : 0.0499999999999972 = 0.0499999999999972 + 0 + 0 + 0 # BOUND : color 2 20 MODIFY_CNF 11 BEGIN : [Mon Jul 10 21:35:26 2006] MODIFY_CNF 11 END : 23970997 bytes (0 seconds) [Mon Jul 10 21:35:26 2006] MODIFY_CNF 11 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 11 BEGIN : [Mon Jul 10 21:35:26 2006] CMD : minisat /tmp/csp2sat29227.cnf /tmp/csp2sat29227.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 361807 1088738 | 120602 0 0 nan | 0.000 % | | 100 | 361807 1088738 | 132662 100 964 9.6 | 25.042 % | | 251 | 361807 1088738 | 145928 251 2070 8.2 | 25.042 % | | 479 | 361807 1088738 | 160521 479 3980 8.3 | 25.042 % | | 816 | 361807 1088738 | 176573 816 7238 8.9 | 25.042 % | | 1322 | 361807 1088738 | 194230 1322 11039 8.4 | 25.042 % | | 2081 | 361807 1088738 | 213653 2081 17987 8.6 | 25.042 % | | 3220 | 361807 1088738 | 235019 3220 27787 8.6 | 25.042 % | | 4929 | 361807 1088738 | 258521 4929 45124 9.2 | 25.042 % | | 7491 | 361807 1088738 | 284373 7491 70594 9.4 | 25.042 % | | 11336 | 361807 1088738 | 312810 11336 107011 9.4 | 25.042 % | | 17103 | 361807 1088738 | 344091 17103 171250 10.0 | 25.042 % | | 25753 | 361807 1088738 | 378500 25753 271163 10.5 | 25.042 % | | 38727 | 361808 1088738 | 416350 38726 403436 10.4 | 25.042 % | | 58188 | 361486 1087775 | 457985 45334 459492 10.1 | 25.049 % | ============================================================================== restarts : 15 conflicts : 65735 (1550 /sec) decisions : 77436 (1826 /sec) propagations : 4789622 (112963 /sec) conflict literals : 662930 (10.27 % deleted) Memory used : 45.52 MB CPU time : 42.4 s UNSATISFIABLE VERIFY_CNF 11 END : (42 seconds) [Mon Jul 10 21:36:08 2006] VERIFY_CNF 11 CPU : 42.56 = 0.0100000000000051 + 0.01 + 42.41 + 0.13 # RESULT : color 11 UNSATISFIABLE # BOUND : color 12 20 MODIFY_CNF 16 BEGIN : [Mon Jul 10 21:36:08 2006] MODIFY_CNF 16 END : 23970997 bytes (0 seconds) [Mon Jul 10 21:36:08 2006] MODIFY_CNF 16 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 16 BEGIN : [Mon Jul 10 21:36:08 2006] CMD : minisat /tmp/csp2sat29227.cnf /tmp/csp2sat29227.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 507927 1527098 | 169309 0 0 nan | 0.000 % | | 100 | 507927 1527098 | 186239 100 2768 27.7 | 21.002 % | | 252 | 507927 1527098 | 204863 252 3892 15.4 | 21.002 % | | 478 | 507927 1527098 | 225350 478 12177 25.5 | 21.002 % | ============================================================================== restarts : 4 conflicts : 560 (42 /sec) decisions : 1701 (127 /sec) propagations : 765179 (56933 /sec) conflict literals : 14420 (1.78 % deleted) Memory used : 45.46 MB CPU time : 13.44 s SATISFIABLE VERIFY_CNF 16 END : (14 seconds) [Mon Jul 10 21:36:22 2006] VERIFY_CNF 16 CPU : 13.59 = 0 + 0 + 13.46 + 0.13 # RESULT : color 16 SATISFIABLE SHOW_RESULT 16 BEGIN : [Mon Jul 10 21:36:22 2006] # ASSIGN : color 16 # ASSIGN : n1 12 # ASSIGN : n2 15 # ASSIGN : n3 1 # ASSIGN : n4 11 # ASSIGN : n5 9 # ASSIGN : n6 6 # ASSIGN : n7 2 # ASSIGN : n8 12 # ASSIGN : n9 3 # ASSIGN : n10 4 # ASSIGN : n11 10 # ASSIGN : n12 8 # ASSIGN : n13 16 # ASSIGN : n14 14 # ASSIGN : n15 12 # ASSIGN : n16 13 # ASSIGN : n17 3 # ASSIGN : n18 15 # ASSIGN : n19 4 # ASSIGN : n20 13 # ASSIGN : n21 3 # ASSIGN : n22 7 # ASSIGN : n23 2 # ASSIGN : n24 5 # ASSIGN : n25 9 # ASSIGN : n26 12 # ASSIGN : n27 7 # ASSIGN : n28 15 # ASSIGN : n29 14 # ASSIGN : n30 12 # ASSIGN : n31 3 # ASSIGN : n32 13 # ASSIGN : n33 2 # ASSIGN : n34 8 # ASSIGN : n35 1 # ASSIGN : n36 4 # ASSIGN : n37 11 # ASSIGN : n38 13 # ASSIGN : n39 3 # ASSIGN : n40 16 # ASSIGN : n41 9 # ASSIGN : n42 10 # ASSIGN : n43 8 # ASSIGN : n44 5 # ASSIGN : n45 9 # ASSIGN : n46 5 # ASSIGN : n47 14 # ASSIGN : n48 12 # ASSIGN : n49 9 # ASSIGN : n50 1 # ASSIGN : n51 14 # ASSIGN : n52 12 # ASSIGN : n53 13 # ASSIGN : n54 3 # ASSIGN : n55 10 # ASSIGN : n56 16 # ASSIGN : n57 7 # ASSIGN : n58 4 # ASSIGN : n59 10 # ASSIGN : n60 7 # ASSIGN : n61 11 # ASSIGN : n62 13 # ASSIGN : n63 3 # ASSIGN : n64 15 # ASSIGN : n65 16 # ASSIGN : n66 6 # ASSIGN : n67 8 # ASSIGN : n68 14 # ASSIGN : n69 12 # ASSIGN : n70 8 # ASSIGN : n71 14 # ASSIGN : n72 2 # ASSIGN : n73 16 # ASSIGN : n74 6 # ASSIGN : n75 4 # ASSIGN : n76 10 # ASSIGN : n77 7 # ASSIGN : n78 11 # ASSIGN : n79 13 # ASSIGN : n80 4 # ASSIGN : n81 10 # ASSIGN : n82 7 # ASSIGN : n83 11 # ASSIGN : n84 13 # ASSIGN : n85 4 # ASSIGN : n86 16 # ASSIGN : n87 8 # ASSIGN : n88 14 # ASSIGN : n89 2 # ASSIGN : n90 16 # ASSIGN : n91 6 # ASSIGN : n92 8 # ASSIGN : n93 14 # ASSIGN : n94 2 # ASSIGN : n95 16 # ASSIGN : n96 6 # ASSIGN : n97 11 # ASSIGN : n98 13 # ASSIGN : n99 5 # ASSIGN : n100 3 # ASSIGN : n101 4 # ASSIGN : n102 10 # ASSIGN : n103 7 # ASSIGN : n104 15 # ASSIGN : n105 15 # ASSIGN : n106 9 # ASSIGN : n107 1 # ASSIGN : n108 10 # ASSIGN : n109 7 # ASSIGN : n110 16 # ASSIGN : n111 6 # ASSIGN : n112 4 # ASSIGN : n113 2 # ASSIGN : n114 8 # ASSIGN : n115 1 # ASSIGN : n116 8 # ASSIGN : n117 5 # ASSIGN : n118 11 # ASSIGN : n119 5 # ASSIGN : n120 1 # ASSIGN : n121 4 # ASSIGN : n122 10 # ASSIGN : n123 11 # ASSIGN : n124 6 # ASSIGN : n125 16 # ASSIGN : n126 8 # ASSIGN : n127 12 # ASSIGN : n128 9 # ASSIGN : n129 3 # ASSIGN : n130 14 # ASSIGN : n131 13 # ASSIGN : n132 14 # ASSIGN : n133 13 # ASSIGN : n134 14 # ASSIGN : n135 13 # ASSIGN : n136 16 # ASSIGN : n137 15 # ASSIGN : n138 15 # ASSIGN : n139 14 # ASSIGN : n140 8 # ASSIGN : n141 3 # ASSIGN : n142 14 # ASSIGN : n143 9 # ASSIGN : n144 2 # ASSIGN : n145 16 # ASSIGN : n146 1 # ASSIGN : n147 4 # ASSIGN : n148 3 # ASSIGN : n149 10 # ASSIGN : n150 8 # ASSIGN : n151 13 # ASSIGN : n152 6 # ASSIGN : n153 10 # ASSIGN : n154 13 # ASSIGN : n155 3 # ASSIGN : n156 1 # ASSIGN : n157 8 # ASSIGN : n158 14 # ASSIGN : n159 12 # ASSIGN : n160 16 # ASSIGN : n161 9 # ASSIGN : n162 4 # ASSIGN : n163 10 # ASSIGN : n164 7 # ASSIGN : n165 8 # ASSIGN : n166 4 # ASSIGN : n167 15 # ASSIGN : n168 6 # ASSIGN : n169 11 # ASSIGN : n170 13 # ASSIGN : n171 3 # ASSIGN : n172 14 # ASSIGN : n173 12 # ASSIGN : n174 9 # ASSIGN : n175 2 # ASSIGN : n176 1 # ASSIGN : n177 5 # ASSIGN : n178 15 # ASSIGN : n179 16 # ASSIGN : n180 11 # ASSIGN : n181 10 # ASSIGN : n182 8 # ASSIGN : n183 6 # ASSIGN : n184 16 # ASSIGN : n185 14 # ASSIGN : n186 15 # ASSIGN : n187 14 # ASSIGN : n188 16 # ASSIGN : n189 14 # ASSIGN : n190 8 # ASSIGN : n191 2 # ASSIGN : n192 3 # ASSIGN : n193 15 # ASSIGN : n194 16 # ASSIGN : n195 13 # ASSIGN : n196 1 # ASSIGN : n197 12 # ASSIGN : n198 1 # ASSIGN : n199 1 # ASSIGN : n200 9 # ASSIGN : n201 5 # ASSIGN : n202 9 # ASSIGN : n203 13 # ASSIGN : n204 4 # ASSIGN : n205 10 # ASSIGN : n206 2 # ASSIGN : n207 16 # ASSIGN : n208 14 # ASSIGN : n209 12 # ASSIGN : n210 9 # ASSIGN : n211 15 # ASSIGN : n212 10 # ASSIGN : n213 1 # ASSIGN : n214 12 # ASSIGN : n215 16 # ASSIGN : n216 13 # ASSIGN : n217 11 # ASSIGN : n218 10 # ASSIGN : n219 7 # ASSIGN : n220 11 # ASSIGN : n221 6 # ASSIGN : n222 8 # ASSIGN : n223 14 # ASSIGN : n224 11 # ASSIGN : n225 13 # ASSIGN : n226 7 # ASSIGN : n227 16 # ASSIGN : n228 4 # ASSIGN : n229 15 # ASSIGN : n230 6 # ASSIGN : n231 4 # ASSIGN : n232 2 # ASSIGN : n233 7 # ASSIGN : n234 6 # ASSIGN : n235 15 # ASSIGN : n236 14 # ASSIGN : n237 12 # ASSIGN : n238 3 # ASSIGN : n239 12 # ASSIGN : n240 3 # ASSIGN : n241 14 # ASSIGN : n242 10 # ASSIGN : n243 3 # ASSIGN : n244 15 # ASSIGN : n245 4 # ASSIGN : n246 7 # ASSIGN : n247 8 # ASSIGN : n248 14 # ASSIGN : n249 12 # ASSIGN : n250 6 # ASSIGN : n251 11 # ASSIGN : n252 13 # ASSIGN : n253 3 # ASSIGN : n254 9 # ASSIGN : n255 16 # ASSIGN : n256 1 # ASSIGN : n257 10 # ASSIGN : n258 7 # ASSIGN : n259 15 # ASSIGN : n260 16 # ASSIGN : n261 6 # ASSIGN : n262 14 # ASSIGN : n263 12 # ASSIGN : n264 13 # ASSIGN : n265 3 # ASSIGN : n266 1 # ASSIGN : n267 8 # ASSIGN : n268 7 # ASSIGN : n269 14 # ASSIGN : n270 12 # ASSIGN : n271 8 # ASSIGN : n272 9 # ASSIGN : n273 16 # ASSIGN : n274 6 # ASSIGN : n275 11 # ASSIGN : n276 13 # ASSIGN : n277 11 # ASSIGN : n278 9 # ASSIGN : n279 16 # ASSIGN : n280 6 # ASSIGN : n281 11 # ASSIGN : n282 13 # ASSIGN : n283 3 # ASSIGN : n284 16 # ASSIGN : n285 15 # ASSIGN : n286 1 # ASSIGN : n287 10 # ASSIGN : n288 7 # ASSIGN : n289 8 # ASSIGN : n290 14 # ASSIGN : n291 4 # ASSIGN : n292 14 # ASSIGN : n293 13 # ASSIGN : n294 15 # ASSIGN : n295 7 # ASSIGN : n296 10 # ASSIGN : n297 12 # ASSIGN : n298 9 # ASSIGN : n299 5 # ASSIGN : n300 11 # ASSIGN : n301 3 # ASSIGN : n302 1 # ASSIGN : n303 4 # ASSIGN : n304 12 # ASSIGN : n305 6 # ASSIGN : n306 3 # ASSIGN : n307 7 # ASSIGN : n308 14 # ASSIGN : n309 5 # ASSIGN : n310 9 # ASSIGN : n311 2 # ASSIGN : n312 16 # ASSIGN : n313 15 # ASSIGN : n314 14 # ASSIGN : n315 16 # ASSIGN : n316 16 # ASSIGN : n317 5 # ASSIGN : n318 8 # ASSIGN : n319 12 # ASSIGN : n320 15 # ASSIGN : n321 2 # ASSIGN : n322 16 # ASSIGN : n323 1 # ASSIGN : n324 4 # ASSIGN : n325 11 # ASSIGN : n326 6 # ASSIGN : n327 15 # ASSIGN : n328 11 # ASSIGN : n329 6 # ASSIGN : n330 8 # ASSIGN : n331 5 # ASSIGN : n332 9 # ASSIGN : n333 2 # ASSIGN : n334 16 # ASSIGN : n335 9 # ASSIGN : n336 2 # ASSIGN : n337 16 # ASSIGN : n338 13 # ASSIGN : n339 15 # ASSIGN : n340 11 # ASSIGN : n341 4 # ASSIGN : n342 10 # ASSIGN : n343 7 # ASSIGN : n344 4 # ASSIGN : n345 10 # ASSIGN : n346 7 # ASSIGN : n347 15 # ASSIGN : n348 4 # ASSIGN : n349 10 # ASSIGN : n350 9 # ASSIGN : n351 6 # ASSIGN : n352 2 SHOW_RESULT 16 END : 16 (0 seconds) [Mon Jul 10 21:36:22 2006] SHOW_RESULT 16 CPU : 0.0499999999999972 = 0.0499999999999972 + 0 + 0 + 0 # BOUND : color 12 16 MODIFY_CNF 14 BEGIN : [Mon Jul 10 21:36:22 2006] MODIFY_CNF 14 END : 23970997 bytes (0 seconds) [Mon Jul 10 21:36:22 2006] MODIFY_CNF 14 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 14 BEGIN : [Mon Jul 10 21:36:22 2006] CMD : minisat /tmp/csp2sat29227.cnf /tmp/csp2sat29227.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 449479 1351754 | 149826 0 0 nan | 0.000 % | | 100 | 449479 1351754 | 164808 100 2455 24.6 | 22.618 % | | 251 | 449479 1351754 | 181289 251 3712 14.8 | 22.618 % | | 477 | 449479 1351754 | 199418 477 6457 13.5 | 22.618 % | ============================================================================== restarts : 4 conflicts : 529 (84 /sec) decisions : 1149 (183 /sec) propagations : 364491 (57948 /sec) conflict literals : 6778 (5.90 % deleted) Memory used : 45.46 MB CPU time : 6.29 s SATISFIABLE VERIFY_CNF 14 END : (6 seconds) [Mon Jul 10 21:36:28 2006] VERIFY_CNF 14 CPU : 6.47 = 0 + 0.01 + 6.31 + 0.15 # RESULT : color 14 SATISFIABLE SHOW_RESULT 14 BEGIN : [Mon Jul 10 21:36:28 2006] # ASSIGN : color 14 # ASSIGN : n1 3 # ASSIGN : n2 13 # ASSIGN : n3 13 # ASSIGN : n4 6 # ASSIGN : n5 5 # ASSIGN : n6 12 # ASSIGN : n7 4 # ASSIGN : n8 3 # ASSIGN : n9 10 # ASSIGN : n10 2 # ASSIGN : n11 1 # ASSIGN : n12 9 # ASSIGN : n13 11 # ASSIGN : n14 7 # ASSIGN : n15 3 # ASSIGN : n16 14 # ASSIGN : n17 10 # ASSIGN : n18 13 # ASSIGN : n19 2 # ASSIGN : n20 14 # ASSIGN : n21 10 # ASSIGN : n22 11 # ASSIGN : n23 4 # ASSIGN : n24 6 # ASSIGN : n25 5 # ASSIGN : n26 3 # ASSIGN : n27 11 # ASSIGN : n28 13 # ASSIGN : n29 7 # ASSIGN : n30 3 # ASSIGN : n31 10 # ASSIGN : n32 14 # ASSIGN : n33 4 # ASSIGN : n34 9 # ASSIGN : n35 13 # ASSIGN : n36 2 # ASSIGN : n37 6 # ASSIGN : n38 14 # ASSIGN : n39 10 # ASSIGN : n40 11 # ASSIGN : n41 5 # ASSIGN : n42 1 # ASSIGN : n43 9 # ASSIGN : n44 5 # ASSIGN : n45 5 # ASSIGN : n46 4 # ASSIGN : n47 7 # ASSIGN : n48 3 # ASSIGN : n49 5 # ASSIGN : n50 13 # ASSIGN : n51 7 # ASSIGN : n52 3 # ASSIGN : n53 14 # ASSIGN : n54 10 # ASSIGN : n55 1 # ASSIGN : n56 8 # ASSIGN : n57 11 # ASSIGN : n58 2 # ASSIGN : n59 1 # ASSIGN : n60 11 # ASSIGN : n61 6 # ASSIGN : n62 14 # ASSIGN : n63 10 # ASSIGN : n64 4 # ASSIGN : n65 8 # ASSIGN : n66 12 # ASSIGN : n67 9 # ASSIGN : n68 7 # ASSIGN : n69 3 # ASSIGN : n70 9 # ASSIGN : n71 7 # ASSIGN : n72 4 # ASSIGN : n73 8 # ASSIGN : n74 12 # ASSIGN : n75 2 # ASSIGN : n76 1 # ASSIGN : n77 11 # ASSIGN : n78 6 # ASSIGN : n79 14 # ASSIGN : n80 2 # ASSIGN : n81 1 # ASSIGN : n82 11 # ASSIGN : n83 6 # ASSIGN : n84 14 # ASSIGN : n85 2 # ASSIGN : n86 14 # ASSIGN : n87 9 # ASSIGN : n88 7 # ASSIGN : n89 4 # ASSIGN : n90 8 # ASSIGN : n91 12 # ASSIGN : n92 9 # ASSIGN : n93 7 # ASSIGN : n94 4 # ASSIGN : n95 8 # ASSIGN : n96 12 # ASSIGN : n97 6 # ASSIGN : n98 14 # ASSIGN : n99 8 # ASSIGN : n100 10 # ASSIGN : n101 2 # ASSIGN : n102 1 # ASSIGN : n103 11 # ASSIGN : n104 13 # ASSIGN : n105 3 # ASSIGN : n106 5 # ASSIGN : n107 13 # ASSIGN : n108 1 # ASSIGN : n109 11 # ASSIGN : n110 8 # ASSIGN : n111 12 # ASSIGN : n112 4 # ASSIGN : n113 2 # ASSIGN : n114 9 # ASSIGN : n115 6 # ASSIGN : n116 9 # ASSIGN : n117 3 # ASSIGN : n118 9 # ASSIGN : n119 6 # ASSIGN : n120 13 # ASSIGN : n121 2 # ASSIGN : n122 1 # ASSIGN : n123 6 # ASSIGN : n124 12 # ASSIGN : n125 8 # ASSIGN : n126 9 # ASSIGN : n127 3 # ASSIGN : n128 5 # ASSIGN : n129 10 # ASSIGN : n130 7 # ASSIGN : n131 14 # ASSIGN : n132 7 # ASSIGN : n133 14 # ASSIGN : n134 7 # ASSIGN : n135 14 # ASSIGN : n136 14 # ASSIGN : n137 13 # ASSIGN : n138 13 # ASSIGN : n139 7 # ASSIGN : n140 7 # ASSIGN : n141 12 # ASSIGN : n142 7 # ASSIGN : n143 5 # ASSIGN : n144 4 # ASSIGN : n145 8 # ASSIGN : n146 13 # ASSIGN : n147 2 # ASSIGN : n148 10 # ASSIGN : n149 1 # ASSIGN : n150 9 # ASSIGN : n151 14 # ASSIGN : n152 12 # ASSIGN : n153 1 # ASSIGN : n154 14 # ASSIGN : n155 10 # ASSIGN : n156 10 # ASSIGN : n157 9 # ASSIGN : n158 7 # ASSIGN : n159 3 # ASSIGN : n160 8 # ASSIGN : n161 5 # ASSIGN : n162 2 # ASSIGN : n163 1 # ASSIGN : n164 11 # ASSIGN : n165 9 # ASSIGN : n166 2 # ASSIGN : n167 13 # ASSIGN : n168 3 # ASSIGN : n169 6 # ASSIGN : n170 14 # ASSIGN : n171 10 # ASSIGN : n172 7 # ASSIGN : n173 3 # ASSIGN : n174 5 # ASSIGN : n175 4 # ASSIGN : n176 11 # ASSIGN : n177 13 # ASSIGN : n178 4 # ASSIGN : n179 8 # ASSIGN : n180 6 # ASSIGN : n181 1 # ASSIGN : n182 9 # ASSIGN : n183 12 # ASSIGN : n184 8 # ASSIGN : n185 1 # ASSIGN : n186 9 # ASSIGN : n187 7 # ASSIGN : n188 2 # ASSIGN : n189 7 # ASSIGN : n190 9 # ASSIGN : n191 4 # ASSIGN : n192 10 # ASSIGN : n193 1 # ASSIGN : n194 2 # ASSIGN : n195 3 # ASSIGN : n196 13 # ASSIGN : n197 3 # ASSIGN : n198 13 # ASSIGN : n199 13 # ASSIGN : n200 5 # ASSIGN : n201 4 # ASSIGN : n202 5 # ASSIGN : n203 14 # ASSIGN : n204 2 # ASSIGN : n205 1 # ASSIGN : n206 4 # ASSIGN : n207 8 # ASSIGN : n208 7 # ASSIGN : n209 3 # ASSIGN : n210 5 # ASSIGN : n211 4 # ASSIGN : n212 1 # ASSIGN : n213 11 # ASSIGN : n214 3 # ASSIGN : n215 8 # ASSIGN : n216 14 # ASSIGN : n217 6 # ASSIGN : n218 1 # ASSIGN : n219 11 # ASSIGN : n220 6 # ASSIGN : n221 12 # ASSIGN : n222 9 # ASSIGN : n223 7 # ASSIGN : n224 6 # ASSIGN : n225 14 # ASSIGN : n226 11 # ASSIGN : n227 8 # ASSIGN : n228 2 # ASSIGN : n229 3 # ASSIGN : n230 12 # ASSIGN : n231 2 # ASSIGN : n232 4 # ASSIGN : n233 11 # ASSIGN : n234 12 # ASSIGN : n235 3 # ASSIGN : n236 2 # ASSIGN : n237 3 # ASSIGN : n238 10 # ASSIGN : n239 3 # ASSIGN : n240 10 # ASSIGN : n241 14 # ASSIGN : n242 1 # ASSIGN : n243 10 # ASSIGN : n244 13 # ASSIGN : n245 2 # ASSIGN : n246 11 # ASSIGN : n247 9 # ASSIGN : n248 7 # ASSIGN : n249 3 # ASSIGN : n250 12 # ASSIGN : n251 6 # ASSIGN : n252 14 # ASSIGN : n253 10 # ASSIGN : n254 5 # ASSIGN : n255 8 # ASSIGN : n256 13 # ASSIGN : n257 1 # ASSIGN : n258 11 # ASSIGN : n259 5 # ASSIGN : n260 8 # ASSIGN : n261 12 # ASSIGN : n262 7 # ASSIGN : n263 3 # ASSIGN : n264 14 # ASSIGN : n265 10 # ASSIGN : n266 13 # ASSIGN : n267 9 # ASSIGN : n268 11 # ASSIGN : n269 7 # ASSIGN : n270 3 # ASSIGN : n271 9 # ASSIGN : n272 5 # ASSIGN : n273 8 # ASSIGN : n274 12 # ASSIGN : n275 6 # ASSIGN : n276 14 # ASSIGN : n277 6 # ASSIGN : n278 5 # ASSIGN : n279 8 # ASSIGN : n280 12 # ASSIGN : n281 6 # ASSIGN : n282 14 # ASSIGN : n283 10 # ASSIGN : n284 14 # ASSIGN : n285 13 # ASSIGN : n286 13 # ASSIGN : n287 1 # ASSIGN : n288 11 # ASSIGN : n289 9 # ASSIGN : n290 7 # ASSIGN : n291 2 # ASSIGN : n292 7 # ASSIGN : n293 14 # ASSIGN : n294 13 # ASSIGN : n295 11 # ASSIGN : n296 1 # ASSIGN : n297 3 # ASSIGN : n298 5 # ASSIGN : n299 8 # ASSIGN : n300 6 # ASSIGN : n301 10 # ASSIGN : n302 13 # ASSIGN : n303 2 # ASSIGN : n304 3 # ASSIGN : n305 12 # ASSIGN : n306 10 # ASSIGN : n307 11 # ASSIGN : n308 7 # ASSIGN : n309 14 # ASSIGN : n310 5 # ASSIGN : n311 4 # ASSIGN : n312 8 # ASSIGN : n313 13 # ASSIGN : n314 12 # ASSIGN : n315 14 # ASSIGN : n316 14 # ASSIGN : n317 8 # ASSIGN : n318 9 # ASSIGN : n319 3 # ASSIGN : n320 5 # ASSIGN : n321 4 # ASSIGN : n322 1 # ASSIGN : n323 13 # ASSIGN : n324 2 # ASSIGN : n325 6 # ASSIGN : n326 12 # ASSIGN : n327 13 # ASSIGN : n328 6 # ASSIGN : n329 12 # ASSIGN : n330 9 # ASSIGN : n331 13 # ASSIGN : n332 5 # ASSIGN : n333 4 # ASSIGN : n334 8 # ASSIGN : n335 5 # ASSIGN : n336 4 # ASSIGN : n337 8 # ASSIGN : n338 14 # ASSIGN : n339 13 # ASSIGN : n340 6 # ASSIGN : n341 2 # ASSIGN : n342 1 # ASSIGN : n343 11 # ASSIGN : n344 2 # ASSIGN : n345 1 # ASSIGN : n346 11 # ASSIGN : n347 13 # ASSIGN : n348 2 # ASSIGN : n349 1 # ASSIGN : n350 5 # ASSIGN : n351 12 # ASSIGN : n352 4 SHOW_RESULT 14 END : 14 (0 seconds) [Mon Jul 10 21:36:28 2006] SHOW_RESULT 14 CPU : 0.0500000000000114 = 0.0500000000000114 + 0 + 0 + 0 # BOUND : color 12 14 MODIFY_CNF 13 BEGIN : [Mon Jul 10 21:36:28 2006] MODIFY_CNF 13 END : 23970997 bytes (0 seconds) [Mon Jul 10 21:36:28 2006] MODIFY_CNF 13 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 13 BEGIN : [Mon Jul 10 21:36:28 2006] CMD : minisat /tmp/csp2sat29227.cnf /tmp/csp2sat29227.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 420255 1264082 | 140085 0 0 nan | 0.000 % | | 101 | 420255 1264082 | 154093 101 1032 10.2 | 23.426 % | | 252 | 420255 1264082 | 169502 252 2589 10.3 | 23.426 % | | 478 | 420255 1264082 | 186453 478 4890 10.2 | 23.426 % | | 815 | 420255 1264082 | 205098 815 7533 9.2 | 23.426 % | | 1322 | 420255 1264082 | 225608 1322 11239 8.5 | 23.426 % | | 2082 | 420255 1264082 | 248169 2082 16720 8.0 | 23.426 % | | 3221 | 420255 1264082 | 272986 3221 28453 8.8 | 23.426 % | | 4929 | 420255 1264082 | 300284 4929 45141 9.2 | 23.426 % | | 7491 | 420255 1264082 | 330313 7491 67534 9.0 | 23.426 % | | 11335 | 420255 1264082 | 363344 11335 110126 9.7 | 23.426 % | | 17102 | 420255 1264082 | 399678 17102 174872 10.2 | 23.426 % | | 25752 | 420255 1264082 | 439646 25752 269973 10.5 | 23.426 % | | 38726 | 420255 1264082 | 483611 38726 432531 11.2 | 23.426 % | | 58187 | 420255 1264082 | 531972 58187 636800 10.9 | 23.426 % | | 87379 | 420255 1264082 | 585169 87379 1006340 11.5 | 23.426 % | | 131169 | 420255 1264082 | 643686 131169 1534308 11.7 | 23.426 % | | 196854 | 420256 1264082 | 708055 196853 2305765 11.7 | 23.426 % | | 295381 | 420071 1263530 | 778861 265694 3162563 11.9 | 23.431 % | ============================================================================== restarts : 19 conflicts : 346651 (418 /sec) decisions : 399111 (481 /sec) propagations : 15719265 (18958 /sec) conflict literals : 4033133 (9.95 % deleted) Memory used : 52.73 MB CPU time : 829.15 s UNSATISFIABLE VERIFY_CNF 13 END : (830 seconds) [Mon Jul 10 21:50:18 2006] VERIFY_CNF 13 CPU : 829.87 = 0 + 0.01 + 829.15 + 0.71 # RESULT : color 13 UNSATISFIABLE # BOUND : color 14 14 MAIN END : (976 seconds) [Mon Jul 10 21:50:18 2006] MAIN CPU : 975.73 = 71.03 + 0.6 + 902.83 + 1.27