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:  14.73 ms