YES

(format LCTRS :logic QF_LIA)
(fun sum 1 :sort (Int Int))
(fun sum2 1 :sort (Int Int))
(fun u1 3 :sort (Int Int Int Int))
(fun u2 4 :sort (Int Int Int Int Int))

(rule (u1 x_0 i_1 z_2) z_2 :guard (not (<= i_1 x_0)) :vars ((x_0 Int) (i_1 Int) (z_2 Int)))
(rule (u2 x_3 i_4 j_5 z_6) (u1 x_3 (+ i_4 1) z_6) :guard (not (< j_5 i_4)) :vars ((x_3 Int) (i_4 Int) (j_5 Int) (z_6 Int)))
(rule (u2 x_7 i_8 j_9 z_10) (u2 x_7 i_8 (+ j_9 1) (+ z_10 1)) :guard (< j_9 i_8) :vars ((x_7 Int) (i_8 Int) (j_9 Int) (z_10 Int)))
(rule (u1 x_11 i_12 z_13) (u2 x_11 i_12 0 z_13) :guard (<= i_12 x_11) :vars ((x_11 Int) (i_12 Int) (z_13 Int)))
(rule (sum2 x_14) (u1 x_14 0 0) :vars ((x_14 Int)))
(rule (sum x_15) (+ x_15 (sum (- x_15 1))) :guard (< 0 x_15) :vars ((x_15 Int)))
(rule (sum x_16) 0 :guard (<= x_16 0) :vars ((x_16 Int)))

Confluent by Newmans Lemma with proof:
terminating and no critical pairs

Elapsed Time:  12.59 ms