equal
deleted
inserted
replaced
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 |
|