----- Otter 3.0.4, August 1995 ----- The job was started by mccune on gyro, Wed Nov 1 21:32:49 1995 ----> UNIT CONFLICT at 955.82 sec ----> 6050 [binary,6049.1,1132.1] -> . Length of proof is 32. Level of proof is 22. ---------------- PROOF ---------------- 1 [] -> x=x. 2 [] x*y=z, x*u=z -> y=u. 5,4 [] -> (x*y)*z=x*y*z. 6 [] -> x*y*y*y*x*y=y*y*y*y*x*x. 7 [] B*A*B*B*B*A=A*A*B*B*B*B -> . 8 [copy,6,flip.1] -> x*x*x*x*y*y=y*x*x*x*y*x. 9 [para_into,6.1.1.2.2.2.2,4.1.1,demod,5,5] -> x*y*z*z*z*x*y*z=z*z*z*z*x*y*x*y. 13 [para_from,6.1.1,4.1.1.1,demod,5,5,5,5,5,5,5,5,5] -> x*x*x*x*y*y*z=y*x*x*x*y*x*z. 19 [para_into,13.1.1.2.2.2.2,8.1.1] -> x*x*x*x*y*z*z*z*y*z=z*x*x*x*z*x*z*z*y*y. 38 [hyper,2,1.1,9.1] -> x*x*x*x*y*x*y=y*x*x*x*x*y*x. 41 [para_into,9.1.1.2.2.2.2.2.2,4.1.1,demod,5,5] -> x*y*z*u*u*u*x*y*z*u=u*u*u*u*x*y*z*x*y*z. 66 [para_from,38.1.1,4.1.1.1,demod,5,5,5,5,5,5,5,5,5,5,5] -> x*y*y*y*y*x*y*z=y*y*y*y*x*y*x*z. 277 [hyper,2,13.1,19.1] -> x*x*x*y*y*y*y*z*z=x*x*x*z*y*y*y*z*y. 566 [hyper,2,66.1,41.1] -> x*x*x*x*y*x*y*x*y=x*y*x*x*x*y*x*y*x. 695 [hyper,2,1.1,277.1] -> x*x*y*z*z*z*y*z=x*x*z*z*z*z*y*y. 699 [hyper,2,1.1,695.1] -> x*y*y*y*y*z*z=x*z*y*y*y*z*y. 717 [para_from,699.1.1,4.1.1.1,demod,5,5,5,5,5,5,5,5,5,5,5] -> x*y*z*z*z*y*z*u=x*z*z*z*z*y*y*u. 718 [copy,717,flip.1] -> x*y*y*y*y*z*z*u=x*z*y*y*y*z*y*u. 905 [hyper,2,718.1,566.1] -> x*x*x*x*y*y*y*x=x*x*x*y*x*y*x*y. 925 [hyper,2,1.1,905.1] -> x*x*y*x*y*x*y=x*x*x*y*y*y*x. 939 [hyper,2,1.1,925.1] -> x*x*y*y*y*x=x*y*x*y*x*y. 977 [hyper,2,1.1,939.1] -> x*y*x*y*x=y*x*x*x*y. 978 [hyper,2,939.1,1.1] -> x*y*y*y*x=y*x*y*x*y. 1017 [para_into,977.1.1.2.2.2,4.1.1,demod,5,5] -> x*y*z*x*y*z*x=y*z*x*x*x*y*z. 1054 [para_from,977.1.1,4.1.1.1,demod,5,5,5,5,5,5,5] -> x*y*y*y*x*z=y*x*y*x*y*z. 1088 [copy,1054,flip.1] -> x*y*x*y*x*z=y*x*x*x*y*z. 1132 [para_from,978.1.1,7.1.1.2] B*B*A*B*A*B=A*A*B*B*B*B -> . 1505 [para_into,1088.1.1.2,1088.1.1] -> x*x*y*y*y*x*z=y*x*x*x*y*y*z. 1566 [copy,1505,flip.1] -> x*y*y*y*x*x*z=y*y*x*x*x*y*z. 3129 [hyper,2,38.1,1017.1] -> x*x*x*y*x*y=y*x*x*y*x*x. 4718 [hyper,2,1017.1,1566.1] -> x*x*y*x*x*y=x*x*x*y*y*x. 4942 [hyper,2,1.1,4718.1] -> x*x*y*y*x=x*y*x*x*y. 5054 [hyper,2,1.1,4942.1] -> x*y*y*x=y*x*x*y. 5272 [para_from,5054.1.1,4.1.1.1,demod,5,5,5,5,5] -> x*y*y*x*z=y*x*x*y*z. 5383 [hyper,2,3129.1,5272.1] -> x*x*y*x*y=y*y*x*x*x. 5972 [para_from,5383.1.1,4.1.1.1,demod,5,5,5,5,5,5,5] -> x*x*y*y*y*z=y*y*x*y*x*z. 6049 [copy,5972,flip.1] -> x*x*y*x*y*z=y*y*x*x*x*z. 6050 [binary,6049.1,1132.1] -> . ------------ end of proof -------------