formulas(assumptions).

% Sorting
all x (Object(x) -> -Relation1(x)).
all x all F (Ex1(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) -> Ex1(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) -> Ex1(F,z)))))).

end_of_list.
