| System | Version | Divisions | Entrants | Affiliation | |||
|---|---|---|---|---|---|---|---|
| Darwin | 1.4.4 | EPR | Peter Baumgartner (Alexander Fuchs, Cesare Tinelli) | NICTA (University of Iowa) | |||
| E | 1.1pre | FOF FNT CNF SAT EPR UEQ LTB | Stephan Schulz | Technische Universität München | |||
| EP | 1.1pre | FOF* FNT* LTB* | Stephan Schulz | Technische Universität München | |||
| E-Darwin | 1.2 | CNF EPR | Björn Pelzer | University Koblenz-Landau | |||
| E-KRHyper | 1.1.3 | FOF FNT CNF SAT EPR LTB | Björn Pelzer | University Koblenz-Landau | |||
| Equinox | 4.1 | FOF CNF UEQ | Koen Claessen | Chalmers University of Technology | |||
| Infinox | 1.0 | FOF FNT CNF SAT EPR UEQ (demos) | Ann Lillieström (Koen Claessen) | Chalmers University of Technology | |||
| iProver | 0.5 | EPR | CASC | CASC-J4 EPR winner | |||
| iProver | 0.7 | FOF FNT CNF SAT EPR | Konstantin Korovin | The University of Manchester | |||
| iProver-SInE | 0.7 | LTB | Konstantin Korovin | The University of Manchester | |||
| iProver-Eq | 0.5 | FOF CNF UEQ | Konstantin Korovin (Christoph Sticksel) | The University of Manchester | |||
| Isabelle/HOL | 2009 | THF | Jasmin Blanchette (Larry Paulson, Tobias Nipkow, Makarius Wenzel, Stefan Berghofer) | Technische Universität München (University of Cambridge, Technische Universität München) | |||
| leanCoP | 2.1 | FOF* | Jens Otten | University of Potsdam | |||
| leanCoP-SInE | 2.1 | LTB* | Jens Otten (Thomas Raths) | University of Potsdam | |||
| LEO-II | 1.0 | THF | Christoph Benzmüller (Frank Theiss) | International University in Germany | |||
| matita | 1.0 | UEQ | Wilmer Ricciotti | University of Bologna | |||
| Metis | 2.2 | FOF* FNT* CNF SAT EPR UEQ | Joe Hurd | Galois, Inc. | |||
| OSHL-S | 0.6 | FOF FNT CNF SAT EPR | Hao Xu (David Plaisted) | University of North Carolina at Chapel Hill | |||
| Otter | 3.3 | FOF CNF UEQ | CASC (William McCune) | CASC (Argonne National Laboratory) | |||
| Paradox | 3.0 | FNT* SAT | CASC | CASC-J4 FNT* winner CASC-J4 SAT runner-up | |||
| SInE | 0.4 | LTB* | CASC | CASC-J4 LTB* winner (SInE 0.3, updated for the new LTB rules) | |||
| TPS | 3.20080227G1d | THF | Peter B. Andrews (Chad E. Brown) | Carnegie Mellon University (Saarland University) | |||
| Vampire | 10.0 | FOF* CNF | CASC | CASC-J4 FOF* and CNF winner | |||
| Vampire | 11.0 | FOF* CNF UEQ LTB* | Andrei Voronkov (Krystof Hoder) | The University of Manchester | |||
| Waldmeister | 806 | UEQ | CASC | CASC-J4 UEQ winner | |||
| Waldmeister | C09a | UEQ | Thomas Hillenbrand | Max Planck Institut für Informatik |