Our Trophies

CASC

Vampire has won at least one division of the world cup in theorem proving CASC since 1999. All together Vampire won 45 titles: more than any other prover. We take part in the following divisions of the competition:

1. The FOF division: first-order theorems. This division was ranked second in importance after the MIX division before 2007 and is now recognised as the main competition division.
2. The CNF division: first-order problems in conjunctive normal form. This division was called MIX and recognised as the main competition division before 2007.
3. The LTB division: problems with very large axiomatisations (some of them contain about 3.5 million axioms).
4. The EPR division: problems that fall within the Effectively Propositional fragment. We entered this track for the first time in 2015. The track is traditionally won by iProver
5. The FNT division: first-order non-theorems. We entered this track for the first time in 2015. Our success is supported heavily by our implementation of finite model building.
6. The TFA division: typed first-order theorems with arithmetic. We entered this track for the first time in 2015. Such problems are typically the domain of SMT solvers.
7. The SLH division: typed first-order theorems without arithmetic generated by Sledgehammer. This division has a much shorter time limit and is designed to reflect the Sledgehammer use case.

Here is the list of our achievements:

Note: winner* means that Vampire solved more problems that all other provers in this division (this has not been computed post 2013) and '-' means that the division did not exist that year. Tracks EPR, FNT, and TFA were entered for the first time in 2015. Track SLH only ran in 2017.

SMTCOMP

Since 2016 we have also entered SMTCOMP. We performed well both years (full details will be added here soon). You can view the results for 2016 and 2017 directly. Vampire competed in all tracks with quantifiers and without bitvectors or floating point.