src/HOL/ex/SAT_Examples.thy
author nipkow
Fri Mar 06 17:38:47 2009 +0100 (2009-03-06)
changeset 30313 b2441b0c8d38
parent 23609 451ab1a20ac3
child 30510 4120fc59dd85
permissions -rw-r--r--
added lemmas
     1 (*  Title:      HOL/ex/SAT_Examples.thy
     2     ID:         $Id$
     3     Author:     Alwen Tiu, Tjark Weber
     4     Copyright   2005-2006
     5 *)
     6 
     7 header {* Examples for the 'sat' and 'satx' tactic *}
     8 
     9 theory SAT_Examples imports Main
    10 
    11 begin
    12 
    13 (* ML {* sat.solver := "zchaff_with_proofs"; *} *)
    14 (* ML {* sat.solver := "minisat_with_proofs"; *} *)
    15 ML {* set sat.trace_sat; *}
    16 ML {* set quick_and_dirty; *}
    17 
    18 lemma "True"
    19 by sat
    20 
    21 lemma "a | ~a"
    22 by sat
    23 
    24 lemma "(a | b) & ~a \<Longrightarrow> b"
    25 by sat
    26 
    27 lemma "(a & b) | (c & d) \<Longrightarrow> (a & b) | (c & d)"
    28 (*
    29 apply (tactic {* cnf.cnf_rewrite_tac 1 *})
    30 *)
    31 by sat
    32 
    33 lemma "(a & b) | (c & d) \<Longrightarrow> (a & b) | (c & d)"
    34 (*
    35 apply (tactic {* cnf.cnfx_rewrite_tac 1 *})
    36 apply (erule exE | erule conjE)+
    37 *)
    38 by satx
    39 
    40 lemma "(a & b | c & d) & (e & f | g & h) | (i & j | k & l) & (m & n | p & q)
    41   \<Longrightarrow> (a & b | c & d) & (e & f | g & h) | (i & j | k & l) & (m & n | p & q)"
    42 (*
    43 apply (tactic {* cnf.cnf_rewrite_tac 1 *})
    44 *)
    45 by sat
    46 
    47 lemma "(a & b | c & d) & (e & f | g & h) | (i & j | k & l) & (m & n | p & q)
    48   \<Longrightarrow> (a & b | c & d) & (e & f | g & h) | (i & j | k & l) & (m & n | p & q)"
    49 (*
    50 apply (tactic {* cnf.cnfx_rewrite_tac 1 *})
    51 apply (erule exE | erule conjE)+
    52 *)
    53 by satx
    54 
    55 lemma "P=P=P=P=P=P=P=P=P=P"
    56 by sat
    57 
    58 lemma "P=P=P=P=P=P=P=P=P=P"
    59 by satx
    60 
    61 lemma  "!! a b c. [| a | b | c | d ;
    62 e | f | (a & d) ;
    63 ~(a | (c & ~c)) | b ;
    64 ~(b & (x | ~x)) | c ;
    65 ~(d | False) | c ;
    66 ~(c | (~p & (p | (q & ~q)))) |] ==> False"
    67 by sat
    68 
    69 lemma  "!! a b c. [| a | b | c | d ;
    70 e | f | (a & d) ;
    71 ~(a | (c & ~c)) | b ;
    72 ~(b & (x | ~x)) | c ;
    73 ~(d | False) | c ;
    74 ~(c | (~p & (p | (q & ~q)))) |] ==> False"
    75 by satx
    76 
    77 text {* eta-Equivalence *}
    78 
    79 lemma "(ALL x. P x) | ~ All P"
    80 by sat
    81 
    82 ML {* reset sat.trace_sat; *}
    83 ML {* reset quick_and_dirty; *}
    84 
    85 method_setup rawsat =
    86   {* Method.no_args (Method.SIMPLE_METHOD' sat.rawsat_tac) *}
    87   "SAT solver (no preprocessing)"
    88 
    89 (* ML {* Toplevel.profiling := 1; *} *)
    90 
    91 (* Translated from TPTP problem library: PUZ015-2.006.dimacs *)
    92 
    93 lemma assumes 1: "~x0"
    94 and 2: "~x30"
    95 and 3: "~x29"
    96 and 4: "~x59"
    97 and 5: "x1 | x31 | x0"
    98 and 6: "x2 | x32 | x1"
    99 and 7: "x3 | x33 | x2"
   100 and 8: "x4 | x34 | x3"
   101 and 9: "x35 | x4"
   102 and 10: "x5 | x36 | x30"
   103 and 11: "x6 | x37 | x5 | x31"
   104 and 12: "x7 | x38 | x6 | x32"
   105 and 13: "x8 | x39 | x7 | x33"
   106 and 14: "x9 | x40 | x8 | x34"
   107 and 15: "x41 | x9 | x35"
   108 and 16: "x10 | x42 | x36"
   109 and 17: "x11 | x43 | x10 | x37"
   110 and 18: "x12 | x44 | x11 | x38"
   111 and 19: "x13 | x45 | x12 | x39"
   112 and 20: "x14 | x46 | x13 | x40"
   113 and 21: "x47 | x14 | x41"
   114 and 22: "x15 | x48 | x42"
   115 and 23: "x16 | x49 | x15 | x43"
   116 and 24: "x17 | x50 | x16 | x44"
   117 and 25: "x18 | x51 | x17 | x45"
   118 and 26: "x19 | x52 | x18 | x46"
   119 and 27: "x53 | x19 | x47"
   120 and 28: "x20 | x54 | x48"
   121 and 29: "x21 | x55 | x20 | x49"
   122 and 30: "x22 | x56 | x21 | x50"
   123 and 31: "x23 | x57 | x22 | x51"
   124 and 32: "x24 | x58 | x23 | x52"
   125 and 33: "x59 | x24 | x53"
   126 and 34: "x25 | x54"
   127 and 35: "x26 | x25 | x55"
   128 and 36: "x27 | x26 | x56"
   129 and 37: "x28 | x27 | x57"
   130 and 38: "x29 | x28 | x58"
   131 and 39: "~x1 | ~x31"
   132 and 40: "~x1 | ~x0"
   133 and 41: "~x31 | ~x0"
   134 and 42: "~x2 | ~x32"
   135 and 43: "~x2 | ~x1"
   136 and 44: "~x32 | ~x1"
   137 and 45: "~x3 | ~x33"
   138 and 46: "~x3 | ~x2"
   139 and 47: "~x33 | ~x2"
   140 and 48: "~x4 | ~x34"
   141 and 49: "~x4 | ~x3"
   142 and 50: "~x34 | ~x3"
   143 and 51: "~x35 | ~x4"
   144 and 52: "~x5 | ~x36"
   145 and 53: "~x5 | ~x30"
   146 and 54: "~x36 | ~x30"
   147 and 55: "~x6 | ~x37"
   148 and 56: "~x6 | ~x5"
   149 and 57: "~x6 | ~x31"
   150 and 58: "~x37 | ~x5"
   151 and 59: "~x37 | ~x31"
   152 and 60: "~x5 | ~x31"
   153 and 61: "~x7 | ~x38"
   154 and 62: "~x7 | ~x6"
   155 and 63: "~x7 | ~x32"
   156 and 64: "~x38 | ~x6"
   157 and 65: "~x38 | ~x32"
   158 and 66: "~x6 | ~x32"
   159 and 67: "~x8 | ~x39"
   160 and 68: "~x8 | ~x7"
   161 and 69: "~x8 | ~x33"
   162 and 70: "~x39 | ~x7"
   163 and 71: "~x39 | ~x33"
   164 and 72: "~x7 | ~x33"
   165 and 73: "~x9 | ~x40"
   166 and 74: "~x9 | ~x8"
   167 and 75: "~x9 | ~x34"
   168 and 76: "~x40 | ~x8"
   169 and 77: "~x40 | ~x34"
   170 and 78: "~x8 | ~x34"
   171 and 79: "~x41 | ~x9"
   172 and 80: "~x41 | ~x35"
   173 and 81: "~x9 | ~x35"
   174 and 82: "~x10 | ~x42"
   175 and 83: "~x10 | ~x36"
   176 and 84: "~x42 | ~x36"
   177 and 85: "~x11 | ~x43"
   178 and 86: "~x11 | ~x10"
   179 and 87: "~x11 | ~x37"
   180 and 88: "~x43 | ~x10"
   181 and 89: "~x43 | ~x37"
   182 and 90: "~x10 | ~x37"
   183 and 91: "~x12 | ~x44"
   184 and 92: "~x12 | ~x11"
   185 and 93: "~x12 | ~x38"
   186 and 94: "~x44 | ~x11"
   187 and 95: "~x44 | ~x38"
   188 and 96: "~x11 | ~x38"
   189 and 97: "~x13 | ~x45"
   190 and 98: "~x13 | ~x12"
   191 and 99: "~x13 | ~x39"
   192 and 100: "~x45 | ~x12"
   193 and 101: "~x45 | ~x39"
   194 and 102: "~x12 | ~x39"
   195 and 103: "~x14 | ~x46"
   196 and 104: "~x14 | ~x13"
   197 and 105: "~x14 | ~x40"
   198 and 106: "~x46 | ~x13"
   199 and 107: "~x46 | ~x40"
   200 and 108: "~x13 | ~x40"
   201 and 109: "~x47 | ~x14"
   202 and 110: "~x47 | ~x41"
   203 and 111: "~x14 | ~x41"
   204 and 112: "~x15 | ~x48"
   205 and 113: "~x15 | ~x42"
   206 and 114: "~x48 | ~x42"
   207 and 115: "~x16 | ~x49"
   208 and 116: "~x16 | ~x15"
   209 and 117: "~x16 | ~x43"
   210 and 118: "~x49 | ~x15"
   211 and 119: "~x49 | ~x43"
   212 and 120: "~x15 | ~x43"
   213 and 121: "~x17 | ~x50"
   214 and 122: "~x17 | ~x16"
   215 and 123: "~x17 | ~x44"
   216 and 124: "~x50 | ~x16"
   217 and 125: "~x50 | ~x44"
   218 and 126: "~x16 | ~x44"
   219 and 127: "~x18 | ~x51"
   220 and 128: "~x18 | ~x17"
   221 and 129: "~x18 | ~x45"
   222 and 130: "~x51 | ~x17"
   223 and 131: "~x51 | ~x45"
   224 and 132: "~x17 | ~x45"
   225 and 133: "~x19 | ~x52"
   226 and 134: "~x19 | ~x18"
   227 and 135: "~x19 | ~x46"
   228 and 136: "~x52 | ~x18"
   229 and 137: "~x52 | ~x46"
   230 and 138: "~x18 | ~x46"
   231 and 139: "~x53 | ~x19"
   232 and 140: "~x53 | ~x47"
   233 and 141: "~x19 | ~x47"
   234 and 142: "~x20 | ~x54"
   235 and 143: "~x20 | ~x48"
   236 and 144: "~x54 | ~x48"
   237 and 145: "~x21 | ~x55"
   238 and 146: "~x21 | ~x20"
   239 and 147: "~x21 | ~x49"
   240 and 148: "~x55 | ~x20"
   241 and 149: "~x55 | ~x49"
   242 and 150: "~x20 | ~x49"
   243 and 151: "~x22 | ~x56"
   244 and 152: "~x22 | ~x21"
   245 and 153: "~x22 | ~x50"
   246 and 154: "~x56 | ~x21"
   247 and 155: "~x56 | ~x50"
   248 and 156: "~x21 | ~x50"
   249 and 157: "~x23 | ~x57"
   250 and 158: "~x23 | ~x22"
   251 and 159: "~x23 | ~x51"
   252 and 160: "~x57 | ~x22"
   253 and 161: "~x57 | ~x51"
   254 and 162: "~x22 | ~x51"
   255 and 163: "~x24 | ~x58"
   256 and 164: "~x24 | ~x23"
   257 and 165: "~x24 | ~x52"
   258 and 166: "~x58 | ~x23"
   259 and 167: "~x58 | ~x52"
   260 and 168: "~x23 | ~x52"
   261 and 169: "~x59 | ~x24"
   262 and 170: "~x59 | ~x53"
   263 and 171: "~x24 | ~x53"
   264 and 172: "~x25 | ~x54"
   265 and 173: "~x26 | ~x25"
   266 and 174: "~x26 | ~x55"
   267 and 175: "~x25 | ~x55"
   268 and 176: "~x27 | ~x26"
   269 and 177: "~x27 | ~x56"
   270 and 178: "~x26 | ~x56"
   271 and 179: "~x28 | ~x27"
   272 and 180: "~x28 | ~x57"
   273 and 181: "~x27 | ~x57"
   274 and 182: "~x29 | ~x28"
   275 and 183: "~x29 | ~x58"
   276 and 184: "~x28 | ~x58"
   277 shows "False"
   278 using 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19
   279 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39
   280 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59
   281 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79
   282 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99
   283 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119
   284 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139
   285 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159
   286 160 161 162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179
   287 180 181 182 183 184
   288 (*
   289 by sat
   290 *)
   291 by rawsat  -- {* this is without CNF conversion *}
   292 
   293 (* Translated from TPTP problem library: MSC007-1.008.dimacs *)
   294 
   295 lemma assumes 1: "x0 | x1 | x2 | x3 | x4 | x5 | x6"
   296 and 2: "x7 | x8 | x9 | x10 | x11 | x12 | x13"
   297 and 3: "x14 | x15 | x16 | x17 | x18 | x19 | x20"
   298 and 4: "x21 | x22 | x23 | x24 | x25 | x26 | x27"
   299 and 5: "x28 | x29 | x30 | x31 | x32 | x33 | x34"
   300 and 6: "x35 | x36 | x37 | x38 | x39 | x40 | x41"
   301 and 7: "x42 | x43 | x44 | x45 | x46 | x47 | x48"
   302 and 8: "x49 | x50 | x51 | x52 | x53 | x54 | x55"
   303 and 9: "~x0 | ~x7"
   304 and 10: "~x0 | ~x14"
   305 and 11: "~x0 | ~x21"
   306 and 12: "~x0 | ~x28"
   307 and 13: "~x0 | ~x35"
   308 and 14: "~x0 | ~x42"
   309 and 15: "~x0 | ~x49"
   310 and 16: "~x7 | ~x14"
   311 and 17: "~x7 | ~x21"
   312 and 18: "~x7 | ~x28"
   313 and 19: "~x7 | ~x35"
   314 and 20: "~x7 | ~x42"
   315 and 21: "~x7 | ~x49"
   316 and 22: "~x14 | ~x21"
   317 and 23: "~x14 | ~x28"
   318 and 24: "~x14 | ~x35"
   319 and 25: "~x14 | ~x42"
   320 and 26: "~x14 | ~x49"
   321 and 27: "~x21 | ~x28"
   322 and 28: "~x21 | ~x35"
   323 and 29: "~x21 | ~x42"
   324 and 30: "~x21 | ~x49"
   325 and 31: "~x28 | ~x35"
   326 and 32: "~x28 | ~x42"
   327 and 33: "~x28 | ~x49"
   328 and 34: "~x35 | ~x42"
   329 and 35: "~x35 | ~x49"
   330 and 36: "~x42 | ~x49"
   331 and 37: "~x1 | ~x8"
   332 and 38: "~x1 | ~x15"
   333 and 39: "~x1 | ~x22"
   334 and 40: "~x1 | ~x29"
   335 and 41: "~x1 | ~x36"
   336 and 42: "~x1 | ~x43"
   337 and 43: "~x1 | ~x50"
   338 and 44: "~x8 | ~x15"
   339 and 45: "~x8 | ~x22"
   340 and 46: "~x8 | ~x29"
   341 and 47: "~x8 | ~x36"
   342 and 48: "~x8 | ~x43"
   343 and 49: "~x8 | ~x50"
   344 and 50: "~x15 | ~x22"
   345 and 51: "~x15 | ~x29"
   346 and 52: "~x15 | ~x36"
   347 and 53: "~x15 | ~x43"
   348 and 54: "~x15 | ~x50"
   349 and 55: "~x22 | ~x29"
   350 and 56: "~x22 | ~x36"
   351 and 57: "~x22 | ~x43"
   352 and 58: "~x22 | ~x50"
   353 and 59: "~x29 | ~x36"
   354 and 60: "~x29 | ~x43"
   355 and 61: "~x29 | ~x50"
   356 and 62: "~x36 | ~x43"
   357 and 63: "~x36 | ~x50"
   358 and 64: "~x43 | ~x50"
   359 and 65: "~x2 | ~x9"
   360 and 66: "~x2 | ~x16"
   361 and 67: "~x2 | ~x23"
   362 and 68: "~x2 | ~x30"
   363 and 69: "~x2 | ~x37"
   364 and 70: "~x2 | ~x44"
   365 and 71: "~x2 | ~x51"
   366 and 72: "~x9 | ~x16"
   367 and 73: "~x9 | ~x23"
   368 and 74: "~x9 | ~x30"
   369 and 75: "~x9 | ~x37"
   370 and 76: "~x9 | ~x44"
   371 and 77: "~x9 | ~x51"
   372 and 78: "~x16 | ~x23"
   373 and 79: "~x16 | ~x30"
   374 and 80: "~x16 | ~x37"
   375 and 81: "~x16 | ~x44"
   376 and 82: "~x16 | ~x51"
   377 and 83: "~x23 | ~x30"
   378 and 84: "~x23 | ~x37"
   379 and 85: "~x23 | ~x44"
   380 and 86: "~x23 | ~x51"
   381 and 87: "~x30 | ~x37"
   382 and 88: "~x30 | ~x44"
   383 and 89: "~x30 | ~x51"
   384 and 90: "~x37 | ~x44"
   385 and 91: "~x37 | ~x51"
   386 and 92: "~x44 | ~x51"
   387 and 93: "~x3 | ~x10"
   388 and 94: "~x3 | ~x17"
   389 and 95: "~x3 | ~x24"
   390 and 96: "~x3 | ~x31"
   391 and 97: "~x3 | ~x38"
   392 and 98: "~x3 | ~x45"
   393 and 99: "~x3 | ~x52"
   394 and 100: "~x10 | ~x17"
   395 and 101: "~x10 | ~x24"
   396 and 102: "~x10 | ~x31"
   397 and 103: "~x10 | ~x38"
   398 and 104: "~x10 | ~x45"
   399 and 105: "~x10 | ~x52"
   400 and 106: "~x17 | ~x24"
   401 and 107: "~x17 | ~x31"
   402 and 108: "~x17 | ~x38"
   403 and 109: "~x17 | ~x45"
   404 and 110: "~x17 | ~x52"
   405 and 111: "~x24 | ~x31"
   406 and 112: "~x24 | ~x38"
   407 and 113: "~x24 | ~x45"
   408 and 114: "~x24 | ~x52"
   409 and 115: "~x31 | ~x38"
   410 and 116: "~x31 | ~x45"
   411 and 117: "~x31 | ~x52"
   412 and 118: "~x38 | ~x45"
   413 and 119: "~x38 | ~x52"
   414 and 120: "~x45 | ~x52"
   415 and 121: "~x4 | ~x11"
   416 and 122: "~x4 | ~x18"
   417 and 123: "~x4 | ~x25"
   418 and 124: "~x4 | ~x32"
   419 and 125: "~x4 | ~x39"
   420 and 126: "~x4 | ~x46"
   421 and 127: "~x4 | ~x53"
   422 and 128: "~x11 | ~x18"
   423 and 129: "~x11 | ~x25"
   424 and 130: "~x11 | ~x32"
   425 and 131: "~x11 | ~x39"
   426 and 132: "~x11 | ~x46"
   427 and 133: "~x11 | ~x53"
   428 and 134: "~x18 | ~x25"
   429 and 135: "~x18 | ~x32"
   430 and 136: "~x18 | ~x39"
   431 and 137: "~x18 | ~x46"
   432 and 138: "~x18 | ~x53"
   433 and 139: "~x25 | ~x32"
   434 and 140: "~x25 | ~x39"
   435 and 141: "~x25 | ~x46"
   436 and 142: "~x25 | ~x53"
   437 and 143: "~x32 | ~x39"
   438 and 144: "~x32 | ~x46"
   439 and 145: "~x32 | ~x53"
   440 and 146: "~x39 | ~x46"
   441 and 147: "~x39 | ~x53"
   442 and 148: "~x46 | ~x53"
   443 and 149: "~x5 | ~x12"
   444 and 150: "~x5 | ~x19"
   445 and 151: "~x5 | ~x26"
   446 and 152: "~x5 | ~x33"
   447 and 153: "~x5 | ~x40"
   448 and 154: "~x5 | ~x47"
   449 and 155: "~x5 | ~x54"
   450 and 156: "~x12 | ~x19"
   451 and 157: "~x12 | ~x26"
   452 and 158: "~x12 | ~x33"
   453 and 159: "~x12 | ~x40"
   454 and 160: "~x12 | ~x47"
   455 and 161: "~x12 | ~x54"
   456 and 162: "~x19 | ~x26"
   457 and 163: "~x19 | ~x33"
   458 and 164: "~x19 | ~x40"
   459 and 165: "~x19 | ~x47"
   460 and 166: "~x19 | ~x54"
   461 and 167: "~x26 | ~x33"
   462 and 168: "~x26 | ~x40"
   463 and 169: "~x26 | ~x47"
   464 and 170: "~x26 | ~x54"
   465 and 171: "~x33 | ~x40"
   466 and 172: "~x33 | ~x47"
   467 and 173: "~x33 | ~x54"
   468 and 174: "~x40 | ~x47"
   469 and 175: "~x40 | ~x54"
   470 and 176: "~x47 | ~x54"
   471 and 177: "~x6 | ~x13"
   472 and 178: "~x6 | ~x20"
   473 and 179: "~x6 | ~x27"
   474 and 180: "~x6 | ~x34"
   475 and 181: "~x6 | ~x41"
   476 and 182: "~x6 | ~x48"
   477 and 183: "~x6 | ~x55"
   478 and 184: "~x13 | ~x20"
   479 and 185: "~x13 | ~x27"
   480 and 186: "~x13 | ~x34"
   481 and 187: "~x13 | ~x41"
   482 and 188: "~x13 | ~x48"
   483 and 189: "~x13 | ~x55"
   484 and 190: "~x20 | ~x27"
   485 and 191: "~x20 | ~x34"
   486 and 192: "~x20 | ~x41"
   487 and 193: "~x20 | ~x48"
   488 and 194: "~x20 | ~x55"
   489 and 195: "~x27 | ~x34"
   490 and 196: "~x27 | ~x41"
   491 and 197: "~x27 | ~x48"
   492 and 198: "~x27 | ~x55"
   493 and 199: "~x34 | ~x41"
   494 and 200: "~x34 | ~x48"
   495 and 201: "~x34 | ~x55"
   496 and 202: "~x41 | ~x48"
   497 and 203: "~x41 | ~x55"
   498 and 204: "~x48 | ~x55"
   499 shows "False"
   500 using 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19
   501 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39
   502 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59
   503 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79
   504 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99
   505 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119
   506 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139
   507 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159
   508 160 161 162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179
   509 180 181 182 183 184 185 186 187 188 189 190 191 192 193 194 195 196 197 198 199
   510 200 201 202 203 204
   511 (*
   512 by sat
   513 *)
   514 by rawsat  -- {* this is without CNF conversion *}
   515 
   516 (* Old sequent clause representation ("[c_i, p, ~q, \<dots>] \<turnstile> False"):
   517    sat, zchaff_with_proofs: 8705 resolution steps in
   518                             +++ User 1.154  All 1.189 secs
   519    sat, minisat_with_proofs: 40790 resolution steps in
   520                              +++ User 3.762  All 3.806 secs
   521 
   522    rawsat, zchaff_with_proofs: 8705 resolution steps in
   523                                +++ User 0.731  All 0.751 secs
   524    rawsat, minisat_with_proofs: 40790 resolution steps in
   525                                 +++ User 3.514  All 3.550 secs
   526 
   527    CNF clause representation ("[c_1 && \<dots> && c_n, p, ~q, \<dots>] \<turnstile> False"):
   528    rawsat, zchaff_with_proofs: 8705 resolution steps in
   529                                +++ User 0.653  All 0.670 secs
   530    rawsat, minisat_with_proofs: 40790 resolution steps in
   531                                 +++ User 1.860  All 1.886 secs
   532 
   533    (as of 2006-08-30, on a 2.5 GHz Pentium 4)
   534 *)
   535 
   536 (* ML {* Toplevel.profiling := 0; *} *)
   537 
   538 end