Solving a Smullyan style knight and knave problem using natural deduction. How to shorten this proof? [ EDITED, there were 2 useless lines in the deduction below]

The Smullyan style problem : 

John: If (and only if) Bill is a knave, then I am a knave.

Bill: We are of different kinds.

With the understanding that knights only tell true statements and knaves only tell false statements, identify John and Bill's types.

(It therefore follows that if $J$ is the proposition that John is a knight, and John says a logical statement $X$, that $J\leftrightarrow X$ is a tautology.)

My attempt uses natural deduction; but the reasoning is rather long. 

Can you think of a shorter natural deduction style proof? 

What would be the quickest way to solve the problem according to you? 

Below , "J" means " John is a knight" and "B" means " Bill is a knight". 

Note: this solution makes Bill's statement true and John's statement false; which is coherent with their being a knight and a knave respectively. 

Indeed if we have ( B &amp; ~J) ( that is our alledged solution) John's statement is false, since this statement is equivalent to ( B &lt;-> J) , which, in turn, is equivalent to ~ (B&amp;~J) &amp; ~ ( J&amp;~B).
Here's a proof I made on http://proofs.openlogicproject.org/
  Mine is 13 statements versus your 39 (since your proof didn't go to my statement 14).  On the other hand, I stuck with a bidirectional formulation and I gather different systems do different things with $\leftrightarrow$E.  Still, make of this what you will.
I understand that this is not a natural deduction proof, but in response to benrg's comment above, I read somewhere else that you can use algebra in the Galois field of two elements GF(2) to solve things like these, and in that case if you take Z=&quot;A is a knave&quot; then you would formalize &quot;A asserts p&quot; as Z + p = 1, since either Z or p are true, but not both . I don't know the details of how to scale this for difficult problems but for the OP's problem, a solution is pretty short:

Take: A = &quot;A is a knight&quot;, B = &quot;B is a knight&quot;, Z = &quot;A is a knave&quot; and Y = &quot;B is a knave&quot;
By definition: A+Z = B+Y = 1
Inclusive p or q is &quot;p + q - pq = 1&quot;
The claims give us the equations: Z + AB + YZ - ABYZ = 1 and Y + AY + BZ - ABYZ = 1
ABYZ = 0 so Z + AB + YZ = Z(1 + Y) + AB = 1 and Y + AY + BZ = Y(1 + A) + BZ = 1
Using (2) (1+Y) = B and (1+A)=Z, substituting in (5) we end up with: B(Z+A)=1 and Z(Y+B)=1
Then B=1 and Z=1, that is, A is a knave and B is a knight.