YES
LCTRS
  Theories
    Core
  Sorts
    Unit
  Signature
    a: Unit
    b: Unit
    c: Unit
    d: Unit
    f: (Unit, Unit, Unit, Unit) -> Unit
  Rules
    a -> b
    a -> c
    b -> a
    b -> c
    f(a, a, b, b) -> f(c, c, c, c)
Confluent by Almost Development Closedness with proof:
    * Critical Pair
      Inner Rule
        a -> c
      Outer Rule
        a -> b
      Pair
        c ≈ b
    which reaches the trivial constrained equation
      c ≈ b 
        -o-> c ≈ b 
        -o-> c ≈ c 
    * Critical Pair
      Inner Rule
        a -> b
      Outer Rule
        a -> c
      Pair
        b ≈ c
    which reaches the trivial constrained equation
      b ≈ c 
        -o-> c ≈ c 
        -o-> c ≈ c 
    * Critical Pair
      Inner Rule
        b -> c
      Outer Rule
        b -> a
      Pair
        c ≈ a
    which reaches the trivial constrained equation
      c ≈ a 
        -o-> c ≈ a 
        -o-> c ≈ c 
    * Critical Pair
      Inner Rule
        b -> a
      Outer Rule
        b -> c
      Pair
        a ≈ c
    which reaches the trivial constrained equation
      a ≈ c 
        -o-> c ≈ c 
        -o-> c ≈ c 
    * Critical Pair
      Inner Rule
        a -> b
      Outer Rule
        f(a, a, b, b) -> f(c, c, c, c)
      Pair
        f(b, a, b, b) ≈ f(c, c, c, c)
    which reaches the trivial constrained equation
      f(b, a, b, b) ≈ f(c, c, c, c) 
        -o-> f(c, c, c, c) ≈ f(c, c, c, c) 
    * Critical Pair
      Inner Rule
        a -> b
      Outer Rule
        f(a, a, b, b) -> f(c, c, c, c)
      Pair
        f(a, b, b, b) ≈ f(c, c, c, c)
    which reaches the trivial constrained equation
      f(a, b, b, b) ≈ f(c, c, c, c) 
        -o-> f(c, c, c, c) ≈ f(c, c, c, c) 
    * Critical Pair
      Inner Rule
        a -> c
      Outer Rule
        f(a, a, b, b) -> f(c, c, c, c)
      Pair
        f(c, a, b, b) ≈ f(c, c, c, c)
    which reaches the trivial constrained equation
      f(c, a, b, b) ≈ f(c, c, c, c) 
        -o-> f(c, c, c, c) ≈ f(c, c, c, c) 
    * Critical Pair
      Inner Rule
        a -> c
      Outer Rule
        f(a, a, b, b) -> f(c, c, c, c)
      Pair
        f(a, c, b, b) ≈ f(c, c, c, c)
    which reaches the trivial constrained equation
      f(a, c, b, b) ≈ f(c, c, c, c) 
        -o-> f(c, c, c, c) ≈ f(c, c, c, c) 
    * Critical Pair
      Inner Rule
        b -> a
      Outer Rule
        f(a, a, b, b) -> f(c, c, c, c)
      Pair
        f(a, a, a, b) ≈ f(c, c, c, c)
    which reaches the trivial constrained equation
      f(a, a, a, b) ≈ f(c, c, c, c) 
        -o-> f(c, c, c, c) ≈ f(c, c, c, c) 
    * Critical Pair
      Inner Rule
        b -> a
      Outer Rule
        f(a, a, b, b) -> f(c, c, c, c)
      Pair
        f(a, a, b, a) ≈ f(c, c, c, c)
    which reaches the trivial constrained equation
      f(a, a, b, a) ≈ f(c, c, c, c) 
        -o-> f(c, c, c, c) ≈ f(c, c, c, c) 
    * Critical Pair
      Inner Rule
        b -> c
      Outer Rule
        f(a, a, b, b) -> f(c, c, c, c)
      Pair
        f(a, a, c, b) ≈ f(c, c, c, c)
    which reaches the trivial constrained equation
      f(a, a, c, b) ≈ f(c, c, c, c) 
        -o-> f(c, c, c, c) ≈ f(c, c, c, c) 
    * Critical Pair
      Inner Rule
        b -> c
      Outer Rule
        f(a, a, b, b) -> f(c, c, c, c)
      Pair
        f(a, a, b, c) ≈ f(c, c, c, c)
    which reaches the trivial constrained equation
      f(a, a, b, c) ≈ f(c, c, c, c) 
        -o-> f(c, c, c, c) ≈ f(c, c, c, c) 

Elapsed Time: 104.64 ms