src/HOL/SMT_Examples/Boogie_Max.certs2
author boehmes
Thu May 01 22:57:38 2014 +0200 (2014-05-01)
changeset 56818 689a3eeb6f9e
child 57170 3afada8f820d
permissions -rw-r--r--
use SMT2 for Boogie examples
     1 336198ca2566b9b7e0ce4a688dd7f9094f37a0b9 843 0
     2 unsat
     3 ((set-logic AUFLIA)
     4 (declare-fun ?v0!5 () Int)
     5 (declare-fun ?v0!4 () Int)
     6 (declare-fun ?v0!3 () Int)
     7 (declare-fun ?v0!2 () Int)
     8 (declare-fun k!10 () Bool)
     9 (declare-fun k!00 () Bool)
    10 (proof
    11 (let (($x109 (= v_b_max_G_3$ v_b_max_G_2$)))
    12 (let ((?x135 (v_b_array$ v_b_k_G_1$)))
    13 (let (($x136 (= ?x135 v_b_max_G_3$)))
    14 (let (($x2120 (forall ((?v0 Int) )(!(let (($x1020 (<= (+ (v_b_array$ ?v0) (* (- 1) v_b_max_G_3$)) 0)))
    15 (let (($x1005 (>= (+ ?v0 (* (- 1) v_b_p_G_1$)) 0)))
    16 (let (($x838 (>= ?v0 0)))
    17 (let (($x1399 (not $x838)))
    18 (or $x1399 $x1005 $x1020))))) :pattern ( (v_b_array$ ?v0) )))
    19 ))
    20 (let (($x2128 (or (not $x2120) $x136)))
    21 (let (($x2131 (not $x2128)))
    22 (let (($x1312 (>= (+ v_b_max_G_3$ (* (- 1) (v_b_array$ ?v0!5))) 0)))
    23 (let (($x1290 (<= (+ v_b_p_G_1$ (* (- 1) ?v0!5)) 0)))
    24 (let (($x1173 (>= ?v0!5 0)))
    25 (let (($x1540 (not $x1173)))
    26 (let (($x1555 (or $x1540 $x1290 $x1312)))
    27 (let (($x1560 (not $x1555)))
    28 (let (($x2134 (or $x1560 $x2131)))
    29 (let (($x2137 (not $x2134)))
    30 (let (($x996 (>= v_b_p_G_1$ 2)))
    31 (let (($x1606 (not $x996)))
    32 (let (($x991 (= (+ v_b_p_G_0$ (* (- 1) v_b_p_G_1$)) (- 1))))
    33 (let (($x1605 (not $x991)))
    34 (let (($x989 (>= v_b_k_G_1$ 0)))
    35 (let (($x1604 (not $x989)))
    36 (let (($x1603 (not $x109)))
    37 (let (($x107 (= v_b_k_G_1$ v_b_p_G_0$)))
    38 (let (($x1602 (not $x107)))
    39 (let ((?x101 (v_b_array$ v_b_p_G_0$)))
    40 (let (($x104 (= v_b_max_G_2$ ?x101)))
    41 (let (($x1601 (not $x104)))
    42 (let (($x980 (>= (+ v_b_max_G_1$ (* (- 1) ?x101)) 0)))
    43 (let (($x885 (>= v_b_p_G_0$ 1)))
    44 (let (($x1529 (not $x885)))
    45 (let (($x882 (>= v_b_k_G_0$ 0)))
    46 (let (($x1528 (not $x882)))
    47 (let (($x2140 (or $x1528 $x1529 $x980 $x1601 $x1602 $x1603 $x1604 $x1605 $x1606 $x2137)))
    48 (let (($x2143 (not $x2140)))
    49 (let (($x985 (not $x980)))
    50 (let (($x2146 (or $x1528 $x1529 $x985 (not (= v_b_k_G_1$ v_b_k_G_0$)) (not (= v_b_max_G_3$ v_b_max_G_1$)) $x1604 $x1605 $x1606 $x2137)))
    51 (let ((?x1179 (v_b_array$ ?v0!5)))
    52 (let (($x1799 (= ?x101 ?x1179)))
    53 (let (($x1803 (not $x1799)))
    54 (let (($x1703 (>= (+ ?x101 (* (- 1) ?x1179)) 0)))
    55 (let (($x1693 (not $x1703)))
    56 (let (($x2149 (not $x2146)))
    57 (let ((@x2389 (hypothesis $x2149)))
    58 (let (($x2024 (<= (+ v_b_max_G_1$ (* (- 1) v_b_max_G_3$)) 0)))
    59 (let (($x2022 (= v_b_max_G_1$ v_b_max_G_3$)))
    60 (let ((@x2401 (symm (commutativity (= $x2022 (= v_b_max_G_3$ v_b_max_G_1$))) (= (= v_b_max_G_3$ v_b_max_G_1$) $x2022))))
    61 (let (($x145 (= v_b_max_G_3$ v_b_max_G_1$)))
    62 (let ((@x2406 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x2022) $x2024)) (mp (unit-resolution (def-axiom (or $x2146 $x145)) @x2389 $x145) @x2401 $x2022) $x2024)))
    63 (let (($x1678 (not $x1312)))
    64 (let ((?x62 (v_b_array$ v_b_k_G_0$)))
    65 (let (($x63 (= ?x62 v_b_max_G_1$)))
    66 (let (($x2152 (or $x2143 $x2149)))
    67 (let (($x2155 (not $x2152)))
    68 (let (($x919 (<= (+ v_b_length$ (* (- 1) v_b_p_G_0$)) 0)))
    69 (let (($x2158 (or $x1528 $x1529 $x919 $x2155)))
    70 (let (($x2161 (not $x2158)))
    71 (let (($x1253 (>= (+ v_b_max_G_4$ (* (- 1) (v_b_array$ ?v0!4))) 0)))
    72 (let (($x1142 (<= (+ v_b_length$ (* (- 1) ?v0!4)) 0)))
    73 (let (($x1139 (>= ?v0!4 0)))
    74 (let (($x1489 (not $x1139)))
    75 (let (($x1131 (= (v_b_array$ ?v0!3) v_b_max_G_4$)))
    76 (let (($x1126 (<= (+ v_b_length$ (* (- 1) ?v0!3)) 0)))
    77 (let (($x1484 (or (not (>= ?v0!3 0)) $x1126 $x1131)))
    78 (let (($x1516 (or (not $x1484) $x1489 $x1142 $x1253)))
    79 (let (($x1517 (not $x1516)))
    80 (let (($x2103 (forall ((?v0 Int) )(!(let ((?x46 (v_b_array$ ?v0)))
    81 (let (($x86 (= ?x46 v_b_max_G_4$)))
    82 (let (($x930 (<= (+ v_b_length$ (* (- 1) ?v0)) 0)))
    83 (let (($x838 (>= ?v0 0)))
    84 (let (($x1399 (not $x838)))
    85 (let (($x1458 (or $x1399 $x930 $x86)))
    86 (not $x1458))))))) :pattern ( (v_b_array$ ?v0) )))
    87 ))
    88 (let (($x2108 (or $x2103 $x1517)))
    89 (let (($x2111 (not $x2108)))
    90 (let (($x73 (= v_b_max_G_4$ v_b_max_G_1$)))
    91 (let (($x1531 (not $x73)))
    92 (let (($x971 (not $x919)))
    93 (let (($x2114 (or $x1528 $x1529 $x971 (not k!00) $x1531 (not k!10) $x2111)))
    94 (let (($x2117 (not $x2114)))
    95 (let (($x2164 (or $x2117 $x2161)))
    96 (let (($x2167 (not $x2164)))
    97 (let (($x2095 (forall ((?v0 Int) )(!(let (($x903 (<= (+ (v_b_array$ ?v0) (* (- 1) v_b_max_G_1$)) 0)))
    98 (let (($x888 (>= (+ ?v0 (* (- 1) v_b_p_G_0$)) 0)))
    99 (let (($x838 (>= ?v0 0)))
   100 (let (($x1399 (not $x838)))
   101 (or $x1399 $x888 $x903))))) :pattern ( (v_b_array$ ?v0) )))
   102 ))
   103 (let (($x2100 (not $x2095)))
   104 (let (($x2170 (or $x1528 $x1529 $x2100 (not $x63) $x2167)))
   105 (let (($x2173 (not $x2170)))
   106 (let ((?x30 (v_b_array$ 0)))
   107 (let (($x50 (= ?x30 v_b_max_G_0$)))
   108 (let (($x1095 (not $x50)))
   109 (let (($x2176 (or $x1095 $x2173)))
   110 (let (($x2179 (not $x2176)))
   111 (let (($x2087 (forall ((?v0 Int) )(!(let (($x851 (>= (+ v_b_max_G_0$ (* (- 1) (v_b_array$ ?v0))) 0)))
   112 (let (($x841 (>= ?v0 1)))
   113 (let (($x838 (>= ?v0 0)))
   114 (let (($x1399 (not $x838)))
   115 (or $x1399 $x841 $x851))))) :pattern ( (v_b_array$ ?v0) )))
   116 ))
   117 (let (($x2182 (or (not $x2087) $x2179)))
   118 (let (($x2185 (not $x2182)))
   119 (let (($x1083 (>= (+ v_b_max_G_0$ (* (- 1) (v_b_array$ ?v0!2))) 0)))
   120 (let (($x831 (>= ?v0!2 1)))
   121 (let (($x1391 (or (not (>= ?v0!2 0)) $x831 $x1083)))
   122 (let (($x1079 (not $x831)))
   123 (let (($x1396 (not $x1391)))
   124 (let ((@x1966 (hypothesis $x1396)))
   125 (let (($x1078 (>= ?v0!2 0)))
   126 (let ((@x1951 ((_ th-lemma arith eq-propagate 0 0) (unit-resolution (def-axiom (or $x1391 $x1078)) @x1966 $x1078) (unit-resolution (def-axiom (or $x1391 $x1079)) @x1966 $x1079) (= ?v0!2 0))))
   127 (let ((@x1955 (symm (monotonicity @x1951 (= (v_b_array$ ?v0!2) ?x30)) (= ?x30 (v_b_array$ ?v0!2)))))
   128 (let (($x31 (= v_b_max_G_0$ ?x30)))
   129 (let (($x201 (and (not (<= v_b_length$ 0)) $x31)))
   130 (let (($x572 (forall ((?v0 Int) )(let ((?x46 (v_b_array$ ?v0)))
   131 (let (($x132 (<= ?x46 v_b_max_G_3$)))
   132 (or (not (and (<= 0 ?v0) (not (<= v_b_p_G_1$ ?v0)))) $x132))))
   133 ))
   134 (let (($x595 (or (not $x572) $x136)))
   135 (let (($x600 (and $x572 $x595)))
   136 (let (($x116 (<= 2 v_b_p_G_1$)))
   137 (let (($x456 (= v_b_p_G_1$ (+ 1 v_b_p_G_0$))))
   138 (let (($x110 (<= 0 v_b_k_G_1$)))
   139 (let (($x144 (= v_b_k_G_1$ v_b_k_G_0$)))
   140 (let (($x143 (<= ?x101 v_b_max_G_1$)))
   141 (let (($x54 (<= 1 v_b_p_G_0$)))
   142 (let (($x52 (<= 0 v_b_k_G_0$)))
   143 (let (($x654 (and $x52 $x54 $x143 $x144 $x145 $x110 $x456 $x116)))
   144 (let (($x669 (not $x654)))
   145 (let (($x670 (or $x669 $x600)))
   146 (let (($x441 (not $x143)))
   147 (let (($x544 (and $x52 $x54 $x441 $x104 $x107 $x109 $x110 $x456 $x116)))
   148 (let (($x606 (not $x544)))
   149 (let (($x607 (or $x606 $x600)))
   150 (let (($x675 (and $x607 $x670)))
   151 (let (($x69 (<= v_b_length$ v_b_p_G_0$)))
   152 (let (($x415 (not $x69)))
   153 (let (($x429 (and $x52 $x54 $x415)))
   154 (let (($x681 (not $x429)))
   155 (let (($x682 (or $x681 $x675)))
   156 (let (($x377 (forall ((?v0 Int) )(let ((?x46 (v_b_array$ ?v0)))
   157 (let (($x89 (<= ?x46 v_b_max_G_4$)))
   158 (let (($x351 (not (<= v_b_length$ ?v0))))
   159 (let (($x43 (<= 0 ?v0)))
   160 (let (($x354 (and $x43 $x351)))
   161 (let (($x360 (not $x354)))
   162 (or $x360 $x89))))))))
   163 ))
   164 (let (($x366 (exists ((?v0 Int) )(let ((?x46 (v_b_array$ ?v0)))
   165 (let (($x86 (= ?x46 v_b_max_G_4$)))
   166 (let (($x351 (not (<= v_b_length$ ?v0))))
   167 (let (($x43 (<= 0 ?v0)))
   168 (let (($x354 (and $x43 $x351)))
   169 (let (($x360 (not $x354)))
   170 (or $x360 $x86))))))))
   171 ))
   172 (let (($x398 (or (not $x366) $x377)))
   173 (let (($x403 (and $x366 $x398)))
   174 (let (($x75 (= v_b_p_G_2$ v_b_p_G_0$)))
   175 (let (($x71 (= v_b_k_G_2$ v_b_k_G_0$)))
   176 (let (($x338 (and $x52 $x54 $x69 $x71 $x73 $x75)))
   177 (let (($x409 (not $x338)))
   178 (let (($x410 (or $x409 $x403)))
   179 (let (($x687 (and $x410 $x682)))
   180 (let (($x259 (forall ((?v0 Int) )(let ((?x46 (v_b_array$ ?v0)))
   181 (let (($x59 (<= ?x46 v_b_max_G_1$)))
   182 (or (not (and (<= 0 ?v0) (not (<= v_b_p_G_0$ ?v0)))) $x59))))
   183 ))
   184 (let (($x294 (and $x50 $x52 $x54 $x259 $x63)))
   185 (let (($x694 (or (not $x294) $x687)))
   186 (let (($x699 (and $x50 $x694)))
   187 (let (($x234 (forall ((?v0 Int) )(let ((?x46 (v_b_array$ ?v0)))
   188 (let (($x47 (<= ?x46 v_b_max_G_0$)))
   189 (or (not (and (<= 0 ?v0) (not (<= 1 ?v0)))) $x47))))
   190 ))
   191 (let (($x705 (not $x234)))
   192 (let (($x706 (or $x705 $x699)))
   193 (let (($x711 (and $x234 $x706)))
   194 (let (($x718 (or (not $x201) $x711)))
   195 (let (($x138 (=> (and $x136 false) true)))
   196 (let (($x139 (and $x136 $x138)))
   197 (let (($x134 (forall ((?v0 Int) )(let ((?x46 (v_b_array$ ?v0)))
   198 (let (($x132 (<= ?x46 v_b_max_G_3$)))
   199 (=> (and (<= 0 ?v0) (< ?v0 v_b_p_G_1$)) $x132))))
   200 ))
   201 (let (($x140 (=> $x134 $x139)))
   202 (let (($x141 (and $x134 $x140)))
   203 (let (($x117 (and $x110 $x116)))
   204 (let (($x118 (and $x117 true)))
   205 (let (($x119 (and (= v_b_p_G_1$ (+ v_b_p_G_0$ 1)) $x118)))
   206 (let (($x111 (and $x110 $x54)))
   207 (let (($x120 (and $x111 $x119)))
   208 (let (($x121 (and true $x120)))
   209 (let (($x146 (and $x145 $x121)))
   210 (let (($x147 (and $x144 $x146)))
   211 (let (($x148 (and true $x147)))
   212 (let (($x55 (and $x52 $x54)))
   213 (let (($x149 (and $x55 $x148)))
   214 (let (($x150 (and $x143 $x149)))
   215 (let (($x151 (and $x55 $x150)))
   216 (let (($x152 (and true $x151)))
   217 (let (($x153 (=> $x152 $x141)))
   218 (let (($x122 (and $x109 $x121)))
   219 (let (($x123 (and $x107 $x122)))
   220 (let (($x124 (and true $x123)))
   221 (let (($x105 (and $x54 $x54)))
   222 (let (($x125 (and $x105 $x124)))
   223 (let (($x126 (and $x104 $x125)))
   224 (let (($x127 (and (< v_b_max_G_1$ ?x101) $x126)))
   225 (let (($x128 (and $x55 $x127)))
   226 (let (($x129 (and true $x128)))
   227 (let (($x142 (=> $x129 $x141)))
   228 (let (($x98 (and (< v_b_p_G_0$ v_b_length$) $x55)))
   229 (let (($x99 (and $x55 $x98)))
   230 (let (($x100 (and true $x99)))
   231 (let (($x155 (=> $x100 (and $x142 $x153))))
   232 (let (($x91 (forall ((?v0 Int) )(let ((?x46 (v_b_array$ ?v0)))
   233 (let (($x89 (<= ?x46 v_b_max_G_4$)))
   234 (let (($x43 (<= 0 ?v0)))
   235 (let (($x85 (and $x43 (< ?v0 v_b_length$))))
   236 (=> $x85 $x89))))))
   237 ))
   238 (let (($x92 (=> $x91 true)))
   239 (let (($x93 (and $x91 $x92)))
   240 (let (($x88 (exists ((?v0 Int) )(let ((?x46 (v_b_array$ ?v0)))
   241 (let (($x86 (= ?x46 v_b_max_G_4$)))
   242 (let (($x43 (<= 0 ?v0)))
   243 (let (($x85 (and $x43 (< ?v0 v_b_length$))))
   244 (=> $x85 $x86))))))
   245 ))
   246 (let (($x94 (=> $x88 $x93)))
   247 (let (($x78 (and $x71 (and $x73 (and $x75 true)))))
   248 (let (($x79 (and true $x78)))
   249 (let (($x80 (and $x55 $x79)))
   250 (let (($x81 (and $x69 $x80)))
   251 (let (($x82 (and $x55 $x81)))
   252 (let (($x83 (and true $x82)))
   253 (let (($x96 (=> $x83 (and $x88 $x94))))
   254 (let (($x64 (and $x63 $x55)))
   255 (let (($x61 (forall ((?v0 Int) )(let ((?x46 (v_b_array$ ?v0)))
   256 (let (($x59 (<= ?x46 v_b_max_G_1$)))
   257 (=> (and (<= 0 ?v0) (< ?v0 v_b_p_G_0$)) $x59))))
   258 ))
   259 (let (($x65 (and $x61 $x64)))
   260 (let (($x66 (and $x55 $x65)))
   261 (let (($x67 (and true $x66)))
   262 (let (($x68 (and $x50 $x67)))
   263 (let (($x157 (=> $x68 (and $x96 $x155))))
   264 (let (($x49 (forall ((?v0 Int) )(let ((?x46 (v_b_array$ ?v0)))
   265 (let (($x47 (<= ?x46 v_b_max_G_0$)))
   266 (=> (and (<= 0 ?v0) (< ?v0 1)) $x47))))
   267 ))
   268 (let (($x159 (=> $x49 (and $x50 $x157))))
   269 (let (($x34 (<= 1 1)))
   270 (let (($x35 (and $x34 $x34)))
   271 (let (($x32 (<= 0 0)))
   272 (let (($x36 (and $x32 $x35)))
   273 (let (($x37 (and $x32 $x36)))
   274 (let (($x38 (and $x31 $x37)))
   275 (let (($x39 (and true $x38)))
   276 (let (($x41 (and true (and (< 0 v_b_length$) $x39))))
   277 (let (($x161 (=> $x41 (and $x49 $x159))))
   278 (let (($x162 (not $x161)))
   279 (let ((@x579 (monotonicity (rewrite (= (and $x136 false) false)) (= $x138 (=> false true)))))
   280 (let ((@x583 (trans @x579 (rewrite (= (=> false true) true)) (= $x138 true))))
   281 (let ((@x590 (trans (monotonicity @x583 (= $x139 (and $x136 true))) (rewrite (= (and $x136 true) $x136)) (= $x139 $x136))))
   282 (let ((?x46 (v_b_array$ ?0)))
   283 (let (($x132 (<= ?x46 v_b_max_G_3$)))
   284 (let (($x567 (or (not (and (<= 0 ?0) (not (<= v_b_p_G_1$ ?0)))) $x132)))
   285 (let (($x133 (=> (and (<= 0 ?0) (< ?0 v_b_p_G_1$)) $x132)))
   286 (let (($x568 (= (=> (and (<= 0 ?0) (not (<= v_b_p_G_1$ ?0))) $x132) $x567)))
   287 (let (($x564 (= $x133 (=> (and (<= 0 ?0) (not (<= v_b_p_G_1$ ?0))) $x132))))
   288 (let (($x557 (not (<= v_b_p_G_1$ ?0))))
   289 (let (($x43 (<= 0 ?0)))
   290 (let (($x560 (and $x43 $x557)))
   291 (let ((@x212 (rewrite (= $x43 $x43))))
   292 (let ((@x562 (monotonicity @x212 (rewrite (= (< ?0 v_b_p_G_1$) $x557)) (= (and $x43 (< ?0 v_b_p_G_1$)) $x560))))
   293 (let ((@x574 (quant-intro (trans (monotonicity @x562 $x564) (rewrite $x568) (= $x133 $x567)) (= $x134 $x572))))
   294 (let ((@x599 (trans (monotonicity @x574 @x590 (= $x140 (=> $x572 $x136))) (rewrite (= (=> $x572 $x136) $x595)) (= $x140 $x595))))
   295 (let ((@x656 (rewrite (= (and $x55 (and $x143 $x52 $x54 $x144 $x145 $x110 $x456 $x116)) $x654))))
   296 (let (($x646 (and $x143 $x52 $x54 $x144 $x145 $x110 $x456 $x116)))
   297 (let ((@x648 (rewrite (= (and $x143 (and $x52 $x54 $x144 $x145 $x110 $x456 $x116)) $x646))))
   298 (let (($x638 (and $x52 $x54 $x144 $x145 $x110 $x456 $x116)))
   299 (let (($x623 (and $x144 $x145 $x110 $x54 $x456 $x116)))
   300 (let (($x615 (and $x145 $x110 $x54 $x456 $x116)))
   301 (let (($x482 (and $x110 $x54 $x456 $x116)))
   302 (let ((@x463 (rewrite (= $x116 $x116))))
   303 (let ((@x450 (rewrite (= $x110 $x110))))
   304 (let ((@x467 (monotonicity (monotonicity @x450 @x463 (= $x117 $x117)) (= $x118 $x118))))
   305 (let ((@x460 (rewrite (= $x456 $x456))))
   306 (let ((@x458 (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)) $x456))))
   307 (let ((@x473 (monotonicity (trans @x458 @x460 (= (= v_b_p_G_1$ (+ v_b_p_G_0$ 1)) $x456)) (trans @x467 (rewrite (= $x118 $x117)) (= $x118 $x117)) (= $x119 (and $x456 $x117)))))
   308 (let ((@x478 (trans @x473 (rewrite (= (and $x456 $x117) (and $x456 $x110 $x116))) (= $x119 (and $x456 $x110 $x116)))))
   309 (let ((@x481 (monotonicity (monotonicity @x450 (rewrite (= $x54 $x54)) (= $x111 $x111)) @x478 (= $x120 (and $x111 (and $x456 $x110 $x116))))))
   310 (let ((@x486 (trans @x481 (rewrite (= (and $x111 (and $x456 $x110 $x116)) $x482)) (= $x120 $x482))))
   311 (let ((@x493 (trans (monotonicity @x486 (= $x121 (and true $x482))) (rewrite (= (and true $x482) $x482)) (= $x121 $x482))))
   312 (let ((@x619 (trans (monotonicity @x493 (= $x146 (and $x145 $x482))) (rewrite (= (and $x145 $x482) $x615)) (= $x146 $x615))))
   313 (let ((@x627 (trans (monotonicity @x619 (= $x147 (and $x144 $x615))) (rewrite (= (and $x144 $x615) $x623)) (= $x147 $x623))))
   314 (let ((@x634 (trans (monotonicity @x627 (= $x148 (and true $x623))) (rewrite (= (and true $x623) $x623)) (= $x148 $x623))))
   315 (let ((@x240 (rewrite (= $x54 $x54))))
   316 (let ((@x238 (rewrite (= $x52 $x52))))
   317 (let ((@x242 (monotonicity @x238 @x240 (= $x55 $x55))))
   318 (let ((@x642 (trans (monotonicity @x242 @x634 (= $x149 (and $x55 $x623))) (rewrite (= (and $x55 $x623) $x638)) (= $x149 $x638))))
   319 (let ((@x650 (trans (monotonicity @x642 (= $x150 (and $x143 $x638))) @x648 (= $x150 $x646))))
   320 (let ((@x658 (trans (monotonicity @x242 @x650 (= $x151 (and $x55 $x646))) @x656 (= $x151 $x654))))
   321 (let ((@x665 (trans (monotonicity @x658 (= $x152 (and true $x654))) (rewrite (= (and true $x654) $x654)) (= $x152 $x654))))
   322 (let ((@x668 (monotonicity @x665 (monotonicity @x574 @x599 (= $x141 $x600)) (= $x153 (=> $x654 $x600)))))
   323 (let ((@x546 (rewrite (= (and $x55 (and $x441 $x104 $x54 $x107 $x109 $x110 $x456 $x116)) $x544))))
   324 (let (($x536 (and $x441 $x104 $x54 $x107 $x109 $x110 $x456 $x116)))
   325 (let ((@x538 (rewrite (= (and $x441 (and $x104 $x54 $x107 $x109 $x110 $x456 $x116)) $x536))))
   326 (let (($x528 (and $x104 $x54 $x107 $x109 $x110 $x456 $x116)))
   327 (let (($x520 (and $x54 $x107 $x109 $x110 $x456 $x116)))
   328 (let (($x505 (and $x107 $x109 $x110 $x54 $x456 $x116)))
   329 (let ((@x501 (trans (monotonicity @x493 (= $x122 (and $x109 $x482))) (rewrite (= (and $x109 $x482) (and $x109 $x110 $x54 $x456 $x116))) (= $x122 (and $x109 $x110 $x54 $x456 $x116)))))
   330 (let ((@x504 (monotonicity @x501 (= $x123 (and $x107 (and $x109 $x110 $x54 $x456 $x116))))))
   331 (let ((@x509 (trans @x504 (rewrite (= (and $x107 (and $x109 $x110 $x54 $x456 $x116)) $x505)) (= $x123 $x505))))
   332 (let ((@x516 (trans (monotonicity @x509 (= $x124 (and true $x505))) (rewrite (= (and true $x505) $x505)) (= $x124 $x505))))
   333 (let ((@x448 (trans (monotonicity @x240 @x240 (= $x105 $x105)) (rewrite (= $x105 $x54)) (= $x105 $x54))))
   334 (let ((@x524 (trans (monotonicity @x448 @x516 (= $x125 (and $x54 $x505))) (rewrite (= (and $x54 $x505) $x520)) (= $x125 $x520))))
   335 (let ((@x532 (trans (monotonicity @x524 (= $x126 (and $x104 $x520))) (rewrite (= (and $x104 $x520) $x528)) (= $x126 $x528))))
   336 (let ((@x535 (monotonicity (rewrite (= (< v_b_max_G_1$ ?x101) $x441)) @x532 (= $x127 (and $x441 $x528)))))
   337 (let ((@x543 (monotonicity @x242 (trans @x535 @x538 (= $x127 $x536)) (= $x128 (and $x55 $x536)))))
   338 (let ((@x551 (monotonicity (trans @x543 @x546 (= $x128 $x544)) (= $x129 (and true $x544)))))
   339 (let ((@x605 (monotonicity (trans @x551 (rewrite (= (and true $x544) $x544)) (= $x129 $x544)) (monotonicity @x574 @x599 (= $x141 $x600)) (= $x142 (=> $x544 $x600)))))
   340 (let ((@x677 (monotonicity (trans @x605 (rewrite (= (=> $x544 $x600) $x607)) (= $x142 $x607)) (trans @x668 (rewrite (= (=> $x654 $x600) $x670)) (= $x153 $x670)) (= (and $x142 $x153) $x675))))
   341 (let ((@x420 (monotonicity (rewrite (= (< v_b_p_G_0$ v_b_length$) $x415)) @x242 (= $x98 (and $x415 $x55)))))
   342 (let ((@x425 (trans @x420 (rewrite (= (and $x415 $x55) (and $x415 $x52 $x54))) (= $x98 (and $x415 $x52 $x54)))))
   343 (let ((@x433 (trans (monotonicity @x242 @x425 (= $x99 (and $x55 (and $x415 $x52 $x54)))) (rewrite (= (and $x55 (and $x415 $x52 $x54)) $x429)) (= $x99 $x429))))
   344 (let ((@x440 (trans (monotonicity @x433 (= $x100 (and true $x429))) (rewrite (= (and true $x429) $x429)) (= $x100 $x429))))
   345 (let ((@x686 (trans (monotonicity @x440 @x677 (= $x155 (=> $x429 $x675))) (rewrite (= (=> $x429 $x675) $x682)) (= $x155 $x682))))
   346 (let (($x89 (<= ?x46 v_b_max_G_4$)))
   347 (let (($x351 (not (<= v_b_length$ ?0))))
   348 (let (($x354 (and $x43 $x351)))
   349 (let (($x360 (not $x354)))
   350 (let (($x372 (or $x360 $x89)))
   351 (let (($x85 (and $x43 (< ?0 v_b_length$))))
   352 (let (($x90 (=> $x85 $x89)))
   353 (let ((@x356 (monotonicity @x212 (rewrite (= (< ?0 v_b_length$) $x351)) (= $x85 $x354))))
   354 (let ((@x376 (trans (monotonicity @x356 (= $x90 (=> $x354 $x89))) (rewrite (= (=> $x354 $x89) $x372)) (= $x90 $x372))))
   355 (let ((@x382 (monotonicity (quant-intro @x376 (= $x91 $x377)) (= $x92 (=> $x377 true)))))
   356 (let ((@x386 (trans @x382 (rewrite (= (=> $x377 true) true)) (= $x92 true))))
   357 (let ((@x389 (monotonicity (quant-intro @x376 (= $x91 $x377)) @x386 (= $x93 (and $x377 true)))))
   358 (let (($x86 (= ?x46 v_b_max_G_4$)))
   359 (let (($x361 (or $x360 $x86)))
   360 (let (($x87 (=> $x85 $x86)))
   361 (let ((@x365 (trans (monotonicity @x356 (= $x87 (=> $x354 $x86))) (rewrite (= (=> $x354 $x86) $x361)) (= $x87 $x361))))
   362 (let ((@x396 (monotonicity (quant-intro @x365 (= $x88 $x366)) (trans @x389 (rewrite (= (and $x377 true) $x377)) (= $x93 $x377)) (= $x94 (=> $x366 $x377)))))
   363 (let ((@x405 (monotonicity (quant-intro @x365 (= $x88 $x366)) (trans @x396 (rewrite (= (=> $x366 $x377) $x398)) (= $x94 $x398)) (= (and $x88 $x94) $x403))))
   364 (let (($x330 (and $x69 $x52 $x54 $x71 $x73 $x75)))
   365 (let (($x322 (and $x52 $x54 $x71 $x73 $x75)))
   366 (let ((@x316 (rewrite (= (and true (and $x71 $x73 $x75)) (and $x71 $x73 $x75)))))
   367 (let ((@x303 (monotonicity (rewrite (= (and $x75 true) $x75)) (= (and $x73 (and $x75 true)) (and $x73 $x75)))))
   368 (let ((@x311 (trans (monotonicity @x303 (= $x78 (and $x71 (and $x73 $x75)))) (rewrite (= (and $x71 (and $x73 $x75)) (and $x71 $x73 $x75))) (= $x78 (and $x71 $x73 $x75)))))
   369 (let ((@x318 (trans (monotonicity @x311 (= $x79 (and true (and $x71 $x73 $x75)))) @x316 (= $x79 (and $x71 $x73 $x75)))))
   370 (let ((@x326 (trans (monotonicity @x242 @x318 (= $x80 (and $x55 (and $x71 $x73 $x75)))) (rewrite (= (and $x55 (and $x71 $x73 $x75)) $x322)) (= $x80 $x322))))
   371 (let ((@x334 (trans (monotonicity @x326 (= $x81 (and $x69 $x322))) (rewrite (= (and $x69 $x322) $x330)) (= $x81 $x330))))
   372 (let ((@x342 (trans (monotonicity @x242 @x334 (= $x82 (and $x55 $x330))) (rewrite (= (and $x55 $x330) $x338)) (= $x82 $x338))))
   373 (let ((@x349 (trans (monotonicity @x342 (= $x83 (and true $x338))) (rewrite (= (and true $x338) $x338)) (= $x83 $x338))))
   374 (let ((@x414 (trans (monotonicity @x349 @x405 (= $x96 (=> $x338 $x403))) (rewrite (= (=> $x338 $x403) $x410)) (= $x96 $x410))))
   375 (let (($x279 (and $x52 $x54 $x259 $x63)))
   376 (let ((@x273 (rewrite (= (and $x259 (and $x63 $x52 $x54)) (and $x259 $x63 $x52 $x54)))))
   377 (let ((@x267 (trans (monotonicity @x242 (= $x64 $x64)) (rewrite (= $x64 (and $x63 $x52 $x54))) (= $x64 (and $x63 $x52 $x54)))))
   378 (let (($x59 (<= ?x46 v_b_max_G_1$)))
   379 (let (($x254 (or (not (and $x43 (not (<= v_b_p_G_0$ ?0)))) $x59)))
   380 (let (($x60 (=> (and $x43 (< ?0 v_b_p_G_0$)) $x59)))
   381 (let ((@x256 (rewrite (= (=> (and $x43 (not (<= v_b_p_G_0$ ?0))) $x59) $x254))))
   382 (let (($x244 (not (<= v_b_p_G_0$ ?0))))
   383 (let (($x247 (and $x43 $x244)))
   384 (let ((@x249 (monotonicity @x212 (rewrite (= (< ?0 v_b_p_G_0$) $x244)) (= (and $x43 (< ?0 v_b_p_G_0$)) $x247))))
   385 (let ((@x258 (trans (monotonicity @x249 (= $x60 (=> $x247 $x59))) @x256 (= $x60 $x254))))
   386 (let ((@x270 (monotonicity (quant-intro @x258 (= $x61 $x259)) @x267 (= $x65 (and $x259 (and $x63 $x52 $x54))))))
   387 (let ((@x278 (monotonicity @x242 (trans @x270 @x273 (= $x65 (and $x259 $x63 $x52 $x54))) (= $x66 (and $x55 (and $x259 $x63 $x52 $x54))))))
   388 (let ((@x283 (trans @x278 (rewrite (= (and $x55 (and $x259 $x63 $x52 $x54)) $x279)) (= $x66 $x279))))
   389 (let ((@x290 (trans (monotonicity @x283 (= $x67 (and true $x279))) (rewrite (= (and true $x279) $x279)) (= $x67 $x279))))
   390 (let ((@x298 (trans (monotonicity @x290 (= $x68 (and $x50 $x279))) (rewrite (= (and $x50 $x279) $x294)) (= $x68 $x294))))
   391 (let ((@x692 (monotonicity @x298 (monotonicity @x414 @x686 (= (and $x96 $x155) $x687)) (= $x157 (=> $x294 $x687)))))
   392 (let ((@x701 (monotonicity (trans @x692 (rewrite (= (=> $x294 $x687) $x694)) (= $x157 $x694)) (= (and $x50 $x157) $x699))))
   393 (let (($x47 (<= ?x46 v_b_max_G_0$)))
   394 (let (($x229 (or (not (and $x43 (not (<= 1 ?0)))) $x47)))
   395 (let (($x48 (=> (and $x43 (< ?0 1)) $x47)))
   396 (let ((@x220 (monotonicity (rewrite (= (<= 1 ?0) (<= 1 ?0))) (= (not (<= 1 ?0)) (not (<= 1 ?0))))))
   397 (let ((@x221 (trans (rewrite (= (< ?0 1) (not (<= 1 ?0)))) @x220 (= (< ?0 1) (not (<= 1 ?0))))))
   398 (let ((@x224 (monotonicity @x212 @x221 (= (and $x43 (< ?0 1)) (and $x43 (not (<= 1 ?0)))))))
   399 (let ((@x227 (monotonicity @x224 (= $x48 (=> (and $x43 (not (<= 1 ?0))) $x47)))))
   400 (let ((@x233 (trans @x227 (rewrite (= (=> (and $x43 (not (<= 1 ?0))) $x47) $x229)) (= $x48 $x229))))
   401 (let ((@x704 (monotonicity (quant-intro @x233 (= $x49 $x234)) @x701 (= $x159 (=> $x234 $x699)))))
   402 (let ((@x713 (monotonicity (quant-intro @x233 (= $x49 $x234)) (trans @x704 (rewrite (= (=> $x234 $x699) $x706)) (= $x159 $x706)) (= (and $x49 $x159) $x711))))
   403 (let ((@x176 (rewrite (= (and true true) true))))
   404 (let ((@x174 (monotonicity (rewrite (= $x34 true)) (rewrite (= $x34 true)) (= $x35 (and true true)))))
   405 (let ((@x180 (monotonicity (rewrite (= $x32 true)) (trans @x174 @x176 (= $x35 true)) (= $x36 (and true true)))))
   406 (let ((@x184 (monotonicity (rewrite (= $x32 true)) (trans @x180 @x176 (= $x36 true)) (= $x37 (and true true)))))
   407 (let ((@x189 (monotonicity (trans @x184 @x176 (= $x37 true)) (= $x38 (and $x31 true)))))
   408 (let ((@x196 (monotonicity (trans @x189 (rewrite (= (and $x31 true) $x31)) (= $x38 $x31)) (= $x39 (and true $x31)))))
   409 (let ((@x203 (monotonicity (rewrite (= (< 0 v_b_length$) (not (<= v_b_length$ 0)))) (trans @x196 (rewrite (= (and true $x31) $x31)) (= $x39 $x31)) (= (and (< 0 v_b_length$) $x39) $x201))))
   410 (let ((@x210 (trans (monotonicity @x203 (= $x41 (and true $x201))) (rewrite (= (and true $x201) $x201)) (= $x41 $x201))))
   411 (let ((@x722 (trans (monotonicity @x210 @x713 (= $x161 (=> $x201 $x711))) (rewrite (= (=> $x201 $x711) $x718)) (= $x161 $x718))))
   412 (let ((@x726 (mp (asserted $x162) (monotonicity @x722 (= $x162 (not $x718))) (not $x718))))
   413 (let ((@x737 (mp (and-elim (not-or-elim @x726 $x201) $x31) (rewrite* (= $x31 $x31)) $x31)))
   414 (let ((@x1930 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not (= v_b_max_G_0$ (v_b_array$ ?v0!2))) $x1083)) (unit-resolution (def-axiom (or $x1391 (not $x1083))) @x1966 (not $x1083)) (trans @x737 @x1955 (= v_b_max_G_0$ (v_b_array$ ?v0!2))) false)))
   415 (let (($x1582 (forall ((?v0 Int) )(let (($x1020 (<= (+ (v_b_array$ ?v0) (* (- 1) v_b_max_G_3$)) 0)))
   416 (let (($x1005 (>= (+ ?v0 (* (- 1) v_b_p_G_1$)) 0)))
   417 (let (($x838 (>= ?v0 0)))
   418 (let (($x1399 (not $x838)))
   419 (or $x1399 $x1005 $x1020))))))
   420 ))
   421 (let (($x1590 (not (or (not $x1582) $x136))))
   422 (let (($x1595 (or $x1560 $x1590)))
   423 (let (($x1607 (not $x1595)))
   424 (let (($x1620 (not (or $x1528 $x1529 $x985 (not $x144) (not $x145) $x1604 $x1605 $x1606 $x1607))))
   425 (let (($x1609 (not (or $x1528 $x1529 $x980 $x1601 $x1602 $x1603 $x1604 $x1605 $x1606 $x1607))))
   426 (let (($x1625 (or $x1609 $x1620)))
   427 (let (($x1633 (not (or $x1528 $x1529 $x919 (not $x1625)))))
   428 (let (($x1466 (forall ((?v0 Int) )(let ((?x46 (v_b_array$ ?v0)))
   429 (let (($x86 (= ?x46 v_b_max_G_4$)))
   430 (let (($x930 (<= (+ v_b_length$ (* (- 1) ?v0)) 0)))
   431 (let (($x838 (>= ?v0 0)))
   432 (let (($x1399 (not $x838)))
   433 (let (($x1458 (or $x1399 $x930 $x86)))
   434 (not $x1458))))))))
   435 ))
   436 (let (($x1522 (or $x1466 $x1517)))
   437 (let (($x1535 (not (or $x1528 $x1529 $x971 (not k!00) $x1531 (not k!10) (not $x1522)))))
   438 (let (($x1638 (or $x1535 $x1633)))
   439 (let (($x1441 (forall ((?v0 Int) )(let (($x903 (<= (+ (v_b_array$ ?v0) (* (- 1) v_b_max_G_1$)) 0)))
   440 (let (($x888 (>= (+ ?v0 (* (- 1) v_b_p_G_0$)) 0)))
   441 (let (($x838 (>= ?v0 0)))
   442 (let (($x1399 (not $x838)))
   443 (or $x1399 $x888 $x903))))))
   444 ))
   445 (let (($x1648 (not (or $x1528 $x1529 (not $x1441) (not $x63) (not $x1638)))))
   446 (let (($x1653 (or $x1095 $x1648)))
   447 (let (($x1419 (forall ((?v0 Int) )(let (($x851 (>= (+ v_b_max_G_0$ (* (- 1) (v_b_array$ ?v0))) 0)))
   448 (let (($x841 (>= ?v0 1)))
   449 (let (($x838 (>= ?v0 0)))
   450 (let (($x1399 (not $x838)))
   451 (or $x1399 $x841 $x851))))))
   452 ))
   453 (let (($x1662 (not (or (not $x1419) (not $x1653)))))
   454 (let (($x1667 (or $x1396 $x1662)))
   455 (let (($x2147 (= (or $x1528 $x1529 $x985 (not $x144) (not $x145) $x1604 $x1605 $x1606 $x1607) $x2146)))
   456 (let (($x1020 (<= (+ ?x46 (* (- 1) v_b_max_G_3$)) 0)))
   457 (let (($x1005 (>= (+ ?0 (* (- 1) v_b_p_G_1$)) 0)))
   458 (let (($x838 (>= ?0 0)))
   459 (let (($x1399 (not $x838)))
   460 (let (($x1577 (or $x1399 $x1005 $x1020)))
   461 (let ((@x2127 (monotonicity (quant-intro (refl (= $x1577 $x1577)) (= $x1582 $x2120)) (= (not $x1582) (not $x2120)))))
   462 (let ((@x2133 (monotonicity (monotonicity @x2127 (= (or (not $x1582) $x136) $x2128)) (= $x1590 $x2131))))
   463 (let ((@x2148 (monotonicity (monotonicity (monotonicity @x2133 (= $x1595 $x2134)) (= $x1607 $x2137)) $x2147)))
   464 (let ((@x2142 (monotonicity (monotonicity (monotonicity @x2133 (= $x1595 $x2134)) (= $x1607 $x2137)) (= (or $x1528 $x1529 $x980 $x1601 $x1602 $x1603 $x1604 $x1605 $x1606 $x1607) $x2140))))
   465 (let ((@x2154 (monotonicity (monotonicity @x2142 (= $x1609 $x2143)) (monotonicity @x2148 (= $x1620 $x2149)) (= $x1625 $x2152))))
   466 (let ((@x2160 (monotonicity (monotonicity @x2154 (= (not $x1625) $x2155)) (= (or $x1528 $x1529 $x919 (not $x1625)) $x2158))))
   467 (let (($x2115 (= (or $x1528 $x1529 $x971 (not k!00) $x1531 (not k!10) (not $x1522)) $x2114)))
   468 (let (($x930 (<= (+ v_b_length$ (* (- 1) ?0)) 0)))
   469 (let (($x1458 (or $x1399 $x930 $x86)))
   470 (let (($x1463 (not $x1458)))
   471 (let ((@x2110 (monotonicity (quant-intro (refl (= $x1463 $x1463)) (= $x1466 $x2103)) (= $x1522 $x2108))))
   472 (let ((@x2119 (monotonicity (monotonicity (monotonicity @x2110 (= (not $x1522) $x2111)) $x2115) (= $x1535 $x2117))))
   473 (let ((@x2166 (monotonicity @x2119 (monotonicity @x2160 (= $x1633 $x2161)) (= $x1638 $x2164))))
   474 (let (($x903 (<= (+ ?x46 (* (- 1) v_b_max_G_1$)) 0)))
   475 (let (($x888 (>= (+ ?0 (* (- 1) v_b_p_G_0$)) 0)))
   476 (let (($x1436 (or $x1399 $x888 $x903)))
   477 (let ((@x2102 (monotonicity (quant-intro (refl (= $x1436 $x1436)) (= $x1441 $x2095)) (= (not $x1441) $x2100))))
   478 (let ((@x2172 (monotonicity @x2102 (monotonicity @x2166 (= (not $x1638) $x2167)) (= (or $x1528 $x1529 (not $x1441) (not $x63) (not $x1638)) $x2170))))
   479 (let ((@x2181 (monotonicity (monotonicity (monotonicity @x2172 (= $x1648 $x2173)) (= $x1653 $x2176)) (= (not $x1653) $x2179))))
   480 (let (($x851 (>= (+ v_b_max_G_0$ (* (- 1) ?x46)) 0)))
   481 (let (($x841 (>= ?0 1)))
   482 (let (($x1414 (or $x1399 $x841 $x851)))
   483 (let ((@x2094 (monotonicity (quant-intro (refl (= $x1414 $x1414)) (= $x1419 $x2087)) (= (not $x1419) (not $x2087)))))
   484 (let ((@x2187 (monotonicity (monotonicity @x2094 @x2181 (= (or (not $x1419) (not $x1653)) $x2182)) (= $x1662 $x2185))))
   485 (let (($x1193 (not $x136)))
   486 (let (($x1026 (forall ((?v0 Int) )(let (($x1020 (<= (+ (v_b_array$ ?v0) (* (- 1) v_b_max_G_3$)) 0)))
   487 (let (($x838 (>= ?v0 0)))
   488 (let (($x1012 (and $x838 (not (>= (+ ?v0 (* (- 1) v_b_p_G_1$)) 0)))))
   489 (let (($x1015 (not $x1012)))
   490 (or $x1015 $x1020))))))
   491 ))
   492 (let (($x1196 (and $x1026 $x1193)))
   493 (let (($x1295 (not $x1290)))
   494 (let (($x1298 (and $x1173 $x1295)))
   495 (let (($x1301 (not $x1298)))
   496 (let (($x1317 (or $x1301 $x1312)))
   497 (let (($x1320 (not $x1317)))
   498 (let (($x1323 (or $x1320 $x1196)))
   499 (let (($x1339 (and $x882 $x885 $x980 $x144 $x145 $x989 $x991 $x996 $x1323)))
   500 (let (($x1329 (and $x882 $x885 $x985 $x104 $x107 $x109 $x989 $x991 $x996 $x1323)))
   501 (let (($x1344 (or $x1329 $x1339)))
   502 (let (($x1350 (and $x882 $x885 $x971 $x1344)))
   503 (let (($x1145 (not (and $x1139 (not $x1142)))))
   504 (let (($x1258 (or $x1145 $x1253)))
   505 (let (($x1261 (not $x1258)))
   506 (let (($x1129 (not (and (>= ?v0!3 0) (not $x1126)))))
   507 (let (($x1132 (or $x1129 $x1131)))
   508 (let (($x1264 (and $x1132 $x1261)))
   509 (let (($x1119 (forall ((?v0 Int) )(let ((?x46 (v_b_array$ ?v0)))
   510 (let (($x86 (= ?x46 v_b_max_G_4$)))
   511 (let (($x838 (>= ?v0 0)))
   512 (let (($x936 (and $x838 (not (<= (+ v_b_length$ (* (- 1) ?v0)) 0)))))
   513 (let (($x939 (not $x936)))
   514 (let (($x942 (or $x939 $x86)))
   515 (not $x942))))))))
   516 ))
   517 (let (($x1267 (or $x1119 $x1264)))
   518 (let (($x1273 (and $x882 $x885 $x919 k!00 $x73 k!10 $x1267)))
   519 (let (($x1355 (or $x1273 $x1350)))
   520 (let (($x909 (forall ((?v0 Int) )(let (($x903 (<= (+ (v_b_array$ ?v0) (* (- 1) v_b_max_G_1$)) 0)))
   521 (let (($x838 (>= ?v0 0)))
   522 (let (($x895 (and $x838 (not (>= (+ ?v0 (* (- 1) v_b_p_G_0$)) 0)))))
   523 (let (($x898 (not $x895)))
   524 (or $x898 $x903))))))
   525 ))
   526 (let (($x1361 (and $x882 $x885 $x909 $x63 $x1355)))
   527 (let (($x1366 (or $x1095 $x1361)))
   528 (let (($x862 (forall ((?v0 Int) )(let (($x851 (>= (+ v_b_max_G_0$ (* (- 1) (v_b_array$ ?v0))) 0)))
   529 (let (($x838 (>= ?v0 0)))
   530 (let (($x849 (and $x838 (not (>= ?v0 1)))))
   531 (let (($x854 (not $x849)))
   532 (or $x854 $x851))))))
   533 ))
   534 (let (($x1369 (and $x862 $x1366)))
   535 (let (($x1077 (not (and $x1078 $x1079))))
   536 (let (($x1084 (or $x1077 $x1083)))
   537 (let (($x1085 (not $x1084)))
   538 (let (($x1372 (or $x1085 $x1369)))
   539 (let ((@x1622 (rewrite (= (and $x882 $x885 $x980 $x144 $x145 $x989 $x991 $x996 $x1595) $x1620))))
   540 (let (($x1012 (and $x838 (not $x1005))))
   541 (let (($x1015 (not $x1012)))
   542 (let (($x1023 (or $x1015 $x1020)))
   543 (let ((@x1569 (monotonicity (rewrite (= $x1012 (not (or $x1399 $x1005)))) (= $x1015 (not (not (or $x1399 $x1005)))))))
   544 (let ((@x1573 (trans @x1569 (rewrite (= (not (not (or $x1399 $x1005))) (or $x1399 $x1005))) (= $x1015 (or $x1399 $x1005)))))
   545 (let ((@x1581 (trans (monotonicity @x1573 (= $x1023 (or (or $x1399 $x1005) $x1020))) (rewrite (= (or (or $x1399 $x1005) $x1020) $x1577)) (= $x1023 $x1577))))
   546 (let ((@x1587 (monotonicity (quant-intro @x1581 (= $x1026 $x1582)) (= $x1196 (and $x1582 $x1193)))))
   547 (let ((@x1547 (monotonicity (rewrite (= $x1298 (not (or $x1540 $x1290)))) (= $x1301 (not (not (or $x1540 $x1290)))))))
   548 (let ((@x1551 (trans @x1547 (rewrite (= (not (not (or $x1540 $x1290))) (or $x1540 $x1290))) (= $x1301 (or $x1540 $x1290)))))
   549 (let ((@x1559 (trans (monotonicity @x1551 (= $x1317 (or (or $x1540 $x1290) $x1312))) (rewrite (= (or (or $x1540 $x1290) $x1312) $x1555)) (= $x1317 $x1555))))
   550 (let ((@x1597 (monotonicity (monotonicity @x1559 (= $x1320 $x1560)) (trans @x1587 (rewrite (= (and $x1582 $x1193) $x1590)) (= $x1196 $x1590)) (= $x1323 $x1595))))
   551 (let ((@x1616 (monotonicity @x1597 (= $x1339 (and $x882 $x885 $x980 $x144 $x145 $x989 $x991 $x996 $x1595)))))
   552 (let ((@x1611 (rewrite (= (and $x882 $x885 $x985 $x104 $x107 $x109 $x989 $x991 $x996 $x1595) $x1609))))
   553 (let ((@x1600 (monotonicity @x1597 (= $x1329 (and $x882 $x885 $x985 $x104 $x107 $x109 $x989 $x991 $x996 $x1595)))))
   554 (let ((@x1627 (monotonicity (trans @x1600 @x1611 (= $x1329 $x1609)) (trans @x1616 @x1622 (= $x1339 $x1620)) (= $x1344 $x1625))))
   555 (let ((@x1637 (trans (monotonicity @x1627 (= $x1350 (and $x882 $x885 $x971 $x1625))) (rewrite (= (and $x882 $x885 $x971 $x1625) $x1633)) (= $x1350 $x1633))))
   556 (let ((@x1537 (rewrite (= (and $x882 $x885 $x919 k!00 $x73 k!10 $x1522) $x1535))))
   557 (let ((@x1496 (monotonicity (rewrite (= (and $x1139 (not $x1142)) (not (or $x1489 $x1142)))) (= $x1145 (not (not (or $x1489 $x1142)))))))
   558 (let ((@x1500 (trans @x1496 (rewrite (= (not (not (or $x1489 $x1142))) (or $x1489 $x1142))) (= $x1145 (or $x1489 $x1142)))))
   559 (let ((@x1508 (trans (monotonicity @x1500 (= $x1258 (or (or $x1489 $x1142) $x1253))) (rewrite (= (or (or $x1489 $x1142) $x1253) (or $x1489 $x1142 $x1253))) (= $x1258 (or $x1489 $x1142 $x1253)))))
   560 (let (($x1470 (or (not (>= ?v0!3 0)) $x1126)))
   561 (let ((@x1476 (monotonicity (rewrite (= (and (>= ?v0!3 0) (not $x1126)) (not $x1470))) (= $x1129 (not (not $x1470))))))
   562 (let ((@x1483 (monotonicity (trans @x1476 (rewrite (= (not (not $x1470)) $x1470)) (= $x1129 $x1470)) (= $x1132 (or $x1470 $x1131)))))
   563 (let ((@x1514 (monotonicity (trans @x1483 (rewrite (= (or $x1470 $x1131) $x1484)) (= $x1132 $x1484)) (monotonicity @x1508 (= $x1261 (not (or $x1489 $x1142 $x1253)))) (= $x1264 (and $x1484 (not (or $x1489 $x1142 $x1253)))))))
   564 (let ((@x1521 (trans @x1514 (rewrite (= (and $x1484 (not (or $x1489 $x1142 $x1253))) $x1517)) (= $x1264 $x1517))))
   565 (let (($x936 (and $x838 (not $x930))))
   566 (let (($x939 (not $x936)))
   567 (let (($x942 (or $x939 $x86)))
   568 (let ((@x1450 (monotonicity (rewrite (= $x936 (not (or $x1399 $x930)))) (= $x939 (not (not (or $x1399 $x930)))))))
   569 (let ((@x1454 (trans @x1450 (rewrite (= (not (not (or $x1399 $x930))) (or $x1399 $x930))) (= $x939 (or $x1399 $x930)))))
   570 (let ((@x1462 (trans (monotonicity @x1454 (= $x942 (or (or $x1399 $x930) $x86))) (rewrite (= (or (or $x1399 $x930) $x86) $x1458)) (= $x942 $x1458))))
   571 (let ((@x1468 (quant-intro (monotonicity @x1462 (= (not $x942) $x1463)) (= $x1119 $x1466))))
   572 (let ((@x1527 (monotonicity (monotonicity @x1468 @x1521 (= $x1267 $x1522)) (= $x1273 (and $x882 $x885 $x919 k!00 $x73 k!10 $x1522)))))
   573 (let (($x895 (and $x838 (not $x888))))
   574 (let (($x898 (not $x895)))
   575 (let (($x906 (or $x898 $x903)))
   576 (let ((@x1428 (monotonicity (rewrite (= $x895 (not (or $x1399 $x888)))) (= $x898 (not (not (or $x1399 $x888)))))))
   577 (let ((@x1432 (trans @x1428 (rewrite (= (not (not (or $x1399 $x888))) (or $x1399 $x888))) (= $x898 (or $x1399 $x888)))))
   578 (let ((@x1440 (trans (monotonicity @x1432 (= $x906 (or (or $x1399 $x888) $x903))) (rewrite (= (or (or $x1399 $x888) $x903) $x1436)) (= $x906 $x1436))))
   579 (let ((@x1643 (monotonicity (quant-intro @x1440 (= $x909 $x1441)) (monotonicity (trans @x1527 @x1537 (= $x1273 $x1535)) @x1637 (= $x1355 $x1638)) (= $x1361 (and $x882 $x885 $x1441 $x63 $x1638)))))
   580 (let ((@x1652 (trans @x1643 (rewrite (= (and $x882 $x885 $x1441 $x63 $x1638) $x1648)) (= $x1361 $x1648))))
   581 (let (($x849 (and $x838 (not $x841))))
   582 (let (($x854 (not $x849)))
   583 (let (($x859 (or $x854 $x851)))
   584 (let ((@x1406 (monotonicity (rewrite (= $x849 (not (or $x1399 $x841)))) (= $x854 (not (not (or $x1399 $x841)))))))
   585 (let ((@x1410 (trans @x1406 (rewrite (= (not (not (or $x1399 $x841))) (or $x1399 $x841))) (= $x854 (or $x1399 $x841)))))
   586 (let ((@x1418 (trans (monotonicity @x1410 (= $x859 (or (or $x1399 $x841) $x851))) (rewrite (= (or (or $x1399 $x841) $x851) $x1414)) (= $x859 $x1414))))
   587 (let ((@x1658 (monotonicity (quant-intro @x1418 (= $x862 $x1419)) (monotonicity @x1652 (= $x1366 $x1653)) (= $x1369 (and $x1419 $x1653)))))
   588 (let ((@x1385 (rewrite (= (not (not (or (not $x1078) $x831))) (or (not $x1078) $x831)))))
   589 (let ((@x1383 (monotonicity (rewrite (= (and $x1078 $x1079) (not (or (not $x1078) $x831)))) (= $x1077 (not (not (or (not $x1078) $x831)))))))
   590 (let ((@x1390 (monotonicity (trans @x1383 @x1385 (= $x1077 (or (not $x1078) $x831))) (= $x1084 (or (or (not $x1078) $x831) $x1083)))))
   591 (let ((@x1395 (trans @x1390 (rewrite (= (or (or (not $x1078) $x831) $x1083) $x1391)) (= $x1084 $x1391))))
   592 (let ((@x1669 (monotonicity (monotonicity @x1395 (= $x1085 $x1396)) (trans @x1658 (rewrite (= (and $x1419 $x1653) $x1662)) (= $x1369 $x1662)) (= $x1372 $x1667))))
   593 (let (($x1181 (<= (+ ?x1179 (* (- 1) v_b_max_G_3$)) 0)))
   594 (let (($x1182 (or (not (and $x1173 (not (>= (+ ?v0!5 (* (- 1) v_b_p_G_1$)) 0)))) $x1181)))
   595 (let (($x1183 (not $x1182)))
   596 (let (($x1200 (or $x1183 $x1196)))
   597 (let (($x1041 (and $x882 $x885 $x980 $x144 $x145 $x989 $x991 $x996)))
   598 (let (($x1044 (not $x1041)))
   599 (let (($x1208 (not $x1044)))
   600 (let (($x1211 (and $x1208 $x1200)))
   601 (let (($x999 (and $x882 $x885 $x985 $x104 $x107 $x109 $x989 $x991 $x996)))
   602 (let (($x1002 (not $x999)))
   603 (let (($x1169 (not $x1002)))
   604 (let (($x1204 (and $x1169 $x1200)))
   605 (let (($x1215 (or $x1204 $x1211)))
   606 (let (($x974 (and $x882 $x885 $x971)))
   607 (let (($x977 (not $x974)))
   608 (let (($x1166 (not $x977)))
   609 (let (($x1219 (and $x1166 $x1215)))
   610 (let (($x1150 (not (or $x1145 (<= (+ (v_b_array$ ?v0!4) (* (- 1) v_b_max_G_4$)) 0)))))
   611 (let (($x1154 (and $x1132 $x1150)))
   612 (let (($x1158 (or $x1119 $x1154)))
   613 (let (($x922 (and $x882 $x885 $x919 k!00 $x73 k!10)))
   614 (let (($x925 (not $x922)))
   615 (let (($x1113 (not $x925)))
   616 (let (($x1162 (and $x1113 $x1158)))
   617 (let (($x1223 (or $x1162 $x1219)))
   618 (let (($x912 (and $x882 $x885 $x909 $x63)))
   619 (let (($x1227 (and $x912 $x1223)))
   620 (let (($x1231 (or $x1095 $x1227)))
   621 (let (($x1235 (and $x862 $x1231)))
   622 (let (($x1239 (or $x1085 $x1235)))
   623 (let (($x1305 (= (+ ?x1179 (* (- 1) v_b_max_G_3$)) (+ (* (- 1) v_b_max_G_3$) ?x1179))))
   624 (let ((@x1309 (monotonicity (rewrite $x1305) (= $x1181 (<= (+ (* (- 1) v_b_max_G_3$) ?x1179) 0)))))
   625 (let ((@x1316 (trans @x1309 (rewrite (= (<= (+ (* (- 1) v_b_max_G_3$) ?x1179) 0) $x1312)) (= $x1181 $x1312))))
   626 (let (($x1302 (= (not (and $x1173 (not (>= (+ ?v0!5 (* (- 1) v_b_p_G_1$)) 0)))) $x1301)))
   627 (let (($x1299 (= (and $x1173 (not (>= (+ ?v0!5 (* (- 1) v_b_p_G_1$)) 0))) $x1298)))
   628 (let (($x1175 (>= (+ ?v0!5 (* (- 1) v_b_p_G_1$)) 0)))
   629 (let (($x1283 (= (+ ?v0!5 (* (- 1) v_b_p_G_1$)) (+ (* (- 1) v_b_p_G_1$) ?v0!5))))
   630 (let ((@x1287 (monotonicity (rewrite $x1283) (= $x1175 (>= (+ (* (- 1) v_b_p_G_1$) ?v0!5) 0)))))
   631 (let ((@x1294 (trans @x1287 (rewrite (= (>= (+ (* (- 1) v_b_p_G_1$) ?v0!5) 0) $x1290)) (= $x1175 $x1290))))
   632 (let ((@x1303 (monotonicity (monotonicity (monotonicity @x1294 (= (not $x1175) $x1295)) $x1299) $x1302)))
   633 (let ((@x1322 (monotonicity (monotonicity @x1303 @x1316 (= $x1182 $x1317)) (= $x1183 $x1320))))
   634 (let ((@x1338 (monotonicity (rewrite (= $x1208 $x1041)) (monotonicity @x1322 (= $x1200 $x1323)) (= $x1211 (and $x1041 $x1323)))))
   635 (let ((@x1328 (monotonicity (rewrite (= $x1169 $x999)) (monotonicity @x1322 (= $x1200 $x1323)) (= $x1204 (and $x999 $x1323)))))
   636 (let ((@x1346 (monotonicity (trans @x1328 (rewrite (= (and $x999 $x1323) $x1329)) (= $x1204 $x1329)) (trans @x1338 (rewrite (= (and $x1041 $x1323) $x1339)) (= $x1211 $x1339)) (= $x1215 $x1344))))
   637 (let ((@x1349 (monotonicity (rewrite (= $x1166 $x974)) @x1346 (= $x1219 (and $x974 $x1344)))))
   638 (let (($x1259 (= (or $x1145 (<= (+ (v_b_array$ ?v0!4) (* (- 1) v_b_max_G_4$)) 0)) $x1258)))
   639 (let (($x1148 (<= (+ (v_b_array$ ?v0!4) (* (- 1) v_b_max_G_4$)) 0)))
   640 (let (($x1254 (= (<= (+ (* (- 1) v_b_max_G_4$) (v_b_array$ ?v0!4)) 0) $x1253)))
   641 (let (($x1249 (= $x1148 (<= (+ (* (- 1) v_b_max_G_4$) (v_b_array$ ?v0!4)) 0))))
   642 (let (($x1246 (= (+ (v_b_array$ ?v0!4) (* (- 1) v_b_max_G_4$)) (+ (* (- 1) v_b_max_G_4$) (v_b_array$ ?v0!4)))))
   643 (let ((@x1257 (trans (monotonicity (rewrite $x1246) $x1249) (rewrite $x1254) (= $x1148 $x1253))))
   644 (let ((@x1266 (monotonicity (monotonicity (monotonicity @x1257 $x1259) (= $x1150 $x1261)) (= $x1154 $x1264))))
   645 (let ((@x1272 (monotonicity (rewrite (= $x1113 $x922)) (monotonicity @x1266 (= $x1158 $x1267)) (= $x1162 (and $x922 $x1267)))))
   646 (let ((@x1357 (monotonicity (trans @x1272 (rewrite (= (and $x922 $x1267) $x1273)) (= $x1162 $x1273)) (trans @x1349 (rewrite (= (and $x974 $x1344) $x1350)) (= $x1219 $x1350)) (= $x1223 $x1355))))
   647 (let ((@x1365 (trans (monotonicity @x1357 (= $x1227 (and $x912 $x1355))) (rewrite (= (and $x912 $x1355) $x1361)) (= $x1227 $x1361))))
   648 (let ((@x1374 (monotonicity (monotonicity (monotonicity @x1365 (= $x1231 $x1366)) (= $x1235 $x1369)) (= $x1239 $x1372))))
   649 (let (($x1029 (not $x1026)))
   650 (let (($x1032 (or $x1029 $x136)))
   651 (let (($x1035 (and $x1026 $x1032)))
   652 (let (($x1047 (or $x1044 $x1035)))
   653 (let (($x1038 (or $x1002 $x1035)))
   654 (let (($x1050 (and $x1038 $x1047)))
   655 (let (($x1053 (or $x977 $x1050)))
   656 (let (($x959 (forall ((?v0 Int) )(let (($x838 (>= ?v0 0)))
   657 (let (($x936 (and $x838 (not (<= (+ v_b_length$ (* (- 1) ?v0)) 0)))))
   658 (let (($x939 (not $x936)))
   659 (or $x939 (<= (+ (v_b_array$ ?v0) (* (- 1) v_b_max_G_4$)) 0))))))
   660 ))
   661 (let (($x945 (exists ((?v0 Int) )(let ((?x46 (v_b_array$ ?v0)))
   662 (let (($x86 (= ?x46 v_b_max_G_4$)))
   663 (let (($x838 (>= ?v0 0)))
   664 (let (($x936 (and $x838 (not (<= (+ v_b_length$ (* (- 1) ?v0)) 0)))))
   665 (let (($x939 (not $x936)))
   666 (or $x939 $x86)))))))
   667 ))
   668 (let (($x948 (not $x945)))
   669 (let (($x962 (or $x948 $x959)))
   670 (let (($x965 (and $x945 $x962)))
   671 (let (($x968 (or $x925 $x965)))
   672 (let (($x1056 (and $x968 $x1053)))
   673 (let (($x915 (not $x912)))
   674 (let (($x1059 (or $x915 $x1056)))
   675 (let (($x1062 (and $x50 $x1059)))
   676 (let (($x878 (not $x862)))
   677 (let (($x1065 (or $x878 $x1062)))
   678 (let (($x1071 (not (and $x862 $x1065))))
   679 (let ((@x1192 (nnf-neg (nnf-pos (refl (~ $x1023 $x1023)) (~ $x1026 $x1026)) (~ (not $x1029) $x1026))))
   680 (let ((@x1203 (nnf-neg (sk (~ $x1029 $x1183)) (nnf-neg @x1192 (refl (~ $x1193 $x1193)) (~ (not $x1032) $x1196)) (~ (not $x1035) $x1200))))
   681 (let ((@x1218 (nnf-neg (nnf-neg (refl (~ $x1169 $x1169)) @x1203 (~ (not $x1038) $x1204)) (nnf-neg (refl (~ $x1208 $x1208)) @x1203 (~ (not $x1047) $x1211)) (~ (not $x1050) $x1215))))
   682 (let ((@x1157 (nnf-neg (nnf-neg (sk (~ $x945 $x1132)) (~ (not $x948) $x1132)) (sk (~ (not $x959) $x1150)) (~ (not $x962) $x1154))))
   683 (let ((@x1161 (nnf-neg (nnf-neg (refl (~ (not $x942) (not $x942))) (~ $x948 $x1119)) @x1157 (~ (not $x965) $x1158))))
   684 (let ((@x1226 (nnf-neg (nnf-neg (refl (~ $x1113 $x1113)) @x1161 (~ (not $x968) $x1162)) (nnf-neg (refl (~ $x1166 $x1166)) @x1218 (~ (not $x1053) $x1219)) (~ (not $x1056) $x1223))))
   685 (let ((@x1109 (monotonicity (refl (~ $x882 $x882)) (refl (~ $x885 $x885)) (nnf-pos (refl (~ $x906 $x906)) (~ $x909 $x909)) (refl (~ $x63 $x63)) (~ $x912 $x912))))
   686 (let ((@x1230 (nnf-neg (nnf-neg @x1109 (~ (not $x915) $x912)) @x1226 (~ (not $x1059) $x1227))))
   687 (let ((@x1094 (nnf-neg (nnf-pos (refl (~ $x859 $x859)) (~ $x862 $x862)) (~ (not $x878) $x862))))
   688 (let ((@x1238 (nnf-neg @x1094 (nnf-neg (refl (~ $x1095 $x1095)) @x1230 (~ (not $x1062) $x1231)) (~ (not $x1065) $x1235))))
   689 (let (($x749 (and $x52 $x54 $x69 k!00 $x73 k!10)))
   690 (let (($x752 (not $x749)))
   691 (let (($x785 (or $x752 $x403)))
   692 (let (($x788 (and $x785 $x682)))
   693 (let (($x738 (not $x279)))
   694 (let (($x816 (or $x738 $x788)))
   695 (let (($x819 (and $x50 $x816)))
   696 (let (($x822 (or $x705 $x819)))
   697 (let (($x825 (and $x234 $x822)))
   698 (let (($x828 (not $x825)))
   699 (let ((@x1011 (monotonicity (rewrite (= (<= v_b_p_G_1$ ?0) $x1005)) (= $x557 (not $x1005)))))
   700 (let ((@x837 (rewrite (= $x43 $x838))))
   701 (let ((@x1017 (monotonicity (monotonicity @x837 @x1011 (= $x560 $x1012)) (= (not $x560) $x1015))))
   702 (let ((@x1028 (quant-intro (monotonicity @x1017 (rewrite (= $x132 $x1020)) (= $x567 $x1023)) (= $x572 $x1026))))
   703 (let ((@x1034 (monotonicity (monotonicity @x1028 (= (not $x572) $x1029)) (= $x595 $x1032))))
   704 (let ((@x886 (rewrite (= $x54 $x885))))
   705 (let ((@x883 (rewrite (= $x52 $x882))))
   706 (let ((@x1043 (monotonicity @x883 @x886 (rewrite (= $x143 $x980)) (rewrite (= $x110 $x989)) (rewrite (= $x456 $x991)) (rewrite (= $x116 $x996)) (= $x654 $x1041))))
   707 (let ((@x1049 (monotonicity (monotonicity @x1043 (= $x669 $x1044)) (monotonicity @x1028 @x1034 (= $x600 $x1035)) (= $x670 $x1047))))
   708 (let ((@x1001 (monotonicity @x883 @x886 (monotonicity (rewrite (= $x143 $x980)) (= $x441 $x985)) (rewrite (= $x110 $x989)) (rewrite (= $x456 $x991)) (rewrite (= $x116 $x996)) (= $x544 $x999))))
   709 (let ((@x1040 (monotonicity (monotonicity @x1001 (= $x606 $x1002)) (monotonicity @x1028 @x1034 (= $x600 $x1035)) (= $x607 $x1038))))
   710 (let ((@x976 (monotonicity @x883 @x886 (monotonicity (rewrite (= $x69 $x919)) (= $x415 $x971)) (= $x429 $x974))))
   711 (let ((@x1055 (monotonicity (monotonicity @x976 (= $x681 $x977)) (monotonicity @x1040 @x1049 (= $x675 $x1050)) (= $x682 $x1053))))
   712 (let ((@x935 (monotonicity (rewrite (= (<= v_b_length$ ?0) $x930)) (= $x351 (not $x930)))))
   713 (let ((@x941 (monotonicity (monotonicity @x837 @x935 (= $x354 $x936)) (= $x360 $x939))))
   714 (let ((@x958 (monotonicity @x941 (rewrite (= $x89 (<= (+ ?x46 (* (- 1) v_b_max_G_4$)) 0))) (= $x372 (or $x939 (<= (+ ?x46 (* (- 1) v_b_max_G_4$)) 0))))))
   715 (let ((@x950 (monotonicity (quant-intro (monotonicity @x941 (= $x361 $x942)) (= $x366 $x945)) (= (not $x366) $x948))))
   716 (let ((@x967 (monotonicity (quant-intro (monotonicity @x941 (= $x361 $x942)) (= $x366 $x945)) (monotonicity @x950 (quant-intro @x958 (= $x377 $x959)) (= $x398 $x962)) (= $x403 $x965))))
   717 (let ((@x927 (monotonicity (monotonicity @x883 @x886 (rewrite (= $x69 $x919)) (= $x749 $x922)) (= $x752 $x925))))
   718 (let ((@x1058 (monotonicity (monotonicity @x927 @x967 (= $x785 $x968)) @x1055 (= $x788 $x1056))))
   719 (let ((@x894 (monotonicity (rewrite (= (<= v_b_p_G_0$ ?0) $x888)) (= $x244 (not $x888)))))
   720 (let ((@x900 (monotonicity (monotonicity @x837 @x894 (= $x247 $x895)) (= (not $x247) $x898))))
   721 (let ((@x911 (quant-intro (monotonicity @x900 (rewrite (= $x59 $x903)) (= $x254 $x906)) (= $x259 $x909))))
   722 (let ((@x917 (monotonicity (monotonicity @x883 @x886 @x911 (= $x279 $x912)) (= $x738 $x915))))
   723 (let ((@x1064 (monotonicity (monotonicity @x917 @x1058 (= $x816 $x1059)) (= $x819 $x1062))))
   724 (let ((@x848 (monotonicity (rewrite (= (<= 1 ?0) $x841)) (= (not (<= 1 ?0)) (not $x841)))))
   725 (let ((@x834 (monotonicity (monotonicity @x837 @x848 (= (and $x43 (not (<= 1 ?0))) $x849)) (= (not (and $x43 (not (<= 1 ?0)))) $x854))))
   726 (let ((@x877 (quant-intro (monotonicity @x834 (rewrite (= $x47 $x851)) (= $x229 $x859)) (= $x234 $x862))))
   727 (let ((@x1067 (monotonicity (monotonicity @x877 (= $x705 $x878)) @x1064 (= $x822 $x1065))))
   728 (let ((@x1073 (monotonicity (monotonicity @x877 @x1067 (= $x825 (and $x862 $x1065))) (= $x828 $x1071))))
   729 (let ((@x796 (monotonicity (monotonicity @x238 @x240 @x450 @x460 @x463 (= $x654 $x654)) (= $x669 $x669))))
   730 (let ((@x784 (monotonicity (monotonicity @x238 @x240 @x450 @x460 @x463 (= $x544 $x544)) (= $x606 $x606))))
   731 (let ((@x800 (monotonicity (monotonicity @x784 (= $x607 $x607)) (monotonicity @x796 (= $x670 $x670)) (= $x675 $x675))))
   732 (let ((@x780 (monotonicity (monotonicity @x238 @x240 (= $x429 $x429)) (= $x681 $x681))))
   733 (let ((@x846 (monotonicity (monotonicity @x238 @x240 (= $x749 $x749)) (= $x752 $x752))))
   734 (let ((@x864 (monotonicity (monotonicity @x846 (= $x785 $x785)) (monotonicity @x780 @x800 (= $x682 $x682)) (= $x788 $x788))))
   735 (let ((@x762 (monotonicity (monotonicity @x238 @x240 (= $x279 $x279)) (= $x738 $x738))))
   736 (let ((@x868 (monotonicity (monotonicity @x762 @x864 (= $x816 $x816)) (= $x819 $x819))))
   737 (let ((@x874 (monotonicity (monotonicity (monotonicity @x868 (= $x822 $x822)) (= $x825 $x825)) (= $x828 $x828))))
   738 (let ((@x751 (monotonicity (apply-def (intro-def (= $x71 k!00)) (~ $x71 k!00)) (apply-def (intro-def (= $x75 k!10)) (~ $x75 k!10)) (= $x338 $x749))))
   739 (let ((@x790 (monotonicity (monotonicity (monotonicity @x751 (= $x409 $x752)) (= $x410 $x785)) (= $x687 $x788))))
   740 (let ((@x821 (monotonicity (monotonicity @x790 (= (or $x738 $x687) $x816)) (= (and $x50 (or $x738 $x687)) $x819))))
   741 (let ((@x827 (monotonicity (monotonicity @x821 (= (or $x705 (and $x50 (or $x738 $x687))) $x822)) (= (and $x234 (or $x705 (and $x50 (or $x738 $x687)))) $x825))))
   742 (let ((@x830 (monotonicity @x827 (= (not (and $x234 (or $x705 (and $x50 (or $x738 $x687))))) $x828))))
   743 (let (($x739 (or $x738 $x687)))
   744 (let (($x740 (and $x50 $x739)))
   745 (let (($x741 (or $x705 $x740)))
   746 (let (($x742 (and $x234 $x741)))
   747 (let (($x743 (not $x742)))
   748 (let ((@x766 (monotonicity (monotonicity @x238 @x240 (= $x338 $x338)) (= $x409 $x409))))
   749 (let ((@x804 (monotonicity (monotonicity @x766 (= $x410 $x410)) (monotonicity @x780 @x800 (= $x682 $x682)) (= $x687 $x687))))
   750 (let ((@x808 (monotonicity (monotonicity @x762 @x804 (= $x739 $x739)) (= $x740 $x740))))
   751 (let ((@x814 (monotonicity (monotonicity (monotonicity @x808 (= $x741 $x741)) (= $x742 $x742)) (= $x743 $x743))))
   752 (let ((@x746 (mp (not-or-elim @x726 (not $x711)) (rewrite* (= (not $x711) $x743)) $x743)))
   753 (let ((@x1242 (mp~ (mp (mp (mp (mp @x746 @x814 $x743) @x830 $x828) @x874 $x828) @x1073 $x1071) (nnf-neg (sk (~ $x878 $x1085)) @x1238 (~ $x1071 $x1239)) $x1239)))
   754 (let ((@x2191 (mp (mp (mp @x1242 @x1374 $x1372) @x1669 $x1667) (monotonicity @x2187 (= $x1667 (or $x1396 $x2185))) (or $x1396 $x2185))))
   755 (let ((@x2302 (unit-resolution (def-axiom (or $x2182 $x2176)) (unit-resolution @x2191 (lemma @x1930 $x1391) $x2185) $x2176)))
   756 (let ((@x2309 (unit-resolution (def-axiom (or $x2179 $x1095 $x2173)) (mp @x737 (symm (commutativity (= $x50 $x31)) (= $x31 $x50)) $x50) (or $x2179 $x2173))))
   757 (let ((@x2310 (unit-resolution @x2309 @x2302 $x2173)))
   758 (let ((@x2410 (monotonicity (unit-resolution (def-axiom (or $x2146 $x144)) @x2389 $x144) (= ?x135 ?x62))))
   759 (let ((@x2413 (trans @x2410 (unit-resolution (def-axiom (or $x2170 $x63)) @x2310 $x63) (= ?x135 v_b_max_G_1$))))
   760 (let ((@x2414 (trans @x2413 (symm (unit-resolution (def-axiom (or $x2146 $x145)) @x2389 $x145) $x2022) $x136)))
   761 (let ((@x2416 (unit-resolution (def-axiom (or $x2137 $x1560 $x2131)) (unit-resolution (def-axiom (or $x2128 $x1193)) @x2414 $x2128) (unit-resolution (def-axiom (or $x2146 $x2134)) @x2389 $x2134) $x1560)))
   762 (let ((@x2421 (unit-resolution ((_ th-lemma arith assign-bounds 1 -1 -1) (or $x1693 $x985 $x1312 (not $x2024))) (unit-resolution (def-axiom (or $x1555 $x1678)) @x2416 $x1678) @x2406 (unit-resolution (def-axiom (or $x2146 $x980)) @x2389 $x980) $x1693)))
   763 (let (($x1798 (= v_b_p_G_0$ ?v0!5)))
   764 (let (($x1800 (>= (+ v_b_p_G_0$ (* (- 1) ?v0!5)) 0)))
   765 (let (($x1764 (>= (+ v_b_p_G_0$ (* (- 1) v_b_p_G_1$)) (- 1))))
   766 (let ((@x2426 (unit-resolution ((_ th-lemma arith triangle-eq) (or $x1605 $x1764)) (unit-resolution (def-axiom (or $x2146 $x991)) @x2389 $x991) $x1764)))
   767 (let ((@x2430 (unit-resolution ((_ th-lemma arith assign-bounds -1 -1) (or $x1800 $x1290 (not $x1764))) (unit-resolution (def-axiom (or $x1555 $x1295)) @x2416 $x1295) @x2426 $x1800)))
   768 (let (($x1751 (<= (+ v_b_p_G_0$ (* (- 1) ?v0!5)) 0)))
   769 (let (($x1728 (>= (+ v_b_max_G_1$ (* (- 1) ?x1179)) 0)))
   770 (let (($x2195 (not $x1728)))
   771 (let ((@x2433 (unit-resolution ((_ th-lemma arith assign-bounds -1 -1) (or $x2195 $x1312 (not $x2024))) @x2406 (unit-resolution (def-axiom (or $x1555 $x1678)) @x2416 $x1678) $x2195)))
   772 (let ((@x2333 (unit-resolution (def-axiom (or $x2170 $x2095)) @x2310 $x2095)))
   773 (let (($x1716 (or $x2100 $x1540 $x1751 $x1728)))
   774 (let (($x1775 (<= (+ ?x1179 (* (- 1) v_b_max_G_1$)) 0)))
   775 (let (($x1789 (>= (+ ?v0!5 (* (- 1) v_b_p_G_0$)) 0)))
   776 (let (($x1717 (or $x2100 (or $x1540 $x1789 $x1775))))
   777 (let (($x1739 (= (+ ?x1179 (* (- 1) v_b_max_G_1$)) (+ (* (- 1) v_b_max_G_1$) ?x1179))))
   778 (let ((@x1726 (monotonicity (rewrite $x1739) (= $x1775 (<= (+ (* (- 1) v_b_max_G_1$) ?x1179) 0)))))
   779 (let ((@x1732 (trans @x1726 (rewrite (= (<= (+ (* (- 1) v_b_max_G_1$) ?x1179) 0) $x1728)) (= $x1775 $x1728))))
   780 (let (($x1743 (= (+ ?v0!5 (* (- 1) v_b_p_G_0$)) (+ (* (- 1) v_b_p_G_0$) ?v0!5))))
   781 (let ((@x1749 (monotonicity (rewrite $x1743) (= $x1789 (>= (+ (* (- 1) v_b_p_G_0$) ?v0!5) 0)))))
   782 (let ((@x1755 (trans @x1749 (rewrite (= (>= (+ (* (- 1) v_b_p_G_0$) ?v0!5) 0) $x1751)) (= $x1789 $x1751))))
   783 (let ((@x1715 (monotonicity @x1755 @x1732 (= (or $x1540 $x1789 $x1775) (or $x1540 $x1751 $x1728)))))
   784 (let ((@x1690 (trans (monotonicity @x1715 (= $x1717 (or $x2100 (or $x1540 $x1751 $x1728)))) (rewrite (= (or $x2100 (or $x1540 $x1751 $x1728)) $x1716)) (= $x1717 $x1716))))
   785 (let ((@x2435 (unit-resolution (mp ((_ quant-inst ?v0!5) $x1717) @x1690 $x1716) @x2333 (unit-resolution (def-axiom (or $x1555 $x1173)) @x2416 $x1173) @x2433 $x1751)))
   786 (let ((@x2436 (unit-resolution ((_ th-lemma arith triangle-eq) (or $x1798 (not $x1751) (not $x1800))) @x2435 @x2430 $x1798)))
   787 (let ((@x1807 (monotonicity (symm (hypothesis $x1798) (= ?v0!5 v_b_p_G_0$)) (= ?x1179 ?x101))))
   788 (let ((@x1796 (lemma (unit-resolution (hypothesis $x1803) (symm @x1807 $x1799) false) (or (not $x1798) $x1799))))
   789 (let ((@x2437 (unit-resolution @x1796 @x2436 (unit-resolution ((_ th-lemma arith triangle-eq) (or $x1803 $x1703)) @x2421 $x1803) false)))
   790 (let (($x2228 (= v_b_max_G_1$ v_b_max_G_4$)))
   791 (let ((@x2349 (symm (unit-resolution (def-axiom (or $x2114 $x73)) (hypothesis $x2117) $x73) $x2228)))
   792 (let ((@x2352 ((_ th-lemma arith triangle-eq) (or (not $x2228) (<= (+ v_b_max_G_1$ (* (- 1) v_b_max_G_4$)) 0)))))
   793 (let ((@x2353 (unit-resolution @x2352 @x2349 (<= (+ v_b_max_G_1$ (* (- 1) v_b_max_G_4$)) 0))))
   794 (let (($x2265 (>= (+ v_b_max_G_1$ (* (- 1) (v_b_array$ ?v0!4))) 0)))
   795 (let (($x1143 (not $x1142)))
   796 (let (($x2077 (not $x2103)))
   797 (let (($x2282 (= ?x62 v_b_max_G_4$)))
   798 (let (($x2283 (or $x1528 (<= (+ v_b_length$ (* (- 1) v_b_k_G_0$)) 0) $x2282)))
   799 (let ((@x2313 (trans (unit-resolution (def-axiom (or $x2170 $x63)) @x2310 $x63) (symm (hypothesis $x73) $x2228) $x2282)))
   800 (let ((@x2316 (unit-resolution ((_ quant-inst v_b_k_G_0$) (or $x2077 (not $x2283))) (hypothesis $x2103) (unit-resolution (def-axiom (or $x2283 (not $x2282))) @x2313 $x2283) false)))
   801 (let ((@x2355 (unit-resolution (lemma @x2316 (or $x2077 $x1531)) (unit-resolution (def-axiom (or $x2114 $x73)) (hypothesis $x2117) $x73) $x2077)))
   802 (let ((@x2356 (unit-resolution (def-axiom (or $x2111 $x2103 $x1517)) @x2355 (unit-resolution (def-axiom (or $x2114 $x2108)) (hypothesis $x2117) $x2108) $x1517)))
   803 (let ((@x2343 ((_ th-lemma arith farkas -1 -1 1) (hypothesis (<= (+ v_b_p_G_0$ (* (- 1) ?v0!4)) 0)) (hypothesis $x919) (hypothesis $x1143) false)))
   804 (let ((@x2346 (lemma @x2343 (or (not (<= (+ v_b_p_G_0$ (* (- 1) ?v0!4)) 0)) $x971 $x1142))))
   805 (let ((@x2359 (unit-resolution @x2346 (unit-resolution (def-axiom (or $x2114 $x919)) (hypothesis $x2117) $x919) (unit-resolution (def-axiom (or $x1516 $x1143)) @x2356 $x1143) (not (<= (+ v_b_p_G_0$ (* (- 1) ?v0!4)) 0)))))
   806 (let (($x2272 (<= (+ v_b_p_G_0$ (* (- 1) ?v0!4)) 0)))
   807 (let (($x2296 (or $x2100 $x1489 $x2272 $x2265)))
   808 (let (($x2249 (<= (+ (v_b_array$ ?v0!4) (* (- 1) v_b_max_G_1$)) 0)))
   809 (let (($x2241 (>= (+ ?v0!4 (* (- 1) v_b_p_G_0$)) 0)))
   810 (let (($x2300 (or $x2100 (or $x1489 $x2241 $x2249))))
   811 (let (($x2266 (= (<= (+ (* (- 1) v_b_max_G_1$) (v_b_array$ ?v0!4)) 0) $x2265)))
   812 (let (($x2260 (= $x2249 (<= (+ (* (- 1) v_b_max_G_1$) (v_b_array$ ?v0!4)) 0))))
   813 (let (($x2278 (= (+ (v_b_array$ ?v0!4) (* (- 1) v_b_max_G_1$)) (+ (* (- 1) v_b_max_G_1$) (v_b_array$ ?v0!4)))))
   814 (let ((@x2292 (trans (monotonicity (rewrite $x2278) $x2260) (rewrite $x2266) (= $x2249 $x2265))))
   815 (let (($x2253 (= (+ ?v0!4 (* (- 1) v_b_p_G_0$)) (+ (* (- 1) v_b_p_G_0$) ?v0!4))))
   816 (let ((@x2258 (monotonicity (rewrite $x2253) (= $x2241 (>= (+ (* (- 1) v_b_p_G_0$) ?v0!4) 0)))))
   817 (let ((@x2276 (trans @x2258 (rewrite (= (>= (+ (* (- 1) v_b_p_G_0$) ?v0!4) 0) $x2272)) (= $x2241 $x2272))))
   818 (let ((@x2295 (monotonicity @x2276 @x2292 (= (or $x1489 $x2241 $x2249) (or $x1489 $x2272 $x2265)))))
   819 (let ((@x2319 (trans (monotonicity @x2295 (= $x2300 (or $x2100 (or $x1489 $x2272 $x2265)))) (rewrite (= (or $x2100 (or $x1489 $x2272 $x2265)) $x2296)) (= $x2300 $x2296))))
   820 (let ((@x2362 (unit-resolution (mp ((_ quant-inst ?v0!4) $x2300) @x2319 $x2296) @x2333 (unit-resolution (def-axiom (or $x1516 $x1139)) @x2356 $x1139) (or $x2272 $x2265))))
   821 (let ((@x2365 ((_ th-lemma arith farkas 1 -1 1) (unit-resolution (def-axiom (or $x1516 (not $x1253))) @x2356 (not $x1253)) (unit-resolution @x2362 @x2359 $x2265) @x2353 false)))
   822 (let ((@x2373 (unit-resolution (def-axiom (or $x2167 $x2117 $x2161)) (lemma @x2365 $x2114) (unit-resolution (def-axiom (or $x2170 $x2164)) @x2310 $x2164) $x2161)))
   823 (let ((@x2243 (unit-resolution (def-axiom (or $x2155 $x2143 $x2149)) (unit-resolution (def-axiom (or $x2158 $x2152)) @x2373 $x2152) $x2152)))
   824 (let ((@x2244 (unit-resolution @x2243 (lemma @x2437 $x2146) $x2143)))
   825 (let ((@x1791 (trans (monotonicity (hypothesis $x107) (= ?x135 ?x101)) (symm (hypothesis $x104) (= ?x101 v_b_max_G_2$)) (= ?x135 v_b_max_G_2$))))
   826 (let ((@x1769 (trans @x1791 (symm (hypothesis $x109) (= v_b_max_G_2$ v_b_max_G_3$)) $x136)))
   827 (let ((@x1771 (lemma (unit-resolution (hypothesis $x1193) @x1769 false) (or $x136 $x1603 $x1601 $x1602))))
   828 (let ((@x2380 (unit-resolution @x1771 (unit-resolution (def-axiom (or $x2140 $x109)) @x2244 $x109) (unit-resolution (def-axiom (or $x2140 $x104)) @x2244 $x104) (unit-resolution (def-axiom (or $x2140 $x107)) @x2244 $x107) $x136)))
   829 (let ((@x2368 (unit-resolution ((_ th-lemma arith triangle-eq) (or $x1605 $x1764)) (unit-resolution (def-axiom (or $x2140 $x991)) @x2244 $x991) $x1764)))
   830 (let ((@x1699 (unit-resolution (def-axiom (or $x2137 $x1560 $x2131)) (unit-resolution (def-axiom (or $x2128 $x1193)) (hypothesis $x136) $x2128) (hypothesis $x2134) $x1560)))
   831 (let (($x2205 (not $x1800)))
   832 (let (($x1838 (<= (+ ?x101 (* (- 1) v_b_max_G_3$)) 0)))
   833 (let ((@x1685 (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$))))
   834 (let ((@x1675 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not (= ?x101 v_b_max_G_3$)) $x1838)) @x1685 $x1838)))
   835 (let ((@x1696 (lemma ((_ th-lemma arith farkas -1 -1 1) (hypothesis $x1678) (hypothesis $x1838) (hypothesis $x1703) false) (or $x1693 $x1312 (not $x1838)))))
   836 (let ((@x1677 (unit-resolution @x1696 (unit-resolution (def-axiom (or $x1555 $x1678)) @x1699 $x1678) @x1675 $x1693)))
   837 (let ((@x2193 (unit-resolution @x1796 (unit-resolution ((_ th-lemma arith triangle-eq) (or $x1803 $x1703)) @x1677 $x1803) (not $x1798))))
   838 (let ((@x2198 (unit-resolution ((_ th-lemma arith assign-bounds 1 1 1) (or $x2195 $x1312 (not $x1838) $x980)) (unit-resolution (def-axiom (or $x1555 $x1678)) @x1699 $x1678) @x1675 (hypothesis $x985) $x2195)))
   839 (let ((@x2202 (unit-resolution (mp ((_ quant-inst ?v0!5) $x1717) @x1690 $x1716) (hypothesis $x2095) (unit-resolution (def-axiom (or $x1555 $x1173)) @x1699 $x1173) (or $x1751 $x1728))))
   840 (let ((@x2209 (unit-resolution ((_ th-lemma arith triangle-eq) (or $x1798 (not $x1751) $x2205)) (unit-resolution @x2202 @x2198 $x1751) (or $x1798 $x2205))))
   841 (let ((@x2211 ((_ th-lemma arith farkas -1 1 1) (unit-resolution @x2209 @x2193 $x2205) (hypothesis $x1764) (unit-resolution (def-axiom (or $x1555 $x1295)) @x1699 $x1295) false)))
   842 (let ((@x2370 (unit-resolution (lemma @x2211 (or $x1193 (not $x1764) $x2100 $x980 $x2137 $x1601 $x1603)) @x2333 (or $x1193 (not $x1764) $x980 $x2137 $x1601 $x1603))))
   843 (unit-resolution @x2370 @x2368 @x2380 (unit-resolution (def-axiom (or $x2140 $x985)) @x2244 $x985) (unit-resolution (def-axiom (or $x2140 $x2134)) @x2244 $x2134) (unit-resolution (def-axiom (or $x2140 $x104)) @x2244 $x104) (unit-resolution (def-axiom (or $x2140 $x109)) @x2244 $x109) false)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
   844