YES

(format LCTRS :logic QF_LIA)
(fun fact 1 :sort (Int Int))
(fun return 1 :sort (Int Int))
(fun u2 3 :sort (Int Int Int Int))

(rule (fact x_0) (u2 x_0 1 1) :vars ((x_0 Int)))
(rule (u2 x_1 i_2 z_3) (u2 x_1 (+ i_2 1) (* z_3 i_2)) :guard (<= i_2 x_1) :vars ((x_1 Int) (i_2 Int) (z_3 Int)))
(rule (u2 x_4 i_5 z_6) (return z_6) :guard (> i_5 x_4) :vars ((x_4 Int) (i_5 Int) (z_6 Int)))

Confluent by Parallel Closedness with proof:
no critical pairs

Elapsed Time:   8.80 ms