YES
LCTRS
  Theories
    Core, Ints
  Signature
    a: Int
    b: Int
    f: (Int, Int) -> Int
    g: Int -> Int
  Rules
    f(a, ?10) -> ?10
    f(b, ?11) -> ?11
    f(g(?12), ?13) -> f(b, ?13)
    g(?14) -> a
Confluent by Strongly Closedness with proof:
    * Critical Pair
      Inner Rule
        g(?14') -> a
      Outer Rule
        f(g(?12"), ?13") -> f(b, ?13")
      Pair
        f(a, ?13") ≈ f(b, ?13")
    which reaches the trivial constrained equation
      f(a, ?13") ≈ f(b, ?13") 
        -> ?13" ≈ f(b, ?13") 
        -> ?13" ≈ ?13" 
    and the trivial constrained equation
      f(a, ?13") ≈ f(b, ?13") 
        -> f(a, ?13") ≈ ?13" 
        -> ?13" ≈ ?13" 

Elapsed Time:  63.44 ms