Thu, 26 Aug 2010 14:58:45 +0200 | blanchet | if the goal contains no constants or frees, fall back on chained facts, then on local facts, etc., instead of generating a trivial ATP problem | changeset | files |
Thu, 26 Aug 2010 14:05:22 +0200 | blanchet | improve SPASS hack, when a clause comes from several facts | changeset | files |