# TIMEOUT 18000 MAIN BEGIN : [Sun Jun 18 20:10:01 2006] READ BEGIN : csp/j6-per10-2.csp [Sun Jun 18 20:10:01 2006] READ END : csp/j6-per10-2.csp (0 seconds) [Sun Jun 18 20:10:01 2006] READ CPU : 0.42 = 0.42 + 0 + 0 + 0 # BOUND : makespan 1000 2117 GENERATE_CNF 2117 BEGIN : [Sun Jun 18 20:10:01 2006] GENERATE_CNF 2117 END : 77799 variables 823964 clauses 17311924 bytes (32 seconds) [Sun Jun 18 20:10:33 2006] GENERATE_CNF 2117 CPU : 30.93 = 30.8 + 0.13 + 0 + 0 MODIFY_CNF 1558 BEGIN : [Sun Jun 18 20:10:33 2006] MODIFY_CNF 1558 END : 17311930 bytes (0 seconds) [Sun Jun 18 20:10:33 2006] MODIFY_CNF 1558 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1558 BEGIN : [Sun Jun 18 20:10:33 2006] CMD : minisat /tmp/csp2sat14214.cnf /tmp/csp2sat14214.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 622107 1789466 | 207369 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 14 (13 /sec) decisions : 168 (153 /sec) propagations : 178311 (162101 /sec) conflict literals : 239 (19.53 % deleted) Memory used : 36.00 MB CPU time : 1.1 s SATISFIABLE VERIFY_CNF 1558 END : (1 seconds) [Sun Jun 18 20:10:34 2006] VERIFY_CNF 1558 CPU : 1.24 = 0 + 0 + 1.13 + 0.11 # RESULT : makespan 1558 SATISFIABLE SHOW_RESULT 1558 BEGIN : [Sun Jun 18 20:10:34 2006] # ASSIGN : makespan 1558 # ASSIGN : s_0_0 1436 # ASSIGN : s_0_1 279 # ASSIGN : s_0_2 257 # ASSIGN : s_0_3 47 # ASSIGN : s_0_4 113 # ASSIGN : s_0_5 658 # ASSIGN : s_1_0 17 # ASSIGN : s_1_1 604 # ASSIGN : s_1_2 378 # ASSIGN : s_1_3 91 # ASSIGN : s_1_4 778 # ASSIGN : s_1_5 959 # ASSIGN : s_2_0 215 # ASSIGN : s_2_1 736 # ASSIGN : s_2_2 620 # ASSIGN : s_2_3 314 # ASSIGN : s_2_4 782 # ASSIGN : s_2_5 1261 # ASSIGN : s_3_0 326 # ASSIGN : s_3_1 1066 # ASSIGN : s_3_2 698 # ASSIGN : s_3_3 354 # ASSIGN : s_3_4 1218 # ASSIGN : s_3_5 1489 # ASSIGN : s_4_0 498 # ASSIGN : s_4_1 1248 # ASSIGN : s_4_2 987 # ASSIGN : s_4_3 687 # ASSIGN : s_4_4 1317 # ASSIGN : s_4_5 1549 # ASSIGN : s_5_0 658 # ASSIGN : s_5_1 1343 # ASSIGN : s_5_2 1201 # ASSIGN : s_5_3 1175 # ASSIGN : s_5_4 1542 # ASSIGN : s_5_5 1552 SHOW_RESULT 1558 END : 1558 (0 seconds) [Sun Jun 18 20:10:34 2006] SHOW_RESULT 1558 CPU : 0.139999999999999 = 0.129999999999999 + 0.00999999999999998 + 0 + 0 # BOUND : makespan 1000 1558 MODIFY_CNF 1279 BEGIN : [Sun Jun 18 20:10:34 2006] MODIFY_CNF 1279 END : 17311930 bytes (0 seconds) [Sun Jun 18 20:10:34 2006] MODIFY_CNF 1279 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1279 BEGIN : [Sun Jun 18 20:10:34 2006] CMD : minisat /tmp/csp2sat14214.cnf /tmp/csp2sat14214.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 521667 1488146 | 173889 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 1 (1 /sec) decisions : 107 (99 /sec) propagations : 79043 (73188 /sec) conflict literals : 6 (0.00 % deleted) Memory used : 36.00 MB CPU time : 1.08 s SATISFIABLE VERIFY_CNF 1279 END : (1 seconds) [Sun Jun 18 20:10:35 2006] VERIFY_CNF 1279 CPU : 1.22 = 0 + 0 + 1.12 + 0.1 # RESULT : makespan 1279 SATISFIABLE SHOW_RESULT 1279 BEGIN : [Sun Jun 18 20:10:35 2006] # ASSIGN : makespan 1279 # ASSIGN : s_0_0 1157 # ASSIGN : s_0_1 733 # ASSIGN : s_0_2 16 # ASSIGN : s_0_3 56 # ASSIGN : s_0_4 122 # ASSIGN : s_0_5 266 # ASSIGN : s_1_0 14 # ASSIGN : s_1_1 323 # ASSIGN : s_1_2 869 # ASSIGN : s_1_3 100 # ASSIGN : s_1_4 499 # ASSIGN : s_1_5 567 # ASSIGN : s_2_0 196 # ASSIGN : s_2_1 1233 # ASSIGN : s_2_2 38 # ASSIGN : s_2_3 365 # ASSIGN : s_2_4 503 # ASSIGN : s_2_5 982 # ASSIGN : s_3_0 88 # ASSIGN : s_3_1 1058 # ASSIGN : s_3_2 116 # ASSIGN : s_3_3 405 # ASSIGN : s_3_4 939 # ASSIGN : s_3_5 1210 # ASSIGN : s_4_0 295 # ASSIGN : s_4_1 455 # ASSIGN : s_4_2 524 # ASSIGN : s_4_3 738 # ASSIGN : s_4_4 1038 # ASSIGN : s_4_5 1270 # ASSIGN : s_5_0 578 # ASSIGN : s_5_1 124 # ASSIGN : s_5_2 1095 # ASSIGN : s_5_3 1237 # ASSIGN : s_5_4 1263 # ASSIGN : s_5_5 1273 SHOW_RESULT 1279 END : 1279 (1 seconds) [Sun Jun 18 20:10:36 2006] SHOW_RESULT 1279 CPU : 0.130000000000001 = 0.120000000000001 + 0.01 + 0 + 0 # BOUND : makespan 1000 1279 MODIFY_CNF 1139 BEGIN : [Sun Jun 18 20:10:36 2006] MODIFY_CNF 1139 END : 17311930 bytes (0 seconds) [Sun Jun 18 20:10:36 2006] MODIFY_CNF 1139 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1139 BEGIN : [Sun Jun 18 20:10:36 2006] CMD : minisat /tmp/csp2sat14214.cnf /tmp/csp2sat14214.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 471267 1336946 | 157089 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 4 (4 /sec) decisions : 87 (79 /sec) propagations : 83715 (76105 /sec) conflict literals : 29 (0.00 % deleted) Memory used : 36.00 MB CPU time : 1.1 s SATISFIABLE VERIFY_CNF 1139 END : (1 seconds) [Sun Jun 18 20:10:37 2006] VERIFY_CNF 1139 CPU : 1.23 = 0 + 0 + 1.14 + 0.09 # RESULT : makespan 1139 SATISFIABLE SHOW_RESULT 1139 BEGIN : [Sun Jun 18 20:10:37 2006] # ASSIGN : makespan 1139 # ASSIGN : s_0_0 1017 # ASSIGN : s_0_1 593 # ASSIGN : s_0_2 6 # ASSIGN : s_0_3 42 # ASSIGN : s_0_4 86 # ASSIGN : s_0_5 230 # ASSIGN : s_1_0 168 # ASSIGN : s_1_1 25 # ASSIGN : s_1_2 284 # ASSIGN : s_1_3 874 # ASSIGN : s_1_4 280 # ASSIGN : s_1_5 531 # ASSIGN : s_2_0 18 # ASSIGN : s_2_1 157 # ASSIGN : s_2_2 1061 # ASSIGN : s_2_3 117 # ASSIGN : s_2_4 363 # ASSIGN : s_2_5 833 # ASSIGN : s_3_0 140 # ASSIGN : s_3_1 918 # ASSIGN : s_3_2 510 # ASSIGN : s_3_3 177 # ASSIGN : s_3_4 799 # ASSIGN : s_3_5 1070 # ASSIGN : s_4_0 242 # ASSIGN : s_4_1 505 # ASSIGN : s_4_2 28 # ASSIGN : s_4_3 574 # ASSIGN : s_4_4 898 # ASSIGN : s_4_5 1130 # ASSIGN : s_5_0 402 # ASSIGN : s_5_1 203 # ASSIGN : s_5_2 919 # ASSIGN : s_5_3 1097 # ASSIGN : s_5_4 1123 # ASSIGN : s_5_5 1133 SHOW_RESULT 1139 END : 1139 (0 seconds) [Sun Jun 18 20:10:37 2006] SHOW_RESULT 1139 CPU : 0.18 = 0.18 + 0 + 0 + 0 # BOUND : makespan 1000 1139 MODIFY_CNF 1069 BEGIN : [Sun Jun 18 20:10:37 2006] MODIFY_CNF 1069 END : 17311929 bytes (0 seconds) [Sun Jun 18 20:10:37 2006] MODIFY_CNF 1069 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1069 BEGIN : [Sun Jun 18 20:10:37 2006] CMD : minisat /tmp/csp2sat14214.cnf /tmp/csp2sat14214.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 446067 1261346 | 148689 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 11 (10 /sec) decisions : 83 (73 /sec) propagations : 152850 (134079 /sec) conflict literals : 193 (21.22 % deleted) Memory used : 36.00 MB CPU time : 1.14 s SATISFIABLE VERIFY_CNF 1069 END : (1 seconds) [Sun Jun 18 20:10:38 2006] VERIFY_CNF 1069 CPU : 1.28 = 0 + 0 + 1.18 + 0.1 # RESULT : makespan 1069 SATISFIABLE SHOW_RESULT 1069 BEGIN : [Sun Jun 18 20:10:38 2006] # ASSIGN : makespan 1069 # ASSIGN : s_0_0 303 # ASSIGN : s_0_1 556 # ASSIGN : s_0_2 534 # ASSIGN : s_0_3 1025 # ASSIGN : s_0_4 881 # ASSIGN : s_0_5 2 # ASSIGN : s_1_0 7 # ASSIGN : s_1_1 937 # ASSIGN : s_1_2 620 # ASSIGN : s_1_3 85 # ASSIGN : s_1_4 81 # ASSIGN : s_1_5 318 # ASSIGN : s_2_0 942 # ASSIGN : s_2_1 891 # ASSIGN : s_2_2 6 # ASSIGN : s_2_3 608 # ASSIGN : s_2_4 86 # ASSIGN : s_2_5 663 # ASSIGN : s_3_0 1041 # ASSIGN : s_3_1 74 # ASSIGN : s_3_2 233 # ASSIGN : s_3_3 648 # ASSIGN : s_3_4 522 # ASSIGN : s_3_5 981 # ASSIGN : s_4_0 143 # ASSIGN : s_4_1 5 # ASSIGN : s_4_2 846 # ASSIGN : s_4_3 308 # ASSIGN : s_4_4 621 # ASSIGN : s_4_5 1060 # ASSIGN : s_5_0 425 # ASSIGN : s_5_1 226 # ASSIGN : s_5_2 84 # ASSIGN : s_5_3 58 # ASSIGN : s_5_4 1053 # ASSIGN : s_5_5 1063 SHOW_RESULT 1069 END : 1069 (0 seconds) [Sun Jun 18 20:10:38 2006] SHOW_RESULT 1069 CPU : 0.129999999999999 = 0.109999999999999 + 0.02 + 0 + 0 # BOUND : makespan 1000 1069 MODIFY_CNF 1034 BEGIN : [Sun Jun 18 20:10:38 2006] MODIFY_CNF 1034 END : 17311929 bytes (0 seconds) [Sun Jun 18 20:10:38 2006] MODIFY_CNF 1034 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1034 BEGIN : [Sun Jun 18 20:10:38 2006] CMD : minisat /tmp/csp2sat14214.cnf /tmp/csp2sat14214.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 433467 1223546 | 144489 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 7 (6 /sec) decisions : 81 (72 /sec) propagations : 121349 (107388 /sec) conflict literals : 61 (19.74 % deleted) Memory used : 36.00 MB CPU time : 1.13 s SATISFIABLE VERIFY_CNF 1034 END : (2 seconds) [Sun Jun 18 20:10:40 2006] VERIFY_CNF 1034 CPU : 1.29 = 0.0100000000000016 + 0 + 1.17 + 0.11 # RESULT : makespan 1034 SATISFIABLE SHOW_RESULT 1034 BEGIN : [Sun Jun 18 20:10:40 2006] # ASSIGN : makespan 1034 # ASSIGN : s_0_0 813 # ASSIGN : s_0_1 324 # ASSIGN : s_0_2 1 # ASSIGN : s_0_3 990 # ASSIGN : s_0_4 649 # ASSIGN : s_0_5 23 # ASSIGN : s_1_0 13 # ASSIGN : s_1_1 898 # ASSIGN : s_1_2 650 # ASSIGN : s_1_3 109 # ASSIGN : s_1_4 1030 # ASSIGN : s_1_5 348 # ASSIGN : s_2_0 935 # ASSIGN : s_2_1 57 # ASSIGN : s_2_2 572 # ASSIGN : s_2_3 17 # ASSIGN : s_2_4 136 # ASSIGN : s_2_5 707 # ASSIGN : s_3_0 604 # ASSIGN : s_3_1 103 # ASSIGN : s_3_2 283 # ASSIGN : s_3_3 632 # ASSIGN : s_3_4 4 # ASSIGN : s_3_5 965 # ASSIGN : s_4_0 633 # ASSIGN : s_4_1 255 # ASSIGN : s_4_2 41 # ASSIGN : s_4_3 332 # ASSIGN : s_4_4 793 # ASSIGN : s_4_5 1025 # ASSIGN : s_5_0 87 # ASSIGN : s_5_1 677 # ASSIGN : s_5_2 876 # ASSIGN : s_5_3 61 # ASSIGN : s_5_4 1018 # ASSIGN : s_5_5 1028 SHOW_RESULT 1034 END : 1034 (0 seconds) [Sun Jun 18 20:10:40 2006] SHOW_RESULT 1034 CPU : 0.129999999999999 = 0.129999999999999 + 0 + 0 + 0 # BOUND : makespan 1000 1034 MODIFY_CNF 1017 BEGIN : [Sun Jun 18 20:10:40 2006] MODIFY_CNF 1017 END : 17311929 bytes (0 seconds) [Sun Jun 18 20:10:40 2006] MODIFY_CNF 1017 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1017 BEGIN : [Sun Jun 18 20:10:40 2006] CMD : minisat /tmp/csp2sat14214.cnf /tmp/csp2sat14214.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 427347 1205186 | 142449 0 0 nan | 0.000 % | | 105 | 427347 1205186 | 156693 105 1623 15.5 | 59.754 % | ============================================================================== restarts : 2 conflicts : 127 (74 /sec) decisions : 249 (145 /sec) propagations : 765163 (444862 /sec) conflict literals : 1885 (25.99 % deleted) Memory used : 36.02 MB CPU time : 1.72 s SATISFIABLE VERIFY_CNF 1017 END : (2 seconds) [Sun Jun 18 20:10:42 2006] VERIFY_CNF 1017 CPU : 1.85 = 0 + 0 + 1.76 + 0.09 # RESULT : makespan 1017 SATISFIABLE SHOW_RESULT 1017 BEGIN : [Sun Jun 18 20:10:42 2006] # ASSIGN : makespan 1017 # ASSIGN : s_0_0 796 # ASSIGN : s_0_1 0 # ASSIGN : s_0_2 325 # ASSIGN : s_0_3 973 # ASSIGN : s_0_4 648 # ASSIGN : s_0_5 347 # ASSIGN : s_1_0 558 # ASSIGN : s_1_1 659 # ASSIGN : s_1_2 791 # ASSIGN : s_1_3 308 # ASSIGN : s_1_4 644 # ASSIGN : s_1_5 6 # ASSIGN : s_2_0 918 # ASSIGN : s_2_1 485 # ASSIGN : s_2_2 571 # ASSIGN : s_2_3 531 # ASSIGN : s_2_4 49 # ASSIGN : s_2_5 690 # ASSIGN : s_3_0 8 # ASSIGN : s_3_1 333 # ASSIGN : s_3_2 36 # ASSIGN : s_3_3 624 # ASSIGN : s_3_4 525 # ASSIGN : s_3_5 957 # ASSIGN : s_4_0 632 # ASSIGN : s_4_1 563 # ASSIGN : s_4_2 349 # ASSIGN : s_4_3 8 # ASSIGN : s_4_4 792 # ASSIGN : s_4_5 344 # ASSIGN : s_5_0 41 # ASSIGN : s_5_1 818 # ASSIGN : s_5_2 649 # ASSIGN : s_5_3 598 # ASSIGN : s_5_4 31 # ASSIGN : s_5_5 0 SHOW_RESULT 1017 END : 1017 (0 seconds) [Sun Jun 18 20:10:42 2006] SHOW_RESULT 1017 CPU : 0.130000000000003 = 0.130000000000003 + 0 + 0 + 0 # BOUND : makespan 1000 1017 MODIFY_CNF 1008 BEGIN : [Sun Jun 18 20:10:42 2006] MODIFY_CNF 1008 END : 17311929 bytes (0 seconds) [Sun Jun 18 20:10:42 2006] MODIFY_CNF 1008 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1008 BEGIN : [Sun Jun 18 20:10:42 2006] CMD : minisat /tmp/csp2sat14214.cnf /tmp/csp2sat14214.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 424107 1195466 | 141369 0 0 nan | 0.000 % | | 100 | 424107 1195466 | 155505 100 1093 10.9 | 60.182 % | | 250 | 424110 1195466 | 171056 247 2451 9.9 | 60.182 % | ============================================================================== restarts : 3 conflicts : 404 (134 /sec) decisions : 496 (165 /sec) propagations : 2417983 (803317 /sec) conflict literals : 3807 (35.30 % deleted) Memory used : 35.71 MB CPU time : 3.01 s UNSATISFIABLE VERIFY_CNF 1008 END : (3 seconds) [Sun Jun 18 20:10:45 2006] VERIFY_CNF 1008 CPU : 3.15 = 0 + 0 + 3.01 + 0.14 # RESULT : makespan 1008 UNSATISFIABLE # BOUND : makespan 1009 1017 MODIFY_CNF 1013 BEGIN : [Sun Jun 18 20:10:45 2006] MODIFY_CNF 1013 END : 17311929 bytes (0 seconds) [Sun Jun 18 20:10:45 2006] MODIFY_CNF 1013 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1013 BEGIN : [Sun Jun 18 20:10:45 2006] CMD : minisat /tmp/csp2sat14214.cnf /tmp/csp2sat14214.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 425907 1200866 | 141969 0 0 nan | 0.000 % | | 100 | 425907 1200866 | 156165 100 1565 15.7 | 59.944 % | ============================================================================== restarts : 2 conflicts : 176 (92 /sec) decisions : 294 (154 /sec) propagations : 1092133 (571797 /sec) conflict literals : 2311 (28.74 % deleted) Memory used : 36.02 MB CPU time : 1.91 s SATISFIABLE VERIFY_CNF 1013 END : (2 seconds) [Sun Jun 18 20:10:47 2006] VERIFY_CNF 1013 CPU : 2.02 = 0 + 0 + 1.95 + 0.0700000000000001 # RESULT : makespan 1013 SATISFIABLE SHOW_RESULT 1013 BEGIN : [Sun Jun 18 20:10:47 2006] # ASSIGN : makespan 1013 # ASSIGN : s_0_0 173 # ASSIGN : s_0_1 604 # ASSIGN : s_0_2 1 # ASSIGN : s_0_3 929 # ASSIGN : s_0_4 23 # ASSIGN : s_0_5 303 # ASSIGN : s_1_0 939 # ASSIGN : s_1_1 274 # ASSIGN : s_1_2 24 # ASSIGN : s_1_3 406 # ASSIGN : s_1_4 19 # ASSIGN : s_1_5 637 # ASSIGN : s_2_0 295 # ASSIGN : s_2_1 406 # ASSIGN : s_2_2 895 # ASSIGN : s_2_3 973 # ASSIGN : s_2_4 459 # ASSIGN : s_2_5 67 # ASSIGN : s_3_0 394 # ASSIGN : s_3_1 452 # ASSIGN : s_3_2 606 # ASSIGN : s_3_3 61 # ASSIGN : s_3_4 914 # ASSIGN : s_3_5 1 # ASSIGN : s_4_0 7 # ASSIGN : s_4_1 941 # ASSIGN : s_4_2 392 # ASSIGN : s_4_3 629 # ASSIGN : s_4_4 167 # ASSIGN : s_4_5 1010 # ASSIGN : s_5_0 422 # ASSIGN : s_5_1 51 # ASSIGN : s_5_2 250 # ASSIGN : s_5_3 25 # ASSIGN : s_5_4 9 # ASSIGN : s_5_5 1004 SHOW_RESULT 1013 END : 1013 (0 seconds) [Sun Jun 18 20:10:47 2006] SHOW_RESULT 1013 CPU : 0.129999999999995 = 0.129999999999995 + 0 + 0 + 0 # BOUND : makespan 1009 1013 MODIFY_CNF 1011 BEGIN : [Sun Jun 18 20:10:47 2006] MODIFY_CNF 1011 END : 17311929 bytes (0 seconds) [Sun Jun 18 20:10:47 2006] MODIFY_CNF 1011 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1011 BEGIN : [Sun Jun 18 20:10:47 2006] CMD : minisat /tmp/csp2sat14214.cnf /tmp/csp2sat14214.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 425187 1198706 | 141729 0 0 nan | 0.000 % | | 100 | 425187 1198706 | 155901 100 1158 11.6 | 60.039 % | | 251 | 425191 1198706 | 171492 247 2410 9.8 | 60.039 % | ============================================================================== restarts : 3 conflicts : 399 (136 /sec) decisions : 500 (171 /sec) propagations : 2370846 (809162 /sec) conflict literals : 3505 (35.06 % deleted) Memory used : 35.72 MB CPU time : 2.93 s UNSATISFIABLE VERIFY_CNF 1011 END : (3 seconds) [Sun Jun 18 20:10:50 2006] VERIFY_CNF 1011 CPU : 3.01 = 0 + 0 + 2.93 + 0.08 # RESULT : makespan 1011 UNSATISFIABLE # BOUND : makespan 1012 1013 MODIFY_CNF 1012 BEGIN : [Sun Jun 18 20:10:50 2006] MODIFY_CNF 1012 END : 17311929 bytes (0 seconds) [Sun Jun 18 20:10:50 2006] MODIFY_CNF 1012 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1012 BEGIN : [Sun Jun 18 20:10:50 2006] CMD : minisat /tmp/csp2sat14214.cnf /tmp/csp2sat14214.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 425547 1199786 | 141849 0 0 nan | 0.000 % | | 101 | 425547 1199786 | 156033 101 1123 11.1 | 59.992 % | ============================================================================== restarts : 2 conflicts : 156 (89 /sec) decisions : 290 (166 /sec) propagations : 911875 (521071 /sec) conflict literals : 1632 (28.64 % deleted) Memory used : 36.02 MB CPU time : 1.75 s SATISFIABLE VERIFY_CNF 1012 END : (2 seconds) [Sun Jun 18 20:10:52 2006] VERIFY_CNF 1012 CPU : 2 = 0.0100000000000051 + 0 + 1.79 + 0.2 # RESULT : makespan 1012 SATISFIABLE SHOW_RESULT 1012 BEGIN : [Sun Jun 18 20:10:52 2006] # ASSIGN : makespan 1012 # ASSIGN : s_0_0 730 # ASSIGN : s_0_1 98 # ASSIGN : s_0_2 22 # ASSIGN : s_0_3 52 # ASSIGN : s_0_4 864 # ASSIGN : s_0_5 423 # ASSIGN : s_1_0 0 # ASSIGN : s_1_1 635 # ASSIGN : s_1_2 782 # ASSIGN : s_1_3 396 # ASSIGN : s_1_4 1008 # ASSIGN : s_1_5 94 # ASSIGN : s_2_0 625 # ASSIGN : s_2_1 966 # ASSIGN : s_2_2 44 # ASSIGN : s_2_3 4 # ASSIGN : s_2_4 189 # ASSIGN : s_2_5 724 # ASSIGN : s_3_0 591 # ASSIGN : s_3_1 439 # ASSIGN : s_3_2 122 # ASSIGN : s_3_3 619 # ASSIGN : s_3_4 23 # ASSIGN : s_3_5 952 # ASSIGN : s_4_0 852 # ASSIGN : s_4_1 27 # ASSIGN : s_4_2 411 # ASSIGN : s_4_3 96 # ASSIGN : s_4_4 627 # ASSIGN : s_4_5 408 # ASSIGN : s_5_0 74 # ASSIGN : s_5_1 767 # ASSIGN : s_5_2 625 # ASSIGN : s_5_3 986 # ASSIGN : s_5_4 13 # ASSIGN : s_5_5 7 SHOW_RESULT 1012 END : 1012 (0 seconds) [Sun Jun 18 20:10:52 2006] SHOW_RESULT 1012 CPU : 0.129999999999997 = 0.119999999999997 + 0.01 + 0 + 0 # BOUND : makespan 1012 1012 MAIN END : (51 seconds) [Sun Jun 18 20:10:52 2006] MAIN CPU : 50.74 = 32.29 + 0.18 + 17.18 + 1.09