Our Trophies

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 prover.

We traditionally take part in the following two divisions of the competition:

  1. 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 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).

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?