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

(fun log 2 :sort (Real Real Real))
(fun lif 3 :sort (Bool Real Real Real))

(rule (log x y) (lif (and (>= x y) (> y 1)) x y))
(rule (lif true x y) (+ 1 (log (/ x y) y)))
(rule (lif false x y) 0)