Divisions
Competition Divisions
- The THF Division - 150 Typed Higher-order theorems
- The TFA Division - 100 Typed First-order theorems with arithmetic
- The FOF Division - 300 First-order theorems
- The FNT Division - 150 First-order non-theorems
- The EPR Division - 100 Effectively propositional CNF
- The LTB Division - 750 large-theory first-order theorems
Demonstration Division
- Special hardware; Special entrants