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