; @author Naoki Nishida
; @cops 857
(format CTRS oriented :problem infeasibility)
(fun 0 0)
(fun div 2)
(fun false 0)
(fun lt 2)
(fun m 2)
(fun pair 2)
(fun s 1)
(fun true 0)
(rule (lt x 0) false)
(rule (lt 0 (s x)) true)
(rule (lt (s x) (s y)) (lt x y))
(rule (m 0 (s y)) 0)
(rule (m x 0) x)
(rule (m (s x) (s y)) (m x y))
(rule (div 0 (s x)) (pair 0 0))
(rule (div (s x) (s y)) (pair 0 (s x)) (= (lt x y) true))
(rule (div (s x) (s y)) (pair (s q) r) (= (lt x y) false) (= (div (m x y) (s y)) (pair q r)))
(infeasible? (= (lt x1 x2) true) (= (lt x1 x2) false) (= (div (m x1 x2) (s x2)) (pair x3 x4)))