Trophies
Vampire has won at least one division of the world cup in theorem proving, CASC, since 1999. All together Vampire won 64 titles: more than any other prover. We take part in the following divisions of the competition:
- FOF: 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.
- CNF: first-order problems in conjunctive normal form. This division was called MIX and recognised as the main competition division before 2007.
- LTB (and its predecessor SEM): problems with very large axiomatisations, some containing upwards of 3.5 million axioms.
- EPR: 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
- UEQ: unit equational problems, containing only clauses with a single equation. Specialist systems based on completion are usually dominant here.
- FNT: 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.
- TFN: the typed version of FNT.
- TFA: 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.
- SLH: 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.
- THF: higher-order theorems. This has so far used a specialised branch of Vampire, developed mainly by Ahmed Bhayat.
Here is a table of our achievements:
| Year | FOF | CNF | LTB | EPR | UEQ | FNT | TFN | TFA | SLH | THF |
|---|---|---|---|---|---|---|---|---|---|---|
| 1999 | W | - | - | - | - | - | - | - | ||
| 2000 | W | - | - | - | - | - | - | |||
| 2001 | W | - | - | - | - | - | - | |||
| 2002 | W | W | - | - | - | - | - | - | ||
| 2003 | W | W | - | - | - | - | - | - | ||
| 2004 | W | W | - | - | - | - | - | - | ||
| 2005 | W | W | - | - | - | - | - | - | ||
| 2006 | W | W | - | - | - | - | - | - | ||
| 2007 | W | W | - | - | - | - | - | |||
| 2008 | W | W | - | - | - | - | ||||
| 2009 | W | W | W | - | - | - | ||||
| 2010 | W | W | W | - | - | - | ||||
| 2011 | W | W | - | - | ||||||
| 2012 | W | - | W | - | - | - | ||||
| 2013 | W | - | - | - | - | |||||
| 2014 | W | - | - | - | - | |||||
| 2015 | W | - | W | W | - | W | W | - | ||
| 2016 | W | - | W | - | W | W | - | |||
| 2017 | W | - | W | - | W | - | W | W | ||
| 2018 | W | - | - | W | - | W | - | |||
| 2019 | W | - | W | W | - | W | - | |||
| 2020 | W | - | - | W | - | W | - | |||
| 2021 | W | - | W | - | W | - | - | |||
| 2022 | W | - | W | - | W | - | ||||
| 2023 | W | - | - | - | W | W | W | W |
(- indicates the division did not run that year, W that Vampire won the division)
Since 2016 we have also entered SMT-COMP with some success.