(meta-info (comment "Example 12 from Kop et al. 2013"))
(format LCTRS :logic QF_LRA)

(fun sumroot 1 :sort (Real Real))
(fun sqrt 1 :sort (Real Real))

(rule (sumroot x) 0 :guard (>= 0 x))
(rule (sumroot x) (+ (sqrt x) (sumroot  (- x 1))) :guard (not (>= 0 x)))