Termination proof of /tmp/tmpL2vP6m/DuplicateNodes.jar

Termination of the given JBC could be proven:

0 JBC

↳1 JBC2FIG (⇐)

↳2 FIGraph

↳3 FIGtoITRSProof (⇐)

↳4 AND

    ↳5 ITRS

        ↳6 ITRStoIDPProof (⇔)

        ↳7 IDP

        ↳8 UsableRulesProof (⇔)

        ↳9 IDP

        ↳10 ItpfGraphProof (⇔)

        ↳11 IDP

        ↳12 IDPNonInfProof (⇐)

        ↳13 AND

            ↳14 IDP

                ↳15 IDependencyGraphProof (⇔)

                ↳16 TRUE

            ↳17 IDP

                ↳18 IDependencyGraphProof (⇔)

                ↳19 TRUE

    ↳20 ITRS

        ↳21 GroundTermsRemoverProof (⇔)

        ↳22 ITRS

        ↳23 ITRSFilterProcessorProof (⇐)

        ↳24 ITRS

        ↳25 ITRSFSMergerProof (⇐)

        ↳26 ITRS

        ↳27 ITRStoIDPProof (⇔)

        ↳28 IDP

        ↳29 UsableRulesProof (⇔)

        ↳30 IDP

        ↳31 ItpfGraphProof (⇔)

        ↳32 IDP

        ↳33 IDPNonInfProof (⇐)

        ↳34 AND

            ↳35 IDP

                ↳36 IDependencyGraphProof (⇔)

                ↳37 TRUE

            ↳38 IDP

                ↳39 IDependencyGraphProof (⇔)

                ↳40 IDP

                ↳41 IDPNonInfProof (⇐)

                ↳42 AND

                    ↳43 IDP

                        ↳44 IDependencyGraphProof (⇔)

                        ↳45 TRUE

                    ↳46 IDP

                        ↳47 IDependencyGraphProof (⇔)

                        ↳48 TRUE

(0) Obligation:

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

public class DuplicateNodes {
    public static void main(String[] args) {
		Random.args = args;
        Tree tree = Tree.createTree();

		randomlyDuplicate(tree);
    }

	public static void randomlyDuplicate(Tree tree) {
		Tree cur = tree;
		
		while (cur != null) {
			if (Random.random() > 42) {
				cur.right = new Tree(cur.left, cur.right);
				cur = cur.left;
			} else {
				cur.left = new Tree(cur.left, cur.right);
				cur = cur.right;
			}
		}
	}
}


public class List {
  Tree value;
  List next;

  public List(Tree value, List next) {
    this.value = value;
    this.next = next;
  }
}


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

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


public class Tree {
  Tree left;
  Tree right;
  Object value;

  public Tree(Tree l, Tree r) {
    this.left = l;
    this.right = r;
  }

  public Tree() {
  }

  public static Tree createNode() {
   if (Random.random() == 0) {
      return null;
    }
    Tree result = new Tree();
    return result;
  }

  public static Tree createTree() {
    Tree result = createNode();
    List list = new List(result, null);
    
    int counter = Random.random();
    while (counter > 0 && list != null) {
      Tree first = list.value;
      list = list.next;

      if (first != null) {
        Tree left = createNode();
        Tree right = createNode();
        first.left = left;
        first.right = right;
        list = new List(left, list);
        list = new List(right, list);
      }

      counter--;
    }

    return result;
  }

  public static void main(String[] args) {
    Random.args = args;
    createTree();
  }
}

(1) JBC2FIG (SOUND transformation)

Constructed FIGraph.

(2) Obligation:

FIGraph based on JBC Program:
Graph of 876 nodes with 2 SCCs.

(3) FIGtoITRSProof (SOUND transformation)

Transformed FIGraph to ITRS rules

(4) Complex Obligation (AND)

(5) Obligation:

ITRS 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 TRS R consists of the following rules:
Load35058(java.lang.Object(ARRAY(i4, a115115data)), i5816, java.lang.Object(Tree(o96125, o96126))) → Load35058ARR1(java.lang.Object(ARRAY(i4, a115115data)), i5816, java.lang.Object(Tree(o96125, o96126)), java.lang.Object(java.lang.String(i5968)))
Load35058ARR1(java.lang.Object(ARRAY(i4, a115115data)), i5816, java.lang.Object(Tree(java.lang.Object(Tree(o96125, o96126)), o96126)), java.lang.Object(java.lang.String(i5968))) → Cond_Load35058ARR1(i5968 <= 42 && i5816 > 0 && i5816 < i4 && i5816 + 1 > 0, java.lang.Object(ARRAY(i4, a115115data)), i5816, java.lang.Object(Tree(java.lang.Object(Tree(o96125, o96126)), o96126)), java.lang.Object(java.lang.String(i5968)))
Cond_Load35058ARR1(TRUE, java.lang.Object(ARRAY(i4, a115115data)), i5816, java.lang.Object(Tree(java.lang.Object(Tree(o96125, o96126)), o96126)), java.lang.Object(java.lang.String(i5968))) → Load35058(java.lang.Object(ARRAY(i4, a115115data)), i5816 + 1, o96126)
Load35058(java.lang.Object(ARRAY(i4, a115115data)), i5816, java.lang.Object(Tree(o96140, o96141))) → Load35058ARR2(java.lang.Object(ARRAY(i4, a115115data)), i5816, java.lang.Object(Tree(o96140, o96141)), java.lang.Object(java.lang.String(i5968)))
Load35058ARR2(java.lang.Object(ARRAY(i4, a115115data)), i5816, java.lang.Object(Tree(o96140, java.lang.Object(Tree(o96140, o96141)))), java.lang.Object(java.lang.String(i5968))) → Cond_Load35058ARR2(i5968 > 42 && i5816 > 0 && i5816 < i4 && i5816 + 1 > 0, java.lang.Object(ARRAY(i4, a115115data)), i5816, java.lang.Object(Tree(o96140, java.lang.Object(Tree(o96140, o96141)))), java.lang.Object(java.lang.String(i5968)))
Cond_Load35058ARR2(TRUE, java.lang.Object(ARRAY(i4, a115115data)), i5816, java.lang.Object(Tree(o96140, java.lang.Object(Tree(o96140, o96141)))), java.lang.Object(java.lang.String(i5968))) → Load35058(java.lang.Object(ARRAY(i4, a115115data)), i5816 + 1, o96140)
The set Q consists of the following terms:
Load35058(java.lang.Object(ARRAY(x0, x1)), x2, java.lang.Object(Tree(x3, x4)))
Load35058ARR1(java.lang.Object(ARRAY(x0, x1)), x2, java.lang.Object(Tree(java.lang.Object(Tree(x3, x4)), x4)), java.lang.Object(java.lang.String(x5)))
Cond_Load35058ARR1(TRUE, java.lang.Object(ARRAY(x0, x1)), x2, java.lang.Object(Tree(java.lang.Object(Tree(x3, x4)), x4)), java.lang.Object(java.lang.String(x5)))
Load35058ARR2(java.lang.Object(ARRAY(x0, x1)), x2, java.lang.Object(Tree(x3, java.lang.Object(Tree(x3, x4)))), java.lang.Object(java.lang.String(x5)))
Cond_Load35058ARR2(TRUE, java.lang.Object(ARRAY(x0, x1)), x2, java.lang.Object(Tree(x3, java.lang.Object(Tree(x3, x4)))), java.lang.Object(java.lang.String(x5)))

(6) ITRStoIDPProof (EQUIVALENT transformation)

Added dependency pairs

(7) 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

The ITRS R consists of the following rules:
Load35058(java.lang.Object(ARRAY(i4, a115115data)), i5816, java.lang.Object(Tree(o96125, o96126))) → Load35058ARR1(java.lang.Object(ARRAY(i4, a115115data)), i5816, java.lang.Object(Tree(o96125, o96126)), java.lang.Object(java.lang.String(i5968)))
Load35058ARR1(java.lang.Object(ARRAY(i4, a115115data)), i5816, java.lang.Object(Tree(java.lang.Object(Tree(o96125, o96126)), o96126)), java.lang.Object(java.lang.String(i5968))) → Cond_Load35058ARR1(i5968 <= 42 && i5816 > 0 && i5816 < i4 && i5816 + 1 > 0, java.lang.Object(ARRAY(i4, a115115data)), i5816, java.lang.Object(Tree(java.lang.Object(Tree(o96125, o96126)), o96126)), java.lang.Object(java.lang.String(i5968)))
Cond_Load35058ARR1(TRUE, java.lang.Object(ARRAY(i4, a115115data)), i5816, java.lang.Object(Tree(java.lang.Object(Tree(o96125, o96126)), o96126)), java.lang.Object(java.lang.String(i5968))) → Load35058(java.lang.Object(ARRAY(i4, a115115data)), i5816 + 1, o96126)
Load35058(java.lang.Object(ARRAY(i4, a115115data)), i5816, java.lang.Object(Tree(o96140, o96141))) → Load35058ARR2(java.lang.Object(ARRAY(i4, a115115data)), i5816, java.lang.Object(Tree(o96140, o96141)), java.lang.Object(java.lang.String(i5968)))
Load35058ARR2(java.lang.Object(ARRAY(i4, a115115data)), i5816, java.lang.Object(Tree(o96140, java.lang.Object(Tree(o96140, o96141)))), java.lang.Object(java.lang.String(i5968))) → Cond_Load35058ARR2(i5968 > 42 && i5816 > 0 && i5816 < i4 && i5816 + 1 > 0, java.lang.Object(ARRAY(i4, a115115data)), i5816, java.lang.Object(Tree(o96140, java.lang.Object(Tree(o96140, o96141)))), java.lang.Object(java.lang.String(i5968)))
Cond_Load35058ARR2(TRUE, java.lang.Object(ARRAY(i4, a115115data)), i5816, java.lang.Object(Tree(o96140, java.lang.Object(Tree(o96140, o96141)))), java.lang.Object(java.lang.String(i5968))) → Load35058(java.lang.Object(ARRAY(i4, a115115data)), i5816 + 1, o96140)

The integer pair graph contains the following rules and edges:
(0): LOAD35058(java.lang.Object(ARRAY(i4[0], a115115data[0])), i5816[0], java.lang.Object(Tree(o96125[0], o96126[0]))) → LOAD35058ARR1(java.lang.Object(ARRAY(i4[0], a115115data[0])), i5816[0], java.lang.Object(Tree(o96125[0], o96126[0])), java.lang.Object(java.lang.String(i5968[0])))
(1): LOAD35058ARR1(java.lang.Object(ARRAY(i4[1], a115115data[1])), i5816[1], java.lang.Object(Tree(java.lang.Object(Tree(o96125[1], o96126[1])), o96126[1])), java.lang.Object(java.lang.String(i5968[1]))) → COND_LOAD35058ARR1(i5968[1] <= 42 && i5816[1] > 0 && i5816[1] < i4[1] && i5816[1] + 1 > 0, java.lang.Object(ARRAY(i4[1], a115115data[1])), i5816[1], java.lang.Object(Tree(java.lang.Object(Tree(o96125[1], o96126[1])), o96126[1])), java.lang.Object(java.lang.String(i5968[1])))
(2): COND_LOAD35058ARR1(TRUE, java.lang.Object(ARRAY(i4[2], a115115data[2])), i5816[2], java.lang.Object(Tree(java.lang.Object(Tree(o96125[2], o96126[2])), o96126[2])), java.lang.Object(java.lang.String(i5968[2]))) → LOAD35058(java.lang.Object(ARRAY(i4[2], a115115data[2])), i5816[2] + 1, o96126[2])
(3): LOAD35058(java.lang.Object(ARRAY(i4[3], a115115data[3])), i5816[3], java.lang.Object(Tree(o96140[3], o96141[3]))) → LOAD35058ARR2(java.lang.Object(ARRAY(i4[3], a115115data[3])), i5816[3], java.lang.Object(Tree(o96140[3], o96141[3])), java.lang.Object(java.lang.String(i5968[3])))
(4): LOAD35058ARR2(java.lang.Object(ARRAY(i4[4], a115115data[4])), i5816[4], java.lang.Object(Tree(o96140[4], java.lang.Object(Tree(o96140[4], o96141[4])))), java.lang.Object(java.lang.String(i5968[4]))) → COND_LOAD35058ARR2(i5968[4] > 42 && i5816[4] > 0 && i5816[4] < i4[4] && i5816[4] + 1 > 0, java.lang.Object(ARRAY(i4[4], a115115data[4])), i5816[4], java.lang.Object(Tree(o96140[4], java.lang.Object(Tree(o96140[4], o96141[4])))), java.lang.Object(java.lang.String(i5968[4])))
(5): COND_LOAD35058ARR2(TRUE, java.lang.Object(ARRAY(i4[5], a115115data[5])), i5816[5], java.lang.Object(Tree(o96140[5], java.lang.Object(Tree(o96140[5], o96141[5])))), java.lang.Object(java.lang.String(i5968[5]))) → LOAD35058(java.lang.Object(ARRAY(i4[5], a115115data[5])), i5816[5] + 1, o96140[5])

(0) -> (1), if ((java.lang.Object(java.lang.String(i5968[0])) →^* java.lang.Object(java.lang.String(i5968[1])))∧(java.lang.Object(ARRAY(i4[0], a115115data[0])) →^* java.lang.Object(ARRAY(i4[1], a115115data[1])))∧(i5816[0] →^* i5816[1])∧(java.lang.Object(Tree(o96125[0], o96126[0])) →^* java.lang.Object(Tree(java.lang.Object(Tree(o96125[1], o96126[1])), o96126[1]))))

(1) -> (2), if ((java.lang.Object(ARRAY(i4[1], a115115data[1])) →^* java.lang.Object(ARRAY(i4[2], a115115data[2])))∧(i5968[1] <= 42 && i5816[1] > 0 && i5816[1] < i4[1] && i5816[1] + 1 > 0 →^* TRUE)∧(java.lang.Object(Tree(java.lang.Object(Tree(o96125[1], o96126[1])), o96126[1])) →^* java.lang.Object(Tree(java.lang.Object(Tree(o96125[2], o96126[2])), o96126[2])))∧(i5816[1] →^* i5816[2])∧(java.lang.Object(java.lang.String(i5968[1])) →^* java.lang.Object(java.lang.String(i5968[2]))))

(2) -> (0), if ((o96126[2] →^* java.lang.Object(Tree(o96125[0], o96126[0])))∧(i5816[2] + 1 →^* i5816[0])∧(java.lang.Object(ARRAY(i4[2], a115115data[2])) →^* java.lang.Object(ARRAY(i4[0], a115115data[0]))))

(2) -> (3), if ((java.lang.Object(ARRAY(i4[2], a115115data[2])) →^* java.lang.Object(ARRAY(i4[3], a115115data[3])))∧(i5816[2] + 1 →^* i5816[3])∧(o96126[2] →^* java.lang.Object(Tree(o96140[3], o96141[3]))))

(3) -> (4), if ((java.lang.Object(Tree(o96140[3], o96141[3])) →^* java.lang.Object(Tree(o96140[4], java.lang.Object(Tree(o96140[4], o96141[4])))))∧(java.lang.Object(ARRAY(i4[3], a115115data[3])) →^* java.lang.Object(ARRAY(i4[4], a115115data[4])))∧(java.lang.Object(java.lang.String(i5968[3])) →^* java.lang.Object(java.lang.String(i5968[4])))∧(i5816[3] →^* i5816[4]))

(4) -> (5), if ((i5816[4] →^* i5816[5])∧(java.lang.Object(ARRAY(i4[4], a115115data[4])) →^* java.lang.Object(ARRAY(i4[5], a115115data[5])))∧(i5968[4] > 42 && i5816[4] > 0 && i5816[4] < i4[4] && i5816[4] + 1 > 0 →^* TRUE)∧(java.lang.Object(java.lang.String(i5968[4])) →^* java.lang.Object(java.lang.String(i5968[5])))∧(java.lang.Object(Tree(o96140[4], java.lang.Object(Tree(o96140[4], o96141[4])))) →^* java.lang.Object(Tree(o96140[5], java.lang.Object(Tree(o96140[5], o96141[5]))))))

(5) -> (0), if ((java.lang.Object(ARRAY(i4[5], a115115data[5])) →^* java.lang.Object(ARRAY(i4[0], a115115data[0])))∧(i5816[5] + 1 →^* i5816[0])∧(o96140[5] →^* java.lang.Object(Tree(o96125[0], o96126[0]))))

(5) -> (3), if ((i5816[5] + 1 →^* i5816[3])∧(java.lang.Object(ARRAY(i4[5], a115115data[5])) →^* java.lang.Object(ARRAY(i4[3], a115115data[3])))∧(o96140[5] →^* java.lang.Object(Tree(o96140[3], o96141[3]))))

The set Q consists of the following terms:
Load35058(java.lang.Object(ARRAY(x0, x1)), x2, java.lang.Object(Tree(x3, x4)))
Load35058ARR1(java.lang.Object(ARRAY(x0, x1)), x2, java.lang.Object(Tree(java.lang.Object(Tree(x3, x4)), x4)), java.lang.Object(java.lang.String(x5)))
Cond_Load35058ARR1(TRUE, java.lang.Object(ARRAY(x0, x1)), x2, java.lang.Object(Tree(java.lang.Object(Tree(x3, x4)), x4)), java.lang.Object(java.lang.String(x5)))
Load35058ARR2(java.lang.Object(ARRAY(x0, x1)), x2, java.lang.Object(Tree(x3, java.lang.Object(Tree(x3, x4)))), java.lang.Object(java.lang.String(x5)))
Cond_Load35058ARR2(TRUE, java.lang.Object(ARRAY(x0, x1)), x2, java.lang.Object(Tree(x3, java.lang.Object(Tree(x3, x4)))), java.lang.Object(java.lang.String(x5)))

(8) UsableRulesProof (EQUIVALENT transformation)

As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [LPAR04] we can delete all non-usable rules [FROCOS05] from R.

(9) 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): LOAD35058(java.lang.Object(ARRAY(i4[0], a115115data[0])), i5816[0], java.lang.Object(Tree(o96125[0], o96126[0]))) → LOAD35058ARR1(java.lang.Object(ARRAY(i4[0], a115115data[0])), i5816[0], java.lang.Object(Tree(o96125[0], o96126[0])), java.lang.Object(java.lang.String(i5968[0])))
(1): LOAD35058ARR1(java.lang.Object(ARRAY(i4[1], a115115data[1])), i5816[1], java.lang.Object(Tree(java.lang.Object(Tree(o96125[1], o96126[1])), o96126[1])), java.lang.Object(java.lang.String(i5968[1]))) → COND_LOAD35058ARR1(i5968[1] <= 42 && i5816[1] > 0 && i5816[1] < i4[1] && i5816[1] + 1 > 0, java.lang.Object(ARRAY(i4[1], a115115data[1])), i5816[1], java.lang.Object(Tree(java.lang.Object(Tree(o96125[1], o96126[1])), o96126[1])), java.lang.Object(java.lang.String(i5968[1])))
(2): COND_LOAD35058ARR1(TRUE, java.lang.Object(ARRAY(i4[2], a115115data[2])), i5816[2], java.lang.Object(Tree(java.lang.Object(Tree(o96125[2], o96126[2])), o96126[2])), java.lang.Object(java.lang.String(i5968[2]))) → LOAD35058(java.lang.Object(ARRAY(i4[2], a115115data[2])), i5816[2] + 1, o96126[2])
(3): LOAD35058(java.lang.Object(ARRAY(i4[3], a115115data[3])), i5816[3], java.lang.Object(Tree(o96140[3], o96141[3]))) → LOAD35058ARR2(java.lang.Object(ARRAY(i4[3], a115115data[3])), i5816[3], java.lang.Object(Tree(o96140[3], o96141[3])), java.lang.Object(java.lang.String(i5968[3])))
(4): LOAD35058ARR2(java.lang.Object(ARRAY(i4[4], a115115data[4])), i5816[4], java.lang.Object(Tree(o96140[4], java.lang.Object(Tree(o96140[4], o96141[4])))), java.lang.Object(java.lang.String(i5968[4]))) → COND_LOAD35058ARR2(i5968[4] > 42 && i5816[4] > 0 && i5816[4] < i4[4] && i5816[4] + 1 > 0, java.lang.Object(ARRAY(i4[4], a115115data[4])), i5816[4], java.lang.Object(Tree(o96140[4], java.lang.Object(Tree(o96140[4], o96141[4])))), java.lang.Object(java.lang.String(i5968[4])))
(5): COND_LOAD35058ARR2(TRUE, java.lang.Object(ARRAY(i4[5], a115115data[5])), i5816[5], java.lang.Object(Tree(o96140[5], java.lang.Object(Tree(o96140[5], o96141[5])))), java.lang.Object(java.lang.String(i5968[5]))) → LOAD35058(java.lang.Object(ARRAY(i4[5], a115115data[5])), i5816[5] + 1, o96140[5])

(10) ItpfGraphProof (EQUIVALENT transformation)

Applied rule ItpfICap [ICap]

