Vampire Subprocess Prover

This pre-release integrates our fast tree formulae representation with a vampire subprocess prover that can determine if a first order formula is a theorem.

• Support for formulae representation up to 2nd order. Some utilities for checking formula and term properties.
• A first order TPTP converter for formulae.
• A Problem class for representing theorem proving problems.
• A Vampire Subprocess prover which will attempt to solve a given problem by calling vampire on it.