# TIMEOUT 7200 MAIN BEGIN : [Mon Jul 10 17:12:18 2006] READ BEGIN : csp/queen5_5.csp [Mon Jul 10 17:12:18 2006] READ END : csp/queen5_5.csp (0 seconds) [Mon Jul 10 17:12:18 2006] READ CPU : 0.27 = 0.26 + 0.01 + 0 + 0 # BOUND : color 2 8 GENERATE_CNF 8 BEGIN : [Mon Jul 10 17:12:18 2006] GENERATE_CNF 8 END : 578 variables 3154 clauses 45227 bytes (0 seconds) [Mon Jul 10 17:12:18 2006] GENERATE_CNF 8 CPU : 0.16 = 0.16 + 0 + 0 + 0 MODIFY_CNF 5 BEGIN : [Mon Jul 10 17:12:18 2006] MODIFY_CNF 5 END : 45231 bytes (0 seconds) [Mon Jul 10 17:12:18 2006] MODIFY_CNF 5 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 5 BEGIN : [Mon Jul 10 17:12:18 2006] CMD : minisat /tmp/csp2sat24572.cnf /tmp/csp2sat24572.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 2039 6252 | 679 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 0 (nan /sec) decisions : 13 (inf /sec) propagations : 578 (inf /sec) conflict literals : 0 ( nan % deleted) Memory used : 0.90 MB CPU time : 0 s SATISFIABLE VERIFY_CNF 5 END : (0 seconds) [Mon Jul 10 17:12:18 2006] VERIFY_CNF 5 CPU : 0 = 0 + 0 + 0 + 0 # RESULT : color 5 SATISFIABLE SHOW_RESULT 5 BEGIN : [Mon Jul 10 17:12:18 2006] # ASSIGN : color 5 # ASSIGN : n1 3 # ASSIGN : n2 4 # ASSIGN : n3 5 # ASSIGN : n4 1 # ASSIGN : n5 2 # ASSIGN : n6 5 # ASSIGN : n7 1 # ASSIGN : n8 2 # ASSIGN : n9 3 # ASSIGN : n10 4 # ASSIGN : n11 2 # ASSIGN : n12 3 # ASSIGN : n13 4 # ASSIGN : n14 5 # ASSIGN : n15 1 # ASSIGN : n16 4 # ASSIGN : n17 5 # ASSIGN : n18 1 # ASSIGN : n19 2 # ASSIGN : n20 3 # ASSIGN : n21 1 # ASSIGN : n22 2 # ASSIGN : n23 3 # ASSIGN : n24 4 # ASSIGN : n25 5 SHOW_RESULT 5 END : 5 (0 seconds) [Mon Jul 10 17:12:18 2006] SHOW_RESULT 5 CPU : 0 = 0 + 0 + 0 + 0 # BOUND : color 2 5 MODIFY_CNF 3 BEGIN : [Mon Jul 10 17:12:18 2006] MODIFY_CNF 3 END : 45231 bytes (0 seconds) [Mon Jul 10 17:12:18 2006] MODIFY_CNF 3 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 3 BEGIN : [Mon Jul 10 17:12:18 2006] CMD : minisat /tmp/csp2sat24572.cnf /tmp/csp2sat24572.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 1399 4332 | 466 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 7 (inf /sec) decisions : 7 (inf /sec) propagations : 695 (inf /sec) conflict literals : 10 (16.67 % deleted) Memory used : 0.90 MB CPU time : 0 s UNSATISFIABLE VERIFY_CNF 3 END : (0 seconds) [Mon Jul 10 17:12:18 2006] VERIFY_CNF 3 CPU : 0 = 0 + 0 + 0 + 0 # RESULT : color 3 UNSATISFIABLE # BOUND : color 4 5 MODIFY_CNF 4 BEGIN : [Mon Jul 10 17:12:18 2006] MODIFY_CNF 4 END : 45231 bytes (0 seconds) [Mon Jul 10 17:12:18 2006] MODIFY_CNF 4 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 4 BEGIN : [Mon Jul 10 17:12:18 2006] CMD : minisat /tmp/csp2sat24572.cnf /tmp/csp2sat24572.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 1719 5292 | 573 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 35 (inf /sec) decisions : 40 (inf /sec) propagations : 1891 (inf /sec) conflict literals : 115 (13.53 % deleted) Memory used : 0.90 MB CPU time : 0 s UNSATISFIABLE VERIFY_CNF 4 END : (0 seconds) [Mon Jul 10 17:12:18 2006] VERIFY_CNF 4 CPU : 0.01 = 0 + 0 + 0 + 0.01 # RESULT : color 4 UNSATISFIABLE # BOUND : color 5 5 MAIN END : (0 seconds) [Mon Jul 10 17:12:18 2006] MAIN CPU : 0.44 = 0.42 + 0.01 + 0 + 0.01