# TIMEOUT 7200
MAIN  BEGIN :  [Thu Jul  6 09:58:07 2006]
READ  BEGIN : csp/4-FullIns_3.csp [Thu Jul  6 09:58:07 2006]
READ  END : csp/4-FullIns_3.csp (1 seconds) [Thu Jul  6 09:58:08 2006]
READ  CPU : 0.94 = 0.91 + 0.03 + 0 + 0

# BOUND : color 2 14

GENERATE_CNF 14 BEGIN :  [Thu Jul  6 09:58:08 2006]
GENERATE_CNF 14 END : 2920 variables 19010 clauses 320668 bytes (1 seconds) [Thu Jul  6 09:58:09 2006]
GENERATE_CNF 14 CPU : 0.9 = 0.89 + 0.01 + 0 + 0

MODIFY_CNF 8 BEGIN :  [Thu Jul  6 09:58:09 2006]
MODIFY_CNF 8 END : 320672 bytes (0 seconds) [Thu Jul  6 09:58:09 2006]
MODIFY_CNF 8 CPU : 0 = 0 + 0 + 0 + 0

VERIFY_CNF 8 BEGIN :  [Thu Jul  6 09:58:09 2006]
CMD : minisat /tmp/csp2sat13816.cnf /tmp/csp2sat13816.out
==================================[MINISAT]===================================
| Conflicts |     ORIGINAL     |              LEARNT              | Progress |
|           | Clauses Literals |   Limit Clauses Literals  Lit/Cl |          |
==============================================================================
|         0 |   11829    35224 |    3943       0        0     nan |  0.000 % |
==============================================================================
restarts              : 1
conflicts             : 0              (0 /sec)
decisions             : 336            (16800 /sec)
propagations          : 2920           (146000 /sec)
conflict literals     : 0              ( nan % deleted)
Memory used           : 1.80 MB
CPU time              : 0.02 s

SATISFIABLE
VERIFY_CNF 8 END :  (0 seconds) [Thu Jul  6 09:58:09 2006]
VERIFY_CNF 8 CPU : 0.03 = 0 + 0 + 0.03 + 0

# RESULT : color 8 SATISFIABLE
SHOW_RESULT 8 BEGIN :  [Thu Jul  6 09:58:09 2006]
# ASSIGN : color 8
# ASSIGN : n1 8
# ASSIGN : n2 2
# ASSIGN : n3 1
# ASSIGN : n4 1
# ASSIGN : n5 2
# ASSIGN : n6 2
# ASSIGN : n7 1
# ASSIGN : n8 1
# ASSIGN : n9 2
# ASSIGN : n10 2
# ASSIGN : n11 1
# ASSIGN : n12 1
# ASSIGN : n13 5
# ASSIGN : n14 6
# ASSIGN : n15 7
# ASSIGN : n16 8
# ASSIGN : n17 1
# ASSIGN : n18 2
# 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 3
# ASSIGN : n29 3
# ASSIGN : n30 3
# ASSIGN : n31 3
# ASSIGN : n32 3
# ASSIGN : n33 3
# ASSIGN : n34 3
# ASSIGN : n35 3
# ASSIGN : n36 3
# ASSIGN : n37 4
# ASSIGN : n38 4
# ASSIGN : n39 4
# ASSIGN : n40 4
# ASSIGN : n41 4
# ASSIGN : n42 4
# ASSIGN : n43 4
# ASSIGN : n44 4
# ASSIGN : n45 4
# ASSIGN : n46 4
# ASSIGN : n47 4
# ASSIGN : n48 4
# ASSIGN : n49 4
# ASSIGN : n50 4
# ASSIGN : n51 4
# ASSIGN : n52 4
# ASSIGN : n53 4
# ASSIGN : n54 4
# ASSIGN : n55 5
# ASSIGN : n56 5
# ASSIGN : n57 5
# ASSIGN : n58 5
# ASSIGN : n59 5
# ASSIGN : n60 5
# ASSIGN : n61 5
# ASSIGN : n62 5
# ASSIGN : n63 5
# ASSIGN : n64 5
# ASSIGN : n65 5
# ASSIGN : n66 5
# ASSIGN : n67 5
# ASSIGN : n68 5
# ASSIGN : n69 5
# ASSIGN : n70 5
# ASSIGN : n71 5
# ASSIGN : n72 5
# 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 1
# ASSIGN : n86 1
# ASSIGN : n87 1
# ASSIGN : n88 1
# ASSIGN : n89 1
# ASSIGN : n90 1
# ASSIGN : n91 2
# ASSIGN : n92 2
# ASSIGN : n93 2
# 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 3
# ASSIGN : n110 4
# ASSIGN : n111 5
# ASSIGN : n112 6
# ASSIGN : n113 7
# ASSIGN : n114 8
SHOW_RESULT 8 END : 8 (0 seconds) [Thu Jul  6 09:58:09 2006]
SHOW_RESULT 8 CPU : 0.01 = 0.01 + 0 + 0 + 0

