YES (format LCTRS :logic QF_LIA) (fun f2 2 :sort (Int Int Int)) (fun u_25 1 :sort (Int Int)) (fun u_31 2 :sort (Int Int Int)) (fun u_34 1 :sort (Int Int)) (rule (u_34 w_10_0) w_10_0 :vars ((w_10_0 Int))) (rule (u_31 m_1 w_9_2) (u_34 (f2 (- m_1 1) w_9_2)) :vars ((m_1 Int) (w_9_2 Int))) (rule (u_25 w_8_3) w_8_3 :vars ((w_8_3 Int))) (rule (f2 m_4 n_5) (u_31 m_4 (f2 m_4 (- n_5 1))) :guard (and (or (<= m_4 0) (distinct n_5 0)) (distinct m_4 1)) :vars ((m_4 Int) (n_5 Int))) (rule (f2 m_6 n_7) (+ n_7 1) :guard (and (or (<= m_6 0) (distinct n_7 0)) (= m_6 1)) :vars ((m_6 Int) (n_7 Int))) (rule (f2 m_8 n_9) (u_25 (f2 (- m_8 1) 1)) :guard (and (> m_8 0) (= n_9 0)) :vars ((m_8 Int) (n_9 Int))) Confluent by Parallel Closedness with proof: no critical pairs Elapsed Time: 12.84 ms