 \(\textsf{SKK}\) can be assigned the type \(p\rightarrow p\). There is a proof in TA\(_\textrm{CL}\) ending in \(\textsf{SKK}\colon p\rightarrow p\)  that does not contain the long formula above. However, there is a proof of \(\textsf{SKK}\colon p\rightarrow p\) that contains the above formula the second antecedent of which is not a subformula of \(p\rightarrow p\), indeed, the sets of the subformulas of the two formulas are disjoint. (We picked two different propositional variables, \(p\) and \(q\) to emphasize this point.) Some important cases of the problem of inhabitation, however, are decidable.