|
1 #2 := false |
|
2 #9 := 1::int |
|
3 decl ?x1!1 :: int |
|
4 #91 := ?x1!1 |
|
5 #68 := -2::int |
|
6 #129 := (* -2::int ?x1!1) |
|
7 decl ?x2!0 :: int |
|
8 #90 := ?x2!0 |
|
9 #7 := 2::int |
|
10 #128 := (* 2::int ?x2!0) |
|
11 #130 := (+ #128 #129) |
|
12 #131 := (<= #130 1::int) |
|
13 #136 := (not #131) |
|
14 #55 := 0::int |
|
15 #53 := -1::int |
|
16 #115 := (* -1::int ?x1!1) |
|
17 #116 := (+ ?x2!0 #115) |
|
18 #117 := (<= #116 0::int) |
|
19 #139 := (or #117 #136) |
|
20 #142 := (not #139) |
|
21 #92 := (* -2::int ?x2!0) |
|
22 #93 := (* 2::int ?x1!1) |
|
23 #94 := (+ #93 #92) |
|
24 #95 := (>= #94 -1::int) |
|
25 #96 := (not #95) |
|
26 #97 := (* -1::int ?x2!0) |
|
27 #98 := (+ ?x1!1 #97) |
|
28 #99 := (>= #98 0::int) |
|
29 #100 := (or #99 #96) |
|
30 #101 := (not #100) |
|
31 #143 := (iff #101 #142) |
|
32 #140 := (iff #100 #139) |
|
33 #137 := (iff #96 #136) |
|
34 #134 := (iff #95 #131) |
|
35 #122 := (+ #92 #93) |
|
36 #125 := (>= #122 -1::int) |
|
37 #132 := (iff #125 #131) |
|
38 #133 := [rewrite]: #132 |
|
39 #126 := (iff #95 #125) |
|
40 #123 := (= #94 #122) |
|
41 #124 := [rewrite]: #123 |
|
42 #127 := [monotonicity #124]: #126 |
|
43 #135 := [trans #127 #133]: #134 |
|
44 #138 := [monotonicity #135]: #137 |
|
45 #120 := (iff #99 #117) |
|
46 #109 := (+ #97 ?x1!1) |
|
47 #112 := (>= #109 0::int) |
|
48 #118 := (iff #112 #117) |
|
49 #119 := [rewrite]: #118 |
|
50 #113 := (iff #99 #112) |
|
51 #110 := (= #98 #109) |
|
52 #111 := [rewrite]: #110 |
|
53 #114 := [monotonicity #111]: #113 |
|
54 #121 := [trans #114 #119]: #120 |
|
55 #141 := [monotonicity #121 #138]: #140 |
|
56 #144 := [monotonicity #141]: #143 |
|
57 #5 := (:var 0 int) |
|
58 #71 := (* -2::int #5) |
|
59 #4 := (:var 1 int) |
|
60 #8 := (* 2::int #4) |
|
61 #72 := (+ #8 #71) |
|
62 #70 := (>= #72 -1::int) |
|
63 #69 := (not #70) |
|
64 #57 := (* -1::int #5) |
|
65 #58 := (+ #4 #57) |
|
66 #56 := (>= #58 0::int) |
|
67 #75 := (or #56 #69) |
|
68 #78 := (forall (vars (?x1 int) (?x2 int)) #75) |
|
69 #81 := (not #78) |
|
70 #102 := (~ #81 #101) |
|
71 #103 := [sk]: #102 |
|
72 #11 := (* 2::int #5) |
|
73 #10 := (+ #8 1::int) |
|
74 #12 := (< #10 #11) |
|
75 #6 := (< #4 #5) |
|
76 #13 := (implies #6 #12) |
|
77 #14 := (forall (vars (?x1 int) (?x2 int)) #13) |
|
78 #15 := (not #14) |
|
79 #84 := (iff #15 #81) |
|
80 #32 := (+ 1::int #8) |
|
81 #35 := (< #32 #11) |
|
82 #41 := (not #6) |
|
83 #42 := (or #41 #35) |
|
84 #47 := (forall (vars (?x1 int) (?x2 int)) #42) |
|
85 #50 := (not #47) |
|
86 #82 := (iff #50 #81) |
|
87 #79 := (iff #47 #78) |
|
88 #76 := (iff #42 #75) |
|
89 #73 := (iff #35 #69) |
|
90 #74 := [rewrite]: #73 |
|
91 #66 := (iff #41 #56) |
|
92 #54 := (not #56) |
|
93 #61 := (not #54) |
|
94 #64 := (iff #61 #56) |
|
95 #65 := [rewrite]: #64 |
|
96 #62 := (iff #41 #61) |
|
97 #59 := (iff #6 #54) |
|
98 #60 := [rewrite]: #59 |
|
99 #63 := [monotonicity #60]: #62 |
|
100 #67 := [trans #63 #65]: #66 |
|
101 #77 := [monotonicity #67 #74]: #76 |
|
102 #80 := [quant-intro #77]: #79 |
|
103 #83 := [monotonicity #80]: #82 |
|
104 #51 := (iff #15 #50) |
|
105 #48 := (iff #14 #47) |
|
106 #45 := (iff #13 #42) |
|
107 #38 := (implies #6 #35) |
|
108 #43 := (iff #38 #42) |
|
109 #44 := [rewrite]: #43 |
|
110 #39 := (iff #13 #38) |
|
111 #36 := (iff #12 #35) |
|
112 #33 := (= #10 #32) |
|
113 #34 := [rewrite]: #33 |
|
114 #37 := [monotonicity #34]: #36 |
|
115 #40 := [monotonicity #37]: #39 |
|
116 #46 := [trans #40 #44]: #45 |
|
117 #49 := [quant-intro #46]: #48 |
|
118 #52 := [monotonicity #49]: #51 |
|
119 #85 := [trans #52 #83]: #84 |
|
120 #31 := [asserted]: #15 |
|
121 #86 := [mp #31 #85]: #81 |
|
122 #106 := [mp~ #86 #103]: #101 |
|
123 #107 := [mp #106 #144]: #142 |
|
124 #146 := [not-or-elim #107]: #131 |
|
125 #108 := (not #117) |
|
126 #145 := [not-or-elim #107]: #108 |
|
127 [th-lemma #145 #146]: false |
|
128 unsat |