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