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.