An example of a proof that is explanatory but not beautiful? (or vice versa) This question has a philosophical bent, but hopefully it will evoke straightforward, mathematical answers that would be appropriate for this list (like my earlier question about beautiful proofs appropriate for high school level.)
The background is this:  we routinely distinguish between proofs that explain and proofs that demonstrate. This distinction has been around at least since Aristotle's time, but it is an open question, for instance in contemporary philosophy of mathematics, what explanation really means.  One recent suggestion has been that explanation might be related to beauty.  It seems reasonable that explanatory proofs are nicer than non-explanatory ones in SOME way, but are they necessarily more beautiful? And similarly, is beauty necessary for explanation? It seems a good way to attempt to answer these question is to look at a bunch of good examples.  And it seems a good way to get examples is to ask mathematicians, which is why I post the question here.
To clarify: the question is not at all to discuss the nature of explanation or beauty (if you want to discuss, I can give you my email address and we can chat offline). The purpose to is collect some good mathematical examples that help understand the relation between beauty and explanation in mathematics.
Examples that would be relevant:  beautiful proofs that are not explanatory, explanatory proofs that are not beautiful.  
Thanks in advance.
 A: I'm not sure this question is appropriate for MO, but: I find the usual proof of the Recursion Theorem beautiful but not explanatory. (See my answer to another MO question: Are there proofs that you feel you did not "understand" for a long time?)
