#===================================================
#
#  Examples for RQE based geometrical inequality proving - SMT-LIB file [2]
#    
#   It meant to be as an input formula for a solver as SMT-RAT or Z3 etc.
#    
#  Version 2.0 - 17/04/20
#===================================================

#===================================================

#1: Bottema1.1b IsoscelesCF 

(set-logic QF_NRA)
(declare-const b Real)
(assert (> (* 2 b) 1))
(assert (<  (* (+ (* 2 b) 1)  (+ (* 2 b) 1) )  (* 3 (+ (* b b) (* 2 b)) )  ))
(check-sat)
(exit) 

(set-logic QF_NRA)
(declare-const b Real)
(assert (> (* 2 b) 1))
(assert (>=  (* (+ (* 2 b) 1)  (+ (* 2 b) 1) )  (* 4 (+ (* b b) (* 2 b)) )  ))
(check-sat)
(exit) 

(set-logic QF_NRA)
(declare-const b Real)
(declare-const m Real)
(assert (or  (< m 3)  (>= m 4)))
(assert (> (* 2 b) 1))
(assert (=  (* (+ (* 2 b) 1)  (+ (* 2 b) 1) )  (* m (+ (* b b) (* 2 b)) )  ))
(check-sat)
(exit)