YES (format LCTRS :logic QF_LIA) (fun sum2 1 :sort (Int Int)) (fun u 3 :sort (Int Int Int Int)) (rule (u x_0 i_1 z_2) z_2 :guard (not (<= i_1 x_0)) :vars ((x_0 Int) (i_1 Int) (z_2 Int))) (rule (u x_3 i_4 z_5) (u x_3 (+ i_4 1) (+ z_5 i_4)) :guard (<= i_4 x_3) :vars ((x_3 Int) (i_4 Int) (z_5 Int))) (rule (sum2 x_6) (u x_6 0 0) :vars ((x_6 Int))) Confluent by Orthogonality with proof: no critical pairs Elapsed Time: 14.83 ms