# TIMEOUT 7200
MAIN  BEGIN :  [Mon Jul 10 21:12:56 2006]
READ  BEGIN : csp/school1.csp [Mon Jul 10 21:12:56 2006]
READ  END : csp/school1.csp (28 seconds) [Mon Jul 10 21:13:24 2006]
READ  CPU : 28.6 = 28.26 + 0.34 + 0 + 0

# BOUND : color 2 42

GENERATE_CNF 42 BEGIN :  [Mon Jul 10 21:13:24 2006]
GENERATE_CNF 42 END : 55172 variables 1655843 clauses 34121194 bytes (71 seconds) [Mon Jul 10 21:14:35 2006]
GENERATE_CNF 42 CPU : 70 = 69.77 + 0.23 + 0 + 0

MODIFY_CNF 22 BEGIN :  [Mon Jul 10 21:14:35 2006]
MODIFY_CNF 22 END : 34121199 bytes (0 seconds) [Mon Jul 10 21:14:35 2006]
MODIFY_CNF 22 CPU : 0 = 0 + 0 + 0 + 0

VERIFY_CNF 22 BEGIN :  [Mon Jul 10 21:14:35 2006]
CMD : minisat /tmp/csp2sat28870.cnf /tmp/csp2sat28870.out
==================================[MINISAT]===================================
| Conflicts |     ORIGINAL     |              LEARNT              | Progress |
|           | Clauses Literals |   Limit Clauses Literals  Lit/Cl |          |
==============================================================================
|         0 |  889728  2674770 |  296576       0        0     nan |  0.000 % |
|       100 |  889728  2674770 |  326233     100     2441    24.4 | 16.090 % |
|       251 |  889728  2674770 |  358856     251     4200    16.7 | 16.090 % |
==============================================================================
restarts              : 3
conflicts             : 289            (41 /sec)
decisions             : 1727           (243 /sec)
propagations          : 265135         (37343 /sec)
conflict literals     : 5095           (3.65 % deleted)
Memory used           : 63.05 MB
CPU time              : 7.1 s

SATISFIABLE
VERIFY_CNF 22 END :  (7 seconds) [Mon Jul 10 21:14:42 2006]
VERIFY_CNF 22 CPU : 7.32 = 0 + 0.01 + 7.13 + 0.18

