# TIMEOUT 18000
MAIN  BEGIN :  [Sun Jun 18 16:08:36 2006]
READ  BEGIN : csp/gp04-08.csp [Sun Jun 18 16:08:36 2006]
READ  END : csp/gp04-08.csp (0 seconds) [Sun Jun 18 16:08:36 2006]
READ  CPU : 0.11 = 0.11 + 0 + 0 + 0

# BOUND : makespan 1000 1610

GENERATE_CNF 1610 BEGIN :  [Sun Jun 18 16:08:36 2006]
GENERATE_CNF 1610 END : 26516 variables 167013 clauses 3341998 bytes (6 seconds) [Sun Jun 18 16:08:42 2006]
GENERATE_CNF 1610 CPU : 6.07 = 6.07 + 0 + 0 + 0

MODIFY_CNF 1305 BEGIN :  [Sun Jun 18 16:08:42 2006]
MODIFY_CNF 1305 END : 3342004 bytes (0 seconds) [Sun Jun 18 16:08:42 2006]
MODIFY_CNF 1305 CPU : 0 = 0 + 0 + 0 + 0

VERIFY_CNF 1305 BEGIN :  [Sun Jun 18 16:08:42 2006]
CMD : minisat /tmp/csp2sat9051.cnf /tmp/csp2sat9051.out
==================================[MINISAT]===================================
| Conflicts |     ORIGINAL     |              LEARNT              | Progress |
|           | Clauses Literals |   Limit Clauses Literals  Lit/Cl |          |
==============================================================================
|         0 |  137520   386372 |   45840       0        0     nan |  0.000 % |
==============================================================================
restarts              : 1
conflicts             : 0              (0 /sec)
decisions             : 25             (125 /sec)
propagations          : 26516          (132580 /sec)
conflict literals     : 0              ( nan % deleted)
Memory used           : 9.11 MB
CPU time              : 0.2 s

SATISFIABLE
VERIFY_CNF 1305 END :  (0 seconds) [Sun Jun 18 16:08:42 2006]
VERIFY_CNF 1305 CPU : 0.23 = 0 + 0 + 0.21 + 0.02

# RESULT : makespan 1305 SATISFIABLE
SHOW_RESULT 1305 BEGIN :  [Sun Jun 18 16:08:42 2006]
# ASSIGN : makespan 1305
# ASSIGN : s_0_0 698
# ASSIGN : s_0_1 708
# ASSIGN : s_0_2 583
# ASSIGN : s_0_3 5
# ASSIGN : s_1_0 18
# ASSIGN : s_1_1 27
# ASSIGN : s_1_2 651
# ASSIGN : s_1_3 330
# ASSIGN : s_2_0 83
# ASSIGN : s_2_1 43
# ASSIGN : s_2_2 74
# ASSIGN : s_2_3 951
# ASSIGN : s_3_0 938
# ASSIGN : s_3_1 352
# ASSIGN : s_3_2 75
# ASSIGN : s_3_3 1304
SHOW_RESULT 1305 END : 1305 (0 seconds) [Sun Jun 18 16:08:42 2006]
SHOW_RESULT 1305 CPU : 0.0300000000000002 = 0.0300000000000002 + 0 + 0 + 0

# BOUND : makespan 1000 1305

MODIFY_CNF 1152 BEGIN :  [Sun Jun 18 16:08:42 2006]
MODIFY_CNF 1152 END : 3342004 bytes (1 seconds) [Sun Jun 18 16:08:43 2006]
MODIFY_CNF 1152 CPU : 0 = 0 + 0 + 0 + 0

VERIFY_CNF 1152 BEGIN :  [Sun Jun 18 16:08:43 2006]
CMD : minisat /tmp/csp2sat9051.cnf /tmp/csp2sat9051.out
==================================[MINISAT]===================================
| Conflicts |     ORIGINAL     |              LEARNT              | Progress |
|           | Clauses Literals |   Limit Clauses Literals  Lit/Cl |          |
==============================================================================
|         0 |  122832   342308 |   40944       0        0     nan |  0.000 % |
==============================================================================
restarts              : 1
conflicts             : 2              (10 /sec)
decisions             : 3              (14 /sec)
propagations          : 16243          (77348 /sec)
conflict literals     : 1              (0.00 % deleted)
Memory used           : 9.00 MB
CPU time              : 0.21 s

