; @author Akihisa Yamada
; @cops 1276
(format TRS :problem infeasibility)
(fun + 2)
(fun 0 0)
(fun s 1)
(rule (+ 0 x) x)
(rule (+ (s x) y) (s (+ x y)))
(infeasible? (= (+ (s x) y) (s y)))