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

(fun f 4 :sort (Unit Unit Unit Unit Unit))
(fun a 0 :sort (Unit))
(fun b 0 :sort (Unit))
(fun c 0 :sort (Unit))
(fun d 0 :sort (Unit))

(rule (f a a b b) (f c c c c))
(rule a b)
(rule a c)
(rule b a)
(rule b c)