# RESULT : color 22 SATISFIABLE
SHOW_RESULT 22 BEGIN :  [Mon Jul 10 21:14:42 2006]
# ASSIGN : color 22
# ASSIGN : n1 1
# ASSIGN : n2 16
# ASSIGN : n3 18
# ASSIGN : n4 13
# ASSIGN : n5 11
# ASSIGN : n6 20
# ASSIGN : n7 4
# ASSIGN : n8 10
# ASSIGN : n9 8
# ASSIGN : n10 5
# ASSIGN : n11 21
# ASSIGN : n12 2
# ASSIGN : n13 22
# ASSIGN : n14 14
# ASSIGN : n15 1
# ASSIGN : n16 3
# ASSIGN : n17 19
# ASSIGN : n18 18
# ASSIGN : n19 5
# ASSIGN : n20 20
# ASSIGN : n21 10
# ASSIGN : n22 9
# ASSIGN : n23 4
# ASSIGN : n24 13
# ASSIGN : n25 11
# ASSIGN : n26 1
# ASSIGN : n27 9
# ASSIGN : n28 17
# ASSIGN : n29 7
# ASSIGN : n30 1
# ASSIGN : n31 10
# ASSIGN : n32 3
# ASSIGN : n33 4
# ASSIGN : n34 2
# ASSIGN : n35 17
# ASSIGN : n36 5
# ASSIGN : n37 13
# ASSIGN : n38 3
# ASSIGN : n39 10
# ASSIGN : n40 21
# ASSIGN : n41 11
# ASSIGN : n42 21
# ASSIGN : n43 2
# ASSIGN : n44 12
# ASSIGN : n45 11
# ASSIGN : n46 4
# ASSIGN : n47 7
# ASSIGN : n48 15
# ASSIGN : n49 6
# ASSIGN : n50 8
# ASSIGN : n51 14
# ASSIGN : n52 1
# ASSIGN : n53 6
# ASSIGN : n54 10
# ASSIGN : n55 21
# ASSIGN : n56 16
# ASSIGN : n57 9
# ASSIGN : n58 3
# ASSIGN : n59 21
# ASSIGN : n60 9
# ASSIGN : n61 13
# ASSIGN : n62 6
# ASSIGN : n63 10
# ASSIGN : n64 4
# ASSIGN : n65 16
# ASSIGN : n66 20
# ASSIGN : n67 2
# ASSIGN : n68 7
# ASSIGN : n69 1
# ASSIGN : n70 2
# ASSIGN : n71 14
# ASSIGN : n72 18
# ASSIGN : n73 16
# ASSIGN : n74 15
# ASSIGN : n75 5
# ASSIGN : n76 6
# ASSIGN : n77 9
# ASSIGN : n78 13
# ASSIGN : n79 3
# ASSIGN : n80 5
# ASSIGN : n81 21
# ASSIGN : n82 9
# ASSIGN : n83 13
# ASSIGN : n84 18
# ASSIGN : n85 5
# ASSIGN : n86 17
# ASSIGN : n87 2
# ASSIGN : n88 7
# ASSIGN : n89 4
# ASSIGN : n90 16
# ASSIGN : n91 12
# ASSIGN : n92 2
# ASSIGN : n93 7
# ASSIGN : n94 4
# ASSIGN : n95 16
# ASSIGN : n96 20
# ASSIGN : n97 13
# ASSIGN : n98 6
# ASSIGN : n99 3
# ASSIGN : n100 22
# ASSIGN : n101 5
# ASSIGN : n102 21
# ASSIGN : n103 9
# ASSIGN : n104 21
# ASSIGN : n105 10
# ASSIGN : n106 17
# ASSIGN : n107 11
# ASSIGN : n108 21
# ASSIGN : n109 9
# ASSIGN : n110 16
# ASSIGN : n111 14
# ASSIGN : n112 4
# ASSIGN : n113 5
# ASSIGN : n114 15
# ASSIGN : n115 2
# ASSIGN : n116 3
# ASSIGN : n117 2
# ASSIGN : n118 13
# ASSIGN : n119 2
# ASSIGN : n120 14
# ASSIGN : n121 5
# ASSIGN : n122 21
# ASSIGN : n123 13
# ASSIGN : n124 20
# ASSIGN : n125 16
# ASSIGN : n126 2
# ASSIGN : n127 1
# ASSIGN : n128 11
# ASSIGN : n129 10
# ASSIGN : n130 19
# ASSIGN : n131 7
# ASSIGN : n132 17
# ASSIGN : n133 3
# ASSIGN : n134 18
# ASSIGN : n135 8
# ASSIGN : n136 22
# ASSIGN : n137 21
# ASSIGN : n138 21
# ASSIGN : n139 7
# ASSIGN : n140 3
# ASSIGN : n141 1
# ASSIGN : n142 3
# ASSIGN : n143 11
# ASSIGN : n144 4
# ASSIGN : n145 16
# ASSIGN : n146 17
# ASSIGN : n147 5
# ASSIGN : n148 10
# ASSIGN : n149 21
# ASSIGN : n150 2
# ASSIGN : n151 19
# ASSIGN : n152 12
# ASSIGN : n153 21
# ASSIGN : n154 12
# ASSIGN : n155 10
# ASSIGN : n156 22
# ASSIGN : n157 2
# ASSIGN : n158 7
# ASSIGN : n159 1
# ASSIGN : n160 16
# ASSIGN : n161 11
# ASSIGN : n162 3
# ASSIGN : n163 6
# ASSIGN : n164 9
# ASSIGN : n165 2
# ASSIGN : n166 5
# ASSIGN : n167 17
# ASSIGN : n168 3
# ASSIGN : n169 13
# ASSIGN : n170 14
# ASSIGN : n171 10
# ASSIGN : n172 7
# ASSIGN : n173 1
# ASSIGN : n174 11
# ASSIGN : n175 4
# ASSIGN : n176 6
# ASSIGN : n177 8
# ASSIGN : n178 4
# ASSIGN : n179 16
# ASSIGN : n180 13
# ASSIGN : n181 6
# ASSIGN : n182 2
# ASSIGN : n183 12
# ASSIGN : n184 16
# ASSIGN : n185 5
# ASSIGN : n186 6
# ASSIGN : n187 5
# ASSIGN : n188 1
# ASSIGN : n189 7
# ASSIGN : n190 2
# ASSIGN : n191 4
# ASSIGN : n192 10
# ASSIGN : n193 22
# ASSIGN : n194 1
# ASSIGN : n195 2
# ASSIGN : n196 18
# ASSIGN : n197 1
# ASSIGN : n198 18
# ASSIGN : n199 17
# ASSIGN : n200 11
# ASSIGN : n201 4
# ASSIGN : n202 11
# ASSIGN : n203 14
# ASSIGN : n204 5
# ASSIGN : n205 21
# ASSIGN : n206 4
# ASSIGN : n207 16
# ASSIGN : n208 7
# ASSIGN : n209 1
# ASSIGN : n210 11
# ASSIGN : n211 4
# ASSIGN : n212 6
# ASSIGN : n213 9
# ASSIGN : n214 1
# ASSIGN : n215 8
# ASSIGN : n216 22
# ASSIGN : n217 13
# ASSIGN : n218 6
# ASSIGN : n219 9
# ASSIGN : n220 13
# ASSIGN : n221 8
# ASSIGN : n222 2
# ASSIGN : n223 7
# ASSIGN : n224 13
# ASSIGN : n225 17
# ASSIGN : n226 9
# ASSIGN : n227 16
# ASSIGN : n228 5
# ASSIGN : n229 3
# ASSIGN : n230 12
# ASSIGN : n231 5
# ASSIGN : n232 4
# ASSIGN : n233 9
# ASSIGN : n234 12
# ASSIGN : n235 1
# ASSIGN : n236 22
# ASSIGN : n237 1
# ASSIGN : n238 10
# ASSIGN : n239 1
# ASSIGN : n240 10
# ASSIGN : n241 22
# ASSIGN : n242 21
# ASSIGN : n243 3
# ASSIGN : n244 17
# ASSIGN : n245 5
# ASSIGN : n246 9
# ASSIGN : n247 2
# ASSIGN : n248 20
# ASSIGN : n249 1
# ASSIGN : n250 12
# ASSIGN : n251 13
# ASSIGN : n252 3
# ASSIGN : n253 10
# ASSIGN : n254 11
# ASSIGN : n255 16
# ASSIGN : n256 19
# ASSIGN : n257 3
# ASSIGN : n258 9
# ASSIGN : n259 11
# ASSIGN : n260 16
# ASSIGN : n261 12
# ASSIGN : n262 7
# ASSIGN : n263 1
# ASSIGN : n264 8
# ASSIGN : n265 6
# ASSIGN : n266 18
# ASSIGN : n267 2
# ASSIGN : n268 9
# ASSIGN : n269 7
# ASSIGN : n270 1
# ASSIGN : n271 2
# ASSIGN : n272 11
# ASSIGN : n273 16
# ASSIGN : n274 20
# ASSIGN : n275 13
# ASSIGN : n276 6
# ASSIGN : n277 13
# ASSIGN : n278 11
# ASSIGN : n279 16
# ASSIGN : n280 20
# ASSIGN : n281 13
# ASSIGN : n282 6
# ASSIGN : n283 19
# ASSIGN : n284 22
# ASSIGN : n285 22
# ASSIGN : n286 18
# ASSIGN : n287 21
# ASSIGN : n288 9
# ASSIGN : n289 8
# ASSIGN : n290 7
# ASSIGN : n291 3
# ASSIGN : n292 7
# ASSIGN : n293 3
# ASSIGN : n294 17
# ASSIGN : n295 9
# ASSIGN : n296 6
# ASSIGN : n297 1
# ASSIGN : n298 11
# ASSIGN : n299 21
# ASSIGN : n300 13
# ASSIGN : n301 10
# ASSIGN : n302 8
# ASSIGN : n303 5
# ASSIGN : n304 15
# ASSIGN : n305 12
# ASSIGN : n306 10
# ASSIGN : n307 9
# ASSIGN : n308 20
# ASSIGN : n309 20
# ASSIGN : n310 6
# ASSIGN : n311 4
# ASSIGN : n312 16
# ASSIGN : n313 20
# ASSIGN : n314 22
# ASSIGN : n315 22
# ASSIGN : n316 21
# ASSIGN : n317 21
# ASSIGN : n318 2
# ASSIGN : n319 1
# ASSIGN : n320 19
# ASSIGN : n321 15
# ASSIGN : n322 16
# ASSIGN : n323 17
# ASSIGN : n324 18
# ASSIGN : n325 13
# ASSIGN : n326 20
# ASSIGN : n327 17
# ASSIGN : n328 22
# ASSIGN : n329 12
# ASSIGN : n330 2
# ASSIGN : n331 8
# ASSIGN : n332 11
# ASSIGN : n333 4
# ASSIGN : n334 16
# ASSIGN : n335 11
# ASSIGN : n336 4
# ASSIGN : n337 16
# ASSIGN : n338 19
# ASSIGN : n339 17
# ASSIGN : n340 13
# ASSIGN : n341 15
# ASSIGN : n342 8
# ASSIGN : n343 9
# ASSIGN : n344 15
# ASSIGN : n345 21
# ASSIGN : n346 9
# ASSIGN : n347 17
# ASSIGN : n348 5
# ASSIGN : n349 6
# ASSIGN : n350 19
# ASSIGN : n351 15
# ASSIGN : n352 18
# ASSIGN : n353 8
# ASSIGN : n354 21
# ASSIGN : n355 22
# ASSIGN : n356 2
# ASSIGN : n357 15
# ASSIGN : n358 18
# ASSIGN : n359 16
# ASSIGN : n360 20
# ASSIGN : n361 22
# ASSIGN : n362 22
# ASSIGN : n363 19
# ASSIGN : n364 17
# ASSIGN : n365 5
# ASSIGN : n366 21
# ASSIGN : n367 2
# ASSIGN : n368 7
# ASSIGN : n369 1
# ASSIGN : n370 11
# ASSIGN : n371 4
# ASSIGN : n372 16
# ASSIGN : n373 22
# ASSIGN : n374 22
# ASSIGN : n375 10
# ASSIGN : n376 9
# ASSIGN : n377 14
# ASSIGN : n378 1
# ASSIGN : n379 22
# ASSIGN : n380 20
# ASSIGN : n381 21
# ASSIGN : n382 18
# ASSIGN : n383 19
# ASSIGN : n384 22
# ASSIGN : n385 12
SHOW_RESULT 22 END : 22 (0 seconds) [Mon Jul 10 21:14:42 2006]
SHOW_RESULT 22 CPU : 0.0600000000000023 = 0.0600000000000023 + 0 + 0 + 0

# BOUND : color 2 22

MODIFY_CNF 12 BEGIN :  [Mon Jul 10 21:14:42 2006]
MODIFY_CNF 12 END : 34121199 bytes (0 seconds) [Mon Jul 10 21:14:42 2006]
MODIFY_CNF 12 CPU : 0 = 0 + 0 + 0 + 0

