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 (quad x_0) (+ (twice x_0) (twice x_0)) :vars ((x_0 Int)))
(rule (u x_1 i_2 z_3) z_3 :guard (not (< i_2 x_1)) :vars ((x_1 Int) (i_2 Int) (z_3 Int)))
(rule (u x_4 i_5 z_6) (u x_4 (+ i_5 1) (+ z_6 2)) :guard (< i_5 x_4) :vars ((x_4 Int) (i_5 Int) (z_6 Int)))
(rule (twice x_7) (u x_7 0 0) :vars ((x_7 Int)))

Confluent by Parallel Closedness with proof:
no critical pairs

Elapsed Time:  10.84 ms