# TIMEOUT 18000 MAIN BEGIN : [Sun Jun 18 20:12:39 2006] READ BEGIN : csp/j6-per20-2.csp [Sun Jun 18 20:12:39 2006] READ END : csp/j6-per20-2.csp (0 seconds) [Sun Jun 18 20:12:39 2006] READ CPU : 0.4 = 0.4 + 0 + 0 + 0 # BOUND : makespan 1000 1803 GENERATE_CNF 1803 BEGIN : [Sun Jun 18 20:12:39 2006] GENERATE_CNF 1803 END : 66181 variables 692002 clauses 14502996 bytes (26 seconds) [Sun Jun 18 20:13:05 2006] GENERATE_CNF 1803 CPU : 25.27 = 25.13 + 0.14 + 0 + 0 MODIFY_CNF 1401 BEGIN : [Sun Jun 18 20:13:05 2006] MODIFY_CNF 1401 END : 14503002 bytes (0 seconds) [Sun Jun 18 20:13:05 2006] MODIFY_CNF 1401 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1401 BEGIN : [Sun Jun 18 20:13:05 2006] CMD : minisat /tmp/csp2sat14288.cnf /tmp/csp2sat14288.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 546665 1574758 | 182221 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 5 (6 /sec) decisions : 158 (178 /sec) propagations : 105454 (118488 /sec) conflict literals : 52 (3.70 % deleted) Memory used : 30.67 MB CPU time : 0.89 s SATISFIABLE VERIFY_CNF 1401 END : (1 seconds) [Sun Jun 18 20:13:06 2006] VERIFY_CNF 1401 CPU : 0.99 = 0 + 0 + 0.92 + 0.07 # RESULT : makespan 1401 SATISFIABLE SHOW_RESULT 1401 BEGIN : [Sun Jun 18 20:13:06 2006] # ASSIGN : makespan 1401 # ASSIGN : s_0_0 707 # ASSIGN : s_0_1 5 # ASSIGN : s_0_2 1174 # ASSIGN : s_0_3 76 # ASSIGN : s_0_4 55 # ASSIGN : s_0_5 468 # ASSIGN : s_1_0 1177 # ASSIGN : s_1_1 994 # ASSIGN : s_1_2 224 # ASSIGN : s_1_3 453 # ASSIGN : s_1_4 118 # ASSIGN : s_1_5 733 # ASSIGN : s_2_0 1341 # ASSIGN : s_2_1 947 # ASSIGN : s_2_2 131 # ASSIGN : s_2_3 630 # ASSIGN : s_2_4 221 # ASSIGN : s_2_5 871 # ASSIGN : s_3_0 463 # ASSIGN : s_3_1 729 # ASSIGN : s_3_2 646 # ASSIGN : s_3_3 919 # ASSIGN : s_3_4 1075 # ASSIGN : s_3_5 936 # ASSIGN : s_4_0 340 # ASSIGN : s_4_1 587 # ASSIGN : s_4_2 831 # ASSIGN : s_4_3 1022 # ASSIGN : s_4_4 1343 # ASSIGN : s_4_5 1134 # ASSIGN : s_5_0 773 # ASSIGN : s_5_1 327 # ASSIGN : s_5_2 133 # ASSIGN : s_5_3 1373 # ASSIGN : s_5_4 1366 # ASSIGN : s_5_5 1356 SHOW_RESULT 1401 END : 1401 (0 seconds) [Sun Jun 18 20:13:06 2006] SHOW_RESULT 1401 CPU : 0.119999999999999 = 0.109999999999999 + 0.00999999999999998 + 0 + 0 # BOUND : makespan 1000 1401 MODIFY_CNF 1200 BEGIN : [Sun Jun 18 20:13:06 2006] MODIFY_CNF 1200 END : 14503002 bytes (0 seconds) [Sun Jun 18 20:13:06 2006] MODIFY_CNF 1200 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1200 BEGIN : [Sun Jun 18 20:13:06 2006] CMD : minisat /tmp/csp2sat14288.cnf /tmp/csp2sat14288.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 474305 1357678 | 158101 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 3 (4 /sec) decisions : 85 (100 /sec) propagations : 80521 (94731 /sec) conflict literals : 29 (3.33 % deleted) Memory used : 30.70 MB CPU time : 0.85 s SATISFIABLE VERIFY_CNF 1200 END : (1 seconds) [Sun Jun 18 20:13:07 2006] VERIFY_CNF 1200 CPU : 0.99 = 0 + 0 + 0.87 + 0.12 # RESULT : makespan 1200 SATISFIABLE SHOW_RESULT 1200 BEGIN : [Sun Jun 18 20:13:07 2006] # ASSIGN : makespan 1200 # ASSIGN : s_0_0 373 # ASSIGN : s_0_1 302 # ASSIGN : s_0_2 439 # ASSIGN : s_0_3 666 # ASSIGN : s_0_4 352 # ASSIGN : s_0_5 3 # ASSIGN : s_1_0 1036 # ASSIGN : s_1_1 519 # ASSIGN : s_1_2 807 # ASSIGN : s_1_3 0 # ASSIGN : s_1_4 380 # ASSIGN : s_1_5 242 # ASSIGN : s_2_0 7 # ASSIGN : s_2_1 1153 # ASSIGN : s_2_2 5 # ASSIGN : s_2_3 177 # ASSIGN : s_2_4 483 # ASSIGN : s_2_5 418 # ASSIGN : s_3_0 67 # ASSIGN : s_3_1 702 # ASSIGN : s_3_2 265 # ASSIGN : s_3_3 546 # ASSIGN : s_3_4 892 # ASSIGN : s_3_5 563 # ASSIGN : s_4_0 250 # ASSIGN : s_4_1 377 # ASSIGN : s_4_2 59 # ASSIGN : s_4_3 1043 # ASSIGN : s_4_4 1160 # ASSIGN : s_4_5 834 # ASSIGN : s_5_0 489 # ASSIGN : s_5_1 893 # ASSIGN : s_5_2 348 # ASSIGN : s_5_3 1155 # ASSIGN : s_5_4 1183 # ASSIGN : s_5_5 1190 SHOW_RESULT 1200 END : 1200 (0 seconds) [Sun Jun 18 20:13:07 2006] SHOW_RESULT 1200 CPU : 0.109999999999999 = 0.109999999999999 + 0 + 0 + 0 # BOUND : makespan 1000 1200 MODIFY_CNF 1100 BEGIN : [Sun Jun 18 20:13:07 2006] MODIFY_CNF 1100 END : 14503002 bytes (0 seconds) [Sun Jun 18 20:13:07 2006] MODIFY_CNF 1100 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1100 BEGIN : [Sun Jun 18 20:13:07 2006] CMD : minisat /tmp/csp2sat14288.cnf /tmp/csp2sat14288.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 438305 1249678 | 146101 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 1 (1 /sec) decisions : 78 (92 /sec) propagations : 70299 (82705 /sec) conflict literals : 3 (0.00 % deleted) Memory used : 30.70 MB CPU time : 0.85 s SATISFIABLE VERIFY_CNF 1100 END : (1 seconds) [Sun Jun 18 20:13:08 2006] VERIFY_CNF 1100 CPU : 1 = 0 + 0 + 0.89 + 0.11 # RESULT : makespan 1100 SATISFIABLE SHOW_RESULT 1100 BEGIN : [Sun Jun 18 20:13:08 2006] # ASSIGN : makespan 1100 # ASSIGN : s_0_0 974 # ASSIGN : s_0_1 697 # ASSIGN : s_0_2 747 # ASSIGN : s_0_3 320 # ASSIGN : s_0_4 2 # ASSIGN : s_0_5 81 # ASSIGN : s_1_0 753 # ASSIGN : s_1_1 917 # ASSIGN : s_1_2 518 # ASSIGN : s_1_3 126 # ASSIGN : s_1_4 23 # ASSIGN : s_1_5 380 # ASSIGN : s_2_0 1040 # ASSIGN : s_2_1 58 # ASSIGN : s_2_2 19 # ASSIGN : s_2_3 712 # ASSIGN : s_2_4 131 # ASSIGN : s_2_5 540 # ASSIGN : s_3_0 422 # ASSIGN : s_3_1 105 # ASSIGN : s_3_2 21 # ASSIGN : s_3_3 303 # ASSIGN : s_3_4 802 # ASSIGN : s_3_5 605 # ASSIGN : s_4_0 621 # ASSIGN : s_4_1 295 # ASSIGN : s_4_2 104 # ASSIGN : s_4_3 953 # ASSIGN : s_4_4 1070 # ASSIGN : s_4_5 744 # ASSIGN : s_5_0 18 # ASSIGN : s_5_1 437 # ASSIGN : s_5_2 974 # ASSIGN : s_5_3 1065 # ASSIGN : s_5_4 1093 # ASSIGN : s_5_5 964 SHOW_RESULT 1100 END : 1100 (0 seconds) [Sun Jun 18 20:13:08 2006] SHOW_RESULT 1100 CPU : 0.100000000000001 = 0.100000000000001 + 0 + 0 + 0 # BOUND : makespan 1000 1100 MODIFY_CNF 1050 BEGIN : [Sun Jun 18 20:13:08 2006] MODIFY_CNF 1050 END : 14503001 bytes (0 seconds) [Sun Jun 18 20:13:08 2006] MODIFY_CNF 1050 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1050 BEGIN : [Sun Jun 18 20:13:08 2006] CMD : minisat /tmp/csp2sat14288.cnf /tmp/csp2sat14288.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 420305 1195678 | 140101 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 5 (6 /sec) decisions : 72 (81 /sec) propagations : 83703 (94048 /sec) conflict literals : 59 (7.81 % deleted) Memory used : 30.70 MB CPU time : 0.89 s SATISFIABLE VERIFY_CNF 1050 END : (1 seconds) [Sun Jun 18 20:13:09 2006] VERIFY_CNF 1050 CPU : 1.02 = 0 + 0 + 0.93 + 0.09 # RESULT : makespan 1050 SATISFIABLE SHOW_RESULT 1050 BEGIN : [Sun Jun 18 20:13:09 2006] # ASSIGN : makespan 1050 # ASSIGN : s_0_0 293 # ASSIGN : s_0_1 1000 # ASSIGN : s_0_2 773 # ASSIGN : s_0_3 387 # ASSIGN : s_0_4 5 # ASSIGN : s_0_5 54 # ASSIGN : s_1_0 886 # ASSIGN : s_1_1 703 # ASSIGN : s_1_2 474 # ASSIGN : s_1_3 159 # ASSIGN : s_1_4 26 # ASSIGN : s_1_5 336 # ASSIGN : s_2_0 4 # ASSIGN : s_2_1 64 # ASSIGN : s_2_2 762 # ASSIGN : s_2_3 764 # ASSIGN : s_2_4 129 # ASSIGN : s_2_5 538 # ASSIGN : s_3_0 110 # ASSIGN : s_3_1 371 # ASSIGN : s_3_2 27 # ASSIGN : s_3_3 10 # ASSIGN : s_3_4 742 # ASSIGN : s_3_5 603 # ASSIGN : s_4_0 359 # ASSIGN : s_4_1 561 # ASSIGN : s_4_2 168 # ASSIGN : s_4_3 47 # ASSIGN : s_4_4 1010 # ASSIGN : s_4_5 801 # ASSIGN : s_5_0 482 # ASSIGN : s_5_1 111 # ASSIGN : s_5_2 383 # ASSIGN : s_5_3 1005 # ASSIGN : s_5_4 1033 # ASSIGN : s_5_5 1040 SHOW_RESULT 1050 END : 1050 (0 seconds) [Sun Jun 18 20:13:09 2006] SHOW_RESULT 1050 CPU : 0.0999999999999979 = 0.0999999999999979 + 0 + 0 + 0 # BOUND : makespan 1000 1050 MODIFY_CNF 1025 BEGIN : [Sun Jun 18 20:13:09 2006] MODIFY_CNF 1025 END : 14503001 bytes (0 seconds) [Sun Jun 18 20:13:09 2006] MODIFY_CNF 1025 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1025 BEGIN : [Sun Jun 18 20:13:09 2006] CMD : minisat /tmp/csp2sat14288.cnf /tmp/csp2sat14288.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 411305 1168678 | 137101 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 33 (34 /sec) decisions : 110 (115 /sec) propagations : 187030 (194823 /sec) conflict literals : 362 (18.83 % deleted) Memory used : 30.70 MB CPU time : 0.96 s SATISFIABLE VERIFY_CNF 1025 END : (2 seconds) [Sun Jun 18 20:13:11 2006] VERIFY_CNF 1025 CPU : 1.1 = 0 + 0 + 0.97 + 0.13 # RESULT : makespan 1025 SATISFIABLE SHOW_RESULT 1025 BEGIN : [Sun Jun 18 20:13:11 2006] # ASSIGN : makespan 1025 # ASSIGN : s_0_0 0 # ASSIGN : s_0_1 954 # ASSIGN : s_0_2 697 # ASSIGN : s_0_3 317 # ASSIGN : s_0_4 1004 # ASSIGN : s_0_5 78 # ASSIGN : s_1_0 678 # ASSIGN : s_1_1 481 # ASSIGN : s_1_2 112 # ASSIGN : s_1_3 848 # ASSIGN : s_1_4 9 # ASSIGN : s_1_5 343 # ASSIGN : s_2_0 470 # ASSIGN : s_2_1 423 # ASSIGN : s_2_2 1023 # ASSIGN : s_2_3 76 # ASSIGN : s_2_4 595 # ASSIGN : s_2_5 530 # ASSIGN : s_3_0 842 # ASSIGN : s_3_1 9 # ASSIGN : s_3_2 584 # ASSIGN : s_3_3 825 # ASSIGN : s_3_4 264 # ASSIGN : s_3_5 667 # ASSIGN : s_4_0 555 # ASSIGN : s_4_1 199 # ASSIGN : s_4_2 341 # ASSIGN : s_4_3 694 # ASSIGN : s_4_4 532 # ASSIGN : s_4_5 806 # ASSIGN : s_5_0 66 # ASSIGN : s_5_1 664 # ASSIGN : s_5_2 924 # ASSIGN : s_5_3 38 # ASSIGN : s_5_4 588 # ASSIGN : s_5_5 1015 SHOW_RESULT 1025 END : 1025 (0 seconds) [Sun Jun 18 20:13:11 2006] SHOW_RESULT 1025 CPU : 0.109999999999999 = 0.109999999999999 + 0 + 0 + 0 # BOUND : makespan 1000 1025 MODIFY_CNF 1012 BEGIN : [Sun Jun 18 20:13:11 2006] MODIFY_CNF 1012 END : 14503001 bytes (0 seconds) [Sun Jun 18 20:13:11 2006] MODIFY_CNF 1012 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1012 BEGIN : [Sun Jun 18 20:13:11 2006] CMD : minisat /tmp/csp2sat14288.cnf /tmp/csp2sat14288.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 406625 1154638 | 135541 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 12 (13 /sec) decisions : 88 (95 /sec) propagations : 114473 (123089 /sec) conflict literals : 79 (13.19 % deleted) Memory used : 30.70 MB CPU time : 0.93 s SATISFIABLE VERIFY_CNF 1012 END : (1 seconds) [Sun Jun 18 20:13:12 2006] VERIFY_CNF 1012 CPU : 1.04 = 0 + 0 + 0.96 + 0.08 # RESULT : makespan 1012 SATISFIABLE SHOW_RESULT 1012 BEGIN : [Sun Jun 18 20:13:12 2006] # ASSIGN : makespan 1012 # ASSIGN : s_0_0 539 # ASSIGN : s_0_1 1 # ASSIGN : s_0_2 291 # ASSIGN : s_0_3 635 # ASSIGN : s_0_4 518 # ASSIGN : s_0_5 51 # ASSIGN : s_1_0 605 # ASSIGN : s_1_1 107 # ASSIGN : s_1_2 783 # ASSIGN : s_1_3 428 # ASSIGN : s_1_4 4 # ASSIGN : s_1_5 290 # ASSIGN : s_2_0 952 # ASSIGN : s_2_1 356 # ASSIGN : s_2_2 541 # ASSIGN : s_2_3 63 # ASSIGN : s_2_4 543 # ASSIGN : s_2_5 476 # ASSIGN : s_3_0 769 # ASSIGN : s_3_1 403 # ASSIGN : s_3_2 17 # ASSIGN : s_3_3 0 # ASSIGN : s_3_4 135 # ASSIGN : s_3_5 624 # ASSIGN : s_4_0 416 # ASSIGN : s_4_1 593 # ASSIGN : s_4_2 100 # ASSIGN : s_4_3 304 # ASSIGN : s_4_4 972 # ASSIGN : s_4_5 763 # ASSIGN : s_5_0 12 # ASSIGN : s_5_1 735 # ASSIGN : s_5_2 644 # ASSIGN : s_5_3 607 # ASSIGN : s_5_4 995 # ASSIGN : s_5_5 1002 SHOW_RESULT 1012 END : 1012 (0 seconds) [Sun Jun 18 20:13:12 2006] SHOW_RESULT 1012 CPU : 0.100000000000001 = 0.100000000000001 + 0 + 0 + 0 # BOUND : makespan 1000 1012 MODIFY_CNF 1006 BEGIN : [Sun Jun 18 20:13:12 2006] MODIFY_CNF 1006 END : 14503000 bytes (0 seconds) [Sun Jun 18 20:13:12 2006] MODIFY_CNF 1006 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1006 BEGIN : [Sun Jun 18 20:13:12 2006] CMD : minisat /tmp/csp2sat14288.cnf /tmp/csp2sat14288.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 404465 1148158 | 134821 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 43 (40 /sec) decisions : 111 (104 /sec) propagations : 268909 (251317 /sec) conflict literals : 557 (28.86 % deleted) Memory used : 30.70 MB CPU time : 1.07 s SATISFIABLE VERIFY_CNF 1006 END : (1 seconds) [Sun Jun 18 20:13:13 2006] VERIFY_CNF 1006 CPU : 1.18 = 0 + 0 + 1.1 + 0.0800000000000001 # RESULT : makespan 1006 SATISFIABLE SHOW_RESULT 1006 BEGIN : [Sun Jun 18 20:13:13 2006] # ASSIGN : makespan 1006 # ASSIGN : s_0_0 940 # ASSIGN : s_0_1 47 # ASSIGN : s_0_2 336 # ASSIGN : s_0_3 563 # ASSIGN : s_0_4 26 # ASSIGN : s_0_5 97 # ASSIGN : s_1_0 185 # ASSIGN : s_1_1 592 # ASSIGN : s_1_2 775 # ASSIGN : s_1_3 5 # ASSIGN : s_1_4 487 # ASSIGN : s_1_5 349 # ASSIGN : s_2_0 125 # ASSIGN : s_2_1 0 # ASSIGN : s_2_2 1004 # ASSIGN : s_2_3 210 # ASSIGN : s_2_4 590 # ASSIGN : s_2_5 525 # ASSIGN : s_3_0 353 # ASSIGN : s_3_1 799 # ASSIGN : s_3_2 2 # ASSIGN : s_3_3 989 # ASSIGN : s_3_4 85 # ASSIGN : s_3_5 641 # ASSIGN : s_4_0 2 # ASSIGN : s_4_1 134 # ASSIGN : s_4_2 584 # ASSIGN : s_4_3 451 # ASSIGN : s_4_4 428 # ASSIGN : s_4_5 780 # ASSIGN : s_5_0 536 # ASSIGN : s_5_1 276 # ASSIGN : s_5_2 91 # ASSIGN : s_5_3 182 # ASSIGN : s_5_4 999 # ASSIGN : s_5_5 989 SHOW_RESULT 1006 END : 1006 (0 seconds) [Sun Jun 18 20:13:13 2006] SHOW_RESULT 1006 CPU : 0.100000000000001 = 0.100000000000001 + 0 + 0 + 0 # BOUND : makespan 1000 1006 MODIFY_CNF 1003 BEGIN : [Sun Jun 18 20:13:13 2006] MODIFY_CNF 1003 END : 14503000 bytes (0 seconds) [Sun Jun 18 20:13:13 2006] MODIFY_CNF 1003 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1003 BEGIN : [Sun Jun 18 20:13:13 2006] CMD : minisat /tmp/csp2sat14288.cnf /tmp/csp2sat14288.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 403385 1144918 | 134461 0 0 nan | 0.000 % | | 100 | 403385 1144918 | 147907 100 1362 13.6 | 52.867 % | ============================================================================== restarts : 2 conflicts : 111 (85 /sec) decisions : 207 (159 /sec) propagations : 635212 (488625 /sec) conflict literals : 1523 (31.18 % deleted) Memory used : 30.72 MB CPU time : 1.3 s SATISFIABLE VERIFY_CNF 1003 END : (2 seconds) [Sun Jun 18 20:13:15 2006] VERIFY_CNF 1003 CPU : 1.45 = 0 + 0 + 1.34 + 0.11 # RESULT : makespan 1003 SATISFIABLE SHOW_RESULT 1003 BEGIN : [Sun Jun 18 20:13:15 2006] # ASSIGN : makespan 1003 # ASSIGN : s_0_0 694 # ASSIGN : s_0_1 644 # ASSIGN : s_0_2 417 # ASSIGN : s_0_3 30 # ASSIGN : s_0_4 8 # ASSIGN : s_0_5 764 # ASSIGN : s_1_0 3 # ASSIGN : s_1_1 402 # ASSIGN : s_1_2 173 # ASSIGN : s_1_3 826 # ASSIGN : s_1_4 723 # ASSIGN : s_1_5 585 # ASSIGN : s_2_0 760 # ASSIGN : s_2_1 956 # ASSIGN : s_2_2 27 # ASSIGN : s_2_3 519 # ASSIGN : s_2_4 29 # ASSIGN : s_2_5 454 # ASSIGN : s_3_0 820 # ASSIGN : s_3_1 70 # ASSIGN : s_3_2 706 # ASSIGN : s_3_3 803 # ASSIGN : s_3_4 438 # ASSIGN : s_3_5 299 # ASSIGN : s_4_0 571 # ASSIGN : s_4_1 260 # ASSIGN : s_4_2 789 # ASSIGN : s_4_3 407 # ASSIGN : s_4_4 980 # ASSIGN : s_4_5 51 # ASSIGN : s_5_0 167 # ASSIGN : s_5_1 696 # ASSIGN : s_5_2 76 # ASSIGN : s_5_3 2 # ASSIGN : s_5_4 973 # ASSIGN : s_5_5 575 SHOW_RESULT 1003 END : 1003 (0 seconds) [Sun Jun 18 20:13:15 2006] SHOW_RESULT 1003 CPU : 0.100000000000001 = 0.100000000000001 + 0 + 0 + 0 # BOUND : makespan 1000 1003 MODIFY_CNF 1001 BEGIN : [Sun Jun 18 20:13:15 2006] MODIFY_CNF 1001 END : 14503000 bytes (0 seconds) [Sun Jun 18 20:13:15 2006] MODIFY_CNF 1001 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1001 BEGIN : [Sun Jun 18 20:13:15 2006] CMD : minisat /tmp/csp2sat14288.cnf /tmp/csp2sat14288.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 402665 1142758 | 134221 0 0 nan | 0.000 % | | 100 | 402665 1142758 | 147643 100 1295 12.9 | 52.979 % | ============================================================================== restarts : 2 conflicts : 146 (104 /sec) decisions : 255 (182 /sec) propagations : 783289 (559492 /sec) conflict literals : 1806 (27.03 % deleted) Memory used : 30.72 MB CPU time : 1.4 s SATISFIABLE VERIFY_CNF 1001 END : (1 seconds) [Sun Jun 18 20:13:16 2006] VERIFY_CNF 1001 CPU : 1.55 = 0 + 0.01 + 1.43 + 0.11 # RESULT : makespan 1001 SATISFIABLE SHOW_RESULT 1001 BEGIN : [Sun Jun 18 20:13:16 2006] # ASSIGN : makespan 1001 # ASSIGN : s_0_0 1 # ASSIGN : s_0_1 333 # ASSIGN : s_0_2 106 # ASSIGN : s_0_3 383 # ASSIGN : s_0_4 85 # ASSIGN : s_0_5 762 # ASSIGN : s_1_0 837 # ASSIGN : s_1_1 654 # ASSIGN : s_1_2 425 # ASSIGN : s_1_3 6 # ASSIGN : s_1_4 183 # ASSIGN : s_1_5 287 # ASSIGN : s_2_0 190 # ASSIGN : s_2_1 26 # ASSIGN : s_2_2 104 # ASSIGN : s_2_3 760 # ASSIGN : s_2_4 286 # ASSIGN : s_2_5 695 # ASSIGN : s_3_0 250 # ASSIGN : s_3_1 464 # ASSIGN : s_3_2 4 # ASSIGN : s_3_3 226 # ASSIGN : s_3_4 733 # ASSIGN : s_3_5 87 # ASSIGN : s_4_0 67 # ASSIGN : s_4_1 859 # ASSIGN : s_4_2 668 # ASSIGN : s_4_3 243 # ASSIGN : s_4_4 44 # ASSIGN : s_4_5 459 # ASSIGN : s_5_0 433 # ASSIGN : s_5_1 73 # ASSIGN : s_5_2 910 # ASSIGN : s_5_3 355 # ASSIGN : s_5_4 37 # ASSIGN : s_5_5 27 SHOW_RESULT 1001 END : 1001 (0 seconds) [Sun Jun 18 20:13:16 2006] SHOW_RESULT 1001 CPU : 0.100000000000001 = 0.100000000000001 + 0 + 0 + 0 # BOUND : makespan 1000 1001 MODIFY_CNF 1000 BEGIN : [Sun Jun 18 20:13:16 2006] MODIFY_CNF 1000 END : 14503000 bytes (0 seconds) [Sun Jun 18 20:13:16 2006] MODIFY_CNF 1000 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1000 BEGIN : [Sun Jun 18 20:13:16 2006] CMD : minisat /tmp/csp2sat14288.cnf /tmp/csp2sat14288.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 402306 1141678 | 134102 0 0 nan | 0.000 % | | 100 | 402306 1141678 | 147512 100 1166 11.7 | 53.035 % | | 250 | 402306 1141678 | 162263 250 2624 10.5 | 53.035 % | ============================================================================== restarts : 3 conflicts : 427 (176 /sec) decisions : 615 (253 /sec) propagations : 2189765 (901138 /sec) conflict literals : 4771 (30.87 % deleted) Memory used : 30.72 MB CPU time : 2.43 s SATISFIABLE VERIFY_CNF 1000 END : (3 seconds) [Sun Jun 18 20:13:19 2006] VERIFY_CNF 1000 CPU : 2.54 = 0 + 0 + 2.47 + 0.07 # RESULT : makespan 1000 SATISFIABLE SHOW_RESULT 1000 BEGIN : [Sun Jun 18 20:13:19 2006] # ASSIGN : makespan 1000 # ASSIGN : s_0_0 527 # ASSIGN : s_0_1 11 # ASSIGN : s_0_2 300 # ASSIGN : s_0_3 595 # ASSIGN : s_0_4 979 # ASSIGN : s_0_5 61 # ASSIGN : s_1_0 593 # ASSIGN : s_1_1 233 # ASSIGN : s_1_2 4 # ASSIGN : s_1_3 416 # ASSIGN : s_1_4 759 # ASSIGN : s_1_5 862 # ASSIGN : s_2_0 940 # ASSIGN : s_2_1 893 # ASSIGN : s_2_2 298 # ASSIGN : s_2_3 51 # ASSIGN : s_2_4 350 # ASSIGN : s_2_5 797 # ASSIGN : s_3_0 757 # ASSIGN : s_3_1 443 # ASSIGN : s_3_2 674 # ASSIGN : s_3_3 19 # ASSIGN : s_3_4 36 # ASSIGN : s_3_5 304 # ASSIGN : s_4_0 404 # ASSIGN : s_4_1 91 # ASSIGN : s_4_2 809 # ASSIGN : s_4_3 292 # ASSIGN : s_4_4 13 # ASSIGN : s_4_5 588 # ASSIGN : s_5_0 0 # ASSIGN : s_5_1 633 # ASSIGN : s_5_2 542 # ASSIGN : s_5_3 972 # ASSIGN : s_5_4 965 # ASSIGN : s_5_5 532 SHOW_RESULT 1000 END : 1000 (0 seconds) [Sun Jun 18 20:13:19 2006] SHOW_RESULT 1000 CPU : 0.109999999999999 = 0.109999999999999 + 0 + 0 + 0 # BOUND : makespan 1000 1000 MAIN END : (40 seconds) [Sun Jun 18 20:13:19 2006] MAIN CPU : 39.61 = 26.6 + 0.16 + 11.88 + 0.97