; @author Naoki Nishida
; @cops 848
(format CTRS oriented :problem infeasibility)
(fun 0 0)
(fun cons 2)
(fun false 0)
(fun le 2)
(fun nil 0)
(fun s 1)
(fun split 2)
(fun tp2 2)
(fun true 0)
(rule (split x nil) (tp2 nil nil))
(rule (split x (cons y ys)) (tp2 zs1 (cons y zs2)) (= (split x ys) (tp2 zs1 zs2)) (= (le x y) true))
(rule (split x (cons y ys)) (tp2 (cons y zs1) zs2) (= (split x ys) (tp2 zs1 zs2)) (= (le x y) false))
(rule (le 0 y) true)
(rule (le (s x) 0) false)
(rule (le (s x) (s y)) (le x y))
(infeasible? (= (split x1 x3) (tp2 zs1 zs2)) (= (le x1 x2) true) (= (split x1 x3) (tp2 x4 x5)) (= (le x1 x2) false))