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