| System | Version | Divisions | R | Entrant (Associates) | Entrant's Affiliation | Entry date | Description | Solutions | V | Source |
|---|---|---|---|---|---|---|---|---|---|---|
| CASC-J13 | ||||||||||
| Connect++ | 0.7.2 | FOF FNT | Dr Sean B Holden | University of Cambridge | 29/06/26 | |||||
| CSIPlusPlus | 1.0 | FOF UEQ | Guoyan Zeng (Yang Xu, Baojie Rui, Stephan Schulz, Peiyao Liu, Hailin Guo, Jun Liu, Shuwei Chen) | Xihua University | 25/06/26 | |||||
| Drodi | 4.1.1 | FOF FNT UEQ | Oscar Contreras | Amateur Programmer | 24/03/26 | |||||
| E | 3.5.1 | THF FOF FNT UEQ | Stephan Schulz | DHBW Stuttgart | 08/05/26 | |||||
| FindProof | 0.1 | UEQ | Nik Murzin | Wolfram Institute | 29/06/26 | |||||
| FMB4J | 0.1 | FNT | Michael Rawson (Joe Hall) | University of Southampton | 28/06/26 | |||||
| iProver | 3.9.4 | FOF FNT UEQ | Konstantin Korovin | The University of Manchester | 29/06/26 | |||||
| LEO-II | 1.7.0 | THF | ✓ | Alexander Steen (Christoph Benzmüller) | University of Greifswald | 20/05/26 | Description | Samples | Source | |
| Leo-III | 1.8.0 | THF | Alexander Steen (Christoph Benzmüller) | University of Greifswald | 20/05/26 | |||||
| Mace4 | 2026-6A | FNT | Jeff Machado (Larry Lesyna) | Independent Researcher (LXL Technology) | 30/04/26 | |||||
| mrs | 0.2.0 | FOF FNT UEQ | Olivier Roland | - | 27/06/26 | |||||
| Prover9 | 1109a | FOF | ✓ | CASC (William McCune, Bob Veroff) | CASC (University of New Mexico) | 23/03/26 | Description | Samples | | Source |
| Prover9 | 2026-6A | FOF UEQ | Jeff Machado (Larry Lesyna) | Independent Researcher (LXL Technology) | 30/04/26 | |||||
| SATResetCoP | 1.0 | FOF | Martin Fixman (Fredrik Rømming, Sean Holden) | University of Cambridge | 18/06/26 | |||||
| SPASS-SCL | 0.1.1 | FOF | Simon Schwarz (Yasmine Briefs, Lorenz Leutgeb, Christoph Weidenbach, Fabian Wobito) | Max Planck Institute for Informatics | 29/06/26 | |||||
| SUPr | 1.0 | FOF | Teddy Kim (Adam Pease) | Naval Postgraduate School | 12/06/26 | |||||
| Twee | 2.7 | UEQ | Nick Smallbone (Guy Axelrod) | Chalmers University of Technology | 09/05/26 | |||||
| Vampire | 4.8 | FNT | ✓ | CASC | CASC-29 winner | 23/03/26 | Description | Samples | Source | |
| Vampire | 5.0 | THF FOF UEQ | ✓ | CASC | CASC-30 winner | 23/03/26 | Description | Samples | | Source |
| Vampire | 5.0.1 | THF FOF FNT UEQ | Márton Hajdu (Filip Bártek, Ahmed Bhayat, Jonas Bodingbauer, Robin Coutelier, Matthias Hetzenberger, Petra Hozzová, Laura Kovács, Jack McKeown, Merisa Mustajbasic, Axel Polaczek, Jakob Rath, Michael Rawson, Giles Reger, Martin Riener, Martin Suda, Johannes Schoisswohl, Andrei Voronkov, Eva Maria Wagner) | TU Wien | 29/06/26 | |||||
| VIP | 1.718281828459 | FOF | Ilies Nokrani (David Delahaye, Clémence Gerardin) | Université Montpellier - LIRMM | 29/06/26 | |||||
| Zipperposition | 2.1.9999 | THF FOF | ✓ | Jasmin Blanchette (Alexander Bentkamp, Simon Cruanes, Petar Vukmirović) | Ludwig-Maximilians-Universität München | 29/06/26 | Description | Samples | | Source |
| ProoVer 2026 | ||||||||||
| FindProof | 0.1 | ProoVer | Nik Murzin | Wolfram Institute | 29/06/26 | |||||
| GAPT | 2.20 | ProoVer | Fabian Achammer | TU Wien | 22/06/26 | |||||
| GDV | 2.0 | ProoVer | Geoff Sutcliffe | University of Miami | 08/04/26 | Description | ||||
| GDV-LP | 2.0 | ProoVer | Frédéric Blanqui (Geoff Sutcliffe) | ENS Paris-Saclay, INRIA | 12/06/26 | Description | ||||
| MaCheck | 1.0 | ProoVer | Matthew Farah (Alicia Marianache) | McMaster University | 29/06/26 | |||||
| mrs | 0.2.0 | ProoVer | Olivier Roland | - | 27/06/26 | |||||
| Nörgler | 1.1 | ProoVer | Alexander Steen (Melanie Taprogge, Happy Sariyanto) | University of Greifswald | 20/05/26 | |||||
| ProofCheck | 1.0 | ProoVer | Jeff Machado (Larry Lesyna) | Independent Researcher (LXL Technology) | 30/04/26 | |||||
| PyCheck | 0.1 | ProoVer | Stephan Schulz | DHBW Stuttgart | 08/05/26 | |||||
| VaLeaDate | 0.1 | ProoVer | Jonas Bodingbauer (Laura Kovacs) | TU Wien | 28/06/26 |
Division Lists
| Competition Divisions | ||||
|---|---|---|---|---|
| THF | FOF | FNT | UEQ | ProoVer |
|
E 3.5.1 LEO-II 1.7.0 Leo-III 1.8.0 Vampire 5.0.1 |
Connect++ 0.7.2 CSIPlusPlus 1.0 Drodi 4.1.1 E 3.5.1 iProver 3.9.4 mrs 0.2.0 Prover9 2026-6A SATResetCoP 1.0 SPASS-SCL 0.1.1 SUPr 1.0 Vampire 5.0.1 VIP 1.718281828459 Zipperposition 2.1.9999 |
Connect++ 0.7.2 Drodi 4.1.1 E 3.5.1 iProver 3.9.4 FMB4J 0.1 Mace4 2026-6A mrs 0.2.0 Vampire 5.0.1 |
CSIPlusPlus 1.0 Drodi 4.1.1 E 3.5.1 FindProof 0.1 iProver 3.9.4 mrs 0.2.0 Prover9 2026-6A Twee 2.7 Vampire 5.0.1 |
FindProof 0.1 GAPT 2.20 MaCheck 1.0 mrs 0.2.0 Nörgler 1.1 ProofCheck 1.0 PyCheck 0.1 VaLeaDate 0.1 |
| Demonstration Divisions | ||||
|
Vampire 5.0 |
Prover9 1109a Vampire 5.0 |
Vampire 4.8 |
Vampire 5.0 |
GDV 2.0 GDV-LP 2.0 |
Personal Details
| Who | System | T-Shirt | Rego | Here? | Dinner? | Notes |
|---|---|---|---|---|---|---|
| Fabian Achammer | GAPT 2.20 | Medium | 
| |||
| Jasmin Blanchette | Zipperposition 2.1.9999 | Large |
| |||
| Frédéric Blanqui | GDV-LP 2.0 | Medium |
| |||
| Jonas Bodingbauer | VaLeaDate 0.1 | Medium | ||||
| Yasmine Briefs | SPASS-SCL 0.1.1 | Small |
| Yes | Yes | |
| Oscar Contreras | Drodi 4.1.1 | Large |
| No | No |
Oscar Contreras, c/ Portugal, 4, Urb. Penas Albas 28810 Villalbilla Madrid, Spain |
| Matthew Farah | MaCheck 1.0 | XLarge | 
| |||
| Martin Fixman | SATResetCoP 1.0 | Large |
| |||
| Joe Hall | FMB4J 0.1 | Medium |
| |||
| Márton Hajdu | Vampire 5.0.1 | Large | ||||
| Dr Sean B Holden | Connect++ 0.7.2 | Large | ||||
| Teddy Kim | SUPr 1.0 | Medium |
| No | No | T-shirt only, give to Adam |
| Konstantin Korovin | iProver 3.9.4 | Medium | ||||
| Jeff Machado | Mace4 2026-6A, Prover9 2026-6A, ProofCheck 1.0 | XXLarge | 
| No | No | Post |
| Aart Middeldorp | Panelist | XLarge | Free | Yes | Yes | |
| Nik Murzin | FindProof 0.1 | Medium | ||||
| Cláudia Nalon | Panelist | Small | Free | No | No | |
| Ilies Nokrani | VIP 1.718281828459 | Medium | ||||
| Adam Pease | SUPr 1.0 | Medium |
| |||
| Michael Rawson | FMB4J 0.1 | Medium | Yes | Yes | ||
| Olivier Roland | mrs 0.2.0 | Medium |
| |||
| Stephan Schulz | E 3.5.1, PyCheck 0.1 | XXLarge |
| |||
| Simon Schwarz | SPASS-SCL 0.1.1 | Large |
| Yes | Yes | |
| Martina Seidl | Panelist | Large | Free | |||
| Nick Smallbone | Twee 2.7 | XLarge | ||||
| Alexander Steen | LEO-II 1.7.0, Leo-III 1.8.0, Nörgler 1.1 | Medium |
| No | Melanie | |
| Geoff Sutcliffe | Organizer, GDV 2.0 | XLarge ✓ | Free | Yes | Yes | Wear |
| Guoyan Zeng | CSIPlusPlus 1.0 | Small |
|