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--
```     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
```