UNSATISFIABLE
VERIFY_CNF 1152 END :  (0 seconds) [Sun Jun 18 16:08:43 2006]
VERIFY_CNF 1152 CPU : 0.22 = 0 + 0 + 0.21 + 0.01

# RESULT : makespan 1152 UNSATISFIABLE
# BOUND : makespan 1153 1305

MODIFY_CNF 1229 BEGIN :  [Sun Jun 18 16:08:43 2006]
MODIFY_CNF 1229 END : 3342004 bytes (0 seconds) [Sun Jun 18 16:08:43 2006]
MODIFY_CNF 1229 CPU : 0 = 0 + 0 + 0 + 0

VERIFY_CNF 1229 BEGIN :  [Sun Jun 18 16:08:43 2006]
CMD : minisat /tmp/csp2sat9051.cnf /tmp/csp2sat9051.out
==================================[MINISAT]===================================
| Conflicts |     ORIGINAL     |              LEARNT              | Progress |
|           | Clauses Literals |   Limit Clauses Literals  Lit/Cl |          |
==============================================================================
|         0 |  130224   364484 |   43408       0        0     nan |  0.000 % |
==============================================================================
restarts              : 1
conflicts             : 2              (10 /sec)
decisions             : 3              (15 /sec)
propagations          : 14934          (74670 /sec)
conflict literals     : 1              (0.00 % deleted)
Memory used           : 9.00 MB
CPU time              : 0.2 s

UNSATISFIABLE
VERIFY_CNF 1229 END :  (0 seconds) [Sun Jun 18 16:08:43 2006]
VERIFY_CNF 1229 CPU : 0.22 = 0 + 0 + 0.2 + 0.02

# RESULT : makespan 1229 UNSATISFIABLE
# BOUND : makespan 1230 1305

MODIFY_CNF 1267 BEGIN :  [Sun Jun 18 16:08:43 2006]
MODIFY_CNF 1267 END : 3342004 bytes (0 seconds) [Sun Jun 18 16:08:43 2006]
MODIFY_CNF 1267 CPU : 0 = 0 + 0 + 0 + 0

VERIFY_CNF 1267 BEGIN :  [Sun Jun 18 16:08:43 2006]
CMD : minisat /tmp/csp2sat9051.cnf /tmp/csp2sat9051.out
==================================[MINISAT]===================================
| Conflicts |     ORIGINAL     |              LEARNT              | Progress |
|           | Clauses Literals |   Limit Clauses Literals  Lit/Cl |          |
==============================================================================
|         0 |  133872   375428 |   44624       0        0     nan |  0.000 % |
==============================================================================
restarts              : 1
conflicts             : 0              (0 /sec)
decisions             : 15             (79 /sec)
propagations          : 26516          (139558 /sec)
conflict literals     : 0              ( nan % deleted)
Memory used           : 9.12 MB
CPU time              : 0.19 s

SATISFIABLE
VERIFY_CNF 1267 END :  (1 seconds) [Sun Jun 18 16:08:44 2006]
VERIFY_CNF 1267 CPU : 0.24 = 0 + 0 + 0.2 + 0.04

# RESULT : makespan 1267 SATISFIABLE
SHOW_RESULT 1267 BEGIN :  [Sun Jun 18 16:08:44 2006]
# ASSIGN : makespan 1267
# ASSIGN : s_0_0 1257
# ASSIGN : s_0_1 654
# ASSIGN : s_0_2 261
# ASSIGN : s_0_3 329
# ASSIGN : s_1_0 1242
# ASSIGN : s_1_1 1251
# ASSIGN : s_1_2 335
# ASSIGN : s_1_3 8
# ASSIGN : s_2_0 8
# ASSIGN : s_2_1 623
# ASSIGN : s_2_2 7
# ASSIGN : s_2_3 913
# ASSIGN : s_3_0 623
# ASSIGN : s_3_1 267
# ASSIGN : s_3_2 989
# ASSIGN : s_3_3 1266
SHOW_RESULT 1267 END : 1267 (0 seconds) [Sun Jun 18 16:08:44 2006]
SHOW_RESULT 1267 CPU : 0.04 = 0.04 + 0 + 0 + 0

# BOUND : makespan 1230 1267

