MAYBE

(format LCTRS :logic QF_LIA)
(fun hikaku 2 :sort (Int Int Int))
(fun max 2 :sort (Int Int Result2))
(fun min 2 :sort (Int Int Result1))
(fun return 1 :sort (Int Int))
(fun return1 1 :sort (Int Result1))
(fun return2 1 :sort (Int Result2))
(fun sum2 2 :sort (Int Int Int))
(fun u1 4 :sort (Int Int Int Int Int))
(fun u2 5 :sort (Int Int Int Int Result1 Int))
(fun u3 5 :sort (Int Int Int Int Result2 Int))

(rule (u3 x_0 y_1 t_2 i_3 (return2 k_4)) (u3 x_0 y_1 (+ t_2 i_3) (+ i_3 1) (max x_0 y_1)) :guard (not (<= i_3 k_4)) :vars ((x_0 Int) (y_1 Int) (t_2 Int) (i_3 Int) (k_4 Int)))
(rule (u3 x_5 y_6 t_7 i_8 (return2 k_9)) (return t_7) :guard (<= i_8 k_9) :vars ((x_5 Int) (y_6 Int) (t_7 Int) (i_8 Int) (k_9 Int)))
(rule (u2 x_10 y_11 t_12 i_13 (return1 k_14)) (u3 x_10 y_11 t_12 k_14 (max x_10 y_11)) :vars ((x_10 Int) (y_11 Int) (t_12 Int) (i_13 Int) (k_14 Int)))
(rule (u1 x_15 y_16 t_17 i_18) (u2 x_15 y_16 0 i_18 (min x_15 y_16)) :guard (not (> x_15 y_16)) :vars ((x_15 Int) (y_16 Int) (t_17 Int) (i_18 Int)))
(rule (u1 x_19 y_20 t_21 i_22) (return 0) :guard (> x_19 y_20) :vars ((x_19 Int) (y_20 Int) (t_21 Int) (i_22 Int)))
(rule (sum2 x_23 y_24) (u1 x_23 y_24 0 rnd_25) :vars ((x_23 Int) (y_24 Int) (rnd_25 Int)))
(rule (min x_26 y_27) (return1 y_27) :guard (not (> y_27 x_26)) :vars ((x_26 Int) (y_27 Int)))
(rule (min x_28 y_29) (return1 x_28) :guard (> y_29 x_28) :vars ((x_28 Int) (y_29 Int)))
(rule (max x_30 y_31) (return2 y_31) :guard (not (> x_30 y_31)) :vars ((x_30 Int) (y_31 Int)))
(rule (max x_32 y_33) (return2 x_32) :guard (> x_32 y_33) :vars ((x_32 Int) (y_33 Int)))

Confluence could not be determined.

Elapsed Time:   6.22 ms