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.