formulas(sos).

all p all q (Proposition(p)&Proposition(q)-> (VAC(p)=VAC(q)->p=q)).

all p (Proposition(p)<->Property(VAC(p))).

all x all d (Object(x)&Point(d)-> (SituationAt(x,d)<->Ex1At(A,x,d)& (all F (Property(F)-> (EncAt(x,F,d)-> (exists p (Proposition(p)&F=VAC(p)))))))).

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

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 p all d (Object(x)&Proposition(p)&Point(d)-> (EncpAt(x,p,d)<-> (exists F (Property(F)&F=VAC(p)&EncAt(x,F,d))))).

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

all d (Point(d)-> (exists x (Object(x)&Ex1At(A,x,d)& (all F (Property(F)-> (EncAt(x,F,d)<-> (exists p (Proposition(p)&True(p,d)&F=VAC(p))))))))).
end_of_list.