% When we run this in prover9, we get a proof, but then it does another
% search and fails...why?

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

% Russell axiom for the description: [UNUSED]
% 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 x (object(x) & is_the(x,F))) -> (all y (object(y) -> (is_the(y,F) -> exemplifies1(F,y)))))).

end_of_list.