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$?
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.
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.