 Besides helping in the completion of the proof, the automated theorem provers were also very instrumental in the finding of some novel results. First, Gödel’s set of original assumptions was shown to be inconsistent by LEO-II by proving that self-difference becomes an essential property of every entity; a re-formulation of the definition of essence due to Dana Scott—this involved the addition of a missing conjunct, ϕX, in the definition—was shown by Nitpick to be consistent. Second, LEO-II and Satallax managed to prove C, T1 and T2 using only the logic system K and, moreover, Nitpick found a counter-model for T3 in K thus showing that more logical power is required to complete the rest of the proof. Third, using LEO-II and Satallax, it is shown that the logic system KB (system K with the Brouwer axiom) is sufficient to establish the necessity of God’s existence, □•∃•Xμ . gμ→σ X, which is a double-win for automated reasoning: a gain in logical economy, and the deeper philosophical result of having effectively dismissed a major criticism against Gödel’s proof, namely his use of the stronger logic system S5. Fourth, the authors also prove in KB that: