check conformance between claims (in first line, in CPF)

[jwaldmann]

So far, the competition specification prescribes that output starts with the plain result, as in

YES
<?xml version="1.0" ...

Do we still want this?

• pro: the answer is clearly visibible (for a human, for a simple-minded program) (otherwise, need to parse a huge XML structure)
• con: this is just another source of ambiguity (what if the first line reads "YES" but the actual proof contains "NO") that needs to be checked - by whom? By another un-verified program?

Ideally, conformance of the claims (in the first line, in the CPF) should be checked by CeTA, which then actually needs three arguments:

1. benchmark (TRS),
2. claim,
3. proof (CPF)

Cf. https://github.com/jwaldmann/ceta-postproc/blob/master/src/Main.hs#L43

... case certify_proof a problemString {- claim -} proofString of ...

Note that the current post-processor ceta-2.30-1 does NOT check conformance of claims (and hence, this issue is marked as a bug)

[jwaldmann]

three-argument ceta: see 7d4881e

[jwaldmann]

this seems to be fixed in principle now. Closing this issue, will open separate issues if any problem turns up.