% File ex5: Illustrate processing input formulas (instead of clauses).
% There is nothing to prove.

formulas(assumptions).

   (all x exists y (x * y = e & y * x = e)).

end_of_list.

formulas(goals).

   (all x (x * x = e)) -> (all x all y (x * y = y * x)).

end_of_list.

% After input processing ...
% 
%    formulas(sos).
%    x * f1(x) = e.  [clausify(1)].
%    f1(x) * x = e.  [clausify(1)].
%    x * x = e.  [deny(2)].
%    c2 * c1 != c1 * c2.  [deny(2)].
%    end_of_list.
