MAYBE

(format LCTRS :logic QF_LIA)
(fun init 3 :sort (Int Int Int Int))
(fun m 3 :sort (Int Int Int Int))
(fun m0 3 :sort (Int Int Int Int))
(fun m1 3 :sort (Int Int Int Int))
(fun m2 3 :sort (Int Int Int Int))
(fun m3 3 :sort (Int Int Int Int))
(fun merge 3 :sort (Int Int Int Int))
(fun split 3 :sort (Int Int Int Int))
(fun tuple 4 :sort (Int Int Int Int Int))

(rule (init x_0 y_1 z_2) (m x_0 y_1 z_2) :vars ((x_0 Int) (y_1 Int) (z_2 Int)))
(rule (m1 x_3 y_4 z_5) (m y_4 y_4 z_5) :vars ((x_3 Int) (y_4 Int) (z_5 Int)))
(rule (m0 x_6 y_7 z_8) (split x_6 y_7 z_8) :vars ((x_6 Int) (y_7 Int) (z_8 Int)))
(rule (m2 x_9 y_10 z_11) (m z_11 y_10 z_11) :vars ((x_9 Int) (y_10 Int) (z_11 Int)))
(rule (m3 x_12 y_13 z_14) (merge y_13 z_14 z_14) :vars ((x_12 Int) (y_13 Int) (z_14 Int)))
(rule (merge x_15 y_16 z_17) (merge (- x_15 1) y_16 z_17) :guard (and (>= x_15 1) (>= y_16 1)) :vars ((x_15 Int) (y_16 Int) (z_17 Int)))
(rule (split x_18 y_19 z_20) (split (- x_18 2) y_19 z_20) :guard (>= x_18 2) :vars ((x_18 Int) (y_19 Int) (z_20 Int)))
(rule (merge x_21 y_22 z_23) (merge x_21 (- y_22 1) z_23) :guard (and (>= x_21 1) (>= y_22 1)) :vars ((x_21 Int) (y_22 Int) (z_23 Int)))
(rule (m x_24 y_25 z_26) (tuple (m0 x_24 u_27 v_28) (m1 x_24 u_27 v_28) (m2 x_24 u_27 v_28) (m3 x_24 u_27 v_28)) :guard (and (>= x_24 2) (and (>= u_27 0) (and (>= v_28 0) (and (>= (+ x_24 1) (* 2 u_27)) (and (>= (* 2 u_27) x_24) (and (>= x_24 (* 2 v_28)) (>= (+ (* 2 v_28) 1) x_24))))))) :vars ((x_24 Int) (y_25 Int) (z_26 Int) (u_27 Int) (v_28 Int)))

Confluence could not be determined.

Elapsed Time:  89.74 ms