%%%%%%%%%%%%%%%%%%%%%  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, 28).
lex([1,A,B,C,_*_,_+_,_@,p(_,_,_)]).

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

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

list(sos).
(x + y) * y = y.
x * (y + z) = (x * y) + (x * z).
x + x@ = 1.

p(x,y,z) = (x*y@) + ((x*z) + (y@ * z)).
p(x,x,y) = y.
p(x,y,y) = x.
p(x,y,x) = x.

end_of_list.

% weight_list(pick_and_purge).
% weight(A, 0).
% weight(B, 0).
% weight(C, 0).
% end_of_list.

% End of ordinary input (which includes preceding weight_list) which
% gives a proof of length 135 in 92 seconds.  The following was contributed
% by Larry Wos and leads quickly to a proof of length 78.

assign(max_weight, 8).

weight_list(pick_and_purge).
weight(A, 0).
weight(B, 0).
weight(C, 0).
% Following are the positive deduced steps of temp.wos.dualba2.test.out15,
% 73 of them from a proof listed as of length 78.
weight(1*x@ =x@ ,4).
weight(x@ + (1*y)=1* (x@ +y),4).
weight(x+ ((y+x)*z)= (y+x)* (x+z),4).
weight(((x+y)*z)+y= (x+y)* (z+y),4).
weight((x* (y+z))* (x*z)=x*z,4).
weight(1* (x@ +y@ )=x@ +y@ ,4).
weight(1*1=1,4).
weight((x+y)* (y+y)=y+y,4).
weight(((x+y)* (z+y))*y=y,4).
weight(((x+y@ )*1)*y@ =y@ ,4).
weight(1* (x@ +1)=x@ +1,4).
weight((1* (x+1))*1=1,4).
weight((1*x)+1=1* (x+1),4).
weight((1* (x+1))* (1+1)=1+1,4).
weight(1@ + (1+ (1@ *1))=1,4).
weight(x@ + (((y+x@ )*x)+ (x@ *x))=y+x@ ,4).
weight(x@ * (x@ + (x+x))=x@ ,4).
weight((x*y)+ ((x*z)+ (z@ *z))=x* (y+ ((x*z)+ (z@ *z))),4).
weight(x* ((x*y)+ (y@ *y))= (x*y)+ (y@ *y),4).
weight(x* (y@ + ((x*y)+ (y@ *y)))=x,4).
weight((x@ *y)+x@ =x@ * (y+ (x@ + (x+x))),4).
weight(1* (x+1)=1,4).
weight(1+1=1,4).
weight(x@ +1=1,4).
weight(1@ *1=1@ ,4).
weight((x+1@ )*1=x+1@ ,4).
weight(x* (1@ + ((x*1)+1@ ))=x,4).
weight(x* ((x*1)+1@ )= (x*1)+1@ ,4).
weight(1@ +1@ =1@ ,4).
weight(1@ * (x+1@ )=1@ * (x+1),4).
weight(1@ + (x+1@ )=x+1@ ,4).
weight((x*1)+1@ =x,4).
weight(x*x=x,4).
weight(x+1=1,4).
weight(1@ * (x+1@ )=1@ ,4).
weight(1@ +x=x,4).
weight(x*1=x,4).
weight(x*1@ =1@ ,4).
weight(x+1@ =x,4).
weight(1@ *x=1@ ,4).
weight((x*y)+x=x* (y+x),4).
weight(x+ (x*y)=x* (x+y),4).
weight(x* (y+x)=x,4).
weight(x* (x+y)=x* (1+y),4).
weight((x*y)+x=x,4).
weight(x* (1+x@ )=x,4).
weight(x*x@ =1@ ,4).
weight(x@ *x=1@ ,4).
weight(x* ((y+x)+z)=x* (x+z),4).
weight(x@ @ =x,4).
weight((x*y)+ (x@ *y)=y,4).
weight(1@ =x*x@ ,4).
weight(x@ * (y+x)=x@ *y,4).
weight(x@ * (x+y)=x@ *y,4).
weight((x* (1+y))+ (x@ *y)=x+y,4).
weight(x*x@ =y*y@ ,4).
weight(x@ * ((y+x)+z)=x@ * (y+z),4).
weight(1+x=1,4).
weight(x* (x+y)=x,4).
weight(x+ (x@ *y)=x+y,4).
weight(x* ((y+x)+z)=x,4).
weight(x+ (x*y)=x,4).
weight((x+y)+z=y+ (x+z),4).
weight(x+ (x+y)=x+y,4).
weight((x*y)+y=y,4).
weight(x+ ((y*x)+z)=x+z,4).
weight(x+ (y*x)=x,4).
weight(x+ (y* (x+z))=x+ (y*z),4).
weight((x*y)+ (y*z)=y* ((x*y)+z),4).
weight((x*y)+ (z*x)=x* (y+ (z*x)),4).
weight(x+ ((x+y)*z)= (x+y)* (x+z),4).
weight(x*y=y*x,4).
weight(x+ (y*z)= (x+z)* (x+y),4).
end_of_list.