----- Otter 3.1-b0, May 2000 ----- ----> UNIT CONFLICT at 14.07 sec ----> 5807 [binary,5806.1,1.1] $F. Length of proof is 75. Level of proof is 24. ---------------- PROOF ---------------- 1 [] x=x. 3,2 [] (x#x)# (y#x)=x. 4 [] x# (y# (x#z))= ((z#y)#y)#x. 6 [] (((((X# (((Y#Z)# (Y# (U#Z)))#Y))#Y)# (((Y#Z)# (Y# (U#Z)))# (X# (Y#Y))))# ((((V# (V#W))#W)# (V# (V# (W#W))))#Y))#Y)# ((((V# (V#W))#W)# (V# (V# (W#W))))# ((((X# (((Y#Z)# (Y# (U#Z)))#Y))#Y)# (((Y#Z)# (Y# (U#Z)))# (X# (Y#Y))))# (Y#Y)))!=W. 7 [copy,4,flip.1] ((x#y)#y)#z=z# (y# (z#x)). 9,8 [para_into,2.1.1.1,2.1.1] x# (y# (x#x))=x#x. 10 [para_into,2.1.1.2,2.1.1] ((x#y)# (x#y))#y=x#y. 23 [para_into,4.1.1.2,4.1.1] x# (((y#x)#x)#z)= (((z#y)#z)#z)#x. 24 [para_into,4.1.1.2,2.1.1] x#y= ((y# (y#y))# (y#y))#x. 25 [para_into,4.1.1,8.1.1,flip.1] ((x#y)#y)#x=x#x. 28 [copy,23,flip.1] (((x#y)#x)#x)#z=z# (((y#z)#z)#x). 29 [copy,24,flip.1] ((x# (x#x))# (x#x))#y=y#x. 47,46 [para_into,25.1.1.1.1,2.1.1,demod,3] (x# (y#x))# (x#x)=x. 49 [back_demod,29,demod,47] x#y=y#x. 54 [para_into,49.1.1,25.1.1,flip.1] x# ((x#y)#y)=x#x. 57,56 [para_into,49.1.1,10.1.1,flip.1] x# ((y#x)# (y#x))=y#x. 59,58 [para_into,49.1.1,8.1.1,flip.1] (x# (y#y))#y=y#y. 62,61 [para_into,49.1.1,2.1.1,flip.1] (x#y)# (y#y)=y. 66 [para_from,49.1.1,25.1.1.1] (x# (y#x))#y=y#y. 77,76 [para_from,49.1.1,2.1.1.2] (x#x)# (x#y)=x. 81,80 [para_into,61.1.1.1,49.1.1] (x#y)# (x#x)=x. 91,90 [para_from,76.1.1,61.1.1.1] x# ((x#y)# (x#y))=x#y. 108 [para_into,54.1.1.2.1,49.1.1] x# ((y#x)#y)=x#x. 113 [para_into,54.1.1.2,49.1.1] x# (y# (x#y))=x#x. 120 [para_from,54.1.1,4.1.1.2,demod,81,flip.1] ((x#y)#y)# (y#x)=y. 125 [para_into,6.1.1.1.1.1.1.1.2.1.2.2,49.1.1] (((((X# (((Y#Z)# (Y# (Z#U)))#Y))#Y)# (((Y#Z)# (Y# (U#Z)))# (X# (Y#Y))))# ((((V# (V#W))#W)# (V# (V# (W#W))))#Y))#Y)# ((((V# (V#W))#W)# (V# (V# (W#W))))# ((((X# (((Y#Z)# (Y# (U#Z)))#Y))#Y)# (((Y#Z)# (Y# (U#Z)))# (X# (Y#Y))))# (Y#Y)))!=W. 185,184 [para_into,66.1.1.1.2,49.1.1] (x# (x#y))#y=y#y. 231 [back_demod,125,demod,185,185] (((((X# (((Y#Z)# (Y# (Z#U)))#Y))#Y)# (((Y#Z)# (Y# (U#Z)))# (X# (Y#Y))))# (((W#W)# (V# (V# (W#W))))#Y))#Y)# (((W#W)# (V# (V# (W#W))))# ((((X# (((Y#Z)# (Y# (U#Z)))#Y))#Y)# (((Y#Z)# (Y# (U#Z)))# (X# (Y#Y))))# (Y#Y)))!=W. 295,294 [para_into,108.1.1.2,49.1.1] x# (y# (y#x))=x#x. 299 [back_demod,231,demod,295,77,295,77] (((((X# (((Y#Z)# (Y# (Z#U)))#Y))#Y)# (((Y#Z)# (Y# (U#Z)))# (X# (Y#Y))))# (W#Y))#Y)# (W# ((((X# (((Y#Z)# (Y# (U#Z)))#Y))#Y)# (((Y#Z)# (Y# (U#Z)))# (X# (Y#Y))))# (Y#Y)))!=W. 335 [para_from,108.1.1,4.1.1.2,demod,62,flip.1] ((x#y)#y)# (x#y)=y. 351 [para_from,113.1.1,4.1.1.2,flip.1] (((x#y)#x)#x)#y=y# (x#x). 361 [para_into,120.1.1.1.1,76.1.1,demod,81] (x# (x#y))#x=x#y. 371 [para_into,120.1.1.1.1,2.1.1,demod,62] (x# (y#x))#x=y#x. 373 [para_into,120.1.1.1,49.1.1] (x# (y#x))# (x#y)=x. 427 [para_from,294.1.1,4.1.1.2,flip.1] (((x#y)#y)#y)#x=x# (y#y). 452 [para_into,7.1.1.1,49.1.1] (x# (y#x))#z=z# (x# (z#y)). 507 [para_from,7.1.1,120.1.1.1] (x# (x# (x#y)))# (x# (y#x))=x. 565 [para_into,335.1.1.1,7.1.1] (x# (x# (x#y)))# ((y#x)#x)=x. 571 [para_into,335.1.1,49.1.1] (x#y)# ((x#y)#y)=y. 686,685 [para_into,361.1.1.1,49.1.1] ((x#y)#x)#x=x#y. 689 [para_into,361.1.1.1,4.1.1] (((x#y)#y)#y)#y=y# (y#x). 692,691 [para_into,361.1.1,49.1.1] x# (x# (x#y))=x#y. 694,693 [back_demod,351,demod,686] (x#y)#y=y# (x#x). 695 [back_demod,28,demod,694,91,694] (x#y)#z=z# ((z# (y#y))#x). 697 [back_demod,565,demod,692,694] (x#y)# (x# (y#y))=x. 700,699 [back_demod,507,demod,692] (x#y)# (x# (y#x))=x. 703 [back_demod,689,demod,694,694,91] x# (y#y)=x# (x#y). 761 [back_demod,571,demod,694] (x#y)# (y# (x#x))=y. 842 [back_demod,427,demod,694] ((x# (y#y))#x)#y=y# (x#x). 901,900 [back_demod,120,demod,694] (x# (y#y))# (x#y)=x. 950,949 [para_into,371.1.1.1,49.1.1,demod,694] (x# (y#y))#x=y#x. 954,953 [back_demod,842,demod,950] (x#y)#x=x# (y#y). 969 [para_into,373.1.1.2,373.1.1,demod,700,954,57,694] x# (y#y)=x# (y#x). 1120 [para_into,761.1.1.2,703.1.1] (x#y)# (y# (y#x))=y. 1123,1122 [para_into,761.1.1.2,49.1.1] (x#y)# ((x#x)#y)=y. 1230 [para_into,969.1.1,703.1.1] x# (x#y)=x# (y#x). 1233 [para_into,969.1.1,49.1.1] (x#x)#y=y# (x#y). 1236 [copy,1230,flip.1] x# (y#x)=x# (x#y). 1237 [copy,1233,flip.1] x# (y#x)= (y#y)#x. 1729 [para_into,452.1.1.1.2,1237.1.1,demod,1123,flip.1] x# ((y#z)# (x#z))=z#x. 1732 [para_into,452.1.1.1.2,1230.1.1,demod,700,flip.1] x# ((y#z)# (x#y))=y#x. 1738,1737 [para_into,452.1.1.1.2,1120.1.1,demod,954,91,flip.1] x# ((y# (y#z))# (x# (z#y)))= (y#z)#x. 2032 [para_into,1729.1.1.2.1,1236.1.1,demod,1738] (x#y)#z= (y#x)#z. 2256 [para_into,2032.1.1,49.1.1] x# (y#z)= (z#y)#x. 2277 [copy,2256,flip.1] (x#y)#z=z# (y#x). 2587 [para_from,2277.1.1,1729.1.1.2] x# ((x#y)# (y#z))=y#x. 2867,2866 [para_into,1732.1.1.2,2256.1.1] x# ((y#x)# (y#z))=y#x. 2870 [para_into,1732.1.1,2256.1.1] ((x#y)# (y#z))#x=y#x. 3660 [para_into,2587.1.1.2.1,697.1.1,demod,901] (x#y)# (x# ((x# (y#y))#z))=x. 4028 [para_into,2870.1.1.1.1,697.1.1,demod,901] (x# ((x# (y#y))#z))# (x#y)=x. 5139 [para_into,299.1.1.1.1.1.2.1,49.1.1] (((((X# (((Y#Z)# (Y# (Z#U)))#Y))#Y)# (((Y# (U#Z))# (Y#Z))# (X# (Y#Y))))# (W#Y))#Y)# (W# ((((X# (((Y#Z)# (Y# (U#Z)))#Y))#Y)# (((Y#Z)# (Y# (U#Z)))# (X# (Y#Y))))# (Y#Y)))!=W. 5541,5540 [para_into,695.1.1,2277.1.1,flip.1] x# ((x# (y#y))#z)=x# (y#z). 5545 [back_demod,4028,demod,5541] (x# (y#z))# (x#y)=x. 5550,5549 [back_demod,3660,demod,5541] (x#y)# (x# (y#z))=x. 5620 [back_demod,5139,demod,5550,59] ((((Y#Y)# (((Y# (U#Z))# (Y#Z))# (X# (Y#Y))))# (W#Y))#Y)# (W# ((((X# (((Y#Z)# (Y# (U#Z)))#Y))#Y)# (((Y#Z)# (Y# (U#Z)))# (X# (Y#Y))))# (Y#Y)))!=W. 5648,5647 [para_into,5545.1.1.1.2,2866.1.1] (x# (y#z))# (x#z)=x. 5662,5661 [para_into,5545.1.1.1.2,1122.1.1] (x#y)# (x# (z#y))=x. 5806 [back_demod,5620,demod,5648,9,77,954,2867,5662,59,5662,9,77,5550] W!=W. 5807 [binary,5806.1,1.1] $F. ------------ end of proof -------------