YES

(format LCTRS :logic QF_LIA)
(fun quad 1 :sort (Int Int))
(fun twice 1 :sort (Int Int))
(fun u 3 :sort (Int Int Int Int))

(rule (u x_0 i_1 z_2) z_2 :guard (>= i_1 x_0) :vars ((x_0 Int) (i_1 Int) (z_2 Int)))
(rule (u x_3 i_4 z_5) (u x_3 (+ i_4 1) (+ z_5 2)) :guard (< i_4 x_3) :vars ((x_3 Int) (i_4 Int) (z_5 Int)))
(rule (twice x_6) (u x_6 0 0) :vars ((x_6 Int)))
(rule (quad x_7) (+ (twice x_7) (twice x_7)) :vars ((x_7 Int)))

Confluent by Parallel Closedness with proof:
no critical pairs

Elapsed Time:  13.95 ms