#!/usr/bin/env python3

from z3 import *
import math

N = int(sys.argv[1])
INT_SIZE = math.ceil(math.log(4*N)) + 1

S = Solver()

Y = [BitVec(f"Y{i + 1}", INT_SIZE) for i in range(N)]

S.add(And(*(And(1 <= y, y <= N) for y in Y)))

S.add(Distinct(*Y))

for k in range(1, N):
    for i in range(0, N - k):
        for j in range(0, N - k):
            if i != j:
                S.add(Y[i + k] - Y[i] != Y[j + k] - Y[j])

def all_smt(s, initial_terms):
    def block_term(s, m, t):
        s.add(t != m.eval(t, model_completion=True))
    def fix_term(s, m, t):
        s.add(t == m.eval(t, model_completion=True))
    def all_smt_rec(terms):
        if sat == s.check():
           m = s.model()
           yield m
           for i in range(len(terms)):
               s.push()
               block_term(s, m, terms[i])
               for j in range(i):
                   fix_term(s, m, terms[j])
               yield from all_smt_rec(terms[i:])
               s.pop()
    yield from all_smt_rec(list(initial_terms))

count = 0
for m in all_smt(S, Y):
    count += 1

print(f"count: {count}")