set(auto2).

formulas(sos).
all x (Situation(x)->Object(x)).
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 all y (Ex1At(A,x,W)&Ex1At(A,y,W)-> ((all F (Property(F)-> (Enc(x,F)<->Enc(y,F))))->x=y)).
end_of_list.

formulas(goals).
all s1 all s2 ((Situation(s1)&Situation(s2)) -> ((all p (Proposition(p)-> (TrueIn(p,s1)<->TrueIn(p,s2)))) ->s1=s2)).
end_of_list.