| System | Divisions | Entrant | Affiliation |
|---|---|---|---|
| CSE 1.2 | FOF | Feng Cao | Southwest Jiaotong University |
| CSE_E 1.1 | FOF | Feng Cao | Southwest Jiaotong University |
| CVC4 1.7 | THF TFA FOF FNT | Andrew Reynolds | University of Iowa |
| E 2.4 | FOF FNT EPR UEQ LTB | Stephan Schulz | DHBW Stuttgart |
| Enigma 0.4 | FOF (demo) | Jan Jakubuv | Czech Technical University in Prague |
| Etableau 0.1 | FOF EPR | John Hester | University of Florida |
| GKC 0.4 | FOF EPR UEQ LTB | Tanel Tammet | Tallinn University of Technology |
| iProver 2.8 | EPR (demo) | CASC | CASC-J9 winner |
| iProver 3.0 | FOF FNT EPR UEQ LTB | Konstantin Korovin | University of Manchester |
| leanCoP 2.2 | FOF | Jens Otten | University of Oslo |
| LEO-II 1.7.0 | THF | Alexander Steen | University of Luxembourg |
| Leo-III 1.4 | THF LTB | Alexander Steen | University of Luxembourg |
| MaedMax 1.3 | UEQ | Sarah Winkler | University of Innsbruck |
| MaLARea 0.6 | LTB (demo) | CASC | CASC-J9 winner |
| MaLARea 0.8 | LTB (demo) | Josef Urban | Czech Technical University in Prague |
| nanoCoP 1.1 | FOF | Jens Otten | University of Oslo |
| Prover9 1109a | FOF (demo) | CASC | CASC |
| PyRes 1.0 | FOF FNT EPR | Stephan Schulz | DHBW Stuttgart |
| Satallax 3.3 | THF (demo) | CASC | CASC-J9 winner |
| Satallax 3.4 | THF | Michael Färber | Inria Saclay |
| Twee 2.2 | FOF UEQ | Nick Smallbone | Chalmers University of Technology |
| Vampire 4.3 | TFA FOF FNT (demo) | CASC | CASC-J9 winner |
| Vampire 4.4 | THF TFA FOF FNT EPR UEQ LTB | Giles Reger | University of Manchester |
| Waldmeister 710 | UEQ (demo) | CASC | CASC-J7 winner |
| Zipperposition 1.5 | THF FOF | Petar Vukmirović | Vrije Universiteit Amsterdam |