Let we have a formula $\varphi(x_1,x_2...x_k)$. Now we apply a refutation method: $\varphi(x_1,x_2...x_k)\Leftrightarrow(\varphi(x_1=1,x_2...x_k)\lor\varphi(x_1=0,x_2...x_k))$. Latter formula seems to be longer, but no, good algorithm reduces number of literal occurences. On each step we can modify the formula without changing it's solution space. This gives much more power than resolution has. For example, Tseytin contradiction can be refuted this way in linear time using deterministic algorithm.
But what is the worst case for this algorithm?
Example:
$$\varphi=(x\lor y\lor z)(x\lor\overline y\lor t)(x\lor\overline z\lor\overline v)(\overline x\lor\overline t\lor\overline v)(\overline x\lor\overline z\lor v)(y\lor\overline z\lor v)(\overline y\lor\overline t\lor\overline v)\land(\overline y\lor z\lor t)$$
Step 1. Getting rid of $t$.
Putting $t$. Affected remaining clauses: $(\overline x\lor\overline v)(\overline y\lor\overline v)$. Reducing them: $\overline v\lor \overline x\overline y$.
Putting $\overline t$. Affected remaining clauses: $(x\lor\overline y)(\overline y\lor z)$. Reducing them: $\overline y\lor xz$.
Combining them using OR: $\overline v\lor\overline y\lor xz$.
Step 2. Getting rid of $y$.
Putting $y$. Affected subformula: $\overline v\lor xz$.
Putting $\overline y$. Affected subformula: $(x\lor z)(\overline z\lor v)$.
Combining them: $\overline v\lor xz\lor(x\lor z)(\overline z\lor v)$. Reduction: $x\lor z\lor\overline v$.
Step 3. Getting rid of $x$.
Putting $x$. Affected subformula: $\overline z\lor v$.
Putting $\overline x$. Affected subformula: $(z\lor \overline v)(\overline z\lor\overline v)$. Reduction: $\overline v$.
Combining them: $1$.
All clauses are covered, formula is satisfiable.
But what would be the hardest case for this and is it possible to break exponential bound using this method? Is this method general enough (we can modify formula by any ways until solution space is unchanged and this is checkable in polynomial time) that saying it requires superpolynomial time (for unsatisfiable formula) will imply $\mathsf{NP\ne coNP}$?
Note that for unsatisfiable formula it's possible to non-deterministically ignore some clauses if refutation can be done without their usage.