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

(fun eval1 2 :sort (Int Int Int))
(fun eval2 2 :sort (Int Int Int))
(fun eval3 2 :sort (Int Int Int))

(rule (eval1 x y) (eval2 x y) :guard (and (and (> x 0) (> y 0)) (> x y)))
(rule (eval1 x y) (eval3 x y) :guard (and (and (> x 0) (> y 0)) (not (> x y))))
(rule (eval2 x y) (eval2 (+ x (-1)) (+ y 1)) :guard (> x 0))
(rule (eval2 x y) (eval1 x y) :guard (not (> x 0)))
(rule (eval3 x y) (eval3 (+ x 1) (+ y (-1))) :guard (> y 0))
(rule (eval3 x y) (eval1 x y) :guard (not (> y 0)))