formulas(assumptions). % Def: none_greater all x (Object(x) -> (Ex1(none_greater,x) <-> (Ex1(conceivable,x) & -(exists y (Object(y) & Ex2(greater_than,y,x) & Ex1(conceivable,y)))))). % Sorting on none_greater Relation1(none_greater). % Premise 1 exists x (Object(x) & Ex1(none_greater,x)). % Premise 2 (- (exists x(Object(x) & Is_the(x,none_greater) & Ex1(e,x)))) -> (all x ((Object(x) & Is_the(x, none_greater)) -> exists y (Object(y) & Ex2(greater_than,y,x) & Ex1(conceivable,y)))). % Lemma 2 exists x (Object(x) & Ex1(none_greater,x)) -> exists x (Object(x) & Ex1(none_greater,x) & (all y (Object(y) -> (Ex1(none_greater,y) -> Ex2(id,y,x))))). % Unique Exemplification Axiom all x all F ((Object(x) & Relation1(F)) -> (Is_the(x,F) <-> (Ex1(F,x) & (all z ((Object(z) & Ex1(F,z)) -> Ex2(id,x,z)))))). % Bridge Principle all x all y ((Object(x) & Object(y)) -> (Ex2(id,x,y) <-> x=y)). end_of_list. formulas(goals). exists x (Object(x) & Is_the(x, none_greater) & Ex1(e,x)). end_of_list.