MODIFY_CNF 1248 BEGIN :  [Sun Jun 18 16:08:44 2006]
MODIFY_CNF 1248 END : 3342004 bytes (0 seconds) [Sun Jun 18 16:08:44 2006]
MODIFY_CNF 1248 CPU : 0 = 0 + 0 + 0 + 0

VERIFY_CNF 1248 BEGIN :  [Sun Jun 18 16:08:44 2006]
CMD : minisat /tmp/csp2sat9051.cnf /tmp/csp2sat9051.out
==================================[MINISAT]===================================
| Conflicts |     ORIGINAL     |              LEARNT              | Progress |
|           | Clauses Literals |   Limit Clauses Literals  Lit/Cl |          |
==============================================================================
|         0 |  132048   369956 |   44016       0        0     nan |  0.000 % |
==============================================================================
restarts              : 1
conflicts             : 2              (10 /sec)
decisions             : 3              (15 /sec)
propagations          : 20364          (101820 /sec)
conflict literals     : 1              (0.00 % deleted)
Memory used           : 9.00 MB
CPU time              : 0.2 s

UNSATISFIABLE
VERIFY_CNF 1248 END :  (0 seconds) [Sun Jun 18 16:08:44 2006]
VERIFY_CNF 1248 CPU : 0.23 = 0.00999999999999979 + 0 + 0.2 + 0.02

# RESULT : makespan 1248 UNSATISFIABLE
# BOUND : makespan 1249 1267

MODIFY_CNF 1258 BEGIN :  [Sun Jun 18 16:08:44 2006]
MODIFY_CNF 1258 END : 3342004 bytes (0 seconds) [Sun Jun 18 16:08:44 2006]
MODIFY_CNF 1258 CPU : 0 = 0 + 0 + 0 + 0

VERIFY_CNF 1258 BEGIN :  [Sun Jun 18 16:08:44 2006]
CMD : minisat /tmp/csp2sat9051.cnf /tmp/csp2sat9051.out
==================================[MINISAT]===================================
| Conflicts |     ORIGINAL     |              LEARNT              | Progress |
|           | Clauses Literals |   Limit Clauses Literals  Lit/Cl |          |
==============================================================================
|         0 |  133008   372836 |   44336       0        0     nan |  0.000 % |
==============================================================================
restarts              : 1
conflicts             : 3              (15 /sec)
decisions             : 3              (15 /sec)
propagations          : 24722          (123610 /sec)
conflict literals     : 3              (0.00 % deleted)
Memory used           : 8.98 MB
CPU time              : 0.2 s

UNSATISFIABLE
VERIFY_CNF 1258 END :  (0 seconds) [Sun Jun 18 16:08:44 2006]
VERIFY_CNF 1258 CPU : 0.22 = 0 + 0 + 0.2 + 0.02

# RESULT : makespan 1258 UNSATISFIABLE
# BOUND : makespan 1259 1267

MODIFY_CNF 1263 BEGIN :  [Sun Jun 18 16:08:44 2006]
MODIFY_CNF 1263 END : 3342004 bytes (0 seconds) [Sun Jun 18 16:08:44 2006]
MODIFY_CNF 1263 CPU : 0.0100000000000007 = 0.0100000000000007 + 0 + 0 + 0

VERIFY_CNF 1263 BEGIN :  [Sun Jun 18 16:08:44 2006]
CMD : minisat /tmp/csp2sat9051.cnf /tmp/csp2sat9051.out
==================================[MINISAT]===================================
| Conflicts |     ORIGINAL     |              LEARNT              | Progress |
|           | Clauses Literals |   Limit Clauses Literals  Lit/Cl |          |
==============================================================================
|         0 |  133488   374276 |   44496       0        0     nan |  0.000 % |
==============================================================================
restarts              : 1
conflicts             : 0              (0 /sec)
decisions             : 15             (71 /sec)
propagations          : 26516          (126267 /sec)
conflict literals     : 0              ( nan % deleted)
Memory used           : 9.11 MB
CPU time              : 0.21 s

SATISFIABLE
VERIFY_CNF 1263 END :  (0 seconds) [Sun Jun 18 16:08:44 2006]
VERIFY_CNF 1263 CPU : 0.24 = 0 + 0 + 0.22 + 0.02

