YES

(format LCTRS :logic QF_LIA)
(fun f1 2 :sort (Int Int Int))
(fun u_11 2 :sort (Int Int Int))
(fun u_14 1 :sort (Int Int))
(fun u_34 1 :sort (Int Int))
(fun u_7 1 :sort (Int Int))

(rule (u_14 w_5_0) w_5_0 :vars ((w_5_0 Int)))
(rule (u_11 m_1 w_4_2) (u_14 (f1 (- m_1 1) w_4_2)) :vars ((m_1 Int) (w_4_2 Int)))
(rule (u_7 w_3_3) w_3_3 :vars ((w_3_3 Int)))
(rule (f1 m_4 n_5) (u_11 m_4 (f1 m_4 (- n_5 1))) :guard (and (distinct m_4 0) (or (<= m_4 0) (distinct n_5 0))) :vars ((m_4 Int) (n_5 Int)))
(rule (f1 m_6 n_7) (u_7 (f1 (- m_6 1) 1)) :guard (and (and (distinct m_6 0) (> m_6 0)) (= n_7 0)) :vars ((m_6 Int) (n_7 Int)))
(rule (f1 m_8 n_9) (+ n_9 1) :guard (= m_8 0) :vars ((m_8 Int) (n_9 Int)))

Confluent by Orthogonality with proof:
no critical pairs

Elapsed Time:  19.22 ms