formulas(sos).

all p (Proposition(p) -> Proposition(NEG(p))).

all d all p (Point(d) & Proposition(p) -> (True(NEG(p),d) <-> -True(p,d))).

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

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

all x (World(x) -> Object(x)).

end_of_list.