set(auto2).
assign(nest_penalty,10).
assign(skolem_penalty,1).
assign(max_weight,29).
assign(max_vars,1).

formulas(usable).
% axioms for theorem 12
all y all z ((Object(y) & Object(z)) -> (exists x (Object(x) & Ex1(A,x,W) & (all F (Property(F) -> (Enc(x,F) <-> Enc(y,F) | Enc(z,F))))))).
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 (Object(x) -> (Situation(x) <-> (Ex1(A,x,W) & (all F (Property(F) -> (Enc(x,F) -> (exists p (Proposition(p) & F=VAC(p))))))))).
end_of_list.

formulas(sos).
% denial of theorem 12
-(all x all y ((Object(x) & Object(y)) -> ((Situation(x) & Situation(y)) -> (exists z (Object(z) & Situation(z) & PartOf(x,z) & PartOf(y,z)))))).
end_of_list.