src/HOL/ex/SAT_Examples.thy
author webertj
Fri, 23 Sep 2005 22:58:50 +0200
changeset 17618 1330157e156a
child 17622 5d03a69481b6
permissions -rw-r--r--
new sat tactic imports resolution proofs from zChaff
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
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
     7
header {* Examples for the 'sat' command *}
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
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
    13
(* Translated from TPTP problem library: PUZ015-2.006.dimacs *)
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
    14
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
    15
lemma assumes 1: "~x0"
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
    16
and 2: "~x30"
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
    17
and 3: "~x29"
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
    18
and 4: "~x59"
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
    19
and 5: "x1 | x31 | x0"
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
    20
and 6: "x2 | x32 | x1"
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
    21
and 7: "x3 | x33 | x2"
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
    22
and 8: "x4 | x34 | x3"
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
    23
and 9: "x35 | x4"
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
    24
and 10: "x5 | x36 | x30"
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
    25
and 11: "x6 | x37 | x5 | x31"
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
    26
and 12: "x7 | x38 | x6 | x32"
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
    27
and 13: "x8 | x39 | x7 | x33"
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
    28
and 14: "x9 | x40 | x8 | x34"
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
    29
and 15: "x41 | x9 | x35"
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
    30
and 16: "x10 | x42 | x36"
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
    31
and 17: "x11 | x43 | x10 | x37"
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
    32
and 18: "x12 | x44 | x11 | x38"
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
    33
and 19: "x13 | x45 | x12 | x39"
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
    34
and 20: "x14 | x46 | x13 | x40"
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
    35
and 21: "x47 | x14 | x41"
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
    36
and 22: "x15 | x48 | x42"
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
    37
and 23: "x16 | x49 | x15 | x43"
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
    38
and 24: "x17 | x50 | x16 | x44"
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
    39
and 25: "x18 | x51 | x17 | x45"
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
    40
and 26: "x19 | x52 | x18 | x46"
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
    41
and 27: "x53 | x19 | x47"
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
    42
and 28: "x20 | x54 | x48"
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
    43
and 29: "x21 | x55 | x20 | x49"
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
    44
and 30: "x22 | x56 | x21 | x50"
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
    45
and 31: "x23 | x57 | x22 | x51"
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
    46
and 32: "x24 | x58 | x23 | x52"
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
    47
and 33: "x59 | x24 | x53"
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
    48
and 34: "x25 | x54"
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
    49
and 35: "x26 | x25 | x55"
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
    50
and 36: "x27 | x26 | x56"
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
    51
and 37: "x28 | x27 | x57"
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
    52
and 38: "x29 | x28 | x58"
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
    53
and 39: "~x1 | ~x31"
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
    54
and 40: "~x1 | ~x0"
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
    55
and 41: "~x31 | ~x0"
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
    56
and 42: "~x2 | ~x32"
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
    57
and 43: "~x2 | ~x1"
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
    58
and 44: "~x32 | ~x1"
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
    59
and 45: "~x3 | ~x33"
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
    60
and 46: "~x3 | ~x2"
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
    61
and 47: "~x33 | ~x2"
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
    62
and 48: "~x4 | ~x34"
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
    63
and 49: "~x4 | ~x3"
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
    64
and 50: "~x34 | ~x3"
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
    65
and 51: "~x35 | ~x4"
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
    66
and 52: "~x5 | ~x36"
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
    67
and 53: "~x5 | ~x30"
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
    68
and 54: "~x36 | ~x30"
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
    69
and 55: "~x6 | ~x37"
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
    70
and 56: "~x6 | ~x5"
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
    71
and 57: "~x6 | ~x31"
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
    72
and 58: "~x37 | ~x5"
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
    73
and 59: "~x37 | ~x31"
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
    74
and 60: "~x5 | ~x31"
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
    75
and 61: "~x7 | ~x38"
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
    76
and 62: "~x7 | ~x6"
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
    77
and 63: "~x7 | ~x32"
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
    78
and 64: "~x38 | ~x6"
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
    79
and 65: "~x38 | ~x32"
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
    80
and 66: "~x6 | ~x32"
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
    81
and 67: "~x8 | ~x39"
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
    82
and 68: "~x8 | ~x7"
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
    83
and 69: "~x8 | ~x33"
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
    84
and 70: "~x39 | ~x7"
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
    85
and 71: "~x39 | ~x33"
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
    86
and 72: "~x7 | ~x33"
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
    87
and 73: "~x9 | ~x40"
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
    88
and 74: "~x9 | ~x8"
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
    89
and 75: "~x9 | ~x34"
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
    90
and 76: "~x40 | ~x8"
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
    91
and 77: "~x40 | ~x34"
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
    92
and 78: "~x8 | ~x34"
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
    93
and 79: "~x41 | ~x9"
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
    94
and 80: "~x41 | ~x35"
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
    95
and 81: "~x9 | ~x35"
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
    96
and 82: "~x10 | ~x42"
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
    97
and 83: "~x10 | ~x36"
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
    98
and 84: "~x42 | ~x36"
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
    99
