src/HOL/SMT_Examples/Boogie_Max.certs

--- a/src/HOL/SMT_Examples/Boogie_Max.certs	Wed Sep 30 23:31:18 2020 +0200
+++ b/src/HOL/SMT_Examples/Boogie_Max.certs	Wed Sep 30 23:37:07 2020 +0200
@@ -777,3 +777,782 @@
 (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))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
 
+5c906235df8ae94e7242f53402af877022224c12 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))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
+