formulas(sos).

% Every proposition has a negation
all p (Proposition(p) -> Proposition(NEG(p))).

% NEG(p) is True wrt point d iff not-(p is True wrt d)
all d all p (Point(d) & Proposition(p) -> (True(NEG(p),d) <-> -True(p,d))).

% Definition of Maximal1.
all x (Object(x) -> (Maximal1(x) <-> Situation(x) & (all p (Proposition(p) -> TrueIn(p,x)|TrueIn(NEG(p),x))))).

% Definition of World.
all x (Object(x) -> (World(x) <-> Situation(x) & (exists y (Point(y) & (all p (Proposition(p) -> (TrueIn(p,x)<->True(p,y)))))))).

% Sorting on Worlds
all x (World(x) -> Object(x)).

end_of_list.

formulas(goals).
all x (World(x) -> Maximal1(x)).
end_of_list.