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))).

% Lemma1
all x all F all y ((object(x) & relation1(F) & object(y)) -> ((is_the(x,F)  & x=y) -> exemplifies1(F,y))).


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.