# BOUND : color 2 8

MODIFY_CNF 5 BEGIN :  [Thu Jul  6 09:58:09 2006]
MODIFY_CNF 5 END : 320672 bytes (0 seconds) [Thu Jul  6 09:58:09 2006]
MODIFY_CNF 5 CPU : 0 = 0 + 0 + 0 + 0

VERIFY_CNF 5 BEGIN :  [Thu Jul  6 09:58:09 2006]
CMD : minisat /tmp/csp2sat13816.cnf /tmp/csp2sat13816.out
==================================[MINISAT]===================================
| Conflicts |     ORIGINAL     |              LEARNT              | Progress |
|           | Clauses Literals |   Limit Clauses Literals  Lit/Cl |          |
==============================================================================
|         0 |    8583    25486 |    2861       0        0     nan |  0.000 % |
|       101 |    8591    25486 |    3147      92      399     4.3 | 47.363 % |
==============================================================================
restarts              : 2
conflicts             : 148            (7400 /sec)
decisions             : 206            (10300 /sec)
propagations          : 10478          (523900 /sec)
conflict literals     : 544            (14.47 % deleted)
Memory used           : 1.82 MB
CPU time              : 0.02 s

UNSATISFIABLE
VERIFY_CNF 5 END :  (0 seconds) [Thu Jul  6 09:58:09 2006]
VERIFY_CNF 5 CPU : 0.03 = 0 + 0 + 0.02 + 0.01

# RESULT : color 5 UNSATISFIABLE
# BOUND : color 6 8

MODIFY_CNF 7 BEGIN :  [Thu Jul  6 09:58:09 2006]
MODIFY_CNF 7 END : 320672 bytes (0 seconds) [Thu Jul  6 09:58:09 2006]
MODIFY_CNF 7 CPU : 0 = 0 + 0 + 0 + 0

VERIFY_CNF 7 BEGIN :  [Thu Jul  6 09:58:09 2006]
CMD : minisat /tmp/csp2sat13816.cnf /tmp/csp2sat13816.out
==================================[MINISAT]===================================
| Conflicts |     ORIGINAL     |              LEARNT              | Progress |
|           | Clauses Literals |   Limit Clauses Literals  Lit/Cl |          |
==============================================================================
|         0 |   10747    31978 |    3582       0        0     nan |  0.000 % |
==============================================================================
restarts              : 1
conflicts             : 0              (0 /sec)
decisions             : 308            (15400 /sec)
propagations          : 2920           (146000 /sec)
conflict literals     : 0              ( nan % deleted)
Memory used           : 1.80 MB
CPU time              : 0.02 s

SATISFIABLE
VERIFY_CNF 7 END :  (0 seconds) [Thu Jul  6 09:58:09 2006]
VERIFY_CNF 7 CPU : 0.02 = 0 + 0 + 0.02 + 0

