set(auto2).
clear(fof_reduction).

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

all x (Object(x) -> (Situation(x) <-> Ex1(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) <-> Ex1(A,x,W)&Ex1(A,y,W)& (all F (Property(F) -> (Enc(x,F) -> Enc(y,F)))))).

all x all y (Ex1(A,x,W) & Ex1(A,y,W)-> ((all F (Property(F) -> (Enc(x,F) <-> Enc(y,F)))) -> x=y)).

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