VERIFY_CNF 12 BEGIN :  [Mon Jul 10 21:14:42 2006]
CMD : minisat /tmp/csp2sat28870.cnf /tmp/csp2sat28870.out
==================================[MINISAT]===================================
| Conflicts |     ORIGINAL     |              LEARNT              | Progress |
|           | Clauses Literals |   Limit Clauses Literals  Lit/Cl |          |
==============================================================================
|         0 |  507828  1529070 |  169276       0        0     nan |  0.000 % |
|       100 |  507828  1529070 |  186203     100     1710    17.1 | 23.086 % |
|       251 |  507828  1529070 |  204823     251     3222    12.8 | 23.086 % |
|       476 |  507828  1529070 |  225306     476     4937    10.4 | 23.086 % |
|       813 |  507828  1529070 |  247836     813     7570     9.3 | 23.086 % |
|      1320 |  507828  1529070 |  272620    1320    11716     8.9 | 23.086 % |
|      2079 |  507828  1529070 |  299882    2079    18057     8.7 | 23.086 % |
|      3220 |  507828  1529070 |  329871    3220    29463     9.2 | 23.086 % |
|      4929 |  507828  1529070 |  362858    4929    43313     8.8 | 23.086 % |
|      7491 |  507828  1529070 |  399143    7491    70647     9.4 | 23.086 % |
|     11337 |  507828  1529070 |  439058   11337   117774    10.4 | 23.086 % |
|     17103 |  507828  1529070 |  482964   17103   188127    11.0 | 23.086 % |
|     25752 |  507828  1529070 |  531260   25752   290137    11.3 | 23.086 % |
|     38726 |  507828  1529070 |  584386   38726   443950    11.5 | 23.086 % |
|     58188 |  507828  1529070 |  642825   58188   677742    11.6 | 23.086 % |
|     87382 |  507828  1529070 |  707107   87382  1018206    11.7 | 23.086 % |
|    131172 |  507829  1529070 |  777818  131171  1499311    11.4 | 23.086 % |
==============================================================================
restarts              : 17
conflicts             : 169027         (697 /sec)
decisions             : 194685         (803 /sec)
propagations          : 8514817        (35126 /sec)
conflict literals     : 1846533        (9.66 % deleted)
Memory used           : 65.29 MB
CPU time              : 242.41 s

UNSATISFIABLE
VERIFY_CNF 12 END :  (243 seconds) [Mon Jul 10 21:18:45 2006]
VERIFY_CNF 12 CPU : 242.76 = 0 + 0.01 + 242.41 + 0.34

# RESULT : color 12 UNSATISFIABLE
# BOUND : color 13 22

MODIFY_CNF 17 BEGIN :  [Mon Jul 10 21:18:45 2006]
MODIFY_CNF 17 END : 34121199 bytes (0 seconds) [Mon Jul 10 21:18:45 2006]
MODIFY_CNF 17 CPU : 0 = 0 + 0 + 0 + 0

VERIFY_CNF 17 BEGIN :  [Mon Jul 10 21:18:45 2006]
CMD : minisat /tmp/csp2sat28870.cnf /tmp/csp2sat28870.out
==================================[MINISAT]===================================
| Conflicts |     ORIGINAL     |              LEARNT              | Progress |
|           | Clauses Literals |   Limit Clauses Literals  Lit/Cl |          |
==============================================================================
|         0 |  698778  2101920 |  232926       0        0     nan |  0.000 % |
|       100 |  698778  2101920 |  256218     100     1217    12.2 | 19.588 % |
|       252 |  698778  2101920 |  281840     252     2232     8.9 | 19.588 % |
==============================================================================
restarts              : 3
conflicts             : 289            (22 /sec)
decisions             : 1188           (89 /sec)
propagations          : 192923         (14473 /sec)
conflict literals     : 2487           (12.18 % deleted)
Memory used           : 63.04 MB
CPU time              : 13.33 s

SATISFIABLE
VERIFY_CNF 17 END :  (13 seconds) [Mon Jul 10 21:18:58 2006]
VERIFY_CNF 17 CPU : 13.52 = 0 + 0.01 + 13.36 + 0.15