# RESULT : makespan 1263 SATISFIABLE
SHOW_RESULT 1263 BEGIN :  [Sun Jun 18 16:08:44 2006]
# ASSIGN : makespan 1263
# ASSIGN : s_0_0 1253
# ASSIGN : s_0_1 650
# ASSIGN : s_0_2 257
# ASSIGN : s_0_3 325
# ASSIGN : s_1_0 1238
# ASSIGN : s_1_1 1247
# ASSIGN : s_1_2 331
# ASSIGN : s_1_3 4
# ASSIGN : s_2_0 4
# ASSIGN : s_2_1 619
# ASSIGN : s_2_2 3
# ASSIGN : s_2_3 909
# ASSIGN : s_3_0 619
# ASSIGN : s_3_1 263
# ASSIGN : s_3_2 985
# ASSIGN : s_3_3 1262
SHOW_RESULT 1263 END : 1263 (0 seconds) [Sun Jun 18 16:08:44 2006]
SHOW_RESULT 1263 CPU : 0.04 = 0.04 + 0 + 0 + 0

# BOUND : makespan 1259 1263

MODIFY_CNF 1261 BEGIN :  [Sun Jun 18 16:08:44 2006]
MODIFY_CNF 1261 END : 3342004 bytes (0 seconds) [Sun Jun 18 16:08:44 2006]
MODIFY_CNF 1261 CPU : 0 = 0 + 0 + 0 + 0

VERIFY_CNF 1261 BEGIN :  [Sun Jun 18 16:08:44 2006]
CMD : minisat /tmp/csp2sat9051.cnf /tmp/csp2sat9051.out
==================================[MINISAT]===================================
| Conflicts |     ORIGINAL     |              LEARNT              | Progress |
|           | Clauses Literals |   Limit Clauses Literals  Lit/Cl |          |
==============================================================================
|         0 |  133296   373700 |   44432       0        0     nan |  0.000 % |
==============================================================================
restarts              : 1
conflicts             : 0              (0 /sec)
decisions             : 15             (75 /sec)
propagations          : 26516          (132580 /sec)
conflict literals     : 0              ( nan % deleted)
Memory used           : 9.12 MB
CPU time              : 0.2 s

SATISFIABLE
VERIFY_CNF 1261 END :  (1 seconds) [Sun Jun 18 16:08:45 2006]
VERIFY_CNF 1261 CPU : 0.23 = 0 + 0 + 0.2 + 0.03

# RESULT : makespan 1261 SATISFIABLE
SHOW_RESULT 1261 BEGIN :  [Sun Jun 18 16:08:45 2006]
# ASSIGN : makespan 1261
# ASSIGN : s_0_0 1251
# ASSIGN : s_0_1 648
# ASSIGN : s_0_2 255
# ASSIGN : s_0_3 323
# ASSIGN : s_1_0 1236
# ASSIGN : s_1_1 1245
# ASSIGN : s_1_2 329
# ASSIGN : s_1_3 2
# ASSIGN : s_2_0 2
# ASSIGN : s_2_1 617
# ASSIGN : s_2_2 1
# ASSIGN : s_2_3 907
# ASSIGN : s_3_0 617
# ASSIGN : s_3_1 261
# ASSIGN : s_3_2 983
# ASSIGN : s_3_3 1260
SHOW_RESULT 1261 END : 1261 (0 seconds) [Sun Jun 18 16:08:45 2006]
SHOW_RESULT 1261 CPU : 0.04 = 0.04 + 0 + 0 + 0

# BOUND : makespan 1259 1261

MODIFY_CNF 1260 BEGIN :  [Sun Jun 18 16:08:45 2006]
MODIFY_CNF 1260 END : 3342004 bytes (0 seconds) [Sun Jun 18 16:08:45 2006]
MODIFY_CNF 1260 CPU : 0 = 0 + 0 + 0 + 0

VERIFY_CNF 1260 BEGIN :  [Sun Jun 18 16:08:45 2006]
CMD : minisat /tmp/csp2sat9051.cnf /tmp/csp2sat9051.out
==================================[MINISAT]===================================
| Conflicts |     ORIGINAL     |              LEARNT              | Progress |
|           | Clauses Literals |   Limit Clauses Literals  Lit/Cl |          |
==============================================================================
|         0 |  133200   373412 |   44400       0        0     nan |  0.000 % |
==============================================================================
restarts              : 1
conflicts             : 0              (0 /sec)
decisions             : 12             (67 /sec)
propagations          : 26516          (147311 /sec)
conflict literals     : 0              ( nan % deleted)
Memory used           : 9.11 MB
CPU time              : 0.18 s

