set(auto2).

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

formulas(goals).
exists x (World(x)&Actual(x)).
end_of_list.