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

Elapsed Time:  48.48 ms