import itertools, random, sys
nw=int(sys.argv[1]) if len(sys.argv)>1 else 2
W=range(nw)
PROPS=list(itertools.product([0,1],repeat=nw))
def cl(F,w):
    t=F[0]
    if t=='atom': return F[1][w]
    if t=='trig': return F[1][w] & F[2][w]
    if t=='not': return 1-cl(F[1],w)
    if t=='and': return cl(F[1],w)&cl(F[2],w)
    if t=='or': return cl(F[1],w)|cl(F[2],w)
    if t=='imp': return (1-cl(F[1],w))|cl(F[2],w)
def dyn(C,F):
    t=F[0]
    if t=='atom': return frozenset(w for w in C if F[1][w])
    if t=='trig':
        if any(not F[1][w] for w in C): return None
        return frozenset(w for w in C if F[2][w])
    if t=='not':
        D=dyn(C,F[1]); return None if D is None else C-D
    if t=='and':
        D=dyn(C,F[1]); 
        if D is None: return None
        return dyn(D,F[2])
    if t=='or':
        D=dyn(C,F[1])
        if D is None: return None
        E=dyn(C-D,F[2])
        return None if E is None else D|E
    if t=='imp':
        D=dyn(C,F[1])
        if D is None: return None
        E=dyn(D,F[2])
        if E is None: return None
        return C-(D-E)
def occs(F):
    t=F[0]
    if t=='atom': return []
    if t=='trig': return [([],F)]
    if t=='not': return [([('not',)]+K,x) for K,x in occs(F[1])]
    r=[]
    for K,x in occs(F[1]): r.append(([(t,'L',F[2])]+K,x))
    for K,x in occs(F[2]): r.append(([(t,'R',F[1])]+K,x))
    return r
def plug(K,X):
    for fr in reversed(K):
        if fr[0]=='not': X=('not',X)
        elif fr[1]=='L': X=(fr[0],X,fr[2])
        else: X=(fr[0],fr[2],X)
    return X
def variants(K, sibs):
    # replace L-frames' right sibling by any atom in sibs (prefix-preserving)
    idx=[i for i,fr in enumerate(K) if fr[0]!='not' and fr[1]=='L']
    for choice in itertools.product(sibs,repeat=len(idx)):
        K2=list(K)
        for i,c in zip(idx,choice):
            K2[i]=(K[i][0],'L',('atom',c))
        yield K2
def transp(C,F,inc=True):
    for K,x in occs(F):
        Ks = variants(K,PROPS) if inc else [K]
        for K2 in Ks:
            for g in PROPS:
                A=plug(K2,('and',('atom',x[1]),('atom',g)))  # (d and g) ; note atom&atom classical
                B=plug(K2,('atom',g))
                for w in C:
                    if cl(A,w)!=cl(B,w): return False
    return True
def symbols_tokens(F,number):
    # returns list of tokens (a,b) in order
    t=F[0]
    if t=='atom': return []
    if t=='trig': return [(F[1],F[2])]
    r=[]
    for c in F[1:]: r+=symbols_tokens(c,number)
    return r
def evalv(F,w,val,ctr):
    # val: function token-key -> bool ; ctr list for numbering if numbered
    t=F[0]
    if t=='atom': return F[1][w]
    if t=='trig':
        return val(F)
    if t=='not': return 1-evalv(F[1],w,val,ctr)
    a=evalv(F[1],w,val,ctr); b=evalv(F[2],w,val,ctr)
    if t=='and': return a&b
    if t=='or': return a|b
    return (1-a)|b
def super_val(F,w,tied=True):
    toks=symbols_tokens(F,None)
    keys=sorted(set(toks)) if tied else list(range(len(toks)))
    free=[]
    # symbol free at w if p(w)==0
    fixed={}
    for i,(a,b) in enumerate(toks):
        k=(a,b) if tied else i
        if a[w]: fixed[k]=b[w]
        else: fixed[k]=None
    fk=[k for k in fixed if fixed[k] is None]
    vals=set()
    for asg in itertools.product([0,1],repeat=len(fk)):
        d=dict(fixed); d.update(dict(zip(fk,asg)))
        if tied:
            v=evalv(F,w,lambda T: d[(T[1],T[2])],None)
        else:
            cnt=[0]
            def val(T):
                k=cnt[0]; cnt[0]+=1; return d[k]
            v=evalv(F,w,val,cnt)
        vals.add(v)
    return vals.pop() if len(vals)==1 else '#'
def sk(F,w):
    t=F[0]
    if t=='atom': return F[1][w]
    if t=='trig': return F[2][w] if F[1][w] else '#'
    if t=='not':
        a=sk(F[1],w); return '#' if a=='#' else 1-a
    a=sk(F[1],w); b=sk(F[2],w)
    if t=='and':
        if a==0 or b==0: return 0
        if a=='#' or b=='#': return '#'
        return 1
    if t=='or':
        if a==1 or b==1: return 1
        if a=='#' or b=='#': return '#'
        return 0
    if a==0 or b==1: return 1
    if a=='#' or b=='#': return '#'
    return 0
def acc(C,F,mode,inc=True):
    for K,x in occs(F):
        Ks = variants(K,PROPS) if inc else [K]
        for K2 in Ks:
            G=plug(K2,x)
            for w in C:
                if mode=='K': v=super_val(G,w,False)
                elif mode=='S': v=super_val(G,w,True)
                else: v=sk(G,w)
                if v=='#': return False
    return True
def rnd(d):
    if d==0 or random.random()<0.25:
        if random.random()<0.6:
            return ('trig',random.choice(PROPS[:]),random.choice(PROPS))
        return ('atom',random.choice(PROPS))
    r=random.random()
    if r<0.2: return ('not',rnd(d-1))
    return (random.choice(['and','or','imp']),rnd(d-1),rnd(d-1))
def subsets():
    for r in range(1,nw+1):
        for c in itertools.combinations(W,r): yield frozenset(c)
random.seed(int(sys.argv[2]) if len(sys.argv)>2 else 0)
N=int(sys.argv[3]) if len(sys.argv)>3 else 20000
bad={}
for _ in range(N):
    F=rnd(3)
    for C in subsets():
        D=dyn(C,F); ti=transp(C,F,True)
        if (D is not None)!=ti: bad.setdefault('thm1',(C,F))
        if D is not None and D!=frozenset(w for w in C if cl(F,w)): bad.setdefault('thm1ii',(C,F))
        ka=acc(C,F,'K'); sa=acc(C,F,'S'); ska=acc(C,F,'SK')
        if ka!=ska: bad.setdefault('kleene_vs_SK',(C,F))
        if ka!=sa: bad.setdefault('thm36',(C,F))
        if ti and not ka: bad.setdefault('thm38a',(C,F))
        for w in C:
            if super_val(F,w,False)!=sk(F,w): bad.setdefault('thm41',(C,F,w))
print(bad)