% This input file is for Otter 3.0.4.
%
% Lemma 2. If a Robbins algebra satisfies 
%
%     exists C exists D, n(C+D)=n(C),
%
% then it satisfies 
%
%     exists A exists B, A+B=A.
% 
% This is not a search.  It is a proof-check.  The steps of the
% proof are included in the "hints" list to lead Otter directly
% to the proof.  It takes only a few seconds.
%
% The purpose of this job is to construct a proof object that can
% be checked by the proof checker.

op(500, xfy, +).

assign(max_mem, 28000).

clear(print_kept).
clear(print_new_demod).
clear(print_back_demod).
% clear(print_given).

% assign(pick_given_ratio, 4).
assign(max_weight, 0).

set(build_proof_object).
set(para_from).
set(para_into).
set(order_eq).
clear(para_from_right).

% assign(max_proofs, -1).

list(usable).
x = x.
end_of_list.

list(sos).
x + y = y + x.
(x + y) + z = x + (y + z).
n(n(x + y) + n(x + n(y))) = x.        % Robbins axiom
n(C + D) = n(C).                      % hypothesis
end_of_list.

list(demodulators).
(x + y) + z = x + (y + z).
end_of_list.

list(passive).
x + y != x.                % Denial of lemma 2 condition
end_of_list.

assign(bsub_hint_wt, 0). set(keep_hint_subsumers).

list(hints).

x+y=y+x.
(x+y)+z=x+y+z.
n(n(x+y)+n(x+n(y)))=x.
n(C+D)=n(C).

x+y+z=y+x+z.
x+y+z=y+z+x.
x+y+z=z+x+y.
n(n(x+y)+n(y+n(x)))=y.
n(n(x+y)+n(n(y)+x))=x.
n(n(x+n(y))+n(x+y))=x.
n(D+C)=n(C).
n(n(x+y+z)+n(y+n(z+x)))=y.
n(n(C)+n(D+n(C)))=D.
n(n(x+y)+n(n(x)+y))=y.
n(n(x+y+z)+n(n(x+y)+z))=z.
n(n(n(x)+y)+n(y+x))=y.
n(n(n(x)+y)+n(x+y))=y.
n(n(n(n(x)+y)+x+y)+y)=n(n(x)+y).
n(n(n(C)+x)+n(x+D+C))=x.
n(n(n(C)+D)+n(C))=D.
n(n(x+n(n(x)+y)+y)+y)=n(n(x)+y).
n(n(n(n(x)+y)+x+y+y)+n(n(x)+y))=y.
n(n(D+C+n(n(C)+x)+x)+x)=n(n(C)+x).
n(n(x+D)+n(x+n(n(C)+D)+n(C)))=x.
n(n(n(n(x)+y)+n(x+y)+n(y+z)+z)+z)=n(n(n(n(x)+y)+n(x+y))+z).
n(n(n(n(n(x)+y)+x+y+y)+n(n(x)+y)+z)+n(y+z))=z.
n(n(C+n(n(C)+x)+x+D)+x)=n(n(C)+x).
n(n(n(n(x)+y)+n(x+y)+n(y+z)+z)+z)=n(y+z).
n(n(n(x+n(n(x)+y)+y+y)+n(n(x)+y)+z)+n(y+z))=z.
n(n(n(C)+D)+n(n(C+n(n(C)+D)+D+D)+n(n(C)+D)+n(C)))=n(C+n(n(C)+D)+D+D).
n(n(n(n(x)+n(C))+n(x+n(C))+D+n(D+n(C)))+n(D+n(C)))=n(n(C)+n(D+n(C))).
n(n(n(n(n(x)+y)+n(x+y)+n(y+z)+z)+z+u)+n(n(y+z)+u))=u.
n(n(n(x+n(n(x)+y)+y+y)+n(n(x)+y)+z)+n(z+y))=z.
n(n(n(n(x)+n(C))+n(x+n(C))+D+n(D+n(C)))+n(D+n(C)))=D.
n(n(n(n(n(x)+n(C))+n(x+n(C))+n(n(C)+D)+D)+D+n(C))+D)=n(C).
n(n(x+y)+n(n(z+n(n(z)+y)+y+y)+n(n(z)+y)+x))=x.
n(n(n(n(n(x)+n(C))+n(x+n(C))+D+n(D+n(C)))+D+n(C))+D)=n(n(n(x)+n(C))+n(x+n(C))+D+n(D+n(C))).
n(C+n(n(C)+D)+D+D)=n(C).
n(n(n(n(n(x)+n(C))+n(x+n(C))+n(D+n(C))+D)+D+n(C))+D)=n(n(n(x)+n(C))+n(x+n(C))+D+n(D+n(C))).
n(C+n(D+n(C))+D+D)=n(C).
n(n(n(n(n(x)+n(C))+n(x+n(C))+n(n(C)+D)+D)+D+n(C))+D)=n(n(n(x)+n(C))+n(x+n(C))+D+n(D+n(C))).
n(D+D+C+n(D+n(C)))=n(C).
n(n(n(x)+n(C))+n(x+n(C))+D+n(D+n(C)))=n(C).
n(n(D+D+C+n(D+n(C))+n(n(C)+x)+x)+x)=n(n(D+D+C+n(D+n(C)))+x).
n(n(n(C)+n(C))+n(D+C+n(C))+D+n(D+n(C)))=n(C).
n(n(D+D+C+n(D+n(C))+n(n(C)+x)+x)+x)=n(n(C)+x).
n(n(D+C+n(C))+n(n(C)+n(C))+D+n(D+n(C)))=n(C).
n(n(D+C+n(C)+n(n(C)+n(C))+D+n(D+n(C)))+n(C))=n(n(C)+n(C))+D+n(D+n(C)).
n(n(D+C+n(C)+D+n(n(C)+n(C))+n(D+n(C)))+n(C))=n(n(C)+n(C))+D+n(D+n(C)).
n(n(D+C+D+n(C)+n(n(C)+n(C))+n(D+n(C)))+n(C))=n(n(C)+n(C))+D+n(D+n(C)).
n(n(D+D+C+n(C)+n(n(C)+n(C))+n(D+n(C)))+n(C))=n(n(C)+n(C))+D+n(D+n(C)).
n(n(D+D+C+n(C)+n(D+n(C))+n(n(C)+n(C)))+n(C))=n(n(C)+n(C))+D+n(D+n(C)).
n(n(D+D+C+n(D+n(C))+n(n(C)+n(C))+n(C))+n(C))=n(n(C)+n(C))+D+n(D+n(C)).
n(n(C)+n(C))+D+n(D+n(C))=n(n(C)+n(C)).

end_of_list.