; @author Raul Gutierrez
; @author Salvador Lucas
; @cops 918
(format CTRS oriented :problem infeasibility)
(fun 0 0)
(fun 1 0)
(fun and 2)
(fun f 1)
(fun implies 2)
(fun not 1)
(fun or 2)
(rule (or 0 x) x)
(rule (or x 0) x)
(rule (or 1 x) 1)
(rule (or x 1) 1)
(rule (or x (not x)) 1)
(rule (or (not x) x) 1)
(rule (and 0 x) 0)
(rule (and x 0) 0)
(rule (and 1 x) x)
(rule (and x 1) x)
(rule (and x (not x)) 0)
(rule (and (not x) x) 0)
(rule (not 1) 0)
(rule (not 0) 1)
(rule (implies x y) 1 (= (not x) 1))
(rule (implies x y) 1 (= y 1))
(rule (implies x y) 0 (= x 1) (= y 0))
(rule (f x) (f 0) (= (implies x 0) y) (= (implies x y) z) (= (implies z 0) 1))
(infeasible? (= (implies x 0) y) (= (implies x y) z) (= (implies z 0) 1))