set(auto2).
set(print_initial_clauses).
set(print_given).
% set(print_gen).

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