----- Otter 3.0.4, August 1995 -----
The job was started by mccune on gyro, Wed Nov  1 22:01:57 1995
----> UNIT CONFLICT at   0.08 sec ----> 36 [binary,35.1,1.1]  -> .

Length of proof is 8.  Level of proof is 5.

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

1 []  -> x=x.
2 [] A* ((((A*B@ )*B)@ *C)* (D@ *D))=C -> .
3 []  -> x@ *x=y@ *y.
4 []  -> x@ * (x*y)=y.
6 []  -> (x*y)*y@ =x.
8 [para_from,3.1.1,2.1.1.2.2] A* ((((A*B@ )*B)@ *C)* (x@ *x))=C -> .
10,9 [para_into,4.1.1.2,4.1.1]  -> x@ @ *y=x*y.
12,11 [para_into,4.1.1.2,3.1.1,demod,10]  -> x* (y@ *y)=x.
13 [back_demod,8,demod,12] A* (((A*B@ )*B)@ *C)=C -> .
24 [para_into,11.1.1,4.1.1,flip.1]  -> x@ @ =x.
31,30 [para_from,24.1.1,6.1.1.2]  -> (x*y@ )*y=x.
33,32 [para_from,24.1.1,4.1.1.1]  -> x* (x@ *y)=y.
35 [back_demod,13,demod,31,33] C=C -> .
36 [binary,35.1,1.1]  -> .

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