set(auto2).

formulas(sos).
Point(W).
True(T,W).
Proposition(L).
-True(L,W).
all p (Proposition(p)<->Property(VAC(p))).
all x all p (Object(x)&Proposition(p)-> (Encp(x,p)<-> (exists F (Property(F)&F=VAC(p)&Enc(x,F))))).
all p all d all x (Object(x)&Proposition(p)&Point(d)-> (Ex1At(VAC(p),x,d)<->True(p,d))).
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))))))).
exists x (Object(x)&Ex1At(A,x,W)& (all F (Property(F)-> (Enc(x,F)<->F=VAC(T))))).
exists x (Object(x)&Ex1At(A,x,W)& (all F (Property(F)-> (Enc(x,F)<->F=VAC(L))))).
end_of_list.

formulas(goals).
(exists x (Situation(x)&Actual(x))) & (exists y (Situation(y) & -Actual(y))).
end_of_list.