# TIMEOUT 18000 MAIN BEGIN : [Sun Jun 18 16:21:08 2006] READ BEGIN : csp/gp06-07.csp [Sun Jun 18 16:21:08 2006] READ END : csp/gp06-07.csp (1 seconds) [Sun Jun 18 16:21:09 2006] READ CPU : 0.41 = 0.41 + 0 + 0 + 0 # BOUND : makespan 1000 3233 GENERATE_CNF 3233 BEGIN : [Sun Jun 18 16:21:09 2006] GENERATE_CNF 3233 END : 119091 variables 1303972 clauses 29154880 bytes (51 seconds) [Sun Jun 18 16:22:00 2006] GENERATE_CNF 3233 CPU : 51.03 = 50.8 + 0.23 + 0 + 0 MODIFY_CNF 2116 BEGIN : [Sun Jun 18 16:22:00 2006] MODIFY_CNF 2116 END : 29154887 bytes (0 seconds) [Sun Jun 18 16:22:00 2006] MODIFY_CNF 2116 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 2116 BEGIN : [Sun Jun 18 16:22:00 2006] CMD : minisat /tmp/csp2sat9799.cnf /tmp/csp2sat9799.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 901235 2585558 | 300411 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 0 (0 /sec) decisions : 156 (89 /sec) propagations : 119091 (67665 /sec) conflict literals : 0 ( nan % deleted) Memory used : 55.42 MB CPU time : 1.76 s SATISFIABLE VERIFY_CNF 2116 END : (2 seconds) [Sun Jun 18 16:22:02 2006] VERIFY_CNF 2116 CPU : 1.97 = 0 + 0 + 1.82 + 0.15 # RESULT : makespan 2116 SATISFIABLE SHOW_RESULT 2116 BEGIN : [Sun Jun 18 16:22:02 2006] # ASSIGN : makespan 2116 # ASSIGN : s_0_0 114 # ASSIGN : s_0_1 77 # ASSIGN : s_0_2 78 # ASSIGN : s_0_3 832 # ASSIGN : s_0_4 102 # ASSIGN : s_0_5 1116 # ASSIGN : s_1_0 770 # ASSIGN : s_1_1 417 # ASSIGN : s_1_2 112 # ASSIGN : s_1_3 1122 # ASSIGN : s_1_4 114 # ASSIGN : s_1_5 1139 # ASSIGN : s_2_0 1086 # ASSIGN : s_2_1 1091 # ASSIGN : s_2_2 116 # ASSIGN : s_2_3 1123 # ASSIGN : s_2_4 115 # ASSIGN : s_2_5 1466 # ASSIGN : s_3_0 1105 # ASSIGN : s_3_1 1106 # ASSIGN : s_3_2 1123 # ASSIGN : s_3_3 1131 # ASSIGN : s_3_4 425 # ASSIGN : s_3_5 1467 # ASSIGN : s_4_0 1108 # ASSIGN : s_4_1 1123 # ASSIGN : s_4_2 1124 # ASSIGN : s_4_3 1431 # ASSIGN : s_4_4 1126 # ASSIGN : s_4_5 1468 # ASSIGN : s_5_0 1116 # ASSIGN : s_5_1 1130 # ASSIGN : s_5_2 1743 # ASSIGN : s_5_3 1744 # ASSIGN : s_5_4 2114 # ASSIGN : s_5_5 2115 SHOW_RESULT 2116 END : 2116 (1 seconds) [Sun Jun 18 16:22:03 2006] SHOW_RESULT 2116 CPU : 0.220000000000001 = 0.210000000000001 + 0.00999999999999998 + 0 + 0 # BOUND : makespan 1000 2116 MODIFY_CNF 1558 BEGIN : [Sun Jun 18 16:22:03 2006] MODIFY_CNF 1558 END : 29154886 bytes (0 seconds) [Sun Jun 18 16:22:03 2006] MODIFY_CNF 1558 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1558 BEGIN : [Sun Jun 18 16:22:03 2006] CMD : minisat /tmp/csp2sat9799.cnf /tmp/csp2sat9799.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 700355 1982918 | 233451 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 0 (0 /sec) decisions : 135 (79 /sec) propagations : 119091 (69644 /sec) conflict literals : 0 ( nan % deleted) Memory used : 55.42 MB CPU time : 1.71 s SATISFIABLE VERIFY_CNF 1558 END : (2 seconds) [Sun Jun 18 16:22:05 2006] VERIFY_CNF 1558 CPU : 1.99 = 0 + 0 + 1.77 + 0.22 # RESULT : makespan 1558 SATISFIABLE SHOW_RESULT 1558 BEGIN : [Sun Jun 18 16:22:05 2006] # ASSIGN : makespan 1558 # ASSIGN : s_0_0 194 # ASSIGN : s_0_1 98 # ASSIGN : s_0_2 99 # ASSIGN : s_0_3 850 # ASSIGN : s_0_4 123 # ASSIGN : s_0_5 135 # ASSIGN : s_1_0 889 # ASSIGN : s_1_1 1205 # ASSIGN : s_1_2 154 # ASSIGN : s_1_3 156 # ASSIGN : s_1_4 157 # ASSIGN : s_1_5 158 # ASSIGN : s_2_0 1527 # ASSIGN : s_2_1 154 # ASSIGN : s_2_2 557 # ASSIGN : s_2_3 178 # ASSIGN : s_2_4 484 # ASSIGN : s_2_5 485 # ASSIGN : s_3_0 1532 # ASSIGN : s_3_1 169 # ASSIGN : s_3_2 1552 # ASSIGN : s_3_3 186 # ASSIGN : s_3_4 548 # ASSIGN : s_3_5 486 # ASSIGN : s_4_0 1533 # ASSIGN : s_4_1 486 # ASSIGN : s_4_2 1553 # ASSIGN : s_4_3 1134 # ASSIGN : s_4_4 1228 # ASSIGN : s_4_5 487 # ASSIGN : s_5_0 1541 # ASSIGN : s_5_1 558 # ASSIGN : s_5_2 1555 # ASSIGN : s_5_3 1171 # ASSIGN : s_5_4 1556 # ASSIGN : s_5_5 1557 SHOW_RESULT 1558 END : 1558 (0 seconds) [Sun Jun 18 16:22:05 2006] SHOW_RESULT 1558 CPU : 0.200000000000003 = 0.200000000000003 + 0 + 0 + 0 # BOUND : makespan 1000 1558 MODIFY_CNF 1279 BEGIN : [Sun Jun 18 16:22:05 2006] MODIFY_CNF 1279 END : 29154886 bytes (0 seconds) [Sun Jun 18 16:22:05 2006] MODIFY_CNF 1279 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1279 BEGIN : [Sun Jun 18 16:22:05 2006] CMD : minisat /tmp/csp2sat9799.cnf /tmp/csp2sat9799.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 599915 1681598 | 199971 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 2 (1 /sec) decisions : 8 (5 /sec) propagations : 84423 (49083 /sec) conflict literals : 1 (0.00 % deleted) Memory used : 54.82 MB CPU time : 1.72 s UNSATISFIABLE VERIFY_CNF 1279 END : (2 seconds) [Sun Jun 18 16:22:07 2006] VERIFY_CNF 1279 CPU : 1.87 = 0 + 0 + 1.72 + 0.15 # RESULT : makespan 1279 UNSATISFIABLE # BOUND : makespan 1280 1558 MODIFY_CNF 1419 BEGIN : [Sun Jun 18 16:22:07 2006] MODIFY_CNF 1419 END : 29154886 bytes (0 seconds) [Sun Jun 18 16:22:07 2006] MODIFY_CNF 1419 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1419 BEGIN : [Sun Jun 18 16:22:07 2006] CMD : minisat /tmp/csp2sat9799.cnf /tmp/csp2sat9799.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 650315 1832798 | 216771 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 1 (1 /sec) decisions : 124 (75 /sec) propagations : 123554 (74430 /sec) conflict literals : 7 (0.00 % deleted) Memory used : 55.42 MB CPU time : 1.66 s SATISFIABLE VERIFY_CNF 1419 END : (2 seconds) [Sun Jun 18 16:22:09 2006] VERIFY_CNF 1419 CPU : 1.96 = 0 + 0 + 1.72 + 0.24 # RESULT : makespan 1419 SATISFIABLE SHOW_RESULT 1419 BEGIN : [Sun Jun 18 16:22:09 2006] # ASSIGN : makespan 1419 # ASSIGN : s_0_0 756 # ASSIGN : s_0_1 5 # ASSIGN : s_0_2 322 # ASSIGN : s_0_3 472 # ASSIGN : s_0_4 346 # ASSIGN : s_0_5 6 # ASSIGN : s_1_0 440 # ASSIGN : s_1_1 1066 # ASSIGN : s_1_2 356 # ASSIGN : s_1_3 28 # ASSIGN : s_1_4 358 # ASSIGN : s_1_5 29 # ASSIGN : s_2_0 24 # ASSIGN : s_2_1 29 # ASSIGN : s_2_2 443 # ASSIGN : s_2_3 53 # ASSIGN : s_2_4 359 # ASSIGN : s_2_5 360 # ASSIGN : s_3_0 1412 # ASSIGN : s_3_1 44 # ASSIGN : s_3_2 1413 # ASSIGN : s_3_3 61 # ASSIGN : s_3_4 429 # ASSIGN : s_3_5 361 # ASSIGN : s_4_0 353 # ASSIGN : s_4_1 361 # ASSIGN : s_4_2 1414 # ASSIGN : s_4_3 1009 # ASSIGN : s_4_4 1109 # ASSIGN : s_4_5 362 # ASSIGN : s_5_0 419 # ASSIGN : s_5_1 433 # ASSIGN : s_5_2 1416 # ASSIGN : s_5_3 1046 # ASSIGN : s_5_4 1417 # ASSIGN : s_5_5 1418 SHOW_RESULT 1419 END : 1419 (0 seconds) [Sun Jun 18 16:22:09 2006] SHOW_RESULT 1419 CPU : 0.189999999999998 = 0.189999999999998 + 0 + 0 + 0 # BOUND : makespan 1280 1419 MODIFY_CNF 1349 BEGIN : [Sun Jun 18 16:22:09 2006] MODIFY_CNF 1349 END : 29154886 bytes (0 seconds) [Sun Jun 18 16:22:09 2006] MODIFY_CNF 1349 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1349 BEGIN : [Sun Jun 18 16:22:09 2006] CMD : minisat /tmp/csp2sat9799.cnf /tmp/csp2sat9799.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 625115 1757198 | 208371 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 0 (0 /sec) decisions : 109 (65 /sec) propagations : 119091 (70888 /sec) conflict literals : 0 ( nan % deleted) Memory used : 55.42 MB CPU time : 1.68 s SATISFIABLE VERIFY_CNF 1349 END : (2 seconds) [Sun Jun 18 16:22:11 2006] VERIFY_CNF 1349 CPU : 1.97 = 0 + 0 + 1.73 + 0.24 # RESULT : makespan 1349 SATISFIABLE SHOW_RESULT 1349 BEGIN : [Sun Jun 18 16:22:11 2006] # ASSIGN : makespan 1349 # ASSIGN : s_0_0 676 # ASSIGN : s_0_1 2 # ASSIGN : s_0_2 319 # ASSIGN : s_0_3 392 # ASSIGN : s_0_4 343 # ASSIGN : s_0_5 3 # ASSIGN : s_1_0 360 # ASSIGN : s_1_1 996 # ASSIGN : s_1_2 353 # ASSIGN : s_1_3 25 # ASSIGN : s_1_4 355 # ASSIGN : s_1_5 26 # ASSIGN : s_2_0 18 # ASSIGN : s_2_1 23 # ASSIGN : s_2_2 373 # ASSIGN : s_2_3 47 # ASSIGN : s_2_4 356 # ASSIGN : s_2_5 357 # ASSIGN : s_3_0 37 # ASSIGN : s_3_1 38 # ASSIGN : s_3_2 1343 # ASSIGN : s_3_3 55 # ASSIGN : s_3_4 359 # ASSIGN : s_3_5 358 # ASSIGN : s_4_0 340 # ASSIGN : s_4_1 348 # ASSIGN : s_4_2 1344 # ASSIGN : s_4_3 355 # ASSIGN : s_4_4 1039 # ASSIGN : s_4_5 392 # ASSIGN : s_5_0 1332 # ASSIGN : s_5_1 349 # ASSIGN : s_5_2 1346 # ASSIGN : s_5_3 962 # ASSIGN : s_5_4 1347 # ASSIGN : s_5_5 1348 SHOW_RESULT 1349 END : 1349 (0 seconds) [Sun Jun 18 16:22:11 2006] SHOW_RESULT 1349 CPU : 0.200000000000005 = 0.190000000000005 + 0.01 + 0 + 0 # BOUND : makespan 1280 1349 MODIFY_CNF 1314 BEGIN : [Sun Jun 18 16:22:11 2006] MODIFY_CNF 1314 END : 29154886 bytes (0 seconds) [Sun Jun 18 16:22:11 2006] MODIFY_CNF 1314 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1314 BEGIN : [Sun Jun 18 16:22:11 2006] CMD : minisat /tmp/csp2sat9799.cnf /tmp/csp2sat9799.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 612515 1719398 | 204171 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 0 (0 /sec) decisions : 88 (49 /sec) propagations : 119091 (66162 /sec) conflict literals : 0 ( nan % deleted) Memory used : 55.42 MB CPU time : 1.8 s SATISFIABLE VERIFY_CNF 1314 END : (2 seconds) [Sun Jun 18 16:22:13 2006] VERIFY_CNF 1314 CPU : 2.01 = 0 + 0 + 1.85 + 0.16 # RESULT : makespan 1314 SATISFIABLE SHOW_RESULT 1314 BEGIN : [Sun Jun 18 16:22:13 2006] # ASSIGN : makespan 1314 # ASSIGN : s_0_0 658 # ASSIGN : s_0_1 17 # ASSIGN : s_0_2 302 # ASSIGN : s_0_3 18 # ASSIGN : s_0_4 0 # ASSIGN : s_0_5 607 # ASSIGN : s_1_0 342 # ASSIGN : s_1_1 961 # ASSIGN : s_1_2 9 # ASSIGN : s_1_3 11 # ASSIGN : s_1_4 12 # ASSIGN : s_1_5 13 # ASSIGN : s_2_0 284 # ASSIGN : s_2_1 289 # ASSIGN : s_2_2 341 # ASSIGN : s_2_3 313 # ASSIGN : s_2_4 321 # ASSIGN : s_2_5 340 # ASSIGN : s_3_0 303 # ASSIGN : s_3_1 304 # ASSIGN : s_3_2 326 # ASSIGN : s_3_3 327 # ASSIGN : s_3_4 631 # ASSIGN : s_3_5 630 # ASSIGN : s_4_0 306 # ASSIGN : s_4_1 321 # ASSIGN : s_4_2 1311 # ASSIGN : s_4_3 627 # ASSIGN : s_4_4 322 # ASSIGN : s_4_5 664 # ASSIGN : s_5_0 314 # ASSIGN : s_5_1 328 # ASSIGN : s_5_2 1313 # ASSIGN : s_5_3 941 # ASSIGN : s_5_4 1311 # ASSIGN : s_5_5 1312 SHOW_RESULT 1314 END : 1314 (0 seconds) [Sun Jun 18 16:22:13 2006] SHOW_RESULT 1314 CPU : 0.199999999999996 = 0.199999999999996 + 0 + 0 + 0 # BOUND : makespan 1280 1314 MODIFY_CNF 1297 BEGIN : [Sun Jun 18 16:22:13 2006] MODIFY_CNF 1297 END : 29154886 bytes (0 seconds) [Sun Jun 18 16:22:13 2006] MODIFY_CNF 1297 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1297 BEGIN : [Sun Jun 18 16:22:13 2006] CMD : minisat /tmp/csp2sat9799.cnf /tmp/csp2sat9799.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 606395 1701038 | 202131 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 0 (0 /sec) decisions : 91 (50 /sec) propagations : 119091 (65435 /sec) conflict literals : 0 ( nan % deleted) Memory used : 55.42 MB CPU time : 1.82 s SATISFIABLE VERIFY_CNF 1297 END : (2 seconds) [Sun Jun 18 16:22:15 2006] VERIFY_CNF 1297 CPU : 2 = 0 + 0 + 1.89 + 0.11 # RESULT : makespan 1297 SATISFIABLE SHOW_RESULT 1297 BEGIN : [Sun Jun 18 16:22:15 2006] # ASSIGN : makespan 1297 # ASSIGN : s_0_0 325 # ASSIGN : s_0_1 13 # ASSIGN : s_0_2 206 # ASSIGN : s_0_3 1013 # ASSIGN : s_0_4 230 # ASSIGN : s_0_5 242 # ASSIGN : s_1_0 981 # ASSIGN : s_1_1 628 # ASSIGN : s_1_2 253 # ASSIGN : s_1_3 255 # ASSIGN : s_1_4 263 # ASSIGN : s_1_5 266 # ASSIGN : s_2_0 251 # ASSIGN : s_2_1 1259 # ASSIGN : s_2_2 289 # ASSIGN : s_2_3 256 # ASSIGN : s_2_4 264 # ASSIGN : s_2_5 265 # ASSIGN : s_3_0 0 # ASSIGN : s_3_1 1274 # ASSIGN : s_3_2 1291 # ASSIGN : s_3_3 293 # ASSIGN : s_3_4 594 # ASSIGN : s_3_5 593 # ASSIGN : s_4_0 281 # ASSIGN : s_4_1 14 # ASSIGN : s_4_2 1292 # ASSIGN : s_4_3 606 # ASSIGN : s_4_4 289 # ASSIGN : s_4_5 645 # ASSIGN : s_5_0 1 # ASSIGN : s_5_1 15 # ASSIGN : s_5_2 1294 # ASSIGN : s_5_3 643 # ASSIGN : s_5_4 1295 # ASSIGN : s_5_5 1296 SHOW_RESULT 1297 END : 1297 (0 seconds) [Sun Jun 18 16:22:15 2006] SHOW_RESULT 1297 CPU : 0.200000000000005 = 0.190000000000005 + 0.01 + 0 + 0 # BOUND : makespan 1280 1297 MODIFY_CNF 1288 BEGIN : [Sun Jun 18 16:22:15 2006] MODIFY_CNF 1288 END : 29154886 bytes (0 seconds) [Sun Jun 18 16:22:15 2006] MODIFY_CNF 1288 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1288 BEGIN : [Sun Jun 18 16:22:15 2006] CMD : minisat /tmp/csp2sat9799.cnf /tmp/csp2sat9799.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 603155 1691318 | 201051 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 2 (1 /sec) decisions : 8 (5 /sec) propagations : 90113 (52698 /sec) conflict literals : 1 (0.00 % deleted) Memory used : 54.83 MB CPU time : 1.71 s UNSATISFIABLE VERIFY_CNF 1288 END : (2 seconds) [Sun Jun 18 16:22:17 2006] VERIFY_CNF 1288 CPU : 1.9 = 0 + 0 + 1.71 + 0.19 # RESULT : makespan 1288 UNSATISFIABLE # BOUND : makespan 1289 1297 MODIFY_CNF 1293 BEGIN : [Sun Jun 18 16:22:17 2006] MODIFY_CNF 1293 END : 29154886 bytes (0 seconds) [Sun Jun 18 16:22:17 2006] MODIFY_CNF 1293 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1293 BEGIN : [Sun Jun 18 16:22:17 2006] CMD : minisat /tmp/csp2sat9799.cnf /tmp/csp2sat9799.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 604955 1696718 | 201651 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 1 (1 /sec) decisions : 67 (39 /sec) propagations : 124381 (71897 /sec) conflict literals : 2 (50.00 % deleted) Memory used : 55.42 MB CPU time : 1.73 s SATISFIABLE VERIFY_CNF 1293 END : (2 seconds) [Sun Jun 18 16:22:19 2006] VERIFY_CNF 1293 CPU : 1.99 = 0 + 0 + 1.78 + 0.21 # RESULT : makespan 1293 SATISFIABLE SHOW_RESULT 1293 BEGIN : [Sun Jun 18 16:22:19 2006] # ASSIGN : makespan 1293 # ASSIGN : s_0_0 353 # ASSIGN : s_0_1 25 # ASSIGN : s_0_2 271 # ASSIGN : s_0_3 1009 # ASSIGN : s_0_4 0 # ASSIGN : s_0_5 295 # ASSIGN : s_1_0 1 # ASSIGN : s_1_1 924 # ASSIGN : s_1_2 1288 # ASSIGN : s_1_3 0 # ASSIGN : s_1_4 317 # ASSIGN : s_1_5 318 # ASSIGN : s_2_0 1271 # ASSIGN : s_2_1 1277 # ASSIGN : s_2_2 301 # ASSIGN : s_2_3 34 # ASSIGN : s_2_4 1292 # ASSIGN : s_2_5 42 # ASSIGN : s_3_0 344 # ASSIGN : s_3_1 8 # ASSIGN : s_3_2 7 # ASSIGN : s_3_3 44 # ASSIGN : s_3_4 611 # ASSIGN : s_3_5 43 # ASSIGN : s_4_0 345 # ASSIGN : s_4_1 7 # ASSIGN : s_4_2 10 # ASSIGN : s_4_3 602 # ASSIGN : s_4_4 12 # ASSIGN : s_4_5 645 # ASSIGN : s_5_0 1276 # ASSIGN : s_5_1 26 # ASSIGN : s_5_2 1290 # ASSIGN : s_5_3 639 # ASSIGN : s_5_4 1291 # ASSIGN : s_5_5 1292 SHOW_RESULT 1293 END : 1293 (0 seconds) [Sun Jun 18 16:22:19 2006] SHOW_RESULT 1293 CPU : 0.19 = 0.18 + 0.01 + 0 + 0 # BOUND : makespan 1289 1293 MODIFY_CNF 1291 BEGIN : [Sun Jun 18 16:22:19 2006] MODIFY_CNF 1291 END : 29154886 bytes (0 seconds) [Sun Jun 18 16:22:19 2006] MODIFY_CNF 1291 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1291 BEGIN : [Sun Jun 18 16:22:19 2006] CMD : minisat /tmp/csp2sat9799.cnf /tmp/csp2sat9799.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 604235 1694558 | 201411 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 1 (1 /sec) decisions : 61 (34 /sec) propagations : 124381 (69487 /sec) conflict literals : 2 (50.00 % deleted) Memory used : 55.42 MB CPU time : 1.79 s SATISFIABLE VERIFY_CNF 1291 END : (2 seconds) [Sun Jun 18 16:22:21 2006] VERIFY_CNF 1291 CPU : 2 = 0 + 0 + 1.84 + 0.16 # RESULT : makespan 1291 SATISFIABLE SHOW_RESULT 1291 BEGIN : [Sun Jun 18 16:22:21 2006] # ASSIGN : makespan 1291 # ASSIGN : s_0_0 350 # ASSIGN : s_0_1 0 # ASSIGN : s_0_2 1 # ASSIGN : s_0_3 1006 # ASSIGN : s_0_4 25 # ASSIGN : s_0_5 293 # ASSIGN : s_1_0 0 # ASSIGN : s_1_1 922 # ASSIGN : s_1_2 1286 # ASSIGN : s_1_3 1290 # ASSIGN : s_1_4 1288 # ASSIGN : s_1_5 316 # ASSIGN : s_2_0 1269 # ASSIGN : s_2_1 1275 # ASSIGN : s_2_2 299 # ASSIGN : s_2_3 31 # ASSIGN : s_2_4 1290 # ASSIGN : s_2_5 39 # ASSIGN : s_3_0 341 # ASSIGN : s_3_1 5 # ASSIGN : s_3_2 34 # ASSIGN : s_3_3 41 # ASSIGN : s_3_4 608 # ASSIGN : s_3_5 40 # ASSIGN : s_4_0 342 # ASSIGN : s_4_1 22 # ASSIGN : s_4_2 35 # ASSIGN : s_4_3 599 # ASSIGN : s_4_4 37 # ASSIGN : s_4_5 643 # ASSIGN : s_5_0 1274 # ASSIGN : s_5_1 23 # ASSIGN : s_5_2 1288 # ASSIGN : s_5_3 636 # ASSIGN : s_5_4 1289 # ASSIGN : s_5_5 1290 SHOW_RESULT 1291 END : 1291 (1 seconds) [Sun Jun 18 16:22:22 2006] SHOW_RESULT 1291 CPU : 0.200000000000003 = 0.200000000000003 + 0 + 0 + 0 # BOUND : makespan 1289 1291 MODIFY_CNF 1290 BEGIN : [Sun Jun 18 16:22:22 2006] MODIFY_CNF 1290 END : 29154886 bytes (0 seconds) [Sun Jun 18 16:22:22 2006] MODIFY_CNF 1290 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1290 BEGIN : [Sun Jun 18 16:22:22 2006] CMD : minisat /tmp/csp2sat9799.cnf /tmp/csp2sat9799.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 603875 1693478 | 201291 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 2 (1 /sec) decisions : 65 (37 /sec) propagations : 128382 (72944 /sec) conflict literals : 5 (16.67 % deleted) Memory used : 55.42 MB CPU time : 1.76 s SATISFIABLE VERIFY_CNF 1290 END : (2 seconds) [Sun Jun 18 16:22:24 2006] VERIFY_CNF 1290 CPU : 2 = 0 + 0 + 1.83 + 0.17 # RESULT : makespan 1290 SATISFIABLE SHOW_RESULT 1290 BEGIN : [Sun Jun 18 16:22:24 2006] # ASSIGN : makespan 1290 # ASSIGN : s_0_0 307 # ASSIGN : s_0_1 0 # ASSIGN : s_0_2 268 # ASSIGN : s_0_3 998 # ASSIGN : s_0_4 963 # ASSIGN : s_0_5 975 # ASSIGN : s_1_0 974 # ASSIGN : s_1_1 294 # ASSIGN : s_1_2 292 # ASSIGN : s_1_3 16 # ASSIGN : s_1_4 17 # ASSIGN : s_1_5 647 # ASSIGN : s_2_0 272 # ASSIGN : s_2_1 279 # ASSIGN : s_2_2 310 # ASSIGN : s_2_3 1282 # ASSIGN : s_2_4 1280 # ASSIGN : s_2_5 1281 # ASSIGN : s_3_0 0 # ASSIGN : s_3_1 1 # ASSIGN : s_3_2 1284 # ASSIGN : s_3_3 698 # ASSIGN : s_3_4 18 # ASSIGN : s_3_5 1288 # ASSIGN : s_4_0 966 # ASSIGN : s_4_1 660 # ASSIGN : s_4_2 1285 # ASSIGN : s_4_3 661 # ASSIGN : s_4_4 975 # ASSIGN : s_4_5 0 # ASSIGN : s_5_0 277 # ASSIGN : s_5_1 674 # ASSIGN : s_5_2 1287 # ASSIGN : s_5_3 291 # ASSIGN : s_5_4 1288 # ASSIGN : s_5_5 1289 SHOW_RESULT 1290 END : 1290 (0 seconds) [Sun Jun 18 16:22:24 2006] SHOW_RESULT 1290 CPU : 0.199999999999996 = 0.199999999999996 + 0 + 0 + 0 # BOUND : makespan 1289 1290 MODIFY_CNF 1289 BEGIN : [Sun Jun 18 16:22:24 2006] MODIFY_CNF 1289 END : 29154886 bytes (0 seconds) [Sun Jun 18 16:22:24 2006] MODIFY_CNF 1289 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1289 BEGIN : [Sun Jun 18 16:22:24 2006] CMD : minisat /tmp/csp2sat9799.cnf /tmp/csp2sat9799.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 603515 1692398 | 201171 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 2 (1 /sec) decisions : 8 (5 /sec) propagations : 90072 (52984 /sec) conflict literals : 1 (0.00 % deleted) Memory used : 54.83 MB CPU time : 1.7 s UNSATISFIABLE VERIFY_CNF 1289 END : (2 seconds) [Sun Jun 18 16:22:26 2006] VERIFY_CNF 1289 CPU : 1.88 = 0 + 0 + 1.7 + 0.18 # RESULT : makespan 1289 UNSATISFIABLE # BOUND : makespan 1290 1290 MAIN END : (78 seconds) [Sun Jun 18 16:22:26 2006] MAIN CPU : 76.81 = 53 + 0.27 + 21.36 + 2.18