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 Parallel Closedness with proof: no critical pairs Elapsed Time: 15.23 ms