; @author Naoki Nishida
; @cops 884
(format CTRS oriented :problem infeasibility)
(fun a 1)
(fun b 0)
(fun c 1)
(fun f 2)
(rule (f (c x) (c (c y))) (a (a x)) (= (c (f x y)) (c (a b))))
(rule (f (c (c (c x))) y) (a y) (= (c (f (c x) (c (c y)))) (c (a (a b)))))
(rule (a x) b)
(rule (a x) (f x x))
(infeasible? (= (c (f (c (c x1)) y)) (c (a b))) (= (c (f (c x1) (c (c (c (c y)))))) (c (a (a b)))))