YES (format LCTRS :logic QF_LIA) (fun plus 2 :sort (Int Int Int)) (fun sum 1 :sort (Int Int)) (fun sumsum 1 :sort (Int Int)) (fun sumsum1 1 :sort (Int Int)) (fun u0 4 :sort (Int Int Int Int Int)) (fun u1 4 :sort (Int Int Int Int Int)) (rule (plus x_0 y_1) (+ x_0 y_1) :vars ((x_0 Int) (y_1 Int))) (rule (u0 x_2 i_3 j_4 z_5) (u1 x_2 i_3 0 z_5) :guard (>= x_2 i_3) :vars ((x_2 Int) (i_3 Int) (j_4 Int) (z_5 Int))) (rule (u0 x_6 i_7 j_8 z_9) z_9 :guard (not (>= x_6 i_7)) :vars ((x_6 Int) (i_7 Int) (j_8 Int) (z_9 Int))) (rule (u1 x_10 i_11 j_12 z_13) (u1 x_10 i_11 (+ j_12 1) (+ z_13 j_12)) :guard (>= i_11 j_12) :vars ((x_10 Int) (i_11 Int) (j_12 Int) (z_13 Int))) (rule (u1 x_14 i_15 j_16 z_17) (u0 x_14 (+ i_15 1) j_16 z_17) :guard (not (>= i_15 j_16)) :vars ((x_14 Int) (i_15 Int) (j_16 Int) (z_17 Int))) (rule (sumsum1 x_18) (u0 x_18 0 0 0) :vars ((x_18 Int))) (rule (sumsum x_19) 0 :guard (<= x_19 0) :vars ((x_19 Int))) (rule (sumsum x_20) (plus (sumsum (- x_20 1)) (sum x_20)) :guard (>= (- x_20 1) 0) :vars ((x_20 Int))) (rule (sum x_21) (plus (sum (- x_21 1)) x_21) :guard (>= (- x_21 1) 0) :vars ((x_21 Int))) (rule (sum x_22) 0 :guard (<= x_22 0) :vars ((x_22 Int))) Confluent by Newmans Lemma with proof: terminating and no critical pairs Elapsed Time: 14.87 ms