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