# TIMEOUT 18000 MAIN BEGIN : [Mon Jun 19 02:06:02 2006] READ BEGIN : csp/j7-per20-2.csp [Mon Jun 19 02:06:02 2006] READ END : csp/j7-per20-2.csp (0 seconds) [Mon Jun 19 02:06:02 2006] READ CPU : 0.64 = 0.64 + 0 + 0 + 0 # BOUND : makespan 1000 2165 GENERATE_CNF 2165 BEGIN : [Mon Jun 19 02:06:02 2006] GENERATE_CNF 2165 END : 107987 variables 1361349 clauses 30301409 bytes (51 seconds) [Mon Jun 19 02:06:53 2006] GENERATE_CNF 2165 CPU : 50.58 = 50.37 + 0.21 + 0 + 0 MODIFY_CNF 1582 BEGIN : [Mon Jun 19 02:06:53 2006] MODIFY_CNF 1582 END : 30301415 bytes (0 seconds) [Mon Jun 19 02:06:53 2006] MODIFY_CNF 1582 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1582 BEGIN : [Mon Jun 19 02:06:53 2006] CMD : minisat /tmp/csp2sat20553.cnf /tmp/csp2sat20553.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 1017609 2946269 | 339203 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 46 (22 /sec) decisions : 321 (151 /sec) propagations : 467958 (219699 /sec) conflict literals : 915 (12.86 % deleted) Memory used : 60.91 MB CPU time : 2.13 s SATISFIABLE VERIFY_CNF 1582 END : (2 seconds) [Mon Jun 19 02:06:55 2006] VERIFY_CNF 1582 CPU : 2.33 = 0 + 0 + 2.17 + 0.16 # RESULT : makespan 1582 SATISFIABLE SHOW_RESULT 1582 BEGIN : [Mon Jun 19 02:06:55 2006] # ASSIGN : makespan 1582 # ASSIGN : s_0_0 587 # ASSIGN : s_0_1 1368 # ASSIGN : s_0_2 23 # ASSIGN : s_0_3 507 # ASSIGN : s_0_4 6 # ASSIGN : s_0_5 315 # ASSIGN : s_0_6 234 # ASSIGN : s_1_0 1023 # ASSIGN : s_1_1 1231 # ASSIGN : s_1_2 244 # ASSIGN : s_1_3 552 # ASSIGN : s_1_4 58 # ASSIGN : s_1_5 534 # ASSIGN : s_1_6 366 # ASSIGN : s_2_0 1336 # ASSIGN : s_2_1 1117 # ASSIGN : s_2_2 274 # ASSIGN : s_2_3 713 # ASSIGN : s_2_4 352 # ASSIGN : s_2_5 843 # ASSIGN : s_2_6 605 # ASSIGN : s_3_0 1452 # ASSIGN : s_3_1 442 # ASSIGN : s_3_2 407 # ASSIGN : s_3_3 906 # ASSIGN : s_3_4 599 # ASSIGN : s_3_5 1041 # ASSIGN : s_3_6 658 # ASSIGN : s_4_0 466 # ASSIGN : s_4_1 1580 # ASSIGN : s_4_2 512 # ASSIGN : s_4_3 1141 # ASSIGN : s_4_4 605 # ASSIGN : s_4_5 1159 # ASSIGN : s_4_6 911 # ASSIGN : s_5_0 523 # ASSIGN : s_5_1 421 # ASSIGN : s_5_2 647 # ASSIGN : s_5_3 1160 # ASSIGN : s_5_4 974 # ASSIGN : s_5_5 1542 # ASSIGN : s_5_6 976 # ASSIGN : s_6_0 720 # ASSIGN : s_6_1 110 # ASSIGN : s_6_2 1196 # ASSIGN : s_6_3 1548 # ASSIGN : s_6_4 1407 # ASSIGN : s_6_5 1562 # ASSIGN : s_6_6 1561 SHOW_RESULT 1582 END : 1582 (0 seconds) [Mon Jun 19 02:06:55 2006] SHOW_RESULT 1582 CPU : 0.19 = 0.18 + 0.01 + 0 + 0 # BOUND : makespan 1000 1582 MODIFY_CNF 1291 BEGIN : [Mon Jun 19 02:06:55 2006] MODIFY_CNF 1291 END : 30301415 bytes (0 seconds) [Mon Jun 19 02:06:55 2006] MODIFY_CNF 1291 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1291 BEGIN : [Mon Jun 19 02:06:55 2006] CMD : minisat /tmp/csp2sat20553.cnf /tmp/csp2sat20553.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 846501 2432945 | 282167 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 0 (0 /sec) decisions : 142 (83 /sec) propagations : 107987 (62783 /sec) conflict literals : 0 ( nan % deleted) Memory used : 60.91 MB CPU time : 1.72 s SATISFIABLE VERIFY_CNF 1291 END : (3 seconds) [Mon Jun 19 02:06:58 2006] VERIFY_CNF 1291 CPU : 2.04 = 0 + 0 + 1.77 + 0.27 # RESULT : makespan 1291 SATISFIABLE SHOW_RESULT 1291 BEGIN : [Mon Jun 19 02:06:58 2006] # ASSIGN : makespan 1291 # ASSIGN : s_0_0 66 # ASSIGN : s_0_1 828 # ASSIGN : s_0_2 1080 # ASSIGN : s_0_3 21 # ASSIGN : s_0_4 473 # ASSIGN : s_0_5 281 # ASSIGN : s_0_6 199 # ASSIGN : s_1_0 832 # ASSIGN : s_1_1 1040 # ASSIGN : s_1_2 197 # ASSIGN : s_1_3 521 # ASSIGN : s_1_4 11 # ASSIGN : s_1_5 503 # ASSIGN : s_1_6 280 # ASSIGN : s_2_0 1045 # ASSIGN : s_2_1 1177 # ASSIGN : s_2_2 791 # ASSIGN : s_2_3 71 # ASSIGN : s_2_4 201 # ASSIGN : s_2_5 551 # ASSIGN : s_2_6 448 # ASSIGN : s_3_0 1161 # ASSIGN : s_3_1 38 # ASSIGN : s_3_2 227 # ASSIGN : s_3_3 343 # ASSIGN : s_3_4 490 # ASSIGN : s_3_5 749 # ASSIGN : s_3_6 501 # ASSIGN : s_4_0 216 # ASSIGN : s_4_1 195 # ASSIGN : s_4_2 262 # ASSIGN : s_4_3 478 # ASSIGN : s_4_4 496 # ASSIGN : s_4_5 867 # ASSIGN : s_4_6 802 # ASSIGN : s_5_0 291 # ASSIGN : s_5_1 197 # ASSIGN : s_5_2 355 # ASSIGN : s_5_3 682 # ASSIGN : s_5_4 1064 # ASSIGN : s_5_5 1250 # ASSIGN : s_5_6 1066 # ASSIGN : s_6_0 529 # ASSIGN : s_6_1 218 # ASSIGN : s_6_2 869 # ASSIGN : s_6_3 1116 # ASSIGN : s_6_4 1129 # ASSIGN : s_6_5 1270 # ASSIGN : s_6_6 1290 SHOW_RESULT 1291 END : 1291 (0 seconds) [Mon Jun 19 02:06:58 2006] SHOW_RESULT 1291 CPU : 0.189999999999998 = 0.189999999999998 + 0 + 0 + 0 # BOUND : makespan 1000 1291 MODIFY_CNF 1145 BEGIN : [Mon Jun 19 02:06:58 2006] MODIFY_CNF 1145 END : 30301415 bytes (0 seconds) [Mon Jun 19 02:06:58 2006] MODIFY_CNF 1145 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1145 BEGIN : [Mon Jun 19 02:06:58 2006] CMD : minisat /tmp/csp2sat20553.cnf /tmp/csp2sat20553.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 760653 2175401 | 253551 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 10 (5 /sec) decisions : 123 (64 /sec) propagations : 132229 (68869 /sec) conflict literals : 172 (0.00 % deleted) Memory used : 60.91 MB CPU time : 1.92 s SATISFIABLE VERIFY_CNF 1145 END : (2 seconds) [Mon Jun 19 02:07:00 2006] VERIFY_CNF 1145 CPU : 2.11 = 0 + 0 + 1.97 + 0.14 # RESULT : makespan 1145 SATISFIABLE SHOW_RESULT 1145 BEGIN : [Mon Jun 19 02:07:00 2006] # ASSIGN : makespan 1145 # ASSIGN : s_0_0 801 # ASSIGN : s_0_1 363 # ASSIGN : s_0_2 934 # ASSIGN : s_0_3 100 # ASSIGN : s_0_4 2 # ASSIGN : s_0_5 145 # ASSIGN : s_0_6 19 # ASSIGN : s_1_0 937 # ASSIGN : s_1_1 575 # ASSIGN : s_1_2 3 # ASSIGN : s_1_3 355 # ASSIGN : s_1_4 712 # ASSIGN : s_1_5 337 # ASSIGN : s_1_6 135 # ASSIGN : s_2_0 685 # ASSIGN : s_2_1 1029 # ASSIGN : s_2_2 607 # ASSIGN : s_2_3 899 # ASSIGN : s_2_4 56 # ASSIGN : s_2_5 406 # ASSIGN : s_2_6 303 # ASSIGN : s_3_0 68 # ASSIGN : s_3_1 743 # ASSIGN : s_3_2 33 # ASSIGN : s_3_3 198 # ASSIGN : s_3_4 345 # ASSIGN : s_3_5 604 # ASSIGN : s_3_6 356 # ASSIGN : s_4_0 287 # ASSIGN : s_4_1 1143 # ASSIGN : s_4_2 96 # ASSIGN : s_4_3 333 # ASSIGN : s_4_4 351 # ASSIGN : s_4_5 722 # ASSIGN : s_4_6 657 # ASSIGN : s_5_0 4 # ASSIGN : s_5_1 900 # ASSIGN : s_5_2 189 # ASSIGN : s_5_3 516 # ASSIGN : s_5_4 898 # ASSIGN : s_5_5 1105 # ASSIGN : s_5_6 921 # ASSIGN : s_6_0 382 # ASSIGN : s_6_1 52 # ASSIGN : s_6_2 723 # ASSIGN : s_6_3 1111 # ASSIGN : s_6_4 970 # ASSIGN : s_6_5 1125 # ASSIGN : s_6_6 1124 SHOW_RESULT 1145 END : 1145 (0 seconds) [Mon Jun 19 02:07:00 2006] SHOW_RESULT 1145 CPU : 0.180000000000002 = 0.170000000000002 + 0.00999999999999998 + 0 + 0 # BOUND : makespan 1000 1145 MODIFY_CNF 1072 BEGIN : [Mon Jun 19 02:07:00 2006] MODIFY_CNF 1072 END : 30301414 bytes (0 seconds) [Mon Jun 19 02:07:00 2006] MODIFY_CNF 1072 CPU : 0.01 = 0 + 0.01 + 0 + 0 VERIFY_CNF 1072 BEGIN : [Mon Jun 19 02:07:00 2006] CMD : minisat /tmp/csp2sat20553.cnf /tmp/csp2sat20553.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 717729 2046629 | 239243 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 9 (5 /sec) decisions : 169 (88 /sec) propagations : 143445 (74711 /sec) conflict literals : 158 (6.51 % deleted) Memory used : 60.91 MB CPU time : 1.92 s SATISFIABLE VERIFY_CNF 1072 END : (2 seconds) [Mon Jun 19 02:07:02 2006] VERIFY_CNF 1072 CPU : 2.15 = 0 + 0 + 1.97 + 0.18 # RESULT : makespan 1072 SATISFIABLE SHOW_RESULT 1072 BEGIN : [Mon Jun 19 02:07:02 2006] # ASSIGN : makespan 1072 # ASSIGN : s_0_0 444 # ASSIGN : s_0_1 230 # ASSIGN : s_0_2 610 # ASSIGN : s_0_3 7 # ASSIGN : s_0_4 52 # ASSIGN : s_0_5 821 # ASSIGN : s_0_6 142 # ASSIGN : s_1_0 577 # ASSIGN : s_1_1 86 # ASSIGN : s_1_2 822 # ASSIGN : s_1_3 852 # ASSIGN : s_1_4 391 # ASSIGN : s_1_5 1013 # ASSIGN : s_1_6 223 # ASSIGN : s_2_0 956 # ASSIGN : s_2_1 472 # ASSIGN : s_2_2 878 # ASSIGN : s_2_3 251 # ASSIGN : s_2_4 598 # ASSIGN : s_2_5 53 # ASSIGN : s_2_6 419 # ASSIGN : s_3_0 785 # ASSIGN : s_3_1 915 # ASSIGN : s_3_2 13 # ASSIGN : s_3_3 116 # ASSIGN : s_3_4 69 # ASSIGN : s_3_5 281 # ASSIGN : s_3_6 534 # ASSIGN : s_4_0 26 # ASSIGN : s_4_1 913 # ASSIGN : s_4_2 979 # ASSIGN : s_4_3 381 # ASSIGN : s_4_4 75 # ASSIGN : s_4_5 399 # ASSIGN : s_4_6 782 # ASSIGN : s_5_0 378 # ASSIGN : s_5_1 442 # ASSIGN : s_5_2 48 # ASSIGN : s_5_3 463 # ASSIGN : s_5_4 845 # ASSIGN : s_5_5 1031 # ASSIGN : s_5_6 847 # ASSIGN : s_6_0 72 # ASSIGN : s_6_1 586 # ASSIGN : s_6_2 375 # ASSIGN : s_6_3 1038 # ASSIGN : s_6_4 897 # ASSIGN : s_6_5 1051 # ASSIGN : s_6_6 1071 SHOW_RESULT 1072 END : 1072 (0 seconds) [Mon Jun 19 02:07:02 2006] SHOW_RESULT 1072 CPU : 0.19 = 0.18 + 0.01 + 0 + 0 # BOUND : makespan 1000 1072 MODIFY_CNF 1036 BEGIN : [Mon Jun 19 02:07:02 2006] MODIFY_CNF 1036 END : 30301414 bytes (0 seconds) [Mon Jun 19 02:07:02 2006] MODIFY_CNF 1036 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1036 BEGIN : [Mon Jun 19 02:07:02 2006] CMD : minisat /tmp/csp2sat20553.cnf /tmp/csp2sat20553.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 696561 1983125 | 232187 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 92 (37 /sec) decisions : 251 (101 /sec) propagations : 669283 (269872 /sec) conflict literals : 2999 (10.10 % deleted) Memory used : 60.91 MB CPU time : 2.48 s SATISFIABLE VERIFY_CNF 1036 END : (3 seconds) [Mon Jun 19 02:07:05 2006] VERIFY_CNF 1036 CPU : 2.69 = 0 + 0 + 2.53 + 0.16 # RESULT : makespan 1036 SATISFIABLE SHOW_RESULT 1036 BEGIN : [Mon Jun 19 02:07:05 2006] # ASSIGN : makespan 1036 # ASSIGN : s_0_0 212 # ASSIGN : s_0_1 612 # ASSIGN : s_0_2 401 # ASSIGN : s_0_3 167 # ASSIGN : s_0_4 1019 # ASSIGN : s_0_5 824 # ASSIGN : s_0_6 86 # ASSIGN : s_1_0 828 # ASSIGN : s_1_1 475 # ASSIGN : s_1_2 612 # ASSIGN : s_1_3 6 # ASSIGN : s_1_4 642 # ASSIGN : s_1_5 343 # ASSIGN : s_1_6 174 # ASSIGN : s_2_0 648 # ASSIGN : s_2_1 844 # ASSIGN : s_2_2 958 # ASSIGN : s_2_3 212 # ASSIGN : s_2_4 395 # ASSIGN : s_2_5 2 # ASSIGN : s_2_6 342 # ASSIGN : s_3_0 70 # ASSIGN : s_3_1 318 # ASSIGN : s_3_2 0 # ASSIGN : s_3_3 883 # ASSIGN : s_3_4 866 # ASSIGN : s_3_5 200 # ASSIGN : s_3_6 516 # ASSIGN : s_4_0 9 # ASSIGN : s_4_1 1013 # ASSIGN : s_4_2 865 # ASSIGN : s_4_3 1018 # ASSIGN : s_4_4 55 # ASSIGN : s_4_5 361 # ASSIGN : s_4_6 764 # ASSIGN : s_5_0 764 # ASSIGN : s_5_1 1015 # ASSIGN : s_5_2 35 # ASSIGN : s_5_3 362 # ASSIGN : s_5_4 1013 # ASSIGN : s_5_5 744 # ASSIGN : s_5_6 829 # ASSIGN : s_6_0 345 # ASSIGN : s_6_1 7 # ASSIGN : s_6_2 648 # ASSIGN : s_6_3 859 # ASSIGN : s_6_4 872 # ASSIGN : s_6_5 1016 # ASSIGN : s_6_6 1015 SHOW_RESULT 1036 END : 1036 (0 seconds) [Mon Jun 19 02:07:05 2006] SHOW_RESULT 1036 CPU : 0.19 = 0.18 + 0.01 + 0 + 0 # BOUND : makespan 1000 1036 MODIFY_CNF 1018 BEGIN : [Mon Jun 19 02:07:05 2006] MODIFY_CNF 1018 END : 30301414 bytes (0 seconds) [Mon Jun 19 02:07:05 2006] MODIFY_CNF 1018 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1018 BEGIN : [Mon Jun 19 02:07:05 2006] CMD : minisat /tmp/csp2sat20553.cnf /tmp/csp2sat20553.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 685977 1951373 | 228659 0 0 nan | 0.000 % | | 100 | 685977 1951373 | 251524 100 3032 30.3 | 59.244 % | | 250 | 685977 1951373 | 276677 250 5031 20.1 | 59.244 % | ============================================================================== restarts : 3 conflicts : 273 (78 /sec) decisions : 482 (137 /sec) propagations : 1862927 (530748 /sec) conflict literals : 5264 (24.60 % deleted) Memory used : 60.93 MB CPU time : 3.51 s SATISFIABLE VERIFY_CNF 1018 END : (4 seconds) [Mon Jun 19 02:07:09 2006] VERIFY_CNF 1018 CPU : 3.77 = 0 + 0 + 3.56 + 0.21 # RESULT : makespan 1018 SATISFIABLE SHOW_RESULT 1018 BEGIN : [Mon Jun 19 02:07:09 2006] # ASSIGN : makespan 1018 # ASSIGN : s_0_0 179 # ASSIGN : s_0_1 806 # ASSIGN : s_0_2 583 # ASSIGN : s_0_3 525 # ASSIGN : s_0_4 26 # ASSIGN : s_0_5 333 # ASSIGN : s_0_6 81 # ASSIGN : s_1_0 622 # ASSIGN : s_1_1 377 # ASSIGN : s_1_2 553 # ASSIGN : s_1_3 1 # ASSIGN : s_1_4 830 # ASSIGN : s_1_5 532 # ASSIGN : s_1_6 162 # ASSIGN : s_2_0 836 # ASSIGN : s_2_1 692 # ASSIGN : s_2_2 328 # ASSIGN : s_2_3 198 # ASSIGN : s_2_4 406 # ASSIGN : s_2_5 0 # ASSIGN : s_2_6 965 # ASSIGN : s_3_0 49 # ASSIGN : s_3_1 535 # ASSIGN : s_3_2 500 # ASSIGN : s_3_3 365 # ASSIGN : s_3_4 43 # ASSIGN : s_3_5 215 # ASSIGN : s_3_6 717 # ASSIGN : s_4_0 3 # ASSIGN : s_4_1 375 # ASSIGN : s_4_2 407 # ASSIGN : s_4_3 507 # ASSIGN : s_4_4 69 # ASSIGN : s_4_5 635 # ASSIGN : s_4_6 570 # ASSIGN : s_5_0 952 # ASSIGN : s_5_1 514 # ASSIGN : s_5_2 1 # ASSIGN : s_5_3 570 # ASSIGN : s_5_4 1016 # ASSIGN : s_5_5 550 # ASSIGN : s_5_6 330 # ASSIGN : s_6_0 312 # ASSIGN : s_6_1 1 # ASSIGN : s_6_2 794 # ASSIGN : s_6_3 1005 # ASSIGN : s_6_4 653 # ASSIGN : s_6_5 615 # ASSIGN : s_6_6 652 SHOW_RESULT 1018 END : 1018 (0 seconds) [Mon Jun 19 02:07:09 2006] SHOW_RESULT 1018 CPU : 0.19 = 0.18 + 0.01 + 0 + 0 # BOUND : makespan 1000 1018 MODIFY_CNF 1009 BEGIN : [Mon Jun 19 02:07:09 2006] MODIFY_CNF 1009 END : 30301414 bytes (0 seconds) [Mon Jun 19 02:07:09 2006] MODIFY_CNF 1009 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1009 BEGIN : [Mon Jun 19 02:07:09 2006] CMD : minisat /tmp/csp2sat20553.cnf /tmp/csp2sat20553.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 680685 1935497 | 226895 0 0 nan | 0.000 % | | 102 | 680685 1935497 | 249584 102 2139 21.0 | 59.661 % | | 254 | 680685 1935497 | 274542 254 4875 19.2 | 59.661 % | | 480 | 680685 1935497 | 301997 480 8274 17.2 | 59.661 % | ============================================================================== restarts : 4 conflicts : 788 (127 /sec) decisions : 1126 (181 /sec) propagations : 4862868 (783071 /sec) conflict literals : 13024 (27.21 % deleted) Memory used : 60.93 MB CPU time : 6.21 s SATISFIABLE VERIFY_CNF 1009 END : (7 seconds) [Mon Jun 19 02:07:16 2006] VERIFY_CNF 1009 CPU : 6.44 = 0 + 0 + 6.26 + 0.18 # RESULT : makespan 1009 SATISFIABLE SHOW_RESULT 1009 BEGIN : [Mon Jun 19 02:07:16 2006] # ASSIGN : makespan 1009 # ASSIGN : s_0_0 552 # ASSIGN : s_0_1 49 # ASSIGN : s_0_2 705 # ASSIGN : s_0_3 964 # ASSIGN : s_0_4 32 # ASSIGN : s_0_5 273 # ASSIGN : s_0_6 471 # ASSIGN : s_1_0 801 # ASSIGN : s_1_1 418 # ASSIGN : s_1_2 577 # ASSIGN : s_1_3 55 # ASSIGN : s_1_4 615 # ASSIGN : s_1_5 13 # ASSIGN : s_1_6 232 # ASSIGN : s_2_0 685 # ASSIGN : s_2_1 872 # ASSIGN : s_2_2 607 # ASSIGN : s_2_3 230 # ASSIGN : s_2_4 360 # ASSIGN : s_2_5 31 # ASSIGN : s_2_6 819 # ASSIGN : s_3_0 55 # ASSIGN : s_3_1 261 # ASSIGN : s_3_2 215 # ASSIGN : s_3_3 436 # ASSIGN : s_3_4 842 # ASSIGN : s_3_5 848 # ASSIGN : s_3_6 571 # ASSIGN : s_4_0 8 # ASSIGN : s_4_1 870 # ASSIGN : s_4_2 916 # ASSIGN : s_4_3 382 # ASSIGN : s_4_4 54 # ASSIGN : s_4_5 465 # ASSIGN : s_4_6 400 # ASSIGN : s_5_0 185 # ASSIGN : s_5_1 986 # ASSIGN : s_5_2 250 # ASSIGN : s_5_3 582 # ASSIGN : s_5_4 1007 # ASSIGN : s_5_5 966 # ASSIGN : s_5_6 1 # ASSIGN : s_6_0 249 # ASSIGN : s_6_1 555 # ASSIGN : s_6_2 4 # ASSIGN : s_6_3 216 # ASSIGN : s_6_4 866 # ASSIGN : s_6_5 229 # ASSIGN : s_6_6 0 SHOW_RESULT 1009 END : 1009 (0 seconds) [Mon Jun 19 02:07:16 2006] SHOW_RESULT 1009 CPU : 0.18 = 0.18 + 0 + 0 + 0 # BOUND : makespan 1000 1009 MODIFY_CNF 1004 BEGIN : [Mon Jun 19 02:07:16 2006] MODIFY_CNF 1004 END : 30301413 bytes (0 seconds) [Mon Jun 19 02:07:16 2006] MODIFY_CNF 1004 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1004 BEGIN : [Mon Jun 19 02:07:16 2006] CMD : minisat /tmp/csp2sat20553.cnf /tmp/csp2sat20553.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 677745 1926677 | 225915 0 0 nan | 0.000 % | | 100 | 677745 1926677 | 248506 100 1604 16.0 | 59.892 % | | 251 | 677745 1926677 | 273357 251 3798 15.1 | 59.892 % | | 476 | 677745 1926677 | 300692 476 7467 15.7 | 59.892 % | | 813 | 677745 1926677 | 330762 813 12457 15.3 | 59.892 % | | 1319 | 677745 1926677 | 363838 1319 19313 14.6 | 59.892 % | ============================================================================== restarts : 6 conflicts : 1491 (142 /sec) decisions : 2085 (198 /sec) propagations : 9586875 (910434 /sec) conflict literals : 22665 (30.80 % deleted) Memory used : 60.93 MB CPU time : 10.53 s SATISFIABLE VERIFY_CNF 1004 END : (11 seconds) [Mon Jun 19 02:07:27 2006] VERIFY_CNF 1004 CPU : 10.79 = 0 + 0 + 10.57 + 0.22 # RESULT : makespan 1004 SATISFIABLE SHOW_RESULT 1004 BEGIN : [Mon Jun 19 02:07:27 2006] # ASSIGN : makespan 1004 # ASSIGN : s_0_0 304 # ASSIGN : s_0_1 461 # ASSIGN : s_0_2 93 # ASSIGN : s_0_3 959 # ASSIGN : s_0_4 69 # ASSIGN : s_0_5 674 # ASSIGN : s_0_6 870 # ASSIGN : s_1_0 796 # ASSIGN : s_1_1 196 # ASSIGN : s_1_2 519 # ASSIGN : s_1_3 35 # ASSIGN : s_1_4 333 # ASSIGN : s_1_5 9 # ASSIGN : s_1_6 628 # ASSIGN : s_2_0 680 # ASSIGN : s_2_1 347 # ASSIGN : s_2_2 8 # ASSIGN : s_2_3 821 # ASSIGN : s_2_4 86 # ASSIGN : s_2_5 476 # ASSIGN : s_2_6 951 # ASSIGN : s_3_0 483 # ASSIGN : s_3_1 39 # ASSIGN : s_3_2 642 # ASSIGN : s_3_3 686 # ASSIGN : s_3_4 680 # ASSIGN : s_3_5 866 # ASSIGN : s_3_6 235 # ASSIGN : s_4_0 437 # ASSIGN : s_4_1 37 # ASSIGN : s_4_2 549 # ASSIGN : s_4_3 642 # ASSIGN : s_4_4 698 # ASSIGN : s_4_5 54 # ASSIGN : s_4_6 484 # ASSIGN : s_5_0 613 # ASSIGN : s_5_1 4 # ASSIGN : s_5_2 677 # ASSIGN : s_5_3 231 # ASSIGN : s_5_4 25 # ASSIGN : s_5_5 27 # ASSIGN : s_5_6 47 # ASSIGN : s_6_0 1 # ASSIGN : s_6_1 673 # ASSIGN : s_6_2 308 # ASSIGN : s_6_3 660 # ASSIGN : s_6_4 519 # ASSIGN : s_6_5 984 # ASSIGN : s_6_6 0 SHOW_RESULT 1004 END : 1004 (0 seconds) [Mon Jun 19 02:07:27 2006] SHOW_RESULT 1004 CPU : 0.180000000000002 = 0.170000000000002 + 0.00999999999999995 + 0 + 0 # BOUND : makespan 1000 1004 MODIFY_CNF 1002 BEGIN : [Mon Jun 19 02:07:27 2006] MODIFY_CNF 1002 END : 30301413 bytes (0 seconds) [Mon Jun 19 02:07:27 2006] MODIFY_CNF 1002 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1002 BEGIN : [Mon Jun 19 02:07:27 2006] CMD : minisat /tmp/csp2sat20553.cnf /tmp/csp2sat20553.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 676569 1923149 | 225523 0 0 nan | 0.000 % | | 102 | 676569 1923149 | 248075 102 1544 15.1 | 59.985 % | | 252 | 676569 1923149 | 272882 252 4056 16.1 | 59.985 % | | 479 | 676569 1923149 | 300171 479 7224 15.1 | 59.985 % | | 819 | 676569 1923149 | 330188 819 11584 14.1 | 59.985 % | | 1326 | 676569 1923149 | 363207 1326 18268 13.8 | 59.985 % | | 2085 | 676569 1923149 | 399527 2085 29682 14.2 | 59.985 % | | 3224 | 676571 1923149 | 439480 3222 45927 14.3 | 59.985 % | | 4932 | 673385 1913603 | 483428 4137 59955 14.5 | 60.239 % | ============================================================================== restarts : 9 conflicts : 6299 (154 /sec) decisions : 7790 (191 /sec) propagations : 41086468 (1005543 /sec) conflict literals : 92702 (35.43 % deleted) Memory used : 60.51 MB CPU time : 40.86 s UNSATISFIABLE VERIFY_CNF 1002 END : (41 seconds) [Mon Jun 19 02:08:08 2006] VERIFY_CNF 1002 CPU : 41.01 = 0.00999999999999801 + 0 + 40.86 + 0.14 # RESULT : makespan 1002 UNSATISFIABLE # BOUND : makespan 1003 1004 MODIFY_CNF 1003 BEGIN : [Mon Jun 19 02:08:08 2006] MODIFY_CNF 1003 END : 30301413 bytes (0 seconds) [Mon Jun 19 02:08:08 2006] MODIFY_CNF 1003 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1003 BEGIN : [Mon Jun 19 02:08:08 2006] CMD : minisat /tmp/csp2sat20553.cnf /tmp/csp2sat20553.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 677157 1924913 | 225719 0 0 nan | 0.000 % | | 102 | 677157 1924913 | 248290 102 1692 16.6 | 59.939 % | | 252 | 677157 1924913 | 273119 252 4243 16.8 | 59.939 % | | 478 | 677157 1924913 | 300431 478 7811 16.3 | 59.939 % | ============================================================================== restarts : 4 conflicts : 549 (110 /sec) decisions : 912 (183 /sec) propagations : 3529307 (707276 /sec) conflict literals : 8872 (27.88 % deleted) Memory used : 60.93 MB CPU time : 4.99 s SATISFIABLE VERIFY_CNF 1003 END : (5 seconds) [Mon Jun 19 02:08:13 2006] VERIFY_CNF 1003 CPU : 5.25000000000001 = 0 + 0 + 5.04000000000001 + 0.21 # RESULT : makespan 1003 SATISFIABLE SHOW_RESULT 1003 BEGIN : [Mon Jun 19 02:08:13 2006] # ASSIGN : makespan 1003 # ASSIGN : s_0_0 303 # ASSIGN : s_0_1 459 # ASSIGN : s_0_2 92 # ASSIGN : s_0_3 958 # ASSIGN : s_0_4 67 # ASSIGN : s_0_5 672 # ASSIGN : s_0_6 868 # ASSIGN : s_1_0 795 # ASSIGN : s_1_1 194 # ASSIGN : s_1_2 517 # ASSIGN : s_1_3 33 # ASSIGN : s_1_4 331 # ASSIGN : s_1_5 8 # ASSIGN : s_1_6 627 # ASSIGN : s_2_0 679 # ASSIGN : s_2_1 345 # ASSIGN : s_2_2 6 # ASSIGN : s_2_3 819 # ASSIGN : s_2_4 84 # ASSIGN : s_2_5 474 # ASSIGN : s_2_6 949 # ASSIGN : s_3_0 482 # ASSIGN : s_3_1 37 # ASSIGN : s_3_2 641 # ASSIGN : s_3_3 684 # ASSIGN : s_3_4 678 # ASSIGN : s_3_5 864 # ASSIGN : s_3_6 234 # ASSIGN : s_4_0 436 # ASSIGN : s_4_1 35 # ASSIGN : s_4_2 547 # ASSIGN : s_4_3 640 # ASSIGN : s_4_4 697 # ASSIGN : s_4_5 53 # ASSIGN : s_4_6 482 # ASSIGN : s_5_0 612 # ASSIGN : s_5_1 3 # ASSIGN : s_5_2 676 # ASSIGN : s_5_3 230 # ASSIGN : s_5_4 24 # ASSIGN : s_5_5 26 # ASSIGN : s_5_6 46 # ASSIGN : s_6_0 0 # ASSIGN : s_6_1 671 # ASSIGN : s_6_2 306 # ASSIGN : s_6_3 658 # ASSIGN : s_6_4 517 # ASSIGN : s_6_5 982 # ASSIGN : s_6_6 1002 SHOW_RESULT 1003 END : 1003 (0 seconds) [Mon Jun 19 02:08:13 2006] SHOW_RESULT 1003 CPU : 0.180000000000002 = 0.170000000000002 + 0.01 + 0 + 0 # BOUND : makespan 1003 1003 MAIN END : (131 seconds) [Mon Jun 19 02:08:13 2006] MAIN CPU : 131.52 = 52.66 + 0.29 + 76.7 + 1.87