; @author Naoki Nishida
; @cops 834
(format CTRS oriented :problem infeasibility)
(fun 0 0)
(fun cons 2)
(fun false 0)
(fun le 2)
(fun min 1)
(fun nil 0)
(fun s 1)
(fun true 0)
(rule (le 0 (s x)) true)
(rule (le x 0) false)
(rule (le (s x) (s y)) (le x y))
(rule (min (cons x nil)) x)
(rule (min (cons x l)) x (= (le x (min l)) true))
(rule (min (cons x l)) (min l) (= (le x (min l)) false))
(rule (min (cons x l)) (min l) (= (min l) x))
(infeasible? (= (le x1 (min x2)) true) (= (le x1 (min x2)) false))