# TIMEOUT 7200
MAIN  BEGIN :  [Wed Jul  5 19:49:13 2006]
READ  BEGIN : csp/1-Insertions_4.csp [Wed Jul  5 19:49:13 2006]
READ  END : csp/1-Insertions_4.csp (0 seconds) [Wed Jul  5 19:49:13 2006]
READ  CPU : 0.42 = 0.41 + 0.01 + 0 + 0

# BOUND : color 2 5

GENERATE_CNF 5 BEGIN :  [Wed Jul  5 19:49:13 2006]
GENERATE_CNF 5 END : 938 variables 3295 clauses 45975 bytes (0 seconds) [Wed Jul  5 19:49:13 2006]
GENERATE_CNF 5 CPU : 0.19 = 0.19 + 0 + 0 + 0

MODIFY_CNF 3 BEGIN :  [Wed Jul  5 19:49:13 2006]
MODIFY_CNF 3 END : 45979 bytes (0 seconds) [Wed Jul  5 19:49:13 2006]
MODIFY_CNF 3 CPU : 0 = 0 + 0 + 0 + 0

VERIFY_CNF 3 BEGIN :  [Wed Jul  5 19:49:13 2006]
CMD : minisat /tmp/csp2sat31609.cnf /tmp/csp2sat31609.out
==================================[MINISAT]===================================
| Conflicts |     ORIGINAL     |              LEARNT              | Progress |
|           | Clauses Literals |   Limit Clauses Literals  Lit/Cl |          |
==============================================================================
|         0 |    1960     6249 |     653       0        0     nan |  0.000 % |
|       101 |    1960     6249 |     718     101     1228    12.2 | 36.141 % |
==============================================================================
restarts              : 2
conflicts             : 232            (11600 /sec)
decisions             : 284            (14200 /sec)
propagations          : 46378          (2318900 /sec)
conflict literals     : 2070           (7.55 % deleted)
Memory used           : 0.93 MB
CPU time              : 0.02 s

UNSATISFIABLE
VERIFY_CNF 3 END :  (0 seconds) [Wed Jul  5 19:49:13 2006]
VERIFY_CNF 3 CPU : 0.02 = 0 + 0 + 0.02 + 0

# RESULT : color 3 UNSATISFIABLE
# BOUND : color 4 5

MODIFY_CNF 4 BEGIN :  [Wed Jul  5 19:49:13 2006]
MODIFY_CNF 4 END : 45979 bytes (0 seconds) [Wed Jul  5 19:49:13 2006]
MODIFY_CNF 4 CPU : 0 = 0 + 0 + 0 + 0

VERIFY_CNF 4 BEGIN :  [Wed Jul  5 19:49:13 2006]
CMD : minisat /tmp/csp2sat31609.cnf /tmp/csp2sat31609.out
==================================[MINISAT]===================================
| Conflicts |     ORIGINAL     |              LEARNT              | Progress |
|           | Clauses Literals |   Limit Clauses Literals  Lit/Cl |          |
==============================================================================
|         0 |    2424     7641 |     808       0        0     nan |  0.000 % |
|       100 |    2424     7641 |     888     100     1662    16.6 | 28.892 % |
|       251 |    2424     7641 |     977     251     4565    18.2 | 28.891 % |
|       477 |    2424     7641 |    1075     477     8641    18.1 | 28.892 % |
|       814 |    2424     7641 |    1182     814    15756    19.4 | 28.891 % |
|      1320 |    2424     7641 |    1301    1320    26430    20.0 | 28.892 % |
|      2081 |    2424     7641 |    1431    1215    24044    19.8 | 28.895 % |
|      3220 |    2424     7641 |    1574    1405    26596    18.9 | 28.895 % |
|      4928 |    2424     7641 |    1732    2051    48880    23.8 | 28.892 % |
|      7490 |    2424     7641 |    1905    1359    28608    21.1 | 28.892 % |
|     11335 |    2424     7641 |    2095    1661    34450    20.7 | 28.892 % |
|     17101 |    2424     7641 |    2305    2257    49803    22.1 | 28.897 % |
|     25750 |    2424     7641 |    2535    2466    49556    20.1 | 28.892 % |
|     38726 |    2424     7641 |    2789    2016    43873    21.8 | 28.897 % |
|     58187 |    2424     7641 |    3068    2302    47465    20.6 | 28.892 % |
|     87379 |    2424     7641 |    3375    3143    88285    28.1 | 28.899 % |
|    131169 |    2424     7641 |    3712    2890    69670    24.1 | 28.897 % |
|    196853 |    2424     7641 |    4084    3998    88615    22.2 | 28.892 % |
|    295379 |    2425     7641 |    4492    2725    57470    21.1 | 28.891 % |
|    443168 |    2425     7641 |    4941    4290    87939    20.5 | 28.895 % |
|    664852 |    2400     7572 |    5435    3227    74709    23.2 | 28.998 % |
|    997378 |    2402     7572 |    5979    4715    91810    19.5 | 28.998 % |
|   1496167 |    2054     6900 |    6577    4208    61465    14.6 | 39.553 % |
==============================================================================
restarts              : 23
conflicts             : 1506976        (9779 /sec)
decisions             : 1934758        (12555 /sec)
propagations          : 175313683      (1137662 /sec)
conflict literals     : 34359116       (14.88 % deleted)
Memory used           : 3.26 MB
CPU time              : 154.1 s

UNSATISFIABLE
VERIFY_CNF 4 END :  (155 seconds) [Wed Jul  5 19:51:48 2006]
VERIFY_CNF 4 CPU : 154.3 = 0 + 0 + 154.1 + 0.2

# RESULT : color 4 UNSATISFIABLE
# BOUND : color 5 5

MAIN  END :  (155 seconds) [Wed Jul  5 19:51:48 2006]
MAIN  CPU : 154.93 = 0.6 + 0.01 + 154.12 + 0.2