Set Theory
- 764 abstract problems, 321 FOF problems, 695 CNF problems
- Largest domain in the TPTP
- Five axiomatizations
- Two older ones [LS74][MOW76]
- Two NBG [BL+86][Qua92]
- One naive [Pas99]
- Very general problems, some equality, CNF ones are non-Horn
- Problem's based on the NBG axioms are hard challenges
- New problems from Belinfante
Category Theory
- 19 abstract problems, 58 CNF problems
- Four axiomatizations, all developed at ANL
- One based on Mitchell [Mit67]
- Two based on [Sco79]
- One proposed to Larry Wos by Art Quaife [Qua89]
- Problems have some equality