0 JBC
↳1 JBC2FIG (⇒)
↳2 JBCTerminationGraph
↳3 FIGtoITRSProof (⇒)
↳4 AND
↳5 IDP
↳6 IDPNonInfProof (⇒)
↳7 IDP
↳8 IDependencyGraphProof (⇔)
↳9 TRUE
↳10 IDP
↳11 IDPtoQDPProof (⇒)
↳12 QDP
↳13 UsableRulesProof (⇔)
↳14 QDP
↳15 QReductionProof (⇔)
↳16 QDP
↳17 QDPSizeChangeProof (⇔)
↳18 YES
↳19 IDP
↳20 IDPNonInfProof (⇒)
↳21 AND
↳22 IDP
↳23 IDependencyGraphProof (⇔)
↳24 IDP
↳25 UsableRulesProof (⇔)
↳26 IDP
↳27 IDPNonInfProof (⇒)
↳28 AND
↳29 IDP
↳30 IDependencyGraphProof (⇔)
↳31 TRUE
↳32 IDP
↳33 IDependencyGraphProof (⇔)
↳34 TRUE
↳35 IDP
↳36 IDependencyGraphProof (⇔)
↳37 TRUE
↳38 IDP
↳39 IDPNonInfProof (⇒)
↳40 IDP
↳41 IDependencyGraphProof (⇔)
↳42 TRUE
↳43 IDP
↳44 IDPNonInfProof (⇒)
↳45 IDP
↳46 IDependencyGraphProof (⇔)
↳47 TRUE
↳48 IDP
↳49 IDPNonInfProof (⇒)
↳50 IDP
↳51 IDependencyGraphProof (⇔)
↳52 TRUE
public class Test8 {
public static void main(String[] args) {
List[] ls = { List.mk(args.length), List.mk(args.length), List.mk(args.length) };
test(ls, ls.length - 1);
}
private static void test(List[] ls, int start) {
if (start >= 0) {
int len = length(ls[start]);
for (int i = 0; i < len; i++)
bubble(ls[start]);
test(ls, start - 1);
}
}
private static void bubble(List l) {
if (l == null || l.getTail() == null)
return;
if (l.head > l.getTail().head) {
int temp = l.head;
l.head = l.getTail().head;
l.getTail().head = temp;
}
bubble(l.getTail());
}
private static int length(List list) {
if (list == null)
return 0;
else
return 1 + length(list.getTail());
}
}
public class List {
public int head;
private List tail;
public List(int head, List tail) {
this.head = head;
this.tail = tail;
}
public List getTail() {
return tail;
}
public static List mk(int len) {
List result = null;
while (len-- > 0)
result = new List(len, result);
return result;
}
}
Generated 196 rules for P and 114 rules for R.
Combined rules. Obtained 8 rules for P and 49 rules for R.
Filtered ground terms:
4340_0_bubble_NULL(x1, x2, x3) → 4340_0_bubble_NULL(x2, x3)
Cond_4340_0_bubble_NULL7(x1, x2, x3, x4) → Cond_4340_0_bubble_NULL7(x1, x3, x4)
Cond_4340_0_bubble_NULL6(x1, x2, x3, x4) → Cond_4340_0_bubble_NULL6(x1, x3, x4)
Cond_4340_0_bubble_NULL5(x1, x2, x3, x4) → Cond_4340_0_bubble_NULL5(x1, x3, x4)
Cond_4340_0_bubble_NULL4(x1, x2, x3, x4) → Cond_4340_0_bubble_NULL4(x1, x3, x4)
Cond_4340_0_bubble_NULL3(x1, x2, x3, x4) → Cond_4340_0_bubble_NULL3(x1, x3, x4)
Cond_4340_0_bubble_NULL2(x1, x2, x3, x4) → Cond_4340_0_bubble_NULL2(x1, x3, x4)
Cond_4340_0_bubble_NULL1(x1, x2, x3, x4) → Cond_4340_0_bubble_NULL1(x1, x3, x4)
Cond_4340_0_bubble_NULL(x1, x2, x3, x4) → Cond_4340_0_bubble_NULL(x1, x3, x4)
8557_0_bubble_Return(x1) → 8557_0_bubble_Return
8622_0_bubble_Return(x1) → 8622_0_bubble_Return
8601_0_bubble_Return(x1) → 8601_0_bubble_Return
8577_0_bubble_Return(x1) → 8577_0_bubble_Return
8259_0_bubble_Return(x1) → 8259_0_bubble_Return
8255_0_bubble_Return(x1) → 8255_0_bubble_Return
8233_0_bubble_Return(x1) → 8233_0_bubble_Return
8175_0_bubble_Return(x1) → 8175_0_bubble_Return
4673_0_bubble_Return(x1, x2) → 4673_0_bubble_Return(x2)
4650_0_bubble_Return(x1, x2) → 4650_0_bubble_Return(x2)
4619_0_bubble_Return(x1, x2) → 4619_0_bubble_Return(x2)
4383_0_bubble_Return(x1, x2) → 4383_0_bubble_Return
4580_0_bubble_Return(x1, x2) → 4580_0_bubble_Return(x2)
Filtered duplicate args:
4340_0_bubble_NULL(x1, x2) → 4340_0_bubble_NULL(x2)
Cond_4340_0_bubble_NULL7(x1, x2, x3) → Cond_4340_0_bubble_NULL7(x1, x3)
Cond_4340_0_bubble_NULL6(x1, x2, x3) → Cond_4340_0_bubble_NULL6(x1, x3)
Cond_4340_0_bubble_NULL5(x1, x2, x3) → Cond_4340_0_bubble_NULL5(x1, x3)
Cond_4340_0_bubble_NULL4(x1, x2, x3) → Cond_4340_0_bubble_NULL4(x1, x3)
Cond_4340_0_bubble_NULL3(x1, x2, x3) → Cond_4340_0_bubble_NULL3(x1, x3)
Cond_4340_0_bubble_NULL2(x1, x2, x3) → Cond_4340_0_bubble_NULL2(x1, x3)
Cond_4340_0_bubble_NULL1(x1, x2, x3) → Cond_4340_0_bubble_NULL1(x1, x3)
Cond_4340_0_bubble_NULL(x1, x2, x3) → Cond_4340_0_bubble_NULL(x1, x3)
Combined rules. Obtained 8 rules for P and 49 rules for R.
Finished conversion. Obtained 8 rules for P and 49 rules for R. System has predefined symbols.
Generated 41 rules for P and 95 rules for R.
Combined rules. Obtained 4 rules for P and 37 rules for R.
Filtered ground terms:
2393_0_length_NONNULL(x1, x2, x3) → 2393_0_length_NONNULL(x2, x3)
3981_0_length_Return(x1) → 3981_0_length_Return
4077_0_length_Return(x1) → 4077_0_length_Return
4046_0_length_Return(x1) → 4046_0_length_Return
4014_0_length_Return(x1) → 4014_0_length_Return
2734_0_length_Return(x1) → 2734_0_length_Return
2718_0_length_Return(x1) → 2718_0_length_Return
2680_0_length_Return(x1) → 2680_0_length_Return
2643_0_length_Return(x1) → 2643_0_length_Return
2421_0_length_Return(x1, x2) → 2421_0_length_Return
Filtered duplicate args:
2393_0_length_NONNULL(x1, x2) → 2393_0_length_NONNULL(x2)
Finished conversion. Obtained 4 rules for P and 37 rules for R. System has no predefined symbols.
Generated 82 rules for P and 457 rules for R.
Combined rules. Obtained 24 rules for P and 122 rules for R.
Filtered ground terms:
6147_0_test_GE(x1, x2, x3, x4, x5, x6, x7) → 6147_0_test_GE(x2, x3, x4, x5, x6, x7)
ARRAY(x1, x2) → ARRAY(x2)
4077_0_length_Return(x1, x2) → 4077_0_length_Return(x2)
4046_0_length_Return(x1, x2) → 4046_0_length_Return(x2)
4014_0_length_Return(x1, x2) → 4014_0_length_Return(x2)
3981_0_length_Return(x1, x2) → 3981_0_length_Return(x2)
2734_0_length_Return(x1, x2) → 2734_0_length_Return
2718_0_length_Return(x1, x2) → 2718_0_length_Return
2680_0_length_Return(x1, x2) → 2680_0_length_Return
2643_0_length_Return(x1, x2) → 2643_0_length_Return
Cond_7152_1_test_InvokeMethod12(x1, x2, x3, x4, x5, x6, x7) → Cond_7152_1_test_InvokeMethod12(x1, x3, x4, x5, x6, x7)
8622_0_bubble_Return(x1) → 8622_0_bubble_Return
Cond_7152_1_test_InvokeMethod11(x1, x2, x3, x4, x5, x6, x7) → Cond_7152_1_test_InvokeMethod11(x1, x3, x4, x5, x6, x7)
8601_0_bubble_Return(x1) → 8601_0_bubble_Return
Cond_7152_1_test_InvokeMethod10(x1, x2, x3, x4, x5, x6, x7) → Cond_7152_1_test_InvokeMethod10(x1, x3, x4, x5, x6, x7)
8577_0_bubble_Return(x1) → 8577_0_bubble_Return
Cond_7152_1_test_InvokeMethod9(x1, x2, x3, x4, x5, x6, x7) → Cond_7152_1_test_InvokeMethod9(x1, x3, x4, x5, x6, x7)
8557_0_bubble_Return(x1) → 8557_0_bubble_Return
Cond_7152_1_test_InvokeMethod8(x1, x2, x3, x4, x5, x6, x7) → Cond_7152_1_test_InvokeMethod8(x1, x3, x4, x5, x6, x7)
8259_0_bubble_Return(x1) → 8259_0_bubble_Return
Cond_7152_1_test_InvokeMethod7(x1, x2, x3, x4, x5, x6, x7) → Cond_7152_1_test_InvokeMethod7(x1, x3, x4, x5, x6, x7)
8255_0_bubble_Return(x1) → 8255_0_bubble_Return
Cond_7152_1_test_InvokeMethod6(x1, x2, x3, x4, x5, x6, x7) → Cond_7152_1_test_InvokeMethod6(x1, x3, x4, x5, x6, x7)
8233_0_bubble_Return(x1) → 8233_0_bubble_Return
Cond_7152_1_test_InvokeMethod5(x1, x2, x3, x4, x5, x6, x7) → Cond_7152_1_test_InvokeMethod5(x1, x3, x4, x5, x6, x7)
8175_0_bubble_Return(x1) → 8175_0_bubble_Return
Cond_7152_1_test_InvokeMethod4(x1, x2, x3, x4, x5, x6, x7) → Cond_7152_1_test_InvokeMethod4(x1, x3, x4, x5, x6)
4673_0_bubble_Return(x1, x2) → 4673_0_bubble_Return
4650_0_bubble_Return(x1, x2) → 4650_0_bubble_Return(x2)
Cond_7152_1_test_InvokeMethod2(x1, x2, x3, x4, x5, x6, x7) → Cond_7152_1_test_InvokeMethod2(x1, x3, x4, x5, x6)
4619_0_bubble_Return(x1, x2) → 4619_0_bubble_Return
Cond_7152_1_test_InvokeMethod1(x1, x2, x3, x4, x5, x6, x7) → Cond_7152_1_test_InvokeMethod1(x1, x3, x4, x5, x6)
4580_0_bubble_Return(x1, x2) → 4580_0_bubble_Return
Cond_7152_1_test_InvokeMethod(x1, x2, x3, x4, x5, x6, x7) → Cond_7152_1_test_InvokeMethod(x1, x3, x4, x5, x6)
4383_0_bubble_Return(x1, x2) → 4383_0_bubble_Return
7152_0_bubble_Load(x1, x2) → 7152_0_bubble_Load(x2)
Cond_6147_0_test_GE1(x1, x2, x3, x4, x5, x6, x7, x8) → Cond_6147_0_test_GE1(x1, x3, x4, x5, x6, x7, x8)
3816_0_length_Load(x1, x2) → 3816_0_length_Load(x2)
Cond_6147_0_test_GE(x1, x2, x3, x4, x5, x6, x7, x8) → Cond_6147_0_test_GE(x1, x3, x4, x5, x6, x7, x8)
2421_0_length_Return(x1, x2, x3) → 2421_0_length_Return
8190_0_bubble_Return(x1, x2) → 8190_0_bubble_Return
8177_0_bubble_Load(x1, x2) → 8177_0_bubble_Load(x2)
8219_0_bubble_Return(x1, x2) → 8219_0_bubble_Return
8205_0_bubble_Load(x1, x2) → 8205_0_bubble_Load(x2)
8159_0_bubble_Return(x1, x2) → 8159_0_bubble_Return
8145_0_bubble_Load(x1, x2) → 8145_0_bubble_Load(x2)
8113_0_bubble_Return(x1, x2) → 8113_0_bubble_Return
8096_0_bubble_Load(x1, x2) → 8096_0_bubble_Load(x2)
Cond_2598_1_length_InvokeMethod7(x1, x2, x3, x4) → Cond_2598_1_length_InvokeMethod7(x1)
2598_1_length_InvokeMethod(x1, x2, x3) → 2598_1_length_InvokeMethod(x1, x3)
Cond_2598_1_length_InvokeMethod6(x1, x2, x3, x4) → Cond_2598_1_length_InvokeMethod6(x1)
Cond_2598_1_length_InvokeMethod5(x1, x2, x3, x4) → Cond_2598_1_length_InvokeMethod5(x1)
Cond_2598_1_length_InvokeMethod4(x1, x2, x3, x4) → Cond_2598_1_length_InvokeMethod4(x1)
Cond_2598_1_length_InvokeMethod3(x1, x2, x3, x4) → Cond_2598_1_length_InvokeMethod3(x1, x2)
Cond_2598_1_length_InvokeMethod2(x1, x2, x3, x4) → Cond_2598_1_length_InvokeMethod2(x1, x2)
Cond_2598_1_length_InvokeMethod1(x1, x2, x3, x4) → Cond_2598_1_length_InvokeMethod1(x1, x2)
Cond_2598_1_length_InvokeMethod(x1, x2, x3, x4) → Cond_2598_1_length_InvokeMethod(x1, x2)
2393_0_length_NONNULL(x1, x2, x3) → 2393_0_length_NONNULL(x2, x3)
Cond_2618_1_length_InvokeMethod7(x1, x2, x3, x4) → Cond_2618_1_length_InvokeMethod7(x1)
2618_1_length_InvokeMethod(x1, x2, x3) → 2618_1_length_InvokeMethod(x1, x3)
Cond_2618_1_length_InvokeMethod6(x1, x2, x3, x4) → Cond_2618_1_length_InvokeMethod6(x1)
Cond_2618_1_length_InvokeMethod5(x1, x2, x3, x4) → Cond_2618_1_length_InvokeMethod5(x1)
Cond_2618_1_length_InvokeMethod4(x1, x2, x3, x4) → Cond_2618_1_length_InvokeMethod4(x1)
Cond_2618_1_length_InvokeMethod3(x1, x2, x3, x4) → Cond_2618_1_length_InvokeMethod3(x1, x2)
Cond_2618_1_length_InvokeMethod2(x1, x2, x3, x4) → Cond_2618_1_length_InvokeMethod2(x1, x2)
Cond_2618_1_length_InvokeMethod1(x1, x2, x3, x4) → Cond_2618_1_length_InvokeMethod1(x1, x2)
Cond_2618_1_length_InvokeMethod(x1, x2, x3, x4) → Cond_2618_1_length_InvokeMethod(x1, x2)
Cond_2578_1_length_InvokeMethod7(x1, x2, x3, x4) → Cond_2578_1_length_InvokeMethod7(x1)
2578_1_length_InvokeMethod(x1, x2, x3) → 2578_1_length_InvokeMethod(x1, x3)
Cond_2578_1_length_InvokeMethod6(x1, x2, x3, x4) → Cond_2578_1_length_InvokeMethod6(x1)
Cond_2578_1_length_InvokeMethod5(x1, x2, x3, x4) → Cond_2578_1_length_InvokeMethod5(x1)
Cond_2578_1_length_InvokeMethod4(x1, x2, x3, x4) → Cond_2578_1_length_InvokeMethod4(x1)
Cond_2578_1_length_InvokeMethod3(x1, x2, x3, x4) → Cond_2578_1_length_InvokeMethod3(x1, x2)
Cond_2578_1_length_InvokeMethod2(x1, x2, x3, x4) → Cond_2578_1_length_InvokeMethod2(x1, x2)
Cond_2578_1_length_InvokeMethod1(x1, x2, x3, x4) → Cond_2578_1_length_InvokeMethod1(x1, x2)
Cond_2578_1_length_InvokeMethod(x1, x2, x3, x4) → Cond_2578_1_length_InvokeMethod(x1, x2)
Cond_2540_1_length_InvokeMethod7(x1, x2, x3, x4) → Cond_2540_1_length_InvokeMethod7(x1)
2540_1_length_InvokeMethod(x1, x2, x3) → 2540_1_length_InvokeMethod(x1, x3)
Cond_2540_1_length_InvokeMethod6(x1, x2, x3, x4) → Cond_2540_1_length_InvokeMethod6(x1)
Cond_2540_1_length_InvokeMethod5(x1, x2, x3, x4) → Cond_2540_1_length_InvokeMethod5(x1)
Cond_2540_1_length_InvokeMethod4(x1, x2, x3, x4) → Cond_2540_1_length_InvokeMethod4(x1)
Cond_2540_1_length_InvokeMethod3(x1, x2, x3, x4) → Cond_2540_1_length_InvokeMethod3(x1, x2)
Cond_2540_1_length_InvokeMethod2(x1, x2, x3, x4) → Cond_2540_1_length_InvokeMethod2(x1, x2)
Cond_2540_1_length_InvokeMethod1(x1, x2, x3, x4) → Cond_2540_1_length_InvokeMethod1(x1, x2)
Cond_2540_1_length_InvokeMethod(x1, x2, x3, x4) → Cond_2540_1_length_InvokeMethod(x1, x2)
8177_1_bubble_InvokeMethod(x1, x2) → 8177_1_bubble_InvokeMethod(x1)
4340_0_bubble_NULL(x1, x2, x3) → 4340_0_bubble_NULL(x2, x3)
Cond_5194_0_bubble_LE(x1, x2, x3, x4, x5) → Cond_5194_0_bubble_LE(x1, x3, x4, x5)
5194_0_bubble_LE(x1, x2, x3, x4) → 5194_0_bubble_LE(x2, x3, x4)
Cond_5189_0_bubble_LE(x1, x2, x3, x4, x5) → Cond_5189_0_bubble_LE(x1, x3, x4, x5)
5189_0_bubble_LE(x1, x2, x3, x4) → 5189_0_bubble_LE(x2, x3, x4)
8205_1_bubble_InvokeMethod(x1, x2) → 8205_1_bubble_InvokeMethod(x1)
Cond_5207_0_bubble_LE(x1, x2, x3, x4, x5) → Cond_5207_0_bubble_LE(x1, x4, x5)
5207_0_bubble_LE(x1, x2, x3, x4) → 5207_0_bubble_LE(x3, x4)
Cond_5201_0_bubble_LE(x1, x2, x3, x4, x5) → Cond_5201_0_bubble_LE(x1, x4, x5)
5201_0_bubble_LE(x1, x2, x3, x4) → 5201_0_bubble_LE(x3, x4)
8145_1_bubble_InvokeMethod(x1, x2) → 8145_1_bubble_InvokeMethod(x1)
Cond_5178_0_bubble_LE(x1, x2, x3, x4, x5) → Cond_5178_0_bubble_LE(x1, x4, x5)
5178_0_bubble_LE(x1, x2, x3, x4) → 5178_0_bubble_LE(x3, x4)
Cond_5170_0_bubble_LE(x1, x2, x3, x4, x5) → Cond_5170_0_bubble_LE(x1, x4, x5)
5170_0_bubble_LE(x1, x2, x3, x4) → 5170_0_bubble_LE(x3, x4)
8096_1_bubble_InvokeMethod(x1, x2) → 8096_1_bubble_InvokeMethod(x1)
Cond_5132_0_bubble_LE(x1, x2, x3, x4, x5) → Cond_5132_0_bubble_LE(x1, x4, x5)
5132_0_bubble_LE(x1, x2, x3, x4) → 5132_0_bubble_LE(x3, x4)
Cond_5129_0_bubble_LE(x1, x2, x3, x4, x5) → Cond_5129_0_bubble_LE(x1, x4, x5)
5129_0_bubble_LE(x1, x2, x3, x4) → 5129_0_bubble_LE(x3, x4)
7661_0_test_Return(x1) → 7661_0_test_Return
3458_0_test_Return(x1) → 3458_0_test_Return
Filtered duplicate args:
6147_0_test_GE(x1, x2, x3, x4, x5, x6) → 6147_0_test_GE(x1, x2, x5, x6)
Cond_6147_0_test_GE1(x1, x2, x3, x4, x5, x6, x7) → Cond_6147_0_test_GE1(x1, x2, x3, x6, x7)
Cond_6147_0_test_GE(x1, x2, x3, x4, x5, x6, x7) → Cond_6147_0_test_GE(x1, x2, x3, x6, x7)
2393_0_length_NONNULL(x1, x2) → 2393_0_length_NONNULL(x2)
4340_0_bubble_NULL(x1, x2) → 4340_0_bubble_NULL(x2)
Filtered unneeded arguments:
Cond_6147_0_test_GE(x1, x2, x3, x4, x5) → Cond_6147_0_test_GE(x1, x2, x3)
Cond_7152_1_test_InvokeMethod5(x1, x2, x3, x4, x5, x6) → Cond_7152_1_test_InvokeMethod5(x1, x2, x3, x4, x5)
Cond_7152_1_test_InvokeMethod6(x1, x2, x3, x4, x5, x6) → Cond_7152_1_test_InvokeMethod6(x1, x2, x3, x4, x5)
Cond_7152_1_test_InvokeMethod7(x1, x2, x3, x4, x5, x6) → Cond_7152_1_test_InvokeMethod7(x1, x2, x3, x4, x5)
Cond_7152_1_test_InvokeMethod8(x1, x2, x3, x4, x5, x6) → Cond_7152_1_test_InvokeMethod8(x1, x2, x3, x4, x5)
Cond_7152_1_test_InvokeMethod9(x1, x2, x3, x4, x5, x6) → Cond_7152_1_test_InvokeMethod9(x1, x2, x3, x4, x5)
Cond_7152_1_test_InvokeMethod10(x1, x2, x3, x4, x5, x6) → Cond_7152_1_test_InvokeMethod10(x1, x2, x3, x4, x5)
Cond_7152_1_test_InvokeMethod11(x1, x2, x3, x4, x5, x6) → Cond_7152_1_test_InvokeMethod11(x1, x2, x3, x4, x5)
Cond_7152_1_test_InvokeMethod12(x1, x2, x3, x4, x5, x6) → Cond_7152_1_test_InvokeMethod12(x1, x2, x3, x4, x5)
Cond_5129_0_bubble_LE(x1, x2, x3) → Cond_5129_0_bubble_LE(x1)
Cond_5132_0_bubble_LE(x1, x2, x3) → Cond_5132_0_bubble_LE(x1)
Cond_5170_0_bubble_LE(x1, x2, x3) → Cond_5170_0_bubble_LE(x1)
Cond_5178_0_bubble_LE(x1, x2, x3) → Cond_5178_0_bubble_LE(x1)
Cond_5201_0_bubble_LE(x1, x2, x3) → Cond_5201_0_bubble_LE(x1)
Cond_5207_0_bubble_LE(x1, x2, x3) → Cond_5207_0_bubble_LE(x1)
Cond_5189_0_bubble_LE(x1, x2, x3, x4) → Cond_5189_0_bubble_LE(x1, x2)
Cond_5194_0_bubble_LE(x1, x2, x3, x4) → Cond_5194_0_bubble_LE(x1, x2)
Filtered all free variables:
3816_1_test_InvokeMethod(x1, x2, x3, x4) → 3816_1_test_InvokeMethod(x2, x3, x4)
5129_0_bubble_LE(x1, x2) → 5129_0_bubble_LE
5132_0_bubble_LE(x1, x2) → 5132_0_bubble_LE
5170_0_bubble_LE(x1, x2) → 5170_0_bubble_LE
5178_0_bubble_LE(x1, x2) → 5178_0_bubble_LE
5201_0_bubble_LE(x1, x2) → 5201_0_bubble_LE
5207_0_bubble_LE(x1, x2) → 5207_0_bubble_LE
5189_0_bubble_LE(x1, x2, x3) → 5189_0_bubble_LE(x1)
5194_0_bubble_LE(x1, x2, x3) → 5194_0_bubble_LE(x1)
2540_1_length_InvokeMethod(x1, x2) → 2540_1_length_InvokeMethod(x1)
2393_0_length_NONNULL(x1) → 2393_0_length_NONNULL
2578_1_length_InvokeMethod(x1, x2) → 2578_1_length_InvokeMethod(x1)
2618_1_length_InvokeMethod(x1, x2) → 2618_1_length_InvokeMethod(x1)
2598_1_length_InvokeMethod(x1, x2) → 2598_1_length_InvokeMethod(x1)
Combined rules. Obtained 17 rules for P and 118 rules for R.
Finished conversion. Obtained 17 rules for P and 118 rules for R. System has predefined symbols.
Generated 21 rules for P and 557 rules for R.
Combined rules. Obtained 1 rules for P and 0 rules for R.
Filtered ground terms:
1442_1_main_InvokeMethod(x1, x2, x3, x4) → 1442_1_main_InvokeMethod(x1, x2, x3)
DATA_3(x1, x2, x3) → DATA_3(x1, x2)
ARRAY(x1, x2) → ARRAY(x2)
List(x1) → List
1442_0_mk_Inc(x1, x2, x3, x4) → 1442_0_mk_Inc(x2, x3, x4)
Cond_1442_1_main_InvokeMethod(x1, x2, x3, x4, x5) → Cond_1442_1_main_InvokeMethod(x1, x2, x3, x4)
Filtered duplicate args:
1442_1_main_InvokeMethod(x1, x2, x3) → 1442_1_main_InvokeMethod(x1, x3)
1442_0_mk_Inc(x1, x2, x3) → 1442_0_mk_Inc(x2, x3)
Cond_1442_1_main_InvokeMethod(x1, x2, x3, x4) → Cond_1442_1_main_InvokeMethod(x1, x2, x4)
Combined rules. Obtained 1 rules for P and 0 rules for R.
Finished conversion. Obtained 1 rules for P and 0 rules for R. System has predefined symbols.
Generated 21 rules for P and 591 rules for R.
Combined rules. Obtained 1 rules for P and 0 rules for R.
Filtered ground terms:
1171_1_main_InvokeMethod(x1, x2, x3, x4, x5, x6) → 1171_1_main_InvokeMethod(x1, x2, x3, x4, x6)
DATA_3(x1, x2, x3) → DATA_3(x1)
List(x1) → List
1171_0_mk_Inc(x1, x2, x3, x4) → 1171_0_mk_Inc(x2, x3, x4)
Cond_1171_1_main_InvokeMethod(x1, x2, x3, x4, x5, x6, x7) → Cond_1171_1_main_InvokeMethod(x1, x2, x3, x4, x5, x7)
Filtered duplicate args:
1171_1_main_InvokeMethod(x1, x2, x3, x4, x5) → 1171_1_main_InvokeMethod(x1, x2, x4, x5)
1171_0_mk_Inc(x1, x2, x3) → 1171_0_mk_Inc(x2, x3)
Cond_1171_1_main_InvokeMethod(x1, x2, x3, x4, x5, x6) → Cond_1171_1_main_InvokeMethod(x1, x2, x3, x5, x6)
Combined rules. Obtained 1 rules for P and 0 rules for R.
Finished conversion. Obtained 1 rules for P and 0 rules for R. System has predefined symbols.
Generated 21 rules for P and 626 rules for R.
Combined rules. Obtained 1 rules for P and 0 rules for R.
Filtered ground terms:
544_1_main_InvokeMethod(x1, x2, x3, x4, x5, x6) → 544_1_main_InvokeMethod(x1, x2, x6)
DATA_3(x1, x2, x3) → DATA_3
List(x1) → List
544_0_mk_Inc(x1, x2, x3, x4) → 544_0_mk_Inc(x2, x3, x4)
Cond_544_1_main_InvokeMethod(x1, x2, x3, x4, x5, x6, x7) → Cond_544_1_main_InvokeMethod(x1, x2, x3, x7)
Filtered duplicate args:
544_0_mk_Inc(x1, x2, x3) → 544_0_mk_Inc(x2, x3)
Combined rules. Obtained 1 rules for P and 0 rules for R.
Finished conversion. Obtained 1 rules for P and 0 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
(0) -> (1), if ((x3[0] <= x2[0] →* TRUE)∧(java.lang.Object(List(x0[0], java.lang.Object(List(EOC, x1[0], x2[0])), x3[0])) →* java.lang.Object(List(x0[1], java.lang.Object(List(EOC, x1[1], x2[1])), x3[1]))))
(1) -> (0), if ((java.lang.Object(List(EOC, x1[1], x2[1])) →* java.lang.Object(List(x0[0], java.lang.Object(List(EOC, x1[0], x2[0])), x3[0]))))
(1) -> (2), if ((java.lang.Object(List(EOC, x1[1], x2[1])) →* java.lang.Object(List(x0[2], java.lang.Object(List(EOC, x1[2], x2[2])), x3[2]))))
(1) -> (4), if ((java.lang.Object(List(EOC, x1[1], x2[1])) →* java.lang.Object(List(EOC, java.lang.Object(List(EOC, x0[4], x1[4])), x2[4]))))
(1) -> (6), if ((java.lang.Object(List(EOC, x1[1], x2[1])) →* java.lang.Object(List(EOC, java.lang.Object(List(EOC, x0[6], x1[6])), x2[6]))))
(2) -> (3), if ((x3[2] > x2[2] →* TRUE)∧(java.lang.Object(List(x0[2], java.lang.Object(List(EOC, x1[2], x2[2])), x3[2])) →* java.lang.Object(List(x0[3], java.lang.Object(List(EOC, x1[3], x2[3])), x3[3]))))
(3) -> (0), if ((java.lang.Object(List(EOC, x1[3], x3[3])) →* java.lang.Object(List(x0[0], java.lang.Object(List(EOC, x1[0], x2[0])), x3[0]))))
(3) -> (2), if ((java.lang.Object(List(EOC, x1[3], x3[3])) →* java.lang.Object(List(x0[2], java.lang.Object(List(EOC, x1[2], x2[2])), x3[2]))))
(3) -> (4), if ((java.lang.Object(List(EOC, x1[3], x3[3])) →* java.lang.Object(List(EOC, java.lang.Object(List(EOC, x0[4], x1[4])), x2[4]))))
(3) -> (6), if ((java.lang.Object(List(EOC, x1[3], x3[3])) →* java.lang.Object(List(EOC, java.lang.Object(List(EOC, x0[6], x1[6])), x2[6]))))
(4) -> (5), if ((x2[4] <= x1[4] →* TRUE)∧(java.lang.Object(List(EOC, java.lang.Object(List(EOC, x0[4], x1[4])), x2[4])) →* java.lang.Object(List(EOC, java.lang.Object(List(EOC, x0[5], x1[5])), x2[5]))))
(5) -> (0), if ((java.lang.Object(List(EOC, x0[5], x1[5])) →* java.lang.Object(List(x0[0], java.lang.Object(List(EOC, x1[0], x2[0])), x3[0]))))
(5) -> (2), if ((java.lang.Object(List(EOC, x0[5], x1[5])) →* java.lang.Object(List(x0[2], java.lang.Object(List(EOC, x1[2], x2[2])), x3[2]))))
(5) -> (4), if ((java.lang.Object(List(EOC, x0[5], x1[5])) →* java.lang.Object(List(EOC, java.lang.Object(List(EOC, x0[4], x1[4])), x2[4]))))
(5) -> (6), if ((java.lang.Object(List(EOC, x0[5], x1[5])) →* java.lang.Object(List(EOC, java.lang.Object(List(EOC, x0[6], x1[6])), x2[6]))))
(6) -> (7), if ((x2[6] > x1[6] →* TRUE)∧(java.lang.Object(List(EOC, java.lang.Object(List(EOC, x0[6], x1[6])), x2[6])) →* java.lang.Object(List(EOC, java.lang.Object(List(EOC, x0[7], x1[7])), x2[7]))))
(7) -> (0), if ((java.lang.Object(List(EOC, x0[7], x2[7])) →* java.lang.Object(List(x0[0], java.lang.Object(List(EOC, x1[0], x2[0])), x3[0]))))
(7) -> (2), if ((java.lang.Object(List(EOC, x0[7], x2[7])) →* java.lang.Object(List(x0[2], java.lang.Object(List(EOC, x1[2], x2[2])), x3[2]))))
(7) -> (4), if ((java.lang.Object(List(EOC, x0[7], x2[7])) →* java.lang.Object(List(EOC, java.lang.Object(List(EOC, x0[4], x1[4])), x2[4]))))
(7) -> (6), if ((java.lang.Object(List(EOC, x0[7], x2[7])) →* java.lang.Object(List(EOC, java.lang.Object(List(EOC, x0[6], x1[6])), x2[6]))))
(1) (<=(x3[0], x2[0])=TRUE∧java.lang.Object(List(x0[0], java.lang.Object(List(EOC, x1[0], x2[0])), x3[0]))=java.lang.Object(List(x0[1], java.lang.Object(List(EOC, x1[1], x2[1])), x3[1])) ⇒ 4340_0_BUBBLE_NULL(java.lang.Object(List(x0[0], java.lang.Object(List(EOC, x1[0], x2[0])), x3[0])))≥NonInfC∧4340_0_BUBBLE_NULL(java.lang.Object(List(x0[0], java.lang.Object(List(EOC, x1[0], x2[0])), x3[0])))≥COND_4340_0_BUBBLE_NULL(<=(x3[0], x2[0]), java.lang.Object(List(x0[0], java.lang.Object(List(EOC, x1[0], x2[0])), x3[0])))∧(UIncreasing(COND_4340_0_BUBBLE_NULL(<=(x3[0], x2[0]), java.lang.Object(List(x0[0], java.lang.Object(List(EOC, x1[0], x2[0])), x3[0])))), ≥))
(2) (<=(x3[0], x2[0])=TRUE ⇒ 4340_0_BUBBLE_NULL(java.lang.Object(List(x0[0], java.lang.Object(List(EOC, x1[0], x2[0])), x3[0])))≥NonInfC∧4340_0_BUBBLE_NULL(java.lang.Object(List(x0[0], java.lang.Object(List(EOC, x1[0], x2[0])), x3[0])))≥COND_4340_0_BUBBLE_NULL(<=(x3[0], x2[0]), java.lang.Object(List(x0[0], java.lang.Object(List(EOC, x1[0], x2[0])), x3[0])))∧(UIncreasing(COND_4340_0_BUBBLE_NULL(<=(x3[0], x2[0]), java.lang.Object(List(x0[0], java.lang.Object(List(EOC, x1[0], x2[0])), x3[0])))), ≥))
(3) (0 ≥ 0 ⇒ (UIncreasing(COND_4340_0_BUBBLE_NULL(<=(x3[0], x2[0]), java.lang.Object(List(x0[0], java.lang.Object(List(EOC, x1[0], x2[0])), x3[0])))), ≥)∧[(15)bni_54 + (-1)Bound*bni_54] + [(16)bni_54]x1[0] + [(4)bni_54]x0[0] ≥ 0∧[(-1)bso_55] ≥ 0)
(4) (0 ≥ 0 ⇒ (UIncreasing(COND_4340_0_BUBBLE_NULL(<=(x3[0], x2[0]), java.lang.Object(List(x0[0], java.lang.Object(List(EOC, x1[0], x2[0])), x3[0])))), ≥)∧[(15)bni_54 + (-1)Bound*bni_54] + [(16)bni_54]x1[0] + [(4)bni_54]x0[0] ≥ 0∧[(-1)bso_55] ≥ 0)
(5) (0 ≥ 0 ⇒ (UIncreasing(COND_4340_0_BUBBLE_NULL(<=(x3[0], x2[0]), java.lang.Object(List(x0[0], java.lang.Object(List(EOC, x1[0], x2[0])), x3[0])))), ≥)∧[(15)bni_54 + (-1)Bound*bni_54] + [(16)bni_54]x1[0] + [(4)bni_54]x0[0] ≥ 0∧[(-1)bso_55] ≥ 0)
(6) (0 ≥ 0 ⇒ (UIncreasing(COND_4340_0_BUBBLE_NULL(<=(x3[0], x2[0]), java.lang.Object(List(x0[0], java.lang.Object(List(EOC, x1[0], x2[0])), x3[0])))), ≥)∧0 ≥ 0∧0 ≥ 0∧[(16)bni_54] ≥ 0∧[(4)bni_54] ≥ 0∧[(15)bni_54 + (-1)Bound*bni_54] ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[(-1)bso_55] ≥ 0)
(7) (<=(x3[0], x2[0])=TRUE∧java.lang.Object(List(x0[0], java.lang.Object(List(EOC, x1[0], x2[0])), x3[0]))=java.lang.Object(List(x0[1], java.lang.Object(List(EOC, x1[1], x2[1])), x3[1])) ⇒ COND_4340_0_BUBBLE_NULL(TRUE, java.lang.Object(List(x0[1], java.lang.Object(List(EOC, x1[1], x2[1])), x3[1])))≥NonInfC∧COND_4340_0_BUBBLE_NULL(TRUE, java.lang.Object(List(x0[1], java.lang.Object(List(EOC, x1[1], x2[1])), x3[1])))≥4340_0_BUBBLE_NULL(java.lang.Object(List(EOC, x1[1], x2[1])))∧(UIncreasing(4340_0_BUBBLE_NULL(java.lang.Object(List(EOC, x1[1], x2[1])))), ≥))
(8) (<=(x3[0], x2[0])=TRUE ⇒ COND_4340_0_BUBBLE_NULL(TRUE, java.lang.Object(List(x0[0], java.lang.Object(List(EOC, x1[0], x2[0])), x3[0])))≥NonInfC∧COND_4340_0_BUBBLE_NULL(TRUE, java.lang.Object(List(x0[0], java.lang.Object(List(EOC, x1[0], x2[0])), x3[0])))≥4340_0_BUBBLE_NULL(java.lang.Object(List(EOC, x1[0], x2[0])))∧(UIncreasing(4340_0_BUBBLE_NULL(java.lang.Object(List(EOC, x1[1], x2[1])))), ≥))
(9) (0 ≥ 0 ⇒ (UIncreasing(4340_0_BUBBLE_NULL(java.lang.Object(List(EOC, x1[1], x2[1])))), ≥)∧[(15)bni_56 + (-1)Bound*bni_56] + [(16)bni_56]x1[0] + [(4)bni_56]x0[0] ≥ 0∧[12 + (-1)bso_57] + [12]x1[0] + [4]x0[0] ≥ 0)
(10) (0 ≥ 0 ⇒ (UIncreasing(4340_0_BUBBLE_NULL(java.lang.Object(List(EOC, x1[1], x2[1])))), ≥)∧[(15)bni_56 + (-1)Bound*bni_56] + [(16)bni_56]x1[0] + [(4)bni_56]x0[0] ≥ 0∧[12 + (-1)bso_57] + [12]x1[0] + [4]x0[0] ≥ 0)
(11) (0 ≥ 0 ⇒ (UIncreasing(4340_0_BUBBLE_NULL(java.lang.Object(List(EOC, x1[1], x2[1])))), ≥)∧[(15)bni_56 + (-1)Bound*bni_56] + [(16)bni_56]x1[0] + [(4)bni_56]x0[0] ≥ 0∧[12 + (-1)bso_57] + [12]x1[0] + [4]x0[0] ≥ 0)
(12) (0 ≥ 0 ⇒ (UIncreasing(4340_0_BUBBLE_NULL(java.lang.Object(List(EOC, x1[1], x2[1])))), ≥)∧0 ≥ 0∧0 ≥ 0∧[(16)bni_56] ≥ 0∧[(4)bni_56] ≥ 0∧[(15)bni_56 + (-1)Bound*bni_56] ≥ 0∧0 ≥ 0∧0 ≥ 0∧[12 + (-1)bso_57] ≥ 0∧[1] ≥ 0∧[1] ≥ 0)
(13) (>(x3[2], x2[2])=TRUE∧java.lang.Object(List(x0[2], java.lang.Object(List(EOC, x1[2], x2[2])), x3[2]))=java.lang.Object(List(x0[3], java.lang.Object(List(EOC, x1[3], x2[3])), x3[3])) ⇒ 4340_0_BUBBLE_NULL(java.lang.Object(List(x0[2], java.lang.Object(List(EOC, x1[2], x2[2])), x3[2])))≥NonInfC∧4340_0_BUBBLE_NULL(java.lang.Object(List(x0[2], java.lang.Object(List(EOC, x1[2], x2[2])), x3[2])))≥COND_4340_0_BUBBLE_NULL1(>(x3[2], x2[2]), java.lang.Object(List(x0[2], java.lang.Object(List(EOC, x1[2], x2[2])), x3[2])))∧(UIncreasing(COND_4340_0_BUBBLE_NULL1(>(x3[2], x2[2]), java.lang.Object(List(x0[2], java.lang.Object(List(EOC, x1[2], x2[2])), x3[2])))), ≥))
(14) (>(x3[2], x2[2])=TRUE ⇒ 4340_0_BUBBLE_NULL(java.lang.Object(List(x0[2], java.lang.Object(List(EOC, x1[2], x2[2])), x3[2])))≥NonInfC∧4340_0_BUBBLE_NULL(java.lang.Object(List(x0[2], java.lang.Object(List(EOC, x1[2], x2[2])), x3[2])))≥COND_4340_0_BUBBLE_NULL1(>(x3[2], x2[2]), java.lang.Object(List(x0[2], java.lang.Object(List(EOC, x1[2], x2[2])), x3[2])))∧(UIncreasing(COND_4340_0_BUBBLE_NULL1(>(x3[2], x2[2]), java.lang.Object(List(x0[2], java.lang.Object(List(EOC, x1[2], x2[2])), x3[2])))), ≥))
(15) (0 ≥ 0 ⇒ (UIncreasing(COND_4340_0_BUBBLE_NULL1(>(x3[2], x2[2]), java.lang.Object(List(x0[2], java.lang.Object(List(EOC, x1[2], x2[2])), x3[2])))), ≥)∧[(15)bni_58 + (-1)Bound*bni_58] + [(16)bni_58]x1[2] + [(4)bni_58]x0[2] ≥ 0∧[(-1)bso_59] ≥ 0)
(16) (0 ≥ 0 ⇒ (UIncreasing(COND_4340_0_BUBBLE_NULL1(>(x3[2], x2[2]), java.lang.Object(List(x0[2], java.lang.Object(List(EOC, x1[2], x2[2])), x3[2])))), ≥)∧[(15)bni_58 + (-1)Bound*bni_58] + [(16)bni_58]x1[2] + [(4)bni_58]x0[2] ≥ 0∧[(-1)bso_59] ≥ 0)
(17) (0 ≥ 0 ⇒ (UIncreasing(COND_4340_0_BUBBLE_NULL1(>(x3[2], x2[2]), java.lang.Object(List(x0[2], java.lang.Object(List(EOC, x1[2], x2[2])), x3[2])))), ≥)∧[(15)bni_58 + (-1)Bound*bni_58] + [(16)bni_58]x1[2] + [(4)bni_58]x0[2] ≥ 0∧[(-1)bso_59] ≥ 0)
(18) (0 ≥ 0 ⇒ (UIncreasing(COND_4340_0_BUBBLE_NULL1(>(x3[2], x2[2]), java.lang.Object(List(x0[2], java.lang.Object(List(EOC, x1[2], x2[2])), x3[2])))), ≥)∧0 ≥ 0∧0 ≥ 0∧[(16)bni_58] ≥ 0∧[(4)bni_58] ≥ 0∧[(15)bni_58 + (-1)Bound*bni_58] ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[(-1)bso_59] ≥ 0)
(19) (>(x3[2], x2[2])=TRUE∧java.lang.Object(List(x0[2], java.lang.Object(List(EOC, x1[2], x2[2])), x3[2]))=java.lang.Object(List(x0[3], java.lang.Object(List(EOC, x1[3], x2[3])), x3[3])) ⇒ COND_4340_0_BUBBLE_NULL1(TRUE, java.lang.Object(List(x0[3], java.lang.Object(List(EOC, x1[3], x2[3])), x3[3])))≥NonInfC∧COND_4340_0_BUBBLE_NULL1(TRUE, java.lang.Object(List(x0[3], java.lang.Object(List(EOC, x1[3], x2[3])), x3[3])))≥4340_0_BUBBLE_NULL(java.lang.Object(List(EOC, x1[3], x3[3])))∧(UIncreasing(4340_0_BUBBLE_NULL(java.lang.Object(List(EOC, x1[3], x3[3])))), ≥))
(20) (>(x3[2], x2[2])=TRUE ⇒ COND_4340_0_BUBBLE_NULL1(TRUE, java.lang.Object(List(x0[2], java.lang.Object(List(EOC, x1[2], x2[2])), x3[2])))≥NonInfC∧COND_4340_0_BUBBLE_NULL1(TRUE, java.lang.Object(List(x0[2], java.lang.Object(List(EOC, x1[2], x2[2])), x3[2])))≥4340_0_BUBBLE_NULL(java.lang.Object(List(EOC, x1[2], x3[2])))∧(UIncreasing(4340_0_BUBBLE_NULL(java.lang.Object(List(EOC, x1[3], x3[3])))), ≥))
(21) (0 ≥ 0 ⇒ (UIncreasing(4340_0_BUBBLE_NULL(java.lang.Object(List(EOC, x1[3], x3[3])))), ≥)∧[(15)bni_60 + (-1)Bound*bni_60] + [(16)bni_60]x1[2] + [(4)bni_60]x0[2] ≥ 0∧[12 + (-1)bso_61] + [12]x1[2] + [4]x0[2] ≥ 0)
(22) (0 ≥ 0 ⇒ (UIncreasing(4340_0_BUBBLE_NULL(java.lang.Object(List(EOC, x1[3], x3[3])))), ≥)∧[(15)bni_60 + (-1)Bound*bni_60] + [(16)bni_60]x1[2] + [(4)bni_60]x0[2] ≥ 0∧[12 + (-1)bso_61] + [12]x1[2] + [4]x0[2] ≥ 0)
(23) (0 ≥ 0 ⇒ (UIncreasing(4340_0_BUBBLE_NULL(java.lang.Object(List(EOC, x1[3], x3[3])))), ≥)∧[(15)bni_60 + (-1)Bound*bni_60] + [(16)bni_60]x1[2] + [(4)bni_60]x0[2] ≥ 0∧[12 + (-1)bso_61] + [12]x1[2] + [4]x0[2] ≥ 0)
(24) (0 ≥ 0 ⇒ (UIncreasing(4340_0_BUBBLE_NULL(java.lang.Object(List(EOC, x1[3], x3[3])))), ≥)∧0 ≥ 0∧0 ≥ 0∧[(16)bni_60] ≥ 0∧[(4)bni_60] ≥ 0∧[(15)bni_60 + (-1)Bound*bni_60] ≥ 0∧0 ≥ 0∧0 ≥ 0∧[12 + (-1)bso_61] ≥ 0∧[1] ≥ 0∧[1] ≥ 0)
(25) (<=(x2[4], x1[4])=TRUE∧java.lang.Object(List(EOC, java.lang.Object(List(EOC, x0[4], x1[4])), x2[4]))=java.lang.Object(List(EOC, java.lang.Object(List(EOC, x0[5], x1[5])), x2[5])) ⇒ 4340_0_BUBBLE_NULL(java.lang.Object(List(EOC, java.lang.Object(List(EOC, x0[4], x1[4])), x2[4])))≥NonInfC∧4340_0_BUBBLE_NULL(java.lang.Object(List(EOC, java.lang.Object(List(EOC, x0[4], x1[4])), x2[4])))≥COND_4340_0_BUBBLE_NULL2(<=(x2[4], x1[4]), java.lang.Object(List(EOC, java.lang.Object(List(EOC, x0[4], x1[4])), x2[4])))∧(UIncreasing(COND_4340_0_BUBBLE_NULL2(<=(x2[4], x1[4]), java.lang.Object(List(EOC, java.lang.Object(List(EOC, x0[4], x1[4])), x2[4])))), ≥))
(26) (<=(x2[4], x1[4])=TRUE ⇒ 4340_0_BUBBLE_NULL(java.lang.Object(List(EOC, java.lang.Object(List(EOC, x0[4], x1[4])), x2[4])))≥NonInfC∧4340_0_BUBBLE_NULL(java.lang.Object(List(EOC, java.lang.Object(List(EOC, x0[4], x1[4])), x2[4])))≥COND_4340_0_BUBBLE_NULL2(<=(x2[4], x1[4]), java.lang.Object(List(EOC, java.lang.Object(List(EOC, x0[4], x1[4])), x2[4])))∧(UIncreasing(COND_4340_0_BUBBLE_NULL2(<=(x2[4], x1[4]), java.lang.Object(List(EOC, java.lang.Object(List(EOC, x0[4], x1[4])), x2[4])))), ≥))
(27) (0 ≥ 0 ⇒ (UIncreasing(COND_4340_0_BUBBLE_NULL2(<=(x2[4], x1[4]), java.lang.Object(List(EOC, java.lang.Object(List(EOC, x0[4], x1[4])), x2[4])))), ≥)∧[(19)bni_62 + (-1)Bound*bni_62] + [(16)bni_62]x0[4] ≥ 0∧[(-1)bso_63] ≥ 0)
(28) (0 ≥ 0 ⇒ (UIncreasing(COND_4340_0_BUBBLE_NULL2(<=(x2[4], x1[4]), java.lang.Object(List(EOC, java.lang.Object(List(EOC, x0[4], x1[4])), x2[4])))), ≥)∧[(19)bni_62 + (-1)Bound*bni_62] + [(16)bni_62]x0[4] ≥ 0∧[(-1)bso_63] ≥ 0)
(29) (0 ≥ 0 ⇒ (UIncreasing(COND_4340_0_BUBBLE_NULL2(<=(x2[4], x1[4]), java.lang.Object(List(EOC, java.lang.Object(List(EOC, x0[4], x1[4])), x2[4])))), ≥)∧[(19)bni_62 + (-1)Bound*bni_62] + [(16)bni_62]x0[4] ≥ 0∧[(-1)bso_63] ≥ 0)
(30) (0 ≥ 0 ⇒ (UIncreasing(COND_4340_0_BUBBLE_NULL2(<=(x2[4], x1[4]), java.lang.Object(List(EOC, java.lang.Object(List(EOC, x0[4], x1[4])), x2[4])))), ≥)∧0 ≥ 0∧0 ≥ 0∧[(16)bni_62] ≥ 0∧[(19)bni_62 + (-1)Bound*bni_62] ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[(-1)bso_63] ≥ 0)
(31) (<=(x2[4], x1[4])=TRUE∧java.lang.Object(List(EOC, java.lang.Object(List(EOC, x0[4], x1[4])), x2[4]))=java.lang.Object(List(EOC, java.lang.Object(List(EOC, x0[5], x1[5])), x2[5])) ⇒ COND_4340_0_BUBBLE_NULL2(TRUE, java.lang.Object(List(EOC, java.lang.Object(List(EOC, x0[5], x1[5])), x2[5])))≥NonInfC∧COND_4340_0_BUBBLE_NULL2(TRUE, java.lang.Object(List(EOC, java.lang.Object(List(EOC, x0[5], x1[5])), x2[5])))≥4340_0_BUBBLE_NULL(java.lang.Object(List(EOC, x0[5], x1[5])))∧(UIncreasing(4340_0_BUBBLE_NULL(java.lang.Object(List(EOC, x0[5], x1[5])))), ≥))
(32) (<=(x2[4], x1[4])=TRUE ⇒ COND_4340_0_BUBBLE_NULL2(TRUE, java.lang.Object(List(EOC, java.lang.Object(List(EOC, x0[4], x1[4])), x2[4])))≥NonInfC∧COND_4340_0_BUBBLE_NULL2(TRUE, java.lang.Object(List(EOC, java.lang.Object(List(EOC, x0[4], x1[4])), x2[4])))≥4340_0_BUBBLE_NULL(java.lang.Object(List(EOC, x0[4], x1[4])))∧(UIncreasing(4340_0_BUBBLE_NULL(java.lang.Object(List(EOC, x0[5], x1[5])))), ≥))
(33) (0 ≥ 0 ⇒ (UIncreasing(4340_0_BUBBLE_NULL(java.lang.Object(List(EOC, x0[5], x1[5])))), ≥)∧[(19)bni_64 + (-1)Bound*bni_64] + [(16)bni_64]x0[4] ≥ 0∧[16 + (-1)bso_65] + [12]x0[4] ≥ 0)
(34) (0 ≥ 0 ⇒ (UIncreasing(4340_0_BUBBLE_NULL(java.lang.Object(List(EOC, x0[5], x1[5])))), ≥)∧[(19)bni_64 + (-1)Bound*bni_64] + [(16)bni_64]x0[4] ≥ 0∧[16 + (-1)bso_65] + [12]x0[4] ≥ 0)
(35) (0 ≥ 0 ⇒ (UIncreasing(4340_0_BUBBLE_NULL(java.lang.Object(List(EOC, x0[5], x1[5])))), ≥)∧[(19)bni_64 + (-1)Bound*bni_64] + [(16)bni_64]x0[4] ≥ 0∧[16 + (-1)bso_65] + [12]x0[4] ≥ 0)
(36) (0 ≥ 0 ⇒ (UIncreasing(4340_0_BUBBLE_NULL(java.lang.Object(List(EOC, x0[5], x1[5])))), ≥)∧0 ≥ 0∧0 ≥ 0∧[(16)bni_64] ≥ 0∧[(19)bni_64 + (-1)Bound*bni_64] ≥ 0∧0 ≥ 0∧0 ≥ 0∧[16 + (-1)bso_65] ≥ 0∧[1] ≥ 0)
(37) (>(x2[6], x1[6])=TRUE∧java.lang.Object(List(EOC, java.lang.Object(List(EOC, x0[6], x1[6])), x2[6]))=java.lang.Object(List(EOC, java.lang.Object(List(EOC, x0[7], x1[7])), x2[7])) ⇒ 4340_0_BUBBLE_NULL(java.lang.Object(List(EOC, java.lang.Object(List(EOC, x0[6], x1[6])), x2[6])))≥NonInfC∧4340_0_BUBBLE_NULL(java.lang.Object(List(EOC, java.lang.Object(List(EOC, x0[6], x1[6])), x2[6])))≥COND_4340_0_BUBBLE_NULL3(>(x2[6], x1[6]), java.lang.Object(List(EOC, java.lang.Object(List(EOC, x0[6], x1[6])), x2[6])))∧(UIncreasing(COND_4340_0_BUBBLE_NULL3(>(x2[6], x1[6]), java.lang.Object(List(EOC, java.lang.Object(List(EOC, x0[6], x1[6])), x2[6])))), ≥))
(38) (>(x2[6], x1[6])=TRUE ⇒ 4340_0_BUBBLE_NULL(java.lang.Object(List(EOC, java.lang.Object(List(EOC, x0[6], x1[6])), x2[6])))≥NonInfC∧4340_0_BUBBLE_NULL(java.lang.Object(List(EOC, java.lang.Object(List(EOC, x0[6], x1[6])), x2[6])))≥COND_4340_0_BUBBLE_NULL3(>(x2[6], x1[6]), java.lang.Object(List(EOC, java.lang.Object(List(EOC, x0[6], x1[6])), x2[6])))∧(UIncreasing(COND_4340_0_BUBBLE_NULL3(>(x2[6], x1[6]), java.lang.Object(List(EOC, java.lang.Object(List(EOC, x0[6], x1[6])), x2[6])))), ≥))
(39) (0 ≥ 0 ⇒ (UIncreasing(COND_4340_0_BUBBLE_NULL3(>(x2[6], x1[6]), java.lang.Object(List(EOC, java.lang.Object(List(EOC, x0[6], x1[6])), x2[6])))), ≥)∧[(19)bni_66 + (-1)Bound*bni_66] + [(16)bni_66]x0[6] ≥ 0∧[(-1)bso_67] ≥ 0)
(40) (0 ≥ 0 ⇒ (UIncreasing(COND_4340_0_BUBBLE_NULL3(>(x2[6], x1[6]), java.lang.Object(List(EOC, java.lang.Object(List(EOC, x0[6], x1[6])), x2[6])))), ≥)∧[(19)bni_66 + (-1)Bound*bni_66] + [(16)bni_66]x0[6] ≥ 0∧[(-1)bso_67] ≥ 0)
(41) (0 ≥ 0 ⇒ (UIncreasing(COND_4340_0_BUBBLE_NULL3(>(x2[6], x1[6]), java.lang.Object(List(EOC, java.lang.Object(List(EOC, x0[6], x1[6])), x2[6])))), ≥)∧[(19)bni_66 + (-1)Bound*bni_66] + [(16)bni_66]x0[6] ≥ 0∧[(-1)bso_67] ≥ 0)
(42) (0 ≥ 0 ⇒ (UIncreasing(COND_4340_0_BUBBLE_NULL3(>(x2[6], x1[6]), java.lang.Object(List(EOC, java.lang.Object(List(EOC, x0[6], x1[6])), x2[6])))), ≥)∧0 ≥ 0∧0 ≥ 0∧[(16)bni_66] ≥ 0∧[(19)bni_66 + (-1)Bound*bni_66] ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[(-1)bso_67] ≥ 0)
(43) (>(x2[6], x1[6])=TRUE∧java.lang.Object(List(EOC, java.lang.Object(List(EOC, x0[6], x1[6])), x2[6]))=java.lang.Object(List(EOC, java.lang.Object(List(EOC, x0[7], x1[7])), x2[7])) ⇒ COND_4340_0_BUBBLE_NULL3(TRUE, java.lang.Object(List(EOC, java.lang.Object(List(EOC, x0[7], x1[7])), x2[7])))≥NonInfC∧COND_4340_0_BUBBLE_NULL3(TRUE, java.lang.Object(List(EOC, java.lang.Object(List(EOC, x0[7], x1[7])), x2[7])))≥4340_0_BUBBLE_NULL(java.lang.Object(List(EOC, x0[7], x2[7])))∧(UIncreasing(4340_0_BUBBLE_NULL(java.lang.Object(List(EOC, x0[7], x2[7])))), ≥))
(44) (>(x2[6], x1[6])=TRUE ⇒ COND_4340_0_BUBBLE_NULL3(TRUE, java.lang.Object(List(EOC, java.lang.Object(List(EOC, x0[6], x1[6])), x2[6])))≥NonInfC∧COND_4340_0_BUBBLE_NULL3(TRUE, java.lang.Object(List(EOC, java.lang.Object(List(EOC, x0[6], x1[6])), x2[6])))≥4340_0_BUBBLE_NULL(java.lang.Object(List(EOC, x0[6], x2[6])))∧(UIncreasing(4340_0_BUBBLE_NULL(java.lang.Object(List(EOC, x0[7], x2[7])))), ≥))
(45) (0 ≥ 0 ⇒ (UIncreasing(4340_0_BUBBLE_NULL(java.lang.Object(List(EOC, x0[7], x2[7])))), ≥)∧[(19)bni_68 + (-1)Bound*bni_68] + [(16)bni_68]x0[6] ≥ 0∧[16 + (-1)bso_69] + [12]x0[6] ≥ 0)
(46) (0 ≥ 0 ⇒ (UIncreasing(4340_0_BUBBLE_NULL(java.lang.Object(List(EOC, x0[7], x2[7])))), ≥)∧[(19)bni_68 + (-1)Bound*bni_68] + [(16)bni_68]x0[6] ≥ 0∧[16 + (-1)bso_69] + [12]x0[6] ≥ 0)
(47) (0 ≥ 0 ⇒ (UIncreasing(4340_0_BUBBLE_NULL(java.lang.Object(List(EOC, x0[7], x2[7])))), ≥)∧[(19)bni_68 + (-1)Bound*bni_68] + [(16)bni_68]x0[6] ≥ 0∧[16 + (-1)bso_69] + [12]x0[6] ≥ 0)
(48) (0 ≥ 0 ⇒ (UIncreasing(4340_0_BUBBLE_NULL(java.lang.Object(List(EOC, x0[7], x2[7])))), ≥)∧0 ≥ 0∧0 ≥ 0∧[(16)bni_68] ≥ 0∧[(19)bni_68 + (-1)Bound*bni_68] ≥ 0∧0 ≥ 0∧0 ≥ 0∧[16 + (-1)bso_69] ≥ 0∧[1] ≥ 0)
POL(TRUE) = 0
POL(FALSE) = 0
POL(8177_1_bubble_InvokeMethod(x1, x2)) = 0
POL(4580_0_bubble_Return(x1)) = 0
POL(java.lang.Object(x1)) = [2]x1
POL(List(x1, x2, x3)) = [2]x2 + [2]x1
POL(EOC) = [1]
POL(NULL) = 0
POL(8255_0_bubble_Return) = 0
POL(8175_0_bubble_Return) = 0
POL(8601_0_bubble_Return) = 0
POL(8205_1_bubble_InvokeMethod(x1, x2)) = 0
POL(8259_0_bubble_Return) = 0
POL(8622_0_bubble_Return) = 0
POL(8145_1_bubble_InvokeMethod(x1, x2)) = 0
POL(8233_0_bubble_Return) = 0
POL(8577_0_bubble_Return) = 0
POL(8096_1_bubble_InvokeMethod(x1, x2)) = 0
POL(8557_0_bubble_Return) = 0
POL(4340_0_bubble_NULL(x1)) = 0
POL(4383_0_bubble_Return) = 0
POL(4619_0_bubble_Return(x1)) = 0
POL(4650_0_bubble_Return(x1)) = 0
POL(4673_0_bubble_Return(x1)) = 0
POL(4340_0_BUBBLE_NULL(x1)) = [-1] + x1
POL(COND_4340_0_BUBBLE_NULL(x1, x2)) = [-1] + x2
POL(<=(x1, x2)) = 0
POL(COND_4340_0_BUBBLE_NULL1(x1, x2)) = [-1] + x2
POL(>(x1, x2)) = 0
POL(COND_4340_0_BUBBLE_NULL2(x1, x2)) = [-1] + x2
POL(COND_4340_0_BUBBLE_NULL3(x1, x2)) = [-1] + x2
COND_4340_0_BUBBLE_NULL(TRUE, java.lang.Object(List(x0[1], java.lang.Object(List(EOC, x1[1], x2[1])), x3[1]))) → 4340_0_BUBBLE_NULL(java.lang.Object(List(EOC, x1[1], x2[1])))
COND_4340_0_BUBBLE_NULL1(TRUE, java.lang.Object(List(x0[3], java.lang.Object(List(EOC, x1[3], x2[3])), x3[3]))) → 4340_0_BUBBLE_NULL(java.lang.Object(List(EOC, x1[3], x3[3])))
COND_4340_0_BUBBLE_NULL2(TRUE, java.lang.Object(List(EOC, java.lang.Object(List(EOC, x0[5], x1[5])), x2[5]))) → 4340_0_BUBBLE_NULL(java.lang.Object(List(EOC, x0[5], x1[5])))
COND_4340_0_BUBBLE_NULL3(TRUE, java.lang.Object(List(EOC, java.lang.Object(List(EOC, x0[7], x1[7])), x2[7]))) → 4340_0_BUBBLE_NULL(java.lang.Object(List(EOC, x0[7], x2[7])))
4340_0_BUBBLE_NULL(java.lang.Object(List(x0[0], java.lang.Object(List(EOC, x1[0], x2[0])), x3[0]))) → COND_4340_0_BUBBLE_NULL(<=(x3[0], x2[0]), java.lang.Object(List(x0[0], java.lang.Object(List(EOC, x1[0], x2[0])), x3[0])))
COND_4340_0_BUBBLE_NULL(TRUE, java.lang.Object(List(x0[1], java.lang.Object(List(EOC, x1[1], x2[1])), x3[1]))) → 4340_0_BUBBLE_NULL(java.lang.Object(List(EOC, x1[1], x2[1])))
4340_0_BUBBLE_NULL(java.lang.Object(List(x0[2], java.lang.Object(List(EOC, x1[2], x2[2])), x3[2]))) → COND_4340_0_BUBBLE_NULL1(>(x3[2], x2[2]), java.lang.Object(List(x0[2], java.lang.Object(List(EOC, x1[2], x2[2])), x3[2])))
COND_4340_0_BUBBLE_NULL1(TRUE, java.lang.Object(List(x0[3], java.lang.Object(List(EOC, x1[3], x2[3])), x3[3]))) → 4340_0_BUBBLE_NULL(java.lang.Object(List(EOC, x1[3], x3[3])))
4340_0_BUBBLE_NULL(java.lang.Object(List(EOC, java.lang.Object(List(EOC, x0[4], x1[4])), x2[4]))) → COND_4340_0_BUBBLE_NULL2(<=(x2[4], x1[4]), java.lang.Object(List(EOC, java.lang.Object(List(EOC, x0[4], x1[4])), x2[4])))
COND_4340_0_BUBBLE_NULL2(TRUE, java.lang.Object(List(EOC, java.lang.Object(List(EOC, x0[5], x1[5])), x2[5]))) → 4340_0_BUBBLE_NULL(java.lang.Object(List(EOC, x0[5], x1[5])))
4340_0_BUBBLE_NULL(java.lang.Object(List(EOC, java.lang.Object(List(EOC, x0[6], x1[6])), x2[6]))) → COND_4340_0_BUBBLE_NULL3(>(x2[6], x1[6]), java.lang.Object(List(EOC, java.lang.Object(List(EOC, x0[6], x1[6])), x2[6])))
COND_4340_0_BUBBLE_NULL3(TRUE, java.lang.Object(List(EOC, java.lang.Object(List(EOC, x0[7], x1[7])), x2[7]))) → 4340_0_BUBBLE_NULL(java.lang.Object(List(EOC, x0[7], x2[7])))
4340_0_BUBBLE_NULL(java.lang.Object(List(x0[0], java.lang.Object(List(EOC, x1[0], x2[0])), x3[0]))) → COND_4340_0_BUBBLE_NULL(<=(x3[0], x2[0]), java.lang.Object(List(x0[0], java.lang.Object(List(EOC, x1[0], x2[0])), x3[0])))
4340_0_BUBBLE_NULL(java.lang.Object(List(x0[2], java.lang.Object(List(EOC, x1[2], x2[2])), x3[2]))) → COND_4340_0_BUBBLE_NULL1(>(x3[2], x2[2]), java.lang.Object(List(x0[2], java.lang.Object(List(EOC, x1[2], x2[2])), x3[2])))
4340_0_BUBBLE_NULL(java.lang.Object(List(EOC, java.lang.Object(List(EOC, x0[4], x1[4])), x2[4]))) → COND_4340_0_BUBBLE_NULL2(<=(x2[4], x1[4]), java.lang.Object(List(EOC, java.lang.Object(List(EOC, x0[4], x1[4])), x2[4])))
4340_0_BUBBLE_NULL(java.lang.Object(List(EOC, java.lang.Object(List(EOC, x0[6], x1[6])), x2[6]))) → COND_4340_0_BUBBLE_NULL3(>(x2[6], x1[6]), java.lang.Object(List(EOC, java.lang.Object(List(EOC, x0[6], x1[6])), x2[6])))
| != | ~ | 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 |
(0) -> (0), if ((x1[0] →* java.lang.Object(List(x0[0]', x1[0]'))))
(0) -> (1), if ((x1[0] →* java.lang.Object(List(EOC, x0[1]))))
(1) -> (0), if ((x0[1] →* java.lang.Object(List(x0[0], x1[0]))))
(1) -> (1), if ((x0[1] →* java.lang.Object(List(EOC, x0[1]'))))
2393_0_LENGTH_NONNULL(java.lang.Object(List(x0[0], x1[0]))) → 2393_0_LENGTH_NONNULL(x1[0])
2393_0_LENGTH_NONNULL(java.lang.Object(List(EOC, x0[1]))) → 2393_0_LENGTH_NONNULL(x0[1])
2540_1_length_InvokeMethod(2643_0_length_Return, java.lang.Object(List(EOC, NULL))) → 3981_0_length_Return
2578_1_length_InvokeMethod(2643_0_length_Return, java.lang.Object(List(EOC, NULL))) → 4014_0_length_Return
2618_1_length_InvokeMethod(2643_0_length_Return, java.lang.Object(List(EOC, NULL))) → 4077_0_length_Return
2598_1_length_InvokeMethod(2643_0_length_Return, java.lang.Object(List(EOC, NULL))) → 4046_0_length_Return
2393_0_length_NONNULL(NULL) → 2421_0_length_Return
2598_1_length_InvokeMethod(2421_0_length_Return, NULL) → 2718_0_length_Return
2598_1_length_InvokeMethod(2680_0_length_Return, java.lang.Object(List(EOC, NULL))) → 4046_0_length_Return
2598_1_length_InvokeMethod(2718_0_length_Return, java.lang.Object(List(EOC, NULL))) → 4046_0_length_Return
2598_1_length_InvokeMethod(2734_0_length_Return, java.lang.Object(List(EOC, NULL))) → 4046_0_length_Return
2598_1_length_InvokeMethod(3981_0_length_Return, java.lang.Object(List(EOC, java.lang.Object(List(EOC, x0))))) → 4046_0_length_Return
2598_1_length_InvokeMethod(4014_0_length_Return, java.lang.Object(List(EOC, java.lang.Object(List(EOC, x0))))) → 4046_0_length_Return
2598_1_length_InvokeMethod(4046_0_length_Return, java.lang.Object(List(EOC, java.lang.Object(List(EOC, x0))))) → 4046_0_length_Return
2598_1_length_InvokeMethod(4077_0_length_Return, java.lang.Object(List(EOC, java.lang.Object(List(EOC, x0))))) → 4046_0_length_Return
2618_1_length_InvokeMethod(2421_0_length_Return, NULL) → 2734_0_length_Return
2618_1_length_InvokeMethod(2680_0_length_Return, java.lang.Object(List(EOC, NULL))) → 4077_0_length_Return
2618_1_length_InvokeMethod(2718_0_length_Return, java.lang.Object(List(EOC, NULL))) → 4077_0_length_Return
2618_1_length_InvokeMethod(2734_0_length_Return, java.lang.Object(List(EOC, NULL))) → 4077_0_length_Return
2618_1_length_InvokeMethod(3981_0_length_Return, java.lang.Object(List(EOC, java.lang.Object(List(EOC, x0))))) → 4077_0_length_Return
2618_1_length_InvokeMethod(4014_0_length_Return, java.lang.Object(List(EOC, java.lang.Object(List(EOC, x0))))) → 4077_0_length_Return
2618_1_length_InvokeMethod(4046_0_length_Return, java.lang.Object(List(EOC, java.lang.Object(List(EOC, x0))))) → 4077_0_length_Return
2618_1_length_InvokeMethod(4077_0_length_Return, java.lang.Object(List(EOC, java.lang.Object(List(EOC, x0))))) → 4077_0_length_Return
2578_1_length_InvokeMethod(2421_0_length_Return, NULL) → 2680_0_length_Return
2578_1_length_InvokeMethod(2680_0_length_Return, java.lang.Object(List(EOC, NULL))) → 4014_0_length_Return
2578_1_length_InvokeMethod(2718_0_length_Return, java.lang.Object(List(EOC, NULL))) → 4014_0_length_Return
2578_1_length_InvokeMethod(2734_0_length_Return, java.lang.Object(List(EOC, NULL))) → 4014_0_length_Return
2578_1_length_InvokeMethod(3981_0_length_Return, java.lang.Object(List(EOC, java.lang.Object(List(EOC, x0))))) → 4014_0_length_Return
2578_1_length_InvokeMethod(4014_0_length_Return, java.lang.Object(List(EOC, java.lang.Object(List(EOC, x0))))) → 4014_0_length_Return
2578_1_length_InvokeMethod(4046_0_length_Return, java.lang.Object(List(EOC, java.lang.Object(List(EOC, x0))))) → 4014_0_length_Return
2578_1_length_InvokeMethod(4077_0_length_Return, java.lang.Object(List(EOC, java.lang.Object(List(EOC, x0))))) → 4014_0_length_Return
2540_1_length_InvokeMethod(2421_0_length_Return, NULL) → 2643_0_length_Return
2540_1_length_InvokeMethod(2680_0_length_Return, java.lang.Object(List(EOC, NULL))) → 3981_0_length_Return
2540_1_length_InvokeMethod(2718_0_length_Return, java.lang.Object(List(EOC, NULL))) → 3981_0_length_Return
2540_1_length_InvokeMethod(2734_0_length_Return, java.lang.Object(List(EOC, NULL))) → 3981_0_length_Return
2540_1_length_InvokeMethod(3981_0_length_Return, java.lang.Object(List(EOC, java.lang.Object(List(EOC, x0))))) → 3981_0_length_Return
2540_1_length_InvokeMethod(4014_0_length_Return, java.lang.Object(List(EOC, java.lang.Object(List(EOC, x0))))) → 3981_0_length_Return
2540_1_length_InvokeMethod(4046_0_length_Return, java.lang.Object(List(EOC, java.lang.Object(List(EOC, x0))))) → 3981_0_length_Return
2540_1_length_InvokeMethod(4077_0_length_Return, java.lang.Object(List(EOC, java.lang.Object(List(EOC, x0))))) → 3981_0_length_Return
2540_1_length_InvokeMethod(2643_0_length_Return, java.lang.Object(List(EOC, NULL)))
2578_1_length_InvokeMethod(2643_0_length_Return, java.lang.Object(List(EOC, NULL)))
2618_1_length_InvokeMethod(2643_0_length_Return, java.lang.Object(List(EOC, NULL)))
2598_1_length_InvokeMethod(2643_0_length_Return, java.lang.Object(List(EOC, NULL)))
2393_0_length_NONNULL(NULL)
2598_1_length_InvokeMethod(2421_0_length_Return, NULL)
2598_1_length_InvokeMethod(2680_0_length_Return, java.lang.Object(List(EOC, NULL)))
2598_1_length_InvokeMethod(2718_0_length_Return, java.lang.Object(List(EOC, NULL)))
2598_1_length_InvokeMethod(2734_0_length_Return, java.lang.Object(List(EOC, NULL)))
2598_1_length_InvokeMethod(3981_0_length_Return, java.lang.Object(List(EOC, java.lang.Object(List(EOC, x0)))))
2598_1_length_InvokeMethod(4014_0_length_Return, java.lang.Object(List(EOC, java.lang.Object(List(EOC, x0)))))
2598_1_length_InvokeMethod(4046_0_length_Return, java.lang.Object(List(EOC, java.lang.Object(List(EOC, x0)))))
2598_1_length_InvokeMethod(4077_0_length_Return, java.lang.Object(List(EOC, java.lang.Object(List(EOC, x0)))))
2618_1_length_InvokeMethod(2421_0_length_Return, NULL)
2618_1_length_InvokeMethod(2680_0_length_Return, java.lang.Object(List(EOC, NULL)))
2618_1_length_InvokeMethod(2718_0_length_Return, java.lang.Object(List(EOC, NULL)))
2618_1_length_InvokeMethod(2734_0_length_Return, java.lang.Object(List(EOC, NULL)))
2618_1_length_InvokeMethod(3981_0_length_Return, java.lang.Object(List(EOC, java.lang.Object(List(EOC, x0)))))
2618_1_length_InvokeMethod(4014_0_length_Return, java.lang.Object(List(EOC, java.lang.Object(List(EOC, x0)))))
2618_1_length_InvokeMethod(4046_0_length_Return, java.lang.Object(List(EOC, java.lang.Object(List(EOC, x0)))))
2618_1_length_InvokeMethod(4077_0_length_Return, java.lang.Object(List(EOC, java.lang.Object(List(EOC, x0)))))
2578_1_length_InvokeMethod(2421_0_length_Return, NULL)
2578_1_length_InvokeMethod(2680_0_length_Return, java.lang.Object(List(EOC, NULL)))
2578_1_length_InvokeMethod(2718_0_length_Return, java.lang.Object(List(EOC, NULL)))
2578_1_length_InvokeMethod(2734_0_length_Return, java.lang.Object(List(EOC, NULL)))
2578_1_length_InvokeMethod(3981_0_length_Return, java.lang.Object(List(EOC, java.lang.Object(List(EOC, x0)))))
2578_1_length_InvokeMethod(4014_0_length_Return, java.lang.Object(List(EOC, java.lang.Object(List(EOC, x0)))))
2578_1_length_InvokeMethod(4046_0_length_Return, java.lang.Object(List(EOC, java.lang.Object(List(EOC, x0)))))
2578_1_length_InvokeMethod(4077_0_length_Return, java.lang.Object(List(EOC, java.lang.Object(List(EOC, x0)))))
2540_1_length_InvokeMethod(2421_0_length_Return, NULL)
2540_1_length_InvokeMethod(2680_0_length_Return, java.lang.Object(List(EOC, NULL)))
2540_1_length_InvokeMethod(2718_0_length_Return, java.lang.Object(List(EOC, NULL)))
2540_1_length_InvokeMethod(2734_0_length_Return, java.lang.Object(List(EOC, NULL)))
2540_1_length_InvokeMethod(3981_0_length_Return, java.lang.Object(List(EOC, java.lang.Object(List(EOC, x0)))))
2540_1_length_InvokeMethod(4014_0_length_Return, java.lang.Object(List(EOC, java.lang.Object(List(EOC, x0)))))
2540_1_length_InvokeMethod(4046_0_length_Return, java.lang.Object(List(EOC, java.lang.Object(List(EOC, x0)))))
2540_1_length_InvokeMethod(4077_0_length_Return, java.lang.Object(List(EOC, java.lang.Object(List(EOC, x0)))))
2393_0_LENGTH_NONNULL(java.lang.Object(List(x0[0], x1[0]))) → 2393_0_LENGTH_NONNULL(x1[0])
2393_0_LENGTH_NONNULL(java.lang.Object(List(EOC, x0[1]))) → 2393_0_LENGTH_NONNULL(x0[1])
2540_1_length_InvokeMethod(2643_0_length_Return, java.lang.Object(List(EOC, NULL)))
2578_1_length_InvokeMethod(2643_0_length_Return, java.lang.Object(List(EOC, NULL)))
2618_1_length_InvokeMethod(2643_0_length_Return, java.lang.Object(List(EOC, NULL)))
2598_1_length_InvokeMethod(2643_0_length_Return, java.lang.Object(List(EOC, NULL)))
2393_0_length_NONNULL(NULL)
2598_1_length_InvokeMethod(2421_0_length_Return, NULL)
2598_1_length_InvokeMethod(2680_0_length_Return, java.lang.Object(List(EOC, NULL)))
2598_1_length_InvokeMethod(2718_0_length_Return, java.lang.Object(List(EOC, NULL)))
2598_1_length_InvokeMethod(2734_0_length_Return, java.lang.Object(List(EOC, NULL)))
2598_1_length_InvokeMethod(3981_0_length_Return, java.lang.Object(List(EOC, java.lang.Object(List(EOC, x0)))))
2598_1_length_InvokeMethod(4014_0_length_Return, java.lang.Object(List(EOC, java.lang.Object(List(EOC, x0)))))
2598_1_length_InvokeMethod(4046_0_length_Return, java.lang.Object(List(EOC, java.lang.Object(List(EOC, x0)))))
2598_1_length_InvokeMethod(4077_0_length_Return, java.lang.Object(List(EOC, java.lang.Object(List(EOC, x0)))))
2618_1_length_InvokeMethod(2421_0_length_Return, NULL)
2618_1_length_InvokeMethod(2680_0_length_Return, java.lang.Object(List(EOC, NULL)))
2618_1_length_InvokeMethod(2718_0_length_Return, java.lang.Object(List(EOC, NULL)))
2618_1_length_InvokeMethod(2734_0_length_Return, java.lang.Object(List(EOC, NULL)))
2618_1_length_InvokeMethod(3981_0_length_Return, java.lang.Object(List(EOC, java.lang.Object(List(EOC, x0)))))
2618_1_length_InvokeMethod(4014_0_length_Return, java.lang.Object(List(EOC, java.lang.Object(List(EOC, x0)))))
2618_1_length_InvokeMethod(4046_0_length_Return, java.lang.Object(List(EOC, java.lang.Object(List(EOC, x0)))))
2618_1_length_InvokeMethod(4077_0_length_Return, java.lang.Object(List(EOC, java.lang.Object(List(EOC, x0)))))
2578_1_length_InvokeMethod(2421_0_length_Return, NULL)
2578_1_length_InvokeMethod(2680_0_length_Return, java.lang.Object(List(EOC, NULL)))
2578_1_length_InvokeMethod(2718_0_length_Return, java.lang.Object(List(EOC, NULL)))
2578_1_length_InvokeMethod(2734_0_length_Return, java.lang.Object(List(EOC, NULL)))
2578_1_length_InvokeMethod(3981_0_length_Return, java.lang.Object(List(EOC, java.lang.Object(List(EOC, x0)))))
2578_1_length_InvokeMethod(4014_0_length_Return, java.lang.Object(List(EOC, java.lang.Object(List(EOC, x0)))))
2578_1_length_InvokeMethod(4046_0_length_Return, java.lang.Object(List(EOC, java.lang.Object(List(EOC, x0)))))
2578_1_length_InvokeMethod(4077_0_length_Return, java.lang.Object(List(EOC, java.lang.Object(List(EOC, x0)))))
2540_1_length_InvokeMethod(2421_0_length_Return, NULL)
2540_1_length_InvokeMethod(2680_0_length_Return, java.lang.Object(List(EOC, NULL)))
2540_1_length_InvokeMethod(2718_0_length_Return, java.lang.Object(List(EOC, NULL)))
2540_1_length_InvokeMethod(2734_0_length_Return, java.lang.Object(List(EOC, NULL)))
2540_1_length_InvokeMethod(3981_0_length_Return, java.lang.Object(List(EOC, java.lang.Object(List(EOC, x0)))))
2540_1_length_InvokeMethod(4014_0_length_Return, java.lang.Object(List(EOC, java.lang.Object(List(EOC, x0)))))
2540_1_length_InvokeMethod(4046_0_length_Return, java.lang.Object(List(EOC, java.lang.Object(List(EOC, x0)))))
2540_1_length_InvokeMethod(4077_0_length_Return, java.lang.Object(List(EOC, java.lang.Object(List(EOC, x0)))))
2540_1_length_InvokeMethod(2643_0_length_Return, java.lang.Object(List(EOC, NULL)))
2578_1_length_InvokeMethod(2643_0_length_Return, java.lang.Object(List(EOC, NULL)))
2618_1_length_InvokeMethod(2643_0_length_Return, java.lang.Object(List(EOC, NULL)))
2598_1_length_InvokeMethod(2643_0_length_Return, java.lang.Object(List(EOC, NULL)))
2393_0_length_NONNULL(NULL)
2598_1_length_InvokeMethod(2421_0_length_Return, NULL)
2598_1_length_InvokeMethod(2680_0_length_Return, java.lang.Object(List(EOC, NULL)))
2598_1_length_InvokeMethod(2718_0_length_Return, java.lang.Object(List(EOC, NULL)))
2598_1_length_InvokeMethod(2734_0_length_Return, java.lang.Object(List(EOC, NULL)))
2598_1_length_InvokeMethod(3981_0_length_Return, java.lang.Object(List(EOC, java.lang.Object(List(EOC, x0)))))
2598_1_length_InvokeMethod(4014_0_length_Return, java.lang.Object(List(EOC, java.lang.Object(List(EOC, x0)))))
2598_1_length_InvokeMethod(4046_0_length_Return, java.lang.Object(List(EOC, java.lang.Object(List(EOC, x0)))))
2598_1_length_InvokeMethod(4077_0_length_Return, java.lang.Object(List(EOC, java.lang.Object(List(EOC, x0)))))
2618_1_length_InvokeMethod(2421_0_length_Return, NULL)
2618_1_length_InvokeMethod(2680_0_length_Return, java.lang.Object(List(EOC, NULL)))
2618_1_length_InvokeMethod(2718_0_length_Return, java.lang.Object(List(EOC, NULL)))
2618_1_length_InvokeMethod(2734_0_length_Return, java.lang.Object(List(EOC, NULL)))
2618_1_length_InvokeMethod(3981_0_length_Return, java.lang.Object(List(EOC, java.lang.Object(List(EOC, x0)))))
2618_1_length_InvokeMethod(4014_0_length_Return, java.lang.Object(List(EOC, java.lang.Object(List(EOC, x0)))))
2618_1_length_InvokeMethod(4046_0_length_Return, java.lang.Object(List(EOC, java.lang.Object(List(EOC, x0)))))
2618_1_length_InvokeMethod(4077_0_length_Return, java.lang.Object(List(EOC, java.lang.Object(List(EOC, x0)))))
2578_1_length_InvokeMethod(2421_0_length_Return, NULL)
2578_1_length_InvokeMethod(2680_0_length_Return, java.lang.Object(List(EOC, NULL)))
2578_1_length_InvokeMethod(2718_0_length_Return, java.lang.Object(List(EOC, NULL)))
2578_1_length_InvokeMethod(2734_0_length_Return, java.lang.Object(List(EOC, NULL)))
2578_1_length_InvokeMethod(3981_0_length_Return, java.lang.Object(List(EOC, java.lang.Object(List(EOC, x0)))))
2578_1_length_InvokeMethod(4014_0_length_Return, java.lang.Object(List(EOC, java.lang.Object(List(EOC, x0)))))
2578_1_length_InvokeMethod(4046_0_length_Return, java.lang.Object(List(EOC, java.lang.Object(List(EOC, x0)))))
2578_1_length_InvokeMethod(4077_0_length_Return, java.lang.Object(List(EOC, java.lang.Object(List(EOC, x0)))))
2540_1_length_InvokeMethod(2421_0_length_Return, NULL)
2540_1_length_InvokeMethod(2680_0_length_Return, java.lang.Object(List(EOC, NULL)))
2540_1_length_InvokeMethod(2718_0_length_Return, java.lang.Object(List(EOC, NULL)))
2540_1_length_InvokeMethod(2734_0_length_Return, java.lang.Object(List(EOC, NULL)))
2540_1_length_InvokeMethod(3981_0_length_Return, java.lang.Object(List(EOC, java.lang.Object(List(EOC, x0)))))
2540_1_length_InvokeMethod(4014_0_length_Return, java.lang.Object(List(EOC, java.lang.Object(List(EOC, x0)))))
2540_1_length_InvokeMethod(4046_0_length_Return, java.lang.Object(List(EOC, java.lang.Object(List(EOC, x0)))))
2540_1_length_InvokeMethod(4077_0_length_Return, java.lang.Object(List(EOC, java.lang.Object(List(EOC, x0)))))
2393_0_LENGTH_NONNULL(java.lang.Object(List(x0[0], x1[0]))) → 2393_0_LENGTH_NONNULL(x1[0])
2393_0_LENGTH_NONNULL(java.lang.Object(List(EOC, x0[1]))) → 2393_0_LENGTH_NONNULL(x0[1])
From the DPs we obtained the following set of size-change graphs:
| != | ~ | 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 ((x6[0] < x5[0] && x4[0] >= 0 && x4[0] <= 2 →* TRUE)∧(java.lang.Object(ARRAY(DATA_3(x1[0], x2[0], x3[0]))) →* java.lang.Object(ARRAY(DATA_3(x1[1], x2[1], x3[1]))))∧(x4[0] →* x4[1])∧(x6[0] →* x6[1])∧(x5[0] →* x5[1]))
(1) -> (2), if ((7152_0_bubble_Load(x7[1]) →* 4383_0_bubble_Return)∧(java.lang.Object(ARRAY(DATA_3(x1[1], x2[1], x3[1]))) →* java.lang.Object(ARRAY(DATA_3(x1[2], x2[2], x3[2]))))∧(x4[1] →* x4[2])∧(x5[1] →* x5[2])∧(x6[1] →* x6[2])∧(x7[1] →* NULL))
(1) -> (4), if ((7152_0_bubble_Load(x7[1]) →* 4580_0_bubble_Return)∧(java.lang.Object(ARRAY(DATA_3(x1[1], x2[1], x3[1]))) →* java.lang.Object(ARRAY(DATA_3(x1[4], x2[4], x3[4]))))∧(x4[1] →* x4[4])∧(x5[1] →* x5[4])∧(x6[1] →* x6[4])∧(x7[1] →* java.lang.Object(List(EOC))))
(1) -> (6), if ((7152_0_bubble_Load(x7[1]) →* 4619_0_bubble_Return)∧(java.lang.Object(ARRAY(DATA_3(x1[1], x2[1], x3[1]))) →* java.lang.Object(ARRAY(DATA_3(x1[6], x2[6], x3[6]))))∧(x4[1] →* x4[6])∧(x5[1] →* x5[6])∧(x6[1] →* x6[6])∧(x7[1] →* java.lang.Object(List(EOC))))
(1) -> (8), if ((7152_0_bubble_Load(x7[1]) →* 4650_0_bubble_Return(java.lang.Object(List(x0[8]))))∧(java.lang.Object(ARRAY(DATA_3(x1[1], x2[1], x3[1]))) →* java.lang.Object(ARRAY(DATA_3(x2[8], x3[8], x4[8]))))∧(x4[1] →* x5[8])∧(x5[1] →* x6[8])∧(x6[1] →* x7[8])∧(x7[1] →* java.lang.Object(List(x0[8]))))
(1) -> (10), if ((7152_0_bubble_Load(x7[1]) →* 4673_0_bubble_Return)∧(java.lang.Object(ARRAY(DATA_3(x1[1], x2[1], x3[1]))) →* java.lang.Object(ARRAY(DATA_3(x1[10], x2[10], x3[10]))))∧(x4[1] →* x4[10])∧(x5[1] →* x5[10])∧(x6[1] →* x6[10])∧(x7[1] →* java.lang.Object(List(EOC))))
(1) -> (12), if ((7152_0_bubble_Load(x7[1]) →* 8175_0_bubble_Return)∧(java.lang.Object(ARRAY(DATA_3(x1[1], x2[1], x3[1]))) →* java.lang.Object(ARRAY(DATA_3(x1[12], x2[12], x3[12]))))∧(x4[1] →* x4[12])∧(x5[1] →* x5[12])∧(x6[1] →* x6[12])∧(x7[1] →* x7[12]))
(1) -> (14), if ((7152_0_bubble_Load(x7[1]) →* 8233_0_bubble_Return)∧(java.lang.Object(ARRAY(DATA_3(x1[1], x2[1], x3[1]))) →* java.lang.Object(ARRAY(DATA_3(x1[14], x2[14], x3[14]))))∧(x4[1] →* x4[14])∧(x5[1] →* x5[14])∧(x6[1] →* x6[14])∧(x7[1] →* x7[14]))
(1) -> (16), if ((7152_0_bubble_Load(x7[1]) →* 8255_0_bubble_Return)∧(java.lang.Object(ARRAY(DATA_3(x1[1], x2[1], x3[1]))) →* java.lang.Object(ARRAY(DATA_3(x1[16], x2[16], x3[16]))))∧(x4[1] →* x4[16])∧(x5[1] →* x5[16])∧(x6[1] →* x6[16])∧(x7[1] →* x7[16]))
(1) -> (18), if ((7152_0_bubble_Load(x7[1]) →* 8259_0_bubble_Return)∧(java.lang.Object(ARRAY(DATA_3(x1[1], x2[1], x3[1]))) →* java.lang.Object(ARRAY(DATA_3(x1[18], x2[18], x3[18]))))∧(x4[1] →* x4[18])∧(x5[1] →* x5[18])∧(x6[1] →* x6[18])∧(x7[1] →* x7[18]))
(1) -> (20), if ((7152_0_bubble_Load(x7[1]) →* 8557_0_bubble_Return)∧(java.lang.Object(ARRAY(DATA_3(x1[1], x2[1], x3[1]))) →* java.lang.Object(ARRAY(DATA_3(x1[20], x2[20], x3[20]))))∧(x4[1] →* x4[20])∧(x5[1] →* x5[20])∧(x6[1] →* x6[20])∧(x7[1] →* x7[20]))
(1) -> (22), if ((7152_0_bubble_Load(x7[1]) →* 8577_0_bubble_Return)∧(java.lang.Object(ARRAY(DATA_3(x1[1], x2[1], x3[1]))) →* java.lang.Object(ARRAY(DATA_3(x1[22], x2[22], x3[22]))))∧(x4[1] →* x4[22])∧(x5[1] →* x5[22])∧(x6[1] →* x6[22])∧(x7[1] →* x7[22]))
(1) -> (24), if ((7152_0_bubble_Load(x7[1]) →* 8601_0_bubble_Return)∧(java.lang.Object(ARRAY(DATA_3(x1[1], x2[1], x3[1]))) →* java.lang.Object(ARRAY(DATA_3(x1[24], x2[24], x3[24]))))∧(x4[1] →* x4[24])∧(x5[1] →* x5[24])∧(x6[1] →* x6[24])∧(x7[1] →* x7[24]))
(1) -> (26), if ((7152_0_bubble_Load(x7[1]) →* 8622_0_bubble_Return)∧(java.lang.Object(ARRAY(DATA_3(x1[1], x2[1], x3[1]))) →* java.lang.Object(ARRAY(DATA_3(x1[26], x2[26], x3[26]))))∧(x4[1] →* x4[26])∧(x5[1] →* x5[26])∧(x6[1] →* x6[26])∧(x7[1] →* x7[26]))
(2) -> (3), if ((x6[2] >= 0 →* TRUE)∧(java.lang.Object(ARRAY(DATA_3(x1[2], x2[2], x3[2]))) →* java.lang.Object(ARRAY(DATA_3(x1[3], x2[3], x3[3]))))∧(x4[2] →* x4[3])∧(x5[2] →* x5[3])∧(x6[2] →* x6[3]))
(3) -> (0), if ((java.lang.Object(ARRAY(DATA_3(x1[3], x2[3], x3[3]))) →* java.lang.Object(ARRAY(DATA_3(x1[0], x2[0], x3[0]))))∧(x4[3] →* x4[0])∧(x6[3] + 1 →* x6[0])∧(x5[3] →* x5[0]))
(3) -> (28), if ((java.lang.Object(ARRAY(DATA_3(x1[3], x2[3], x3[3]))) →* java.lang.Object(ARRAY(DATA_3(x0[28], x1[28], x2[28]))))∧(x4[3] →* x3[28])∧(x6[3] + 1 →* x4[28])∧(x5[3] →* x5[28]))
(3) -> (30), if ((java.lang.Object(ARRAY(DATA_3(x1[3], x2[3], x3[3]))) →* java.lang.Object(ARRAY(DATA_3(x0[30], x1[30], x2[30]))))∧(x4[3] →* x3[30])∧(x6[3] + 1 →* x4[30])∧(x5[3] →* x5[30]))
(3) -> (32), if ((java.lang.Object(ARRAY(DATA_3(x1[3], x2[3], x3[3]))) →* java.lang.Object(ARRAY(DATA_3(x0[32], x1[32], x2[32]))))∧(x4[3] →* x3[32])∧(x6[3] + 1 →* x4[32])∧(x5[3] →* x5[32]))
(4) -> (5), if ((x6[4] >= 0 →* TRUE)∧(java.lang.Object(ARRAY(DATA_3(x1[4], x2[4], x3[4]))) →* java.lang.Object(ARRAY(DATA_3(x1[5], x2[5], x3[5]))))∧(x4[4] →* x4[5])∧(x5[4] →* x5[5])∧(x6[4] →* x6[5]))
(5) -> (0), if ((java.lang.Object(ARRAY(DATA_3(x1[5], x2[5], x3[5]))) →* java.lang.Object(ARRAY(DATA_3(x1[0], x2[0], x3[0]))))∧(x4[5] →* x4[0])∧(x6[5] + 1 →* x6[0])∧(x5[5] →* x5[0]))
(5) -> (28), if ((java.lang.Object(ARRAY(DATA_3(x1[5], x2[5], x3[5]))) →* java.lang.Object(ARRAY(DATA_3(x0[28], x1[28], x2[28]))))∧(x4[5] →* x3[28])∧(x6[5] + 1 →* x4[28])∧(x5[5] →* x5[28]))
(5) -> (30), if ((java.lang.Object(ARRAY(DATA_3(x1[5], x2[5], x3[5]))) →* java.lang.Object(ARRAY(DATA_3(x0[30], x1[30], x2[30]))))∧(x4[5] →* x3[30])∧(x6[5] + 1 →* x4[30])∧(x5[5] →* x5[30]))
(5) -> (32), if ((java.lang.Object(ARRAY(DATA_3(x1[5], x2[5], x3[5]))) →* java.lang.Object(ARRAY(DATA_3(x0[32], x1[32], x2[32]))))∧(x4[5] →* x3[32])∧(x6[5] + 1 →* x4[32])∧(x5[5] →* x5[32]))
(6) -> (7), if ((x6[6] >= 0 →* TRUE)∧(java.lang.Object(ARRAY(DATA_3(x1[6], x2[6], x3[6]))) →* java.lang.Object(ARRAY(DATA_3(x1[7], x2[7], x3[7]))))∧(x4[6] →* x4[7])∧(x5[6] →* x5[7])∧(x6[6] →* x6[7]))
(7) -> (0), if ((java.lang.Object(ARRAY(DATA_3(x1[7], x2[7], x3[7]))) →* java.lang.Object(ARRAY(DATA_3(x1[0], x2[0], x3[0]))))∧(x4[7] →* x4[0])∧(x6[7] + 1 →* x6[0])∧(x5[7] →* x5[0]))
(7) -> (28), if ((java.lang.Object(ARRAY(DATA_3(x1[7], x2[7], x3[7]))) →* java.lang.Object(ARRAY(DATA_3(x0[28], x1[28], x2[28]))))∧(x4[7] →* x3[28])∧(x6[7] + 1 →* x4[28])∧(x5[7] →* x5[28]))
(7) -> (30), if ((java.lang.Object(ARRAY(DATA_3(x1[7], x2[7], x3[7]))) →* java.lang.Object(ARRAY(DATA_3(x0[30], x1[30], x2[30]))))∧(x4[7] →* x3[30])∧(x6[7] + 1 →* x4[30])∧(x5[7] →* x5[30]))
(7) -> (32), if ((java.lang.Object(ARRAY(DATA_3(x1[7], x2[7], x3[7]))) →* java.lang.Object(ARRAY(DATA_3(x0[32], x1[32], x2[32]))))∧(x4[7] →* x3[32])∧(x6[7] + 1 →* x4[32])∧(x5[7] →* x5[32]))
(8) -> (9), if ((x7[8] >= 0 →* TRUE)∧(4650_0_bubble_Return(java.lang.Object(List(x0[8]))) →* 4650_0_bubble_Return(java.lang.Object(List(x0[9]))))∧(java.lang.Object(ARRAY(DATA_3(x2[8], x3[8], x4[8]))) →* java.lang.Object(ARRAY(DATA_3(x2[9], x3[9], x4[9]))))∧(x5[8] →* x5[9])∧(x6[8] →* x6[9])∧(x7[8] →* x7[9])∧(java.lang.Object(List(x0[8])) →* java.lang.Object(List(x0[9]))))
(9) -> (0), if ((java.lang.Object(ARRAY(DATA_3(x2[9], x3[9], x4[9]))) →* java.lang.Object(ARRAY(DATA_3(x1[0], x2[0], x3[0]))))∧(x5[9] →* x4[0])∧(x7[9] + 1 →* x6[0])∧(x6[9] →* x5[0]))
(9) -> (28), if ((java.lang.Object(ARRAY(DATA_3(x2[9], x3[9], x4[9]))) →* java.lang.Object(ARRAY(DATA_3(x0[28], x1[28], x2[28]))))∧(x5[9] →* x3[28])∧(x7[9] + 1 →* x4[28])∧(x6[9] →* x5[28]))
(9) -> (30), if ((java.lang.Object(ARRAY(DATA_3(x2[9], x3[9], x4[9]))) →* java.lang.Object(ARRAY(DATA_3(x0[30], x1[30], x2[30]))))∧(x5[9] →* x3[30])∧(x7[9] + 1 →* x4[30])∧(x6[9] →* x5[30]))
(9) -> (32), if ((java.lang.Object(ARRAY(DATA_3(x2[9], x3[9], x4[9]))) →* java.lang.Object(ARRAY(DATA_3(x0[32], x1[32], x2[32]))))∧(x5[9] →* x3[32])∧(x7[9] + 1 →* x4[32])∧(x6[9] →* x5[32]))
(10) -> (11), if ((x6[10] >= 0 →* TRUE)∧(java.lang.Object(ARRAY(DATA_3(x1[10], x2[10], x3[10]))) →* java.lang.Object(ARRAY(DATA_3(x1[11], x2[11], x3[11]))))∧(x4[10] →* x4[11])∧(x5[10] →* x5[11])∧(x6[10] →* x6[11]))
(11) -> (0), if ((java.lang.Object(ARRAY(DATA_3(x1[11], x2[11], x3[11]))) →* java.lang.Object(ARRAY(DATA_3(x1[0], x2[0], x3[0]))))∧(x4[11] →* x4[0])∧(x6[11] + 1 →* x6[0])∧(x5[11] →* x5[0]))
(11) -> (28), if ((java.lang.Object(ARRAY(DATA_3(x1[11], x2[11], x3[11]))) →* java.lang.Object(ARRAY(DATA_3(x0[28], x1[28], x2[28]))))∧(x4[11] →* x3[28])∧(x6[11] + 1 →* x4[28])∧(x5[11] →* x5[28]))
(11) -> (30), if ((java.lang.Object(ARRAY(DATA_3(x1[11], x2[11], x3[11]))) →* java.lang.Object(ARRAY(DATA_3(x0[30], x1[30], x2[30]))))∧(x4[11] →* x3[30])∧(x6[11] + 1 →* x4[30])∧(x5[11] →* x5[30]))
(11) -> (32), if ((java.lang.Object(ARRAY(DATA_3(x1[11], x2[11], x3[11]))) →* java.lang.Object(ARRAY(DATA_3(x0[32], x1[32], x2[32]))))∧(x4[11] →* x3[32])∧(x6[11] + 1 →* x4[32])∧(x5[11] →* x5[32]))
(12) -> (13), if ((x6[12] >= 0 →* TRUE)∧(java.lang.Object(ARRAY(DATA_3(x1[12], x2[12], x3[12]))) →* java.lang.Object(ARRAY(DATA_3(x1[13], x2[13], x3[13]))))∧(x4[12] →* x4[13])∧(x5[12] →* x5[13])∧(x6[12] →* x6[13])∧(x7[12] →* x7[13]))
(13) -> (0), if ((java.lang.Object(ARRAY(DATA_3(x1[13], x2[13], x3[13]))) →* java.lang.Object(ARRAY(DATA_3(x1[0], x2[0], x3[0]))))∧(x4[13] →* x4[0])∧(x6[13] + 1 →* x6[0])∧(x5[13] →* x5[0]))
(13) -> (28), if ((java.lang.Object(ARRAY(DATA_3(x1[13], x2[13], x3[13]))) →* java.lang.Object(ARRAY(DATA_3(x0[28], x1[28], x2[28]))))∧(x4[13] →* x3[28])∧(x6[13] + 1 →* x4[28])∧(x5[13] →* x5[28]))
(13) -> (30), if ((java.lang.Object(ARRAY(DATA_3(x1[13], x2[13], x3[13]))) →* java.lang.Object(ARRAY(DATA_3(x0[30], x1[30], x2[30]))))∧(x4[13] →* x3[30])∧(x6[13] + 1 →* x4[30])∧(x5[13] →* x5[30]))
(13) -> (32), if ((java.lang.Object(ARRAY(DATA_3(x1[13], x2[13], x3[13]))) →* java.lang.Object(ARRAY(DATA_3(x0[32], x1[32], x2[32]))))∧(x4[13] →* x3[32])∧(x6[13] + 1 →* x4[32])∧(x5[13] →* x5[32]))
(14) -> (15), if ((x6[14] >= 0 →* TRUE)∧(java.lang.Object(ARRAY(DATA_3(x1[14], x2[14], x3[14]))) →* java.lang.Object(ARRAY(DATA_3(x1[15], x2[15], x3[15]))))∧(x4[14] →* x4[15])∧(x5[14] →* x5[15])∧(x6[14] →* x6[15])∧(x7[14] →* x7[15]))
(15) -> (0), if ((java.lang.Object(ARRAY(DATA_3(x1[15], x2[15], x3[15]))) →* java.lang.Object(ARRAY(DATA_3(x1[0], x2[0], x3[0]))))∧(x4[15] →* x4[0])∧(x6[15] + 1 →* x6[0])∧(x5[15] →* x5[0]))
(15) -> (28), if ((java.lang.Object(ARRAY(DATA_3(x1[15], x2[15], x3[15]))) →* java.lang.Object(ARRAY(DATA_3(x0[28], x1[28], x2[28]))))∧(x4[15] →* x3[28])∧(x6[15] + 1 →* x4[28])∧(x5[15] →* x5[28]))
(15) -> (30), if ((java.lang.Object(ARRAY(DATA_3(x1[15], x2[15], x3[15]))) →* java.lang.Object(ARRAY(DATA_3(x0[30], x1[30], x2[30]))))∧(x4[15] →* x3[30])∧(x6[15] + 1 →* x4[30])∧(x5[15] →* x5[30]))
(15) -> (32), if ((java.lang.Object(ARRAY(DATA_3(x1[15], x2[15], x3[15]))) →* java.lang.Object(ARRAY(DATA_3(x0[32], x1[32], x2[32]))))∧(x4[15] →* x3[32])∧(x6[15] + 1 →* x4[32])∧(x5[15] →* x5[32]))
(16) -> (17), if ((x6[16] >= 0 →* TRUE)∧(java.lang.Object(ARRAY(DATA_3(x1[16], x2[16], x3[16]))) →* java.lang.Object(ARRAY(DATA_3(x1[17], x2[17], x3[17]))))∧(x4[16] →* x4[17])∧(x5[16] →* x5[17])∧(x6[16] →* x6[17])∧(x7[16] →* x7[17]))
(17) -> (0), if ((java.lang.Object(ARRAY(DATA_3(x1[17], x2[17], x3[17]))) →* java.lang.Object(ARRAY(DATA_3(x1[0], x2[0], x3[0]))))∧(x4[17] →* x4[0])∧(x6[17] + 1 →* x6[0])∧(x5[17] →* x5[0]))
(17) -> (28), if ((java.lang.Object(ARRAY(DATA_3(x1[17], x2[17], x3[17]))) →* java.lang.Object(ARRAY(DATA_3(x0[28], x1[28], x2[28]))))∧(x4[17] →* x3[28])∧(x6[17] + 1 →* x4[28])∧(x5[17] →* x5[28]))
(17) -> (30), if ((java.lang.Object(ARRAY(DATA_3(x1[17], x2[17], x3[17]))) →* java.lang.Object(ARRAY(DATA_3(x0[30], x1[30], x2[30]))))∧(x4[17] →* x3[30])∧(x6[17] + 1 →* x4[30])∧(x5[17] →* x5[30]))
(17) -> (32), if ((java.lang.Object(ARRAY(DATA_3(x1[17], x2[17], x3[17]))) →* java.lang.Object(ARRAY(DATA_3(x0[32], x1[32], x2[32]))))∧(x4[17] →* x3[32])∧(x6[17] + 1 →* x4[32])∧(x5[17] →* x5[32]))
(18) -> (19), if ((x6[18] >= 0 →* TRUE)∧(java.lang.Object(ARRAY(DATA_3(x1[18], x2[18], x3[18]))) →* java.lang.Object(ARRAY(DATA_3(x1[19], x2[19], x3[19]))))∧(x4[18] →* x4[19])∧(x5[18] →* x5[19])∧(x6[18] →* x6[19])∧(x7[18] →* x7[19]))
(19) -> (0), if ((java.lang.Object(ARRAY(DATA_3(x1[19], x2[19], x3[19]))) →* java.lang.Object(ARRAY(DATA_3(x1[0], x2[0], x3[0]))))∧(x4[19] →* x4[0])∧(x6[19] + 1 →* x6[0])∧(x5[19] →* x5[0]))
(19) -> (28), if ((java.lang.Object(ARRAY(DATA_3(x1[19], x2[19], x3[19]))) →* java.lang.Object(ARRAY(DATA_3(x0[28], x1[28], x2[28]))))∧(x4[19] →* x3[28])∧(x6[19] + 1 →* x4[28])∧(x5[19] →* x5[28]))
(19) -> (30), if ((java.lang.Object(ARRAY(DATA_3(x1[19], x2[19], x3[19]))) →* java.lang.Object(ARRAY(DATA_3(x0[30], x1[30], x2[30]))))∧(x4[19] →* x3[30])∧(x6[19] + 1 →* x4[30])∧(x5[19] →* x5[30]))
(19) -> (32), if ((java.lang.Object(ARRAY(DATA_3(x1[19], x2[19], x3[19]))) →* java.lang.Object(ARRAY(DATA_3(x0[32], x1[32], x2[32]))))∧(x4[19] →* x3[32])∧(x6[19] + 1 →* x4[32])∧(x5[19] →* x5[32]))
(20) -> (21), if ((x6[20] >= 0 →* TRUE)∧(java.lang.Object(ARRAY(DATA_3(x1[20], x2[20], x3[20]))) →* java.lang.Object(ARRAY(DATA_3(x1[21], x2[21], x3[21]))))∧(x4[20] →* x4[21])∧(x5[20] →* x5[21])∧(x6[20] →* x6[21])∧(x7[20] →* x7[21]))
(21) -> (0), if ((java.lang.Object(ARRAY(DATA_3(x1[21], x2[21], x3[21]))) →* java.lang.Object(ARRAY(DATA_3(x1[0], x2[0], x3[0]))))∧(x4[21] →* x4[0])∧(x6[21] + 1 →* x6[0])∧(x5[21] →* x5[0]))
(21) -> (28), if ((java.lang.Object(ARRAY(DATA_3(x1[21], x2[21], x3[21]))) →* java.lang.Object(ARRAY(DATA_3(x0[28], x1[28], x2[28]))))∧(x4[21] →* x3[28])∧(x6[21] + 1 →* x4[28])∧(x5[21] →* x5[28]))
(21) -> (30), if ((java.lang.Object(ARRAY(DATA_3(x1[21], x2[21], x3[21]))) →* java.lang.Object(ARRAY(DATA_3(x0[30], x1[30], x2[30]))))∧(x4[21] →* x3[30])∧(x6[21] + 1 →* x4[30])∧(x5[21] →* x5[30]))
(21) -> (32), if ((java.lang.Object(ARRAY(DATA_3(x1[21], x2[21], x3[21]))) →* java.lang.Object(ARRAY(DATA_3(x0[32], x1[32], x2[32]))))∧(x4[21] →* x3[32])∧(x6[21] + 1 →* x4[32])∧(x5[21] →* x5[32]))
(22) -> (23), if ((x6[22] >= 0 →* TRUE)∧(java.lang.Object(ARRAY(DATA_3(x1[22], x2[22], x3[22]))) →* java.lang.Object(ARRAY(DATA_3(x1[23], x2[23], x3[23]))))∧(x4[22] →* x4[23])∧(x5[22] →* x5[23])∧(x6[22] →* x6[23])∧(x7[22] →* x7[23]))
(23) -> (0), if ((java.lang.Object(ARRAY(DATA_3(x1[23], x2[23], x3[23]))) →* java.lang.Object(ARRAY(DATA_3(x1[0], x2[0], x3[0]))))∧(x4[23] →* x4[0])∧(x6[23] + 1 →* x6[0])∧(x5[23] →* x5[0]))
(23) -> (28), if ((java.lang.Object(ARRAY(DATA_3(x1[23], x2[23], x3[23]))) →* java.lang.Object(ARRAY(DATA_3(x0[28], x1[28], x2[28]))))∧(x4[23] →* x3[28])∧(x6[23] + 1 →* x4[28])∧(x5[23] →* x5[28]))
(23) -> (30), if ((java.lang.Object(ARRAY(DATA_3(x1[23], x2[23], x3[23]))) →* java.lang.Object(ARRAY(DATA_3(x0[30], x1[30], x2[30]))))∧(x4[23] →* x3[30])∧(x6[23] + 1 →* x4[30])∧(x5[23] →* x5[30]))
(23) -> (32), if ((java.lang.Object(ARRAY(DATA_3(x1[23], x2[23], x3[23]))) →* java.lang.Object(ARRAY(DATA_3(x0[32], x1[32], x2[32]))))∧(x4[23] →* x3[32])∧(x6[23] + 1 →* x4[32])∧(x5[23] →* x5[32]))
(24) -> (25), if ((x6[24] >= 0 →* TRUE)∧(java.lang.Object(ARRAY(DATA_3(x1[24], x2[24], x3[24]))) →* java.lang.Object(ARRAY(DATA_3(x1[25], x2[25], x3[25]))))∧(x4[24] →* x4[25])∧(x5[24] →* x5[25])∧(x6[24] →* x6[25])∧(x7[24] →* x7[25]))
(25) -> (0), if ((java.lang.Object(ARRAY(DATA_3(x1[25], x2[25], x3[25]))) →* java.lang.Object(ARRAY(DATA_3(x1[0], x2[0], x3[0]))))∧(x4[25] →* x4[0])∧(x6[25] + 1 →* x6[0])∧(x5[25] →* x5[0]))
(25) -> (28), if ((java.lang.Object(ARRAY(DATA_3(x1[25], x2[25], x3[25]))) →* java.lang.Object(ARRAY(DATA_3(x0[28], x1[28], x2[28]))))∧(x4[25] →* x3[28])∧(x6[25] + 1 →* x4[28])∧(x5[25] →* x5[28]))
(25) -> (30), if ((java.lang.Object(ARRAY(DATA_3(x1[25], x2[25], x3[25]))) →* java.lang.Object(ARRAY(DATA_3(x0[30], x1[30], x2[30]))))∧(x4[25] →* x3[30])∧(x6[25] + 1 →* x4[30])∧(x5[25] →* x5[30]))
(25) -> (32), if ((java.lang.Object(ARRAY(DATA_3(x1[25], x2[25], x3[25]))) →* java.lang.Object(ARRAY(DATA_3(x0[32], x1[32], x2[32]))))∧(x4[25] →* x3[32])∧(x6[25] + 1 →* x4[32])∧(x5[25] →* x5[32]))
(26) -> (27), if ((x6[26] >= 0 →* TRUE)∧(java.lang.Object(ARRAY(DATA_3(x1[26], x2[26], x3[26]))) →* java.lang.Object(ARRAY(DATA_3(x1[27], x2[27], x3[27]))))∧(x4[26] →* x4[27])∧(x5[26] →* x5[27])∧(x6[26] →* x6[27])∧(x7[26] →* x7[27]))
(27) -> (0), if ((java.lang.Object(ARRAY(DATA_3(x1[27], x2[27], x3[27]))) →* java.lang.Object(ARRAY(DATA_3(x1[0], x2[0], x3[0]))))∧(x4[27] →* x4[0])∧(x6[27] + 1 →* x6[0])∧(x5[27] →* x5[0]))
(27) -> (28), if ((java.lang.Object(ARRAY(DATA_3(x1[27], x2[27], x3[27]))) →* java.lang.Object(ARRAY(DATA_3(x0[28], x1[28], x2[28]))))∧(x4[27] →* x3[28])∧(x6[27] + 1 →* x4[28])∧(x5[27] →* x5[28]))
(27) -> (30), if ((java.lang.Object(ARRAY(DATA_3(x1[27], x2[27], x3[27]))) →* java.lang.Object(ARRAY(DATA_3(x0[30], x1[30], x2[30]))))∧(x4[27] →* x3[30])∧(x6[27] + 1 →* x4[30])∧(x5[27] →* x5[30]))
(27) -> (32), if ((java.lang.Object(ARRAY(DATA_3(x1[27], x2[27], x3[27]))) →* java.lang.Object(ARRAY(DATA_3(x0[32], x1[32], x2[32]))))∧(x4[27] →* x3[32])∧(x6[27] + 1 →* x4[32])∧(x5[27] →* x5[32]))
(28) -> (29), if ((x5[28] <= x4[28] && x3[28] >= 0 && 2 >= x3[28] - 1 && 0 <= x3[28] - 1 →* TRUE)∧(java.lang.Object(ARRAY(DATA_3(x0[28], x1[28], x2[28]))) →* java.lang.Object(ARRAY(DATA_3(x0[29], x1[29], x2[29]))))∧(x3[28] →* x3[29])∧(x4[28] →* x4[29])∧(x5[28] →* x5[29]))
(29) -> (0), if ((java.lang.Object(ARRAY(DATA_3(x0[29], x1[29], x2[29]))) →* java.lang.Object(ARRAY(DATA_3(x1[0], x2[0], x3[0]))))∧(x3[29] - 1 →* x4[0])∧(0 →* x6[0])∧(0 →* x5[0]))
(29) -> (28), if ((java.lang.Object(ARRAY(DATA_3(x0[29], x1[29], x2[29]))) →* java.lang.Object(ARRAY(DATA_3(x0[28], x1[28], x2[28]))))∧(x3[29] - 1 →* x3[28])∧(0 →* x4[28])∧(0 →* x5[28]))
(29) -> (30), if ((java.lang.Object(ARRAY(DATA_3(x0[29], x1[29], x2[29]))) →* java.lang.Object(ARRAY(DATA_3(x0[30], x1[30], x2[30]))))∧(x3[29] - 1 →* x3[30])∧(0 →* x4[30])∧(0 →* x5[30]))
(29) -> (32), if ((java.lang.Object(ARRAY(DATA_3(x0[29], x1[29], x2[29]))) →* java.lang.Object(ARRAY(DATA_3(x0[32], x1[32], x2[32]))))∧(x3[29] - 1 →* x3[32])∧(0 →* x4[32])∧(0 →* x5[32]))
(30) -> (31), if ((x5[30] <= x4[30] && x3[30] >= 0 && 2 >= x3[30] - 1 && 0 <= x3[30] - 1 →* TRUE)∧(java.lang.Object(ARRAY(DATA_3(x0[30], x1[30], x2[30]))) →* java.lang.Object(ARRAY(DATA_3(x0[31], x1[31], x2[31]))))∧(x3[30] →* x3[31])∧(x4[30] →* x4[31])∧(x5[30] →* x5[31]))
(31) -> (0), if ((java.lang.Object(ARRAY(DATA_3(x0[31], x1[31], x2[31]))) →* java.lang.Object(ARRAY(DATA_3(x1[0], x2[0], x3[0]))))∧(x3[31] - 1 →* x4[0])∧(0 →* x6[0])∧(1 →* x5[0]))
(31) -> (28), if ((java.lang.Object(ARRAY(DATA_3(x0[31], x1[31], x2[31]))) →* java.lang.Object(ARRAY(DATA_3(x0[28], x1[28], x2[28]))))∧(x3[31] - 1 →* x3[28])∧(0 →* x4[28])∧(1 →* x5[28]))
(31) -> (30), if ((java.lang.Object(ARRAY(DATA_3(x0[31], x1[31], x2[31]))) →* java.lang.Object(ARRAY(DATA_3(x0[30], x1[30], x2[30]))))∧(x3[31] - 1 →* x3[30])∧(0 →* x4[30])∧(1 →* x5[30]))
(31) -> (32), if ((java.lang.Object(ARRAY(DATA_3(x0[31], x1[31], x2[31]))) →* java.lang.Object(ARRAY(DATA_3(x0[32], x1[32], x2[32]))))∧(x3[31] - 1 →* x3[32])∧(0 →* x4[32])∧(1 →* x5[32]))
(32) -> (33), if ((x5[32] <= x4[32] && x3[32] >= 0 && 2 >= x3[32] - 1 && 0 <= x3[32] - 1 →* TRUE)∧(java.lang.Object(ARRAY(DATA_3(x0[32], x1[32], x2[32]))) →* java.lang.Object(ARRAY(DATA_3(x0[33], x1[33], x2[33]))))∧(x3[32] →* x3[33])∧(x4[32] →* x4[33])∧(x5[32] →* x5[33]))
(33) -> (0), if ((java.lang.Object(ARRAY(DATA_3(x0[33], x1[33], x2[33]))) →* java.lang.Object(ARRAY(DATA_3(x1[0], x2[0], x3[0]))))∧(x3[33] - 1 →* x4[0])∧(0 →* x6[0])∧(x6[33] →* x5[0]))
(33) -> (28), if ((java.lang.Object(ARRAY(DATA_3(x0[33], x1[33], x2[33]))) →* java.lang.Object(ARRAY(DATA_3(x0[28], x1[28], x2[28]))))∧(x3[33] - 1 →* x3[28])∧(0 →* x4[28])∧(x6[33] →* x5[28]))
(33) -> (30), if ((java.lang.Object(ARRAY(DATA_3(x0[33], x1[33], x2[33]))) →* java.lang.Object(ARRAY(DATA_3(x0[30], x1[30], x2[30]))))∧(x3[33] - 1 →* x3[30])∧(0 →* x4[30])∧(x6[33] →* x5[30]))
(33) -> (32), if ((java.lang.Object(ARRAY(DATA_3(x0[33], x1[33], x2[33]))) →* java.lang.Object(ARRAY(DATA_3(x0[32], x1[32], x2[32]))))∧(x3[33] - 1 →* x3[32])∧(0 →* x4[32])∧(x6[33] →* x5[32]))
(1) (&&(&&(<(x6[0], x5[0]), >=(x4[0], 0)), <=(x4[0], 2))=TRUE∧java.lang.Object(ARRAY(DATA_3(x1[0], x2[0], x3[0])))=java.lang.Object(ARRAY(DATA_3(x1[1], x2[1], x3[1])))∧x4[0]=x4[1]∧x6[0]=x6[1]∧x5[0]=x5[1] ⇒ 6147_0_TEST_GE(java.lang.Object(ARRAY(DATA_3(x1[0], x2[0], x3[0]))), x4[0], x6[0], x5[0])≥NonInfC∧6147_0_TEST_GE(java.lang.Object(ARRAY(DATA_3(x1[0], x2[0], x3[0]))), x4[0], x6[0], x5[0])≥COND_6147_0_TEST_GE(&&(&&(<(x6[0], x5[0]), >=(x4[0], 0)), <=(x4[0], 2)), java.lang.Object(ARRAY(DATA_3(x1[0], x2[0], x3[0]))), x4[0], x6[0], x5[0])∧(UIncreasing(COND_6147_0_TEST_GE(&&(&&(<(x6[0], x5[0]), >=(x4[0], 0)), <=(x4[0], 2)), java.lang.Object(ARRAY(DATA_3(x1[0], x2[0], x3[0]))), x4[0], x6[0], x5[0])), ≥))
(2) (<=(x4[0], 2)=TRUE∧<(x6[0], x5[0])=TRUE∧>=(x4[0], 0)=TRUE ⇒ 6147_0_TEST_GE(java.lang.Object(ARRAY(DATA_3(x1[0], x2[0], x3[0]))), x4[0], x6[0], x5[0])≥NonInfC∧6147_0_TEST_GE(java.lang.Object(ARRAY(DATA_3(x1[0], x2[0], x3[0]))), x4[0], x6[0], x5[0])≥COND_6147_0_TEST_GE(&&(&&(<(x6[0], x5[0]), >=(x4[0], 0)), <=(x4[0], 2)), java.lang.Object(ARRAY(DATA_3(x1[0], x2[0], x3[0]))), x4[0], x6[0], x5[0])∧(UIncreasing(COND_6147_0_TEST_GE(&&(&&(<(x6[0], x5[0]), >=(x4[0], 0)), <=(x4[0], 2)), java.lang.Object(ARRAY(DATA_3(x1[0], x2[0], x3[0]))), x4[0], x6[0], x5[0])), ≥))
(3) ([2] + [-1]x4[0] ≥ 0∧x5[0] + [-1] + [-1]x6[0] ≥ 0∧x4[0] ≥ 0 ⇒ (UIncreasing(COND_6147_0_TEST_GE(&&(&&(<(x6[0], x5[0]), >=(x4[0], 0)), <=(x4[0], 2)), java.lang.Object(ARRAY(DATA_3(x1[0], x2[0], x3[0]))), x4[0], x6[0], x5[0])), ≥)∧[(-1)bni_123 + (-1)Bound*bni_123] + [bni_123]x4[0] ≥ 0∧[(-1)bso_124] ≥ 0)
(4) ([2] + [-1]x4[0] ≥ 0∧x5[0] + [-1] + [-1]x6[0] ≥ 0∧x4[0] ≥ 0 ⇒ (UIncreasing(COND_6147_0_TEST_GE(&&(&&(<(x6[0], x5[0]), >=(x4[0], 0)), <=(x4[0], 2)), java.lang.Object(ARRAY(DATA_3(x1[0], x2[0], x3[0]))), x4[0], x6[0], x5[0])), ≥)∧[(-1)bni_123 + (-1)Bound*bni_123] + [bni_123]x4[0] ≥ 0∧[(-1)bso_124] ≥ 0)
(5) ([2] + [-1]x4[0] ≥ 0∧x5[0] + [-1] + [-1]x6[0] ≥ 0∧x4[0] ≥ 0 ⇒ (UIncreasing(COND_6147_0_TEST_GE(&&(&&(<(x6[0], x5[0]), >=(x4[0], 0)), <=(x4[0], 2)), java.lang.Object(ARRAY(DATA_3(x1[0], x2[0], x3[0]))), x4[0], x6[0], x5[0])), ≥)∧[(-1)bni_123 + (-1)Bound*bni_123] + [bni_123]x4[0] ≥ 0∧[(-1)bso_124] ≥ 0)
(6) ([2] + [-1]x4[0] ≥ 0∧x5[0] ≥ 0∧x4[0] ≥ 0 ⇒ (UIncreasing(COND_6147_0_TEST_GE(&&(&&(<(x6[0], x5[0]), >=(x4[0], 0)), <=(x4[0], 2)), java.lang.Object(ARRAY(DATA_3(x1[0], x2[0], x3[0]))), x4[0], x6[0], x5[0])), ≥)∧[(-1)bni_123 + (-1)Bound*bni_123] + [bni_123]x4[0] ≥ 0∧[(-1)bso_124] ≥ 0)
(7) ([2] + [-1]x4[0] ≥ 0∧x5[0] ≥ 0∧x4[0] ≥ 0∧x6[0] ≥ 0 ⇒ (UIncreasing(COND_6147_0_TEST_GE(&&(&&(<(x6[0], x5[0]), >=(x4[0], 0)), <=(x4[0], 2)), java.lang.Object(ARRAY(DATA_3(x1[0], x2[0], x3[0]))), x4[0], x6[0], x5[0])), ≥)∧[(-1)bni_123 + (-1)Bound*bni_123] + [bni_123]x4[0] ≥ 0∧[(-1)bso_124] ≥ 0)
(8) ([2] + [-1]x4[0] ≥ 0∧x5[0] ≥ 0∧x4[0] ≥ 0∧x6[0] ≥ 0 ⇒ (UIncreasing(COND_6147_0_TEST_GE(&&(&&(<(x6[0], x5[0]), >=(x4[0], 0)), <=(x4[0], 2)), java.lang.Object(ARRAY(DATA_3(x1[0], x2[0], x3[0]))), x4[0], x6[0], x5[0])), ≥)∧[(-1)bni_123 + (-1)Bound*bni_123] + [bni_123]x4[0] ≥ 0∧[(-1)bso_124] ≥ 0)
(9) (COND_6147_0_TEST_GE(TRUE, java.lang.Object(ARRAY(DATA_3(x1[1], x2[1], x3[1]))), x4[1], x6[1], x5[1])≥NonInfC∧COND_6147_0_TEST_GE(TRUE, java.lang.Object(ARRAY(DATA_3(x1[1], x2[1], x3[1]))), x4[1], x6[1], x5[1])≥7152_1_TEST_INVOKEMETHOD(7152_0_bubble_Load(x7[1]), java.lang.Object(ARRAY(DATA_3(x1[1], x2[1], x3[1]))), x4[1], x5[1], x6[1], x7[1])∧(UIncreasing(7152_1_TEST_INVOKEMETHOD(7152_0_bubble_Load(x7[1]), java.lang.Object(ARRAY(DATA_3(x1[1], x2[1], x3[1]))), x4[1], x5[1], x6[1], x7[1])), ≥))
(10) ((UIncreasing(7152_1_TEST_INVOKEMETHOD(7152_0_bubble_Load(x7[1]), java.lang.Object(ARRAY(DATA_3(x1[1], x2[1], x3[1]))), x4[1], x5[1], x6[1], x7[1])), ≥)∧[(-1)bso_126] ≥ 0)
(11) ((UIncreasing(7152_1_TEST_INVOKEMETHOD(7152_0_bubble_Load(x7[1]), java.lang.Object(ARRAY(DATA_3(x1[1], x2[1], x3[1]))), x4[1], x5[1], x6[1], x7[1])), ≥)∧[(-1)bso_126] ≥ 0)
(12) ((UIncreasing(7152_1_TEST_INVOKEMETHOD(7152_0_bubble_Load(x7[1]), java.lang.Object(ARRAY(DATA_3(x1[1], x2[1], x3[1]))), x4[1], x5[1], x6[1], x7[1])), ≥)∧[(-1)bso_126] ≥ 0)
(13) ((UIncreasing(7152_1_TEST_INVOKEMETHOD(7152_0_bubble_Load(x7[1]), java.lang.Object(ARRAY(DATA_3(x1[1], x2[1], x3[1]))), x4[1], x5[1], x6[1], x7[1])), ≥)∧0 = 0∧0 = 0∧0 = 0∧[(-1)bso_126] ≥ 0)
(14) (>=(x6[2], 0)=TRUE∧java.lang.Object(ARRAY(DATA_3(x1[2], x2[2], x3[2])))=java.lang.Object(ARRAY(DATA_3(x1[3], x2[3], x3[3])))∧x4[2]=x4[3]∧x5[2]=x5[3]∧x6[2]=x6[3] ⇒ 7152_1_TEST_INVOKEMETHOD(4383_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[2], x2[2], x3[2]))), x4[2], x5[2], x6[2], NULL)≥NonInfC∧7152_1_TEST_INVOKEMETHOD(4383_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[2], x2[2], x3[2]))), x4[2], x5[2], x6[2], NULL)≥COND_7152_1_TEST_INVOKEMETHOD(>=(x6[2], 0), 4383_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[2], x2[2], x3[2]))), x4[2], x5[2], x6[2], NULL)∧(UIncreasing(COND_7152_1_TEST_INVOKEMETHOD(>=(x6[2], 0), 4383_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[2], x2[2], x3[2]))), x4[2], x5[2], x6[2], NULL)), ≥))
(15) (>=(x6[2], 0)=TRUE ⇒ 7152_1_TEST_INVOKEMETHOD(4383_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[2], x2[2], x3[2]))), x4[2], x5[2], x6[2], NULL)≥NonInfC∧7152_1_TEST_INVOKEMETHOD(4383_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[2], x2[2], x3[2]))), x4[2], x5[2], x6[2], NULL)≥COND_7152_1_TEST_INVOKEMETHOD(>=(x6[2], 0), 4383_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[2], x2[2], x3[2]))), x4[2], x5[2], x6[2], NULL)∧(UIncreasing(COND_7152_1_TEST_INVOKEMETHOD(>=(x6[2], 0), 4383_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[2], x2[2], x3[2]))), x4[2], x5[2], x6[2], NULL)), ≥))
(16) (x6[2] ≥ 0 ⇒ (UIncreasing(COND_7152_1_TEST_INVOKEMETHOD(>=(x6[2], 0), 4383_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[2], x2[2], x3[2]))), x4[2], x5[2], x6[2], NULL)), ≥)∧[(-1)bni_127 + (-1)Bound*bni_127] + [bni_127]x4[2] ≥ 0∧[(-1)bso_128] ≥ 0)
(17) (x6[2] ≥ 0 ⇒ (UIncreasing(COND_7152_1_TEST_INVOKEMETHOD(>=(x6[2], 0), 4383_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[2], x2[2], x3[2]))), x4[2], x5[2], x6[2], NULL)), ≥)∧[(-1)bni_127 + (-1)Bound*bni_127] + [bni_127]x4[2] ≥ 0∧[(-1)bso_128] ≥ 0)
(18) (x6[2] ≥ 0 ⇒ (UIncreasing(COND_7152_1_TEST_INVOKEMETHOD(>=(x6[2], 0), 4383_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[2], x2[2], x3[2]))), x4[2], x5[2], x6[2], NULL)), ≥)∧[(-1)bni_127 + (-1)Bound*bni_127] + [bni_127]x4[2] ≥ 0∧[(-1)bso_128] ≥ 0)
(19) (x6[2] ≥ 0 ⇒ (UIncreasing(COND_7152_1_TEST_INVOKEMETHOD(>=(x6[2], 0), 4383_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[2], x2[2], x3[2]))), x4[2], x5[2], x6[2], NULL)), ≥)∧0 = 0∧[bni_127] = 0∧[(-1)bni_127 + (-1)Bound*bni_127] ≥ 0∧0 = 0∧0 = 0∧[(-1)bso_128] ≥ 0)
(20) (COND_7152_1_TEST_INVOKEMETHOD(TRUE, 4383_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[3], x2[3], x3[3]))), x4[3], x5[3], x6[3], NULL)≥NonInfC∧COND_7152_1_TEST_INVOKEMETHOD(TRUE, 4383_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[3], x2[3], x3[3]))), x4[3], x5[3], x6[3], NULL)≥6147_0_TEST_GE(java.lang.Object(ARRAY(DATA_3(x1[3], x2[3], x3[3]))), x4[3], +(x6[3], 1), x5[3])∧(UIncreasing(6147_0_TEST_GE(java.lang.Object(ARRAY(DATA_3(x1[3], x2[3], x3[3]))), x4[3], +(x6[3], 1), x5[3])), ≥))
(21) ((UIncreasing(6147_0_TEST_GE(java.lang.Object(ARRAY(DATA_3(x1[3], x2[3], x3[3]))), x4[3], +(x6[3], 1), x5[3])), ≥)∧[(-1)bso_130] ≥ 0)
(22) ((UIncreasing(6147_0_TEST_GE(java.lang.Object(ARRAY(DATA_3(x1[3], x2[3], x3[3]))), x4[3], +(x6[3], 1), x5[3])), ≥)∧[(-1)bso_130] ≥ 0)
(23) ((UIncreasing(6147_0_TEST_GE(java.lang.Object(ARRAY(DATA_3(x1[3], x2[3], x3[3]))), x4[3], +(x6[3], 1), x5[3])), ≥)∧[(-1)bso_130] ≥ 0)
(24) ((UIncreasing(6147_0_TEST_GE(java.lang.Object(ARRAY(DATA_3(x1[3], x2[3], x3[3]))), x4[3], +(x6[3], 1), x5[3])), ≥)∧0 = 0∧0 = 0∧0 = 0∧[(-1)bso_130] ≥ 0)
(25) (>=(x6[4], 0)=TRUE∧java.lang.Object(ARRAY(DATA_3(x1[4], x2[4], x3[4])))=java.lang.Object(ARRAY(DATA_3(x1[5], x2[5], x3[5])))∧x4[4]=x4[5]∧x5[4]=x5[5]∧x6[4]=x6[5] ⇒ 7152_1_TEST_INVOKEMETHOD(4580_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[4], x2[4], x3[4]))), x4[4], x5[4], x6[4], java.lang.Object(List(EOC)))≥NonInfC∧7152_1_TEST_INVOKEMETHOD(4580_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[4], x2[4], x3[4]))), x4[4], x5[4], x6[4], java.lang.Object(List(EOC)))≥COND_7152_1_TEST_INVOKEMETHOD1(>=(x6[4], 0), 4580_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[4], x2[4], x3[4]))), x4[4], x5[4], x6[4], java.lang.Object(List(EOC)))∧(UIncreasing(COND_7152_1_TEST_INVOKEMETHOD1(>=(x6[4], 0), 4580_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[4], x2[4], x3[4]))), x4[4], x5[4], x6[4], java.lang.Object(List(EOC)))), ≥))
(26) (>=(x6[4], 0)=TRUE ⇒ 7152_1_TEST_INVOKEMETHOD(4580_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[4], x2[4], x3[4]))), x4[4], x5[4], x6[4], java.lang.Object(List(EOC)))≥NonInfC∧7152_1_TEST_INVOKEMETHOD(4580_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[4], x2[4], x3[4]))), x4[4], x5[4], x6[4], java.lang.Object(List(EOC)))≥COND_7152_1_TEST_INVOKEMETHOD1(>=(x6[4], 0), 4580_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[4], x2[4], x3[4]))), x4[4], x5[4], x6[4], java.lang.Object(List(EOC)))∧(UIncreasing(COND_7152_1_TEST_INVOKEMETHOD1(>=(x6[4], 0), 4580_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[4], x2[4], x3[4]))), x4[4], x5[4], x6[4], java.lang.Object(List(EOC)))), ≥))
(27) (x6[4] ≥ 0 ⇒ (UIncreasing(COND_7152_1_TEST_INVOKEMETHOD1(>=(x6[4], 0), 4580_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[4], x2[4], x3[4]))), x4[4], x5[4], x6[4], java.lang.Object(List(EOC)))), ≥)∧[(-1)bni_131 + (-1)Bound*bni_131] + [bni_131]x4[4] ≥ 0∧[(-1)bso_132] ≥ 0)
(28) (x6[4] ≥ 0 ⇒ (UIncreasing(COND_7152_1_TEST_INVOKEMETHOD1(>=(x6[4], 0), 4580_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[4], x2[4], x3[4]))), x4[4], x5[4], x6[4], java.lang.Object(List(EOC)))), ≥)∧[(-1)bni_131 + (-1)Bound*bni_131] + [bni_131]x4[4] ≥ 0∧[(-1)bso_132] ≥ 0)
(29) (x6[4] ≥ 0 ⇒ (UIncreasing(COND_7152_1_TEST_INVOKEMETHOD1(>=(x6[4], 0), 4580_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[4], x2[4], x3[4]))), x4[4], x5[4], x6[4], java.lang.Object(List(EOC)))), ≥)∧[(-1)bni_131 + (-1)Bound*bni_131] + [bni_131]x4[4] ≥ 0∧[(-1)bso_132] ≥ 0)
(30) (x6[4] ≥ 0 ⇒ (UIncreasing(COND_7152_1_TEST_INVOKEMETHOD1(>=(x6[4], 0), 4580_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[4], x2[4], x3[4]))), x4[4], x5[4], x6[4], java.lang.Object(List(EOC)))), ≥)∧0 = 0∧[bni_131] = 0∧[(-1)bni_131 + (-1)Bound*bni_131] ≥ 0∧0 = 0∧0 = 0∧[(-1)bso_132] ≥ 0)
(31) (COND_7152_1_TEST_INVOKEMETHOD1(TRUE, 4580_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[5], x2[5], x3[5]))), x4[5], x5[5], x6[5], java.lang.Object(List(EOC)))≥NonInfC∧COND_7152_1_TEST_INVOKEMETHOD1(TRUE, 4580_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[5], x2[5], x3[5]))), x4[5], x5[5], x6[5], java.lang.Object(List(EOC)))≥6147_0_TEST_GE(java.lang.Object(ARRAY(DATA_3(x1[5], x2[5], x3[5]))), x4[5], +(x6[5], 1), x5[5])∧(UIncreasing(6147_0_TEST_GE(java.lang.Object(ARRAY(DATA_3(x1[5], x2[5], x3[5]))), x4[5], +(x6[5], 1), x5[5])), ≥))
(32) ((UIncreasing(6147_0_TEST_GE(java.lang.Object(ARRAY(DATA_3(x1[5], x2[5], x3[5]))), x4[5], +(x6[5], 1), x5[5])), ≥)∧[(-1)bso_134] ≥ 0)
(33) ((UIncreasing(6147_0_TEST_GE(java.lang.Object(ARRAY(DATA_3(x1[5], x2[5], x3[5]))), x4[5], +(x6[5], 1), x5[5])), ≥)∧[(-1)bso_134] ≥ 0)
(34) ((UIncreasing(6147_0_TEST_GE(java.lang.Object(ARRAY(DATA_3(x1[5], x2[5], x3[5]))), x4[5], +(x6[5], 1), x5[5])), ≥)∧[(-1)bso_134] ≥ 0)
(35) ((UIncreasing(6147_0_TEST_GE(java.lang.Object(ARRAY(DATA_3(x1[5], x2[5], x3[5]))), x4[5], +(x6[5], 1), x5[5])), ≥)∧0 = 0∧0 = 0∧0 = 0∧[(-1)bso_134] ≥ 0)
(36) (>=(x6[6], 0)=TRUE∧java.lang.Object(ARRAY(DATA_3(x1[6], x2[6], x3[6])))=java.lang.Object(ARRAY(DATA_3(x1[7], x2[7], x3[7])))∧x4[6]=x4[7]∧x5[6]=x5[7]∧x6[6]=x6[7] ⇒ 7152_1_TEST_INVOKEMETHOD(4619_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[6], x2[6], x3[6]))), x4[6], x5[6], x6[6], java.lang.Object(List(EOC)))≥NonInfC∧7152_1_TEST_INVOKEMETHOD(4619_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[6], x2[6], x3[6]))), x4[6], x5[6], x6[6], java.lang.Object(List(EOC)))≥COND_7152_1_TEST_INVOKEMETHOD2(>=(x6[6], 0), 4619_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[6], x2[6], x3[6]))), x4[6], x5[6], x6[6], java.lang.Object(List(EOC)))∧(UIncreasing(COND_7152_1_TEST_INVOKEMETHOD2(>=(x6[6], 0), 4619_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[6], x2[6], x3[6]))), x4[6], x5[6], x6[6], java.lang.Object(List(EOC)))), ≥))
(37) (>=(x6[6], 0)=TRUE ⇒ 7152_1_TEST_INVOKEMETHOD(4619_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[6], x2[6], x3[6]))), x4[6], x5[6], x6[6], java.lang.Object(List(EOC)))≥NonInfC∧7152_1_TEST_INVOKEMETHOD(4619_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[6], x2[6], x3[6]))), x4[6], x5[6], x6[6], java.lang.Object(List(EOC)))≥COND_7152_1_TEST_INVOKEMETHOD2(>=(x6[6], 0), 4619_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[6], x2[6], x3[6]))), x4[6], x5[6], x6[6], java.lang.Object(List(EOC)))∧(UIncreasing(COND_7152_1_TEST_INVOKEMETHOD2(>=(x6[6], 0), 4619_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[6], x2[6], x3[6]))), x4[6], x5[6], x6[6], java.lang.Object(List(EOC)))), ≥))
(38) (x6[6] ≥ 0 ⇒ (UIncreasing(COND_7152_1_TEST_INVOKEMETHOD2(>=(x6[6], 0), 4619_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[6], x2[6], x3[6]))), x4[6], x5[6], x6[6], java.lang.Object(List(EOC)))), ≥)∧[(-1)bni_135 + (-1)Bound*bni_135] + [bni_135]x4[6] ≥ 0∧[(-1)bso_136] ≥ 0)
(39) (x6[6] ≥ 0 ⇒ (UIncreasing(COND_7152_1_TEST_INVOKEMETHOD2(>=(x6[6], 0), 4619_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[6], x2[6], x3[6]))), x4[6], x5[6], x6[6], java.lang.Object(List(EOC)))), ≥)∧[(-1)bni_135 + (-1)Bound*bni_135] + [bni_135]x4[6] ≥ 0∧[(-1)bso_136] ≥ 0)
(40) (x6[6] ≥ 0 ⇒ (UIncreasing(COND_7152_1_TEST_INVOKEMETHOD2(>=(x6[6], 0), 4619_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[6], x2[6], x3[6]))), x4[6], x5[6], x6[6], java.lang.Object(List(EOC)))), ≥)∧[(-1)bni_135 + (-1)Bound*bni_135] + [bni_135]x4[6] ≥ 0∧[(-1)bso_136] ≥ 0)
(41) (x6[6] ≥ 0 ⇒ (UIncreasing(COND_7152_1_TEST_INVOKEMETHOD2(>=(x6[6], 0), 4619_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[6], x2[6], x3[6]))), x4[6], x5[6], x6[6], java.lang.Object(List(EOC)))), ≥)∧0 = 0∧[bni_135] = 0∧[(-1)bni_135 + (-1)Bound*bni_135] ≥ 0∧0 = 0∧0 = 0∧[(-1)bso_136] ≥ 0)
(42) (COND_7152_1_TEST_INVOKEMETHOD2(TRUE, 4619_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[7], x2[7], x3[7]))), x4[7], x5[7], x6[7], java.lang.Object(List(EOC)))≥NonInfC∧COND_7152_1_TEST_INVOKEMETHOD2(TRUE, 4619_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[7], x2[7], x3[7]))), x4[7], x5[7], x6[7], java.lang.Object(List(EOC)))≥6147_0_TEST_GE(java.lang.Object(ARRAY(DATA_3(x1[7], x2[7], x3[7]))), x4[7], +(x6[7], 1), x5[7])∧(UIncreasing(6147_0_TEST_GE(java.lang.Object(ARRAY(DATA_3(x1[7], x2[7], x3[7]))), x4[7], +(x6[7], 1), x5[7])), ≥))
(43) ((UIncreasing(6147_0_TEST_GE(java.lang.Object(ARRAY(DATA_3(x1[7], x2[7], x3[7]))), x4[7], +(x6[7], 1), x5[7])), ≥)∧[(-1)bso_138] ≥ 0)
(44) ((UIncreasing(6147_0_TEST_GE(java.lang.Object(ARRAY(DATA_3(x1[7], x2[7], x3[7]))), x4[7], +(x6[7], 1), x5[7])), ≥)∧[(-1)bso_138] ≥ 0)
(45) ((UIncreasing(6147_0_TEST_GE(java.lang.Object(ARRAY(DATA_3(x1[7], x2[7], x3[7]))), x4[7], +(x6[7], 1), x5[7])), ≥)∧[(-1)bso_138] ≥ 0)
(46) ((UIncreasing(6147_0_TEST_GE(java.lang.Object(ARRAY(DATA_3(x1[7], x2[7], x3[7]))), x4[7], +(x6[7], 1), x5[7])), ≥)∧0 = 0∧0 = 0∧0 = 0∧[(-1)bso_138] ≥ 0)
(47) (>=(x7[8], 0)=TRUE∧4650_0_bubble_Return(java.lang.Object(List(x0[8])))=4650_0_bubble_Return(java.lang.Object(List(x0[9])))∧java.lang.Object(ARRAY(DATA_3(x2[8], x3[8], x4[8])))=java.lang.Object(ARRAY(DATA_3(x2[9], x3[9], x4[9])))∧x5[8]=x5[9]∧x6[8]=x6[9]∧x7[8]=x7[9]∧java.lang.Object(List(x0[8]))=java.lang.Object(List(x0[9])) ⇒ 7152_1_TEST_INVOKEMETHOD(4650_0_bubble_Return(java.lang.Object(List(x0[8]))), java.lang.Object(ARRAY(DATA_3(x2[8], x3[8], x4[8]))), x5[8], x6[8], x7[8], java.lang.Object(List(x0[8])))≥NonInfC∧7152_1_TEST_INVOKEMETHOD(4650_0_bubble_Return(java.lang.Object(List(x0[8]))), java.lang.Object(ARRAY(DATA_3(x2[8], x3[8], x4[8]))), x5[8], x6[8], x7[8], java.lang.Object(List(x0[8])))≥COND_7152_1_TEST_INVOKEMETHOD3(>=(x7[8], 0), 4650_0_bubble_Return(java.lang.Object(List(x0[8]))), java.lang.Object(ARRAY(DATA_3(x2[8], x3[8], x4[8]))), x5[8], x6[8], x7[8], java.lang.Object(List(x0[8])))∧(UIncreasing(COND_7152_1_TEST_INVOKEMETHOD3(>=(x7[8], 0), 4650_0_bubble_Return(java.lang.Object(List(x0[8]))), java.lang.Object(ARRAY(DATA_3(x2[8], x3[8], x4[8]))), x5[8], x6[8], x7[8], java.lang.Object(List(x0[8])))), ≥))
(48) (>=(x7[8], 0)=TRUE ⇒ 7152_1_TEST_INVOKEMETHOD(4650_0_bubble_Return(java.lang.Object(List(x0[8]))), java.lang.Object(ARRAY(DATA_3(x2[8], x3[8], x4[8]))), x5[8], x6[8], x7[8], java.lang.Object(List(x0[8])))≥NonInfC∧7152_1_TEST_INVOKEMETHOD(4650_0_bubble_Return(java.lang.Object(List(x0[8]))), java.lang.Object(ARRAY(DATA_3(x2[8], x3[8], x4[8]))), x5[8], x6[8], x7[8], java.lang.Object(List(x0[8])))≥COND_7152_1_TEST_INVOKEMETHOD3(>=(x7[8], 0), 4650_0_bubble_Return(java.lang.Object(List(x0[8]))), java.lang.Object(ARRAY(DATA_3(x2[8], x3[8], x4[8]))), x5[8], x6[8], x7[8], java.lang.Object(List(x0[8])))∧(UIncreasing(COND_7152_1_TEST_INVOKEMETHOD3(>=(x7[8], 0), 4650_0_bubble_Return(java.lang.Object(List(x0[8]))), java.lang.Object(ARRAY(DATA_3(x2[8], x3[8], x4[8]))), x5[8], x6[8], x7[8], java.lang.Object(List(x0[8])))), ≥))
(49) (x7[8] ≥ 0 ⇒ (UIncreasing(COND_7152_1_TEST_INVOKEMETHOD3(>=(x7[8], 0), 4650_0_bubble_Return(java.lang.Object(List(x0[8]))), java.lang.Object(ARRAY(DATA_3(x2[8], x3[8], x4[8]))), x5[8], x6[8], x7[8], java.lang.Object(List(x0[8])))), ≥)∧[(-1)bni_139 + (-1)Bound*bni_139] + [bni_139]x5[8] ≥ 0∧[(-1)bso_140] ≥ 0)
(50) (x7[8] ≥ 0 ⇒ (UIncreasing(COND_7152_1_TEST_INVOKEMETHOD3(>=(x7[8], 0), 4650_0_bubble_Return(java.lang.Object(List(x0[8]))), java.lang.Object(ARRAY(DATA_3(x2[8], x3[8], x4[8]))), x5[8], x6[8], x7[8], java.lang.Object(List(x0[8])))), ≥)∧[(-1)bni_139 + (-1)Bound*bni_139] + [bni_139]x5[8] ≥ 0∧[(-1)bso_140] ≥ 0)
(51) (x7[8] ≥ 0 ⇒ (UIncreasing(COND_7152_1_TEST_INVOKEMETHOD3(>=(x7[8], 0), 4650_0_bubble_Return(java.lang.Object(List(x0[8]))), java.lang.Object(ARRAY(DATA_3(x2[8], x3[8], x4[8]))), x5[8], x6[8], x7[8], java.lang.Object(List(x0[8])))), ≥)∧[(-1)bni_139 + (-1)Bound*bni_139] + [bni_139]x5[8] ≥ 0∧[(-1)bso_140] ≥ 0)
(52) (x7[8] ≥ 0 ⇒ (UIncreasing(COND_7152_1_TEST_INVOKEMETHOD3(>=(x7[8], 0), 4650_0_bubble_Return(java.lang.Object(List(x0[8]))), java.lang.Object(ARRAY(DATA_3(x2[8], x3[8], x4[8]))), x5[8], x6[8], x7[8], java.lang.Object(List(x0[8])))), ≥)∧0 = 0∧[bni_139] = 0∧[(-1)bni_139 + (-1)Bound*bni_139] ≥ 0∧0 = 0∧0 = 0∧[(-1)bso_140] ≥ 0)
(53) (COND_7152_1_TEST_INVOKEMETHOD3(TRUE, 4650_0_bubble_Return(java.lang.Object(List(x0[9]))), java.lang.Object(ARRAY(DATA_3(x2[9], x3[9], x4[9]))), x5[9], x6[9], x7[9], java.lang.Object(List(x0[9])))≥NonInfC∧COND_7152_1_TEST_INVOKEMETHOD3(TRUE, 4650_0_bubble_Return(java.lang.Object(List(x0[9]))), java.lang.Object(ARRAY(DATA_3(x2[9], x3[9], x4[9]))), x5[9], x6[9], x7[9], java.lang.Object(List(x0[9])))≥6147_0_TEST_GE(java.lang.Object(ARRAY(DATA_3(x2[9], x3[9], x4[9]))), x5[9], +(x7[9], 1), x6[9])∧(UIncreasing(6147_0_TEST_GE(java.lang.Object(ARRAY(DATA_3(x2[9], x3[9], x4[9]))), x5[9], +(x7[9], 1), x6[9])), ≥))
(54) ((UIncreasing(6147_0_TEST_GE(java.lang.Object(ARRAY(DATA_3(x2[9], x3[9], x4[9]))), x5[9], +(x7[9], 1), x6[9])), ≥)∧[(-1)bso_142] ≥ 0)
(55) ((UIncreasing(6147_0_TEST_GE(java.lang.Object(ARRAY(DATA_3(x2[9], x3[9], x4[9]))), x5[9], +(x7[9], 1), x6[9])), ≥)∧[(-1)bso_142] ≥ 0)
(56) ((UIncreasing(6147_0_TEST_GE(java.lang.Object(ARRAY(DATA_3(x2[9], x3[9], x4[9]))), x5[9], +(x7[9], 1), x6[9])), ≥)∧[(-1)bso_142] ≥ 0)
(57) ((UIncreasing(6147_0_TEST_GE(java.lang.Object(ARRAY(DATA_3(x2[9], x3[9], x4[9]))), x5[9], +(x7[9], 1), x6[9])), ≥)∧0 = 0∧0 = 0∧0 = 0∧[(-1)bso_142] ≥ 0)
(58) (>=(x6[10], 0)=TRUE∧java.lang.Object(ARRAY(DATA_3(x1[10], x2[10], x3[10])))=java.lang.Object(ARRAY(DATA_3(x1[11], x2[11], x3[11])))∧x4[10]=x4[11]∧x5[10]=x5[11]∧x6[10]=x6[11] ⇒ 7152_1_TEST_INVOKEMETHOD(4673_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[10], x2[10], x3[10]))), x4[10], x5[10], x6[10], java.lang.Object(List(EOC)))≥NonInfC∧7152_1_TEST_INVOKEMETHOD(4673_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[10], x2[10], x3[10]))), x4[10], x5[10], x6[10], java.lang.Object(List(EOC)))≥COND_7152_1_TEST_INVOKEMETHOD4(>=(x6[10], 0), 4673_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[10], x2[10], x3[10]))), x4[10], x5[10], x6[10], java.lang.Object(List(EOC)))∧(UIncreasing(COND_7152_1_TEST_INVOKEMETHOD4(>=(x6[10], 0), 4673_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[10], x2[10], x3[10]))), x4[10], x5[10], x6[10], java.lang.Object(List(EOC)))), ≥))
(59) (>=(x6[10], 0)=TRUE ⇒ 7152_1_TEST_INVOKEMETHOD(4673_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[10], x2[10], x3[10]))), x4[10], x5[10], x6[10], java.lang.Object(List(EOC)))≥NonInfC∧7152_1_TEST_INVOKEMETHOD(4673_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[10], x2[10], x3[10]))), x4[10], x5[10], x6[10], java.lang.Object(List(EOC)))≥COND_7152_1_TEST_INVOKEMETHOD4(>=(x6[10], 0), 4673_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[10], x2[10], x3[10]))), x4[10], x5[10], x6[10], java.lang.Object(List(EOC)))∧(UIncreasing(COND_7152_1_TEST_INVOKEMETHOD4(>=(x6[10], 0), 4673_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[10], x2[10], x3[10]))), x4[10], x5[10], x6[10], java.lang.Object(List(EOC)))), ≥))
(60) (x6[10] ≥ 0 ⇒ (UIncreasing(COND_7152_1_TEST_INVOKEMETHOD4(>=(x6[10], 0), 4673_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[10], x2[10], x3[10]))), x4[10], x5[10], x6[10], java.lang.Object(List(EOC)))), ≥)∧[(-1)bni_143 + (-1)Bound*bni_143] + [bni_143]x4[10] ≥ 0∧[(-1)bso_144] ≥ 0)
(61) (x6[10] ≥ 0 ⇒ (UIncreasing(COND_7152_1_TEST_INVOKEMETHOD4(>=(x6[10], 0), 4673_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[10], x2[10], x3[10]))), x4[10], x5[10], x6[10], java.lang.Object(List(EOC)))), ≥)∧[(-1)bni_143 + (-1)Bound*bni_143] + [bni_143]x4[10] ≥ 0∧[(-1)bso_144] ≥ 0)
(62) (x6[10] ≥ 0 ⇒ (UIncreasing(COND_7152_1_TEST_INVOKEMETHOD4(>=(x6[10], 0), 4673_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[10], x2[10], x3[10]))), x4[10], x5[10], x6[10], java.lang.Object(List(EOC)))), ≥)∧[(-1)bni_143 + (-1)Bound*bni_143] + [bni_143]x4[10] ≥ 0∧[(-1)bso_144] ≥ 0)
(63) (x6[10] ≥ 0 ⇒ (UIncreasing(COND_7152_1_TEST_INVOKEMETHOD4(>=(x6[10], 0), 4673_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[10], x2[10], x3[10]))), x4[10], x5[10], x6[10], java.lang.Object(List(EOC)))), ≥)∧0 = 0∧[bni_143] = 0∧[(-1)bni_143 + (-1)Bound*bni_143] ≥ 0∧0 = 0∧0 = 0∧[(-1)bso_144] ≥ 0)
(64) (COND_7152_1_TEST_INVOKEMETHOD4(TRUE, 4673_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[11], x2[11], x3[11]))), x4[11], x5[11], x6[11], java.lang.Object(List(EOC)))≥NonInfC∧COND_7152_1_TEST_INVOKEMETHOD4(TRUE, 4673_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[11], x2[11], x3[11]))), x4[11], x5[11], x6[11], java.lang.Object(List(EOC)))≥6147_0_TEST_GE(java.lang.Object(ARRAY(DATA_3(x1[11], x2[11], x3[11]))), x4[11], +(x6[11], 1), x5[11])∧(UIncreasing(6147_0_TEST_GE(java.lang.Object(ARRAY(DATA_3(x1[11], x2[11], x3[11]))), x4[11], +(x6[11], 1), x5[11])), ≥))
(65) ((UIncreasing(6147_0_TEST_GE(java.lang.Object(ARRAY(DATA_3(x1[11], x2[11], x3[11]))), x4[11], +(x6[11], 1), x5[11])), ≥)∧[(-1)bso_146] ≥ 0)
(66) ((UIncreasing(6147_0_TEST_GE(java.lang.Object(ARRAY(DATA_3(x1[11], x2[11], x3[11]))), x4[11], +(x6[11], 1), x5[11])), ≥)∧[(-1)bso_146] ≥ 0)
(67) ((UIncreasing(6147_0_TEST_GE(java.lang.Object(ARRAY(DATA_3(x1[11], x2[11], x3[11]))), x4[11], +(x6[11], 1), x5[11])), ≥)∧[(-1)bso_146] ≥ 0)
(68) ((UIncreasing(6147_0_TEST_GE(java.lang.Object(ARRAY(DATA_3(x1[11], x2[11], x3[11]))), x4[11], +(x6[11], 1), x5[11])), ≥)∧0 = 0∧0 = 0∧0 = 0∧[(-1)bso_146] ≥ 0)
(69) (>=(x6[12], 0)=TRUE∧java.lang.Object(ARRAY(DATA_3(x1[12], x2[12], x3[12])))=java.lang.Object(ARRAY(DATA_3(x1[13], x2[13], x3[13])))∧x4[12]=x4[13]∧x5[12]=x5[13]∧x6[12]=x6[13]∧x7[12]=x7[13] ⇒ 7152_1_TEST_INVOKEMETHOD(8175_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[12], x2[12], x3[12]))), x4[12], x5[12], x6[12], x7[12])≥NonInfC∧7152_1_TEST_INVOKEMETHOD(8175_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[12], x2[12], x3[12]))), x4[12], x5[12], x6[12], x7[12])≥COND_7152_1_TEST_INVOKEMETHOD5(>=(x6[12], 0), 8175_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[12], x2[12], x3[12]))), x4[12], x5[12], x6[12], x7[12])∧(UIncreasing(COND_7152_1_TEST_INVOKEMETHOD5(>=(x6[12], 0), 8175_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[12], x2[12], x3[12]))), x4[12], x5[12], x6[12], x7[12])), ≥))
(70) (>=(x6[12], 0)=TRUE ⇒ 7152_1_TEST_INVOKEMETHOD(8175_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[12], x2[12], x3[12]))), x4[12], x5[12], x6[12], x7[12])≥NonInfC∧7152_1_TEST_INVOKEMETHOD(8175_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[12], x2[12], x3[12]))), x4[12], x5[12], x6[12], x7[12])≥COND_7152_1_TEST_INVOKEMETHOD5(>=(x6[12], 0), 8175_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[12], x2[12], x3[12]))), x4[12], x5[12], x6[12], x7[12])∧(UIncreasing(COND_7152_1_TEST_INVOKEMETHOD5(>=(x6[12], 0), 8175_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[12], x2[12], x3[12]))), x4[12], x5[12], x6[12], x7[12])), ≥))
(71) (x6[12] ≥ 0 ⇒ (UIncreasing(COND_7152_1_TEST_INVOKEMETHOD5(>=(x6[12], 0), 8175_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[12], x2[12], x3[12]))), x4[12], x5[12], x6[12], x7[12])), ≥)∧[(-1)bni_147 + (-1)Bound*bni_147] + [bni_147]x4[12] ≥ 0∧[(-1)bso_148] ≥ 0)
(72) (x6[12] ≥ 0 ⇒ (UIncreasing(COND_7152_1_TEST_INVOKEMETHOD5(>=(x6[12], 0), 8175_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[12], x2[12], x3[12]))), x4[12], x5[12], x6[12], x7[12])), ≥)∧[(-1)bni_147 + (-1)Bound*bni_147] + [bni_147]x4[12] ≥ 0∧[(-1)bso_148] ≥ 0)
(73) (x6[12] ≥ 0 ⇒ (UIncreasing(COND_7152_1_TEST_INVOKEMETHOD5(>=(x6[12], 0), 8175_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[12], x2[12], x3[12]))), x4[12], x5[12], x6[12], x7[12])), ≥)∧[(-1)bni_147 + (-1)Bound*bni_147] + [bni_147]x4[12] ≥ 0∧[(-1)bso_148] ≥ 0)
(74) (x6[12] ≥ 0 ⇒ (UIncreasing(COND_7152_1_TEST_INVOKEMETHOD5(>=(x6[12], 0), 8175_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[12], x2[12], x3[12]))), x4[12], x5[12], x6[12], x7[12])), ≥)∧0 = 0∧[bni_147] = 0∧[(-1)bni_147 + (-1)Bound*bni_147] ≥ 0∧0 = 0∧0 = 0∧[(-1)bso_148] ≥ 0)
(75) (COND_7152_1_TEST_INVOKEMETHOD5(TRUE, 8175_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[13], x2[13], x3[13]))), x4[13], x5[13], x6[13], x7[13])≥NonInfC∧COND_7152_1_TEST_INVOKEMETHOD5(TRUE, 8175_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[13], x2[13], x3[13]))), x4[13], x5[13], x6[13], x7[13])≥6147_0_TEST_GE(java.lang.Object(ARRAY(DATA_3(x1[13], x2[13], x3[13]))), x4[13], +(x6[13], 1), x5[13])∧(UIncreasing(6147_0_TEST_GE(java.lang.Object(ARRAY(DATA_3(x1[13], x2[13], x3[13]))), x4[13], +(x6[13], 1), x5[13])), ≥))
(76) ((UIncreasing(6147_0_TEST_GE(java.lang.Object(ARRAY(DATA_3(x1[13], x2[13], x3[13]))), x4[13], +(x6[13], 1), x5[13])), ≥)∧[(-1)bso_150] ≥ 0)
(77) ((UIncreasing(6147_0_TEST_GE(java.lang.Object(ARRAY(DATA_3(x1[13], x2[13], x3[13]))), x4[13], +(x6[13], 1), x5[13])), ≥)∧[(-1)bso_150] ≥ 0)
(78) ((UIncreasing(6147_0_TEST_GE(java.lang.Object(ARRAY(DATA_3(x1[13], x2[13], x3[13]))), x4[13], +(x6[13], 1), x5[13])), ≥)∧[(-1)bso_150] ≥ 0)
(79) ((UIncreasing(6147_0_TEST_GE(java.lang.Object(ARRAY(DATA_3(x1[13], x2[13], x3[13]))), x4[13], +(x6[13], 1), x5[13])), ≥)∧0 = 0∧0 = 0∧0 = 0∧[(-1)bso_150] ≥ 0)
(80) (>=(x6[14], 0)=TRUE∧java.lang.Object(ARRAY(DATA_3(x1[14], x2[14], x3[14])))=java.lang.Object(ARRAY(DATA_3(x1[15], x2[15], x3[15])))∧x4[14]=x4[15]∧x5[14]=x5[15]∧x6[14]=x6[15]∧x7[14]=x7[15] ⇒ 7152_1_TEST_INVOKEMETHOD(8233_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[14], x2[14], x3[14]))), x4[14], x5[14], x6[14], x7[14])≥NonInfC∧7152_1_TEST_INVOKEMETHOD(8233_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[14], x2[14], x3[14]))), x4[14], x5[14], x6[14], x7[14])≥COND_7152_1_TEST_INVOKEMETHOD6(>=(x6[14], 0), 8233_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[14], x2[14], x3[14]))), x4[14], x5[14], x6[14], x7[14])∧(UIncreasing(COND_7152_1_TEST_INVOKEMETHOD6(>=(x6[14], 0), 8233_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[14], x2[14], x3[14]))), x4[14], x5[14], x6[14], x7[14])), ≥))
(81) (>=(x6[14], 0)=TRUE ⇒ 7152_1_TEST_INVOKEMETHOD(8233_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[14], x2[14], x3[14]))), x4[14], x5[14], x6[14], x7[14])≥NonInfC∧7152_1_TEST_INVOKEMETHOD(8233_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[14], x2[14], x3[14]))), x4[14], x5[14], x6[14], x7[14])≥COND_7152_1_TEST_INVOKEMETHOD6(>=(x6[14], 0), 8233_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[14], x2[14], x3[14]))), x4[14], x5[14], x6[14], x7[14])∧(UIncreasing(COND_7152_1_TEST_INVOKEMETHOD6(>=(x6[14], 0), 8233_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[14], x2[14], x3[14]))), x4[14], x5[14], x6[14], x7[14])), ≥))
(82) (x6[14] ≥ 0 ⇒ (UIncreasing(COND_7152_1_TEST_INVOKEMETHOD6(>=(x6[14], 0), 8233_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[14], x2[14], x3[14]))), x4[14], x5[14], x6[14], x7[14])), ≥)∧[(-1)bni_151 + (-1)Bound*bni_151] + [bni_151]x4[14] ≥ 0∧[(-1)bso_152] ≥ 0)
(83) (x6[14] ≥ 0 ⇒ (UIncreasing(COND_7152_1_TEST_INVOKEMETHOD6(>=(x6[14], 0), 8233_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[14], x2[14], x3[14]))), x4[14], x5[14], x6[14], x7[14])), ≥)∧[(-1)bni_151 + (-1)Bound*bni_151] + [bni_151]x4[14] ≥ 0∧[(-1)bso_152] ≥ 0)
(84) (x6[14] ≥ 0 ⇒ (UIncreasing(COND_7152_1_TEST_INVOKEMETHOD6(>=(x6[14], 0), 8233_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[14], x2[14], x3[14]))), x4[14], x5[14], x6[14], x7[14])), ≥)∧[(-1)bni_151 + (-1)Bound*bni_151] + [bni_151]x4[14] ≥ 0∧[(-1)bso_152] ≥ 0)
(85) (x6[14] ≥ 0 ⇒ (UIncreasing(COND_7152_1_TEST_INVOKEMETHOD6(>=(x6[14], 0), 8233_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[14], x2[14], x3[14]))), x4[14], x5[14], x6[14], x7[14])), ≥)∧0 = 0∧[bni_151] = 0∧[(-1)bni_151 + (-1)Bound*bni_151] ≥ 0∧0 = 0∧0 = 0∧[(-1)bso_152] ≥ 0)
(86) (COND_7152_1_TEST_INVOKEMETHOD6(TRUE, 8233_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[15], x2[15], x3[15]))), x4[15], x5[15], x6[15], x7[15])≥NonInfC∧COND_7152_1_TEST_INVOKEMETHOD6(TRUE, 8233_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[15], x2[15], x3[15]))), x4[15], x5[15], x6[15], x7[15])≥6147_0_TEST_GE(java.lang.Object(ARRAY(DATA_3(x1[15], x2[15], x3[15]))), x4[15], +(x6[15], 1), x5[15])∧(UIncreasing(6147_0_TEST_GE(java.lang.Object(ARRAY(DATA_3(x1[15], x2[15], x3[15]))), x4[15], +(x6[15], 1), x5[15])), ≥))
(87) ((UIncreasing(6147_0_TEST_GE(java.lang.Object(ARRAY(DATA_3(x1[15], x2[15], x3[15]))), x4[15], +(x6[15], 1), x5[15])), ≥)∧[(-1)bso_154] ≥ 0)
(88) ((UIncreasing(6147_0_TEST_GE(java.lang.Object(ARRAY(DATA_3(x1[15], x2[15], x3[15]))), x4[15], +(x6[15], 1), x5[15])), ≥)∧[(-1)bso_154] ≥ 0)
(89) ((UIncreasing(6147_0_TEST_GE(java.lang.Object(ARRAY(DATA_3(x1[15], x2[15], x3[15]))), x4[15], +(x6[15], 1), x5[15])), ≥)∧[(-1)bso_154] ≥ 0)
(90) ((UIncreasing(6147_0_TEST_GE(java.lang.Object(ARRAY(DATA_3(x1[15], x2[15], x3[15]))), x4[15], +(x6[15], 1), x5[15])), ≥)∧0 = 0∧0 = 0∧0 = 0∧[(-1)bso_154] ≥ 0)
(91) (>=(x6[16], 0)=TRUE∧java.lang.Object(ARRAY(DATA_3(x1[16], x2[16], x3[16])))=java.lang.Object(ARRAY(DATA_3(x1[17], x2[17], x3[17])))∧x4[16]=x4[17]∧x5[16]=x5[17]∧x6[16]=x6[17]∧x7[16]=x7[17] ⇒ 7152_1_TEST_INVOKEMETHOD(8255_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[16], x2[16], x3[16]))), x4[16], x5[16], x6[16], x7[16])≥NonInfC∧7152_1_TEST_INVOKEMETHOD(8255_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[16], x2[16], x3[16]))), x4[16], x5[16], x6[16], x7[16])≥COND_7152_1_TEST_INVOKEMETHOD7(>=(x6[16], 0), 8255_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[16], x2[16], x3[16]))), x4[16], x5[16], x6[16], x7[16])∧(UIncreasing(COND_7152_1_TEST_INVOKEMETHOD7(>=(x6[16], 0), 8255_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[16], x2[16], x3[16]))), x4[16], x5[16], x6[16], x7[16])), ≥))
(92) (>=(x6[16], 0)=TRUE ⇒ 7152_1_TEST_INVOKEMETHOD(8255_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[16], x2[16], x3[16]))), x4[16], x5[16], x6[16], x7[16])≥NonInfC∧7152_1_TEST_INVOKEMETHOD(8255_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[16], x2[16], x3[16]))), x4[16], x5[16], x6[16], x7[16])≥COND_7152_1_TEST_INVOKEMETHOD7(>=(x6[16], 0), 8255_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[16], x2[16], x3[16]))), x4[16], x5[16], x6[16], x7[16])∧(UIncreasing(COND_7152_1_TEST_INVOKEMETHOD7(>=(x6[16], 0), 8255_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[16], x2[16], x3[16]))), x4[16], x5[16], x6[16], x7[16])), ≥))
(93) (x6[16] ≥ 0 ⇒ (UIncreasing(COND_7152_1_TEST_INVOKEMETHOD7(>=(x6[16], 0), 8255_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[16], x2[16], x3[16]))), x4[16], x5[16], x6[16], x7[16])), ≥)∧[(-1)bni_155 + (-1)Bound*bni_155] + [bni_155]x4[16] ≥ 0∧[(-1)bso_156] ≥ 0)
(94) (x6[16] ≥ 0 ⇒ (UIncreasing(COND_7152_1_TEST_INVOKEMETHOD7(>=(x6[16], 0), 8255_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[16], x2[16], x3[16]))), x4[16], x5[16], x6[16], x7[16])), ≥)∧[(-1)bni_155 + (-1)Bound*bni_155] + [bni_155]x4[16] ≥ 0∧[(-1)bso_156] ≥ 0)
(95) (x6[16] ≥ 0 ⇒ (UIncreasing(COND_7152_1_TEST_INVOKEMETHOD7(>=(x6[16], 0), 8255_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[16], x2[16], x3[16]))), x4[16], x5[16], x6[16], x7[16])), ≥)∧[(-1)bni_155 + (-1)Bound*bni_155] + [bni_155]x4[16] ≥ 0∧[(-1)bso_156] ≥ 0)
(96) (x6[16] ≥ 0 ⇒ (UIncreasing(COND_7152_1_TEST_INVOKEMETHOD7(>=(x6[16], 0), 8255_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[16], x2[16], x3[16]))), x4[16], x5[16], x6[16], x7[16])), ≥)∧0 = 0∧[bni_155] = 0∧[(-1)bni_155 + (-1)Bound*bni_155] ≥ 0∧0 = 0∧0 = 0∧[(-1)bso_156] ≥ 0)
(97) (COND_7152_1_TEST_INVOKEMETHOD7(TRUE, 8255_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[17], x2[17], x3[17]))), x4[17], x5[17], x6[17], x7[17])≥NonInfC∧COND_7152_1_TEST_INVOKEMETHOD7(TRUE, 8255_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[17], x2[17], x3[17]))), x4[17], x5[17], x6[17], x7[17])≥6147_0_TEST_GE(java.lang.Object(ARRAY(DATA_3(x1[17], x2[17], x3[17]))), x4[17], +(x6[17], 1), x5[17])∧(UIncreasing(6147_0_TEST_GE(java.lang.Object(ARRAY(DATA_3(x1[17], x2[17], x3[17]))), x4[17], +(x6[17], 1), x5[17])), ≥))
(98) ((UIncreasing(6147_0_TEST_GE(java.lang.Object(ARRAY(DATA_3(x1[17], x2[17], x3[17]))), x4[17], +(x6[17], 1), x5[17])), ≥)∧[(-1)bso_158] ≥ 0)
(99) ((UIncreasing(6147_0_TEST_GE(java.lang.Object(ARRAY(DATA_3(x1[17], x2[17], x3[17]))), x4[17], +(x6[17], 1), x5[17])), ≥)∧[(-1)bso_158] ≥ 0)
(100) ((UIncreasing(6147_0_TEST_GE(java.lang.Object(ARRAY(DATA_3(x1[17], x2[17], x3[17]))), x4[17], +(x6[17], 1), x5[17])), ≥)∧[(-1)bso_158] ≥ 0)
(101) ((UIncreasing(6147_0_TEST_GE(java.lang.Object(ARRAY(DATA_3(x1[17], x2[17], x3[17]))), x4[17], +(x6[17], 1), x5[17])), ≥)∧0 = 0∧0 = 0∧0 = 0∧[(-1)bso_158] ≥ 0)
(102) (>=(x6[18], 0)=TRUE∧java.lang.Object(ARRAY(DATA_3(x1[18], x2[18], x3[18])))=java.lang.Object(ARRAY(DATA_3(x1[19], x2[19], x3[19])))∧x4[18]=x4[19]∧x5[18]=x5[19]∧x6[18]=x6[19]∧x7[18]=x7[19] ⇒ 7152_1_TEST_INVOKEMETHOD(8259_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[18], x2[18], x3[18]))), x4[18], x5[18], x6[18], x7[18])≥NonInfC∧7152_1_TEST_INVOKEMETHOD(8259_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[18], x2[18], x3[18]))), x4[18], x5[18], x6[18], x7[18])≥COND_7152_1_TEST_INVOKEMETHOD8(>=(x6[18], 0), 8259_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[18], x2[18], x3[18]))), x4[18], x5[18], x6[18], x7[18])∧(UIncreasing(COND_7152_1_TEST_INVOKEMETHOD8(>=(x6[18], 0), 8259_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[18], x2[18], x3[18]))), x4[18], x5[18], x6[18], x7[18])), ≥))
(103) (>=(x6[18], 0)=TRUE ⇒ 7152_1_TEST_INVOKEMETHOD(8259_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[18], x2[18], x3[18]))), x4[18], x5[18], x6[18], x7[18])≥NonInfC∧7152_1_TEST_INVOKEMETHOD(8259_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[18], x2[18], x3[18]))), x4[18], x5[18], x6[18], x7[18])≥COND_7152_1_TEST_INVOKEMETHOD8(>=(x6[18], 0), 8259_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[18], x2[18], x3[18]))), x4[18], x5[18], x6[18], x7[18])∧(UIncreasing(COND_7152_1_TEST_INVOKEMETHOD8(>=(x6[18], 0), 8259_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[18], x2[18], x3[18]))), x4[18], x5[18], x6[18], x7[18])), ≥))
(104) (x6[18] ≥ 0 ⇒ (UIncreasing(COND_7152_1_TEST_INVOKEMETHOD8(>=(x6[18], 0), 8259_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[18], x2[18], x3[18]))), x4[18], x5[18], x6[18], x7[18])), ≥)∧[(-1)bni_159 + (-1)Bound*bni_159] + [bni_159]x4[18] ≥ 0∧[(-1)bso_160] ≥ 0)
(105) (x6[18] ≥ 0 ⇒ (UIncreasing(COND_7152_1_TEST_INVOKEMETHOD8(>=(x6[18], 0), 8259_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[18], x2[18], x3[18]))), x4[18], x5[18], x6[18], x7[18])), ≥)∧[(-1)bni_159 + (-1)Bound*bni_159] + [bni_159]x4[18] ≥ 0∧[(-1)bso_160] ≥ 0)
(106) (x6[18] ≥ 0 ⇒ (UIncreasing(COND_7152_1_TEST_INVOKEMETHOD8(>=(x6[18], 0), 8259_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[18], x2[18], x3[18]))), x4[18], x5[18], x6[18], x7[18])), ≥)∧[(-1)bni_159 + (-1)Bound*bni_159] + [bni_159]x4[18] ≥ 0∧[(-1)bso_160] ≥ 0)
(107) (x6[18] ≥ 0 ⇒ (UIncreasing(COND_7152_1_TEST_INVOKEMETHOD8(>=(x6[18], 0), 8259_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[18], x2[18], x3[18]))), x4[18], x5[18], x6[18], x7[18])), ≥)∧0 = 0∧[bni_159] = 0∧[(-1)bni_159 + (-1)Bound*bni_159] ≥ 0∧0 = 0∧0 = 0∧[(-1)bso_160] ≥ 0)
(108) (COND_7152_1_TEST_INVOKEMETHOD8(TRUE, 8259_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[19], x2[19], x3[19]))), x4[19], x5[19], x6[19], x7[19])≥NonInfC∧COND_7152_1_TEST_INVOKEMETHOD8(TRUE, 8259_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[19], x2[19], x3[19]))), x4[19], x5[19], x6[19], x7[19])≥6147_0_TEST_GE(java.lang.Object(ARRAY(DATA_3(x1[19], x2[19], x3[19]))), x4[19], +(x6[19], 1), x5[19])∧(UIncreasing(6147_0_TEST_GE(java.lang.Object(ARRAY(DATA_3(x1[19], x2[19], x3[19]))), x4[19], +(x6[19], 1), x5[19])), ≥))
(109) ((UIncreasing(6147_0_TEST_GE(java.lang.Object(ARRAY(DATA_3(x1[19], x2[19], x3[19]))), x4[19], +(x6[19], 1), x5[19])), ≥)∧[(-1)bso_162] ≥ 0)
(110) ((UIncreasing(6147_0_TEST_GE(java.lang.Object(ARRAY(DATA_3(x1[19], x2[19], x3[19]))), x4[19], +(x6[19], 1), x5[19])), ≥)∧[(-1)bso_162] ≥ 0)
(111) ((UIncreasing(6147_0_TEST_GE(java.lang.Object(ARRAY(DATA_3(x1[19], x2[19], x3[19]))), x4[19], +(x6[19], 1), x5[19])), ≥)∧[(-1)bso_162] ≥ 0)
(112) ((UIncreasing(6147_0_TEST_GE(java.lang.Object(ARRAY(DATA_3(x1[19], x2[19], x3[19]))), x4[19], +(x6[19], 1), x5[19])), ≥)∧0 = 0∧0 = 0∧0 = 0∧[(-1)bso_162] ≥ 0)
(113) (>=(x6[20], 0)=TRUE∧java.lang.Object(ARRAY(DATA_3(x1[20], x2[20], x3[20])))=java.lang.Object(ARRAY(DATA_3(x1[21], x2[21], x3[21])))∧x4[20]=x4[21]∧x5[20]=x5[21]∧x6[20]=x6[21]∧x7[20]=x7[21] ⇒ 7152_1_TEST_INVOKEMETHOD(8557_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[20], x2[20], x3[20]))), x4[20], x5[20], x6[20], x7[20])≥NonInfC∧7152_1_TEST_INVOKEMETHOD(8557_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[20], x2[20], x3[20]))), x4[20], x5[20], x6[20], x7[20])≥COND_7152_1_TEST_INVOKEMETHOD9(>=(x6[20], 0), 8557_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[20], x2[20], x3[20]))), x4[20], x5[20], x6[20], x7[20])∧(UIncreasing(COND_7152_1_TEST_INVOKEMETHOD9(>=(x6[20], 0), 8557_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[20], x2[20], x3[20]))), x4[20], x5[20], x6[20], x7[20])), ≥))
(114) (>=(x6[20], 0)=TRUE ⇒ 7152_1_TEST_INVOKEMETHOD(8557_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[20], x2[20], x3[20]))), x4[20], x5[20], x6[20], x7[20])≥NonInfC∧7152_1_TEST_INVOKEMETHOD(8557_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[20], x2[20], x3[20]))), x4[20], x5[20], x6[20], x7[20])≥COND_7152_1_TEST_INVOKEMETHOD9(>=(x6[20], 0), 8557_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[20], x2[20], x3[20]))), x4[20], x5[20], x6[20], x7[20])∧(UIncreasing(COND_7152_1_TEST_INVOKEMETHOD9(>=(x6[20], 0), 8557_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[20], x2[20], x3[20]))), x4[20], x5[20], x6[20], x7[20])), ≥))
(115) (x6[20] ≥ 0 ⇒ (UIncreasing(COND_7152_1_TEST_INVOKEMETHOD9(>=(x6[20], 0), 8557_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[20], x2[20], x3[20]))), x4[20], x5[20], x6[20], x7[20])), ≥)∧[(-1)bni_163 + (-1)Bound*bni_163] + [bni_163]x4[20] ≥ 0∧[(-1)bso_164] ≥ 0)
(116) (x6[20] ≥ 0 ⇒ (UIncreasing(COND_7152_1_TEST_INVOKEMETHOD9(>=(x6[20], 0), 8557_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[20], x2[20], x3[20]))), x4[20], x5[20], x6[20], x7[20])), ≥)∧[(-1)bni_163 + (-1)Bound*bni_163] + [bni_163]x4[20] ≥ 0∧[(-1)bso_164] ≥ 0)
(117) (x6[20] ≥ 0 ⇒ (UIncreasing(COND_7152_1_TEST_INVOKEMETHOD9(>=(x6[20], 0), 8557_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[20], x2[20], x3[20]))), x4[20], x5[20], x6[20], x7[20])), ≥)∧[(-1)bni_163 + (-1)Bound*bni_163] + [bni_163]x4[20] ≥ 0∧[(-1)bso_164] ≥ 0)
(118) (x6[20] ≥ 0 ⇒ (UIncreasing(COND_7152_1_TEST_INVOKEMETHOD9(>=(x6[20], 0), 8557_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[20], x2[20], x3[20]))), x4[20], x5[20], x6[20], x7[20])), ≥)∧0 = 0∧[bni_163] = 0∧[(-1)bni_163 + (-1)Bound*bni_163] ≥ 0∧0 = 0∧0 = 0∧[(-1)bso_164] ≥ 0)
(119) (COND_7152_1_TEST_INVOKEMETHOD9(TRUE, 8557_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[21], x2[21], x3[21]))), x4[21], x5[21], x6[21], x7[21])≥NonInfC∧COND_7152_1_TEST_INVOKEMETHOD9(TRUE, 8557_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[21], x2[21], x3[21]))), x4[21], x5[21], x6[21], x7[21])≥6147_0_TEST_GE(java.lang.Object(ARRAY(DATA_3(x1[21], x2[21], x3[21]))), x4[21], +(x6[21], 1), x5[21])∧(UIncreasing(6147_0_TEST_GE(java.lang.Object(ARRAY(DATA_3(x1[21], x2[21], x3[21]))), x4[21], +(x6[21], 1), x5[21])), ≥))
(120) ((UIncreasing(6147_0_TEST_GE(java.lang.Object(ARRAY(DATA_3(x1[21], x2[21], x3[21]))), x4[21], +(x6[21], 1), x5[21])), ≥)∧[(-1)bso_166] ≥ 0)
(121) ((UIncreasing(6147_0_TEST_GE(java.lang.Object(ARRAY(DATA_3(x1[21], x2[21], x3[21]))), x4[21], +(x6[21], 1), x5[21])), ≥)∧[(-1)bso_166] ≥ 0)
(122) ((UIncreasing(6147_0_TEST_GE(java.lang.Object(ARRAY(DATA_3(x1[21], x2[21], x3[21]))), x4[21], +(x6[21], 1), x5[21])), ≥)∧[(-1)bso_166] ≥ 0)
(123) ((UIncreasing(6147_0_TEST_GE(java.lang.Object(ARRAY(DATA_3(x1[21], x2[21], x3[21]))), x4[21], +(x6[21], 1), x5[21])), ≥)∧0 = 0∧0 = 0∧0 = 0∧[(-1)bso_166] ≥ 0)
(124) (>=(x6[22], 0)=TRUE∧java.lang.Object(ARRAY(DATA_3(x1[22], x2[22], x3[22])))=java.lang.Object(ARRAY(DATA_3(x1[23], x2[23], x3[23])))∧x4[22]=x4[23]∧x5[22]=x5[23]∧x6[22]=x6[23]∧x7[22]=x7[23] ⇒ 7152_1_TEST_INVOKEMETHOD(8577_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[22], x2[22], x3[22]))), x4[22], x5[22], x6[22], x7[22])≥NonInfC∧7152_1_TEST_INVOKEMETHOD(8577_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[22], x2[22], x3[22]))), x4[22], x5[22], x6[22], x7[22])≥COND_7152_1_TEST_INVOKEMETHOD10(>=(x6[22], 0), 8577_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[22], x2[22], x3[22]))), x4[22], x5[22], x6[22], x7[22])∧(UIncreasing(COND_7152_1_TEST_INVOKEMETHOD10(>=(x6[22], 0), 8577_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[22], x2[22], x3[22]))), x4[22], x5[22], x6[22], x7[22])), ≥))
(125) (>=(x6[22], 0)=TRUE ⇒ 7152_1_TEST_INVOKEMETHOD(8577_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[22], x2[22], x3[22]))), x4[22], x5[22], x6[22], x7[22])≥NonInfC∧7152_1_TEST_INVOKEMETHOD(8577_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[22], x2[22], x3[22]))), x4[22], x5[22], x6[22], x7[22])≥COND_7152_1_TEST_INVOKEMETHOD10(>=(x6[22], 0), 8577_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[22], x2[22], x3[22]))), x4[22], x5[22], x6[22], x7[22])∧(UIncreasing(COND_7152_1_TEST_INVOKEMETHOD10(>=(x6[22], 0), 8577_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[22], x2[22], x3[22]))), x4[22], x5[22], x6[22], x7[22])), ≥))
(126) (x6[22] ≥ 0 ⇒ (UIncreasing(COND_7152_1_TEST_INVOKEMETHOD10(>=(x6[22], 0), 8577_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[22], x2[22], x3[22]))), x4[22], x5[22], x6[22], x7[22])), ≥)∧[(-1)bni_167 + (-1)Bound*bni_167] + [bni_167]x4[22] ≥ 0∧[(-1)bso_168] ≥ 0)
(127) (x6[22] ≥ 0 ⇒ (UIncreasing(COND_7152_1_TEST_INVOKEMETHOD10(>=(x6[22], 0), 8577_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[22], x2[22], x3[22]))), x4[22], x5[22], x6[22], x7[22])), ≥)∧[(-1)bni_167 + (-1)Bound*bni_167] + [bni_167]x4[22] ≥ 0∧[(-1)bso_168] ≥ 0)
(128) (x6[22] ≥ 0 ⇒ (UIncreasing(COND_7152_1_TEST_INVOKEMETHOD10(>=(x6[22], 0), 8577_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[22], x2[22], x3[22]))), x4[22], x5[22], x6[22], x7[22])), ≥)∧[(-1)bni_167 + (-1)Bound*bni_167] + [bni_167]x4[22] ≥ 0∧[(-1)bso_168] ≥ 0)
(129) (x6[22] ≥ 0 ⇒ (UIncreasing(COND_7152_1_TEST_INVOKEMETHOD10(>=(x6[22], 0), 8577_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[22], x2[22], x3[22]))), x4[22], x5[22], x6[22], x7[22])), ≥)∧0 = 0∧[bni_167] = 0∧[(-1)bni_167 + (-1)Bound*bni_167] ≥ 0∧0 = 0∧0 = 0∧[(-1)bso_168] ≥ 0)
(130) (COND_7152_1_TEST_INVOKEMETHOD10(TRUE, 8577_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[23], x2[23], x3[23]))), x4[23], x5[23], x6[23], x7[23])≥NonInfC∧COND_7152_1_TEST_INVOKEMETHOD10(TRUE, 8577_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[23], x2[23], x3[23]))), x4[23], x5[23], x6[23], x7[23])≥6147_0_TEST_GE(java.lang.Object(ARRAY(DATA_3(x1[23], x2[23], x3[23]))), x4[23], +(x6[23], 1), x5[23])∧(UIncreasing(6147_0_TEST_GE(java.lang.Object(ARRAY(DATA_3(x1[23], x2[23], x3[23]))), x4[23], +(x6[23], 1), x5[23])), ≥))
(131) ((UIncreasing(6147_0_TEST_GE(java.lang.Object(ARRAY(DATA_3(x1[23], x2[23], x3[23]))), x4[23], +(x6[23], 1), x5[23])), ≥)∧[(-1)bso_170] ≥ 0)
(132) ((UIncreasing(6147_0_TEST_GE(java.lang.Object(ARRAY(DATA_3(x1[23], x2[23], x3[23]))), x4[23], +(x6[23], 1), x5[23])), ≥)∧[(-1)bso_170] ≥ 0)
(133) ((UIncreasing(6147_0_TEST_GE(java.lang.Object(ARRAY(DATA_3(x1[23], x2[23], x3[23]))), x4[23], +(x6[23], 1), x5[23])), ≥)∧[(-1)bso_170] ≥ 0)
(134) ((UIncreasing(6147_0_TEST_GE(java.lang.Object(ARRAY(DATA_3(x1[23], x2[23], x3[23]))), x4[23], +(x6[23], 1), x5[23])), ≥)∧0 = 0∧0 = 0∧0 = 0∧[(-1)bso_170] ≥ 0)
(135) (>=(x6[24], 0)=TRUE∧java.lang.Object(ARRAY(DATA_3(x1[24], x2[24], x3[24])))=java.lang.Object(ARRAY(DATA_3(x1[25], x2[25], x3[25])))∧x4[24]=x4[25]∧x5[24]=x5[25]∧x6[24]=x6[25]∧x7[24]=x7[25] ⇒ 7152_1_TEST_INVOKEMETHOD(8601_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[24], x2[24], x3[24]))), x4[24], x5[24], x6[24], x7[24])≥NonInfC∧7152_1_TEST_INVOKEMETHOD(8601_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[24], x2[24], x3[24]))), x4[24], x5[24], x6[24], x7[24])≥COND_7152_1_TEST_INVOKEMETHOD11(>=(x6[24], 0), 8601_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[24], x2[24], x3[24]))), x4[24], x5[24], x6[24], x7[24])∧(UIncreasing(COND_7152_1_TEST_INVOKEMETHOD11(>=(x6[24], 0), 8601_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[24], x2[24], x3[24]))), x4[24], x5[24], x6[24], x7[24])), ≥))
(136) (>=(x6[24], 0)=TRUE ⇒ 7152_1_TEST_INVOKEMETHOD(8601_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[24], x2[24], x3[24]))), x4[24], x5[24], x6[24], x7[24])≥NonInfC∧7152_1_TEST_INVOKEMETHOD(8601_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[24], x2[24], x3[24]))), x4[24], x5[24], x6[24], x7[24])≥COND_7152_1_TEST_INVOKEMETHOD11(>=(x6[24], 0), 8601_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[24], x2[24], x3[24]))), x4[24], x5[24], x6[24], x7[24])∧(UIncreasing(COND_7152_1_TEST_INVOKEMETHOD11(>=(x6[24], 0), 8601_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[24], x2[24], x3[24]))), x4[24], x5[24], x6[24], x7[24])), ≥))
(137) (x6[24] ≥ 0 ⇒ (UIncreasing(COND_7152_1_TEST_INVOKEMETHOD11(>=(x6[24], 0), 8601_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[24], x2[24], x3[24]))), x4[24], x5[24], x6[24], x7[24])), ≥)∧[(-1)bni_171 + (-1)Bound*bni_171] + [bni_171]x4[24] ≥ 0∧[(-1)bso_172] ≥ 0)
(138) (x6[24] ≥ 0 ⇒ (UIncreasing(COND_7152_1_TEST_INVOKEMETHOD11(>=(x6[24], 0), 8601_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[24], x2[24], x3[24]))), x4[24], x5[24], x6[24], x7[24])), ≥)∧[(-1)bni_171 + (-1)Bound*bni_171] + [bni_171]x4[24] ≥ 0∧[(-1)bso_172] ≥ 0)
(139) (x6[24] ≥ 0 ⇒ (UIncreasing(COND_7152_1_TEST_INVOKEMETHOD11(>=(x6[24], 0), 8601_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[24], x2[24], x3[24]))), x4[24], x5[24], x6[24], x7[24])), ≥)∧[(-1)bni_171 + (-1)Bound*bni_171] + [bni_171]x4[24] ≥ 0∧[(-1)bso_172] ≥ 0)
(140) (x6[24] ≥ 0 ⇒ (UIncreasing(COND_7152_1_TEST_INVOKEMETHOD11(>=(x6[24], 0), 8601_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[24], x2[24], x3[24]))), x4[24], x5[24], x6[24], x7[24])), ≥)∧0 = 0∧[bni_171] = 0∧[(-1)bni_171 + (-1)Bound*bni_171] ≥ 0∧0 = 0∧0 = 0∧[(-1)bso_172] ≥ 0)
(141) (COND_7152_1_TEST_INVOKEMETHOD11(TRUE, 8601_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[25], x2[25], x3[25]))), x4[25], x5[25], x6[25], x7[25])≥NonInfC∧COND_7152_1_TEST_INVOKEMETHOD11(TRUE, 8601_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[25], x2[25], x3[25]))), x4[25], x5[25], x6[25], x7[25])≥6147_0_TEST_GE(java.lang.Object(ARRAY(DATA_3(x1[25], x2[25], x3[25]))), x4[25], +(x6[25], 1), x5[25])∧(UIncreasing(6147_0_TEST_GE(java.lang.Object(ARRAY(DATA_3(x1[25], x2[25], x3[25]))), x4[25], +(x6[25], 1), x5[25])), ≥))
(142) ((UIncreasing(6147_0_TEST_GE(java.lang.Object(ARRAY(DATA_3(x1[25], x2[25], x3[25]))), x4[25], +(x6[25], 1), x5[25])), ≥)∧[(-1)bso_174] ≥ 0)
(143) ((UIncreasing(6147_0_TEST_GE(java.lang.Object(ARRAY(DATA_3(x1[25], x2[25], x3[25]))), x4[25], +(x6[25], 1), x5[25])), ≥)∧[(-1)bso_174] ≥ 0)
(144) ((UIncreasing(6147_0_TEST_GE(java.lang.Object(ARRAY(DATA_3(x1[25], x2[25], x3[25]))), x4[25], +(x6[25], 1), x5[25])), ≥)∧[(-1)bso_174] ≥ 0)
(145) ((UIncreasing(6147_0_TEST_GE(java.lang.Object(ARRAY(DATA_3(x1[25], x2[25], x3[25]))), x4[25], +(x6[25], 1), x5[25])), ≥)∧0 = 0∧0 = 0∧0 = 0∧[(-1)bso_174] ≥ 0)
(146) (>=(x6[26], 0)=TRUE∧java.lang.Object(ARRAY(DATA_3(x1[26], x2[26], x3[26])))=java.lang.Object(ARRAY(DATA_3(x1[27], x2[27], x3[27])))∧x4[26]=x4[27]∧x5[26]=x5[27]∧x6[26]=x6[27]∧x7[26]=x7[27] ⇒ 7152_1_TEST_INVOKEMETHOD(8622_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[26], x2[26], x3[26]))), x4[26], x5[26], x6[26], x7[26])≥NonInfC∧7152_1_TEST_INVOKEMETHOD(8622_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[26], x2[26], x3[26]))), x4[26], x5[26], x6[26], x7[26])≥COND_7152_1_TEST_INVOKEMETHOD12(>=(x6[26], 0), 8622_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[26], x2[26], x3[26]))), x4[26], x5[26], x6[26], x7[26])∧(UIncreasing(COND_7152_1_TEST_INVOKEMETHOD12(>=(x6[26], 0), 8622_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[26], x2[26], x3[26]))), x4[26], x5[26], x6[26], x7[26])), ≥))
(147) (>=(x6[26], 0)=TRUE ⇒ 7152_1_TEST_INVOKEMETHOD(8622_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[26], x2[26], x3[26]))), x4[26], x5[26], x6[26], x7[26])≥NonInfC∧7152_1_TEST_INVOKEMETHOD(8622_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[26], x2[26], x3[26]))), x4[26], x5[26], x6[26], x7[26])≥COND_7152_1_TEST_INVOKEMETHOD12(>=(x6[26], 0), 8622_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[26], x2[26], x3[26]))), x4[26], x5[26], x6[26], x7[26])∧(UIncreasing(COND_7152_1_TEST_INVOKEMETHOD12(>=(x6[26], 0), 8622_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[26], x2[26], x3[26]))), x4[26], x5[26], x6[26], x7[26])), ≥))
(148) (x6[26] ≥ 0 ⇒ (UIncreasing(COND_7152_1_TEST_INVOKEMETHOD12(>=(x6[26], 0), 8622_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[26], x2[26], x3[26]))), x4[26], x5[26], x6[26], x7[26])), ≥)∧[(-1)bni_175 + (-1)Bound*bni_175] + [bni_175]x4[26] ≥ 0∧[(-1)bso_176] ≥ 0)
(149) (x6[26] ≥ 0 ⇒ (UIncreasing(COND_7152_1_TEST_INVOKEMETHOD12(>=(x6[26], 0), 8622_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[26], x2[26], x3[26]))), x4[26], x5[26], x6[26], x7[26])), ≥)∧[(-1)bni_175 + (-1)Bound*bni_175] + [bni_175]x4[26] ≥ 0∧[(-1)bso_176] ≥ 0)
(150) (x6[26] ≥ 0 ⇒ (UIncreasing(COND_7152_1_TEST_INVOKEMETHOD12(>=(x6[26], 0), 8622_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[26], x2[26], x3[26]))), x4[26], x5[26], x6[26], x7[26])), ≥)∧[(-1)bni_175 + (-1)Bound*bni_175] + [bni_175]x4[26] ≥ 0∧[(-1)bso_176] ≥ 0)
(151) (x6[26] ≥ 0 ⇒ (UIncreasing(COND_7152_1_TEST_INVOKEMETHOD12(>=(x6[26], 0), 8622_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[26], x2[26], x3[26]))), x4[26], x5[26], x6[26], x7[26])), ≥)∧0 = 0∧[bni_175] = 0∧[(-1)bni_175 + (-1)Bound*bni_175] ≥ 0∧0 = 0∧0 = 0∧[(-1)bso_176] ≥ 0)
(152) (COND_7152_1_TEST_INVOKEMETHOD12(TRUE, 8622_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[27], x2[27], x3[27]))), x4[27], x5[27], x6[27], x7[27])≥NonInfC∧COND_7152_1_TEST_INVOKEMETHOD12(TRUE, 8622_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[27], x2[27], x3[27]))), x4[27], x5[27], x6[27], x7[27])≥6147_0_TEST_GE(java.lang.Object(ARRAY(DATA_3(x1[27], x2[27], x3[27]))), x4[27], +(x6[27], 1), x5[27])∧(UIncreasing(6147_0_TEST_GE(java.lang.Object(ARRAY(DATA_3(x1[27], x2[27], x3[27]))), x4[27], +(x6[27], 1), x5[27])), ≥))
(153) ((UIncreasing(6147_0_TEST_GE(java.lang.Object(ARRAY(DATA_3(x1[27], x2[27], x3[27]))), x4[27], +(x6[27], 1), x5[27])), ≥)∧[(-1)bso_178] ≥ 0)
(154) ((UIncreasing(6147_0_TEST_GE(java.lang.Object(ARRAY(DATA_3(x1[27], x2[27], x3[27]))), x4[27], +(x6[27], 1), x5[27])), ≥)∧[(-1)bso_178] ≥ 0)
(155) ((UIncreasing(6147_0_TEST_GE(java.lang.Object(ARRAY(DATA_3(x1[27], x2[27], x3[27]))), x4[27], +(x6[27], 1), x5[27])), ≥)∧[(-1)bso_178] ≥ 0)
(156) ((UIncreasing(6147_0_TEST_GE(java.lang.Object(ARRAY(DATA_3(x1[27], x2[27], x3[27]))), x4[27], +(x6[27], 1), x5[27])), ≥)∧0 = 0∧0 = 0∧0 = 0∧[(-1)bso_178] ≥ 0)
(157) (&&(&&(&&(<=(x5[28], x4[28]), >=(x3[28], 0)), >=(2, -(x3[28], 1))), <=(0, -(x3[28], 1)))=TRUE∧java.lang.Object(ARRAY(DATA_3(x0[28], x1[28], x2[28])))=java.lang.Object(ARRAY(DATA_3(x0[29], x1[29], x2[29])))∧x3[28]=x3[29]∧x4[28]=x4[29]∧x5[28]=x5[29] ⇒ 6147_0_TEST_GE(java.lang.Object(ARRAY(DATA_3(x0[28], x1[28], x2[28]))), x3[28], x4[28], x5[28])≥NonInfC∧6147_0_TEST_GE(java.lang.Object(ARRAY(DATA_3(x0[28], x1[28], x2[28]))), x3[28], x4[28], x5[28])≥COND_6147_0_TEST_GE1(&&(&&(&&(<=(x5[28], x4[28]), >=(x3[28], 0)), >=(2, -(x3[28], 1))), <=(0, -(x3[28], 1))), java.lang.Object(ARRAY(DATA_3(x0[28], x1[28], x2[28]))), x3[28], x4[28], x5[28])∧(UIncreasing(COND_6147_0_TEST_GE1(&&(&&(&&(<=(x5[28], x4[28]), >=(x3[28], 0)), >=(2, -(x3[28], 1))), <=(0, -(x3[28], 1))), java.lang.Object(ARRAY(DATA_3(x0[28], x1[28], x2[28]))), x3[28], x4[28], x5[28])), ≥))
(158) (<=(0, -(x3[28], 1))=TRUE∧>=(2, -(x3[28], 1))=TRUE∧<=(x5[28], x4[28])=TRUE∧>=(x3[28], 0)=TRUE ⇒ 6147_0_TEST_GE(java.lang.Object(ARRAY(DATA_3(x0[28], x1[28], x2[28]))), x3[28], x4[28], x5[28])≥NonInfC∧6147_0_TEST_GE(java.lang.Object(ARRAY(DATA_3(x0[28], x1[28], x2[28]))), x3[28], x4[28], x5[28])≥COND_6147_0_TEST_GE1(&&(&&(&&(<=(x5[28], x4[28]), >=(x3[28], 0)), >=(2, -(x3[28], 1))), <=(0, -(x3[28], 1))), java.lang.Object(ARRAY(DATA_3(x0[28], x1[28], x2[28]))), x3[28], x4[28], x5[28])∧(UIncreasing(COND_6147_0_TEST_GE1(&&(&&(&&(<=(x5[28], x4[28]), >=(x3[28], 0)), >=(2, -(x3[28], 1))), <=(0, -(x3[28], 1))), java.lang.Object(ARRAY(DATA_3(x0[28], x1[28], x2[28]))), x3[28], x4[28], x5[28])), ≥))
(159) (x3[28] + [-1] ≥ 0∧[3] + [-1]x3[28] ≥ 0∧x4[28] + [-1]x5[28] ≥ 0∧x3[28] ≥ 0 ⇒ (UIncreasing(COND_6147_0_TEST_GE1(&&(&&(&&(<=(x5[28], x4[28]), >=(x3[28], 0)), >=(2, -(x3[28], 1))), <=(0, -(x3[28], 1))), java.lang.Object(ARRAY(DATA_3(x0[28], x1[28], x2[28]))), x3[28], x4[28], x5[28])), ≥)∧[(-1)bni_179 + (-1)Bound*bni_179] + [bni_179]x3[28] ≥ 0∧[(-1)bso_180] ≥ 0)
(160) (x3[28] + [-1] ≥ 0∧[3] + [-1]x3[28] ≥ 0∧x4[28] + [-1]x5[28] ≥ 0∧x3[28] ≥ 0 ⇒ (UIncreasing(COND_6147_0_TEST_GE1(&&(&&(&&(<=(x5[28], x4[28]), >=(x3[28], 0)), >=(2, -(x3[28], 1))), <=(0, -(x3[28], 1))), java.lang.Object(ARRAY(DATA_3(x0[28], x1[28], x2[28]))), x3[28], x4[28], x5[28])), ≥)∧[(-1)bni_179 + (-1)Bound*bni_179] + [bni_179]x3[28] ≥ 0∧[(-1)bso_180] ≥ 0)
(161) (x3[28] + [-1] ≥ 0∧[3] + [-1]x3[28] ≥ 0∧x4[28] + [-1]x5[28] ≥ 0∧x3[28] ≥ 0 ⇒ (UIncreasing(COND_6147_0_TEST_GE1(&&(&&(&&(<=(x5[28], x4[28]), >=(x3[28], 0)), >=(2, -(x3[28], 1))), <=(0, -(x3[28], 1))), java.lang.Object(ARRAY(DATA_3(x0[28], x1[28], x2[28]))), x3[28], x4[28], x5[28])), ≥)∧[(-1)bni_179 + (-1)Bound*bni_179] + [bni_179]x3[28] ≥ 0∧[(-1)bso_180] ≥ 0)
(162) (x3[28] ≥ 0∧[2] + [-1]x3[28] ≥ 0∧x4[28] + [-1]x5[28] ≥ 0∧[1] + x3[28] ≥ 0 ⇒ (UIncreasing(COND_6147_0_TEST_GE1(&&(&&(&&(<=(x5[28], x4[28]), >=(x3[28], 0)), >=(2, -(x3[28], 1))), <=(0, -(x3[28], 1))), java.lang.Object(ARRAY(DATA_3(x0[28], x1[28], x2[28]))), x3[28], x4[28], x5[28])), ≥)∧[(-1)Bound*bni_179] + [bni_179]x3[28] ≥ 0∧[(-1)bso_180] ≥ 0)
(163) (x3[28] ≥ 0∧[2] + [-1]x3[28] ≥ 0∧x4[28] ≥ 0∧[1] + x3[28] ≥ 0 ⇒ (UIncreasing(COND_6147_0_TEST_GE1(&&(&&(&&(<=(x5[28], x4[28]), >=(x3[28], 0)), >=(2, -(x3[28], 1))), <=(0, -(x3[28], 1))), java.lang.Object(ARRAY(DATA_3(x0[28], x1[28], x2[28]))), x3[28], x4[28], x5[28])), ≥)∧[(-1)Bound*bni_179] + [bni_179]x3[28] ≥ 0∧[(-1)bso_180] ≥ 0)
(164) (x3[28] ≥ 0∧[2] + [-1]x3[28] ≥ 0∧x4[28] ≥ 0∧[1] + x3[28] ≥ 0∧x5[28] ≥ 0 ⇒ (UIncreasing(COND_6147_0_TEST_GE1(&&(&&(&&(<=(x5[28], x4[28]), >=(x3[28], 0)), >=(2, -(x3[28], 1))), <=(0, -(x3[28], 1))), java.lang.Object(ARRAY(DATA_3(x0[28], x1[28], x2[28]))), x3[28], x4[28], x5[28])), ≥)∧[(-1)Bound*bni_179] + [bni_179]x3[28] ≥ 0∧[(-1)bso_180] ≥ 0)
(165) (x3[28] ≥ 0∧[2] + [-1]x3[28] ≥ 0∧x4[28] ≥ 0∧[1] + x3[28] ≥ 0∧x5[28] ≥ 0 ⇒ (UIncreasing(COND_6147_0_TEST_GE1(&&(&&(&&(<=(x5[28], x4[28]), >=(x3[28], 0)), >=(2, -(x3[28], 1))), <=(0, -(x3[28], 1))), java.lang.Object(ARRAY(DATA_3(x0[28], x1[28], x2[28]))), x3[28], x4[28], x5[28])), ≥)∧[(-1)Bound*bni_179] + [bni_179]x3[28] ≥ 0∧[(-1)bso_180] ≥ 0)
(166) (COND_6147_0_TEST_GE1(TRUE, java.lang.Object(ARRAY(DATA_3(x0[29], x1[29], x2[29]))), x3[29], x4[29], x5[29])≥NonInfC∧COND_6147_0_TEST_GE1(TRUE, java.lang.Object(ARRAY(DATA_3(x0[29], x1[29], x2[29]))), x3[29], x4[29], x5[29])≥6147_0_TEST_GE(java.lang.Object(ARRAY(DATA_3(x0[29], x1[29], x2[29]))), -(x3[29], 1), 0, 0)∧(UIncreasing(6147_0_TEST_GE(java.lang.Object(ARRAY(DATA_3(x0[29], x1[29], x2[29]))), -(x3[29], 1), 0, 0)), ≥))
(167) ((UIncreasing(6147_0_TEST_GE(java.lang.Object(ARRAY(DATA_3(x0[29], x1[29], x2[29]))), -(x3[29], 1), 0, 0)), ≥)∧[1 + (-1)bso_182] ≥ 0)
(168) ((UIncreasing(6147_0_TEST_GE(java.lang.Object(ARRAY(DATA_3(x0[29], x1[29], x2[29]))), -(x3[29], 1), 0, 0)), ≥)∧[1 + (-1)bso_182] ≥ 0)
(169) ((UIncreasing(6147_0_TEST_GE(java.lang.Object(ARRAY(DATA_3(x0[29], x1[29], x2[29]))), -(x3[29], 1), 0, 0)), ≥)∧[1 + (-1)bso_182] ≥ 0)
(170) ((UIncreasing(6147_0_TEST_GE(java.lang.Object(ARRAY(DATA_3(x0[29], x1[29], x2[29]))), -(x3[29], 1), 0, 0)), ≥)∧0 = 0∧0 = 0∧0 = 0∧[1 + (-1)bso_182] ≥ 0)
(171) (&&(&&(&&(<=(x5[30], x4[30]), >=(x3[30], 0)), >=(2, -(x3[30], 1))), <=(0, -(x3[30], 1)))=TRUE∧java.lang.Object(ARRAY(DATA_3(x0[30], x1[30], x2[30])))=java.lang.Object(ARRAY(DATA_3(x0[31], x1[31], x2[31])))∧x3[30]=x3[31]∧x4[30]=x4[31]∧x5[30]=x5[31] ⇒ 6147_0_TEST_GE(java.lang.Object(ARRAY(DATA_3(x0[30], x1[30], x2[30]))), x3[30], x4[30], x5[30])≥NonInfC∧6147_0_TEST_GE(java.lang.Object(ARRAY(DATA_3(x0[30], x1[30], x2[30]))), x3[30], x4[30], x5[30])≥COND_6147_0_TEST_GE2(&&(&&(&&(<=(x5[30], x4[30]), >=(x3[30], 0)), >=(2, -(x3[30], 1))), <=(0, -(x3[30], 1))), java.lang.Object(ARRAY(DATA_3(x0[30], x1[30], x2[30]))), x3[30], x4[30], x5[30])∧(UIncreasing(COND_6147_0_TEST_GE2(&&(&&(&&(<=(x5[30], x4[30]), >=(x3[30], 0)), >=(2, -(x3[30], 1))), <=(0, -(x3[30], 1))), java.lang.Object(ARRAY(DATA_3(x0[30], x1[30], x2[30]))), x3[30], x4[30], x5[30])), ≥))
(172) (<=(0, -(x3[30], 1))=TRUE∧>=(2, -(x3[30], 1))=TRUE∧<=(x5[30], x4[30])=TRUE∧>=(x3[30], 0)=TRUE ⇒ 6147_0_TEST_GE(java.lang.Object(ARRAY(DATA_3(x0[30], x1[30], x2[30]))), x3[30], x4[30], x5[30])≥NonInfC∧6147_0_TEST_GE(java.lang.Object(ARRAY(DATA_3(x0[30], x1[30], x2[30]))), x3[30], x4[30], x5[30])≥COND_6147_0_TEST_GE2(&&(&&(&&(<=(x5[30], x4[30]), >=(x3[30], 0)), >=(2, -(x3[30], 1))), <=(0, -(x3[30], 1))), java.lang.Object(ARRAY(DATA_3(x0[30], x1[30], x2[30]))), x3[30], x4[30], x5[30])∧(UIncreasing(COND_6147_0_TEST_GE2(&&(&&(&&(<=(x5[30], x4[30]), >=(x3[30], 0)), >=(2, -(x3[30], 1))), <=(0, -(x3[30], 1))), java.lang.Object(ARRAY(DATA_3(x0[30], x1[30], x2[30]))), x3[30], x4[30], x5[30])), ≥))
(173) (x3[30] + [-1] ≥ 0∧[3] + [-1]x3[30] ≥ 0∧x4[30] + [-1]x5[30] ≥ 0∧x3[30] ≥ 0 ⇒ (UIncreasing(COND_6147_0_TEST_GE2(&&(&&(&&(<=(x5[30], x4[30]), >=(x3[30], 0)), >=(2, -(x3[30], 1))), <=(0, -(x3[30], 1))), java.lang.Object(ARRAY(DATA_3(x0[30], x1[30], x2[30]))), x3[30], x4[30], x5[30])), ≥)∧[(-1)bni_183 + (-1)Bound*bni_183] + [bni_183]x3[30] ≥ 0∧[(-1)bso_184] ≥ 0)
(174) (x3[30] + [-1] ≥ 0∧[3] + [-1]x3[30] ≥ 0∧x4[30] + [-1]x5[30] ≥ 0∧x3[30] ≥ 0 ⇒ (UIncreasing(COND_6147_0_TEST_GE2(&&(&&(&&(<=(x5[30], x4[30]), >=(x3[30], 0)), >=(2, -(x3[30], 1))), <=(0, -(x3[30], 1))), java.lang.Object(ARRAY(DATA_3(x0[30], x1[30], x2[30]))), x3[30], x4[30], x5[30])), ≥)∧[(-1)bni_183 + (-1)Bound*bni_183] + [bni_183]x3[30] ≥ 0∧[(-1)bso_184] ≥ 0)
(175) (x3[30] + [-1] ≥ 0∧[3] + [-1]x3[30] ≥ 0∧x4[30] + [-1]x5[30] ≥ 0∧x3[30] ≥ 0 ⇒ (UIncreasing(COND_6147_0_TEST_GE2(&&(&&(&&(<=(x5[30], x4[30]), >=(x3[30], 0)), >=(2, -(x3[30], 1))), <=(0, -(x3[30], 1))), java.lang.Object(ARRAY(DATA_3(x0[30], x1[30], x2[30]))), x3[30], x4[30], x5[30])), ≥)∧[(-1)bni_183 + (-1)Bound*bni_183] + [bni_183]x3[30] ≥ 0∧[(-1)bso_184] ≥ 0)
(176) (x3[30] ≥ 0∧[2] + [-1]x3[30] ≥ 0∧x4[30] + [-1]x5[30] ≥ 0∧[1] + x3[30] ≥ 0 ⇒ (UIncreasing(COND_6147_0_TEST_GE2(&&(&&(&&(<=(x5[30], x4[30]), >=(x3[30], 0)), >=(2, -(x3[30], 1))), <=(0, -(x3[30], 1))), java.lang.Object(ARRAY(DATA_3(x0[30], x1[30], x2[30]))), x3[30], x4[30], x5[30])), ≥)∧[(-1)Bound*bni_183] + [bni_183]x3[30] ≥ 0∧[(-1)bso_184] ≥ 0)
(177) (x3[30] ≥ 0∧[2] + [-1]x3[30] ≥ 0∧x4[30] ≥ 0∧[1] + x3[30] ≥ 0 ⇒ (UIncreasing(COND_6147_0_TEST_GE2(&&(&&(&&(<=(x5[30], x4[30]), >=(x3[30], 0)), >=(2, -(x3[30], 1))), <=(0, -(x3[30], 1))), java.lang.Object(ARRAY(DATA_3(x0[30], x1[30], x2[30]))), x3[30], x4[30], x5[30])), ≥)∧[(-1)Bound*bni_183] + [bni_183]x3[30] ≥ 0∧[(-1)bso_184] ≥ 0)
(178) (x3[30] ≥ 0∧[2] + [-1]x3[30] ≥ 0∧x4[30] ≥ 0∧[1] + x3[30] ≥ 0∧x5[30] ≥ 0 ⇒ (UIncreasing(COND_6147_0_TEST_GE2(&&(&&(&&(<=(x5[30], x4[30]), >=(x3[30], 0)), >=(2, -(x3[30], 1))), <=(0, -(x3[30], 1))), java.lang.Object(ARRAY(DATA_3(x0[30], x1[30], x2[30]))), x3[30], x4[30], x5[30])), ≥)∧[(-1)Bound*bni_183] + [bni_183]x3[30] ≥ 0∧[(-1)bso_184] ≥ 0)
(179) (x3[30] ≥ 0∧[2] + [-1]x3[30] ≥ 0∧x4[30] ≥ 0∧[1] + x3[30] ≥ 0∧x5[30] ≥ 0 ⇒ (UIncreasing(COND_6147_0_TEST_GE2(&&(&&(&&(<=(x5[30], x4[30]), >=(x3[30], 0)), >=(2, -(x3[30], 1))), <=(0, -(x3[30], 1))), java.lang.Object(ARRAY(DATA_3(x0[30], x1[30], x2[30]))), x3[30], x4[30], x5[30])), ≥)∧[(-1)Bound*bni_183] + [bni_183]x3[30] ≥ 0∧[(-1)bso_184] ≥ 0)
(180) (COND_6147_0_TEST_GE2(TRUE, java.lang.Object(ARRAY(DATA_3(x0[31], x1[31], x2[31]))), x3[31], x4[31], x5[31])≥NonInfC∧COND_6147_0_TEST_GE2(TRUE, java.lang.Object(ARRAY(DATA_3(x0[31], x1[31], x2[31]))), x3[31], x4[31], x5[31])≥6147_0_TEST_GE(java.lang.Object(ARRAY(DATA_3(x0[31], x1[31], x2[31]))), -(x3[31], 1), 0, 1)∧(UIncreasing(6147_0_TEST_GE(java.lang.Object(ARRAY(DATA_3(x0[31], x1[31], x2[31]))), -(x3[31], 1), 0, 1)), ≥))
(181) ((UIncreasing(6147_0_TEST_GE(java.lang.Object(ARRAY(DATA_3(x0[31], x1[31], x2[31]))), -(x3[31], 1), 0, 1)), ≥)∧[1 + (-1)bso_186] ≥ 0)
(182) ((UIncreasing(6147_0_TEST_GE(java.lang.Object(ARRAY(DATA_3(x0[31], x1[31], x2[31]))), -(x3[31], 1), 0, 1)), ≥)∧[1 + (-1)bso_186] ≥ 0)
(183) ((UIncreasing(6147_0_TEST_GE(java.lang.Object(ARRAY(DATA_3(x0[31], x1[31], x2[31]))), -(x3[31], 1), 0, 1)), ≥)∧[1 + (-1)bso_186] ≥ 0)
(184) ((UIncreasing(6147_0_TEST_GE(java.lang.Object(ARRAY(DATA_3(x0[31], x1[31], x2[31]))), -(x3[31], 1), 0, 1)), ≥)∧0 = 0∧0 = 0∧0 = 0∧[1 + (-1)bso_186] ≥ 0)
(185) (&&(&&(&&(<=(x5[32], x4[32]), >=(x3[32], 0)), >=(2, -(x3[32], 1))), <=(0, -(x3[32], 1)))=TRUE∧java.lang.Object(ARRAY(DATA_3(x0[32], x1[32], x2[32])))=java.lang.Object(ARRAY(DATA_3(x0[33], x1[33], x2[33])))∧x3[32]=x3[33]∧x4[32]=x4[33]∧x5[32]=x5[33] ⇒ 6147_0_TEST_GE(java.lang.Object(ARRAY(DATA_3(x0[32], x1[32], x2[32]))), x3[32], x4[32], x5[32])≥NonInfC∧6147_0_TEST_GE(java.lang.Object(ARRAY(DATA_3(x0[32], x1[32], x2[32]))), x3[32], x4[32], x5[32])≥COND_6147_0_TEST_GE3(&&(&&(&&(<=(x5[32], x4[32]), >=(x3[32], 0)), >=(2, -(x3[32], 1))), <=(0, -(x3[32], 1))), java.lang.Object(ARRAY(DATA_3(x0[32], x1[32], x2[32]))), x3[32], x4[32], x5[32])∧(UIncreasing(COND_6147_0_TEST_GE3(&&(&&(&&(<=(x5[32], x4[32]), >=(x3[32], 0)), >=(2, -(x3[32], 1))), <=(0, -(x3[32], 1))), java.lang.Object(ARRAY(DATA_3(x0[32], x1[32], x2[32]))), x3[32], x4[32], x5[32])), ≥))
(186) (<=(0, -(x3[32], 1))=TRUE∧>=(2, -(x3[32], 1))=TRUE∧<=(x5[32], x4[32])=TRUE∧>=(x3[32], 0)=TRUE ⇒ 6147_0_TEST_GE(java.lang.Object(ARRAY(DATA_3(x0[32], x1[32], x2[32]))), x3[32], x4[32], x5[32])≥NonInfC∧6147_0_TEST_GE(java.lang.Object(ARRAY(DATA_3(x0[32], x1[32], x2[32]))), x3[32], x4[32], x5[32])≥COND_6147_0_TEST_GE3(&&(&&(&&(<=(x5[32], x4[32]), >=(x3[32], 0)), >=(2, -(x3[32], 1))), <=(0, -(x3[32], 1))), java.lang.Object(ARRAY(DATA_3(x0[32], x1[32], x2[32]))), x3[32], x4[32], x5[32])∧(UIncreasing(COND_6147_0_TEST_GE3(&&(&&(&&(<=(x5[32], x4[32]), >=(x3[32], 0)), >=(2, -(x3[32], 1))), <=(0, -(x3[32], 1))), java.lang.Object(ARRAY(DATA_3(x0[32], x1[32], x2[32]))), x3[32], x4[32], x5[32])), ≥))
(187) (x3[32] + [-1] ≥ 0∧[3] + [-1]x3[32] ≥ 0∧x4[32] + [-1]x5[32] ≥ 0∧x3[32] ≥ 0 ⇒ (UIncreasing(COND_6147_0_TEST_GE3(&&(&&(&&(<=(x5[32], x4[32]), >=(x3[32], 0)), >=(2, -(x3[32], 1))), <=(0, -(x3[32], 1))), java.lang.Object(ARRAY(DATA_3(x0[32], x1[32], x2[32]))), x3[32], x4[32], x5[32])), ≥)∧[(-1)bni_187 + (-1)Bound*bni_187] + [bni_187]x3[32] ≥ 0∧[(-1)bso_188] ≥ 0)
(188) (x3[32] + [-1] ≥ 0∧[3] + [-1]x3[32] ≥ 0∧x4[32] + [-1]x5[32] ≥ 0∧x3[32] ≥ 0 ⇒ (UIncreasing(COND_6147_0_TEST_GE3(&&(&&(&&(<=(x5[32], x4[32]), >=(x3[32], 0)), >=(2, -(x3[32], 1))), <=(0, -(x3[32], 1))), java.lang.Object(ARRAY(DATA_3(x0[32], x1[32], x2[32]))), x3[32], x4[32], x5[32])), ≥)∧[(-1)bni_187 + (-1)Bound*bni_187] + [bni_187]x3[32] ≥ 0∧[(-1)bso_188] ≥ 0)
(189) (x3[32] + [-1] ≥ 0∧[3] + [-1]x3[32] ≥ 0∧x4[32] + [-1]x5[32] ≥ 0∧x3[32] ≥ 0 ⇒ (UIncreasing(COND_6147_0_TEST_GE3(&&(&&(&&(<=(x5[32], x4[32]), >=(x3[32], 0)), >=(2, -(x3[32], 1))), <=(0, -(x3[32], 1))), java.lang.Object(ARRAY(DATA_3(x0[32], x1[32], x2[32]))), x3[32], x4[32], x5[32])), ≥)∧[(-1)bni_187 + (-1)Bound*bni_187] + [bni_187]x3[32] ≥ 0∧[(-1)bso_188] ≥ 0)
(190) (x3[32] ≥ 0∧[2] + [-1]x3[32] ≥ 0∧x4[32] + [-1]x5[32] ≥ 0∧[1] + x3[32] ≥ 0 ⇒ (UIncreasing(COND_6147_0_TEST_GE3(&&(&&(&&(<=(x5[32], x4[32]), >=(x3[32], 0)), >=(2, -(x3[32], 1))), <=(0, -(x3[32], 1))), java.lang.Object(ARRAY(DATA_3(x0[32], x1[32], x2[32]))), x3[32], x4[32], x5[32])), ≥)∧[(-1)Bound*bni_187] + [bni_187]x3[32] ≥ 0∧[(-1)bso_188] ≥ 0)
(191) (x3[32] ≥ 0∧[2] + [-1]x3[32] ≥ 0∧x4[32] ≥ 0∧[1] + x3[32] ≥ 0 ⇒ (UIncreasing(COND_6147_0_TEST_GE3(&&(&&(&&(<=(x5[32], x4[32]), >=(x3[32], 0)), >=(2, -(x3[32], 1))), <=(0, -(x3[32], 1))), java.lang.Object(ARRAY(DATA_3(x0[32], x1[32], x2[32]))), x3[32], x4[32], x5[32])), ≥)∧[(-1)Bound*bni_187] + [bni_187]x3[32] ≥ 0∧[(-1)bso_188] ≥ 0)
(192) (x3[32] ≥ 0∧[2] + [-1]x3[32] ≥ 0∧x4[32] ≥ 0∧[1] + x3[32] ≥ 0∧x5[32] ≥ 0 ⇒ (UIncreasing(COND_6147_0_TEST_GE3(&&(&&(&&(<=(x5[32], x4[32]), >=(x3[32], 0)), >=(2, -(x3[32], 1))), <=(0, -(x3[32], 1))), java.lang.Object(ARRAY(DATA_3(x0[32], x1[32], x2[32]))), x3[32], x4[32], x5[32])), ≥)∧[(-1)Bound*bni_187] + [bni_187]x3[32] ≥ 0∧[(-1)bso_188] ≥ 0)
(193) (x3[32] ≥ 0∧[2] + [-1]x3[32] ≥ 0∧x4[32] ≥ 0∧[1] + x3[32] ≥ 0∧x5[32] ≥ 0 ⇒ (UIncreasing(COND_6147_0_TEST_GE3(&&(&&(&&(<=(x5[32], x4[32]), >=(x3[32], 0)), >=(2, -(x3[32], 1))), <=(0, -(x3[32], 1))), java.lang.Object(ARRAY(DATA_3(x0[32], x1[32], x2[32]))), x3[32], x4[32], x5[32])), ≥)∧[(-1)Bound*bni_187] + [bni_187]x3[32] ≥ 0∧[(-1)bso_188] ≥ 0)
(194) (COND_6147_0_TEST_GE3(TRUE, java.lang.Object(ARRAY(DATA_3(x0[33], x1[33], x2[33]))), x3[33], x4[33], x5[33])≥NonInfC∧COND_6147_0_TEST_GE3(TRUE, java.lang.Object(ARRAY(DATA_3(x0[33], x1[33], x2[33]))), x3[33], x4[33], x5[33])≥6147_0_TEST_GE(java.lang.Object(ARRAY(DATA_3(x0[33], x1[33], x2[33]))), -(x3[33], 1), 0, x6[33])∧(UIncreasing(6147_0_TEST_GE(java.lang.Object(ARRAY(DATA_3(x0[33], x1[33], x2[33]))), -(x3[33], 1), 0, x6[33])), ≥))
(195) ((UIncreasing(6147_0_TEST_GE(java.lang.Object(ARRAY(DATA_3(x0[33], x1[33], x2[33]))), -(x3[33], 1), 0, x6[33])), ≥)∧[1 + (-1)bso_190] ≥ 0)
(196) ((UIncreasing(6147_0_TEST_GE(java.lang.Object(ARRAY(DATA_3(x0[33], x1[33], x2[33]))), -(x3[33], 1), 0, x6[33])), ≥)∧[1 + (-1)bso_190] ≥ 0)
(197) ((UIncreasing(6147_0_TEST_GE(java.lang.Object(ARRAY(DATA_3(x0[33], x1[33], x2[33]))), -(x3[33], 1), 0, x6[33])), ≥)∧[1 + (-1)bso_190] ≥ 0)
(198) ((UIncreasing(6147_0_TEST_GE(java.lang.Object(ARRAY(DATA_3(x0[33], x1[33], x2[33]))), -(x3[33], 1), 0, x6[33])), ≥)∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧[1 + (-1)bso_190] ≥ 0)
POL(TRUE) = 0
POL(FALSE) = 0
POL(3816_0_length_Load(x1)) = [-1]
POL(2393_0_length_NONNULL) = [-1]
POL(7391_1_test_InvokeMethod(x1, x2, x3)) = [-1]
POL(3458_0_test_Return) = [-1]
POL(java.lang.Object(x1)) = [-1]
POL(ARRAY(x1)) = [-1]
POL(DATA_3(x1, x2, x3)) = [-1]
POL(-1) = [-1]
POL(7661_0_test_Return) = [-1]
POL(7152_0_bubble_Load(x1)) = [-1]
POL(5194_0_bubble_LE(x1)) = [-1]
POL(NULL) = [-1]
POL(4383_0_bubble_Return) = [-1]
POL(List(x1)) = [-1]
POL(EOC) = [-1]
POL(4580_0_bubble_Return) = [-1]
POL(5132_0_bubble_LE) = [-1]
POL(8096_1_bubble_InvokeMethod(x1)) = [-1]
POL(8096_0_bubble_Load(x1)) = [-1]
POL(8175_0_bubble_Return) = [-1]
POL(4619_0_bubble_Return) = [-1]
POL(4650_0_bubble_Return(x1)) = [-1]
POL(4673_0_bubble_Return) = [-1]
POL(8557_0_bubble_Return) = [-1]
POL(8233_0_bubble_Return) = [-1]
POL(8255_0_bubble_Return) = [-1]
POL(8259_0_bubble_Return) = [-1]
POL(8577_0_bubble_Return) = [-1]
POL(8601_0_bubble_Return) = [-1]
POL(8622_0_bubble_Return) = [-1]
POL(5178_0_bubble_LE) = [-1]
POL(8145_1_bubble_InvokeMethod(x1)) = [-1]
POL(5207_0_bubble_LE) = [-1]
POL(8205_1_bubble_InvokeMethod(x1)) = [-1]
POL(8177_1_bubble_InvokeMethod(x1)) = [-1]
POL(2421_0_length_Return) = [-1]
POL(2540_1_length_InvokeMethod(x1)) = [-1] + [-1]x1
POL(2643_0_length_Return) = [-1]
POL(3981_0_length_Return(x1)) = x1
POL(Cond_2540_1_length_InvokeMethod(x1, x2)) = [-1] + [-1]x2
POL(>(x1, x2)) = [-1]
POL(0) = 0
POL(+(x1, x2)) = x1 + x2
POL(1) = [1]
POL(4014_0_length_Return(x1)) = x1
POL(Cond_2540_1_length_InvokeMethod1(x1, x2)) = [-1] + [-1]x2
POL(4046_0_length_Return(x1)) = x1
POL(Cond_2540_1_length_InvokeMethod2(x1, x2)) = [-1] + [-1]x2
POL(4077_0_length_Return(x1)) = x1
POL(Cond_2540_1_length_InvokeMethod3(x1, x2)) = [-1] + [-1]x2
POL(Cond_2540_1_length_InvokeMethod4(x1, x2)) = [-1]
POL(2680_0_length_Return) = [-1]
POL(Cond_2540_1_length_InvokeMethod5(x1, x2)) = [-1]
POL(2718_0_length_Return) = [-1]
POL(Cond_2540_1_length_InvokeMethod6(x1, x2)) = [-1]
POL(2734_0_length_Return) = [-1]
POL(Cond_2540_1_length_InvokeMethod7(x1, x2)) = [-1]
POL(Cond_2578_1_length_InvokeMethod(x1, x2)) = [-1] + [-1]x2
POL(Cond_2578_1_length_InvokeMethod1(x1, x2)) = [-1] + [-1]x2
POL(Cond_2578_1_length_InvokeMethod2(x1, x2)) = [-1] + [-1]x2
POL(Cond_2578_1_length_InvokeMethod3(x1, x2)) = [-1] + [-1]x2
POL(Cond_2578_1_length_InvokeMethod4(x1, x2)) = [-1]
POL(Cond_2578_1_length_InvokeMethod5(x1, x2)) = [-1]
POL(Cond_2578_1_length_InvokeMethod6(x1, x2)) = [-1]
POL(Cond_2578_1_length_InvokeMethod7(x1, x2)) = [-1]
POL(Cond_2618_1_length_InvokeMethod(x1, x2)) = [-1] + [-1]x2
POL(Cond_2618_1_length_InvokeMethod1(x1, x2)) = [-1] + [-1]x2
POL(Cond_2618_1_length_InvokeMethod2(x1, x2)) = [-1] + [-1]x2
POL(Cond_2618_1_length_InvokeMethod3(x1, x2)) = [-1] + [-1]x2
POL(Cond_2618_1_length_InvokeMethod4(x1, x2)) = [-1]
POL(Cond_2618_1_length_InvokeMethod5(x1, x2)) = [-1]
POL(Cond_2618_1_length_InvokeMethod6(x1, x2)) = [-1]
POL(Cond_2618_1_length_InvokeMethod7(x1, x2)) = [-1]
POL(Cond_2598_1_length_InvokeMethod(x1, x2)) = [-1] + [-1]x2
POL(Cond_2598_1_length_InvokeMethod1(x1, x2)) = [-1] + [-1]x2
POL(Cond_2598_1_length_InvokeMethod2(x1, x2)) = [-1] + [-1]x2
POL(Cond_2598_1_length_InvokeMethod3(x1, x2)) = [-1] + [-1]x2
POL(Cond_2598_1_length_InvokeMethod4(x1, x2)) = [-1]
POL(Cond_2598_1_length_InvokeMethod5(x1, x2)) = [-1]
POL(Cond_2598_1_length_InvokeMethod6(x1, x2)) = [-1]
POL(Cond_2598_1_length_InvokeMethod7(x1, x2)) = [-1]
POL(8113_0_bubble_Return) = [-1]
POL(8159_0_bubble_Return) = [-1]
POL(8219_0_bubble_Return) = [-1]
POL(8190_0_bubble_Return) = [-1]
POL(6147_0_TEST_GE(x1, x2, x3, x4)) = [-1] + x2
POL(COND_6147_0_TEST_GE(x1, x2, x3, x4, x5)) = [-1] + x3
POL(&&(x1, x2)) = [-1]
POL(<(x1, x2)) = [-1]
POL(>=(x1, x2)) = [-1]
POL(<=(x1, x2)) = [-1]
POL(2) = [2]
POL(7152_1_TEST_INVOKEMETHOD(x1, x2, x3, x4, x5, x6)) = [-1] + x3
POL(COND_7152_1_TEST_INVOKEMETHOD(x1, x2, x3, x4, x5, x6, x7)) = [-1] + x4
POL(COND_7152_1_TEST_INVOKEMETHOD1(x1, x2, x3, x4, x5, x6, x7)) = [-1] + x4
POL(COND_7152_1_TEST_INVOKEMETHOD2(x1, x2, x3, x4, x5, x6, x7)) = [-1] + x4
POL(COND_7152_1_TEST_INVOKEMETHOD3(x1, x2, x3, x4, x5, x6, x7)) = [-1] + x4
POL(COND_7152_1_TEST_INVOKEMETHOD4(x1, x2, x3, x4, x5, x6, x7)) = [-1] + x4
POL(COND_7152_1_TEST_INVOKEMETHOD5(x1, x2, x3, x4, x5, x6, x7)) = [-1] + x4
POL(COND_7152_1_TEST_INVOKEMETHOD6(x1, x2, x3, x4, x5, x6, x7)) = [-1] + x4
POL(COND_7152_1_TEST_INVOKEMETHOD7(x1, x2, x3, x4, x5, x6, x7)) = [-1] + x4
POL(COND_7152_1_TEST_INVOKEMETHOD8(x1, x2, x3, x4, x5, x6, x7)) = [-1] + x4
POL(COND_7152_1_TEST_INVOKEMETHOD9(x1, x2, x3, x4, x5, x6, x7)) = [-1] + x4
POL(COND_7152_1_TEST_INVOKEMETHOD10(x1, x2, x3, x4, x5, x6, x7)) = [-1] + x4
POL(COND_7152_1_TEST_INVOKEMETHOD11(x1, x2, x3, x4, x5, x6, x7)) = [-1] + x4
POL(COND_7152_1_TEST_INVOKEMETHOD12(x1, x2, x3, x4, x5, x6, x7)) = [-1] + x4
POL(COND_6147_0_TEST_GE1(x1, x2, x3, x4, x5)) = [-1] + x3
POL(-(x1, x2)) = x1 + [-1]x2
POL(COND_6147_0_TEST_GE2(x1, x2, x3, x4, x5)) = [-1] + x3
POL(COND_6147_0_TEST_GE3(x1, x2, x3, x4, x5)) = [-1] + x3
COND_6147_0_TEST_GE1(TRUE, java.lang.Object(ARRAY(DATA_3(x0[29], x1[29], x2[29]))), x3[29], x4[29], x5[29]) → 6147_0_TEST_GE(java.lang.Object(ARRAY(DATA_3(x0[29], x1[29], x2[29]))), -(x3[29], 1), 0, 0)
COND_6147_0_TEST_GE2(TRUE, java.lang.Object(ARRAY(DATA_3(x0[31], x1[31], x2[31]))), x3[31], x4[31], x5[31]) → 6147_0_TEST_GE(java.lang.Object(ARRAY(DATA_3(x0[31], x1[31], x2[31]))), -(x3[31], 1), 0, 1)
COND_6147_0_TEST_GE3(TRUE, java.lang.Object(ARRAY(DATA_3(x0[33], x1[33], x2[33]))), x3[33], x4[33], x5[33]) → 6147_0_TEST_GE(java.lang.Object(ARRAY(DATA_3(x0[33], x1[33], x2[33]))), -(x3[33], 1), 0, x6[33])
6147_0_TEST_GE(java.lang.Object(ARRAY(DATA_3(x1[0], x2[0], x3[0]))), x4[0], x6[0], x5[0]) → COND_6147_0_TEST_GE(&&(&&(<(x6[0], x5[0]), >=(x4[0], 0)), <=(x4[0], 2)), java.lang.Object(ARRAY(DATA_3(x1[0], x2[0], x3[0]))), x4[0], x6[0], x5[0])
6147_0_TEST_GE(java.lang.Object(ARRAY(DATA_3(x0[28], x1[28], x2[28]))), x3[28], x4[28], x5[28]) → COND_6147_0_TEST_GE1(&&(&&(&&(<=(x5[28], x4[28]), >=(x3[28], 0)), >=(2, -(x3[28], 1))), <=(0, -(x3[28], 1))), java.lang.Object(ARRAY(DATA_3(x0[28], x1[28], x2[28]))), x3[28], x4[28], x5[28])
6147_0_TEST_GE(java.lang.Object(ARRAY(DATA_3(x0[30], x1[30], x2[30]))), x3[30], x4[30], x5[30]) → COND_6147_0_TEST_GE2(&&(&&(&&(<=(x5[30], x4[30]), >=(x3[30], 0)), >=(2, -(x3[30], 1))), <=(0, -(x3[30], 1))), java.lang.Object(ARRAY(DATA_3(x0[30], x1[30], x2[30]))), x3[30], x4[30], x5[30])
6147_0_TEST_GE(java.lang.Object(ARRAY(DATA_3(x0[32], x1[32], x2[32]))), x3[32], x4[32], x5[32]) → COND_6147_0_TEST_GE3(&&(&&(&&(<=(x5[32], x4[32]), >=(x3[32], 0)), >=(2, -(x3[32], 1))), <=(0, -(x3[32], 1))), java.lang.Object(ARRAY(DATA_3(x0[32], x1[32], x2[32]))), x3[32], x4[32], x5[32])
6147_0_TEST_GE(java.lang.Object(ARRAY(DATA_3(x1[0], x2[0], x3[0]))), x4[0], x6[0], x5[0]) → COND_6147_0_TEST_GE(&&(&&(<(x6[0], x5[0]), >=(x4[0], 0)), <=(x4[0], 2)), java.lang.Object(ARRAY(DATA_3(x1[0], x2[0], x3[0]))), x4[0], x6[0], x5[0])
COND_6147_0_TEST_GE(TRUE, java.lang.Object(ARRAY(DATA_3(x1[1], x2[1], x3[1]))), x4[1], x6[1], x5[1]) → 7152_1_TEST_INVOKEMETHOD(7152_0_bubble_Load(x7[1]), java.lang.Object(ARRAY(DATA_3(x1[1], x2[1], x3[1]))), x4[1], x5[1], x6[1], x7[1])
7152_1_TEST_INVOKEMETHOD(4383_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[2], x2[2], x3[2]))), x4[2], x5[2], x6[2], NULL) → COND_7152_1_TEST_INVOKEMETHOD(>=(x6[2], 0), 4383_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[2], x2[2], x3[2]))), x4[2], x5[2], x6[2], NULL)
COND_7152_1_TEST_INVOKEMETHOD(TRUE, 4383_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[3], x2[3], x3[3]))), x4[3], x5[3], x6[3], NULL) → 6147_0_TEST_GE(java.lang.Object(ARRAY(DATA_3(x1[3], x2[3], x3[3]))), x4[3], +(x6[3], 1), x5[3])
7152_1_TEST_INVOKEMETHOD(4580_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[4], x2[4], x3[4]))), x4[4], x5[4], x6[4], java.lang.Object(List(EOC))) → COND_7152_1_TEST_INVOKEMETHOD1(>=(x6[4], 0), 4580_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[4], x2[4], x3[4]))), x4[4], x5[4], x6[4], java.lang.Object(List(EOC)))
COND_7152_1_TEST_INVOKEMETHOD1(TRUE, 4580_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[5], x2[5], x3[5]))), x4[5], x5[5], x6[5], java.lang.Object(List(EOC))) → 6147_0_TEST_GE(java.lang.Object(ARRAY(DATA_3(x1[5], x2[5], x3[5]))), x4[5], +(x6[5], 1), x5[5])
7152_1_TEST_INVOKEMETHOD(4619_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[6], x2[6], x3[6]))), x4[6], x5[6], x6[6], java.lang.Object(List(EOC))) → COND_7152_1_TEST_INVOKEMETHOD2(>=(x6[6], 0), 4619_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[6], x2[6], x3[6]))), x4[6], x5[6], x6[6], java.lang.Object(List(EOC)))
COND_7152_1_TEST_INVOKEMETHOD2(TRUE, 4619_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[7], x2[7], x3[7]))), x4[7], x5[7], x6[7], java.lang.Object(List(EOC))) → 6147_0_TEST_GE(java.lang.Object(ARRAY(DATA_3(x1[7], x2[7], x3[7]))), x4[7], +(x6[7], 1), x5[7])
7152_1_TEST_INVOKEMETHOD(4650_0_bubble_Return(java.lang.Object(List(x0[8]))), java.lang.Object(ARRAY(DATA_3(x2[8], x3[8], x4[8]))), x5[8], x6[8], x7[8], java.lang.Object(List(x0[8]))) → COND_7152_1_TEST_INVOKEMETHOD3(>=(x7[8], 0), 4650_0_bubble_Return(java.lang.Object(List(x0[8]))), java.lang.Object(ARRAY(DATA_3(x2[8], x3[8], x4[8]))), x5[8], x6[8], x7[8], java.lang.Object(List(x0[8])))
COND_7152_1_TEST_INVOKEMETHOD3(TRUE, 4650_0_bubble_Return(java.lang.Object(List(x0[9]))), java.lang.Object(ARRAY(DATA_3(x2[9], x3[9], x4[9]))), x5[9], x6[9], x7[9], java.lang.Object(List(x0[9]))) → 6147_0_TEST_GE(java.lang.Object(ARRAY(DATA_3(x2[9], x3[9], x4[9]))), x5[9], +(x7[9], 1), x6[9])
7152_1_TEST_INVOKEMETHOD(4673_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[10], x2[10], x3[10]))), x4[10], x5[10], x6[10], java.lang.Object(List(EOC))) → COND_7152_1_TEST_INVOKEMETHOD4(>=(x6[10], 0), 4673_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[10], x2[10], x3[10]))), x4[10], x5[10], x6[10], java.lang.Object(List(EOC)))
COND_7152_1_TEST_INVOKEMETHOD4(TRUE, 4673_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[11], x2[11], x3[11]))), x4[11], x5[11], x6[11], java.lang.Object(List(EOC))) → 6147_0_TEST_GE(java.lang.Object(ARRAY(DATA_3(x1[11], x2[11], x3[11]))), x4[11], +(x6[11], 1), x5[11])
7152_1_TEST_INVOKEMETHOD(8175_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[12], x2[12], x3[12]))), x4[12], x5[12], x6[12], x7[12]) → COND_7152_1_TEST_INVOKEMETHOD5(>=(x6[12], 0), 8175_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[12], x2[12], x3[12]))), x4[12], x5[12], x6[12], x7[12])
COND_7152_1_TEST_INVOKEMETHOD5(TRUE, 8175_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[13], x2[13], x3[13]))), x4[13], x5[13], x6[13], x7[13]) → 6147_0_TEST_GE(java.lang.Object(ARRAY(DATA_3(x1[13], x2[13], x3[13]))), x4[13], +(x6[13], 1), x5[13])
7152_1_TEST_INVOKEMETHOD(8233_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[14], x2[14], x3[14]))), x4[14], x5[14], x6[14], x7[14]) → COND_7152_1_TEST_INVOKEMETHOD6(>=(x6[14], 0), 8233_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[14], x2[14], x3[14]))), x4[14], x5[14], x6[14], x7[14])
COND_7152_1_TEST_INVOKEMETHOD6(TRUE, 8233_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[15], x2[15], x3[15]))), x4[15], x5[15], x6[15], x7[15]) → 6147_0_TEST_GE(java.lang.Object(ARRAY(DATA_3(x1[15], x2[15], x3[15]))), x4[15], +(x6[15], 1), x5[15])
7152_1_TEST_INVOKEMETHOD(8255_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[16], x2[16], x3[16]))), x4[16], x5[16], x6[16], x7[16]) → COND_7152_1_TEST_INVOKEMETHOD7(>=(x6[16], 0), 8255_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[16], x2[16], x3[16]))), x4[16], x5[16], x6[16], x7[16])
COND_7152_1_TEST_INVOKEMETHOD7(TRUE, 8255_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[17], x2[17], x3[17]))), x4[17], x5[17], x6[17], x7[17]) → 6147_0_TEST_GE(java.lang.Object(ARRAY(DATA_3(x1[17], x2[17], x3[17]))), x4[17], +(x6[17], 1), x5[17])
7152_1_TEST_INVOKEMETHOD(8259_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[18], x2[18], x3[18]))), x4[18], x5[18], x6[18], x7[18]) → COND_7152_1_TEST_INVOKEMETHOD8(>=(x6[18], 0), 8259_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[18], x2[18], x3[18]))), x4[18], x5[18], x6[18], x7[18])
COND_7152_1_TEST_INVOKEMETHOD8(TRUE, 8259_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[19], x2[19], x3[19]))), x4[19], x5[19], x6[19], x7[19]) → 6147_0_TEST_GE(java.lang.Object(ARRAY(DATA_3(x1[19], x2[19], x3[19]))), x4[19], +(x6[19], 1), x5[19])
7152_1_TEST_INVOKEMETHOD(8557_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[20], x2[20], x3[20]))), x4[20], x5[20], x6[20], x7[20]) → COND_7152_1_TEST_INVOKEMETHOD9(>=(x6[20], 0), 8557_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[20], x2[20], x3[20]))), x4[20], x5[20], x6[20], x7[20])
COND_7152_1_TEST_INVOKEMETHOD9(TRUE, 8557_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[21], x2[21], x3[21]))), x4[21], x5[21], x6[21], x7[21]) → 6147_0_TEST_GE(java.lang.Object(ARRAY(DATA_3(x1[21], x2[21], x3[21]))), x4[21], +(x6[21], 1), x5[21])
7152_1_TEST_INVOKEMETHOD(8577_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[22], x2[22], x3[22]))), x4[22], x5[22], x6[22], x7[22]) → COND_7152_1_TEST_INVOKEMETHOD10(>=(x6[22], 0), 8577_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[22], x2[22], x3[22]))), x4[22], x5[22], x6[22], x7[22])
COND_7152_1_TEST_INVOKEMETHOD10(TRUE, 8577_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[23], x2[23], x3[23]))), x4[23], x5[23], x6[23], x7[23]) → 6147_0_TEST_GE(java.lang.Object(ARRAY(DATA_3(x1[23], x2[23], x3[23]))), x4[23], +(x6[23], 1), x5[23])
7152_1_TEST_INVOKEMETHOD(8601_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[24], x2[24], x3[24]))), x4[24], x5[24], x6[24], x7[24]) → COND_7152_1_TEST_INVOKEMETHOD11(>=(x6[24], 0), 8601_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[24], x2[24], x3[24]))), x4[24], x5[24], x6[24], x7[24])
COND_7152_1_TEST_INVOKEMETHOD11(TRUE, 8601_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[25], x2[25], x3[25]))), x4[25], x5[25], x6[25], x7[25]) → 6147_0_TEST_GE(java.lang.Object(ARRAY(DATA_3(x1[25], x2[25], x3[25]))), x4[25], +(x6[25], 1), x5[25])
7152_1_TEST_INVOKEMETHOD(8622_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[26], x2[26], x3[26]))), x4[26], x5[26], x6[26], x7[26]) → COND_7152_1_TEST_INVOKEMETHOD12(>=(x6[26], 0), 8622_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[26], x2[26], x3[26]))), x4[26], x5[26], x6[26], x7[26])
COND_7152_1_TEST_INVOKEMETHOD12(TRUE, 8622_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[27], x2[27], x3[27]))), x4[27], x5[27], x6[27], x7[27]) → 6147_0_TEST_GE(java.lang.Object(ARRAY(DATA_3(x1[27], x2[27], x3[27]))), x4[27], +(x6[27], 1), x5[27])
6147_0_TEST_GE(java.lang.Object(ARRAY(DATA_3(x0[28], x1[28], x2[28]))), x3[28], x4[28], x5[28]) → COND_6147_0_TEST_GE1(&&(&&(&&(<=(x5[28], x4[28]), >=(x3[28], 0)), >=(2, -(x3[28], 1))), <=(0, -(x3[28], 1))), java.lang.Object(ARRAY(DATA_3(x0[28], x1[28], x2[28]))), x3[28], x4[28], x5[28])
6147_0_TEST_GE(java.lang.Object(ARRAY(DATA_3(x0[30], x1[30], x2[30]))), x3[30], x4[30], x5[30]) → COND_6147_0_TEST_GE2(&&(&&(&&(<=(x5[30], x4[30]), >=(x3[30], 0)), >=(2, -(x3[30], 1))), <=(0, -(x3[30], 1))), java.lang.Object(ARRAY(DATA_3(x0[30], x1[30], x2[30]))), x3[30], x4[30], x5[30])
6147_0_TEST_GE(java.lang.Object(ARRAY(DATA_3(x0[32], x1[32], x2[32]))), x3[32], x4[32], x5[32]) → COND_6147_0_TEST_GE3(&&(&&(&&(<=(x5[32], x4[32]), >=(x3[32], 0)), >=(2, -(x3[32], 1))), <=(0, -(x3[32], 1))), java.lang.Object(ARRAY(DATA_3(x0[32], x1[32], x2[32]))), x3[32], x4[32], x5[32])