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?