Thu, 24 Mar 2011 17:56:59 +0100add "-?" to "nitrox" tool
blanchet [Thu, 24 Mar 2011 17:56:59 +0100] rev 42972
add "-?" to "nitrox" tool

Thu, 24 Mar 2011 17:49:27 +0100clean up new Skolemizer code -- some old hacks are no longer necessary
blanchet [Thu, 24 Mar 2011 17:49:27 +0100] rev 42971
clean up new Skolemizer code -- some old hacks are no longer necessary

Thu, 24 Mar 2011 17:49:27 +0100specify proper defaults for Nitpick and Refute on TPTP + tuning
blanchet [Thu, 24 Mar 2011 17:49:27 +0100] rev 42970
specify proper defaults for Nitpick and Refute on TPTP + tuning

Thu, 24 Mar 2011 17:49:27 +0100added "nitrox" tool (Nitpick for first-order TPTP problems) to components
blanchet [Thu, 24 Mar 2011 17:49:27 +0100] rev 42969
added "nitrox" tool (Nitpick for first-order TPTP problems) to components

Thu, 24 Mar 2011 17:49:27 +0100made one more Metis example use the new Skolemizer
blanchet [Thu, 24 Mar 2011 17:49:27 +0100] rev 42968
made one more Metis example use the new Skolemizer

Thu, 24 Mar 2011 17:49:27 +0100Metis examples use the new Skolemizer to test it
blanchet [Thu, 24 Mar 2011 17:49:27 +0100] rev 42967
Metis examples use the new Skolemizer to test it

Thu, 24 Mar 2011 17:49:27 +0100new version of Metis 2.3 (29 Dec. 2010)
blanchet [Thu, 24 Mar 2011 17:49:27 +0100] rev 42966
new version of Metis 2.3 (29 Dec. 2010)

Thu, 24 Mar 2011 17:49:27 +0100remove newly added wrong logic
blanchet [Thu, 24 Mar 2011 17:49:27 +0100] rev 42965
remove newly added wrong logic

Thu, 24 Mar 2011 17:49:27 +0100more precise failure reporting in Sledgehammer/SMT
blanchet [Thu, 24 Mar 2011 17:49:27 +0100] rev 42964
more precise failure reporting in Sledgehammer/SMT

Thu, 24 Mar 2011 17:49:27 +0100avoid evil "export_without_context", which breaks if there are local "fixes"
blanchet [Thu, 24 Mar 2011 17:49:27 +0100] rev 42963
avoid evil "export_without_context", which breaks if there are local "fixes"