set(auto2).

formulas(sos).
Point(W).
Property(B).
all x (Object(x)  -> (all w (Point(w) -> (Ex1(B,x,w) <-> -Ex1(A,x,w))))).
exists x (Object(x) & Ex1(A,x,W) & (all F (Property(F) -> (Enc(x,F) <-> Implies(B,F))))).
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)))))).


% theorem 
all F all x (Property(F) & Object(x) -> (Enc(x,F) -> Ex1(F,x,W))).
end_of_list.
