proof6 for the lausal representation CPHP. Let

$$\begin{array}{r c l}{{\mathrm{EXT}^{l}}}&{{=}}&{{\{e_{i,j}^{l}\gets e_{i,j}^{l+1},\ e_{i,j}^{l}\gets e_{i,l}^{l+1},e_{l+1,j}^{l+1}\mid1\leq i\leq l{\mathrm{~and~}}1\leq j\leq l-1\}}}\end{array}$$

for 1 < l ≤ n, where ea
h e n+1 i,j is pi,j . The extension EXTl
orresponds the set of extending lauses in (Cook 1976) similarly to the set of rules (10) in part (ii) of the proof of Theorem 5.1. Furthermore, E(π) 
onsists of the sets of rules (11) and (12)
dened in the proof of Theorem 5.1 (ii). By applying the strategy from the proof of Theorem 5.1 (ii), we obtain a polynomial-length ASP-T proof for

$${\mathsf{n l p(C_{P H P})}}\cup\bigcup_{1<l\leq n}\mathrm{EXT}^{l}\cup\mathrm{E}(\pi).$$

Now, we use the same strategy to onstru t a polynomial ASP-T proof for the program

$$\mathrm{EPHP}_{n}^{n+1}=\mathrm{PHP}_{n}^{n+1}\cup\bigcup_{1\leq l\leq n}\mathrm{EXT}^{l}\cup\mathrm{E}^{\prime}(\pi),$$

where E
′(π) 
onsists of rules c ← al for ea
h literal l ∈ C for ea
h 
lause C ∈ π (that is, rules as in (11) but without the restri tion C 6∈ CPHP) together with the rules

```
in (12). The only dieren
                           e 
                              omes in step (a) in the proof of Theorem 5.1 (ii), that
                                                                                      

```

is, when we have dedu ed Fc 
orresponding to C ∈ CPHP. Sin
e we do not have the rule **⊥ ← ∼**c in EPHPn+1 n, we 
annot dedu
e Tc to obtain a 
ontradi
tion. Instead,

```
we 
   an dedu
         e a 
             ontradi
                   tion without using the ASP-T 
ut rule through a program

```

rule in PHPn+1 n that 
orresponds to the 
lause C . For instan
e, if C = {¬pi,k, ¬pj,k},
we have the rules c ← ∼pi,k and c ← ∼pj,k in E
′(π) and the rule ⊥ ← pi,k, pj,k in PHPn+1 n . From Fc, we dedu
e Tpi,k and Tpj,k . From F⊥ and ⊥ ← pi,k, pj,k , we dedu e F{pi,k, pj,k}, and furthermore, from Tpi,k and F{pi,k, pj,k}, we dedu
e Fpj,k .

This results in a polynomial-length E-ASP-T proof for PHPn+1 n .

(ii): Assume now that there is a polynomial ASP-T proof for PHPn+1 n . By Theorem 3.2, there is a polynomial T-RES proof for comp(PHPn+1 n ). Noti
e that the ompletion comp(PHPn+1 n ) 
onsists of the 
lausal en
oding CPHP of the pigeonhole prin iple and additional lauses (tautologies) for rules of the form pi,j ← ∼p
′
i,j ,
p
′
i,j ← ∼pi,j . It is easy to see that these additional tautologies do not ae
t the length of the minimal T-RES proofs for comp(PHPn+1 n). Thus there is a polynomiallength T-RES proof for the 
lausal pigeonhole en
oding. However, this 
ontradi
ts

```
the fa
      t that the 
                 omplexity of the 
                                  lausal pigeonhole prin
                                                       iple is exponential with
                                                                             

```

respe t to n for (Tree-like) Resolution (Haken 1985).

We an also easily obtain a non-tight program family to witness the separation demonstrated in Theorem 5.2. Consider the family

{PHPn+1 n ∪ {pi,j ← pi,j | 1 ≤ i ≤ n + 1, 1 ≤ j ≤ n}},