Exhaustively search for solutions of $n!=a_1!\cdots a_k!$ with $a_1\le n-2$ (Erdős #373, factorials)

Consider the equation $n!=a_1!\,a_2!\cdots a_k!$ in integers with $n-1>a_1\ge a_2\ge\cdots\ge a_k\ge 2$ (so every factor is a nontrivial factorial and, crucially, $a_1\le n-2$, which excludes the trivial family $n!=(n-1)!\cdot n$ that occurs whenever $n$ is itself a product of small factorials). Erdős conjectured this equation has only finitely many solutions. Only three sporadic solutions are known: $9!=7!\,3!\,3!\,2!$, $10!=7!\,6!=7!\,5!\,3!$, and $16!=14!\,5!\,2!$. GOAL (finite verification): confirm by exhaustive search that no further solution exists for $n\le N$, pushing $N$ as high as feasible; for each $n$ this is a bounded, decidable search (peel off the largest admissible factorial $\le n!$ greedily / by backtracking on prime valuations).

Acceptance. PARTIAL / PRIMARY (finite, machine-checkable): an exhaustive search certifying that for all $n\le N$ (state $N$; the larger the better) the ONLY solutions with $n-1>a_1\ge\cdots\ge a_k\ge 2$ are $n\in\{9,10,16\}$ with the multisets above — delivered as a runnable search script plus its log, using exact big-integer or prime-valuation arithmetic (Legendre's formula) so a referee can recompute. Reporting ANY previously-unknown solution $n\le N$ (with its factorial multiset) would be a significant advance. FULLY RESOLVES (not finite): a proof that the number of such solutions is finite. State the pruning/valuation argument that makes the per-$n$ search complete.