The Turing Machine you describe here can actually be constructed (from a practical standpoint also), but it would be tedious and not of much practical use.

First note that the finite set of symbols $\{ \in, \forall, \exists, x, \prime, \land, \lor, \lnot, \rightarrow, \leftrightarrow \}$ would be more than sufficient to represent all statements expressible in the language of set theory (prime used to differentiate the countably infinite set of variables: $x, x^{\prime}, x^{\prime\prime},\ldots$). We can have the scrap work occur to the left of the place where we list out all of our ZFC theorems.  The (highly inefficient) process can be described as follows:

> (1) Copy the tape counter, which can represent $n$ by $n$ successive primes written from right to left.
  
> (2) Run a Turing Machine that on an input of $n$ primes, writes the first $n$ ZFC axioms (separated by spaces only working left on the tape) according to some recursive (computable) numbering.

> (3) Run a Turing Machine that on an input of $n$ formulas, applies the first $n$ rules of inference in first-order logic (in the sense that there are an infinite number of substitution rules, each applying a specific change of variable) on each of the formulas already on the working part of the tape and writes them all to the left.

> (4) Iterate through each formula on the left, determining whether it's the same as one already in your actual list or a negation of one. If not, add the formula to your list. If it's a negation of one, add the formula, reset your pointer to the beginning of the actual list, and HALT.

> (5) Add a prime to the original counter, reset the pointer to the beginning of the prime list, and go to step (1).

In a nutshell, this procedure at every stage $n$, lists all ZFC theorems provable in $n$ steps (not already listed) by limiting oneself to the first $n$ rules of inference and the first $n$ axioms according to some recursive (computable) enumeration.  Note that the the number of states required for such a Turing Machine is sensitive to ZFC only in the listing of the axioms (i.e., the number of states for the Turing machine carrying out step (2)).

The problem with such a Turing machine is that it exhibits no effective intelligence in its procedure.  Its running time for producing theorems would be exponential as a function of the length of their shortest proofs and emulating it in a programming language such as C++ would not change this fact. Even if there were an obvious contradiction in ZFC with a proof requiring $1000$ lines (considering all of the formal manipulations, this isn't very long), it would most likely take somewhere on the order of $2^{1000}$ years to find.  Therefore, the issue is not with the size of the Turing machine, but its running time.  Indeed, there is an ongoing research program in automated theorem proving to only choose "smart" paths of deduction rather than mindlessly trying them all.

Finally let me address an issue with the number of symbols and coding.  Anything that can be done with a Turing machine having a countable alphabet can be carried out by a Turing Machine having a binary alphabet (with a likely introduction of new states) under suitable coding. This is because there are only finitely many states and hence finitely many possible transitions.  Specifically, given a finite collection of subsets $\{S_1, \ldots, S_n\}$ of a countable alphabet of symbols representing the possible transitions from one state to another, we can assign each symbol a Natural number so that each of the $S_n$ are finite unions of recursive sets (assigning first the $n$-intersection to a computable infinite coinfinite set of Natural numbers; then doing the same for each of the $(n-1)$-intersections with the remaining unassigned symbols and Natural numbers, down to the individual $S_i$) and hence recursive.

Also, with coding, your question admits an annoying answer.  This is similar to a question I asked in [Asymptotic density of provable statements in ZFC](http://mathoverflow.net/questions/50550/asymptotic-density-of-provable-statements-in-zfc).

Specifically, if ZFC is inconsistent, then a Turing machine printing two contradictory statements and then halting would get the job done.  Otherwise, we can bijectively associate the set of Natural numbers with the set of all binary strings.  By taking any computable infinite and coinfinite subset $A$ of the Natural numbers, we can code the statements in the language of set theory so that the ZFC theorems are precisely the Natural numbers (binary strings) from $A$.  This means that a Turing Machine could require an arbitrarily large number of states if $A$ is suitably complex or very few if $A$ were something simple.