Does the complement of a Petersen graph have $K_7$ minor? I'm trying to find out if the complement of a Petersen graph have $K_7$ minor,
the best i could find is a $K_6$ minor but maybe i missed something.
If anyone did any better or have a proof that it doesn't that would be really helpfull.
 A: 
Hint: Let $G$ be a graph and let $X$ and $Y$ be disjoint subgraphs of $G$. These subgraphs $X$ and $Y$ are adjacent if $xy \in E(G)$ for some $x\in V(X)$ and $y \in V(Y)$. The following proposition is well known (It can be proved by the definition of graph minors):
Proposition 1. A graph $G$ has a $K_m$-minor if and only if $G$ can be decomposed into $m$ disjoint connected subgraphs $X_1,\dots , X_m$  so that $X_i$ and $X_j$ are adjacent for $1 ≤ i < j ≤ m$.
If we want to use Proposition 1, we may (worst case scenario) need to iterate over all the 7-divisions (a total of 5880) of the 10 vertices. If symmetry is used well, it may significantly reduce the number of partitions discussed.
All in all, it should not be too hard for a computer to verify that 5880 partions satisfy the conditions in Proposition 1.

Or we can use Sagemath. It took about an hour and 30 minutes in my computer.
def has_minor(G, H):
try:
    m = G.minor(H)
    return True
except ValueError: 
    return False
has_minor(graphs.PetersenGraph().complement(),graphs.CompleteGraph(7))


False

Based on the output, the complement of a Petersen graph does not have a $K_7$ as its a minor. But there is no guarantee that the answer from Sagemath is correct.
