# TIMEOUT 7200 MAIN BEGIN : [Thu Jul 6 19:02:57 2006] READ BEGIN : csp/DSJC125.1.csp [Thu Jul 6 19:02:57 2006] READ END : csp/DSJC125.1.csp (2 seconds) [Thu Jul 6 19:02:59 2006] READ CPU : 1.22 = 1.21 + 0.01 + 0 + 0 # BOUND : color 2 8 GENERATE_CNF 8 BEGIN : [Thu Jul 6 19:02:59 2006] GENERATE_CNF 8 END : 2730 variables 14646 clauses 235514 bytes (0 seconds) [Thu Jul 6 19:02:59 2006] GENERATE_CNF 8 CPU : 0.76 = 0.75 + 0.01 + 0 + 0 MODIFY_CNF 5 BEGIN : [Thu Jul 6 19:02:59 2006] MODIFY_CNF 5 END : 235518 bytes (0 seconds) [Thu Jul 6 19:02:59 2006] MODIFY_CNF 5 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 5 BEGIN : [Thu Jul 6 19:02:59 2006] CMD : minisat /tmp/csp2sat24433.cnf /tmp/csp2sat24433.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 9475 29036 | 3158 0 0 nan | 0.000 % | | 100 | 9475 29036 | 3473 100 2564 25.6 | 27.656 % | ============================================================================== restarts : 2 conflicts : 196 (3920 /sec) decisions : 350 (7000 /sec) propagations : 84067 (1681340 /sec) conflict literals : 6571 (4.63 % deleted) Memory used : 1.60 MB CPU time : 0.05 s SATISFIABLE VERIFY_CNF 5 END : (0 seconds) [Thu Jul 6 19:02:59 2006] VERIFY_CNF 5 CPU : 0.07 = 0.01 + 0 + 0.05 + 0.01 # RESULT : color 5 SATISFIABLE SHOW_RESULT 5 BEGIN : [Thu Jul 6 19:02:59 2006] # ASSIGN : color 5 # ASSIGN : n1 4 # ASSIGN : n2 3 # ASSIGN : n3 1 # ASSIGN : n4 4 # ASSIGN : n5 1 # ASSIGN : n6 4 # ASSIGN : n7 1 # ASSIGN : n8 1 # ASSIGN : n9 3 # ASSIGN : n10 4 # ASSIGN : n11 1 # ASSIGN : n12 4 # ASSIGN : n13 5 # ASSIGN : n14 4 # ASSIGN : n15 5 # ASSIGN : n16 3 # ASSIGN : n17 1 # ASSIGN : n18 5 # ASSIGN : n19 4 # ASSIGN : n20 2 # ASSIGN : n21 5 # ASSIGN : n22 3 # ASSIGN : n23 1 # ASSIGN : n24 1 # ASSIGN : n25 5 # ASSIGN : n26 4 # ASSIGN : n27 1 # ASSIGN : n28 5 # ASSIGN : n29 2 # ASSIGN : n30 4 # ASSIGN : n31 3 # ASSIGN : n32 4 # ASSIGN : n33 1 # ASSIGN : n34 3 # ASSIGN : n35 2 # ASSIGN : n36 4 # ASSIGN : n37 4 # ASSIGN : n38 2 # ASSIGN : n39 1 # ASSIGN : n40 1 # ASSIGN : n41 4 # ASSIGN : n42 2 # ASSIGN : n43 4 # ASSIGN : n44 2 # ASSIGN : n45 2 # ASSIGN : n46 1 # ASSIGN : n47 3 # ASSIGN : n48 5 # ASSIGN : n49 5 # ASSIGN : n50 5 # ASSIGN : n51 3 # ASSIGN : n52 2 # ASSIGN : n53 3 # ASSIGN : n54 1 # ASSIGN : n55 3 # ASSIGN : n56 3 # ASSIGN : n57 3 # ASSIGN : n58 4 # ASSIGN : n59 1 # ASSIGN : n60 5 # ASSIGN : n61 5 # ASSIGN : n62 5 # ASSIGN : n63 5 # ASSIGN : n64 5 # ASSIGN : n65 2 # ASSIGN : n66 2 # ASSIGN : n67 5 # ASSIGN : n68 1 # ASSIGN : n69 3 # ASSIGN : n70 2 # ASSIGN : n71 4 # ASSIGN : n72 3 # ASSIGN : n73 2 # ASSIGN : n74 4 # ASSIGN : n75 1 # ASSIGN : n76 5 # ASSIGN : n77 2 # ASSIGN : n78 1 # ASSIGN : n79 2 # ASSIGN : n80 3 # ASSIGN : n81 1 # ASSIGN : n82 5 # ASSIGN : n83 4 # ASSIGN : n84 4 # ASSIGN : n85 5 # ASSIGN : n86 2 # ASSIGN : n87 1 # ASSIGN : n88 3 # ASSIGN : n89 1 # ASSIGN : n90 4 # ASSIGN : n91 2 # ASSIGN : n92 3 # ASSIGN : n93 3 # ASSIGN : n94 3 # ASSIGN : n95 1 # ASSIGN : n96 4 # ASSIGN : n97 5 # ASSIGN : n98 2 # ASSIGN : n99 2 # ASSIGN : n100 2 # ASSIGN : n101 1 # ASSIGN : n102 5 # ASSIGN : n103 5 # ASSIGN : n104 2 # ASSIGN : n105 5 # ASSIGN : n106 4 # ASSIGN : n107 1 # ASSIGN : n108 1 # ASSIGN : n109 2 # ASSIGN : n110 3 # ASSIGN : n111 4 # ASSIGN : n112 3 # ASSIGN : n113 5 # ASSIGN : n114 1 # ASSIGN : n115 4 # ASSIGN : n116 3 # ASSIGN : n117 1 # ASSIGN : n118 5 # ASSIGN : n119 2 # ASSIGN : n120 5 # ASSIGN : n121 4 # ASSIGN : n122 5 # ASSIGN : n123 2 # ASSIGN : n124 4 # ASSIGN : n125 4 SHOW_RESULT 5 END : 5 (0 seconds) [Thu Jul 6 19:02:59 2006] SHOW_RESULT 5 CPU : 0 = 0 + 0 + 0 + 0 # BOUND : color 2 5 MODIFY_CNF 3 BEGIN : [Thu Jul 6 19:02:59 2006] MODIFY_CNF 3 END : 235518 bytes (0 seconds) [Thu Jul 6 19:02:59 2006] MODIFY_CNF 3 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 3 BEGIN : [Thu Jul 6 19:02:59 2006] CMD : minisat /tmp/csp2sat24433.cnf /tmp/csp2sat24433.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 6531 20204 | 2177 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 16 (800 /sec) decisions : 18 (900 /sec) propagations : 3597 (179850 /sec) conflict literals : 35 (22.22 % deleted) Memory used : 1.58 MB CPU time : 0.02 s UNSATISFIABLE VERIFY_CNF 3 END : (0 seconds) [Thu Jul 6 19:02:59 2006] VERIFY_CNF 3 CPU : 0.02 = 0 + 0 + 0.02 + 0 # RESULT : color 3 UNSATISFIABLE # BOUND : color 4 5 MODIFY_CNF 4 BEGIN : [Thu Jul 6 19:02:59 2006] MODIFY_CNF 4 END : 235518 bytes (0 seconds) [Thu Jul 6 19:02:59 2006] MODIFY_CNF 4 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 4 BEGIN : [Thu Jul 6 19:02:59 2006] CMD : minisat /tmp/csp2sat24433.cnf /tmp/csp2sat24433.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 8003 24620 | 2667 0 0 nan | 0.000 % | | 100 | 8006 24620 | 2933 97 532 5.5 | 32.271 % | ============================================================================== restarts : 2 conflicts : 122 (4067 /sec) decisions : 154 (5133 /sec) propagations : 17098 (569933 /sec) conflict literals : 600 (10.85 % deleted) Memory used : 1.60 MB CPU time : 0.03 s UNSATISFIABLE VERIFY_CNF 4 END : (0 seconds) [Thu Jul 6 19:02:59 2006] VERIFY_CNF 4 CPU : 0.04 = 0 + 0.01 + 0.03 + 0 # RESULT : color 4 UNSATISFIABLE # BOUND : color 5 5 MAIN END : (2 seconds) [Thu Jul 6 19:02:59 2006] MAIN CPU : 2.11 = 1.97 + 0.03 + 0.1 + 0.01