Valid inference in first-order predicate logic I should prove for the following premises and conclusion if the inference/conclusion is valid by using general resolution for clauses. 
The conclusion is valid if it is possible to derivate a contradiction.  After that Put every formula in prenex-form and in skolem-form. Then Create clauses for every formula. Finally Use general resolution for inference.  
Negate the conclusion: 
$ \forall x Ax \land \lnot \forall x \lnot Bx $
The second step. Put every premise in prenex-form. 
The first part:
1.$ \forall x \; (Ax \rightarrow \exists y \; Rxy) $
2.$ \forall x \; \exists y \; (Ax \rightarrow \; Rxy) $ .Extract the $\exists y $
3.$ \forall x \; \exists y \; (\lnot Ax \lor Rxy) $. Disjunction instead of implication.
4.$ \forall x \; (\lnot Ax \lor Rxf(x)) $. Skolem-function for $ \exists y $  
The second part of the premise:
1.$\forall x \; \forall y \; (Rxy \rightarrow \lnot Bx) \;$
2. $ \forall x \; \forall y \; (\lnot Rxy \lor \lnot Bx) \;$.Disjunction instead of implication.   
In program format:
1.$ Rxf(x) \leftarrow Ax $
2.$ Rxy, Bx \leftarrow $  
The third part (the negated conclusion):
1.$ \forall x Ax \land \lnot \forall x \lnot Bx $
2.$ \forall x Ax \land \lnot \forall z \lnot Bz $ .Alphabet
3.$ \forall x Ax \land \exists z \; \lnot \lnot Bz $ .Extract the $ \forall z  $
4.$ \forall x Ax \land \exists z \; Bz $ . Remove the $\lnot \lnot $.
5.$ \forall x \exists z \; Ax \land  Bz $
6.$ \forall x \; Ax \land \forall x Bg(x) $ .  Replace the $\exists z $ for a skolem-function.  
The set of clauses is: {$\lnot Ax \lor Rxf(x), \lnot Rxy \lor \lnot Bx), \leftarrow Ax, Bg(x)$}
The goal in clause-form:
1.$ \leftarrow Ax $
2.$ \leftarrow Bg(x) $ 
Deriving the contradiction by using general resolution for clauses.
1'.$ \leftarrow Ax $. First goal
2'.$ Rxf(x) \leftarrow Ax $ .Sentence 1
3'.$ Rxf(x) \leftarrow $ . Res. 1,2. $ ,\; \theta =[x/x] $
4'.$ \leftarrow Rxy, Bx $  Sentence 2
5'.$ Bg(x) \leftarrow $. Second goal
6'.$ \leftarrow Rxy \; $ Res. 4,5. $ \theta =[g(x)/x] $
7'.$ \; \square \; $Re. 3,6 $ \theta =[f(x)/y] $     
 A: Your strategy, if it is one, is all over the place and much too complicated. The point is to distribute the quantifiers across the implications, using one "trick" re the $y$ quantifier. The last step of the proof is then just propositional logic (a syllogism!).
Note that for any formulas $p(x), q(x)$, possibly with other free variables,
$$
\forall x\,(p(x)\to q(x)) \vdash (\forall x\,p(x)\to \forall x\,q(x))\tag{1}
$$
Also note that if $y$ is not free in $t$, then
$$
\forall y\,(s(y)\to t) \equiv (\exists y\,s(y)\to t)\tag{2}
$$
This is true because $(s(y)\to t) \equiv (\neg s(y)\lor t)$, and if $y$ is not free in $t$ then $\forall y\,(\neg s(y)\lor t) \equiv (\forall y\,\neg s(y)\lor t)$. Using $\forall \neg\equiv \neg \exists$, the last formula is equivalent to $(\neg \exists y\,s(y)\lor t)$, and thus to $(\exists y\,s(y)\to t)$.
Using (1), from your first premise $\forall x \, (Ax \rightarrow \exists y \, Rxy)$ we can infer
$$
\forall x \, Ax \to \forall x \,\exists y \, Rxy.\tag{I}
$$
Using (2), your second premise is equivalent to
$$\forall x \, (\exists y \, Rxy \to \lnot Bx)\tag{pre-II},
$$
and applying (1) to (pre-II) we can derive
$$
\forall x \,\exists y \, Rxy \to \forall x \,\neg Bx\tag{II}.
$$
Now, from (I) and (II), just by propositional logic, we can conclude:
$$
\forall x \, Ax \to \forall x \,\neg Bx,
$$
which is what you wanted to derive.
A: Not sure if this will help in your system, but here is how I would prove the required result using my own "ordinary rules of logic" (without Skolem functions, non-empty domains, etc.) Perhaps you can translate it into your system.
Part 1: Prove that $\forall x:[A(x) \implies \neg B(x)]$


*

*Suppose $A(t)$

*From premise #1, $A(t) \implies \exists y:R(t,y)$

*From (1) and (2),  $\exists y:R(t,y)$

*From (3), $R(t,u)$

*From premise #2 and (4), $\neg B(t)$

*From (1) and (5), we can conclude that $\forall x:[A(x) \implies \neg B(x)]$

Part 2: Prove by contradiction that $\forall x:A(x)\implies \forall x: \neg B(x)$


*Suppose $\forall x: A(x)$

*Suppose to the contrary that we have $B(v)$

*From (6) $A(v)\implies \neg B(v)$

*From (7) $A(v)$

*From (9) and (10), we obtain the contradiction $\neg B(v)$

*From (8) and (11), we can conclude that $\forall x:\neg B(x)$ (by contradiction)

*From (7) and (12), we can conclude, as required, that $\forall x:A(x)\implies \forall x: \neg B(x)$
