Here is Otter's proof in Son of BirdBrain's format:
Searching ... Success, in 1.28 seconds! ---------------- PROOF ---------------- 1 n(n(A)+B)+n(n(A)+n(B))!=A. [] 2 x=x. [] 3 x+y=y+x. [] 5,4 (x+y)+z=x+ (y+z). [] 6 n(n(x+y)+n(x+n(y)))=x. [] 8 x+x=x. [] 10 n(n(A)+n(B))+n(n(A)+B)!=A. [para_from,3,1] 13 x+ (x+y)=x+y. [para_into,4,8,flip.1] 15 x+ (y+z)=y+ (x+z). [para_into,4,3,demod,5] 23,22 x+ (y+x)=x+y. [para_into,13,3] 26 n(n(x)+n(x+n(x)))=x. [para_into,6,8] 36 n(n(n(x)+x)+n(n(x)))=n(x). [para_into,6,8] 42 n(n(x+n(y))+n(x+y))=x. [para_into,6,3] 52 x+ (y+z)=x+ (z+y). [para_into,15,3,demod,5] 81,80 n(n(x+n(x))+n(x))=x. [para_into,26,3] 82 n(n(n(x)+x)+x)=n(x). [para_from,26,6,demod,23] 125 n(n(n(x+n(x))+ (n(x)+x))+x)=n(x+n(x))+n(x). [para_into,80,80,demod,5,81] 139 n(n(n(x+n(x))+x)+x)=n(x+n(x)). [para_from,80,6] 166,165 n(n(x+n(x))+x)=n(x). [para_into,82,3] 180,179 n(n(x)+x)=n(x+n(x)). [back_demod,139,demod,166] 195 n(n(x+n(x))+n(n(x)))=n(x). [back_demod,36,demod,180] 197 n(n(x+ (n(x)+n(x+n(x))))+ (n(x+n(x))+x))=n(x). [para_into,165,165,demod,5,180,5,166] 206,205 n(n(x+ (n(x)+n(x+n(x))))+n(x))=n(x+n(x))+x. [para_from,165,80,demod,166,5,180,5] 223,222 n(n(x+y)+ (y+x))=n(x+ (y+n(x+y))). [para_into,179,52,demod,5] 231,230 n(n(x+ (n(x)+n(x+n(x))))+x)=n(x+n(x))+n(x). [back_demod,125,demod,223] 564,563 n(x+n(x))+x=x. [para_into,195,80,demod,5,223,81,206,81] 582,581 n(x+n(x))+n(x)=n(x). [back_demod,197,demod,564,231] 586,585 n(n(x))=x. [back_demod,80,demod,582] 606,605 n(x+n(y))+n(x+y)=n(x). [para_into,585,42,flip.1] 621 A!=A. [back_demod,10,demod,606,586] 622 $F. [binary,621,2] ------------ end of proof -------------
These activities are projects of the Mathematics and Computer Science Division of Argonne National Laboratory.