time complexity proof of /tmp/tmp5fqJGe/PastaC10.jar

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

0 JBC problem

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

↳2 JBCTerminationGraph

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

↳4 JBCComplexityEdges

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

    ↳6 WeightedIntTrs

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

        ↳8 WeightedIntTrs

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

        ↳10 WeightedIntTrs

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

        ↳12 WeightedIntTrs

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

        ↳14 WeightedIntTrs

    ↳15 JBCGraphEdgesToCpxIntTrsProof (CONCRETE UPPER BOUND(ID), 150 ms)

    ↳16 WeightedIntTrs

        ↳17 StraightLineCodeCompressionProof (BOTH CONCRETE BOUNDS(ID, ID), 24 ms)

        ↳18 WeightedIntTrs

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

        ↳20 WeightedIntTrs

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

        ↳22 WeightedIntTrs

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

        ↳24 WeightedIntTrs

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

↳26 JBCComplexityEdges

    ↳27 JBCGraphEdgesToCpxIntTrsProof (CONCRETE UPPER BOUND(ID), 106 ms)

    ↳28 WeightedIntTrs

    ↳29 StraightLineCodeCompressionProof (BOTH CONCRETE BOUNDS(ID, ID), 30 ms)

    ↳30 WeightedIntTrs

    ↳31 WeightedIntTrsUnneededArgumentFilterProof (CONCRETE UPPER BOUND(ID), 14 ms)

    ↳32 WeightedIntTrs

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

    ↳34 WeightedIntTrs

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

    ↳36 WeightedIntTrs

    ↳37 koat Proof (⇔, 67 ms)

    ↳38 BOUNDS(CONSTANT, 15 + 32 * |#0| + 32 * |#1|)

(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 PastaC10 {
    public static void main(int i, int j) {
        while (i - j >= 1) {
            int rand = new Object().hashCode();
            if (rand < 0) return;
            i = i - rand;
            rand = new Object().hashCode();
            if (rand < 0) return;
            int r = rand + 1;
            j = j + r;
        }
    }
}

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

Constructed TerminationGraph.

(2) Obligation:

Termination Graph based on JBC Program:
PastaC10.main(II)V: Graph of 70 nodes with 1 SCC.

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

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

(4) Obligation:

Set of 64 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 64 jbc graph edges to a weighted ITS with 64 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 64 rules
Start term: main_Load_2(#0, #1, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_Load_2(i1, i4, env, static) -{0,0}> main_Load_4(i1, i4, env, static) :|: 0 >= 0
main_Load_4(i1, i4, env, static) -{0,0}> langle_clinit_rangle_ConstantStackPush_6(i1, i4, env, static) :|: 0 >= 0
langle_clinit_rangle_ConstantStackPush_6(i1, i4, env, static) -{1,1}> langle_clinit_rangle_ArrayCreate_14(iconst_0, i1, i4, env, static) :|: iconst_0 = 0
langle_clinit_rangle_ArrayCreate_14(iconst_0, i1, i4, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_16(a2, i1, i4, iconst_0, env, static) :|: a2 = 2 && iconst_0 = 0 && 0 < a2
langle_clinit_rangle_FieldAccess_16(a2, i1, i4, iconst_0, env, static) -{1,1}> langle_clinit_rangle_New_17(i1, i4, env, static') :|: 0 <= a2 && iconst_0 = 0 && static' <= static + a2 && 0 <= static && 0 < a2
langle_clinit_rangle_New_17(i1, i4, env, static) -{0,0}> langle_clinit_rangle_New_19(i1, i4, env, static) :|: 0 >= 0
langle_clinit_rangle_New_19(i1, i4, env, static) -{0,0}> langle_clinit_rangle_New_20(i1, i4, env, static) :|: 0 <= static
langle_clinit_rangle_New_20(i1, i4, env, static) -{1,1}> langle_clinit_rangle_Duplicate_22(o2, i1, i4, env, static) :|: 0 < o2 && o2 = 1
langle_clinit_rangle_Duplicate_22(o2, i1, i4, env, static) -{1,1}> langle_clinit_rangle_ConstantStackPush_25(o2, i1, i4, env, static) :|: 0 < o2
langle_clinit_rangle_ConstantStackPush_25(o2, i1, i4, env, static) -{1,1}> langle_clinit_rangle_InvokeMethod_27(o2, NULL, i1, i4, env, static) :|: NULL = 0 && 0 < o2
langle_clinit_rangle_InvokeMethod_27(o2, NULL, i1, i4, env, static) -{1,1}> langle_init_rangle_Load_28(o2, i1, i4, env, static) :|: NULL = 0 && 0 < o2
langle_init_rangle_Load_28(o2, i1, i4, env, static) -{1,1}> langle_init_rangle_InvokeMethod_31(o2, i1, i4, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_31(o2, i1, i4, env, static) -{1,1}> langle_init_rangle_Load_33(o2, i1, i4, env, static) :|: 0 < o2
langle_init_rangle_Load_33(o2, i1, i4, env, static) -{1,1}> langle_init_rangle_InvokeMethod_36(o2, i1, i4, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_36(o2, i1, i4, env, static) -{1,1}> langle_init_rangle_Return_39(o2, i1, i4, env, static) :|: 0 < o2
langle_init_rangle_Return_39(o2, i1, i4, env, static) -{1,1}> langle_init_rangle_Return_41(o2, i1, i4, env, static) :|: 0 < o2
langle_init_rangle_Return_41(o2, i1, i4, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_44(o2, i1, i4, env, static) :|: 0 < o2
langle_clinit_rangle_FieldAccess_44(o2, i1, i4, env, static) -{1,1}> langle_clinit_rangle_Return_45(i1, i4, env, static') :|: 0 < o2 && 0 <= o2 && 0 <= static && static' <= static + o2
langle_clinit_rangle_Return_45(i1, i4, env, static) -{1,1}> main_Load_46(i1, i4, env, static) :|: 0 >= 0
main_Load_46(i1, i4, env, static) -{0,0}> main_Load_49(i1, i4, env, static) :|: 0 >= 0
main_Load_49(i1, i4, env, static) -{0,0}> main_Load_50(i1, i4, env, static) :|: 0 <= static
main_Load_50(i1, i4, env, static) -{0,0}> main_Load_51(i1, i4, env, static) :|: 0 >= 0
main_Load_51(i1, i4, env, static) -{0,0}> main_Load_52(i1, i4, env, static) :|: 0 >= 0
main_Load_52(i1, i4, env, static) -{0,0}> main_Load_158(i1, i4, i1, i4, env, static) :|: 0 >= 0
main_Load_158(i1, i4, i25, i38, env, static) -{0,0}> main_Load_274(i1, i4, i25, i38, env, static) :|: 0 >= 0
main_Load_274(i1, i4, i79, i91, env, static) -{1,1}> main_Load_276(i1, i4, i79, i91, env, static) :|: 0 >= 0
main_Load_276(i1, i4, i79, i91, env, static) -{1,1}> main_IntArithmetic_277(i1, i4, i79, i91, env, static) :|: 0 >= 0
main_IntArithmetic_277(i1, i4, i79, i91, env, static) -{1,1}> main_ConstantStackPush_278(i1, i4, i96, i79, i91, env, static) :|: i79 - i91 = i96
main_ConstantStackPush_278(i1, i4, i96, i79, i91, env, static) -{1,1}> main_LT_282(i1, i4, i96, iconst_1, i79, i91, env, static) :|: iconst_1 = 1
main_LT_282(i1, i4, i101, iconst_1, i79, i91, env, static) -{0,0}> main_LT_283(i1, i4, i101, iconst_1, i79, i91, env, static) :|: i101 <= 0 && iconst_1 = 1
main_LT_282(i1, i4, i102, iconst_1, i79, i91, env, static) -{0,0}> main_LT_284(i1, i4, i102, iconst_1, i79, i91, env, static) :|: 1 <= i102 && iconst_1 = 1
main_LT_284(i1, i4, i102, iconst_1, i79, i91, env, static) -{1,1}> main_New_294(i1, i4, i79, i91, env, static) :|: 1 <= i102 && iconst_1 = 1 && iconst_1 <= i102
main_New_294(i1, i4, i79, i91, env, static) -{1,1}> main_Duplicate_299(i1, i4, o16, i79, i91, env, static) :|: o16 = 1 && 0 < o16
main_Duplicate_299(i1, i4, o16, i79, i91, env, static) -{1,1}> main_InvokeMethod_301(i1, i4, o16, i79, i91, env, static) :|: 0 < o16
main_InvokeMethod_301(i1, i4, o16, i79, i91, env, static) -{1,1}> main_InvokeMethod_303(i1, i4, o16, i79, i91, env, static) :|: 0 < o16
main_InvokeMethod_303(i1, i4, o16, i79, i91, env, static) -{1,1}> main_Store_305(i1, i4, i107, i79, i91, env, static) :|: 0 < o16
main_Store_305(i1, i4, i107, i79, i91, env, static) -{1,1}> main_Load_306(i1, i4, i79, i91, i107, env, static) :|: 0 >= 0
main_Load_306(i1, i4, i79, i91, i107, env, static) -{1,1}> main_GE_307(i1, i4, i107, i79, i91, env, static) :|: 0 >= 0
main_GE_307(i1, i4, i112, i79, i91, env, static) -{0,0}> main_GE_308(i1, i4, i112, i79, i91, env, static) :|: i112 <= -1
main_GE_307(i1, i4, i113, i79, i91, env, static) -{0,0}> main_GE_309(i1, i4, i113, i79, i91, env, static) :|: 0 <= i113
main_GE_309(i1, i4, i113, i79, i91, env, static) -{1,1}> main_Load_311(i1, i4, i79, i91, i113, env, static) :|: 0 <= i113
main_Load_311(i1, i4, i79, i91, i113, env, static) -{1,1}> main_Load_313(i1, i4, i79, i91, i113, env, static) :|: 0 <= i113
main_Load_313(i1, i4, i79, i91, i113, env, static) -{1,1}> main_IntArithmetic_315(i1, i4, i79, i113, i91, env, static) :|: 0 <= i113
main_IntArithmetic_315(i1, i4, i79, i113, i91, env, static) -{1,1}> main_Store_317(i1, i4, i114, i91, env, static) :|: 0 <= i113 && i79 - i113 = i114
main_Store_317(i1, i4, i114, i91, env, static) -{1,1}> main_New_318(i1, i4, i114, i91, env, static) :|: 0 >= 0
main_New_318(i1, i4, i114, i91, env, static) -{1,1}> main_Duplicate_325(i1, i4, o18, i114, i91, env, static) :|: o18 = 1 && 0 < o18
main_Duplicate_325(i1, i4, o18, i114, i91, env, static) -{1,1}> main_InvokeMethod_327(i1, i4, o18, i114, i91, env, static) :|: 0 < o18
main_InvokeMethod_327(i1, i4, o18, i114, i91, env, static) -{1,1}> main_InvokeMethod_329(i1, i4, o18, i114, i91, env, static) :|: 0 < o18
main_InvokeMethod_329(i1, i4, o18, i114, i91, env, static) -{1,1}> main_Store_331(i1, i4, i118, i114, i91, env, static) :|: 0 < o18
main_Store_331(i1, i4, i118, i114, i91, env, static) -{1,1}> main_Load_332(i1, i4, i114, i91, i118, env, static) :|: 0 >= 0
main_Load_332(i1, i4, i114, i91, i118, env, static) -{1,1}> main_GE_333(i1, i4, i118, i114, i91, env, static) :|: 0 >= 0
main_GE_333(i1, i4, i123, i114, i91, env, static) -{0,0}> main_GE_334(i1, i4, i123, i114, i91, env, static) :|: i123 <= -1
main_GE_333(i1, i4, i124, i114, i91, env, static) -{0,0}> main_GE_335(i1, i4, i124, i114, i91, env, static) :|: 0 <= i124
main_GE_335(i1, i4, i124, i114, i91, env, static) -{1,1}> main_Load_337(i1, i4, i114, i91, i124, env, static) :|: 0 <= i124
main_Load_337(i1, i4, i114, i91, i124, env, static) -{1,1}> main_ConstantStackPush_339(i1, i4, i124, i114, i91, env, static) :|: 0 <= i124
main_ConstantStackPush_339(i1, i4, i124, i114, i91, env, static) -{1,1}> main_IntArithmetic_340(i1, i4, i124, iconst_1, i114, i91, env, static) :|: 0 <= i124 && iconst_1 = 1
main_IntArithmetic_340(i1, i4, i124, iconst_1, i114, i91, env, static) -{1,1}> main_Store_341(i1, i4, i125, i114, i91, env, static) :|: i124 + iconst_1 = i125 && 0 <= i124 && iconst_1 = 1 && 1 <= i125
main_Store_341(i1, i4, i125, i114, i91, env, static) -{1,1}> main_Load_342(i1, i4, i114, i91, i125, env, static) :|: 1 <= i125
main_Load_342(i1, i4, i114, i91, i125, env, static) -{1,1}> main_Load_343(i1, i4, i91, i114, i125, env, static) :|: 1 <= i125
main_Load_343(i1, i4, i91, i114, i125, env, static) -{1,1}> main_IntArithmetic_344(i1, i4, i91, i125, i114, env, static) :|: 1 <= i125
main_IntArithmetic_344(i1, i4, i91, i125, i114, env, static) -{1,1}> main_Store_345(i1, i4, i126, i114, env, static) :|: i91 + i125 = i126 && 1 <= i125
main_Store_345(i1, i4, i126, i114, env, static) -{1,1}> main_JMP_346(i1, i4, i114, i126, env, static) :|: 0 >= 0
main_JMP_346(i1, i4, i114, i126, env, static) -{1,1}> main_Load_352(i1, i4, i114, i126, env, static) :|: 0 >= 0
main_Load_352(i1, i4, i114, i126, env, static) -{0,0}> main_Load_274(i1, i4, i114, i126, env, static) :|: 0 >= 0

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

obtained
main_Load_2(i1, i4, env, static) -{15,15}> main_Load_274(i1, i4, i1, i4, env, static'1) :|: 0 >= 0 && 0 < 2 && 0 <= static'1 && 0 <= static && 0 <= 1 && 0 < 1 && static''' <= static + 2 && 0 <= static''' && 0 <= 2 && static'1 <= static''' + 1
by chaining
main_Load_2(i1, i4, env, static) -{0,0}> main_Load_4(i1, i4, env, static) :|: 0 >= 0
main_Load_4(i1, i4, env, static) -{0,0}> langle_clinit_rangle_ConstantStackPush_6(i1, i4, env, static) :|: 0 >= 0
langle_clinit_rangle_ConstantStackPush_6(i1, i4, env, static) -{1,1}> langle_clinit_rangle_ArrayCreate_14(iconst_0, i1, i4, env, static) :|: iconst_0 = 0
langle_clinit_rangle_ArrayCreate_14(iconst_0, i1, i4, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_16(a2, i1, i4, iconst_0, env, static) :|: a2 = 2 && iconst_0 = 0 && 0 < a2
langle_clinit_rangle_FieldAccess_16(a2, i1, i4, iconst_0, env, static) -{1,1}> langle_clinit_rangle_New_17(i1, i4, env, static') :|: 0 <= a2 && iconst_0 = 0 && static' <= static + a2 && 0 <= static && 0 < a2
langle_clinit_rangle_New_17(i1, i4, env, static) -{0,0}> langle_clinit_rangle_New_19(i1, i4, env, static) :|: 0 >= 0
langle_clinit_rangle_New_19(i1, i4, env, static) -{0,0}> langle_clinit_rangle_New_20(i1, i4, env, static) :|: 0 <= static
langle_clinit_rangle_New_20(i1, i4, env, static) -{1,1}> langle_clinit_rangle_Duplicate_22(o2, i1, i4, env, static) :|: 0 < o2 && o2 = 1
langle_clinit_rangle_Duplicate_22(o2, i1, i4, env, static) -{1,1}> langle_clinit_rangle_ConstantStackPush_25(o2, i1, i4, env, static) :|: 0 < o2
langle_clinit_rangle_ConstantStackPush_25(o2, i1, i4, env, static) -{1,1}> langle_clinit_rangle_InvokeMethod_27(o2, NULL, i1, i4, env, static) :|: NULL = 0 && 0 < o2
langle_clinit_rangle_InvokeMethod_27(o2, NULL, i1, i4, env, static) -{1,1}> langle_init_rangle_Load_28(o2, i1, i4, env, static) :|: NULL = 0 && 0 < o2
langle_init_rangle_Load_28(o2, i1, i4, env, static) -{1,1}> langle_init_rangle_InvokeMethod_31(o2, i1, i4, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_31(o2, i1, i4, env, static) -{1,1}> langle_init_rangle_Load_33(o2, i1, i4, env, static) :|: 0 < o2
langle_init_rangle_Load_33(o2, i1, i4, env, static) -{1,1}> langle_init_rangle_InvokeMethod_36(o2, i1, i4, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_36(o2, i1, i4, env, static) -{1,1}> langle_init_rangle_Return_39(o2, i1, i4, env, static) :|: 0 < o2
langle_init_rangle_Return_39(o2, i1, i4, env, static) -{1,1}> langle_init_rangle_Return_41(o2, i1, i4, env, static) :|: 0 < o2
langle_init_rangle_Return_41(o2, i1, i4, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_44(o2, i1, i4, env, static) :|: 0 < o2
langle_clinit_rangle_FieldAccess_44(o2, i1, i4, env, static) -{1,1}> langle_clinit_rangle_Return_45(i1, i4, env, static') :|: 0 < o2 && 0 <= o2 && 0 <= static && static' <= static + o2
langle_clinit_rangle_Return_45(i1, i4, env, static) -{1,1}> main_Load_46(i1, i4, env, static) :|: 0 >= 0
main_Load_46(i1, i4, env, static) -{0,0}> main_Load_49(i1, i4, env, static) :|: 0 >= 0
main_Load_49(i1, i4, env, static) -{0,0}> main_Load_50(i1, i4, env, static) :|: 0 <= static
main_Load_50(i1, i4, env, static) -{0,0}> main_Load_51(i1, i4, env, static) :|: 0 >= 0
main_Load_51(i1, i4, env, static) -{0,0}> main_Load_52(i1, i4, env, static) :|: 0 >= 0
main_Load_52(i1, i4, env, static) -{0,0}> main_Load_158(i1, i4, i1, i4, env, static) :|: 0 >= 0
main_Load_158(i1, i4, i25, i38, env, static) -{0,0}> main_Load_274(i1, i4, i25, i38, env, static) :|: 0 >= 0

obtained
main_Load_274(i1, i4, i79, i91, env, static) -{4,4}> main_LT_282(i1, i4, i96', 1, i79, i91, env, static) :|: 0 >= 0 && i79 - i91 = i96'
by chaining
main_Load_274(i1, i4, i79, i91, env, static) -{1,1}> main_Load_276(i1, i4, i79, i91, env, static) :|: 0 >= 0
main_Load_276(i1, i4, i79, i91, env, static) -{1,1}> main_IntArithmetic_277(i1, i4, i79, i91, env, static) :|: 0 >= 0
main_IntArithmetic_277(i1, i4, i79, i91, env, static) -{1,1}> main_ConstantStackPush_278(i1, i4, i96, i79, i91, env, static) :|: i79 - i91 = i96
main_ConstantStackPush_278(i1, i4, i96, i79, i91, env, static) -{1,1}> main_LT_282(i1, i4, i96, iconst_1, i79, i91, env, static) :|: iconst_1 = 1

obtained
main_LT_282(i1, i4, i102, 1, i79, i91, env, static) -{7,7}> main_GE_307(i1, i4, i107', i79, i91, env, static) :|: 0 >= 0 && 1 <= i102 && 0 < 1
by chaining
main_LT_282(i1, i4, i102, iconst_1, i79, i91, env, static) -{0,0}> main_LT_284(i1, i4, i102, iconst_1, i79, i91, env, static) :|: 1 <= i102 && iconst_1 = 1
main_LT_284(i1, i4, i102, iconst_1, i79, i91, env, static) -{1,1}> main_New_294(i1, i4, i79, i91, env, static) :|: 1 <= i102 && iconst_1 = 1 && iconst_1 <= i102
main_New_294(i1, i4, i79, i91, env, static) -{1,1}> main_Duplicate_299(i1, i4, o16, i79, i91, env, static) :|: o16 = 1 && 0 < o16
main_Duplicate_299(i1, i4, o16, i79, i91, env, static) -{1,1}> main_InvokeMethod_301(i1, i4, o16, i79, i91, env, static) :|: 0 < o16
main_InvokeMethod_301(i1, i4, o16, i79, i91, env, static) -{1,1}> main_InvokeMethod_303(i1, i4, o16, i79, i91, env, static) :|: 0 < o16
main_InvokeMethod_303(i1, i4, o16, i79, i91, env, static) -{1,1}> main_Store_305(i1, i4, i107, i79, i91, env, static) :|: 0 < o16
main_Store_305(i1, i4, i107, i79, i91, env, static) -{1,1}> main_Load_306(i1, i4, i79, i91, i107, env, static) :|: 0 >= 0
main_Load_306(i1, i4, i79, i91, i107, env, static) -{1,1}> main_GE_307(i1, i4, i107, i79, i91, env, static) :|: 0 >= 0

obtained
main_GE_307(i1, i4, i113, i79, i91, env, static) -{11,11}> main_GE_333(i1, i4, i118', i114', i91, env, static) :|: 0 >= 0 && 0 <= i113 && 0 < 1 && i79 - i113 = i114'
by chaining
main_GE_307(i1, i4, i113, i79, i91, env, static) -{0,0}> main_GE_309(i1, i4, i113, i79, i91, env, static) :|: 0 <= i113
main_GE_309(i1, i4, i113, i79, i91, env, static) -{1,1}> main_Load_311(i1, i4, i79, i91, i113, env, static) :|: 0 <= i113
main_Load_311(i1, i4, i79, i91, i113, env, static) -{1,1}> main_Load_313(i1, i4, i79, i91, i113, env, static) :|: 0 <= i113
main_Load_313(i1, i4, i79, i91, i113, env, static) -{1,1}> main_IntArithmetic_315(i1, i4, i79, i113, i91, env, static) :|: 0 <= i113
main_IntArithmetic_315(i1, i4, i79, i113, i91, env, static) -{1,1}> main_Store_317(i1, i4, i114, i91, env, static) :|: 0 <= i113 && i79 - i113 = i114
main_Store_317(i1, i4, i114, i91, env, static) -{1,1}> main_New_318(i1, i4, i114, i91, env, static) :|: 0 >= 0
main_New_318(i1, i4, i114, i91, env, static) -{1,1}> main_Duplicate_325(i1, i4, o18, i114, i91, env, static) :|: o18 = 1 && 0 < o18
main_Duplicate_325(i1, i4, o18, i114, i91, env, static) -{1,1}> main_InvokeMethod_327(i1, i4, o18, i114, i91, env, static) :|: 0 < o18
main_InvokeMethod_327(i1, i4, o18, i114, i91, env, static) -{1,1}> main_InvokeMethod_329(i1, i4, o18, i114, i91, env, static) :|: 0 < o18
main_InvokeMethod_329(i1, i4, o18, i114, i91, env, static) -{1,1}> main_Store_331(i1, i4, i118, i114, i91, env, static) :|: 0 < o18
main_Store_331(i1, i4, i118, i114, i91, env, static) -{1,1}> main_Load_332(i1, i4, i114, i91, i118, env, static) :|: 0 >= 0
main_Load_332(i1, i4, i114, i91, i118, env, static) -{1,1}> main_GE_333(i1, i4, i118, i114, i91, env, static) :|: 0 >= 0

obtained
main_GE_333(i1, i4, i124, i114, i91, env, static) -{10,10}> main_Load_274(i1, i4, i114, i126', env, static) :|: 0 >= 0 && i124 + 1 = i125' && 1 <= i125' && 0 <= i124 && i91 + i125' = i126'
by chaining
main_GE_333(i1, i4, i124, i114, i91, env, static) -{0,0}> main_GE_335(i1, i4, i124, i114, i91, env, static) :|: 0 <= i124
main_GE_335(i1, i4, i124, i114, i91, env, static) -{1,1}> main_Load_337(i1, i4, i114, i91, i124, env, static) :|: 0 <= i124
main_Load_337(i1, i4, i114, i91, i124, env, static) -{1,1}> main_ConstantStackPush_339(i1, i4, i124, i114, i91, env, static) :|: 0 <= i124
main_ConstantStackPush_339(i1, i4, i124, i114, i91, env, static) -{1,1}> main_IntArithmetic_340(i1, i4, i124, iconst_1, i114, i91, env, static) :|: 0 <= i124 && iconst_1 = 1
main_IntArithmetic_340(i1, i4, i124, iconst_1, i114, i91, env, static) -{1,1}> main_Store_341(i1, i4, i125, i114, i91, env, static) :|: i124 + iconst_1 = i125 && 0 <= i124 && iconst_1 = 1 && 1 <= i125
main_Store_341(i1, i4, i125, i114, i91, env, static) -{1,1}> main_Load_342(i1, i4, i114, i91, i125, env, static) :|: 1 <= i125
main_Load_342(i1, i4, i114, i91, i125, env, static) -{1,1}> main_Load_343(i1, i4, i91, i114, i125, env, static) :|: 1 <= i125
main_Load_343(i1, i4, i91, i114, i125, env, static) -{1,1}> main_IntArithmetic_344(i1, i4, i91, i125, i114, env, static) :|: 1 <= i125
main_IntArithmetic_344(i1, i4, i91, i125, i114, env, static) -{1,1}> main_Store_345(i1, i4, i126, i114, env, static) :|: i91 + i125 = i126 && 1 <= i125
main_Store_345(i1, i4, i126, i114, env, static) -{1,1}> main_JMP_346(i1, i4, i114, i126, env, static) :|: 0 >= 0
main_JMP_346(i1, i4, i114, i126, env, static) -{1,1}> main_Load_352(i1, i4, i114, i126, env, static) :|: 0 >= 0
main_Load_352(i1, i4, i114, i126, env, static) -{0,0}> main_Load_274(i1, i4, i114, i126, env, static) :|: 0 >= 0

(8) Obligation:

IntTrs with 8 rules
Start term: main_Load_2(#0, #1, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_Load_2(i1, i4, env, static) -{15,15}> main_Load_274(i1, i4, i1, i4, env, static'1) :|: 0 >= 0 && 0 < 2 && 0 <= static'1 && 0 <= static && 0 <= 1 && 0 < 1 && static''' <= static + 2 && 0 <= static''' && 0 <= 2 && static'1 <= static''' + 1
main_Load_274(i1, i4, i79, i91, env, static) -{4,4}> main_LT_282(i1, i4, i96', 1, i79, i91, env, static) :|: 0 >= 0 && i79 - i91 = i96'
main_LT_282(i1, i4, i101, iconst_1, i79, i91, env, static) -{0,0}> main_LT_283(i1, i4, i101, iconst_1, i79, i91, env, static) :|: i101 <= 0 && iconst_1 = 1
main_LT_282(i1, i4, i102, 1, i79, i91, env, static) -{7,7}> main_GE_307(i1, i4, i107', i79, i91, env, static) :|: 0 >= 0 && 1 <= i102 && 0 < 1
main_GE_307(i1, i4, i112, i79, i91, env, static) -{0,0}> main_GE_308(i1, i4, i112, i79, i91, env, static) :|: i112 <= -1
main_GE_307(i1, i4, i113, i79, i91, env, static) -{11,11}> main_GE_333(i1, i4, i118', i114', i91, env, static) :|: 0 >= 0 && 0 <= i113 && 0 < 1 && i79 - i113 = i114'
main_GE_333(i1, i4, i123, i114, i91, env, static) -{0,0}> main_GE_334(i1, i4, i123, i114, i91, env, static) :|: i123 <= -1
main_GE_333(i1, i4, i124, i114, i91, env, static) -{10,10}> main_Load_274(i1, i4, i114, i126', env, static) :|: 0 >= 0 && i124 + 1 = i125' && 1 <= i125' && 0 <= i124 && i91 + i125' = i126'

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

Moved arithmethic from lhss to constraints.

main_LT_282(i1, i4, i102, 1, i79, i91, env, static) -{7,7}> main_GE_307(i1, i4, i107', i79, i91, env, static) :|: 0 >= 0 && 1 <= i102 && 0 < 1
was transformed to
main_LT_282(i1, i4, i102, x, i79, i91, env, static) -{7,7}> main_GE_307(i1, i4, i107', i79, i91, env, static) :|: 0 >= 0 && 1 <= i102 && 0 < 1 && x = 1

(10) Obligation:

IntTrs with 8 rules
Start term: main_Load_2(#0, #1, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_GE_333(i1, i4, i123, i114, i91, env, static) -{0,0}> main_GE_334(i1, i4, i123, i114, i91, env, static) :|: i123 <= -1
main_Load_274(i1, i4, i79, i91, env, static) -{4,4}> main_LT_282(i1, i4, i96', 1, i79, i91, env, static) :|: 0 >= 0 && i79 - i91 = i96'
main_GE_307(i1, i4, i113, i79, i91, env, static) -{11,11}> main_GE_333(i1, i4, i118', i114', i91, env, static) :|: 0 >= 0 && 0 <= i113 && 0 < 1 && i79 - i113 = i114'
main_GE_307(i1, i4, i112, i79, i91, env, static) -{0,0}> main_GE_308(i1, i4, i112, i79, i91, env, static) :|: i112 <= -1
main_Load_2(i1, i4, env, static) -{15,15}> main_Load_274(i1, i4, i1, i4, env, static'1) :|: 0 >= 0 && 0 < 2 && 0 <= static'1 && 0 <= static && 0 <= 1 && 0 < 1 && static''' <= static + 2 && 0 <= static''' && 0 <= 2 && static'1 <= static''' + 1
main_GE_333(i1, i4, i124, i114, i91, env, static) -{10,10}> main_Load_274(i1, i4, i114, i126', env, static) :|: 0 >= 0 && i124 + 1 = i125' && 1 <= i125' && 0 <= i124 && i91 + i125' = i126'
main_LT_282(i1, i4, i102, x, i79, i91, env, static) -{7,7}> main_GE_307(i1, i4, i107', i79, i91, env, static) :|: 0 >= 0 && 1 <= i102 && 0 < 1 && x = 1
main_LT_282(i1, i4, i101, iconst_1, i79, i91, env, static) -{0,0}> main_LT_283(i1, i4, i101, iconst_1, i79, i91, env, static) :|: i101 <= 0 && iconst_1 = 1

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

Moved arithmethic from constraints to rhss.

main_Load_274(i1, i4, i79, i91, env, static) -{4,4}> main_LT_282(i1, i4, i96', 1, i79, i91, env, static) :|: 0 >= 0 && i79 - i91 = i96'
was transformed to
main_Load_274(i1, i4, i79, i91, env, static) -{4,4}> main_LT_282(i1, i4, i79 - i91, 1, i79, i91, env, static) :|: 0 >= 0 && i79 - i91 = i96'

main_GE_307(i1, i4, i113, i79, i91, env, static) -{11,11}> main_GE_333(i1, i4, i118', i114', i91, env, static) :|: 0 >= 0 && 0 <= i113 && 0 < 1 && i79 - i113 = i114'
was transformed to
main_GE_307(i1, i4, i113, i79, i91, env, static) -{11,11}> main_GE_333(i1, i4, i118', i79 - i113, i91, env, static) :|: 0 >= 0 && 0 <= i113 && 0 < 1 && i79 - i113 = i114'

main_GE_333(i1, i4, i124, i114, i91, env, static) -{10,10}> main_Load_274(i1, i4, i114, i126', env, static) :|: 0 >= 0 && i124 + 1 = i125' && 1 <= i125' && 0 <= i124 && i91 + i125' = i126'
was transformed to
main_GE_333(i1, i4, i124, i114, i91, env, static) -{10,10}> main_Load_274(i1, i4, i114, i91 + i124 + 1, env, static) :|: 0 >= 0 && i124 + 1 = i125' && 1 <= i125' && 0 <= i124 && i91 + i125' = i126'

main_LT_282(i1, i4, i101, iconst_1, i79, i91, env, static) -{0,0}> main_LT_283(i1, i4, i101, iconst_1, i79, i91, env, static) :|: i101 <= 0 && iconst_1 = 1
was transformed to
main_LT_282(i1, i4, i101, iconst_1, i79, i91, env, static) -{0,0}> main_LT_283(i1, i4, i101, 1, i79, i91, env, static) :|: i101 <= 0 && iconst_1 = 1

(12) Obligation:

IntTrs with 8 rules
Start term: main_Load_2(#0, #1, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_GE_333(i1, i4, i123, i114, i91, env, static) -{0,0}> main_GE_334(i1, i4, i123, i114, i91, env, static) :|: i123 <= -1
main_Load_274(i1, i4, i79, i91, env, static) -{4,4}> main_LT_282(i1, i4, i79 - i91, 1, i79, i91, env, static) :|: 0 >= 0 && i79 - i91 = i96'
main_GE_307(i1, i4, i113, i79, i91, env, static) -{11,11}> main_GE_333(i1, i4, i118', i79 - i113, i91, env, static) :|: 0 >= 0 && 0 <= i113 && 0 < 1 && i79 - i113 = i114'
main_GE_307(i1, i4, i112, i79, i91, env, static) -{0,0}> main_GE_308(i1, i4, i112, i79, i91, env, static) :|: i112 <= -1
main_Load_2(i1, i4, env, static) -{15,15}> main_Load_274(i1, i4, i1, i4, env, static'1) :|: 0 >= 0 && 0 < 2 && 0 <= static'1 && 0 <= static && 0 <= 1 && 0 < 1 && static''' <= static + 2 && 0 <= static''' && 0 <= 2 && static'1 <= static''' + 1
main_LT_282(i1, i4, i102, x, i79, i91, env, static) -{7,7}> main_GE_307(i1, i4, i107', i79, i91, env, static) :|: 0 >= 0 && 1 <= i102 && 0 < 1 && x = 1
main_GE_333(i1, i4, i124, i114, i91, env, static) -{10,10}> main_Load_274(i1, i4, i114, i91 + i124 + 1, env, static) :|: 0 >= 0 && i124 + 1 = i125' && 1 <= i125' && 0 <= i124 && i91 + i125' = i126'
main_LT_282(i1, i4, i101, iconst_1, i79, i91, env, static) -{0,0}> main_LT_283(i1, i4, i101, 1, i79, i91, env, static) :|: i101 <= 0 && iconst_1 = 1

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

Simplified expressions.

main_Load_274(i1, i4, i79, i91, env, static) -{4,4}> main_LT_282(i1, i4, i79 - i91, 1, i79, i91, env, static) :|: 0 >= 0 && i79 - i91 = i96'
was transformed to
main_Load_274(i1, i4, i79, i91, env, static) -{4,4}> main_LT_282(i1, i4, i79 + -1 * i91, 1, i79, i91, env, static) :|: i79 + -1 * i91 = i96'

main_Load_2(i1, i4, env, static) -{15,15}> main_Load_274(i1, i4, i1, i4, env, static'1) :|: 0 >= 0 && 0 < 2 && 0 <= static'1 && 0 <= static && 0 <= 1 && 0 < 1 && static''' <= static + 2 && 0 <= static''' && 0 <= 2 && static'1 <= static''' + 1
was transformed to
main_Load_2(i1, i4, env, static) -{15,15}> main_Load_274(i1, i4, i1, i4, env, static'1) :|: 0 <= static'1 && 0 <= static && static''' <= static + 2 && 0 <= static''' && static'1 <= static''' + 1

main_GE_307(i1, i4, i113, i79, i91, env, static) -{11,11}> main_GE_333(i1, i4, i118', i79 - i113, i91, env, static) :|: 0 >= 0 && 0 <= i113 && 0 < 1 && i79 - i113 = i114'
was transformed to
main_GE_307(i1, i4, i113, i79, i91, env, static) -{11,11}> main_GE_333(i1, i4, i118', i79 + -1 * i113, i91, env, static) :|: 0 <= i113 && i79 + -1 * i113 = i114'

main_LT_282(i1, i4, i102, x, i79, i91, env, static) -{7,7}> main_GE_307(i1, i4, i107', i79, i91, env, static) :|: 0 >= 0 && 1 <= i102 && 0 < 1 && x = 1
was transformed to
main_LT_282(i1, i4, i102, x, i79, i91, env, static) -{7,7}> main_GE_307(i1, i4, i107', i79, i91, env, static) :|: 1 <= i102 && x = 1

main_GE_333(i1, i4, i124, i114, i91, env, static) -{10,10}> main_Load_274(i1, i4, i114, i91 + i124 + 1, env, static) :|: 0 >= 0 && i124 + 1 = i125' && 1 <= i125' && 0 <= i124 && i91 + i125' = i126'
was transformed to
main_GE_333(i1, i4, i124, i114, i91, env, static) -{10,10}> main_Load_274(i1, i4, i114, i91 + i124 + 1, env, static) :|: i124 + 1 = i125' && 1 <= i125' && 0 <= i124 && i91 + i125' = i126'

(14) Obligation:

IntTrs with 8 rules
Start term: main_Load_2(#0, #1, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_GE_333(i1, i4, i123, i114, i91, env, static) -{0,0}> main_GE_334(i1, i4, i123, i114, i91, env, static) :|: i123 <= -1
main_LT_282(i1, i4, i101, iconst_1, i79, i91, env, static) -{0,0}> main_LT_283(i1, i4, i101, 1, i79, i91, env, static) :|: i101 <= 0 && iconst_1 = 1
main_GE_307(i1, i4, i112, i79, i91, env, static) -{0,0}> main_GE_308(i1, i4, i112, i79, i91, env, static) :|: i112 <= -1
main_Load_274(i1, i4, i79, i91, env, static) -{4,4}> main_LT_282(i1, i4, i79 + -1 * i91, 1, i79, i91, env, static) :|: i79 + -1 * i91 = i96'
main_GE_307(i1, i4, i113, i79, i91, env, static) -{11,11}> main_GE_333(i1, i4, i118', i79 + -1 * i113, i91, env, static) :|: 0 <= i113 && i79 + -1 * i113 = i114'
main_Load_2(i1, i4, env, static) -{15,15}> main_Load_274(i1, i4, i1, i4, env, static'1) :|: 0 <= static'1 && 0 <= static && static''' <= static + 2 && 0 <= static''' && static'1 <= static''' + 1
main_GE_333(i1, i4, i124, i114, i91, env, static) -{10,10}> main_Load_274(i1, i4, i114, i91 + i124 + 1, env, static) :|: i124 + 1 = i125' && 1 <= i125' && 0 <= i124 && i91 + i125' = i126'
main_LT_282(i1, i4, i102, x, i79, i91, env, static) -{7,7}> main_GE_307(i1, i4, i107', i79, i91, env, static) :|: 1 <= i102 && x = 1

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

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

(16) Obligation:

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

(18) Obligation:

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

Moved arithmethic from lhss to constraints.

(20) Obligation:

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

Moved arithmethic from constraints to rhss.

(22) Obligation:

IntTrs with 8 rules
Start term: main_Load_2(#0, #1, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_GE_333(i1, i4, i123, i114, i91, env, static) -{0,0}> main_GE_334(i1, i4, i123, i114, i91, env, static) :|: i123 <= -1
main_Load_274(i1, i4, i79, i91, env, static) -{4,4}> main_LT_282(i1, i4, i79 - i91, 1, i79, i91, env, static) :|: 0 >= 0 && i79 - i91 = i96'
main_GE_307(i1, i4, i113, i79, i91, env, static) -{11,11}> main_GE_333(i1, i4, i118', i79 - i113, i91, env, static) :|: 0 >= 0 && 0 <= i113 && 0 < 1 && i79 - i113 = i114'
main_GE_307(i1, i4, i112, i79, i91, env, static) -{0,0}> main_GE_308(i1, i4, i112, i79, i91, env, static) :|: i112 <= -1
main_Load_2(i1, i4, env, static) -{15,15}> main_Load_274(i1, i4, i1, i4, env, static'1) :|: 0 >= 0 && 0 < 2 && 0 <= static'1 && 0 <= static && 0 <= 1 && 0 < 1 && static''' <= static + 2 && 0 <= static''' && 0 <= 2 && static'1 <= static''' + 1
main_LT_282(i1, i4, i102, x, i79, i91, env, static) -{7,7}> main_GE_307(i1, i4, i107', i79, i91, env, static) :|: 0 >= 0 && 1 <= i102 && 0 < 1 && x = 1
main_GE_333(i1, i4, i124, i114, i91, env, static) -{10,10}> main_Load_274(i1, i4, i114, i91 + i124 + 1, env, static) :|: 0 >= 0 && i124 + 1 = i125' && 1 <= i125' && 0 <= i124 && i91 + i125' = i126'
main_LT_282(i1, i4, i101, iconst_1, i79, i91, env, static) -{0,0}> main_LT_283(i1, i4, i101, 1, i79, i91, env, static) :|: i101 <= 0 && iconst_1 = 1

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

Simplified expressions.

(24) Obligation:

IntTrs with 8 rules
Start term: main_Load_2(#0, #1, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_GE_333(i1, i4, i123, i114, i91, env, static) -{0,0}> main_GE_334(i1, i4, i123, i114, i91, env, static) :|: i123 <= -1
main_LT_282(i1, i4, i101, iconst_1, i79, i91, env, static) -{0,0}> main_LT_283(i1, i4, i101, 1, i79, i91, env, static) :|: i101 <= 0 && iconst_1 = 1
main_GE_307(i1, i4, i112, i79, i91, env, static) -{0,0}> main_GE_308(i1, i4, i112, i79, i91, env, static) :|: i112 <= -1
main_Load_274(i1, i4, i79, i91, env, static) -{4,4}> main_LT_282(i1, i4, i79 + -1 * i91, 1, i79, i91, env, static) :|: i79 + -1 * i91 = i96'
main_GE_307(i1, i4, i113, i79, i91, env, static) -{11,11}> main_GE_333(i1, i4, i118', i79 + -1 * i113, i91, env, static) :|: 0 <= i113 && i79 + -1 * i113 = i114'
main_Load_2(i1, i4, env, static) -{15,15}> main_Load_274(i1, i4, i1, i4, env, static'1) :|: 0 <= static'1 && 0 <= static && static''' <= static + 2 && 0 <= static''' && static'1 <= static''' + 1
main_GE_333(i1, i4, i124, i114, i91, env, static) -{10,10}> main_Load_274(i1, i4, i114, i91 + i124 + 1, env, static) :|: i124 + 1 = i125' && 1 <= i125' && 0 <= i124 && i91 + i125' = i126'
main_LT_282(i1, i4, i102, x, i79, i91, env, static) -{7,7}> main_GE_307(i1, i4, i107', i79, i91, env, static) :|: 1 <= i102 && x = 1

(25) TerminationGraphToComplexityProof (BOTH CONCRETE BOUNDS(ID, ADD(6)) transformation)

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

(26) Obligation:

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

Used field analysis yielded the following read fields:

Considered paths: all paths from start

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

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

(28) Obligation:

IntTrs with 61 rules
Start term: main_Load_2(#0, #1, env, static)
Considered paths: all paths from start
Rules:
main_Load_2(i1, i4, env, static) -{0,0}> main_Load_4(i1, i4, env, static) :|: 0 >= 0
main_Load_4(i1, i4, env, static) -{0,0}> langle_clinit_rangle_ConstantStackPush_6(i1, i4, env, static) :|: 0 >= 0
langle_clinit_rangle_ConstantStackPush_6(i1, i4, env, static) -{1,1}> langle_clinit_rangle_ArrayCreate_14(iconst_0, i1, i4, env, static) :|: iconst_0 = 0
langle_clinit_rangle_ArrayCreate_14(iconst_0, i1, i4, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_16(a2, i1, i4, iconst_0, env, static) :|: a2 = 2 && iconst_0 = 0 && 0 < a2
langle_clinit_rangle_FieldAccess_16(a2, i1, i4, iconst_0, env, static) -{1,1}> langle_clinit_rangle_New_17(i1, i4, env, static') :|: 0 <= a2 && iconst_0 = 0 && static' <= static + a2 && 0 <= static && 0 < a2
langle_clinit_rangle_New_17(i1, i4, env, static) -{0,0}> langle_clinit_rangle_New_19(i1, i4, env, static) :|: 0 >= 0
langle_clinit_rangle_New_19(i1, i4, env, static) -{0,0}> langle_clinit_rangle_New_20(i1, i4, env, static) :|: 0 <= static
langle_clinit_rangle_New_20(i1, i4, env, static) -{1,1}> langle_clinit_rangle_Duplicate_22(o2, i1, i4, env, static) :|: 0 < o2 && o2 = 1
langle_clinit_rangle_Duplicate_22(o2, i1, i4, env, static) -{1,1}> langle_clinit_rangle_ConstantStackPush_25(o2, i1, i4, env, static) :|: 0 < o2
langle_clinit_rangle_ConstantStackPush_25(o2, i1, i4, env, static) -{1,1}> langle_clinit_rangle_InvokeMethod_27(o2, NULL, i1, i4, env, static) :|: NULL = 0 && 0 < o2
langle_clinit_rangle_InvokeMethod_27(o2, NULL, i1, i4, env, static) -{1,1}> langle_init_rangle_Load_28(o2, i1, i4, env, static) :|: NULL = 0 && 0 < o2
langle_init_rangle_Load_28(o2, i1, i4, env, static) -{1,1}> langle_init_rangle_InvokeMethod_31(o2, i1, i4, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_31(o2, i1, i4, env, static) -{1,1}> langle_init_rangle_Load_33(o2, i1, i4, env, static) :|: 0 < o2
langle_init_rangle_Load_33(o2, i1, i4, env, static) -{1,1}> langle_init_rangle_InvokeMethod_36(o2, i1, i4, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_36(o2, i1, i4, env, static) -{1,1}> langle_init_rangle_Return_39(o2, i1, i4, env, static) :|: 0 < o2
langle_init_rangle_Return_39(o2, i1, i4, env, static) -{1,1}> langle_init_rangle_Return_41(o2, i1, i4, env, static) :|: 0 < o2
langle_init_rangle_Return_41(o2, i1, i4, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_44(o2, i1, i4, env, static) :|: 0 < o2
langle_clinit_rangle_FieldAccess_44(o2, i1, i4, env, static) -{1,1}> langle_clinit_rangle_Return_45(i1, i4, env, static') :|: 0 < o2 && 0 <= o2 && 0 <= static && static' <= static + o2
langle_clinit_rangle_Return_45(i1, i4, env, static) -{1,1}> main_Load_46(i1, i4, env, static) :|: 0 >= 0
main_Load_46(i1, i4, env, static) -{0,0}> main_Load_49(i1, i4, env, static) :|: 0 >= 0
main_Load_49(i1, i4, env, static) -{0,0}> main_Load_50(i1, i4, env, static) :|: 0 <= static
main_Load_50(i1, i4, env, static) -{0,0}> main_Load_51(i1, i4, env, static) :|: 0 >= 0
main_Load_51(i1, i4, env, static) -{0,0}> main_Load_52(i1, i4, env, static) :|: 0 >= 0
main_Load_52(i1, i4, env, static) -{0,0}> main_Load_158(i1, i4, i1, i4, env, static) :|: 0 >= 0
main_Load_158(i1, i4, i25, i38, env, static) -{0,0}> main_Load_274(i1, i4, i25, i38, env, static) :|: 0 >= 0
main_Load_274(i1, i4, i79, i91, env, static) -{1,1}> main_Load_276(i1, i4, i79, i91, env, static) :|: 0 >= 0
main_Load_276(i1, i4, i79, i91, env, static) -{1,1}> main_IntArithmetic_277(i1, i4, i79, i91, env, static) :|: 0 >= 0
main_IntArithmetic_277(i1, i4, i79, i91, env, static) -{1,1}> main_ConstantStackPush_278(i1, i4, i96, i79, i91, env, static) :|: i79 - i91 = i96
main_ConstantStackPush_278(i1, i4, i96, i79, i91, env, static) -{1,1}> main_LT_282(i1, i4, i96, iconst_1, i79, i91, env, static) :|: iconst_1 = 1
main_LT_282(i1, i4, i102, iconst_1, i79, i91, env, static) -{0,0}> main_LT_284(i1, i4, i102, iconst_1, i79, i91, env, static) :|: 1 <= i102 && iconst_1 = 1
main_LT_284(i1, i4, i102, iconst_1, i79, i91, env, static) -{1,1}> main_New_294(i1, i4, i79, i91, env, static) :|: 1 <= i102 && iconst_1 = 1 && iconst_1 <= i102
main_New_294(i1, i4, i79, i91, env, static) -{1,1}> main_Duplicate_299(i1, i4, o16, i79, i91, env, static) :|: o16 = 1 && 0 < o16
main_Duplicate_299(i1, i4, o16, i79, i91, env, static) -{1,1}> main_InvokeMethod_301(i1, i4, o16, i79, i91, env, static) :|: 0 < o16
main_InvokeMethod_301(i1, i4, o16, i79, i91, env, static) -{1,1}> main_InvokeMethod_303(i1, i4, o16, i79, i91, env, static) :|: 0 < o16
main_InvokeMethod_303(i1, i4, o16, i79, i91, env, static) -{1,1}> main_Store_305(i1, i4, i107, i79, i91, env, static) :|: 0 < o16
main_Store_305(i1, i4, i107, i79, i91, env, static) -{1,1}> main_Load_306(i1, i4, i79, i91, i107, env, static) :|: 0 >= 0
main_Load_306(i1, i4, i79, i91, i107, env, static) -{1,1}> main_GE_307(i1, i4, i107, i79, i91, env, static) :|: 0 >= 0
main_GE_307(i1, i4, i113, i79, i91, env, static) -{0,0}> main_GE_309(i1, i4, i113, i79, i91, env, static) :|: 0 <= i113
main_GE_309(i1, i4, i113, i79, i91, env, static) -{1,1}> main_Load_311(i1, i4, i79, i91, i113, env, static) :|: 0 <= i113
main_Load_311(i1, i4, i79, i91, i113, env, static) -{1,1}> main_Load_313(i1, i4, i79, i91, i113, env, static) :|: 0 <= i113
main_Load_313(i1, i4, i79, i91, i113, env, static) -{1,1}> main_IntArithmetic_315(i1, i4, i79, i113, i91, env, static) :|: 0 <= i113
main_IntArithmetic_315(i1, i4, i79, i113, i91, env, static) -{1,1}> main_Store_317(i1, i4, i114, i91, env, static) :|: 0 <= i113 && i79 - i113 = i114
main_Store_317(i1, i4, i114, i91, env, static) -{1,1}> main_New_318(i1, i4, i114, i91, env, static) :|: 0 >= 0
main_New_318(i1, i4, i114, i91, env, static) -{1,1}> main_Duplicate_325(i1, i4, o18, i114, i91, env, static) :|: o18 = 1 && 0 < o18
main_Duplicate_325(i1, i4, o18, i114, i91, env, static) -{1,1}> main_InvokeMethod_327(i1, i4, o18, i114, i91, env, static) :|: 0 < o18
main_InvokeMethod_327(i1, i4, o18, i114, i91, env, static) -{1,1}> main_InvokeMethod_329(i1, i4, o18, i114, i91, env, static) :|: 0 < o18
main_InvokeMethod_329(i1, i4, o18, i114, i91, env, static) -{1,1}> main_Store_331(i1, i4, i118, i114, i91, env, static) :|: 0 < o18
main_Store_331(i1, i4, i118, i114, i91, env, static) -{1,1}> main_Load_332(i1, i4, i114, i91, i118, env, static) :|: 0 >= 0
main_Load_332(i1, i4, i114, i91, i118, env, static) -{1,1}> main_GE_333(i1, i4, i118, i114, i91, env, static) :|: 0 >= 0
main_GE_333(i1, i4, i124, i114, i91, env, static) -{0,0}> main_GE_335(i1, i4, i124, i114, i91, env, static) :|: 0 <= i124
main_GE_335(i1, i4, i124, i114, i91, env, static) -{1,1}> main_Load_337(i1, i4, i114, i91, i124, env, static) :|: 0 <= i124
main_Load_337(i1, i4, i114, i91, i124, env, static) -{1,1}> main_ConstantStackPush_339(i1, i4, i124, i114, i91, env, static) :|: 0 <= i124
main_ConstantStackPush_339(i1, i4, i124, i114, i91, env, static) -{1,1}> main_IntArithmetic_340(i1, i4, i124, iconst_1, i114, i91, env, static) :|: 0 <= i124 && iconst_1 = 1
main_IntArithmetic_340(i1, i4, i124, iconst_1, i114, i91, env, static) -{1,1}> main_Store_341(i1, i4, i125, i114, i91, env, static) :|: i124 + iconst_1 = i125 && 0 <= i124 && iconst_1 = 1 && 1 <= i125
main_Store_341(i1, i4, i125, i114, i91, env, static) -{1,1}> main_Load_342(i1, i4, i114, i91, i125, env, static) :|: 1 <= i125
main_Load_342(i1, i4, i114, i91, i125, env, static) -{1,1}> main_Load_343(i1, i4, i91, i114, i125, env, static) :|: 1 <= i125
main_Load_343(i1, i4, i91, i114, i125, env, static) -{1,1}> main_IntArithmetic_344(i1, i4, i91, i125, i114, env, static) :|: 1 <= i125
main_IntArithmetic_344(i1, i4, i91, i125, i114, env, static) -{1,1}> main_Store_345(i1, i4, i126, i114, env, static) :|: i91 + i125 = i126 && 1 <= i125
main_Store_345(i1, i4, i126, i114, env, static) -{1,1}> main_JMP_346(i1, i4, i114, i126, env, static) :|: 0 >= 0
main_JMP_346(i1, i4, i114, i126, env, static) -{1,1}> main_Load_352(i1, i4, i114, i126, env, static) :|: 0 >= 0
main_Load_352(i1, i4, i114, i126, env, static) -{0,0}> main_Load_274(i1, i4, i114, i126, env, static) :|: 0 >= 0

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

obtained
main_Load_274(i1, i4, i79, i91, env, static) -{32,32}> main_Load_274(i1, i4, i114', i126', env, static) :|: 0 >= 0 && 0 < 1 && 1 <= i96' && 0 <= i118' && i118' + 1 = i125' && i79 - i107' = i114' && i79 - i91 = i96' && 1 <= i125' && 0 <= i107' && i91 + i125' = i126'
by chaining
main_Load_274(i1, i4, i79, i91, env, static) -{1,1}> main_Load_276(i1, i4, i79, i91, env, static) :|: 0 >= 0
main_Load_276(i1, i4, i79, i91, env, static) -{1,1}> main_IntArithmetic_277(i1, i4, i79, i91, env, static) :|: 0 >= 0
main_IntArithmetic_277(i1, i4, i79, i91, env, static) -{1,1}> main_ConstantStackPush_278(i1, i4, i96, i79, i91, env, static) :|: i79 - i91 = i96
main_ConstantStackPush_278(i1, i4, i96, i79, i91, env, static) -{1,1}> main_LT_282(i1, i4, i96, iconst_1, i79, i91, env, static) :|: iconst_1 = 1
main_LT_282(i1, i4, i102, iconst_1, i79, i91, env, static) -{0,0}> main_LT_284(i1, i4, i102, iconst_1, i79, i91, env, static) :|: 1 <= i102 && iconst_1 = 1
main_LT_284(i1, i4, i102, iconst_1, i79, i91, env, static) -{1,1}> main_New_294(i1, i4, i79, i91, env, static) :|: 1 <= i102 && iconst_1 = 1 && iconst_1 <= i102
main_New_294(i1, i4, i79, i91, env, static) -{1,1}> main_Duplicate_299(i1, i4, o16, i79, i91, env, static) :|: o16 = 1 && 0 < o16
main_Duplicate_299(i1, i4, o16, i79, i91, env, static) -{1,1}> main_InvokeMethod_301(i1, i4, o16, i79, i91, env, static) :|: 0 < o16
main_InvokeMethod_301(i1, i4, o16, i79, i91, env, static) -{1,1}> main_InvokeMethod_303(i1, i4, o16, i79, i91, env, static) :|: 0 < o16
main_InvokeMethod_303(i1, i4, o16, i79, i91, env, static) -{1,1}> main_Store_305(i1, i4, i107, i79, i91, env, static) :|: 0 < o16
main_Store_305(i1, i4, i107, i79, i91, env, static) -{1,1}> main_Load_306(i1, i4, i79, i91, i107, env, static) :|: 0 >= 0
main_Load_306(i1, i4, i79, i91, i107, env, static) -{1,1}> main_GE_307(i1, i4, i107, i79, i91, env, static) :|: 0 >= 0
main_GE_307(i1, i4, i113, i79, i91, env, static) -{0,0}> main_GE_309(i1, i4, i113, i79, i91, env, static) :|: 0 <= i113
main_GE_309(i1, i4, i113, i79, i91, env, static) -{1,1}> main_Load_311(i1, i4, i79, i91, i113, env, static) :|: 0 <= i113
main_Load_311(i1, i4, i79, i91, i113, env, static) -{1,1}> main_Load_313(i1, i4, i79, i91, i113, env, static) :|: 0 <= i113
main_Load_313(i1, i4, i79, i91, i113, env, static) -{1,1}> main_IntArithmetic_315(i1, i4, i79, i113, i91, env, static) :|: 0 <= i113
main_IntArithmetic_315(i1, i4, i79, i113, i91, env, static) -{1,1}> main_Store_317(i1, i4, i114, i91, env, static) :|: 0 <= i113 && i79 - i113 = i114
main_Store_317(i1, i4, i114, i91, env, static) -{1,1}> main_New_318(i1, i4, i114, i91, env, static) :|: 0 >= 0
main_New_318(i1, i4, i114, i91, env, static) -{1,1}> main_Duplicate_325(i1, i4, o18, i114, i91, env, static) :|: o18 = 1 && 0 < o18
main_Duplicate_325(i1, i4, o18, i114, i91, env, static) -{1,1}> main_InvokeMethod_327(i1, i4, o18, i114, i91, env, static) :|: 0 < o18
main_InvokeMethod_327(i1, i4, o18, i114, i91, env, static) -{1,1}> main_InvokeMethod_329(i1, i4, o18, i114, i91, env, static) :|: 0 < o18
main_InvokeMethod_329(i1, i4, o18, i114, i91, env, static) -{1,1}> main_Store_331(i1, i4, i118, i114, i91, env, static) :|: 0 < o18
main_Store_331(i1, i4, i118, i114, i91, env, static) -{1,1}> main_Load_332(i1, i4, i114, i91, i118, env, static) :|: 0 >= 0
main_Load_332(i1, i4, i114, i91, i118, env, static) -{1,1}> main_GE_333(i1, i4, i118, i114, i91, env, static) :|: 0 >= 0
main_GE_333(i1, i4, i124, i114, i91, env, static) -{0,0}> main_GE_335(i1, i4, i124, i114, i91, env, static) :|: 0 <= i124
main_GE_335(i1, i4, i124, i114, i91, env, static) -{1,1}> main_Load_337(i1, i4, i114, i91, i124, env, static) :|: 0 <= i124
main_Load_337(i1, i4, i114, i91, i124, env, static) -{1,1}> main_ConstantStackPush_339(i1, i4, i124, i114, i91, env, static) :|: 0 <= i124
main_ConstantStackPush_339(i1, i4, i124, i114, i91, env, static) -{1,1}> main_IntArithmetic_340(i1, i4, i124, iconst_1, i114, i91, env, static) :|: 0 <= i124 && iconst_1 = 1
main_IntArithmetic_340(i1, i4, i124, iconst_1, i114, i91, env, static) -{1,1}> main_Store_341(i1, i4, i125, i114, i91, env, static) :|: i124 + iconst_1 = i125 && 0 <= i124 && iconst_1 = 1 && 1 <= i125
main_Store_341(i1, i4, i125, i114, i91, env, static) -{1,1}> main_Load_342(i1, i4, i114, i91, i125, env, static) :|: 1 <= i125
main_Load_342(i1, i4, i114, i91, i125, env, static) -{1,1}> main_Load_343(i1, i4, i91, i114, i125, env, static) :|: 1 <= i125
main_Load_343(i1, i4, i91, i114, i125, env, static) -{1,1}> main_IntArithmetic_344(i1, i4, i91, i125, i114, env, static) :|: 1 <= i125
main_IntArithmetic_344(i1, i4, i91, i125, i114, env, static) -{1,1}> main_Store_345(i1, i4, i126, i114, env, static) :|: i91 + i125 = i126 && 1 <= i125
main_Store_345(i1, i4, i126, i114, env, static) -{1,1}> main_JMP_346(i1, i4, i114, i126, env, static) :|: 0 >= 0
main_JMP_346(i1, i4, i114, i126, env, static) -{1,1}> main_Load_352(i1, i4, i114, i126, env, static) :|: 0 >= 0
main_Load_352(i1, i4, i114, i126, env, static) -{0,0}> main_Load_274(i1, i4, i114, i126, env, static) :|: 0 >= 0

(30) Obligation:

IntTrs with 2 rules
Start term: main_Load_2(#0, #1, env, static)
Considered paths: all paths from start
Rules:
main_Load_2(i1, i4, env, static) -{15,15}> main_Load_274(i1, i4, i1, i4, env, static'1) :|: 0 >= 0 && 0 < 2 && 0 <= static'1 && 0 <= static && 0 <= 1 && 0 < 1 && static''' <= static + 2 && 0 <= static''' && 0 <= 2 && static'1 <= static''' + 1
main_Load_274(i1, i4, i79, i91, env, static) -{32,32}> main_Load_274(i1, i4, i114', i126', env, static) :|: 0 >= 0 && 0 < 1 && 1 <= i96' && 0 <= i118' && i118' + 1 = i125' && i79 - i107' = i114' && i79 - i91 = i96' && 1 <= i125' && 0 <= i107' && i91 + i125' = i126'

(31) 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, x4) → main_Load_2(x1, x2, x4)
main_Load_274(x1, x2, x3, x4, x5, x6) → main_Load_274(x3, x4)

(32) Obligation:

IntTrs with 2 rules
Start term: main_Load_2(#0, #1, static)
Considered paths: all paths from start
Rules:
main_Load_2(i1, i4, static) -{15,15}> main_Load_274(i1, i4) :|: 0 >= 0 && 0 < 2 && 0 <= static'1 && 0 <= static && 0 <= 1 && 0 < 1 && static''' <= static + 2 && 0 <= static''' && 0 <= 2 && static'1 <= static''' + 1
main_Load_274(i79, i91) -{32,32}> main_Load_274(i114', i126') :|: 0 >= 0 && 0 < 1 && 1 <= i96' && 0 <= i118' && i118' + 1 = i125' && i79 - i107' = i114' && i79 - i91 = i96' && 1 <= i125' && 0 <= i107' && i91 + i125' = i126'

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

Moved arithmethic from constraints to rhss.

main_Load_274(i79, i91) -{32,32}> main_Load_274(i114', i126') :|: 0 >= 0 && 0 < 1 && 1 <= i96' && 0 <= i118' && i118' + 1 = i125' && i79 - i107' = i114' && i79 - i91 = i96' && 1 <= i125' && 0 <= i107' && i91 + i125' = i126'
was transformed to
main_Load_274(i79, i91) -{32,32}> main_Load_274(i79 - i107', i91 + i118' + 1) :|: 0 >= 0 && 0 < 1 && 1 <= i96' && 0 <= i118' && i118' + 1 = i125' && i79 - i107' = i114' && i79 - i91 = i96' && 1 <= i125' && 0 <= i107' && i91 + i125' = i126'

(34) Obligation:

IntTrs with 2 rules
Start term: main_Load_2(#0, #1, static)
Considered paths: all paths from start
Rules:
main_Load_274(i79, i91) -{32,32}> main_Load_274(i79 - i107', i91 + i118' + 1) :|: 0 >= 0 && 0 < 1 && 1 <= i96' && 0 <= i118' && i118' + 1 = i125' && i79 - i107' = i114' && i79 - i91 = i96' && 1 <= i125' && 0 <= i107' && i91 + i125' = i126'
main_Load_2(i1, i4, static) -{15,15}> main_Load_274(i1, i4) :|: 0 >= 0 && 0 < 2 && 0 <= static'1 && 0 <= static && 0 <= 1 && 0 < 1 && static''' <= static + 2 && 0 <= static''' && 0 <= 2 && static'1 <= static''' + 1

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

Simplified expressions.

main_Load_2(i1, i4, static) -{15,15}> main_Load_274(i1, i4) :|: 0 >= 0 && 0 < 2 && 0 <= static'1 && 0 <= static && 0 <= 1 && 0 < 1 && static''' <= static + 2 && 0 <= static''' && 0 <= 2 && static'1 <= static''' + 1
was transformed to
main_Load_2(i1, i4, static) -{15,15}> main_Load_274(i1, i4) :|: 0 <= static'1 && 0 <= static && static''' <= static + 2 && 0 <= static''' && static'1 <= static''' + 1

main_Load_274(i79, i91) -{32,32}> main_Load_274(i79 - i107', i91 + i118' + 1) :|: 0 >= 0 && 0 < 1 && 1 <= i96' && 0 <= i118' && i118' + 1 = i125' && i79 - i107' = i114' && i79 - i91 = i96' && 1 <= i125' && 0 <= i107' && i91 + i125' = i126'
was transformed to
main_Load_274(i79, i91) -{32,32}> main_Load_274(i79 + -1 * i107', i91 + i118' + 1) :|: 1 <= i96' && 0 <= i118' && i118' + 1 = i125' && i79 + -1 * i107' = i114' && i79 + -1 * i91 = i96' && 1 <= i125' && 0 <= i107' && i91 + i125' = i126'

(36) Obligation:

IntTrs with 2 rules
Start term: main_Load_2(#0, #1, static)
Considered paths: all paths from start
Rules:
main_Load_274(i79, i91) -{32,32}> main_Load_274(i79 + -1 * i107', i91 + i118' + 1) :|: 1 <= i96' && 0 <= i118' && i118' + 1 = i125' && i79 + -1 * i107' = i114' && i79 + -1 * i91 = i96' && 1 <= i125' && 0 <= i107' && i91 + i125' = i126'
main_Load_2(i1, i4, static) -{15,15}> main_Load_274(i1, i4) :|: 0 <= static'1 && 0 <= static && static''' <= static + 2 && 0 <= static''' && static'1 <= static''' + 1

(37) koat Proof (EQUIVALENT transformation)

YES(?, 32*ar_0 + 32*ar_1 + 15)

Initial complexity problem:
1: T:
(Comp: ?, Cost: 32) main_Load_274(ar_0, ar_1, ar_2) -> Com_1(main_Load_274(ar_0 - i107', ar_1 + i118' + 1, arityPad)) [ 1 <= i96' /\ 0 <= i118' /\ i118' + 1 = i125' /\ ar_0 - i107' = i114' /\ ar_0 - ar_1 = i96' /\ 1 <= i125' /\ 0 <= i107' /\ ar_1 + i125' = i126' ]
(Comp: ?, Cost: 15) main_Load_2(ar_0, ar_1, ar_2) -> Com_1(main_Load_274(ar_0, ar_1, arityPad)) [ 0 <= static'1 /\ 0 <= ar_2 /\ static''' <= ar_2 + 2 /\ 0 <= static''' /\ static'1 <= static''' + 1 ]
(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: 32) main_Load_274(ar_0, ar_1, ar_2) -> Com_1(main_Load_274(ar_0 - i107', ar_1 + i118' + 1, arityPad)) [ 1 <= i96' /\ 0 <= i118' /\ i118' + 1 = i125' /\ ar_0 - i107' = i114' /\ ar_0 - ar_1 = i96' /\ 1 <= i125' /\ 0 <= i107' /\ ar_1 + i125' = i126' ]
(Comp: 1, Cost: 15) main_Load_2(ar_0, ar_1, ar_2) -> Com_1(main_Load_274(ar_0, ar_1, arityPad)) [ 0 <= static'1 /\ 0 <= ar_2 /\ static''' <= ar_2 + 2 /\ 0 <= static''' /\ static'1 <= static''' + 1 ]
(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_274) = V_1 - V_2
Pol(main_Load_2) = V_1 - V_2
Pol(koat_start) = V_1 - V_2
orients all transitions weakly and the transition
main_Load_274(ar_0, ar_1, ar_2) -> Com_1(main_Load_274(ar_0 - i107', ar_1 + i118' + 1, arityPad)) [ 1 <= i96' /\ 0 <= i118' /\ i118' + 1 = i125' /\ ar_0 - i107' = i114' /\ ar_0 - ar_1 = i96' /\ 1 <= i125' /\ 0 <= i107' /\ ar_1 + i125' = i126' ]
strictly and produces the following problem:
3: T:
(Comp: ar_0 + ar_1, Cost: 32) main_Load_274(ar_0, ar_1, ar_2) -> Com_1(main_Load_274(ar_0 - i107', ar_1 + i118' + 1, arityPad)) [ 1 <= i96' /\ 0 <= i118' /\ i118' + 1 = i125' /\ ar_0 - i107' = i114' /\ ar_0 - ar_1 = i96' /\ 1 <= i125' /\ 0 <= i107' /\ ar_1 + i125' = i126' ]
(Comp: 1, Cost: 15) main_Load_2(ar_0, ar_1, ar_2) -> Com_1(main_Load_274(ar_0, ar_1, arityPad)) [ 0 <= static'1 /\ 0 <= ar_2 /\ static''' <= ar_2 + 2 /\ 0 <= static''' /\ static'1 <= static''' + 1 ]
(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 32*ar_0 + 32*ar_1 + 15

Time: 0.195 sec (SMT: 0.176 sec)

(0) Obligation:

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

(2) Obligation:

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

(4) Obligation:

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

(6) Obligation:

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

(8) Obligation:

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

(10) Obligation:

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

(12) Obligation:

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

(14) Obligation:

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

(16) Obligation:

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

(18) Obligation:

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

(20) Obligation:

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

(22) Obligation:

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

(24) Obligation:

(25) TerminationGraphToComplexityProof (BOTH CONCRETE BOUNDS(ID, ADD(6)) transformation)

(26) Obligation:

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

(28) Obligation:

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

(30) Obligation:

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

(32) Obligation:

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

(34) Obligation:

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

(36) Obligation:

(37) koat Proof (EQUIVALENT transformation)

(38) BOUNDS(CONSTANT, 15 + 32 * |#0| + 32 * |#1|)