-rwxr-xr-x 2704 djbsort-20180729/verif/tryinput
#!/usr/bin/env python3

import re
import sys
import hashlib
import struct

n = int(sys.argv[1])

original = []

for i in range(n):
  h = hashlib.sha256()
  h.update(str([n,i]).encode('utf-8'))
  h = h.digest()
  h = h[:4]
  h = struct.unpack('<L',h)[0]
  original += [h]
  print('in_%d_32 = [32,%d]' % (i,h))

print("""
def constant(x,y):
  return x,y

# python keywords include 'and', 'or'
def __and__(x,y):
  assert x[0] == y[0]
  return x[0],x[1] & y[1]

def __or__(x,y):
  assert x[0] == y[0]
  return x[0],x[1] | y[1]

def xor(x,y):
  assert x[0] == y[0]
  return x[0],x[1] ^ y[1]

def invert(x):
  return x[0],2**x[0] - 1 - x[1]

def add(x,y):
  assert x[0] == y[0]
  return x[0],(x[1] + y[1]) % (2**x[0])

def sub(x,y):
  assert x[0] == y[0]
  return x[0],(x[1] - y[1]) % (2**x[0])

def mul(x,y):
  assert x[0] == y[0]
  return x[0],(x[1] * y[1]) % (2**x[0])

def equal(x,y):
  assert x[0] == y[0]
  return 1,x[1] == y[1]

def signedmin(x,y):
  b = x[0]
  assert b == y[0]
  flip = 2**(b-1)
  xsigned = x[1] ^ flip
  ysigned = y[1] ^ flip
  zsigned = min(xsigned,ysigned)
  return b,zsigned ^ flip

def signedmax(x,y):
  b = x[0]
  assert b == y[0]
  flip = 2**(b-1)
  xsigned = x[1] ^ flip
  ysigned = y[1] ^ flip
  zsigned = max(xsigned,ysigned)
  return b,zsigned ^ flip

def signedle(x,y):
  b = x[0]
  assert b == y[0]
  flip = 2**(b-1)
  xsigned = x[1] ^ flip
  ysigned = y[1] ^ flip
  return 1,xsigned <= ysigned

def signedlt(x,y):
  b = x[0]
  assert b == y[0]
  flip = 2**(b-1)
  xsigned = x[1] ^ flip
  ysigned = y[1] ^ flip
  return 1,xsigned < ysigned

def signedrshift(x,y):
  b = x[0]
  assert b == y[0]
  flip = 2**(b-1)
  xsigned = (x[1] ^ flip) - flip
  ysigned = (y[1] ^ flip) - flip
  assert 0 <= ysigned
  assert ysigned < b
  zsigned = xsigned >> ysigned
  return b,(zsigned + flip) ^ flip

def Extract(x,top,bot):
  assert x[0] > top
  assert top > bot
  assert bot >= 0
  return top + 1 - bot,((x[1] & ((2 << top) - 1)) >> bot)

def Reverse(x):
  b = x[0]
  assert b % 8 == 0
  bytes = []
  for j in range(b//8):
    bytes += [255 & (x[1] >> (8*j))]
  bytes.reverse()
  return b,sum(bytes[j] * 256**j for j in range(b//8))

def If(c,x,y):
  assert x[0] == y[0]
  assert c[0] == 1
  if c[1]: return x
  return y
  
def Concat(*args):
  pos,value = 0,0
  for arg in reversed(args):
    pos,value = pos + arg[0],value + (arg[1] << pos)
  return pos,value
""")

program = sys.stdin.read()
program = re.sub(' and\(',' __and__(',program)
program = re.sub(' or\(',' __or__(',program)
print(program)

flip = 2**31
original = [x ^ flip for x in original]
original.sort()
original = [x ^ flip for x in original]

for i in range(n):
  print('assert out%d[1] == %d' % (i,original[i]))