blob: 351bc0c328320d123bd8754d7a519c263e9ec83a (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
|
;; (set-logic QF_SAT)
(declare-fun a () Bool)
(declare-fun b () Bool)
(declare-fun c () Bool)
(declare-fun d () Bool)
(declare-fun e () Bool)
(declare-fun f () Bool)
;; (declare-fun f (Bool Bool) Bool)
(assert (not (=> (and (=> a b) (=> b c)) (=> a c))))
(check-sat)
|