; @author Naoki Nishida
; @cops 853
(format CTRS oriented :problem infeasibility)
(fun 0 0)
(fun app 2)
(fun cons 2)
(fun false 0)
(fun le 2)
(fun nil 0)
(fun pair 2)
(fun qsort 1)
(fun s 1)
(fun split 2)
(fun true 0)
(rule (le 0 x) true)
(rule (le (s x) 0) false)
(rule (le (s x) (s y)) (le x y))
(rule (app nil x) x)
(rule (app (cons x xs) ys) (cons x (app xs ys)))
(rule (split x nil) (pair nil nil))
(rule (qsort nil) nil)
(rule (split x (cons y ys)) (pair xs (cons y zs)) (= (split x ys) (pair xs zs)) (= (le x y) true))
(rule (split x (cons y ys)) (pair (cons y xs) zs) (= (split x ys) (pair xs zs)) (= (le x y) false))
(rule (qsort (cons x xs)) (app (qsort ys) (cons x (qsort zs))) (= (split x xs) (pair ys zs)))
(infeasible? (= (split x1 x3) (pair xs zs)) (= (le x1 x2) true) (= (split x1 x3) (pair x4 x5)) (= (le x1 x2) false))