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

(fun log 2 :sort (Int Int Int))
(fun lif 3 :sort (Bool Int Int Int))
(fun / 2 :sort (Int Int Int))

(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)
(rule (/ x y) z :guard (= x (* y z)))