# RESULT : color 17 SATISFIABLE
SHOW_RESULT 17 BEGIN :  [Mon Jul 10 21:18:58 2006]
# ASSIGN : color 17
# ASSIGN : n1 16
# ASSIGN : n2 17
# ASSIGN : n3 8
# ASSIGN : n4 9
# ASSIGN : n5 1
# ASSIGN : n6 7
# ASSIGN : n7 10
# ASSIGN : n8 16
# ASSIGN : n9 13
# ASSIGN : n10 6
# ASSIGN : n11 3
# ASSIGN : n12 2
# ASSIGN : n13 11
# ASSIGN : n14 4
# ASSIGN : n15 16
# ASSIGN : n16 12
# ASSIGN : n17 13
# ASSIGN : n18 11
# ASSIGN : n19 6
# ASSIGN : n20 12
# ASSIGN : n21 13
# ASSIGN : n22 5
# ASSIGN : n23 10
# ASSIGN : n24 9
# ASSIGN : n25 1
# ASSIGN : n26 16
# ASSIGN : n27 17
# ASSIGN : n28 11
# ASSIGN : n29 4
# ASSIGN : n30 16
# ASSIGN : n31 13
# ASSIGN : n32 12
# ASSIGN : n33 10
# ASSIGN : n34 2
# ASSIGN : n35 8
# ASSIGN : n36 6
# ASSIGN : n37 9
# ASSIGN : n38 12
# ASSIGN : n39 13
# ASSIGN : n40 14
# ASSIGN : n41 1
# ASSIGN : n42 3
# ASSIGN : n43 2
# ASSIGN : n44 17
# ASSIGN : n45 1
# ASSIGN : n46 10
# ASSIGN : n47 4
# ASSIGN : n48 16
# ASSIGN : n49 1
# ASSIGN : n50 11
# ASSIGN : n51 4
# ASSIGN : n52 16
# ASSIGN : n53 12
# ASSIGN : n54 13
# ASSIGN : n55 3
# ASSIGN : n56 15
# ASSIGN : n57 16
# ASSIGN : n58 6
# ASSIGN : n59 3
# ASSIGN : n60 5
# ASSIGN : n61 9
# ASSIGN : n62 12
# ASSIGN : n63 13
# ASSIGN : n64 10
# ASSIGN : n65 15
# ASSIGN : n66 7
# ASSIGN : n67 2
# ASSIGN : n68 4
# ASSIGN : n69 16
# ASSIGN : n70 2
# ASSIGN : n71 4
# ASSIGN : n72 10
# ASSIGN : n73 15
# ASSIGN : n74 7
# ASSIGN : n75 6
# ASSIGN : n76 3
# ASSIGN : n77 14
# ASSIGN : n78 9
# ASSIGN : n79 12
# ASSIGN : n80 6
# ASSIGN : n81 14
# ASSIGN : n82 17
# ASSIGN : n83 9
# ASSIGN : n84 12
# ASSIGN : n85 6
# ASSIGN : n86 1
# ASSIGN : n87 2
# ASSIGN : n88 4
# ASSIGN : n89 10
# ASSIGN : n90 15
# ASSIGN : n91 7
# ASSIGN : n92 2
# ASSIGN : n93 4
# ASSIGN : n94 10
# ASSIGN : n95 15
# ASSIGN : n96 5
# ASSIGN : n97 9
# ASSIGN : n98 12
# ASSIGN : n99 7
# ASSIGN : n100 13
# ASSIGN : n101 6
# ASSIGN : n102 3
# ASSIGN : n103 14
# ASSIGN : n104 16
# ASSIGN : n105 8
# ASSIGN : n106 1
# ASSIGN : n107 11
# ASSIGN : n108 3
# ASSIGN : n109 5
# ASSIGN : n110 15
# ASSIGN : n111 7
# ASSIGN : n112 10
# ASSIGN : n113 6
# ASSIGN : n114 8
# ASSIGN : n115 2
# ASSIGN : n116 8
# ASSIGN : n117 2
# ASSIGN : n118 8
# ASSIGN : n119 9
# ASSIGN : n120 11
# ASSIGN : n121 6
# ASSIGN : n122 3
# ASSIGN : n123 9
# ASSIGN : n124 7
# ASSIGN : n125 15
# ASSIGN : n126 2
# ASSIGN : n127 16
# ASSIGN : n128 1
# ASSIGN : n129 13
# ASSIGN : n130 4
# ASSIGN : n131 12
# ASSIGN : n132 5
# ASSIGN : n133 12
# ASSIGN : n134 4
# ASSIGN : n135 12
# ASSIGN : n136 17
# ASSIGN : n137 16
# ASSIGN : n138 16
# ASSIGN : n139 4
# ASSIGN : n140 14
# ASSIGN : n141 17
# ASSIGN : n142 8
# ASSIGN : n143 1
# ASSIGN : n144 10
# ASSIGN : n145 15
# ASSIGN : n146 11
# ASSIGN : n147 6
# ASSIGN : n148 13
# ASSIGN : n149 3
# ASSIGN : n150 2
# ASSIGN : n151 12
# ASSIGN : n152 7
# ASSIGN : n153 3
# ASSIGN : n154 12
# ASSIGN : n155 13
# ASSIGN : n156 13
# ASSIGN : n157 2
# ASSIGN : n158 8
# ASSIGN : n159 16
# ASSIGN : n160 15
# ASSIGN : n161 1
# ASSIGN : n162 12
# ASSIGN : n163 17
# ASSIGN : n164 14
# ASSIGN : n165 2
# ASSIGN : n166 6
# ASSIGN : n167 11
# ASSIGN : n168 17
# ASSIGN : n169 9
# ASSIGN : n170 12
# ASSIGN : n171 8
# ASSIGN : n172 4
# ASSIGN : n173 16
# ASSIGN : n174 1
# ASSIGN : n175 10
# ASSIGN : n176 5
# ASSIGN : n177 11
# ASSIGN : n178 10
# ASSIGN : n179 15
# ASSIGN : n180 9
# ASSIGN : n181 3
# ASSIGN : n182 2
# ASSIGN : n183 7
# ASSIGN : n184 15
# ASSIGN : n185 1
# ASSIGN : n186 5
# ASSIGN : n187 4
# ASSIGN : n188 2
# ASSIGN : n189 4
# ASSIGN : n190 17
# ASSIGN : n191 10
# ASSIGN : n192 13
# ASSIGN : n193 1
# ASSIGN : n194 2
# ASSIGN : n195 3
# ASSIGN : n196 11
# ASSIGN : n197 16
# ASSIGN : n198 11
# ASSIGN : n199 11
# ASSIGN : n200 1
# ASSIGN : n201 10
# ASSIGN : n202 1
# ASSIGN : n203 12
# ASSIGN : n204 6
# ASSIGN : n205 3
# ASSIGN : n206 10
# ASSIGN : n207 15
# ASSIGN : n208 4
# ASSIGN : n209 16
# ASSIGN : n210 1
# ASSIGN : n211 10
# ASSIGN : n212 3
# ASSIGN : n213 5
# ASSIGN : n214 16
# ASSIGN : n215 15
# ASSIGN : n216 12
# ASSIGN : n217 9
# ASSIGN : n218 3
# ASSIGN : n219 14
# ASSIGN : n220 9
# ASSIGN : n221 7
# ASSIGN : n222 2
# ASSIGN : n223 4
# ASSIGN : n224 9
# ASSIGN : n225 12
# ASSIGN : n226 14
# ASSIGN : n227 15
# ASSIGN : n228 6
# ASSIGN : n229 2
# ASSIGN : n230 7
# ASSIGN : n231 6
# ASSIGN : n232 10
# ASSIGN : n233 5
# ASSIGN : n234 7
# ASSIGN : n235 8
# ASSIGN : n236 15
# ASSIGN : n237 16
# ASSIGN : n238 13
# ASSIGN : n239 16
# ASSIGN : n240 13
# ASSIGN : n241 17
# ASSIGN : n242 3
# ASSIGN : n243 13
# ASSIGN : n244 11
# ASSIGN : n245 17
# ASSIGN : n246 5
# ASSIGN : n247 2
# ASSIGN : n248 4
# ASSIGN : n249 16
# ASSIGN : n250 7
# ASSIGN : n251 9
# ASSIGN : n252 12
# ASSIGN : n253 13
# ASSIGN : n254 1
# ASSIGN : n255 15
# ASSIGN : n256 11
# ASSIGN : n257 3
# ASSIGN : n258 17
# ASSIGN : n259 1
# ASSIGN : n260 15
# ASSIGN : n261 5
# ASSIGN : n262 4
# ASSIGN : n263 16
# ASSIGN : n264 12
# ASSIGN : n265 13
# ASSIGN : n266 11
# ASSIGN : n267 2
# ASSIGN : n268 5
# ASSIGN : n269 4
# ASSIGN : n270 16
# ASSIGN : n271 2
# ASSIGN : n272 1
# ASSIGN : n273 15
# ASSIGN : n274 7
# ASSIGN : n275 9
# ASSIGN : n276 12
# ASSIGN : n277 9
# ASSIGN : n278 1
# ASSIGN : n279 15
# ASSIGN : n280 7
# ASSIGN : n281 9
# ASSIGN : n282 12
# ASSIGN : n283 13
# ASSIGN : n284 17
# ASSIGN : n285 16
# ASSIGN : n286 11
# ASSIGN : n287 3
# ASSIGN : n288 5
# ASSIGN : n289 2
# ASSIGN : n290 4
# ASSIGN : n291 6
# ASSIGN : n292 4
# ASSIGN : n293 12
# ASSIGN : n294 11
# ASSIGN : n295 5
# ASSIGN : n296 3
# ASSIGN : n297 16
# ASSIGN : n298 1
# ASSIGN : n299 15
# ASSIGN : n300 9
# ASSIGN : n301 13
# ASSIGN : n302 11
# ASSIGN : n303 6
# ASSIGN : n304 16
# ASSIGN : n305 7
# ASSIGN : n306 13
# ASSIGN : n307 5
# ASSIGN : n308 4
# ASSIGN : n309 4
# ASSIGN : n310 1
# ASSIGN : n311 10
# ASSIGN : n312 8
# ASSIGN : n313 15
# ASSIGN : n314 17
# ASSIGN : n315 17
# ASSIGN : n316 17
# ASSIGN : n317 15
# ASSIGN : n318 2
# ASSIGN : n319 16
# ASSIGN : n320 1
# ASSIGN : n321 10
# ASSIGN : n322 3
# ASSIGN : n323 8
# ASSIGN : n324 6
# ASSIGN : n325 9
# ASSIGN : n326 5
# ASSIGN : n327 8
# ASSIGN : n328 3
# ASSIGN : n329 7
# ASSIGN : n330 2
# ASSIGN : n331 11
# ASSIGN : n332 1
# ASSIGN : n333 10
# ASSIGN : n334 15
# ASSIGN : n335 1
# ASSIGN : n336 10
# ASSIGN : n337 15
# ASSIGN : n338 12
# ASSIGN : n339 8
# ASSIGN : n340 9
# ASSIGN : n341 6
# ASSIGN : n342 14
# ASSIGN : n343 5
# ASSIGN : n344 6
# ASSIGN : n345 8
# ASSIGN : n346 14
# ASSIGN : n347 11
# ASSIGN : n348 6
# ASSIGN : n349 3
# ASSIGN : n350 1
# ASSIGN : n351 7
# ASSIGN : n352 10
# ASSIGN : n353 6
# ASSIGN : n354 15
# ASSIGN : n355 17
# ASSIGN : n356 8
# ASSIGN : n357 14
# ASSIGN : n358 17
# ASSIGN : n359 15
# ASSIGN : n360 17
# ASSIGN : n361 14
# ASSIGN : n362 17
# ASSIGN : n363 13
# ASSIGN : n364 11
# ASSIGN : n365 6
# ASSIGN : n366 3
# ASSIGN : n367 2
# ASSIGN : n368 4
# ASSIGN : n369 16
# ASSIGN : n370 1
# ASSIGN : n371 10
# ASSIGN : n372 15
# ASSIGN : n373 9
# ASSIGN : n374 12
# ASSIGN : n375 13
# ASSIGN : n376 17
# ASSIGN : n377 17
# ASSIGN : n378 16
# ASSIGN : n379 13
# ASSIGN : n380 2
# ASSIGN : n381 8
# ASSIGN : n382 15
# ASSIGN : n383 14
# ASSIGN : n384 7
# ASSIGN : n385 7
SHOW_RESULT 17 END : 17 (0 seconds) [Mon Jul 10 21:18:58 2006]
SHOW_RESULT 17 CPU : 0.0600000000000023 = 0.0600000000000023 + 0 + 0 + 0

