reduce-algebra/generic/rlsmt/example1.smt2

(set-option :print-success false)
(set-logic QF_NRA)
(set-option :produce-models true)
(set-option :model-values "approximately")
(assert (<= (* v5 (+ (* v26 (* v26 (+ (/ 1 6) (* v26 (* v26 (+ (- (/ 1 120)) (* v26 (* v26 (+ (/ 1 5040) (* v26 (* v26 (+ (- (/ 1 362880)) (* v26 (* v26 (+ (/ 1 39916800) (* v26 (* v26 (+ (- (/ 1 6227020800)) (* v26 (* (/ 1 1307674368000) v26)))))))))))))))))))) (* v5 (* v5 (+ (- (/ 1 6)) (* v5 (* v5 (+ (/ 1 120) (* v5 (* v5 (+ (- (/ 1 5040)) (* v5 (* (/ 1 362880) v5))))))))))))) 0))
(assert (not (<= (* v5 (* v5 (+ (* (- (/ 1 6)) v26) (* v5 (* v5 (+ (* (/ 1 120) v26) (* v5 (* v5 (+ (* (- (/ 1 5040)) v26) (* v5 (* v5 (* (/ 1 362880) v26)))))))))))) (* v26 (* v26 (* v26 (+ (- (/ 1 6)) (* v26 (* v26 (+ (/ 1 120) (* v26 (* v26 (+ (- (/ 1 5040)) (* v26 (* v26 (+ (/ 1 362880) (* v26 (* (- (/ 1 39916800)) v26))))))))))))))))))
(assert (not (<= (* v5 (+ (* v26 (* v26 (+ (/ 1 6) (* v26 (* v26 (+ (- (/ 1 120)) (* v26 (* (/ 1 5040) v26)))))))) (* v5 (* v5 (+ (- (/ 1 6)) (* v5 (* v5 (+ (/ 1 120) (* v5 (* v5 (+ (- (/ 1 5040)) (* v5 (* (/ 1 362880) v5))))))))))))) 0)))
(assert (not (<= (* v5 (* v5 (+ (* (- (/ 1 6)) v26) (* v5 (* v5 (* (/ 1 120) v26)))))) (* v26 (* v26 (* v26 (+ (- (/ 1 6)) (* v26 (* v26 (+ (/ 1 120) (* v26 (* (- (/ 1 5040)) v26))))))))))))
(assert (not (<= (* v5 (+ (* v26 (* (/ 1 6) v26)) (* v5 (* v5 (+ (- (/ 1 6)) (* v5 (* (/ 1 120) v5))))))) 0)))
(assert (not (<= v26 0)))
(assert (not (<= v137 (/ 15707963 5000000))))
(assert (not (<= (/ 31415927 10000000) v137)))
(assert (<= v5 (* (/ 1 2) v137)))
(assert (<= 0 v26))
(assert (not (<= v5 v26)))
(check-sat)
(get-model)