blob: 7b15ad309eef76ff47567b8dc97e210ac93a5fc7 (
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
|
(benchmark euf_simp4.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
(= (H x y) (H y x))
(or (= x (J z y)) (= y (J z y)))
(= (J z y) (f x))
(or (= x (f x)) (not (= y (f x))) )
(or (not (= x (f x))) (not (= (H x (f x)) (H (f x) x) )) )
)
)
|
