formulas(sos). 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 (Object(x) -> (Actual(x) <-> (Situation(x) & all p (Proposition(p) -> (TrueIn(p,x) -> True(p,W)))))). all p all x ((Object(x) & Proposition(p)) -> (TrueIn(p,x) <-> Encp(x,p))). all x all p ((Object(x) & Proposition(p)) -> (Encp(x,p) <-> (exists F (Property(F) & F=VAC(p) & Enc(x,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))))))). Object(ALPHA) & Ex1At(A,ALPHA,W) & (all F (Property(F) -> (Enc(ALPHA,F) <-> (exists p (Proposition(p) & True(p,W) & F=VAC(p)))))). Actual(ALPHA). end_of_list. formulas(goals). all x (Object(x) -> (Situation(x) -> (Actual(x) <-> PartOf(x,ALPHA)))). end_of_list.