The gyroelongated square bipyramid graph X₄

import Definitions.Def_opg37357_obstacle_number

namespace OPG37357

/-- The graph `X₄` from Berman--Chappell--Faudree--Gimbel--Hartman--Williams:
the 1-skeleton of the gyroelongated square bipyramid.  Vertex `0` and vertex
`9` are the two apices, `1,2,3,4` and `5,6,7,8` are the two square rings, and
the eight remaining edges form the alternating antiprism belt. -/
def X4 : SimpleGraph (Fin 10) :=
  SimpleGraph.fromEdgeSet {
    s(0, 1), s(0, 2), s(0, 3), s(0, 4),
    s(1, 2), s(2, 3), s(3, 4), s(4, 1),
    s(1, 5), s(1, 8), s(2, 5), s(2, 6),
    s(3, 6), s(3, 7), s(4, 7), s(4, 8),
    s(5, 6), s(6, 7), s(7, 8), s(8, 5),
    s(9, 5), s(9, 6), s(9, 7), s(9, 8)
  }

end OPG37357