YES (format LCTRS :logic QF_LIA) (fun fact 1 :sort (Int Int)) (rule (fact x_0) 1 :guard (<= x_0 0) :vars ((x_0 Int))) (rule (fact x_1) (* (fact (- x_1 1)) x_1) :guard (>= (- x_1 1) 0) :vars ((x_1 Int))) Confluent by Parallel Closedness with proof: no critical pairs Elapsed Time: 9.95 ms