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

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

(rule (log x y) (lif x y))
(rule (lif x y) (+ 1 (log (/ x y) y)) :guard (and (>= x y) (> y 1)))
(rule (lif x y) 0 :guard (not (and (>= x y) (> y 1))))