| Tue, 22 Jun 2010 19:08:25 +0200 | blanchet | turn on "natural form" filtering in the Mirabelle tests, to see how it performs | changeset | files |
| Tue, 22 Jun 2010 18:47:45 +0200 | blanchet | missing "Unsynchronized" + make exception take a unit | changeset | files |
| Tue, 22 Jun 2010 18:31:49 +0200 | blanchet | added code to optionally perform fact filtering on the original (non-CNF) formulas | changeset | files |
| Tue, 22 Jun 2010 17:10:01 +0200 | blanchet | more cosmetics | changeset | files |
| Tue, 22 Jun 2010 17:07:39 +0200 | blanchet | cosmetics + prevent consideration of inlined Skolem terms in relevance filter | changeset | files |
| Tue, 22 Jun 2010 16:50:55 +0200 | blanchet | canonical argument order | changeset | files |
| Tue, 22 Jun 2010 16:40:36 +0200 | blanchet | leverage new data structure for handling "add:" and "del:" | changeset | files |
| Tue, 22 Jun 2010 16:23:29 +0200 | blanchet | thread original theorem along with CNF theorem, as a step toward killing the Skolem cache | changeset | files |