Adding to black_knight's point, it's worth noting that even in complete theories this often isn't very heartening: interleaving searches for P and for (not P) will often take an enormous amount of time.
Even cleverer strategies can be hopeless. For example, the theory of real closed fields is complete (and hence by your interleaving argument, decidable), but appears to be EXPSPACE-complete (at least from a brief skim of the literature), hence known to be truly intractable. If standard complexity-theoretic conjectures hold up (e.g. P != NP, NP != coNP), then non-gargantuan proofs in proof systems for a wide variety of interesting problems will turn out to be both intractable to locate and incomplete.
None of this is to say that automated theorem proving can't or won't rise to the level of human mathematical activity (I think it will fwiw), but we need to be far cleverer about it.