F=\
lambda t,y:next((b for a,b in t if all(c(a,p(y)[0],{}))),0)
T=type
def p(s,c=0):
q,n=[],0
while s and(c<1or')'!=s[0]):
S=s[0];n+=S=='!'
if S.isalpha():q+=[n,S],;n=0
if'('==S:t,s=p(s[1:],1);q+=(n,t),;n=0
s=s[1:]
return q,s
def c(a,b,d):
if T(a)==T(b):
for x,y in zip(a,b):
p,q=x;n,m=y;z=p<1or p%2==n%2
if T(x)==list:yield all([d.get(q,m)==m,z]);d[q]=m
if T(x)==tuple:yield all([T(y)==tuple,z,*c(q,m,d)])
axioms="""a>(b>a); A
(a>(b>c))>((a>b)>(a>c)); B
(!a>!b)>(b>a); C"""
cases="""
(b>!c)>(c>(b>!c)); A
(a>(a>a))>((a>a)>(a>a)); B
(a>(b>!!!!!c))>((a>b)>(a>!!!!!c)); B
(!a>!b)>(b>a); C
a>(b>c); 0
(!(a>(b>!c))>!(c>c))>((c>c)>(a>(b>!c))); C"""
def a_temp(d):
return [[p((t:=i.split('; '))[0])[0], t[1]] for i in filter(None, d.split('\n'))]
for i in filter(None, cases.split('\n')):
x, y = i.split('; ')
print(F(a_temp(axioms), x), y)
Rj1cCmxhbWJkYSB0LHk6bmV4dCgoYiBmb3IgYSxiIGluIHQgaWYgYWxsKGMoYSxwKHkpWzBdLHt9KSkpLDApClQ9dHlwZQpkZWYgcChzLGM9MCk6CiBxLG49W10sMAogd2hpbGUgcyBhbmQoYzwxb3InKSchPXNbMF0pOgogIFM9c1swXTtuKz1TPT0nIScKICBpZiBTLmlzYWxwaGEoKTpxKz1bbixTXSw7bj0wCiAgaWYnKCc9PVM6dCxzPXAoc1sxOl0sMSk7cSs9KG4sdCksO249MAogIHM9c1sxOl0KIHJldHVybiBxLHMKZGVmIGMoYSxiLGQpOgogaWYgVChhKT09VChiKToKICBmb3IgeCx5IGluIHppcChhLGIpOgogICBwLHE9eDtuLG09eTt6PXA8MW9yIHAlMj09biUyCiAgIGlmIFQoeCk9PWxpc3Q6eWllbGQgYWxsKFtkLmdldChxLG0pPT1tLHpdKTtkW3FdPW0KICAgaWYgVCh4KT09dHVwbGU6eWllbGQgYWxsKFtUKHkpPT10dXBsZSx6LCpjKHEsbSxkKV0pCiAgIApheGlvbXM9IiIiYT4oYj5hKTsgQQooYT4oYj5jKSk+KChhPmIpPihhPmMpKTsgQgooIWE+IWIpPihiPmEpOyBDIiIiIApjYXNlcz0iIiIKKGI+IWMpPihjPihiPiFjKSk7IEEKKGE+KGE+YSkpPigoYT5hKT4oYT5hKSk7IEIKKGE+KGI+ISEhISFjKSk+KChhPmIpPihhPiEhISEhYykpOyBCCighYT4hYik+KGI+YSk7IEMKYT4oYj5jKTsgMAooIShhPihiPiFjKSk+IShjPmMpKT4oKGM+Yyk+KGE+KGI+IWMpKSk7IEMiIiIKZGVmIGFfdGVtcChkKToKCXJldHVybiBbW3AoKHQ6PWkuc3BsaXQoJzsgJykpWzBdKVswXSwgdFsxXV0gZm9yIGkgaW4gZmlsdGVyKE5vbmUsIGQuc3BsaXQoJ1xuJykpXQoKZm9yIGkgaW4gZmlsdGVyKE5vbmUsIGNhc2VzLnNwbGl0KCdcbicpKToKCXgsIHkgPSBpLnNwbGl0KCc7ICcpCglwcmludChGKGFfdGVtcChheGlvbXMpLCB4KSwgeSk=