YES

(format LCTRS :logic QF_NIA)
(fun fact1 1 :sort (Int Int))
(fun u 3 :sort (Int Int Int Int))

(rule (u n_0 i_1 z_2) (u n_0 (+ i_1 1) (* z_2 i_1)) :guard (<= i_1 n_0) :vars ((n_0 Int) (i_1 Int) (z_2 Int)))
(rule (u n_3 i_4 z_5) z_5 :guard (not (<= i_4 n_3)) :vars ((n_3 Int) (i_4 Int) (z_5 Int)))
(rule (fact1 n_6) (u n_6 1 1) :vars ((n_6 Int)))

Confluent by Weak Orthogonality with proof:
no critical pairs

Elapsed Time:  13.93 ms