Why isn't SAT in coNP?
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 &quot;yes&quot; inputs. Because you have simply taken the NP SAT algorithm and flipped it, it runs in nondeterministic polynomial time for all &quot;no&quot; inputs. But we have no such guarantees for the &quot;yes&quot; 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.