MAYBE

(format LCTRS :logic QF_LIA)
(fun fun1 2 :sort (Int Int Unit))
(fun fun2 3 :sort (Int Int Int Unit))
(fun fun3 2 :sort (Int Int Unit))
(fun fun4 2 :sort (Int Int Unit))
(fun fun5 2 :sort (Int Int Unit))
(fun fun6 2 :sort (Int Int Unit))
(fun fun7 2 :sort (Int Int Unit))
(fun fun8 2 :sort (Int Int Unit))

(rule (fun7 x_0 y_1) (fun1 x_0 y_1) :vars ((x_0 Int) (y_1 Int)))
(rule (fun6 x_2 y_3) (fun7 x_2 (- y_3 1)) :vars ((x_2 Int) (y_3 Int)))
(rule (fun5 x_4 y_5) (fun7 x_4 y_5) :vars ((x_4 Int) (y_5 Int)))
(rule (fun4 x_6 y_7) (fun5 x_6 input_8) :vars ((x_6 Int) (y_7 Int) (input_8 Int)))
(rule (fun3 x_9 y_10) (fun4 (- x_9 1) y_10) :vars ((x_9 Int) (y_10 Int)))
(rule (fun2 x_11 y_12 i_13) (fun6 x_11 y_12) :guard (not (= i_13 1)) :vars ((x_11 Int) (y_12 Int) (i_13 Int)))
(rule (fun2 x_14 y_15 i_16) (fun3 x_14 y_15) :guard (= i_16 1) :vars ((x_14 Int) (y_15 Int) (i_16 Int)))
(rule (fun1 x_17 y_18) (fun8 x_17 y_18) :guard (and (<= x_17 0) (<= y_18 0)) :vars ((x_17 Int) (y_18 Int)))
(rule (fun1 x_19 y_20) (fun2 x_19 y_20 input_21) :guard (and (> x_19 0) (> y_20 0)) :vars ((x_19 Int) (y_20 Int) (input_21 Int)))

Confluence could not be determined.

Elapsed Time:  15.94 ms