Vampire is winning at least one division of the world cup in theorem
proving CASC since 1999. All together Vampire won 30 titles: more than any other
We traditionally take part in the following two divisions
of the competition:
- The FOF division: unrestricted first-order problems. This
division was ranked second in importance after the MIX
division before 2007 and is now recognised as the main
- The CNF division: first-order problems in conjunctive normal
form. This division was called MIX and recognised
as the main competition division before 2007.
- The LTB division: problems with very large axiomatisations
(some of them contain about 3.5 million axioms).
Here is the list of our achievements:
| ||FOF ||CNF/MIX ||LTB|
|1999 || ||winner ||-|
|2000 ||winner || ||-|
|2001 || ||winner ||-|
|2002 ||winner ||winner ||-|
|2003 ||winner ||winner ||-|
|2004 ||winner* ||winner ||-|
|2005 ||winner ||winner* ||-|
|2006 ||winner ||winner* ||-|
|2007 ||winner ||winner* ||-|
|2008 ||winner ||winner* |
|2009 ||winner ||winner* ||winner|
|2010 ||winner ||winner ||winner*|
|2011 ||winner* || ||winner*|
|2012 (IJCAR) ||winner* || ||winner|
|2012 (Turing) ||winner* || ||winner|
|2013 ||winner || |
Note: winner* means that Vampire solved more problems that all other provers
in this division and '-' means that the division did not exist that year.
V for Victory for V for Vampire?