op(300,prefix,~).
set(auto2).
clear(fof_reduction).

formulas(sos).
% axioms for theorem 18b
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)-> (Maximal1(x)<->Situation(x)& (all p (Proposition(p)->TrueIn(p,x)|TrueIn(~p,x))))).

all x (World(x)->Object(x)).

all x all y (Ex1At(A,x,W)&Ex1At(A,y,W)-> ((all F (Property(F)-> (Enc(x,F)<->Enc(y,F))))->x=y)).

all x (World(x)->Maximal1(x)).

Point(W).

all p (Proposition(p)->Proposition(~p)).

all d all p (Point(d)&Proposition(p)-> (True(~p,d)<-> -True(p,d))).

% denial of  theorem 18b
-(all x all y (World(x)&World(y)&Actual(x)&Actual(y)->x=y)).
end_of_list.
