(declare-const a0 Int) ; append
(declare-const a1 Int)
(declare-const a2 Int)
(declare-const c0 Int) ; cons
(declare-const c1 Int)
(declare-const c2 Int)
(declare-const n0 Int) ; nil

(assert
 (and
  (>= a0 0)
  (> a1 0)
  (> a2 0)
  (>= c0 0)
  (> c1 0)
  (> c2 0)
  (>= c0 0)
  (> (+ a0 (* a1 n0)) 0)
  (>= a2 0)
  (>= (+ a0 (* a1 c0)) (+ c0 (* c2 a0)))
  (>= (* a1 c2) (* c2 a1))
  (>= a2 (* c2 a2))
 )
)

(check-sat)
(get-value (a0 a1 a2 c0 c1 c2 n0))