Divisions

Competition Divisions (inspired by SPCs)

• The THF Division: THF0 theorems
  • The TNE category: THF with No Equality
  • The TEQ category: THF with Equality

• The TFA division: TFA0 theorems The TFA division has two problem categories:
  • The INT category: TFA with only INTeger arithmetic.
  • The RRL category: THF with only Rational and ReaL arithmetic.

• The FOF Division: FOF non-propositional theorems
  • The FNE category: FOF with No Equality
  • The FEQ category: FOF with Equality
  • The FEP category: FOF Effectively Propositional

• The FNT Division: FOF non-propositional non-theorems
  • The FNQ category: FOF with Equality
  • The FNN category: FOF with no Equality

• The CNF Division: CNF really-non-propositional theorems
  
  • The HEQ category: Horn with some (but not pure) Equality
  • The HNE category: Horn with No Equality
  • The NEQ category: Non-Horn with some (but not pure) Equality
  • The NNE category: Non-Horn with No Equality
  • The PEQ category: Pure Equality

• The SAT Division: CNF really-non-propositional non-theorems
  • The SNE category: SAT with No Equality
  • The SEQ category: SAT with Equality

• The EPR Division: Effectively propositional theorems And non-theorems
  • The EPT category: Effectively Propositional Theorems
  • The EPS category: Effectively Propositional non-theorems

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

• The LTB Division: First-order form non-propositional theorems from large theories, presented in batches
  
  • The CYC category: Problems from the Cyc contribution to the CSR domain
  • The MZR category: Problems from the MPTP contribution to the TPTP
  • The SMO category: Problems from SUMO contribution to the CSR domain

Demonstration Division

• Special hardware
• Special entrants