Mon, 04 Aug 2014 13:06:24 +0200 default on 'metis' for ATPs if preplaying is disabled
blanchet [Mon, 04 Aug 2014 13:06:24 +0200] rev 57778
default on 'metis' for ATPs if preplaying is disabled
Mon, 04 Aug 2014 12:52:48 +0200 more informative preplay failures
blanchet [Mon, 04 Aug 2014 12:52:48 +0200] rev 57777
more informative preplay failures
Mon, 04 Aug 2014 12:28:42 +0200 rationalized sorting of facts -- so that preplaying (almost always) coincides with the real thing, preventing odd failures
blanchet [Mon, 04 Aug 2014 12:28:42 +0200] rev 57776
rationalized sorting of facts -- so that preplaying (almost always) coincides with the real thing, preventing odd failures
Mon, 04 Aug 2014 11:54:23 +0200 slightly earlier exit from preplaying
blanchet [Mon, 04 Aug 2014 11:54:23 +0200] rev 57775
slightly earlier exit from preplaying
Mon, 04 Aug 2014 11:43:19 +0200 honor 'dont_minimize' option when preplaying one-liner proof
blanchet [Mon, 04 Aug 2014 11:43:19 +0200] rev 57774
honor 'dont_minimize' option when preplaying one-liner proof
Sun, 22 Jun 2014 06:16:57 +0100 Metis is being used to emulate E steps;
sultana [Sun, 22 Jun 2014 06:16:57 +0100] rev 57773
Metis is being used to emulate E steps;
Sun, 22 Jun 2014 06:16:56 +0100 updated application of print_tac to take context parameter;
sultana [Sun, 22 Jun 2014 06:16:56 +0100] rev 57772
updated application of print_tac to take context parameter;
Sat, 02 Aug 2014 00:15:08 +0200 better duplicate detection
blanchet [Sat, 02 Aug 2014 00:15:08 +0200] rev 57771
better duplicate detection
Fri, 01 Aug 2014 23:58:42 +0200 normalize conjectures vs. negated conjectures when comparing terms
blanchet [Fri, 01 Aug 2014 23:58:42 +0200] rev 57770
normalize conjectures vs. negated conjectures when comparing terms
Fri, 01 Aug 2014 23:33:43 +0200 tweaked 'clone' formula detection
blanchet [Fri, 01 Aug 2014 23:33:43 +0200] rev 57769
tweaked 'clone' formula detection
(0) -30000 -10000 -3000 -1000 -300 -100 -10 +10 +100 +300 +1000 +3000 +10000 tip