[Termtools] competition results - some comments

[Fabian Emmes]

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?

Best regards,
Fabian
-- 
Fabian Emmes           mailto:emmes at informatik.rwth-aachen.de
LuFG Informatik 2      http://verify.rwth-aachen.de/emmes/
RWTH Aachen            phone: +49 241 80-21241
-------------- next part --------------
A non-text attachment was scrubbed...
Name: not available
Type: application/pgp-signature
Size: 197 bytes
Desc: Digital signature
Url : http://lists.lri.fr/pipermail/termtools/attachments/20100121/870047cc/attachment.pgp