YES

(format LCTRS :logic QF_LIA)
(fun geq 2 :sort (Int Int Bool))
(fun plus 2 :sort (Int Int Int))
(fun sum 1 :sort (Int Int))
(fun sum2 2 :sort (Bool Int Int))

(rule (sum x_0) (sum2 (geq 0 x_0) x_0) :vars ((x_0 Int)))
(rule (sum2 true x_1) 0 :vars ((x_1 Int)))
(rule (sum2 false x_2) (plus x_2 (sum (plus x_2 (- 1)))) :vars ((x_2 Int)))
(rule (plus n_3 m_4) k_5 :guard (= (+ n_3 m_4) k_5) :vars ((n_3 Int) (m_4 Int) (k_5 Int)))
(rule (geq n_6 m_7) true :guard (>= n_6 m_7) :vars ((n_6 Int) (m_7 Int)))
(rule (geq n_8 m_9) false :guard (< n_8 m_9) :vars ((n_8 Int) (m_9 Int)))

Confluent by Weak Orthogonality with proof:
all critical pairs are trivial: 
* CriticalPair
  Left rule: (plus n_3_L m_4_L) -> k_5_L [(= (+ n_3_L m_4_L) k_5_L)]
  Right rule: (plus n_3_R m_4_R) -> k_5_R [(= (+ n_3_R m_4_R) k_5_R)]
  Critical pair: k_5_L ≈ k_5_R [(and (= (+ n_3_R m_4_R) k_5_L) (= (+ n_3_R m_4_R) k_5_R))] but is trivial as k_5_L [(and (= (+ n_3_R m_4_R) k_5_L) (= (+ n_3_R m_4_R) k_5_R))] ~ k_5_R [(and (= (+ n_3_R m_4_R) k_5_L) (= (+ n_3_R m_4_R) k_5_R))]


Elapsed Time:  36.43 ms