----- Otter 3.0.4, August 1995 ----- The job was started by mccune on gyro, Wed Nov 1 21:58:35 1995 ----> UNIT CONFLICT at 2.62 sec ----> 676 [binary,675.1,634.1] -> . Length of proof is 26. Level of proof is 14. ---------------- PROOF ---------------- 1 [] -> x=x. 2 [] B*B@ =A*A@ , A* (B*B@ )=A, (A*B)*C=A* (B*C) -> . 3 [] -> ((x*y)* (alpha*z))* (y* (alpha*z))@ =x. 5 [] -> ((x*beta)*y)@ * ((x*beta)* (y*z))=z. 7 [para_into,3.1.1.1.1,3.1.1] -> (x* (alpha*y))* ((z* (alpha*u))@ * (alpha*y))@ = (x*z)* (alpha*u). 16,15 [para_into,7.1.1,3.1.1,flip.1] -> ((x* (y* (alpha*z))@ )*y)* (alpha*z)=x. 28,27 [para_from,15.1.1,5.1.1.2] -> (((x* (beta* (alpha*y))@ )*beta)*alpha)@ *x=y. 45 [para_from,27.1.1,5.1.1.2.1,demod,28] -> (x*y)@ * (x* (y*z))=z. 99 [para_into,45.1.1.2,45.1.1] -> ((x*y)@ *x)@ *z=y*z. 139,138 [para_into,99.1.1,45.1.1,flip.1] -> x* ((y*x)@ * (y*z))=z. 140 [para_from,99.1.1,15.1.1.1.1,demod,16,flip.1] -> ((x*y)@ *x)@ =y. 144 [para_into,140.1.1.1.1.1,45.1.1] -> (x@ * (y*z)@ )@ =y* (z*x). 154 [para_into,140.1.1.1.1,140.1.1] -> (x* (y*x)@ )@ =y. 170 [para_from,154.1.1,45.1.1.1] -> x* (y* ((x*y)@ *z))=z. 276 [para_from,138.1.1,15.1.1.2,demod,139] -> ((x* (y*z)@ )*y)*z=x. 279 [para_from,138.1.1,3.1.1.2.1.2,demod,139] -> ((x*y)*z)* (y*z)@ =x. 309 [para_into,276.1.1.1.1.2,140.1.1] -> ((x*y)* (z*y)@ )*z=x. 419 [para_from,309.1.1,45.1.1.1.1] -> x@ * (((x*y)* (z*y)@ )* (z*u))=u. 435,434 [para_into,144.1.1,154.1.1,flip.1] -> x* (y@ *y)=x. 480 [para_into,434.1.1,276.1.1,demod,435,flip.1] -> (x*y@ )*y=x. 489 [para_from,434.1.1,154.1.1.1.2.1] -> ((x@ *x)*y@ )@ =y. 493 [para_from,434.1.1,279.1.1.1,demod,435] -> (x*y)*y@ =x. 521,520 [para_into,480.1.1.1,279.1.1,flip.1] -> (x*y)*z=x* (y*z). 553,552 [back_demod,493,demod,521] -> x* (y*y@ )=x. 556 [back_demod,489,demod,521] -> (x@ * (x*y@ ))@ =y. 580,579 [back_demod,419,demod,521,521,521,139] -> x@ * (x*y)=y. 634 [back_demod,2,demod,553,521,unit_del,1,1] B*B@ =A*A@ -> . 635 [back_demod,556,demod,580] -> x@ @ =x. 648,647 [para_into,635.1.1.1,154.1.1,flip.1] -> x* (y*x)@ =y@ . 675 [para_from,552.1.1,170.1.1.2.2,demod,648] -> x*x@ =y*y@ . 676 [binary,675.1,634.1] -> . ------------ end of proof -------------