src/HOL/SMT_Examples/Boogie_Max.certs

auto update;

9c420ec314a920506e90cf4b4e40b4ee3ab35dec 778 0
unsat
((set-logic AUFLIA)
(declare-fun ?v0!3 () Int)
(declare-fun ?v0!2 () Int)
(declare-fun ?v0!1 () Int)
(declare-fun ?v0!0 () Int)
(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 (($x1878 (forall ((?v0 Int) )(! (let (($x746 (<= (+ (v_b_array$ ?v0) (* (- 1) v_b_max_G_3$)) 0)))
(let (($x733 (>= (+ ?v0 (* (- 1) v_b_p_G_1$)) 0)))
(let (($x521 (>= ?v0 0)))
(let (($x1157 (not $x521)))
(or $x1157 $x733 $x746))))) :pattern ( (v_b_array$ ?v0) ) :qid k!17))
))
(let (($x1883 (not $x1878)))
(let (($x1886 (or $x1883 $x136)))
(let (($x1889 (not $x1886)))
(let (($x1070 (>= (+ v_b_max_G_3$ (* (- 1) (v_b_array$ ?v0!3))) 0)))
(let (($x1048 (<= (+ v_b_p_G_1$ (* (- 1) ?v0!3)) 0)))
(let (($x931 (>= ?v0!3 0)))
(let (($x1298 (not $x931)))
(let (($x1313 (or $x1298 $x1048 $x1070)))
(let (($x1318 (not $x1313)))
(let (($x1892 (or $x1318 $x1889)))
(let (($x1895 (not $x1892)))
(let (($x682 (>= v_b_p_G_1$ 2)))
(let (($x1364 (not $x682)))
(let (($x679 (>= v_b_k_G_1$ 0)))
(let (($x1363 (not $x679)))
(let ((?x685 (* (- 1) v_b_p_G_1$)))
(let ((?x686 (+ v_b_p_G_0$ ?x685)))
(let (($x684 (= ?x686 (- 1))))
(let (($x1362 (not $x684)))
(let (($x573 (>= v_b_p_G_0$ 1)))
(let (($x1287 (not $x573)))
(let (($x1361 (not $x109)))
(let (($x107 (= v_b_k_G_1$ v_b_p_G_0$)))
(let (($x1360 (not $x107)))
(let ((?x101 (v_b_array$ v_b_p_G_0$)))
(let (($x104 (= v_b_max_G_2$ ?x101)))
(let (($x1359 (not $x104)))
(let (($x689 (>= (+ v_b_max_G_1$ (* (- 1) ?x101)) 0)))
(let (($x571 (>= v_b_k_G_0$ 0)))
(let (($x1286 (not $x571)))
(let (($x1898 (or $x1286 $x689 $x1359 $x1360 $x1361 $x1287 $x1362 $x1363 $x1364 $x1895)))
(let (($x1901 (not $x1898)))
(let (($x145 (= v_b_max_G_3$ v_b_max_G_1$)))
(let (($x1376 (not $x145)))
(let (($x144 (= v_b_k_G_1$ v_b_k_G_0$)))
(let (($x1375 (not $x144)))
(let (($x692 (not $x689)))
(let (($x1904 (or $x692 $x1286 $x1375 $x1376 $x1287 $x1362 $x1363 $x1364 $x1895)))
(let ((?x937 (v_b_array$ ?v0!3)))
(let (($x1559 (= ?x101 ?x937)))
(let (($x1563 (not $x1559)))
(let ((?x1068 (* (- 1) ?x937)))
(let ((?x1461 (+ ?x101 ?x1068)))
(let (($x1445 (>= ?x1461 0)))
(let (($x1453 (not $x1445)))
(let (($x1907 (not $x1904)))
(let ((@x2130 (hypothesis $x1907)))
(let ((?x744 (* (- 1) v_b_max_G_3$)))
(let ((?x1781 (+ v_b_max_G_1$ ?x744)))
(let (($x1782 (<= ?x1781 0)))
(let (($x1780 (= v_b_max_G_1$ v_b_max_G_3$)))
(let ((@x2143 (mp (unit-resolution (def-axiom (or $x1904 $x145)) @x2130 $x145) (symm (commutativity (= $x1780 $x145)) (= $x145 $x1780)) $x1780)))
(let (($x1436 (not $x1070)))
(let ((?x62 (v_b_array$ v_b_k_G_0$)))
(let (($x63 (= ?x62 v_b_max_G_1$)))
(let (($x1910 (or $x1901 $x1907)))
(let (($x1913 (not $x1910)))
(let ((?x549 (* (- 1) v_b_p_G_0$)))
(let ((?x599 (+ v_b_length$ ?x549)))
(let (($x600 (<= ?x599 0)))
(let (($x1916 (or $x600 $x1286 $x1287 $x1913)))
(let (($x1919 (not $x1916)))
(let (($x1011 (>= (+ v_b_max_G_4$ (* (- 1) (v_b_array$ ?v0!2))) 0)))
(let (($x900 (<= (+ v_b_length$ (* (- 1) ?v0!2)) 0)))
(let (($x897 (>= ?v0!2 0)))
(let (($x1247 (not $x897)))
(let (($x889 (= (v_b_array$ ?v0!1) v_b_max_G_4$)))
(let (($x884 (<= (+ v_b_length$ (* (- 1) ?v0!1)) 0)))
(let (($x881 (>= ?v0!1 0)))
(let (($x1227 (not $x881)))
(let (($x1242 (or $x1227 $x884 $x889)))
(let (($x1273 (not $x1242)))
(let (($x1274 (or $x1273 $x1247 $x900 $x1011)))
(let (($x1275 (not $x1274)))
(let (($x1861 (forall ((?v0 Int) )(! (let ((?x46 (v_b_array$ ?v0)))
(let (($x86 (= ?x46 v_b_max_G_4$)))
(let (($x622 (<= (+ v_b_length$ (* (- 1) ?v0)) 0)))
(let (($x521 (>= ?v0 0)))
(let (($x1157 (not $x521)))
(let (($x1216 (or $x1157 $x622 $x86)))
(not $x1216))))))) :pattern ( (v_b_array$ ?v0) ) :qid k!17))
))
(let (($x1866 (or $x1861 $x1275)))
(let (($x1869 (not $x1866)))
(let (($x75 (= v_b_p_G_2$ v_b_p_G_0$)))
(let (($x1290 (not $x75)))
(let (($x73 (= v_b_max_G_4$ v_b_max_G_1$)))
(let (($x1289 (not $x73)))
(let (($x71 (= v_b_k_G_2$ v_b_k_G_0$)))
(let (($x1288 (not $x71)))
(let (($x661 (not $x600)))
(let (($x1872 (or $x661 $x1286 $x1287 $x1288 $x1289 $x1290 $x1869)))
(let (($x1875 (not $x1872)))
(let (($x1922 (or $x1875 $x1919)))
(let (($x1925 (not $x1922)))
(let (($x1403 (not $x63)))
(let (($x1853 (forall ((?v0 Int) )(! (let (($x561 (<= (+ (v_b_array$ ?v0) (* (- 1) v_b_max_G_1$)) 0)))
(let (($x548 (>= (+ ?v0 (* (- 1) v_b_p_G_0$)) 0)))
(let (($x521 (>= ?v0 0)))
(let (($x1157 (not $x521)))
(or $x1157 $x548 $x561))))) :pattern ( (v_b_array$ ?v0) ) :qid k!17))
))
(let (($x1858 (not $x1853)))
(let ((?x30 (v_b_array$ 0)))
(let (($x50 (= ?x30 v_b_max_G_0$)))
(let (($x851 (not $x50)))
(let (($x1928 (or $x851 $x1858 $x1403 $x1286 $x1287 $x1925)))
(let (($x1931 (not $x1928)))
(let (($x1934 (or $x851 $x1931)))
(let (($x1937 (not $x1934)))
(let (($x1845 (forall ((?v0 Int) )(! (let (($x534 (>= (+ v_b_max_G_0$ (* (- 1) (v_b_array$ ?v0))) 0)))
(let (($x524 (>= ?v0 1)))
(let (($x521 (>= ?v0 0)))
(let (($x1157 (not $x521)))
(or $x1157 $x524 $x534))))) :pattern ( (v_b_array$ ?v0) ) :qid k!17))
))
(let (($x1850 (not $x1845)))
(let (($x1940 (or $x1850 $x1937)))
(let (($x1943 (not $x1940)))
(let (($x839 (>= (+ v_b_max_G_0$ (* (- 1) (v_b_array$ ?v0!0))) 0)))
(let (($x832 (>= ?v0!0 1)))
(let (($x835 (>= ?v0!0 0)))
(let (($x1134 (not $x835)))
(let (($x1149 (or $x1134 $x832 $x839)))
(let (($x833 (not $x832)))
(let (($x1154 (not $x1149)))
(let ((@x1726 (hypothesis $x1154)))
(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))))
(let ((@x1715 (symm (monotonicity @x1711 (= (v_b_array$ ?v0!0) ?x30)) (= ?x30 (v_b_array$ ?v0!0)))))
(let (($x31 (= v_b_max_G_0$ ?x30)))
(let (($x495 (<= v_b_length$ 0)))
(let (($x496 (not $x495)))
(let (($x511 (and $x496 $x31)))
(let (($x752 (forall ((?v0 Int) )(! (let (($x746 (<= (+ (v_b_array$ ?v0) (* (- 1) v_b_max_G_3$)) 0)))
(let (($x521 (>= ?v0 0)))
(let (($x738 (and $x521 (not (>= (+ ?v0 (* (- 1) v_b_p_G_1$)) 0)))))
(let (($x741 (not $x738)))
(or $x741 $x746))))) :qid k!17))
))
(let (($x755 (not $x752)))
(let (($x758 (or $x755 $x136)))
(let (($x761 (and $x752 $x758)))
(let (($x784 (and $x689 $x571 $x144 $x145 $x573 $x684 $x679 $x682)))
(let (($x789 (not $x784)))
(let (($x792 (or $x789 $x761)))
(let (($x725 (and $x571 $x692 $x104 $x107 $x109 $x573 $x684 $x679 $x682)))
(let (($x730 (not $x725)))
(let (($x764 (or $x730 $x761)))
(let (($x795 (and $x764 $x792)))
(let (($x670 (and $x661 $x571 $x573)))
(let (($x675 (not $x670)))
(let (($x798 (or $x675 $x795)))
(let (($x649 (forall ((?v0 Int) )(! (let (($x521 (>= ?v0 0)))
(let (($x626 (and $x521 (not (<= (+ v_b_length$ (* (- 1) ?v0)) 0)))))
(let (($x629 (not $x626)))
(or $x629 (<= (+ (v_b_array$ ?v0) (* (- 1) v_b_max_G_4$)) 0))))) :qid k!17))
))
(let (($x635 (exists ((?v0 Int) )(! (let ((?x46 (v_b_array$ ?v0)))
(let (($x86 (= ?x46 v_b_max_G_4$)))
(let (($x521 (>= ?v0 0)))
(let (($x626 (and $x521 (not (<= (+ v_b_length$ (* (- 1) ?v0)) 0)))))
(let (($x629 (not $x626)))
(or $x629 $x86)))))) :qid k!17))
))
(let (($x638 (not $x635)))
(let (($x652 (or $x638 $x649)))
(let (($x655 (and $x635 $x652)))
(let (($x612 (and $x600 $x571 $x573 $x71 $x73 $x75)))
(let (($x617 (not $x612)))
(let (($x658 (or $x617 $x655)))
(let (($x801 (and $x658 $x798)))
(let (($x567 (forall ((?v0 Int) )(! (let (($x561 (<= (+ (v_b_array$ ?v0) (* (- 1) v_b_max_G_1$)) 0)))
(let (($x521 (>= ?v0 0)))
(let (($x553 (and $x521 (not (>= (+ ?v0 (* (- 1) v_b_p_G_0$)) 0)))))
(let (($x556 (not $x553)))
(or $x556 $x561))))) :qid k!17))
))
(let (($x591 (and $x50 $x567 $x63 $x571 $x573)))
(let (($x596 (not $x591)))
(let (($x804 (or $x596 $x801)))
(let (($x807 (and $x50 $x804)))
(let (($x541 (forall ((?v0 Int) )(! (let (($x534 (>= (+ v_b_max_G_0$ (* (- 1) (v_b_array$ ?v0))) 0)))
(let (($x521 (>= ?v0 0)))
(let (($x526 (and $x521 (not (>= ?v0 1)))))
(let (($x529 (not $x526)))
(or $x529 $x534))))) :qid k!17))
))
(let (($x544 (not $x541)))
(let (($x810 (or $x544 $x807)))
(let (($x813 (and $x541 $x810)))
(let (($x819 (not (or (not $x511) $x813))))
(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$)))
(let (($x43 (<= 0 ?v0)))
(let (($x131 (and $x43 (< ?v0 v_b_p_G_1$))))
(=> $x131 $x132))))) :qid k!17))
))
(let (($x140 (=> $x134 $x139)))
(let (($x141 (and $x134 $x140)))
(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))))
(let (($x54 (<= 1 v_b_p_G_0$)))
(let (($x110 (<= 0 v_b_k_G_1$)))
(let (($x111 (and $x110 $x54)))
(let (($x121 (and true (and $x111 $x119))))
(let (($x148 (and true (and $x144 (and $x145 $x121)))))
(let (($x55 (and (<= 0 v_b_k_G_0$) $x54)))
(let (($x143 (<= ?x101 v_b_max_G_1$)))
(let (($x152 (and true (and $x55 (and $x143 (and $x55 $x148))))))
(let (($x153 (=> $x152 $x141)))
(let (($x126 (and $x104 (and (and $x54 $x54) (and true (and $x107 (and $x109 $x121)))))))
(let (($x102 (< v_b_max_G_1$ ?x101)))
(let (($x129 (and true (and $x55 (and $x102 $x126)))))
(let (($x142 (=> $x129 $x141)))
(let (($x155 (=> (and true (and $x55 (and (< v_b_p_G_0$ v_b_length$) $x55))) (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))))) :qid k!17))
))
(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))))) :qid k!17))
))
(let (($x94 (=> $x88 $x93)))
(let (($x69 (<= v_b_length$ v_b_p_G_0$)))
(let (($x81 (and $x69 (and $x55 (and true (and $x71 (and $x73 (and $x75 true))))))))
(let (($x83 (and true (and $x55 $x81))))
(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$)))
(let (($x43 (<= 0 ?v0)))
(let (($x57 (and $x43 (< ?v0 v_b_p_G_0$))))
(=> $x57 $x59))))) :qid k!17))
))
(let (($x67 (and true (and $x55 (and $x61 $x64)))))
(let (($x157 (=> (and $x50 $x67) (and $x96 $x155))))
(let (($x49 (forall ((?v0 Int) )(! (let ((?x46 (v_b_array$ ?v0)))
(let (($x47 (<= ?x46 v_b_max_G_0$)))
(let (($x43 (<= 0 ?v0)))
(let (($x45 (and $x43 (< ?v0 1))))
(=> $x45 $x47))))) :qid k!17))
))
(let (($x159 (=> $x49 (and $x50 $x157))))
(let (($x32 (<= 0 0)))
(let (($x38 (and $x31 (and $x32 (and $x32 (and (<= 1 1) (<= 1 1)))))))
(let (($x39 (and true $x38)))
(let (($x28 (< 0 v_b_length$)))
(let (($x41 (and true (and $x28 $x39))))
(let (($x161 (=> $x41 (and $x49 $x159))))
(let (($x162 (not $x161)))
(let (($x362 (forall ((?v0 Int) )(! (let ((?x46 (v_b_array$ ?v0)))
(let (($x132 (<= ?x46 v_b_max_G_3$)))
(or (not (and (<= 0 ?v0) (< ?v0 v_b_p_G_1$))) $x132))) :qid k!17))
))
(let (($x385 (or (not $x362) $x136)))
(let (($x390 (and $x362 $x385)))
(let (($x117 (and $x110 (<= 2 v_b_p_G_1$))))
(let (($x308 (= v_b_p_G_1$ (+ 1 v_b_p_G_0$))))
(let (($x313 (and $x308 $x117)))
(let (($x316 (and $x111 $x313)))
(let (($x402 (and $x145 $x316)))
(let (($x405 (and $x144 $x402)))
(let (($x415 (and $x55 $x405)))
(let (($x418 (and $x143 $x415)))
(let (($x421 (and $x55 $x418)))
(let (($x435 (or (not $x421) $x390)))
(let (($x326 (and $x109 $x316)))
(let (($x329 (and $x107 $x326)))
(let (($x339 (and $x54 $x329)))
(let (($x342 (and $x104 $x339)))
(let (($x345 (and $x102 $x342)))
(let (($x348 (and $x55 $x345)))
(let (($x397 (or (not $x348) $x390)))
(let (($x440 (and $x397 $x435)))
(let (($x447 (or (not (and $x55 (and (< v_b_p_G_0$ v_b_length$) $x55))) $x440)))
(let (($x263 (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$))))
(let (($x253 (not $x85)))
(or $x253 $x89)))))) :qid k!17))
))
(let (($x257 (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$))))
(let (($x253 (not $x85)))
(or $x253 $x86)))))) :qid k!17))
))
(let (($x284 (or (not $x257) $x263)))
(let (($x289 (and $x257 $x284)))
(let (($x296 (or (not (and $x55 (and $x69 (and $x55 (and $x71 (and $x73 $x75)))))) $x289)))
(let (($x452 (and $x296 $x447)))
(let (($x203 (forall ((?v0 Int) )(! (let ((?x46 (v_b_array$ ?v0)))
(let (($x59 (<= ?x46 v_b_max_G_1$)))
(or (not (and (<= 0 ?v0) (< ?v0 v_b_p_G_0$))) $x59))) :qid k!17))
))
(let (($x206 (and $x203 $x64)))
(let (($x209 (and $x55 $x206)))
(let (($x219 (and $x50 $x209)))
(let (($x459 (or (not $x219) $x452)))
(let (($x464 (and $x50 $x459)))
(let (($x196 (forall ((?v0 Int) )(! (let ((?x46 (v_b_array$ ?v0)))
(let (($x47 (<= ?x46 v_b_max_G_0$)))
(or (not (and (<= 0 ?v0) (< ?v0 1))) $x47))) :qid k!17))
))
(let (($x471 (or (not $x196) $x464)))
(let (($x476 (and $x196 $x471)))
(let (($x483 (or (not (and $x28 (and $x31 (and $x32 (and $x32 (<= 1 1)))))) $x476)))
(let (($x746 (<= (+ (v_b_array$ ?0) ?x744) 0)))
(let (($x521 (>= ?0 0)))
(let (($x738 (and $x521 (not (>= (+ ?0 ?x685) 0)))))
(let (($x741 (not $x738)))
(let (($x749 (or $x741 $x746)))
(let ((?x46 (v_b_array$ ?0)))
(let (($x132 (<= ?x46 v_b_max_G_3$)))
(let (($x359 (or (not (and (<= 0 ?0) (< ?0 v_b_p_G_1$))) $x132)))
(let ((@x520 (rewrite (= (<= 0 ?0) $x521))))
(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))))
(let ((@x743 (monotonicity @x740 (= (not (and (<= 0 ?0) (< ?0 v_b_p_G_1$))) $x741))))
(let ((@x754 (quant-intro (monotonicity @x743 (rewrite (= $x132 $x746)) (= $x359 $x749)) (= $x362 $x752))))
(let ((@x760 (monotonicity (monotonicity @x754 (= (not $x362) $x755)) (= $x385 $x758))))
(let (($x772 (and $x144 (and $x145 (and (and $x679 $x573) (and $x684 (and $x679 $x682)))))))
(let (($x576 (and $x571 $x573)))
(let (($x770 (= $x402 (and $x145 (and (and $x679 $x573) (and $x684 (and $x679 $x682)))))))
(let ((@x697 (monotonicity (rewrite (= $x110 $x679)) (rewrite (= (<= 2 v_b_p_G_1$) $x682)) (= $x117 (and $x679 $x682)))))
(let ((@x700 (monotonicity (rewrite (= $x308 $x684)) @x697 (= $x313 (and $x684 (and $x679 $x682))))))
(let ((@x575 (rewrite (= $x54 $x573))))
(let ((@x703 (monotonicity (rewrite (= $x110 $x679)) @x575 (= $x111 (and $x679 $x573)))))
(let ((@x706 (monotonicity @x703 @x700 (= $x316 (and (and $x679 $x573) (and $x684 (and $x679 $x682)))))))
(let ((@x578 (monotonicity (rewrite (= (<= 0 v_b_k_G_0$) $x571)) @x575 (= $x55 $x576))))
(let ((@x777 (monotonicity @x578 (monotonicity (monotonicity @x706 $x770) (= $x405 $x772)) (= $x415 (and $x576 $x772)))))
(let ((@x780 (monotonicity (rewrite (= $x143 $x689)) @x777 (= $x418 (and $x689 (and $x576 $x772))))))
(let ((@x783 (monotonicity @x578 @x780 (= $x421 (and $x576 (and $x689 (and $x576 $x772)))))))
(let ((@x788 (trans @x783 (rewrite (= (and $x576 (and $x689 (and $x576 $x772))) $x784)) (= $x421 $x784))))
(let ((@x794 (monotonicity (monotonicity @x788 (= (not $x421) $x789)) (monotonicity @x754 @x760 (= $x390 $x761)) (= $x435 $x792))))
(let (($x710 (and $x107 (and $x109 (and (and $x679 $x573) (and $x684 (and $x679 $x682)))))))
(let ((@x727 (rewrite (= (and $x576 (and $x692 (and $x104 (and $x573 $x710)))) $x725))))
(let (($x708 (= $x326 (and $x109 (and (and $x679 $x573) (and $x684 (and $x679 $x682)))))))
(let ((@x715 (monotonicity @x575 (monotonicity (monotonicity @x706 $x708) (= $x329 $x710)) (= $x339 (and $x573 $x710)))))
(let ((@x721 (monotonicity (rewrite (= $x102 $x692)) (monotonicity @x715 (= $x342 (and $x104 (and $x573 $x710)))) (= $x345 (and $x692 (and $x104 (and $x573 $x710)))))))
(let ((@x724 (monotonicity @x578 @x721 (= $x348 (and $x576 (and $x692 (and $x104 (and $x573 $x710))))))))
(let ((@x732 (monotonicity (trans @x724 @x727 (= $x348 $x725)) (= (not $x348) $x730))))
(let ((@x766 (monotonicity @x732 (monotonicity @x754 @x760 (= $x390 $x761)) (= $x397 $x764))))
(let (($x99 (and $x55 (and (< v_b_p_G_0$ v_b_length$) $x55))))
(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)))))
(let ((@x674 (trans (monotonicity @x578 @x666 (= $x99 (and $x576 (and $x661 $x576)))) (rewrite (= (and $x576 (and $x661 $x576)) $x670)) (= $x99 $x670))))
(let ((@x800 (monotonicity (monotonicity @x674 (= (not $x99) $x675)) (monotonicity @x766 @x794 (= $x440 $x795)) (= $x447 $x798))))
(let (($x626 (and $x521 (not (<= (+ v_b_length$ (* (- 1) ?0)) 0)))))
(let (($x629 (not $x626)))
(let (($x89 (<= ?x46 v_b_max_G_4$)))
(let (($x43 (<= 0 ?0)))
(let (($x85 (and $x43 (< ?0 v_b_length$))))
(let (($x253 (not $x85)))
(let (($x260 (or $x253 $x89)))
(let (($x624 (= (< ?0 v_b_length$) (not (<= (+ v_b_length$ (* (- 1) ?0)) 0)))))
(let ((@x631 (monotonicity (monotonicity @x520 (rewrite $x624) (= $x85 $x626)) (= $x253 $x629))))
(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))))))
(let (($x86 (= ?x46 v_b_max_G_4$)))
(let (($x632 (or $x629 $x86)))
(let (($x254 (or $x253 $x86)))
(let ((@x640 (monotonicity (quant-intro (monotonicity @x631 (= $x254 $x632)) (= $x257 $x635)) (= (not $x257) $x638))))
(let ((@x657 (monotonicity (quant-intro (monotonicity @x631 (= $x254 $x632)) (= $x257 $x635)) (monotonicity @x640 (quant-intro @x648 (= $x263 $x649)) (= $x284 $x652)) (= $x289 $x655))))
(let (($x618 (= (not (and $x55 (and $x69 (and $x55 (and $x71 (and $x73 $x75)))))) $x617)))
(let (($x227 (and $x71 (and $x73 $x75))))
(let (($x237 (and $x55 $x227)))
(let (($x240 (and $x69 $x237)))
(let (($x243 (and $x55 $x240)))
(let ((@x608 (monotonicity (rewrite (= $x69 $x600)) (monotonicity @x578 (= $x237 (and $x576 $x227))) (= $x240 (and $x600 (and $x576 $x227))))))
(let ((@x611 (monotonicity @x578 @x608 (= $x243 (and $x576 (and $x600 (and $x576 $x227)))))))
(let ((@x616 (trans @x611 (rewrite (= (and $x576 (and $x600 (and $x576 $x227))) $x612)) (= $x243 $x612))))
(let ((@x803 (monotonicity (monotonicity (monotonicity @x616 $x618) @x657 (= $x296 $x658)) @x800 (= $x452 $x801))))
(let ((@x593 (rewrite (= (and $x50 (and $x576 (and $x567 (and $x63 $x576)))) $x591))))
(let (($x561 (<= (+ ?x46 (* (- 1) v_b_max_G_1$)) 0)))
(let (($x553 (and $x521 (not (>= (+ ?0 ?x549) 0)))))
(let (($x556 (not $x553)))
(let (($x564 (or $x556 $x561)))
(let (($x59 (<= ?x46 v_b_max_G_1$)))
(let (($x200 (or (not (and $x43 (< ?0 v_b_p_G_0$))) $x59)))
(let ((@x555 (monotonicity @x520 (rewrite (= (< ?0 v_b_p_G_0$) (not (>= (+ ?0 ?x549) 0)))) (= (and $x43 (< ?0 v_b_p_G_0$)) $x553))))
(let ((@x566 (monotonicity (monotonicity @x555 (= (not (and $x43 (< ?0 v_b_p_G_0$))) $x556)) (rewrite (= $x59 $x561)) (= $x200 $x564))))
(let ((@x584 (monotonicity (quant-intro @x566 (= $x203 $x567)) (monotonicity @x578 (= $x64 (and $x63 $x576))) (= $x206 (and $x567 (and $x63 $x576))))))
(let ((@x587 (monotonicity @x578 @x584 (= $x209 (and $x576 (and $x567 (and $x63 $x576)))))))
(let ((@x590 (monotonicity @x587 (= $x219 (and $x50 (and $x576 (and $x567 (and $x63 $x576))))))))
(let ((@x598 (monotonicity (trans @x590 @x593 (= $x219 $x591)) (= (not $x219) $x596))))
(let ((@x809 (monotonicity (monotonicity @x598 @x803 (= $x459 $x804)) (= $x464 $x807))))
(let (($x534 (>= (+ v_b_max_G_0$ (* (- 1) ?x46)) 0)))
(let (($x526 (and $x521 (not (>= ?0 1)))))
(let (($x529 (not $x526)))
(let (($x538 (or $x529 $x534)))
(let (($x47 (<= ?x46 v_b_max_G_0$)))
(let (($x193 (or (not (and $x43 (< ?0 1))) $x47)))
(let ((@x528 (monotonicity @x520 (rewrite (= (< ?0 1) (not (>= ?0 1)))) (= (and $x43 (< ?0 1)) $x526))))
(let ((@x540 (monotonicity (monotonicity @x528 (= (not (and $x43 (< ?0 1))) $x529)) (rewrite (= $x47 $x534)) (= $x193 $x538))))
(let ((@x546 (monotonicity (quant-intro @x540 (= $x196 $x541)) (= (not $x196) $x544))))
(let ((@x815 (monotonicity (quant-intro @x540 (= $x196 $x541)) (monotonicity @x546 @x809 (= $x471 $x810)) (= $x476 $x813))))
(let (($x517 (= (not (and $x28 (and $x31 (and $x32 (and $x32 (<= 1 1)))))) (not $x511))))
(let (($x34 (<= 1 1)))
(let (($x166 (and $x32 $x34)))
(let (($x169 (and $x32 $x166)))
(let (($x172 (and $x31 $x169)))
(let (($x182 (and $x28 $x172)))
(let ((@x513 (rewrite (= (and $x496 (and $x31 (and true (and true true)))) $x511))))
(let ((@x501 (monotonicity (rewrite (= $x32 true)) (rewrite (= $x34 true)) (= $x166 (and true true)))))
(let ((@x504 (monotonicity (rewrite (= $x32 true)) @x501 (= $x169 (and true (and true true))))))
(let ((@x507 (monotonicity @x504 (= $x172 (and $x31 (and true (and true true)))))))
(let ((@x510 (monotonicity (rewrite (= $x28 $x496)) @x507 (= $x182 (and $x496 (and $x31 (and true (and true true))))))))
(let ((@x818 (monotonicity (monotonicity (trans @x510 @x513 (= $x182 $x511)) $x517) @x815 (= $x483 (or (not $x511) $x813)))))
(let ((@x369 (monotonicity (rewrite (= (and $x136 false) false)) (= $x138 (=> false true)))))
(let ((@x373 (trans @x369 (rewrite (= (=> false true) true)) (= $x138 true))))
(let ((@x380 (trans (monotonicity @x373 (= $x139 (and $x136 true))) (rewrite (= (and $x136 true) $x136)) (= $x139 $x136))))
(let ((@x364 (quant-intro (rewrite (= (=> (and $x43 (< ?0 v_b_p_G_1$)) $x132) $x359)) (= $x134 $x362))))
(let ((@x389 (trans (monotonicity @x364 @x380 (= $x140 (=> $x362 $x136))) (rewrite (= (=> $x362 $x136) $x385)) (= $x140 $x385))))
(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))))
(let ((@x315 (monotonicity @x310 (rewrite (= (and $x117 true) $x117)) (= $x119 $x313))))
(let ((@x321 (monotonicity (monotonicity @x315 (= (and $x111 $x119) $x316)) (= $x121 (and true $x316)))))
(let ((@x404 (monotonicity (trans @x321 (rewrite (= (and true $x316) $x316)) (= $x121 $x316)) (= (and $x145 $x121) $x402))))
(let ((@x410 (monotonicity (monotonicity @x404 (= (and $x144 (and $x145 $x121)) $x405)) (= $x148 (and true $x405)))))
(let ((@x417 (monotonicity (trans @x410 (rewrite (= (and true $x405) $x405)) (= $x148 $x405)) (= (and $x55 $x148) $x415))))
(let ((@x423 (monotonicity (monotonicity @x417 (= (and $x143 (and $x55 $x148)) $x418)) (= (and $x55 (and $x143 (and $x55 $x148))) $x421))))
(let ((@x430 (trans (monotonicity @x423 (= $x152 (and true $x421))) (rewrite (= (and true $x421) $x421)) (= $x152 $x421))))
(let ((@x433 (monotonicity @x430 (monotonicity @x364 @x389 (= $x141 $x390)) (= $x153 (=> $x421 $x390)))))
(let (($x340 (= (and (and $x54 $x54) (and true (and $x107 (and $x109 $x121)))) $x339)))
(let ((@x328 (monotonicity (trans @x321 (rewrite (= (and true $x316) $x316)) (= $x121 $x316)) (= (and $x109 $x121) $x326))))
(let ((@x334 (monotonicity (monotonicity @x328 (= (and $x107 (and $x109 $x121)) $x329)) (= (and true (and $x107 (and $x109 $x121))) (and true $x329)))))
(let ((@x338 (trans @x334 (rewrite (= (and true $x329) $x329)) (= (and true (and $x107 (and $x109 $x121))) $x329))))
(let ((@x344 (monotonicity (monotonicity (rewrite (= (and $x54 $x54) $x54)) @x338 $x340) (= $x126 $x342))))
(let ((@x350 (monotonicity (monotonicity @x344 (= (and $x102 $x126) $x345)) (= (and $x55 (and $x102 $x126)) $x348))))
(let ((@x357 (trans (monotonicity @x350 (= $x129 (and true $x348))) (rewrite (= (and true $x348) $x348)) (= $x129 $x348))))
(let ((@x395 (monotonicity @x357 (monotonicity @x364 @x389 (= $x141 $x390)) (= $x142 (=> $x348 $x390)))))
(let ((@x442 (monotonicity (trans @x395 (rewrite (= (=> $x348 $x390) $x397)) (= $x142 $x397)) (trans @x433 (rewrite (= (=> $x421 $x390) $x435)) (= $x153 $x435)) (= (and $x142 $x153) $x440))))
(let ((@x445 (monotonicity (rewrite (= (and true $x99) $x99)) @x442 (= $x155 (=> $x99 $x440)))))
(let ((@x268 (monotonicity (quant-intro (rewrite (= (=> $x85 $x89) $x260)) (= $x91 $x263)) (= $x92 (=> $x263 true)))))
(let ((@x272 (trans @x268 (rewrite (= (=> $x263 true) true)) (= $x92 true))))
(let ((@x275 (monotonicity (quant-intro (rewrite (= (=> $x85 $x89) $x260)) (= $x91 $x263)) @x272 (= $x93 (and $x263 true)))))
(let ((@x282 (monotonicity (quant-intro (rewrite (= (=> $x85 $x86) $x254)) (= $x88 $x257)) (trans @x275 (rewrite (= (and $x263 true) $x263)) (= $x93 $x263)) (= $x94 (=> $x257 $x263)))))
(let ((@x291 (monotonicity (quant-intro (rewrite (= (=> $x85 $x86) $x254)) (= $x88 $x257)) (trans @x282 (rewrite (= (=> $x257 $x263) $x284)) (= $x94 $x284)) (= (and $x88 $x94) $x289))))
(let (($x238 (= (and $x55 (and true (and $x71 (and $x73 (and $x75 true))))) $x237)))
(let (($x79 (and true (and $x71 (and $x73 (and $x75 true))))))
(let ((@x226 (monotonicity (rewrite (= (and $x75 true) $x75)) (= (and $x73 (and $x75 true)) (and $x73 $x75)))))
(let ((@x229 (monotonicity @x226 (= (and $x71 (and $x73 (and $x75 true))) $x227))))
(let ((@x236 (trans (monotonicity @x229 (= $x79 (and true $x227))) (rewrite (= (and true $x227) $x227)) (= $x79 $x227))))
(let ((@x245 (monotonicity (monotonicity (monotonicity @x236 $x238) (= $x81 $x240)) (= (and $x55 $x81) $x243))))
(let ((@x252 (trans (monotonicity @x245 (= $x83 (and true $x243))) (rewrite (= (and true $x243) $x243)) (= $x83 $x243))))
(let ((@x300 (trans (monotonicity @x252 @x291 (= $x96 (=> $x243 $x289))) (rewrite (= (=> $x243 $x289) $x296)) (= $x96 $x296))))
(let ((@x454 (monotonicity @x300 (trans @x445 (rewrite (= (=> $x99 $x440) $x447)) (= $x155 $x447)) (= (and $x96 $x155) $x452))))
(let ((@x205 (quant-intro (rewrite (= (=> (and $x43 (< ?0 v_b_p_G_0$)) $x59) $x200)) (= $x61 $x203))))
(let ((@x211 (monotonicity (monotonicity @x205 (= (and $x61 $x64) $x206)) (= (and $x55 (and $x61 $x64)) $x209))))
(let ((@x218 (trans (monotonicity @x211 (= $x67 (and true $x209))) (rewrite (= (and true $x209) $x209)) (= $x67 $x209))))
(let ((@x457 (monotonicity (monotonicity @x218 (= (and $x50 $x67) $x219)) @x454 (= $x157 (=> $x219 $x452)))))
(let ((@x466 (monotonicity (trans @x457 (rewrite (= (=> $x219 $x452) $x459)) (= $x157 $x459)) (= (and $x50 $x157) $x464))))
(let ((@x198 (quant-intro (rewrite (= (=> (and $x43 (< ?0 1)) $x47) $x193)) (= $x49 $x196))))
(let ((@x475 (trans (monotonicity @x198 @x466 (= $x159 (=> $x196 $x464))) (rewrite (= (=> $x196 $x464) $x471)) (= $x159 $x471))))
(let ((@x168 (monotonicity (rewrite (= (and $x34 $x34) $x34)) (= (and $x32 (and $x34 $x34)) $x166))))
(let ((@x174 (monotonicity (monotonicity @x168 (= (and $x32 (and $x32 (and $x34 $x34))) $x169)) (= $x38 $x172))))
(let ((@x181 (trans (monotonicity @x174 (= $x39 (and true $x172))) (rewrite (= (and true $x172) $x172)) (= $x39 $x172))))
(let ((@x187 (monotonicity (monotonicity @x181 (= (and $x28 $x39) $x182)) (= $x41 (and true $x182)))))
(let ((@x481 (monotonicity (trans @x187 (rewrite (= (and true $x182) $x182)) (= $x41 $x182)) (monotonicity @x198 @x475 (= (and $x49 $x159) $x476)) (= $x161 (=> $x182 $x476)))))
(let ((@x490 (monotonicity (trans @x481 (rewrite (= (=> $x182 $x476) $x483)) (= $x161 $x483)) (= $x162 (not $x483)))))
(let ((@x823 (trans @x490 (monotonicity @x818 (= (not $x483) $x819)) (= $x162 $x819))))
(let ((@x827 (and-elim (not-or-elim (mp (asserted $x162) @x823 $x819) $x511) $x31)))
(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)))
(let (($x1946 (or $x1154 $x1943)))
(let (($x1340 (forall ((?v0 Int) )(! (let (($x746 (<= (+ (v_b_array$ ?v0) (* (- 1) v_b_max_G_3$)) 0)))
(let (($x733 (>= (+ ?v0 (* (- 1) v_b_p_G_1$)) 0)))
(let (($x521 (>= ?v0 0)))
(let (($x1157 (not $x521)))
(or $x1157 $x733 $x746))))) :qid k!17))
))
(let (($x1348 (not (or (not $x1340) $x136))))
(let (($x1353 (or $x1318 $x1348)))
(let (($x1365 (not $x1353)))
(let (($x1378 (not (or $x692 $x1286 $x1375 $x1376 $x1287 $x1362 $x1363 $x1364 $x1365))))
(let (($x1367 (not (or $x1286 $x689 $x1359 $x1360 $x1361 $x1287 $x1362 $x1363 $x1364 $x1365))))
(let (($x1383 (or $x1367 $x1378)))
(let (($x1391 (not (or $x600 $x1286 $x1287 (not $x1383)))))
(let (($x1224 (forall ((?v0 Int) )(! (let ((?x46 (v_b_array$ ?v0)))
(let (($x86 (= ?x46 v_b_max_G_4$)))
(let (($x622 (<= (+ v_b_length$ (* (- 1) ?v0)) 0)))
(let (($x521 (>= ?v0 0)))
(let (($x1157 (not $x521)))
(let (($x1216 (or $x1157 $x622 $x86)))
(not $x1216))))))) :qid k!17))
))
(let (($x1280 (or $x1224 $x1275)))
(let (($x1293 (not (or $x661 $x1286 $x1287 $x1288 $x1289 $x1290 (not $x1280)))))
(let (($x1396 (or $x1293 $x1391)))
(let (($x1199 (forall ((?v0 Int) )(! (let (($x561 (<= (+ (v_b_array$ ?v0) (* (- 1) v_b_max_G_1$)) 0)))
(let (($x548 (>= (+ ?v0 (* (- 1) v_b_p_G_0$)) 0)))
(let (($x521 (>= ?v0 0)))
(let (($x1157 (not $x521)))
(or $x1157 $x548 $x561))))) :qid k!17))
))
(let (($x1406 (not (or $x851 (not $x1199) $x1403 $x1286 $x1287 (not $x1396)))))
(let (($x1411 (or $x851 $x1406)))
(let (($x1177 (forall ((?v0 Int) )(! (let (($x534 (>= (+ v_b_max_G_0$ (* (- 1) (v_b_array$ ?v0))) 0)))
(let (($x524 (>= ?v0 1)))
(let (($x521 (>= ?v0 0)))
(let (($x1157 (not $x521)))
(or $x1157 $x524 $x534))))) :qid k!17))
))
(let (($x1420 (not (or (not $x1177) (not $x1411)))))
(let (($x1425 (or $x1154 $x1420)))
(let (($x733 (>= (+ ?0 ?x685) 0)))
(let (($x1157 (not $x521)))
(let (($x1335 (or $x1157 $x733 $x746)))
(let ((@x1885 (monotonicity (quant-intro (refl (= $x1335 $x1335)) (= $x1340 $x1878)) (= (not $x1340) $x1883))))
(let ((@x1891 (monotonicity (monotonicity @x1885 (= (or (not $x1340) $x136) $x1886)) (= $x1348 $x1889))))
(let ((@x1906 (monotonicity (monotonicity (monotonicity @x1891 (= $x1353 $x1892)) (= $x1365 $x1895)) (= (or $x692 $x1286 $x1375 $x1376 $x1287 $x1362 $x1363 $x1364 $x1365) $x1904))))
(let ((@x1900 (monotonicity (monotonicity (monotonicity @x1891 (= $x1353 $x1892)) (= $x1365 $x1895)) (= (or $x1286 $x689 $x1359 $x1360 $x1361 $x1287 $x1362 $x1363 $x1364 $x1365) $x1898))))
(let ((@x1912 (monotonicity (monotonicity @x1900 (= $x1367 $x1901)) (monotonicity @x1906 (= $x1378 $x1907)) (= $x1383 $x1910))))
(let ((@x1918 (monotonicity (monotonicity @x1912 (= (not $x1383) $x1913)) (= (or $x600 $x1286 $x1287 (not $x1383)) $x1916))))
(let (($x622 (<= (+ v_b_length$ (* (- 1) ?0)) 0)))
(let (($x1216 (or $x1157 $x622 $x86)))
(let (($x1221 (not $x1216)))
(let ((@x1868 (monotonicity (quant-intro (refl (= $x1221 $x1221)) (= $x1224 $x1861)) (= $x1280 $x1866))))
(let ((@x1874 (monotonicity (monotonicity @x1868 (= (not $x1280) $x1869)) (= (or $x661 $x1286 $x1287 $x1288 $x1289 $x1290 (not $x1280)) $x1872))))
(let ((@x1924 (monotonicity (monotonicity @x1874 (= $x1293 $x1875)) (monotonicity @x1918 (= $x1391 $x1919)) (= $x1396 $x1922))))
(let (($x548 (>= (+ ?0 ?x549) 0)))
(let (($x1194 (or $x1157 $x548 $x561)))
(let ((@x1860 (monotonicity (quant-intro (refl (= $x1194 $x1194)) (= $x1199 $x1853)) (= (not $x1199) $x1858))))
(let ((@x1930 (monotonicity @x1860 (monotonicity @x1924 (= (not $x1396) $x1925)) (= (or $x851 (not $x1199) $x1403 $x1286 $x1287 (not $x1396)) $x1928))))
(let ((@x1939 (monotonicity (monotonicity (monotonicity @x1930 (= $x1406 $x1931)) (= $x1411 $x1934)) (= (not $x1411) $x1937))))
(let ((@x1847 (refl (= (or $x1157 (>= ?0 1) $x534) (or $x1157 (>= ?0 1) $x534)))))
(let ((@x1852 (monotonicity (quant-intro @x1847 (= $x1177 $x1845)) (= (not $x1177) $x1850))))
(let ((@x1945 (monotonicity (monotonicity @x1852 @x1939 (= (or (not $x1177) (not $x1411)) $x1940)) (= $x1420 $x1943))))
(let (($x951 (not $x136)))
(let (($x954 (and $x752 $x951)))
(let (($x1053 (not $x1048)))
(let (($x1056 (and $x931 $x1053)))
(let (($x1059 (not $x1056)))
(let (($x1075 (or $x1059 $x1070)))
(let (($x1078 (not $x1075)))
(let (($x1081 (or $x1078 $x954)))
(let (($x1097 (and $x689 $x571 $x144 $x145 $x573 $x684 $x679 $x682 $x1081)))
(let (($x1087 (and $x571 $x692 $x104 $x107 $x109 $x573 $x684 $x679 $x682 $x1081)))
(let (($x1102 (or $x1087 $x1097)))
(let (($x1108 (and $x661 $x571 $x573 $x1102)))
(let (($x903 (not (and $x897 (not $x900)))))
(let (($x1016 (or $x903 $x1011)))
(let (($x1019 (not $x1016)))
(let (($x887 (not (and $x881 (not $x884)))))
(let (($x890 (or $x887 $x889)))
(let (($x1022 (and $x890 $x1019)))
(let (($x877 (forall ((?v0 Int) )(! (let ((?x46 (v_b_array$ ?v0)))
(let (($x86 (= ?x46 v_b_max_G_4$)))
(let (($x521 (>= ?v0 0)))
(let (($x626 (and $x521 (not (<= (+ v_b_length$ (* (- 1) ?v0)) 0)))))
(let (($x629 (not $x626)))
(let (($x632 (or $x629 $x86)))
(not $x632))))))) :qid k!17))
))
(let (($x1025 (or $x877 $x1022)))
(let (($x1031 (and $x600 $x571 $x573 $x71 $x73 $x75 $x1025)))
(let (($x1113 (or $x1031 $x1108)))
(let (($x1119 (and $x50 $x567 $x63 $x571 $x573 $x1113)))
(let (($x1124 (or $x851 $x1119)))
(let (($x1127 (and $x541 $x1124)))
(let (($x831 (not (and $x835 $x833))))
(let (($x840 (or $x831 $x839)))
(let (($x841 (not $x840)))
(let (($x1130 (or $x841 $x1127)))
(let ((@x1380 (rewrite (= (and $x689 $x571 $x144 $x145 $x573 $x684 $x679 $x682 $x1353) $x1378))))
(let ((@x1327 (monotonicity (rewrite (= $x738 (not (or $x1157 $x733)))) (= $x741 (not (not (or $x1157 $x733)))))))
(let ((@x1331 (trans @x1327 (rewrite (= (not (not (or $x1157 $x733))) (or $x1157 $x733))) (= $x741 (or $x1157 $x733)))))
(let ((@x1339 (trans (monotonicity @x1331 (= $x749 (or (or $x1157 $x733) $x746))) (rewrite (= (or (or $x1157 $x733) $x746) $x1335)) (= $x749 $x1335))))
(let ((@x1345 (monotonicity (quant-intro @x1339 (= $x752 $x1340)) (= $x954 (and $x1340 $x951)))))
(let ((@x1305 (monotonicity (rewrite (= $x1056 (not (or $x1298 $x1048)))) (= $x1059 (not (not (or $x1298 $x1048)))))))
(let ((@x1309 (trans @x1305 (rewrite (= (not (not (or $x1298 $x1048))) (or $x1298 $x1048))) (= $x1059 (or $x1298 $x1048)))))
(let ((@x1317 (trans (monotonicity @x1309 (= $x1075 (or (or $x1298 $x1048) $x1070))) (rewrite (= (or (or $x1298 $x1048) $x1070) $x1313)) (= $x1075 $x1313))))
(let ((@x1355 (monotonicity (monotonicity @x1317 (= $x1078 $x1318)) (trans @x1345 (rewrite (= (and $x1340 $x951) $x1348)) (= $x954 $x1348)) (= $x1081 $x1353))))
(let ((@x1374 (monotonicity @x1355 (= $x1097 (and $x689 $x571 $x144 $x145 $x573 $x684 $x679 $x682 $x1353)))))
(let ((@x1369 (rewrite (= (and $x571 $x692 $x104 $x107 $x109 $x573 $x684 $x679 $x682 $x1353) $x1367))))
(let ((@x1358 (monotonicity @x1355 (= $x1087 (and $x571 $x692 $x104 $x107 $x109 $x573 $x684 $x679 $x682 $x1353)))))
(let ((@x1385 (monotonicity (trans @x1358 @x1369 (= $x1087 $x1367)) (trans @x1374 @x1380 (= $x1097 $x1378)) (= $x1102 $x1383))))
(let ((@x1395 (trans (monotonicity @x1385 (= $x1108 (and $x661 $x571 $x573 $x1383))) (rewrite (= (and $x661 $x571 $x573 $x1383) $x1391)) (= $x1108 $x1391))))
(let ((@x1254 (monotonicity (rewrite (= (and $x897 (not $x900)) (not (or $x1247 $x900)))) (= $x903 (not (not (or $x1247 $x900)))))))
(let ((@x1258 (trans @x1254 (rewrite (= (not (not (or $x1247 $x900))) (or $x1247 $x900))) (= $x903 (or $x1247 $x900)))))
(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)))))
(let ((@x1234 (monotonicity (rewrite (= (and $x881 (not $x884)) (not (or $x1227 $x884)))) (= $x887 (not (not (or $x1227 $x884)))))))
(let ((@x1238 (trans @x1234 (rewrite (= (not (not (or $x1227 $x884))) (or $x1227 $x884))) (= $x887 (or $x1227 $x884)))))
(let ((@x1246 (trans (monotonicity @x1238 (= $x890 (or (or $x1227 $x884) $x889))) (rewrite (= (or (or $x1227 $x884) $x889) $x1242)) (= $x890 $x1242))))
(let ((@x1272 (monotonicity @x1246 (monotonicity @x1266 (= $x1019 (not (or $x1247 $x900 $x1011)))) (= $x1022 (and $x1242 (not (or $x1247 $x900 $x1011)))))))
(let ((@x1279 (trans @x1272 (rewrite (= (and $x1242 (not (or $x1247 $x900 $x1011))) $x1275)) (= $x1022 $x1275))))
(let ((@x1208 (monotonicity (rewrite (= $x626 (not (or $x1157 $x622)))) (= $x629 (not (not (or $x1157 $x622)))))))
(let ((@x1212 (trans @x1208 (rewrite (= (not (not (or $x1157 $x622))) (or $x1157 $x622))) (= $x629 (or $x1157 $x622)))))
(let ((@x1220 (trans (monotonicity @x1212 (= $x632 (or (or $x1157 $x622) $x86))) (rewrite (= (or (or $x1157 $x622) $x86) $x1216)) (= $x632 $x1216))))
(let ((@x1226 (quant-intro (monotonicity @x1220 (= (not $x632) $x1221)) (= $x877 $x1224))))
(let ((@x1285 (monotonicity (monotonicity @x1226 @x1279 (= $x1025 $x1280)) (= $x1031 (and $x600 $x571 $x573 $x71 $x73 $x75 $x1280)))))
(let ((@x1297 (trans @x1285 (rewrite (= (and $x600 $x571 $x573 $x71 $x73 $x75 $x1280) $x1293)) (= $x1031 $x1293))))
(let ((@x1186 (monotonicity (rewrite (= $x553 (not (or $x1157 $x548)))) (= $x556 (not (not (or $x1157 $x548)))))))
(let ((@x1190 (trans @x1186 (rewrite (= (not (not (or $x1157 $x548))) (or $x1157 $x548))) (= $x556 (or $x1157 $x548)))))
(let ((@x1198 (trans (monotonicity @x1190 (= $x564 (or (or $x1157 $x548) $x561))) (rewrite (= (or (or $x1157 $x548) $x561) $x1194)) (= $x564 $x1194))))
(let ((@x1401 (monotonicity (quant-intro @x1198 (= $x567 $x1199)) (monotonicity @x1297 @x1395 (= $x1113 $x1396)) (= $x1119 (and $x50 $x1199 $x63 $x571 $x573 $x1396)))))
(let ((@x1410 (trans @x1401 (rewrite (= (and $x50 $x1199 $x63 $x571 $x573 $x1396) $x1406)) (= $x1119 $x1406))))
(let (($x524 (>= ?0 1)))
(let (($x1172 (or $x1157 $x524 $x534)))
(let ((@x1164 (monotonicity (rewrite (= $x526 (not (or $x1157 $x524)))) (= $x529 (not (not (or $x1157 $x524)))))))
(let ((@x1168 (trans @x1164 (rewrite (= (not (not (or $x1157 $x524))) (or $x1157 $x524))) (= $x529 (or $x1157 $x524)))))
(let ((@x1176 (trans (monotonicity @x1168 (= $x538 (or (or $x1157 $x524) $x534))) (rewrite (= (or (or $x1157 $x524) $x534) $x1172)) (= $x538 $x1172))))
(let ((@x1416 (monotonicity (quant-intro @x1176 (= $x541 $x1177)) (monotonicity @x1410 (= $x1124 $x1411)) (= $x1127 (and $x1177 $x1411)))))
(let ((@x1141 (monotonicity (rewrite (= (and $x835 $x833) (not (or $x1134 $x832)))) (= $x831 (not (not (or $x1134 $x832)))))))
(let ((@x1145 (trans @x1141 (rewrite (= (not (not (or $x1134 $x832))) (or $x1134 $x832))) (= $x831 (or $x1134 $x832)))))
(let ((@x1153 (trans (monotonicity @x1145 (= $x840 (or (or $x1134 $x832) $x839))) (rewrite (= (or (or $x1134 $x832) $x839) $x1149)) (= $x840 $x1149))))
(let ((@x1427 (monotonicity (monotonicity @x1153 (= $x841 $x1154)) (trans @x1416 (rewrite (= (and $x1177 $x1411) $x1420)) (= $x1127 $x1420)) (= $x1130 $x1425))))
(let (($x939 (<= (+ ?x937 ?x744) 0)))
(let (($x941 (not (or (not (and $x931 (not (>= (+ ?v0!3 ?x685) 0)))) $x939))))
(let (($x958 (or $x941 $x954)))
(let (($x966 (not $x789)))
(let (($x969 (and $x966 $x958)))
(let (($x927 (not $x730)))
(let (($x962 (and $x927 $x958)))
(let (($x973 (or $x962 $x969)))
(let (($x924 (not $x675)))
(let (($x977 (and $x924 $x973)))
(let (($x908 (not (or $x903 (<= (+ (v_b_array$ ?v0!2) (* (- 1) v_b_max_G_4$)) 0)))))
(let (($x912 (and $x890 $x908)))
(let (($x916 (or $x877 $x912)))
(let (($x871 (not $x617)))
(let (($x920 (and $x871 $x916)))
(let (($x981 (or $x920 $x977)))
(let (($x985 (and $x591 $x981)))
(let (($x989 (or $x851 $x985)))
(let (($x993 (and $x541 $x989)))
(let (($x997 (or $x841 $x993)))
(let (($x1076 (= (or (not (and $x931 (not (>= (+ ?v0!3 ?x685) 0)))) $x939) $x1075)))
(let ((@x1067 (monotonicity (rewrite (= (+ ?x937 ?x744) (+ ?x744 ?x937))) (= $x939 (<= (+ ?x744 ?x937) 0)))))
(let ((@x1074 (trans @x1067 (rewrite (= (<= (+ ?x744 ?x937) 0) $x1070)) (= $x939 $x1070))))
(let ((@x1045 (monotonicity (rewrite (= (+ ?v0!3 ?x685) (+ ?x685 ?v0!3))) (= (>= (+ ?v0!3 ?x685) 0) (>= (+ ?x685 ?v0!3) 0)))))
(let ((@x1052 (trans @x1045 (rewrite (= (>= (+ ?x685 ?v0!3) 0) $x1048)) (= (>= (+ ?v0!3 ?x685) 0) $x1048))))
(let ((@x1058 (monotonicity (monotonicity @x1052 (= (not (>= (+ ?v0!3 ?x685) 0)) $x1053)) (= (and $x931 (not (>= (+ ?v0!3 ?x685) 0))) $x1056))))
(let ((@x1061 (monotonicity @x1058 (= (not (and $x931 (not (>= (+ ?v0!3 ?x685) 0)))) $x1059))))
(let ((@x1083 (monotonicity (monotonicity (monotonicity @x1061 @x1074 $x1076) (= $x941 $x1078)) (= $x958 $x1081))))
(let ((@x1096 (monotonicity (rewrite (= $x966 $x784)) @x1083 (= $x969 (and $x784 $x1081)))))
(let ((@x1086 (monotonicity (rewrite (= $x927 $x725)) @x1083 (= $x962 (and $x725 $x1081)))))
(let ((@x1104 (monotonicity (trans @x1086 (rewrite (= (and $x725 $x1081) $x1087)) (= $x962 $x1087)) (trans @x1096 (rewrite (= (and $x784 $x1081) $x1097)) (= $x969 $x1097)) (= $x973 $x1102))))
(let ((@x1107 (monotonicity (rewrite (= $x924 $x670)) @x1104 (= $x977 (and $x670 $x1102)))))
(let (($x1017 (= (or $x903 (<= (+ (v_b_array$ ?v0!2) (* (- 1) v_b_max_G_4$)) 0)) $x1016)))
(let (($x906 (<= (+ (v_b_array$ ?v0!2) (* (- 1) v_b_max_G_4$)) 0)))
(let (($x1012 (= (<= (+ (* (- 1) v_b_max_G_4$) (v_b_array$ ?v0!2)) 0) $x1011)))
(let (($x1007 (= $x906 (<= (+ (* (- 1) v_b_max_G_4$) (v_b_array$ ?v0!2)) 0))))
(let (($x1004 (= (+ (v_b_array$ ?v0!2) (* (- 1) v_b_max_G_4$)) (+ (* (- 1) v_b_max_G_4$) (v_b_array$ ?v0!2)))))
(let ((@x1015 (trans (monotonicity (rewrite $x1004) $x1007) (rewrite $x1012) (= $x906 $x1011))))
(let ((@x1024 (monotonicity (monotonicity (monotonicity @x1015 $x1017) (= $x908 $x1019)) (= $x912 $x1022))))
(let ((@x1030 (monotonicity (rewrite (= $x871 $x612)) (monotonicity @x1024 (= $x916 $x1025)) (= $x920 (and $x612 $x1025)))))
(let ((@x1115 (monotonicity (trans @x1030 (rewrite (= (and $x612 $x1025) $x1031)) (= $x920 $x1031)) (trans @x1107 (rewrite (= (and $x670 $x1102) $x1108)) (= $x977 $x1108)) (= $x981 $x1113))))
(let ((@x1123 (trans (monotonicity @x1115 (= $x985 (and $x591 $x1113))) (rewrite (= (and $x591 $x1113) $x1119)) (= $x985 $x1119))))
(let ((@x1132 (monotonicity (monotonicity (monotonicity @x1123 (= $x989 $x1124)) (= $x993 $x1127)) (= $x997 $x1130))))
(let ((@x950 (nnf-neg (nnf-pos (refl (~ $x749 $x749)) (~ $x752 $x752)) (~ (not $x755) $x752))))
(let ((@x961 (nnf-neg (sk (~ $x755 $x941)) (nnf-neg @x950 (refl (~ $x951 $x951)) (~ (not $x758) $x954)) (~ (not $x761) $x958))))
(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))))
(let ((@x915 (nnf-neg (nnf-neg (sk (~ $x635 $x890)) (~ (not $x638) $x890)) (sk (~ (not $x649) $x908)) (~ (not $x652) $x912))))
(let ((@x919 (nnf-neg (nnf-neg (refl (~ (not $x632) (not $x632))) (~ $x638 $x877)) @x915 (~ (not $x655) $x916))))
(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))))
(let ((@x867 (monotonicity (refl (~ $x50 $x50)) (nnf-pos (refl (~ $x564 $x564)) (~ $x567 $x567)) (refl (~ $x63 $x63)) (refl (~ $x571 $x571)) (refl (~ $x573 $x573)) (~ $x591 $x591))))
(let ((@x988 (nnf-neg (nnf-neg @x867 (~ (not $x596) $x591)) @x984 (~ (not $x804) $x985))))
(let ((@x850 (nnf-neg (nnf-pos (refl (~ $x538 $x538)) (~ $x541 $x541)) (~ (not $x544) $x541))))
(let ((@x996 (nnf-neg @x850 (nnf-neg (refl (~ $x851 $x851)) @x988 (~ (not $x807) $x989)) (~ (not $x810) $x993))))
(let ((@x1000 (mp~ (not-or-elim (mp (asserted $x162) @x823 $x819) (not $x813)) (nnf-neg (sk (~ $x544 $x841)) @x996 (~ (not $x813) $x997)) $x997)))
(let ((@x1949 (mp (mp (mp @x1000 @x1132 $x1130) @x1427 $x1425) (monotonicity @x1945 (= $x1425 $x1946)) $x1946)))
(let ((@x2086 (unit-resolution (def-axiom (or $x1940 $x1934)) (unit-resolution @x1949 (lemma @x1690 $x1149) $x1943) $x1934)))
(let ((@x2093 (unit-resolution (def-axiom (or $x1937 $x851 $x1931)) (mp @x827 (symm (commutativity (= $x50 $x31)) (= $x31 $x50)) $x50) (or $x1937 $x1931))))
(let ((@x2094 (unit-resolution @x2093 @x2086 $x1931)))
(let ((@x2151 (monotonicity (unit-resolution (def-axiom (or $x1904 $x144)) @x2130 $x144) (= ?x135 ?x62))))
(let ((@x2154 (trans @x2151 (unit-resolution (def-axiom (or $x1928 $x63)) @x2094 $x63) (= ?x135 v_b_max_G_1$))))
(let ((@x2155 (trans @x2154 (symm (unit-resolution (def-axiom (or $x1904 $x145)) @x2130 $x145) $x1780) $x136)))
(let ((@x1523 (def-axiom (or $x1886 $x951))))
(let ((@x1808 (def-axiom (or $x1895 $x1318 $x1889))))
(let ((@x2157 (unit-resolution @x1808 (unit-resolution @x1523 @x2155 $x1886) (unit-resolution (def-axiom (or $x1904 $x1892)) @x2130 $x1892) $x1318)))
(let ((@x1812 (def-axiom (or $x1313 $x1436))))
(let ((@x2162 (unit-resolution ((_ th-lemma arith assign-bounds 1 -1 -1) (or $x1453 $x692 $x1070 (not $x1782))) (unit-resolution @x1812 @x2157 $x1436) (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x1780) $x1782)) @x2143 $x1782) (unit-resolution (def-axiom (or $x1904 $x689)) @x2130 $x689) $x1453)))
(let ((@x1565 ((_ th-lemma arith triangle-eq) (or $x1563 $x1445))))
(let (($x1558 (= v_b_p_G_0$ ?v0!3)))
(let ((?x1046 (* (- 1) ?v0!3)))
(let ((?x1510 (+ v_b_p_G_0$ ?x1046)))
(let (($x1560 (>= ?x1510 0)))
(let (($x1522 (>= ?x686 (- 1))))
(let ((@x2167 (unit-resolution ((_ th-lemma arith triangle-eq) (or $x1362 $x1522)) (unit-resolution (def-axiom (or $x1904 $x684)) @x2130 $x684) $x1522)))
(let ((@x2171 (unit-resolution ((_ th-lemma arith assign-bounds -1 -1) (or $x1560 $x1048 (not $x1522))) (unit-resolution (def-axiom (or $x1313 $x1053)) @x2157 $x1053) @x2167 $x1560)))
(let (($x1511 (<= ?x1510 0)))
(let (($x1488 (>= (+ v_b_max_G_1$ ?x1068) 0)))
(let (($x1955 (not $x1488)))
(let ((@x2174 (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)) @x2143 $x1782) (unit-resolution @x1812 @x2157 $x1436) $x1955)))
(let ((@x2102 (unit-resolution (def-axiom (or $x1928 $x1853)) @x2094 $x1853)))
(let (($x1476 (or $x1858 $x1298 $x1511 $x1488)))
(let (($x1535 (<= (+ ?x937 (* (- 1) v_b_max_G_1$)) 0)))
(let (($x1549 (>= (+ ?v0!3 ?x549) 0)))
(let (($x1501 (or $x1298 $x1549 $x1535)))
(let (($x1464 (or $x1858 $x1501)))
(let (($x1478 (= (+ ?x937 (* (- 1) v_b_max_G_1$)) (+ (* (- 1) v_b_max_G_1$) ?x937))))
(let ((@x1486 (monotonicity (rewrite $x1478) (= $x1535 (<= (+ (* (- 1) v_b_max_G_1$) ?x937) 0)))))
(let ((@x1472 (trans @x1486 (rewrite (= (<= (+ (* (- 1) v_b_max_G_1$) ?x937) 0) $x1488)) (= $x1535 $x1488))))
(let ((@x1509 (monotonicity (rewrite (= (+ ?v0!3 ?x549) (+ ?x549 ?v0!3))) (= $x1549 (>= (+ ?x549 ?v0!3) 0)))))
(let ((@x1497 (trans @x1509 (rewrite (= (>= (+ ?x549 ?v0!3) 0) $x1511)) (= $x1549 $x1511))))
(let ((@x1470 (monotonicity (monotonicity @x1497 @x1472 (= $x1501 (or $x1298 $x1511 $x1488))) (= $x1464 (or $x1858 (or $x1298 $x1511 $x1488))))))
(let ((@x1450 (trans @x1470 (rewrite (= (or $x1858 (or $x1298 $x1511 $x1488)) $x1476)) (= $x1464 $x1476))))
(let ((@x2176 (unit-resolution (mp ((_ quant-inst ?v0!3) $x1464) @x1450 $x1476) @x2102 (unit-resolution (def-axiom (or $x1313 $x931)) @x2157 $x931) @x2174 $x1511)))
(let ((@x2177 (unit-resolution ((_ th-lemma arith triangle-eq) (or $x1558 (not $x1511) (not $x1560))) @x2176 @x2171 $x1558)))
(let ((@x1551 (monotonicity (symm (hypothesis $x1558) (= ?v0!3 v_b_p_G_0$)) (= ?x937 ?x101))))
(let ((@x1540 (lemma (unit-resolution (hypothesis $x1563) (symm @x1551 $x1559) false) (or (not $x1558) $x1559))))
(let ((@x2179 (lemma (unit-resolution @x1540 @x2177 (unit-resolution @x1565 @x2162 $x1563) false) $x1904)))
(let ((@x2036 (symm (unit-resolution (def-axiom (or $x1872 $x73)) (hypothesis $x1875) $x73) (= v_b_max_G_1$ v_b_max_G_4$))))
(let (($x2082 (or (not (= v_b_max_G_1$ v_b_max_G_4$)) (<= (+ v_b_max_G_1$ (* (- 1) v_b_max_G_4$)) 0))))
(let ((@x2084 (unit-resolution ((_ th-lemma arith triangle-eq) $x2082) @x2036 (<= (+ v_b_max_G_1$ (* (- 1) v_b_max_G_4$)) 0))))
(let ((@x2018 (hypothesis $x1875)))
(let (($x2015 (= ?x62 v_b_max_G_4$)))
(let (($x2016 (or $x1286 (<= (+ v_b_length$ (* (- 1) v_b_k_G_0$)) 0) $x2015)))
(let ((@x2038 (unit-resolution (def-axiom (or $x2016 (not $x2015))) (trans (hypothesis $x63) @x2036 $x2015) $x2016)))
(let ((@x2041 (unit-resolution (def-axiom (or $x1869 $x1861 $x1275)) (unit-resolution (def-axiom (or $x1872 $x1866)) @x2018 $x1866) (hypothesis $x1274) $x1861)))
(let ((@x2042 (unit-resolution ((_ quant-inst v_b_k_G_0$) (or (not $x1861) (not $x2016))) @x2041 @x2038 false)))
(let ((@x2096 (unit-resolution (lemma @x2042 (or $x1872 $x1403 $x1275)) @x2018 (unit-resolution (def-axiom (or $x1928 $x63)) @x2094 $x63) $x1275)))
(let (($x2055 (>= (+ v_b_max_G_1$ (* (- 1) (v_b_array$ ?v0!2))) 0)))
(let ((@x2077 ((_ th-lemma arith farkas -1 -1 1) (hypothesis (<= (+ v_b_p_G_0$ (* (- 1) ?v0!2)) 0)) (hypothesis $x600) (hypothesis (not $x900)) false)))
(let ((@x2080 (lemma @x2077 (or (not (<= (+ v_b_p_G_0$ (* (- 1) ?v0!2)) 0)) $x661 $x900))))
(let ((@x2100 (unit-resolution @x2080 (unit-resolution (def-axiom (or $x1872 $x600)) @x2018 $x600) (unit-resolution (def-axiom (or $x1274 (not $x900))) @x2096 (not $x900)) (not (<= (+ v_b_p_G_0$ (* (- 1) ?v0!2)) 0)))))
(let (($x2023 (<= (+ v_b_p_G_0$ (* (- 1) ?v0!2)) 0)))
(let (($x2063 (or $x1858 $x1247 $x2023 $x2055)))
(let (($x2033 (<= (+ (v_b_array$ ?v0!2) (* (- 1) v_b_max_G_1$)) 0)))
(let (($x1999 (>= (+ ?v0!2 ?x549) 0)))
(let (($x2034 (or $x1247 $x1999 $x2033)))
(let (($x2064 (or $x1858 $x2034)))
(let (($x2056 (= (<= (+ (* (- 1) v_b_max_G_1$) (v_b_array$ ?v0!2)) 0) $x2055)))
(let (($x2052 (= $x2033 (<= (+ (* (- 1) v_b_max_G_1$) (v_b_array$ ?v0!2)) 0))))
(let (($x2049 (= (+ (v_b_array$ ?v0!2) (* (- 1) v_b_max_G_1$)) (+ (* (- 1) v_b_max_G_1$) (v_b_array$ ?v0!2)))))
(let ((@x2059 (trans (monotonicity (rewrite $x2049) $x2052) (rewrite $x2056) (= $x2033 $x2055))))
(let ((@x2004 (monotonicity (rewrite (= (+ ?v0!2 ?x549) (+ ?x549 ?v0!2))) (= $x1999 (>= (+ ?x549 ?v0!2) 0)))))
(let ((@x2047 (trans @x2004 (rewrite (= (>= (+ ?x549 ?v0!2) 0) $x2023)) (= $x1999 $x2023))))
(let ((@x2068 (monotonicity (monotonicity @x2047 @x2059 (= $x2034 (or $x1247 $x2023 $x2055))) (= $x2064 (or $x1858 (or $x1247 $x2023 $x2055))))))
(let ((@x2072 (trans @x2068 (rewrite (= (or $x1858 (or $x1247 $x2023 $x2055)) $x2063)) (= $x2064 $x2063))))
(let ((@x2104 (unit-resolution (mp ((_ quant-inst ?v0!2) $x2064) @x2072 $x2063) @x2102 (unit-resolution (def-axiom (or $x1274 $x897)) @x2096 $x897) (or $x2023 $x2055))))
(let ((@x2106 ((_ th-lemma arith farkas -1 1 1) (unit-resolution @x2104 @x2100 $x2055) (unit-resolution (def-axiom (or $x1274 (not $x1011))) @x2096 (not $x1011)) @x2084 false)))
(let ((@x2114 (unit-resolution (def-axiom (or $x1925 $x1875 $x1919)) (lemma @x2106 $x1872) (unit-resolution (def-axiom (or $x1928 $x1922)) @x2094 $x1922) $x1919)))
(let ((@x2001 (unit-resolution (def-axiom (or $x1913 $x1901 $x1907)) (unit-resolution (def-axiom (or $x1916 $x1910)) @x2114 $x1910) $x1910)))
(let ((@x2025 (unit-resolution @x2001 @x2179 $x1901)))
(let ((@x1557 (trans (monotonicity (hypothesis $x107) (= ?x135 ?x101)) (symm (hypothesis $x104) (= ?x101 v_b_max_G_2$)) (= ?x135 v_b_max_G_2$))))
(let ((@x1975 (trans @x1557 (symm (hypothesis $x109) (= v_b_max_G_2$ v_b_max_G_3$)) $x136)))
(let ((@x1978 (lemma (unit-resolution (hypothesis $x951) @x1975 false) (or $x136 $x1361 $x1359 $x1360))))
(let ((@x2121 (unit-resolution @x1978 (unit-resolution (def-axiom (or $x1898 $x109)) @x2025 $x109) (unit-resolution (def-axiom (or $x1898 $x104)) @x2025 $x104) (unit-resolution (def-axiom (or $x1898 $x107)) @x2025 $x107) $x136)))
(let ((@x2109 (unit-resolution ((_ th-lemma arith triangle-eq) (or $x1362 $x1522)) (unit-resolution (def-axiom (or $x1898 $x684)) @x2025 $x684) $x1522)))
(let ((@x1460 (unit-resolution @x1808 (unit-resolution @x1523 (hypothesis $x136) $x1886) (hypothesis $x1892) $x1318)))
(let ((@x1539 (def-axiom (or $x1313 $x1053))))
(let (($x1965 (not $x1560)))
(let (($x1597 (<= (+ ?x101 ?x744) 0)))
(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$))))
(let ((@x1435 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not (= ?x101 v_b_max_G_3$)) $x1597)) @x1431 $x1597)))
(let ((@x1437 (lemma ((_ th-lemma arith farkas -1 -1 1) (hypothesis $x1436) (hypothesis $x1597) (hypothesis $x1445) false) (or $x1453 $x1070 (not $x1597)))))
(let ((@x1952 (unit-resolution @x1565 (unit-resolution @x1437 (unit-resolution @x1812 @x1460 $x1436) @x1435 $x1453) $x1563)))
(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)))
(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))))
(let ((@x1969 (unit-resolution ((_ th-lemma arith triangle-eq) (or $x1558 (not $x1511) $x1965)) (unit-resolution @x1962 @x1958 $x1511) (or $x1558 $x1965))))
(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)))
(let ((@x2111 (unit-resolution (lemma @x1971 (or $x951 (not $x1522) $x1858 $x689 $x1895 $x1359 $x1361)) @x2102 (or $x951 (not $x1522) $x689 $x1895 $x1359 $x1361))))
(unit-resolution @x2111 @x2109 @x2121 (unit-resolution (def-axiom (or $x1898 $x692)) @x2025 $x692) (unit-resolution (def-axiom (or $x1898 $x1892)) @x2025 $x1892) (unit-resolution (def-axiom (or $x1898 $x104)) @x2025 $x104) (unit-resolution (def-axiom (or $x1898 $x109)) @x2025 $x109) false))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))