----- Otter 3.0.4a, November 1995 ----- The job was started by mccune on gyro, Fri May 3 09:54:59 1996 ----> UNIT CONFLICT at 0.06 sec ----> 8 [binary,6.1,2.1] $F. Length of proof is 1. Level of proof is 1. ---------------- PROOF ---------------- 2 [] B* (A*A@ )!=B. 4 [] x=x. 5 [] (x*y)*z!= (x*u)*v|u* (v*z@ )=y. 6 [hyper,5,4] x* (y*y@ )=x. 8 [binary,6.1,2.1] $F. ------------ end of proof ------------- ----> UNIT CONFLICT at 0.07 sec ----> 14 [binary,13.1,1.1] $F. Length of proof is 5. Level of proof is 5. ---------------- PROOF ---------------- 1 [] A*A@ !=B*B@ . 4 [] x=x. 5 [] (x*y)*z!= (x*u)*v|u* (v*z@ )=y. 7,6 [hyper,5,4] x* (y*y@ )=x. 9 [para_from,6.1.1,5.2.1] (x*y)*z!= (x*u)*z|u=y. 11 [para_into,9.1.1,6.1.1,demod,7] x*y!=x*z|z=y. 12 [para_into,11.1.1,6.1.1,flip.1] x*y!=x|y=z*z@ . 13 [hyper,12,6] x*x@ =y*y@ . 14 [binary,13.1,1.1] $F. ------------ end of proof ------------- ----> UNIT CONFLICT at 1.30 sec ----> 247 [binary,245.1,3.1] $F. Length of proof is 25. Level of proof is 19. ---------------- PROOF ---------------- 3 [] (A*B)*C!=A* (B*C). 4 [] x=x. 5 [] (x*y)*z!= (x*u)*v|u* (v*z@ )=y. 7,6 [hyper,5,4] x* (y*y@ )=x. 9 [para_from,6.1.1,5.2.1] (x*y)*z!= (x*u)*z|u=y. 11 [para_into,9.1.1,6.1.1,demod,7] x*y!=x*z|z=y. 12 [para_into,11.1.1,6.1.1,flip.1] x*y!=x|y=z*z@ . 13 [hyper,12,6] x*x@ =y*y@ . 15 [hyper,12,13] (x*x@ )@ =y*y@ . 16 [hyper,5,13] x* ((y*x)@ * (y*z)@ @ )=z. 18 [copy,15,flip.1] x*x@ = (y*y@ )@ . 25 [para_from,18.1.1,6.1.1.2] x* (y*y@ )@ =x. 30,29 [para_into,25.1.1.2.1,18.1.1] x* (y*y@ )@ @ =x. 34 [para_into,16.1.1.2.1.1,6.1.1] (x*x@ )* (y@ * (y*z)@ @ )=z. 36 [para_into,16.1.1.2.1,15.1.1] x@ * ((y*y@ )* (x*z)@ @ )=z. 38 [para_into,16.1.1.2.2.1.1,13.1.1,demod,30] x* (y*x)@ =y@ . 42 [para_into,38.1.1.2.1,38.1.1] (x*y)@ *x@ @ =y@ . 47,46 [para_into,38.1.1.2.1,6.1.1] (x*x@ )*y@ =y@ . 49,48 [back_demod,36,demod,47] x@ * (x*y)@ @ =y. 51,50 [back_demod,34,demod,49] (x*x@ )*y=y. 64 [para_from,50.1.1,9.1.1.1,demod,51] x*y!=z*y|z=x. 65 [para_from,50.1.1,5.1.1.1,demod,51] x*y!=z*u|z* (u*y@ )=x. 84,83 [para_into,48.1.1.1,15.1.1,demod,51,51] x@ @ =x. 86,85 [para_into,48.1.1.2.1.1,38.1.1,demod,84,flip.1] (x*y)@ =y@ *x@ . 94 [back_demod,42,demod,86,84] (x@ *y@ )*y=x@ . 162 [para_into,94.1.1.1.1,83.1.1,demod,84] (x*y@ )*y=x. 166 [hyper,64,162,flip.1] (x*y)*y@ =x. 245 [hyper,65,166,demod,84,flip.1] (x*y)*z=x* (y*z). 247 [binary,245.1,3.1] $F. ------------ end of proof -------------