$NP \ vs \ co-NP$: tautology to SAT and vice versa?
Your algorithm doesn't prove NP = co-NP because you're using a Cook reduction to go from DNF-TAUTOLOGIES to CNF-SAT.  NP and co-NP aren't separate complexity classes under Cook reductions, they are separate under Karp reductions.  Under Karp reduction, changing the output of Turing machine after you've performed the polynomial-time transformation is specifically disallowed.

So while your algorithm is a way to use a SAT solver to validate proofs, it doesn't say anything about whether NP = co-NP.