YES (format LCTRS :logic QF_LIA) (fun f1 1 :sort (Int Int)) (fun u_13 3 :sort (Int Int Int Int)) (rule (u_13 n_0 nx_1 w_4_2) (+ n_0 (+ nx_1 w_4_2)) :vars ((n_0 Int) (nx_1 Int) (w_4_2 Int))) (rule (f1 n_3) (u_13 n_3 (- n_3 1) (f1 (- (- n_3 1) 1))) :guard (and (> n_3 1) (> (- n_3 1) 1)) :vars ((n_3 Int))) (rule (f1 n_4) (+ n_4 (- n_4 1)) :guard (and (> n_4 1) (<= (- n_4 1) 1)) :vars ((n_4 Int))) (rule (f1 n_5) n_5 :guard (<= n_5 1) :vars ((n_5 Int))) Confluent by Parallel Closedness with proof: no critical pairs Elapsed Time: 16.04 ms