MAYBE (format LCTRS :logic QF_LIA) (fun dbl 1 :sort (Int Int)) (rule (dbl 0) 0) (rule (dbl (+ x_0 1)) (+ (dbl x_0) 2) :vars ((x_0 Int))) (rule (dbl (+ x_1 y_2)) (+ (dbl x_1) (dbl y_2)) :vars ((x_1 Int) (y_2 Int))) Confluence could not be determined. Elapsed Time: 25.95 ms