A computer assisted optimal depth lower bound for sorting networks with nine inputs

It is demonstrated that there is no nine-input sorting network of depth six. The proof was obtained by executing on a supercomputer a branch-and-bound algorithm which constructs and tests a critical subset of all possible candidates. Such proofs can be classified as experimental science, rather than mathematics. In keeping with the paradigms of experimental science, a high-level description of the experiment and analysis of the result are given.