YES (format LCTRS :logic QF_LIA) (fun f2 1 :sort (Int Int)) (fun u_15 2 :sort (Int Int Int)) (rule (u_15 n_0 w_4_1) (+ n_0 w_4_1) :guard (distinct n_0 10) :vars ((n_0 Int) (w_4_1 Int))) (rule (u_15 n_2 w_4_3) 10 :guard (= n_2 10) :vars ((n_2 Int) (w_4_3 Int))) (rule (f2 n_4) (u_15 n_4 (f2 (- n_4 1))) :guard (> n_4 1) :vars ((n_4 Int))) (rule (f2 n_5) n_5 :guard (<= n_5 1) :vars ((n_5 Int))) Confluent by Newmans Lemma with proof: terminating and no critical pairs Elapsed Time: 16.69 ms