First Solutions
The Existence of Quasigroups
- John Slaney, Otter/Prover9, 1995
- TPTP GRP domain
Solution of the Robbins Problem
- Bill McCune, EQP, 1996
- TPTP ROB001-1
Inner Five-segment Theorem of Tarski’s Geometry
- Stephan Schulz, E, 2019
- Posed by Art Quaife, 1989
- TPTP GEO033-2
Consistency of High School Biology
- Kostya Korovin, iProver, 2021
- Encoded by Michael Wessel in 2013
- TPTP BIO001+1
Circle of Pure Moufang Proofs
- Larry Wos, Otter, 2021
- TPTP RNG domain