[Termtools] competition results - some comments

[Frederic Blanqui]

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...