First Order Logic Resolution During Resolution, Can a skolemization constant be replaced by a function?
For example:
∃X e(X)∧ g(X) 

After replacing with skolemization constant
e(a)∧g(a)

I separate both the clauses:
e(a)
b(a)

Suppose I have one more clause ~b(X) ∨ ~e(f(X))
Here f(X) is the skolemization function which I got after Existential Elimination for that clause.
So When resolving
e(a)... (1)
b(a).... (2)
~b(X) ∨ ~e(f(X)).... (3)

Resolving  (1) and (3) by Unification a/f(X)
~b(X)..(4)

This is my query. Can I replace a (which is a skolemization constant by f(X) which is a function) by unification.
Resolving  (4) and (2) by Unification X/a
Null
Please let me know
 A: No, you cannot unify $e(a)$ and $\neg e(f(X))$
Formally you can't, because there is no way to substitute anything for $X$ in $\neg e(f(X))$ so it ends up as $\neg e(a)$.  That is: you can substitute terms for a variable, but you can never substitute terms for a constant.
But more importantly, logically you can't, because as the function $f$ indicates, the object that does not have property $e$ is dependent on the variable that you pick, and there is no guarantee that that function ever maps to $a$.
I am wondering though ... is there any way to avoid the function?  For example, if the original statement you were working with is:
$$\forall x (b(x) \rightarrow \exists y \ \neg e(y))$$
Now, there are two ways to rewrite this to get it ready for resolution:
The 'obvious' way is:
$$\forall x (b(x) \rightarrow \exists y \ \neg e(y)) \Leftrightarrow$$
$$\forall x \exists y  (b(x) \rightarrow  \neg e(y)) \Leftrightarrow$$
$$\forall x \exists y  (\neg b(x) \lor  \neg e(y))$$
and that gives you clause $\{ \neg b(x), \neg e(f(x)) \}$
But you can also do:
$$\forall x (b(x) \rightarrow \exists y \ \neg e(y)) \Leftrightarrow$$
$$\exists x b(x) \rightarrow \exists y \ \neg e(y) \Leftrightarrow$$
$$\exists y (\exists x b(x) \rightarrow  \neg e(y) \Leftrightarrow$$
$$\exists y \forall x(b(x) \rightarrow  \neg e(y) \Leftrightarrow$$
$$\exists y \forall x(\neg b(x) \lor  \neg e(y)$$
and that gives you clause $\{ \neg b(x), \neg e(y) \}$
and that one you can resolve with $e(a)$
