# TIMEOUT 7200
MAIN  BEGIN :  [Mon Jul 10 17:12:26 2006]
READ  BEGIN : csp/queen8_12.csp [Mon Jul 10 17:12:26 2006]
READ  END : csp/queen8_12.csp (2 seconds) [Mon Jul 10 17:12:28 2006]
READ  CPU : 2.14 = 2.12 + 0.02 + 0 + 0

# BOUND : color 2 15

GENERATE_CNF 15 BEGIN :  [Mon Jul 10 17:12:28 2006]
GENERATE_CNF 15 END : 4383 variables 45400 clauses 777952 bytes (2 seconds) [Mon Jul 10 17:12:30 2006]
GENERATE_CNF 15 CPU : 2.1 = 2.1 + 0 + 0 + 0

MODIFY_CNF 8 BEGIN :  [Mon Jul 10 17:12:30 2006]
MODIFY_CNF 8 END : 777956 bytes (0 seconds) [Mon Jul 10 17:12:30 2006]
MODIFY_CNF 8 CPU : 0 = 0 + 0 + 0 + 0

VERIFY_CNF 8 BEGIN :  [Mon Jul 10 17:12:30 2006]
CMD : minisat /tmp/csp2sat24586.cnf /tmp/csp2sat24586.out
==================================[MINISAT]===================================
| Conflicts |     ORIGINAL     |              LEARNT              | Progress |
|           | Clauses Literals |   Limit Clauses Literals  Lit/Cl |          |
==============================================================================
|         0 |   25667    77594 |    8555       0        0     nan |  0.000 % |
|       100 |   25667    77594 |    9410     100      648     6.5 | 22.108 % |
|       251 |   25667    77594 |   10351     251     1773     7.1 | 22.109 % |
|       477 |   25667    77594 |   11386     477     3461     7.3 | 22.108 % |
|       815 |   25667    77594 |   12525     815     5942     7.3 | 22.109 % |
|      1321 |   25668    77594 |   13777    1320     9657     7.3 | 22.108 % |
|      2080 |   25668    77594 |   15155    2079    15027     7.2 | 22.108 % |
|      3219 |   25671    77594 |   16671    3215    22500     7.0 | 22.108 % |
|      4928 |   25543    77174 |   18338    3124    19962     6.4 | 22.405 % |
==============================================================================
restarts              : 9
conflicts             : 5087           (17541 /sec)
decisions             : 6320           (21793 /sec)
propagations          : 288844         (996014 /sec)
conflict literals     : 34123          (11.49 % deleted)
Memory used           : 3.25 MB
CPU time              : 0.29 s

UNSATISFIABLE
VERIFY_CNF 8 END :  (0 seconds) [Mon Jul 10 17:12:30 2006]
VERIFY_CNF 8 CPU : 0.31 = 0 + 0 + 0.29 + 0.02

# RESULT : color 8 UNSATISFIABLE
# BOUND : color 9 15

MODIFY_CNF 12 BEGIN :  [Mon Jul 10 17:12:30 2006]
MODIFY_CNF 12 END : 777957 bytes (0 seconds) [Mon Jul 10 17:12:30 2006]
MODIFY_CNF 12 CPU : 0 = 0 + 0 + 0 + 0

VERIFY_CNF 12 BEGIN :  [Mon Jul 10 17:12:30 2006]
CMD : minisat /tmp/csp2sat24586.cnf /tmp/csp2sat24586.out
==================================[MINISAT]===================================
| Conflicts |     ORIGINAL     |              LEARNT              | Progress |
|           | Clauses Literals |   Limit Clauses Literals  Lit/Cl |          |
==============================================================================
|         0 |   36611   110426 |   12203       0        0     nan |  0.000 % |
==============================================================================
restarts              : 1
conflicts             : 76             (844 /sec)
decisions             : 264            (2933 /sec)
propagations          : 37499          (416656 /sec)
conflict literals     : 5213           (1.08 % deleted)
Memory used           : 3.23 MB
CPU time              : 0.09 s

SATISFIABLE
VERIFY_CNF 12 END :  (0 seconds) [Mon Jul 10 17:12:30 2006]
VERIFY_CNF 12 CPU : 0.09 = 0 + 0 + 0.09 + 0