# RESULT : color 7 SATISFIABLE
SHOW_RESULT 7 BEGIN :  [Thu Jul  6 09:58:09 2006]
# ASSIGN : color 7
# ASSIGN : n1 7
# ASSIGN : n2 1
# ASSIGN : n3 3
# ASSIGN : n4 3
# ASSIGN : n5 1
# ASSIGN : n6 1
# ASSIGN : n7 5
# ASSIGN : n8 5
# ASSIGN : n9 1
# ASSIGN : n10 1
# ASSIGN : n11 7
# ASSIGN : n12 7
# ASSIGN : n13 3
# ASSIGN : n14 4
# ASSIGN : n15 5
# ASSIGN : n16 6
# ASSIGN : n17 7
# ASSIGN : n18 1
# ASSIGN : n19 2
# ASSIGN : n20 2
# ASSIGN : n21 2
# ASSIGN : n22 2
# ASSIGN : n23 2
# ASSIGN : n24 2
# ASSIGN : n25 2
# ASSIGN : n26 2
# ASSIGN : n27 2
# ASSIGN : n28 2
# ASSIGN : n29 2
# ASSIGN : n30 2
# ASSIGN : n31 2
# ASSIGN : n32 2
# ASSIGN : n33 2
# ASSIGN : n34 2
# ASSIGN : n35 2
# ASSIGN : n36 2
# ASSIGN : n37 3
# ASSIGN : n38 3
# ASSIGN : n39 3
# ASSIGN : n40 3
# ASSIGN : n41 3
# ASSIGN : n42 3
# ASSIGN : n43 3
# ASSIGN : n44 3
# ASSIGN : n45 3
# ASSIGN : n46 3
# ASSIGN : n47 3
# ASSIGN : n48 3
# ASSIGN : n49 3
# ASSIGN : n50 3
# ASSIGN : n51 3
# ASSIGN : n52 3
# ASSIGN : n53 3
# ASSIGN : n54 3
# ASSIGN : n55 4
# ASSIGN : n56 4
# ASSIGN : n57 4
# ASSIGN : n58 4
# ASSIGN : n59 4
# ASSIGN : n60 4
# 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 5
# ASSIGN : n74 5
# ASSIGN : n75 5
# ASSIGN : n76 5
# ASSIGN : n77 5
# ASSIGN : n78 5
# ASSIGN : n79 5
# ASSIGN : n80 5
# ASSIGN : n81 5
# ASSIGN : n82 5
# ASSIGN : n83 5
# ASSIGN : n84 5
# ASSIGN : n85 5
# ASSIGN : n86 5
# ASSIGN : n87 5
# ASSIGN : n88 5
# ASSIGN : n89 5
# ASSIGN : n90 5
# ASSIGN : n91 1
# ASSIGN : n92 1
# ASSIGN : n93 1
# ASSIGN : n94 1
# ASSIGN : n95 1
# ASSIGN : n96 1
# ASSIGN : n97 1
# ASSIGN : n98 1
# ASSIGN : n99 1
# ASSIGN : n100 1
# ASSIGN : n101 1
# ASSIGN : n102 1
# ASSIGN : n103 1
# ASSIGN : n104 1
# ASSIGN : n105 1
# ASSIGN : n106 1
# ASSIGN : n107 1
# ASSIGN : n108 1
# ASSIGN : n109 2
# ASSIGN : n110 3
# ASSIGN : n111 4
# ASSIGN : n112 5
# ASSIGN : n113 6
# ASSIGN : n114 7
SHOW_RESULT 7 END : 7 (0 seconds) [Thu Jul  6 09:58:09 2006]
SHOW_RESULT 7 CPU : 0 = 0 + 0 + 0 + 0

# BOUND : color 6 7

MODIFY_CNF 6 BEGIN :  [Thu Jul  6 09:58:09 2006]
MODIFY_CNF 6 END : 320672 bytes (0 seconds) [Thu Jul  6 09:58:09 2006]
MODIFY_CNF 6 CPU : 0.01 = 0 + 0.01 + 0 + 0

VERIFY_CNF 6 BEGIN :  [Thu Jul  6 09:58:09 2006]
CMD : minisat /tmp/csp2sat13816.cnf /tmp/csp2sat13816.out
==================================[MINISAT]===================================
| Conflicts |     ORIGINAL     |              LEARNT              | Progress |
|           | Clauses Literals |   Limit Clauses Literals  Lit/Cl |          |
==============================================================================
|         0 |    9665    28732 |    3221       0        0     nan |  0.000 % |
|       100 |    9665    28732 |    3543     100      569     5.7 | 43.288 % |
|       250 |    9666    28732 |    3897     249     1893     7.6 | 43.288 % |
|       475 |    9666    28732 |    4287     474     3681     7.8 | 43.288 % |
|       813 |    9635    28642 |    4715     620     4617     7.4 | 43.356 % |
==============================================================================
restarts              : 5
conflicts             : 1221           (20350 /sec)
decisions             : 2124           (35400 /sec)
propagations          : 108111         (1801850 /sec)
conflict literals     : 8307           (15.81 % deleted)
Memory used           : 1.83 MB
CPU time              : 0.06 s

UNSATISFIABLE
VERIFY_CNF 6 END :  (0 seconds) [Thu Jul  6 09:58:09 2006]
VERIFY_CNF 6 CPU : 0.07 = 0 + 0 + 0.06 + 0.01

# RESULT : color 6 UNSATISFIABLE
# BOUND : color 7 7

MAIN  END :  (2 seconds) [Thu Jul  6 09:58:09 2006]
MAIN  CPU : 2.01 = 1.81 + 0.05 + 0.13 + 0.02