It turns our that there is a error in Hw3.
In problem 6 it is *not* possible to prove the first set unsatisfiable by input resolution.
So please modify the set as follows and do the problem with the new set.

Replace the last closure

(R(x_4), R(y_4) ->).{}

by

(R(x_4) -> Q(y_4)).{y_4 = x_4}

Thanks to Colin who pointed the problem out, and sorry for any inconvenience.


-CT