set(auto2).
clear(fof_reduction).

formulas(sos).
% axioms for theorem 8
all x (Situation(x)->Object(x)).

all x all p (Object(x)&Proposition(p)-> (Encp(x,p)<-> (exists F (Property(F)&F=VAC(p)&Enc(x,F))))).

all p all x (Object(x)&Proposition(p)-> (TrueIn(p,x)<->Encp(x,p))).

all x all y (Object(x)&Object(y)-> (PartOf(x,y)<->Ex1At(A,x,W)&Ex1At(A,y,W)& (all F (Property(F)-> (Enc(x,F)->Enc(y,F)))))).

all p (Proposition(p)-> (Persistent(p)<-> (all x (Situation(x)&TrueIn(p,x)-> (all y (Situation(y)&PartOf(x,y)->TrueIn(p,y))))))).

% denial of theorem 8
-(all x (Proposition(x)->Persistent(x))).
end_of_list.