YES LCTRS Theories Core, Ints Signature a: Int c: Int -> Int f: Int -> Int g: Int -> Int Rules c(!x) -> f(!x) [and(<=(1, !x), <=(!x, 10))] c(!x) -> g(!x) [and(<=(1, !x), <=(!x, 10))] f(!x) -> a [and(<=(1, !x), <=(!x, 5))] f(!x) -> a [and(<=(6, !x), <=(!x, 10))] g(!x) -> a [and(<=(1, !x), <=(!x, 5))] g(!x) -> a [and(<=(6, !x), <=(!x, 10))] DPGraph with indexed dependency pairs {1: c#(!x) -> f#(!x) [and(<=(1, !x), <=(!x, 10))] , 2: c#(!x) -> g#(!x) [and(<=(1, !x), <=(!x, 10))]} and edges 1 -> {} 2 -> {} with 0 SCC(s) Elapsed Time: 28.46 ms