MAYBE

(format LCTRS :logic QF_NIA)
(fun f 1 :sort (Int Unit))
(fun product 2 :sort (Unit Unit Unit))
(fun start 0 :sort (Unit))

(rule (f x_0) (product (f y_1) (f z_2)) :guard (and (and (and (and (> x_0 y_1) (> y_1 0)) (> x_0 z_2)) (> z_2 0)) (= x_0 (* y_1 z_2))) :vars ((x_0 Int) (y_1 Int) (z_2 Int)))
(rule start (f input_3) :vars ((input_3 Int)))

Confluence could not be determined.

Elapsed Time: 258.25 ms