I'm coming from a logic and philosophy of logic background and am becoming more and more interested in comparing human theorem proving and automated theorem proving (ATP). At this stage, I'm trying to track the behavior of ATP algorithms (using unification and resolution) when it comes to cases in which multiple copies of a premise are needed to have a proof of an argument (premises and the conclusion) in Natural Deduction or Sequent Calculus. For example, consider the following argument:
(1') $\forall x \forall y \exists z (Txy \to (Uxz \land Uzy)) $
(2') $\forall x \forall y ((Uxy \land Fx) \to Fy)$
therefore, $\forall x \forall y ((Txy \land Fx) \to Fy)$
I've found a substitution set for the case we have two copies of (2'), but I believe that there is no need to feed the machine with two copies because this implies that we already know how to prove the theorem.
Here is what I've done (which is not following any algorithm, but trying to make a proof with unification and resolution):
(1) $\lnot T (x_1, x_2) \lor U (x_1, f (x_1, x_2)) $
(2) $\lnot T (y_1, y_2) \lor U (f (y_1, y_2), y_2) $
(3) $\lnot U (z_1, z_2) \lor \lnot Fz_1 \lor Fz_2 $
(4) $\lnot U (w_1, w_2) \lor \lnot Fw_1 \lor Fw_2 $
(5) $Tab$
(6) $Fa$
(7) $\lnot Fb$
Unifying (1) and (3) by this set of substitutions: $ \{z_2/f (x_1, x_2), x_1/z_1 \} $ leads to (8)
(8)$\lnot T (z_1, x_2) \lor \lnot Fz_1 \lor Ff (z_1, x_2) $
Unifying (2) and (4) by this set of substitutions: $ \{w1/f (y_1, y_2), y_2/w_2 \} $ leads to (9)
(9) $\lnot T (y_1, w_2) \lor \lnot Ff (y_1, w_2) \lor Fw_2$
Unifying (8) and (9) by this set of substitutions: $\{z_1/y_1, w_2/x_2\} $ leads to (10)
(10) $\lnot T (y_1, x_2) \lor \lnot Fy_1 \lor Fx_2$
And from here (10) can easily be unified with (5)-(7) by this set of substitutions: $\{y_1/a, x_2/b\} $
Therefor here is the picture of substitutions:
$z_2/f (x_1, x_2) $
$x_1/ z_1/ y_1/a$
$w1/f (y_1, y_2) $
$y_2/w_2/x_2/b $
I suspect the answer to by question should already be in this picture but can't see it. Any advice will be much appreciated.
MODIFICATION: When I posted this question, I was thinking there might be a way to skip using multiple copies of a formula by substitution tricks. However, I've realized that using multiple copies is inevitable. Now my question changes to: 'how an algorithm decides to use multiple copies of a formula?'.
I've checked Prover 9 and it has a predicate resolution step before providing a proof. In that stage, an input formula may get called multiple times. Any information about the algorithm behind that process would be very useful for me.