[Termtools] SRS-standard-certifying

Simon Bailey simon.bailey at uibk.ac.at
Sat Nov 8 12:01:28 CET 2008


hi,

On Nov 8, 2008, at 11:54 AM, Johannes Waldmann wrote:
> Then I note that the category seems to be stopped
> (last result is from today, Saturday 7:59 a.m.)
> Why is this? Is it related to the points above?

excerpt from the log:

<<<
Nov 8, 2008 7:59:39 AM: AProVE-CERT on: tpdb-5.0/SRS/secret05/ 
matchbox2.srs
Translating 1226127590627 to bccgbchfjagch
Certifying!
Certification Time's up!
 >>>

coqc was hung in an endless loop trying to certify AProVE's output. i  
had to manually kill that coq process.

this is the output:
http://colo5-c703.uibk.ac.at:8080/termcomp/competition/resultDetail.seam?resultId=30355&cid=10511

maybe somebody can see if that proof is even valid?

regards,
sb


More information about the Termtools mailing list