A Concrete Model for the Quantum Permutation Group on 4 Points

In 2019, Jung–Weber gave an example of a concrete magic unitary M, which defines a C*-algebraic model of the quantum permutation group S4+. We show with the help of a computer that there exist no polynomials up to degree 50 separating the entries of M from the generators of C(S4+). This indicates that the magic unitary M might already define a faithful model of S4+.