A Formalization of the SCL(FOL) Calculus: Simple Clause Learning for First-Order Logic by Martin Desharnais Apr 20