--- Distinct DNF Tautologies with as large as possible monomials By Shalosh B. Ekhad ----------------------------------------------- The largest minimial size of monomials in DNF tautologies with, 2, variables, all of the same size, that is feasible (on density grounds is) , 0 Here is such a distinct DNF tautology with, 2, variales, each of size, 0 1 ----------------------------------------------- The largest minimial size of monomials in DNF tautologies with, 3, variables, all of the same size, that is feasible (on density grounds is) , 1 We were only able to cover, 7, truth-vectors out of the total of, 8, here is such an almost-tautology that is distinct X[1] + X[2] + X[3] ----------------------------------------------- The largest minimial size of monomials in DNF tautologies with, 4, variables, all of the same size, that is feasible (on density grounds is) , 2 Here is such a distinct DNF tautology with, 4, variales, each of size, 2 NotX[1] NotX[3] + NotX[1] X[2] + NotX[2] X[3] + NotX[3] NotX[4] + NotX[4] X[2] + X[1] X[4] ----------------------------------------------- The largest minimial size of monomials in DNF tautologies with, 5, variables, all of the same size, that is feasible (on density grounds is) , 3 We were only able to cover, 31, truth-vectors out of the total of, 32, here is such an almost-tautology that is distinct NotX[1] NotX[3] X[5] + NotX[1] NotX[5] X[2] + NotX[2] NotX[4] NotX[5] + NotX[2] NotX[4] X[1] + NotX[2] X[3] X[4] + NotX[3] NotX[4] X[1] + NotX[3] NotX[5] X[4] + X[1] X[2] X[3] + X[1] X[4] X[5] + X[2] X[3] X[5] ----------------------------------------------- The largest minimial size of monomials in DNF tautologies with, 6, variables, all of the same size, that is feasible (on density grounds is) , 3 Here is such a distinct DNF tautology with, 6, variales, each of size, 3 NotX[1] NotX[2] NotX[4] + NotX[1] NotX[3] X[4] + NotX[1] NotX[5] X[2] + NotX[1] X[3] X[5] + NotX[2] NotX[6] X[1] + NotX[2] X[3] X[4] + NotX[2] X[3] X[6] + NotX[3] X[1] X[6] + NotX[3] X[2] X[5] + NotX[4] NotX[6] X[1] + NotX[5] X[1] X[6] + NotX[5] X[2] X[4] + X[1] X[2] X[3] + X[1] X[4] X[5] ----------------------------------------------- The largest minimial size of monomials in DNF tautologies with, 7, variables, all of the same size, that is feasible (on density grounds is) , 4 Here is such a distinct DNF tautology with, 7, variales, each of size, 4 NotX[1] NotX[2] NotX[3] NotX[5] + NotX[1] NotX[2] NotX[6] X[3] + NotX[1] NotX[2] X[5] X[6] + NotX[1] NotX[3] NotX[7] X[2] + NotX[1] NotX[3] X[4] X[7] + NotX[1] NotX[4] NotX[5] X[6] + NotX[1] NotX[4] NotX[6] NotX[7] + NotX[1] NotX[4] X[2] X[7] + NotX[1] NotX[5] X[3] X[4] + NotX[1] NotX[7] X[3] X[5] + NotX[2] NotX[3] NotX[6] X[5] + NotX[2] NotX[4] NotX[5] X[1] + NotX[2] NotX[6] X[1] X[4] + NotX[2] NotX[7] X[1] X[6] + NotX[2] X[3] X[5] X[7] + NotX[3] NotX[4] NotX[6] X[1] + NotX[3] NotX[5] X[1] X[6] + NotX[3] NotX[6] X[2] X[4] + NotX[3] NotX[7] X[2] X[6] + NotX[4] NotX[5] X[2] X[3] + NotX[4] NotX[7] X[1] X[5] + X[1] X[2] X[3] X[4] + X[1] X[2] X[5] X[7] + X[1] X[3] X[6] X[7] + X[1] X[5] X[6] X[7] + X[2] X[3] X[4] X[7] ----------------------------------------------- The largest minimial size of monomials in DNF tautologies with, 8, variables, all of the same size, that is feasible (on density grounds is) , 5 Here is such a distinct DNF tautology with, 8, variales, each of size, 5 NotX[1] NotX[2] NotX[3] NotX[4] NotX[6] + NotX[1] NotX[2] NotX[3] NotX[7] X[4] + NotX[1] NotX[2] NotX[3] X[6] X[7] + NotX[1] NotX[2] NotX[4] NotX[8] X[3] + NotX[1] NotX[2] NotX[5] X[3] X[8] + NotX[1] NotX[3] NotX[4] NotX[7] X[6] + NotX[1] NotX[3] NotX[5] NotX[6] X[2] + NotX[1] NotX[3] NotX[6] X[5] X[7] + NotX[1] NotX[3] NotX[7] X[2] X[5] + NotX[1] NotX[4] NotX[6] X[3] X[8] + NotX[1] NotX[4] X[2] X[6] X[7] + NotX[1] NotX[5] NotX[6] X[4] X[7] + NotX[1] NotX[5] NotX[8] X[3] X[4] + NotX[1] NotX[6] NotX[8] X[2] X[3] + NotX[1] NotX[7] X[2] X[3] X[8] + NotX[1] X[3] X[4] X[5] X[6] + NotX[1] X[4] X[5] X[7] X[8] + NotX[2] NotX[3] NotX[5] NotX[8] X[6] + NotX[2] NotX[4] NotX[5] NotX[6] X[1] + NotX[2] NotX[4] NotX[7] X[1] X[5] + NotX[2] NotX[4] X[3] X[5] X[8] + NotX[2] NotX[5] NotX[8] X[1] X[4] + NotX[2] NotX[5] X[1] X[6] X[8] + NotX[2] NotX[6] X[1] X[4] X[8] + NotX[2] NotX[7] X[3] X[4] X[5] + NotX[2] NotX[8] X[3] X[5] X[7] + NotX[2] X[1] X[5] X[6] X[7] + NotX[3] NotX[4] NotX[8] X[1] X[7] + NotX[3] NotX[5] X[2] X[4] X[6] + NotX[3] NotX[6] NotX[7] NotX[8] X[2] + NotX[3] NotX[6] X[1] X[7] X[8] + NotX[3] NotX[7] X[1] X[4] X[5] + NotX[3] X[2] X[4] X[6] X[7] + NotX[4] NotX[6] X[1] X[5] X[8] + NotX[4] NotX[7] NotX[8] X[1] X[2] + NotX[4] NotX[8] X[2] X[3] X[6] + NotX[5] NotX[6] NotX[7] X[2] X[4] + NotX[5] NotX[6] X[2] X[3] X[7] + NotX[5] NotX[7] X[1] X[2] X[8] + NotX[5] NotX[8] X[1] X[3] X[6] + NotX[6] NotX[8] X[1] X[4] X[7] + NotX[7] X[1] X[5] X[6] X[8] + NotX[8] X[1] X[3] X[5] X[7] + X[1] X[2] X[3] X[4] X[5] + X[1] X[2] X[6] X[7] X[8] + X[2] X[3] X[4] X[7] X[8] ----------------------------------------------- The largest minimial size of monomials in DNF tautologies with, 9, variables, all of the same size, that is feasible (on density grounds is) , 6 We were only able to cover, 499, truth-vectors out of the total of, 512, here is such an almost-tautology that is distinct NotX[1] NotX[2] NotX[3] NotX[4] NotX[5] NotX[7] + NotX[1] NotX[2] NotX[3] NotX[4] NotX[8] X[5] + NotX[1] NotX[2] NotX[3] NotX[4] X[7] X[8] + NotX[1] NotX[2] NotX[3] NotX[5] NotX[9] X[4] + NotX[1] NotX[2] NotX[3] NotX[6] X[4] X[9] + NotX[1] NotX[2] NotX[4] NotX[6] NotX[7] X[3] + NotX[1] NotX[2] NotX[4] NotX[8] X[3] X[6] + NotX[1] NotX[2] NotX[5] X[3] X[7] X[8] + NotX[1] NotX[2] NotX[7] NotX[9] X[3] X[4] + NotX[1] NotX[2] NotX[8] X[3] X[4] X[9] + NotX[1] NotX[2] NotX[9] X[4] X[5] X[7] + NotX[1] NotX[3] NotX[5] NotX[6] NotX[7] X[2] + NotX[1] NotX[3] NotX[5] NotX[8] X[2] X[6] + NotX[1] NotX[3] NotX[6] NotX[9] X[2] X[5] + NotX[1] NotX[3] NotX[6] X[2] X[7] X[9] + NotX[1] NotX[3] NotX[7] NotX[9] X[4] X[5] + NotX[1] NotX[3] NotX[7] X[2] X[5] X[9] + NotX[1] NotX[3] X[2] X[6] X[7] X[8] + NotX[1] NotX[3] X[4] X[6] X[8] X[9] + NotX[1] NotX[4] NotX[7] NotX[9] X[6] X[8] + NotX[1] NotX[4] NotX[7] X[3] X[8] X[9] + NotX[1] NotX[4] X[3] X[5] X[7] X[8] + NotX[1] NotX[5] NotX[6] NotX[9] X[7] X[8] + NotX[1] NotX[5] NotX[8] NotX[9] X[2] X[3] + NotX[1] NotX[5] NotX[8] X[4] X[6] X[9] + NotX[1] NotX[6] NotX[8] NotX[9] X[3] X[7] + NotX[1] NotX[6] NotX[8] X[2] X[3] X[9] + NotX[1] NotX[7] NotX[9] X[2] X[3] X[8] + NotX[1] NotX[8] X[2] X[5] X[6] X[7] + NotX[1] X[3] X[4] X[5] X[8] X[9] + NotX[2] NotX[3] NotX[4] NotX[5] NotX[8] X[7] + NotX[2] NotX[4] NotX[5] NotX[6] NotX[7] X[1] + NotX[2] NotX[4] NotX[5] NotX[8] X[1] X[6] + NotX[2] NotX[4] NotX[5] X[1] X[7] X[8] + NotX[2] NotX[4] NotX[6] NotX[8] X[7] X[9] + NotX[2] NotX[4] NotX[6] NotX[9] X[1] X[5] + NotX[2] NotX[4] NotX[7] X[1] X[6] X[8] + NotX[2] NotX[4] NotX[7] X[5] X[8] X[9] + NotX[2] NotX[4] NotX[8] X[1] X[5] X[9] + NotX[2] NotX[6] NotX[7] NotX[9] X[1] X[4] + NotX[2] NotX[6] NotX[8] X[1] X[4] X[9] + NotX[2] NotX[7] NotX[9] X[4] X[5] X[6] + NotX[2] NotX[7] X[1] X[4] X[8] X[9] + NotX[2] NotX[8] X[4] X[5] X[6] X[9] + NotX[2] NotX[9] X[1] X[5] X[6] X[7] + NotX[2] X[1] X[5] X[7] X[8] X[9] + NotX[3] NotX[4] NotX[5] X[2] X[6] X[9] + NotX[3] NotX[4] NotX[6] NotX[7] NotX[9] X[5] + NotX[3] NotX[4] NotX[8] NotX[9] X[2] X[6] + NotX[3] NotX[4] NotX[8] X[2] X[7] X[9] + NotX[3] NotX[4] NotX[9] X[2] X[5] X[7] + NotX[3] NotX[4] X[5] X[6] X[8] X[9] + NotX[3] NotX[5] NotX[6] NotX[8] NotX[9] X[7] + NotX[3] NotX[5] NotX[6] NotX[8] X[4] X[7] + NotX[3] NotX[5] NotX[6] X[1] X[7] X[8] + NotX[3] NotX[5] NotX[7] NotX[9] X[1] X[8] + NotX[3] NotX[5] X[1] X[4] X[6] X[7] + NotX[3] NotX[6] NotX[9] X[1] X[4] X[5] + NotX[3] NotX[6] X[2] X[5] X[8] X[9] + NotX[3] NotX[7] NotX[8] X[1] X[4] X[6] + NotX[3] NotX[7] X[2] X[4] X[6] X[8] + NotX[4] NotX[5] NotX[6] NotX[8] NotX[9] X[7] + NotX[4] NotX[5] X[2] X[3] X[6] X[7] + NotX[4] NotX[6] NotX[7] X[1] X[5] X[8] + NotX[4] NotX[7] NotX[9] X[1] X[5] X[6] + NotX[4] NotX[7] X[2] X[3] X[6] X[9] + NotX[4] NotX[8] X[2] X[3] X[5] X[6] + NotX[5] NotX[6] NotX[7] X[2] X[8] X[9] + NotX[5] NotX[6] NotX[8] NotX[9] X[1] X[2] + NotX[5] NotX[6] X[1] X[3] X[7] X[9] + NotX[5] NotX[7] X[3] X[4] X[8] X[9] + NotX[5] NotX[8] X[1] X[3] X[4] X[6] + NotX[5] NotX[9] X[1] X[3] X[6] X[8] + NotX[5] X[2] X[3] X[4] X[8] X[9] + NotX[6] NotX[7] NotX[8] X[1] X[2] X[9] + NotX[6] NotX[7] NotX[8] X[2] X[3] X[5] + NotX[6] NotX[7] NotX[9] X[2] X[3] X[8] + NotX[6] NotX[9] X[1] X[3] X[4] X[7] + NotX[6] NotX[9] X[2] X[3] X[5] X[7] + NotX[8] X[1] X[4] X[5] X[7] X[9] + X[1] X[2] X[3] X[4] X[5] X[6] + X[2] X[3] X[5] X[7] X[8] X[9] + X[2] X[4] X[5] X[6] X[7] X[8] + X[3] X[4] X[6] X[7] X[8] X[9] ----------------------------------------------- The largest minimial size of monomials in DNF tautologies with, 10, variables, all of the same size, that is feasible (on density grounds is) , 6 Here is such a distinct DNF tautology with, 10, variales, each of size, 6 NotX[1] NotX[2] NotX[3] NotX[4] NotX[5] NotX[7] + NotX[1] NotX[2] NotX[3] NotX[4] NotX[8] X[5] + NotX[1] NotX[2] NotX[3] NotX[4] X[7] X[8] + NotX[1] NotX[2] NotX[3] NotX[5] NotX[9] X[4] + NotX[1] NotX[2] NotX[3] NotX[10] X[4] X[5] + NotX[1] NotX[2] NotX[3] X[4] X[9] X[10] + NotX[1] NotX[2] NotX[4] NotX[6] NotX[7] X[3] + NotX[1] NotX[2] NotX[4] NotX[8] X[3] X[6] + NotX[1] NotX[2] NotX[4] NotX[10] X[6] X[8] + NotX[1] NotX[2] NotX[5] NotX[8] NotX[9] X[7] + NotX[1] NotX[2] NotX[6] NotX[7] NotX[10] X[9] + NotX[1] NotX[2] NotX[6] NotX[9] X[3] X[4] + NotX[1] NotX[2] NotX[6] X[3] X[7] X[9] + NotX[1] NotX[2] NotX[7] X[5] X[8] X[10] + NotX[1] NotX[2] NotX[9] X[5] X[7] X[10] + NotX[1] NotX[2] NotX[10] X[3] X[4] X[6] + NotX[1] NotX[2] X[3] X[6] X[8] X[10] + NotX[1] NotX[3] NotX[4] NotX[5] NotX[8] X[7] + NotX[1] NotX[3] NotX[4] NotX[7] NotX[9] X[2] + NotX[1] NotX[3] NotX[4] NotX[10] X[2] X[7] + NotX[1] NotX[3] NotX[5] NotX[10] X[4] X[9] + NotX[1] NotX[3] NotX[5] X[2] X[9] X[10] + NotX[1] NotX[3] NotX[5] X[4] X[6] X[8] + NotX[1] NotX[3] NotX[5] X[6] X[8] X[10] + NotX[1] NotX[3] NotX[6] NotX[9] NotX[10] X[5] + NotX[1] NotX[3] NotX[6] NotX[9] X[4] X[8] + NotX[1] NotX[3] NotX[7] NotX[9] X[4] X[10] + NotX[1] NotX[3] NotX[8] NotX[9] X[2] X[4] + NotX[1] NotX[3] NotX[10] X[2] X[4] X[8] + NotX[1] NotX[4] NotX[5] NotX[9] X[3] X[8] + NotX[1] NotX[4] NotX[6] NotX[10] X[3] X[5] + NotX[1] NotX[4] NotX[6] X[2] X[7] X[10] + NotX[1] NotX[4] NotX[7] NotX[10] X[2] X[9] + NotX[1] NotX[4] X[2] X[5] X[6] X[10] + NotX[1] NotX[5] NotX[6] NotX[7] X[2] X[3] + NotX[1] NotX[5] NotX[6] NotX[8] X[3] X[7] + NotX[1] NotX[5] NotX[7] X[3] X[4] X[6] + NotX[1] NotX[5] NotX[7] X[3] X[8] X[9] + NotX[1] NotX[5] NotX[8] X[2] X[3] X[6] + NotX[1] NotX[5] NotX[8] X[3] X[4] X[10] + NotX[1] NotX[5] X[2] X[3] X[7] X[8] + NotX[1] NotX[6] NotX[9] X[2] X[3] X[5] + NotX[1] NotX[6] NotX[10] X[3] X[4] X[9] + NotX[1] NotX[6] X[2] X[5] X[9] X[10] + NotX[1] NotX[7] X[2] X[4] X[5] X[10] + NotX[1] NotX[7] X[3] X[5] X[9] X[10] + NotX[1] NotX[8] NotX[10] X[2] X[4] X[9] + NotX[1] NotX[8] X[3] X[4] X[6] X[10] + NotX[1] NotX[10] X[2] X[3] X[5] X[6] + NotX[1] X[2] X[5] X[6] X[7] X[10] + NotX[2] NotX[3] NotX[5] NotX[7] NotX[9] X[1] + NotX[2] NotX[3] NotX[5] NotX[10] X[1] X[7] + NotX[2] NotX[3] NotX[6] X[1] X[9] X[10] + NotX[2] NotX[3] NotX[8] NotX[9] X[1] X[5] + NotX[2] NotX[3] NotX[10] X[1] X[5] X[8] + NotX[2] NotX[4] NotX[7] X[1] X[6] X[9] + NotX[2] NotX[4] NotX[8] X[1] X[7] X[10] + NotX[2] NotX[6] NotX[7] NotX[8] X[1] X[3] + NotX[2] NotX[6] NotX[8] NotX[10] X[1] X[9] + NotX[2] NotX[6] NotX[10] X[1] X[3] X[7] + NotX[2] NotX[7] NotX[9] X[1] X[3] X[8] + NotX[2] NotX[7] X[1] X[4] X[8] X[9] + NotX[2] NotX[8] NotX[9] X[1] X[3] X[6] + NotX[2] NotX[8] X[1] X[4] X[6] X[9] + NotX[2] NotX[9] X[1] X[5] X[8] X[10] + NotX[2] X[1] X[3] X[7] X[8] X[10] + NotX[2] X[1] X[6] X[7] X[8] X[9] + NotX[3] NotX[4] NotX[10] X[1] X[8] X[9] + NotX[3] NotX[4] X[1] X[7] X[8] X[10] + NotX[3] NotX[5] NotX[7] X[1] X[6] X[10] + NotX[3] NotX[5] NotX[9] X[1] X[4] X[7] + NotX[3] NotX[7] NotX[9] NotX[10] X[1] X[2] + NotX[3] NotX[8] NotX[9] X[1] X[2] X[10] + NotX[3] NotX[8] NotX[10] X[1] X[5] X[7] + NotX[3] NotX[9] X[1] X[5] X[6] X[7] + NotX[4] NotX[5] NotX[6] X[1] X[2] X[7] + NotX[4] NotX[5] X[1] X[2] X[6] X[8] + NotX[4] NotX[6] NotX[7] X[1] X[3] X[9] + NotX[4] NotX[6] X[1] X[2] X[5] X[9] + NotX[4] NotX[7] NotX[8] NotX[9] X[1] X[3] + NotX[4] NotX[7] X[1] X[3] X[6] X[10] + NotX[4] NotX[8] X[1] X[2] X[6] X[7] + NotX[4] NotX[9] X[1] X[2] X[5] X[8] + NotX[4] NotX[10] X[1] X[3] X[5] X[7] + NotX[5] NotX[6] NotX[7] X[1] X[2] X[8] + NotX[5] NotX[6] NotX[8] X[1] X[2] X[9] + NotX[5] NotX[7] X[1] X[2] X[4] X[9] + NotX[5] NotX[8] NotX[10] X[1] X[2] X[6] + NotX[5] NotX[8] NotX[10] X[1] X[3] X[9] + NotX[5] NotX[9] X[1] X[3] X[4] X[6] + NotX[5] X[1] X[2] X[4] X[7] X[8] + NotX[6] NotX[7] NotX[8] X[1] X[2] X[10] + NotX[6] NotX[8] X[1] X[3] X[4] X[7] + NotX[6] NotX[8] X[1] X[3] X[7] X[10] + NotX[6] NotX[9] NotX[10] X[1] X[2] X[4] + NotX[7] X[1] X[2] X[5] X[6] X[9] + NotX[8] X[1] X[2] X[7] X[9] X[10] + NotX[9] X[1] X[3] X[6] X[7] X[8] + NotX[10] X[1] X[2] X[4] X[5] X[9] + X[1] X[2] X[3] X[4] X[5] X[6] + X[1] X[2] X[4] X[5] X[8] X[10] + X[1] X[3] X[5] X[6] X[8] X[9] ----------------------------------------------- The largest minimial size of monomials in DNF tautologies with, 11, variables, all of the same size, that is feasible (on density grounds is) , 7 Here is such a distinct DNF tautology with, 11, variales, each of size, 7 X[1] X[2] NotX[4] NotX[5] X[6] X[8] X[9] + X[1] NotX[3] X[4] NotX[5] X[6] X[10] X[11] + NotX[1] NotX[2] X[3] NotX[5] X[6] X[10] X[11] + NotX[1] X[2] X[3] NotX[5] X[6] X[8] X[9] + NotX[1] X[3] NotX[5] X[6] X[7] X[8] X[11] + NotX[1] NotX[2] NotX[3] NotX[4] X[5] X[10] X[11] + X[1] NotX[2] NotX[4] X[6] X[8] X[9] X[11] + NotX[1] X[2] NotX[4] X[5] X[6] X[9] X[11] + NotX[1] X[3] NotX[4] X[6] X[7] X[9] X[10] + X[1] X[2] NotX[4] X[5] X[6] X[8] X[11] + NotX[1] NotX[2] NotX[3] X[4] X[7] X[9] X[11] + NotX[1] X[2] NotX[3] X[4] X[8] X[9] X[11] + NotX[1] NotX[3] X[6] X[7] X[9] X[10] X[11] + X[1] NotX[2] X[4] X[6] X[8] X[9] X[10] + NotX[1] X[2] X[4] X[6] X[7] X[9] X[10] + NotX[1] X[4] X[5] X[6] X[8] X[10] X[11] + X[1] X[2] X[3] X[4] X[5] X[6] X[7] + X[1] X[2] X[4] X[5] X[7] X[8] X[10] + X[1] X[3] X[6] X[8] X[9] X[10] X[11] + X[1] X[4] X[5] X[6] X[7] X[8] X[11] + X[1] X[4] X[5] X[6] X[9] X[10] X[11] + NotX[1] X[2] NotX[3] NotX[6] X[7] NotX[8] X[10] + X[1] X[3] X[5] NotX[6] NotX[8] X[9] X[10] + X[1] NotX[2] NotX[3] NotX[5] X[7] NotX[8] X[9] + NotX[1] NotX[2] NotX[5] X[6] NotX[8] X[9] X[10] + NotX[1] X[2] X[3] NotX[5] X[6] NotX[8] X[10] + X[1] X[3] X[4] NotX[5] NotX[8] X[9] X[10] + X[1] X[2] NotX[4] NotX[8] X[9] X[10] X[11] + X[1] NotX[2] NotX[3] X[5] NotX[8] X[9] X[10] + X[1] NotX[3] X[4] X[5] X[7] NotX[8] X[10] + X[1] NotX[2] X[3] X[6] NotX[8] X[9] X[11] + NotX[1] X[3] X[4] X[7] NotX[8] X[9] X[11] + NotX[1] X[2] X[3] NotX[5] NotX[6] NotX[7] X[10] + X[1] X[2] NotX[4] NotX[6] NotX[7] X[8] X[10] + X[1] NotX[2] X[3] NotX[6] NotX[7] X[8] X[9] + X[1] NotX[4] NotX[5] X[6] NotX[7] X[8] X[10] + X[1] NotX[2] NotX[3] NotX[5] NotX[7] X[8] X[11] + NotX[1] X[2] NotX[3] NotX[4] NotX[7] X[10] X[11] + NotX[1] NotX[2] NotX[3] X[4] NotX[7] X[8] X[10] + NotX[1] NotX[2] X[5] X[6] NotX[7] X[10] X[11] + NotX[1] X[3] X[4] X[5] X[6] NotX[7] X[9] + X[1] X[2] X[4] X[5] NotX[7] X[8] X[9] + X[1] X[2] NotX[4] NotX[5] NotX[6] X[7] X[8] + NotX[1] X[3] X[4] NotX[5] NotX[6] X[7] X[11] + X[1] X[2] X[4] NotX[5] NotX[6] X[10] X[11] + X[1] NotX[3] NotX[4] NotX[6] X[8] X[9] X[10] + NotX[1] NotX[2] X[3] NotX[4] NotX[6] X[10] X[11] + NotX[1] X[2] NotX[4] NotX[6] X[7] X[8] X[11] + X[1] X[2] NotX[4] X[5] NotX[6] X[7] X[10] + X[1] NotX[3] X[4] X[5] NotX[6] X[8] X[11] + NotX[1] NotX[2] X[3] X[4] NotX[6] X[8] X[9] + X[1] NotX[2] X[3] NotX[6] X[7] X[9] X[11] + NotX[1] X[2] X[3] X[5] NotX[6] X[9] X[11] + X[1] X[4] NotX[6] X[8] X[9] X[10] X[11] + NotX[1] NotX[2] NotX[3] NotX[4] NotX[5] X[8] X[9] + X[1] NotX[2] X[5] NotX[6] NotX[7] X[8] NotX[9] + NotX[1] X[3] NotX[6] NotX[7] X[8] NotX[9] X[11] + NotX[1] NotX[3] NotX[5] X[6] NotX[7] X[8] NotX[9] + NotX[1] X[3] NotX[4] X[6] NotX[7] X[8] NotX[9] + X[1] NotX[2] NotX[3] X[5] NotX[7] NotX[9] X[10] + X[1] X[2] X[4] X[6] NotX[7] X[8] NotX[9] + NotX[1] NotX[3] NotX[4] NotX[5] NotX[6] X[8] NotX[9] + X[1] NotX[2] NotX[3] NotX[5] NotX[6] X[7] NotX[9] + X[1] X[3] NotX[5] NotX[6] NotX[9] X[10] X[11] + NotX[1] NotX[2] X[3] X[4] NotX[6] X[7] NotX[9] + X[1] NotX[2] X[5] NotX[6] X[7] NotX[9] X[11] + NotX[1] X[2] X[5] NotX[6] NotX[9] X[10] X[11] + X[1] X[3] X[4] NotX[6] X[8] NotX[9] X[11] + NotX[1] NotX[2] NotX[3] NotX[4] NotX[5] X[6] NotX[9] + X[1] X[2] NotX[4] NotX[5] X[6] X[7] NotX[9] + NotX[1] NotX[2] NotX[3] X[4] NotX[5] X[7] NotX[9] + NotX[1] X[2] X[4] NotX[5] X[8] NotX[9] X[11] + X[1] NotX[3] NotX[4] X[6] NotX[9] X[10] X[11] + NotX[1] NotX[4] X[5] X[6] X[7] NotX[9] X[10] + NotX[1] X[2] NotX[3] X[6] X[7] NotX[9] X[10] + NotX[1] NotX[2] X[4] X[5] X[7] NotX[9] X[11] + X[1] NotX[2] X[3] X[6] NotX[9] X[10] X[11] + NotX[1] X[2] X[3] X[5] X[6] NotX[9] X[10] + X[1] X[2] X[4] X[6] X[7] NotX[9] X[11] + X[1] NotX[2] NotX[3] NotX[5] NotX[6] NotX[7] NotX[8] + NotX[1] NotX[3] NotX[6] NotX[7] NotX[8] X[9] X[10] + NotX[1] NotX[2] X[3] X[4] NotX[6] NotX[7] NotX[8] + X[1] X[3] X[4] X[5] NotX[6] NotX[7] NotX[8] + X[1] NotX[4] NotX[5] NotX[7] NotX[8] X[9] X[11] + NotX[1] NotX[2] NotX[3] X[4] NotX[5] NotX[7] NotX[8] + X[1] X[2] NotX[3] NotX[7] NotX[8] X[10] X[11] + NotX[1] X[2] X[4] NotX[7] NotX[8] X[9] X[10] + NotX[1] NotX[2] NotX[3] NotX[4] NotX[5] NotX[6] NotX[8] + NotX[1] X[3] NotX[4] NotX[6] X[7] NotX[8] X[11] + NotX[1] NotX[2] X[3] NotX[4] NotX[5] NotX[8] NotX[10] + NotX[1] X[2] NotX[5] X[6] NotX[8] NotX[10] X[11] + X[1] X[2] NotX[5] NotX[8] X[9] NotX[10] X[11] + X[1] X[3] NotX[4] NotX[8] X[9] NotX[10] X[11] + NotX[1] X[2] NotX[3] X[4] NotX[8] X[9] NotX[10] + X[1] X[2] NotX[3] NotX[8] X[9] NotX[10] X[11] + NotX[1] NotX[2] NotX[5] NotX[6] NotX[7] X[8] NotX[10] + X[1] X[3] NotX[5] NotX[6] NotX[7] X[9] NotX[10] + NotX[1] NotX[3] NotX[5] NotX[7] X[8] X[9] NotX[10] + NotX[1] X[4] NotX[5] NotX[7] X[9] NotX[10] X[11] + X[1] NotX[3] NotX[4] NotX[7] X[8] X[9] NotX[10] + NotX[1] X[3] NotX[4] NotX[7] X[9] NotX[10] X[11] + X[1] X[3] NotX[4] X[5] NotX[7] X[9] NotX[10] + NotX[1] NotX[2] NotX[3] X[4] X[5] NotX[7] NotX[10] + NotX[1] NotX[2] X[3] X[4] X[6] NotX[7] NotX[10] + X[1] X[4] X[6] NotX[7] X[8] X[9] NotX[10] + NotX[1] X[3] NotX[4] NotX[5] NotX[6] X[8] NotX[10] + NotX[1] NotX[2] NotX[3] NotX[4] X[5] NotX[6] NotX[10] + NotX[1] NotX[4] X[5] NotX[6] X[8] X[9] NotX[10] + X[1] X[2] NotX[4] X[5] NotX[6] X[8] NotX[10] + X[1] NotX[2] NotX[5] X[7] X[8] X[9] NotX[10] + X[1] X[2] X[4] NotX[5] X[8] X[9] NotX[10] + NotX[1] NotX[3] NotX[4] X[6] X[8] NotX[10] X[11] + NotX[1] NotX[2] NotX[4] X[6] X[9] NotX[10] X[11] + X[1] NotX[2] NotX[3] X[5] X[7] NotX[10] X[11] + NotX[1] X[3] X[4] X[5] X[6] X[7] NotX[10] + X[1] X[3] X[4] X[5] X[9] NotX[10] X[11] + NotX[1] X[4] NotX[6] NotX[7] NotX[8] NotX[9] X[11] + X[1] X[3] NotX[4] X[5] NotX[7] NotX[8] NotX[9] + NotX[1] X[2] NotX[3] X[4] NotX[7] NotX[8] NotX[9] + X[1] X[2] X[6] NotX[7] NotX[8] NotX[9] X[10] + X[1] NotX[2] X[3] NotX[6] NotX[8] NotX[9] X[10] + X[1] X[4] X[5] NotX[6] X[7] NotX[8] NotX[9] + X[1] X[2] NotX[4] X[7] NotX[8] NotX[9] X[11] + NotX[1] NotX[2] X[3] NotX[4] NotX[5] X[8] NotX[11] + NotX[1] NotX[3] X[4] NotX[5] X[7] X[8] NotX[11] + X[1] NotX[3] NotX[5] X[7] X[9] X[10] NotX[11] + NotX[1] X[4] NotX[5] X[8] X[9] X[10] NotX[11] + X[1] X[2] X[4] NotX[5] X[8] X[10] NotX[11] + NotX[1] NotX[2] NotX[3] NotX[4] X[5] X[6] NotX[11] + NotX[1] X[2] NotX[3] NotX[4] X[6] X[9] NotX[11] + NotX[1] NotX[2] X[3] NotX[4] X[5] X[9] NotX[11] + X[1] NotX[2] NotX[4] X[6] X[7] X[10] NotX[11] + X[1] X[2] NotX[4] X[5] X[6] X[7] NotX[11] + NotX[1] NotX[2] NotX[3] X[4] X[5] X[7] NotX[11] + X[1] NotX[2] NotX[3] X[5] X[8] X[9] NotX[11] + NotX[1] NotX[2] X[3] X[4] X[6] X[7] NotX[11] + NotX[1] X[3] X[5] X[6] X[8] X[9] NotX[11] + X[1] X[3] X[4] X[6] X[7] X[10] NotX[11] + X[1] X[2] NotX[3] NotX[7] NotX[8] NotX[9] NotX[10] + NotX[1] X[4] NotX[5] X[7] NotX[8] NotX[9] NotX[10] + NotX[1] NotX[3] X[5] NotX[8] NotX[9] NotX[10] X[11] + X[1] X[2] NotX[4] NotX[5] NotX[7] NotX[9] NotX[10] + X[1] NotX[2] X[5] X[6] NotX[7] NotX[9] NotX[10] + NotX[1] X[2] X[5] NotX[7] NotX[9] NotX[10] X[11] + X[1] X[2] X[4] NotX[5] NotX[6] NotX[9] NotX[10] + NotX[1] X[3] X[4] X[5] NotX[6] NotX[9] NotX[10] + X[1] NotX[2] X[3] NotX[5] NotX[9] NotX[10] X[11] + NotX[1] X[2] NotX[3] NotX[4] X[6] NotX[9] NotX[10] + NotX[1] NotX[2] X[3] NotX[4] X[5] NotX[9] NotX[10] + NotX[1] X[2] X[3] NotX[4] NotX[9] NotX[10] X[11] + NotX[1] X[2] NotX[3] X[4] X[7] NotX[9] NotX[10] + X[1] NotX[2] X[6] X[7] NotX[9] NotX[10] X[11] + NotX[1] X[3] NotX[6] NotX[7] NotX[8] NotX[10] X[11] + X[1] NotX[3] NotX[5] X[6] NotX[7] NotX[8] NotX[10] + X[1] NotX[2] NotX[3] X[5] NotX[7] NotX[8] NotX[10] + X[1] X[3] X[4] X[6] NotX[7] NotX[8] NotX[10] + NotX[1] X[2] NotX[3] NotX[4] NotX[6] NotX[8] NotX[10] + X[1] X[2] X[4] X[5] X[7] NotX[10] NotX[11] + X[1] X[2] NotX[6] NotX[8] NotX[9] X[10] NotX[11] + X[1] X[2] NotX[3] NotX[7] NotX[9] X[10] NotX[11] + NotX[1] X[3] X[4] X[5] NotX[7] NotX[9] NotX[11] + X[1] X[3] X[5] NotX[7] X[8] NotX[9] NotX[11] + X[1] NotX[4] NotX[5] X[6] X[7] NotX[9] NotX[11] + NotX[1] X[2] NotX[5] X[7] X[8] NotX[9] NotX[11] + NotX[1] X[3] X[4] NotX[5] X[6] NotX[9] NotX[11] + NotX[1] NotX[2] NotX[4] X[5] NotX[9] X[10] NotX[11] + NotX[1] NotX[4] X[5] X[6] X[8] NotX[9] NotX[11] + X[1] NotX[2] NotX[3] X[5] X[7] NotX[9] NotX[11] + X[1] NotX[3] X[4] X[6] X[7] NotX[9] NotX[11] + NotX[1] X[2] NotX[4] NotX[7] NotX[8] X[10] NotX[11] + NotX[1] NotX[3] X[4] NotX[7] NotX[8] X[10] NotX[11] + X[1] X[2] NotX[3] NotX[7] NotX[8] X[9] NotX[11] + X[1] X[2] NotX[7] NotX[8] X[9] X[10] NotX[11] + NotX[1] NotX[2] NotX[6] X[7] NotX[8] X[9] NotX[11] + X[1] NotX[2] X[5] NotX[6] NotX[8] X[9] NotX[11] + NotX[1] X[2] NotX[6] X[7] NotX[8] X[10] NotX[11] + NotX[1] X[3] NotX[4] NotX[5] NotX[8] X[10] NotX[11] + X[1] X[3] NotX[4] NotX[5] NotX[8] X[9] NotX[11] + X[1] X[2] X[4] NotX[5] X[7] NotX[8] NotX[11] + X[1] NotX[2] NotX[5] NotX[6] NotX[7] X[8] NotX[11] + X[1] NotX[2] NotX[3] NotX[5] X[6] NotX[7] NotX[11] + NotX[1] NotX[3] NotX[5] X[6] NotX[7] X[9] NotX[11] + NotX[1] NotX[4] X[5] NotX[7] X[8] X[10] NotX[11] + X[1] NotX[4] X[5] X[6] NotX[7] X[10] NotX[11] + NotX[1] X[2] NotX[3] X[4] NotX[7] X[8] NotX[11] + X[1] NotX[2] X[3] X[6] NotX[7] X[10] NotX[11] + NotX[1] X[3] NotX[5] NotX[6] X[8] X[10] NotX[11] + NotX[1] X[2] NotX[3] NotX[4] NotX[6] X[8] NotX[11] + NotX[1] NotX[3] X[5] NotX[6] X[7] X[10] NotX[11] + X[1] NotX[2] X[3] NotX[6] X[7] X[8] NotX[11] + NotX[1] X[2] X[3] X[5] NotX[6] X[8] NotX[11] + X[1] NotX[3] NotX[7] X[8] NotX[9] NotX[10] NotX[11] + X[1] X[4] X[7] X[8] NotX[9] NotX[10] NotX[11] + NotX[1] X[4] NotX[6] NotX[7] NotX[8] NotX[10] NotX[11] + X[1] X[2] NotX[4] NotX[6] NotX[8] NotX[10] NotX[11] + NotX[1] NotX[3] NotX[5] X[7] NotX[8] NotX[10] NotX[11] + X[1] NotX[2] X[3] NotX[5] NotX[8] NotX[10] NotX[11] + NotX[1] X[2] X[3] NotX[4] NotX[8] NotX[10] NotX[11] + X[1] NotX[2] X[5] X[7] NotX[8] NotX[10] NotX[11] + NotX[1] X[3] X[4] NotX[5] NotX[7] NotX[10] NotX[11] + X[1] NotX[4] X[6] X[7] X[9] NotX[10] NotX[11] + X[1] NotX[2] X[3] X[6] X[8] NotX[10] NotX[11] + NotX[1] X[2] X[4] X[7] X[9] NotX[10] NotX[11] ----------------------------------------------- The largest minimial size of monomials in DNF tautologies with, 12, variables, all of the same size, that is feasible (on density grounds is) , 8 Here is such a distinct DNF tautology with, 12, variales, each of size, 8 X[1] X[2] NotX[3] NotX[7] NotX[9] NotX[10] NotX[11] NotX[12] + X[1] X[4] NotX[5] NotX[6] NotX[9] NotX[10] NotX[11] NotX[12] + X[1] X[2] X[5] X[6] NotX[9] NotX[10] NotX[11] NotX[12] + NotX[1] NotX[4] NotX[6] NotX[8] X[9] NotX[10] NotX[11] NotX[12] + NotX[2] X[3] X[4] NotX[6] NotX[8] NotX[10] NotX[11] NotX[12] + X[1] NotX[2] X[3] NotX[5] NotX[8] NotX[10] NotX[11] NotX[12] + X[1] NotX[4] X[5] NotX[8] X[9] NotX[10] NotX[11] NotX[12] + X[1] NotX[2] X[5] X[6] NotX[8] NotX[10] NotX[11] NotX[12] + X[1] X[6] NotX[7] X[8] X[9] NotX[10] NotX[11] NotX[12] + X[1] NotX[4] NotX[5] NotX[6] X[8] NotX[10] NotX[11] NotX[12] + X[1] X[2] X[5] NotX[6] X[7] NotX[10] NotX[11] NotX[12] + NotX[1] X[3] X[4] X[7] X[9] NotX[10] NotX[11] NotX[12] + X[1] NotX[3] X[4] NotX[8] NotX[9] X[10] NotX[11] NotX[12] + NotX[2] NotX[3] X[4] X[6] NotX[7] NotX[9] NotX[11] NotX[12] + NotX[1] X[2] NotX[3] X[4] NotX[6] NotX[9] NotX[11] NotX[12] + NotX[1] NotX[2] X[3] X[4] NotX[5] NotX[9] NotX[11] NotX[12] + NotX[1] X[2] NotX[5] X[8] NotX[9] X[10] NotX[11] NotX[12] + NotX[2] X[3] NotX[4] X[6] X[8] NotX[9] NotX[11] NotX[12] + NotX[2] NotX[3] X[4] X[6] NotX[7] NotX[8] NotX[11] NotX[12] + NotX[1] NotX[5] NotX[6] NotX[7] X[8] X[9] NotX[11] NotX[12] + X[1] NotX[2] NotX[4] X[6] NotX[7] X[8] NotX[11] NotX[12] + NotX[1] NotX[4] NotX[6] X[7] X[8] X[10] NotX[11] NotX[12] + X[1] X[2] X[4] NotX[5] X[8] X[9] NotX[11] NotX[12] + X[1] X[2] NotX[4] X[6] X[7] X[9] NotX[11] NotX[12] + NotX[1] X[2] NotX[3] X[4] X[7] X[9] NotX[11] NotX[12] + X[1] NotX[3] X[5] X[6] X[7] X[8] NotX[11] NotX[12] + X[1] NotX[2] X[3] X[7] X[8] X[10] NotX[11] NotX[12] + NotX[1] NotX[5] NotX[6] NotX[7] X[8] NotX[9] NotX[10] NotX[12] + X[1] X[3] NotX[4] NotX[6] NotX[7] NotX[9] NotX[10] NotX[12] + X[2] NotX[3] NotX[4] NotX[7] X[8] NotX[9] NotX[10] NotX[12] + X[1] X[2] X[4] NotX[5] X[7] NotX[9] NotX[10] NotX[12] + NotX[1] X[3] X[5] X[6] X[8] NotX[9] NotX[10] NotX[12] + X[1] NotX[3] X[6] NotX[7] NotX[8] X[9] NotX[10] NotX[12] + X[1] X[3] X[4] X[5] NotX[7] NotX[8] NotX[10] NotX[12] + NotX[1] X[3] NotX[5] X[7] NotX[8] NotX[10] X[11] NotX[12] + NotX[1] X[2] X[3] NotX[4] NotX[8] NotX[10] X[11] NotX[12] + NotX[1] NotX[3] X[5] NotX[8] X[9] NotX[10] X[11] NotX[12] + X[1] NotX[2] X[3] NotX[8] X[9] NotX[10] X[11] NotX[12] + X[1] X[2] X[6] X[7] NotX[8] X[9] NotX[10] NotX[12] + X[1] NotX[2] X[3] NotX[6] NotX[7] X[8] NotX[10] NotX[12] + X[1] NotX[3] X[4] X[6] NotX[7] NotX[10] X[11] NotX[12] + X[1] X[2] X[5] NotX[7] X[8] X[9] NotX[10] NotX[12] + X[2] NotX[3] NotX[4] NotX[5] NotX[6] NotX[10] X[11] NotX[12] + X[1] NotX[2] NotX[3] NotX[5] NotX[6] NotX[10] X[11] NotX[12] + NotX[1] X[3] X[4] NotX[6] X[9] NotX[10] X[11] NotX[12] + X[1] X[2] X[4] NotX[6] X[8] NotX[10] X[11] NotX[12] + X[1] X[3] NotX[5] X[6] X[8] NotX[10] X[11] NotX[12] + NotX[1] X[2] NotX[3] NotX[4] X[6] X[8] NotX[10] NotX[12] + X[1] NotX[3] NotX[4] X[5] X[7] NotX[10] X[11] NotX[12] + X[1] X[2] NotX[4] X[5] X[6] NotX[10] X[11] NotX[12] + X[2] X[3] NotX[4] X[5] X[8] NotX[10] X[11] NotX[12] + X[1] NotX[2] X[3] X[7] X[8] X[9] NotX[10] NotX[12] + NotX[1] NotX[2] NotX[5] NotX[7] NotX[8] NotX[9] X[11] NotX[12] + X[1] NotX[2] NotX[3] X[5] NotX[7] NotX[8] NotX[9] NotX[12] + NotX[2] NotX[3] NotX[4] NotX[6] X[7] NotX[8] NotX[9] NotX[12] + X[1] X[4] X[5] NotX[6] NotX[8] NotX[9] X[11] NotX[12] + NotX[1] X[2] X[3] NotX[4] NotX[8] NotX[9] X[10] NotX[12] + X[1] NotX[2] X[3] X[6] NotX[8] NotX[9] X[10] NotX[12] + NotX[1] NotX[4] X[5] NotX[7] X[8] NotX[9] X[10] NotX[12] + NotX[1] NotX[3] X[6] NotX[7] X[8] NotX[9] X[11] NotX[12] + X[2] NotX[3] X[4] X[6] NotX[7] NotX[9] X[10] NotX[12] + NotX[1] NotX[2] X[4] NotX[7] X[8] NotX[9] X[11] NotX[12] + X[1] X[3] X[4] X[5] NotX[7] X[8] NotX[9] NotX[12] + X[1] X[3] NotX[7] X[8] NotX[9] X[10] X[11] NotX[12] + NotX[2] NotX[3] X[4] NotX[5] NotX[6] NotX[9] X[11] NotX[12] + X[1] NotX[2] X[3] NotX[6] X[7] NotX[9] X[11] NotX[12] + X[1] X[2] NotX[4] NotX[5] X[6] X[7] NotX[9] NotX[12] + X[1] NotX[2] NotX[3] NotX[5] X[6] NotX[9] X[11] NotX[12] + X[1] X[2] X[4] NotX[5] X[8] NotX[9] X[10] NotX[12] + X[1] X[3] X[4] NotX[5] X[6] X[8] NotX[9] NotX[12] + X[1] NotX[5] X[7] X[8] NotX[9] X[10] X[11] NotX[12] + X[1] X[2] NotX[4] X[5] X[6] NotX[9] X[10] NotX[12] + X[1] NotX[2] NotX[3] X[5] X[8] NotX[9] X[10] NotX[12] + NotX[2] X[3] X[4] X[6] NotX[9] X[10] X[11] NotX[12] + X[1] NotX[3] X[5] NotX[6] NotX[7] NotX[8] X[9] NotX[12] + X[1] NotX[4] NotX[5] X[6] NotX[7] NotX[8] X[10] NotX[12] + NotX[1] X[2] NotX[3] NotX[4] NotX[6] X[7] NotX[8] NotX[12] + X[1] NotX[3] NotX[4] NotX[6] X[7] NotX[8] X[11] NotX[12] + NotX[1] X[4] X[5] NotX[6] X[7] NotX[8] X[11] NotX[12] + X[1] X[2] X[4] NotX[6] X[7] NotX[8] X[9] NotX[12] + NotX[1] NotX[2] X[3] NotX[4] X[5] NotX[8] X[9] NotX[12] + NotX[2] X[3] NotX[4] X[5] X[6] NotX[8] X[9] NotX[12] + NotX[1] NotX[4] X[6] X[7] NotX[8] X[9] X[10] NotX[12] + NotX[1] X[2] NotX[3] X[4] X[7] NotX[8] X[11] NotX[12] + NotX[1] X[3] X[4] X[6] X[7] NotX[8] X[10] NotX[12] + X[1] X[2] X[4] X[6] X[7] NotX[8] X[10] NotX[12] + X[1] NotX[2] NotX[3] NotX[5] NotX[6] NotX[7] X[10] NotX[12] + X[1] NotX[2] X[3] NotX[6] NotX[7] X[9] X[10] NotX[12] + NotX[1] NotX[3] NotX[4] NotX[5] NotX[7] X[9] X[11] NotX[12] + NotX[1] NotX[2] X[3] NotX[4] NotX[5] NotX[7] X[9] NotX[12] + X[1] NotX[2] NotX[3] X[5] NotX[7] X[9] X[11] NotX[12] + NotX[1] X[2] NotX[3] X[4] NotX[7] X[8] X[9] NotX[12] + NotX[1] NotX[2] X[3] X[4] X[6] NotX[7] X[9] NotX[12] + X[1] NotX[2] X[4] X[6] NotX[7] X[9] X[10] NotX[12] + NotX[1] X[3] X[5] NotX[7] X[8] X[9] X[11] NotX[12] + X[1] X[2] X[5] X[6] NotX[7] X[9] X[10] NotX[12] + X[1] X[2] NotX[4] NotX[5] NotX[6] X[7] X[8] NotX[12] + X[2] X[3] NotX[4] NotX[5] NotX[6] X[7] X[11] NotX[12] + NotX[1] NotX[2] NotX[3] X[4] NotX[5] NotX[6] X[9] NotX[12] + NotX[1] NotX[3] NotX[5] NotX[6] X[7] X[10] X[11] NotX[12] + NotX[1] NotX[3] NotX[4] X[5] NotX[6] X[7] X[8] NotX[12] + NotX[1] NotX[3] NotX[4] X[5] NotX[6] X[9] X[10] NotX[12] + X[1] X[2] NotX[4] X[5] NotX[6] X[8] X[10] NotX[12] + X[1] NotX[3] X[4] X[5] NotX[6] X[8] X[10] NotX[12] + NotX[1] X[2] X[3] X[5] NotX[6] X[8] X[9] NotX[12] + NotX[1] NotX[2] NotX[3] NotX[4] NotX[5] X[6] X[7] NotX[12] + NotX[1] NotX[2] X[3] NotX[4] NotX[5] X[7] X[10] NotX[12] + NotX[1] NotX[2] NotX[3] X[4] NotX[5] X[6] X[10] NotX[12] + X[1] NotX[3] NotX[5] X[6] X[8] X[9] X[11] NotX[12] + X[2] NotX[3] X[4] NotX[5] X[7] X[9] X[11] NotX[12] + NotX[2] X[3] X[4] NotX[5] X[7] X[9] X[10] NotX[12] + NotX[1] X[2] X[3] NotX[5] X[6] X[7] X[8] NotX[12] + NotX[1] NotX[2] NotX[3] NotX[4] X[5] X[6] X[8] NotX[12] + NotX[1] X[2] NotX[3] NotX[4] X[6] X[9] X[10] NotX[12] + X[1] NotX[2] NotX[4] X[8] X[9] X[10] X[11] NotX[12] + NotX[2] X[3] NotX[4] X[5] X[7] X[8] X[10] NotX[12] + NotX[1] X[3] NotX[4] X[5] X[8] X[9] X[10] NotX[12] + NotX[1] NotX[2] NotX[3] X[4] X[5] X[7] X[8] NotX[12] + NotX[1] NotX[3] X[4] X[5] X[7] X[8] X[11] NotX[12] + X[1] NotX[3] X[4] X[5] X[6] X[7] X[11] NotX[12] + NotX[1] X[2] X[3] X[5] X[6] X[8] X[10] NotX[12] + X[1] X[2] X[7] X[8] X[9] X[10] X[11] NotX[12] + NotX[1] X[2] X[3] NotX[4] NotX[8] NotX[9] NotX[10] NotX[11] + X[1] X[2] NotX[4] NotX[7] NotX[9] NotX[10] NotX[11] X[12] + NotX[1] X[3] NotX[4] NotX[6] X[8] NotX[9] NotX[10] NotX[11] + X[1] NotX[2] X[5] NotX[6] X[7] NotX[9] NotX[10] NotX[11] + X[1] X[3] X[5] NotX[6] NotX[9] NotX[10] NotX[11] X[12] + NotX[2] NotX[3] NotX[4] NotX[5] X[7] NotX[9] NotX[10] NotX[11] + X[2] X[3] NotX[4] NotX[5] X[6] NotX[9] NotX[10] NotX[11] + X[1] NotX[2] NotX[3] NotX[5] X[6] NotX[9] NotX[10] NotX[11] + X[1] NotX[2] X[3] NotX[5] NotX[9] NotX[10] NotX[11] X[12] + NotX[1] X[4] NotX[5] X[6] X[8] NotX[9] NotX[10] NotX[11] + NotX[1] X[2] NotX[6] NotX[7] NotX[8] X[9] NotX[10] NotX[11] + NotX[1] X[2] X[4] X[6] NotX[7] NotX[8] NotX[10] NotX[11] + X[1] NotX[2] NotX[3] NotX[6] X[7] NotX[8] NotX[10] NotX[11] + NotX[1] NotX[2] X[5] NotX[6] NotX[8] X[9] NotX[10] NotX[11] + NotX[1] X[2] NotX[4] X[6] NotX[8] X[9] NotX[10] NotX[11] + X[1] X[3] NotX[4] X[7] NotX[8] NotX[10] NotX[11] X[12] + X[2] NotX[3] X[4] X[7] NotX[8] NotX[10] NotX[11] X[12] + X[1] NotX[2] X[6] NotX[8] X[9] NotX[10] NotX[11] X[12] + X[1] X[2] X[4] X[5] NotX[8] NotX[10] NotX[11] X[12] + X[1] NotX[2] NotX[3] NotX[5] NotX[6] NotX[7] NotX[10] NotX[11] + X[1] NotX[2] NotX[3] X[5] NotX[7] X[8] NotX[10] NotX[11] + NotX[1] NotX[3] X[6] NotX[7] X[8] NotX[10] NotX[11] X[12] + NotX[1] NotX[5] NotX[6] X[7] X[9] NotX[10] NotX[11] X[12] + NotX[1] NotX[3] NotX[4] NotX[6] X[7] X[8] NotX[10] NotX[11] + NotX[1] X[2] NotX[3] X[4] NotX[6] NotX[10] NotX[11] X[12] + NotX[1] NotX[2] X[3] NotX[4] NotX[5] X[7] NotX[10] NotX[11] + NotX[1] NotX[2] NotX[3] X[4] NotX[5] X[6] NotX[10] NotX[11] + NotX[1] NotX[2] X[3] X[4] NotX[5] NotX[10] NotX[11] X[12] + NotX[1] NotX[2] X[3] NotX[4] X[5] X[8] NotX[10] NotX[11] + NotX[1] NotX[2] X[5] X[7] X[8] NotX[10] NotX[11] X[12] + NotX[1] X[2] X[3] X[5] X[6] X[8] NotX[10] NotX[11] + X[1] X[4] NotX[5] NotX[7] NotX[8] NotX[9] NotX[11] X[12] + X[2] X[3] NotX[5] X[6] NotX[7] NotX[8] NotX[9] NotX[11] + X[1] X[4] X[5] NotX[7] NotX[8] NotX[9] X[10] NotX[11] + X[2] X[3] X[4] NotX[6] X[7] NotX[8] NotX[9] NotX[11] + NotX[1] X[2] NotX[3] NotX[4] X[6] NotX[8] NotX[9] NotX[11] + X[2] NotX[3] NotX[4] X[7] NotX[8] NotX[9] NotX[11] X[12] + X[2] X[3] NotX[4] NotX[8] NotX[9] X[10] NotX[11] X[12] + NotX[1] X[2] X[4] X[6] X[7] NotX[8] NotX[9] NotX[11] + X[1] NotX[2] X[3] NotX[6] NotX[7] NotX[9] X[10] NotX[11] + NotX[1] NotX[2] X[3] NotX[4] NotX[5] NotX[7] NotX[9] NotX[11] + NotX[1] NotX[2] NotX[3] X[4] NotX[5] NotX[6] NotX[9] NotX[11] + NotX[1] X[3] X[4] X[5] NotX[6] X[7] NotX[9] NotX[11] + X[1] NotX[2] NotX[3] NotX[5] X[7] NotX[9] X[10] NotX[11] + NotX[1] NotX[2] NotX[5] X[7] NotX[9] X[10] NotX[11] X[12] + X[1] X[2] X[4] NotX[5] X[7] NotX[9] NotX[11] X[12] + X[1] NotX[3] NotX[4] X[6] X[7] NotX[9] NotX[11] X[12] + X[2] NotX[3] NotX[4] X[6] X[8] NotX[9] X[10] NotX[11] + NotX[1] NotX[2] X[3] NotX[4] X[5] NotX[9] X[10] NotX[11] + NotX[1] X[2] X[3] NotX[4] NotX[9] X[10] NotX[11] X[12] + X[1] X[3] NotX[4] X[6] X[8] NotX[9] NotX[11] X[12] + NotX[1] NotX[3] X[4] X[5] X[6] X[8] NotX[9] NotX[11] + X[1] NotX[3] X[4] X[7] X[8] NotX[9] NotX[11] X[12] + NotX[1] X[4] X[7] X[8] NotX[9] X[10] NotX[11] X[12] + X[1] X[2] X[4] NotX[5] NotX[7] NotX[8] X[9] NotX[11] + NotX[1] X[3] X[4] NotX[7] NotX[8] X[9] X[10] NotX[11] + X[1] X[2] NotX[4] NotX[5] NotX[6] X[7] NotX[8] NotX[11] + X[1] X[2] NotX[4] X[5] NotX[6] NotX[8] X[9] NotX[11] + X[1] NotX[2] X[5] NotX[6] X[7] NotX[8] X[10] NotX[11] + X[2] NotX[3] NotX[4] NotX[5] X[7] NotX[8] NotX[11] X[12] + X[1] X[3] NotX[5] X[7] NotX[8] X[9] X[10] NotX[11] + NotX[1] NotX[2] NotX[3] NotX[4] X[5] X[6] NotX[8] NotX[11] + X[1] X[2] NotX[4] X[5] X[6] NotX[8] NotX[11] X[12] + NotX[1] NotX[2] NotX[3] X[4] X[5] X[7] NotX[8] NotX[11] + X[1] NotX[2] NotX[3] X[5] NotX[8] X[9] X[10] NotX[11] + X[1] NotX[2] X[3] X[6] NotX[8] X[10] NotX[11] X[12] + NotX[2] X[3] X[4] X[5] X[7] NotX[8] X[9] NotX[11] + X[1] X[2] X[4] X[7] NotX[8] X[10] NotX[11] X[12] + NotX[1] NotX[4] NotX[5] NotX[6] NotX[7] X[9] X[10] NotX[11] + NotX[1] NotX[2] NotX[5] NotX[6] NotX[7] X[9] NotX[11] X[12] + NotX[1] X[3] X[4] X[5] NotX[6] NotX[7] X[8] NotX[11] + X[1] X[5] NotX[6] NotX[7] X[8] X[9] X[10] NotX[11] + NotX[1] NotX[2] NotX[3] NotX[4] NotX[5] X[6] NotX[7] NotX[11] + X[1] X[2] NotX[4] NotX[5] X[6] NotX[7] X[9] NotX[11] + X[1] NotX[2] NotX[3] NotX[5] NotX[7] X[10] NotX[11] X[12] + X[2] NotX[3] X[4] NotX[5] NotX[7] X[10] NotX[11] X[12] + NotX[1] X[2] X[3] NotX[5] X[6] NotX[7] X[9] NotX[11] + NotX[1] X[4] NotX[5] X[6] NotX[7] X[10] NotX[11] X[12] + X[2] NotX[3] X[4] X[5] X[6] NotX[7] X[8] NotX[11] + NotX[2] NotX[3] X[4] X[5] NotX[6] X[8] X[10] NotX[11] + X[1] NotX[3] X[5] NotX[6] X[7] X[8] X[9] NotX[11] + X[1] NotX[2] X[3] NotX[6] X[8] X[9] NotX[11] X[12] + X[1] X[2] X[4] NotX[6] X[8] X[9] NotX[11] X[12] + X[2] X[3] X[4] X[5] NotX[6] X[7] X[10] NotX[11] + X[2] NotX[3] NotX[4] NotX[5] X[8] X[9] NotX[11] X[12] + NotX[1] X[3] NotX[4] NotX[5] X[9] X[10] NotX[11] X[12] + X[1] X[2] NotX[4] NotX[5] X[7] X[8] NotX[11] X[12] + X[1] NotX[2] NotX[3] NotX[5] X[7] X[8] X[9] NotX[11] + NotX[1] NotX[3] NotX[5] X[6] X[7] X[9] NotX[11] X[12] + NotX[1] X[2] NotX[3] NotX[4] X[6] X[8] NotX[11] X[12] + X[1] NotX[2] X[5] X[6] X[8] X[9] NotX[11] X[12] + NotX[1] X[3] X[4] X[5] X[6] X[8] X[10] NotX[11] + X[1] X[2] X[6] X[7] X[8] X[9] NotX[11] X[12] + X[1] X[3] X[4] X[6] X[8] X[10] NotX[11] X[12] + NotX[1] X[3] X[4] NotX[6] NotX[7] NotX[8] NotX[9] NotX[10] + NotX[2] NotX[3] X[4] NotX[5] X[7] NotX[8] NotX[9] NotX[10] + NotX[1] X[3] X[4] NotX[5] NotX[8] NotX[9] NotX[10] X[11] + NotX[1] NotX[2] X[3] NotX[4] X[5] NotX[8] NotX[9] NotX[10] + NotX[2] X[3] NotX[4] X[6] NotX[8] NotX[9] NotX[10] X[12] + X[1] NotX[2] X[3] X[6] NotX[8] NotX[9] NotX[10] X[11] + NotX[1] X[3] X[4] X[5] X[6] NotX[8] NotX[9] NotX[10] + X[1] NotX[4] NotX[5] NotX[7] NotX[9] NotX[10] X[11] X[12] + NotX[1] X[2] NotX[3] X[4] NotX[7] NotX[9] NotX[10] X[11] + X[1] NotX[2] X[5] NotX[7] X[8] NotX[9] NotX[10] X[11] + NotX[1] X[3] X[4] NotX[7] X[8] NotX[9] NotX[10] X[12] + NotX[1] NotX[4] NotX[5] X[6] X[8] NotX[9] NotX[10] X[12] + X[1] NotX[5] X[6] X[8] NotX[9] NotX[10] X[11] X[12] + X[1] NotX[2] X[5] X[6] X[7] X[8] NotX[9] NotX[10] + X[1] X[2] X[4] NotX[5] NotX[7] NotX[8] NotX[10] X[11] + X[1] NotX[2] NotX[3] X[5] NotX[7] NotX[8] NotX[10] X[12] + NotX[2] X[3] X[4] NotX[7] NotX[8] X[9] NotX[10] X[11] + NotX[1] X[2] X[4] NotX[7] NotX[8] X[9] NotX[10] X[11] + NotX[1] X[3] X[4] NotX[5] NotX[6] X[7] NotX[8] NotX[10] + X[1] X[2] NotX[4] X[5] NotX[6] NotX[8] NotX[10] X[11] + NotX[1] X[2] NotX[3] NotX[4] X[6] NotX[8] NotX[10] X[11] + NotX[1] X[3] NotX[4] X[6] NotX[8] X[9] NotX[10] X[12] + X[1] NotX[2] NotX[3] X[6] X[7] NotX[8] X[9] NotX[10] + X[1] X[3] X[4] X[5] NotX[8] NotX[10] X[11] X[12] + X[1] NotX[4] NotX[5] NotX[6] NotX[7] X[8] NotX[10] X[11] + X[2] X[3] NotX[4] NotX[5] NotX[6] NotX[7] NotX[10] X[12] + NotX[1] X[2] NotX[3] NotX[4] NotX[6] NotX[7] X[8] NotX[10] + X[2] NotX[3] X[4] NotX[6] NotX[7] X[9] NotX[10] X[11] + NotX[1] NotX[2] NotX[6] NotX[7] X[9] NotX[10] X[11] X[12] + X[1] X[2] NotX[4] NotX[5] X[6] NotX[7] NotX[10] X[11] + X[1] X[2] X[4] NotX[5] NotX[7] X[8] NotX[10] X[12] + NotX[2] X[3] NotX[4] X[6] NotX[7] X[8] X[9] NotX[10] + NotX[1] NotX[2] NotX[3] X[4] X[5] NotX[7] X[8] NotX[10] + NotX[1] NotX[2] X[6] NotX[7] X[8] NotX[10] X[11] X[12] + NotX[1] X[4] X[5] X[6] NotX[7] X[9] NotX[10] X[12] + X[1] X[3] X[4] X[5] X[6] NotX[7] NotX[10] X[12] + NotX[1] NotX[2] NotX[3] NotX[4] NotX[5] NotX[6] X[7] NotX[10] + NotX[1] X[2] X[3] NotX[5] NotX[6] X[7] X[8] NotX[10] + NotX[1] NotX[2] NotX[3] NotX[4] X[5] NotX[6] X[8] NotX[10] + NotX[2] NotX[3] NotX[4] NotX[6] X[7] X[8] NotX[10] X[12] + X[1] NotX[4] NotX[6] X[7] X[9] NotX[10] X[11] X[12] + X[1] NotX[3] X[4] X[5] NotX[6] X[7] NotX[10] X[11] + X[1] NotX[2] X[3] NotX[6] X[7] NotX[10] X[11] X[12] + NotX[1] X[2] X[3] X[5] NotX[6] X[9] NotX[10] X[12] + NotX[1] X[3] NotX[6] X[7] X[9] NotX[10] X[11] X[12] + NotX[1] NotX[3] X[4] NotX[5] X[6] X[9] NotX[10] X[11] + X[1] X[2] X[4] NotX[5] X[7] NotX[10] X[11] X[12] + X[1] X[3] NotX[5] X[6] X[7] X[9] NotX[10] X[12] + X[2] NotX[3] NotX[4] X[5] X[9] NotX[10] X[11] X[12] + NotX[1] NotX[2] X[3] NotX[4] X[7] X[8] NotX[10] X[11] + X[1] X[2] NotX[4] X[6] X[7] NotX[10] X[11] X[12] + NotX[1] X[2] NotX[3] X[4] X[7] NotX[10] X[11] X[12] + X[1] NotX[3] X[4] X[5] X[6] NotX[10] X[11] X[12] + NotX[1] NotX[2] X[3] X[4] X[6] X[7] NotX[10] X[11] + X[2] X[3] X[4] X[6] X[7] X[8] NotX[10] X[11] + X[1] NotX[4] NotX[5] NotX[6] NotX[7] NotX[8] NotX[9] X[10] + NotX[1] X[2] NotX[3] NotX[4] NotX[6] NotX[7] NotX[8] NotX[9] + X[1] NotX[2] X[3] NotX[6] NotX[7] NotX[8] NotX[9] X[11] + X[1] X[2] X[4] NotX[5] NotX[7] NotX[8] NotX[9] X[10] + NotX[1] NotX[4] X[5] X[6] NotX[7] NotX[8] NotX[9] X[11] + NotX[1] NotX[2] NotX[3] X[4] X[5] NotX[7] NotX[8] NotX[9] + NotX[1] X[2] X[4] X[6] NotX[7] NotX[8] NotX[9] X[10] + NotX[1] X[3] X[4] X[5] NotX[7] NotX[8] NotX[9] X[10] + X[1] X[3] NotX[5] NotX[6] X[7] NotX[8] NotX[9] X[10] + NotX[1] NotX[2] NotX[3] NotX[4] X[5] NotX[6] NotX[8] NotX[9] + NotX[1] NotX[3] NotX[4] NotX[6] X[7] NotX[8] NotX[9] X[12] + X[1] X[2] NotX[4] X[5] NotX[6] NotX[8] NotX[9] X[10] + NotX[1] X[3] X[5] NotX[6] NotX[8] NotX[9] X[10] X[11] + X[2] X[3] X[5] NotX[6] X[7] NotX[8] NotX[9] X[12] + NotX[1] X[2] X[3] NotX[4] NotX[8] NotX[9] X[11] X[12] + X[1] NotX[2] NotX[3] X[7] NotX[8] NotX[9] X[11] X[12] + NotX[1] NotX[2] X[5] X[6] X[7] NotX[8] NotX[9] X[11] + NotX[2] X[3] X[4] X[5] X[7] NotX[8] NotX[9] X[12] + X[2] X[3] X[4] X[5] X[6] NotX[8] NotX[9] X[11] + NotX[1] NotX[2] NotX[3] NotX[4] NotX[5] NotX[6] NotX[7] NotX[9] + NotX[1] X[3] X[4] NotX[5] NotX[6] NotX[7] NotX[9] X[10] + NotX[1] NotX[3] X[4] NotX[6] NotX[7] NotX[9] X[10] X[11] + X[1] X[4] X[5] NotX[6] NotX[7] NotX[9] X[11] X[12] + X[1] X[2] NotX[4] NotX[5] X[6] NotX[7] NotX[9] X[10] + NotX[1] NotX[2] X[3] NotX[4] NotX[7] X[8] NotX[9] X[11] + X[1] NotX[2] NotX[3] X[5] NotX[7] NotX[9] X[10] X[12] + X[1] X[2] X[4] NotX[7] X[8] NotX[9] X[10] X[12] + NotX[1] X[2] NotX[3] NotX[4] NotX[6] X[8] NotX[9] X[10] + NotX[1] NotX[4] NotX[6] X[7] X[8] NotX[9] X[11] X[12] + X[1] X[2] NotX[4] X[5] NotX[6] X[8] NotX[9] X[12] + NotX[1] NotX[2] X[3] X[4] NotX[6] X[7] NotX[9] X[11] + NotX[1] X[2] X[3] X[5] NotX[6] X[8] NotX[9] X[11] + X[1] X[2] X[4] NotX[6] X[7] NotX[9] X[10] X[11] + X[2] X[3] NotX[4] NotX[5] X[8] NotX[9] X[10] X[11] + NotX[1] NotX[3] X[4] NotX[5] X[7] X[8] NotX[9] X[11] + NotX[1] X[3] X[4] NotX[5] X[7] NotX[9] X[10] X[11] + NotX[1] X[2] NotX[3] NotX[4] X[6] NotX[9] X[10] X[11] + X[1] X[2] NotX[4] X[5] X[6] NotX[9] X[11] X[12] + NotX[2] NotX[3] X[4] X[5] X[6] X[7] NotX[9] X[12] + NotX[1] X[2] NotX[3] X[4] X[7] NotX[9] X[10] X[12] + X[1] NotX[3] X[6] X[8] NotX[9] X[10] X[11] X[12] + X[1] NotX[2] X[3] X[6] NotX[9] X[10] X[11] X[12] + X[1] X[2] X[4] X[6] NotX[9] X[10] X[11] X[12] + X[1] X[2] NotX[4] NotX[5] NotX[6] NotX[7] NotX[8] X[9] + NotX[1] NotX[2] X[3] X[4] NotX[6] NotX[7] NotX[8] X[11] + X[1] NotX[2] X[3] NotX[6] NotX[7] NotX[8] X[9] X[12] + X[1] NotX[2] NotX[5] X[6] NotX[7] NotX[8] X[11] X[12] + NotX[1] X[2] NotX[3] X[4] NotX[7] NotX[8] X[9] X[10] + X[1] NotX[3] X[5] NotX[7] NotX[8] X[9] X[10] X[12] + NotX[1] X[3] X[6] NotX[7] NotX[8] X[9] X[10] X[11] + X[2] X[3] X[5] X[6] NotX[7] NotX[8] X[9] X[10] + X[1] X[4] NotX[5] NotX[6] X[7] NotX[8] X[9] X[12] + NotX[1] X[2] NotX[3] NotX[4] NotX[6] NotX[8] X[9] X[12] + X[2] NotX[3] X[4] X[5] NotX[6] NotX[8] X[10] X[12] + NotX[1] X[2] X[3] X[5] NotX[6] NotX[8] X[9] X[10] + NotX[1] NotX[2] X[3] NotX[4] NotX[5] NotX[8] X[11] X[12] + X[1] NotX[2] NotX[3] NotX[5] X[7] NotX[8] X[9] X[10] + X[1] NotX[5] X[6] X[7] NotX[8] X[10] X[11] X[12] + NotX[1] NotX[2] NotX[3] NotX[4] X[5] NotX[8] X[9] X[11] + NotX[2] NotX[3] NotX[4] X[5] X[6] X[7] NotX[8] X[10] + NotX[1] X[2] NotX[4] X[6] NotX[8] X[9] X[10] X[12] + X[1] X[2] NotX[4] X[5] NotX[8] X[9] X[10] X[11] + NotX[2] NotX[3] X[4] X[5] X[7] NotX[8] X[10] X[11] + X[1] NotX[2] X[3] X[7] NotX[8] X[9] X[10] X[11] + NotX[1] X[3] X[4] X[5] X[6] X[7] NotX[8] X[9] + X[1] X[2] NotX[4] NotX[5] NotX[6] NotX[7] X[8] X[10] + X[1] NotX[2] NotX[3] NotX[5] NotX[6] NotX[7] X[11] X[12] + NotX[1] X[2] X[3] NotX[5] NotX[6] NotX[7] X[8] X[9] + NotX[1] X[3] NotX[5] NotX[6] NotX[7] X[9] X[10] X[11] + X[2] NotX[3] X[4] X[5] NotX[6] NotX[7] X[8] X[12] + X[1] NotX[2] X[3] NotX[6] NotX[7] X[8] X[11] X[12] + X[2] X[3] X[4] X[5] NotX[6] NotX[7] X[9] X[10] + NotX[1] NotX[2] NotX[3] X[4] NotX[5] NotX[7] X[11] X[12] + X[1] NotX[2] NotX[5] X[6] NotX[7] X[8] X[9] X[12] + NotX[1] X[2] X[3] NotX[5] X[6] NotX[7] X[8] X[11] + X[1] X[2] X[4] NotX[5] NotX[7] X[9] X[10] X[11] + X[1] X[2] NotX[4] X[5] NotX[7] X[8] X[9] X[12] + NotX[1] NotX[2] NotX[3] X[4] X[5] NotX[7] X[9] X[10] + NotX[1] X[2] NotX[3] X[4] NotX[7] X[8] X[10] X[12] + NotX[1] NotX[2] X[3] X[4] X[6] NotX[7] X[10] X[12] + NotX[2] X[3] X[4] X[5] X[6] NotX[7] X[9] X[11] + NotX[1] X[4] X[5] NotX[7] X[8] X[10] X[11] X[12] + NotX[1] NotX[2] NotX[3] NotX[4] NotX[5] NotX[6] X[9] X[10] + X[1] X[2] NotX[4] NotX[5] NotX[6] X[7] X[11] X[12] + NotX[1] X[2] X[3] NotX[5] NotX[6] X[7] X[9] X[10] + X[1] X[3] NotX[5] NotX[6] X[7] X[8] X[10] X[12] + NotX[2] NotX[3] NotX[4] X[5] NotX[6] X[9] X[10] X[12] + NotX[2] X[3] NotX[4] NotX[6] X[7] X[10] X[11] X[12] + X[2] X[3] NotX[4] X[5] NotX[6] X[7] X[8] X[9] + NotX[1] NotX[2] NotX[3] X[4] NotX[6] X[7] X[11] X[12] + NotX[1] NotX[2] X[3] X[4] NotX[6] X[7] X[9] X[10] + X[1] NotX[2] X[5] NotX[6] X[7] X[8] X[10] X[12] + NotX[1] X[2] X[5] NotX[6] X[8] X[9] X[10] X[12] + X[1] X[4] NotX[6] X[7] X[8] X[9] X[10] X[11] + X[2] X[3] X[4] X[5] NotX[6] X[8] X[11] X[12] + NotX[1] NotX[2] NotX[3] NotX[4] NotX[5] X[6] X[11] X[12] + NotX[1] NotX[3] NotX[4] NotX[5] X[8] X[9] X[11] X[12] + NotX[2] X[3] NotX[4] NotX[5] X[6] X[8] X[9] X[10] + NotX[1] X[3] NotX[4] NotX[5] X[7] X[8] X[10] X[11] + X[1] X[2] NotX[4] NotX[5] X[6] X[9] X[10] X[11] + X[1] NotX[2] NotX[3] NotX[5] X[7] X[8] X[11] X[12] + NotX[1] NotX[3] X[4] NotX[5] X[7] X[9] X[10] X[12] + NotX[1] NotX[2] X[4] NotX[5] X[6] X[7] X[10] X[12] + NotX[1] X[2] X[3] NotX[5] X[6] X[7] X[9] X[12] + NotX[1] NotX[2] NotX[3] NotX[4] X[5] X[8] X[10] X[12] + NotX[1] NotX[3] NotX[4] X[5] X[6] X[8] X[11] X[12] + NotX[1] NotX[2] X[3] NotX[4] X[5] X[9] X[10] X[12] + X[1] X[3] NotX[4] X[5] X[6] X[9] X[11] X[12] + X[2] X[3] NotX[4] X[5] X[8] X[9] X[10] X[12] + X[1] NotX[2] NotX[3] X[5] X[8] X[9] X[11] X[12] + NotX[1] NotX[3] X[4] X[5] X[6] X[7] X[9] X[12] + X[1] NotX[3] X[5] X[7] X[9] X[10] X[11] X[12] + X[2] NotX[3] X[4] X[7] X[9] X[10] X[11] X[12] + NotX[1] X[2] X[3] X[5] X[6] X[8] X[11] X[12] + NotX[1] X[3] X[5] X[6] X[7] X[8] X[10] X[11] + X[1] X[2] X[3] X[4] X[5] X[6] X[7] X[8] + X[1] X[2] X[4] X[5] X[9] X[10] X[11] X[12] + X[1] X[3] X[4] X[6] X[7] X[8] X[9] X[11] ----------------------------------------------- The largest minimial size of monomials in DNF tautologies with, 13, variables, all of the same size, that is feasible (on density grounds is) , 9 We were only able to cover, 8090, truth-vectors out of the total of, 8192, here is such an almost-tautology that is distinct X[2] NotX[3] X[4] NotX[5] X[7] X[9] X[11] X[12] X[13] + X[1] X[3] X[4] NotX[5] X[6] X[7] X[9] X[11] X[13] + NotX[2] NotX[3] NotX[4] X[5] X[8] X[9] X[10] X[12] X[13] + NotX[1] X[2] NotX[3] NotX[4] X[6] X[9] X[10] X[12] X[13] + NotX[2] X[3] NotX[4] X[5] X[6] X[8] X[9] X[10] X[12] + NotX[1] X[3] NotX[4] X[8] X[9] X[10] X[11] X[12] X[13] + NotX[2] NotX[3] X[5] X[6] X[7] X[8] X[9] X[11] X[13] + NotX[1] NotX[3] X[4] X[6] X[8] X[9] X[11] X[12] X[13] + X[2] NotX[3] X[4] X[5] X[7] X[9] X[10] X[11] X[13] + NotX[1] NotX[2] X[3] X[4] X[6] X[7] X[9] X[12] X[13] + X[1] NotX[2] X[4] X[5] X[7] X[9] X[10] X[11] X[12] + NotX[1] X[2] X[3] X[6] X[7] X[8] X[9] X[10] X[13] + X[1] X[2] X[3] X[4] X[5] X[6] X[7] X[8] X[9] + X[1] X[2] X[5] X[7] X[8] X[10] X[11] X[12] X[13] + NotX[1] NotX[2] X[3] X[4] NotX[6] NotX[7] X[8] X[10] X[11] + X[1] X[2] NotX[4] NotX[5] NotX[7] X[8] X[9] X[12] X[13] + X[2] NotX[3] X[4] NotX[5] NotX[7] X[8] X[9] X[11] X[12] + NotX[1] X[3] NotX[5] X[6] NotX[7] X[9] X[10] X[11] X[13] + X[1] X[3] X[4] NotX[5] NotX[7] X[8] X[9] X[10] X[13] + NotX[1] NotX[2] NotX[3] NotX[4] X[5] NotX[7] X[8] X[12] X[13] + NotX[1] NotX[2] NotX[3] X[4] X[5] NotX[7] X[8] X[10] X[11] + X[1] NotX[2] X[4] X[5] X[6] NotX[7] X[10] X[11] X[13] + NotX[2] X[3] X[5] NotX[7] X[8] X[9] X[10] X[11] X[13] + NotX[1] X[2] X[3] X[5] NotX[7] X[8] X[10] X[11] X[13] + X[1] X[2] X[5] NotX[7] X[8] X[9] X[10] X[12] X[13] + NotX[1] NotX[2] NotX[3] NotX[4] NotX[5] NotX[6] X[7] X[12] X[13] + NotX[2] X[3] NotX[4] NotX[5] NotX[6] X[7] X[8] X[12] X[13] + NotX[2] NotX[3] NotX[5] NotX[6] X[7] X[9] X[10] X[11] X[12] + NotX[1] NotX[3] X[4] NotX[5] NotX[6] X[8] X[9] X[11] X[13] + NotX[1] X[2] X[3] NotX[5] NotX[6] X[7] X[10] X[11] X[12] + X[1] X[3] X[4] NotX[5] NotX[6] X[7] X[8] X[12] X[13] + NotX[1] X[2] NotX[3] NotX[4] NotX[6] X[8] X[9] X[12] X[13] + X[1] NotX[2] NotX[4] X[5] NotX[6] X[7] X[9] X[11] X[12] + NotX[1] NotX[2] NotX[3] X[5] NotX[6] X[7] X[8] X[11] X[13] + NotX[1] NotX[2] X[3] X[4] NotX[6] X[7] X[8] X[10] X[13] + NotX[1] NotX[2] NotX[3] NotX[4] NotX[5] X[6] X[9] X[11] X[13] + X[1] NotX[2] NotX[4] NotX[5] X[6] X[8] X[9] X[10] X[11] + X[1] X[2] NotX[4] NotX[5] X[7] X[8] X[11] X[12] X[13] + NotX[1] NotX[2] NotX[3] X[4] NotX[5] X[6] X[10] X[11] X[13] + X[1] NotX[3] X[4] NotX[5] X[6] X[8] X[9] X[10] X[13] + X[2] X[3] NotX[4] X[5] NotX[7] NotX[8] X[10] X[11] X[13] + NotX[1] X[2] NotX[3] X[4] NotX[7] NotX[8] X[9] X[12] X[13] + X[1] X[2] X[4] NotX[7] NotX[8] X[9] X[10] X[12] X[13] + NotX[2] NotX[4] NotX[5] NotX[6] X[7] NotX[8] X[9] X[11] X[12] + X[1] X[2] NotX[4] NotX[5] NotX[6] NotX[8] X[10] X[12] X[13] + X[1] X[3] X[4] NotX[5] NotX[6] X[7] NotX[8] X[10] X[11] + NotX[1] NotX[2] NotX[3] NotX[4] X[5] NotX[6] NotX[8] X[12] X[13] + NotX[1] X[2] NotX[3] NotX[6] X[7] NotX[8] X[10] X[11] X[12] + NotX[1] NotX[2] X[3] X[4] NotX[6] X[7] NotX[8] X[9] X[12] + NotX[1] X[2] X[3] X[5] NotX[6] NotX[8] X[10] X[11] X[12] + X[1] X[2] X[5] NotX[6] X[7] NotX[8] X[10] X[11] X[12] + NotX[2] X[3] NotX[4] NotX[5] X[6] NotX[8] X[9] X[11] X[12] + X[1] NotX[2] NotX[3] NotX[5] NotX[8] X[9] X[10] X[11] X[12] + NotX[1] X[2] X[3] NotX[5] X[6] NotX[8] X[9] X[10] X[13] + NotX[1] NotX[2] NotX[3] NotX[4] X[5] X[6] NotX[8] X[10] X[11] + NotX[1] NotX[2] X[3] NotX[4] X[5] NotX[8] X[9] X[11] X[13] + X[1] X[2] NotX[4] X[6] X[7] NotX[8] X[10] X[11] X[12] + NotX[1] NotX[2] NotX[3] X[4] X[5] X[7] NotX[8] X[11] X[13] + NotX[2] NotX[3] X[4] X[5] NotX[8] X[9] X[11] X[12] X[13] + NotX[2] X[5] X[6] X[7] NotX[8] X[10] X[11] X[12] X[13] + NotX[1] X[3] X[4] X[5] X[6] NotX[8] X[10] X[11] X[13] + X[2] X[3] X[6] X[7] NotX[8] X[9] X[10] X[11] X[12] + NotX[1] NotX[2] NotX[3] NotX[4] NotX[5] NotX[6] NotX[7] X[10] X[11] + NotX[1] X[2] X[3] NotX[5] NotX[6] NotX[7] X[8] X[12] X[13] + NotX[2] X[3] NotX[4] NotX[6] NotX[7] X[8] X[9] X[10] X[11] + X[1] NotX[2] NotX[3] NotX[6] NotX[7] X[8] X[9] X[10] X[12] + NotX[1] NotX[2] NotX[3] X[4] NotX[5] NotX[6] NotX[9] X[12] X[13] + NotX[3] X[4] NotX[5] NotX[6] X[7] X[8] NotX[9] X[10] X[12] + NotX[1] X[2] NotX[3] NotX[4] NotX[6] X[8] NotX[9] X[10] X[11] + NotX[2] X[3] X[4] NotX[6] X[7] NotX[9] X[10] X[11] X[12] + X[1] X[3] X[5] NotX[6] X[7] NotX[9] X[11] X[12] X[13] + NotX[1] NotX[2] NotX[3] NotX[4] NotX[5] X[6] NotX[9] X[10] X[12] + NotX[1] NotX[4] NotX[5] X[7] X[8] NotX[9] X[10] X[11] X[13] + X[2] NotX[3] X[4] NotX[5] X[6] NotX[9] X[10] X[12] X[13] + NotX[1] X[2] X[3] NotX[5] X[6] NotX[9] X[10] X[11] X[12] + NotX[1] X[3] NotX[5] X[6] X[7] NotX[9] X[10] X[12] X[13] + NotX[2] X[3] NotX[4] X[8] NotX[9] X[10] X[11] X[12] X[13] + NotX[1] NotX[4] X[5] X[6] NotX[9] X[10] X[11] X[12] X[13] + X[1] NotX[2] NotX[3] X[7] NotX[9] X[10] X[11] X[12] X[13] + NotX[1] X[2] NotX[3] X[4] X[8] NotX[9] X[10] X[11] X[12] + NotX[1] NotX[2] X[4] X[5] X[6] X[7] X[8] NotX[9] X[11] + NotX[1] X[2] X[3] X[5] X[7] X[8] NotX[9] X[11] X[12] + X[1] X[3] X[4] X[6] X[7] NotX[9] X[11] X[12] X[13] + NotX[2] X[3] NotX[4] NotX[5] NotX[6] NotX[7] NotX[8] X[9] X[10] + NotX[1] X[2] X[3] NotX[5] NotX[6] NotX[7] NotX[8] X[9] X[11] + NotX[1] X[2] NotX[3] NotX[4] NotX[6] NotX[7] NotX[8] X[12] X[13] + X[1] NotX[3] X[5] NotX[6] NotX[7] NotX[8] X[9] X[11] X[13] + NotX[1] NotX[2] X[3] X[4] NotX[6] NotX[7] NotX[8] X[9] X[10] + NotX[2] X[4] X[5] NotX[6] NotX[7] NotX[8] X[10] X[11] X[12] + X[1] X[3] NotX[6] NotX[7] NotX[8] X[9] X[11] X[12] X[13] + X[1] NotX[2] NotX[4] X[5] X[6] NotX[7] NotX[8] X[11] X[13] + X[1] X[2] NotX[4] X[6] NotX[7] NotX[8] X[9] X[11] X[13] + X[1] NotX[4] X[5] X[6] X[7] NotX[10] X[11] X[12] X[13] + NotX[1] X[2] NotX[3] X[4] X[7] NotX[10] X[11] X[12] X[13] + X[1] NotX[3] X[4] X[5] X[6] X[9] NotX[10] X[11] X[13] + X[1] NotX[2] X[4] X[5] X[6] X[7] NotX[10] X[12] X[13] + NotX[1] X[3] X[5] X[6] X[7] X[8] X[9] NotX[10] X[12] + NotX[1] X[2] X[3] NotX[5] NotX[6] NotX[7] NotX[8] NotX[9] X[10] + X[1] NotX[2] NotX[4] X[5] NotX[6] NotX[7] NotX[8] NotX[9] X[12] + NotX[3] X[5] NotX[6] NotX[7] NotX[8] NotX[9] X[10] X[11] X[13] + NotX[2] X[3] NotX[5] NotX[7] NotX[8] NotX[9] X[10] X[12] X[13] + NotX[1] NotX[2] NotX[3] X[4] X[5] NotX[7] NotX[8] NotX[9] X[12] + NotX[1] X[2] NotX[3] X[4] NotX[7] NotX[8] NotX[9] X[10] X[13] + X[1] X[3] X[4] NotX[7] NotX[8] NotX[9] X[10] X[11] X[12] + NotX[2] X[3] NotX[4] NotX[5] NotX[6] X[7] NotX[8] NotX[9] X[13] + NotX[3] X[4] NotX[5] NotX[6] X[7] NotX[8] NotX[9] X[10] X[11] + X[1] X[3] NotX[4] NotX[5] X[6] NotX[8] NotX[9] X[10] X[11] + X[2] NotX[3] NotX[5] NotX[8] NotX[9] X[10] X[11] X[12] X[13] + NotX[1] NotX[2] X[3] NotX[4] X[5] NotX[8] NotX[9] X[10] X[11] + X[1] NotX[3] X[5] X[6] NotX[8] NotX[9] X[10] X[12] X[13] + X[1] X[3] NotX[5] NotX[6] NotX[7] X[8] NotX[9] X[11] X[12] + X[2] NotX[3] NotX[4] NotX[5] NotX[7] X[8] NotX[9] X[10] X[12] + NotX[1] NotX[2] X[3] NotX[4] NotX[5] NotX[7] NotX[9] X[10] X[13] + X[1] NotX[2] NotX[3] NotX[5] NotX[7] NotX[9] X[11] X[12] X[13] + X[1] X[3] X[4] NotX[5] X[6] NotX[7] X[8] NotX[9] X[11] + NotX[1] NotX[2] X[3] X[4] X[6] NotX[7] NotX[9] X[10] X[11] + X[1] NotX[2] X[5] NotX[7] X[8] NotX[9] X[11] X[12] X[13] + X[1] X[2] X[5] NotX[7] X[8] NotX[9] X[10] X[11] X[13] + NotX[1] X[2] X[3] X[5] NotX[8] X[9] NotX[10] X[11] X[13] + NotX[2] NotX[4] NotX[5] NotX[6] NotX[7] X[8] NotX[10] X[11] X[13] + X[1] X[3] X[4] NotX[5] NotX[6] NotX[7] X[8] X[9] NotX[10] + X[1] NotX[2] X[4] X[5] NotX[6] NotX[7] X[9] NotX[10] X[11] + NotX[1] NotX[2] X[3] NotX[4] NotX[5] NotX[7] X[9] NotX[10] X[11] + NotX[1] X[2] X[3] NotX[5] X[6] NotX[7] X[9] NotX[10] X[13] + X[1] X[3] X[4] NotX[5] X[6] NotX[7] X[9] NotX[10] X[11] + X[1] NotX[2] NotX[4] X[5] NotX[7] X[8] X[9] NotX[10] X[11] + X[2] NotX[4] X[5] X[6] NotX[7] X[8] X[9] NotX[10] X[12] + NotX[1] NotX[2] NotX[3] X[4] X[5] NotX[7] X[8] NotX[10] X[12] + NotX[1] NotX[2] X[3] X[4] X[6] NotX[7] X[9] NotX[10] X[12] + NotX[1] X[3] X[5] NotX[7] X[8] X[9] NotX[10] X[11] X[12] + X[3] X[4] NotX[7] X[8] X[9] NotX[10] X[11] X[12] X[13] + X[3] NotX[4] NotX[5] NotX[6] X[7] X[8] NotX[10] X[12] X[13] + X[2] NotX[4] X[5] NotX[6] X[7] NotX[10] X[11] X[12] X[13] + NotX[3] X[4] X[5] NotX[6] X[8] X[9] NotX[10] X[12] X[13] + NotX[2] X[4] X[5] NotX[6] X[7] X[9] NotX[10] X[12] X[13] + NotX[1] X[3] X[4] NotX[6] X[7] X[8] NotX[10] X[12] X[13] + X[1] X[2] X[5] NotX[6] X[8] X[9] NotX[10] X[11] X[12] + NotX[3] NotX[4] NotX[5] X[6] X[8] X[9] NotX[10] X[11] X[12] + NotX[1] NotX[2] X[3] NotX[4] NotX[5] X[7] NotX[10] X[11] X[12] + X[1] NotX[2] NotX[3] NotX[5] X[9] NotX[10] X[11] X[12] X[13] + NotX[1] X[2] X[3] NotX[5] X[6] X[7] NotX[10] X[12] X[13] + X[2] NotX[3] NotX[4] X[5] X[6] X[8] NotX[10] X[11] X[13] + NotX[1] NotX[2] X[3] NotX[4] X[5] X[8] NotX[10] X[11] X[13] + X[1] X[3] NotX[4] X[6] X[8] NotX[10] X[11] X[12] X[13] + X[1] X[2] NotX[4] NotX[5] NotX[7] X[8] NotX[9] NotX[10] X[12] + NotX[1] X[2] X[3] NotX[5] X[6] NotX[7] NotX[9] NotX[10] X[11] + X[2] NotX[4] X[5] NotX[7] X[8] NotX[9] NotX[10] X[11] X[12] + NotX[1] NotX[3] X[4] NotX[7] X[8] NotX[9] NotX[10] X[11] X[13] + NotX[1] X[3] X[4] X[5] X[6] NotX[7] NotX[9] NotX[10] X[12] + X[1] NotX[2] NotX[3] NotX[6] X[7] NotX[9] NotX[10] X[11] X[13] + X[1] X[2] X[4] NotX[6] NotX[9] NotX[10] X[11] X[12] X[13] + NotX[2] NotX[3] NotX[4] NotX[5] X[6] X[7] NotX[9] NotX[10] X[12] + NotX[2] NotX[3] X[4] NotX[5] X[6] NotX[9] NotX[10] X[11] X[12] + NotX[1] NotX[2] X[3] X[4] NotX[5] NotX[9] NotX[10] X[12] X[13] + NotX[1] X[2] NotX[3] NotX[4] X[8] NotX[9] NotX[10] X[12] X[13] + X[1] NotX[3] X[4] X[6] X[8] NotX[9] NotX[10] X[12] X[13] + X[1] X[3] X[4] X[5] X[6] X[8] NotX[9] NotX[10] X[12] + NotX[1] NotX[2] NotX[3] NotX[4] NotX[5] NotX[6] NotX[7] NotX[8] NotX[10] + NotX[2] X[4] X[5] NotX[6] NotX[7] NotX[8] X[9] NotX[10] X[13] + X[2] NotX[3] NotX[5] X[6] NotX[7] NotX[8] X[9] NotX[10] X[12] + X[1] X[4] X[5] X[6] NotX[7] NotX[8] X[9] NotX[10] X[12] + X[1] X[2] NotX[4] NotX[5] NotX[6] NotX[8] NotX[10] X[11] X[13] + NotX[2] X[3] X[4] NotX[5] NotX[6] NotX[8] NotX[10] X[11] X[12] + NotX[1] X[2] X[3] NotX[5] NotX[6] X[7] NotX[8] NotX[10] X[11] + X[2] NotX[3] NotX[4] NotX[6] X[7] NotX[8] X[9] NotX[10] X[12] + X[1] X[2] X[4] NotX[6] NotX[8] X[9] NotX[10] X[12] X[13] + NotX[1] NotX[2] NotX[3] X[4] NotX[5] NotX[8] X[9] NotX[10] X[12] + NotX[2] NotX[3] NotX[4] X[5] X[6] NotX[8] X[9] NotX[10] X[11] + NotX[1] X[2] NotX[3] NotX[4] X[6] NotX[8] NotX[10] X[11] X[13] + X[1] X[2] NotX[4] X[6] X[7] NotX[8] X[9] NotX[10] X[11] + NotX[1] NotX[2] NotX[3] X[4] NotX[5] X[8] X[9] NotX[11] X[12] + NotX[1] NotX[3] X[4] NotX[5] X[7] X[10] NotX[11] X[12] X[13] + NotX[1] NotX[2] X[3] NotX[4] X[5] X[8] NotX[11] X[12] X[13] + X[1] NotX[2] NotX[4] X[5] X[6] X[7] X[8] NotX[11] X[12] + X[1] X[2] NotX[4] X[7] X[8] X[9] NotX[11] X[12] X[13] + NotX[1] NotX[2] NotX[3] X[4] X[5] X[7] X[8] NotX[11] X[12] + NotX[1] NotX[3] X[5] X[6] X[7] X[10] NotX[11] X[12] X[13] + X[1] X[4] X[6] X[7] X[9] X[10] NotX[11] X[12] X[13] + X[2] X[3] NotX[5] NotX[6] NotX[7] NotX[8] NotX[9] NotX[10] X[11] + NotX[1] NotX[2] X[3] NotX[4] NotX[5] NotX[7] NotX[8] NotX[9] NotX[10] + NotX[2] X[3] NotX[4] NotX[5] NotX[7] NotX[8] NotX[9] NotX[10] X[13] + X[1] X[2] NotX[5] X[6] NotX[7] NotX[8] NotX[9] NotX[10] X[11] + NotX[4] X[5] X[6] NotX[7] NotX[8] NotX[9] NotX[10] X[12] X[13] + NotX[1] X[2] NotX[3] X[4] NotX[7] NotX[8] NotX[9] NotX[10] X[12] + X[1] NotX[2] X[4] X[5] NotX[7] NotX[8] NotX[9] NotX[10] X[13] + NotX[3] NotX[4] NotX[6] X[7] NotX[8] NotX[9] NotX[10] X[12] X[13] + NotX[1] X[2] X[3] X[5] NotX[6] NotX[8] NotX[9] NotX[10] X[11] + X[1] NotX[2] NotX[4] NotX[5] X[6] X[7] NotX[8] NotX[9] NotX[10] + X[1] X[2] NotX[5] X[6] X[7] NotX[8] NotX[9] NotX[10] X[12] + NotX[1] NotX[2] NotX[3] NotX[4] X[5] X[6] NotX[8] NotX[9] NotX[10] + X[1] X[2] NotX[4] X[5] NotX[8] NotX[9] NotX[10] X[11] X[12] + NotX[1] NotX[2] X[3] X[5] X[7] NotX[8] NotX[9] NotX[10] X[11] + X[2] X[3] X[5] X[6] NotX[8] NotX[9] NotX[10] X[11] X[13] + NotX[1] X[3] X[5] NotX[6] NotX[7] NotX[9] NotX[10] X[11] X[12] + NotX[1] NotX[2] NotX[3] NotX[4] NotX[5] X[6] NotX[7] NotX[9] NotX[10] + NotX[2] X[3] NotX[4] NotX[5] NotX[7] X[8] NotX[9] NotX[10] X[11] + NotX[2] X[3] NotX[4] NotX[5] X[7] NotX[8] X[9] NotX[11] X[13] + X[1] X[3] X[4] NotX[5] X[6] NotX[8] X[9] NotX[11] X[12] + NotX[1] NotX[2] NotX[3] NotX[4] X[5] X[6] NotX[8] X[9] NotX[11] + X[1] NotX[3] NotX[4] X[5] NotX[8] X[9] NotX[11] X[12] X[13] + NotX[1] X[3] NotX[4] X[5] X[6] NotX[8] X[10] NotX[11] X[12] + X[1] X[2] NotX[4] X[6] X[7] NotX[8] X[9] NotX[11] X[12] + X[1] X[3] NotX[4] X[5] X[7] NotX[8] NotX[11] X[12] X[13] + X[1] NotX[3] X[4] X[6] X[7] NotX[8] X[9] NotX[11] X[13] + NotX[1] NotX[2] NotX[3] NotX[4] NotX[5] NotX[6] NotX[7] X[8] NotX[11] + NotX[1] NotX[2] X[3] X[4] NotX[6] NotX[7] X[8] X[9] NotX[11] + NotX[1] NotX[2] NotX[3] NotX[4] NotX[5] X[6] NotX[7] X[9] NotX[11] + NotX[2] NotX[4] NotX[5] NotX[7] X[8] X[9] NotX[11] X[12] X[13] + NotX[1] X[3] NotX[4] NotX[5] NotX[7] X[8] X[9] X[10] NotX[11] + X[1] X[3] NotX[4] X[5] NotX[7] X[9] NotX[11] X[12] X[13] + NotX[2] NotX[3] X[5] NotX[7] X[8] X[9] X[10] NotX[11] X[12] + NotX[1] X[2] NotX[3] X[4] NotX[7] X[8] NotX[11] X[12] X[13] + NotX[1] NotX[2] X[3] X[4] X[6] NotX[7] X[10] NotX[11] X[13] + X[1] NotX[2] X[4] X[5] X[6] NotX[7] X[9] NotX[11] X[13] + X[2] X[3] X[5] X[6] NotX[7] X[8] X[10] NotX[11] X[12] + X[2] NotX[5] NotX[6] X[8] X[9] X[10] NotX[11] X[12] X[13] + X[1] NotX[2] NotX[3] NotX[6] X[7] X[10] NotX[11] X[12] X[13] + X[2] NotX[3] X[4] X[5] NotX[6] X[7] X[10] NotX[11] X[13] + NotX[1] X[2] X[3] X[5] NotX[6] X[8] NotX[11] X[12] X[13] + X[1] X[3] X[4] X[5] NotX[6] X[7] X[10] NotX[11] X[13] + X[1] NotX[2] NotX[4] NotX[5] X[6] X[7] X[10] NotX[11] X[12] + NotX[1] NotX[4] NotX[5] X[7] X[9] X[10] NotX[11] X[12] X[13] + X[1] X[3] X[5] X[7] X[8] NotX[9] NotX[10] NotX[11] X[13] + NotX[1] X[3] X[4] NotX[6] NotX[7] NotX[8] NotX[10] NotX[11] X[12] + X[1] NotX[2] NotX[4] X[5] X[6] NotX[7] NotX[8] NotX[10] NotX[11] + X[1] X[2] NotX[4] NotX[5] NotX[6] NotX[8] NotX[10] NotX[11] X[12] + X[3] NotX[4] NotX[5] NotX[6] NotX[8] X[9] NotX[10] NotX[11] X[13] + X[1] NotX[2] NotX[3] NotX[6] X[7] NotX[8] NotX[10] NotX[11] X[13] + NotX[1] NotX[2] X[3] NotX[4] X[5] NotX[8] NotX[10] NotX[11] X[12] + NotX[2] X[3] NotX[4] NotX[5] NotX[6] NotX[7] X[9] NotX[10] NotX[11] + X[1] NotX[4] NotX[6] NotX[7] X[8] X[9] NotX[10] NotX[11] X[12] + NotX[1] NotX[4] NotX[5] X[6] NotX[7] X[9] NotX[10] NotX[11] X[12] + X[1] NotX[4] X[5] X[6] NotX[7] X[8] NotX[10] NotX[11] X[12] + NotX[4] X[5] X[6] NotX[7] X[9] NotX[10] NotX[11] X[12] X[13] + NotX[1] NotX[3] X[4] NotX[6] X[7] X[9] NotX[10] NotX[11] X[12] + X[1] NotX[2] X[5] NotX[6] X[8] X[9] NotX[10] NotX[11] X[13] + NotX[1] NotX[4] NotX[5] X[6] X[7] X[9] NotX[10] NotX[11] X[13] + X[1] NotX[3] X[4] NotX[5] X[8] X[9] NotX[10] NotX[11] X[13] + X[1] NotX[2] NotX[5] X[6] X[8] NotX[10] NotX[11] X[12] X[13] + NotX[2] NotX[3] NotX[4] X[7] X[8] NotX[10] NotX[11] X[12] X[13] + NotX[1] X[2] NotX[3] X[6] X[7] X[9] NotX[10] NotX[11] X[12] + NotX[3] X[4] X[5] X[6] X[7] X[9] NotX[10] NotX[11] X[13] + X[2] X[3] X[4] X[5] X[8] X[9] NotX[10] NotX[11] X[13] + X[2] X[3] X[4] X[6] X[7] X[9] NotX[10] NotX[11] X[13] + X[1] X[2] NotX[5] X[6] NotX[7] NotX[8] NotX[9] NotX[11] X[12] + NotX[2] NotX[3] NotX[7] NotX[8] NotX[9] X[10] NotX[11] X[12] X[13] + X[3] X[4] X[5] X[6] NotX[7] NotX[8] NotX[9] NotX[11] X[12] + NotX[1] NotX[3] NotX[4] NotX[6] X[7] NotX[8] NotX[9] X[10] NotX[11] + X[1] X[2] NotX[4] NotX[5] NotX[6] X[9] X[10] X[11] NotX[12] + NotX[1] X[2] X[3] NotX[5] NotX[6] X[8] X[9] NotX[12] X[13] + X[1] X[4] NotX[5] NotX[6] X[7] X[8] X[9] NotX[12] X[13] + NotX[1] X[2] NotX[3] NotX[4] NotX[6] X[8] X[9] X[10] NotX[12] + NotX[1] X[3] NotX[4] X[5] NotX[6] X[8] X[10] NotX[12] X[13] + X[1] X[3] NotX[4] NotX[6] X[7] X[10] X[11] NotX[12] X[13] + X[1] NotX[2] NotX[3] NotX[6] X[8] X[9] X[10] X[11] NotX[12] + X[1] X[2] X[5] NotX[6] X[7] X[9] X[11] NotX[12] X[13] + X[3] X[4] X[5] NotX[6] X[7] X[9] X[10] X[11] NotX[12] + NotX[1] NotX[2] X[3] NotX[4] NotX[5] X[7] X[9] NotX[12] X[13] + NotX[2] X[3] NotX[5] X[6] X[7] X[8] X[10] NotX[12] X[13] + X[1] NotX[2] NotX[4] X[5] X[6] X[8] X[9] X[10] NotX[12] + X[1] X[2] NotX[4] X[6] X[7] X[10] X[11] NotX[12] X[13] + NotX[1] X[2] NotX[3] X[6] X[7] X[8] X[9] NotX[12] X[13] + X[1] NotX[2] X[4] X[6] X[7] X[8] X[9] NotX[12] X[13] + NotX[1] X[3] X[5] X[6] X[7] X[8] X[11] NotX[12] X[13] + NotX[4] NotX[5] NotX[6] NotX[7] NotX[8] NotX[9] NotX[10] NotX[11] X[12] + X[1] NotX[4] X[5] X[6] X[7] NotX[8] NotX[9] NotX[10] NotX[11] + X[1] X[4] X[6] NotX[8] NotX[9] NotX[10] NotX[11] X[12] X[13] + X[3] X[4] X[5] X[7] NotX[8] NotX[9] NotX[10] NotX[11] X[13] + X[1] NotX[2] NotX[3] NotX[6] X[8] NotX[9] NotX[10] NotX[11] X[13] + X[1] X[2] X[5] NotX[6] X[7] NotX[9] NotX[10] NotX[11] X[13] + NotX[2] X[3] NotX[4] NotX[5] X[8] NotX[9] NotX[10] NotX[11] X[12] + NotX[1] NotX[2] NotX[3] X[4] NotX[5] X[6] NotX[9] NotX[10] NotX[11] + X[2] NotX[4] X[5] X[6] X[7] NotX[9] NotX[10] NotX[11] X[12] + NotX[1] X[2] NotX[3] X[4] X[7] NotX[9] NotX[10] NotX[11] X[12] + X[1] NotX[2] X[4] X[6] X[7] NotX[9] X[10] X[11] NotX[12] + X[1] X[4] X[5] X[7] X[8] NotX[9] X[11] NotX[12] X[13] + X[1] NotX[2] NotX[4] X[5] NotX[6] NotX[7] NotX[8] NotX[12] X[13] + X[1] X[3] X[4] NotX[6] NotX[7] NotX[8] X[9] X[11] NotX[12] + X[1] NotX[2] NotX[3] NotX[5] NotX[7] NotX[8] X[10] X[11] NotX[12] + NotX[1] X[5] X[6] NotX[7] NotX[8] X[9] X[10] X[11] NotX[12] + NotX[1] NotX[2] NotX[3] NotX[4] NotX[5] NotX[6] X[7] NotX[8] NotX[12] + X[2] NotX[3] X[4] NotX[5] NotX[6] NotX[8] X[9] NotX[12] X[13] + NotX[1] X[2] X[3] NotX[5] NotX[6] X[7] NotX[8] X[10] NotX[12] + NotX[1] X[2] NotX[3] NotX[4] NotX[6] NotX[8] X[11] NotX[12] X[13] + NotX[1] NotX[3] NotX[6] NotX[8] X[9] X[10] X[11] NotX[12] X[13] + NotX[1] NotX[2] X[3] X[4] NotX[6] X[7] NotX[8] X[10] NotX[12] + X[2] NotX[3] X[4] NotX[5] X[6] X[7] NotX[8] X[9] NotX[12] + NotX[2] X[3] NotX[4] X[6] NotX[8] X[9] X[10] NotX[12] X[13] + X[3] NotX[4] X[5] X[7] NotX[8] X[10] X[11] NotX[12] X[13] + X[1] NotX[2] NotX[3] X[7] NotX[8] X[9] X[10] NotX[12] X[13] + X[2] NotX[3] X[6] NotX[8] X[9] X[10] X[11] NotX[12] X[13] + X[1] X[3] X[4] X[6] NotX[8] X[9] X[10] X[11] NotX[12] + X[2] NotX[3] X[4] NotX[5] NotX[6] NotX[7] X[8] X[11] NotX[12] + NotX[3] NotX[4] X[5] NotX[6] NotX[7] X[9] X[10] NotX[12] X[13] + X[1] X[2] X[5] NotX[6] NotX[7] X[8] X[9] NotX[12] X[13] + NotX[3] X[4] NotX[5] X[6] NotX[7] X[8] X[11] NotX[12] X[13] + NotX[1] NotX[3] NotX[4] X[6] NotX[7] X[8] X[9] X[10] NotX[12] + X[1] NotX[4] X[6] NotX[7] X[8] X[10] X[11] NotX[12] X[13] + NotX[1] X[2] NotX[3] X[4] NotX[7] X[9] X[10] NotX[12] X[13] + NotX[2] NotX[4] NotX[5] NotX[6] X[7] X[8] X[9] NotX[12] X[13] + NotX[1] X[2] X[3] X[5] NotX[6] NotX[8] NotX[9] X[10] NotX[12] + NotX[2] NotX[4] NotX[5] X[6] NotX[8] NotX[9] X[10] X[11] NotX[12] + X[1] X[4] X[7] NotX[8] NotX[9] X[10] X[11] NotX[12] X[13] + NotX[1] X[2] X[3] NotX[5] NotX[6] NotX[7] X[8] NotX[9] NotX[12] + NotX[1] X[4] NotX[5] NotX[6] NotX[7] NotX[9] X[10] NotX[12] X[13] + X[1] X[3] X[4] NotX[5] NotX[6] NotX[7] X[8] NotX[9] NotX[12] + NotX[2] NotX[3] NotX[4] NotX[6] NotX[7] NotX[9] X[10] NotX[12] X[13] + X[1] NotX[2] NotX[3] NotX[6] NotX[7] X[8] NotX[9] X[11] NotX[12] + NotX[3] X[4] X[5] NotX[6] NotX[7] X[8] NotX[9] NotX[12] X[13] + X[1] X[2] NotX[4] NotX[5] NotX[7] X[8] NotX[9] X[11] NotX[12] + NotX[3] NotX[5] X[6] NotX[7] X[8] NotX[9] X[10] X[11] NotX[12] + NotX[1] X[2] X[3] NotX[5] X[6] NotX[7] NotX[9] X[10] NotX[12] + NotX[2] X[3] NotX[4] NotX[7] X[8] NotX[9] X[11] NotX[12] X[13] + X[2] NotX[3] X[4] X[5] X[6] NotX[7] NotX[9] NotX[12] X[13] + NotX[2] NotX[5] NotX[6] X[7] X[8] NotX[9] X[10] X[11] NotX[12] + X[1] NotX[2] NotX[3] NotX[6] X[7] NotX[9] X[10] NotX[12] X[13] + X[1] X[2] NotX[6] X[7] X[8] NotX[9] X[10] X[11] NotX[12] + X[2] X[4] NotX[6] X[7] X[8] NotX[9] X[11] NotX[12] X[13] + NotX[1] NotX[2] NotX[3] NotX[4] NotX[5] X[6] X[7] NotX[9] NotX[12] + X[1] NotX[3] NotX[5] X[6] X[8] NotX[9] X[10] X[11] NotX[12] + NotX[1] X[2] X[3] NotX[5] X[6] X[7] NotX[9] NotX[12] X[13] + X[1] X[3] X[4] NotX[5] X[7] X[8] NotX[9] NotX[12] X[13] + NotX[1] NotX[2] NotX[3] NotX[4] X[5] X[6] X[8] NotX[9] NotX[12] + NotX[1] X[2] NotX[3] NotX[4] X[6] NotX[9] X[10] X[11] NotX[12] + X[1] NotX[2] NotX[4] X[5] X[6] X[7] NotX[9] X[10] NotX[12] + NotX[1] X[2] NotX[3] X[4] X[7] NotX[9] X[11] NotX[12] X[13] + NotX[3] X[4] X[5] X[7] NotX[8] X[9] NotX[10] NotX[12] X[13] + X[1] X[3] X[4] X[5] NotX[8] X[9] NotX[10] NotX[12] X[13] + NotX[1] NotX[2] NotX[3] NotX[4] X[5] NotX[6] NotX[7] NotX[10] NotX[12] + X[1] NotX[4] NotX[5] NotX[7] X[8] X[9] NotX[10] X[11] NotX[12] + X[1] NotX[2] NotX[3] NotX[5] NotX[7] X[9] NotX[10] NotX[12] X[13] + NotX[1] NotX[3] X[4] X[5] X[6] NotX[7] X[8] NotX[10] NotX[12] + NotX[1] NotX[3] X[6] NotX[7] X[8] X[9] NotX[10] NotX[12] X[13] + NotX[1] X[3] X[4] X[5] NotX[7] X[8] NotX[10] X[11] NotX[12] + X[1] X[5] X[6] NotX[7] X[8] X[9] NotX[10] NotX[12] X[13] + NotX[1] X[2] NotX[3] NotX[4] NotX[6] X[8] NotX[10] X[11] NotX[12] + X[2] NotX[3] X[5] NotX[6] X[8] X[9] NotX[10] NotX[12] X[13] + X[1] NotX[2] NotX[6] X[7] X[9] NotX[10] X[11] NotX[12] X[13] + NotX[2] X[3] X[4] NotX[6] X[7] NotX[10] X[11] NotX[12] X[13] + NotX[1] X[2] X[3] X[5] NotX[6] X[8] NotX[10] NotX[12] X[13] + X[1] X[2] NotX[4] NotX[5] X[7] X[8] NotX[10] X[11] NotX[12] + NotX[1] NotX[2] NotX[3] X[4] NotX[5] X[6] NotX[10] X[11] NotX[12] + X[2] NotX[3] X[4] NotX[5] X[6] X[7] X[8] NotX[10] NotX[12] + NotX[1] NotX[2] X[3] X[4] NotX[5] NotX[10] X[11] NotX[12] X[13] + X[2] X[3] NotX[5] X[7] X[9] NotX[10] X[11] NotX[12] X[13] + X[1] NotX[2] NotX[4] X[6] X[7] X[9] NotX[10] NotX[12] X[13] + NotX[2] NotX[3] X[5] NotX[6] NotX[7] NotX[8] NotX[9] X[11] NotX[12] + X[1] X[3] NotX[6] NotX[7] NotX[8] NotX[9] X[10] X[11] NotX[12] + X[2] NotX[3] NotX[4] NotX[7] NotX[8] NotX[9] X[10] X[11] NotX[12] + NotX[2] X[4] NotX[7] NotX[8] NotX[9] X[10] X[11] NotX[12] X[13] + X[1] X[2] X[4] NotX[7] NotX[8] NotX[9] X[10] X[11] NotX[12] + X[2] NotX[3] NotX[4] NotX[6] X[7] NotX[8] NotX[9] X[11] NotX[12] + NotX[1] X[4] X[5] NotX[6] X[8] X[10] NotX[11] NotX[12] X[13] + NotX[2] NotX[3] NotX[4] NotX[5] X[6] X[10] NotX[11] NotX[12] X[13] + NotX[1] NotX[2] NotX[3] X[4] NotX[5] X[6] X[9] NotX[11] NotX[12] + NotX[1] X[3] NotX[4] X[5] X[6] X[9] NotX[11] NotX[12] X[13] + X[1] X[2] NotX[4] X[6] X[8] X[9] NotX[11] NotX[12] X[13] + NotX[2] NotX[3] X[5] X[6] X[8] X[10] NotX[11] NotX[12] X[13] + NotX[3] X[5] X[7] X[8] X[9] X[10] NotX[11] NotX[12] X[13] + NotX[1] NotX[2] X[3] X[4] X[6] X[7] X[9] NotX[11] NotX[12] + X[1] NotX[2] NotX[3] NotX[5] NotX[7] NotX[8] NotX[9] NotX[10] NotX[12] + NotX[1] X[3] X[5] NotX[7] NotX[8] NotX[9] NotX[10] NotX[12] X[13] + X[1] X[2] X[4] NotX[6] NotX[8] NotX[9] NotX[10] X[11] NotX[12] + X[1] NotX[2] X[4] X[6] X[7] NotX[8] NotX[9] NotX[10] NotX[12] + X[1] X[2] X[6] X[7] NotX[8] NotX[9] NotX[10] NotX[12] X[13] + X[1] X[2] NotX[4] X[5] NotX[7] NotX[9] NotX[10] NotX[12] X[13] + X[1] X[3] X[4] X[5] NotX[7] X[8] NotX[9] NotX[10] NotX[12] + NotX[1] NotX[4] NotX[5] NotX[6] X[8] NotX[9] NotX[10] NotX[12] X[13] + NotX[3] NotX[6] X[7] X[8] NotX[9] NotX[10] X[11] NotX[12] X[13] + NotX[1] NotX[2] X[3] NotX[4] NotX[5] X[7] NotX[9] NotX[10] NotX[12] + X[2] NotX[3] NotX[4] X[6] X[8] NotX[9] NotX[10] X[11] NotX[12] + X[1] X[3] NotX[4] X[5] X[7] NotX[9] NotX[10] X[11] NotX[12] + X[1] NotX[2] NotX[3] X[6] X[8] NotX[9] NotX[10] NotX[12] X[13] + NotX[2] X[3] NotX[5] NotX[7] NotX[8] NotX[10] X[11] NotX[12] X[13] + NotX[1] X[2] NotX[3] X[4] NotX[7] NotX[8] NotX[10] X[11] NotX[12] + NotX[1] NotX[2] X[4] X[5] X[6] NotX[7] NotX[8] NotX[10] NotX[12] + NotX[1] NotX[2] NotX[3] X[4] NotX[5] NotX[6] NotX[8] NotX[10] NotX[12] + NotX[3] NotX[4] X[5] NotX[6] X[7] NotX[8] NotX[10] X[11] NotX[12] + X[1] NotX[2] X[5] NotX[7] NotX[9] X[10] NotX[11] NotX[12] X[13] + NotX[1] NotX[3] X[4] NotX[5] X[6] NotX[9] X[10] NotX[11] NotX[12] + X[1] X[2] NotX[4] X[5] NotX[9] X[10] NotX[11] NotX[12] X[13] + X[2] NotX[3] X[4] X[6] X[7] NotX[9] NotX[11] NotX[12] X[13] + NotX[1] X[2] X[3] X[5] X[6] NotX[9] NotX[11] NotX[12] X[13] + NotX[1] X[3] X[6] X[7] NotX[9] X[10] NotX[11] NotX[12] X[13] + NotX[1] X[2] NotX[3] NotX[4] NotX[6] NotX[7] NotX[8] NotX[11] NotX[12] + X[1] X[2] X[4] NotX[6] NotX[7] NotX[8] NotX[11] NotX[12] X[13] + NotX[3] X[5] X[6] NotX[7] NotX[8] X[10] NotX[11] NotX[12] X[13] + X[1] X[2] NotX[5] X[6] NotX[8] X[9] NotX[11] NotX[12] X[13] + NotX[1] X[2] NotX[3] NotX[4] X[6] NotX[8] X[9] NotX[11] NotX[12] + X[1] X[2] NotX[4] X[5] NotX[8] X[9] NotX[11] NotX[12] X[13] + NotX[1] NotX[3] X[4] X[5] X[6] X[7] NotX[8] NotX[11] NotX[12] + X[1] X[3] X[6] X[7] NotX[8] X[10] NotX[11] NotX[12] X[13] + X[2] NotX[3] NotX[5] NotX[6] NotX[7] X[8] NotX[11] NotX[12] X[13] + X[1] NotX[2] NotX[3] NotX[5] NotX[7] X[10] NotX[11] NotX[12] X[13] + NotX[2] X[3] NotX[5] X[6] NotX[7] X[10] NotX[11] NotX[12] X[13] + NotX[1] NotX[2] X[3] NotX[4] X[5] NotX[7] NotX[11] NotX[12] X[13] + X[2] X[3] X[4] X[5] X[6] NotX[7] X[10] NotX[11] NotX[12] + X[2] X[4] X[6] NotX[7] X[8] X[9] X[10] NotX[11] NotX[12] + X[1] X[2] NotX[4] NotX[5] NotX[6] X[9] NotX[11] NotX[12] X[13] + NotX[1] NotX[2] NotX[3] X[4] NotX[5] NotX[6] X[8] NotX[11] NotX[12] + NotX[1] NotX[2] NotX[3] NotX[4] X[5] NotX[6] X[7] NotX[11] NotX[12] + NotX[2] NotX[4] NotX[6] X[7] X[8] X[10] NotX[11] NotX[12] X[13] + NotX[1] NotX[2] NotX[3] X[4] X[5] NotX[6] NotX[11] NotX[12] X[13] + X[1] NotX[2] NotX[6] X[8] X[9] X[10] NotX[11] NotX[12] X[13] + NotX[1] NotX[3] X[4] X[6] X[7] X[9] X[10] X[11] NotX[13] + X[1] NotX[3] X[5] X[7] X[8] X[10] X[11] X[12] NotX[13] + NotX[1] NotX[2] X[3] X[4] X[6] X[7] X[9] X[11] NotX[13] + NotX[1] X[2] X[3] X[5] X[8] X[9] X[10] X[12] NotX[13] + X[1] X[3] X[4] X[7] X[8] X[10] X[11] X[12] NotX[13] + X[2] X[3] NotX[5] NotX[6] NotX[8] NotX[9] NotX[10] NotX[11] NotX[12] + NotX[1] NotX[5] X[6] NotX[7] NotX[9] NotX[10] NotX[11] NotX[12] X[13] + X[3] NotX[4] X[5] NotX[7] X[8] NotX[9] NotX[10] NotX[11] NotX[12] + X[2] NotX[4] NotX[5] X[6] NotX[9] NotX[10] NotX[11] NotX[12] X[13] + NotX[1] NotX[2] X[3] X[4] NotX[5] NotX[9] NotX[10] NotX[11] NotX[12] + NotX[1] NotX[2] X[3] X[5] X[7] NotX[9] NotX[10] NotX[11] NotX[12] + X[2] NotX[3] X[4] X[6] NotX[7] NotX[8] NotX[10] NotX[11] NotX[12] + NotX[1] X[3] X[4] NotX[5] NotX[8] X[9] NotX[10] NotX[11] NotX[12] + X[1] X[3] X[4] NotX[5] X[6] NotX[7] NotX[10] NotX[11] NotX[12] + NotX[2] X[3] X[4] X[5] NotX[7] X[8] NotX[10] NotX[11] NotX[12] + NotX[1] X[2] NotX[3] NotX[4] NotX[6] X[7] NotX[10] NotX[11] NotX[12] + X[3] NotX[4] X[5] NotX[6] X[7] NotX[10] NotX[11] NotX[12] X[13] + NotX[1] X[2] NotX[3] X[4] NotX[6] NotX[10] NotX[11] NotX[12] X[13] + NotX[2] X[4] NotX[6] X[7] X[9] NotX[10] NotX[11] NotX[12] X[13] + NotX[2] X[3] NotX[4] NotX[5] X[8] NotX[10] NotX[11] NotX[12] X[13] + NotX[2] X[3] NotX[4] X[5] X[7] X[9] NotX[10] NotX[11] NotX[12] + NotX[1] NotX[3] X[5] X[6] X[7] X[8] NotX[10] NotX[11] NotX[12] + X[1] X[2] NotX[4] NotX[5] NotX[6] NotX[8] NotX[9] NotX[11] NotX[12] + NotX[1] NotX[4] X[5] X[6] NotX[8] NotX[9] X[10] NotX[11] NotX[12] + X[1] X[2] NotX[5] X[6] NotX[7] NotX[9] X[10] NotX[11] NotX[12] + NotX[1] X[2] NotX[3] NotX[4] NotX[7] X[8] NotX[9] NotX[11] NotX[12] + NotX[2] NotX[4] NotX[5] X[6] NotX[7] X[8] X[9] X[11] NotX[13] + NotX[2] NotX[3] NotX[5] X[6] NotX[7] X[9] X[10] X[11] NotX[13] + NotX[1] X[2] X[3] NotX[5] X[6] NotX[7] X[9] X[11] NotX[13] + X[1] X[2] NotX[4] X[6] NotX[7] X[8] X[9] X[10] NotX[13] + X[1] NotX[3] X[5] X[6] NotX[7] X[8] X[10] X[12] NotX[13] + NotX[1] NotX[2] X[3] X[4] X[6] NotX[7] X[9] X[10] NotX[13] + X[1] X[3] X[4] X[5] NotX[7] X[8] X[10] X[11] NotX[13] + NotX[1] NotX[2] NotX[3] NotX[4] NotX[5] NotX[6] X[7] X[8] NotX[13] + X[1] X[2] NotX[4] NotX[5] NotX[6] X[9] X[10] X[12] NotX[13] + NotX[1] NotX[2] NotX[3] X[4] NotX[5] NotX[6] X[8] X[11] NotX[13] + X[2] NotX[3] X[4] NotX[5] NotX[6] X[7] X[9] X[10] NotX[13] + NotX[1] NotX[2] NotX[3] NotX[4] X[5] NotX[6] X[7] X[11] NotX[13] + X[1] X[3] NotX[4] NotX[6] X[8] X[9] X[10] X[11] NotX[13] + NotX[4] X[5] NotX[6] X[7] X[8] X[10] X[11] X[12] NotX[13] + NotX[2] NotX[3] X[4] NotX[6] X[7] X[8] X[10] X[11] NotX[13] + NotX[1] NotX[2] X[3] X[4] NotX[6] X[7] X[8] X[9] NotX[13] + NotX[1] NotX[2] NotX[3] NotX[4] NotX[5] X[6] X[7] X[9] NotX[13] + NotX[3] NotX[4] NotX[5] X[6] X[7] X[8] X[9] X[10] NotX[13] + NotX[1] NotX[2] X[3] NotX[4] NotX[5] X[7] X[10] X[11] NotX[13] + X[1] NotX[3] X[4] NotX[5] X[6] X[7] X[10] X[12] NotX[13] + X[1] NotX[2] X[4] NotX[5] X[6] X[8] X[9] X[10] NotX[13] + X[2] X[4] NotX[5] X[6] X[8] X[9] X[10] X[11] NotX[13] + NotX[1] NotX[2] NotX[3] NotX[4] X[5] X[6] X[8] X[9] NotX[13] + X[1] NotX[2] NotX[4] X[5] X[6] X[7] X[11] X[12] NotX[13] + X[2] X[3] NotX[4] X[6] X[7] X[8] X[10] X[12] NotX[13] + NotX[1] X[2] NotX[3] X[8] X[9] X[10] X[11] X[12] NotX[13] + NotX[1] NotX[2] NotX[3] X[4] NotX[5] X[6] NotX[9] X[10] NotX[13] + NotX[2] NotX[5] X[6] X[7] X[8] NotX[9] X[10] X[11] NotX[13] + X[1] X[3] X[4] NotX[5] X[6] X[7] NotX[9] X[12] NotX[13] + NotX[1] NotX[3] NotX[4] X[5] X[6] X[8] NotX[9] X[12] NotX[13] + NotX[1] NotX[2] X[3] NotX[4] X[5] X[8] NotX[9] X[12] NotX[13] + NotX[1] X[2] NotX[3] NotX[4] NotX[6] NotX[7] NotX[8] X[11] NotX[13] + X[1] NotX[2] NotX[4] X[5] NotX[6] NotX[7] NotX[8] X[9] NotX[13] + NotX[3] NotX[4] NotX[5] X[6] NotX[7] NotX[8] X[9] X[11] NotX[13] + X[1] NotX[2] NotX[4] X[5] X[6] NotX[7] NotX[8] X[10] NotX[13] + X[1] X[3] NotX[4] X[6] NotX[7] NotX[8] X[9] X[12] NotX[13] + X[1] NotX[4] X[5] NotX[7] NotX[8] X[10] X[11] X[12] NotX[13] + NotX[1] X[2] NotX[3] X[4] NotX[7] NotX[8] X[10] X[11] NotX[13] + NotX[1] NotX[3] X[4] NotX[7] NotX[8] X[9] X[11] X[12] NotX[13] + X[1] X[2] X[4] NotX[7] NotX[8] X[10] X[11] X[12] NotX[13] + NotX[1] NotX[2] NotX[3] X[4] NotX[5] NotX[6] NotX[8] X[10] NotX[13] + NotX[2] X[4] NotX[5] X[6] NotX[8] X[9] X[10] X[12] NotX[13] + NotX[1] X[2] NotX[3] NotX[4] X[6] NotX[8] X[10] X[12] NotX[13] + NotX[1] NotX[2] X[3] NotX[4] X[5] NotX[8] X[9] X[10] NotX[13] + NotX[1] X[3] NotX[4] X[5] X[6] NotX[8] X[11] X[12] NotX[13] + NotX[1] NotX[2] NotX[3] X[4] X[5] X[7] NotX[8] X[10] NotX[13] + NotX[3] X[4] X[5] X[6] NotX[8] X[10] X[11] X[12] NotX[13] + X[2] X[3] X[4] X[5] X[6] NotX[8] X[11] X[12] NotX[13] + NotX[1] X[2] X[3] NotX[5] NotX[6] NotX[7] X[8] X[9] NotX[13] + X[1] X[3] X[4] NotX[5] NotX[6] NotX[7] X[9] X[10] NotX[13] + NotX[1] NotX[2] NotX[3] NotX[4] X[5] NotX[6] NotX[7] X[10] NotX[13] + NotX[3] X[5] NotX[6] NotX[7] X[8] X[9] X[11] X[12] NotX[13] + NotX[1] X[2] NotX[3] NotX[4] X[6] X[9] NotX[10] X[11] NotX[13] + X[1] NotX[4] X[5] X[6] X[7] X[8] X[9] NotX[10] NotX[13] + NotX[1] NotX[3] X[4] X[5] X[7] X[9] NotX[10] X[11] NotX[13] + X[1] NotX[2] X[4] X[7] X[9] NotX[10] X[11] X[12] NotX[13] + X[2] X[4] X[6] X[8] X[9] NotX[10] X[11] X[12] NotX[13] + NotX[2] NotX[3] X[4] NotX[6] NotX[7] NotX[8] NotX[9] X[12] NotX[13] + NotX[2] X[3] X[4] NotX[6] NotX[7] NotX[8] NotX[9] X[10] NotX[13] + X[1] NotX[2] NotX[3] NotX[5] NotX[7] NotX[8] NotX[9] X[12] NotX[13] + NotX[2] X[3] NotX[4] NotX[5] NotX[6] NotX[8] NotX[9] X[11] NotX[13] + X[1] X[2] NotX[4] NotX[5] NotX[6] NotX[8] NotX[9] X[11] NotX[13] + NotX[2] NotX[4] NotX[6] X[7] NotX[8] NotX[9] X[10] X[11] NotX[13] + X[1] NotX[2] X[4] X[5] X[6] NotX[8] NotX[9] X[12] NotX[13] + NotX[1] X[4] X[6] X[7] NotX[8] NotX[9] X[10] X[11] NotX[13] + X[2] X[3] NotX[5] NotX[6] NotX[7] X[8] NotX[9] X[12] NotX[13] + X[1] X[2] X[5] NotX[6] NotX[7] X[8] NotX[9] X[10] NotX[13] + NotX[1] NotX[2] X[3] NotX[4] NotX[5] NotX[7] X[8] NotX[9] NotX[13] + X[2] NotX[3] X[4] NotX[5] NotX[7] X[8] NotX[9] X[12] NotX[13] + X[1] X[3] NotX[4] X[5] X[6] NotX[7] X[8] NotX[9] NotX[13] + X[1] NotX[2] NotX[3] NotX[7] X[8] NotX[9] X[11] X[12] NotX[13] + NotX[1] X[2] X[3] X[5] NotX[7] X[8] NotX[9] X[10] NotX[13] + NotX[2] X[3] NotX[4] NotX[6] X[7] X[8] NotX[9] X[11] NotX[13] + X[1] NotX[2] NotX[3] NotX[6] X[7] NotX[9] X[11] X[12] NotX[13] + NotX[1] X[3] X[5] NotX[6] X[7] X[8] NotX[9] X[10] NotX[13] + NotX[3] NotX[4] NotX[5] X[6] NotX[9] X[10] X[11] X[12] NotX[13] + NotX[2] X[3] NotX[4] NotX[5] X[6] X[8] NotX[9] X[10] NotX[13] + X[1] X[2] NotX[4] NotX[5] X[8] NotX[9] X[10] X[12] NotX[13] + NotX[1] NotX[2] X[3] X[4] NotX[5] NotX[9] NotX[10] X[11] NotX[13] + NotX[1] X[2] NotX[3] X[4] X[7] NotX[9] NotX[10] X[11] NotX[13] + X[1] NotX[3] X[4] X[5] X[6] NotX[9] NotX[10] X[12] NotX[13] + X[2] NotX[3] X[6] X[7] X[8] NotX[9] NotX[10] X[12] NotX[13] + NotX[3] X[5] NotX[6] NotX[7] NotX[8] X[9] NotX[10] X[12] NotX[13] + X[2] NotX[4] X[5] NotX[7] NotX[8] X[9] NotX[10] X[12] NotX[13] + X[2] NotX[3] NotX[5] NotX[6] X[7] NotX[8] X[9] NotX[10] NotX[13] + X[1] X[3] NotX[4] NotX[6] X[7] NotX[8] X[9] NotX[10] NotX[13] + X[1] X[2] X[4] NotX[6] NotX[8] NotX[10] X[11] X[12] NotX[13] + NotX[2] NotX[3] NotX[4] NotX[5] X[7] NotX[8] NotX[10] X[12] NotX[13] + X[1] X[4] X[6] X[7] NotX[8] X[9] NotX[10] X[12] NotX[13] + NotX[1] NotX[3] NotX[4] NotX[6] NotX[7] X[8] NotX[10] X[11] NotX[13] + X[1] X[2] NotX[4] NotX[5] NotX[7] X[9] NotX[10] X[11] NotX[13] + X[1] NotX[2] NotX[3] NotX[5] NotX[7] X[9] NotX[10] X[11] NotX[13] + NotX[1] X[2] NotX[3] X[4] NotX[7] X[8] NotX[10] X[12] NotX[13] + X[1] NotX[2] X[4] X[5] X[6] NotX[7] X[9] NotX[10] NotX[13] + X[2] NotX[3] X[4] NotX[5] NotX[6] X[7] X[8] NotX[10] NotX[13] + NotX[1] X[2] X[3] NotX[5] NotX[6] X[7] X[8] NotX[10] NotX[13] + X[1] X[3] X[4] NotX[5] NotX[6] X[7] X[8] NotX[10] NotX[13] + NotX[1] X[2] NotX[3] NotX[4] NotX[6] X[7] NotX[10] X[12] NotX[13] + NotX[2] X[3] NotX[4] NotX[6] X[9] NotX[10] X[11] X[12] NotX[13] + NotX[1] X[2] X[3] X[5] NotX[6] X[9] NotX[10] X[11] NotX[13] + X[1] X[2] NotX[4] NotX[5] X[7] X[8] NotX[10] X[12] NotX[13] + NotX[1] NotX[3] NotX[5] X[6] X[8] NotX[10] X[11] X[12] NotX[13] + NotX[1] X[2] X[3] NotX[5] X[6] X[7] NotX[10] X[11] NotX[13] + X[1] X[3] NotX[5] X[6] X[7] X[8] NotX[10] X[11] NotX[13] + NotX[2] X[3] NotX[4] NotX[6] NotX[7] X[8] NotX[11] X[12] NotX[13] + X[1] X[2] X[5] NotX[6] NotX[7] X[8] X[9] NotX[11] NotX[13] + NotX[3] NotX[4] NotX[5] NotX[7] X[9] X[10] NotX[11] X[12] NotX[13] + NotX[3] X[4] NotX[5] NotX[7] X[8] X[9] NotX[11] X[12] NotX[13] + X[2] X[3] NotX[5] X[6] NotX[7] X[9] NotX[11] X[12] NotX[13] + X[1] NotX[2] NotX[5] NotX[6] X[7] X[10] NotX[11] X[12] NotX[13] + NotX[3] NotX[4] NotX[6] X[7] X[9] X[10] NotX[11] X[12] NotX[13] + NotX[1] NotX[4] X[5] NotX[6] X[7] X[9] NotX[11] X[12] NotX[13] + X[1] NotX[2] X[5] NotX[6] X[7] X[8] NotX[11] X[12] NotX[13] + X[1] X[3] X[5] NotX[6] X[8] X[9] X[10] NotX[11] NotX[13] + X[2] X[3] NotX[6] X[7] X[8] X[9] NotX[11] X[12] NotX[13] + NotX[1] NotX[2] X[3] NotX[4] NotX[5] X[7] X[9] NotX[11] NotX[13] + NotX[1] X[2] X[3] NotX[5] X[6] X[7] NotX[11] X[12] NotX[13] + X[1] X[3] NotX[5] X[6] X[8] X[9] NotX[11] X[12] NotX[13] + X[2] NotX[3] NotX[4] X[6] X[8] X[9] X[10] NotX[11] NotX[13] + NotX[1] X[2] NotX[3] X[4] X[8] X[9] X[10] NotX[11] NotX[13] + X[1] NotX[3] X[5] X[7] X[8] X[9] NotX[11] X[12] NotX[13] + X[1] NotX[2] X[4] X[5] X[6] X[9] X[10] NotX[11] NotX[13] + NotX[2] X[3] X[4] X[6] X[8] X[10] NotX[11] X[12] NotX[13] + X[1] X[3] X[6] NotX[7] NotX[8] NotX[9] NotX[10] X[11] NotX[13] + NotX[2] NotX[4] NotX[6] X[7] NotX[8] NotX[9] NotX[10] X[12] NotX[13] + NotX[1] X[2] NotX[3] NotX[4] X[6] NotX[8] NotX[9] NotX[10] NotX[13] + NotX[2] NotX[3] X[4] X[7] NotX[8] NotX[9] NotX[10] X[12] NotX[13] + NotX[2] NotX[4] X[5] NotX[6] NotX[7] NotX[9] NotX[10] X[11] NotX[13] + NotX[2] X[3] X[4] X[5] NotX[6] NotX[9] NotX[10] X[11] NotX[13] + X[1] X[2] X[5] NotX[6] X[8] NotX[9] NotX[10] X[12] NotX[13] + NotX[2] X[4] X[5] NotX[6] X[8] NotX[10] NotX[11] X[12] NotX[13] + NotX[1] X[2] X[3] X[5] NotX[6] X[8] NotX[10] NotX[11] NotX[13] + X[1] NotX[2] NotX[3] NotX[5] X[8] NotX[10] NotX[11] X[12] NotX[13] + NotX[1] X[2] X[3] X[5] X[6] NotX[10] NotX[11] X[12] NotX[13] + X[3] X[4] X[6] X[7] X[8] X[9] NotX[10] NotX[11] NotX[13] + X[1] NotX[2] NotX[3] NotX[6] X[7] NotX[8] NotX[9] NotX[11] NotX[13] + X[1] X[2] X[4] NotX[6] NotX[8] NotX[9] X[10] NotX[11] NotX[13] + X[1] NotX[4] NotX[5] NotX[8] NotX[9] X[10] NotX[11] X[12] NotX[13] + NotX[2] X[3] NotX[5] X[6] NotX[8] NotX[9] NotX[11] X[12] NotX[13] + X[1] X[2] NotX[4] X[5] NotX[8] NotX[9] X[10] NotX[11] NotX[13] + X[1] X[4] X[5] X[6] NotX[8] NotX[9] X[10] NotX[11] NotX[13] + NotX[1] X[4] NotX[6] NotX[7] X[8] NotX[9] NotX[11] X[12] NotX[13] + NotX[2] NotX[3] NotX[4] X[5] NotX[6] NotX[9] NotX[11] X[12] NotX[13] + NotX[1] NotX[2] X[3] X[4] NotX[5] NotX[9] NotX[11] X[12] NotX[13] + NotX[2] NotX[3] X[5] X[6] NotX[9] X[10] NotX[11] X[12] NotX[13] + NotX[1] X[2] NotX[3] X[4] NotX[9] X[10] NotX[11] X[12] NotX[13] + NotX[1] NotX[4] NotX[5] NotX[6] NotX[7] NotX[8] X[10] NotX[11] NotX[13] + X[1] NotX[2] NotX[3] NotX[5] NotX[7] NotX[8] X[9] NotX[11] NotX[13] + NotX[1] X[2] NotX[3] X[4] NotX[7] NotX[8] X[9] NotX[11] NotX[13] + X[1] X[2] X[4] NotX[7] NotX[8] X[9] X[10] NotX[11] NotX[13] + X[2] X[3] NotX[4] NotX[6] NotX[8] X[9] NotX[11] X[12] NotX[13] + X[1] X[3] X[4] NotX[6] X[7] NotX[8] NotX[11] X[12] NotX[13] + X[1] NotX[3] X[5] NotX[8] X[9] X[10] NotX[11] X[12] NotX[13] + NotX[1] X[4] X[5] X[6] NotX[8] X[9] NotX[11] X[12] NotX[13] + X[2] X[3] X[4] X[7] NotX[8] X[9] X[10] NotX[11] NotX[13] + NotX[1] X[2] NotX[3] NotX[4] NotX[6] NotX[7] NotX[11] X[12] NotX[13] + X[1] NotX[2] X[6] X[7] NotX[8] X[9] X[11] NotX[12] NotX[13] + NotX[1] X[2] X[3] X[6] X[7] NotX[8] X[10] NotX[12] NotX[13] + NotX[2] X[3] NotX[4] NotX[5] NotX[6] X[8] X[10] NotX[12] NotX[13] + X[3] NotX[4] X[5] NotX[6] X[7] X[9] X[11] NotX[12] NotX[13] + X[2] NotX[3] X[5] NotX[6] X[7] X[9] X[10] NotX[12] NotX[13] + NotX[1] X[2] X[3] X[5] NotX[6] X[9] X[10] NotX[12] NotX[13] + X[1] X[3] X[4] X[5] NotX[6] X[7] X[11] NotX[12] NotX[13] + NotX[1] X[2] X[3] NotX[5] X[7] X[8] X[10] NotX[12] NotX[13] + X[1] X[3] X[4] NotX[5] X[7] X[8] X[10] NotX[12] NotX[13] + NotX[1] NotX[2] X[3] NotX[4] X[5] X[8] X[10] NotX[12] NotX[13] + X[1] X[2] NotX[4] X[6] X[7] X[8] X[10] NotX[12] NotX[13] + X[2] NotX[4] X[5] X[8] X[9] X[10] X[11] NotX[12] NotX[13] + NotX[1] X[2] NotX[3] X[4] X[8] X[9] X[11] NotX[12] NotX[13] + X[1] NotX[3] X[4] X[5] X[9] X[10] X[11] NotX[12] NotX[13] + X[2] X[3] X[4] X[5] X[6] X[7] X[11] NotX[12] NotX[13] + X[3] X[4] X[5] X[6] X[8] X[9] X[11] NotX[12] NotX[13] + NotX[3] NotX[5] NotX[6] X[7] NotX[9] NotX[10] NotX[11] X[12] NotX[13] + NotX[2] X[3] NotX[6] NotX[7] NotX[8] NotX[10] NotX[11] X[12] NotX[13] + X[1] X[2] X[4] NotX[6] NotX[7] NotX[8] NotX[10] NotX[11] NotX[13] + X[1] X[2] NotX[4] X[5] NotX[7] NotX[8] NotX[10] NotX[11] NotX[13] + X[1] X[2] X[5] NotX[6] X[7] NotX[8] NotX[10] NotX[11] NotX[13] + X[1] NotX[2] NotX[3] X[7] NotX[8] X[9] NotX[10] NotX[11] NotX[13] + NotX[2] X[3] X[6] X[7] NotX[8] X[9] NotX[10] NotX[11] NotX[13] + NotX[2] NotX[4] X[5] NotX[7] X[8] X[9] NotX[10] NotX[11] NotX[13] + X[1] X[2] X[6] NotX[7] X[8] X[9] NotX[10] NotX[11] NotX[13] + NotX[4] NotX[5] NotX[6] X[7] X[8] X[9] NotX[10] NotX[11] NotX[13] + X[1] X[3] X[4] X[7] NotX[8] X[9] NotX[10] NotX[12] NotX[13] + X[2] NotX[3] X[4] NotX[5] X[6] NotX[7] NotX[10] NotX[12] NotX[13] + NotX[1] NotX[2] X[3] NotX[4] X[5] NotX[7] NotX[10] NotX[12] NotX[13] + X[1] X[2] NotX[4] X[5] NotX[7] NotX[10] X[11] NotX[12] NotX[13] + X[2] NotX[3] X[4] X[5] NotX[7] NotX[10] X[11] NotX[12] NotX[13] + NotX[2] X[3] X[4] NotX[7] X[9] NotX[10] X[11] NotX[12] NotX[13] + NotX[1] NotX[2] NotX[3] X[4] X[5] NotX[6] NotX[10] NotX[12] NotX[13] + X[1] X[2] X[5] NotX[6] X[7] X[8] NotX[10] NotX[12] NotX[13] + NotX[2] X[3] NotX[4] NotX[5] X[9] NotX[10] X[11] NotX[12] NotX[13] + NotX[1] X[3] NotX[4] X[5] X[6] NotX[10] X[11] NotX[12] NotX[13] + X[1] NotX[2] NotX[3] X[7] X[8] NotX[10] X[11] NotX[12] NotX[13] + X[2] NotX[3] X[4] X[5] X[7] X[9] NotX[10] NotX[12] NotX[13] + NotX[4] X[5] X[6] NotX[7] NotX[8] NotX[9] X[11] NotX[12] NotX[13] + X[3] X[4] X[6] NotX[8] NotX[9] X[10] X[11] NotX[12] NotX[13] + NotX[1] NotX[3] X[4] X[5] NotX[7] NotX[9] X[10] NotX[12] NotX[13] + X[1] NotX[3] X[5] X[6] NotX[7] X[8] NotX[9] NotX[12] NotX[13] + X[1] NotX[2] X[4] X[5] X[6] NotX[7] NotX[9] NotX[12] NotX[13] + NotX[4] X[5] NotX[6] X[8] NotX[9] X[10] X[11] NotX[12] NotX[13] + NotX[1] NotX[3] X[4] X[7] NotX[9] X[10] X[11] NotX[12] NotX[13] + X[1] NotX[3] X[4] X[6] X[7] NotX[9] X[10] NotX[12] NotX[13] + NotX[3] X[4] NotX[6] NotX[7] NotX[8] X[9] X[11] NotX[12] NotX[13] + NotX[1] NotX[4] NotX[5] X[6] NotX[7] NotX[8] X[10] NotX[12] NotX[13] + X[1] NotX[2] NotX[3] NotX[6] X[7] NotX[8] X[11] NotX[12] NotX[13] + X[2] NotX[3] NotX[4] NotX[5] X[7] NotX[8] X[11] NotX[12] NotX[13] + X[1] NotX[5] X[6] NotX[8] X[9] X[10] X[11] NotX[12] NotX[13] + X[1] X[2] NotX[4] X[5] NotX[8] X[10] X[11] NotX[12] NotX[13] + X[1] NotX[2] NotX[5] NotX[8] NotX[9] X[10] NotX[11] NotX[12] NotX[13] + NotX[2] NotX[5] NotX[7] X[8] NotX[9] X[10] NotX[11] NotX[12] NotX[13] + NotX[1] X[2] NotX[3] X[4] NotX[6] NotX[9] NotX[11] NotX[12] NotX[13] + X[1] NotX[2] X[5] NotX[6] NotX[9] X[10] NotX[11] NotX[12] NotX[13] + X[2] NotX[6] X[7] X[8] NotX[9] X[10] NotX[11] NotX[12] NotX[13] + X[1] NotX[2] NotX[3] NotX[5] X[8] NotX[9] NotX[11] NotX[12] NotX[13] + X[2] X[4] NotX[5] X[6] X[7] NotX[9] NotX[11] NotX[12] NotX[13] + NotX[1] X[3] X[4] X[6] NotX[9] X[10] NotX[11] NotX[12] NotX[13] + X[2] NotX[5] NotX[6] NotX[7] NotX[8] X[9] NotX[11] NotX[12] NotX[13] + NotX[2] X[3] NotX[5] NotX[7] NotX[8] X[9] NotX[11] NotX[12] NotX[13] + X[1] X[2] NotX[4] NotX[8] X[9] X[10] NotX[11] NotX[12] NotX[13] + X[1] NotX[2] X[7] NotX[8] X[9] X[10] NotX[11] NotX[12] NotX[13] + X[2] X[4] NotX[5] NotX[6] NotX[7] X[8] NotX[11] NotX[12] NotX[13] + X[1] NotX[5] X[6] NotX[7] X[8] X[9] NotX[11] NotX[12] NotX[13] + NotX[2] X[4] X[5] NotX[7] X[9] X[10] NotX[11] NotX[12] NotX[13] + X[1] X[2] NotX[4] NotX[5] NotX[6] X[8] NotX[11] NotX[12] NotX[13] + X[1] NotX[2] NotX[3] NotX[6] X[8] X[9] NotX[11] NotX[12] NotX[13] + NotX[1] X[5] X[6] X[7] X[8] X[10] NotX[11] NotX[12] NotX[13] + X[2] X[4] X[5] X[7] X[8] X[10] NotX[11] NotX[12] NotX[13] + X[1] X[4] NotX[5] X[7] NotX[8] NotX[9] NotX[10] NotX[12] NotX[13] + NotX[2] NotX[5] X[6] NotX[7] X[8] NotX[9] NotX[10] NotX[12] NotX[13] + X[3] X[5] NotX[6] X[8] NotX[9] NotX[10] X[11] NotX[12] NotX[13] + NotX[2] X[5] X[6] X[7] NotX[9] NotX[10] X[11] NotX[12] NotX[13] + X[1] X[2] X[5] X[6] X[7] NotX[9] NotX[10] NotX[12] NotX[13] + X[2] X[4] X[5] X[6] NotX[7] NotX[8] NotX[10] NotX[12] NotX[13] + NotX[1] NotX[6] X[7] NotX[8] X[9] NotX[10] X[11] NotX[12] NotX[13] + NotX[2] NotX[3] X[4] X[5] NotX[6] NotX[7] NotX[8] X[9] NotX[11] + NotX[2] X[3] X[5] NotX[6] NotX[7] NotX[8] X[10] NotX[11] X[13] + X[3] X[4] NotX[6] NotX[7] NotX[8] X[9] X[10] NotX[11] X[12] + NotX[1] NotX[2] X[3] NotX[4] NotX[5] NotX[7] NotX[8] X[9] NotX[11] + X[1] NotX[4] NotX[5] X[6] NotX[7] NotX[8] NotX[11] X[12] X[13] + X[1] NotX[2] NotX[3] NotX[5] NotX[7] NotX[8] NotX[11] X[12] X[13] + NotX[1] X[4] X[5] X[6] NotX[7] NotX[8] X[9] NotX[11] X[13] + NotX[3] X[4] NotX[5] NotX[6] X[7] NotX[8] X[10] NotX[11] X[13] + NotX[1] X[2] X[3] NotX[5] NotX[6] X[7] NotX[8] NotX[11] X[12] + X[1] X[3] X[4] NotX[5] NotX[6] X[7] NotX[8] NotX[11] X[13] + NotX[2] X[3] NotX[4] X[5] NotX[6] X[7] NotX[8] X[10] NotX[11] + NotX[1] X[2] NotX[3] NotX[6] X[7] NotX[8] X[9] X[10] NotX[11] + NotX[1] X[2] X[3] X[5] NotX[6] NotX[8] X[9] NotX[11] X[13] + NotX[5] X[6] NotX[7] NotX[8] NotX[9] NotX[10] NotX[11] NotX[12] NotX[13] + X[1] NotX[3] X[5] NotX[6] NotX[9] NotX[10] NotX[11] NotX[12] NotX[13] + X[1] NotX[2] X[3] NotX[6] NotX[9] NotX[10] NotX[11] NotX[12] NotX[13] + NotX[1] X[2] X[3] NotX[4] NotX[8] NotX[10] NotX[11] NotX[12] NotX[13] + NotX[4] X[6] X[7] NotX[8] X[9] NotX[10] NotX[11] NotX[12] NotX[13] + NotX[1] X[3] X[4] X[5] NotX[8] NotX[10] NotX[11] NotX[12] NotX[13] + NotX[1] NotX[5] NotX[7] X[8] X[9] NotX[10] NotX[11] NotX[12] NotX[13] + X[1] X[2] NotX[4] NotX[5] X[6] NotX[10] NotX[11] NotX[12] NotX[13] + NotX[3] NotX[4] X[5] X[8] X[9] NotX[10] NotX[11] NotX[12] NotX[13] + NotX[3] NotX[4] X[6] X[7] X[8] NotX[10] NotX[11] NotX[12] NotX[13] + X[1] NotX[2] X[6] X[7] X[8] NotX[10] NotX[11] NotX[12] NotX[13] + NotX[1] X[2] X[3] X[6] X[8] NotX[10] NotX[11] NotX[12] NotX[13] + NotX[4] NotX[5] X[7] NotX[8] NotX[9] X[10] NotX[11] NotX[12] NotX[13] + NotX[1] X[2] X[3] X[5] NotX[6] NotX[8] NotX[9] NotX[11] X[12] + NotX[1] X[4] X[5] NotX[6] X[7] NotX[8] NotX[9] NotX[11] X[12] + X[2] NotX[4] NotX[5] X[6] X[7] NotX[8] NotX[9] X[10] NotX[11] + NotX[1] X[2] NotX[3] NotX[4] X[6] NotX[8] NotX[9] NotX[11] X[13] + NotX[2] X[3] X[4] X[5] NotX[6] NotX[7] NotX[9] NotX[11] X[12] + X[1] X[2] X[4] NotX[6] NotX[7] NotX[9] NotX[11] X[12] X[13] + X[1] X[3] NotX[4] NotX[5] NotX[7] X[8] NotX[9] NotX[11] X[13] + NotX[1] X[2] X[3] NotX[5] X[6] NotX[7] NotX[9] NotX[11] X[12] + X[1] X[3] X[4] NotX[5] NotX[7] X[8] NotX[9] NotX[11] X[12] + X[1] X[2] NotX[4] X[5] NotX[7] NotX[9] NotX[11] X[12] X[13] + X[1] NotX[2] NotX[3] NotX[7] X[8] NotX[9] X[10] NotX[11] X[12] + NotX[1] NotX[3] NotX[7] X[8] NotX[9] X[10] NotX[11] X[12] X[13] + X[1] X[3] X[5] NotX[7] NotX[9] X[10] NotX[11] X[12] X[13] + X[2] NotX[3] X[4] NotX[5] NotX[6] X[7] NotX[9] NotX[11] X[13] + NotX[1] X[3] NotX[5] NotX[6] X[7] X[8] NotX[9] X[10] NotX[11] + NotX[2] NotX[4] X[5] NotX[6] X[8] NotX[9] NotX[11] X[12] X[13] + NotX[1] NotX[2] X[3] NotX[4] NotX[5] X[7] NotX[9] NotX[11] X[12] + X[1] X[2] NotX[4] NotX[5] X[7] X[8] NotX[9] NotX[11] X[13] + NotX[1] X[2] NotX[3] NotX[4] X[7] X[8] NotX[9] X[10] NotX[11] + X[1] NotX[2] X[4] X[6] X[7] NotX[9] X[10] NotX[11] X[13] + NotX[1] X[3] X[4] X[5] X[6] X[7] NotX[9] NotX[11] X[12] + X[1] X[2] X[5] X[7] X[8] NotX[9] X[10] NotX[11] X[12] + X[2] X[3] X[6] X[7] NotX[9] X[10] NotX[11] X[12] X[13] + NotX[2] X[3] X[4] NotX[5] NotX[6] NotX[7] NotX[8] NotX[11] X[13] + NotX[1] NotX[5] NotX[6] NotX[7] NotX[8] X[9] X[10] NotX[11] X[13] ----------------------------------------------- The largest minimial size of monomials in DNF tautologies with, 14, variables, all of the same size, that is feasible (on density grounds is) , 9 Here is such a distinct DNF tautology with, 14, variales, each of size, 9 X[1] X[2] X[3] X[5] X[7] X[8] X[10] X[11] X[12] + X[1] X[2] X[4] X[5] X[7] X[10] X[11] X[12] X[14] + X[1] X[2] X[4] X[8] X[9] X[10] X[12] X[13] X[14] + X[1] X[3] X[4] X[5] X[6] X[7] X[8] X[13] X[14] + NotX[1] NotX[2] X[3] NotX[4] NotX[5] X[6] X[10] X[13] X[14] + X[1] X[2] NotX[4] NotX[5] X[6] X[8] X[10] X[11] X[14] + NotX[1] NotX[2] NotX[3] X[4] NotX[5] X[7] X[8] X[9] X[14] + NotX[1] X[2] NotX[3] NotX[5] X[7] X[8] X[11] X[13] X[14] + X[1] X[2] NotX[3] NotX[5] X[6] X[7] X[9] X[11] X[14] + X[1] NotX[3] X[4] NotX[5] X[6] X[7] X[8] X[10] X[13] + X[1] NotX[3] X[4] NotX[5] X[6] X[8] X[9] X[11] X[14] + NotX[1] NotX[2] X[3] X[4] NotX[5] X[7] X[8] X[12] X[13] + X[1] NotX[2] X[3] NotX[5] X[7] X[9] X[12] X[13] X[14] + X[1] X[2] X[3] NotX[5] X[6] X[9] X[11] X[12] X[14] + X[1] X[3] X[4] NotX[5] X[6] X[7] X[8] X[10] X[12] + NotX[1] NotX[2] NotX[3] NotX[4] X[5] X[6] X[10] X[11] X[13] + NotX[1] NotX[2] X[3] NotX[4] X[5] X[7] X[12] X[13] X[14] + X[1] NotX[2] NotX[4] X[5] X[6] X[9] X[10] X[12] X[14] + X[1] NotX[2] NotX[4] X[6] X[7] X[10] X[12] X[13] X[14] + NotX[1] X[2] X[3] NotX[4] X[6] X[7] X[9] X[11] X[14] + X[1] X[2] NotX[4] X[5] X[8] X[9] X[12] X[13] X[14] + NotX[1] NotX[2] NotX[3] X[5] X[8] X[9] X[11] X[12] X[13] + X[1] NotX[2] NotX[3] X[4] X[7] X[8] X[10] X[12] X[14] + NotX[1] X[2] NotX[3] X[4] X[9] X[10] X[11] X[12] X[13] + NotX[1] NotX[2] X[3] X[4] X[5] X[7] X[9] X[13] X[14] + X[1] NotX[2] X[3] X[4] X[10] X[11] X[12] X[13] X[14] + NotX[1] X[2] X[3] X[8] X[9] X[11] X[12] X[13] X[14] + NotX[1] X[2] X[5] X[6] X[8] X[10] X[12] X[13] X[14] + NotX[1] X[2] X[5] X[9] X[10] X[11] X[12] X[13] X[14] + NotX[1] NotX[2] NotX[3] X[4] NotX[5] NotX[7] X[8] X[13] X[14] + NotX[1] NotX[3] X[4] NotX[5] X[6] NotX[7] X[10] X[11] X[13] + X[1] X[2] NotX[3] NotX[5] X[6] NotX[7] X[11] X[12] X[13] + NotX[1] NotX[2] X[4] NotX[5] NotX[7] X[8] X[9] X[11] X[14] + NotX[1] X[2] X[4] NotX[5] NotX[7] X[10] X[11] X[12] X[13] + NotX[1] NotX[2] X[3] NotX[4] X[5] NotX[7] X[11] X[13] X[14] + X[1] NotX[2] X[3] NotX[4] NotX[7] X[10] X[12] X[13] X[14] + NotX[1] X[2] X[3] NotX[4] X[6] NotX[7] X[11] X[12] X[13] + X[1] NotX[2] NotX[3] X[4] NotX[7] X[8] X[9] X[10] X[13] + X[1] NotX[2] NotX[3] X[6] NotX[7] X[9] X[10] X[12] X[14] + NotX[1] NotX[2] X[3] X[4] X[5] NotX[7] X[9] X[12] X[14] + NotX[1] NotX[2] X[6] NotX[7] X[9] X[10] X[12] X[13] X[14] + X[1] NotX[2] X[4] X[5] X[6] NotX[7] X[8] X[13] X[14] + X[1] X[2] X[3] X[5] NotX[7] X[8] X[9] X[11] X[14] + X[1] X[3] NotX[4] NotX[5] NotX[6] X[8] X[10] X[11] X[13] + X[1] X[2] NotX[3] NotX[5] NotX[6] X[7] X[9] X[10] X[13] + NotX[1] NotX[2] NotX[5] NotX[6] X[9] X[10] X[11] X[12] X[14] + X[1] X[2] X[3] NotX[5] NotX[6] X[8] X[10] X[11] X[14] + X[1] NotX[2] NotX[3] NotX[4] NotX[6] X[8] X[11] X[12] X[13] + NotX[1] X[2] X[3] NotX[4] NotX[6] X[7] X[9] X[10] X[13] + X[1] X[2] NotX[4] NotX[6] X[7] X[8] X[11] X[12] X[14] + X[1] X[2] NotX[3] X[5] NotX[6] X[9] X[10] X[12] X[14] + NotX[1] NotX[2] X[4] X[5] NotX[6] X[8] X[9] X[11] X[14] + X[1] NotX[2] NotX[6] X[7] X[10] X[11] X[12] X[13] X[14] + NotX[1] NotX[2] NotX[3] NotX[4] NotX[5] X[6] X[8] X[9] X[11] + NotX[1] NotX[2] NotX[3] X[4] NotX[5] NotX[6] NotX[8] X[13] X[14] + NotX[1] NotX[2] X[4] NotX[5] NotX[6] X[7] NotX[8] X[10] X[14] + X[1] NotX[2] NotX[3] NotX[4] NotX[6] NotX[8] X[10] X[12] X[13] + NotX[1] NotX[2] NotX[3] X[4] X[5] NotX[6] NotX[8] X[11] X[13] + NotX[1] X[2] X[3] NotX[6] X[7] NotX[8] X[10] X[12] X[14] + X[1] X[2] X[3] NotX[6] NotX[8] X[9] X[10] X[12] X[14] + NotX[1] NotX[2] NotX[4] NotX[5] X[6] NotX[8] X[9] X[10] X[11] + NotX[1] NotX[2] NotX[3] X[4] NotX[5] X[6] NotX[8] X[10] X[12] + NotX[1] NotX[2] NotX[5] X[6] X[7] NotX[8] X[11] X[13] X[14] + NotX[1] X[2] X[4] NotX[5] X[7] NotX[8] X[10] X[11] X[13] + NotX[1] X[2] NotX[3] NotX[4] X[5] NotX[8] X[9] X[13] X[14] + X[1] NotX[2] NotX[4] X[7] NotX[8] X[9] X[10] X[11] X[13] + NotX[1] X[2] NotX[4] X[7] NotX[8] X[11] X[12] X[13] X[14] + X[1] X[2] NotX[4] X[7] NotX[8] X[10] X[11] X[12] X[14] + X[1] NotX[2] NotX[3] X[4] X[7] NotX[8] X[10] X[11] X[14] + NotX[1] NotX[3] X[4] X[5] X[6] X[7] NotX[8] X[9] X[11] + X[1] X[2] NotX[3] X[5] X[6] NotX[8] X[9] X[12] X[13] + NotX[1] X[2] X[3] X[4] X[6] NotX[8] X[9] X[11] X[12] + X[1] X[2] NotX[3] NotX[5] NotX[6] NotX[7] X[8] X[12] X[13] + NotX[1] NotX[2] X[4] NotX[5] NotX[6] NotX[7] X[8] X[10] X[12] + NotX[1] NotX[2] NotX[5] NotX[6] NotX[7] X[8] X[9] X[11] X[13] + NotX[1] X[2] X[3] NotX[4] NotX[6] NotX[7] X[8] X[12] X[13] + NotX[1] NotX[3] X[4] X[5] NotX[6] NotX[7] X[10] X[11] X[14] + NotX[1] X[2] NotX[3] NotX[4] NotX[5] NotX[7] X[10] X[12] X[13] + X[1] X[2] X[3] X[5] NotX[7] X[8] NotX[9] X[10] X[13] + NotX[1] NotX[2] X[3] NotX[4] NotX[5] NotX[6] NotX[9] X[13] X[14] + X[1] X[2] NotX[4] NotX[5] NotX[6] X[7] X[8] NotX[9] X[13] + X[1] X[2] X[4] NotX[5] NotX[6] X[8] NotX[9] X[10] X[13] + NotX[1] NotX[2] NotX[6] X[8] NotX[9] X[10] X[11] X[12] X[13] + X[1] NotX[2] X[5] NotX[6] NotX[9] X[10] X[12] X[13] X[14] + NotX[1] X[2] X[3] NotX[6] X[7] X[8] NotX[9] X[10] X[13] + X[1] X[3] X[4] X[5] NotX[6] X[7] X[8] NotX[9] X[12] + NotX[1] NotX[2] NotX[4] NotX[5] X[6] X[7] NotX[9] X[10] X[13] + NotX[1] NotX[2] NotX[3] X[4] NotX[5] X[7] X[8] NotX[9] X[13] + NotX[1] NotX[2] NotX[5] X[6] NotX[9] X[10] X[11] X[13] X[14] + X[1] X[2] X[4] NotX[5] X[6] NotX[9] X[10] X[11] X[13] + X[1] NotX[2] NotX[3] NotX[4] X[6] NotX[9] X[11] X[12] X[14] + NotX[1] NotX[2] NotX[3] X[4] X[5] X[6] NotX[9] X[10] X[12] + NotX[1] X[2] NotX[3] X[4] X[5] NotX[9] X[11] X[12] X[13] + NotX[1] X[2] NotX[3] X[5] X[8] NotX[9] X[10] X[11] X[14] + X[1] X[2] NotX[3] X[5] X[6] X[8] NotX[9] X[13] X[14] + NotX[1] NotX[2] X[4] X[5] X[7] NotX[9] X[10] X[11] X[12] + NotX[1] X[2] X[3] X[4] X[6] X[8] NotX[9] X[12] X[14] + NotX[1] X[2] X[3] X[6] X[7] X[8] NotX[9] X[10] X[14] + X[1] X[2] NotX[3] NotX[5] NotX[6] NotX[7] NotX[8] X[10] X[11] + NotX[1] X[2] X[3] NotX[4] NotX[6] NotX[7] NotX[8] X[10] X[11] + X[1] NotX[2] X[4] NotX[6] NotX[7] NotX[8] X[9] X[10] X[11] + NotX[1] NotX[2] X[3] X[4] NotX[5] NotX[7] NotX[8] X[10] X[11] + X[1] X[2] NotX[4] NotX[7] NotX[8] X[9] X[11] X[13] X[14] + X[1] X[2] X[3] X[5] NotX[7] NotX[8] X[9] X[11] X[12] + X[1] X[2] NotX[4] X[5] X[6] X[7] X[9] NotX[10] X[12] + NotX[1] X[2] NotX[3] X[4] X[8] X[9] NotX[10] X[11] X[12] + X[1] NotX[2] X[3] X[5] X[7] X[9] NotX[10] X[12] X[13] + X[1] NotX[2] X[4] X[6] X[7] X[8] NotX[10] X[12] X[14] + X[1] NotX[2] X[4] X[7] X[8] NotX[10] X[11] X[12] X[13] + NotX[1] X[2] X[4] X[7] X[9] NotX[10] X[12] X[13] X[14] + X[1] X[2] X[4] X[5] X[8] X[9] NotX[10] X[12] X[14] + X[1] X[2] NotX[4] X[6] NotX[7] NotX[8] NotX[9] X[13] X[14] + X[1] NotX[2] NotX[3] X[4] NotX[7] NotX[8] NotX[9] X[10] X[11] + X[1] X[2] X[3] X[5] NotX[7] NotX[8] NotX[9] X[10] X[11] + X[1] X[2] X[3] NotX[5] NotX[6] NotX[8] NotX[9] X[11] X[12] + X[1] X[2] NotX[3] NotX[5] X[7] NotX[8] NotX[9] X[10] X[14] + NotX[1] X[2] NotX[3] NotX[4] X[5] NotX[8] NotX[9] X[11] X[12] + NotX[1] X[2] X[3] NotX[4] X[7] NotX[8] NotX[9] X[10] X[14] + X[1] X[2] NotX[3] X[5] X[6] NotX[8] NotX[9] X[11] X[14] + NotX[1] X[2] X[4] X[5] X[6] NotX[8] NotX[9] X[10] X[14] + X[1] X[2] X[3] X[5] X[7] NotX[8] NotX[9] X[12] X[13] + X[1] X[2] NotX[3] X[5] NotX[6] NotX[7] NotX[9] X[11] X[12] + NotX[1] X[2] X[3] X[4] NotX[6] NotX[7] NotX[9] X[11] X[12] + NotX[1] NotX[2] NotX[3] NotX[4] NotX[5] X[6] NotX[7] NotX[9] X[14] + X[1] NotX[2] X[4] NotX[5] NotX[7] X[8] NotX[9] X[12] X[14] + NotX[1] X[2] X[4] NotX[5] X[6] NotX[7] NotX[9] X[10] X[14] + X[1] X[2] NotX[5] X[6] NotX[7] X[8] NotX[9] X[12] X[13] + X[1] X[2] NotX[5] X[6] NotX[7] NotX[9] X[11] X[12] X[14] + NotX[1] NotX[2] NotX[3] NotX[7] X[8] NotX[9] X[11] X[12] X[13] + NotX[1] NotX[2] X[3] X[4] X[5] NotX[7] NotX[9] X[11] X[12] + NotX[1] NotX[2] X[4] NotX[5] X[6] NotX[8] X[9] NotX[10] X[12] + X[1] X[2] NotX[5] X[7] NotX[8] NotX[10] X[12] X[13] X[14] + NotX[1] NotX[2] NotX[3] X[6] NotX[8] X[9] NotX[10] X[11] X[12] + X[1] NotX[2] NotX[3] X[7] NotX[8] NotX[10] X[11] X[13] X[14] + X[1] NotX[2] X[4] X[5] NotX[8] X[9] NotX[10] X[13] X[14] + X[1] X[2] X[3] X[5] X[7] NotX[8] NotX[10] X[11] X[14] + X[1] X[2] X[4] NotX[8] X[9] NotX[10] X[11] X[12] X[13] + NotX[1] X[2] NotX[3] NotX[4] NotX[5] NotX[7] NotX[10] X[11] X[12] + NotX[1] NotX[2] X[3] X[4] NotX[5] NotX[7] X[8] NotX[10] X[12] + X[1] NotX[2] X[3] NotX[5] NotX[7] X[8] NotX[10] X[13] X[14] + X[1] NotX[2] X[4] NotX[5] X[6] NotX[7] NotX[10] X[13] X[14] + NotX[1] X[2] X[4] NotX[5] NotX[7] X[8] NotX[10] X[11] X[12] + X[1] NotX[2] NotX[4] X[5] NotX[7] NotX[10] X[12] X[13] X[14] + X[1] NotX[2] NotX[3] X[4] NotX[7] NotX[10] X[11] X[12] X[14] + NotX[1] X[2] X[4] X[5] NotX[7] X[9] NotX[10] X[12] X[14] + X[1] X[2] X[3] NotX[5] NotX[6] X[8] NotX[10] X[11] X[12] + X[1] X[2] NotX[5] NotX[6] X[7] X[8] NotX[10] X[12] X[13] + X[1] X[2] NotX[3] X[5] NotX[6] X[7] NotX[10] X[12] X[13] + X[1] NotX[2] X[4] X[5] NotX[6] X[8] NotX[10] X[12] X[14] + NotX[1] X[2] X[3] X[4] NotX[6] X[7] NotX[10] X[13] X[14] + NotX[1] NotX[2] X[3] NotX[4] NotX[5] X[9] NotX[10] X[11] X[12] + X[1] NotX[2] X[4] NotX[5] X[7] X[8] X[9] NotX[10] X[13] + X[1] X[2] X[4] NotX[5] X[7] X[8] X[9] NotX[10] X[12] + X[1] NotX[2] NotX[3] NotX[4] X[6] X[9] NotX[10] X[12] X[14] + NotX[1] X[2] NotX[3] NotX[4] X[5] X[8] NotX[10] X[13] X[14] + NotX[1] NotX[3] NotX[4] X[5] X[6] X[7] NotX[10] X[11] X[12] + NotX[1] NotX[3] NotX[4] NotX[5] NotX[6] NotX[7] NotX[9] NotX[10] X[14] + X[1] X[2] X[3] X[5] NotX[7] NotX[9] NotX[10] X[11] X[13] + NotX[1] NotX[2] X[5] NotX[6] X[7] X[8] NotX[9] NotX[10] X[12] + NotX[1] X[2] NotX[6] X[7] X[8] NotX[9] NotX[10] X[11] X[12] + NotX[1] NotX[2] NotX[3] NotX[4] NotX[5] X[6] X[7] NotX[9] NotX[10] + X[1] X[2] NotX[3] NotX[5] X[6] X[7] NotX[9] NotX[10] X[14] + NotX[1] NotX[2] NotX[4] X[6] NotX[9] NotX[10] X[11] X[12] X[13] + X[1] NotX[2] X[3] NotX[4] X[7] NotX[9] NotX[10] X[12] X[13] + NotX[1] X[2] X[3] NotX[4] X[6] X[7] NotX[9] NotX[10] X[14] + NotX[1] NotX[2] NotX[3] X[4] X[5] X[6] NotX[9] NotX[10] X[11] + NotX[1] NotX[2] X[3] X[7] NotX[9] NotX[10] X[11] X[12] X[14] + X[1] X[2] X[3] X[6] X[7] X[8] NotX[9] NotX[10] X[12] + X[1] X[2] NotX[5] NotX[6] NotX[7] NotX[8] X[9] NotX[10] X[11] + NotX[1] X[2] X[3] NotX[6] NotX[7] NotX[8] X[9] NotX[10] X[11] + X[1] NotX[2] NotX[5] NotX[7] NotX[8] NotX[10] X[11] X[12] X[13] + NotX[1] NotX[2] NotX[4] X[6] NotX[7] NotX[8] NotX[10] X[11] X[14] + X[1] NotX[2] X[3] NotX[4] NotX[7] NotX[8] NotX[10] X[13] X[14] + X[1] X[2] NotX[4] X[5] NotX[7] NotX[8] X[9] NotX[10] X[14] + X[1] X[2] X[4] X[5] NotX[7] NotX[8] NotX[10] X[11] X[14] + X[1] X[2] NotX[3] NotX[5] NotX[6] X[7] NotX[8] NotX[10] X[14] + NotX[1] NotX[2] NotX[5] NotX[6] NotX[8] X[9] NotX[10] X[11] X[13] + X[1] NotX[3] NotX[4] X[5] NotX[6] X[7] NotX[8] NotX[10] X[11] + X[1] NotX[2] NotX[4] NotX[6] NotX[8] X[9] NotX[10] X[12] X[14] + NotX[1] X[2] X[3] NotX[4] NotX[6] X[7] NotX[8] NotX[10] X[14] + NotX[1] X[2] NotX[3] X[4] NotX[5] NotX[8] NotX[10] X[12] X[13] + X[1] NotX[2] NotX[3] NotX[4] NotX[6] X[8] NotX[11] X[12] X[14] + NotX[1] NotX[2] NotX[3] X[4] X[5] NotX[6] X[8] NotX[11] X[14] + NotX[1] NotX[2] X[5] NotX[6] X[7] X[8] X[10] NotX[11] X[14] + X[1] NotX[2] X[3] NotX[6] X[10] NotX[11] X[12] X[13] X[14] + NotX[1] X[2] X[5] NotX[6] X[7] X[8] NotX[11] X[12] X[14] + NotX[1] NotX[2] NotX[3] NotX[4] NotX[5] X[6] X[7] X[9] NotX[11] + NotX[1] X[2] NotX[3] NotX[4] NotX[5] X[7] NotX[11] X[12] X[13] + NotX[1] X[2] NotX[3] X[4] NotX[5] X[8] NotX[11] X[13] X[14] + X[1] X[2] NotX[3] NotX[5] X[6] X[7] X[9] NotX[11] X[13] + X[1] X[3] X[4] NotX[5] X[6] X[8] NotX[11] X[12] X[13] + NotX[1] NotX[2] NotX[4] X[5] X[6] X[10] NotX[11] X[13] X[14] + NotX[1] X[2] X[3] NotX[4] X[6] X[7] X[9] NotX[11] X[13] + X[1] X[3] NotX[4] X[5] X[6] X[7] X[9] NotX[11] X[14] + NotX[1] NotX[2] NotX[3] X[4] X[5] X[6] X[9] NotX[11] X[12] + NotX[1] X[2] NotX[3] X[9] X[10] NotX[11] X[12] X[13] X[14] + NotX[1] X[2] X[3] X[6] X[7] X[8] X[9] NotX[11] X[12] + X[1] X[2] X[3] X[6] X[7] X[8] X[10] NotX[11] X[14] + X[1] X[2] NotX[3] NotX[5] NotX[6] NotX[7] NotX[8] NotX[9] NotX[10] + NotX[1] X[2] X[3] NotX[4] NotX[6] NotX[7] NotX[8] NotX[9] NotX[10] + NotX[1] NotX[2] X[3] X[4] NotX[5] NotX[7] NotX[8] NotX[9] NotX[10] + X[1] NotX[2] X[4] X[6] NotX[7] NotX[8] NotX[9] NotX[10] X[14] + NotX[1] NotX[2] NotX[3] X[4] NotX[5] X[6] NotX[8] NotX[9] NotX[10] + NotX[1] NotX[3] NotX[4] X[5] X[6] X[7] NotX[8] NotX[9] NotX[10] + X[1] X[2] NotX[4] X[5] X[6] X[7] NotX[8] NotX[9] NotX[10] + X[1] NotX[2] X[3] X[4] NotX[8] NotX[9] NotX[10] X[13] X[14] + NotX[1] X[2] X[3] X[4] X[6] NotX[8] NotX[9] NotX[10] X[13] + X[1] X[2] X[3] X[5] NotX[7] NotX[8] NotX[11] X[12] X[13] + NotX[1] NotX[2] X[4] X[5] NotX[6] NotX[8] X[10] NotX[11] X[13] + NotX[1] NotX[2] X[4] NotX[5] X[7] NotX[8] NotX[11] X[13] X[14] + X[1] X[2] X[3] NotX[5] X[6] NotX[8] NotX[11] X[12] X[14] + NotX[1] NotX[2] NotX[4] X[5] X[6] X[7] NotX[8] NotX[11] X[12] + X[1] NotX[2] NotX[3] X[4] NotX[8] X[10] NotX[11] X[12] X[14] + NotX[1] NotX[2] X[5] X[7] NotX[8] X[10] NotX[11] X[13] X[14] + X[1] NotX[2] X[3] X[4] NotX[8] X[9] NotX[11] X[13] X[14] + NotX[1] X[2] X[3] X[4] X[6] NotX[8] X[9] NotX[11] X[13] + X[1] X[2] X[4] X[5] X[6] NotX[8] NotX[11] X[12] X[14] + NotX[1] NotX[3] NotX[4] X[5] NotX[6] NotX[7] X[9] NotX[11] X[12] + NotX[1] NotX[2] NotX[4] X[5] NotX[6] NotX[7] X[9] NotX[11] X[13] + X[1] NotX[2] X[4] NotX[6] NotX[7] X[8] X[9] NotX[11] X[14] + NotX[1] X[2] X[3] X[4] NotX[6] NotX[7] X[10] NotX[11] X[12] + NotX[1] NotX[2] NotX[4] NotX[5] X[6] NotX[7] X[9] NotX[11] X[14] + X[1] X[2] NotX[3] NotX[5] X[6] NotX[7] NotX[11] X[12] X[14] + NotX[1] NotX[2] NotX[3] NotX[4] X[5] X[6] NotX[7] NotX[11] X[14] + NotX[1] X[2] X[3] NotX[4] X[6] NotX[7] NotX[11] X[12] X[14] + NotX[1] X[2] X[4] X[6] NotX[7] X[9] NotX[11] X[12] X[14] + X[1] X[2] X[3] X[6] NotX[7] X[8] NotX[11] X[12] X[14] + NotX[1] NotX[2] NotX[4] NotX[5] NotX[6] X[9] NotX[11] X[12] X[14] + NotX[1] X[3] X[4] NotX[5] NotX[6] X[7] NotX[11] X[12] X[13] + X[1] X[2] X[3] NotX[5] NotX[6] X[8] NotX[11] X[12] X[13] + X[1] X[2] NotX[5] NotX[6] X[8] X[9] X[10] NotX[11] X[14] + X[1] X[3] X[4] NotX[5] NotX[6] X[7] X[8] NotX[11] X[13] + NotX[1] X[2] NotX[4] NotX[7] NotX[8] NotX[9] X[10] NotX[11] X[14] + X[1] X[3] X[4] NotX[5] NotX[6] NotX[8] NotX[9] X[10] NotX[11] + X[1] X[2] X[4] NotX[6] NotX[8] NotX[9] X[10] NotX[11] X[14] + NotX[1] X[2] NotX[5] NotX[8] NotX[9] X[10] NotX[11] X[13] X[14] + NotX[1] X[2] NotX[3] X[7] NotX[8] NotX[9] X[10] NotX[11] X[14] + X[1] X[2] NotX[4] NotX[6] NotX[7] NotX[9] X[10] NotX[11] X[13] + NotX[1] NotX[2] NotX[6] NotX[7] NotX[9] X[10] NotX[11] X[12] X[14] + NotX[1] NotX[2] X[4] NotX[5] X[6] NotX[7] NotX[9] X[10] NotX[11] + NotX[1] NotX[2] X[3] X[5] NotX[7] NotX[9] NotX[11] X[12] X[14] + NotX[1] NotX[2] X[4] X[5] X[6] NotX[7] X[8] NotX[9] NotX[11] + NotX[1] X[2] X[4] X[6] NotX[7] X[8] NotX[9] NotX[11] X[13] + NotX[1] X[2] NotX[4] X[5] NotX[6] NotX[9] X[10] NotX[11] X[12] + X[1] X[2] NotX[5] X[6] X[7] NotX[9] X[10] NotX[11] X[14] + X[1] NotX[2] NotX[3] NotX[4] X[6] NotX[9] X[10] NotX[11] X[12] + X[1] X[2] NotX[4] X[7] NotX[9] X[10] NotX[11] X[12] X[13] + NotX[1] X[2] NotX[3] X[4] X[5] NotX[9] NotX[11] X[12] X[14] + X[1] X[2] NotX[3] X[5] NotX[9] X[10] NotX[11] X[12] X[14] + NotX[1] NotX[2] X[5] X[7] X[8] NotX[9] NotX[11] X[12] X[14] + X[1] NotX[2] X[3] X[6] X[7] NotX[9] NotX[11] X[12] X[14] + X[1] X[2] X[5] X[6] X[7] NotX[9] X[10] NotX[11] X[13] + X[1] X[3] X[4] X[5] X[6] NotX[9] X[10] NotX[11] X[12] + NotX[1] NotX[2] NotX[4] NotX[5] NotX[6] NotX[7] NotX[8] X[10] NotX[11] + X[1] X[2] NotX[3] NotX[5] NotX[6] NotX[7] NotX[8] X[9] NotX[11] + NotX[1] X[2] X[3] NotX[4] NotX[6] NotX[7] NotX[8] X[9] NotX[11] + NotX[1] NotX[2] X[3] X[4] NotX[5] NotX[7] NotX[8] X[9] NotX[11] + X[1] NotX[2] X[6] NotX[7] NotX[8] X[10] NotX[11] X[13] X[14] + X[1] NotX[2] NotX[3] NotX[4] NotX[6] NotX[8] NotX[9] NotX[10] NotX[11] + NotX[1] X[2] NotX[3] NotX[4] X[5] NotX[8] NotX[9] NotX[10] NotX[11] + NotX[1] NotX[2] X[4] X[6] NotX[8] NotX[9] NotX[10] NotX[11] X[12] + X[1] X[2] NotX[3] X[5] NotX[6] NotX[7] NotX[9] NotX[10] NotX[11] + NotX[1] NotX[2] NotX[6] NotX[7] X[8] NotX[9] NotX[10] NotX[11] X[13] + NotX[1] X[2] X[3] X[4] NotX[6] NotX[7] NotX[9] NotX[10] NotX[11] + NotX[1] X[2] NotX[4] NotX[5] NotX[9] NotX[10] NotX[11] X[12] X[13] + X[1] NotX[2] NotX[3] NotX[4] X[6] NotX[9] NotX[10] NotX[11] X[13] + X[1] NotX[2] NotX[3] X[6] X[7] NotX[9] NotX[10] NotX[11] X[14] + NotX[1] NotX[2] X[3] X[4] X[5] X[7] NotX[9] NotX[10] NotX[11] + X[1] NotX[2] X[4] X[8] NotX[9] NotX[10] NotX[11] X[13] X[14] + NotX[1] X[2] NotX[4] NotX[5] NotX[7] NotX[8] X[9] NotX[10] NotX[11] + NotX[1] NotX[2] NotX[3] X[4] X[5] NotX[6] NotX[8] NotX[10] NotX[11] + X[1] X[2] X[3] NotX[6] NotX[8] X[9] NotX[10] NotX[11] X[13] + X[1] NotX[2] X[4] NotX[8] X[9] NotX[10] NotX[11] X[12] X[14] + X[1] NotX[3] X[4] X[5] NotX[6] NotX[7] X[9] NotX[10] NotX[11] + NotX[1] X[2] NotX[6] NotX[7] X[9] NotX[10] NotX[11] X[12] X[13] + NotX[1] NotX[2] NotX[4] X[5] X[6] NotX[7] NotX[10] NotX[11] X[13] + NotX[1] X[2] NotX[3] NotX[7] X[8] X[9] NotX[10] NotX[11] X[13] + X[1] NotX[2] NotX[3] X[4] NotX[6] NotX[10] NotX[11] X[12] X[14] + NotX[1] NotX[2] X[3] NotX[4] NotX[5] X[6] NotX[10] NotX[11] X[12] + NotX[1] X[2] NotX[4] NotX[5] X[7] NotX[10] NotX[11] X[13] X[14] + X[1] X[3] NotX[4] NotX[5] X[6] X[8] NotX[10] NotX[11] X[14] + NotX[1] NotX[2] NotX[4] X[5] X[6] X[7] NotX[10] NotX[11] X[14] + NotX[1] NotX[2] X[7] X[8] X[9] NotX[10] NotX[11] X[12] X[14] + X[1] X[2] X[3] X[5] X[8] NotX[10] NotX[11] X[12] X[13] + NotX[1] X[2] X[3] NotX[4] X[6] NotX[7] X[8] NotX[12] X[14] + NotX[1] NotX[2] X[5] X[6] NotX[7] X[9] X[11] NotX[12] X[13] + X[1] NotX[2] NotX[7] X[8] X[10] X[11] NotX[12] X[13] X[14] + NotX[1] X[2] X[5] NotX[7] X[8] X[11] NotX[12] X[13] X[14] + X[1] X[2] X[4] X[6] NotX[7] X[9] X[11] NotX[12] X[13] + NotX[1] NotX[2] X[3] NotX[4] NotX[5] NotX[6] X[9] NotX[12] X[14] + NotX[1] NotX[2] NotX[4] NotX[5] NotX[6] X[7] X[8] NotX[12] X[13] + NotX[1] X[2] X[4] NotX[5] NotX[6] X[9] X[10] NotX[12] X[13] + X[1] NotX[2] NotX[3] NotX[4] NotX[6] X[8] X[10] NotX[12] X[14] + X[1] X[2] NotX[3] X[5] NotX[6] X[7] X[10] NotX[12] X[14] + X[1] NotX[2] X[3] NotX[6] X[9] X[10] X[11] NotX[12] X[13] + NotX[1] X[2] X[4] X[5] NotX[6] X[7] X[9] NotX[12] X[13] + NotX[1] X[2] NotX[3] NotX[4] NotX[5] X[9] X[10] NotX[12] X[13] + X[1] X[2] NotX[5] X[6] X[8] X[10] X[11] NotX[12] X[14] + X[1] NotX[2] X[3] NotX[4] X[7] X[9] NotX[12] X[13] X[14] + NotX[1] NotX[2] NotX[3] X[5] X[9] X[11] NotX[12] X[13] X[14] + X[1] NotX[2] NotX[3] X[4] X[7] X[8] X[10] X[11] NotX[12] + X[1] NotX[2] NotX[3] X[6] X[7] X[11] NotX[12] X[13] X[14] + NotX[1] X[2] NotX[3] X[5] X[8] X[9] X[10] NotX[12] X[13] + X[1] X[2] NotX[3] X[5] X[6] X[9] NotX[12] X[13] X[14] + NotX[1] NotX[2] X[3] X[7] X[9] X[11] NotX[12] X[13] X[14] + X[1] NotX[2] X[3] X[6] X[9] X[10] X[11] NotX[12] X[14] + NotX[1] X[2] X[3] X[4] X[6] X[8] X[9] NotX[12] X[13] + NotX[1] X[2] X[4] X[5] X[6] X[7] X[11] NotX[12] X[14] + X[1] X[2] X[3] X[5] X[7] X[8] X[11] NotX[12] X[14] + X[1] X[2] X[3] NotX[5] NotX[6] NotX[8] NotX[9] NotX[10] NotX[11] + X[1] NotX[2] X[3] X[4] NotX[9] X[10] NotX[12] X[13] X[14] + X[1] NotX[2] X[6] X[7] X[8] NotX[9] X[11] NotX[12] X[14] + X[1] NotX[2] NotX[4] NotX[5] NotX[7] NotX[8] X[10] NotX[12] X[13] + X[1] NotX[2] NotX[4] X[5] NotX[7] NotX[8] X[9] NotX[12] X[13] + X[1] NotX[2] NotX[3] X[4] NotX[7] NotX[8] X[9] X[10] NotX[12] + NotX[1] NotX[2] X[3] X[4] X[5] NotX[7] NotX[8] NotX[12] X[14] + NotX[1] X[2] X[3] X[6] NotX[7] NotX[8] X[11] NotX[12] X[13] + X[1] X[2] X[3] X[5] NotX[7] NotX[8] X[9] X[10] NotX[12] + X[1] X[3] NotX[4] NotX[5] NotX[6] NotX[8] X[10] X[11] NotX[12] + X[1] NotX[3] NotX[4] X[5] NotX[6] NotX[8] X[9] X[10] NotX[12] + X[1] X[3] NotX[4] X[5] NotX[6] NotX[8] X[10] NotX[12] X[14] + NotX[1] NotX[2] NotX[3] X[4] NotX[5] X[6] NotX[8] X[9] NotX[12] + NotX[1] X[2] NotX[3] X[4] NotX[5] NotX[8] X[10] NotX[12] X[14] + X[1] X[2] X[3] NotX[5] NotX[8] X[9] X[10] NotX[12] X[14] + NotX[1] X[2] X[4] X[6] NotX[8] X[9] NotX[12] X[13] X[14] + X[1] X[2] X[3] X[5] X[7] NotX[8] X[10] NotX[12] X[14] + X[1] X[2] NotX[3] NotX[6] NotX[7] X[8] X[9] NotX[12] X[13] + NotX[1] X[2] X[3] NotX[6] NotX[7] X[8] X[9] NotX[12] X[14] + NotX[1] X[2] X[4] X[5] NotX[6] NotX[7] NotX[12] X[13] X[14] + X[1] X[2] X[5] NotX[6] NotX[7] X[9] X[10] X[11] NotX[12] + X[1] NotX[2] NotX[4] NotX[5] X[6] NotX[7] X[10] NotX[12] X[14] + NotX[1] NotX[3] X[4] NotX[5] X[6] NotX[7] X[8] NotX[12] X[13] + X[1] X[2] NotX[3] NotX[5] X[6] NotX[7] X[8] NotX[12] X[14] + NotX[1] X[3] X[4] NotX[5] X[6] NotX[7] X[11] NotX[12] X[14] + NotX[1] NotX[3] NotX[4] X[5] X[6] NotX[7] X[9] NotX[12] X[14] + X[1] NotX[2] NotX[3] NotX[4] NotX[6] NotX[8] NotX[9] X[10] NotX[12] + X[1] NotX[3] X[4] NotX[5] X[6] NotX[8] NotX[9] X[11] NotX[12] + NotX[1] X[2] NotX[3] NotX[4] X[5] NotX[8] NotX[9] X[10] NotX[12] + NotX[1] X[2] NotX[3] X[7] NotX[8] NotX[9] X[10] X[11] NotX[12] + NotX[1] X[2] X[7] NotX[8] NotX[9] X[10] NotX[12] X[13] X[14] + X[1] X[2] NotX[3] NotX[5] NotX[6] NotX[7] X[8] NotX[9] NotX[12] + NotX[1] NotX[2] NotX[3] NotX[4] X[5] NotX[6] NotX[7] NotX[9] NotX[12] + NotX[1] X[2] X[3] NotX[4] NotX[6] NotX[7] X[8] NotX[9] NotX[12] + X[1] X[2] NotX[3] X[5] NotX[6] NotX[7] NotX[9] X[10] NotX[12] + NotX[1] NotX[2] X[4] X[5] NotX[6] NotX[7] X[8] NotX[9] NotX[12] + NotX[1] X[2] X[3] X[4] NotX[6] NotX[7] NotX[9] X[10] NotX[12] + NotX[1] X[2] X[4] NotX[6] NotX[7] X[8] NotX[9] X[11] NotX[12] + NotX[1] X[2] NotX[3] NotX[4] NotX[5] NotX[7] NotX[9] NotX[12] X[13] + NotX[1] NotX[2] X[3] X[4] NotX[5] NotX[7] X[8] NotX[9] NotX[12] + X[1] NotX[2] NotX[4] X[5] NotX[7] NotX[9] X[11] NotX[12] X[14] + NotX[1] NotX[2] X[4] X[5] X[6] NotX[7] NotX[9] X[11] NotX[12] + X[1] NotX[2] X[4] X[5] NotX[7] NotX[9] X[10] NotX[12] X[13] + X[1] X[2] NotX[5] NotX[6] X[8] NotX[9] X[10] X[11] NotX[12] + X[1] NotX[3] X[4] X[5] NotX[6] X[8] NotX[9] NotX[12] X[14] + NotX[1] NotX[2] X[4] NotX[6] X[7] X[8] NotX[9] X[10] NotX[12] + X[1] X[3] NotX[4] NotX[5] X[6] X[7] NotX[9] X[10] NotX[12] + X[1] NotX[2] X[4] NotX[5] X[8] NotX[9] X[11] NotX[12] X[14] + NotX[1] NotX[2] NotX[4] X[5] X[7] NotX[9] X[11] NotX[12] X[13] + X[1] NotX[2] X[3] NotX[4] X[7] NotX[9] X[10] NotX[12] X[14] + NotX[1] NotX[2] NotX[3] X[6] X[7] NotX[9] X[10] X[11] NotX[12] + NotX[1] NotX[2] X[3] X[4] X[5] X[7] NotX[9] X[10] NotX[12] + NotX[1] X[2] NotX[5] X[8] NotX[9] NotX[10] X[11] NotX[12] X[14] + X[1] X[2] X[3] NotX[5] X[6] NotX[9] NotX[10] NotX[12] X[13] + NotX[1] X[2] NotX[3] X[4] X[5] NotX[9] NotX[10] NotX[12] X[14] + NotX[1] NotX[2] X[3] X[5] X[7] NotX[9] NotX[10] X[11] NotX[12] + NotX[1] NotX[2] X[6] X[8] NotX[9] NotX[10] NotX[12] X[13] X[14] + NotX[1] X[2] NotX[6] NotX[7] NotX[8] NotX[10] NotX[12] X[13] X[14] + X[1] NotX[2] NotX[5] NotX[6] NotX[8] X[9] NotX[10] NotX[12] X[13] + NotX[1] NotX[2] NotX[5] X[7] NotX[8] X[9] NotX[10] X[11] NotX[12] + NotX[1] X[2] NotX[3] X[7] NotX[8] NotX[10] X[11] NotX[12] X[13] + X[1] NotX[2] X[6] X[7] NotX[8] NotX[10] X[11] NotX[12] X[14] + X[1] NotX[2] NotX[3] NotX[6] NotX[7] NotX[10] X[11] NotX[12] X[14] + NotX[1] X[2] NotX[3] NotX[5] NotX[7] NotX[10] X[11] NotX[12] X[14] + X[1] NotX[2] NotX[3] X[6] NotX[7] X[8] NotX[10] X[11] NotX[12] + X[1] X[2] NotX[3] NotX[5] NotX[6] X[7] X[8] NotX[10] NotX[12] + X[1] X[2] NotX[5] NotX[6] X[8] X[9] NotX[10] NotX[12] X[14] + NotX[1] NotX[2] NotX[3] NotX[4] X[5] NotX[6] X[7] NotX[10] NotX[12] + X[1] NotX[2] NotX[4] NotX[6] X[7] NotX[10] X[11] NotX[12] X[14] + NotX[1] X[2] X[3] NotX[4] NotX[6] X[7] X[8] NotX[10] NotX[12] + X[1] NotX[2] NotX[3] X[4] NotX[6] NotX[10] NotX[12] X[13] X[14] + X[1] X[2] NotX[3] X[5] NotX[6] NotX[10] X[11] NotX[12] X[13] + NotX[1] NotX[2] X[3] NotX[4] NotX[5] X[6] NotX[10] NotX[12] X[13] + X[1] X[2] X[3] NotX[5] X[9] NotX[10] X[11] NotX[12] X[13] + X[1] NotX[2] NotX[3] NotX[4] X[6] X[9] NotX[10] NotX[12] X[13] + X[1] X[2] NotX[4] X[5] X[6] X[7] NotX[10] NotX[12] X[13] + X[1] NotX[2] X[3] X[5] X[8] NotX[10] X[11] NotX[12] X[14] + X[1] X[2] X[3] NotX[5] NotX[6] NotX[8] NotX[9] X[10] NotX[12] + X[1] X[2] X[5] X[7] NotX[9] X[10] NotX[11] NotX[12] X[14] + X[1] NotX[3] X[4] NotX[5] NotX[6] NotX[7] NotX[8] NotX[11] NotX[12] + X[1] X[2] NotX[3] NotX[5] X[6] NotX[7] NotX[8] NotX[11] NotX[12] + NotX[1] X[2] X[3] NotX[4] X[6] NotX[7] NotX[8] NotX[11] NotX[12] + X[1] X[2] X[4] X[5] NotX[7] NotX[8] NotX[11] NotX[12] X[13] + NotX[1] NotX[2] NotX[3] X[4] X[5] X[6] NotX[8] NotX[11] NotX[12] + X[1] X[2] NotX[5] NotX[6] NotX[7] X[8] NotX[11] NotX[12] X[13] + X[1] X[2] NotX[5] X[6] NotX[7] X[10] NotX[11] NotX[12] X[14] + X[1] NotX[2] X[3] NotX[4] NotX[7] X[8] NotX[11] NotX[12] X[13] + NotX[1] NotX[2] X[3] X[4] NotX[7] X[8] X[9] NotX[11] NotX[12] + NotX[1] NotX[2] X[3] NotX[4] X[5] NotX[6] NotX[11] NotX[12] X[14] + X[1] X[2] X[4] NotX[6] X[8] NotX[11] NotX[12] X[13] X[14] + X[1] X[3] X[4] X[5] NotX[6] X[8] NotX[11] NotX[12] X[14] + NotX[1] NotX[2] X[3] X[4] NotX[5] X[7] X[8] NotX[11] NotX[12] + X[1] NotX[2] X[4] NotX[5] X[6] X[8] X[10] NotX[11] NotX[12] + X[1] X[2] X[3] NotX[5] X[6] X[9] NotX[11] NotX[12] X[13] + NotX[1] NotX[2] NotX[3] NotX[4] X[5] X[6] X[7] NotX[11] NotX[12] + X[1] NotX[2] NotX[3] NotX[4] X[6] X[10] NotX[11] NotX[12] X[13] + X[1] NotX[2] NotX[3] X[7] X[10] NotX[11] NotX[12] X[13] X[14] + NotX[1] NotX[2] X[4] X[5] X[6] X[8] X[9] NotX[11] NotX[12] + X[1] NotX[2] X[4] X[5] X[7] X[8] X[9] NotX[11] NotX[12] + X[1] X[2] X[3] X[5] X[8] X[9] X[10] NotX[11] NotX[12] + NotX[1] X[2] NotX[4] NotX[7] NotX[8] NotX[9] NotX[10] X[11] NotX[12] + X[1] NotX[2] NotX[4] NotX[5] NotX[8] NotX[9] NotX[10] X[11] NotX[12] + X[1] X[2] X[3] NotX[5] NotX[6] NotX[9] NotX[10] X[11] NotX[12] + NotX[1] NotX[2] X[4] NotX[6] X[7] NotX[9] NotX[10] X[11] NotX[12] + NotX[1] NotX[2] X[3] NotX[4] NotX[5] X[10] X[12] NotX[13] X[14] + X[1] NotX[2] NotX[4] NotX[5] X[9] X[10] X[12] NotX[13] X[14] + NotX[1] X[2] NotX[3] X[4] NotX[5] X[10] X[11] X[12] NotX[13] + NotX[1] NotX[2] X[3] X[4] NotX[5] X[7] X[8] X[11] NotX[13] + NotX[1] NotX[2] NotX[3] NotX[4] X[5] X[6] X[7] X[11] NotX[13] + X[1] NotX[2] X[3] NotX[4] X[7] X[10] X[11] X[12] NotX[13] + NotX[1] NotX[2] NotX[3] X[4] X[5] X[6] X[9] X[11] NotX[13] + NotX[1] X[2] NotX[3] X[7] X[9] X[10] X[12] NotX[13] X[14] + X[1] X[2] NotX[3] X[5] X[6] X[8] X[10] X[11] NotX[13] + NotX[1] NotX[2] X[3] X[5] X[7] X[10] X[12] NotX[13] X[14] + NotX[1] NotX[2] X[6] X[7] X[9] X[10] X[11] NotX[13] X[14] + X[1] NotX[2] X[4] X[5] X[8] X[10] X[12] NotX[13] X[14] + NotX[1] X[2] X[3] X[6] X[8] X[9] X[11] X[12] NotX[13] + X[1] NotX[2] X[3] NotX[4] X[7] NotX[9] NotX[10] NotX[11] NotX[12] + NotX[1] X[2] NotX[3] X[4] NotX[5] NotX[8] NotX[10] NotX[11] NotX[12] + X[1] NotX[2] NotX[8] X[9] NotX[10] NotX[11] NotX[12] X[13] X[14] + X[1] X[2] X[5] X[6] NotX[7] X[8] NotX[10] NotX[11] NotX[12] + X[1] NotX[2] NotX[3] NotX[4] NotX[6] X[8] NotX[10] NotX[11] NotX[12] + X[1] X[2] NotX[3] X[5] NotX[6] X[7] NotX[10] NotX[11] NotX[12] + X[1] X[2] X[3] X[5] NotX[6] NotX[10] NotX[11] NotX[12] X[14] + NotX[1] X[2] X[4] X[6] X[7] X[8] NotX[10] NotX[11] NotX[12] + X[1] X[2] X[4] X[5] X[6] X[7] NotX[10] NotX[11] NotX[12] + NotX[1] NotX[2] NotX[5] NotX[6] NotX[8] NotX[9] NotX[11] NotX[12] X[14] + X[1] NotX[2] X[4] NotX[7] NotX[9] X[10] NotX[11] NotX[12] X[14] + NotX[1] X[2] NotX[3] X[8] NotX[9] X[10] NotX[11] NotX[12] X[14] + NotX[1] NotX[2] X[5] X[6] X[7] X[8] NotX[9] NotX[11] NotX[12] + X[1] X[2] NotX[3] X[7] NotX[8] X[9] X[10] NotX[13] X[14] + X[1] NotX[3] X[4] X[5] X[6] NotX[8] X[9] NotX[13] X[14] + X[1] NotX[2] X[3] X[4] NotX[8] X[10] X[12] NotX[13] X[14] + X[1] X[2] X[5] X[6] NotX[8] X[9] X[11] NotX[13] X[14] + NotX[1] NotX[2] NotX[3] X[4] NotX[5] NotX[6] NotX[7] NotX[13] X[14] + X[1] X[2] NotX[3] NotX[5] NotX[6] NotX[7] X[8] X[9] NotX[13] + NotX[1] NotX[2] NotX[3] NotX[4] X[5] NotX[6] NotX[7] X[9] NotX[13] + X[1] NotX[2] NotX[4] X[5] NotX[6] NotX[7] X[11] X[12] NotX[13] + NotX[1] X[2] X[3] NotX[4] NotX[6] NotX[7] X[8] X[9] NotX[13] + NotX[1] X[2] NotX[3] NotX[4] NotX[5] NotX[7] X[10] X[11] NotX[13] + X[1] NotX[2] X[3] NotX[5] NotX[7] X[8] X[10] X[11] NotX[13] + NotX[1] NotX[2] NotX[4] X[5] X[6] NotX[7] X[8] X[11] NotX[13] + X[1] NotX[2] X[3] NotX[4] NotX[7] X[8] X[12] NotX[13] X[14] + X[1] NotX[2] NotX[3] X[4] NotX[7] X[8] X[10] X[11] NotX[13] + NotX[1] X[2] NotX[3] X[5] NotX[7] X[11] X[12] NotX[13] X[14] + X[1] NotX[3] NotX[4] NotX[5] NotX[6] X[7] X[12] NotX[13] X[14] + X[1] X[2] NotX[3] NotX[5] NotX[6] X[7] X[8] X[10] NotX[13] + NotX[1] NotX[2] NotX[3] NotX[4] X[5] NotX[6] X[7] X[10] NotX[13] + NotX[1] NotX[2] X[3] NotX[4] X[5] NotX[6] X[12] NotX[13] X[14] + NotX[1] X[2] X[3] NotX[4] NotX[6] X[7] X[8] X[10] NotX[13] + X[1] NotX[2] NotX[3] NotX[6] X[7] X[10] X[11] X[12] NotX[13] + NotX[1] NotX[3] X[4] X[5] NotX[6] X[7] X[10] X[12] NotX[13] + X[1] NotX[2] X[3] NotX[6] X[7] X[8] X[12] NotX[13] X[14] + NotX[1] X[2] X[4] NotX[6] X[8] X[10] X[11] X[12] NotX[13] + X[1] X[3] X[4] X[5] NotX[6] X[7] X[9] X[10] NotX[13] + X[1] NotX[2] NotX[4] NotX[5] NotX[6] NotX[8] NotX[9] X[12] NotX[13] + NotX[1] NotX[2] NotX[4] NotX[6] NotX[8] NotX[9] X[10] X[12] NotX[13] + NotX[1] NotX[2] NotX[5] X[6] X[7] NotX[8] NotX[9] X[10] NotX[13] + NotX[1] X[2] X[4] NotX[5] X[6] NotX[8] NotX[9] X[11] NotX[13] + X[1] X[3] NotX[4] X[5] X[6] NotX[8] NotX[9] X[12] NotX[13] + X[1] X[2] NotX[5] NotX[6] NotX[7] X[8] NotX[9] NotX[13] X[14] + NotX[1] NotX[3] NotX[4] X[5] X[6] NotX[7] NotX[9] X[11] NotX[13] + X[1] NotX[2] NotX[4] NotX[7] NotX[9] X[11] X[12] NotX[13] X[14] + NotX[1] X[2] NotX[4] NotX[7] X[8] NotX[9] X[11] X[12] NotX[13] + X[1] X[2] X[3] X[5] NotX[7] X[8] NotX[9] X[11] NotX[13] + NotX[1] NotX[2] NotX[4] NotX[6] X[8] NotX[9] X[10] NotX[13] X[14] + NotX[1] NotX[2] NotX[4] NotX[5] X[6] NotX[9] X[11] X[12] NotX[13] + NotX[1] NotX[2] NotX[3] X[4] NotX[5] X[6] X[8] NotX[9] NotX[13] + X[1] NotX[3] X[4] NotX[5] X[6] X[8] NotX[9] X[11] NotX[13] + NotX[1] NotX[2] NotX[5] X[8] NotX[9] X[10] X[12] NotX[13] X[14] + NotX[1] X[2] NotX[5] X[7] NotX[9] X[10] X[12] NotX[13] X[14] + X[1] X[2] X[3] NotX[5] X[6] NotX[9] X[10] X[11] NotX[13] + NotX[1] X[2] NotX[3] X[7] X[8] NotX[9] X[11] NotX[13] X[14] + NotX[1] X[2] NotX[6] NotX[7] NotX[8] X[9] X[10] NotX[13] X[14] + X[1] X[2] NotX[3] NotX[5] X[6] NotX[7] NotX[8] X[11] NotX[13] + NotX[1] NotX[2] NotX[4] X[5] X[6] NotX[7] NotX[8] X[10] NotX[13] + NotX[1] X[2] X[3] NotX[4] X[6] NotX[7] NotX[8] X[11] NotX[13] + NotX[1] X[3] NotX[4] X[5] X[6] NotX[7] NotX[8] X[9] NotX[13] + X[1] NotX[2] NotX[3] NotX[4] NotX[6] NotX[8] X[9] NotX[13] X[14] + NotX[1] X[2] NotX[4] NotX[6] X[7] NotX[8] X[9] X[10] NotX[13] + NotX[1] NotX[2] NotX[3] X[4] X[5] NotX[6] NotX[8] X[10] NotX[13] + NotX[1] NotX[2] NotX[3] NotX[6] X[8] NotX[9] NotX[10] X[12] NotX[13] + X[1] X[2] X[4] NotX[5] X[8] NotX[9] NotX[10] X[12] NotX[13] + X[1] NotX[2] X[3] NotX[4] X[7] NotX[9] NotX[10] X[11] NotX[13] + NotX[1] NotX[2] X[4] NotX[6] NotX[7] NotX[8] NotX[10] X[11] NotX[13] + X[1] X[2] X[3] NotX[5] NotX[6] NotX[8] X[9] NotX[10] NotX[13] + NotX[1] NotX[2] NotX[3] NotX[6] X[7] NotX[8] NotX[10] X[12] NotX[13] + NotX[1] X[2] NotX[3] X[4] NotX[5] NotX[8] NotX[10] X[11] NotX[13] + NotX[1] NotX[2] X[3] X[4] NotX[5] X[7] NotX[8] NotX[10] NotX[13] + NotX[1] X[2] NotX[3] NotX[4] X[5] NotX[8] X[9] NotX[10] NotX[13] + X[1] NotX[2] X[3] X[4] NotX[8] NotX[10] X[11] NotX[13] X[14] + NotX[1] X[2] X[4] X[5] NotX[8] NotX[10] X[11] X[12] NotX[13] + NotX[1] NotX[2] NotX[5] NotX[6] NotX[7] X[8] NotX[10] X[11] NotX[13] + X[1] NotX[2] NotX[5] NotX[7] X[9] NotX[10] X[11] NotX[13] X[14] + X[1] NotX[2] NotX[3] NotX[4] NotX[6] X[8] NotX[10] X[11] NotX[13] + X[1] NotX[3] NotX[4] X[5] NotX[6] X[8] X[9] NotX[10] NotX[13] + NotX[1] X[2] NotX[4] X[5] NotX[6] X[8] NotX[10] X[12] NotX[13] + X[1] X[2] NotX[3] X[5] NotX[6] X[7] NotX[10] X[11] NotX[13] + NotX[1] NotX[2] NotX[6] X[7] X[8] NotX[10] X[11] X[12] NotX[13] + NotX[1] X[2] X[3] NotX[6] X[7] NotX[10] X[11] NotX[13] X[14] + NotX[1] X[2] NotX[3] NotX[4] NotX[5] X[7] NotX[10] NotX[13] X[14] + X[1] X[2] NotX[5] X[6] X[7] NotX[10] X[12] NotX[13] X[14] + X[1] NotX[2] NotX[3] X[4] X[7] NotX[10] X[11] NotX[13] X[14] + X[1] X[2] NotX[3] X[6] X[8] NotX[10] X[11] NotX[13] X[14] + NotX[1] NotX[2] X[3] X[4] X[5] X[7] X[9] NotX[10] NotX[13] + NotX[1] NotX[2] X[5] X[6] X[7] NotX[10] X[11] X[12] NotX[13] + X[1] NotX[2] X[3] X[6] X[9] NotX[10] X[12] NotX[13] X[14] + NotX[1] NotX[2] X[4] NotX[5] X[7] X[8] NotX[9] NotX[11] NotX[13] + NotX[1] X[2] NotX[3] NotX[4] X[5] X[8] NotX[9] NotX[11] NotX[13] + NotX[1] X[2] X[4] X[6] NotX[9] NotX[11] X[12] NotX[13] X[14] + X[1] NotX[2] NotX[6] NotX[7] NotX[8] X[9] NotX[11] NotX[13] X[14] + NotX[1] X[2] NotX[4] X[6] NotX[7] NotX[8] NotX[11] X[12] NotX[13] + X[1] X[2] NotX[7] NotX[8] X[9] X[10] NotX[11] X[12] NotX[13] + NotX[1] NotX[2] NotX[5] NotX[8] X[10] NotX[11] X[12] NotX[13] X[14] + NotX[1] X[2] NotX[4] X[5] NotX[8] X[10] NotX[11] NotX[13] X[14] + NotX[1] X[2] X[3] X[6] X[7] NotX[8] NotX[11] NotX[13] X[14] + X[1] X[2] NotX[3] X[5] X[6] NotX[7] NotX[11] NotX[13] X[14] + NotX[1] X[2] X[4] NotX[5] NotX[6] NotX[11] X[12] NotX[13] X[14] + X[1] X[2] NotX[4] NotX[6] X[8] X[10] NotX[11] NotX[13] X[14] + X[1] X[2] X[3] X[5] NotX[6] NotX[11] X[12] NotX[13] X[14] + NotX[1] X[2] NotX[3] NotX[4] NotX[5] X[9] X[10] NotX[11] NotX[13] + NotX[1] NotX[2] X[4] NotX[5] X[8] X[9] NotX[11] X[12] NotX[13] + NotX[1] NotX[2] NotX[4] X[5] X[6] X[8] NotX[11] X[12] NotX[13] + X[1] NotX[2] X[3] NotX[4] X[7] X[9] NotX[11] NotX[13] X[14] + NotX[1] X[2] NotX[4] X[6] X[8] X[9] NotX[11] NotX[13] X[14] + X[1] X[2] NotX[4] X[5] X[6] X[10] NotX[11] X[12] NotX[13] + NotX[1] X[2] NotX[3] X[4] X[9] NotX[11] X[12] NotX[13] X[14] + X[1] X[2] NotX[3] X[6] X[7] X[8] X[10] NotX[11] NotX[13] + X[1] NotX[2] X[3] X[8] X[9] X[10] NotX[11] X[12] NotX[13] + NotX[1] NotX[2] X[5] NotX[7] NotX[8] NotX[9] NotX[10] X[12] NotX[13] + X[1] X[2] NotX[4] X[5] NotX[7] NotX[9] NotX[10] X[11] NotX[13] + X[1] NotX[2] X[6] NotX[7] X[8] NotX[9] NotX[10] X[12] NotX[13] + NotX[1] NotX[2] X[3] NotX[4] NotX[5] NotX[6] NotX[9] NotX[10] NotX[13] + NotX[1] NotX[2] X[3] NotX[4] X[5] NotX[6] X[11] NotX[12] NotX[13] + X[1] NotX[2] NotX[4] NotX[6] X[7] X[10] X[11] NotX[12] NotX[13] + NotX[1] X[2] X[3] X[4] NotX[6] X[7] X[10] NotX[12] NotX[13] + X[1] X[3] NotX[4] NotX[5] X[6] X[8] X[10] NotX[12] NotX[13] + X[1] NotX[2] X[3] NotX[5] X[7] X[9] X[11] NotX[12] NotX[13] + NotX[1] X[2] X[4] NotX[5] X[9] X[11] NotX[12] NotX[13] X[14] + NotX[1] X[2] NotX[3] NotX[4] X[5] X[8] X[9] NotX[12] NotX[13] + NotX[1] NotX[2] X[3] NotX[4] X[6] X[7] X[9] NotX[12] NotX[13] + X[1] NotX[2] NotX[4] X[6] X[7] X[8] X[9] NotX[12] NotX[13] + NotX[1] X[2] NotX[3] X[4] X[5] X[9] NotX[12] NotX[13] X[14] + NotX[1] X[2] NotX[3] X[7] X[9] X[10] X[11] NotX[12] NotX[13] + X[1] NotX[2] X[3] X[4] NotX[8] NotX[9] NotX[10] NotX[11] NotX[13] + X[1] X[2] NotX[5] X[7] X[8] NotX[9] NotX[10] NotX[11] NotX[13] + X[1] NotX[2] NotX[3] X[6] NotX[7] X[9] NotX[10] NotX[11] NotX[13] + X[1] X[2] X[5] NotX[7] X[9] NotX[10] NotX[11] X[12] NotX[13] + NotX[1] X[2] X[3] X[4] NotX[6] X[7] NotX[10] NotX[11] NotX[13] + NotX[1] X[2] NotX[4] NotX[5] X[8] X[9] NotX[10] NotX[11] NotX[13] + X[1] X[2] X[3] NotX[5] X[8] X[9] NotX[10] NotX[11] NotX[13] + X[1] X[2] NotX[3] X[5] X[7] NotX[10] NotX[11] X[12] NotX[13] + X[1] NotX[2] X[3] NotX[4] NotX[7] NotX[8] NotX[9] NotX[11] NotX[13] + X[1] X[2] NotX[4] NotX[6] NotX[8] NotX[9] X[10] NotX[11] NotX[13] + X[1] NotX[2] NotX[4] NotX[8] NotX[9] NotX[11] X[12] NotX[13] X[14] + NotX[1] X[2] NotX[3] NotX[4] NotX[5] NotX[7] NotX[9] NotX[11] NotX[13] + X[1] NotX[2] NotX[3] X[6] NotX[7] X[8] NotX[9] NotX[11] NotX[13] + X[1] X[2] X[3] NotX[5] NotX[6] X[8] NotX[9] NotX[11] NotX[13] + NotX[1] X[2] NotX[4] NotX[6] X[8] NotX[9] NotX[11] X[12] NotX[13] + X[1] NotX[2] NotX[3] X[4] X[7] X[9] NotX[11] NotX[12] NotX[13] + NotX[1] X[2] X[5] X[6] X[8] X[9] NotX[11] NotX[12] NotX[13] + NotX[1] X[2] X[6] X[7] X[8] X[9] NotX[11] NotX[12] NotX[13] + NotX[1] X[2] X[5] NotX[6] NotX[9] NotX[10] X[11] NotX[12] NotX[13] + X[1] X[2] X[3] NotX[5] X[6] NotX[8] NotX[10] NotX[12] NotX[13] + X[1] NotX[2] X[3] NotX[4] NotX[7] X[8] NotX[10] NotX[12] NotX[13] + X[1] X[2] NotX[4] X[6] X[7] X[8] NotX[10] NotX[12] NotX[13] + X[1] X[2] NotX[3] X[6] X[7] X[9] NotX[10] NotX[12] NotX[13] + X[1] X[2] X[3] X[6] X[8] NotX[10] X[11] NotX[12] NotX[13] + NotX[1] NotX[2] NotX[5] NotX[8] NotX[9] X[10] X[11] NotX[12] NotX[13] + X[1] NotX[2] X[3] X[4] NotX[8] NotX[9] X[10] NotX[12] NotX[13] + NotX[1] NotX[2] X[3] NotX[4] NotX[5] X[6] NotX[9] NotX[12] NotX[13] + NotX[1] NotX[2] NotX[4] X[6] X[7] NotX[9] X[10] NotX[12] NotX[13] + X[1] NotX[2] X[3] X[7] X[8] NotX[9] X[10] NotX[12] NotX[13] + X[1] NotX[2] X[5] X[6] X[7] NotX[9] X[10] NotX[12] NotX[13] + NotX[1] X[2] X[4] NotX[6] NotX[7] NotX[8] NotX[12] NotX[13] X[14] + X[1] NotX[2] X[3] NotX[4] NotX[7] NotX[8] X[9] NotX[12] NotX[13] + NotX[1] NotX[2] NotX[6] X[7] NotX[8] X[9] NotX[12] NotX[13] X[14] + X[1] NotX[2] NotX[3] NotX[4] X[6] NotX[8] NotX[12] NotX[13] X[14] + NotX[1] NotX[2] X[3] X[7] NotX[8] X[10] NotX[12] NotX[13] X[14] + X[1] X[2] NotX[3] X[5] NotX[6] NotX[7] X[9] NotX[12] NotX[13] + X[1] NotX[2] NotX[4] NotX[7] X[8] X[9] X[10] NotX[12] NotX[13] + NotX[1] NotX[2] X[3] X[6] NotX[7] X[9] NotX[12] NotX[13] X[14] + X[1] NotX[2] X[3] X[5] NotX[7] X[8] X[10] NotX[12] NotX[13] + NotX[1] X[2] X[3] X[4] X[6] NotX[7] NotX[12] NotX[13] X[14] + X[1] X[3] X[4] X[5] X[6] NotX[7] X[9] NotX[12] NotX[13] + X[1] X[2] X[3] X[4] X[5] X[6] X[7] X[8] X[9] + X[1] X[2] X[3] X[5] X[7] X[9] X[10] X[13] NotX[14] + X[1] X[2] X[4] X[6] X[9] X[10] X[12] X[13] NotX[14] + X[1] NotX[2] X[3] X[4] X[8] NotX[10] NotX[11] NotX[12] NotX[13] + X[1] X[2] X[3] X[6] NotX[7] NotX[9] NotX[11] NotX[12] NotX[13] + X[1] NotX[2] NotX[3] X[4] NotX[6] NotX[9] NotX[11] NotX[12] NotX[13] + NotX[1] NotX[2] X[5] X[6] NotX[9] NotX[11] NotX[12] NotX[13] X[14] + X[1] NotX[2] X[7] NotX[9] X[10] NotX[11] NotX[12] NotX[13] X[14] + X[1] NotX[2] X[3] X[4] NotX[8] X[9] NotX[11] NotX[12] NotX[13] + NotX[1] NotX[2] X[6] NotX[7] X[8] NotX[11] NotX[12] NotX[13] X[14] + X[1] NotX[2] X[5] NotX[7] X[8] X[9] NotX[11] NotX[12] NotX[13] + X[1] NotX[2] NotX[5] NotX[6] X[8] X[10] NotX[11] NotX[12] NotX[13] + NotX[1] X[2] NotX[3] X[4] NotX[5] X[8] NotX[11] NotX[12] NotX[13] + NotX[1] NotX[2] NotX[3] NotX[4] NotX[5] NotX[6] X[7] X[12] X[13] + NotX[1] NotX[2] NotX[3] NotX[4] X[5] NotX[6] NotX[8] X[12] X[13] + NotX[1] NotX[2] NotX[3] NotX[4] NotX[5] NotX[6] NotX[7] X[10] X[11] + NotX[1] NotX[2] NotX[3] NotX[4] NotX[5] NotX[6] NotX[7] NotX[8] NotX[10] + NotX[1] NotX[2] NotX[3] NotX[4] NotX[5] NotX[6] NotX[7] X[8] NotX[11] + NotX[1] X[2] X[3] NotX[4] X[6] NotX[7] X[8] NotX[11] NotX[14] + NotX[1] NotX[2] X[4] X[5] NotX[7] X[8] NotX[11] X[12] NotX[14] + NotX[1] NotX[2] X[3] NotX[4] NotX[5] NotX[6] X[9] NotX[11] NotX[14] + X[1] NotX[2] NotX[3] NotX[4] NotX[6] X[8] X[10] NotX[11] NotX[14] + NotX[1] NotX[2] NotX[4] NotX[6] X[7] X[9] X[10] NotX[11] NotX[14] + X[1] X[2] NotX[3] X[5] NotX[6] X[7] X[10] NotX[11] NotX[14] + NotX[1] X[2] NotX[3] X[4] NotX[5] X[8] NotX[11] X[12] NotX[14] + NotX[1] NotX[2] NotX[3] X[5] X[8] X[10] NotX[11] X[13] NotX[14] + NotX[1] X[2] NotX[3] X[4] X[5] X[10] NotX[11] X[13] NotX[14] + X[1] X[2] X[5] X[6] X[7] X[9] NotX[11] X[13] NotX[14] + NotX[1] X[2] NotX[6] NotX[7] NotX[8] NotX[9] NotX[10] X[11] NotX[14] + X[1] NotX[2] X[3] X[4] NotX[8] NotX[9] NotX[10] X[11] NotX[14] + NotX[1] NotX[2] NotX[4] NotX[5] NotX[6] NotX[9] NotX[10] X[13] NotX[14] + X[1] NotX[2] NotX[4] X[7] NotX[9] NotX[10] X[11] X[13] NotX[14] + X[1] NotX[2] NotX[3] X[4] NotX[9] NotX[10] X[11] X[13] NotX[14] + X[1] X[2] NotX[5] NotX[6] X[7] NotX[8] X[9] NotX[10] NotX[14] + X[1] NotX[2] NotX[3] NotX[4] NotX[6] NotX[8] X[9] NotX[10] NotX[14] + X[1] NotX[2] NotX[4] NotX[5] X[7] NotX[8] NotX[10] X[12] NotX[14] + X[1] X[2] X[3] NotX[5] X[6] NotX[8] NotX[10] X[12] NotX[14] + NotX[1] X[2] NotX[3] X[5] NotX[8] X[9] NotX[10] X[13] NotX[14] + NotX[1] NotX[2] X[3] X[6] X[7] NotX[8] NotX[10] X[13] NotX[14] + NotX[1] NotX[2] X[4] X[7] NotX[8] NotX[10] X[12] X[13] NotX[14] + X[1] X[2] NotX[5] X[6] NotX[7] X[9] NotX[10] X[12] NotX[14] + NotX[1] NotX[2] NotX[3] NotX[4] X[5] X[6] NotX[7] NotX[10] NotX[14] + X[1] NotX[2] NotX[3] X[4] NotX[7] X[9] NotX[10] X[13] NotX[14] + X[1] X[2] NotX[4] NotX[6] X[7] X[9] NotX[10] X[12] NotX[14] + NotX[1] NotX[2] X[5] X[7] X[8] NotX[10] NotX[11] X[12] NotX[14] + X[1] NotX[2] X[4] X[5] X[8] NotX[10] NotX[11] X[12] NotX[14] + NotX[1] NotX[2] NotX[5] NotX[7] NotX[8] NotX[9] X[10] NotX[11] NotX[14] + X[1] X[2] NotX[3] NotX[7] NotX[8] NotX[9] NotX[11] X[12] NotX[14] + X[1] NotX[2] X[3] NotX[5] NotX[8] NotX[9] NotX[11] X[13] NotX[14] + X[1] NotX[2] NotX[3] X[6] NotX[8] NotX[9] X[10] NotX[11] NotX[14] + NotX[1] X[2] X[3] NotX[8] NotX[9] X[10] NotX[11] X[13] NotX[14] + X[1] NotX[2] NotX[3] X[4] NotX[6] NotX[9] NotX[11] X[13] NotX[14] + NotX[1] X[2] NotX[4] NotX[5] X[7] NotX[9] X[10] NotX[11] NotX[14] + X[1] X[2] X[3] NotX[5] X[6] NotX[9] X[10] NotX[11] NotX[14] + X[1] NotX[2] X[3] NotX[4] X[7] NotX[9] X[10] NotX[11] NotX[14] + NotX[1] X[2] NotX[4] X[5] X[8] NotX[9] NotX[11] X[13] NotX[14] + NotX[1] NotX[2] NotX[3] X[6] X[8] NotX[9] NotX[11] X[12] NotX[14] + NotX[1] NotX[2] X[3] X[5] X[7] NotX[9] X[10] NotX[11] NotX[14] + NotX[1] X[2] X[3] X[6] X[7] X[8] NotX[9] NotX[11] NotX[14] + NotX[1] NotX[2] X[3] X[4] X[5] NotX[7] NotX[8] NotX[11] NotX[14] + X[1] NotX[2] NotX[6] NotX[8] X[9] X[10] NotX[11] X[13] NotX[14] + NotX[1] X[2] NotX[3] X[4] NotX[5] NotX[8] X[10] NotX[11] NotX[14] + X[1] NotX[2] X[3] X[4] NotX[8] X[9] NotX[11] X[12] NotX[14] + X[1] NotX[2] X[4] X[6] NotX[8] X[9] NotX[11] X[12] NotX[14] + NotX[1] X[2] X[6] NotX[8] X[10] NotX[11] X[12] X[13] NotX[14] + NotX[1] NotX[2] NotX[4] NotX[5] X[6] NotX[7] X[8] NotX[11] NotX[14] + X[1] X[2] NotX[3] NotX[5] X[6] NotX[7] X[8] NotX[11] NotX[14] + X[1] NotX[2] NotX[5] NotX[7] X[9] NotX[11] X[12] X[13] NotX[14] + NotX[1] NotX[2] X[3] NotX[4] X[5] NotX[7] X[10] NotX[11] NotX[14] + X[1] NotX[2] X[3] NotX[4] NotX[7] X[8] NotX[11] X[12] NotX[14] + NotX[1] NotX[2] NotX[4] X[6] NotX[7] NotX[11] NotX[12] NotX[13] NotX[14] + X[1] X[2] X[5] X[6] NotX[7] NotX[11] NotX[12] NotX[13] NotX[14] + X[1] NotX[2] X[4] X[5] NotX[10] X[11] NotX[12] NotX[13] NotX[14] + X[1] NotX[2] X[4] X[8] NotX[10] X[11] NotX[12] NotX[13] NotX[14] + X[1] X[2] X[3] X[5] X[9] NotX[10] NotX[12] NotX[13] NotX[14] + X[1] NotX[2] X[5] NotX[8] NotX[9] X[11] NotX[12] NotX[13] NotX[14] + X[1] X[3] X[4] X[5] X[6] NotX[8] NotX[12] NotX[13] NotX[14] + X[1] NotX[2] X[4] NotX[5] NotX[7] X[9] NotX[12] NotX[13] NotX[14] + NotX[1] X[2] NotX[3] NotX[5] X[8] X[11] NotX[12] NotX[13] NotX[14] + NotX[1] X[2] X[3] X[6] X[9] X[11] NotX[12] NotX[13] NotX[14] + NotX[1] X[2] NotX[6] X[9] NotX[10] NotX[11] X[12] NotX[13] NotX[14] + NotX[1] X[2] NotX[3] NotX[5] NotX[10] NotX[11] X[12] NotX[13] NotX[14] + X[1] NotX[2] NotX[4] X[7] NotX[10] NotX[11] X[12] NotX[13] NotX[14] + X[1] NotX[2] NotX[6] NotX[8] NotX[9] NotX[11] X[12] NotX[13] NotX[14] + X[1] X[2] X[3] X[5] NotX[6] NotX[9] NotX[11] NotX[13] NotX[14] + NotX[1] X[2] X[4] X[6] X[7] NotX[8] NotX[11] NotX[13] NotX[14] + NotX[1] X[2] X[3] X[4] X[6] NotX[7] NotX[11] NotX[13] NotX[14] + X[1] X[2] X[4] X[5] NotX[7] NotX[11] X[12] NotX[13] NotX[14] + X[1] NotX[2] NotX[3] X[4] NotX[6] NotX[11] X[12] NotX[13] NotX[14] + X[1] X[2] X[5] NotX[6] X[8] NotX[11] X[12] NotX[13] NotX[14] + NotX[1] X[2] NotX[3] X[4] X[5] X[9] NotX[11] NotX[13] NotX[14] + NotX[1] X[2] NotX[7] X[8] NotX[9] NotX[10] X[11] NotX[13] NotX[14] + NotX[1] NotX[2] X[5] NotX[6] NotX[8] NotX[10] X[11] NotX[13] NotX[14] + X[1] NotX[2] X[4] NotX[5] X[6] NotX[8] NotX[10] NotX[13] NotX[14] + X[1] NotX[2] NotX[3] NotX[4] X[6] NotX[8] NotX[10] NotX[13] NotX[14] + X[1] X[2] NotX[3] X[5] X[6] NotX[7] NotX[10] NotX[13] NotX[14] + NotX[1] X[2] NotX[3] NotX[7] NotX[8] X[11] NotX[12] X[13] NotX[14] + X[1] X[2] X[5] NotX[7] NotX[8] X[9] NotX[12] X[13] NotX[14] + NotX[1] NotX[2] X[4] NotX[5] NotX[6] X[7] NotX[8] NotX[12] NotX[14] + X[1] NotX[2] X[3] X[4] NotX[8] X[9] NotX[12] X[13] NotX[14] + NotX[1] NotX[2] NotX[3] X[4] NotX[5] NotX[6] NotX[7] NotX[12] NotX[14] + NotX[1] NotX[2] NotX[6] NotX[7] X[8] X[9] X[10] NotX[12] NotX[14] + NotX[1] X[2] X[3] X[4] NotX[6] NotX[7] X[9] NotX[12] NotX[14] + X[1] NotX[2] NotX[5] X[6] NotX[7] X[9] NotX[12] X[13] NotX[14] + NotX[1] X[2] NotX[4] X[5] NotX[7] X[8] NotX[12] X[13] NotX[14] + X[1] X[2] NotX[3] X[5] X[6] NotX[7] NotX[12] X[13] NotX[14] + X[1] X[2] X[3] NotX[5] NotX[6] X[8] X[9] NotX[12] NotX[14] + NotX[1] NotX[2] NotX[3] NotX[6] X[7] X[10] NotX[12] X[13] NotX[14] + X[1] NotX[2] NotX[3] NotX[6] X[8] X[11] NotX[12] X[13] NotX[14] + NotX[1] NotX[2] X[4] NotX[6] X[7] X[8] X[9] NotX[12] NotX[14] + NotX[1] X[2] NotX[4] NotX[5] X[8] X[11] NotX[12] X[13] NotX[14] + NotX[1] X[2] NotX[3] X[4] NotX[5] X[8] NotX[12] X[13] NotX[14] + NotX[1] NotX[2] X[3] NotX[5] X[8] X[9] X[11] NotX[12] NotX[14] + X[1] NotX[2] X[3] NotX[4] X[7] X[11] NotX[12] X[13] NotX[14] + X[1] X[2] NotX[4] X[6] X[9] X[10] X[11] NotX[12] NotX[14] + X[1] NotX[3] X[4] X[5] X[6] X[7] X[8] NotX[12] NotX[14] + X[1] NotX[2] X[4] X[5] NotX[8] NotX[9] NotX[10] NotX[11] NotX[14] + X[1] NotX[2] NotX[3] X[6] NotX[9] NotX[10] NotX[11] X[13] NotX[14] + NotX[1] X[2] NotX[3] X[4] X[5] NotX[9] NotX[10] NotX[11] NotX[14] + NotX[1] NotX[2] X[3] NotX[4] X[5] NotX[6] NotX[10] NotX[11] NotX[14] + X[1] NotX[2] NotX[3] NotX[6] X[8] NotX[10] NotX[11] X[12] NotX[14] + NotX[1] X[2] X[4] NotX[6] X[7] NotX[10] NotX[11] X[13] NotX[14] + NotX[1] NotX[2] NotX[3] NotX[6] X[8] X[10] X[12] NotX[13] NotX[14] + X[1] X[2] X[4] NotX[6] X[7] X[9] X[11] NotX[13] NotX[14] + X[1] X[2] NotX[3] NotX[5] X[6] X[8] X[11] NotX[13] NotX[14] + X[1] X[2] X[3] NotX[5] X[6] X[9] X[10] NotX[13] NotX[14] + X[1] NotX[2] NotX[3] NotX[4] X[6] X[9] X[10] NotX[13] NotX[14] + NotX[1] NotX[2] X[3] NotX[4] X[5] X[11] X[12] NotX[13] NotX[14] + NotX[1] X[2] X[3] NotX[4] X[6] X[8] X[11] NotX[13] NotX[14] + X[1] NotX[2] NotX[3] X[6] X[8] X[9] X[12] NotX[13] NotX[14] + X[1] NotX[2] X[3] X[5] X[7] X[9] X[11] NotX[13] NotX[14] + NotX[1] X[2] X[4] X[5] X[9] X[10] X[11] NotX[13] NotX[14] + NotX[1] X[2] NotX[6] NotX[7] X[9] NotX[11] NotX[12] X[13] NotX[14] + NotX[1] NotX[2] NotX[5] X[6] X[10] NotX[11] NotX[12] X[13] NotX[14] + X[1] NotX[2] X[3] NotX[4] X[7] X[9] NotX[11] NotX[12] NotX[14] + X[1] NotX[2] X[3] X[4] X[8] NotX[11] NotX[12] X[13] NotX[14] + NotX[1] NotX[2] X[3] NotX[7] NotX[8] NotX[10] X[11] NotX[12] NotX[14] + X[1] X[2] X[3] X[5] NotX[6] NotX[10] NotX[12] X[13] NotX[14] + NotX[1] X[2] NotX[3] NotX[4] NotX[5] X[7] NotX[10] NotX[12] NotX[14] + NotX[1] X[2] NotX[3] X[4] X[5] NotX[10] X[11] NotX[12] NotX[14] + X[1] NotX[2] X[3] X[8] NotX[10] X[11] NotX[12] X[13] NotX[14] + NotX[1] X[2] X[5] X[7] X[8] X[9] NotX[10] NotX[12] NotX[14] + X[1] X[2] X[4] X[6] NotX[10] X[11] NotX[12] X[13] NotX[14] + NotX[1] NotX[2] NotX[6] NotX[8] NotX[9] X[10] X[11] NotX[12] NotX[14] + X[1] X[2] NotX[4] X[6] NotX[7] NotX[9] NotX[12] X[13] NotX[14] + X[1] NotX[2] X[4] NotX[5] NotX[9] X[10] X[11] NotX[12] NotX[14] + NotX[1] X[2] X[4] NotX[9] X[10] X[11] NotX[12] X[13] NotX[14] + X[1] X[2] X[3] X[5] X[7] NotX[9] X[10] NotX[12] NotX[14] + NotX[1] X[2] NotX[4] NotX[6] X[7] X[9] NotX[10] NotX[13] NotX[14] + X[1] NotX[2] NotX[3] X[4] NotX[6] NotX[10] X[11] NotX[13] NotX[14] + X[1] NotX[2] X[3] NotX[5] X[8] NotX[10] X[12] NotX[13] NotX[14] + X[1] X[2] NotX[4] X[6] X[8] NotX[10] X[12] NotX[13] NotX[14] + X[1] X[2] X[5] X[7] NotX[10] X[11] X[12] NotX[13] NotX[14] + NotX[1] X[2] X[4] X[5] X[6] NotX[8] NotX[9] NotX[13] NotX[14] + X[1] X[2] X[4] X[5] NotX[6] NotX[9] X[11] NotX[13] NotX[14] + NotX[1] NotX[3] NotX[4] X[5] X[6] X[7] NotX[9] NotX[13] NotX[14] + X[1] NotX[2] NotX[3] X[6] X[7] X[8] NotX[9] NotX[13] NotX[14] + NotX[1] X[2] NotX[3] X[4] X[5] NotX[9] X[10] NotX[13] NotX[14] + X[1] NotX[2] X[3] X[5] X[8] NotX[9] X[12] NotX[13] NotX[14] + NotX[1] X[2] NotX[5] NotX[6] NotX[7] NotX[8] X[10] NotX[13] NotX[14] + NotX[1] X[2] NotX[5] NotX[7] NotX[8] X[9] X[11] NotX[13] NotX[14] + X[1] NotX[2] NotX[3] NotX[6] NotX[8] X[9] X[10] NotX[13] NotX[14] + X[1] X[2] NotX[3] NotX[5] X[6] X[7] NotX[8] NotX[13] NotX[14] + NotX[1] X[2] X[3] NotX[4] X[6] X[7] NotX[8] NotX[13] NotX[14] + X[1] X[2] NotX[3] X[5] X[6] NotX[8] X[10] NotX[13] NotX[14] + X[1] NotX[2] X[4] X[5] X[6] NotX[8] X[11] NotX[13] NotX[14] + X[1] X[2] X[3] X[5] X[7] NotX[8] X[9] NotX[13] NotX[14] + NotX[1] X[3] NotX[4] X[5] NotX[6] NotX[7] X[10] NotX[13] NotX[14] + X[1] NotX[2] NotX[4] NotX[7] X[8] X[10] X[11] NotX[13] NotX[14] + X[1] NotX[2] NotX[7] X[8] X[9] X[11] X[12] NotX[13] NotX[14] + X[1] X[2] NotX[4] NotX[5] NotX[6] X[8] X[12] NotX[13] NotX[14] + X[1] X[2] X[4] NotX[5] NotX[6] X[10] X[12] NotX[13] NotX[14] + X[1] X[2] NotX[5] NotX[6] X[7] X[9] X[10] NotX[13] NotX[14] + X[1] X[2] NotX[4] X[5] NotX[6] X[7] X[11] NotX[13] NotX[14] + NotX[1] NotX[2] X[4] NotX[5] NotX[6] X[8] X[9] X[12] NotX[14] + X[1] NotX[2] NotX[5] NotX[6] X[7] X[8] X[10] X[12] NotX[14] + X[1] X[2] NotX[5] NotX[6] X[8] X[9] X[10] X[13] NotX[14] + NotX[1] NotX[2] X[3] NotX[4] X[5] NotX[6] X[11] X[13] NotX[14] + NotX[1] X[2] X[3] X[4] NotX[6] X[7] X[10] X[12] NotX[14] + X[1] X[3] X[4] X[5] NotX[6] X[8] X[11] X[13] NotX[14] + NotX[1] X[2] NotX[3] NotX[4] NotX[5] X[7] X[11] X[12] NotX[14] + NotX[1] NotX[2] X[3] NotX[4] NotX[5] X[6] X[10] X[12] NotX[14] + X[1] X[2] NotX[4] NotX[5] X[6] X[9] X[12] X[13] NotX[14] + NotX[1] NotX[2] NotX[3] X[4] NotX[5] X[6] X[8] X[9] NotX[14] + X[1] NotX[2] X[3] NotX[5] X[7] X[8] X[12] X[13] NotX[14] + X[1] NotX[2] X[4] NotX[5] X[6] X[10] X[11] X[12] NotX[14] + X[1] NotX[2] NotX[5] X[7] X[8] X[9] X[10] X[13] NotX[14] + X[1] X[2] X[3] NotX[5] X[6] X[10] X[11] X[13] NotX[14] + X[1] NotX[2] NotX[3] NotX[4] X[6] X[9] X[12] X[13] NotX[14] + NotX[1] X[2] NotX[3] NotX[4] X[5] X[8] X[9] X[12] NotX[14] + X[1] NotX[3] NotX[4] X[5] X[6] X[8] X[9] X[10] NotX[14] + NotX[1] NotX[2] NotX[4] X[5] X[6] X[7] X[9] X[13] NotX[14] + X[1] X[2] NotX[3] X[5] X[6] X[8] X[12] X[13] NotX[14] + X[1] X[2] NotX[3] X[5] X[7] X[10] X[11] X[13] NotX[14] + NotX[1] NotX[2] X[3] X[4] X[5] X[7] X[9] X[10] NotX[14] + NotX[1] NotX[2] X[4] X[6] X[9] X[10] X[11] X[13] NotX[14] + X[1] NotX[2] X[3] X[8] X[9] X[10] X[12] X[13] NotX[14] + X[1] NotX[2] X[4] X[5] X[7] X[8] X[10] X[13] NotX[14] + NotX[1] X[2] X[3] X[6] X[7] X[9] X[11] X[13] NotX[14] + NotX[1] X[3] X[4] X[5] X[6] X[7] X[11] X[13] NotX[14] + NotX[1] X[2] X[3] NotX[4] X[6] X[7] NotX[9] X[13] NotX[14] + NotX[1] NotX[2] X[3] X[6] X[8] NotX[9] X[11] X[13] NotX[14] + X[1] NotX[2] X[3] X[7] NotX[9] X[10] X[11] X[13] NotX[14] + NotX[1] X[2] X[3] X[4] X[6] X[8] NotX[9] X[11] NotX[14] + NotX[1] X[2] X[4] X[7] X[8] NotX[9] X[11] X[12] NotX[14] + NotX[1] NotX[2] NotX[3] NotX[4] NotX[5] X[6] NotX[7] NotX[8] NotX[14] + NotX[1] NotX[2] NotX[4] X[6] NotX[7] NotX[8] X[10] X[13] NotX[14] + X[1] NotX[2] X[3] NotX[4] NotX[7] NotX[8] X[9] X[12] NotX[14] + NotX[1] X[2] X[5] X[6] NotX[7] NotX[8] X[12] X[13] NotX[14] + NotX[1] NotX[2] NotX[3] X[4] NotX[5] NotX[6] NotX[8] X[12] NotX[14] + X[1] X[2] X[3] NotX[5] NotX[6] NotX[8] X[9] X[10] NotX[14] + X[1] NotX[3] X[4] NotX[5] X[6] X[7] NotX[8] X[11] NotX[14] + NotX[1] NotX[2] X[3] X[4] NotX[5] X[7] NotX[8] X[10] NotX[14] + NotX[1] X[2] NotX[3] NotX[4] X[5] NotX[8] X[9] X[10] NotX[14] + X[1] NotX[2] NotX[3] X[4] X[7] NotX[8] X[9] X[13] NotX[14] + X[1] NotX[2] X[3] X[7] NotX[8] X[9] X[10] X[12] NotX[14] + X[1] X[2] NotX[3] X[5] NotX[6] NotX[7] X[9] X[12] NotX[14] + NotX[1] X[2] X[4] X[5] NotX[6] NotX[7] X[9] X[12] NotX[14] + NotX[1] X[3] X[4] NotX[5] X[6] NotX[7] X[8] X[10] NotX[14] + NotX[1] NotX[2] NotX[4] X[5] NotX[7] X[9] X[11] X[13] NotX[14] + X[1] NotX[2] X[3] NotX[4] NotX[7] X[8] X[11] X[13] NotX[14] + NotX[1] NotX[2] X[3] X[4] X[5] NotX[7] X[9] X[11] NotX[14] + X[1] NotX[2] X[5] X[6] NotX[7] X[10] X[11] X[13] NotX[14] + NotX[1] X[2] X[4] NotX[7] X[8] X[9] X[12] X[13] NotX[14] + X[1] X[2] X[3] X[5] NotX[7] X[8] X[9] X[12] NotX[14] + NotX[1] NotX[2] NotX[4] NotX[5] NotX[6] X[9] X[10] X[11] NotX[14] + NotX[1] NotX[2] NotX[3] X[4] X[5] NotX[6] X[8] NotX[10] NotX[14] + NotX[1] X[2] X[3] X[4] NotX[6] X[7] NotX[10] X[11] NotX[14] + NotX[1] X[2] X[3] NotX[6] X[7] X[9] NotX[10] X[13] NotX[14] + X[1] X[2] NotX[3] NotX[5] X[9] NotX[10] X[11] X[13] NotX[14] + X[1] NotX[2] NotX[4] X[6] X[8] NotX[10] X[11] X[12] NotX[14] + X[1] X[3] NotX[4] X[5] X[6] X[8] NotX[10] X[13] NotX[14] + NotX[1] NotX[3] X[4] X[5] X[6] X[7] NotX[10] X[12] NotX[14] + NotX[1] NotX[2] X[4] X[5] X[7] X[9] NotX[10] X[13] NotX[14] + X[1] NotX[2] X[3] X[4] X[9] NotX[10] X[11] X[12] NotX[14] + X[1] NotX[2] X[3] NotX[4] NotX[7] NotX[8] NotX[9] X[11] NotX[14] + X[1] NotX[2] NotX[4] X[5] NotX[7] NotX[8] NotX[9] X[13] NotX[14] + X[1] X[2] X[5] X[6] NotX[7] NotX[8] NotX[9] X[12] NotX[14] + X[1] X[2] NotX[3] NotX[5] NotX[6] X[7] NotX[8] NotX[9] NotX[14] + NotX[1] X[2] X[3] NotX[4] NotX[6] X[7] NotX[8] NotX[9] NotX[14] + NotX[1] X[3] NotX[4] X[5] X[6] X[7] NotX[8] NotX[9] NotX[14] + X[1] NotX[2] X[3] X[4] NotX[8] NotX[9] X[10] X[12] NotX[14] + X[1] NotX[2] X[4] X[7] NotX[8] NotX[9] X[10] X[13] NotX[14] + X[1] X[2] X[4] X[5] X[6] X[7] NotX[8] NotX[9] NotX[14] + NotX[1] NotX[2] NotX[5] X[6] NotX[7] X[8] NotX[9] X[11] NotX[14] + X[1] NotX[2] X[3] NotX[7] X[8] NotX[9] X[12] X[13] NotX[14] + X[1] NotX[2] X[4] NotX[7] X[8] NotX[9] X[10] X[12] NotX[14] + NotX[1] NotX[2] X[3] NotX[4] NotX[5] NotX[6] NotX[9] X[10] NotX[14] + X[1] X[2] X[5] NotX[6] X[8] NotX[9] X[12] X[13] NotX[14] + X[1] X[2] NotX[3] NotX[5] X[6] X[7] NotX[9] X[13] NotX[14] + X[1] NotX[2] NotX[3] NotX[4] X[6] NotX[9] X[10] X[11] NotX[14] + NotX[1] X[2] NotX[3] NotX[4] X[5] X[8] NotX[9] X[11] NotX[14] + NotX[1] NotX[2] NotX[3] NotX[4] NotX[5] NotX[6] X[7] NotX[8] NotX[12] + NotX[1] NotX[2] NotX[3] NotX[4] NotX[5] NotX[6] X[7] X[8] NotX[13] ------------------------------------------ This ends this article, that took, 4113.432, seconds to generate.