YES

(format LCTRS :logic QF_LIA)
(fun a 0 :sort (Int))
(fun f 1 :sort (Int Int))
(fun g 1 :sort (Int Int))

(rule (f x_0) z_1 :guard (= z_1 3) :vars ((x_0 Int) (z_1 Int)))
(rule (g (f x_2)) a :vars ((x_2 Int)))
(rule (g 3) a)

Confluent by Strongly Closedness with proof:
* CriticalPair
  Left rule: (f x_0_L) -> z_1_L [(= z_1_L 3)]
  Right rule: (f x_0_R) -> z_1_R [(= z_1_R 3)]
  Critical pair: z_1_L ≈ z_1_R [(and (= z_1_L 3) (= z_1_R 3))]
 which reaches the trivial constrained equation
  (≈ z_1_L z_1_R) [(and (= z_1_L 3) (= z_1_R 3))]
 and the trivial constrained equation
  (≈ z_1_L z_1_R) [(and (= z_1_L 3) (= z_1_R 3))]
* CriticalPair
  Left rule: (f x_0_L) -> z_1_L [(= z_1_L 3)]
  Right rule: (g (f x_2_R)) -> a
  Critical pair: (g z_1_L) ≈ a [(= z_1_L 3)]
 which reaches the trivial constrained equation
  (≈ (g z_1_L) a) [(= z_1_L 3)]
	-> (≈ a a) [(= z_1_L 3)]
 and the trivial constrained equation
  (≈ (g z_1_L) a) [(= z_1_L 3)]
	-> (≈ a a) [(= z_1_L 3)]


Elapsed Time:  17.86 ms