SATISFIABLE
VERIFY_CNF 1260 END :  (0 seconds) [Sun Jun 18 16:08:45 2006]
VERIFY_CNF 1260 CPU : 0.24 = 0 + 0 + 0.18 + 0.06

# RESULT : makespan 1260 SATISFIABLE
SHOW_RESULT 1260 BEGIN :  [Sun Jun 18 16:08:45 2006]
# ASSIGN : makespan 1260
# ASSIGN : s_0_0 1250
# ASSIGN : s_0_1 647
# ASSIGN : s_0_2 254
# ASSIGN : s_0_3 322
# ASSIGN : s_1_0 1235
# ASSIGN : s_1_1 1244
# ASSIGN : s_1_2 328
# ASSIGN : s_1_3 1
# ASSIGN : s_2_0 1
# ASSIGN : s_2_1 616
# ASSIGN : s_2_2 0
# ASSIGN : s_2_3 906
# ASSIGN : s_3_0 616
# ASSIGN : s_3_1 260
# ASSIGN : s_3_2 982
# ASSIGN : s_3_3 1259
SHOW_RESULT 1260 END : 1260 (0 seconds) [Sun Jun 18 16:08:45 2006]
SHOW_RESULT 1260 CPU : 0.04 = 0.04 + 0 + 0 + 0

# BOUND : makespan 1259 1260

MODIFY_CNF 1259 BEGIN :  [Sun Jun 18 16:08:45 2006]
MODIFY_CNF 1259 END : 3342004 bytes (0 seconds) [Sun Jun 18 16:08:45 2006]
MODIFY_CNF 1259 CPU : 0 = 0 + 0 + 0 + 0

VERIFY_CNF 1259 BEGIN :  [Sun Jun 18 16:08:45 2006]
CMD : minisat /tmp/csp2sat9051.cnf /tmp/csp2sat9051.out
==================================[MINISAT]===================================
| Conflicts |     ORIGINAL     |              LEARNT              | Progress |
|           | Clauses Literals |   Limit Clauses Literals  Lit/Cl |          |
==============================================================================
|         0 |  133104   373124 |   44368       0        0     nan |  0.000 % |
==============================================================================
restarts              : 1
conflicts             : 0              (0 /sec)
decisions             : 10             (53 /sec)
propagations          : 26516          (139558 /sec)
conflict literals     : 0              ( nan % deleted)
Memory used           : 9.11 MB
CPU time              : 0.19 s

SATISFIABLE
VERIFY_CNF 1259 END :  (0 seconds) [Sun Jun 18 16:08:45 2006]
VERIFY_CNF 1259 CPU : 0.23 = 0 + 0 + 0.2 + 0.03

# RESULT : makespan 1259 SATISFIABLE
SHOW_RESULT 1259 BEGIN :  [Sun Jun 18 16:08:45 2006]
# ASSIGN : makespan 1259
# ASSIGN : s_0_0 1249
# ASSIGN : s_0_1 646
# ASSIGN : s_0_2 253
# ASSIGN : s_0_3 321
# ASSIGN : s_1_0 1234
# ASSIGN : s_1_1 1243
# ASSIGN : s_1_2 327
# ASSIGN : s_1_3 0
# ASSIGN : s_2_0 0
# ASSIGN : s_2_1 615
# ASSIGN : s_2_2 1258
# ASSIGN : s_2_3 905
# ASSIGN : s_3_0 615
# ASSIGN : s_3_1 259
# ASSIGN : s_3_2 981
# ASSIGN : s_3_3 1258
SHOW_RESULT 1259 END : 1259 (0 seconds) [Sun Jun 18 16:08:45 2006]
SHOW_RESULT 1259 CPU : 0.04 = 0.04 + 0 + 0 + 0

# BOUND : makespan 1259 1259

MAIN  END :  (9 seconds) [Sun Jun 18 16:08:45 2006]
MAIN  CPU : 8.73 = 6.44 + 0 + 2.02 + 0.27