YES
LCTRS
  Theories
    Core, Ints
  Signature
    f: Int -> Int
    g: Int -> Int
    h: Int -> Int
  Rules
    f(!x) -> 2 [and(<=(1, !x), <=(!x, 3))]
    f(!x) -> g(!x) [and(<=(2, !x), <=(!x, 4))]
    g(!x) -> h(!x)
    h(!x) -> !y [and(!x = 2, !y = !x)]
    h(!x) -> !y [and(!x = 3, !y = 2)]
DPGraph with indexed dependency pairs
  {1: f#(!x) -> g#(!x) [and(<=(2, !x), <=(!x, 4))], 2: g#(!x) -> h#(!x)}
and edges
  1 -> {2}
  2 -> {}
with 0 SCC(s)
  

Elapsed Time:  29.25 ms