% File ex2.in: Illustrate some of the kinds of options that are available.

set(paramodulation).       % inference rules
clear(input_sos_first).    % control search
set(print_kept).           % output
assign(max_seconds, 30).   % limits
lex([a,b]).                % term ordering (rewriting)

formulas(assumptions).

   % identity
   e * x = x.
   x * e = x.

   % inverse
   x' * x = e.
   x * x' = e.

   % associativity
   (x * y) * z = x * (y * z).

   % denial of the theorem
   x * x = e.
   b * a != a * b.

end_of_list.