# BOUND : color 13 17

MODIFY_CNF 15 BEGIN :  [Mon Jul 10 21:18:58 2006]
MODIFY_CNF 15 END : 34121199 bytes (0 seconds) [Mon Jul 10 21:18:58 2006]
MODIFY_CNF 15 CPU : 0 = 0 + 0 + 0 + 0

VERIFY_CNF 15 BEGIN :  [Mon Jul 10 21:18:58 2006]
CMD : minisat /tmp/csp2sat28870.cnf /tmp/csp2sat28870.out
==================================[MINISAT]===================================
| Conflicts |     ORIGINAL     |              LEARNT              | Progress |
|           | Clauses Literals |   Limit Clauses Literals  Lit/Cl |          |
==============================================================================
|         0 |  622398  1872780 |  207466       0        0     nan |  0.000 % |
|       101 |  622398  1872780 |  228212     101     1303    12.9 | 20.987 % |
|       251 |  622398  1872780 |  251033     251     2715    10.8 | 20.987 % |
==============================================================================
restarts              : 3
conflicts             : 312            (10 /sec)
decisions             : 967            (32 /sec)
propagations          : 253083         (8487 /sec)
conflict literals     : 3351           (13.01 % deleted)
Memory used           : 63.05 MB
CPU time              : 29.82 s

SATISFIABLE
VERIFY_CNF 15 END :  (31 seconds) [Mon Jul 10 21:19:29 2006]
VERIFY_CNF 15 CPU : 30.07 = 0 + 0.01 + 29.85 + 0.21

