доказать с помощью метода резолюции отн. сем следования

[Whiteboss]

Проверьте пожалуйста:
$H1=\forall x \exists z B(x,z,a)$
$H2=\forall u \exists w A(u,w,w) \vee \exists z \forall w B(w,z,z) \vee \exists z \forall x A(x,c,z)$
$A1= \neg (\forall x \exists w A(x,x,w)) \wedge \forall u \exists v B(u,v,b) $
$ A2=\exists v \exists w B(b,v,w) \wedge \exists z A(b,z,z) \wedge \exists v \forall u B(u,v,a)$
Привёл H1,H2,неА1,неА2 к СНФ
$H1=\forall x B(x,f(x),a)$
$H2=\forall u \forall w \forall x ( A(u,f(u),f(u)) \vee B(w,a,a) \vee A(x,c,a))$
$ \neg (A1)= \forall x \forall v (A(x,x,f(x)) \vee \neg B(a,v,b)) $
$ \neg (A2)= \forall v \forall w \forall z ( \neg B(b,v,w) \vee \neg A(b,z,z) \vee \neg B(f(v),v,a))$
И дальше получается что А1 и А2 не следуют из посылок(если я правильно всё нашел) но в задании сказано доказать(что подразумевает что всё должно получиться) с помощью метода резолюции отн. сем следования вот поэтому у меня и появились сомнения в правильности моего решения.