blob: 03377005c0a68e0e2d5945d0880142c09e3d84b9 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
|
(set-logic QF_UF)
(set-info :status unsat)
(declare-sort U 0)
(declare-fun f (U) U)
(declare-fun g (U) U)
(declare-fun a () U)
(declare-fun b () U)
(declare-fun c () U)
(declare-fun d () U)
(declare-fun e () U)
(declare-fun h () U)
(declare-fun i () U)
(assert (or
(= a c)
(= h c)
(not (= h d))
(not (= h e))
(= h i)
(= (= (f a) d) (= d (f b)))
(= (not (= (f a) d)) (not (= d (f b))))
(not (= (not (= d (f b))) (= (f a) d)))
(not (= (= d (f b)) (not (= (f a) d))))
(xor (= (f a) d) (not (= d (f b))))
(xor (not (= (f a) d)) (= d (f b)))
(not (xor (= (f a) d) (= d (f b))))
(not (xor (not (= (f a) d)) (not (= d (f b)))))
))
(assert (not (= h i)))
(assert (or (not (= (f a) d)) (not (= d (f b)))))
(assert (or (= (f a) d) (= d (f b))))
(assert (and (not (= b e)) (not (= c a))))
(assert (and (= h e) (not (= b e))))
(assert (not (or (= b h) (= c h))))
(assert (not (or (= b h) (not (= d h)))))
(check-sat)
|