# RESULT : color 15 SATISFIABLE
SHOW_RESULT 15 BEGIN :  [Mon Jul 10 21:19:29 2006]
# ASSIGN : color 15
# ASSIGN : n1 7
# ASSIGN : n2 14
# ASSIGN : n3 5
# ASSIGN : n4 15
# ASSIGN : n5 6
# ASSIGN : n6 4
# ASSIGN : n7 3
# ASSIGN : n8 7
# ASSIGN : n9 8
# ASSIGN : n10 13
# ASSIGN : n11 14
# ASSIGN : n12 2
# ASSIGN : n13 1
# ASSIGN : n14 12
# ASSIGN : n15 7
# ASSIGN : n16 10
# ASSIGN : n17 8
# ASSIGN : n18 5
# ASSIGN : n19 13
# ASSIGN : n20 10
# ASSIGN : n21 8
# ASSIGN : n22 9
# ASSIGN : n23 3
# ASSIGN : n24 15
# ASSIGN : n25 6
# ASSIGN : n26 7
# ASSIGN : n27 9
# ASSIGN : n28 5
# ASSIGN : n29 12
# ASSIGN : n30 7
# ASSIGN : n31 8
# ASSIGN : n32 10
# ASSIGN : n33 3
# ASSIGN : n34 2
# ASSIGN : n35 5
# ASSIGN : n36 13
# ASSIGN : n37 15
# ASSIGN : n38 10
# ASSIGN : n39 8
# ASSIGN : n40 13
# ASSIGN : n41 6
# ASSIGN : n42 14
# ASSIGN : n43 2
# ASSIGN : n44 11
# ASSIGN : n45 6
# ASSIGN : n46 3
# ASSIGN : n47 12
# ASSIGN : n48 7
# ASSIGN : n49 6
# ASSIGN : n50 5
# ASSIGN : n51 12
# ASSIGN : n52 7
# ASSIGN : n53 10
# ASSIGN : n54 8
# ASSIGN : n55 14
# ASSIGN : n56 1
# ASSIGN : n57 7
# ASSIGN : n58 13
# ASSIGN : n59 14
# ASSIGN : n60 9
# ASSIGN : n61 15
# ASSIGN : n62 10
# ASSIGN : n63 11
# ASSIGN : n64 3
# ASSIGN : n65 1
# ASSIGN : n66 4
# ASSIGN : n67 2
# ASSIGN : n68 12
# ASSIGN : n69 7
# ASSIGN : n70 2
# ASSIGN : n71 12
# ASSIGN : n72 3
# ASSIGN : n73 1
# ASSIGN : n74 4
# ASSIGN : n75 13
# ASSIGN : n76 14
# ASSIGN : n77 9
# ASSIGN : n78 15
# ASSIGN : n79 10
# ASSIGN : n80 13
# ASSIGN : n81 14
# ASSIGN : n82 9
# ASSIGN : n83 15
# ASSIGN : n84 10
# ASSIGN : n85 13
# ASSIGN : n86 1
# ASSIGN : n87 2
# ASSIGN : n88 12
# ASSIGN : n89 3
# ASSIGN : n90 1
# ASSIGN : n91 4
# ASSIGN : n92 2
# ASSIGN : n93 12
# ASSIGN : n94 11
# ASSIGN : n95 1
# ASSIGN : n96 4
# ASSIGN : n97 15
# ASSIGN : n98 10
# ASSIGN : n99 1
# ASSIGN : n100 8
# ASSIGN : n101 13
# ASSIGN : n102 14
# ASSIGN : n103 9
# ASSIGN : n104 14
# ASSIGN : n105 3
# ASSIGN : n106 5
# ASSIGN : n107 6
# ASSIGN : n108 14
# ASSIGN : n109 9
# ASSIGN : n110 1
# ASSIGN : n111 4
# ASSIGN : n112 13
# ASSIGN : n113 3
# ASSIGN : n114 2
# ASSIGN : n115 5
# ASSIGN : n116 2
# ASSIGN : n117 15
# ASSIGN : n118 2
# ASSIGN : n119 15
# ASSIGN : n120 5
# ASSIGN : n121 13
# ASSIGN : n122 14
# ASSIGN : n123 15
# ASSIGN : n124 4
# ASSIGN : n125 1
# ASSIGN : n126 2
# ASSIGN : n127 7
# ASSIGN : n128 6
# ASSIGN : n129 8
# ASSIGN : n130 12
# ASSIGN : n131 10
# ASSIGN : n132 12
# ASSIGN : n133 11
# ASSIGN : n134 12
# ASSIGN : n135 10
# ASSIGN : n136 15
# ASSIGN : n137 14
# ASSIGN : n138 14
# ASSIGN : n139 12
# ASSIGN : n140 2
# ASSIGN : n141 11
# ASSIGN : n142 12
# ASSIGN : n143 6
# ASSIGN : n144 3
# ASSIGN : n145 1
# ASSIGN : n146 5
# ASSIGN : n147 13
# ASSIGN : n148 8
# ASSIGN : n149 14
# ASSIGN : n150 2
# ASSIGN : n151 10
# ASSIGN : n152 4
# ASSIGN : n153 14
# ASSIGN : n154 10
# ASSIGN : n155 8
# ASSIGN : n156 8
# ASSIGN : n157 2
# ASSIGN : n158 12
# ASSIGN : n159 7
# ASSIGN : n160 1
# ASSIGN : n161 6
# ASSIGN : n162 4
# ASSIGN : n163 14
# ASSIGN : n164 9
# ASSIGN : n165 2
# ASSIGN : n166 13
# ASSIGN : n167 5
# ASSIGN : n168 7
# ASSIGN : n169 15
# ASSIGN : n170 10
# ASSIGN : n171 8
# ASSIGN : n172 12
# ASSIGN : n173 7
# ASSIGN : n174 6
# ASSIGN : n175 3
# ASSIGN : n176 10
# ASSIGN : n177 5
# ASSIGN : n178 3
# ASSIGN : n179 1
# ASSIGN : n180 15
# ASSIGN : n181 14
# ASSIGN : n182 2
# ASSIGN : n183 4
# ASSIGN : n184 1
# ASSIGN : n185 4
# ASSIGN : n186 9
# ASSIGN : n187 2
# ASSIGN : n188 5
# ASSIGN : n189 12
# ASSIGN : n190 2
# ASSIGN : n191 3
# ASSIGN : n192 8
# ASSIGN : n193 6
# ASSIGN : n194 7
# ASSIGN : n195 8
# ASSIGN : n196 5
# ASSIGN : n197 7
# ASSIGN : n198 5
# ASSIGN : n199 5
# ASSIGN : n200 6
# ASSIGN : n201 3
# ASSIGN : n202 6
# ASSIGN : n203 10
# ASSIGN : n204 13
# ASSIGN : n205 14
# ASSIGN : n206 3
# ASSIGN : n207 1
# ASSIGN : n208 12
# ASSIGN : n209 7
# ASSIGN : n210 6
# ASSIGN : n211 3
# ASSIGN : n212 14
# ASSIGN : n213 9
# ASSIGN : n214 7
# ASSIGN : n215 1
# ASSIGN : n216 10
# ASSIGN : n217 15
# ASSIGN : n218 14
# ASSIGN : n219 9
# ASSIGN : n220 15
# ASSIGN : n221 4
# ASSIGN : n222 2
# ASSIGN : n223 12
# ASSIGN : n224 15
# ASSIGN : n225 10
# ASSIGN : n226 9
# ASSIGN : n227 1
# ASSIGN : n228 13
# ASSIGN : n229 7
# ASSIGN : n230 4
# ASSIGN : n231 13
# ASSIGN : n232 3
# ASSIGN : n233 9
# ASSIGN : n234 4
# ASSIGN : n235 7
# ASSIGN : n236 15
# ASSIGN : n237 7
# ASSIGN : n238 8
# ASSIGN : n239 7
# ASSIGN : n240 8
# ASSIGN : n241 15
# ASSIGN : n242 14
# ASSIGN : n243 8
# ASSIGN : n244 11
# ASSIGN : n245 13
# ASSIGN : n246 9
# ASSIGN : n247 2
# ASSIGN : n248 12
# ASSIGN : n249 7
# ASSIGN : n250 4
# ASSIGN : n251 15
# ASSIGN : n252 10
# ASSIGN : n253 8
# ASSIGN : n254 6
# ASSIGN : n255 1
# ASSIGN : n256 5
# ASSIGN : n257 14
# ASSIGN : n258 9
# ASSIGN : n259 6
# ASSIGN : n260 1
# ASSIGN : n261 4
# ASSIGN : n262 12
# ASSIGN : n263 7
# ASSIGN : n264 10
# ASSIGN : n265 8
# ASSIGN : n266 5
# ASSIGN : n267 2
# ASSIGN : n268 9
# ASSIGN : n269 12
# ASSIGN : n270 7
# ASSIGN : n271 2
# ASSIGN : n272 6
# ASSIGN : n273 1
# ASSIGN : n274 4
# ASSIGN : n275 15
# ASSIGN : n276 10
# ASSIGN : n277 15
# ASSIGN : n278 6
# ASSIGN : n279 1
# ASSIGN : n280 4
# ASSIGN : n281 15
# ASSIGN : n282 10
# ASSIGN : n283 8
# ASSIGN : n284 15
# ASSIGN : n285 14
# ASSIGN : n286 5
# ASSIGN : n287 14
# ASSIGN : n288 9
# ASSIGN : n289 2
# ASSIGN : n290 12
# ASSIGN : n291 13
# ASSIGN : n292 12
# ASSIGN : n293 10
# ASSIGN : n294 5
# ASSIGN : n295 9
# ASSIGN : n296 14
# ASSIGN : n297 7
# ASSIGN : n298 6
# ASSIGN : n299 1
# ASSIGN : n300 15
# ASSIGN : n301 8
# ASSIGN : n302 5
# ASSIGN : n303 13
# ASSIGN : n304 7
# ASSIGN : n305 4
# ASSIGN : n306 8
# ASSIGN : n307 9
# ASSIGN : n308 11
# ASSIGN : n309 2
# ASSIGN : n310 6
# ASSIGN : n311 3
# ASSIGN : n312 1
# ASSIGN : n313 14
# ASSIGN : n314 15
# ASSIGN : n315 15
# ASSIGN : n316 15
# ASSIGN : n317 1
# ASSIGN : n318 2
# ASSIGN : n319 7
# ASSIGN : n320 6
# ASSIGN : n321 3
# ASSIGN : n322 14
# ASSIGN : n323 5
# ASSIGN : n324 13
# ASSIGN : n325 15
# ASSIGN : n326 4
# ASSIGN : n327 5
# ASSIGN : n328 15
# ASSIGN : n329 4
# ASSIGN : n330 2
# ASSIGN : n331 5
# ASSIGN : n332 6
# ASSIGN : n333 3
# ASSIGN : n334 1
# ASSIGN : n335 6
# ASSIGN : n336 3
# ASSIGN : n337 1
# ASSIGN : n338 10
# ASSIGN : n339 5
# ASSIGN : n340 15
# ASSIGN : n341 13
# ASSIGN : n342 14
# ASSIGN : n343 9
# ASSIGN : n344 13
# ASSIGN : n345 14
# ASSIGN : n346 9
# ASSIGN : n347 11
# ASSIGN : n348 13
# ASSIGN : n349 14
# ASSIGN : n350 6
# ASSIGN : n351 4
# ASSIGN : n352 3
# ASSIGN : n353 13
# ASSIGN : n354 15
# ASSIGN : n355 11
# ASSIGN : n356 2
# ASSIGN : n357 12
# ASSIGN : n358 11
# ASSIGN : n359 11
# ASSIGN : n360 11
# ASSIGN : n361 15
# ASSIGN : n362 12
# ASSIGN : n363 11
# ASSIGN : n364 5
# ASSIGN : n365 13
# ASSIGN : n366 14
# ASSIGN : n367 2
# ASSIGN : n368 12
# ASSIGN : n369 7
# ASSIGN : n370 6
# ASSIGN : n371 3
# ASSIGN : n372 1
# ASSIGN : n373 15
# ASSIGN : n374 10
# ASSIGN : n375 8
# ASSIGN : n376 11
# ASSIGN : n377 9
# ASSIGN : n378 7
# ASSIGN : n379 13
# ASSIGN : n380 2
# ASSIGN : n381 11
# ASSIGN : n382 12
# ASSIGN : n383 15
# ASSIGN : n384 4
# ASSIGN : n385 4
SHOW_RESULT 15 END : 15 (0 seconds) [Mon Jul 10 21:19:29 2006]
SHOW_RESULT 15 CPU : 0.0500000000000114 = 0.0500000000000114 + 0 + 0 + 0

# BOUND : color 13 15

MODIFY_CNF 14 BEGIN :  [Mon Jul 10 21:19:29 2006]
MODIFY_CNF 14 END : 34121199 bytes (0 seconds) [Mon Jul 10 21:19:29 2006]
MODIFY_CNF 14 CPU : 0 = 0 + 0 + 0 + 0

VERIFY_CNF 14 BEGIN :  [Mon Jul 10 21:19:29 2006]
CMD : minisat /tmp/csp2sat28870.cnf /tmp/csp2sat28870.out
==================================[MINISAT]===================================
| Conflicts |     ORIGINAL     |              LEARNT              | Progress |
|           | Clauses Literals |   Limit Clauses Literals  Lit/Cl |          |
==============================================================================
|         0 |  584208  1758210 |  194736       0        0     nan |  0.000 % |
|       100 |  584208  1758210 |  214209     100     1080    10.8 | 21.687 % |
|       251 |  584208  1758210 |  235630     251     2199     8.8 | 21.687 % |
==============================================================================
restarts              : 3
conflicts             : 325            (19 /sec)
decisions             : 876            (51 /sec)
propagations          : 196783         (11481 /sec)
conflict literals     : 2701           (12.90 % deleted)
Memory used           : 63.05 MB
CPU time              : 17.14 s

SATISFIABLE
VERIFY_CNF 14 END :  (17 seconds) [Mon Jul 10 21:19:46 2006]
VERIFY_CNF 14 CPU : 17.31 = 0 + 0.01 + 17.17 + 0.13

