NO
LCTRS
  Theories
    Core, Ints
  Signature
    f: (Int, Int) -> Int
    g: (Int, Int) -> Int
    h: Int -> Int
  Rules
    f(?8, ?9) -> g(?8, +(1, 1))
    f(?10, ?11) -> h(g(?11, +(1, 1)))
Not confluent by "two different NFs found" with proof:
  * Critical Pair
    Inner Rule
      f(?10', ?11') -> h(g(?11', +(1, 1)))
    Outer Rule
      f(?8", ?9") -> g(?8", +(1, 1))
    Pair
      h(g(?9", +(1, 1))) ≈ g(?8", +(1, 1))
  reaches the non-trivial normal form
    h(g(?9", +(1, 1))) ≈ g(?8", +(1, 1)) 
      ->^* h(g(?9", ?126')) ≈ g(?8", +(1, 1)) [?126' = +(1, 1)]
      -> h(g(?9", ?126')) ≈ g(?8", ?144') [?126' = +(1, 1), ?144' = +(1, 1)]

Elapsed Time:  72.56 ms