----- Otter 3.0.4, August 1995 ----- The job was started by mccune on gyro, Wed Nov 1 21:57:51 1995 ----> UNIT CONFLICT at 3.38 sec ----> 565 [binary,563.1,20.1] -> . Length of proof is 27. Level of proof is 11. ---------------- PROOF ---------------- 1 [] -> x=x. 2 [] B*B@ =A*A@ , A* (B*B@ )=A, (A*B)*C=A* (B*C) -> . 3 [] -> x* (x@ *y)=y. 5 [] -> (x*y@ )*y=x. 7 [] -> x@ *x=y*y@ . 8 [] -> ((x* (alpha*y))*beta)*z=x* (alpha* ((y*beta)*z)). 15 [para_into,7.1.1,7.1.1] -> x*x@ =y*y@ . 16 [para_from,7.1.1,5.1.1.1] -> (x*x@ )*y=y@ @ . 18,17 [para_from,7.1.1,3.1.1.2] -> x* (y*y@ )=x. 19 [copy,16,flip.1] -> x@ @ = (y*y@ )*x. 20 [back_demod,2,demod,18,unit_del,15,1] (A*B)*C=A* (B*C) -> . 25,24 [para_into,17.1.1,3.1.1] -> x@ @ =x. 28,27 [back_demod,19,demod,25,flip.1] -> (x*x@ )*y=y. 31 [para_from,24.1.1,5.1.1.1.2] -> (x*y)*y@ =x. 33 [para_from,24.1.1,3.1.1.2.1] -> x@ * (x*y)=y. 37 [para_into,8.1.1.1.1.2,3.1.1] -> ((x*y)*beta)*z=x* (alpha* (((alpha@ *y)*beta)*z)). 38 [para_into,8.1.1.1.1,17.1.1] -> (x*beta)*y=x* (alpha* ((alpha@ *beta)*y)). 48 [copy,38,flip.1] -> x* (alpha* ((alpha@ *beta)*y))= (x*beta)*y. 52,51 [para_into,27.1.1.1.2,24.1.1] -> (x@ *x)*y=y. 61 [para_into,33.1.1.2,31.1.1] -> (x*y)@ *x=y@ . 76,75 [para_into,61.1.1.1.1,33.1.1,flip.1] -> (x*y)@ =y@ *x@ . 94 [para_from,75.1.1,33.1.1.1] -> (x@ *y@ )* ((y*x)*z)=z. 160,159 [para_into,37.1.1.1.1,51.1.1,demod,52,flip.1] -> alpha* (((alpha@ *x)*beta)*y)= (x*beta)*y. 167,166 [para_into,37.1.1.1.1,15.1.1,demod,28,160,flip.1] -> x* ((x@ *beta)*y)=beta*y. 173,172 [para_into,37.1.1.1.1,3.1.1,demod,160,flip.1] -> x* (((x@ *y)*beta)*z)= (y*beta)*z. 181 [para_into,37.1.1,3.1.1,demod,76,76,173,flip.1] -> x* ((y*beta)* ((beta@ * (y@ *x@ ))*z))=z. 195,194 [back_demod,48,demod,167,flip.1] -> (x*beta)*y=x* (beta*y). 215 [back_demod,181,demod,195] -> x* (y* (beta* ((beta@ * (y@ *x@ ))*z)))=z. 233 [para_into,194.1.1,3.1.1,demod,76,flip.1] -> x* (beta* ((beta@ *x@ )*y))=y. 380 [para_into,94.1.1.1.2,24.1.1] -> (x@ *y)* ((y@ *x)*z)=z. 420,419 [para_from,233.1.1,3.1.1.2,demod,25,flip.1] -> beta* ((beta@ *x)*y)=x*y. 423 [back_demod,215,demod,420] -> x* (y* ((y@ *x@ )*z))=z. 563 [para_into,423.1.1.2.2,380.1.1,demod,25,flip.1] -> (x*y)*z=x* (y*z). 565 [binary,563.1,20.1] -> . ------------ end of proof -------------