formulas(sos). Point(W). all p (Proposition(p)<->Property(VAC(p))). all F all x (Property(F)&Object(x)<->Proposition(PLUG(F,x))). all p all d all x (Object(x)&Proposition(p)&Point(d)-> (Ex1At(VAC(p),x,d)<->True(p,d))). all x all F all d (Object(x)&Property(F)&Point(d)-> (True(PLUG(F,x),d)<->Ex1At(F,x,d))). all x (World(x)->Object(x)). World(ALPHA)&Actual(ALPHA)& (all x (Actual(x)&World(x)->x=ALPHA)). all p (Proposition(p)-> (TrueIn(p,ALPHA)<->Ex1At(VAC(p),ALPHA,W))). end_of_list.