YES
LCTRS
  Theories
    Core, Ints
  Signature
    c: (Int, Int) -> Int
    f: (Int, Int) -> Int
    g: (Int, Int) -> Int
    h: Int -> Int
  Rules
    c(?18, ?19) -> g(4, 2) [not(?18 = ?19)]
    f(?20, ?21) -> c(4, ?20) [<=(?21, ?20)]
    f(?22, ?23) -> h(g(?23, *(2, 2))) [and(<=(?22, ?23), ?23 = 2)]
    g(?24, ?25) -> g(?25, ?24)
    h(?26) -> ?26
Confluent by Almost Development Closedness with proof:
    * Critical Pair
      Inner Rule
        f(?22', ?23') -> h(g(?23', *(2, 2))) [and(<=(?22', ?23'), ?23' = 2)]
      Outer Rule
        f(?20", ?21") -> c(4, ?20") [<=(?21", ?20")]
      Pair
        h(g(?21", *(2, 2))) ≈ c(4, ?20") [and(<=(?20", ?21"), ?21" = 2), <=(?21", ?20")]
    which reaches the trivial constrained equation
      h(g(?21", *(2, 2))) ≈ c(4, ?20") [and(<=(?20", ?21"), ?21" = 2), <=(?21", ?20")]
        -o-> g(?329', ?21") ≈ c(4, ?20") [and(<=(?20", ?21"), ?21" = 2), <=(?21", ?20"), and(<=(?20", ?21"), ?21" = 2), <=(?21", ?20"), ?329' = *(2, 2)]
        -o-> g(?329', ?21") ≈ g(4, 2) [and(<=(?20", ?21"), ?21" = 2), <=(?21", ?20"), and(<=(?20", ?21"), ?21" = 2), <=(?21", ?20"), ?329' = *(2, 2)]
    * Critical Pair
      Inner Rule
        f(?20', ?21') -> c(4, ?20') [<=(?21', ?20')]
      Outer Rule
        f(?22", ?23") -> h(g(?23", *(2, 2))) [and(<=(?22", ?23"), ?23" = 2)]
      Pair
        c(4, ?22") ≈ h(g(?23", *(2, 2))) [<=(?23", ?22"), and(<=(?22", ?23"), ?23" = 2)]
    which reaches the trivial constrained equation
      c(4, ?22") ≈ h(g(?23", *(2, 2))) [<=(?23", ?22"), and(<=(?22", ?23"), ?23" = 2)]
        -o-> g(4, 2) ≈ h(g(?23", *(2, 2))) [<=(?23", ?22"), and(<=(?22", ?23"), ?23" = 2)]
        -o-> g(4, 2) ≈ g(?792', ?23") [<=(?23", ?22"), and(<=(?22", ?23"), ?23" = 2), <=(?23", ?22"), and(<=(?22", ?23"), ?23" = 2), ?792' = *(2, 2)]

Elapsed Time: 437.67 ms