equal
deleted
inserted
replaced
1 43550507f510d81bc4fb9ef8c1fd14424eaa9070 37 0 |
|
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 |
|