Usually, a graph theoretic problem asks whether some class of graphs $C$ possesses a quality $P$. For example, $C$ is the class of all graphs and $P$ is the reconstructability property in Kelly-Ulam conjecture. Also, $C$ is the class of trees and $P$ is the existence of some graceful labeling in the graceful tree conjecture. The formal definition of a proof (the Hilbert-style deduction system) implies any provable assertion can be, in principle, proved by a computer. Yet in our examples, it's far from obvious how the program executed by a computer must look like to give us the proof in some period of time.

Meanwhile, there is another type of graph theoretic problems where the idea of the computer proof is straightforward. Namely, when we ask whether some $n$-vertex graph possesses a property $P$. Then we can simply use brute force generating $2^{n(n-1)/2}$ possible graphs with the vertex set $\{1,...,n\}$ and checking whether all graphs satisfy $P$. An example here is Conway's 99-graph problem asking about the existence of a $99$-vertex graph in which all pairs of adjacent and non-adjacent vertices have exactly $1$ and $2$ common neighbors, respectively. Denoting this last property as $Q$ and proving there is no such graph, we may put $n=99$ and $P=\neg Q$. Another example concerns diagonal Ramsey numbers. Say, the value of $R(5,5)$ is still unknown and we just have $43\leq R(5,5)\leq48$. If we want to improve these bounds proving $R(5,5)\leq47$, it's sufficient to generate all $2^{1081}$ $2$-edge-colorings of $K_{47}$ and check that they contain $K_5$ of one color. Here, $n=47$ and $P$ can be stated as a graph or its complement contain $K_5$.

I think that problems of the second type are of some philosophical interest. Namely, they are quite simple for understanding (at least we know how a computer could prove them) and still difficult to find the solution within a reasonable period. My question is about some other graph theoretic problems of this type you are familiar with.