Interpolation conjecture for the calculus of structures

Let $T$ and $R$ be structures, and let $\mathsf{SKS}$ denote the calculus-of-structures system for classical propositional logic. Write $\mathsf{SKS}\setminus\{\mathord{\downarrow}\text{-identity},\mathord{\downarrow}\text{-weakening}\}$ and $\mathsf{SKS}\setminus\{\mathord{\uparrow}\text{-identity},\mathord{\uparrow}\text{-weakening}\}$ for the systems obtained by omitting the indicated rules.

Interpolation conjecture. For every derivation $T\vdash_{\mathsf{SKS}}R$, there is a structure $P$ and derivations

$$T\vdash_{\mathsf{SKS}\setminus\{\text{identity},\text{weakening}\}}P$$

and

$$P\vdash_{\mathsf{SKS}\setminus\{\text{dual identity},\text{dual weakening}\}}R.$$

The derivation is separated into a top phase whose rules do not introduce new atoms going down and a bottom phase whose rules do not introduce new atoms going up; consequently, $P$ contains only atoms occurring in both $T$ and $R$ and is an interpolant. The source states that a semantic proof is available in the propositional case, while a syntactic proof extending to predicate logic remains desirable.