set(auto2).
clear(fof_reduction).

formulas(sos).
% axioms for theorem 17
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)).

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

% denial of theorem 17
-(all x (World(x)->Possible(x))).
end_of_list.