[Termtools] Competition: qualification rounds

Claude Marché Claude.Marche at lri.fr
Thu May 31 09:40:57 CEST 2007


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

-- 
Claude Marché                          | tel: +33 1 72 92 59 69           
INRIA Futurs - ProVal                  | mobile: +33 6 33 14 57 93 
Parc Orsay Université - ZAC des Vignes | fax: +33 1 74 85 42 29   
3, rue Jacques Monod - Bâtiment N      | http://www.lri.fr/~marche/
F-91893 ORSAY Cedex                    |




 



More information about the Termtools mailing list