(declare-const c Int)
(declare-const l Int)
(declare-const a Int)
(declare-const r Int)
(declare-const k Int)
(declare-const s Int)
(declare-const o Int)
(declare-const n Int)

(assert (and (>= c 0) (<= c 9)))
(assert (and (>= l 0) (<= l 9)))
(assert (and (>= a 0) (<= a 9)))
(assert (and (>= r 0) (<= r 9)))
(assert (and (>= k 0) (<= k 9)))
(assert (and (>= s 0) (<= s 9)))
(assert (and (>= o 0) (<= o 9)))
(assert (and (>= n 0) (<= n 9)))

(assert (not (= c l)))
(assert (not (= c a)))
(assert (not (= c r)))
(assert (not (= c k)))
(assert (not (= c s)))
(assert (not (= c o)))
(assert (not (= c n)))
(assert (not (= l a)))
(assert (not (= l r)))
(assert (not (= l k)))
(assert (not (= l s)))
(assert (not (= l o)))
(assert (not (= l n)))
(assert (not (= a r)))
(assert (not (= a k)))
(assert (not (= a s)))
(assert (not (= a o)))
(assert (not (= a n)))
(assert (not (= r k)))
(assert (not (= r s)))
(assert (not (= r o)))
(assert (not (= r n)))
(assert (not (= k s)))
(assert (not (= k o)))
(assert (not (= k n)))
(assert (not (= s o)))
(assert (not (= s n)))
(assert (not (= o n)))

; r + n = s,
; or r + n = s + 10
(assert (or (= (+ r n) s) (= (+ r n) (+ s 10))))

; a + o = s,
; or a + o = s + 10,
; or r + n > 9 and a + o + 1 = s,
; or r + n > 9 and a + o + 1 = s + 10
(assert (or
  (= (+ a o) s)
  (= (+ a o) (+ s 10))
  (and (> (+ r n) 9) (= (+ a o 1) s))
  (and (> (+ r n) 9) (= (+ a o 1) (+ s 10)))
))

; l + s = a,
; or l + s = a + 10,
; or a + o > 9 and l + s + 1 = a,
; or a + o > 9 and l + s + 1 = a + 10
(assert (or
  (= (+ l s) a)
  (= (+ l s) (+ a 10))
  (and (> (+ a o) 9) (= (+ l s 1) a))
  (and (> (+ a o) 9) (= (+ l s 1) (+ a 10)))
))

; c + k = l + 10,
; or c + k + 1 = l + 10
(assert (or
  (= (+ c k) (+ l 10))
  (and (> (+ l s) 9) (= (+ c k 1) (+ l 10)))
))

; c must be 1 since the sum is a 5 digit number
(assert (= c 1))

; k cannot be 0 - no leading zeros
(assert (not (= k 0)))

(check-sat)
(get-model)