(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)
which gives
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