Version 4.5-poly-hol for higher-order and polymorphic problems

This version of Vampire supports FOL with rank-1 polymorphism and (TPTP's TF1) and higher-order logic (THF).

It has diverged somewhat from the main Vampire branch. You should not use this version if you are not interested in TF1 or THF problems e.g. if you want to run on just first-order problems or SMTLIB problems then use the main 4.5.1 release.

This release contains a few minor bug fixes implemented since CASC

4.4

Version 4.4 of Vampire (as submitted to CASC 2019)

CASC 2018

The version of Vampire submitted to CASC 2018

CASC 2019 THF Submission

The THF submission for CASC 2019. This has diverged from the master branch but future plans may bring it back into master. Do not use this version for attempting non THF problems as it will not perform as well as the master branch.

ijcar2018-data

Vampire extended to reason about datatypes and codatatypes.

Corresponds to the version used for experiments in the paper "Superposition with Datatypes and Codatatypes"

4.2.2

A stable version tagged as Vampire code is made available publicly. Corresponds (roughly) to the version used in the ASE 2017 tutorial.

CASC 2016

The version of Vampire submitted to CASC in 2016