# TIMEOUT 18000 MAIN BEGIN : [Mon Jun 19 01:13:21 2006] READ BEGIN : csp/j7-per0-1.csp [Mon Jun 19 01:13:21 2006] READ END : csp/j7-per0-1.csp (1 seconds) [Mon Jun 19 01:13:22 2006] READ CPU : 0.63 = 0.62 + 0.01 + 0 + 0 # BOUND : makespan 1000 2202 GENERATE_CNF 2202 BEGIN : [Mon Jun 19 01:13:22 2006] GENERATE_CNF 2202 END : 109837 variables 1380492 clauses 30765086 bytes (52 seconds) [Mon Jun 19 01:14:14 2006] GENERATE_CNF 2202 CPU : 51.92 = 51.72 + 0.2 + 0 + 0 MODIFY_CNF 1601 BEGIN : [Mon Jun 19 01:14:14 2006] MODIFY_CNF 1601 END : 30765092 bytes (0 seconds) [Mon Jun 19 01:14:14 2006] MODIFY_CNF 1601 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1601 BEGIN : [Mon Jun 19 01:14:14 2006] CMD : minisat /tmp/csp2sat18929.cnf /tmp/csp2sat18929.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 1026168 2970096 | 342056 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 7 (4 /sec) decisions : 257 (135 /sec) propagations : 162417 (85035 /sec) conflict literals : 57 (14.93 % deleted) Memory used : 61.82 MB CPU time : 1.91 s SATISFIABLE VERIFY_CNF 1601 END : (2 seconds) [Mon Jun 19 01:14:16 2006] VERIFY_CNF 1601 CPU : 2.1 = 0 + 0 + 1.97 + 0.13 # RESULT : makespan 1601 SATISFIABLE SHOW_RESULT 1601 BEGIN : [Mon Jun 19 01:14:16 2006] # ASSIGN : makespan 1601 # ASSIGN : s_0_0 55 # ASSIGN : s_0_1 1329 # ASSIGN : s_0_2 93 # ASSIGN : s_0_3 202 # ASSIGN : s_0_4 56 # ASSIGN : s_0_5 263 # ASSIGN : s_0_6 601 # ASSIGN : s_1_0 599 # ASSIGN : s_1_1 1394 # ASSIGN : s_1_2 200 # ASSIGN : s_1_3 429 # ASSIGN : s_1_4 100 # ASSIGN : s_1_5 753 # ASSIGN : s_1_6 992 # ASSIGN : s_2_0 64 # ASSIGN : s_2_1 1059 # ASSIGN : s_2_2 371 # ASSIGN : s_2_3 735 # ASSIGN : s_2_4 129 # ASSIGN : s_2_5 782 # ASSIGN : s_2_6 1232 # ASSIGN : s_3_0 389 # ASSIGN : s_3_1 713 # ASSIGN : s_3_2 542 # ASSIGN : s_3_3 860 # ASSIGN : s_3_4 153 # ASSIGN : s_3_5 1225 # ASSIGN : s_3_6 1475 # ASSIGN : s_4_0 145 # ASSIGN : s_4_1 301 # ASSIGN : s_4_2 914 # ASSIGN : s_4_3 954 # ASSIGN : s_4_4 430 # ASSIGN : s_4_5 1360 # ASSIGN : s_4_6 1539 # ASSIGN : s_5_0 305 # ASSIGN : s_5_1 434 # ASSIGN : s_5_2 1095 # ASSIGN : s_5_3 1156 # ASSIGN : s_5_4 678 # ASSIGN : s_5_5 1550 # ASSIGN : s_5_6 1585 # ASSIGN : s_6_0 855 # ASSIGN : s_6_1 459 # ASSIGN : s_6_2 1242 # ASSIGN : s_6_3 1530 # ASSIGN : s_6_4 1521 # ASSIGN : s_6_5 1582 # ASSIGN : s_6_6 1592 SHOW_RESULT 1601 END : 1601 (0 seconds) [Mon Jun 19 01:14:16 2006] SHOW_RESULT 1601 CPU : 0.19 = 0.18 + 0.00999999999999998 + 0 + 0 # BOUND : makespan 1000 1601 MODIFY_CNF 1300 BEGIN : [Mon Jun 19 01:14:16 2006] MODIFY_CNF 1300 END : 30765092 bytes (0 seconds) [Mon Jun 19 01:14:16 2006] MODIFY_CNF 1300 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1300 BEGIN : [Mon Jun 19 01:14:16 2006] CMD : minisat /tmp/csp2sat18929.cnf /tmp/csp2sat18929.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 849180 2439132 | 283060 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 3 (2 /sec) decisions : 227 (121 /sec) propagations : 158991 (85022 /sec) conflict literals : 13 (0.00 % deleted) Memory used : 61.82 MB CPU time : 1.87 s SATISFIABLE VERIFY_CNF 1300 END : (2 seconds) [Mon Jun 19 01:14:18 2006] VERIFY_CNF 1300 CPU : 2.11 = 0 + 0 + 1.93 + 0.18 # RESULT : makespan 1300 SATISFIABLE SHOW_RESULT 1300 BEGIN : [Mon Jun 19 01:14:18 2006] # ASSIGN : makespan 1300 # ASSIGN : s_0_0 125 # ASSIGN : s_0_1 1021 # ASSIGN : s_0_2 1193 # ASSIGN : s_0_3 37 # ASSIGN : s_0_4 0 # ASSIGN : s_0_5 527 # ASSIGN : s_0_6 126 # ASSIGN : s_1_0 915 # ASSIGN : s_1_1 310 # ASSIGN : s_1_2 139 # ASSIGN : s_1_3 1069 # ASSIGN : s_1_4 45 # ASSIGN : s_1_5 110 # ASSIGN : s_1_6 517 # ASSIGN : s_2_0 9 # ASSIGN : s_2_1 1086 # ASSIGN : s_2_2 422 # ASSIGN : s_2_3 98 # ASSIGN : s_2_4 74 # ASSIGN : s_2_5 145 # ASSIGN : s_2_6 757 # ASSIGN : s_3_0 365 # ASSIGN : s_3_1 547 # ASSIGN : s_3_2 694 # ASSIGN : s_3_3 271 # ASSIGN : s_3_4 1064 # ASSIGN : s_3_5 865 # ASSIGN : s_3_6 1000 # ASSIGN : s_4_0 209 # ASSIGN : s_4_1 889 # ASSIGN : s_4_2 593 # ASSIGN : s_4_3 391 # ASSIGN : s_4_4 641 # ASSIGN : s_4_5 1018 # ASSIGN : s_4_6 1238 # ASSIGN : s_5_0 1113 # ASSIGN : s_5_1 1259 # ASSIGN : s_5_2 633 # ASSIGN : s_5_3 695 # ASSIGN : s_5_4 216 # ASSIGN : s_5_5 1197 # ASSIGN : s_5_6 1284 # ASSIGN : s_6_0 518 # ASSIGN : s_6_1 56 # ASSIGN : s_6_2 914 # ASSIGN : s_6_3 1239 # ASSIGN : s_6_4 905 # ASSIGN : s_6_5 1229 # ASSIGN : s_6_6 1291 SHOW_RESULT 1300 END : 1300 (0 seconds) [Mon Jun 19 01:14:18 2006] SHOW_RESULT 1300 CPU : 0.200000000000003 = 0.200000000000003 + 0 + 0 + 0 # BOUND : makespan 1000 1300 MODIFY_CNF 1150 BEGIN : [Mon Jun 19 01:14:18 2006] MODIFY_CNF 1150 END : 30765092 bytes (0 seconds) [Mon Jun 19 01:14:18 2006] MODIFY_CNF 1150 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1150 BEGIN : [Mon Jun 19 01:14:18 2006] CMD : minisat /tmp/csp2sat18929.cnf /tmp/csp2sat18929.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 760980 2174532 | 253660 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 12 (6 /sec) decisions : 121 (58 /sec) propagations : 162257 (78008 /sec) conflict literals : 351 (5.90 % deleted) Memory used : 61.82 MB CPU time : 2.08 s SATISFIABLE VERIFY_CNF 1150 END : (3 seconds) [Mon Jun 19 01:14:21 2006] VERIFY_CNF 1150 CPU : 2.33 = 0 + 0 + 2.13 + 0.2 # RESULT : makespan 1150 SATISFIABLE SHOW_RESULT 1150 BEGIN : [Mon Jun 19 01:14:21 2006] # ASSIGN : makespan 1150 # ASSIGN : s_0_0 996 # ASSIGN : s_0_1 912 # ASSIGN : s_0_2 1043 # ASSIGN : s_0_3 851 # ASSIGN : s_0_4 4 # ASSIGN : s_0_5 436 # ASSIGN : s_0_6 45 # ASSIGN : s_1_0 70 # ASSIGN : s_1_1 705 # ASSIGN : s_1_2 251 # ASSIGN : s_1_3 980 # ASSIGN : s_1_4 41 # ASSIGN : s_1_5 12 # ASSIGN : s_1_6 447 # ASSIGN : s_2_0 5 # ASSIGN : s_2_1 977 # ASSIGN : s_2_2 422 # ASSIGN : s_2_3 930 # ASSIGN : s_2_4 121 # ASSIGN : s_2_5 145 # ASSIGN : s_2_6 687 # ASSIGN : s_3_0 997 # ASSIGN : s_3_1 446 # ASSIGN : s_3_2 593 # ASSIGN : s_3_3 9 # ASSIGN : s_3_4 198 # ASSIGN : s_3_5 774 # ASSIGN : s_3_6 933 # ASSIGN : s_4_0 753 # ASSIGN : s_4_1 305 # ASSIGN : s_4_2 63 # ASSIGN : s_4_3 103 # ASSIGN : s_4_4 434 # ASSIGN : s_4_5 909 # ASSIGN : s_4_6 1088 # ASSIGN : s_5_0 224 # ASSIGN : s_5_1 26 # ASSIGN : s_5_2 163 # ASSIGN : s_5_3 308 # ASSIGN : s_5_4 682 # ASSIGN : s_5_5 1099 # ASSIGN : s_5_6 1134 # ASSIGN : s_6_0 325 # ASSIGN : s_6_1 51 # ASSIGN : s_6_2 764 # ASSIGN : s_6_3 712 # ASSIGN : s_6_4 1122 # ASSIGN : s_6_5 1131 # ASSIGN : s_6_6 1141 SHOW_RESULT 1150 END : 1150 (0 seconds) [Mon Jun 19 01:14:21 2006] SHOW_RESULT 1150 CPU : 0.2 = 0.18 + 0.02 + 0 + 0 # BOUND : makespan 1000 1150 MODIFY_CNF 1075 BEGIN : [Mon Jun 19 01:14:21 2006] MODIFY_CNF 1075 END : 30765091 bytes (0 seconds) [Mon Jun 19 01:14:21 2006] MODIFY_CNF 1075 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1075 BEGIN : [Mon Jun 19 01:14:21 2006] CMD : minisat /tmp/csp2sat18929.cnf /tmp/csp2sat18929.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 716880 2042232 | 238960 0 0 nan | 0.000 % | | 100 | 716880 2042232 | 262856 100 3113 31.1 | 57.812 % | ============================================================================== restarts : 2 conflicts : 117 (39 /sec) decisions : 273 (91 /sec) propagations : 902305 (301774 /sec) conflict literals : 3461 (19.00 % deleted) Memory used : 61.84 MB CPU time : 2.99 s SATISFIABLE VERIFY_CNF 1075 END : (3 seconds) [Mon Jun 19 01:14:24 2006] VERIFY_CNF 1075 CPU : 3.25 = 0 + 0.01 + 3.06 + 0.18 # RESULT : makespan 1075 SATISFIABLE SHOW_RESULT 1075 BEGIN : [Mon Jun 19 01:14:24 2006] # ASSIGN : makespan 1075 # ASSIGN : s_0_0 522 # ASSIGN : s_0_1 672 # ASSIGN : s_0_2 11 # ASSIGN : s_0_3 604 # ASSIGN : s_0_4 567 # ASSIGN : s_0_5 737 # ASSIGN : s_0_6 131 # ASSIGN : s_1_0 25 # ASSIGN : s_1_1 190 # ASSIGN : s_1_2 397 # ASSIGN : s_1_3 665 # ASSIGN : s_1_4 604 # ASSIGN : s_1_5 568 # ASSIGN : s_1_6 835 # ASSIGN : s_2_0 179 # ASSIGN : s_2_1 6 # ASSIGN : s_2_2 904 # ASSIGN : s_2_3 545 # ASSIGN : s_2_4 521 # ASSIGN : s_2_5 244 # ASSIGN : s_2_6 592 # ASSIGN : s_3_0 281 # ASSIGN : s_3_1 903 # ASSIGN : s_3_2 732 # ASSIGN : s_3_3 434 # ASSIGN : s_3_4 37 # ASSIGN : s_3_5 597 # ASSIGN : s_3_6 528 # ASSIGN : s_4_0 523 # ASSIGN : s_4_1 744 # ASSIGN : s_4_2 692 # ASSIGN : s_4_3 873 # ASSIGN : s_4_4 273 # ASSIGN : s_4_5 65 # ASSIGN : s_4_6 19 # ASSIGN : s_5_0 438 # ASSIGN : s_5_1 1050 # ASSIGN : s_5_2 572 # ASSIGN : s_5_3 60 # ASSIGN : s_5_4 633 # ASSIGN : s_5_5 23 # ASSIGN : s_5_6 12 # ASSIGN : s_6_0 679 # ASSIGN : s_6_1 418 # ASSIGN : s_6_2 118 # ASSIGN : s_6_3 3 # ASSIGN : s_6_4 1066 # ASSIGN : s_6_5 55 # ASSIGN : s_6_6 109 SHOW_RESULT 1075 END : 1075 (0 seconds) [Mon Jun 19 01:14:24 2006] SHOW_RESULT 1075 CPU : 0.190000000000002 = 0.170000000000002 + 0.02 + 0 + 0 # BOUND : makespan 1000 1075 MODIFY_CNF 1037 BEGIN : [Mon Jun 19 01:14:24 2006] MODIFY_CNF 1037 END : 30765091 bytes (0 seconds) [Mon Jun 19 01:14:24 2006] MODIFY_CNF 1037 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1037 BEGIN : [Mon Jun 19 01:14:24 2006] CMD : minisat /tmp/csp2sat18929.cnf /tmp/csp2sat18929.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 694536 1975200 | 231512 0 0 nan | 0.000 % | | 100 | 694536 1975200 | 254663 100 2993 29.9 | 59.542 % | | 251 | 694536 1975200 | 280129 251 5241 20.9 | 59.542 % | | 477 | 694537 1975200 | 308142 476 8500 17.9 | 59.542 % | | 814 | 694537 1975200 | 338956 813 12846 15.8 | 59.542 % | | 1321 | 694537 1975200 | 372852 1320 19191 14.5 | 59.542 % | | 2082 | 694538 1975200 | 410137 2080 30091 14.5 | 59.542 % | | 3221 | 694539 1975200 | 451151 3218 44634 13.9 | 59.542 % | | 4929 | 666991 1892751 | 496266 2197 25855 11.8 | 61.869 % | ============================================================================== restarts : 9 conflicts : 5142 (134 /sec) decisions : 6063 (158 /sec) propagations : 37325357 (974298 /sec) conflict literals : 68550 (36.64 % deleted) Memory used : 61.39 MB CPU time : 38.31 s UNSATISFIABLE VERIFY_CNF 1037 END : (39 seconds) [Mon Jun 19 01:15:03 2006] VERIFY_CNF 1037 CPU : 38.45 = 0 + 0 + 38.31 + 0.14 # RESULT : makespan 1037 UNSATISFIABLE # BOUND : makespan 1038 1075 MODIFY_CNF 1056 BEGIN : [Mon Jun 19 01:15:03 2006] MODIFY_CNF 1056 END : 30765091 bytes (0 seconds) [Mon Jun 19 01:15:03 2006] MODIFY_CNF 1056 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1056 BEGIN : [Mon Jun 19 01:15:03 2006] CMD : minisat /tmp/csp2sat18929.cnf /tmp/csp2sat18929.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 705708 2008716 | 235236 0 0 nan | 0.000 % | | 101 | 705708 2008716 | 258759 101 2580 25.5 | 58.677 % | | 251 | 705708 2008716 | 284635 251 4752 18.9 | 58.677 % | | 476 | 705708 2008716 | 313099 476 7470 15.7 | 58.677 % | | 815 | 705708 2008716 | 344409 815 12522 15.4 | 58.677 % | | 1322 | 705709 2008716 | 378849 1321 20170 15.3 | 58.677 % | | 2081 | 705709 2008716 | 416734 2080 31692 15.2 | 58.677 % | ============================================================================== restarts : 7 conflicts : 3023 (134 /sec) decisions : 3890 (172 /sec) propagations : 21657707 (957882 /sec) conflict literals : 46331 (35.16 % deleted) Memory used : 61.84 MB CPU time : 22.61 s SATISFIABLE VERIFY_CNF 1056 END : (23 seconds) [Mon Jun 19 01:15:26 2006] VERIFY_CNF 1056 CPU : 22.86 = 0 + 0 + 22.66 + 0.2 # RESULT : makespan 1056 SATISFIABLE SHOW_RESULT 1056 BEGIN : [Mon Jun 19 01:15:26 2006] # ASSIGN : makespan 1056 # ASSIGN : s_0_0 70 # ASSIGN : s_0_1 5 # ASSIGN : s_0_2 949 # ASSIGN : s_0_3 888 # ASSIGN : s_0_4 489 # ASSIGN : s_0_5 550 # ASSIGN : s_0_6 71 # ASSIGN : s_1_0 614 # ASSIGN : s_1_1 407 # ASSIGN : s_1_2 236 # ASSIGN : s_1_3 37 # ASSIGN : s_1_4 8 # ASSIGN : s_1_5 207 # ASSIGN : s_1_6 770 # ASSIGN : s_2_0 5 # ASSIGN : s_2_1 77 # ASSIGN : s_2_2 778 # ASSIGN : s_2_3 957 # ASSIGN : s_2_4 1032 # ASSIGN : s_2_5 250 # ASSIGN : s_2_6 527 # ASSIGN : s_3_0 768 # ASSIGN : s_3_1 260 # ASSIGN : s_3_2 65 # ASSIGN : s_3_3 420 # ASSIGN : s_3_4 526 # ASSIGN : s_3_5 921 # ASSIGN : s_3_6 0 # ASSIGN : s_4_0 458 # ASSIGN : s_4_1 621 # ASSIGN : s_4_2 418 # ASSIGN : s_4_3 216 # ASSIGN : s_4_4 762 # ASSIGN : s_4_5 28 # ASSIGN : s_4_6 1010 # ASSIGN : s_5_0 947 # ASSIGN : s_5_1 1031 # ASSIGN : s_5_2 3 # ASSIGN : s_5_3 514 # ASSIGN : s_5_4 72 # ASSIGN : s_5_5 889 # ASSIGN : s_5_6 64 # ASSIGN : s_6_0 71 # ASSIGN : s_6_1 750 # ASSIGN : s_6_2 471 # ASSIGN : s_6_3 1004 # ASSIGN : s_6_4 62 # ASSIGN : s_6_5 18 # ASSIGN : s_6_6 462 SHOW_RESULT 1056 END : 1056 (0 seconds) [Mon Jun 19 01:15:26 2006] SHOW_RESULT 1056 CPU : 0.19 = 0.18 + 0.01 + 0 + 0 # BOUND : makespan 1038 1056 MODIFY_CNF 1047 BEGIN : [Mon Jun 19 01:15:26 2006] MODIFY_CNF 1047 END : 30765091 bytes (0 seconds) [Mon Jun 19 01:15:26 2006] MODIFY_CNF 1047 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1047 BEGIN : [Mon Jun 19 01:15:26 2006] CMD : minisat /tmp/csp2sat18929.cnf /tmp/csp2sat18929.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 700416 1992840 | 233472 0 0 nan | 0.000 % | | 100 | 700416 1992840 | 256819 100 3248 32.5 | 59.087 % | | 250 | 700416 1992840 | 282501 250 5839 23.4 | 59.087 % | | 475 | 700416 1992840 | 310751 475 8895 18.7 | 59.087 % | | 812 | 700416 1992840 | 341826 812 13760 16.9 | 59.087 % | | 1319 | 700416 1992840 | 376008 1319 21337 16.2 | 59.087 % | | 2079 | 700416 1992840 | 413609 2079 31692 15.2 | 59.087 % | | 3218 | 700416 1992840 | 454970 3218 50570 15.7 | 59.087 % | | 4928 | 700417 1992840 | 500467 4927 74739 15.2 | 59.087 % | | 7491 | 690423 1962912 | 550514 5072 72411 14.3 | 59.947 % | ============================================================================== restarts : 10 conflicts : 8551 (129 /sec) decisions : 10164 (154 /sec) propagations : 65225866 (986776 /sec) conflict literals : 124689 (38.64 % deleted) Memory used : 61.39 MB CPU time : 66.1 s UNSATISFIABLE VERIFY_CNF 1047 END : (66 seconds) [Mon Jun 19 01:16:32 2006] VERIFY_CNF 1047 CPU : 66.28 = 0 + 0 + 66.1 + 0.18 # RESULT : makespan 1047 UNSATISFIABLE # BOUND : makespan 1048 1056 MODIFY_CNF 1052 BEGIN : [Mon Jun 19 01:16:32 2006] MODIFY_CNF 1052 END : 30765091 bytes (0 seconds) [Mon Jun 19 01:16:32 2006] MODIFY_CNF 1052 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1052 BEGIN : [Mon Jun 19 01:16:32 2006] CMD : minisat /tmp/csp2sat18929.cnf /tmp/csp2sat18929.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 703356 2001660 | 234452 0 0 nan | 0.000 % | | 100 | 703356 2001660 | 257897 100 2520 25.2 | 58.859 % | | 252 | 703356 2001660 | 283686 252 4461 17.7 | 58.859 % | | 477 | 703356 2001660 | 312055 477 7520 15.8 | 58.859 % | | 815 | 703357 2001660 | 343261 814 12251 15.1 | 58.859 % | | 1321 | 703357 2001660 | 377587 1320 20000 15.2 | 58.859 % | | 2082 | 703357 2001660 | 415346 2081 31486 15.1 | 58.859 % | | 3222 | 703357 2001660 | 456880 3221 48700 15.1 | 58.859 % | | 4931 | 703357 2001660 | 502568 4930 77841 15.8 | 58.859 % | | 7495 | 703360 2001660 | 552825 7491 116311 15.5 | 58.859 % | ============================================================================== restarts : 10 conflicts : 11042 (128 /sec) decisions : 13036 (151 /sec) propagations : 84266795 (974408 /sec) conflict literals : 167717 (39.03 % deleted) Memory used : 61.40 MB CPU time : 86.48 s UNSATISFIABLE VERIFY_CNF 1052 END : (87 seconds) [Mon Jun 19 01:17:59 2006] VERIFY_CNF 1052 CPU : 86.67 = 0 + 0 + 86.48 + 0.19 # RESULT : makespan 1052 UNSATISFIABLE # BOUND : makespan 1053 1056 MODIFY_CNF 1054 BEGIN : [Mon Jun 19 01:17:59 2006] MODIFY_CNF 1054 END : 30765091 bytes (0 seconds) [Mon Jun 19 01:17:59 2006] MODIFY_CNF 1054 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1054 BEGIN : [Mon Jun 19 01:17:59 2006] CMD : minisat /tmp/csp2sat18929.cnf /tmp/csp2sat18929.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 704532 2005188 | 234844 0 0 nan | 0.000 % | | 100 | 704532 2005188 | 258328 100 2992 29.9 | 58.768 % | | 250 | 704532 2005188 | 284161 250 5332 21.3 | 58.768 % | | 475 | 704532 2005188 | 312577 475 10255 21.6 | 58.768 % | | 812 | 704532 2005188 | 343835 812 15150 18.7 | 58.768 % | | 1318 | 704532 2005188 | 378218 1318 21768 16.5 | 58.768 % | | 2077 | 704532 2005188 | 416040 2077 34780 16.7 | 58.768 % | | 3217 | 704532 2005188 | 457644 3217 52476 16.3 | 58.768 % | | 4926 | 704532 2005188 | 503408 4926 80339 16.3 | 58.768 % | | 7489 | 704532 2005188 | 553749 7489 119030 15.9 | 58.768 % | | 11335 | 701449 1995957 | 609124 10427 165303 15.9 | 59.043 % | ============================================================================== restarts : 11 conflicts : 12972 (124 /sec) decisions : 15083 (145 /sec) propagations : 100914236 (967167 /sec) conflict literals : 200489 (39.92 % deleted) Memory used : 61.40 MB CPU time : 104.34 s UNSATISFIABLE VERIFY_CNF 1054 END : (104 seconds) [Mon Jun 19 01:19:43 2006] VERIFY_CNF 1054 CPU : 104.47 = 0 + 0 + 104.34 + 0.13 # RESULT : makespan 1054 UNSATISFIABLE # BOUND : makespan 1055 1056 MODIFY_CNF 1055 BEGIN : [Mon Jun 19 01:19:43 2006] MODIFY_CNF 1055 END : 30765091 bytes (0 seconds) [Mon Jun 19 01:19:43 2006] MODIFY_CNF 1055 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1055 BEGIN : [Mon Jun 19 01:19:43 2006] CMD : minisat /tmp/csp2sat18929.cnf /tmp/csp2sat18929.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 705120 2006952 | 235040 0 0 nan | 0.000 % | | 103 | 705120 2006952 | 258544 103 2620 25.4 | 58.722 % | | 253 | 705120 2006952 | 284398 253 4567 18.1 | 58.722 % | | 478 | 705120 2006952 | 312838 478 8095 16.9 | 58.722 % | | 815 | 705120 2006952 | 344122 815 13388 16.4 | 58.722 % | | 1322 | 705120 2006952 | 378534 1322 20190 15.3 | 58.722 % | | 2082 | 705121 2006952 | 416387 2081 32121 15.4 | 58.722 % | | 3221 | 705121 2006952 | 458026 3220 49349 15.3 | 58.722 % | | 4929 | 705121 2006952 | 503829 4928 77884 15.8 | 58.722 % | ============================================================================== restarts : 9 conflicts : 6021 (132 /sec) decisions : 7414 (163 /sec) propagations : 44818953 (982656 /sec) conflict literals : 94410 (37.32 % deleted) Memory used : 61.84 MB CPU time : 45.61 s SATISFIABLE VERIFY_CNF 1055 END : (46 seconds) [Mon Jun 19 01:20:29 2006] VERIFY_CNF 1055 CPU : 45.86 = 0 + 0 + 45.67 + 0.19 # RESULT : makespan 1055 SATISFIABLE SHOW_RESULT 1055 BEGIN : [Mon Jun 19 01:20:29 2006] # ASSIGN : makespan 1055 # ASSIGN : s_0_0 69 # ASSIGN : s_0_1 4 # ASSIGN : s_0_2 948 # ASSIGN : s_0_3 887 # ASSIGN : s_0_4 481 # ASSIGN : s_0_5 549 # ASSIGN : s_0_6 70 # ASSIGN : s_1_0 613 # ASSIGN : s_1_1 406 # ASSIGN : s_1_2 235 # ASSIGN : s_1_3 36 # ASSIGN : s_1_4 1026 # ASSIGN : s_1_5 206 # ASSIGN : s_1_6 769 # ASSIGN : s_2_0 4 # ASSIGN : s_2_1 76 # ASSIGN : s_2_2 777 # ASSIGN : s_2_3 955 # ASSIGN : s_2_4 1002 # ASSIGN : s_2_5 249 # ASSIGN : s_2_6 526 # ASSIGN : s_3_0 767 # ASSIGN : s_3_1 259 # ASSIGN : s_3_2 64 # ASSIGN : s_3_3 419 # ASSIGN : s_3_4 518 # ASSIGN : s_3_5 920 # ASSIGN : s_3_6 0 # ASSIGN : s_4_0 457 # ASSIGN : s_4_1 620 # ASSIGN : s_4_2 417 # ASSIGN : s_4_3 215 # ASSIGN : s_4_4 754 # ASSIGN : s_4_5 27 # ASSIGN : s_4_6 1009 # ASSIGN : s_5_0 946 # ASSIGN : s_5_1 1030 # ASSIGN : s_5_2 3 # ASSIGN : s_5_3 513 # ASSIGN : s_5_4 64 # ASSIGN : s_5_5 888 # ASSIGN : s_5_6 506 # ASSIGN : s_6_0 70 # ASSIGN : s_6_1 749 # ASSIGN : s_6_2 470 # ASSIGN : s_6_3 1003 # ASSIGN : s_6_4 55 # ASSIGN : s_6_5 17 # ASSIGN : s_6_6 461 SHOW_RESULT 1055 END : 1055 (0 seconds) [Mon Jun 19 01:20:29 2006] SHOW_RESULT 1055 CPU : 0.199999999999996 = 0.199999999999996 + 0 + 0 + 0 # BOUND : makespan 1055 1055 MAIN END : (428 seconds) [Mon Jun 19 01:20:29 2006] MAIN CPU : 428.11 = 53.45 + 0.29 + 372.65 + 1.72