YES (format LCTRS :logic QF_LIA) (fun A 2 :sort (Int Int Int)) (rule (A m_0 n_1) (A (- m_0 1) (A m_0 (- n_1 1))) :guard (and (not (= m_0 0)) (not (= n_1 0))) :vars ((m_0 Int) (n_1 Int))) (rule (A m_2 0) (A (- m_2 1) 1) :guard (not (= m_2 0)) :vars ((m_2 Int))) (rule (A 0 n_3) (+ n_3 1) :vars ((n_3 Int))) Confluent by Almost Parallel Closedness with proof: no critical pairs Elapsed Time: 23.93 ms