; @author Naoki Nishida
; @cops 880
(format CTRS oriented :problem infeasibility)
(fun a 0)
(fun b 0)
(fun d 0)
(fun f 2)
(fun g 1)
(fun h 1)
(fun s 1)
(rule (f x y) (g x) (= a d))
(rule (f x y) (h x) (= b d))
(rule (g (s x)) x)
(rule (h (s x)) x)
(rule a d)
(rule b d)
(infeasible? (= a d) (= b d))