[Termtools] Termination Competition 2017 - finished

[Jera Hensel]

Dear all,

indeed, there are bugs in a processor of AProVE that cause these incorrect answers. We decided to deactivate the processor since it is never used outside of the ITS category.

Thanks for reporting the bugs, and thanks to Johannes for all his work within the last four years!

Best regards,
Jera

> Am 05.09.2017 um 17:56 schrieb Yamada, Akihisa <Akihisa.Yamada at uibk.ac.at>:
> 
> 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
> 
> _______________________________________________
> Termtools mailing list
> Termtools at lists.lri.fr
> http://lists.lri.fr/cgi-bin/mailman/listinfo/termtools