- 14 abstract problems, 23 CNF problems
- One axiomatization from Tom Jech [Jec93]
- Mostly non-Horn problems with some equality

- 41 abstract problems, 47 CNF problems
- Two axiomatizations
- One from [MOW76]
- Equality axiomatization from Bill McCune

- Predominance of UEQ problems
- Includes "SAM's Lemma", an open problem of Bumcroft, solved by ATP, e.g.,
`LAT005-3.p`