; @author Naoki Nishida
; @cops 808
(format CTRS oriented :problem infeasibility)
(fun 0 0)
(fun cons 2)
(fun false 0)
(fun insert 2)
(fun lte 2)
(fun nil 0)
(fun ordered 1)
(fun s 1)
(fun true 0)
(rule (lte 0 n) true)
(rule (lte (s m) 0) false)
(rule (lte (s m) (s n)) (lte m n))
(rule (insert nil m) (cons m nil))
(rule (insert (cons n l) m) (cons m (cons n l)) (= (lte m n) true))
(rule (insert (cons n l) m) (cons n (insert l m)) (= (lte m n) false))
(rule (ordered nil) true)
(rule (ordered (cons m nil)) true)
(rule (ordered (cons m (cons n l))) (ordered (cons n l)) (= (lte m n) true))
(rule (ordered (cons m (cons n l))) false (= (lte m n) false))
(infeasible? (= (lte x3 x1) true) (= (lte x3 x1) false))