----- Otter 3.1-b0, May 2000 ----- ----> UNIT CONFLICT at 10.52 sec ----> 4802 [binary,4801.1,1.1] $F. Length of proof is 93. Level of proof is 21. ---------------- PROOF ---------------- 1 [] x=x. 3,2 [] (x#x)# (y#x)=x. 4 [] x# (y# (x#z))= ((z#y)#y)#x. 6 [] (((((X#Y)# (X# (Z#Y)))# (X# (X# ((U#V)# (V#V)))))# ((X# (X# ((X#Y)# (X# (Z#Y)))))# ((U#V)# (V#V))))# (V# (V# ((W# (V6# (V6# ((W# (V7# (V7#V7)))# ((V7# (V7#W))#V7)))))# ((V6# (V6#W))# ((W# (V7# (V7#V7)))# ((V7# (V7#W))#V7)))))))# ((V# (V# ((((X#Y)# (X# (Z#Y)))# (X# (X# ((U#V)# (V#V)))))# ((X# (X# ((X#Y)# (X# (Z#Y)))))# ((U#V)# (V#V))))))# ((W# (V6# (V6# ((W# (V7# (V7#V7)))# ((V7# (V7#W))#V7)))))# ((V6# (V6#W))# ((W# (V7# (V7#V7)))# ((V7# (V7#W))#V7)))))!=W. 7 [copy,4,flip.1] ((x#y)#y)#z=z# (y# (z#x)). 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. 12 [para_into,4.1.1.2.2,10.1.1,demod,3,flip.1] ((x#y)#y)# ((z#x)# (z#x))=z#x. 16 [para_into,4.1.1.2.2,4.1.1,flip.1] (((x# (y#z))#u)#u)#y=y# (u# (((z#x)#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. 39 [para_into,6.1.1.1.1.2.1.2,4.1.1] (((((X#Y)# (X# (Z#Y)))# (X# (X# ((U#V)# (V#V)))))# ((X# ((((Z#Y)# (X#Y))# (X#Y))#X))# ((U#V)# (V#V))))# (V# (V# ((W# (V6# (V6# ((W# (V7# (V7#V7)))# ((V7# (V7#W))#V7)))))# ((V6# (V6#W))# ((W# (V7# (V7#V7)))# ((V7# (V7#W))#V7)))))))# ((V# (V# ((((X#Y)# (X# (Z#Y)))# (X# (X# ((U#V)# (V#V)))))# ((X# (X# ((X#Y)# (X# (Z#Y)))))# ((U#V)# (V#V))))))# ((W# (V6# (V6# ((W# (V7# (V7#V7)))# ((V7# (V7#W))#V7)))))# ((V6# (V6#W))# ((W# (V7# (V7#V7)))# ((V7# (V7#W))#V7)))))!=W. 49,48 [para_into,25.1.1.1.1,2.1.1,demod,3] (x# (y#x))# (x#x)=x. 51 [back_demod,29,demod,49] x#y=y#x. 56 [para_into,51.1.1,25.1.1,flip.1] x# ((x#y)#y)=x#x. 59,58 [para_into,51.1.1,10.1.1,flip.1] x# ((y#x)# (y#x))=y#x. 64,63 [para_into,51.1.1,2.1.1,flip.1] (x#y)# (y#y)=y. 67 [back_demod,39,demod,64,64,64,64] (((((X#Y)# (X# (Z#Y)))# (X# (X#V)))# ((X# ((((Z#Y)# (X#Y))# (X#Y))#X))#V))# (V# (V# ((W# (V6# (V6# ((W# (V7# (V7#V7)))# ((V7# (V7#W))#V7)))))# ((V6# (V6#W))# ((W# (V7# (V7#V7)))# ((V7# (V7#W))#V7)))))))# ((V# (V# ((((X#Y)# (X# (Z#Y)))# (X# (X#V)))# ((X# (X# ((X#Y)# (X# (Z#Y)))))#V))))# ((W# (V6# (V6# ((W# (V7# (V7#V7)))# ((V7# (V7#W))#V7)))))# ((V6# (V6#W))# ((W# (V7# (V7#V7)))# ((V7# (V7#W))#V7)))))!=W. 71 [para_from,51.1.1,25.1.1.1] (x# (y#x))#y=y#y. 73 [para_from,51.1.1,10.1.1.1.2] ((x#y)# (y#x))#y=x#y. 75 [para_from,51.1.1,10.1.1.1.1] ((x#y)# (y#x))#x=y#x. 82,81 [para_from,51.1.1,2.1.1.2] (x#x)# (x#y)=x. 86,85 [para_into,63.1.1.1,51.1.1] (x#y)# (x#x)=x. 96,95 [para_from,81.1.1,63.1.1.1] x# ((x#y)# (x#y))=x#y. 100,99 [para_from,81.1.1,2.1.1.2] ((x#y)# (x#y))#x=x#y. 112 [para_into,7.1.1.1,51.1.1] (x# (y#x))#z=z# (x# (z#y)). 171 [para_into,56.1.1.2.1,51.1.1] x# ((y#x)#y)=x#x. 177 [para_into,56.1.1.2,51.1.1] x# (y# (x#y))=x#x. 190 [para_from,56.1.1,4.1.1.2,demod,86,flip.1] ((x#y)#y)# (y#x)=y. 249 [para_into,12.1.1.1,7.1.1] (x# (x# (x#y)))# ((z# (y#x))# (z# (y#x)))=z# (y#x). 284,283 [para_into,71.1.1.1.2,51.1.1] (x# (x#y))#y=y#y. 403,402 [para_into,171.1.1.2,51.1.1] x# (y# (y#x))=x#x. 415 [para_from,171.1.1,4.1.1.2,demod,64,flip.1] ((x#y)#y)# (x#y)=y. 548 [para_into,177.1.1,4.1.1] ((x#x)#x)#y=y#y. 553 [copy,548,flip.1] x#x= ((y#y)#y)#x. 560 [para_from,177.1.1,4.1.1.2,flip.1] (((x#y)#x)#x)#y=y# (x#x). 570,569 [para_into,190.1.1.1.1,81.1.1,demod,86] (x# (x#y))#x=x#y. 583 [para_into,190.1.1.1.1,2.1.1,demod,64] (x# (y#x))#x=y#x. 585 [para_into,190.1.1.1,51.1.1] (x# (y#x))# (x#y)=x. 589 [para_into,190.1.1.1,7.1.1] (x# (x# (x#y)))# (x# (y#x))=x. 606 [back_demod,67,demod,570,570,570,570] (((((X#Y)# (X# (Z#Y)))# (X# (X#V)))# ((X# ((((Z#Y)# (X#Y))# (X#Y))#X))#V))# (V# (V# ((W# (V6# (V6# ((W# (V7# (V7#V7)))# (V7#W)))))# ((V6# (V6#W))# ((W# (V7# (V7#V7)))# (V7#W)))))))# ((V# (V# ((((X#Y)# (X# (Z#Y)))# (X# (X#V)))# ((X# (X# ((X#Y)# (X# (Z#Y)))))#V))))# ((W# (V6# (V6# ((W# (V7# (V7#V7)))# (V7#W)))))# ((V6# (V6#W))# ((W# (V7# (V7#V7)))# (V7#W)))))!=W. 695 [para_from,402.1.1,4.1.1.2,flip.1] (((x#y)#y)#y)#x=x# (y#y). 789,788 [para_into,415.1.1.1,51.1.1] (x# (y#x))# (y#x)=x. 792 [para_into,415.1.1.1,7.1.1] (x# (x# (x#y)))# ((y#x)#x)=x. 798 [para_into,415.1.1,51.1.1] (x#y)# ((x#y)#y)=y. 827 [para_into,548.1.1,51.1.1] x# ((y#y)#y)=x#x. 833 [copy,827,flip.1] x#x=x# ((y#y)#y). 836,835 [para_from,548.1.1,16.1.1.1,demod,100,789,flip.1] x# ((x#y)# (y#x))=x#y. 893 [para_from,553.1.1,63.1.1.2] (x#y)# (((z#z)#z)#y)=y. 940,939 [para_into,569.1.1.1,51.1.1] ((x#y)#x)#x=x#y. 943 [para_into,569.1.1.1,4.1.1] (((x#y)#y)#y)#y=y# (y#x). 946,945 [para_into,569.1.1,51.1.1] x# (x# (x#y))=x#y. 948,947 [back_demod,560,demod,940] (x#y)#y=y# (x#x). 951 [back_demod,28,demod,948,96,948] (x#y)#z=z# ((z# (y#y))#x). 953 [back_demod,792,demod,946,948] (x#y)# (x# (y#y))=x. 956,955 [back_demod,589,demod,946] (x#y)# (x# (y#x))=x. 958,957 [back_demod,249,demod,946] (x#y)# ((z# (y#x))# (z# (y#x)))=z# (y#x). 961 [back_demod,943,demod,948,948,96] x# (y#y)=x# (x#y). 997,996 [back_demod,893,demod,948] (x#y)# ((z# (z#z))#y)=y. 1017 [back_demod,833,demod,948] x#x=x# (y# (y#y)). 1037 [back_demod,798,demod,948] (x#y)# (y# (x#x))=y. 1095 [back_demod,695,demod,948] ((x# (y#y))#x)#y=y# (x#x). 1153 [back_demod,606,demod,948] (((((X#Y)# (X# (Z#Y)))# (X# (X#V)))# ((X# (((X#Y)# ((Z#Y)# (Z#Y)))#X))#V))# (V# (V# ((W# (V6# (V6# ((W# (V7# (V7#V7)))# (V7#W)))))# ((V6# (V6#W))# ((W# (V7# (V7#V7)))# (V7#W)))))))# ((V# (V# ((((X#Y)# (X# (Z#Y)))# (X# (X#V)))# ((X# (X# ((X#Y)# (X# (Z#Y)))))#V))))# ((W# (V6# (V6# ((W# (V7# (V7#V7)))# (V7#W)))))# ((V6# (V6#W))# ((W# (V7# (V7#V7)))# (V7#W)))))!=W. 1325,1324 [back_demod,190,demod,948] (x# (y#y))# (x#y)=x. 1398,1397 [para_into,583.1.1.1,51.1.1,demod,948] (x# (y#y))#x=y#x. 1402,1401 [back_demod,1095,demod,1398] (x#y)#x=x# (y#y). 1455 [para_into,585.1.1.2,585.1.1,demod,956,1402,59,948] x# (y#y)=x# (y#x). 1456 [copy,1455,flip.1] x# (y#x)=x# (y#y). 1470,1469 [para_from,73.1.1,177.1.1.2.2,flip.1] ((x#y)# (y#x))# ((x#y)# (y#x))= ((x#y)# (y#x))# (y# (x#y)). 1485 [para_into,947.1.1.1,585.1.1,demod,958] x# (x#y)=x# (y#x). 1502 [copy,1485,flip.1] x# (y#x)=x# (x#y). 1523,1522 [para_from,75.1.1,73.1.1.1.2,demod,836,1470,836] ((x#y)# (y#x))# (y# (x#y))=x#y. 1529,1528 [back_demod,1469,demod,1523] ((x#y)# (y#x))# ((x#y)# (y#x))=x#y. 1551,1550 [para_into,953.1.1.2,51.1.1] (x#y)# ((y#y)#x)=x. 1567 [para_into,961.1.1,51.1.1] (x#x)#y=y# (y#x). 1571 [copy,1567,flip.1] x# (x#y)= (y#y)#x. 1651,1650 [para_from,1017.1.1,2.1.1.1] (x# (y# (y#y)))# (z#x)=x. 1653 [back_demod,1153,demod,1651,403,1651,284,82,1651,403,1651,284,82] (((((X#Y)# (X# (Z#Y)))# (X# (X#V)))# ((X# (((X#Y)# ((Z#Y)# (Z#Y)))#X))#V))# (V# (V#W)))# ((V# (V# ((((X#Y)# (X# (Z#Y)))# (X# (X#V)))# ((X# (X# ((X#Y)# (X# (Z#Y)))))#V))))#W)!=W. 1659,1658 [para_into,1037.1.1.1,75.1.1,demod,1529] (x#y)# (y# (y#x))=y. 2177 [para_into,112.1.1.1.2,1571.1.1,demod,1551,flip.1] x# ((y#z)# (x#y))=y#x. 2183 [para_into,112.1.1.1.2,1502.1.1,demod,1659,flip.1] x# ((y#z)# (x#z))=z#x. 2190,2189 [para_into,112.1.1.1.2,1037.1.1,demod,1402,82,flip.1] x# ((y# (z#z))# (x# (z#y)))= (y#z)#x. 3014 [para_into,2177.1.1.2.1,947.1.1,demod,2190] (x#y)#z= (y#x)#z. 3094 [para_into,2177.1.1.2,51.1.1] x# ((x#y)# (y#z))=y#x. 3212 [para_into,3014.1.1,51.1.1] x# (y#z)= (z#y)#x. 3236 [copy,3212,flip.1] (x#y)#z=z# (y#x). 3637,3636 [para_into,3236.1.1,1456.1.1,flip.1] (x# (y#z))# (z#y)= (y#z)# (x#x). 3959,3958 [para_from,2183.1.1,71.1.1.1.2,demod,3637] ((x#y)# ((z#y)# (z#y)))#x=x#x. 3968 [back_demod,1653,demod,3959] (((((X#Y)# (X# (Z#Y)))# (X# (X#V)))# ((X# (X#X))#V))# (V# (V#W)))# ((V# (V# ((((X#Y)# (X# (Z#Y)))# (X# (X#V)))# ((X# (X# ((X#Y)# (X# (Z#Y)))))#V))))#W)!=W. 4484 [para_into,3094.1.1.2.1,953.1.1,demod,1325] (x#y)# (x# ((x# (y#y))#z))=x. 4658,4657 [para_into,951.1.1,3236.1.1,flip.1] x# ((x# (y#y))#z)=x# (y#z). 4667 [back_demod,4484,demod,4658] (x#y)# (x# (y#z))=x. 4748,4747 [para_into,4667.1.1.2.2,3094.1.1] (x#y)# (x# (z#y))=x. 4801 [back_demod,3968,demod,4748,946,997,946,4748,946,4748,997,997] W!=W. 4802 [binary,4801.1,1.1] $F. ------------ end of proof -------------