time complexity proof of /tmp/tmp495IXC/Test2.jar

The time complexity of the given JBC problem could be proven to be BOUNDS(CONSTANT, 39353 + 561 * |#0|).

0 JBC problem

↳1 JBCToGraph (BOTH CONCRETE BOUNDS(ID, ID), 1011 ms)

↳2 JBCTerminationGraph

↳3 TerminationGraphToComplexityProof (BOTH CONCRETE BOUNDS(ID, ADD(3)), 0 ms)

↳4 JBCComplexityEdges

    ↳5 JBCGraphEdgesToCpxIntTrsProof (CONCRETE UPPER BOUND(ID), 120 ms)

    ↳6 WeightedIntTrs

        ↳7 StraightLineCodeCompressionProof (BOTH CONCRETE BOUNDS(ID, ID), 65 ms)

        ↳8 WeightedIntTrs

        ↳9 MovedArithmeticFromConstraintsProof (BOTH CONCRETE BOUNDS(ID, ID), 0 ms)

        ↳10 WeightedIntTrs

        ↳11 ExpressionSimplificationProof (BOTH CONCRETE BOUNDS(ID, ID), 3 ms)

        ↳12 WeightedIntTrs

    ↳13 JBCGraphEdgesToCpxIntTrsProof (CONCRETE UPPER BOUND(ID), 127 ms)

    ↳14 WeightedIntTrs

        ↳15 StraightLineCodeCompressionProof (BOTH CONCRETE BOUNDS(ID, ID), 53 ms)

        ↳16 WeightedIntTrs

        ↳17 RemoveDivModProof (CONCRETE UPPER BOUND(ID), 0 ms)

        ↳18 WeightedIntTrs

        ↳19 MovedArithmeticFromConstraintsProof (BOTH CONCRETE BOUNDS(ID, ID), 0 ms)

        ↳20 WeightedIntTrs

        ↳21 ExpressionSimplificationProof (BOTH CONCRETE BOUNDS(ID, ID), 1 ms)

        ↳22 WeightedIntTrs

↳23 TerminationGraphToComplexityProof (BOTH CONCRETE BOUNDS(ID, ADD(3)), 0 ms)

↳24 JBCComplexityEdges

    ↳25 JBCGraphEdgesToCpxIntTrsProof (CONCRETE UPPER BOUND(ID), 155 ms)

    ↳26 WeightedIntTrs

    ↳27 StraightLineCodeCompressionProof (BOTH CONCRETE BOUNDS(ID, ID), 65 ms)

    ↳28 WeightedIntTrs

    ↳29 WeightedIntTrsUnneededArgumentFilterProof (CONCRETE UPPER BOUND(ID), 40 ms)

    ↳30 WeightedIntTrs

    ↳31 MovedArithmeticFromConstraintsProof (BOTH CONCRETE BOUNDS(ID, ID), 0 ms)

    ↳32 WeightedIntTrs

    ↳33 ExpressionSimplificationProof (BOTH CONCRETE BOUNDS(ID, ID), 0 ms)

    ↳34 WeightedIntTrs

    ↳35 koat Proof (⇔, 1074 ms)

    ↳36 BOUNDS(CONSTANT, 39350 + 561 * |#0|)

(0) Obligation:

Need to prove time_complexity of the following program:

public class Test2 {
    public static void main(String[] args) {
	iter(args.length, args.length % 5, args.length % 4);
    }

    private static void iter(int x, int y, int z) {
	while (x + y + 3 * z >= 0) {
	    if (x > y)
		x--;
	    else if (y > z) {
		x++;
		y -= 2;
	    }
	    else if (y <= z) {
		x = add(x, 1);
		y = add(y, 1);
		z = z - 1;
	    }
	}
    }

    private static int add(int v, int w) {
	return v + w;
    }
}

(1) JBCToGraph (BOTH CONCRETE BOUNDS(ID, ID) transformation)

Constructed TerminationGraph.

(2) Obligation:

Termination Graph based on JBC Program:
Test2.main([Ljava/lang/String;)V: Graph of 101 nodes with 1 SCC.

(3) TerminationGraphToComplexityProof (BOTH CONCRETE BOUNDS(ID, ADD(3)) transformation)

Extracted set of 100 edges for the analysis of TIME complexity. Kept leaves.

(4) Obligation:

Set of 100 edges based on JBC Program.
Performed SCC analyses:

Used field analysis yielded the following read fields:

Considered paths: nonterm paths and paths from start to sinks

(5) JBCGraphEdgesToCpxIntTrsProof (CONCRETE UPPER BOUND(ID) transformation)

Transformed 100 jbc graph edges to a weighted ITS with 100 rules.
Used simplified encoding of division and modulo.
Filtered conditions with variables that do not depend on the variables on the lhs or rhs without taking transitive dependencies into account.
Did no encode lower bounds for putfield and astore.

(6) Obligation:

IntTrs with 100 rules
Start term: main_Load_1(#0, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_Load_1(o1, env, static) -{0,0}> main_Load_3(o1, env, static) :|: 0 < o1
main_Load_3(o1, env, static) -{0,0}> langle_clinit_rangle_ConstantStackPush_5(o1, env, static) :|: 0 < o1
langle_clinit_rangle_ConstantStackPush_5(o1, env, static) -{1,1}> langle_clinit_rangle_ArrayCreate_9(iconst_0, o1, env, static) :|: iconst_0 = 0 && 0 < o1
langle_clinit_rangle_ArrayCreate_9(iconst_0, o1, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_10(a2, o1, iconst_0, env, static) :|: a2 = 2 && iconst_0 = 0 && 0 < a2 && 0 < o1
langle_clinit_rangle_FieldAccess_10(a2, o1, iconst_0, env, static) -{1,1}> langle_clinit_rangle_New_13(o1, env, static') :|: 0 <= a2 && iconst_0 = 0 && static' <= static + a2 && 0 <= static && 0 < a2 && 0 < o1
langle_clinit_rangle_New_13(o1, env, static) -{0,0}> langle_clinit_rangle_New_15(o1, env, static) :|: 0 < o1
langle_clinit_rangle_New_15(o1, env, static) -{0,0}> langle_clinit_rangle_New_16(o1, env, static) :|: 0 <= static && 0 < o1
langle_clinit_rangle_New_16(o1, env, static) -{1,1}> langle_clinit_rangle_Duplicate_18(o4, o1, env, static) :|: o4 = 1 && 0 < o4 && 0 < o1
langle_clinit_rangle_Duplicate_18(o4, o1, env, static) -{1,1}> langle_clinit_rangle_ConstantStackPush_20(o4, o1, env, static) :|: 0 < o4 && 0 < o1
langle_clinit_rangle_ConstantStackPush_20(o4, o1, env, static) -{1,1}> langle_clinit_rangle_InvokeMethod_22(o4, NULL, o1, env, static) :|: NULL = 0 && 0 < o4 && 0 < o1
langle_clinit_rangle_InvokeMethod_22(o4, NULL, o1, env, static) -{1,1}> langle_init_rangle_Load_24(o4, o1, env, static) :|: NULL = 0 && 0 < o4 && 0 < o1
langle_init_rangle_Load_24(o4, o1, env, static) -{1,1}> langle_init_rangle_InvokeMethod_25(o4, o1, env, static) :|: 0 < o4 && 0 < o1
langle_init_rangle_InvokeMethod_25(o4, o1, env, static) -{1,1}> langle_init_rangle_Load_27(o4, o1, env, static) :|: 0 < o4 && 0 < o1
langle_init_rangle_Load_27(o4, o1, env, static) -{1,1}> langle_init_rangle_InvokeMethod_30(o4, o1, env, static) :|: 0 < o4 && 0 < o1
langle_init_rangle_InvokeMethod_30(o4, o1, env, static) -{1,1}> langle_init_rangle_Return_32(o4, o1, env, static) :|: 0 < o4 && 0 < o1
langle_init_rangle_Return_32(o4, o1, env, static) -{1,1}> langle_init_rangle_Return_35(o4, o1, env, static) :|: 0 < o4 && 0 < o1
langle_init_rangle_Return_35(o4, o1, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_37(o4, o1, env, static) :|: 0 < o4 && 0 < o1
langle_clinit_rangle_FieldAccess_37(o4, o1, env, static) -{1,1}> langle_clinit_rangle_Return_40(o1, env, static') :|: 0 <= o4 && 0 < o4 && 0 <= static && 0 < o1 && static' <= static + o4
langle_clinit_rangle_Return_40(o1, env, static) -{1,1}> main_Load_41(o1, env, static) :|: 0 < o1
main_Load_41(o1, env, static) -{0,0}> main_Load_42(o1, env, static) :|: 0 < o1
main_Load_42(o1, env, static) -{0,0}> main_Load_43(o1, env, static) :|: 0 <= static && 0 < o1
main_Load_43(o1, env, static) -{0,0}> main_Load_45(o1, env, static) :|: 0 < o1
main_Load_45(o1, env, static) -{0,0}> main_Load_47(o1, env, static) :|: 0 < o1
main_Load_47(o1, env, static) -{1,1}> main_ArrayLength_51(o1, env, static) :|: 0 < o1
main_ArrayLength_51(a6, env, static) -{0,0}> main_ArrayLength_52(a6, i4, env, static) :|: 0 <= i4 && 0 < a6 && i4 < a6
main_ArrayLength_52(a6, i4, env, static) -{1,1}> main_Load_54(a6, i4, env, static) :|: 0 <= i4 && 0 < a6
main_Load_54(a6, i4, env, static) -{1,1}> main_ArrayLength_56(a6, i4, env, static) :|: 0 <= i4 && 0 < a6
main_ArrayLength_56(a6, i4, env, static) -{1,1}> main_ConstantStackPush_58(a6, i4, env, static) :|: 0 <= i4 && 0 < a6
main_ConstantStackPush_58(a6, i4, env, static) -{1,1}> main_IntArithmetic_60(a6, i4, iconst_5, env, static) :|: iconst_5 = 5 && 0 <= i4 && 0 < a6
main_IntArithmetic_60(a6, i4, iconst_5, env, static) -{1,1}> main_Load_62(a6, i4, i6, env, static) :|: 0 <= i6 && iconst_5 = 5 && i6 < iconst_5 && 0 <= i4 && i6 <= 4 && 0 < a6
main_Load_62(a6, i4, i6, env, static) -{1,1}> main_ArrayLength_64(a6, i4, i6, env, static) :|: 0 <= i6 && 0 <= i4 && i6 <= 4 && 0 < a6
main_ArrayLength_64(a6, i4, i6, env, static) -{1,1}> main_ConstantStackPush_66(a6, i4, i6, env, static) :|: 0 <= i6 && 0 <= i4 && i6 <= 4 && 0 < a6
main_ConstantStackPush_66(a6, i4, i6, env, static) -{1,1}> main_IntArithmetic_68(a6, i4, i6, iconst_4, env, static) :|: 0 <= i6 && iconst_4 = 4 && 0 <= i4 && i6 <= 4 && 0 < a6
main_IntArithmetic_68(a6, i4, i6, iconst_4, env, static) -{1,1}> main_InvokeMethod_70(a6, i4, i6, i8, env, static) :|: 0 <= i6 && i8 <= 3 && i8 < iconst_4 && iconst_4 = 4 && 0 <= i4 && i6 <= 4 && 0 < a6 && 0 <= i8
main_InvokeMethod_70(a6, i4, i6, i8, env, static) -{1,1}> iter_Load_72(i4, i6, i8, a6, env, static) :|: 0 <= i6 && i8 <= 3 && 0 <= i4 && i6 <= 4 && 0 < a6 && 0 <= i8
iter_Load_72(i4, i6, i8, a6, env, static) -{0,0}> iter_Load_577(i4, i6, i8, a6, i4, env, static) :|: 0 <= i6 && i8 <= 3 && -1 <= i6 && 0 <= i4 && -1 <= i4 && i6 <= 4 && 0 < a6 && 0 <= i8
iter_Load_577(i249, i250, i8, a110, i69, env, static) -{0,0}> iter_Load_710(i249, i250, i8, a110, i69, env, static) :|: i8 <= 3 && 0 < a110 && -1 <= i250 && -1 <= i249 && -1 <= i8 && 0 <= i8 && 0 <= i69
iter_Load_710(i301, i302, i303, a131, i69, env, static) -{0,0}> iter_Load_762(i301, i302, i303, a131, i69, env, static) :|: i303 <= 3 && -1 <= i302 && -2 <= i302 && 0 <= i69 && -1 <= i303 && -1 <= i301 && 0 < a131
iter_Load_762(i326, i327, i303, a139, i69, env, static) -{0,0}> iter_Load_796(i326, i327, i303, a139, i69, env, static) :|: -1 <= i326 && i303 <= 3 && 0 <= i69 && -1 <= i303 && -2 <= i327 && 0 < a139
iter_Load_796(i342, i327, i303, a145, i69, env, static) -{0,0}> iter_Load_899(i342, i327, i303, a145, i69, env, static) :|: i303 <= 3 && -2 <= i303 && 0 < a145 && 0 <= i69 && -1 <= i303 && -2 <= i327
iter_Load_899(i380, i381, i382, a164, i69, env, static) -{0,0}> iter_Load_1043(i380, i381, i382, a164, i69, env, static) :|: -2 <= i381 && i382 <= 3 && 0 < a164 && -2 <= i382 && 0 <= i69
iter_Load_1043(i426, i427, i382, a176, i69, env, static) -{0,0}> iter_Load_1320(i426, i427, i382, a176, i69, env, static) :|: 0 < a176 && i382 <= 3 && -2 <= i382 && 0 <= i69
iter_Load_1320(i522, i523, i524, a208, i69, env, static) -{1,1}> iter_Load_1321(i522, i523, i524, a208, i69, env, static) :|: 0 <= i69 && 0 < a208
iter_Load_1321(i522, i523, i524, a208, i69, env, static) -{1,1}> iter_IntArithmetic_1324(i522, i523, i524, a208, i69, env, static) :|: 0 <= i69 && 0 < a208
iter_IntArithmetic_1324(i522, i523, i524, a208, i69, env, static) -{1,1}> iter_ConstantStackPush_1327(i538, i522, i523, i524, a208, i69, env, static) :|: i522 + i523 = i538 && 0 <= i69 && 0 < a208
iter_ConstantStackPush_1327(i538, i522, i523, i524, a208, i69, env, static) -{1,1}> iter_Load_1329(i538, iconst_3, i522, i523, i524, a208, i69, env, static) :|: iconst_3 = 3 && 0 <= i69 && 0 < a208
iter_Load_1329(i538, iconst_3, i522, i523, i524, a208, i69, env, static) -{1,1}> iter_IntArithmetic_1330(i538, iconst_3, i524, i522, i523, a208, i69, env, static) :|: iconst_3 = 3 && 0 <= i69 && 0 < a208
iter_IntArithmetic_1330(i538, iconst_3, i524, i522, i523, a208, i69, env, static) -{1,1}> iter_IntArithmetic_1332(i538, i540, i522, i523, i524, a208, i69, env, static) :|: iconst_3 * i524 = i540 && iconst_3 = 3 && 0 <= i69 && 0 < a208
iter_IntArithmetic_1332(i538, i540, i522, i523, i524, a208, i69, env, static) -{1,1}> iter_LT_1335(i541, i522, i523, i524, a208, i69, env, static) :|: i538 + i540 = i541 && 0 <= i69 && 0 < a208
iter_LT_1335(i547, i522, i523, i524, a208, i69, env, static) -{0,0}> iter_LT_1336(i547, i522, i523, i524, a208, i69, env, static) :|: 0 <= i69 && i547 <= -1 && 0 < a208
iter_LT_1335(i548, i522, i523, i524, a208, i69, env, static) -{0,0}> iter_LT_1337(i548, i522, i523, i524, a208, i69, env, static) :|: 0 <= i548 && 0 <= i69 && 0 < a208
iter_LT_1337(i548, i522, i523, i524, a208, i69, env, static) -{1,1}> iter_Load_1340(i522, i523, i524, a208, i69, env, static) :|: 0 <= i548 && 0 <= i69 && 0 < a208
iter_Load_1340(i522, i523, i524, a208, i69, env, static) -{1,1}> iter_Load_1342(i522, i523, i524, a208, i69, env, static) :|: 0 <= i69 && 0 < a208
iter_Load_1342(i522, i523, i524, a208, i69, env, static) -{1,1}> iter_LE_1349(i522, i523, i524, a208, i69, env, static) :|: 0 <= i69 && 0 < a208
iter_LE_1349(i522, i523, i524, a208, i69, env, static) -{0,0}> iter_LE_1354(i522, i523, i524, a208, i69, env, static) :|: i522 <= i523 && 0 <= i69 && 0 < a208
iter_LE_1349(i522, i523, i524, a208, i69, env, static) -{0,0}> iter_LE_1355(i522, i523, i524, a208, i69, env, static) :|: i523 < i522 && 0 <= i69 && 0 < a208
iter_LE_1354(i522, i523, i524, a208, i69, env, static) -{1,1}> iter_Load_1363(i522, i523, i524, a208, i69, env, static) :|: i522 <= i523 && 0 <= i69 && 0 < a208
iter_LE_1355(i522, i523, i524, a208, i69, env, static) -{1,1}> iter_Inc_1364(i522, i523, i524, a208, i69, env, static) :|: i523 < i522 && 0 <= i69 && 0 < a208
iter_Load_1363(i522, i523, i524, a208, i69, env, static) -{1,1}> iter_Load_1365(i523, i522, i524, a208, i69, env, static) :|: 0 <= i69 && 0 < a208
iter_Inc_1364(i522, i523, i524, a208, i69, env, static) -{1,1}> iter_JMP_1366(i551, i523, i524, a208, i69, env, static) :|: i522 + -1 = i551 && 0 <= i69 && 0 < a208
iter_Load_1365(i523, i522, i524, a208, i69, env, static) -{1,1}> iter_LE_1378(i523, i524, i522, a208, i69, env, static) :|: 0 <= i69 && 0 < a208
iter_JMP_1366(i551, i523, i524, a208, i69, env, static) -{1,1}> iter_Load_1395(i551, i523, i524, a208, i69, env, static) :|: 0 <= i69 && 0 < a208
iter_LE_1378(i523, i524, i522, a208, i69, env, static) -{0,0}> iter_LE_1404(i523, i524, i522, a208, i69, env, static) :|: 0 <= i69 && i523 <= i524 && 0 < a208
iter_LE_1378(i523, i524, i522, a208, i69, env, static) -{0,0}> iter_LE_1405(i523, i524, i522, a208, i69, env, static) :|: 0 <= i69 && i524 < i523 && 0 < a208
iter_Load_1395(i551, i523, i524, a208, i69, env, static) -{1,1}> iter_Load_1407(i551, i523, i524, a208, i69, env, static) :|: 0 <= i69 && 0 < a208
iter_LE_1404(i523, i524, i522, a208, i69, env, static) -{1,1}> iter_Load_1408(i522, i523, i524, a208, i69, env, static) :|: 0 <= i69 && i523 <= i524 && 0 < a208
iter_LE_1405(i523, i524, i522, a208, i69, env, static) -{1,1}> iter_Inc_1409(i522, i523, i524, a208, i69, env, static) :|: 0 <= i69 && i524 < i523 && 0 < a208
iter_Load_1407(i551, i523, i524, a208, i69, env, static) -{1,1}> iter_IntArithmetic_1414(i551, i523, i524, a208, i69, env, static) :|: 0 <= i69 && 0 < a208
iter_Load_1408(i522, i523, i524, a208, i69, env, static) -{1,1}> iter_Load_1415(i523, i522, i524, a208, i69, env, static) :|: 0 <= i69 && 0 < a208
iter_Inc_1409(i522, i523, i524, a208, i69, env, static) -{1,1}> iter_Inc_1417(i561, i523, i524, a208, i69, env, static) :|: 0 <= i69 && i522 + 1 = i561 && 0 < a208
iter_IntArithmetic_1414(i551, i523, i524, a208, i69, env, static) -{1,1}> iter_ConstantStackPush_1421(i562, i551, i523, i524, a208, i69, env, static) :|: i551 + i523 = i562 && 0 <= i69 && 0 < a208
iter_Load_1415(i523, i522, i524, a208, i69, env, static) -{1,1}> iter_GT_1423(i523, i524, i522, a208, i69, env, static) :|: 0 <= i69 && 0 < a208
iter_Inc_1417(i561, i523, i524, a208, i69, env, static) -{1,1}> iter_JMP_1425(i561, i566, i524, a208, i69, env, static) :|: i523 + -2 = i566 && 0 <= i69 && 0 < a208
iter_ConstantStackPush_1421(i562, i551, i523, i524, a208, i69, env, static) -{0,0}> iter_ConstantStackPush_1327(i562, i551, i523, i524, a208, i69, env, static) :|: 0 <= i69 && 0 < a208
iter_GT_1423(i523, i524, i522, a208, i69, env, static) -{0,0}> iter_GT_1429(i523, i524, i522, a208, i69, env, static) :|: 0 <= i69 && i523 <= i524 && 0 < a208
iter_JMP_1425(i561, i566, i524, a208, i69, env, static) -{1,1}> iter_Load_1435(i561, i566, i524, a208, i69, env, static) :|: 0 <= i69 && 0 < a208
iter_GT_1429(i523, i524, i522, a208, i69, env, static) -{1,1}> iter_Load_1436(i522, i523, i524, a208, i69, env, static) :|: 0 <= i69 && i523 <= i524 && 0 < a208
iter_Load_1435(i561, i566, i524, a208, i69, env, static) -{0,0}> iter_Load_1320(i561, i566, i524, a208, i69, env, static) :|: 0 <= i69 && 0 < a208
iter_Load_1436(i522, i523, i524, a208, i69, env, static) -{1,1}> iter_ConstantStackPush_1437(i522, i523, i524, a208, i69, env, static) :|: 0 <= i69 && 0 < a208
iter_ConstantStackPush_1437(i522, i523, i524, a208, i69, env, static) -{1,1}> iter_InvokeMethod_1438(i522, iconst_1, i523, i524, a208, i69, env, static) :|: iconst_1 = 1 && 0 <= i69 && 0 < a208
iter_InvokeMethod_1438(i522, iconst_1, i523, i524, a208, i69, env, static) -{1,1}> add_Load_1439(i522, iconst_1, i523, i524, a208, i69, env, static) :|: iconst_1 = 1 && 0 <= i69 && 0 < a208
add_Load_1439(i522, iconst_1, i523, i524, a208, i69, env, static) -{1,1}> add_Load_1440(i522, iconst_1, i523, i524, a208, i69, env, static) :|: iconst_1 = 1 && 0 <= i69 && 0 < a208
add_Load_1440(i522, iconst_1, i523, i524, a208, i69, env, static) -{1,1}> add_IntArithmetic_1441(i522, iconst_1, i523, i524, a208, i69, env, static) :|: iconst_1 = 1 && 0 <= i69 && 0 < a208
add_IntArithmetic_1441(i522, iconst_1, i523, i524, a208, i69, env, static) -{1,1}> add_Return_1442(i571, i523, i524, a208, i69, env, static) :|: i522 + iconst_1 = i571 && iconst_1 = 1 && 0 <= i69 && 0 < a208
add_Return_1442(i571, i523, i524, a208, i69, env, static) -{1,1}> iter_Store_1443(i571, i523, i524, a208, i69, env, static) :|: 0 <= i69 && 0 < a208
iter_Store_1443(i571, i523, i524, a208, i69, env, static) -{1,1}> iter_Load_1444(i571, i523, i524, a208, i69, env, static) :|: 0 <= i69 && 0 < a208
iter_Load_1444(i571, i523, i524, a208, i69, env, static) -{1,1}> iter_ConstantStackPush_1445(i523, i571, i524, a208, i69, env, static) :|: 0 <= i69 && 0 < a208
iter_ConstantStackPush_1445(i523, i571, i524, a208, i69, env, static) -{1,1}> iter_InvokeMethod_1446(i523, iconst_1, i571, i524, a208, i69, env, static) :|: iconst_1 = 1 && 0 <= i69 && 0 < a208
iter_InvokeMethod_1446(i523, iconst_1, i571, i524, a208, i69, env, static) -{1,1}> add_Load_1447(i523, iconst_1, i571, i524, a208, i69, env, static) :|: iconst_1 = 1 && 0 <= i69 && 0 < a208
add_Load_1447(i523, iconst_1, i571, i524, a208, i69, env, static) -{1,1}> add_Load_1448(i523, iconst_1, i571, i524, a208, i69, env, static) :|: iconst_1 = 1 && 0 <= i69 && 0 < a208
add_Load_1448(i523, iconst_1, i571, i524, a208, i69, env, static) -{1,1}> add_IntArithmetic_1449(i523, iconst_1, i571, i524, a208, i69, env, static) :|: iconst_1 = 1 && 0 <= i69 && 0 < a208
add_IntArithmetic_1449(i523, iconst_1, i571, i524, a208, i69, env, static) -{1,1}> add_Return_1450(i578, i571, i524, a208, i69, env, static) :|: iconst_1 = 1 && i523 + iconst_1 = i578 && 0 <= i69 && 0 < a208
add_Return_1450(i578, i571, i524, a208, i69, env, static) -{1,1}> iter_Store_1451(i578, i571, i524, a208, i69, env, static) :|: 0 <= i69 && 0 < a208
iter_Store_1451(i578, i571, i524, a208, i69, env, static) -{1,1}> iter_Load_1452(i571, i578, i524, a208, i69, env, static) :|: 0 <= i69 && 0 < a208
iter_Load_1452(i571, i578, i524, a208, i69, env, static) -{1,1}> iter_ConstantStackPush_1453(i524, i571, i578, a208, i69, env, static) :|: 0 <= i69 && 0 < a208
iter_ConstantStackPush_1453(i524, i571, i578, a208, i69, env, static) -{1,1}> iter_IntArithmetic_1454(i524, iconst_1, i571, i578, a208, i69, env, static) :|: iconst_1 = 1 && 0 <= i69 && 0 < a208
iter_IntArithmetic_1454(i524, iconst_1, i571, i578, a208, i69, env, static) -{1,1}> iter_Store_1455(i582, i571, i578, a208, i69, env, static) :|: iconst_1 = 1 && 0 <= i69 && i524 - iconst_1 = i582 && 0 < a208
iter_Store_1455(i582, i571, i578, a208, i69, env, static) -{1,1}> iter_JMP_1456(i571, i578, i582, a208, i69, env, static) :|: 0 <= i69 && 0 < a208
iter_JMP_1456(i571, i578, i582, a208, i69, env, static) -{1,1}> iter_Load_1457(i571, i578, i582, a208, i69, env, static) :|: 0 <= i69 && 0 < a208
iter_Load_1457(i571, i578, i582, a208, i69, env, static) -{0,0}> iter_Load_1320(i571, i578, i582, a208, i69, env, static) :|: 0 <= i69 && 0 < a208

(7) StraightLineCodeCompressionProof (BOTH CONCRETE BOUNDS(ID, ID) transformation)

obtained
main_Load_1(o1, env, static) -{26,26}> iter_Load_1320(i4', i6', i8', o1, i4', env, static'1) :|: static'1 <= static''' + 1 && 0 <= i4' && 0 <= 2 && -2 <= i8' && -1 <= i8' && 0 < o1 && i8' <= 3 && static''' <= static + 2 && i6' <= 4 && 0 <= static && i6' < 5 && -1 <= i6' && 0 <= static''' && i8' < 4 && 0 <= i6' && 0 < 2 && -1 <= i4' && 0 <= 1 && -2 <= i6' && 0 < 1 && 0 <= i8' && 0 <= static'1 && i4' < o1
by chaining
main_Load_1(o1, env, static) -{0,0}> main_Load_3(o1, env, static) :|: 0 < o1
main_Load_3(o1, env, static) -{0,0}> langle_clinit_rangle_ConstantStackPush_5(o1, env, static) :|: 0 < o1
langle_clinit_rangle_ConstantStackPush_5(o1, env, static) -{1,1}> langle_clinit_rangle_ArrayCreate_9(iconst_0, o1, env, static) :|: iconst_0 = 0 && 0 < o1
langle_clinit_rangle_ArrayCreate_9(iconst_0, o1, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_10(a2, o1, iconst_0, env, static) :|: a2 = 2 && iconst_0 = 0 && 0 < a2 && 0 < o1
langle_clinit_rangle_FieldAccess_10(a2, o1, iconst_0, env, static) -{1,1}> langle_clinit_rangle_New_13(o1, env, static') :|: 0 <= a2 && iconst_0 = 0 && static' <= static + a2 && 0 <= static && 0 < a2 && 0 < o1
langle_clinit_rangle_New_13(o1, env, static) -{0,0}> langle_clinit_rangle_New_15(o1, env, static) :|: 0 < o1
langle_clinit_rangle_New_15(o1, env, static) -{0,0}> langle_clinit_rangle_New_16(o1, env, static) :|: 0 <= static && 0 < o1
langle_clinit_rangle_New_16(o1, env, static) -{1,1}> langle_clinit_rangle_Duplicate_18(o4, o1, env, static) :|: o4 = 1 && 0 < o4 && 0 < o1
langle_clinit_rangle_Duplicate_18(o4, o1, env, static) -{1,1}> langle_clinit_rangle_ConstantStackPush_20(o4, o1, env, static) :|: 0 < o4 && 0 < o1
langle_clinit_rangle_ConstantStackPush_20(o4, o1, env, static) -{1,1}> langle_clinit_rangle_InvokeMethod_22(o4, NULL, o1, env, static) :|: NULL = 0 && 0 < o4 && 0 < o1
langle_clinit_rangle_InvokeMethod_22(o4, NULL, o1, env, static) -{1,1}> langle_init_rangle_Load_24(o4, o1, env, static) :|: NULL = 0 && 0 < o4 && 0 < o1
langle_init_rangle_Load_24(o4, o1, env, static) -{1,1}> langle_init_rangle_InvokeMethod_25(o4, o1, env, static) :|: 0 < o4 && 0 < o1
langle_init_rangle_InvokeMethod_25(o4, o1, env, static) -{1,1}> langle_init_rangle_Load_27(o4, o1, env, static) :|: 0 < o4 && 0 < o1
langle_init_rangle_Load_27(o4, o1, env, static) -{1,1}> langle_init_rangle_InvokeMethod_30(o4, o1, env, static) :|: 0 < o4 && 0 < o1
langle_init_rangle_InvokeMethod_30(o4, o1, env, static) -{1,1}> langle_init_rangle_Return_32(o4, o1, env, static) :|: 0 < o4 && 0 < o1
langle_init_rangle_Return_32(o4, o1, env, static) -{1,1}> langle_init_rangle_Return_35(o4, o1, env, static) :|: 0 < o4 && 0 < o1
langle_init_rangle_Return_35(o4, o1, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_37(o4, o1, env, static) :|: 0 < o4 && 0 < o1
langle_clinit_rangle_FieldAccess_37(o4, o1, env, static) -{1,1}> langle_clinit_rangle_Return_40(o1, env, static') :|: 0 <= o4 && 0 < o4 && 0 <= static && 0 < o1 && static' <= static + o4
langle_clinit_rangle_Return_40(o1, env, static) -{1,1}> main_Load_41(o1, env, static) :|: 0 < o1
main_Load_41(o1, env, static) -{0,0}> main_Load_42(o1, env, static) :|: 0 < o1
main_Load_42(o1, env, static) -{0,0}> main_Load_43(o1, env, static) :|: 0 <= static && 0 < o1
main_Load_43(o1, env, static) -{0,0}> main_Load_45(o1, env, static) :|: 0 < o1
main_Load_45(o1, env, static) -{0,0}> main_Load_47(o1, env, static) :|: 0 < o1
main_Load_47(o1, env, static) -{1,1}> main_ArrayLength_51(o1, env, static) :|: 0 < o1
main_ArrayLength_51(a6, env, static) -{0,0}> main_ArrayLength_52(a6, i4, env, static) :|: 0 <= i4 && 0 < a6 && i4 < a6
main_ArrayLength_52(a6, i4, env, static) -{1,1}> main_Load_54(a6, i4, env, static) :|: 0 <= i4 && 0 < a6
main_Load_54(a6, i4, env, static) -{1,1}> main_ArrayLength_56(a6, i4, env, static) :|: 0 <= i4 && 0 < a6
main_ArrayLength_56(a6, i4, env, static) -{1,1}> main_ConstantStackPush_58(a6, i4, env, static) :|: 0 <= i4 && 0 < a6
main_ConstantStackPush_58(a6, i4, env, static) -{1,1}> main_IntArithmetic_60(a6, i4, iconst_5, env, static) :|: iconst_5 = 5 && 0 <= i4 && 0 < a6
main_IntArithmetic_60(a6, i4, iconst_5, env, static) -{1,1}> main_Load_62(a6, i4, i6, env, static) :|: 0 <= i6 && iconst_5 = 5 && i6 < iconst_5 && 0 <= i4 && i6 <= 4 && 0 < a6
main_Load_62(a6, i4, i6, env, static) -{1,1}> main_ArrayLength_64(a6, i4, i6, env, static) :|: 0 <= i6 && 0 <= i4 && i6 <= 4 && 0 < a6
main_ArrayLength_64(a6, i4, i6, env, static) -{1,1}> main_ConstantStackPush_66(a6, i4, i6, env, static) :|: 0 <= i6 && 0 <= i4 && i6 <= 4 && 0 < a6
main_ConstantStackPush_66(a6, i4, i6, env, static) -{1,1}> main_IntArithmetic_68(a6, i4, i6, iconst_4, env, static) :|: 0 <= i6 && iconst_4 = 4 && 0 <= i4 && i6 <= 4 && 0 < a6
main_IntArithmetic_68(a6, i4, i6, iconst_4, env, static) -{1,1}> main_InvokeMethod_70(a6, i4, i6, i8, env, static) :|: 0 <= i6 && i8 <= 3 && i8 < iconst_4 && iconst_4 = 4 && 0 <= i4 && i6 <= 4 && 0 < a6 && 0 <= i8
main_InvokeMethod_70(a6, i4, i6, i8, env, static) -{1,1}> iter_Load_72(i4, i6, i8, a6, env, static) :|: 0 <= i6 && i8 <= 3 && 0 <= i4 && i6 <= 4 && 0 < a6 && 0 <= i8
iter_Load_72(i4, i6, i8, a6, env, static) -{0,0}> iter_Load_577(i4, i6, i8, a6, i4, env, static) :|: 0 <= i6 && i8 <= 3 && -1 <= i6 && 0 <= i4 && -1 <= i4 && i6 <= 4 && 0 < a6 && 0 <= i8
iter_Load_577(i249, i250, i8, a110, i69, env, static) -{0,0}> iter_Load_710(i249, i250, i8, a110, i69, env, static) :|: i8 <= 3 && 0 < a110 && -1 <= i250 && -1 <= i249 && -1 <= i8 && 0 <= i8 && 0 <= i69
iter_Load_710(i301, i302, i303, a131, i69, env, static) -{0,0}> iter_Load_762(i301, i302, i303, a131, i69, env, static) :|: i303 <= 3 && -1 <= i302 && -2 <= i302 && 0 <= i69 && -1 <= i303 && -1 <= i301 && 0 < a131
iter_Load_762(i326, i327, i303, a139, i69, env, static) -{0,0}> iter_Load_796(i326, i327, i303, a139, i69, env, static) :|: -1 <= i326 && i303 <= 3 && 0 <= i69 && -1 <= i303 && -2 <= i327 && 0 < a139
iter_Load_796(i342, i327, i303, a145, i69, env, static) -{0,0}> iter_Load_899(i342, i327, i303, a145, i69, env, static) :|: i303 <= 3 && -2 <= i303 && 0 < a145 && 0 <= i69 && -1 <= i303 && -2 <= i327
iter_Load_899(i380, i381, i382, a164, i69, env, static) -{0,0}> iter_Load_1043(i380, i381, i382, a164, i69, env, static) :|: -2 <= i381 && i382 <= 3 && 0 < a164 && -2 <= i382 && 0 <= i69
iter_Load_1043(i426, i427, i382, a176, i69, env, static) -{0,0}> iter_Load_1320(i426, i427, i382, a176, i69, env, static) :|: 0 < a176 && i382 <= 3 && -2 <= i382 && 0 <= i69

obtained
iter_Load_1320(i522, i523, i524, a208, i69, env, static) -{3,3}> iter_ConstantStackPush_1327(i538', i522, i523, i524, a208, i69, env, static) :|: 0 <= i69 && 0 < a208 && i522 + i523 = i538'
by chaining
iter_Load_1320(i522, i523, i524, a208, i69, env, static) -{1,1}> iter_Load_1321(i522, i523, i524, a208, i69, env, static) :|: 0 <= i69 && 0 < a208
iter_Load_1321(i522, i523, i524, a208, i69, env, static) -{1,1}> iter_IntArithmetic_1324(i522, i523, i524, a208, i69, env, static) :|: 0 <= i69 && 0 < a208
iter_IntArithmetic_1324(i522, i523, i524, a208, i69, env, static) -{1,1}> iter_ConstantStackPush_1327(i538, i522, i523, i524, a208, i69, env, static) :|: i522 + i523 = i538 && 0 <= i69 && 0 < a208

obtained
iter_ConstantStackPush_1327(i538, i522, i523, i524, a208, i69, env, static) -{4,4}> iter_LT_1335(i541', i522, i523, i524, a208, i69, env, static) :|: 3 * i524 = i540' && 0 < a208 && 0 <= i69 && i538 + i540' = i541'
by chaining
iter_ConstantStackPush_1327(i538, i522, i523, i524, a208, i69, env, static) -{1,1}> iter_Load_1329(i538, iconst_3, i522, i523, i524, a208, i69, env, static) :|: iconst_3 = 3 && 0 <= i69 && 0 < a208
iter_Load_1329(i538, iconst_3, i522, i523, i524, a208, i69, env, static) -{1,1}> iter_IntArithmetic_1330(i538, iconst_3, i524, i522, i523, a208, i69, env, static) :|: iconst_3 = 3 && 0 <= i69 && 0 < a208
iter_IntArithmetic_1330(i538, iconst_3, i524, i522, i523, a208, i69, env, static) -{1,1}> iter_IntArithmetic_1332(i538, i540, i522, i523, i524, a208, i69, env, static) :|: iconst_3 * i524 = i540 && iconst_3 = 3 && 0 <= i69 && 0 < a208
iter_IntArithmetic_1332(i538, i540, i522, i523, i524, a208, i69, env, static) -{1,1}> iter_LT_1335(i541, i522, i523, i524, a208, i69, env, static) :|: i538 + i540 = i541 && 0 <= i69 && 0 < a208

obtained
iter_LT_1335(i548, i522, i523, i524, a208, i69, env, static) -{3,3}> iter_LE_1349(i522, i523, i524, a208, i69, env, static) :|: 0 <= i548 && 0 <= i69 && 0 < a208
by chaining
iter_LT_1335(i548, i522, i523, i524, a208, i69, env, static) -{0,0}> iter_LT_1337(i548, i522, i523, i524, a208, i69, env, static) :|: 0 <= i548 && 0 <= i69 && 0 < a208
iter_LT_1337(i548, i522, i523, i524, a208, i69, env, static) -{1,1}> iter_Load_1340(i522, i523, i524, a208, i69, env, static) :|: 0 <= i548 && 0 <= i69 && 0 < a208
iter_Load_1340(i522, i523, i524, a208, i69, env, static) -{1,1}> iter_Load_1342(i522, i523, i524, a208, i69, env, static) :|: 0 <= i69 && 0 < a208
iter_Load_1342(i522, i523, i524, a208, i69, env, static) -{1,1}> iter_LE_1349(i522, i523, i524, a208, i69, env, static) :|: 0 <= i69 && 0 < a208

obtained
iter_LE_1349(i522, i523, i524, a208, i69, env, static) -{6,6}> iter_ConstantStackPush_1327(i562', i551', i523, i524, a208, i69, env, static) :|: i522 + -1 = i551' && 0 <= i69 && 0 < a208 && i551' + i523 = i562' && i523 < i522
by chaining
iter_LE_1349(i522, i523, i524, a208, i69, env, static) -{0,0}> iter_LE_1355(i522, i523, i524, a208, i69, env, static) :|: i523 < i522 && 0 <= i69 && 0 < a208
iter_LE_1355(i522, i523, i524, a208, i69, env, static) -{1,1}> iter_Inc_1364(i522, i523, i524, a208, i69, env, static) :|: i523 < i522 && 0 <= i69 && 0 < a208
iter_Inc_1364(i522, i523, i524, a208, i69, env, static) -{1,1}> iter_JMP_1366(i551, i523, i524, a208, i69, env, static) :|: i522 + -1 = i551 && 0 <= i69 && 0 < a208
iter_JMP_1366(i551, i523, i524, a208, i69, env, static) -{1,1}> iter_Load_1395(i551, i523, i524, a208, i69, env, static) :|: 0 <= i69 && 0 < a208
iter_Load_1395(i551, i523, i524, a208, i69, env, static) -{1,1}> iter_Load_1407(i551, i523, i524, a208, i69, env, static) :|: 0 <= i69 && 0 < a208
iter_Load_1407(i551, i523, i524, a208, i69, env, static) -{1,1}> iter_IntArithmetic_1414(i551, i523, i524, a208, i69, env, static) :|: 0 <= i69 && 0 < a208
iter_IntArithmetic_1414(i551, i523, i524, a208, i69, env, static) -{1,1}> iter_ConstantStackPush_1421(i562, i551, i523, i524, a208, i69, env, static) :|: i551 + i523 = i562 && 0 <= i69 && 0 < a208
iter_ConstantStackPush_1421(i562, i551, i523, i524, a208, i69, env, static) -{0,0}> iter_ConstantStackPush_1327(i562, i551, i523, i524, a208, i69, env, static) :|: 0 <= i69 && 0 < a208

obtained
iter_LE_1349(i522, i523, i524, a208, i69, env, static) -{3,3}> iter_LE_1378(i523, i524, i522, a208, i69, env, static) :|: i522 <= i523 && 0 <= i69 && 0 < a208
by chaining
iter_LE_1349(i522, i523, i524, a208, i69, env, static) -{0,0}> iter_LE_1354(i522, i523, i524, a208, i69, env, static) :|: i522 <= i523 && 0 <= i69 && 0 < a208
iter_LE_1354(i522, i523, i524, a208, i69, env, static) -{1,1}> iter_Load_1363(i522, i523, i524, a208, i69, env, static) :|: i522 <= i523 && 0 <= i69 && 0 < a208
iter_Load_1363(i522, i523, i524, a208, i69, env, static) -{1,1}> iter_Load_1365(i523, i522, i524, a208, i69, env, static) :|: 0 <= i69 && 0 < a208
iter_Load_1365(i523, i522, i524, a208, i69, env, static) -{1,1}> iter_LE_1378(i523, i524, i522, a208, i69, env, static) :|: 0 <= i69 && 0 < a208

obtained
iter_LE_1378(i523, i524, i522, a208, i69, env, static) -{4,4}> iter_Load_1320(i561', i566', i524, a208, i69, env, static) :|: i522 + 1 = i561' && 0 <= i69 && 0 < a208 && i523 + -2 = i566' && i524 < i523
by chaining
iter_LE_1378(i523, i524, i522, a208, i69, env, static) -{0,0}> iter_LE_1405(i523, i524, i522, a208, i69, env, static) :|: 0 <= i69 && i524 < i523 && 0 < a208
iter_LE_1405(i523, i524, i522, a208, i69, env, static) -{1,1}> iter_Inc_1409(i522, i523, i524, a208, i69, env, static) :|: 0 <= i69 && i524 < i523 && 0 < a208
iter_Inc_1409(i522, i523, i524, a208, i69, env, static) -{1,1}> iter_Inc_1417(i561, i523, i524, a208, i69, env, static) :|: 0 <= i69 && i522 + 1 = i561 && 0 < a208
iter_Inc_1417(i561, i523, i524, a208, i69, env, static) -{1,1}> iter_JMP_1425(i561, i566, i524, a208, i69, env, static) :|: i523 + -2 = i566 && 0 <= i69 && 0 < a208
iter_JMP_1425(i561, i566, i524, a208, i69, env, static) -{1,1}> iter_Load_1435(i561, i566, i524, a208, i69, env, static) :|: 0 <= i69 && 0 < a208
iter_Load_1435(i561, i566, i524, a208, i69, env, static) -{0,0}> iter_Load_1320(i561, i566, i524, a208, i69, env, static) :|: 0 <= i69 && 0 < a208

obtained
iter_LE_1378(i523, i524, i522, a208, i69, env, static) -{25,25}> iter_Load_1320(i571', i578', i582', a208, i69, env, static) :|: i523 <= i524 && 0 <= i69 && 0 < a208 && i522 + 1 = i571' && i524 - 1 = i582' && i523 + 1 = i578'
by chaining
iter_LE_1378(i523, i524, i522, a208, i69, env, static) -{0,0}> iter_LE_1404(i523, i524, i522, a208, i69, env, static) :|: 0 <= i69 && i523 <= i524 && 0 < a208
iter_LE_1404(i523, i524, i522, a208, i69, env, static) -{1,1}> iter_Load_1408(i522, i523, i524, a208, i69, env, static) :|: 0 <= i69 && i523 <= i524 && 0 < a208
iter_Load_1408(i522, i523, i524, a208, i69, env, static) -{1,1}> iter_Load_1415(i523, i522, i524, a208, i69, env, static) :|: 0 <= i69 && 0 < a208
iter_Load_1415(i523, i522, i524, a208, i69, env, static) -{1,1}> iter_GT_1423(i523, i524, i522, a208, i69, env, static) :|: 0 <= i69 && 0 < a208
iter_GT_1423(i523, i524, i522, a208, i69, env, static) -{0,0}> iter_GT_1429(i523, i524, i522, a208, i69, env, static) :|: 0 <= i69 && i523 <= i524 && 0 < a208
iter_GT_1429(i523, i524, i522, a208, i69, env, static) -{1,1}> iter_Load_1436(i522, i523, i524, a208, i69, env, static) :|: 0 <= i69 && i523 <= i524 && 0 < a208
iter_Load_1436(i522, i523, i524, a208, i69, env, static) -{1,1}> iter_ConstantStackPush_1437(i522, i523, i524, a208, i69, env, static) :|: 0 <= i69 && 0 < a208
iter_ConstantStackPush_1437(i522, i523, i524, a208, i69, env, static) -{1,1}> iter_InvokeMethod_1438(i522, iconst_1, i523, i524, a208, i69, env, static) :|: iconst_1 = 1 && 0 <= i69 && 0 < a208
iter_InvokeMethod_1438(i522, iconst_1, i523, i524, a208, i69, env, static) -{1,1}> add_Load_1439(i522, iconst_1, i523, i524, a208, i69, env, static) :|: iconst_1 = 1 && 0 <= i69 && 0 < a208
add_Load_1439(i522, iconst_1, i523, i524, a208, i69, env, static) -{1,1}> add_Load_1440(i522, iconst_1, i523, i524, a208, i69, env, static) :|: iconst_1 = 1 && 0 <= i69 && 0 < a208
add_Load_1440(i522, iconst_1, i523, i524, a208, i69, env, static) -{1,1}> add_IntArithmetic_1441(i522, iconst_1, i523, i524, a208, i69, env, static) :|: iconst_1 = 1 && 0 <= i69 && 0 < a208
add_IntArithmetic_1441(i522, iconst_1, i523, i524, a208, i69, env, static) -{1,1}> add_Return_1442(i571, i523, i524, a208, i69, env, static) :|: i522 + iconst_1 = i571 && iconst_1 = 1 && 0 <= i69 && 0 < a208
add_Return_1442(i571, i523, i524, a208, i69, env, static) -{1,1}> iter_Store_1443(i571, i523, i524, a208, i69, env, static) :|: 0 <= i69 && 0 < a208
iter_Store_1443(i571, i523, i524, a208, i69, env, static) -{1,1}> iter_Load_1444(i571, i523, i524, a208, i69, env, static) :|: 0 <= i69 && 0 < a208
iter_Load_1444(i571, i523, i524, a208, i69, env, static) -{1,1}> iter_ConstantStackPush_1445(i523, i571, i524, a208, i69, env, static) :|: 0 <= i69 && 0 < a208
iter_ConstantStackPush_1445(i523, i571, i524, a208, i69, env, static) -{1,1}> iter_InvokeMethod_1446(i523, iconst_1, i571, i524, a208, i69, env, static) :|: iconst_1 = 1 && 0 <= i69 && 0 < a208
iter_InvokeMethod_1446(i523, iconst_1, i571, i524, a208, i69, env, static) -{1,1}> add_Load_1447(i523, iconst_1, i571, i524, a208, i69, env, static) :|: iconst_1 = 1 && 0 <= i69 && 0 < a208
add_Load_1447(i523, iconst_1, i571, i524, a208, i69, env, static) -{1,1}> add_Load_1448(i523, iconst_1, i571, i524, a208, i69, env, static) :|: iconst_1 = 1 && 0 <= i69 && 0 < a208
add_Load_1448(i523, iconst_1, i571, i524, a208, i69, env, static) -{1,1}> add_IntArithmetic_1449(i523, iconst_1, i571, i524, a208, i69, env, static) :|: iconst_1 = 1 && 0 <= i69 && 0 < a208
add_IntArithmetic_1449(i523, iconst_1, i571, i524, a208, i69, env, static) -{1,1}> add_Return_1450(i578, i571, i524, a208, i69, env, static) :|: iconst_1 = 1 && i523 + iconst_1 = i578 && 0 <= i69 && 0 < a208
add_Return_1450(i578, i571, i524, a208, i69, env, static) -{1,1}> iter_Store_1451(i578, i571, i524, a208, i69, env, static) :|: 0 <= i69 && 0 < a208
iter_Store_1451(i578, i571, i524, a208, i69, env, static) -{1,1}> iter_Load_1452(i571, i578, i524, a208, i69, env, static) :|: 0 <= i69 && 0 < a208
iter_Load_1452(i571, i578, i524, a208, i69, env, static) -{1,1}> iter_ConstantStackPush_1453(i524, i571, i578, a208, i69, env, static) :|: 0 <= i69 && 0 < a208
iter_ConstantStackPush_1453(i524, i571, i578, a208, i69, env, static) -{1,1}> iter_IntArithmetic_1454(i524, iconst_1, i571, i578, a208, i69, env, static) :|: iconst_1 = 1 && 0 <= i69 && 0 < a208
iter_IntArithmetic_1454(i524, iconst_1, i571, i578, a208, i69, env, static) -{1,1}> iter_Store_1455(i582, i571, i578, a208, i69, env, static) :|: iconst_1 = 1 && 0 <= i69 && i524 - iconst_1 = i582 && 0 < a208
iter_Store_1455(i582, i571, i578, a208, i69, env, static) -{1,1}> iter_JMP_1456(i571, i578, i582, a208, i69, env, static) :|: 0 <= i69 && 0 < a208
iter_JMP_1456(i571, i578, i582, a208, i69, env, static) -{1,1}> iter_Load_1457(i571, i578, i582, a208, i69, env, static) :|: 0 <= i69 && 0 < a208
iter_Load_1457(i571, i578, i582, a208, i69, env, static) -{0,0}> iter_Load_1320(i571, i578, i582, a208, i69, env, static) :|: 0 <= i69 && 0 < a208

(8) Obligation:

IntTrs with 9 rules
Start term: main_Load_1(#0, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_Load_1(o1, env, static) -{26,26}> iter_Load_1320(i4', i6', i8', o1, i4', env, static'1) :|: static'1 <= static''' + 1 && 0 <= i4' && 0 <= 2 && -2 <= i8' && -1 <= i8' && 0 < o1 && i8' <= 3 && static''' <= static + 2 && i6' <= 4 && 0 <= static && i6' < 5 && -1 <= i6' && 0 <= static''' && i8' < 4 && 0 <= i6' && 0 < 2 && -1 <= i4' && 0 <= 1 && -2 <= i6' && 0 < 1 && 0 <= i8' && 0 <= static'1 && i4' < o1
iter_Load_1320(i522, i523, i524, a208, i69, env, static) -{3,3}> iter_ConstantStackPush_1327(i538', i522, i523, i524, a208, i69, env, static) :|: 0 <= i69 && 0 < a208 && i522 + i523 = i538'
iter_ConstantStackPush_1327(i538, i522, i523, i524, a208, i69, env, static) -{4,4}> iter_LT_1335(i541', i522, i523, i524, a208, i69, env, static) :|: 3 * i524 = i540' && 0 < a208 && 0 <= i69 && i538 + i540' = i541'
iter_LT_1335(i547, i522, i523, i524, a208, i69, env, static) -{0,0}> iter_LT_1336(i547, i522, i523, i524, a208, i69, env, static) :|: 0 <= i69 && i547 <= -1 && 0 < a208
iter_LT_1335(i548, i522, i523, i524, a208, i69, env, static) -{3,3}> iter_LE_1349(i522, i523, i524, a208, i69, env, static) :|: 0 <= i548 && 0 <= i69 && 0 < a208
iter_LE_1349(i522, i523, i524, a208, i69, env, static) -{6,6}> iter_ConstantStackPush_1327(i562', i551', i523, i524, a208, i69, env, static) :|: i522 + -1 = i551' && 0 <= i69 && 0 < a208 && i551' + i523 = i562' && i523 < i522
iter_LE_1349(i522, i523, i524, a208, i69, env, static) -{3,3}> iter_LE_1378(i523, i524, i522, a208, i69, env, static) :|: i522 <= i523 && 0 <= i69 && 0 < a208
iter_LE_1378(i523, i524, i522, a208, i69, env, static) -{4,4}> iter_Load_1320(i561', i566', i524, a208, i69, env, static) :|: i522 + 1 = i561' && 0 <= i69 && 0 < a208 && i523 + -2 = i566' && i524 < i523
iter_LE_1378(i523, i524, i522, a208, i69, env, static) -{25,25}> iter_Load_1320(i571', i578', i582', a208, i69, env, static) :|: i523 <= i524 && 0 <= i69 && 0 < a208 && i522 + 1 = i571' && i524 - 1 = i582' && i523 + 1 = i578'

(9) MovedArithmeticFromConstraintsProof (BOTH CONCRETE BOUNDS(ID, ID) transformation)

Moved arithmethic from constraints to rhss.

iter_LE_1378(i523, i524, i522, a208, i69, env, static) -{4,4}> iter_Load_1320(i561', i566', i524, a208, i69, env, static) :|: i522 + 1 = i561' && 0 <= i69 && 0 < a208 && i523 + -2 = i566' && i524 < i523
was transformed to
iter_LE_1378(i523, i524, i522, a208, i69, env, static) -{4,4}> iter_Load_1320(i522 + 1, i523 + -2, i524, a208, i69, env, static) :|: i522 + 1 = i561' && 0 <= i69 && 0 < a208 && i523 + -2 = i566' && i524 < i523

iter_Load_1320(i522, i523, i524, a208, i69, env, static) -{3,3}> iter_ConstantStackPush_1327(i538', i522, i523, i524, a208, i69, env, static) :|: 0 <= i69 && 0 < a208 && i522 + i523 = i538'
was transformed to
iter_Load_1320(i522, i523, i524, a208, i69, env, static) -{3,3}> iter_ConstantStackPush_1327(i522 + i523, i522, i523, i524, a208, i69, env, static) :|: 0 <= i69 && 0 < a208 && i522 + i523 = i538'

iter_LE_1349(i522, i523, i524, a208, i69, env, static) -{6,6}> iter_ConstantStackPush_1327(i562', i551', i523, i524, a208, i69, env, static) :|: i522 + -1 = i551' && 0 <= i69 && 0 < a208 && i551' + i523 = i562' && i523 < i522
was transformed to
iter_LE_1349(i522, i523, i524, a208, i69, env, static) -{6,6}> iter_ConstantStackPush_1327(i522 + -1 + i523, i522 + -1, i523, i524, a208, i69, env, static) :|: i522 + -1 = i551' && 0 <= i69 && 0 < a208 && i551' + i523 = i562' && i523 < i522

iter_LE_1378(i523, i524, i522, a208, i69, env, static) -{25,25}> iter_Load_1320(i571', i578', i582', a208, i69, env, static) :|: i523 <= i524 && 0 <= i69 && 0 < a208 && i522 + 1 = i571' && i524 - 1 = i582' && i523 + 1 = i578'
was transformed to
iter_LE_1378(i523, i524, i522, a208, i69, env, static) -{25,25}> iter_Load_1320(i522 + 1, i523 + 1, i524 - 1, a208, i69, env, static) :|: i523 <= i524 && 0 <= i69 && 0 < a208 && i522 + 1 = i571' && i524 - 1 = i582' && i523 + 1 = i578'

iter_ConstantStackPush_1327(i538, i522, i523, i524, a208, i69, env, static) -{4,4}> iter_LT_1335(i541', i522, i523, i524, a208, i69, env, static) :|: 3 * i524 = i540' && 0 < a208 && 0 <= i69 && i538 + i540' = i541'
was transformed to
iter_ConstantStackPush_1327(i538, i522, i523, i524, a208, i69, env, static) -{4,4}> iter_LT_1335(i538 + 3 * i524, i522, i523, i524, a208, i69, env, static) :|: 3 * i524 = i540' && 0 < a208 && 0 <= i69 && i538 + i540' = i541'

(10) Obligation:

IntTrs with 9 rules
Start term: main_Load_1(#0, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
iter_LE_1378(i523, i524, i522, a208, i69, env, static) -{4,4}> iter_Load_1320(i522 + 1, i523 + -2, i524, a208, i69, env, static) :|: i522 + 1 = i561' && 0 <= i69 && 0 < a208 && i523 + -2 = i566' && i524 < i523
iter_Load_1320(i522, i523, i524, a208, i69, env, static) -{3,3}> iter_ConstantStackPush_1327(i522 + i523, i522, i523, i524, a208, i69, env, static) :|: 0 <= i69 && 0 < a208 && i522 + i523 = i538'
iter_LE_1349(i522, i523, i524, a208, i69, env, static) -{6,6}> iter_ConstantStackPush_1327(i522 + -1 + i523, i522 + -1, i523, i524, a208, i69, env, static) :|: i522 + -1 = i551' && 0 <= i69 && 0 < a208 && i551' + i523 = i562' && i523 < i522
iter_LE_1378(i523, i524, i522, a208, i69, env, static) -{25,25}> iter_Load_1320(i522 + 1, i523 + 1, i524 - 1, a208, i69, env, static) :|: i523 <= i524 && 0 <= i69 && 0 < a208 && i522 + 1 = i571' && i524 - 1 = i582' && i523 + 1 = i578'
iter_LE_1349(i522, i523, i524, a208, i69, env, static) -{3,3}> iter_LE_1378(i523, i524, i522, a208, i69, env, static) :|: i522 <= i523 && 0 <= i69 && 0 < a208
iter_LT_1335(i548, i522, i523, i524, a208, i69, env, static) -{3,3}> iter_LE_1349(i522, i523, i524, a208, i69, env, static) :|: 0 <= i548 && 0 <= i69 && 0 < a208
iter_ConstantStackPush_1327(i538, i522, i523, i524, a208, i69, env, static) -{4,4}> iter_LT_1335(i538 + 3 * i524, i522, i523, i524, a208, i69, env, static) :|: 3 * i524 = i540' && 0 < a208 && 0 <= i69 && i538 + i540' = i541'
main_Load_1(o1, env, static) -{26,26}> iter_Load_1320(i4', i6', i8', o1, i4', env, static'1) :|: static'1 <= static''' + 1 && 0 <= i4' && 0 <= 2 && -2 <= i8' && -1 <= i8' && 0 < o1 && i8' <= 3 && static''' <= static + 2 && i6' <= 4 && 0 <= static && i6' < 5 && -1 <= i6' && 0 <= static''' && i8' < 4 && 0 <= i6' && 0 < 2 && -1 <= i4' && 0 <= 1 && -2 <= i6' && 0 < 1 && 0 <= i8' && 0 <= static'1 && i4' < o1
iter_LT_1335(i547, i522, i523, i524, a208, i69, env, static) -{0,0}> iter_LT_1336(i547, i522, i523, i524, a208, i69, env, static) :|: 0 <= i69 && i547 <= -1 && 0 < a208

(11) ExpressionSimplificationProof (BOTH CONCRETE BOUNDS(ID, ID) transformation)

Simplified expressions.

iter_LE_1378(i523, i524, i522, a208, i69, env, static) -{4,4}> iter_Load_1320(i522 + 1, i523 + -2, i524, a208, i69, env, static) :|: i522 + 1 = i561' && 0 <= i69 && 0 < a208 && i523 + -2 = i566' && i524 < i523
was transformed to
iter_LE_1378(i523, i524, i522, a208, i69, env, static) -{4,4}> iter_Load_1320(i522 + 1, i523 - 2, i524, a208, i69, env, static) :|: i522 + 1 = i561' && 0 <= i69 && 0 < a208 && i523 - 2 = i566' && i524 < i523

iter_LE_1349(i522, i523, i524, a208, i69, env, static) -{6,6}> iter_ConstantStackPush_1327(i522 + -1 + i523, i522 + -1, i523, i524, a208, i69, env, static) :|: i522 + -1 = i551' && 0 <= i69 && 0 < a208 && i551' + i523 = i562' && i523 < i522
was transformed to
iter_LE_1349(i522, i523, i524, a208, i69, env, static) -{6,6}> iter_ConstantStackPush_1327(i522 - 1 + i523, i522 - 1, i523, i524, a208, i69, env, static) :|: i522 - 1 = i551' && 0 <= i69 && 0 < a208 && i551' + i523 = i562' && i523 < i522

main_Load_1(o1, env, static) -{26,26}> iter_Load_1320(i4', i6', i8', o1, i4', env, static'1) :|: static'1 <= static''' + 1 && 0 <= i4' && 0 <= 2 && -2 <= i8' && -1 <= i8' && 0 < o1 && i8' <= 3 && static''' <= static + 2 && i6' <= 4 && 0 <= static && i6' < 5 && -1 <= i6' && 0 <= static''' && i8' < 4 && 0 <= i6' && 0 < 2 && -1 <= i4' && 0 <= 1 && -2 <= i6' && 0 < 1 && 0 <= i8' && 0 <= static'1 && i4' < o1
was transformed to
main_Load_1(o1, env, static) -{26,26}> iter_Load_1320(i4', i6', i8', o1, i4', env, static'1) :|: static'1 <= static''' + 1 && 0 <= i4' && -2 <= i8' && -1 <= i8' && 0 < o1 && i8' <= 3 && static''' <= static + 2 && i6' <= 4 && 0 <= static && i6' < 5 && -1 <= i6' && 0 <= static''' && i8' < 4 && 0 <= i6' && -1 <= i4' && -2 <= i6' && 0 <= i8' && 0 <= static'1 && i4' < o1

(12) Obligation:

IntTrs with 9 rules
Start term: main_Load_1(#0, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
iter_LE_1378(i523, i524, i522, a208, i69, env, static) -{25,25}> iter_Load_1320(i522 + 1, i523 + 1, i524 - 1, a208, i69, env, static) :|: i523 <= i524 && 0 <= i69 && 0 < a208 && i522 + 1 = i571' && i524 - 1 = i582' && i523 + 1 = i578'
iter_ConstantStackPush_1327(i538, i522, i523, i524, a208, i69, env, static) -{4,4}> iter_LT_1335(i538 + 3 * i524, i522, i523, i524, a208, i69, env, static) :|: 3 * i524 = i540' && 0 < a208 && 0 <= i69 && i538 + i540' = i541'
iter_LE_1378(i523, i524, i522, a208, i69, env, static) -{4,4}> iter_Load_1320(i522 + 1, i523 - 2, i524, a208, i69, env, static) :|: i522 + 1 = i561' && 0 <= i69 && 0 < a208 && i523 - 2 = i566' && i524 < i523
iter_LE_1349(i522, i523, i524, a208, i69, env, static) -{6,6}> iter_ConstantStackPush_1327(i522 - 1 + i523, i522 - 1, i523, i524, a208, i69, env, static) :|: i522 - 1 = i551' && 0 <= i69 && 0 < a208 && i551' + i523 = i562' && i523 < i522
iter_Load_1320(i522, i523, i524, a208, i69, env, static) -{3,3}> iter_ConstantStackPush_1327(i522 + i523, i522, i523, i524, a208, i69, env, static) :|: 0 <= i69 && 0 < a208 && i522 + i523 = i538'
iter_LE_1349(i522, i523, i524, a208, i69, env, static) -{3,3}> iter_LE_1378(i523, i524, i522, a208, i69, env, static) :|: i522 <= i523 && 0 <= i69 && 0 < a208
main_Load_1(o1, env, static) -{26,26}> iter_Load_1320(i4', i6', i8', o1, i4', env, static'1) :|: static'1 <= static''' + 1 && 0 <= i4' && -2 <= i8' && -1 <= i8' && 0 < o1 && i8' <= 3 && static''' <= static + 2 && i6' <= 4 && 0 <= static && i6' < 5 && -1 <= i6' && 0 <= static''' && i8' < 4 && 0 <= i6' && -1 <= i4' && -2 <= i6' && 0 <= i8' && 0 <= static'1 && i4' < o1
iter_LT_1335(i548, i522, i523, i524, a208, i69, env, static) -{3,3}> iter_LE_1349(i522, i523, i524, a208, i69, env, static) :|: 0 <= i548 && 0 <= i69 && 0 < a208
iter_LT_1335(i547, i522, i523, i524, a208, i69, env, static) -{0,0}> iter_LT_1336(i547, i522, i523, i524, a208, i69, env, static) :|: 0 <= i69 && i547 <= -1 && 0 < a208

(13) JBCGraphEdgesToCpxIntTrsProof (CONCRETE UPPER BOUND(ID) transformation)

Transformed 100 jbc graph edges to a weighted ITS with 100 rules.
Filtered conditions with variables that do not depend on the variables on the lhs or rhs without taking transitive dependencies into account.
Did no encode lower bounds for putfield and astore.

(14) Obligation:

IntTrs with 100 rules
Start term: main_Load_1(#0, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_Load_1(o1, env, static) -{0,0}> main_Load_3(o1, env, static) :|: 0 < o1
main_Load_3(o1, env, static) -{0,0}> langle_clinit_rangle_ConstantStackPush_5(o1, env, static) :|: 0 < o1
langle_clinit_rangle_ConstantStackPush_5(o1, env, static) -{1,1}> langle_clinit_rangle_ArrayCreate_9(iconst_0, o1, env, static) :|: iconst_0 = 0 && 0 < o1
langle_clinit_rangle_ArrayCreate_9(iconst_0, o1, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_10(a2, o1, iconst_0, env, static) :|: a2 = 2 && iconst_0 = 0 && 0 < a2 && 0 < o1
langle_clinit_rangle_FieldAccess_10(a2, o1, iconst_0, env, static) -{1,1}> langle_clinit_rangle_New_13(o1, env, static') :|: 0 <= a2 && iconst_0 = 0 && static' <= static + a2 && 0 <= static && 0 < a2 && 0 < o1
langle_clinit_rangle_New_13(o1, env, static) -{0,0}> langle_clinit_rangle_New_15(o1, env, static) :|: 0 < o1
langle_clinit_rangle_New_15(o1, env, static) -{0,0}> langle_clinit_rangle_New_16(o1, env, static) :|: 0 <= static && 0 < o1
langle_clinit_rangle_New_16(o1, env, static) -{1,1}> langle_clinit_rangle_Duplicate_18(o4, o1, env, static) :|: o4 = 1 && 0 < o4 && 0 < o1
langle_clinit_rangle_Duplicate_18(o4, o1, env, static) -{1,1}> langle_clinit_rangle_ConstantStackPush_20(o4, o1, env, static) :|: 0 < o4 && 0 < o1
langle_clinit_rangle_ConstantStackPush_20(o4, o1, env, static) -{1,1}> langle_clinit_rangle_InvokeMethod_22(o4, NULL, o1, env, static) :|: NULL = 0 && 0 < o4 && 0 < o1
langle_clinit_rangle_InvokeMethod_22(o4, NULL, o1, env, static) -{1,1}> langle_init_rangle_Load_24(o4, o1, env, static) :|: NULL = 0 && 0 < o4 && 0 < o1
langle_init_rangle_Load_24(o4, o1, env, static) -{1,1}> langle_init_rangle_InvokeMethod_25(o4, o1, env, static) :|: 0 < o4 && 0 < o1
langle_init_rangle_InvokeMethod_25(o4, o1, env, static) -{1,1}> langle_init_rangle_Load_27(o4, o1, env, static) :|: 0 < o4 && 0 < o1
langle_init_rangle_Load_27(o4, o1, env, static) -{1,1}> langle_init_rangle_InvokeMethod_30(o4, o1, env, static) :|: 0 < o4 && 0 < o1
langle_init_rangle_InvokeMethod_30(o4, o1, env, static) -{1,1}> langle_init_rangle_Return_32(o4, o1, env, static) :|: 0 < o4 && 0 < o1
langle_init_rangle_Return_32(o4, o1, env, static) -{1,1}> langle_init_rangle_Return_35(o4, o1, env, static) :|: 0 < o4 && 0 < o1
langle_init_rangle_Return_35(o4, o1, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_37(o4, o1, env, static) :|: 0 < o4 && 0 < o1
langle_clinit_rangle_FieldAccess_37(o4, o1, env, static) -{1,1}> langle_clinit_rangle_Return_40(o1, env, static') :|: 0 <= o4 && 0 < o4 && 0 <= static && 0 < o1 && static' <= static + o4
langle_clinit_rangle_Return_40(o1, env, static) -{1,1}> main_Load_41(o1, env, static) :|: 0 < o1
main_Load_41(o1, env, static) -{0,0}> main_Load_42(o1, env, static) :|: 0 < o1
main_Load_42(o1, env, static) -{0,0}> main_Load_43(o1, env, static) :|: 0 <= static && 0 < o1
main_Load_43(o1, env, static) -{0,0}> main_Load_45(o1, env, static) :|: 0 < o1
main_Load_45(o1, env, static) -{0,0}> main_Load_47(o1, env, static) :|: 0 < o1
main_Load_47(o1, env, static) -{1,1}> main_ArrayLength_51(o1, env, static) :|: 0 < o1
main_ArrayLength_51(a6, env, static) -{0,0}> main_ArrayLength_52(a6, i4, env, static) :|: 0 <= i4 && 0 < a6 && i4 < a6
main_ArrayLength_52(a6, i4, env, static) -{1,1}> main_Load_54(a6, i4, env, static) :|: 0 <= i4 && 0 < a6
main_Load_54(a6, i4, env, static) -{1,1}> main_ArrayLength_56(a6, i4, env, static) :|: 0 <= i4 && 0 < a6
main_ArrayLength_56(a6, i4, env, static) -{1,1}> main_ConstantStackPush_58(a6, i4, env, static) :|: 0 <= i4 && 0 < a6
main_ConstantStackPush_58(a6, i4, env, static) -{1,1}> main_IntArithmetic_60(a6, i4, iconst_5, env, static) :|: iconst_5 = 5 && 0 <= i4 && 0 < a6
main_IntArithmetic_60(a6, i4, iconst_5, env, static) -{1,1}> main_Load_62(a6, i4, i6, env, static) :|: iconst_5 = 5 && 0 <= i6 && 0 <= i4 && i6 <= 4 && 0 < a6 && i4 % iconst_5 = i6
main_Load_62(a6, i4, i6, env, static) -{1,1}> main_ArrayLength_64(a6, i4, i6, env, static) :|: 0 <= i6 && 0 <= i4 && i6 <= 4 && 0 < a6
main_ArrayLength_64(a6, i4, i6, env, static) -{1,1}> main_ConstantStackPush_66(a6, i4, i6, env, static) :|: 0 <= i6 && 0 <= i4 && i6 <= 4 && 0 < a6
main_ConstantStackPush_66(a6, i4, i6, env, static) -{1,1}> main_IntArithmetic_68(a6, i4, i6, iconst_4, env, static) :|: 0 <= i6 && iconst_4 = 4 && 0 <= i4 && i6 <= 4 && 0 < a6
main_IntArithmetic_68(a6, i4, i6, iconst_4, env, static) -{1,1}> main_InvokeMethod_70(a6, i4, i6, i8, env, static) :|: 0 <= i6 && i8 <= 3 && iconst_4 = 4 && i4 % iconst_4 = i8 && 0 <= i4 && i6 <= 4 && 0 < a6 && 0 <= i8
main_InvokeMethod_70(a6, i4, i6, i8, env, static) -{1,1}> iter_Load_72(i4, i6, i8, a6, env, static) :|: 0 <= i6 && i8 <= 3 && 0 <= i4 && i6 <= 4 && 0 < a6 && 0 <= i8
iter_Load_72(i4, i6, i8, a6, env, static) -{0,0}> iter_Load_577(i4, i6, i8, a6, i4, env, static) :|: 0 <= i6 && i8 <= 3 && -1 <= i6 && 0 <= i4 && -1 <= i4 && i6 <= 4 && 0 < a6 && 0 <= i8
iter_Load_577(i249, i250, i8, a110, i69, env, static) -{0,0}> iter_Load_710(i249, i250, i8, a110, i69, env, static) :|: i8 <= 3 && 0 < a110 && -1 <= i250 && -1 <= i249 && -1 <= i8 && 0 <= i8 && 0 <= i69
iter_Load_710(i301, i302, i303, a131, i69, env, static) -{0,0}> iter_Load_762(i301, i302, i303, a131, i69, env, static) :|: i303 <= 3 && -1 <= i302 && -2 <= i302 && 0 <= i69 && -1 <= i303 && -1 <= i301 && 0 < a131
iter_Load_762(i326, i327, i303, a139, i69, env, static) -{0,0}> iter_Load_796(i326, i327, i303, a139, i69, env, static) :|: -1 <= i326 && i303 <= 3 && 0 <= i69 && -1 <= i303 && -2 <= i327 && 0 < a139
iter_Load_796(i342, i327, i303, a145, i69, env, static) -{0,0}> iter_Load_899(i342, i327, i303, a145, i69, env, static) :|: i303 <= 3 && -2 <= i303 && 0 < a145 && 0 <= i69 && -1 <= i303 && -2 <= i327
iter_Load_899(i380, i381, i382, a164, i69, env, static) -{0,0}> iter_Load_1043(i380, i381, i382, a164, i69, env, static) :|: -2 <= i381 && i382 <= 3 && 0 < a164 && -2 <= i382 && 0 <= i69
iter_Load_1043(i426, i427, i382, a176, i69, env, static) -{0,0}> iter_Load_1320(i426, i427, i382, a176, i69, env, static) :|: 0 < a176 && i382 <= 3 && -2 <= i382 && 0 <= i69
iter_Load_1320(i522, i523, i524, a208, i69, env, static) -{1,1}> iter_Load_1321(i522, i523, i524, a208, i69, env, static) :|: 0 <= i69 && 0 < a208
iter_Load_1321(i522, i523, i524, a208, i69, env, static) -{1,1}> iter_IntArithmetic_1324(i522, i523, i524, a208, i69, env, static) :|: 0 <= i69 && 0 < a208
iter_IntArithmetic_1324(i522, i523, i524, a208, i69, env, static) -{1,1}> iter_ConstantStackPush_1327(i538, i522, i523, i524, a208, i69, env, static) :|: i522 + i523 = i538 && 0 <= i69 && 0 < a208
iter_ConstantStackPush_1327(i538, i522, i523, i524, a208, i69, env, static) -{1,1}> iter_Load_1329(i538, iconst_3, i522, i523, i524, a208, i69, env, static) :|: iconst_3 = 3 && 0 <= i69 && 0 < a208
iter_Load_1329(i538, iconst_3, i522, i523, i524, a208, i69, env, static) -{1,1}> iter_IntArithmetic_1330(i538, iconst_3, i524, i522, i523, a208, i69, env, static) :|: iconst_3 = 3 && 0 <= i69 && 0 < a208
iter_IntArithmetic_1330(i538, iconst_3, i524, i522, i523, a208, i69, env, static) -{1,1}> iter_IntArithmetic_1332(i538, i540, i522, i523, i524, a208, i69, env, static) :|: iconst_3 * i524 = i540 && iconst_3 = 3 && 0 <= i69 && 0 < a208
iter_IntArithmetic_1332(i538, i540, i522, i523, i524, a208, i69, env, static) -{1,1}> iter_LT_1335(i541, i522, i523, i524, a208, i69, env, static) :|: i538 + i540 = i541 && 0 <= i69 && 0 < a208
iter_LT_1335(i547, i522, i523, i524, a208, i69, env, static) -{0,0}> iter_LT_1336(i547, i522, i523, i524, a208, i69, env, static) :|: 0 <= i69 && i547 <= -1 && 0 < a208
iter_LT_1335(i548, i522, i523, i524, a208, i69, env, static) -{0,0}> iter_LT_1337(i548, i522, i523, i524, a208, i69, env, static) :|: 0 <= i548 && 0 <= i69 && 0 < a208
iter_LT_1337(i548, i522, i523, i524, a208, i69, env, static) -{1,1}> iter_Load_1340(i522, i523, i524, a208, i69, env, static) :|: 0 <= i548 && 0 <= i69 && 0 < a208
iter_Load_1340(i522, i523, i524, a208, i69, env, static) -{1,1}> iter_Load_1342(i522, i523, i524, a208, i69, env, static) :|: 0 <= i69 && 0 < a208
iter_Load_1342(i522, i523, i524, a208, i69, env, static) -{1,1}> iter_LE_1349(i522, i523, i524, a208, i69, env, static) :|: 0 <= i69 && 0 < a208
iter_LE_1349(i522, i523, i524, a208, i69, env, static) -{0,0}> iter_LE_1354(i522, i523, i524, a208, i69, env, static) :|: i522 <= i523 && 0 <= i69 && 0 < a208
iter_LE_1349(i522, i523, i524, a208, i69, env, static) -{0,0}> iter_LE_1355(i522, i523, i524, a208, i69, env, static) :|: i523 < i522 && 0 <= i69 && 0 < a208
iter_LE_1354(i522, i523, i524, a208, i69, env, static) -{1,1}> iter_Load_1363(i522, i523, i524, a208, i69, env, static) :|: i522 <= i523 && 0 <= i69 && 0 < a208
iter_LE_1355(i522, i523, i524, a208, i69, env, static) -{1,1}> iter_Inc_1364(i522, i523, i524, a208, i69, env, static) :|: i523 < i522 && 0 <= i69 && 0 < a208
iter_Load_1363(i522, i523, i524, a208, i69, env, static) -{1,1}> iter_Load_1365(i523, i522, i524, a208, i69, env, static) :|: 0 <= i69 && 0 < a208
iter_Inc_1364(i522, i523, i524, a208, i69, env, static) -{1,1}> iter_JMP_1366(i551, i523, i524, a208, i69, env, static) :|: i522 + -1 = i551 && 0 <= i69 && 0 < a208
iter_Load_1365(i523, i522, i524, a208, i69, env, static) -{1,1}> iter_LE_1378(i523, i524, i522, a208, i69, env, static) :|: 0 <= i69 && 0 < a208
iter_JMP_1366(i551, i523, i524, a208, i69, env, static) -{1,1}> iter_Load_1395(i551, i523, i524, a208, i69, env, static) :|: 0 <= i69 && 0 < a208
iter_LE_1378(i523, i524, i522, a208, i69, env, static) -{0,0}> iter_LE_1404(i523, i524, i522, a208, i69, env, static) :|: 0 <= i69 && i523 <= i524 && 0 < a208
iter_LE_1378(i523, i524, i522, a208, i69, env, static) -{0,0}> iter_LE_1405(i523, i524, i522, a208, i69, env, static) :|: 0 <= i69 && i524 < i523 && 0 < a208
iter_Load_1395(i551, i523, i524, a208, i69, env, static) -{1,1}> iter_Load_1407(i551, i523, i524, a208, i69, env, static) :|: 0 <= i69 && 0 < a208
iter_LE_1404(i523, i524, i522, a208, i69, env, static) -{1,1}> iter_Load_1408(i522, i523, i524, a208, i69, env, static) :|: 0 <= i69 && i523 <= i524 && 0 < a208
iter_LE_1405(i523, i524, i522, a208, i69, env, static) -{1,1}> iter_Inc_1409(i522, i523, i524, a208, i69, env, static) :|: 0 <= i69 && i524 < i523 && 0 < a208
iter_Load_1407(i551, i523, i524, a208, i69, env, static) -{1,1}> iter_IntArithmetic_1414(i551, i523, i524, a208, i69, env, static) :|: 0 <= i69 && 0 < a208
iter_Load_1408(i522, i523, i524, a208, i69, env, static) -{1,1}> iter_Load_1415(i523, i522, i524, a208, i69, env, static) :|: 0 <= i69 && 0 < a208
iter_Inc_1409(i522, i523, i524, a208, i69, env, static) -{1,1}> iter_Inc_1417(i561, i523, i524, a208, i69, env, static) :|: 0 <= i69 && i522 + 1 = i561 && 0 < a208
iter_IntArithmetic_1414(i551, i523, i524, a208, i69, env, static) -{1,1}> iter_ConstantStackPush_1421(i562, i551, i523, i524, a208, i69, env, static) :|: i551 + i523 = i562 && 0 <= i69 && 0 < a208
iter_Load_1415(i523, i522, i524, a208, i69, env, static) -{1,1}> iter_GT_1423(i523, i524, i522, a208, i69, env, static) :|: 0 <= i69 && 0 < a208
iter_Inc_1417(i561, i523, i524, a208, i69, env, static) -{1,1}> iter_JMP_1425(i561, i566, i524, a208, i69, env, static) :|: i523 + -2 = i566 && 0 <= i69 && 0 < a208
iter_ConstantStackPush_1421(i562, i551, i523, i524, a208, i69, env, static) -{0,0}> iter_ConstantStackPush_1327(i562, i551, i523, i524, a208, i69, env, static) :|: 0 <= i69 && 0 < a208
iter_GT_1423(i523, i524, i522, a208, i69, env, static) -{0,0}> iter_GT_1429(i523, i524, i522, a208, i69, env, static) :|: 0 <= i69 && i523 <= i524 && 0 < a208
iter_JMP_1425(i561, i566, i524, a208, i69, env, static) -{1,1}> iter_Load_1435(i561, i566, i524, a208, i69, env, static) :|: 0 <= i69 && 0 < a208
iter_GT_1429(i523, i524, i522, a208, i69, env, static) -{1,1}> iter_Load_1436(i522, i523, i524, a208, i69, env, static) :|: 0 <= i69 && i523 <= i524 && 0 < a208
iter_Load_1435(i561, i566, i524, a208, i69, env, static) -{0,0}> iter_Load_1320(i561, i566, i524, a208, i69, env, static) :|: 0 <= i69 && 0 < a208
iter_Load_1436(i522, i523, i524, a208, i69, env, static) -{1,1}> iter_ConstantStackPush_1437(i522, i523, i524, a208, i69, env, static) :|: 0 <= i69 && 0 < a208
iter_ConstantStackPush_1437(i522, i523, i524, a208, i69, env, static) -{1,1}> iter_InvokeMethod_1438(i522, iconst_1, i523, i524, a208, i69, env, static) :|: iconst_1 = 1 && 0 <= i69 && 0 < a208
iter_InvokeMethod_1438(i522, iconst_1, i523, i524, a208, i69, env, static) -{1,1}> add_Load_1439(i522, iconst_1, i523, i524, a208, i69, env, static) :|: iconst_1 = 1 && 0 <= i69 && 0 < a208
add_Load_1439(i522, iconst_1, i523, i524, a208, i69, env, static) -{1,1}> add_Load_1440(i522, iconst_1, i523, i524, a208, i69, env, static) :|: iconst_1 = 1 && 0 <= i69 && 0 < a208
add_Load_1440(i522, iconst_1, i523, i524, a208, i69, env, static) -{1,1}> add_IntArithmetic_1441(i522, iconst_1, i523, i524, a208, i69, env, static) :|: iconst_1 = 1 && 0 <= i69 && 0 < a208
add_IntArithmetic_1441(i522, iconst_1, i523, i524, a208, i69, env, static) -{1,1}> add_Return_1442(i571, i523, i524, a208, i69, env, static) :|: i522 + iconst_1 = i571 && iconst_1 = 1 && 0 <= i69 && 0 < a208
add_Return_1442(i571, i523, i524, a208, i69, env, static) -{1,1}> iter_Store_1443(i571, i523, i524, a208, i69, env, static) :|: 0 <= i69 && 0 < a208
iter_Store_1443(i571, i523, i524, a208, i69, env, static) -{1,1}> iter_Load_1444(i571, i523, i524, a208, i69, env, static) :|: 0 <= i69 && 0 < a208
iter_Load_1444(i571, i523, i524, a208, i69, env, static) -{1,1}> iter_ConstantStackPush_1445(i523, i571, i524, a208, i69, env, static) :|: 0 <= i69 && 0 < a208
iter_ConstantStackPush_1445(i523, i571, i524, a208, i69, env, static) -{1,1}> iter_InvokeMethod_1446(i523, iconst_1, i571, i524, a208, i69, env, static) :|: iconst_1 = 1 && 0 <= i69 && 0 < a208
iter_InvokeMethod_1446(i523, iconst_1, i571, i524, a208, i69, env, static) -{1,1}> add_Load_1447(i523, iconst_1, i571, i524, a208, i69, env, static) :|: iconst_1 = 1 && 0 <= i69 && 0 < a208
add_Load_1447(i523, iconst_1, i571, i524, a208, i69, env, static) -{1,1}> add_Load_1448(i523, iconst_1, i571, i524, a208, i69, env, static) :|: iconst_1 = 1 && 0 <= i69 && 0 < a208
add_Load_1448(i523, iconst_1, i571, i524, a208, i69, env, static) -{1,1}> add_IntArithmetic_1449(i523, iconst_1, i571, i524, a208, i69, env, static) :|: iconst_1 = 1 && 0 <= i69 && 0 < a208
add_IntArithmetic_1449(i523, iconst_1, i571, i524, a208, i69, env, static) -{1,1}> add_Return_1450(i578, i571, i524, a208, i69, env, static) :|: iconst_1 = 1 && i523 + iconst_1 = i578 && 0 <= i69 && 0 < a208
add_Return_1450(i578, i571, i524, a208, i69, env, static) -{1,1}> iter_Store_1451(i578, i571, i524, a208, i69, env, static) :|: 0 <= i69 && 0 < a208
iter_Store_1451(i578, i571, i524, a208, i69, env, static) -{1,1}> iter_Load_1452(i571, i578, i524, a208, i69, env, static) :|: 0 <= i69 && 0 < a208
iter_Load_1452(i571, i578, i524, a208, i69, env, static) -{1,1}> iter_ConstantStackPush_1453(i524, i571, i578, a208, i69, env, static) :|: 0 <= i69 && 0 < a208
iter_ConstantStackPush_1453(i524, i571, i578, a208, i69, env, static) -{1,1}> iter_IntArithmetic_1454(i524, iconst_1, i571, i578, a208, i69, env, static) :|: iconst_1 = 1 && 0 <= i69 && 0 < a208
iter_IntArithmetic_1454(i524, iconst_1, i571, i578, a208, i69, env, static) -{1,1}> iter_Store_1455(i582, i571, i578, a208, i69, env, static) :|: iconst_1 = 1 && 0 <= i69 && i524 - iconst_1 = i582 && 0 < a208
iter_Store_1455(i582, i571, i578, a208, i69, env, static) -{1,1}> iter_JMP_1456(i571, i578, i582, a208, i69, env, static) :|: 0 <= i69 && 0 < a208
iter_JMP_1456(i571, i578, i582, a208, i69, env, static) -{1,1}> iter_Load_1457(i571, i578, i582, a208, i69, env, static) :|: 0 <= i69 && 0 < a208
iter_Load_1457(i571, i578, i582, a208, i69, env, static) -{0,0}> iter_Load_1320(i571, i578, i582, a208, i69, env, static) :|: 0 <= i69 && 0 < a208

(15) StraightLineCodeCompressionProof (BOTH CONCRETE BOUNDS(ID, ID) transformation)

obtained
main_Load_1(o1, env, static) -{26,26}> iter_Load_1320(i4', i6', i8', o1, i4', env, static'1) :|: i4' % 5 = i6' && 0 <= i4' && static'1 <= static''' + 1 && -2 <= i8' && -1 <= i8' && 0 < o1 && i8' <= 3 && 0 <= 2 && i6' <= 4 && static''' <= static + 2 && 0 <= static && -1 <= i6' && i4' % 4 = i8' && 0 <= static''' && 0 <= i6' && 0 < 2 && -1 <= i4' && 0 <= 1 && -2 <= i6' && 0 < 1 && 0 <= i8' && 0 <= static'1 && i4' < o1
by chaining
main_Load_1(o1, env, static) -{0,0}> main_Load_3(o1, env, static) :|: 0 < o1
main_Load_3(o1, env, static) -{0,0}> langle_clinit_rangle_ConstantStackPush_5(o1, env, static) :|: 0 < o1
langle_clinit_rangle_ConstantStackPush_5(o1, env, static) -{1,1}> langle_clinit_rangle_ArrayCreate_9(iconst_0, o1, env, static) :|: iconst_0 = 0 && 0 < o1
langle_clinit_rangle_ArrayCreate_9(iconst_0, o1, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_10(a2, o1, iconst_0, env, static) :|: a2 = 2 && iconst_0 = 0 && 0 < a2 && 0 < o1
langle_clinit_rangle_FieldAccess_10(a2, o1, iconst_0, env, static) -{1,1}> langle_clinit_rangle_New_13(o1, env, static') :|: 0 <= a2 && iconst_0 = 0 && static' <= static + a2 && 0 <= static && 0 < a2 && 0 < o1
langle_clinit_rangle_New_13(o1, env, static) -{0,0}> langle_clinit_rangle_New_15(o1, env, static) :|: 0 < o1
langle_clinit_rangle_New_15(o1, env, static) -{0,0}> langle_clinit_rangle_New_16(o1, env, static) :|: 0 <= static && 0 < o1
langle_clinit_rangle_New_16(o1, env, static) -{1,1}> langle_clinit_rangle_Duplicate_18(o4, o1, env, static) :|: o4 = 1 && 0 < o4 && 0 < o1
langle_clinit_rangle_Duplicate_18(o4, o1, env, static) -{1,1}> langle_clinit_rangle_ConstantStackPush_20(o4, o1, env, static) :|: 0 < o4 && 0 < o1
langle_clinit_rangle_ConstantStackPush_20(o4, o1, env, static) -{1,1}> langle_clinit_rangle_InvokeMethod_22(o4, NULL, o1, env, static) :|: NULL = 0 && 0 < o4 && 0 < o1
langle_clinit_rangle_InvokeMethod_22(o4, NULL, o1, env, static) -{1,1}> langle_init_rangle_Load_24(o4, o1, env, static) :|: NULL = 0 && 0 < o4 && 0 < o1
langle_init_rangle_Load_24(o4, o1, env, static) -{1,1}> langle_init_rangle_InvokeMethod_25(o4, o1, env, static) :|: 0 < o4 && 0 < o1
langle_init_rangle_InvokeMethod_25(o4, o1, env, static) -{1,1}> langle_init_rangle_Load_27(o4, o1, env, static) :|: 0 < o4 && 0 < o1
langle_init_rangle_Load_27(o4, o1, env, static) -{1,1}> langle_init_rangle_InvokeMethod_30(o4, o1, env, static) :|: 0 < o4 && 0 < o1
langle_init_rangle_InvokeMethod_30(o4, o1, env, static) -{1,1}> langle_init_rangle_Return_32(o4, o1, env, static) :|: 0 < o4 && 0 < o1
langle_init_rangle_Return_32(o4, o1, env, static) -{1,1}> langle_init_rangle_Return_35(o4, o1, env, static) :|: 0 < o4 && 0 < o1
langle_init_rangle_Return_35(o4, o1, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_37(o4, o1, env, static) :|: 0 < o4 && 0 < o1
langle_clinit_rangle_FieldAccess_37(o4, o1, env, static) -{1,1}> langle_clinit_rangle_Return_40(o1, env, static') :|: 0 <= o4 && 0 < o4 && 0 <= static && 0 < o1 && static' <= static + o4
langle_clinit_rangle_Return_40(o1, env, static) -{1,1}> main_Load_41(o1, env, static) :|: 0 < o1
main_Load_41(o1, env, static) -{0,0}> main_Load_42(o1, env, static) :|: 0 < o1
main_Load_42(o1, env, static) -{0,0}> main_Load_43(o1, env, static) :|: 0 <= static && 0 < o1
main_Load_43(o1, env, static) -{0,0}> main_Load_45(o1, env, static) :|: 0 < o1
main_Load_45(o1, env, static) -{0,0}> main_Load_47(o1, env, static) :|: 0 < o1
main_Load_47(o1, env, static) -{1,1}> main_ArrayLength_51(o1, env, static) :|: 0 < o1
main_ArrayLength_51(a6, env, static) -{0,0}> main_ArrayLength_52(a6, i4, env, static) :|: 0 <= i4 && 0 < a6 && i4 < a6
main_ArrayLength_52(a6, i4, env, static) -{1,1}> main_Load_54(a6, i4, env, static) :|: 0 <= i4 && 0 < a6
main_Load_54(a6, i4, env, static) -{1,1}> main_ArrayLength_56(a6, i4, env, static) :|: 0 <= i4 && 0 < a6
main_ArrayLength_56(a6, i4, env, static) -{1,1}> main_ConstantStackPush_58(a6, i4, env, static) :|: 0 <= i4 && 0 < a6
main_ConstantStackPush_58(a6, i4, env, static) -{1,1}> main_IntArithmetic_60(a6, i4, iconst_5, env, static) :|: iconst_5 = 5 && 0 <= i4 && 0 < a6
main_IntArithmetic_60(a6, i4, iconst_5, env, static) -{1,1}> main_Load_62(a6, i4, i6, env, static) :|: iconst_5 = 5 && 0 <= i6 && 0 <= i4 && i6 <= 4 && 0 < a6 && i4 % iconst_5 = i6
main_Load_62(a6, i4, i6, env, static) -{1,1}> main_ArrayLength_64(a6, i4, i6, env, static) :|: 0 <= i6 && 0 <= i4 && i6 <= 4 && 0 < a6
main_ArrayLength_64(a6, i4, i6, env, static) -{1,1}> main_ConstantStackPush_66(a6, i4, i6, env, static) :|: 0 <= i6 && 0 <= i4 && i6 <= 4 && 0 < a6
main_ConstantStackPush_66(a6, i4, i6, env, static) -{1,1}> main_IntArithmetic_68(a6, i4, i6, iconst_4, env, static) :|: 0 <= i6 && iconst_4 = 4 && 0 <= i4 && i6 <= 4 && 0 < a6
main_IntArithmetic_68(a6, i4, i6, iconst_4, env, static) -{1,1}> main_InvokeMethod_70(a6, i4, i6, i8, env, static) :|: 0 <= i6 && i8 <= 3 && iconst_4 = 4 && i4 % iconst_4 = i8 && 0 <= i4 && i6 <= 4 && 0 < a6 && 0 <= i8
main_InvokeMethod_70(a6, i4, i6, i8, env, static) -{1,1}> iter_Load_72(i4, i6, i8, a6, env, static) :|: 0 <= i6 && i8 <= 3 && 0 <= i4 && i6 <= 4 && 0 < a6 && 0 <= i8
iter_Load_72(i4, i6, i8, a6, env, static) -{0,0}> iter_Load_577(i4, i6, i8, a6, i4, env, static) :|: 0 <= i6 && i8 <= 3 && -1 <= i6 && 0 <= i4 && -1 <= i4 && i6 <= 4 && 0 < a6 && 0 <= i8
iter_Load_577(i249, i250, i8, a110, i69, env, static) -{0,0}> iter_Load_710(i249, i250, i8, a110, i69, env, static) :|: i8 <= 3 && 0 < a110 && -1 <= i250 && -1 <= i249 && -1 <= i8 && 0 <= i8 && 0 <= i69
iter_Load_710(i301, i302, i303, a131, i69, env, static) -{0,0}> iter_Load_762(i301, i302, i303, a131, i69, env, static) :|: i303 <= 3 && -1 <= i302 && -2 <= i302 && 0 <= i69 && -1 <= i303 && -1 <= i301 && 0 < a131
iter_Load_762(i326, i327, i303, a139, i69, env, static) -{0,0}> iter_Load_796(i326, i327, i303, a139, i69, env, static) :|: -1 <= i326 && i303 <= 3 && 0 <= i69 && -1 <= i303 && -2 <= i327 && 0 < a139
iter_Load_796(i342, i327, i303, a145, i69, env, static) -{0,0}> iter_Load_899(i342, i327, i303, a145, i69, env, static) :|: i303 <= 3 && -2 <= i303 && 0 < a145 && 0 <= i69 && -1 <= i303 && -2 <= i327
iter_Load_899(i380, i381, i382, a164, i69, env, static) -{0,0}> iter_Load_1043(i380, i381, i382, a164, i69, env, static) :|: -2 <= i381 && i382 <= 3 && 0 < a164 && -2 <= i382 && 0 <= i69
iter_Load_1043(i426, i427, i382, a176, i69, env, static) -{0,0}> iter_Load_1320(i426, i427, i382, a176, i69, env, static) :|: 0 < a176 && i382 <= 3 && -2 <= i382 && 0 <= i69

(16) Obligation:

IntTrs with 9 rules
Start term: main_Load_1(#0, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_Load_1(o1, env, static) -{26,26}> iter_Load_1320(i4', i6', i8', o1, i4', env, static'1) :|: i4' % 5 = i6' && 0 <= i4' && static'1 <= static''' + 1 && -2 <= i8' && -1 <= i8' && 0 < o1 && i8' <= 3 && 0 <= 2 && i6' <= 4 && static''' <= static + 2 && 0 <= static && -1 <= i6' && i4' % 4 = i8' && 0 <= static''' && 0 <= i6' && 0 < 2 && -1 <= i4' && 0 <= 1 && -2 <= i6' && 0 < 1 && 0 <= i8' && 0 <= static'1 && i4' < o1
iter_Load_1320(i522, i523, i524, a208, i69, env, static) -{3,3}> iter_ConstantStackPush_1327(i538', i522, i523, i524, a208, i69, env, static) :|: 0 <= i69 && 0 < a208 && i522 + i523 = i538'
iter_ConstantStackPush_1327(i538, i522, i523, i524, a208, i69, env, static) -{4,4}> iter_LT_1335(i541', i522, i523, i524, a208, i69, env, static) :|: 3 * i524 = i540' && 0 < a208 && 0 <= i69 && i538 + i540' = i541'
iter_LT_1335(i547, i522, i523, i524, a208, i69, env, static) -{0,0}> iter_LT_1336(i547, i522, i523, i524, a208, i69, env, static) :|: 0 <= i69 && i547 <= -1 && 0 < a208
iter_LT_1335(i548, i522, i523, i524, a208, i69, env, static) -{3,3}> iter_LE_1349(i522, i523, i524, a208, i69, env, static) :|: 0 <= i548 && 0 <= i69 && 0 < a208
iter_LE_1349(i522, i523, i524, a208, i69, env, static) -{6,6}> iter_ConstantStackPush_1327(i562', i551', i523, i524, a208, i69, env, static) :|: i522 + -1 = i551' && 0 <= i69 && 0 < a208 && i551' + i523 = i562' && i523 < i522
iter_LE_1349(i522, i523, i524, a208, i69, env, static) -{3,3}> iter_LE_1378(i523, i524, i522, a208, i69, env, static) :|: i522 <= i523 && 0 <= i69 && 0 < a208
iter_LE_1378(i523, i524, i522, a208, i69, env, static) -{4,4}> iter_Load_1320(i561', i566', i524, a208, i69, env, static) :|: i522 + 1 = i561' && 0 <= i69 && 0 < a208 && i523 + -2 = i566' && i524 < i523
iter_LE_1378(i523, i524, i522, a208, i69, env, static) -{25,25}> iter_Load_1320(i571', i578', i582', a208, i69, env, static) :|: i523 <= i524 && 0 <= i69 && 0 < a208 && i522 + 1 = i571' && i524 - 1 = i582' && i523 + 1 = i578'

(17) RemoveDivModProof (CONCRETE UPPER BOUND(ID) transformation)

Removed div and mod.

main_Load_1(o1, env, static) -{26,26}> iter_Load_1320(i4', i6', i8', o1, i4', env, static'1) :|: i4' % 5 = i6' && 0 <= i4' && static'1 <= static''' + 1 && -2 <= i8' && -1 <= i8' && 0 < o1 && i8' <= 3 && 0 <= 2 && i6' <= 4 && static''' <= static + 2 && 0 <= static && -1 <= i6' && i4' % 4 = i8' && 0 <= static''' && 0 <= i6' && 0 < 2 && -1 <= i4' && 0 <= 1 && -2 <= i6' && 0 < 1 && 0 <= i8' && 0 <= static'1 && i4' < o1
was transformed to
main_Load_1'(o1, env, static) -{26,26}> iter_Load_1320(i4', i6', i8', o1, i4', env, static'1) :|: i4' - 4 * div1 < 4 && i4' - 4 * div1 + 4 > 0 && i4' - 5 * div < 5 && i4' - 5 * div + 5 > 0 && i4' - 5 * div = i6' && 0 <= i4' && static'1 <= static''' + 1 && -2 <= i8' && -1 <= i8' && 0 < o1 && i8' <= 3 && 0 <= 2 && i6' <= 4 && static''' <= static + 2 && 0 <= static && -1 <= i6' && i4' - 4 * div1 = i8' && 0 <= static''' && 0 <= i6' && 0 < 2 && -1 <= i4' && 0 <= 1 && -2 <= i6' && 0 < 1 && 0 <= i8' && 0 <= static'1 && i4' < o1
main_Load_1(o1, env, static) -{26,26}> main_Load_1'(o1, env, static) :|: i4' - 5 * div = i6' && 0 <= i4' && static'1 <= static''' + 1 && -2 <= i8' && -1 <= i8' && 0 < o1 && i8' <= 3 && 0 <= 2 && i6' <= 4 && static''' <= static + 2 && 0 <= static && -1 <= i6' && i4' - 4 * div1 = i8' && 0 <= static''' && 0 <= i6' && 0 < 2 && -1 <= i4' && 0 <= 1 && -2 <= i6' && 0 < 1 && 0 <= i8' && 0 <= static'1 && i4' < o1

(18) Obligation:

IntTrs with 10 rules
Start term: main_Load_1(#0, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
iter_LE_1378(i523, i524, i522, a208, i69, env, static) -{4,4}> iter_Load_1320(i561', i566', i524, a208, i69, env, static) :|: i522 + 1 = i561' && 0 <= i69 && 0 < a208 && i523 + -2 = i566' && i524 < i523
iter_Load_1320(i522, i523, i524, a208, i69, env, static) -{3,3}> iter_ConstantStackPush_1327(i538', i522, i523, i524, a208, i69, env, static) :|: 0 <= i69 && 0 < a208 && i522 + i523 = i538'
iter_LE_1349(i522, i523, i524, a208, i69, env, static) -{6,6}> iter_ConstantStackPush_1327(i562', i551', i523, i524, a208, i69, env, static) :|: i522 + -1 = i551' && 0 <= i69 && 0 < a208 && i551' + i523 = i562' && i523 < i522
iter_LE_1378(i523, i524, i522, a208, i69, env, static) -{25,25}> iter_Load_1320(i571', i578', i582', a208, i69, env, static) :|: i523 <= i524 && 0 <= i69 && 0 < a208 && i522 + 1 = i571' && i524 - 1 = i582' && i523 + 1 = i578'
iter_LE_1349(i522, i523, i524, a208, i69, env, static) -{3,3}> iter_LE_1378(i523, i524, i522, a208, i69, env, static) :|: i522 <= i523 && 0 <= i69 && 0 < a208
main_Load_1'(o1, env, static) -{26,26}> iter_Load_1320(i4', i6', i8', o1, i4', env, static'1) :|: i4' - 4 * div1 < 4 && i4' - 4 * div1 + 4 > 0 && i4' - 5 * div < 5 && i4' - 5 * div + 5 > 0 && i4' - 5 * div = i6' && 0 <= i4' && static'1 <= static''' + 1 && -2 <= i8' && -1 <= i8' && 0 < o1 && i8' <= 3 && 0 <= 2 && i6' <= 4 && static''' <= static + 2 && 0 <= static && -1 <= i6' && i4' - 4 * div1 = i8' && 0 <= static''' && 0 <= i6' && 0 < 2 && -1 <= i4' && 0 <= 1 && -2 <= i6' && 0 < 1 && 0 <= i8' && 0 <= static'1 && i4' < o1
iter_LT_1335(i548, i522, i523, i524, a208, i69, env, static) -{3,3}> iter_LE_1349(i522, i523, i524, a208, i69, env, static) :|: 0 <= i548 && 0 <= i69 && 0 < a208
iter_ConstantStackPush_1327(i538, i522, i523, i524, a208, i69, env, static) -{4,4}> iter_LT_1335(i541', i522, i523, i524, a208, i69, env, static) :|: 3 * i524 = i540' && 0 < a208 && 0 <= i69 && i538 + i540' = i541'
main_Load_1(o1, env, static) -{26,26}> main_Load_1'(o1, env, static) :|: i4' - 5 * div = i6' && 0 <= i4' && static'1 <= static''' + 1 && -2 <= i8' && -1 <= i8' && 0 < o1 && i8' <= 3 && 0 <= 2 && i6' <= 4 && static''' <= static + 2 && 0 <= static && -1 <= i6' && i4' - 4 * div1 = i8' && 0 <= static''' && 0 <= i6' && 0 < 2 && -1 <= i4' && 0 <= 1 && -2 <= i6' && 0 < 1 && 0 <= i8' && 0 <= static'1 && i4' < o1
iter_LT_1335(i547, i522, i523, i524, a208, i69, env, static) -{0,0}> iter_LT_1336(i547, i522, i523, i524, a208, i69, env, static) :|: 0 <= i69 && i547 <= -1 && 0 < a208

(19) MovedArithmeticFromConstraintsProof (BOTH CONCRETE BOUNDS(ID, ID) transformation)

Moved arithmethic from constraints to rhss.

main_Load_1'(o1, env, static) -{26,26}> iter_Load_1320(i4', i6', i8', o1, i4', env, static'1) :|: i4' - 4 * div1 < 4 && i4' - 4 * div1 + 4 > 0 && i4' - 5 * div < 5 && i4' - 5 * div + 5 > 0 && i4' - 5 * div = i6' && 0 <= i4' && static'1 <= static''' + 1 && -2 <= i8' && -1 <= i8' && 0 < o1 && i8' <= 3 && 0 <= 2 && i6' <= 4 && static''' <= static + 2 && 0 <= static && -1 <= i6' && i4' - 4 * div1 = i8' && 0 <= static''' && 0 <= i6' && 0 < 2 && -1 <= i4' && 0 <= 1 && -2 <= i6' && 0 < 1 && 0 <= i8' && 0 <= static'1 && i4' < o1
was transformed to
main_Load_1'(o1, env, static) -{26,26}> iter_Load_1320(i4', i4' - 5 * div, i4' - 4 * div1, o1, i4', env, static'1) :|: i4' - 4 * div1 < 4 && i4' - 4 * div1 + 4 > 0 && i4' - 5 * div < 5 && i4' - 5 * div + 5 > 0 && i4' - 5 * div = i6' && 0 <= i4' && static'1 <= static''' + 1 && -2 <= i8' && -1 <= i8' && 0 < o1 && i8' <= 3 && 0 <= 2 && i6' <= 4 && static''' <= static + 2 && 0 <= static && -1 <= i6' && i4' - 4 * div1 = i8' && 0 <= static''' && 0 <= i6' && 0 < 2 && -1 <= i4' && 0 <= 1 && -2 <= i6' && 0 < 1 && 0 <= i8' && 0 <= static'1 && i4' < o1

(20) Obligation:

IntTrs with 10 rules
Start term: main_Load_1(#0, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
iter_LE_1378(i523, i524, i522, a208, i69, env, static) -{4,4}> iter_Load_1320(i522 + 1, i523 + -2, i524, a208, i69, env, static) :|: i522 + 1 = i561' && 0 <= i69 && 0 < a208 && i523 + -2 = i566' && i524 < i523
iter_Load_1320(i522, i523, i524, a208, i69, env, static) -{3,3}> iter_ConstantStackPush_1327(i522 + i523, i522, i523, i524, a208, i69, env, static) :|: 0 <= i69 && 0 < a208 && i522 + i523 = i538'
iter_LE_1349(i522, i523, i524, a208, i69, env, static) -{6,6}> iter_ConstantStackPush_1327(i522 + -1 + i523, i522 + -1, i523, i524, a208, i69, env, static) :|: i522 + -1 = i551' && 0 <= i69 && 0 < a208 && i551' + i523 = i562' && i523 < i522
iter_LE_1378(i523, i524, i522, a208, i69, env, static) -{25,25}> iter_Load_1320(i522 + 1, i523 + 1, i524 - 1, a208, i69, env, static) :|: i523 <= i524 && 0 <= i69 && 0 < a208 && i522 + 1 = i571' && i524 - 1 = i582' && i523 + 1 = i578'
iter_LE_1349(i522, i523, i524, a208, i69, env, static) -{3,3}> iter_LE_1378(i523, i524, i522, a208, i69, env, static) :|: i522 <= i523 && 0 <= i69 && 0 < a208
iter_ConstantStackPush_1327(i538, i522, i523, i524, a208, i69, env, static) -{4,4}> iter_LT_1335(i538 + 3 * i524, i522, i523, i524, a208, i69, env, static) :|: 3 * i524 = i540' && 0 < a208 && 0 <= i69 && i538 + i540' = i541'
iter_LT_1335(i548, i522, i523, i524, a208, i69, env, static) -{3,3}> iter_LE_1349(i522, i523, i524, a208, i69, env, static) :|: 0 <= i548 && 0 <= i69 && 0 < a208
main_Load_1'(o1, env, static) -{26,26}> iter_Load_1320(i4', i4' - 5 * div, i4' - 4 * div1, o1, i4', env, static'1) :|: i4' - 4 * div1 < 4 && i4' - 4 * div1 + 4 > 0 && i4' - 5 * div < 5 && i4' - 5 * div + 5 > 0 && i4' - 5 * div = i6' && 0 <= i4' && static'1 <= static''' + 1 && -2 <= i8' && -1 <= i8' && 0 < o1 && i8' <= 3 && 0 <= 2 && i6' <= 4 && static''' <= static + 2 && 0 <= static && -1 <= i6' && i4' - 4 * div1 = i8' && 0 <= static''' && 0 <= i6' && 0 < 2 && -1 <= i4' && 0 <= 1 && -2 <= i6' && 0 < 1 && 0 <= i8' && 0 <= static'1 && i4' < o1
iter_LT_1335(i547, i522, i523, i524, a208, i69, env, static) -{0,0}> iter_LT_1336(i547, i522, i523, i524, a208, i69, env, static) :|: 0 <= i69 && i547 <= -1 && 0 < a208
main_Load_1(o1, env, static) -{26,26}> main_Load_1'(o1, env, static) :|: i4' - 5 * div = i6' && 0 <= i4' && static'1 <= static''' + 1 && -2 <= i8' && -1 <= i8' && 0 < o1 && i8' <= 3 && 0 <= 2 && i6' <= 4 && static''' <= static + 2 && 0 <= static && -1 <= i6' && i4' - 4 * div1 = i8' && 0 <= static''' && 0 <= i6' && 0 < 2 && -1 <= i4' && 0 <= 1 && -2 <= i6' && 0 < 1 && 0 <= i8' && 0 <= static'1 && i4' < o1

(21) ExpressionSimplificationProof (BOTH CONCRETE BOUNDS(ID, ID) transformation)

Simplified expressions.

main_Load_1'(o1, env, static) -{26,26}> iter_Load_1320(i4', i4' - 5 * div, i4' - 4 * div1, o1, i4', env, static'1) :|: i4' - 4 * div1 < 4 && i4' - 4 * div1 + 4 > 0 && i4' - 5 * div < 5 && i4' - 5 * div + 5 > 0 && i4' - 5 * div = i6' && 0 <= i4' && static'1 <= static''' + 1 && -2 <= i8' && -1 <= i8' && 0 < o1 && i8' <= 3 && 0 <= 2 && i6' <= 4 && static''' <= static + 2 && 0 <= static && -1 <= i6' && i4' - 4 * div1 = i8' && 0 <= static''' && 0 <= i6' && 0 < 2 && -1 <= i4' && 0 <= 1 && -2 <= i6' && 0 < 1 && 0 <= i8' && 0 <= static'1 && i4' < o1
was transformed to
main_Load_1'(o1, env, static) -{26,26}> iter_Load_1320(i4', i4' + -5 * div, i4' + -4 * div1, o1, i4', env, static'1) :|: i4' + -4 * div1 < 4 && 0 < i4' + -4 * div1 + 4 && i4' + -5 * div < 5 && 0 < i4' + -5 * div + 5 && i4' + -5 * div = i6' && 0 <= i4' && static'1 <= static''' + 1 && -2 <= i8' && -1 <= i8' && 0 < o1 && i8' <= 3 && i6' <= 4 && static''' <= static + 2 && 0 <= static && -1 <= i6' && i4' + -4 * div1 = i8' && 0 <= static''' && 0 <= i6' && -1 <= i4' && -2 <= i6' && 0 <= i8' && 0 <= static'1 && i4' < o1

main_Load_1(o1, env, static) -{26,26}> main_Load_1'(o1, env, static) :|: i4' - 5 * div = i6' && 0 <= i4' && static'1 <= static''' + 1 && -2 <= i8' && -1 <= i8' && 0 < o1 && i8' <= 3 && 0 <= 2 && i6' <= 4 && static''' <= static + 2 && 0 <= static && -1 <= i6' && i4' - 4 * div1 = i8' && 0 <= static''' && 0 <= i6' && 0 < 2 && -1 <= i4' && 0 <= 1 && -2 <= i6' && 0 < 1 && 0 <= i8' && 0 <= static'1 && i4' < o1
was transformed to
main_Load_1(o1, env, static) -{26,26}> main_Load_1'(o1, env, static) :|: i4' + -5 * div = i6' && 0 <= i4' && static'1 <= static''' + 1 && -2 <= i8' && -1 <= i8' && 0 < o1 && i8' <= 3 && i6' <= 4 && static''' <= static + 2 && 0 <= static && -1 <= i6' && i4' + -4 * div1 = i8' && 0 <= static''' && 0 <= i6' && -1 <= i4' && -2 <= i6' && 0 <= i8' && 0 <= static'1 && i4' < o1

(22) Obligation:

IntTrs with 10 rules
Start term: main_Load_1(#0, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_Load_1(o1, env, static) -{26,26}> main_Load_1'(o1, env, static) :|: i4' + -5 * div = i6' && 0 <= i4' && static'1 <= static''' + 1 && -2 <= i8' && -1 <= i8' && 0 < o1 && i8' <= 3 && i6' <= 4 && static''' <= static + 2 && 0 <= static && -1 <= i6' && i4' + -4 * div1 = i8' && 0 <= static''' && 0 <= i6' && -1 <= i4' && -2 <= i6' && 0 <= i8' && 0 <= static'1 && i4' < o1
iter_LE_1378(i523, i524, i522, a208, i69, env, static) -{25,25}> iter_Load_1320(i522 + 1, i523 + 1, i524 - 1, a208, i69, env, static) :|: i523 <= i524 && 0 <= i69 && 0 < a208 && i522 + 1 = i571' && i524 - 1 = i582' && i523 + 1 = i578'
iter_ConstantStackPush_1327(i538, i522, i523, i524, a208, i69, env, static) -{4,4}> iter_LT_1335(i538 + 3 * i524, i522, i523, i524, a208, i69, env, static) :|: 3 * i524 = i540' && 0 < a208 && 0 <= i69 && i538 + i540' = i541'
iter_LE_1378(i523, i524, i522, a208, i69, env, static) -{4,4}> iter_Load_1320(i522 + 1, i523 - 2, i524, a208, i69, env, static) :|: i522 + 1 = i561' && 0 <= i69 && 0 < a208 && i523 - 2 = i566' && i524 < i523
iter_LE_1349(i522, i523, i524, a208, i69, env, static) -{6,6}> iter_ConstantStackPush_1327(i522 - 1 + i523, i522 - 1, i523, i524, a208, i69, env, static) :|: i522 - 1 = i551' && 0 <= i69 && 0 < a208 && i551' + i523 = i562' && i523 < i522
iter_Load_1320(i522, i523, i524, a208, i69, env, static) -{3,3}> iter_ConstantStackPush_1327(i522 + i523, i522, i523, i524, a208, i69, env, static) :|: 0 <= i69 && 0 < a208 && i522 + i523 = i538'
main_Load_1'(o1, env, static) -{26,26}> iter_Load_1320(i4', i4' + -5 * div, i4' + -4 * div1, o1, i4', env, static'1) :|: i4' + -4 * div1 < 4 && 0 < i4' + -4 * div1 + 4 && i4' + -5 * div < 5 && 0 < i4' + -5 * div + 5 && i4' + -5 * div = i6' && 0 <= i4' && static'1 <= static''' + 1 && -2 <= i8' && -1 <= i8' && 0 < o1 && i8' <= 3 && i6' <= 4 && static''' <= static + 2 && 0 <= static && -1 <= i6' && i4' + -4 * div1 = i8' && 0 <= static''' && 0 <= i6' && -1 <= i4' && -2 <= i6' && 0 <= i8' && 0 <= static'1 && i4' < o1
iter_LE_1349(i522, i523, i524, a208, i69, env, static) -{3,3}> iter_LE_1378(i523, i524, i522, a208, i69, env, static) :|: i522 <= i523 && 0 <= i69 && 0 < a208
iter_LT_1335(i548, i522, i523, i524, a208, i69, env, static) -{3,3}> iter_LE_1349(i522, i523, i524, a208, i69, env, static) :|: 0 <= i548 && 0 <= i69 && 0 < a208
iter_LT_1335(i547, i522, i523, i524, a208, i69, env, static) -{0,0}> iter_LT_1336(i547, i522, i523, i524, a208, i69, env, static) :|: 0 <= i69 && i547 <= -1 && 0 < a208

(23) TerminationGraphToComplexityProof (BOTH CONCRETE BOUNDS(ID, ADD(3)) transformation)

Extracted set of 99 edges for the analysis of TIME complexity. Dropped leaves.

(24) Obligation:

Set of 99 edges based on JBC Program.
Performed SCC analyses:

Used field analysis yielded the following read fields:

Considered paths: all paths from start

(25) JBCGraphEdgesToCpxIntTrsProof (CONCRETE UPPER BOUND(ID) transformation)

Transformed 99 jbc graph edges to a weighted ITS with 99 rules.
Used simplified encoding of division and modulo.
Filtered conditions with variables that do not depend on the variables on the lhs or rhs without taking transitive dependencies into account.
Filtered fields of type java.lang.Object.
Did no encode lower bounds for putfield and astore.

(26) Obligation:

IntTrs with 99 rules
Start term: main_Load_1(#0, env, static)
Considered paths: all paths from start
Rules:
main_Load_1(o1, env, static) -{0,0}> main_Load_3(o1, env, static) :|: 0 < o1
main_Load_3(o1, env, static) -{0,0}> langle_clinit_rangle_ConstantStackPush_5(o1, env, static) :|: 0 < o1
langle_clinit_rangle_ConstantStackPush_5(o1, env, static) -{1,1}> langle_clinit_rangle_ArrayCreate_9(iconst_0, o1, env, static) :|: iconst_0 = 0 && 0 < o1
langle_clinit_rangle_ArrayCreate_9(iconst_0, o1, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_10(a2, o1, iconst_0, env, static) :|: a2 = 2 && iconst_0 = 0 && 0 < a2 && 0 < o1
langle_clinit_rangle_FieldAccess_10(a2, o1, iconst_0, env, static) -{1,1}> langle_clinit_rangle_New_13(o1, env, static') :|: 0 <= a2 && iconst_0 = 0 && static' <= static + a2 && 0 <= static && 0 < a2 && 0 < o1
langle_clinit_rangle_New_13(o1, env, static) -{0,0}> langle_clinit_rangle_New_15(o1, env, static) :|: 0 < o1
langle_clinit_rangle_New_15(o1, env, static) -{0,0}> langle_clinit_rangle_New_16(o1, env, static) :|: 0 <= static && 0 < o1
langle_clinit_rangle_New_16(o1, env, static) -{1,1}> langle_clinit_rangle_Duplicate_18(o4, o1, env, static) :|: o4 = 1 && 0 < o4 && 0 < o1
langle_clinit_rangle_Duplicate_18(o4, o1, env, static) -{1,1}> langle_clinit_rangle_ConstantStackPush_20(o4, o1, env, static) :|: 0 < o4 && 0 < o1
langle_clinit_rangle_ConstantStackPush_20(o4, o1, env, static) -{1,1}> langle_clinit_rangle_InvokeMethod_22(o4, NULL, o1, env, static) :|: NULL = 0 && 0 < o4 && 0 < o1
langle_clinit_rangle_InvokeMethod_22(o4, NULL, o1, env, static) -{1,1}> langle_init_rangle_Load_24(o4, o1, env, static) :|: NULL = 0 && 0 < o4 && 0 < o1
langle_init_rangle_Load_24(o4, o1, env, static) -{1,1}> langle_init_rangle_InvokeMethod_25(o4, o1, env, static) :|: 0 < o4 && 0 < o1
langle_init_rangle_InvokeMethod_25(o4, o1, env, static) -{1,1}> langle_init_rangle_Load_27(o4, o1, env, static) :|: 0 < o4 && 0 < o1
langle_init_rangle_Load_27(o4, o1, env, static) -{1,1}> langle_init_rangle_InvokeMethod_30(o4, o1, env, static) :|: 0 < o4 && 0 < o1
langle_init_rangle_InvokeMethod_30(o4, o1, env, static) -{1,1}> langle_init_rangle_Return_32(o4, o1, env, static) :|: 0 < o4 && 0 < o1
langle_init_rangle_Return_32(o4, o1, env, static) -{1,1}> langle_init_rangle_Return_35(o4, o1, env, static) :|: 0 < o4 && 0 < o1
langle_init_rangle_Return_35(o4, o1, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_37(o4, o1, env, static) :|: 0 < o4 && 0 < o1
langle_clinit_rangle_FieldAccess_37(o4, o1, env, static) -{1,1}> langle_clinit_rangle_Return_40(o1, env, static') :|: 0 <= o4 && 0 < o4 && 0 <= static && 0 < o1 && static' <= static + o4
langle_clinit_rangle_Return_40(o1, env, static) -{1,1}> main_Load_41(o1, env, static) :|: 0 < o1
main_Load_41(o1, env, static) -{0,0}> main_Load_42(o1, env, static) :|: 0 < o1
main_Load_42(o1, env, static) -{0,0}> main_Load_43(o1, env, static) :|: 0 <= static && 0 < o1
main_Load_43(o1, env, static) -{0,0}> main_Load_45(o1, env, static) :|: 0 < o1
main_Load_45(o1, env, static) -{0,0}> main_Load_47(o1, env, static) :|: 0 < o1
main_Load_47(o1, env, static) -{1,1}> main_ArrayLength_51(o1, env, static) :|: 0 < o1
main_ArrayLength_51(a6, env, static) -{0,0}> main_ArrayLength_52(a6, i4, env, static) :|: 0 <= i4 && 0 < a6 && i4 < a6
main_ArrayLength_52(a6, i4, env, static) -{1,1}> main_Load_54(a6, i4, env, static) :|: 0 <= i4 && 0 < a6
main_Load_54(a6, i4, env, static) -{1,1}> main_ArrayLength_56(a6, i4, env, static) :|: 0 <= i4 && 0 < a6
main_ArrayLength_56(a6, i4, env, static) -{1,1}> main_ConstantStackPush_58(a6, i4, env, static) :|: 0 <= i4 && 0 < a6
main_ConstantStackPush_58(a6, i4, env, static) -{1,1}> main_IntArithmetic_60(a6, i4, iconst_5, env, static) :|: iconst_5 = 5 && 0 <= i4 && 0 < a6
main_IntArithmetic_60(a6, i4, iconst_5, env, static) -{1,1}> main_Load_62(a6, i4, i6, env, static) :|: 0 <= i6 && iconst_5 = 5 && i6 < iconst_5 && 0 <= i4 && i6 <= 4 && 0 < a6
main_Load_62(a6, i4, i6, env, static) -{1,1}> main_ArrayLength_64(a6, i4, i6, env, static) :|: 0 <= i6 && 0 <= i4 && i6 <= 4 && 0 < a6
main_ArrayLength_64(a6, i4, i6, env, static) -{1,1}> main_ConstantStackPush_66(a6, i4, i6, env, static) :|: 0 <= i6 && 0 <= i4 && i6 <= 4 && 0 < a6
main_ConstantStackPush_66(a6, i4, i6, env, static) -{1,1}> main_IntArithmetic_68(a6, i4, i6, iconst_4, env, static) :|: 0 <= i6 && iconst_4 = 4 && 0 <= i4 && i6 <= 4 && 0 < a6
main_IntArithmetic_68(a6, i4, i6, iconst_4, env, static) -{1,1}> main_InvokeMethod_70(a6, i4, i6, i8, env, static) :|: 0 <= i6 && i8 <= 3 && i8 < iconst_4 && iconst_4 = 4 && 0 <= i4 && i6 <= 4 && 0 < a6 && 0 <= i8
main_InvokeMethod_70(a6, i4, i6, i8, env, static) -{1,1}> iter_Load_72(i4, i6, i8, a6, env, static) :|: 0 <= i6 && i8 <= 3 && 0 <= i4 && i6 <= 4 && 0 < a6 && 0 <= i8
iter_Load_72(i4, i6, i8, a6, env, static) -{0,0}> iter_Load_577(i4, i6, i8, a6, i4, env, static) :|: 0 <= i6 && i8 <= 3 && -1 <= i6 && 0 <= i4 && -1 <= i4 && i6 <= 4 && 0 < a6 && 0 <= i8
iter_Load_577(i249, i250, i8, a110, i69, env, static) -{0,0}> iter_Load_710(i249, i250, i8, a110, i69, env, static) :|: i8 <= 3 && 0 < a110 && -1 <= i250 && -1 <= i249 && -1 <= i8 && 0 <= i8 && 0 <= i69
iter_Load_710(i301, i302, i303, a131, i69, env, static) -{0,0}> iter_Load_762(i301, i302, i303, a131, i69, env, static) :|: i303 <= 3 && -1 <= i302 && -2 <= i302 && 0 <= i69 && -1 <= i303 && -1 <= i301 && 0 < a131
iter_Load_762(i326, i327, i303, a139, i69, env, static) -{0,0}> iter_Load_796(i326, i327, i303, a139, i69, env, static) :|: -1 <= i326 && i303 <= 3 && 0 <= i69 && -1 <= i303 && -2 <= i327 && 0 < a139
iter_Load_796(i342, i327, i303, a145, i69, env, static) -{0,0}> iter_Load_899(i342, i327, i303, a145, i69, env, static) :|: i303 <= 3 && -2 <= i303 && 0 < a145 && 0 <= i69 && -1 <= i303 && -2 <= i327
iter_Load_899(i380, i381, i382, a164, i69, env, static) -{0,0}> iter_Load_1043(i380, i381, i382, a164, i69, env, static) :|: -2 <= i381 && i382 <= 3 && 0 < a164 && -2 <= i382 && 0 <= i69
iter_Load_1043(i426, i427, i382, a176, i69, env, static) -{0,0}> iter_Load_1320(i426, i427, i382, a176, i69, env, static) :|: 0 < a176 && i382 <= 3 && -2 <= i382 && 0 <= i69
iter_Load_1320(i522, i523, i524, a208, i69, env, static) -{1,1}> iter_Load_1321(i522, i523, i524, a208, i69, env, static) :|: 0 <= i69 && 0 < a208
iter_Load_1321(i522, i523, i524, a208, i69, env, static) -{1,1}> iter_IntArithmetic_1324(i522, i523, i524, a208, i69, env, static) :|: 0 <= i69 && 0 < a208
iter_IntArithmetic_1324(i522, i523, i524, a208, i69, env, static) -{1,1}> iter_ConstantStackPush_1327(i538, i522, i523, i524, a208, i69, env, static) :|: i522 + i523 = i538 && 0 <= i69 && 0 < a208
iter_ConstantStackPush_1327(i538, i522, i523, i524, a208, i69, env, static) -{1,1}> iter_Load_1329(i538, iconst_3, i522, i523, i524, a208, i69, env, static) :|: iconst_3 = 3 && 0 <= i69 && 0 < a208
iter_Load_1329(i538, iconst_3, i522, i523, i524, a208, i69, env, static) -{1,1}> iter_IntArithmetic_1330(i538, iconst_3, i524, i522, i523, a208, i69, env, static) :|: iconst_3 = 3 && 0 <= i69 && 0 < a208
iter_IntArithmetic_1330(i538, iconst_3, i524, i522, i523, a208, i69, env, static) -{1,1}> iter_IntArithmetic_1332(i538, i540, i522, i523, i524, a208, i69, env, static) :|: iconst_3 * i524 = i540 && iconst_3 = 3 && 0 <= i69 && 0 < a208
iter_IntArithmetic_1332(i538, i540, i522, i523, i524, a208, i69, env, static) -{1,1}> iter_LT_1335(i541, i522, i523, i524, a208, i69, env, static) :|: i538 + i540 = i541 && 0 <= i69 && 0 < a208
iter_LT_1335(i548, i522, i523, i524, a208, i69, env, static) -{0,0}> iter_LT_1337(i548, i522, i523, i524, a208, i69, env, static) :|: 0 <= i548 && 0 <= i69 && 0 < a208
iter_LT_1337(i548, i522, i523, i524, a208, i69, env, static) -{1,1}> iter_Load_1340(i522, i523, i524, a208, i69, env, static) :|: 0 <= i548 && 0 <= i69 && 0 < a208
iter_Load_1340(i522, i523, i524, a208, i69, env, static) -{1,1}> iter_Load_1342(i522, i523, i524, a208, i69, env, static) :|: 0 <= i69 && 0 < a208
iter_Load_1342(i522, i523, i524, a208, i69, env, static) -{1,1}> iter_LE_1349(i522, i523, i524, a208, i69, env, static) :|: 0 <= i69 && 0 < a208
iter_LE_1349(i522, i523, i524, a208, i69, env, static) -{0,0}> iter_LE_1354(i522, i523, i524, a208, i69, env, static) :|: i522 <= i523 && 0 <= i69 && 0 < a208
iter_LE_1349(i522, i523, i524, a208, i69, env, static) -{0,0}> iter_LE_1355(i522, i523, i524, a208, i69, env, static) :|: i523 < i522 && 0 <= i69 && 0 < a208
iter_LE_1354(i522, i523, i524, a208, i69, env, static) -{1,1}> iter_Load_1363(i522, i523, i524, a208, i69, env, static) :|: i522 <= i523 && 0 <= i69 && 0 < a208
iter_LE_1355(i522, i523, i524, a208, i69, env, static) -{1,1}> iter_Inc_1364(i522, i523, i524, a208, i69, env, static) :|: i523 < i522 && 0 <= i69 && 0 < a208
iter_Load_1363(i522, i523, i524, a208, i69, env, static) -{1,1}> iter_Load_1365(i523, i522, i524, a208, i69, env, static) :|: 0 <= i69 && 0 < a208
iter_Inc_1364(i522, i523, i524, a208, i69, env, static) -{1,1}> iter_JMP_1366(i551, i523, i524, a208, i69, env, static) :|: i522 + -1 = i551 && 0 <= i69 && 0 < a208
iter_Load_1365(i523, i522, i524, a208, i69, env, static) -{1,1}> iter_LE_1378(i523, i524, i522, a208, i69, env, static) :|: 0 <= i69 && 0 < a208
iter_JMP_1366(i551, i523, i524, a208, i69, env, static) -{1,1}> iter_Load_1395(i551, i523, i524, a208, i69, env, static) :|: 0 <= i69 && 0 < a208
iter_LE_1378(i523, i524, i522, a208, i69, env, static) -{0,0}> iter_LE_1404(i523, i524, i522, a208, i69, env, static) :|: 0 <= i69 && i523 <= i524 && 0 < a208
iter_LE_1378(i523, i524, i522, a208, i69, env, static) -{0,0}> iter_LE_1405(i523, i524, i522, a208, i69, env, static) :|: 0 <= i69 && i524 < i523 && 0 < a208
iter_Load_1395(i551, i523, i524, a208, i69, env, static) -{1,1}> iter_Load_1407(i551, i523, i524, a208, i69, env, static) :|: 0 <= i69 && 0 < a208
iter_LE_1404(i523, i524, i522, a208, i69, env, static) -{1,1}> iter_Load_1408(i522, i523, i524, a208, i69, env, static) :|: 0 <= i69 && i523 <= i524 && 0 < a208
iter_LE_1405(i523, i524, i522, a208, i69, env, static) -{1,1}> iter_Inc_1409(i522, i523, i524, a208, i69, env, static) :|: 0 <= i69 && i524 < i523 && 0 < a208
iter_Load_1407(i551, i523, i524, a208, i69, env, static) -{1,1}> iter_IntArithmetic_1414(i551, i523, i524, a208, i69, env, static) :|: 0 <= i69 && 0 < a208
iter_Load_1408(i522, i523, i524, a208, i69, env, static) -{1,1}> iter_Load_1415(i523, i522, i524, a208, i69, env, static) :|: 0 <= i69 && 0 < a208
iter_Inc_1409(i522, i523, i524, a208, i69, env, static) -{1,1}> iter_Inc_1417(i561, i523, i524, a208, i69, env, static) :|: 0 <= i69 && i522 + 1 = i561 && 0 < a208
iter_IntArithmetic_1414(i551, i523, i524, a208, i69, env, static) -{1,1}> iter_ConstantStackPush_1421(i562, i551, i523, i524, a208, i69, env, static) :|: i551 + i523 = i562 && 0 <= i69 && 0 < a208
iter_Load_1415(i523, i522, i524, a208, i69, env, static) -{1,1}> iter_GT_1423(i523, i524, i522, a208, i69, env, static) :|: 0 <= i69 && 0 < a208
iter_Inc_1417(i561, i523, i524, a208, i69, env, static) -{1,1}> iter_JMP_1425(i561, i566, i524, a208, i69, env, static) :|: i523 + -2 = i566 && 0 <= i69 && 0 < a208
iter_ConstantStackPush_1421(i562, i551, i523, i524, a208, i69, env, static) -{0,0}> iter_ConstantStackPush_1327(i562, i551, i523, i524, a208, i69, env, static) :|: 0 <= i69 && 0 < a208
iter_GT_1423(i523, i524, i522, a208, i69, env, static) -{0,0}> iter_GT_1429(i523, i524, i522, a208, i69, env, static) :|: 0 <= i69 && i523 <= i524 && 0 < a208
iter_JMP_1425(i561, i566, i524, a208, i69, env, static) -{1,1}> iter_Load_1435(i561, i566, i524, a208, i69, env, static) :|: 0 <= i69 && 0 < a208
iter_GT_1429(i523, i524, i522, a208, i69, env, static) -{1,1}> iter_Load_1436(i522, i523, i524, a208, i69, env, static) :|: 0 <= i69 && i523 <= i524 && 0 < a208
iter_Load_1435(i561, i566, i524, a208, i69, env, static) -{0,0}> iter_Load_1320(i561, i566, i524, a208, i69, env, static) :|: 0 <= i69 && 0 < a208
iter_Load_1436(i522, i523, i524, a208, i69, env, static) -{1,1}> iter_ConstantStackPush_1437(i522, i523, i524, a208, i69, env, static) :|: 0 <= i69 && 0 < a208
iter_ConstantStackPush_1437(i522, i523, i524, a208, i69, env, static) -{1,1}> iter_InvokeMethod_1438(i522, iconst_1, i523, i524, a208, i69, env, static) :|: iconst_1 = 1 && 0 <= i69 && 0 < a208
iter_InvokeMethod_1438(i522, iconst_1, i523, i524, a208, i69, env, static) -{1,1}> add_Load_1439(i522, iconst_1, i523, i524, a208, i69, env, static) :|: iconst_1 = 1 && 0 <= i69 && 0 < a208
add_Load_1439(i522, iconst_1, i523, i524, a208, i69, env, static) -{1,1}> add_Load_1440(i522, iconst_1, i523, i524, a208, i69, env, static) :|: iconst_1 = 1 && 0 <= i69 && 0 < a208
add_Load_1440(i522, iconst_1, i523, i524, a208, i69, env, static) -{1,1}> add_IntArithmetic_1441(i522, iconst_1, i523, i524, a208, i69, env, static) :|: iconst_1 = 1 && 0 <= i69 && 0 < a208
add_IntArithmetic_1441(i522, iconst_1, i523, i524, a208, i69, env, static) -{1,1}> add_Return_1442(i571, i523, i524, a208, i69, env, static) :|: i522 + iconst_1 = i571 && iconst_1 = 1 && 0 <= i69 && 0 < a208
add_Return_1442(i571, i523, i524, a208, i69, env, static) -{1,1}> iter_Store_1443(i571, i523, i524, a208, i69, env, static) :|: 0 <= i69 && 0 < a208
iter_Store_1443(i571, i523, i524, a208, i69, env, static) -{1,1}> iter_Load_1444(i571, i523, i524, a208, i69, env, static) :|: 0 <= i69 && 0 < a208
iter_Load_1444(i571, i523, i524, a208, i69, env, static) -{1,1}> iter_ConstantStackPush_1445(i523, i571, i524, a208, i69, env, static) :|: 0 <= i69 && 0 < a208
iter_ConstantStackPush_1445(i523, i571, i524, a208, i69, env, static) -{1,1}> iter_InvokeMethod_1446(i523, iconst_1, i571, i524, a208, i69, env, static) :|: iconst_1 = 1 && 0 <= i69 && 0 < a208
iter_InvokeMethod_1446(i523, iconst_1, i571, i524, a208, i69, env, static) -{1,1}> add_Load_1447(i523, iconst_1, i571, i524, a208, i69, env, static) :|: iconst_1 = 1 && 0 <= i69 && 0 < a208
add_Load_1447(i523, iconst_1, i571, i524, a208, i69, env, static) -{1,1}> add_Load_1448(i523, iconst_1, i571, i524, a208, i69, env, static) :|: iconst_1 = 1 && 0 <= i69 && 0 < a208
add_Load_1448(i523, iconst_1, i571, i524, a208, i69, env, static) -{1,1}> add_IntArithmetic_1449(i523, iconst_1, i571, i524, a208, i69, env, static) :|: iconst_1 = 1 && 0 <= i69 && 0 < a208
add_IntArithmetic_1449(i523, iconst_1, i571, i524, a208, i69, env, static) -{1,1}> add_Return_1450(i578, i571, i524, a208, i69, env, static) :|: iconst_1 = 1 && i523 + iconst_1 = i578 && 0 <= i69 && 0 < a208
add_Return_1450(i578, i571, i524, a208, i69, env, static) -{1,1}> iter_Store_1451(i578, i571, i524, a208, i69, env, static) :|: 0 <= i69 && 0 < a208
iter_Store_1451(i578, i571, i524, a208, i69, env, static) -{1,1}> iter_Load_1452(i571, i578, i524, a208, i69, env, static) :|: 0 <= i69 && 0 < a208
iter_Load_1452(i571, i578, i524, a208, i69, env, static) -{1,1}> iter_ConstantStackPush_1453(i524, i571, i578, a208, i69, env, static) :|: 0 <= i69 && 0 < a208
iter_ConstantStackPush_1453(i524, i571, i578, a208, i69, env, static) -{1,1}> iter_IntArithmetic_1454(i524, iconst_1, i571, i578, a208, i69, env, static) :|: iconst_1 = 1 && 0 <= i69 && 0 < a208
iter_IntArithmetic_1454(i524, iconst_1, i571, i578, a208, i69, env, static) -{1,1}> iter_Store_1455(i582, i571, i578, a208, i69, env, static) :|: iconst_1 = 1 && 0 <= i69 && i524 - iconst_1 = i582 && 0 < a208
iter_Store_1455(i582, i571, i578, a208, i69, env, static) -{1,1}> iter_JMP_1456(i571, i578, i582, a208, i69, env, static) :|: 0 <= i69 && 0 < a208
iter_JMP_1456(i571, i578, i582, a208, i69, env, static) -{1,1}> iter_Load_1457(i571, i578, i582, a208, i69, env, static) :|: 0 <= i69 && 0 < a208
iter_Load_1457(i571, i578, i582, a208, i69, env, static) -{0,0}> iter_Load_1320(i571, i578, i582, a208, i69, env, static) :|: 0 <= i69 && 0 < a208

(27) StraightLineCodeCompressionProof (BOTH CONCRETE BOUNDS(ID, ID) transformation)

obtained
iter_ConstantStackPush_1327(i538, i522, i523, i524, a208, i69, env, static) -{7,7}> iter_LE_1349(i522, i523, i524, a208, i69, env, static) :|: 3 * i524 = i540' && 0 <= i69 && 0 < a208 && 0 <= i541' && i538 + i540' = i541'
by chaining
iter_ConstantStackPush_1327(i538, i522, i523, i524, a208, i69, env, static) -{1,1}> iter_Load_1329(i538, iconst_3, i522, i523, i524, a208, i69, env, static) :|: iconst_3 = 3 && 0 <= i69 && 0 < a208
iter_Load_1329(i538, iconst_3, i522, i523, i524, a208, i69, env, static) -{1,1}> iter_IntArithmetic_1330(i538, iconst_3, i524, i522, i523, a208, i69, env, static) :|: iconst_3 = 3 && 0 <= i69 && 0 < a208
iter_IntArithmetic_1330(i538, iconst_3, i524, i522, i523, a208, i69, env, static) -{1,1}> iter_IntArithmetic_1332(i538, i540, i522, i523, i524, a208, i69, env, static) :|: iconst_3 * i524 = i540 && iconst_3 = 3 && 0 <= i69 && 0 < a208
iter_IntArithmetic_1332(i538, i540, i522, i523, i524, a208, i69, env, static) -{1,1}> iter_LT_1335(i541, i522, i523, i524, a208, i69, env, static) :|: i538 + i540 = i541 && 0 <= i69 && 0 < a208
iter_LT_1335(i548, i522, i523, i524, a208, i69, env, static) -{0,0}> iter_LT_1337(i548, i522, i523, i524, a208, i69, env, static) :|: 0 <= i548 && 0 <= i69 && 0 < a208
iter_LT_1337(i548, i522, i523, i524, a208, i69, env, static) -{1,1}> iter_Load_1340(i522, i523, i524, a208, i69, env, static) :|: 0 <= i548 && 0 <= i69 && 0 < a208
iter_Load_1340(i522, i523, i524, a208, i69, env, static) -{1,1}> iter_Load_1342(i522, i523, i524, a208, i69, env, static) :|: 0 <= i69 && 0 < a208
iter_Load_1342(i522, i523, i524, a208, i69, env, static) -{1,1}> iter_LE_1349(i522, i523, i524, a208, i69, env, static) :|: 0 <= i69 && 0 < a208

(28) Obligation:

IntTrs with 7 rules
Start term: main_Load_1(#0, env, static)
Considered paths: all paths from start
Rules:
main_Load_1(o1, env, static) -{26,26}> iter_Load_1320(i4', i6', i8', o1, i4', env, static'1) :|: static'1 <= static''' + 1 && 0 <= i4' && 0 <= 2 && -2 <= i8' && -1 <= i8' && 0 < o1 && i8' <= 3 && static''' <= static + 2 && i6' <= 4 && 0 <= static && i6' < 5 && -1 <= i6' && 0 <= static''' && i8' < 4 && 0 <= i6' && 0 < 2 && -1 <= i4' && 0 <= 1 && -2 <= i6' && 0 < 1 && 0 <= i8' && 0 <= static'1 && i4' < o1
iter_Load_1320(i522, i523, i524, a208, i69, env, static) -{3,3}> iter_ConstantStackPush_1327(i538', i522, i523, i524, a208, i69, env, static) :|: 0 <= i69 && 0 < a208 && i522 + i523 = i538'
iter_ConstantStackPush_1327(i538, i522, i523, i524, a208, i69, env, static) -{7,7}> iter_LE_1349(i522, i523, i524, a208, i69, env, static) :|: 3 * i524 = i540' && 0 <= i69 && 0 < a208 && 0 <= i541' && i538 + i540' = i541'
iter_LE_1349(i522, i523, i524, a208, i69, env, static) -{6,6}> iter_ConstantStackPush_1327(i562', i551', i523, i524, a208, i69, env, static) :|: i522 + -1 = i551' && 0 <= i69 && 0 < a208 && i551' + i523 = i562' && i523 < i522
iter_LE_1349(i522, i523, i524, a208, i69, env, static) -{3,3}> iter_LE_1378(i523, i524, i522, a208, i69, env, static) :|: i522 <= i523 && 0 <= i69 && 0 < a208
iter_LE_1378(i523, i524, i522, a208, i69, env, static) -{4,4}> iter_Load_1320(i561', i566', i524, a208, i69, env, static) :|: i522 + 1 = i561' && 0 <= i69 && 0 < a208 && i523 + -2 = i566' && i524 < i523
iter_LE_1378(i523, i524, i522, a208, i69, env, static) -{25,25}> iter_Load_1320(i571', i578', i582', a208, i69, env, static) :|: i523 <= i524 && 0 <= i69 && 0 < a208 && i522 + 1 = i571' && i524 - 1 = i582' && i523 + 1 = i578'

(29) WeightedIntTrsUnneededArgumentFilterProof (CONCRETE UPPER BOUND(ID) transformation)

Some arguments are removed because they cannot influence termination. We removed arguments according to the following replacements:

main_Load_1(x1, x2, x3) → main_Load_1(x1, x3)
iter_Load_1320(x1, x2, x3, x4, x5, x6, x7) → iter_Load_1320(x1, x2, x3, x4, x5)
iter_ConstantStackPush_1327(x1, x2, x3, x4, x5, x6, x7, x8) → iter_ConstantStackPush_1327(x1, x2, x3, x4, x5, x6)
iter_LE_1349(x1, x2, x3, x4, x5, x6, x7) → iter_LE_1349(x1, x2, x3, x4, x5)
iter_LE_1378(x1, x2, x3, x4, x5, x6, x7) → iter_LE_1378(x1, x2, x3, x4, x5)

(30) Obligation:

IntTrs with 7 rules
Start term: main_Load_1(#0, static)
Considered paths: all paths from start
Rules:
main_Load_1(o1, static) -{26,26}> iter_Load_1320(i4', i6', i8', o1, i4') :|: static'1 <= static''' + 1 && 0 <= i4' && 0 <= 2 && -2 <= i8' && -1 <= i8' && 0 < o1 && i8' <= 3 && static''' <= static + 2 && i6' <= 4 && 0 <= static && i6' < 5 && -1 <= i6' && 0 <= static''' && i8' < 4 && 0 <= i6' && 0 < 2 && -1 <= i4' && 0 <= 1 && -2 <= i6' && 0 < 1 && 0 <= i8' && 0 <= static'1 && i4' < o1
iter_Load_1320(i522, i523, i524, a208, i69) -{3,3}> iter_ConstantStackPush_1327(i538', i522, i523, i524, a208, i69) :|: 0 <= i69 && 0 < a208 && i522 + i523 = i538'
iter_ConstantStackPush_1327(i538, i522, i523, i524, a208, i69) -{7,7}> iter_LE_1349(i522, i523, i524, a208, i69) :|: 3 * i524 = i540' && 0 <= i69 && 0 < a208 && 0 <= i541' && i538 + i540' = i541'
iter_LE_1349(i522, i523, i524, a208, i69) -{6,6}> iter_ConstantStackPush_1327(i562', i551', i523, i524, a208, i69) :|: i522 + -1 = i551' && 0 <= i69 && 0 < a208 && i551' + i523 = i562' && i523 < i522
iter_LE_1349(i522, i523, i524, a208, i69) -{3,3}> iter_LE_1378(i523, i524, i522, a208, i69) :|: i522 <= i523 && 0 <= i69 && 0 < a208
iter_LE_1378(i523, i524, i522, a208, i69) -{4,4}> iter_Load_1320(i561', i566', i524, a208, i69) :|: i522 + 1 = i561' && 0 <= i69 && 0 < a208 && i523 + -2 = i566' && i524 < i523
iter_LE_1378(i523, i524, i522, a208, i69) -{25,25}> iter_Load_1320(i571', i578', i582', a208, i69) :|: i523 <= i524 && 0 <= i69 && 0 < a208 && i522 + 1 = i571' && i524 - 1 = i582' && i523 + 1 = i578'

(31) MovedArithmeticFromConstraintsProof (BOTH CONCRETE BOUNDS(ID, ID) transformation)

Moved arithmethic from constraints to rhss.

iter_Load_1320(i522, i523, i524, a208, i69) -{3,3}> iter_ConstantStackPush_1327(i538', i522, i523, i524, a208, i69) :|: 0 <= i69 && 0 < a208 && i522 + i523 = i538'
was transformed to
iter_Load_1320(i522, i523, i524, a208, i69) -{3,3}> iter_ConstantStackPush_1327(i522 + i523, i522, i523, i524, a208, i69) :|: 0 <= i69 && 0 < a208 && i522 + i523 = i538'

iter_LE_1349(i522, i523, i524, a208, i69) -{6,6}> iter_ConstantStackPush_1327(i562', i551', i523, i524, a208, i69) :|: i522 + -1 = i551' && 0 <= i69 && 0 < a208 && i551' + i523 = i562' && i523 < i522
was transformed to
iter_LE_1349(i522, i523, i524, a208, i69) -{6,6}> iter_ConstantStackPush_1327(i522 + -1 + i523, i522 + -1, i523, i524, a208, i69) :|: i522 + -1 = i551' && 0 <= i69 && 0 < a208 && i551' + i523 = i562' && i523 < i522

iter_LE_1378(i523, i524, i522, a208, i69) -{4,4}> iter_Load_1320(i561', i566', i524, a208, i69) :|: i522 + 1 = i561' && 0 <= i69 && 0 < a208 && i523 + -2 = i566' && i524 < i523
was transformed to
iter_LE_1378(i523, i524, i522, a208, i69) -{4,4}> iter_Load_1320(i522 + 1, i523 + -2, i524, a208, i69) :|: i522 + 1 = i561' && 0 <= i69 && 0 < a208 && i523 + -2 = i566' && i524 < i523

iter_LE_1378(i523, i524, i522, a208, i69) -{25,25}> iter_Load_1320(i571', i578', i582', a208, i69) :|: i523 <= i524 && 0 <= i69 && 0 < a208 && i522 + 1 = i571' && i524 - 1 = i582' && i523 + 1 = i578'
was transformed to
iter_LE_1378(i523, i524, i522, a208, i69) -{25,25}> iter_Load_1320(i522 + 1, i523 + 1, i524 - 1, a208, i69) :|: i523 <= i524 && 0 <= i69 && 0 < a208 && i522 + 1 = i571' && i524 - 1 = i582' && i523 + 1 = i578'

(32) Obligation:

IntTrs with 7 rules
Start term: main_Load_1(#0, static)
Considered paths: all paths from start
Rules:
iter_Load_1320(i522, i523, i524, a208, i69) -{3,3}> iter_ConstantStackPush_1327(i522 + i523, i522, i523, i524, a208, i69) :|: 0 <= i69 && 0 < a208 && i522 + i523 = i538'
iter_ConstantStackPush_1327(i538, i522, i523, i524, a208, i69) -{7,7}> iter_LE_1349(i522, i523, i524, a208, i69) :|: 3 * i524 = i540' && 0 <= i69 && 0 < a208 && 0 <= i541' && i538 + i540' = i541'
iter_LE_1349(i522, i523, i524, a208, i69) -{6,6}> iter_ConstantStackPush_1327(i522 + -1 + i523, i522 + -1, i523, i524, a208, i69) :|: i522 + -1 = i551' && 0 <= i69 && 0 < a208 && i551' + i523 = i562' && i523 < i522
main_Load_1(o1, static) -{26,26}> iter_Load_1320(i4', i6', i8', o1, i4') :|: static'1 <= static''' + 1 && 0 <= i4' && 0 <= 2 && -2 <= i8' && -1 <= i8' && 0 < o1 && i8' <= 3 && static''' <= static + 2 && i6' <= 4 && 0 <= static && i6' < 5 && -1 <= i6' && 0 <= static''' && i8' < 4 && 0 <= i6' && 0 < 2 && -1 <= i4' && 0 <= 1 && -2 <= i6' && 0 < 1 && 0 <= i8' && 0 <= static'1 && i4' < o1
iter_LE_1378(i523, i524, i522, a208, i69) -{4,4}> iter_Load_1320(i522 + 1, i523 + -2, i524, a208, i69) :|: i522 + 1 = i561' && 0 <= i69 && 0 < a208 && i523 + -2 = i566' && i524 < i523
iter_LE_1378(i523, i524, i522, a208, i69) -{25,25}> iter_Load_1320(i522 + 1, i523 + 1, i524 - 1, a208, i69) :|: i523 <= i524 && 0 <= i69 && 0 < a208 && i522 + 1 = i571' && i524 - 1 = i582' && i523 + 1 = i578'
iter_LE_1349(i522, i523, i524, a208, i69) -{3,3}> iter_LE_1378(i523, i524, i522, a208, i69) :|: i522 <= i523 && 0 <= i69 && 0 < a208

(33) ExpressionSimplificationProof (BOTH CONCRETE BOUNDS(ID, ID) transformation)

Simplified expressions.

iter_LE_1349(i522, i523, i524, a208, i69) -{6,6}> iter_ConstantStackPush_1327(i522 + -1 + i523, i522 + -1, i523, i524, a208, i69) :|: i522 + -1 = i551' && 0 <= i69 && 0 < a208 && i551' + i523 = i562' && i523 < i522
was transformed to
iter_LE_1349(i522, i523, i524, a208, i69) -{6,6}> iter_ConstantStackPush_1327(i522 - 1 + i523, i522 - 1, i523, i524, a208, i69) :|: i522 - 1 = i551' && 0 <= i69 && 0 < a208 && i551' + i523 = i562' && i523 < i522

iter_LE_1378(i523, i524, i522, a208, i69) -{4,4}> iter_Load_1320(i522 + 1, i523 + -2, i524, a208, i69) :|: i522 + 1 = i561' && 0 <= i69 && 0 < a208 && i523 + -2 = i566' && i524 < i523
was transformed to
iter_LE_1378(i523, i524, i522, a208, i69) -{4,4}> iter_Load_1320(i522 + 1, i523 - 2, i524, a208, i69) :|: i522 + 1 = i561' && 0 <= i69 && 0 < a208 && i523 - 2 = i566' && i524 < i523

main_Load_1(o1, static) -{26,26}> iter_Load_1320(i4', i6', i8', o1, i4') :|: static'1 <= static''' + 1 && 0 <= i4' && 0 <= 2 && -2 <= i8' && -1 <= i8' && 0 < o1 && i8' <= 3 && static''' <= static + 2 && i6' <= 4 && 0 <= static && i6' < 5 && -1 <= i6' && 0 <= static''' && i8' < 4 && 0 <= i6' && 0 < 2 && -1 <= i4' && 0 <= 1 && -2 <= i6' && 0 < 1 && 0 <= i8' && 0 <= static'1 && i4' < o1
was transformed to
main_Load_1(o1, static) -{26,26}> iter_Load_1320(i4', i6', i8', o1, i4') :|: static'1 <= static''' + 1 && 0 <= i4' && -2 <= i8' && -1 <= i8' && 0 < o1 && i8' <= 3 && static''' <= static + 2 && i6' <= 4 && 0 <= static && i6' < 5 && -1 <= i6' && 0 <= static''' && i8' < 4 && 0 <= i6' && -1 <= i4' && -2 <= i6' && 0 <= i8' && 0 <= static'1 && i4' < o1

(34) Obligation:

IntTrs with 7 rules
Start term: main_Load_1(#0, static)
Considered paths: all paths from start
Rules:
iter_LE_1378(i523, i524, i522, a208, i69) -{4,4}> iter_Load_1320(i522 + 1, i523 - 2, i524, a208, i69) :|: i522 + 1 = i561' && 0 <= i69 && 0 < a208 && i523 - 2 = i566' && i524 < i523
iter_Load_1320(i522, i523, i524, a208, i69) -{3,3}> iter_ConstantStackPush_1327(i522 + i523, i522, i523, i524, a208, i69) :|: 0 <= i69 && 0 < a208 && i522 + i523 = i538'
iter_ConstantStackPush_1327(i538, i522, i523, i524, a208, i69) -{7,7}> iter_LE_1349(i522, i523, i524, a208, i69) :|: 3 * i524 = i540' && 0 <= i69 && 0 < a208 && 0 <= i541' && i538 + i540' = i541'
iter_LE_1349(i522, i523, i524, a208, i69) -{6,6}> iter_ConstantStackPush_1327(i522 - 1 + i523, i522 - 1, i523, i524, a208, i69) :|: i522 - 1 = i551' && 0 <= i69 && 0 < a208 && i551' + i523 = i562' && i523 < i522
main_Load_1(o1, static) -{26,26}> iter_Load_1320(i4', i6', i8', o1, i4') :|: static'1 <= static''' + 1 && 0 <= i4' && -2 <= i8' && -1 <= i8' && 0 < o1 && i8' <= 3 && static''' <= static + 2 && i6' <= 4 && 0 <= static && i6' < 5 && -1 <= i6' && 0 <= static''' && i8' < 4 && 0 <= i6' && -1 <= i4' && -2 <= i6' && 0 <= i8' && 0 <= static'1 && i4' < o1
iter_LE_1349(i522, i523, i524, a208, i69) -{3,3}> iter_LE_1378(i523, i524, i522, a208, i69) :|: i522 <= i523 && 0 <= i69 && 0 < a208
iter_LE_1378(i523, i524, i522, a208, i69) -{25,25}> iter_Load_1320(i522 + 1, i523 + 1, i524 - 1, a208, i69) :|: i523 <= i524 && 0 <= i69 && 0 < a208 && i522 + 1 = i571' && i524 - 1 = i582' && i523 + 1 = i578'

(35) koat Proof (EQUIVALENT transformation)

YES(?, 561*ar_0 + 39350)

Initial complexity problem:
1: T:
(Comp: ?, Cost: 4) iter_LE_1378(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(iter_Load_1320(ar_2 + 1, ar_0 - 2, ar_1, ar_3, ar_4, arityPad)) [ ar_2 + 1 = i561' /\ 0 <= ar_4 /\ 0 < ar_3 /\ ar_0 - 2 = i566' /\ ar_1 < ar_0 ]
(Comp: ?, Cost: 3) iter_Load_1320(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(iter_ConstantStackPush_1327(ar_0 + ar_1, ar_0, ar_1, ar_2, ar_3, ar_4)) [ 0 <= ar_4 /\ 0 < ar_3 /\ ar_0 + ar_1 = i538' ]
(Comp: ?, Cost: 7) iter_ConstantStackPush_1327(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(iter_LE_1349(ar_1, ar_2, ar_3, ar_4, ar_5, arityPad)) [ 3*ar_3 = i540' /\ 0 <= ar_5 /\ 0 < ar_4 /\ 0 <= i541' /\ ar_0 + i540' = i541' ]
(Comp: ?, Cost: 6) iter_LE_1349(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(iter_ConstantStackPush_1327(ar_0 + ar_1 - 1, ar_0 - 1, ar_1, ar_2, ar_3, ar_4)) [ ar_0 - 1 = i551' /\ 0 <= ar_4 /\ 0 < ar_3 /\ i551' + ar_1 = i562' /\ ar_1 < ar_0 ]
(Comp: ?, Cost: 26) main_Load_1(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(iter_Load_1320(i4', i6', i8', ar_0, i4', arityPad)) [ static'1 <= static''' + 1 /\ 0 <= i4' /\ -2 <= i8' /\ -1 <= i8' /\ 0 < ar_0 /\ i8' <= 3 /\ static''' <= ar_1 + 2 /\ i6' <= 4 /\ 0 <= ar_1 /\ i6' < 5 /\ -1 <= i6' /\ 0 <= static''' /\ i8' < 4 /\ 0 <= i6' /\ -1 <= i4' /\ -2 <= i6' /\ 0 <= i8' /\ 0 <= static'1 /\ i4' < ar_0 ]
(Comp: ?, Cost: 3) iter_LE_1349(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(iter_LE_1378(ar_1, ar_2, ar_0, ar_3, ar_4, arityPad)) [ ar_0 <= ar_1 /\ 0 <= ar_4 /\ 0 < ar_3 ]
(Comp: ?, Cost: 25) iter_LE_1378(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(iter_Load_1320(ar_2 + 1, ar_0 + 1, ar_1 - 1, ar_3, ar_4, arityPad)) [ ar_0 <= ar_1 /\ 0 <= ar_4 /\ 0 < ar_3 /\ ar_2 + 1 = i571' /\ ar_1 - 1 = i582' /\ ar_0 + 1 = i578' ]
(Comp: 1, Cost: 0) koat_start(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(main_Load_1(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5)) [ 0 <= 0 ]
start location: koat_start
leaf cost: 0

Repeatedly propagating knowledge in problem 1 produces the following problem:
2: T:
(Comp: ?, Cost: 4) iter_LE_1378(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(iter_Load_1320(ar_2 + 1, ar_0 - 2, ar_1, ar_3, ar_4, arityPad)) [ ar_2 + 1 = i561' /\ 0 <= ar_4 /\ 0 < ar_3 /\ ar_0 - 2 = i566' /\ ar_1 < ar_0 ]
(Comp: ?, Cost: 3) iter_Load_1320(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(iter_ConstantStackPush_1327(ar_0 + ar_1, ar_0, ar_1, ar_2, ar_3, ar_4)) [ 0 <= ar_4 /\ 0 < ar_3 /\ ar_0 + ar_1 = i538' ]
(Comp: ?, Cost: 7) iter_ConstantStackPush_1327(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(iter_LE_1349(ar_1, ar_2, ar_3, ar_4, ar_5, arityPad)) [ 3*ar_3 = i540' /\ 0 <= ar_5 /\ 0 < ar_4 /\ 0 <= i541' /\ ar_0 + i540' = i541' ]
(Comp: ?, Cost: 6) iter_LE_1349(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(iter_ConstantStackPush_1327(ar_0 + ar_1 - 1, ar_0 - 1, ar_1, ar_2, ar_3, ar_4)) [ ar_0 - 1 = i551' /\ 0 <= ar_4 /\ 0 < ar_3 /\ i551' + ar_1 = i562' /\ ar_1 < ar_0 ]
(Comp: 1, Cost: 26) main_Load_1(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(iter_Load_1320(i4', i6', i8', ar_0, i4', arityPad)) [ static'1 <= static''' + 1 /\ 0 <= i4' /\ -2 <= i8' /\ -1 <= i8' /\ 0 < ar_0 /\ i8' <= 3 /\ static''' <= ar_1 + 2 /\ i6' <= 4 /\ 0 <= ar_1 /\ i6' < 5 /\ -1 <= i6' /\ 0 <= static''' /\ i8' < 4 /\ 0 <= i6' /\ -1 <= i4' /\ -2 <= i6' /\ 0 <= i8' /\ 0 <= static'1 /\ i4' < ar_0 ]
(Comp: ?, Cost: 3) iter_LE_1349(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(iter_LE_1378(ar_1, ar_2, ar_0, ar_3, ar_4, arityPad)) [ ar_0 <= ar_1 /\ 0 <= ar_4 /\ 0 < ar_3 ]
(Comp: ?, Cost: 25) iter_LE_1378(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(iter_Load_1320(ar_2 + 1, ar_0 + 1, ar_1 - 1, ar_3, ar_4, arityPad)) [ ar_0 <= ar_1 /\ 0 <= ar_4 /\ 0 < ar_3 /\ ar_2 + 1 = i571' /\ ar_1 - 1 = i582' /\ ar_0 + 1 = i578' ]
(Comp: 1, Cost: 0) koat_start(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(main_Load_1(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5)) [ 0 <= 0 ]
start location: koat_start
leaf cost: 0

Applied AI with 'oct' on problem 2 to obtain the following invariants:
For symbol iter_ConstantStackPush_1327: X_5 - X_6 - 1 >= 0 /\ X_6 >= 0 /\ X_5 + X_6 - 1 >= 0 /\ -X_4 + X_6 + 3 >= 0 /\ -X_3 + X_6 + 4 >= 0 /\ X_5 - 1 >= 0 /\ -X_4 + X_5 + 2 >= 0 /\ -X_3 + X_5 + 3 >= 0 /\ -X_4 + 3 >= 0 /\ X_3 - X_4 + 3 >= 0 /\ -X_3 - X_4 + 7 >= 0 /\ -X_3 + X_4 + 4 >= 0 /\ -X_3 + 4 >= 0 /\ -X_1 + X_2 + 4 >= 0
For symbol iter_LE_1349: X_4 - X_5 - 1 >= 0 /\ X_5 >= 0 /\ X_4 + X_5 - 1 >= 0 /\ -X_3 + X_5 + 3 >= 0 /\ -X_2 + X_5 + 4 >= 0 /\ X_1 + X_5 + 13 >= 0 /\ X_4 - 1 >= 0 /\ -X_3 + X_4 + 2 >= 0 /\ -X_2 + X_4 + 3 >= 0 /\ X_1 + X_4 + 12 >= 0 /\ -X_3 + 3 >= 0 /\ X_2 - X_3 + 3 >= 0 /\ -X_2 - X_3 + 7 >= 0 /\ X_1 - X_3 + 16 >= 0 /\ -X_2 + X_3 + 4 >= 0 /\ X_1 + X_3 + 10 >= 0 /\ -X_2 + 4 >= 0 /\ X_1 - X_2 + 17 >= 0 /\ X_1 + X_2 + 13 >= 0 /\ X_1 + 13 >= 0
For symbol iter_LE_1378: X_4 - X_5 - 1 >= 0 /\ X_5 >= 0 /\ X_4 + X_5 - 1 >= 0 /\ X_3 + X_5 + 13 >= 0 /\ -X_3 + X_5 + 4 >= 0 /\ X_2 + X_5 + 7 >= 0 /\ -X_2 + X_5 + 3 >= 0 /\ X_1 + X_5 + 6 >= 0 /\ -X_1 + X_5 + 4 >= 0 /\ X_4 - 1 >= 0 /\ X_3 + X_4 + 12 >= 0 /\ -X_3 + X_4 + 3 >= 0 /\ X_2 + X_4 + 6 >= 0 /\ -X_2 + X_4 + 2 >= 0 /\ X_1 + X_4 + 5 >= 0 /\ -X_1 + X_4 + 3 >= 0 /\ -X_3 + 4 >= 0 /\ X_2 - X_3 + 4 >= 0 /\ -X_2 - X_3 + 7 >= 0 /\ X_1 - X_3 >= 0 /\ -X_1 - X_3 + 8 >= 0 /\ X_3 + 13 >= 0 /\ X_2 + X_3 + 10 >= 0 /\ -X_2 + X_3 + 16 >= 0 /\ X_1 + X_3 + 13 >= 0 /\ -X_1 + X_3 + 17 >= 0 /\ -X_2 + 3 >= 0 /\ X_1 - X_2 + 3 >= 0 /\ -X_1 - X_2 + 7 >= 0 /\ X_2 + 7 >= 0 /\ X_1 + X_2 + 10 >= 0 /\ -X_1 + X_2 + 4 >= 0 /\ -X_1 + 4 >= 0 /\ X_1 + 6 >= 0
For symbol iter_Load_1320: X_4 - X_5 - 1 >= 0 /\ X_5 >= 0 /\ X_4 + X_5 - 1 >= 0 /\ -X_3 + X_5 + 3 >= 0 /\ -X_2 + X_5 + 4 >= 0 /\ X_4 - 1 >= 0 /\ -X_3 + X_4 + 2 >= 0 /\ -X_2 + X_4 + 3 >= 0 /\ -X_3 + 3 >= 0 /\ X_2 - X_3 + 3 >= 0 /\ -X_2 - X_3 + 7 >= 0 /\ -X_2 + X_3 + 4 >= 0 /\ -X_2 + 4 >= 0

This yielded the following problem:
3: T:
(Comp: 1, Cost: 0) koat_start(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(main_Load_1(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5)) [ 0 <= 0 ]
(Comp: ?, Cost: 25) iter_LE_1378(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(iter_Load_1320(ar_2 + 1, ar_0 + 1, ar_1 - 1, ar_3, ar_4, arityPad)) [ ar_3 - ar_4 - 1 >= 0 /\ ar_4 >= 0 /\ ar_3 + ar_4 - 1 >= 0 /\ ar_2 + ar_4 + 13 >= 0 /\ -ar_2 + ar_4 + 4 >= 0 /\ ar_1 + ar_4 + 7 >= 0 /\ -ar_1 + ar_4 + 3 >= 0 /\ ar_0 + ar_4 + 6 >= 0 /\ -ar_0 + ar_4 + 4 >= 0 /\ ar_3 - 1 >= 0 /\ ar_2 + ar_3 + 12 >= 0 /\ -ar_2 + ar_3 + 3 >= 0 /\ ar_1 + ar_3 + 6 >= 0 /\ -ar_1 + ar_3 + 2 >= 0 /\ ar_0 + ar_3 + 5 >= 0 /\ -ar_0 + ar_3 + 3 >= 0 /\ -ar_2 + 4 >= 0 /\ ar_1 - ar_2 + 4 >= 0 /\ -ar_1 - ar_2 + 7 >= 0 /\ ar_0 - ar_2 >= 0 /\ -ar_0 - ar_2 + 8 >= 0 /\ ar_2 + 13 >= 0 /\ ar_1 + ar_2 + 10 >= 0 /\ -ar_1 + ar_2 + 16 >= 0 /\ ar_0 + ar_2 + 13 >= 0 /\ -ar_0 + ar_2 + 17 >= 0 /\ -ar_1 + 3 >= 0 /\ ar_0 - ar_1 + 3 >= 0 /\ -ar_0 - ar_1 + 7 >= 0 /\ ar_1 + 7 >= 0 /\ ar_0 + ar_1 + 10 >= 0 /\ -ar_0 + ar_1 + 4 >= 0 /\ -ar_0 + 4 >= 0 /\ ar_0 + 6 >= 0 /\ ar_0 <= ar_1 /\ 0 <= ar_4 /\ 0 < ar_3 /\ ar_2 + 1 = i571' /\ ar_1 - 1 = i582' /\ ar_0 + 1 = i578' ]
(Comp: ?, Cost: 3) iter_LE_1349(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(iter_LE_1378(ar_1, ar_2, ar_0, ar_3, ar_4, arityPad)) [ ar_3 - ar_4 - 1 >= 0 /\ ar_4 >= 0 /\ ar_3 + ar_4 - 1 >= 0 /\ -ar_2 + ar_4 + 3 >= 0 /\ -ar_1 + ar_4 + 4 >= 0 /\ ar_0 + ar_4 + 13 >= 0 /\ ar_3 - 1 >= 0 /\ -ar_2 + ar_3 + 2 >= 0 /\ -ar_1 + ar_3 + 3 >= 0 /\ ar_0 + ar_3 + 12 >= 0 /\ -ar_2 + 3 >= 0 /\ ar_1 - ar_2 + 3 >= 0 /\ -ar_1 - ar_2 + 7 >= 0 /\ ar_0 - ar_2 + 16 >= 0 /\ -ar_1 + ar_2 + 4 >= 0 /\ ar_0 + ar_2 + 10 >= 0 /\ -ar_1 + 4 >= 0 /\ ar_0 - ar_1 + 17 >= 0 /\ ar_0 + ar_1 + 13 >= 0 /\ ar_0 + 13 >= 0 /\ ar_0 <= ar_1 /\ 0 <= ar_4 /\ 0 < ar_3 ]
(Comp: 1, Cost: 26) main_Load_1(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(iter_Load_1320(i4', i6', i8', ar_0, i4', arityPad)) [ static'1 <= static''' + 1 /\ 0 <= i4' /\ -2 <= i8' /\ -1 <= i8' /\ 0 < ar_0 /\ i8' <= 3 /\ static''' <= ar_1 + 2 /\ i6' <= 4 /\ 0 <= ar_1 /\ i6' < 5 /\ -1 <= i6' /\ 0 <= static''' /\ i8' < 4 /\ 0 <= i6' /\ -1 <= i4' /\ -2 <= i6' /\ 0 <= i8' /\ 0 <= static'1 /\ i4' < ar_0 ]
(Comp: ?, Cost: 6) iter_LE_1349(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(iter_ConstantStackPush_1327(ar_0 + ar_1 - 1, ar_0 - 1, ar_1, ar_2, ar_3, ar_4)) [ ar_3 - ar_4 - 1 >= 0 /\ ar_4 >= 0 /\ ar_3 + ar_4 - 1 >= 0 /\ -ar_2 + ar_4 + 3 >= 0 /\ -ar_1 + ar_4 + 4 >= 0 /\ ar_0 + ar_4 + 13 >= 0 /\ ar_3 - 1 >= 0 /\ -ar_2 + ar_3 + 2 >= 0 /\ -ar_1 + ar_3 + 3 >= 0 /\ ar_0 + ar_3 + 12 >= 0 /\ -ar_2 + 3 >= 0 /\ ar_1 - ar_2 + 3 >= 0 /\ -ar_1 - ar_2 + 7 >= 0 /\ ar_0 - ar_2 + 16 >= 0 /\ -ar_1 + ar_2 + 4 >= 0 /\ ar_0 + ar_2 + 10 >= 0 /\ -ar_1 + 4 >= 0 /\ ar_0 - ar_1 + 17 >= 0 /\ ar_0 + ar_1 + 13 >= 0 /\ ar_0 + 13 >= 0 /\ ar_0 - 1 = i551' /\ 0 <= ar_4 /\ 0 < ar_3 /\ i551' + ar_1 = i562' /\ ar_1 < ar_0 ]
(Comp: ?, Cost: 7) iter_ConstantStackPush_1327(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(iter_LE_1349(ar_1, ar_2, ar_3, ar_4, ar_5, arityPad)) [ ar_4 - ar_5 - 1 >= 0 /\ ar_5 >= 0 /\ ar_4 + ar_5 - 1 >= 0 /\ -ar_3 + ar_5 + 3 >= 0 /\ -ar_2 + ar_5 + 4 >= 0 /\ ar_4 - 1 >= 0 /\ -ar_3 + ar_4 + 2 >= 0 /\ -ar_2 + ar_4 + 3 >= 0 /\ -ar_3 + 3 >= 0 /\ ar_2 - ar_3 + 3 >= 0 /\ -ar_2 - ar_3 + 7 >= 0 /\ -ar_2 + ar_3 + 4 >= 0 /\ -ar_2 + 4 >= 0 /\ -ar_0 + ar_1 + 4 >= 0 /\ 3*ar_3 = i540' /\ 0 <= ar_5 /\ 0 < ar_4 /\ 0 <= i541' /\ ar_0 + i540' = i541' ]
(Comp: ?, Cost: 3) iter_Load_1320(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(iter_ConstantStackPush_1327(ar_0 + ar_1, ar_0, ar_1, ar_2, ar_3, ar_4)) [ ar_3 - ar_4 - 1 >= 0 /\ ar_4 >= 0 /\ ar_3 + ar_4 - 1 >= 0 /\ -ar_2 + ar_4 + 3 >= 0 /\ -ar_1 + ar_4 + 4 >= 0 /\ ar_3 - 1 >= 0 /\ -ar_2 + ar_3 + 2 >= 0 /\ -ar_1 + ar_3 + 3 >= 0 /\ -ar_2 + 3 >= 0 /\ ar_1 - ar_2 + 3 >= 0 /\ -ar_1 - ar_2 + 7 >= 0 /\ -ar_1 + ar_2 + 4 >= 0 /\ -ar_1 + 4 >= 0 /\ 0 <= ar_4 /\ 0 < ar_3 /\ ar_0 + ar_1 = i538' ]
(Comp: ?, Cost: 4) iter_LE_1378(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(iter_Load_1320(ar_2 + 1, ar_0 - 2, ar_1, ar_3, ar_4, arityPad)) [ ar_3 - ar_4 - 1 >= 0 /\ ar_4 >= 0 /\ ar_3 + ar_4 - 1 >= 0 /\ ar_2 + ar_4 + 13 >= 0 /\ -ar_2 + ar_4 + 4 >= 0 /\ ar_1 + ar_4 + 7 >= 0 /\ -ar_1 + ar_4 + 3 >= 0 /\ ar_0 + ar_4 + 6 >= 0 /\ -ar_0 + ar_4 + 4 >= 0 /\ ar_3 - 1 >= 0 /\ ar_2 + ar_3 + 12 >= 0 /\ -ar_2 + ar_3 + 3 >= 0 /\ ar_1 + ar_3 + 6 >= 0 /\ -ar_1 + ar_3 + 2 >= 0 /\ ar_0 + ar_3 + 5 >= 0 /\ -ar_0 + ar_3 + 3 >= 0 /\ -ar_2 + 4 >= 0 /\ ar_1 - ar_2 + 4 >= 0 /\ -ar_1 - ar_2 + 7 >= 0 /\ ar_0 - ar_2 >= 0 /\ -ar_0 - ar_2 + 8 >= 0 /\ ar_2 + 13 >= 0 /\ ar_1 + ar_2 + 10 >= 0 /\ -ar_1 + ar_2 + 16 >= 0 /\ ar_0 + ar_2 + 13 >= 0 /\ -ar_0 + ar_2 + 17 >= 0 /\ -ar_1 + 3 >= 0 /\ ar_0 - ar_1 + 3 >= 0 /\ -ar_0 - ar_1 + 7 >= 0 /\ ar_1 + 7 >= 0 /\ ar_0 + ar_1 + 10 >= 0 /\ -ar_0 + ar_1 + 4 >= 0 /\ -ar_0 + 4 >= 0 /\ ar_0 + 6 >= 0 /\ ar_2 + 1 = i561' /\ 0 <= ar_4 /\ 0 < ar_3 /\ ar_0 - 2 = i566' /\ ar_1 < ar_0 ]
start location: koat_start
leaf cost: 0

A polynomial rank function with
Pol(koat_start) = 11*V_1 + 771
Pol(main_Load_1) = 11*V_1 + 771
Pol(iter_LE_1378) = 8*V_1 + 25*V_2 + 11*V_3 + 671
Pol(iter_Load_1320) = 11*V_1 + 8*V_2 + 25*V_3 + 675
Pol(iter_LE_1349) = 11*V_1 + 8*V_2 + 25*V_3 + 673
Pol(iter_ConstantStackPush_1327) = 11*V_2 + 8*V_3 + 25*V_4 + 675
orients all transitions weakly and the transitions
iter_LE_1378(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(iter_Load_1320(ar_2 + 1, ar_0 + 1, ar_1 - 1, ar_3, ar_4, arityPad)) [ ar_3 - ar_4 - 1 >= 0 /\ ar_4 >= 0 /\ ar_3 + ar_4 - 1 >= 0 /\ ar_2 + ar_4 + 13 >= 0 /\ -ar_2 + ar_4 + 4 >= 0 /\ ar_1 + ar_4 + 7 >= 0 /\ -ar_1 + ar_4 + 3 >= 0 /\ ar_0 + ar_4 + 6 >= 0 /\ -ar_0 + ar_4 + 4 >= 0 /\ ar_3 - 1 >= 0 /\ ar_2 + ar_3 + 12 >= 0 /\ -ar_2 + ar_3 + 3 >= 0 /\ ar_1 + ar_3 + 6 >= 0 /\ -ar_1 + ar_3 + 2 >= 0 /\ ar_0 + ar_3 + 5 >= 0 /\ -ar_0 + ar_3 + 3 >= 0 /\ -ar_2 + 4 >= 0 /\ ar_1 - ar_2 + 4 >= 0 /\ -ar_1 - ar_2 + 7 >= 0 /\ ar_0 - ar_2 >= 0 /\ -ar_0 - ar_2 + 8 >= 0 /\ ar_2 + 13 >= 0 /\ ar_1 + ar_2 + 10 >= 0 /\ -ar_1 + ar_2 + 16 >= 0 /\ ar_0 + ar_2 + 13 >= 0 /\ -ar_0 + ar_2 + 17 >= 0 /\ -ar_1 + 3 >= 0 /\ ar_0 - ar_1 + 3 >= 0 /\ -ar_0 - ar_1 + 7 >= 0 /\ ar_1 + 7 >= 0 /\ ar_0 + ar_1 + 10 >= 0 /\ -ar_0 + ar_1 + 4 >= 0 /\ -ar_0 + 4 >= 0 /\ ar_0 + 6 >= 0 /\ ar_0 <= ar_1 /\ 0 <= ar_4 /\ 0 < ar_3 /\ ar_2 + 1 = i571' /\ ar_1 - 1 = i582' /\ ar_0 + 1 = i578' ]
iter_LE_1378(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(iter_Load_1320(ar_2 + 1, ar_0 - 2, ar_1, ar_3, ar_4, arityPad)) [ ar_3 - ar_4 - 1 >= 0 /\ ar_4 >= 0 /\ ar_3 + ar_4 - 1 >= 0 /\ ar_2 + ar_4 + 13 >= 0 /\ -ar_2 + ar_4 + 4 >= 0 /\ ar_1 + ar_4 + 7 >= 0 /\ -ar_1 + ar_4 + 3 >= 0 /\ ar_0 + ar_4 + 6 >= 0 /\ -ar_0 + ar_4 + 4 >= 0 /\ ar_3 - 1 >= 0 /\ ar_2 + ar_3 + 12 >= 0 /\ -ar_2 + ar_3 + 3 >= 0 /\ ar_1 + ar_3 + 6 >= 0 /\ -ar_1 + ar_3 + 2 >= 0 /\ ar_0 + ar_3 + 5 >= 0 /\ -ar_0 + ar_3 + 3 >= 0 /\ -ar_2 + 4 >= 0 /\ ar_1 - ar_2 + 4 >= 0 /\ -ar_1 - ar_2 + 7 >= 0 /\ ar_0 - ar_2 >= 0 /\ -ar_0 - ar_2 + 8 >= 0 /\ ar_2 + 13 >= 0 /\ ar_1 + ar_2 + 10 >= 0 /\ -ar_1 + ar_2 + 16 >= 0 /\ ar_0 + ar_2 + 13 >= 0 /\ -ar_0 + ar_2 + 17 >= 0 /\ -ar_1 + 3 >= 0 /\ ar_0 - ar_1 + 3 >= 0 /\ -ar_0 - ar_1 + 7 >= 0 /\ ar_1 + 7 >= 0 /\ ar_0 + ar_1 + 10 >= 0 /\ -ar_0 + ar_1 + 4 >= 0 /\ -ar_0 + 4 >= 0 /\ ar_0 + 6 >= 0 /\ ar_2 + 1 = i561' /\ 0 <= ar_4 /\ 0 < ar_3 /\ ar_0 - 2 = i566' /\ ar_1 < ar_0 ]
iter_LE_1349(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(iter_LE_1378(ar_1, ar_2, ar_0, ar_3, ar_4, arityPad)) [ ar_3 - ar_4 - 1 >= 0 /\ ar_4 >= 0 /\ ar_3 + ar_4 - 1 >= 0 /\ -ar_2 + ar_4 + 3 >= 0 /\ -ar_1 + ar_4 + 4 >= 0 /\ ar_0 + ar_4 + 13 >= 0 /\ ar_3 - 1 >= 0 /\ -ar_2 + ar_3 + 2 >= 0 /\ -ar_1 + ar_3 + 3 >= 0 /\ ar_0 + ar_3 + 12 >= 0 /\ -ar_2 + 3 >= 0 /\ ar_1 - ar_2 + 3 >= 0 /\ -ar_1 - ar_2 + 7 >= 0 /\ ar_0 - ar_2 + 16 >= 0 /\ -ar_1 + ar_2 + 4 >= 0 /\ ar_0 + ar_2 + 10 >= 0 /\ -ar_1 + 4 >= 0 /\ ar_0 - ar_1 + 17 >= 0 /\ ar_0 + ar_1 + 13 >= 0 /\ ar_0 + 13 >= 0 /\ ar_0 <= ar_1 /\ 0 <= ar_4 /\ 0 < ar_3 ]
iter_ConstantStackPush_1327(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(iter_LE_1349(ar_1, ar_2, ar_3, ar_4, ar_5, arityPad)) [ ar_4 - ar_5 - 1 >= 0 /\ ar_5 >= 0 /\ ar_4 + ar_5 - 1 >= 0 /\ -ar_3 + ar_5 + 3 >= 0 /\ -ar_2 + ar_5 + 4 >= 0 /\ ar_4 - 1 >= 0 /\ -ar_3 + ar_4 + 2 >= 0 /\ -ar_2 + ar_4 + 3 >= 0 /\ -ar_3 + 3 >= 0 /\ ar_2 - ar_3 + 3 >= 0 /\ -ar_2 - ar_3 + 7 >= 0 /\ -ar_2 + ar_3 + 4 >= 0 /\ -ar_2 + 4 >= 0 /\ -ar_0 + ar_1 + 4 >= 0 /\ 3*ar_3 = i540' /\ 0 <= ar_5 /\ 0 < ar_4 /\ 0 <= i541' /\ ar_0 + i540' = i541' ]
strictly and produces the following problem:
4: T:
(Comp: 1, Cost: 0) koat_start(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(main_Load_1(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5)) [ 0 <= 0 ]
(Comp: 11*ar_0 + 771, Cost: 25) iter_LE_1378(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(iter_Load_1320(ar_2 + 1, ar_0 + 1, ar_1 - 1, ar_3, ar_4, arityPad)) [ ar_3 - ar_4 - 1 >= 0 /\ ar_4 >= 0 /\ ar_3 + ar_4 - 1 >= 0 /\ ar_2 + ar_4 + 13 >= 0 /\ -ar_2 + ar_4 + 4 >= 0 /\ ar_1 + ar_4 + 7 >= 0 /\ -ar_1 + ar_4 + 3 >= 0 /\ ar_0 + ar_4 + 6 >= 0 /\ -ar_0 + ar_4 + 4 >= 0 /\ ar_3 - 1 >= 0 /\ ar_2 + ar_3 + 12 >= 0 /\ -ar_2 + ar_3 + 3 >= 0 /\ ar_1 + ar_3 + 6 >= 0 /\ -ar_1 + ar_3 + 2 >= 0 /\ ar_0 + ar_3 + 5 >= 0 /\ -ar_0 + ar_3 + 3 >= 0 /\ -ar_2 + 4 >= 0 /\ ar_1 - ar_2 + 4 >= 0 /\ -ar_1 - ar_2 + 7 >= 0 /\ ar_0 - ar_2 >= 0 /\ -ar_0 - ar_2 + 8 >= 0 /\ ar_2 + 13 >= 0 /\ ar_1 + ar_2 + 10 >= 0 /\ -ar_1 + ar_2 + 16 >= 0 /\ ar_0 + ar_2 + 13 >= 0 /\ -ar_0 + ar_2 + 17 >= 0 /\ -ar_1 + 3 >= 0 /\ ar_0 - ar_1 + 3 >= 0 /\ -ar_0 - ar_1 + 7 >= 0 /\ ar_1 + 7 >= 0 /\ ar_0 + ar_1 + 10 >= 0 /\ -ar_0 + ar_1 + 4 >= 0 /\ -ar_0 + 4 >= 0 /\ ar_0 + 6 >= 0 /\ ar_0 <= ar_1 /\ 0 <= ar_4 /\ 0 < ar_3 /\ ar_2 + 1 = i571' /\ ar_1 - 1 = i582' /\ ar_0 + 1 = i578' ]
(Comp: 11*ar_0 + 771, Cost: 3) iter_LE_1349(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(iter_LE_1378(ar_1, ar_2, ar_0, ar_3, ar_4, arityPad)) [ ar_3 - ar_4 - 1 >= 0 /\ ar_4 >= 0 /\ ar_3 + ar_4 - 1 >= 0 /\ -ar_2 + ar_4 + 3 >= 0 /\ -ar_1 + ar_4 + 4 >= 0 /\ ar_0 + ar_4 + 13 >= 0 /\ ar_3 - 1 >= 0 /\ -ar_2 + ar_3 + 2 >= 0 /\ -ar_1 + ar_3 + 3 >= 0 /\ ar_0 + ar_3 + 12 >= 0 /\ -ar_2 + 3 >= 0 /\ ar_1 - ar_2 + 3 >= 0 /\ -ar_1 - ar_2 + 7 >= 0 /\ ar_0 - ar_2 + 16 >= 0 /\ -ar_1 + ar_2 + 4 >= 0 /\ ar_0 + ar_2 + 10 >= 0 /\ -ar_1 + 4 >= 0 /\ ar_0 - ar_1 + 17 >= 0 /\ ar_0 + ar_1 + 13 >= 0 /\ ar_0 + 13 >= 0 /\ ar_0 <= ar_1 /\ 0 <= ar_4 /\ 0 < ar_3 ]
(Comp: 1, Cost: 26) main_Load_1(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(iter_Load_1320(i4', i6', i8', ar_0, i4', arityPad)) [ static'1 <= static''' + 1 /\ 0 <= i4' /\ -2 <= i8' /\ -1 <= i8' /\ 0 < ar_0 /\ i8' <= 3 /\ static''' <= ar_1 + 2 /\ i6' <= 4 /\ 0 <= ar_1 /\ i6' < 5 /\ -1 <= i6' /\ 0 <= static''' /\ i8' < 4 /\ 0 <= i6' /\ -1 <= i4' /\ -2 <= i6' /\ 0 <= i8' /\ 0 <= static'1 /\ i4' < ar_0 ]
(Comp: ?, Cost: 6) iter_LE_1349(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(iter_ConstantStackPush_1327(ar_0 + ar_1 - 1, ar_0 - 1, ar_1, ar_2, ar_3, ar_4)) [ ar_3 - ar_4 - 1 >= 0 /\ ar_4 >= 0 /\ ar_3 + ar_4 - 1 >= 0 /\ -ar_2 + ar_4 + 3 >= 0 /\ -ar_1 + ar_4 + 4 >= 0 /\ ar_0 + ar_4 + 13 >= 0 /\ ar_3 - 1 >= 0 /\ -ar_2 + ar_3 + 2 >= 0 /\ -ar_1 + ar_3 + 3 >= 0 /\ ar_0 + ar_3 + 12 >= 0 /\ -ar_2 + 3 >= 0 /\ ar_1 - ar_2 + 3 >= 0 /\ -ar_1 - ar_2 + 7 >= 0 /\ ar_0 - ar_2 + 16 >= 0 /\ -ar_1 + ar_2 + 4 >= 0 /\ ar_0 + ar_2 + 10 >= 0 /\ -ar_1 + 4 >= 0 /\ ar_0 - ar_1 + 17 >= 0 /\ ar_0 + ar_1 + 13 >= 0 /\ ar_0 + 13 >= 0 /\ ar_0 - 1 = i551' /\ 0 <= ar_4 /\ 0 < ar_3 /\ i551' + ar_1 = i562' /\ ar_1 < ar_0 ]
(Comp: 11*ar_0 + 771, Cost: 7) iter_ConstantStackPush_1327(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(iter_LE_1349(ar_1, ar_2, ar_3, ar_4, ar_5, arityPad)) [ ar_4 - ar_5 - 1 >= 0 /\ ar_5 >= 0 /\ ar_4 + ar_5 - 1 >= 0 /\ -ar_3 + ar_5 + 3 >= 0 /\ -ar_2 + ar_5 + 4 >= 0 /\ ar_4 - 1 >= 0 /\ -ar_3 + ar_4 + 2 >= 0 /\ -ar_2 + ar_4 + 3 >= 0 /\ -ar_3 + 3 >= 0 /\ ar_2 - ar_3 + 3 >= 0 /\ -ar_2 - ar_3 + 7 >= 0 /\ -ar_2 + ar_3 + 4 >= 0 /\ -ar_2 + 4 >= 0 /\ -ar_0 + ar_1 + 4 >= 0 /\ 3*ar_3 = i540' /\ 0 <= ar_5 /\ 0 < ar_4 /\ 0 <= i541' /\ ar_0 + i540' = i541' ]
(Comp: ?, Cost: 3) iter_Load_1320(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(iter_ConstantStackPush_1327(ar_0 + ar_1, ar_0, ar_1, ar_2, ar_3, ar_4)) [ ar_3 - ar_4 - 1 >= 0 /\ ar_4 >= 0 /\ ar_3 + ar_4 - 1 >= 0 /\ -ar_2 + ar_4 + 3 >= 0 /\ -ar_1 + ar_4 + 4 >= 0 /\ ar_3 - 1 >= 0 /\ -ar_2 + ar_3 + 2 >= 0 /\ -ar_1 + ar_3 + 3 >= 0 /\ -ar_2 + 3 >= 0 /\ ar_1 - ar_2 + 3 >= 0 /\ -ar_1 - ar_2 + 7 >= 0 /\ -ar_1 + ar_2 + 4 >= 0 /\ -ar_1 + 4 >= 0 /\ 0 <= ar_4 /\ 0 < ar_3 /\ ar_0 + ar_1 = i538' ]
(Comp: 11*ar_0 + 771, Cost: 4) iter_LE_1378(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(iter_Load_1320(ar_2 + 1, ar_0 - 2, ar_1, ar_3, ar_4, arityPad)) [ ar_3 - ar_4 - 1 >= 0 /\ ar_4 >= 0 /\ ar_3 + ar_4 - 1 >= 0 /\ ar_2 + ar_4 + 13 >= 0 /\ -ar_2 + ar_4 + 4 >= 0 /\ ar_1 + ar_4 + 7 >= 0 /\ -ar_1 + ar_4 + 3 >= 0 /\ ar_0 + ar_4 + 6 >= 0 /\ -ar_0 + ar_4 + 4 >= 0 /\ ar_3 - 1 >= 0 /\ ar_2 + ar_3 + 12 >= 0 /\ -ar_2 + ar_3 + 3 >= 0 /\ ar_1 + ar_3 + 6 >= 0 /\ -ar_1 + ar_3 + 2 >= 0 /\ ar_0 + ar_3 + 5 >= 0 /\ -ar_0 + ar_3 + 3 >= 0 /\ -ar_2 + 4 >= 0 /\ ar_1 - ar_2 + 4 >= 0 /\ -ar_1 - ar_2 + 7 >= 0 /\ ar_0 - ar_2 >= 0 /\ -ar_0 - ar_2 + 8 >= 0 /\ ar_2 + 13 >= 0 /\ ar_1 + ar_2 + 10 >= 0 /\ -ar_1 + ar_2 + 16 >= 0 /\ ar_0 + ar_2 + 13 >= 0 /\ -ar_0 + ar_2 + 17 >= 0 /\ -ar_1 + 3 >= 0 /\ ar_0 - ar_1 + 3 >= 0 /\ -ar_0 - ar_1 + 7 >= 0 /\ ar_1 + 7 >= 0 /\ ar_0 + ar_1 + 10 >= 0 /\ -ar_0 + ar_1 + 4 >= 0 /\ -ar_0 + 4 >= 0 /\ ar_0 + 6 >= 0 /\ ar_2 + 1 = i561' /\ 0 <= ar_4 /\ 0 < ar_3 /\ ar_0 - 2 = i566' /\ ar_1 < ar_0 ]
start location: koat_start
leaf cost: 0

Repeatedly propagating knowledge in problem 4 produces the following problem:
5: T:
(Comp: 1, Cost: 0) koat_start(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(main_Load_1(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5)) [ 0 <= 0 ]
(Comp: 11*ar_0 + 771, Cost: 25) iter_LE_1378(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(iter_Load_1320(ar_2 + 1, ar_0 + 1, ar_1 - 1, ar_3, ar_4, arityPad)) [ ar_3 - ar_4 - 1 >= 0 /\ ar_4 >= 0 /\ ar_3 + ar_4 - 1 >= 0 /\ ar_2 + ar_4 + 13 >= 0 /\ -ar_2 + ar_4 + 4 >= 0 /\ ar_1 + ar_4 + 7 >= 0 /\ -ar_1 + ar_4 + 3 >= 0 /\ ar_0 + ar_4 + 6 >= 0 /\ -ar_0 + ar_4 + 4 >= 0 /\ ar_3 - 1 >= 0 /\ ar_2 + ar_3 + 12 >= 0 /\ -ar_2 + ar_3 + 3 >= 0 /\ ar_1 + ar_3 + 6 >= 0 /\ -ar_1 + ar_3 + 2 >= 0 /\ ar_0 + ar_3 + 5 >= 0 /\ -ar_0 + ar_3 + 3 >= 0 /\ -ar_2 + 4 >= 0 /\ ar_1 - ar_2 + 4 >= 0 /\ -ar_1 - ar_2 + 7 >= 0 /\ ar_0 - ar_2 >= 0 /\ -ar_0 - ar_2 + 8 >= 0 /\ ar_2 + 13 >= 0 /\ ar_1 + ar_2 + 10 >= 0 /\ -ar_1 + ar_2 + 16 >= 0 /\ ar_0 + ar_2 + 13 >= 0 /\ -ar_0 + ar_2 + 17 >= 0 /\ -ar_1 + 3 >= 0 /\ ar_0 - ar_1 + 3 >= 0 /\ -ar_0 - ar_1 + 7 >= 0 /\ ar_1 + 7 >= 0 /\ ar_0 + ar_1 + 10 >= 0 /\ -ar_0 + ar_1 + 4 >= 0 /\ -ar_0 + 4 >= 0 /\ ar_0 + 6 >= 0 /\ ar_0 <= ar_1 /\ 0 <= ar_4 /\ 0 < ar_3 /\ ar_2 + 1 = i571' /\ ar_1 - 1 = i582' /\ ar_0 + 1 = i578' ]
(Comp: 11*ar_0 + 771, Cost: 3) iter_LE_1349(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(iter_LE_1378(ar_1, ar_2, ar_0, ar_3, ar_4, arityPad)) [ ar_3 - ar_4 - 1 >= 0 /\ ar_4 >= 0 /\ ar_3 + ar_4 - 1 >= 0 /\ -ar_2 + ar_4 + 3 >= 0 /\ -ar_1 + ar_4 + 4 >= 0 /\ ar_0 + ar_4 + 13 >= 0 /\ ar_3 - 1 >= 0 /\ -ar_2 + ar_3 + 2 >= 0 /\ -ar_1 + ar_3 + 3 >= 0 /\ ar_0 + ar_3 + 12 >= 0 /\ -ar_2 + 3 >= 0 /\ ar_1 - ar_2 + 3 >= 0 /\ -ar_1 - ar_2 + 7 >= 0 /\ ar_0 - ar_2 + 16 >= 0 /\ -ar_1 + ar_2 + 4 >= 0 /\ ar_0 + ar_2 + 10 >= 0 /\ -ar_1 + 4 >= 0 /\ ar_0 - ar_1 + 17 >= 0 /\ ar_0 + ar_1 + 13 >= 0 /\ ar_0 + 13 >= 0 /\ ar_0 <= ar_1 /\ 0 <= ar_4 /\ 0 < ar_3 ]
(Comp: 1, Cost: 26) main_Load_1(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(iter_Load_1320(i4', i6', i8', ar_0, i4', arityPad)) [ static'1 <= static''' + 1 /\ 0 <= i4' /\ -2 <= i8' /\ -1 <= i8' /\ 0 < ar_0 /\ i8' <= 3 /\ static''' <= ar_1 + 2 /\ i6' <= 4 /\ 0 <= ar_1 /\ i6' < 5 /\ -1 <= i6' /\ 0 <= static''' /\ i8' < 4 /\ 0 <= i6' /\ -1 <= i4' /\ -2 <= i6' /\ 0 <= i8' /\ 0 <= static'1 /\ i4' < ar_0 ]
(Comp: 11*ar_0 + 771, Cost: 6) iter_LE_1349(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(iter_ConstantStackPush_1327(ar_0 + ar_1 - 1, ar_0 - 1, ar_1, ar_2, ar_3, ar_4)) [ ar_3 - ar_4 - 1 >= 0 /\ ar_4 >= 0 /\ ar_3 + ar_4 - 1 >= 0 /\ -ar_2 + ar_4 + 3 >= 0 /\ -ar_1 + ar_4 + 4 >= 0 /\ ar_0 + ar_4 + 13 >= 0 /\ ar_3 - 1 >= 0 /\ -ar_2 + ar_3 + 2 >= 0 /\ -ar_1 + ar_3 + 3 >= 0 /\ ar_0 + ar_3 + 12 >= 0 /\ -ar_2 + 3 >= 0 /\ ar_1 - ar_2 + 3 >= 0 /\ -ar_1 - ar_2 + 7 >= 0 /\ ar_0 - ar_2 + 16 >= 0 /\ -ar_1 + ar_2 + 4 >= 0 /\ ar_0 + ar_2 + 10 >= 0 /\ -ar_1 + 4 >= 0 /\ ar_0 - ar_1 + 17 >= 0 /\ ar_0 + ar_1 + 13 >= 0 /\ ar_0 + 13 >= 0 /\ ar_0 - 1 = i551' /\ 0 <= ar_4 /\ 0 < ar_3 /\ i551' + ar_1 = i562' /\ ar_1 < ar_0 ]
(Comp: 11*ar_0 + 771, Cost: 7) iter_ConstantStackPush_1327(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(iter_LE_1349(ar_1, ar_2, ar_3, ar_4, ar_5, arityPad)) [ ar_4 - ar_5 - 1 >= 0 /\ ar_5 >= 0 /\ ar_4 + ar_5 - 1 >= 0 /\ -ar_3 + ar_5 + 3 >= 0 /\ -ar_2 + ar_5 + 4 >= 0 /\ ar_4 - 1 >= 0 /\ -ar_3 + ar_4 + 2 >= 0 /\ -ar_2 + ar_4 + 3 >= 0 /\ -ar_3 + 3 >= 0 /\ ar_2 - ar_3 + 3 >= 0 /\ -ar_2 - ar_3 + 7 >= 0 /\ -ar_2 + ar_3 + 4 >= 0 /\ -ar_2 + 4 >= 0 /\ -ar_0 + ar_1 + 4 >= 0 /\ 3*ar_3 = i540' /\ 0 <= ar_5 /\ 0 < ar_4 /\ 0 <= i541' /\ ar_0 + i540' = i541' ]
(Comp: 22*ar_0 + 1543, Cost: 3) iter_Load_1320(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(iter_ConstantStackPush_1327(ar_0 + ar_1, ar_0, ar_1, ar_2, ar_3, ar_4)) [ ar_3 - ar_4 - 1 >= 0 /\ ar_4 >= 0 /\ ar_3 + ar_4 - 1 >= 0 /\ -ar_2 + ar_4 + 3 >= 0 /\ -ar_1 + ar_4 + 4 >= 0 /\ ar_3 - 1 >= 0 /\ -ar_2 + ar_3 + 2 >= 0 /\ -ar_1 + ar_3 + 3 >= 0 /\ -ar_2 + 3 >= 0 /\ ar_1 - ar_2 + 3 >= 0 /\ -ar_1 - ar_2 + 7 >= 0 /\ -ar_1 + ar_2 + 4 >= 0 /\ -ar_1 + 4 >= 0 /\ 0 <= ar_4 /\ 0 < ar_3 /\ ar_0 + ar_1 = i538' ]
(Comp: 11*ar_0 + 771, Cost: 4) iter_LE_1378(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(iter_Load_1320(ar_2 + 1, ar_0 - 2, ar_1, ar_3, ar_4, arityPad)) [ ar_3 - ar_4 - 1 >= 0 /\ ar_4 >= 0 /\ ar_3 + ar_4 - 1 >= 0 /\ ar_2 + ar_4 + 13 >= 0 /\ -ar_2 + ar_4 + 4 >= 0 /\ ar_1 + ar_4 + 7 >= 0 /\ -ar_1 + ar_4 + 3 >= 0 /\ ar_0 + ar_4 + 6 >= 0 /\ -ar_0 + ar_4 + 4 >= 0 /\ ar_3 - 1 >= 0 /\ ar_2 + ar_3 + 12 >= 0 /\ -ar_2 + ar_3 + 3 >= 0 /\ ar_1 + ar_3 + 6 >= 0 /\ -ar_1 + ar_3 + 2 >= 0 /\ ar_0 + ar_3 + 5 >= 0 /\ -ar_0 + ar_3 + 3 >= 0 /\ -ar_2 + 4 >= 0 /\ ar_1 - ar_2 + 4 >= 0 /\ -ar_1 - ar_2 + 7 >= 0 /\ ar_0 - ar_2 >= 0 /\ -ar_0 - ar_2 + 8 >= 0 /\ ar_2 + 13 >= 0 /\ ar_1 + ar_2 + 10 >= 0 /\ -ar_1 + ar_2 + 16 >= 0 /\ ar_0 + ar_2 + 13 >= 0 /\ -ar_0 + ar_2 + 17 >= 0 /\ -ar_1 + 3 >= 0 /\ ar_0 - ar_1 + 3 >= 0 /\ -ar_0 - ar_1 + 7 >= 0 /\ ar_1 + 7 >= 0 /\ ar_0 + ar_1 + 10 >= 0 /\ -ar_0 + ar_1 + 4 >= 0 /\ -ar_0 + 4 >= 0 /\ ar_0 + 6 >= 0 /\ ar_2 + 1 = i561' /\ 0 <= ar_4 /\ 0 < ar_3 /\ ar_0 - 2 = i566' /\ ar_1 < ar_0 ]
start location: koat_start
leaf cost: 0

Complexity upper bound 561*ar_0 + 39350

Time: 1.140 sec (SMT: 0.961 sec)

(0) Obligation:

(1) JBCToGraph (BOTH CONCRETE BOUNDS(ID, ID) transformation)

(2) Obligation:

(3) TerminationGraphToComplexityProof (BOTH CONCRETE BOUNDS(ID, ADD(3)) transformation)

(4) Obligation:

(5) JBCGraphEdgesToCpxIntTrsProof (CONCRETE UPPER BOUND(ID) transformation)

(6) Obligation:

(7) StraightLineCodeCompressionProof (BOTH CONCRETE BOUNDS(ID, ID) transformation)

(8) Obligation:

(9) MovedArithmeticFromConstraintsProof (BOTH CONCRETE BOUNDS(ID, ID) transformation)

(10) Obligation:

(11) ExpressionSimplificationProof (BOTH CONCRETE BOUNDS(ID, ID) transformation)

(12) Obligation:

(13) JBCGraphEdgesToCpxIntTrsProof (CONCRETE UPPER BOUND(ID) transformation)

(14) Obligation:

(15) StraightLineCodeCompressionProof (BOTH CONCRETE BOUNDS(ID, ID) transformation)

(16) Obligation:

(17) RemoveDivModProof (CONCRETE UPPER BOUND(ID) transformation)

(18) Obligation:

(19) MovedArithmeticFromConstraintsProof (BOTH CONCRETE BOUNDS(ID, ID) transformation)

(20) Obligation:

(21) ExpressionSimplificationProof (BOTH CONCRETE BOUNDS(ID, ID) transformation)

(22) Obligation:

(23) TerminationGraphToComplexityProof (BOTH CONCRETE BOUNDS(ID, ADD(3)) transformation)

(24) Obligation:

(25) JBCGraphEdgesToCpxIntTrsProof (CONCRETE UPPER BOUND(ID) transformation)

(26) Obligation:

(27) StraightLineCodeCompressionProof (BOTH CONCRETE BOUNDS(ID, ID) transformation)

(28) Obligation:

(29) WeightedIntTrsUnneededArgumentFilterProof (CONCRETE UPPER BOUND(ID) transformation)

(30) Obligation:

(31) MovedArithmeticFromConstraintsProof (BOTH CONCRETE BOUNDS(ID, ID) transformation)

(32) Obligation:

(33) ExpressionSimplificationProof (BOTH CONCRETE BOUNDS(ID, ID) transformation)

(34) Obligation:

(35) koat Proof (EQUIVALENT transformation)

(36) BOUNDS(CONSTANT, 39350 + 561 * |#0|)