(meta-info (comment "Ctrl example from examples-transformed/student/sumfrom01.ctrs"))
(format LCTRS :logic QF_LIA)
(fun u3 5 :sort (Int Int Int Int Result2 Int))
(fun return2 1 :sort (Int Result2))
(fun max 2 :sort (Int Int Result2))
(fun return 1 :sort (Int Int))
(fun u2 5 :sort (Int Int Int Int Result1 Int))
(fun return1 1 :sort (Int Result1))
(fun u1 4 :sort (Int Int Int Int Int))
(fun min 2 :sort (Int Int Result1))
(fun sum2 2 :sort (Int Int Int))
(fun hikaku 2 :sort (Int Int Int))

(rule (u3 x y t i (return2 k)) (u3 x y (+ t i) (+ i 1) (max x y)) :guard (not (<= i k)) :vars ((x Int) (y Int) (t Int) (i Int) (k Int)))
(rule (u3 x y t i (return2 k)) (return t) :guard (<= i k) :vars ((x Int) (y Int) (t Int) (i Int) (k Int)))
(rule (u2 x y t i (return1 k)) (u3 x y t k (max x y)) :vars ((x Int) (y Int) (t Int) (i Int) (k Int)))
(rule (u1 x y t i) (u2 x y 0 i (min x y)) :guard (not (> x y)) :vars ((x Int) (y Int) (t Int) (i Int)))
(rule (u1 x y t i) (return 0) :guard (> x y) :vars ((x Int) (y Int) (t Int) (i Int)))
(rule (sum2 x y) (u1 x y 0 rnd) :vars ((x Int) (y Int) (rnd Int)))
(rule (min x y) (return1 y) :guard (not (> y x)) :vars ((x Int) (y Int)))
(rule (min x y) (return1 x) :guard (> y x) :vars ((x Int) (y Int)))
(rule (max x y) (return2 y) :guard (not (> x y)) :vars ((x Int) (y Int)))
(rule (max x y) (return2 x) :guard (> x y) :vars ((x Int) (y Int)))