(declare-const f0 Int) ; f
(declare-const f1 Int)

(assert (>= f0 0))
(assert (> f1 0))
(assert (> f0 (+ f0 (* f1 f0))))
(assert (>= f1 (* f1 f1)))

(check-sat)
(get-value (f0 f1))