Divisions
Competition Divisions
- The THF Division - 500 Typed Higher-order theorems
- The TFA Division - 200 Typed First-order theorems with Arithmetic
- The FOF Division - 500 First-order theorems
- The FNT Division - 200 First-order non-theorems
- The EPR Division - 150 Effectively propositional CNF
- The LTB Division - 5000 Large-Theory first-order theorems
Demonstration Division
- Special hardware; Special entrants