time complexity proof of /tmp/tmpYlQKZ3/PastaC2.jar

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

0 JBC problem

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

↳2 JBCTerminationGraph

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

↳4 JBCComplexityEdges

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

    ↳6 WeightedIntTrs

        ↳7 StraightLineCodeCompressionProof (BOTH CONCRETE BOUNDS(ID, ID), 28 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), 85 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 TerminationGraphToComplexityProof (BOTH CONCRETE BOUNDS(ID, ADD(4)), 1 ms)

↳22 JBCComplexityEdges

    ↳23 JBCGraphEdgesToCpxIntTrsProof (CONCRETE UPPER BOUND(ID), 62 ms)

    ↳24 WeightedIntTrs

    ↳25 StraightLineCodeCompressionProof (BOTH CONCRETE BOUNDS(ID, ID), 14 ms)

    ↳26 WeightedIntTrs

    ↳27 WeightedIntTrsUnneededArgumentFilterProof (CONCRETE UPPER BOUND(ID), 4 ms)

    ↳28 WeightedIntTrs

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

    ↳30 WeightedIntTrs

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

    ↳32 WeightedIntTrs

    ↳33 koat Proof (⇔, 83 ms)

    ↳34 BOUNDS(CONSTANT, 88 + 157 * |#0| + 30 * |#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 PastaC2 {
    public static void main(int x) {
        while (x >= 0) {
            x = x+1;
            int y = 1;
            while (x >= y) {
                y++;
            }
            x = x-2;
        }
    }
}

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

Constructed TerminationGraph.

(2) Obligation:

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

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

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

(4) Obligation:

