----- Otter 3.1-b0, May 2000 ----- ----> UNIT CONFLICT at 0.88 sec ----> 393 [binary,392.1,51.1] $Ans(Veroff). Length of proof is 24. Level of proof is 12. ---------------- PROOF ---------------- 1 [] x=x. 3,2 [] (((((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. 4 [] (A#C)# (A# (B#C))!=A|B#A!=A#B|$Ans(Veroff). 6,5 [para_into,2.1.1.1.1.2.1,2.1.1,demod,3] (((((x# (((y#z)# (y# (u#z)))#y))#y)# (((y#z)# (y# (u#z)))# (x# (y#y))))# (v#y))#y)# (v# ((((x# (((y#z)# (y# (u#z)))#y))#y)# (((y#z)# (y# (u#z)))# (x# (y#y))))# (y#y)))=v. 7 [back_demod,2,demod,6] ((x# (x#y))#y)# (x# (x# (y#y)))=y. 15 [para_into,5.1.1.1.1.1,5.1.1,demod,6] ((((x#y)# (x# (z#y)))# (u#x))#x)# (u# (((x#y)# (x# (z#y)))# (x#x)))=u. 17 [para_into,5.1.1,7.1.1,flip.1] ((x# (((y#z)# (y# (u#z)))#y))#y)# (((y#z)# (y# (u#z)))# (x# (y#y)))=y. 48,47 [para_into,15.1.1,7.1.1,flip.1] (x#y)# (x# (z#y))=x. 49 [back_demod,17,demod,48,48] ((x# (y#y))#y)# (y# (x# (y#y)))=y. 51 [back_demod,4,demod,48,unit_del,1] B#A!=A#B|$Ans(Veroff). 60 [para_into,47.1.1.2.2,47.1.1] (x# (y# (z#u)))# (x#y)=x. 66 [para_into,47.1.1.2,47.1.1] ((x#y)# (z#y))#x=x#y. 98 [para_into,60.1.1.1.2,47.1.1] (x#y)# (x# (y#z))=x. 106 [para_into,60.1.1.1,47.1.1] x# ((x#y)#x)=x#y. 198 [para_from,98.1.1,47.1.1.2] ((x#y)# (y#z))#x=x#y. 221,220 [para_from,106.1.1,47.1.1.2] (x#x)# (x#y)=x. 238 [para_into,220.1.1.1,220.1.1] x# ((x#x)#y)=x#x. 253,252 [para_from,220.1.1,47.1.1.2] ((x#x)#y)#x=x#x. 264 [para_from,220.1.1,7.1.1.2.2,demod,253] (x#x)# ((x#x)#x)=x. 303,302 [para_from,238.1.1,47.1.1.2] (x#y)# (x#x)=x. 318 [para_from,264.1.1,47.1.1.2.2] (x# ((y#y)#y))# (x#y)=x. 321,320 [para_into,66.1.1.1.1,302.1.1,demod,303] (x# (y# (x#x)))# (x#z)=x. 377,376 [para_from,49.1.1,198.1.1.1,flip.1] (x# (y#y))#y=y# (x# (y#y)). 379,378 [para_from,49.1.1,318.1.1.2,demod,377,321,48,377,flip.1] x# (y# (x#x))=x#x. 380 [para_from,49.1.1,198.1.1.1.2,demod,377,379,377,379,377,379] (x#x)#y=y# (x#x). 384 [para_into,378.1.1.2.2,302.1.1,demod,221] (x#x)# (y#x)=x. 392 [para_into,380.1.1.1,384.1.1,demod,221] x#y=y#x. 393 [binary,392.1,51.1] $Ans(Veroff). ------------ end of proof -------------