Do we know something about this refutation method for SAT? 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.
As far as I can tell the earliest mention of the procedure you outline, later described in the literature as variable elimination by clause distribution, was in the paper "ZRes: The old Davis-Putnam procedure meets ZBDD" by Philippe Chatalic and Laurent Simon.  The procedure was described again, along with other formula simplification techniques, in "Effective Preprocessing in SAT through Variable and Clause Elimination" by Niklas Eén and Armin Biere.

The procedure was shown to be a workable way to improve SAT solver performance if care is taken to minimize clause growth as the implicants of removed terms are distributed, or to use data structures that efficiently manage large clause sets.