|
33010
|
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
|