The other direction is a little bit trickier: (it is my opinion that) the fact that a proof explains something well - if it does - makes it beautiful, at least to some degree. "Beauty" in mathematics, to me, is a fundamentally emotional property; it's not just the simplicity of the proof, or the cleverness of the argument, but my reaction upon reading through it that determines what sort of beauty it possesses for me, and explanatory proofs automatically score high in this regard. So I'm not sure a truly explanatory, but ugly proof exists.
The closest I can think of for this category are theorems asserting that such-and-such technical construction has some desired properties - often, these theorems are perfectly clear yet unremarkable, and the beauty of the construction comes in how it is applied or the idea behind it in the first place, not in the proof that it is what it ought to be. As an example, consider Kleene's proof that the statement "Turing machine $e$ on input $k$ halts" is a $\Sigma^0_1$ formula in the language of arithmetic. The proof of this is completely explanatory, but ugly. The real beauty is in the realization that arithmetic can express this kind of statement efficiently, which is at least plausible as soon as the question is brought up at first. But this kind of example feels pretty unconvincing.
LARGELY UNRELATED EDIT: Re: the Recursion Theorem, there are more explanatory proofs. It can be gotten as a corollary of Lawvere's Fixed Point Theorem (see Lawvere's fixed point theorem and the Recursion Theorem); staying within computability theory, Adam Day has given an absolutely wonderful argument (http://sigmaone.wordpress.com/2013/04/19/the-recursion-theorem/). A rule of thumb I tend to believe: all beautiful proofs can be "unpacked" to reveal an explanatory proof which, while maybe not as beautiful, is still beautiful in the same way.
A: I think Fourier analysis generates a lot of interesting examples of this phenomenon; it is an extremely powerful tool, but it's not always easy to see what the tool is actually doing.
A good case study is the classical isoperimetric inequality.  There is a gorgeous and short proof using Fourier series which you can teach to an undergraduate.  But the concept of length and area sort of disappear into the Fourier coefficients well before the key inequality, and so it takes a bit of effort to see the geometry.
Compare this to, say, Euler's proof using the calculus of variations.  It is very direct: it attacks the problem of minimizing the area functional over the space of curves with a given length head on, and the argument doesn't really use anything outside of the standard set of tools for similar optimization problems.  But Euler's original proof had a crucial gap involving the problem of determining when a critical point is a global minimizer, and it took centuries to get it right.
So we see a sharp contrast between elegance and simplicity (the Fourier series argument) and direct, explanatory power (calculus of variations).
A: David Hilbert's proof of the transcendence of $e$ and $\pi$ is extremely elegant, and totally mysterious.
A: I would suggest that the proof of Burnside using group characters that a group of order $p^{a}q^{b}$ ($p$,$q$ primes) is solvable is beautiful, but not really explanatory, from
a group theoretical point of view. The same can be probably be said for Frobenius's characterization of finite permutation groups in which no non-identity element fixes more than one point. While there are now "explanatory" proofs of the first result using purely group-theoretic methods,(which are arguably less beautiful) there is presently no purely group-theoretic proof of the second (although Terry Tao has recently found an alternative proof using character theory of certain commutative algebras, which can be seen on his blog).
A: I think proving compactness of logic from completeness is explanatory but not beautiful. The proof with ultraproducts is more beautiful. 
A: In the game of 'chomp', the first player always has a winning strategy, by a simple and (I think) beautiful argument (he can 'steal' a possible winning strategy from the second player). However, as far as I know, apart from special cases, there is no general known way of describing the winning strategy (which would maybe count as more explanatory)
A: A proof that many people say they find beautiful, but in my view is not at all explanatory, is Zagier's one-sentence proof of the sum of two squares theorem. 
A: I'd say that the proof of the four-colour theorem (particularly the "first generation" proof of Appel and Haken) is explanatory (we see that the source of four-colourability is the presence of unavoidable subconfigurations in any planar graph which are all reducible, in that the four-colourability of any planar graph containing such a configuration can be deduced from the four-colourability of a smaller graph) but not beautiful.  (See for instance the Notices article at http://www.ams.org/notices/199807/thomas.pdf for a description of the proof strategy.)
A: Applications of Zorn's lemma, like the basis existence theorem, the existence of ultrafilters or the existence of a well-ordering may count. These proofs are short and beautiful but they remain (at least for me) somehow mysterious. 
A: Bombieri's proof of the analog of the Riemann hypothesis for a curve C over a finite field is beautiful, in that it uses little more than the Riemann-Roch theorem for curves. But it seems less enlightening than the proof of Weil using the Jacobian of C or the proof of Grothendieck using Riemann-Roch for CxC, even though these require a great deal more background.
A: Since this thread has some new activity: I've always found Rosenblum's proof of Fuglede's theorem (apply Liouville's theorem to the appropriate operator-valued function) extremely elegant, but rather mystifying and non-explanatory.
It wasn't until much later that I saw a proof using the spectral theorem, as presented in Halmos's article What Does the Spectral Theorem Say? (American Mathematical Monthly, Vol. 70, No. 3 (Mar., 1963), pp. 241–247) which I feel gives a better feeling for why the result is true.
(If I recall correctly: apparently Fuglede's original proof used the spectral theorem, but I haven't ever looked it up.)
A: 1) "There is no simple group of order $n$" (for various composite values of $n$ in the interval $[50,200] \setminus \{60,168\}$ or so).  These arguments are explanatory but not beautiful.  They seem very ad hoc and futile in the sense that there are obviously plenty of larger values of $n$ for which one will not succeed in proving the result in the same way.  To my taste under/graduate algebra courses ask too many of this type of question: it's not beautiful and it's not practical, since by the way we know all the orders of finite simple groups!
2) The classification of finite simple groups is (it seems; I am no expert) neither explanatory nor beautiful.  The first generation proof was, it turned out, not even within two hundred pages of being formally complete.  This is an impressive list of negatives for what everyone agrees is one of the most important theorems of all time.  It seems that the goal of the third generation proof is to be more explanatory.
3) The theory of the $26$ sporadic simple groups is beautiful to an almost ridiculous degree.  There seems to be plenty of room for it to be more explanatory...which is beautiful.
A: I find Furstenburg's proof of van der Waerden's theorem using the Stone-Čech compactification of the natural numbers beautiful but not so explanatory. 
A: There are some theorems where it is clear that a straightforward but tedious computation can establish them, and where it is also fairly clear that there is little hope of eliminating the computation.  "Checkers is a draw" is a rather extreme example.  Few people would call the proof beautiful.  On the other hand, I would consider the proof explanatory, because what better explanation is there that there is no winning strategy than an explicit recipe for countering every winning attempt?  To deny that the proof is explanatory would, I think, be to implicitly demand more explanation, and it seems clear to me that there is not going to be any way to get a better explanation than just giving the strategy.  (Parts of the proof could perhaps be made more conceptual, but there is always going to be a large computational residuum.)
In short, sometimes the best explanation of a fact is simply that that's how a certain tedious calculation turns out.
