; @author Jonas Schöpf
; this LCTRS needs splitting in order to be analyzed properly
(format LCTRS :smtlib 2.6)
(theory Ints)

(fun f (-> Int Int))
(fun g (-> Int Int))
(fun a Int)
(fun c Int)

(rule c (f x) :guard (and (<= 1 x) (<= x 10)))
(rule c (g x) :guard (and (<= 1 x) (<= x 10)))
(rule (f x) a :guard (and (<= 1 x) (<= x 5)))
(rule (f x) a :guard (and (<= 6 x) (<= x 10)))
(rule (g x) a :guard (and (<= 1 x) (<= x 5)))
(rule (g x) a :guard (and (<= 6 x) (<= x 10)))
