time complexity proof of /tmp/tmpYSk55x/PastaA1.jar

The time complexity of the given JBC problem could be proven to be BOUNDS(CONSTANT, 40 + 43 * |#0| + 10 * |#0|^2).

0 JBC problem

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

↳2 JBCTerminationGraph

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

↳4 JBCComplexityEdges

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

    ↳6 WeightedIntTrs

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

        ↳8 WeightedIntTrs

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

        ↳10 WeightedIntTrs

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

        ↳12 WeightedIntTrs

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

    ↳14 WeightedIntTrs

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

        ↳16 WeightedIntTrs

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

        ↳18 WeightedIntTrs

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

        ↳20 WeightedIntTrs

        ↳21 koat Proof (⇔, 174 ms)

        ↳22 BOUNDS(CONSTANT, 81 + 143 * |#0| + 30 * |#0|^2)

↳23 TerminationGraphToComplexityProof (BOTH CONCRETE BOUNDS(ID, ADD(4)), 11 ms)

↳24 JBCComplexityEdges

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

    ↳26 WeightedIntTrs

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

    ↳28 WeightedIntTrs

    ↳29 WeightedIntTrsUnneededArgumentFilterProof (CONCRETE UPPER BOUND(ID), 7 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 (⇔, 52 ms)

    ↳36 BOUNDS(CONSTANT, 36 + 43 * |#0| + 10 * |#0|^2)

(0) Obligation:

Need to prove time_complexity of the following program:

/**
 * Example taken from "A Term Rewriting Approach to the Automated Termination
 * Analysis of Imperative Programs" (http://www.cs.unm.edu/~spf/papers/2009-02.pdf)
 * and converted to Java.
 */

public class PastaA1 {
    public static void main(int x) {
        while (x > 0) {
            int y = 0;
            while (y < x) {
                y++;
            }
            x--;
        }
    }
}

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

Constructed TerminationGraph.

(2) Obligation:

Termination Graph based on JBC Program:
PastaA1.main(I)V: Graph of 58 nodes with 1 SCC.

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

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

(4) Obligation:

Set of 54 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 54 jbc graph edges to a weighted ITS with 54 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 54 rules
Start term: main_Load_1(#0, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_Load_1(i1, env, static) -{0,0}> main_Load_4(i1, env, static) :|: 0 >= 0
main_Load_4(i1, env, static) -{0,0}> langle_clinit_rangle_ConstantStackPush_5(i1, env, static) :|: 0 >= 0
langle_clinit_rangle_ConstantStackPush_5(i1, env, static) -{1,1}> langle_clinit_rangle_ArrayCreate_12(iconst_0, i1, env, static) :|: iconst_0 = 0
langle_clinit_rangle_ArrayCreate_12(iconst_0, i1, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_14(a2, i1, iconst_0, env, static) :|: a2 = 2 && iconst_0 = 0 && 0 < a2
langle_clinit_rangle_FieldAccess_14(a2, i1, iconst_0, env, static) -{1,1}> langle_clinit_rangle_New_16(i1, env, static') :|: 0 <= a2 && iconst_0 = 0 && static' <= static + a2 && 0 <= static && 0 < a2
langle_clinit_rangle_New_16(i1, env, static) -{0,0}> langle_clinit_rangle_New_18(i1, env, static) :|: 0 >= 0
langle_clinit_rangle_New_18(i1, env, static) -{0,0}> langle_clinit_rangle_New_19(i1, env, static) :|: 0 <= static
langle_clinit_rangle_New_19(i1, env, static) -{1,1}> langle_clinit_rangle_Duplicate_20(o2, i1, env, static) :|: 0 < o2 && o2 = 1
langle_clinit_rangle_Duplicate_20(o2, i1, env, static) -{1,1}> langle_clinit_rangle_ConstantStackPush_22(o2, i1, env, static) :|: 0 < o2
langle_clinit_rangle_ConstantStackPush_22(o2, i1, env, static) -{1,1}> langle_clinit_rangle_InvokeMethod_23(o2, NULL, i1, env, static) :|: NULL = 0 && 0 < o2
langle_clinit_rangle_InvokeMethod_23(o2, NULL, i1, env, static) -{1,1}> langle_init_rangle_Load_24(o2, i1, env, static) :|: NULL = 0 && 0 < o2
langle_init_rangle_Load_24(o2, i1, env, static) -{1,1}> langle_init_rangle_InvokeMethod_26(o2, i1, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_26(o2, i1, env, static) -{1,1}> langle_init_rangle_Load_28(o2, i1, env, static) :|: 0 < o2
langle_init_rangle_Load_28(o2, i1, env, static) -{1,1}> langle_init_rangle_InvokeMethod_30(o2, i1, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_30(o2, i1, env, static) -{1,1}> langle_init_rangle_Return_32(o2, i1, env, static) :|: 0 < o2
langle_init_rangle_Return_32(o2, i1, env, static) -{1,1}> langle_init_rangle_Return_34(o2, i1, env, static) :|: 0 < o2
langle_init_rangle_Return_34(o2, i1, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_36(o2, i1, env, static) :|: 0 < o2
langle_clinit_rangle_FieldAccess_36(o2, i1, env, static) -{1,1}> langle_clinit_rangle_Return_39(i1, env, static') :|: 0 < o2 && 0 <= o2 && 0 <= static && static' <= static + o2
langle_clinit_rangle_Return_39(i1, env, static) -{1,1}> main_Load_41(i1, env, static) :|: 0 >= 0
main_Load_41(i1, env, static) -{0,0}> main_Load_42(i1, env, static) :|: 0 >= 0
main_Load_42(i1, env, static) -{0,0}> main_Load_43(i1, env, static) :|: 0 <= static
main_Load_43(i1, env, static) -{0,0}> main_Load_46(i1, env, static) :|: 0 >= 0
main_Load_46(i1, env, static) -{0,0}> main_Load_48(i1, env, static) :|: 0 >= 0
main_Load_48(i1, env, static) -{1,1}> main_LE_52(i1, env, static) :|: 0 >= 0
main_LE_52(i9, env, static) -{0,0}> main_LE_53(i9, env, static) :|: i9 <= 0
main_LE_52(i10, env, static) -{0,0}> main_LE_54(i10, env, static) :|: 1 <= i10
main_LE_54(i10, env, static) -{1,1}> main_ConstantStackPush_58(i10, env, static) :|: 1 <= i10 && 0 < i10
main_ConstantStackPush_58(i10, env, static) -{0,0}> main_ConstantStackPush_434(i10, i10, env, static) :|: 1 <= i10
main_ConstantStackPush_434(i95, i151, env, static) -{1,1}> main_Store_437(i95, iconst_0, i151, env, static) :|: 1 <= i151 && 1 <= i95 && iconst_0 = 0
main_Store_437(i95, iconst_0, i151, env, static) -{1,1}> main_Load_438(i95, i151, iconst_0, env, static) :|: 1 <= i151 && 1 <= i95 && iconst_0 = 0
main_Load_438(i95, i151, iconst_0, env, static) -{1,1}> main_Load_439(i95, iconst_0, i151, env, static) :|: 1 <= i151 && 1 <= i95 && iconst_0 = 0
main_Load_439(i95, iconst_0, i151, env, static) -{1,1}> main_GE_441(i95, iconst_0, i151, env, static) :|: 1 <= i151 && 1 <= i95 && iconst_0 = 0
main_GE_441(i95, iconst_0, i151, env, static) -{1,1}> main_Inc_446(i95, i151, iconst_0, env, static) :|: iconst_0 < i151 && 1 <= i151 && 1 <= i95 && iconst_0 = 0
main_Inc_446(i95, i151, iconst_0, env, static) -{1,1}> main_JMP_447(i95, i151, iconst_1, env, static) :|: 1 <= i151 && 1 <= i95 && iconst_1 = 1 && iconst_0 = 0
main_JMP_447(i95, i151, iconst_1, env, static) -{1,1}> main_Load_448(i95, i151, iconst_1, env, static) :|: 1 <= i151 && 1 <= i95 && iconst_1 = 1
main_Load_448(i95, i151, iconst_1, env, static) -{0,0}> main_Load_477(i95, i151, iconst_1, env, static) :|: iconst_1 <= 2 && 1 <= iconst_1 && 1 <= i151 && 1 <= i95 && iconst_1 = 1
main_Load_477(i95, i160, i161, env, static) -{0,0}> main_Load_517(i95, i160, i161, env, static) :|: i161 <= 2 && 1 <= i160 && 1 <= i95 && 1 <= i161 && i161 <= 3
main_Load_517(i95, i180, i181, env, static) -{0,0}> main_Load_554(i95, i180, i181, env, static) :|: 1 <= i95 && 1 <= i181 && 1 <= i180 && i181 <= 3
main_Load_554(i95, i194, i195, env, static) -{1,1}> main_Load_558(i95, i195, i194, env, static) :|: 1 <= i95 && 1 <= i195
main_Load_558(i95, i195, i194, env, static) -{1,1}> main_GE_569(i95, i195, i194, env, static) :|: 1 <= i95 && 1 <= i195
main_GE_569(i95, i195, i194, env, static) -{0,0}> main_GE_571(i95, i195, i194, env, static) :|: 1 <= i95 && i194 <= i195 && 1 <= i195
main_GE_569(i95, i195, i194, env, static) -{0,0}> main_GE_572(i95, i195, i194, env, static) :|: 1 <= i95 && 1 <= i195 && i195 < i194
main_GE_571(i95, i195, i194, env, static) -{1,1}> main_Inc_573(i95, i194, env, static) :|: 1 <= i95 && i194 <= i195 && 1 <= i195
main_GE_572(i95, i195, i194, env, static) -{1,1}> main_Inc_574(i95, i194, i195, env, static) :|: 1 <= i95 && 2 <= i194 && 1 <= i195 && i195 < i194
main_Inc_573(i95, i194, env, static) -{1,1}> main_JMP_575(i95, i204, env, static) :|: i194 + -1 = i204 && 1 <= i95
main_Inc_574(i95, i194, i195, env, static) -{1,1}> main_JMP_576(i95, i194, i205, env, static) :|: i195 + 1 = i205 && 2 <= i205 && 1 <= i95 && 2 <= i194 && 1 <= i195
main_JMP_575(i95, i204, env, static) -{1,1}> main_Load_578(i95, i204, env, static) :|: 1 <= i95
main_JMP_576(i95, i194, i205, env, static) -{1,1}> main_Load_584(i95, i194, i205, env, static) :|: 2 <= i205 && 1 <= i95 && 2 <= i194
main_Load_578(i95, i204, env, static) -{1,1}> main_LE_589(i95, i204, env, static) :|: 1 <= i95
main_Load_584(i95, i194, i205, env, static) -{0,0}> main_Load_554(i95, i194, i205, env, static) :|: 1 <= i205 && 2 <= i205 && 1 <= i95 && 2 <= i194
main_LE_589(i95, i218, env, static) -{0,0}> main_LE_590(i95, i218, env, static) :|: 1 <= i95 && i218 <= 0
main_LE_589(i95, i219, env, static) -{0,0}> main_LE_591(i95, i219, env, static) :|: 1 <= i219 && 1 <= i95
main_LE_591(i95, i219, env, static) -{1,1}> main_ConstantStackPush_593(i95, i219, env, static) :|: 1 <= i219 && 1 <= i95 && 0 < i219
main_ConstantStackPush_593(i95, i219, env, static) -{0,0}> main_ConstantStackPush_434(i95, i219, env, static) :|: 1 <= i219 && 1 <= i95

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

obtained
main_Load_1(i1, env, static) -{16,16}> main_LE_52(i1, env, static'1) :|: 0 >= 0 && static'1 <= static''' + 1 && 0 <= 2 && 0 <= static''' && static''' <= static + 2 && 0 < 1 && 0 <= 1 && 0 <= static && 0 <= static'1 && 0 < 2
by chaining
main_Load_1(i1, env, static) -{0,0}> main_Load_4(i1, env, static) :|: 0 >= 0
main_Load_4(i1, env, static) -{0,0}> langle_clinit_rangle_ConstantStackPush_5(i1, env, static) :|: 0 >= 0
langle_clinit_rangle_ConstantStackPush_5(i1, env, static) -{1,1}> langle_clinit_rangle_ArrayCreate_12(iconst_0, i1, env, static) :|: iconst_0 = 0
langle_clinit_rangle_ArrayCreate_12(iconst_0, i1, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_14(a2, i1, iconst_0, env, static) :|: a2 = 2 && iconst_0 = 0 && 0 < a2
langle_clinit_rangle_FieldAccess_14(a2, i1, iconst_0, env, static) -{1,1}> langle_clinit_rangle_New_16(i1, env, static') :|: 0 <= a2 && iconst_0 = 0 && static' <= static + a2 && 0 <= static && 0 < a2
langle_clinit_rangle_New_16(i1, env, static) -{0,0}> langle_clinit_rangle_New_18(i1, env, static) :|: 0 >= 0
langle_clinit_rangle_New_18(i1, env, static) -{0,0}> langle_clinit_rangle_New_19(i1, env, static) :|: 0 <= static
langle_clinit_rangle_New_19(i1, env, static) -{1,1}> langle_clinit_rangle_Duplicate_20(o2, i1, env, static) :|: 0 < o2 && o2 = 1
langle_clinit_rangle_Duplicate_20(o2, i1, env, static) -{1,1}> langle_clinit_rangle_ConstantStackPush_22(o2, i1, env, static) :|: 0 < o2
langle_clinit_rangle_ConstantStackPush_22(o2, i1, env, static) -{1,1}> langle_clinit_rangle_InvokeMethod_23(o2, NULL, i1, env, static) :|: NULL = 0 && 0 < o2
langle_clinit_rangle_InvokeMethod_23(o2, NULL, i1, env, static) -{1,1}> langle_init_rangle_Load_24(o2, i1, env, static) :|: NULL = 0 && 0 < o2
langle_init_rangle_Load_24(o2, i1, env, static) -{1,1}> langle_init_rangle_InvokeMethod_26(o2, i1, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_26(o2, i1, env, static) -{1,1}> langle_init_rangle_Load_28(o2, i1, env, static) :|: 0 < o2
langle_init_rangle_Load_28(o2, i1, env, static) -{1,1}> langle_init_rangle_InvokeMethod_30(o2, i1, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_30(o2, i1, env, static) -{1,1}> langle_init_rangle_Return_32(o2, i1, env, static) :|: 0 < o2
langle_init_rangle_Return_32(o2, i1, env, static) -{1,1}> langle_init_rangle_Return_34(o2, i1, env, static) :|: 0 < o2
langle_init_rangle_Return_34(o2, i1, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_36(o2, i1, env, static) :|: 0 < o2
langle_clinit_rangle_FieldAccess_36(o2, i1, env, static) -{1,1}> langle_clinit_rangle_Return_39(i1, env, static') :|: 0 < o2 && 0 <= o2 && 0 <= static && static' <= static + o2
langle_clinit_rangle_Return_39(i1, env, static) -{1,1}> main_Load_41(i1, env, static) :|: 0 >= 0
main_Load_41(i1, env, static) -{0,0}> main_Load_42(i1, env, static) :|: 0 >= 0
main_Load_42(i1, env, static) -{0,0}> main_Load_43(i1, env, static) :|: 0 <= static
main_Load_43(i1, env, static) -{0,0}> main_Load_46(i1, env, static) :|: 0 >= 0
main_Load_46(i1, env, static) -{0,0}> main_Load_48(i1, env, static) :|: 0 >= 0
main_Load_48(i1, env, static) -{1,1}> main_LE_52(i1, env, static) :|: 0 >= 0

obtained
main_LE_52(i10, env, static) -{1,1}> main_ConstantStackPush_434(i10, i10, env, static) :|: 1 <= i10 && 0 < i10
by chaining
main_LE_52(i10, env, static) -{0,0}> main_LE_54(i10, env, static) :|: 1 <= i10
main_LE_54(i10, env, static) -{1,1}> main_ConstantStackPush_58(i10, env, static) :|: 1 <= i10 && 0 < i10
main_ConstantStackPush_58(i10, env, static) -{0,0}> main_ConstantStackPush_434(i10, i10, env, static) :|: 1 <= i10

obtained
main_ConstantStackPush_434(i95, i151, env, static) -{7,7}> main_Load_554(i95, i151, 1, env, static) :|: 1 <= i151 && 1 <= 3 && 1 <= i95 && 0 < i151 && 1 <= 1 && 1 <= 2
by chaining
main_ConstantStackPush_434(i95, i151, env, static) -{1,1}> main_Store_437(i95, iconst_0, i151, env, static) :|: 1 <= i151 && 1 <= i95 && iconst_0 = 0
main_Store_437(i95, iconst_0, i151, env, static) -{1,1}> main_Load_438(i95, i151, iconst_0, env, static) :|: 1 <= i151 && 1 <= i95 && iconst_0 = 0
main_Load_438(i95, i151, iconst_0, env, static) -{1,1}> main_Load_439(i95, iconst_0, i151, env, static) :|: 1 <= i151 && 1 <= i95 && iconst_0 = 0
main_Load_439(i95, iconst_0, i151, env, static) -{1,1}> main_GE_441(i95, iconst_0, i151, env, static) :|: 1 <= i151 && 1 <= i95 && iconst_0 = 0
main_GE_441(i95, iconst_0, i151, env, static) -{1,1}> main_Inc_446(i95, i151, iconst_0, env, static) :|: iconst_0 < i151 && 1 <= i151 && 1 <= i95 && iconst_0 = 0
main_Inc_446(i95, i151, iconst_0, env, static) -{1,1}> main_JMP_447(i95, i151, iconst_1, env, static) :|: 1 <= i151 && 1 <= i95 && iconst_1 = 1 && iconst_0 = 0
main_JMP_447(i95, i151, iconst_1, env, static) -{1,1}> main_Load_448(i95, i151, iconst_1, env, static) :|: 1 <= i151 && 1 <= i95 && iconst_1 = 1
main_Load_448(i95, i151, iconst_1, env, static) -{0,0}> main_Load_477(i95, i151, iconst_1, env, static) :|: iconst_1 <= 2 && 1 <= iconst_1 && 1 <= i151 && 1 <= i95 && iconst_1 = 1
main_Load_477(i95, i160, i161, env, static) -{0,0}> main_Load_517(i95, i160, i161, env, static) :|: i161 <= 2 && 1 <= i160 && 1 <= i95 && 1 <= i161 && i161 <= 3
main_Load_517(i95, i180, i181, env, static) -{0,0}> main_Load_554(i95, i180, i181, env, static) :|: 1 <= i95 && 1 <= i181 && 1 <= i180 && i181 <= 3

obtained
main_Load_554(i95, i194, i195, env, static) -{2,2}> main_GE_569(i95, i195, i194, env, static) :|: 1 <= i95 && 1 <= i195
by chaining
main_Load_554(i95, i194, i195, env, static) -{1,1}> main_Load_558(i95, i195, i194, env, static) :|: 1 <= i95 && 1 <= i195
main_Load_558(i95, i195, i194, env, static) -{1,1}> main_GE_569(i95, i195, i194, env, static) :|: 1 <= i95 && 1 <= i195

obtained
main_GE_569(i95, i195, i194, env, static) -{3,3}> main_Load_554(i95, i194, i205', env, static) :|: 1 <= i195 && 2 <= i194 && i195 < i194 && 1 <= i95 && 1 <= i205' && 2 <= i205' && i195 + 1 = i205'
by chaining
main_GE_569(i95, i195, i194, env, static) -{0,0}> main_GE_572(i95, i195, i194, env, static) :|: 1 <= i95 && 1 <= i195 && i195 < i194
main_GE_572(i95, i195, i194, env, static) -{1,1}> main_Inc_574(i95, i194, i195, env, static) :|: 1 <= i95 && 2 <= i194 && 1 <= i195 && i195 < i194
main_Inc_574(i95, i194, i195, env, static) -{1,1}> main_JMP_576(i95, i194, i205, env, static) :|: i195 + 1 = i205 && 2 <= i205 && 1 <= i95 && 2 <= i194 && 1 <= i195
main_JMP_576(i95, i194, i205, env, static) -{1,1}> main_Load_584(i95, i194, i205, env, static) :|: 2 <= i205 && 1 <= i95 && 2 <= i194
main_Load_584(i95, i194, i205, env, static) -{0,0}> main_Load_554(i95, i194, i205, env, static) :|: 1 <= i205 && 2 <= i205 && 1 <= i95 && 2 <= i194

obtained
main_GE_569(i95, i195, i194, env, static) -{4,4}> main_LE_589(i95, i204', env, static) :|: 1 <= i95 && i194 + -1 = i204' && i194 <= i195 && 1 <= i195
by chaining
main_GE_569(i95, i195, i194, env, static) -{0,0}> main_GE_571(i95, i195, i194, env, static) :|: 1 <= i95 && i194 <= i195 && 1 <= i195
main_GE_571(i95, i195, i194, env, static) -{1,1}> main_Inc_573(i95, i194, env, static) :|: 1 <= i95 && i194 <= i195 && 1 <= i195
main_Inc_573(i95, i194, env, static) -{1,1}> main_JMP_575(i95, i204, env, static) :|: i194 + -1 = i204 && 1 <= i95
main_JMP_575(i95, i204, env, static) -{1,1}> main_Load_578(i95, i204, env, static) :|: 1 <= i95
main_Load_578(i95, i204, env, static) -{1,1}> main_LE_589(i95, i204, env, static) :|: 1 <= i95

obtained
main_LE_589(i95, i219, env, static) -{1,1}> main_ConstantStackPush_434(i95, i219, env, static) :|: 0 < i219 && 1 <= i219 && 1 <= i95
by chaining
main_LE_589(i95, i219, env, static) -{0,0}> main_LE_591(i95, i219, env, static) :|: 1 <= i219 && 1 <= i95
main_LE_591(i95, i219, env, static) -{1,1}> main_ConstantStackPush_593(i95, i219, env, static) :|: 1 <= i219 && 1 <= i95 && 0 < i219
main_ConstantStackPush_593(i95, i219, env, static) -{0,0}> main_ConstantStackPush_434(i95, i219, env, static) :|: 1 <= i219 && 1 <= i95

(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(i1, env, static) -{16,16}> main_LE_52(i1, env, static'1) :|: 0 >= 0 && static'1 <= static''' + 1 && 0 <= 2 && 0 <= static''' && static''' <= static + 2 && 0 < 1 && 0 <= 1 && 0 <= static && 0 <= static'1 && 0 < 2
main_LE_52(i9, env, static) -{0,0}> main_LE_53(i9, env, static) :|: i9 <= 0
main_LE_52(i10, env, static) -{1,1}> main_ConstantStackPush_434(i10, i10, env, static) :|: 1 <= i10 && 0 < i10
main_ConstantStackPush_434(i95, i151, env, static) -{7,7}> main_Load_554(i95, i151, 1, env, static) :|: 1 <= i151 && 1 <= 3 && 1 <= i95 && 0 < i151 && 1 <= 1 && 1 <= 2
main_Load_554(i95, i194, i195, env, static) -{2,2}> main_GE_569(i95, i195, i194, env, static) :|: 1 <= i95 && 1 <= i195
main_GE_569(i95, i195, i194, env, static) -{3,3}> main_Load_554(i95, i194, i205', env, static) :|: 1 <= i195 && 2 <= i194 && i195 < i194 && 1 <= i95 && 1 <= i205' && 2 <= i205' && i195 + 1 = i205'
main_GE_569(i95, i195, i194, env, static) -{4,4}> main_LE_589(i95, i204', env, static) :|: 1 <= i95 && i194 + -1 = i204' && i194 <= i195 && 1 <= i195
main_LE_589(i95, i218, env, static) -{0,0}> main_LE_590(i95, i218, env, static) :|: 1 <= i95 && i218 <= 0
main_LE_589(i95, i219, env, static) -{1,1}> main_ConstantStackPush_434(i95, i219, env, static) :|: 0 < i219 && 1 <= i219 && 1 <= i95

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

Moved arithmethic from constraints to rhss.

main_GE_569(i95, i195, i194, env, static) -{3,3}> main_Load_554(i95, i194, i205', env, static) :|: 1 <= i195 && 2 <= i194 && i195 < i194 && 1 <= i95 && 1 <= i205' && 2 <= i205' && i195 + 1 = i205'
was transformed to
main_GE_569(i95, i195, i194, env, static) -{3,3}> main_Load_554(i95, i194, i195 + 1, env, static) :|: 1 <= i195 && 2 <= i194 && i195 < i194 && 1 <= i95 && 1 <= i205' && 2 <= i205' && i195 + 1 = i205'

main_GE_569(i95, i195, i194, env, static) -{4,4}> main_LE_589(i95, i204', env, static) :|: 1 <= i95 && i194 + -1 = i204' && i194 <= i195 && 1 <= i195
was transformed to
main_GE_569(i95, i195, i194, env, static) -{4,4}> main_LE_589(i95, i194 + -1, env, static) :|: 1 <= i95 && i194 + -1 = i204' && i194 <= i195 && 1 <= i195

(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:
main_GE_569(i95, i195, i194, env, static) -{3,3}> main_Load_554(i95, i194, i195 + 1, env, static) :|: 1 <= i195 && 2 <= i194 && i195 < i194 && 1 <= i95 && 1 <= i205' && 2 <= i205' && i195 + 1 = i205'
main_GE_569(i95, i195, i194, env, static) -{4,4}> main_LE_589(i95, i194 + -1, env, static) :|: 1 <= i95 && i194 + -1 = i204' && i194 <= i195 && 1 <= i195
main_Load_554(i95, i194, i195, env, static) -{2,2}> main_GE_569(i95, i195, i194, env, static) :|: 1 <= i95 && 1 <= i195
main_LE_52(i9, env, static) -{0,0}> main_LE_53(i9, env, static) :|: i9 <= 0
main_LE_589(i95, i219, env, static) -{1,1}> main_ConstantStackPush_434(i95, i219, env, static) :|: 0 < i219 && 1 <= i219 && 1 <= i95
main_Load_1(i1, env, static) -{16,16}> main_LE_52(i1, env, static'1) :|: 0 >= 0 && static'1 <= static''' + 1 && 0 <= 2 && 0 <= static''' && static''' <= static + 2 && 0 < 1 && 0 <= 1 && 0 <= static && 0 <= static'1 && 0 < 2
main_LE_589(i95, i218, env, static) -{0,0}> main_LE_590(i95, i218, env, static) :|: 1 <= i95 && i218 <= 0
main_ConstantStackPush_434(i95, i151, env, static) -{7,7}> main_Load_554(i95, i151, 1, env, static) :|: 1 <= i151 && 1 <= 3 && 1 <= i95 && 0 < i151 && 1 <= 1 && 1 <= 2
main_LE_52(i10, env, static) -{1,1}> main_ConstantStackPush_434(i10, i10, env, static) :|: 1 <= i10 && 0 < i10

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

Simplified expressions.

main_GE_569(i95, i195, i194, env, static) -{4,4}> main_LE_589(i95, i194 + -1, env, static) :|: 1 <= i95 && i194 + -1 = i204' && i194 <= i195 && 1 <= i195
was transformed to
main_GE_569(i95, i195, i194, env, static) -{4,4}> main_LE_589(i95, i194 - 1, env, static) :|: 1 <= i95 && i194 - 1 = i204' && i194 <= i195 && 1 <= i195

main_Load_1(i1, env, static) -{16,16}> main_LE_52(i1, env, static'1) :|: 0 >= 0 && static'1 <= static''' + 1 && 0 <= 2 && 0 <= static''' && static''' <= static + 2 && 0 < 1 && 0 <= 1 && 0 <= static && 0 <= static'1 && 0 < 2
was transformed to
main_Load_1(i1, env, static) -{16,16}> main_LE_52(i1, env, static'1) :|: static'1 <= static''' + 1 && 0 <= static''' && static''' <= static + 2 && 0 <= static && 0 <= static'1

main_ConstantStackPush_434(i95, i151, env, static) -{7,7}> main_Load_554(i95, i151, 1, env, static) :|: 1 <= i151 && 1 <= 3 && 1 <= i95 && 0 < i151 && 1 <= 1 && 1 <= 2
was transformed to
main_ConstantStackPush_434(i95, i151, env, static) -{7,7}> main_Load_554(i95, i151, 1, env, static) :|: 1 <= i151 && 1 <= i95 && 0 < i151

(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:
main_Load_554(i95, i194, i195, env, static) -{2,2}> main_GE_569(i95, i195, i194, env, static) :|: 1 <= i95 && 1 <= i195
main_LE_52(i9, env, static) -{0,0}> main_LE_53(i9, env, static) :|: i9 <= 0
main_LE_589(i95, i219, env, static) -{1,1}> main_ConstantStackPush_434(i95, i219, env, static) :|: 0 < i219 && 1 <= i219 && 1 <= i95
main_ConstantStackPush_434(i95, i151, env, static) -{7,7}> main_Load_554(i95, i151, 1, env, static) :|: 1 <= i151 && 1 <= i95 && 0 < i151
main_Load_1(i1, env, static) -{16,16}> main_LE_52(i1, env, static'1) :|: static'1 <= static''' + 1 && 0 <= static''' && static''' <= static + 2 && 0 <= static && 0 <= static'1
main_LE_589(i95, i218, env, static) -{0,0}> main_LE_590(i95, i218, env, static) :|: 1 <= i95 && i218 <= 0
main_GE_569(i95, i195, i194, env, static) -{4,4}> main_LE_589(i95, i194 - 1, env, static) :|: 1 <= i95 && i194 - 1 = i204' && i194 <= i195 && 1 <= i195
main_GE_569(i95, i195, i194, env, static) -{3,3}> main_Load_554(i95, i194, i195 + 1, env, static) :|: 1 <= i195 && 2 <= i194 && i195 < i194 && 1 <= i95 && 1 <= i205' && 2 <= i205' && i195 + 1 = i205'
main_LE_52(i10, env, static) -{1,1}> main_ConstantStackPush_434(i10, i10, env, static) :|: 1 <= i10 && 0 < i10

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

Transformed 54 jbc graph edges to a weighted ITS with 54 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:

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

(16) Obligation:

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

Moved arithmethic from constraints to rhss.

(18) Obligation:

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

Simplified expressions.

(20) Obligation:

(21) koat Proof (EQUIVALENT transformation)

YES(?, 30*ar_0^2 + 143*ar_0 + 81)

Initial complexity problem:
1: T:
(Comp: ?, Cost: 2) main_Load_554(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_GE_569(ar_0, ar_2, ar_1, ar_3, ar_4)) [ 1 <= ar_0 /\ 1 <= ar_2 ]
(Comp: ?, Cost: 0) main_LE_52(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_LE_53(ar_0, ar_1, ar_2, arityPad, arityPad)) [ ar_0 <= 0 ]
(Comp: ?, Cost: 1) main_LE_589(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_ConstantStackPush_434(ar_0, ar_1, ar_2, ar_3, arityPad)) [ 0 < ar_1 /\ 1 <= ar_1 /\ 1 <= ar_0 ]
(Comp: ?, Cost: 7) main_ConstantStackPush_434(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_Load_554(ar_0, ar_1, 1, ar_2, ar_3)) [ 1 <= ar_1 /\ 1 <= ar_0 /\ 0 < ar_1 ]
(Comp: ?, Cost: 16) main_Load_1(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_LE_52(ar_0, ar_1, static'1, arityPad, arityPad)) [ static'1 <= static''' + 1 /\ 0 <= static''' /\ static''' <= ar_2 + 2 /\ 0 <= ar_2 /\ 0 <= static'1 ]
(Comp: ?, Cost: 0) main_LE_589(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_LE_590(ar_0, ar_1, ar_2, ar_3, arityPad)) [ 1 <= ar_0 /\ ar_1 <= 0 ]
(Comp: ?, Cost: 4) main_GE_569(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_LE_589(ar_0, ar_2 - 1, ar_3, ar_4, arityPad)) [ 1 <= ar_0 /\ ar_2 - 1 = i204' /\ ar_2 <= ar_1 /\ 1 <= ar_1 ]
(Comp: ?, Cost: 3) main_GE_569(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_Load_554(ar_0, ar_2, ar_1 + 1, ar_3, ar_4)) [ 1 <= ar_1 /\ 2 <= ar_2 /\ ar_1 < ar_2 /\ 1 <= ar_0 /\ 1 <= i205' /\ 2 <= i205' /\ ar_1 + 1 = i205' ]
(Comp: ?, Cost: 1) main_LE_52(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_ConstantStackPush_434(ar_0, ar_0, ar_1, ar_2, arityPad)) [ 1 <= ar_0 /\ 0 < ar_0 ]
(Comp: 1, Cost: 0) koat_start(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_Load_1(ar_0, ar_1, ar_2, ar_3, ar_4)) [ 0 <= 0 ]
start location: koat_start
leaf cost: 0

Repeatedly propagating knowledge in problem 1 produces the following problem:
2: T:
(Comp: ?, Cost: 2) main_Load_554(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_GE_569(ar_0, ar_2, ar_1, ar_3, ar_4)) [ 1 <= ar_0 /\ 1 <= ar_2 ]
(Comp: 1, Cost: 0) main_LE_52(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_LE_53(ar_0, ar_1, ar_2, arityPad, arityPad)) [ ar_0 <= 0 ]
(Comp: ?, Cost: 1) main_LE_589(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_ConstantStackPush_434(ar_0, ar_1, ar_2, ar_3, arityPad)) [ 0 < ar_1 /\ 1 <= ar_1 /\ 1 <= ar_0 ]
(Comp: ?, Cost: 7) main_ConstantStackPush_434(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_Load_554(ar_0, ar_1, 1, ar_2, ar_3)) [ 1 <= ar_1 /\ 1 <= ar_0 /\ 0 < ar_1 ]
(Comp: 1, Cost: 16) main_Load_1(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_LE_52(ar_0, ar_1, static'1, arityPad, arityPad)) [ static'1 <= static''' + 1 /\ 0 <= static''' /\ static''' <= ar_2 + 2 /\ 0 <= ar_2 /\ 0 <= static'1 ]
(Comp: ?, Cost: 0) main_LE_589(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_LE_590(ar_0, ar_1, ar_2, ar_3, arityPad)) [ 1 <= ar_0 /\ ar_1 <= 0 ]
(Comp: ?, Cost: 4) main_GE_569(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_LE_589(ar_0, ar_2 - 1, ar_3, ar_4, arityPad)) [ 1 <= ar_0 /\ ar_2 - 1 = i204' /\ ar_2 <= ar_1 /\ 1 <= ar_1 ]
(Comp: ?, Cost: 3) main_GE_569(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_Load_554(ar_0, ar_2, ar_1 + 1, ar_3, ar_4)) [ 1 <= ar_1 /\ 2 <= ar_2 /\ ar_1 < ar_2 /\ 1 <= ar_0 /\ 1 <= i205' /\ 2 <= i205' /\ ar_1 + 1 = i205' ]
(Comp: 1, Cost: 1) main_LE_52(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_ConstantStackPush_434(ar_0, ar_0, ar_1, ar_2, arityPad)) [ 1 <= ar_0 /\ 0 < ar_0 ]
(Comp: 1, Cost: 0) koat_start(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_Load_1(ar_0, ar_1, ar_2, ar_3, ar_4)) [ 0 <= 0 ]
start location: koat_start
leaf cost: 0

A polynomial rank function with
Pol(main_Load_554) = 1
Pol(main_GE_569) = 1
Pol(main_LE_52) = 1
Pol(main_LE_53) = 0
Pol(main_LE_589) = 1
Pol(main_ConstantStackPush_434) = 1
Pol(main_Load_1) = 1
Pol(main_LE_590) = 0
Pol(koat_start) = 1
orients all transitions weakly and the transition
main_LE_589(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_LE_590(ar_0, ar_1, ar_2, ar_3, arityPad)) [ 1 <= ar_0 /\ ar_1 <= 0 ]
strictly and produces the following problem:
3: T:
(Comp: ?, Cost: 2) main_Load_554(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_GE_569(ar_0, ar_2, ar_1, ar_3, ar_4)) [ 1 <= ar_0 /\ 1 <= ar_2 ]
(Comp: 1, Cost: 0) main_LE_52(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_LE_53(ar_0, ar_1, ar_2, arityPad, arityPad)) [ ar_0 <= 0 ]
(Comp: ?, Cost: 1) main_LE_589(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_ConstantStackPush_434(ar_0, ar_1, ar_2, ar_3, arityPad)) [ 0 < ar_1 /\ 1 <= ar_1 /\ 1 <= ar_0 ]
(Comp: ?, Cost: 7) main_ConstantStackPush_434(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_Load_554(ar_0, ar_1, 1, ar_2, ar_3)) [ 1 <= ar_1 /\ 1 <= ar_0 /\ 0 < ar_1 ]
(Comp: 1, Cost: 16) main_Load_1(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_LE_52(ar_0, ar_1, static'1, arityPad, arityPad)) [ static'1 <= static''' + 1 /\ 0 <= static''' /\ static''' <= ar_2 + 2 /\ 0 <= ar_2 /\ 0 <= static'1 ]
(Comp: 1, Cost: 0) main_LE_589(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_LE_590(ar_0, ar_1, ar_2, ar_3, arityPad)) [ 1 <= ar_0 /\ ar_1 <= 0 ]
(Comp: ?, Cost: 4) main_GE_569(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_LE_589(ar_0, ar_2 - 1, ar_3, ar_4, arityPad)) [ 1 <= ar_0 /\ ar_2 - 1 = i204' /\ ar_2 <= ar_1 /\ 1 <= ar_1 ]
(Comp: ?, Cost: 3) main_GE_569(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_Load_554(ar_0, ar_2, ar_1 + 1, ar_3, ar_4)) [ 1 <= ar_1 /\ 2 <= ar_2 /\ ar_1 < ar_2 /\ 1 <= ar_0 /\ 1 <= i205' /\ 2 <= i205' /\ ar_1 + 1 = i205' ]
(Comp: 1, Cost: 1) main_LE_52(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_ConstantStackPush_434(ar_0, ar_0, ar_1, ar_2, arityPad)) [ 1 <= ar_0 /\ 0 < ar_0 ]
(Comp: 1, Cost: 0) koat_start(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_Load_1(ar_0, ar_1, ar_2, ar_3, ar_4)) [ 0 <= 0 ]
start location: koat_start
leaf cost: 0

A polynomial rank function with
Pol(main_Load_554) = 2*V_2 - 2
Pol(main_GE_569) = 2*V_3 - 2
Pol(main_LE_52) = 2*V_1 - 1
Pol(main_LE_53) = 2*V_1 - 1
Pol(main_LE_589) = 2*V_2
Pol(main_ConstantStackPush_434) = 2*V_2 - 1
Pol(main_Load_1) = 2*V_1 - 1
Pol(main_LE_590) = 2*V_2
Pol(koat_start) = 2*V_1 - 1
orients all transitions weakly and the transitions
main_LE_589(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_ConstantStackPush_434(ar_0, ar_1, ar_2, ar_3, arityPad)) [ 0 < ar_1 /\ 1 <= ar_1 /\ 1 <= ar_0 ]
main_ConstantStackPush_434(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_Load_554(ar_0, ar_1, 1, ar_2, ar_3)) [ 1 <= ar_1 /\ 1 <= ar_0 /\ 0 < ar_1 ]
strictly and produces the following problem:
4: T:
(Comp: ?, Cost: 2) main_Load_554(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_GE_569(ar_0, ar_2, ar_1, ar_3, ar_4)) [ 1 <= ar_0 /\ 1 <= ar_2 ]
(Comp: 1, Cost: 0) main_LE_52(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_LE_53(ar_0, ar_1, ar_2, arityPad, arityPad)) [ ar_0 <= 0 ]
(Comp: 2*ar_0 + 1, Cost: 1) main_LE_589(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_ConstantStackPush_434(ar_0, ar_1, ar_2, ar_3, arityPad)) [ 0 < ar_1 /\ 1 <= ar_1 /\ 1 <= ar_0 ]
(Comp: 2*ar_0 + 1, Cost: 7) main_ConstantStackPush_434(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_Load_554(ar_0, ar_1, 1, ar_2, ar_3)) [ 1 <= ar_1 /\ 1 <= ar_0 /\ 0 < ar_1 ]
(Comp: 1, Cost: 16) main_Load_1(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_LE_52(ar_0, ar_1, static'1, arityPad, arityPad)) [ static'1 <= static''' + 1 /\ 0 <= static''' /\ static''' <= ar_2 + 2 /\ 0 <= ar_2 /\ 0 <= static'1 ]
(Comp: 1, Cost: 0) main_LE_589(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_LE_590(ar_0, ar_1, ar_2, ar_3, arityPad)) [ 1 <= ar_0 /\ ar_1 <= 0 ]
(Comp: ?, Cost: 4) main_GE_569(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_LE_589(ar_0, ar_2 - 1, ar_3, ar_4, arityPad)) [ 1 <= ar_0 /\ ar_2 - 1 = i204' /\ ar_2 <= ar_1 /\ 1 <= ar_1 ]
(Comp: ?, Cost: 3) main_GE_569(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_Load_554(ar_0, ar_2, ar_1 + 1, ar_3, ar_4)) [ 1 <= ar_1 /\ 2 <= ar_2 /\ ar_1 < ar_2 /\ 1 <= ar_0 /\ 1 <= i205' /\ 2 <= i205' /\ ar_1 + 1 = i205' ]
(Comp: 1, Cost: 1) main_LE_52(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_ConstantStackPush_434(ar_0, ar_0, ar_1, ar_2, arityPad)) [ 1 <= ar_0 /\ 0 < ar_0 ]
(Comp: 1, Cost: 0) koat_start(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_Load_1(ar_0, ar_1, ar_2, ar_3, ar_4)) [ 0 <= 0 ]
start location: koat_start
leaf cost: 0

A polynomial rank function with
Pol(main_Load_554) = 1
Pol(main_GE_569) = 1
Pol(main_LE_589) = 0
and size complexities
S("koat_start(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_Load_1(ar_0, ar_1, ar_2, ar_3, ar_4)) [ 0 <= 0 ]", 0-0) = ar_0
S("koat_start(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_Load_1(ar_0, ar_1, ar_2, ar_3, ar_4)) [ 0 <= 0 ]", 0-1) = ar_1
S("koat_start(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_Load_1(ar_0, ar_1, ar_2, ar_3, ar_4)) [ 0 <= 0 ]", 0-2) = ar_2
S("koat_start(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_Load_1(ar_0, ar_1, ar_2, ar_3, ar_4)) [ 0 <= 0 ]", 0-3) = ar_3
S("koat_start(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_Load_1(ar_0, ar_1, ar_2, ar_3, ar_4)) [ 0 <= 0 ]", 0-4) = ar_4
S("main_LE_52(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_ConstantStackPush_434(ar_0, ar_0, ar_1, ar_2, arityPad)) [ 1 <= ar_0 /\\ 0 < ar_0 ]", 0-0) = ar_0
S("main_LE_52(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_ConstantStackPush_434(ar_0, ar_0, ar_1, ar_2, arityPad)) [ 1 <= ar_0 /\\ 0 < ar_0 ]", 0-1) = ar_0
S("main_LE_52(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_ConstantStackPush_434(ar_0, ar_0, ar_1, ar_2, arityPad)) [ 1 <= ar_0 /\\ 0 < ar_0 ]", 0-2) = ar_1
S("main_LE_52(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_ConstantStackPush_434(ar_0, ar_0, ar_1, ar_2, arityPad)) [ 1 <= ar_0 /\\ 0 < ar_0 ]", 0-3) = ar_2 + 3
S("main_LE_52(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_ConstantStackPush_434(ar_0, ar_0, ar_1, ar_2, arityPad)) [ 1 <= ar_0 /\\ 0 < ar_0 ]", 0-4) = ?
S("main_GE_569(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_Load_554(ar_0, ar_2, ar_1 + 1, ar_3, ar_4)) [ 1 <= ar_1 /\\ 2 <= ar_2 /\\ ar_1 < ar_2 /\\ 1 <= ar_0 /\\ 1 <= i205' /\\ 2 <= i205' /\\ ar_1 + 1 = i205' ]", 0-0) = ar_0
S("main_GE_569(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_Load_554(ar_0, ar_2, ar_1 + 1, ar_3, ar_4)) [ 1 <= ar_1 /\\ 2 <= ar_2 /\\ ar_1 < ar_2 /\\ 1 <= ar_0 /\\ 1 <= i205' /\\ 2 <= i205' /\\ ar_1 + 1 = i205' ]", 0-1) = ?
S("main_GE_569(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_Load_554(ar_0, ar_2, ar_1 + 1, ar_3, ar_4)) [ 1 <= ar_1 /\\ 2 <= ar_2 /\\ ar_1 < ar_2 /\\ 1 <= ar_0 /\\ 1 <= i205' /\\ 2 <= i205' /\\ ar_1 + 1 = i205' ]", 0-2) = ?
S("main_GE_569(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_Load_554(ar_0, ar_2, ar_1 + 1, ar_3, ar_4)) [ 1 <= ar_1 /\\ 2 <= ar_2 /\\ ar_1 < ar_2 /\\ 1 <= ar_0 /\\ 1 <= i205' /\\ 2 <= i205' /\\ ar_1 + 1 = i205' ]", 0-3) = ar_1
S("main_GE_569(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_Load_554(ar_0, ar_2, ar_1 + 1, ar_3, ar_4)) [ 1 <= ar_1 /\\ 2 <= ar_2 /\\ ar_1 < ar_2 /\\ 1 <= ar_0 /\\ 1 <= i205' /\\ 2 <= i205' /\\ ar_1 + 1 = i205' ]", 0-4) = ar_2 + 3
S("main_GE_569(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_LE_589(ar_0, ar_2 - 1, ar_3, ar_4, arityPad)) [ 1 <= ar_0 /\\ ar_2 - 1 = i204' /\\ ar_2 <= ar_1 /\\ 1 <= ar_1 ]", 0-0) = ar_0
S("main_GE_569(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_LE_589(ar_0, ar_2 - 1, ar_3, ar_4, arityPad)) [ 1 <= ar_0 /\\ ar_2 - 1 = i204' /\\ ar_2 <= ar_1 /\\ 1 <= ar_1 ]", 0-1) = ?
S("main_GE_569(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_LE_589(ar_0, ar_2 - 1, ar_3, ar_4, arityPad)) [ 1 <= ar_0 /\\ ar_2 - 1 = i204' /\\ ar_2 <= ar_1 /\\ 1 <= ar_1 ]", 0-2) = ar_1
S("main_GE_569(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_LE_589(ar_0, ar_2 - 1, ar_3, ar_4, arityPad)) [ 1 <= ar_0 /\\ ar_2 - 1 = i204' /\\ ar_2 <= ar_1 /\\ 1 <= ar_1 ]", 0-3) = ar_2 + 3
S("main_GE_569(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_LE_589(ar_0, ar_2 - 1, ar_3, ar_4, arityPad)) [ 1 <= ar_0 /\\ ar_2 - 1 = i204' /\\ ar_2 <= ar_1 /\\ 1 <= ar_1 ]", 0-4) = ?
S("main_LE_589(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_LE_590(ar_0, ar_1, ar_2, ar_3, arityPad)) [ 1 <= ar_0 /\\ ar_1 <= 0 ]", 0-0) = ar_0
S("main_LE_589(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_LE_590(ar_0, ar_1, ar_2, ar_3, arityPad)) [ 1 <= ar_0 /\\ ar_1 <= 0 ]", 0-1) = ?
S("main_LE_589(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_LE_590(ar_0, ar_1, ar_2, ar_3, arityPad)) [ 1 <= ar_0 /\\ ar_1 <= 0 ]", 0-2) = ar_1
S("main_LE_589(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_LE_590(ar_0, ar_1, ar_2, ar_3, arityPad)) [ 1 <= ar_0 /\\ ar_1 <= 0 ]", 0-3) = ar_2 + 3
S("main_LE_589(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_LE_590(ar_0, ar_1, ar_2, ar_3, arityPad)) [ 1 <= ar_0 /\\ ar_1 <= 0 ]", 0-4) = ?
S("main_Load_1(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_LE_52(ar_0, ar_1, static'1, arityPad, arityPad)) [ static'1 <= static''' + 1 /\\ 0 <= static''' /\\ static''' <= ar_2 + 2 /\\ 0 <= ar_2 /\\ 0 <= static'1 ]", 0-0) = ar_0
S("main_Load_1(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_LE_52(ar_0, ar_1, static'1, arityPad, arityPad)) [ static'1 <= static''' + 1 /\\ 0 <= static''' /\\ static''' <= ar_2 + 2 /\\ 0 <= ar_2 /\\ 0 <= static'1 ]", 0-1) = ar_1
S("main_Load_1(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_LE_52(ar_0, ar_1, static'1, arityPad, arityPad)) [ static'1 <= static''' + 1 /\\ 0 <= static''' /\\ static''' <= ar_2 + 2 /\\ 0 <= ar_2 /\\ 0 <= static'1 ]", 0-2) = ar_2 + 3
S("main_Load_1(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_LE_52(ar_0, ar_1, static'1, arityPad, arityPad)) [ static'1 <= static''' + 1 /\\ 0 <= static''' /\\ static''' <= ar_2 + 2 /\\ 0 <= ar_2 /\\ 0 <= static'1 ]", 0-3) = ?
S("main_Load_1(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_LE_52(ar_0, ar_1, static'1, arityPad, arityPad)) [ static'1 <= static''' + 1 /\\ 0 <= static''' /\\ static''' <= ar_2 + 2 /\\ 0 <= ar_2 /\\ 0 <= static'1 ]", 0-4) = ?
S("main_ConstantStackPush_434(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_Load_554(ar_0, ar_1, 1, ar_2, ar_3)) [ 1 <= ar_1 /\\ 1 <= ar_0 /\\ 0 < ar_1 ]", 0-0) = ar_0
S("main_ConstantStackPush_434(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_Load_554(ar_0, ar_1, 1, ar_2, ar_3)) [ 1 <= ar_1 /\\ 1 <= ar_0 /\\ 0 < ar_1 ]", 0-1) = ?
S("main_ConstantStackPush_434(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_Load_554(ar_0, ar_1, 1, ar_2, ar_3)) [ 1 <= ar_1 /\\ 1 <= ar_0 /\\ 0 < ar_1 ]", 0-2) = 1
S("main_ConstantStackPush_434(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_Load_554(ar_0, ar_1, 1, ar_2, ar_3)) [ 1 <= ar_1 /\\ 1 <= ar_0 /\\ 0 < ar_1 ]", 0-3) = ar_1
S("main_ConstantStackPush_434(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_Load_554(ar_0, ar_1, 1, ar_2, ar_3)) [ 1 <= ar_1 /\\ 1 <= ar_0 /\\ 0 < ar_1 ]", 0-4) = ar_2 + 3
S("main_LE_589(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_ConstantStackPush_434(ar_0, ar_1, ar_2, ar_3, arityPad)) [ 0 < ar_1 /\\ 1 <= ar_1 /\\ 1 <= ar_0 ]", 0-0) = ar_0
S("main_LE_589(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_ConstantStackPush_434(ar_0, ar_1, ar_2, ar_3, arityPad)) [ 0 < ar_1 /\\ 1 <= ar_1 /\\ 1 <= ar_0 ]", 0-1) = ?
S("main_LE_589(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_ConstantStackPush_434(ar_0, ar_1, ar_2, ar_3, arityPad)) [ 0 < ar_1 /\\ 1 <= ar_1 /\\ 1 <= ar_0 ]", 0-2) = ar_1
S("main_LE_589(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_ConstantStackPush_434(ar_0, ar_1, ar_2, ar_3, arityPad)) [ 0 < ar_1 /\\ 1 <= ar_1 /\\ 1 <= ar_0 ]", 0-3) = ar_2 + 3
S("main_LE_589(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_ConstantStackPush_434(ar_0, ar_1, ar_2, ar_3, arityPad)) [ 0 < ar_1 /\\ 1 <= ar_1 /\\ 1 <= ar_0 ]", 0-4) = ?
S("main_LE_52(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_LE_53(ar_0, ar_1, ar_2, arityPad, arityPad)) [ ar_0 <= 0 ]", 0-0) = ar_0
S("main_LE_52(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_LE_53(ar_0, ar_1, ar_2, arityPad, arityPad)) [ ar_0 <= 0 ]", 0-1) = ar_1
S("main_LE_52(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_LE_53(ar_0, ar_1, ar_2, arityPad, arityPad)) [ ar_0 <= 0 ]", 0-2) = ar_2 + 3
S("main_LE_52(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_LE_53(ar_0, ar_1, ar_2, arityPad, arityPad)) [ ar_0 <= 0 ]", 0-3) = ?
S("main_LE_52(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_LE_53(ar_0, ar_1, ar_2, arityPad, arityPad)) [ ar_0 <= 0 ]", 0-4) = ?
S("main_Load_554(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_GE_569(ar_0, ar_2, ar_1, ar_3, ar_4)) [ 1 <= ar_0 /\\ 1 <= ar_2 ]", 0-0) = ar_0
S("main_Load_554(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_GE_569(ar_0, ar_2, ar_1, ar_3, ar_4)) [ 1 <= ar_0 /\\ 1 <= ar_2 ]", 0-1) = ?
S("main_Load_554(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_GE_569(ar_0, ar_2, ar_1, ar_3, ar_4)) [ 1 <= ar_0 /\\ 1 <= ar_2 ]", 0-2) = ?
S("main_Load_554(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_GE_569(ar_0, ar_2, ar_1, ar_3, ar_4)) [ 1 <= ar_0 /\\ 1 <= ar_2 ]", 0-3) = ar_1
S("main_Load_554(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_GE_569(ar_0, ar_2, ar_1, ar_3, ar_4)) [ 1 <= ar_0 /\\ 1 <= ar_2 ]", 0-4) = ar_2 + 3
orients the transitions
main_Load_554(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_GE_569(ar_0, ar_2, ar_1, ar_3, ar_4)) [ 1 <= ar_0 /\ 1 <= ar_2 ]
main_GE_569(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_Load_554(ar_0, ar_2, ar_1 + 1, ar_3, ar_4)) [ 1 <= ar_1 /\ 2 <= ar_2 /\ ar_1 < ar_2 /\ 1 <= ar_0 /\ 1 <= i205' /\ 2 <= i205' /\ ar_1 + 1 = i205' ]
main_GE_569(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_LE_589(ar_0, ar_2 - 1, ar_3, ar_4, arityPad)) [ 1 <= ar_0 /\ ar_2 - 1 = i204' /\ ar_2 <= ar_1 /\ 1 <= ar_1 ]
weakly and the transition
main_GE_569(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_LE_589(ar_0, ar_2 - 1, ar_3, ar_4, arityPad)) [ 1 <= ar_0 /\ ar_2 - 1 = i204' /\ ar_2 <= ar_1 /\ 1 <= ar_1 ]
strictly and produces the following problem:
5: T:
(Comp: ?, Cost: 2) main_Load_554(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_GE_569(ar_0, ar_2, ar_1, ar_3, ar_4)) [ 1 <= ar_0 /\ 1 <= ar_2 ]
(Comp: 1, Cost: 0) main_LE_52(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_LE_53(ar_0, ar_1, ar_2, arityPad, arityPad)) [ ar_0 <= 0 ]
(Comp: 2*ar_0 + 1, Cost: 1) main_LE_589(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_ConstantStackPush_434(ar_0, ar_1, ar_2, ar_3, arityPad)) [ 0 < ar_1 /\ 1 <= ar_1 /\ 1 <= ar_0 ]
(Comp: 2*ar_0 + 1, Cost: 7) main_ConstantStackPush_434(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_Load_554(ar_0, ar_1, 1, ar_2, ar_3)) [ 1 <= ar_1 /\ 1 <= ar_0 /\ 0 < ar_1 ]
(Comp: 1, Cost: 16) main_Load_1(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_LE_52(ar_0, ar_1, static'1, arityPad, arityPad)) [ static'1 <= static''' + 1 /\ 0 <= static''' /\ static''' <= ar_2 + 2 /\ 0 <= ar_2 /\ 0 <= static'1 ]
(Comp: 1, Cost: 0) main_LE_589(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_LE_590(ar_0, ar_1, ar_2, ar_3, arityPad)) [ 1 <= ar_0 /\ ar_1 <= 0 ]
(Comp: 2*ar_0 + 1, Cost: 4) main_GE_569(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_LE_589(ar_0, ar_2 - 1, ar_3, ar_4, arityPad)) [ 1 <= ar_0 /\ ar_2 - 1 = i204' /\ ar_2 <= ar_1 /\ 1 <= ar_1 ]
(Comp: ?, Cost: 3) main_GE_569(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_Load_554(ar_0, ar_2, ar_1 + 1, ar_3, ar_4)) [ 1 <= ar_1 /\ 2 <= ar_2 /\ ar_1 < ar_2 /\ 1 <= ar_0 /\ 1 <= i205' /\ 2 <= i205' /\ ar_1 + 1 = i205' ]
(Comp: 1, Cost: 1) main_LE_52(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_ConstantStackPush_434(ar_0, ar_0, ar_1, ar_2, arityPad)) [ 1 <= ar_0 /\ 0 < ar_0 ]
(Comp: 1, Cost: 0) koat_start(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_Load_1(ar_0, ar_1, ar_2, ar_3, ar_4)) [ 0 <= 0 ]
start location: koat_start
leaf cost: 0

A polynomial rank function with
Pol(main_Load_554) = V_2 - V_3
Pol(main_GE_569) = -V_2 + V_3
and size complexities
S("koat_start(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_Load_1(ar_0, ar_1, ar_2, ar_3, ar_4)) [ 0 <= 0 ]", 0-0) = ar_0
S("koat_start(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_Load_1(ar_0, ar_1, ar_2, ar_3, ar_4)) [ 0 <= 0 ]", 0-1) = ar_1
S("koat_start(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_Load_1(ar_0, ar_1, ar_2, ar_3, ar_4)) [ 0 <= 0 ]", 0-2) = ar_2
S("koat_start(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_Load_1(ar_0, ar_1, ar_2, ar_3, ar_4)) [ 0 <= 0 ]", 0-3) = ar_3
S("koat_start(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_Load_1(ar_0, ar_1, ar_2, ar_3, ar_4)) [ 0 <= 0 ]", 0-4) = ar_4
S("main_LE_52(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_ConstantStackPush_434(ar_0, ar_0, ar_1, ar_2, arityPad)) [ 1 <= ar_0 /\\ 0 < ar_0 ]", 0-0) = ar_0
S("main_LE_52(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_ConstantStackPush_434(ar_0, ar_0, ar_1, ar_2, arityPad)) [ 1 <= ar_0 /\\ 0 < ar_0 ]", 0-1) = ar_0
S("main_LE_52(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_ConstantStackPush_434(ar_0, ar_0, ar_1, ar_2, arityPad)) [ 1 <= ar_0 /\\ 0 < ar_0 ]", 0-2) = ar_1
S("main_LE_52(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_ConstantStackPush_434(ar_0, ar_0, ar_1, ar_2, arityPad)) [ 1 <= ar_0 /\\ 0 < ar_0 ]", 0-3) = ar_2 + 3
S("main_LE_52(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_ConstantStackPush_434(ar_0, ar_0, ar_1, ar_2, arityPad)) [ 1 <= ar_0 /\\ 0 < ar_0 ]", 0-4) = ?
S("main_GE_569(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_Load_554(ar_0, ar_2, ar_1 + 1, ar_3, ar_4)) [ 1 <= ar_1 /\\ 2 <= ar_2 /\\ ar_1 < ar_2 /\\ 1 <= ar_0 /\\ 1 <= i205' /\\ 2 <= i205' /\\ ar_1 + 1 = i205' ]", 0-0) = ar_0
S("main_GE_569(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_Load_554(ar_0, ar_2, ar_1 + 1, ar_3, ar_4)) [ 1 <= ar_1 /\\ 2 <= ar_2 /\\ ar_1 < ar_2 /\\ 1 <= ar_0 /\\ 1 <= i205' /\\ 2 <= i205' /\\ ar_1 + 1 = i205' ]", 0-1) = 3*ar_0 + 9
S("main_GE_569(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_Load_554(ar_0, ar_2, ar_1 + 1, ar_3, ar_4)) [ 1 <= ar_1 /\\ 2 <= ar_2 /\\ ar_1 < ar_2 /\\ 1 <= ar_0 /\\ 1 <= i205' /\\ 2 <= i205' /\\ ar_1 + 1 = i205' ]", 0-2) = 3*ar_0 + 27
S("main_GE_569(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_Load_554(ar_0, ar_2, ar_1 + 1, ar_3, ar_4)) [ 1 <= ar_1 /\\ 2 <= ar_2 /\\ ar_1 < ar_2 /\\ 1 <= ar_0 /\\ 1 <= i205' /\\ 2 <= i205' /\\ ar_1 + 1 = i205' ]", 0-3) = ar_1
S("main_GE_569(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_Load_554(ar_0, ar_2, ar_1 + 1, ar_3, ar_4)) [ 1 <= ar_1 /\\ 2 <= ar_2 /\\ ar_1 < ar_2 /\\ 1 <= ar_0 /\\ 1 <= i205' /\\ 2 <= i205' /\\ ar_1 + 1 = i205' ]", 0-4) = ar_2 + 3
S("main_GE_569(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_LE_589(ar_0, ar_2 - 1, ar_3, ar_4, arityPad)) [ 1 <= ar_0 /\\ ar_2 - 1 = i204' /\\ ar_2 <= ar_1 /\\ 1 <= ar_1 ]", 0-0) = ar_0
S("main_GE_569(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_LE_589(ar_0, ar_2 - 1, ar_3, ar_4, arityPad)) [ 1 <= ar_0 /\\ ar_2 - 1 = i204' /\\ ar_2 <= ar_1 /\\ 1 <= ar_1 ]", 0-1) = 3*ar_0 + 9
S("main_GE_569(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_LE_589(ar_0, ar_2 - 1, ar_3, ar_4, arityPad)) [ 1 <= ar_0 /\\ ar_2 - 1 = i204' /\\ ar_2 <= ar_1 /\\ 1 <= ar_1 ]", 0-2) = ar_1
S("main_GE_569(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_LE_589(ar_0, ar_2 - 1, ar_3, ar_4, arityPad)) [ 1 <= ar_0 /\\ ar_2 - 1 = i204' /\\ ar_2 <= ar_1 /\\ 1 <= ar_1 ]", 0-3) = ar_2 + 3
S("main_GE_569(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_LE_589(ar_0, ar_2 - 1, ar_3, ar_4, arityPad)) [ 1 <= ar_0 /\\ ar_2 - 1 = i204' /\\ ar_2 <= ar_1 /\\ 1 <= ar_1 ]", 0-4) = ?
S("main_LE_589(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_LE_590(ar_0, ar_1, ar_2, ar_3, arityPad)) [ 1 <= ar_0 /\\ ar_1 <= 0 ]", 0-0) = ar_0
S("main_LE_589(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_LE_590(ar_0, ar_1, ar_2, ar_3, arityPad)) [ 1 <= ar_0 /\\ ar_1 <= 0 ]", 0-1) = 3*ar_0 + 27
S("main_LE_589(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_LE_590(ar_0, ar_1, ar_2, ar_3, arityPad)) [ 1 <= ar_0 /\\ ar_1 <= 0 ]", 0-2) = ar_1
S("main_LE_589(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_LE_590(ar_0, ar_1, ar_2, ar_3, arityPad)) [ 1 <= ar_0 /\\ ar_1 <= 0 ]", 0-3) = ar_2 + 3
S("main_LE_589(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_LE_590(ar_0, ar_1, ar_2, ar_3, arityPad)) [ 1 <= ar_0 /\\ ar_1 <= 0 ]", 0-4) = ?
S("main_Load_1(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_LE_52(ar_0, ar_1, static'1, arityPad, arityPad)) [ static'1 <= static''' + 1 /\\ 0 <= static''' /\\ static''' <= ar_2 + 2 /\\ 0 <= ar_2 /\\ 0 <= static'1 ]", 0-0) = ar_0
S("main_Load_1(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_LE_52(ar_0, ar_1, static'1, arityPad, arityPad)) [ static'1 <= static''' + 1 /\\ 0 <= static''' /\\ static''' <= ar_2 + 2 /\\ 0 <= ar_2 /\\ 0 <= static'1 ]", 0-1) = ar_1
S("main_Load_1(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_LE_52(ar_0, ar_1, static'1, arityPad, arityPad)) [ static'1 <= static''' + 1 /\\ 0 <= static''' /\\ static''' <= ar_2 + 2 /\\ 0 <= ar_2 /\\ 0 <= static'1 ]", 0-2) = ar_2 + 3
S("main_Load_1(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_LE_52(ar_0, ar_1, static'1, arityPad, arityPad)) [ static'1 <= static''' + 1 /\\ 0 <= static''' /\\ static''' <= ar_2 + 2 /\\ 0 <= ar_2 /\\ 0 <= static'1 ]", 0-3) = ?
S("main_Load_1(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_LE_52(ar_0, ar_1, static'1, arityPad, arityPad)) [ static'1 <= static''' + 1 /\\ 0 <= static''' /\\ static''' <= ar_2 + 2 /\\ 0 <= ar_2 /\\ 0 <= static'1 ]", 0-4) = ?
S("main_ConstantStackPush_434(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_Load_554(ar_0, ar_1, 1, ar_2, ar_3)) [ 1 <= ar_1 /\\ 1 <= ar_0 /\\ 0 < ar_1 ]", 0-0) = ar_0
S("main_ConstantStackPush_434(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_Load_554(ar_0, ar_1, 1, ar_2, ar_3)) [ 1 <= ar_1 /\\ 1 <= ar_0 /\\ 0 < ar_1 ]", 0-1) = 3*ar_0 + 9
S("main_ConstantStackPush_434(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_Load_554(ar_0, ar_1, 1, ar_2, ar_3)) [ 1 <= ar_1 /\\ 1 <= ar_0 /\\ 0 < ar_1 ]", 0-2) = 1
S("main_ConstantStackPush_434(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_Load_554(ar_0, ar_1, 1, ar_2, ar_3)) [ 1 <= ar_1 /\\ 1 <= ar_0 /\\ 0 < ar_1 ]", 0-3) = ar_1
S("main_ConstantStackPush_434(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_Load_554(ar_0, ar_1, 1, ar_2, ar_3)) [ 1 <= ar_1 /\\ 1 <= ar_0 /\\ 0 < ar_1 ]", 0-4) = ar_2 + 3
S("main_LE_589(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_ConstantStackPush_434(ar_0, ar_1, ar_2, ar_3, arityPad)) [ 0 < ar_1 /\\ 1 <= ar_1 /\\ 1 <= ar_0 ]", 0-0) = ar_0
S("main_LE_589(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_ConstantStackPush_434(ar_0, ar_1, ar_2, ar_3, arityPad)) [ 0 < ar_1 /\\ 1 <= ar_1 /\\ 1 <= ar_0 ]", 0-1) = 3*ar_0 + 9
S("main_LE_589(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_ConstantStackPush_434(ar_0, ar_1, ar_2, ar_3, arityPad)) [ 0 < ar_1 /\\ 1 <= ar_1 /\\ 1 <= ar_0 ]", 0-2) = ar_1
S("main_LE_589(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_ConstantStackPush_434(ar_0, ar_1, ar_2, ar_3, arityPad)) [ 0 < ar_1 /\\ 1 <= ar_1 /\\ 1 <= ar_0 ]", 0-3) = ar_2 + 3
S("main_LE_589(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_ConstantStackPush_434(ar_0, ar_1, ar_2, ar_3, arityPad)) [ 0 < ar_1 /\\ 1 <= ar_1 /\\ 1 <= ar_0 ]", 0-4) = ?
S("main_LE_52(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_LE_53(ar_0, ar_1, ar_2, arityPad, arityPad)) [ ar_0 <= 0 ]", 0-0) = ar_0
S("main_LE_52(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_LE_53(ar_0, ar_1, ar_2, arityPad, arityPad)) [ ar_0 <= 0 ]", 0-1) = ar_1
S("main_LE_52(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_LE_53(ar_0, ar_1, ar_2, arityPad, arityPad)) [ ar_0 <= 0 ]", 0-2) = ar_2 + 3
S("main_LE_52(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_LE_53(ar_0, ar_1, ar_2, arityPad, arityPad)) [ ar_0 <= 0 ]", 0-3) = ?
S("main_LE_52(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_LE_53(ar_0, ar_1, ar_2, arityPad, arityPad)) [ ar_0 <= 0 ]", 0-4) = ?
S("main_Load_554(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_GE_569(ar_0, ar_2, ar_1, ar_3, ar_4)) [ 1 <= ar_0 /\\ 1 <= ar_2 ]", 0-0) = ar_0
S("main_Load_554(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_GE_569(ar_0, ar_2, ar_1, ar_3, ar_4)) [ 1 <= ar_0 /\\ 1 <= ar_2 ]", 0-1) = 3*ar_0 + 84
S("main_Load_554(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_GE_569(ar_0, ar_2, ar_1, ar_3, ar_4)) [ 1 <= ar_0 /\\ 1 <= ar_2 ]", 0-2) = 3*ar_0 + 9
S("main_Load_554(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_GE_569(ar_0, ar_2, ar_1, ar_3, ar_4)) [ 1 <= ar_0 /\\ 1 <= ar_2 ]", 0-3) = ar_1
S("main_Load_554(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_GE_569(ar_0, ar_2, ar_1, ar_3, ar_4)) [ 1 <= ar_0 /\\ 1 <= ar_2 ]", 0-4) = ar_2 + 3
orients the transitions
main_Load_554(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_GE_569(ar_0, ar_2, ar_1, ar_3, ar_4)) [ 1 <= ar_0 /\ 1 <= ar_2 ]
main_GE_569(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_Load_554(ar_0, ar_2, ar_1 + 1, ar_3, ar_4)) [ 1 <= ar_1 /\ 2 <= ar_2 /\ ar_1 < ar_2 /\ 1 <= ar_0 /\ 1 <= i205' /\ 2 <= i205' /\ ar_1 + 1 = i205' ]
weakly and the transition
main_GE_569(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_Load_554(ar_0, ar_2, ar_1 + 1, ar_3, ar_4)) [ 1 <= ar_1 /\ 2 <= ar_2 /\ ar_1 < ar_2 /\ 1 <= ar_0 /\ 1 <= i205' /\ 2 <= i205' /\ ar_1 + 1 = i205' ]
strictly and produces the following problem:
6: T:
(Comp: ?, Cost: 2) main_Load_554(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_GE_569(ar_0, ar_2, ar_1, ar_3, ar_4)) [ 1 <= ar_0 /\ 1 <= ar_2 ]
(Comp: 1, Cost: 0) main_LE_52(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_LE_53(ar_0, ar_1, ar_2, arityPad, arityPad)) [ ar_0 <= 0 ]
(Comp: 2*ar_0 + 1, Cost: 1) main_LE_589(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_ConstantStackPush_434(ar_0, ar_1, ar_2, ar_3, arityPad)) [ 0 < ar_1 /\ 1 <= ar_1 /\ 1 <= ar_0 ]
(Comp: 2*ar_0 + 1, Cost: 7) main_ConstantStackPush_434(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_Load_554(ar_0, ar_1, 1, ar_2, ar_3)) [ 1 <= ar_1 /\ 1 <= ar_0 /\ 0 < ar_1 ]
(Comp: 1, Cost: 16) main_Load_1(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_LE_52(ar_0, ar_1, static'1, arityPad, arityPad)) [ static'1 <= static''' + 1 /\ 0 <= static''' /\ static''' <= ar_2 + 2 /\ 0 <= ar_2 /\ 0 <= static'1 ]
(Comp: 1, Cost: 0) main_LE_589(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_LE_590(ar_0, ar_1, ar_2, ar_3, arityPad)) [ 1 <= ar_0 /\ ar_1 <= 0 ]
(Comp: 2*ar_0 + 1, Cost: 4) main_GE_569(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_LE_589(ar_0, ar_2 - 1, ar_3, ar_4, arityPad)) [ 1 <= ar_0 /\ ar_2 - 1 = i204' /\ ar_2 <= ar_1 /\ 1 <= ar_1 ]
(Comp: 6*ar_0^2 + 23*ar_0 + 10, Cost: 3) main_GE_569(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_Load_554(ar_0, ar_2, ar_1 + 1, ar_3, ar_4)) [ 1 <= ar_1 /\ 2 <= ar_2 /\ ar_1 < ar_2 /\ 1 <= ar_0 /\ 1 <= i205' /\ 2 <= i205' /\ ar_1 + 1 = i205' ]
(Comp: 1, Cost: 1) main_LE_52(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_ConstantStackPush_434(ar_0, ar_0, ar_1, ar_2, arityPad)) [ 1 <= ar_0 /\ 0 < ar_0 ]
(Comp: 1, Cost: 0) koat_start(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_Load_1(ar_0, ar_1, ar_2, ar_3, ar_4)) [ 0 <= 0 ]
start location: koat_start
leaf cost: 0

Repeatedly propagating knowledge in problem 6 produces the following problem:
7: T:
(Comp: 6*ar_0^2 + 25*ar_0 + 11, Cost: 2) main_Load_554(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_GE_569(ar_0, ar_2, ar_1, ar_3, ar_4)) [ 1 <= ar_0 /\ 1 <= ar_2 ]
(Comp: 1, Cost: 0) main_LE_52(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_LE_53(ar_0, ar_1, ar_2, arityPad, arityPad)) [ ar_0 <= 0 ]
(Comp: 2*ar_0 + 1, Cost: 1) main_LE_589(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_ConstantStackPush_434(ar_0, ar_1, ar_2, ar_3, arityPad)) [ 0 < ar_1 /\ 1 <= ar_1 /\ 1 <= ar_0 ]
(Comp: 2*ar_0 + 1, Cost: 7) main_ConstantStackPush_434(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_Load_554(ar_0, ar_1, 1, ar_2, ar_3)) [ 1 <= ar_1 /\ 1 <= ar_0 /\ 0 < ar_1 ]
(Comp: 1, Cost: 16) main_Load_1(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_LE_52(ar_0, ar_1, static'1, arityPad, arityPad)) [ static'1 <= static''' + 1 /\ 0 <= static''' /\ static''' <= ar_2 + 2 /\ 0 <= ar_2 /\ 0 <= static'1 ]
(Comp: 1, Cost: 0) main_LE_589(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_LE_590(ar_0, ar_1, ar_2, ar_3, arityPad)) [ 1 <= ar_0 /\ ar_1 <= 0 ]
(Comp: 2*ar_0 + 1, Cost: 4) main_GE_569(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_LE_589(ar_0, ar_2 - 1, ar_3, ar_4, arityPad)) [ 1 <= ar_0 /\ ar_2 - 1 = i204' /\ ar_2 <= ar_1 /\ 1 <= ar_1 ]
(Comp: 6*ar_0^2 + 23*ar_0 + 10, Cost: 3) main_GE_569(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_Load_554(ar_0, ar_2, ar_1 + 1, ar_3, ar_4)) [ 1 <= ar_1 /\ 2 <= ar_2 /\ ar_1 < ar_2 /\ 1 <= ar_0 /\ 1 <= i205' /\ 2 <= i205' /\ ar_1 + 1 = i205' ]
(Comp: 1, Cost: 1) main_LE_52(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_ConstantStackPush_434(ar_0, ar_0, ar_1, ar_2, arityPad)) [ 1 <= ar_0 /\ 0 < ar_0 ]
(Comp: 1, Cost: 0) koat_start(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_Load_1(ar_0, ar_1, ar_2, ar_3, ar_4)) [ 0 <= 0 ]
start location: koat_start
leaf cost: 0

Complexity upper bound 30*ar_0^2 + 143*ar_0 + 81

Time: 0.251 sec (SMT: 0.211 sec)

(22) BOUNDS(CONSTANT, 81 + 143 * |#0| + 30 * |#0|^2)

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

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

(24) Obligation:

Set of 52 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 52 jbc graph edges to a weighted ITS with 52 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 52 rules
Start term: main_Load_1(#0, env, static)
Considered paths: all paths from start
Rules:
main_Load_1(i1, env, static) -{0,0}> main_Load_4(i1, env, static) :|: 0 >= 0
main_Load_4(i1, env, static) -{0,0}> langle_clinit_rangle_ConstantStackPush_5(i1, env, static) :|: 0 >= 0
langle_clinit_rangle_ConstantStackPush_5(i1, env, static) -{1,1}> langle_clinit_rangle_ArrayCreate_12(iconst_0, i1, env, static) :|: iconst_0 = 0
langle_clinit_rangle_ArrayCreate_12(iconst_0, i1, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_14(a2, i1, iconst_0, env, static) :|: a2 = 2 && iconst_0 = 0 && 0 < a2
langle_clinit_rangle_FieldAccess_14(a2, i1, iconst_0, env, static) -{1,1}> langle_clinit_rangle_New_16(i1, env, static') :|: 0 <= a2 && iconst_0 = 0 && static' <= static + a2 && 0 <= static && 0 < a2
langle_clinit_rangle_New_16(i1, env, static) -{0,0}> langle_clinit_rangle_New_18(i1, env, static) :|: 0 >= 0
langle_clinit_rangle_New_18(i1, env, static) -{0,0}> langle_clinit_rangle_New_19(i1, env, static) :|: 0 <= static
langle_clinit_rangle_New_19(i1, env, static) -{1,1}> langle_clinit_rangle_Duplicate_20(o2, i1, env, static) :|: 0 < o2 && o2 = 1
langle_clinit_rangle_Duplicate_20(o2, i1, env, static) -{1,1}> langle_clinit_rangle_ConstantStackPush_22(o2, i1, env, static) :|: 0 < o2
langle_clinit_rangle_ConstantStackPush_22(o2, i1, env, static) -{1,1}> langle_clinit_rangle_InvokeMethod_23(o2, NULL, i1, env, static) :|: NULL = 0 && 0 < o2
langle_clinit_rangle_InvokeMethod_23(o2, NULL, i1, env, static) -{1,1}> langle_init_rangle_Load_24(o2, i1, env, static) :|: NULL = 0 && 0 < o2
langle_init_rangle_Load_24(o2, i1, env, static) -{1,1}> langle_init_rangle_InvokeMethod_26(o2, i1, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_26(o2, i1, env, static) -{1,1}> langle_init_rangle_Load_28(o2, i1, env, static) :|: 0 < o2
langle_init_rangle_Load_28(o2, i1, env, static) -{1,1}> langle_init_rangle_InvokeMethod_30(o2, i1, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_30(o2, i1, env, static) -{1,1}> langle_init_rangle_Return_32(o2, i1, env, static) :|: 0 < o2
langle_init_rangle_Return_32(o2, i1, env, static) -{1,1}> langle_init_rangle_Return_34(o2, i1, env, static) :|: 0 < o2
langle_init_rangle_Return_34(o2, i1, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_36(o2, i1, env, static) :|: 0 < o2
langle_clinit_rangle_FieldAccess_36(o2, i1, env, static) -{1,1}> langle_clinit_rangle_Return_39(i1, env, static') :|: 0 < o2 && 0 <= o2 && 0 <= static && static' <= static + o2
langle_clinit_rangle_Return_39(i1, env, static) -{1,1}> main_Load_41(i1, env, static) :|: 0 >= 0
main_Load_41(i1, env, static) -{0,0}> main_Load_42(i1, env, static) :|: 0 >= 0
main_Load_42(i1, env, static) -{0,0}> main_Load_43(i1, env, static) :|: 0 <= static
main_Load_43(i1, env, static) -{0,0}> main_Load_46(i1, env, static) :|: 0 >= 0
main_Load_46(i1, env, static) -{0,0}> main_Load_48(i1, env, static) :|: 0 >= 0
main_Load_48(i1, env, static) -{1,1}> main_LE_52(i1, env, static) :|: 0 >= 0
main_LE_52(i10, env, static) -{0,0}> main_LE_54(i10, env, static) :|: 1 <= i10
main_LE_54(i10, env, static) -{1,1}> main_ConstantStackPush_58(i10, env, static) :|: 1 <= i10 && 0 < i10
main_ConstantStackPush_58(i10, env, static) -{0,0}> main_ConstantStackPush_434(i10, i10, env, static) :|: 1 <= i10
main_ConstantStackPush_434(i95, i151, env, static) -{1,1}> main_Store_437(i95, iconst_0, i151, env, static) :|: 1 <= i151 && 1 <= i95 && iconst_0 = 0
main_Store_437(i95, iconst_0, i151, env, static) -{1,1}> main_Load_438(i95, i151, iconst_0, env, static) :|: 1 <= i151 && 1 <= i95 && iconst_0 = 0
main_Load_438(i95, i151, iconst_0, env, static) -{1,1}> main_Load_439(i95, iconst_0, i151, env, static) :|: 1 <= i151 && 1 <= i95 && iconst_0 = 0
main_Load_439(i95, iconst_0, i151, env, static) -{1,1}> main_GE_441(i95, iconst_0, i151, env, static) :|: 1 <= i151 && 1 <= i95 && iconst_0 = 0
main_GE_441(i95, iconst_0, i151, env, static) -{1,1}> main_Inc_446(i95, i151, iconst_0, env, static) :|: iconst_0 < i151 && 1 <= i151 && 1 <= i95 && iconst_0 = 0
main_Inc_446(i95, i151, iconst_0, env, static) -{1,1}> main_JMP_447(i95, i151, iconst_1, env, static) :|: 1 <= i151 && 1 <= i95 && iconst_1 = 1 && iconst_0 = 0
main_JMP_447(i95, i151, iconst_1, env, static) -{1,1}> main_Load_448(i95, i151, iconst_1, env, static) :|: 1 <= i151 && 1 <= i95 && iconst_1 = 1
main_Load_448(i95, i151, iconst_1, env, static) -{0,0}> main_Load_477(i95, i151, iconst_1, env, static) :|: iconst_1 <= 2 && 1 <= iconst_1 && 1 <= i151 && 1 <= i95 && iconst_1 = 1
main_Load_477(i95, i160, i161, env, static) -{0,0}> main_Load_517(i95, i160, i161, env, static) :|: i161 <= 2 && 1 <= i160 && 1 <= i95 && 1 <= i161 && i161 <= 3
main_Load_517(i95, i180, i181, env, static) -{0,0}> main_Load_554(i95, i180, i181, env, static) :|: 1 <= i95 && 1 <= i181 && 1 <= i180 && i181 <= 3
main_Load_554(i95, i194, i195, env, static) -{1,1}> main_Load_558(i95, i195, i194, env, static) :|: 1 <= i95 && 1 <= i195
main_Load_558(i95, i195, i194, env, static) -{1,1}> main_GE_569(i95, i195, i194, env, static) :|: 1 <= i95 && 1 <= i195
main_GE_569(i95, i195, i194, env, static) -{0,0}> main_GE_571(i95, i195, i194, env, static) :|: 1 <= i95 && i194 <= i195 && 1 <= i195
main_GE_569(i95, i195, i194, env, static) -{0,0}> main_GE_572(i95, i195, i194, env, static) :|: 1 <= i95 && 1 <= i195 && i195 < i194
main_GE_571(i95, i195, i194, env, static) -{1,1}> main_Inc_573(i95, i194, env, static) :|: 1 <= i95 && i194 <= i195 && 1 <= i195
main_GE_572(i95, i195, i194, env, static) -{1,1}> main_Inc_574(i95, i194, i195, env, static) :|: 1 <= i95 && 2 <= i194 && 1 <= i195 && i195 < i194
main_Inc_573(i95, i194, env, static) -{1,1}> main_JMP_575(i95, i204, env, static) :|: i194 + -1 = i204 && 1 <= i95
main_Inc_574(i95, i194, i195, env, static) -{1,1}> main_JMP_576(i95, i194, i205, env, static) :|: i195 + 1 = i205 && 2 <= i205 && 1 <= i95 && 2 <= i194 && 1 <= i195
main_JMP_575(i95, i204, env, static) -{1,1}> main_Load_578(i95, i204, env, static) :|: 1 <= i95
main_JMP_576(i95, i194, i205, env, static) -{1,1}> main_Load_584(i95, i194, i205, env, static) :|: 2 <= i205 && 1 <= i95 && 2 <= i194
main_Load_578(i95, i204, env, static) -{1,1}> main_LE_589(i95, i204, env, static) :|: 1 <= i95
main_Load_584(i95, i194, i205, env, static) -{0,0}> main_Load_554(i95, i194, i205, env, static) :|: 1 <= i205 && 2 <= i205 && 1 <= i95 && 2 <= i194
main_LE_589(i95, i219, env, static) -{0,0}> main_LE_591(i95, i219, env, static) :|: 1 <= i219 && 1 <= i95
main_LE_591(i95, i219, env, static) -{1,1}> main_ConstantStackPush_593(i95, i219, env, static) :|: 1 <= i219 && 1 <= i95 && 0 < i219
main_ConstantStackPush_593(i95, i219, env, static) -{0,0}> main_ConstantStackPush_434(i95, i219, env, static) :|: 1 <= i219 && 1 <= i95

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

obtained
main_Load_1(i1, env, static) -{17,17}> main_ConstantStackPush_434(i1, i1, env, static'1) :|: 1 <= i1 && 0 < 2 && 0 <= static'1 && 0 <= static && 0 <= 1 && 0 < 1 && static''' <= static + 2 && 0 <= static''' && 0 <= 2 && 0 >= 0 && 0 < i1 && static'1 <= static''' + 1
by chaining
main_Load_1(i1, env, static) -{0,0}> main_Load_4(i1, env, static) :|: 0 >= 0
main_Load_4(i1, env, static) -{0,0}> langle_clinit_rangle_ConstantStackPush_5(i1, env, static) :|: 0 >= 0
langle_clinit_rangle_ConstantStackPush_5(i1, env, static) -{1,1}> langle_clinit_rangle_ArrayCreate_12(iconst_0, i1, env, static) :|: iconst_0 = 0
langle_clinit_rangle_ArrayCreate_12(iconst_0, i1, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_14(a2, i1, iconst_0, env, static) :|: a2 = 2 && iconst_0 = 0 && 0 < a2
langle_clinit_rangle_FieldAccess_14(a2, i1, iconst_0, env, static) -{1,1}> langle_clinit_rangle_New_16(i1, env, static') :|: 0 <= a2 && iconst_0 = 0 && static' <= static + a2 && 0 <= static && 0 < a2
langle_clinit_rangle_New_16(i1, env, static) -{0,0}> langle_clinit_rangle_New_18(i1, env, static) :|: 0 >= 0
langle_clinit_rangle_New_18(i1, env, static) -{0,0}> langle_clinit_rangle_New_19(i1, env, static) :|: 0 <= static
langle_clinit_rangle_New_19(i1, env, static) -{1,1}> langle_clinit_rangle_Duplicate_20(o2, i1, env, static) :|: 0 < o2 && o2 = 1
langle_clinit_rangle_Duplicate_20(o2, i1, env, static) -{1,1}> langle_clinit_rangle_ConstantStackPush_22(o2, i1, env, static) :|: 0 < o2
langle_clinit_rangle_ConstantStackPush_22(o2, i1, env, static) -{1,1}> langle_clinit_rangle_InvokeMethod_23(o2, NULL, i1, env, static) :|: NULL = 0 && 0 < o2
langle_clinit_rangle_InvokeMethod_23(o2, NULL, i1, env, static) -{1,1}> langle_init_rangle_Load_24(o2, i1, env, static) :|: NULL = 0 && 0 < o2
langle_init_rangle_Load_24(o2, i1, env, static) -{1,1}> langle_init_rangle_InvokeMethod_26(o2, i1, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_26(o2, i1, env, static) -{1,1}> langle_init_rangle_Load_28(o2, i1, env, static) :|: 0 < o2
langle_init_rangle_Load_28(o2, i1, env, static) -{1,1}> langle_init_rangle_InvokeMethod_30(o2, i1, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_30(o2, i1, env, static) -{1,1}> langle_init_rangle_Return_32(o2, i1, env, static) :|: 0 < o2
langle_init_rangle_Return_32(o2, i1, env, static) -{1,1}> langle_init_rangle_Return_34(o2, i1, env, static) :|: 0 < o2
langle_init_rangle_Return_34(o2, i1, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_36(o2, i1, env, static) :|: 0 < o2
langle_clinit_rangle_FieldAccess_36(o2, i1, env, static) -{1,1}> langle_clinit_rangle_Return_39(i1, env, static') :|: 0 < o2 && 0 <= o2 && 0 <= static && static' <= static + o2
langle_clinit_rangle_Return_39(i1, env, static) -{1,1}> main_Load_41(i1, env, static) :|: 0 >= 0
main_Load_41(i1, env, static) -{0,0}> main_Load_42(i1, env, static) :|: 0 >= 0
main_Load_42(i1, env, static) -{0,0}> main_Load_43(i1, env, static) :|: 0 <= static
main_Load_43(i1, env, static) -{0,0}> main_Load_46(i1, env, static) :|: 0 >= 0
main_Load_46(i1, env, static) -{0,0}> main_Load_48(i1, env, static) :|: 0 >= 0
main_Load_48(i1, env, static) -{1,1}> main_LE_52(i1, env, static) :|: 0 >= 0
main_LE_52(i10, env, static) -{0,0}> main_LE_54(i10, env, static) :|: 1 <= i10
main_LE_54(i10, env, static) -{1,1}> main_ConstantStackPush_58(i10, env, static) :|: 1 <= i10 && 0 < i10
main_ConstantStackPush_58(i10, env, static) -{0,0}> main_ConstantStackPush_434(i10, i10, env, static) :|: 1 <= i10

obtained
main_GE_569(i95, i195, i194, env, static) -{5,5}> main_ConstantStackPush_434(i95, i204', env, static) :|: 1 <= i195 && 1 <= i204' && 1 <= i95 && i194 <= i195 && i194 + -1 = i204' && 0 < i204'
by chaining
main_GE_569(i95, i195, i194, env, static) -{0,0}> main_GE_571(i95, i195, i194, env, static) :|: 1 <= i95 && i194 <= i195 && 1 <= i195
main_GE_571(i95, i195, i194, env, static) -{1,1}> main_Inc_573(i95, i194, env, static) :|: 1 <= i95 && i194 <= i195 && 1 <= i195
main_Inc_573(i95, i194, env, static) -{1,1}> main_JMP_575(i95, i204, env, static) :|: i194 + -1 = i204 && 1 <= i95
main_JMP_575(i95, i204, env, static) -{1,1}> main_Load_578(i95, i204, env, static) :|: 1 <= i95
main_Load_578(i95, i204, env, static) -{1,1}> main_LE_589(i95, i204, env, static) :|: 1 <= i95
main_LE_589(i95, i219, env, static) -{0,0}> main_LE_591(i95, i219, env, static) :|: 1 <= i219 && 1 <= i95
main_LE_591(i95, i219, env, static) -{1,1}> main_ConstantStackPush_593(i95, i219, env, static) :|: 1 <= i219 && 1 <= i95 && 0 < i219
main_ConstantStackPush_593(i95, i219, env, static) -{0,0}> main_ConstantStackPush_434(i95, i219, env, static) :|: 1 <= i219 && 1 <= i95

(28) Obligation:

IntTrs with 5 rules
Start term: main_Load_1(#0, env, static)
Considered paths: all paths from start
Rules:
main_Load_1(i1, env, static) -{17,17}> main_ConstantStackPush_434(i1, i1, env, static'1) :|: 1 <= i1 && 0 < 2 && 0 <= static'1 && 0 <= static && 0 <= 1 && 0 < 1 && static''' <= static + 2 && 0 <= static''' && 0 <= 2 && 0 >= 0 && 0 < i1 && static'1 <= static''' + 1
main_ConstantStackPush_434(i95, i151, env, static) -{7,7}> main_Load_554(i95, i151, 1, env, static) :|: 1 <= i151 && 1 <= 3 && 1 <= i95 && 0 < i151 && 1 <= 1 && 1 <= 2
main_Load_554(i95, i194, i195, env, static) -{2,2}> main_GE_569(i95, i195, i194, env, static) :|: 1 <= i95 && 1 <= i195
main_GE_569(i95, i195, i194, env, static) -{3,3}> main_Load_554(i95, i194, i205', env, static) :|: 1 <= i195 && 2 <= i194 && i195 < i194 && 1 <= i95 && 1 <= i205' && 2 <= i205' && i195 + 1 = i205'
main_GE_569(i95, i195, i194, env, static) -{5,5}> main_ConstantStackPush_434(i95, i204', env, static) :|: 1 <= i195 && 1 <= i204' && 1 <= i95 && i194 <= i195 && i194 + -1 = i204' && 0 < i204'

(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)
main_ConstantStackPush_434(x1, x2, x3, x4) → main_ConstantStackPush_434(x1, x2)
main_Load_554(x1, x2, x3, x4, x5) → main_Load_554(x1, x2, x3)
main_GE_569(x1, x2, x3, x4, x5) → main_GE_569(x1, x2, x3)

(30) Obligation:

IntTrs with 5 rules
Start term: main_Load_1(#0, static)
Considered paths: all paths from start
Rules:
main_Load_1(i1, static) -{17,17}> main_ConstantStackPush_434(i1, i1) :|: 1 <= i1 && 0 < 2 && 0 <= static'1 && 0 <= static && 0 <= 1 && 0 < 1 && static''' <= static + 2 && 0 <= static''' && 0 <= 2 && 0 >= 0 && 0 < i1 && static'1 <= static''' + 1
main_ConstantStackPush_434(i95, i151) -{7,7}> main_Load_554(i95, i151, 1) :|: 1 <= i151 && 1 <= 3 && 1 <= i95 && 0 < i151 && 1 <= 1 && 1 <= 2
main_Load_554(i95, i194, i195) -{2,2}> main_GE_569(i95, i195, i194) :|: 1 <= i95 && 1 <= i195
main_GE_569(i95, i195, i194) -{3,3}> main_Load_554(i95, i194, i205') :|: 1 <= i195 && 2 <= i194 && i195 < i194 && 1 <= i95 && 1 <= i205' && 2 <= i205' && i195 + 1 = i205'
main_GE_569(i95, i195, i194) -{5,5}> main_ConstantStackPush_434(i95, i204') :|: 1 <= i195 && 1 <= i204' && 1 <= i95 && i194 <= i195 && i194 + -1 = i204' && 0 < i204'

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

Moved arithmethic from constraints to rhss.

main_GE_569(i95, i195, i194) -{5,5}> main_ConstantStackPush_434(i95, i204') :|: 1 <= i195 && 1 <= i204' && 1 <= i95 && i194 <= i195 && i194 + -1 = i204' && 0 < i204'
was transformed to
main_GE_569(i95, i195, i194) -{5,5}> main_ConstantStackPush_434(i95, i194 + -1) :|: 1 <= i195 && 1 <= i204' && 1 <= i95 && i194 <= i195 && i194 + -1 = i204' && 0 < i204'

main_GE_569(i95, i195, i194) -{3,3}> main_Load_554(i95, i194, i205') :|: 1 <= i195 && 2 <= i194 && i195 < i194 && 1 <= i95 && 1 <= i205' && 2 <= i205' && i195 + 1 = i205'
was transformed to
main_GE_569(i95, i195, i194) -{3,3}> main_Load_554(i95, i194, i195 + 1) :|: 1 <= i195 && 2 <= i194 && i195 < i194 && 1 <= i95 && 1 <= i205' && 2 <= i205' && i195 + 1 = i205'

(32) Obligation:

IntTrs with 5 rules
Start term: main_Load_1(#0, static)
Considered paths: all paths from start
Rules:
main_GE_569(i95, i195, i194) -{5,5}> main_ConstantStackPush_434(i95, i194 + -1) :|: 1 <= i195 && 1 <= i204' && 1 <= i95 && i194 <= i195 && i194 + -1 = i204' && 0 < i204'
main_Load_1(i1, static) -{17,17}> main_ConstantStackPush_434(i1, i1) :|: 1 <= i1 && 0 < 2 && 0 <= static'1 && 0 <= static && 0 <= 1 && 0 < 1 && static''' <= static + 2 && 0 <= static''' && 0 <= 2 && 0 >= 0 && 0 < i1 && static'1 <= static''' + 1
main_Load_554(i95, i194, i195) -{2,2}> main_GE_569(i95, i195, i194) :|: 1 <= i95 && 1 <= i195
main_GE_569(i95, i195, i194) -{3,3}> main_Load_554(i95, i194, i195 + 1) :|: 1 <= i195 && 2 <= i194 && i195 < i194 && 1 <= i95 && 1 <= i205' && 2 <= i205' && i195 + 1 = i205'
main_ConstantStackPush_434(i95, i151) -{7,7}> main_Load_554(i95, i151, 1) :|: 1 <= i151 && 1 <= 3 && 1 <= i95 && 0 < i151 && 1 <= 1 && 1 <= 2

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

Simplified expressions.

main_Load_1(i1, static) -{17,17}> main_ConstantStackPush_434(i1, i1) :|: 1 <= i1 && 0 < 2 && 0 <= static'1 && 0 <= static && 0 <= 1 && 0 < 1 && static''' <= static + 2 && 0 <= static''' && 0 <= 2 && 0 >= 0 && 0 < i1 && static'1 <= static''' + 1
was transformed to
main_Load_1(i1, static) -{17,17}> main_ConstantStackPush_434(i1, i1) :|: 1 <= i1 && 0 <= static'1 && 0 <= static && static''' <= static + 2 && 0 <= static''' && 0 < i1 && static'1 <= static''' + 1

main_GE_569(i95, i195, i194) -{5,5}> main_ConstantStackPush_434(i95, i194 + -1) :|: 1 <= i195 && 1 <= i204' && 1 <= i95 && i194 <= i195 && i194 + -1 = i204' && 0 < i204'
was transformed to
main_GE_569(i95, i195, i194) -{5,5}> main_ConstantStackPush_434(i95, i194 - 1) :|: 1 <= i195 && 1 <= i204' && 1 <= i95 && i194 <= i195 && i194 - 1 = i204' && 0 < i204'

main_ConstantStackPush_434(i95, i151) -{7,7}> main_Load_554(i95, i151, 1) :|: 1 <= i151 && 1 <= 3 && 1 <= i95 && 0 < i151 && 1 <= 1 && 1 <= 2
was transformed to
main_ConstantStackPush_434(i95, i151) -{7,7}> main_Load_554(i95, i151, 1) :|: 1 <= i151 && 1 <= i95 && 0 < i151

(34) Obligation:

IntTrs with 5 rules
Start term: main_Load_1(#0, static)
Considered paths: all paths from start
Rules:
main_ConstantStackPush_434(i95, i151) -{7,7}> main_Load_554(i95, i151, 1) :|: 1 <= i151 && 1 <= i95 && 0 < i151
main_GE_569(i95, i195, i194) -{5,5}> main_ConstantStackPush_434(i95, i194 - 1) :|: 1 <= i195 && 1 <= i204' && 1 <= i95 && i194 <= i195 && i194 - 1 = i204' && 0 < i204'
main_Load_1(i1, static) -{17,17}> main_ConstantStackPush_434(i1, i1) :|: 1 <= i1 && 0 <= static'1 && 0 <= static && static''' <= static + 2 && 0 <= static''' && 0 < i1 && static'1 <= static''' + 1
main_GE_569(i95, i195, i194) -{3,3}> main_Load_554(i95, i194, i195 + 1) :|: 1 <= i195 && 2 <= i194 && i195 < i194 && 1 <= i95 && 1 <= i205' && 2 <= i205' && i195 + 1 = i205'
main_Load_554(i95, i194, i195) -{2,2}> main_GE_569(i95, i195, i194) :|: 1 <= i95 && 1 <= i195

(35) koat Proof (EQUIVALENT transformation)

YES(?, 43*ar_0 + 10*ar_0^2 + 36)

Initial complexity problem:
1: T:
(Comp: ?, Cost: 7) main_ConstantStackPush_434(ar_0, ar_1, ar_2) -> Com_1(main_Load_554(ar_0, ar_1, 1)) [ 1 <= ar_1 /\ 1 <= ar_0 /\ 0 < ar_1 ]
(Comp: ?, Cost: 5) main_GE_569(ar_0, ar_1, ar_2) -> Com_1(main_ConstantStackPush_434(ar_0, ar_2 - 1, arityPad)) [ 1 <= ar_1 /\ 1 <= i204' /\ 1 <= ar_0 /\ ar_2 <= ar_1 /\ ar_2 - 1 = i204' /\ 0 < i204' ]
(Comp: ?, Cost: 17) main_Load_1(ar_0, ar_1, ar_2) -> Com_1(main_ConstantStackPush_434(ar_0, ar_0, arityPad)) [ 1 <= ar_0 /\ 0 <= static'1 /\ 0 <= ar_1 /\ static''' <= ar_1 + 2 /\ 0 <= static''' /\ 0 < ar_0 /\ static'1 <= static''' + 1 ]
(Comp: ?, Cost: 3) main_GE_569(ar_0, ar_1, ar_2) -> Com_1(main_Load_554(ar_0, ar_2, ar_1 + 1)) [ 1 <= ar_1 /\ 2 <= ar_2 /\ ar_1 < ar_2 /\ 1 <= ar_0 /\ 1 <= i205' /\ 2 <= i205' /\ ar_1 + 1 = i205' ]
(Comp: ?, Cost: 2) main_Load_554(ar_0, ar_1, ar_2) -> Com_1(main_GE_569(ar_0, ar_2, ar_1)) [ 1 <= ar_0 /\ 1 <= ar_2 ]
(Comp: 1, Cost: 0) koat_start(ar_0, ar_1, ar_2) -> Com_1(main_Load_1(ar_0, ar_1, ar_2)) [ 0 <= 0 ]
start location: koat_start
leaf cost: 0

Repeatedly propagating knowledge in problem 1 produces the following problem:
2: T:
(Comp: ?, Cost: 7) main_ConstantStackPush_434(ar_0, ar_1, ar_2) -> Com_1(main_Load_554(ar_0, ar_1, 1)) [ 1 <= ar_1 /\ 1 <= ar_0 /\ 0 < ar_1 ]
(Comp: ?, Cost: 5) main_GE_569(ar_0, ar_1, ar_2) -> Com_1(main_ConstantStackPush_434(ar_0, ar_2 - 1, arityPad)) [ 1 <= ar_1 /\ 1 <= i204' /\ 1 <= ar_0 /\ ar_2 <= ar_1 /\ ar_2 - 1 = i204' /\ 0 < i204' ]
(Comp: 1, Cost: 17) main_Load_1(ar_0, ar_1, ar_2) -> Com_1(main_ConstantStackPush_434(ar_0, ar_0, arityPad)) [ 1 <= ar_0 /\ 0 <= static'1 /\ 0 <= ar_1 /\ static''' <= ar_1 + 2 /\ 0 <= static''' /\ 0 < ar_0 /\ static'1 <= static''' + 1 ]
(Comp: ?, Cost: 3) main_GE_569(ar_0, ar_1, ar_2) -> Com_1(main_Load_554(ar_0, ar_2, ar_1 + 1)) [ 1 <= ar_1 /\ 2 <= ar_2 /\ ar_1 < ar_2 /\ 1 <= ar_0 /\ 1 <= i205' /\ 2 <= i205' /\ ar_1 + 1 = i205' ]
(Comp: ?, Cost: 2) main_Load_554(ar_0, ar_1, ar_2) -> Com_1(main_GE_569(ar_0, ar_2, ar_1)) [ 1 <= ar_0 /\ 1 <= ar_2 ]
(Comp: 1, Cost: 0) koat_start(ar_0, ar_1, ar_2) -> Com_1(main_Load_1(ar_0, ar_1, ar_2)) [ 0 <= 0 ]
start location: koat_start
leaf cost: 0

A polynomial rank function with
Pol(main_ConstantStackPush_434) = 2*V_2 + 1
Pol(main_Load_554) = 2*V_2
Pol(main_GE_569) = 2*V_3
Pol(main_Load_1) = 2*V_1 + 1
Pol(koat_start) = 2*V_1 + 1
orients all transitions weakly and the transitions
main_GE_569(ar_0, ar_1, ar_2) -> Com_1(main_ConstantStackPush_434(ar_0, ar_2 - 1, arityPad)) [ 1 <= ar_1 /\ 1 <= i204' /\ 1 <= ar_0 /\ ar_2 <= ar_1 /\ ar_2 - 1 = i204' /\ 0 < i204' ]
main_ConstantStackPush_434(ar_0, ar_1, ar_2) -> Com_1(main_Load_554(ar_0, ar_1, 1)) [ 1 <= ar_1 /\ 1 <= ar_0 /\ 0 < ar_1 ]
strictly and produces the following problem:
3: T:
(Comp: 2*ar_0 + 1, Cost: 7) main_ConstantStackPush_434(ar_0, ar_1, ar_2) -> Com_1(main_Load_554(ar_0, ar_1, 1)) [ 1 <= ar_1 /\ 1 <= ar_0 /\ 0 < ar_1 ]
(Comp: 2*ar_0 + 1, Cost: 5) main_GE_569(ar_0, ar_1, ar_2) -> Com_1(main_ConstantStackPush_434(ar_0, ar_2 - 1, arityPad)) [ 1 <= ar_1 /\ 1 <= i204' /\ 1 <= ar_0 /\ ar_2 <= ar_1 /\ ar_2 - 1 = i204' /\ 0 < i204' ]
(Comp: 1, Cost: 17) main_Load_1(ar_0, ar_1, ar_2) -> Com_1(main_ConstantStackPush_434(ar_0, ar_0, arityPad)) [ 1 <= ar_0 /\ 0 <= static'1 /\ 0 <= ar_1 /\ static''' <= ar_1 + 2 /\ 0 <= static''' /\ 0 < ar_0 /\ static'1 <= static''' + 1 ]
(Comp: ?, Cost: 3) main_GE_569(ar_0, ar_1, ar_2) -> Com_1(main_Load_554(ar_0, ar_2, ar_1 + 1)) [ 1 <= ar_1 /\ 2 <= ar_2 /\ ar_1 < ar_2 /\ 1 <= ar_0 /\ 1 <= i205' /\ 2 <= i205' /\ ar_1 + 1 = i205' ]
(Comp: ?, Cost: 2) main_Load_554(ar_0, ar_1, ar_2) -> Com_1(main_GE_569(ar_0, ar_2, ar_1)) [ 1 <= ar_0 /\ 1 <= ar_2 ]
(Comp: 1, Cost: 0) koat_start(ar_0, ar_1, ar_2) -> Com_1(main_Load_1(ar_0, ar_1, ar_2)) [ 0 <= 0 ]
start location: koat_start
leaf cost: 0

A polynomial rank function with
Pol(main_Load_554) = V_2 - V_3
Pol(main_GE_569) = -V_2 + V_3
and size complexities
S("koat_start(ar_0, ar_1, ar_2) -> Com_1(main_Load_1(ar_0, ar_1, ar_2)) [ 0 <= 0 ]", 0-0) = ar_0
S("koat_start(ar_0, ar_1, ar_2) -> Com_1(main_Load_1(ar_0, ar_1, ar_2)) [ 0 <= 0 ]", 0-1) = ar_1
S("koat_start(ar_0, ar_1, ar_2) -> Com_1(main_Load_1(ar_0, ar_1, ar_2)) [ 0 <= 0 ]", 0-2) = ar_2
S("main_Load_554(ar_0, ar_1, ar_2) -> Com_1(main_GE_569(ar_0, ar_2, ar_1)) [ 1 <= ar_0 /\\ 1 <= ar_2 ]", 0-0) = ar_0
S("main_Load_554(ar_0, ar_1, ar_2) -> Com_1(main_GE_569(ar_0, ar_2, ar_1)) [ 1 <= ar_0 /\\ 1 <= ar_2 ]", 0-1) = ar_0 + 1
S("main_Load_554(ar_0, ar_1, ar_2) -> Com_1(main_GE_569(ar_0, ar_2, ar_1)) [ 1 <= ar_0 /\\ 1 <= ar_2 ]", 0-2) = ar_0
S("main_GE_569(ar_0, ar_1, ar_2) -> Com_1(main_Load_554(ar_0, ar_2, ar_1 + 1)) [ 1 <= ar_1 /\\ 2 <= ar_2 /\\ ar_1 < ar_2 /\\ 1 <= ar_0 /\\ 1 <= i205' /\\ 2 <= i205' /\\ ar_1 + 1 = i205' ]", 0-0) = ar_0
S("main_GE_569(ar_0, ar_1, ar_2) -> Com_1(main_Load_554(ar_0, ar_2, ar_1 + 1)) [ 1 <= ar_1 /\\ 2 <= ar_2 /\\ ar_1 < ar_2 /\\ 1 <= ar_0 /\\ 1 <= i205' /\\ 2 <= i205' /\\ ar_1 + 1 = i205' ]", 0-1) = ar_0
S("main_GE_569(ar_0, ar_1, ar_2) -> Com_1(main_Load_554(ar_0, ar_2, ar_1 + 1)) [ 1 <= ar_1 /\\ 2 <= ar_2 /\\ ar_1 < ar_2 /\\ 1 <= ar_0 /\\ 1 <= i205' /\\ 2 <= i205' /\\ ar_1 + 1 = i205' ]", 0-2) = ar_0
S("main_Load_1(ar_0, ar_1, ar_2) -> Com_1(main_ConstantStackPush_434(ar_0, ar_0, arityPad)) [ 1 <= ar_0 /\\ 0 <= static'1 /\\ 0 <= ar_1 /\\ static''' <= ar_1 + 2 /\\ 0 <= static''' /\\ 0 < ar_0 /\\ static'1 <= static''' + 1 ]", 0-0) = ar_0
S("main_Load_1(ar_0, ar_1, ar_2) -> Com_1(main_ConstantStackPush_434(ar_0, ar_0, arityPad)) [ 1 <= ar_0 /\\ 0 <= static'1 /\\ 0 <= ar_1 /\\ static''' <= ar_1 + 2 /\\ 0 <= static''' /\\ 0 < ar_0 /\\ static'1 <= static''' + 1 ]", 0-1) = ar_0
S("main_Load_1(ar_0, ar_1, ar_2) -> Com_1(main_ConstantStackPush_434(ar_0, ar_0, arityPad)) [ 1 <= ar_0 /\\ 0 <= static'1 /\\ 0 <= ar_1 /\\ static''' <= ar_1 + 2 /\\ 0 <= static''' /\\ 0 < ar_0 /\\ static'1 <= static''' + 1 ]", 0-2) = ?
S("main_GE_569(ar_0, ar_1, ar_2) -> Com_1(main_ConstantStackPush_434(ar_0, ar_2 - 1, arityPad)) [ 1 <= ar_1 /\\ 1 <= i204' /\\ 1 <= ar_0 /\\ ar_2 <= ar_1 /\\ ar_2 - 1 = i204' /\\ 0 < i204' ]", 0-0) = ar_0
S("main_GE_569(ar_0, ar_1, ar_2) -> Com_1(main_ConstantStackPush_434(ar_0, ar_2 - 1, arityPad)) [ 1 <= ar_1 /\\ 1 <= i204' /\\ 1 <= ar_0 /\\ ar_2 <= ar_1 /\\ ar_2 - 1 = i204' /\\ 0 < i204' ]", 0-1) = ar_0
S("main_GE_569(ar_0, ar_1, ar_2) -> Com_1(main_ConstantStackPush_434(ar_0, ar_2 - 1, arityPad)) [ 1 <= ar_1 /\\ 1 <= i204' /\\ 1 <= ar_0 /\\ ar_2 <= ar_1 /\\ ar_2 - 1 = i204' /\\ 0 < i204' ]", 0-2) = ?
S("main_ConstantStackPush_434(ar_0, ar_1, ar_2) -> Com_1(main_Load_554(ar_0, ar_1, 1)) [ 1 <= ar_1 /\\ 1 <= ar_0 /\\ 0 < ar_1 ]", 0-0) = ar_0
S("main_ConstantStackPush_434(ar_0, ar_1, ar_2) -> Com_1(main_Load_554(ar_0, ar_1, 1)) [ 1 <= ar_1 /\\ 1 <= ar_0 /\\ 0 < ar_1 ]", 0-1) = ar_0
S("main_ConstantStackPush_434(ar_0, ar_1, ar_2) -> Com_1(main_Load_554(ar_0, ar_1, 1)) [ 1 <= ar_1 /\\ 1 <= ar_0 /\\ 0 < ar_1 ]", 0-2) = 1
orients the transitions
main_Load_554(ar_0, ar_1, ar_2) -> Com_1(main_GE_569(ar_0, ar_2, ar_1)) [ 1 <= ar_0 /\ 1 <= ar_2 ]
main_GE_569(ar_0, ar_1, ar_2) -> Com_1(main_Load_554(ar_0, ar_2, ar_1 + 1)) [ 1 <= ar_1 /\ 2 <= ar_2 /\ ar_1 < ar_2 /\ 1 <= ar_0 /\ 1 <= i205' /\ 2 <= i205' /\ ar_1 + 1 = i205' ]
weakly and the transition
main_GE_569(ar_0, ar_1, ar_2) -> Com_1(main_Load_554(ar_0, ar_2, ar_1 + 1)) [ 1 <= ar_1 /\ 2 <= ar_2 /\ ar_1 < ar_2 /\ 1 <= ar_0 /\ 1 <= i205' /\ 2 <= i205' /\ ar_1 + 1 = i205' ]
strictly and produces the following problem:
4: T:
(Comp: 2*ar_0 + 1, Cost: 7) main_ConstantStackPush_434(ar_0, ar_1, ar_2) -> Com_1(main_Load_554(ar_0, ar_1, 1)) [ 1 <= ar_1 /\ 1 <= ar_0 /\ 0 < ar_1 ]
(Comp: 2*ar_0 + 1, Cost: 5) main_GE_569(ar_0, ar_1, ar_2) -> Com_1(main_ConstantStackPush_434(ar_0, ar_2 - 1, arityPad)) [ 1 <= ar_1 /\ 1 <= i204' /\ 1 <= ar_0 /\ ar_2 <= ar_1 /\ ar_2 - 1 = i204' /\ 0 < i204' ]
(Comp: 1, Cost: 17) main_Load_1(ar_0, ar_1, ar_2) -> Com_1(main_ConstantStackPush_434(ar_0, ar_0, arityPad)) [ 1 <= ar_0 /\ 0 <= static'1 /\ 0 <= ar_1 /\ static''' <= ar_1 + 2 /\ 0 <= static''' /\ 0 < ar_0 /\ static'1 <= static''' + 1 ]
(Comp: 2*ar_0^2 + 3*ar_0 + 1, Cost: 3) main_GE_569(ar_0, ar_1, ar_2) -> Com_1(main_Load_554(ar_0, ar_2, ar_1 + 1)) [ 1 <= ar_1 /\ 2 <= ar_2 /\ ar_1 < ar_2 /\ 1 <= ar_0 /\ 1 <= i205' /\ 2 <= i205' /\ ar_1 + 1 = i205' ]
(Comp: ?, Cost: 2) main_Load_554(ar_0, ar_1, ar_2) -> Com_1(main_GE_569(ar_0, ar_2, ar_1)) [ 1 <= ar_0 /\ 1 <= ar_2 ]
(Comp: 1, Cost: 0) koat_start(ar_0, ar_1, ar_2) -> Com_1(main_Load_1(ar_0, ar_1, ar_2)) [ 0 <= 0 ]
start location: koat_start
leaf cost: 0

Repeatedly propagating knowledge in problem 4 produces the following problem:
5: T:
(Comp: 2*ar_0 + 1, Cost: 7) main_ConstantStackPush_434(ar_0, ar_1, ar_2) -> Com_1(main_Load_554(ar_0, ar_1, 1)) [ 1 <= ar_1 /\ 1 <= ar_0 /\ 0 < ar_1 ]
(Comp: 2*ar_0 + 1, Cost: 5) main_GE_569(ar_0, ar_1, ar_2) -> Com_1(main_ConstantStackPush_434(ar_0, ar_2 - 1, arityPad)) [ 1 <= ar_1 /\ 1 <= i204' /\ 1 <= ar_0 /\ ar_2 <= ar_1 /\ ar_2 - 1 = i204' /\ 0 < i204' ]
(Comp: 1, Cost: 17) main_Load_1(ar_0, ar_1, ar_2) -> Com_1(main_ConstantStackPush_434(ar_0, ar_0, arityPad)) [ 1 <= ar_0 /\ 0 <= static'1 /\ 0 <= ar_1 /\ static''' <= ar_1 + 2 /\ 0 <= static''' /\ 0 < ar_0 /\ static'1 <= static''' + 1 ]
(Comp: 2*ar_0^2 + 3*ar_0 + 1, Cost: 3) main_GE_569(ar_0, ar_1, ar_2) -> Com_1(main_Load_554(ar_0, ar_2, ar_1 + 1)) [ 1 <= ar_1 /\ 2 <= ar_2 /\ ar_1 < ar_2 /\ 1 <= ar_0 /\ 1 <= i205' /\ 2 <= i205' /\ ar_1 + 1 = i205' ]
(Comp: 2*ar_0^2 + 5*ar_0 + 2, Cost: 2) main_Load_554(ar_0, ar_1, ar_2) -> Com_1(main_GE_569(ar_0, ar_2, ar_1)) [ 1 <= ar_0 /\ 1 <= ar_2 ]
(Comp: 1, Cost: 0) koat_start(ar_0, ar_1, ar_2) -> Com_1(main_Load_1(ar_0, ar_1, ar_2)) [ 0 <= 0 ]
start location: koat_start
leaf cost: 0

Complexity upper bound 43*ar_0 + 10*ar_0^2 + 36

Time: 0.224 sec (SMT: 0.213 sec)

(0) Obligation:

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

(2) Obligation:

(3) TerminationGraphToComplexityProof (BOTH CONCRETE BOUNDS(ID, ADD(4)) 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) MovedArithmeticFromConstraintsProof (BOTH CONCRETE BOUNDS(ID, ID) transformation)

(18) Obligation:

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

(20) Obligation:

(21) koat Proof (EQUIVALENT transformation)

(22) BOUNDS(CONSTANT, 81 + 143 * |#0| + 30 * |#0|^2)

(23) TerminationGraphToComplexityProof (BOTH CONCRETE BOUNDS(ID, ADD(4)) 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, 36 + 43 * |#0| + 10 * |#0|^2)