| author | wenzelm |
| Mon, 18 Aug 2014 12:17:31 +0200 | |
| changeset 57978 | 8f4a332500e4 |
| parent 56727 | 75f4fdafb285 |
| permissions | -rw-r--r-- |
|
50662
b1f4291eb916
regenerate certificates -- and use oracle in a few cases where the Z3 proof parser can't deal with Z3 3.2 proofs
blanchet
parents:
49995
diff
changeset
|
1 |
43550507f510d81bc4fb9ef8c1fd14424eaa9070 37 0 |
| 53824 | 2 |
#2 := false |
3 |
#10 := 0::Int |
|
4 |
decl f3 :: Int |
|
5 |
#7 := f3 |
|
6 |
#12 := (<= f3 0::Int) |
|
7 |
#54 := (not #12) |
|
8 |
decl f4 :: Int |
|
9 |
#8 := f4 |
|
10 |
#13 := (<= f4 0::Int) |
|
11 |
#9 := (* f3 f4) |
|
12 |
#11 := (<= #9 0::Int) |
|
13 |
#37 := (not #11) |
|
14 |
#44 := (or #37 #12 #13) |
|
15 |
#47 := (not #44) |
|
16 |
#14 := (or #12 #13) |
|
17 |
#15 := (implies #11 #14) |
|
18 |
#16 := (not #15) |
|
19 |
#50 := (iff #16 #47) |
|
20 |
#38 := (or #37 #14) |
|
21 |
#41 := (not #38) |
|
22 |
#48 := (iff #41 #47) |
|
23 |
#45 := (iff #38 #44) |
|
24 |
#46 := [rewrite]: #45 |
|
25 |
#49 := [monotonicity #46]: #48 |
|
26 |
#42 := (iff #16 #41) |
|
27 |
#39 := (iff #15 #38) |
|
28 |
#40 := [rewrite]: #39 |
|
29 |
#43 := [monotonicity #40]: #42 |
|
30 |
#51 := [trans #43 #49]: #50 |
|
31 |
#36 := [asserted]: #16 |
|
32 |
#52 := [mp #36 #51]: #47 |
|
33 |
#55 := [not-or-elim #52]: #54 |
|
34 |
#56 := (not #13) |
|
35 |
#57 := [not-or-elim #52]: #56 |
|
36 |
#53 := [not-or-elim #52]: #11 |
|
37 |
[th-lemma arith farkas 1 1 1 #53 #57 #55]: false |
|
38 |
unsat |