Divisions

Competition Divisions

• The THF Division (THF axioms with a provable conjecture)

• The FOF Division (FOF axioms with a provable conjecture)

• The FNT Division (FOF axioms possibly with non-provable conjecture)

• The CNF Division (unsatisfiable clause sets)

• The SAT Division (satisfiable clause sets) Suspended

• The EPR Division (finite HU clause sets)

• The UEQ Division (unsatisfiable unit equality clause sets)

• The LTB Division (batches of large-theory FOF problems)

Demonstration Division

• Special hardware; Special entrants
• The TFA Division (TFA axioms with a provable conjecture)