Superposition with equality resolution and equality factoring is said to be a complete calculus for first-order logic. The purpose of equality factoring is basically to get rid of paraduplicate literals like $p(X)$ | $p(Y)$, which is fine.
But all the papers I have on the topic agree that factoring applies only to positive equality. In other words, it doesn't handle paraduplicate negative literals like $\lnot p(X)$ | $\lnot p(Y)$. How do you deal with those?