YES

(format LCTRS)
(fun a 0 :sort (Unit))
(fun b 0 :sort (Unit))
(fun c 0 :sort (Unit))
(fun d 0 :sort (Unit))
(fun f 4 :sort (Unit Unit Unit Unit Unit))

(rule (f a a b b) (f c c c c))
(rule a b)
(rule a c)
(rule b a)
(rule b c)

Confluent by Almost Parallel Closedness with proof:
* CriticalPair
  Left rule: a -> b
  Right rule: (f a a b b) -> (f c c c c)
  Critical 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)) []
	-||-> (≈ (f c c c c) (f c c c c)) []
* CriticalPair
  Left rule: a -> b
  Right rule: (f a a b b) -> (f c c c c)
  Critical 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)) []
	-||-> (≈ (f c c c c) (f c c c c)) []
* CriticalPair
  Left rule: a -> c
  Right rule: (f a a b b) -> (f c c c c)
  Critical 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)) []
	-||-> (≈ (f c c c c) (f c c c c)) []
* CriticalPair
  Left rule: a -> c
  Right rule: (f a a b b) -> (f c c c c)
  Critical 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)) []
	-||-> (≈ (f c c c c) (f c c c c)) []
* CriticalPair
  Left rule: b -> a
  Right rule: (f a a b b) -> (f c c c c)
  Critical 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)) []
	-||-> (≈ (f c c c c) (f c c c c)) []
* CriticalPair
  Left rule: b -> a
  Right rule: (f a a b b) -> (f c c c c)
  Critical 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)) []
	-||-> (≈ (f c c c c) (f c c c c)) []
* CriticalPair
  Left rule: b -> c
  Right rule: (f a a b b) -> (f c c c c)
  Critical 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)) []
	-||-> (≈ (f c c c c) (f c c c c)) []
* CriticalPair
  Left rule: b -> c
  Right rule: (f a a b b) -> (f c c c c)
  Critical 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)) []
	-||-> (≈ (f c c c c) (f c c c c)) []
* CriticalPair
  Left rule: a -> c
  Right rule: a -> b
  Critical pair: c ≈ b
 which reaches the trivial constrained equation
  (≈ c b) []
	-||-> (≈ c c) []
* CriticalPair
  Left rule: a -> b
  Right rule: a -> c
  Critical pair: b ≈ c
 which reaches the trivial constrained equation
  (≈ b c) []
	-||-> (≈ c c) []
* CriticalPair
  Left rule: b -> c
  Right rule: b -> a
  Critical pair: c ≈ a
 which reaches the trivial constrained equation
  (≈ c a) []
	-||-> (≈ c c) []
* CriticalPair
  Left rule: b -> a
  Right rule: b -> c
  Critical pair: a ≈ c
 which reaches the trivial constrained equation
  (≈ a c) []
	-||-> (≈ c c) []


Elapsed Time:  84.84 ms