; @author Naoki Nishida ; @cops 871 (format CTRS oriented :problem infeasibility) (fun A 0) (fun B 0) (fun a 0) (fun b 0) (fun c 0) (fun f 1) (fun g 2) (fun h 2) (fun s 1) (fun t 0) (rule (f x) A (= (s x) t)) (rule (f x) B (= (s x) t)) (rule (s a) t) (rule (s b) t) (rule a c) (rule b c) (rule (g x x) (h x x)) (infeasible? (= (s x1) t))