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

formulas(sos).
% axioms for theorem 22
Point(W).

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

all p all d all x (Object(x)&Proposition(p)&Point(d)-> (Ex1At(VAC(p),x,d)<->True(p,d))).

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

all x (Object(x)-> (Actual(x)<->Situation(x)& (all p (Proposition(p)-> (TrueIn(p,x)->True(p,W)))))).

all x (Object(x)-> (World(x)<->Situation(x)& (exists y (Point(y)& (all p (Proposition(p)-> (TrueIn(p,x)<->True(p,y)))))))).

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

World(ALPHA)&Actual(ALPHA)& (all x (Actual(x)&World(x)->x=ALPHA)).

% denial of theorem 22
-(all p (Proposition(p)-> (TrueIn(p,ALPHA)<->Ex1At(VAC(p),ALPHA,W)))).
end_of_list.