equal
deleted
inserted
replaced
1 #2 := false |
|
2 #5 := 3::int |
|
3 #6 := 8::int |
|
4 #7 := (<= 3::int 8::int) |
|
5 #8 := (ite #7 8::int 3::int) |
|
6 #4 := 5::int |
|
7 #9 := (< 5::int #8) |
|
8 #10 := (not #9) |
|
9 #50 := (iff #10 false) |
|
10 #1 := true |
|
11 #45 := (not true) |
|
12 #48 := (iff #45 false) |
|
13 #49 := [rewrite]: #48 |
|
14 #46 := (iff #10 #45) |
|
15 #43 := (iff #9 true) |
|
16 #38 := (< 5::int 8::int) |
|
17 #41 := (iff #38 true) |
|
18 #42 := [rewrite]: #41 |
|
19 #39 := (iff #9 #38) |
|
20 #36 := (= #8 8::int) |
|
21 #31 := (ite true 8::int 3::int) |
|
22 #34 := (= #31 8::int) |
|
23 #35 := [rewrite]: #34 |
|
24 #32 := (= #8 #31) |
|
25 #29 := (iff #7 true) |
|
26 #30 := [rewrite]: #29 |
|
27 #33 := [monotonicity #30]: #32 |
|
28 #37 := [trans #33 #35]: #36 |
|
29 #40 := [monotonicity #37]: #39 |
|
30 #44 := [trans #40 #42]: #43 |
|
31 #47 := [monotonicity #44]: #46 |
|
32 #51 := [trans #47 #49]: #50 |
|
33 #26 := [asserted]: #10 |
|
34 [mp #26 #51]: false |
|
35 unsat |
|