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 FEW Division - FEQ with a wall clock limit

• The FNT Division - 200 First-order non-theorems

• The EPR Division - 75 Effectively propositional CNF

• The UEQ Division - 200 Unit equality CNF
  • Back by popular demand; in hiatus since 2014

• The LTB Division - 10000 Large-Theory first-order theorems
  • 8 versions of each problem - solve any version

Demonstration Division

• Special hardware; Special entrants