equal
deleted
inserted
replaced
|
1 (benchmark Isabelle |
|
2 :extrafuns ( |
|
3 (uf_2 Int) |
|
4 (uf_1 Int) |
|
5 ) |
|
6 :assumption (= (mod (+ uf_1 uf_2) 2) 0) |
|
7 :assumption (= (mod uf_1 4) 3) |
|
8 :assumption (not (and (= (mod uf_1 2) 1) (= (mod uf_2 2) 1))) |
|
9 :formula true |
|
10 ) |