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

Elapsed Time: 207.62 ms