YES
LCTRS
  Theories
    Core, Ints
  Sorts
    Unit
  Signature
    a: Unit
    b: Unit
    c: Unit
    f: Int -> Unit
    g: Int -> Unit
    h: Int -> Unit
  Rules
    f(!x) -> g(!x) [>=(!x, 0)]
    f(!x) -> h(!x) [<=(!x, 2)]
    g(1) -> a
    g(!x) -> b [>=(!x, 2)]
    g(!x) -> c [<(!x, 1)]
    h(!x) -> a [<=(!x, 1)]
    h(!x) -> b [>(!x, 1)]
* DPGraph approximation on the DP problem
  dependency pairs:
    {f#(!x) -> g#(!x) [>=(!x, 0)], f#(!x) -> h#(!x) [<=(!x, 2)]}
  rules:
    {f(!x) -> g(!x) [>=(!x, 0)]
    , f(!x) -> h(!x) [<=(!x, 2)]
    , g(1) -> a
    , g(!x) -> b [>=(!x, 2)]
    , g(!x) -> c [<(!x, 1)]
    , h(!x) -> a [<=(!x, 1)]
    , h(!x) -> b [>(!x, 1)]}
resulting in the DP graph
  DPGraph with indexed dependency pairs
    {1: f#(!x) -> g#(!x) [>=(!x, 0)], 2: f#(!x) -> h#(!x) [<=(!x, 2)]}
  and edges
    1 -> {}
    2 -> {}
with 0 SCC(s)
  

Elapsed Time:   6.32 ms