----- Otter 3.0.4, August 1995 -----
The job was started by mccune on gyro, Wed Nov  1 22:02:18 1995
----> UNIT CONFLICT at   0.12 sec ----> 43 [binary,41.1,32.1]  -> .

Length of proof is 9.  Level of proof is 4.

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

2 [] A* ((((A*B@ )*B)@ *C)* ((alpha*D)@ * (beta*D)))=C -> .
4,3 []  -> beta=alpha.
5 []  -> x@ *x=y@ *y.
7,6 []  -> x@ * (x*y)=y.
8 []  -> (x*y)*y@ =x.
10 [back_demod,2,demod,4] A* ((((A*B@ )*B)@ *C)* ((alpha*D)@ * (alpha*D)))=C -> .
12,11 [para_into,6.1.1.2,6.1.1]  -> x@ @ *y=x*y.
15 [para_into,8.1.1.1,6.1.1]  -> x* (y*x)@ =y@ .
22,21 [para_from,5.1.1,6.1.1.2,demod,12]  -> x* (y@ *y)=x.
23 [back_demod,10,demod,22] A* (((A*B@ )*B)@ *C)=C -> .
27,26 [para_into,21.1.1,6.1.1,flip.1]  -> x@ @ =x.
31,30 [para_into,15.1.1.2.1,8.1.1,flip.1]  -> (x*y)@ =y@ *x@ .
32 [back_demod,23,demod,31,31,27,7] A* (A@ *C)=C -> .
41 [para_from,26.1.1,6.1.1.1]  -> x* (x@ *y)=y.
43 [binary,41.1,32.1]  -> .

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