not(X[1]) and X[2] and X[3] and not(X[4]) and not(X[5]) and X[6] and X[7] or X[1] and X[2] and not(X[3]) and not(X[4]) and not(X[5]) and not(X[6]) and not(X[8]) or X[1] and X[2] and not(X[3]) and X[4] and not(X[5]) and X[7] and X[8] or X[1] and not(X[2]) and not(X[3]) and not(X[4]) and not(X[6]) and not(X[7]) and not(X[8]) or X[1] and X[2] and X[3] and X[5] and X[6] and X[7] and not(X[8]) or X[1] and not(X[2]) and not(X[4]) and X[5] and X[6] and not(X[7]) and not(X[8]) or not(X[1]) and not(X[3]) and X[4] and X[5] and X[6] and not(X[7]) and not(X[8]) or not(X[2]) and X[3] and not(X[4]) and X[5] and X[6] and not(X[7]) and X[8] or X[1] and X[2] and X[3] and X[4] and X[5] and not(X[6]) and not(X[9]) or not(X[1]) and X[2] and X[3] and not(X[4]) and X[5] and not(X[7]) and X[9] or X[1] and not(X[2]) and not(X[3]) and X[4] and not(X[6]) and not(X[7]) and X[9] or X[1] and not(X[2]) and X[3] and X[5] and X[6] and X[7] and not(X[9]) or X[1] and X[2] and not(X[4]) and not(X[5]) and X[6] and not(X[7]) and X[9] or not(X[1]) and X[3] and not(X[4]) and not(X[5]) and X[6] and not(X[7]) and X[9] or not(X[2]) and not(X[3]) and X[4] and not(X[5]) and X[6] and X[7] and not(X[9]) or not(X[1]) and not(X[2]) and X[3] and not(X[4]) and X[5] and not(X[8]) and X[9] or not(X[1]) and X[2] and not(X[3]) and X[4] and not(X[6]) and not(X[8]) and not(X[9]) or not(X[1]) and X[2] and X[3] and not(X[5]) and not(X[6]) and X[8] and X[9] or X[1] and not(X[2]) and X[4] and not(X[5]) and not(X[6]) and X[8] and not(X[9]) or X[1] and not(X[3]) and X[4] and not(X[5]) and not(X[6]) and not(X[8]) and not(X[9]) or X[2] and not(X[3]) and not(X[4]) and X[5] and X[6] and X[8] and X[9] or not(X[1]) and not(X[2]) and not(X[3]) and X[4] and X[7] and not(X[8]) and X[9] or X[1] and not(X[2]) and X[3] and X[5] and X[7] and X[8] and X[9] or X[1] and X[2] and not(X[4]) and not(X[5]) and X[7] and X[8] and X[9] or not(X[1]) and not(X[3]) and not(X[4]) and X[5] and not(X[7]) and not(X[8]) and X[9] or not(X[2]) and not(X[3]) and not(X[4]) and X[5] and X[7] and X[8] and X[9] or not(X[1]) and not(X[2]) and not(X[3]) and X[6] and not(X[7]) and not(X[8]) and not(X[9]) or not(X[1]) and X[2] and X[4] and X[6] and X[7] and X[8] and not(X[9]) or not(X[1]) and X[3] and X[4] and not(X[6]) and X[7] and X[8] and not(X[9]) or X[2] and not(X[3]) and X[4] and X[6] and X[7] and not(X[8]) and not(X[9]) or X[1] and X[2] and X[5] and X[6] and not(X[7]) and not(X[8]) and X[9] or X[1] and X[3] and X[5] and not(X[6]) and X[7] and not(X[8]) and X[9] or X[2] and not(X[3]) and X[5] and X[6] and X[7] and not(X[8]) and X[9] or X[1] and not(X[4]) and not(X[5]) and X[6] and X[7] and not(X[8]) and X[9] or not(X[2]) and X[4] and X[5] and X[6] and not(X[7]) and not(X[8]) and X[9] or X[3] and X[4] and not(X[5]) and X[6] and X[7] and X[8] and X[9] or not(X[1]) and X[2] and not(X[3]) and not(X[4]) and X[5] and not(X[6]) and not(X[10]) or not(X[1]) and X[2] and not(X[3]) and not(X[4]) and not(X[5]) and X[7] and X[10] or not(X[1]) and X[2] and X[3] and not(X[4]) and not(X[6]) and X[7] and not(X[10]) or not(X[1]) and X[2] and X[3] and X[5] and X[6] and X[7] and not(X[10]) or not(X[1]) and not(X[2]) and X[4] and not(X[5]) and X[6] and not(X[7]) and X[10] or not(X[1]) and X[3] and not(X[4]) and X[5] and not(X[6]) and X[7] and X[10] or not(X[2]) and not(X[3]) and not(X[4]) and not(X[5]) and not(X[6]) and X[7] and not(X[10]) or X[1] and X[2] and X[3] and X[4] and not(X[5]) and not(X[8]) and X[10] or not(X[1]) and X[2] and X[3] and X[4] and not(X[6]) and not(X[8]) and not(X[10]) or X[1] and X[2] and not(X[3]) and X[5] and not(X[6]) and not(X[8]) and X[10] or X[1] and X[2] and X[4] and X[5] and X[6] and X[8] and not(X[10]) or X[1] and X[3] and not(X[4]) and not(X[5]) and not(X[6]) and not(X[8]) and not(X[10]) or not(X[2]) and X[3] and not(X[4]) and not(X[5]) and X[6] and X[8] and X[10] or not(X[1]) and X[2] and X[3] and X[4] and X[7] and not(X[8]) and X[10] or not(X[1]) and not(X[2]) and X[3] and not(X[5]) and X[7] and not(X[8]) and not(X[10]) or not(X[1]) and not(X[2]) and X[4] and X[5] and not(X[7]) and X[8] and X[10] or not(X[1]) and not(X[3]) and not(X[4]) and not(X[5]) and not(X[7]) and X[8] and not(X[10]) or not(X[2]) and X[3] and not(X[4]) and not(X[5]) and X[7] and X[8] and not(X[10]) or X[1] and not(X[2]) and not(X[3]) and X[6] and not(X[7]) and X[8] and X[10] or not(X[1]) and not(X[2]) and X[4] and not(X[6]) and not(X[7]) and not(X[8]) and X[10] or X[1] and not(X[3]) and not(X[4]) and not(X[6]) and not(X[7]) and X[8] and not(X[10]) or not(X[2]) and not(X[3]) and not(X[4]) and not(X[6]) and X[7] and not(X[8]) and X[10] or X[1] and X[2] and X[5] and not(X[6]) and X[7] and X[8] and X[10] or X[1] and X[3] and X[5] and not(X[6]) and not(X[7]) and not(X[8]) and X[10] or not(X[2]) and X[3] and not(X[5]) and not(X[6]) and not(X[7]) and X[8] and not(X[10]) or not(X[1]) and not(X[4]) and not(X[5]) and not(X[6]) and not(X[7]) and not(X[8]) and not(X[10]) or not(X[2]) and X[4] and X[5] and X[6] and not(X[7]) and X[8] and not(X[10]) or X[3] and not(X[4]) and X[5] and X[6] and X[7] and X[8] and X[10] or X[1] and X[2] and X[3] and X[4] and not(X[5]) and not(X[9]) and not(X[10]) or not(X[1]) and X[2] and not(X[3]) and X[4] and not(X[6]) and X[9] and not(X[10]) or X[1] and X[2] and not(X[3]) and X[5] and not(X[6]) and X[9] and not(X[10]) or X[1] and X[2] and not(X[4]) and X[5] and X[6] and not(X[9]) and X[10] or X[1] and not(X[3]) and not(X[4]) and not(X[5]) and X[6] and not(X[9]) and X[10] or X[2] and not(X[3]) and not(X[4]) and X[5] and X[6] and not(X[9]) and X[10] or X[1] and not(X[2]) and not(X[3]) and X[4] and X[7] and X[9] and X[10] or not(X[1]) and X[2] and not(X[3]) and not(X[5]) and X[7] and X[9] and not(X[10]) or not(X[1]) and not(X[2]) and not(X[4]) and X[5] and X[7] and not(X[9]) and not(X[10]) or X[1] and not(X[3]) and not(X[4]) and X[5] and X[7] and not(X[9]) and not(X[10]) or X[2] and not(X[3]) and not(X[4]) and not(X[5]) and X[7] and not(X[9]) and not(X[10]) or X[1] and not(X[2]) and not(X[3]) and X[6] and X[7] and X[9] and not(X[10]) or not(X[1]) and X[2] and X[4] and not(X[6]) and not(X[7]) and X[9] and X[10] or not(X[1]) and X[3] and not(X[4]) and not(X[6]) and not(X[7]) and not(X[9]) and X[10] or not(X[2]) and not(X[3]) and X[4] and not(X[6]) and X[7] and X[9] and not(X[10]) or X[1] and not(X[2]) and not(X[5]) and X[6] and not(X[7]) and X[9] and not(X[10]) or X[1] and X[3] and X[5] and not(X[6]) and not(X[7]) and X[9] and not(X[10]) or not(X[2]) and not(X[3]) and X[5] and X[6] and X[7] and not(X[9]) and X[10] or not(X[1]) and X[4] and not(X[5]) and X[6] and not(X[7]) and X[9] and not(X[10]) or not(X[2]) and X[4] and X[5] and X[6] and X[7] and not(X[9]) and not(X[10]) or not(X[3]) and X[4] and not(X[5]) and X[6] and not(X[7]) and not(X[9]) and not(X[10]) or X[1] and X[2] and X[3] and not(X[4]) and X[8] and not(X[9]) and not(X[10]) or X[1] and not(X[2]) and X[3] and not(X[5]) and not(X[8]) and not(X[9]) and not(X[10]) or X[1] and X[2] and X[4] and not(X[5]) and not(X[8]) and X[9] and not(X[10]) or not(X[1]) and not(X[3]) and X[4] and not(X[5]) and X[8] and X[9] and X[10] or X[2] and not(X[3]) and X[4] and not(X[5]) and not(X[8]) and X[9] and X[10] or not(X[1]) and not(X[2]) and X[3] and X[6] and not(X[8]) and not(X[9]) and X[10] or not(X[1]) and not(X[2]) and X[4] and not(X[6]) and not(X[8]) and not(X[9]) and not(X[10]) or not(X[1]) and not(X[3]) and X[4] and not(X[6]) and X[8] and not(X[9]) and X[10] or X[2] and not(X[3]) and X[4] and not(X[6]) and X[8] and not(X[9]) and not(X[10]) or X[1] and not(X[2]) and X[5] and not(X[6]) and X[8] and not(X[9]) and X[10] or X[1] and X[3] and not(X[5]) and X[6] and X[8] and not(X[9]) and X[10] or X[2] and X[3] and not(X[5]) and not(X[6]) and not(X[8]) and X[9] and X[10] or X[1] and X[4] and X[5] and not(X[6]) and not(X[8]) and not(X[9]) and not(X[10]) or X[2] and X[4] and X[5] and X[6] and X[8] and X[9] and X[10] or not(X[3]) and not(X[4]) and X[5] and X[6] and X[8] and not(X[9]) and not(X[10]) or not(X[1]) and X[2] and X[3] and not(X[7]) and X[8] and not(X[9]) and not(X[10]) or not(X[1]) and X[2] and X[4] and not(X[7]) and not(X[8]) and not(X[9]) and X[10] or not(X[1]) and not(X[3]) and not(X[4]) and not(X[7]) and X[8] and not(X[9]) and X[10] or X[2] and not(X[3]) and X[4] and not(X[7]) and X[8] and not(X[9]) and X[10] or X[1] and not(X[2]) and not(X[5]) and not(X[7]) and not(X[8]) and X[9] and X[10] or X[1] and X[3] and not(X[5]) and not(X[7]) and not(X[8]) and not(X[9]) and X[10] or not(X[2]) and X[3] and not(X[5]) and X[7] and not(X[8]) and X[9] and X[10] or not(X[1]) and X[4] and X[5] and X[7] and X[8] and X[9] and X[10] or not(X[2]) and not(X[4]) and not(X[5]) and X[7] and X[8] and X[9] and X[10] or X[3] and not(X[4]) and not(X[5]) and X[7] and not(X[8]) and not(X[9]) and X[10] or X[1] and X[2] and not(X[6]) and not(X[7]) and X[8] and X[9] and X[10] or not(X[1]) and X[3] and X[6] and not(X[7]) and not(X[8]) and not(X[9]) and not(X[10]) or not(X[2]) and not(X[3]) and not(X[6]) and not(X[7]) and not(X[8]) and not(X[9]) and X[10] or not(X[1]) and X[4] and not(X[6]) and not(X[7]) and not(X[8]) and X[9] and not(X[10]) or not(X[2]) and X[4] and not(X[6]) and X[7] and not(X[8]) and not(X[9]) and X[10] or X[3] and X[4] and not(X[6]) and X[7] and X[8] and X[9] and not(X[10]) or X[1] and X[5] and X[6] and not(X[7]) and not(X[8]) and not(X[9]) and not(X[10]) or not(X[2]) and X[5] and not(X[6]) and not(X[7]) and X[8] and not(X[9]) and not(X[10]) or X[3] and not(X[5]) and not(X[6]) and not(X[7]) and X[8] and not(X[9]) and X[10] or not(X[4]) and X[5] and not(X[6]) and not(X[7]) and not(X[8]) and not(X[9]) and not(X[10]) or not(X[1]) and X[2] and not(X[3]) and not(X[4]) and not(X[5]) and X[6] and not(X[7]) and not(X[8]) or not(X[1]) and not(X[2]) and not(X[3]) and not(X[4]) and not(X[5]) and X[6] and X[7] and not(X[9]) or not(X[1]) and not(X[2]) and not(X[3]) and not(X[4]) and not(X[5]) and X[6] and not(X[8]) and X[9] or not(X[1]) and not(X[2]) and X[3] and X[4] and X[5] and X[7] and not(X[8]) and X[9] or not(X[1]) and X[2] and X[3] and X[4] and X[6] and not(X[7]) and not(X[8]) and X[9] or X[1] and not(X[2]) and X[3] and X[5] and X[6] and X[7] and not(X[8]) and X[9] or X[1] and X[2] and X[4] and not(X[5]) and X[6] and not(X[7]) and X[8] and X[9] or X[1] and X[3] and not(X[4]) and X[5] and not(X[6]) and X[7] and not(X[8]) and not(X[9]) or not(X[2]) and not(X[3]) and not(X[4]) and X[5] and X[6] and not(X[7]) and X[8] and X[9] or not(X[1]) and X[2] and X[3] and X[4] and not(X[5]) and X[6] and X[7] and not(X[10]) or not(X[1]) and X[2] and not(X[3]) and X[4] and X[5] and X[6] and X[8] and not(X[10]) or not(X[1]) and X[2] and X[3] and not(X[4]) and X[5] and X[7] and not(X[8]) and X[10] or not(X[1]) and X[2] and X[3] and X[4] and X[6] and not(X[7]) and X[8] and X[10] or not(X[1]) and X[2] and not(X[3]) and X[5] and not(X[6]) and X[7] and not(X[8]) and X[10] or X[1] and not(X[2]) and not(X[4]) and not(X[5]) and not(X[6]) and not(X[7]) and X[8] and X[10] or X[1] and X[3] and X[4] and not(X[5]) and not(X[6]) and X[7] and X[8] and X[10] or not(X[2]) and not(X[3]) and not(X[4]) and not(X[5]) and not(X[6]) and X[7] and X[8] and X[10] or X[1] and not(X[2]) and not(X[3]) and not(X[4]) and not(X[5]) and X[6] and not(X[9]) and not(X[10]) or X[1] and X[2] and X[3] and not(X[4]) and not(X[5]) and X[7] and not(X[9]) and not(X[10]) or not(X[1]) and X[2] and X[3] and not(X[4]) and X[6] and not(X[7]) and not(X[9]) and X[10] or X[1] and X[2] and X[3] and not(X[5]) and not(X[6]) and not(X[7]) and X[9] and not(X[10]) or X[1] and X[2] and not(X[4]) and not(X[5]) and X[6] and not(X[7]) and not(X[9]) and not(X[10]) or X[1] and X[3] and X[4] and X[5] and X[6] and not(X[7]) and not(X[9]) and X[10] or not(X[2]) and X[3] and X[4] and not(X[5]) and X[6] and X[7] and not(X[9]) and X[10] or X[1] and not(X[2]) and X[3] and X[4] and not(X[5]) and not(X[8]) and X[9] and not(X[10]) or not(X[1]) and not(X[2]) and not(X[3]) and X[4] and not(X[6]) and X[8] and not(X[9]) and not(X[10]) or not(X[1]) and not(X[2]) and X[3] and not(X[5]) and not(X[6]) and X[8] and X[9] and X[10] or not(X[1]) and X[2] and not(X[4]) and X[5] and not(X[6]) and X[8] and X[9] and X[10] or X[1] and not(X[3]) and not(X[4]) and not(X[5]) and not(X[6]) and X[8] and not(X[9]) and X[10] or X[2] and not(X[3]) and not(X[4]) and X[5] and X[6] and not(X[8]) and not(X[9]) and not(X[10]) or X[1] and not(X[2]) and X[3] and X[4] and not(X[7]) and X[8] and X[9] and X[10] or not(X[1]) and not(X[2]) and X[3] and X[5] and X[7] and X[8] and X[9] and not(X[10]) or not(X[1]) and X[2] and X[4] and X[5] and not(X[7]) and X[8] and X[9] and not(X[10]) or not(X[1]) and not(X[3]) and not(X[4]) and not(X[5]) and not(X[7]) and X[8] and X[9] and X[10] or not(X[2]) and not(X[3]) and not(X[4]) and X[5] and X[7] and not(X[8]) and X[9] and not(X[10]) or not(X[1]) and not(X[2]) and not(X[3]) and X[6] and X[7] and X[8] and X[9] and not(X[10]) or X[1] and X[2] and X[4] and X[6] and X[7] and X[8] and not(X[9]) and X[10] or X[1] and not(X[3]) and X[4] and X[6] and not(X[7]) and not(X[8]) and not(X[9]) and X[10] or not(X[2]) and not(X[3]) and not(X[4]) and X[6] and X[7] and not(X[8]) and X[9] and X[10] or not(X[1]) and not(X[2]) and X[5] and not(X[6]) and not(X[7]) and X[8] and X[9] and not(X[10]) or not(X[1]) and not(X[3]) and X[5] and not(X[6]) and X[7] and X[8] and not(X[9]) and X[10] or not(X[2]) and X[3] and not(X[5]) and X[6] and not(X[7]) and X[8] and not(X[9]) and not(X[10]) or not(X[1]) and not(X[4]) and not(X[5]) and not(X[6]) and not(X[7]) and not(X[8]) and X[9] and X[10] or not(X[2]) and not(X[4]) and X[5] and not(X[6]) and not(X[7]) and X[8] and X[9] and X[10] or X[3] and not(X[4]) and not(X[5]) and not(X[6]) and X[7] and X[8] and not(X[9]) and X[10] or X[1] and X[2] and X[3] and not(X[4]) and X[5] and X[6] and not(X[7]) and X[8] and X[9] or not(X[1]) and X[2] and X[3] and X[4] and X[5] and not(X[6]) and not(X[7]) and X[8] and X[10] or not(X[1]) and not(X[2]) and X[3] and X[4] and X[5] and X[6] and X[7] and not(X[9]) and X[10] or X[1] and not(X[2]) and not(X[3]) and X[4] and X[5] and not(X[6]) and X[8] and not(X[9]) and not(X[10]) or X[1] and X[2] and X[3] and not(X[4]) and X[5] and X[7] and X[8] and X[9] and not(X[10]) or not(X[1]) and X[2] and not(X[3]) and not(X[4]) and not(X[6]) and not(X[7]) and not(X[8]) and not(X[9]) and X[10] or X[1] and not(X[2]) and X[3] and X[5] and not(X[6]) and X[7] and X[8] and not(X[9]) and not(X[10]) or X[1] and X[2] and not(X[4]) and X[5] and not(X[6]) and not(X[7]) and X[8] and not(X[9]) and X[10] or X[1] and not(X[3]) and X[4] and not(X[5]) and not(X[6]) and not(X[7]) and X[8] and X[9] and not(X[10]) or not(X[2]) and X[3] and X[4] and not(X[5]) and X[6] and X[7] and X[8] and not(X[9]) and not(X[10]) or not(X[1]) and not(X[2]) and not(X[3]) and X[4] and not(X[5]) and not(X[6]) and not(X[7]) and X[8] and X[9] and not(X[10])