%==============================================================================

set(binary_res).

formula_list(sos).
 all x (P(x) -> Q(x)).
 P(a).
 all z (Q(z) -> $ANS(z)).
end_of_list.

%==============================================================================
