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