; @author Naoki Nishida
; @cops 893
(format CTRS oriented :problem infeasibility)
(fun 0 0)
(fun add 2)
(fun div 2)
(fun false 0)
(fun lte 2)
(fun minus 2)
(fun mod 2)
(fun mult 2)
(fun power 2)
(fun s 1)
(fun true 0)
(rule (add 0 x) x)
(rule (add (s x) y) (s (add x y)))
(rule (mult 0 y) 0)
(rule (mult (s x) y) (add (mult x y) y))
(rule (lte 0 y) true)
(rule (lte (s x) 0) false)
(rule (lte (s x) (s y)) (lte x y))
(rule (minus 0 (s y)) 0)
(rule (minus x 0) x)
(rule (minus (s x) (s y)) (minus x y))
(rule (mod 0 y) 0)
(rule (mod x 0) x)
(rule (mod x (s y)) (mod (minus x (s y)) (s y)) (= (lte (s y) x) true))
(rule (mod x (s y)) x (= (lte (s y) x) false))
(rule (div 0 (s x)) 0)
(rule (div (s x) (s y)) 0 (= (lte (s x) y) true))
(rule (div (s x) (s y)) (s q) (= (lte (s x) y) false) (= (div (minus x y) (s y)) q))
(rule (power x 0) (s 0))
(rule (power x n) (mult (mult y y) (s 0)) (= (mod n (s (s 0))) 0) (= (power x (div n (s (s 0)))) y))
(rule (power x n) (mult (mult y y) x) (= (mod n (s (s 0))) (s z)) (= (power x (div n (s (s 0)))) y))
(infeasible? (= (lte (s x1) x2) true) (= (lte (s x1) x2) false) (= (div (minus x1 x2) (s x2)) x3))