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 approximation on the DP problem
      dependency pairs:
        {f#(?14) -> g#(?14) [and(<=(2, ?14), <=(?14, 4))], g#(?16) -> h#(?16)}
      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)))]}
    resulting in the DP graph
      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
          Pos ε: f(?14') -> g(?14') [and(<=(2, ?14'), <=(?14', 4))]
        Outer Rule
          f(?15") -> 2 [and(<=(1, ?15"), <=(?15", 3))]
        Pair
          g(?15") ≈ 2 [and(<=(1, ?15"), <=(?15", 3)), and(<=(2, ?15"), <=(?15", 4))]
      which reaches the trivial constrained equation
        g(?15") ≈ 2 [and(<=(1, ?15"), <=(?15", 3)), and(<=(2, ?15"), <=(?15", 4))]
          -> h(?15") ≈ 2 [and(<=(1, ?15"), <=(?15", 3)), and(<=(2, ?15"), <=(?15", 4))]
          ->^* ?32' ≈ 2 [and(<=(1, ?15"), <=(?15", 3)), and(<=(2, ?15"), <=(?15", 4)), ?32' = ?32', or(and(?15" = 3, ?32' = 2), and(?15" = 2, ?32' = ?15"))]
      * Critical Pair
        Inner Rule
          Pos ε: f(?15') -> 2 [and(<=(1, ?15'), <=(?15', 3))]
        Outer Rule
          f(?14") -> g(?14") [and(<=(2, ?14"), <=(?14", 4))]
        Pair
          2 ≈ g(?14") [and(<=(2, ?14"), <=(?14", 4)), and(<=(1, ?14"), <=(?14", 3))]
      which reaches the trivial constrained equation
        2 ≈ g(?14") [and(<=(2, ?14"), <=(?14", 4)), and(<=(1, ?14"), <=(?14", 3))]
          -> 2 ≈ h(?14") [and(<=(2, ?14"), <=(?14", 4)), and(<=(1, ?14"), <=(?14", 3))]
          -> 2 ≈ ?67' [and(<=(2, ?14"), <=(?14", 4)), and(<=(1, ?14"), <=(?14", 3)), ?67' = ?67', or(and(?14" = 3, ?67' = 2), and(?14" = 2, ?67' = ?14"))]
      * Critical Pair
        Inner Rule
          Pos ε: 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:  76.34 ms