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

% See comments after clauses.
%
% assign(max_weight, 28).
% assign(max_mem, 28000).

%%%%%%%%%%%%%%%%%%%%%  Clauses
  
list(usable).
x = x.
end_of_list.

list(sos).

x * (y + z) = (x * y) + (x * z).
x + (y * z) = (x + y) * (x + z).
x + x@ = 1.
x * x@ = 0.

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

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

end_of_list.

list(passive).
(A + B) * B != B.
end_of_list.

% This file has been modified by Larry Wos so that a shorter 
% proof is found.  The original proof, found with the above
% commented-out commands, is 816 steps.
% The rest of the file reflects Larry's changes, and leads
% to a shorter, quicker proof.

assign(pick_given_ratio, 12).
set(ancestor_subsume).
assign(max_weight, 4).
assign(heat,3).
  
list(hot).
x * (y + z) = (x * y) + (x * z).
x + (y * z) = (x + y) * (x + z).
x + x@ = 1.
x * x@ = 0.
end_of_list.

%%%%%%%%%%%%%%%%%%%%%  Resonators, specially tuned to find a quick, short proof.

weight_list(pick_and_purge).
% Following are those of weight less or equal 10 from temp.wos.boolean.shorten.out100, proof of a2.
weight(0*1=0,1).
weight(0@ =1,1).
weight(0+1=1,1).
weight(1*1=1,1).
weight(1+1=1,1).
weight(0+0=0,1).
weight(1+0=1,1).
weight(1*0=0,1).
weight(1@ =0,1).
weight(x+0=x*1,1).
weight(x+x=x,1).
weight(x*x=x,1).
weight(0+x=x,1).
weight(1*x=x,1).
weight(x*1=x,1).
weight(x+1=1,1).
weight((x+y)*x=x,1).
weight((x*y)+x=x,1).
weight((x*y)+y=y,1).
%  Following are all proof steps from .out100 with wt02 for those used as demods and with back_demod in their history, proof of a2.
weight(((x*y)+x)* ((x*y)+z)=x* (y+z),4).
weight((x+ ((y*z)+y))* (x+ ((y*z)+u))= (x+y)* (x+ (z+u)),4).
weight((x+y)* (x+ (y@ +z))= (x+ (0+y))* (x+ (0+z)),4).
weight(x* (y+ (x@ +z))= ((x*y)+ (0+x))* ((x*y)+ (0+z)),4).
weight(((x*y)+ (0+x))* ((x*y)+ (0+z))=x* (y+ (x@ +z)),4).
weight((x+y)* (x+y@ )=x+0,4).
weight(x* (x@ +y)= (0+x)* (0+y),4).
weight(((x+y)* (x+z))* (x+ (y*z)@ )=x+0,4).
weight((x+x)*1=x+0,4).
weight((x+ (y+z))* (x+ (y+z@ ))=x+ (y+0),4).
weight((x*y)+0= (x* (y+y))*1,4).
weight(x+0= (x+x)*1,4).
weight(x* (y+x@ )= (x* (y+y))*1,4).
weight((x* (y+y))*1=x* (y+x@ ),4).
weight((x* (x+x))*1=x*1,4).
weight(x* ((y*z)+x@ )= (x* (y* (z+z)))*1,4).
weight(x@ * (x@ + (x@ +x@ ))=x@ ,4).
weight((x+y@ )* (x+ (y@ + (y@ +y@ )))=x+y@ ,4).
weight(1* (x+ (x@ + (x@ +x@ )))=1,4).
weight(x* (y+ (x@ +x@ ))= (x*y)+ (0+0),4).
weight(x+ ((y*z)+ (0+0))= (x+y)* (x+ (z+ (y@ +y@ ))),4).
weight((x+ (0+y))* (x+ (0+ (y@ +y@ )))=x+ (0+ (0+0)),4).
weight((1*1)+ (0+ (0+0))=1,4).
weight((0+ (0+x@ ))* (0+ (0+x@ ))=x@ ,4).
weight(0@ = (0+1)* (0+1),4).
weight(0* ((0+1)* (0+1))=0,4).
weight((x+ (0+ ((y*z)+y@ )))* (x+ (0+ ((y*z)+z)))=x+z,4).
weight(1* ((1*1)+ (0+1))=1,4).
weight((x+1)* (x+ ((1*1)+ (0+1)))=x+1,4).
weight((x+0)* ((x+ (0+1))* (x+ (0+1)))=x+0,4).
weight((0+1)* (0+ (1+ ((1*1)+ (0+1))))= (1*1)+ (0+1),4).
weight(1* (x+ ((1*1)+ (0+1)))= (1*x)+1,4).
weight(x+ ((1*y)+1)= (x+1)* (x+ (y+ ((1*1)+ (0+1)))),4).
weight((x+1)* (x+ (y+ ((1*1)+ (0+1))))=x+ ((1*y)+1),4).
weight(x@ * (x@ + (x+x))=x@ ,4).
weight((x+y@ )* (x+ (y@ + (y+y)))=x+y@ ,4).
weight(1* (x+ (x@ + (x+x)))=1,4).
weight((1*1)+ (0+1)=0+ ((1*1)+1),4).
weight((0+ ((1*1)+1))* ((1*1)+ (0+ (1+1)))=1,4).
weight((1*1)* ((0+1)* (0+ (1+1)))=1*1,4).
weight((x+ (0+1))* (x+ (0+ (1+1)))= (x+ (0+1))* (x+ (0+1)),4).
weight((0+1)* (0+ (1+1))= (0+1)* (0+1),4).
weight((0+1)* (0+1)=1,4).
weight((0+1)* (0+ (1+1))=1,4).
weight(0*1=0,2).
weight(0@ =1,2).
weight((x+0)* (x+1)=x+0,4).
weight(0+1=1,4).
weight(1* (0+ (1+1))=1,4).
weight(1*1=1,2).
weight(0+ (1+1)=1+1,2).
weight((x+1)* (x+ (1+1))=x+1,4).
weight(1+1=1,2).
weight(1+ (0+ (0+0))=1,4).
weight(x* (0+x@ )= (x*0)*1,4).
weight(0+0=0,4).
weight(1+0=1,2).
weight(((x*y)+z@ )* ((x* (y+y))* ((z@ +x)* (z@ +y)))=x*y,4).
weight(1* ((x* (y+y))* (((x*y)@ +x)* ((x*y)@ +y)))=x*y,4).
weight(1*0=0,4).
weight(1* (1* (x@ +x@ ))=x@ ,4).
weight(1@ =0,4).
weight((x+0)* ((x+1)*1)=x,4).
weight((x+ (y+z@ ))* ((x+ (y+z))* (x+ (z@ +z)))=x+y,4).
weight(1* (((x+y@ )* ((x+y)* ((y@ +y)+ (y@ +y))))* (x@ +x))=x,4).
weight(x* (y+x@ )= (x*y)*1,4).
weight(x+0=x*1,4).
weight((x*x)*1=x*1,4).
weight((x*1)* ((x+1)*1)=x,2).
weight((x*1)* (x+1)=x*1,2).
weight((x+x)*1=x*1,2).
weight((x+y)* (x+y@ )=x*1,2).
weight(x* (x@ *1)= (0+x)*0,4).
weight((x*1)* ((x+1)+y)= (x*1)* ((x*1)+y),4).
weight((x*1)* ((x*1)*1)=x,4).
weight(x+x=x,4).
weight(x*x=x,4).
weight(1* (0+x)=x,2).
weight(x@ * (x@ +x)=x@ ,2).
weight((x+1)* (x+ (0+y))=x+y,4).
weight((x*y)+x=x* (y+x),4).
weight(x@ + (x@ +x)=x@ +x,4).
weight(0+ (0+x)=0+x,4).
weight(0+x=x,4).
weight(((x*y)+x@ )* ((x*y)+y)=y,4).
weight(1*x=x,4).
weight((x+y@ )* (x+y)=x*1,4).
weight((x+1)* (x+y)=x+y,4).
weight(x* (x@ *1)=x*0,4).
weight(x*1=x,4).
weight(x+1=1,4).
weight((x+y)*x=x,4).
weight(x* (y+x)=x,4).
weight(((x+y)* (x+z))*x=x,4).
weight((x*y)+x=x,4).
weight(x* (y*x)=y*x,4).
weight((x*y)+y=y,4).
end_of_list.