(meta-info (comment "Example 1 standard TRS taken from Nagele et al. 2016"))
(format LCTRS)

(fun f 2 :sort (Unit Unit Unit))

(rule (f (f x y) z) (f x (f y z)))
(rule (f x y) (f y x))
