%%%%%%%%%%%%%%%%%%%%%  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).

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

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([A, B, 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.
 
%%%%%%%%%%%%%%%%%%%%%  Clauses

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

list(sos).
n(n(x + y) + n(x + n(y))) = x.       % Robbins axiom
c + d = c.                           % hypothesis
n(A + n(B)) + n(n(A) + n(B)) != B.   % denial of Huntington axiom
end_of_list.

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

