formulas(sos).
Proposition(L).
all p (Proposition(p) -> Proposition(NEG(p))).
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)-> (Maximal1(x)<->Situation(x)& (all p (Proposition(p)->TrueIn(p,x)|TrueIn(NEG(p),x))))).
all x (Object(x) -> (Partial1(x) <-> -Maximal1(x))).
exists x (Object(x) & Ex1At(A,x,W) & (all F (Property(F) -> (Enc(x,F) <-> F!=F)))).
end_of_list.

formulas(goals).
exists x (Situation(x) & Partial1(x)).
end_of_list.
