src/HOL/SMT_Examples/Boogie_Max.certs2

use SMT2 for Boogie examples

336198ca2566b9b7e0ce4a688dd7f9094f37a0b9 843 0
unsat
((set-logic AUFLIA)
(declare-fun ?v0!5 () Int)
(declare-fun ?v0!4 () Int)
(declare-fun ?v0!3 () Int)
(declare-fun ?v0!2 () Int)
(declare-fun k!10 () Bool)
(declare-fun k!00 () Bool)
(proof
(let (($x109 (= v_b_max_G_3$ v_b_max_G_2$)))
(let ((?x135 (v_b_array$ v_b_k_G_1$)))
(let (($x136 (= ?x135 v_b_max_G_3$)))
(let (($x2120 (forall ((?v0 Int) )(!(let (($x1020 (<= (+ (v_b_array$ ?v0) (* (- 1) v_b_max_G_3$)) 0)))
(let (($x1005 (>= (+ ?v0 (* (- 1) v_b_p_G_1$)) 0)))
(let (($x838 (>= ?v0 0)))
(let (($x1399 (not $x838)))
(or $x1399 $x1005 $x1020))))) :pattern ( (v_b_array$ ?v0) )))
))
(let (($x2128 (or (not $x2120) $x136)))
(let (($x2131 (not $x2128)))
(let (($x1312 (>= (+ v_b_max_G_3$ (* (- 1) (v_b_array$ ?v0!5))) 0)))
(let (($x1290 (<= (+ v_b_p_G_1$ (* (- 1) ?v0!5)) 0)))
(let (($x1173 (>= ?v0!5 0)))
(let (($x1540 (not $x1173)))
(let (($x1555 (or $x1540 $x1290 $x1312)))
(let (($x1560 (not $x1555)))
(let (($x2134 (or $x1560 $x2131)))
(let (($x2137 (not $x2134)))
(let (($x996 (>= v_b_p_G_1$ 2)))
(let (($x1606 (not $x996)))
(let (($x991 (= (+ v_b_p_G_0$ (* (- 1) v_b_p_G_1$)) (- 1))))
(let (($x1605 (not $x991)))
(let (($x989 (>= v_b_k_G_1$ 0)))
(let (($x1604 (not $x989)))
(let (($x1603 (not $x109)))
(let (($x107 (= v_b_k_G_1$ v_b_p_G_0$)))
(let (($x1602 (not $x107)))
(let ((?x101 (v_b_array$ v_b_p_G_0$)))
(let (($x104 (= v_b_max_G_2$ ?x101)))
(let (($x1601 (not $x104)))
(let (($x980 (>= (+ v_b_max_G_1$ (* (- 1) ?x101)) 0)))
(let (($x885 (>= v_b_p_G_0$ 1)))
(let (($x1529 (not $x885)))
(let (($x882 (>= v_b_k_G_0$ 0)))
(let (($x1528 (not $x882)))
(let (($x2140 (or $x1528 $x1529 $x980 $x1601 $x1602 $x1603 $x1604 $x1605 $x1606 $x2137)))
(let (($x2143 (not $x2140)))
(let (($x985 (not $x980)))
(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)))
(let ((?x1179 (v_b_array$ ?v0!5)))
(let (($x1799 (= ?x101 ?x1179)))
(let (($x1803 (not $x1799)))
(let (($x1703 (>= (+ ?x101 (* (- 1) ?x1179)) 0)))
(let (($x1693 (not $x1703)))
(let (($x2149 (not $x2146)))
(let ((@x2389 (hypothesis $x2149)))
(let (($x2024 (<= (+ v_b_max_G_1$ (* (- 1) v_b_max_G_3$)) 0)))
(let (($x2022 (= v_b_max_G_1$ v_b_max_G_3$)))
(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))))
(let (($x145 (= v_b_max_G_3$ v_b_max_G_1$)))
(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)))
(let (($x1678 (not $x1312)))
(let ((?x62 (v_b_array$ v_b_k_G_0$)))
(let (($x63 (= ?x62 v_b_max_G_1$)))
(let (($x2152 (or $x2143 $x2149)))
(let (($x2155 (not $x2152)))
(let (($x919 (<= (+ v_b_length$ (* (- 1) v_b_p_G_0$)) 0)))
(let (($x2158 (or $x1528 $x1529 $x919 $x2155)))
(let (($x2161 (not $x2158)))
(let (($x1253 (>= (+ v_b_max_G_4$ (* (- 1) (v_b_array$ ?v0!4))) 0)))
(let (($x1142 (<= (+ v_b_length$ (* (- 1) ?v0!4)) 0)))
(let (($x1139 (>= ?v0!4 0)))
(let (($x1489 (not $x1139)))
(let (($x1131 (= (v_b_array$ ?v0!3) v_b_max_G_4$)))
(let (($x1126 (<= (+ v_b_length$ (* (- 1) ?v0!3)) 0)))
(let (($x1484 (or (not (>= ?v0!3 0)) $x1126 $x1131)))
(let (($x1516 (or (not $x1484) $x1489 $x1142 $x1253)))
(let (($x1517 (not $x1516)))
(let (($x2103 (forall ((?v0 Int) )(!(let ((?x46 (v_b_array$ ?v0)))
(let (($x86 (= ?x46 v_b_max_G_4$)))
(let (($x930 (<= (+ v_b_length$ (* (- 1) ?v0)) 0)))
(let (($x838 (>= ?v0 0)))
(let (($x1399 (not $x838)))
(let (($x1458 (or $x1399 $x930 $x86)))
(not $x1458))))))) :pattern ( (v_b_array$ ?v0) )))
))
(let (($x2108 (or $x2103 $x1517)))
(let (($x2111 (not $x2108)))
(let (($x73 (= v_b_max_G_4$ v_b_max_G_1$)))
(let (($x1531 (not $x73)))
(let (($x971 (not $x919)))
(let (($x2114 (or $x1528 $x1529 $x971 (not k!00) $x1531 (not k!10) $x2111)))
(let (($x2117 (not $x2114)))
(let (($x2164 (or $x2117 $x2161)))
(let (($x2167 (not $x2164)))
(let (($x2095 (forall ((?v0 Int) )(!(let (($x903 (<= (+ (v_b_array$ ?v0) (* (- 1) v_b_max_G_1$)) 0)))
(let (($x888 (>= (+ ?v0 (* (- 1) v_b_p_G_0$)) 0)))
(let (($x838 (>= ?v0 0)))
(let (($x1399 (not $x838)))
(or $x1399 $x888 $x903))))) :pattern ( (v_b_array$ ?v0) )))
))
(let (($x2100 (not $x2095)))
(let (($x2170 (or $x1528 $x1529 $x2100 (not $x63) $x2167)))
(let (($x2173 (not $x2170)))
(let ((?x30 (v_b_array$ 0)))
(let (($x50 (= ?x30 v_b_max_G_0$)))
(let (($x1095 (not $x50)))
(let (($x2176 (or $x1095 $x2173)))
(let (($x2179 (not $x2176)))
(let (($x2087 (forall ((?v0 Int) )(!(let (($x851 (>= (+ v_b_max_G_0$ (* (- 1) (v_b_array$ ?v0))) 0)))
(let (($x841 (>= ?v0 1)))
(let (($x838 (>= ?v0 0)))
(let (($x1399 (not $x838)))
(or $x1399 $x841 $x851))))) :pattern ( (v_b_array$ ?v0) )))
))
(let (($x2182 (or (not $x2087) $x2179)))
(let (($x2185 (not $x2182)))
(let (($x1083 (>= (+ v_b_max_G_0$ (* (- 1) (v_b_array$ ?v0!2))) 0)))
(let (($x831 (>= ?v0!2 1)))
(let (($x1391 (or (not (>= ?v0!2 0)) $x831 $x1083)))
(let (($x1079 (not $x831)))
(let (($x1396 (not $x1391)))
(let ((@x1966 (hypothesis $x1396)))
(let (($x1078 (>= ?v0!2 0)))
(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))))
(let ((@x1955 (symm (monotonicity @x1951 (= (v_b_array$ ?v0!2) ?x30)) (= ?x30 (v_b_array$ ?v0!2)))))
(let (($x31 (= v_b_max_G_0$ ?x30)))
(let (($x201 (and (not (<= v_b_length$ 0)) $x31)))
(let (($x572 (forall ((?v0 Int) )(let ((?x46 (v_b_array$ ?v0)))
(let (($x132 (<= ?x46 v_b_max_G_3$)))
(or (not (and (<= 0 ?v0) (not (<= v_b_p_G_1$ ?v0)))) $x132))))
))
(let (($x595 (or (not $x572) $x136)))
(let (($x600 (and $x572 $x595)))
(let (($x116 (<= 2 v_b_p_G_1$)))
(let (($x456 (= v_b_p_G_1$ (+ 1 v_b_p_G_0$))))
(let (($x110 (<= 0 v_b_k_G_1$)))
(let (($x144 (= v_b_k_G_1$ v_b_k_G_0$)))
(let (($x143 (<= ?x101 v_b_max_G_1$)))
(let (($x54 (<= 1 v_b_p_G_0$)))
(let (($x52 (<= 0 v_b_k_G_0$)))
(let (($x654 (and $x52 $x54 $x143 $x144 $x145 $x110 $x456 $x116)))
(let (($x669 (not $x654)))
(let (($x670 (or $x669 $x600)))
(let (($x441 (not $x143)))
(let (($x544 (and $x52 $x54 $x441 $x104 $x107 $x109 $x110 $x456 $x116)))
(let (($x606 (not $x544)))
(let (($x607 (or $x606 $x600)))
(let (($x675 (and $x607 $x670)))
(let (($x69 (<= v_b_length$ v_b_p_G_0$)))
(let (($x415 (not $x69)))
(let (($x429 (and $x52 $x54 $x415)))
(let (($x681 (not $x429)))
(let (($x682 (or $x681 $x675)))
(let (($x377 (forall ((?v0 Int) )(let ((?x46 (v_b_array$ ?v0)))
(let (($x89 (<= ?x46 v_b_max_G_4$)))
(let (($x351 (not (<= v_b_length$ ?v0))))
(let (($x43 (<= 0 ?v0)))
(let (($x354 (and $x43 $x351)))
(let (($x360 (not $x354)))
(or $x360 $x89))))))))
))
(let (($x366 (exists ((?v0 Int) )(let ((?x46 (v_b_array$ ?v0)))
(let (($x86 (= ?x46 v_b_max_G_4$)))
(let (($x351 (not (<= v_b_length$ ?v0))))
(let (($x43 (<= 0 ?v0)))
(let (($x354 (and $x43 $x351)))
(let (($x360 (not $x354)))
(or $x360 $x86))))))))
))
(let (($x398 (or (not $x366) $x377)))
(let (($x403 (and $x366 $x398)))
(let (($x75 (= v_b_p_G_2$ v_b_p_G_0$)))
(let (($x71 (= v_b_k_G_2$ v_b_k_G_0$)))
(let (($x338 (and $x52 $x54 $x69 $x71 $x73 $x75)))
(let (($x409 (not $x338)))
(let (($x410 (or $x409 $x403)))
(let (($x687 (and $x410 $x682)))
(let (($x259 (forall ((?v0 Int) )(let ((?x46 (v_b_array$ ?v0)))
(let (($x59 (<= ?x46 v_b_max_G_1$)))
(or (not (and (<= 0 ?v0) (not (<= v_b_p_G_0$ ?v0)))) $x59))))
))
(let (($x294 (and $x50 $x52 $x54 $x259 $x63)))
(let (($x694 (or (not $x294) $x687)))
(let (($x699 (and $x50 $x694)))
(let (($x234 (forall ((?v0 Int) )(let ((?x46 (v_b_array$ ?v0)))
(let (($x47 (<= ?x46 v_b_max_G_0$)))
(or (not (and (<= 0 ?v0) (not (<= 1 ?v0)))) $x47))))
))
(let (($x705 (not $x234)))
(let (($x706 (or $x705 $x699)))
(let (($x711 (and $x234 $x706)))
(let (($x718 (or (not $x201) $x711)))
(let (($x138 (=> (and $x136 false) true)))
(let (($x139 (and $x136 $x138)))
(let (($x134 (forall ((?v0 Int) )(let ((?x46 (v_b_array$ ?v0)))
(let (($x132 (<= ?x46 v_b_max_G_3$)))
(=> (and (<= 0 ?v0) (< ?v0 v_b_p_G_1$)) $x132))))
))
(let (($x140 (=> $x134 $x139)))
(let (($x141 (and $x134 $x140)))
(let (($x117 (and $x110 $x116)))
(let (($x118 (and $x117 true)))
(let (($x119 (and (= v_b_p_G_1$ (+ v_b_p_G_0$ 1)) $x118)))
(let (($x111 (and $x110 $x54)))
(let (($x120 (and $x111 $x119)))
(let (($x121 (and true $x120)))
(let (($x146 (and $x145 $x121)))
(let (($x147 (and $x144 $x146)))
(let (($x148 (and true $x147)))
(let (($x55 (and $x52 $x54)))
(let (($x149 (and $x55 $x148)))
(let (($x150 (and $x143 $x149)))
(let (($x151 (and $x55 $x150)))
(let (($x152 (and true $x151)))
(let (($x153 (=> $x152 $x141)))
(let (($x122 (and $x109 $x121)))
(let (($x123 (and $x107 $x122)))
(let (($x124 (and true $x123)))
(let (($x105 (and $x54 $x54)))
(let (($x125 (and $x105 $x124)))
(let (($x126 (and $x104 $x125)))
(let (($x127 (and (< v_b_max_G_1$ ?x101) $x126)))
(let (($x128 (and $x55 $x127)))
(let (($x129 (and true $x128)))
(let (($x142 (=> $x129 $x141)))
(let (($x98 (and (< v_b_p_G_0$ v_b_length$) $x55)))
(let (($x99 (and $x55 $x98)))
(let (($x100 (and true $x99)))
(let (($x155 (=> $x100 (and $x142 $x153))))
(let (($x91 (forall ((?v0 Int) )(let ((?x46 (v_b_array$ ?v0)))
(let (($x89 (<= ?x46 v_b_max_G_4$)))
(let (($x43 (<= 0 ?v0)))
(let (($x85 (and $x43 (< ?v0 v_b_length$))))
(=> $x85 $x89))))))
))
(let (($x92 (=> $x91 true)))
(let (($x93 (and $x91 $x92)))
(let (($x88 (exists ((?v0 Int) )(let ((?x46 (v_b_array$ ?v0)))
(let (($x86 (= ?x46 v_b_max_G_4$)))
(let (($x43 (<= 0 ?v0)))
(let (($x85 (and $x43 (< ?v0 v_b_length$))))
(=> $x85 $x86))))))
))
(let (($x94 (=> $x88 $x93)))
(let (($x78 (and $x71 (and $x73 (and $x75 true)))))
(let (($x79 (and true $x78)))
(let (($x80 (and $x55 $x79)))
(let (($x81 (and $x69 $x80)))
(let (($x82 (and $x55 $x81)))
(let (($x83 (and true $x82)))
(let (($x96 (=> $x83 (and $x88 $x94))))
(let (($x64 (and $x63 $x55)))
(let (($x61 (forall ((?v0 Int) )(let ((?x46 (v_b_array$ ?v0)))
(let (($x59 (<= ?x46 v_b_max_G_1$)))
(=> (and (<= 0 ?v0) (< ?v0 v_b_p_G_0$)) $x59))))
))
(let (($x65 (and $x61 $x64)))
(let (($x66 (and $x55 $x65)))
(let (($x67 (and true $x66)))
(let (($x68 (and $x50 $x67)))
(let (($x157 (=> $x68 (and $x96 $x155))))
(let (($x49 (forall ((?v0 Int) )(let ((?x46 (v_b_array$ ?v0)))
(let (($x47 (<= ?x46 v_b_max_G_0$)))
(=> (and (<= 0 ?v0) (< ?v0 1)) $x47))))
))
(let (($x159 (=> $x49 (and $x50 $x157))))
(let (($x34 (<= 1 1)))
(let (($x35 (and $x34 $x34)))
(let (($x32 (<= 0 0)))
(let (($x36 (and $x32 $x35)))
(let (($x37 (and $x32 $x36)))
(let (($x38 (and $x31 $x37)))
(let (($x39 (and true $x38)))
(let (($x41 (and true (and (< 0 v_b_length$) $x39))))
(let (($x161 (=> $x41 (and $x49 $x159))))
(let (($x162 (not $x161)))
(let ((@x579 (monotonicity (rewrite (= (and $x136 false) false)) (= $x138 (=> false true)))))
(let ((@x583 (trans @x579 (rewrite (= (=> false true) true)) (= $x138 true))))
(let ((@x590 (trans (monotonicity @x583 (= $x139 (and $x136 true))) (rewrite (= (and $x136 true) $x136)) (= $x139 $x136))))
(let ((?x46 (v_b_array$ ?0)))
(let (($x132 (<= ?x46 v_b_max_G_3$)))
(let (($x567 (or (not (and (<= 0 ?0) (not (<= v_b_p_G_1$ ?0)))) $x132)))
(let (($x133 (=> (and (<= 0 ?0) (< ?0 v_b_p_G_1$)) $x132)))
(let (($x568 (= (=> (and (<= 0 ?0) (not (<= v_b_p_G_1$ ?0))) $x132) $x567)))
(let (($x564 (= $x133 (=> (and (<= 0 ?0) (not (<= v_b_p_G_1$ ?0))) $x132))))
(let (($x557 (not (<= v_b_p_G_1$ ?0))))
(let (($x43 (<= 0 ?0)))
(let (($x560 (and $x43 $x557)))
(let ((@x212 (rewrite (= $x43 $x43))))
(let ((@x562 (monotonicity @x212 (rewrite (= (< ?0 v_b_p_G_1$) $x557)) (= (and $x43 (< ?0 v_b_p_G_1$)) $x560))))
(let ((@x574 (quant-intro (trans (monotonicity @x562 $x564) (rewrite $x568) (= $x133 $x567)) (= $x134 $x572))))
(let ((@x599 (trans (monotonicity @x574 @x590 (= $x140 (=> $x572 $x136))) (rewrite (= (=> $x572 $x136) $x595)) (= $x140 $x595))))
(let ((@x656 (rewrite (= (and $x55 (and $x143 $x52 $x54 $x144 $x145 $x110 $x456 $x116)) $x654))))
(let (($x646 (and $x143 $x52 $x54 $x144 $x145 $x110 $x456 $x116)))
(let ((@x648 (rewrite (= (and $x143 (and $x52 $x54 $x144 $x145 $x110 $x456 $x116)) $x646))))
(let (($x638 (and $x52 $x54 $x144 $x145 $x110 $x456 $x116)))
(let (($x623 (and $x144 $x145 $x110 $x54 $x456 $x116)))
(let (($x615 (and $x145 $x110 $x54 $x456 $x116)))
(let (($x482 (and $x110 $x54 $x456 $x116)))
(let ((@x463 (rewrite (= $x116 $x116))))
(let ((@x450 (rewrite (= $x110 $x110))))
(let ((@x467 (monotonicity (monotonicity @x450 @x463 (= $x117 $x117)) (= $x118 $x118))))
(let ((@x460 (rewrite (= $x456 $x456))))
(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))))
(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)))))
(let ((@x478 (trans @x473 (rewrite (= (and $x456 $x117) (and $x456 $x110 $x116))) (= $x119 (and $x456 $x110 $x116)))))
(let ((@x481 (monotonicity (monotonicity @x450 (rewrite (= $x54 $x54)) (= $x111 $x111)) @x478 (= $x120 (and $x111 (and $x456 $x110 $x116))))))
(let ((@x486 (trans @x481 (rewrite (= (and $x111 (and $x456 $x110 $x116)) $x482)) (= $x120 $x482))))
(let ((@x493 (trans (monotonicity @x486 (= $x121 (and true $x482))) (rewrite (= (and true $x482) $x482)) (= $x121 $x482))))
(let ((@x619 (trans (monotonicity @x493 (= $x146 (and $x145 $x482))) (rewrite (= (and $x145 $x482) $x615)) (= $x146 $x615))))
(let ((@x627 (trans (monotonicity @x619 (= $x147 (and $x144 $x615))) (rewrite (= (and $x144 $x615) $x623)) (= $x147 $x623))))
(let ((@x634 (trans (monotonicity @x627 (= $x148 (and true $x623))) (rewrite (= (and true $x623) $x623)) (= $x148 $x623))))
(let ((@x240 (rewrite (= $x54 $x54))))
(let ((@x238 (rewrite (= $x52 $x52))))
(let ((@x242 (monotonicity @x238 @x240 (= $x55 $x55))))
(let ((@x642 (trans (monotonicity @x242 @x634 (= $x149 (and $x55 $x623))) (rewrite (= (and $x55 $x623) $x638)) (= $x149 $x638))))
(let ((@x650 (trans (monotonicity @x642 (= $x150 (and $x143 $x638))) @x648 (= $x150 $x646))))
(let ((@x658 (trans (monotonicity @x242 @x650 (= $x151 (and $x55 $x646))) @x656 (= $x151 $x654))))
(let ((@x665 (trans (monotonicity @x658 (= $x152 (and true $x654))) (rewrite (= (and true $x654) $x654)) (= $x152 $x654))))
(let ((@x668 (monotonicity @x665 (monotonicity @x574 @x599 (= $x141 $x600)) (= $x153 (=> $x654 $x600)))))
(let ((@x546 (rewrite (= (and $x55 (and $x441 $x104 $x54 $x107 $x109 $x110 $x456 $x116)) $x544))))
(let (($x536 (and $x441 $x104 $x54 $x107 $x109 $x110 $x456 $x116)))
(let ((@x538 (rewrite (= (and $x441 (and $x104 $x54 $x107 $x109 $x110 $x456 $x116)) $x536))))
(let (($x528 (and $x104 $x54 $x107 $x109 $x110 $x456 $x116)))
(let (($x520 (and $x54 $x107 $x109 $x110 $x456 $x116)))
(let (($x505 (and $x107 $x109 $x110 $x54 $x456 $x116)))
(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)))))
(let ((@x504 (monotonicity @x501 (= $x123 (and $x107 (and $x109 $x110 $x54 $x456 $x116))))))
(let ((@x509 (trans @x504 (rewrite (= (and $x107 (and $x109 $x110 $x54 $x456 $x116)) $x505)) (= $x123 $x505))))
(let ((@x516 (trans (monotonicity @x509 (= $x124 (and true $x505))) (rewrite (= (and true $x505) $x505)) (= $x124 $x505))))
(let ((@x448 (trans (monotonicity @x240 @x240 (= $x105 $x105)) (rewrite (= $x105 $x54)) (= $x105 $x54))))
(let ((@x524 (trans (monotonicity @x448 @x516 (= $x125 (and $x54 $x505))) (rewrite (= (and $x54 $x505) $x520)) (= $x125 $x520))))
(let ((@x532 (trans (monotonicity @x524 (= $x126 (and $x104 $x520))) (rewrite (= (and $x104 $x520) $x528)) (= $x126 $x528))))
(let ((@x535 (monotonicity (rewrite (= (< v_b_max_G_1$ ?x101) $x441)) @x532 (= $x127 (and $x441 $x528)))))
(let ((@x543 (monotonicity @x242 (trans @x535 @x538 (= $x127 $x536)) (= $x128 (and $x55 $x536)))))
(let ((@x551 (monotonicity (trans @x543 @x546 (= $x128 $x544)) (= $x129 (and true $x544)))))
(let ((@x605 (monotonicity (trans @x551 (rewrite (= (and true $x544) $x544)) (= $x129 $x544)) (monotonicity @x574 @x599 (= $x141 $x600)) (= $x142 (=> $x544 $x600)))))
(let ((@x677 (monotonicity (trans @x605 (rewrite (= (=> $x544 $x600) $x607)) (= $x142 $x607)) (trans @x668 (rewrite (= (=> $x654 $x600) $x670)) (= $x153 $x670)) (= (and $x142 $x153) $x675))))
(let ((@x420 (monotonicity (rewrite (= (< v_b_p_G_0$ v_b_length$) $x415)) @x242 (= $x98 (and $x415 $x55)))))
(let ((@x425 (trans @x420 (rewrite (= (and $x415 $x55) (and $x415 $x52 $x54))) (= $x98 (and $x415 $x52 $x54)))))
(let ((@x433 (trans (monotonicity @x242 @x425 (= $x99 (and $x55 (and $x415 $x52 $x54)))) (rewrite (= (and $x55 (and $x415 $x52 $x54)) $x429)) (= $x99 $x429))))
(let ((@x440 (trans (monotonicity @x433 (= $x100 (and true $x429))) (rewrite (= (and true $x429) $x429)) (= $x100 $x429))))
(let ((@x686 (trans (monotonicity @x440 @x677 (= $x155 (=> $x429 $x675))) (rewrite (= (=> $x429 $x675) $x682)) (= $x155 $x682))))
(let (($x89 (<= ?x46 v_b_max_G_4$)))
(let (($x351 (not (<= v_b_length$ ?0))))
(let (($x354 (and $x43 $x351)))
(let (($x360 (not $x354)))
(let (($x372 (or $x360 $x89)))
(let (($x85 (and $x43 (< ?0 v_b_length$))))
(let (($x90 (=> $x85 $x89)))
(let ((@x356 (monotonicity @x212 (rewrite (= (< ?0 v_b_length$) $x351)) (= $x85 $x354))))
(let ((@x376 (trans (monotonicity @x356 (= $x90 (=> $x354 $x89))) (rewrite (= (=> $x354 $x89) $x372)) (= $x90 $x372))))
(let ((@x382 (monotonicity (quant-intro @x376 (= $x91 $x377)) (= $x92 (=> $x377 true)))))
(let ((@x386 (trans @x382 (rewrite (= (=> $x377 true) true)) (= $x92 true))))
(let ((@x389 (monotonicity (quant-intro @x376 (= $x91 $x377)) @x386 (= $x93 (and $x377 true)))))
(let (($x86 (= ?x46 v_b_max_G_4$)))
(let (($x361 (or $x360 $x86)))
(let (($x87 (=> $x85 $x86)))
(let ((@x365 (trans (monotonicity @x356 (= $x87 (=> $x354 $x86))) (rewrite (= (=> $x354 $x86) $x361)) (= $x87 $x361))))
(let ((@x396 (monotonicity (quant-intro @x365 (= $x88 $x366)) (trans @x389 (rewrite (= (and $x377 true) $x377)) (= $x93 $x377)) (= $x94 (=> $x366 $x377)))))
(let ((@x405 (monotonicity (quant-intro @x365 (= $x88 $x366)) (trans @x396 (rewrite (= (=> $x366 $x377) $x398)) (= $x94 $x398)) (= (and $x88 $x94) $x403))))
(let (($x330 (and $x69 $x52 $x54 $x71 $x73 $x75)))
(let (($x322 (and $x52 $x54 $x71 $x73 $x75)))
(let ((@x316 (rewrite (= (and true (and $x71 $x73 $x75)) (and $x71 $x73 $x75)))))
(let ((@x303 (monotonicity (rewrite (= (and $x75 true) $x75)) (= (and $x73 (and $x75 true)) (and $x73 $x75)))))
(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)))))
(let ((@x318 (trans (monotonicity @x311 (= $x79 (and true (and $x71 $x73 $x75)))) @x316 (= $x79 (and $x71 $x73 $x75)))))
(let ((@x326 (trans (monotonicity @x242 @x318 (= $x80 (and $x55 (and $x71 $x73 $x75)))) (rewrite (= (and $x55 (and $x71 $x73 $x75)) $x322)) (= $x80 $x322))))
(let ((@x334 (trans (monotonicity @x326 (= $x81 (and $x69 $x322))) (rewrite (= (and $x69 $x322) $x330)) (= $x81 $x330))))
(let ((@x342 (trans (monotonicity @x242 @x334 (= $x82 (and $x55 $x330))) (rewrite (= (and $x55 $x330) $x338)) (= $x82 $x338))))
(let ((@x349 (trans (monotonicity @x342 (= $x83 (and true $x338))) (rewrite (= (and true $x338) $x338)) (= $x83 $x338))))
(let ((@x414 (trans (monotonicity @x349 @x405 (= $x96 (=> $x338 $x403))) (rewrite (= (=> $x338 $x403) $x410)) (= $x96 $x410))))
(let (($x279 (and $x52 $x54 $x259 $x63)))
(let ((@x273 (rewrite (= (and $x259 (and $x63 $x52 $x54)) (and $x259 $x63 $x52 $x54)))))
(let ((@x267 (trans (monotonicity @x242 (= $x64 $x64)) (rewrite (= $x64 (and $x63 $x52 $x54))) (= $x64 (and $x63 $x52 $x54)))))
(let (($x59 (<= ?x46 v_b_max_G_1$)))
(let (($x254 (or (not (and $x43 (not (<= v_b_p_G_0$ ?0)))) $x59)))
(let (($x60 (=> (and $x43 (< ?0 v_b_p_G_0$)) $x59)))
(let ((@x256 (rewrite (= (=> (and $x43 (not (<= v_b_p_G_0$ ?0))) $x59) $x254))))
(let (($x244 (not (<= v_b_p_G_0$ ?0))))
(let (($x247 (and $x43 $x244)))
(let ((@x249 (monotonicity @x212 (rewrite (= (< ?0 v_b_p_G_0$) $x244)) (= (and $x43 (< ?0 v_b_p_G_0$)) $x247))))
(let ((@x258 (trans (monotonicity @x249 (= $x60 (=> $x247 $x59))) @x256 (= $x60 $x254))))
(let ((@x270 (monotonicity (quant-intro @x258 (= $x61 $x259)) @x267 (= $x65 (and $x259 (and $x63 $x52 $x54))))))
(let ((@x278 (monotonicity @x242 (trans @x270 @x273 (= $x65 (and $x259 $x63 $x52 $x54))) (= $x66 (and $x55 (and $x259 $x63 $x52 $x54))))))
(let ((@x283 (trans @x278 (rewrite (= (and $x55 (and $x259 $x63 $x52 $x54)) $x279)) (= $x66 $x279))))
(let ((@x290 (trans (monotonicity @x283 (= $x67 (and true $x279))) (rewrite (= (and true $x279) $x279)) (= $x67 $x279))))
(let ((@x298 (trans (monotonicity @x290 (= $x68 (and $x50 $x279))) (rewrite (= (and $x50 $x279) $x294)) (= $x68 $x294))))
(let ((@x692 (monotonicity @x298 (monotonicity @x414 @x686 (= (and $x96 $x155) $x687)) (= $x157 (=> $x294 $x687)))))
(let ((@x701 (monotonicity (trans @x692 (rewrite (= (=> $x294 $x687) $x694)) (= $x157 $x694)) (= (and $x50 $x157) $x699))))
(let (($x47 (<= ?x46 v_b_max_G_0$)))
(let (($x229 (or (not (and $x43 (not (<= 1 ?0)))) $x47)))
(let (($x48 (=> (and $x43 (< ?0 1)) $x47)))
(let ((@x220 (monotonicity (rewrite (= (<= 1 ?0) (<= 1 ?0))) (= (not (<= 1 ?0)) (not (<= 1 ?0))))))
(let ((@x221 (trans (rewrite (= (< ?0 1) (not (<= 1 ?0)))) @x220 (= (< ?0 1) (not (<= 1 ?0))))))
(let ((@x224 (monotonicity @x212 @x221 (= (and $x43 (< ?0 1)) (and $x43 (not (<= 1 ?0)))))))
(let ((@x227 (monotonicity @x224 (= $x48 (=> (and $x43 (not (<= 1 ?0))) $x47)))))
(let ((@x233 (trans @x227 (rewrite (= (=> (and $x43 (not (<= 1 ?0))) $x47) $x229)) (= $x48 $x229))))
(let ((@x704 (monotonicity (quant-intro @x233 (= $x49 $x234)) @x701 (= $x159 (=> $x234 $x699)))))
(let ((@x713 (monotonicity (quant-intro @x233 (= $x49 $x234)) (trans @x704 (rewrite (= (=> $x234 $x699) $x706)) (= $x159 $x706)) (= (and $x49 $x159) $x711))))
(let ((@x176 (rewrite (= (and true true) true))))
(let ((@x174 (monotonicity (rewrite (= $x34 true)) (rewrite (= $x34 true)) (= $x35 (and true true)))))
(let ((@x180 (monotonicity (rewrite (= $x32 true)) (trans @x174 @x176 (= $x35 true)) (= $x36 (and true true)))))
(let ((@x184 (monotonicity (rewrite (= $x32 true)) (trans @x180 @x176 (= $x36 true)) (= $x37 (and true true)))))
(let ((@x189 (monotonicity (trans @x184 @x176 (= $x37 true)) (= $x38 (and $x31 true)))))
(let ((@x196 (monotonicity (trans @x189 (rewrite (= (and $x31 true) $x31)) (= $x38 $x31)) (= $x39 (and true $x31)))))
(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))))
(let ((@x210 (trans (monotonicity @x203 (= $x41 (and true $x201))) (rewrite (= (and true $x201) $x201)) (= $x41 $x201))))
(let ((@x722 (trans (monotonicity @x210 @x713 (= $x161 (=> $x201 $x711))) (rewrite (= (=> $x201 $x711) $x718)) (= $x161 $x718))))
(let ((@x726 (mp (asserted $x162) (monotonicity @x722 (= $x162 (not $x718))) (not $x718))))
(let ((@x737 (mp (and-elim (not-or-elim @x726 $x201) $x31) (rewrite* (= $x31 $x31)) $x31)))
(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)))
(let (($x1582 (forall ((?v0 Int) )(let (($x1020 (<= (+ (v_b_array$ ?v0) (* (- 1) v_b_max_G_3$)) 0)))
(let (($x1005 (>= (+ ?v0 (* (- 1) v_b_p_G_1$)) 0)))
(let (($x838 (>= ?v0 0)))
(let (($x1399 (not $x838)))
(or $x1399 $x1005 $x1020))))))
))
(let (($x1590 (not (or (not $x1582) $x136))))
(let (($x1595 (or $x1560 $x1590)))
(let (($x1607 (not $x1595)))
(let (($x1620 (not (or $x1528 $x1529 $x985 (not $x144) (not $x145) $x1604 $x1605 $x1606 $x1607))))
(let (($x1609 (not (or $x1528 $x1529 $x980 $x1601 $x1602 $x1603 $x1604 $x1605 $x1606 $x1607))))
(let (($x1625 (or $x1609 $x1620)))
(let (($x1633 (not (or $x1528 $x1529 $x919 (not $x1625)))))
(let (($x1466 (forall ((?v0 Int) )(let ((?x46 (v_b_array$ ?v0)))
(let (($x86 (= ?x46 v_b_max_G_4$)))
(let (($x930 (<= (+ v_b_length$ (* (- 1) ?v0)) 0)))
(let (($x838 (>= ?v0 0)))
(let (($x1399 (not $x838)))
(let (($x1458 (or $x1399 $x930 $x86)))
(not $x1458))))))))
))
(let (($x1522 (or $x1466 $x1517)))
(let (($x1535 (not (or $x1528 $x1529 $x971 (not k!00) $x1531 (not k!10) (not $x1522)))))
(let (($x1638 (or $x1535 $x1633)))
(let (($x1441 (forall ((?v0 Int) )(let (($x903 (<= (+ (v_b_array$ ?v0) (* (- 1) v_b_max_G_1$)) 0)))
(let (($x888 (>= (+ ?v0 (* (- 1) v_b_p_G_0$)) 0)))
(let (($x838 (>= ?v0 0)))
(let (($x1399 (not $x838)))
(or $x1399 $x888 $x903))))))
))
(let (($x1648 (not (or $x1528 $x1529 (not $x1441) (not $x63) (not $x1638)))))
(let (($x1653 (or $x1095 $x1648)))
(let (($x1419 (forall ((?v0 Int) )(let (($x851 (>= (+ v_b_max_G_0$ (* (- 1) (v_b_array$ ?v0))) 0)))
(let (($x841 (>= ?v0 1)))
(let (($x838 (>= ?v0 0)))
(let (($x1399 (not $x838)))
(or $x1399 $x841 $x851))))))
))
(let (($x1662 (not (or (not $x1419) (not $x1653)))))
(let (($x1667 (or $x1396 $x1662)))
(let (($x2147 (= (or $x1528 $x1529 $x985 (not $x144) (not $x145) $x1604 $x1605 $x1606 $x1607) $x2146)))
(let (($x1020 (<= (+ ?x46 (* (- 1) v_b_max_G_3$)) 0)))
(let (($x1005 (>= (+ ?0 (* (- 1) v_b_p_G_1$)) 0)))
(let (($x838 (>= ?0 0)))
(let (($x1399 (not $x838)))
(let (($x1577 (or $x1399 $x1005 $x1020)))
(let ((@x2127 (monotonicity (quant-intro (refl (= $x1577 $x1577)) (= $x1582 $x2120)) (= (not $x1582) (not $x2120)))))
(let ((@x2133 (monotonicity (monotonicity @x2127 (= (or (not $x1582) $x136) $x2128)) (= $x1590 $x2131))))
(let ((@x2148 (monotonicity (monotonicity (monotonicity @x2133 (= $x1595 $x2134)) (= $x1607 $x2137)) $x2147)))
(let ((@x2142 (monotonicity (monotonicity (monotonicity @x2133 (= $x1595 $x2134)) (= $x1607 $x2137)) (= (or $x1528 $x1529 $x980 $x1601 $x1602 $x1603 $x1604 $x1605 $x1606 $x1607) $x2140))))
(let ((@x2154 (monotonicity (monotonicity @x2142 (= $x1609 $x2143)) (monotonicity @x2148 (= $x1620 $x2149)) (= $x1625 $x2152))))
(let ((@x2160 (monotonicity (monotonicity @x2154 (= (not $x1625) $x2155)) (= (or $x1528 $x1529 $x919 (not $x1625)) $x2158))))
(let (($x2115 (= (or $x1528 $x1529 $x971 (not k!00) $x1531 (not k!10) (not $x1522)) $x2114)))
(let (($x930 (<= (+ v_b_length$ (* (- 1) ?0)) 0)))
(let (($x1458 (or $x1399 $x930 $x86)))
(let (($x1463 (not $x1458)))
(let ((@x2110 (monotonicity (quant-intro (refl (= $x1463 $x1463)) (= $x1466 $x2103)) (= $x1522 $x2108))))
(let ((@x2119 (monotonicity (monotonicity (monotonicity @x2110 (= (not $x1522) $x2111)) $x2115) (= $x1535 $x2117))))
(let ((@x2166 (monotonicity @x2119 (monotonicity @x2160 (= $x1633 $x2161)) (= $x1638 $x2164))))
(let (($x903 (<= (+ ?x46 (* (- 1) v_b_max_G_1$)) 0)))
(let (($x888 (>= (+ ?0 (* (- 1) v_b_p_G_0$)) 0)))
(let (($x1436 (or $x1399 $x888 $x903)))
(let ((@x2102 (monotonicity (quant-intro (refl (= $x1436 $x1436)) (= $x1441 $x2095)) (= (not $x1441) $x2100))))
(let ((@x2172 (monotonicity @x2102 (monotonicity @x2166 (= (not $x1638) $x2167)) (= (or $x1528 $x1529 (not $x1441) (not $x63) (not $x1638)) $x2170))))
(let ((@x2181 (monotonicity (monotonicity (monotonicity @x2172 (= $x1648 $x2173)) (= $x1653 $x2176)) (= (not $x1653) $x2179))))
(let (($x851 (>= (+ v_b_max_G_0$ (* (- 1) ?x46)) 0)))
(let (($x841 (>= ?0 1)))
(let (($x1414 (or $x1399 $x841 $x851)))
(let ((@x2094 (monotonicity (quant-intro (refl (= $x1414 $x1414)) (= $x1419 $x2087)) (= (not $x1419) (not $x2087)))))
(let ((@x2187 (monotonicity (monotonicity @x2094 @x2181 (= (or (not $x1419) (not $x1653)) $x2182)) (= $x1662 $x2185))))
(let (($x1193 (not $x136)))
(let (($x1026 (forall ((?v0 Int) )(let (($x1020 (<= (+ (v_b_array$ ?v0) (* (- 1) v_b_max_G_3$)) 0)))
(let (($x838 (>= ?v0 0)))
(let (($x1012 (and $x838 (not (>= (+ ?v0 (* (- 1) v_b_p_G_1$)) 0)))))
(let (($x1015 (not $x1012)))
(or $x1015 $x1020))))))
))
(let (($x1196 (and $x1026 $x1193)))
(let (($x1295 (not $x1290)))
(let (($x1298 (and $x1173 $x1295)))
(let (($x1301 (not $x1298)))
(let (($x1317 (or $x1301 $x1312)))
(let (($x1320 (not $x1317)))
(let (($x1323 (or $x1320 $x1196)))
(let (($x1339 (and $x882 $x885 $x980 $x144 $x145 $x989 $x991 $x996 $x1323)))
(let (($x1329 (and $x882 $x885 $x985 $x104 $x107 $x109 $x989 $x991 $x996 $x1323)))
(let (($x1344 (or $x1329 $x1339)))
(let (($x1350 (and $x882 $x885 $x971 $x1344)))
(let (($x1145 (not (and $x1139 (not $x1142)))))
(let (($x1258 (or $x1145 $x1253)))
(let (($x1261 (not $x1258)))
(let (($x1129 (not (and (>= ?v0!3 0) (not $x1126)))))
(let (($x1132 (or $x1129 $x1131)))
(let (($x1264 (and $x1132 $x1261)))
(let (($x1119 (forall ((?v0 Int) )(let ((?x46 (v_b_array$ ?v0)))
(let (($x86 (= ?x46 v_b_max_G_4$)))
(let (($x838 (>= ?v0 0)))
(let (($x936 (and $x838 (not (<= (+ v_b_length$ (* (- 1) ?v0)) 0)))))
(let (($x939 (not $x936)))
(let (($x942 (or $x939 $x86)))
(not $x942))))))))
))
(let (($x1267 (or $x1119 $x1264)))
(let (($x1273 (and $x882 $x885 $x919 k!00 $x73 k!10 $x1267)))
(let (($x1355 (or $x1273 $x1350)))
(let (($x909 (forall ((?v0 Int) )(let (($x903 (<= (+ (v_b_array$ ?v0) (* (- 1) v_b_max_G_1$)) 0)))
(let (($x838 (>= ?v0 0)))
(let (($x895 (and $x838 (not (>= (+ ?v0 (* (- 1) v_b_p_G_0$)) 0)))))
(let (($x898 (not $x895)))
(or $x898 $x903))))))
))
(let (($x1361 (and $x882 $x885 $x909 $x63 $x1355)))
(let (($x1366 (or $x1095 $x1361)))
(let (($x862 (forall ((?v0 Int) )(let (($x851 (>= (+ v_b_max_G_0$ (* (- 1) (v_b_array$ ?v0))) 0)))
(let (($x838 (>= ?v0 0)))
(let (($x849 (and $x838 (not (>= ?v0 1)))))
(let (($x854 (not $x849)))
(or $x854 $x851))))))
))
(let (($x1369 (and $x862 $x1366)))
(let (($x1077 (not (and $x1078 $x1079))))
(let (($x1084 (or $x1077 $x1083)))
(let (($x1085 (not $x1084)))
(let (($x1372 (or $x1085 $x1369)))
(let ((@x1622 (rewrite (= (and $x882 $x885 $x980 $x144 $x145 $x989 $x991 $x996 $x1595) $x1620))))
(let (($x1012 (and $x838 (not $x1005))))
(let (($x1015 (not $x1012)))
(let (($x1023 (or $x1015 $x1020)))
(let ((@x1569 (monotonicity (rewrite (= $x1012 (not (or $x1399 $x1005)))) (= $x1015 (not (not (or $x1399 $x1005)))))))
(let ((@x1573 (trans @x1569 (rewrite (= (not (not (or $x1399 $x1005))) (or $x1399 $x1005))) (= $x1015 (or $x1399 $x1005)))))
(let ((@x1581 (trans (monotonicity @x1573 (= $x1023 (or (or $x1399 $x1005) $x1020))) (rewrite (= (or (or $x1399 $x1005) $x1020) $x1577)) (= $x1023 $x1577))))
(let ((@x1587 (monotonicity (quant-intro @x1581 (= $x1026 $x1582)) (= $x1196 (and $x1582 $x1193)))))
(let ((@x1547 (monotonicity (rewrite (= $x1298 (not (or $x1540 $x1290)))) (= $x1301 (not (not (or $x1540 $x1290)))))))
(let ((@x1551 (trans @x1547 (rewrite (= (not (not (or $x1540 $x1290))) (or $x1540 $x1290))) (= $x1301 (or $x1540 $x1290)))))
(let ((@x1559 (trans (monotonicity @x1551 (= $x1317 (or (or $x1540 $x1290) $x1312))) (rewrite (= (or (or $x1540 $x1290) $x1312) $x1555)) (= $x1317 $x1555))))
(let ((@x1597 (monotonicity (monotonicity @x1559 (= $x1320 $x1560)) (trans @x1587 (rewrite (= (and $x1582 $x1193) $x1590)) (= $x1196 $x1590)) (= $x1323 $x1595))))
(let ((@x1616 (monotonicity @x1597 (= $x1339 (and $x882 $x885 $x980 $x144 $x145 $x989 $x991 $x996 $x1595)))))
(let ((@x1611 (rewrite (= (and $x882 $x885 $x985 $x104 $x107 $x109 $x989 $x991 $x996 $x1595) $x1609))))
(let ((@x1600 (monotonicity @x1597 (= $x1329 (and $x882 $x885 $x985 $x104 $x107 $x109 $x989 $x991 $x996 $x1595)))))
(let ((@x1627 (monotonicity (trans @x1600 @x1611 (= $x1329 $x1609)) (trans @x1616 @x1622 (= $x1339 $x1620)) (= $x1344 $x1625))))
(let ((@x1637 (trans (monotonicity @x1627 (= $x1350 (and $x882 $x885 $x971 $x1625))) (rewrite (= (and $x882 $x885 $x971 $x1625) $x1633)) (= $x1350 $x1633))))
(let ((@x1537 (rewrite (= (and $x882 $x885 $x919 k!00 $x73 k!10 $x1522) $x1535))))
(let ((@x1496 (monotonicity (rewrite (= (and $x1139 (not $x1142)) (not (or $x1489 $x1142)))) (= $x1145 (not (not (or $x1489 $x1142)))))))
(let ((@x1500 (trans @x1496 (rewrite (= (not (not (or $x1489 $x1142))) (or $x1489 $x1142))) (= $x1145 (or $x1489 $x1142)))))
(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)))))
(let (($x1470 (or (not (>= ?v0!3 0)) $x1126)))
(let ((@x1476 (monotonicity (rewrite (= (and (>= ?v0!3 0) (not $x1126)) (not $x1470))) (= $x1129 (not (not $x1470))))))
(let ((@x1483 (monotonicity (trans @x1476 (rewrite (= (not (not $x1470)) $x1470)) (= $x1129 $x1470)) (= $x1132 (or $x1470 $x1131)))))
(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)))))))
(let ((@x1521 (trans @x1514 (rewrite (= (and $x1484 (not (or $x1489 $x1142 $x1253))) $x1517)) (= $x1264 $x1517))))
(let (($x936 (and $x838 (not $x930))))
(let (($x939 (not $x936)))
(let (($x942 (or $x939 $x86)))
(let ((@x1450 (monotonicity (rewrite (= $x936 (not (or $x1399 $x930)))) (= $x939 (not (not (or $x1399 $x930)))))))
(let ((@x1454 (trans @x1450 (rewrite (= (not (not (or $x1399 $x930))) (or $x1399 $x930))) (= $x939 (or $x1399 $x930)))))
(let ((@x1462 (trans (monotonicity @x1454 (= $x942 (or (or $x1399 $x930) $x86))) (rewrite (= (or (or $x1399 $x930) $x86) $x1458)) (= $x942 $x1458))))
(let ((@x1468 (quant-intro (monotonicity @x1462 (= (not $x942) $x1463)) (= $x1119 $x1466))))
(let ((@x1527 (monotonicity (monotonicity @x1468 @x1521 (= $x1267 $x1522)) (= $x1273 (and $x882 $x885 $x919 k!00 $x73 k!10 $x1522)))))
(let (($x895 (and $x838 (not $x888))))
(let (($x898 (not $x895)))
(let (($x906 (or $x898 $x903)))
(let ((@x1428 (monotonicity (rewrite (= $x895 (not (or $x1399 $x888)))) (= $x898 (not (not (or $x1399 $x888)))))))
(let ((@x1432 (trans @x1428 (rewrite (= (not (not (or $x1399 $x888))) (or $x1399 $x888))) (= $x898 (or $x1399 $x888)))))
(let ((@x1440 (trans (monotonicity @x1432 (= $x906 (or (or $x1399 $x888) $x903))) (rewrite (= (or (or $x1399 $x888) $x903) $x1436)) (= $x906 $x1436))))
(let ((@x1643 (monotonicity (quant-intro @x1440 (= $x909 $x1441)) (monotonicity (trans @x1527 @x1537 (= $x1273 $x1535)) @x1637 (= $x1355 $x1638)) (= $x1361 (and $x882 $x885 $x1441 $x63 $x1638)))))
(let ((@x1652 (trans @x1643 (rewrite (= (and $x882 $x885 $x1441 $x63 $x1638) $x1648)) (= $x1361 $x1648))))
(let (($x849 (and $x838 (not $x841))))
(let (($x854 (not $x849)))
(let (($x859 (or $x854 $x851)))
(let ((@x1406 (monotonicity (rewrite (= $x849 (not (or $x1399 $x841)))) (= $x854 (not (not (or $x1399 $x841)))))))
(let ((@x1410 (trans @x1406 (rewrite (= (not (not (or $x1399 $x841))) (or $x1399 $x841))) (= $x854 (or $x1399 $x841)))))
(let ((@x1418 (trans (monotonicity @x1410 (= $x859 (or (or $x1399 $x841) $x851))) (rewrite (= (or (or $x1399 $x841) $x851) $x1414)) (= $x859 $x1414))))
(let ((@x1658 (monotonicity (quant-intro @x1418 (= $x862 $x1419)) (monotonicity @x1652 (= $x1366 $x1653)) (= $x1369 (and $x1419 $x1653)))))
(let ((@x1385 (rewrite (= (not (not (or (not $x1078) $x831))) (or (not $x1078) $x831)))))
(let ((@x1383 (monotonicity (rewrite (= (and $x1078 $x1079) (not (or (not $x1078) $x831)))) (= $x1077 (not (not (or (not $x1078) $x831)))))))
(let ((@x1390 (monotonicity (trans @x1383 @x1385 (= $x1077 (or (not $x1078) $x831))) (= $x1084 (or (or (not $x1078) $x831) $x1083)))))
(let ((@x1395 (trans @x1390 (rewrite (= (or (or (not $x1078) $x831) $x1083) $x1391)) (= $x1084 $x1391))))
(let ((@x1669 (monotonicity (monotonicity @x1395 (= $x1085 $x1396)) (trans @x1658 (rewrite (= (and $x1419 $x1653) $x1662)) (= $x1369 $x1662)) (= $x1372 $x1667))))
(let (($x1181 (<= (+ ?x1179 (* (- 1) v_b_max_G_3$)) 0)))
(let (($x1182 (or (not (and $x1173 (not (>= (+ ?v0!5 (* (- 1) v_b_p_G_1$)) 0)))) $x1181)))
(let (($x1183 (not $x1182)))
(let (($x1200 (or $x1183 $x1196)))
(let (($x1041 (and $x882 $x885 $x980 $x144 $x145 $x989 $x991 $x996)))
(let (($x1044 (not $x1041)))
(let (($x1208 (not $x1044)))
(let (($x1211 (and $x1208 $x1200)))
(let (($x999 (and $x882 $x885 $x985 $x104 $x107 $x109 $x989 $x991 $x996)))
(let (($x1002 (not $x999)))
(let (($x1169 (not $x1002)))
(let (($x1204 (and $x1169 $x1200)))
(let (($x1215 (or $x1204 $x1211)))
(let (($x974 (and $x882 $x885 $x971)))
(let (($x977 (not $x974)))
(let (($x1166 (not $x977)))
(let (($x1219 (and $x1166 $x1215)))
(let (($x1150 (not (or $x1145 (<= (+ (v_b_array$ ?v0!4) (* (- 1) v_b_max_G_4$)) 0)))))
(let (($x1154 (and $x1132 $x1150)))
(let (($x1158 (or $x1119 $x1154)))
(let (($x922 (and $x882 $x885 $x919 k!00 $x73 k!10)))
(let (($x925 (not $x922)))
(let (($x1113 (not $x925)))
(let (($x1162 (and $x1113 $x1158)))
(let (($x1223 (or $x1162 $x1219)))
(let (($x912 (and $x882 $x885 $x909 $x63)))
(let (($x1227 (and $x912 $x1223)))
(let (($x1231 (or $x1095 $x1227)))
(let (($x1235 (and $x862 $x1231)))
(let (($x1239 (or $x1085 $x1235)))
(let (($x1305 (= (+ ?x1179 (* (- 1) v_b_max_G_3$)) (+ (* (- 1) v_b_max_G_3$) ?x1179))))
(let ((@x1309 (monotonicity (rewrite $x1305) (= $x1181 (<= (+ (* (- 1) v_b_max_G_3$) ?x1179) 0)))))
(let ((@x1316 (trans @x1309 (rewrite (= (<= (+ (* (- 1) v_b_max_G_3$) ?x1179) 0) $x1312)) (= $x1181 $x1312))))
(let (($x1302 (= (not (and $x1173 (not (>= (+ ?v0!5 (* (- 1) v_b_p_G_1$)) 0)))) $x1301)))
(let (($x1299 (= (and $x1173 (not (>= (+ ?v0!5 (* (- 1) v_b_p_G_1$)) 0))) $x1298)))
(let (($x1175 (>= (+ ?v0!5 (* (- 1) v_b_p_G_1$)) 0)))
(let (($x1283 (= (+ ?v0!5 (* (- 1) v_b_p_G_1$)) (+ (* (- 1) v_b_p_G_1$) ?v0!5))))
(let ((@x1287 (monotonicity (rewrite $x1283) (= $x1175 (>= (+ (* (- 1) v_b_p_G_1$) ?v0!5) 0)))))
(let ((@x1294 (trans @x1287 (rewrite (= (>= (+ (* (- 1) v_b_p_G_1$) ?v0!5) 0) $x1290)) (= $x1175 $x1290))))
(let ((@x1303 (monotonicity (monotonicity (monotonicity @x1294 (= (not $x1175) $x1295)) $x1299) $x1302)))
(let ((@x1322 (monotonicity (monotonicity @x1303 @x1316 (= $x1182 $x1317)) (= $x1183 $x1320))))
(let ((@x1338 (monotonicity (rewrite (= $x1208 $x1041)) (monotonicity @x1322 (= $x1200 $x1323)) (= $x1211 (and $x1041 $x1323)))))
(let ((@x1328 (monotonicity (rewrite (= $x1169 $x999)) (monotonicity @x1322 (= $x1200 $x1323)) (= $x1204 (and $x999 $x1323)))))
(let ((@x1346 (monotonicity (trans @x1328 (rewrite (= (and $x999 $x1323) $x1329)) (= $x1204 $x1329)) (trans @x1338 (rewrite (= (and $x1041 $x1323) $x1339)) (= $x1211 $x1339)) (= $x1215 $x1344))))
(let ((@x1349 (monotonicity (rewrite (= $x1166 $x974)) @x1346 (= $x1219 (and $x974 $x1344)))))
(let (($x1259 (= (or $x1145 (<= (+ (v_b_array$ ?v0!4) (* (- 1) v_b_max_G_4$)) 0)) $x1258)))
(let (($x1148 (<= (+ (v_b_array$ ?v0!4) (* (- 1) v_b_max_G_4$)) 0)))
(let (($x1254 (= (<= (+ (* (- 1) v_b_max_G_4$) (v_b_array$ ?v0!4)) 0) $x1253)))
(let (($x1249 (= $x1148 (<= (+ (* (- 1) v_b_max_G_4$) (v_b_array$ ?v0!4)) 0))))
(let (($x1246 (= (+ (v_b_array$ ?v0!4) (* (- 1) v_b_max_G_4$)) (+ (* (- 1) v_b_max_G_4$) (v_b_array$ ?v0!4)))))
(let ((@x1257 (trans (monotonicity (rewrite $x1246) $x1249) (rewrite $x1254) (= $x1148 $x1253))))
(let ((@x1266 (monotonicity (monotonicity (monotonicity @x1257 $x1259) (= $x1150 $x1261)) (= $x1154 $x1264))))
(let ((@x1272 (monotonicity (rewrite (= $x1113 $x922)) (monotonicity @x1266 (= $x1158 $x1267)) (= $x1162 (and $x922 $x1267)))))
(let ((@x1357 (monotonicity (trans @x1272 (rewrite (= (and $x922 $x1267) $x1273)) (= $x1162 $x1273)) (trans @x1349 (rewrite (= (and $x974 $x1344) $x1350)) (= $x1219 $x1350)) (= $x1223 $x1355))))
(let ((@x1365 (trans (monotonicity @x1357 (= $x1227 (and $x912 $x1355))) (rewrite (= (and $x912 $x1355) $x1361)) (= $x1227 $x1361))))
(let ((@x1374 (monotonicity (monotonicity (monotonicity @x1365 (= $x1231 $x1366)) (= $x1235 $x1369)) (= $x1239 $x1372))))
(let (($x1029 (not $x1026)))
(let (($x1032 (or $x1029 $x136)))
(let (($x1035 (and $x1026 $x1032)))
(let (($x1047 (or $x1044 $x1035)))
(let (($x1038 (or $x1002 $x1035)))
(let (($x1050 (and $x1038 $x1047)))
(let (($x1053 (or $x977 $x1050)))
(let (($x959 (forall ((?v0 Int) )(let (($x838 (>= ?v0 0)))
(let (($x936 (and $x838 (not (<= (+ v_b_length$ (* (- 1) ?v0)) 0)))))
(let (($x939 (not $x936)))
(or $x939 (<= (+ (v_b_array$ ?v0) (* (- 1) v_b_max_G_4$)) 0))))))
))
(let (($x945 (exists ((?v0 Int) )(let ((?x46 (v_b_array$ ?v0)))
(let (($x86 (= ?x46 v_b_max_G_4$)))
(let (($x838 (>= ?v0 0)))
(let (($x936 (and $x838 (not (<= (+ v_b_length$ (* (- 1) ?v0)) 0)))))
(let (($x939 (not $x936)))
(or $x939 $x86)))))))
))
(let (($x948 (not $x945)))
(let (($x962 (or $x948 $x959)))
(let (($x965 (and $x945 $x962)))
(let (($x968 (or $x925 $x965)))
(let (($x1056 (and $x968 $x1053)))
(let (($x915 (not $x912)))
(let (($x1059 (or $x915 $x1056)))
(let (($x1062 (and $x50 $x1059)))
(let (($x878 (not $x862)))
(let (($x1065 (or $x878 $x1062)))
(let (($x1071 (not (and $x862 $x1065))))
(let ((@x1192 (nnf-neg (nnf-pos (refl (~ $x1023 $x1023)) (~ $x1026 $x1026)) (~ (not $x1029) $x1026))))
(let ((@x1203 (nnf-neg (sk (~ $x1029 $x1183)) (nnf-neg @x1192 (refl (~ $x1193 $x1193)) (~ (not $x1032) $x1196)) (~ (not $x1035) $x1200))))
(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))))
(let ((@x1157 (nnf-neg (nnf-neg (sk (~ $x945 $x1132)) (~ (not $x948) $x1132)) (sk (~ (not $x959) $x1150)) (~ (not $x962) $x1154))))
(let ((@x1161 (nnf-neg (nnf-neg (refl (~ (not $x942) (not $x942))) (~ $x948 $x1119)) @x1157 (~ (not $x965) $x1158))))
(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))))
(let ((@x1109 (monotonicity (refl (~ $x882 $x882)) (refl (~ $x885 $x885)) (nnf-pos (refl (~ $x906 $x906)) (~ $x909 $x909)) (refl (~ $x63 $x63)) (~ $x912 $x912))))
(let ((@x1230 (nnf-neg (nnf-neg @x1109 (~ (not $x915) $x912)) @x1226 (~ (not $x1059) $x1227))))
(let ((@x1094 (nnf-neg (nnf-pos (refl (~ $x859 $x859)) (~ $x862 $x862)) (~ (not $x878) $x862))))
(let ((@x1238 (nnf-neg @x1094 (nnf-neg (refl (~ $x1095 $x1095)) @x1230 (~ (not $x1062) $x1231)) (~ (not $x1065) $x1235))))
(let (($x749 (and $x52 $x54 $x69 k!00 $x73 k!10)))
(let (($x752 (not $x749)))
(let (($x785 (or $x752 $x403)))
(let (($x788 (and $x785 $x682)))
(let (($x738 (not $x279)))
(let (($x816 (or $x738 $x788)))
(let (($x819 (and $x50 $x816)))
(let (($x822 (or $x705 $x819)))
(let (($x825 (and $x234 $x822)))
(let (($x828 (not $x825)))
(let ((@x1011 (monotonicity (rewrite (= (<= v_b_p_G_1$ ?0) $x1005)) (= $x557 (not $x1005)))))
(let ((@x837 (rewrite (= $x43 $x838))))
(let ((@x1017 (monotonicity (monotonicity @x837 @x1011 (= $x560 $x1012)) (= (not $x560) $x1015))))
(let ((@x1028 (quant-intro (monotonicity @x1017 (rewrite (= $x132 $x1020)) (= $x567 $x1023)) (= $x572 $x1026))))
(let ((@x1034 (monotonicity (monotonicity @x1028 (= (not $x572) $x1029)) (= $x595 $x1032))))
(let ((@x886 (rewrite (= $x54 $x885))))
(let ((@x883 (rewrite (= $x52 $x882))))
(let ((@x1043 (monotonicity @x883 @x886 (rewrite (= $x143 $x980)) (rewrite (= $x110 $x989)) (rewrite (= $x456 $x991)) (rewrite (= $x116 $x996)) (= $x654 $x1041))))
(let ((@x1049 (monotonicity (monotonicity @x1043 (= $x669 $x1044)) (monotonicity @x1028 @x1034 (= $x600 $x1035)) (= $x670 $x1047))))
(let ((@x1001 (monotonicity @x883 @x886 (monotonicity (rewrite (= $x143 $x980)) (= $x441 $x985)) (rewrite (= $x110 $x989)) (rewrite (= $x456 $x991)) (rewrite (= $x116 $x996)) (= $x544 $x999))))
(let ((@x1040 (monotonicity (monotonicity @x1001 (= $x606 $x1002)) (monotonicity @x1028 @x1034 (= $x600 $x1035)) (= $x607 $x1038))))
(let ((@x976 (monotonicity @x883 @x886 (monotonicity (rewrite (= $x69 $x919)) (= $x415 $x971)) (= $x429 $x974))))
(let ((@x1055 (monotonicity (monotonicity @x976 (= $x681 $x977)) (monotonicity @x1040 @x1049 (= $x675 $x1050)) (= $x682 $x1053))))
(let ((@x935 (monotonicity (rewrite (= (<= v_b_length$ ?0) $x930)) (= $x351 (not $x930)))))
(let ((@x941 (monotonicity (monotonicity @x837 @x935 (= $x354 $x936)) (= $x360 $x939))))
(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))))))
(let ((@x950 (monotonicity (quant-intro (monotonicity @x941 (= $x361 $x942)) (= $x366 $x945)) (= (not $x366) $x948))))
(let ((@x967 (monotonicity (quant-intro (monotonicity @x941 (= $x361 $x942)) (= $x366 $x945)) (monotonicity @x950 (quant-intro @x958 (= $x377 $x959)) (= $x398 $x962)) (= $x403 $x965))))
(let ((@x927 (monotonicity (monotonicity @x883 @x886 (rewrite (= $x69 $x919)) (= $x749 $x922)) (= $x752 $x925))))
(let ((@x1058 (monotonicity (monotonicity @x927 @x967 (= $x785 $x968)) @x1055 (= $x788 $x1056))))
(let ((@x894 (monotonicity (rewrite (= (<= v_b_p_G_0$ ?0) $x888)) (= $x244 (not $x888)))))
(let ((@x900 (monotonicity (monotonicity @x837 @x894 (= $x247 $x895)) (= (not $x247) $x898))))
(let ((@x911 (quant-intro (monotonicity @x900 (rewrite (= $x59 $x903)) (= $x254 $x906)) (= $x259 $x909))))
(let ((@x917 (monotonicity (monotonicity @x883 @x886 @x911 (= $x279 $x912)) (= $x738 $x915))))
(let ((@x1064 (monotonicity (monotonicity @x917 @x1058 (= $x816 $x1059)) (= $x819 $x1062))))
(let ((@x848 (monotonicity (rewrite (= (<= 1 ?0) $x841)) (= (not (<= 1 ?0)) (not $x841)))))
(let ((@x834 (monotonicity (monotonicity @x837 @x848 (= (and $x43 (not (<= 1 ?0))) $x849)) (= (not (and $x43 (not (<= 1 ?0)))) $x854))))
(let ((@x877 (quant-intro (monotonicity @x834 (rewrite (= $x47 $x851)) (= $x229 $x859)) (= $x234 $x862))))
(let ((@x1067 (monotonicity (monotonicity @x877 (= $x705 $x878)) @x1064 (= $x822 $x1065))))
(let ((@x1073 (monotonicity (monotonicity @x877 @x1067 (= $x825 (and $x862 $x1065))) (= $x828 $x1071))))
(let ((@x796 (monotonicity (monotonicity @x238 @x240 @x450 @x460 @x463 (= $x654 $x654)) (= $x669 $x669))))
(let ((@x784 (monotonicity (monotonicity @x238 @x240 @x450 @x460 @x463 (= $x544 $x544)) (= $x606 $x606))))
(let ((@x800 (monotonicity (monotonicity @x784 (= $x607 $x607)) (monotonicity @x796 (= $x670 $x670)) (= $x675 $x675))))
(let ((@x780 (monotonicity (monotonicity @x238 @x240 (= $x429 $x429)) (= $x681 $x681))))
(let ((@x846 (monotonicity (monotonicity @x238 @x240 (= $x749 $x749)) (= $x752 $x752))))
(let ((@x864 (monotonicity (monotonicity @x846 (= $x785 $x785)) (monotonicity @x780 @x800 (= $x682 $x682)) (= $x788 $x788))))
(let ((@x762 (monotonicity (monotonicity @x238 @x240 (= $x279 $x279)) (= $x738 $x738))))
(let ((@x868 (monotonicity (monotonicity @x762 @x864 (= $x816 $x816)) (= $x819 $x819))))
(let ((@x874 (monotonicity (monotonicity (monotonicity @x868 (= $x822 $x822)) (= $x825 $x825)) (= $x828 $x828))))
(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))))
(let ((@x790 (monotonicity (monotonicity (monotonicity @x751 (= $x409 $x752)) (= $x410 $x785)) (= $x687 $x788))))
(let ((@x821 (monotonicity (monotonicity @x790 (= (or $x738 $x687) $x816)) (= (and $x50 (or $x738 $x687)) $x819))))
(let ((@x827 (monotonicity (monotonicity @x821 (= (or $x705 (and $x50 (or $x738 $x687))) $x822)) (= (and $x234 (or $x705 (and $x50 (or $x738 $x687)))) $x825))))
(let ((@x830 (monotonicity @x827 (= (not (and $x234 (or $x705 (and $x50 (or $x738 $x687))))) $x828))))
(let (($x739 (or $x738 $x687)))
(let (($x740 (and $x50 $x739)))
(let (($x741 (or $x705 $x740)))
(let (($x742 (and $x234 $x741)))
(let (($x743 (not $x742)))
(let ((@x766 (monotonicity (monotonicity @x238 @x240 (= $x338 $x338)) (= $x409 $x409))))
(let ((@x804 (monotonicity (monotonicity @x766 (= $x410 $x410)) (monotonicity @x780 @x800 (= $x682 $x682)) (= $x687 $x687))))
(let ((@x808 (monotonicity (monotonicity @x762 @x804 (= $x739 $x739)) (= $x740 $x740))))
(let ((@x814 (monotonicity (monotonicity (monotonicity @x808 (= $x741 $x741)) (= $x742 $x742)) (= $x743 $x743))))
(let ((@x746 (mp (not-or-elim @x726 (not $x711)) (rewrite* (= (not $x711) $x743)) $x743)))
(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)))
(let ((@x2191 (mp (mp (mp @x1242 @x1374 $x1372) @x1669 $x1667) (monotonicity @x2187 (= $x1667 (or $x1396 $x2185))) (or $x1396 $x2185))))
(let ((@x2302 (unit-resolution (def-axiom (or $x2182 $x2176)) (unit-resolution @x2191 (lemma @x1930 $x1391) $x2185) $x2176)))
(let ((@x2309 (unit-resolution (def-axiom (or $x2179 $x1095 $x2173)) (mp @x737 (symm (commutativity (= $x50 $x31)) (= $x31 $x50)) $x50) (or $x2179 $x2173))))
(let ((@x2310 (unit-resolution @x2309 @x2302 $x2173)))
(let ((@x2410 (monotonicity (unit-resolution (def-axiom (or $x2146 $x144)) @x2389 $x144) (= ?x135 ?x62))))
(let ((@x2413 (trans @x2410 (unit-resolution (def-axiom (or $x2170 $x63)) @x2310 $x63) (= ?x135 v_b_max_G_1$))))
(let ((@x2414 (trans @x2413 (symm (unit-resolution (def-axiom (or $x2146 $x145)) @x2389 $x145) $x2022) $x136)))
(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)))
(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)))
(let (($x1798 (= v_b_p_G_0$ ?v0!5)))
(let (($x1800 (>= (+ v_b_p_G_0$ (* (- 1) ?v0!5)) 0)))
(let (($x1764 (>= (+ v_b_p_G_0$ (* (- 1) v_b_p_G_1$)) (- 1))))
(let ((@x2426 (unit-resolution ((_ th-lemma arith triangle-eq) (or $x1605 $x1764)) (unit-resolution (def-axiom (or $x2146 $x991)) @x2389 $x991) $x1764)))
(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)))
(let (($x1751 (<= (+ v_b_p_G_0$ (* (- 1) ?v0!5)) 0)))
(let (($x1728 (>= (+ v_b_max_G_1$ (* (- 1) ?x1179)) 0)))
(let (($x2195 (not $x1728)))
(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)))
(let ((@x2333 (unit-resolution (def-axiom (or $x2170 $x2095)) @x2310 $x2095)))
(let (($x1716 (or $x2100 $x1540 $x1751 $x1728)))
(let (($x1775 (<= (+ ?x1179 (* (- 1) v_b_max_G_1$)) 0)))
(let (($x1789 (>= (+ ?v0!5 (* (- 1) v_b_p_G_0$)) 0)))
(let (($x1717 (or $x2100 (or $x1540 $x1789 $x1775))))
(let (($x1739 (= (+ ?x1179 (* (- 1) v_b_max_G_1$)) (+ (* (- 1) v_b_max_G_1$) ?x1179))))
(let ((@x1726 (monotonicity (rewrite $x1739) (= $x1775 (<= (+ (* (- 1) v_b_max_G_1$) ?x1179) 0)))))
(let ((@x1732 (trans @x1726 (rewrite (= (<= (+ (* (- 1) v_b_max_G_1$) ?x1179) 0) $x1728)) (= $x1775 $x1728))))
(let (($x1743 (= (+ ?v0!5 (* (- 1) v_b_p_G_0$)) (+ (* (- 1) v_b_p_G_0$) ?v0!5))))
(let ((@x1749 (monotonicity (rewrite $x1743) (= $x1789 (>= (+ (* (- 1) v_b_p_G_0$) ?v0!5) 0)))))
(let ((@x1755 (trans @x1749 (rewrite (= (>= (+ (* (- 1) v_b_p_G_0$) ?v0!5) 0) $x1751)) (= $x1789 $x1751))))
(let ((@x1715 (monotonicity @x1755 @x1732 (= (or $x1540 $x1789 $x1775) (or $x1540 $x1751 $x1728)))))
(let ((@x1690 (trans (monotonicity @x1715 (= $x1717 (or $x2100 (or $x1540 $x1751 $x1728)))) (rewrite (= (or $x2100 (or $x1540 $x1751 $x1728)) $x1716)) (= $x1717 $x1716))))
(let ((@x2435 (unit-resolution (mp ((_ quant-inst ?v0!5) $x1717) @x1690 $x1716) @x2333 (unit-resolution (def-axiom (or $x1555 $x1173)) @x2416 $x1173) @x2433 $x1751)))
(let ((@x2436 (unit-resolution ((_ th-lemma arith triangle-eq) (or $x1798 (not $x1751) (not $x1800))) @x2435 @x2430 $x1798)))
(let ((@x1807 (monotonicity (symm (hypothesis $x1798) (= ?v0!5 v_b_p_G_0$)) (= ?x1179 ?x101))))
(let ((@x1796 (lemma (unit-resolution (hypothesis $x1803) (symm @x1807 $x1799) false) (or (not $x1798) $x1799))))
(let ((@x2437 (unit-resolution @x1796 @x2436 (unit-resolution ((_ th-lemma arith triangle-eq) (or $x1803 $x1703)) @x2421 $x1803) false)))
(let (($x2228 (= v_b_max_G_1$ v_b_max_G_4$)))
(let ((@x2349 (symm (unit-resolution (def-axiom (or $x2114 $x73)) (hypothesis $x2117) $x73) $x2228)))
(let ((@x2352 ((_ th-lemma arith triangle-eq) (or (not $x2228) (<= (+ v_b_max_G_1$ (* (- 1) v_b_max_G_4$)) 0)))))
(let ((@x2353 (unit-resolution @x2352 @x2349 (<= (+ v_b_max_G_1$ (* (- 1) v_b_max_G_4$)) 0))))
(let (($x2265 (>= (+ v_b_max_G_1$ (* (- 1) (v_b_array$ ?v0!4))) 0)))
(let (($x1143 (not $x1142)))
(let (($x2077 (not $x2103)))
(let (($x2282 (= ?x62 v_b_max_G_4$)))
(let (($x2283 (or $x1528 (<= (+ v_b_length$ (* (- 1) v_b_k_G_0$)) 0) $x2282)))
(let ((@x2313 (trans (unit-resolution (def-axiom (or $x2170 $x63)) @x2310 $x63) (symm (hypothesis $x73) $x2228) $x2282)))
(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)))
(let ((@x2355 (unit-resolution (lemma @x2316 (or $x2077 $x1531)) (unit-resolution (def-axiom (or $x2114 $x73)) (hypothesis $x2117) $x73) $x2077)))
(let ((@x2356 (unit-resolution (def-axiom (or $x2111 $x2103 $x1517)) @x2355 (unit-resolution (def-axiom (or $x2114 $x2108)) (hypothesis $x2117) $x2108) $x1517)))
(let ((@x2343 ((_ th-lemma arith farkas -1 -1 1) (hypothesis (<= (+ v_b_p_G_0$ (* (- 1) ?v0!4)) 0)) (hypothesis $x919) (hypothesis $x1143) false)))
(let ((@x2346 (lemma @x2343 (or (not (<= (+ v_b_p_G_0$ (* (- 1) ?v0!4)) 0)) $x971 $x1142))))
(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)))))
(let (($x2272 (<= (+ v_b_p_G_0$ (* (- 1) ?v0!4)) 0)))
(let (($x2296 (or $x2100 $x1489 $x2272 $x2265)))
(let (($x2249 (<= (+ (v_b_array$ ?v0!4) (* (- 1) v_b_max_G_1$)) 0)))
(let (($x2241 (>= (+ ?v0!4 (* (- 1) v_b_p_G_0$)) 0)))
(let (($x2300 (or $x2100 (or $x1489 $x2241 $x2249))))
(let (($x2266 (= (<= (+ (* (- 1) v_b_max_G_1$) (v_b_array$ ?v0!4)) 0) $x2265)))
(let (($x2260 (= $x2249 (<= (+ (* (- 1) v_b_max_G_1$) (v_b_array$ ?v0!4)) 0))))
(let (($x2278 (= (+ (v_b_array$ ?v0!4) (* (- 1) v_b_max_G_1$)) (+ (* (- 1) v_b_max_G_1$) (v_b_array$ ?v0!4)))))
(let ((@x2292 (trans (monotonicity (rewrite $x2278) $x2260) (rewrite $x2266) (= $x2249 $x2265))))
(let (($x2253 (= (+ ?v0!4 (* (- 1) v_b_p_G_0$)) (+ (* (- 1) v_b_p_G_0$) ?v0!4))))
(let ((@x2258 (monotonicity (rewrite $x2253) (= $x2241 (>= (+ (* (- 1) v_b_p_G_0$) ?v0!4) 0)))))
(let ((@x2276 (trans @x2258 (rewrite (= (>= (+ (* (- 1) v_b_p_G_0$) ?v0!4) 0) $x2272)) (= $x2241 $x2272))))
(let ((@x2295 (monotonicity @x2276 @x2292 (= (or $x1489 $x2241 $x2249) (or $x1489 $x2272 $x2265)))))
(let ((@x2319 (trans (monotonicity @x2295 (= $x2300 (or $x2100 (or $x1489 $x2272 $x2265)))) (rewrite (= (or $x2100 (or $x1489 $x2272 $x2265)) $x2296)) (= $x2300 $x2296))))
(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))))
(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)))
(let ((@x2373 (unit-resolution (def-axiom (or $x2167 $x2117 $x2161)) (lemma @x2365 $x2114) (unit-resolution (def-axiom (or $x2170 $x2164)) @x2310 $x2164) $x2161)))
(let ((@x2243 (unit-resolution (def-axiom (or $x2155 $x2143 $x2149)) (unit-resolution (def-axiom (or $x2158 $x2152)) @x2373 $x2152) $x2152)))
(let ((@x2244 (unit-resolution @x2243 (lemma @x2437 $x2146) $x2143)))
(let ((@x1791 (trans (monotonicity (hypothesis $x107) (= ?x135 ?x101)) (symm (hypothesis $x104) (= ?x101 v_b_max_G_2$)) (= ?x135 v_b_max_G_2$))))
(let ((@x1769 (trans @x1791 (symm (hypothesis $x109) (= v_b_max_G_2$ v_b_max_G_3$)) $x136)))
(let ((@x1771 (lemma (unit-resolution (hypothesis $x1193) @x1769 false) (or $x136 $x1603 $x1601 $x1602))))
(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)))
(let ((@x2368 (unit-resolution ((_ th-lemma arith triangle-eq) (or $x1605 $x1764)) (unit-resolution (def-axiom (or $x2140 $x991)) @x2244 $x991) $x1764)))
(let ((@x1699 (unit-resolution (def-axiom (or $x2137 $x1560 $x2131)) (unit-resolution (def-axiom (or $x2128 $x1193)) (hypothesis $x136) $x2128) (hypothesis $x2134) $x1560)))
(let (($x2205 (not $x1800)))
(let (($x1838 (<= (+ ?x101 (* (- 1) v_b_max_G_3$)) 0)))
(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$))))
(let ((@x1675 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not (= ?x101 v_b_max_G_3$)) $x1838)) @x1685 $x1838)))
(let ((@x1696 (lemma ((_ th-lemma arith farkas -1 -1 1) (hypothesis $x1678) (hypothesis $x1838) (hypothesis $x1703) false) (or $x1693 $x1312 (not $x1838)))))
(let ((@x1677 (unit-resolution @x1696 (unit-resolution (def-axiom (or $x1555 $x1678)) @x1699 $x1678) @x1675 $x1693)))
(let ((@x2193 (unit-resolution @x1796 (unit-resolution ((_ th-lemma arith triangle-eq) (or $x1803 $x1703)) @x1677 $x1803) (not $x1798))))
(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)))
(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))))
(let ((@x2209 (unit-resolution ((_ th-lemma arith triangle-eq) (or $x1798 (not $x1751) $x2205)) (unit-resolution @x2202 @x2198 $x1751) (or $x1798 $x2205))))
(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)))
(let ((@x2370 (unit-resolution (lemma @x2211 (or $x1193 (not $x1764) $x2100 $x980 $x2137 $x1601 $x1603)) @x2333 (or $x1193 (not $x1764) $x980 $x2137 $x1601 $x1603))))
(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)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))