VeXocide

    (define d::int)
    (define e::int)
    (define m::int)
    (define n::int)
    (define o::int)
    (define r::int)
    (define s::int)
    (define y::int)

    (assert
       (and
          (and (>= d 0) (<= d 9))
          (and (>= e 0) (<= e 9))
          (and (>= m 0) (<= m 9))
          (and (>= n 0) (<= n 9))
          (and (>= o 0) (<= o 9))
          (and (>= r 0) (<= r 9))
          (and (>= s 0) (<= s 9))
          (and (>= y 0) (<= y 9))
          (and (/= d e) (/= d m) (/= d n) (/= d o) (/= d r) (/= d s) (/= d y))
          (and (/= e m) (/= e n) (/= e o) (/= e r) (/= e s) (/= e y))
          (and (/= m n) (/= m o) (/= m r) (/= m s) (/= m y))
          (and (/= n o) (/= n r) (/= n s) (/= n y))
          (and (/= o r) (/= o s) (/= o y))
          (and (/= r s) (/= r y))
          (/= s y)
          (=
             (+
                (+ (* s 1000) (* e 100) (* n 10) d)
                (+ (* m 1000) (* o 100) (* r 10) e)
             )
             (+ (* m 10000) (* o 1000) (* n 100) (* e 10) y)
          )
       )
    )

    (check)
    (show-model)

    sat
    (= m 1)
    (= r 8)
    (= y 2)
    (= o 0)
    (= s 9)
    (= n 6)
    (= d 7)
    (= e 5)
    ./bin/yices money.ys  0.01s user 0.00s system 76% cpu 0.012 total

    ProxyCommand ssh -T host1 'nc %h %p'

    ProxyCommand ssh -W %h:%p host1

    31 c0             xor %eax, %eax

    b8 00 00 00 00    mov $0, %eax