YES
LCTRS
  Theories
    Core, Ints
  Signature
    a: Int
    c: Int -> Int
    f: Int -> Int
    g: Int -> Int
  Rules
    c(?12) -> f(?12) [and(<=(1, ?12), <=(?12, 10))]
    c(?13) -> g(?13) [and(<=(1, ?13), <=(?13, 10))]
    f(?14) -> a [or(and(<=(6, ?14), <=(?14, 10)), and(<=(1, ?14), <=(?14, 5)))]
    g(?15) -> a [or(and(<=(6, ?15), <=(?15, 10)), and(<=(1, ?15), <=(?15, 5)))]
Confluent by Almost Development Closedness with proof:
    * Critical Pair
      Inner Rule
        c(?13') -> g(?13') [and(<=(1, ?13'), <=(?13', 10))]
      Outer Rule
        c(?12") -> f(?12") [and(<=(1, ?12"), <=(?12", 10))]
      Pair
        g(?12") ≈ f(?12") [and(<=(1, ?12"), <=(?12", 10)), and(<=(1, ?12"), <=(?12", 10))]
    which reaches the trivial constrained equation
      g(?12") ≈ f(?12") [and(<=(1, ?12"), <=(?12", 10)), and(<=(1, ?12"), <=(?12", 10))]
        -o-> a ≈ f(?12") [and(<=(1, ?12"), <=(?12", 10)), and(<=(1, ?12"), <=(?12", 10))]
        -o-> a ≈ a [and(<=(1, ?12"), <=(?12", 10)), and(<=(1, ?12"), <=(?12", 10))]
    * Critical Pair
      Inner Rule
        c(?12') -> f(?12') [and(<=(1, ?12'), <=(?12', 10))]
      Outer Rule
        c(?13") -> g(?13") [and(<=(1, ?13"), <=(?13", 10))]
      Pair
        f(?13") ≈ g(?13") [and(<=(1, ?13"), <=(?13", 10)), and(<=(1, ?13"), <=(?13", 10))]
    which reaches the trivial constrained equation
      f(?13") ≈ g(?13") [and(<=(1, ?13"), <=(?13", 10)), and(<=(1, ?13"), <=(?13", 10))]
        -o-> a ≈ g(?13") [and(<=(1, ?13"), <=(?13", 10)), and(<=(1, ?13"), <=(?13", 10))]
        -o-> a ≈ a [and(<=(1, ?13"), <=(?13", 10)), and(<=(1, ?13"), <=(?13", 10))]

Elapsed Time: 142.44 ms