Learning Pilog -3: Unification and Proof Search