A Mechanically Verified, Efficient, Sound and Complete Theorem Prover For First Order Logic by Tom Ridge Sep 28