----- Otter 3.0.4, August 1995 -----
The job was started by mccune on gyro, Wed Nov  1 21:24:26 1995
-----> EMPTY CLAUSE at   4.89 sec ----> 462 [hyper,4,412.1,134.1]  -> .

Length of proof is 7.  Level of proof is 6.

---------------- PROOF ----------------

4 [] A*B*A*B*A*B=A*A*A*B*B*B, B*B*B*A*A*A=A*A*A*B*B*B -> .
6,5 []  -> (x*y)*z=x*y*z.
7 []  -> x*y*z*u=y*z*u*x.
8 [copy,7,flip.1]  -> x*y*z*u=u*x*y*z.
9 [para_into,7.1.1.2.2,7.1.1,demod,6,6]  -> x*y*z*u*v*w=y*w*z*u*v*x.
22 [para_into,8.1.1,7.1.1]  -> x*y*z*u=z*u*x*y.
111 [para_into,9.1.1.2,22.1.1,demod,6]  -> x*y*z*u*v*w=v*u*w*y*z*x.
134 [copy,111,flip.1]  -> x*y*z*u*v*w=w*u*v*y*x*z.
373 [para_into,134.1.1.2,8.1.1,demod,6]  -> x*y*z*u*v*w=z*w*y*u*x*v.
412 [copy,373,flip.1]  -> x*y*z*u*v*w=v*z*x*u*w*y.
462 [hyper,4,412.1,134.1]  -> .

------------ end of proof -------------