Induced subgraph decider for C(S₀,₅)

Built-in examples: 

No certificate generated yet.

The curve graph C(S₀,₅) has vertices corresponding to isotopy classes of essential nonperipheral simple closed curves, and edges for disjointness.

This tool uses fast obstructions (triangle, 4-cycle, and Petersen homomorphism checks) to rigorously prove NO.

It uses a bounded certificate search to find YES certificates for induced subgraphs of the Petersen graph or forests (which embed in the Farey graph).

If the graph passes obstructions but fails the bounded search, it returns INCONCLUSIVE in Practical Mode. The Exact Mode using Aougab-Biringer-Gaster exhaustive bound is currently marked unavailable.