| System | Version | Divisions | Entrants | Affiliation |
|---|---|---|---|---|
| Darwin | 1.2 | MIX SAT* EPR | Alexander Fuchs (Peter Baumgartner, Cesare Tinelli) | University of Iowa (Max-Planck-Institut für Informatik, University of Iowa) |
| DCTP | 10.21p | EPR | CASC | CASC-J2 EPR winner |
| E | 0.9pre3 | MIX FOF SAT EPR UEQ | Stephan Schulz | TU München |
| EP | 0.9pre3 | MIX* FOF* | Stephan Schulz | TU München |
| Mace2 | 2.2 | SAT* | William McCune | Argonne National Laboratory |
| Mace4 | 0705D | SAT* | William McCune | Argonne National Laboratory |
| MathServ | 0.62 | MIX FOF SAT EPR UEQ (demo) | Jürgen Zimmer (Serge Autexier) | Universität des Saarlandes |
| Muscadet | 2.5 | FOF | Dominique Pastre | Universite Rene Descartes - Paris |
| Octopus | JN05 | MIX FOF (demo) | Monty Newborn (Zongyan Wang) | McGill University |
| Otter | 3.3 | MIX* FOF UEQ | CASC (William McCune) | CASC (Argonne National Laboratory) |
| Paradox | 1.0 | SAT* | CASC | CASC-J2 SAT* winner |
| Paradox | 1.3 | SAT* EPR | Koen Claessen (Niklas Sörensson) | Chalmers University of Technology |
| Prover9 | 0705 | MIX* FOF* UEQ | William McCune | Argonne National Laboratory |
| THEO | JN05 | MIX FOF | Monty Newborn | McGill University |
| Vampire | 7.0 | MIX* FOF* | CASC | CASC-J2 MIX, MIX*, FOF, and FOF* winner |
| Vampire | 8.0 | MIX* FOF* EPR UEQ | Andrei Voronkov | University of Manchester |
| Waldmeister | 704 | UEQ | CASC | CASC-J2 UEQ winner |