equal
deleted
inserted
replaced
|
1 (benchmark Isabelle |
|
2 :extrafuns ( |
|
3 (uf_3 Int) |
|
4 (uf_2 Int) |
|
5 (uf_1 Int) |
|
6 (uf_4 Int) |
|
7 (uf_5 Int) |
|
8 (uf_6 Int) |
|
9 (uf_7 Int) |
|
10 (uf_8 Int) |
|
11 (uf_9 Int) |
|
12 (uf_10 Int) |
|
13 (uf_11 Int) |
|
14 ) |
|
15 :assumption (= uf_1 (- (ite (< uf_2 0) (~ uf_2) uf_2) uf_3)) |
|
16 :assumption (= uf_4 (- (ite (< uf_1 0) (~ uf_1) uf_1) uf_2)) |
|
17 :assumption (= uf_5 (- (ite (< uf_4 0) (~ uf_4) uf_4) uf_1)) |
|
18 :assumption (= uf_6 (- (ite (< uf_5 0) (~ uf_5) uf_5) uf_4)) |
|
19 :assumption (= uf_7 (- (ite (< uf_6 0) (~ uf_6) uf_6) uf_5)) |
|
20 :assumption (= uf_8 (- (ite (< uf_7 0) (~ uf_7) uf_7) uf_6)) |
|
21 :assumption (= uf_9 (- (ite (< uf_8 0) (~ uf_8) uf_8) uf_7)) |
|
22 :assumption (= uf_10 (- (ite (< uf_9 0) (~ uf_9) uf_9) uf_8)) |
|
23 :assumption (= uf_11 (- (ite (< uf_10 0) (~ uf_10) uf_10) uf_9)) |
|
24 :assumption (not (and (= uf_3 uf_10) (= uf_2 uf_11))) |
|
25 :formula true |
|
26 ) |