33010
|
1 |
(benchmark Isabelle
|
|
2 |
:extrasorts ( T1)
|
|
3 |
:extrapreds (
|
|
4 |
(up_1)
|
|
5 |
(up_2)
|
|
6 |
(up_3)
|
|
7 |
(up_4)
|
|
8 |
(up_5)
|
|
9 |
(up_6)
|
|
10 |
(up_8)
|
|
11 |
(up_9)
|
|
12 |
(up_7)
|
|
13 |
)
|
|
14 |
:assumption (or up_1 (or up_2 (or up_3 up_4)))
|
|
15 |
:assumption (or up_5 (or up_6 (and up_1 up_4)))
|
|
16 |
:assumption (or (not (or up_1 (and up_3 (not up_3)))) up_2)
|
|
17 |
:assumption (or (not (and up_2 (or up_7 (not up_7)))) up_3)
|
|
18 |
:assumption (or (not (or up_4 false)) up_3)
|
|
19 |
:assumption (not (or up_3 (and (not up_8) (or up_8 (and up_9 (not up_9))))))
|
|
20 |
:assumption (not false)
|
|
21 |
:formula true
|
|
22 |
)
|