# TIMEOUT 18000 MAIN BEGIN : [Sun Jun 18 19:51:05 2006] READ BEGIN : csp/j5-per10-1.csp [Sun Jun 18 19:51:05 2006] READ END : csp/j5-per10-1.csp (0 seconds) [Sun Jun 18 19:51:05 2006] READ CPU : 0.23 = 0.23 + 0 + 0 + 0 # BOUND : makespan 1000 1476 GENERATE_CNF 1476 BEGIN : [Sun Jun 18 19:51:05 2006] GENERATE_CNF 1476 END : 37653 variables 307928 clauses 6320279 bytes (12 seconds) [Sun Jun 18 19:51:17 2006] GENERATE_CNF 1476 CPU : 11.26 = 11.23 + 0.03 + 0 + 0 MODIFY_CNF 1238 BEGIN : [Sun Jun 18 19:51:17 2006] MODIFY_CNF 1238 END : 6320285 bytes (0 seconds) [Sun Jun 18 19:51:17 2006] MODIFY_CNF 1238 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1238 BEGIN : [Sun Jun 18 19:51:17 2006] CMD : minisat /tmp/csp2sat13783.cnf /tmp/csp2sat13783.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 259948 742774 | 86649 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 1 (3 /sec) decisions : 59 (151 /sec) propagations : 42248 (108328 /sec) conflict literals : 7 (0.00 % deleted) Memory used : 15.57 MB CPU time : 0.39 s SATISFIABLE VERIFY_CNF 1238 END : (0 seconds) [Sun Jun 18 19:51:17 2006] VERIFY_CNF 1238 CPU : 0.44 = 0.00999999999999979 + 0 + 0.41 + 0.02 # RESULT : makespan 1238 SATISFIABLE SHOW_RESULT 1238 BEGIN : [Sun Jun 18 19:51:17 2006] # ASSIGN : makespan 1238 # ASSIGN : s_0_0 26 # ASSIGN : s_0_1 961 # ASSIGN : s_0_2 662 # ASSIGN : s_0_3 82 # ASSIGN : s_0_4 151 # ASSIGN : s_1_0 852 # ASSIGN : s_1_1 1096 # ASSIGN : s_1_2 54 # ASSIGN : s_1_3 212 # ASSIGN : s_1_4 561 # ASSIGN : s_2_0 70 # ASSIGN : s_2_1 313 # ASSIGN : s_2_2 290 # ASSIGN : s_2_3 695 # ASSIGN : s_2_4 632 # ASSIGN : s_3_0 1052 # ASSIGN : s_3_1 278 # ASSIGN : s_3_2 334 # ASSIGN : s_3_3 1018 # ASSIGN : s_3_4 663 # ASSIGN : s_4_0 317 # ASSIGN : s_4_1 667 # ASSIGN : s_4_2 956 # ASSIGN : s_4_3 1053 # ASSIGN : s_4_4 1205 SHOW_RESULT 1238 END : 1238 (0 seconds) [Sun Jun 18 19:51:17 2006] SHOW_RESULT 1238 CPU : 0.0600000000000007 = 0.0500000000000007 + 0.01 + 0 + 0 # BOUND : makespan 1000 1238 MODIFY_CNF 1119 BEGIN : [Sun Jun 18 19:51:17 2006] MODIFY_CNF 1119 END : 6320285 bytes (0 seconds) [Sun Jun 18 19:51:17 2006] MODIFY_CNF 1119 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1119 BEGIN : [Sun Jun 18 19:51:17 2006] CMD : minisat /tmp/csp2sat13783.cnf /tmp/csp2sat13783.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 236148 671374 | 78716 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 1 (3 /sec) decisions : 49 (132 /sec) propagations : 39383 (106441 /sec) conflict literals : 7 (12.50 % deleted) Memory used : 15.61 MB CPU time : 0.37 s SATISFIABLE VERIFY_CNF 1119 END : (1 seconds) [Sun Jun 18 19:51:18 2006] VERIFY_CNF 1119 CPU : 0.45 = 0 + 0 + 0.39 + 0.06 # RESULT : makespan 1119 SATISFIABLE SHOW_RESULT 1119 BEGIN : [Sun Jun 18 19:51:18 2006] # ASSIGN : makespan 1119 # ASSIGN : s_0_0 53 # ASSIGN : s_0_1 915 # ASSIGN : s_0_2 507 # ASSIGN : s_0_3 1050 # ASSIGN : s_0_4 97 # ASSIGN : s_1_0 676 # ASSIGN : s_1_1 370 # ASSIGN : s_1_2 938 # ASSIGN : s_1_3 21 # ASSIGN : s_1_4 605 # ASSIGN : s_2_0 876 # ASSIGN : s_2_1 16 # ASSIGN : s_2_2 1096 # ASSIGN : s_2_3 374 # ASSIGN : s_2_4 700 # ASSIGN : s_3_0 490 # ASSIGN : s_3_1 335 # ASSIGN : s_3_2 7 # ASSIGN : s_3_3 697 # ASSIGN : s_3_4 731 # ASSIGN : s_4_0 140 # ASSIGN : s_4_1 512 # ASSIGN : s_4_2 801 # ASSIGN : s_4_3 898 # ASSIGN : s_4_4 1086 SHOW_RESULT 1119 END : 1119 (0 seconds) [Sun Jun 18 19:51:18 2006] SHOW_RESULT 1119 CPU : 0.0499999999999989 = 0.0499999999999989 + 0 + 0 + 0 # BOUND : makespan 1000 1119 MODIFY_CNF 1059 BEGIN : [Sun Jun 18 19:51:18 2006] MODIFY_CNF 1059 END : 6320284 bytes (0 seconds) [Sun Jun 18 19:51:18 2006] MODIFY_CNF 1059 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1059 BEGIN : [Sun Jun 18 19:51:18 2006] CMD : minisat /tmp/csp2sat13783.cnf /tmp/csp2sat13783.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 224148 635374 | 74716 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 6 (15 /sec) decisions : 45 (115 /sec) propagations : 58251 (149362 /sec) conflict literals : 52 (20.00 % deleted) Memory used : 15.61 MB CPU time : 0.39 s SATISFIABLE VERIFY_CNF 1059 END : (0 seconds) [Sun Jun 18 19:51:18 2006] VERIFY_CNF 1059 CPU : 0.47 = 0 + 0 + 0.41 + 0.06 # RESULT : makespan 1059 SATISFIABLE SHOW_RESULT 1059 BEGIN : [Sun Jun 18 19:51:18 2006] # ASSIGN : makespan 1059 # ASSIGN : s_0_0 411 # ASSIGN : s_0_1 889 # ASSIGN : s_0_2 595 # ASSIGN : s_0_3 455 # ASSIGN : s_0_4 1 # ASSIGN : s_1_0 211 # ASSIGN : s_1_1 58 # ASSIGN : s_1_2 901 # ASSIGN : s_1_3 524 # ASSIGN : s_1_4 416 # ASSIGN : s_2_0 839 # ASSIGN : s_2_1 520 # ASSIGN : s_2_2 70 # ASSIGN : s_2_3 132 # ASSIGN : s_2_4 487 # ASSIGN : s_3_0 4 # ASSIGN : s_3_1 1024 # ASSIGN : s_3_2 190 # ASSIGN : s_3_3 873 # ASSIGN : s_3_4 518 # ASSIGN : s_4_0 489 # ASSIGN : s_4_1 200 # ASSIGN : s_4_2 93 # ASSIGN : s_4_3 907 # ASSIGN : s_4_4 874 SHOW_RESULT 1059 END : 1059 (0 seconds) [Sun Jun 18 19:51:18 2006] SHOW_RESULT 1059 CPU : 0.0500000000000007 = 0.0500000000000007 + 0 + 0 + 0 # BOUND : makespan 1000 1059 MODIFY_CNF 1029 BEGIN : [Sun Jun 18 19:51:18 2006] MODIFY_CNF 1029 END : 6320284 bytes (0 seconds) [Sun Jun 18 19:51:18 2006] MODIFY_CNF 1029 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1029 BEGIN : [Sun Jun 18 19:51:18 2006] CMD : minisat /tmp/csp2sat13783.cnf /tmp/csp2sat13783.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 218148 617374 | 72716 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 13 (32 /sec) decisions : 55 (134 /sec) propagations : 86350 (210610 /sec) conflict literals : 155 (13.41 % deleted) Memory used : 15.61 MB CPU time : 0.41 s SATISFIABLE VERIFY_CNF 1029 END : (1 seconds) [Sun Jun 18 19:51:19 2006] VERIFY_CNF 1029 CPU : 0.5 = 0 + 0 + 0.43 + 0.07 # RESULT : makespan 1029 SATISFIABLE SHOW_RESULT 1029 BEGIN : [Sun Jun 18 19:51:19 2006] # ASSIGN : makespan 1029 # ASSIGN : s_0_0 985 # ASSIGN : s_0_1 556 # ASSIGN : s_0_2 691 # ASSIGN : s_0_3 46 # ASSIGN : s_0_4 146 # ASSIGN : s_1_0 249 # ASSIGN : s_1_1 107 # ASSIGN : s_1_2 488 # ASSIGN : s_1_3 646 # ASSIGN : s_1_4 36 # ASSIGN : s_2_0 29 # ASSIGN : s_2_1 710 # ASSIGN : s_2_2 668 # ASSIGN : s_2_3 286 # ASSIGN : s_2_4 609 # ASSIGN : s_3_0 449 # ASSIGN : s_3_1 72 # ASSIGN : s_3_2 121 # ASSIGN : s_3_3 995 # ASSIGN : s_3_4 640 # ASSIGN : s_4_0 635 # ASSIGN : s_4_1 267 # ASSIGN : s_4_2 18 # ASSIGN : s_4_3 115 # ASSIGN : s_4_4 996 SHOW_RESULT 1029 END : 1029 (0 seconds) [Sun Jun 18 19:51:19 2006] SHOW_RESULT 1029 CPU : 0.0600000000000005 = 0.0600000000000005 + 0 + 0 + 0 # BOUND : makespan 1000 1029 MODIFY_CNF 1014 BEGIN : [Sun Jun 18 19:51:19 2006] MODIFY_CNF 1014 END : 6320284 bytes (0 seconds) [Sun Jun 18 19:51:19 2006] MODIFY_CNF 1014 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1014 BEGIN : [Sun Jun 18 19:51:19 2006] CMD : minisat /tmp/csp2sat13783.cnf /tmp/csp2sat13783.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 215148 608374 | 71716 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 7 (17 /sec) decisions : 38 (93 /sec) propagations : 68027 (165920 /sec) conflict literals : 68 (8.11 % deleted) Memory used : 15.61 MB CPU time : 0.41 s SATISFIABLE VERIFY_CNF 1014 END : (0 seconds) [Sun Jun 18 19:51:19 2006] VERIFY_CNF 1014 CPU : 0.48 = 0 + 0 + 0.43 + 0.05 # RESULT : makespan 1014 SATISFIABLE SHOW_RESULT 1014 BEGIN : [Sun Jun 18 19:51:19 2006] # ASSIGN : makespan 1014 # ASSIGN : s_0_0 970 # ASSIGN : s_0_1 541 # ASSIGN : s_0_2 676 # ASSIGN : s_0_3 31 # ASSIGN : s_0_4 131 # ASSIGN : s_1_0 234 # ASSIGN : s_1_1 92 # ASSIGN : s_1_2 473 # ASSIGN : s_1_3 631 # ASSIGN : s_1_4 21 # ASSIGN : s_2_0 14 # ASSIGN : s_2_1 695 # ASSIGN : s_2_2 653 # ASSIGN : s_2_3 271 # ASSIGN : s_2_4 594 # ASSIGN : s_3_0 434 # ASSIGN : s_3_1 57 # ASSIGN : s_3_2 106 # ASSIGN : s_3_3 980 # ASSIGN : s_3_4 625 # ASSIGN : s_4_0 620 # ASSIGN : s_4_1 252 # ASSIGN : s_4_2 3 # ASSIGN : s_4_3 100 # ASSIGN : s_4_4 981 SHOW_RESULT 1014 END : 1014 (1 seconds) [Sun Jun 18 19:51:20 2006] SHOW_RESULT 1014 CPU : 0.0499999999999989 = 0.0499999999999989 + 0 + 0 + 0 # BOUND : makespan 1000 1014 MODIFY_CNF 1007 BEGIN : [Sun Jun 18 19:51:20 2006] MODIFY_CNF 1007 END : 6320283 bytes (0 seconds) [Sun Jun 18 19:51:20 2006] MODIFY_CNF 1007 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1007 BEGIN : [Sun Jun 18 19:51:20 2006] CMD : minisat /tmp/csp2sat13783.cnf /tmp/csp2sat13783.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 213748 604174 | 71249 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 44 (92 /sec) decisions : 110 (229 /sec) propagations : 203847 (424681 /sec) conflict literals : 379 (21.53 % deleted) Memory used : 15.61 MB CPU time : 0.48 s SATISFIABLE VERIFY_CNF 1007 END : (0 seconds) [Sun Jun 18 19:51:20 2006] VERIFY_CNF 1007 CPU : 0.57 = 0 + 0 + 0.49 + 0.08 # RESULT : makespan 1007 SATISFIABLE SHOW_RESULT 1007 BEGIN : [Sun Jun 18 19:51:20 2006] # ASSIGN : makespan 1007 # ASSIGN : s_0_0 6 # ASSIGN : s_0_1 803 # ASSIGN : s_0_2 509 # ASSIGN : s_0_3 938 # ASSIGN : s_0_4 99 # ASSIGN : s_1_0 587 # ASSIGN : s_1_1 355 # ASSIGN : s_1_2 849 # ASSIGN : s_1_3 6 # ASSIGN : s_1_4 516 # ASSIGN : s_2_0 787 # ASSIGN : s_2_1 36 # ASSIGN : s_2_2 377 # ASSIGN : s_2_3 463 # ASSIGN : s_2_4 5 # ASSIGN : s_3_0 401 # ASSIGN : s_3_1 1 # ASSIGN : s_3_2 39 # ASSIGN : s_3_3 367 # ASSIGN : s_3_4 619 # ASSIGN : s_4_0 50 # ASSIGN : s_4_1 497 # ASSIGN : s_4_2 400 # ASSIGN : s_4_3 786 # ASSIGN : s_4_4 974 SHOW_RESULT 1007 END : 1007 (0 seconds) [Sun Jun 18 19:51:20 2006] SHOW_RESULT 1007 CPU : 0.0600000000000005 = 0.0600000000000005 + 0 + 0 + 0 # BOUND : makespan 1000 1007 MODIFY_CNF 1003 BEGIN : [Sun Jun 18 19:51:20 2006] MODIFY_CNF 1003 END : 6320283 bytes (0 seconds) [Sun Jun 18 19:51:20 2006] MODIFY_CNF 1003 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1003 BEGIN : [Sun Jun 18 19:51:20 2006] CMD : minisat /tmp/csp2sat13783.cnf /tmp/csp2sat13783.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 212948 601774 | 70982 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 43 (83 /sec) decisions : 83 (160 /sec) propagations : 211004 (405777 /sec) conflict literals : 411 (21.11 % deleted) Memory used : 15.61 MB CPU time : 0.52 s SATISFIABLE VERIFY_CNF 1003 END : (1 seconds) [Sun Jun 18 19:51:21 2006] VERIFY_CNF 1003 CPU : 0.58 = 0 + 0 + 0.54 + 0.04 # RESULT : makespan 1003 SATISFIABLE SHOW_RESULT 1003 BEGIN : [Sun Jun 18 19:51:21 2006] # ASSIGN : makespan 1003 # ASSIGN : s_0_0 2 # ASSIGN : s_0_1 799 # ASSIGN : s_0_2 505 # ASSIGN : s_0_3 934 # ASSIGN : s_0_4 95 # ASSIGN : s_1_0 583 # ASSIGN : s_1_1 351 # ASSIGN : s_1_2 845 # ASSIGN : s_1_3 2 # ASSIGN : s_1_4 512 # ASSIGN : s_2_0 783 # ASSIGN : s_2_1 32 # ASSIGN : s_2_2 373 # ASSIGN : s_2_3 459 # ASSIGN : s_2_4 1 # ASSIGN : s_3_0 397 # ASSIGN : s_3_1 968 # ASSIGN : s_3_2 35 # ASSIGN : s_3_3 363 # ASSIGN : s_3_4 613 # ASSIGN : s_4_0 46 # ASSIGN : s_4_1 493 # ASSIGN : s_4_2 396 # ASSIGN : s_4_3 782 # ASSIGN : s_4_4 970 SHOW_RESULT 1003 END : 1003 (0 seconds) [Sun Jun 18 19:51:21 2006] SHOW_RESULT 1003 CPU : 0.0599999999999989 = 0.0499999999999989 + 0.01 + 0 + 0 # BOUND : makespan 1000 1003 MODIFY_CNF 1001 BEGIN : [Sun Jun 18 19:51:21 2006] MODIFY_CNF 1001 END : 6320283 bytes (0 seconds) [Sun Jun 18 19:51:21 2006] MODIFY_CNF 1001 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1001 BEGIN : [Sun Jun 18 19:51:21 2006] CMD : minisat /tmp/csp2sat13783.cnf /tmp/csp2sat13783.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 212548 600574 | 70849 0 0 nan | 0.000 % | | 101 | 212552 600574 | 77933 97 848 8.7 | 45.346 % | ============================================================================== restarts : 2 conflicts : 145 (175 /sec) decisions : 165 (199 /sec) propagations : 707583 (852510 /sec) conflict literals : 1083 (33.31 % deleted) Memory used : 15.48 MB CPU time : 0.83 s UNSATISFIABLE VERIFY_CNF 1001 END : (1 seconds) [Sun Jun 18 19:51:22 2006] VERIFY_CNF 1001 CPU : 0.9 = 0 + 0 + 0.83 + 0.07 # RESULT : makespan 1001 UNSATISFIABLE # BOUND : makespan 1002 1003 MODIFY_CNF 1002 BEGIN : [Sun Jun 18 19:51:22 2006] MODIFY_CNF 1002 END : 6320283 bytes (0 seconds) [Sun Jun 18 19:51:22 2006] MODIFY_CNF 1002 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1002 BEGIN : [Sun Jun 18 19:51:22 2006] CMD : minisat /tmp/csp2sat13783.cnf /tmp/csp2sat13783.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 212748 601174 | 70916 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 41 (87 /sec) decisions : 79 (168 /sec) propagations : 183989 (391466 /sec) conflict literals : 382 (18.72 % deleted) Memory used : 15.61 MB CPU time : 0.47 s SATISFIABLE VERIFY_CNF 1002 END : (0 seconds) [Sun Jun 18 19:51:22 2006] VERIFY_CNF 1002 CPU : 0.55 = 0 + 0 + 0.49 + 0.06 # RESULT : makespan 1002 SATISFIABLE SHOW_RESULT 1002 BEGIN : [Sun Jun 18 19:51:22 2006] # ASSIGN : makespan 1002 # ASSIGN : s_0_0 1 # ASSIGN : s_0_1 798 # ASSIGN : s_0_2 504 # ASSIGN : s_0_3 933 # ASSIGN : s_0_4 94 # ASSIGN : s_1_0 582 # ASSIGN : s_1_1 350 # ASSIGN : s_1_2 844 # ASSIGN : s_1_3 1 # ASSIGN : s_1_4 511 # ASSIGN : s_2_0 782 # ASSIGN : s_2_1 31 # ASSIGN : s_2_2 372 # ASSIGN : s_2_3 458 # ASSIGN : s_2_4 0 # ASSIGN : s_3_0 396 # ASSIGN : s_3_1 967 # ASSIGN : s_3_2 34 # ASSIGN : s_3_3 362 # ASSIGN : s_3_4 612 # ASSIGN : s_4_0 45 # ASSIGN : s_4_1 492 # ASSIGN : s_4_2 395 # ASSIGN : s_4_3 781 # ASSIGN : s_4_4 969 SHOW_RESULT 1002 END : 1002 (0 seconds) [Sun Jun 18 19:51:22 2006] SHOW_RESULT 1002 CPU : 0.0500000000000007 = 0.0500000000000007 + 0 + 0 + 0 # BOUND : makespan 1002 1002 MAIN END : (17 seconds) [Sun Jun 18 19:51:22 2006] MAIN CPU : 16.87 = 11.89 + 0.05 + 4.42 + 0.51