made sorting of Vampire facts more robust in the face of names that deviate from the standard scheme

robustly handle empty proof blocks in Isar proof output

propagate right result when enough proofs have been found

correctly parse E proofs that assume '=' and '!=' bind more tightly than connectives

don't lose error messages

don't pass --auto-schedule to E indiscriminately -- use it instead of 'auto' in one slice

careful with partial applications

don't perform preplaying steps if preplaying is disabled

adjust TPTP THF parser to give priority to @ over other operators, to parse Ehoh proofs

tuned punctuation