Termination proof of /tmp/tmpZ5134q/ListContentTail.jar

Termination of the given JBC could be proven:

0 JBC

↳1 JBC2FIG (⇒)

↳2 JBCTerminationGraph

↳3 FIGtoITRSProof (⇒)

↳4 AND

    ↳5 IDP

        ↳6 IDPNonInfProof (⇒)

        ↳7 AND

            ↳8 IDP

                ↳9 IDependencyGraphProof (⇔)

                ↳10 TRUE

            ↳11 IDP

                ↳12 IDependencyGraphProof (⇔)

                ↳13 TRUE

    ↳14 IDP

        ↳15 IDPNonInfProof (⇒)

        ↳16 IDP

        ↳17 IDPNonInfProof (⇒)

        ↳18 IDP

        ↳19 IDependencyGraphProof (⇔)

        ↳20 IDP

        ↳21 IDPNonInfProof (⇒)

        ↳22 AND

            ↳23 IDP

                ↳24 IDependencyGraphProof (⇔)

                ↳25 TRUE

            ↳26 IDP

                ↳27 IDPNonInfProof (⇒)

                ↳28 IDP

                ↳29 IDependencyGraphProof (⇔)

                ↳30 TRUE

    ↳31 IDP

        ↳32 IDPNonInfProof (⇒)

        ↳33 AND

            ↳34 IDP

                ↳35 IDependencyGraphProof (⇔)

                ↳36 TRUE

            ↳37 IDP

                ↳38 IDependencyGraphProof (⇔)

                ↳39 TRUE

(0) Obligation:

JBC Problem based on JBC Program:
Manifest-Version: 1.0 Created-By: 1.6.0_16 (Sun Microsystems Inc.) Main-Class: ListContentTail

public class ListContentTail{

  public static void main(String[] args) {
    Random.args = args;
    IntList l = IntList.createIntList();

    int m = IntList.nth(Random.random(),l);

    while (m > 0) {

      l = l.next;
      m = IntList.nth(Random.random(),l);
    }
  }
}

class IntList {
  int value;
  IntList next;

  public IntList(int value, IntList next) {
    this.value = value;
    this.next = next;
  }

  public static IntList createIntList() {

    int i = Random.random();
    IntList l = null;

    while (i > 0) {
      l = new IntList(Random.random(), l);
      i--;
    }

    return l;
  }

  public static int nth(int n, IntList l){

    while (n > 1 && l != null) {
      n--;
      l = l.next;
    }

    if (l == null) return 0;
    else           return l.value;
  }





}






public class Random {
  static String[] args;
  static int index = 0;

  public static int random() {
    String string = args[index];
    index++;
    return string.length();
  }
}

(1) JBC2FIG (SOUND transformation)

Constructed FIGraph.

(2) Obligation:

