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 TRS/TRCSR - PALINDROME_complete-noand_FR