set(auto).

formulas(sos).

Property(A).
Point(W).
all x (Point(x) -> -Property(x)).
all F all G ((Property(F) & Property(G)) -> (Implies(F,G) <-> (all x all w (Point(w) -> (Ex1(F,x,w) -> Ex1(G,x,w)))))).
all x all G ((Object(x) & Property(G)) -> (IsAFormOf(x,G) <-> Ex1(A,x,W) & (all F (Property(F) -> (Enc(x,F) <-> Implies(G,F)))))).
all x all G ((Object(x) & Property(G)) -> (IsTheFormOf(x,G) <-> (IsAFormOf(x,G)  & (all y (IsAFormOf(y,G) -> y=x))))). 
all x all y ((Object(x) & Object(y)) -> (PartPH(x,y) <-> (exists F (Property(F) & IsTheFormOf(y,F) & Enc(x,F))))).

% Negation of right-to-left direction of theorem 4:
-(all x all y all G ((Object(x) & Object(y) & Property(G)) -> (IsTheFormOf(x,G) -> (PartPH(y,x) -> Enc(y,G))))).

end_of_list.

