|
1 #2 := false |
|
2 decl uf_1 :: int |
|
3 #5 := uf_1 |
|
4 #7 := 2::int |
|
5 #29 := (* 2::int uf_1) |
|
6 #4 := 0::int |
|
7 #54 := (= 0::int #29) |
|
8 #55 := (not #54) |
|
9 #61 := (= #29 0::int) |
|
10 #104 := (not #61) |
|
11 #110 := (iff #104 #55) |
|
12 #108 := (iff #61 #54) |
|
13 #109 := [commutativity]: #108 |
|
14 #111 := [monotonicity #109]: #110 |
|
15 #62 := (<= #29 0::int) |
|
16 #100 := (not #62) |
|
17 #30 := (<= uf_1 0::int) |
|
18 #31 := (not #30) |
|
19 #6 := (< 0::int uf_1) |
|
20 #32 := (iff #6 #31) |
|
21 #33 := [rewrite]: #32 |
|
22 #27 := [asserted]: #6 |
|
23 #34 := [mp #27 #33]: #31 |
|
24 #101 := (or #100 #30) |
|
25 #102 := [th-lemma]: #101 |
|
26 #103 := [unit-resolution #102 #34]: #100 |
|
27 #105 := (or #104 #62) |
|
28 #106 := [th-lemma]: #105 |
|
29 #107 := [unit-resolution #106 #103]: #104 |
|
30 #112 := [mp #107 #111]: #55 |
|
31 #56 := (= uf_1 #29) |
|
32 #57 := (not #56) |
|
33 #53 := (= 0::int uf_1) |
|
34 #50 := (not #53) |
|
35 #58 := (and #50 #55 #57) |
|
36 #69 := (not #58) |
|
37 #42 := (distinct 0::int uf_1 #29) |
|
38 #47 := (not #42) |
|
39 #9 := (- uf_1 uf_1) |
|
40 #8 := (* uf_1 2::int) |
|
41 #10 := (distinct uf_1 #8 #9) |
|
42 #11 := (not #10) |
|
43 #48 := (iff #11 #47) |
|
44 #45 := (iff #10 #42) |
|
45 #39 := (distinct uf_1 #29 0::int) |
|
46 #43 := (iff #39 #42) |
|
47 #44 := [rewrite]: #43 |
|
48 #40 := (iff #10 #39) |
|
49 #37 := (= #9 0::int) |
|
50 #38 := [rewrite]: #37 |
|
51 #35 := (= #8 #29) |
|
52 #36 := [rewrite]: #35 |
|
53 #41 := [monotonicity #36 #38]: #40 |
|
54 #46 := [trans #41 #44]: #45 |
|
55 #49 := [monotonicity #46]: #48 |
|
56 #28 := [asserted]: #11 |
|
57 #52 := [mp #28 #49]: #47 |
|
58 #80 := (or #42 #69) |
|
59 #81 := [def-axiom]: #80 |
|
60 #82 := [unit-resolution #81 #52]: #69 |
|
61 #59 := (= uf_1 0::int) |
|
62 #83 := (not #59) |
|
63 #89 := (iff #83 #50) |
|
64 #87 := (iff #59 #53) |
|
65 #88 := [commutativity]: #87 |
|
66 #90 := [monotonicity #88]: #89 |
|
67 #84 := (or #83 #30) |
|
68 #85 := [th-lemma]: #84 |
|
69 #86 := [unit-resolution #85 #34]: #83 |
|
70 #91 := [mp #86 #90]: #50 |
|
71 #64 := -1::int |
|
72 #65 := (* -1::int #29) |
|
73 #66 := (+ uf_1 #65) |
|
74 #68 := (>= #66 0::int) |
|
75 #92 := (not #68) |
|
76 #93 := (or #92 #30) |
|
77 #94 := [th-lemma]: #93 |
|
78 #95 := [unit-resolution #94 #34]: #92 |
|
79 #96 := (or #57 #68) |
|
80 #97 := [th-lemma]: #96 |
|
81 #98 := [unit-resolution #97 #95]: #57 |
|
82 #76 := (or #58 #53 #54 #56) |
|
83 #77 := [def-axiom]: #76 |
|
84 #99 := [unit-resolution #77 #98 #91 #82]: #54 |
|
85 [unit-resolution #99 #112]: false |
|
86 unsat |