| System | Version | Divisions | Entrants | Affiliation |
|---|---|---|---|---|
| CVC3 | 2.4 | TFA | Cesare Tinelli (Clark Barrett) | University of Iowa (New York University) |
| E(P/LTB) | 1.4pre | FOF FNT CNF EPR UEQ LTB | Stephan Schulz | Technische Universität München |
| E-Darwin | 1.4 | FOF FNT CNF EPR UEQ | Björn Pelzer | Universität Koblenz-Landau |
| E-KRHyper | 1.2 | FOF FNT CNF EPR UEQ LTB | Björn Pelzer | Universität Koblenz-Landau |
| E-MaLeS | 1.0 | FOF | Daniel Kuehlwein (Josef Urban, Stephan Schulz) | Radboud Universiteit Nijmegen (Technische Universität München) |
| FIMO | 0.2 | FNT EPR | Orkunt Sabuncu | University of Potsdam |
| H2WO4 | 11.07 | TFA (demo) | David Stanovsky | Charles University in Prague |
| iProver | 0.8 | EPR | CASC | CASC-J5 EPR winner |
| iProver(‑SInE) | 0.9 | FOF FNT CNF EPR UEQ LTB | Konstantin Korovin | The University of Manchester |
| iProver‑Eq(‑SInE) | 0.7 | FOF FNT CNF EPR UEQ LTB | Christoph Sticksel (Konstantin Korovin) | The University of Manchester |
| Isabelle/HOL | 2011 | THF | Jasmin Blanchette (Larry Paulson, Tobias Nipkow, Markus Wenzel) | Technische Universität München |
| leanCoP | 2.2 | FOF | Jens Otten | University of Potsdam |
| LEO-II | 1.2 | THF | CASC | CASC-J5 THF winner |
| LEO-II | 1.2.8 | THF FOF CNF | Christoph Benzmüller | Freie Universität Berlin |
| MELIA | 0.1 | TFA | Peter Baumgartner | NICTA and ANU |
| Metis | 2.3 | FOF CNF EPR UEQ | Joe Hurd | Galois, Inc. |
| MetiTarski | 1.8 | TFA (demo) | Lawrence C. Paulson | University of Cambridge |
| Muscadet | 4.1 | FOF | Dominique Pastre | University Paris Descartes |
| Nitpick | 2011 | TNT | Jasmin Blanchette | Technische Universität München |
| Nitrox | 0.2 | FNT | Jasmin Blanchette (Emina Torlak) | Technische Universität München |
| Otter | 3.3 | FOF CNF UEQ | CASC (William McCune) | CASC (Argonne National Laboratory) |
| Paradox | 3.0 | FNT | CASC | CASC-J5 FNT winner |
| Refute | 2011 | TNT | Jasmin Blanchette (Tjark Weber) | Technische Universität München |
| Satallax | 2.1 | THF TNT | Chad Brown | Saarland University |
| SPASS+T | 2.2.14 | TFA | Uwe Waldmann (Stephan Zimmer) | Max-Planck-Institut für Informatik (AbsInt GmbH) |
| SPASS-XDB | 0.8 | TFA (demo) | Geoff Sutcliffe (Martin Suda, David Stanovsky) | University of Miami (Max‑Planck‑Institut für Informatik and Saarland University, Charles University in Prague) |
| TPS | 3.110228S1a | THF | Chad Brown | Saarland University |
| Vampire | 0.6 | FOF CNF | CASC | CASC-J5 FOF and CNF winner |
| Vampire | 1.8 | FOF CNF EPR UEQ LTB | Krystof Hoder (Andrei Voronkov) | The University of Manchester |
| Waldmeister | 710 | UEQ | CASC | CASC-J5 UEQ winner |
| Z3 | 2.20 | TFA (demo) | Nikolaj Bjorner (Leonardo de Moura) | Microsoft Research |