[Termtools] certified - strange proofs

[Christian Sternagel]

I do have some remarks:

- It would be convenient (as already suggested in Nancy) if methods
with different instances (like DP: classical, nachum; or EDG: various
approximations) would be annotated by some unique identifier in an
XML-proof.

- It should not be the responsibility of a "tool-to-be-certified" to
generate correct output, since certification is done to check the
tool. I think this can be avoided by Rainbow by always providing at
least the statement to be proved (i.e. the input TRS).

cheers

christian

P.S.: the current situation is of course my fault since I did not inform
myself properly. Currently only uncaught exceptions produce an exit state
different from 0. MAYBE is not considered as erroneous outcome.

P.S.S.: I think it is easy to find this 'wrong' proofs since they
are only produced if ttt2-cert timed out (at 60 seconds since we thought that
this would be the timeout for the whole competition---but I do not think
that a higher timeout would bring much better results anyway).

I will compile a list of this faulty proofs to the best of my knowledge.