1
(benchmark Isabelle
2
:extrasorts ( T2 T3 T1)
3
:extrafuns (
4
(uf_2 T1 T2)
5
(uf_3 T1 T3)
6
(uf_1 T2 T3 T1)
7
(uf_6 T2)
8
(uf_4 T2)
9
(uf_5 T3)
10
)
11
:assumption (forall (?x1 T1) (= (uf_1 (uf_2 ?x1) (uf_3 ?x1)) ?x1))
12
:assumption (forall (?x2 T2) (?x3 T3) (= (uf_3 (uf_1 ?x2 ?x3)) ?x3))
13
:assumption (forall (?x4 T2) (?x5 T3) (= (uf_2 (uf_1 ?x4 ?x5)) ?x4))
14
:assumption (= (uf_2 (uf_1 uf_4 uf_5)) uf_6)
15
:assumption (not (= uf_4 uf_6))
16
:formula true
17