57170
|
1 |
3587bd3f21d47d812a1b3b30d0e7ce50216a24d3 779 0
|
|
2 |
unsat
|
|
3 |
((set-logic AUFLIA)
|
|
4 |
(declare-fun ?v0!3 () Int)
|
|
5 |
(declare-fun ?v0!2 () Int)
|
|
6 |
(declare-fun ?v0!1 () Int)
|
|
7 |
(declare-fun ?v0!0 () Int)
|
|
8 |
(proof
|
|
9 |
(let (($x109 (= v_b_max_G_3$ v_b_max_G_2$)))
|
|
10 |
(let ((?x135 (v_b_array$ v_b_k_G_1$)))
|
|
11 |
(let (($x136 (= ?x135 v_b_max_G_3$)))
|
|
12 |
(let (($x1878 (forall ((?v0 Int) )(!(let (($x746 (<= (+ (v_b_array$ ?v0) (* (- 1) v_b_max_G_3$)) 0)))
|
|
13 |
(let (($x733 (>= (+ ?v0 (* (- 1) v_b_p_G_1$)) 0)))
|
|
14 |
(let (($x521 (>= ?v0 0)))
|
|
15 |
(let (($x1157 (not $x521)))
|
|
16 |
(or $x1157 $x733 $x746))))) :pattern ( (v_b_array$ ?v0) )))
|
|
17 |
))
|
|
18 |
(let (($x1883 (not $x1878)))
|
|
19 |
(let (($x1886 (or $x1883 $x136)))
|
|
20 |
(let (($x1889 (not $x1886)))
|
|
21 |
(let (($x1070 (>= (+ v_b_max_G_3$ (* (- 1) (v_b_array$ ?v0!3))) 0)))
|
|
22 |
(let (($x1048 (<= (+ v_b_p_G_1$ (* (- 1) ?v0!3)) 0)))
|
|
23 |
(let (($x931 (>= ?v0!3 0)))
|
|
24 |
(let (($x1298 (not $x931)))
|
|
25 |
(let (($x1313 (or $x1298 $x1048 $x1070)))
|
|
26 |
(let (($x1318 (not $x1313)))
|
|
27 |
(let (($x1892 (or $x1318 $x1889)))
|
|
28 |
(let (($x1895 (not $x1892)))
|
|
29 |
(let (($x682 (>= v_b_p_G_1$ 2)))
|
|
30 |
(let (($x1364 (not $x682)))
|
|
31 |
(let (($x679 (>= v_b_k_G_1$ 0)))
|
|
32 |
(let (($x1363 (not $x679)))
|
|
33 |
(let ((?x685 (* (- 1) v_b_p_G_1$)))
|
|
34 |
(let ((?x686 (+ v_b_p_G_0$ ?x685)))
|
|
35 |
(let (($x684 (= ?x686 (- 1))))
|
|
36 |
(let (($x1362 (not $x684)))
|
|
37 |
(let (($x573 (>= v_b_p_G_0$ 1)))
|
|
38 |
(let (($x1287 (not $x573)))
|
|
39 |
(let (($x1361 (not $x109)))
|
|
40 |
(let (($x107 (= v_b_k_G_1$ v_b_p_G_0$)))
|
|
41 |
(let (($x1360 (not $x107)))
|
|
42 |
(let ((?x101 (v_b_array$ v_b_p_G_0$)))
|
|
43 |
(let (($x104 (= v_b_max_G_2$ ?x101)))
|
|
44 |
(let (($x1359 (not $x104)))
|
|
45 |
(let (($x689 (>= (+ v_b_max_G_1$ (* (- 1) ?x101)) 0)))
|
|
46 |
(let (($x571 (>= v_b_k_G_0$ 0)))
|
|
47 |
(let (($x1286 (not $x571)))
|
|
48 |
(let (($x1898 (or $x1286 $x689 $x1359 $x1360 $x1361 $x1287 $x1362 $x1363 $x1364 $x1895)))
|
|
49 |
(let (($x1901 (not $x1898)))
|
|
50 |
(let (($x145 (= v_b_max_G_3$ v_b_max_G_1$)))
|
|
51 |
(let (($x1376 (not $x145)))
|
|
52 |
(let (($x144 (= v_b_k_G_1$ v_b_k_G_0$)))
|
|
53 |
(let (($x1375 (not $x144)))
|
|
54 |
(let (($x692 (not $x689)))
|
|
55 |
(let (($x1904 (or $x692 $x1286 $x1375 $x1376 $x1287 $x1362 $x1363 $x1364 $x1895)))
|
|
56 |
(let ((?x937 (v_b_array$ ?v0!3)))
|
|
57 |
(let (($x1559 (= ?x101 ?x937)))
|
|
58 |
(let (($x1563 (not $x1559)))
|
|
59 |
(let ((?x1068 (* (- 1) ?x937)))
|
|
60 |
(let ((?x1461 (+ ?x101 ?x1068)))
|
|
61 |
(let (($x1445 (>= ?x1461 0)))
|
|
62 |
(let (($x1453 (not $x1445)))
|
|
63 |
(let (($x1907 (not $x1904)))
|
|
64 |
(let ((@x2149 (hypothesis $x1907)))
|
|
65 |
(let ((?x744 (* (- 1) v_b_max_G_3$)))
|
|
66 |
(let ((?x1781 (+ v_b_max_G_1$ ?x744)))
|
|
67 |
(let (($x1782 (<= ?x1781 0)))
|
|
68 |
(let (($x1780 (= v_b_max_G_1$ v_b_max_G_3$)))
|
|
69 |
(let ((@x2162 (mp (unit-resolution (def-axiom (or $x1904 $x145)) @x2149 $x145) (symm (commutativity (= $x1780 $x145)) (= $x145 $x1780)) $x1780)))
|
|
70 |
(let (($x1436 (not $x1070)))
|
|
71 |
(let ((?x62 (v_b_array$ v_b_k_G_0$)))
|
|
72 |
(let (($x63 (= ?x62 v_b_max_G_1$)))
|
|
73 |
(let (($x1910 (or $x1901 $x1907)))
|
|
74 |
(let (($x1913 (not $x1910)))
|
|
75 |
(let ((?x549 (* (- 1) v_b_p_G_0$)))
|
|
76 |
(let ((?x599 (+ v_b_length$ ?x549)))
|
|
77 |
(let (($x600 (<= ?x599 0)))
|
|
78 |
(let (($x1916 (or $x600 $x1286 $x1287 $x1913)))
|
|
79 |
(let (($x1919 (not $x1916)))
|
|
80 |
(let (($x1011 (>= (+ v_b_max_G_4$ (* (- 1) (v_b_array$ ?v0!2))) 0)))
|
|
81 |
(let (($x900 (<= (+ v_b_length$ (* (- 1) ?v0!2)) 0)))
|
|
82 |
(let (($x897 (>= ?v0!2 0)))
|
|
83 |
(let (($x1247 (not $x897)))
|
|
84 |
(let (($x889 (= (v_b_array$ ?v0!1) v_b_max_G_4$)))
|
|
85 |
(let (($x884 (<= (+ v_b_length$ (* (- 1) ?v0!1)) 0)))
|
|
86 |
(let (($x881 (>= ?v0!1 0)))
|
|
87 |
(let (($x1227 (not $x881)))
|
|
88 |
(let (($x1242 (or $x1227 $x884 $x889)))
|
|
89 |
(let (($x1273 (not $x1242)))
|
|
90 |
(let (($x1274 (or $x1273 $x1247 $x900 $x1011)))
|
|
91 |
(let (($x1275 (not $x1274)))
|
|
92 |
(let (($x1861 (forall ((?v0 Int) )(!(let ((?x46 (v_b_array$ ?v0)))
|
|
93 |
(let (($x86 (= ?x46 v_b_max_G_4$)))
|
|
94 |
(let (($x622 (<= (+ v_b_length$ (* (- 1) ?v0)) 0)))
|
|
95 |
(let (($x521 (>= ?v0 0)))
|
|
96 |
(let (($x1157 (not $x521)))
|
|
97 |
(let (($x1216 (or $x1157 $x622 $x86)))
|
|
98 |
(not $x1216))))))) :pattern ( (v_b_array$ ?v0) )))
|
|
99 |
))
|
|
100 |
(let (($x1866 (or $x1861 $x1275)))
|
|
101 |
(let (($x1869 (not $x1866)))
|
|
102 |
(let (($x75 (= v_b_p_G_2$ v_b_p_G_0$)))
|
|
103 |
(let (($x1290 (not $x75)))
|
|
104 |
(let (($x73 (= v_b_max_G_4$ v_b_max_G_1$)))
|
|
105 |
(let (($x1289 (not $x73)))
|
|
106 |
(let (($x71 (= v_b_k_G_2$ v_b_k_G_0$)))
|
|
107 |
(let (($x1288 (not $x71)))
|
|
108 |
(let (($x661 (not $x600)))
|
|
109 |
(let (($x1872 (or $x661 $x1286 $x1287 $x1288 $x1289 $x1290 $x1869)))
|
|
110 |
(let (($x1875 (not $x1872)))
|
|
111 |
(let (($x1922 (or $x1875 $x1919)))
|
|
112 |
(let (($x1925 (not $x1922)))
|
|
113 |
(let (($x1403 (not $x63)))
|
|
114 |
(let (($x1853 (forall ((?v0 Int) )(!(let (($x561 (<= (+ (v_b_array$ ?v0) (* (- 1) v_b_max_G_1$)) 0)))
|
|
115 |
(let (($x548 (>= (+ ?v0 (* (- 1) v_b_p_G_0$)) 0)))
|
|
116 |
(let (($x521 (>= ?v0 0)))
|
|
117 |
(let (($x1157 (not $x521)))
|
|
118 |
(or $x1157 $x548 $x561))))) :pattern ( (v_b_array$ ?v0) )))
|
|
119 |
))
|
|
120 |
(let (($x1858 (not $x1853)))
|
|
121 |
(let ((?x30 (v_b_array$ 0)))
|
|
122 |
(let (($x50 (= ?x30 v_b_max_G_0$)))
|
|
123 |
(let (($x851 (not $x50)))
|
|
124 |
(let (($x1928 (or $x851 $x1858 $x1403 $x1286 $x1287 $x1925)))
|
|
125 |
(let (($x1931 (not $x1928)))
|
|
126 |
(let (($x1934 (or $x851 $x1931)))
|
|
127 |
(let (($x1937 (not $x1934)))
|
|
128 |
(let (($x1845 (forall ((?v0 Int) )(!(let (($x534 (>= (+ v_b_max_G_0$ (* (- 1) (v_b_array$ ?v0))) 0)))
|
|
129 |
(let (($x524 (>= ?v0 1)))
|
|
130 |
(let (($x521 (>= ?v0 0)))
|
|
131 |
(let (($x1157 (not $x521)))
|
|
132 |
(or $x1157 $x524 $x534))))) :pattern ( (v_b_array$ ?v0) )))
|
|
133 |
))
|
|
134 |
(let (($x1850 (not $x1845)))
|
|
135 |
(let (($x1940 (or $x1850 $x1937)))
|
|
136 |
(let (($x1943 (not $x1940)))
|
|
137 |
(let (($x839 (>= (+ v_b_max_G_0$ (* (- 1) (v_b_array$ ?v0!0))) 0)))
|
|
138 |
(let (($x832 (>= ?v0!0 1)))
|
|
139 |
(let (($x835 (>= ?v0!0 0)))
|
|
140 |
(let (($x1134 (not $x835)))
|
|
141 |
(let (($x1149 (or $x1134 $x832 $x839)))
|
|
142 |
(let (($x833 (not $x832)))
|
|
143 |
(let (($x1154 (not $x1149)))
|
|
144 |
(let ((@x1726 (hypothesis $x1154)))
|
|
145 |
(let ((@x1711 ((_ th-lemma arith eq-propagate 0 0) (unit-resolution (def-axiom (or $x1149 $x835)) @x1726 $x835) (unit-resolution (def-axiom (or $x1149 $x833)) @x1726 $x833) (= ?v0!0 0))))
|
|
146 |
(let ((@x1715 (symm (monotonicity @x1711 (= (v_b_array$ ?v0!0) ?x30)) (= ?x30 (v_b_array$ ?v0!0)))))
|
|
147 |
(let (($x31 (= v_b_max_G_0$ ?x30)))
|
|
148 |
(let (($x495 (<= v_b_length$ 0)))
|
|
149 |
(let (($x496 (not $x495)))
|
|
150 |
(let (($x511 (and $x496 $x31)))
|
|
151 |
(let (($x752 (forall ((?v0 Int) )(let (($x746 (<= (+ (v_b_array$ ?v0) (* (- 1) v_b_max_G_3$)) 0)))
|
|
152 |
(let (($x521 (>= ?v0 0)))
|
|
153 |
(let (($x738 (and $x521 (not (>= (+ ?v0 (* (- 1) v_b_p_G_1$)) 0)))))
|
|
154 |
(let (($x741 (not $x738)))
|
|
155 |
(or $x741 $x746))))))
|
|
156 |
))
|
|
157 |
(let (($x755 (not $x752)))
|
|
158 |
(let (($x758 (or $x755 $x136)))
|
|
159 |
(let (($x761 (and $x752 $x758)))
|
|
160 |
(let (($x784 (and $x689 $x571 $x144 $x145 $x573 $x684 $x679 $x682)))
|
|
161 |
(let (($x789 (not $x784)))
|
|
162 |
(let (($x792 (or $x789 $x761)))
|
|
163 |
(let (($x725 (and $x571 $x692 $x104 $x107 $x109 $x573 $x684 $x679 $x682)))
|
|
164 |
(let (($x730 (not $x725)))
|
|
165 |
(let (($x764 (or $x730 $x761)))
|
|
166 |
(let (($x795 (and $x764 $x792)))
|
|
167 |
(let (($x670 (and $x661 $x571 $x573)))
|
|
168 |
(let (($x675 (not $x670)))
|
|
169 |
(let (($x798 (or $x675 $x795)))
|
|
170 |
(let (($x649 (forall ((?v0 Int) )(let (($x521 (>= ?v0 0)))
|
|
171 |
(let (($x626 (and $x521 (not (<= (+ v_b_length$ (* (- 1) ?v0)) 0)))))
|
|
172 |
(let (($x629 (not $x626)))
|
|
173 |
(or $x629 (<= (+ (v_b_array$ ?v0) (* (- 1) v_b_max_G_4$)) 0))))))
|
|
174 |
))
|
|
175 |
(let (($x635 (exists ((?v0 Int) )(let ((?x46 (v_b_array$ ?v0)))
|
|
176 |
(let (($x86 (= ?x46 v_b_max_G_4$)))
|
|
177 |
(let (($x521 (>= ?v0 0)))
|
|
178 |
(let (($x626 (and $x521 (not (<= (+ v_b_length$ (* (- 1) ?v0)) 0)))))
|
|
179 |
(let (($x629 (not $x626)))
|
|
180 |
(or $x629 $x86)))))))
|
|
181 |
))
|
|
182 |
(let (($x638 (not $x635)))
|
|
183 |
(let (($x652 (or $x638 $x649)))
|
|
184 |
(let (($x655 (and $x635 $x652)))
|
|
185 |
(let (($x612 (and $x600 $x571 $x573 $x71 $x73 $x75)))
|
|
186 |
(let (($x617 (not $x612)))
|
|
187 |
(let (($x658 (or $x617 $x655)))
|
|
188 |
(let (($x801 (and $x658 $x798)))
|
|
189 |
(let (($x567 (forall ((?v0 Int) )(let (($x561 (<= (+ (v_b_array$ ?v0) (* (- 1) v_b_max_G_1$)) 0)))
|
|
190 |
(let (($x521 (>= ?v0 0)))
|
|
191 |
(let (($x553 (and $x521 (not (>= (+ ?v0 (* (- 1) v_b_p_G_0$)) 0)))))
|
|
192 |
(let (($x556 (not $x553)))
|
|
193 |
(or $x556 $x561))))))
|
|
194 |
))
|
|
195 |
(let (($x591 (and $x50 $x567 $x63 $x571 $x573)))
|
|
196 |
(let (($x596 (not $x591)))
|
|
197 |
(let (($x804 (or $x596 $x801)))
|
|
198 |
(let (($x807 (and $x50 $x804)))
|
|
199 |
(let (($x541 (forall ((?v0 Int) )(let (($x534 (>= (+ v_b_max_G_0$ (* (- 1) (v_b_array$ ?v0))) 0)))
|
|
200 |
(let (($x521 (>= ?v0 0)))
|
|
201 |
(let (($x526 (and $x521 (not (>= ?v0 1)))))
|
|
202 |
(let (($x529 (not $x526)))
|
|
203 |
(or $x529 $x534))))))
|
|
204 |
))
|
|
205 |
(let (($x544 (not $x541)))
|
|
206 |
(let (($x810 (or $x544 $x807)))
|
|
207 |
(let (($x813 (and $x541 $x810)))
|
|
208 |
(let (($x819 (not (or (not $x511) $x813))))
|
|
209 |
(let (($x138 (=> (and $x136 false) true)))
|
|
210 |
(let (($x139 (and $x136 $x138)))
|
|
211 |
(let (($x134 (forall ((?v0 Int) )(let ((?x46 (v_b_array$ ?v0)))
|
|
212 |
(let (($x132 (<= ?x46 v_b_max_G_3$)))
|
|
213 |
(let (($x43 (<= 0 ?v0)))
|
|
214 |
(let (($x131 (and $x43 (< ?v0 v_b_p_G_1$))))
|
|
215 |
(=> $x131 $x132))))))
|
|
216 |
))
|
|
217 |
(let (($x140 (=> $x134 $x139)))
|
|
218 |
(let (($x141 (and $x134 $x140)))
|
|
219 |
(let (($x119 (and (= v_b_p_G_1$ (+ v_b_p_G_0$ 1)) (and (and (<= 0 v_b_k_G_1$) (<= 2 v_b_p_G_1$)) true))))
|
|
220 |
(let (($x54 (<= 1 v_b_p_G_0$)))
|
|
221 |
(let (($x110 (<= 0 v_b_k_G_1$)))
|
|
222 |
(let (($x111 (and $x110 $x54)))
|
|
223 |
(let (($x121 (and true (and $x111 $x119))))
|
|
224 |
(let (($x148 (and true (and $x144 (and $x145 $x121)))))
|
|
225 |
(let (($x55 (and (<= 0 v_b_k_G_0$) $x54)))
|
|
226 |
(let (($x143 (<= ?x101 v_b_max_G_1$)))
|
|
227 |
(let (($x152 (and true (and $x55 (and $x143 (and $x55 $x148))))))
|
|
228 |
(let (($x153 (=> $x152 $x141)))
|
|
229 |
(let (($x126 (and $x104 (and (and $x54 $x54) (and true (and $x107 (and $x109 $x121)))))))
|
|
230 |
(let (($x102 (< v_b_max_G_1$ ?x101)))
|
|
231 |
(let (($x129 (and true (and $x55 (and $x102 $x126)))))
|
|
232 |
(let (($x142 (=> $x129 $x141)))
|
|
233 |
(let (($x155 (=> (and true (and $x55 (and (< v_b_p_G_0$ v_b_length$) $x55))) (and $x142 $x153))))
|
|
234 |
(let (($x91 (forall ((?v0 Int) )(let ((?x46 (v_b_array$ ?v0)))
|
|
235 |
(let (($x89 (<= ?x46 v_b_max_G_4$)))
|
|
236 |
(let (($x43 (<= 0 ?v0)))
|
|
237 |
(let (($x85 (and $x43 (< ?v0 v_b_length$))))
|
|
238 |
(=> $x85 $x89))))))
|
|
239 |
))
|
|
240 |
(let (($x92 (=> $x91 true)))
|
|
241 |
(let (($x93 (and $x91 $x92)))
|
|
242 |
(let (($x88 (exists ((?v0 Int) )(let ((?x46 (v_b_array$ ?v0)))
|
|
243 |
(let (($x86 (= ?x46 v_b_max_G_4$)))
|
|
244 |
(let (($x43 (<= 0 ?v0)))
|
|
245 |
(let (($x85 (and $x43 (< ?v0 v_b_length$))))
|
|
246 |
(=> $x85 $x86))))))
|
|
247 |
))
|
|
248 |
(let (($x94 (=> $x88 $x93)))
|
|
249 |
(let (($x69 (<= v_b_length$ v_b_p_G_0$)))
|
|
250 |
(let (($x81 (and $x69 (and $x55 (and true (and $x71 (and $x73 (and $x75 true))))))))
|
|
251 |
(let (($x83 (and true (and $x55 $x81))))
|
|
252 |
(let (($x96 (=> $x83 (and $x88 $x94))))
|
|
253 |
(let (($x64 (and $x63 $x55)))
|
|
254 |
(let (($x61 (forall ((?v0 Int) )(let ((?x46 (v_b_array$ ?v0)))
|
|
255 |
(let (($x59 (<= ?x46 v_b_max_G_1$)))
|
|
256 |
(let (($x43 (<= 0 ?v0)))
|
|
257 |
(let (($x57 (and $x43 (< ?v0 v_b_p_G_0$))))
|
|
258 |
(=> $x57 $x59))))))
|
|
259 |
))
|
|
260 |
(let (($x67 (and true (and $x55 (and $x61 $x64)))))
|
|
261 |
(let (($x157 (=> (and $x50 $x67) (and $x96 $x155))))
|
|
262 |
(let (($x49 (forall ((?v0 Int) )(let ((?x46 (v_b_array$ ?v0)))
|
|
263 |
(let (($x47 (<= ?x46 v_b_max_G_0$)))
|
|
264 |
(let (($x43 (<= 0 ?v0)))
|
|
265 |
(let (($x45 (and $x43 (< ?v0 1))))
|
|
266 |
(=> $x45 $x47))))))
|
|
267 |
))
|
|
268 |
(let (($x159 (=> $x49 (and $x50 $x157))))
|
|
269 |
(let (($x32 (<= 0 0)))
|
|
270 |
(let (($x38 (and $x31 (and $x32 (and $x32 (and (<= 1 1) (<= 1 1)))))))
|
|
271 |
(let (($x39 (and true $x38)))
|
|
272 |
(let (($x28 (< 0 v_b_length$)))
|
|
273 |
(let (($x41 (and true (and $x28 $x39))))
|
|
274 |
(let (($x161 (=> $x41 (and $x49 $x159))))
|
|
275 |
(let (($x162 (not $x161)))
|
|
276 |
(let (($x362 (forall ((?v0 Int) )(let ((?x46 (v_b_array$ ?v0)))
|
|
277 |
(let (($x132 (<= ?x46 v_b_max_G_3$)))
|
|
278 |
(or (not (and (<= 0 ?v0) (< ?v0 v_b_p_G_1$))) $x132))))
|
|
279 |
))
|
|
280 |
(let (($x385 (or (not $x362) $x136)))
|
|
281 |
(let (($x390 (and $x362 $x385)))
|
|
282 |
(let (($x117 (and $x110 (<= 2 v_b_p_G_1$))))
|
|
283 |
(let (($x308 (= v_b_p_G_1$ (+ 1 v_b_p_G_0$))))
|
|
284 |
(let (($x313 (and $x308 $x117)))
|
|
285 |
(let (($x316 (and $x111 $x313)))
|
|
286 |
(let (($x402 (and $x145 $x316)))
|
|
287 |
(let (($x405 (and $x144 $x402)))
|
|
288 |
(let (($x415 (and $x55 $x405)))
|
|
289 |
(let (($x418 (and $x143 $x415)))
|
|
290 |
(let (($x421 (and $x55 $x418)))
|
|
291 |
(let (($x435 (or (not $x421) $x390)))
|
|
292 |
(let (($x326 (and $x109 $x316)))
|
|
293 |
(let (($x329 (and $x107 $x326)))
|
|
294 |
(let (($x339 (and $x54 $x329)))
|
|
295 |
(let (($x342 (and $x104 $x339)))
|
|
296 |
(let (($x345 (and $x102 $x342)))
|
|
297 |
(let (($x348 (and $x55 $x345)))
|
|
298 |
(let (($x397 (or (not $x348) $x390)))
|
|
299 |
(let (($x440 (and $x397 $x435)))
|
|
300 |
(let (($x447 (or (not (and $x55 (and (< v_b_p_G_0$ v_b_length$) $x55))) $x440)))
|
|
301 |
(let (($x263 (forall ((?v0 Int) )(let ((?x46 (v_b_array$ ?v0)))
|
|
302 |
(let (($x89 (<= ?x46 v_b_max_G_4$)))
|
|
303 |
(let (($x43 (<= 0 ?v0)))
|
|
304 |
(let (($x85 (and $x43 (< ?v0 v_b_length$))))
|
|
305 |
(let (($x253 (not $x85)))
|
|
306 |
(or $x253 $x89)))))))
|
|
307 |
))
|
|
308 |
(let (($x257 (exists ((?v0 Int) )(let ((?x46 (v_b_array$ ?v0)))
|
|
309 |
(let (($x86 (= ?x46 v_b_max_G_4$)))
|
|
310 |
(let (($x43 (<= 0 ?v0)))
|
|
311 |
(let (($x85 (and $x43 (< ?v0 v_b_length$))))
|
|
312 |
(let (($x253 (not $x85)))
|
|
313 |
(or $x253 $x86)))))))
|
|
314 |
))
|
|
315 |
(let (($x284 (or (not $x257) $x263)))
|
|
316 |
(let (($x289 (and $x257 $x284)))
|
|
317 |
(let (($x296 (or (not (and $x55 (and $x69 (and $x55 (and $x71 (and $x73 $x75)))))) $x289)))
|
|
318 |
(let (($x452 (and $x296 $x447)))
|
|
319 |
(let (($x203 (forall ((?v0 Int) )(let ((?x46 (v_b_array$ ?v0)))
|
|
320 |
(let (($x59 (<= ?x46 v_b_max_G_1$)))
|
|
321 |
(or (not (and (<= 0 ?v0) (< ?v0 v_b_p_G_0$))) $x59))))
|
|
322 |
))
|
|
323 |
(let (($x206 (and $x203 $x64)))
|
|
324 |
(let (($x209 (and $x55 $x206)))
|
|
325 |
(let (($x219 (and $x50 $x209)))
|
|
326 |
(let (($x459 (or (not $x219) $x452)))
|
|
327 |
(let (($x464 (and $x50 $x459)))
|
|
328 |
(let (($x196 (forall ((?v0 Int) )(let ((?x46 (v_b_array$ ?v0)))
|
|
329 |
(let (($x47 (<= ?x46 v_b_max_G_0$)))
|
|
330 |
(or (not (and (<= 0 ?v0) (< ?v0 1))) $x47))))
|
|
331 |
))
|
|
332 |
(let (($x471 (or (not $x196) $x464)))
|
|
333 |
(let (($x476 (and $x196 $x471)))
|
|
334 |
(let (($x483 (or (not (and $x28 (and $x31 (and $x32 (and $x32 (<= 1 1)))))) $x476)))
|
|
335 |
(let (($x746 (<= (+ (v_b_array$ ?0) ?x744) 0)))
|
|
336 |
(let (($x521 (>= ?0 0)))
|
|
337 |
(let (($x738 (and $x521 (not (>= (+ ?0 ?x685) 0)))))
|
|
338 |
(let (($x741 (not $x738)))
|
|
339 |
(let (($x749 (or $x741 $x746)))
|
|
340 |
(let ((?x46 (v_b_array$ ?0)))
|
|
341 |
(let (($x132 (<= ?x46 v_b_max_G_3$)))
|
|
342 |
(let (($x359 (or (not (and (<= 0 ?0) (< ?0 v_b_p_G_1$))) $x132)))
|
|
343 |
(let ((@x520 (rewrite (= (<= 0 ?0) $x521))))
|
|
344 |
(let ((@x740 (monotonicity @x520 (rewrite (= (< ?0 v_b_p_G_1$) (not (>= (+ ?0 ?x685) 0)))) (= (and (<= 0 ?0) (< ?0 v_b_p_G_1$)) $x738))))
|
|
345 |
(let ((@x743 (monotonicity @x740 (= (not (and (<= 0 ?0) (< ?0 v_b_p_G_1$))) $x741))))
|
|
346 |
(let ((@x754 (quant-intro (monotonicity @x743 (rewrite (= $x132 $x746)) (= $x359 $x749)) (= $x362 $x752))))
|
|
347 |
(let ((@x760 (monotonicity (monotonicity @x754 (= (not $x362) $x755)) (= $x385 $x758))))
|
|
348 |
(let (($x772 (and $x144 (and $x145 (and (and $x679 $x573) (and $x684 (and $x679 $x682)))))))
|
|
349 |
(let (($x576 (and $x571 $x573)))
|
|
350 |
(let (($x770 (= $x402 (and $x145 (and (and $x679 $x573) (and $x684 (and $x679 $x682)))))))
|
|
351 |
(let ((@x697 (monotonicity (rewrite (= $x110 $x679)) (rewrite (= (<= 2 v_b_p_G_1$) $x682)) (= $x117 (and $x679 $x682)))))
|
|
352 |
(let ((@x700 (monotonicity (rewrite (= $x308 $x684)) @x697 (= $x313 (and $x684 (and $x679 $x682))))))
|
|
353 |
(let ((@x575 (rewrite (= $x54 $x573))))
|
|
354 |
(let ((@x703 (monotonicity (rewrite (= $x110 $x679)) @x575 (= $x111 (and $x679 $x573)))))
|
|
355 |
(let ((@x706 (monotonicity @x703 @x700 (= $x316 (and (and $x679 $x573) (and $x684 (and $x679 $x682)))))))
|
|
356 |
(let ((@x578 (monotonicity (rewrite (= (<= 0 v_b_k_G_0$) $x571)) @x575 (= $x55 $x576))))
|
|
357 |
(let ((@x777 (monotonicity @x578 (monotonicity (monotonicity @x706 $x770) (= $x405 $x772)) (= $x415 (and $x576 $x772)))))
|
|
358 |
(let ((@x780 (monotonicity (rewrite (= $x143 $x689)) @x777 (= $x418 (and $x689 (and $x576 $x772))))))
|
|
359 |
(let ((@x783 (monotonicity @x578 @x780 (= $x421 (and $x576 (and $x689 (and $x576 $x772)))))))
|
|
360 |
(let ((@x788 (trans @x783 (rewrite (= (and $x576 (and $x689 (and $x576 $x772))) $x784)) (= $x421 $x784))))
|
|
361 |
(let ((@x794 (monotonicity (monotonicity @x788 (= (not $x421) $x789)) (monotonicity @x754 @x760 (= $x390 $x761)) (= $x435 $x792))))
|
|
362 |
(let (($x710 (and $x107 (and $x109 (and (and $x679 $x573) (and $x684 (and $x679 $x682)))))))
|
|
363 |
(let ((@x727 (rewrite (= (and $x576 (and $x692 (and $x104 (and $x573 $x710)))) $x725))))
|
|
364 |
(let (($x708 (= $x326 (and $x109 (and (and $x679 $x573) (and $x684 (and $x679 $x682)))))))
|
|
365 |
(let ((@x715 (monotonicity @x575 (monotonicity (monotonicity @x706 $x708) (= $x329 $x710)) (= $x339 (and $x573 $x710)))))
|
|
366 |
(let ((@x721 (monotonicity (rewrite (= $x102 $x692)) (monotonicity @x715 (= $x342 (and $x104 (and $x573 $x710)))) (= $x345 (and $x692 (and $x104 (and $x573 $x710)))))))
|
|
367 |
(let ((@x724 (monotonicity @x578 @x721 (= $x348 (and $x576 (and $x692 (and $x104 (and $x573 $x710))))))))
|
|
368 |
(let ((@x732 (monotonicity (trans @x724 @x727 (= $x348 $x725)) (= (not $x348) $x730))))
|
|
369 |
(let ((@x766 (monotonicity @x732 (monotonicity @x754 @x760 (= $x390 $x761)) (= $x397 $x764))))
|
|
370 |
(let (($x99 (and $x55 (and (< v_b_p_G_0$ v_b_length$) $x55))))
|
|
371 |
(let ((@x666 (monotonicity (rewrite (= (< v_b_p_G_0$ v_b_length$) $x661)) @x578 (= (and (< v_b_p_G_0$ v_b_length$) $x55) (and $x661 $x576)))))
|
|
372 |
(let ((@x674 (trans (monotonicity @x578 @x666 (= $x99 (and $x576 (and $x661 $x576)))) (rewrite (= (and $x576 (and $x661 $x576)) $x670)) (= $x99 $x670))))
|
|
373 |
(let ((@x800 (monotonicity (monotonicity @x674 (= (not $x99) $x675)) (monotonicity @x766 @x794 (= $x440 $x795)) (= $x447 $x798))))
|
|
374 |
(let (($x626 (and $x521 (not (<= (+ v_b_length$ (* (- 1) ?0)) 0)))))
|
|
375 |
(let (($x629 (not $x626)))
|
|
376 |
(let (($x89 (<= ?x46 v_b_max_G_4$)))
|
|
377 |
(let (($x43 (<= 0 ?0)))
|
|
378 |
(let (($x85 (and $x43 (< ?0 v_b_length$))))
|
|
379 |
(let (($x253 (not $x85)))
|
|
380 |
(let (($x260 (or $x253 $x89)))
|
|
381 |
(let (($x624 (= (< ?0 v_b_length$) (not (<= (+ v_b_length$ (* (- 1) ?0)) 0)))))
|
|
382 |
(let ((@x631 (monotonicity (monotonicity @x520 (rewrite $x624) (= $x85 $x626)) (= $x253 $x629))))
|
|
383 |
(let ((@x648 (monotonicity @x631 (rewrite (= $x89 (<= (+ ?x46 (* (- 1) v_b_max_G_4$)) 0))) (= $x260 (or $x629 (<= (+ ?x46 (* (- 1) v_b_max_G_4$)) 0))))))
|
|
384 |
(let (($x86 (= ?x46 v_b_max_G_4$)))
|
|
385 |
(let (($x632 (or $x629 $x86)))
|
|
386 |
(let (($x254 (or $x253 $x86)))
|
|
387 |
(let ((@x640 (monotonicity (quant-intro (monotonicity @x631 (= $x254 $x632)) (= $x257 $x635)) (= (not $x257) $x638))))
|
|
388 |
(let ((@x657 (monotonicity (quant-intro (monotonicity @x631 (= $x254 $x632)) (= $x257 $x635)) (monotonicity @x640 (quant-intro @x648 (= $x263 $x649)) (= $x284 $x652)) (= $x289 $x655))))
|
|
389 |
(let (($x618 (= (not (and $x55 (and $x69 (and $x55 (and $x71 (and $x73 $x75)))))) $x617)))
|
|
390 |
(let (($x227 (and $x71 (and $x73 $x75))))
|
|
391 |
(let (($x237 (and $x55 $x227)))
|
|
392 |
(let (($x240 (and $x69 $x237)))
|
|
393 |
(let (($x243 (and $x55 $x240)))
|
|
394 |
(let ((@x608 (monotonicity (rewrite (= $x69 $x600)) (monotonicity @x578 (= $x237 (and $x576 $x227))) (= $x240 (and $x600 (and $x576 $x227))))))
|
|
395 |
(let ((@x611 (monotonicity @x578 @x608 (= $x243 (and $x576 (and $x600 (and $x576 $x227)))))))
|
|
396 |
(let ((@x616 (trans @x611 (rewrite (= (and $x576 (and $x600 (and $x576 $x227))) $x612)) (= $x243 $x612))))
|
|
397 |
(let ((@x803 (monotonicity (monotonicity (monotonicity @x616 $x618) @x657 (= $x296 $x658)) @x800 (= $x452 $x801))))
|
|
398 |
(let ((@x593 (rewrite (= (and $x50 (and $x576 (and $x567 (and $x63 $x576)))) $x591))))
|
|
399 |
(let (($x561 (<= (+ ?x46 (* (- 1) v_b_max_G_1$)) 0)))
|
|
400 |
(let (($x553 (and $x521 (not (>= (+ ?0 ?x549) 0)))))
|
|
401 |
(let (($x556 (not $x553)))
|
|
402 |
(let (($x564 (or $x556 $x561)))
|
|
403 |
(let (($x59 (<= ?x46 v_b_max_G_1$)))
|
|
404 |
(let (($x200 (or (not (and $x43 (< ?0 v_b_p_G_0$))) $x59)))
|
|
405 |
(let ((@x555 (monotonicity @x520 (rewrite (= (< ?0 v_b_p_G_0$) (not (>= (+ ?0 ?x549) 0)))) (= (and $x43 (< ?0 v_b_p_G_0$)) $x553))))
|
|
406 |
(let ((@x566 (monotonicity (monotonicity @x555 (= (not (and $x43 (< ?0 v_b_p_G_0$))) $x556)) (rewrite (= $x59 $x561)) (= $x200 $x564))))
|
|
407 |
(let ((@x584 (monotonicity (quant-intro @x566 (= $x203 $x567)) (monotonicity @x578 (= $x64 (and $x63 $x576))) (= $x206 (and $x567 (and $x63 $x576))))))
|
|
408 |
(let ((@x587 (monotonicity @x578 @x584 (= $x209 (and $x576 (and $x567 (and $x63 $x576)))))))
|
|
409 |
(let ((@x590 (monotonicity @x587 (= $x219 (and $x50 (and $x576 (and $x567 (and $x63 $x576))))))))
|
|
410 |
(let ((@x598 (monotonicity (trans @x590 @x593 (= $x219 $x591)) (= (not $x219) $x596))))
|
|
411 |
(let ((@x809 (monotonicity (monotonicity @x598 @x803 (= $x459 $x804)) (= $x464 $x807))))
|
|
412 |
(let (($x534 (>= (+ v_b_max_G_0$ (* (- 1) ?x46)) 0)))
|
|
413 |
(let (($x526 (and $x521 (not (>= ?0 1)))))
|
|
414 |
(let (($x529 (not $x526)))
|
|
415 |
(let (($x538 (or $x529 $x534)))
|
|
416 |
(let (($x47 (<= ?x46 v_b_max_G_0$)))
|
|
417 |
(let (($x193 (or (not (and $x43 (< ?0 1))) $x47)))
|
|
418 |
(let ((@x528 (monotonicity @x520 (rewrite (= (< ?0 1) (not (>= ?0 1)))) (= (and $x43 (< ?0 1)) $x526))))
|
|
419 |
(let ((@x540 (monotonicity (monotonicity @x528 (= (not (and $x43 (< ?0 1))) $x529)) (rewrite (= $x47 $x534)) (= $x193 $x538))))
|
|
420 |
(let ((@x546 (monotonicity (quant-intro @x540 (= $x196 $x541)) (= (not $x196) $x544))))
|
|
421 |
(let ((@x815 (monotonicity (quant-intro @x540 (= $x196 $x541)) (monotonicity @x546 @x809 (= $x471 $x810)) (= $x476 $x813))))
|
|
422 |
(let (($x517 (= (not (and $x28 (and $x31 (and $x32 (and $x32 (<= 1 1)))))) (not $x511))))
|
|
423 |
(let (($x34 (<= 1 1)))
|
|
424 |
(let (($x166 (and $x32 $x34)))
|
|
425 |
(let (($x169 (and $x32 $x166)))
|
|
426 |
(let (($x172 (and $x31 $x169)))
|
|
427 |
(let (($x182 (and $x28 $x172)))
|
|
428 |
(let ((@x513 (rewrite (= (and $x496 (and $x31 (and true (and true true)))) $x511))))
|
|
429 |
(let ((@x501 (monotonicity (rewrite (= $x32 true)) (rewrite (= $x34 true)) (= $x166 (and true true)))))
|
|
430 |
(let ((@x504 (monotonicity (rewrite (= $x32 true)) @x501 (= $x169 (and true (and true true))))))
|
|
431 |
(let ((@x507 (monotonicity @x504 (= $x172 (and $x31 (and true (and true true)))))))
|
|
432 |
(let ((@x510 (monotonicity (rewrite (= $x28 $x496)) @x507 (= $x182 (and $x496 (and $x31 (and true (and true true))))))))
|
|
433 |
(let ((@x818 (monotonicity (monotonicity (trans @x510 @x513 (= $x182 $x511)) $x517) @x815 (= $x483 (or (not $x511) $x813)))))
|
|
434 |
(let ((@x369 (monotonicity (rewrite (= (and $x136 false) false)) (= $x138 (=> false true)))))
|
|
435 |
(let ((@x373 (trans @x369 (rewrite (= (=> false true) true)) (= $x138 true))))
|
|
436 |
(let ((@x380 (trans (monotonicity @x373 (= $x139 (and $x136 true))) (rewrite (= (and $x136 true) $x136)) (= $x139 $x136))))
|
|
437 |
(let ((@x364 (quant-intro (rewrite (= (=> (and $x43 (< ?0 v_b_p_G_1$)) $x132) $x359)) (= $x134 $x362))))
|
|
438 |
(let ((@x389 (trans (monotonicity @x364 @x380 (= $x140 (=> $x362 $x136))) (rewrite (= (=> $x362 $x136) $x385)) (= $x140 $x385))))
|
|
439 |
(let ((@x310 (monotonicity (rewrite (= (+ v_b_p_G_0$ 1) (+ 1 v_b_p_G_0$))) (= (= v_b_p_G_1$ (+ v_b_p_G_0$ 1)) $x308))))
|
|
440 |
(let ((@x315 (monotonicity @x310 (rewrite (= (and $x117 true) $x117)) (= $x119 $x313))))
|
|
441 |
(let ((@x321 (monotonicity (monotonicity @x315 (= (and $x111 $x119) $x316)) (= $x121 (and true $x316)))))
|
|
442 |
(let ((@x404 (monotonicity (trans @x321 (rewrite (= (and true $x316) $x316)) (= $x121 $x316)) (= (and $x145 $x121) $x402))))
|
|
443 |
(let ((@x410 (monotonicity (monotonicity @x404 (= (and $x144 (and $x145 $x121)) $x405)) (= $x148 (and true $x405)))))
|
|
444 |
(let ((@x417 (monotonicity (trans @x410 (rewrite (= (and true $x405) $x405)) (= $x148 $x405)) (= (and $x55 $x148) $x415))))
|
|
445 |
(let ((@x423 (monotonicity (monotonicity @x417 (= (and $x143 (and $x55 $x148)) $x418)) (= (and $x55 (and $x143 (and $x55 $x148))) $x421))))
|
|
446 |
(let ((@x430 (trans (monotonicity @x423 (= $x152 (and true $x421))) (rewrite (= (and true $x421) $x421)) (= $x152 $x421))))
|
|
447 |
(let ((@x433 (monotonicity @x430 (monotonicity @x364 @x389 (= $x141 $x390)) (= $x153 (=> $x421 $x390)))))
|
|
448 |
(let (($x340 (= (and (and $x54 $x54) (and true (and $x107 (and $x109 $x121)))) $x339)))
|
|
449 |
(let ((@x328 (monotonicity (trans @x321 (rewrite (= (and true $x316) $x316)) (= $x121 $x316)) (= (and $x109 $x121) $x326))))
|
|
450 |
(let ((@x334 (monotonicity (monotonicity @x328 (= (and $x107 (and $x109 $x121)) $x329)) (= (and true (and $x107 (and $x109 $x121))) (and true $x329)))))
|
|
451 |
(let ((@x338 (trans @x334 (rewrite (= (and true $x329) $x329)) (= (and true (and $x107 (and $x109 $x121))) $x329))))
|
|
452 |
(let ((@x344 (monotonicity (monotonicity (rewrite (= (and $x54 $x54) $x54)) @x338 $x340) (= $x126 $x342))))
|
|
453 |
(let ((@x350 (monotonicity (monotonicity @x344 (= (and $x102 $x126) $x345)) (= (and $x55 (and $x102 $x126)) $x348))))
|
|
454 |
(let ((@x357 (trans (monotonicity @x350 (= $x129 (and true $x348))) (rewrite (= (and true $x348) $x348)) (= $x129 $x348))))
|
|
455 |
(let ((@x395 (monotonicity @x357 (monotonicity @x364 @x389 (= $x141 $x390)) (= $x142 (=> $x348 $x390)))))
|
|
456 |
(let ((@x442 (monotonicity (trans @x395 (rewrite (= (=> $x348 $x390) $x397)) (= $x142 $x397)) (trans @x433 (rewrite (= (=> $x421 $x390) $x435)) (= $x153 $x435)) (= (and $x142 $x153) $x440))))
|
|
457 |
(let ((@x445 (monotonicity (rewrite (= (and true $x99) $x99)) @x442 (= $x155 (=> $x99 $x440)))))
|
|
458 |
(let ((@x268 (monotonicity (quant-intro (rewrite (= (=> $x85 $x89) $x260)) (= $x91 $x263)) (= $x92 (=> $x263 true)))))
|
|
459 |
(let ((@x272 (trans @x268 (rewrite (= (=> $x263 true) true)) (= $x92 true))))
|
|
460 |
(let ((@x275 (monotonicity (quant-intro (rewrite (= (=> $x85 $x89) $x260)) (= $x91 $x263)) @x272 (= $x93 (and $x263 true)))))
|
|
461 |
(let ((@x282 (monotonicity (quant-intro (rewrite (= (=> $x85 $x86) $x254)) (= $x88 $x257)) (trans @x275 (rewrite (= (and $x263 true) $x263)) (= $x93 $x263)) (= $x94 (=> $x257 $x263)))))
|
|
462 |
(let ((@x291 (monotonicity (quant-intro (rewrite (= (=> $x85 $x86) $x254)) (= $x88 $x257)) (trans @x282 (rewrite (= (=> $x257 $x263) $x284)) (= $x94 $x284)) (= (and $x88 $x94) $x289))))
|
|
463 |
(let (($x238 (= (and $x55 (and true (and $x71 (and $x73 (and $x75 true))))) $x237)))
|
|
464 |
(let (($x79 (and true (and $x71 (and $x73 (and $x75 true))))))
|
|
465 |
(let ((@x226 (monotonicity (rewrite (= (and $x75 true) $x75)) (= (and $x73 (and $x75 true)) (and $x73 $x75)))))
|
|
466 |
(let ((@x229 (monotonicity @x226 (= (and $x71 (and $x73 (and $x75 true))) $x227))))
|
|
467 |
(let ((@x236 (trans (monotonicity @x229 (= $x79 (and true $x227))) (rewrite (= (and true $x227) $x227)) (= $x79 $x227))))
|
|
468 |
(let ((@x245 (monotonicity (monotonicity (monotonicity @x236 $x238) (= $x81 $x240)) (= (and $x55 $x81) $x243))))
|
|
469 |
(let ((@x252 (trans (monotonicity @x245 (= $x83 (and true $x243))) (rewrite (= (and true $x243) $x243)) (= $x83 $x243))))
|
|
470 |
(let ((@x300 (trans (monotonicity @x252 @x291 (= $x96 (=> $x243 $x289))) (rewrite (= (=> $x243 $x289) $x296)) (= $x96 $x296))))
|
|
471 |
(let ((@x454 (monotonicity @x300 (trans @x445 (rewrite (= (=> $x99 $x440) $x447)) (= $x155 $x447)) (= (and $x96 $x155) $x452))))
|
|
472 |
(let ((@x205 (quant-intro (rewrite (= (=> (and $x43 (< ?0 v_b_p_G_0$)) $x59) $x200)) (= $x61 $x203))))
|
|
473 |
(let ((@x211 (monotonicity (monotonicity @x205 (= (and $x61 $x64) $x206)) (= (and $x55 (and $x61 $x64)) $x209))))
|
|
474 |
(let ((@x218 (trans (monotonicity @x211 (= $x67 (and true $x209))) (rewrite (= (and true $x209) $x209)) (= $x67 $x209))))
|
|
475 |
(let ((@x457 (monotonicity (monotonicity @x218 (= (and $x50 $x67) $x219)) @x454 (= $x157 (=> $x219 $x452)))))
|
|
476 |
(let ((@x466 (monotonicity (trans @x457 (rewrite (= (=> $x219 $x452) $x459)) (= $x157 $x459)) (= (and $x50 $x157) $x464))))
|
|
477 |
(let ((@x198 (quant-intro (rewrite (= (=> (and $x43 (< ?0 1)) $x47) $x193)) (= $x49 $x196))))
|
|
478 |
(let ((@x475 (trans (monotonicity @x198 @x466 (= $x159 (=> $x196 $x464))) (rewrite (= (=> $x196 $x464) $x471)) (= $x159 $x471))))
|
|
479 |
(let ((@x168 (monotonicity (rewrite (= (and $x34 $x34) $x34)) (= (and $x32 (and $x34 $x34)) $x166))))
|
|
480 |
(let ((@x174 (monotonicity (monotonicity @x168 (= (and $x32 (and $x32 (and $x34 $x34))) $x169)) (= $x38 $x172))))
|
|
481 |
(let ((@x181 (trans (monotonicity @x174 (= $x39 (and true $x172))) (rewrite (= (and true $x172) $x172)) (= $x39 $x172))))
|
|
482 |
(let ((@x187 (monotonicity (monotonicity @x181 (= (and $x28 $x39) $x182)) (= $x41 (and true $x182)))))
|
|
483 |
(let ((@x481 (monotonicity (trans @x187 (rewrite (= (and true $x182) $x182)) (= $x41 $x182)) (monotonicity @x198 @x475 (= (and $x49 $x159) $x476)) (= $x161 (=> $x182 $x476)))))
|
|
484 |
(let ((@x490 (monotonicity (trans @x481 (rewrite (= (=> $x182 $x476) $x483)) (= $x161 $x483)) (= $x162 (not $x483)))))
|
|
485 |
(let ((@x823 (trans @x490 (monotonicity @x818 (= (not $x483) $x819)) (= $x162 $x819))))
|
|
486 |
(let ((@x827 (and-elim (not-or-elim (mp (asserted $x162) @x823 $x819) $x511) $x31)))
|
|
487 |
(let ((@x1690 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not (= v_b_max_G_0$ (v_b_array$ ?v0!0))) $x839)) (unit-resolution (def-axiom (or $x1149 (not $x839))) @x1726 (not $x839)) (trans @x827 @x1715 (= v_b_max_G_0$ (v_b_array$ ?v0!0))) false)))
|
|
488 |
(let (($x1946 (or $x1154 $x1943)))
|
|
489 |
(let (($x1340 (forall ((?v0 Int) )(let (($x746 (<= (+ (v_b_array$ ?v0) (* (- 1) v_b_max_G_3$)) 0)))
|
|
490 |
(let (($x733 (>= (+ ?v0 (* (- 1) v_b_p_G_1$)) 0)))
|
|
491 |
(let (($x521 (>= ?v0 0)))
|
|
492 |
(let (($x1157 (not $x521)))
|
|
493 |
(or $x1157 $x733 $x746))))))
|
|
494 |
))
|
|
495 |
(let (($x1348 (not (or (not $x1340) $x136))))
|
|
496 |
(let (($x1353 (or $x1318 $x1348)))
|
|
497 |
(let (($x1365 (not $x1353)))
|
|
498 |
(let (($x1378 (not (or $x692 $x1286 $x1375 $x1376 $x1287 $x1362 $x1363 $x1364 $x1365))))
|
|
499 |
(let (($x1367 (not (or $x1286 $x689 $x1359 $x1360 $x1361 $x1287 $x1362 $x1363 $x1364 $x1365))))
|
|
500 |
(let (($x1383 (or $x1367 $x1378)))
|
|
501 |
(let (($x1391 (not (or $x600 $x1286 $x1287 (not $x1383)))))
|
|
502 |
(let (($x1224 (forall ((?v0 Int) )(let ((?x46 (v_b_array$ ?v0)))
|
|
503 |
(let (($x86 (= ?x46 v_b_max_G_4$)))
|
|
504 |
(let (($x622 (<= (+ v_b_length$ (* (- 1) ?v0)) 0)))
|
|
505 |
(let (($x521 (>= ?v0 0)))
|
|
506 |
(let (($x1157 (not $x521)))
|
|
507 |
(let (($x1216 (or $x1157 $x622 $x86)))
|
|
508 |
(not $x1216))))))))
|
|
509 |
))
|
|
510 |
(let (($x1280 (or $x1224 $x1275)))
|
|
511 |
(let (($x1293 (not (or $x661 $x1286 $x1287 $x1288 $x1289 $x1290 (not $x1280)))))
|
|
512 |
(let (($x1396 (or $x1293 $x1391)))
|
|
513 |
(let (($x1199 (forall ((?v0 Int) )(let (($x561 (<= (+ (v_b_array$ ?v0) (* (- 1) v_b_max_G_1$)) 0)))
|
|
514 |
(let (($x548 (>= (+ ?v0 (* (- 1) v_b_p_G_0$)) 0)))
|
|
515 |
(let (($x521 (>= ?v0 0)))
|
|
516 |
(let (($x1157 (not $x521)))
|
|
517 |
(or $x1157 $x548 $x561))))))
|
|
518 |
))
|
|
519 |
(let (($x1406 (not (or $x851 (not $x1199) $x1403 $x1286 $x1287 (not $x1396)))))
|
|
520 |
(let (($x1411 (or $x851 $x1406)))
|
|
521 |
(let (($x1177 (forall ((?v0 Int) )(let (($x534 (>= (+ v_b_max_G_0$ (* (- 1) (v_b_array$ ?v0))) 0)))
|
|
522 |
(let (($x524 (>= ?v0 1)))
|
|
523 |
(let (($x521 (>= ?v0 0)))
|
|
524 |
(let (($x1157 (not $x521)))
|
|
525 |
(or $x1157 $x524 $x534))))))
|
|
526 |
))
|
|
527 |
(let (($x1420 (not (or (not $x1177) (not $x1411)))))
|
|
528 |
(let (($x1425 (or $x1154 $x1420)))
|
|
529 |
(let (($x733 (>= (+ ?0 ?x685) 0)))
|
|
530 |
(let (($x1157 (not $x521)))
|
|
531 |
(let (($x1335 (or $x1157 $x733 $x746)))
|
|
532 |
(let ((@x1885 (monotonicity (quant-intro (refl (= $x1335 $x1335)) (= $x1340 $x1878)) (= (not $x1340) $x1883))))
|
|
533 |
(let ((@x1891 (monotonicity (monotonicity @x1885 (= (or (not $x1340) $x136) $x1886)) (= $x1348 $x1889))))
|
|
534 |
(let ((@x1906 (monotonicity (monotonicity (monotonicity @x1891 (= $x1353 $x1892)) (= $x1365 $x1895)) (= (or $x692 $x1286 $x1375 $x1376 $x1287 $x1362 $x1363 $x1364 $x1365) $x1904))))
|
|
535 |
(let ((@x1900 (monotonicity (monotonicity (monotonicity @x1891 (= $x1353 $x1892)) (= $x1365 $x1895)) (= (or $x1286 $x689 $x1359 $x1360 $x1361 $x1287 $x1362 $x1363 $x1364 $x1365) $x1898))))
|
|
536 |
(let ((@x1912 (monotonicity (monotonicity @x1900 (= $x1367 $x1901)) (monotonicity @x1906 (= $x1378 $x1907)) (= $x1383 $x1910))))
|
|
537 |
(let ((@x1918 (monotonicity (monotonicity @x1912 (= (not $x1383) $x1913)) (= (or $x600 $x1286 $x1287 (not $x1383)) $x1916))))
|
|
538 |
(let (($x622 (<= (+ v_b_length$ (* (- 1) ?0)) 0)))
|
|
539 |
(let (($x1216 (or $x1157 $x622 $x86)))
|
|
540 |
(let (($x1221 (not $x1216)))
|
|
541 |
(let ((@x1868 (monotonicity (quant-intro (refl (= $x1221 $x1221)) (= $x1224 $x1861)) (= $x1280 $x1866))))
|
|
542 |
(let ((@x1874 (monotonicity (monotonicity @x1868 (= (not $x1280) $x1869)) (= (or $x661 $x1286 $x1287 $x1288 $x1289 $x1290 (not $x1280)) $x1872))))
|
|
543 |
(let ((@x1924 (monotonicity (monotonicity @x1874 (= $x1293 $x1875)) (monotonicity @x1918 (= $x1391 $x1919)) (= $x1396 $x1922))))
|
|
544 |
(let (($x548 (>= (+ ?0 ?x549) 0)))
|
|
545 |
(let (($x1194 (or $x1157 $x548 $x561)))
|
|
546 |
(let ((@x1860 (monotonicity (quant-intro (refl (= $x1194 $x1194)) (= $x1199 $x1853)) (= (not $x1199) $x1858))))
|
|
547 |
(let ((@x1930 (monotonicity @x1860 (monotonicity @x1924 (= (not $x1396) $x1925)) (= (or $x851 (not $x1199) $x1403 $x1286 $x1287 (not $x1396)) $x1928))))
|
|
548 |
(let ((@x1939 (monotonicity (monotonicity (monotonicity @x1930 (= $x1406 $x1931)) (= $x1411 $x1934)) (= (not $x1411) $x1937))))
|
|
549 |
(let ((@x1847 (refl (= (or $x1157 (>= ?0 1) $x534) (or $x1157 (>= ?0 1) $x534)))))
|
|
550 |
(let ((@x1852 (monotonicity (quant-intro @x1847 (= $x1177 $x1845)) (= (not $x1177) $x1850))))
|
|
551 |
(let ((@x1945 (monotonicity (monotonicity @x1852 @x1939 (= (or (not $x1177) (not $x1411)) $x1940)) (= $x1420 $x1943))))
|
|
552 |
(let (($x951 (not $x136)))
|
|
553 |
(let (($x954 (and $x752 $x951)))
|
|
554 |
(let (($x1053 (not $x1048)))
|
|
555 |
(let (($x1056 (and $x931 $x1053)))
|
|
556 |
(let (($x1059 (not $x1056)))
|
|
557 |
(let (($x1075 (or $x1059 $x1070)))
|
|
558 |
(let (($x1078 (not $x1075)))
|
|
559 |
(let (($x1081 (or $x1078 $x954)))
|
|
560 |
(let (($x1097 (and $x689 $x571 $x144 $x145 $x573 $x684 $x679 $x682 $x1081)))
|
|
561 |
(let (($x1087 (and $x571 $x692 $x104 $x107 $x109 $x573 $x684 $x679 $x682 $x1081)))
|
|
562 |
(let (($x1102 (or $x1087 $x1097)))
|
|
563 |
(let (($x1108 (and $x661 $x571 $x573 $x1102)))
|
|
564 |
(let (($x903 (not (and $x897 (not $x900)))))
|
|
565 |
(let (($x1016 (or $x903 $x1011)))
|
|
566 |
(let (($x1019 (not $x1016)))
|
|
567 |
(let (($x887 (not (and $x881 (not $x884)))))
|
|
568 |
(let (($x890 (or $x887 $x889)))
|
|
569 |
(let (($x1022 (and $x890 $x1019)))
|
|
570 |
(let (($x877 (forall ((?v0 Int) )(let ((?x46 (v_b_array$ ?v0)))
|
|
571 |
(let (($x86 (= ?x46 v_b_max_G_4$)))
|
|
572 |
(let (($x521 (>= ?v0 0)))
|
|
573 |
(let (($x626 (and $x521 (not (<= (+ v_b_length$ (* (- 1) ?v0)) 0)))))
|
|
574 |
(let (($x629 (not $x626)))
|
|
575 |
(let (($x632 (or $x629 $x86)))
|
|
576 |
(not $x632))))))))
|
|
577 |
))
|
|
578 |
(let (($x1025 (or $x877 $x1022)))
|
|
579 |
(let (($x1031 (and $x600 $x571 $x573 $x71 $x73 $x75 $x1025)))
|
|
580 |
(let (($x1113 (or $x1031 $x1108)))
|
|
581 |
(let (($x1119 (and $x50 $x567 $x63 $x571 $x573 $x1113)))
|
|
582 |
(let (($x1124 (or $x851 $x1119)))
|
|
583 |
(let (($x1127 (and $x541 $x1124)))
|
|
584 |
(let (($x831 (not (and $x835 $x833))))
|
|
585 |
(let (($x840 (or $x831 $x839)))
|
|
586 |
(let (($x841 (not $x840)))
|
|
587 |
(let (($x1130 (or $x841 $x1127)))
|
|
588 |
(let ((@x1380 (rewrite (= (and $x689 $x571 $x144 $x145 $x573 $x684 $x679 $x682 $x1353) $x1378))))
|
|
589 |
(let ((@x1327 (monotonicity (rewrite (= $x738 (not (or $x1157 $x733)))) (= $x741 (not (not (or $x1157 $x733)))))))
|
|
590 |
(let ((@x1331 (trans @x1327 (rewrite (= (not (not (or $x1157 $x733))) (or $x1157 $x733))) (= $x741 (or $x1157 $x733)))))
|
|
591 |
(let ((@x1339 (trans (monotonicity @x1331 (= $x749 (or (or $x1157 $x733) $x746))) (rewrite (= (or (or $x1157 $x733) $x746) $x1335)) (= $x749 $x1335))))
|
|
592 |
(let ((@x1345 (monotonicity (quant-intro @x1339 (= $x752 $x1340)) (= $x954 (and $x1340 $x951)))))
|
|
593 |
(let ((@x1305 (monotonicity (rewrite (= $x1056 (not (or $x1298 $x1048)))) (= $x1059 (not (not (or $x1298 $x1048)))))))
|
|
594 |
(let ((@x1309 (trans @x1305 (rewrite (= (not (not (or $x1298 $x1048))) (or $x1298 $x1048))) (= $x1059 (or $x1298 $x1048)))))
|
|
595 |
(let ((@x1317 (trans (monotonicity @x1309 (= $x1075 (or (or $x1298 $x1048) $x1070))) (rewrite (= (or (or $x1298 $x1048) $x1070) $x1313)) (= $x1075 $x1313))))
|
|
596 |
(let ((@x1355 (monotonicity (monotonicity @x1317 (= $x1078 $x1318)) (trans @x1345 (rewrite (= (and $x1340 $x951) $x1348)) (= $x954 $x1348)) (= $x1081 $x1353))))
|
|
597 |
(let ((@x1374 (monotonicity @x1355 (= $x1097 (and $x689 $x571 $x144 $x145 $x573 $x684 $x679 $x682 $x1353)))))
|
|
598 |
(let ((@x1369 (rewrite (= (and $x571 $x692 $x104 $x107 $x109 $x573 $x684 $x679 $x682 $x1353) $x1367))))
|
|
599 |
(let ((@x1358 (monotonicity @x1355 (= $x1087 (and $x571 $x692 $x104 $x107 $x109 $x573 $x684 $x679 $x682 $x1353)))))
|
|
600 |
(let ((@x1385 (monotonicity (trans @x1358 @x1369 (= $x1087 $x1367)) (trans @x1374 @x1380 (= $x1097 $x1378)) (= $x1102 $x1383))))
|
|
601 |
(let ((@x1395 (trans (monotonicity @x1385 (= $x1108 (and $x661 $x571 $x573 $x1383))) (rewrite (= (and $x661 $x571 $x573 $x1383) $x1391)) (= $x1108 $x1391))))
|
|
602 |
(let ((@x1254 (monotonicity (rewrite (= (and $x897 (not $x900)) (not (or $x1247 $x900)))) (= $x903 (not (not (or $x1247 $x900)))))))
|
|
603 |
(let ((@x1258 (trans @x1254 (rewrite (= (not (not (or $x1247 $x900))) (or $x1247 $x900))) (= $x903 (or $x1247 $x900)))))
|
|
604 |
(let ((@x1266 (trans (monotonicity @x1258 (= $x1016 (or (or $x1247 $x900) $x1011))) (rewrite (= (or (or $x1247 $x900) $x1011) (or $x1247 $x900 $x1011))) (= $x1016 (or $x1247 $x900 $x1011)))))
|
|
605 |
(let ((@x1234 (monotonicity (rewrite (= (and $x881 (not $x884)) (not (or $x1227 $x884)))) (= $x887 (not (not (or $x1227 $x884)))))))
|
|
606 |
(let ((@x1238 (trans @x1234 (rewrite (= (not (not (or $x1227 $x884))) (or $x1227 $x884))) (= $x887 (or $x1227 $x884)))))
|
|
607 |
(let ((@x1246 (trans (monotonicity @x1238 (= $x890 (or (or $x1227 $x884) $x889))) (rewrite (= (or (or $x1227 $x884) $x889) $x1242)) (= $x890 $x1242))))
|
|
608 |
(let ((@x1272 (monotonicity @x1246 (monotonicity @x1266 (= $x1019 (not (or $x1247 $x900 $x1011)))) (= $x1022 (and $x1242 (not (or $x1247 $x900 $x1011)))))))
|
|
609 |
(let ((@x1279 (trans @x1272 (rewrite (= (and $x1242 (not (or $x1247 $x900 $x1011))) $x1275)) (= $x1022 $x1275))))
|
|
610 |
(let ((@x1208 (monotonicity (rewrite (= $x626 (not (or $x1157 $x622)))) (= $x629 (not (not (or $x1157 $x622)))))))
|
|
611 |
(let ((@x1212 (trans @x1208 (rewrite (= (not (not (or $x1157 $x622))) (or $x1157 $x622))) (= $x629 (or $x1157 $x622)))))
|
|
612 |
(let ((@x1220 (trans (monotonicity @x1212 (= $x632 (or (or $x1157 $x622) $x86))) (rewrite (= (or (or $x1157 $x622) $x86) $x1216)) (= $x632 $x1216))))
|
|
613 |
(let ((@x1226 (quant-intro (monotonicity @x1220 (= (not $x632) $x1221)) (= $x877 $x1224))))
|
|
614 |
(let ((@x1285 (monotonicity (monotonicity @x1226 @x1279 (= $x1025 $x1280)) (= $x1031 (and $x600 $x571 $x573 $x71 $x73 $x75 $x1280)))))
|
|
615 |
(let ((@x1297 (trans @x1285 (rewrite (= (and $x600 $x571 $x573 $x71 $x73 $x75 $x1280) $x1293)) (= $x1031 $x1293))))
|
|
616 |
(let ((@x1186 (monotonicity (rewrite (= $x553 (not (or $x1157 $x548)))) (= $x556 (not (not (or $x1157 $x548)))))))
|
|
617 |
(let ((@x1190 (trans @x1186 (rewrite (= (not (not (or $x1157 $x548))) (or $x1157 $x548))) (= $x556 (or $x1157 $x548)))))
|
|
618 |
(let ((@x1198 (trans (monotonicity @x1190 (= $x564 (or (or $x1157 $x548) $x561))) (rewrite (= (or (or $x1157 $x548) $x561) $x1194)) (= $x564 $x1194))))
|
|
619 |
(let ((@x1401 (monotonicity (quant-intro @x1198 (= $x567 $x1199)) (monotonicity @x1297 @x1395 (= $x1113 $x1396)) (= $x1119 (and $x50 $x1199 $x63 $x571 $x573 $x1396)))))
|
|
620 |
(let ((@x1410 (trans @x1401 (rewrite (= (and $x50 $x1199 $x63 $x571 $x573 $x1396) $x1406)) (= $x1119 $x1406))))
|
|
621 |
(let (($x524 (>= ?0 1)))
|
|
622 |
(let (($x1172 (or $x1157 $x524 $x534)))
|
|
623 |
(let ((@x1164 (monotonicity (rewrite (= $x526 (not (or $x1157 $x524)))) (= $x529 (not (not (or $x1157 $x524)))))))
|
|
624 |
(let ((@x1168 (trans @x1164 (rewrite (= (not (not (or $x1157 $x524))) (or $x1157 $x524))) (= $x529 (or $x1157 $x524)))))
|
|
625 |
(let ((@x1176 (trans (monotonicity @x1168 (= $x538 (or (or $x1157 $x524) $x534))) (rewrite (= (or (or $x1157 $x524) $x534) $x1172)) (= $x538 $x1172))))
|
|
626 |
(let ((@x1416 (monotonicity (quant-intro @x1176 (= $x541 $x1177)) (monotonicity @x1410 (= $x1124 $x1411)) (= $x1127 (and $x1177 $x1411)))))
|
|
627 |
(let ((@x1141 (monotonicity (rewrite (= (and $x835 $x833) (not (or $x1134 $x832)))) (= $x831 (not (not (or $x1134 $x832)))))))
|
|
628 |
(let ((@x1145 (trans @x1141 (rewrite (= (not (not (or $x1134 $x832))) (or $x1134 $x832))) (= $x831 (or $x1134 $x832)))))
|
|
629 |
(let ((@x1153 (trans (monotonicity @x1145 (= $x840 (or (or $x1134 $x832) $x839))) (rewrite (= (or (or $x1134 $x832) $x839) $x1149)) (= $x840 $x1149))))
|
|
630 |
(let ((@x1427 (monotonicity (monotonicity @x1153 (= $x841 $x1154)) (trans @x1416 (rewrite (= (and $x1177 $x1411) $x1420)) (= $x1127 $x1420)) (= $x1130 $x1425))))
|
|
631 |
(let (($x939 (<= (+ ?x937 ?x744) 0)))
|
|
632 |
(let (($x941 (not (or (not (and $x931 (not (>= (+ ?v0!3 ?x685) 0)))) $x939))))
|
|
633 |
(let (($x958 (or $x941 $x954)))
|
|
634 |
(let (($x966 (not $x789)))
|
|
635 |
(let (($x969 (and $x966 $x958)))
|
|
636 |
(let (($x927 (not $x730)))
|
|
637 |
(let (($x962 (and $x927 $x958)))
|
|
638 |
(let (($x973 (or $x962 $x969)))
|
|
639 |
(let (($x924 (not $x675)))
|
|
640 |
(let (($x977 (and $x924 $x973)))
|
|
641 |
(let (($x908 (not (or $x903 (<= (+ (v_b_array$ ?v0!2) (* (- 1) v_b_max_G_4$)) 0)))))
|
|
642 |
(let (($x912 (and $x890 $x908)))
|
|
643 |
(let (($x916 (or $x877 $x912)))
|
|
644 |
(let (($x871 (not $x617)))
|
|
645 |
(let (($x920 (and $x871 $x916)))
|
|
646 |
(let (($x981 (or $x920 $x977)))
|
|
647 |
(let (($x985 (and $x591 $x981)))
|
|
648 |
(let (($x989 (or $x851 $x985)))
|
|
649 |
(let (($x993 (and $x541 $x989)))
|
|
650 |
(let (($x997 (or $x841 $x993)))
|
|
651 |
(let (($x1076 (= (or (not (and $x931 (not (>= (+ ?v0!3 ?x685) 0)))) $x939) $x1075)))
|
|
652 |
(let ((@x1067 (monotonicity (rewrite (= (+ ?x937 ?x744) (+ ?x744 ?x937))) (= $x939 (<= (+ ?x744 ?x937) 0)))))
|
|
653 |
(let ((@x1074 (trans @x1067 (rewrite (= (<= (+ ?x744 ?x937) 0) $x1070)) (= $x939 $x1070))))
|
|
654 |
(let ((@x1045 (monotonicity (rewrite (= (+ ?v0!3 ?x685) (+ ?x685 ?v0!3))) (= (>= (+ ?v0!3 ?x685) 0) (>= (+ ?x685 ?v0!3) 0)))))
|
|
655 |
(let ((@x1052 (trans @x1045 (rewrite (= (>= (+ ?x685 ?v0!3) 0) $x1048)) (= (>= (+ ?v0!3 ?x685) 0) $x1048))))
|
|
656 |
(let ((@x1058 (monotonicity (monotonicity @x1052 (= (not (>= (+ ?v0!3 ?x685) 0)) $x1053)) (= (and $x931 (not (>= (+ ?v0!3 ?x685) 0))) $x1056))))
|
|
657 |
(let ((@x1061 (monotonicity @x1058 (= (not (and $x931 (not (>= (+ ?v0!3 ?x685) 0)))) $x1059))))
|
|
658 |
(let ((@x1083 (monotonicity (monotonicity (monotonicity @x1061 @x1074 $x1076) (= $x941 $x1078)) (= $x958 $x1081))))
|
|
659 |
(let ((@x1096 (monotonicity (rewrite (= $x966 $x784)) @x1083 (= $x969 (and $x784 $x1081)))))
|
|
660 |
(let ((@x1086 (monotonicity (rewrite (= $x927 $x725)) @x1083 (= $x962 (and $x725 $x1081)))))
|
|
661 |
(let ((@x1104 (monotonicity (trans @x1086 (rewrite (= (and $x725 $x1081) $x1087)) (= $x962 $x1087)) (trans @x1096 (rewrite (= (and $x784 $x1081) $x1097)) (= $x969 $x1097)) (= $x973 $x1102))))
|
|
662 |
(let ((@x1107 (monotonicity (rewrite (= $x924 $x670)) @x1104 (= $x977 (and $x670 $x1102)))))
|
|
663 |
(let (($x1017 (= (or $x903 (<= (+ (v_b_array$ ?v0!2) (* (- 1) v_b_max_G_4$)) 0)) $x1016)))
|
|
664 |
(let (($x906 (<= (+ (v_b_array$ ?v0!2) (* (- 1) v_b_max_G_4$)) 0)))
|
|
665 |
(let (($x1012 (= (<= (+ (* (- 1) v_b_max_G_4$) (v_b_array$ ?v0!2)) 0) $x1011)))
|
|
666 |
(let (($x1007 (= $x906 (<= (+ (* (- 1) v_b_max_G_4$) (v_b_array$ ?v0!2)) 0))))
|
|
667 |
(let (($x1004 (= (+ (v_b_array$ ?v0!2) (* (- 1) v_b_max_G_4$)) (+ (* (- 1) v_b_max_G_4$) (v_b_array$ ?v0!2)))))
|
|
668 |
(let ((@x1015 (trans (monotonicity (rewrite $x1004) $x1007) (rewrite $x1012) (= $x906 $x1011))))
|
|
669 |
(let ((@x1024 (monotonicity (monotonicity (monotonicity @x1015 $x1017) (= $x908 $x1019)) (= $x912 $x1022))))
|
|
670 |
(let ((@x1030 (monotonicity (rewrite (= $x871 $x612)) (monotonicity @x1024 (= $x916 $x1025)) (= $x920 (and $x612 $x1025)))))
|
|
671 |
(let ((@x1115 (monotonicity (trans @x1030 (rewrite (= (and $x612 $x1025) $x1031)) (= $x920 $x1031)) (trans @x1107 (rewrite (= (and $x670 $x1102) $x1108)) (= $x977 $x1108)) (= $x981 $x1113))))
|
|
672 |
(let ((@x1123 (trans (monotonicity @x1115 (= $x985 (and $x591 $x1113))) (rewrite (= (and $x591 $x1113) $x1119)) (= $x985 $x1119))))
|
|
673 |
(let ((@x1132 (monotonicity (monotonicity (monotonicity @x1123 (= $x989 $x1124)) (= $x993 $x1127)) (= $x997 $x1130))))
|
|
674 |
(let ((@x950 (nnf-neg (nnf-pos (refl (~ $x749 $x749)) (~ $x752 $x752)) (~ (not $x755) $x752))))
|
|
675 |
(let ((@x961 (nnf-neg (sk (~ $x755 $x941)) (nnf-neg @x950 (refl (~ $x951 $x951)) (~ (not $x758) $x954)) (~ (not $x761) $x958))))
|
|
676 |
(let ((@x976 (nnf-neg (nnf-neg (refl (~ $x927 $x927)) @x961 (~ (not $x764) $x962)) (nnf-neg (refl (~ $x966 $x966)) @x961 (~ (not $x792) $x969)) (~ (not $x795) $x973))))
|
|
677 |
(let ((@x915 (nnf-neg (nnf-neg (sk (~ $x635 $x890)) (~ (not $x638) $x890)) (sk (~ (not $x649) $x908)) (~ (not $x652) $x912))))
|
|
678 |
(let ((@x919 (nnf-neg (nnf-neg (refl (~ (not $x632) (not $x632))) (~ $x638 $x877)) @x915 (~ (not $x655) $x916))))
|
|
679 |
(let ((@x984 (nnf-neg (nnf-neg (refl (~ $x871 $x871)) @x919 (~ (not $x658) $x920)) (nnf-neg (refl (~ $x924 $x924)) @x976 (~ (not $x798) $x977)) (~ (not $x801) $x981))))
|
|
680 |
(let ((@x867 (monotonicity (refl (~ $x50 $x50)) (nnf-pos (refl (~ $x564 $x564)) (~ $x567 $x567)) (refl (~ $x63 $x63)) (refl (~ $x571 $x571)) (refl (~ $x573 $x573)) (~ $x591 $x591))))
|
|
681 |
(let ((@x988 (nnf-neg (nnf-neg @x867 (~ (not $x596) $x591)) @x984 (~ (not $x804) $x985))))
|
|
682 |
(let ((@x850 (nnf-neg (nnf-pos (refl (~ $x538 $x538)) (~ $x541 $x541)) (~ (not $x544) $x541))))
|
|
683 |
(let ((@x996 (nnf-neg @x850 (nnf-neg (refl (~ $x851 $x851)) @x988 (~ (not $x807) $x989)) (~ (not $x810) $x993))))
|
|
684 |
(let ((@x1000 (mp~ (not-or-elim (mp (asserted $x162) @x823 $x819) (not $x813)) (nnf-neg (sk (~ $x544 $x841)) @x996 (~ (not $x813) $x997)) $x997)))
|
|
685 |
(let ((@x1949 (mp (mp (mp @x1000 @x1132 $x1130) @x1427 $x1425) (monotonicity @x1945 (= $x1425 $x1946)) $x1946)))
|
|
686 |
(let ((@x2062 (unit-resolution (def-axiom (or $x1940 $x1934)) (unit-resolution @x1949 (lemma @x1690 $x1149) $x1943) $x1934)))
|
|
687 |
(let ((@x2069 (unit-resolution (def-axiom (or $x1937 $x851 $x1931)) (mp @x827 (symm (commutativity (= $x50 $x31)) (= $x31 $x50)) $x50) (or $x1937 $x1931))))
|
|
688 |
(let ((@x2070 (unit-resolution @x2069 @x2062 $x1931)))
|
|
689 |
(let ((@x2170 (monotonicity (unit-resolution (def-axiom (or $x1904 $x144)) @x2149 $x144) (= ?x135 ?x62))))
|
|
690 |
(let ((@x2173 (trans @x2170 (unit-resolution (def-axiom (or $x1928 $x63)) @x2070 $x63) (= ?x135 v_b_max_G_1$))))
|
|
691 |
(let ((@x2174 (trans @x2173 (symm (unit-resolution (def-axiom (or $x1904 $x145)) @x2149 $x145) $x1780) $x136)))
|
|
692 |
(let ((@x1523 (def-axiom (or $x1886 $x951))))
|
|
693 |
(let ((@x1808 (def-axiom (or $x1895 $x1318 $x1889))))
|
|
694 |
(let ((@x2176 (unit-resolution @x1808 (unit-resolution @x1523 @x2174 $x1886) (unit-resolution (def-axiom (or $x1904 $x1892)) @x2149 $x1892) $x1318)))
|
|
695 |
(let ((@x1812 (def-axiom (or $x1313 $x1436))))
|
|
696 |
(let ((@x2181 (unit-resolution ((_ th-lemma arith assign-bounds 1 -1 -1) (or $x1453 $x692 $x1070 (not $x1782))) (unit-resolution @x1812 @x2176 $x1436) (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x1780) $x1782)) @x2162 $x1782) (unit-resolution (def-axiom (or $x1904 $x689)) @x2149 $x689) $x1453)))
|
|
697 |
(let ((@x1565 ((_ th-lemma arith triangle-eq) (or $x1563 $x1445))))
|
|
698 |
(let (($x1558 (= v_b_p_G_0$ ?v0!3)))
|
|
699 |
(let ((?x1046 (* (- 1) ?v0!3)))
|
|
700 |
(let ((?x1510 (+ v_b_p_G_0$ ?x1046)))
|
|
701 |
(let (($x1560 (>= ?x1510 0)))
|
|
702 |
(let (($x1522 (>= ?x686 (- 1))))
|
|
703 |
(let ((@x2186 (unit-resolution ((_ th-lemma arith triangle-eq) (or $x1362 $x1522)) (unit-resolution (def-axiom (or $x1904 $x684)) @x2149 $x684) $x1522)))
|
|
704 |
(let ((@x2190 (unit-resolution ((_ th-lemma arith assign-bounds -1 -1) (or $x1560 $x1048 (not $x1522))) (unit-resolution (def-axiom (or $x1313 $x1053)) @x2176 $x1053) @x2186 $x1560)))
|
|
705 |
(let (($x1511 (<= ?x1510 0)))
|
|
706 |
(let (($x1488 (>= (+ v_b_max_G_1$ ?x1068) 0)))
|
|
707 |
(let (($x1955 (not $x1488)))
|
|
708 |
(let ((@x2193 (unit-resolution ((_ th-lemma arith assign-bounds -1 -1) (or $x1955 $x1070 (not $x1782))) (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x1780) $x1782)) @x2162 $x1782) (unit-resolution @x1812 @x2176 $x1436) $x1955)))
|
|
709 |
(let ((@x2093 (unit-resolution (def-axiom (or $x1928 $x1853)) @x2070 $x1853)))
|
|
710 |
(let (($x1476 (or $x1858 $x1298 $x1511 $x1488)))
|
|
711 |
(let (($x1535 (<= (+ ?x937 (* (- 1) v_b_max_G_1$)) 0)))
|
|
712 |
(let (($x1549 (>= (+ ?v0!3 ?x549) 0)))
|
|
713 |
(let (($x1501 (or $x1298 $x1549 $x1535)))
|
|
714 |
(let (($x1464 (or $x1858 $x1501)))
|
|
715 |
(let (($x1478 (= (+ ?x937 (* (- 1) v_b_max_G_1$)) (+ (* (- 1) v_b_max_G_1$) ?x937))))
|
|
716 |
(let ((@x1486 (monotonicity (rewrite $x1478) (= $x1535 (<= (+ (* (- 1) v_b_max_G_1$) ?x937) 0)))))
|
|
717 |
(let ((@x1472 (trans @x1486 (rewrite (= (<= (+ (* (- 1) v_b_max_G_1$) ?x937) 0) $x1488)) (= $x1535 $x1488))))
|
|
718 |
(let ((@x1509 (monotonicity (rewrite (= (+ ?v0!3 ?x549) (+ ?x549 ?v0!3))) (= $x1549 (>= (+ ?x549 ?v0!3) 0)))))
|
|
719 |
(let ((@x1497 (trans @x1509 (rewrite (= (>= (+ ?x549 ?v0!3) 0) $x1511)) (= $x1549 $x1511))))
|
|
720 |
(let ((@x1470 (monotonicity (monotonicity @x1497 @x1472 (= $x1501 (or $x1298 $x1511 $x1488))) (= $x1464 (or $x1858 (or $x1298 $x1511 $x1488))))))
|
|
721 |
(let ((@x1450 (trans @x1470 (rewrite (= (or $x1858 (or $x1298 $x1511 $x1488)) $x1476)) (= $x1464 $x1476))))
|
|
722 |
(let ((@x2195 (unit-resolution (mp ((_ quant-inst ?v0!3) $x1464) @x1450 $x1476) @x2093 (unit-resolution (def-axiom (or $x1313 $x931)) @x2176 $x931) @x2193 $x1511)))
|
|
723 |
(let ((@x2196 (unit-resolution ((_ th-lemma arith triangle-eq) (or $x1558 (not $x1511) (not $x1560))) @x2195 @x2190 $x1558)))
|
|
724 |
(let ((@x1551 (monotonicity (symm (hypothesis $x1558) (= ?v0!3 v_b_p_G_0$)) (= ?x937 ?x101))))
|
|
725 |
(let ((@x1540 (lemma (unit-resolution (hypothesis $x1563) (symm @x1551 $x1559) false) (or (not $x1558) $x1559))))
|
|
726 |
(let ((@x2198 (lemma (unit-resolution @x1540 @x2196 (unit-resolution @x1565 @x2181 $x1563) false) $x1904)))
|
|
727 |
(let (($x1990 (<= (+ v_b_max_G_1$ (* (- 1) v_b_max_G_4$)) 0)))
|
|
728 |
(let (($x1988 (= v_b_max_G_1$ v_b_max_G_4$)))
|
|
729 |
(let ((@x2109 (symm (unit-resolution (def-axiom (or $x1872 $x73)) (hypothesis $x1875) $x73) $x1988)))
|
|
730 |
(let (($x2025 (>= (+ v_b_max_G_1$ (* (- 1) (v_b_array$ ?v0!2))) 0)))
|
|
731 |
(let (($x901 (not $x900)))
|
|
732 |
(let (($x1835 (not $x1861)))
|
|
733 |
(let (($x2042 (= ?x62 v_b_max_G_4$)))
|
|
734 |
(let (($x2043 (or $x1286 (<= (+ v_b_length$ (* (- 1) v_b_k_G_0$)) 0) $x2042)))
|
|
735 |
(let ((@x2073 (trans (unit-resolution (def-axiom (or $x1928 $x63)) @x2070 $x63) (symm (hypothesis $x73) $x1988) $x2042)))
|
|
736 |
(let ((@x2076 (unit-resolution ((_ quant-inst v_b_k_G_0$) (or $x1835 (not $x2043))) (hypothesis $x1861) (unit-resolution (def-axiom (or $x2043 (not $x2042))) @x2073 $x2043) false)))
|
|
737 |
(let ((@x2115 (unit-resolution (lemma @x2076 (or $x1835 $x1289)) (unit-resolution (def-axiom (or $x1872 $x73)) (hypothesis $x1875) $x73) $x1835)))
|
|
738 |
(let ((@x2116 (unit-resolution (def-axiom (or $x1869 $x1861 $x1275)) @x2115 (unit-resolution (def-axiom (or $x1872 $x1866)) (hypothesis $x1875) $x1866) $x1275)))
|
|
739 |
(let ((@x2103 ((_ th-lemma arith farkas -1 -1 1) (hypothesis (<= (+ v_b_p_G_0$ (* (- 1) ?v0!2)) 0)) (hypothesis $x600) (hypothesis $x901) false)))
|
|
740 |
(let ((@x2106 (lemma @x2103 (or (not (<= (+ v_b_p_G_0$ (* (- 1) ?v0!2)) 0)) $x661 $x900))))
|
|
741 |
(let ((@x2119 (unit-resolution @x2106 (unit-resolution (def-axiom (or $x1872 $x600)) (hypothesis $x1875) $x600) (unit-resolution (def-axiom (or $x1274 $x901)) @x2116 $x901) (not (<= (+ v_b_p_G_0$ (* (- 1) ?v0!2)) 0)))))
|
|
742 |
(let (($x2032 (<= (+ v_b_p_G_0$ (* (- 1) ?v0!2)) 0)))
|
|
743 |
(let (($x2056 (or $x1858 $x1247 $x2032 $x2025)))
|
|
744 |
(let (($x2009 (<= (+ (v_b_array$ ?v0!2) (* (- 1) v_b_max_G_1$)) 0)))
|
|
745 |
(let (($x2001 (>= (+ ?v0!2 ?x549) 0)))
|
|
746 |
(let (($x2010 (or $x1247 $x2001 $x2009)))
|
|
747 |
(let (($x2060 (or $x1858 $x2010)))
|
|
748 |
(let (($x2026 (= (<= (+ (* (- 1) v_b_max_G_1$) (v_b_array$ ?v0!2)) 0) $x2025)))
|
|
749 |
(let (($x2020 (= $x2009 (<= (+ (* (- 1) v_b_max_G_1$) (v_b_array$ ?v0!2)) 0))))
|
|
750 |
(let (($x2038 (= (+ (v_b_array$ ?v0!2) (* (- 1) v_b_max_G_1$)) (+ (* (- 1) v_b_max_G_1$) (v_b_array$ ?v0!2)))))
|
|
751 |
(let ((@x2052 (trans (monotonicity (rewrite $x2038) $x2020) (rewrite $x2026) (= $x2009 $x2025))))
|
|
752 |
(let ((@x2018 (monotonicity (rewrite (= (+ ?v0!2 ?x549) (+ ?x549 ?v0!2))) (= $x2001 (>= (+ ?x549 ?v0!2) 0)))))
|
|
753 |
(let ((@x2036 (trans @x2018 (rewrite (= (>= (+ ?x549 ?v0!2) 0) $x2032)) (= $x2001 $x2032))))
|
|
754 |
(let ((@x2031 (monotonicity (monotonicity @x2036 @x2052 (= $x2010 (or $x1247 $x2032 $x2025))) (= $x2060 (or $x1858 (or $x1247 $x2032 $x2025))))))
|
|
755 |
(let ((@x2079 (trans @x2031 (rewrite (= (or $x1858 (or $x1247 $x2032 $x2025)) $x2056)) (= $x2060 $x2056))))
|
|
756 |
(let ((@x2122 (unit-resolution (mp ((_ quant-inst ?v0!2) $x2060) @x2079 $x2056) @x2093 (unit-resolution (def-axiom (or $x1274 $x897)) @x2116 $x897) (or $x2032 $x2025))))
|
|
757 |
(let ((@x2125 ((_ th-lemma arith farkas 1 -1 1) (unit-resolution (def-axiom (or $x1274 (not $x1011))) @x2116 (not $x1011)) (unit-resolution @x2122 @x2119 $x2025) (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x1988) $x1990)) @x2109 $x1990) false)))
|
|
758 |
(let ((@x2133 (unit-resolution (def-axiom (or $x1925 $x1875 $x1919)) (lemma @x2125 $x1872) (unit-resolution (def-axiom (or $x1928 $x1922)) @x2070 $x1922) $x1919)))
|
|
759 |
(let ((@x2003 (unit-resolution (def-axiom (or $x1913 $x1901 $x1907)) (unit-resolution (def-axiom (or $x1916 $x1910)) @x2133 $x1910) $x1910)))
|
|
760 |
(let ((@x2004 (unit-resolution @x2003 @x2198 $x1901)))
|
|
761 |
(let ((@x1528 (trans (monotonicity (hypothesis $x107) (= ?x135 ?x101)) (symm (hypothesis $x104) (= ?x101 v_b_max_G_2$)) (= ?x135 v_b_max_G_2$))))
|
|
762 |
(let ((@x1529 (trans @x1528 (symm (hypothesis $x109) (= v_b_max_G_2$ v_b_max_G_3$)) $x136)))
|
|
763 |
(let ((@x1532 (lemma (unit-resolution (hypothesis $x951) @x1529 false) (or $x136 $x1361 $x1359 $x1360))))
|
|
764 |
(let ((@x2140 (unit-resolution @x1532 (unit-resolution (def-axiom (or $x1898 $x109)) @x2004 $x109) (unit-resolution (def-axiom (or $x1898 $x104)) @x2004 $x104) (unit-resolution (def-axiom (or $x1898 $x107)) @x2004 $x107) $x136)))
|
|
765 |
(let ((@x2128 (unit-resolution ((_ th-lemma arith triangle-eq) (or $x1362 $x1522)) (unit-resolution (def-axiom (or $x1898 $x684)) @x2004 $x684) $x1522)))
|
|
766 |
(let ((@x1460 (unit-resolution @x1808 (unit-resolution @x1523 (hypothesis $x136) $x1886) (hypothesis $x1892) $x1318)))
|
|
767 |
(let ((@x1539 (def-axiom (or $x1313 $x1053))))
|
|
768 |
(let (($x1965 (not $x1560)))
|
|
769 |
(let (($x1597 (<= (+ ?x101 ?x744) 0)))
|
|
770 |
(let ((@x1431 (trans (symm (hypothesis $x104) (= ?x101 v_b_max_G_2$)) (symm (hypothesis $x109) (= v_b_max_G_2$ v_b_max_G_3$)) (= ?x101 v_b_max_G_3$))))
|
|
771 |
(let ((@x1435 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not (= ?x101 v_b_max_G_3$)) $x1597)) @x1431 $x1597)))
|
|
772 |
(let ((@x1437 (lemma ((_ th-lemma arith farkas -1 -1 1) (hypothesis $x1436) (hypothesis $x1597) (hypothesis $x1445) false) (or $x1453 $x1070 (not $x1597)))))
|
|
773 |
(let ((@x1952 (unit-resolution @x1565 (unit-resolution @x1437 (unit-resolution @x1812 @x1460 $x1436) @x1435 $x1453) $x1563)))
|
|
774 |
(let ((@x1958 (unit-resolution ((_ th-lemma arith assign-bounds 1 1 1) (or $x1955 $x1070 (not $x1597) $x689)) (unit-resolution @x1812 @x1460 $x1436) @x1435 (hypothesis $x692) $x1955)))
|
|
775 |
(let ((@x1962 (unit-resolution (mp ((_ quant-inst ?v0!3) $x1464) @x1450 $x1476) (hypothesis $x1853) (unit-resolution (def-axiom (or $x1313 $x931)) @x1460 $x931) (or $x1511 $x1488))))
|
|
776 |
(let ((@x1969 (unit-resolution ((_ th-lemma arith triangle-eq) (or $x1558 (not $x1511) $x1965)) (unit-resolution @x1962 @x1958 $x1511) (or $x1558 $x1965))))
|
|
777 |
(let ((@x1971 ((_ th-lemma arith farkas -1 1 1) (unit-resolution @x1969 (unit-resolution @x1540 @x1952 (not $x1558)) $x1965) (hypothesis $x1522) (unit-resolution @x1539 @x1460 $x1053) false)))
|
|
778 |
(let ((@x2130 (unit-resolution (lemma @x1971 (or $x951 (not $x1522) $x1858 $x689 $x1895 $x1359 $x1361)) @x2093 (or $x951 (not $x1522) $x689 $x1895 $x1359 $x1361))))
|
|
779 |
(unit-resolution @x2130 @x2128 @x2140 (unit-resolution (def-axiom (or $x1898 $x692)) @x2004 $x692) (unit-resolution (def-axiom (or $x1898 $x1892)) @x2004 $x1892) (unit-resolution (def-axiom (or $x1898 $x104)) @x2004 $x104) (unit-resolution (def-axiom (or $x1898 $x109)) @x2004 $x109) false)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
|
|
780 |
|