Biplanar Graphs on at Most Sixteen Vertices Are 9-Colorable

A graph is biplanar if its edge set can be partitioned into two planar graphs. The Earth–Moon problem asks for the largest chromatic number of a biplanar graph. Kirchweger, Scheucher, and Szeider proved by SAT-based exhaustive search that every biplanar graph on at most 13 vertices is 9-colorable; their state-of-knowledge table left the 10-chromatic cases at orders 14, 15, and 16 open. We show that every biplanar graph on at most 16 vertices is 9-colorable. The proof is non-computational and combines Gallai's structure theory for small color-critical graphs, Dirac's edge lower bound, Weinstein's strengthening for critical graphs with bounded clique number, and the classical non-biplanarity of K9.