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