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