MAYBE

(format LCTRS :logic QF_LIA)
(fun fact 1 :sort (Int Int))
(fun return 1 :sort (Int Int))
(fun u1 3 :sort (Int Int Int Int))
(fun u2 3 :sort (Int Int Int Int))
(fun u3 3 :sort (Int Int Int Int))

(rule (fact x_0) (u1 x_0 i_1 z_2) :vars ((x_0 Int) (i_1 Int) (z_2 Int)))
(rule (u1 x_3 i_4 z_5) (u2 x_3 1 1) :vars ((x_3 Int) (i_4 Int) (z_5 Int)))
(rule (u2 x_6 i_7 z_8) (u2 x_6 (+ i_7 1) (* z_8 i_7)) :guard (<= i_7 x_6) :vars ((x_6 Int) (i_7 Int) (z_8 Int)))
(rule (u2 x_9 i_10 z_11) (u3 x_9 i_10 z_11) :guard (not (<= i_10 x_9)) :vars ((x_9 Int) (i_10 Int) (z_11 Int)))
(rule (u3 x_12 i_13 z_14) (return z_14) :vars ((x_12 Int) (i_13 Int) (z_14 Int)))

Confluence could not be determined.

Elapsed Time:   2.49 ms