# TIMEOUT 7200 MAIN BEGIN : [Wed Jul 5 19:48:49 2006] READ BEGIN : csp/1-FullIns_5.csp [Wed Jul 5 19:48:49 2006] READ END : csp/1-FullIns_5.csp (5 seconds) [Wed Jul 5 19:48:54 2006] READ CPU : 5.09 = 5.04 + 0.05 + 0 + 0 # BOUND : color 2 14 GENERATE_CNF 14 BEGIN : [Wed Jul 5 19:48:54 2006] GENERATE_CNF 14 END : 11020 variables 102356 clauses 1840378 bytes (5 seconds) [Wed Jul 5 19:48:59 2006] GENERATE_CNF 14 CPU : 4.81 = 4.79 + 0.02 + 0 + 0 MODIFY_CNF 8 BEGIN : [Wed Jul 5 19:48:59 2006] MODIFY_CNF 8 END : 1840382 bytes (0 seconds) [Wed Jul 5 19:48:59 2006] MODIFY_CNF 8 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 8 BEGIN : [Wed Jul 5 19:48:59 2006] CMD : minisat /tmp/csp2sat31593.cnf /tmp/csp2sat31593.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 61695 186352 | 20565 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 1 (8 /sec) decisions : 1923 (16025 /sec) propagations : 11332 (94433 /sec) conflict literals : 5 (0.00 % deleted) Memory used : 5.67 MB CPU time : 0.12 s SATISFIABLE VERIFY_CNF 8 END : (0 seconds) [Wed Jul 5 19:48:59 2006] VERIFY_CNF 8 CPU : 0.14 = 0 + 0 + 0.13 + 0.01 # RESULT : color 8 SATISFIABLE SHOW_RESULT 8 BEGIN : [Wed Jul 5 19:48:59 2006] # ASSIGN : color 8 # ASSIGN : n1 3 # ASSIGN : n2 1 # ASSIGN : n3 5 # ASSIGN : n4 5 # ASSIGN : n5 3 # ASSIGN : n6 3 # ASSIGN : n7 7 # ASSIGN : n8 3 # ASSIGN : n9 5 # ASSIGN : n10 6 # ASSIGN : n11 8 # ASSIGN : n12 8 # ASSIGN : n13 2 # ASSIGN : n14 8 # ASSIGN : n15 1 # ASSIGN : n16 2 # ASSIGN : n17 1 # ASSIGN : n18 1 # ASSIGN : n19 3 # ASSIGN : n20 3 # ASSIGN : n21 3 # ASSIGN : n22 3 # ASSIGN : n23 3 # ASSIGN : n24 3 # ASSIGN : n25 3 # ASSIGN : n26 3 # ASSIGN : n27 5 # ASSIGN : n28 8 # ASSIGN : n29 3 # ASSIGN : n30 1 # ASSIGN : n31 3 # ASSIGN : n32 2 # ASSIGN : n33 2 # ASSIGN : n34 7 # ASSIGN : n35 3 # ASSIGN : n36 3 # ASSIGN : n37 2 # ASSIGN : n38 6 # ASSIGN : n39 5 # ASSIGN : n40 2 # ASSIGN : n41 2 # ASSIGN : n42 2 # ASSIGN : n43 2 # ASSIGN : n44 2 # ASSIGN : n45 2 # ASSIGN : n46 2 # ASSIGN : n47 2 # ASSIGN : n48 2 # ASSIGN : n49 3 # ASSIGN : n50 3 # ASSIGN : n51 3 # ASSIGN : n52 3 # ASSIGN : n53 3 # ASSIGN : n54 3 # ASSIGN : n55 3 # ASSIGN : n56 3 # ASSIGN : n57 3 # ASSIGN : n58 2 # ASSIGN : n59 3 # ASSIGN : n60 2 # ASSIGN : n61 1 # ASSIGN : n62 1 # ASSIGN : n63 1 # ASSIGN : n64 1 # ASSIGN : n65 1 # ASSIGN : n66 1 # ASSIGN : n67 1 # ASSIGN : n68 1 # ASSIGN : n69 7 # ASSIGN : n70 1 # ASSIGN : n71 1 # ASSIGN : n72 1 # ASSIGN : n73 1 # ASSIGN : n74 1 # ASSIGN : n75 1 # ASSIGN : n76 1 # ASSIGN : n77 1 # ASSIGN : n78 1 # ASSIGN : n79 1 # ASSIGN : n80 1 # ASSIGN : n81 1 # ASSIGN : n82 1 # ASSIGN : n83 1 # ASSIGN : n84 1 # ASSIGN : n85 3 # ASSIGN : n86 1 # ASSIGN : n87 1 # ASSIGN : n88 1 # ASSIGN : n89 1 # ASSIGN : n90 1 # ASSIGN : n91 8 # ASSIGN : n92 1 # ASSIGN : n93 2 # ASSIGN : n94 4 # ASSIGN : n95 4 # ASSIGN : n96 4 # ASSIGN : n97 4 # ASSIGN : n98 4 # ASSIGN : n99 4 # ASSIGN : n100 4 # ASSIGN : n101 4 # ASSIGN : n102 4 # ASSIGN : n103 4 # ASSIGN : n104 4 # ASSIGN : n105 4 # ASSIGN : n106 4 # ASSIGN : n107 4 # ASSIGN : n108 6 # ASSIGN : n109 4 # ASSIGN : n110 4 # ASSIGN : n111 4 # ASSIGN : n112 4 # ASSIGN : n113 4 # ASSIGN : n114 4 # ASSIGN : n115 4 # ASSIGN : n116 4 # ASSIGN : n117 4 # ASSIGN : n118 4 # ASSIGN : n119 4 # ASSIGN : n120 4 # ASSIGN : n121 4 # ASSIGN : n122 4 # ASSIGN : n123 4 # ASSIGN : n124 4 # ASSIGN : n125 4 # ASSIGN : n126 4 # ASSIGN : n127 4 # ASSIGN : n128 4 # ASSIGN : n129 4 # ASSIGN : n130 4 # ASSIGN : n131 4 # ASSIGN : n132 4 # ASSIGN : n133 4 # ASSIGN : n134 4 # ASSIGN : n135 4 # ASSIGN : n136 4 # ASSIGN : n137 4 # ASSIGN : n138 4 # ASSIGN : n139 4 # ASSIGN : n140 4 # ASSIGN : n141 4 # ASSIGN : n142 4 # ASSIGN : n143 4 # ASSIGN : n144 4 # ASSIGN : n145 4 # ASSIGN : n146 4 # ASSIGN : n147 4 # ASSIGN : n148 4 # ASSIGN : n149 4 # ASSIGN : n150 4 # ASSIGN : n151 4 # ASSIGN : n152 4 # ASSIGN : n153 4 # ASSIGN : n154 4 # ASSIGN : n155 4 # ASSIGN : n156 4 # ASSIGN : n157 4 # ASSIGN : n158 4 # ASSIGN : n159 4 # ASSIGN : n160 4 # ASSIGN : n161 4 # ASSIGN : n162 4 # ASSIGN : n163 4 # ASSIGN : n164 4 # ASSIGN : n165 4 # ASSIGN : n166 4 # ASSIGN : n167 4 # ASSIGN : n168 4 # ASSIGN : n169 4 # ASSIGN : n170 4 # ASSIGN : n171 4 # ASSIGN : n172 4 # ASSIGN : n173 4 # ASSIGN : n174 4 # ASSIGN : n175 4 # ASSIGN : n176 4 # ASSIGN : n177 4 # ASSIGN : n178 4 # ASSIGN : n179 4 # ASSIGN : n180 4 # ASSIGN : n181 4 # ASSIGN : n182 4 # ASSIGN : n183 4 # ASSIGN : n184 4 # ASSIGN : n185 4 # ASSIGN : n186 4 # ASSIGN : n187 5 # ASSIGN : n188 5 # ASSIGN : n189 5 # ASSIGN : n190 5 # ASSIGN : n191 5 # ASSIGN : n192 5 # ASSIGN : n193 5 # ASSIGN : n194 5 # ASSIGN : n195 5 # ASSIGN : n196 5 # ASSIGN : n197 5 # ASSIGN : n198 5 # ASSIGN : n199 5 # ASSIGN : n200 5 # ASSIGN : n201 5 # ASSIGN : n202 5 # ASSIGN : n203 5 # ASSIGN : n204 5 # ASSIGN : n205 5 # ASSIGN : n206 5 # ASSIGN : n207 5 # ASSIGN : n208 5 # ASSIGN : n209 5 # ASSIGN : n210 5 # ASSIGN : n211 5 # ASSIGN : n212 5 # ASSIGN : n213 5 # ASSIGN : n214 5 # ASSIGN : n215 5 # ASSIGN : n216 5 # ASSIGN : n217 5 # ASSIGN : n218 5 # ASSIGN : n219 5 # ASSIGN : n220 5 # ASSIGN : n221 5 # ASSIGN : n222 5 # ASSIGN : n223 5 # ASSIGN : n224 5 # ASSIGN : n225 5 # ASSIGN : n226 5 # ASSIGN : n227 5 # ASSIGN : n228 5 # ASSIGN : n229 5 # ASSIGN : n230 5 # ASSIGN : n231 5 # ASSIGN : n232 5 # ASSIGN : n233 5 # ASSIGN : n234 5 # ASSIGN : n235 5 # ASSIGN : n236 5 # ASSIGN : n237 5 # ASSIGN : n238 5 # ASSIGN : n239 5 # ASSIGN : n240 5 # ASSIGN : n241 5 # ASSIGN : n242 5 # ASSIGN : n243 5 # ASSIGN : n244 5 # ASSIGN : n245 5 # ASSIGN : n246 5 # ASSIGN : n247 5 # ASSIGN : n248 5 # ASSIGN : n249 5 # ASSIGN : n250 5 # ASSIGN : n251 5 # ASSIGN : n252 5 # ASSIGN : n253 5 # ASSIGN : n254 5 # ASSIGN : n255 5 # ASSIGN : n256 5 # ASSIGN : n257 5 # ASSIGN : n258 5 # ASSIGN : n259 5 # ASSIGN : n260 5 # ASSIGN : n261 5 # ASSIGN : n262 5 # ASSIGN : n263 5 # ASSIGN : n264 5 # ASSIGN : n265 5 # ASSIGN : n266 5 # ASSIGN : n267 5 # ASSIGN : n268 5 # ASSIGN : n269 5 # ASSIGN : n270 5 # ASSIGN : n271 5 # ASSIGN : n272 5 # ASSIGN : n273 5 # ASSIGN : n274 5 # ASSIGN : n275 5 # ASSIGN : n276 5 # ASSIGN : n277 5 # ASSIGN : n278 5 # ASSIGN : n279 5 # ASSIGN : n280 6 # ASSIGN : n281 7 # ASSIGN : n282 8 SHOW_RESULT 8 END : 8 (0 seconds) [Wed Jul 5 19:48:59 2006] SHOW_RESULT 8 CPU : 0.0300000000000011 = 0.0300000000000011 + 0 + 0 + 0 # BOUND : color 2 8 MODIFY_CNF 5 BEGIN : [Wed Jul 5 19:48:59 2006] MODIFY_CNF 5 END : 1840382 bytes (0 seconds) [Wed Jul 5 19:48:59 2006] MODIFY_CNF 5 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 5 BEGIN : [Wed Jul 5 19:48:59 2006] CMD : minisat /tmp/csp2sat31593.cnf /tmp/csp2sat31593.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 42213 127906 | 14071 0 0 nan | 0.000 % | | 100 | 42213 127906 | 15478 100 1657 16.6 | 30.808 % | | 250 | 42213 127906 | 17025 250 4184 16.7 | 30.808 % | | 476 | 42213 127906 | 18728 476 7600 16.0 | 30.808 % | | 813 | 42213 127906 | 20601 813 11638 14.3 | 30.808 % | | 1320 | 42213 127906 | 22661 1320 18249 13.8 | 30.808 % | | 2080 | 42213 127906 | 24927 2080 27518 13.2 | 30.808 % | | 3219 | 42213 127906 | 27420 3219 42658 13.3 | 30.808 % | | 4927 | 42213 127906 | 30162 4927 64517 13.1 | 30.808 % | | 7489 | 42213 127906 | 33178 7489 97913 13.1 | 30.808 % | | 11334 | 42213 127906 | 36496 11334 143397 12.7 | 30.808 % | | 17101 | 42017 127321 | 40146 8972 109274 12.2 | 30.835 % | ============================================================================== restarts : 12 conflicts : 23164 (1825 /sec) decisions : 28089 (2213 /sec) propagations : 12617883 (994317 /sec) conflict literals : 274931 (18.09 % deleted) Memory used : 5.93 MB CPU time : 12.69 s UNSATISFIABLE VERIFY_CNF 5 END : (13 seconds) [Wed Jul 5 19:49:12 2006] VERIFY_CNF 5 CPU : 12.72 = 0 + 0.01 + 12.69 + 0.02 # RESULT : color 5 UNSATISFIABLE # BOUND : color 6 8 MODIFY_CNF 7 BEGIN : [Wed Jul 5 19:49:12 2006] MODIFY_CNF 7 END : 1840382 bytes (0 seconds) [Wed Jul 5 19:49:12 2006] MODIFY_CNF 7 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 7 BEGIN : [Wed Jul 5 19:49:12 2006] CMD : minisat /tmp/csp2sat31593.cnf /tmp/csp2sat31593.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 55201 166870 | 18400 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 0 (0 /sec) decisions : 1606 (13383 /sec) propagations : 11020 (91833 /sec) conflict literals : 0 ( nan % deleted) Memory used : 5.71 MB CPU time : 0.12 s SATISFIABLE VERIFY_CNF 7 END : (0 seconds) [Wed Jul 5 19:49:12 2006] VERIFY_CNF 7 CPU : 0.159999999999999 = 0 + 0.01 + 0.129999999999999 + 0.02 # RESULT : color 7 SATISFIABLE SHOW_RESULT 7 BEGIN : [Wed Jul 5 19:49:12 2006] # ASSIGN : color 7 # ASSIGN : n1 7 # ASSIGN : n2 1 # ASSIGN : n3 4 # ASSIGN : n4 4 # ASSIGN : n5 1 # ASSIGN : n6 1 # ASSIGN : n7 6 # ASSIGN : n8 1 # ASSIGN : n9 4 # ASSIGN : n10 5 # ASSIGN : n11 5 # ASSIGN : n12 7 # ASSIGN : n13 4 # ASSIGN : n14 1 # ASSIGN : n15 1 # ASSIGN : n16 7 # ASSIGN : n17 1 # ASSIGN : n18 4 # ASSIGN : n19 6 # ASSIGN : n20 6 # ASSIGN : n21 6 # ASSIGN : n22 6 # ASSIGN : n23 6 # ASSIGN : n24 6 # ASSIGN : n25 6 # ASSIGN : n26 6 # ASSIGN : n27 6 # ASSIGN : n28 7 # ASSIGN : n29 6 # ASSIGN : n30 1 # ASSIGN : n31 2 # ASSIGN : n32 2 # ASSIGN : n33 2 # ASSIGN : n34 2 # ASSIGN : n35 2 # ASSIGN : n36 2 # ASSIGN : n37 2 # ASSIGN : n38 5 # ASSIGN : n39 5 # ASSIGN : n40 2 # ASSIGN : n41 2 # ASSIGN : n42 2 # ASSIGN : n43 2 # ASSIGN : n44 2 # ASSIGN : n45 2 # ASSIGN : n46 2 # ASSIGN : n47 2 # ASSIGN : n48 2 # ASSIGN : n49 2 # ASSIGN : n50 2 # ASSIGN : n51 2 # ASSIGN : n52 2 # ASSIGN : n53 2 # ASSIGN : n54 2 # ASSIGN : n55 2 # ASSIGN : n56 2 # ASSIGN : n57 2 # ASSIGN : n58 2 # ASSIGN : n59 2 # ASSIGN : n60 2 # ASSIGN : n61 1 # ASSIGN : n62 1 # ASSIGN : n63 1 # ASSIGN : n64 1 # ASSIGN : n65 1 # ASSIGN : n66 1 # ASSIGN : n67 1 # ASSIGN : n68 1 # ASSIGN : n69 6 # ASSIGN : n70 1 # ASSIGN : n71 1 # ASSIGN : n72 1 # ASSIGN : n73 1 # ASSIGN : n74 1 # ASSIGN : n75 1 # ASSIGN : n76 1 # ASSIGN : n77 1 # ASSIGN : n78 1 # ASSIGN : n79 1 # ASSIGN : n80 1 # ASSIGN : n81 1 # ASSIGN : n82 1 # ASSIGN : n83 1 # ASSIGN : n84 1 # ASSIGN : n85 6 # ASSIGN : n86 1 # ASSIGN : n87 1 # ASSIGN : n88 1 # ASSIGN : n89 1 # ASSIGN : n90 1 # ASSIGN : n91 7 # ASSIGN : n92 1 # ASSIGN : n93 2 # ASSIGN : n94 3 # ASSIGN : n95 3 # ASSIGN : n96 3 # ASSIGN : n97 3 # ASSIGN : n98 3 # ASSIGN : n99 3 # ASSIGN : n100 3 # ASSIGN : n101 3 # ASSIGN : n102 3 # ASSIGN : n103 3 # ASSIGN : n104 3 # ASSIGN : n105 3 # ASSIGN : n106 3 # ASSIGN : n107 3 # ASSIGN : n108 7 # ASSIGN : n109 3 # ASSIGN : n110 3 # ASSIGN : n111 3 # ASSIGN : n112 3 # ASSIGN : n113 3 # ASSIGN : n114 3 # ASSIGN : n115 3 # ASSIGN : n116 3 # ASSIGN : n117 3 # ASSIGN : n118 3 # ASSIGN : n119 3 # ASSIGN : n120 3 # ASSIGN : n121 3 # ASSIGN : n122 3 # ASSIGN : n123 3 # ASSIGN : n124 3 # ASSIGN : n125 3 # ASSIGN : n126 3 # ASSIGN : n127 3 # ASSIGN : n128 3 # ASSIGN : n129 3 # ASSIGN : n130 3 # ASSIGN : n131 3 # ASSIGN : n132 3 # ASSIGN : n133 3 # ASSIGN : n134 3 # ASSIGN : n135 3 # ASSIGN : n136 3 # ASSIGN : n137 3 # ASSIGN : n138 3 # ASSIGN : n139 3 # ASSIGN : n140 3 # ASSIGN : n141 3 # ASSIGN : n142 3 # ASSIGN : n143 3 # ASSIGN : n144 3 # ASSIGN : n145 3 # ASSIGN : n146 3 # ASSIGN : n147 3 # ASSIGN : n148 3 # ASSIGN : n149 3 # ASSIGN : n150 3 # ASSIGN : n151 3 # ASSIGN : n152 3 # ASSIGN : n153 3 # ASSIGN : n154 3 # ASSIGN : n155 3 # ASSIGN : n156 3 # ASSIGN : n157 3 # ASSIGN : n158 3 # ASSIGN : n159 3 # ASSIGN : n160 3 # ASSIGN : n161 3 # ASSIGN : n162 3 # ASSIGN : n163 3 # ASSIGN : n164 3 # ASSIGN : n165 3 # ASSIGN : n166 3 # ASSIGN : n167 3 # ASSIGN : n168 3 # ASSIGN : n169 3 # ASSIGN : n170 3 # ASSIGN : n171 3 # ASSIGN : n172 3 # ASSIGN : n173 3 # ASSIGN : n174 3 # ASSIGN : n175 3 # ASSIGN : n176 3 # ASSIGN : n177 3 # ASSIGN : n178 3 # ASSIGN : n179 3 # ASSIGN : n180 3 # ASSIGN : n181 3 # ASSIGN : n182 3 # ASSIGN : n183 3 # ASSIGN : n184 3 # ASSIGN : n185 3 # ASSIGN : n186 3 # ASSIGN : n187 4 # ASSIGN : n188 4 # ASSIGN : n189 4 # ASSIGN : n190 4 # ASSIGN : n191 4 # ASSIGN : n192 4 # ASSIGN : n193 4 # ASSIGN : n194 4 # ASSIGN : n195 4 # ASSIGN : n196 4 # ASSIGN : n197 4 # ASSIGN : n198 4 # ASSIGN : n199 4 # ASSIGN : n200 4 # ASSIGN : n201 4 # ASSIGN : n202 4 # ASSIGN : n203 4 # ASSIGN : n204 4 # ASSIGN : n205 4 # ASSIGN : n206 4 # ASSIGN : n207 4 # ASSIGN : n208 4 # ASSIGN : n209 4 # ASSIGN : n210 4 # ASSIGN : n211 4 # ASSIGN : n212 4 # ASSIGN : n213 4 # ASSIGN : n214 4 # ASSIGN : n215 4 # ASSIGN : n216 4 # ASSIGN : n217 4 # ASSIGN : n218 4 # ASSIGN : n219 4 # ASSIGN : n220 4 # ASSIGN : n221 4 # ASSIGN : n222 4 # ASSIGN : n223 4 # ASSIGN : n224 4 # ASSIGN : n225 4 # ASSIGN : n226 4 # ASSIGN : n227 4 # ASSIGN : n228 4 # ASSIGN : n229 4 # ASSIGN : n230 4 # ASSIGN : n231 4 # ASSIGN : n232 4 # ASSIGN : n233 4 # ASSIGN : n234 4 # ASSIGN : n235 4 # ASSIGN : n236 4 # ASSIGN : n237 4 # ASSIGN : n238 4 # ASSIGN : n239 4 # ASSIGN : n240 4 # ASSIGN : n241 4 # ASSIGN : n242 4 # ASSIGN : n243 4 # ASSIGN : n244 4 # ASSIGN : n245 4 # ASSIGN : n246 4 # ASSIGN : n247 4 # ASSIGN : n248 4 # ASSIGN : n249 4 # ASSIGN : n250 4 # ASSIGN : n251 4 # ASSIGN : n252 4 # ASSIGN : n253 4 # ASSIGN : n254 4 # ASSIGN : n255 4 # ASSIGN : n256 4 # ASSIGN : n257 4 # ASSIGN : n258 4 # ASSIGN : n259 4 # ASSIGN : n260 4 # ASSIGN : n261 4 # ASSIGN : n262 4 # ASSIGN : n263 4 # ASSIGN : n264 4 # ASSIGN : n265 4 # ASSIGN : n266 4 # ASSIGN : n267 4 # ASSIGN : n268 4 # ASSIGN : n269 4 # ASSIGN : n270 4 # ASSIGN : n271 4 # ASSIGN : n272 4 # ASSIGN : n273 4 # ASSIGN : n274 4 # ASSIGN : n275 4 # ASSIGN : n276 4 # ASSIGN : n277 4 # ASSIGN : n278 4 # ASSIGN : n279 4 # ASSIGN : n280 5 # ASSIGN : n281 6 # ASSIGN : n282 7 SHOW_RESULT 7 END : 7 (0 seconds) [Wed Jul 5 19:49:12 2006] SHOW_RESULT 7 CPU : 0.0199999999999996 = 0.0199999999999996 + 0 + 0 + 0 # BOUND : color 6 7 MODIFY_CNF 6 BEGIN : [Wed Jul 5 19:49:12 2006] MODIFY_CNF 6 END : 1840382 bytes (0 seconds) [Wed Jul 5 19:49:12 2006] MODIFY_CNF 6 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 6 BEGIN : [Wed Jul 5 19:49:12 2006] CMD : minisat /tmp/csp2sat31593.cnf /tmp/csp2sat31593.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 48707 147388 | 16235 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 0 (0 /sec) decisions : 609 (4685 /sec) propagations : 11020 (84769 /sec) conflict literals : 0 ( nan % deleted) Memory used : 5.66 MB CPU time : 0.13 s SATISFIABLE VERIFY_CNF 6 END : (0 seconds) [Wed Jul 5 19:49:12 2006] VERIFY_CNF 6 CPU : 0.150000000000001 = 0 + 0 + 0.140000000000001 + 0.01 # RESULT : color 6 SATISFIABLE SHOW_RESULT 6 BEGIN : [Wed Jul 5 19:49:12 2006] # ASSIGN : color 6 # ASSIGN : n1 5 # ASSIGN : n2 6 # ASSIGN : n3 3 # ASSIGN : n4 3 # ASSIGN : n5 6 # ASSIGN : n6 6 # ASSIGN : n7 5 # ASSIGN : n8 6 # ASSIGN : n9 3 # ASSIGN : n10 4 # ASSIGN : n11 4 # ASSIGN : n12 4 # ASSIGN : n13 4 # ASSIGN : n14 4 # ASSIGN : n15 4 # ASSIGN : n16 4 # ASSIGN : n17 4 # ASSIGN : n18 4 # ASSIGN : n19 3 # ASSIGN : n20 3 # ASSIGN : n21 3 # ASSIGN : n22 3 # ASSIGN : n23 3 # ASSIGN : n24 3 # ASSIGN : n25 3 # ASSIGN : n26 3 # ASSIGN : n27 3 # ASSIGN : n28 4 # ASSIGN : n29 5 # ASSIGN : n30 6 # ASSIGN : n31 1 # ASSIGN : n32 1 # ASSIGN : n33 1 # ASSIGN : n34 1 # ASSIGN : n35 1 # ASSIGN : n36 1 # ASSIGN : n37 5 # ASSIGN : n38 1 # ASSIGN : n39 3 # ASSIGN : n40 1 # ASSIGN : n41 1 # ASSIGN : n42 1 # ASSIGN : n43 1 # ASSIGN : n44 1 # ASSIGN : n45 1 # ASSIGN : n46 1 # ASSIGN : n47 1 # ASSIGN : n48 1 # ASSIGN : n49 1 # ASSIGN : n50 1 # ASSIGN : n51 1 # ASSIGN : n52 1 # ASSIGN : n53 1 # ASSIGN : n54 1 # ASSIGN : n55 1 # ASSIGN : n56 1 # ASSIGN : n57 1 # ASSIGN : n58 1 # ASSIGN : n59 1 # ASSIGN : n60 1 # ASSIGN : n61 4 # ASSIGN : n62 4 # ASSIGN : n63 4 # ASSIGN : n64 4 # ASSIGN : n65 4 # ASSIGN : n66 4 # ASSIGN : n67 4 # ASSIGN : n68 4 # ASSIGN : n69 4 # ASSIGN : n70 4 # ASSIGN : n71 4 # ASSIGN : n72 4 # ASSIGN : n73 4 # ASSIGN : n74 4 # ASSIGN : n75 4 # ASSIGN : n76 4 # ASSIGN : n77 4 # ASSIGN : n78 4 # ASSIGN : n79 4 # ASSIGN : n80 4 # ASSIGN : n81 4 # ASSIGN : n82 4 # ASSIGN : n83 4 # ASSIGN : n84 4 # ASSIGN : n85 4 # ASSIGN : n86 4 # ASSIGN : n87 4 # ASSIGN : n88 4 # ASSIGN : n89 4 # ASSIGN : n90 4 # ASSIGN : n91 5 # ASSIGN : n92 6 # ASSIGN : n93 1 # ASSIGN : n94 2 # ASSIGN : n95 2 # ASSIGN : n96 2 # ASSIGN : n97 2 # ASSIGN : n98 2 # ASSIGN : n99 2 # ASSIGN : n100 2 # ASSIGN : n101 2 # ASSIGN : n102 2 # ASSIGN : n103 2 # ASSIGN : n104 2 # ASSIGN : n105 2 # ASSIGN : n106 2 # ASSIGN : n107 2 # ASSIGN : n108 2 # ASSIGN : n109 2 # ASSIGN : n110 2 # ASSIGN : n111 2 # ASSIGN : n112 2 # ASSIGN : n113 2 # ASSIGN : n114 2 # ASSIGN : n115 2 # ASSIGN : n116 2 # ASSIGN : n117 2 # ASSIGN : n118 2 # ASSIGN : n119 2 # ASSIGN : n120 2 # ASSIGN : n121 2 # ASSIGN : n122 2 # ASSIGN : n123 2 # ASSIGN : n124 2 # ASSIGN : n125 2 # ASSIGN : n126 2 # ASSIGN : n127 2 # ASSIGN : n128 2 # ASSIGN : n129 2 # ASSIGN : n130 2 # ASSIGN : n131 2 # ASSIGN : n132 2 # ASSIGN : n133 2 # ASSIGN : n134 2 # ASSIGN : n135 2 # ASSIGN : n136 2 # ASSIGN : n137 2 # ASSIGN : n138 2 # ASSIGN : n139 2 # ASSIGN : n140 2 # ASSIGN : n141 2 # ASSIGN : n142 2 # ASSIGN : n143 2 # ASSIGN : n144 2 # ASSIGN : n145 2 # ASSIGN : n146 2 # ASSIGN : n147 2 # ASSIGN : n148 2 # ASSIGN : n149 2 # ASSIGN : n150 2 # ASSIGN : n151 2 # ASSIGN : n152 2 # ASSIGN : n153 2 # ASSIGN : n154 2 # ASSIGN : n155 2 # ASSIGN : n156 2 # ASSIGN : n157 2 # ASSIGN : n158 2 # ASSIGN : n159 2 # ASSIGN : n160 2 # ASSIGN : n161 2 # ASSIGN : n162 2 # ASSIGN : n163 2 # ASSIGN : n164 2 # ASSIGN : n165 2 # ASSIGN : n166 2 # ASSIGN : n167 2 # ASSIGN : n168 2 # ASSIGN : n169 2 # ASSIGN : n170 2 # ASSIGN : n171 2 # ASSIGN : n172 2 # ASSIGN : n173 2 # ASSIGN : n174 2 # ASSIGN : n175 2 # ASSIGN : n176 2 # ASSIGN : n177 2 # ASSIGN : n178 2 # ASSIGN : n179 2 # ASSIGN : n180 2 # ASSIGN : n181 2 # ASSIGN : n182 2 # ASSIGN : n183 2 # ASSIGN : n184 2 # ASSIGN : n185 2 # ASSIGN : n186 2 # ASSIGN : n187 3 # ASSIGN : n188 3 # ASSIGN : n189 3 # ASSIGN : n190 3 # ASSIGN : n191 3 # ASSIGN : n192 3 # ASSIGN : n193 3 # ASSIGN : n194 3 # ASSIGN : n195 3 # ASSIGN : n196 3 # ASSIGN : n197 3 # ASSIGN : n198 3 # ASSIGN : n199 3 # ASSIGN : n200 3 # ASSIGN : n201 3 # ASSIGN : n202 3 # ASSIGN : n203 3 # ASSIGN : n204 3 # ASSIGN : n205 3 # ASSIGN : n206 3 # ASSIGN : n207 3 # ASSIGN : n208 3 # ASSIGN : n209 3 # ASSIGN : n210 3 # ASSIGN : n211 3 # ASSIGN : n212 3 # ASSIGN : n213 3 # ASSIGN : n214 3 # ASSIGN : n215 3 # ASSIGN : n216 3 # ASSIGN : n217 3 # ASSIGN : n218 3 # ASSIGN : n219 3 # ASSIGN : n220 3 # ASSIGN : n221 3 # ASSIGN : n222 3 # ASSIGN : n223 3 # ASSIGN : n224 3 # ASSIGN : n225 3 # ASSIGN : n226 3 # ASSIGN : n227 3 # ASSIGN : n228 3 # ASSIGN : n229 3 # ASSIGN : n230 3 # ASSIGN : n231 3 # ASSIGN : n232 3 # ASSIGN : n233 3 # ASSIGN : n234 3 # ASSIGN : n235 3 # ASSIGN : n236 3 # ASSIGN : n237 3 # ASSIGN : n238 3 # ASSIGN : n239 3 # ASSIGN : n240 3 # ASSIGN : n241 3 # ASSIGN : n242 3 # ASSIGN : n243 3 # ASSIGN : n244 3 # ASSIGN : n245 3 # ASSIGN : n246 3 # ASSIGN : n247 3 # ASSIGN : n248 3 # ASSIGN : n249 3 # ASSIGN : n250 3 # ASSIGN : n251 3 # ASSIGN : n252 3 # ASSIGN : n253 3 # ASSIGN : n254 3 # ASSIGN : n255 3 # ASSIGN : n256 3 # ASSIGN : n257 3 # ASSIGN : n258 3 # ASSIGN : n259 3 # ASSIGN : n260 3 # ASSIGN : n261 3 # ASSIGN : n262 3 # ASSIGN : n263 3 # ASSIGN : n264 3 # ASSIGN : n265 3 # ASSIGN : n266 3 # ASSIGN : n267 3 # ASSIGN : n268 3 # ASSIGN : n269 3 # ASSIGN : n270 3 # ASSIGN : n271 3 # ASSIGN : n272 3 # ASSIGN : n273 3 # ASSIGN : n274 3 # ASSIGN : n275 3 # ASSIGN : n276 3 # ASSIGN : n277 3 # ASSIGN : n278 3 # ASSIGN : n279 3 # ASSIGN : n280 4 # ASSIGN : n281 5 # ASSIGN : n282 6 SHOW_RESULT 6 END : 6 (0 seconds) [Wed Jul 5 19:49:12 2006] SHOW_RESULT 6 CPU : 0.0199999999999996 = 0.0199999999999996 + 0 + 0 + 0 # BOUND : color 6 6 MAIN END : (23 seconds) [Wed Jul 5 19:49:12 2006] MAIN CPU : 23.14 = 9.9 + 0.09 + 13.09 + 0.06