blob: 9c7b03f6ecc6fe35f189fab602e6cf89bcb84ffe (
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
|
(benchmark euf_simp2.smt
:status unsat
:logic QF_UF
:category { crafted }
:extrafuns ((x U))
:extrafuns ((y U))
:extrafuns ((z U))
:extrafuns ((f U U))
:extrafuns ((g U U))
:extrafuns ((H U U U))
:extrafuns ((J U U U))
:formula
(and
(not (= x y))
(= (f x) (f z))
(= (g y) (g z))
(= (g y) (g z))
(= (g y) y)
(= (f x) x)
(= (f z) z)
(= (g z) z)
(or (not (= x z)) (not (= y z)))
)
)
|