A Mechanically Verified, Efficient, Sound and Complete Theorem Prover For First Order Logicby Tom Ridge28 Sep