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