(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])