Make TPTP Vampire proofs GDV compliant

[selig]

In Geoff's 'Service Tools' he has a proof checker called GDV... I'm not sure what GDV stands for.

This currently doesn't work for Vampire as it doesn't output the SZS status of each inference as suggested here: http://tptp.cs.miami.edu/TPTP/QuickGuide/Derivations.html

In that situation GDV assumes that the SZS status is "thm", i.e., the inferred formula is a logical consequence of its parents, and tests that with Otter.

However, when we negate the conjecture the status should be cth (countertheorem). There may be other cases where the thm status is too strong.

It would be nice to include the SZS status in TPTP proofs to make them work with GDV... shouldn't take much work.

[MichaelRawson]

Geoff says additionally that not all tools assume status(thm), so we should always provide the correct status.