Resolution Algorithms and one Example Problems? 
We have a problem in one Resolution question.

There is $5$ clauses, and want to prove the $6$th clause is true. which of the following clause is need more than one times to prove $6$th clause? $t$ to $z$ be variables, $A$ to $C$ is constant values, $f$ be function, $D$ and $E$ are predicates. 

$1) \neg E(t, u) \lor E(u, t)$
$2) \neg D(v, w) \lor E(f(v), w)$
$3) \neg E(x, y) \lor \neg E(y, z) \lor E(x, z)$
$4) D(A, C)$
$5) \neg E(C, B)$
$6) \neg D(A, B)$

The solution is option $2$ (i.e The clause $2$ is used more that one times for proving the $6$th clause is true). 

my question is about solving this problems, is there anyway to quickly
  get this answer? or we should completely solve it? any idea for
  getting this solution?

 A: To prove 6) from 1)-5), by Resolution, we have to add to 1)-5) its negation:

6') $D(A, B)$.

Then we need Unification.
Performing the following substitution:

$A \to v, \ B \to z,\ C \to u, x, \ f(A) \to t, y$

we get:
$1) \neg E(f(A), C) \lor E(C, f(A))$
$2) \neg D(A, w) \lor E(f(A), w)$
$3) \neg E(C, f(A)) \lor \neg E(f(A), B) \lor E(C, B)$
$4) D(A, C)$
$5) \neg E(C, B)$
$6') D(A, B)$.
Now, we have to apply resolution a first time with 6') and 2), with $B \to w$, to get :

7) $E(f(A),B)$

and a second time with 4) and 2), with $C \to w$, to get :

8) $E(f(A), C)$.

Using now 1) and 8) we get:

9) $E(C, f(A))$.

Finally, 9), 7) and 3) will get:

10) $E(C,B)$

that, with 5), will produce the sought contradiction.

Comment : this is a case where the "original" formulae are more easily managed...
The clause 2) is derived from : 

$\forall v \ \forall w \ [D(v, w) \to E(f(v), w)]$;

thus, "instantiating" twice with $A,B$ and $A,C$ respectively, gives:

$D(A, B) \to E(f(A), B)$

and

$D(A, C) \to E(f(A), C)$,

that are "well-fitted" for modus ponens with 4) and 6'). 
