The Space of an Unsatisfiable Formula I am reading the paper Measuring the hardness of SAT instances by Ans&oacute;tegui, Bonet, Levy and Many&agrave; (Proc. 23rd AAAI Conf. on AI, pp.&nbsp;222&ndash;228, 2008) (PDF). I am trying to understand the demonstration of the last part of the Lemma 3 (in bold). For this, I get an example. Let be $\Gamma = (a+b)(a+b')(a'+c)(a'+c')$ then its tree-like refutation is:



Following the demonstration of the last part of the Lemma 3, $[b\rightarrow 1]\Gamma=(1)(a)(a'+c)(a'+c')$, and adding the literal $b'$ where $[b\rightarrow 1]$ has removed it, we get $\Gamma' = (1)(a+b')(a'+c)(a'+c')$. In accordance the paper the tree-like refutation of $\Gamma'$ is a proof for $\Gamma \vdash b'$. The natural question, I think so, How it is posible that the tree-like refutation of $\Gamma'$ be a proof for $\Gamma \vdash b'$ if $\Gamma \neq \Gamma'$?.


  Lemma 3 The space satisfies the following three properties:
  
  
  $s(\Gamma \cup \{\Box\})$ = 0
  For any unsatisfiable formula $\Gamma$, and any partial truth assignment $\phi$, we have $s(\phi(\Gamma))\leq s(\Gamma)$.
  For any unsatisfiable formula $\Gamma$, if $\Box\notin\Gamma$, then there exists a variable $x$ and an assignment $\phi\colon\{x\}\to\{0,1\}$, such that $s(\phi(\Gamma))\leq s(\Gamma)-1$.
  
  
  The space of a formula is the minimum measure on formulas that satisfy (1), (2) and (3). In other words, we could define the space as:3
  
  $$s(\Gamma) = \min_{x, \overline{x}\in\Gamma, b\in\{0,1\}} \big\{
\max\{s([x\mapsto b](\Gamma))+1, s([x\mapsto\overline{b}](\Gamma))\}\;\big\}$$
  when $\Box\notin\Gamma$, and $s(\Gamma\cup\{\Box\}) = 0$.
Here is the original refutation:


From $a'+c$ and $a'+c'$ deduce $a'$.
From $a$ and $a'$ deduce $\square$.


When you add $b'$ back, you get:


From $a'+c$ and $a'+c'$ deduce $a'$.
From $a+b'$ and $a'$ deduce $b'$.


More generally, since the only difference between $\Gamma$ and $\Gamma'$ is the addition of $b'$, it is not hard to prove by induction that for every line $\ell$ proved in the refutation of $\Gamma$, the corresponding line in the corresponding $\Gamma'$ proof is either $\ell$ or $\ell+b'$. Hence the $\Gamma'$ proof proves either $\square$ or $b'$. It can happen that it indeed proves $\square$, in which case we can deduce $b'$ by weakening, which is an admissible rule for resolution space (we can get rid of it without increasing the space).