# RESULT : color 14 SATISFIABLE
SHOW_RESULT 14 BEGIN :  [Mon Jul 10 21:19:46 2006]
# ASSIGN : color 14
# ASSIGN : n1 8
# ASSIGN : n2 2
# ASSIGN : n3 6
# ASSIGN : n4 1
# ASSIGN : n5 12
# ASSIGN : n6 13
# ASSIGN : n7 14
# ASSIGN : n8 8
# ASSIGN : n9 5
# ASSIGN : n10 10
# ASSIGN : n11 11
# ASSIGN : n12 4
# ASSIGN : n13 7
# ASSIGN : n14 9
# ASSIGN : n15 8
# ASSIGN : n16 2
# ASSIGN : n17 5
# ASSIGN : n18 6
# ASSIGN : n19 10
# ASSIGN : n20 2
# ASSIGN : n21 5
# ASSIGN : n22 7
# ASSIGN : n23 14
# ASSIGN : n24 1
# ASSIGN : n25 12
# ASSIGN : n26 8
# ASSIGN : n27 7
# ASSIGN : n28 6
# ASSIGN : n29 9
# ASSIGN : n30 8
# ASSIGN : n31 5
# ASSIGN : n32 2
# ASSIGN : n33 14
# ASSIGN : n34 4
# ASSIGN : n35 6
# ASSIGN : n36 10
# ASSIGN : n37 1
# ASSIGN : n38 2
# ASSIGN : n39 5
# ASSIGN : n40 11
# ASSIGN : n41 12
# ASSIGN : n42 11
# ASSIGN : n43 4
# ASSIGN : n44 12
# ASSIGN : n45 12
# ASSIGN : n46 14
# ASSIGN : n47 9
# ASSIGN : n48 8
# ASSIGN : n49 12
# ASSIGN : n50 6
# ASSIGN : n51 9
# ASSIGN : n52 8
# ASSIGN : n53 2
# ASSIGN : n54 5
# ASSIGN : n55 11
# ASSIGN : n56 3
# ASSIGN : n57 8
# ASSIGN : n58 10
# ASSIGN : n59 11
# ASSIGN : n60 7
# ASSIGN : n61 1
# ASSIGN : n62 2
# ASSIGN : n63 5
# ASSIGN : n64 14
# ASSIGN : n65 3
# ASSIGN : n66 13
# ASSIGN : n67 4
# ASSIGN : n68 9
# ASSIGN : n69 8
# ASSIGN : n70 4
# ASSIGN : n71 9
# ASSIGN : n72 14
# ASSIGN : n73 3
# ASSIGN : n74 13
# ASSIGN : n75 10
# ASSIGN : n76 11
# ASSIGN : n77 7
# ASSIGN : n78 1
# ASSIGN : n79 2
# ASSIGN : n80 10
# ASSIGN : n81 11
# ASSIGN : n82 7
# ASSIGN : n83 1
# ASSIGN : n84 2
# ASSIGN : n85 10
# ASSIGN : n86 3
# ASSIGN : n87 4
# ASSIGN : n88 9
# ASSIGN : n89 14
# ASSIGN : n90 3
# ASSIGN : n91 13
# ASSIGN : n92 4
# ASSIGN : n93 9
# ASSIGN : n94 14
# ASSIGN : n95 3
# ASSIGN : n96 13
# ASSIGN : n97 1
# ASSIGN : n98 2
# ASSIGN : n99 3
# ASSIGN : n100 5
# ASSIGN : n101 10
# ASSIGN : n102 11
# ASSIGN : n103 7
# ASSIGN : n104 13
# ASSIGN : n105 8
# ASSIGN : n106 12
# ASSIGN : n107 6
# ASSIGN : n108 11
# ASSIGN : n109 7
# ASSIGN : n110 3
# ASSIGN : n111 13
# ASSIGN : n112 14
# ASSIGN : n113 10
# ASSIGN : n114 4
# ASSIGN : n115 1
# ASSIGN : n116 4
# ASSIGN : n117 1
# ASSIGN : n118 4
# ASSIGN : n119 1
# ASSIGN : n120 6
# ASSIGN : n121 10
# ASSIGN : n122 11
# ASSIGN : n123 1
# ASSIGN : n124 13
# ASSIGN : n125 3
# ASSIGN : n126 4
# ASSIGN : n127 8
# ASSIGN : n128 12
# ASSIGN : n129 5
# ASSIGN : n130 9
# ASSIGN : n131 2
# ASSIGN : n132 9
# ASSIGN : n133 2
# ASSIGN : n134 9
# ASSIGN : n135 2
# ASSIGN : n136 14
# ASSIGN : n137 13
# ASSIGN : n138 13
# ASSIGN : n139 9
# ASSIGN : n140 4
# ASSIGN : n141 13
# ASSIGN : n142 9
# ASSIGN : n143 12
# ASSIGN : n144 14
# ASSIGN : n145 3
# ASSIGN : n146 6
# ASSIGN : n147 10
# ASSIGN : n148 5
# ASSIGN : n149 11
# ASSIGN : n150 4
# ASSIGN : n151 2
# ASSIGN : n152 13
# ASSIGN : n153 11
# ASSIGN : n154 2
# ASSIGN : n155 5
# ASSIGN : n156 5
# ASSIGN : n157 4
# ASSIGN : n158 9
# ASSIGN : n159 8
# ASSIGN : n160 3
# ASSIGN : n161 12
# ASSIGN : n162 2
# ASSIGN : n163 11
# ASSIGN : n164 7
# ASSIGN : n165 4
# ASSIGN : n166 10
# ASSIGN : n167 6
# ASSIGN : n168 8
# ASSIGN : n169 1
# ASSIGN : n170 2
# ASSIGN : n171 5
# ASSIGN : n172 9
# ASSIGN : n173 8
# ASSIGN : n174 12
# ASSIGN : n175 14
# ASSIGN : n176 2
# ASSIGN : n177 6
# ASSIGN : n178 14
# ASSIGN : n179 3
# ASSIGN : n180 1
# ASSIGN : n181 11
# ASSIGN : n182 4
# ASSIGN : n183 13
# ASSIGN : n184 3
# ASSIGN : n185 4
# ASSIGN : n186 7
# ASSIGN : n187 9
# ASSIGN : n188 8
# ASSIGN : n189 9
# ASSIGN : n190 4
# ASSIGN : n191 14
# ASSIGN : n192 5
# ASSIGN : n193 13
# ASSIGN : n194 14
# ASSIGN : n195 5
# ASSIGN : n196 6
# ASSIGN : n197 8
# ASSIGN : n198 6
# ASSIGN : n199 6
# ASSIGN : n200 12
# ASSIGN : n201 14
# ASSIGN : n202 12
# ASSIGN : n203 2
# ASSIGN : n204 10
# ASSIGN : n205 11
# ASSIGN : n206 14
# ASSIGN : n207 3
# ASSIGN : n208 9
# ASSIGN : n209 8
# ASSIGN : n210 12
# ASSIGN : n211 14
# ASSIGN : n212 11
# ASSIGN : n213 7
# ASSIGN : n214 8
# ASSIGN : n215 3
# ASSIGN : n216 2
# ASSIGN : n217 1
# ASSIGN : n218 11
# ASSIGN : n219 7
# ASSIGN : n220 1
# ASSIGN : n221 13
# ASSIGN : n222 4
# ASSIGN : n223 9
# ASSIGN : n224 1
# ASSIGN : n225 2
# ASSIGN : n226 7
# ASSIGN : n227 3
# ASSIGN : n228 10
# ASSIGN : n229 8
# ASSIGN : n230 13
# ASSIGN : n231 10
# ASSIGN : n232 14
# ASSIGN : n233 7
# ASSIGN : n234 13
# ASSIGN : n235 8
# ASSIGN : n236 7
# ASSIGN : n237 8
# ASSIGN : n238 5
# ASSIGN : n239 8
# ASSIGN : n240 5
# ASSIGN : n241 14
# ASSIGN : n242 11
# ASSIGN : n243 5
# ASSIGN : n244 6
# ASSIGN : n245 10
# ASSIGN : n246 7
# ASSIGN : n247 4
# ASSIGN : n248 9
# ASSIGN : n249 8
# ASSIGN : n250 13
# ASSIGN : n251 1
# ASSIGN : n252 2
# ASSIGN : n253 5
# ASSIGN : n254 12
# ASSIGN : n255 3
# ASSIGN : n256 6
# ASSIGN : n257 11
# ASSIGN : n258 7
# ASSIGN : n259 12
# ASSIGN : n260 3
# ASSIGN : n261 13
# ASSIGN : n262 9
# ASSIGN : n263 8
# ASSIGN : n264 2
# ASSIGN : n265 5
# ASSIGN : n266 6
# ASSIGN : n267 4
# ASSIGN : n268 7
# ASSIGN : n269 9
# ASSIGN : n270 8
# ASSIGN : n271 4
# ASSIGN : n272 12
# ASSIGN : n273 3
# ASSIGN : n274 13
# ASSIGN : n275 1
# ASSIGN : n276 2
# ASSIGN : n277 1
# ASSIGN : n278 12
# ASSIGN : n279 3
# ASSIGN : n280 13
# ASSIGN : n281 1
# ASSIGN : n282 2
# ASSIGN : n283 5
# ASSIGN : n284 14
# ASSIGN : n285 13
# ASSIGN : n286 6
# ASSIGN : n287 11
# ASSIGN : n288 7
# ASSIGN : n289 4
# ASSIGN : n290 9
# ASSIGN : n291 10
# ASSIGN : n292 9
# ASSIGN : n293 2
# ASSIGN : n294 6
# ASSIGN : n295 7
# ASSIGN : n296 11
# ASSIGN : n297 8
# ASSIGN : n298 12
# ASSIGN : n299 3
# ASSIGN : n300 1
# ASSIGN : n301 5
# ASSIGN : n302 6
# ASSIGN : n303 10
# ASSIGN : n304 8
# ASSIGN : n305 13
# ASSIGN : n306 5
# ASSIGN : n307 7
# ASSIGN : n308 9
# ASSIGN : n309 2
# ASSIGN : n310 12
# ASSIGN : n311 14
# ASSIGN : n312 3
# ASSIGN : n313 12
# ASSIGN : n314 14
# ASSIGN : n315 14
# ASSIGN : n316 14
# ASSIGN : n317 3
# ASSIGN : n318 4
# ASSIGN : n319 8
# ASSIGN : n320 12
# ASSIGN : n321 14
# ASSIGN : n322 11
# ASSIGN : n323 6
# ASSIGN : n324 10
# ASSIGN : n325 1
# ASSIGN : n326 13
# ASSIGN : n327 6
# ASSIGN : n328 1
# ASSIGN : n329 13
# ASSIGN : n330 4
# ASSIGN : n331 6
# ASSIGN : n332 12
# ASSIGN : n333 14
# ASSIGN : n334 3
# ASSIGN : n335 12
# ASSIGN : n336 14
# ASSIGN : n337 3
# ASSIGN : n338 2
# ASSIGN : n339 6
# ASSIGN : n340 1
# ASSIGN : n341 10
# ASSIGN : n342 11
# ASSIGN : n343 7
# ASSIGN : n344 10
# ASSIGN : n345 11
# ASSIGN : n346 7
# ASSIGN : n347 6
# ASSIGN : n348 10
# ASSIGN : n349 11
# ASSIGN : n350 12
# ASSIGN : n351 13
# ASSIGN : n352 14
# ASSIGN : n353 10
# ASSIGN : n354 12
# ASSIGN : n355 7
# ASSIGN : n356 4
# ASSIGN : n357 9
# ASSIGN : n358 14
# ASSIGN : n359 3
# ASSIGN : n360 13
# ASSIGN : n361 1
# ASSIGN : n362 4
# ASSIGN : n363 5
# ASSIGN : n364 6
# ASSIGN : n365 10
# ASSIGN : n366 11
# ASSIGN : n367 4
# ASSIGN : n368 9
# ASSIGN : n369 8
# ASSIGN : n370 12
# ASSIGN : n371 14
# ASSIGN : n372 3
# ASSIGN : n373 1
# ASSIGN : n374 2
# ASSIGN : n375 5
# ASSIGN : n376 7
# ASSIGN : n377 7
# ASSIGN : n378 8
# ASSIGN : n379 14
# ASSIGN : n380 4
# ASSIGN : n381 9
# ASSIGN : n382 12
# ASSIGN : n383 13
# ASSIGN : n384 13
# ASSIGN : n385 13
SHOW_RESULT 14 END : 14 (0 seconds) [Mon Jul 10 21:19:46 2006]
SHOW_RESULT 14 CPU : 0.0600000000000023 = 0.0600000000000023 + 0 + 0 + 0

