| Mon, 20 Jun 2011 12:13:43 +0200 |
blanchet |
clean up SPASS FLOTTER hack
|
changeset |
files
|
| Mon, 20 Jun 2011 11:42:41 +0200 |
blanchet |
remove automatic recovery from (some) unsound proofs, now that we use sound encodings for all the interesting provers
|
changeset |
files
|
| Mon, 20 Jun 2011 10:41:02 +0200 |
blanchet |
only refer to facts found in TPTP file -- e.g. facts that simplify to true are excluded
|
changeset |
files
|
| Mon, 20 Jun 2011 10:41:02 +0200 |
blanchet |
slightly better setup for E
|
changeset |
files
|
| Mon, 20 Jun 2011 10:41:02 +0200 |
blanchet |
respect "really_all" argument, which is used by "ATP_Export"
|
changeset |
files
|
| Mon, 20 Jun 2011 10:41:02 +0200 |
blanchet |
slightly better setup for SPASS and Vampire as more results have come in
|
changeset |
files
|
| Mon, 20 Jun 2011 10:41:02 +0200 |
blanchet |
optimized SPASS and Vampire time slices, like E before
|
changeset |
files
|
| Mon, 20 Jun 2011 10:41:02 +0200 |
blanchet |
optimized E's time slicing, based on latest exhaustive Judgment Day results
|
changeset |
files
|
| Mon, 20 Jun 2011 10:41:02 +0200 |
blanchet |
deal with ATP time slices in a more flexible/robust fashion
|
changeset |
files
|
| Mon, 20 Jun 2011 09:19:31 +0200 |
wenzelm |
literal unicode in README.html allows to copy/paste from Lobo output;
|
changeset |
files
|
| Sun, 19 Jun 2011 22:53:37 +0200 |
wenzelm |
merged;
|
changeset |
files
|
| Sun, 19 Jun 2011 22:53:15 +0200 |
wenzelm |
explain special control symbols;
|
changeset |
files
|
| Sun, 19 Jun 2011 22:52:49 +0200 |
wenzelm |
accept control symbols;
|
changeset |
files
|
| Sun, 19 Jun 2011 18:12:49 +0200 |
blanchet |
fixed silly ATP exporter bug: if the proof of lemma A relies on B and C, and the proof of B relies on C, return {B, C}, not {B}, as the set of dependencies
|
changeset |
files
|