[Termination tools] Several issues

[Jörg Endrullis]

I also want to thank Claude and Hans for organizing the competition!

Claude Marche schrieb:
> I expected this answer from you, of course. But my proposal could be
> made less strict. For example :
> 
> 1) first run each tool with a timeout of 5 seconds
> 2) if no tool solved the pb within 1 second (not 5), rerun the tools which
> were unsuccessfull with a timeout of 1 minute.
> 3) if no tool solves the pb within 30 seconds, rerun the tools which
> were unsuccesfull with a timeout of 5 minutes.

I would suggest another alternative. We could introduce an overall 
timeout (1 minute * number of problems). First we run the whole contest 
with a timeout of 10 seconds. After that we could rerun the tools on the 
problems they were unsuccessful with the timeout ((overall - spent) / 
(problems left)). This would encourage fast termination provers but 
allow to spent more time for a limited number of problems.

There is one more thing to mention: I would appreciate every tool to be 
open source.

Best Regards,
Jörg Endrullis