#!/usr/bin/python2.7

from z3 import *

def main():
    s1, s2, s3, s5, s6, s7, s9, s11, s12, s13, s14, s15 = Ints('s1, s2, s3, s5, s6, s7, s9, s11, s12, s13, s14, s15')
    solve(((((s1 * 5) + 500) / 10) == ord('K')) and (((s1 * 2) - 3) == ord('a')) and ((s1 + v6) == ord('i')))
    solve((((s2 / 2) * 3) + 2) == ord('e'))
    solve(((s3 * 2) == ord('r')))
    solve(((((s5 * 3) + 2) / 2) == ord('L')))
    solve((s6 == 55))
    solve((((s7 + 83) / 2) == ord('S')))
    solve((((s9 * 2) + 1) / 3) == ord('1'))
    solve((s11 == 83))
    solve((((s12 * 2) - 1) == ord('_')))
    solve((s13 == ord('R')))
    solve(((((102 - s14) + 54) / 2) == ord('3')))
    solve(((s15 + 40) == ord('l')))

if __name__ == "__main__":
    main()