Herbrand Universe + Resolution

Can anyone here explain how Question4, iii in the tut was arrived at? It almost seems arbitrary
Is the universe extracted from the clausal form or from the original ?
Why was iii a,b,c instead of f(a) ?

also

When looking at resolution and hoping to arrive at a []. Is it acceptable to arrive at [] early ? i.e. if i get there in 2 steps, do i need to continue or can i decide then that its not satisfiable because i was able to reach a [] ?

From my understanding (and I may be wrong)

(1) The Herbrand Universe is a list of the constants and the functions (with all possible elements being possible assigments to the function). Since iii has no functions you just list the three constants.

(2) yes; the moment you have the [] you've won.

 
  ,= ,-_-. =.
 ((_/)o o(\_))
  `-'(. .)`-'
      \_/

http://ilanpillemer.com
Entia non sunt multiplicanda praeter necessitatem

Thanks muchly..