This is an unofficial reimagining of the Archive of Formal Proofs
The Generalized Multiset Ordering is NP-Completeby René Thiemann and Lukas Schmidinger