set(auto2).
clear(fof_reduction).

formulas(sos).
% axioms for theorem 6
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 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 x all y (Ex1At(A,x,W) & Ex1At(A,y,W) -> ((all F (Property(F) -> (Enc(x,F) <-> Enc(y,F)))) -> x=y)).

% denial of theorem 6
-(all x all y ((Object(x) & Object(y)) -> ((Situation(x)&Situation(y)) -> ((all z (Situation(z)-> (PartOf(z,x)<->PartOf(z,y)))) ->x=y)))).

end_of_list.