| System | Divisions | Entrant | Affiliation |
|---|---|---|---|
| Beagle 0.9.22 | TFA TFN | Peter Baumgartner | NICTA/ANU |
| CVC4 1.4 | TFA | CASC | CASC-J7 TFA winner |
| CVC4 1.5 | TFA TFN FOF FNT | Andrew Reynolds | EPFL |
| E 1.9.1 | FOF FNT EPR LTB | Stephan Schulz | DHBW Stuttgart |
| ePrincess 1.0 | FOF | Peter Backeman | Uppsala University |
| ET 0.2 | FOF | Josef Urban | Radboud University Nijmegen |
| Geo-III 2015E | FOF FNT EPR | Hans de Nivelle | University of Wroclaw |
| iProver 0.9 | EPR | CASC | CASC-J7 EPR winner |
| iProver 1.0 | FNT | CASC | CASC-J7 FNT winner |
| iProver 2.0 | FOF FNT EPR LTB | Konstantin Korovin | University of Manchester |
| iProverModulo 0.7-0.3 | FOF | Guillaume Burel | ENSIIE/Cedric/Deducteam |
| Isabelle 2015 | THF | Jasmin Blanchette | Inria Nancy |
| leanCoP 2.2 | FOF | Jens Otten | University of Potsdam |
| LEO-II 1.6.2 | THF | Christoph Benzmüller | Freie Universität Berlin |
| MaLARea 0.5 | LTB | CASC | CASC-24 LTB winner |
| Muscadet 4.5 | FOF | Dominique Pastre | University Paris Descartes |
| Nitpick 2015 | THN | Jasmin Blanchette | Inria Nancy |
| Princess 20150706 | TFA TFN | Philipp Rümmer (Peter Backeman) | Uppsala University |
| Prover9 2009‑11A | FOF | William McCune | CASC |
| Refute 2015 | THN | Jasmin Blanchette | Inria Nancy |
| Satallax 2.8 | THF THN | Nik Sultana | Cambridge University |
| Satallax‑MaLeS 1.3 | THF | CASC | CASC-J7 THF winner |
| SPASS+T 2.2.22 | TFA | Uwe Waldmann | Max-Planck-Institut für Informatik |
| Vampire 2.6 | FOF | CASC | CASC-J7 FOF winner |
| Vampire 4.0 | TFA FOF FNT EPR LTB | Andrei Voronkov | University of Manchester |
| VampireZ3 1.0 | TFA | Giles Reger | University of Manchester |
| ZenonArith 0.1.0 | TFA | Guillaume Bury | Inria |