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

formulas(sos).
% axioms for theorem 15
all p (Proposition(p) -> Proposition(~p)).

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

all x (Object(x) -> (Maximal1(x) <-> Situation(x) & (all p (Proposition(p) -> TrueIn(p,x)|TrueIn(~p,x))))).

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)).
end_of_list.