formulas(sos).
all y all z ((Object(y) & Object(z)) -> (exists x (Object(x) & Ex1At(A,x,W) & (all F (Property(F) -> (Enc(x,F) <-> Enc(y,F) | Enc(z,F))))))).
all x all y ((Object(x) & Object(y)) -> (PartOf(x,y) <-> (Ex1At(A,x,W) & Ex1At(A,y,W) & (all F (Property(F) -> (Enc(x,F) -> Enc(y,F))))))).
all x (Object(x) -> (Situation(x) <-> (Ex1At(A,x,W) & (all F (Property(F) -> (Enc(x,F) -> (exists p (Proposition(p) & F=VAC(p))))))))).
end_of_list.