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 approximation on the DP problem
  dependency pairs:
    {f#(!x) -> g#(!x) [and(<=(2, !x), <=(!x, 4))], g#(!x) -> h#(!x)}
  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))]}
resulting in the DP graph
  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:  18.72 ms