----- Otter 3.0.4, August 1995 ----- The job was started by mccune on gyro, Wed Nov 1 21:59:28 1995 ----> UNIT CONFLICT at 103.17 sec ----> 1450 [binary,1449.1,3.1] -> . Length of proof is 74. Level of proof is 16. ---------------- PROOF ---------------- 1 [] -> x=x. 2 [] O*O=A*A, O*O=B*B, O*O=C*C, P*P=O*O, Q*Q=O*O, R*R=O*O, U*U=O*O, V*V=O*O, W*W=O*O -> . 3 [] -> x*y=y*x. 4 [] -> x* (y*x)=y. 7,6 [] -> A*P=O. 9,8 [] -> B*Q=O. 11,10 [] -> C*R=O. 12 [] -> P*Q=W. 14 [] -> P*R=V. 16 [] -> Q*R=U. 18 [] -> A*B=W. 21,20 [] -> A*C=V. 23,22 [] -> B*C=U. 24 [] -> U*V=W. 26 [para_into,3.1.1.1,3.1.2] -> (x*y)*z=z* (y*x). 27 [para_into,3.1.1.2,3.1.2] -> x* (y*z)= (z*y)*x. 28 [para_into,6.1.1,3.1.2] -> P*A=O. 33,32 [para_into,10.1.1,3.1.2] -> R*C=O. 38 [para_into,4.1.1.2,12.1.1] -> Q*W=P. 43,42 [para_into,4.1.1.2,8.1.1] -> Q*O=B. 44 [para_into,4.1.1.2,6.1.1] -> P*O=A. 46 [para_into,4.1.1.2,4.1.1] -> (x*y)*x=y. 48 [para_into,4.1.1.2,3.1.2] -> x* (x*y)=y. 50 [para_into,4.1.1,3.1.2] -> (x*y)*y=x. 54 [para_from,14.1.1,4.1.1.2] -> R*V=P. 58 [para_from,16.1.1,4.1.1.2] -> R*U=Q. 60 [para_into,18.1.1,3.1.2] -> B*A=W. 62 [para_from,18.1.1,4.1.1.2] -> B*W=A. 64 [para_into,20.1.1,3.1.2] -> C*A=V. 69,68 [para_into,22.1.1,3.1.2] -> C*B=U. 71,70 [para_from,22.1.1,4.1.1.2] -> C*U=B. 73,72 [para_into,24.1.1,3.1.2] -> V*U=W. 75,74 [para_from,24.1.1,4.1.1.2] -> V*W=U. 77,76 [para_from,28.1.1,4.1.1.2] -> A*O=P. 81,80 [para_from,32.1.1,4.1.1.2] -> C*O=R. 86 [para_into,26.1.1.2,3.1.2] -> (x*y)* (z*u)= (u*z)* (y*x). 88 [para_into,26.1.1,4.1.1,flip.1] -> (x* (y*z))* (z*y)=x. 102 [para_into,38.1.1,3.1.2] -> W*Q=P. 123,122 [para_into,54.1.1,3.1.2] -> V*R=P. 125,124 [para_from,54.1.1,4.1.1.2] -> V*P=R. 134 [para_into,58.1.1,3.1.2] -> U*R=Q. 139,138 [para_from,60.1.1,4.1.1.2] -> A*W=B. 140 [para_into,62.1.1,3.1.2] -> W*B=A. 150 [para_into,46.1.1.1,64.1.1] -> V*C=A. 161,160 [para_from,68.1.1,4.1.1.2] -> B*U=C. 163,162 [para_from,72.1.1,46.1.1.1] -> W*V=U. 169,168 [para_into,48.1.1.1,27.1.1] -> ((x*y)*z)* ((z* (y*x))*u)=u. 194 [gL,86] -> (x*y)* (z*u)= (x*z)* (y*u). 196 [para_into,194.1.1.1,150.1.1,flip.1] -> (V*x)* (C*y)=A* (x*y). 640,639 [para_into,196.1.1.2,48.1.1] -> (V*x)*y=A* (x* (C*y)). 646,645 [para_into,196.1.2.2,140.1.1,demod,75,69] -> U*U=A*A. 647 [para_into,196.1.2.2,134.1.1,demod,73,11] -> W*O=A*Q. 651 [para_into,196.1.2.2,102.1.1,demod,75,7] -> U* (C*Q)=O. 653 [para_into,196.1.2.2,58.1.1,demod,123,71] -> P*B=A*Q. 658,657 [para_into,196.1.2.2,44.1.1,demod,125,81] -> R*R=A*A. 659 [para_into,196.1.2.2,32.1.1,demod,123,77] -> P* (C*C)=P. 666 [back_demod,2,demod,658,646] O*O=A*A, O*O=B*B, O*O=C*C, P*P=O*O, Q*Q=O*O, V*V=O*O, W*W=O*O -> . 676 [para_from,645.1.1,48.1.1.2] -> U* (A*A)=U. 690 [para_from,647.1.1,48.1.1.2] -> W* (A*Q)=O. 710 [para_from,651.1.1,88.1.1.1] -> O* (Q*C)=U. 715 [para_from,651.1.1,50.1.1.1] -> O* (C*Q)=U. 733 [para_from,653.1.1,50.1.1.1] -> (A*Q)*B=P. 736,735 [para_from,653.1.1,48.1.1.2] -> P* (A*Q)=B. 738,737 [para_from,653.1.1,46.1.1.1] -> (A*Q)*P=B. 763,762 [para_from,659.1.1,48.1.1.2] -> P*P=C*C. 764 [back_demod,666,demod,763] O*O=A*A, O*O=B*B, O*O=C*C, Q*Q=O*O, V*V=O*O, W*W=O*O -> . 801 [para_into,690.1.2,651.1.2,gL-id] -> W* (A*x)=U* (C*x). 811 [para_into,801.1.1.2.2,160.1.2,demod,161,21,163,flip.1] -> U* (C*C)=U. 816,815 [para_into,801.1.1.2,48.1.1] -> W*x=U* (C* (A*x)). 827 [back_demod,764,demod,816,139,69,646] O*O=A*A, O*O=B*B, O*O=C*C, Q*Q=O*O, V*V=O*O -> . 951 [para_into,733.1.1,27.1.2] -> B* (Q*A)=P. 1034 [para_into,811.1.2,715.1.2,gL-id] -> U* (x*C)=O* (x*Q). 1036,1035 [para_into,811.1.2,710.1.2,gL-id] -> U* (C*x)=O* (Q*x). 1038,1037 [para_into,811.1.2,676.1.2,gL-id] -> x* (C*C)=x* (A*A). 1087 [back_demod,651,demod,1036] -> O* (Q*Q)=O. 1099 [back_demod,659,demod,1038] -> P* (A*A)=P. 1112,1111 [para_into,168.1.1.2.2,762.1.2,demod,763,1038,169,flip.1] -> C*C=A*A. 1121 [back_demod,827,demod,1112] O*O=A*A, O*O=B*B, Q*Q=O*O, V*V=O*O -> . 1123,1122 [back_demod,762,demod,1112] -> P*P=A*A. 1131,1130 [para_into,1034.1.1.2.1,737.1.2,demod,738,23,646,9,flip.1] -> O*O=A*A. 1158 [back_demod,1121,demod,1131,1131,1131,1131,unit_del,1,flip.1] B*B=A*A, Q*Q=A*A, V*V=A*A -> . 1234,1233 [para_from,1087.1.1,48.1.1.2,demod,1131,flip.1] -> Q*Q=A*A. 1252 [back_demod,1158,demod,1234,unit_del,1] B*B=A*A, V*V=A*A -> . 1253 [para_into,1099.1.2,951.1.2,gL-id,flip.1] -> B* (Q*x)=P* (A*x). 1266,1265 [para_into,1253.1.1.2.2,32.1.2,demod,33,43,77,1123] -> B*B=A*A. 1282 [back_demod,1252,demod,1266,unit_del,1] V*V=A*A -> . 1441 [para_into,1282.1.1,50.1.2,demod,640] (A* (V* (C*x)))*x=A*A -> . 1449 [para_into,1441.1.1.1.2.2.2,735.1.2,demod,736,69,73,139,1266] A*A=A*A -> . 1450 [binary,1449.1,3.1] -> . ------------ end of proof -------------