set(auto2).

formulas(sos).
% axioms for theorem 3
all x all y (PartOf(x,y)->Object(x)&Object(y)).

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

% denial of theorem 3
-(all x all y (Situation(y)&PartOf(x,y)->Situation(x))).
end_of_list.


