; @author Naoki Nishida
; @cops 852
(format CTRS oriented :problem infeasibility)
(fun 0 0)
(fun false 0)
(fun gcd 2)
(fun lt 2)
(fun m 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 (gcd x x) x)
(rule (gcd (s x) 0) (s x))
(rule (gcd 0 (s y)) (s y))
(rule (gcd (s x) (s y)) (gcd (m x y) (s y)) (= (lt y x) true))
(rule (gcd (s x) (s y)) (gcd (s x) (m y x)) (= (lt x y) true))
(infeasible? (= (lt x2 x2) true))