Finding the proof of this logic problem. Prove of disprove:
Premises:
1) $J \lor (\lnot K \lor J)$
2) $K \lor (\lnot J \lor K)$
Conclusion:
$(J \land K) \lor (\lnot J \land \lnot K)$
Proof:
4)$ (J \lor J) \lor \lnot K$ [Commutation and association of 1)]
5) $J \lor \lnot K$ [Duplication of 4)]
6) $(K \lor K) \lor \lnot J$ [Commutation and association of 2)]
7) $K \lor \lnot J$ [Duplication of 6)]
8) $(J \lor \lnot K) \land (K \lor \lnot J)$ [Conjunction of 5) and 7)]
9) $[J \land (K \lor \lnot J)] \lor [\lnot K \land (K \lor \lnot J)]$ [Distribution of 8)]
10) $[(J \land K) \lor (J \land \lnot J)] \lor [\lnot K \land K] \lor (\lnot K \land \lnot J)] $Distribution of 9)
11) $[(J \land K) \lor (\lnot J \land \lnot K)] \lor [(J \land \lnot J) \lor (K \land \lnot K)]$
Association of 10)
12) As $[(J \land \lnot J) \lor (K \land \lnot K)]$ is always false, then by Disjunctive Syllogism:
$(J \land K) \lor (\lnot J \land \lnot K)$, as desired. Q.E.D
I have two questions:
1) Is everything correct?
2) Is there a shorter proof?
 A: I think you did just fine, and your proof is absolutely correct.  And very well documented.
I think from $$[(J \land K) \lor (J \land \lnot J)] \lor [\lnot K \land K] \lor (\lnot K \land \lnot J)]\tag{10}$$
 you could simply state $$[(J\land K) \lor \underbrace{(F\lor F)}_{false} \lor (\lnot K \land \lnot J)]\tag{11}$$
And finally $$[(J\land K) \lor (\lnot J \land \lnot K)]\tag {12}$$
But I think, in the end, it simply comes down to how explicit one wants to be. For example, between my (11) and (12), In addition to disjunctive syllogism, I also used the commutative property of $\land$ when flipping from $\lnot K \land \lnot J$ to $\lnot J \land \lnot K$, just as you relied on commutativity between your $(10)$ and $(11)$.  
All in all, there's little to improve in your proof. The only thing to add, if you want to be completely explicit in terms of justification in your steps $(10)$ and $(11),$ add commutativity along with associativity of $(10).$  Nice job.
A: An alternate approach: if 1) holds, you must have J true or not K or J true. So either J is true or K is false.
if 2) holds, by the same argument, K is true or J is false. 
So if J is true, K is true which implies J and K true which implies the conclusion. 
If J is false, then 1) implies K false. So not J and not K is true which implies the conclusion so done.
