YES (format LCTRS :logic QF_LIA) (fun f1 2 :sort (Int Int Int)) (fun u_11 2 :sort (Int Int Int)) (fun u_14 1 :sort (Int Int)) (fun u_7 1 :sort (Int Int)) (rule (u_14 w_5_0) w_5_0 :vars ((w_5_0 Int))) (rule (u_11 m_1 w_4_2) (u_14 (f1 (- m_1 1) w_4_2)) :vars ((m_1 Int) (w_4_2 Int))) (rule (u_7 w_3_3) w_3_3 :vars ((w_3_3 Int))) (rule (f1 m_4 n_5) (u_11 m_4 (f1 m_4 (- n_5 1))) :guard (and (distinct m_4 0) (or (<= m_4 0) (distinct n_5 0))) :vars ((m_4 Int) (n_5 Int))) (rule (f1 m_6 n_7) (u_7 (f1 (- m_6 1) 1)) :guard (and (and (distinct m_6 0) (> m_6 0)) (= n_7 0)) :vars ((m_6 Int) (n_7 Int))) (rule (f1 m_8 n_9) (+ n_9 1) :guard (= m_8 0) :vars ((m_8 Int) (n_9 Int))) Confluent by Parallel Closedness with proof: no critical pairs Elapsed Time: 13.78 ms