  We investigate the size complexity of proofs in $Res(s)$ -- an extension of
Resolution working on $s$-DNFs instead of clauses -- for families of
contradictions given in the {\em unusual binary} encoding. A motivation of our
work is size lower bounds of refutations in Resolution for families of
contradictions in the usual unary encoding. Our main interest is the $k$-Clique
Principle, whose Resolution complexity is still unknown.
  Our main result is a $n^{\Omega(k)}$ lower bound for the size of refutations
of the binary $k$-Clique Principle in $Res(\lfloor \frac{1}{2}\log \log
n\rfloor)$. This improves the result of Lauria, Pudl\'ak et al. [24] who proved
the lower bound for Resolution, that is $Res(1)$.
  Our second lower bound proves that in $RES(s)$ for $s\leq
\log^{\frac{1}{2-\epsilon}}(n)$, the shortest proofs of the $BinPHP^m_n$,
requires size $2^{n^{1-\delta}}$, for any $\delta>0$. Furthermore we prove that
$BinPHP^m_n$ can be refuted in size $2^{\Theta(n)}$ in treelike $Res(1)$,
contrasting with the unary case, where $PHP^m_n$ requires treelike $RES(1)$ \
refutations of size $2^{\Omega(n \log n)}$ [9,16].
  Furthermore we study under what conditions the complexity of refutations in
Resolution will not increase significantly (more than a polynomial factor) when
shifting between the unary encoding and the binary encoding. We show that this
is true, from unary to binary, for propositional encodings of principles
expressible as a $\Pi_2$-formula and involving {\em total variable
comparisons}. We then show that this is true, from binary to unary, when one
considers the \emph{functional unary encoding}. Finally we prove that the
binary encoding of the general Ordering principle $OP$ -- with no total
ordering constraints -- is polynomially provable in Resolution.
