YES
LCTRS
  Theories
    Core, Ints
  Signature
    a: Int
    b: Int
    f: Int -> Int
    g: Int -> Int
  Rules
    a -> f(!n) [>=(!n, 0)]
    a -> g(!n) [>=(!n, 0)]
    f(!n) -> b [!n = 0]
    g(!n) -> b [!n = 0]
    f(!n) -> f(!m) [and(>(!n, 0), *(2, !m) = !n)]
    f(!n) -> f(!m) [and(>(!n, 0), +(*(2, !m), 1) = !n)]
    g(!n) -> g(!m) [and(>(!n, 0), *(2, !m) = !n)]
    g(!n) -> g(!m) [and(>(!n, 0), +(*(2, !m), 1) = !n)]
* DPGraph approximation on the DP problem
  dependency pairs:
    {a# -> f#(!n) [>=(!n, 0)]
    , a# -> g#(!n) [>=(!n, 0)]
    , f#(!n) -> f#(!m) [and(>(!n, 0), =(*(2, !m), !n))]
    , f#(!n) -> f#(!m) [and(>(!n, 0), =(+(*(2, !m), 1), !n))]
    , g#(!n) -> g#(!m) [and(>(!n, 0), =(*(2, !m), !n))]
    , g#(!n) -> g#(!m) [and(>(!n, 0), =(+(*(2, !m), 1), !n))]}
  rules:
    {a -> f(!n) [>=(!n, 0)]
    , a -> g(!n) [>=(!n, 0)]
    , f(!n) -> b [=(!n, 0)]
    , g(!n) -> b [=(!n, 0)]
    , f(!n) -> f(!m) [and(>(!n, 0), =(*(2, !m), !n))]
    , f(!n) -> f(!m) [and(>(!n, 0), =(+(*(2, !m), 1), !n))]
    , g(!n) -> g(!m) [and(>(!n, 0), =(*(2, !m), !n))]
    , g(!n) -> g(!m) [and(>(!n, 0), =(+(*(2, !m), 1), !n))]}
resulting in the DP graph
  DPGraph with indexed dependency pairs
    {1: a# -> f#(!n) [>=(!n, 0)]
    , 2: a# -> g#(!n) [>=(!n, 0)]
    , 3: f#(!n) -> f#(!m) [and(>(!n, 0), =(*(2, !m), !n))]
    , 4: f#(!n) -> f#(!m) [and(>(!n, 0), =(+(*(2, !m), 1), !n))]
    , 5: g#(!n) -> g#(!m) [and(>(!n, 0), =(*(2, !m), !n))]
    , 6: g#(!n) -> g#(!m) [and(>(!n, 0), =(+(*(2, !m), 1), !n))]}
  and edges
    1 -> {3, 4}
    2 -> {5, 6}
    3 -> {3, 4}
    4 -> {3, 4}
    5 -> {5, 6}
    6 -> {5, 6}
with 2 SCC(s)
  SCC:
    {g#(!n) -> g#(!m) [and(>(!n, 0), =(*(2, !m), !n))]
    , g#(!n) -> g#(!m) [and(>(!n, 0), =(+(*(2, !m), 1), !n))]}
  SCC:
    {f#(!n) -> f#(!m) [and(>(!n, 0), =(*(2, !m), !n))]
    , f#(!n) -> f#(!m) [and(>(!n, 0), =(+(*(2, !m), 1), !n))]}
* RPO with precedence:
  {g#}
* DPGraph approximation on the DP problem
  dependency pairs:
    {g#(!n) -> g#(!m) [and(>(!n, 0), =(+(*(2, !m), 1), !n))]}
  rules:
    {}
resulting in the DP graph
  DPGraph with indexed dependency pairs
    {1: g#(!n) -> g#(!m) [and(>(!n, 0), =(+(*(2, !m), 1), !n))]}
  and edges
    1 -> {1}
with 1 SCC(s)
  SCC:
    {g#(!n) -> g#(!m) [and(>(!n, 0), =(+(*(2, !m), 1), !n))]}
* RPO with precedence:
  {g#}
* RPO with precedence:
  {f#}
* DPGraph approximation on the DP problem
  dependency pairs:
    {f#(!n) -> f#(!m) [and(>(!n, 0), =(+(*(2, !m), 1), !n))]}
  rules:
    {}
resulting in the DP graph
  DPGraph with indexed dependency pairs
    {1: f#(!n) -> f#(!m) [and(>(!n, 0), =(+(*(2, !m), 1), !n))]}
  and edges
    1 -> {1}
with 1 SCC(s)
  SCC:
    {f#(!n) -> f#(!m) [and(>(!n, 0), =(+(*(2, !m), 1), !n))]}
* RPO with precedence:
  {f#}

Elapsed Time:  97.16 ms