formulas(assumptions).

% Definition of Nonegreater
all x (object(x) -> (exemplifies1(nonegreater,x) <->
        (exemplifies1(conceivable,x) &
                -(exists y (object(y) & exemplifies2(greaterthan,y,x) &
                        exemplifies1(conceivable,y)))))).

% Connectedness of Greater Than
all x all y ((object(x) & object(y)) -> (exemplifies2(greaterthan,x,y) | exemplifies2(greaterthan,y,x) |  x=y)).

end_of_list.

formulas(goals).

exists x (object(x) & exemplifies1(nonegreater,x)) ->
	exists x (object(x) & exemplifies1(nonegreater,x) & (all y (object(y) -> (exemplifies1(nonegreater,y) -> y=x)))).

end_of_list.