NO
LCTRS
  Theories
    Core, Ints
  Signature
    f: Int -> Int
    g: (Int, Int) -> Int
    h: Int -> Int
  Rules
    f(?14) -> g(?14, ?14) [<=(?14, 0)]
    g(?15, +(?15, ?16)) -> f(?16) [and(>(?15, 0), >(?16, 0))]
    g(f(?17), ?18) -> g(?17, ?19) [and(>(?17, 0), >(?19, ?17))]
    h(f(?20)) -> h(?20) [>=(?20, 0)]
Not confluent by "two different NFs found" with proof:
  * Critical Pair
    Inner Rule
      g(f(?17'), ?18') -> g(?17', ?19') [and(>(?17', 0), >(?19', ?17'))]
    Outer Rule
      g(f(?17"), ?18") -> g(?17", ?19") [and(>(?17", 0), >(?19", ?17"))]
    Pair
      g(?17", ?19') ≈ g(?17", ?19") [and(>(?17", 0), >(?19', ?17")), and(>(?17", 0), >(?19", ?17"))]
  reaches the non-trivial normal form
    g(?17", ?19') ≈ g(?17", ?19") [and(>(?17", 0), >(?19', ?17")), and(>(?17", 0), >(?19", ?17"))]

Elapsed Time: 101.72 ms