|
33010
|
1 |
#2 := false
|
|
|
2 |
#7 := 4::int
|
|
|
3 |
#5 := 1::int
|
|
|
4 |
#4 := 3::int
|
|
|
5 |
#6 := (+ 3::int 1::int)
|
|
|
6 |
#8 := (= #6 4::int)
|
|
|
7 |
#9 := (not #8)
|
|
|
8 |
#39 := (iff #9 false)
|
|
|
9 |
#1 := true
|
|
|
10 |
#34 := (not true)
|
|
|
11 |
#37 := (iff #34 false)
|
|
|
12 |
#38 := [rewrite]: #37
|
|
|
13 |
#35 := (iff #9 #34)
|
|
|
14 |
#32 := (iff #8 true)
|
|
|
15 |
#27 := (= 4::int 4::int)
|
|
|
16 |
#30 := (iff #27 true)
|
|
|
17 |
#31 := [rewrite]: #30
|
|
|
18 |
#28 := (iff #8 #27)
|
|
|
19 |
#26 := [rewrite]: #8
|
|
|
20 |
#29 := [monotonicity #26]: #28
|
|
|
21 |
#33 := [trans #29 #31]: #32
|
|
|
22 |
#36 := [monotonicity #33]: #35
|
|
|
23 |
#40 := [trans #36 #38]: #39
|
|
|
24 |
#25 := [asserted]: #9
|
|
|
25 |
[mp #25 #40]: false
|
|
|
26 |
unsat
|