[Termtools] Competition: qualification rounds

[Rene Thiemann]

Dear Claude,

Joerg wrote:
> But "qualif - quot" should be solved within 3 seconds.

The same applies for AProVE, the 8 seconds seem to be far to much. On our 
machines the time is about 3 seconds (2.4 Ghz Intel).

Joerg wrote:
> I think the reason is, that jambox does not find minisat.
> In the runme script there is a variable:
>   INSTALLDIR=.
> The "." works only if the woring directory is indeed equal to the jambox
> installation directory.

As for Jambox the statement 

PATH=./bin:$PATH

in our runme-file only works if initially a make was called which compiles 
(special versions of) minisat into the bin-directory.

So Claude, can you please check whether 

cp /.../tpdp/qualif/quot.trs /.../aprovedir
cd /.../aprovedir
make clean
make 
time ./runme quot.trs 60

also needs 8 seconds for the runme-call in the last line? If you use similar 
machines to ours (as was the case in the last years) we would be quite 
surprised if AProVE needs clearly more than 3 seconds.

Thanks for your effort and best regards,
Rene
-- 
René Thiemann         mailto:thiemann at informatik.rwth-aachen.de
LuFG Informatik II    http://www-i2.informatik.rwth-aachen.de/thiemann
RWTH Aachen           phone: +49 241 80-21241