#!/usr/bin/python3

from z3 import *
import itertools, sys

def chk (SEQ_LEN, SUBSEQ_LEN):
    s=Solver()
    # not booleans, beacause we will sum them:
    items=[Int("item_%d" % i) for i in range(SEQ_LEN)]

    for item in items:
        s.add(And(item>=0, item<SEQ_LEN))

    s.add(Distinct(*items))

    or_chain=[]
    # n choose k:
    for comb in itertools.combinations(items, SUBSEQ_LEN):
        #print(comb)
        and_chain_asc=[]
        and_chain_desc=[]
        for pair_start in range(SUBSEQ_LEN-1):
            and_chain_asc.append(comb[pair_start] < comb[pair_start+1])
            and_chain_desc.append(comb[pair_start] > comb[pair_start+1])
        #print (and_chain_asc)
        #print (and_chain_desc)
        or_chain.append(And(*and_chain_asc))
        or_chain.append(And(*and_chain_desc))
    #print (or_chain)
    s.add(Or(*or_chain)==False)

    return s.check()==sat
    #print (s.check())
    #m=s.model()
    #print (m)
    #for item in items:
    #    #print (m[item])
    #    print (m[item].as_long())

for SEQ_LEN in range(2, 100):
    for SUBSEQ_LEN in range(2, 100):
        if chk(SEQ_LEN, SUBSEQ_LEN)==False:
            print ("unsat", SEQ_LEN, SUBSEQ_LEN)
            k=SUBSEQ_LEN-1
            assert SEQ_LEN >= k**2+1
            sys.stdout.flush()
        else:
            break