formulas(assumptions). 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))). % 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) & Ex1(F,y) & (all z (Object(z) -> (Ex1(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) -> Ex1(F,y))). end_of_list.