formulas(assumptions).

% Definition of Nonegreater
all x (Object(x) -> (Ex1(none_greater,x) <->
        (Ex1(conceivable,x) &
                -(exists y (Object(y) & Ex2(greater_than,y,x) &
                        Ex1(conceivable,y)))))).

% Connectedness of Greater Than
all x all y ((Object(x) & Object(y)) -> (Ex2(greater_than,x,y) | Ex2(greater_than,y,x) |  x=y)).

end_of_list.

formulas(goals).

exists x (Object(x) & Ex1(none_greater,x)) ->
	exists x (Object(x) & Ex1(none_greater,x) & (all y (Object(y) -> (Ex1(none_greater,y) -> y=x)))).

end_of_list.