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

Elapsed Time: 417.82 ms