Set of 56 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 56 jbc graph edges to a weighted ITS with 56 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 56 rules
Start term: main_Load_2(#0, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_Load_2(i2, env, static) -{0,0}> main_Load_4(i2, env, static) :|: 0 >= 0
main_Load_4(i2, env, static) -{0,0}> langle_clinit_rangle_ConstantStackPush_6(i2, env, static) :|: 0 >= 0
langle_clinit_rangle_ConstantStackPush_6(i2, env, static) -{1,1}> langle_clinit_rangle_ArrayCreate_12(iconst_0, i2, env, static) :|: iconst_0 = 0
langle_clinit_rangle_ArrayCreate_12(iconst_0, i2, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_14(a2, i2, iconst_0, env, static) :|: a2 = 2 && iconst_0 = 0 && 0 < a2
langle_clinit_rangle_FieldAccess_14(a2, i2, iconst_0, env, static) -{1,1}> langle_clinit_rangle_New_16(i2, env, static') :|: 0 <= a2 && iconst_0 = 0 && static' <= static + a2 && 0 <= static && 0 < a2
langle_clinit_rangle_New_16(i2, env, static) -{0,0}> langle_clinit_rangle_New_17(i2, env, static) :|: 0 >= 0
langle_clinit_rangle_New_17(i2, env, static) -{0,0}> langle_clinit_rangle_New_19(i2, env, static) :|: 0 <= static
langle_clinit_rangle_New_19(i2, env, static) -{1,1}> langle_clinit_rangle_Duplicate_20(o2, i2, env, static) :|: 0 < o2 && o2 = 1
langle_clinit_rangle_Duplicate_20(o2, i2, env, static) -{1,1}> langle_clinit_rangle_ConstantStackPush_22(o2, i2, env, static) :|: 0 < o2
langle_clinit_rangle_ConstantStackPush_22(o2, i2, env, static) -{1,1}> langle_clinit_rangle_InvokeMethod_23(o2, NULL, i2, env, static) :|: NULL = 0 && 0 < o2
langle_clinit_rangle_InvokeMethod_23(o2, NULL, i2, env, static) -{1,1}> langle_init_rangle_Load_25(o2, i2, env, static) :|: NULL = 0 && 0 < o2
langle_init_rangle_Load_25(o2, i2, env, static) -{1,1}> langle_init_rangle_InvokeMethod_27(o2, i2, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_27(o2, i2, env, static) -{1,1}> langle_init_rangle_Load_29(o2, i2, env, static) :|: 0 < o2
langle_init_rangle_Load_29(o2, i2, env, static) -{1,1}> langle_init_rangle_InvokeMethod_31(o2, i2, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_31(o2, i2, env, static) -{1,1}> langle_init_rangle_Return_34(o2, i2, env, static) :|: 0 < o2
langle_init_rangle_Return_34(o2, i2, env, static) -{1,1}> langle_init_rangle_Return_36(o2, i2, env, static) :|: 0 < o2
langle_init_rangle_Return_36(o2, i2, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_39(o2, i2, env, static) :|: 0 < o2
langle_clinit_rangle_FieldAccess_39(o2, i2, env, static) -{1,1}> langle_clinit_rangle_Return_40(i2, env, static') :|: 0 < o2 && 0 <= o2 && 0 <= static && static' <= static + o2
langle_clinit_rangle_Return_40(i2, env, static) -{1,1}> main_Load_41(i2, env, static) :|: 0 >= 0
main_Load_41(i2, env, static) -{0,0}> main_Load_42(i2, env, static) :|: 0 >= 0
main_Load_42(i2, env, static) -{0,0}> main_Load_44(i2, env, static) :|: 0 <= static
main_Load_44(i2, env, static) -{0,0}> main_Load_45(i2, env, static) :|: 0 >= 0
main_Load_45(i2, env, static) -{0,0}> main_Load_48(i2, env, static) :|: 0 >= 0
main_Load_48(i2, env, static) -{1,1}> main_LT_52(i2, env, static) :|: 0 >= 0
main_LT_52(i9, env, static) -{0,0}> main_LT_53(i9, env, static) :|: i9 <= -1
main_LT_52(i10, env, static) -{0,0}> main_LT_54(i10, env, static) :|: 0 <= i10
main_LT_54(i10, env, static) -{1,1}> main_Load_56(i10, env, static) :|: 0 <= i10
main_Load_56(i10, env, static) -{0,0}> main_Load_308(i10, i10, env, static) :|: 0 <= i10
main_Load_308(i10, i72, env, static) -{1,1}> main_ConstantStackPush_309(i10, i72, env, static) :|: 0 <= i10 && 0 <= i72
main_ConstantStackPush_309(i10, i72, env, static) -{1,1}> main_IntArithmetic_310(i10, i72, iconst_1, env, static) :|: 0 <= i10 && iconst_1 = 1 && 0 <= i72
main_IntArithmetic_310(i10, i72, iconst_1, env, static) -{1,1}> main_Store_311(i10, i74, env, static) :|: 0 <= i10 && 1 <= i74 && i72 + iconst_1 = i74 && iconst_1 = 1 && 0 <= i72
main_Store_311(i10, i74, env, static) -{1,1}> main_ConstantStackPush_313(i10, i74, env, static) :|: 0 <= i10 && 1 <= i74
main_ConstantStackPush_313(i10, i74, env, static) -{1,1}> main_Store_314(i10, iconst_1, i74, env, static) :|: 0 <= i10 && 1 <= i74 && iconst_1 = 1
main_Store_314(i10, iconst_1, i74, env, static) -{1,1}> main_Load_316(i10, i74, iconst_1, env, static) :|: 0 <= i10 && 1 <= i74 && iconst_1 = 1
main_Load_316(i10, i74, iconst_1, env, static) -{0,0}> main_Load_361(i10, i74, iconst_1, env, static) :|: 0 <= i10 && 1 <= iconst_1 && 1 <= i74 && iconst_1 = 1 && iconst_1 <= 3
main_Load_361(i10, i82, i83, env, static) -{0,0}> main_Load_393(i10, i82, i83, env, static) :|: 0 <= i10 && 1 <= i83 && i83 <= 3 && i83 <= 4
main_Load_393(i10, i92, i93, env, static) -{0,0}> main_Load_413(i10, i92, i93, env, static) :|: 0 <= i10 && 1 <= i93 && i93 <= 4
main_Load_413(i10, i100, i101, env, static) -{1,1}> main_Load_414(i10, i100, i101, env, static) :|: 0 <= i10 && 1 <= i101
main_Load_414(i10, i100, i101, env, static) -{1,1}> main_LT_420(i10, i100, i101, env, static) :|: 0 <= i10 && 1 <= i101
main_LT_420(i10, i100, i101, env, static) -{0,0}> main_LT_427(i10, i100, i101, env, static) :|: 0 <= i10 && i100 < i101 && 1 <= i101
main_LT_420(i10, i100, i101, env, static) -{0,0}> main_LT_428(i10, i100, i101, env, static) :|: 0 <= i10 && 1 <= i101 && i101 <= i100
main_LT_427(i10, i100, i101, env, static) -{1,1}> main_Load_429(i10, i100, env, static) :|: 0 <= i10 && i100 < i101 && 1 <= i101
main_LT_428(i10, i100, i101, env, static) -{1,1}> main_Inc_431(i10, i100, i101, env, static) :|: 0 <= i10 && 1 <= i101 && 1 <= i100 && i101 <= i100
main_Load_429(i10, i100, env, static) -{1,1}> main_ConstantStackPush_433(i10, i100, env, static) :|: 0 <= i10
main_Inc_431(i10, i100, i101, env, static) -{1,1}> main_JMP_436(i10, i100, i105, env, static) :|: 0 <= i10 && 1 <= i101 && 2 <= i105 && 1 <= i100 && i101 + 1 = i105
main_ConstantStackPush_433(i10, i100, env, static) -{1,1}> main_IntArithmetic_438(i10, i100, iconst_2, env, static) :|: 0 <= i10 && iconst_2 = 2
main_JMP_436(i10, i100, i105, env, static) -{1,1}> main_Load_442(i10, i100, i105, env, static) :|: 0 <= i10 && 2 <= i105 && 1 <= i100
main_IntArithmetic_438(i10, i100, iconst_2, env, static) -{1,1}> main_Store_444(i10, i108, env, static) :|: 0 <= i10 && iconst_2 = 2 && i100 - iconst_2 = i108
main_Load_442(i10, i100, i105, env, static) -{0,0}> main_Load_413(i10, i100, i105, env, static) :|: 0 <= i10 && 2 <= i105 && 1 <= i100 && 1 <= i105
main_Store_444(i10, i108, env, static) -{1,1}> main_JMP_445(i10, i108, env, static) :|: 0 <= i10
main_JMP_445(i10, i108, env, static) -{1,1}> main_Load_446(i10, i108, env, static) :|: 0 <= i10
main_Load_446(i10, i108, env, static) -{1,1}> main_LT_447(i10, i108, env, static) :|: 0 <= i10
main_LT_447(i10, i117, env, static) -{0,0}> main_LT_449(i10, i117, env, static) :|: 0 <= i10 && i117 <= -1
main_LT_447(i10, i118, env, static) -{0,0}> main_LT_450(i10, i118, env, static) :|: 0 <= i10 && 0 <= i118
main_LT_450(i10, i118, env, static) -{1,1}> main_Load_457(i10, i118, env, static) :|: 0 <= i10 && 0 <= i118
main_Load_457(i10, i118, env, static) -{0,0}> main_Load_308(i10, i118, env, static) :|: 0 <= i10 && 0 <= i118

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

obtained
main_Load_2(i2, env, static) -{16,16}> main_LT_52(i2, 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_2(i2, env, static) -{0,0}> main_Load_4(i2, env, static) :|: 0 >= 0
main_Load_4(i2, env, static) -{0,0}> langle_clinit_rangle_ConstantStackPush_6(i2, env, static) :|: 0 >= 0
langle_clinit_rangle_ConstantStackPush_6(i2, env, static) -{1,1}> langle_clinit_rangle_ArrayCreate_12(iconst_0, i2, env, static) :|: iconst_0 = 0
langle_clinit_rangle_ArrayCreate_12(iconst_0, i2, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_14(a2, i2, iconst_0, env, static) :|: a2 = 2 && iconst_0 = 0 && 0 < a2
langle_clinit_rangle_FieldAccess_14(a2, i2, iconst_0, env, static) -{1,1}> langle_clinit_rangle_New_16(i2, env, static') :|: 0 <= a2 && iconst_0 = 0 && static' <= static + a2 && 0 <= static && 0 < a2
langle_clinit_rangle_New_16(i2, env, static) -{0,0}> langle_clinit_rangle_New_17(i2, env, static) :|: 0 >= 0
langle_clinit_rangle_New_17(i2, env, static) -{0,0}> langle_clinit_rangle_New_19(i2, env, static) :|: 0 <= static
langle_clinit_rangle_New_19(i2, env, static) -{1,1}> langle_clinit_rangle_Duplicate_20(o2, i2, env, static) :|: 0 < o2 && o2 = 1
langle_clinit_rangle_Duplicate_20(o2, i2, env, static) -{1,1}> langle_clinit_rangle_ConstantStackPush_22(o2, i2, env, static) :|: 0 < o2
langle_clinit_rangle_ConstantStackPush_22(o2, i2, env, static) -{1,1}> langle_clinit_rangle_InvokeMethod_23(o2, NULL, i2, env, static) :|: NULL = 0 && 0 < o2
langle_clinit_rangle_InvokeMethod_23(o2, NULL, i2, env, static) -{1,1}> langle_init_rangle_Load_25(o2, i2, env, static) :|: NULL = 0 && 0 < o2
langle_init_rangle_Load_25(o2, i2, env, static) -{1,1}> langle_init_rangle_InvokeMethod_27(o2, i2, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_27(o2, i2, env, static) -{1,1}> langle_init_rangle_Load_29(o2, i2, env, static) :|: 0 < o2
langle_init_rangle_Load_29(o2, i2, env, static) -{1,1}> langle_init_rangle_InvokeMethod_31(o2, i2, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_31(o2, i2, env, static) -{1,1}> langle_init_rangle_Return_34(o2, i2, env, static) :|: 0 < o2
langle_init_rangle_Return_34(o2, i2, env, static) -{1,1}> langle_init_rangle_Return_36(o2, i2, env, static) :|: 0 < o2
langle_init_rangle_Return_36(o2, i2, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_39(o2, i2, env, static) :|: 0 < o2
langle_clinit_rangle_FieldAccess_39(o2, i2, env, static) -{1,1}> langle_clinit_rangle_Return_40(i2, env, static') :|: 0 < o2 && 0 <= o2 && 0 <= static && static' <= static + o2
langle_clinit_rangle_Return_40(i2, env, static) -{1,1}> main_Load_41(i2, env, static) :|: 0 >= 0
main_Load_41(i2, env, static) -{0,0}> main_Load_42(i2, env, static) :|: 0 >= 0
main_Load_42(i2, env, static) -{0,0}> main_Load_44(i2, env, static) :|: 0 <= static
main_Load_44(i2, env, static) -{0,0}> main_Load_45(i2, env, static) :|: 0 >= 0
main_Load_45(i2, env, static) -{0,0}> main_Load_48(i2, env, static) :|: 0 >= 0
main_Load_48(i2, env, static) -{1,1}> main_LT_52(i2, env, static) :|: 0 >= 0

obtained
main_LT_52(i10, env, static) -{1,1}> main_Load_308(i10, i10, env, static) :|: 0 <= i10
by chaining
main_LT_52(i10, env, static) -{0,0}> main_LT_54(i10, env, static) :|: 0 <= i10
main_LT_54(i10, env, static) -{1,1}> main_Load_56(i10, env, static) :|: 0 <= i10
main_Load_56(i10, env, static) -{0,0}> main_Load_308(i10, i10, env, static) :|: 0 <= i10

obtained
main_Load_308(i10, i72, env, static) -{6,6}> main_Load_413(i10, i74', 1, env, static) :|: i72 + 1 = i74' && 1 <= 4 && 0 <= i72 && 0 <= i10 && 1 <= 1 && 1 <= i74' && 1 <= 3
by chaining
main_Load_308(i10, i72, env, static) -{1,1}> main_ConstantStackPush_309(i10, i72, env, static) :|: 0 <= i10 && 0 <= i72
main_ConstantStackPush_309(i10, i72, env, static) -{1,1}> main_IntArithmetic_310(i10, i72, iconst_1, env, static) :|: 0 <= i10 && iconst_1 = 1 && 0 <= i72
main_IntArithmetic_310(i10, i72, iconst_1, env, static) -{1,1}> main_Store_311(i10, i74, env, static) :|: 0 <= i10 && 1 <= i74 && i72 + iconst_1 = i74 && iconst_1 = 1 && 0 <= i72
main_Store_311(i10, i74, env, static) -{1,1}> main_ConstantStackPush_313(i10, i74, env, static) :|: 0 <= i10 && 1 <= i74
main_ConstantStackPush_313(i10, i74, env, static) -{1,1}> main_Store_314(i10, iconst_1, i74, env, static) :|: 0 <= i10 && 1 <= i74 && iconst_1 = 1
main_Store_314(i10, iconst_1, i74, env, static) -{1,1}> main_Load_316(i10, i74, iconst_1, env, static) :|: 0 <= i10 && 1 <= i74 && iconst_1 = 1
main_Load_316(i10, i74, iconst_1, env, static) -{0,0}> main_Load_361(i10, i74, iconst_1, env, static) :|: 0 <= i10 && 1 <= iconst_1 && 1 <= i74 && iconst_1 = 1 && iconst_1 <= 3
main_Load_361(i10, i82, i83, env, static) -{0,0}> main_Load_393(i10, i82, i83, env, static) :|: 0 <= i10 && 1 <= i83 && i83 <= 3 && i83 <= 4
main_Load_393(i10, i92, i93, env, static) -{0,0}> main_Load_413(i10, i92, i93, env, static) :|: 0 <= i10 && 1 <= i93 && i93 <= 4

obtained
main_Load_413(i10, i100, i101, env, static) -{2,2}> main_LT_420(i10, i100, i101, env, static) :|: 0 <= i10 && 1 <= i101
by chaining
main_Load_413(i10, i100, i101, env, static) -{1,1}> main_Load_414(i10, i100, i101, env, static) :|: 0 <= i10 && 1 <= i101
main_Load_414(i10, i100, i101, env, static) -{1,1}> main_LT_420(i10, i100, i101, env, static) :|: 0 <= i10 && 1 <= i101

obtained
main_LT_420(i10, i100, i101, env, static) -{3,3}> main_Load_413(i10, i100, i105', env, static) :|: i101 + 1 = i105' && 1 <= i105' && 1 <= i101 && 1 <= i100 && i101 <= i100 && 0 <= i10 && 2 <= i105'
by chaining
main_LT_420(i10, i100, i101, env, static) -{0,0}> main_LT_428(i10, i100, i101, env, static) :|: 0 <= i10 && 1 <= i101 && i101 <= i100
main_LT_428(i10, i100, i101, env, static) -{1,1}> main_Inc_431(i10, i100, i101, env, static) :|: 0 <= i10 && 1 <= i101 && 1 <= i100 && i101 <= i100
main_Inc_431(i10, i100, i101, env, static) -{1,1}> main_JMP_436(i10, i100, i105, env, static) :|: 0 <= i10 && 1 <= i101 && 2 <= i105 && 1 <= i100 && i101 + 1 = i105
main_JMP_436(i10, i100, i105, env, static) -{1,1}> main_Load_442(i10, i100, i105, env, static) :|: 0 <= i10 && 2 <= i105 && 1 <= i100
main_Load_442(i10, i100, i105, env, static) -{0,0}> main_Load_413(i10, i100, i105, env, static) :|: 0 <= i10 && 2 <= i105 && 1 <= i100 && 1 <= i105

obtained
main_LT_420(i10, i100, i101, env, static) -{7,7}> main_LT_447(i10, i108', env, static) :|: 0 <= i10 && 1 <= i101 && i100 < i101 && i100 - 2 = i108'
by chaining
main_LT_420(i10, i100, i101, env, static) -{0,0}> main_LT_427(i10, i100, i101, env, static) :|: 0 <= i10 && i100 < i101 && 1 <= i101
main_LT_427(i10, i100, i101, env, static) -{1,1}> main_Load_429(i10, i100, env, static) :|: 0 <= i10 && i100 < i101 && 1 <= i101
main_Load_429(i10, i100, env, static) -{1,1}> main_ConstantStackPush_433(i10, i100, env, static) :|: 0 <= i10
main_ConstantStackPush_433(i10, i100, env, static) -{1,1}> main_IntArithmetic_438(i10, i100, iconst_2, env, static) :|: 0 <= i10 && iconst_2 = 2
main_IntArithmetic_438(i10, i100, iconst_2, env, static) -{1,1}> main_Store_444(i10, i108, env, static) :|: 0 <= i10 && iconst_2 = 2 && i100 - iconst_2 = i108
main_Store_444(i10, i108, env, static) -{1,1}> main_JMP_445(i10, i108, env, static) :|: 0 <= i10
main_JMP_445(i10, i108, env, static) -{1,1}> main_Load_446(i10, i108, env, static) :|: 0 <= i10
main_Load_446(i10, i108, env, static) -{1,1}> main_LT_447(i10, i108, env, static) :|: 0 <= i10

obtained
main_LT_447(i10, i118, env, static) -{1,1}> main_Load_308(i10, i118, env, static) :|: 0 <= i10 && 0 <= i118
by chaining
main_LT_447(i10, i118, env, static) -{0,0}> main_LT_450(i10, i118, env, static) :|: 0 <= i10 && 0 <= i118
main_LT_450(i10, i118, env, static) -{1,1}> main_Load_457(i10, i118, env, static) :|: 0 <= i10 && 0 <= i118
main_Load_457(i10, i118, env, static) -{0,0}> main_Load_308(i10, i118, env, static) :|: 0 <= i10 && 0 <= i118

(8) Obligation:

IntTrs with 9 rules
Start term: main_Load_2(#0, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_Load_2(i2, env, static) -{16,16}> main_LT_52(i2, 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_LT_52(i9, env, static) -{0,0}> main_LT_53(i9, env, static) :|: i9 <= -1
main_LT_52(i10, env, static) -{1,1}> main_Load_308(i10, i10, env, static) :|: 0 <= i10
main_Load_308(i10, i72, env, static) -{6,6}> main_Load_413(i10, i74', 1, env, static) :|: i72 + 1 = i74' && 1 <= 4 && 0 <= i72 && 0 <= i10 && 1 <= 1 && 1 <= i74' && 1 <= 3
main_Load_413(i10, i100, i101, env, static) -{2,2}> main_LT_420(i10, i100, i101, env, static) :|: 0 <= i10 && 1 <= i101
main_LT_420(i10, i100, i101, env, static) -{3,3}> main_Load_413(i10, i100, i105', env, static) :|: i101 + 1 = i105' && 1 <= i105' && 1 <= i101 && 1 <= i100 && i101 <= i100 && 0 <= i10 && 2 <= i105'
main_LT_420(i10, i100, i101, env, static) -{7,7}> main_LT_447(i10, i108', env, static) :|: 0 <= i10 && 1 <= i101 && i100 < i101 && i100 - 2 = i108'
main_LT_447(i10, i117, env, static) -{0,0}> main_LT_449(i10, i117, env, static) :|: 0 <= i10 && i117 <= -1
main_LT_447(i10, i118, env, static) -{1,1}> main_Load_308(i10, i118, env, static) :|: 0 <= i10 && 0 <= i118

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

Moved arithmethic from constraints to rhss.

main_LT_420(i10, i100, i101, env, static) -{7,7}> main_LT_447(i10, i108', env, static) :|: 0 <= i10 && 1 <= i101 && i100 < i101 && i100 - 2 = i108'
was transformed to
main_LT_420(i10, i100, i101, env, static) -{7,7}> main_LT_447(i10, i100 - 2, env, static) :|: 0 <= i10 && 1 <= i101 && i100 < i101 && i100 - 2 = i108'

main_LT_420(i10, i100, i101, env, static) -{3,3}> main_Load_413(i10, i100, i105', env, static) :|: i101 + 1 = i105' && 1 <= i105' && 1 <= i101 && 1 <= i100 && i101 <= i100 && 0 <= i10 && 2 <= i105'
was transformed to
main_LT_420(i10, i100, i101, env, static) -{3,3}> main_Load_413(i10, i100, i101 + 1, env, static) :|: i101 + 1 = i105' && 1 <= i105' && 1 <= i101 && 1 <= i100 && i101 <= i100 && 0 <= i10 && 2 <= i105'

main_Load_308(i10, i72, env, static) -{6,6}> main_Load_413(i10, i74', 1, env, static) :|: i72 + 1 = i74' && 1 <= 4 && 0 <= i72 && 0 <= i10 && 1 <= 1 && 1 <= i74' && 1 <= 3
was transformed to
main_Load_308(i10, i72, env, static) -{6,6}> main_Load_413(i10, i72 + 1, 1, env, static) :|: i72 + 1 = i74' && 1 <= 4 && 0 <= i72 && 0 <= i10 && 1 <= 1 && 1 <= i74' && 1 <= 3

(10) Obligation:

IntTrs with 9 rules
Start term: main_Load_2(#0, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_LT_420(i10, i100, i101, env, static) -{7,7}> main_LT_447(i10, i100 - 2, env, static) :|: 0 <= i10 && 1 <= i101 && i100 < i101 && i100 - 2 = i108'
main_Load_413(i10, i100, i101, env, static) -{2,2}> main_LT_420(i10, i100, i101, env, static) :|: 0 <= i10 && 1 <= i101
main_LT_447(i10, i117, env, static) -{0,0}> main_LT_449(i10, i117, env, static) :|: 0 <= i10 && i117 <= -1
main_Load_2(i2, env, static) -{16,16}> main_LT_52(i2, 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_LT_447(i10, i118, env, static) -{1,1}> main_Load_308(i10, i118, env, static) :|: 0 <= i10 && 0 <= i118
main_LT_420(i10, i100, i101, env, static) -{3,3}> main_Load_413(i10, i100, i101 + 1, env, static) :|: i101 + 1 = i105' && 1 <= i105' && 1 <= i101 && 1 <= i100 && i101 <= i100 && 0 <= i10 && 2 <= i105'
main_Load_308(i10, i72, env, static) -{6,6}> main_Load_413(i10, i72 + 1, 1, env, static) :|: i72 + 1 = i74' && 1 <= 4 && 0 <= i72 && 0 <= i10 && 1 <= 1 && 1 <= i74' && 1 <= 3
main_LT_52(i9, env, static) -{0,0}> main_LT_53(i9, env, static) :|: i9 <= -1
main_LT_52(i10, env, static) -{1,1}> main_Load_308(i10, i10, env, static) :|: 0 <= i10

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

Simplified expressions.

main_Load_2(i2, env, static) -{16,16}> main_LT_52(i2, 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_2(i2, env, static) -{16,16}> main_LT_52(i2, env, static'1) :|: static'1 <= static''' + 1 && 0 <= static''' && static''' <= static + 2 && 0 <= static && 0 <= static'1

main_Load_308(i10, i72, env, static) -{6,6}> main_Load_413(i10, i72 + 1, 1, env, static) :|: i72 + 1 = i74' && 1 <= 4 && 0 <= i72 && 0 <= i10 && 1 <= 1 && 1 <= i74' && 1 <= 3
was transformed to
main_Load_308(i10, i72, env, static) -{6,6}> main_Load_413(i10, i72 + 1, 1, env, static) :|: i72 + 1 = i74' && 0 <= i72 && 0 <= i10 && 1 <= i74'

(12) Obligation:

IntTrs with 9 rules
Start term: main_Load_2(#0, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_Load_308(i10, i72, env, static) -{6,6}> main_Load_413(i10, i72 + 1, 1, env, static) :|: i72 + 1 = i74' && 0 <= i72 && 0 <= i10 && 1 <= i74'
main_LT_420(i10, i100, i101, env, static) -{3,3}> main_Load_413(i10, i100, i101 + 1, env, static) :|: i101 + 1 = i105' && 1 <= i105' && 1 <= i101 && 1 <= i100 && i101 <= i100 && 0 <= i10 && 2 <= i105'
main_Load_413(i10, i100, i101, env, static) -{2,2}> main_LT_420(i10, i100, i101, env, static) :|: 0 <= i10 && 1 <= i101
main_LT_447(i10, i117, env, static) -{0,0}> main_LT_449(i10, i117, env, static) :|: 0 <= i10 && i117 <= -1
main_Load_2(i2, env, static) -{16,16}> main_LT_52(i2, env, static'1) :|: static'1 <= static''' + 1 && 0 <= static''' && static''' <= static + 2 && 0 <= static && 0 <= static'1
main_LT_447(i10, i118, env, static) -{1,1}> main_Load_308(i10, i118, env, static) :|: 0 <= i10 && 0 <= i118
main_LT_420(i10, i100, i101, env, static) -{7,7}> main_LT_447(i10, i100 - 2, env, static) :|: 0 <= i10 && 1 <= i101 && i100 < i101 && i100 - 2 = i108'
main_LT_52(i9, env, static) -{0,0}> main_LT_53(i9, env, static) :|: i9 <= -1
main_LT_52(i10, env, static) -{1,1}> main_Load_308(i10, i10, env, static) :|: 0 <= i10

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

Transformed 56 jbc graph edges to a weighted ITS with 56 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) TerminationGraphToComplexityProof (BOTH CONCRETE BOUNDS(ID, ADD(4)) transformation)

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

(22) Obligation:

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

Used field analysis yielded the following read fields:

Considered paths: all paths from start

(23) 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.
Filtered fields of type java.lang.Object.
Did no encode lower bounds for putfield and astore.

(24) Obligation:

IntTrs with 54 rules
Start term: main_Load_2(#0, env, static)
Considered paths: all paths from start
Rules:
main_Load_2(i2, env, static) -{0,0}> main_Load_4(i2, env, static) :|: 0 >= 0
main_Load_4(i2, env, static) -{0,0}> langle_clinit_rangle_ConstantStackPush_6(i2, env, static) :|: 0 >= 0
langle_clinit_rangle_ConstantStackPush_6(i2, env, static) -{1,1}> langle_clinit_rangle_ArrayCreate_12(iconst_0, i2, env, static) :|: iconst_0 = 0
langle_clinit_rangle_ArrayCreate_12(iconst_0, i2, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_14(a2, i2, iconst_0, env, static) :|: a2 = 2 && iconst_0 = 0 && 0 < a2
langle_clinit_rangle_FieldAccess_14(a2, i2, iconst_0, env, static) -{1,1}> langle_clinit_rangle_New_16(i2, env, static') :|: 0 <= a2 && iconst_0 = 0 && static' <= static + a2 && 0 <= static && 0 < a2
langle_clinit_rangle_New_16(i2, env, static) -{0,0}> langle_clinit_rangle_New_17(i2, env, static) :|: 0 >= 0
langle_clinit_rangle_New_17(i2, env, static) -{0,0}> langle_clinit_rangle_New_19(i2, env, static) :|: 0 <= static
langle_clinit_rangle_New_19(i2, env, static) -{1,1}> langle_clinit_rangle_Duplicate_20(o2, i2, env, static) :|: 0 < o2 && o2 = 1
langle_clinit_rangle_Duplicate_20(o2, i2, env, static) -{1,1}> langle_clinit_rangle_ConstantStackPush_22(o2, i2, env, static) :|: 0 < o2
langle_clinit_rangle_ConstantStackPush_22(o2, i2, env, static) -{1,1}> langle_clinit_rangle_InvokeMethod_23(o2, NULL, i2, env, static) :|: NULL = 0 && 0 < o2
langle_clinit_rangle_InvokeMethod_23(o2, NULL, i2, env, static) -{1,1}> langle_init_rangle_Load_25(o2, i2, env, static) :|: NULL = 0 && 0 < o2
langle_init_rangle_Load_25(o2, i2, env, static) -{1,1}> langle_init_rangle_InvokeMethod_27(o2, i2, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_27(o2, i2, env, static) -{1,1}> langle_init_rangle_Load_29(o2, i2, env, static) :|: 0 < o2
langle_init_rangle_Load_29(o2, i2, env, static) -{1,1}> langle_init_rangle_InvokeMethod_31(o2, i2, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_31(o2, i2, env, static) -{1,1}> langle_init_rangle_Return_34(o2, i2, env, static) :|: 0 < o2
langle_init_rangle_Return_34(o2, i2, env, static) -{1,1}> langle_init_rangle_Return_36(o2, i2, env, static) :|: 0 < o2
langle_init_rangle_Return_36(o2, i2, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_39(o2, i2, env, static) :|: 0 < o2
langle_clinit_rangle_FieldAccess_39(o2, i2, env, static) -{1,1}> langle_clinit_rangle_Return_40(i2, env, static') :|: 0 < o2 && 0 <= o2 && 0 <= static && static' <= static + o2
langle_clinit_rangle_Return_40(i2, env, static) -{1,1}> main_Load_41(i2, env, static) :|: 0 >= 0
main_Load_41(i2, env, static) -{0,0}> main_Load_42(i2, env, static) :|: 0 >= 0
main_Load_42(i2, env, static) -{0,0}> main_Load_44(i2, env, static) :|: 0 <= static
main_Load_44(i2, env, static) -{0,0}> main_Load_45(i2, env, static) :|: 0 >= 0
main_Load_45(i2, env, static) -{0,0}> main_Load_48(i2, env, static) :|: 0 >= 0
main_Load_48(i2, env, static) -{1,1}> main_LT_52(i2, env, static) :|: 0 >= 0
main_LT_52(i10, env, static) -{0,0}> main_LT_54(i10, env, static) :|: 0 <= i10
main_LT_54(i10, env, static) -{1,1}> main_Load_56(i10, env, static) :|: 0 <= i10
main_Load_56(i10, env, static) -{0,0}> main_Load_308(i10, i10, env, static) :|: 0 <= i10
main_Load_308(i10, i72, env, static) -{1,1}> main_ConstantStackPush_309(i10, i72, env, static) :|: 0 <= i10 && 0 <= i72
main_ConstantStackPush_309(i10, i72, env, static) -{1,1}> main_IntArithmetic_310(i10, i72, iconst_1, env, static) :|: 0 <= i10 && iconst_1 = 1 && 0 <= i72
main_IntArithmetic_310(i10, i72, iconst_1, env, static) -{1,1}> main_Store_311(i10, i74, env, static) :|: 0 <= i10 && 1 <= i74 && i72 + iconst_1 = i74 && iconst_1 = 1 && 0 <= i72
main_Store_311(i10, i74, env, static) -{1,1}> main_ConstantStackPush_313(i10, i74, env, static) :|: 0 <= i10 && 1 <= i74
main_ConstantStackPush_313(i10, i74, env, static) -{1,1}> main_Store_314(i10, iconst_1, i74, env, static) :|: 0 <= i10 && 1 <= i74 && iconst_1 = 1
main_Store_314(i10, iconst_1, i74, env, static) -{1,1}> main_Load_316(i10, i74, iconst_1, env, static) :|: 0 <= i10 && 1 <= i74 && iconst_1 = 1
main_Load_316(i10, i74, iconst_1, env, static) -{0,0}> main_Load_361(i10, i74, iconst_1, env, static) :|: 0 <= i10 && 1 <= iconst_1 && 1 <= i74 && iconst_1 = 1 && iconst_1 <= 3
main_Load_361(i10, i82, i83, env, static) -{0,0}> main_Load_393(i10, i82, i83, env, static) :|: 0 <= i10 && 1 <= i83 && i83 <= 3 && i83 <= 4
main_Load_393(i10, i92, i93, env, static) -{0,0}> main_Load_413(i10, i92, i93, env, static) :|: 0 <= i10 && 1 <= i93 && i93 <= 4
main_Load_413(i10, i100, i101, env, static) -{1,1}> main_Load_414(i10, i100, i101, env, static) :|: 0 <= i10 && 1 <= i101
main_Load_414(i10, i100, i101, env, static) -{1,1}> main_LT_420(i10, i100, i101, env, static) :|: 0 <= i10 && 1 <= i101
main_LT_420(i10, i100, i101, env, static) -{0,0}> main_LT_427(i10, i100, i101, env, static) :|: 0 <= i10 && i100 < i101 && 1 <= i101
main_LT_420(i10, i100, i101, env, static) -{0,0}> main_LT_428(i10, i100, i101, env, static) :|: 0 <= i10 && 1 <= i101 && i101 <= i100
main_LT_427(i10, i100, i101, env, static) -{1,1}> main_Load_429(i10, i100, env, static) :|: 0 <= i10 && i100 < i101 && 1 <= i101
main_LT_428(i10, i100, i101, env, static) -{1,1}> main_Inc_431(i10, i100, i101, env, static) :|: 0 <= i10 && 1 <= i101 && 1 <= i100 && i101 <= i100
main_Load_429(i10, i100, env, static) -{1,1}> main_ConstantStackPush_433(i10, i100, env, static) :|: 0 <= i10
main_Inc_431(i10, i100, i101, env, static) -{1,1}> main_JMP_436(i10, i100, i105, env, static) :|: 0 <= i10 && 1 <= i101 && 2 <= i105 && 1 <= i100 && i101 + 1 = i105
main_ConstantStackPush_433(i10, i100, env, static) -{1,1}> main_IntArithmetic_438(i10, i100, iconst_2, env, static) :|: 0 <= i10 && iconst_2 = 2
main_JMP_436(i10, i100, i105, env, static) -{1,1}> main_Load_442(i10, i100, i105, env, static) :|: 0 <= i10 && 2 <= i105 && 1 <= i100
main_IntArithmetic_438(i10, i100, iconst_2, env, static) -{1,1}> main_Store_444(i10, i108, env, static) :|: 0 <= i10 && iconst_2 = 2 && i100 - iconst_2 = i108
main_Load_442(i10, i100, i105, env, static) -{0,0}> main_Load_413(i10, i100, i105, env, static) :|: 0 <= i10 && 2 <= i105 && 1 <= i100 && 1 <= i105
main_Store_444(i10, i108, env, static) -{1,1}> main_JMP_445(i10, i108, env, static) :|: 0 <= i10
main_JMP_445(i10, i108, env, static) -{1,1}> main_Load_446(i10, i108, env, static) :|: 0 <= i10
main_Load_446(i10, i108, env, static) -{1,1}> main_LT_447(i10, i108, env, static) :|: 0 <= i10
main_LT_447(i10, i118, env, static) -{0,0}> main_LT_450(i10, i118, env, static) :|: 0 <= i10 && 0 <= i118
main_LT_450(i10, i118, env, static) -{1,1}> main_Load_457(i10, i118, env, static) :|: 0 <= i10 && 0 <= i118
main_Load_457(i10, i118, env, static) -{0,0}> main_Load_308(i10, i118, env, static) :|: 0 <= i10 && 0 <= i118

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

obtained
main_Load_2(i2, env, static) -{17,17}> main_Load_308(i2, i2, env, static'1) :|: 0 <= i2 && 0 < 2 && 0 <= static'1 && 0 <= static && 0 <= 1 && 0 < 1 && static''' <= static + 2 && 0 <= static''' && 0 <= 2 && 0 >= 0 && static'1 <= static''' + 1
by chaining
main_Load_2(i2, env, static) -{0,0}> main_Load_4(i2, env, static) :|: 0 >= 0
main_Load_4(i2, env, static) -{0,0}> langle_clinit_rangle_ConstantStackPush_6(i2, env, static) :|: 0 >= 0
langle_clinit_rangle_ConstantStackPush_6(i2, env, static) -{1,1}> langle_clinit_rangle_ArrayCreate_12(iconst_0, i2, env, static) :|: iconst_0 = 0
langle_clinit_rangle_ArrayCreate_12(iconst_0, i2, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_14(a2, i2, iconst_0, env, static) :|: a2 = 2 && iconst_0 = 0 && 0 < a2
langle_clinit_rangle_FieldAccess_14(a2, i2, iconst_0, env, static) -{1,1}> langle_clinit_rangle_New_16(i2, env, static') :|: 0 <= a2 && iconst_0 = 0 && static' <= static + a2 && 0 <= static && 0 < a2
langle_clinit_rangle_New_16(i2, env, static) -{0,0}> langle_clinit_rangle_New_17(i2, env, static) :|: 0 >= 0
langle_clinit_rangle_New_17(i2, env, static) -{0,0}> langle_clinit_rangle_New_19(i2, env, static) :|: 0 <= static
langle_clinit_rangle_New_19(i2, env, static) -{1,1}> langle_clinit_rangle_Duplicate_20(o2, i2, env, static) :|: 0 < o2 && o2 = 1
langle_clinit_rangle_Duplicate_20(o2, i2, env, static) -{1,1}> langle_clinit_rangle_ConstantStackPush_22(o2, i2, env, static) :|: 0 < o2
langle_clinit_rangle_ConstantStackPush_22(o2, i2, env, static) -{1,1}> langle_clinit_rangle_InvokeMethod_23(o2, NULL, i2, env, static) :|: NULL = 0 && 0 < o2
langle_clinit_rangle_InvokeMethod_23(o2, NULL, i2, env, static) -{1,1}> langle_init_rangle_Load_25(o2, i2, env, static) :|: NULL = 0 && 0 < o2
langle_init_rangle_Load_25(o2, i2, env, static) -{1,1}> langle_init_rangle_InvokeMethod_27(o2, i2, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_27(o2, i2, env, static) -{1,1}> langle_init_rangle_Load_29(o2, i2, env, static) :|: 0 < o2
langle_init_rangle_Load_29(o2, i2, env, static) -{1,1}> langle_init_rangle_InvokeMethod_31(o2, i2, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_31(o2, i2, env, static) -{1,1}> langle_init_rangle_Return_34(o2, i2, env, static) :|: 0 < o2
langle_init_rangle_Return_34(o2, i2, env, static) -{1,1}> langle_init_rangle_Return_36(o2, i2, env, static) :|: 0 < o2
langle_init_rangle_Return_36(o2, i2, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_39(o2, i2, env, static) :|: 0 < o2
langle_clinit_rangle_FieldAccess_39(o2, i2, env, static) -{1,1}> langle_clinit_rangle_Return_40(i2, env, static') :|: 0 < o2 && 0 <= o2 && 0 <= static && static' <= static + o2
langle_clinit_rangle_Return_40(i2, env, static) -{1,1}> main_Load_41(i2, env, static) :|: 0 >= 0
main_Load_41(i2, env, static) -{0,0}> main_Load_42(i2, env, static) :|: 0 >= 0
main_Load_42(i2, env, static) -{0,0}> main_Load_44(i2, env, static) :|: 0 <= static
main_Load_44(i2, env, static) -{0,0}> main_Load_45(i2, env, static) :|: 0 >= 0
main_Load_45(i2, env, static) -{0,0}> main_Load_48(i2, env, static) :|: 0 >= 0
main_Load_48(i2, env, static) -{1,1}> main_LT_52(i2, env, static) :|: 0 >= 0
main_LT_52(i10, env, static) -{0,0}> main_LT_54(i10, env, static) :|: 0 <= i10
main_LT_54(i10, env, static) -{1,1}> main_Load_56(i10, env, static) :|: 0 <= i10
main_Load_56(i10, env, static) -{0,0}> main_Load_308(i10, i10, env, static) :|: 0 <= i10

obtained
main_LT_420(i10, i100, i101, env, static) -{8,8}> main_Load_308(i10, i108', env, static) :|: i100 - 2 = i108' && 0 <= i10 && 0 <= i108' && i100 < i101 && 1 <= i101
by chaining
main_LT_420(i10, i100, i101, env, static) -{0,0}> main_LT_427(i10, i100, i101, env, static) :|: 0 <= i10 && i100 < i101 && 1 <= i101
main_LT_427(i10, i100, i101, env, static) -{1,1}> main_Load_429(i10, i100, env, static) :|: 0 <= i10 && i100 < i101 && 1 <= i101
main_Load_429(i10, i100, env, static) -{1,1}> main_ConstantStackPush_433(i10, i100, env, static) :|: 0 <= i10
main_ConstantStackPush_433(i10, i100, env, static) -{1,1}> main_IntArithmetic_438(i10, i100, iconst_2, env, static) :|: 0 <= i10 && iconst_2 = 2
main_IntArithmetic_438(i10, i100, iconst_2, env, static) -{1,1}> main_Store_444(i10, i108, env, static) :|: 0 <= i10 && iconst_2 = 2 && i100 - iconst_2 = i108
main_Store_444(i10, i108, env, static) -{1,1}> main_JMP_445(i10, i108, env, static) :|: 0 <= i10
main_JMP_445(i10, i108, env, static) -{1,1}> main_Load_446(i10, i108, env, static) :|: 0 <= i10
main_Load_446(i10, i108, env, static) -{1,1}> main_LT_447(i10, i108, env, static) :|: 0 <= i10
main_LT_447(i10, i118, env, static) -{0,0}> main_LT_450(i10, i118, env, static) :|: 0 <= i10 && 0 <= i118
main_LT_450(i10, i118, env, static) -{1,1}> main_Load_457(i10, i118, env, static) :|: 0 <= i10 && 0 <= i118
main_Load_457(i10, i118, env, static) -{0,0}> main_Load_308(i10, i118, env, static) :|: 0 <= i10 && 0 <= i118

(26) Obligation:

IntTrs with 5 rules
Start term: main_Load_2(#0, env, static)
Considered paths: all paths from start
Rules:
main_Load_2(i2, env, static) -{17,17}> main_Load_308(i2, i2, env, static'1) :|: 0 <= i2 && 0 < 2 && 0 <= static'1 && 0 <= static && 0 <= 1 && 0 < 1 && static''' <= static + 2 && 0 <= static''' && 0 <= 2 && 0 >= 0 && static'1 <= static''' + 1
main_Load_308(i10, i72, env, static) -{6,6}> main_Load_413(i10, i74', 1, env, static) :|: i72 + 1 = i74' && 1 <= 4 && 0 <= i72 && 0 <= i10 && 1 <= 1 && 1 <= i74' && 1 <= 3
main_Load_413(i10, i100, i101, env, static) -{2,2}> main_LT_420(i10, i100, i101, env, static) :|: 0 <= i10 && 1 <= i101
main_LT_420(i10, i100, i101, env, static) -{3,3}> main_Load_413(i10, i100, i105', env, static) :|: i101 + 1 = i105' && 1 <= i105' && 1 <= i101 && 1 <= i100 && i101 <= i100 && 0 <= i10 && 2 <= i105'
main_LT_420(i10, i100, i101, env, static) -{8,8}> main_Load_308(i10, i108', env, static) :|: i100 - 2 = i108' && 0 <= i10 && 0 <= i108' && i100 < i101 && 1 <= i101

(27) 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_2(x1, x2, x3) → main_Load_2(x1, x3)
main_Load_308(x1, x2, x3, x4) → main_Load_308(x1, x2)
main_Load_413(x1, x2, x3, x4, x5) → main_Load_413(x1, x2, x3)
main_LT_420(x1, x2, x3, x4, x5) → main_LT_420(x1, x2, x3)

(28) Obligation:

IntTrs with 5 rules
Start term: main_Load_2(#0, static)
Considered paths: all paths from start
Rules:
main_Load_2(i2, static) -{17,17}> main_Load_308(i2, i2) :|: 0 <= i2 && 0 < 2 && 0 <= static'1 && 0 <= static && 0 <= 1 && 0 < 1 && static''' <= static + 2 && 0 <= static''' && 0 <= 2 && 0 >= 0 && static'1 <= static''' + 1
main_Load_308(i10, i72) -{6,6}> main_Load_413(i10, i74', 1) :|: i72 + 1 = i74' && 1 <= 4 && 0 <= i72 && 0 <= i10 && 1 <= 1 && 1 <= i74' && 1 <= 3
main_Load_413(i10, i100, i101) -{2,2}> main_LT_420(i10, i100, i101) :|: 0 <= i10 && 1 <= i101
main_LT_420(i10, i100, i101) -{3,3}> main_Load_413(i10, i100, i105') :|: i101 + 1 = i105' && 1 <= i105' && 1 <= i101 && 1 <= i100 && i101 <= i100 && 0 <= i10 && 2 <= i105'
main_LT_420(i10, i100, i101) -{8,8}> main_Load_308(i10, i108') :|: i100 - 2 = i108' && 0 <= i10 && 0 <= i108' && i100 < i101 && 1 <= i101

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

Moved arithmethic from constraints to rhss.

main_Load_308(i10, i72) -{6,6}> main_Load_413(i10, i74', 1) :|: i72 + 1 = i74' && 1 <= 4 && 0 <= i72 && 0 <= i10 && 1 <= 1 && 1 <= i74' && 1 <= 3
was transformed to
main_Load_308(i10, i72) -{6,6}> main_Load_413(i10, i72 + 1, 1) :|: i72 + 1 = i74' && 1 <= 4 && 0 <= i72 && 0 <= i10 && 1 <= 1 && 1 <= i74' && 1 <= 3

main_LT_420(i10, i100, i101) -{3,3}> main_Load_413(i10, i100, i105') :|: i101 + 1 = i105' && 1 <= i105' && 1 <= i101 && 1 <= i100 && i101 <= i100 && 0 <= i10 && 2 <= i105'
was transformed to
main_LT_420(i10, i100, i101) -{3,3}> main_Load_413(i10, i100, i101 + 1) :|: i101 + 1 = i105' && 1 <= i105' && 1 <= i101 && 1 <= i100 && i101 <= i100 && 0 <= i10 && 2 <= i105'

main_LT_420(i10, i100, i101) -{8,8}> main_Load_308(i10, i108') :|: i100 - 2 = i108' && 0 <= i10 && 0 <= i108' && i100 < i101 && 1 <= i101
was transformed to
main_LT_420(i10, i100, i101) -{8,8}> main_Load_308(i10, i100 - 2) :|: i100 - 2 = i108' && 0 <= i10 && 0 <= i108' && i100 < i101 && 1 <= i101

(30) Obligation:

IntTrs with 5 rules
Start term: main_Load_2(#0, static)
Considered paths: all paths from start
Rules:
main_Load_308(i10, i72) -{6,6}> main_Load_413(i10, i72 + 1, 1) :|: i72 + 1 = i74' && 1 <= 4 && 0 <= i72 && 0 <= i10 && 1 <= 1 && 1 <= i74' && 1 <= 3
main_LT_420(i10, i100, i101) -{3,3}> main_Load_413(i10, i100, i101 + 1) :|: i101 + 1 = i105' && 1 <= i105' && 1 <= i101 && 1 <= i100 && i101 <= i100 && 0 <= i10 && 2 <= i105'
main_Load_413(i10, i100, i101) -{2,2}> main_LT_420(i10, i100, i101) :|: 0 <= i10 && 1 <= i101
main_LT_420(i10, i100, i101) -{8,8}> main_Load_308(i10, i100 - 2) :|: i100 - 2 = i108' && 0 <= i10 && 0 <= i108' && i100 < i101 && 1 <= i101
main_Load_2(i2, static) -{17,17}> main_Load_308(i2, i2) :|: 0 <= i2 && 0 < 2 && 0 <= static'1 && 0 <= static && 0 <= 1 && 0 < 1 && static''' <= static + 2 && 0 <= static''' && 0 <= 2 && 0 >= 0 && static'1 <= static''' + 1

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

Simplified expressions.

main_Load_308(i10, i72) -{6,6}> main_Load_413(i10, i72 + 1, 1) :|: i72 + 1 = i74' && 1 <= 4 && 0 <= i72 && 0 <= i10 && 1 <= 1 && 1 <= i74' && 1 <= 3
was transformed to
main_Load_308(i10, i72) -{6,6}> main_Load_413(i10, i72 + 1, 1) :|: i72 + 1 = i74' && 0 <= i72 && 0 <= i10 && 1 <= i74'

main_Load_2(i2, static) -{17,17}> main_Load_308(i2, i2) :|: 0 <= i2 && 0 < 2 && 0 <= static'1 && 0 <= static && 0 <= 1 && 0 < 1 && static''' <= static + 2 && 0 <= static''' && 0 <= 2 && 0 >= 0 && static'1 <= static''' + 1
was transformed to
main_Load_2(i2, static) -{17,17}> main_Load_308(i2, i2) :|: 0 <= i2 && 0 <= static'1 && 0 <= static && static''' <= static + 2 && 0 <= static''' && static'1 <= static''' + 1

(32) Obligation:

IntTrs with 5 rules
Start term: main_Load_2(#0, static)
Considered paths: all paths from start
Rules:
main_LT_420(i10, i100, i101) -{3,3}> main_Load_413(i10, i100, i101 + 1) :|: i101 + 1 = i105' && 1 <= i105' && 1 <= i101 && 1 <= i100 && i101 <= i100 && 0 <= i10 && 2 <= i105'
main_LT_420(i10, i100, i101) -{8,8}> main_Load_308(i10, i100 - 2) :|: i100 - 2 = i108' && 0 <= i10 && 0 <= i108' && i100 < i101 && 1 <= i101
main_Load_413(i10, i100, i101) -{2,2}> main_LT_420(i10, i100, i101) :|: 0 <= i10 && 1 <= i101
main_Load_2(i2, static) -{17,17}> main_Load_308(i2, i2) :|: 0 <= i2 && 0 <= static'1 && 0 <= static && static''' <= static + 2 && 0 <= static''' && static'1 <= static''' + 1
main_Load_308(i10, i72) -{6,6}> main_Load_413(i10, i72 + 1, 1) :|: i72 + 1 = i74' && 0 <= i72 && 0 <= i10 && 1 <= i74'

(33) koat Proof (EQUIVALENT transformation)

YES(?, 30*ar_0^2 + 157*ar_0 + 88)

Initial complexity problem:
1: T:
(Comp: ?, Cost: 3) main_LT_420(ar_0, ar_1, ar_2) -> Com_1(main_Load_413(ar_0, ar_1, ar_2 + 1)) [ ar_2 + 1 = i105' /\ 1 <= i105' /\ 1 <= ar_2 /\ 1 <= ar_1 /\ ar_2 <= ar_1 /\ 0 <= ar_0 /\ 2 <= i105' ]
(Comp: ?, Cost: 8) main_LT_420(ar_0, ar_1, ar_2) -> Com_1(main_Load_308(ar_0, ar_1 - 2, arityPad)) [ ar_1 - 2 = i108' /\ 0 <= ar_0 /\ 0 <= i108' /\ ar_1 < ar_2 /\ 1 <= ar_2 ]
(Comp: ?, Cost: 2) main_Load_413(ar_0, ar_1, ar_2) -> Com_1(main_LT_420(ar_0, ar_1, ar_2)) [ 0 <= ar_0 /\ 1 <= ar_2 ]
(Comp: ?, Cost: 17) main_Load_2(ar_0, ar_1, ar_2) -> Com_1(main_Load_308(ar_0, ar_0, arityPad)) [ 0 <= ar_0 /\ 0 <= static'1 /\ 0 <= ar_1 /\ static''' <= ar_1 + 2 /\ 0 <= static''' /\ static'1 <= static''' + 1 ]
(Comp: ?, Cost: 6) main_Load_308(ar_0, ar_1, ar_2) -> Com_1(main_Load_413(ar_0, ar_1 + 1, 1)) [ ar_1 + 1 = i74' /\ 0 <= ar_1 /\ 0 <= ar_0 /\ 1 <= i74' ]
(Comp: 1, Cost: 0) koat_start(ar_0, ar_1, ar_2) -> Com_1(main_Load_2(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: 3) main_LT_420(ar_0, ar_1, ar_2) -> Com_1(main_Load_413(ar_0, ar_1, ar_2 + 1)) [ ar_2 + 1 = i105' /\ 1 <= i105' /\ 1 <= ar_2 /\ 1 <= ar_1 /\ ar_2 <= ar_1 /\ 0 <= ar_0 /\ 2 <= i105' ]
(Comp: ?, Cost: 8) main_LT_420(ar_0, ar_1, ar_2) -> Com_1(main_Load_308(ar_0, ar_1 - 2, arityPad)) [ ar_1 - 2 = i108' /\ 0 <= ar_0 /\ 0 <= i108' /\ ar_1 < ar_2 /\ 1 <= ar_2 ]
(Comp: ?, Cost: 2) main_Load_413(ar_0, ar_1, ar_2) -> Com_1(main_LT_420(ar_0, ar_1, ar_2)) [ 0 <= ar_0 /\ 1 <= ar_2 ]
(Comp: 1, Cost: 17) main_Load_2(ar_0, ar_1, ar_2) -> Com_1(main_Load_308(ar_0, ar_0, arityPad)) [ 0 <= ar_0 /\ 0 <= static'1 /\ 0 <= ar_1 /\ static''' <= ar_1 + 2 /\ 0 <= static''' /\ static'1 <= static''' + 1 ]
(Comp: ?, Cost: 6) main_Load_308(ar_0, ar_1, ar_2) -> Com_1(main_Load_413(ar_0, ar_1 + 1, 1)) [ ar_1 + 1 = i74' /\ 0 <= ar_1 /\ 0 <= ar_0 /\ 1 <= i74' ]
(Comp: 1, Cost: 0) koat_start(ar_0, ar_1, ar_2) -> Com_1(main_Load_2(ar_0, ar_1, ar_2)) [ 0 <= 0 ]
start location: koat_start
leaf cost: 0

A polynomial rank function with
Pol(main_LT_420) = 2*V_2 - 2
Pol(main_Load_413) = 2*V_2 - 2
Pol(main_Load_308) = 2*V_2 + 1
Pol(main_Load_2) = 2*V_1 + 1
Pol(koat_start) = 2*V_1 + 1
orients all transitions weakly and the transitions
main_Load_308(ar_0, ar_1, ar_2) -> Com_1(main_Load_413(ar_0, ar_1 + 1, 1)) [ ar_1 + 1 = i74' /\ 0 <= ar_1 /\ 0 <= ar_0 /\ 1 <= i74' ]
main_LT_420(ar_0, ar_1, ar_2) -> Com_1(main_Load_308(ar_0, ar_1 - 2, arityPad)) [ ar_1 - 2 = i108' /\ 0 <= ar_0 /\ 0 <= i108' /\ ar_1 < ar_2 /\ 1 <= ar_2 ]
strictly and produces the following problem:
3: T:
(Comp: ?, Cost: 3) main_LT_420(ar_0, ar_1, ar_2) -> Com_1(main_Load_413(ar_0, ar_1, ar_2 + 1)) [ ar_2 + 1 = i105' /\ 1 <= i105' /\ 1 <= ar_2 /\ 1 <= ar_1 /\ ar_2 <= ar_1 /\ 0 <= ar_0 /\ 2 <= i105' ]
(Comp: 2*ar_0 + 1, Cost: 8) main_LT_420(ar_0, ar_1, ar_2) -> Com_1(main_Load_308(ar_0, ar_1 - 2, arityPad)) [ ar_1 - 2 = i108' /\ 0 <= ar_0 /\ 0 <= i108' /\ ar_1 < ar_2 /\ 1 <= ar_2 ]
(Comp: ?, Cost: 2) main_Load_413(ar_0, ar_1, ar_2) -> Com_1(main_LT_420(ar_0, ar_1, ar_2)) [ 0 <= ar_0 /\ 1 <= ar_2 ]
(Comp: 1, Cost: 17) main_Load_2(ar_0, ar_1, ar_2) -> Com_1(main_Load_308(ar_0, ar_0, arityPad)) [ 0 <= ar_0 /\ 0 <= static'1 /\ 0 <= ar_1 /\ static''' <= ar_1 + 2 /\ 0 <= static''' /\ static'1 <= static''' + 1 ]
(Comp: 2*ar_0 + 1, Cost: 6) main_Load_308(ar_0, ar_1, ar_2) -> Com_1(main_Load_413(ar_0, ar_1 + 1, 1)) [ ar_1 + 1 = i74' /\ 0 <= ar_1 /\ 0 <= ar_0 /\ 1 <= i74' ]
(Comp: 1, Cost: 0) koat_start(ar_0, ar_1, ar_2) -> Com_1(main_Load_2(ar_0, ar_1, ar_2)) [ 0 <= 0 ]
start location: koat_start
leaf cost: 0

A polynomial rank function with
Pol(main_Load_413) = V_2 - V_3 + 1
Pol(main_LT_420) = V_2 - V_3 + 1
and size complexities
S("koat_start(ar_0, ar_1, ar_2) -> Com_1(main_Load_2(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_2(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_2(ar_0, ar_1, ar_2)) [ 0 <= 0 ]", 0-2) = ar_2
S("main_Load_308(ar_0, ar_1, ar_2) -> Com_1(main_Load_413(ar_0, ar_1 + 1, 1)) [ ar_1 + 1 = i74' /\\ 0 <= ar_1 /\\ 0 <= ar_0 /\\ 1 <= i74' ]", 0-0) = ar_0
S("main_Load_308(ar_0, ar_1, ar_2) -> Com_1(main_Load_413(ar_0, ar_1 + 1, 1)) [ ar_1 + 1 = i74' /\\ 0 <= ar_1 /\\ 0 <= ar_0 /\\ 1 <= i74' ]", 0-1) = 3*ar_0 + 9
S("main_Load_308(ar_0, ar_1, ar_2) -> Com_1(main_Load_413(ar_0, ar_1 + 1, 1)) [ ar_1 + 1 = i74' /\\ 0 <= ar_1 /\\ 0 <= ar_0 /\\ 1 <= i74' ]", 0-2) = 1
S("main_Load_2(ar_0, ar_1, ar_2) -> Com_1(main_Load_308(ar_0, ar_0, arityPad)) [ 0 <= ar_0 /\\ 0 <= static'1 /\\ 0 <= ar_1 /\\ static''' <= ar_1 + 2 /\\ 0 <= static''' /\\ static'1 <= static''' + 1 ]", 0-0) = ar_0
S("main_Load_2(ar_0, ar_1, ar_2) -> Com_1(main_Load_308(ar_0, ar_0, arityPad)) [ 0 <= ar_0 /\\ 0 <= static'1 /\\ 0 <= ar_1 /\\ static''' <= ar_1 + 2 /\\ 0 <= static''' /\\ static'1 <= static''' + 1 ]", 0-1) = ar_0
S("main_Load_2(ar_0, ar_1, ar_2) -> Com_1(main_Load_308(ar_0, ar_0, arityPad)) [ 0 <= ar_0 /\\ 0 <= static'1 /\\ 0 <= ar_1 /\\ static''' <= ar_1 + 2 /\\ 0 <= static''' /\\ static'1 <= static''' + 1 ]", 0-2) = ?
S("main_Load_413(ar_0, ar_1, ar_2) -> Com_1(main_LT_420(ar_0, ar_1, ar_2)) [ 0 <= ar_0 /\\ 1 <= ar_2 ]", 0-0) = ar_0
S("main_Load_413(ar_0, ar_1, ar_2) -> Com_1(main_LT_420(ar_0, ar_1, ar_2)) [ 0 <= ar_0 /\\ 1 <= ar_2 ]", 0-1) = 3*ar_0 + 9
S("main_Load_413(ar_0, ar_1, ar_2) -> Com_1(main_LT_420(ar_0, ar_1, ar_2)) [ 0 <= ar_0 /\\ 1 <= ar_2 ]", 0-2) = ?
S("main_LT_420(ar_0, ar_1, ar_2) -> Com_1(main_Load_308(ar_0, ar_1 - 2, arityPad)) [ ar_1 - 2 = i108' /\\ 0 <= ar_0 /\\ 0 <= i108' /\\ ar_1 < ar_2 /\\ 1 <= ar_2 ]", 0-0) = ar_0
S("main_LT_420(ar_0, ar_1, ar_2) -> Com_1(main_Load_308(ar_0, ar_1 - 2, arityPad)) [ ar_1 - 2 = i108' /\\ 0 <= ar_0 /\\ 0 <= i108' /\\ ar_1 < ar_2 /\\ 1 <= ar_2 ]", 0-1) = 3*ar_0 + 9
S("main_LT_420(ar_0, ar_1, ar_2) -> Com_1(main_Load_308(ar_0, ar_1 - 2, arityPad)) [ ar_1 - 2 = i108' /\\ 0 <= ar_0 /\\ 0 <= i108' /\\ ar_1 < ar_2 /\\ 1 <= ar_2 ]", 0-2) = ?
S("main_LT_420(ar_0, ar_1, ar_2) -> Com_1(main_Load_413(ar_0, ar_1, ar_2 + 1)) [ ar_2 + 1 = i105' /\\ 1 <= i105' /\\ 1 <= ar_2 /\\ 1 <= ar_1 /\\ ar_2 <= ar_1 /\\ 0 <= ar_0 /\\ 2 <= i105' ]", 0-0) = ar_0
S("main_LT_420(ar_0, ar_1, ar_2) -> Com_1(main_Load_413(ar_0, ar_1, ar_2 + 1)) [ ar_2 + 1 = i105' /\\ 1 <= i105' /\\ 1 <= ar_2 /\\ 1 <= ar_1 /\\ ar_2 <= ar_1 /\\ 0 <= ar_0 /\\ 2 <= i105' ]", 0-1) = 3*ar_0 + 9
S("main_LT_420(ar_0, ar_1, ar_2) -> Com_1(main_Load_413(ar_0, ar_1, ar_2 + 1)) [ ar_2 + 1 = i105' /\\ 1 <= i105' /\\ 1 <= ar_2 /\\ 1 <= ar_1 /\\ ar_2 <= ar_1 /\\ 0 <= ar_0 /\\ 2 <= i105' ]", 0-2) = ?
orients the transitions
main_Load_413(ar_0, ar_1, ar_2) -> Com_1(main_LT_420(ar_0, ar_1, ar_2)) [ 0 <= ar_0 /\ 1 <= ar_2 ]
main_LT_420(ar_0, ar_1, ar_2) -> Com_1(main_Load_413(ar_0, ar_1, ar_2 + 1)) [ ar_2 + 1 = i105' /\ 1 <= i105' /\ 1 <= ar_2 /\ 1 <= ar_1 /\ ar_2 <= ar_1 /\ 0 <= ar_0 /\ 2 <= i105' ]
weakly and the transition
main_LT_420(ar_0, ar_1, ar_2) -> Com_1(main_Load_413(ar_0, ar_1, ar_2 + 1)) [ ar_2 + 1 = i105' /\ 1 <= i105' /\ 1 <= ar_2 /\ 1 <= ar_1 /\ ar_2 <= ar_1 /\ 0 <= ar_0 /\ 2 <= i105' ]
strictly and produces the following problem:
4: T:
(Comp: 6*ar_0^2 + 25*ar_0 + 11, Cost: 3) main_LT_420(ar_0, ar_1, ar_2) -> Com_1(main_Load_413(ar_0, ar_1, ar_2 + 1)) [ ar_2 + 1 = i105' /\ 1 <= i105' /\ 1 <= ar_2 /\ 1 <= ar_1 /\ ar_2 <= ar_1 /\ 0 <= ar_0 /\ 2 <= i105' ]
(Comp: 2*ar_0 + 1, Cost: 8) main_LT_420(ar_0, ar_1, ar_2) -> Com_1(main_Load_308(ar_0, ar_1 - 2, arityPad)) [ ar_1 - 2 = i108' /\ 0 <= ar_0 /\ 0 <= i108' /\ ar_1 < ar_2 /\ 1 <= ar_2 ]
(Comp: ?, Cost: 2) main_Load_413(ar_0, ar_1, ar_2) -> Com_1(main_LT_420(ar_0, ar_1, ar_2)) [ 0 <= ar_0 /\ 1 <= ar_2 ]
(Comp: 1, Cost: 17) main_Load_2(ar_0, ar_1, ar_2) -> Com_1(main_Load_308(ar_0, ar_0, arityPad)) [ 0 <= ar_0 /\ 0 <= static'1 /\ 0 <= ar_1 /\ static''' <= ar_1 + 2 /\ 0 <= static''' /\ static'1 <= static''' + 1 ]
(Comp: 2*ar_0 + 1, Cost: 6) main_Load_308(ar_0, ar_1, ar_2) -> Com_1(main_Load_413(ar_0, ar_1 + 1, 1)) [ ar_1 + 1 = i74' /\ 0 <= ar_1 /\ 0 <= ar_0 /\ 1 <= i74' ]
(Comp: 1, Cost: 0) koat_start(ar_0, ar_1, ar_2) -> Com_1(main_Load_2(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: 6*ar_0^2 + 25*ar_0 + 11, Cost: 3) main_LT_420(ar_0, ar_1, ar_2) -> Com_1(main_Load_413(ar_0, ar_1, ar_2 + 1)) [ ar_2 + 1 = i105' /\ 1 <= i105' /\ 1 <= ar_2 /\ 1 <= ar_1 /\ ar_2 <= ar_1 /\ 0 <= ar_0 /\ 2 <= i105' ]
(Comp: 2*ar_0 + 1, Cost: 8) main_LT_420(ar_0, ar_1, ar_2) -> Com_1(main_Load_308(ar_0, ar_1 - 2, arityPad)) [ ar_1 - 2 = i108' /\ 0 <= ar_0 /\ 0 <= i108' /\ ar_1 < ar_2 /\ 1 <= ar_2 ]
(Comp: 27*ar_0 + 6*ar_0^2 + 12, Cost: 2) main_Load_413(ar_0, ar_1, ar_2) -> Com_1(main_LT_420(ar_0, ar_1, ar_2)) [ 0 <= ar_0 /\ 1 <= ar_2 ]
(Comp: 1, Cost: 17) main_Load_2(ar_0, ar_1, ar_2) -> Com_1(main_Load_308(ar_0, ar_0, arityPad)) [ 0 <= ar_0 /\ 0 <= static'1 /\ 0 <= ar_1 /\ static''' <= ar_1 + 2 /\ 0 <= static''' /\ static'1 <= static''' + 1 ]
(Comp: 2*ar_0 + 1, Cost: 6) main_Load_308(ar_0, ar_1, ar_2) -> Com_1(main_Load_413(ar_0, ar_1 + 1, 1)) [ ar_1 + 1 = i74' /\ 0 <= ar_1 /\ 0 <= ar_0 /\ 1 <= i74' ]
(Comp: 1, Cost: 0) koat_start(ar_0, ar_1, ar_2) -> Com_1(main_Load_2(ar_0, ar_1, ar_2)) [ 0 <= 0 ]
start location: koat_start
leaf cost: 0

Complexity upper bound 30*ar_0^2 + 157*ar_0 + 88

Time: 0.201 sec (SMT: 0.180 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) TerminationGraphToComplexityProof (BOTH CONCRETE BOUNDS(ID, ADD(4)) transformation)

(22) Obligation:

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

(24) Obligation:

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

(26) Obligation:

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

(28) Obligation:

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

(30) Obligation:

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

(32) Obligation:

(33) koat Proof (EQUIVALENT transformation)

(34) BOUNDS(CONSTANT, 88 + 157 * |#0| + 30 * |#0|^2)