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