(meta-info (comment "Ctrl example from examples-transformed/fact.ctrs"))
(format LCTRS :logic QF_NIA)

(fun fact1 1 :sort (Int  Int))
(fun u 3 :sort (Int Int Int  Int))
(rule (u  n i z) (u  n (+  i 1) (*  z i)) :guard (<= i n))
(rule (u  n i z) z :guard (not (<= i n)))
(rule (fact1  n) (u  n 1 1))