The answer is as follows. While the fact that
is
logically equivalent to allows us to remove one
of the variables introduced by extended resolution, we cannot combine
this encoding with others to remove subsequent variables. As a
specific example, suppose that we learn both

and

and wish to conclude from this that

There is no single pseudo-Boolean axiom that is equivalent to (40).

Matt Ginsberg 2004-02-19