%%%%%%%%%%%%%%%%%%%%%  Basic options

op(400, xfx, [*,+,^,v,/,\,#]).  % infix operators
op(300,yf,@).                   % postfix operator

clear(print_kept).
clear(print_new_demod).
clear(print_back_demod).

assign(pick_given_ratio, 4).
assign(max_mem, 20000).

%%%%%%%%%%%%%%%%%%%%%  Standard for equational problems

set(knuth_bendix).
set(build_proof_object).

%%%%%%%%%%%%%%%%%%%%%  Standard options for hyperresolution

set(output_sequent).
set(hyper_res).
set(order_history).
set(unit_deletion).
set(para_from_units_only).
set(para_into_units_only).

%%%%%%%%%%%%%%%%%%%%%  Modifications to strategy

assign(max_weight, 23).

%%%%%%%%%%%%%%%%%%%%%  Clauses

list(usable).
x = x.
(A * B) + (A * C) != A * (B + C) | (A + B) * B != B | B + B@ != A + A@.
end_of_list.

list(sos).

y + (x * (y * z)) = y.         % L1
((x * y) + (y * z)) + y = y.   % L3
(x + y) * (x + y@) = x.        % B1

y * (x + (y + z)) = y.         % L2
((x + y) * (y + z)) * y = y.   % L4
(x * y) + (x * y@) = x.        % B2

% lemmas

x + y = y + x.
x * y = y * x.
(x + y) + z = x + (y + z).
(x * y) * z = x * (y * z).
end_of_list.

% This is the end of the ordinary input, which gets a proof of length 119
% in about 80 seconds (on gyro).  Including  rest of the file causes Otter
% to find a 17-step proof in just a few seconds.  The hints are from
% a proof of distributivity found be the prototype equational prover
% in "basic" paramodulation mode.

assign(bsub_hint_wt, 0).
clear(para_into_units_only).

list(hints).
x + (y * x) = x.
x * (y + x) = x.
x + (x * y) = x.
x * (y * (z + x)) = x * y.
x + (y + x) = x + y.
x + ((y * x) + z) = x + z.
x * (y * z) = z * (x * y).
(x * (y * z)) + (x * (y * z@ )) = x * y.
(x + y) * ((x + y@ ) * z) = x * z.
(x + y) * (y + x) = x + y.
-((A * B) + (C * A) = A * (B + C)).
(x + y) * (z * (y + x)) = (x + y) * z.
(x + y) * (z * y) = z * y.
x * (y + z) = (z + y) * x.
(x * y) + (z * (x * y@ )) = (x * y) + (z * x).
(x + y) * (z * y@ ) = x * (z * y@ ).
(x * y) + (z * x) = (z + y) * x.
-((A * B) + (C * A) = (C + B) * A).
end_of_list.