(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

(0) -> (1), if (((i5968[0] →^* i5968[1]))∧((i4[0] →^* i4[1])∧(a115115data[0] →^* a115115data[1]))∧(i5816[0] →^* i5816[1])∧((o96125[0] →^* java.lang.Object(Tree(o96125[1], o96126[1])))∧(o96126[0] →^* o96126[1])))

(1) -> (2), if (((i4[1] →^* i4[2])∧(a115115data[1] →^* a115115data[2]))∧(i5968[1] <= 42 && i5816[1] > 0 && i5816[1] < i4[1] && i5816[1] + 1 > 0 →^* TRUE)∧((o96125[1] →^* o96125[2])∧(o96126[1] →^* o96126[2]))∧(i5816[1] →^* i5816[2])∧((i5968[1] →^* i5968[2])))

(2) -> (0), if ((o96126[2] →^* java.lang.Object(Tree(o96125[0], o96126[0])))∧(i5816[2] + 1 →^* i5816[0])∧((i4[2] →^* i4[0])∧(a115115data[2] →^* a115115data[0])))

(2) -> (3), if (((i4[2] →^* i4[3])∧(a115115data[2] →^* a115115data[3]))∧(i5816[2] + 1 →^* i5816[3])∧(o96126[2] →^* java.lang.Object(Tree(o96140[3], o96141[3]))))

(3) -> (4), if (((o96140[3] →^* o96140[4])∧(o96141[3] →^* java.lang.Object(Tree(o96140[4], o96141[4]))))∧((i4[3] →^* i4[4])∧(a115115data[3] →^* a115115data[4]))∧((i5968[3] →^* i5968[4]))∧(i5816[3] →^* i5816[4]))

(4) -> (5), if ((i5816[4] →^* i5816[5])∧((i4[4] →^* i4[5])∧(a115115data[4] →^* a115115data[5]))∧(i5968[4] > 42 && i5816[4] > 0 && i5816[4] < i4[4] && i5816[4] + 1 > 0 →^* TRUE)∧((i5968[4] →^* i5968[5]))∧((o96140[4] →^* o96140[5])∧(o96141[4] →^* o96141[5])))

(5) -> (0), if (((i4[5] →^* i4[0])∧(a115115data[5] →^* a115115data[0]))∧(i5816[5] + 1 →^* i5816[0])∧(o96140[5] →^* java.lang.Object(Tree(o96125[0], o96126[0]))))

(5) -> (3), if ((i5816[5] + 1 →^* i5816[3])∧((i4[5] →^* i4[3])∧(a115115data[5] →^* a115115data[3]))∧(o96140[5] →^* java.lang.Object(Tree(o96140[3], o96141[3]))))

(12) 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 LOAD35058(java.lang.Object(ARRAY(i4, a115115data)), i5816, java.lang.Object(Tree(o96125, o96126))) → LOAD35058ARR1(java.lang.Object(ARRAY(i4, a115115data)), i5816, java.lang.Object(Tree(o96125, o96126)), java.lang.Object(java.lang.String(i5968))) the following chains were created:

We consider the chain COND_LOAD35058ARR1(TRUE, java.lang.Object(ARRAY(i4[2], a115115data[2])), i5816[2], java.lang.Object(Tree(java.lang.Object(Tree(o96125[2], o96126[2])), o96126[2])), java.lang.Object(java.lang.String(i5968[2]))) → LOAD35058(java.lang.Object(ARRAY(i4[2], a115115data[2])), +(i5816[2], 1), o96126[2]), LOAD35058(java.lang.Object(ARRAY(i4[0], a115115data[0])), i5816[0], java.lang.Object(Tree(o96125[0], o96126[0]))) → LOAD35058ARR1(java.lang.Object(ARRAY(i4[0], a115115data[0])), i5816[0], java.lang.Object(Tree(o96125[0], o96126[0])), java.lang.Object(java.lang.String(i5968[0]))), LOAD35058ARR1(java.lang.Object(ARRAY(i4[1], a115115data[1])), i5816[1], java.lang.Object(Tree(java.lang.Object(Tree(o96125[1], o96126[1])), o96126[1])), java.lang.Object(java.lang.String(i5968[1]))) → COND_LOAD35058ARR1(&&(&&(&&(<=(i5968[1], 42), >(i5816[1], 0)), <(i5816[1], i4[1])), >(+(i5816[1], 1), 0)), java.lang.Object(ARRAY(i4[1], a115115data[1])), i5816[1], java.lang.Object(Tree(java.lang.Object(Tree(o96125[1], o96126[1])), o96126[1])), java.lang.Object(java.lang.String(i5968[1]))) which results in the following constraint:
(1)    (o96126[2]=java.lang.Object(Tree(o96125[0], o96126[0]))∧+(i5816[2], 1)=i5816[0]∧i4[2]=i4[0]∧a115115data[2]=a115115data[0]∧i5968[0]=i5968[1]∧i4[0]=i4[1]∧a115115data[0]=a115115data[1]∧i5816[0]=i5816[1]∧o96125[0]=java.lang.Object(Tree(o96125[1], o96126[1]))∧o96126[0]=o96126[1] ⇒ LOAD35058(java.lang.Object(ARRAY(i4[0], a115115data[0])), i5816[0], java.lang.Object(Tree(o96125[0], o96126[0])))≥LOAD35058ARR1(java.lang.Object(ARRAY(i4[0], a115115data[0])), i5816[0], java.lang.Object(Tree(o96125[0], o96126[0])), java.lang.Object(java.lang.String(i5968[0])))∧(U^Increasing(LOAD35058ARR1(java.lang.Object(ARRAY(i4[0], a115115data[0])), i5816[0], java.lang.Object(Tree(o96125[0], o96126[0])), java.lang.Object(java.lang.String(i5968[0])))), ≥))

We simplified constraint (1) using rules (III), (IV) which results in the following new constraint:
(2)    (LOAD35058(java.lang.Object(ARRAY(i4[2], a115115data[2])), +(i5816[2], 1), java.lang.Object(Tree(java.lang.Object(Tree(o96125[1], o96126[0])), o96126[0])))≥LOAD35058ARR1(java.lang.Object(ARRAY(i4[2], a115115data[2])), +(i5816[2], 1), java.lang.Object(Tree(java.lang.Object(Tree(o96125[1], o96126[0])), o96126[0])), java.lang.Object(java.lang.String(i5968[0])))∧(U^Increasing(LOAD35058ARR1(java.lang.Object(ARRAY(i4[0], a115115data[0])), i5816[0], java.lang.Object(Tree(o96125[0], o96126[0])), java.lang.Object(java.lang.String(i5968[0])))), ≥))

We simplified constraint (2) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(3)    ((U^Increasing(LOAD35058ARR1(java.lang.Object(ARRAY(i4[0], a115115data[0])), i5816[0], java.lang.Object(Tree(o96125[0], o96126[0])), java.lang.Object(java.lang.String(i5968[0])))), ≥)∧[3 + (-1)bso_37] ≥ 0)

We simplified constraint (3) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(4)    ((U^Increasing(LOAD35058ARR1(java.lang.Object(ARRAY(i4[0], a115115data[0])), i5816[0], java.lang.Object(Tree(o96125[0], o96126[0])), java.lang.Object(java.lang.String(i5968[0])))), ≥)∧[3 + (-1)bso_37] ≥ 0)

We simplified constraint (4) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(5)    ((U^Increasing(LOAD35058ARR1(java.lang.Object(ARRAY(i4[0], a115115data[0])), i5816[0], java.lang.Object(Tree(o96125[0], o96126[0])), java.lang.Object(java.lang.String(i5968[0])))), ≥)∧[3 + (-1)bso_37] ≥ 0)

We simplified constraint (5) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:
(6)    ((U^Increasing(LOAD35058ARR1(java.lang.Object(ARRAY(i4[0], a115115data[0])), i5816[0], java.lang.Object(Tree(o96125[0], o96126[0])), java.lang.Object(java.lang.String(i5968[0])))), ≥)∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[3 + (-1)bso_37] ≥ 0)
We consider the chain COND_LOAD35058ARR2(TRUE, java.lang.Object(ARRAY(i4[5], a115115data[5])), i5816[5], java.lang.Object(Tree(o96140[5], java.lang.Object(Tree(o96140[5], o96141[5])))), java.lang.Object(java.lang.String(i5968[5]))) → LOAD35058(java.lang.Object(ARRAY(i4[5], a115115data[5])), +(i5816[5], 1), o96140[5]), LOAD35058(java.lang.Object(ARRAY(i4[0], a115115data[0])), i5816[0], java.lang.Object(Tree(o96125[0], o96126[0]))) → LOAD35058ARR1(java.lang.Object(ARRAY(i4[0], a115115data[0])), i5816[0], java.lang.Object(Tree(o96125[0], o96126[0])), java.lang.Object(java.lang.String(i5968[0]))), LOAD35058ARR1(java.lang.Object(ARRAY(i4[1], a115115data[1])), i5816[1], java.lang.Object(Tree(java.lang.Object(Tree(o96125[1], o96126[1])), o96126[1])), java.lang.Object(java.lang.String(i5968[1]))) → COND_LOAD35058ARR1(&&(&&(&&(<=(i5968[1], 42), >(i5816[1], 0)), <(i5816[1], i4[1])), >(+(i5816[1], 1), 0)), java.lang.Object(ARRAY(i4[1], a115115data[1])), i5816[1], java.lang.Object(Tree(java.lang.Object(Tree(o96125[1], o96126[1])), o96126[1])), java.lang.Object(java.lang.String(i5968[1]))) which results in the following constraint:
(7)    (i4[5]=i4[0]∧a115115data[5]=a115115data[0]∧+(i5816[5], 1)=i5816[0]∧o96140[5]=java.lang.Object(Tree(o96125[0], o96126[0]))∧i5968[0]=i5968[1]∧i4[0]=i4[1]∧a115115data[0]=a115115data[1]∧i5816[0]=i5816[1]∧o96125[0]=java.lang.Object(Tree(o96125[1], o96126[1]))∧o96126[0]=o96126[1] ⇒ LOAD35058(java.lang.Object(ARRAY(i4[0], a115115data[0])), i5816[0], java.lang.Object(Tree(o96125[0], o96126[0])))≥LOAD35058ARR1(java.lang.Object(ARRAY(i4[0], a115115data[0])), i5816[0], java.lang.Object(Tree(o96125[0], o96126[0])), java.lang.Object(java.lang.String(i5968[0])))∧(U^Increasing(LOAD35058ARR1(java.lang.Object(ARRAY(i4[0], a115115data[0])), i5816[0], java.lang.Object(Tree(o96125[0], o96126[0])), java.lang.Object(java.lang.String(i5968[0])))), ≥))

We simplified constraint (7) using rules (III), (IV) which results in the following new constraint:
(8)    (LOAD35058(java.lang.Object(ARRAY(i4[5], a115115data[5])), +(i5816[5], 1), java.lang.Object(Tree(java.lang.Object(Tree(o96125[1], o96126[0])), o96126[0])))≥LOAD35058ARR1(java.lang.Object(ARRAY(i4[5], a115115data[5])), +(i5816[5], 1), java.lang.Object(Tree(java.lang.Object(Tree(o96125[1], o96126[0])), o96126[0])), java.lang.Object(java.lang.String(i5968[0])))∧(U^Increasing(LOAD35058ARR1(java.lang.Object(ARRAY(i4[0], a115115data[0])), i5816[0], java.lang.Object(Tree(o96125[0], o96126[0])), java.lang.Object(java.lang.String(i5968[0])))), ≥))

We simplified constraint (8) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(9)    ((U^Increasing(LOAD35058ARR1(java.lang.Object(ARRAY(i4[0], a115115data[0])), i5816[0], java.lang.Object(Tree(o96125[0], o96126[0])), java.lang.Object(java.lang.String(i5968[0])))), ≥)∧[3 + (-1)bso_37] ≥ 0)

We simplified constraint (9) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(10)    ((U^Increasing(LOAD35058ARR1(java.lang.Object(ARRAY(i4[0], a115115data[0])), i5816[0], java.lang.Object(Tree(o96125[0], o96126[0])), java.lang.Object(java.lang.String(i5968[0])))), ≥)∧[3 + (-1)bso_37] ≥ 0)

We simplified constraint (10) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(11)    ((U^Increasing(LOAD35058ARR1(java.lang.Object(ARRAY(i4[0], a115115data[0])), i5816[0], java.lang.Object(Tree(o96125[0], o96126[0])), java.lang.Object(java.lang.String(i5968[0])))), ≥)∧[3 + (-1)bso_37] ≥ 0)

We simplified constraint (11) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:
(12)    ((U^Increasing(LOAD35058ARR1(java.lang.Object(ARRAY(i4[0], a115115data[0])), i5816[0], java.lang.Object(Tree(o96125[0], o96126[0])), java.lang.Object(java.lang.String(i5968[0])))), ≥)∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[3 + (-1)bso_37] ≥ 0)

For Pair LOAD35058ARR1(java.lang.Object(ARRAY(i4, a115115data)), i5816, java.lang.Object(Tree(java.lang.Object(Tree(o96125, o96126)), o96126)), java.lang.Object(java.lang.String(i5968))) → COND_LOAD35058ARR1(&&(&&(&&(<=(i5968, 42), >(i5816, 0)), <(i5816, i4)), >(+(i5816, 1), 0)), java.lang.Object(ARRAY(i4, a115115data)), i5816, java.lang.Object(Tree(java.lang.Object(Tree(o96125, o96126)), o96126)), java.lang.Object(java.lang.String(i5968))) the following chains were created:

We consider the chain LOAD35058ARR1(java.lang.Object(ARRAY(i4[1], a115115data[1])), i5816[1], java.lang.Object(Tree(java.lang.Object(Tree(o96125[1], o96126[1])), o96126[1])), java.lang.Object(java.lang.String(i5968[1]))) → COND_LOAD35058ARR1(&&(&&(&&(<=(i5968[1], 42), >(i5816[1], 0)), <(i5816[1], i4[1])), >(+(i5816[1], 1), 0)), java.lang.Object(ARRAY(i4[1], a115115data[1])), i5816[1], java.lang.Object(Tree(java.lang.Object(Tree(o96125[1], o96126[1])), o96126[1])), java.lang.Object(java.lang.String(i5968[1]))), COND_LOAD35058ARR1(TRUE, java.lang.Object(ARRAY(i4[2], a115115data[2])), i5816[2], java.lang.Object(Tree(java.lang.Object(Tree(o96125[2], o96126[2])), o96126[2])), java.lang.Object(java.lang.String(i5968[2]))) → LOAD35058(java.lang.Object(ARRAY(i4[2], a115115data[2])), +(i5816[2], 1), o96126[2]) which results in the following constraint:
(13)    (i4[1]=i4[2]∧a115115data[1]=a115115data[2]∧&&(&&(&&(<=(i5968[1], 42), >(i5816[1], 0)), <(i5816[1], i4[1])), >(+(i5816[1], 1), 0))=TRUE∧o96125[1]=o96125[2]∧o96126[1]=o96126[2]∧i5816[1]=i5816[2]∧i5968[1]=i5968[2] ⇒ LOAD35058ARR1(java.lang.Object(ARRAY(i4[1], a115115data[1])), i5816[1], java.lang.Object(Tree(java.lang.Object(Tree(o96125[1], o96126[1])), o96126[1])), java.lang.Object(java.lang.String(i5968[1])))≥COND_LOAD35058ARR1(&&(&&(&&(<=(i5968[1], 42), >(i5816[1], 0)), <(i5816[1], i4[1])), >(+(i5816[1], 1), 0)), java.lang.Object(ARRAY(i4[1], a115115data[1])), i5816[1], java.lang.Object(Tree(java.lang.Object(Tree(o96125[1], o96126[1])), o96126[1])), java.lang.Object(java.lang.String(i5968[1])))∧(U^Increasing(COND_LOAD35058ARR1(&&(&&(&&(<=(i5968[1], 42), >(i5816[1], 0)), <(i5816[1], i4[1])), >(+(i5816[1], 1), 0)), java.lang.Object(ARRAY(i4[1], a115115data[1])), i5816[1], java.lang.Object(Tree(java.lang.Object(Tree(o96125[1], o96126[1])), o96126[1])), java.lang.Object(java.lang.String(i5968[1])))), ≥))

We simplified constraint (13) using rule (IV) which results in the following new constraint:
(14)    (&&(&&(&&(<=(i5968[1], 42), >(i5816[1], 0)), <(i5816[1], i4[1])), >(+(i5816[1], 1), 0))=TRUE ⇒ LOAD35058ARR1(java.lang.Object(ARRAY(i4[1], a115115data[1])), i5816[1], java.lang.Object(Tree(java.lang.Object(Tree(o96125[1], o96126[1])), o96126[1])), java.lang.Object(java.lang.String(i5968[1])))≥COND_LOAD35058ARR1(&&(&&(&&(<=(i5968[1], 42), >(i5816[1], 0)), <(i5816[1], i4[1])), >(+(i5816[1], 1), 0)), java.lang.Object(ARRAY(i4[1], a115115data[1])), i5816[1], java.lang.Object(Tree(java.lang.Object(Tree(o96125[1], o96126[1])), o96126[1])), java.lang.Object(java.lang.String(i5968[1])))∧(U^Increasing(COND_LOAD35058ARR1(&&(&&(&&(<=(i5968[1], 42), >(i5816[1], 0)), <(i5816[1], i4[1])), >(+(i5816[1], 1), 0)), java.lang.Object(ARRAY(i4[1], a115115data[1])), i5816[1], java.lang.Object(Tree(java.lang.Object(Tree(o96125[1], o96126[1])), o96126[1])), java.lang.Object(java.lang.String(i5968[1])))), ≥))

We simplified constraint (14) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(15)    (0 ≥ 0 ⇒ (U^Increasing(COND_LOAD35058ARR1(&&(&&(&&(<=(i5968[1], 42), >(i5816[1], 0)), <(i5816[1], i4[1])), >(+(i5816[1], 1), 0)), java.lang.Object(ARRAY(i4[1], a115115data[1])), i5816[1], java.lang.Object(Tree(java.lang.Object(Tree(o96125[1], o96126[1])), o96126[1])), java.lang.Object(java.lang.String(i5968[1])))), ≥)∧[3 + (-1)bso_38] ≥ 0)

We simplified constraint (15) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(16)    (0 ≥ 0 ⇒ (U^Increasing(COND_LOAD35058ARR1(&&(&&(&&(<=(i5968[1], 42), >(i5816[1], 0)), <(i5816[1], i4[1])), >(+(i5816[1], 1), 0)), java.lang.Object(ARRAY(i4[1], a115115data[1])), i5816[1], java.lang.Object(Tree(java.lang.Object(Tree(o96125[1], o96126[1])), o96126[1])), java.lang.Object(java.lang.String(i5968[1])))), ≥)∧[3 + (-1)bso_38] ≥ 0)

We simplified constraint (16) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(17)    (0 ≥ 0 ⇒ (U^Increasing(COND_LOAD35058ARR1(&&(&&(&&(<=(i5968[1], 42), >(i5816[1], 0)), <(i5816[1], i4[1])), >(+(i5816[1], 1), 0)), java.lang.Object(ARRAY(i4[1], a115115data[1])), i5816[1], java.lang.Object(Tree(java.lang.Object(Tree(o96125[1], o96126[1])), o96126[1])), java.lang.Object(java.lang.String(i5968[1])))), ≥)∧[3 + (-1)bso_38] ≥ 0)

We simplified constraint (17) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:
(18)    (0 ≥ 0 ⇒ (U^Increasing(COND_LOAD35058ARR1(&&(&&(&&(<=(i5968[1], 42), >(i5816[1], 0)), <(i5816[1], i4[1])), >(+(i5816[1], 1), 0)), java.lang.Object(ARRAY(i4[1], a115115data[1])), i5816[1], java.lang.Object(Tree(java.lang.Object(Tree(o96125[1], o96126[1])), o96126[1])), java.lang.Object(java.lang.String(i5968[1])))), ≥)∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[3 + (-1)bso_38] ≥ 0)

For Pair COND_LOAD35058ARR1(TRUE, java.lang.Object(ARRAY(i4, a115115data)), i5816, java.lang.Object(Tree(java.lang.Object(Tree(o96125, o96126)), o96126)), java.lang.Object(java.lang.String(i5968))) → LOAD35058(java.lang.Object(ARRAY(i4, a115115data)), +(i5816, 1), o96126) the following chains were created:

We consider the chain LOAD35058ARR1(java.lang.Object(ARRAY(i4[1], a115115data[1])), i5816[1], java.lang.Object(Tree(java.lang.Object(Tree(o96125[1], o96126[1])), o96126[1])), java.lang.Object(java.lang.String(i5968[1]))) → COND_LOAD35058ARR1(&&(&&(&&(<=(i5968[1], 42), >(i5816[1], 0)), <(i5816[1], i4[1])), >(+(i5816[1], 1), 0)), java.lang.Object(ARRAY(i4[1], a115115data[1])), i5816[1], java.lang.Object(Tree(java.lang.Object(Tree(o96125[1], o96126[1])), o96126[1])), java.lang.Object(java.lang.String(i5968[1]))), COND_LOAD35058ARR1(TRUE, java.lang.Object(ARRAY(i4[2], a115115data[2])), i5816[2], java.lang.Object(Tree(java.lang.Object(Tree(o96125[2], o96126[2])), o96126[2])), java.lang.Object(java.lang.String(i5968[2]))) → LOAD35058(java.lang.Object(ARRAY(i4[2], a115115data[2])), +(i5816[2], 1), o96126[2]), LOAD35058(java.lang.Object(ARRAY(i4[0], a115115data[0])), i5816[0], java.lang.Object(Tree(o96125[0], o96126[0]))) → LOAD35058ARR1(java.lang.Object(ARRAY(i4[0], a115115data[0])), i5816[0], java.lang.Object(Tree(o96125[0], o96126[0])), java.lang.Object(java.lang.String(i5968[0]))) which results in the following constraint:
(19)    (i4[1]=i4[2]∧a115115data[1]=a115115data[2]∧&&(&&(&&(<=(i5968[1], 42), >(i5816[1], 0)), <(i5816[1], i4[1])), >(+(i5816[1], 1), 0))=TRUE∧o96125[1]=o96125[2]∧o96126[1]=o96126[2]∧i5816[1]=i5816[2]∧i5968[1]=i5968[2]∧o96126[2]=java.lang.Object(Tree(o96125[0], o96126[0]))∧+(i5816[2], 1)=i5816[0]∧i4[2]=i4[0]∧a115115data[2]=a115115data[0] ⇒ COND_LOAD35058ARR1(TRUE, java.lang.Object(ARRAY(i4[2], a115115data[2])), i5816[2], java.lang.Object(Tree(java.lang.Object(Tree(o96125[2], o96126[2])), o96126[2])), java.lang.Object(java.lang.String(i5968[2])))≥LOAD35058(java.lang.Object(ARRAY(i4[2], a115115data[2])), +(i5816[2], 1), o96126[2])∧(U^Increasing(LOAD35058(java.lang.Object(ARRAY(i4[2], a115115data[2])), +(i5816[2], 1), o96126[2])), ≥))

We simplified constraint (19) using rules (III), (IV) which results in the following new constraint:
(20)    (&&(&&(&&(<=(i5968[1], 42), >(i5816[1], 0)), <(i5816[1], i4[1])), >(+(i5816[1], 1), 0))=TRUE ⇒ COND_LOAD35058ARR1(TRUE, java.lang.Object(ARRAY(i4[1], a115115data[1])), i5816[1], java.lang.Object(Tree(java.lang.Object(Tree(o96125[1], java.lang.Object(Tree(o96125[0], o96126[0])))), java.lang.Object(Tree(o96125[0], o96126[0])))), java.lang.Object(java.lang.String(i5968[1])))≥LOAD35058(java.lang.Object(ARRAY(i4[1], a115115data[1])), +(i5816[1], 1), java.lang.Object(Tree(o96125[0], o96126[0])))∧(U^Increasing(LOAD35058(java.lang.Object(ARRAY(i4[2], a115115data[2])), +(i5816[2], 1), o96126[2])), ≥))

We simplified constraint (20) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(21)    (0 ≥ 0 ⇒ (U^Increasing(LOAD35058(java.lang.Object(ARRAY(i4[2], a115115data[2])), +(i5816[2], 1), o96126[2])), ≥)∧[186 + (-1)bso_39] + [152]o96126[0] + [152]o96125[0] + [32]o96125[1] ≥ 0)

We simplified constraint (21) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(22)    (0 ≥ 0 ⇒ (U^Increasing(LOAD35058(java.lang.Object(ARRAY(i4[2], a115115data[2])), +(i5816[2], 1), o96126[2])), ≥)∧[186 + (-1)bso_39] + [152]o96126[0] + [152]o96125[0] + [32]o96125[1] ≥ 0)

We simplified constraint (22) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(23)    (0 ≥ 0 ⇒ (U^Increasing(LOAD35058(java.lang.Object(ARRAY(i4[2], a115115data[2])), +(i5816[2], 1), o96126[2])), ≥)∧[186 + (-1)bso_39] + [152]o96126[0] + [152]o96125[0] + [32]o96125[1] ≥ 0)

We simplified constraint (23) using rules (IDP_UNRESTRICTED_VARS), (IDP_POLY_GCD) which results in the following new constraint:
(24)    (0 ≥ 0 ⇒ (U^Increasing(LOAD35058(java.lang.Object(ARRAY(i4[2], a115115data[2])), +(i5816[2], 1), o96126[2])), ≥)∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[186 + (-1)bso_39] ≥ 0∧[1] ≥ 0∧[1] ≥ 0∧[1] ≥ 0)
We consider the chain LOAD35058ARR1(java.lang.Object(ARRAY(i4[1], a115115data[1])), i5816[1], java.lang.Object(Tree(java.lang.Object(Tree(o96125[1], o96126[1])), o96126[1])), java.lang.Object(java.lang.String(i5968[1]))) → COND_LOAD35058ARR1(&&(&&(&&(<=(i5968[1], 42), >(i5816[1], 0)), <(i5816[1], i4[1])), >(+(i5816[1], 1), 0)), java.lang.Object(ARRAY(i4[1], a115115data[1])), i5816[1], java.lang.Object(Tree(java.lang.Object(Tree(o96125[1], o96126[1])), o96126[1])), java.lang.Object(java.lang.String(i5968[1]))), COND_LOAD35058ARR1(TRUE, java.lang.Object(ARRAY(i4[2], a115115data[2])), i5816[2], java.lang.Object(Tree(java.lang.Object(Tree(o96125[2], o96126[2])), o96126[2])), java.lang.Object(java.lang.String(i5968[2]))) → LOAD35058(java.lang.Object(ARRAY(i4[2], a115115data[2])), +(i5816[2], 1), o96126[2]), LOAD35058(java.lang.Object(ARRAY(i4[3], a115115data[3])), i5816[3], java.lang.Object(Tree(o96140[3], o96141[3]))) → LOAD35058ARR2(java.lang.Object(ARRAY(i4[3], a115115data[3])), i5816[3], java.lang.Object(Tree(o96140[3], o96141[3])), java.lang.Object(java.lang.String(i5968[3]))) which results in the following constraint:
(25)    (i4[1]=i4[2]∧a115115data[1]=a115115data[2]∧&&(&&(&&(<=(i5968[1], 42), >(i5816[1], 0)), <(i5816[1], i4[1])), >(+(i5816[1], 1), 0))=TRUE∧o96125[1]=o96125[2]∧o96126[1]=o96126[2]∧i5816[1]=i5816[2]∧i5968[1]=i5968[2]∧i4[2]=i4[3]∧a115115data[2]=a115115data[3]∧+(i5816[2], 1)=i5816[3]∧o96126[2]=java.lang.Object(Tree(o96140[3], o96141[3])) ⇒ COND_LOAD35058ARR1(TRUE, java.lang.Object(ARRAY(i4[2], a115115data[2])), i5816[2], java.lang.Object(Tree(java.lang.Object(Tree(o96125[2], o96126[2])), o96126[2])), java.lang.Object(java.lang.String(i5968[2])))≥LOAD35058(java.lang.Object(ARRAY(i4[2], a115115data[2])), +(i5816[2], 1), o96126[2])∧(U^Increasing(LOAD35058(java.lang.Object(ARRAY(i4[2], a115115data[2])), +(i5816[2], 1), o96126[2])), ≥))

We simplified constraint (25) using rules (III), (IV) which results in the following new constraint:
(26)    (&&(&&(&&(<=(i5968[1], 42), >(i5816[1], 0)), <(i5816[1], i4[1])), >(+(i5816[1], 1), 0))=TRUE ⇒ COND_LOAD35058ARR1(TRUE, java.lang.Object(ARRAY(i4[1], a115115data[1])), i5816[1], java.lang.Object(Tree(java.lang.Object(Tree(o96125[1], java.lang.Object(Tree(o96140[3], o96141[3])))), java.lang.Object(Tree(o96140[3], o96141[3])))), java.lang.Object(java.lang.String(i5968[1])))≥LOAD35058(java.lang.Object(ARRAY(i4[1], a115115data[1])), +(i5816[1], 1), java.lang.Object(Tree(o96140[3], o96141[3])))∧(U^Increasing(LOAD35058(java.lang.Object(ARRAY(i4[2], a115115data[2])), +(i5816[2], 1), o96126[2])), ≥))

We simplified constraint (26) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(27)    (0 ≥ 0 ⇒ (U^Increasing(LOAD35058(java.lang.Object(ARRAY(i4[2], a115115data[2])), +(i5816[2], 1), o96126[2])), ≥)∧[186 + (-1)bso_39] + [152]o96141[3] + [152]o96140[3] + [32]o96125[1] ≥ 0)

We simplified constraint (27) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(28)    (0 ≥ 0 ⇒ (U^Increasing(LOAD35058(java.lang.Object(ARRAY(i4[2], a115115data[2])), +(i5816[2], 1), o96126[2])), ≥)∧[186 + (-1)bso_39] + [152]o96141[3] + [152]o96140[3] + [32]o96125[1] ≥ 0)

We simplified constraint (28) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(29)    (0 ≥ 0 ⇒ (U^Increasing(LOAD35058(java.lang.Object(ARRAY(i4[2], a115115data[2])), +(i5816[2], 1), o96126[2])), ≥)∧[186 + (-1)bso_39] + [152]o96141[3] + [152]o96140[3] + [32]o96125[1] ≥ 0)

We simplified constraint (29) using rules (IDP_UNRESTRICTED_VARS), (IDP_POLY_GCD) which results in the following new constraint:
(30)    (0 ≥ 0 ⇒ (U^Increasing(LOAD35058(java.lang.Object(ARRAY(i4[2], a115115data[2])), +(i5816[2], 1), o96126[2])), ≥)∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[186 + (-1)bso_39] ≥ 0∧[1] ≥ 0∧[1] ≥ 0∧[1] ≥ 0)

For Pair LOAD35058(java.lang.Object(ARRAY(i4, a115115data)), i5816, java.lang.Object(Tree(o96140, o96141))) → LOAD35058ARR2(java.lang.Object(ARRAY(i4, a115115data)), i5816, java.lang.Object(Tree(o96140, o96141)), java.lang.Object(java.lang.String(i5968))) the following chains were created:

We consider the chain COND_LOAD35058ARR1(TRUE, java.lang.Object(ARRAY(i4[2], a115115data[2])), i5816[2], java.lang.Object(Tree(java.lang.Object(Tree(o96125[2], o96126[2])), o96126[2])), java.lang.Object(java.lang.String(i5968[2]))) → LOAD35058(java.lang.Object(ARRAY(i4[2], a115115data[2])), +(i5816[2], 1), o96126[2]), LOAD35058(java.lang.Object(ARRAY(i4[3], a115115data[3])), i5816[3], java.lang.Object(Tree(o96140[3], o96141[3]))) → LOAD35058ARR2(java.lang.Object(ARRAY(i4[3], a115115data[3])), i5816[3], java.lang.Object(Tree(o96140[3], o96141[3])), java.lang.Object(java.lang.String(i5968[3]))), LOAD35058ARR2(java.lang.Object(ARRAY(i4[4], a115115data[4])), i5816[4], java.lang.Object(Tree(o96140[4], java.lang.Object(Tree(o96140[4], o96141[4])))), java.lang.Object(java.lang.String(i5968[4]))) → COND_LOAD35058ARR2(&&(&&(&&(>(i5968[4], 42), >(i5816[4], 0)), <(i5816[4], i4[4])), >(+(i5816[4], 1), 0)), java.lang.Object(ARRAY(i4[4], a115115data[4])), i5816[4], java.lang.Object(Tree(o96140[4], java.lang.Object(Tree(o96140[4], o96141[4])))), java.lang.Object(java.lang.String(i5968[4]))) which results in the following constraint:
(31)    (i4[2]=i4[3]∧a115115data[2]=a115115data[3]∧+(i5816[2], 1)=i5816[3]∧o96126[2]=java.lang.Object(Tree(o96140[3], o96141[3]))∧o96140[3]=o96140[4]∧o96141[3]=java.lang.Object(Tree(o96140[4], o96141[4]))∧i4[3]=i4[4]∧a115115data[3]=a115115data[4]∧i5968[3]=i5968[4]∧i5816[3]=i5816[4] ⇒ LOAD35058(java.lang.Object(ARRAY(i4[3], a115115data[3])), i5816[3], java.lang.Object(Tree(o96140[3], o96141[3])))≥LOAD35058ARR2(java.lang.Object(ARRAY(i4[3], a115115data[3])), i5816[3], java.lang.Object(Tree(o96140[3], o96141[3])), java.lang.Object(java.lang.String(i5968[3])))∧(U^Increasing(LOAD35058ARR2(java.lang.Object(ARRAY(i4[3], a115115data[3])), i5816[3], java.lang.Object(Tree(o96140[3], o96141[3])), java.lang.Object(java.lang.String(i5968[3])))), ≥))

We simplified constraint (31) using rules (III), (IV) which results in the following new constraint:
(32)    (LOAD35058(java.lang.Object(ARRAY(i4[2], a115115data[2])), +(i5816[2], 1), java.lang.Object(Tree(o96140[3], java.lang.Object(Tree(o96140[3], o96141[4])))))≥LOAD35058ARR2(java.lang.Object(ARRAY(i4[2], a115115data[2])), +(i5816[2], 1), java.lang.Object(Tree(o96140[3], java.lang.Object(Tree(o96140[3], o96141[4])))), java.lang.Object(java.lang.String(i5968[3])))∧(U^Increasing(LOAD35058ARR2(java.lang.Object(ARRAY(i4[3], a115115data[3])), i5816[3], java.lang.Object(Tree(o96140[3], o96141[3])), java.lang.Object(java.lang.String(i5968[3])))), ≥))

We simplified constraint (32) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(33)    ((U^Increasing(LOAD35058ARR2(java.lang.Object(ARRAY(i4[3], a115115data[3])), i5816[3], java.lang.Object(Tree(o96140[3], o96141[3])), java.lang.Object(java.lang.String(i5968[3])))), ≥)∧[(-1)bso_40] ≥ 0)

We simplified constraint (33) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(34)    ((U^Increasing(LOAD35058ARR2(java.lang.Object(ARRAY(i4[3], a115115data[3])), i5816[3], java.lang.Object(Tree(o96140[3], o96141[3])), java.lang.Object(java.lang.String(i5968[3])))), ≥)∧[(-1)bso_40] ≥ 0)

We simplified constraint (34) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(35)    ((U^Increasing(LOAD35058ARR2(java.lang.Object(ARRAY(i4[3], a115115data[3])), i5816[3], java.lang.Object(Tree(o96140[3], o96141[3])), java.lang.Object(java.lang.String(i5968[3])))), ≥)∧[(-1)bso_40] ≥ 0)

We simplified constraint (35) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:
(36)    ((U^Increasing(LOAD35058ARR2(java.lang.Object(ARRAY(i4[3], a115115data[3])), i5816[3], java.lang.Object(Tree(o96140[3], o96141[3])), java.lang.Object(java.lang.String(i5968[3])))), ≥)∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[(-1)bso_40] ≥ 0)
We consider the chain COND_LOAD35058ARR2(TRUE, java.lang.Object(ARRAY(i4[5], a115115data[5])), i5816[5], java.lang.Object(Tree(o96140[5], java.lang.Object(Tree(o96140[5], o96141[5])))), java.lang.Object(java.lang.String(i5968[5]))) → LOAD35058(java.lang.Object(ARRAY(i4[5], a115115data[5])), +(i5816[5], 1), o96140[5]), LOAD35058(java.lang.Object(ARRAY(i4[3], a115115data[3])), i5816[3], java.lang.Object(Tree(o96140[3], o96141[3]))) → LOAD35058ARR2(java.lang.Object(ARRAY(i4[3], a115115data[3])), i5816[3], java.lang.Object(Tree(o96140[3], o96141[3])), java.lang.Object(java.lang.String(i5968[3]))), LOAD35058ARR2(java.lang.Object(ARRAY(i4[4], a115115data[4])), i5816[4], java.lang.Object(Tree(o96140[4], java.lang.Object(Tree(o96140[4], o96141[4])))), java.lang.Object(java.lang.String(i5968[4]))) → COND_LOAD35058ARR2(&&(&&(&&(>(i5968[4], 42), >(i5816[4], 0)), <(i5816[4], i4[4])), >(+(i5816[4], 1), 0)), java.lang.Object(ARRAY(i4[4], a115115data[4])), i5816[4], java.lang.Object(Tree(o96140[4], java.lang.Object(Tree(o96140[4], o96141[4])))), java.lang.Object(java.lang.String(i5968[4]))) which results in the following constraint:
(37)    (+(i5816[5], 1)=i5816[3]∧i4[5]=i4[3]∧a115115data[5]=a115115data[3]∧o96140[5]=java.lang.Object(Tree(o96140[3], o96141[3]))∧o96140[3]=o96140[4]∧o96141[3]=java.lang.Object(Tree(o96140[4], o96141[4]))∧i4[3]=i4[4]∧a115115data[3]=a115115data[4]∧i5968[3]=i5968[4]∧i5816[3]=i5816[4] ⇒ LOAD35058(java.lang.Object(ARRAY(i4[3], a115115data[3])), i5816[3], java.lang.Object(Tree(o96140[3], o96141[3])))≥LOAD35058ARR2(java.lang.Object(ARRAY(i4[3], a115115data[3])), i5816[3], java.lang.Object(Tree(o96140[3], o96141[3])), java.lang.Object(java.lang.String(i5968[3])))∧(U^Increasing(LOAD35058ARR2(java.lang.Object(ARRAY(i4[3], a115115data[3])), i5816[3], java.lang.Object(Tree(o96140[3], o96141[3])), java.lang.Object(java.lang.String(i5968[3])))), ≥))

We simplified constraint (37) using rules (III), (IV) which results in the following new constraint:
(38)    (LOAD35058(java.lang.Object(ARRAY(i4[5], a115115data[5])), +(i5816[5], 1), java.lang.Object(Tree(o96140[3], java.lang.Object(Tree(o96140[3], o96141[4])))))≥LOAD35058ARR2(java.lang.Object(ARRAY(i4[5], a115115data[5])), +(i5816[5], 1), java.lang.Object(Tree(o96140[3], java.lang.Object(Tree(o96140[3], o96141[4])))), java.lang.Object(java.lang.String(i5968[3])))∧(U^Increasing(LOAD35058ARR2(java.lang.Object(ARRAY(i4[3], a115115data[3])), i5816[3], java.lang.Object(Tree(o96140[3], o96141[3])), java.lang.Object(java.lang.String(i5968[3])))), ≥))

We simplified constraint (38) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(39)    ((U^Increasing(LOAD35058ARR2(java.lang.Object(ARRAY(i4[3], a115115data[3])), i5816[3], java.lang.Object(Tree(o96140[3], o96141[3])), java.lang.Object(java.lang.String(i5968[3])))), ≥)∧[(-1)bso_40] ≥ 0)

We simplified constraint (39) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(40)    ((U^Increasing(LOAD35058ARR2(java.lang.Object(ARRAY(i4[3], a115115data[3])), i5816[3], java.lang.Object(Tree(o96140[3], o96141[3])), java.lang.Object(java.lang.String(i5968[3])))), ≥)∧[(-1)bso_40] ≥ 0)

We simplified constraint (40) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(41)    ((U^Increasing(LOAD35058ARR2(java.lang.Object(ARRAY(i4[3], a115115data[3])), i5816[3], java.lang.Object(Tree(o96140[3], o96141[3])), java.lang.Object(java.lang.String(i5968[3])))), ≥)∧[(-1)bso_40] ≥ 0)

We simplified constraint (41) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:
(42)    ((U^Increasing(LOAD35058ARR2(java.lang.Object(ARRAY(i4[3], a115115data[3])), i5816[3], java.lang.Object(Tree(o96140[3], o96141[3])), java.lang.Object(java.lang.String(i5968[3])))), ≥)∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[(-1)bso_40] ≥ 0)

For Pair LOAD35058ARR2(java.lang.Object(ARRAY(i4, a115115data)), i5816, java.lang.Object(Tree(o96140, java.lang.Object(Tree(o96140, o96141)))), java.lang.Object(java.lang.String(i5968))) → COND_LOAD35058ARR2(&&(&&(&&(>(i5968, 42), >(i5816, 0)), <(i5816, i4)), >(+(i5816, 1), 0)), java.lang.Object(ARRAY(i4, a115115data)), i5816, java.lang.Object(Tree(o96140, java.lang.Object(Tree(o96140, o96141)))), java.lang.Object(java.lang.String(i5968))) the following chains were created:

We consider the chain LOAD35058ARR2(java.lang.Object(ARRAY(i4[4], a115115data[4])), i5816[4], java.lang.Object(Tree(o96140[4], java.lang.Object(Tree(o96140[4], o96141[4])))), java.lang.Object(java.lang.String(i5968[4]))) → COND_LOAD35058ARR2(&&(&&(&&(>(i5968[4], 42), >(i5816[4], 0)), <(i5816[4], i4[4])), >(+(i5816[4], 1), 0)), java.lang.Object(ARRAY(i4[4], a115115data[4])), i5816[4], java.lang.Object(Tree(o96140[4], java.lang.Object(Tree(o96140[4], o96141[4])))), java.lang.Object(java.lang.String(i5968[4]))), COND_LOAD35058ARR2(TRUE, java.lang.Object(ARRAY(i4[5], a115115data[5])), i5816[5], java.lang.Object(Tree(o96140[5], java.lang.Object(Tree(o96140[5], o96141[5])))), java.lang.Object(java.lang.String(i5968[5]))) → LOAD35058(java.lang.Object(ARRAY(i4[5], a115115data[5])), +(i5816[5], 1), o96140[5]) which results in the following constraint:
(43)    (i5816[4]=i5816[5]∧i4[4]=i4[5]∧a115115data[4]=a115115data[5]∧&&(&&(&&(>(i5968[4], 42), >(i5816[4], 0)), <(i5816[4], i4[4])), >(+(i5816[4], 1), 0))=TRUE∧i5968[4]=i5968[5]∧o96140[4]=o96140[5]∧o96141[4]=o96141[5] ⇒ LOAD35058ARR2(java.lang.Object(ARRAY(i4[4], a115115data[4])), i5816[4], java.lang.Object(Tree(o96140[4], java.lang.Object(Tree(o96140[4], o96141[4])))), java.lang.Object(java.lang.String(i5968[4])))≥COND_LOAD35058ARR2(&&(&&(&&(>(i5968[4], 42), >(i5816[4], 0)), <(i5816[4], i4[4])), >(+(i5816[4], 1), 0)), java.lang.Object(ARRAY(i4[4], a115115data[4])), i5816[4], java.lang.Object(Tree(o96140[4], java.lang.Object(Tree(o96140[4], o96141[4])))), java.lang.Object(java.lang.String(i5968[4])))∧(U^Increasing(COND_LOAD35058ARR2(&&(&&(&&(>(i5968[4], 42), >(i5816[4], 0)), <(i5816[4], i4[4])), >(+(i5816[4], 1), 0)), java.lang.Object(ARRAY(i4[4], a115115data[4])), i5816[4], java.lang.Object(Tree(o96140[4], java.lang.Object(Tree(o96140[4], o96141[4])))), java.lang.Object(java.lang.String(i5968[4])))), ≥))

We simplified constraint (43) using rule (IV) which results in the following new constraint:
(44)    (&&(&&(&&(>(i5968[4], 42), >(i5816[4], 0)), <(i5816[4], i4[4])), >(+(i5816[4], 1), 0))=TRUE ⇒ LOAD35058ARR2(java.lang.Object(ARRAY(i4[4], a115115data[4])), i5816[4], java.lang.Object(Tree(o96140[4], java.lang.Object(Tree(o96140[4], o96141[4])))), java.lang.Object(java.lang.String(i5968[4])))≥COND_LOAD35058ARR2(&&(&&(&&(>(i5968[4], 42), >(i5816[4], 0)), <(i5816[4], i4[4])), >(+(i5816[4], 1), 0)), java.lang.Object(ARRAY(i4[4], a115115data[4])), i5816[4], java.lang.Object(Tree(o96140[4], java.lang.Object(Tree(o96140[4], o96141[4])))), java.lang.Object(java.lang.String(i5968[4])))∧(U^Increasing(COND_LOAD35058ARR2(&&(&&(&&(>(i5968[4], 42), >(i5816[4], 0)), <(i5816[4], i4[4])), >(+(i5816[4], 1), 0)), java.lang.Object(ARRAY(i4[4], a115115data[4])), i5816[4], java.lang.Object(Tree(o96140[4], java.lang.Object(Tree(o96140[4], o96141[4])))), java.lang.Object(java.lang.String(i5968[4])))), ≥))

We simplified constraint (44) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(45)    (0 ≥ 0 ⇒ (U^Increasing(COND_LOAD35058ARR2(&&(&&(&&(>(i5968[4], 42), >(i5816[4], 0)), <(i5816[4], i4[4])), >(+(i5816[4], 1), 0)), java.lang.Object(ARRAY(i4[4], a115115data[4])), i5816[4], java.lang.Object(Tree(o96140[4], java.lang.Object(Tree(o96140[4], o96141[4])))), java.lang.Object(java.lang.String(i5968[4])))), ≥)∧[16 + (-1)bso_41] + [16]o96141[4] + [20]o96140[4] + i5816[4] ≥ 0)

We simplified constraint (45) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(46)    (0 ≥ 0 ⇒ (U^Increasing(COND_LOAD35058ARR2(&&(&&(&&(>(i5968[4], 42), >(i5816[4], 0)), <(i5816[4], i4[4])), >(+(i5816[4], 1), 0)), java.lang.Object(ARRAY(i4[4], a115115data[4])), i5816[4], java.lang.Object(Tree(o96140[4], java.lang.Object(Tree(o96140[4], o96141[4])))), java.lang.Object(java.lang.String(i5968[4])))), ≥)∧[16 + (-1)bso_41] + [16]o96141[4] + [20]o96140[4] + i5816[4] ≥ 0)

We simplified constraint (46) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(47)    (0 ≥ 0 ⇒ (U^Increasing(COND_LOAD35058ARR2(&&(&&(&&(>(i5968[4], 42), >(i5816[4], 0)), <(i5816[4], i4[4])), >(+(i5816[4], 1), 0)), java.lang.Object(ARRAY(i4[4], a115115data[4])), i5816[4], java.lang.Object(Tree(o96140[4], java.lang.Object(Tree(o96140[4], o96141[4])))), java.lang.Object(java.lang.String(i5968[4])))), ≥)∧[16 + (-1)bso_41] + [16]o96141[4] + [20]o96140[4] + i5816[4] ≥ 0)

We simplified constraint (47) using rules (IDP_UNRESTRICTED_VARS), (IDP_POLY_GCD) which results in the following new constraint:
(48)    (0 ≥ 0 ⇒ (U^Increasing(COND_LOAD35058ARR2(&&(&&(&&(>(i5968[4], 42), >(i5816[4], 0)), <(i5816[4], i4[4])), >(+(i5816[4], 1), 0)), java.lang.Object(ARRAY(i4[4], a115115data[4])), i5816[4], java.lang.Object(Tree(o96140[4], java.lang.Object(Tree(o96140[4], o96141[4])))), java.lang.Object(java.lang.String(i5968[4])))), ≥)∧0 ≥ 0∧[1] ≥ 0∧0 ≥ 0∧0 ≥ 0∧[16 + (-1)bso_41] ≥ 0∧[1] ≥ 0∧[1] ≥ 0)

For Pair COND_LOAD35058ARR2(TRUE, java.lang.Object(ARRAY(i4, a115115data)), i5816, java.lang.Object(Tree(o96140, java.lang.Object(Tree(o96140, o96141)))), java.lang.Object(java.lang.String(i5968))) → LOAD35058(java.lang.Object(ARRAY(i4, a115115data)), +(i5816, 1), o96140) the following chains were created:

We consider the chain LOAD35058ARR2(java.lang.Object(ARRAY(i4[4], a115115data[4])), i5816[4], java.lang.Object(Tree(o96140[4], java.lang.Object(Tree(o96140[4], o96141[4])))), java.lang.Object(java.lang.String(i5968[4]))) → COND_LOAD35058ARR2(&&(&&(&&(>(i5968[4], 42), >(i5816[4], 0)), <(i5816[4], i4[4])), >(+(i5816[4], 1), 0)), java.lang.Object(ARRAY(i4[4], a115115data[4])), i5816[4], java.lang.Object(Tree(o96140[4], java.lang.Object(Tree(o96140[4], o96141[4])))), java.lang.Object(java.lang.String(i5968[4]))), COND_LOAD35058ARR2(TRUE, java.lang.Object(ARRAY(i4[5], a115115data[5])), i5816[5], java.lang.Object(Tree(o96140[5], java.lang.Object(Tree(o96140[5], o96141[5])))), java.lang.Object(java.lang.String(i5968[5]))) → LOAD35058(java.lang.Object(ARRAY(i4[5], a115115data[5])), +(i5816[5], 1), o96140[5]), LOAD35058(java.lang.Object(ARRAY(i4[0], a115115data[0])), i5816[0], java.lang.Object(Tree(o96125[0], o96126[0]))) → LOAD35058ARR1(java.lang.Object(ARRAY(i4[0], a115115data[0])), i5816[0], java.lang.Object(Tree(o96125[0], o96126[0])), java.lang.Object(java.lang.String(i5968[0]))) which results in the following constraint:
(49)    (i5816[4]=i5816[5]∧i4[4]=i4[5]∧a115115data[4]=a115115data[5]∧&&(&&(&&(>(i5968[4], 42), >(i5816[4], 0)), <(i5816[4], i4[4])), >(+(i5816[4], 1), 0))=TRUE∧i5968[4]=i5968[5]∧o96140[4]=o96140[5]∧o96141[4]=o96141[5]∧i4[5]=i4[0]∧a115115data[5]=a115115data[0]∧+(i5816[5], 1)=i5816[0]∧o96140[5]=java.lang.Object(Tree(o96125[0], o96126[0])) ⇒ COND_LOAD35058ARR2(TRUE, java.lang.Object(ARRAY(i4[5], a115115data[5])), i5816[5], java.lang.Object(Tree(o96140[5], java.lang.Object(Tree(o96140[5], o96141[5])))), java.lang.Object(java.lang.String(i5968[5])))≥LOAD35058(java.lang.Object(ARRAY(i4[5], a115115data[5])), +(i5816[5], 1), o96140[5])∧(U^Increasing(LOAD35058(java.lang.Object(ARRAY(i4[5], a115115data[5])), +(i5816[5], 1), o96140[5])), ≥))

We simplified constraint (49) using rules (III), (IV) which results in the following new constraint:
(50)    (&&(&&(&&(>(i5968[4], 42), >(i5816[4], 0)), <(i5816[4], i4[4])), >(+(i5816[4], 1), 0))=TRUE ⇒ COND_LOAD35058ARR2(TRUE, java.lang.Object(ARRAY(i4[4], a115115data[4])), i5816[4], java.lang.Object(Tree(java.lang.Object(Tree(o96125[0], o96126[0])), java.lang.Object(Tree(java.lang.Object(Tree(o96125[0], o96126[0])), o96141[4])))), java.lang.Object(java.lang.String(i5968[4])))≥LOAD35058(java.lang.Object(ARRAY(i4[4], a115115data[4])), +(i5816[4], 1), java.lang.Object(Tree(o96125[0], o96126[0])))∧(U^Increasing(LOAD35058(java.lang.Object(ARRAY(i4[5], a115115data[5])), +(i5816[5], 1), o96140[5])), ≥))

We simplified constraint (50) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(51)    (0 ≥ 0 ⇒ (U^Increasing(LOAD35058(java.lang.Object(ARRAY(i4[5], a115115data[5])), +(i5816[5], 1), o96140[5])), ≥)∧[96 + (-1)bso_42] + [16]o96141[4] + [72]o96126[0] + [72]o96125[0] + i5816[4] ≥ 0)

We simplified constraint (51) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(52)    (0 ≥ 0 ⇒ (U^Increasing(LOAD35058(java.lang.Object(ARRAY(i4[5], a115115data[5])), +(i5816[5], 1), o96140[5])), ≥)∧[96 + (-1)bso_42] + [16]o96141[4] + [72]o96126[0] + [72]o96125[0] + i5816[4] ≥ 0)

We simplified constraint (52) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(53)    (0 ≥ 0 ⇒ (U^Increasing(LOAD35058(java.lang.Object(ARRAY(i4[5], a115115data[5])), +(i5816[5], 1), o96140[5])), ≥)∧[96 + (-1)bso_42] + [16]o96141[4] + [72]o96126[0] + [72]o96125[0] + i5816[4] ≥ 0)

We simplified constraint (53) using rules (IDP_UNRESTRICTED_VARS), (IDP_POLY_GCD) which results in the following new constraint:
(54)    (0 ≥ 0 ⇒ (U^Increasing(LOAD35058(java.lang.Object(ARRAY(i4[5], a115115data[5])), +(i5816[5], 1), o96140[5])), ≥)∧0 ≥ 0∧[1] ≥ 0∧0 ≥ 0∧0 ≥ 0∧[96 + (-1)bso_42] ≥ 0∧[1] ≥ 0∧[1] ≥ 0∧[1] ≥ 0)
We consider the chain LOAD35058ARR2(java.lang.Object(ARRAY(i4[4], a115115data[4])), i5816[4], java.lang.Object(Tree(o96140[4], java.lang.Object(Tree(o96140[4], o96141[4])))), java.lang.Object(java.lang.String(i5968[4]))) → COND_LOAD35058ARR2(&&(&&(&&(>(i5968[4], 42), >(i5816[4], 0)), <(i5816[4], i4[4])), >(+(i5816[4], 1), 0)), java.lang.Object(ARRAY(i4[4], a115115data[4])), i5816[4], java.lang.Object(Tree(o96140[4], java.lang.Object(Tree(o96140[4], o96141[4])))), java.lang.Object(java.lang.String(i5968[4]))), COND_LOAD35058ARR2(TRUE, java.lang.Object(ARRAY(i4[5], a115115data[5])), i5816[5], java.lang.Object(Tree(o96140[5], java.lang.Object(Tree(o96140[5], o96141[5])))), java.lang.Object(java.lang.String(i5968[5]))) → LOAD35058(java.lang.Object(ARRAY(i4[5], a115115data[5])), +(i5816[5], 1), o96140[5]), LOAD35058(java.lang.Object(ARRAY(i4[3], a115115data[3])), i5816[3], java.lang.Object(Tree(o96140[3], o96141[3]))) → LOAD35058ARR2(java.lang.Object(ARRAY(i4[3], a115115data[3])), i5816[3], java.lang.Object(Tree(o96140[3], o96141[3])), java.lang.Object(java.lang.String(i5968[3]))) which results in the following constraint:
(55)    (i5816[4]=i5816[5]∧i4[4]=i4[5]∧a115115data[4]=a115115data[5]∧&&(&&(&&(>(i5968[4], 42), >(i5816[4], 0)), <(i5816[4], i4[4])), >(+(i5816[4], 1), 0))=TRUE∧i5968[4]=i5968[5]∧o96140[4]=o96140[5]∧o96141[4]=o96141[5]∧+(i5816[5], 1)=i5816[3]∧i4[5]=i4[3]∧a115115data[5]=a115115data[3]∧o96140[5]=java.lang.Object(Tree(o96140[3], o96141[3])) ⇒ COND_LOAD35058ARR2(TRUE, java.lang.Object(ARRAY(i4[5], a115115data[5])), i5816[5], java.lang.Object(Tree(o96140[5], java.lang.Object(Tree(o96140[5], o96141[5])))), java.lang.Object(java.lang.String(i5968[5])))≥LOAD35058(java.lang.Object(ARRAY(i4[5], a115115data[5])), +(i5816[5], 1), o96140[5])∧(U^Increasing(LOAD35058(java.lang.Object(ARRAY(i4[5], a115115data[5])), +(i5816[5], 1), o96140[5])), ≥))

We simplified constraint (55) using rules (III), (IV) which results in the following new constraint:
(56)    (&&(&&(&&(>(i5968[4], 42), >(i5816[4], 0)), <(i5816[4], i4[4])), >(+(i5816[4], 1), 0))=TRUE ⇒ COND_LOAD35058ARR2(TRUE, java.lang.Object(ARRAY(i4[4], a115115data[4])), i5816[4], java.lang.Object(Tree(java.lang.Object(Tree(o96140[3], o96141[3])), java.lang.Object(Tree(java.lang.Object(Tree(o96140[3], o96141[3])), o96141[4])))), java.lang.Object(java.lang.String(i5968[4])))≥LOAD35058(java.lang.Object(ARRAY(i4[4], a115115data[4])), +(i5816[4], 1), java.lang.Object(Tree(o96140[3], o96141[3])))∧(U^Increasing(LOAD35058(java.lang.Object(ARRAY(i4[5], a115115data[5])), +(i5816[5], 1), o96140[5])), ≥))

We simplified constraint (56) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(57)    (0 ≥ 0 ⇒ (U^Increasing(LOAD35058(java.lang.Object(ARRAY(i4[5], a115115data[5])), +(i5816[5], 1), o96140[5])), ≥)∧[96 + (-1)bso_42] + [16]o96141[4] + [72]o96141[3] + [72]o96140[3] + i5816[4] ≥ 0)

We simplified constraint (57) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(58)    (0 ≥ 0 ⇒ (U^Increasing(LOAD35058(java.lang.Object(ARRAY(i4[5], a115115data[5])), +(i5816[5], 1), o96140[5])), ≥)∧[96 + (-1)bso_42] + [16]o96141[4] + [72]o96141[3] + [72]o96140[3] + i5816[4] ≥ 0)

We simplified constraint (58) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(59)    (0 ≥ 0 ⇒ (U^Increasing(LOAD35058(java.lang.Object(ARRAY(i4[5], a115115data[5])), +(i5816[5], 1), o96140[5])), ≥)∧[96 + (-1)bso_42] + [16]o96141[4] + [72]o96141[3] + [72]o96140[3] + i5816[4] ≥ 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(LOAD35058(java.lang.Object(ARRAY(i4[5], a115115data[5])), +(i5816[5], 1), o96140[5])), ≥)∧0 ≥ 0∧[1] ≥ 0∧0 ≥ 0∧0 ≥ 0∧[96 + (-1)bso_42] ≥ 0∧[1] ≥ 0∧[1] ≥ 0∧[1] ≥ 0)

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

