Divisions

Competition Divisions

• The MIX Division: Mixed CNF really non-propositional theorems
  
  • The HNE Category: Horn with No Equality
  • The HEQ Category: Horn with some (but not pure) Equality
  • The NNE Category: Non-Horn with No Equality
  • The NEQ Category: Non-Horn with some (but not pure) Equality
  • The PEQ Category: Pure Equality
  The MIX division has two classes.

• The FOF Division: Mixed FOF really non-propositional theorems
  • The FNE Category: FOF with no Equality
  • The FEQ Category: FOF with Equality
  The FOF division has two classes.

• The SAT Division: Mixed CNF really non-propositional non-theorems
  • The SNE Category: SAT with No Equality
  • The SEQ Category: SAT with Equality
  The SAT division has two classes.

• The EPR Division: CNF non-propositional theorems and non-theorems with a finite Herbrand Universe
  
  • The EPT Category: Effectively Propositional Theorems (unsatisfiable clauses)
  • The EPS Category: Effectively Propositional non-theorems (Satisfiable clauses)

• The UEQ Division: Unit equality CNF really non-propositional theorems
  

Demonstration Division

• Special hardware
• Special entrants