; @author Naoki Nishida
; @cops 886
(format CTRS oriented :problem infeasibility)
(fun 0 0)
(fun cons 2)
(fun eq 2)
(fun false 0)
(fun filter 3)
(fun lte 2)
(fun m 2)
(fun mod 2)
(fun nil 0)
(fun s 1)
(fun true 0)
(rule (eq 0 0) true)
(rule (eq (s x) 0) false)
(rule (eq 0 (s y)) false)
(rule (eq (s x) (s y)) (eq x y))
(rule (lte 0 y) true)
(rule (lte (s x) 0) false)
(rule (lte (s x) (s y)) (lte x y))
(rule (m 0 (s y)) 0)
(rule (m x 0) x)
(rule (m (s x) (s y)) (m x y))
(rule (mod 0 y) 0)
(rule (mod (s x) 0) 0)
(rule (mod (s x) (s y)) (mod (m x y) (s y)) (= (lte y x) true))
(rule (mod (s x) (s y)) (s x) (= (lte y x) false))
(rule (filter n r nil) nil)
(rule (filter n r (cons x xs)) (cons x (filter n r xs)) (= (mod x n) r') (= (eq r r') true))
(rule (filter n r (cons x xs)) (filter n r xs) (= (mod x n) r') (= (eq r r') false))
(infeasible? (= (lte x2 x1) true) (= (lte x2 x1) false))