src/HOL/SMT_Examples/Boogie_Max.certs2
author haftmann
Sat Jul 05 11:01:53 2014 +0200 (2014-07-05)
changeset 57514 bdc2c6b40bf2
parent 57204 7c36ce8e45f6
permissions -rw-r--r--
prefer ac_simps collections over separate name bindings for add and mult
     1 9c420ec314a920506e90cf4b4e40b4ee3ab35dec 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