An obvious approach to NP = coNP, is there a counterexample?
It is not known whether NP=coNP or NP≠coNP, but the latter is strongly suspected. It is not even known whether P≠NP implies NP≠coNP.

It is known that NP≠coNP implies P≠NP, and this approach for proving P≠NP is known as "Cook's program".



Now to your particular proof system. As far as I understand, your proof system maintains a collection of DNFs, which are initially the clauses of the original CNF (so they are trivial DNFs in the sense that all terms have width 1). At each step, you take two DNFs and combine them to a new DNF.

This system is similar to "depth-2 Frege", which is the following system. You start with "axioms" which are the clauses of the original CNF that you are trying to refute. The proof consists of a sequence of "lines" (propositions), each one either an axiom or following from previous lines via one or more derivation rules. In addition, all the lines are constrained to be formulas of depth 2 (CNFs or DNFs). The exact choice of derivation rules doesn't matter - fix any finite set of derivation rules of your choice.

It seems that one can simulate your proof system using depth-2 Frege in such a way that the number of lines in the Frege proof is comparable to the size of your proof. To know for sure, one needs to examine the exact simplification rules that you use, and show how to simulate them using depth-2 Frege. I believe that this should work out.

The pigeonhole principle is hard not only for Resolution, but also for bounded depth Frege. In particular, refuting the pigeonhole principle using depth-2 Frege takes $2^{n^{\Omega(1)}}$ lines, where $n$ can be taken as the size of the formula. See for example Fu and Urquhart.