[Termtools] Termination Competition 2017 - finished

[Yamada, Akihisa]

Dear Johannes,

thank you very much for the great web interface! It is exciting that we have so many unexpected results!

Due to the new certified ITS category, it seems that two of AProVE's 'NO's are wrong:

ITS/From_T2/ludcmp.c.i.ludcmp.pl.t2.fixed.t2.smt2: cf. https://termcomp.imn.htwk-leipzig.de/pairs/306778192
ITS/From_AProVE_2014/RetValRec.jar-obl-8.smt2: cf. https://termcomp.imn.htwk-leipzig.de/pairs/306778289

For other inconsistencies I couldn't judge from certified results.

Strange results from NaTT: oops, I did something CeTA doesn't know :)
Strange results from T2: they are basically that the output proofs don't follow CPF.

Best regards,
Akihisa

> On 5 Sep 2017, at 16:56, Johannes Waldmann <johannes.waldmann at htwk-leipzig.de> wrote:
> 
> Dear all,
> 
> 
> Starexec just finished running the competition jobs.
> 
> results: https://termcomp.imn.htwk-leipzig.de/competitions/65
> 
> inconsistencies this year:
> https://termcomp.imn.htwk-leipzig.de/problems/False/24394/24399/24400/24402
> 
> compare to last year:
> https://termcomp.imn.htwk-leipzig.de/combine/Y2016/65
> (but note https://github.com/jwaldmann/star-exec-presenter/issues/178 )
> 
> comments welcome.
> 
> 
> I will be running the "demonstration categories"
> (with just one participant) tomorrow morning.
> 
> 
> - Johannes.
> _______________________________________________
> Termtools mailing list
> Termtools at lists.lri.fr
> http://lists.lri.fr/cgi-bin/mailman/listinfo/termtools