import pycosat, time
def solve(cp, w, N):
    """Masked inverse problem: free neighbour trace e(t) for t<N, lit-phase coordinates constant
       (e(t+p)=e(t) at lit t), spatial inverse a_{k+1}(t)=a_k(t+1) XOR (a_k(t) OR a_{k-1}(t)),
       light cone a_k(t)=0 for k>w+t, start row has its leftmost lit cell at exactly -w."""
    p=len(cp); nv=[0]; cl=[]
    def new(): nv[0]+=1; return nv[0]
    T_=new(); cl.append([T_]); F_=-T_
    val={}
    for t in range(N+2): val[(0,t)]= T_ if cp[t%p] else F_
    for t in range(N): val[(1,t)]=new()
    for t in range(N-p):                                  # lit-phase coordinates repeat
        if cp[t%p]==1:
            a,b=val[(1,t)],val[(1,t+p)]; cl+= [[-a,b],[a,-b]]
    for k in range(1,N):
        for t in range(0,N-k):
            if (k,t+1) not in val or (k,t) not in val or (k-1,t) not in val: continue
            y=new(); x=val[(k,t+1)]; a=val[(k,t)]; b=val[(k-1,t)]
            o=new(); cl+= [[-a,o],[-b,o],[-o,a,b]]
            cl+= [[-y,x,o],[-y,-x,-o],[y,-x,o],[y,x,-o]]
            val[(k+1,t)]=y
    for (k,t),v in val.items():
        if k>w+t and k>=1: cl.append([-v])              # dark outside the light cone
    if (w,0) not in val: return None
    cl.append([val[(w,0)]])                              # leftmost lit lamp exactly at -w (nonzero, width w)
    return pycosat.solve(cl)!="UNSAT"
def death_time(cp,w,Nmax):
    lo,hi=1,Nmax
    if solve(cp,w,hi): return None
    while lo<hi:
        mid=(lo+hi)//2
        if solve(cp,w,mid): lo=mid+1
        else: hi=mid
    return lo
if __name__=="__main__":
    t0=time.time()
    for cp in ((0,0,1),(0,1)):
        row=[]
        for w in (4,8,12,16,20,24,28,32):
            d=death_time(cp,w,4*w+40)
            row.append(f"w={w}: {'NONE (hidden up to '+str(4*w+40)+')' if d is None else d}")
            if time.time()-t0>230: break
        print(f"Mia {''.join(map(str,cp))}: certified horizon by which no hidden configuration exists:  "+"  ".join(row),flush=True)
        if time.time()-t0>230: break