# TIMEOUT 7200 MAIN BEGIN : [Thu Jul 6 14:32:22 2006] READ BEGIN : csp/david.csp [Thu Jul 6 14:32:22 2006] READ END : csp/david.csp (1 seconds) [Thu Jul 6 14:32:23 2006] READ CPU : 0.72 = 0.7 + 0.02 + 0 + 0 # BOUND : color 2 12 GENERATE_CNF 12 BEGIN : [Thu Jul 6 14:32:23 2006] GENERATE_CNF 12 END : 2042 variables 12338 clauses 199702 bytes (1 seconds) [Thu Jul 6 14:32:24 2006] GENERATE_CNF 12 CPU : 0.58 = 0.57 + 0.01 + 0 + 0 MODIFY_CNF 7 BEGIN : [Thu Jul 6 14:32:24 2006] MODIFY_CNF 7 END : 199706 bytes (0 seconds) [Thu Jul 6 14:32:24 2006] MODIFY_CNF 7 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 7 BEGIN : [Thu Jul 6 14:32:24 2006] CMD : minisat /tmp/csp2sat19124.cnf /tmp/csp2sat19124.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 7751 23220 | 2583 0 0 nan | 0.000 % | | 100 | 7751 23220 | 2841 100 854 8.5 | 34.427 % | | 251 | 7751 23220 | 3125 251 1790 7.1 | 34.427 % | | 476 | 7751 23220 | 3437 476 3026 6.4 | 34.427 % | | 813 | 7754 23220 | 3781 810 4909 6.1 | 34.428 % | | 1320 | 7630 22848 | 4159 945 5434 5.8 | 34.623 % | ============================================================================== restarts : 6 conflicts : 1403 (28060 /sec) decisions : 1897 (37940 /sec) propagations : 71707 (1434140 /sec) conflict literals : 7928 (9.25 % deleted) Memory used : 1.44 MB CPU time : 0.05 s UNSATISFIABLE VERIFY_CNF 7 END : (0 seconds) [Thu Jul 6 14:32:24 2006] VERIFY_CNF 7 CPU : 0.05 = 0 + 0 + 0.05 + 0 # RESULT : color 7 UNSATISFIABLE # BOUND : color 8 12 MODIFY_CNF 10 BEGIN : [Thu Jul 6 14:32:24 2006] MODIFY_CNF 10 END : 199707 bytes (0 seconds) [Thu Jul 6 14:32:24 2006] MODIFY_CNF 10 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 10 BEGIN : [Thu Jul 6 14:32:24 2006] CMD : minisat /tmp/csp2sat19124.cnf /tmp/csp2sat19124.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 10187 30528 | 3395 0 0 nan | 0.000 % | | 100 | 10187 30528 | 3734 100 1273 12.7 | 21.499 % | | 250 | 10187 30528 | 4107 250 2201 8.8 | 21.499 % | | 475 | 10187 30528 | 4518 475 4052 8.5 | 21.499 % | | 812 | 10187 30528 | 4970 812 6749 8.3 | 21.499 % | | 1318 | 10187 30528 | 5467 1318 11199 8.5 | 21.499 % | | 2077 | 10187 30528 | 6014 2077 17573 8.5 | 21.499 % | | 3217 | 10187 30528 | 6615 3217 29218 9.1 | 21.500 % | | 4927 | 10187 30528 | 7277 4927 48310 9.8 | 21.499 % | | 7491 | 10187 30528 | 8005 7491 73471 9.8 | 21.499 % | | 11335 | 10187 30528 | 8805 7030 71806 10.2 | 21.499 % | | 17101 | 10170 30480 | 9686 7797 82719 10.6 | 21.548 % | | 25752 | 10157 30444 | 10654 6227 63788 10.2 | 21.597 % | | 38728 | 10086 30324 | 11720 6105 55021 9.0 | 21.793 % | ============================================================================== restarts : 14 conflicts : 43702 (11036 /sec) decisions : 52996 (13383 /sec) propagations : 1970233 (497534 /sec) conflict literals : 439120 (7.03 % deleted) Memory used : 2.45 MB CPU time : 3.96 s UNSATISFIABLE VERIFY_CNF 10 END : (4 seconds) [Thu Jul 6 14:32:28 2006] VERIFY_CNF 10 CPU : 3.97 = 0 + 0 + 3.96 + 0.01 # RESULT : color 10 UNSATISFIABLE # BOUND : color 11 12 MODIFY_CNF 11 BEGIN : [Thu Jul 6 14:32:28 2006] MODIFY_CNF 11 END : 199707 bytes (0 seconds) [Thu Jul 6 14:32:28 2006] MODIFY_CNF 11 CPU : 0 = 0 + 0 + 0 + 0 VERIFY_CNF 11 BEGIN : [Thu Jul 6 14:32:28 2006] CMD : minisat /tmp/csp2sat19124.cnf /tmp/csp2sat19124.out ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 10999 32964 | 3666 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 0 (0 /sec) decisions : 293 (29300 /sec) propagations : 2042 (204200 /sec) conflict literals : 0 ( nan % deleted) Memory used : 1.43 MB CPU time : 0.01 s SATISFIABLE VERIFY_CNF 11 END : (0 seconds) [Thu Jul 6 14:32:28 2006] VERIFY_CNF 11 CPU : 0.0299999999999998 = 0 + 0.01 + 0.00999999999999979 + 0.01 # RESULT : color 11 SATISFIABLE SHOW_RESULT 11 BEGIN : [Thu Jul 6 14:32:28 2006] # ASSIGN : color 11 # ASSIGN : n1 4 # ASSIGN : n2 10 # ASSIGN : n3 3 # ASSIGN : n4 8 # ASSIGN : n5 7 # ASSIGN : n6 7 # ASSIGN : n7 1 # ASSIGN : n8 1 # ASSIGN : n9 4 # ASSIGN : n10 1 # ASSIGN : n11 5 # ASSIGN : n12 5 # ASSIGN : n13 1 # ASSIGN : n14 11 # ASSIGN : n15 1 # ASSIGN : n16 4 # ASSIGN : n17 1 # ASSIGN : n18 1 # ASSIGN : n19 6 # ASSIGN : n20 6 # ASSIGN : n21 4 # ASSIGN : n22 1 # ASSIGN : n23 2 # ASSIGN : n24 7 # ASSIGN : n25 8 # ASSIGN : n26 8 # ASSIGN : n27 2 # ASSIGN : n28 2 # ASSIGN : n29 3 # ASSIGN : n30 3 # ASSIGN : n31 1 # ASSIGN : n32 1 # ASSIGN : n33 4 # ASSIGN : n34 2 # ASSIGN : n35 4 # ASSIGN : n36 2 # ASSIGN : n37 2 # ASSIGN : n38 8 # ASSIGN : n39 4 # ASSIGN : n40 6 # ASSIGN : n41 8 # ASSIGN : n42 2 # ASSIGN : n43 3 # ASSIGN : n44 6 # ASSIGN : n45 3 # ASSIGN : n46 3 # ASSIGN : n47 8 # ASSIGN : n48 8 # ASSIGN : n49 2 # ASSIGN : n50 4 # ASSIGN : n51 3 # ASSIGN : n52 3 # ASSIGN : n53 4 # ASSIGN : n54 5 # ASSIGN : n55 4 # ASSIGN : n56 8 # ASSIGN : n57 8 # ASSIGN : n58 5 # ASSIGN : n59 7 # ASSIGN : n60 10 # ASSIGN : n61 8 # ASSIGN : n62 8 # ASSIGN : n63 7 # ASSIGN : n64 8 # ASSIGN : n65 8 # ASSIGN : n66 5 # ASSIGN : n67 6 # ASSIGN : n68 4 # ASSIGN : n69 7 # ASSIGN : n70 6 # ASSIGN : n71 8 # ASSIGN : n72 8 # ASSIGN : n73 8 # ASSIGN : n74 7 # ASSIGN : n75 8 # ASSIGN : n76 7 # ASSIGN : n77 8 # ASSIGN : n78 8 # ASSIGN : n79 7 # ASSIGN : n80 8 # ASSIGN : n81 8 # ASSIGN : n82 8 # ASSIGN : n83 9 # ASSIGN : n84 10 # ASSIGN : n85 11 # ASSIGN : n86 11 # ASSIGN : n87 11 SHOW_RESULT 11 END : 11 (0 seconds) [Thu Jul 6 14:32:28 2006] SHOW_RESULT 11 CPU : 0.01 = 0 + 0.01 + 0 + 0 # BOUND : color 11 11 MAIN END : (6 seconds) [Thu Jul 6 14:32:28 2006] MAIN CPU : 5.36 = 1.27 + 0.05 + 4.02 + 0.02