0 JBC
↳1 JBC2FIG (⇒)
↳2 JBCTerminationGraph
↳3 FIGtoITRSProof (⇒)
↳4 AND
↳5 IDP
↳6 IDPNonInfProof (⇒)
↳7 AND
↳8 IDP
↳9 IDependencyGraphProof (⇔)
↳10 TRUE
↳11 IDP
↳12 IDependencyGraphProof (⇔)
↳13 TRUE
↳14 IDP
↳15 IDPNonInfProof (⇒)
↳16 IDP
↳17 IDependencyGraphProof (⇔)
↳18 TRUE
↳19 IDP
↳20 IDPNonInfProof (⇒)
↳21 IDP
↳22 IDependencyGraphProof (⇔)
↳23 TRUE
public class Power {
public static void main(String args[]) {
for (int i = 0; i < args.length; i++) {
even(power(args.length, args[i].length()));
odd( power(args.length, args[i].length()));
}
// power(args.length, args.length);
}
public static int power(int a, int n) {
if (n <= 0) return 1;
else if (n == 1) return a;
else {
int r = power(a * a, n/2);
if (n % 2 == 0) return r;
else return a * r;
}
}
public static boolean even(int n) {
if (n <= 0) return true;
else if (n == 1) return false;
else return odd(n - 1);
}
public static boolean odd(int n) {
if (n <= 0) return false;
else if (n == 1) return true;
else return even(n - 1);
}
}
Generated 26 rules for P and 26 rules for R.
Combined rules. Obtained 1 rules for P and 5 rules for R.
Filtered ground terms:
924_0_even_GT(x1, x2, x3) → 924_0_even_GT(x2, x3)
Cond_924_0_even_GT(x1, x2, x3, x4) → Cond_924_0_even_GT(x1, x3, x4)
1422_0_odd_Return(x1, x2) → 1422_0_odd_Return(x2)
1224_0_even_Return(x1, x2) → 1224_0_even_Return(x2)
1067_0_even_Return(x1, x2, x3) → 1067_0_even_Return
1372_0_odd_Return(x1, x2, x3) → 1372_0_odd_Return
980_0_even_Return(x1, x2) → 980_0_even_Return(x2)
Filtered duplicate args:
924_0_even_GT(x1, x2) → 924_0_even_GT(x2)
Cond_924_0_even_GT(x1, x2, x3) → Cond_924_0_even_GT(x1, x3)
Combined rules. Obtained 1 rules for P and 5 rules for R.
Finished conversion. Obtained 1 rules for P and 5 rules for R. System has predefined symbols.
Generated 16 rules for P and 27 rules for R.
Combined rules. Obtained 1 rules for P and 6 rules for R.
Filtered ground terms:
730_0_power_GT(x1, x2, x3) → 730_0_power_GT(x2, x3)
Cond_730_0_power_GT(x1, x2, x3, x4) → Cond_730_0_power_GT(x1, x3, x4)
1287_0_power_Return(x1) → 1287_0_power_Return
Cond_1072_0_power_NE(x1, x2, x3) → Cond_1072_0_power_NE(x1, x3)
1072_0_power_NE(x1, x2) → 1072_0_power_NE(x2)
1188_0_power_Return(x1) → 1188_0_power_Return
845_0_power_Return(x1, x2) → 845_0_power_Return
763_0_power_Return(x1, x2) → 763_0_power_Return
Filtered duplicate args:
730_0_power_GT(x1, x2) → 730_0_power_GT(x2)
Cond_730_0_power_GT(x1, x2, x3) → Cond_730_0_power_GT(x1, x3)
Filtered unneeded arguments:
Cond_1072_0_power_NE(x1, x2) → Cond_1072_0_power_NE(x1)
Combined rules. Obtained 1 rules for P and 6 rules for R.
Finished conversion. Obtained 1 rules for P and 6 rules for R. System has predefined symbols.
Generated 76 rules for P and 193 rules for R.
Combined rules. Obtained 14 rules for P and 25 rules for R.
Filtered ground terms:
2420_0_even_Load(x1, x2) → 2420_0_even_Load(x2)
1287_0_power_Return(x1, x2) → 1287_0_power_Return(x2)
845_0_power_Return(x1, x2, x3, x4) → 845_0_power_Return(x2, x4)
2595_0_power_Load(x1, x2, x3) → 2595_0_power_Load(x2, x3)
Cond_2420_1_main_InvokeMethod2(x1, x2, x3, x4, x5) → Cond_2420_1_main_InvokeMethod2(x1, x3, x4)
1067_0_even_Return(x1, x2, x3) → 1067_0_even_Return
2636_0_odd_Load(x1, x2) → 2636_0_odd_Load(x2)
2387_0_power_Load(x1, x2, x3) → 2387_0_power_Load(x2, x3)
Cond_2636_1_main_InvokeMethod2(x1, x2, x3, x4, x5) → Cond_2636_1_main_InvokeMethod2(x1, x3, x4)
1372_0_odd_Return(x1, x2, x3) → 1372_0_odd_Return
Cond_2636_1_main_InvokeMethod1(x1, x2, x3, x4, x5) → Cond_2636_1_main_InvokeMethod1(x1, x3, x4)
1347_0_odd_Return(x1, x2) → 1347_0_odd_Return(x2)
1422_0_odd_Return(x1, x2) → 1422_0_odd_Return(x2)
763_0_power_Return(x1, x2, x3, x4) → 763_0_power_Return(x2)
1188_0_power_Return(x1, x2, x3, x4) → 1188_0_power_Return(x2, x3, x4)
Cond_2420_1_main_InvokeMethod1(x1, x2, x3, x4, x5) → Cond_2420_1_main_InvokeMethod1(x1, x3, x4)
980_0_even_Return(x1, x2, x3) → 980_0_even_Return(x2)
1224_0_even_Return(x1, x2) → 1224_0_even_Return(x2)
Cond_1072_0_power_NE(x1, x2, x3, x4, x5) → Cond_1072_0_power_NE(x1, x3, x4, x5)
1072_0_power_NE(x1, x2, x3, x4) → 1072_0_power_NE(x2, x3, x4)
730_0_power_GT(x1, x2, x3, x4) → 730_0_power_GT(x2, x3, x4)
Cond_730_0_power_GT2(x1, x2, x3, x4, x5) → Cond_730_0_power_GT2(x1, x3, x4, x5)
960_0_power_Return(x1, x2, x3) → 960_0_power_Return(x2)
Cond_730_0_power_GT1(x1, x2, x3, x4, x5) → Cond_730_0_power_GT1(x1, x3, x4, x5)
Cond_730_0_power_GT(x1, x2, x3, x4, x5) → Cond_730_0_power_GT(x1, x3)
1300_0_odd_GT(x1, x2, x3) → 1300_0_odd_GT(x2, x3)
Cond_924_0_even_GT3(x1, x2, x3, x4) → Cond_924_0_even_GT3(x1, x3, x4)
924_0_even_GT(x1, x2, x3) → 924_0_even_GT(x2, x3)
1353_0_odd_Return(x1, x2) → 1353_0_odd_Return(x2)
Cond_924_0_even_GT2(x1, x2, x3, x4) → Cond_924_0_even_GT2(x1, x3, x4)
Cond_924_0_even_GT1(x1, x2, x3, x4) → Cond_924_0_even_GT1(x1)
Cond_924_0_even_GT(x1, x2, x3, x4) → Cond_924_0_even_GT(x1, x3, x4)
Cond_1300_0_odd_GT3(x1, x2, x3, x4) → Cond_1300_0_odd_GT3(x1, x3, x4)
1406_0_even_Return(x1, x2) → 1406_0_even_Return(x2)
Cond_1300_0_odd_GT2(x1, x2, x3, x4) → Cond_1300_0_odd_GT2(x1, x3, x4)
Cond_1300_0_odd_GT1(x1, x2, x3, x4) → Cond_1300_0_odd_GT1(x1)
Cond_1300_0_odd_GT(x1, x2, x3, x4) → Cond_1300_0_odd_GT(x1, x3, x4)
Filtered duplicate args:
845_0_power_Return(x1, x2) → 845_0_power_Return(x2)
1188_0_power_Return(x1, x2, x3) → 1188_0_power_Return(x1, x3)
730_0_power_GT(x1, x2, x3) → 730_0_power_GT(x1, x3)
Cond_730_0_power_GT2(x1, x2, x3, x4) → Cond_730_0_power_GT2(x1, x2, x4)
Cond_730_0_power_GT1(x1, x2, x3, x4) → Cond_730_0_power_GT1(x1, x2, x4)
1300_0_odd_GT(x1, x2) → 1300_0_odd_GT(x2)
Cond_924_0_even_GT3(x1, x2, x3) → Cond_924_0_even_GT3(x1, x3)
924_0_even_GT(x1, x2) → 924_0_even_GT(x2)
Cond_924_0_even_GT2(x1, x2, x3) → Cond_924_0_even_GT2(x1, x3)
Cond_924_0_even_GT(x1, x2, x3) → Cond_924_0_even_GT(x1, x3)
Cond_1300_0_odd_GT3(x1, x2, x3) → Cond_1300_0_odd_GT3(x1, x3)
Cond_1300_0_odd_GT2(x1, x2, x3) → Cond_1300_0_odd_GT2(x1, x3)
Cond_1300_0_odd_GT(x1, x2, x3) → Cond_1300_0_odd_GT(x1, x3)
Filtered unneeded arguments:
Cond_2420_1_main_InvokeMethod(x1, x2, x3, x4, x5) → Cond_2420_1_main_InvokeMethod(x1, x2, x3, x4)
Cond_2636_1_main_InvokeMethod(x1, x2, x3, x4, x5) → Cond_2636_1_main_InvokeMethod(x1, x2, x3, x4)
Cond_1300_0_odd_GT(x1, x2) → Cond_1300_0_odd_GT(x1)
Cond_924_0_even_GT(x1, x2) → Cond_924_0_even_GT(x1)
Cond_1072_0_power_NE(x1, x2, x3, x4) → Cond_1072_0_power_NE(x1, x2, x3)
Filtered all free variables:
2595_1_main_InvokeMethod(x1, x2, x3, x4, x5) → 2595_1_main_InvokeMethod(x2, x3, x4, x5)
2636_1_main_InvokeMethod(x1, x2, x3, x4) → 2636_1_main_InvokeMethod(x2, x3, x4)
Cond_2636_1_main_InvokeMethod(x1, x2, x3, x4) → Cond_2636_1_main_InvokeMethod(x1, x3, x4)
2387_1_main_InvokeMethod(x1, x2, x3, x4, x5) → 2387_1_main_InvokeMethod(x2, x3, x4, x5)
2420_1_main_InvokeMethod(x1, x2, x3, x4) → 2420_1_main_InvokeMethod(x2, x3, x4)
Cond_2420_1_main_InvokeMethod(x1, x2, x3, x4) → Cond_2420_1_main_InvokeMethod(x1, x3, x4)
1347_0_odd_Return(x1) → 1347_0_odd_Return
980_0_even_Return(x1) → 980_0_even_Return
Combined rules. Obtained 12 rules for P and 25 rules for R.
Finished conversion. Obtained 12 rules for P and 25 rules for R. System has predefined symbols.
!= | ~ | Neq: (Integer, Integer) -> Boolean |
* | ~ | Mul: (Integer, Integer) -> Integer |
>= | ~ | Ge: (Integer, Integer) -> Boolean |
-1 | ~ | UnaryMinus: (Integer) -> Integer |
| | ~ | Bwor: (Integer, Integer) -> Integer |
/ | ~ | Div: (Integer, Integer) -> Integer |
= | ~ | Eq: (Integer, Integer) -> Boolean |
~ | Bwxor: (Integer, Integer) -> Integer | |
|| | ~ | Lor: (Boolean, Boolean) -> Boolean |
! | ~ | Lnot: (Boolean) -> Boolean |
< | ~ | Lt: (Integer, Integer) -> Boolean |
- | ~ | Sub: (Integer, Integer) -> Integer |
<= | ~ | Le: (Integer, Integer) -> Boolean |
> | ~ | Gt: (Integer, Integer) -> Boolean |
~ | ~ | Bwnot: (Integer) -> Integer |
% | ~ | Mod: (Integer, Integer) -> Integer |
& | ~ | Bwand: (Integer, Integer) -> Integer |
+ | ~ | Add: (Integer, Integer) -> Integer |
&& | ~ | Land: (Boolean, Boolean) -> Boolean |
Integer, Boolean
(0) -> (1), if ((x0[0] > 0 && !(x0[0] = 1) && 0 < x0[0] - 1 && !(x0[0] - 1 = 1) →* TRUE)∧(x0[0] →* x0[1]))
(1) -> (0), if ((x0[1] - 1 - 1 →* x0[0]))
(1) (&&(&&(&&(>(x0[0], 0), !(=(x0[0], 1))), <(0, -(x0[0], 1))), !(=(-(x0[0], 1), 1)))=TRUE∧x0[0]=x0[1] ⇒ 924_0_EVEN_GT(x0[0])≥NonInfC∧924_0_EVEN_GT(x0[0])≥COND_924_0_EVEN_GT(&&(&&(&&(>(x0[0], 0), !(=(x0[0], 1))), <(0, -(x0[0], 1))), !(=(-(x0[0], 1), 1))), x0[0])∧(UIncreasing(COND_924_0_EVEN_GT(&&(&&(&&(>(x0[0], 0), !(=(x0[0], 1))), <(0, -(x0[0], 1))), !(=(-(x0[0], 1), 1))), x0[0])), ≥))
(2) (<(0, -(x0[0], 1))=TRUE∧>(x0[0], 0)=TRUE∧<(-(x0[0], 1), 1)=TRUE∧<(x0[0], 1)=TRUE ⇒ 924_0_EVEN_GT(x0[0])≥NonInfC∧924_0_EVEN_GT(x0[0])≥COND_924_0_EVEN_GT(&&(&&(&&(>(x0[0], 0), !(=(x0[0], 1))), <(0, -(x0[0], 1))), !(=(-(x0[0], 1), 1))), x0[0])∧(UIncreasing(COND_924_0_EVEN_GT(&&(&&(&&(>(x0[0], 0), !(=(x0[0], 1))), <(0, -(x0[0], 1))), !(=(-(x0[0], 1), 1))), x0[0])), ≥))
(3) (<(0, -(x0[0], 1))=TRUE∧>(x0[0], 0)=TRUE∧<(-(x0[0], 1), 1)=TRUE∧>(x0[0], 1)=TRUE ⇒ 924_0_EVEN_GT(x0[0])≥NonInfC∧924_0_EVEN_GT(x0[0])≥COND_924_0_EVEN_GT(&&(&&(&&(>(x0[0], 0), !(=(x0[0], 1))), <(0, -(x0[0], 1))), !(=(-(x0[0], 1), 1))), x0[0])∧(UIncreasing(COND_924_0_EVEN_GT(&&(&&(&&(>(x0[0], 0), !(=(x0[0], 1))), <(0, -(x0[0], 1))), !(=(-(x0[0], 1), 1))), x0[0])), ≥))
(4) (x0[0] + [-2] ≥ 0∧x0[0] + [-1] ≥ 0∧[1] + [-1]x0[0] ≥ 0∧[-1]x0[0] ≥ 0 ⇒ (UIncreasing(COND_924_0_EVEN_GT(&&(&&(&&(>(x0[0], 0), !(=(x0[0], 1))), <(0, -(x0[0], 1))), !(=(-(x0[0], 1), 1))), x0[0])), ≥)∧[bni_23 + (-1)Bound*bni_23] + [(2)bni_23]x0[0] ≥ 0∧[(-1)bso_24] ≥ 0)
(5) (x0[0] + [-2] ≥ 0∧x0[0] + [-1] ≥ 0∧[1] + [-1]x0[0] ≥ 0∧x0[0] + [-2] ≥ 0 ⇒ (UIncreasing(COND_924_0_EVEN_GT(&&(&&(&&(>(x0[0], 0), !(=(x0[0], 1))), <(0, -(x0[0], 1))), !(=(-(x0[0], 1), 1))), x0[0])), ≥)∧[bni_23 + (-1)Bound*bni_23] + [(2)bni_23]x0[0] ≥ 0∧[(-1)bso_24] ≥ 0)
(6) (x0[0] + [-2] ≥ 0∧x0[0] + [-1] ≥ 0∧[1] + [-1]x0[0] ≥ 0∧[-1]x0[0] ≥ 0 ⇒ (UIncreasing(COND_924_0_EVEN_GT(&&(&&(&&(>(x0[0], 0), !(=(x0[0], 1))), <(0, -(x0[0], 1))), !(=(-(x0[0], 1), 1))), x0[0])), ≥)∧[bni_23 + (-1)Bound*bni_23] + [(2)bni_23]x0[0] ≥ 0∧[(-1)bso_24] ≥ 0)
(7) (x0[0] + [-2] ≥ 0∧x0[0] + [-1] ≥ 0∧[1] + [-1]x0[0] ≥ 0∧x0[0] + [-2] ≥ 0 ⇒ (UIncreasing(COND_924_0_EVEN_GT(&&(&&(&&(>(x0[0], 0), !(=(x0[0], 1))), <(0, -(x0[0], 1))), !(=(-(x0[0], 1), 1))), x0[0])), ≥)∧[bni_23 + (-1)Bound*bni_23] + [(2)bni_23]x0[0] ≥ 0∧[(-1)bso_24] ≥ 0)
(9) (x0[0] + [-2] ≥ 0∧x0[0] + [-1] ≥ 0∧x0[0] + [-3] ≥ 0∧[-1]x0[0] ≥ 0 ⇒ (UIncreasing(COND_924_0_EVEN_GT(&&(&&(&&(>(x0[0], 0), !(=(x0[0], 1))), <(0, -(x0[0], 1))), !(=(-(x0[0], 1), 1))), x0[0])), ≥)∧[bni_23 + (-1)Bound*bni_23] + [(2)bni_23]x0[0] ≥ 0∧[(-1)bso_24] ≥ 0)
(11) (x0[0] + [-2] ≥ 0∧x0[0] + [-1] ≥ 0∧x0[0] + [-3] ≥ 0∧x0[0] + [-2] ≥ 0 ⇒ (UIncreasing(COND_924_0_EVEN_GT(&&(&&(&&(>(x0[0], 0), !(=(x0[0], 1))), <(0, -(x0[0], 1))), !(=(-(x0[0], 1), 1))), x0[0])), ≥)∧[bni_23 + (-1)Bound*bni_23] + [(2)bni_23]x0[0] ≥ 0∧[(-1)bso_24] ≥ 0)
(12) (x0[0] + [-2] ≥ 0∧x0[0] + [-1] ≥ 0∧[1] + [-1]x0[0] ≥ 0∧[-1]x0[0] ≥ 0 ⇒ (UIncreasing(COND_924_0_EVEN_GT(&&(&&(&&(>(x0[0], 0), !(=(x0[0], 1))), <(0, -(x0[0], 1))), !(=(-(x0[0], 1), 1))), x0[0])), ≥)∧[bni_23 + (-1)Bound*bni_23] + [(2)bni_23]x0[0] ≥ 0∧[(-1)bso_24] ≥ 0)
(13) (x0[0] + [-2] ≥ 0∧x0[0] + [-1] ≥ 0∧[1] + [-1]x0[0] ≥ 0∧x0[0] + [-2] ≥ 0 ⇒ (UIncreasing(COND_924_0_EVEN_GT(&&(&&(&&(>(x0[0], 0), !(=(x0[0], 1))), <(0, -(x0[0], 1))), !(=(-(x0[0], 1), 1))), x0[0])), ≥)∧[bni_23 + (-1)Bound*bni_23] + [(2)bni_23]x0[0] ≥ 0∧[(-1)bso_24] ≥ 0)
(14) (x0[0] + [-2] ≥ 0∧x0[0] + [-1] ≥ 0∧x0[0] + [-3] ≥ 0∧[-1]x0[0] ≥ 0 ⇒ (UIncreasing(COND_924_0_EVEN_GT(&&(&&(&&(>(x0[0], 0), !(=(x0[0], 1))), <(0, -(x0[0], 1))), !(=(-(x0[0], 1), 1))), x0[0])), ≥)∧[bni_23 + (-1)Bound*bni_23] + [(2)bni_23]x0[0] ≥ 0∧[(-1)bso_24] ≥ 0)
(15) (x0[0] + [-2] ≥ 0∧x0[0] + [-1] ≥ 0∧x0[0] + [-3] ≥ 0∧x0[0] + [-2] ≥ 0 ⇒ (UIncreasing(COND_924_0_EVEN_GT(&&(&&(&&(>(x0[0], 0), !(=(x0[0], 1))), <(0, -(x0[0], 1))), !(=(-(x0[0], 1), 1))), x0[0])), ≥)∧[bni_23 + (-1)Bound*bni_23] + [(2)bni_23]x0[0] ≥ 0∧[(-1)bso_24] ≥ 0)
(16) (x0[0] ≥ 0∧[1] + x0[0] ≥ 0∧[-1] + x0[0] ≥ 0∧x0[0] ≥ 0 ⇒ (UIncreasing(COND_924_0_EVEN_GT(&&(&&(&&(>(x0[0], 0), !(=(x0[0], 1))), <(0, -(x0[0], 1))), !(=(-(x0[0], 1), 1))), x0[0])), ≥)∧[(5)bni_23 + (-1)Bound*bni_23] + [(2)bni_23]x0[0] ≥ 0∧[(-1)bso_24] ≥ 0)
(17) ([1] + x0[0] ≥ 0∧[2] + x0[0] ≥ 0∧x0[0] ≥ 0∧[1] + x0[0] ≥ 0 ⇒ (UIncreasing(COND_924_0_EVEN_GT(&&(&&(&&(>(x0[0], 0), !(=(x0[0], 1))), <(0, -(x0[0], 1))), !(=(-(x0[0], 1), 1))), x0[0])), ≥)∧[(7)bni_23 + (-1)Bound*bni_23] + [(2)bni_23]x0[0] ≥ 0∧[(-1)bso_24] ≥ 0)
(18) (COND_924_0_EVEN_GT(TRUE, x0[1])≥NonInfC∧COND_924_0_EVEN_GT(TRUE, x0[1])≥924_0_EVEN_GT(-(-(x0[1], 1), 1))∧(UIncreasing(924_0_EVEN_GT(-(-(x0[1], 1), 1))), ≥))
(19) ((UIncreasing(924_0_EVEN_GT(-(-(x0[1], 1), 1))), ≥)∧[4 + (-1)bso_26] ≥ 0)
(20) ((UIncreasing(924_0_EVEN_GT(-(-(x0[1], 1), 1))), ≥)∧[4 + (-1)bso_26] ≥ 0)
(21) ((UIncreasing(924_0_EVEN_GT(-(-(x0[1], 1), 1))), ≥)∧[4 + (-1)bso_26] ≥ 0)
(22) ((UIncreasing(924_0_EVEN_GT(-(-(x0[1], 1), 1))), ≥)∧0 = 0∧[4 + (-1)bso_26] ≥ 0)
POL(TRUE) = 0
POL(FALSE) = 0
POL(924_0_even_GT(x1)) = [-1] + [-1]x1
POL(Cond_924_0_even_GT(x1, x2)) = [-1] + [-1]x2
POL(<=(x1, x2)) = [-1]
POL(0) = 0
POL(980_0_even_Return(x1)) = x1
POL(1172_1_even_InvokeMethod(x1, x2)) = [-1]
POL(1372_0_odd_Return) = [-1]
POL(1) = [1]
POL(1224_0_even_Return(x1)) = [-1]
POL(1422_0_odd_Return(x1)) = [-1]
POL(1401_1_odd_InvokeMethod(x1, x2)) = [-1]
POL(1067_0_even_Return) = [-1]
POL(924_0_EVEN_GT(x1)) = [1] + [2]x1
POL(COND_924_0_EVEN_GT(x1, x2)) = [1] + [2]x2
POL(&&(x1, x2)) = [-1]
POL(>(x1, x2)) = [-1]
POL(!(x1)) = [-1]
POL(=(x1, x2)) = [-1]
POL(<(x1, x2)) = [-1]
POL(-(x1, x2)) = x1 + [-1]x2
COND_924_0_EVEN_GT(TRUE, x0[1]) → 924_0_EVEN_GT(-(-(x0[1], 1), 1))
924_0_EVEN_GT(x0[0]) → COND_924_0_EVEN_GT(&&(&&(&&(>(x0[0], 0), !(=(x0[0], 1))), <(0, -(x0[0], 1))), !(=(-(x0[0], 1), 1))), x0[0])
924_0_EVEN_GT(x0[0]) → COND_924_0_EVEN_GT(&&(&&(&&(>(x0[0], 0), !(=(x0[0], 1))), <(0, -(x0[0], 1))), !(=(-(x0[0], 1), 1))), x0[0])
!= | ~ | Neq: (Integer, Integer) -> Boolean |
* | ~ | Mul: (Integer, Integer) -> Integer |
>= | ~ | Ge: (Integer, Integer) -> Boolean |
-1 | ~ | UnaryMinus: (Integer) -> Integer |
| | ~ | Bwor: (Integer, Integer) -> Integer |
/ | ~ | Div: (Integer, Integer) -> Integer |
= | ~ | Eq: (Integer, Integer) -> Boolean |
~ | Bwxor: (Integer, Integer) -> Integer | |
|| | ~ | Lor: (Boolean, Boolean) -> Boolean |
! | ~ | Lnot: (Boolean) -> Boolean |
< | ~ | Lt: (Integer, Integer) -> Boolean |
- | ~ | Sub: (Integer, Integer) -> Integer |
<= | ~ | Le: (Integer, Integer) -> Boolean |
> | ~ | Gt: (Integer, Integer) -> Boolean |
~ | ~ | Bwnot: (Integer) -> Integer |
% | ~ | Mod: (Integer, Integer) -> Integer |
& | ~ | Bwand: (Integer, Integer) -> Integer |
+ | ~ | Add: (Integer, Integer) -> Integer |
&& | ~ | Land: (Boolean, Boolean) -> Boolean |
Integer, Boolean
!= | ~ | Neq: (Integer, Integer) -> Boolean |
* | ~ | Mul: (Integer, Integer) -> Integer |
>= | ~ | Ge: (Integer, Integer) -> Boolean |
-1 | ~ | UnaryMinus: (Integer) -> Integer |
| | ~ | Bwor: (Integer, Integer) -> Integer |
/ | ~ | Div: (Integer, Integer) -> Integer |
= | ~ | Eq: (Integer, Integer) -> Boolean |
~ | Bwxor: (Integer, Integer) -> Integer | |
|| | ~ | Lor: (Boolean, Boolean) -> Boolean |
! | ~ | Lnot: (Boolean) -> Boolean |
< | ~ | Lt: (Integer, Integer) -> Boolean |
- | ~ | Sub: (Integer, Integer) -> Integer |
<= | ~ | Le: (Integer, Integer) -> Boolean |
> | ~ | Gt: (Integer, Integer) -> Boolean |
~ | ~ | Bwnot: (Integer) -> Integer |
% | ~ | Mod: (Integer, Integer) -> Integer |
& | ~ | Bwand: (Integer, Integer) -> Integer |
+ | ~ | Add: (Integer, Integer) -> Integer |
&& | ~ | Land: (Boolean, Boolean) -> Boolean |
Integer
!= | ~ | Neq: (Integer, Integer) -> Boolean |
* | ~ | Mul: (Integer, Integer) -> Integer |
>= | ~ | Ge: (Integer, Integer) -> Boolean |
-1 | ~ | UnaryMinus: (Integer) -> Integer |
| | ~ | Bwor: (Integer, Integer) -> Integer |
/ | ~ | Div: (Integer, Integer) -> Integer |
= | ~ | Eq: (Integer, Integer) -> Boolean |
~ | Bwxor: (Integer, Integer) -> Integer | |
|| | ~ | Lor: (Boolean, Boolean) -> Boolean |
! | ~ | Lnot: (Boolean) -> Boolean |
< | ~ | Lt: (Integer, Integer) -> Boolean |
- | ~ | Sub: (Integer, Integer) -> Integer |
<= | ~ | Le: (Integer, Integer) -> Boolean |
> | ~ | Gt: (Integer, Integer) -> Boolean |
~ | ~ | Bwnot: (Integer) -> Integer |
% | ~ | Mod: (Integer, Integer) -> Integer |
& | ~ | Bwand: (Integer, Integer) -> Integer |
+ | ~ | Add: (Integer, Integer) -> Integer |
&& | ~ | Land: (Boolean, Boolean) -> Boolean |
Integer, Boolean
(0) -> (1), if ((x0[0] > 1 →* TRUE)∧(x0[0] →* x0[1]))
(1) -> (0), if ((x0[1] / 2 →* x0[0]))
(1) (>(x0[0], 1)=TRUE∧x0[0]=x0[1] ⇒ 730_0_POWER_GT(x0[0])≥NonInfC∧730_0_POWER_GT(x0[0])≥COND_730_0_POWER_GT(>(x0[0], 1), x0[0])∧(UIncreasing(COND_730_0_POWER_GT(>(x0[0], 1), x0[0])), ≥))
(2) (>(x0[0], 1)=TRUE ⇒ 730_0_POWER_GT(x0[0])≥NonInfC∧730_0_POWER_GT(x0[0])≥COND_730_0_POWER_GT(>(x0[0], 1), x0[0])∧(UIncreasing(COND_730_0_POWER_GT(>(x0[0], 1), x0[0])), ≥))
(3) (x0[0] + [-2] ≥ 0 ⇒ (UIncreasing(COND_730_0_POWER_GT(>(x0[0], 1), x0[0])), ≥)∧[(-1)bni_26 + (-1)Bound*bni_26] + [bni_26]x0[0] ≥ 0∧[(-1)bso_27] ≥ 0)
(4) (x0[0] + [-2] ≥ 0 ⇒ (UIncreasing(COND_730_0_POWER_GT(>(x0[0], 1), x0[0])), ≥)∧[(-1)bni_26 + (-1)Bound*bni_26] + [bni_26]x0[0] ≥ 0∧[(-1)bso_27] ≥ 0)
(5) (x0[0] + [-2] ≥ 0 ⇒ (UIncreasing(COND_730_0_POWER_GT(>(x0[0], 1), x0[0])), ≥)∧[(-1)bni_26 + (-1)Bound*bni_26] + [bni_26]x0[0] ≥ 0∧[(-1)bso_27] ≥ 0)
(6) (x0[0] ≥ 0 ⇒ (UIncreasing(COND_730_0_POWER_GT(>(x0[0], 1), x0[0])), ≥)∧[bni_26 + (-1)Bound*bni_26] + [bni_26]x0[0] ≥ 0∧[(-1)bso_27] ≥ 0)
(7) (>(x0[0], 1)=TRUE∧x0[0]=x0[1]∧/(x0[1], 2)=x0[0]1 ⇒ COND_730_0_POWER_GT(TRUE, x0[1])≥NonInfC∧COND_730_0_POWER_GT(TRUE, x0[1])≥730_0_POWER_GT(/(x0[1], 2))∧(UIncreasing(730_0_POWER_GT(/(x0[1], 2))), ≥))
(8) (>(x0[0], 1)=TRUE ⇒ COND_730_0_POWER_GT(TRUE, x0[0])≥NonInfC∧COND_730_0_POWER_GT(TRUE, x0[0])≥730_0_POWER_GT(/(x0[0], 2))∧(UIncreasing(730_0_POWER_GT(/(x0[1], 2))), ≥))
(9) (x0[0] + [-2] ≥ 0 ⇒ (UIncreasing(730_0_POWER_GT(/(x0[1], 2))), ≥)∧[(-1)bni_28 + (-1)Bound*bni_28] + [bni_28]x0[0] ≥ 0∧[1 + (-1)bso_32] + x0[0] + [-1]max{x0[0], [-1]x0[0]} ≥ 0)
(10) (x0[0] + [-2] ≥ 0 ⇒ (UIncreasing(730_0_POWER_GT(/(x0[1], 2))), ≥)∧[(-1)bni_28 + (-1)Bound*bni_28] + [bni_28]x0[0] ≥ 0∧[1 + (-1)bso_32] + x0[0] + [-1]max{x0[0], [-1]x0[0]} ≥ 0)
(11) (x0[0] + [-2] ≥ 0∧[2]x0[0] ≥ 0 ⇒ (UIncreasing(730_0_POWER_GT(/(x0[1], 2))), ≥)∧[(-1)bni_28 + (-1)Bound*bni_28] + [bni_28]x0[0] ≥ 0∧[1 + (-1)bso_32] ≥ 0)
(12) (x0[0] ≥ 0∧[4] + [2]x0[0] ≥ 0 ⇒ (UIncreasing(730_0_POWER_GT(/(x0[1], 2))), ≥)∧[bni_28 + (-1)Bound*bni_28] + [bni_28]x0[0] ≥ 0∧[1 + (-1)bso_32] ≥ 0)
(13) (x0[0] ≥ 0∧[2] + x0[0] ≥ 0 ⇒ (UIncreasing(730_0_POWER_GT(/(x0[1], 2))), ≥)∧[bni_28 + (-1)Bound*bni_28] + [bni_28]x0[0] ≥ 0∧[1 + (-1)bso_32] ≥ 0)
POL(TRUE) = [1]
POL(FALSE) = 0
POL(730_0_power_GT(x1)) = [-1] + [-1]x1
POL(0) = 0
POL(763_0_power_Return) = [-1]
POL(955_1_power_InvokeMethod(x1, x2, x3)) = [-1] + [-1]x3 + [-1]x2 + [-1]x1
POL(845_0_power_Return) = [-1]
POL(1) = [1]
POL(1072_0_power_NE(x1)) = [-1] + [-1]x1
POL(2) = [2]
POL(1188_0_power_Return) = [-1]
POL(1287_0_power_Return) = [-1]
POL(Cond_1072_0_power_NE(x1, x2)) = [-1] + [-1]x2 + [-1]x1
POL(!(x1)) = [-1]
POL(=(x1, x2)) = [-1]
POL(730_0_POWER_GT(x1)) = [-1] + x1
POL(COND_730_0_POWER_GT(x1, x2)) = [-1] + x2
POL(>(x1, x2)) = [-1]
Polynomial Interpretations with Context Sensitive Arithemetic Replacement
POL(TermCSAR-Mode @ Context)
POL(/(x1, 2)1 @ {730_0_POWER_GT_1/0}) = max{x1, [-1]x1} + [-1]
COND_730_0_POWER_GT(TRUE, x0[1]) → 730_0_POWER_GT(/(x0[1], 2))
730_0_POWER_GT(x0[0]) → COND_730_0_POWER_GT(>(x0[0], 1), x0[0])
COND_730_0_POWER_GT(TRUE, x0[1]) → 730_0_POWER_GT(/(x0[1], 2))
730_0_POWER_GT(x0[0]) → COND_730_0_POWER_GT(>(x0[0], 1), x0[0])
/1 →
!= | ~ | Neq: (Integer, Integer) -> Boolean |
* | ~ | Mul: (Integer, Integer) -> Integer |
>= | ~ | Ge: (Integer, Integer) -> Boolean |
-1 | ~ | UnaryMinus: (Integer) -> Integer |
| | ~ | Bwor: (Integer, Integer) -> Integer |
/ | ~ | Div: (Integer, Integer) -> Integer |
= | ~ | Eq: (Integer, Integer) -> Boolean |
~ | Bwxor: (Integer, Integer) -> Integer | |
|| | ~ | Lor: (Boolean, Boolean) -> Boolean |
! | ~ | Lnot: (Boolean) -> Boolean |
< | ~ | Lt: (Integer, Integer) -> Boolean |
- | ~ | Sub: (Integer, Integer) -> Integer |
<= | ~ | Le: (Integer, Integer) -> Boolean |
> | ~ | Gt: (Integer, Integer) -> Boolean |
~ | ~ | Bwnot: (Integer) -> Integer |
% | ~ | Mod: (Integer, Integer) -> Integer |
& | ~ | Bwand: (Integer, Integer) -> Integer |
+ | ~ | Add: (Integer, Integer) -> Integer |
&& | ~ | Land: (Boolean, Boolean) -> Boolean |
Integer, Boolean
!= | ~ | Neq: (Integer, Integer) -> Boolean |
* | ~ | Mul: (Integer, Integer) -> Integer |
>= | ~ | Ge: (Integer, Integer) -> Boolean |
-1 | ~ | UnaryMinus: (Integer) -> Integer |
| | ~ | Bwor: (Integer, Integer) -> Integer |
/ | ~ | Div: (Integer, Integer) -> Integer |
= | ~ | Eq: (Integer, Integer) -> Boolean |
~ | Bwxor: (Integer, Integer) -> Integer | |
|| | ~ | Lor: (Boolean, Boolean) -> Boolean |
! | ~ | Lnot: (Boolean) -> Boolean |
< | ~ | Lt: (Integer, Integer) -> Boolean |
- | ~ | Sub: (Integer, Integer) -> Integer |
<= | ~ | Le: (Integer, Integer) -> Boolean |
> | ~ | Gt: (Integer, Integer) -> Boolean |
~ | ~ | Bwnot: (Integer) -> Integer |
% | ~ | Mod: (Integer, Integer) -> Integer |
& | ~ | Bwand: (Integer, Integer) -> Integer |
+ | ~ | Add: (Integer, Integer) -> Integer |
&& | ~ | Land: (Boolean, Boolean) -> Boolean |
Integer, Boolean
(0) -> (2), if ((java.lang.Object(ARRAY(x0[0], x3[0])) →* java.lang.Object(ARRAY(x1[2], x2[2])))∧(x4[0] →* x3[2])∧(x1[0] →* x4[2]))
(0) -> (4), if ((java.lang.Object(ARRAY(x0[0], x3[0])) →* java.lang.Object(ARRAY(x2[4], x3[4])))∧(x4[0] →* x4[4])∧(x1[0] →* 0))
(0) -> (15), if ((java.lang.Object(ARRAY(x0[0], x3[0])) →* java.lang.Object(ARRAY(x2[15], x3[15])))∧(x4[0] →* x4[15])∧(x1[0] →* 1))
(1) -> (2), if ((java.lang.Object(ARRAY(x0[1], x4[1])) →* java.lang.Object(ARRAY(x1[2], x2[2])))∧(x5[1] →* x3[2])∧(1 →* x4[2]))
(1) -> (4), if ((java.lang.Object(ARRAY(x0[1], x4[1])) →* java.lang.Object(ARRAY(x2[4], x3[4])))∧(x5[1] →* x4[4])∧(1 →* 0))
(1) -> (15), if ((java.lang.Object(ARRAY(x0[1], x4[1])) →* java.lang.Object(ARRAY(x2[15], x3[15])))∧(x5[1] →* x4[15]))
(2) -> (3), if ((x3[2] >= 0 && x3[2] < x1[2] →* TRUE)∧(java.lang.Object(ARRAY(x1[2], x2[2])) →* java.lang.Object(ARRAY(x1[3], x2[3])))∧(x3[2] →* x3[3])∧(x4[2] →* x4[3]))
(3) -> (6), if ((java.lang.Object(ARRAY(x1[3], x2[3])) →* java.lang.Object(ARRAY(x2[6], x3[6])))∧(x3[3] →* x4[6])∧(x1[3] →* x0[6])∧(x5[3] →* x5[6]))
(3) -> (7), if ((java.lang.Object(ARRAY(x1[3], x2[3])) →* java.lang.Object(ARRAY(x3[7], x4[7])))∧(x3[3] →* x5[7])∧(x1[3] →* x0[7])∧(x5[3] →* 0))
(3) -> (14), if ((java.lang.Object(ARRAY(x1[3], x2[3])) →* java.lang.Object(ARRAY(x2[14], x3[14])))∧(x3[3] →* x4[14])∧(x1[3] →* x0[14])∧(x5[3] →* 1))
(4) -> (5), if ((x4[4] >= 0 && x4[4] < x2[4] →* TRUE)∧(java.lang.Object(ARRAY(x2[4], x3[4])) →* java.lang.Object(ARRAY(x2[5], x3[5])))∧(x4[4] →* x4[5]))
(5) -> (6), if ((java.lang.Object(ARRAY(x2[5], x3[5])) →* java.lang.Object(ARRAY(x2[6], x3[6])))∧(x4[5] →* x4[6])∧(x2[5] →* x0[6])∧(x6[5] →* x5[6]))
(5) -> (7), if ((java.lang.Object(ARRAY(x2[5], x3[5])) →* java.lang.Object(ARRAY(x3[7], x4[7])))∧(x4[5] →* x5[7])∧(x2[5] →* x0[7])∧(x6[5] →* 0))
(5) -> (14), if ((java.lang.Object(ARRAY(x2[5], x3[5])) →* java.lang.Object(ARRAY(x2[14], x3[14])))∧(x4[5] →* x4[14])∧(x2[5] →* x0[14])∧(x6[5] →* 1))
(6) -> (8), if ((java.lang.Object(ARRAY(x0[6], x3[6])) →* java.lang.Object(ARRAY(x1[8], x2[8])))∧(x4[6] →* x3[8])∧(x1[6] →* x4[8]))
(6) -> (10), if ((java.lang.Object(ARRAY(x0[6], x3[6])) →* java.lang.Object(ARRAY(x1[10], x2[10])))∧(x4[6] →* x3[10])∧(x1[6] →* 0))
(6) -> (12), if ((java.lang.Object(ARRAY(x0[6], x3[6])) →* java.lang.Object(ARRAY(x2[12], x3[12])))∧(x4[6] →* x4[12])∧(x1[6] →* 1))
(7) -> (8), if ((java.lang.Object(ARRAY(x0[7], x4[7])) →* java.lang.Object(ARRAY(x1[8], x2[8])))∧(x5[7] →* x3[8])∧(1 →* x4[8]))
(7) -> (10), if ((java.lang.Object(ARRAY(x0[7], x4[7])) →* java.lang.Object(ARRAY(x1[10], x2[10])))∧(x5[7] →* x3[10])∧(1 →* 0))
(7) -> (12), if ((java.lang.Object(ARRAY(x0[7], x4[7])) →* java.lang.Object(ARRAY(x2[12], x3[12])))∧(x5[7] →* x4[12]))
(8) -> (9), if ((x3[8] >= 0 && x1[8] > x3[8] + 1 && 0 <= x3[8] + 1 →* TRUE)∧(java.lang.Object(ARRAY(x1[8], x2[8])) →* java.lang.Object(ARRAY(x1[9], x2[9])))∧(x3[8] →* x3[9])∧(x4[8] →* x4[9]))
(9) -> (0), if ((java.lang.Object(ARRAY(x1[9], x2[9])) →* java.lang.Object(ARRAY(x2[0], x3[0])))∧(x3[9] + 1 →* x4[0])∧(x1[9] →* x0[0])∧(x5[9] →* x5[0]))
(9) -> (1), if ((java.lang.Object(ARRAY(x1[9], x2[9])) →* java.lang.Object(ARRAY(x3[1], x4[1])))∧(x3[9] + 1 →* x5[1])∧(x1[9] →* x0[1])∧(x5[9] →* 0))
(9) -> (17), if ((java.lang.Object(ARRAY(x1[9], x2[9])) →* java.lang.Object(ARRAY(x2[17], x3[17])))∧(x3[9] + 1 →* x4[17])∧(x1[9] →* x0[17])∧(x5[9] →* 1))
(10) -> (11), if ((x3[10] >= 0 && x1[10] > x3[10] + 1 && 0 <= x3[10] + 1 →* TRUE)∧(java.lang.Object(ARRAY(x1[10], x2[10])) →* java.lang.Object(ARRAY(x1[11], x2[11])))∧(x3[10] →* x3[11]))
(11) -> (0), if ((java.lang.Object(ARRAY(x1[11], x2[11])) →* java.lang.Object(ARRAY(x2[0], x3[0])))∧(x3[11] + 1 →* x4[0])∧(x1[11] →* x0[0])∧(x5[11] →* x5[0]))
(11) -> (1), if ((java.lang.Object(ARRAY(x1[11], x2[11])) →* java.lang.Object(ARRAY(x3[1], x4[1])))∧(x3[11] + 1 →* x5[1])∧(x1[11] →* x0[1])∧(x5[11] →* 0))
(11) -> (17), if ((java.lang.Object(ARRAY(x1[11], x2[11])) →* java.lang.Object(ARRAY(x2[17], x3[17])))∧(x3[11] + 1 →* x4[17])∧(x1[11] →* x0[17])∧(x5[11] →* 1))
(12) -> (13), if ((x4[12] >= 0 && x2[12] > x4[12] + 1 && 0 <= x4[12] + 1 →* TRUE)∧(java.lang.Object(ARRAY(x2[12], x3[12])) →* java.lang.Object(ARRAY(x2[13], x3[13])))∧(x4[12] →* x4[13]))
(13) -> (0), if ((java.lang.Object(ARRAY(x2[13], x3[13])) →* java.lang.Object(ARRAY(x2[0], x3[0])))∧(x4[13] + 1 →* x4[0])∧(x2[13] →* x0[0])∧(x6[13] →* x5[0]))
(13) -> (1), if ((java.lang.Object(ARRAY(x2[13], x3[13])) →* java.lang.Object(ARRAY(x3[1], x4[1])))∧(x4[13] + 1 →* x5[1])∧(x2[13] →* x0[1])∧(x6[13] →* 0))
(13) -> (17), if ((java.lang.Object(ARRAY(x2[13], x3[13])) →* java.lang.Object(ARRAY(x2[17], x3[17])))∧(x4[13] + 1 →* x4[17])∧(x2[13] →* x0[17])∧(x6[13] →* 1))
(14) -> (8), if ((java.lang.Object(ARRAY(x0[14], x3[14])) →* java.lang.Object(ARRAY(x1[8], x2[8])))∧(x4[14] →* x3[8])∧(x0[14] →* x4[8]))
(14) -> (10), if ((java.lang.Object(ARRAY(x0[14], x3[14])) →* java.lang.Object(ARRAY(x1[10], x2[10])))∧(x4[14] →* x3[10])∧(x0[14] →* 0))
(14) -> (12), if ((java.lang.Object(ARRAY(x0[14], x3[14])) →* java.lang.Object(ARRAY(x2[12], x3[12])))∧(x4[14] →* x4[12])∧(x0[14] →* 1))
(15) -> (16), if ((x4[15] >= 0 && x4[15] < x2[15] →* TRUE)∧(java.lang.Object(ARRAY(x2[15], x3[15])) →* java.lang.Object(ARRAY(x2[16], x3[16])))∧(x4[15] →* x4[16]))
(16) -> (6), if ((java.lang.Object(ARRAY(x2[16], x3[16])) →* java.lang.Object(ARRAY(x2[6], x3[6])))∧(x4[16] →* x4[6])∧(x2[16] →* x0[6])∧(x6[16] →* x5[6]))
(16) -> (7), if ((java.lang.Object(ARRAY(x2[16], x3[16])) →* java.lang.Object(ARRAY(x3[7], x4[7])))∧(x4[16] →* x5[7])∧(x2[16] →* x0[7])∧(x6[16] →* 0))
(16) -> (14), if ((java.lang.Object(ARRAY(x2[16], x3[16])) →* java.lang.Object(ARRAY(x2[14], x3[14])))∧(x4[16] →* x4[14])∧(x2[16] →* x0[14])∧(x6[16] →* 1))
(17) -> (2), if ((java.lang.Object(ARRAY(x0[17], x3[17])) →* java.lang.Object(ARRAY(x1[2], x2[2])))∧(x4[17] →* x3[2])∧(x0[17] →* x4[2]))
(17) -> (4), if ((java.lang.Object(ARRAY(x0[17], x3[17])) →* java.lang.Object(ARRAY(x2[4], x3[4])))∧(x4[17] →* x4[4])∧(x0[17] →* 0))
(17) -> (15), if ((java.lang.Object(ARRAY(x0[17], x3[17])) →* java.lang.Object(ARRAY(x2[15], x3[15])))∧(x4[17] →* x4[15])∧(x0[17] →* 1))
(1) (&&(&&(>=(x3[8], 0), >(x1[8], +(x3[8], 1))), <=(0, +(x3[8], 1)))=TRUE∧java.lang.Object(ARRAY(x1[8], x2[8]))=java.lang.Object(ARRAY(x1[9], x2[9]))∧x3[8]=x3[9]∧x4[8]=x4[9]∧java.lang.Object(ARRAY(x1[9], x2[9]))=java.lang.Object(ARRAY(x2[0], x3[0]))∧+(x3[9], 1)=x4[0]∧x1[9]=x0[0]∧x5[9]=x5[0] ⇒ 2387_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x2[0], x3[0])), x4[0], x0[0], x5[0])≥NonInfC∧2387_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x2[0], x3[0])), x4[0], x0[0], x5[0])≥2420_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x0[0], x3[0])), x4[0], x1[0])∧(UIncreasing(2420_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x0[0], x3[0])), x4[0], x1[0])), ≥))
(2) (<=(0, +(x3[8], 1))=TRUE∧>=(x3[8], 0)=TRUE∧>(x1[8], +(x3[8], 1))=TRUE ⇒ 2387_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x1[8], x2[8])), +(x3[8], 1), x1[8], x5[9])≥NonInfC∧2387_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x1[8], x2[8])), +(x3[8], 1), x1[8], x5[9])≥2420_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x1[8], x2[8])), +(x3[8], 1), x1[0])∧(UIncreasing(2420_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x0[0], x3[0])), x4[0], x1[0])), ≥))
(3) (x3[8] + [1] ≥ 0∧x3[8] ≥ 0∧x1[8] + [-2] + [-1]x3[8] ≥ 0 ⇒ (UIncreasing(2420_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x0[0], x3[0])), x4[0], x1[0])), ≥)∧[(-1)Bound*bni_101] + [bni_101]x1[8] + [(-1)bni_101]x3[8] ≥ 0∧[1 + (-1)bso_102] ≥ 0)
(4) (x3[8] + [1] ≥ 0∧x3[8] ≥ 0∧x1[8] + [-2] + [-1]x3[8] ≥ 0 ⇒ (UIncreasing(2420_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x0[0], x3[0])), x4[0], x1[0])), ≥)∧[(-1)Bound*bni_101] + [bni_101]x1[8] + [(-1)bni_101]x3[8] ≥ 0∧[1 + (-1)bso_102] ≥ 0)
(5) (x3[8] + [1] ≥ 0∧x3[8] ≥ 0∧x1[8] + [-2] + [-1]x3[8] ≥ 0 ⇒ (UIncreasing(2420_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x0[0], x3[0])), x4[0], x1[0])), ≥)∧[(-1)Bound*bni_101] + [bni_101]x1[8] + [(-1)bni_101]x3[8] ≥ 0∧[1 + (-1)bso_102] ≥ 0)
(6) (x3[8] + [1] ≥ 0∧x3[8] ≥ 0∧x1[8] + [-2] + [-1]x3[8] ≥ 0 ⇒ (UIncreasing(2420_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x0[0], x3[0])), x4[0], x1[0])), ≥)∧0 = 0∧[(-1)Bound*bni_101] + [bni_101]x1[8] + [(-1)bni_101]x3[8] ≥ 0∧0 = 0∧0 = 0∧[1 + (-1)bso_102] ≥ 0)
(7) (x3[8] + [1] ≥ 0∧x3[8] ≥ 0∧x1[8] ≥ 0 ⇒ (UIncreasing(2420_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x0[0], x3[0])), x4[0], x1[0])), ≥)∧0 = 0∧[(-1)Bound*bni_101 + (2)bni_101] + [bni_101]x1[8] ≥ 0∧0 = 0∧0 = 0∧[1 + (-1)bso_102] ≥ 0)
(8) (&&(&&(>=(x3[10], 0), >(x1[10], +(x3[10], 1))), <=(0, +(x3[10], 1)))=TRUE∧java.lang.Object(ARRAY(x1[10], x2[10]))=java.lang.Object(ARRAY(x1[11], x2[11]))∧x3[10]=x3[11]∧java.lang.Object(ARRAY(x1[11], x2[11]))=java.lang.Object(ARRAY(x2[0], x3[0]))∧+(x3[11], 1)=x4[0]∧x1[11]=x0[0]∧x5[11]=x5[0] ⇒ 2387_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x2[0], x3[0])), x4[0], x0[0], x5[0])≥NonInfC∧2387_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x2[0], x3[0])), x4[0], x0[0], x5[0])≥2420_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x0[0], x3[0])), x4[0], x1[0])∧(UIncreasing(2420_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x0[0], x3[0])), x4[0], x1[0])), ≥))
(9) (<=(0, +(x3[10], 1))=TRUE∧>=(x3[10], 0)=TRUE∧>(x1[10], +(x3[10], 1))=TRUE ⇒ 2387_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x1[10], x2[10])), +(x3[10], 1), x1[10], x5[11])≥NonInfC∧2387_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x1[10], x2[10])), +(x3[10], 1), x1[10], x5[11])≥2420_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x1[10], x2[10])), +(x3[10], 1), x1[0])∧(UIncreasing(2420_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x0[0], x3[0])), x4[0], x1[0])), ≥))
(10) (x3[10] + [1] ≥ 0∧x3[10] ≥ 0∧x1[10] + [-2] + [-1]x3[10] ≥ 0 ⇒ (UIncreasing(2420_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x0[0], x3[0])), x4[0], x1[0])), ≥)∧[(-1)Bound*bni_101] + [bni_101]x1[10] + [(-1)bni_101]x3[10] ≥ 0∧[1 + (-1)bso_102] ≥ 0)
(11) (x3[10] + [1] ≥ 0∧x3[10] ≥ 0∧x1[10] + [-2] + [-1]x3[10] ≥ 0 ⇒ (UIncreasing(2420_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x0[0], x3[0])), x4[0], x1[0])), ≥)∧[(-1)Bound*bni_101] + [bni_101]x1[10] + [(-1)bni_101]x3[10] ≥ 0∧[1 + (-1)bso_102] ≥ 0)
(12) (x3[10] + [1] ≥ 0∧x3[10] ≥ 0∧x1[10] + [-2] + [-1]x3[10] ≥ 0 ⇒ (UIncreasing(2420_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x0[0], x3[0])), x4[0], x1[0])), ≥)∧[(-1)Bound*bni_101] + [bni_101]x1[10] + [(-1)bni_101]x3[10] ≥ 0∧[1 + (-1)bso_102] ≥ 0)
(13) (x3[10] + [1] ≥ 0∧x3[10] ≥ 0∧x1[10] + [-2] + [-1]x3[10] ≥ 0 ⇒ (UIncreasing(2420_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x0[0], x3[0])), x4[0], x1[0])), ≥)∧0 = 0∧[(-1)Bound*bni_101] + [bni_101]x1[10] + [(-1)bni_101]x3[10] ≥ 0∧0 = 0∧0 = 0∧[1 + (-1)bso_102] ≥ 0)
(14) (x3[10] + [1] ≥ 0∧x3[10] ≥ 0∧x1[10] ≥ 0 ⇒ (UIncreasing(2420_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x0[0], x3[0])), x4[0], x1[0])), ≥)∧0 = 0∧[(-1)Bound*bni_101 + (2)bni_101] + [bni_101]x1[10] ≥ 0∧0 = 0∧0 = 0∧[1 + (-1)bso_102] ≥ 0)
(15) (&&(&&(>=(x4[12], 0), >(x2[12], +(x4[12], 1))), <=(0, +(x4[12], 1)))=TRUE∧java.lang.Object(ARRAY(x2[12], x3[12]))=java.lang.Object(ARRAY(x2[13], x3[13]))∧x4[12]=x4[13]∧java.lang.Object(ARRAY(x2[13], x3[13]))=java.lang.Object(ARRAY(x2[0], x3[0]))∧+(x4[13], 1)=x4[0]∧x2[13]=x0[0]∧x6[13]=x5[0] ⇒ 2387_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x2[0], x3[0])), x4[0], x0[0], x5[0])≥NonInfC∧2387_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x2[0], x3[0])), x4[0], x0[0], x5[0])≥2420_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x0[0], x3[0])), x4[0], x1[0])∧(UIncreasing(2420_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x0[0], x3[0])), x4[0], x1[0])), ≥))
(16) (<=(0, +(x4[12], 1))=TRUE∧>=(x4[12], 0)=TRUE∧>(x2[12], +(x4[12], 1))=TRUE ⇒ 2387_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x2[12], x3[12])), +(x4[12], 1), x2[12], x6[13])≥NonInfC∧2387_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x2[12], x3[12])), +(x4[12], 1), x2[12], x6[13])≥2420_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x2[12], x3[12])), +(x4[12], 1), x1[0])∧(UIncreasing(2420_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x0[0], x3[0])), x4[0], x1[0])), ≥))
(17) (x4[12] + [1] ≥ 0∧x4[12] ≥ 0∧x2[12] + [-2] + [-1]x4[12] ≥ 0 ⇒ (UIncreasing(2420_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x0[0], x3[0])), x4[0], x1[0])), ≥)∧[(-1)Bound*bni_101] + [bni_101]x2[12] + [(-1)bni_101]x4[12] ≥ 0∧[1 + (-1)bso_102] ≥ 0)
(18) (x4[12] + [1] ≥ 0∧x4[12] ≥ 0∧x2[12] + [-2] + [-1]x4[12] ≥ 0 ⇒ (UIncreasing(2420_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x0[0], x3[0])), x4[0], x1[0])), ≥)∧[(-1)Bound*bni_101] + [bni_101]x2[12] + [(-1)bni_101]x4[12] ≥ 0∧[1 + (-1)bso_102] ≥ 0)
(19) (x4[12] + [1] ≥ 0∧x4[12] ≥ 0∧x2[12] + [-2] + [-1]x4[12] ≥ 0 ⇒ (UIncreasing(2420_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x0[0], x3[0])), x4[0], x1[0])), ≥)∧[(-1)Bound*bni_101] + [bni_101]x2[12] + [(-1)bni_101]x4[12] ≥ 0∧[1 + (-1)bso_102] ≥ 0)
(20) (x4[12] + [1] ≥ 0∧x4[12] ≥ 0∧x2[12] + [-2] + [-1]x4[12] ≥ 0 ⇒ (UIncreasing(2420_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x0[0], x3[0])), x4[0], x1[0])), ≥)∧0 = 0∧[(-1)Bound*bni_101] + [bni_101]x2[12] + [(-1)bni_101]x4[12] ≥ 0∧0 = 0∧0 = 0∧[1 + (-1)bso_102] ≥ 0)
(21) (x4[12] + [1] ≥ 0∧x4[12] ≥ 0∧x2[12] ≥ 0 ⇒ (UIncreasing(2420_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x0[0], x3[0])), x4[0], x1[0])), ≥)∧0 = 0∧[(-1)Bound*bni_101 + (2)bni_101] + [bni_101]x2[12] ≥ 0∧0 = 0∧0 = 0∧[1 + (-1)bso_102] ≥ 0)
(22) (&&(&&(>=(x3[8], 0), >(x1[8], +(x3[8], 1))), <=(0, +(x3[8], 1)))=TRUE∧java.lang.Object(ARRAY(x1[8], x2[8]))=java.lang.Object(ARRAY(x1[9], x2[9]))∧x3[8]=x3[9]∧x4[8]=x4[9]∧java.lang.Object(ARRAY(x1[9], x2[9]))=java.lang.Object(ARRAY(x3[1], x4[1]))∧+(x3[9], 1)=x5[1]∧x1[9]=x0[1]∧x5[9]=0 ⇒ 2387_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x3[1], x4[1])), x5[1], x0[1], 0)≥NonInfC∧2387_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x3[1], x4[1])), x5[1], x0[1], 0)≥2420_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x0[1], x4[1])), x5[1], 1)∧(UIncreasing(2420_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x0[1], x4[1])), x5[1], 1)), ≥))
(23) (<=(0, +(x3[8], 1))=TRUE∧>=(x3[8], 0)=TRUE∧>(x1[8], +(x3[8], 1))=TRUE ⇒ 2387_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x1[8], x2[8])), +(x3[8], 1), x1[8], 0)≥NonInfC∧2387_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x1[8], x2[8])), +(x3[8], 1), x1[8], 0)≥2420_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x1[8], x2[8])), +(x3[8], 1), 1)∧(UIncreasing(2420_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x0[1], x4[1])), x5[1], 1)), ≥))
(24) (x3[8] + [1] ≥ 0∧x3[8] ≥ 0∧x1[8] + [-2] + [-1]x3[8] ≥ 0 ⇒ (UIncreasing(2420_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x0[1], x4[1])), x5[1], 1)), ≥)∧[(-1)Bound*bni_103] + [bni_103]x1[8] + [(-1)bni_103]x3[8] ≥ 0∧[1 + (-1)bso_104] ≥ 0)
(25) (x3[8] + [1] ≥ 0∧x3[8] ≥ 0∧x1[8] + [-2] + [-1]x3[8] ≥ 0 ⇒ (UIncreasing(2420_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x0[1], x4[1])), x5[1], 1)), ≥)∧[(-1)Bound*bni_103] + [bni_103]x1[8] + [(-1)bni_103]x3[8] ≥ 0∧[1 + (-1)bso_104] ≥ 0)
(26) (x3[8] + [1] ≥ 0∧x3[8] ≥ 0∧x1[8] + [-2] + [-1]x3[8] ≥ 0 ⇒ (UIncreasing(2420_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x0[1], x4[1])), x5[1], 1)), ≥)∧[(-1)Bound*bni_103] + [bni_103]x1[8] + [(-1)bni_103]x3[8] ≥ 0∧[1 + (-1)bso_104] ≥ 0)
(27) (x3[8] + [1] ≥ 0∧x3[8] ≥ 0∧x1[8] + [-2] + [-1]x3[8] ≥ 0 ⇒ (UIncreasing(2420_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x0[1], x4[1])), x5[1], 1)), ≥)∧0 = 0∧[(-1)Bound*bni_103] + [bni_103]x1[8] + [(-1)bni_103]x3[8] ≥ 0∧0 = 0∧[1 + (-1)bso_104] ≥ 0)
(28) (x3[8] + [1] ≥ 0∧x3[8] ≥ 0∧x1[8] ≥ 0 ⇒ (UIncreasing(2420_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x0[1], x4[1])), x5[1], 1)), ≥)∧0 = 0∧[(-1)Bound*bni_103 + (2)bni_103] + [bni_103]x1[8] ≥ 0∧0 = 0∧[1 + (-1)bso_104] ≥ 0)
(29) (&&(&&(>=(x3[10], 0), >(x1[10], +(x3[10], 1))), <=(0, +(x3[10], 1)))=TRUE∧java.lang.Object(ARRAY(x1[10], x2[10]))=java.lang.Object(ARRAY(x1[11], x2[11]))∧x3[10]=x3[11]∧java.lang.Object(ARRAY(x1[11], x2[11]))=java.lang.Object(ARRAY(x3[1], x4[1]))∧+(x3[11], 1)=x5[1]∧x1[11]=x0[1]∧x5[11]=0 ⇒ 2387_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x3[1], x4[1])), x5[1], x0[1], 0)≥NonInfC∧2387_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x3[1], x4[1])), x5[1], x0[1], 0)≥2420_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x0[1], x4[1])), x5[1], 1)∧(UIncreasing(2420_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x0[1], x4[1])), x5[1], 1)), ≥))
(30) (<=(0, +(x3[10], 1))=TRUE∧>=(x3[10], 0)=TRUE∧>(x1[10], +(x3[10], 1))=TRUE ⇒ 2387_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x1[10], x2[10])), +(x3[10], 1), x1[10], 0)≥NonInfC∧2387_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x1[10], x2[10])), +(x3[10], 1), x1[10], 0)≥2420_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x1[10], x2[10])), +(x3[10], 1), 1)∧(UIncreasing(2420_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x0[1], x4[1])), x5[1], 1)), ≥))
(31) (x3[10] + [1] ≥ 0∧x3[10] ≥ 0∧x1[10] + [-2] + [-1]x3[10] ≥ 0 ⇒ (UIncreasing(2420_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x0[1], x4[1])), x5[1], 1)), ≥)∧[(-1)Bound*bni_103] + [bni_103]x1[10] + [(-1)bni_103]x3[10] ≥ 0∧[1 + (-1)bso_104] ≥ 0)
(32) (x3[10] + [1] ≥ 0∧x3[10] ≥ 0∧x1[10] + [-2] + [-1]x3[10] ≥ 0 ⇒ (UIncreasing(2420_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x0[1], x4[1])), x5[1], 1)), ≥)∧[(-1)Bound*bni_103] + [bni_103]x1[10] + [(-1)bni_103]x3[10] ≥ 0∧[1 + (-1)bso_104] ≥ 0)
(33) (x3[10] + [1] ≥ 0∧x3[10] ≥ 0∧x1[10] + [-2] + [-1]x3[10] ≥ 0 ⇒ (UIncreasing(2420_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x0[1], x4[1])), x5[1], 1)), ≥)∧[(-1)Bound*bni_103] + [bni_103]x1[10] + [(-1)bni_103]x3[10] ≥ 0∧[1 + (-1)bso_104] ≥ 0)
(34) (x3[10] + [1] ≥ 0∧x3[10] ≥ 0∧x1[10] + [-2] + [-1]x3[10] ≥ 0 ⇒ (UIncreasing(2420_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x0[1], x4[1])), x5[1], 1)), ≥)∧0 = 0∧[(-1)Bound*bni_103] + [bni_103]x1[10] + [(-1)bni_103]x3[10] ≥ 0∧0 = 0∧[1 + (-1)bso_104] ≥ 0)
(35) (x3[10] + [1] ≥ 0∧x3[10] ≥ 0∧x1[10] ≥ 0 ⇒ (UIncreasing(2420_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x0[1], x4[1])), x5[1], 1)), ≥)∧0 = 0∧[(-1)Bound*bni_103 + (2)bni_103] + [bni_103]x1[10] ≥ 0∧0 = 0∧[1 + (-1)bso_104] ≥ 0)
(36) (&&(&&(>=(x4[12], 0), >(x2[12], +(x4[12], 1))), <=(0, +(x4[12], 1)))=TRUE∧java.lang.Object(ARRAY(x2[12], x3[12]))=java.lang.Object(ARRAY(x2[13], x3[13]))∧x4[12]=x4[13]∧java.lang.Object(ARRAY(x2[13], x3[13]))=java.lang.Object(ARRAY(x3[1], x4[1]))∧+(x4[13], 1)=x5[1]∧x2[13]=x0[1]∧x6[13]=0 ⇒ 2387_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x3[1], x4[1])), x5[1], x0[1], 0)≥NonInfC∧2387_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x3[1], x4[1])), x5[1], x0[1], 0)≥2420_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x0[1], x4[1])), x5[1], 1)∧(UIncreasing(2420_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x0[1], x4[1])), x5[1], 1)), ≥))
(37) (<=(0, +(x4[12], 1))=TRUE∧>=(x4[12], 0)=TRUE∧>(x2[12], +(x4[12], 1))=TRUE ⇒ 2387_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x2[12], x3[12])), +(x4[12], 1), x2[12], 0)≥NonInfC∧2387_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x2[12], x3[12])), +(x4[12], 1), x2[12], 0)≥2420_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x2[12], x3[12])), +(x4[12], 1), 1)∧(UIncreasing(2420_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x0[1], x4[1])), x5[1], 1)), ≥))
(38) (x4[12] + [1] ≥ 0∧x4[12] ≥ 0∧x2[12] + [-2] + [-1]x4[12] ≥ 0 ⇒ (UIncreasing(2420_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x0[1], x4[1])), x5[1], 1)), ≥)∧[(-1)Bound*bni_103] + [bni_103]x2[12] + [(-1)bni_103]x4[12] ≥ 0∧[1 + (-1)bso_104] ≥ 0)
(39) (x4[12] + [1] ≥ 0∧x4[12] ≥ 0∧x2[12] + [-2] + [-1]x4[12] ≥ 0 ⇒ (UIncreasing(2420_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x0[1], x4[1])), x5[1], 1)), ≥)∧[(-1)Bound*bni_103] + [bni_103]x2[12] + [(-1)bni_103]x4[12] ≥ 0∧[1 + (-1)bso_104] ≥ 0)
(40) (x4[12] + [1] ≥ 0∧x4[12] ≥ 0∧x2[12] + [-2] + [-1]x4[12] ≥ 0 ⇒ (UIncreasing(2420_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x0[1], x4[1])), x5[1], 1)), ≥)∧[(-1)Bound*bni_103] + [bni_103]x2[12] + [(-1)bni_103]x4[12] ≥ 0∧[1 + (-1)bso_104] ≥ 0)
(41) (x4[12] + [1] ≥ 0∧x4[12] ≥ 0∧x2[12] + [-2] + [-1]x4[12] ≥ 0 ⇒ (UIncreasing(2420_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x0[1], x4[1])), x5[1], 1)), ≥)∧0 = 0∧[(-1)Bound*bni_103] + [bni_103]x2[12] + [(-1)bni_103]x4[12] ≥ 0∧0 = 0∧[1 + (-1)bso_104] ≥ 0)
(42) (x4[12] + [1] ≥ 0∧x4[12] ≥ 0∧x2[12] ≥ 0 ⇒ (UIncreasing(2420_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x0[1], x4[1])), x5[1], 1)), ≥)∧0 = 0∧[(-1)Bound*bni_103 + (2)bni_103] + [bni_103]x2[12] ≥ 0∧0 = 0∧[1 + (-1)bso_104] ≥ 0)
(43) (&&(>=(x3[2], 0), <(x3[2], x1[2]))=TRUE∧java.lang.Object(ARRAY(x1[2], x2[2]))=java.lang.Object(ARRAY(x1[3], x2[3]))∧x3[2]=x3[3]∧x4[2]=x4[3] ⇒ 2420_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x1[2], x2[2])), x3[2], x4[2])≥NonInfC∧2420_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x1[2], x2[2])), x3[2], x4[2])≥COND_2420_1_MAIN_INVOKEMETHOD(&&(>=(x3[2], 0), <(x3[2], x1[2])), java.lang.Object(ARRAY(x1[2], x2[2])), x3[2], x4[2])∧(UIncreasing(COND_2420_1_MAIN_INVOKEMETHOD(&&(>=(x3[2], 0), <(x3[2], x1[2])), java.lang.Object(ARRAY(x1[2], x2[2])), x3[2], x4[2])), ≥))
(44) (>=(x3[2], 0)=TRUE∧<(x3[2], x1[2])=TRUE ⇒ 2420_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x1[2], x2[2])), x3[2], x4[2])≥NonInfC∧2420_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x1[2], x2[2])), x3[2], x4[2])≥COND_2420_1_MAIN_INVOKEMETHOD(&&(>=(x3[2], 0), <(x3[2], x1[2])), java.lang.Object(ARRAY(x1[2], x2[2])), x3[2], x4[2])∧(UIncreasing(COND_2420_1_MAIN_INVOKEMETHOD(&&(>=(x3[2], 0), <(x3[2], x1[2])), java.lang.Object(ARRAY(x1[2], x2[2])), x3[2], x4[2])), ≥))
(45) (x3[2] ≥ 0∧x1[2] + [-1] + [-1]x3[2] ≥ 0 ⇒ (UIncreasing(COND_2420_1_MAIN_INVOKEMETHOD(&&(>=(x3[2], 0), <(x3[2], x1[2])), java.lang.Object(ARRAY(x1[2], x2[2])), x3[2], x4[2])), ≥)∧[(-1)Bound*bni_105] + [bni_105]x1[2] + [(-1)bni_105]x3[2] ≥ 0∧[(-1)bso_106] ≥ 0)
(46) (x3[2] ≥ 0∧x1[2] + [-1] + [-1]x3[2] ≥ 0 ⇒ (UIncreasing(COND_2420_1_MAIN_INVOKEMETHOD(&&(>=(x3[2], 0), <(x3[2], x1[2])), java.lang.Object(ARRAY(x1[2], x2[2])), x3[2], x4[2])), ≥)∧[(-1)Bound*bni_105] + [bni_105]x1[2] + [(-1)bni_105]x3[2] ≥ 0∧[(-1)bso_106] ≥ 0)
(47) (x3[2] ≥ 0∧x1[2] + [-1] + [-1]x3[2] ≥ 0 ⇒ (UIncreasing(COND_2420_1_MAIN_INVOKEMETHOD(&&(>=(x3[2], 0), <(x3[2], x1[2])), java.lang.Object(ARRAY(x1[2], x2[2])), x3[2], x4[2])), ≥)∧[(-1)Bound*bni_105] + [bni_105]x1[2] + [(-1)bni_105]x3[2] ≥ 0∧[(-1)bso_106] ≥ 0)
(48) (x3[2] ≥ 0∧x1[2] + [-1] + [-1]x3[2] ≥ 0 ⇒ (UIncreasing(COND_2420_1_MAIN_INVOKEMETHOD(&&(>=(x3[2], 0), <(x3[2], x1[2])), java.lang.Object(ARRAY(x1[2], x2[2])), x3[2], x4[2])), ≥)∧0 = 0∧0 = 0∧[(-1)Bound*bni_105] + [bni_105]x1[2] + [(-1)bni_105]x3[2] ≥ 0∧0 = 0∧0 = 0∧[(-1)bso_106] ≥ 0)
(49) (x3[2] ≥ 0∧x1[2] ≥ 0 ⇒ (UIncreasing(COND_2420_1_MAIN_INVOKEMETHOD(&&(>=(x3[2], 0), <(x3[2], x1[2])), java.lang.Object(ARRAY(x1[2], x2[2])), x3[2], x4[2])), ≥)∧0 = 0∧0 = 0∧[(-1)Bound*bni_105 + bni_105] + [bni_105]x1[2] ≥ 0∧0 = 0∧0 = 0∧[(-1)bso_106] ≥ 0)
(50) (java.lang.Object(ARRAY(x0[0], x3[0]))=java.lang.Object(ARRAY(x1[2], x2[2]))∧x4[0]=x3[2]∧x1[0]=x4[2]∧&&(>=(x3[2], 0), <(x3[2], x1[2]))=TRUE∧java.lang.Object(ARRAY(x1[2], x2[2]))=java.lang.Object(ARRAY(x1[3], x2[3]))∧x3[2]=x3[3]∧x4[2]=x4[3] ⇒ COND_2420_1_MAIN_INVOKEMETHOD(TRUE, java.lang.Object(ARRAY(x1[3], x2[3])), x3[3], x4[3])≥NonInfC∧COND_2420_1_MAIN_INVOKEMETHOD(TRUE, java.lang.Object(ARRAY(x1[3], x2[3])), x3[3], x4[3])≥2595_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x1[3], x2[3])), x3[3], x1[3], x5[3])∧(UIncreasing(2595_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x1[3], x2[3])), x3[3], x1[3], x5[3])), ≥))
(51) (>=(x3[2], 0)=TRUE∧<(x3[2], x1[2])=TRUE ⇒ COND_2420_1_MAIN_INVOKEMETHOD(TRUE, java.lang.Object(ARRAY(x1[2], x3[0])), x3[2], x1[0])≥NonInfC∧COND_2420_1_MAIN_INVOKEMETHOD(TRUE, java.lang.Object(ARRAY(x1[2], x3[0])), x3[2], x1[0])≥2595_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x1[2], x3[0])), x3[2], x1[2], x5[3])∧(UIncreasing(2595_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x1[3], x2[3])), x3[3], x1[3], x5[3])), ≥))
(52) (x3[2] ≥ 0∧x1[2] + [-1] + [-1]x3[2] ≥ 0 ⇒ (UIncreasing(2595_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x1[3], x2[3])), x3[3], x1[3], x5[3])), ≥)∧[(-1)Bound*bni_107] + [(-1)bni_107]x3[2] + [bni_107]x1[2] ≥ 0∧[(-1)bso_108] ≥ 0)
(53) (x3[2] ≥ 0∧x1[2] + [-1] + [-1]x3[2] ≥ 0 ⇒ (UIncreasing(2595_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x1[3], x2[3])), x3[3], x1[3], x5[3])), ≥)∧[(-1)Bound*bni_107] + [(-1)bni_107]x3[2] + [bni_107]x1[2] ≥ 0∧[(-1)bso_108] ≥ 0)
(54) (x3[2] ≥ 0∧x1[2] + [-1] + [-1]x3[2] ≥ 0 ⇒ (UIncreasing(2595_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x1[3], x2[3])), x3[3], x1[3], x5[3])), ≥)∧[(-1)Bound*bni_107] + [(-1)bni_107]x3[2] + [bni_107]x1[2] ≥ 0∧[(-1)bso_108] ≥ 0)
(55) (x3[2] ≥ 0∧x1[2] + [-1] + [-1]x3[2] ≥ 0 ⇒ (UIncreasing(2595_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x1[3], x2[3])), x3[3], x1[3], x5[3])), ≥)∧0 = 0∧0 = 0∧[(-1)Bound*bni_107] + [(-1)bni_107]x3[2] + [bni_107]x1[2] ≥ 0∧0 = 0∧0 = 0∧[(-1)bso_108] ≥ 0)
(56) (x3[2] ≥ 0∧x1[2] ≥ 0 ⇒ (UIncreasing(2595_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x1[3], x2[3])), x3[3], x1[3], x5[3])), ≥)∧0 = 0∧0 = 0∧[(-1)Bound*bni_107 + bni_107] + [bni_107]x1[2] ≥ 0∧0 = 0∧0 = 0∧[(-1)bso_108] ≥ 0)
(57) (java.lang.Object(ARRAY(x0[1], x4[1]))=java.lang.Object(ARRAY(x1[2], x2[2]))∧x5[1]=x3[2]∧1=x4[2]∧&&(>=(x3[2], 0), <(x3[2], x1[2]))=TRUE∧java.lang.Object(ARRAY(x1[2], x2[2]))=java.lang.Object(ARRAY(x1[3], x2[3]))∧x3[2]=x3[3]∧x4[2]=x4[3] ⇒ COND_2420_1_MAIN_INVOKEMETHOD(TRUE, java.lang.Object(ARRAY(x1[3], x2[3])), x3[3], x4[3])≥NonInfC∧COND_2420_1_MAIN_INVOKEMETHOD(TRUE, java.lang.Object(ARRAY(x1[3], x2[3])), x3[3], x4[3])≥2595_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x1[3], x2[3])), x3[3], x1[3], x5[3])∧(UIncreasing(2595_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x1[3], x2[3])), x3[3], x1[3], x5[3])), ≥))
(58) (>=(x3[2], 0)=TRUE∧<(x3[2], x1[2])=TRUE ⇒ COND_2420_1_MAIN_INVOKEMETHOD(TRUE, java.lang.Object(ARRAY(x1[2], x4[1])), x3[2], 1)≥NonInfC∧COND_2420_1_MAIN_INVOKEMETHOD(TRUE, java.lang.Object(ARRAY(x1[2], x4[1])), x3[2], 1)≥2595_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x1[2], x4[1])), x3[2], x1[2], x5[3])∧(UIncreasing(2595_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x1[3], x2[3])), x3[3], x1[3], x5[3])), ≥))
(59) (x3[2] ≥ 0∧x1[2] + [-1] + [-1]x3[2] ≥ 0 ⇒ (UIncreasing(2595_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x1[3], x2[3])), x3[3], x1[3], x5[3])), ≥)∧[(-1)Bound*bni_107] + [(-1)bni_107]x3[2] + [bni_107]x1[2] ≥ 0∧[(-1)bso_108] ≥ 0)
(60) (x3[2] ≥ 0∧x1[2] + [-1] + [-1]x3[2] ≥ 0 ⇒ (UIncreasing(2595_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x1[3], x2[3])), x3[3], x1[3], x5[3])), ≥)∧[(-1)Bound*bni_107] + [(-1)bni_107]x3[2] + [bni_107]x1[2] ≥ 0∧[(-1)bso_108] ≥ 0)
(61) (x3[2] ≥ 0∧x1[2] + [-1] + [-1]x3[2] ≥ 0 ⇒ (UIncreasing(2595_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x1[3], x2[3])), x3[3], x1[3], x5[3])), ≥)∧[(-1)Bound*bni_107] + [(-1)bni_107]x3[2] + [bni_107]x1[2] ≥ 0∧[(-1)bso_108] ≥ 0)
(62) (x3[2] ≥ 0∧x1[2] + [-1] + [-1]x3[2] ≥ 0 ⇒ (UIncreasing(2595_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x1[3], x2[3])), x3[3], x1[3], x5[3])), ≥)∧0 = 0∧[(-1)Bound*bni_107] + [(-1)bni_107]x3[2] + [bni_107]x1[2] ≥ 0∧0 = 0∧[(-1)bso_108] ≥ 0)
(63) (x3[2] ≥ 0∧x1[2] ≥ 0 ⇒ (UIncreasing(2595_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x1[3], x2[3])), x3[3], x1[3], x5[3])), ≥)∧0 = 0∧[(-1)Bound*bni_107 + bni_107] + [bni_107]x1[2] ≥ 0∧0 = 0∧[(-1)bso_108] ≥ 0)
(64) (java.lang.Object(ARRAY(x0[17], x3[17]))=java.lang.Object(ARRAY(x1[2], x2[2]))∧x4[17]=x3[2]∧x0[17]=x4[2]∧&&(>=(x3[2], 0), <(x3[2], x1[2]))=TRUE∧java.lang.Object(ARRAY(x1[2], x2[2]))=java.lang.Object(ARRAY(x1[3], x2[3]))∧x3[2]=x3[3]∧x4[2]=x4[3] ⇒ COND_2420_1_MAIN_INVOKEMETHOD(TRUE, java.lang.Object(ARRAY(x1[3], x2[3])), x3[3], x4[3])≥NonInfC∧COND_2420_1_MAIN_INVOKEMETHOD(TRUE, java.lang.Object(ARRAY(x1[3], x2[3])), x3[3], x4[3])≥2595_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x1[3], x2[3])), x3[3], x1[3], x5[3])∧(UIncreasing(2595_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x1[3], x2[3])), x3[3], x1[3], x5[3])), ≥))
(65) (>=(x3[2], 0)=TRUE∧<(x3[2], x1[2])=TRUE ⇒ COND_2420_1_MAIN_INVOKEMETHOD(TRUE, java.lang.Object(ARRAY(x1[2], x3[17])), x3[2], x1[2])≥NonInfC∧COND_2420_1_MAIN_INVOKEMETHOD(TRUE, java.lang.Object(ARRAY(x1[2], x3[17])), x3[2], x1[2])≥2595_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x1[2], x3[17])), x3[2], x1[2], x5[3])∧(UIncreasing(2595_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x1[3], x2[3])), x3[3], x1[3], x5[3])), ≥))
(66) (x3[2] ≥ 0∧x1[2] + [-1] + [-1]x3[2] ≥ 0 ⇒ (UIncreasing(2595_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x1[3], x2[3])), x3[3], x1[3], x5[3])), ≥)∧[(-1)Bound*bni_107] + [(-1)bni_107]x3[2] + [bni_107]x1[2] ≥ 0∧[(-1)bso_108] ≥ 0)
(67) (x3[2] ≥ 0∧x1[2] + [-1] + [-1]x3[2] ≥ 0 ⇒ (UIncreasing(2595_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x1[3], x2[3])), x3[3], x1[3], x5[3])), ≥)∧[(-1)Bound*bni_107] + [(-1)bni_107]x3[2] + [bni_107]x1[2] ≥ 0∧[(-1)bso_108] ≥ 0)
(68) (x3[2] ≥ 0∧x1[2] + [-1] + [-1]x3[2] ≥ 0 ⇒ (UIncreasing(2595_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x1[3], x2[3])), x3[3], x1[3], x5[3])), ≥)∧[(-1)Bound*bni_107] + [(-1)bni_107]x3[2] + [bni_107]x1[2] ≥ 0∧[(-1)bso_108] ≥ 0)
(69) (x3[2] ≥ 0∧x1[2] + [-1] + [-1]x3[2] ≥ 0 ⇒ (UIncreasing(2595_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x1[3], x2[3])), x3[3], x1[3], x5[3])), ≥)∧0 = 0∧[(-1)Bound*bni_107] + [(-1)bni_107]x3[2] + [bni_107]x1[2] ≥ 0∧0 = 0∧[(-1)bso_108] ≥ 0)
(70) (x3[2] ≥ 0∧x1[2] ≥ 0 ⇒ (UIncreasing(2595_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x1[3], x2[3])), x3[3], x1[3], x5[3])), ≥)∧0 = 0∧[(-1)Bound*bni_107 + bni_107] + [bni_107]x1[2] ≥ 0∧0 = 0∧[(-1)bso_108] ≥ 0)
(71) (&&(>=(x4[4], 0), <(x4[4], x2[4]))=TRUE∧java.lang.Object(ARRAY(x2[4], x3[4]))=java.lang.Object(ARRAY(x2[5], x3[5]))∧x4[4]=x4[5] ⇒ 2420_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x2[4], x3[4])), x4[4], 0)≥NonInfC∧2420_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x2[4], x3[4])), x4[4], 0)≥COND_2420_1_MAIN_INVOKEMETHOD1(&&(>=(x4[4], 0), <(x4[4], x2[4])), java.lang.Object(ARRAY(x2[4], x3[4])), x4[4], 0)∧(UIncreasing(COND_2420_1_MAIN_INVOKEMETHOD1(&&(>=(x4[4], 0), <(x4[4], x2[4])), java.lang.Object(ARRAY(x2[4], x3[4])), x4[4], 0)), ≥))
(72) (>=(x4[4], 0)=TRUE∧<(x4[4], x2[4])=TRUE ⇒ 2420_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x2[4], x3[4])), x4[4], 0)≥NonInfC∧2420_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x2[4], x3[4])), x4[4], 0)≥COND_2420_1_MAIN_INVOKEMETHOD1(&&(>=(x4[4], 0), <(x4[4], x2[4])), java.lang.Object(ARRAY(x2[4], x3[4])), x4[4], 0)∧(UIncreasing(COND_2420_1_MAIN_INVOKEMETHOD1(&&(>=(x4[4], 0), <(x4[4], x2[4])), java.lang.Object(ARRAY(x2[4], x3[4])), x4[4], 0)), ≥))
(73) (x4[4] ≥ 0∧x2[4] + [-1] + [-1]x4[4] ≥ 0 ⇒ (UIncreasing(COND_2420_1_MAIN_INVOKEMETHOD1(&&(>=(x4[4], 0), <(x4[4], x2[4])), java.lang.Object(ARRAY(x2[4], x3[4])), x4[4], 0)), ≥)∧[(-1)Bound*bni_109] + [bni_109]x2[4] + [(-1)bni_109]x4[4] ≥ 0∧[(-1)bso_110] ≥ 0)
(74) (x4[4] ≥ 0∧x2[4] + [-1] + [-1]x4[4] ≥ 0 ⇒ (UIncreasing(COND_2420_1_MAIN_INVOKEMETHOD1(&&(>=(x4[4], 0), <(x4[4], x2[4])), java.lang.Object(ARRAY(x2[4], x3[4])), x4[4], 0)), ≥)∧[(-1)Bound*bni_109] + [bni_109]x2[4] + [(-1)bni_109]x4[4] ≥ 0∧[(-1)bso_110] ≥ 0)
(75) (x4[4] ≥ 0∧x2[4] + [-1] + [-1]x4[4] ≥ 0 ⇒ (UIncreasing(COND_2420_1_MAIN_INVOKEMETHOD1(&&(>=(x4[4], 0), <(x4[4], x2[4])), java.lang.Object(ARRAY(x2[4], x3[4])), x4[4], 0)), ≥)∧[(-1)Bound*bni_109] + [bni_109]x2[4] + [(-1)bni_109]x4[4] ≥ 0∧[(-1)bso_110] ≥ 0)
(76) (x4[4] ≥ 0∧x2[4] + [-1] + [-1]x4[4] ≥ 0 ⇒ (UIncreasing(COND_2420_1_MAIN_INVOKEMETHOD1(&&(>=(x4[4], 0), <(x4[4], x2[4])), java.lang.Object(ARRAY(x2[4], x3[4])), x4[4], 0)), ≥)∧0 = 0∧[(-1)Bound*bni_109] + [bni_109]x2[4] + [(-1)bni_109]x4[4] ≥ 0∧0 = 0∧[(-1)bso_110] ≥ 0)
(77) (x4[4] ≥ 0∧x2[4] ≥ 0 ⇒ (UIncreasing(COND_2420_1_MAIN_INVOKEMETHOD1(&&(>=(x4[4], 0), <(x4[4], x2[4])), java.lang.Object(ARRAY(x2[4], x3[4])), x4[4], 0)), ≥)∧0 = 0∧[(-1)Bound*bni_109 + bni_109] + [bni_109]x2[4] ≥ 0∧0 = 0∧[(-1)bso_110] ≥ 0)
(78) (java.lang.Object(ARRAY(x0[0], x3[0]))=java.lang.Object(ARRAY(x2[4], x3[4]))∧x4[0]=x4[4]∧x1[0]=0∧&&(>=(x4[4], 0), <(x4[4], x2[4]))=TRUE∧java.lang.Object(ARRAY(x2[4], x3[4]))=java.lang.Object(ARRAY(x2[5], x3[5]))∧x4[4]=x4[5] ⇒ COND_2420_1_MAIN_INVOKEMETHOD1(TRUE, java.lang.Object(ARRAY(x2[5], x3[5])), x4[5], 0)≥NonInfC∧COND_2420_1_MAIN_INVOKEMETHOD1(TRUE, java.lang.Object(ARRAY(x2[5], x3[5])), x4[5], 0)≥2595_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x2[5], x3[5])), x4[5], x2[5], x6[5])∧(UIncreasing(2595_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x2[5], x3[5])), x4[5], x2[5], x6[5])), ≥))
(79) (>=(x4[4], 0)=TRUE∧<(x4[4], x2[4])=TRUE ⇒ COND_2420_1_MAIN_INVOKEMETHOD1(TRUE, java.lang.Object(ARRAY(x2[4], x3[0])), x4[4], 0)≥NonInfC∧COND_2420_1_MAIN_INVOKEMETHOD1(TRUE, java.lang.Object(ARRAY(x2[4], x3[0])), x4[4], 0)≥2595_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x2[4], x3[0])), x4[4], x2[4], x6[5])∧(UIncreasing(2595_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x2[5], x3[5])), x4[5], x2[5], x6[5])), ≥))
(80) (x4[4] ≥ 0∧x2[4] + [-1] + [-1]x4[4] ≥ 0 ⇒ (UIncreasing(2595_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x2[5], x3[5])), x4[5], x2[5], x6[5])), ≥)∧[(-1)Bound*bni_111] + [(-1)bni_111]x4[4] + [bni_111]x2[4] ≥ 0∧[(-1)bso_112] ≥ 0)
(81) (x4[4] ≥ 0∧x2[4] + [-1] + [-1]x4[4] ≥ 0 ⇒ (UIncreasing(2595_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x2[5], x3[5])), x4[5], x2[5], x6[5])), ≥)∧[(-1)Bound*bni_111] + [(-1)bni_111]x4[4] + [bni_111]x2[4] ≥ 0∧[(-1)bso_112] ≥ 0)
(82) (x4[4] ≥ 0∧x2[4] + [-1] + [-1]x4[4] ≥ 0 ⇒ (UIncreasing(2595_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x2[5], x3[5])), x4[5], x2[5], x6[5])), ≥)∧[(-1)Bound*bni_111] + [(-1)bni_111]x4[4] + [bni_111]x2[4] ≥ 0∧[(-1)bso_112] ≥ 0)
(83) (x4[4] ≥ 0∧x2[4] + [-1] + [-1]x4[4] ≥ 0 ⇒ (UIncreasing(2595_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x2[5], x3[5])), x4[5], x2[5], x6[5])), ≥)∧0 = 0∧[(-1)Bound*bni_111] + [(-1)bni_111]x4[4] + [bni_111]x2[4] ≥ 0∧0 = 0∧[(-1)bso_112] ≥ 0)
(84) (x4[4] ≥ 0∧x2[4] ≥ 0 ⇒ (UIncreasing(2595_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x2[5], x3[5])), x4[5], x2[5], x6[5])), ≥)∧0 = 0∧[(-1)Bound*bni_111 + bni_111] + [bni_111]x2[4] ≥ 0∧0 = 0∧[(-1)bso_112] ≥ 0)
(85) (java.lang.Object(ARRAY(x0[1], x4[1]))=java.lang.Object(ARRAY(x2[4], x3[4]))∧x5[1]=x4[4]∧1=0∧&&(>=(x4[4], 0), <(x4[4], x2[4]))=TRUE∧java.lang.Object(ARRAY(x2[4], x3[4]))=java.lang.Object(ARRAY(x2[5], x3[5]))∧x4[4]=x4[5] ⇒ COND_2420_1_MAIN_INVOKEMETHOD1(TRUE, java.lang.Object(ARRAY(x2[5], x3[5])), x4[5], 0)≥NonInfC∧COND_2420_1_MAIN_INVOKEMETHOD1(TRUE, java.lang.Object(ARRAY(x2[5], x3[5])), x4[5], 0)≥2595_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x2[5], x3[5])), x4[5], x2[5], x6[5])∧(UIncreasing(2595_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x2[5], x3[5])), x4[5], x2[5], x6[5])), ≥))
(86) (java.lang.Object(ARRAY(x0[17], x3[17]))=java.lang.Object(ARRAY(x2[4], x3[4]))∧x4[17]=x4[4]∧x0[17]=0∧&&(>=(x4[4], 0), <(x4[4], x2[4]))=TRUE∧java.lang.Object(ARRAY(x2[4], x3[4]))=java.lang.Object(ARRAY(x2[5], x3[5]))∧x4[4]=x4[5] ⇒ COND_2420_1_MAIN_INVOKEMETHOD1(TRUE, java.lang.Object(ARRAY(x2[5], x3[5])), x4[5], 0)≥NonInfC∧COND_2420_1_MAIN_INVOKEMETHOD1(TRUE, java.lang.Object(ARRAY(x2[5], x3[5])), x4[5], 0)≥2595_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x2[5], x3[5])), x4[5], x2[5], x6[5])∧(UIncreasing(2595_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x2[5], x3[5])), x4[5], x2[5], x6[5])), ≥))
(87) (>=(x4[4], 0)=TRUE∧<(x4[4], 0)=TRUE ⇒ COND_2420_1_MAIN_INVOKEMETHOD1(TRUE, java.lang.Object(ARRAY(0, x3[17])), x4[4], 0)≥NonInfC∧COND_2420_1_MAIN_INVOKEMETHOD1(TRUE, java.lang.Object(ARRAY(0, x3[17])), x4[4], 0)≥2595_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(0, x3[17])), x4[4], 0, x6[5])∧(UIncreasing(2595_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x2[5], x3[5])), x4[5], x2[5], x6[5])), ≥))
(88) (x4[4] ≥ 0∧[-1] + [-1]x4[4] ≥ 0 ⇒ (UIncreasing(2595_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x2[5], x3[5])), x4[5], x2[5], x6[5])), ≥)∧[(-1)Bound*bni_111] + [(-1)bni_111]x4[4] ≥ 0∧[(-1)bso_112] ≥ 0)
(89) (x4[4] ≥ 0∧[-1] + [-1]x4[4] ≥ 0 ⇒ (UIncreasing(2595_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x2[5], x3[5])), x4[5], x2[5], x6[5])), ≥)∧[(-1)Bound*bni_111] + [(-1)bni_111]x4[4] ≥ 0∧[(-1)bso_112] ≥ 0)
(90) (x4[4] ≥ 0∧[-1] + [-1]x4[4] ≥ 0 ⇒ (UIncreasing(2595_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x2[5], x3[5])), x4[5], x2[5], x6[5])), ≥)∧[(-1)Bound*bni_111] + [(-1)bni_111]x4[4] ≥ 0∧[(-1)bso_112] ≥ 0)
(91) (x4[4] ≥ 0∧[-1] + [-1]x4[4] ≥ 0 ⇒ (UIncreasing(2595_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x2[5], x3[5])), x4[5], x2[5], x6[5])), ≥)∧0 = 0∧[(-1)Bound*bni_111] + [(-1)bni_111]x4[4] ≥ 0∧0 = 0∧[(-1)bso_112] ≥ 0)
(92) (&&(>=(x3[2], 0), <(x3[2], x1[2]))=TRUE∧java.lang.Object(ARRAY(x1[2], x2[2]))=java.lang.Object(ARRAY(x1[3], x2[3]))∧x3[2]=x3[3]∧x4[2]=x4[3]∧java.lang.Object(ARRAY(x1[3], x2[3]))=java.lang.Object(ARRAY(x2[6], x3[6]))∧x3[3]=x4[6]∧x1[3]=x0[6]∧x5[3]=x5[6] ⇒ 2595_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x2[6], x3[6])), x4[6], x0[6], x5[6])≥NonInfC∧2595_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x2[6], x3[6])), x4[6], x0[6], x5[6])≥2636_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x0[6], x3[6])), x4[6], x1[6])∧(UIncreasing(2636_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x0[6], x3[6])), x4[6], x1[6])), ≥))
(93) (>=(x3[2], 0)=TRUE∧<(x3[2], x1[2])=TRUE ⇒ 2595_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x1[2], x2[2])), x3[2], x1[2], x5[3])≥NonInfC∧2595_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x1[2], x2[2])), x3[2], x1[2], x5[3])≥2636_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x1[2], x2[2])), x3[2], x1[6])∧(UIncreasing(2636_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x0[6], x3[6])), x4[6], x1[6])), ≥))
(94) (x3[2] ≥ 0∧x1[2] + [-1] + [-1]x3[2] ≥ 0 ⇒ (UIncreasing(2636_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x0[6], x3[6])), x4[6], x1[6])), ≥)∧[(-1)Bound*bni_113] + [bni_113]x1[2] + [(-1)bni_113]x3[2] ≥ 0∧[(-1)bso_114] ≥ 0)
(95) (x3[2] ≥ 0∧x1[2] + [-1] + [-1]x3[2] ≥ 0 ⇒ (UIncreasing(2636_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x0[6], x3[6])), x4[6], x1[6])), ≥)∧[(-1)Bound*bni_113] + [bni_113]x1[2] + [(-1)bni_113]x3[2] ≥ 0∧[(-1)bso_114] ≥ 0)
(96) (x3[2] ≥ 0∧x1[2] + [-1] + [-1]x3[2] ≥ 0 ⇒ (UIncreasing(2636_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x0[6], x3[6])), x4[6], x1[6])), ≥)∧[(-1)Bound*bni_113] + [bni_113]x1[2] + [(-1)bni_113]x3[2] ≥ 0∧[(-1)bso_114] ≥ 0)
(97) (x3[2] ≥ 0∧x1[2] + [-1] + [-1]x3[2] ≥ 0 ⇒ (UIncreasing(2636_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x0[6], x3[6])), x4[6], x1[6])), ≥)∧0 = 0∧[(-1)Bound*bni_113] + [bni_113]x1[2] + [(-1)bni_113]x3[2] ≥ 0∧0 = 0∧0 = 0∧[(-1)bso_114] ≥ 0)
(98) (x3[2] ≥ 0∧x1[2] ≥ 0 ⇒ (UIncreasing(2636_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x0[6], x3[6])), x4[6], x1[6])), ≥)∧0 = 0∧[(-1)Bound*bni_113 + bni_113] + [bni_113]x1[2] ≥ 0∧0 = 0∧0 = 0∧[(-1)bso_114] ≥ 0)
(99) (&&(>=(x4[4], 0), <(x4[4], x2[4]))=TRUE∧java.lang.Object(ARRAY(x2[4], x3[4]))=java.lang.Object(ARRAY(x2[5], x3[5]))∧x4[4]=x4[5]∧java.lang.Object(ARRAY(x2[5], x3[5]))=java.lang.Object(ARRAY(x2[6], x3[6]))∧x4[5]=x4[6]∧x2[5]=x0[6]∧x6[5]=x5[6] ⇒ 2595_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x2[6], x3[6])), x4[6], x0[6], x5[6])≥NonInfC∧2595_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x2[6], x3[6])), x4[6], x0[6], x5[6])≥2636_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x0[6], x3[6])), x4[6], x1[6])∧(UIncreasing(2636_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x0[6], x3[6])), x4[6], x1[6])), ≥))
(100) (>=(x4[4], 0)=TRUE∧<(x4[4], x2[4])=TRUE ⇒ 2595_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x2[4], x3[4])), x4[4], x2[4], x6[5])≥NonInfC∧2595_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x2[4], x3[4])), x4[4], x2[4], x6[5])≥2636_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x2[4], x3[4])), x4[4], x1[6])∧(UIncreasing(2636_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x0[6], x3[6])), x4[6], x1[6])), ≥))
(101) (x4[4] ≥ 0∧x2[4] + [-1] + [-1]x4[4] ≥ 0 ⇒ (UIncreasing(2636_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x0[6], x3[6])), x4[6], x1[6])), ≥)∧[(-1)Bound*bni_113] + [bni_113]x2[4] + [(-1)bni_113]x4[4] ≥ 0∧[(-1)bso_114] ≥ 0)
(102) (x4[4] ≥ 0∧x2[4] + [-1] + [-1]x4[4] ≥ 0 ⇒ (UIncreasing(2636_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x0[6], x3[6])), x4[6], x1[6])), ≥)∧[(-1)Bound*bni_113] + [bni_113]x2[4] + [(-1)bni_113]x4[4] ≥ 0∧[(-1)bso_114] ≥ 0)
(103) (x4[4] ≥ 0∧x2[4] + [-1] + [-1]x4[4] ≥ 0 ⇒ (UIncreasing(2636_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x0[6], x3[6])), x4[6], x1[6])), ≥)∧[(-1)Bound*bni_113] + [bni_113]x2[4] + [(-1)bni_113]x4[4] ≥ 0∧[(-1)bso_114] ≥ 0)
(104) (x4[4] ≥ 0∧x2[4] + [-1] + [-1]x4[4] ≥ 0 ⇒ (UIncreasing(2636_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x0[6], x3[6])), x4[6], x1[6])), ≥)∧0 = 0∧[(-1)Bound*bni_113] + [bni_113]x2[4] + [(-1)bni_113]x4[4] ≥ 0∧0 = 0∧0 = 0∧[(-1)bso_114] ≥ 0)
(105) (x4[4] ≥ 0∧x2[4] ≥ 0 ⇒ (UIncreasing(2636_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x0[6], x3[6])), x4[6], x1[6])), ≥)∧0 = 0∧[(-1)Bound*bni_113 + bni_113] + [bni_113]x2[4] ≥ 0∧0 = 0∧0 = 0∧[(-1)bso_114] ≥ 0)
(106) (&&(>=(x4[15], 0), <(x4[15], x2[15]))=TRUE∧java.lang.Object(ARRAY(x2[15], x3[15]))=java.lang.Object(ARRAY(x2[16], x3[16]))∧x4[15]=x4[16]∧java.lang.Object(ARRAY(x2[16], x3[16]))=java.lang.Object(ARRAY(x2[6], x3[6]))∧x4[16]=x4[6]∧x2[16]=x0[6]∧x6[16]=x5[6] ⇒ 2595_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x2[6], x3[6])), x4[6], x0[6], x5[6])≥NonInfC∧2595_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x2[6], x3[6])), x4[6], x0[6], x5[6])≥2636_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x0[6], x3[6])), x4[6], x1[6])∧(UIncreasing(2636_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x0[6], x3[6])), x4[6], x1[6])), ≥))
(107) (>=(x4[15], 0)=TRUE∧<(x4[15], x2[15])=TRUE ⇒ 2595_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x2[15], x3[15])), x4[15], x2[15], x6[16])≥NonInfC∧2595_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x2[15], x3[15])), x4[15], x2[15], x6[16])≥2636_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x2[15], x3[15])), x4[15], x1[6])∧(UIncreasing(2636_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x0[6], x3[6])), x4[6], x1[6])), ≥))
(108) (x4[15] ≥ 0∧x2[15] + [-1] + [-1]x4[15] ≥ 0 ⇒ (UIncreasing(2636_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x0[6], x3[6])), x4[6], x1[6])), ≥)∧[(-1)Bound*bni_113] + [bni_113]x2[15] + [(-1)bni_113]x4[15] ≥ 0∧[(-1)bso_114] ≥ 0)
(109) (x4[15] ≥ 0∧x2[15] + [-1] + [-1]x4[15] ≥ 0 ⇒ (UIncreasing(2636_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x0[6], x3[6])), x4[6], x1[6])), ≥)∧[(-1)Bound*bni_113] + [bni_113]x2[15] + [(-1)bni_113]x4[15] ≥ 0∧[(-1)bso_114] ≥ 0)
(110) (x4[15] ≥ 0∧x2[15] + [-1] + [-1]x4[15] ≥ 0 ⇒ (UIncreasing(2636_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x0[6], x3[6])), x4[6], x1[6])), ≥)∧[(-1)Bound*bni_113] + [bni_113]x2[15] + [(-1)bni_113]x4[15] ≥ 0∧[(-1)bso_114] ≥ 0)
(111) (x4[15] ≥ 0∧x2[15] + [-1] + [-1]x4[15] ≥ 0 ⇒ (UIncreasing(2636_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x0[6], x3[6])), x4[6], x1[6])), ≥)∧0 = 0∧[(-1)Bound*bni_113] + [bni_113]x2[15] + [(-1)bni_113]x4[15] ≥ 0∧0 = 0∧0 = 0∧[(-1)bso_114] ≥ 0)
(112) (x4[15] ≥ 0∧x2[15] ≥ 0 ⇒ (UIncreasing(2636_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x0[6], x3[6])), x4[6], x1[6])), ≥)∧0 = 0∧[(-1)Bound*bni_113 + bni_113] + [bni_113]x2[15] ≥ 0∧0 = 0∧0 = 0∧[(-1)bso_114] ≥ 0)
(113) (&&(>=(x3[2], 0), <(x3[2], x1[2]))=TRUE∧java.lang.Object(ARRAY(x1[2], x2[2]))=java.lang.Object(ARRAY(x1[3], x2[3]))∧x3[2]=x3[3]∧x4[2]=x4[3]∧java.lang.Object(ARRAY(x1[3], x2[3]))=java.lang.Object(ARRAY(x3[7], x4[7]))∧x3[3]=x5[7]∧x1[3]=x0[7]∧x5[3]=0 ⇒ 2595_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x3[7], x4[7])), x5[7], x0[7], 0)≥NonInfC∧2595_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x3[7], x4[7])), x5[7], x0[7], 0)≥2636_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x0[7], x4[7])), x5[7], 1)∧(UIncreasing(2636_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x0[7], x4[7])), x5[7], 1)), ≥))
(114) (>=(x3[2], 0)=TRUE∧<(x3[2], x1[2])=TRUE ⇒ 2595_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x1[2], x2[2])), x3[2], x1[2], 0)≥NonInfC∧2595_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x1[2], x2[2])), x3[2], x1[2], 0)≥2636_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x1[2], x2[2])), x3[2], 1)∧(UIncreasing(2636_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x0[7], x4[7])), x5[7], 1)), ≥))
(115) (x3[2] ≥ 0∧x1[2] + [-1] + [-1]x3[2] ≥ 0 ⇒ (UIncreasing(2636_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x0[7], x4[7])), x5[7], 1)), ≥)∧[(-1)Bound*bni_115] + [bni_115]x1[2] + [(-1)bni_115]x3[2] ≥ 0∧[(-1)bso_116] ≥ 0)
(116) (x3[2] ≥ 0∧x1[2] + [-1] + [-1]x3[2] ≥ 0 ⇒ (UIncreasing(2636_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x0[7], x4[7])), x5[7], 1)), ≥)∧[(-1)Bound*bni_115] + [bni_115]x1[2] + [(-1)bni_115]x3[2] ≥ 0∧[(-1)bso_116] ≥ 0)
(117) (x3[2] ≥ 0∧x1[2] + [-1] + [-1]x3[2] ≥ 0 ⇒ (UIncreasing(2636_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x0[7], x4[7])), x5[7], 1)), ≥)∧[(-1)Bound*bni_115] + [bni_115]x1[2] + [(-1)bni_115]x3[2] ≥ 0∧[(-1)bso_116] ≥ 0)
(118) (x3[2] ≥ 0∧x1[2] + [-1] + [-1]x3[2] ≥ 0 ⇒ (UIncreasing(2636_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x0[7], x4[7])), x5[7], 1)), ≥)∧0 = 0∧[(-1)Bound*bni_115] + [bni_115]x1[2] + [(-1)bni_115]x3[2] ≥ 0∧0 = 0∧[(-1)bso_116] ≥ 0)
(119) (x3[2] ≥ 0∧x1[2] ≥ 0 ⇒ (UIncreasing(2636_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x0[7], x4[7])), x5[7], 1)), ≥)∧0 = 0∧[(-1)Bound*bni_115 + bni_115] + [bni_115]x1[2] ≥ 0∧0 = 0∧[(-1)bso_116] ≥ 0)
(120) (&&(>=(x4[4], 0), <(x4[4], x2[4]))=TRUE∧java.lang.Object(ARRAY(x2[4], x3[4]))=java.lang.Object(ARRAY(x2[5], x3[5]))∧x4[4]=x4[5]∧java.lang.Object(ARRAY(x2[5], x3[5]))=java.lang.Object(ARRAY(x3[7], x4[7]))∧x4[5]=x5[7]∧x2[5]=x0[7]∧x6[5]=0 ⇒ 2595_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x3[7], x4[7])), x5[7], x0[7], 0)≥NonInfC∧2595_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x3[7], x4[7])), x5[7], x0[7], 0)≥2636_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x0[7], x4[7])), x5[7], 1)∧(UIncreasing(2636_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x0[7], x4[7])), x5[7], 1)), ≥))
(121) (>=(x4[4], 0)=TRUE∧<(x4[4], x2[4])=TRUE ⇒ 2595_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x2[4], x3[4])), x4[4], x2[4], 0)≥NonInfC∧2595_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x2[4], x3[4])), x4[4], x2[4], 0)≥2636_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x2[4], x3[4])), x4[4], 1)∧(UIncreasing(2636_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x0[7], x4[7])), x5[7], 1)), ≥))
(122) (x4[4] ≥ 0∧x2[4] + [-1] + [-1]x4[4] ≥ 0 ⇒ (UIncreasing(2636_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x0[7], x4[7])), x5[7], 1)), ≥)∧[(-1)Bound*bni_115] + [bni_115]x2[4] + [(-1)bni_115]x4[4] ≥ 0∧[(-1)bso_116] ≥ 0)
(123) (x4[4] ≥ 0∧x2[4] + [-1] + [-1]x4[4] ≥ 0 ⇒ (UIncreasing(2636_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x0[7], x4[7])), x5[7], 1)), ≥)∧[(-1)Bound*bni_115] + [bni_115]x2[4] + [(-1)bni_115]x4[4] ≥ 0∧[(-1)bso_116] ≥ 0)
(124) (x4[4] ≥ 0∧x2[4] + [-1] + [-1]x4[4] ≥ 0 ⇒ (UIncreasing(2636_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x0[7], x4[7])), x5[7], 1)), ≥)∧[(-1)Bound*bni_115] + [bni_115]x2[4] + [(-1)bni_115]x4[4] ≥ 0∧[(-1)bso_116] ≥ 0)
(125) (x4[4] ≥ 0∧x2[4] + [-1] + [-1]x4[4] ≥ 0 ⇒ (UIncreasing(2636_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x0[7], x4[7])), x5[7], 1)), ≥)∧0 = 0∧[(-1)Bound*bni_115] + [bni_115]x2[4] + [(-1)bni_115]x4[4] ≥ 0∧0 = 0∧[(-1)bso_116] ≥ 0)
(126) (x4[4] ≥ 0∧x2[4] ≥ 0 ⇒ (UIncreasing(2636_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x0[7], x4[7])), x5[7], 1)), ≥)∧0 = 0∧[(-1)Bound*bni_115 + bni_115] + [bni_115]x2[4] ≥ 0∧0 = 0∧[(-1)bso_116] ≥ 0)
(127) (&&(>=(x4[15], 0), <(x4[15], x2[15]))=TRUE∧java.lang.Object(ARRAY(x2[15], x3[15]))=java.lang.Object(ARRAY(x2[16], x3[16]))∧x4[15]=x4[16]∧java.lang.Object(ARRAY(x2[16], x3[16]))=java.lang.Object(ARRAY(x3[7], x4[7]))∧x4[16]=x5[7]∧x2[16]=x0[7]∧x6[16]=0 ⇒ 2595_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x3[7], x4[7])), x5[7], x0[7], 0)≥NonInfC∧2595_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x3[7], x4[7])), x5[7], x0[7], 0)≥2636_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x0[7], x4[7])), x5[7], 1)∧(UIncreasing(2636_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x0[7], x4[7])), x5[7], 1)), ≥))
(128) (>=(x4[15], 0)=TRUE∧<(x4[15], x2[15])=TRUE ⇒ 2595_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x2[15], x3[15])), x4[15], x2[15], 0)≥NonInfC∧2595_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x2[15], x3[15])), x4[15], x2[15], 0)≥2636_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x2[15], x3[15])), x4[15], 1)∧(UIncreasing(2636_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x0[7], x4[7])), x5[7], 1)), ≥))
(129) (x4[15] ≥ 0∧x2[15] + [-1] + [-1]x4[15] ≥ 0 ⇒ (UIncreasing(2636_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x0[7], x4[7])), x5[7], 1)), ≥)∧[(-1)Bound*bni_115] + [bni_115]x2[15] + [(-1)bni_115]x4[15] ≥ 0∧[(-1)bso_116] ≥ 0)
(130) (x4[15] ≥ 0∧x2[15] + [-1] + [-1]x4[15] ≥ 0 ⇒ (UIncreasing(2636_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x0[7], x4[7])), x5[7], 1)), ≥)∧[(-1)Bound*bni_115] + [bni_115]x2[15] + [(-1)bni_115]x4[15] ≥ 0∧[(-1)bso_116] ≥ 0)
(131) (x4[15] ≥ 0∧x2[15] + [-1] + [-1]x4[15] ≥ 0 ⇒ (UIncreasing(2636_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x0[7], x4[7])), x5[7], 1)), ≥)∧[(-1)Bound*bni_115] + [bni_115]x2[15] + [(-1)bni_115]x4[15] ≥ 0∧[(-1)bso_116] ≥ 0)
(132) (x4[15] ≥ 0∧x2[15] + [-1] + [-1]x4[15] ≥ 0 ⇒ (UIncreasing(2636_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x0[7], x4[7])), x5[7], 1)), ≥)∧0 = 0∧[(-1)Bound*bni_115] + [bni_115]x2[15] + [(-1)bni_115]x4[15] ≥ 0∧0 = 0∧[(-1)bso_116] ≥ 0)
(133) (x4[15] ≥ 0∧x2[15] ≥ 0 ⇒ (UIncreasing(2636_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x0[7], x4[7])), x5[7], 1)), ≥)∧0 = 0∧[(-1)Bound*bni_115 + bni_115] + [bni_115]x2[15] ≥ 0∧0 = 0∧[(-1)bso_116] ≥ 0)
(134) (&&(&&(>=(x3[8], 0), >(x1[8], +(x3[8], 1))), <=(0, +(x3[8], 1)))=TRUE∧java.lang.Object(ARRAY(x1[8], x2[8]))=java.lang.Object(ARRAY(x1[9], x2[9]))∧x3[8]=x3[9]∧x4[8]=x4[9] ⇒ 2636_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x1[8], x2[8])), x3[8], x4[8])≥NonInfC∧2636_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x1[8], x2[8])), x3[8], x4[8])≥COND_2636_1_MAIN_INVOKEMETHOD(&&(&&(>=(x3[8], 0), >(x1[8], +(x3[8], 1))), <=(0, +(x3[8], 1))), java.lang.Object(ARRAY(x1[8], x2[8])), x3[8], x4[8])∧(UIncreasing(COND_2636_1_MAIN_INVOKEMETHOD(&&(&&(>=(x3[8], 0), >(x1[8], +(x3[8], 1))), <=(0, +(x3[8], 1))), java.lang.Object(ARRAY(x1[8], x2[8])), x3[8], x4[8])), ≥))
(135) (<=(0, +(x3[8], 1))=TRUE∧>=(x3[8], 0)=TRUE∧>(x1[8], +(x3[8], 1))=TRUE ⇒ 2636_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x1[8], x2[8])), x3[8], x4[8])≥NonInfC∧2636_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x1[8], x2[8])), x3[8], x4[8])≥COND_2636_1_MAIN_INVOKEMETHOD(&&(&&(>=(x3[8], 0), >(x1[8], +(x3[8], 1))), <=(0, +(x3[8], 1))), java.lang.Object(ARRAY(x1[8], x2[8])), x3[8], x4[8])∧(UIncreasing(COND_2636_1_MAIN_INVOKEMETHOD(&&(&&(>=(x3[8], 0), >(x1[8], +(x3[8], 1))), <=(0, +(x3[8], 1))), java.lang.Object(ARRAY(x1[8], x2[8])), x3[8], x4[8])), ≥))
(136) (x3[8] + [1] ≥ 0∧x3[8] ≥ 0∧x1[8] + [-2] + [-1]x3[8] ≥ 0 ⇒ (UIncreasing(COND_2636_1_MAIN_INVOKEMETHOD(&&(&&(>=(x3[8], 0), >(x1[8], +(x3[8], 1))), <=(0, +(x3[8], 1))), java.lang.Object(ARRAY(x1[8], x2[8])), x3[8], x4[8])), ≥)∧[(-1)Bound*bni_117] + [bni_117]x1[8] + [(-1)bni_117]x3[8] ≥ 0∧[(-1)bso_118] ≥ 0)
(137) (x3[8] + [1] ≥ 0∧x3[8] ≥ 0∧x1[8] + [-2] + [-1]x3[8] ≥ 0 ⇒ (UIncreasing(COND_2636_1_MAIN_INVOKEMETHOD(&&(&&(>=(x3[8], 0), >(x1[8], +(x3[8], 1))), <=(0, +(x3[8], 1))), java.lang.Object(ARRAY(x1[8], x2[8])), x3[8], x4[8])), ≥)∧[(-1)Bound*bni_117] + [bni_117]x1[8] + [(-1)bni_117]x3[8] ≥ 0∧[(-1)bso_118] ≥ 0)
(138) (x3[8] + [1] ≥ 0∧x3[8] ≥ 0∧x1[8] + [-2] + [-1]x3[8] ≥ 0 ⇒ (UIncreasing(COND_2636_1_MAIN_INVOKEMETHOD(&&(&&(>=(x3[8], 0), >(x1[8], +(x3[8], 1))), <=(0, +(x3[8], 1))), java.lang.Object(ARRAY(x1[8], x2[8])), x3[8], x4[8])), ≥)∧[(-1)Bound*bni_117] + [bni_117]x1[8] + [(-1)bni_117]x3[8] ≥ 0∧[(-1)bso_118] ≥ 0)
(139) (x3[8] + [1] ≥ 0∧x3[8] ≥ 0∧x1[8] + [-2] + [-1]x3[8] ≥ 0 ⇒ (UIncreasing(COND_2636_1_MAIN_INVOKEMETHOD(&&(&&(>=(x3[8], 0), >(x1[8], +(x3[8], 1))), <=(0, +(x3[8], 1))), java.lang.Object(ARRAY(x1[8], x2[8])), x3[8], x4[8])), ≥)∧0 = 0∧0 = 0∧[(-1)Bound*bni_117] + [bni_117]x1[8] + [(-1)bni_117]x3[8] ≥ 0∧0 = 0∧0 = 0∧[(-1)bso_118] ≥ 0)
(140) (x3[8] + [1] ≥ 0∧x3[8] ≥ 0∧x1[8] ≥ 0 ⇒ (UIncreasing(COND_2636_1_MAIN_INVOKEMETHOD(&&(&&(>=(x3[8], 0), >(x1[8], +(x3[8], 1))), <=(0, +(x3[8], 1))), java.lang.Object(ARRAY(x1[8], x2[8])), x3[8], x4[8])), ≥)∧0 = 0∧0 = 0∧[(-1)Bound*bni_117 + (2)bni_117] + [bni_117]x1[8] ≥ 0∧0 = 0∧0 = 0∧[(-1)bso_118] ≥ 0)
(141) (java.lang.Object(ARRAY(x0[6], x3[6]))=java.lang.Object(ARRAY(x1[8], x2[8]))∧x4[6]=x3[8]∧x1[6]=x4[8]∧&&(&&(>=(x3[8], 0), >(x1[8], +(x3[8], 1))), <=(0, +(x3[8], 1)))=TRUE∧java.lang.Object(ARRAY(x1[8], x2[8]))=java.lang.Object(ARRAY(x1[9], x2[9]))∧x3[8]=x3[9]∧x4[8]=x4[9] ⇒ COND_2636_1_MAIN_INVOKEMETHOD(TRUE, java.lang.Object(ARRAY(x1[9], x2[9])), x3[9], x4[9])≥NonInfC∧COND_2636_1_MAIN_INVOKEMETHOD(TRUE, java.lang.Object(ARRAY(x1[9], x2[9])), x3[9], x4[9])≥2387_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x1[9], x2[9])), +(x3[9], 1), x1[9], x5[9])∧(UIncreasing(2387_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x1[9], x2[9])), +(x3[9], 1), x1[9], x5[9])), ≥))
(142) (<=(0, +(x3[8], 1))=TRUE∧>=(x3[8], 0)=TRUE∧>(x1[8], +(x3[8], 1))=TRUE ⇒ COND_2636_1_MAIN_INVOKEMETHOD(TRUE, java.lang.Object(ARRAY(x1[8], x3[6])), x3[8], x1[6])≥NonInfC∧COND_2636_1_MAIN_INVOKEMETHOD(TRUE, java.lang.Object(ARRAY(x1[8], x3[6])), x3[8], x1[6])≥2387_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x1[8], x3[6])), +(x3[8], 1), x1[8], x5[9])∧(UIncreasing(2387_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x1[9], x2[9])), +(x3[9], 1), x1[9], x5[9])), ≥))
(143) (x3[8] + [1] ≥ 0∧x3[8] ≥ 0∧x1[8] + [-2] + [-1]x3[8] ≥ 0 ⇒ (UIncreasing(2387_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x1[9], x2[9])), +(x3[9], 1), x1[9], x5[9])), ≥)∧[(-1)Bound*bni_119] + [(-1)bni_119]x3[8] + [bni_119]x1[8] ≥ 0∧[(-1)bso_120] ≥ 0)
(144) (x3[8] + [1] ≥ 0∧x3[8] ≥ 0∧x1[8] + [-2] + [-1]x3[8] ≥ 0 ⇒ (UIncreasing(2387_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x1[9], x2[9])), +(x3[9], 1), x1[9], x5[9])), ≥)∧[(-1)Bound*bni_119] + [(-1)bni_119]x3[8] + [bni_119]x1[8] ≥ 0∧[(-1)bso_120] ≥ 0)
(145) (x3[8] + [1] ≥ 0∧x3[8] ≥ 0∧x1[8] + [-2] + [-1]x3[8] ≥ 0 ⇒ (UIncreasing(2387_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x1[9], x2[9])), +(x3[9], 1), x1[9], x5[9])), ≥)∧[(-1)Bound*bni_119] + [(-1)bni_119]x3[8] + [bni_119]x1[8] ≥ 0∧[(-1)bso_120] ≥ 0)
(146) (x3[8] + [1] ≥ 0∧x3[8] ≥ 0∧x1[8] + [-2] + [-1]x3[8] ≥ 0 ⇒ (UIncreasing(2387_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x1[9], x2[9])), +(x3[9], 1), x1[9], x5[9])), ≥)∧0 = 0∧0 = 0∧[(-1)Bound*bni_119] + [(-1)bni_119]x3[8] + [bni_119]x1[8] ≥ 0∧0 = 0∧0 = 0∧[(-1)bso_120] ≥ 0)
(147) (x3[8] + [1] ≥ 0∧x3[8] ≥ 0∧x1[8] ≥ 0 ⇒ (UIncreasing(2387_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x1[9], x2[9])), +(x3[9], 1), x1[9], x5[9])), ≥)∧0 = 0∧0 = 0∧[(-1)Bound*bni_119 + (2)bni_119] + [bni_119]x1[8] ≥ 0∧0 = 0∧0 = 0∧[(-1)bso_120] ≥ 0)
(148) (java.lang.Object(ARRAY(x0[7], x4[7]))=java.lang.Object(ARRAY(x1[8], x2[8]))∧x5[7]=x3[8]∧1=x4[8]∧&&(&&(>=(x3[8], 0), >(x1[8], +(x3[8], 1))), <=(0, +(x3[8], 1)))=TRUE∧java.lang.Object(ARRAY(x1[8], x2[8]))=java.lang.Object(ARRAY(x1[9], x2[9]))∧x3[8]=x3[9]∧x4[8]=x4[9] ⇒ COND_2636_1_MAIN_INVOKEMETHOD(TRUE, java.lang.Object(ARRAY(x1[9], x2[9])), x3[9], x4[9])≥NonInfC∧COND_2636_1_MAIN_INVOKEMETHOD(TRUE, java.lang.Object(ARRAY(x1[9], x2[9])), x3[9], x4[9])≥2387_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x1[9], x2[9])), +(x3[9], 1), x1[9], x5[9])∧(UIncreasing(2387_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x1[9], x2[9])), +(x3[9], 1), x1[9], x5[9])), ≥))
(149) (<=(0, +(x3[8], 1))=TRUE∧>=(x3[8], 0)=TRUE∧>(x1[8], +(x3[8], 1))=TRUE ⇒ COND_2636_1_MAIN_INVOKEMETHOD(TRUE, java.lang.Object(ARRAY(x1[8], x4[7])), x3[8], 1)≥NonInfC∧COND_2636_1_MAIN_INVOKEMETHOD(TRUE, java.lang.Object(ARRAY(x1[8], x4[7])), x3[8], 1)≥2387_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x1[8], x4[7])), +(x3[8], 1), x1[8], x5[9])∧(UIncreasing(2387_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x1[9], x2[9])), +(x3[9], 1), x1[9], x5[9])), ≥))
(150) (x3[8] + [1] ≥ 0∧x3[8] ≥ 0∧x1[8] + [-2] + [-1]x3[8] ≥ 0 ⇒ (UIncreasing(2387_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x1[9], x2[9])), +(x3[9], 1), x1[9], x5[9])), ≥)∧[(-1)Bound*bni_119] + [(-1)bni_119]x3[8] + [bni_119]x1[8] ≥ 0∧[(-1)bso_120] ≥ 0)
(151) (x3[8] + [1] ≥ 0∧x3[8] ≥ 0∧x1[8] + [-2] + [-1]x3[8] ≥ 0 ⇒ (UIncreasing(2387_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x1[9], x2[9])), +(x3[9], 1), x1[9], x5[9])), ≥)∧[(-1)Bound*bni_119] + [(-1)bni_119]x3[8] + [bni_119]x1[8] ≥ 0∧[(-1)bso_120] ≥ 0)
(152) (x3[8] + [1] ≥ 0∧x3[8] ≥ 0∧x1[8] + [-2] + [-1]x3[8] ≥ 0 ⇒ (UIncreasing(2387_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x1[9], x2[9])), +(x3[9], 1), x1[9], x5[9])), ≥)∧[(-1)Bound*bni_119] + [(-1)bni_119]x3[8] + [bni_119]x1[8] ≥ 0∧[(-1)bso_120] ≥ 0)
(153) (x3[8] + [1] ≥ 0∧x3[8] ≥ 0∧x1[8] + [-2] + [-1]x3[8] ≥ 0 ⇒ (UIncreasing(2387_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x1[9], x2[9])), +(x3[9], 1), x1[9], x5[9])), ≥)∧0 = 0∧[(-1)Bound*bni_119] + [(-1)bni_119]x3[8] + [bni_119]x1[8] ≥ 0∧0 = 0∧[(-1)bso_120] ≥ 0)
(154) (x3[8] + [1] ≥ 0∧x3[8] ≥ 0∧x1[8] ≥ 0 ⇒ (UIncreasing(2387_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x1[9], x2[9])), +(x3[9], 1), x1[9], x5[9])), ≥)∧0 = 0∧[(-1)Bound*bni_119 + (2)bni_119] + [bni_119]x1[8] ≥ 0∧0 = 0∧[(-1)bso_120] ≥ 0)
(155) (java.lang.Object(ARRAY(x0[14], x3[14]))=java.lang.Object(ARRAY(x1[8], x2[8]))∧x4[14]=x3[8]∧x0[14]=x4[8]∧&&(&&(>=(x3[8], 0), >(x1[8], +(x3[8], 1))), <=(0, +(x3[8], 1)))=TRUE∧java.lang.Object(ARRAY(x1[8], x2[8]))=java.lang.Object(ARRAY(x1[9], x2[9]))∧x3[8]=x3[9]∧x4[8]=x4[9] ⇒ COND_2636_1_MAIN_INVOKEMETHOD(TRUE, java.lang.Object(ARRAY(x1[9], x2[9])), x3[9], x4[9])≥NonInfC∧COND_2636_1_MAIN_INVOKEMETHOD(TRUE, java.lang.Object(ARRAY(x1[9], x2[9])), x3[9], x4[9])≥2387_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x1[9], x2[9])), +(x3[9], 1), x1[9], x5[9])∧(UIncreasing(2387_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x1[9], x2[9])), +(x3[9], 1), x1[9], x5[9])), ≥))
(156) (<=(0, +(x3[8], 1))=TRUE∧>=(x3[8], 0)=TRUE∧>(x1[8], +(x3[8], 1))=TRUE ⇒ COND_2636_1_MAIN_INVOKEMETHOD(TRUE, java.lang.Object(ARRAY(x1[8], x3[14])), x3[8], x1[8])≥NonInfC∧COND_2636_1_MAIN_INVOKEMETHOD(TRUE, java.lang.Object(ARRAY(x1[8], x3[14])), x3[8], x1[8])≥2387_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x1[8], x3[14])), +(x3[8], 1), x1[8], x5[9])∧(UIncreasing(2387_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x1[9], x2[9])), +(x3[9], 1), x1[9], x5[9])), ≥))
(157) (x3[8] + [1] ≥ 0∧x3[8] ≥ 0∧x1[8] + [-2] + [-1]x3[8] ≥ 0 ⇒ (UIncreasing(2387_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x1[9], x2[9])), +(x3[9], 1), x1[9], x5[9])), ≥)∧[(-1)Bound*bni_119] + [(-1)bni_119]x3[8] + [bni_119]x1[8] ≥ 0∧[(-1)bso_120] ≥ 0)
(158) (x3[8] + [1] ≥ 0∧x3[8] ≥ 0∧x1[8] + [-2] + [-1]x3[8] ≥ 0 ⇒ (UIncreasing(2387_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x1[9], x2[9])), +(x3[9], 1), x1[9], x5[9])), ≥)∧[(-1)Bound*bni_119] + [(-1)bni_119]x3[8] + [bni_119]x1[8] ≥ 0∧[(-1)bso_120] ≥ 0)
(159) (x3[8] + [1] ≥ 0∧x3[8] ≥ 0∧x1[8] + [-2] + [-1]x3[8] ≥ 0 ⇒ (UIncreasing(2387_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x1[9], x2[9])), +(x3[9], 1), x1[9], x5[9])), ≥)∧[(-1)Bound*bni_119] + [(-1)bni_119]x3[8] + [bni_119]x1[8] ≥ 0∧[(-1)bso_120] ≥ 0)
(160) (x3[8] + [1] ≥ 0∧x3[8] ≥ 0∧x1[8] + [-2] + [-1]x3[8] ≥ 0 ⇒ (UIncreasing(2387_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x1[9], x2[9])), +(x3[9], 1), x1[9], x5[9])), ≥)∧0 = 0∧[(-1)Bound*bni_119] + [(-1)bni_119]x3[8] + [bni_119]x1[8] ≥ 0∧0 = 0∧[(-1)bso_120] ≥ 0)
(161) (x3[8] + [1] ≥ 0∧x3[8] ≥ 0∧x1[8] ≥ 0 ⇒ (UIncreasing(2387_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x1[9], x2[9])), +(x3[9], 1), x1[9], x5[9])), ≥)∧0 = 0∧[(-1)Bound*bni_119 + (2)bni_119] + [bni_119]x1[8] ≥ 0∧0 = 0∧[(-1)bso_120] ≥ 0)
(162) (&&(&&(>=(x3[10], 0), >(x1[10], +(x3[10], 1))), <=(0, +(x3[10], 1)))=TRUE∧java.lang.Object(ARRAY(x1[10], x2[10]))=java.lang.Object(ARRAY(x1[11], x2[11]))∧x3[10]=x3[11] ⇒ 2636_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x1[10], x2[10])), x3[10], 0)≥NonInfC∧2636_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x1[10], x2[10])), x3[10], 0)≥COND_2636_1_MAIN_INVOKEMETHOD1(&&(&&(>=(x3[10], 0), >(x1[10], +(x3[10], 1))), <=(0, +(x3[10], 1))), java.lang.Object(ARRAY(x1[10], x2[10])), x3[10], 0)∧(UIncreasing(COND_2636_1_MAIN_INVOKEMETHOD1(&&(&&(>=(x3[10], 0), >(x1[10], +(x3[10], 1))), <=(0, +(x3[10], 1))), java.lang.Object(ARRAY(x1[10], x2[10])), x3[10], 0)), ≥))
(163) (<=(0, +(x3[10], 1))=TRUE∧>=(x3[10], 0)=TRUE∧>(x1[10], +(x3[10], 1))=TRUE ⇒ 2636_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x1[10], x2[10])), x3[10], 0)≥NonInfC∧2636_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x1[10], x2[10])), x3[10], 0)≥COND_2636_1_MAIN_INVOKEMETHOD1(&&(&&(>=(x3[10], 0), >(x1[10], +(x3[10], 1))), <=(0, +(x3[10], 1))), java.lang.Object(ARRAY(x1[10], x2[10])), x3[10], 0)∧(UIncreasing(COND_2636_1_MAIN_INVOKEMETHOD1(&&(&&(>=(x3[10], 0), >(x1[10], +(x3[10], 1))), <=(0, +(x3[10], 1))), java.lang.Object(ARRAY(x1[10], x2[10])), x3[10], 0)), ≥))
(164) (x3[10] + [1] ≥ 0∧x3[10] ≥ 0∧x1[10] + [-2] + [-1]x3[10] ≥ 0 ⇒ (UIncreasing(COND_2636_1_MAIN_INVOKEMETHOD1(&&(&&(>=(x3[10], 0), >(x1[10], +(x3[10], 1))), <=(0, +(x3[10], 1))), java.lang.Object(ARRAY(x1[10], x2[10])), x3[10], 0)), ≥)∧[(-1)Bound*bni_121] + [bni_121]x1[10] + [(-1)bni_121]x3[10] ≥ 0∧[(-1)bso_122] ≥ 0)
(165) (x3[10] + [1] ≥ 0∧x3[10] ≥ 0∧x1[10] + [-2] + [-1]x3[10] ≥ 0 ⇒ (UIncreasing(COND_2636_1_MAIN_INVOKEMETHOD1(&&(&&(>=(x3[10], 0), >(x1[10], +(x3[10], 1))), <=(0, +(x3[10], 1))), java.lang.Object(ARRAY(x1[10], x2[10])), x3[10], 0)), ≥)∧[(-1)Bound*bni_121] + [bni_121]x1[10] + [(-1)bni_121]x3[10] ≥ 0∧[(-1)bso_122] ≥ 0)
(166) (x3[10] + [1] ≥ 0∧x3[10] ≥ 0∧x1[10] + [-2] + [-1]x3[10] ≥ 0 ⇒ (UIncreasing(COND_2636_1_MAIN_INVOKEMETHOD1(&&(&&(>=(x3[10], 0), >(x1[10], +(x3[10], 1))), <=(0, +(x3[10], 1))), java.lang.Object(ARRAY(x1[10], x2[10])), x3[10], 0)), ≥)∧[(-1)Bound*bni_121] + [bni_121]x1[10] + [(-1)bni_121]x3[10] ≥ 0∧[(-1)bso_122] ≥ 0)
(167) (x3[10] + [1] ≥ 0∧x3[10] ≥ 0∧x1[10] + [-2] + [-1]x3[10] ≥ 0 ⇒ (UIncreasing(COND_2636_1_MAIN_INVOKEMETHOD1(&&(&&(>=(x3[10], 0), >(x1[10], +(x3[10], 1))), <=(0, +(x3[10], 1))), java.lang.Object(ARRAY(x1[10], x2[10])), x3[10], 0)), ≥)∧0 = 0∧[(-1)Bound*bni_121] + [bni_121]x1[10] + [(-1)bni_121]x3[10] ≥ 0∧0 = 0∧[(-1)bso_122] ≥ 0)
(168) (x3[10] + [1] ≥ 0∧x3[10] ≥ 0∧x1[10] ≥ 0 ⇒ (UIncreasing(COND_2636_1_MAIN_INVOKEMETHOD1(&&(&&(>=(x3[10], 0), >(x1[10], +(x3[10], 1))), <=(0, +(x3[10], 1))), java.lang.Object(ARRAY(x1[10], x2[10])), x3[10], 0)), ≥)∧0 = 0∧[(-1)Bound*bni_121 + (2)bni_121] + [bni_121]x1[10] ≥ 0∧0 = 0∧[(-1)bso_122] ≥ 0)
(169) (java.lang.Object(ARRAY(x0[6], x3[6]))=java.lang.Object(ARRAY(x1[10], x2[10]))∧x4[6]=x3[10]∧x1[6]=0∧&&(&&(>=(x3[10], 0), >(x1[10], +(x3[10], 1))), <=(0, +(x3[10], 1)))=TRUE∧java.lang.Object(ARRAY(x1[10], x2[10]))=java.lang.Object(ARRAY(x1[11], x2[11]))∧x3[10]=x3[11] ⇒ COND_2636_1_MAIN_INVOKEMETHOD1(TRUE, java.lang.Object(ARRAY(x1[11], x2[11])), x3[11], 0)≥NonInfC∧COND_2636_1_MAIN_INVOKEMETHOD1(TRUE, java.lang.Object(ARRAY(x1[11], x2[11])), x3[11], 0)≥2387_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x1[11], x2[11])), +(x3[11], 1), x1[11], x5[11])∧(UIncreasing(2387_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x1[11], x2[11])), +(x3[11], 1), x1[11], x5[11])), ≥))
(170) (<=(0, +(x3[10], 1))=TRUE∧>=(x3[10], 0)=TRUE∧>(x1[10], +(x3[10], 1))=TRUE ⇒ COND_2636_1_MAIN_INVOKEMETHOD1(TRUE, java.lang.Object(ARRAY(x1[10], x3[6])), x3[10], 0)≥NonInfC∧COND_2636_1_MAIN_INVOKEMETHOD1(TRUE, java.lang.Object(ARRAY(x1[10], x3[6])), x3[10], 0)≥2387_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x1[10], x3[6])), +(x3[10], 1), x1[10], x5[11])∧(UIncreasing(2387_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x1[11], x2[11])), +(x3[11], 1), x1[11], x5[11])), ≥))
(171) (x3[10] + [1] ≥ 0∧x3[10] ≥ 0∧x1[10] + [-2] + [-1]x3[10] ≥ 0 ⇒ (UIncreasing(2387_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x1[11], x2[11])), +(x3[11], 1), x1[11], x5[11])), ≥)∧[(-1)Bound*bni_123] + [(-1)bni_123]x3[10] + [bni_123]x1[10] ≥ 0∧[(-1)bso_124] ≥ 0)
(172) (x3[10] + [1] ≥ 0∧x3[10] ≥ 0∧x1[10] + [-2] + [-1]x3[10] ≥ 0 ⇒ (UIncreasing(2387_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x1[11], x2[11])), +(x3[11], 1), x1[11], x5[11])), ≥)∧[(-1)Bound*bni_123] + [(-1)bni_123]x3[10] + [bni_123]x1[10] ≥ 0∧[(-1)bso_124] ≥ 0)
(173) (x3[10] + [1] ≥ 0∧x3[10] ≥ 0∧x1[10] + [-2] + [-1]x3[10] ≥ 0 ⇒ (UIncreasing(2387_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x1[11], x2[11])), +(x3[11], 1), x1[11], x5[11])), ≥)∧[(-1)Bound*bni_123] + [(-1)bni_123]x3[10] + [bni_123]x1[10] ≥ 0∧[(-1)bso_124] ≥ 0)
(174) (x3[10] + [1] ≥ 0∧x3[10] ≥ 0∧x1[10] + [-2] + [-1]x3[10] ≥ 0 ⇒ (UIncreasing(2387_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x1[11], x2[11])), +(x3[11], 1), x1[11], x5[11])), ≥)∧0 = 0∧[(-1)Bound*bni_123] + [(-1)bni_123]x3[10] + [bni_123]x1[10] ≥ 0∧0 = 0∧[(-1)bso_124] ≥ 0)
(175) (x3[10] + [1] ≥ 0∧x3[10] ≥ 0∧x1[10] ≥ 0 ⇒ (UIncreasing(2387_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x1[11], x2[11])), +(x3[11], 1), x1[11], x5[11])), ≥)∧0 = 0∧[(-1)Bound*bni_123 + (2)bni_123] + [bni_123]x1[10] ≥ 0∧0 = 0∧[(-1)bso_124] ≥ 0)
(176) (java.lang.Object(ARRAY(x0[7], x4[7]))=java.lang.Object(ARRAY(x1[10], x2[10]))∧x5[7]=x3[10]∧1=0∧&&(&&(>=(x3[10], 0), >(x1[10], +(x3[10], 1))), <=(0, +(x3[10], 1)))=TRUE∧java.lang.Object(ARRAY(x1[10], x2[10]))=java.lang.Object(ARRAY(x1[11], x2[11]))∧x3[10]=x3[11] ⇒ COND_2636_1_MAIN_INVOKEMETHOD1(TRUE, java.lang.Object(ARRAY(x1[11], x2[11])), x3[11], 0)≥NonInfC∧COND_2636_1_MAIN_INVOKEMETHOD1(TRUE, java.lang.Object(ARRAY(x1[11], x2[11])), x3[11], 0)≥2387_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x1[11], x2[11])), +(x3[11], 1), x1[11], x5[11])∧(UIncreasing(2387_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x1[11], x2[11])), +(x3[11], 1), x1[11], x5[11])), ≥))
(177) (java.lang.Object(ARRAY(x0[14], x3[14]))=java.lang.Object(ARRAY(x1[10], x2[10]))∧x4[14]=x3[10]∧x0[14]=0∧&&(&&(>=(x3[10], 0), >(x1[10], +(x3[10], 1))), <=(0, +(x3[10], 1)))=TRUE∧java.lang.Object(ARRAY(x1[10], x2[10]))=java.lang.Object(ARRAY(x1[11], x2[11]))∧x3[10]=x3[11] ⇒ COND_2636_1_MAIN_INVOKEMETHOD1(TRUE, java.lang.Object(ARRAY(x1[11], x2[11])), x3[11], 0)≥NonInfC∧COND_2636_1_MAIN_INVOKEMETHOD1(TRUE, java.lang.Object(ARRAY(x1[11], x2[11])), x3[11], 0)≥2387_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x1[11], x2[11])), +(x3[11], 1), x1[11], x5[11])∧(UIncreasing(2387_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x1[11], x2[11])), +(x3[11], 1), x1[11], x5[11])), ≥))
(178) (<=(0, +(x3[10], 1))=TRUE∧>=(x3[10], 0)=TRUE∧>(0, +(x3[10], 1))=TRUE ⇒ COND_2636_1_MAIN_INVOKEMETHOD1(TRUE, java.lang.Object(ARRAY(0, x3[14])), x3[10], 0)≥NonInfC∧COND_2636_1_MAIN_INVOKEMETHOD1(TRUE, java.lang.Object(ARRAY(0, x3[14])), x3[10], 0)≥2387_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(0, x3[14])), +(x3[10], 1), 0, x5[11])∧(UIncreasing(2387_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x1[11], x2[11])), +(x3[11], 1), x1[11], x5[11])), ≥))
(179) (x3[10] + [1] ≥ 0∧x3[10] ≥ 0∧[-2] + [-1]x3[10] ≥ 0 ⇒ (UIncreasing(2387_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x1[11], x2[11])), +(x3[11], 1), x1[11], x5[11])), ≥)∧[(-1)Bound*bni_123] + [(-1)bni_123]x3[10] ≥ 0∧[(-1)bso_124] ≥ 0)
(180) (x3[10] + [1] ≥ 0∧x3[10] ≥ 0∧[-2] + [-1]x3[10] ≥ 0 ⇒ (UIncreasing(2387_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x1[11], x2[11])), +(x3[11], 1), x1[11], x5[11])), ≥)∧[(-1)Bound*bni_123] + [(-1)bni_123]x3[10] ≥ 0∧[(-1)bso_124] ≥ 0)
(181) (x3[10] + [1] ≥ 0∧x3[10] ≥ 0∧[-2] + [-1]x3[10] ≥ 0 ⇒ (UIncreasing(2387_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x1[11], x2[11])), +(x3[11], 1), x1[11], x5[11])), ≥)∧[(-1)Bound*bni_123] + [(-1)bni_123]x3[10] ≥ 0∧[(-1)bso_124] ≥ 0)
(182) (x3[10] + [1] ≥ 0∧x3[10] ≥ 0∧[-2] + [-1]x3[10] ≥ 0 ⇒ (UIncreasing(2387_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x1[11], x2[11])), +(x3[11], 1), x1[11], x5[11])), ≥)∧0 = 0∧[(-1)Bound*bni_123] + [(-1)bni_123]x3[10] ≥ 0∧0 = 0∧[(-1)bso_124] ≥ 0)
(183) (&&(&&(>=(x4[12], 0), >(x2[12], +(x4[12], 1))), <=(0, +(x4[12], 1)))=TRUE∧java.lang.Object(ARRAY(x2[12], x3[12]))=java.lang.Object(ARRAY(x2[13], x3[13]))∧x4[12]=x4[13] ⇒ 2636_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x2[12], x3[12])), x4[12], 1)≥NonInfC∧2636_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x2[12], x3[12])), x4[12], 1)≥COND_2636_1_MAIN_INVOKEMETHOD2(&&(&&(>=(x4[12], 0), >(x2[12], +(x4[12], 1))), <=(0, +(x4[12], 1))), java.lang.Object(ARRAY(x2[12], x3[12])), x4[12], 1)∧(UIncreasing(COND_2636_1_MAIN_INVOKEMETHOD2(&&(&&(>=(x4[12], 0), >(x2[12], +(x4[12], 1))), <=(0, +(x4[12], 1))), java.lang.Object(ARRAY(x2[12], x3[12])), x4[12], 1)), ≥))
(184) (<=(0, +(x4[12], 1))=TRUE∧>=(x4[12], 0)=TRUE∧>(x2[12], +(x4[12], 1))=TRUE ⇒ 2636_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x2[12], x3[12])), x4[12], 1)≥NonInfC∧2636_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x2[12], x3[12])), x4[12], 1)≥COND_2636_1_MAIN_INVOKEMETHOD2(&&(&&(>=(x4[12], 0), >(x2[12], +(x4[12], 1))), <=(0, +(x4[12], 1))), java.lang.Object(ARRAY(x2[12], x3[12])), x4[12], 1)∧(UIncreasing(COND_2636_1_MAIN_INVOKEMETHOD2(&&(&&(>=(x4[12], 0), >(x2[12], +(x4[12], 1))), <=(0, +(x4[12], 1))), java.lang.Object(ARRAY(x2[12], x3[12])), x4[12], 1)), ≥))
(185) (x4[12] + [1] ≥ 0∧x4[12] ≥ 0∧x2[12] + [-2] + [-1]x4[12] ≥ 0 ⇒ (UIncreasing(COND_2636_1_MAIN_INVOKEMETHOD2(&&(&&(>=(x4[12], 0), >(x2[12], +(x4[12], 1))), <=(0, +(x4[12], 1))), java.lang.Object(ARRAY(x2[12], x3[12])), x4[12], 1)), ≥)∧[(-1)Bound*bni_125] + [bni_125]x2[12] + [(-1)bni_125]x4[12] ≥ 0∧[(-1)bso_126] ≥ 0)
(186) (x4[12] + [1] ≥ 0∧x4[12] ≥ 0∧x2[12] + [-2] + [-1]x4[12] ≥ 0 ⇒ (UIncreasing(COND_2636_1_MAIN_INVOKEMETHOD2(&&(&&(>=(x4[12], 0), >(x2[12], +(x4[12], 1))), <=(0, +(x4[12], 1))), java.lang.Object(ARRAY(x2[12], x3[12])), x4[12], 1)), ≥)∧[(-1)Bound*bni_125] + [bni_125]x2[12] + [(-1)bni_125]x4[12] ≥ 0∧[(-1)bso_126] ≥ 0)
(187) (x4[12] + [1] ≥ 0∧x4[12] ≥ 0∧x2[12] + [-2] + [-1]x4[12] ≥ 0 ⇒ (UIncreasing(COND_2636_1_MAIN_INVOKEMETHOD2(&&(&&(>=(x4[12], 0), >(x2[12], +(x4[12], 1))), <=(0, +(x4[12], 1))), java.lang.Object(ARRAY(x2[12], x3[12])), x4[12], 1)), ≥)∧[(-1)Bound*bni_125] + [bni_125]x2[12] + [(-1)bni_125]x4[12] ≥ 0∧[(-1)bso_126] ≥ 0)
(188) (x4[12] + [1] ≥ 0∧x4[12] ≥ 0∧x2[12] + [-2] + [-1]x4[12] ≥ 0 ⇒ (UIncreasing(COND_2636_1_MAIN_INVOKEMETHOD2(&&(&&(>=(x4[12], 0), >(x2[12], +(x4[12], 1))), <=(0, +(x4[12], 1))), java.lang.Object(ARRAY(x2[12], x3[12])), x4[12], 1)), ≥)∧0 = 0∧[(-1)Bound*bni_125] + [bni_125]x2[12] + [(-1)bni_125]x4[12] ≥ 0∧0 = 0∧[(-1)bso_126] ≥ 0)
(189) (x4[12] + [1] ≥ 0∧x4[12] ≥ 0∧x2[12] ≥ 0 ⇒ (UIncreasing(COND_2636_1_MAIN_INVOKEMETHOD2(&&(&&(>=(x4[12], 0), >(x2[12], +(x4[12], 1))), <=(0, +(x4[12], 1))), java.lang.Object(ARRAY(x2[12], x3[12])), x4[12], 1)), ≥)∧0 = 0∧[(-1)Bound*bni_125 + (2)bni_125] + [bni_125]x2[12] ≥ 0∧0 = 0∧[(-1)bso_126] ≥ 0)
(190) (java.lang.Object(ARRAY(x0[6], x3[6]))=java.lang.Object(ARRAY(x2[12], x3[12]))∧x4[6]=x4[12]∧x1[6]=1∧&&(&&(>=(x4[12], 0), >(x2[12], +(x4[12], 1))), <=(0, +(x4[12], 1)))=TRUE∧java.lang.Object(ARRAY(x2[12], x3[12]))=java.lang.Object(ARRAY(x2[13], x3[13]))∧x4[12]=x4[13] ⇒ COND_2636_1_MAIN_INVOKEMETHOD2(TRUE, java.lang.Object(ARRAY(x2[13], x3[13])), x4[13], 1)≥NonInfC∧COND_2636_1_MAIN_INVOKEMETHOD2(TRUE, java.lang.Object(ARRAY(x2[13], x3[13])), x4[13], 1)≥2387_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x2[13], x3[13])), +(x4[13], 1), x2[13], x6[13])∧(UIncreasing(2387_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x2[13], x3[13])), +(x4[13], 1), x2[13], x6[13])), ≥))
(191) (<=(0, +(x4[12], 1))=TRUE∧>=(x4[12], 0)=TRUE∧>(x2[12], +(x4[12], 1))=TRUE ⇒ COND_2636_1_MAIN_INVOKEMETHOD2(TRUE, java.lang.Object(ARRAY(x2[12], x3[6])), x4[12], 1)≥NonInfC∧COND_2636_1_MAIN_INVOKEMETHOD2(TRUE, java.lang.Object(ARRAY(x2[12], x3[6])), x4[12], 1)≥2387_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x2[12], x3[6])), +(x4[12], 1), x2[12], x6[13])∧(UIncreasing(2387_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x2[13], x3[13])), +(x4[13], 1), x2[13], x6[13])), ≥))
(192) (x4[12] + [1] ≥ 0∧x4[12] ≥ 0∧x2[12] + [-2] + [-1]x4[12] ≥ 0 ⇒ (UIncreasing(2387_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x2[13], x3[13])), +(x4[13], 1), x2[13], x6[13])), ≥)∧[(-1)Bound*bni_127] + [(-1)bni_127]x4[12] + [bni_127]x2[12] ≥ 0∧[(-1)bso_128] ≥ 0)
(193) (x4[12] + [1] ≥ 0∧x4[12] ≥ 0∧x2[12] + [-2] + [-1]x4[12] ≥ 0 ⇒ (UIncreasing(2387_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x2[13], x3[13])), +(x4[13], 1), x2[13], x6[13])), ≥)∧[(-1)Bound*bni_127] + [(-1)bni_127]x4[12] + [bni_127]x2[12] ≥ 0∧[(-1)bso_128] ≥ 0)
(194) (x4[12] + [1] ≥ 0∧x4[12] ≥ 0∧x2[12] + [-2] + [-1]x4[12] ≥ 0 ⇒ (UIncreasing(2387_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x2[13], x3[13])), +(x4[13], 1), x2[13], x6[13])), ≥)∧[(-1)Bound*bni_127] + [(-1)bni_127]x4[12] + [bni_127]x2[12] ≥ 0∧[(-1)bso_128] ≥ 0)
(195) (x4[12] + [1] ≥ 0∧x4[12] ≥ 0∧x2[12] + [-2] + [-1]x4[12] ≥ 0 ⇒ (UIncreasing(2387_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x2[13], x3[13])), +(x4[13], 1), x2[13], x6[13])), ≥)∧0 = 0∧[(-1)Bound*bni_127] + [(-1)bni_127]x4[12] + [bni_127]x2[12] ≥ 0∧0 = 0∧[(-1)bso_128] ≥ 0)
(196) (x4[12] + [1] ≥ 0∧x4[12] ≥ 0∧x2[12] ≥ 0 ⇒ (UIncreasing(2387_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x2[13], x3[13])), +(x4[13], 1), x2[13], x6[13])), ≥)∧0 = 0∧[(-1)Bound*bni_127 + (2)bni_127] + [bni_127]x2[12] ≥ 0∧0 = 0∧[(-1)bso_128] ≥ 0)
(197) (java.lang.Object(ARRAY(x0[7], x4[7]))=java.lang.Object(ARRAY(x2[12], x3[12]))∧x5[7]=x4[12]∧&&(&&(>=(x4[12], 0), >(x2[12], +(x4[12], 1))), <=(0, +(x4[12], 1)))=TRUE∧java.lang.Object(ARRAY(x2[12], x3[12]))=java.lang.Object(ARRAY(x2[13], x3[13]))∧x4[12]=x4[13] ⇒ COND_2636_1_MAIN_INVOKEMETHOD2(TRUE, java.lang.Object(ARRAY(x2[13], x3[13])), x4[13], 1)≥NonInfC∧COND_2636_1_MAIN_INVOKEMETHOD2(TRUE, java.lang.Object(ARRAY(x2[13], x3[13])), x4[13], 1)≥2387_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x2[13], x3[13])), +(x4[13], 1), x2[13], x6[13])∧(UIncreasing(2387_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x2[13], x3[13])), +(x4[13], 1), x2[13], x6[13])), ≥))
(198) (<=(0, +(x4[12], 1))=TRUE∧>=(x4[12], 0)=TRUE∧>(x2[12], +(x4[12], 1))=TRUE ⇒ COND_2636_1_MAIN_INVOKEMETHOD2(TRUE, java.lang.Object(ARRAY(x2[12], x4[7])), x4[12], 1)≥NonInfC∧COND_2636_1_MAIN_INVOKEMETHOD2(TRUE, java.lang.Object(ARRAY(x2[12], x4[7])), x4[12], 1)≥2387_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x2[12], x4[7])), +(x4[12], 1), x2[12], x6[13])∧(UIncreasing(2387_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x2[13], x3[13])), +(x4[13], 1), x2[13], x6[13])), ≥))
(199) (x4[12] + [1] ≥ 0∧x4[12] ≥ 0∧x2[12] + [-2] + [-1]x4[12] ≥ 0 ⇒ (UIncreasing(2387_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x2[13], x3[13])), +(x4[13], 1), x2[13], x6[13])), ≥)∧[(-1)Bound*bni_127] + [(-1)bni_127]x4[12] + [bni_127]x2[12] ≥ 0∧[(-1)bso_128] ≥ 0)
(200) (x4[12] + [1] ≥ 0∧x4[12] ≥ 0∧x2[12] + [-2] + [-1]x4[12] ≥ 0 ⇒ (UIncreasing(2387_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x2[13], x3[13])), +(x4[13], 1), x2[13], x6[13])), ≥)∧[(-1)Bound*bni_127] + [(-1)bni_127]x4[12] + [bni_127]x2[12] ≥ 0∧[(-1)bso_128] ≥ 0)
(201) (x4[12] + [1] ≥ 0∧x4[12] ≥ 0∧x2[12] + [-2] + [-1]x4[12] ≥ 0 ⇒ (UIncreasing(2387_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x2[13], x3[13])), +(x4[13], 1), x2[13], x6[13])), ≥)∧[(-1)Bound*bni_127] + [(-1)bni_127]x4[12] + [bni_127]x2[12] ≥ 0∧[(-1)bso_128] ≥ 0)
(202) (x4[12] + [1] ≥ 0∧x4[12] ≥ 0∧x2[12] + [-2] + [-1]x4[12] ≥ 0 ⇒ (UIncreasing(2387_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x2[13], x3[13])), +(x4[13], 1), x2[13], x6[13])), ≥)∧0 = 0∧[(-1)Bound*bni_127] + [(-1)bni_127]x4[12] + [bni_127]x2[12] ≥ 0∧0 = 0∧[(-1)bso_128] ≥ 0)
(203) (x4[12] + [1] ≥ 0∧x4[12] ≥ 0∧x2[12] ≥ 0 ⇒ (UIncreasing(2387_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x2[13], x3[13])), +(x4[13], 1), x2[13], x6[13])), ≥)∧0 = 0∧[(-1)Bound*bni_127 + (2)bni_127] + [bni_127]x2[12] ≥ 0∧0 = 0∧[(-1)bso_128] ≥ 0)
(204) (java.lang.Object(ARRAY(x0[14], x3[14]))=java.lang.Object(ARRAY(x2[12], x3[12]))∧x4[14]=x4[12]∧x0[14]=1∧&&(&&(>=(x4[12], 0), >(x2[12], +(x4[12], 1))), <=(0, +(x4[12], 1)))=TRUE∧java.lang.Object(ARRAY(x2[12], x3[12]))=java.lang.Object(ARRAY(x2[13], x3[13]))∧x4[12]=x4[13] ⇒ COND_2636_1_MAIN_INVOKEMETHOD2(TRUE, java.lang.Object(ARRAY(x2[13], x3[13])), x4[13], 1)≥NonInfC∧COND_2636_1_MAIN_INVOKEMETHOD2(TRUE, java.lang.Object(ARRAY(x2[13], x3[13])), x4[13], 1)≥2387_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x2[13], x3[13])), +(x4[13], 1), x2[13], x6[13])∧(UIncreasing(2387_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x2[13], x3[13])), +(x4[13], 1), x2[13], x6[13])), ≥))
(205) (<=(0, +(x4[12], 1))=TRUE∧>=(x4[12], 0)=TRUE∧>(1, +(x4[12], 1))=TRUE ⇒ COND_2636_1_MAIN_INVOKEMETHOD2(TRUE, java.lang.Object(ARRAY(1, x3[14])), x4[12], 1)≥NonInfC∧COND_2636_1_MAIN_INVOKEMETHOD2(TRUE, java.lang.Object(ARRAY(1, x3[14])), x4[12], 1)≥2387_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(1, x3[14])), +(x4[12], 1), 1, x6[13])∧(UIncreasing(2387_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x2[13], x3[13])), +(x4[13], 1), x2[13], x6[13])), ≥))
(206) (x4[12] + [1] ≥ 0∧x4[12] ≥ 0∧[-1] + [-1]x4[12] ≥ 0 ⇒ (UIncreasing(2387_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x2[13], x3[13])), +(x4[13], 1), x2[13], x6[13])), ≥)∧[bni_127 + (-1)Bound*bni_127] + [(-1)bni_127]x4[12] ≥ 0∧[(-1)bso_128] ≥ 0)
(207) (x4[12] + [1] ≥ 0∧x4[12] ≥ 0∧[-1] + [-1]x4[12] ≥ 0 ⇒ (UIncreasing(2387_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x2[13], x3[13])), +(x4[13], 1), x2[13], x6[13])), ≥)∧[bni_127 + (-1)Bound*bni_127] + [(-1)bni_127]x4[12] ≥ 0∧[(-1)bso_128] ≥ 0)
(208) (x4[12] + [1] ≥ 0∧x4[12] ≥ 0∧[-1] + [-1]x4[12] ≥ 0 ⇒ (UIncreasing(2387_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x2[13], x3[13])), +(x4[13], 1), x2[13], x6[13])), ≥)∧[bni_127 + (-1)Bound*bni_127] + [(-1)bni_127]x4[12] ≥ 0∧[(-1)bso_128] ≥ 0)
(209) (x4[12] + [1] ≥ 0∧x4[12] ≥ 0∧[-1] + [-1]x4[12] ≥ 0 ⇒ (UIncreasing(2387_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x2[13], x3[13])), +(x4[13], 1), x2[13], x6[13])), ≥)∧0 = 0∧[bni_127 + (-1)Bound*bni_127] + [(-1)bni_127]x4[12] ≥ 0∧0 = 0∧[(-1)bso_128] ≥ 0)
(210) (&&(>=(x3[2], 0), <(x3[2], x1[2]))=TRUE∧java.lang.Object(ARRAY(x1[2], x2[2]))=java.lang.Object(ARRAY(x1[3], x2[3]))∧x3[2]=x3[3]∧x4[2]=x4[3]∧java.lang.Object(ARRAY(x1[3], x2[3]))=java.lang.Object(ARRAY(x2[14], x3[14]))∧x3[3]=x4[14]∧x1[3]=x0[14]∧x5[3]=1 ⇒ 2595_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x2[14], x3[14])), x4[14], x0[14], 1)≥NonInfC∧2595_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x2[14], x3[14])), x4[14], x0[14], 1)≥2636_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x0[14], x3[14])), x4[14], x0[14])∧(UIncreasing(2636_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x0[14], x3[14])), x4[14], x0[14])), ≥))
(211) (>=(x3[2], 0)=TRUE∧<(x3[2], x1[2])=TRUE ⇒ 2595_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x1[2], x2[2])), x3[2], x1[2], 1)≥NonInfC∧2595_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x1[2], x2[2])), x3[2], x1[2], 1)≥2636_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x1[2], x2[2])), x3[2], x1[2])∧(UIncreasing(2636_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x0[14], x3[14])), x4[14], x0[14])), ≥))
(212) (x3[2] ≥ 0∧x1[2] + [-1] + [-1]x3[2] ≥ 0 ⇒ (UIncreasing(2636_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x0[14], x3[14])), x4[14], x0[14])), ≥)∧[(-1)Bound*bni_129] + [bni_129]x1[2] + [(-1)bni_129]x3[2] ≥ 0∧[(-1)bso_130] ≥ 0)
(213) (x3[2] ≥ 0∧x1[2] + [-1] + [-1]x3[2] ≥ 0 ⇒ (UIncreasing(2636_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x0[14], x3[14])), x4[14], x0[14])), ≥)∧[(-1)Bound*bni_129] + [bni_129]x1[2] + [(-1)bni_129]x3[2] ≥ 0∧[(-1)bso_130] ≥ 0)
(214) (x3[2] ≥ 0∧x1[2] + [-1] + [-1]x3[2] ≥ 0 ⇒ (UIncreasing(2636_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x0[14], x3[14])), x4[14], x0[14])), ≥)∧[(-1)Bound*bni_129] + [bni_129]x1[2] + [(-1)bni_129]x3[2] ≥ 0∧[(-1)bso_130] ≥ 0)
(215) (x3[2] ≥ 0∧x1[2] + [-1] + [-1]x3[2] ≥ 0 ⇒ (UIncreasing(2636_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x0[14], x3[14])), x4[14], x0[14])), ≥)∧0 = 0∧[(-1)Bound*bni_129] + [bni_129]x1[2] + [(-1)bni_129]x3[2] ≥ 0∧0 = 0∧[(-1)bso_130] ≥ 0)
(216) (x3[2] ≥ 0∧x1[2] ≥ 0 ⇒ (UIncreasing(2636_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x0[14], x3[14])), x4[14], x0[14])), ≥)∧0 = 0∧[(-1)Bound*bni_129 + bni_129] + [bni_129]x1[2] ≥ 0∧0 = 0∧[(-1)bso_130] ≥ 0)
(217) (&&(>=(x4[4], 0), <(x4[4], x2[4]))=TRUE∧java.lang.Object(ARRAY(x2[4], x3[4]))=java.lang.Object(ARRAY(x2[5], x3[5]))∧x4[4]=x4[5]∧java.lang.Object(ARRAY(x2[5], x3[5]))=java.lang.Object(ARRAY(x2[14], x3[14]))∧x4[5]=x4[14]∧x2[5]=x0[14]∧x6[5]=1 ⇒ 2595_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x2[14], x3[14])), x4[14], x0[14], 1)≥NonInfC∧2595_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x2[14], x3[14])), x4[14], x0[14], 1)≥2636_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x0[14], x3[14])), x4[14], x0[14])∧(UIncreasing(2636_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x0[14], x3[14])), x4[14], x0[14])), ≥))
(218) (>=(x4[4], 0)=TRUE∧<(x4[4], x2[4])=TRUE ⇒ 2595_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x2[4], x3[4])), x4[4], x2[4], 1)≥NonInfC∧2595_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x2[4], x3[4])), x4[4], x2[4], 1)≥2636_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x2[4], x3[4])), x4[4], x2[4])∧(UIncreasing(2636_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x0[14], x3[14])), x4[14], x0[14])), ≥))
(219) (x4[4] ≥ 0∧x2[4] + [-1] + [-1]x4[4] ≥ 0 ⇒ (UIncreasing(2636_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x0[14], x3[14])), x4[14], x0[14])), ≥)∧[(-1)Bound*bni_129] + [bni_129]x2[4] + [(-1)bni_129]x4[4] ≥ 0∧[(-1)bso_130] ≥ 0)
(220) (x4[4] ≥ 0∧x2[4] + [-1] + [-1]x4[4] ≥ 0 ⇒ (UIncreasing(2636_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x0[14], x3[14])), x4[14], x0[14])), ≥)∧[(-1)Bound*bni_129] + [bni_129]x2[4] + [(-1)bni_129]x4[4] ≥ 0∧[(-1)bso_130] ≥ 0)
(221) (x4[4] ≥ 0∧x2[4] + [-1] + [-1]x4[4] ≥ 0 ⇒ (UIncreasing(2636_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x0[14], x3[14])), x4[14], x0[14])), ≥)∧[(-1)Bound*bni_129] + [bni_129]x2[4] + [(-1)bni_129]x4[4] ≥ 0∧[(-1)bso_130] ≥ 0)
(222) (x4[4] ≥ 0∧x2[4] + [-1] + [-1]x4[4] ≥ 0 ⇒ (UIncreasing(2636_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x0[14], x3[14])), x4[14], x0[14])), ≥)∧0 = 0∧[(-1)Bound*bni_129] + [bni_129]x2[4] + [(-1)bni_129]x4[4] ≥ 0∧0 = 0∧[(-1)bso_130] ≥ 0)
(223) (x4[4] ≥ 0∧x2[4] ≥ 0 ⇒ (UIncreasing(2636_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x0[14], x3[14])), x4[14], x0[14])), ≥)∧0 = 0∧[(-1)Bound*bni_129 + bni_129] + [bni_129]x2[4] ≥ 0∧0 = 0∧[(-1)bso_130] ≥ 0)
(224) (&&(>=(x4[15], 0), <(x4[15], x2[15]))=TRUE∧java.lang.Object(ARRAY(x2[15], x3[15]))=java.lang.Object(ARRAY(x2[16], x3[16]))∧x4[15]=x4[16]∧java.lang.Object(ARRAY(x2[16], x3[16]))=java.lang.Object(ARRAY(x2[14], x3[14]))∧x4[16]=x4[14]∧x2[16]=x0[14]∧x6[16]=1 ⇒ 2595_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x2[14], x3[14])), x4[14], x0[14], 1)≥NonInfC∧2595_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x2[14], x3[14])), x4[14], x0[14], 1)≥2636_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x0[14], x3[14])), x4[14], x0[14])∧(UIncreasing(2636_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x0[14], x3[14])), x4[14], x0[14])), ≥))
(225) (>=(x4[15], 0)=TRUE∧<(x4[15], x2[15])=TRUE ⇒ 2595_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x2[15], x3[15])), x4[15], x2[15], 1)≥NonInfC∧2595_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x2[15], x3[15])), x4[15], x2[15], 1)≥2636_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x2[15], x3[15])), x4[15], x2[15])∧(UIncreasing(2636_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x0[14], x3[14])), x4[14], x0[14])), ≥))
(226) (x4[15] ≥ 0∧x2[15] + [-1] + [-1]x4[15] ≥ 0 ⇒ (UIncreasing(2636_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x0[14], x3[14])), x4[14], x0[14])), ≥)∧[(-1)Bound*bni_129] + [bni_129]x2[15] + [(-1)bni_129]x4[15] ≥ 0∧[(-1)bso_130] ≥ 0)
(227) (x4[15] ≥ 0∧x2[15] + [-1] + [-1]x4[15] ≥ 0 ⇒ (UIncreasing(2636_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x0[14], x3[14])), x4[14], x0[14])), ≥)∧[(-1)Bound*bni_129] + [bni_129]x2[15] + [(-1)bni_129]x4[15] ≥ 0∧[(-1)bso_130] ≥ 0)
(228) (x4[15] ≥ 0∧x2[15] + [-1] + [-1]x4[15] ≥ 0 ⇒ (UIncreasing(2636_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x0[14], x3[14])), x4[14], x0[14])), ≥)∧[(-1)Bound*bni_129] + [bni_129]x2[15] + [(-1)bni_129]x4[15] ≥ 0∧[(-1)bso_130] ≥ 0)
(229) (x4[15] ≥ 0∧x2[15] + [-1] + [-1]x4[15] ≥ 0 ⇒ (UIncreasing(2636_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x0[14], x3[14])), x4[14], x0[14])), ≥)∧0 = 0∧[(-1)Bound*bni_129] + [bni_129]x2[15] + [(-1)bni_129]x4[15] ≥ 0∧0 = 0∧[(-1)bso_130] ≥ 0)
(230) (x4[15] ≥ 0∧x2[15] ≥ 0 ⇒ (UIncreasing(2636_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x0[14], x3[14])), x4[14], x0[14])), ≥)∧0 = 0∧[(-1)Bound*bni_129 + bni_129] + [bni_129]x2[15] ≥ 0∧0 = 0∧[(-1)bso_130] ≥ 0)
(231) (&&(>=(x4[15], 0), <(x4[15], x2[15]))=TRUE∧java.lang.Object(ARRAY(x2[15], x3[15]))=java.lang.Object(ARRAY(x2[16], x3[16]))∧x4[15]=x4[16] ⇒ 2420_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x2[15], x3[15])), x4[15], 1)≥NonInfC∧2420_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x2[15], x3[15])), x4[15], 1)≥COND_2420_1_MAIN_INVOKEMETHOD2(&&(>=(x4[15], 0), <(x4[15], x2[15])), java.lang.Object(ARRAY(x2[15], x3[15])), x4[15], 1)∧(UIncreasing(COND_2420_1_MAIN_INVOKEMETHOD2(&&(>=(x4[15], 0), <(x4[15], x2[15])), java.lang.Object(ARRAY(x2[15], x3[15])), x4[15], 1)), ≥))
(232) (>=(x4[15], 0)=TRUE∧<(x4[15], x2[15])=TRUE ⇒ 2420_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x2[15], x3[15])), x4[15], 1)≥NonInfC∧2420_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x2[15], x3[15])), x4[15], 1)≥COND_2420_1_MAIN_INVOKEMETHOD2(&&(>=(x4[15], 0), <(x4[15], x2[15])), java.lang.Object(ARRAY(x2[15], x3[15])), x4[15], 1)∧(UIncreasing(COND_2420_1_MAIN_INVOKEMETHOD2(&&(>=(x4[15], 0), <(x4[15], x2[15])), java.lang.Object(ARRAY(x2[15], x3[15])), x4[15], 1)), ≥))
(233) (x4[15] ≥ 0∧x2[15] + [-1] + [-1]x4[15] ≥ 0 ⇒ (UIncreasing(COND_2420_1_MAIN_INVOKEMETHOD2(&&(>=(x4[15], 0), <(x4[15], x2[15])), java.lang.Object(ARRAY(x2[15], x3[15])), x4[15], 1)), ≥)∧[(-1)Bound*bni_131] + [bni_131]x2[15] + [(-1)bni_131]x4[15] ≥ 0∧[(-1)bso_132] ≥ 0)
(234) (x4[15] ≥ 0∧x2[15] + [-1] + [-1]x4[15] ≥ 0 ⇒ (UIncreasing(COND_2420_1_MAIN_INVOKEMETHOD2(&&(>=(x4[15], 0), <(x4[15], x2[15])), java.lang.Object(ARRAY(x2[15], x3[15])), x4[15], 1)), ≥)∧[(-1)Bound*bni_131] + [bni_131]x2[15] + [(-1)bni_131]x4[15] ≥ 0∧[(-1)bso_132] ≥ 0)
(235) (x4[15] ≥ 0∧x2[15] + [-1] + [-1]x4[15] ≥ 0 ⇒ (UIncreasing(COND_2420_1_MAIN_INVOKEMETHOD2(&&(>=(x4[15], 0), <(x4[15], x2[15])), java.lang.Object(ARRAY(x2[15], x3[15])), x4[15], 1)), ≥)∧[(-1)Bound*bni_131] + [bni_131]x2[15] + [(-1)bni_131]x4[15] ≥ 0∧[(-1)bso_132] ≥ 0)
(236) (x4[15] ≥ 0∧x2[15] + [-1] + [-1]x4[15] ≥ 0 ⇒ (UIncreasing(COND_2420_1_MAIN_INVOKEMETHOD2(&&(>=(x4[15], 0), <(x4[15], x2[15])), java.lang.Object(ARRAY(x2[15], x3[15])), x4[15], 1)), ≥)∧0 = 0∧[(-1)Bound*bni_131] + [bni_131]x2[15] + [(-1)bni_131]x4[15] ≥ 0∧0 = 0∧[(-1)bso_132] ≥ 0)
(237) (x4[15] ≥ 0∧x2[15] ≥ 0 ⇒ (UIncreasing(COND_2420_1_MAIN_INVOKEMETHOD2(&&(>=(x4[15], 0), <(x4[15], x2[15])), java.lang.Object(ARRAY(x2[15], x3[15])), x4[15], 1)), ≥)∧0 = 0∧[(-1)Bound*bni_131 + bni_131] + [bni_131]x2[15] ≥ 0∧0 = 0∧[(-1)bso_132] ≥ 0)
(238) (java.lang.Object(ARRAY(x0[0], x3[0]))=java.lang.Object(ARRAY(x2[15], x3[15]))∧x4[0]=x4[15]∧x1[0]=1∧&&(>=(x4[15], 0), <(x4[15], x2[15]))=TRUE∧java.lang.Object(ARRAY(x2[15], x3[15]))=java.lang.Object(ARRAY(x2[16], x3[16]))∧x4[15]=x4[16] ⇒ COND_2420_1_MAIN_INVOKEMETHOD2(TRUE, java.lang.Object(ARRAY(x2[16], x3[16])), x4[16], 1)≥NonInfC∧COND_2420_1_MAIN_INVOKEMETHOD2(TRUE, java.lang.Object(ARRAY(x2[16], x3[16])), x4[16], 1)≥2595_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x2[16], x3[16])), x4[16], x2[16], x6[16])∧(UIncreasing(2595_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x2[16], x3[16])), x4[16], x2[16], x6[16])), ≥))
(239) (>=(x4[15], 0)=TRUE∧<(x4[15], x2[15])=TRUE ⇒ COND_2420_1_MAIN_INVOKEMETHOD2(TRUE, java.lang.Object(ARRAY(x2[15], x3[0])), x4[15], 1)≥NonInfC∧COND_2420_1_MAIN_INVOKEMETHOD2(TRUE, java.lang.Object(ARRAY(x2[15], x3[0])), x4[15], 1)≥2595_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x2[15], x3[0])), x4[15], x2[15], x6[16])∧(UIncreasing(2595_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x2[16], x3[16])), x4[16], x2[16], x6[16])), ≥))
(240) (x4[15] ≥ 0∧x2[15] + [-1] + [-1]x4[15] ≥ 0 ⇒ (UIncreasing(2595_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x2[16], x3[16])), x4[16], x2[16], x6[16])), ≥)∧[(-1)Bound*bni_133] + [(-1)bni_133]x4[15] + [bni_133]x2[15] ≥ 0∧[(-1)bso_134] ≥ 0)
(241) (x4[15] ≥ 0∧x2[15] + [-1] + [-1]x4[15] ≥ 0 ⇒ (UIncreasing(2595_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x2[16], x3[16])), x4[16], x2[16], x6[16])), ≥)∧[(-1)Bound*bni_133] + [(-1)bni_133]x4[15] + [bni_133]x2[15] ≥ 0∧[(-1)bso_134] ≥ 0)
(242) (x4[15] ≥ 0∧x2[15] + [-1] + [-1]x4[15] ≥ 0 ⇒ (UIncreasing(2595_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x2[16], x3[16])), x4[16], x2[16], x6[16])), ≥)∧[(-1)Bound*bni_133] + [(-1)bni_133]x4[15] + [bni_133]x2[15] ≥ 0∧[(-1)bso_134] ≥ 0)
(243) (x4[15] ≥ 0∧x2[15] + [-1] + [-1]x4[15] ≥ 0 ⇒ (UIncreasing(2595_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x2[16], x3[16])), x4[16], x2[16], x6[16])), ≥)∧0 = 0∧[(-1)Bound*bni_133] + [(-1)bni_133]x4[15] + [bni_133]x2[15] ≥ 0∧0 = 0∧[(-1)bso_134] ≥ 0)
(244) (x4[15] ≥ 0∧x2[15] ≥ 0 ⇒ (UIncreasing(2595_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x2[16], x3[16])), x4[16], x2[16], x6[16])), ≥)∧0 = 0∧[(-1)Bound*bni_133 + bni_133] + [bni_133]x2[15] ≥ 0∧0 = 0∧[(-1)bso_134] ≥ 0)
(245) (java.lang.Object(ARRAY(x0[1], x4[1]))=java.lang.Object(ARRAY(x2[15], x3[15]))∧x5[1]=x4[15]∧&&(>=(x4[15], 0), <(x4[15], x2[15]))=TRUE∧java.lang.Object(ARRAY(x2[15], x3[15]))=java.lang.Object(ARRAY(x2[16], x3[16]))∧x4[15]=x4[16] ⇒ COND_2420_1_MAIN_INVOKEMETHOD2(TRUE, java.lang.Object(ARRAY(x2[16], x3[16])), x4[16], 1)≥NonInfC∧COND_2420_1_MAIN_INVOKEMETHOD2(TRUE, java.lang.Object(ARRAY(x2[16], x3[16])), x4[16], 1)≥2595_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x2[16], x3[16])), x4[16], x2[16], x6[16])∧(UIncreasing(2595_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x2[16], x3[16])), x4[16], x2[16], x6[16])), ≥))
(246) (>=(x4[15], 0)=TRUE∧<(x4[15], x2[15])=TRUE ⇒ COND_2420_1_MAIN_INVOKEMETHOD2(TRUE, java.lang.Object(ARRAY(x2[15], x4[1])), x4[15], 1)≥NonInfC∧COND_2420_1_MAIN_INVOKEMETHOD2(TRUE, java.lang.Object(ARRAY(x2[15], x4[1])), x4[15], 1)≥2595_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x2[15], x4[1])), x4[15], x2[15], x6[16])∧(UIncreasing(2595_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x2[16], x3[16])), x4[16], x2[16], x6[16])), ≥))
(247) (x4[15] ≥ 0∧x2[15] + [-1] + [-1]x4[15] ≥ 0 ⇒ (UIncreasing(2595_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x2[16], x3[16])), x4[16], x2[16], x6[16])), ≥)∧[(-1)Bound*bni_133] + [(-1)bni_133]x4[15] + [bni_133]x2[15] ≥ 0∧[(-1)bso_134] ≥ 0)
(248) (x4[15] ≥ 0∧x2[15] + [-1] + [-1]x4[15] ≥ 0 ⇒ (UIncreasing(2595_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x2[16], x3[16])), x4[16], x2[16], x6[16])), ≥)∧[(-1)Bound*bni_133] + [(-1)bni_133]x4[15] + [bni_133]x2[15] ≥ 0∧[(-1)bso_134] ≥ 0)
(249) (x4[15] ≥ 0∧x2[15] + [-1] + [-1]x4[15] ≥ 0 ⇒ (UIncreasing(2595_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x2[16], x3[16])), x4[16], x2[16], x6[16])), ≥)∧[(-1)Bound*bni_133] + [(-1)bni_133]x4[15] + [bni_133]x2[15] ≥ 0∧[(-1)bso_134] ≥ 0)
(250) (x4[15] ≥ 0∧x2[15] + [-1] + [-1]x4[15] ≥ 0 ⇒ (UIncreasing(2595_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x2[16], x3[16])), x4[16], x2[16], x6[16])), ≥)∧0 = 0∧[(-1)Bound*bni_133] + [(-1)bni_133]x4[15] + [bni_133]x2[15] ≥ 0∧0 = 0∧[(-1)bso_134] ≥ 0)
(251) (x4[15] ≥ 0∧x2[15] ≥ 0 ⇒ (UIncreasing(2595_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x2[16], x3[16])), x4[16], x2[16], x6[16])), ≥)∧0 = 0∧[(-1)Bound*bni_133 + bni_133] + [bni_133]x2[15] ≥ 0∧0 = 0∧[(-1)bso_134] ≥ 0)
(252) (java.lang.Object(ARRAY(x0[17], x3[17]))=java.lang.Object(ARRAY(x2[15], x3[15]))∧x4[17]=x4[15]∧x0[17]=1∧&&(>=(x4[15], 0), <(x4[15], x2[15]))=TRUE∧java.lang.Object(ARRAY(x2[15], x3[15]))=java.lang.Object(ARRAY(x2[16], x3[16]))∧x4[15]=x4[16] ⇒ COND_2420_1_MAIN_INVOKEMETHOD2(TRUE, java.lang.Object(ARRAY(x2[16], x3[16])), x4[16], 1)≥NonInfC∧COND_2420_1_MAIN_INVOKEMETHOD2(TRUE, java.lang.Object(ARRAY(x2[16], x3[16])), x4[16], 1)≥2595_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x2[16], x3[16])), x4[16], x2[16], x6[16])∧(UIncreasing(2595_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x2[16], x3[16])), x4[16], x2[16], x6[16])), ≥))
(253) (>=(x4[15], 0)=TRUE∧<(x4[15], 1)=TRUE ⇒ COND_2420_1_MAIN_INVOKEMETHOD2(TRUE, java.lang.Object(ARRAY(1, x3[17])), x4[15], 1)≥NonInfC∧COND_2420_1_MAIN_INVOKEMETHOD2(TRUE, java.lang.Object(ARRAY(1, x3[17])), x4[15], 1)≥2595_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(1, x3[17])), x4[15], 1, x6[16])∧(UIncreasing(2595_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x2[16], x3[16])), x4[16], x2[16], x6[16])), ≥))
(254) (x4[15] ≥ 0∧[-1]x4[15] ≥ 0 ⇒ (UIncreasing(2595_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x2[16], x3[16])), x4[16], x2[16], x6[16])), ≥)∧[bni_133 + (-1)Bound*bni_133] + [(-1)bni_133]x4[15] ≥ 0∧[(-1)bso_134] ≥ 0)
(255) (x4[15] ≥ 0∧[-1]x4[15] ≥ 0 ⇒ (UIncreasing(2595_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x2[16], x3[16])), x4[16], x2[16], x6[16])), ≥)∧[bni_133 + (-1)Bound*bni_133] + [(-1)bni_133]x4[15] ≥ 0∧[(-1)bso_134] ≥ 0)
(256) (x4[15] ≥ 0∧[-1]x4[15] ≥ 0 ⇒ (UIncreasing(2595_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x2[16], x3[16])), x4[16], x2[16], x6[16])), ≥)∧[bni_133 + (-1)Bound*bni_133] + [(-1)bni_133]x4[15] ≥ 0∧[(-1)bso_134] ≥ 0)
(257) (x4[15] ≥ 0∧[-1]x4[15] ≥ 0 ⇒ (UIncreasing(2595_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x2[16], x3[16])), x4[16], x2[16], x6[16])), ≥)∧0 = 0∧[bni_133 + (-1)Bound*bni_133] + [(-1)bni_133]x4[15] ≥ 0∧0 = 0∧[(-1)bso_134] ≥ 0)
(258) (0 ≥ 0∧0 ≥ 0 ⇒ (UIncreasing(2595_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x2[16], x3[16])), x4[16], x2[16], x6[16])), ≥)∧0 = 0∧[bni_133 + (-1)Bound*bni_133] ≥ 0∧0 = 0∧[(-1)bso_134] ≥ 0)
(259) (&&(&&(>=(x3[8], 0), >(x1[8], +(x3[8], 1))), <=(0, +(x3[8], 1)))=TRUE∧java.lang.Object(ARRAY(x1[8], x2[8]))=java.lang.Object(ARRAY(x1[9], x2[9]))∧x3[8]=x3[9]∧x4[8]=x4[9]∧java.lang.Object(ARRAY(x1[9], x2[9]))=java.lang.Object(ARRAY(x2[17], x3[17]))∧+(x3[9], 1)=x4[17]∧x1[9]=x0[17]∧x5[9]=1 ⇒ 2387_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x2[17], x3[17])), x4[17], x0[17], 1)≥NonInfC∧2387_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x2[17], x3[17])), x4[17], x0[17], 1)≥2420_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x0[17], x3[17])), x4[17], x0[17])∧(UIncreasing(2420_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x0[17], x3[17])), x4[17], x0[17])), ≥))
(260) (<=(0, +(x3[8], 1))=TRUE∧>=(x3[8], 0)=TRUE∧>(x1[8], +(x3[8], 1))=TRUE ⇒ 2387_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x1[8], x2[8])), +(x3[8], 1), x1[8], 1)≥NonInfC∧2387_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x1[8], x2[8])), +(x3[8], 1), x1[8], 1)≥2420_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x1[8], x2[8])), +(x3[8], 1), x1[8])∧(UIncreasing(2420_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x0[17], x3[17])), x4[17], x0[17])), ≥))
(261) (x3[8] + [1] ≥ 0∧x3[8] ≥ 0∧x1[8] + [-2] + [-1]x3[8] ≥ 0 ⇒ (UIncreasing(2420_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x0[17], x3[17])), x4[17], x0[17])), ≥)∧[(-1)Bound*bni_135] + [bni_135]x1[8] + [(-1)bni_135]x3[8] ≥ 0∧[1 + (-1)bso_136] ≥ 0)
(262) (x3[8] + [1] ≥ 0∧x3[8] ≥ 0∧x1[8] + [-2] + [-1]x3[8] ≥ 0 ⇒ (UIncreasing(2420_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x0[17], x3[17])), x4[17], x0[17])), ≥)∧[(-1)Bound*bni_135] + [bni_135]x1[8] + [(-1)bni_135]x3[8] ≥ 0∧[1 + (-1)bso_136] ≥ 0)
(263) (x3[8] + [1] ≥ 0∧x3[8] ≥ 0∧x1[8] + [-2] + [-1]x3[8] ≥ 0 ⇒ (UIncreasing(2420_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x0[17], x3[17])), x4[17], x0[17])), ≥)∧[(-1)Bound*bni_135] + [bni_135]x1[8] + [(-1)bni_135]x3[8] ≥ 0∧[1 + (-1)bso_136] ≥ 0)
(264) (x3[8] + [1] ≥ 0∧x3[8] ≥ 0∧x1[8] + [-2] + [-1]x3[8] ≥ 0 ⇒ (UIncreasing(2420_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x0[17], x3[17])), x4[17], x0[17])), ≥)∧0 = 0∧[(-1)Bound*bni_135] + [bni_135]x1[8] + [(-1)bni_135]x3[8] ≥ 0∧0 = 0∧[1 + (-1)bso_136] ≥ 0)
(265) (x3[8] + [1] ≥ 0∧x3[8] ≥ 0∧x1[8] ≥ 0 ⇒ (UIncreasing(2420_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x0[17], x3[17])), x4[17], x0[17])), ≥)∧0 = 0∧[(-1)Bound*bni_135 + (2)bni_135] + [bni_135]x1[8] ≥ 0∧0 = 0∧[1 + (-1)bso_136] ≥ 0)
(266) (&&(&&(>=(x3[10], 0), >(x1[10], +(x3[10], 1))), <=(0, +(x3[10], 1)))=TRUE∧java.lang.Object(ARRAY(x1[10], x2[10]))=java.lang.Object(ARRAY(x1[11], x2[11]))∧x3[10]=x3[11]∧java.lang.Object(ARRAY(x1[11], x2[11]))=java.lang.Object(ARRAY(x2[17], x3[17]))∧+(x3[11], 1)=x4[17]∧x1[11]=x0[17]∧x5[11]=1 ⇒ 2387_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x2[17], x3[17])), x4[17], x0[17], 1)≥NonInfC∧2387_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x2[17], x3[17])), x4[17], x0[17], 1)≥2420_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x0[17], x3[17])), x4[17], x0[17])∧(UIncreasing(2420_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x0[17], x3[17])), x4[17], x0[17])), ≥))
(267) (<=(0, +(x3[10], 1))=TRUE∧>=(x3[10], 0)=TRUE∧>(x1[10], +(x3[10], 1))=TRUE ⇒ 2387_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x1[10], x2[10])), +(x3[10], 1), x1[10], 1)≥NonInfC∧2387_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x1[10], x2[10])), +(x3[10], 1), x1[10], 1)≥2420_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x1[10], x2[10])), +(x3[10], 1), x1[10])∧(UIncreasing(2420_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x0[17], x3[17])), x4[17], x0[17])), ≥))
(268) (x3[10] + [1] ≥ 0∧x3[10] ≥ 0∧x1[10] + [-2] + [-1]x3[10] ≥ 0 ⇒ (UIncreasing(2420_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x0[17], x3[17])), x4[17], x0[17])), ≥)∧[(-1)Bound*bni_135] + [bni_135]x1[10] + [(-1)bni_135]x3[10] ≥ 0∧[1 + (-1)bso_136] ≥ 0)
(269) (x3[10] + [1] ≥ 0∧x3[10] ≥ 0∧x1[10] + [-2] + [-1]x3[10] ≥ 0 ⇒ (UIncreasing(2420_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x0[17], x3[17])), x4[17], x0[17])), ≥)∧[(-1)Bound*bni_135] + [bni_135]x1[10] + [(-1)bni_135]x3[10] ≥ 0∧[1 + (-1)bso_136] ≥ 0)
(270) (x3[10] + [1] ≥ 0∧x3[10] ≥ 0∧x1[10] + [-2] + [-1]x3[10] ≥ 0 ⇒ (UIncreasing(2420_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x0[17], x3[17])), x4[17], x0[17])), ≥)∧[(-1)Bound*bni_135] + [bni_135]x1[10] + [(-1)bni_135]x3[10] ≥ 0∧[1 + (-1)bso_136] ≥ 0)
(271) (x3[10] + [1] ≥ 0∧x3[10] ≥ 0∧x1[10] + [-2] + [-1]x3[10] ≥ 0 ⇒ (UIncreasing(2420_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x0[17], x3[17])), x4[17], x0[17])), ≥)∧0 = 0∧[(-1)Bound*bni_135] + [bni_135]x1[10] + [(-1)bni_135]x3[10] ≥ 0∧0 = 0∧[1 + (-1)bso_136] ≥ 0)
(272) (x3[10] + [1] ≥ 0∧x3[10] ≥ 0∧x1[10] ≥ 0 ⇒ (UIncreasing(2420_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x0[17], x3[17])), x4[17], x0[17])), ≥)∧0 = 0∧[(-1)Bound*bni_135 + (2)bni_135] + [bni_135]x1[10] ≥ 0∧0 = 0∧[1 + (-1)bso_136] ≥ 0)
(273) (&&(&&(>=(x4[12], 0), >(x2[12], +(x4[12], 1))), <=(0, +(x4[12], 1)))=TRUE∧java.lang.Object(ARRAY(x2[12], x3[12]))=java.lang.Object(ARRAY(x2[13], x3[13]))∧x4[12]=x4[13]∧java.lang.Object(ARRAY(x2[13], x3[13]))=java.lang.Object(ARRAY(x2[17], x3[17]))∧+(x4[13], 1)=x4[17]∧x2[13]=x0[17]∧x6[13]=1 ⇒ 2387_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x2[17], x3[17])), x4[17], x0[17], 1)≥NonInfC∧2387_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x2[17], x3[17])), x4[17], x0[17], 1)≥2420_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x0[17], x3[17])), x4[17], x0[17])∧(UIncreasing(2420_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x0[17], x3[17])), x4[17], x0[17])), ≥))
(274) (<=(0, +(x4[12], 1))=TRUE∧>=(x4[12], 0)=TRUE∧>(x2[12], +(x4[12], 1))=TRUE ⇒ 2387_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x2[12], x3[12])), +(x4[12], 1), x2[12], 1)≥NonInfC∧2387_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x2[12], x3[12])), +(x4[12], 1), x2[12], 1)≥2420_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x2[12], x3[12])), +(x4[12], 1), x2[12])∧(UIncreasing(2420_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x0[17], x3[17])), x4[17], x0[17])), ≥))
(275) (x4[12] + [1] ≥ 0∧x4[12] ≥ 0∧x2[12] + [-2] + [-1]x4[12] ≥ 0 ⇒ (UIncreasing(2420_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x0[17], x3[17])), x4[17], x0[17])), ≥)∧[(-1)Bound*bni_135] + [bni_135]x2[12] + [(-1)bni_135]x4[12] ≥ 0∧[1 + (-1)bso_136] ≥ 0)
(276) (x4[12] + [1] ≥ 0∧x4[12] ≥ 0∧x2[12] + [-2] + [-1]x4[12] ≥ 0 ⇒ (UIncreasing(2420_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x0[17], x3[17])), x4[17], x0[17])), ≥)∧[(-1)Bound*bni_135] + [bni_135]x2[12] + [(-1)bni_135]x4[12] ≥ 0∧[1 + (-1)bso_136] ≥ 0)
(277) (x4[12] + [1] ≥ 0∧x4[12] ≥ 0∧x2[12] + [-2] + [-1]x4[12] ≥ 0 ⇒ (UIncreasing(2420_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x0[17], x3[17])), x4[17], x0[17])), ≥)∧[(-1)Bound*bni_135] + [bni_135]x2[12] + [(-1)bni_135]x4[12] ≥ 0∧[1 + (-1)bso_136] ≥ 0)
(278) (x4[12] + [1] ≥ 0∧x4[12] ≥ 0∧x2[12] + [-2] + [-1]x4[12] ≥ 0 ⇒ (UIncreasing(2420_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x0[17], x3[17])), x4[17], x0[17])), ≥)∧0 = 0∧[(-1)Bound*bni_135] + [bni_135]x2[12] + [(-1)bni_135]x4[12] ≥ 0∧0 = 0∧[1 + (-1)bso_136] ≥ 0)
(279) (x4[12] + [1] ≥ 0∧x4[12] ≥ 0∧x2[12] ≥ 0 ⇒ (UIncreasing(2420_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x0[17], x3[17])), x4[17], x0[17])), ≥)∧0 = 0∧[(-1)Bound*bni_135 + (2)bni_135] + [bni_135]x2[12] ≥ 0∧0 = 0∧[1 + (-1)bso_136] ≥ 0)
POL(TRUE) = 0
POL(FALSE) = 0
POL(2387_0_power_Load(x1, x2)) = [-1] + x2
POL(730_0_power_GT(x1, x2)) = [-1] + x1 + x2
POL(2420_0_even_Load(x1)) = [-1]
POL(1300_0_odd_GT(x1)) = [-1] + x1
POL(2636_0_odd_Load(x1)) = [-1]
POL(Cond_1300_0_odd_GT(x1, x2)) = [-1] + x2
POL(<=(x1, x2)) = [-1]
POL(0) = 0
POL(1347_0_odd_Return) = [-1]
POL(1) = [1]
POL(Cond_1300_0_odd_GT1(x1, x2)) = [-1]
POL(>(x1, x2)) = [-1]
POL(1372_0_odd_Return) = [-1]
POL(Cond_1300_0_odd_GT2(x1, x2)) = [-1] + x2
POL(&&(x1, x2)) = [-1]
POL(!(x1)) = [-1]
POL(=(x1, x2)) = [-1]
POL(1401_1_odd_InvokeMethod(x1, x2)) = [-1] + x1 + x2
POL(1406_0_even_Return(x1)) = x1
POL(-(x1, x2)) = x1 + [-1]x2
POL(Cond_1300_0_odd_GT3(x1, x2)) = [-1] + x2
POL(1224_0_even_Return(x1)) = [-1] + x1
POL(1422_0_odd_Return(x1)) = [-1] + x1
POL(1067_0_even_Return) = [-1]
POL(Cond_924_0_even_GT(x1, x2)) = [-1] + x2
POL(980_0_even_Return) = [-1]
POL(Cond_924_0_even_GT1(x1, x2)) = [-1]
POL(Cond_924_0_even_GT2(x1, x2)) = [-1] + x2
POL(1172_1_even_InvokeMethod(x1, x2)) = [-1] + x1 + x2
POL(1353_0_odd_Return(x1)) = x1
POL(Cond_924_0_even_GT3(x1, x2)) = [-1] + x2
POL(763_0_power_Return(x1)) = [-1] + x1
POL(Cond_730_0_power_GT(x1, x2, x3)) = [-1] + x2
POL(845_0_power_Return(x1)) = [-1] + x1
POL(Cond_730_0_power_GT1(x1, x2, x3)) = [-1] + x2 + x3
POL(2) = [2]
POL(955_1_power_InvokeMethod(x1, x2, x3, x4, x5)) = [-1] + [-1]x1 + x3 + x2 + x4 + x5
POL(960_0_power_Return(x1)) = x1
POL(*(x1, x2)) = x1·x2
POL(Cond_730_0_power_GT2(x1, x2, x3)) = [-1] + x2 + x3
POL(1072_0_power_NE(x1, x2, x3)) = [-1] + x2 + x1 + x3
POL(1188_0_power_Return(x1, x2)) = [-1] + x2 + x1
POL(1287_0_power_Return(x1)) = [-1] + x1
POL(Cond_1072_0_power_NE(x1, x2, x3, x4)) = [-1] + x2 + x3 + x4
POL(2387_1_MAIN_INVOKEMETHOD(x1, x2, x3, x4)) = [-1]x2 + [-1]x1
POL(java.lang.Object(x1)) = x1
POL(ARRAY(x1, x2)) = [-1] + [-1]x1
POL(2420_1_MAIN_INVOKEMETHOD(x1, x2, x3)) = [-1] + [-1]x1 + [-1]x2
POL(COND_2420_1_MAIN_INVOKEMETHOD(x1, x2, x3, x4)) = [-1] + [-1]x3 + [-1]x2
POL(>=(x1, x2)) = [-1]
POL(<(x1, x2)) = [-1]
POL(2595_1_MAIN_INVOKEMETHOD(x1, x2, x3, x4)) = [-1] + [-1]x2 + [-1]x1
POL(COND_2420_1_MAIN_INVOKEMETHOD1(x1, x2, x3, x4)) = [-1] + [-1]x3 + [-1]x2
POL(2636_1_MAIN_INVOKEMETHOD(x1, x2, x3)) = [-1] + [-1]x1 + [-1]x2
POL(COND_2636_1_MAIN_INVOKEMETHOD(x1, x2, x3, x4)) = [-1] + [-1]x3 + [-1]x2
POL(+(x1, x2)) = x1 + x2
POL(COND_2636_1_MAIN_INVOKEMETHOD1(x1, x2, x3, x4)) = [-1] + [-1]x3 + [-1]x2
POL(COND_2636_1_MAIN_INVOKEMETHOD2(x1, x2, x3, x4)) = [-1] + [-1]x3 + [-1]x2
POL(COND_2420_1_MAIN_INVOKEMETHOD2(x1, x2, x3, x4)) = [-1] + [-1]x3 + [-1]x2
2387_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x2[0], x3[0])), x4[0], x0[0], x5[0]) → 2420_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x0[0], x3[0])), x4[0], x1[0])
2387_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x3[1], x4[1])), x5[1], x0[1], 0) → 2420_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x0[1], x4[1])), x5[1], 1)
2387_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x2[17], x3[17])), x4[17], x0[17], 1) → 2420_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x0[17], x3[17])), x4[17], x0[17])
2387_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x2[0], x3[0])), x4[0], x0[0], x5[0]) → 2420_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x0[0], x3[0])), x4[0], x1[0])
2387_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x3[1], x4[1])), x5[1], x0[1], 0) → 2420_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x0[1], x4[1])), x5[1], 1)
2420_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x1[2], x2[2])), x3[2], x4[2]) → COND_2420_1_MAIN_INVOKEMETHOD(&&(>=(x3[2], 0), <(x3[2], x1[2])), java.lang.Object(ARRAY(x1[2], x2[2])), x3[2], x4[2])
COND_2420_1_MAIN_INVOKEMETHOD(TRUE, java.lang.Object(ARRAY(x1[3], x2[3])), x3[3], x4[3]) → 2595_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x1[3], x2[3])), x3[3], x1[3], x5[3])
2420_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x2[4], x3[4])), x4[4], 0) → COND_2420_1_MAIN_INVOKEMETHOD1(&&(>=(x4[4], 0), <(x4[4], x2[4])), java.lang.Object(ARRAY(x2[4], x3[4])), x4[4], 0)
COND_2420_1_MAIN_INVOKEMETHOD1(TRUE, java.lang.Object(ARRAY(x2[5], x3[5])), x4[5], 0) → 2595_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x2[5], x3[5])), x4[5], x2[5], x6[5])
2595_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x2[6], x3[6])), x4[6], x0[6], x5[6]) → 2636_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x0[6], x3[6])), x4[6], x1[6])
2595_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x3[7], x4[7])), x5[7], x0[7], 0) → 2636_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x0[7], x4[7])), x5[7], 1)
2636_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x1[8], x2[8])), x3[8], x4[8]) → COND_2636_1_MAIN_INVOKEMETHOD(&&(&&(>=(x3[8], 0), >(x1[8], +(x3[8], 1))), <=(0, +(x3[8], 1))), java.lang.Object(ARRAY(x1[8], x2[8])), x3[8], x4[8])
COND_2636_1_MAIN_INVOKEMETHOD(TRUE, java.lang.Object(ARRAY(x1[9], x2[9])), x3[9], x4[9]) → 2387_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x1[9], x2[9])), +(x3[9], 1), x1[9], x5[9])
2636_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x1[10], x2[10])), x3[10], 0) → COND_2636_1_MAIN_INVOKEMETHOD1(&&(&&(>=(x3[10], 0), >(x1[10], +(x3[10], 1))), <=(0, +(x3[10], 1))), java.lang.Object(ARRAY(x1[10], x2[10])), x3[10], 0)
COND_2636_1_MAIN_INVOKEMETHOD1(TRUE, java.lang.Object(ARRAY(x1[11], x2[11])), x3[11], 0) → 2387_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x1[11], x2[11])), +(x3[11], 1), x1[11], x5[11])
2636_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x2[12], x3[12])), x4[12], 1) → COND_2636_1_MAIN_INVOKEMETHOD2(&&(&&(>=(x4[12], 0), >(x2[12], +(x4[12], 1))), <=(0, +(x4[12], 1))), java.lang.Object(ARRAY(x2[12], x3[12])), x4[12], 1)
COND_2636_1_MAIN_INVOKEMETHOD2(TRUE, java.lang.Object(ARRAY(x2[13], x3[13])), x4[13], 1) → 2387_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x2[13], x3[13])), +(x4[13], 1), x2[13], x6[13])
2595_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x2[14], x3[14])), x4[14], x0[14], 1) → 2636_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x0[14], x3[14])), x4[14], x0[14])
2420_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x2[15], x3[15])), x4[15], 1) → COND_2420_1_MAIN_INVOKEMETHOD2(&&(>=(x4[15], 0), <(x4[15], x2[15])), java.lang.Object(ARRAY(x2[15], x3[15])), x4[15], 1)
COND_2420_1_MAIN_INVOKEMETHOD2(TRUE, java.lang.Object(ARRAY(x2[16], x3[16])), x4[16], 1) → 2595_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x2[16], x3[16])), x4[16], x2[16], x6[16])
2387_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x2[17], x3[17])), x4[17], x0[17], 1) → 2420_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x0[17], x3[17])), x4[17], x0[17])
2420_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x1[2], x2[2])), x3[2], x4[2]) → COND_2420_1_MAIN_INVOKEMETHOD(&&(>=(x3[2], 0), <(x3[2], x1[2])), java.lang.Object(ARRAY(x1[2], x2[2])), x3[2], x4[2])
COND_2420_1_MAIN_INVOKEMETHOD(TRUE, java.lang.Object(ARRAY(x1[3], x2[3])), x3[3], x4[3]) → 2595_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x1[3], x2[3])), x3[3], x1[3], x5[3])
2420_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x2[4], x3[4])), x4[4], 0) → COND_2420_1_MAIN_INVOKEMETHOD1(&&(>=(x4[4], 0), <(x4[4], x2[4])), java.lang.Object(ARRAY(x2[4], x3[4])), x4[4], 0)
COND_2420_1_MAIN_INVOKEMETHOD1(TRUE, java.lang.Object(ARRAY(x2[5], x3[5])), x4[5], 0) → 2595_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x2[5], x3[5])), x4[5], x2[5], x6[5])
2595_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x2[6], x3[6])), x4[6], x0[6], x5[6]) → 2636_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x0[6], x3[6])), x4[6], x1[6])
2595_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x3[7], x4[7])), x5[7], x0[7], 0) → 2636_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x0[7], x4[7])), x5[7], 1)
2636_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x1[8], x2[8])), x3[8], x4[8]) → COND_2636_1_MAIN_INVOKEMETHOD(&&(&&(>=(x3[8], 0), >(x1[8], +(x3[8], 1))), <=(0, +(x3[8], 1))), java.lang.Object(ARRAY(x1[8], x2[8])), x3[8], x4[8])
COND_2636_1_MAIN_INVOKEMETHOD(TRUE, java.lang.Object(ARRAY(x1[9], x2[9])), x3[9], x4[9]) → 2387_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x1[9], x2[9])), +(x3[9], 1), x1[9], x5[9])
2636_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x1[10], x2[10])), x3[10], 0) → COND_2636_1_MAIN_INVOKEMETHOD1(&&(&&(>=(x3[10], 0), >(x1[10], +(x3[10], 1))), <=(0, +(x3[10], 1))), java.lang.Object(ARRAY(x1[10], x2[10])), x3[10], 0)
COND_2636_1_MAIN_INVOKEMETHOD1(TRUE, java.lang.Object(ARRAY(x1[11], x2[11])), x3[11], 0) → 2387_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x1[11], x2[11])), +(x3[11], 1), x1[11], x5[11])
2636_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x2[12], x3[12])), x4[12], 1) → COND_2636_1_MAIN_INVOKEMETHOD2(&&(&&(>=(x4[12], 0), >(x2[12], +(x4[12], 1))), <=(0, +(x4[12], 1))), java.lang.Object(ARRAY(x2[12], x3[12])), x4[12], 1)
COND_2636_1_MAIN_INVOKEMETHOD2(TRUE, java.lang.Object(ARRAY(x2[13], x3[13])), x4[13], 1) → 2387_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x2[13], x3[13])), +(x4[13], 1), x2[13], x6[13])
2595_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x2[14], x3[14])), x4[14], x0[14], 1) → 2636_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x0[14], x3[14])), x4[14], x0[14])
2420_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x2[15], x3[15])), x4[15], 1) → COND_2420_1_MAIN_INVOKEMETHOD2(&&(>=(x4[15], 0), <(x4[15], x2[15])), java.lang.Object(ARRAY(x2[15], x3[15])), x4[15], 1)
COND_2420_1_MAIN_INVOKEMETHOD2(TRUE, java.lang.Object(ARRAY(x2[16], x3[16])), x4[16], 1) → 2595_1_MAIN_INVOKEMETHOD(java.lang.Object(ARRAY(x2[16], x3[16])), x4[16], x2[16], x6[16])
!= | ~ | Neq: (Integer, Integer) -> Boolean |
* | ~ | Mul: (Integer, Integer) -> Integer |
>= | ~ | Ge: (Integer, Integer) -> Boolean |
-1 | ~ | UnaryMinus: (Integer) -> Integer |
| | ~ | Bwor: (Integer, Integer) -> Integer |
/ | ~ | Div: (Integer, Integer) -> Integer |
= | ~ | Eq: (Integer, Integer) -> Boolean |
~ | Bwxor: (Integer, Integer) -> Integer | |
|| | ~ | Lor: (Boolean, Boolean) -> Boolean |
! | ~ | Lnot: (Boolean) -> Boolean |
< | ~ | Lt: (Integer, Integer) -> Boolean |
- | ~ | Sub: (Integer, Integer) -> Integer |
<= | ~ | Le: (Integer, Integer) -> Boolean |
> | ~ | Gt: (Integer, Integer) -> Boolean |
~ | ~ | Bwnot: (Integer) -> Integer |
% | ~ | Mod: (Integer, Integer) -> Integer |
& | ~ | Bwand: (Integer, Integer) -> Integer |
+ | ~ | Add: (Integer, Integer) -> Integer |
&& | ~ | Land: (Boolean, Boolean) -> Boolean |
Integer, Boolean
(2) -> (3), if ((x3[2] >= 0 && x3[2] < x1[2] →* TRUE)∧(java.lang.Object(ARRAY(x1[2], x2[2])) →* java.lang.Object(ARRAY(x1[3], x2[3])))∧(x3[2] →* x3[3])∧(x4[2] →* x4[3]))
(4) -> (5), if ((x4[4] >= 0 && x4[4] < x2[4] →* TRUE)∧(java.lang.Object(ARRAY(x2[4], x3[4])) →* java.lang.Object(ARRAY(x2[5], x3[5])))∧(x4[4] →* x4[5]))
(3) -> (6), if ((java.lang.Object(ARRAY(x1[3], x2[3])) →* java.lang.Object(ARRAY(x2[6], x3[6])))∧(x3[3] →* x4[6])∧(x1[3] →* x0[6])∧(x5[3] →* x5[6]))
(5) -> (6), if ((java.lang.Object(ARRAY(x2[5], x3[5])) →* java.lang.Object(ARRAY(x2[6], x3[6])))∧(x4[5] →* x4[6])∧(x2[5] →* x0[6])∧(x6[5] →* x5[6]))
(16) -> (6), if ((java.lang.Object(ARRAY(x2[16], x3[16])) →* java.lang.Object(ARRAY(x2[6], x3[6])))∧(x4[16] →* x4[6])∧(x2[16] →* x0[6])∧(x6[16] →* x5[6]))
(3) -> (7), if ((java.lang.Object(ARRAY(x1[3], x2[3])) →* java.lang.Object(ARRAY(x3[7], x4[7])))∧(x3[3] →* x5[7])∧(x1[3] →* x0[7])∧(x5[3] →* 0))
(5) -> (7), if ((java.lang.Object(ARRAY(x2[5], x3[5])) →* java.lang.Object(ARRAY(x3[7], x4[7])))∧(x4[5] →* x5[7])∧(x2[5] →* x0[7])∧(x6[5] →* 0))
(16) -> (7), if ((java.lang.Object(ARRAY(x2[16], x3[16])) →* java.lang.Object(ARRAY(x3[7], x4[7])))∧(x4[16] →* x5[7])∧(x2[16] →* x0[7])∧(x6[16] →* 0))
(6) -> (8), if ((java.lang.Object(ARRAY(x0[6], x3[6])) →* java.lang.Object(ARRAY(x1[8], x2[8])))∧(x4[6] →* x3[8])∧(x1[6] →* x4[8]))
(7) -> (8), if ((java.lang.Object(ARRAY(x0[7], x4[7])) →* java.lang.Object(ARRAY(x1[8], x2[8])))∧(x5[7] →* x3[8])∧(1 →* x4[8]))
(14) -> (8), if ((java.lang.Object(ARRAY(x0[14], x3[14])) →* java.lang.Object(ARRAY(x1[8], x2[8])))∧(x4[14] →* x3[8])∧(x0[14] →* x4[8]))
(8) -> (9), if ((x3[8] >= 0 && x1[8] > x3[8] + 1 && 0 <= x3[8] + 1 →* TRUE)∧(java.lang.Object(ARRAY(x1[8], x2[8])) →* java.lang.Object(ARRAY(x1[9], x2[9])))∧(x3[8] →* x3[9])∧(x4[8] →* x4[9]))
(6) -> (10), if ((java.lang.Object(ARRAY(x0[6], x3[6])) →* java.lang.Object(ARRAY(x1[10], x2[10])))∧(x4[6] →* x3[10])∧(x1[6] →* 0))
(7) -> (10), if ((java.lang.Object(ARRAY(x0[7], x4[7])) →* java.lang.Object(ARRAY(x1[10], x2[10])))∧(x5[7] →* x3[10])∧(1 →* 0))
(14) -> (10), if ((java.lang.Object(ARRAY(x0[14], x3[14])) →* java.lang.Object(ARRAY(x1[10], x2[10])))∧(x4[14] →* x3[10])∧(x0[14] →* 0))
(10) -> (11), if ((x3[10] >= 0 && x1[10] > x3[10] + 1 && 0 <= x3[10] + 1 →* TRUE)∧(java.lang.Object(ARRAY(x1[10], x2[10])) →* java.lang.Object(ARRAY(x1[11], x2[11])))∧(x3[10] →* x3[11]))
(6) -> (12), if ((java.lang.Object(ARRAY(x0[6], x3[6])) →* java.lang.Object(ARRAY(x2[12], x3[12])))∧(x4[6] →* x4[12])∧(x1[6] →* 1))
(7) -> (12), if ((java.lang.Object(ARRAY(x0[7], x4[7])) →* java.lang.Object(ARRAY(x2[12], x3[12])))∧(x5[7] →* x4[12]))
(14) -> (12), if ((java.lang.Object(ARRAY(x0[14], x3[14])) →* java.lang.Object(ARRAY(x2[12], x3[12])))∧(x4[14] →* x4[12])∧(x0[14] →* 1))
(12) -> (13), if ((x4[12] >= 0 && x2[12] > x4[12] + 1 && 0 <= x4[12] + 1 →* TRUE)∧(java.lang.Object(ARRAY(x2[12], x3[12])) →* java.lang.Object(ARRAY(x2[13], x3[13])))∧(x4[12] →* x4[13]))
(3) -> (14), if ((java.lang.Object(ARRAY(x1[3], x2[3])) →* java.lang.Object(ARRAY(x2[14], x3[14])))∧(x3[3] →* x4[14])∧(x1[3] →* x0[14])∧(x5[3] →* 1))
(5) -> (14), if ((java.lang.Object(ARRAY(x2[5], x3[5])) →* java.lang.Object(ARRAY(x2[14], x3[14])))∧(x4[5] →* x4[14])∧(x2[5] →* x0[14])∧(x6[5] →* 1))
(16) -> (14), if ((java.lang.Object(ARRAY(x2[16], x3[16])) →* java.lang.Object(ARRAY(x2[14], x3[14])))∧(x4[16] →* x4[14])∧(x2[16] →* x0[14])∧(x6[16] →* 1))
(15) -> (16), if ((x4[15] >= 0 && x4[15] < x2[15] →* TRUE)∧(java.lang.Object(ARRAY(x2[15], x3[15])) →* java.lang.Object(ARRAY(x2[16], x3[16])))∧(x4[15] →* x4[16]))