For recursive rules $F(\vec{x}) \land \varphi \implies F(\vec{x}')$, we could conjoin $\vec{x} \neq \vec{x}'$ to the condition to exclude the case that the arguments of $F$ remain unchanged. This could help to avoid computing redundant rules both in ADCL and ABMC.
