YES

(format LCTRS :logic QF_LIA)
(fun a 0 :sort (Unit))
(fun b 0 :sort (Unit))
(fun c 0 :sort (Unit))
(fun d 0 :sort (Unit))
(fun f 2 :sort (Int Unit Unit))

(rule d d)
(rule (f x_0 b) c :guard (<= x_0 10) :vars ((x_0 Int)))
(rule a b)
(rule (f x_1 a) c :guard (<= x_1 3) :vars ((x_1 Int)))

Confluent by Parallel Closedness with proof:
* CriticalPair
  Left rule: a -> b
  Right rule: (f x_1_R a) -> c [(and (<= x_1_R 3) (<= x_1_R 3))]
  Critical pair: (f x_1_R b) ≈ c [(and (<= x_1_R 3) (<= x_1_R 3))]
 which reaches the trivial constrained equation
  (≈ (f x_1_R b) c) [(and (<= x_1_R 3) (<= x_1_R 3))]
	-||-> (≈ c c) [(and (<= x_1_R 3) (<= x_1_R 3))]


Elapsed Time:  15.40 ms