op(400, xfx, +).
op(300, fy, ~).

set(knuth_bendix).
assign(pick_given_ratio, 3).

set(hyper_res).  set(unit_deletion).
assign(neg_weight, -10).

assign(max_mem, 200000).
assign(max_weight, 30).
% assign(max_seconds, 120).

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

list(usable).
x = x.

% Denial of the Robbins basis.

B + A != A + B
   | (A + B) + C != A + (B + C)
   | ~ (~ (A + B) + ~ (~ A + B)) != B
   | $Ans(Robbins_basis).

end_of_list.

list(sos).

% Each of the following 10 equations is a single axiom for
% Boolean algebra in terms of {OR,NOT}.  In particular,
% each is equivalent to the Robbins basis.
% 
% It's easy to check that these are valid in Boolean algebra.
% To prove completeness, we derive the Robbins basis.

% This input file should work for all but the first of these axioms.

  ~ (~ (x + y) + ~ z) + ~ (~ (~ u + u) + (~ z + x)) = z.    % 13345 685 sec
% ~ (~ (~ (x + y) + z) + ~ (x + ~ (~ z + ~ (z + u)))) = z.  % 20615   6 sec
% ~ (~ (x + y) + ~ z) + ~ (x + ~ (z + ~ (~ z + u))) = z.    % 20629  19 sec
% ~ (~ (x + y) + ~ (~ (x + z) + ~ (~ y + ~ (y + u)))) = y.  % 20775  18 sec
% ~ (x + ~ y) + ~ (~ (x + z) + ~ (y + ~ (~ y + u))) = y.    % 20787  80 sec
% ~ (~ (x + y) + ~ (~ (~ y + ~ (z + y)) + ~ (x + u))) = y.  % 24070  28 sec
% ~ (x + ~ y) + ~ (~ (y + ~ (z + ~ y)) + ~ (x + u)) = y.    % 24086  44 sec
% ~ (~ (x + y) + ~ (~ (~ y + ~ (z + y)) + ~ (u + x))) = y.  % 24412  40 sec
% ~ (x + ~ y) + ~ (~ (y + ~ (z + ~ y)) + ~ (u + x)) = y.    % 24429  36 sec
% ~ (~ (~ (x + y) + z) + ~ (~ (~ z + ~ (u + z)) + y)) = z.  % 24970  47 sec

end_of_list.

% Include the following line to get a proof for 13345.
%
assign(max_weight, 42). assign(change_limit_after, 100). assign(new_max_weight, 22).
