YES (format LCTRS :logic QF_LIA) (fun double 1 :sort (Int Int)) (rule (double x_0) 0 :guard (<= x_0 0) :vars ((x_0 Int))) (rule (double x_1) (+ 2 (double (- x_1 1))) :guard (> x_1 0) :vars ((x_1 Int))) Confluent by Weak Orthogonality with proof: no critical pairs Elapsed Time: 35.26 ms