In August 2003 the computer program GRAFFITI made conjecture 1001 stating that for any benzenoid graph, the size of a maximum matching equals the number of positive eigenvalues. Later, the authors learned that this conjecture was already known in 1982 to I. Gutman (Kragujevac). Here we present a proof…