% This input file is for Otter 3.0.4.
%
% Lemma 1. If a Robbins algebra satisfies 
%
%     exists C exists D, C+D=C,
%
% then it satisfies 
%
%     exists A, A+A=A.
% 
% This is a heavily restricted search which takes about 25 minutes on a
% SPARC 5.
%
% The purpose of this job is to construct a proof object that can
% be checked by the proof checker.

op(500, xfy, +).

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

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

set(knuth_bendix).
set(build_proof_object).

assign(max_weight, 30).
clear(eq_units_both_ways).
set(dynamic_demod_lex_dep).
assign(max_distinct_vars, 3).
assign(pick_given_ratio, 3).
lex([C, D, n(x), x+x]).

weight_list(purge_gen).

weight($(0) + ($(0) + ($(0) + $(0))),500).
weight(n(n($(0))), 500).

weight(n(x+x) = $(0), 500).
weight(n(x+C) = $(0), 500).
weight(n(C+x) = $(0), 500).
weight(n(x+D) = $(0), 500).
weight(n(D+x) = $(0), 500).

weight($(0) = $(0)+  ($(0)+$(0)), 500).

weight($(0) = n($(0)+  ($(0)+$(0))), 500).
weight($(0) = n($(0)+ n($(0)+$(0))), 500).
weight($(0) = n(n($(0)+$(0))+$(0)), 500).
end_of_list.

weight_list(pick_given).
weight($(1) = $(2), 1).
end_of_list.
 

list(usable).
x = x.
x + y = y + x.
(x + y) + z = x + (y + z).
x + (y + z) = y + (x + z).   % AC helper
end_of_list.

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

list(passive).
x + x != x.         % denial of a sufficient condition (see RBA-2)
end_of_list.