[Termtools] competition results - some comments
frederic.blanqui at inria.fr
Fri Jan 22 02:11:30 CET 2010
Fabian Emmes a écrit :
> Dear all,
> On 21. Jan, 09:46, Fabian Emmes wrote:
>> On 21. Jan, 15:46, Frederic Blanqui wrote:
>>> 1) I am suprised by the score of AProVE-COLOR. It does not reflect the
>>> experiments I did before the competition. And, indeed, with the version
>>> I had of AProVE before the competition, I get on my computer 119 proofs
>>> (instead of 70 only!) among the 263 problems solved by TTT2Cert. So, I
>>> wonder what's going wrong with AProVE-COLOR.
>> We also are very surprised by this result. All other versions of AProVE
>> gave results similar to what we expected. In our internal benchmarks --
>> with the versions submitted to the competition -- AProVE-COLOR could
>> give about 3/4 of the results (Yes and No) of AProVE-CeTa.
> the reason for AProVE-COLOR performing so badly in the competition is a
> missing minisat2core binary, which it expects in bin/. Unfortunately
> this was not catched in our local tests, since our testing machines have
> a directory containing minisat2core in their $PATH.
> As this is a rather unfortunate situation for both, the CoLoR team and
> the AProVE team, I would like to apologize for missing this one.
> Would it be possible -- and considered fair by the other teams --, to
> rerun AProVE-COLOR, after Simon adds the missing binary?
and all the certifiers on the new generated proofs...
More information about the Termtools