The problem of evaluating the truth of a proposition (including whether it leads to a contradiction or not) from a computational point of view amounts to evaluating the boolean expression corresponding to that proposition.
Determining whether your proposition F would lead to a contradiction or not is the same as being able to determining whether the corresponding boolean expression is satisfiable or not. At the present time there is no known method for evaluating the truth of a general boolean expression without actually calculating the expression itself. This is known as the boolean satisfiability problem, and it is conjectured that there is no efficient algorithm for evaluating whether it has a truth value or not. The only guaranteed way of determining whether it is satisfiable or not, and determining the corresponding variable assignment, is to evaluate all possible combinations of the boolean expression.
This fact that there is no known general efficient solution, and the conjecture that the can't be one, is known as the P vs NP problem.
Here efficient means that it can be solved in (deterministic) polynomial time.
Inefficient means that the problem is solvable in Non-deterministic polynomial time (The "NP" in NP-complete). For practical purposes this means the only way of finding a solution is to evaluate every possible input combination, which can take up to an exponential amount of time.
The P vs NP problem first gained importance after Cook and Levin independently proved the NP-completness theorem in the 70s. In particular Cook was working on automated theorem proving procedures, and it was in this context that he ended up with his result regarding boolean satisfiability.
There is a remote possibility that P=NP and that there is such an efficient procedure, but it is considered highly unlikely, and if it were true, the consequence would be significant for our understanding of computation and science in general.
"If P = NP, then the world would be a profoundly different place than we usually assume it to be. There would be no special value in "creative leaps," no fundamental gap between solving a problem and recognizing the solution once it's found." — Scott Aaronson, MIT
To summarize, the answer to your overall question "Before starting the Reductio Ad Absurdum, how can you guess or divine that F causes the contradiction?": There is no known method for doing so beforehand. Being able to do so implies an efficient method for solving boolean satisfiability, and it is conjectured (but not yet proven conclusively) that an efficient method is impossible.