(meta-info (comment "Example 3 from Winkler et al. 2018"))
(format LCTRS :logic QF_LIA)

(fun fact 1 :sort (Int Int))

(rule (fact x) 1 :guard (<= x 0))
(rule (fact x) (* (fact (- x 1)) x) :guard (>= (- x 1) 0))