<s>[INST] Proof Checking a "Logic Equation" Puzzle Did a "logic equation" puzzle that took me several hours. Feel like it should have been faster, and that there surely is a more elegant path to the solution.
Sharing the proof to spot redundancies, omissions, faulty logic and areas to simplify. If there are best practices I should follow in terms of formatting and expression, that would also be a nice contribution.
You can try your hand at the puzzle here before you look at my proof, if you like.

Given that all variables are unique integers, and given the following
  statements:
$B \ne 1; B \ne 2; B \ne 5$
$D \ne 4; D \ne 6$
$D+E=C+F$
$B+C=A+F$
Find the value of all variables.
$$ \begin{array}{c|lcr} & \text{1} & \text{2} & \text{3} & \text{4} &
 \text{5} & \text{6} \\ \hline A & & & & & & \\ B & x & x & & & x & \\
 C \\ D &  &  & & x &  & x\\ E \\ F \\ \end{array} $$

Proof:
Given that the sum of all variables (A-F) is 21 and that $B + C = A + F$,


*

*$21 - (D+E) = A + B + C + F$

*$D+E$ must produce an odd-numbered sum so that $21 - (D+3)$ produces an even-numbered difference.

*$D$ and $E$ must have opposite parity.


Given that the sum of all variables (A-F) is 21 and that $A+F \ne C+F$,


*

*A sum of 7 is impossible for $D+E$, $B+C$ or $A+F$ as it would create a paradox $(A+F=C+F)$
Given that $D+E = C+F$ and that $D$ and $E$ have opposite parity,


*

*$C$ and $F$ must have opposite parity.


Given that $D+E=C+F$ and $B+C=A+F$,


*

*Sums of 3, 10 and 11 are not possible for $D+E$, $C+F$ or $A+F$ because they cannot be produced two or more ways in this data-set.


Given that $(21-(D+E))/2=B+C$, that $D+E$ must be odd, that $D+E>4$, that $D+E \ne 7$, that $D \ne 4$ and that $D \ne 6$,


*

*$E \ne 1$

*If $D+E$ produced a sum equal to 5, both $B+C$ and $A+F$ would produce a sum of 8.

*If $D+E$ produced a sum equal to 9, both $B+C$ and $A+F$ would produce a sum of 6.


Testing the only eligible odd number for B (3) given that $B+C$ must produce a sum of 6 or 8, the only possible option for C would be 5. This leads to a paradox when entering values for $D+E=C+F$ ($5=7$).
Given that both $B+C$ and $A+F$ must both produce equal- and even-numbered sums; this signals common parity for B and C, and common parity for A and F.
Given that the remaining options for B are 4 and 6; this signals even parity for B and C, and odd parity for A and F.
As $B+C$ must equal 8 given that $B$ cannot be 1, 2, 3, or 5, $B=6$ and $C=2$.
Given that $C=2$ and that $C+F \ne 7$, $F=3$.
Given that $D+E=5$ and that $E \ne 1$, $D=1$ and $E=4$.
$A+3=8$, so $A=5$.
Result:
$$ \begin{array}{c|lcr} & \text{1} & \text{2} & \text{3} & \text{4} &
 \text{5} & \text{6} \\ \hline A & & & & & ✓ & \\ B & x & x & & & x & ✓ \\
 C & & ✓ \\ D & ✓ &  & & x &  & x\\ E & & & & ✓\\ F & & & ✓\\ \end{array} $$
 [/INST] This goes a little faster:
Start is same as yours:  
Since $B+C=A+F$, we have $B+C+A+F$ is even, and since $A$ through $F$ add up to $21$, $D+E$ must be odd
But we cannot have $D+E=7$, for then $B+C=A+F=7$, and also $C+F=7$, and so $A+F=C+F$ which is impossible.
OK, so far it's the same. 
But at this point in your proof you note that $D+E$ cannot be $3$,$10$, or $11$ ... but note for same reason you state it also cannot be $4$ (that is: $D+E=C+F=4$ does not work)
So: $D+E$ is odd, greater than $4$, and smaller than $10$, but is not equal to $7$, so there are only two options left: $D+E=5$ or $D+E=9$
But the latter doesn't work, for then $D+E=C+F=9$, so $A+B=3$, and $B$ is neither $1$ or $2$
So, $D+E=C+F=5$ and $A+B=11$, and since $B$ is not $5$, we have $B=6$ and $A=5$
Since $B+C=A+F$ that means $F=C+1$, and since $D+E=C+F$ and since you only have numbers $1,2,3,4$ left, that means $F=3$ and $C=2$.
So $D$ and $E$ are $1$ and $4$, and since $D$ is not $4$, we have $D=1$ and $E=4$
Note that I never used the clue that $D$ is not $6$ ....
</s>