Divisions

Competition Divisions (inspired by SPCs)

• THF Division: TH0 theorems

• TFA division: TF0 theorems with arithmetic

• FOF Division: FOF non-propositional theorems

• FNT Division: FOF non-propositional non-theorems

• CNF Division: CNF non-EPR theorems (discontinued)

• SAT Division: CNF non-EPR non-theorems (discontinued)

• EPR Division: Effectively propositional theorems and non-theorems

• UEQ Division: Unit equality CNF non-EPR theorems (just revived)

• LTB Division: FOF non-propositional theorems from large theories, presented in batches

Demonstration Division