Satisfiability,
Revisited

Most formulas are not in CNF. With recursion, this is not a problem.