(format LCTRS :logic QF_LIA)

(fun max 2 :sort (Int Int Int))

(rule (max x y) x :guard (>= x y))
(rule (max x y) y :guard (>= y x))
(rule (max x y) (max y x))