Inclusion Proof Explorer
Enter two complexity class names to find a chain of theorems explaining why A ⊆ B (or A = B). Useful for spotting erroneous theorems that cause spurious equalities in the Hasse diagram.