Mon, 14 May 2012 15:54:26 +0200 | blanchet | added debugging function | changeset | files |
Sun, 13 May 2012 16:31:01 +0200 | blanchet | LEO-II's "--sos" option confusingly disables rather than enables SOS, and SOS seems to be ignored anyway; also, pass a number of facts that's more appropriate for each prover | changeset | files |
Sun, 13 May 2012 16:31:01 +0200 | blanchet | eta-reduce definition-like equations for THF provers; Satallax in particular seems to love that | changeset | files |