NO
LCTRS
  Theories
    Core, Ints
  Sorts
    Unit
  Signature
    f: Int -> Unit
    g: Int -> Unit
    h: Int -> Unit
  Rules
    f(?12) -> g(?12)
    f(?13) -> h(?13) [and(<=(1, ?13), >=(?13, 2))]
    g(?14) -> h(1) [?14 = +(*(2, ?15), 1)]
    g(?16) -> h(2) [?16 = *(2, ?17)]
Not confluent by "two different NFs found" with proof:
  * Critical Pair
    Inner Rule
      f(?13') -> h(?13') [and(<=(1, ?13'), >=(?13', 2))]
    Outer Rule
      f(?12") -> g(?12")
    Pair
      h(?12") ≈ g(?12") [and(<=(1, ?12"), >=(?12", 2))]
  has the following instance
    Critical Pair
      Inner Rule
        f(?13') -> h(?13') [and(<=(1, ?13'), >=(?13', 2))]
      Outer Rule
        f(?12") -> g(?12")
      Pair
        h(?12") ≈ g(?12") [=(?12", +(*(2, ?253'), 1)), and(<=(1, ?12"), >=(?12", 2))]
  which reaches the non-trivial normal form
    h(?12") ≈ g(?12") [?12" = +(*(2, ?253'), 1), and(<=(1, ?12"), >=(?12", 2))]
      -> h(?12") ≈ h(1) [?12" = +(*(2, ?253'), 1), and(<=(1, ?12"), >=(?12", 2)), ?12" = +(*(2, ?265'), 1)]

Elapsed Time: 160.23 ms