Divisions

Competition Divisions

• The FOF Division (FOF axioms with a provable conjecture)
  • 2 problem categories (for analysis of specialization);
    2 ranking classes (for analysis of capability)

• The FNT Division (FOF axioms possibly with non-provable conjecture)
  • 2 problem categories; 2 ranking classes

• The CNF Division (unsatisfiable clause sets)
  • 5 problem categories; 1 ranking class

• The SAT Division (satisfiable clause sets)
  • 2 problem categories; 1 ranking class

• The EPR Division (finite HU clause sets)
  • 2 problem categories; 1 ranking class

• The UEQ Division (unsatisfiable unit equality clause sets)
  • 1 problem category; 1 ranking class

• The LTB Division (batches of FOF problems)
  • 3 problem categories; 2 ranking class
  • Real $$$$ prizes

Demonstration Division

• The THF Division (THF axioms with a provable conjecture)
  • 2 problem categories; 0 ranking classes

• Special hardware
• Special entrants