; @author Jonas Schöpf
; @author Aart Middeldorp
; @doi 10.1007/978-3-031-38499-8_27
; Example 1
(format LCTRS :smtlib 2.6)
(theory Ints)

(fun max (-> 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))