Usage and Installation

The TFF models and tests can be run using the latest release or master branch of the Vampire theorem prover.

If you want to run the THF models, you need to either install the LEO-III theorem prover or build the Vampire hol branch from source using these instructions. Make sure to add the -DCMAKE_BUILD_HOL=ON flag.