----- Otter 3.0.4, August 1995 -----
The job was started by wos on snow.mcs.anl.gov, Wed Dec 13 07:50:22 1995
The command was "/home/mccune/bin-rs6000/otter".

%%%%%%%%%%%%%%%%%%%%%  Basic options

op(400,xfx,[*,+,^,v,/,\,#]).    % infix operators
op(300,yf,@).   % postfix operator
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,8).  %  Eight clauses are chosen by weight and one by
 breadth first, repeatedly.
assign(max_mem,20000).   %  Limit the memory usage in kilobytes.

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

set(knuth_bendix).
   dependent: set(para_from).   %  Paramodulate <em>from</em> the chosen clause.
   dependent: set(para_into).   %  Paramodulate <em>into</em> 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.

%%%%%%%%%%%%%%%%%%%%%  Standard options for hyperresolution

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.
set(build_proof_object).
   dependent: set(order_history).  %  List ancestors in the order nucleus, clause unifying with first literal, clause unifying with second.

%%%%%%%%%%%%%%%%%%%%%  Standard options for hyperresolution

set(output_sequent).
set(hyper_res).
WARNING: set(order_history) flag already set.
set(order_history).   %  List ancestors in the order nucleus, clause unifying with first literal, clause unifying with second.
set(unit_deletion).
set(para_from_units_only).
set(para_into_units_only).

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

assign(max_weight,25).   %  Disallow clauses with weight strictly greater than 8.
%  Used to direct the reasoning and to purge unwanted clauses.
weight_list(pick_and_purge).
%  Following are McCune's proof steps.
weight((x* (y*z))+y=y,2).
weight(x* (y+ (z+x))=x,2).
weight(x* (y+x)=x,2).
weight((x+ (y+z))*y=y,2).
weight(x+ (y*x)=x,2).
weight(x* (x+y)=x,2).
weight((x+y)*y=y,2).
weight((x+y)* (y+x@ )=y,2).
weight((x+y)* (y@ +x)=x,2).
weight((x+y@ )* (x+y)=x,2).
weight(x+ (y+ (z*x))=x+y,2).
weight(x+ (x*y)=x,2).
weight((x*y)+y=y,2).
weight(x*x=x,2).
weight((x+y)*x=x,2).
weight(x+ (y+x)=x+y,2).
weight(x+x=x,2).
weight((x*y)+ (y*x@ )=y,2).
weight((x*y)+ (y@ *x)=x,2).
weight((x*y@ )+ (x*y)=x,2).
weight(x* (y* (z+x))=x*y,2).
weight(x* (y*x)=x*y,2).
weight((x*y)+x=x,2).
weight(x+ (x+y)=x+y,2).
weight(x+ ((x*y)+z)=x+z,2).
weight(x+ ((y*x)+z)=x+z,2).
weight(x+ (y+z)=y+ (x+z),2).
weight(x+ (y+ (z* (x+y)))=x+y,2).
weight(x+ (y+z)=y+ (z+x),2).
weight(x+ (y+z)=z+ (x+y),2).
weight((x+ (y+z))* (x+ (y+z@ ))=x+y,2).
weight((x+ (y+z))* (x+y)=x+y,2).
weight((x+ (y+z))*z=z,2).
weight((x*y)+ (z+y)=z+y,2).
weight(x* (y+ (z+ (u+x)))=x,2).
weight(x* ((x+y)*z)=x*z,2).
weight(x* ((y+x)*z)=x*z,2).
weight((x*y)+ (x* (y*z))=x*y,2).
weight((x+y)* (z*y)=z*y,2).
weight((x+ (y+ (z+u)))*u=u,2).
weight((x+ (y*x@ ))*x@ =y*x@ ,2).
weight((x+y)* (x@ +y)=y,2).
weight((x+y@ )* (y+x)=x,2).
weight((x+y)* ((y+x@ )*z)=y*z,2).
weight(x* (x@ + (x*y))=x*y,2).
weight((x@ +y)* (y+x)=y,2).
weight((x* (y+x@ ))+x@ =y+x@ ,2).
weight((x*y)+ (x@ *y)=y,2).
weight((x*y@ )+ (y*x)=x,2).
weight((x* (y*z))+ (z@ * (x*y))=x*y,2).
weight((x@ *y)+ (y*x)=y,2).
weight((x*y)+ (z+ (y*x))= (x*y)+z,2).
weight(x+ (y+ (x*z))=x+y,2).
weight(x+ (y*x@ )=x+y,2).
weight(x@ + (x*y)=x@ +y,2).
weight(x@ + (y*x)=x@ +y,2).
weight((x+y)*x@ =y*x@ ,2).
weight(x* (x@ +y)=x*y,2).
weight((x@ +y)* (x+y)=y,2).
weight(x@ * (x+ (x@ *y))=x@ *y,2).
weight((x@ +y)*x=x*y,2).
weight(((x+y)@ * (x+y@ ))+x=x+y@ ,2).
weight(x+ (x@ *y)=x+y,2).
weight(x@ * (x+y)=x@ *y,2).
weight(x+ (x@ +y)=x+x@ ,2).
weight(x+ (y+x@ )=x+x@ ,2).
weight(x@ + (x+y)=x@ +x,2).
weight(x* (y+x@ )=x*y,2).
weight((x*y)+x@ =y+x@ ,2).
weight((x@ *y)+ ((x@ @ +y)*x)=x@ @ +y,2).
weight((x@ +x)* (x+y)=x+y,2).
weight((x@ *y)+ (x* (x@ @ +y))=x@ @ +y,2).
weight(x* (x@ @ *y)=x*y,2).
weight(((x@ @ *y)+x)* (x@ +y)=x@ @ *y,2).
weight(x+ ((x@ *y)+z)=x+ (y+z),2).
weight((x@ *y)+z= (x@ +z)* (x+ (y+z)),2).
weight((x@ @ +x)* (x@ +y)=x@ @ *y,2).
weight(x@ @ +y= (x@ +x@ @ )* (x+y),2).
weight((x@ +x@ @ )* (x+y)=x+y,2).
weight(((x+y)@ +x)* (x+ (y+y@ ))=x+y@ ,2).
weight(x@ @ *y=x*y,2).
weight(x@ @ +y=x+y,2).
weight(x@ @ =x,2).
weight((x+y)* (x@ + ((z*x)+y))= (z*x)+y,2).
weight(x+ (((x+y)*z)+y)=x+y,2).
weight((x*y)+z=z+ (y*x),2).
weight(x+ ((x@ +y)*z)=x+z,2).
weight((x*y)+ ((x@ + (z*y))* (x+y))=y,2).
weight((x+y)* (x+ (z+y@ ))=x+ (y*z),2).
weight(x@ + ((x+y)*z)=x@ +z,2).
weight(x@ + ((y*x)+z)=x@ + (y+z),2).
weight((x+y)* (x@ + (z+y))= (z*x)+y,2).
weight((x*y)+z= (y+z)* (y@ + (x+z)),2).
weight(x+ (y+y@ )=y+y@ ,2).
weight(((x+y)@ +x)* (y+y@ )=x+y@ ,2).
weight((x+x@ )*y=y,2).
weight(x* (y+y@ )=x,2).
weight((x@ +y)@ +x=x,2).
weight((x+y)@ +x=x+y@ ,2).
weight(x+x@ =y+y@ ,2).
weight(x+ (y+z)@ = (x+ (y+z@ ))* (x+y@ ),2).
weight((x+y)@ =y@ *x@ ,2).
weight(((x+y)*z)+y@ =z+y@ ,2).
weight((x@ + ((x@ +y)*z))* (x+z)= (x@ +y)*z,2).
weight(((x+ (y*z))*y)+ (y*z)= (x+ (y*z))*y,2).
weight(x+ ((x+y)*z)=x+ (y*z),2).
weight((((x+y)*z)+y)* (x+y)= ((x+y)*z)+y,2).
weight((x+y)* (x@ + (((x+y)*z)+y))= ((x+y)*z)+y,2).
weight((x@ + (y*z))* (x+z)= (x@ +y)*z,2).
weight((x*y)+ ((x@ +z)*y)=y,2).
weight(((x@ +y)*z)+ (z*x)=z,2).
weight((x*y)+ (y*z)= (x+z)*y,2).
weight((x+ (y*z))*y= (x+z)*y,2).
weight((x*y)+ (y@ * (z*x))=x* (y+z),2).
weight(((x*y)+z)*x=x* (y+z),2).
weight(((x+y)*z)+y= (x+y)* (z+y),2).
weight((x+y)* (x@ + (z+y))= (x+y)* (z+y),2).
weight((x*y)+z= (y+z)* (x+z),2).
end_of_list.

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

list(usable).
0 []  -> x=x.
0 [] (A*B)+ (A*C)=A* (B+C), (A+B)*B=B, B+B@ =A+A@  -> .
end_of_list.

list(sos).
0 []  -> y+ (x* (y*z))=y.   % L1
0 []  -> ((x*y)+ (y*z))+y=y.  % L3
0 []  -> (x+y)* (x+y@ )=x.  % B1

0 []  -> y* (x+ (y+z))=y. % L2
0 []  -> ((x+y)* (y+z))*y=y. % L4
0 []  -> (x*y)+ (x*y@ )=x. % B2

% lemmas

0 []  -> x+y=y+x.
0 []  -> x*y=y*x.
0 []  -> (x+y)+z=x+ (y+z).
0 []  -> (x*y)*z=x* (y*z).
end_of_list.