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

(fun start 0 :sort ( Unit))
(fun f 1 :sort (Int  Unit))
(fun product 2 :sort (Unit Unit  Unit))

(rule (f  x) (product  (f  y) (f  z)) :guard (and (and (and (and (> x y) (> y 0)) (> x z)) (> z 0)) (= x (* y z))))
(rule start (f  input))