The proving then proceeds by selecting a subgoal p j (θ j ), searching P for a logical premise p i (θ i ) for which p j and p i and their arguments θ j and θ i are equal (or they unify).
if such a logical premise is found, then the sub-goal is proved and removed from G. the case of the sub-goals g 1 to g 4 in steps 1 and 2 of Figure 1, where predicates match those of p 1 to p 4 and variables unify as x 2 := x 1 and v 2 := v 1 .