LOAD35058(java.lang.Object(ARRAY(i4, a115115data)), i5816, java.lang.Object(Tree(o96125, o96126))) → LOAD35058ARR1(java.lang.Object(ARRAY(i4, a115115data)), i5816, java.lang.Object(Tree(o96125, o96126)), java.lang.Object(java.lang.String(i5968)))
- ((U^Increasing(LOAD35058ARR1(java.lang.Object(ARRAY(i4[0], a115115data[0])), i5816[0], java.lang.Object(Tree(o96125[0], o96126[0])), java.lang.Object(java.lang.String(i5968[0])))), ≥)∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[3 + (-1)bso_37] ≥ 0)
- ((U^Increasing(LOAD35058ARR1(java.lang.Object(ARRAY(i4[0], a115115data[0])), i5816[0], java.lang.Object(Tree(o96125[0], o96126[0])), java.lang.Object(java.lang.String(i5968[0])))), ≥)∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[3 + (-1)bso_37] ≥ 0)
LOAD35058ARR1(java.lang.Object(ARRAY(i4, a115115data)), i5816, java.lang.Object(Tree(java.lang.Object(Tree(o96125, o96126)), o96126)), java.lang.Object(java.lang.String(i5968))) → COND_LOAD35058ARR1(&&(&&(&&(<=(i5968, 42), >(i5816, 0)), <(i5816, i4)), >(+(i5816, 1), 0)), java.lang.Object(ARRAY(i4, a115115data)), i5816, java.lang.Object(Tree(java.lang.Object(Tree(o96125, o96126)), o96126)), java.lang.Object(java.lang.String(i5968)))
- (0 ≥ 0 ⇒ (U^Increasing(COND_LOAD35058ARR1(&&(&&(&&(<=(i5968[1], 42), >(i5816[1], 0)), <(i5816[1], i4[1])), >(+(i5816[1], 1), 0)), java.lang.Object(ARRAY(i4[1], a115115data[1])), i5816[1], java.lang.Object(Tree(java.lang.Object(Tree(o96125[1], o96126[1])), o96126[1])), java.lang.Object(java.lang.String(i5968[1])))), ≥)∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[3 + (-1)bso_38] ≥ 0)
COND_LOAD35058ARR1(TRUE, java.lang.Object(ARRAY(i4, a115115data)), i5816, java.lang.Object(Tree(java.lang.Object(Tree(o96125, o96126)), o96126)), java.lang.Object(java.lang.String(i5968))) → LOAD35058(java.lang.Object(ARRAY(i4, a115115data)), +(i5816, 1), o96126)
- (0 ≥ 0 ⇒ (U^Increasing(LOAD35058(java.lang.Object(ARRAY(i4[2], a115115data[2])), +(i5816[2], 1), o96126[2])), ≥)∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[186 + (-1)bso_39] ≥ 0∧[1] ≥ 0∧[1] ≥ 0∧[1] ≥ 0)
- (0 ≥ 0 ⇒ (U^Increasing(LOAD35058(java.lang.Object(ARRAY(i4[2], a115115data[2])), +(i5816[2], 1), o96126[2])), ≥)∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[186 + (-1)bso_39] ≥ 0∧[1] ≥ 0∧[1] ≥ 0∧[1] ≥ 0)
LOAD35058(java.lang.Object(ARRAY(i4, a115115data)), i5816, java.lang.Object(Tree(o96140, o96141))) → LOAD35058ARR2(java.lang.Object(ARRAY(i4, a115115data)), i5816, java.lang.Object(Tree(o96140, o96141)), java.lang.Object(java.lang.String(i5968)))
- ((U^Increasing(LOAD35058ARR2(java.lang.Object(ARRAY(i4[3], a115115data[3])), i5816[3], java.lang.Object(Tree(o96140[3], o96141[3])), java.lang.Object(java.lang.String(i5968[3])))), ≥)∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[(-1)bso_40] ≥ 0)
- ((U^Increasing(LOAD35058ARR2(java.lang.Object(ARRAY(i4[3], a115115data[3])), i5816[3], java.lang.Object(Tree(o96140[3], o96141[3])), java.lang.Object(java.lang.String(i5968[3])))), ≥)∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[(-1)bso_40] ≥ 0)
LOAD35058ARR2(java.lang.Object(ARRAY(i4, a115115data)), i5816, java.lang.Object(Tree(o96140, java.lang.Object(Tree(o96140, o96141)))), java.lang.Object(java.lang.String(i5968))) → COND_LOAD35058ARR2(&&(&&(&&(>(i5968, 42), >(i5816, 0)), <(i5816, i4)), >(+(i5816, 1), 0)), java.lang.Object(ARRAY(i4, a115115data)), i5816, java.lang.Object(Tree(o96140, java.lang.Object(Tree(o96140, o96141)))), java.lang.Object(java.lang.String(i5968)))
- (0 ≥ 0 ⇒ (U^Increasing(COND_LOAD35058ARR2(&&(&&(&&(>(i5968[4], 42), >(i5816[4], 0)), <(i5816[4], i4[4])), >(+(i5816[4], 1), 0)), java.lang.Object(ARRAY(i4[4], a115115data[4])), i5816[4], java.lang.Object(Tree(o96140[4], java.lang.Object(Tree(o96140[4], o96141[4])))), java.lang.Object(java.lang.String(i5968[4])))), ≥)∧0 ≥ 0∧[1] ≥ 0∧0 ≥ 0∧0 ≥ 0∧[16 + (-1)bso_41] ≥ 0∧[1] ≥ 0∧[1] ≥ 0)
COND_LOAD35058ARR2(TRUE, java.lang.Object(ARRAY(i4, a115115data)), i5816, java.lang.Object(Tree(o96140, java.lang.Object(Tree(o96140, o96141)))), java.lang.Object(java.lang.String(i5968))) → LOAD35058(java.lang.Object(ARRAY(i4, a115115data)), +(i5816, 1), o96140)
- (0 ≥ 0 ⇒ (U^Increasing(LOAD35058(java.lang.Object(ARRAY(i4[5], a115115data[5])), +(i5816[5], 1), o96140[5])), ≥)∧0 ≥ 0∧[1] ≥ 0∧0 ≥ 0∧0 ≥ 0∧[96 + (-1)bso_42] ≥ 0∧[1] ≥ 0∧[1] ≥ 0∧[1] ≥ 0)
- (0 ≥ 0 ⇒ (U^Increasing(LOAD35058(java.lang.Object(ARRAY(i4[5], a115115data[5])), +(i5816[5], 1), o96140[5])), ≥)∧0 ≥ 0∧[1] ≥ 0∧0 ≥ 0∧0 ≥ 0∧[96 + (-1)bso_42] ≥ 0∧[1] ≥ 0∧[1] ≥ 0∧[1] ≥ 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 with natural coefficients for all symbols [NONINF][POLO]:

POL(TRUE) = 0
POL(FALSE) = 0
POL(LOAD35058(x₁, x₂, x₃)) = [2]x₃ + [2]x₁
POL(java.lang.Object(x₁)) = [2]x₁
POL(ARRAY(x₁, x₂)) = [2]
POL(Tree(x₁, x₂)) = [2] + [2]x₂ + [2]x₁
POL(LOAD35058ARR1(x₁, x₂, x₃, x₄)) = [1] + x₄ + [2]x₃
POL(java.lang.String(x₁)) = [2]
POL(COND_LOAD35058ARR1(x₁, x₂, x₃, x₄, x₅)) = [2] + [2]x₄
POL(&&(x₁, x₂)) = 0
POL(<=(x₁, x₂)) = 0
POL(42) = 0
POL(>(x₁, x₂)) = 0
POL(0) = 0
POL(<(x₁, x₂)) = 0
POL(+(x₁, x₂)) = 0
POL(1) = 0
POL(LOAD35058ARR2(x₁, x₂, x₃, x₄)) = [2]x₃ + [2]x₂ + [2]x₁
POL(COND_LOAD35058ARR2(x₁, x₂, x₃, x₄, x₅)) = [3]x₅ + x₄ + x₃

The following pairs are in P_>:

LOAD35058(java.lang.Object(ARRAY(i4[0], a115115data[0])), i5816[0], java.lang.Object(Tree(o96125[0], o96126[0]))) → LOAD35058ARR1(java.lang.Object(ARRAY(i4[0], a115115data[0])), i5816[0], java.lang.Object(Tree(o96125[0], o96126[0])), java.lang.Object(java.lang.String(i5968[0])))
LOAD35058ARR1(java.lang.Object(ARRAY(i4[1], a115115data[1])), i5816[1], java.lang.Object(Tree(java.lang.Object(Tree(o96125[1], o96126[1])), o96126[1])), java.lang.Object(java.lang.String(i5968[1]))) → COND_LOAD35058ARR1(&&(&&(&&(<=(i5968[1], 42), >(i5816[1], 0)), <(i5816[1], i4[1])), >(+(i5816[1], 1), 0)), java.lang.Object(ARRAY(i4[1], a115115data[1])), i5816[1], java.lang.Object(Tree(java.lang.Object(Tree(o96125[1], o96126[1])), o96126[1])), java.lang.Object(java.lang.String(i5968[1])))
COND_LOAD35058ARR1(TRUE, java.lang.Object(ARRAY(i4[2], a115115data[2])), i5816[2], java.lang.Object(Tree(java.lang.Object(Tree(o96125[2], o96126[2])), o96126[2])), java.lang.Object(java.lang.String(i5968[2]))) → LOAD35058(java.lang.Object(ARRAY(i4[2], a115115data[2])), +(i5816[2], 1), o96126[2])
LOAD35058ARR2(java.lang.Object(ARRAY(i4[4], a115115data[4])), i5816[4], java.lang.Object(Tree(o96140[4], java.lang.Object(Tree(o96140[4], o96141[4])))), java.lang.Object(java.lang.String(i5968[4]))) → COND_LOAD35058ARR2(&&(&&(&&(>(i5968[4], 42), >(i5816[4], 0)), <(i5816[4], i4[4])), >(+(i5816[4], 1), 0)), java.lang.Object(ARRAY(i4[4], a115115data[4])), i5816[4], java.lang.Object(Tree(o96140[4], java.lang.Object(Tree(o96140[4], o96141[4])))), java.lang.Object(java.lang.String(i5968[4])))
COND_LOAD35058ARR2(TRUE, java.lang.Object(ARRAY(i4[5], a115115data[5])), i5816[5], java.lang.Object(Tree(o96140[5], java.lang.Object(Tree(o96140[5], o96141[5])))), java.lang.Object(java.lang.String(i5968[5]))) → LOAD35058(java.lang.Object(ARRAY(i4[5], a115115data[5])), +(i5816[5], 1), o96140[5])

The following pairs are in P_bound:

LOAD35058(java.lang.Object(ARRAY(i4[0], a115115data[0])), i5816[0], java.lang.Object(Tree(o96125[0], o96126[0]))) → LOAD35058ARR1(java.lang.Object(ARRAY(i4[0], a115115data[0])), i5816[0], java.lang.Object(Tree(o96125[0], o96126[0])), java.lang.Object(java.lang.String(i5968[0])))
LOAD35058ARR1(java.lang.Object(ARRAY(i4[1], a115115data[1])), i5816[1], java.lang.Object(Tree(java.lang.Object(Tree(o96125[1], o96126[1])), o96126[1])), java.lang.Object(java.lang.String(i5968[1]))) → COND_LOAD35058ARR1(&&(&&(&&(<=(i5968[1], 42), >(i5816[1], 0)), <(i5816[1], i4[1])), >(+(i5816[1], 1), 0)), java.lang.Object(ARRAY(i4[1], a115115data[1])), i5816[1], java.lang.Object(Tree(java.lang.Object(Tree(o96125[1], o96126[1])), o96126[1])), java.lang.Object(java.lang.String(i5968[1])))
COND_LOAD35058ARR1(TRUE, java.lang.Object(ARRAY(i4[2], a115115data[2])), i5816[2], java.lang.Object(Tree(java.lang.Object(Tree(o96125[2], o96126[2])), o96126[2])), java.lang.Object(java.lang.String(i5968[2]))) → LOAD35058(java.lang.Object(ARRAY(i4[2], a115115data[2])), +(i5816[2], 1), o96126[2])
LOAD35058(java.lang.Object(ARRAY(i4[3], a115115data[3])), i5816[3], java.lang.Object(Tree(o96140[3], o96141[3]))) → LOAD35058ARR2(java.lang.Object(ARRAY(i4[3], a115115data[3])), i5816[3], java.lang.Object(Tree(o96140[3], o96141[3])), java.lang.Object(java.lang.String(i5968[3])))
LOAD35058ARR2(java.lang.Object(ARRAY(i4[4], a115115data[4])), i5816[4], java.lang.Object(Tree(o96140[4], java.lang.Object(Tree(o96140[4], o96141[4])))), java.lang.Object(java.lang.String(i5968[4]))) → COND_LOAD35058ARR2(&&(&&(&&(>(i5968[4], 42), >(i5816[4], 0)), <(i5816[4], i4[4])), >(+(i5816[4], 1), 0)), java.lang.Object(ARRAY(i4[4], a115115data[4])), i5816[4], java.lang.Object(Tree(o96140[4], java.lang.Object(Tree(o96140[4], o96141[4])))), java.lang.Object(java.lang.String(i5968[4])))
COND_LOAD35058ARR2(TRUE, java.lang.Object(ARRAY(i4[5], a115115data[5])), i5816[5], java.lang.Object(Tree(o96140[5], java.lang.Object(Tree(o96140[5], o96141[5])))), java.lang.Object(java.lang.String(i5968[5]))) → LOAD35058(java.lang.Object(ARRAY(i4[5], a115115data[5])), +(i5816[5], 1), o96140[5])

The following pairs are in P_≥:

LOAD35058(java.lang.Object(ARRAY(i4[3], a115115data[3])), i5816[3], java.lang.Object(Tree(o96140[3], o96141[3]))) → LOAD35058ARR2(java.lang.Object(ARRAY(i4[3], a115115data[3])), i5816[3], java.lang.Object(Tree(o96140[3], o96141[3])), java.lang.Object(java.lang.String(i5968[3])))

At least the following rules have been oriented under context sensitive arithmetic replacement:

TRUE¹ → &&(TRUE, TRUE)¹
FALSE¹ → &&(TRUE, FALSE)¹
FALSE¹ → &&(FALSE, TRUE)¹
FALSE¹ → &&(FALSE, FALSE)¹

(13) Complex Obligation (AND)

(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:
none

R is empty.

The integer pair graph contains the following rules and edges:
(3): LOAD35058(java.lang.Object(ARRAY(i4[3], a115115data[3])), i5816[3], java.lang.Object(Tree(o96140[3], o96141[3]))) → LOAD35058ARR2(java.lang.Object(ARRAY(i4[3], a115115data[3])), i5816[3], java.lang.Object(Tree(o96140[3], o96141[3])), java.lang.Object(java.lang.String(i5968[3])))

The set Q consists of the following terms:
Load35058(java.lang.Object(ARRAY(x0, x1)), x2, java.lang.Object(Tree(x3, x4)))
Load35058ARR1(java.lang.Object(ARRAY(x0, x1)), x2, java.lang.Object(Tree(java.lang.Object(Tree(x3, x4)), x4)), java.lang.Object(java.lang.String(x5)))
Cond_Load35058ARR1(TRUE, java.lang.Object(ARRAY(x0, x1)), x2, java.lang.Object(Tree(java.lang.Object(Tree(x3, x4)), x4)), java.lang.Object(java.lang.String(x5)))
Load35058ARR2(java.lang.Object(ARRAY(x0, x1)), x2, java.lang.Object(Tree(x3, java.lang.Object(Tree(x3, x4)))), java.lang.Object(java.lang.String(x5)))
Cond_Load35058ARR2(TRUE, java.lang.Object(ARRAY(x0, x1)), x2, java.lang.Object(Tree(x3, java.lang.Object(Tree(x3, x4)))), java.lang.Object(java.lang.String(x5)))

(15) IDependencyGraphProof (EQUIVALENT transformation)

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

(16) TRUE

(17) 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:
none

R is empty.

The integer pair graph is empty.

The set Q consists of the following terms:
Load35058(java.lang.Object(ARRAY(x0, x1)), x2, java.lang.Object(Tree(x3, x4)))
Load35058ARR1(java.lang.Object(ARRAY(x0, x1)), x2, java.lang.Object(Tree(java.lang.Object(Tree(x3, x4)), x4)), java.lang.Object(java.lang.String(x5)))
Cond_Load35058ARR1(TRUE, java.lang.Object(ARRAY(x0, x1)), x2, java.lang.Object(Tree(java.lang.Object(Tree(x3, x4)), x4)), java.lang.Object(java.lang.String(x5)))
Load35058ARR2(java.lang.Object(ARRAY(x0, x1)), x2, java.lang.Object(Tree(x3, java.lang.Object(Tree(x3, x4)))), java.lang.Object(java.lang.String(x5)))
Cond_Load35058ARR2(TRUE, java.lang.Object(ARRAY(x0, x1)), x2, java.lang.Object(Tree(x3, java.lang.Object(Tree(x3, x4)))), java.lang.Object(java.lang.String(x5)))

(18) IDependencyGraphProof (EQUIVALENT transformation)

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

(19) TRUE

(20) Obligation:

ITRS 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 TRS R consists of the following rules:
Load34990(java.lang.Object(ARRAY(i4, a115115data)), i5816, java.lang.Object(Tree), java.lang.Object(List(java.lang.Object(Tree), o92885)), i5824) → Load34990ARR3(java.lang.Object(ARRAY(i4, a115115data)), i5816, java.lang.Object(Tree), java.lang.Object(List(java.lang.Object(Tree), o92885)), i5824, java.lang.Object(java.lang.String(0)), java.lang.Object(java.lang.String(0)))
Load34990ARR3(java.lang.Object(ARRAY(i4, a115115data)), i5816, java.lang.Object(Tree), java.lang.Object(List(java.lang.Object(Tree), o92885)), i5824, java.lang.Object(java.lang.String(0)), java.lang.Object(java.lang.String(0))) → Cond_Load34990ARR3(i5816 + 1 > 0 && i5816 + 1 < i4 && i5816 > 0 && i5816 < i4 && i5824 > 0 && i5816 + 1 + 1 > 0, java.lang.Object(ARRAY(i4, a115115data)), i5816, java.lang.Object(Tree), java.lang.Object(List(java.lang.Object(Tree), o92885)), i5824, java.lang.Object(java.lang.String(0)), java.lang.Object(java.lang.String(0)))
Cond_Load34990ARR3(TRUE, java.lang.Object(ARRAY(i4, a115115data)), i5816, java.lang.Object(Tree), java.lang.Object(List(java.lang.Object(Tree), o92885)), i5824, java.lang.Object(java.lang.String(0)), java.lang.Object(java.lang.String(0))) → New39186(java.lang.Object(ARRAY(i4, a115115data)), i5816 + 1 + 1, java.lang.Object(Tree), o92885, i5824, NULL, NULL)
Inc35127(java.lang.Object(ARRAY(i4, a115115data)), i5816, o92510, o92885, i5824) → Load34990(java.lang.Object(ARRAY(i4, a115115data)), i5816, o92510, o92885, i5824 + -1)
Load34990(java.lang.Object(ARRAY(i4, a115115data)), i5816, o92510, java.lang.Object(List(NULL, o92885)), i5824) → Cond_Load34990(i5824 > 0, java.lang.Object(ARRAY(i4, a115115data)), i5816, o92510, java.lang.Object(List(NULL, o92885)), i5824)
Cond_Load34990(TRUE, java.lang.Object(ARRAY(i4, a115115data)), i5816, o92510, java.lang.Object(List(NULL, o92885)), i5824) → Load34990(java.lang.Object(ARRAY(i4, a115115data)), i5816, o92510, o92885, i5824 + -1)
New39186(java.lang.Object(ARRAY(i4, a115115data)), i6609, o92510, o92885, i5824, NULL, NULL) → Inc35127(java.lang.Object(ARRAY(i4, a115115data)), i6609, o92510, java.lang.Object(List(NULL, java.lang.Object(List(NULL, o92885)))), i5824)
Load34990(java.lang.Object(ARRAY(i4, a115115data)), i5816, o92510, java.lang.Object(List(java.lang.Object(Tree), o92885)), i5824) → Load34990ARR4(java.lang.Object(ARRAY(i4, a115115data)), i5816, o92510, java.lang.Object(List(java.lang.Object(Tree), o92885)), i5824, java.lang.Object(java.lang.String(0)), java.lang.Object(java.lang.String(0)))
Load34990ARR4(java.lang.Object(ARRAY(i4, a115115data)), i5816, o92510, java.lang.Object(List(java.lang.Object(Tree), o92885)), i5824, java.lang.Object(java.lang.String(0)), java.lang.Object(java.lang.String(0))) → Cond_Load34990ARR4(i5816 + 1 > 0 && i5816 + 1 < i4 && i5816 > 0 && i5816 < i4 && i5824 > 0 && i5816 + 1 + 1 > 0, java.lang.Object(ARRAY(i4, a115115data)), i5816, o92510, java.lang.Object(List(java.lang.Object(Tree), o92885)), i5824, java.lang.Object(java.lang.String(0)), java.lang.Object(java.lang.String(0)))
Cond_Load34990ARR4(TRUE, java.lang.Object(ARRAY(i4, a115115data)), i5816, o92510, java.lang.Object(List(java.lang.Object(Tree), o92885)), i5824, java.lang.Object(java.lang.String(0)), java.lang.Object(java.lang.String(0))) → Inc35127(java.lang.Object(ARRAY(i4, a115115data)), i5816 + 1 + 1, o92510new, java.lang.Object(List(NULL, java.lang.Object(List(NULL, o92885)))), i5824)
New40185(java.lang.Object(ARRAY(i4, a115115data)), i6609, o92510, o92885, i5824, NULL, java.lang.Object(Tree)) → Inc35127(java.lang.Object(ARRAY(i4, a115115data)), i6609, o92510, java.lang.Object(List(java.lang.Object(Tree), java.lang.Object(List(NULL, o92885)))), i5824)
Load34990(java.lang.Object(ARRAY(i4, a115115data)), i5816, o92510, java.lang.Object(List(java.lang.Object(Tree), o92885)), i5824) → Load34990ARR5(java.lang.Object(ARRAY(i4, a115115data)), i5816, o92510, java.lang.Object(List(java.lang.Object(Tree), o92885)), i5824, java.lang.Object(java.lang.String(i6986)), java.lang.Object(java.lang.String(0)))
Load34990ARR5(java.lang.Object(ARRAY(i4, a115115data)), i5816, o92510, java.lang.Object(List(java.lang.Object(Tree), o92885)), i5824, java.lang.Object(java.lang.String(i6986)), java.lang.Object(java.lang.String(0))) → Cond_Load34990ARR5(!(i6986 = 0) && i5816 + 1 > 0 && i5816 + 1 < i4 && i5816 > 0 && i5816 < i4 && i5824 > 0 && i5816 + 1 + 1 > 0, java.lang.Object(ARRAY(i4, a115115data)), i5816, o92510, java.lang.Object(List(java.lang.Object(Tree), o92885)), i5824, java.lang.Object(java.lang.String(i6986)), java.lang.Object(java.lang.String(0)))
Cond_Load34990ARR5(TRUE, java.lang.Object(ARRAY(i4, a115115data)), i5816, o92510, java.lang.Object(List(java.lang.Object(Tree), o92885)), i5824, java.lang.Object(java.lang.String(i6986)), java.lang.Object(java.lang.String(0))) → Inc35127(java.lang.Object(ARRAY(i4, a115115data)), i5816 + 1 + 1, o92510new, java.lang.Object(List(java.lang.Object(Tree), java.lang.Object(List(NULL, o92885)))), i5824)
New40288(java.lang.Object(ARRAY(i4, a115115data)), i6905, o92510, o92885, i5824, java.lang.Object(Tree), NULL) → Inc35127(java.lang.Object(ARRAY(i4, a115115data)), i6905, o92510, java.lang.Object(List(NULL, java.lang.Object(List(java.lang.Object(Tree), o92885)))), i5824)
Load34990(java.lang.Object(ARRAY(i4, a115115data)), i5816, o92510, java.lang.Object(List(java.lang.Object(Tree), o92885)), i5824) → Load34990ARR6(java.lang.Object(ARRAY(i4, a115115data)), i5816, o92510, java.lang.Object(List(java.lang.Object(Tree), o92885)), i5824, java.lang.Object(java.lang.String(0)), java.lang.Object(java.lang.String(i6164)))
Load34990ARR6(java.lang.Object(ARRAY(i4, a115115data)), i5816, o92510, java.lang.Object(List(java.lang.Object(Tree), o92885)), i5824, java.lang.Object(java.lang.String(0)), java.lang.Object(java.lang.String(i6164))) → Cond_Load34990ARR6(i5816 + 1 > 0 && i5816 + 1 < i4 && !(i6164 = 0) && i5816 > 0 && i5816 < i4 && i5824 > 0 && i5816 + 1 + 1 > 0, java.lang.Object(ARRAY(i4, a115115data)), i5816, o92510, java.lang.Object(List(java.lang.Object(Tree), o92885)), i5824, java.lang.Object(java.lang.String(0)), java.lang.Object(java.lang.String(i6164)))
Cond_Load34990ARR6(TRUE, java.lang.Object(ARRAY(i4, a115115data)), i5816, o92510, java.lang.Object(List(java.lang.Object(Tree), o92885)), i5824, java.lang.Object(java.lang.String(0)), java.lang.Object(java.lang.String(i6164))) → Inc35127(java.lang.Object(ARRAY(i4, a115115data)), i5816 + 1 + 1, o92510new, java.lang.Object(List(NULL, java.lang.Object(List(java.lang.Object(Tree), o92885)))), i5824)
New40846(java.lang.Object(ARRAY(i4, a115115data)), i6905, o92510, o92885, i5824, java.lang.Object(Tree), java.lang.Object(Tree)) → Inc35127(java.lang.Object(ARRAY(i4, a115115data)), i6905, o92510, java.lang.Object(List(java.lang.Object(Tree), java.lang.Object(List(java.lang.Object(Tree), o92885)))), i5824)
Load34990(java.lang.Object(ARRAY(i4, a115115data)), i5816, o92510, java.lang.Object(List(java.lang.Object(Tree), o92885)), i5824) → Load34990ARR7(java.lang.Object(ARRAY(i4, a115115data)), i5816, o92510, java.lang.Object(List(java.lang.Object(Tree), o92885)), i5824, java.lang.Object(java.lang.String(i7504)), java.lang.Object(java.lang.String(i6164)))
Load34990ARR7(java.lang.Object(ARRAY(i4, a115115data)), i5816, o92510, java.lang.Object(List(java.lang.Object(Tree), o92885)), i5824, java.lang.Object(java.lang.String(i7504)), java.lang.Object(java.lang.String(i6164))) → Cond_Load34990ARR7(!(i7504 = 0) && i5816 + 1 > 0 && i5816 + 1 < i4 && !(i6164 = 0) && i5816 > 0 && i5816 < i4 && i5824 > 0 && i5816 + 1 + 1 > 0, java.lang.Object(ARRAY(i4, a115115data)), i5816, o92510, java.lang.Object(List(java.lang.Object(Tree), o92885)), i5824, java.lang.Object(java.lang.String(i7504)), java.lang.Object(java.lang.String(i6164)))
Cond_Load34990ARR7(TRUE, java.lang.Object(ARRAY(i4, a115115data)), i5816, o92510, java.lang.Object(List(java.lang.Object(Tree), o92885)), i5824, java.lang.Object(java.lang.String(i7504)), java.lang.Object(java.lang.String(i6164))) → Inc35127(java.lang.Object(ARRAY(i4, a115115data)), i5816 + 1 + 1, o92510new, java.lang.Object(List(java.lang.Object(Tree), java.lang.Object(List(java.lang.Object(Tree), o92885)))), i5824)
Load34990(java.lang.Object(ARRAY(i4, a115115data)), i5816, java.lang.Object(Tree), java.lang.Object(List(java.lang.Object(Tree), o92885)), i5824) → Load34990ARR8(java.lang.Object(ARRAY(i4, a115115data)), i5816, java.lang.Object(Tree), java.lang.Object(List(java.lang.Object(Tree), o92885)), i5824, java.lang.Object(java.lang.String(i6986)), java.lang.Object(java.lang.String(0)))
Load34990ARR8(java.lang.Object(ARRAY(i4, a115115data)), i5816, java.lang.Object(Tree), java.lang.Object(List(java.lang.Object(Tree), o92885)), i5824, java.lang.Object(java.lang.String(i6986)), java.lang.Object(java.lang.String(0))) → Cond_Load34990ARR8(!(i6986 = 0) && i5816 + 1 > 0 && i5816 + 1 < i4 && i5816 > 0 && i5816 < i4 && i5824 > 0 && i5816 + 1 + 1 > 0, java.lang.Object(ARRAY(i4, a115115data)), i5816, java.lang.Object(Tree), java.lang.Object(List(java.lang.Object(Tree), o92885)), i5824, java.lang.Object(java.lang.String(i6986)), java.lang.Object(java.lang.String(0)))
Cond_Load34990ARR8(TRUE, java.lang.Object(ARRAY(i4, a115115data)), i5816, java.lang.Object(Tree), java.lang.Object(List(java.lang.Object(Tree), o92885)), i5824, java.lang.Object(java.lang.String(i6986)), java.lang.Object(java.lang.String(0))) → New40185(java.lang.Object(ARRAY(i4, a115115data)), i5816 + 1 + 1, java.lang.Object(Tree), o92885, i5824, NULL, java.lang.Object(Tree))
Load34990(java.lang.Object(ARRAY(i4, a115115data)), i5816, java.lang.Object(Tree), java.lang.Object(List(java.lang.Object(Tree), o92885)), i5824) → Load34990ARR9(java.lang.Object(ARRAY(i4, a115115data)), i5816, java.lang.Object(Tree), java.lang.Object(List(java.lang.Object(Tree), o92885)), i5824, java.lang.Object(java.lang.String(0)), java.lang.Object(java.lang.String(i6164)))
Load34990ARR9(java.lang.Object(ARRAY(i4, a115115data)), i5816, java.lang.Object(Tree), java.lang.Object(List(java.lang.Object(Tree), o92885)), i5824, java.lang.Object(java.lang.String(0)), java.lang.Object(java.lang.String(i6164))) → Cond_Load34990ARR9(i5816 + 1 > 0 && i5816 + 1 < i4 && !(i6164 = 0) && i5816 > 0 && i5816 < i4 && i5824 > 0 && i5816 + 1 + 1 > 0, java.lang.Object(ARRAY(i4, a115115data)), i5816, java.lang.Object(Tree), java.lang.Object(List(java.lang.Object(Tree), o92885)), i5824, java.lang.Object(java.lang.String(0)), java.lang.Object(java.lang.String(i6164)))
Cond_Load34990ARR9(TRUE, java.lang.Object(ARRAY(i4, a115115data)), i5816, java.lang.Object(Tree), java.lang.Object(List(java.lang.Object(Tree), o92885)), i5824, java.lang.Object(java.lang.String(0)), java.lang.Object(java.lang.String(i6164))) → New40288(java.lang.Object(ARRAY(i4, a115115data)), i5816 + 1 + 1, java.lang.Object(Tree), o92885, i5824, java.lang.Object(Tree), NULL)
Load34990(java.lang.Object(ARRAY(i4, a115115data)), i5816, java.lang.Object(Tree), java.lang.Object(List(java.lang.Object(Tree), o92885)), i5824) → Load34990ARR10(java.lang.Object(ARRAY(i4, a115115data)), i5816, java.lang.Object(Tree), java.lang.Object(List(java.lang.Object(Tree), o92885)), i5824, java.lang.Object(java.lang.String(i7504)), java.lang.Object(java.lang.String(i6164)))
Load34990ARR10(java.lang.Object(ARRAY(i4, a115115data)), i5816, java.lang.Object(Tree), java.lang.Object(List(java.lang.Object(Tree), o92885)), i5824, java.lang.Object(java.lang.String(i7504)), java.lang.Object(java.lang.String(i6164))) → Cond_Load34990ARR10(!(i7504 = 0) && i5816 + 1 > 0 && i5816 + 1 < i4 && !(i6164 = 0) && i5816 > 0 && i5816 < i4 && i5824 > 0 && i5816 + 1 + 1 > 0, java.lang.Object(ARRAY(i4, a115115data)), i5816, java.lang.Object(Tree), java.lang.Object(List(java.lang.Object(Tree), o92885)), i5824, java.lang.Object(java.lang.String(i7504)), java.lang.Object(java.lang.String(i6164)))
Cond_Load34990ARR10(TRUE, java.lang.Object(ARRAY(i4, a115115data)), i5816, java.lang.Object(Tree), java.lang.Object(List(java.lang.Object(Tree), o92885)), i5824, java.lang.Object(java.lang.String(i7504)), java.lang.Object(java.lang.String(i6164))) → New40846(java.lang.Object(ARRAY(i4, a115115data)), i5816 + 1 + 1, java.lang.Object(Tree), o92885, i5824, java.lang.Object(Tree), java.lang.Object(Tree))
The set Q consists of the following terms:
Load34990ARR3(java.lang.Object(ARRAY(x0, x1)), x2, java.lang.Object(Tree), java.lang.Object(List(java.lang.Object(Tree), x3)), x4, java.lang.Object(java.lang.String(0)), java.lang.Object(java.lang.String(0)))
Cond_Load34990ARR3(TRUE, java.lang.Object(ARRAY(x0, x1)), x2, java.lang.Object(Tree), java.lang.Object(List(java.lang.Object(Tree), x3)), x4, java.lang.Object(java.lang.String(0)), java.lang.Object(java.lang.String(0)))
Inc35127(java.lang.Object(ARRAY(x0, x1)), x2, x3, x4, x5)
Load34990(java.lang.Object(ARRAY(x0, x1)), x2, x3, java.lang.Object(List(NULL, x4)), x5)
Cond_Load34990(TRUE, java.lang.Object(ARRAY(x0, x1)), x2, x3, java.lang.Object(List(NULL, x4)), x5)
New39186(java.lang.Object(ARRAY(x0, x1)), x2, x3, x4, x5, NULL, NULL)
Load34990(java.lang.Object(ARRAY(x0, x1)), x2, x3, java.lang.Object(List(java.lang.Object(Tree), x4)), x5)
Load34990ARR4(java.lang.Object(ARRAY(x0, x1)), x2, x3, java.lang.Object(List(java.lang.Object(Tree), x4)), x5, java.lang.Object(java.lang.String(0)), java.lang.Object(java.lang.String(0)))
Cond_Load34990ARR4(TRUE, java.lang.Object(ARRAY(x0, x1)), x2, x3, java.lang.Object(List(java.lang.Object(Tree), x4)), x5, java.lang.Object(java.lang.String(0)), java.lang.Object(java.lang.String(0)))
New40185(java.lang.Object(ARRAY(x0, x1)), x2, x3, x4, x5, NULL, java.lang.Object(Tree))
Load34990ARR5(java.lang.Object(ARRAY(x0, x1)), x2, x3, java.lang.Object(List(java.lang.Object(Tree), x4)), x5, java.lang.Object(java.lang.String(x6)), java.lang.Object(java.lang.String(0)))
Cond_Load34990ARR5(TRUE, java.lang.Object(ARRAY(x0, x1)), x2, x3, java.lang.Object(List(java.lang.Object(Tree), x4)), x5, java.lang.Object(java.lang.String(x6)), java.lang.Object(java.lang.String(0)))
New40288(java.lang.Object(ARRAY(x0, x1)), x2, x3, x4, x5, java.lang.Object(Tree), NULL)
Load34990ARR6(java.lang.Object(ARRAY(x0, x1)), x2, x3, java.lang.Object(List(java.lang.Object(Tree), x4)), x5, java.lang.Object(java.lang.String(0)), java.lang.Object(java.lang.String(x6)))
Cond_Load34990ARR6(TRUE, java.lang.Object(ARRAY(x0, x1)), x2, x3, java.lang.Object(List(java.lang.Object(Tree), x4)), x5, java.lang.Object(java.lang.String(0)), java.lang.Object(java.lang.String(x6)))
New40846(java.lang.Object(ARRAY(x0, x1)), x2, x3, x4, x5, java.lang.Object(Tree), java.lang.Object(Tree))
Load34990ARR7(java.lang.Object(ARRAY(x0, x1)), x2, x3, java.lang.Object(List(java.lang.Object(Tree), x4)), x5, java.lang.Object(java.lang.String(x6)), java.lang.Object(java.lang.String(x7)))
Cond_Load34990ARR7(TRUE, java.lang.Object(ARRAY(x0, x1)), x2, x3, java.lang.Object(List(java.lang.Object(Tree), x4)), x5, java.lang.Object(java.lang.String(x6)), java.lang.Object(java.lang.String(x7)))
Load34990ARR8(java.lang.Object(ARRAY(x0, x1)), x2, java.lang.Object(Tree), java.lang.Object(List(java.lang.Object(Tree), x3)), x4, java.lang.Object(java.lang.String(x5)), java.lang.Object(java.lang.String(0)))
Cond_Load34990ARR8(TRUE, java.lang.Object(ARRAY(x0, x1)), x2, java.lang.Object(Tree), java.lang.Object(List(java.lang.Object(Tree), x3)), x4, java.lang.Object(java.lang.String(x5)), java.lang.Object(java.lang.String(0)))
Load34990ARR9(java.lang.Object(ARRAY(x0, x1)), x2, java.lang.Object(Tree), java.lang.Object(List(java.lang.Object(Tree), x3)), x4, java.lang.Object(java.lang.String(0)), java.lang.Object(java.lang.String(x5)))
Cond_Load34990ARR9(TRUE, java.lang.Object(ARRAY(x0, x1)), x2, java.lang.Object(Tree), java.lang.Object(List(java.lang.Object(Tree), x3)), x4, java.lang.Object(java.lang.String(0)), java.lang.Object(java.lang.String(x5)))
Load34990ARR10(java.lang.Object(ARRAY(x0, x1)), x2, java.lang.Object(Tree), java.lang.Object(List(java.lang.Object(Tree), x3)), x4, java.lang.Object(java.lang.String(x5)), java.lang.Object(java.lang.String(x6)))
Cond_Load34990ARR10(TRUE, java.lang.Object(ARRAY(x0, x1)), x2, java.lang.Object(Tree), java.lang.Object(List(java.lang.Object(Tree), x3)), x4, java.lang.Object(java.lang.String(x5)), java.lang.Object(java.lang.String(x6)))

(21) GroundTermsRemoverProof (EQUIVALENT transformation)

Some arguments are removed because they always contain the same ground term.
We removed the following ground terms:

java.lang.Object(Tree)
NULL
java.lang.Object(java.lang.String(0))

We removed arguments according to the following replacements:

New40846(x1, x2, x3, x4, x5, x6, x7) → New40846(x1, x2, x3, x4, x5)
Cond_Load34990ARR10(x1, x2, x3, x4, x5, x6, x7, x8) → Cond_Load34990ARR10(x1, x2, x3, x5, x6, x7, x8)
Load34990ARR10(x1, x2, x3, x4, x5, x6, x7) → Load34990ARR10(x1, x2, x4, x5, x6, x7)
New40288(x1, x2, x3, x4, x5, x6, x7) → New40288(x1, x2, x3, x4, x5)
Cond_Load34990ARR9(x1, x2, x3, x4, x5, x6, x7, x8) → Cond_Load34990ARR9(x1, x2, x3, x5, x6, x8)
Load34990ARR9(x1, x2, x3, x4, x5, x6, x7) → Load34990ARR9(x1, x2, x4, x5, x7)
New40185(x1, x2, x3, x4, x5, x6, x7) → New40185(x1, x2, x3, x4, x5)
Cond_Load34990ARR8(x1, x2, x3, x4, x5, x6, x7, x8) → Cond_Load34990ARR8(x1, x2, x3, x5, x6, x7)
Load34990ARR8(x1, x2, x3, x4, x5, x6, x7) → Load34990ARR8(x1, x2, x4, x5, x6)
Cond_Load34990ARR6(x1, x2, x3, x4, x5, x6, x7, x8) → Cond_Load34990ARR6(x1, x2, x3, x4, x5, x6, x8)
Load34990ARR6(x1, x2, x3, x4, x5, x6, x7) → Load34990ARR6(x1, x2, x3, x4, x5, x7)
Cond_Load34990ARR5(x1, x2, x3, x4, x5, x6, x7, x8) → Cond_Load34990ARR5(x1, x2, x3, x4, x5, x6, x7)
Load34990ARR5(x1, x2, x3, x4, x5, x6, x7) → Load34990ARR5(x1, x2, x3, x4, x5, x6)
Cond_Load34990ARR4(x1, x2, x3, x4, x5, x6, x7, x8) → Cond_Load34990ARR4(x1, x2, x3, x4, x5, x6)
Load34990ARR4(x1, x2, x3, x4, x5, x6, x7) → Load34990ARR4(x1, x2, x3, x4, x5)
New39186(x1, x2, x3, x4, x5, x6, x7) → New39186(x1, x2, x3, x4, x5)
Cond_Load34990ARR3(x1, x2, x3, x4, x5, x6, x7, x8) → Cond_Load34990ARR3(x1, x2, x3, x5, x6)
Load34990ARR3(x1, x2, x3, x4, x5, x6, x7) → Load34990ARR3(x1, x2, x4, x5)

(22) Obligation:

ITRS 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 TRS R consists of the following rules:
Load34990(java.lang.Object(ARRAY(i4, a115115data)), i5816, java.lang.Object(Tree), java.lang.Object(List(java.lang.Object(Tree), o92885)), i5824) → Load34990ARR3(java.lang.Object(ARRAY(i4, a115115data)), i5816, java.lang.Object(List(java.lang.Object(Tree), o92885)), i5824)
Load34990ARR3(java.lang.Object(ARRAY(i4, a115115data)), i5816, java.lang.Object(List(java.lang.Object(Tree), o92885)), i5824) → Cond_Load34990ARR3(i5816 + 1 > 0 && i5816 + 1 < i4 && i5816 > 0 && i5816 < i4 && i5824 > 0 && i5816 + 1 + 1 > 0, java.lang.Object(ARRAY(i4, a115115data)), i5816, java.lang.Object(List(java.lang.Object(Tree), o92885)), i5824)
Cond_Load34990ARR3(TRUE, java.lang.Object(ARRAY(i4, a115115data)), i5816, java.lang.Object(List(java.lang.Object(Tree), o92885)), i5824) → New39186(java.lang.Object(ARRAY(i4, a115115data)), i5816 + 1 + 1, java.lang.Object(Tree), o92885, i5824)
Inc35127(java.lang.Object(ARRAY(i4, a115115data)), i5816, o92510, o92885, i5824) → Load34990(java.lang.Object(ARRAY(i4, a115115data)), i5816, o92510, o92885, i5824 + -1)
Load34990(java.lang.Object(ARRAY(i4, a115115data)), i5816, o92510, java.lang.Object(List(NULL, o92885)), i5824) → Cond_Load34990(i5824 > 0, java.lang.Object(ARRAY(i4, a115115data)), i5816, o92510, java.lang.Object(List(NULL, o92885)), i5824)
Cond_Load34990(TRUE, java.lang.Object(ARRAY(i4, a115115data)), i5816, o92510, java.lang.Object(List(NULL, o92885)), i5824) → Load34990(java.lang.Object(ARRAY(i4, a115115data)), i5816, o92510, o92885, i5824 + -1)
New39186(java.lang.Object(ARRAY(i4, a115115data)), i6609, o92510, o92885, i5824) → Inc35127(java.lang.Object(ARRAY(i4, a115115data)), i6609, o92510, java.lang.Object(List(NULL, java.lang.Object(List(NULL, o92885)))), i5824)
Load34990(java.lang.Object(ARRAY(i4, a115115data)), i5816, o92510, java.lang.Object(List(java.lang.Object(Tree), o92885)), i5824) → Load34990ARR4(java.lang.Object(ARRAY(i4, a115115data)), i5816, o92510, java.lang.Object(List(java.lang.Object(Tree), o92885)), i5824)
Load34990ARR4(java.lang.Object(ARRAY(i4, a115115data)), i5816, o92510, java.lang.Object(List(java.lang.Object(Tree), o92885)), i5824) → Cond_Load34990ARR4(i5816 + 1 > 0 && i5816 + 1 < i4 && i5816 > 0 && i5816 < i4 && i5824 > 0 && i5816 + 1 + 1 > 0, java.lang.Object(ARRAY(i4, a115115data)), i5816, o92510, java.lang.Object(List(java.lang.Object(Tree), o92885)), i5824)
Cond_Load34990ARR4(TRUE, java.lang.Object(ARRAY(i4, a115115data)), i5816, o92510, java.lang.Object(List(java.lang.Object(Tree), o92885)), i5824) → Inc35127(java.lang.Object(ARRAY(i4, a115115data)), i5816 + 1 + 1, o92510new, java.lang.Object(List(NULL, java.lang.Object(List(NULL, o92885)))), i5824)
New40185(java.lang.Object(ARRAY(i4, a115115data)), i6609, o92510, o92885, i5824) → Inc35127(java.lang.Object(ARRAY(i4, a115115data)), i6609, o92510, java.lang.Object(List(java.lang.Object(Tree), java.lang.Object(List(NULL, o92885)))), i5824)
Load34990(java.lang.Object(ARRAY(i4, a115115data)), i5816, o92510, java.lang.Object(List(java.lang.Object(Tree), o92885)), i5824) → Load34990ARR5(java.lang.Object(ARRAY(i4, a115115data)), i5816, o92510, java.lang.Object(List(java.lang.Object(Tree), o92885)), i5824, java.lang.Object(java.lang.String(i6986)))
Load34990ARR5(java.lang.Object(ARRAY(i4, a115115data)), i5816, o92510, java.lang.Object(List(java.lang.Object(Tree), o92885)), i5824, java.lang.Object(java.lang.String(i6986))) → Cond_Load34990ARR5(!(i6986 = 0) && i5816 + 1 > 0 && i5816 + 1 < i4 && i5816 > 0 && i5816 < i4 && i5824 > 0 && i5816 + 1 + 1 > 0, java.lang.Object(ARRAY(i4, a115115data)), i5816, o92510, java.lang.Object(List(java.lang.Object(Tree), o92885)), i5824, java.lang.Object(java.lang.String(i6986)))
Cond_Load34990ARR5(TRUE, java.lang.Object(ARRAY(i4, a115115data)), i5816, o92510, java.lang.Object(List(java.lang.Object(Tree), o92885)), i5824, java.lang.Object(java.lang.String(i6986))) → Inc35127(java.lang.Object(ARRAY(i4, a115115data)), i5816 + 1 + 1, o92510new, java.lang.Object(List(java.lang.Object(Tree), java.lang.Object(List(NULL, o92885)))), i5824)
New40288(java.lang.Object(ARRAY(i4, a115115data)), i6905, o92510, o92885, i5824) → Inc35127(java.lang.Object(ARRAY(i4, a115115data)), i6905, o92510, java.lang.Object(List(NULL, java.lang.Object(List(java.lang.Object(Tree), o92885)))), i5824)
Load34990(java.lang.Object(ARRAY(i4, a115115data)), i5816, o92510, java.lang.Object(List(java.lang.Object(Tree), o92885)), i5824) → Load34990ARR6(java.lang.Object(ARRAY(i4, a115115data)), i5816, o92510, java.lang.Object(List(java.lang.Object(Tree), o92885)), i5824, java.lang.Object(java.lang.String(i6164)))
Load34990ARR6(java.lang.Object(ARRAY(i4, a115115data)), i5816, o92510, java.lang.Object(List(java.lang.Object(Tree), o92885)), i5824, java.lang.Object(java.lang.String(i6164))) → Cond_Load34990ARR6(i5816 + 1 > 0 && i5816 + 1 < i4 && !(i6164 = 0) && i5816 > 0 && i5816 < i4 && i5824 > 0 && i5816 + 1 + 1 > 0, java.lang.Object(ARRAY(i4, a115115data)), i5816, o92510, java.lang.Object(List(java.lang.Object(Tree), o92885)), i5824, java.lang.Object(java.lang.String(i6164)))
Cond_Load34990ARR6(TRUE, java.lang.Object(ARRAY(i4, a115115data)), i5816, o92510, java.lang.Object(List(java.lang.Object(Tree), o92885)), i5824, java.lang.Object(java.lang.String(i6164))) → Inc35127(java.lang.Object(ARRAY(i4, a115115data)), i5816 + 1 + 1, o92510new, java.lang.Object(List(NULL, java.lang.Object(List(java.lang.Object(Tree), o92885)))), i5824)
New40846(java.lang.Object(ARRAY(i4, a115115data)), i6905, o92510, o92885, i5824) → Inc35127(java.lang.Object(ARRAY(i4, a115115data)), i6905, o92510, java.lang.Object(List(java.lang.Object(Tree), java.lang.Object(List(java.lang.Object(Tree), o92885)))), i5824)
Load34990(java.lang.Object(ARRAY(i4, a115115data)), i5816, o92510, java.lang.Object(List(java.lang.Object(Tree), o92885)), i5824) → Load34990ARR7(java.lang.Object(ARRAY(i4, a115115data)), i5816, o92510, java.lang.Object(List(java.lang.Object(Tree), o92885)), i5824, java.lang.Object(java.lang.String(i7504)), java.lang.Object(java.lang.String(i6164)))
Load34990ARR7(java.lang.Object(ARRAY(i4, a115115data)), i5816, o92510, java.lang.Object(List(java.lang.Object(Tree), o92885)), i5824, java.lang.Object(java.lang.String(i7504)), java.lang.Object(java.lang.String(i6164))) → Cond_Load34990ARR7(!(i7504 = 0) && i5816 + 1 > 0 && i5816 + 1 < i4 && !(i6164 = 0) && i5816 > 0 && i5816 < i4 && i5824 > 0 && i5816 + 1 + 1 > 0, java.lang.Object(ARRAY(i4, a115115data)), i5816, o92510, java.lang.Object(List(java.lang.Object(Tree), o92885)), i5824, java.lang.Object(java.lang.String(i7504)), java.lang.Object(java.lang.String(i6164)))
Cond_Load34990ARR7(TRUE, java.lang.Object(ARRAY(i4, a115115data)), i5816, o92510, java.lang.Object(List(java.lang.Object(Tree), o92885)), i5824, java.lang.Object(java.lang.String(i7504)), java.lang.Object(java.lang.String(i6164))) → Inc35127(java.lang.Object(ARRAY(i4, a115115data)), i5816 + 1 + 1, o92510new, java.lang.Object(List(java.lang.Object(Tree), java.lang.Object(List(java.lang.Object(Tree), o92885)))), i5824)
Load34990(java.lang.Object(ARRAY(i4, a115115data)), i5816, java.lang.Object(Tree), java.lang.Object(List(java.lang.Object(Tree), o92885)), i5824) → Load34990ARR8(java.lang.Object(ARRAY(i4, a115115data)), i5816, java.lang.Object(List(java.lang.Object(Tree), o92885)), i5824, java.lang.Object(java.lang.String(i6986)))
Load34990ARR8(java.lang.Object(ARRAY(i4, a115115data)), i5816, java.lang.Object(List(java.lang.Object(Tree), o92885)), i5824, java.lang.Object(java.lang.String(i6986))) → Cond_Load34990ARR8(!(i6986 = 0) && i5816 + 1 > 0 && i5816 + 1 < i4 && i5816 > 0 && i5816 < i4 && i5824 > 0 && i5816 + 1 + 1 > 0, java.lang.Object(ARRAY(i4, a115115data)), i5816, java.lang.Object(List(java.lang.Object(Tree), o92885)), i5824, java.lang.Object(java.lang.String(i6986)))
Cond_Load34990ARR8(TRUE, java.lang.Object(ARRAY(i4, a115115data)), i5816, java.lang.Object(List(java.lang.Object(Tree), o92885)), i5824, java.lang.Object(java.lang.String(i6986))) → New40185(java.lang.Object(ARRAY(i4, a115115data)), i5816 + 1 + 1, java.lang.Object(Tree), o92885, i5824)
Load34990(java.lang.Object(ARRAY(i4, a115115data)), i5816, java.lang.Object(Tree), java.lang.Object(List(java.lang.Object(Tree), o92885)), i5824) → Load34990ARR9(java.lang.Object(ARRAY(i4, a115115data)), i5816, java.lang.Object(List(java.lang.Object(Tree), o92885)), i5824, java.lang.Object(java.lang.String(i6164)))
Load34990ARR9(java.lang.Object(ARRAY(i4, a115115data)), i5816, java.lang.Object(List(java.lang.Object(Tree), o92885)), i5824, java.lang.Object(java.lang.String(i6164))) → Cond_Load34990ARR9(i5816 + 1 > 0 && i5816 + 1 < i4 && !(i6164 = 0) && i5816 > 0 && i5816 < i4 && i5824 > 0 && i5816 + 1 + 1 > 0, java.lang.Object(ARRAY(i4, a115115data)), i5816, java.lang.Object(List(java.lang.Object(Tree), o92885)), i5824, java.lang.Object(java.lang.String(i6164)))
Cond_Load34990ARR9(TRUE, java.lang.Object(ARRAY(i4, a115115data)), i5816, java.lang.Object(List(java.lang.Object(Tree), o92885)), i5824, java.lang.Object(java.lang.String(i6164))) → New40288(java.lang.Object(ARRAY(i4, a115115data)), i5816 + 1 + 1, java.lang.Object(Tree), o92885, i5824)
Load34990(java.lang.Object(ARRAY(i4, a115115data)), i5816, java.lang.Object(Tree), java.lang.Object(List(java.lang.Object(Tree), o92885)), i5824) → Load34990ARR10(java.lang.Object(ARRAY(i4, a115115data)), i5816, java.lang.Object(List(java.lang.Object(Tree), o92885)), i5824, java.lang.Object(java.lang.String(i7504)), java.lang.Object(java.lang.String(i6164)))
Load34990ARR10(java.lang.Object(ARRAY(i4, a115115data)), i5816, java.lang.Object(List(java.lang.Object(Tree), o92885)), i5824, java.lang.Object(java.lang.String(i7504)), java.lang.Object(java.lang.String(i6164))) → Cond_Load34990ARR10(!(i7504 = 0) && i5816 + 1 > 0 && i5816 + 1 < i4 && !(i6164 = 0) && i5816 > 0 && i5816 < i4 && i5824 > 0 && i5816 + 1 + 1 > 0, java.lang.Object(ARRAY(i4, a115115data)), i5816, java.lang.Object(List(java.lang.Object(Tree), o92885)), i5824, java.lang.Object(java.lang.String(i7504)), java.lang.Object(java.lang.String(i6164)))
Cond_Load34990ARR10(TRUE, java.lang.Object(ARRAY(i4, a115115data)), i5816, java.lang.Object(List(java.lang.Object(Tree), o92885)), i5824, java.lang.Object(java.lang.String(i7504)), java.lang.Object(java.lang.String(i6164))) → New40846(java.lang.Object(ARRAY(i4, a115115data)), i5816 + 1 + 1, java.lang.Object(Tree), o92885, i5824)
The set Q consists of the following terms:
Load34990ARR3(java.lang.Object(ARRAY(x0, x1)), x2, java.lang.Object(List(java.lang.Object(Tree), x3)), x4)
Cond_Load34990ARR3(TRUE, java.lang.Object(ARRAY(x0, x1)), x2, java.lang.Object(List(java.lang.Object(Tree), x3)), x4)
Inc35127(java.lang.Object(ARRAY(x0, x1)), x2, x3, x4, x5)
Load34990(java.lang.Object(ARRAY(x0, x1)), x2, x3, java.lang.Object(List(NULL, x4)), x5)
Cond_Load34990(TRUE, java.lang.Object(ARRAY(x0, x1)), x2, x3, java.lang.Object(List(NULL, x4)), x5)
New39186(java.lang.Object(ARRAY(x0, x1)), x2, x3, x4, x5)
Load34990(java.lang.Object(ARRAY(x0, x1)), x2, x3, java.lang.Object(List(java.lang.Object(Tree), x4)), x5)
Load34990ARR4(java.lang.Object(ARRAY(x0, x1)), x2, x3, java.lang.Object(List(java.lang.Object(Tree), x4)), x5)
Cond_Load34990ARR4(TRUE, java.lang.Object(ARRAY(x0, x1)), x2, x3, java.lang.Object(List(java.lang.Object(Tree), x4)), x5)
New40185(java.lang.Object(ARRAY(x0, x1)), x2, x3, x4, x5)
Load34990ARR5(java.lang.Object(ARRAY(x0, x1)), x2, x3, java.lang.Object(List(java.lang.Object(Tree), x4)), x5, java.lang.Object(java.lang.String(x6)))
Cond_Load34990ARR5(TRUE, java.lang.Object(ARRAY(x0, x1)), x2, x3, java.lang.Object(List(java.lang.Object(Tree), x4)), x5, java.lang.Object(java.lang.String(x6)))
New40288(java.lang.Object(ARRAY(x0, x1)), x2, x3, x4, x5)
Load34990ARR6(java.lang.Object(ARRAY(x0, x1)), x2, x3, java.lang.Object(List(java.lang.Object(Tree), x4)), x5, java.lang.Object(java.lang.String(x6)))
Cond_Load34990ARR6(TRUE, java.lang.Object(ARRAY(x0, x1)), x2, x3, java.lang.Object(List(java.lang.Object(Tree), x4)), x5, java.lang.Object(java.lang.String(x6)))
New40846(java.lang.Object(ARRAY(x0, x1)), x2, x3, x4, x5)
Load34990ARR7(java.lang.Object(ARRAY(x0, x1)), x2, x3, java.lang.Object(List(java.lang.Object(Tree), x4)), x5, java.lang.Object(java.lang.String(x6)), java.lang.Object(java.lang.String(x7)))
Cond_Load34990ARR7(TRUE, java.lang.Object(ARRAY(x0, x1)), x2, x3, java.lang.Object(List(java.lang.Object(Tree), x4)), x5, java.lang.Object(java.lang.String(x6)), java.lang.Object(java.lang.String(x7)))
Load34990ARR8(java.lang.Object(ARRAY(x0, x1)), x2, java.lang.Object(List(java.lang.Object(Tree), x3)), x4, java.lang.Object(java.lang.String(x5)))
Cond_Load34990ARR8(TRUE, java.lang.Object(ARRAY(x0, x1)), x2, java.lang.Object(List(java.lang.Object(Tree), x3)), x4, java.lang.Object(java.lang.String(x5)))
Load34990ARR9(java.lang.Object(ARRAY(x0, x1)), x2, java.lang.Object(List(java.lang.Object(Tree), x3)), x4, java.lang.Object(java.lang.String(x5)))
Cond_Load34990ARR9(TRUE, java.lang.Object(ARRAY(x0, x1)), x2, java.lang.Object(List(java.lang.Object(Tree), x3)), x4, java.lang.Object(java.lang.String(x5)))
Load34990ARR10(java.lang.Object(ARRAY(x0, x1)), x2, java.lang.Object(List(java.lang.Object(Tree), x3)), x4, java.lang.Object(java.lang.String(x5)), java.lang.Object(java.lang.String(x6)))
Cond_Load34990ARR10(TRUE, java.lang.Object(ARRAY(x0, x1)), x2, java.lang.Object(List(java.lang.Object(Tree), x3)), x4, java.lang.Object(java.lang.String(x5)), java.lang.Object(java.lang.String(x6)))

(23) ITRSFilterProcessorProof (SOUND transformation)

We filter according the heuristic IdpCand1ShapeHeuristic
We removed arguments according to the following replacements:

Load34990(x1, x2, x3, x4, x5) → Load34990(x1, x2, x5)
List(x1, x2) → List
Load34990ARR3(x1, x2, x3, x4) → Load34990ARR3(x1, x2, x4)
Cond_Load34990ARR3(x1, x2, x3, x4, x5) → Cond_Load34990ARR3(x1, x2, x3, x5)
New39186(x1, x2, x3, x4, x5) → New39186(x1, x2, x5)
Inc35127(x1, x2, x3, x4, x5) → Inc35127(x1, x2, x5)
Cond_Load34990(x1, x2, x3, x4, x5, x6) → Cond_Load34990(x1, x2, x3, x6)
Load34990ARR4(x1, x2, x3, x4, x5) → Load34990ARR4(x1, x2, x5)
Cond_Load34990ARR4(x1, x2, x3, x4, x5, x6) → Cond_Load34990ARR4(x1, x2, x3, x6)
New40185(x1, x2, x3, x4, x5) → New40185(x1, x2, x5)
Load34990ARR5(x1, x2, x3, x4, x5, x6) → Load34990ARR5(x1, x2, x5, x6)
Cond_Load34990ARR5(x1, x2, x3, x4, x5, x6, x7) → Cond_Load34990ARR5(x1, x2, x3, x6, x7)
New40288(x1, x2, x3, x4, x5) → New40288(x1, x2, x5)
Load34990ARR6(x1, x2, x3, x4, x5, x6) → Load34990ARR6(x1, x2, x5, x6)
Cond_Load34990ARR6(x1, x2, x3, x4, x5, x6, x7) → Cond_Load34990ARR6(x1, x2, x3, x6, x7)
New40846(x1, x2, x3, x4, x5) → New40846(x1, x2, x5)
Load34990ARR7(x1, x2, x3, x4, x5, x6, x7) → Load34990ARR7(x1, x2, x5, x6, x7)
Cond_Load34990ARR7(x1, x2, x3, x4, x5, x6, x7, x8) → Cond_Load34990ARR7(x1, x2, x3, x6, x7, x8)
Load34990ARR8(x1, x2, x3, x4, x5) → Load34990ARR8(x1, x2, x4, x5)
Cond_Load34990ARR8(x1, x2, x3, x4, x5, x6) → Cond_Load34990ARR8(x1, x2, x3, x5, x6)
Load34990ARR9(x1, x2, x3, x4, x5) → Load34990ARR9(x1, x2, x4, x5)
Cond_Load34990ARR9(x1, x2, x3, x4, x5, x6) → Cond_Load34990ARR9(x1, x2, x3, x5, x6)
Load34990ARR10(x1, x2, x3, x4, x5, x6) → Load34990ARR10(x1, x2, x4, x5, x6)
Cond_Load34990ARR10(x1, x2, x3, x4, x5, x6, x7) → Cond_Load34990ARR10(x1, x2, x3, x5, x6, x7)

(24) Obligation:

ITRS 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 TRS R consists of the following rules:
Load34990(java.lang.Object(ARRAY(i4, a115115data)), i5816, i5824) → Load34990ARR3(java.lang.Object(ARRAY(i4, a115115data)), i5816, i5824)
Load34990ARR3(java.lang.Object(ARRAY(i4, a115115data)), i5816, i5824) → Cond_Load34990ARR3(i5816 + 1 > 0 && i5816 + 1 < i4 && i5816 > 0 && i5816 < i4 && i5824 > 0 && i5816 + 1 + 1 > 0, java.lang.Object(ARRAY(i4, a115115data)), i5816, i5824)
Cond_Load34990ARR3(TRUE, java.lang.Object(ARRAY(i4, a115115data)), i5816, i5824) → New39186(java.lang.Object(ARRAY(i4, a115115data)), i5816 + 1 + 1, i5824)
Inc35127(java.lang.Object(ARRAY(i4, a115115data)), i5816, i5824) → Load34990(java.lang.Object(ARRAY(i4, a115115data)), i5816, i5824 + -1)
Load34990(java.lang.Object(ARRAY(i4, a115115data)), i5816, i5824) → Cond_Load34990(i5824 > 0, java.lang.Object(ARRAY(i4, a115115data)), i5816, i5824)
Cond_Load34990(TRUE, java.lang.Object(ARRAY(i4, a115115data)), i5816, i5824) → Load34990(java.lang.Object(ARRAY(i4, a115115data)), i5816, i5824 + -1)
New39186(java.lang.Object(ARRAY(i4, a115115data)), i6609, i5824) → Inc35127(java.lang.Object(ARRAY(i4, a115115data)), i6609, i5824)
Load34990(java.lang.Object(ARRAY(i4, a115115data)), i5816, i5824) → Load34990ARR4(java.lang.Object(ARRAY(i4, a115115data)), i5816, i5824)
Load34990ARR4(java.lang.Object(ARRAY(i4, a115115data)), i5816, i5824) → Cond_Load34990ARR4(i5816 + 1 > 0 && i5816 + 1 < i4 && i5816 > 0 && i5816 < i4 && i5824 > 0 && i5816 + 1 + 1 > 0, java.lang.Object(ARRAY(i4, a115115data)), i5816, i5824)
Cond_Load34990ARR4(TRUE, java.lang.Object(ARRAY(i4, a115115data)), i5816, i5824) → Inc35127(java.lang.Object(ARRAY(i4, a115115data)), i5816 + 1 + 1, i5824)
New40185(java.lang.Object(ARRAY(i4, a115115data)), i6609, i5824) → Inc35127(java.lang.Object(ARRAY(i4, a115115data)), i6609, i5824)
Load34990(java.lang.Object(ARRAY(i4, a115115data)), i5816, i5824) → Load34990ARR5(java.lang.Object(ARRAY(i4, a115115data)), i5816, i5824, java.lang.Object(java.lang.String(i6986)))
Load34990ARR5(java.lang.Object(ARRAY(i4, a115115data)), i5816, i5824, java.lang.Object(java.lang.String(i6986))) → Cond_Load34990ARR5(!(i6986 = 0) && i5816 + 1 > 0 && i5816 + 1 < i4 && i5816 > 0 && i5816 < i4 && i5824 > 0 && i5816 + 1 + 1 > 0, java.lang.Object(ARRAY(i4, a115115data)), i5816, i5824, java.lang.Object(java.lang.String(i6986)))
Cond_Load34990ARR5(TRUE, java.lang.Object(ARRAY(i4, a115115data)), i5816, i5824, java.lang.Object(java.lang.String(i6986))) → Inc35127(java.lang.Object(ARRAY(i4, a115115data)), i5816 + 1 + 1, i5824)
New40288(java.lang.Object(ARRAY(i4, a115115data)), i6905, i5824) → Inc35127(java.lang.Object(ARRAY(i4, a115115data)), i6905, i5824)
Load34990(java.lang.Object(ARRAY(i4, a115115data)), i5816, i5824) → Load34990ARR6(java.lang.Object(ARRAY(i4, a115115data)), i5816, i5824, java.lang.Object(java.lang.String(i6164)))
Load34990ARR6(java.lang.Object(ARRAY(i4, a115115data)), i5816, i5824, java.lang.Object(java.lang.String(i6164))) → Cond_Load34990ARR6(i5816 + 1 > 0 && i5816 + 1 < i4 && !(i6164 = 0) && i5816 > 0 && i5816 < i4 && i5824 > 0 && i5816 + 1 + 1 > 0, java.lang.Object(ARRAY(i4, a115115data)), i5816, i5824, java.lang.Object(java.lang.String(i6164)))
Cond_Load34990ARR6(TRUE, java.lang.Object(ARRAY(i4, a115115data)), i5816, i5824, java.lang.Object(java.lang.String(i6164))) → Inc35127(java.lang.Object(ARRAY(i4, a115115data)), i5816 + 1 + 1, i5824)
New40846(java.lang.Object(ARRAY(i4, a115115data)), i6905, i5824) → Inc35127(java.lang.Object(ARRAY(i4, a115115data)), i6905, i5824)
Load34990(java.lang.Object(ARRAY(i4, a115115data)), i5816, i5824) → Load34990ARR7(java.lang.Object(ARRAY(i4, a115115data)), i5816, i5824, java.lang.Object(java.lang.String(i7504)), java.lang.Object(java.lang.String(i6164)))
Load34990ARR7(java.lang.Object(ARRAY(i4, a115115data)), i5816, i5824, java.lang.Object(java.lang.String(i7504)), java.lang.Object(java.lang.String(i6164))) → Cond_Load34990ARR7(!(i7504 = 0) && i5816 + 1 > 0 && i5816 + 1 < i4 && !(i6164 = 0) && i5816 > 0 && i5816 < i4 && i5824 > 0 && i5816 + 1 + 1 > 0, java.lang.Object(ARRAY(i4, a115115data)), i5816, i5824, java.lang.Object(java.lang.String(i7504)), java.lang.Object(java.lang.String(i6164)))
Cond_Load34990ARR7(TRUE, java.lang.Object(ARRAY(i4, a115115data)), i5816, i5824, java.lang.Object(java.lang.String(i7504)), java.lang.Object(java.lang.String(i6164))) → Inc35127(java.lang.Object(ARRAY(i4, a115115data)), i5816 + 1 + 1, i5824)
Load34990(java.lang.Object(ARRAY(i4, a115115data)), i5816, i5824) → Load34990ARR8(java.lang.Object(ARRAY(i4, a115115data)), i5816, i5824, java.lang.Object(java.lang.String(i6986)))
Load34990ARR8(java.lang.Object(ARRAY(i4, a115115data)), i5816, i5824, java.lang.Object(java.lang.String(i6986))) → Cond_Load34990ARR8(!(i6986 = 0) && i5816 + 1 > 0 && i5816 + 1 < i4 && i5816 > 0 && i5816 < i4 && i5824 > 0 && i5816 + 1 + 1 > 0, java.lang.Object(ARRAY(i4, a115115data)), i5816, i5824, java.lang.Object(java.lang.String(i6986)))
Cond_Load34990ARR8(TRUE, java.lang.Object(ARRAY(i4, a115115data)), i5816, i5824, java.lang.Object(java.lang.String(i6986))) → New40185(java.lang.Object(ARRAY(i4, a115115data)), i5816 + 1 + 1, i5824)
Load34990(java.lang.Object(ARRAY(i4, a115115data)), i5816, i5824) → Load34990ARR9(java.lang.Object(ARRAY(i4, a115115data)), i5816, i5824, java.lang.Object(java.lang.String(i6164)))
Load34990ARR9(java.lang.Object(ARRAY(i4, a115115data)), i5816, i5824, java.lang.Object(java.lang.String(i6164))) → Cond_Load34990ARR9(i5816 + 1 > 0 && i5816 + 1 < i4 && !(i6164 = 0) && i5816 > 0 && i5816 < i4 && i5824 > 0 && i5816 + 1 + 1 > 0, java.lang.Object(ARRAY(i4, a115115data)), i5816, i5824, java.lang.Object(java.lang.String(i6164)))
Cond_Load34990ARR9(TRUE, java.lang.Object(ARRAY(i4, a115115data)), i5816, i5824, java.lang.Object(java.lang.String(i6164))) → New40288(java.lang.Object(ARRAY(i4, a115115data)), i5816 + 1 + 1, i5824)
Load34990(java.lang.Object(ARRAY(i4, a115115data)), i5816, i5824) → Load34990ARR10(java.lang.Object(ARRAY(i4, a115115data)), i5816, i5824, java.lang.Object(java.lang.String(i7504)), java.lang.Object(java.lang.String(i6164)))
Load34990ARR10(java.lang.Object(ARRAY(i4, a115115data)), i5816, i5824, java.lang.Object(java.lang.String(i7504)), java.lang.Object(java.lang.String(i6164))) → Cond_Load34990ARR10(!(i7504 = 0) && i5816 + 1 > 0 && i5816 + 1 < i4 && !(i6164 = 0) && i5816 > 0 && i5816 < i4 && i5824 > 0 && i5816 + 1 + 1 > 0, java.lang.Object(ARRAY(i4, a115115data)), i5816, i5824, java.lang.Object(java.lang.String(i7504)), java.lang.Object(java.lang.String(i6164)))
Cond_Load34990ARR10(TRUE, java.lang.Object(ARRAY(i4, a115115data)), i5816, i5824, java.lang.Object(java.lang.String(i7504)), java.lang.Object(java.lang.String(i6164))) → New40846(java.lang.Object(ARRAY(i4, a115115data)), i5816 + 1 + 1, i5824)
The set Q consists of the following terms:
Load34990(java.lang.Object(ARRAY(x0, x1)), x2, x3)
Load34990ARR3(java.lang.Object(ARRAY(x0, x1)), x2, x3)
Cond_Load34990ARR3(TRUE, java.lang.Object(ARRAY(x0, x1)), x2, x3)
Inc35127(java.lang.Object(ARRAY(x0, x1)), x2, x3)
Cond_Load34990(TRUE, java.lang.Object(ARRAY(x0, x1)), x2, x3)
New39186(java.lang.Object(ARRAY(x0, x1)), x2, x3)
Load34990ARR4(java.lang.Object(ARRAY(x0, x1)), x2, x3)
Cond_Load34990ARR4(TRUE, java.lang.Object(ARRAY(x0, x1)), x2, x3)
New40185(java.lang.Object(ARRAY(x0, x1)), x2, x3)
Load34990ARR5(java.lang.Object(ARRAY(x0, x1)), x2, x3, java.lang.Object(java.lang.String(x4)))
Cond_Load34990ARR5(TRUE, java.lang.Object(ARRAY(x0, x1)), x2, x3, java.lang.Object(java.lang.String(x4)))
New40288(java.lang.Object(ARRAY(x0, x1)), x2, x3)
Load34990ARR6(java.lang.Object(ARRAY(x0, x1)), x2, x3, java.lang.Object(java.lang.String(x4)))
Cond_Load34990ARR6(TRUE, java.lang.Object(ARRAY(x0, x1)), x2, x3, java.lang.Object(java.lang.String(x4)))
New40846(java.lang.Object(ARRAY(x0, x1)), x2, x3)
Load34990ARR7(java.lang.Object(ARRAY(x0, x1)), x2, x3, java.lang.Object(java.lang.String(x4)), java.lang.Object(java.lang.String(x5)))
Cond_Load34990ARR7(TRUE, java.lang.Object(ARRAY(x0, x1)), x2, x3, java.lang.Object(java.lang.String(x4)), java.lang.Object(java.lang.String(x5)))
Load34990ARR8(java.lang.Object(ARRAY(x0, x1)), x2, x3, java.lang.Object(java.lang.String(x4)))
Cond_Load34990ARR8(TRUE, java.lang.Object(ARRAY(x0, x1)), x2, x3, java.lang.Object(java.lang.String(x4)))
Load34990ARR9(java.lang.Object(ARRAY(x0, x1)), x2, x3, java.lang.Object(java.lang.String(x4)))
Cond_Load34990ARR9(TRUE, java.lang.Object(ARRAY(x0, x1)), x2, x3, java.lang.Object(java.lang.String(x4)))
Load34990ARR10(java.lang.Object(ARRAY(x0, x1)), x2, x3, java.lang.Object(java.lang.String(x4)), java.lang.Object(java.lang.String(x5)))
Cond_Load34990ARR10(TRUE, java.lang.Object(ARRAY(x0, x1)), x2, x3, java.lang.Object(java.lang.String(x4)), java.lang.Object(java.lang.String(x5)))

(25) ITRSFSMergerProof (SOUND transformation)

The following function symbols have been merged:

New39186, New40185	>	New39186_3
New40288, New40846	>	New40288_3

(26) Obligation:

ITRS 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 TRS R consists of the following rules:
Load34990(java.lang.Object(ARRAY(i4, a115115data)), i5816, i5824) → Load34990ARR3(java.lang.Object(ARRAY(i4, a115115data)), i5816, i5824)
Load34990ARR3(java.lang.Object(ARRAY(i4, a115115data)), i5816, i5824) → Cond_Load34990ARR3(i5816 + 1 > 0 && i5816 + 1 < i4 && i5816 > 0 && i5816 < i4 && i5824 > 0 && i5816 + 1 + 1 > 0, java.lang.Object(ARRAY(i4, a115115data)), i5816, i5824)
Cond_Load34990ARR3(TRUE, java.lang.Object(ARRAY(i4, a115115data)), i5816, i5824) → New39186(java.lang.Object(ARRAY(i4, a115115data)), i5816 + 1 + 1, i5824)
Inc35127(java.lang.Object(ARRAY(i4, a115115data)), i5816, i5824) → Load34990(java.lang.Object(ARRAY(i4, a115115data)), i5816, i5824 + -1)
Load34990(java.lang.Object(ARRAY(i4, a115115data)), i5816, i5824) → Cond_Load34990(i5824 > 0, java.lang.Object(ARRAY(i4, a115115data)), i5816, i5824)
Cond_Load34990(TRUE, java.lang.Object(ARRAY(i4, a115115data)), i5816, i5824) → Load34990(java.lang.Object(ARRAY(i4, a115115data)), i5816, i5824 + -1)
New39186(java.lang.Object(ARRAY(i4, a115115data)), i6609, i5824) → Inc35127(java.lang.Object(ARRAY(i4, a115115data)), i6609, i5824)
Load34990(java.lang.Object(ARRAY(i4, a115115data)), i5816, i5824) → Load34990ARR4(java.lang.Object(ARRAY(i4, a115115data)), i5816, i5824)
Load34990ARR4(java.lang.Object(ARRAY(i4, a115115data)), i5816, i5824) → Cond_Load34990ARR4(i5816 + 1 > 0 && i5816 + 1 < i4 && i5816 > 0 && i5816 < i4 && i5824 > 0 && i5816 + 1 + 1 > 0, java.lang.Object(ARRAY(i4, a115115data)), i5816, i5824)
Cond_Load34990ARR4(TRUE, java.lang.Object(ARRAY(i4, a115115data)), i5816, i5824) → Inc35127(java.lang.Object(ARRAY(i4, a115115data)), i5816 + 1 + 1, i5824)
Load34990(java.lang.Object(ARRAY(i4, a115115data)), i5816, i5824) → Load34990ARR5(java.lang.Object(ARRAY(i4, a115115data)), i5816, i5824, java.lang.Object(java.lang.String(i6986)))
Load34990ARR5(java.lang.Object(ARRAY(i4, a115115data)), i5816, i5824, java.lang.Object(java.lang.String(i6986))) → Cond_Load34990ARR5(!(i6986 = 0) && i5816 + 1 > 0 && i5816 + 1 < i4 && i5816 > 0 && i5816 < i4 && i5824 > 0 && i5816 + 1 + 1 > 0, java.lang.Object(ARRAY(i4, a115115data)), i5816, i5824, java.lang.Object(java.lang.String(i6986)))
Cond_Load34990ARR5(TRUE, java.lang.Object(ARRAY(i4, a115115data)), i5816, i5824, java.lang.Object(java.lang.String(i6986))) → Inc35127(java.lang.Object(ARRAY(i4, a115115data)), i5816 + 1 + 1, i5824)
New40288(java.lang.Object(ARRAY(i4, a115115data)), i6905, i5824) → Inc35127(java.lang.Object(ARRAY(i4, a115115data)), i6905, i5824)
Load34990(java.lang.Object(ARRAY(i4, a115115data)), i5816, i5824) → Load34990ARR6(java.lang.Object(ARRAY(i4, a115115data)), i5816, i5824, java.lang.Object(java.lang.String(i6164)))
Load34990ARR6(java.lang.Object(ARRAY(i4, a115115data)), i5816, i5824, java.lang.Object(java.lang.String(i6164))) → Cond_Load34990ARR6(i5816 + 1 > 0 && i5816 + 1 < i4 && !(i6164 = 0) && i5816 > 0 && i5816 < i4 && i5824 > 0 && i5816 + 1 + 1 > 0, java.lang.Object(ARRAY(i4, a115115data)), i5816, i5824, java.lang.Object(java.lang.String(i6164)))
Cond_Load34990ARR6(TRUE, java.lang.Object(ARRAY(i4, a115115data)), i5816, i5824, java.lang.Object(java.lang.String(i6164))) → Inc35127(java.lang.Object(ARRAY(i4, a115115data)), i5816 + 1 + 1, i5824)
Load34990(java.lang.Object(ARRAY(i4, a115115data)), i5816, i5824) → Load34990ARR7(java.lang.Object(ARRAY(i4, a115115data)), i5816, i5824, java.lang.Object(java.lang.String(i7504)), java.lang.Object(java.lang.String(i6164)))
Load34990ARR7(java.lang.Object(ARRAY(i4, a115115data)), i5816, i5824, java.lang.Object(java.lang.String(i7504)), java.lang.Object(java.lang.String(i6164))) → Cond_Load34990ARR7(!(i7504 = 0) && i5816 + 1 > 0 && i5816 + 1 < i4 && !(i6164 = 0) && i5816 > 0 && i5816 < i4 && i5824 > 0 && i5816 + 1 + 1 > 0, java.lang.Object(ARRAY(i4, a115115data)), i5816, i5824, java.lang.Object(java.lang.String(i7504)), java.lang.Object(java.lang.String(i6164)))
Cond_Load34990ARR7(TRUE, java.lang.Object(ARRAY(i4, a115115data)), i5816, i5824, java.lang.Object(java.lang.String(i7504)), java.lang.Object(java.lang.String(i6164))) → Inc35127(java.lang.Object(ARRAY(i4, a115115data)), i5816 + 1 + 1, i5824)
Load34990(java.lang.Object(ARRAY(i4, a115115data)), i5816, i5824) → Load34990ARR8(java.lang.Object(ARRAY(i4, a115115data)), i5816, i5824, java.lang.Object(java.lang.String(i6986)))
Load34990ARR8(java.lang.Object(ARRAY(i4, a115115data)), i5816, i5824, java.lang.Object(java.lang.String(i6986))) → Cond_Load34990ARR8(!(i6986 = 0) && i5816 + 1 > 0 && i5816 + 1 < i4 && i5816 > 0 && i5816 < i4 && i5824 > 0 && i5816 + 1 + 1 > 0, java.lang.Object(ARRAY(i4, a115115data)), i5816, i5824, java.lang.Object(java.lang.String(i6986)))
Cond_Load34990ARR8(TRUE, java.lang.Object(ARRAY(i4, a115115data)), i5816, i5824, java.lang.Object(java.lang.String(i6986))) → New39186(java.lang.Object(ARRAY(i4, a115115data)), i5816 + 1 + 1, i5824)
Load34990(java.lang.Object(ARRAY(i4, a115115data)), i5816, i5824) → Load34990ARR9(java.lang.Object(ARRAY(i4, a115115data)), i5816, i5824, java.lang.Object(java.lang.String(i6164)))
Load34990ARR9(java.lang.Object(ARRAY(i4, a115115data)), i5816, i5824, java.lang.Object(java.lang.String(i6164))) → Cond_Load34990ARR9(i5816 + 1 > 0 && i5816 + 1 < i4 && !(i6164 = 0) && i5816 > 0 && i5816 < i4 && i5824 > 0 && i5816 + 1 + 1 > 0, java.lang.Object(ARRAY(i4, a115115data)), i5816, i5824, java.lang.Object(java.lang.String(i6164)))
Cond_Load34990ARR9(TRUE, java.lang.Object(ARRAY(i4, a115115data)), i5816, i5824, java.lang.Object(java.lang.String(i6164))) → New40288(java.lang.Object(ARRAY(i4, a115115data)), i5816 + 1 + 1, i5824)
Load34990(java.lang.Object(ARRAY(i4, a115115data)), i5816, i5824) → Load34990ARR10(java.lang.Object(ARRAY(i4, a115115data)), i5816, i5824, java.lang.Object(java.lang.String(i7504)), java.lang.Object(java.lang.String(i6164)))
Load34990ARR10(java.lang.Object(ARRAY(i4, a115115data)), i5816, i5824, java.lang.Object(java.lang.String(i7504)), java.lang.Object(java.lang.String(i6164))) → Cond_Load34990ARR10(!(i7504 = 0) && i5816 + 1 > 0 && i5816 + 1 < i4 && !(i6164 = 0) && i5816 > 0 && i5816 < i4 && i5824 > 0 && i5816 + 1 + 1 > 0, java.lang.Object(ARRAY(i4, a115115data)), i5816, i5824, java.lang.Object(java.lang.String(i7504)), java.lang.Object(java.lang.String(i6164)))
Cond_Load34990ARR10(TRUE, java.lang.Object(ARRAY(i4, a115115data)), i5816, i5824, java.lang.Object(java.lang.String(i7504)), java.lang.Object(java.lang.String(i6164))) → New40288(java.lang.Object(ARRAY(i4, a115115data)), i5816 + 1 + 1, i5824)
The set Q consists of the following terms:
Load34990(java.lang.Object(ARRAY(x0, x1)), x2, x3)
Load34990ARR3(java.lang.Object(ARRAY(x0, x1)), x2, x3)
Cond_Load34990ARR3(TRUE, java.lang.Object(ARRAY(x0, x1)), x2, x3)
Inc35127(java.lang.Object(ARRAY(x0, x1)), x2, x3)
Cond_Load34990(TRUE, java.lang.Object(ARRAY(x0, x1)), x2, x3)
New39186(java.lang.Object(ARRAY(x0, x1)), x2, x3)
Load34990ARR4(java.lang.Object(ARRAY(x0, x1)), x2, x3)
Cond_Load34990ARR4(TRUE, java.lang.Object(ARRAY(x0, x1)), x2, x3)
Load34990ARR5(java.lang.Object(ARRAY(x0, x1)), x2, x3, java.lang.Object(java.lang.String(x4)))
Cond_Load34990ARR5(TRUE, java.lang.Object(ARRAY(x0, x1)), x2, x3, java.lang.Object(java.lang.String(x4)))
New40288(java.lang.Object(ARRAY(x0, x1)), x2, x3)
Load34990ARR6(java.lang.Object(ARRAY(x0, x1)), x2, x3, java.lang.Object(java.lang.String(x4)))
Cond_Load34990ARR6(TRUE, java.lang.Object(ARRAY(x0, x1)), x2, x3, java.lang.Object(java.lang.String(x4)))
Load34990ARR7(java.lang.Object(ARRAY(x0, x1)), x2, x3, java.lang.Object(java.lang.String(x4)), java.lang.Object(java.lang.String(x5)))
Cond_Load34990ARR7(TRUE, java.lang.Object(ARRAY(x0, x1)), x2, x3, java.lang.Object(java.lang.String(x4)), java.lang.Object(java.lang.String(x5)))
Load34990ARR8(java.lang.Object(ARRAY(x0, x1)), x2, x3, java.lang.Object(java.lang.String(x4)))
Cond_Load34990ARR8(TRUE, java.lang.Object(ARRAY(x0, x1)), x2, x3, java.lang.Object(java.lang.String(x4)))
Load34990ARR9(java.lang.Object(ARRAY(x0, x1)), x2, x3, java.lang.Object(java.lang.String(x4)))
Cond_Load34990ARR9(TRUE, java.lang.Object(ARRAY(x0, x1)), x2, x3, java.lang.Object(java.lang.String(x4)))
Load34990ARR10(java.lang.Object(ARRAY(x0, x1)), x2, x3, java.lang.Object(java.lang.String(x4)), java.lang.Object(java.lang.String(x5)))
Cond_Load34990ARR10(TRUE, java.lang.Object(ARRAY(x0, x1)), x2, x3, java.lang.Object(java.lang.String(x4)), java.lang.Object(java.lang.String(x5)))

(27) ITRStoIDPProof (EQUIVALENT transformation)

Added dependency pairs

(28) 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

The ITRS R consists of the following rules:
Load34990(java.lang.Object(ARRAY(i4, a115115data)), i5816, i5824) → Load34990ARR3(java.lang.Object(ARRAY(i4, a115115data)), i5816, i5824)
Load34990ARR3(java.lang.Object(ARRAY(i4, a115115data)), i5816, i5824) → Cond_Load34990ARR3(i5816 + 1 > 0 && i5816 + 1 < i4 && i5816 > 0 && i5816 < i4 && i5824 > 0 && i5816 + 1 + 1 > 0, java.lang.Object(ARRAY(i4, a115115data)), i5816, i5824)
Cond_Load34990ARR3(TRUE, java.lang.Object(ARRAY(i4, a115115data)), i5816, i5824) → New39186(java.lang.Object(ARRAY(i4, a115115data)), i5816 + 1 + 1, i5824)
Inc35127(java.lang.Object(ARRAY(i4, a115115data)), i5816, i5824) → Load34990(java.lang.Object(ARRAY(i4, a115115data)), i5816, i5824 + -1)
Load34990(java.lang.Object(ARRAY(i4, a115115data)), i5816, i5824) → Cond_Load34990(i5824 > 0, java.lang.Object(ARRAY(i4, a115115data)), i5816, i5824)
Cond_Load34990(TRUE, java.lang.Object(ARRAY(i4, a115115data)), i5816, i5824) → Load34990(java.lang.Object(ARRAY(i4, a115115data)), i5816, i5824 + -1)
New39186(java.lang.Object(ARRAY(i4, a115115data)), i6609, i5824) → Inc35127(java.lang.Object(ARRAY(i4, a115115data)), i6609, i5824)
Load34990(java.lang.Object(ARRAY(i4, a115115data)), i5816, i5824) → Load34990ARR4(java.lang.Object(ARRAY(i4, a115115data)), i5816, i5824)
Load34990ARR4(java.lang.Object(ARRAY(i4, a115115data)), i5816, i5824) → Cond_Load34990ARR4(i5816 + 1 > 0 && i5816 + 1 < i4 && i5816 > 0 && i5816 < i4 && i5824 > 0 && i5816 + 1 + 1 > 0, java.lang.Object(ARRAY(i4, a115115data)), i5816, i5824)
Cond_Load34990ARR4(TRUE, java.lang.Object(ARRAY(i4, a115115data)), i5816, i5824) → Inc35127(java.lang.Object(ARRAY(i4, a115115data)), i5816 + 1 + 1, i5824)
Load34990(java.lang.Object(ARRAY(i4, a115115data)), i5816, i5824) → Load34990ARR5(java.lang.Object(ARRAY(i4, a115115data)), i5816, i5824, java.lang.Object(java.lang.String(i6986)))
Load34990ARR5(java.lang.Object(ARRAY(i4, a115115data)), i5816, i5824, java.lang.Object(java.lang.String(i6986))) → Cond_Load34990ARR5(!(i6986 = 0) && i5816 + 1 > 0 && i5816 + 1 < i4 && i5816 > 0 && i5816 < i4 && i5824 > 0 && i5816 + 1 + 1 > 0, java.lang.Object(ARRAY(i4, a115115data)), i5816, i5824, java.lang.Object(java.lang.String(i6986)))
Cond_Load34990ARR5(TRUE, java.lang.Object(ARRAY(i4, a115115data)), i5816, i5824, java.lang.Object(java.lang.String(i6986))) → Inc35127(java.lang.Object(ARRAY(i4, a115115data)), i5816 + 1 + 1, i5824)
New40288(java.lang.Object(ARRAY(i4, a115115data)), i6905, i5824) → Inc35127(java.lang.Object(ARRAY(i4, a115115data)), i6905, i5824)
Load34990(java.lang.Object(ARRAY(i4, a115115data)), i5816, i5824) → Load34990ARR6(java.lang.Object(ARRAY(i4, a115115data)), i5816, i5824, java.lang.Object(java.lang.String(i6164)))
Load34990ARR6(java.lang.Object(ARRAY(i4, a115115data)), i5816, i5824, java.lang.Object(java.lang.String(i6164))) → Cond_Load34990ARR6(i5816 + 1 > 0 && i5816 + 1 < i4 && !(i6164 = 0) && i5816 > 0 && i5816 < i4 && i5824 > 0 && i5816 + 1 + 1 > 0, java.lang.Object(ARRAY(i4, a115115data)), i5816, i5824, java.lang.Object(java.lang.String(i6164)))
Cond_Load34990ARR6(TRUE, java.lang.Object(ARRAY(i4, a115115data)), i5816, i5824, java.lang.Object(java.lang.String(i6164))) → Inc35127(java.lang.Object(ARRAY(i4, a115115data)), i5816 + 1 + 1, i5824)
Load34990(java.lang.Object(ARRAY(i4, a115115data)), i5816, i5824) → Load34990ARR7(java.lang.Object(ARRAY(i4, a115115data)), i5816, i5824, java.lang.Object(java.lang.String(i7504)), java.lang.Object(java.lang.String(i6164)))
Load34990ARR7(java.lang.Object(ARRAY(i4, a115115data)), i5816, i5824, java.lang.Object(java.lang.String(i7504)), java.lang.Object(java.lang.String(i6164))) → Cond_Load34990ARR7(!(i7504 = 0) && i5816 + 1 > 0 && i5816 + 1 < i4 && !(i6164 = 0) && i5816 > 0 && i5816 < i4 && i5824 > 0 && i5816 + 1 + 1 > 0, java.lang.Object(ARRAY(i4, a115115data)), i5816, i5824, java.lang.Object(java.lang.String(i7504)), java.lang.Object(java.lang.String(i6164)))
Cond_Load34990ARR7(TRUE, java.lang.Object(ARRAY(i4, a115115data)), i5816, i5824, java.lang.Object(java.lang.String(i7504)), java.lang.Object(java.lang.String(i6164))) → Inc35127(java.lang.Object(ARRAY(i4, a115115data)), i5816 + 1 + 1, i5824)
Load34990(java.lang.Object(ARRAY(i4, a115115data)), i5816, i5824) → Load34990ARR8(java.lang.Object(ARRAY(i4, a115115data)), i5816, i5824, java.lang.Object(java.lang.String(i6986)))
Load34990ARR8(java.lang.Object(ARRAY(i4, a115115data)), i5816, i5824, java.lang.Object(java.lang.String(i6986))) → Cond_Load34990ARR8(!(i6986 = 0) && i5816 + 1 > 0 && i5816 + 1 < i4 && i5816 > 0 && i5816 < i4 && i5824 > 0 && i5816 + 1 + 1 > 0, java.lang.Object(ARRAY(i4, a115115data)), i5816, i5824, java.lang.Object(java.lang.String(i6986)))
Cond_Load34990ARR8(TRUE, java.lang.Object(ARRAY(i4, a115115data)), i5816, i5824, java.lang.Object(java.lang.String(i6986))) → New39186(java.lang.Object(ARRAY(i4, a115115data)), i5816 + 1 + 1, i5824)
Load34990(java.lang.Object(ARRAY(i4, a115115data)), i5816, i5824) → Load34990ARR9(java.lang.Object(ARRAY(i4, a115115data)), i5816, i5824, java.lang.Object(java.lang.String(i6164)))
Load34990ARR9(java.lang.Object(ARRAY(i4, a115115data)), i5816, i5824, java.lang.Object(java.lang.String(i6164))) → Cond_Load34990ARR9(i5816 + 1 > 0 && i5816 + 1 < i4 && !(i6164 = 0) && i5816 > 0 && i5816 < i4 && i5824 > 0 && i5816 + 1 + 1 > 0, java.lang.Object(ARRAY(i4, a115115data)), i5816, i5824, java.lang.Object(java.lang.String(i6164)))
Cond_Load34990ARR9(TRUE, java.lang.Object(ARRAY(i4, a115115data)), i5816, i5824, java.lang.Object(java.lang.String(i6164))) → New40288(java.lang.Object(ARRAY(i4, a115115data)), i5816 + 1 + 1, i5824)
Load34990(java.lang.Object(ARRAY(i4, a115115data)), i5816, i5824) → Load34990ARR10(java.lang.Object(ARRAY(i4, a115115data)), i5816, i5824, java.lang.Object(java.lang.String(i7504)), java.lang.Object(java.lang.String(i6164)))
Load34990ARR10(java.lang.Object(ARRAY(i4, a115115data)), i5816, i5824, java.lang.Object(java.lang.String(i7504)), java.lang.Object(java.lang.String(i6164))) → Cond_Load34990ARR10(!(i7504 = 0) && i5816 + 1 > 0 && i5816 + 1 < i4 && !(i6164 = 0) && i5816 > 0 && i5816 < i4 && i5824 > 0 && i5816 + 1 + 1 > 0, java.lang.Object(ARRAY(i4, a115115data)), i5816, i5824, java.lang.Object(java.lang.String(i7504)), java.lang.Object(java.lang.String(i6164)))
Cond_Load34990ARR10(TRUE, java.lang.Object(ARRAY(i4, a115115data)), i5816, i5824, java.lang.Object(java.lang.String(i7504)), java.lang.Object(java.lang.String(i6164))) → New40288(java.lang.Object(ARRAY(i4, a115115data)), i5816 + 1 + 1, i5824)

The integer pair graph contains the following rules and edges:
(0): LOAD34990(java.lang.Object(ARRAY(i4[0], a115115data[0])), i5816[0], i5824[0]) → LOAD34990ARR3(java.lang.Object(ARRAY(i4[0], a115115data[0])), i5816[0], i5824[0])
(1): LOAD34990ARR3(java.lang.Object(ARRAY(i4[1], a115115data[1])), i5816[1], i5824[1]) → COND_LOAD34990ARR3(i5816[1] + 1 > 0 && i5816[1] + 1 < i4[1] && i5816[1] > 0 && i5816[1] < i4[1] && i5824[1] > 0 && i5816[1] + 1 + 1 > 0, java.lang.Object(ARRAY(i4[1], a115115data[1])), i5816[1], i5824[1])
(2): COND_LOAD34990ARR3(TRUE, java.lang.Object(ARRAY(i4[2], a115115data[2])), i5816[2], i5824[2]) → NEW39186(java.lang.Object(ARRAY(i4[2], a115115data[2])), i5816[2] + 1 + 1, i5824[2])
(3): INC35127(java.lang.Object(ARRAY(i4[3], a115115data[3])), i5816[3], i5824[3]) → LOAD34990(java.lang.Object(ARRAY(i4[3], a115115data[3])), i5816[3], i5824[3] + -1)
(4): LOAD34990(java.lang.Object(ARRAY(i4[4], a115115data[4])), i5816[4], i5824[4]) → COND_LOAD34990(i5824[4] > 0, java.lang.Object(ARRAY(i4[4], a115115data[4])), i5816[4], i5824[4])
(5): COND_LOAD34990(TRUE, java.lang.Object(ARRAY(i4[5], a115115data[5])), i5816[5], i5824[5]) → LOAD34990(java.lang.Object(ARRAY(i4[5], a115115data[5])), i5816[5], i5824[5] + -1)
(6): NEW39186(java.lang.Object(ARRAY(i4[6], a115115data[6])), i6609[6], i5824[6]) → INC35127(java.lang.Object(ARRAY(i4[6], a115115data[6])), i6609[6], i5824[6])
(7): LOAD34990(java.lang.Object(ARRAY(i4[7], a115115data[7])), i5816[7], i5824[7]) → LOAD34990ARR4(java.lang.Object(ARRAY(i4[7], a115115data[7])), i5816[7], i5824[7])
(8): LOAD34990ARR4(java.lang.Object(ARRAY(i4[8], a115115data[8])), i5816[8], i5824[8]) → COND_LOAD34990ARR4(i5816[8] + 1 > 0 && i5816[8] + 1 < i4[8] && i5816[8] > 0 && i5816[8] < i4[8] && i5824[8] > 0 && i5816[8] + 1 + 1 > 0, java.lang.Object(ARRAY(i4[8], a115115data[8])), i5816[8], i5824[8])
(9): COND_LOAD34990ARR4(TRUE, java.lang.Object(ARRAY(i4[9], a115115data[9])), i5816[9], i5824[9]) → INC35127(java.lang.Object(ARRAY(i4[9], a115115data[9])), i5816[9] + 1 + 1, i5824[9])
(10): LOAD34990(java.lang.Object(ARRAY(i4[10], a115115data[10])), i5816[10], i5824[10]) → LOAD34990ARR5(java.lang.Object(ARRAY(i4[10], a115115data[10])), i5816[10], i5824[10], java.lang.Object(java.lang.String(i6986[10])))
(11): LOAD34990ARR5(java.lang.Object(ARRAY(i4[11], a115115data[11])), i5816[11], i5824[11], java.lang.Object(java.lang.String(i6986[11]))) → COND_LOAD34990ARR5(!(i6986[11] = 0) && i5816[11] + 1 > 0 && i5816[11] + 1 < i4[11] && i5816[11] > 0 && i5816[11] < i4[11] && i5824[11] > 0 && i5816[11] + 1 + 1 > 0, java.lang.Object(ARRAY(i4[11], a115115data[11])), i5816[11], i5824[11], java.lang.Object(java.lang.String(i6986[11])))
(12): COND_LOAD34990ARR5(TRUE, java.lang.Object(ARRAY(i4[12], a115115data[12])), i5816[12], i5824[12], java.lang.Object(java.lang.String(i6986[12]))) → INC35127(java.lang.Object(ARRAY(i4[12], a115115data[12])), i5816[12] + 1 + 1, i5824[12])
(13): NEW40288(java.lang.Object(ARRAY(i4[13], a115115data[13])), i6905[13], i5824[13]) → INC35127(java.lang.Object(ARRAY(i4[13], a115115data[13])), i6905[13], i5824[13])
(14): LOAD34990(java.lang.Object(ARRAY(i4[14], a115115data[14])), i5816[14], i5824[14]) → LOAD34990ARR6(java.lang.Object(ARRAY(i4[14], a115115data[14])), i5816[14], i5824[14], java.lang.Object(java.lang.String(i6164[14])))
(15): LOAD34990ARR6(java.lang.Object(ARRAY(i4[15], a115115data[15])), i5816[15], i5824[15], java.lang.Object(java.lang.String(i6164[15]))) → COND_LOAD34990ARR6(i5816[15] + 1 > 0 && i5816[15] + 1 < i4[15] && !(i6164[15] = 0) && i5816[15] > 0 && i5816[15] < i4[15] && i5824[15] > 0 && i5816[15] + 1 + 1 > 0, java.lang.Object(ARRAY(i4[15], a115115data[15])), i5816[15], i5824[15], java.lang.Object(java.lang.String(i6164[15])))
(16): COND_LOAD34990ARR6(TRUE, java.lang.Object(ARRAY(i4[16], a115115data[16])), i5816[16], i5824[16], java.lang.Object(java.lang.String(i6164[16]))) → INC35127(java.lang.Object(ARRAY(i4[16], a115115data[16])), i5816[16] + 1 + 1, i5824[16])
(17): LOAD34990(java.lang.Object(ARRAY(i4[17], a115115data[17])), i5816[17], i5824[17]) → LOAD34990ARR7(java.lang.Object(ARRAY(i4[17], a115115data[17])), i5816[17], i5824[17], java.lang.Object(java.lang.String(i7504[17])), java.lang.Object(java.lang.String(i6164[17])))
(18): LOAD34990ARR7(java.lang.Object(ARRAY(i4[18], a115115data[18])), i5816[18], i5824[18], java.lang.Object(java.lang.String(i7504[18])), java.lang.Object(java.lang.String(i6164[18]))) → COND_LOAD34990ARR7(!(i7504[18] = 0) && i5816[18] + 1 > 0 && i5816[18] + 1 < i4[18] && !(i6164[18] = 0) && i5816[18] > 0 && i5816[18] < i4[18] && i5824[18] > 0 && i5816[18] + 1 + 1 > 0, java.lang.Object(ARRAY(i4[18], a115115data[18])), i5816[18], i5824[18], java.lang.Object(java.lang.String(i7504[18])), java.lang.Object(java.lang.String(i6164[18])))
(19): COND_LOAD34990ARR7(TRUE, java.lang.Object(ARRAY(i4[19], a115115data[19])), i5816[19], i5824[19], java.lang.Object(java.lang.String(i7504[19])), java.lang.Object(java.lang.String(i6164[19]))) → INC35127(java.lang.Object(ARRAY(i4[19], a115115data[19])), i5816[19] + 1 + 1, i5824[19])
(20): LOAD34990(java.lang.Object(ARRAY(i4[20], a115115data[20])), i5816[20], i5824[20]) → LOAD34990ARR8(java.lang.Object(ARRAY(i4[20], a115115data[20])), i5816[20], i5824[20], java.lang.Object(java.lang.String(i6986[20])))
(21): LOAD34990ARR8(java.lang.Object(ARRAY(i4[21], a115115data[21])), i5816[21], i5824[21], java.lang.Object(java.lang.String(i6986[21]))) → COND_LOAD34990ARR8(!(i6986[21] = 0) && i5816[21] + 1 > 0 && i5816[21] + 1 < i4[21] && i5816[21] > 0 && i5816[21] < i4[21] && i5824[21] > 0 && i5816[21] + 1 + 1 > 0, java.lang.Object(ARRAY(i4[21], a115115data[21])), i5816[21], i5824[21], java.lang.Object(java.lang.String(i6986[21])))
(22): COND_LOAD34990ARR8(TRUE, java.lang.Object(ARRAY(i4[22], a115115data[22])), i5816[22], i5824[22], java.lang.Object(java.lang.String(i6986[22]))) → NEW39186(java.lang.Object(ARRAY(i4[22], a115115data[22])), i5816[22] + 1 + 1, i5824[22])
(23): LOAD34990(java.lang.Object(ARRAY(i4[23], a115115data[23])), i5816[23], i5824[23]) → LOAD34990ARR9(java.lang.Object(ARRAY(i4[23], a115115data[23])), i5816[23], i5824[23], java.lang.Object(java.lang.String(i6164[23])))
(24): LOAD34990ARR9(java.lang.Object(ARRAY(i4[24], a115115data[24])), i5816[24], i5824[24], java.lang.Object(java.lang.String(i6164[24]))) → COND_LOAD34990ARR9(i5816[24] + 1 > 0 && i5816[24] + 1 < i4[24] && !(i6164[24] = 0) && i5816[24] > 0 && i5816[24] < i4[24] && i5824[24] > 0 && i5816[24] + 1 + 1 > 0, java.lang.Object(ARRAY(i4[24], a115115data[24])), i5816[24], i5824[24], java.lang.Object(java.lang.String(i6164[24])))
(25): COND_LOAD34990ARR9(TRUE, java.lang.Object(ARRAY(i4[25], a115115data[25])), i5816[25], i5824[25], java.lang.Object(java.lang.String(i6164[25]))) → NEW40288(java.lang.Object(ARRAY(i4[25], a115115data[25])), i5816[25] + 1 + 1, i5824[25])
(26): LOAD34990(java.lang.Object(ARRAY(i4[26], a115115data[26])), i5816[26], i5824[26]) → LOAD34990ARR10(java.lang.Object(ARRAY(i4[26], a115115data[26])), i5816[26], i5824[26], java.lang.Object(java.lang.String(i7504[26])), java.lang.Object(java.lang.String(i6164[26])))
(27): LOAD34990ARR10(java.lang.Object(ARRAY(i4[27], a115115data[27])), i5816[27], i5824[27], java.lang.Object(java.lang.String(i7504[27])), java.lang.Object(java.lang.String(i6164[27]))) → COND_LOAD34990ARR10(!(i7504[27] = 0) && i5816[27] + 1 > 0 && i5816[27] + 1 < i4[27] && !(i6164[27] = 0) && i5816[27] > 0 && i5816[27] < i4[27] && i5824[27] > 0 && i5816[27] + 1 + 1 > 0, java.lang.Object(ARRAY(i4[27], a115115data[27])), i5816[27], i5824[27], java.lang.Object(java.lang.String(i7504[27])), java.lang.Object(java.lang.String(i6164[27])))
(28): COND_LOAD34990ARR10(TRUE, java.lang.Object(ARRAY(i4[28], a115115data[28])), i5816[28], i5824[28], java.lang.Object(java.lang.String(i7504[28])), java.lang.Object(java.lang.String(i6164[28]))) → NEW40288(java.lang.Object(ARRAY(i4[28], a115115data[28])), i5816[28] + 1 + 1, i5824[28])

(0) -> (1), if ((java.lang.Object(ARRAY(i4[0], a115115data[0])) →^* java.lang.Object(ARRAY(i4[1], a115115data[1])))∧(i5824[0] →^* i5824[1])∧(i5816[0] →^* i5816[1]))

(1) -> (2), if ((i5824[1] →^* i5824[2])∧(i5816[1] →^* i5816[2])∧(java.lang.Object(ARRAY(i4[1], a115115data[1])) →^* java.lang.Object(ARRAY(i4[2], a115115data[2])))∧(i5816[1] + 1 > 0 && i5816[1] + 1 < i4[1] && i5816[1] > 0 && i5816[1] < i4[1] && i5824[1] > 0 && i5816[1] + 1 + 1 > 0 →^* TRUE))

(2) -> (6), if ((i5824[2] →^* i5824[6])∧(i5816[2] + 1 + 1 →^* i6609[6])∧(java.lang.Object(ARRAY(i4[2], a115115data[2])) →^* java.lang.Object(ARRAY(i4[6], a115115data[6]))))

(3) -> (0), if ((i5824[3] + -1 →^* i5824[0])∧(i5816[3] →^* i5816[0])∧(java.lang.Object(ARRAY(i4[3], a115115data[3])) →^* java.lang.Object(ARRAY(i4[0], a115115data[0]))))

(3) -> (4), if ((i5824[3] + -1 →^* i5824[4])∧(java.lang.Object(ARRAY(i4[3], a115115data[3])) →^* java.lang.Object(ARRAY(i4[4], a115115data[4])))∧(i5816[3] →^* i5816[4]))

(3) -> (7), if ((i5824[3] + -1 →^* i5824[7])∧(java.lang.Object(ARRAY(i4[3], a115115data[3])) →^* java.lang.Object(ARRAY(i4[7], a115115data[7])))∧(i5816[3] →^* i5816[7]))

(3) -> (10), if ((i5824[3] + -1 →^* i5824[10])∧(java.lang.Object(ARRAY(i4[3], a115115data[3])) →^* java.lang.Object(ARRAY(i4[10], a115115data[10])))∧(i5816[3] →^* i5816[10]))

(3) -> (14), if ((i5816[3] →^* i5816[14])∧(java.lang.Object(ARRAY(i4[3], a115115data[3])) →^* java.lang.Object(ARRAY(i4[14], a115115data[14])))∧(i5824[3] + -1 →^* i5824[14]))

(3) -> (17), if ((i5824[3] + -1 →^* i5824[17])∧(i5816[3] →^* i5816[17])∧(java.lang.Object(ARRAY(i4[3], a115115data[3])) →^* java.lang.Object(ARRAY(i4[17], a115115data[17]))))

(3) -> (20), if ((java.lang.Object(ARRAY(i4[3], a115115data[3])) →^* java.lang.Object(ARRAY(i4[20], a115115data[20])))∧(i5816[3] →^* i5816[20])∧(i5824[3] + -1 →^* i5824[20]))

(3) -> (23), if ((i5824[3] + -1 →^* i5824[23])∧(java.lang.Object(ARRAY(i4[3], a115115data[3])) →^* java.lang.Object(ARRAY(i4[23], a115115data[23])))∧(i5816[3] →^* i5816[23]))

(3) -> (26), if ((java.lang.Object(ARRAY(i4[3], a115115data[3])) →^* java.lang.Object(ARRAY(i4[26], a115115data[26])))∧(i5816[3] →^* i5816[26])∧(i5824[3] + -1 →^* i5824[26]))

(4) -> (5), if ((java.lang.Object(ARRAY(i4[4], a115115data[4])) →^* java.lang.Object(ARRAY(i4[5], a115115data[5])))∧(i5816[4] →^* i5816[5])∧(i5824[4] →^* i5824[5])∧(i5824[4] > 0 →^* TRUE))

(5) -> (0), if ((i5816[5] →^* i5816[0])∧(i5824[5] + -1 →^* i5824[0])∧(java.lang.Object(ARRAY(i4[5], a115115data[5])) →^* java.lang.Object(ARRAY(i4[0], a115115data[0]))))

(5) -> (4), if ((i5824[5] + -1 →^* i5824[4])∧(java.lang.Object(ARRAY(i4[5], a115115data[5])) →^* java.lang.Object(ARRAY(i4[4], a115115data[4])))∧(i5816[5] →^* i5816[4]))

(5) -> (7), if ((i5816[5] →^* i5816[7])∧(java.lang.Object(ARRAY(i4[5], a115115data[5])) →^* java.lang.Object(ARRAY(i4[7], a115115data[7])))∧(i5824[5] + -1 →^* i5824[7]))

(5) -> (10), if ((java.lang.Object(ARRAY(i4[5], a115115data[5])) →^* java.lang.Object(ARRAY(i4[10], a115115data[10])))∧(i5816[5] →^* i5816[10])∧(i5824[5] + -1 →^* i5824[10]))

(5) -> (14), if ((java.lang.Object(ARRAY(i4[5], a115115data[5])) →^* java.lang.Object(ARRAY(i4[14], a115115data[14])))∧(i5824[5] + -1 →^* i5824[14])∧(i5816[5] →^* i5816[14]))

(5) -> (17), if ((java.lang.Object(ARRAY(i4[5], a115115data[5])) →^* java.lang.Object(ARRAY(i4[17], a115115data[17])))∧(i5824[5] + -1 →^* i5824[17])∧(i5816[5] →^* i5816[17]))

(5) -> (20), if ((i5816[5] →^* i5816[20])∧(i5824[5] + -1 →^* i5824[20])∧(java.lang.Object(ARRAY(i4[5], a115115data[5])) →^* java.lang.Object(ARRAY(i4[20], a115115data[20]))))

(5) -> (23), if ((i5824[5] + -1 →^* i5824[23])∧(i5816[5] →^* i5816[23])∧(java.lang.Object(ARRAY(i4[5], a115115data[5])) →^* java.lang.Object(ARRAY(i4[23], a115115data[23]))))

(5) -> (26), if ((i5824[5] + -1 →^* i5824[26])∧(i5816[5] →^* i5816[26])∧(java.lang.Object(ARRAY(i4[5], a115115data[5])) →^* java.lang.Object(ARRAY(i4[26], a115115data[26]))))

(6) -> (3), if ((i5824[6] →^* i5824[3])∧(i6609[6] →^* i5816[3])∧(java.lang.Object(ARRAY(i4[6], a115115data[6])) →^* java.lang.Object(ARRAY(i4[3], a115115data[3]))))

(7) -> (8), if ((i5824[7] →^* i5824[8])∧(java.lang.Object(ARRAY(i4[7], a115115data[7])) →^* java.lang.Object(ARRAY(i4[8], a115115data[8])))∧(i5816[7] →^* i5816[8]))

(8) -> (9), if ((i5816[8] + 1 > 0 && i5816[8] + 1 < i4[8] && i5816[8] > 0 && i5816[8] < i4[8] && i5824[8] > 0 && i5816[8] + 1 + 1 > 0 →^* TRUE)∧(i5816[8] →^* i5816[9])∧(i5824[8] →^* i5824[9])∧(java.lang.Object(ARRAY(i4[8], a115115data[8])) →^* java.lang.Object(ARRAY(i4[9], a115115data[9]))))

(9) -> (3), if ((java.lang.Object(ARRAY(i4[9], a115115data[9])) →^* java.lang.Object(ARRAY(i4[3], a115115data[3])))∧(i5816[9] + 1 + 1 →^* i5816[3])∧(i5824[9] →^* i5824[3]))

(10) -> (11), if ((java.lang.Object(java.lang.String(i6986[10])) →^* java.lang.Object(java.lang.String(i6986[11])))∧(java.lang.Object(ARRAY(i4[10], a115115data[10])) →^* java.lang.Object(ARRAY(i4[11], a115115data[11])))∧(i5816[10] →^* i5816[11])∧(i5824[10] →^* i5824[11]))

(11) -> (12), if ((i5824[11] →^* i5824[12])∧(i5816[11] →^* i5816[12])∧(java.lang.Object(ARRAY(i4[11], a115115data[11])) →^* java.lang.Object(ARRAY(i4[12], a115115data[12])))∧(java.lang.Object(java.lang.String(i6986[11])) →^* java.lang.Object(java.lang.String(i6986[12])))∧(!(i6986[11] = 0) && i5816[11] + 1 > 0 && i5816[11] + 1 < i4[11] && i5816[11] > 0 && i5816[11] < i4[11] && i5824[11] > 0 && i5816[11] + 1 + 1 > 0 →^* TRUE))

(12) -> (3), if ((i5824[12] →^* i5824[3])∧(i5816[12] + 1 + 1 →^* i5816[3])∧(java.lang.Object(ARRAY(i4[12], a115115data[12])) →^* java.lang.Object(ARRAY(i4[3], a115115data[3]))))

(13) -> (3), if ((java.lang.Object(ARRAY(i4[13], a115115data[13])) →^* java.lang.Object(ARRAY(i4[3], a115115data[3])))∧(i6905[13] →^* i5816[3])∧(i5824[13] →^* i5824[3]))

(14) -> (15), if ((i5824[14] →^* i5824[15])∧(i5816[14] →^* i5816[15])∧(java.lang.Object(java.lang.String(i6164[14])) →^* java.lang.Object(java.lang.String(i6164[15])))∧(java.lang.Object(ARRAY(i4[14], a115115data[14])) →^* java.lang.Object(ARRAY(i4[15], a115115data[15]))))

(15) -> (16), if ((i5816[15] →^* i5816[16])∧(i5824[15] →^* i5824[16])∧(i5816[15] + 1 > 0 && i5816[15] + 1 < i4[15] && !(i6164[15] = 0) && i5816[15] > 0 && i5816[15] < i4[15] && i5824[15] > 0 && i5816[15] + 1 + 1 > 0 →^* TRUE)∧(java.lang.Object(ARRAY(i4[15], a115115data[15])) →^* java.lang.Object(ARRAY(i4[16], a115115data[16])))∧(java.lang.Object(java.lang.String(i6164[15])) →^* java.lang.Object(java.lang.String(i6164[16]))))

(16) -> (3), if ((i5824[16] →^* i5824[3])∧(i5816[16] + 1 + 1 →^* i5816[3])∧(java.lang.Object(ARRAY(i4[16], a115115data[16])) →^* java.lang.Object(ARRAY(i4[3], a115115data[3]))))

(17) -> (18), if ((java.lang.Object(java.lang.String(i6164[17])) →^* java.lang.Object(java.lang.String(i6164[18])))∧(i5824[17] →^* i5824[18])∧(java.lang.Object(java.lang.String(i7504[17])) →^* java.lang.Object(java.lang.String(i7504[18])))∧(java.lang.Object(ARRAY(i4[17], a115115data[17])) →^* java.lang.Object(ARRAY(i4[18], a115115data[18])))∧(i5816[17] →^* i5816[18]))

(18) -> (19), if ((java.lang.Object(java.lang.String(i6164[18])) →^* java.lang.Object(java.lang.String(i6164[19])))∧(java.lang.Object(java.lang.String(i7504[18])) →^* java.lang.Object(java.lang.String(i7504[19])))∧(!(i7504[18] = 0) && i5816[18] + 1 > 0 && i5816[18] + 1 < i4[18] && !(i6164[18] = 0) && i5816[18] > 0 && i5816[18] < i4[18] && i5824[18] > 0 && i5816[18] + 1 + 1 > 0 →^* TRUE)∧(java.lang.Object(ARRAY(i4[18], a115115data[18])) →^* java.lang.Object(ARRAY(i4[19], a115115data[19])))∧(i5816[18] →^* i5816[19])∧(i5824[18] →^* i5824[19]))

(19) -> (3), if ((i5816[19] + 1 + 1 →^* i5816[3])∧(i5824[19] →^* i5824[3])∧(java.lang.Object(ARRAY(i4[19], a115115data[19])) →^* java.lang.Object(ARRAY(i4[3], a115115data[3]))))

(20) -> (21), if ((java.lang.Object(java.lang.String(i6986[20])) →^* java.lang.Object(java.lang.String(i6986[21])))∧(i5816[20] →^* i5816[21])∧(java.lang.Object(ARRAY(i4[20], a115115data[20])) →^* java.lang.Object(ARRAY(i4[21], a115115data[21])))∧(i5824[20] →^* i5824[21]))

(21) -> (22), if ((java.lang.Object(ARRAY(i4[21], a115115data[21])) →^* java.lang.Object(ARRAY(i4[22], a115115data[22])))∧(java.lang.Object(java.lang.String(i6986[21])) →^* java.lang.Object(java.lang.String(i6986[22])))∧(!(i6986[21] = 0) && i5816[21] + 1 > 0 && i5816[21] + 1 < i4[21] && i5816[21] > 0 && i5816[21] < i4[21] && i5824[21] > 0 && i5816[21] + 1 + 1 > 0 →^* TRUE)∧(i5816[21] →^* i5816[22])∧(i5824[21] →^* i5824[22]))

(22) -> (6), if ((i5816[22] + 1 + 1 →^* i6609[6])∧(java.lang.Object(ARRAY(i4[22], a115115data[22])) →^* java.lang.Object(ARRAY(i4[6], a115115data[6])))∧(i5824[22] →^* i5824[6]))

(23) -> (24), if ((java.lang.Object(java.lang.String(i6164[23])) →^* java.lang.Object(java.lang.String(i6164[24])))∧(i5816[23] →^* i5816[24])∧(java.lang.Object(ARRAY(i4[23], a115115data[23])) →^* java.lang.Object(ARRAY(i4[24], a115115data[24])))∧(i5824[23] →^* i5824[24]))

(24) -> (25), if ((java.lang.Object(ARRAY(i4[24], a115115data[24])) →^* java.lang.Object(ARRAY(i4[25], a115115data[25])))∧(i5816[24] + 1 > 0 && i5816[24] + 1 < i4[24] && !(i6164[24] = 0) && i5816[24] > 0 && i5816[24] < i4[24] && i5824[24] > 0 && i5816[24] + 1 + 1 > 0 →^* TRUE)∧(java.lang.Object(java.lang.String(i6164[24])) →^* java.lang.Object(java.lang.String(i6164[25])))∧(i5816[24] →^* i5816[25])∧(i5824[24] →^* i5824[25]))

(25) -> (13), if ((i5824[25] →^* i5824[13])∧(java.lang.Object(ARRAY(i4[25], a115115data[25])) →^* java.lang.Object(ARRAY(i4[13], a115115data[13])))∧(i5816[25] + 1 + 1 →^* i6905[13]))

(26) -> (27), if ((java.lang.Object(java.lang.String(i7504[26])) →^* java.lang.Object(java.lang.String(i7504[27])))∧(java.lang.Object(ARRAY(i4[26], a115115data[26])) →^* java.lang.Object(ARRAY(i4[27], a115115data[27])))∧(java.lang.Object(java.lang.String(i6164[26])) →^* java.lang.Object(java.lang.String(i6164[27])))∧(i5824[26] →^* i5824[27])∧(i5816[26] →^* i5816[27]))

(27) -> (28), if ((i5824[27] →^* i5824[28])∧(!(i7504[27] = 0) && i5816[27] + 1 > 0 && i5816[27] + 1 < i4[27] && !(i6164[27] = 0) && i5816[27] > 0 && i5816[27] < i4[27] && i5824[27] > 0 && i5816[27] + 1 + 1 > 0 →^* TRUE)∧(java.lang.Object(java.lang.String(i7504[27])) →^* java.lang.Object(java.lang.String(i7504[28])))∧(java.lang.Object(java.lang.String(i6164[27])) →^* java.lang.Object(java.lang.String(i6164[28])))∧(i5816[27] →^* i5816[28])∧(java.lang.Object(ARRAY(i4[27], a115115data[27])) →^* java.lang.Object(ARRAY(i4[28], a115115data[28]))))

(28) -> (13), if ((i5824[28] →^* i5824[13])∧(i5816[28] + 1 + 1 →^* i6905[13])∧(java.lang.Object(ARRAY(i4[28], a115115data[28])) →^* java.lang.Object(ARRAY(i4[13], a115115data[13]))))

The set Q consists of the following terms:
Load34990(java.lang.Object(ARRAY(x0, x1)), x2, x3)
Load34990ARR3(java.lang.Object(ARRAY(x0, x1)), x2, x3)
Cond_Load34990ARR3(TRUE, java.lang.Object(ARRAY(x0, x1)), x2, x3)
Inc35127(java.lang.Object(ARRAY(x0, x1)), x2, x3)
Cond_Load34990(TRUE, java.lang.Object(ARRAY(x0, x1)), x2, x3)
New39186(java.lang.Object(ARRAY(x0, x1)), x2, x3)
Load34990ARR4(java.lang.Object(ARRAY(x0, x1)), x2, x3)
Cond_Load34990ARR4(TRUE, java.lang.Object(ARRAY(x0, x1)), x2, x3)
Load34990ARR5(java.lang.Object(ARRAY(x0, x1)), x2, x3, java.lang.Object(java.lang.String(x4)))
Cond_Load34990ARR5(TRUE, java.lang.Object(ARRAY(x0, x1)), x2, x3, java.lang.Object(java.lang.String(x4)))
New40288(java.lang.Object(ARRAY(x0, x1)), x2, x3)
Load34990ARR6(java.lang.Object(ARRAY(x0, x1)), x2, x3, java.lang.Object(java.lang.String(x4)))
Cond_Load34990ARR6(TRUE, java.lang.Object(ARRAY(x0, x1)), x2, x3, java.lang.Object(java.lang.String(x4)))
Load34990ARR7(java.lang.Object(ARRAY(x0, x1)), x2, x3, java.lang.Object(java.lang.String(x4)), java.lang.Object(java.lang.String(x5)))
Cond_Load34990ARR7(TRUE, java.lang.Object(ARRAY(x0, x1)), x2, x3, java.lang.Object(java.lang.String(x4)), java.lang.Object(java.lang.String(x5)))
Load34990ARR8(java.lang.Object(ARRAY(x0, x1)), x2, x3, java.lang.Object(java.lang.String(x4)))
Cond_Load34990ARR8(TRUE, java.lang.Object(ARRAY(x0, x1)), x2, x3, java.lang.Object(java.lang.String(x4)))
Load34990ARR9(java.lang.Object(ARRAY(x0, x1)), x2, x3, java.lang.Object(java.lang.String(x4)))
Cond_Load34990ARR9(TRUE, java.lang.Object(ARRAY(x0, x1)), x2, x3, java.lang.Object(java.lang.String(x4)))
Load34990ARR10(java.lang.Object(ARRAY(x0, x1)), x2, x3, java.lang.Object(java.lang.String(x4)), java.lang.Object(java.lang.String(x5)))
Cond_Load34990ARR10(TRUE, java.lang.Object(ARRAY(x0, x1)), x2, x3, java.lang.Object(java.lang.String(x4)), java.lang.Object(java.lang.String(x5)))

(29) UsableRulesProof (EQUIVALENT transformation)

As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [LPAR04] we can delete all non-usable rules [FROCOS05] from R.

(30) 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): LOAD34990(java.lang.Object(ARRAY(i4[0], a115115data[0])), i5816[0], i5824[0]) → LOAD34990ARR3(java.lang.Object(ARRAY(i4[0], a115115data[0])), i5816[0], i5824[0])
(1): LOAD34990ARR3(java.lang.Object(ARRAY(i4[1], a115115data[1])), i5816[1], i5824[1]) → COND_LOAD34990ARR3(i5816[1] + 1 > 0 && i5816[1] + 1 < i4[1] && i5816[1] > 0 && i5816[1] < i4[1] && i5824[1] > 0 && i5816[1] + 1 + 1 > 0, java.lang.Object(ARRAY(i4[1], a115115data[1])), i5816[1], i5824[1])
(2): COND_LOAD34990ARR3(TRUE, java.lang.Object(ARRAY(i4[2], a115115data[2])), i5816[2], i5824[2]) → NEW39186(java.lang.Object(ARRAY(i4[2], a115115data[2])), i5816[2] + 1 + 1, i5824[2])
(3): INC35127(java.lang.Object(ARRAY(i4[3], a115115data[3])), i5816[3], i5824[3]) → LOAD34990(java.lang.Object(ARRAY(i4[3], a115115data[3])), i5816[3], i5824[3] + -1)
(4): LOAD34990(java.lang.Object(ARRAY(i4[4], a115115data[4])), i5816[4], i5824[4]) → COND_LOAD34990(i5824[4] > 0, java.lang.Object(ARRAY(i4[4], a115115data[4])), i5816[4], i5824[4])
(5): COND_LOAD34990(TRUE, java.lang.Object(ARRAY(i4[5], a115115data[5])), i5816[5], i5824[5]) → LOAD34990(java.lang.Object(ARRAY(i4[5], a115115data[5])), i5816[5], i5824[5] + -1)
(6): NEW39186(java.lang.Object(ARRAY(i4[6], a115115data[6])), i6609[6], i5824[6]) → INC35127(java.lang.Object(ARRAY(i4[6], a115115data[6])), i6609[6], i5824[6])
(7): LOAD34990(java.lang.Object(ARRAY(i4[7], a115115data[7])), i5816[7], i5824[7]) → LOAD34990ARR4(java.lang.Object(ARRAY(i4[7], a115115data[7])), i5816[7], i5824[7])
(8): LOAD34990ARR4(java.lang.Object(ARRAY(i4[8], a115115data[8])), i5816[8], i5824[8]) → COND_LOAD34990ARR4(i5816[8] + 1 > 0 && i5816[8] + 1 < i4[8] && i5816[8] > 0 && i5816[8] < i4[8] && i5824[8] > 0 && i5816[8] + 1 + 1 > 0, java.lang.Object(ARRAY(i4[8], a115115data[8])), i5816[8], i5824[8])
(9): COND_LOAD34990ARR4(TRUE, java.lang.Object(ARRAY(i4[9], a115115data[9])), i5816[9], i5824[9]) → INC35127(java.lang.Object(ARRAY(i4[9], a115115data[9])), i5816[9] + 1 + 1, i5824[9])
(10): LOAD34990(java.lang.Object(ARRAY(i4[10], a115115data[10])), i5816[10], i5824[10]) → LOAD34990ARR5(java.lang.Object(ARRAY(i4[10], a115115data[10])), i5816[10], i5824[10], java.lang.Object(java.lang.String(i6986[10])))
(11): LOAD34990ARR5(java.lang.Object(ARRAY(i4[11], a115115data[11])), i5816[11], i5824[11], java.lang.Object(java.lang.String(i6986[11]))) → COND_LOAD34990ARR5(!(i6986[11] = 0) && i5816[11] + 1 > 0 && i5816[11] + 1 < i4[11] && i5816[11] > 0 && i5816[11] < i4[11] && i5824[11] > 0 && i5816[11] + 1 + 1 > 0, java.lang.Object(ARRAY(i4[11], a115115data[11])), i5816[11], i5824[11], java.lang.Object(java.lang.String(i6986[11])))
(12): COND_LOAD34990ARR5(TRUE, java.lang.Object(ARRAY(i4[12], a115115data[12])), i5816[12], i5824[12], java.lang.Object(java.lang.String(i6986[12]))) → INC35127(java.lang.Object(ARRAY(i4[12], a115115data[12])), i5816[12] + 1 + 1, i5824[12])
(13): NEW40288(java.lang.Object(ARRAY(i4[13], a115115data[13])), i6905[13], i5824[13]) → INC35127(java.lang.Object(ARRAY(i4[13], a115115data[13])), i6905[13], i5824[13])
(14): LOAD34990(java.lang.Object(ARRAY(i4[14], a115115data[14])), i5816[14], i5824[14]) → LOAD34990ARR6(java.lang.Object(ARRAY(i4[14], a115115data[14])), i5816[14], i5824[14], java.lang.Object(java.lang.String(i6164[14])))
(15): LOAD34990ARR6(java.lang.Object(ARRAY(i4[15], a115115data[15])), i5816[15], i5824[15], java.lang.Object(java.lang.String(i6164[15]))) → COND_LOAD34990ARR6(i5816[15] + 1 > 0 && i5816[15] + 1 < i4[15] && !(i6164[15] = 0) && i5816[15] > 0 && i5816[15] < i4[15] && i5824[15] > 0 && i5816[15] + 1 + 1 > 0, java.lang.Object(ARRAY(i4[15], a115115data[15])), i5816[15], i5824[15], java.lang.Object(java.lang.String(i6164[15])))
(16): COND_LOAD34990ARR6(TRUE, java.lang.Object(ARRAY(i4[16], a115115data[16])), i5816[16], i5824[16], java.lang.Object(java.lang.String(i6164[16]))) → INC35127(java.lang.Object(ARRAY(i4[16], a115115data[16])), i5816[16] + 1 + 1, i5824[16])
(17): LOAD34990(java.lang.Object(ARRAY(i4[17], a115115data[17])), i5816[17], i5824[17]) → LOAD34990ARR7(java.lang.Object(ARRAY(i4[17], a115115data[17])), i5816[17], i5824[17], java.lang.Object(java.lang.String(i7504[17])), java.lang.Object(java.lang.String(i6164[17])))
(18): LOAD34990ARR7(java.lang.Object(ARRAY(i4[18], a115115data[18])), i5816[18], i5824[18], java.lang.Object(java.lang.String(i7504[18])), java.lang.Object(java.lang.String(i6164[18]))) → COND_LOAD34990ARR7(!(i7504[18] = 0) && i5816[18] + 1 > 0 && i5816[18] + 1 < i4[18] && !(i6164[18] = 0) && i5816[18] > 0 && i5816[18] < i4[18] && i5824[18] > 0 && i5816[18] + 1 + 1 > 0, java.lang.Object(ARRAY(i4[18], a115115data[18])), i5816[18], i5824[18], java.lang.Object(java.lang.String(i7504[18])), java.lang.Object(java.lang.String(i6164[18])))
(19): COND_LOAD34990ARR7(TRUE, java.lang.Object(ARRAY(i4[19], a115115data[19])), i5816[19], i5824[19], java.lang.Object(java.lang.String(i7504[19])), java.lang.Object(java.lang.String(i6164[19]))) → INC35127(java.lang.Object(ARRAY(i4[19], a115115data[19])), i5816[19] + 1 + 1, i5824[19])
(20): LOAD34990(java.lang.Object(ARRAY(i4[20], a115115data[20])), i5816[20], i5824[20]) → LOAD34990ARR8(java.lang.Object(ARRAY(i4[20], a115115data[20])), i5816[20], i5824[20], java.lang.Object(java.lang.String(i6986[20])))
(21): LOAD34990ARR8(java.lang.Object(ARRAY(i4[21], a115115data[21])), i5816[21], i5824[21], java.lang.Object(java.lang.String(i6986[21]))) → COND_LOAD34990ARR8(!(i6986[21] = 0) && i5816[21] + 1 > 0 && i5816[21] + 1 < i4[21] && i5816[21] > 0 && i5816[21] < i4[21] && i5824[21] > 0 && i5816[21] + 1 + 1 > 0, java.lang.Object(ARRAY(i4[21], a115115data[21])), i5816[21], i5824[21], java.lang.Object(java.lang.String(i6986[21])))
(22): COND_LOAD34990ARR8(TRUE, java.lang.Object(ARRAY(i4[22], a115115data[22])), i5816[22], i5824[22], java.lang.Object(java.lang.String(i6986[22]))) → NEW39186(java.lang.Object(ARRAY(i4[22], a115115data[22])), i5816[22] + 1 + 1, i5824[22])
(23): LOAD34990(java.lang.Object(ARRAY(i4[23], a115115data[23])), i5816[23], i5824[23]) → LOAD34990ARR9(java.lang.Object(ARRAY(i4[23], a115115data[23])), i5816[23], i5824[23], java.lang.Object(java.lang.String(i6164[23])))
(24): LOAD34990ARR9(java.lang.Object(ARRAY(i4[24], a115115data[24])), i5816[24], i5824[24], java.lang.Object(java.lang.String(i6164[24]))) → COND_LOAD34990ARR9(i5816[24] + 1 > 0 && i5816[24] + 1 < i4[24] && !(i6164[24] = 0) && i5816[24] > 0 && i5816[24] < i4[24] && i5824[24] > 0 && i5816[24] + 1 + 1 > 0, java.lang.Object(ARRAY(i4[24], a115115data[24])), i5816[24], i5824[24], java.lang.Object(java.lang.String(i6164[24])))
(25): COND_LOAD34990ARR9(TRUE, java.lang.Object(ARRAY(i4[25], a115115data[25])), i5816[25], i5824[25], java.lang.Object(java.lang.String(i6164[25]))) → NEW40288(java.lang.Object(ARRAY(i4[25], a115115data[25])), i5816[25] + 1 + 1, i5824[25])
(26): LOAD34990(java.lang.Object(ARRAY(i4[26], a115115data[26])), i5816[26], i5824[26]) → LOAD34990ARR10(java.lang.Object(ARRAY(i4[26], a115115data[26])), i5816[26], i5824[26], java.lang.Object(java.lang.String(i7504[26])), java.lang.Object(java.lang.String(i6164[26])))
(27): LOAD34990ARR10(java.lang.Object(ARRAY(i4[27], a115115data[27])), i5816[27], i5824[27], java.lang.Object(java.lang.String(i7504[27])), java.lang.Object(java.lang.String(i6164[27]))) → COND_LOAD34990ARR10(!(i7504[27] = 0) && i5816[27] + 1 > 0 && i5816[27] + 1 < i4[27] && !(i6164[27] = 0) && i5816[27] > 0 && i5816[27] < i4[27] && i5824[27] > 0 && i5816[27] + 1 + 1 > 0, java.lang.Object(ARRAY(i4[27], a115115data[27])), i5816[27], i5824[27], java.lang.Object(java.lang.String(i7504[27])), java.lang.Object(java.lang.String(i6164[27])))
(28): COND_LOAD34990ARR10(TRUE, java.lang.Object(ARRAY(i4[28], a115115data[28])), i5816[28], i5824[28], java.lang.Object(java.lang.String(i7504[28])), java.lang.Object(java.lang.String(i6164[28]))) → NEW40288(java.lang.Object(ARRAY(i4[28], a115115data[28])), i5816[28] + 1 + 1, i5824[28])