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.