Barnette's Conjecture: is every 3-connected cubic planar bipartite graph Hamiltonian?

A graph is *cubic* if every vertex has degree $3$, *planar* if it embeds in the plane, *bipartite* if its vertices can be 2-colored so that every edge joins the two colors, and $3$-*connected* if it remains connected after deleting any two vertices. Barnette (1969) conjectured that **every $3$-connected cubic planar bipartite graph has a Hamiltonian cycle** (a cycle visiting every vertex exactly once). Decide the conjecture: prove it, or exhibit a single counterexample. The computational sub-question posed here: verify (or refute) the conjecture for all such graphs up to $n$ vertices, generated exhaustively with a planar-graph generator such as $\texttt{plantri}$.

Acceptance. FULLY RESOLVES: (a) a counterexample -- the adjacency list of a $3$-connected cubic planar bipartite graph together with a certificate that it has no Hamiltonian cycle (an exhaustive/ILP search log) -- or (b) a complete proof. PARTIAL PROGRESS: an exhaustive verification, using $\texttt{plantri}$ to enumerate all $3$-connected cubic planar bipartite graphs, that every such graph on at most $n$ vertices is Hamiltonian for some $n>65$ (report $n$ and the count checked), or a proof for a new structural class. Provide the generator invocation and the Hamiltonicity checker.