set(auto2).
clear(fof_reduction).

formulas(sos).
% axioms for theorem 11
Proposition(L).

-True(L,W).

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 11
-(exists p (Proposition(p) & (all x (Situation(x)&Actual(x)-> -TrueIn(p,x))))).
end_of_list.