# RESULT : color 12 SATISFIABLE
SHOW_RESULT 12 BEGIN :  [Mon Jul 10 17:12:30 2006]
# ASSIGN : color 12
# ASSIGN : n1 4
# ASSIGN : n2 11
# ASSIGN : n3 6
# ASSIGN : n4 9
# ASSIGN : n5 7
# ASSIGN : n6 3
# ASSIGN : n7 2
# ASSIGN : n8 5
# ASSIGN : n9 10
# ASSIGN : n10 12
# ASSIGN : n11 8
# ASSIGN : n12 1
# ASSIGN : n13 2
# ASSIGN : n14 9
# ASSIGN : n15 12
# ASSIGN : n16 3
# ASSIGN : n17 10
# ASSIGN : n18 1
# ASSIGN : n19 8
# ASSIGN : n20 7
# ASSIGN : n21 4
# ASSIGN : n22 5
# ASSIGN : n23 6
# ASSIGN : n24 11
# ASSIGN : n25 8
# ASSIGN : n26 3
# ASSIGN : n27 10
# ASSIGN : n28 5
# ASSIGN : n29 12
# ASSIGN : n30 7
# ASSIGN : n31 4
# ASSIGN : n32 9
# ASSIGN : n33 6
# ASSIGN : n34 11
# ASSIGN : n35 1
# ASSIGN : n36 2
# ASSIGN : n37 10
# ASSIGN : n38 1
# ASSIGN : n39 8
# ASSIGN : n40 7
# ASSIGN : n41 2
# ASSIGN : n42 5
# ASSIGN : n43 6
# ASSIGN : n44 11
# ASSIGN : n45 12
# ASSIGN : n46 9
# ASSIGN : n47 3
# ASSIGN : n48 4
# ASSIGN : n49 12
# ASSIGN : n50 7
# ASSIGN : n51 9
# ASSIGN : n52 10
# ASSIGN : n53 11
# ASSIGN : n54 8
# ASSIGN : n55 1
# ASSIGN : n56 2
# ASSIGN : n57 3
# ASSIGN : n58 4
# ASSIGN : n59 5
# ASSIGN : n60 6
# ASSIGN : n61 9
# ASSIGN : n62 10
# ASSIGN : n63 11
# ASSIGN : n64 12
# ASSIGN : n65 1
# ASSIGN : n66 2
# ASSIGN : n67 3
# ASSIGN : n68 4
# ASSIGN : n69 5
# ASSIGN : n70 6
# ASSIGN : n71 7
# ASSIGN : n72 8
# ASSIGN : n73 11
# ASSIGN : n74 12
# ASSIGN : n75 1
# ASSIGN : n76 2
# ASSIGN : n77 3
# ASSIGN : n78 4
# ASSIGN : n79 5
# ASSIGN : n80 6
# ASSIGN : n81 7
# ASSIGN : n82 8
# ASSIGN : n83 9
# ASSIGN : n84 10
# ASSIGN : n85 1
# ASSIGN : n86 2
# ASSIGN : n87 3
# ASSIGN : n88 4
# ASSIGN : n89 5
# ASSIGN : n90 6
# ASSIGN : n91 7
# ASSIGN : n92 8
# ASSIGN : n93 9
# ASSIGN : n94 10
# ASSIGN : n95 11
# ASSIGN : n96 12
SHOW_RESULT 12 END : 12 (0 seconds) [Mon Jul 10 17:12:30 2006]
SHOW_RESULT 12 CPU : 0.00999999999999979 = 0.00999999999999979 + 0 + 0 + 0

# BOUND : color 9 12

MODIFY_CNF 10 BEGIN :  [Mon Jul 10 17:12:30 2006]
MODIFY_CNF 10 END : 777957 bytes (0 seconds) [Mon Jul 10 17:12:30 2006]
MODIFY_CNF 10 CPU : 0 = 0 + 0 + 0 + 0

