set(auto2).
set(print_initial_clauses).
set(print_given).

formulas(sos).

% axioms for the lemma
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))))). 

% lemma
-(all x all G ((Object(x) & Property(G)) -> (IsTheFormOf(x,G) -> (all F (Property(F) -> (Enc(x,F) <-> Implies(G,F))))))).

end_of_list.