YES
LCTRS
  Theories
    Core, Ints
  Signature
    f: Int -> Int
    g: Int -> Int
    h: Int -> Int
  Rules
    f(?14) -> g(?14) [and(<=(2, ?14), <=(?14, 4))]
    f(?15) -> 2 [and(<=(1, ?15), <=(?15, 3))]
    g(?16) -> h(?16)
    h(?17) -> ?18 [or(and(?17 = 3, ?18 = 2), and(?17 = 2, ?18 = ?17))]
Confluent by NewmansLemma with proof:
  Termination:
    DPGraph with indexed dependency pairs
      {1: f#(?14) -> g#(?14) [and(<=(2, ?14), <=(?14, 4))], 2: g#(?16) -> h#(?16)}
    and edges
      1 -> {2}
      2 -> {}
    with 0 SCC(s)
      
  Local Confluence:
      * Critical Pair
        Inner Rule
          f(?15') -> 2 [and(<=(1, ?15'), <=(?15', 3))]
        Outer Rule
          f(?14") -> g(?14") [and(<=(2, ?14"), <=(?14", 4))]
        Pair
          2 ≈ g(?14") [and(<=(1, ?14"), <=(?14", 3)), and(<=(2, ?14"), <=(?14", 4))]
      which reaches the trivial constrained equation
        2 ≈ g(?14") [and(<=(1, ?14"), <=(?14", 3)), and(<=(2, ?14"), <=(?14", 4))]
          -> 2 ≈ h(?14") [and(<=(1, ?14"), <=(?14", 3)), and(<=(2, ?14"), <=(?14", 4))]
          -> 2 ≈ ?257' [and(<=(1, ?14"), <=(?14", 3)), and(<=(2, ?14"), <=(?14", 4)), or(and(?14" = 3, ?257' = 2), and(?14" = 2, ?257' = ?14"))]
      * Critical Pair
        Inner Rule
          f(?14') -> g(?14') [and(<=(2, ?14'), <=(?14', 4))]
        Outer Rule
          f(?15") -> 2 [and(<=(1, ?15"), <=(?15", 3))]
        Pair
          g(?15") ≈ 2 [and(<=(2, ?15"), <=(?15", 4)), and(<=(1, ?15"), <=(?15", 3))]
      which reaches the trivial constrained equation
        g(?15") ≈ 2 [and(<=(2, ?15"), <=(?15", 4)), and(<=(1, ?15"), <=(?15", 3))]
          -> h(?15") ≈ 2 [and(<=(2, ?15"), <=(?15", 4)), and(<=(1, ?15"), <=(?15", 3))]
          ->^* ?272' ≈ 2 [and(<=(2, ?15"), <=(?15", 4)), and(<=(1, ?15"), <=(?15", 3)), or(and(?15" = 3, ?272' = 2), and(?15" = 2, ?272' = ?15"))]
      * Critical Pair
        Inner Rule
          h(?17') -> ?18' [or(and(?17' = 3, ?18' = 2), and(?17' = 2, ?18' = ?17'))]
        Outer Rule
          h(?17") -> ?18" [or(and(?17" = 3, ?18" = 2), and(?17" = 2, ?18" = ?17"))]
        Pair
          ?18' ≈ ?18" [or(and(?17" = 3, ?18' = 2), and(?17" = 2, ?18' = ?17")), or(and(?17" = 3, ?18" = 2), and(?17" = 2, ?18" = ?17"))]
      which reaches the trivial constrained equation
        ?18' ≈ ?18" [or(and(?17" = 3, ?18' = 2), and(?17" = 2, ?18' = ?17")), or(and(?17" = 3, ?18" = 2), and(?17" = 2, ?18" = ?17"))]

Elapsed Time: 132.55 ms