Divisions
Competition Divisions
- The THF Division - 500 Typed Higher-order theorems
- The TFA Division - 250 Typed First-order theorems with Arithmetic
- The FOF Division - 500 First-order theorems
- The FNT Division - 250 First-order non-theorems
- The UEQ Division - 250 Unit equality CNF
- The LTB Division - 10000 Large-Theory first-order theorems
- 8 versions of each problem - solve any version
Demonstration Division
- Special hardware; Special entrants