set(auto2).
clear(quiet).
set(print_given).

formulas(sos).
% axioms for theorem 7
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 7 (takes 15000 seconds w/out fof_reduction)
% with fof_reduction, it takes a second or two!  But, fof_reduction
% does not work robustly on mac os X (strange bug!)
-(all x (Situation(x)->PartOf(x,x)) &
(all x all y (Situation(x)&Situation(y) -> (PartOf(x,y)&x!=y-> -PartOf(y,x))) &
(all x all y all z (Situation(x)&Situation(y)&Situation(z)-> (PartOf(x,y)&PartOf(y,z)->PartOf(x,z)))))).
end_of_list.