YES
LCTRS
  Theories
    Core, Ints
  Sorts
    Unit
  Signature
    a: Unit
    b: Unit
    c: Unit
    d: Unit
    f: (Int, Unit) -> Unit
  Rules
    a -> b
    d -> d
    f(?4, a) -> c [<=(?4, 3)]
    f(?5, b) -> c [<=(?5, 10)]
Confluent by Development Closedness with proof:
    * Critical Pair
      Inner Rule
        a -> b
      Outer Rule
        f(?4", a) -> c [<=(?4", 3)]
      Pair
        f(?4", b) ≈ c [<=(?4", 3)]
    which reaches the trivial constrained equation
      f(?4", b) ≈ c [<=(?4", 3)]
        -o-> c ≈ c [<=(?4", 3)]

Elapsed Time:  71.81 ms