formulas(assumptions).

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

% Russell axiom for the description:
all F all x ((relation1(F) & object(x)) -> (is_the(x,F)  <-> (exemplifies1(F,x) & (all y (object(y) -> (exemplifies1(F,y) -> y=x)))))).

end_of_list.

formulas(goals).

% all F (relation1(F) -> ((exists y (object(y) & is_the(y,F))) -> (all z (object(z) -> (is_the(z,F) -> exemplifies1(F,z)))))). 

end_of_list.