Vampire supports multiple output modes for CASC, SMTCOMP, etc. that have their own rules about extra (non-proof) lines in the output.
We should make sure that these rules are followed when outputting e.g. warnings, errors, stats, and so on.
For example, in TPTP output mode, every non-proof line should start with % to indicate that it is a comment and the various systems in the TPTP ecosystem won't try to interpret these lines.
The task is to make a wrapper for printing that knows about the current output mode, use this wrapper everywhere, and maybe even ban any other printing in the future.
Vampire supports multiple output modes for CASC, SMTCOMP, etc. that have their own rules about extra (non-proof) lines in the output.
We should make sure that these rules are followed when outputting e.g. warnings, errors, stats, and so on.
For example, in TPTP output mode, every non-proof line should start with
%to indicate that it is a comment and the various systems in the TPTP ecosystem won't try to interpret these lines.The task is to make a wrapper for printing that knows about the current output mode, use this wrapper everywhere, and maybe even ban any other printing in the future.