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

Elapsed Time:  62.46 ms