YES (format LCTRS :logic QF_LIA) (fun sum 1 :sort (Int Int)) (fun test 1 :sort (Int Unit)) (rule (test x_0) (test y_1) :guard (and (> x_0 0) (= x_0 (+ y_1 1))) :vars ((x_0 Int) (y_1 Int))) (rule (sum x_2) (+ x_2 (sum (- x_2 1))) :guard (< 0 x_2) :vars ((x_2 Int))) (rule (sum 0) 0) (rule (sum x_3) 0 :guard (< x_3 0) :vars ((x_3 Int))) Confluent by Almost Parallel Closedness with proof: * CriticalPair Left rule: (test x_0_L) -> (test y_1_L) [(and (> x_0_L 0) (= x_0_L (+ y_1_L 1)))] Right rule: (test x_0_R) -> (test y_1_R) [(and (> x_0_R 0) (= x_0_R (+ y_1_R 1)))] Critical pair: (test y_1_L) ≈ (test y_1_R) [(and (and (> x_0_R 0) (= x_0_R (+ y_1_L 1))) (and (> x_0_R 0) (= x_0_R (+ y_1_R 1))))] which reaches the trivial constrained equation (≈ (test y_1_L) (test y_1_R)) [(and (and (> x_0_R 0) (= x_0_R (+ y_1_L 1))) (and (> x_0_R 0) (= x_0_R (+ y_1_R 1))))] Elapsed Time: 24.79 ms