# TIMEOUT 18000 MAIN BEGIN : [Sun Jun 18 19:47:54 2006] READ BEGIN : csp/j3-per20-0.csp [Sun Jun 18 19:47:54 2006] READ END : csp/j3-per20-0.csp (0 seconds) [Sun Jun 18 19:47:54 2006] READ CPU : 0.05 = 0.05 + 0 + 0 + 0 # BOUND : makespan 1000 1095 GENERATE_CNF 1095 BEGIN : [Sun Jun 18 19:47:54 2006] GENERATE_CNF 1095 END : 10015 variables 39923 clauses 701942 bytes (1 seconds) [Sun Jun 18 19:47:55 2006] GENERATE_CNF 1095 CPU : 1.37 = 1.37 + 0 + 0 + 0 MODIFY_CNF 1047 BEGIN : [Sun Jun 18 19:47:55 2006] MODIFY_CNF 1047 END : 701947 bytes (0 seconds) [Sun Jun 18 19:47:55 2006] MODIFY_CNF 1047 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1047 BEGIN : [Sun Jun 18 19:47:55 2006] CMD : minisat /tmp/csp2sat13592.cnf /tmp/csp2sat13592.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 38091 104419 | 12697 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 0 (0 /sec) decisions : 10 (200 /sec) propagations : 10015 (200300 /sec) conflict literals : 0 ( nan % deleted) Memory used : 3.39 MB CPU time : 0.05 s SATISFIABLE VERIFY_CNF 1047 END : (0 seconds) [Sun Jun 18 19:47:55 2006] VERIFY_CNF 1047 CPU : 0.07 = 0 + 0.01 + 0.06 + 0 # RESULT : makespan 1047 SATISFIABLE SHOW_RESULT 1047 BEGIN : [Sun Jun 18 19:47:55 2006] # ASSIGN : makespan 1047 # ASSIGN : s_0_0 683 # ASSIGN : s_0_1 626 # ASSIGN : s_0_2 21 # ASSIGN : s_1_0 47 # ASSIGN : s_1_1 679 # ASSIGN : s_1_2 479 # ASSIGN : s_2_0 414 # ASSIGN : s_2_1 25 # ASSIGN : s_2_2 905 SHOW_RESULT 1047 END : 1047 (0 seconds) [Sun Jun 18 19:47:55 2006] SHOW_RESULT 1047 CPU : 0.02 = 0.01 + 0.01 + 0 + 0 # BOUND : makespan 1000 1047 MODIFY_CNF 1023 BEGIN : [Sun Jun 18 19:47:55 2006] MODIFY_CNF 1023 END : 701947 bytes (0 seconds) [Sun Jun 18 19:47:55 2006] MODIFY_CNF 1023 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1023 BEGIN : [Sun Jun 18 19:47:55 2006] CMD : minisat /tmp/csp2sat13592.cnf /tmp/csp2sat13592.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 37227 101827 | 12409 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 5 (125 /sec) decisions : 5 (125 /sec) propagations : 17653 (441325 /sec) conflict literals : 7 (12.50 % deleted) Memory used : 3.36 MB CPU time : 0.04 s UNSATISFIABLE VERIFY_CNF 1023 END : (0 seconds) [Sun Jun 18 19:47:55 2006] VERIFY_CNF 1023 CPU : 0.06 = 0 + 0 + 0.04 + 0.02 # RESULT : makespan 1023 UNSATISFIABLE # BOUND : makespan 1024 1047 MODIFY_CNF 1035 BEGIN : [Sun Jun 18 19:47:55 2006] MODIFY_CNF 1035 END : 701947 bytes (0 seconds) [Sun Jun 18 19:47:55 2006] MODIFY_CNF 1035 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1035 BEGIN : [Sun Jun 18 19:47:55 2006] CMD : minisat /tmp/csp2sat13592.cnf /tmp/csp2sat13592.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 37659 103123 | 12553 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 0 (0 /sec) decisions : 10 (200 /sec) propagations : 10015 (200300 /sec) conflict literals : 0 ( nan % deleted) Memory used : 3.39 MB CPU time : 0.05 s SATISFIABLE VERIFY_CNF 1035 END : (0 seconds) [Sun Jun 18 19:47:55 2006] VERIFY_CNF 1035 CPU : 0.05 = 0 + 0 + 0.05 + 0 # RESULT : makespan 1035 SATISFIABLE SHOW_RESULT 1035 BEGIN : [Sun Jun 18 19:47:55 2006] # ASSIGN : makespan 1035 # ASSIGN : s_0_0 671 # ASSIGN : s_0_1 614 # ASSIGN : s_0_2 9 # ASSIGN : s_1_0 35 # ASSIGN : s_1_1 667 # ASSIGN : s_1_2 467 # ASSIGN : s_2_0 402 # ASSIGN : s_2_1 13 # ASSIGN : s_2_2 893 SHOW_RESULT 1035 END : 1035 (0 seconds) [Sun Jun 18 19:47:55 2006] SHOW_RESULT 1035 CPU : 0.01 = 0.01 + 0 + 0 + 0 # BOUND : makespan 1024 1035 MODIFY_CNF 1029 BEGIN : [Sun Jun 18 19:47:55 2006] MODIFY_CNF 1029 END : 701947 bytes (0 seconds) [Sun Jun 18 19:47:55 2006] MODIFY_CNF 1029 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1029 BEGIN : [Sun Jun 18 19:47:55 2006] CMD : minisat /tmp/csp2sat13592.cnf /tmp/csp2sat13592.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 37443 102475 | 12481 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 0 (0 /sec) decisions : 10 (200 /sec) propagations : 10015 (200300 /sec) conflict literals : 0 ( nan % deleted) Memory used : 3.39 MB CPU time : 0.05 s SATISFIABLE VERIFY_CNF 1029 END : (0 seconds) [Sun Jun 18 19:47:55 2006] VERIFY_CNF 1029 CPU : 0.06 = 0 + 0 + 0.05 + 0.01 # RESULT : makespan 1029 SATISFIABLE SHOW_RESULT 1029 BEGIN : [Sun Jun 18 19:47:55 2006] # ASSIGN : makespan 1029 # ASSIGN : s_0_0 665 # ASSIGN : s_0_1 608 # ASSIGN : s_0_2 3 # ASSIGN : s_1_0 29 # ASSIGN : s_1_1 661 # ASSIGN : s_1_2 461 # ASSIGN : s_2_0 396 # ASSIGN : s_2_1 7 # ASSIGN : s_2_2 887 SHOW_RESULT 1029 END : 1029 (0 seconds) [Sun Jun 18 19:47:55 2006] SHOW_RESULT 1029 CPU : 0.02 = 0.01 + 0.01 + 0 + 0 # BOUND : makespan 1024 1029 MODIFY_CNF 1026 BEGIN : [Sun Jun 18 19:47:55 2006] MODIFY_CNF 1026 END : 701947 bytes (0 seconds) [Sun Jun 18 19:47:55 2006] MODIFY_CNF 1026 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1026 BEGIN : [Sun Jun 18 19:47:55 2006] CMD : minisat /tmp/csp2sat13592.cnf /tmp/csp2sat13592.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 37335 102151 | 12445 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 0 (0 /sec) decisions : 8 (200 /sec) propagations : 10015 (250375 /sec) conflict literals : 0 ( nan % deleted) Memory used : 3.39 MB CPU time : 0.04 s SATISFIABLE VERIFY_CNF 1026 END : (0 seconds) [Sun Jun 18 19:47:55 2006] VERIFY_CNF 1026 CPU : 0.06 = 0 + 0 + 0.05 + 0.01 # RESULT : makespan 1026 SATISFIABLE SHOW_RESULT 1026 BEGIN : [Sun Jun 18 19:47:55 2006] # ASSIGN : makespan 1026 # ASSIGN : s_0_0 662 # ASSIGN : s_0_1 605 # ASSIGN : s_0_2 0 # ASSIGN : s_1_0 26 # ASSIGN : s_1_1 658 # ASSIGN : s_1_2 458 # ASSIGN : s_2_0 393 # ASSIGN : s_2_1 4 # ASSIGN : s_2_2 884 SHOW_RESULT 1026 END : 1026 (0 seconds) [Sun Jun 18 19:47:55 2006] SHOW_RESULT 1026 CPU : 0.02 = 0.02 + 0 + 0 + 0 # BOUND : makespan 1024 1026 MODIFY_CNF 1025 BEGIN : [Sun Jun 18 19:47:55 2006] MODIFY_CNF 1025 END : 701947 bytes (0 seconds) [Sun Jun 18 19:47:55 2006] MODIFY_CNF 1025 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 1025 BEGIN : [Sun Jun 18 19:47:55 2006] CMD : minisat /tmp/csp2sat13592.cnf /tmp/csp2sat13592.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 37299 102043 | 12433 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 5 (100 /sec) decisions : 5 (100 /sec) propagations : 17762 (355240 /sec) conflict literals : 8 (11.11 % deleted) Memory used : 3.36 MB CPU time : 0.05 s UNSATISFIABLE VERIFY_CNF 1025 END : (0 seconds) [Sun Jun 18 19:47:55 2006] VERIFY_CNF 1025 CPU : 0.05 = 0 + 0 + 0.05 + 0 # RESULT : makespan 1025 UNSATISFIABLE # BOUND : makespan 1026 1026 MAIN END : (1 seconds) [Sun Jun 18 19:47:55 2006] MAIN CPU : 1.84 = 1.47 + 0.03 + 0.3 + 0.04