Versions of the ontological argument have formed an important thread in recent work employing theorem provers, both because of their inherent interest and the technical challenges they bring with them. Prover9 and Mace have again been used recently by Jack Horner in order to analyze a version of the ontological argument in Spinoza’s Ethics (found invalid) and to propose an alternative (Horner 2019). Significant work has been done on versions of Anselm’s ontological argument (Oppenheimer & Za