[Termtools] TC 2014 - certified categories

[Johannes Waldmann]

Dear all,


two certifiers were registered (CeTA, Rainbow)
but only CeTA actually made a pre-submission.

To simplify matters, I propose to run CeTA as a post-processor
on starexec (instead of a two-stage competition with
downloading solver outputs, and uploading for certification later).

Please test ceta-postproc.5  This contains original CeTA sources,
and a small driver program. Please report issues by email or
(preferred) to the tracker at https://github.com/jwaldmann/ceta-postproc

It should work for standard rewriting,
but there may well be some quirks for relative and complexity.


I do think we should have competition among certifiers,
but I don't think we'll have it this year.
Especially if certifiers handle different CPF subsets
(or extensions), then solver authors need time to adapt
(but at the moment it seems they need all their time
already for adapting to starexec).


- Johannes.