Our Trophies

Vampire is winning at least one division of the world cup in theorem proving CASC since 1999. All together Vampire won 23 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:

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?