----- Otter 3.0.4, August 1995 ----- The job was started by mccune on gyro, Wed Nov 1 21:51:22 1995 -----> EMPTY CLAUSE at 28.95 sec ----> 6098 [back_demod,2,demod,5275,unit_del,31,1] -> . Length of proof is 33. Level of proof is 9. ---------------- PROOF ---------------- 1 [] -> x=x. 2 [] B*A=A*B, (A*B)*C=A* (B*C) -> . 4,3 [] -> (x+y)*y=y. 5 [] -> x* (y+z)= (y*x)+ (z*x). 6 [copy,5,flip.1] -> (x*y)+ (z*y)=y* (x+z). 9,8 [] -> x+x@ =1. 11,10 [] -> (x*y)+y=y. 12 [] -> x+ (y*z)= (y+x)* (z+x). 13 [] -> x*x@ =0. 15 [copy,12,flip.1] -> (x+y)* (z+y)=y+ (x*z). 18 [para_into,10.1.1.1,13.1.1] -> 0+x@ =x@ . 21,20 [para_into,10.1.1.1,3.1.1] -> x+x=x. 23,22 [para_from,10.1.1,3.1.1.1] -> x*x=x. 29 [para_into,6.1.1.2,3.1.1,demod,11,flip.1] -> x* (y+ (z+x))=x. 31 [para_into,6.1.1,20.1.1,demod,21] -> x*y=y*x. 36,35 [para_from,22.1.1,6.1.1.2,demod,11,flip.1] -> x* (y+x)=x. 38,37 [para_from,22.1.1,6.1.1.1] -> x+ (y*x)=x* (x+y). 56 [para_into,12.1.1.2,22.1.1,demod,23] -> x+y=y+x. 72 [para_into,18.1.1,8.1.1,flip.1] -> 0@ =1. 76 [para_from,72.1.1,13.1.1.2] -> 0*1=0. 94,93 [para_into,15.1.1.2,20.1.1,demod,4,38,flip.1] -> x* (x+y)=x. 98 [para_into,15.1.1.2,10.1.1,demod,4,flip.1] -> x+ (y* (z*x))=x. 115 [back_demod,37,demod,94] -> x+ (y*x)=x. 130 [para_from,76.1.1,12.1.1.2] -> x+0= (0+x)* (1+x). 135 [copy,130,flip.1] -> (0+x)* (1+x)=x+0. 141 [para_into,31.1.1,13.1.1,flip.1] -> x@ *x=0. 150 [para_from,141.1.1,12.1.1.2] -> x+0= (y@ +x)* (y+x). 153,152 [para_from,141.1.1,10.1.1.1] -> 0+x=x. 155,154 [para_from,141.1.1,6.1.1.1,demod,153,flip.1] -> x* (x@ +y)=y*x. 156 [copy,150,flip.1] -> (x@ +y)* (x+y)=y+0. 161,160 [back_demod,135,demod,153,36,flip.1] -> x+0=x. 164 [copy,156,flip.1,demod,161,flip.1] -> (x@ +y)* (x+y)=y. 235,234 [para_into,56.1.1,12.1.1,flip.1] -> (x*y)+z= (x+z)* (y+z). 236 [para_into,56.1.1,8.1.1,flip.1] -> x@ +x=1. 276,275 [para_from,236.1.1,29.1.1.2] -> x*1=x. 366 [para_into,115.1.1.2,93.1.1] -> (x+y)+x=x+y. 1269 [para_into,366.1.1,56.1.1] -> x+ (x+y)=x+y. 1623 [para_into,154.1.1.2,1269.1.1,demod,155,flip.1] -> (x@ +y)*x=y*x. 1922 [para_into,164.1.1.1,56.1.1] -> (x+y@ )* (y+x)=x. 4171,4170 [para_into,1623.1.1.1,12.1.1] -> ((x+y@ )* (z+y@ ))*y= (x*z)*y. 5275,5274 [para_into,1922.1.1.2,98.1.1,demod,235,235,9,276,4171] -> (x*y)*z=x* (y*z). 6098 [back_demod,2,demod,5275,unit_del,31,1] -> . ------------ end of proof -------------