Graph Theory
1 abstract problem, 1 CNF problems
Smallest domain in the TPTP
Only propositional problem in mathematics
One problem from Tseitin,
GRA001-1.p
, that came from Pelletier's test set
An open area for ATP, and probably needs induction