- 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

- 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