#!/usr/bin/python3

from z3 import *
import functools, operator, sys

def product(i):
    return functools.reduce(operator.mul, i, 1)

def f(k):
    s=Solver()
    a=[Int("%d" % i) for i in range(k)]
    #a=[BitVec("%d" % i, 32) for i in range(k)]
    for i in range(k):
        s.add(a[i]>0)
    #for i in range(k):
    #    s.add(a[i]<10)
    for i in range(k-1):
        s.add(a[i]<=a[i+1])
    s.add(sum(a)==product(a))

    def print_model(): 
        print (f"{k=}", ", as list:", " ".join(list(map(str, [m[a[i]].as_long() for i in range(k)]))))
        sys.stdout.flush()

    # enumerate all possible solutions:
    results=[]
    while True:
        if s.check()==sat:
            if len(results)==1: # already have one solution
                return False
            m=s.model()
            print_model()

            results.append(m)
            block=[]
            for d in m:
                c=d()
                block.append(c!=m[d])
            s.add(Or(block))
        else:
            if len(results)==1: # have only one solution
                return True
            else:
                return False

for i in range(2, 5+1):
    if f(i):
        print (f"only one solution, k={i}")
    sys.stdout.flush()