- 285 abstract problems, 309 CNF problems
- Four axiomatizations
- Two older ones [LS74]
- Two built on NBG set theory [BL+86][Qua92]

- Those based on the NBG have the same properties ...
- Very general problems, some equality, CNF ones are non-Horn
- Hard challenges

- 5 abstract problems, 19 CNF problems
- Second smallest mathematics domain in the TPTP
- Two axiomatization, all developed at ANL
- One old one [MOW76]
- One by Bledsoe [BL90]

- Mixture of problems
- With and without equality
- Horn and non-Horn

- Includes the Intermediate Value Theorem, e.g.,
`ANA002-1.p`

and "the sum of two continuous functions is continuous", e.g.,`ANA005-3.p`