----- Otter 3.1-b0, May 2000 ----- ----> UNIT CONFLICT at 5.38 sec ----> 2437 [binary,2436.1,1799.1] $F. Length of proof is 62. Level of proof is 16. ---------------- PROOF ---------------- 127 [] x=x. 128 [] (x#y)# (x# (z#y))=x. 130 [] x#y=y#x. 131 [] ((Z#Y)#Y)#X!=X# (Y# (X#Z))| (X#X)# (Y#X)!=X. 132 [para_into,128.1.1.1,128.1.1] x# ((x#y)# (z# (x# (u#y))))=x#y. 137,136 [para_into,128.1.1.2,128.1.1] ((x#y)# (z#y))#x=x#y. 138 [para_into,132.1.1.2.2,128.1.1] x# ((x#y)#x)=x#y. 140 [para_into,132.1.1.2,132.1.1] x# ((x# (y#z))#z)=x# (y#z). 146 [para_into,136.1.1.1.2,136.1.1] ((x#y)# (y#z))#x=x#y. 150 [para_from,136.1.1,132.1.1.2.2] x# ((x#y)# ((x# (z#y))#u))=x#y. 154 [para_from,136.1.1,128.1.1.2.2] (x#y)# (x# (y#z))=x. 159,158 [para_from,138.1.1,128.1.1.2] (x#x)# (x#y)=x. 169,168 [para_into,140.1.1.2.1.2,136.1.1,demod,137] x# ((x# (y#z))#y)=x# (y#z). 173,172 [para_into,140.1.1.2,136.1.1,demod,159,flip.1] (x#x)# (y#x)=x. 174 [back_demod,131,demod,173,unit_del,127] ((Z#Y)#Y)#X!=X# (Y# (X#Z)). 179 [para_into,130.1.1,140.1.1,flip.1] ((x# (y#z))#z)#x=x# (y#z). 187 [para_into,130.1.1,128.1.1,flip.1] (x# (y#z))# (x#z)=x. 189 [para_from,130.1.1,140.1.1.2] x# (y# (x# (z#y)))=x# (z#y). 191 [para_from,130.1.1,140.1.1.2.1] x# (((y#z)#x)#z)=x# (y#z). 193 [para_from,130.1.1,140.1.1.2.1.2,demod,169] x# (y#z)=x# (z#y). 195,194 [para_from,130.1.1,138.1.1.2] x# (x# (x#y))=x#y. 196 [para_from,130.1.1,136.1.1.1] ((x#y)# (z#y))#z=z#y. 202 [para_from,130.1.1,128.1.1.2] (x#y)# ((z#y)#x)=x. 252 [para_from,158.1.1,150.1.1.2.2.1.2] x# ((x# (y#z))# ((x#y)#u))=x# (y#z). 256 [para_into,168.1.1.2.1,130.1.1] x# (((y#z)#x)#y)=x# (y#z). 292 [para_into,174.1.1.1.1,130.1.1] ((Y#Z)#Y)#X!=X# (Y# (X#Z)). 304,303 [para_into,187.1.1.1,130.1.1] ((x#y)#z)# (z#y)=z. 360 [para_into,193.1.1,130.1.1] (x#y)#z=z# (y#x). 382 [para_into,194.1.1,130.1.1] (x# (x#y))#x=x#y. 450 [para_into,202.1.1.2.1,187.1.1] (x# (y#z))# (y#x)=x. 517 [para_from,154.1.1,189.1.1.2,flip.1] x# (y# (x#y))=x#x. 687 [para_from,303.1.1,196.1.1.1.2,demod,304] ((x# (y#z))#y)# ((u#z)#y)=y. 700 [para_into,360.1.1.1,193.1.1] (x# (y#z))#u=u# ((z#y)#x). 728 [para_from,360.1.1,146.1.1.1] ((x#y)# (x#z))#z=z#x. 853 [para_from,450.1.1,179.1.1.1,flip.1] x# (y# (y#x))=x#x. 918 [para_into,517.1.1.2.2,191.1.1] x# ((((y#z)#x)#z)# (x# (y#z)))=x#x. 932 [para_into,517.1.1,130.1.1] (x# (y#x))#y=y#y. 1193 [para_into,853.1.1,130.1.1] (x# (x#y))#y=y#y. 1199 [para_from,853.1.1,189.1.1.2] x# (y#y)=x# (x#y). 1227 [copy,1199,flip.1] x# (x#y)=x# (y#y). 1237 [para_into,918.1.1.2.2,130.1.1] x# ((((y#z)#x)#z)# ((y#z)#x))=x#x. 1249 [para_into,932.1.1.1.2,256.1.1] ((((x#y)#z)#x)# (z# (x#y)))#z=z#z. 1275 [para_from,932.1.1,168.1.1.2] x# (y#y)=x# (y#x). 1293 [copy,1275,flip.1] x# (y#x)=x# (y#y). 1329 [para_from,1193.1.1,179.1.1.1] (x#x)#y=y# (y#x). 1350,1349 [para_into,1199.1.1.2,1199.1.1,demod,173,flip.1] x# (x# (y#y))=x#y. 1404,1403 [para_from,1199.1.1,382.1.1.1.2,demod,195] (x#y)#x=x# (y#y). 1435 [back_demod,1237,demod,1404] x# (((y#z)#x)# (z#z))=x#x. 1458 [back_demod,292,demod,1404] (Y# (Z#Z))#X!=X# (Y# (X#Z)). 1470,1469 [para_into,1227.1.1,360.1.1] ((x#y)#z)# (y#x)= (x#y)# (z#z). 1477 [back_demod,1249,demod,1470] (((x#y)#z)# (x#x))#z=z#z. 1762 [para_into,1435.1.1.2.1.1,1199.1.1,demod,159] x# (((y# (y#z))#x)#z)=x#x. 1799 [para_into,1458.1.1,700.1.1] X# ((Z#Z)#Y)!=X# (Y# (X#Z)). 1848 [para_from,1477.1.1,191.1.1.2] (x#x)# (y#y)= (x#x)# ((x#z)#y). 1976 [para_into,1762.1.1.2.1,130.1.1] x# ((x# (y# (y#z)))#z)=x#x. 2015 [para_into,1848.1.1.1,1848.1.1,demod,1404,159,159] x# (y#y)=x# (((x#x)#z)#y). 2080 [para_into,1976.1.1,252.1.1] x# (y# (y# ((x#y)#z)))=x#x. 2107,2106 [para_into,2015.1.1,1199.1.1,flip.1] x# (((x#x)#y)#z)=x# (x#z). 2116 [para_into,2080.1.1.2.2.2,360.1.1] x# (y# (y# (z# (y#x))))=x#x. 2181 [para_into,2106.1.1.2,1293.1.1,demod,2107,1350,flip.1] x# (x# (y# ((x#x)#z)))=x#y. 2272 [para_into,2181.1.1.2.2,728.1.1,demod,2107,195,flip.1] x# ((y#z)# (y# ((x#x)#u)))=x#y. 2274 [para_into,2181.1.1.2.2,687.1.1,flip.1] x# ((y# (z#x))#z)=x# (x#z). 2328 [para_into,2272.1.1.2.2.2.1,1848.1.1,demod,1404,159] (x#x)# ((y#z)# (y# (x#u)))= (x#x)#y. 2356 [para_into,2274.1.1.2.1.2,1329.1.1,demod,1350] x# ((y# (x# (x#z)))# (z#z))=x#z. 2421,2420 [para_into,2328.1.1.2.2.2,130.1.1] (x#x)# ((y#z)# (y# (u#x)))= (x#x)#y. 2436 [para_into,2356.1.1.2.1,2116.1.1,demod,2421] x# ((y#y)#z)=x# (z# (x#y)). 2437 [binary,2436.1,1799.1] $F. ------------ end of proof -------------