YES

(format LCTRS :logic QF_LIA)
(fun return 1 :sort (Int Unit))
(fun sum2 2 :sort (Int Int Unit))
(fun u 3 :sort (Int Int Int Unit))
(fun v 3 :sort (Int Int Int Unit))

(rule (u a_0 b_1 c_2) (return c_2) :guard (not (< a_0 b_1)) :vars ((a_0 Int) (b_1 Int) (c_2 Int)))
(rule (v a_3 b_4 c_5) (return c_5) :guard (not (>= b_4 a_3)) :vars ((a_3 Int) (b_4 Int) (c_5 Int)))
(rule (v a_6 b_7 c_8) (v a_6 (- b_7 1) (+ c_8 b_7)) :guard (>= b_7 a_6) :vars ((a_6 Int) (b_7 Int) (c_8 Int)))
(rule (u a_9 b_10 c_11) (v a_9 b_10 c_11) :guard (< a_9 b_10) :vars ((a_9 Int) (b_10 Int) (c_11 Int)))
(rule (sum2 a_12 b_13) (u a_12 b_13 0) :vars ((a_12 Int) (b_13 Int)))

Confluent by Weak Orthogonality with proof:
no critical pairs

Elapsed Time:  10.31 ms