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.