set(auto2).
clear(fof_reduction).

formulas(sos).
% axioms for theorem 14a
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 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) -> (Maximal2(x) <-> (Situation(x) & (all p (Proposition(p) -> TrueIn(p,x)))))).

exists x (Object(x) & Ex1At(A,x,W) & (all F (Property(F) -> (Enc(x,F) <-> (exists p (Proposition(p) & F=VAC(p))))))).

% denail of theorem 14a
-(exists x (Situation(x) & Maximal2(x))).
end_of_list.