 that is, that God is flawless and that monotheism holds, respectively. At this point, it would be fair to say that any of these results would be enough to vindicate the application of automated reasoning in exact philosophy. Now, for the bad news followed by good news: Fifth, the formula sσ ⊃• □•sσ can also be formally derived which is unfortunate since it implies that there are no contingent truths and that everything is determined, i.e. there is no free will. However, the issue has been addressed by follow-up work based on Fitting’s and Anderson’s variants of the ontological argument (Fuenmayor &amp; Benzmüller 2017, Fitting 2002, Anderson 1990). 