formulas(sos).

all x all d ((Object(x) & Point(d)) -> (WorldAt(x,d) <-> 
  (SituationAt(x,d) & (exists d2 (Point(d2) & (all p (Proposition(p) -> (TrueInAt(p,x,d2) <-> True(p,d2))))))))).

all x all d (WorldAt(x,d) -> Object(x) & Point(d)).

all x all p ((Object(x) & Proposition(p)) ->
 ((exists d (Point(d) & TrueInAt(p,x,d))) -> (all d (Point(d) -> TrueInAt(p,x,d))))).

all p (NecessarilyTrue(p) <-> (all d (Point(d) -> True(p,d)))).

Point(W).

all x (World(x) <-> WorldAt(x,W)).

all x all p (TrueIn(p,x) <-> TrueInAt(p,x,W)).

end_of_list.