Improving error messages

[ZachJHansen]

It would be nice to catch bad user input that will produce invalid TPTP files before piping that output to Vampire. The Vampire error messages can be too cryptic. A common issue is that a misnamed or missing variable in a quantification can produce a syntactically valid formula, but when passed to Vampire the variable is treated as type "$i" (Vampire's generic) rather than Anthem's $g, producing a semantic error. For example,

assumption: forall V X p(X, Y).

contains a typo (V should be called Y, or vice versa) but the bug doesn't get caught until Vampire produces the message

% Exception at proof search level
Parsing Error on line 35
Argument 2 of predicate p expected something of sort general but got something of sort $i