[John Baez wrote in #23](https://forum.azimuthproject.org/discussion/comment/17859/#Comment_17859):

> As far as I know, this doesn't rule out the possibility that this problem is in NP.

We know that \\(\mathsf{DTIME}(f(n)) \subsetneq \mathsf{DSPACE}(f(n))\\). This is because, intuitively, in order to use up all of that space you needed to take the time to write it out. But the containment is strict because often times you can just mutate your input. For example [qsort](http://www.cplusplus.com/reference/cstdlib/qsort/) runs in \\(\mathsf{DTIME}(\mathcal{O}(n \, \mathsf{ln}(n)))\\) but only takes \\(\mathsf{DSPACE}(\mathcal{O}(n))\\) (this is including its input string).

We also know that \\(\mathsf{PSPACE} \subsetneq \mathsf{EXPSPACE}\\) from the [space hierarchy separation theorem](https://en.wikipedia.org/wiki/Space_hierarchy_theorem).

From the above two observations, we have \\(\mathsf{P} \subsetneq \mathsf{EXSPACE}\\).

Hence, a polynomial time reduction of Petri net reachability to SAT would suffice to prove \\(\mathsf{EXPSPACE} \subseteq \mathsf{NP}\\) and thus \\(\mathsf{P} \neq \mathsf{NP}\\). By the simple argument above I feel I deserve at least half the Millenium prize money if someone in this thread comes up with such a polynomial time reduction ;-)