set(auto2).
clear(fof_reduction).

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

all x (Object(x) -> (Situation(x) <-> Ex1At(A,x,W) & (all F (Property(F) -> (Enc(x,F) -> (exists p (Proposition(p) & F=VAC(p)))))))).

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

% denial of theorem 4
-(all x all y ((Situation(x) & Situation(y)) -> (PartOf(x,y)  <-> (all p (Proposition(p) -> (TrueIn(p,x) -> TrueIn(p,y))))))).
end_of_list.