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:

(To see the PDF version of the formulas, please check this link:

https://math.stackexchange.com/q/4745621/1205609)

(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 f (y_1, y_2), y_2) $

(3) $U (z_1, z_2) \lor \lnot Fz_1 \lor Fz_2$

(4) $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 if the answer to by question should already be in this picture but can't see it. Any advice will be much appreciated.