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

Elapsed Time:  32.50 ms