Is there a nonexhaustive proof that the maximum number of spanning trees in a connected $10$-vertex $3$-regular graph is $2000$? It is well-known that the number of spanning trees in the Petersen graph is $2000$. The Petersen graph, in fact, has the most spanning trees out of all connected $10$-vertex $3$-regular (a.k.a. cubic) graphs. I believe this was first shown by Valdes in a 1991 conference paper. However, the proof is simply an exhaustive proof where the number of spanning trees in each of the $19$ connected $10$-vertex $3$-regular graphs is checked manually.
My question is the following:

Is there a nonexhaustive proof that the maximum number of spanning trees in a connected $10$-vertex $3$-regular graph is $2000$?

 A: Here's a starting point for an argument; if there is a non-exhaustive proof, maybe it can be obtained by improving these bounds. I don't mean this as a final answer, but it's a proof of concept that a non-exhaustive proof could possibly exist, and what it could look like.
Lemma. If a $10$-vertex cubic graph is Hamiltonian, it has at most $3205$ spanning trees.
Proof. Actually, all we need is that the graph as a $3$-edge-coloring. If there is a Hamiltonian cycle, we can color its edges alternately red and blue, and then color the leftover matching green.
We count the number of spanning trees that use $0$, $1$, or $2$ red edges.

*

*If $0$ red edges are used, then there are at most $\binom{10}{9}=10$ trees, since we need to pick $9$ of the remaining edges.

*If $1$ red edge is used, then the blue and green edges form two paths of lengths $a,b$ (with $a+b=10$) from one endpoint of the red edge to the other, or from an endpoint back to itself. Either way, one edge from each path must be deleted, for at most $ab \le 25$ trees.

*If $2$ red edges are used, then the blue and green paths form four paths of length $a,b,c,d$ with $a+b+c+d=10$ that start and end at one of the chosen red edges. We must delete an edge from all but one of the paths to get a tree, so there are at most $abc+abd+acd+bcd$ trees. This is maximized when $a,b,c,d = 2,2,3,3$ in some order, when we get an upper bound of $60$.

Altogether there are at most $\binom 50 \cdot 10 + \binom51 \cdot 25 + \binom 52 \cdot 60 = 735$ such trees. There are also at most $735$ trees that use at most $2$ blue edges, and at most $735$ trees that use at most $2$ green edges. Finally, there are at most $\binom 53^3 = 1000$ trees that use $3$ edges of each color. The total is $3 \cdot 735 + 1000 = 3205$. $\square$
(Note that $735$ is close to the truth; some cubic graphs have $\approx 600$ graphs of this type, in some edge-colorings. On the other hand, $1000$ is a bad overestimate.)

If we could get this bound from $3205$ down to less than $2000$, we'd be done.

*

*If a $10$-vertex cubic graph has a bridge, then it connects two $5$-vertex pieces with $7$ edges each. (The number of vertices in each piece must be odd by degree counts, and $3$ vertices is too small to have any vertices of degre $3$.) A spanning tree must take the bridge and $4$ edges from each piece, and there are $\binom 74^2 = 1225$ ways to do that, some of which won't even make trees.

*The Petersen graph is the unique smallest bridgeless cubic graph that's not Hamiltonian. (This is also something we can prove without an exhaustive search.)

