----- Otter 3.0.4, August 1995 -----
The job was started by wos on merlin.mcs.anl.gov, Tue Oct  3 15:20:56 1995
The command was "otter304".

op(400,xfx,[*,+,^,v,/,\,#]).  %  make all association explicit
op(300,yf,@).
clear(print_kept).  %  Do not enter into the output file clauses as they are retained.
clear(print_new_demod).
clear(print_back_demod).
assign(pick_given_ratio,12).  %  Twelve clauses are chosen by weight and one by breadth first, repeatedly.
assign(max_mem,28000).  %  Limit the memory usage in kilobytes.

%%%%%%%%%%%%%%%%%%%%%  Standard for equational problems

set(knuth_bendix).
   dependent: set(para_from).  %  Paramodulate from the chosen clause.
   dependent: set(para_into).  %  Paramodulate into the chosen clause.
   dependent: clear(para_from_right).
   dependent: clear(para_into_right).
   dependent: set(para_from_vars).
   dependent: set(eq_units_both_ways).
   dependent: set(dynamic_demod_all).
   dependent: set(dynamic_demod).  %  Adjoin demodulators during the run.
   dependent: set(order_eq).  %  Flip arguments if righthand heavier than lefthand.
   dependent: set(back_demod).  %  Apply new demodulators to retained clauses.
   dependent: set(process_input).  % Treat input clauses as if they were generated by applying an inference rule.
   dependent: set(lrpo).  %  Activate the LRPO ordering for orienting equalities and deciding dynamic demodulators.
set(ancestor_subsume).  %  Compare path lengths for derivations to the same conclusion.
WARNING: set(back_sub) flag already set.
set(back_sub).  %  Purge an existing clauses when a new clause captures such.

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

assign(max_weight,4).  %  Disallow clauses with weight strictly greater than 4.
assign(max_proofs,2).  %  Place limit of 2 on the number of proofs to be completed.
assign(heat,3).  %  Limits the recursion through the hot list.

%  Used to direct the reasoning and to purge unwanted clauses.
weight_list(pick_and_purge).
%  Following are those of weight less or equal 10 from temp.boolean.shorten.exp25.out, 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).
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.

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

list(usable).
0 [] x=x.
end_of_list.

list(sos).
0 [] x* (y+z)= (x*y)+ (x*z).
0 [] x+ (y*z)= (x+y)* (x+z).
0 [] x+x@ =1.
0 [] x*x@ =0.
0 [] (x*y@ )+ ((x*x)+ (y@ *x))=x.
0 [] (x*x@ )+ ((x*z)+ (x@ *z))=z.
0 [] (x*y@ )+ ((x*y)+ (y@ *y))=x.
0 [] (x+y@ )* ((x+x)* (y@ +x))=x.
0 [] (x+x@ )* ((x+z)* (x@ +z))=z.
0 [] (x+y@ )* ((x+y)* (y@ +y))=x.
end_of_list.

list(passive).
1 [] (A*B)+B!=B|$Ans(A2).
2 [] (A+B)*B!=B|$Ans(A4).
end_of_list.

list(hot).
3 [] x* (y+z)= (x*y)+ (x*z).
4 [] x+ (y*z)= (x+y)* (x+z).
5 [] x+x@ =1.
6 [] x*x@ =0.
end_of_list.