Concerning the derivation in post #8, ~E(x) v V(x) v C(f(x)) and E(a) do not imply V(x) v C(f(x)), only V(a) v C(f(a)), and, in any case, the derivation must use the resolution rule only (it is sound and complete). My derivation has 12 steps and follows the informal reasoning. First we prove ~V(a) (the pusher

is not a VIP) and use it to show C(f(a)) and S(a,f(a)) (the official f(a) searched

). Then we get P(f(a)) from the third conjunct of the second hypothesis and derive the empty disjunct from the negation of the conclusion and C(f(a)).