from z3 import *

set_param('parallel.enable',True)

inps=[Int(f"inp{i+1}") for i in range(14)]

curr_inppos=0
next_idx={"x": 0, "y": 0, "z": 0, "w": 0}
curr_v_m={}

s=Then('simplify','psmt').solver()

# Assert the given boolean clause
def c(clause):
    s.add(clause)
# Generate a new numbered var for the given base var (x1, x2, ...)
def new_v(base):
    curr_v_m[base]=Int(f"{base}{next_idx[base]}")
    next_idx[base]+=1
    return curr_v(base)
# Get the current numbered var for a given base var
def curr_v(v):
    if v in ["x","y","z","w"]:
        return curr_v_m[v]
    else:
        return int(v)

# Inputs are in range 1..9
for v in inps:
    c(v>=1)
    c(v<=9)

# Initialize x,y,z,w to zero
c(new_v("x")==0)
c(new_v("y")==0)
c(new_v("z")==0)
c(new_v("w")==0)

# Construct formula according to input
with open("in") as f:
    for l in f.readlines():
        lv=l.strip().split(" ")
        a=curr_v(lv[1])
        b=0
        if len(lv)>2:
            b=curr_v(lv[2])
        if lv[0]=="inp":
            c(new_v(lv[1])==inps[curr_inppos])
            curr_inppos+=1
        elif lv[0]=="add":
            c(new_v(lv[1])==a+b)
        elif lv[0]=="mul":
            c(new_v(lv[1])==a*b)
        elif lv[0]=="eql":
            nv=new_v(lv[1])
            c(Implies(a==b,nv==1))
            c(Implies(a!=b,nv==0))
        elif lv[0]=="mod":
            c(a>=0)
            c(b>0)
            c(new_v(lv[1])==a%b)
        elif lv[0]=="div":
            c(b!=0)
            c(new_v(lv[1])==a/b)
        else:
            raise("??!")

# Should end with z=0
c(curr_v("z")==0)

# Maximize by fixing one digit at a time
print('1: ',end='')
s.push()
for v in inps:
    for i in range(10,0,-1):
        s.push()
        c(v==i)
        if s.check()==sat:
            s.pop()
            c(v==i)
            print(str(i),end='')
            break
        else:
            s.pop()
            continue
s.pop()
# Minimize by fixing one digit at a time
print('\n2: ',end='')
s.push()
for v in inps:
    for i in range(1,10):
        s.push()
        c(v==i)
        if s.check()==sat:
            s.pop()
            c(v==i)
            print(str(i),end='')
            break
        else:
            s.pop()
            continue
s.pop()
print('')