formulas(assumptions).

% Description Theorem 1
all F (Relation1(F) -> ((exists y (Object(y) & Ex1(F,y) & (all z (Object(z) -> (Ex1(F,z) -> z=y))))) -> (exists u (Object(u) & Is_the(u,F))))).

% Description Theorem 2
all F (Relation1(F) -> ((exists x (Object(x) & Is_the(x,F))) -> (all y (Object(y) -> (Is_the(y,F) -> Ex1(F,y)))))).

% Sorting on Is_the 
all x all F (Is_the(x,F) -> (Relation1(F) & Object(x))).

% Def: none_greater
all x (Object(x) -> (Ex1(none_greater,x) <-> 
	(Ex1(conceivable,x) & 
		-(exists y (Object(y) & Ex2(greater_than,y,x) &
			Ex1(conceivable,y)))))).

% The following is not used in this file, but was used
% in the subproof of Lemma 2.
% Connectedness of Greater Than
% all x all y ((Object(x) & Object(y)) ->
%  (Ex2(greater_than,x,y) | Ex2(greater_than,y,x) | x=y)).

% Premise 1
exists x (Object(x) & Ex1(none_greater,x)).

% Lemma 2 
exists x (Object(x) & Ex1(none_greater,x)) ->
	exists x (Object(x) & Ex1(none_greater,x) & (all y (Object(y) -> (Ex1(none_greater,y) -> y=x)))).

% Premise 2
all x (Object(x) -> ((Is_the(x,none_greater) & -Ex1(e,x)) -> 
	exists y (Object(y) & Ex2(greater_than,y,x) & Ex1(conceivable,y)))).

% Definition of God
Is_the(g,none_greater).

end_of_list.

formulas(goals).

Ex1(e,g).

end_of_list.