Usage

This page gives information on how to use Vampire. See Download for how to download Vampire.

Manual

Vampire manual is not finished yet. While there is no manual, you can use the CAV 2013 tutorial paper, which describes main features of Vampire and some of its options.

Basic Usage

The most basic usage of Vampire is to save your problem in TPTP format and run vampire problem.p as this will run Vampire in default mode with a 60 second time-limit.

However, a better way to run Vampire is in portfolio mode i.e. vampire --mode casc -t 300 problem.p this will run for 300 seconds trying lots of different strategies. This will perform much better than default mode as it will try combinations of options, that are turned off by default, which may work well for your problem.

If you think the problem is satisfiable then you can also run vampire --mode casc_sat -t 300 problem.p which will use a set of strategies suited to satisfiable problems (as entered into the most recent CASC competition).

Finally, if your problem is in SMT-LIB format you can run vampire --input_syntax smtlib2 problem.smt2 to specify a different input language, or vampire --mode smtcomp problem.p to use the latest SMT-COMP schedule, which automatically selects the appropriate input language.

Note that all of these competition modes are really shortcuts for other combinations e.g. casc mode is a shortcut for vampire --mode portflio --schedule casc -t 300s -p tptp

Options and More Advanced Usage

To see a full list of options with some explanations run vampire --show_options on if there is an option with an unsatisfactory explanation then please report it either via the Issues tab or directly to Giles Reger.

For more advanced usage we recommend looking at a number of tutorials that have been given on Vampire. For example, the recent ASE 2017 tutorial.