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. formulas(goals). all x all y ((Object(x) & Object(y)) -> ((Situation(x) & Situation(y)) -> (exists z (Object(z) & Situation(z) & PartOf(x,z) & PartOf(y,z))))). end_of_list.