Consider the greatest common divisor problem:
gcd( u, 0, u ).
gcd( u, v, w ) ← not zero( v ), gcd( v, u mod v, w ).
Now give the goal
← gcd( 15, 10, x ).
resolution fails using the first clause (10 does not match 0), so using the second clause and unifying gcd(u,v,w) with gcd(15,10,x) gives
gcd( 15, 10, x ) ← not zero( 10 ),
gcd( 10, 15 mode 10, x ), gcd( 15, 10, x ).
Since (i) not zero(10) is true, (ii) 15 mod 10 is 5, and (iii) cancel gcd(15,10,x) from both sides, we obtain the subgoal
← gcd( 10, 5, x ).
Note that this is just another goal to be resolved like the original goal.
This we do by unification as before, obtaining
gcd( 10, 5, x ) ← not zero( 5 ),
gcd( 5, 10 mod 5, x ), gcd( 10, 5, x ).
and so get the further subgoal
← gcd( 5, 0, x ).
Now this matches the first rule
gcd( u, 0, u ).
so instantiating x to 5 results in the empty statement, and the system will reply with something like
Yes: x = 5