# BOUND : color 13 14

MODIFY_CNF 13 BEGIN :  [Mon Jul 10 21:19:46 2006]
MODIFY_CNF 13 END : 34121199 bytes (0 seconds) [Mon Jul 10 21:19:46 2006]
MODIFY_CNF 13 CPU : 0 = 0 + 0 + 0 + 0

VERIFY_CNF 13 BEGIN :  [Mon Jul 10 21:19:46 2006]
CMD : minisat /tmp/csp2sat28870.cnf /tmp/csp2sat28870.out
==================================[MINISAT]===================================
| Conflicts |     ORIGINAL     |              LEARNT              | Progress |
|           | Clauses Literals |   Limit Clauses Literals  Lit/Cl |          |
==============================================================================
|         0 |  546018  1643640 |  182006       0        0     nan |  0.000 % |
|       100 |  546018  1643640 |  200206     100     1321    13.2 | 22.386 % |
|       251 |  546018  1643640 |  220227     251     2940    11.7 | 22.386 % |
|       476 |  546018  1643640 |  242249     476     4478     9.4 | 22.386 % |
|       815 |  546018  1643640 |  266474     815     8146    10.0 | 22.386 % |
|      1322 |  546018  1643640 |  293122    1322    12576     9.5 | 22.386 % |
|      2082 |  546018  1643640 |  322434    2082    21758    10.5 | 22.386 % |
|      3223 |  546018  1643640 |  354678    3223    30502     9.5 | 22.386 % |
|      4931 |  546018  1643640 |  390146    4931    45847     9.3 | 22.386 % |
|      7493 |  546018  1643640 |  429160    7493    72350     9.7 | 22.386 % |
|     11337 |  546018  1643640 |  472076   11337   114345    10.1 | 22.386 % |
|     17104 |  546018  1643640 |  519284   17104   185284    10.8 | 22.386 % |
|     25753 |  546018  1643640 |  571212   25753   282036    11.0 | 22.386 % |
|     38727 |  546018  1643640 |  628334   38727   453808    11.7 | 22.386 % |
|     58188 |  546018  1643640 |  691167   58188   681667    11.7 | 22.386 % |
|     87381 |  546018  1643640 |  760284   87381  1043441    11.9 | 22.386 % |
|    131170 |  546018  1643640 |  836312  131170  1588765    12.1 | 22.386 % |
|    196856 |  546020  1643640 |  919943  196854  2359321    12.0 | 22.386 % |
|    295383 |  545361  1641660 | 1011938  215066  2557282    11.9 | 22.395 % |
==============================================================================
restarts              : 19
conflicts             : 364132         (433 /sec)
decisions             : 417759         (497 /sec)
propagations          : 17083575       (20325 /sec)
conflict literals     : 4213622        (10.93 % deleted)
Memory used           : 70.33 MB
CPU time              : 840.54 s

UNSATISFIABLE
VERIFY_CNF 13 END :  (842 seconds) [Mon Jul 10 21:33:48 2006]
VERIFY_CNF 13 CPU : 842.07 = 0 + 0 + 840.54 + 1.53

# RESULT : color 13 UNSATISFIABLE
# BOUND : color 14 14

MAIN  END :  (1252 seconds) [Mon Jul 10 21:33:48 2006]
MAIN  CPU : 1251.94 = 98.32 + 0.62 + 1150.46 + 2.54