Mon, 06 Jun 2011 20:36:35 +0200 make "metisX"'s default more like old "metis"
blanchet [Mon, 06 Jun 2011 20:36:35 +0200] rev 43199
make "metisX"'s default more like old "metis"
Mon, 06 Jun 2011 20:36:35 +0200 whitespace tuning
blanchet [Mon, 06 Jun 2011 20:36:35 +0200] rev 43198
whitespace tuning
Mon, 06 Jun 2011 20:36:35 +0200 tuned Metis examples
blanchet [Mon, 06 Jun 2011 20:36:35 +0200] rev 43197
tuned Metis examples
Mon, 06 Jun 2011 20:36:35 +0200 more through tests of new Metis
blanchet [Mon, 06 Jun 2011 20:36:35 +0200] rev 43196
more through tests of new Metis
Mon, 06 Jun 2011 20:36:35 +0200 improved correctness of handling of higher-order occurrences of "Not" in new Metis (and probably in old Metis)
blanchet [Mon, 06 Jun 2011 20:36:35 +0200] rev 43195
improved correctness of handling of higher-order occurrences of "Not" in new Metis (and probably in old Metis)
Mon, 06 Jun 2011 20:36:35 +0200 fixed type helper indices in new Metis
blanchet [Mon, 06 Jun 2011 20:36:35 +0200] rev 43194
fixed type helper indices in new Metis
Mon, 06 Jun 2011 20:36:35 +0200 improved ATP clausifier so it can deal with "x => (y <=> z)"
blanchet [Mon, 06 Jun 2011 20:36:35 +0200] rev 43193
improved ATP clausifier so it can deal with "x => (y <=> z)"
Mon, 06 Jun 2011 20:36:35 +0200 avoid renumbering hypotheses
blanchet [Mon, 06 Jun 2011 20:36:35 +0200] rev 43192
avoid renumbering hypotheses
Mon, 06 Jun 2011 20:36:35 +0200 fixed reconstruction of new Skolem constants in new Metis
blanchet [Mon, 06 Jun 2011 20:36:35 +0200] rev 43191
fixed reconstruction of new Skolem constants in new Metis
Mon, 06 Jun 2011 20:36:35 +0200 don't translate new Skolemizer assumptions in new Metis
blanchet [Mon, 06 Jun 2011 20:36:35 +0200] rev 43190
don't translate new Skolemizer assumptions in new Metis
(0) -30000 -10000 -3000 -1000 -300 -100 -10 +10 +100 +300 +1000 +3000 +10000 tip