VERIFY_CNF 10 BEGIN :  [Mon Jul 10 17:12:30 2006]
CMD : minisat /tmp/csp2sat24586.cnf /tmp/csp2sat24586.out
==================================[MINISAT]===================================
| Conflicts |     ORIGINAL     |              LEARNT              | Progress |
|           | Clauses Literals |   Limit Clauses Literals  Lit/Cl |          |
==============================================================================
|         0 |   31139    94010 |   10379       0        0     nan |  0.000 % |
|       100 |   31139    94010 |   11416     100      739     7.4 | 17.682 % |
|       250 |   31139    94010 |   12558     250     1865     7.5 | 17.682 % |
|       475 |   31139    94010 |   13814     475     3803     8.0 | 17.682 % |
|       812 |   31139    94010 |   15195     812     6359     7.8 | 17.682 % |
|      1319 |   31139    94010 |   16715    1319    11202     8.5 | 17.682 % |
|      2078 |   31139    94010 |   18387    2078    17178     8.3 | 17.682 % |
|      3217 |   31139    94010 |   20225    3217    26229     8.2 | 17.682 % |
|      4926 |   31139    94010 |   22248    4926    43263     8.8 | 17.682 % |
|      7488 |   31139    94010 |   24473    7488    69645     9.3 | 17.682 % |
|     11332 |   31139    94010 |   26920   11332   110777     9.8 | 17.682 % |
|     17100 |   31140    94010 |   29612   17099   158834     9.3 | 17.682 % |
|     25749 |   31143    94010 |   32573   25745   233947     9.1 | 17.682 % |
==============================================================================
restarts              : 13
conflicts             : 32301          (4750 /sec)
decisions             : 38897          (5720 /sec)
propagations          : 1554063        (228539 /sec)
conflict literals     : 282979         (10.33 % deleted)
Memory used           : 4.85 MB
CPU time              : 6.8 s

UNSATISFIABLE
VERIFY_CNF 10 END :  (7 seconds) [Mon Jul 10 17:12:37 2006]
VERIFY_CNF 10 CPU : 6.85 = 0 + 0.02 + 6.8 + 0.03

# RESULT : color 10 UNSATISFIABLE
# BOUND : color 11 12

MODIFY_CNF 11 BEGIN :  [Mon Jul 10 17:12:37 2006]
MODIFY_CNF 11 END : 777957 bytes (0 seconds) [Mon Jul 10 17:12:37 2006]
MODIFY_CNF 11 CPU : 0 = 0 + 0 + 0 + 0

VERIFY_CNF 11 BEGIN :  [Mon Jul 10 17:12:37 2006]
CMD : minisat /tmp/csp2sat24586.cnf /tmp/csp2sat24586.out
==================================[MINISAT]===================================
| Conflicts |     ORIGINAL     |              LEARNT              | Progress |
|           | Clauses Literals |   Limit Clauses Literals  Lit/Cl |          |
==============================================================================
|         0 |   33875   102218 |   11291       0        0     nan |  0.000 % |
|       101 |   33875   102218 |   12420     101      781     7.7 | 15.469 % |
|       251 |   33875   102218 |   13662     251     1680     6.7 | 15.469 % |
|       477 |   33875   102218 |   15028     477     3220     6.8 | 15.469 % |
|       814 |   33875   102218 |   16531     814     6826     8.4 | 15.469 % |
|      1320 |   33875   102218 |   18184    1320    11427     8.7 | 15.469 % |
|      2079 |   33875   102218 |   20002    2079    17582     8.5 | 15.469 % |
|      3218 |   33875   102218 |   22002    3218    28291     8.8 | 15.469 % |
|      4927 |   33875   102218 |   24203    4927    47069     9.6 | 15.469 % |
|      7490 |   33875   102218 |   26623    7490    74237     9.9 | 15.469 % |
|     11334 |   33875   102218 |   29285   11334   115557    10.2 | 15.469 % |
|     17101 |   33875   102218 |   32214   17101   175694    10.3 | 15.469 % |
|     25750 |   33875   102218 |   35435   25750   265242    10.3 | 15.469 % |
|     38725 |   33878   102218 |   38979   16234   153773     9.5 | 15.469 % |
|     58188 |   33692   101651 |   42877   20192   183571     9.1 | 15.697 % |
==============================================================================
restarts              : 15
conflicts             : 60255          (3628 /sec)
decisions             : 71319          (4294 /sec)
propagations          : 2278737        (137191 /sec)
conflict literals     : 591930         (9.10 % deleted)
Memory used           : 5.94 MB
CPU time              : 16.61 s

UNSATISFIABLE
VERIFY_CNF 11 END :  (17 seconds) [Mon Jul 10 17:12:54 2006]
VERIFY_CNF 11 CPU : 16.62 = 0 + 0 + 16.61 + 0.01

# RESULT : color 11 UNSATISFIABLE
# BOUND : color 12 12

MAIN  END :  (28 seconds) [Mon Jul 10 17:12:54 2006]
MAIN  CPU : 28.12 = 4.23 + 0.04 + 23.79 + 0.06