; @author Naoki Nishida
; @cops 861
(format CTRS oriented :problem infeasibility)
(fun 0 0)
(fun cons 2)
(fun get 1)
(fun nil 0)
(fun s 1)
(fun ssp' 2)
(fun sub 2)
(fun tp2 2)
(rule (ssp' xs 0) nil)
(rule (ssp' (cons y' ws) v) (cons y' ys') (= (sub v y') w) (= (ssp' ws w) ys'))
(rule (ssp' (cons x' xs') v) (cons y' ys') (= (get xs') (tp2 y' zs)) (= (sub v y') w) (= (ssp' (cons x' zs) w) ys'))
(rule (sub z 0) z)
(rule (sub (s v) (s w)) z (= (sub v w) z))
(rule (get (cons y ys)) (tp2 y ys))
(rule (get (cons x' xs')) (tp2 y (cons x' zs)) (= (get xs') (tp2 y zs)))
(infeasible? (= (get x2) (tp2 x3 x4)))