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(!z, 0), 1), 1) [and(>(!x, 1), !z = -(!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#(!z, 0) [and(>(!x, 1), =(!z, -(!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(!z, 0), 1), 1) [and(>(!x, 1), =(!z, -(!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#(!z, 0) [and(>(!x, 1), =(!z, -(!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:  52.02 ms