YES

(format LCTRS :logic QF_LIA)
(fun eval1 2 :sort (Int Int Int))
(fun eval2 2 :sort (Int Int Int))
(fun eval3 2 :sort (Int Int Int))

(rule (eval1 x_0 y_1) (eval2 x_0 y_1) :guard (and (and (> x_0 0) (> y_1 0)) (> x_0 y_1)) :vars ((x_0 Int) (y_1 Int)))
(rule (eval1 x_2 y_3) (eval3 x_2 y_3) :guard (and (and (> x_2 0) (> y_3 0)) (not (> x_2 y_3))) :vars ((x_2 Int) (y_3 Int)))
(rule (eval2 x_4 y_5) (eval2 (+ x_4 -1) (+ y_5 1)) :guard (> x_4 0) :vars ((x_4 Int) (y_5 Int)))
(rule (eval2 x_6 y_7) (eval1 x_6 y_7) :guard (not (> x_6 0)) :vars ((x_6 Int) (y_7 Int)))
(rule (eval3 x_8 y_9) (eval3 (+ x_8 1) (+ y_9 -1)) :guard (> y_9 0) :vars ((x_8 Int) (y_9 Int)))
(rule (eval3 x_10 y_11) (eval1 x_10 y_11) :guard (not (> y_11 0)) :vars ((x_10 Int) (y_11 Int)))

Confluent by Weak Orthogonality with proof:
no critical pairs

Elapsed Time:  16.73 ms