----- Otter 3.0.3+, Oct 1994 ----- The job was started by mccune on altair.mcs.anl.gov, Thu Jan 12 15:24:42 1995 ----> UNIT CONFLICT at 28597.93 sec ----> 13342 [binary,13341,3] $F. Length of proof is 125. Level of proof is 16. ---------------- PROOF ---------------- 1 [] h(x,y)=g(x)*g(y)*x*y. 2 [] g(x)=x*x. 3 [] x=x. 5,4 [] x*x*x*y=y. 7,6 [] (x*y)*z=x*y*z. 8 [] h(h(h(A,B),C),D)*E!=E. 9 [copy,8,demod,1,2,2,7,7,1,2,7,7,7,7,7,2,7,7,7,7,7,7,7,7,7,7,7,7,7,7,7,7,7,1,2,7,7,7,7,7,7,7,7,7,7,7,7,7,7,7,7,7,7,7,7,2,7,7,7,7,7,7,7,7,7,7,7,7,7,7,7,7,7,7,7,7,7,7,7,7,7,7,7,7,7,7,7,7,7,7,7,7,7,7,7,7,7,7,7,7,7,7,7,7,7,7,7,7,7,7,7,7,7,7,7,7,7,7,7,7,7,7,7,7,7,7,7,7,7,7,7,7,7,7,7,7,7,7,7,7,7,7,7,7,7,7,7,7,7,7,7,7,7,7,7,7,7,7,7,7,7,7,7,7,7,7,7,7,7,7,7,7,7,7,7,7,7,7,7,7,7,7,7] A*A*B*B*A*B*A*A*B*B*A*B*C*C*A*A*B*B*A*B*C*A*A*B*B*A*B*A*A*B*B*A*B*C*C*A*A*B*B*A*B*C*D*D*A*A*B*B*A*B*A*A*B*B*A*B*C*C*A*A*B*B*A*B*C*D*E!=E. 10 [para_into,6,4,demod,7,7,flip.1] x*y*x*y*x*y*z=z. 16,15 [para_into,10,4] x*y*x*y*x*z=y*y*z. 17 [para_into,15,15] x*y*x*y*z*z*u=y*y*z*x*z*x*u. 20 [para_into,15,4] x*y*x*y*z=y*y*x*x*z. 22,21 [para_into,15,6,demod,7,7,7] x*y*z*x*y*z*x*u=y*z*y*z*u. 23 [copy,17,flip.1] x*x*y*z*y*z*u=z*x*z*x*y*y*u. 24 [copy,20,flip.1] x*x*y*y*z=y*x*y*x*z. 25 [para_into,20,20] x*y*x*z*z*y*y*u=y*y*x*x*z*y*z*u. 28 [para_into,20,6,demod,7,7,7] x*y*z*x*y*z*u=y*z*y*z*x*x*u. 30,29 [para_into,20,4,flip.1] x*x*y*y*x*x*z=y*x*y*z. 31 [para_into,20,6,demod,7,7,7] x*y*z*x*y*z*u=z*z*x*y*x*y*u. 32 [copy,25,flip.1] x*x*y*y*z*x*z*u=y*x*y*z*z*x*x*u. 33 [copy,28,flip.1] x*y*x*y*z*z*u=z*x*y*z*x*y*u. 34 [copy,31,flip.1] x*x*y*z*y*z*u=y*z*x*y*z*x*u. 39 [para_from,20,9,demod,22,16] A*A*B*B*A*B*A*A*B*B*A*B*C*C*A*A*B*B*A*B*C*A*A*B*B*A*B*A*A*B*B*A*B*C*C*A*A*B*B*A*B*C*D*D*A*A*B*A*B*B*C*C*A*A*B*B*A*B*C*D*E!=E. 43 [para_into,17,6,demod,7,7,7] x*y*x*y*z*u*z*u*v=y*y*z*u*x*z*u*x*v. 44 [para_into,17,6,demod,7,7,7] x*y*z*x*y*z*u*u*v=y*z*y*z*u*x*u*x*v. 45 [para_into,17,6,demod,7,7,7] x*y*z*x*y*z*u*u*v=z*z*u*x*y*u*x*y*v. 48 [copy,43,flip.1] x*x*y*z*u*y*z*u*v=u*x*u*x*y*z*y*z*v. 49 [copy,44,flip.1] x*y*x*y*z*u*z*u*v=u*x*y*u*x*y*z*z*v. 50 [copy,45,flip.1] x*x*y*z*u*y*z*u*v=z*u*x*z*u*x*y*y*v. 52 [para_from,17,15] x*y*x*y*z*z*u*x*u*x*v=y*y*z*x*z*u*u*v. 56 [para_into,24,20] x*x*y*z*z*y*y*u=y*x*y*x*z*y*z*u. 62 [para_from,24,17] x*y*x*y*z*u*z*u*v=y*y*u*x*u*x*z*z*v. 73 [para_from,24,20] x*y*x*z*y*z*y*u=y*y*x*x*y*z*z*u. 74 [copy,62,flip.1] x*x*y*z*y*z*u*u*v=z*x*z*x*u*y*u*y*v. 77 [para_into,29,20] x*x*y*y*x*z*z*x*x*u=y*x*y*z*x*z*u. 83 [para_into,29,6,demod,7,7,7] x*x*y*z*y*z*x*x*u=y*z*x*y*z*u. 90 [para_into,21,29] x*y*z*x*y*z*u*x*u*v=y*z*y*z*x*u*u*x*x*v. 97 [para_into,21,29] x*y*x*x*y*z*x*z*u=y*x*y*x*z*z*x*x*u. 100 [para_into,21,21] x*y*z*x*y*x*u*x*u*v=y*z*y*z*u*z*x*u*z*v. 101 [para_into,21,20] x*y*z*x*y*x*x*z*z*u=y*z*y*z*z*x*u. 105 [para_into,21,15] x*y*z*x*y*x*x*u=y*z*y*z*z*x*z*u. 106 [para_into,21,6,demod,7,7,7] x*y*z*u*x*y*z*u*x*v=y*z*u*y*z*u*v. 108 [para_into,21,4] x*y*x*x*y*z=y*x*y*x*x*z. 110,109 [para_into,21,29,demod,5] x*y*y*x*x*y*x*z=y*x*y*y*z. 117 [copy,97,flip.1] x*y*x*y*z*z*y*y*u=y*x*y*y*x*z*y*z*u. 119 [copy,100,flip.1] x*y*x*y*z*y*u*z*y*v=u*x*y*u*x*u*z*u*z*v. 120 [back_demod,39,demod,110,30,30,110,30,30] B*A*B*B*C*A*C*B*B*A*B*C*B*A*B*B*C*A*C*B*B*A*B*C*D*D*A*A*B*A*B*B*C*C*A*A*B*B*A*B*C*D*E!=E. 123 [copy,105,flip.1] x*y*x*y*y*z*y*u=z*x*y*z*x*z*z*u. 136 [para_from,21,15] x*y*x*x*z*x*z*u=y*y*z*y*x*z*y*u. 148 [copy,136,flip.1] x*x*y*x*z*y*x*u=z*x*z*z*y*z*y*u. 154 [para_into,120,20] B*A*B*B*C*A*C*B*B*A*B*C*B*A*B*B*C*A*C*B*B*A*B*C*D*D*A*B*B*A*A*B*C*C*A*A*B*B*A*B*C*D*E!=E. 161 [para_into,23,21,flip.1] x*y*x*y*z*z*u*z*x*u*z*v=y*y*z*x*x*u*x*u*v. 195 [para_from,25,21,demod,5,5,flip.1] x*y*x*y*y*x*x*z=y*x*y*y*z. 227 [para_into,28,6,demod,7,7,7] x*y*z*u*x*y*z*u*v=y*z*u*y*z*u*x*x*v. 229,228 [para_into,28,4,flip.1] x*y*x*y*z*z*y*y*u=z*x*y*z*x*u. 235 [para_into,28,21,flip.1] x*y*x*y*z*z*u*x*y*u*x*v=z*x*y*z*y*u*y*u*v. 237 [para_into,28,20] x*y*z*x*z*z*y*y*u=y*z*y*z*x*x*y*z*u. 238 [para_into,28,15,flip.1] x*y*x*y*z*z*x*y*x*u=z*x*y*z*y*y*u. 240 [para_into,28,4,demod,5] x*y*y*x*z=y*x*x*y*z. 251,250 [para_into,28,25,demod,5,5,5,flip.1] x*y*y*x*y*y*z=y*x*x*z. 254 [copy,227,flip.1] x*y*z*x*y*z*u*u*v=u*x*y*z*u*x*y*z*v. 256,255 [back_demod,117,demod,229,flip.1] x*y*x*x*y*z*x*z*u=z*y*x*z*y*u. 260 [copy,237,flip.1] x*y*x*y*z*z*x*y*u=z*x*y*z*y*y*x*x*u. 302 [para_into,31,20] x*y*z*x*z*z*y*y*u=z*z*x*y*x*y*y*z*u. 310 [copy,302,flip.1] x*x*y*z*y*z*z*x*u=y*z*x*y*x*x*z*z*u. 326,325 [para_from,31,4] x*x*y*y*x*z*x*z*u=z*y*x*z*y*u. 334 [para_into,32,31,demod,5,5,5] x*x*y*x*x*y*z=y*y*x*z. 339,338 [para_from,32,31,demod,5] x*x*y*y*x*y*z*z*x*x*u=y*y*x*y*z*x*z*u. 340 [para_from,32,28,demod,339,256] x*x*y*x*z*y*z*u=y*x*z*x*y*z*x*u. 345 [copy,340,flip.1] x*y*z*y*x*z*y*u=y*y*x*y*z*x*z*u. 351,350 [para_into,33,29,demod,5,5,flip.1] x*y*x*x*y*x*z=y*x*y*z. 353,352 [para_into,33,25,demod,5,flip.1] x*y*z*x*y*z*y*y*u=z*z*x*y*x*u. 370,369 [para_from,33,4] x*x*y*x*z*y*x*z*u=z*x*z*y*y*u. 409 [para_into,240,6,demod,7,7,7] x*y*z*z*x*y*u=z*x*y*x*y*z*u. 417 [para_into,240,20] x*y*x*x*y*y*z=y*x*x*y*y*x*z. 422,421 [para_into,240,29,flip.1] x*y*y*x*y*x*x*z=y*y*x*y*z. 438 [copy,417,flip.1] x*y*y*x*x*y*z=y*x*y*y*x*x*z. 470 [para_from,240,154] B*A*B*B*C*A*C*B*B*A*B*C*B*A*B*B*C*A*C*B*B*A*B*C*D*D*A*B*B*A*A*B*C*C*A*B*A*A*B*B*C*D*E!=E. 564 [para_into,470,24] B*A*B*B*C*A*C*B*B*A*B*C*B*A*B*B*C*A*C*B*B*A*B*C*D*D*A*B*B*A*A*B*C*C*A*B*B*A*B*A*C*D*E!=E. 630 [para_from,48,31,demod,16,5] x*y*z*x*z*y*y*u=y*x*y*z*y*x*z*u. 639 [copy,630,flip.1] x*y*x*z*x*y*z*u=y*x*z*y*z*x*x*u. 645 [para_into,49,48,demod,16,5,5,flip.1] x*y*z*x*y*x*z*x*u=y*z*y*x*z*u. 669 [para_into,50,15,flip.1] x*y*z*x*y*z*u*u*x*y*x*v=z*z*u*x*y*u*y*y*v. 710 [para_into,52,50,demod,422,5,5] x*y*x*y*z*x*z*u=y*y*z*x*x*z*x*u. 713 [copy,710,flip.1] x*x*y*z*z*y*z*u=z*x*z*x*y*z*y*u. 788 [para_into,73,240] x*y*x*z*y*y*z*z*y*u=y*y*x*x*y*z*z*y*z*u. 804 [para_from,74,28,demod,5,5] x*y*x*z*y*z*y*u=y*x*y*y*x*z*z*u. 816 [para_into,77,240,demod,326] x*y*z*x*y*x*z*u=y*z*y*x*z*x*x*u. 823,822 [para_from,77,31,demod,5,229] x*x*y*y*x*y*z*x*z*u=y*z*y*x*z*y*u. 860,859 [para_from,83,45,demod,22,16] x*y*y*x*z*z*y*z*z*u=y*x*x*z*y*y*u. 895 [para_into,90,56,demod,351,251,16] x*y*z*x*y*x*x*z*x*u=y*z*y*x*x*z*u. 1001 [para_into,105,24] x*y*z*x*y*u*x*u*x*v=y*z*y*z*z*x*z*u*u*v. 1011,1010 [para_into,105,101,demod,5,5,flip.1] x*y*x*y*y*z*y*x*z*u=z*x*y*x*z*x*u. 1029 [para_from,105,83,demod,5] x*x*y*z*y*x*x*z*x*u=y*z*x*y*z*z*x*z*z*u. 1046 [para_into,106,6,demod,7,7,7] x*y*z*u*v*x*y*z*u*v*x*w=y*z*u*v*y*z*u*v*w. 1078 [para_into,106,50,demod,251] x*x*y*z*x*z*z*y*y*u=x*y*z*x*y*z*y*z*x*u. 1083 [copy,1078,flip.1] x*y*z*x*y*z*y*z*x*u=x*x*y*z*x*z*z*y*y*u. 1121 [para_from,106,20,flip.1] x*x*y*y*z*u*y*x*z*u*y*v=y*x*x*z*u*x*z*u*v. 1255 [para_into,119,20] x*x*y*y*z*x*u*z*x*v=u*y*x*u*y*u*z*u*z*v. 1258 [para_from,119,100,demod,5,5] x*y*z*y*x*z*y*z*u=y*z*y*x*z*y*z*x*u. 1272 [para_from,123,105,demod,5] x*y*z*y*x*z*y*z*z*u=y*y*x*y*z*x*u. 1400 [para_into,136,240,demod,30,flip.1] x*x*y*x*z*y*x*y*z*u=z*x*y*z*y*y*u. 1563,1562 [para_from,148,108,demod,5] x*y*z*x*z*z*y*z*y*u=y*x*y*z*y*x*u. 1702,1701 [para_into,161,123,demod,1563,5] x*y*x*z*x*y*x*z*u=z*z*y*x*y*u. 1985,1984 [para_from,195,34,flip.1] x*y*z*x*y*z*y*x*x*u=z*z*y*x*y*y*u. 2029,2028 [para_into,227,4,flip.1] x*y*z*x*y*z*u*u*z*z*v=u*x*y*z*u*x*y*v. 2177,2176 [para_into,228,29,demod,2029] x*y*x*y*z*z*y*u*y*u*v=u*z*x*y*u*z*x*v. 2328,2327 [para_into,238,238,demod,1011,5,5,flip.1] x*y*x*z*z*x*y*x*u=z*y*x*y*z*u. 2536,2535 [para_into,254,31,demod,5,flip.1] x*x*y*z*x*x*y*z*u=y*z*y*z*x*u. 2609,2608 [para_into,260,28,demod,2177,5,flip.1] x*y*z*x*z*z*y*y*u*y*z*u*v=u*x*y*z*u*x*v. 3482,3481 [para_from,334,106,demod,5] x*y*z*z*x*y*x*x*z*u=y*z*z*y*z*x*u. 4028,4027 [para_into,409,4,flip.1] x*y*z*y*z*x*z*z*u=y*z*x*x*y*u. 6154,6153 [para_into,639,438,demod,4028,flip.1] x*y*z*x*z*y*y*z*x*x*z*u=y*y*z*x*x*y*x*x*u. 6570,6569 [para_from,788,639,demod,6154] x*y*z*z*x*x*z*y*y*z*y*u=x*x*z*y*y*x*y*y*u. 7266,7265 [para_from,895,227,demod,1985,5,flip.1] x*y*z*x*y*x*z*z*y*z*u=y*y*x*z*x*x*y*u. 8159,8158 [para_into,1010,6,demod,7,7,7] x*y*x*y*y*z*u*y*x*z*u*v=z*u*x*y*x*z*u*x*v. 8183,8182 [para_from,1010,345,demod,2609] x*y*z*y*x*u*z*y*z*u*z*v=y*y*u*x*y*z*u*x*v. 8397 [para_from,1029,564] B*A*B*B*C*A*C*B*B*A*B*C*B*A*C*A*B*C*A*A*B*A*A*C*D*D*A*B*B*A*A*B*C*C*A*B*B*A*B*A*C*D*E!=E. 8711,8710 [para_into,1046,713,demod,5,2536] x*y*y*z*y*x*y*z*x*z*u=z*x*z*x*y*z*x*u. 8754 [back_demod,8397,demod,8711,7266,3482,823] B*A*B*B*C*A*B*C*B*A*C*B*D*D*A*B*B*A*A*B*C*C*A*B*B*A*B*A*C*D*E!=E. 9307,9306 [para_from,1083,1001,demod,5] x*y*y*z*x*y*x*x*z*z*u=y*z*y*z*z*x*y*u. 9606,9605 [para_into,1121,788,demod,6570,860,422,5] x*x*y*y*x*z*z*y*x*x*u=y*x*z*x*y*y*z*u. 9628 [back_demod,8754,demod,9606] B*A*B*B*C*A*B*C*B*A*C*B*D*D*A*A*B*C*B*A*A*C*A*B*A*C*D*E!=E. 11004,11003 [para_into,1255,310,demod,9307,326,5,flip.1] x*y*z*x*y*x*u*z*u*u*x*v=u*y*z*u*y*u*x*z*v. 11052,11051 [para_into,1258,645,demod,8183,8159] x*y*z*y*x*z*z*u*z*y*u*v=u*x*y*z*y*u*x*y*v. 11163,11162 [para_into,1272,669,demod,11052,5,370,flip.1] x*y*x*z*z*u*u*x*y*x*v=u*z*y*x*y*u*z*v. 11967,11966 [para_from,1400,235,demod,353,11163,5,flip.1] x*y*z*x*z*z*u*y*z*y*u*v=y*u*x*y*z*y*u*x*v. 11975,11974 [para_from,1400,50,demod,353,11967,flip.1] x*y*x*z*u*x*y*x*z*u*v=u*u*z*z*y*x*y*v. 13314 [para_into,9628,816,demod,11163] B*A*B*C*A*C*B*A*B*A*D*C*B*C*A*D*A*A*C*A*B*A*C*D*E!=E. 13331 [para_into,13314,20] B*A*B*C*A*C*A*A*B*B*D*C*B*C*A*D*A*A*C*A*B*A*C*D*E!=E. 13335 [para_into,13331,804] A*B*A*A*B*C*C*A*B*B*D*C*B*C*A*D*A*A*C*A*B*A*C*D*E!=E. 13341 [para_into,13335,409,demod,11004,11975,5,2328,1702,5,16,5] E!=E. 13342 [binary,13341,3] $F. ------------ end of proof -------------