(meta-info (comment "Example 2 from Kop et al. 2013"))
(format LCTRS :logic QF_LIA)
(fun sum 1 :sort (Int Int))
(fun sum2 2 :sort (Bool Int Int))
(fun geq 2 :sort (Int Int Bool))
(fun s 1 :sort (Int Int))
(fun plus 2 :sort (Int Int Int))
(fun p 1 :sort (Int Int))
(fun geq2 4 :sort (Int Int Int Int Bool))

(rule (sum x) (sum2 (geq 0 x) x))
(rule (sum2 true x) 0)
(rule (sum2 false (s x)) (plus (s x) (sum x)))
(rule (plus (p x) y) (p (plus x y)))
(rule (plus (s x) y) (s (plus x y)))
(rule (plus 0 y) y)
(rule (s (p x)) x)
(rule (p (s x)) x)
(rule (geq x y) (geq2 x y 0 0))
(rule (geq2 (s x) y z u) (geq2 x y (s z) u))
(rule (geq2 (p x) y z u) (geq2 x y z (s u)))
(rule (geq2 0 (s x) y z) (geq2 0 x y (s z)))
(rule (geq2 0 (p x) y z) (geq2 0 x (s y) z))
(rule (geq2 0 0 (s x) (s y)) (geq2 0 0 x y))
(rule (geq2 0 0 x 0) true)
(rule (geq2 0 0 0 (s x)) false)