[Termtools] Competition: qualification rounds

Joerg Endrullis joerg at endrullis.de
Thu May 31 11:01:46 CEST 2007


There seems to be a technical problem with jambox.
I can reconstruct that "qualif - a3b3" and "qualif - a3b4" are not solved,
since jambox needs more than 20 seconds for them.

But "qualif - quot" should be solved within 3 seconds.
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.
Maybe this is not the case?

Best regards,
Joerg

Claude Marché wrote:
> It is apparently a technical problem when torpa calls minisat. For
> matchbox, I can run a qualification round with 1 minute instead. I was
> using 20s for quickly testing
>
>   
>>>>>> "Johannes" == Johannes Waldmann <waldmann at imn.htwk-leipzig.de> writes:
>>>>>>             
>
>     Johannes> Claude Marché wrote:
>     >> Done. With 20 seconds time limit, no tool find any proof. 
>
>     Johannes> could you double-check this?
>
>     Johannes> On my (slow) machine, I get
>
>     Johannes>             jw1     z086
>     Johannes> torpa-1.7   9 sec   19 sec
>     Johannes> matchbox   30 sec   30 sec
>
>     Johannes> So I believe your results for matchbox
>     Johannes> (but then your machine is not that fast, I was hoping for more :-)
>     Johannes> but not for torpa.
>
>     Johannes> Best regards, Johannes.
>     Johannes> _______________________________________________
>     Johannes> Termtools mailing list
>     Johannes> Termtools at lists.lri.fr
>     Johannes> http://lists.lri.fr/mailman/listinfo/termtools
>
>   



More information about the Termtools mailing list