Divisions

Competition Divisions (inspired by SPCs)

• THF Division: TH0 theorems

• THN Division: TH0 non-theorems (discontinued)

• TFA division: TF0 theorems with arithmetic

• TFN Division: TFF non-theorems

• FOF Division: FOF non-propositional theorems

• FNT Division: FOF non-propositional non-theorems (discontinued)

• 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 (back from hiatus)

• LTB Division: FOF theorems from large theories, presented in batches (discontinued)

• SLH Division: TH0 theorems from Sledgehammer (discontinued)

• ICU Division: Hard problems supplied by entrants

Demonstration Division