  We present a new method for reducing the size of graphs with a given
property. Our method, which is based on clausal proof minimization, allowed us
to compute several 553-vertex unit-distance graphs with chromatic number 5,
while the smallest published unit-distance graph with chromatic number 5 has
1581 vertices. The latter graph was constructed by Aubrey de Grey to show that
the chromatic number of the plane is at least 5. The lack of a 4-coloring of
our graphs is due to a clear pattern enforced on some vertices. Also, our
graphs can be mechanically validated in a second, which suggests that the
pattern is based on a reasonably short argument.
