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