- 19 abstract problems, 24 CNF problems
- One axiomatization, from Wick and McCune
- Bill told me the axioms are not complete
- Mostly non-theorems (possibly as a result)

- Problems have no equality

- 151 abstract problems, 73 FOF problems, 238 CNF problems
- Four axiomatizations
- Two Tarskian, developed at ANL
- One Hilbert, from Dan Benanav
- One for curves and trajectories, from Lars Kulik

- Problems have some equality
- FOF problems based on Kulik's axioms
- Many CNF problems with some equality, non-Horn

- Good range of difficulties - nice test problems