YES

(format LCTRS :logic QF_LIA)
(fun U2 4 :sort (Int Int Int Int Int))
(fun U7 4 :sort (Int Int Int Int Int))
(fun ackermann 2 :sort (Int Int Int))

(rule (ackermann x_0 y_1) (U2 x_0 y_1 x_0 y_1) :vars ((x_0 Int) (y_1 Int)))
(rule (U7 x_2 y_3 m_4 n_5) (U7 x_2 y_3 (- m_4 1) 1) :guard (and (<= n_5 0) (> m_4 0)) :vars ((x_2 Int) (y_3 Int) (m_4 Int) (n_5 Int)))
(rule (U7 x_6 y_7 m_8 n_9) (+ n_9 1) :guard (and (<= n_9 0) (not (> m_8 0))) :vars ((x_6 Int) (y_7 Int) (m_8 Int) (n_9 Int)))
(rule (U7 x_10 y_11 m_12 n_13) (U7 x_10 y_11 (- m_12 1) (U2 m_12 (- n_13 1) m_12 (- n_13 1))) :guard (and (not (<= n_13 0)) (> m_12 0)) :vars ((x_10 Int) (y_11 Int) (m_12 Int) (n_13 Int)))
(rule (U7 x_14 y_15 m_16 n_17) (+ n_17 1) :guard (and (not (<= n_17 0)) (not (> m_16 0))) :vars ((x_14 Int) (y_15 Int) (m_16 Int) (n_17 Int)))
(rule (U2 x_18 y_19 m_20 n_21) 0 :guard (or (< y_19 0) (< x_18 0)) :vars ((x_18 Int) (y_19 Int) (m_20 Int) (n_21 Int)))
(rule (U2 x_22 y_23 m_24 n_25) (U7 x_22 y_23 m_24 n_25) :guard (and (not (or (< y_23 0) (< x_22 0))) (> m_24 0)) :vars ((x_22 Int) (y_23 Int) (m_24 Int) (n_25 Int)))
(rule (U2 x_26 y_27 m_28 n_29) (+ n_29 1) :guard (and (not (or (< y_27 0) (< x_26 0))) (not (> m_28 0))) :vars ((x_26 Int) (y_27 Int) (m_28 Int) (n_29 Int)))

Confluent by Newmans Lemma with proof:
terminating and no critical pairs

Elapsed Time:  25.82 ms