# TIMEOUT 18000 MAIN BEGIN : [Mon Jun 19 07:08:15 2006] READ BEGIN : csp/j8-per0-2.csp [Mon Jun 19 07:08:15 2006] READ END : csp/j8-per0-2.csp (1 seconds) [Mon Jun 19 07:08:16 2006] READ CPU : 0.96 = 0.93 + 0.03 + 0 + 0 # BOUND : makespan 1000 2737 GENERATE_CNF 2737 BEGIN : [Mon Jun 19 07:08:16 2006] GENERATE_CNF 2737 END : 177995 variables 2630988 clauses 60919687 bytes (102 seconds) [Mon Jun 19 07:09:58 2006] GENERATE_CNF 2737 CPU : 101 = 100.62 + 0.38 + 0 + 0 MODIFY_CNF 1868 BEGIN : [Mon Jun 19 07:09:58 2006] MODIFY_CNF 1868 END : 60919693 bytes (0 seconds) [Mon Jun 19 07:09:58 2006] MODIFY_CNF 1868 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1868 BEGIN : [Mon Jun 19 07:09:58 2006] CMD : minisat /tmp/csp2sat23031.cnf /tmp/csp2sat23031.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 1851015 5377106 | 617005 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 66 (15 /sec) decisions : 426 (98 /sec) propagations : 911716 (210558 /sec) conflict literals : 2082 (9.20 % deleted) Memory used : 109.83 MB CPU time : 4.33 s SATISFIABLE VERIFY_CNF 1868 END : (4 seconds) [Mon Jun 19 07:10:02 2006] VERIFY_CNF 1868 CPU : 4.86 = 0 + 0 + 4.44 + 0.42 # RESULT : makespan 1868 SATISFIABLE SHOW_RESULT 1868 BEGIN : [Mon Jun 19 07:10:02 2006] # ASSIGN : makespan 1868 # ASSIGN : s_0_0 1660 # ASSIGN : s_0_1 199 # ASSIGN : s_0_2 1 # ASSIGN : s_0_3 279 # ASSIGN : s_0_4 463 # ASSIGN : s_0_5 868 # ASSIGN : s_0_6 9 # ASSIGN : s_0_7 138 # ASSIGN : s_1_0 1596 # ASSIGN : s_1_1 40 # ASSIGN : s_1_2 70 # ASSIGN : s_1_3 590 # ASSIGN : s_1_4 681 # ASSIGN : s_1_5 1065 # ASSIGN : s_1_6 109 # ASSIGN : s_1_7 143 # ASSIGN : s_2_0 1573 # ASSIGN : s_2_1 486 # ASSIGN : s_2_2 116 # ASSIGN : s_2_3 803 # ASSIGN : s_2_4 938 # ASSIGN : s_2_5 1103 # ASSIGN : s_2_6 322 # ASSIGN : s_2_7 701 # ASSIGN : s_3_0 1485 # ASSIGN : s_3_1 716 # ASSIGN : s_3_2 241 # ASSIGN : s_3_3 1225 # ASSIGN : s_3_4 1138 # ASSIGN : s_3_5 1239 # ASSIGN : s_3_6 507 # ASSIGN : s_3_7 738 # ASSIGN : s_4_0 1224 # ASSIGN : s_4_1 912 # ASSIGN : s_4_2 448 # ASSIGN : s_4_3 1230 # ASSIGN : s_4_4 1196 # ASSIGN : s_4_5 1452 # ASSIGN : s_4_6 559 # ASSIGN : s_4_7 1093 # ASSIGN : s_5_0 479 # ASSIGN : s_5_1 1186 # ASSIGN : s_5_2 628 # ASSIGN : s_5_3 1467 # ASSIGN : s_5_4 1223 # ASSIGN : s_5_5 1711 # ASSIGN : s_5_6 650 # ASSIGN : s_5_7 1695 # ASSIGN : s_6_0 366 # ASSIGN : s_6_1 1223 # ASSIGN : s_6_2 943 # ASSIGN : s_6_3 1481 # ASSIGN : s_6_4 1294 # ASSIGN : s_6_5 1866 # ASSIGN : s_6_6 1220 # ASSIGN : s_6_7 1829 # ASSIGN : s_7_0 17 # ASSIGN : s_7_1 1431 # ASSIGN : s_7_2 1217 # ASSIGN : s_7_3 1866 # ASSIGN : s_7_4 1815 # ASSIGN : s_7_5 1867 # ASSIGN : s_7_6 1795 # ASSIGN : s_7_7 1832 SHOW_RESULT 1868 END : 1868 (1 seconds) [Mon Jun 19 07:10:03 2006] SHOW_RESULT 1868 CPU : 0.340000000000002 = 0.310000000000002 + 0.03 + 0 + 0 # BOUND : makespan 1000 1868 MODIFY_CNF 1434 BEGIN : [Mon Jun 19 07:10:03 2006] MODIFY_CNF 1434 END : 60919693 bytes (0 seconds) [Mon Jun 19 07:10:03 2006] MODIFY_CNF 1434 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1434 BEGIN : [Mon Jun 19 07:10:03 2006] CMD : minisat /tmp/csp2sat23031.cnf /tmp/csp2sat23031.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 1462151 4210514 | 487383 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 0 (0 /sec) decisions : 236 (61 /sec) propagations : 177995 (46232 /sec) conflict literals : 0 ( nan % deleted) Memory used : 109.83 MB CPU time : 3.85 s SATISFIABLE VERIFY_CNF 1434 END : (4 seconds) [Mon Jun 19 07:10:07 2006] VERIFY_CNF 1434 CPU : 4.32 = 0 + 0.01 + 3.94 + 0.37 # RESULT : makespan 1434 SATISFIABLE SHOW_RESULT 1434 BEGIN : [Mon Jun 19 07:10:07 2006] # ASSIGN : makespan 1434 # ASSIGN : s_0_0 917 # ASSIGN : s_0_1 124 # ASSIGN : s_0_2 2 # ASSIGN : s_0_3 660 # ASSIGN : s_0_4 442 # ASSIGN : s_0_5 204 # ASSIGN : s_0_6 10 # ASSIGN : s_0_7 434 # ASSIGN : s_1_0 1125 # ASSIGN : s_1_1 1189 # ASSIGN : s_1_2 983 # ASSIGN : s_1_3 7 # ASSIGN : s_1_4 144 # ASSIGN : s_1_5 401 # ASSIGN : s_1_6 110 # ASSIGN : s_1_7 439 # ASSIGN : s_2_0 10 # ASSIGN : s_2_1 1219 # ASSIGN : s_2_2 1022 # ASSIGN : s_2_3 98 # ASSIGN : s_2_4 700 # ASSIGN : s_2_5 489 # ASSIGN : s_2_6 281 # ASSIGN : s_2_7 886 # ASSIGN : s_3_0 33 # ASSIGN : s_3_1 211 # ASSIGN : s_3_2 238 # ASSIGN : s_3_3 233 # ASSIGN : s_3_4 865 # ASSIGN : s_3_5 625 # ASSIGN : s_3_6 445 # ASSIGN : s_3_7 923 # ASSIGN : s_4_0 121 # ASSIGN : s_4_1 602 # ASSIGN : s_4_2 127 # ASSIGN : s_4_3 275 # ASSIGN : s_4_4 1097 # ASSIGN : s_4_5 838 # ASSIGN : s_4_6 497 # ASSIGN : s_4_7 1278 # ASSIGN : s_5_0 172 # ASSIGN : s_5_1 462 # ASSIGN : s_5_2 548 # ASSIGN : s_5_3 574 # ASSIGN : s_5_4 1124 # ASSIGN : s_5_5 1226 # ASSIGN : s_5_6 588 # ASSIGN : s_5_7 1381 # ASSIGN : s_6_0 321 # ASSIGN : s_6_1 499 # ASSIGN : s_6_2 570 # ASSIGN : s_6_3 844 # ASSIGN : s_6_4 1195 # ASSIGN : s_6_5 1396 # ASSIGN : s_6_6 1192 # ASSIGN : s_6_7 1397 # ASSIGN : s_7_0 434 # ASSIGN : s_7_1 783 # ASSIGN : s_7_2 1147 # ASSIGN : s_7_3 1361 # ASSIGN : s_7_4 1382 # ASSIGN : s_7_5 1399 # ASSIGN : s_7_6 1362 # ASSIGN : s_7_7 1400 SHOW_RESULT 1434 END : 1434 (0 seconds) [Mon Jun 19 07:10:07 2006] SHOW_RESULT 1434 CPU : 0.329999999999998 = 0.329999999999998 + 0 + 0 + 0 # BOUND : makespan 1000 1434 MODIFY_CNF 1217 BEGIN : [Mon Jun 19 07:10:07 2006] MODIFY_CNF 1217 END : 60919693 bytes (0 seconds) [Mon Jun 19 07:10:07 2006] MODIFY_CNF 1217 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1217 BEGIN : [Mon Jun 19 07:10:07 2006] CMD : minisat /tmp/csp2sat23031.cnf /tmp/csp2sat23031.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 1267719 3627218 | 422573 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 5 (1 /sec) decisions : 189 (48 /sec) propagations : 217241 (55560 /sec) conflict literals : 69 (2.82 % deleted) Memory used : 109.83 MB CPU time : 3.91 s SATISFIABLE VERIFY_CNF 1217 END : (5 seconds) [Mon Jun 19 07:10:12 2006] VERIFY_CNF 1217 CPU : 4.33 = 0 + 0 + 4.01 + 0.32 # RESULT : makespan 1217 SATISFIABLE SHOW_RESULT 1217 BEGIN : [Mon Jun 19 07:10:12 2006] # ASSIGN : makespan 1217 # ASSIGN : s_0_0 1009 # ASSIGN : s_0_1 745 # ASSIGN : s_0_2 0 # ASSIGN : s_0_3 825 # ASSIGN : s_0_4 475 # ASSIGN : s_0_5 147 # ASSIGN : s_0_6 18 # ASSIGN : s_0_7 142 # ASSIGN : s_1_0 16 # ASSIGN : s_1_1 950 # ASSIGN : s_1_2 1178 # ASSIGN : s_1_3 599 # ASSIGN : s_1_4 693 # ASSIGN : s_1_5 80 # ASSIGN : s_1_6 118 # ASSIGN : s_1_7 152 # ASSIGN : s_2_0 957 # ASSIGN : s_2_1 980 # ASSIGN : s_2_2 480 # ASSIGN : s_2_3 690 # ASSIGN : s_2_4 1 # ASSIGN : s_2_5 344 # ASSIGN : s_2_6 166 # ASSIGN : s_2_7 653 # ASSIGN : s_3_0 405 # ASSIGN : s_3_1 1195 # ASSIGN : s_3_2 8 # ASSIGN : s_3_3 232 # ASSIGN : s_3_4 272 # ASSIGN : s_3_5 493 # ASSIGN : s_3_6 330 # ASSIGN : s_3_7 706 # ASSIGN : s_4_0 4 # ASSIGN : s_4_1 564 # ASSIGN : s_4_2 244 # ASSIGN : s_4_3 10 # ASSIGN : s_4_4 355 # ASSIGN : s_4_5 750 # ASSIGN : s_4_6 382 # ASSIGN : s_4_7 1061 # ASSIGN : s_5_0 253 # ASSIGN : s_5_1 163 # ASSIGN : s_5_2 215 # ASSIGN : s_5_3 237 # ASSIGN : s_5_4 402 # ASSIGN : s_5_5 1009 # ASSIGN : s_5_6 473 # ASSIGN : s_5_7 1164 # ASSIGN : s_6_0 138 # ASSIGN : s_6_1 879 # ASSIGN : s_6_2 605 # ASSIGN : s_6_3 251 # ASSIGN : s_6_4 958 # ASSIGN : s_6_5 1179 # ASSIGN : s_6_6 1159 # ASSIGN : s_6_7 1180 # ASSIGN : s_7_0 581 # ASSIGN : s_7_1 200 # ASSIGN : s_7_2 930 # ASSIGN : s_7_3 1144 # ASSIGN : s_7_4 1145 # ASSIGN : s_7_5 1182 # ASSIGN : s_7_6 1162 # ASSIGN : s_7_7 1183 SHOW_RESULT 1217 END : 1217 (0 seconds) [Mon Jun 19 07:10:12 2006] SHOW_RESULT 1217 CPU : 0.320000000000007 = 0.320000000000007 + 0 + 0 + 0 # BOUND : makespan 1000 1217 MODIFY_CNF 1108 BEGIN : [Mon Jun 19 07:10:12 2006] MODIFY_CNF 1108 END : 60919693 bytes (0 seconds) [Mon Jun 19 07:10:12 2006] MODIFY_CNF 1108 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1108 BEGIN : [Mon Jun 19 07:10:12 2006] CMD : minisat /tmp/csp2sat23031.cnf /tmp/csp2sat23031.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 1170055 3334226 | 390018 0 0 nan | 0.000 % | | 100 | 1170055 3334226 | 429019 100 2018 20.2 | 64.091 % | ============================================================================== restarts : 2 conflicts : 176 (33 /sec) decisions : 469 (87 /sec) propagations : 1481067 (275291 /sec) conflict literals : 3612 (19.75 % deleted) Memory used : 109.85 MB CPU time : 5.38 s SATISFIABLE VERIFY_CNF 1108 END : (6 seconds) [Mon Jun 19 07:10:18 2006] VERIFY_CNF 1108 CPU : 5.8 = 0 + 0 + 5.47 + 0.33 # RESULT : makespan 1108 SATISFIABLE SHOW_RESULT 1108 BEGIN : [Mon Jun 19 07:10:18 2006] # ASSIGN : makespan 1108 # ASSIGN : s_0_0 680 # ASSIGN : s_0_1 221 # ASSIGN : s_0_2 465 # ASSIGN : s_0_3 496 # ASSIGN : s_0_4 890 # ASSIGN : s_0_5 24 # ASSIGN : s_0_6 301 # ASSIGN : s_0_7 19 # ASSIGN : s_1_0 464 # ASSIGN : s_1_1 528 # ASSIGN : s_1_2 1047 # ASSIGN : s_1_3 48 # ASSIGN : s_1_4 150 # ASSIGN : s_1_5 426 # ASSIGN : s_1_6 14 # ASSIGN : s_1_7 558 # ASSIGN : s_2_0 569 # ASSIGN : s_2_1 306 # ASSIGN : s_2_2 8 # ASSIGN : s_2_3 139 # ASSIGN : s_2_4 594 # ASSIGN : s_2_5 759 # ASSIGN : s_2_6 941 # ASSIGN : s_2_7 521 # ASSIGN : s_3_0 592 # ASSIGN : s_3_1 570 # ASSIGN : s_3_2 687 # ASSIGN : s_3_3 682 # ASSIGN : s_3_4 4 # ASSIGN : s_3_5 895 # ASSIGN : s_3_6 114 # ASSIGN : s_3_7 166 # ASSIGN : s_4_0 888 # ASSIGN : s_4_1 2 # ASSIGN : s_4_2 894 # ASSIGN : s_4_3 274 # ASSIGN : s_4_4 861 # ASSIGN : s_4_5 500 # ASSIGN : s_4_6 183 # ASSIGN : s_4_7 1005 # ASSIGN : s_5_0 937 # ASSIGN : s_5_1 184 # ASSIGN : s_5_2 1086 # ASSIGN : s_5_3 34 # ASSIGN : s_5_4 79 # ASSIGN : s_5_5 246 # ASSIGN : s_5_6 401 # ASSIGN : s_5_7 150 # ASSIGN : s_6_0 2 # ASSIGN : s_6_1 672 # ASSIGN : s_6_2 133 # ASSIGN : s_6_3 757 # ASSIGN : s_6_4 407 # ASSIGN : s_6_5 1 # ASSIGN : s_6_6 1105 # ASSIGN : s_6_7 130 # ASSIGN : s_7_0 115 # ASSIGN : s_7_1 743 # ASSIGN : s_7_2 473 # ASSIGN : s_7_3 1107 # ASSIGN : s_7_4 62 # ASSIGN : s_7_5 23 # ASSIGN : s_7_6 94 # ASSIGN : s_7_7 28 SHOW_RESULT 1108 END : 1108 (0 seconds) [Mon Jun 19 07:10:18 2006] SHOW_RESULT 1108 CPU : 0.309999999999988 = 0.309999999999988 + 0 + 0 + 0 # BOUND : makespan 1000 1108 MODIFY_CNF 1054 BEGIN : [Mon Jun 19 07:10:18 2006] MODIFY_CNF 1054 END : 60919692 bytes (0 seconds) [Mon Jun 19 07:10:18 2006] MODIFY_CNF 1054 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1054 BEGIN : [Mon Jun 19 07:10:18 2006] CMD : minisat /tmp/csp2sat23031.cnf /tmp/csp2sat23031.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 1121671 3189074 | 373890 0 0 nan | 0.000 % | | 100 | 1121671 3189074 | 411279 100 2428 24.3 | 66.063 % | | 250 | 1121671 3189074 | 452406 250 4639 18.6 | 66.063 % | | 475 | 1121671 3189074 | 497647 475 8347 17.6 | 66.063 % | | 812 | 1121671 3189074 | 547412 812 13159 16.2 | 66.063 % | ============================================================================== restarts : 5 conflicts : 895 (85 /sec) decisions : 1414 (134 /sec) propagations : 6887202 (650964 /sec) conflict literals : 14204 (30.76 % deleted) Memory used : 109.85 MB CPU time : 10.58 s SATISFIABLE VERIFY_CNF 1054 END : (11 seconds) [Mon Jun 19 07:10:29 2006] VERIFY_CNF 1054 CPU : 11 = 0 + 0 + 10.66 + 0.34 # RESULT : makespan 1054 SATISFIABLE SHOW_RESULT 1054 BEGIN : [Mon Jun 19 07:10:29 2006] # ASSIGN : makespan 1054 # ASSIGN : s_0_0 549 # ASSIGN : s_0_1 206 # ASSIGN : s_0_2 312 # ASSIGN : s_0_3 22 # ASSIGN : s_0_4 331 # ASSIGN : s_0_5 857 # ASSIGN : s_0_6 757 # ASSIGN : s_0_7 1 # ASSIGN : s_1_0 479 # ASSIGN : s_1_1 577 # ASSIGN : s_1_2 320 # ASSIGN : s_1_3 359 # ASSIGN : s_1_4 63 # ASSIGN : s_1_5 8 # ASSIGN : s_1_6 543 # ASSIGN : s_1_7 607 # ASSIGN : s_2_0 867 # ASSIGN : s_2_1 362 # ASSIGN : s_2_2 577 # ASSIGN : s_2_3 224 # ASSIGN : s_2_4 702 # ASSIGN : s_2_5 46 # ASSIGN : s_2_6 890 # ASSIGN : s_2_7 9 # ASSIGN : s_3_0 759 # ASSIGN : s_3_1 668 # ASSIGN : s_3_2 847 # ASSIGN : s_3_3 450 # ASSIGN : s_3_4 5 # ASSIGN : s_3_5 455 # ASSIGN : s_3_6 705 # ASSIGN : s_3_7 86 # ASSIGN : s_4_0 1048 # ASSIGN : s_4_1 1 # ASSIGN : s_4_2 707 # ASSIGN : s_4_3 818 # ASSIGN : s_4_4 675 # ASSIGN : s_4_5 182 # ASSIGN : s_4_6 579 # ASSIGN : s_4_7 441 # ASSIGN : s_5_0 891 # ASSIGN : s_5_1 631 # ASSIGN : s_5_2 825 # ASSIGN : s_5_3 1040 # ASSIGN : s_5_4 560 # ASSIGN : s_5_5 670 # ASSIGN : s_5_6 7 # ASSIGN : s_5_7 544 # ASSIGN : s_6_0 357 # ASSIGN : s_6_1 286 # ASSIGN : s_6_2 12 # ASSIGN : s_6_3 470 # ASSIGN : s_6_4 867 # ASSIGN : s_6_5 856 # ASSIGN : s_6_6 864 # ASSIGN : s_6_7 6 # ASSIGN : s_7_0 8 # ASSIGN : s_7_1 690 # ASSIGN : s_7_2 359 # ASSIGN : s_7_3 7 # ASSIGN : s_7_4 652 # ASSIGN : s_7_5 669 # ASSIGN : s_7_6 670 # ASSIGN : s_7_7 573 SHOW_RESULT 1054 END : 1054 (1 seconds) [Mon Jun 19 07:10:30 2006] SHOW_RESULT 1054 CPU : 0.310000000000006 = 0.290000000000006 + 0.02 + 0 + 0 # BOUND : makespan 1000 1054 MODIFY_CNF 1027 BEGIN : [Mon Jun 19 07:10:30 2006] MODIFY_CNF 1027 END : 60919692 bytes (0 seconds) [Mon Jun 19 07:10:30 2006] MODIFY_CNF 1027 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1027 BEGIN : [Mon Jun 19 07:10:30 2006] CMD : minisat /tmp/csp2sat23031.cnf /tmp/csp2sat23031.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 1097479 3116498 | 365826 0 0 nan | 0.000 % | | 101 | 1097479 3116498 | 402408 101 3053 30.2 | 67.049 % | | 251 | 1097480 3116498 | 442649 250 6527 26.1 | 67.049 % | | 476 | 1097480 3116498 | 486914 475 9145 19.3 | 67.049 % | | 813 | 1097480 3116498 | 535605 812 13243 16.3 | 67.049 % | | 1321 | 1097480 3116498 | 589166 1320 20476 15.5 | 67.049 % | | 2081 | 1097480 3116498 | 648083 2080 30527 14.7 | 67.049 % | | 3220 | 1097486 3116498 | 712891 3213 44968 14.0 | 67.049 % | ============================================================================== restarts : 8 conflicts : 4226 (107 /sec) decisions : 5221 (132 /sec) propagations : 34824108 (882070 /sec) conflict literals : 55901 (35.87 % deleted) Memory used : 109.11 MB CPU time : 39.48 s UNSATISFIABLE VERIFY_CNF 1027 END : (39 seconds) [Mon Jun 19 07:11:09 2006] VERIFY_CNF 1027 CPU : 39.79 = 0 + 0 + 39.48 + 0.31 # RESULT : makespan 1027 UNSATISFIABLE # BOUND : makespan 1028 1054 MODIFY_CNF 1041 BEGIN : [Mon Jun 19 07:11:09 2006] MODIFY_CNF 1041 END : 60919692 bytes (0 seconds) [Mon Jun 19 07:11:09 2006] MODIFY_CNF 1041 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1041 BEGIN : [Mon Jun 19 07:11:09 2006] CMD : minisat /tmp/csp2sat23031.cnf /tmp/csp2sat23031.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 1110023 3154130 | 370007 0 0 nan | 0.000 % | | 100 | 1110023 3154130 | 407007 100 2250 22.5 | 66.538 % | | 250 | 1110023 3154130 | 447708 250 4882 19.5 | 66.538 % | | 476 | 1110023 3154130 | 492479 476 8237 17.3 | 66.538 % | | 813 | 1110023 3154130 | 541727 813 12445 15.3 | 66.538 % | | 1319 | 1110023 3154130 | 595899 1319 20070 15.2 | 66.538 % | | 2079 | 1110023 3154130 | 655489 2079 30165 14.5 | 66.538 % | | 3220 | 1110025 3154130 | 721038 3218 45271 14.1 | 66.538 % | | 4928 | 1110025 3154130 | 793142 4926 73708 15.0 | 66.538 % | | 7490 | 1110025 3154130 | 872457 7488 115425 15.4 | 66.538 % | | 11334 | 1104663 3138089 | 959702 9285 138783 14.9 | 66.786 % | ============================================================================== restarts : 11 conflicts : 13589 (115 /sec) decisions : 16524 (140 /sec) propagations : 109480134 (927562 /sec) conflict literals : 207599 (37.86 % deleted) Memory used : 109.11 MB CPU time : 118.03 s UNSATISFIABLE VERIFY_CNF 1041 END : (119 seconds) [Mon Jun 19 07:13:08 2006] VERIFY_CNF 1041 CPU : 118.49 = 0 + 0 + 118.03 + 0.46 # RESULT : makespan 1041 UNSATISFIABLE # BOUND : makespan 1042 1054 MODIFY_CNF 1048 BEGIN : [Mon Jun 19 07:13:08 2006] MODIFY_CNF 1048 END : 60919692 bytes (0 seconds) [Mon Jun 19 07:13:08 2006] MODIFY_CNF 1048 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1048 BEGIN : [Mon Jun 19 07:13:08 2006] CMD : minisat /tmp/csp2sat23031.cnf /tmp/csp2sat23031.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 1116295 3172946 | 372098 0 0 nan | 0.000 % | | 101 | 1116295 3172946 | 409307 101 2256 22.3 | 66.282 % | | 254 | 1116295 3172946 | 450238 254 4757 18.7 | 66.282 % | | 483 | 1116295 3172946 | 495262 483 7615 15.8 | 66.282 % | | 820 | 1116295 3172946 | 544788 820 11718 14.3 | 66.282 % | | 1327 | 1116295 3172946 | 599267 1327 20948 15.8 | 66.282 % | | 2087 | 1116295 3172946 | 659194 2087 31542 15.1 | 66.282 % | | 3226 | 1116295 3172946 | 725113 3226 50946 15.8 | 66.282 % | | 4934 | 1116295 3172946 | 797625 4934 77295 15.7 | 66.282 % | | 7498 | 1116295 3172946 | 877387 7498 117752 15.7 | 66.282 % | | 11342 | 1116295 3172946 | 965126 11342 188621 16.6 | 66.282 % | | 17108 | 1111365 3158195 | 1061639 15261 251982 16.5 | 66.510 % | ============================================================================== restarts : 12 conflicts : 21389 (115 /sec) decisions : 25447 (136 /sec) propagations : 172896636 (927060 /sec) conflict literals : 355150 (37.90 % deleted) Memory used : 109.13 MB CPU time : 186.5 s UNSATISFIABLE VERIFY_CNF 1048 END : (187 seconds) [Mon Jun 19 07:16:15 2006] VERIFY_CNF 1048 CPU : 186.86 = 0 + 0 + 186.5 + 0.36 # RESULT : makespan 1048 UNSATISFIABLE # BOUND : makespan 1049 1054 MODIFY_CNF 1051 BEGIN : [Mon Jun 19 07:16:15 2006] MODIFY_CNF 1051 END : 60919692 bytes (0 seconds) [Mon Jun 19 07:16:15 2006] MODIFY_CNF 1051 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1051 BEGIN : [Mon Jun 19 07:16:15 2006] CMD : minisat /tmp/csp2sat23031.cnf /tmp/csp2sat23031.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 1118983 3181010 | 372994 0 0 nan | 0.000 % | | 100 | 1118983 3181010 | 410293 100 1893 18.9 | 66.173 % | | 250 | 1118983 3181010 | 451322 250 4695 18.8 | 66.173 % | | 475 | 1118983 3181010 | 496455 475 8487 17.9 | 66.173 % | | 815 | 1118983 3181010 | 546100 815 15463 19.0 | 66.173 % | | 1321 | 1118984 3181010 | 600710 1320 23534 17.8 | 66.173 % | | 2080 | 1118984 3181010 | 660781 2079 36260 17.4 | 66.173 % | | 3219 | 1118984 3181010 | 726859 3218 54992 17.1 | 66.173 % | | 4929 | 1118984 3181010 | 799545 4928 82980 16.8 | 66.173 % | | 7491 | 1118984 3181010 | 879500 7490 126461 16.9 | 66.173 % | | 11335 | 1118984 3181010 | 967450 11334 189822 16.7 | 66.173 % | | 17103 | 1118985 3181010 | 1064195 17101 293944 17.2 | 66.173 % | | 25752 | 1097495 3116648 | 1170614 16750 258047 15.4 | 67.133 % | ============================================================================== restarts : 13 conflicts : 26293 (111 /sec) decisions : 31312 (133 /sec) propagations : 213451334 (904762 /sec) conflict literals : 447232 (39.27 % deleted) Memory used : 109.15 MB CPU time : 235.92 s UNSATISFIABLE VERIFY_CNF 1051 END : (236 seconds) [Mon Jun 19 07:20:11 2006] VERIFY_CNF 1051 CPU : 236.39 = 0 + 0 + 235.92 + 0.47 # RESULT : makespan 1051 UNSATISFIABLE # BOUND : makespan 1052 1054 MODIFY_CNF 1053 BEGIN : [Mon Jun 19 07:20:11 2006] MODIFY_CNF 1053 END : 60919692 bytes (0 seconds) [Mon Jun 19 07:20:11 2006] MODIFY_CNF 1053 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1053 BEGIN : [Mon Jun 19 07:20:11 2006] CMD : minisat /tmp/csp2sat23031.cnf /tmp/csp2sat23031.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 1120775 3186386 | 373591 0 0 nan | 0.000 % | | 100 | 1120775 3186386 | 410950 100 2134 21.3 | 66.100 % | | 251 | 1120775 3186386 | 452045 251 4949 19.7 | 66.100 % | | 477 | 1120775 3186386 | 497249 477 9469 19.9 | 66.100 % | | 814 | 1120775 3186386 | 546974 814 14453 17.8 | 66.100 % | | 1320 | 1120775 3186386 | 601672 1320 22625 17.1 | 66.100 % | | 2080 | 1120775 3186386 | 661839 2080 34337 16.5 | 66.100 % | | 3219 | 1120775 3186386 | 728023 3219 53114 16.5 | 66.100 % | ============================================================================== restarts : 8 conflicts : 4419 (116 /sec) decisions : 5818 (152 /sec) propagations : 34949600 (914193 /sec) conflict literals : 72856 (33.82 % deleted) Memory used : 109.85 MB CPU time : 38.23 s SATISFIABLE VERIFY_CNF 1053 END : (39 seconds) [Mon Jun 19 07:20:50 2006] VERIFY_CNF 1053 CPU : 38.7299999999999 = 0 + 0 + 38.3199999999999 + 0.41 # RESULT : makespan 1053 SATISFIABLE SHOW_RESULT 1053 BEGIN : [Mon Jun 19 07:20:50 2006] # ASSIGN : makespan 1053 # ASSIGN : s_0_0 350 # ASSIGN : s_0_1 259 # ASSIGN : s_0_2 2 # ASSIGN : s_0_3 864 # ASSIGN : s_0_4 38 # ASSIGN : s_0_5 663 # ASSIGN : s_0_6 563 # ASSIGN : s_0_7 1048 # ASSIGN : s_1_0 876 # ASSIGN : s_1_1 985 # ASSIGN : s_1_2 10 # ASSIGN : s_1_3 523 # ASSIGN : s_1_4 614 # ASSIGN : s_1_5 1015 # ASSIGN : s_1_6 947 # ASSIGN : s_1_7 73 # ASSIGN : s_2_0 664 # ASSIGN : s_2_1 44 # ASSIGN : s_2_2 263 # ASSIGN : s_2_3 388 # ASSIGN : s_2_4 871 # ASSIGN : s_2_5 527 # ASSIGN : s_2_6 687 # ASSIGN : s_2_7 7 # ASSIGN : s_3_0 558 # ASSIGN : s_3_1 22 # ASSIGN : s_3_2 49 # ASSIGN : s_3_3 3 # ASSIGN : s_3_4 256 # ASSIGN : s_3_5 314 # ASSIGN : s_3_6 1001 # ASSIGN : s_3_7 646 # ASSIGN : s_4_0 845 # ASSIGN : s_4_1 339 # ASSIGN : s_4_2 942 # ASSIGN : s_4_3 623 # ASSIGN : s_4_4 11 # ASSIGN : s_4_5 55 # ASSIGN : s_4_6 851 # ASSIGN : s_4_7 520 # ASSIGN : s_5_0 696 # ASSIGN : s_5_1 1016 # ASSIGN : s_5_2 644 # ASSIGN : s_5_3 846 # ASSIGN : s_5_4 543 # ASSIGN : s_5_5 860 # ASSIGN : s_5_6 7 # ASSIGN : s_5_7 628 # ASSIGN : s_6_0 940 # ASSIGN : s_6_1 546 # ASSIGN : s_6_2 666 # ASSIGN : s_6_3 8 # ASSIGN : s_6_4 356 # ASSIGN : s_6_5 7 # ASSIGN : s_6_6 4 # ASSIGN : s_6_7 1 # ASSIGN : s_7_0 1 # ASSIGN : s_7_1 617 # ASSIGN : s_7_2 403 # ASSIGN : s_7_3 387 # ASSIGN : s_7_4 1036 # ASSIGN : s_7_5 0 # ASSIGN : s_7_6 981 # ASSIGN : s_7_7 1002 SHOW_RESULT 1053 END : 1053 (0 seconds) [Mon Jun 19 07:20:50 2006] SHOW_RESULT 1053 CPU : 0.310000000000002 = 0.310000000000002 + 0 + 0 + 0 # BOUND : makespan 1052 1053 MODIFY_CNF 1052 BEGIN : [Mon Jun 19 07:20:50 2006] MODIFY_CNF 1052 END : 60919692 bytes (0 seconds) [Mon Jun 19 07:20:50 2006] MODIFY_CNF 1052 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1052 BEGIN : [Mon Jun 19 07:20:50 2006] CMD : minisat /tmp/csp2sat23031.cnf /tmp/csp2sat23031.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 1119879 3183698 | 373293 0 0 nan | 0.000 % | | 100 | 1119879 3183698 | 410622 100 2146 21.5 | 66.136 % | | 250 | 1119879 3183698 | 451684 250 4501 18.0 | 66.136 % | | 477 | 1119879 3183698 | 496852 477 7946 16.7 | 66.136 % | | 814 | 1119879 3183698 | 546538 814 13754 16.9 | 66.136 % | | 1321 | 1119879 3183698 | 601192 1321 21416 16.2 | 66.136 % | | 2080 | 1119879 3183698 | 661311 2080 34346 16.5 | 66.136 % | | 3220 | 1119879 3183698 | 727442 3220 52310 16.2 | 66.136 % | | 4928 | 1119879 3183698 | 800186 4928 81901 16.6 | 66.136 % | | 7490 | 1119879 3183698 | 880205 7490 125545 16.8 | 66.136 % | | 11334 | 1119879 3183698 | 968225 11334 190065 16.8 | 66.136 % | ============================================================================== restarts : 11 conflicts : 13403 (117 /sec) decisions : 16419 (143 /sec) propagations : 107659104 (939926 /sec) conflict literals : 224312 (37.63 % deleted) Memory used : 109.85 MB CPU time : 114.54 s SATISFIABLE VERIFY_CNF 1052 END : (115 seconds) [Mon Jun 19 07:22:45 2006] VERIFY_CNF 1052 CPU : 115 = 0 + 0 + 114.64 + 0.36 # RESULT : makespan 1052 SATISFIABLE SHOW_RESULT 1052 BEGIN : [Mon Jun 19 07:22:45 2006] # ASSIGN : makespan 1052 # ASSIGN : s_0_0 495 # ASSIGN : s_0_1 720 # ASSIGN : s_0_2 1 # ASSIGN : s_0_3 14 # ASSIGN : s_0_4 834 # ASSIGN : s_0_5 198 # ASSIGN : s_0_6 395 # ASSIGN : s_0_7 9 # ASSIGN : s_1_0 120 # ASSIGN : s_1_1 47 # ASSIGN : s_1_2 1013 # ASSIGN : s_1_3 449 # ASSIGN : s_1_4 184 # ASSIGN : s_1_5 5 # ASSIGN : s_1_6 86 # ASSIGN : s_1_7 566 # ASSIGN : s_2_0 208 # ASSIGN : s_2_1 800 # ASSIGN : s_2_2 675 # ASSIGN : s_2_3 540 # ASSIGN : s_2_4 19 # ASSIGN : s_2_5 399 # ASSIGN : s_2_6 231 # ASSIGN : s_2_7 1015 # ASSIGN : s_3_0 407 # ASSIGN : s_3_1 1025 # ASSIGN : s_3_2 806 # ASSIGN : s_3_3 1047 # ASSIGN : s_3_4 748 # ASSIGN : s_3_5 535 # ASSIGN : s_3_6 0 # ASSIGN : s_3_7 52 # ASSIGN : s_4_0 1 # ASSIGN : s_4_1 539 # ASSIGN : s_4_2 12 # ASSIGN : s_4_3 214 # ASSIGN : s_4_4 721 # ASSIGN : s_4_5 793 # ASSIGN : s_4_6 123 # ASSIGN : s_4_7 436 # ASSIGN : s_5_0 249 # ASSIGN : s_5_1 6 # ASSIGN : s_5_2 398 # ASSIGN : s_5_3 200 # ASSIGN : s_5_4 441 # ASSIGN : s_5_5 43 # ASSIGN : s_5_6 516 # ASSIGN : s_5_7 420 # ASSIGN : s_6_0 7 # ASSIGN : s_6_1 441 # ASSIGN : s_6_2 124 # ASSIGN : s_6_3 699 # ASSIGN : s_6_4 512 # ASSIGN : s_6_5 4 # ASSIGN : s_6_6 120 # ASSIGN : s_6_7 417 # ASSIGN : s_7_0 703 # ASSIGN : s_7_1 77 # ASSIGN : s_7_2 461 # ASSIGN : s_7_3 698 # ASSIGN : s_7_4 1 # ASSIGN : s_7_5 0 # ASSIGN : s_7_6 57 # ASSIGN : s_7_7 18 SHOW_RESULT 1052 END : 1052 (0 seconds) [Mon Jun 19 07:22:45 2006] SHOW_RESULT 1052 CPU : 0.310000000000002 = 0.310000000000002 + 0 + 0 + 0 # BOUND : makespan 1052 1052 MAIN END : (870 seconds) [Mon Jun 19 07:22:45 2006] MAIN CPU : 869.82 = 103.78 + 0.48 + 761.41 + 4.15