[Termtools] Re: time limit for coq?

[Frederic Blanqui]

On Wed, 6 Jun 2007, Frederic Blanqui wrote:

> hello claude. could you remember what is the time limit for coq?
>
> it is interesting to note that tpa and ttt2 output proofs that cannot be 
> checked by coq in this time limit:
>
> TRS/TRCSR - OvConsOS_nokinds_noand_GM

the proof produced by tpa for this problem can be checked by coq in 1330 
seconds = 22 minutes.

11:29 huggy ~/rainbow-cvs runme ../TPA-cert/tpa_opt ../tpdb/TRS/TRCSR/OvConsOS_nokinds_noand_GM.trs
../tpdb/TRS/TRCSR/OvConsOS_nokinds_noand_GM.trs
tpa_opt... 45.56
rainbow... 0.07
coq... 1330.86
YES