Why isn't SAT in coNP?

I understand why NP=coNP if SAT is in coNP (How do I prove that SAT in coNP implies NP=coNP?).

But I'm missing why the following machine doesn't turing recognize the complementary of SAT:

Given a turing machine M that recognizes SAT, the following turing machine recognizes coSAT:

• Run M on the input word w.

• If M accepts - reject.

• If M rejects - accept.

Because coSAT is the language of all unsatisfiable formulas, a formula is unsatisfiable if it doesn't have a satisfiable interpretation, which is exactly the opposite of what M outputs.

What am I missing in here?

You are missing a major part of the definition of $CoNP$: you need a proof that your machine $M$ runs in nondeterministic polynomial time for all "yes" inputs. Because you have simply taken the NP SAT algorithm and flipped it, it runs in nondeterministic polynomial time for all "no" inputs. But we have no such guarantees for the "yes" inputs.

The real answer is, nobody knows that SAT isn't in $CoNP$. If we knew that, we would know that $CoNP = NP$, but this is still an open problem. So, nobody can point to a specific reason that you can't build a machine that decides the complement of SAT it nondeterministic polynomial time. It's just that nobody has been able to do it yet, or prove that it's impossible.

StackExchange Computer Science Q#128148, answer score: 2