equal
deleted
inserted
replaced
1 #2 := false |
|
2 decl uf_1 :: int |
|
3 #4 := uf_1 |
|
4 decl uf_3 :: int |
|
5 #6 := uf_3 |
|
6 #9 := (+ uf_3 uf_1) |
|
7 decl uf_2 :: int |
|
8 #5 := uf_2 |
|
9 #10 := (+ uf_2 #9) |
|
10 #7 := (+ uf_2 uf_3) |
|
11 #8 := (+ uf_1 #7) |
|
12 #11 := (= #8 #10) |
|
13 #12 := (not #11) |
|
14 #51 := (iff #12 false) |
|
15 #1 := true |
|
16 #46 := (not true) |
|
17 #49 := (iff #46 false) |
|
18 #50 := [rewrite]: #49 |
|
19 #47 := (iff #12 #46) |
|
20 #44 := (iff #11 true) |
|
21 #39 := (= #8 #8) |
|
22 #42 := (iff #39 true) |
|
23 #43 := [rewrite]: #42 |
|
24 #40 := (iff #11 #39) |
|
25 #37 := (= #10 #8) |
|
26 #29 := (+ uf_1 uf_3) |
|
27 #32 := (+ uf_2 #29) |
|
28 #35 := (= #32 #8) |
|
29 #36 := [rewrite]: #35 |
|
30 #33 := (= #10 #32) |
|
31 #30 := (= #9 #29) |
|
32 #31 := [rewrite]: #30 |
|
33 #34 := [monotonicity #31]: #33 |
|
34 #38 := [trans #34 #36]: #37 |
|
35 #41 := [monotonicity #38]: #40 |
|
36 #45 := [trans #41 #43]: #44 |
|
37 #48 := [monotonicity #45]: #47 |
|
38 #52 := [trans #48 #50]: #51 |
|
39 #28 := [asserted]: #12 |
|
40 [mp #28 #52]: false |
|
41 unsat |
|