and 85: "~x11 | ~x43"
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   100
and 86: "~x11 | ~x10"
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   101
and 87: "~x11 | ~x37"
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   102
and 88: "~x43 | ~x10"
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   103
and 89: "~x43 | ~x37"
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   104
and 90: "~x10 | ~x37"
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   105
and 91: "~x12 | ~x44"
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   106
and 92: "~x12 | ~x11"
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   107
and 93: "~x12 | ~x38"
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   108
and 94: "~x44 | ~x11"
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   109
and 95: "~x44 | ~x38"
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   110
and 96: "~x11 | ~x38"
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   111
and 97: "~x13 | ~x45"
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   112
and 98: "~x13 | ~x12"
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   113
and 99: "~x13 | ~x39"
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   114
and 100: "~x45 | ~x12"
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   115
and 101: "~x45 | ~x39"
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   116
and 102: "~x12 | ~x39"
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   117
and 103: "~x14 | ~x46"
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   118
and 104: "~x14 | ~x13"
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   119
and 105: "~x14 | ~x40"
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   120
and 106: "~x46 | ~x13"
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   121
and 107: "~x46 | ~x40"
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   122
and 108: "~x13 | ~x40"
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   123
and 109: "~x47 | ~x14"
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   124
and 110: "~x47 | ~x41"
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   125
and 111: "~x14 | ~x41"
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   126
and 112: "~x15 | ~x48"
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   127
and 113: "~x15 | ~x42"
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   128
and 114: "~x48 | ~x42"
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   129
and 115: "~x16 | ~x49"
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   130
and 116: "~x16 | ~x15"
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   131
and 117: "~x16 | ~x43"
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   132
and 118: "~x49 | ~x15"
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   133
and 119: "~x49 | ~x43"
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   134
and 120: "~x15 | ~x43"
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   135
and 121: "~x17 | ~x50"
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   136
and 122: "~x17 | ~x16"
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   137
and 123: "~x17 | ~x44"
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   138
and 124: "~x50 | ~x16"
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   139
and 125: "~x50 | ~x44"
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   140
and 126: "~x16 | ~x44"
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   141
and 127: "~x18 | ~x51"
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   142
and 128: "~x18 | ~x17"
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   143
and 129: "~x18 | ~x45"
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   144
and 130: "~x51 | ~x17"
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   145
and 131: "~x51 | ~x45"
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   146
and 132: "~x17 | ~x45"
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   147
and 133: "~x19 | ~x52"
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   148
and 134: "~x19 | ~x18"
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   149
and 135: "~x19 | ~x46"
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   150
and 136: "~x52 | ~x18"
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   151
and 137: "~x52 | ~x46"
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   152
and 138: "~x18 | ~x46"
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   153
and 139: "~x53 | ~x19"
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   154
and 140: "~x53 | ~x47"
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   155
and 141: "~x19 | ~x47"
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   156
and 142: "~x20 | ~x54"
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   157
and 143: "~x20 | ~x48"
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   158
and 144: "~x54 | ~x48"
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   159
and 145: "~x21 | ~x55"
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   160
and 146: "~x21 | ~x20"
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   161
and 147: "~x21 | ~x49"
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   162
and 148: "~x55 | ~x20"
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   163
and 149: "~x55 | ~x49"
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   164
and 150: "~x20 | ~x49"
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   165
and 151: "~x22 | ~x56"
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   166
and 152: "~x22 | ~x21"
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   167
and 153: "~x22 | ~x50"
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   168
and 154: "~x56 | ~x21"
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   169
and 155: "~x56 | ~x50"
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   170
and 156: "~x21 | ~x50"
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   171
and 157: "~x23 | ~x57"
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   172
and 158: "~x23 | ~x22"
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   173
and 159: "~x23 | ~x51"
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   174
and 160: "~x57 | ~x22"
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   175
and 161: "~x57 | ~x51"
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   176
and 162: "~x22 | ~x51"
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   177
and 163: "~x24 | ~x58"
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   178
and 164: "~x24 | ~x23"
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   179
and 165: "~x24 | ~x52"
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   180
and 166: "~x58 | ~x23"
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   181
and 167: "~x58 | ~x52"
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   182
and 168: "~x23 | ~x52"
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   183
and 169: "~x59 | ~x24"
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   184
and 170: "~x59 | ~x53"
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   185
and 171: "~x24 | ~x53"
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   186
and 172: "~x25 | ~x54"
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   187
and 173: "~x26 | ~x25"
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   188
and 174: "~x26 | ~x55"
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   189
and 175: "~x25 | ~x55"
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   190
and 176: "~x27 | ~x26"
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   191
and 177: "~x27 | ~x56"
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   192
and 178: "~x26 | ~x56"
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   193
and 179: "~x28 | ~x27"
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   194
and 180: "~x28 | ~x57"
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   195
and 181: "~x27 | ~x57"
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   196
and 182: "~x29 | ~x28"
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   197
and 183: "~x29 | ~x58"
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   198
and 184: "~x28 | ~x58"
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   199
shows "False"
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   200
using 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   201
20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   202
40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   203
60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   204
80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   205
100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   206
120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   207
140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   208
160 161 162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179 
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   209
180 181 182 183 184 
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   210
by sat
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   211
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   212
end