Paired resolution and $\mathsf{NP}$ vs. $\mathsf{coNP}$? Let we resolve only two clauses at time and then get rid of them. Such resolution clearly takes $O(n)$ steps.

Sequence is a set of instructions in the form $(C_{S_1}\cup C_{S_2},v\cup\overline v),...$, where $S_i$ denotes a set of merged clauses, $v\in C_{S_1},\overline v\in C_{S_2}$.

Of course such resolution taken deterministically or randomly is wrong with high probability.

For example, let's consider $\varphi=(x\oplus y)(x\oplus z)(y\oplus z)$.

Clearly this formula is unsatisfiable. But what can I get using resolution:

$(x\oplus y)\Leftrightarrow(x\lor y)\land(\overline x\lor\overline y)$.

Resolving $x$ and $\overline x$: $(y\lor\overline y)=1$.

Doing this for other clauses gives us tautology.

So, this means, that sequence $(C_1\cup C_2,x\cup \overline x),(C_3\cup C_4,x\cup \overline x),(C_5\cup C_6,y\cup \overline y)$ is wrong.

But there is a correct sequence:$(C_1\cup C_4,x\cup\overline x),(C_2\cup C_3,\overline x\cup x),(C_{\{1,4\}}\cup C_5,\overline z\cup z),(C_{\{2,3\}}\cup C_6,z\cup\overline z),(C_{\{\{1,4\},5\}}\cup C_{\{\{2,3\},6\}},y\cup\overline y)$

Showing this:

Initial formula: $(x\lor y)(\overline x\lor\overline y)(x\lor z)(\overline x\lor\overline z)(y\lor z)(\overline y\lor\overline z)$


$(x\lor y)(\overline x\lor\overline z)\mapsto(y\lor\overline z)$
$(\overline x\lor\overline y)(x\lor z)\mapsto(\overline y\lor z)$
$(y\lor\overline z)(y\lor z)\mapsto y$
$(\overline y\lor z)(\overline y\lor\overline z)\mapsto\overline y$
$y\land\overline y\mapsto0$


There are exponentially many sequences for any formula. Same applies for number of possible assignments.

But what I'm asking: is such type of resolution is proved not to be refutation-complete? In other words have someone proved that not every unsatisfiable formula has a sequence that results in empty clause? Or is it an open question? (Otherwise we'd know that $\mathsf{NP=coNP}$)

P.S. This type of resolution is sound, so only thing that I do not know is refutation-completeness.
It is known that some formulas require exponentially long Resolution proofs. Therefore Resolution cannot be used (directly) to prove that $\mathsf{NP}=\mathsf{coNP}$.

Note that the details of your procedure are completely irrelevant. The lower bounds show that whatever algorithm you use to create your Resolution refutations, there will be some formulas on which it will take exponential time, simply because every Resolution refutation of these formulas is exponentially long.