FIGraph based on JBC Program:
ListContentTail.main([Ljava/lang/String;)V: Graph of 276 nodes with 2 SCCs.

IntList.createIntList()LIntList;: Graph of 162 nodes with 1 SCC.

(3) FIGtoITRSProof (SOUND transformation)

Transformed FIGraph SCCs to IDPs. Logs:

Log for SCC 0:

Generated 38 rules for P and 49 rules for R.

Combined rules. Obtained 2 rules for P and 0 rules for R.

Filtered ground terms:

2735_1_createIntList_InvokeMethod(x1, x2, x3, x4, x5) → 2735_1_createIntList_InvokeMethod(x1, x2, x3)
IntList(x1) → IntList
2735_0_random_ArrayAccess(x1, x2, x3) → 2735_0_random_ArrayAccess(x2, x3)
Cond_2830_1_createIntList_InvokeMethod(x1, x2, x3, x4, x5, x6) → Cond_2830_1_createIntList_InvokeMethod(x1, x2, x3, x4)
2830_0_random_IntArithmetic(x1, x2, x3, x4) → 2830_0_random_IntArithmetic(x2, x3)
2830_1_createIntList_InvokeMethod(x1, x2, x3, x4, x5) → 2830_1_createIntList_InvokeMethod(x1, x2, x3)
Cond_2735_1_createIntList_InvokeMethod(x1, x2, x3, x4, x5, x6) → Cond_2735_1_createIntList_InvokeMethod(x1, x2, x3, x4)

Filtered unneeded arguments:

2735_1_createIntList_InvokeMethod(x1, x2, x3) → 2735_1_createIntList_InvokeMethod(x1, x2)
Cond_2735_1_createIntList_InvokeMethod(x1, x2, x3, x4) → Cond_2735_1_createIntList_InvokeMethod(x1, x2, x3)
2830_1_createIntList_InvokeMethod(x1, x2, x3) → 2830_1_createIntList_InvokeMethod(x1, x2)
Cond_2830_1_createIntList_InvokeMethod(x1, x2, x3, x4) → Cond_2830_1_createIntList_InvokeMethod(x1, x2, x3)

Combined rules. Obtained 2 rules for P and 0 rules for R.

Finished conversion. Obtained 2 rules for P and 0 rules for R. System has predefined symbols.

Log for SCC 1:

Generated 73 rules for P and 69 rules for R.

Combined rules. Obtained 9 rules for P and 0 rules for R.

Filtered ground terms:

4683_0_nth_NONNULL(x1, x2, x3) → 4683_0_nth_NONNULL(x2, x3)
4619_0_nth_LE(x1, x2, x3, x4, x5) → 4619_0_nth_LE(x2, x3, x4)
IntList(x1, x2, x3) → IntList(x2, x3)
3247_0_random_ArrayAccess(x1, x2, x3) → 3247_0_random_ArrayAccess(x2, x3)
Cond_4683_1_main_InvokeMethod2(x1, x2, x3, x4) → Cond_4683_1_main_InvokeMethod2(x1, x3, x4)
3429_0_random_IntArithmetic(x1, x2, x3, x4) → 3429_0_random_IntArithmetic(x2, x3)

Filtered duplicate args:

4683_1_main_InvokeMethod(x1, x2, x3) → 4683_1_main_InvokeMethod(x1, x3)
4683_0_nth_NONNULL(x1, x2) → 4683_0_nth_NONNULL(x2)
Cond_4619_1_main_InvokeMethod3(x1, x2, x3, x4) → Cond_4619_1_main_InvokeMethod3(x1, x2, x4)
4619_0_nth_LE(x1, x2, x3) → 4619_0_nth_LE(x2, x3)
4619_1_main_InvokeMethod(x1, x2, x3) → 4619_1_main_InvokeMethod(x1, x3)
Cond_4619_1_main_InvokeMethod2(x1, x2, x3, x4) → Cond_4619_1_main_InvokeMethod2(x1, x2, x4)
Cond_4619_1_main_InvokeMethod1(x1, x2, x3, x4) → Cond_4619_1_main_InvokeMethod1(x1, x2, x4)
Cond_4683_1_main_InvokeMethod2(x1, x2, x3) → Cond_4683_1_main_InvokeMethod2(x1, x3)
Cond_4683_1_main_InvokeMethod1(x1, x2, x3, x4) → Cond_4683_1_main_InvokeMethod1(x1, x2, x4)
Cond_4683_1_main_InvokeMethod(x1, x2, x3, x4) → Cond_4683_1_main_InvokeMethod(x1, x2, x4)
Cond_4619_1_main_InvokeMethod(x1, x2, x3, x4) → Cond_4619_1_main_InvokeMethod(x1, x2, x4)

Combined rules. Obtained 9 rules for P and 0 rules for R.

Finished conversion. Obtained 9 rules for P and 0 rules for R. System has predefined symbols.

Log for SCC 2:

Generated 19 rules for P and 165 rules for R.

Combined rules. Obtained 2 rules for P and 0 rules for R.

Filtered ground terms:

IntList(x1, x2) → IntList(x2)
2655_0_nth_ConstantStackPush(x1, x2, x3, x4) → 2655_0_nth_ConstantStackPush(x2, x3, x4)

Filtered duplicate args:

2655_1_main_InvokeMethod(x1, x2, x3) → 2655_1_main_InvokeMethod(x1, x3)
2655_0_nth_ConstantStackPush(x1, x2, x3) → 2655_0_nth_ConstantStackPush(x2, x3)
Cond_2655_1_main_InvokeMethod1(x1, x2, x3, x4) → Cond_2655_1_main_InvokeMethod1(x1, x2, x4)
Cond_2655_1_main_InvokeMethod(x1, x2, x3, x4) → Cond_2655_1_main_InvokeMethod(x1, x2, x4)

Combined rules. Obtained 2 rules for P and 0 rules for R.

Finished conversion. Obtained 2 rules for P and 0 rules for R. System has predefined symbols.

(4) Complex Obligation (AND)

(5) Obligation:

IDP problem:
The following function symbols are pre-defined:

!=	~	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

The following domains are used:

Boolean, Integer

R is empty.

The integer pair graph contains the following rules and edges:
(0): 2735_1_CREATEINTLIST_INVOKEMETHOD(2735_0_random_ArrayAccess(java.lang.Object(ARRAY(x0[0], x1[0])), x2[0]), x3[0]) → COND_2735_1_CREATEINTLIST_INVOKEMETHOD(x2[0] >= 1 && x2[0] < x0[0], 2735_0_random_ArrayAccess(java.lang.Object(ARRAY(x0[0], x1[0])), x2[0]), x3[0])
(1): COND_2735_1_CREATEINTLIST_INVOKEMETHOD(TRUE, 2735_0_random_ArrayAccess(java.lang.Object(ARRAY(x0[1], x1[1])), x2[1]), x3[1]) → 2830_1_CREATEINTLIST_INVOKEMETHOD(2830_0_random_IntArithmetic(x5[1], x6[1]), x3[1])
(2): 2830_1_CREATEINTLIST_INVOKEMETHOD(2830_0_random_IntArithmetic(java.lang.Object(java.lang.String(x0[2], x1[2])), x2[2]), x4[2]) → COND_2830_1_CREATEINTLIST_INVOKEMETHOD(x4[2] > 0 && x2[2] > 0 && 0 < x4[2] + -1, 2830_0_random_IntArithmetic(java.lang.Object(java.lang.String(x0[2], x1[2])), x2[2]), x4[2])
(3): COND_2830_1_CREATEINTLIST_INVOKEMETHOD(TRUE, 2830_0_random_IntArithmetic(java.lang.Object(java.lang.String(x0[3], x1[3])), x2[3]), x4[3]) → 2735_1_CREATEINTLIST_INVOKEMETHOD(2735_0_random_ArrayAccess(java.lang.Object(ARRAY(x6[3], x7[3])), x8[3]), x4[3] + -1)

(0) -> (1), if ((x2[0] >= 1 && x2[0] < x0[0] →^* TRUE)∧(2735_0_random_ArrayAccess(java.lang.Object(ARRAY(x0[0], x1[0])), x2[0]) →^* 2735_0_random_ArrayAccess(java.lang.Object(ARRAY(x0[1], x1[1])), x2[1]))∧(x3[0] →^* x3[1]))

(1) -> (2), if ((2830_0_random_IntArithmetic(x5[1], x6[1]) →^* 2830_0_random_IntArithmetic(java.lang.Object(java.lang.String(x0[2], x1[2])), x2[2]))∧(x3[1] →^* x4[2]))

(2) -> (3), if ((x4[2] > 0 && x2[2] > 0 && 0 < x4[2] + -1 →^* TRUE)∧(2830_0_random_IntArithmetic(java.lang.Object(java.lang.String(x0[2], x1[2])), x2[2]) →^* 2830_0_random_IntArithmetic(java.lang.Object(java.lang.String(x0[3], x1[3])), x2[3]))∧(x4[2] →^* x4[3]))

(3) -> (0), if ((2735_0_random_ArrayAccess(java.lang.Object(ARRAY(x6[3], x7[3])), x8[3]) →^* 2735_0_random_ArrayAccess(java.lang.Object(ARRAY(x0[0], x1[0])), x2[0]))∧(x4[3] + -1 →^* x3[0]))

The set Q is empty.

(6) IDPNonInfProof (SOUND transformation)

The constraints were generated the following way:
The DP Problem is simplified using the Induction Calculus [NONINF] with the following steps:
Note that final constraints are written in bold face.

For Pair 2735_1_CREATEINTLIST_INVOKEMETHOD(2735_0_random_ArrayAccess(java.lang.Object(ARRAY(x0, x1)), x2), x3) → COND_2735_1_CREATEINTLIST_INVOKEMETHOD(&&(>=(x2, 1), <(x2, x0)), 2735_0_random_ArrayAccess(java.lang.Object(ARRAY(x0, x1)), x2), x3) the following chains were created:

We consider the chain 2735_1_CREATEINTLIST_INVOKEMETHOD(2735_0_random_ArrayAccess(java.lang.Object(ARRAY(x0[0], x1[0])), x2[0]), x3[0]) → COND_2735_1_CREATEINTLIST_INVOKEMETHOD(&&(>=(x2[0], 1), <(x2[0], x0[0])), 2735_0_random_ArrayAccess(java.lang.Object(ARRAY(x0[0], x1[0])), x2[0]), x3[0]), COND_2735_1_CREATEINTLIST_INVOKEMETHOD(TRUE, 2735_0_random_ArrayAccess(java.lang.Object(ARRAY(x0[1], x1[1])), x2[1]), x3[1]) → 2830_1_CREATEINTLIST_INVOKEMETHOD(2830_0_random_IntArithmetic(x5[1], x6[1]), x3[1]) which results in the following constraint:
(1)    (&&(>=(x2[0], 1), <(x2[0], x0[0]))=TRUE∧2735_0_random_ArrayAccess(java.lang.Object(ARRAY(x0[0], x1[0])), x2[0])=2735_0_random_ArrayAccess(java.lang.Object(ARRAY(x0[1], x1[1])), x2[1])∧x3[0]=x3[1] ⇒ 2735_1_CREATEINTLIST_INVOKEMETHOD(2735_0_random_ArrayAccess(java.lang.Object(ARRAY(x0[0], x1[0])), x2[0]), x3[0])≥NonInfC∧2735_1_CREATEINTLIST_INVOKEMETHOD(2735_0_random_ArrayAccess(java.lang.Object(ARRAY(x0[0], x1[0])), x2[0]), x3[0])≥COND_2735_1_CREATEINTLIST_INVOKEMETHOD(&&(>=(x2[0], 1), <(x2[0], x0[0])), 2735_0_random_ArrayAccess(java.lang.Object(ARRAY(x0[0], x1[0])), x2[0]), x3[0])∧(U^Increasing(COND_2735_1_CREATEINTLIST_INVOKEMETHOD(&&(>=(x2[0], 1), <(x2[0], x0[0])), 2735_0_random_ArrayAccess(java.lang.Object(ARRAY(x0[0], x1[0])), x2[0]), x3[0])), ≥))

We simplified constraint (1) using rules (I), (II), (IV), (IDP_BOOLEAN) which results in the following new constraint:
(2)    (>=(x2[0], 1)=TRUE∧<(x2[0], x0[0])=TRUE ⇒ 2735_1_CREATEINTLIST_INVOKEMETHOD(2735_0_random_ArrayAccess(java.lang.Object(ARRAY(x0[0], x1[0])), x2[0]), x3[0])≥NonInfC∧2735_1_CREATEINTLIST_INVOKEMETHOD(2735_0_random_ArrayAccess(java.lang.Object(ARRAY(x0[0], x1[0])), x2[0]), x3[0])≥COND_2735_1_CREATEINTLIST_INVOKEMETHOD(&&(>=(x2[0], 1), <(x2[0], x0[0])), 2735_0_random_ArrayAccess(java.lang.Object(ARRAY(x0[0], x1[0])), x2[0]), x3[0])∧(U^Increasing(COND_2735_1_CREATEINTLIST_INVOKEMETHOD(&&(>=(x2[0], 1), <(x2[0], x0[0])), 2735_0_random_ArrayAccess(java.lang.Object(ARRAY(x0[0], x1[0])), x2[0]), x3[0])), ≥))

We simplified constraint (2) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(3)    (x2[0] + [-1] ≥ 0∧x0[0] + [-1] + [-1]x2[0] ≥ 0 ⇒ (U^Increasing(COND_2735_1_CREATEINTLIST_INVOKEMETHOD(&&(>=(x2[0], 1), <(x2[0], x0[0])), 2735_0_random_ArrayAccess(java.lang.Object(ARRAY(x0[0], x1[0])), x2[0]), x3[0])), ≥)∧[(-1)Bound*bni_22] + [bni_22]x3[0] ≥ 0∧[1 + (-1)bso_23] ≥ 0)

We simplified constraint (3) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(4)    (x2[0] + [-1] ≥ 0∧x0[0] + [-1] + [-1]x2[0] ≥ 0 ⇒ (U^Increasing(COND_2735_1_CREATEINTLIST_INVOKEMETHOD(&&(>=(x2[0], 1), <(x2[0], x0[0])), 2735_0_random_ArrayAccess(java.lang.Object(ARRAY(x0[0], x1[0])), x2[0]), x3[0])), ≥)∧[(-1)Bound*bni_22] + [bni_22]x3[0] ≥ 0∧[1 + (-1)bso_23] ≥ 0)

We simplified constraint (4) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(5)    (x2[0] + [-1] ≥ 0∧x0[0] + [-1] + [-1]x2[0] ≥ 0 ⇒ (U^Increasing(COND_2735_1_CREATEINTLIST_INVOKEMETHOD(&&(>=(x2[0], 1), <(x2[0], x0[0])), 2735_0_random_ArrayAccess(java.lang.Object(ARRAY(x0[0], x1[0])), x2[0]), x3[0])), ≥)∧[(-1)Bound*bni_22] + [bni_22]x3[0] ≥ 0∧[1 + (-1)bso_23] ≥ 0)

We simplified constraint (5) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:
(6)    (x2[0] + [-1] ≥ 0∧x0[0] + [-1] + [-1]x2[0] ≥ 0 ⇒ (U^Increasing(COND_2735_1_CREATEINTLIST_INVOKEMETHOD(&&(>=(x2[0], 1), <(x2[0], x0[0])), 2735_0_random_ArrayAccess(java.lang.Object(ARRAY(x0[0], x1[0])), x2[0]), x3[0])), ≥)∧[bni_22] = 0∧0 = 0∧[(-1)Bound*bni_22] ≥ 0∧0 = 0∧0 = 0∧[1 + (-1)bso_23] ≥ 0)

We simplified constraint (6) using rule (IDP_SMT_SPLIT) which results in the following new constraint:
(7)    (x2[0] ≥ 0∧x0[0] + [-2] + [-1]x2[0] ≥ 0 ⇒ (U^Increasing(COND_2735_1_CREATEINTLIST_INVOKEMETHOD(&&(>=(x2[0], 1), <(x2[0], x0[0])), 2735_0_random_ArrayAccess(java.lang.Object(ARRAY(x0[0], x1[0])), x2[0]), x3[0])), ≥)∧[bni_22] = 0∧0 = 0∧[(-1)Bound*bni_22] ≥ 0∧0 = 0∧0 = 0∧[1 + (-1)bso_23] ≥ 0)

We simplified constraint (7) using rule (IDP_SMT_SPLIT) which results in the following new constraint:
(8)    (x2[0] ≥ 0∧x0[0] ≥ 0 ⇒ (U^Increasing(COND_2735_1_CREATEINTLIST_INVOKEMETHOD(&&(>=(x2[0], 1), <(x2[0], x0[0])), 2735_0_random_ArrayAccess(java.lang.Object(ARRAY(x0[0], x1[0])), x2[0]), x3[0])), ≥)∧[bni_22] = 0∧0 = 0∧[(-1)Bound*bni_22] ≥ 0∧0 = 0∧0 = 0∧[1 + (-1)bso_23] ≥ 0)

For Pair COND_2735_1_CREATEINTLIST_INVOKEMETHOD(TRUE, 2735_0_random_ArrayAccess(java.lang.Object(ARRAY(x0, x1)), x2), x3) → 2830_1_CREATEINTLIST_INVOKEMETHOD(2830_0_random_IntArithmetic(x5, x6), x3) the following chains were created:

We consider the chain COND_2735_1_CREATEINTLIST_INVOKEMETHOD(TRUE, 2735_0_random_ArrayAccess(java.lang.Object(ARRAY(x0[1], x1[1])), x2[1]), x3[1]) → 2830_1_CREATEINTLIST_INVOKEMETHOD(2830_0_random_IntArithmetic(x5[1], x6[1]), x3[1]) which results in the following constraint:
(9)    (COND_2735_1_CREATEINTLIST_INVOKEMETHOD(TRUE, 2735_0_random_ArrayAccess(java.lang.Object(ARRAY(x0[1], x1[1])), x2[1]), x3[1])≥NonInfC∧COND_2735_1_CREATEINTLIST_INVOKEMETHOD(TRUE, 2735_0_random_ArrayAccess(java.lang.Object(ARRAY(x0[1], x1[1])), x2[1]), x3[1])≥2830_1_CREATEINTLIST_INVOKEMETHOD(2830_0_random_IntArithmetic(x5[1], x6[1]), x3[1])∧(U^Increasing(2830_1_CREATEINTLIST_INVOKEMETHOD(2830_0_random_IntArithmetic(x5[1], x6[1]), x3[1])), ≥))

We simplified constraint (9) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(10)    ((U^Increasing(2830_1_CREATEINTLIST_INVOKEMETHOD(2830_0_random_IntArithmetic(x5[1], x6[1]), x3[1])), ≥)∧[(-1)bso_25] ≥ 0)

We simplified constraint (10) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(11)    ((U^Increasing(2830_1_CREATEINTLIST_INVOKEMETHOD(2830_0_random_IntArithmetic(x5[1], x6[1]), x3[1])), ≥)∧[(-1)bso_25] ≥ 0)

We simplified constraint (11) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(12)    ((U^Increasing(2830_1_CREATEINTLIST_INVOKEMETHOD(2830_0_random_IntArithmetic(x5[1], x6[1]), x3[1])), ≥)∧[(-1)bso_25] ≥ 0)

We simplified constraint (12) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:
(13)    ((U^Increasing(2830_1_CREATEINTLIST_INVOKEMETHOD(2830_0_random_IntArithmetic(x5[1], x6[1]), x3[1])), ≥)∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧[(-1)bso_25] ≥ 0)

For Pair 2830_1_CREATEINTLIST_INVOKEMETHOD(2830_0_random_IntArithmetic(java.lang.Object(java.lang.String(x0, x1)), x2), x4) → COND_2830_1_CREATEINTLIST_INVOKEMETHOD(&&(&&(>(x4, 0), >(x2, 0)), <(0, +(x4, -1))), 2830_0_random_IntArithmetic(java.lang.Object(java.lang.String(x0, x1)), x2), x4) the following chains were created:

We consider the chain 2830_1_CREATEINTLIST_INVOKEMETHOD(2830_0_random_IntArithmetic(java.lang.Object(java.lang.String(x0[2], x1[2])), x2[2]), x4[2]) → COND_2830_1_CREATEINTLIST_INVOKEMETHOD(&&(&&(>(x4[2], 0), >(x2[2], 0)), <(0, +(x4[2], -1))), 2830_0_random_IntArithmetic(java.lang.Object(java.lang.String(x0[2], x1[2])), x2[2]), x4[2]), COND_2830_1_CREATEINTLIST_INVOKEMETHOD(TRUE, 2830_0_random_IntArithmetic(java.lang.Object(java.lang.String(x0[3], x1[3])), x2[3]), x4[3]) → 2735_1_CREATEINTLIST_INVOKEMETHOD(2735_0_random_ArrayAccess(java.lang.Object(ARRAY(x6[3], x7[3])), x8[3]), +(x4[3], -1)) which results in the following constraint:
(14)    (&&(&&(>(x4[2], 0), >(x2[2], 0)), <(0, +(x4[2], -1)))=TRUE∧2830_0_random_IntArithmetic(java.lang.Object(java.lang.String(x0[2], x1[2])), x2[2])=2830_0_random_IntArithmetic(java.lang.Object(java.lang.String(x0[3], x1[3])), x2[3])∧x4[2]=x4[3] ⇒ 2830_1_CREATEINTLIST_INVOKEMETHOD(2830_0_random_IntArithmetic(java.lang.Object(java.lang.String(x0[2], x1[2])), x2[2]), x4[2])≥NonInfC∧2830_1_CREATEINTLIST_INVOKEMETHOD(2830_0_random_IntArithmetic(java.lang.Object(java.lang.String(x0[2], x1[2])), x2[2]), x4[2])≥COND_2830_1_CREATEINTLIST_INVOKEMETHOD(&&(&&(>(x4[2], 0), >(x2[2], 0)), <(0, +(x4[2], -1))), 2830_0_random_IntArithmetic(java.lang.Object(java.lang.String(x0[2], x1[2])), x2[2]), x4[2])∧(U^Increasing(COND_2830_1_CREATEINTLIST_INVOKEMETHOD(&&(&&(>(x4[2], 0), >(x2[2], 0)), <(0, +(x4[2], -1))), 2830_0_random_IntArithmetic(java.lang.Object(java.lang.String(x0[2], x1[2])), x2[2]), x4[2])), ≥))

We simplified constraint (14) using rules (I), (II), (IV), (IDP_BOOLEAN) which results in the following new constraint:
(15)    (<(0, +(x4[2], -1))=TRUE∧>(x4[2], 0)=TRUE∧>(x2[2], 0)=TRUE ⇒ 2830_1_CREATEINTLIST_INVOKEMETHOD(2830_0_random_IntArithmetic(java.lang.Object(java.lang.String(x0[2], x1[2])), x2[2]), x4[2])≥NonInfC∧2830_1_CREATEINTLIST_INVOKEMETHOD(2830_0_random_IntArithmetic(java.lang.Object(java.lang.String(x0[2], x1[2])), x2[2]), x4[2])≥COND_2830_1_CREATEINTLIST_INVOKEMETHOD(&&(&&(>(x4[2], 0), >(x2[2], 0)), <(0, +(x4[2], -1))), 2830_0_random_IntArithmetic(java.lang.Object(java.lang.String(x0[2], x1[2])), x2[2]), x4[2])∧(U^Increasing(COND_2830_1_CREATEINTLIST_INVOKEMETHOD(&&(&&(>(x4[2], 0), >(x2[2], 0)), <(0, +(x4[2], -1))), 2830_0_random_IntArithmetic(java.lang.Object(java.lang.String(x0[2], x1[2])), x2[2]), x4[2])), ≥))

We simplified constraint (15) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(16)    (x4[2] + [-2] ≥ 0∧x4[2] + [-1] ≥ 0∧x2[2] + [-1] ≥ 0 ⇒ (U^Increasing(COND_2830_1_CREATEINTLIST_INVOKEMETHOD(&&(&&(>(x4[2], 0), >(x2[2], 0)), <(0, +(x4[2], -1))), 2830_0_random_IntArithmetic(java.lang.Object(java.lang.String(x0[2], x1[2])), x2[2]), x4[2])), ≥)∧[(-1)bni_26 + (-1)Bound*bni_26] + [bni_26]x4[2] ≥ 0∧[(-1)bso_27] ≥ 0)

We simplified constraint (16) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(17)    (x4[2] + [-2] ≥ 0∧x4[2] + [-1] ≥ 0∧x2[2] + [-1] ≥ 0 ⇒ (U^Increasing(COND_2830_1_CREATEINTLIST_INVOKEMETHOD(&&(&&(>(x4[2], 0), >(x2[2], 0)), <(0, +(x4[2], -1))), 2830_0_random_IntArithmetic(java.lang.Object(java.lang.String(x0[2], x1[2])), x2[2]), x4[2])), ≥)∧[(-1)bni_26 + (-1)Bound*bni_26] + [bni_26]x4[2] ≥ 0∧[(-1)bso_27] ≥ 0)

We simplified constraint (17) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(18)    (x4[2] + [-2] ≥ 0∧x4[2] + [-1] ≥ 0∧x2[2] + [-1] ≥ 0 ⇒ (U^Increasing(COND_2830_1_CREATEINTLIST_INVOKEMETHOD(&&(&&(>(x4[2], 0), >(x2[2], 0)), <(0, +(x4[2], -1))), 2830_0_random_IntArithmetic(java.lang.Object(java.lang.String(x0[2], x1[2])), x2[2]), x4[2])), ≥)∧[(-1)bni_26 + (-1)Bound*bni_26] + [bni_26]x4[2] ≥ 0∧[(-1)bso_27] ≥ 0)

We simplified constraint (18) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:
(19)    (x4[2] + [-2] ≥ 0∧x4[2] + [-1] ≥ 0∧x2[2] + [-1] ≥ 0 ⇒ (U^Increasing(COND_2830_1_CREATEINTLIST_INVOKEMETHOD(&&(&&(>(x4[2], 0), >(x2[2], 0)), <(0, +(x4[2], -1))), 2830_0_random_IntArithmetic(java.lang.Object(java.lang.String(x0[2], x1[2])), x2[2]), x4[2])), ≥)∧0 = 0∧0 = 0∧[(-1)bni_26 + (-1)Bound*bni_26] + [bni_26]x4[2] ≥ 0∧0 = 0∧0 = 0∧[(-1)bso_27] ≥ 0)

We simplified constraint (19) using rule (IDP_SMT_SPLIT) which results in the following new constraint:
(20)    (x4[2] ≥ 0∧[1] + x4[2] ≥ 0∧x2[2] + [-1] ≥ 0 ⇒ (U^Increasing(COND_2830_1_CREATEINTLIST_INVOKEMETHOD(&&(&&(>(x4[2], 0), >(x2[2], 0)), <(0, +(x4[2], -1))), 2830_0_random_IntArithmetic(java.lang.Object(java.lang.String(x0[2], x1[2])), x2[2]), x4[2])), ≥)∧0 = 0∧0 = 0∧[bni_26 + (-1)Bound*bni_26] + [bni_26]x4[2] ≥ 0∧0 = 0∧0 = 0∧[(-1)bso_27] ≥ 0)

We simplified constraint (20) using rule (IDP_SMT_SPLIT) which results in the following new constraint:
(21)    (x4[2] ≥ 0∧[1] + x4[2] ≥ 0∧x2[2] ≥ 0 ⇒ (U^Increasing(COND_2830_1_CREATEINTLIST_INVOKEMETHOD(&&(&&(>(x4[2], 0), >(x2[2], 0)), <(0, +(x4[2], -1))), 2830_0_random_IntArithmetic(java.lang.Object(java.lang.String(x0[2], x1[2])), x2[2]), x4[2])), ≥)∧0 = 0∧0 = 0∧[bni_26 + (-1)Bound*bni_26] + [bni_26]x4[2] ≥ 0∧0 = 0∧0 = 0∧[(-1)bso_27] ≥ 0)

For Pair COND_2830_1_CREATEINTLIST_INVOKEMETHOD(TRUE, 2830_0_random_IntArithmetic(java.lang.Object(java.lang.String(x0, x1)), x2), x4) → 2735_1_CREATEINTLIST_INVOKEMETHOD(2735_0_random_ArrayAccess(java.lang.Object(ARRAY(x6, x7)), x8), +(x4, -1)) the following chains were created:

We consider the chain COND_2830_1_CREATEINTLIST_INVOKEMETHOD(TRUE, 2830_0_random_IntArithmetic(java.lang.Object(java.lang.String(x0[3], x1[3])), x2[3]), x4[3]) → 2735_1_CREATEINTLIST_INVOKEMETHOD(2735_0_random_ArrayAccess(java.lang.Object(ARRAY(x6[3], x7[3])), x8[3]), +(x4[3], -1)) which results in the following constraint:
(22)    (COND_2830_1_CREATEINTLIST_INVOKEMETHOD(TRUE, 2830_0_random_IntArithmetic(java.lang.Object(java.lang.String(x0[3], x1[3])), x2[3]), x4[3])≥NonInfC∧COND_2830_1_CREATEINTLIST_INVOKEMETHOD(TRUE, 2830_0_random_IntArithmetic(java.lang.Object(java.lang.String(x0[3], x1[3])), x2[3]), x4[3])≥2735_1_CREATEINTLIST_INVOKEMETHOD(2735_0_random_ArrayAccess(java.lang.Object(ARRAY(x6[3], x7[3])), x8[3]), +(x4[3], -1))∧(U^Increasing(2735_1_CREATEINTLIST_INVOKEMETHOD(2735_0_random_ArrayAccess(java.lang.Object(ARRAY(x6[3], x7[3])), x8[3]), +(x4[3], -1))), ≥))

We simplified constraint (22) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(23)    ((U^Increasing(2735_1_CREATEINTLIST_INVOKEMETHOD(2735_0_random_ArrayAccess(java.lang.Object(ARRAY(x6[3], x7[3])), x8[3]), +(x4[3], -1))), ≥)∧[(-1)bso_29] ≥ 0)

We simplified constraint (23) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(24)    ((U^Increasing(2735_1_CREATEINTLIST_INVOKEMETHOD(2735_0_random_ArrayAccess(java.lang.Object(ARRAY(x6[3], x7[3])), x8[3]), +(x4[3], -1))), ≥)∧[(-1)bso_29] ≥ 0)

We simplified constraint (24) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(25)    ((U^Increasing(2735_1_CREATEINTLIST_INVOKEMETHOD(2735_0_random_ArrayAccess(java.lang.Object(ARRAY(x6[3], x7[3])), x8[3]), +(x4[3], -1))), ≥)∧[(-1)bso_29] ≥ 0)

We simplified constraint (25) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:
(26)    ((U^Increasing(2735_1_CREATEINTLIST_INVOKEMETHOD(2735_0_random_ArrayAccess(java.lang.Object(ARRAY(x6[3], x7[3])), x8[3]), +(x4[3], -1))), ≥)∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧[(-1)bso_29] ≥ 0)

To summarize, we get the following constraints P_≥ for the following pairs.

2735_1_CREATEINTLIST_INVOKEMETHOD(2735_0_random_ArrayAccess(java.lang.Object(ARRAY(x0, x1)), x2), x3) → COND_2735_1_CREATEINTLIST_INVOKEMETHOD(&&(>=(x2, 1), <(x2, x0)), 2735_0_random_ArrayAccess(java.lang.Object(ARRAY(x0, x1)), x2), x3)
- (x2[0] ≥ 0∧x0[0] ≥ 0 ⇒ (U^Increasing(COND_2735_1_CREATEINTLIST_INVOKEMETHOD(&&(>=(x2[0], 1), <(x2[0], x0[0])), 2735_0_random_ArrayAccess(java.lang.Object(ARRAY(x0[0], x1[0])), x2[0]), x3[0])), ≥)∧[bni_22] = 0∧0 = 0∧[(-1)Bound*bni_22] ≥ 0∧0 = 0∧0 = 0∧[1 + (-1)bso_23] ≥ 0)
COND_2735_1_CREATEINTLIST_INVOKEMETHOD(TRUE, 2735_0_random_ArrayAccess(java.lang.Object(ARRAY(x0, x1)), x2), x3) → 2830_1_CREATEINTLIST_INVOKEMETHOD(2830_0_random_IntArithmetic(x5, x6), x3)
- ((U^Increasing(2830_1_CREATEINTLIST_INVOKEMETHOD(2830_0_random_IntArithmetic(x5[1], x6[1]), x3[1])), ≥)∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧[(-1)bso_25] ≥ 0)
2830_1_CREATEINTLIST_INVOKEMETHOD(2830_0_random_IntArithmetic(java.lang.Object(java.lang.String(x0, x1)), x2), x4) → COND_2830_1_CREATEINTLIST_INVOKEMETHOD(&&(&&(>(x4, 0), >(x2, 0)), <(0, +(x4, -1))), 2830_0_random_IntArithmetic(java.lang.Object(java.lang.String(x0, x1)), x2), x4)
- (x4[2] ≥ 0∧[1] + x4[2] ≥ 0∧x2[2] ≥ 0 ⇒ (U^Increasing(COND_2830_1_CREATEINTLIST_INVOKEMETHOD(&&(&&(>(x4[2], 0), >(x2[2], 0)), <(0, +(x4[2], -1))), 2830_0_random_IntArithmetic(java.lang.Object(java.lang.String(x0[2], x1[2])), x2[2]), x4[2])), ≥)∧0 = 0∧0 = 0∧[bni_26 + (-1)Bound*bni_26] + [bni_26]x4[2] ≥ 0∧0 = 0∧0 = 0∧[(-1)bso_27] ≥ 0)
COND_2830_1_CREATEINTLIST_INVOKEMETHOD(TRUE, 2830_0_random_IntArithmetic(java.lang.Object(java.lang.String(x0, x1)), x2), x4) → 2735_1_CREATEINTLIST_INVOKEMETHOD(2735_0_random_ArrayAccess(java.lang.Object(ARRAY(x6, x7)), x8), +(x4, -1))
- ((U^Increasing(2735_1_CREATEINTLIST_INVOKEMETHOD(2735_0_random_ArrayAccess(java.lang.Object(ARRAY(x6[3], x7[3])), x8[3]), +(x4[3], -1))), ≥)∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧[(-1)bso_29] ≥ 0)

The constraints for P_> respective P_bound are constructed from P_≥ where we just replace every occurence of "t ≥ s" in P_≥ by "t > s" respective "t ≥ c". Here c stands for the fresh constant used for P_bound.
Using the following integer polynomial ordering the resulting constraints can be solved
Polynomial interpretation over integers[POLO]:

POL(TRUE) = 0
POL(FALSE) = 0
POL(2735_1_CREATEINTLIST_INVOKEMETHOD(x₁, x₂)) = [1] + x₂ + [-1]x₁
POL(2735_0_random_ArrayAccess(x₁, x₂)) = [-1]x₁
POL(java.lang.Object(x₁)) = x₁
POL(ARRAY(x₁, x₂)) = [-1]
POL(COND_2735_1_CREATEINTLIST_INVOKEMETHOD(x₁, x₂, x₃)) = x₃ + [-1]x₂
POL(&&(x₁, x₂)) = 0
POL(>=(x₁, x₂)) = [-1]
POL(1) = [1]
POL(<(x₁, x₂)) = [-1]
POL(2830_1_CREATEINTLIST_INVOKEMETHOD(x₁, x₂)) = [-1] + [-1]x₁ + x₂
POL(2830_0_random_IntArithmetic(x₁, x₂)) = 0
POL(java.lang.String(x₁, x₂)) = [-1] + [2]x₂ + [-1]x₁
POL(COND_2830_1_CREATEINTLIST_INVOKEMETHOD(x₁, x₂, x₃)) = [-1] + x₃ + [-1]x₂
POL(>(x₁, x₂)) = [-1]
POL(0) = 0
POL(+(x₁, x₂)) = x₁ + x₂
POL(-1) = [-1]

The following pairs are in P_>:

2735_1_CREATEINTLIST_INVOKEMETHOD(2735_0_random_ArrayAccess(java.lang.Object(ARRAY(x0[0], x1[0])), x2[0]), x3[0]) → COND_2735_1_CREATEINTLIST_INVOKEMETHOD(&&(>=(x2[0], 1), <(x2[0], x0[0])), 2735_0_random_ArrayAccess(java.lang.Object(ARRAY(x0[0], x1[0])), x2[0]), x3[0])

The following pairs are in P_bound:

2830_1_CREATEINTLIST_INVOKEMETHOD(2830_0_random_IntArithmetic(java.lang.Object(java.lang.String(x0[2], x1[2])), x2[2]), x4[2]) → COND_2830_1_CREATEINTLIST_INVOKEMETHOD(&&(&&(>(x4[2], 0), >(x2[2], 0)), <(0, +(x4[2], -1))), 2830_0_random_IntArithmetic(java.lang.Object(java.lang.String(x0[2], x1[2])), x2[2]), x4[2])

The following pairs are in P_≥:

COND_2735_1_CREATEINTLIST_INVOKEMETHOD(TRUE, 2735_0_random_ArrayAccess(java.lang.Object(ARRAY(x0[1], x1[1])), x2[1]), x3[1]) → 2830_1_CREATEINTLIST_INVOKEMETHOD(2830_0_random_IntArithmetic(x5[1], x6[1]), x3[1])
2830_1_CREATEINTLIST_INVOKEMETHOD(2830_0_random_IntArithmetic(java.lang.Object(java.lang.String(x0[2], x1[2])), x2[2]), x4[2]) → COND_2830_1_CREATEINTLIST_INVOKEMETHOD(&&(&&(>(x4[2], 0), >(x2[2], 0)), <(0, +(x4[2], -1))), 2830_0_random_IntArithmetic(java.lang.Object(java.lang.String(x0[2], x1[2])), x2[2]), x4[2])
COND_2830_1_CREATEINTLIST_INVOKEMETHOD(TRUE, 2830_0_random_IntArithmetic(java.lang.Object(java.lang.String(x0[3], x1[3])), x2[3]), x4[3]) → 2735_1_CREATEINTLIST_INVOKEMETHOD(2735_0_random_ArrayAccess(java.lang.Object(ARRAY(x6[3], x7[3])), x8[3]), +(x4[3], -1))

There are no usable rules.

(7) Complex Obligation (AND)

(8) Obligation:

IDP problem:
The following function symbols are pre-defined:

!=	~	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

The following domains are used:

Boolean, Integer

R is empty.

The integer pair graph contains the following rules and edges:
(1): COND_2735_1_CREATEINTLIST_INVOKEMETHOD(TRUE, 2735_0_random_ArrayAccess(java.lang.Object(ARRAY(x0[1], x1[1])), x2[1]), x3[1]) → 2830_1_CREATEINTLIST_INVOKEMETHOD(2830_0_random_IntArithmetic(x5[1], x6[1]), x3[1])
(2): 2830_1_CREATEINTLIST_INVOKEMETHOD(2830_0_random_IntArithmetic(java.lang.Object(java.lang.String(x0[2], x1[2])), x2[2]), x4[2]) → COND_2830_1_CREATEINTLIST_INVOKEMETHOD(x4[2] > 0 && x2[2] > 0 && 0 < x4[2] + -1, 2830_0_random_IntArithmetic(java.lang.Object(java.lang.String(x0[2], x1[2])), x2[2]), x4[2])
(3): COND_2830_1_CREATEINTLIST_INVOKEMETHOD(TRUE, 2830_0_random_IntArithmetic(java.lang.Object(java.lang.String(x0[3], x1[3])), x2[3]), x4[3]) → 2735_1_CREATEINTLIST_INVOKEMETHOD(2735_0_random_ArrayAccess(java.lang.Object(ARRAY(x6[3], x7[3])), x8[3]), x4[3] + -1)

(1) -> (2), if ((2830_0_random_IntArithmetic(x5[1], x6[1]) →^* 2830_0_random_IntArithmetic(java.lang.Object(java.lang.String(x0[2], x1[2])), x2[2]))∧(x3[1] →^* x4[2]))

The set Q is empty.

(9) IDependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 0 SCCs with 3 less nodes.

(10) TRUE

(11) Obligation:

IDP problem:
The following function symbols are pre-defined:

!=	~	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

The following domains are used:

Boolean, Integer

R is empty.

The integer pair graph contains the following rules and edges:
(0): 2735_1_CREATEINTLIST_INVOKEMETHOD(2735_0_random_ArrayAccess(java.lang.Object(ARRAY(x0[0], x1[0])), x2[0]), x3[0]) → COND_2735_1_CREATEINTLIST_INVOKEMETHOD(x2[0] >= 1 && x2[0] < x0[0], 2735_0_random_ArrayAccess(java.lang.Object(ARRAY(x0[0], x1[0])), x2[0]), x3[0])
(1): COND_2735_1_CREATEINTLIST_INVOKEMETHOD(TRUE, 2735_0_random_ArrayAccess(java.lang.Object(ARRAY(x0[1], x1[1])), x2[1]), x3[1]) → 2830_1_CREATEINTLIST_INVOKEMETHOD(2830_0_random_IntArithmetic(x5[1], x6[1]), x3[1])
(3): COND_2830_1_CREATEINTLIST_INVOKEMETHOD(TRUE, 2830_0_random_IntArithmetic(java.lang.Object(java.lang.String(x0[3], x1[3])), x2[3]), x4[3]) → 2735_1_CREATEINTLIST_INVOKEMETHOD(2735_0_random_ArrayAccess(java.lang.Object(ARRAY(x6[3], x7[3])), x8[3]), x4[3] + -1)

(3) -> (0), if ((2735_0_random_ArrayAccess(java.lang.Object(ARRAY(x6[3], x7[3])), x8[3]) →^* 2735_0_random_ArrayAccess(java.lang.Object(ARRAY(x0[0], x1[0])), x2[0]))∧(x4[3] + -1 →^* x3[0]))

The set Q is empty.

(12) IDependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 0 SCCs with 3 less nodes.

(13) TRUE

(14) Obligation:

IDP problem:
The following function symbols are pre-defined:

!=	~	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

The following domains are used:

Boolean, Integer

R is empty.

The integer pair graph contains the following rules and edges:
(0): 3247_1_MAIN_INVOKEMETHOD(3247_0_random_ArrayAccess(java.lang.Object(ARRAY(x0[0], x1[0])), x2[0]), x3[0]) → COND_3247_1_MAIN_INVOKEMETHOD(x2[0] >= 2 && x2[0] < x0[0], 3247_0_random_ArrayAccess(java.lang.Object(ARRAY(x0[0], x1[0])), x2[0]), x3[0])
(1): COND_3247_1_MAIN_INVOKEMETHOD(TRUE, 3247_0_random_ArrayAccess(java.lang.Object(ARRAY(x0[1], x1[1])), x2[1]), x3[1]) → 3429_1_MAIN_INVOKEMETHOD(3429_0_random_IntArithmetic(x4[1], x5[1]), x3[1])
(2): 3429_1_MAIN_INVOKEMETHOD(3429_0_random_IntArithmetic(java.lang.Object(java.lang.String(x0[2], x1[2])), x2[2]), x4[2]) → COND_3429_1_MAIN_INVOKEMETHOD(x2[2] > 0, 3429_0_random_IntArithmetic(java.lang.Object(java.lang.String(x0[2], x1[2])), x2[2]), x4[2])
(3): COND_3429_1_MAIN_INVOKEMETHOD(TRUE, 3429_0_random_IntArithmetic(java.lang.Object(java.lang.String(x0[3], x1[3])), x2[3]), x4[3]) → 4619_1_MAIN_INVOKEMETHOD(4619_0_nth_LE(x4[3], x1[3]), x4[3])
(4): 4619_1_MAIN_INVOKEMETHOD(4619_0_nth_LE(x1[4], x0[4]), x3[4]) → COND_4619_1_MAIN_INVOKEMETHOD(x0[4] <= 1, 4619_0_nth_LE(x1[4], x0[4]), x3[4])
(5): COND_4619_1_MAIN_INVOKEMETHOD(TRUE, 4619_0_nth_LE(x1[5], x0[5]), x3[5]) → 4683_1_MAIN_INVOKEMETHOD(4683_0_nth_NONNULL(x1[5]), x3[5])
(6): 4683_1_MAIN_INVOKEMETHOD(4683_0_nth_NONNULL(java.lang.Object(IntList(x0[6], x1[6]))), java.lang.Object(IntList(x2[6], x3[6]))) → COND_4683_1_MAIN_INVOKEMETHOD(x1[6] > 0, 4683_0_nth_NONNULL(java.lang.Object(IntList(x0[6], x1[6]))), java.lang.Object(IntList(x2[6], x3[6])))
(7): COND_4683_1_MAIN_INVOKEMETHOD(TRUE, 4683_0_nth_NONNULL(java.lang.Object(IntList(x0[7], x1[7]))), java.lang.Object(IntList(x2[7], x3[7]))) → 3247_1_MAIN_INVOKEMETHOD(3247_0_random_ArrayAccess(java.lang.Object(ARRAY(x4[7], x5[7])), x6[7]), x2[7])
(8): 4683_1_MAIN_INVOKEMETHOD(4683_0_nth_NONNULL(java.lang.Object(IntList(x0[8], x1[8]))), java.lang.Object(IntList(x0[8], x1[8]))) → COND_4683_1_MAIN_INVOKEMETHOD1(x1[8] > 0, 4683_0_nth_NONNULL(java.lang.Object(IntList(x0[8], x1[8]))), java.lang.Object(IntList(x0[8], x1[8])))
(9): COND_4683_1_MAIN_INVOKEMETHOD1(TRUE, 4683_0_nth_NONNULL(java.lang.Object(IntList(x0[9], x1[9]))), java.lang.Object(IntList(x0[9], x1[9]))) → 3247_1_MAIN_INVOKEMETHOD(3247_0_random_ArrayAccess(java.lang.Object(ARRAY(x2[9], x3[9])), x4[9]), x0[9])
(10): 4683_1_MAIN_INVOKEMETHOD(4683_0_nth_NONNULL(NULL), java.lang.Object(IntList(x0[10], x1[10]))) → COND_4683_1_MAIN_INVOKEMETHOD2(0 > 0, 4683_0_nth_NONNULL(NULL), java.lang.Object(IntList(x0[10], x1[10])))
(11): COND_4683_1_MAIN_INVOKEMETHOD2(TRUE, 4683_0_nth_NONNULL(NULL), java.lang.Object(IntList(x0[11], x1[11]))) → 3247_1_MAIN_INVOKEMETHOD(3247_0_random_ArrayAccess(java.lang.Object(ARRAY(x2[11], x3[11])), x4[11]), x0[11])
(12): 4619_1_MAIN_INVOKEMETHOD(4619_0_nth_LE(java.lang.Object(IntList(x1[12], x2[12])), x0[12]), x4[12]) → COND_4619_1_MAIN_INVOKEMETHOD1(x0[12] > 1, 4619_0_nth_LE(java.lang.Object(IntList(x1[12], x2[12])), x0[12]), x4[12])
(13): COND_4619_1_MAIN_INVOKEMETHOD1(TRUE, 4619_0_nth_LE(java.lang.Object(IntList(x1[13], x2[13])), x0[13]), x4[13]) → 4619_1_MAIN_INVOKEMETHOD(4619_0_nth_LE(x1[13], x0[13] + -1), x4[13])
(14): 4619_1_MAIN_INVOKEMETHOD(4619_0_nth_LE(java.lang.Object(IntList(x1[14], x2[14])), x0[14]), java.lang.Object(IntList(x1[14], x2[14]))) → COND_4619_1_MAIN_INVOKEMETHOD2(x0[14] > 1, 4619_0_nth_LE(java.lang.Object(IntList(x1[14], x2[14])), x0[14]), java.lang.Object(IntList(x1[14], x2[14])))
(15): COND_4619_1_MAIN_INVOKEMETHOD2(TRUE, 4619_0_nth_LE(java.lang.Object(IntList(x1[15], x2[15])), x0[15]), java.lang.Object(IntList(x1[15], x2[15]))) → 4619_1_MAIN_INVOKEMETHOD(4619_0_nth_LE(x1[15], x0[15] + -1), java.lang.Object(IntList(x1[15], x2[15])))
(16): 4619_1_MAIN_INVOKEMETHOD(4619_0_nth_LE(NULL, x0[16]), x2[16]) → COND_4619_1_MAIN_INVOKEMETHOD3(x0[16] > 1, 4619_0_nth_LE(NULL, x0[16]), x2[16])
(17): COND_4619_1_MAIN_INVOKEMETHOD3(TRUE, 4619_0_nth_LE(NULL, x0[17]), x2[17]) → 4683_1_MAIN_INVOKEMETHOD(4683_0_nth_NONNULL(NULL), x2[17])

(0) -> (1), if ((x2[0] >= 2 && x2[0] < x0[0] →^* TRUE)∧(3247_0_random_ArrayAccess(java.lang.Object(ARRAY(x0[0], x1[0])), x2[0]) →^* 3247_0_random_ArrayAccess(java.lang.Object(ARRAY(x0[1], x1[1])), x2[1]))∧(x3[0] →^* x3[1]))

(1) -> (2), if ((3429_0_random_IntArithmetic(x4[1], x5[1]) →^* 3429_0_random_IntArithmetic(java.lang.Object(java.lang.String(x0[2], x1[2])), x2[2]))∧(x3[1] →^* x4[2]))

(2) -> (3), if ((x2[2] > 0 →^* TRUE)∧(3429_0_random_IntArithmetic(java.lang.Object(java.lang.String(x0[2], x1[2])), x2[2]) →^* 3429_0_random_IntArithmetic(java.lang.Object(java.lang.String(x0[3], x1[3])), x2[3]))∧(x4[2] →^* x4[3]))

(3) -> (4), if ((4619_0_nth_LE(x4[3], x1[3]) →^* 4619_0_nth_LE(x1[4], x0[4]))∧(x4[3] →^* x3[4]))

(3) -> (12), if ((4619_0_nth_LE(x4[3], x1[3]) →^* 4619_0_nth_LE(java.lang.Object(IntList(x1[12], x2[12])), x0[12]))∧(x4[3] →^* x4[12]))

(3) -> (14), if ((4619_0_nth_LE(x4[3], x1[3]) →^* 4619_0_nth_LE(java.lang.Object(IntList(x1[14], x2[14])), x0[14]))∧(x4[3] →^* java.lang.Object(IntList(x1[14], x2[14]))))

(3) -> (16), if ((4619_0_nth_LE(x4[3], x1[3]) →^* 4619_0_nth_LE(NULL, x0[16]))∧(x4[3] →^* x2[16]))

(4) -> (5), if ((x0[4] <= 1 →^* TRUE)∧(4619_0_nth_LE(x1[4], x0[4]) →^* 4619_0_nth_LE(x1[5], x0[5]))∧(x3[4] →^* x3[5]))

(5) -> (6), if ((4683_0_nth_NONNULL(x1[5]) →^* 4683_0_nth_NONNULL(java.lang.Object(IntList(x0[6], x1[6]))))∧(x3[5] →^* java.lang.Object(IntList(x2[6], x3[6]))))

(5) -> (8), if ((4683_0_nth_NONNULL(x1[5]) →^* 4683_0_nth_NONNULL(java.lang.Object(IntList(x0[8], x1[8]))))∧(x3[5] →^* java.lang.Object(IntList(x0[8], x1[8]))))

(5) -> (10), if ((4683_0_nth_NONNULL(x1[5]) →^* 4683_0_nth_NONNULL(NULL))∧(x3[5] →^* java.lang.Object(IntList(x0[10], x1[10]))))

(6) -> (7), if ((x1[6] > 0 →^* TRUE)∧(4683_0_nth_NONNULL(java.lang.Object(IntList(x0[6], x1[6]))) →^* 4683_0_nth_NONNULL(java.lang.Object(IntList(x0[7], x1[7]))))∧(java.lang.Object(IntList(x2[6], x3[6])) →^* java.lang.Object(IntList(x2[7], x3[7]))))

(7) -> (0), if ((3247_0_random_ArrayAccess(java.lang.Object(ARRAY(x4[7], x5[7])), x6[7]) →^* 3247_0_random_ArrayAccess(java.lang.Object(ARRAY(x0[0], x1[0])), x2[0]))∧(x2[7] →^* x3[0]))

(8) -> (9), if ((x1[8] > 0 →^* TRUE)∧(4683_0_nth_NONNULL(java.lang.Object(IntList(x0[8], x1[8]))) →^* 4683_0_nth_NONNULL(java.lang.Object(IntList(x0[9], x1[9]))))∧(java.lang.Object(IntList(x0[8], x1[8])) →^* java.lang.Object(IntList(x0[9], x1[9]))))

(9) -> (0), if ((3247_0_random_ArrayAccess(java.lang.Object(ARRAY(x2[9], x3[9])), x4[9]) →^* 3247_0_random_ArrayAccess(java.lang.Object(ARRAY(x0[0], x1[0])), x2[0]))∧(x0[9] →^* x3[0]))

(10) -> (11), if ((0 > 0 →^* TRUE)∧(java.lang.Object(IntList(x0[10], x1[10])) →^* java.lang.Object(IntList(x0[11], x1[11]))))

(11) -> (0), if ((3247_0_random_ArrayAccess(java.lang.Object(ARRAY(x2[11], x3[11])), x4[11]) →^* 3247_0_random_ArrayAccess(java.lang.Object(ARRAY(x0[0], x1[0])), x2[0]))∧(x0[11] →^* x3[0]))

(12) -> (13), if ((x0[12] > 1 →^* TRUE)∧(4619_0_nth_LE(java.lang.Object(IntList(x1[12], x2[12])), x0[12]) →^* 4619_0_nth_LE(java.lang.Object(IntList(x1[13], x2[13])), x0[13]))∧(x4[12] →^* x4[13]))

(13) -> (4), if ((4619_0_nth_LE(x1[13], x0[13] + -1) →^* 4619_0_nth_LE(x1[4], x0[4]))∧(x4[13] →^* x3[4]))

(13) -> (12), if ((4619_0_nth_LE(x1[13], x0[13] + -1) →^* 4619_0_nth_LE(java.lang.Object(IntList(x1[12], x2[12])), x0[12]))∧(x4[13] →^* x4[12]))

(13) -> (14), if ((4619_0_nth_LE(x1[13], x0[13] + -1) →^* 4619_0_nth_LE(java.lang.Object(IntList(x1[14], x2[14])), x0[14]))∧(x4[13] →^* java.lang.Object(IntList(x1[14], x2[14]))))

(13) -> (16), if ((4619_0_nth_LE(x1[13], x0[13] + -1) →^* 4619_0_nth_LE(NULL, x0[16]))∧(x4[13] →^* x2[16]))

(14) -> (15), if ((x0[14] > 1 →^* TRUE)∧(4619_0_nth_LE(java.lang.Object(IntList(x1[14], x2[14])), x0[14]) →^* 4619_0_nth_LE(java.lang.Object(IntList(x1[15], x2[15])), x0[15]))∧(java.lang.Object(IntList(x1[14], x2[14])) →^* java.lang.Object(IntList(x1[15], x2[15]))))

(15) -> (4), if ((4619_0_nth_LE(x1[15], x0[15] + -1) →^* 4619_0_nth_LE(x1[4], x0[4]))∧(java.lang.Object(IntList(x1[15], x2[15])) →^* x3[4]))

(15) -> (12), if ((4619_0_nth_LE(x1[15], x0[15] + -1) →^* 4619_0_nth_LE(java.lang.Object(IntList(x1[12], x2[12])), x0[12]))∧(java.lang.Object(IntList(x1[15], x2[15])) →^* x4[12]))

(15) -> (14), if ((4619_0_nth_LE(x1[15], x0[15] + -1) →^* 4619_0_nth_LE(java.lang.Object(IntList(x1[14], x2[14])), x0[14]))∧(java.lang.Object(IntList(x1[15], x2[15])) →^* java.lang.Object(IntList(x1[14], x2[14]))))

(15) -> (16), if ((4619_0_nth_LE(x1[15], x0[15] + -1) →^* 4619_0_nth_LE(NULL, x0[16]))∧(java.lang.Object(IntList(x1[15], x2[15])) →^* x2[16]))

(16) -> (17), if ((x0[16] > 1 →^* TRUE)∧(4619_0_nth_LE(NULL, x0[16]) →^* 4619_0_nth_LE(NULL, x0[17]))∧(x2[16] →^* x2[17]))

(17) -> (6), if ((4683_0_nth_NONNULL(NULL) →^* 4683_0_nth_NONNULL(java.lang.Object(IntList(x0[6], x1[6]))))∧(x2[17] →^* java.lang.Object(IntList(x2[6], x3[6]))))

(17) -> (8), if ((4683_0_nth_NONNULL(NULL) →^* 4683_0_nth_NONNULL(java.lang.Object(IntList(x0[8], x1[8]))))∧(x2[17] →^* java.lang.Object(IntList(x0[8], x1[8]))))

(17) -> (10), if (x2[17] →^* java.lang.Object(IntList(x0[10], x1[10])))

The set Q is empty.

(15) IDPNonInfProof (SOUND transformation)

The constraints were generated the following way:
The DP Problem is simplified using the Induction Calculus [NONINF] with the following steps:
Note that final constraints are written in bold face.

For Pair 3247_1_MAIN_INVOKEMETHOD(3247_0_random_ArrayAccess(java.lang.Object(ARRAY(x0, x1)), x2), x3) → COND_3247_1_MAIN_INVOKEMETHOD(&&(>=(x2, 2), <(x2, x0)), 3247_0_random_ArrayAccess(java.lang.Object(ARRAY(x0, x1)), x2), x3) the following chains were created:

We consider the chain 3247_1_MAIN_INVOKEMETHOD(3247_0_random_ArrayAccess(java.lang.Object(ARRAY(x0[0], x1[0])), x2[0]), x3[0]) → COND_3247_1_MAIN_INVOKEMETHOD(&&(>=(x2[0], 2), <(x2[0], x0[0])), 3247_0_random_ArrayAccess(java.lang.Object(ARRAY(x0[0], x1[0])), x2[0]), x3[0]), COND_3247_1_MAIN_INVOKEMETHOD(TRUE, 3247_0_random_ArrayAccess(java.lang.Object(ARRAY(x0[1], x1[1])), x2[1]), x3[1]) → 3429_1_MAIN_INVOKEMETHOD(3429_0_random_IntArithmetic(x4[1], x5[1]), x3[1]) which results in the following constraint:
(1)    (&&(>=(x2[0], 2), <(x2[0], x0[0]))=TRUE∧3247_0_random_ArrayAccess(java.lang.Object(ARRAY(x0[0], x1[0])), x2[0])=3247_0_random_ArrayAccess(java.lang.Object(ARRAY(x0[1], x1[1])), x2[1])∧x3[0]=x3[1] ⇒ 3247_1_MAIN_INVOKEMETHOD(3247_0_random_ArrayAccess(java.lang.Object(ARRAY(x0[0], x1[0])), x2[0]), x3[0])≥NonInfC∧3247_1_MAIN_INVOKEMETHOD(3247_0_random_ArrayAccess(java.lang.Object(ARRAY(x0[0], x1[0])), x2[0]), x3[0])≥COND_3247_1_MAIN_INVOKEMETHOD(&&(>=(x2[0], 2), <(x2[0], x0[0])), 3247_0_random_ArrayAccess(java.lang.Object(ARRAY(x0[0], x1[0])), x2[0]), x3[0])∧(U^Increasing(COND_3247_1_MAIN_INVOKEMETHOD(&&(>=(x2[0], 2), <(x2[0], x0[0])), 3247_0_random_ArrayAccess(java.lang.Object(ARRAY(x0[0], x1[0])), x2[0]), x3[0])), ≥))

We simplified constraint (1) using rules (I), (II), (IV) which results in the following new constraint:
(2)    (&&(>=(x2[0], 2), <(x2[0], x0[0]))=TRUE ⇒ 3247_1_MAIN_INVOKEMETHOD(3247_0_random_ArrayAccess(java.lang.Object(ARRAY(x0[0], x1[0])), x2[0]), x3[0])≥NonInfC∧3247_1_MAIN_INVOKEMETHOD(3247_0_random_ArrayAccess(java.lang.Object(ARRAY(x0[0], x1[0])), x2[0]), x3[0])≥COND_3247_1_MAIN_INVOKEMETHOD(&&(>=(x2[0], 2), <(x2[0], x0[0])), 3247_0_random_ArrayAccess(java.lang.Object(ARRAY(x0[0], x1[0])), x2[0]), x3[0])∧(U^Increasing(COND_3247_1_MAIN_INVOKEMETHOD(&&(>=(x2[0], 2), <(x2[0], x0[0])), 3247_0_random_ArrayAccess(java.lang.Object(ARRAY(x0[0], x1[0])), x2[0]), x3[0])), ≥))

We simplified constraint (2) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(3)    (0 ≥ 0 ⇒ (U^Increasing(COND_3247_1_MAIN_INVOKEMETHOD(&&(>=(x2[0], 2), <(x2[0], x0[0])), 3247_0_random_ArrayAccess(java.lang.Object(ARRAY(x0[0], x1[0])), x2[0]), x3[0])), ≥)∧[(-1)bni_72 + (-1)Bound*bni_72] + [(2)bni_72]x3[0] ≥ 0∧[(-1)bso_73] ≥ 0)

We simplified constraint (3) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(4)    (0 ≥ 0 ⇒ (U^Increasing(COND_3247_1_MAIN_INVOKEMETHOD(&&(>=(x2[0], 2), <(x2[0], x0[0])), 3247_0_random_ArrayAccess(java.lang.Object(ARRAY(x0[0], x1[0])), x2[0]), x3[0])), ≥)∧[(-1)bni_72 + (-1)Bound*bni_72] + [(2)bni_72]x3[0] ≥ 0∧[(-1)bso_73] ≥ 0)

We simplified constraint (4) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(5)    (0 ≥ 0 ⇒ (U^Increasing(COND_3247_1_MAIN_INVOKEMETHOD(&&(>=(x2[0], 2), <(x2[0], x0[0])), 3247_0_random_ArrayAccess(java.lang.Object(ARRAY(x0[0], x1[0])), x2[0]), x3[0])), ≥)∧[(-1)bni_72 + (-1)Bound*bni_72] + [(2)bni_72]x3[0] ≥ 0∧[(-1)bso_73] ≥ 0)

We simplified constraint (5) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:
(6)    (0 ≥ 0 ⇒ (U^Increasing(COND_3247_1_MAIN_INVOKEMETHOD(&&(>=(x2[0], 2), <(x2[0], x0[0])), 3247_0_random_ArrayAccess(java.lang.Object(ARRAY(x0[0], x1[0])), x2[0]), x3[0])), ≥)∧[(2)bni_72] ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[(-1)bni_72 + (-1)Bound*bni_72] ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[(-1)bso_73] ≥ 0)

For Pair COND_3247_1_MAIN_INVOKEMETHOD(TRUE, 3247_0_random_ArrayAccess(java.lang.Object(ARRAY(x0, x1)), x2), x3) → 3429_1_MAIN_INVOKEMETHOD(3429_0_random_IntArithmetic(x4, x5), x3) the following chains were created:

We consider the chain 3247_1_MAIN_INVOKEMETHOD(3247_0_random_ArrayAccess(java.lang.Object(ARRAY(x0[0], x1[0])), x2[0]), x3[0]) → COND_3247_1_MAIN_INVOKEMETHOD(&&(>=(x2[0], 2), <(x2[0], x0[0])), 3247_0_random_ArrayAccess(java.lang.Object(ARRAY(x0[0], x1[0])), x2[0]), x3[0]), COND_3247_1_MAIN_INVOKEMETHOD(TRUE, 3247_0_random_ArrayAccess(java.lang.Object(ARRAY(x0[1], x1[1])), x2[1]), x3[1]) → 3429_1_MAIN_INVOKEMETHOD(3429_0_random_IntArithmetic(x4[1], x5[1]), x3[1]), 3429_1_MAIN_INVOKEMETHOD(3429_0_random_IntArithmetic(java.lang.Object(java.lang.String(x0[2], x1[2])), x2[2]), x4[2]) → COND_3429_1_MAIN_INVOKEMETHOD(>(x2[2], 0), 3429_0_random_IntArithmetic(java.lang.Object(java.lang.String(x0[2], x1[2])), x2[2]), x4[2]) which results in the following constraint:
(7)    (&&(>=(x2[0], 2), <(x2[0], x0[0]))=TRUE∧3247_0_random_ArrayAccess(java.lang.Object(ARRAY(x0[0], x1[0])), x2[0])=3247_0_random_ArrayAccess(java.lang.Object(ARRAY(x0[1], x1[1])), x2[1])∧x3[0]=x3[1]∧3429_0_random_IntArithmetic(x4[1], x5[1])=3429_0_random_IntArithmetic(java.lang.Object(java.lang.String(x0[2], x1[2])), x2[2])∧x3[1]=x4[2] ⇒ COND_3247_1_MAIN_INVOKEMETHOD(TRUE, 3247_0_random_ArrayAccess(java.lang.Object(ARRAY(x0[1], x1[1])), x2[1]), x3[1])≥NonInfC∧COND_3247_1_MAIN_INVOKEMETHOD(TRUE, 3247_0_random_ArrayAccess(java.lang.Object(ARRAY(x0[1], x1[1])), x2[1]), x3[1])≥3429_1_MAIN_INVOKEMETHOD(3429_0_random_IntArithmetic(x4[1], x5[1]), x3[1])∧(U^Increasing(3429_1_MAIN_INVOKEMETHOD(3429_0_random_IntArithmetic(x4[1], x5[1]), x3[1])), ≥))

We simplified constraint (7) using rules (I), (II), (III), (IV) which results in the following new constraint:
(8)    (&&(>=(x2[0], 2), <(x2[0], x0[0]))=TRUE ⇒ COND_3247_1_MAIN_INVOKEMETHOD(TRUE, 3247_0_random_ArrayAccess(java.lang.Object(ARRAY(x0[0], x1[0])), x2[0]), x3[0])≥NonInfC∧COND_3247_1_MAIN_INVOKEMETHOD(TRUE, 3247_0_random_ArrayAccess(java.lang.Object(ARRAY(x0[0], x1[0])), x2[0]), x3[0])≥3429_1_MAIN_INVOKEMETHOD(3429_0_random_IntArithmetic(java.lang.Object(java.lang.String(x0[2], x1[2])), x5[1]), x3[0])∧(U^Increasing(3429_1_MAIN_INVOKEMETHOD(3429_0_random_IntArithmetic(x4[1], x5[1]), x3[1])), ≥))

We simplified constraint (8) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(9)    (0 ≥ 0 ⇒ (U^Increasing(3429_1_MAIN_INVOKEMETHOD(3429_0_random_IntArithmetic(x4[1], x5[1]), x3[1])), ≥)∧[(-1)bni_74 + (-1)Bound*bni_74] + [(2)bni_74]x3[0] ≥ 0∧[(-1)bso_75] ≥ 0)

We simplified constraint (9) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(10)    (0 ≥ 0 ⇒ (U^Increasing(3429_1_MAIN_INVOKEMETHOD(3429_0_random_IntArithmetic(x4[1], x5[1]), x3[1])), ≥)∧[(-1)bni_74 + (-1)Bound*bni_74] + [(2)bni_74]x3[0] ≥ 0∧[(-1)bso_75] ≥ 0)

We simplified constraint (10) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(11)    (0 ≥ 0 ⇒ (U^Increasing(3429_1_MAIN_INVOKEMETHOD(3429_0_random_IntArithmetic(x4[1], x5[1]), x3[1])), ≥)∧[(-1)bni_74 + (-1)Bound*bni_74] + [(2)bni_74]x3[0] ≥ 0∧[(-1)bso_75] ≥ 0)

We simplified constraint (11) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:
(12)    (0 ≥ 0 ⇒ (U^Increasing(3429_1_MAIN_INVOKEMETHOD(3429_0_random_IntArithmetic(x4[1], x5[1]), x3[1])), ≥)∧[(2)bni_74] ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[(-1)bni_74 + (-1)Bound*bni_74] ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[(-1)bso_75] ≥ 0)

For Pair 3429_1_MAIN_INVOKEMETHOD(3429_0_random_IntArithmetic(java.lang.Object(java.lang.String(x0, x1)), x2), x4) → COND_3429_1_MAIN_INVOKEMETHOD(>(x2, 0), 3429_0_random_IntArithmetic(java.lang.Object(java.lang.String(x0, x1)), x2), x4) the following chains were created:

We consider the chain 3429_1_MAIN_INVOKEMETHOD(3429_0_random_IntArithmetic(java.lang.Object(java.lang.String(x0[2], x1[2])), x2[2]), x4[2]) → COND_3429_1_MAIN_INVOKEMETHOD(>(x2[2], 0), 3429_0_random_IntArithmetic(java.lang.Object(java.lang.String(x0[2], x1[2])), x2[2]), x4[2]), COND_3429_1_MAIN_INVOKEMETHOD(TRUE, 3429_0_random_IntArithmetic(java.lang.Object(java.lang.String(x0[3], x1[3])), x2[3]), x4[3]) → 4619_1_MAIN_INVOKEMETHOD(4619_0_nth_LE(x4[3], x1[3]), x4[3]) which results in the following constraint:
(13)    (>(x2[2], 0)=TRUE∧3429_0_random_IntArithmetic(java.lang.Object(java.lang.String(x0[2], x1[2])), x2[2])=3429_0_random_IntArithmetic(java.lang.Object(java.lang.String(x0[3], x1[3])), x2[3])∧x4[2]=x4[3] ⇒ 3429_1_MAIN_INVOKEMETHOD(3429_0_random_IntArithmetic(java.lang.Object(java.lang.String(x0[2], x1[2])), x2[2]), x4[2])≥NonInfC∧3429_1_MAIN_INVOKEMETHOD(3429_0_random_IntArithmetic(java.lang.Object(java.lang.String(x0[2], x1[2])), x2[2]), x4[2])≥COND_3429_1_MAIN_INVOKEMETHOD(>(x2[2], 0), 3429_0_random_IntArithmetic(java.lang.Object(java.lang.String(x0[2], x1[2])), x2[2]), x4[2])∧(U^Increasing(COND_3429_1_MAIN_INVOKEMETHOD(>(x2[2], 0), 3429_0_random_IntArithmetic(java.lang.Object(java.lang.String(x0[2], x1[2])), x2[2]), x4[2])), ≥))

We simplified constraint (13) using rules (I), (II), (IV) which results in the following new constraint:
(14)    (>(x2[2], 0)=TRUE ⇒ 3429_1_MAIN_INVOKEMETHOD(3429_0_random_IntArithmetic(java.lang.Object(java.lang.String(x0[2], x1[2])), x2[2]), x4[2])≥NonInfC∧3429_1_MAIN_INVOKEMETHOD(3429_0_random_IntArithmetic(java.lang.Object(java.lang.String(x0[2], x1[2])), x2[2]), x4[2])≥COND_3429_1_MAIN_INVOKEMETHOD(>(x2[2], 0), 3429_0_random_IntArithmetic(java.lang.Object(java.lang.String(x0[2], x1[2])), x2[2]), x4[2])∧(U^Increasing(COND_3429_1_MAIN_INVOKEMETHOD(>(x2[2], 0), 3429_0_random_IntArithmetic(java.lang.Object(java.lang.String(x0[2], x1[2])), x2[2]), x4[2])), ≥))

We simplified constraint (14) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(15)    (0 ≥ 0 ⇒ (U^Increasing(COND_3429_1_MAIN_INVOKEMETHOD(>(x2[2], 0), 3429_0_random_IntArithmetic(java.lang.Object(java.lang.String(x0[2], x1[2])), x2[2]), x4[2])), ≥)∧[(-1)bni_76 + (-1)Bound*bni_76] + [(2)bni_76]x4[2] ≥ 0∧[(-1)bso_77] ≥ 0)

We simplified constraint (15) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(16)    (0 ≥ 0 ⇒ (U^Increasing(COND_3429_1_MAIN_INVOKEMETHOD(>(x2[2], 0), 3429_0_random_IntArithmetic(java.lang.Object(java.lang.String(x0[2], x1[2])), x2[2]), x4[2])), ≥)∧[(-1)bni_76 + (-1)Bound*bni_76] + [(2)bni_76]x4[2] ≥ 0∧[(-1)bso_77] ≥ 0)

We simplified constraint (16) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(17)    (0 ≥ 0 ⇒ (U^Increasing(COND_3429_1_MAIN_INVOKEMETHOD(>(x2[2], 0), 3429_0_random_IntArithmetic(java.lang.Object(java.lang.String(x0[2], x1[2])), x2[2]), x4[2])), ≥)∧[(-1)bni_76 + (-1)Bound*bni_76] + [(2)bni_76]x4[2] ≥ 0∧[(-1)bso_77] ≥ 0)

We simplified constraint (17) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:
(18)    (0 ≥ 0 ⇒ (U^Increasing(COND_3429_1_MAIN_INVOKEMETHOD(>(x2[2], 0), 3429_0_random_IntArithmetic(java.lang.Object(java.lang.String(x0[2], x1[2])), x2[2]), x4[2])), ≥)∧[(2)bni_76] ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[(-1)bni_76 + (-1)Bound*bni_76] ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[(-1)bso_77] ≥ 0)

For Pair COND_3429_1_MAIN_INVOKEMETHOD(TRUE, 3429_0_random_IntArithmetic(java.lang.Object(java.lang.String(x0, x1)), x2), x4) → 4619_1_MAIN_INVOKEMETHOD(4619_0_nth_LE(x4, x1), x4) the following chains were created:

We consider the chain 3429_1_MAIN_INVOKEMETHOD(3429_0_random_IntArithmetic(java.lang.Object(java.lang.String(x0[2], x1[2])), x2[2]), x4[2]) → COND_3429_1_MAIN_INVOKEMETHOD(>(x2[2], 0), 3429_0_random_IntArithmetic(java.lang.Object(java.lang.String(x0[2], x1[2])), x2[2]), x4[2]), COND_3429_1_MAIN_INVOKEMETHOD(TRUE, 3429_0_random_IntArithmetic(java.lang.Object(java.lang.String(x0[3], x1[3])), x2[3]), x4[3]) → 4619_1_MAIN_INVOKEMETHOD(4619_0_nth_LE(x4[3], x1[3]), x4[3]) which results in the following constraint:
(19)    (>(x2[2], 0)=TRUE∧3429_0_random_IntArithmetic(java.lang.Object(java.lang.String(x0[2], x1[2])), x2[2])=3429_0_random_IntArithmetic(java.lang.Object(java.lang.String(x0[3], x1[3])), x2[3])∧x4[2]=x4[3] ⇒ COND_3429_1_MAIN_INVOKEMETHOD(TRUE, 3429_0_random_IntArithmetic(java.lang.Object(java.lang.String(x0[3], x1[3])), x2[3]), x4[3])≥NonInfC∧COND_3429_1_MAIN_INVOKEMETHOD(TRUE, 3429_0_random_IntArithmetic(java.lang.Object(java.lang.String(x0[3], x1[3])), x2[3]), x4[3])≥4619_1_MAIN_INVOKEMETHOD(4619_0_nth_LE(x4[3], x1[3]), x4[3])∧(U^Increasing(4619_1_MAIN_INVOKEMETHOD(4619_0_nth_LE(x4[3], x1[3]), x4[3])), ≥))

We simplified constraint (19) using rules (I), (II), (III) which results in the following new constraint:
(20)    (>(x2[2], 0)=TRUE ⇒ COND_3429_1_MAIN_INVOKEMETHOD(TRUE, 3429_0_random_IntArithmetic(java.lang.Object(java.lang.String(x0[2], x1[2])), x2[2]), x4[2])≥NonInfC∧COND_3429_1_MAIN_INVOKEMETHOD(TRUE, 3429_0_random_IntArithmetic(java.lang.Object(java.lang.String(x0[2], x1[2])), x2[2]), x4[2])≥4619_1_MAIN_INVOKEMETHOD(4619_0_nth_LE(x4[2], x1[2]), x4[2])∧(U^Increasing(4619_1_MAIN_INVOKEMETHOD(4619_0_nth_LE(x4[3], x1[3]), x4[3])), ≥))

We simplified constraint (20) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(21)    (0 ≥ 0 ⇒ (U^Increasing(4619_1_MAIN_INVOKEMETHOD(4619_0_nth_LE(x4[3], x1[3]), x4[3])), ≥)∧[(-1)bni_78 + (-1)Bound*bni_78] + [(2)bni_78]x4[2] ≥ 0∧[(-1)bso_79] ≥ 0)

We simplified constraint (21) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(22)    (0 ≥ 0 ⇒ (U^Increasing(4619_1_MAIN_INVOKEMETHOD(4619_0_nth_LE(x4[3], x1[3]), x4[3])), ≥)∧[(-1)bni_78 + (-1)Bound*bni_78] + [(2)bni_78]x4[2] ≥ 0∧[(-1)bso_79] ≥ 0)

We simplified constraint (22) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(23)    (0 ≥ 0 ⇒ (U^Increasing(4619_1_MAIN_INVOKEMETHOD(4619_0_nth_LE(x4[3], x1[3]), x4[3])), ≥)∧[(-1)bni_78 + (-1)Bound*bni_78] + [(2)bni_78]x4[2] ≥ 0∧[(-1)bso_79] ≥ 0)

We simplified constraint (23) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:
(24)    (0 ≥ 0 ⇒ (U^Increasing(4619_1_MAIN_INVOKEMETHOD(4619_0_nth_LE(x4[3], x1[3]), x4[3])), ≥)∧[(2)bni_78] ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[(-1)bni_78 + (-1)Bound*bni_78] ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[(-1)bso_79] ≥ 0)

For Pair 4619_1_MAIN_INVOKEMETHOD(4619_0_nth_LE(x1, x0), x3) → COND_4619_1_MAIN_INVOKEMETHOD(<=(x0, 1), 4619_0_nth_LE(x1, x0), x3) the following chains were created:

We consider the chain 4619_1_MAIN_INVOKEMETHOD(4619_0_nth_LE(x1[4], x0[4]), x3[4]) → COND_4619_1_MAIN_INVOKEMETHOD(<=(x0[4], 1), 4619_0_nth_LE(x1[4], x0[4]), x3[4]), COND_4619_1_MAIN_INVOKEMETHOD(TRUE, 4619_0_nth_LE(x1[5], x0[5]), x3[5]) → 4683_1_MAIN_INVOKEMETHOD(4683_0_nth_NONNULL(x1[5]), x3[5]) which results in the following constraint:
(25)    (<=(x0[4], 1)=TRUE∧4619_0_nth_LE(x1[4], x0[4])=4619_0_nth_LE(x1[5], x0[5])∧x3[4]=x3[5] ⇒ 4619_1_MAIN_INVOKEMETHOD(4619_0_nth_LE(x1[4], x0[4]), x3[4])≥NonInfC∧4619_1_MAIN_INVOKEMETHOD(4619_0_nth_LE(x1[4], x0[4]), x3[4])≥COND_4619_1_MAIN_INVOKEMETHOD(<=(x0[4], 1), 4619_0_nth_LE(x1[4], x0[4]), x3[4])∧(U^Increasing(COND_4619_1_MAIN_INVOKEMETHOD(<=(x0[4], 1), 4619_0_nth_LE(x1[4], x0[4]), x3[4])), ≥))

We simplified constraint (25) using rules (I), (II), (IV) which results in the following new constraint:
(26)    (<=(x0[4], 1)=TRUE ⇒ 4619_1_MAIN_INVOKEMETHOD(4619_0_nth_LE(x1[4], x0[4]), x3[4])≥NonInfC∧4619_1_MAIN_INVOKEMETHOD(4619_0_nth_LE(x1[4], x0[4]), x3[4])≥COND_4619_1_MAIN_INVOKEMETHOD(<=(x0[4], 1), 4619_0_nth_LE(x1[4], x0[4]), x3[4])∧(U^Increasing(COND_4619_1_MAIN_INVOKEMETHOD(<=(x0[4], 1), 4619_0_nth_LE(x1[4], x0[4]), x3[4])), ≥))

We simplified constraint (26) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(27)    (0 ≥ 0 ⇒ (U^Increasing(COND_4619_1_MAIN_INVOKEMETHOD(<=(x0[4], 1), 4619_0_nth_LE(x1[4], x0[4]), x3[4])), ≥)∧[(-1)bni_80 + (-1)Bound*bni_80] + [bni_80]x3[4] + [bni_80]x1[4] ≥ 0∧[(-1)bso_81] + x1[4] ≥ 0)

We simplified constraint (27) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(28)    (0 ≥ 0 ⇒ (U^Increasing(COND_4619_1_MAIN_INVOKEMETHOD(<=(x0[4], 1), 4619_0_nth_LE(x1[4], x0[4]), x3[4])), ≥)∧[(-1)bni_80 + (-1)Bound*bni_80] + [bni_80]x3[4] + [bni_80]x1[4] ≥ 0∧[(-1)bso_81] + x1[4] ≥ 0)

We simplified constraint (28) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(29)    (0 ≥ 0 ⇒ (U^Increasing(COND_4619_1_MAIN_INVOKEMETHOD(<=(x0[4], 1), 4619_0_nth_LE(x1[4], x0[4]), x3[4])), ≥)∧[(-1)bni_80 + (-1)Bound*bni_80] + [bni_80]x3[4] + [bni_80]x1[4] ≥ 0∧[(-1)bso_81] + x1[4] ≥ 0)

We simplified constraint (29) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:
(30)    (0 ≥ 0 ⇒ (U^Increasing(COND_4619_1_MAIN_INVOKEMETHOD(<=(x0[4], 1), 4619_0_nth_LE(x1[4], x0[4]), x3[4])), ≥)∧[bni_80] ≥ 0∧0 ≥ 0∧[bni_80] ≥ 0∧[(-1)bni_80 + (-1)Bound*bni_80] ≥ 0∧0 ≥ 0∧0 ≥ 0∧[1] ≥ 0∧[(-1)bso_81] ≥ 0)

For Pair COND_4619_1_MAIN_INVOKEMETHOD(TRUE, 4619_0_nth_LE(x1, x0), x3) → 4683_1_MAIN_INVOKEMETHOD(4683_0_nth_NONNULL(x1), x3) the following chains were created:

We consider the chain 4619_1_MAIN_INVOKEMETHOD(4619_0_nth_LE(x1[4], x0[4]), x3[4]) → COND_4619_1_MAIN_INVOKEMETHOD(<=(x0[4], 1), 4619_0_nth_LE(x1[4], x0[4]), x3[4]), COND_4619_1_MAIN_INVOKEMETHOD(TRUE, 4619_0_nth_LE(x1[5], x0[5]), x3[5]) → 4683_1_MAIN_INVOKEMETHOD(4683_0_nth_NONNULL(x1[5]), x3[5]), 4683_1_MAIN_INVOKEMETHOD(4683_0_nth_NONNULL(java.lang.Object(IntList(x0[6], x1[6]))), java.lang.Object(IntList(x2[6], x3[6]))) → COND_4683_1_MAIN_INVOKEMETHOD(>(x1[6], 0), 4683_0_nth_NONNULL(java.lang.Object(IntList(x0[6], x1[6]))), java.lang.Object(IntList(x2[6], x3[6]))) which results in the following constraint:
(31)    (<=(x0[4], 1)=TRUE∧4619_0_nth_LE(x1[4], x0[4])=4619_0_nth_LE(x1[5], x0[5])∧x3[4]=x3[5]∧4683_0_nth_NONNULL(x1[5])=4683_0_nth_NONNULL(java.lang.Object(IntList(x0[6], x1[6])))∧x3[5]=java.lang.Object(IntList(x2[6], x3[6])) ⇒ COND_4619_1_MAIN_INVOKEMETHOD(TRUE, 4619_0_nth_LE(x1[5], x0[5]), x3[5])≥NonInfC∧COND_4619_1_MAIN_INVOKEMETHOD(TRUE, 4619_0_nth_LE(x1[5], x0[5]), x3[5])≥4683_1_MAIN_INVOKEMETHOD(4683_0_nth_NONNULL(x1[5]), x3[5])∧(U^Increasing(4683_1_MAIN_INVOKEMETHOD(4683_0_nth_NONNULL(x1[5]), x3[5])), ≥))

We simplified constraint (31) using rules (I), (II), (III) which results in the following new constraint:
(32)    (<=(x0[4], 1)=TRUE ⇒ COND_4619_1_MAIN_INVOKEMETHOD(TRUE, 4619_0_nth_LE(java.lang.Object(IntList(x0[6], x1[6])), x0[4]), java.lang.Object(IntList(x2[6], x3[6])))≥NonInfC∧COND_4619_1_MAIN_INVOKEMETHOD(TRUE, 4619_0_nth_LE(java.lang.Object(IntList(x0[6], x1[6])), x0[4]), java.lang.Object(IntList(x2[6], x3[6])))≥4683_1_MAIN_INVOKEMETHOD(4683_0_nth_NONNULL(java.lang.Object(IntList(x0[6], x1[6]))), java.lang.Object(IntList(x2[6], x3[6])))∧(U^Increasing(4683_1_MAIN_INVOKEMETHOD(4683_0_nth_NONNULL(x1[5]), x3[5])), ≥))

We simplified constraint (32) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(33)    (0 ≥ 0 ⇒ (U^Increasing(4683_1_MAIN_INVOKEMETHOD(4683_0_nth_NONNULL(x1[5]), x3[5])), ≥)∧[(-1)bni_82 + (-1)Bound*bni_82] + [(9)bni_82]x2[6] ≥ 0∧[(-1)bso_83] ≥ 0)

We simplified constraint (33) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(34)    (0 ≥ 0 ⇒ (U^Increasing(4683_1_MAIN_INVOKEMETHOD(4683_0_nth_NONNULL(x1[5]), x3[5])), ≥)∧[(-1)bni_82 + (-1)Bound*bni_82] + [(9)bni_82]x2[6] ≥ 0∧[(-1)bso_83] ≥ 0)

We simplified constraint (34) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(35)    (0 ≥ 0 ⇒ (U^Increasing(4683_1_MAIN_INVOKEMETHOD(4683_0_nth_NONNULL(x1[5]), x3[5])), ≥)∧[(-1)bni_82 + (-1)Bound*bni_82] + [(9)bni_82]x2[6] ≥ 0∧[(-1)bso_83] ≥ 0)

We simplified constraint (35) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:
(36)    (0 ≥ 0 ⇒ (U^Increasing(4683_1_MAIN_INVOKEMETHOD(4683_0_nth_NONNULL(x1[5]), x3[5])), ≥)∧0 ≥ 0∧[(9)bni_82] ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[(-1)bni_82 + (-1)Bound*bni_82] ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[(-1)bso_83] ≥ 0)
We consider the chain 4619_1_MAIN_INVOKEMETHOD(4619_0_nth_LE(x1[4], x0[4]), x3[4]) → COND_4619_1_MAIN_INVOKEMETHOD(<=(x0[4], 1), 4619_0_nth_LE(x1[4], x0[4]), x3[4]), COND_4619_1_MAIN_INVOKEMETHOD(TRUE, 4619_0_nth_LE(x1[5], x0[5]), x3[5]) → 4683_1_MAIN_INVOKEMETHOD(4683_0_nth_NONNULL(x1[5]), x3[5]), 4683_1_MAIN_INVOKEMETHOD(4683_0_nth_NONNULL(java.lang.Object(IntList(x0[8], x1[8]))), java.lang.Object(IntList(x0[8], x1[8]))) → COND_4683_1_MAIN_INVOKEMETHOD1(>(x1[8], 0), 4683_0_nth_NONNULL(java.lang.Object(IntList(x0[8], x1[8]))), java.lang.Object(IntList(x0[8], x1[8]))) which results in the following constraint:
(37)    (<=(x0[4], 1)=TRUE∧4619_0_nth_LE(x1[4], x0[4])=4619_0_nth_LE(x1[5], x0[5])∧x3[4]=x3[5]∧4683_0_nth_NONNULL(x1[5])=4683_0_nth_NONNULL(java.lang.Object(IntList(x0[8], x1[8])))∧x3[5]=java.lang.Object(IntList(x0[8], x1[8])) ⇒ COND_4619_1_MAIN_INVOKEMETHOD(TRUE, 4619_0_nth_LE(x1[5], x0[5]), x3[5])≥NonInfC∧COND_4619_1_MAIN_INVOKEMETHOD(TRUE, 4619_0_nth_LE(x1[5], x0[5]), x3[5])≥4683_1_MAIN_INVOKEMETHOD(4683_0_nth_NONNULL(x1[5]), x3[5])∧(U^Increasing(4683_1_MAIN_INVOKEMETHOD(4683_0_nth_NONNULL(x1[5]), x3[5])), ≥))

We simplified constraint (37) using rules (I), (II), (III) which results in the following new constraint:
(38)    (<=(x0[4], 1)=TRUE ⇒ COND_4619_1_MAIN_INVOKEMETHOD(TRUE, 4619_0_nth_LE(java.lang.Object(IntList(x0[8], x1[8])), x0[4]), java.lang.Object(IntList(x0[8], x1[8])))≥NonInfC∧COND_4619_1_MAIN_INVOKEMETHOD(TRUE, 4619_0_nth_LE(java.lang.Object(IntList(x0[8], x1[8])), x0[4]), java.lang.Object(IntList(x0[8], x1[8])))≥4683_1_MAIN_INVOKEMETHOD(4683_0_nth_NONNULL(java.lang.Object(IntList(x0[8], x1[8]))), java.lang.Object(IntList(x0[8], x1[8])))∧(U^Increasing(4683_1_MAIN_INVOKEMETHOD(4683_0_nth_NONNULL(x1[5]), x3[5])), ≥))

We simplified constraint (38) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(39)    (0 ≥ 0 ⇒ (U^Increasing(4683_1_MAIN_INVOKEMETHOD(4683_0_nth_NONNULL(x1[5]), x3[5])), ≥)∧[(-1)bni_82 + (-1)Bound*bni_82] + [(9)bni_82]x0[8] ≥ 0∧[(-1)bso_83] ≥ 0)

We simplified constraint (39) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(40)    (0 ≥ 0 ⇒ (U^Increasing(4683_1_MAIN_INVOKEMETHOD(4683_0_nth_NONNULL(x1[5]), x3[5])), ≥)∧[(-1)bni_82 + (-1)Bound*bni_82] + [(9)bni_82]x0[8] ≥ 0∧[(-1)bso_83] ≥ 0)

We simplified constraint (40) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(41)    (0 ≥ 0 ⇒ (U^Increasing(4683_1_MAIN_INVOKEMETHOD(4683_0_nth_NONNULL(x1[5]), x3[5])), ≥)∧[(-1)bni_82 + (-1)Bound*bni_82] + [(9)bni_82]x0[8] ≥ 0∧[(-1)bso_83] ≥ 0)

We simplified constraint (41) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:
(42)    (0 ≥ 0 ⇒ (U^Increasing(4683_1_MAIN_INVOKEMETHOD(4683_0_nth_NONNULL(x1[5]), x3[5])), ≥)∧0 ≥ 0∧[(9)bni_82] ≥ 0∧0 ≥ 0∧[(-1)bni_82 + (-1)Bound*bni_82] ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[(-1)bso_83] ≥ 0)
We consider the chain 4619_1_MAIN_INVOKEMETHOD(4619_0_nth_LE(x1[4], x0[4]), x3[4]) → COND_4619_1_MAIN_INVOKEMETHOD(<=(x0[4], 1), 4619_0_nth_LE(x1[4], x0[4]), x3[4]), COND_4619_1_MAIN_INVOKEMETHOD(TRUE, 4619_0_nth_LE(x1[5], x0[5]), x3[5]) → 4683_1_MAIN_INVOKEMETHOD(4683_0_nth_NONNULL(x1[5]), x3[5]), 4683_1_MAIN_INVOKEMETHOD(4683_0_nth_NONNULL(NULL), java.lang.Object(IntList(x0[10], x1[10]))) → COND_4683_1_MAIN_INVOKEMETHOD2(>(0, 0), 4683_0_nth_NONNULL(NULL), java.lang.Object(IntList(x0[10], x1[10]))) which results in the following constraint:
(43)    (<=(x0[4], 1)=TRUE∧4619_0_nth_LE(x1[4], x0[4])=4619_0_nth_LE(x1[5], x0[5])∧x3[4]=x3[5]∧4683_0_nth_NONNULL(x1[5])=4683_0_nth_NONNULL(NULL)∧x3[5]=java.lang.Object(IntList(x0[10], x1[10])) ⇒ COND_4619_1_MAIN_INVOKEMETHOD(TRUE, 4619_0_nth_LE(x1[5], x0[5]), x3[5])≥NonInfC∧COND_4619_1_MAIN_INVOKEMETHOD(TRUE, 4619_0_nth_LE(x1[5], x0[5]), x3[5])≥4683_1_MAIN_INVOKEMETHOD(4683_0_nth_NONNULL(x1[5]), x3[5])∧(U^Increasing(4683_1_MAIN_INVOKEMETHOD(4683_0_nth_NONNULL(x1[5]), x3[5])), ≥))

We simplified constraint (43) using rules (I), (II), (III) which results in the following new constraint:
(44)    (<=(x0[4], 1)=TRUE ⇒ COND_4619_1_MAIN_INVOKEMETHOD(TRUE, 4619_0_nth_LE(NULL, x0[4]), java.lang.Object(IntList(x0[10], x1[10])))≥NonInfC∧COND_4619_1_MAIN_INVOKEMETHOD(TRUE, 4619_0_nth_LE(NULL, x0[4]), java.lang.Object(IntList(x0[10], x1[10])))≥4683_1_MAIN_INVOKEMETHOD(4683_0_nth_NONNULL(NULL), java.lang.Object(IntList(x0[10], x1[10])))∧(U^Increasing(4683_1_MAIN_INVOKEMETHOD(4683_0_nth_NONNULL(x1[5]), x3[5])), ≥))

We simplified constraint (44) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(45)    (0 ≥ 0 ⇒ (U^Increasing(4683_1_MAIN_INVOKEMETHOD(4683_0_nth_NONNULL(x1[5]), x3[5])), ≥)∧[(-1)bni_82 + (-1)Bound*bni_82] + [(9)bni_82]x0[10] ≥ 0∧[(-1)bso_83] ≥ 0)

We simplified constraint (45) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(46)    (0 ≥ 0 ⇒ (U^Increasing(4683_1_MAIN_INVOKEMETHOD(4683_0_nth_NONNULL(x1[5]), x3[5])), ≥)∧[(-1)bni_82 + (-1)Bound*bni_82] + [(9)bni_82]x0[10] ≥ 0∧[(-1)bso_83] ≥ 0)

We simplified constraint (46) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(47)    (0 ≥ 0 ⇒ (U^Increasing(4683_1_MAIN_INVOKEMETHOD(4683_0_nth_NONNULL(x1[5]), x3[5])), ≥)∧[(-1)bni_82 + (-1)Bound*bni_82] + [(9)bni_82]x0[10] ≥ 0∧[(-1)bso_83] ≥ 0)

We simplified constraint (47) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:
(48)    (0 ≥ 0 ⇒ (U^Increasing(4683_1_MAIN_INVOKEMETHOD(4683_0_nth_NONNULL(x1[5]), x3[5])), ≥)∧0 ≥ 0∧[(9)bni_82] ≥ 0∧0 ≥ 0∧[(-1)bni_82 + (-1)Bound*bni_82] ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[(-1)bso_83] ≥ 0)

For Pair 4683_1_MAIN_INVOKEMETHOD(4683_0_nth_NONNULL(java.lang.Object(IntList(x0, x1))), java.lang.Object(IntList(x2, x3))) → COND_4683_1_MAIN_INVOKEMETHOD(>(x1, 0), 4683_0_nth_NONNULL(java.lang.Object(IntList(x0, x1))), java.lang.Object(IntList(x2, x3))) the following chains were created:

We consider the chain 4683_1_MAIN_INVOKEMETHOD(4683_0_nth_NONNULL(java.lang.Object(IntList(x0[6], x1[6]))), java.lang.Object(IntList(x2[6], x3[6]))) → COND_4683_1_MAIN_INVOKEMETHOD(>(x1[6], 0), 4683_0_nth_NONNULL(java.lang.Object(IntList(x0[6], x1[6]))), java.lang.Object(IntList(x2[6], x3[6]))), COND_4683_1_MAIN_INVOKEMETHOD(TRUE, 4683_0_nth_NONNULL(java.lang.Object(IntList(x0[7], x1[7]))), java.lang.Object(IntList(x2[7], x3[7]))) → 3247_1_MAIN_INVOKEMETHOD(3247_0_random_ArrayAccess(java.lang.Object(ARRAY(x4[7], x5[7])), x6[7]), x2[7]) which results in the following constraint:
(49)    (>(x1[6], 0)=TRUE∧4683_0_nth_NONNULL(java.lang.Object(IntList(x0[6], x1[6])))=4683_0_nth_NONNULL(java.lang.Object(IntList(x0[7], x1[7])))∧java.lang.Object(IntList(x2[6], x3[6]))=java.lang.Object(IntList(x2[7], x3[7])) ⇒ 4683_1_MAIN_INVOKEMETHOD(4683_0_nth_NONNULL(java.lang.Object(IntList(x0[6], x1[6]))), java.lang.Object(IntList(x2[6], x3[6])))≥NonInfC∧4683_1_MAIN_INVOKEMETHOD(4683_0_nth_NONNULL(java.lang.Object(IntList(x0[6], x1[6]))), java.lang.Object(IntList(x2[6], x3[6])))≥COND_4683_1_MAIN_INVOKEMETHOD(>(x1[6], 0), 4683_0_nth_NONNULL(java.lang.Object(IntList(x0[6], x1[6]))), java.lang.Object(IntList(x2[6], x3[6])))∧(U^Increasing(COND_4683_1_MAIN_INVOKEMETHOD(>(x1[6], 0), 4683_0_nth_NONNULL(java.lang.Object(IntList(x0[6], x1[6]))), java.lang.Object(IntList(x2[6], x3[6])))), ≥))

We simplified constraint (49) using rules (I), (II), (IV) which results in the following new constraint:
(50)    (>(x1[6], 0)=TRUE ⇒ 4683_1_MAIN_INVOKEMETHOD(4683_0_nth_NONNULL(java.lang.Object(IntList(x0[6], x1[6]))), java.lang.Object(IntList(x2[6], x3[6])))≥NonInfC∧4683_1_MAIN_INVOKEMETHOD(4683_0_nth_NONNULL(java.lang.Object(IntList(x0[6], x1[6]))), java.lang.Object(IntList(x2[6], x3[6])))≥COND_4683_1_MAIN_INVOKEMETHOD(>(x1[6], 0), 4683_0_nth_NONNULL(java.lang.Object(IntList(x0[6], x1[6]))), java.lang.Object(IntList(x2[6], x3[6])))∧(U^Increasing(COND_4683_1_MAIN_INVOKEMETHOD(>(x1[6], 0), 4683_0_nth_NONNULL(java.lang.Object(IntList(x0[6], x1[6]))), java.lang.Object(IntList(x2[6], x3[6])))), ≥))

We simplified constraint (50) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(51)    (0 ≥ 0 ⇒ (U^Increasing(COND_4683_1_MAIN_INVOKEMETHOD(>(x1[6], 0), 4683_0_nth_NONNULL(java.lang.Object(IntList(x0[6], x1[6]))), java.lang.Object(IntList(x2[6], x3[6])))), ≥)∧[(-1)bni_84 + (-1)Bound*bni_84] + [(9)bni_84]x2[6] ≥ 0∧[(-1)bso_85] ≥ 0)

We simplified constraint (51) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(52)    (0 ≥ 0 ⇒ (U^Increasing(COND_4683_1_MAIN_INVOKEMETHOD(>(x1[6], 0), 4683_0_nth_NONNULL(java.lang.Object(IntList(x0[6], x1[6]))), java.lang.Object(IntList(x2[6], x3[6])))), ≥)∧[(-1)bni_84 + (-1)Bound*bni_84] + [(9)bni_84]x2[6] ≥ 0∧[(-1)bso_85] ≥ 0)

We simplified constraint (52) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(53)    (0 ≥ 0 ⇒ (U^Increasing(COND_4683_1_MAIN_INVOKEMETHOD(>(x1[6], 0), 4683_0_nth_NONNULL(java.lang.Object(IntList(x0[6], x1[6]))), java.lang.Object(IntList(x2[6], x3[6])))), ≥)∧[(-1)bni_84 + (-1)Bound*bni_84] + [(9)bni_84]x2[6] ≥ 0∧[(-1)bso_85] ≥ 0)

We simplified constraint (53) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:
(54)    (0 ≥ 0 ⇒ (U^Increasing(COND_4683_1_MAIN_INVOKEMETHOD(>(x1[6], 0), 4683_0_nth_NONNULL(java.lang.Object(IntList(x0[6], x1[6]))), java.lang.Object(IntList(x2[6], x3[6])))), ≥)∧0 ≥ 0∧[(9)bni_84] ≥ 0∧0 ≥ 0∧0 ≥ 0∧[(-1)bni_84 + (-1)Bound*bni_84] ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[(-1)bso_85] ≥ 0)

For Pair COND_4683_1_MAIN_INVOKEMETHOD(TRUE, 4683_0_nth_NONNULL(java.lang.Object(IntList(x0, x1))), java.lang.Object(IntList(x2, x3))) → 3247_1_MAIN_INVOKEMETHOD(3247_0_random_ArrayAccess(java.lang.Object(ARRAY(x4, x5)), x6), x2) the following chains were created:

We consider the chain 4683_1_MAIN_INVOKEMETHOD(4683_0_nth_NONNULL(java.lang.Object(IntList(x0[6], x1[6]))), java.lang.Object(IntList(x2[6], x3[6]))) → COND_4683_1_MAIN_INVOKEMETHOD(>(x1[6], 0), 4683_0_nth_NONNULL(java.lang.Object(IntList(x0[6], x1[6]))), java.lang.Object(IntList(x2[6], x3[6]))), COND_4683_1_MAIN_INVOKEMETHOD(TRUE, 4683_0_nth_NONNULL(java.lang.Object(IntList(x0[7], x1[7]))), java.lang.Object(IntList(x2[7], x3[7]))) → 3247_1_MAIN_INVOKEMETHOD(3247_0_random_ArrayAccess(java.lang.Object(ARRAY(x4[7], x5[7])), x6[7]), x2[7]), 3247_1_MAIN_INVOKEMETHOD(3247_0_random_ArrayAccess(java.lang.Object(ARRAY(x0[0], x1[0])), x2[0]), x3[0]) → COND_3247_1_MAIN_INVOKEMETHOD(&&(>=(x2[0], 2), <(x2[0], x0[0])), 3247_0_random_ArrayAccess(java.lang.Object(ARRAY(x0[0], x1[0])), x2[0]), x3[0]) which results in the following constraint:
(55)    (>(x1[6], 0)=TRUE∧4683_0_nth_NONNULL(java.lang.Object(IntList(x0[6], x1[6])))=4683_0_nth_NONNULL(java.lang.Object(IntList(x0[7], x1[7])))∧java.lang.Object(IntList(x2[6], x3[6]))=java.lang.Object(IntList(x2[7], x3[7]))∧3247_0_random_ArrayAccess(java.lang.Object(ARRAY(x4[7], x5[7])), x6[7])=3247_0_random_ArrayAccess(java.lang.Object(ARRAY(x0[0], x1[0])), x2[0])∧x2[7]=x3[0] ⇒ COND_4683_1_MAIN_INVOKEMETHOD(TRUE, 4683_0_nth_NONNULL(java.lang.Object(IntList(x0[7], x1[7]))), java.lang.Object(IntList(x2[7], x3[7])))≥NonInfC∧COND_4683_1_MAIN_INVOKEMETHOD(TRUE, 4683_0_nth_NONNULL(java.lang.Object(IntList(x0[7], x1[7]))), java.lang.Object(IntList(x2[7], x3[7])))≥3247_1_MAIN_INVOKEMETHOD(3247_0_random_ArrayAccess(java.lang.Object(ARRAY(x4[7], x5[7])), x6[7]), x2[7])∧(U^Increasing(3247_1_MAIN_INVOKEMETHOD(3247_0_random_ArrayAccess(java.lang.Object(ARRAY(x4[7], x5[7])), x6[7]), x2[7])), ≥))

We simplified constraint (55) using rules (I), (II), (III), (IV) which results in the following new constraint:
(56)    (>(x1[6], 0)=TRUE ⇒ COND_4683_1_MAIN_INVOKEMETHOD(TRUE, 4683_0_nth_NONNULL(java.lang.Object(IntList(x0[6], x1[6]))), java.lang.Object(IntList(x2[6], x3[6])))≥NonInfC∧COND_4683_1_MAIN_INVOKEMETHOD(TRUE, 4683_0_nth_NONNULL(java.lang.Object(IntList(x0[6], x1[6]))), java.lang.Object(IntList(x2[6], x3[6])))≥3247_1_MAIN_INVOKEMETHOD(3247_0_random_ArrayAccess(java.lang.Object(ARRAY(x4[7], x5[7])), x6[7]), x2[6])∧(U^Increasing(3247_1_MAIN_INVOKEMETHOD(3247_0_random_ArrayAccess(java.lang.Object(ARRAY(x4[7], x5[7])), x6[7]), x2[7])), ≥))

We simplified constraint (56) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(57)    (0 ≥ 0 ⇒ (U^Increasing(3247_1_MAIN_INVOKEMETHOD(3247_0_random_ArrayAccess(java.lang.Object(ARRAY(x4[7], x5[7])), x6[7]), x2[7])), ≥)∧[(-1)bni_86 + (-1)Bound*bni_86] + [(9)bni_86]x2[6] ≥ 0∧[(-1)bso_87] + [7]x2[6] ≥ 0)

We simplified constraint (57) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(58)    (0 ≥ 0 ⇒ (U^Increasing(3247_1_MAIN_INVOKEMETHOD(3247_0_random_ArrayAccess(java.lang.Object(ARRAY(x4[7], x5[7])), x6[7]), x2[7])), ≥)∧[(-1)bni_86 + (-1)Bound*bni_86] + [(9)bni_86]x2[6] ≥ 0∧[(-1)bso_87] + [7]x2[6] ≥ 0)

We simplified constraint (58) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(59)    (0 ≥ 0 ⇒ (U^Increasing(3247_1_MAIN_INVOKEMETHOD(3247_0_random_ArrayAccess(java.lang.Object(ARRAY(x4[7], x5[7])), x6[7]), x2[7])), ≥)∧[(-1)bni_86 + (-1)Bound*bni_86] + [(9)bni_86]x2[6] ≥ 0∧[(-1)bso_87] + [7]x2[6] ≥ 0)

We simplified constraint (59) using rules (IDP_UNRESTRICTED_VARS), (IDP_POLY_GCD) which results in the following new constraint:
(60)    (0 ≥ 0 ⇒ (U^Increasing(3247_1_MAIN_INVOKEMETHOD(3247_0_random_ArrayAccess(java.lang.Object(ARRAY(x4[7], x5[7])), x6[7]), x2[7])), ≥)∧0 ≥ 0∧[(9)bni_86] ≥ 0∧0 ≥ 0∧0 ≥ 0∧[(-1)bni_86 + (-1)Bound*bni_86] ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[(-1)bso_87] ≥ 0∧[1] ≥ 0)

For Pair 4683_1_MAIN_INVOKEMETHOD(4683_0_nth_NONNULL(java.lang.Object(IntList(x0, x1))), java.lang.Object(IntList(x0, x1))) → COND_4683_1_MAIN_INVOKEMETHOD1(>(x1, 0), 4683_0_nth_NONNULL(java.lang.Object(IntList(x0, x1))), java.lang.Object(IntList(x0, x1))) the following chains were created:

We consider the chain 4683_1_MAIN_INVOKEMETHOD(4683_0_nth_NONNULL(java.lang.Object(IntList(x0[8], x1[8]))), java.lang.Object(IntList(x0[8], x1[8]))) → COND_4683_1_MAIN_INVOKEMETHOD1(>(x1[8], 0), 4683_0_nth_NONNULL(java.lang.Object(IntList(x0[8], x1[8]))), java.lang.Object(IntList(x0[8], x1[8]))), COND_4683_1_MAIN_INVOKEMETHOD1(TRUE, 4683_0_nth_NONNULL(java.lang.Object(IntList(x0[9], x1[9]))), java.lang.Object(IntList(x0[9], x1[9]))) → 3247_1_MAIN_INVOKEMETHOD(3247_0_random_ArrayAccess(java.lang.Object(ARRAY(x2[9], x3[9])), x4[9]), x0[9]) which results in the following constraint:
(61)    (>(x1[8], 0)=TRUE∧4683_0_nth_NONNULL(java.lang.Object(IntList(x0[8], x1[8])))=4683_0_nth_NONNULL(java.lang.Object(IntList(x0[9], x1[9])))∧java.lang.Object(IntList(x0[8], x1[8]))=java.lang.Object(IntList(x0[9], x1[9])) ⇒ 4683_1_MAIN_INVOKEMETHOD(4683_0_nth_NONNULL(java.lang.Object(IntList(x0[8], x1[8]))), java.lang.Object(IntList(x0[8], x1[8])))≥NonInfC∧4683_1_MAIN_INVOKEMETHOD(4683_0_nth_NONNULL(java.lang.Object(IntList(x0[8], x1[8]))), java.lang.Object(IntList(x0[8], x1[8])))≥COND_4683_1_MAIN_INVOKEMETHOD1(>(x1[8], 0), 4683_0_nth_NONNULL(java.lang.Object(IntList(x0[8], x1[8]))), java.lang.Object(IntList(x0[8], x1[8])))∧(U^Increasing(COND_4683_1_MAIN_INVOKEMETHOD1(>(x1[8], 0), 4683_0_nth_NONNULL(java.lang.Object(IntList(x0[8], x1[8]))), java.lang.Object(IntList(x0[8], x1[8])))), ≥))

We simplified constraint (61) using rules (I), (II), (IV) which results in the following new constraint:
(62)    (>(x1[8], 0)=TRUE ⇒ 4683_1_MAIN_INVOKEMETHOD(4683_0_nth_NONNULL(java.lang.Object(IntList(x0[8], x1[8]))), java.lang.Object(IntList(x0[8], x1[8])))≥NonInfC∧4683_1_MAIN_INVOKEMETHOD(4683_0_nth_NONNULL(java.lang.Object(IntList(x0[8], x1[8]))), java.lang.Object(IntList(x0[8], x1[8])))≥COND_4683_1_MAIN_INVOKEMETHOD1(>(x1[8], 0), 4683_0_nth_NONNULL(java.lang.Object(IntList(x0[8], x1[8]))), java.lang.Object(IntList(x0[8], x1[8])))∧(U^Increasing(COND_4683_1_MAIN_INVOKEMETHOD1(>(x1[8], 0), 4683_0_nth_NONNULL(java.lang.Object(IntList(x0[8], x1[8]))), java.lang.Object(IntList(x0[8], x1[8])))), ≥))

We simplified constraint (62) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(63)    (0 ≥ 0 ⇒ (U^Increasing(COND_4683_1_MAIN_INVOKEMETHOD1(>(x1[8], 0), 4683_0_nth_NONNULL(java.lang.Object(IntList(x0[8], x1[8]))), java.lang.Object(IntList(x0[8], x1[8])))), ≥)∧[(-1)bni_88 + (-1)Bound*bni_88] + [(9)bni_88]x0[8] ≥ 0∧[(-1)bso_89] ≥ 0)

We simplified constraint (63) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(64)    (0 ≥ 0 ⇒ (U^Increasing(COND_4683_1_MAIN_INVOKEMETHOD1(>(x1[8], 0), 4683_0_nth_NONNULL(java.lang.Object(IntList(x0[8], x1[8]))), java.lang.Object(IntList(x0[8], x1[8])))), ≥)∧[(-1)bni_88 + (-1)Bound*bni_88] + [(9)bni_88]x0[8] ≥ 0∧[(-1)bso_89] ≥ 0)

We simplified constraint (64) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(65)    (0 ≥ 0 ⇒ (U^Increasing(COND_4683_1_MAIN_INVOKEMETHOD1(>(x1[8], 0), 4683_0_nth_NONNULL(java.lang.Object(IntList(x0[8], x1[8]))), java.lang.Object(IntList(x0[8], x1[8])))), ≥)∧[(-1)bni_88 + (-1)Bound*bni_88] + [(9)bni_88]x0[8] ≥ 0∧[(-1)bso_89] ≥ 0)

We simplified constraint (65) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:
(66)    (0 ≥ 0 ⇒ (U^Increasing(COND_4683_1_MAIN_INVOKEMETHOD1(>(x1[8], 0), 4683_0_nth_NONNULL(java.lang.Object(IntList(x0[8], x1[8]))), java.lang.Object(IntList(x0[8], x1[8])))), ≥)∧0 ≥ 0∧[(9)bni_88] ≥ 0∧[(-1)bni_88 + (-1)Bound*bni_88] ≥ 0∧0 ≥ 0∧0 ≥ 0∧[(-1)bso_89] ≥ 0)

For Pair COND_4683_1_MAIN_INVOKEMETHOD1(TRUE, 4683_0_nth_NONNULL(java.lang.Object(IntList(x0, x1))), java.lang.Object(IntList(x0, x1))) → 3247_1_MAIN_INVOKEMETHOD(3247_0_random_ArrayAccess(java.lang.Object(ARRAY(x2, x3)), x4), x0) the following chains were created:

We consider the chain 4683_1_MAIN_INVOKEMETHOD(4683_0_nth_NONNULL(java.lang.Object(IntList(x0[8], x1[8]))), java.lang.Object(IntList(x0[8], x1[8]))) → COND_4683_1_MAIN_INVOKEMETHOD1(>(x1[8], 0), 4683_0_nth_NONNULL(java.lang.Object(IntList(x0[8], x1[8]))), java.lang.Object(IntList(x0[8], x1[8]))), COND_4683_1_MAIN_INVOKEMETHOD1(TRUE, 4683_0_nth_NONNULL(java.lang.Object(IntList(x0[9], x1[9]))), java.lang.Object(IntList(x0[9], x1[9]))) → 3247_1_MAIN_INVOKEMETHOD(3247_0_random_ArrayAccess(java.lang.Object(ARRAY(x2[9], x3[9])), x4[9]), x0[9]), 3247_1_MAIN_INVOKEMETHOD(3247_0_random_ArrayAccess(java.lang.Object(ARRAY(x0[0], x1[0])), x2[0]), x3[0]) → COND_3247_1_MAIN_INVOKEMETHOD(&&(>=(x2[0], 2), <(x2[0], x0[0])), 3247_0_random_ArrayAccess(java.lang.Object(ARRAY(x0[0], x1[0])), x2[0]), x3[0]) which results in the following constraint:
(67)    (>(x1[8], 0)=TRUE∧4683_0_nth_NONNULL(java.lang.Object(IntList(x0[8], x1[8])))=4683_0_nth_NONNULL(java.lang.Object(IntList(x0[9], x1[9])))∧java.lang.Object(IntList(x0[8], x1[8]))=java.lang.Object(IntList(x0[9], x1[9]))∧3247_0_random_ArrayAccess(java.lang.Object(ARRAY(x2[9], x3[9])), x4[9])=3247_0_random_ArrayAccess(java.lang.Object(ARRAY(x0[0], x1[0])), x2[0])∧x0[9]=x3[0] ⇒ COND_4683_1_MAIN_INVOKEMETHOD1(TRUE, 4683_0_nth_NONNULL(java.lang.Object(IntList(x0[9], x1[9]))), java.lang.Object(IntList(x0[9], x1[9])))≥NonInfC∧COND_4683_1_MAIN_INVOKEMETHOD1(TRUE, 4683_0_nth_NONNULL(java.lang.Object(IntList(x0[9], x1[9]))), java.lang.Object(IntList(x0[9], x1[9])))≥3247_1_MAIN_INVOKEMETHOD(3247_0_random_ArrayAccess(java.lang.Object(ARRAY(x2[9], x3[9])), x4[9]), x0[9])∧(U^Increasing(3247_1_MAIN_INVOKEMETHOD(3247_0_random_ArrayAccess(java.lang.Object(ARRAY(x2[9], x3[9])), x4[9]), x0[9])), ≥))

We simplified constraint (67) using rules (I), (II), (III), (IV) which results in the following new constraint:
(68)    (>(x1[8], 0)=TRUE ⇒ COND_4683_1_MAIN_INVOKEMETHOD1(TRUE, 4683_0_nth_NONNULL(java.lang.Object(IntList(x0[8], x1[8]))), java.lang.Object(IntList(x0[8], x1[8])))≥NonInfC∧COND_4683_1_MAIN_INVOKEMETHOD1(TRUE, 4683_0_nth_NONNULL(java.lang.Object(IntList(x0[8], x1[8]))), java.lang.Object(IntList(x0[8], x1[8])))≥3247_1_MAIN_INVOKEMETHOD(3247_0_random_ArrayAccess(java.lang.Object(ARRAY(x2[9], x3[9])), x4[9]), x0[8])∧(U^Increasing(3247_1_MAIN_INVOKEMETHOD(3247_0_random_ArrayAccess(java.lang.Object(ARRAY(x2[9], x3[9])), x4[9]), x0[9])), ≥))

We simplified constraint (68) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(69)    (0 ≥ 0 ⇒ (U^Increasing(3247_1_MAIN_INVOKEMETHOD(3247_0_random_ArrayAccess(java.lang.Object(ARRAY(x2[9], x3[9])), x4[9]), x0[9])), ≥)∧[(-1)bni_90 + (-1)Bound*bni_90] + [(9)bni_90]x0[8] ≥ 0∧[(-1)bso_91] + [7]x0[8] ≥ 0)

We simplified constraint (69) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(70)    (0 ≥ 0 ⇒ (U^Increasing(3247_1_MAIN_INVOKEMETHOD(3247_0_random_ArrayAccess(java.lang.Object(ARRAY(x2[9], x3[9])), x4[9]), x0[9])), ≥)∧[(-1)bni_90 + (-1)Bound*bni_90] + [(9)bni_90]x0[8] ≥ 0∧[(-1)bso_91] + [7]x0[8] ≥ 0)

We simplified constraint (70) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(71)    (0 ≥ 0 ⇒ (U^Increasing(3247_1_MAIN_INVOKEMETHOD(3247_0_random_ArrayAccess(java.lang.Object(ARRAY(x2[9], x3[9])), x4[9]), x0[9])), ≥)∧[(-1)bni_90 + (-1)Bound*bni_90] + [(9)bni_90]x0[8] ≥ 0∧[(-1)bso_91] + [7]x0[8] ≥ 0)

We simplified constraint (71) using rules (IDP_UNRESTRICTED_VARS), (IDP_POLY_GCD) which results in the following new constraint:
(72)    (0 ≥ 0 ⇒ (U^Increasing(3247_1_MAIN_INVOKEMETHOD(3247_0_random_ArrayAccess(java.lang.Object(ARRAY(x2[9], x3[9])), x4[9]), x0[9])), ≥)∧0 ≥ 0∧[(9)bni_90] ≥ 0∧[(-1)bni_90 + (-1)Bound*bni_90] ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[(-1)bso_91] ≥ 0∧[1] ≥ 0)

For Pair 4683_1_MAIN_INVOKEMETHOD(4683_0_nth_NONNULL(NULL), java.lang.Object(IntList(x0, x1))) → COND_4683_1_MAIN_INVOKEMETHOD2(>(0, 0), 4683_0_nth_NONNULL(NULL), java.lang.Object(IntList(x0, x1))) the following chains were created:

We consider the chain 4683_1_MAIN_INVOKEMETHOD(4683_0_nth_NONNULL(NULL), java.lang.Object(IntList(x0[10], x1[10]))) → COND_4683_1_MAIN_INVOKEMETHOD2(>(0, 0), 4683_0_nth_NONNULL(NULL), java.lang.Object(IntList(x0[10], x1[10]))), COND_4683_1_MAIN_INVOKEMETHOD2(TRUE, 4683_0_nth_NONNULL(NULL), java.lang.Object(IntList(x0[11], x1[11]))) → 3247_1_MAIN_INVOKEMETHOD(3247_0_random_ArrayAccess(java.lang.Object(ARRAY(x2[11], x3[11])), x4[11]), x0[11]) which results in the following constraint:
(73) (>(0, 0)=TRUE∧java.lang.Object(IntList(x0[10], x1[10]))=java.lang.Object(IntList(x0[11], x1[11])) ⇒ 4683_1_MAIN_INVOKEMETHOD(4683_0_nth_NONNULL(NULL), java.lang.Object(IntList(x0[10], x1[10])))≥NonInfC∧4683_1_MAIN_INVOKEMETHOD(4683_0_nth_NONNULL(NULL), java.lang.Object(IntList(x0[10], x1[10])))≥COND_4683_1_MAIN_INVOKEMETHOD2(>(0, 0), 4683_0_nth_NONNULL(NULL), java.lang.Object(IntList(x0[10], x1[10])))∧(U^Increasing(COND_4683_1_MAIN_INVOKEMETHOD2(>(0, 0), 4683_0_nth_NONNULL(NULL), java.lang.Object(IntList(x0[10], x1[10])))), ≥))

We solved constraint (73) using rules (I), (II), (IDP_CONSTANT_FOLD).

For Pair COND_4683_1_MAIN_INVOKEMETHOD2(TRUE, 4683_0_nth_NONNULL(NULL), java.lang.Object(IntList(x0, x1))) → 3247_1_MAIN_INVOKEMETHOD(3247_0_random_ArrayAccess(java.lang.Object(ARRAY(x2, x3)), x4), x0) the following chains were created:

We consider the chain 4683_1_MAIN_INVOKEMETHOD(4683_0_nth_NONNULL(NULL), java.lang.Object(IntList(x0[10], x1[10]))) → COND_4683_1_MAIN_INVOKEMETHOD2(>(0, 0), 4683_0_nth_NONNULL(NULL), java.lang.Object(IntList(x0[10], x1[10]))), COND_4683_1_MAIN_INVOKEMETHOD2(TRUE, 4683_0_nth_NONNULL(NULL), java.lang.Object(IntList(x0[11], x1[11]))) → 3247_1_MAIN_INVOKEMETHOD(3247_0_random_ArrayAccess(java.lang.Object(ARRAY(x2[11], x3[11])), x4[11]), x0[11]), 3247_1_MAIN_INVOKEMETHOD(3247_0_random_ArrayAccess(java.lang.Object(ARRAY(x0[0], x1[0])), x2[0]), x3[0]) → COND_3247_1_MAIN_INVOKEMETHOD(&&(>=(x2[0], 2), <(x2[0], x0[0])), 3247_0_random_ArrayAccess(java.lang.Object(ARRAY(x0[0], x1[0])), x2[0]), x3[0]) which results in the following constraint:
(74) (>(0, 0)=TRUE∧java.lang.Object(IntList(x0[10], x1[10]))=java.lang.Object(IntList(x0[11], x1[11]))∧3247_0_random_ArrayAccess(java.lang.Object(ARRAY(x2[11], x3[11])), x4[11])=3247_0_random_ArrayAccess(java.lang.Object(ARRAY(x0[0], x1[0])), x2[0])∧x0[11]=x3[0] ⇒ COND_4683_1_MAIN_INVOKEMETHOD2(TRUE, 4683_0_nth_NONNULL(NULL), java.lang.Object(IntList(x0[11], x1[11])))≥NonInfC∧COND_4683_1_MAIN_INVOKEMETHOD2(TRUE, 4683_0_nth_NONNULL(NULL), java.lang.Object(IntList(x0[11], x1[11])))≥3247_1_MAIN_INVOKEMETHOD(3247_0_random_ArrayAccess(java.lang.Object(ARRAY(x2[11], x3[11])), x4[11]), x0[11])∧(U^Increasing(3247_1_MAIN_INVOKEMETHOD(3247_0_random_ArrayAccess(java.lang.Object(ARRAY(x2[11], x3[11])), x4[11]), x0[11])), ≥))

We solved constraint (74) using rules (I), (II), (IDP_CONSTANT_FOLD).

For Pair 4619_1_MAIN_INVOKEMETHOD(4619_0_nth_LE(java.lang.Object(IntList(x1, x2)), x0), x4) → COND_4619_1_MAIN_INVOKEMETHOD1(>(x0, 1), 4619_0_nth_LE(java.lang.Object(IntList(x1, x2)), x0), x4) the following chains were created:

We consider the chain 4619_1_MAIN_INVOKEMETHOD(4619_0_nth_LE(java.lang.Object(IntList(x1[12], x2[12])), x0[12]), x4[12]) → COND_4619_1_MAIN_INVOKEMETHOD1(>(x0[12], 1), 4619_0_nth_LE(java.lang.Object(IntList(x1[12], x2[12])), x0[12]), x4[12]), COND_4619_1_MAIN_INVOKEMETHOD1(TRUE, 4619_0_nth_LE(java.lang.Object(IntList(x1[13], x2[13])), x0[13]), x4[13]) → 4619_1_MAIN_INVOKEMETHOD(4619_0_nth_LE(x1[13], +(x0[13], -1)), x4[13]) which results in the following constraint:
(75)    (>(x0[12], 1)=TRUE∧4619_0_nth_LE(java.lang.Object(IntList(x1[12], x2[12])), x0[12])=4619_0_nth_LE(java.lang.Object(IntList(x1[13], x2[13])), x0[13])∧x4[12]=x4[13] ⇒ 4619_1_MAIN_INVOKEMETHOD(4619_0_nth_LE(java.lang.Object(IntList(x1[12], x2[12])), x0[12]), x4[12])≥NonInfC∧4619_1_MAIN_INVOKEMETHOD(4619_0_nth_LE(java.lang.Object(IntList(x1[12], x2[12])), x0[12]), x4[12])≥COND_4619_1_MAIN_INVOKEMETHOD1(>(x0[12], 1), 4619_0_nth_LE(java.lang.Object(IntList(x1[12], x2[12])), x0[12]), x4[12])∧(U^Increasing(COND_4619_1_MAIN_INVOKEMETHOD1(>(x0[12], 1), 4619_0_nth_LE(java.lang.Object(IntList(x1[12], x2[12])), x0[12]), x4[12])), ≥))

We simplified constraint (75) using rules (I), (II), (IV) which results in the following new constraint:
(76)    (>(x0[12], 1)=TRUE ⇒ 4619_1_MAIN_INVOKEMETHOD(4619_0_nth_LE(java.lang.Object(IntList(x1[12], x2[12])), x0[12]), x4[12])≥NonInfC∧4619_1_MAIN_INVOKEMETHOD(4619_0_nth_LE(java.lang.Object(IntList(x1[12], x2[12])), x0[12]), x4[12])≥COND_4619_1_MAIN_INVOKEMETHOD1(>(x0[12], 1), 4619_0_nth_LE(java.lang.Object(IntList(x1[12], x2[12])), x0[12]), x4[12])∧(U^Increasing(COND_4619_1_MAIN_INVOKEMETHOD1(>(x0[12], 1), 4619_0_nth_LE(java.lang.Object(IntList(x1[12], x2[12])), x0[12]), x4[12])), ≥))

We simplified constraint (76) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(77)    (0 ≥ 0 ⇒ (U^Increasing(COND_4619_1_MAIN_INVOKEMETHOD1(>(x0[12], 1), 4619_0_nth_LE(java.lang.Object(IntList(x1[12], x2[12])), x0[12]), x4[12])), ≥)∧[(-1)bni_92 + (-1)Bound*bni_92] + [bni_92]x4[12] + [(9)bni_92]x1[12] ≥ 0∧[(-1)bso_93] ≥ 0)

We simplified constraint (77) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(78)    (0 ≥ 0 ⇒ (U^Increasing(COND_4619_1_MAIN_INVOKEMETHOD1(>(x0[12], 1), 4619_0_nth_LE(java.lang.Object(IntList(x1[12], x2[12])), x0[12]), x4[12])), ≥)∧[(-1)bni_92 + (-1)Bound*bni_92] + [bni_92]x4[12] + [(9)bni_92]x1[12] ≥ 0∧[(-1)bso_93] ≥ 0)

We simplified constraint (78) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(79)    (0 ≥ 0 ⇒ (U^Increasing(COND_4619_1_MAIN_INVOKEMETHOD1(>(x0[12], 1), 4619_0_nth_LE(java.lang.Object(IntList(x1[12], x2[12])), x0[12]), x4[12])), ≥)∧[(-1)bni_92 + (-1)Bound*bni_92] + [bni_92]x4[12] + [(9)bni_92]x1[12] ≥ 0∧[(-1)bso_93] ≥ 0)

We simplified constraint (79) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:
(80)    (0 ≥ 0 ⇒ (U^Increasing(COND_4619_1_MAIN_INVOKEMETHOD1(>(x0[12], 1), 4619_0_nth_LE(java.lang.Object(IntList(x1[12], x2[12])), x0[12]), x4[12])), ≥)∧[bni_92] ≥ 0∧0 ≥ 0∧0 ≥ 0∧[(9)bni_92] ≥ 0∧[(-1)bni_92 + (-1)Bound*bni_92] ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[(-1)bso_93] ≥ 0)

For Pair COND_4619_1_MAIN_INVOKEMETHOD1(TRUE, 4619_0_nth_LE(java.lang.Object(IntList(x1, x2)), x0), x4) → 4619_1_MAIN_INVOKEMETHOD(4619_0_nth_LE(x1, +(x0, -1)), x4) the following chains were created:

We consider the chain 4619_1_MAIN_INVOKEMETHOD(4619_0_nth_LE(java.lang.Object(IntList(x1[12], x2[12])), x0[12]), x4[12]) → COND_4619_1_MAIN_INVOKEMETHOD1(>(x0[12], 1), 4619_0_nth_LE(java.lang.Object(IntList(x1[12], x2[12])), x0[12]), x4[12]), COND_4619_1_MAIN_INVOKEMETHOD1(TRUE, 4619_0_nth_LE(java.lang.Object(IntList(x1[13], x2[13])), x0[13]), x4[13]) → 4619_1_MAIN_INVOKEMETHOD(4619_0_nth_LE(x1[13], +(x0[13], -1)), x4[13]) which results in the following constraint:
(81)    (>(x0[12], 1)=TRUE∧4619_0_nth_LE(java.lang.Object(IntList(x1[12], x2[12])), x0[12])=4619_0_nth_LE(java.lang.Object(IntList(x1[13], x2[13])), x0[13])∧x4[12]=x4[13] ⇒ COND_4619_1_MAIN_INVOKEMETHOD1(TRUE, 4619_0_nth_LE(java.lang.Object(IntList(x1[13], x2[13])), x0[13]), x4[13])≥NonInfC∧COND_4619_1_MAIN_INVOKEMETHOD1(TRUE, 4619_0_nth_LE(java.lang.Object(IntList(x1[13], x2[13])), x0[13]), x4[13])≥4619_1_MAIN_INVOKEMETHOD(4619_0_nth_LE(x1[13], +(x0[13], -1)), x4[13])∧(U^Increasing(4619_1_MAIN_INVOKEMETHOD(4619_0_nth_LE(x1[13], +(x0[13], -1)), x4[13])), ≥))

We simplified constraint (81) using rules (I), (II), (III) which results in the following new constraint:
(82)    (>(x0[12], 1)=TRUE ⇒ COND_4619_1_MAIN_INVOKEMETHOD1(TRUE, 4619_0_nth_LE(java.lang.Object(IntList(x1[12], x2[12])), x0[12]), x4[12])≥NonInfC∧COND_4619_1_MAIN_INVOKEMETHOD1(TRUE, 4619_0_nth_LE(java.lang.Object(IntList(x1[12], x2[12])), x0[12]), x4[12])≥4619_1_MAIN_INVOKEMETHOD(4619_0_nth_LE(x1[12], +(x0[12], -1)), x4[12])∧(U^Increasing(4619_1_MAIN_INVOKEMETHOD(4619_0_nth_LE(x1[13], +(x0[13], -1)), x4[13])), ≥))

We simplified constraint (82) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(83)    (0 ≥ 0 ⇒ (U^Increasing(4619_1_MAIN_INVOKEMETHOD(4619_0_nth_LE(x1[13], +(x0[13], -1)), x4[13])), ≥)∧[(-1)bni_94 + (-1)Bound*bni_94] + [bni_94]x4[12] + [(9)bni_94]x1[12] ≥ 0∧[(-1)bso_95] + [8]x1[12] ≥ 0)

We simplified constraint (83) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(84)    (0 ≥ 0 ⇒ (U^Increasing(4619_1_MAIN_INVOKEMETHOD(4619_0_nth_LE(x1[13], +(x0[13], -1)), x4[13])), ≥)∧[(-1)bni_94 + (-1)Bound*bni_94] + [bni_94]x4[12] + [(9)bni_94]x1[12] ≥ 0∧[(-1)bso_95] + [8]x1[12] ≥ 0)

We simplified constraint (84) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(85)    (0 ≥ 0 ⇒ (U^Increasing(4619_1_MAIN_INVOKEMETHOD(4619_0_nth_LE(x1[13], +(x0[13], -1)), x4[13])), ≥)∧[(-1)bni_94 + (-1)Bound*bni_94] + [bni_94]x4[12] + [(9)bni_94]x1[12] ≥ 0∧[(-1)bso_95] + [8]x1[12] ≥ 0)

We simplified constraint (85) using rules (IDP_UNRESTRICTED_VARS), (IDP_POLY_GCD) which results in the following new constraint:
(86)    (0 ≥ 0 ⇒ (U^Increasing(4619_1_MAIN_INVOKEMETHOD(4619_0_nth_LE(x1[13], +(x0[13], -1)), x4[13])), ≥)∧[bni_94] ≥ 0∧0 ≥ 0∧0 ≥ 0∧[(9)bni_94] ≥ 0∧[(-1)bni_94 + (-1)Bound*bni_94] ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[(-1)bso_95] ≥ 0∧[1] ≥ 0)

For Pair 4619_1_MAIN_INVOKEMETHOD(4619_0_nth_LE(java.lang.Object(IntList(x1, x2)), x0), java.lang.Object(IntList(x1, x2))) → COND_4619_1_MAIN_INVOKEMETHOD2(>(x0, 1), 4619_0_nth_LE(java.lang.Object(IntList(x1, x2)), x0), java.lang.Object(IntList(x1, x2))) the following chains were created:

We consider the chain 4619_1_MAIN_INVOKEMETHOD(4619_0_nth_LE(java.lang.Object(IntList(x1[14], x2[14])), x0[14]), java.lang.Object(IntList(x1[14], x2[14]))) → COND_4619_1_MAIN_INVOKEMETHOD2(>(x0[14], 1), 4619_0_nth_LE(java.lang.Object(IntList(x1[14], x2[14])), x0[14]), java.lang.Object(IntList(x1[14], x2[14]))), COND_4619_1_MAIN_INVOKEMETHOD2(TRUE, 4619_0_nth_LE(java.lang.Object(IntList(x1[15], x2[15])), x0[15]), java.lang.Object(IntList(x1[15], x2[15]))) → 4619_1_MAIN_INVOKEMETHOD(4619_0_nth_LE(x1[15], +(x0[15], -1)), java.lang.Object(IntList(x1[15], x2[15]))) which results in the following constraint:
(87)    (>(x0[14], 1)=TRUE∧4619_0_nth_LE(java.lang.Object(IntList(x1[14], x2[14])), x0[14])=4619_0_nth_LE(java.lang.Object(IntList(x1[15], x2[15])), x0[15])∧java.lang.Object(IntList(x1[14], x2[14]))=java.lang.Object(IntList(x1[15], x2[15])) ⇒ 4619_1_MAIN_INVOKEMETHOD(4619_0_nth_LE(java.lang.Object(IntList(x1[14], x2[14])), x0[14]), java.lang.Object(IntList(x1[14], x2[14])))≥NonInfC∧4619_1_MAIN_INVOKEMETHOD(4619_0_nth_LE(java.lang.Object(IntList(x1[14], x2[14])), x0[14]), java.lang.Object(IntList(x1[14], x2[14])))≥COND_4619_1_MAIN_INVOKEMETHOD2(>(x0[14], 1), 4619_0_nth_LE(java.lang.Object(IntList(x1[14], x2[14])), x0[14]), java.lang.Object(IntList(x1[14], x2[14])))∧(U^Increasing(COND_4619_1_MAIN_INVOKEMETHOD2(>(x0[14], 1), 4619_0_nth_LE(java.lang.Object(IntList(x1[14], x2[14])), x0[14]), java.lang.Object(IntList(x1[14], x2[14])))), ≥))

We simplified constraint (87) using rules (I), (II), (IV) which results in the following new constraint:
(88)    (>(x0[14], 1)=TRUE ⇒ 4619_1_MAIN_INVOKEMETHOD(4619_0_nth_LE(java.lang.Object(IntList(x1[14], x2[14])), x0[14]), java.lang.Object(IntList(x1[14], x2[14])))≥NonInfC∧4619_1_MAIN_INVOKEMETHOD(4619_0_nth_LE(java.lang.Object(IntList(x1[14], x2[14])), x0[14]), java.lang.Object(IntList(x1[14], x2[14])))≥COND_4619_1_MAIN_INVOKEMETHOD2(>(x0[14], 1), 4619_0_nth_LE(java.lang.Object(IntList(x1[14], x2[14])), x0[14]), java.lang.Object(IntList(x1[14], x2[14])))∧(U^Increasing(COND_4619_1_MAIN_INVOKEMETHOD2(>(x0[14], 1), 4619_0_nth_LE(java.lang.Object(IntList(x1[14], x2[14])), x0[14]), java.lang.Object(IntList(x1[14], x2[14])))), ≥))

We simplified constraint (88) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(89)    (0 ≥ 0 ⇒ (U^Increasing(COND_4619_1_MAIN_INVOKEMETHOD2(>(x0[14], 1), 4619_0_nth_LE(java.lang.Object(IntList(x1[14], x2[14])), x0[14]), java.lang.Object(IntList(x1[14], x2[14])))), ≥)∧[(-1)bni_96 + (-1)Bound*bni_96] + [(18)bni_96]x1[14] ≥ 0∧[(-1)bso_97] ≥ 0)

We simplified constraint (89) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(90)    (0 ≥ 0 ⇒ (U^Increasing(COND_4619_1_MAIN_INVOKEMETHOD2(>(x0[14], 1), 4619_0_nth_LE(java.lang.Object(IntList(x1[14], x2[14])), x0[14]), java.lang.Object(IntList(x1[14], x2[14])))), ≥)∧[(-1)bni_96 + (-1)Bound*bni_96] + [(18)bni_96]x1[14] ≥ 0∧[(-1)bso_97] ≥ 0)

We simplified constraint (90) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(91)    (0 ≥ 0 ⇒ (U^Increasing(COND_4619_1_MAIN_INVOKEMETHOD2(>(x0[14], 1), 4619_0_nth_LE(java.lang.Object(IntList(x1[14], x2[14])), x0[14]), java.lang.Object(IntList(x1[14], x2[14])))), ≥)∧[(-1)bni_96 + (-1)Bound*bni_96] + [(18)bni_96]x1[14] ≥ 0∧[(-1)bso_97] ≥ 0)

We simplified constraint (91) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:
(92)    (0 ≥ 0 ⇒ (U^Increasing(COND_4619_1_MAIN_INVOKEMETHOD2(>(x0[14], 1), 4619_0_nth_LE(java.lang.Object(IntList(x1[14], x2[14])), x0[14]), java.lang.Object(IntList(x1[14], x2[14])))), ≥)∧0 ≥ 0∧[(18)bni_96] ≥ 0∧0 ≥ 0∧[(-1)bni_96 + (-1)Bound*bni_96] ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[(-1)bso_97] ≥ 0)

For Pair COND_4619_1_MAIN_INVOKEMETHOD2(TRUE, 4619_0_nth_LE(java.lang.Object(IntList(x1, x2)), x0), java.lang.Object(IntList(x1, x2))) → 4619_1_MAIN_INVOKEMETHOD(4619_0_nth_LE(x1, +(x0, -1)), java.lang.Object(IntList(x1, x2))) the following chains were created:

We consider the chain 4619_1_MAIN_INVOKEMETHOD(4619_0_nth_LE(java.lang.Object(IntList(x1[14], x2[14])), x0[14]), java.lang.Object(IntList(x1[14], x2[14]))) → COND_4619_1_MAIN_INVOKEMETHOD2(>(x0[14], 1), 4619_0_nth_LE(java.lang.Object(IntList(x1[14], x2[14])), x0[14]), java.lang.Object(IntList(x1[14], x2[14]))), COND_4619_1_MAIN_INVOKEMETHOD2(TRUE, 4619_0_nth_LE(java.lang.Object(IntList(x1[15], x2[15])), x0[15]), java.lang.Object(IntList(x1[15], x2[15]))) → 4619_1_MAIN_INVOKEMETHOD(4619_0_nth_LE(x1[15], +(x0[15], -1)), java.lang.Object(IntList(x1[15], x2[15]))) which results in the following constraint:
(93)    (>(x0[14], 1)=TRUE∧4619_0_nth_LE(java.lang.Object(IntList(x1[14], x2[14])), x0[14])=4619_0_nth_LE(java.lang.Object(IntList(x1[15], x2[15])), x0[15])∧java.lang.Object(IntList(x1[14], x2[14]))=java.lang.Object(IntList(x1[15], x2[15])) ⇒ COND_4619_1_MAIN_INVOKEMETHOD2(TRUE, 4619_0_nth_LE(java.lang.Object(IntList(x1[15], x2[15])), x0[15]), java.lang.Object(IntList(x1[15], x2[15])))≥NonInfC∧COND_4619_1_MAIN_INVOKEMETHOD2(TRUE, 4619_0_nth_LE(java.lang.Object(IntList(x1[15], x2[15])), x0[15]), java.lang.Object(IntList(x1[15], x2[15])))≥4619_1_MAIN_INVOKEMETHOD(4619_0_nth_LE(x1[15], +(x0[15], -1)), java.lang.Object(IntList(x1[15], x2[15])))∧(U^Increasing(4619_1_MAIN_INVOKEMETHOD(4619_0_nth_LE(x1[15], +(x0[15], -1)), java.lang.Object(IntList(x1[15], x2[15])))), ≥))

We simplified constraint (93) using rules (I), (II), (III) which results in the following new constraint:
(94)    (>(x0[14], 1)=TRUE ⇒ COND_4619_1_MAIN_INVOKEMETHOD2(TRUE, 4619_0_nth_LE(java.lang.Object(IntList(x1[14], x2[14])), x0[14]), java.lang.Object(IntList(x1[14], x2[14])))≥NonInfC∧COND_4619_1_MAIN_INVOKEMETHOD2(TRUE, 4619_0_nth_LE(java.lang.Object(IntList(x1[14], x2[14])), x0[14]), java.lang.Object(IntList(x1[14], x2[14])))≥4619_1_MAIN_INVOKEMETHOD(4619_0_nth_LE(x1[14], +(x0[14], -1)), java.lang.Object(IntList(x1[14], x2[14])))∧(U^Increasing(4619_1_MAIN_INVOKEMETHOD(4619_0_nth_LE(x1[15], +(x0[15], -1)), java.lang.Object(IntList(x1[15], x2[15])))), ≥))

We simplified constraint (94) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(95)    (0 ≥ 0 ⇒ (U^Increasing(4619_1_MAIN_INVOKEMETHOD(4619_0_nth_LE(x1[15], +(x0[15], -1)), java.lang.Object(IntList(x1[15], x2[15])))), ≥)∧[(-1)bni_98 + (-1)Bound*bni_98] + [(18)bni_98]x1[14] ≥ 0∧[(-1)bso_99] + [8]x1[14] ≥ 0)

We simplified constraint (95) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(96)    (0 ≥ 0 ⇒ (U^Increasing(4619_1_MAIN_INVOKEMETHOD(4619_0_nth_LE(x1[15], +(x0[15], -1)), java.lang.Object(IntList(x1[15], x2[15])))), ≥)∧[(-1)bni_98 + (-1)Bound*bni_98] + [(18)bni_98]x1[14] ≥ 0∧[(-1)bso_99] + [8]x1[14] ≥ 0)

We simplified constraint (96) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(97)    (0 ≥ 0 ⇒ (U^Increasing(4619_1_MAIN_INVOKEMETHOD(4619_0_nth_LE(x1[15], +(x0[15], -1)), java.lang.Object(IntList(x1[15], x2[15])))), ≥)∧[(-1)bni_98 + (-1)Bound*bni_98] + [(18)bni_98]x1[14] ≥ 0∧[(-1)bso_99] + [8]x1[14] ≥ 0)

We simplified constraint (97) using rules (IDP_UNRESTRICTED_VARS), (IDP_POLY_GCD) which results in the following new constraint:
(98)    (0 ≥ 0 ⇒ (U^Increasing(4619_1_MAIN_INVOKEMETHOD(4619_0_nth_LE(x1[15], +(x0[15], -1)), java.lang.Object(IntList(x1[15], x2[15])))), ≥)∧0 ≥ 0∧[(18)bni_98] ≥ 0∧0 ≥ 0∧[(-1)bni_98 + (-1)Bound*bni_98] ≥ 0∧0 ≥ 0∧0 ≥ 0∧[(-1)bso_99] ≥ 0∧[1] ≥ 0)

For Pair 4619_1_MAIN_INVOKEMETHOD(4619_0_nth_LE(NULL, x0), x2) → COND_4619_1_MAIN_INVOKEMETHOD3(>(x0, 1), 4619_0_nth_LE(NULL, x0), x2) the following chains were created:

We consider the chain 4619_1_MAIN_INVOKEMETHOD(4619_0_nth_LE(NULL, x0[16]), x2[16]) → COND_4619_1_MAIN_INVOKEMETHOD3(>(x0[16], 1), 4619_0_nth_LE(NULL, x0[16]), x2[16]), COND_4619_1_MAIN_INVOKEMETHOD3(TRUE, 4619_0_nth_LE(NULL, x0[17]), x2[17]) → 4683_1_MAIN_INVOKEMETHOD(4683_0_nth_NONNULL(NULL), x2[17]) which results in the following constraint:
(99)    (>(x0[16], 1)=TRUE∧4619_0_nth_LE(NULL, x0[16])=4619_0_nth_LE(NULL, x0[17])∧x2[16]=x2[17] ⇒ 4619_1_MAIN_INVOKEMETHOD(4619_0_nth_LE(NULL, x0[16]), x2[16])≥NonInfC∧4619_1_MAIN_INVOKEMETHOD(4619_0_nth_LE(NULL, x0[16]), x2[16])≥COND_4619_1_MAIN_INVOKEMETHOD3(>(x0[16], 1), 4619_0_nth_LE(NULL, x0[16]), x2[16])∧(U^Increasing(COND_4619_1_MAIN_INVOKEMETHOD3(>(x0[16], 1), 4619_0_nth_LE(NULL, x0[16]), x2[16])), ≥))

We simplified constraint (99) using rules (I), (II), (IV), (DELETE_TRIVIAL_REDUCESTO) which results in the following new constraint:
(100)    (>(x0[16], 1)=TRUE ⇒ 4619_1_MAIN_INVOKEMETHOD(4619_0_nth_LE(NULL, x0[16]), x2[16])≥NonInfC∧4619_1_MAIN_INVOKEMETHOD(4619_0_nth_LE(NULL, x0[16]), x2[16])≥COND_4619_1_MAIN_INVOKEMETHOD3(>(x0[16], 1), 4619_0_nth_LE(NULL, x0[16]), x2[16])∧(U^Increasing(COND_4619_1_MAIN_INVOKEMETHOD3(>(x0[16], 1), 4619_0_nth_LE(NULL, x0[16]), x2[16])), ≥))

We simplified constraint (100) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(101)    (0 ≥ 0 ⇒ (U^Increasing(COND_4619_1_MAIN_INVOKEMETHOD3(>(x0[16], 1), 4619_0_nth_LE(NULL, x0[16]), x2[16])), ≥)∧[bni_100 + (-1)Bound*bni_100] + [bni_100]x2[16] ≥ 0∧[1 + (-1)bso_101] ≥ 0)

We simplified constraint (101) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(102)    (0 ≥ 0 ⇒ (U^Increasing(COND_4619_1_MAIN_INVOKEMETHOD3(>(x0[16], 1), 4619_0_nth_LE(NULL, x0[16]), x2[16])), ≥)∧[bni_100 + (-1)Bound*bni_100] + [bni_100]x2[16] ≥ 0∧[1 + (-1)bso_101] ≥ 0)

We simplified constraint (102) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(103)    (0 ≥ 0 ⇒ (U^Increasing(COND_4619_1_MAIN_INVOKEMETHOD3(>(x0[16], 1), 4619_0_nth_LE(NULL, x0[16]), x2[16])), ≥)∧[bni_100 + (-1)Bound*bni_100] + [bni_100]x2[16] ≥ 0∧[1 + (-1)bso_101] ≥ 0)

We simplified constraint (103) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:
(104)    (0 ≥ 0 ⇒ (U^Increasing(COND_4619_1_MAIN_INVOKEMETHOD3(>(x0[16], 1), 4619_0_nth_LE(NULL, x0[16]), x2[16])), ≥)∧[bni_100] ≥ 0∧0 ≥ 0∧[bni_100 + (-1)Bound*bni_100] ≥ 0∧0 ≥ 0∧0 ≥ 0∧[1 + (-1)bso_101] ≥ 0)

For Pair COND_4619_1_MAIN_INVOKEMETHOD3(TRUE, 4619_0_nth_LE(NULL, x0), x2) → 4683_1_MAIN_INVOKEMETHOD(4683_0_nth_NONNULL(NULL), x2) the following chains were created:

We consider the chain 4619_1_MAIN_INVOKEMETHOD(4619_0_nth_LE(NULL, x0[16]), x2[16]) → COND_4619_1_MAIN_INVOKEMETHOD3(>(x0[16], 1), 4619_0_nth_LE(NULL, x0[16]), x2[16]), COND_4619_1_MAIN_INVOKEMETHOD3(TRUE, 4619_0_nth_LE(NULL, x0[17]), x2[17]) → 4683_1_MAIN_INVOKEMETHOD(4683_0_nth_NONNULL(NULL), x2[17]), 4683_1_MAIN_INVOKEMETHOD(4683_0_nth_NONNULL(java.lang.Object(IntList(x0[6], x1[6]))), java.lang.Object(IntList(x2[6], x3[6]))) → COND_4683_1_MAIN_INVOKEMETHOD(>(x1[6], 0), 4683_0_nth_NONNULL(java.lang.Object(IntList(x0[6], x1[6]))), java.lang.Object(IntList(x2[6], x3[6]))) which results in the following constraint:
(105) (>(x0[16], 1)=TRUE∧4619_0_nth_LE(NULL, x0[16])=4619_0_nth_LE(NULL, x0[17])∧x2[16]=x2[17]∧4683_0_nth_NONNULL(NULL)=4683_0_nth_NONNULL(java.lang.Object(IntList(x0[6], x1[6])))∧x2[17]=java.lang.Object(IntList(x2[6], x3[6])) ⇒ COND_4619_1_MAIN_INVOKEMETHOD3(TRUE, 4619_0_nth_LE(NULL, x0[17]), x2[17])≥NonInfC∧COND_4619_1_MAIN_INVOKEMETHOD3(TRUE, 4619_0_nth_LE(NULL, x0[17]), x2[17])≥4683_1_MAIN_INVOKEMETHOD(4683_0_nth_NONNULL(NULL), x2[17])∧(U^Increasing(4683_1_MAIN_INVOKEMETHOD(4683_0_nth_NONNULL(NULL), x2[17])), ≥))

We solved constraint (105) using rules (I), (II), (DELETE_TRIVIAL_REDUCESTO).
We consider the chain 4619_1_MAIN_INVOKEMETHOD(4619_0_nth_LE(NULL, x0[16]), x2[16]) → COND_4619_1_MAIN_INVOKEMETHOD3(>(x0[16], 1), 4619_0_nth_LE(NULL, x0[16]), x2[16]), COND_4619_1_MAIN_INVOKEMETHOD3(TRUE, 4619_0_nth_LE(NULL, x0[17]), x2[17]) → 4683_1_MAIN_INVOKEMETHOD(4683_0_nth_NONNULL(NULL), x2[17]), 4683_1_MAIN_INVOKEMETHOD(4683_0_nth_NONNULL(java.lang.Object(IntList(x0[8], x1[8]))), java.lang.Object(IntList(x0[8], x1[8]))) → COND_4683_1_MAIN_INVOKEMETHOD1(>(x1[8], 0), 4683_0_nth_NONNULL(java.lang.Object(IntList(x0[8], x1[8]))), java.lang.Object(IntList(x0[8], x1[8]))) which results in the following constraint:
(106) (>(x0[16], 1)=TRUE∧4619_0_nth_LE(NULL, x0[16])=4619_0_nth_LE(NULL, x0[17])∧x2[16]=x2[17]∧4683_0_nth_NONNULL(NULL)=4683_0_nth_NONNULL(java.lang.Object(IntList(x0[8], x1[8])))∧x2[17]=java.lang.Object(IntList(x0[8], x1[8])) ⇒ COND_4619_1_MAIN_INVOKEMETHOD3(TRUE, 4619_0_nth_LE(NULL, x0[17]), x2[17])≥NonInfC∧COND_4619_1_MAIN_INVOKEMETHOD3(TRUE, 4619_0_nth_LE(NULL, x0[17]), x2[17])≥4683_1_MAIN_INVOKEMETHOD(4683_0_nth_NONNULL(NULL), x2[17])∧(U^Increasing(4683_1_MAIN_INVOKEMETHOD(4683_0_nth_NONNULL(NULL), x2[17])), ≥))

We solved constraint (106) using rules (I), (II), (DELETE_TRIVIAL_REDUCESTO).
We consider the chain 4619_1_MAIN_INVOKEMETHOD(4619_0_nth_LE(NULL, x0[16]), x2[16]) → COND_4619_1_MAIN_INVOKEMETHOD3(>(x0[16], 1), 4619_0_nth_LE(NULL, x0[16]), x2[16]), COND_4619_1_MAIN_INVOKEMETHOD3(TRUE, 4619_0_nth_LE(NULL, x0[17]), x2[17]) → 4683_1_MAIN_INVOKEMETHOD(4683_0_nth_NONNULL(NULL), x2[17]), 4683_1_MAIN_INVOKEMETHOD(4683_0_nth_NONNULL(NULL), java.lang.Object(IntList(x0[10], x1[10]))) → COND_4683_1_MAIN_INVOKEMETHOD2(>(0, 0), 4683_0_nth_NONNULL(NULL), java.lang.Object(IntList(x0[10], x1[10]))) which results in the following constraint:
(107)    (>(x0[16], 1)=TRUE∧4619_0_nth_LE(NULL, x0[16])=4619_0_nth_LE(NULL, x0[17])∧x2[16]=x2[17]∧x2[17]=java.lang.Object(IntList(x0[10], x1[10])) ⇒ COND_4619_1_MAIN_INVOKEMETHOD3(TRUE, 4619_0_nth_LE(NULL, x0[17]), x2[17])≥NonInfC∧COND_4619_1_MAIN_INVOKEMETHOD3(TRUE, 4619_0_nth_LE(NULL, x0[17]), x2[17])≥4683_1_MAIN_INVOKEMETHOD(4683_0_nth_NONNULL(NULL), x2[17])∧(U^Increasing(4683_1_MAIN_INVOKEMETHOD(4683_0_nth_NONNULL(NULL), x2[17])), ≥))

We simplified constraint (107) using rules (I), (II), (III), (DELETE_TRIVIAL_REDUCESTO) which results in the following new constraint:
(108)    (>(x0[16], 1)=TRUE ⇒ COND_4619_1_MAIN_INVOKEMETHOD3(TRUE, 4619_0_nth_LE(NULL, x0[16]), java.lang.Object(IntList(x0[10], x1[10])))≥NonInfC∧COND_4619_1_MAIN_INVOKEMETHOD3(TRUE, 4619_0_nth_LE(NULL, x0[16]), java.lang.Object(IntList(x0[10], x1[10])))≥4683_1_MAIN_INVOKEMETHOD(4683_0_nth_NONNULL(NULL), java.lang.Object(IntList(x0[10], x1[10])))∧(U^Increasing(4683_1_MAIN_INVOKEMETHOD(4683_0_nth_NONNULL(NULL), x2[17])), ≥))

We simplified constraint (108) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(109)    (0 ≥ 0 ⇒ (U^Increasing(4683_1_MAIN_INVOKEMETHOD(4683_0_nth_NONNULL(NULL), x2[17])), ≥)∧[(-1)Bound*bni_102] + [(9)bni_102]x0[10] ≥ 0∧[1 + (-1)bso_103] ≥ 0)

We simplified constraint (109) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(110)    (0 ≥ 0 ⇒ (U^Increasing(4683_1_MAIN_INVOKEMETHOD(4683_0_nth_NONNULL(NULL), x2[17])), ≥)∧[(-1)Bound*bni_102] + [(9)bni_102]x0[10] ≥ 0∧[1 + (-1)bso_103] ≥ 0)

We simplified constraint (110) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(111)    (0 ≥ 0 ⇒ (U^Increasing(4683_1_MAIN_INVOKEMETHOD(4683_0_nth_NONNULL(NULL), x2[17])), ≥)∧[(-1)Bound*bni_102] + [(9)bni_102]x0[10] ≥ 0∧[1 + (-1)bso_103] ≥ 0)

We simplified constraint (111) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:
(112)    (0 ≥ 0 ⇒ (U^Increasing(4683_1_MAIN_INVOKEMETHOD(4683_0_nth_NONNULL(NULL), x2[17])), ≥)∧0 ≥ 0∧[(9)bni_102] ≥ 0∧0 ≥ 0∧[(-1)Bound*bni_102] ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[1 + (-1)bso_103] ≥ 0)

To summarize, we get the following constraints P_≥ for the following pairs.

3247_1_MAIN_INVOKEMETHOD(3247_0_random_ArrayAccess(java.lang.Object(ARRAY(x0, x1)), x2), x3) → COND_3247_1_MAIN_INVOKEMETHOD(&&(>=(x2, 2), <(x2, x0)), 3247_0_random_ArrayAccess(java.lang.Object(ARRAY(x0, x1)), x2), x3)
- (0 ≥ 0 ⇒ (U^Increasing(COND_3247_1_MAIN_INVOKEMETHOD(&&(>=(x2[0], 2), <(x2[0], x0[0])), 3247_0_random_ArrayAccess(java.lang.Object(ARRAY(x0[0], x1[0])), x2[0]), x3[0])), ≥)∧[(2)bni_72] ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[(-1)bni_72 + (-1)Bound*bni_72] ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[(-1)bso_73] ≥ 0)
COND_3247_1_MAIN_INVOKEMETHOD(TRUE, 3247_0_random_ArrayAccess(java.lang.Object(ARRAY(x0, x1)), x2), x3) → 3429_1_MAIN_INVOKEMETHOD(3429_0_random_IntArithmetic(x4, x5), x3)
- (0 ≥ 0 ⇒ (U^Increasing(3429_1_MAIN_INVOKEMETHOD(3429_0_random_IntArithmetic(x4[1], x5[1]), x3[1])), ≥)∧[(2)bni_74] ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[(-1)bni_74 + (-1)Bound*bni_74] ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[(-1)bso_75] ≥ 0)
3429_1_MAIN_INVOKEMETHOD(3429_0_random_IntArithmetic(java.lang.Object(java.lang.String(x0, x1)), x2), x4) → COND_3429_1_MAIN_INVOKEMETHOD(>(x2, 0), 3429_0_random_IntArithmetic(java.lang.Object(java.lang.String(x0, x1)), x2), x4)
- (0 ≥ 0 ⇒ (U^Increasing(COND_3429_1_MAIN_INVOKEMETHOD(>(x2[2], 0), 3429_0_random_IntArithmetic(java.lang.Object(java.lang.String(x0[2], x1[2])), x2[2]), x4[2])), ≥)∧[(2)bni_76] ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[(-1)bni_76 + (-1)Bound*bni_76] ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[(-1)bso_77] ≥ 0)
COND_3429_1_MAIN_INVOKEMETHOD(TRUE, 3429_0_random_IntArithmetic(java.lang.Object(java.lang.String(x0, x1)), x2), x4) → 4619_1_MAIN_INVOKEMETHOD(4619_0_nth_LE(x4, x1), x4)
- (0 ≥ 0 ⇒ (U^Increasing(4619_1_MAIN_INVOKEMETHOD(4619_0_nth_LE(x4[3], x1[3]), x4[3])), ≥)∧[(2)bni_78] ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[(-1)bni_78 + (-1)Bound*bni_78] ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[(-1)bso_79] ≥ 0)
4619_1_MAIN_INVOKEMETHOD(4619_0_nth_LE(x1, x0), x3) → COND_4619_1_MAIN_INVOKEMETHOD(<=(x0, 1), 4619_0_nth_LE(x1, x0), x3)
- (0 ≥ 0 ⇒ (U^Increasing(COND_4619_1_MAIN_INVOKEMETHOD(<=(x0[4], 1), 4619_0_nth_LE(x1[4], x0[4]), x3[4])), ≥)∧[bni_80] ≥ 0∧0 ≥ 0∧[bni_80] ≥ 0∧[(-1)bni_80 + (-1)Bound*bni_80] ≥ 0∧0 ≥ 0∧0 ≥ 0∧[1] ≥ 0∧[(-1)bso_81] ≥ 0)
COND_4619_1_MAIN_INVOKEMETHOD(TRUE, 4619_0_nth_LE(x1, x0), x3) → 4683_1_MAIN_INVOKEMETHOD(4683_0_nth_NONNULL(x1), x3)
- (0 ≥ 0 ⇒ (U^Increasing(4683_1_MAIN_INVOKEMETHOD(4683_0_nth_NONNULL(x1[5]), x3[5])), ≥)∧0 ≥ 0∧[(9)bni_82] ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[(-1)bni_82 + (-1)Bound*bni_82] ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[(-1)bso_83] ≥ 0)
- (0 ≥ 0 ⇒ (U^Increasing(4683_1_MAIN_INVOKEMETHOD(4683_0_nth_NONNULL(x1[5]), x3[5])), ≥)∧0 ≥ 0∧[(9)bni_82] ≥ 0∧0 ≥ 0∧[(-1)bni_82 + (-1)Bound*bni_82] ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[(-1)bso_83] ≥ 0)
- (0 ≥ 0 ⇒ (U^Increasing(4683_1_MAIN_INVOKEMETHOD(4683_0_nth_NONNULL(x1[5]), x3[5])), ≥)∧0 ≥ 0∧[(9)bni_82] ≥ 0∧0 ≥ 0∧[(-1)bni_82 + (-1)Bound*bni_82] ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[(-1)bso_83] ≥ 0)
4683_1_MAIN_INVOKEMETHOD(4683_0_nth_NONNULL(java.lang.Object(IntList(x0, x1))), java.lang.Object(IntList(x2, x3))) → COND_4683_1_MAIN_INVOKEMETHOD(>(x1, 0), 4683_0_nth_NONNULL(java.lang.Object(IntList(x0, x1))), java.lang.Object(IntList(x2, x3)))
- (0 ≥ 0 ⇒ (U^Increasing(COND_4683_1_MAIN_INVOKEMETHOD(>(x1[6], 0), 4683_0_nth_NONNULL(java.lang.Object(IntList(x0[6], x1[6]))), java.lang.Object(IntList(x2[6], x3[6])))), ≥)∧0 ≥ 0∧[(9)bni_84] ≥ 0∧0 ≥ 0∧0 ≥ 0∧[(-1)bni_84 + (-1)Bound*bni_84] ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[(-1)bso_85] ≥ 0)
COND_4683_1_MAIN_INVOKEMETHOD(TRUE, 4683_0_nth_NONNULL(java.lang.Object(IntList(x0, x1))), java.lang.Object(IntList(x2, x3))) → 3247_1_MAIN_INVOKEMETHOD(3247_0_random_ArrayAccess(java.lang.Object(ARRAY(x4, x5)), x6), x2)
- (0 ≥ 0 ⇒ (U^Increasing(3247_1_MAIN_INVOKEMETHOD(3247_0_random_ArrayAccess(java.lang.Object(ARRAY(x4[7], x5[7])), x6[7]), x2[7])), ≥)∧0 ≥ 0∧[(9)bni_86] ≥ 0∧0 ≥ 0∧0 ≥ 0∧[(-1)bni_86 + (-1)Bound*bni_86] ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[(-1)bso_87] ≥ 0∧[1] ≥ 0)
4683_1_MAIN_INVOKEMETHOD(4683_0_nth_NONNULL(java.lang.Object(IntList(x0, x1))), java.lang.Object(IntList(x0, x1))) → COND_4683_1_MAIN_INVOKEMETHOD1(>(x1, 0), 4683_0_nth_NONNULL(java.lang.Object(IntList(x0, x1))), java.lang.Object(IntList(x0, x1)))
- (0 ≥ 0 ⇒ (U^Increasing(COND_4683_1_MAIN_INVOKEMETHOD1(>(x1[8], 0), 4683_0_nth_NONNULL(java.lang.Object(IntList(x0[8], x1[8]))), java.lang.Object(IntList(x0[8], x1[8])))), ≥)∧0 ≥ 0∧[(9)bni_88] ≥ 0∧[(-1)bni_88 + (-1)Bound*bni_88] ≥ 0∧0 ≥ 0∧0 ≥ 0∧[(-1)bso_89] ≥ 0)
COND_4683_1_MAIN_INVOKEMETHOD1(TRUE, 4683_0_nth_NONNULL(java.lang.Object(IntList(x0, x1))), java.lang.Object(IntList(x0, x1))) → 3247_1_MAIN_INVOKEMETHOD(3247_0_random_ArrayAccess(java.lang.Object(ARRAY(x2, x3)), x4), x0)
- (0 ≥ 0 ⇒ (U^Increasing(3247_1_MAIN_INVOKEMETHOD(3247_0_random_ArrayAccess(java.lang.Object(ARRAY(x2[9], x3[9])), x4[9]), x0[9])), ≥)∧0 ≥ 0∧[(9)bni_90] ≥ 0∧[(-1)bni_90 + (-1)Bound*bni_90] ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[(-1)bso_91] ≥ 0∧[1] ≥ 0)
4683_1_MAIN_INVOKEMETHOD(4683_0_nth_NONNULL(NULL), java.lang.Object(IntList(x0, x1))) → COND_4683_1_MAIN_INVOKEMETHOD2(>(0, 0), 4683_0_nth_NONNULL(NULL), java.lang.Object(IntList(x0, x1)))
COND_4683_1_MAIN_INVOKEMETHOD2(TRUE, 4683_0_nth_NONNULL(NULL), java.lang.Object(IntList(x0, x1))) → 3247_1_MAIN_INVOKEMETHOD(3247_0_random_ArrayAccess(java.lang.Object(ARRAY(x2, x3)), x4), x0)
4619_1_MAIN_INVOKEMETHOD(4619_0_nth_LE(java.lang.Object(IntList(x1, x2)), x0), x4) → COND_4619_1_MAIN_INVOKEMETHOD1(>(x0, 1), 4619_0_nth_LE(java.lang.Object(IntList(x1, x2)), x0), x4)
- (0 ≥ 0 ⇒ (U^Increasing(COND_4619_1_MAIN_INVOKEMETHOD1(>(x0[12], 1), 4619_0_nth_LE(java.lang.Object(IntList(x1[12], x2[12])), x0[12]), x4[12])), ≥)∧[bni_92] ≥ 0∧0 ≥ 0∧0 ≥ 0∧[(9)bni_92] ≥ 0∧[(-1)bni_92 + (-1)Bound*bni_92] ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[(-1)bso_93] ≥ 0)
COND_4619_1_MAIN_INVOKEMETHOD1(TRUE, 4619_0_nth_LE(java.lang.Object(IntList(x1, x2)), x0), x4) → 4619_1_MAIN_INVOKEMETHOD(4619_0_nth_LE(x1, +(x0, -1)), x4)
- (0 ≥ 0 ⇒ (U^Increasing(4619_1_MAIN_INVOKEMETHOD(4619_0_nth_LE(x1[13], +(x0[13], -1)), x4[13])), ≥)∧[bni_94] ≥ 0∧0 ≥ 0∧0 ≥ 0∧[(9)bni_94] ≥ 0∧[(-1)bni_94 + (-1)Bound*bni_94] ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[(-1)bso_95] ≥ 0∧[1] ≥ 0)
4619_1_MAIN_INVOKEMETHOD(4619_0_nth_LE(java.lang.Object(IntList(x1, x2)), x0), java.lang.Object(IntList(x1, x2))) → COND_4619_1_MAIN_INVOKEMETHOD2(>(x0, 1), 4619_0_nth_LE(java.lang.Object(IntList(x1, x2)), x0), java.lang.Object(IntList(x1, x2)))
- (0 ≥ 0 ⇒ (U^Increasing(COND_4619_1_MAIN_INVOKEMETHOD2(>(x0[14], 1), 4619_0_nth_LE(java.lang.Object(IntList(x1[14], x2[14])), x0[14]), java.lang.Object(IntList(x1[14], x2[14])))), ≥)∧0 ≥ 0∧[(18)bni_96] ≥ 0∧0 ≥ 0∧[(-1)bni_96 + (-1)Bound*bni_96] ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[(-1)bso_97] ≥ 0)
COND_4619_1_MAIN_INVOKEMETHOD2(TRUE, 4619_0_nth_LE(java.lang.Object(IntList(x1, x2)), x0), java.lang.Object(IntList(x1, x2))) → 4619_1_MAIN_INVOKEMETHOD(4619_0_nth_LE(x1, +(x0, -1)), java.lang.Object(IntList(x1, x2)))
- (0 ≥ 0 ⇒ (U^Increasing(4619_1_MAIN_INVOKEMETHOD(4619_0_nth_LE(x1[15], +(x0[15], -1)), java.lang.Object(IntList(x1[15], x2[15])))), ≥)∧0 ≥ 0∧[(18)bni_98] ≥ 0∧0 ≥ 0∧[(-1)bni_98 + (-1)Bound*bni_98] ≥ 0∧0 ≥ 0∧0 ≥ 0∧[(-1)bso_99] ≥ 0∧[1] ≥ 0)
4619_1_MAIN_INVOKEMETHOD(4619_0_nth_LE(NULL, x0), x2) → COND_4619_1_MAIN_INVOKEMETHOD3(>(x0, 1), 4619_0_nth_LE(NULL, x0), x2)
- (0 ≥ 0 ⇒ (U^Increasing(COND_4619_1_MAIN_INVOKEMETHOD3(>(x0[16], 1), 4619_0_nth_LE(NULL, x0[16]), x2[16])), ≥)∧[bni_100] ≥ 0∧0 ≥ 0∧[bni_100 + (-1)Bound*bni_100] ≥ 0∧0 ≥ 0∧0 ≥ 0∧[1 + (-1)bso_101] ≥ 0)
COND_4619_1_MAIN_INVOKEMETHOD3(TRUE, 4619_0_nth_LE(NULL, x0), x2) → 4683_1_MAIN_INVOKEMETHOD(4683_0_nth_NONNULL(NULL), x2)
- (0 ≥ 0 ⇒ (U^Increasing(4683_1_MAIN_INVOKEMETHOD(4683_0_nth_NONNULL(NULL), x2[17])), ≥)∧0 ≥ 0∧[(9)bni_102] ≥ 0∧0 ≥ 0∧[(-1)Bound*bni_102] ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[1 + (-1)bso_103] ≥ 0)

POL(TRUE) = 0
POL(FALSE) = 0
POL(3247_1_MAIN_INVOKEMETHOD(x₁, x₂)) = [-1] + [2]x₂ + [-1]x₁
POL(3247_0_random_ArrayAccess(x₁, x₂)) = 0
POL(java.lang.Object(x₁)) = [3]x₁
POL(ARRAY(x₁, x₂)) = 0
POL(COND_3247_1_MAIN_INVOKEMETHOD(x₁, x₂, x₃)) = [-1] + [2]x₃ + [-1]x₂
POL(&&(x₁, x₂)) = 0
POL(>=(x₁, x₂)) = 0
POL(2) = 0
POL(<(x₁, x₂)) = 0
POL(3429_1_MAIN_INVOKEMETHOD(x₁, x₂)) = [-1] + [2]x₂ + [-1]x₁
POL(3429_0_random_IntArithmetic(x₁, x₂)) = 0
POL(java.lang.String(x₁, x₂)) = 0
POL(COND_3429_1_MAIN_INVOKEMETHOD(x₁, x₂, x₃)) = [-1] + [2]x₃ + [-1]x₂
POL(>(x₁, x₂)) = 0
POL(0) = 0
POL(4619_1_MAIN_INVOKEMETHOD(x₁, x₂)) = [-1] + x₂ + x₁
POL(4619_0_nth_LE(x₁, x₂)) = x₁
POL(COND_4619_1_MAIN_INVOKEMETHOD(x₁, x₂, x₃)) = [-1] + x₃
POL(<=(x₁, x₂)) = 0
POL(1) = 0
POL(4683_1_MAIN_INVOKEMETHOD(x₁, x₂)) = [-1] + x₂ + [-1]x₁
POL(4683_0_nth_NONNULL(x₁)) = 0
POL(IntList(x₁, x₂)) = [3]x₁
POL(COND_4683_1_MAIN_INVOKEMETHOD(x₁, x₂, x₃)) = [-1] + x₃ + [-1]x₂
POL(COND_4683_1_MAIN_INVOKEMETHOD1(x₁, x₂, x₃)) = [-1] + x₃ + [-1]x₂
POL(NULL) = [2]
POL(COND_4683_1_MAIN_INVOKEMETHOD2(x₁, x₂, x₃)) = [-1] + [-1]x₃ + [-1]x₂ + [-1]x₁
POL(COND_4619_1_MAIN_INVOKEMETHOD1(x₁, x₂, x₃)) = [-1] + x₃ + x₂
POL(+(x₁, x₂)) = 0
POL(-1) = 0
POL(COND_4619_1_MAIN_INVOKEMETHOD2(x₁, x₂, x₃)) = [-1] + [2]x₃
POL(COND_4619_1_MAIN_INVOKEMETHOD3(x₁, x₂, x₃)) = [2] + x₃ + [-1]x₂

The following pairs are in P_>:

4683_1_MAIN_INVOKEMETHOD(4683_0_nth_NONNULL(NULL), java.lang.Object(IntList(x0[10], x1[10]))) → COND_4683_1_MAIN_INVOKEMETHOD2(>(0, 0), 4683_0_nth_NONNULL(NULL), java.lang.Object(IntList(x0[10], x1[10])))
COND_4683_1_MAIN_INVOKEMETHOD2(TRUE, 4683_0_nth_NONNULL(NULL), java.lang.Object(IntList(x0[11], x1[11]))) → 3247_1_MAIN_INVOKEMETHOD(3247_0_random_ArrayAccess(java.lang.Object(ARRAY(x2[11], x3[11])), x4[11]), x0[11])
4619_1_MAIN_INVOKEMETHOD(4619_0_nth_LE(NULL, x0[16]), x2[16]) → COND_4619_1_MAIN_INVOKEMETHOD3(>(x0[16], 1), 4619_0_nth_LE(NULL, x0[16]), x2[16])
COND_4619_1_MAIN_INVOKEMETHOD3(TRUE, 4619_0_nth_LE(NULL, x0[17]), x2[17]) → 4683_1_MAIN_INVOKEMETHOD(4683_0_nth_NONNULL(NULL), x2[17])

The following pairs are in P_bound:

3247_1_MAIN_INVOKEMETHOD(3247_0_random_ArrayAccess(java.lang.Object(ARRAY(x0[0], x1[0])), x2[0]), x3[0]) → COND_3247_1_MAIN_INVOKEMETHOD(&&(>=(x2[0], 2), <(x2[0], x0[0])), 3247_0_random_ArrayAccess(java.lang.Object(ARRAY(x0[0], x1[0])), x2[0]), x3[0])
COND_3247_1_MAIN_INVOKEMETHOD(TRUE, 3247_0_random_ArrayAccess(java.lang.Object(ARRAY(x0[1], x1[1])), x2[1]), x3[1]) → 3429_1_MAIN_INVOKEMETHOD(3429_0_random_IntArithmetic(x4[1], x5[1]), x3[1])
3429_1_MAIN_INVOKEMETHOD(3429_0_random_IntArithmetic(java.lang.Object(java.lang.String(x0[2], x1[2])), x2[2]), x4[2]) → COND_3429_1_MAIN_INVOKEMETHOD(>(x2[2], 0), 3429_0_random_IntArithmetic(java.lang.Object(java.lang.String(x0[2], x1[2])), x2[2]), x4[2])
COND_3429_1_MAIN_INVOKEMETHOD(TRUE, 3429_0_random_IntArithmetic(java.lang.Object(java.lang.String(x0[3], x1[3])), x2[3]), x4[3]) → 4619_1_MAIN_INVOKEMETHOD(4619_0_nth_LE(x4[3], x1[3]), x4[3])
4619_1_MAIN_INVOKEMETHOD(4619_0_nth_LE(x1[4], x0[4]), x3[4]) → COND_4619_1_MAIN_INVOKEMETHOD(<=(x0[4], 1), 4619_0_nth_LE(x1[4], x0[4]), x3[4])
COND_4619_1_MAIN_INVOKEMETHOD(TRUE, 4619_0_nth_LE(x1[5], x0[5]), x3[5]) → 4683_1_MAIN_INVOKEMETHOD(4683_0_nth_NONNULL(x1[5]), x3[5])
4683_1_MAIN_INVOKEMETHOD(4683_0_nth_NONNULL(java.lang.Object(IntList(x0[6], x1[6]))), java.lang.Object(IntList(x2[6], x3[6]))) → COND_4683_1_MAIN_INVOKEMETHOD(>(x1[6], 0), 4683_0_nth_NONNULL(java.lang.Object(IntList(x0[6], x1[6]))), java.lang.Object(IntList(x2[6], x3[6])))
COND_4683_1_MAIN_INVOKEMETHOD(TRUE, 4683_0_nth_NONNULL(java.lang.Object(IntList(x0[7], x1[7]))), java.lang.Object(IntList(x2[7], x3[7]))) → 3247_1_MAIN_INVOKEMETHOD(3247_0_random_ArrayAccess(java.lang.Object(ARRAY(x4[7], x5[7])), x6[7]), x2[7])
4683_1_MAIN_INVOKEMETHOD(4683_0_nth_NONNULL(java.lang.Object(IntList(x0[8], x1[8]))), java.lang.Object(IntList(x0[8], x1[8]))) → COND_4683_1_MAIN_INVOKEMETHOD1(>(x1[8], 0), 4683_0_nth_NONNULL(java.lang.Object(IntList(x0[8], x1[8]))), java.lang.Object(IntList(x0[8], x1[8])))
COND_4683_1_MAIN_INVOKEMETHOD1(TRUE, 4683_0_nth_NONNULL(java.lang.Object(IntList(x0[9], x1[9]))), java.lang.Object(IntList(x0[9], x1[9]))) → 3247_1_MAIN_INVOKEMETHOD(3247_0_random_ArrayAccess(java.lang.Object(ARRAY(x2[9], x3[9])), x4[9]), x0[9])
4683_1_MAIN_INVOKEMETHOD(4683_0_nth_NONNULL(NULL), java.lang.Object(IntList(x0[10], x1[10]))) → COND_4683_1_MAIN_INVOKEMETHOD2(>(0, 0), 4683_0_nth_NONNULL(NULL), java.lang.Object(IntList(x0[10], x1[10])))
COND_4683_1_MAIN_INVOKEMETHOD2(TRUE, 4683_0_nth_NONNULL(NULL), java.lang.Object(IntList(x0[11], x1[11]))) → 3247_1_MAIN_INVOKEMETHOD(3247_0_random_ArrayAccess(java.lang.Object(ARRAY(x2[11], x3[11])), x4[11]), x0[11])
4619_1_MAIN_INVOKEMETHOD(4619_0_nth_LE(java.lang.Object(IntList(x1[12], x2[12])), x0[12]), x4[12]) → COND_4619_1_MAIN_INVOKEMETHOD1(>(x0[12], 1), 4619_0_nth_LE(java.lang.Object(IntList(x1[12], x2[12])), x0[12]), x4[12])
COND_4619_1_MAIN_INVOKEMETHOD1(TRUE, 4619_0_nth_LE(java.lang.Object(IntList(x1[13], x2[13])), x0[13]), x4[13]) → 4619_1_MAIN_INVOKEMETHOD(4619_0_nth_LE(x1[13], +(x0[13], -1)), x4[13])
4619_1_MAIN_INVOKEMETHOD(4619_0_nth_LE(java.lang.Object(IntList(x1[14], x2[14])), x0[14]), java.lang.Object(IntList(x1[14], x2[14]))) → COND_4619_1_MAIN_INVOKEMETHOD2(>(x0[14], 1), 4619_0_nth_LE(java.lang.Object(IntList(x1[14], x2[14])), x0[14]), java.lang.Object(IntList(x1[14], x2[14])))
COND_4619_1_MAIN_INVOKEMETHOD2(TRUE, 4619_0_nth_LE(java.lang.Object(IntList(x1[15], x2[15])), x0[15]), java.lang.Object(IntList(x1[15], x2[15]))) → 4619_1_MAIN_INVOKEMETHOD(4619_0_nth_LE(x1[15], +(x0[15], -1)), java.lang.Object(IntList(x1[15], x2[15])))
4619_1_MAIN_INVOKEMETHOD(4619_0_nth_LE(NULL, x0[16]), x2[16]) → COND_4619_1_MAIN_INVOKEMETHOD3(>(x0[16], 1), 4619_0_nth_LE(NULL, x0[16]), x2[16])
COND_4619_1_MAIN_INVOKEMETHOD3(TRUE, 4619_0_nth_LE(NULL, x0[17]), x2[17]) → 4683_1_MAIN_INVOKEMETHOD(4683_0_nth_NONNULL(NULL), x2[17])

The following pairs are in P_≥:

3247_1_MAIN_INVOKEMETHOD(3247_0_random_ArrayAccess(java.lang.Object(ARRAY(x0[0], x1[0])), x2[0]), x3[0]) → COND_3247_1_MAIN_INVOKEMETHOD(&&(>=(x2[0], 2), <(x2[0], x0[0])), 3247_0_random_ArrayAccess(java.lang.Object(ARRAY(x0[0], x1[0])), x2[0]), x3[0])
COND_3247_1_MAIN_INVOKEMETHOD(TRUE, 3247_0_random_ArrayAccess(java.lang.Object(ARRAY(x0[1], x1[1])), x2[1]), x3[1]) → 3429_1_MAIN_INVOKEMETHOD(3429_0_random_IntArithmetic(x4[1], x5[1]), x3[1])
3429_1_MAIN_INVOKEMETHOD(3429_0_random_IntArithmetic(java.lang.Object(java.lang.String(x0[2], x1[2])), x2[2]), x4[2]) → COND_3429_1_MAIN_INVOKEMETHOD(>(x2[2], 0), 3429_0_random_IntArithmetic(java.lang.Object(java.lang.String(x0[2], x1[2])), x2[2]), x4[2])
COND_3429_1_MAIN_INVOKEMETHOD(TRUE, 3429_0_random_IntArithmetic(java.lang.Object(java.lang.String(x0[3], x1[3])), x2[3]), x4[3]) → 4619_1_MAIN_INVOKEMETHOD(4619_0_nth_LE(x4[3], x1[3]), x4[3])
4619_1_MAIN_INVOKEMETHOD(4619_0_nth_LE(x1[4], x0[4]), x3[4]) → COND_4619_1_MAIN_INVOKEMETHOD(<=(x0[4], 1), 4619_0_nth_LE(x1[4], x0[4]), x3[4])
COND_4619_1_MAIN_INVOKEMETHOD(TRUE, 4619_0_nth_LE(x1[5], x0[5]), x3[5]) → 4683_1_MAIN_INVOKEMETHOD(4683_0_nth_NONNULL(x1[5]), x3[5])
4683_1_MAIN_INVOKEMETHOD(4683_0_nth_NONNULL(java.lang.Object(IntList(x0[6], x1[6]))), java.lang.Object(IntList(x2[6], x3[6]))) → COND_4683_1_MAIN_INVOKEMETHOD(>(x1[6], 0), 4683_0_nth_NONNULL(java.lang.Object(IntList(x0[6], x1[6]))), java.lang.Object(IntList(x2[6], x3[6])))
COND_4683_1_MAIN_INVOKEMETHOD(TRUE, 4683_0_nth_NONNULL(java.lang.Object(IntList(x0[7], x1[7]))), java.lang.Object(IntList(x2[7], x3[7]))) → 3247_1_MAIN_INVOKEMETHOD(3247_0_random_ArrayAccess(java.lang.Object(ARRAY(x4[7], x5[7])), x6[7]), x2[7])
4683_1_MAIN_INVOKEMETHOD(4683_0_nth_NONNULL(java.lang.Object(IntList(x0[8], x1[8]))), java.lang.Object(IntList(x0[8], x1[8]))) → COND_4683_1_MAIN_INVOKEMETHOD1(>(x1[8], 0), 4683_0_nth_NONNULL(java.lang.Object(IntList(x0[8], x1[8]))), java.lang.Object(IntList(x0[8], x1[8])))
COND_4683_1_MAIN_INVOKEMETHOD1(TRUE, 4683_0_nth_NONNULL(java.lang.Object(IntList(x0[9], x1[9]))), java.lang.Object(IntList(x0[9], x1[9]))) → 3247_1_MAIN_INVOKEMETHOD(3247_0_random_ArrayAccess(java.lang.Object(ARRAY(x2[9], x3[9])), x4[9]), x0[9])
4619_1_MAIN_INVOKEMETHOD(4619_0_nth_LE(java.lang.Object(IntList(x1[12], x2[12])), x0[12]), x4[12]) → COND_4619_1_MAIN_INVOKEMETHOD1(>(x0[12], 1), 4619_0_nth_LE(java.lang.Object(IntList(x1[12], x2[12])), x0[12]), x4[12])
COND_4619_1_MAIN_INVOKEMETHOD1(TRUE, 4619_0_nth_LE(java.lang.Object(IntList(x1[13], x2[13])), x0[13]), x4[13]) → 4619_1_MAIN_INVOKEMETHOD(4619_0_nth_LE(x1[13], +(x0[13], -1)), x4[13])
4619_1_MAIN_INVOKEMETHOD(4619_0_nth_LE(java.lang.Object(IntList(x1[14], x2[14])), x0[14]), java.lang.Object(IntList(x1[14], x2[14]))) → COND_4619_1_MAIN_INVOKEMETHOD2(>(x0[14], 1), 4619_0_nth_LE(java.lang.Object(IntList(x1[14], x2[14])), x0[14]), java.lang.Object(IntList(x1[14], x2[14])))
COND_4619_1_MAIN_INVOKEMETHOD2(TRUE, 4619_0_nth_LE(java.lang.Object(IntList(x1[15], x2[15])), x0[15]), java.lang.Object(IntList(x1[15], x2[15]))) → 4619_1_MAIN_INVOKEMETHOD(4619_0_nth_LE(x1[15], +(x0[15], -1)), java.lang.Object(IntList(x1[15], x2[15])))

There are no usable rules.

(16) Obligation:

IDP problem:
The following function symbols are pre-defined:

!=	~	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

The following domains are used:

Boolean, Integer

R is empty.

The integer pair graph contains the following rules and edges:
(0): 3247_1_MAIN_INVOKEMETHOD(3247_0_random_ArrayAccess(java.lang.Object(ARRAY(x0[0], x1[0])), x2[0]), x3[0]) → COND_3247_1_MAIN_INVOKEMETHOD(x2[0] >= 2 && x2[0] < x0[0], 3247_0_random_ArrayAccess(java.lang.Object(ARRAY(x0[0], x1[0])), x2[0]), x3[0])
(1): COND_3247_1_MAIN_INVOKEMETHOD(TRUE, 3247_0_random_ArrayAccess(java.lang.Object(ARRAY(x0[1], x1[1])), x2[1]), x3[1]) → 3429_1_MAIN_INVOKEMETHOD(3429_0_random_IntArithmetic(x4[1], x5[1]), x3[1])
(2): 3429_1_MAIN_INVOKEMETHOD(3429_0_random_IntArithmetic(java.lang.Object(java.lang.String(x0[2], x1[2])), x2[2]), x4[2]) → COND_3429_1_MAIN_INVOKEMETHOD(x2[2] > 0, 3429_0_random_IntArithmetic(java.lang.Object(java.lang.String(x0[2], x1[2])), x2[2]), x4[2])
(3): COND_3429_1_MAIN_INVOKEMETHOD(TRUE, 3429_0_random_IntArithmetic(java.lang.Object(java.lang.String(x0[3], x1[3])), x2[3]), x4[3]) → 4619_1_MAIN_INVOKEMETHOD(4619_0_nth_LE(x4[3], x1[3]), x4[3])
(4): 4619_1_MAIN_INVOKEMETHOD(4619_0_nth_LE(x1[4], x0[4]), x3[4]) → COND_4619_1_MAIN_INVOKEMETHOD(x0[4] <= 1, 4619_0_nth_LE(x1[4], x0[4]), x3[4])
(5): COND_4619_1_MAIN_INVOKEMETHOD(TRUE, 4619_0_nth_LE(x1[5], x0[5]), x3[5]) → 4683_1_MAIN_INVOKEMETHOD(4683_0_nth_NONNULL(x1[5]), x3[5])
(6): 4683_1_MAIN_INVOKEMETHOD(4683_0_nth_NONNULL(java.lang.Object(IntList(x0[6], x1[6]))), java.lang.Object(IntList(x2[6], x3[6]))) → COND_4683_1_MAIN_INVOKEMETHOD(x1[6] > 0, 4683_0_nth_NONNULL(java.lang.Object(IntList(x0[6], x1[6]))), java.lang.Object(IntList(x2[6], x3[6])))
(7): COND_4683_1_MAIN_INVOKEMETHOD(TRUE, 4683_0_nth_NONNULL(java.lang.Object(IntList(x0[7], x1[7]))), java.lang.Object(IntList(x2[7], x3[7]))) → 3247_1_MAIN_INVOKEMETHOD(3247_0_random_ArrayAccess(java.lang.Object(ARRAY(x4[7], x5[7])), x6[7]), x2[7])
(8): 4683_1_MAIN_INVOKEMETHOD(4683_0_nth_NONNULL(java.lang.Object(IntList(x0[8], x1[8]))), java.lang.Object(IntList(x0[8], x1[8]))) → COND_4683_1_MAIN_INVOKEMETHOD1(x1[8] > 0, 4683_0_nth_NONNULL(java.lang.Object(IntList(x0[8], x1[8]))), java.lang.Object(IntList(x0[8], x1[8])))
(9): COND_4683_1_MAIN_INVOKEMETHOD1(TRUE, 4683_0_nth_NONNULL(java.lang.Object(IntList(x0[9], x1[9]))), java.lang.Object(IntList(x0[9], x1[9]))) → 3247_1_MAIN_INVOKEMETHOD(3247_0_random_ArrayAccess(java.lang.Object(ARRAY(x2[9], x3[9])), x4[9]), x0[9])
(12): 4619_1_MAIN_INVOKEMETHOD(4619_0_nth_LE(java.lang.Object(IntList(x1[12], x2[12])), x0[12]), x4[12]) → COND_4619_1_MAIN_INVOKEMETHOD1(x0[12] > 1, 4619_0_nth_LE(java.lang.Object(IntList(x1[12], x2[12])), x0[12]), x4[12])
(13): COND_4619_1_MAIN_INVOKEMETHOD1(TRUE, 4619_0_nth_LE(java.lang.Object(IntList(x1[13], x2[13])), x0[13]), x4[13]) → 4619_1_MAIN_INVOKEMETHOD(4619_0_nth_LE(x1[13], x0[13] + -1), x4[13])
(14): 4619_1_MAIN_INVOKEMETHOD(4619_0_nth_LE(java.lang.Object(IntList(x1[14], x2[14])), x0[14]), java.lang.Object(IntList(x1[14], x2[14]))) → COND_4619_1_MAIN_INVOKEMETHOD2(x0[14] > 1, 4619_0_nth_LE(java.lang.Object(IntList(x1[14], x2[14])), x0[14]), java.lang.Object(IntList(x1[14], x2[14])))
(15): COND_4619_1_MAIN_INVOKEMETHOD2(TRUE, 4619_0_nth_LE(java.lang.Object(IntList(x1[15], x2[15])), x0[15]), java.lang.Object(IntList(x1[15], x2[15]))) → 4619_1_MAIN_INVOKEMETHOD(4619_0_nth_LE(x1[15], x0[15] + -1), java.lang.Object(IntList(x1[15], x2[15])))