Has any previously unknown result been proven by an automated theorem prover?

Robbins' conjecture that all Robbins algebras are Boolean algebras was first proved using EQP, after Tarski and others had tried and failed to prove or disprove it.

Check out A Summary of New Results in Mathematics Obtained with Argonne's Automated Deduction Software. It lists many solved problems (even though it's an old page, it summarizes results obtained until 1995).

Some information is also here, section What has Automated Theorem Proving been Really Useful for?.

The Robbins Conjecture, which has already been mentioned, is probably the most interesting example for what automated theorem provers are capable of already. Another interesting piece of information I remember is that the Logic Theorist programme in the mid-fifties was able to prove much of the Principia Mathematica by itself and even managed to find a more elegant proof for the Isosceles Triangle Theorem than Russell himself.

However, I would like to clarify what you said about the Four Colour Theorem: what Wikipedia refers to is the proof of this theorem using Coq, which is an interactive theorem prover. The basic idea is that the user provides a step-by-step proof and the theorem prover proves the validity of each step itself. Different theorem provers have different levels of automation; the only one I am familiar with is Isabelle, which has quite powerful automation. A remarkable example is Cantor's theorem that there is no injective mapping from a set to its powerset, which can be proven completely automatically by one of Isabelle's many proof methods. However, this is more or less a coincidence, the system can't usually prove theorems like this on its own, but it handles things like tedious simplifications and case distinctions quite well and sometimes solves problems that are not immediately obvious to me automatically. Unfortunately, most often, it is the other way round.