formulas(assumptions).

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 equality:
all F all x all w ((relation1(F) & object(x) & object(w)) -> 
        ((is_the(x,F) & x=w) <-> 
                (exists y (object(y) & exemplifies1(F,y) & (all z (object(z) -> (exemplifies1(F,z) -> z=y))) & y=w)))).

end_of_list.

formulas(goals).

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

end_of_list.