You're mixing things up. By a "general theorem prover", we typically mean "a program which can decide for every sentence in FOL whether it's valid" (I say FOL, because the situation is even worse for HOL), i.e. a decider for the set of valid FOL sentences. The sentence ZFC -> CH (where ZFC and CH are expanded as needed) is not valid because CH doesn't follow from the ZFC axioms. Neither is ZFC -> not(CH) valid. We know both of these results from proofs specific to this problem, but a general purpose theorem prover would give us both of these results for free. If we had such a tool, mathematics would essentially be "solved" (maybe apart from deciding what questions to ask). But since FOL is undecidable, it can't exist.

What you are asking for is a machine that for each pair of formulas A, B (correctly) decides that either A -> B or A -> not(B), but this is impossible for model-theoretic reasons (not all theories are complete) and that has nothing to do with decidability.