formulas(assumptions).

% Typing 
all x (object(x) -> -relation1(x)).
all x (object(x) -> -relation2(x)).
all F (relation1(F) -> -relation2(F)).
all x all F (exemplifies1(F,x) -> (relation1(F) &  object(x))).
all x all y all R (exemplifies2(R,x,y) -> (relation2(R) & object(x) & object(y))).
all x all F (is_the(x,F) -> (relation1(F) & object(x))).

% Typing on Constants
relation1(e).
relation1(conceivable).
relation1(nonegreater).
relation2(greaterthan).

% Def: nonegreater
all x (object(x) -> (exemplifies1(nonegreater,x) <-> 
	(exemplifies1(conceivable,x) & 
		-(exists y (object(y) & exemplifies2(greaterthan,y,x) &
			exemplifies1(conceivable,y)))))).

% Premise 1
exists x (object(x) & exemplifies1(nonegreater,x)).

% Lemma 2 
exists x (object(x) & exemplifies1(nonegreater,x)) ->
	exists x (object(x) & exemplifies1(nonegreater,x) & (all y (object(y) -> (exemplifies1(nonegreater,y) -> y=x)))).

% Instance of Description Theorem 1
% exists x (object(x) & exemplifies1(nonegreater,x) & (all y (object(y) -> (exemplifies1(nonegreater,y) -> y=x)))) ->
% exists y (object(y) & is_the(y,nonegreater)).

% General formulation of Description Theorem 1
all F (relation1(F) -> ((exists x (object(x) & exemplifies1(F,x) & (all y (object(y) -> (exemplifies1(F,y) -> y=x))))) -> (exists x (object(x) & is_the(x,F))))).

% Description Theorem 2
all F (relation1(F) -> ((exists x (object(x) & is_the(x,F))) -> (all y (object(y) -> (is_the(y,F) -> exemplifies1(F,y)))))).

% Instance of Description Theorem 2
% all x (object(x) -> (is_the(x,nonegreater) -> exemplifies1(nonegreater,x))).

% Premise 2
all x (object(x) -> ((is_the(x,nonegreater) & -exemplifies1(e,x)) -> 
	exists y (object(y) & exemplifies2(greaterthan,y,x) & exemplifies1(conceivable,y)))).

% Definition god
% all x (object(x) -> (is_the(x,nonegreater) -> x=g)). 
is_the(g,nonegreater).

end_of_list.

formulas(goals).         % to be negated and placed in the sos list

% exemplifies1(e,g).

end_of_list.