| System | Version | Divisions | Entrants | Affiliation |
|---|---|---|---|---|
| Darwin | 1.3 | FOF CNF SAT* EPR | Alexander Fuchs* (Peter Baumgartner, Cesare Tinelli) | University of Iowa (National ICT Australia, University of Iowa) |
| FM-Darwin | 1.3 | SAT* EPR | Alexander Fuchs* (Peter Baumgartner, Cesare Tinelli) | University of Iowa (National ICT Australia, University of Iowa) |
| DCTP | 10.21p | EPR | CASC | CASC-20 EPR winner |
| E | 0.99 | FOF CNF SAT EPR UEQ | Stephan Schulz* | Technische Universität München |
| EP | 0.99 | FOF* CNF* | Stephan Schulz* | Technische Universität München |
| Equinox | 1.0 | FOF CNF EPR UEQ | Koen Claessen* | Chalmers University of Technology |
| Faust | 1.0 | FOF CNF* | Yury Puzis* | University of Miami |
| Geo | 2006i | FOF* CNF* SAT* EPR UEQ | Hans de Nivelle* (Jia Meng) | Max-Planck Institut für Informatik (National ICT Australia) |
| iProver | 0.1 | CNF EPR | Konstantin Korovin* | The University of Manchester |
| MathServe | 0.80 | FOF CNF SAT EPR UEQ (demo) | Juergen Zimmer (Serge Autexier*) | Universität des Saarlandes |
| Muscadet | 2.6 | FOF | Dominique Pastre* | Université René Descartes Paris‑5 |
| Octopus | 2006 | FOF CNF (demo) | Monty Newborn* | McGill University |
| Otter | 3.3 | FOF CNF* UEQ | CASC (William McCune) | CASC (Argonne National Laboratory) |
| Paradox | 1.3 | SAT* | CASC | CASC-20 SAT* winner |
| Paradox | 2.0 | SAT* EPR | Koen Claessen* (Niklas Sörensson) | Chalmers University of Technology |
| Theo | 2006 | FOF CNF* | Monty Newborn* | McGill University |
| Vampire | 8.0 | FOF* CNF* | CASC | CASC-20 FOF* and CNF* winner |
| Vampire | 8.1 | FOF* CNF* EPR UEQ | Andrei Voronkov | University of Manchester |
| Waldmeister | 704 | UEQ | CASC | CASC-20 UEQ winner |
| Waldmeister | 806 | UEQ | Thomas Hillenbrand* (Bernd Löchner) | Max-Planck-Institut für Informatik |