| System | Version | Divisions | Entrants | Affiliation |
|---|---|---|---|---|
| Darwin | 1.3 | EPR | CASC | CASC-J3 EPR winner |
| Darwin | 1.4.1 | EPR | Peter Baumgartner (Alexander Fuchs, Cesare Tinelli) | NICTA (University of Iowa) |
| FM-Darwin | 1.4.1 | FNT* SAT* | Peter Baumgartner (Alexander Fuchs, Cesare Tinelli) | NICTA (University of Iowa) |
| E | 0.999 | FOF CNF FNT SAT EPR UEQ | Stephan Schulz | Technische Universität München |
| EP | 0.999 | FOF* CNF* | Stephan Schulz | Technische Universität München |
| E-KRHyper | 1.0 | CNF* EPR | Björn Pelzer | University Koblenz-Landau |
| Equinox | 1.2 | FOF CNF EPR UEQ | Koen Claessen | Chalmers University of Technology |
| Fampire | 1.3 | FOF (demo) | Josef Urban | Charles University |
| Geo | 2007f | FOF* CNF* FNT* SAT* EPR UEQ | Hans de Nivelle | University of Wroclaw |
| iProver | 0.2 | FOF CNF FNT SAT EPR | Konstantin Korovin | The University of Manchester |
| leanCoP | 2.0 | FOF | Jens Otten (Thomas Raths) | University of Potsdam |
| ileanCoP | 1.2 | FOF (demo) | Jens Otten | University of Potsdam |
| Metis | 2.0 | FOF CNF* FNT* SAT* EPR UEQ | Joe Hurd | Oxford University |
| Muscadet | 2.7 | FOF | Dominique Pastre | Université René Descartes Paris‑5 |
| Otter | 3.3 | FOF CNF* UEQ | CASC (William McCune) | CASC (Argonne National Laboratory) |
| Paradox | 1.3 | SAT* | CASC | CASC-J3 SAT* winner |
| Paradox | 2.2 | FNT* SAT* EPR | Koen Claessen (Niklas Sörensson) | Chalmers University of Technology |
| Vampire | 8.1 | FOF* CNF* | CASC | CASC-J3 FOF* and CNF* winner |
| Vampire | 9.0 | FOF* CNF* EPR UEQ | Andrei Voronkov | The University of Manchester |
| Waldmeister | 806 | UEQ | CASC | CASC-J3 UEQ winner |