op(300,prefix,~). set(auto2). clear(fof_reduction). formulas(sos). % axioms for theorem 10 Point(W). all p (Proposition(p)->Proposition(~p)). 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 (Actual(x) -> Object(x)). % denial of theorem 10 -(all x (Situation(x)&Actual(x)-> -(exists p (Proposition(p)&TrueIn(p,x)&TrueIn(~p,x))))). end_of_list.