I'm coming form 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') For all x all y exists z (Txy -> (Uxz & Uzy))
(2') For all x all y ((Uxy & Fx) -> Fy)
therefore For all x all y ((Txy & Fx) -> 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)-T(x1,x2) or U(x1,f(x1,x2)) ,
(2)-T(y1,y2) or U(f(y1,y2),y2) ,
(3) U(z1,z2) or -Fz1 or Fz2 ,
(4) U(w1,w2) or -Fw1 or Fw2 ,
(5) Tab ,
(6) Fa ,
(7)-Fb ,
Unifying (1) and (3) by this set of substitutions: {z2/f(x1,x2), x1/z1} leads to (8)
(8)-T(z1,x2) or -Fz1 or Ff(z1,x2)
Unifying (2) and (4) by this set of substitutions: {w1/f(y1,y2), y2/w2} leads to (9)
(9)-T(y1,w2) or -Ff(y1,w2) or Fw2
Unifying (8) and (9) by this set of substitutions: {z1/y1, w2/x2} leads to (10)
(10)-T(y1,x2) or -Fy1 or Fx2
And from here (10) can easily be unified with (5)-(7) by this set of substitutions: {y1/a, x2/b}
Therefor here is the picture of substitutions:
z2/f(x1,x2) , x1/z1/y1/a , w1/f(y1,y2) , y2/w2/x2/b ,
I suspect the answer to by question should already be in this picture, but can't see it. Any advise will be much appreciated.