test/regress/regress0/uf/euf_simp03.smt


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


(benchmark euf_simp3.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 (f x)) (f (f (f x))))
 (= (f (f x)) y)
 (= (f (f (f (f x)))) z)
 (= (f x) z)
 (not (= (f x) y))
 )
)