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