PROVER9's Clausification of the Premises and Conclusion of the Ontological Argument

Description Theorem 1

-Relation1(x) | -Object(y) | -Ex1(x,y) | Object(f1(x,y)) | Object(f2(x)).
-Relation1(x) | -Object(y) | -Ex1(x,y) | Object(f1(x,y)) | Is_the(f2(x),x).
-Relation1(x) | -Object(y) | -Ex1(x,y) | Ex1(x,f1(x,y)) | Object(f2(x)). 
-Relation1(x) | -Object(y) | -Ex1(x,y) | Ex1(x,f1(x,y)) | Is_the(f2(x),x).
-Relation1(x) | -Object(y) | -Ex1(x,y) | f1(x,y) != y | Object(f2(x)). 
-Relation1(x) | -Object(y) | -Ex1(x,y) | f1(x,y) != y | Is_the(f2(x),x).

Description Theorem 2

-Relation1(x) | -Object(y) | -Is_the(y,x) | -Object(z) | -Is_the(z,x) | Ex1(x,z). 

Sorting on Is_the

-Is_the(x,y) | Relation1(y).
-Is_the(x,y) | Object(x). 

Definition of none_greater

-Object(x) | -Ex1(none_greater,x) | Ex1(conceivable,x).
-Object(x) | -Ex1(none_greater,x) | -Object(y) | -Ex2(greater_than,y,x) | -Ex1(conceivable,y).
-Object(x) | Ex1(none_greater,x) | -Ex1(conceivable,x) | Object(f3(x)).
-Object(x) | Ex1(none_greater,x) | -Ex1(conceivable,x) | Ex2(greater_than,f3(x),x).
-Object(x) | Ex1(none_greater,x) | -Ex1(conceivable,x) | Ex1(conceivable,f3(x)).

Premise 1

Object(c1).
Ex1(none_greater,c1). 

Lemma 2

-Object(x) | -Ex1(none_greater,x) | Object(c2).
-Object(x) | -Ex1(none_greater,x) | Ex1(none_greater,c2).
-Object(x) | -Ex1(none_greater,x) | -Object(y) | -Ex1(none_greater,y) | c2 = y.

Premise 2

 
-Object(x) | -Is_the(x,none_greater) | Ex1(e,x) | Object(f4(x)).
-Object(x) | -Is_the(x,none_greater) | Ex1(e,x) | Ex2(greater_than,f4(x),x). 
-Object(x) | -Is_the(x,none_greater) | Ex1(e,x) | Ex1(conceivable,f4(x)).

Definition of God

Is_the(g,none_greater).

Negation of the Conclusion

-Ex1(e,g).