YES
LCTRS
  Theories
    Core, Ints
  Signature
    a: Int
    f: Int -> Int
    g: (Int, Int) -> Int
  Rules
    a -> g(+(1, 1), +(3, 1))
    f(a) -> g(4, 4)
    g(?9, ?10) -> f(g(?11, ?10)) [?11 = -(?9, 2)]
Confluent by Toyama81 with proof:
  * Critical Pair
    Inner Rule
      a -> g(+(1, 1), +(3, 1))
    Outer Rule
      f(a) -> g(4, 4)
    Pair
      f(g(+(1, 1), +(3, 1))) ≈ g(4, 4)
  which reaches the trivial constrained equation
    f(g(+(1, 1), +(3, 1))) ≈ g(4, 4) 
      -||-> f(g(?647', ?657')) ≈ g(4, 4) [?647' = +(1, 1), ?657' = +(3, 1)]
      -||-> f(g(?647', ?657')) ≈ f(g(?747', 4)) [?647' = +(1, 1), ?657' = +(3, 1), ?747' = -(4, 2)]
  * Critical Pair
    Inner Rule
      g(?9', ?10') -> f(g(?11', ?10')) [?11' = -(?9', 2)]
    Outer Rule
      g(?9", ?10") -> f(g(?11", ?10")) [?11" = -(?9", 2)]
    Pair
      f(g(?11', ?10")) ≈ f(g(?11", ?10")) [?11' = -(?9", 2), ?11" = -(?9", 2)]
  which reaches the trivial constrained equation
    f(g(?11', ?10")) ≈ f(g(?11", ?10")) [?11' = -(?9", 2), ?11" = -(?9", 2)]
      -||-> f(g(?11', ?10")) ≈ f(g(?11", ?10")) [?11' = -(?9", 2), ?11" = -(?9", 2)]
      -||-> f(g(?11', ?10")) ≈ f(g(?11", ?10")) [?11' = -(?9", 2), ?11" = -(?9", 2)]
  * Parallel Critical Pair
    Top
      f(a) 
    Inner Rule(s)
      Pos 0: a -> g(+(1, 1), +(3, 1))
    Outer Rule
      f(a) -> g(4, 4)
    Pair
      f(g(+(1, 1), +(3, 1))) ≈ g(4, 4)
  satisfies the variable condition
    {} ⊆ {}
  and reaches the trivial constrained equation
    f(g(+(1, 1), +(3, 1))) ≈ g(4, 4) 
      ->^* f(g(?1075', ?1085')) ≈ g(4, 4) [?1075' = +(1, 1), ?1085' = +(3, 1)]
      -||->_{1} f(g(?1075', ?1085')) ≈ f(g(?1175', 4)) [?1075' = +(1, 1), ?1085' = +(3, 1), ?1175' = -(4, 2)]
  * Parallel Critical Pair
    Top
      g(?9", ?10") [=(?582', -(?9", 2)), =(?11", -(?9", 2))]
    Inner Rule(s)
      Pos ε: g(?580', ?581') -> f(g(?582', ?581')) [=(?582', -(?580', 2))]
    Outer Rule
      g(?9", ?10") -> f(g(?11", ?10")) [=(?11", -(?9", 2))]
    Pair
      f(g(?582', ?10")) ≈ f(g(?11", ?10")) [=(?582', -(?9", 2)), =(?11", -(?9", 2))]
  satisfies the variable condition
    {} ⊆ {?10"}
  and reaches the trivial constrained equation
    f(g(?582', ?10")) ≈ f(g(?11", ?10")) [?582' = -(?9", 2), ?11" = -(?9", 2)]
      ->^* f(g(?582', ?10")) ≈ f(g(?11", ?10")) [?582' = -(?9", 2), ?11" = -(?9", 2)]
      -||->_{} f(g(?582', ?10")) ≈ f(g(?11", ?10")) [?582' = -(?9", 2), ?11" = -(?9", 2)]

Elapsed Time: 288.40 ms