formulas(assumptions).

% Description Axiom:
all F all G all x ((relation1(F) & relation1(G) & object(x)) ->
 ((is_the(x,F) & exemplifies1(G,x)) <->
  (exists y (object(y) & exemplifies1(F,y) & (all z (object(z) -> (exemplifies1(F,z) -> z=y))) & exemplifies1(G,y))))).

end_of_list.

formulas(goals).

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

end_of_list.