fork download
  1. F=\
  2. lambda t,y:next((b for a,b in t if all(c(a,p(y)[0],{}))),0)
  3. T=type
  4. def p(s,c=0):
  5. q,n=[],0
  6. while s and(c<1or')'!=s[0]):
  7. S=s[0];n+=S=='!'
  8. if S.isalpha():q+=[n,S],;n=0
  9. if'('==S:t,s=p(s[1:],1);q+=(n,t),;n=0
  10. s=s[1:]
  11. return q,s
  12. def c(a,b,d):
  13. if T(a)==T(b):
  14. for x,y in zip(a,b):
  15. p,q=x;n,m=y;z=p<1or p%2==n%2
  16. if T(x)==list:yield all([d.get(q,m)==m,z]);d[q]=m
  17. if T(x)==tuple:yield all([T(y)==tuple,z,*c(q,m,d)])
  18.  
  19. axioms="""a>(b>a); A
  20. (a>(b>c))>((a>b)>(a>c)); B
  21. (!a>!b)>(b>a); C"""
  22. cases="""
  23. (b>!c)>(c>(b>!c)); A
  24. (a>(a>a))>((a>a)>(a>a)); B
  25. (a>(b>!!!!!c))>((a>b)>(a>!!!!!c)); B
  26. (!a>!b)>(b>a); C
  27. a>(b>c); 0
  28. (!(a>(b>!c))>!(c>c))>((c>c)>(a>(b>!c))); C"""
  29. def a_temp(d):
  30. return [[p((t:=i.split('; '))[0])[0], t[1]] for i in filter(None, d.split('\n'))]
  31.  
  32. for i in filter(None, cases.split('\n')):
  33. x, y = i.split('; ')
  34. print(F(a_temp(axioms), x), y)
Success #stdin #stdout 0.13s 14100KB
stdin
Standard input is empty
stdout
A A
B B
B B
C C
0 0
C C