time complexity proof of /tmp/tmpf5C7xB/Et4.jar

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

0 JBC problem

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

↳2 JBCTerminationGraph

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

↳4 JBCComplexityEdges

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

    ↳6 WeightedIntTrs

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

        ↳8 WeightedIntTrs

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

        ↳10 WeightedIntTrs

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

        ↳12 WeightedIntTrs

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

        ↳14 WeightedIntTrs

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

        ↳16 WeightedIntTrs

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

        ↳18 WeightedIntTrs

    ↳19 JBCGraphEdgesToCpxIntTrsProof (CONCRETE UPPER BOUND(ID), 109 ms)

    ↳20 WeightedIntTrs

        ↳21 StraightLineCodeCompressionProof (BOTH CONCRETE BOUNDS(ID, ID), 54 ms)

        ↳22 WeightedIntTrs

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

        ↳24 WeightedIntTrs

        ↳25 LinearizedLhssProof (BOTH CONCRETE BOUNDS(ID, ID), 0 ms)

        ↳26 WeightedIntTrs

        ↳27 RemoveDivModProof (CONCRETE UPPER BOUND(ID), 0 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 TerminationGraphToComplexityProof (BOTH CONCRETE BOUNDS(ID, ADD(3)), 0 ms)

↳34 JBCComplexityEdges

    ↳35 JBCGraphEdgesToCpxIntTrsProof (CONCRETE UPPER BOUND(ID), 69 ms)

    ↳36 WeightedIntTrs

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

    ↳38 WeightedIntTrs

    ↳39 WeightedIntTrsUnneededArgumentFilterProof (CONCRETE UPPER BOUND(ID), 36 ms)

    ↳40 WeightedIntTrs

    ↳41 LinearizedLhssProof (BOTH CONCRETE BOUNDS(ID, ID), 0 ms)

    ↳42 WeightedIntTrs

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

    ↳44 WeightedIntTrs

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

    ↳46 WeightedIntTrs

    ↳47 koat Proof (⇔, 232 ms)

    ↳48 BOUNDS(CONSTANT, 381 + 37 * |#0|)

(0) Obligation:

Need to prove time_complexity of the following program:

public class Et4 {
    public static void main(int a, int b, int c) {
	   	while ( (b - c >= 1) && (a == c)) {
                    int r =  new Object().hashCode();
                    if (r < 0) r = -r;
	   		b = 10;
	   		c = c + 1 + r;
	   	    a = c;
	   	}
    }
}

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

Constructed TerminationGraph.

(2) Obligation:

Termination Graph based on JBC Program:
Et4.main(III)V: Graph of 71 nodes with 1 SCC.

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

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

(4) Obligation:

Set of 69 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 69 jbc graph edges to a weighted ITS with 69 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.

(6) Obligation:

IntTrs with 69 rules
Start term: main_Load_1(#0, #1, #2, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_Load_1(i1, i3, i5, env, static) -{0,0}> main_Load_4(i1, i3, i5, env, static) :|: 0 >= 0
main_Load_4(i1, i3, i5, env, static) -{0,0}> langle_clinit_rangle_ConstantStackPush_6(i1, i3, i5, env, static) :|: 0 >= 0
langle_clinit_rangle_ConstantStackPush_6(i1, i3, i5, env, static) -{1,1}> langle_clinit_rangle_ArrayCreate_12(iconst_0, i1, i3, i5, env, static) :|: iconst_0 = 0
langle_clinit_rangle_ArrayCreate_12(iconst_0, i1, i3, i5, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_14(a2, i1, i3, i5, iconst_0, env, static) :|: a2 = 2 && iconst_0 = 0 && 0 < a2
langle_clinit_rangle_FieldAccess_14(a2, i1, i3, i5, iconst_0, env, static) -{1,1}> langle_clinit_rangle_New_16(i1, i3, i5, env, static') :|: 0 <= a2 && iconst_0 = 0 && static' <= static + a2 && 0 <= static && 0 < a2
langle_clinit_rangle_New_16(i1, i3, i5, env, static) -{0,0}> langle_clinit_rangle_New_18(i1, i3, i5, env, static) :|: 0 >= 0
langle_clinit_rangle_New_18(i1, i3, i5, env, static) -{0,0}> langle_clinit_rangle_New_19(i1, i3, i5, env, static) :|: 0 <= static
langle_clinit_rangle_New_19(i1, i3, i5, env, static) -{1,1}> langle_clinit_rangle_Duplicate_20(o2, i1, i3, i5, env, static) :|: 0 < o2 && o2 = 1
langle_clinit_rangle_Duplicate_20(o2, i1, i3, i5, env, static) -{1,1}> langle_clinit_rangle_ConstantStackPush_22(o2, i1, i3, i5, env, static) :|: 0 < o2
langle_clinit_rangle_ConstantStackPush_22(o2, i1, i3, i5, env, static) -{1,1}> langle_clinit_rangle_InvokeMethod_23(o2, NULL, i1, i3, i5, env, static) :|: NULL = 0 && 0 < o2
langle_clinit_rangle_InvokeMethod_23(o2, NULL, i1, i3, i5, env, static) -{1,1}> langle_init_rangle_Load_25(o2, i1, i3, i5, env, static) :|: NULL = 0 && 0 < o2
langle_init_rangle_Load_25(o2, i1, i3, i5, env, static) -{1,1}> langle_init_rangle_InvokeMethod_26(o2, i1, i3, i5, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_26(o2, i1, i3, i5, env, static) -{1,1}> langle_init_rangle_Load_27(o2, i1, i3, i5, env, static) :|: 0 < o2
langle_init_rangle_Load_27(o2, i1, i3, i5, env, static) -{1,1}> langle_init_rangle_InvokeMethod_29(o2, i1, i3, i5, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_29(o2, i1, i3, i5, env, static) -{1,1}> langle_init_rangle_Return_31(o2, i1, i3, i5, env, static) :|: 0 < o2
langle_init_rangle_Return_31(o2, i1, i3, i5, env, static) -{1,1}> langle_init_rangle_Return_33(o2, i1, i3, i5, env, static) :|: 0 < o2
langle_init_rangle_Return_33(o2, i1, i3, i5, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_36(o2, i1, i3, i5, env, static) :|: 0 < o2
langle_clinit_rangle_FieldAccess_36(o2, i1, i3, i5, env, static) -{1,1}> langle_clinit_rangle_Return_38(i1, i3, i5, env, static') :|: 0 < o2 && 0 <= o2 && 0 <= static && static' <= static + o2
langle_clinit_rangle_Return_38(i1, i3, i5, env, static) -{1,1}> main_Load_41(i1, i3, i5, env, static) :|: 0 >= 0
main_Load_41(i1, i3, i5, env, static) -{0,0}> main_Load_42(i1, i3, i5, env, static) :|: 0 >= 0
main_Load_42(i1, i3, i5, env, static) -{0,0}> main_Load_44(i1, i3, i5, env, static) :|: 0 <= static
main_Load_44(i1, i3, i5, env, static) -{0,0}> main_Load_45(i1, i3, i5, env, static) :|: 0 >= 0
main_Load_45(i1, i3, i5, env, static) -{0,0}> main_Load_47(i1, i3, i5, env, static) :|: 0 >= 0
main_Load_47(i1, i3, i5, env, static) -{0,0}> main_Load_181(i1, i3, i5, i1, i3, i5, env, static) :|: 0 >= 0
main_Load_181(i48, i3, i5, i49, i50, i51, env, static) -{1,1}> main_Load_183(i48, i3, i5, i50, i49, i51, env, static) :|: 0 >= 0
main_Load_183(i48, i3, i5, i50, i49, i51, env, static) -{1,1}> main_IntArithmetic_184(i48, i3, i5, i50, i51, i49, env, static) :|: 0 >= 0
main_IntArithmetic_184(i48, i3, i5, i50, i51, i49, env, static) -{1,1}> main_ConstantStackPush_185(i48, i3, i5, i61, i49, i51, env, static) :|: i50 - i51 = i61
main_ConstantStackPush_185(i48, i3, i5, i61, i49, i51, env, static) -{1,1}> main_LT_192(i48, i3, i5, i61, iconst_1, i49, i51, env, static) :|: iconst_1 = 1
main_LT_192(i48, i3, i5, i69, iconst_1, i49, i51, env, static) -{0,0}> main_LT_196(i48, i3, i5, i69, iconst_1, i49, i51, env, static) :|: iconst_1 = 1 && i69 <= 0
main_LT_192(i48, i3, i5, i71, iconst_1, i49, i51, env, static) -{0,0}> main_LT_198(i48, i3, i5, i71, iconst_1, i49, i51, env, static) :|: iconst_1 = 1 && 1 <= i71
main_LT_198(i48, i3, i5, i71, iconst_1, i49, i51, env, static) -{1,1}> main_Load_230(i48, i3, i5, i49, i51, env, static) :|: iconst_1 <= i71 && iconst_1 = 1 && 1 <= i71
main_Load_230(i48, i3, i5, i49, i51, env, static) -{1,1}> main_Load_240(i48, i3, i5, i49, i51, env, static) :|: 0 >= 0
main_Load_240(i48, i3, i5, i49, i51, env, static) -{1,1}> main_NE_267(i48, i3, i5, i49, i51, env, static) :|: 0 >= 0
main_NE_267(i48, i3, i5, i49, i51, env, static) -{0,0}> main_NE_268(i48, i3, i5, i49, i51, env, static) :|: !(i49 = i51)
main_NE_267(i48, i3, i5, i49, i51, env, static) -{0,0}> main_NE_269(i48, i3, i5, i51, env, static) :|: i49 = i51
main_NE_269(i48, i3, i5, i51, env, static) -{1,1}> main_New_278(i48, i3, i5, i51, env, static) :|: i51 = i51
main_New_278(i48, i3, i5, i51, env, static) -{1,1}> main_Duplicate_282(i48, i3, i5, o21, i51, env, static) :|: o21 = 1 && 0 < o21
main_Duplicate_282(i48, i3, i5, o21, i51, env, static) -{1,1}> main_InvokeMethod_283(i48, i3, i5, o21, i51, env, static) :|: 0 < o21
main_InvokeMethod_283(i48, i3, i5, o21, i51, env, static) -{1,1}> main_InvokeMethod_286(i48, i3, i5, o21, i51, env, static) :|: 0 < o21
main_InvokeMethod_286(i48, i3, i5, o21, i51, env, static) -{1,1}> main_Store_288(i48, i3, i5, i92, i51, env, static) :|: 0 < o21
main_Store_288(i48, i3, i5, i92, i51, env, static) -{1,1}> main_Load_290(i48, i3, i5, i51, i92, env, static) :|: 0 >= 0
main_Load_290(i48, i3, i5, i51, i92, env, static) -{1,1}> main_GE_291(i48, i3, i5, i92, i51, env, static) :|: 0 >= 0
main_GE_291(i48, i3, i5, i98, i51, env, static) -{0,0}> main_GE_292(i48, i3, i5, i98, i51, env, static) :|: i98 <= -1
main_GE_291(i48, i3, i5, i99, i51, env, static) -{0,0}> main_GE_293(i48, i3, i5, i99, i51, env, static) :|: 0 <= i99
main_GE_292(i48, i3, i5, i98, i51, env, static) -{1,1}> main_Load_294(i48, i3, i5, i51, i98, env, static) :|: i98 <= -1 && i98 < 0
main_GE_293(i48, i3, i5, i99, i51, env, static) -{1,1}> main_ConstantStackPush_296(i48, i3, i5, i51, i99, env, static) :|: 0 <= i99
main_Load_294(i48, i3, i5, i51, i98, env, static) -{1,1}> main_IntArithmetic_297(i48, i3, i5, i98, i51, env, static) :|: i98 <= -1
main_ConstantStackPush_296(i48, i3, i5, i51, i99, env, static) -{1,1}> main_Store_298(i48, i3, i5, iconst_10, i51, i99, env, static) :|: iconst_10 = 10 && 0 <= i99
main_IntArithmetic_297(i48, i3, i5, i98, i51, env, static) -{1,1}> main_Store_299(i48, i3, i5, i100, i51, env, static) :|: i98 <= -1 && -i98 = i100 && 1 <= i100
main_Store_298(i48, i3, i5, iconst_10, i51, i99, env, static) -{1,1}> main_Load_300(i48, i3, i5, iconst_10, i51, i99, env, static) :|: iconst_10 = 10 && 0 <= i99
main_Store_299(i48, i3, i5, i100, i51, env, static) -{1,1}> main_ConstantStackPush_301(i48, i3, i5, i51, i100, env, static) :|: 1 <= i100
main_Load_300(i48, i3, i5, iconst_10, i51, i99, env, static) -{1,1}> main_ConstantStackPush_302(i48, i3, i5, i51, iconst_10, i99, env, static) :|: iconst_10 = 10 && 0 <= i99
main_ConstantStackPush_301(i48, i3, i5, i51, i100, env, static) -{1,1}> main_Store_304(i48, i3, i5, iconst_10, i51, i100, env, static) :|: iconst_10 = 10 && 1 <= i100
main_ConstantStackPush_302(i48, i3, i5, i51, iconst_10, i99, env, static) -{1,1}> main_IntArithmetic_305(i48, i3, i5, i51, iconst_1, iconst_10, i99, env, static) :|: iconst_1 = 1 && iconst_10 = 10 && 0 <= i99
main_Store_304(i48, i3, i5, iconst_10, i51, i100, env, static) -{1,1}> main_Load_306(i48, i3, i5, iconst_10, i51, i100, env, static) :|: iconst_10 = 10 && 1 <= i100
main_IntArithmetic_305(i48, i3, i5, i51, iconst_1, iconst_10, i99, env, static) -{1,1}> main_Load_308(i48, i3, i5, i101, iconst_10, i99, env, static) :|: i51 + iconst_1 = i101 && iconst_1 = 1 && iconst_10 = 10 && 0 <= i99
main_Load_306(i48, i3, i5, iconst_10, i51, i100, env, static) -{1,1}> main_ConstantStackPush_309(i48, i3, i5, i51, iconst_10, i100, env, static) :|: iconst_10 = 10 && 1 <= i100
main_Load_308(i48, i3, i5, i101, iconst_10, i99, env, static) -{1,1}> main_IntArithmetic_310(i48, i3, i5, i101, i99, iconst_10, env, static) :|: iconst_10 = 10 && 0 <= i99
main_ConstantStackPush_309(i48, i3, i5, i51, iconst_10, i100, env, static) -{1,1}> main_IntArithmetic_311(i48, i3, i5, i51, iconst_1, iconst_10, i100, env, static) :|: iconst_1 = 1 && iconst_10 = 10 && 1 <= i100
main_IntArithmetic_310(i48, i3, i5, i101, i99, iconst_10, env, static) -{1,1}> main_Store_312(i48, i3, i5, i102, iconst_10, env, static) :|: iconst_10 = 10 && 0 <= i99 && i101 + i99 = i102
main_IntArithmetic_311(i48, i3, i5, i51, iconst_1, iconst_10, i100, env, static) -{1,1}> main_Load_314(i48, i3, i5, i103, iconst_10, i100, env, static) :|: iconst_1 = 1 && iconst_10 = 10 && i51 + iconst_1 = i103 && 1 <= i100
main_Store_312(i48, i3, i5, i102, iconst_10, env, static) -{0,0}> main_Store_325(i48, i3, i5, i102, iconst_10, env, static) :|: iconst_10 = 10
main_Load_314(i48, i3, i5, i103, iconst_10, i100, env, static) -{1,1}> main_IntArithmetic_317(i48, i3, i5, i103, i100, iconst_10, env, static) :|: iconst_10 = 10 && 1 <= i100
main_IntArithmetic_317(i48, i3, i5, i103, i100, iconst_10, env, static) -{1,1}> main_Store_325(i48, i3, i5, i104, iconst_10, env, static) :|: iconst_10 = 10 && 1 <= i100 && i103 + i100 = i104
main_Store_325(i48, i3, i5, i104, iconst_10, env, static) -{1,1}> main_Load_326(i48, i3, i5, iconst_10, i104, env, static) :|: iconst_10 = 10
main_Load_326(i48, i3, i5, iconst_10, i104, env, static) -{1,1}> main_Store_329(i48, i3, i5, i104, iconst_10, env, static) :|: iconst_10 = 10
main_Store_329(i48, i3, i5, i104, iconst_10, env, static) -{1,1}> main_JMP_331(i48, i3, i5, i104, iconst_10, env, static) :|: iconst_10 = 10
main_JMP_331(i48, i3, i5, i104, iconst_10, env, static) -{1,1}> main_Load_334(i48, i3, i5, i104, iconst_10, env, static) :|: iconst_10 = 10
main_Load_334(i48, i3, i5, i104, iconst_10, env, static) -{0,0}> main_Load_181(i48, i3, i5, i104, iconst_10, i104, env, static) :|: iconst_10 = 10

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

obtained
main_Load_1(i1, i3, i5, env, static) -{15,15}> main_Load_181(i1, i3, i5, i1, i3, i5, env, static'1) :|: 0 >= 0 && static'1 <= static''' + 1 && 0 <= 2 && 0 <= static''' && static''' <= static + 2 && 0 < 1 && 0 <= 1 && 0 <= static && 0 <= static'1 && 0 < 2
by chaining
main_Load_1(i1, i3, i5, env, static) -{0,0}> main_Load_4(i1, i3, i5, env, static) :|: 0 >= 0
main_Load_4(i1, i3, i5, env, static) -{0,0}> langle_clinit_rangle_ConstantStackPush_6(i1, i3, i5, env, static) :|: 0 >= 0
langle_clinit_rangle_ConstantStackPush_6(i1, i3, i5, env, static) -{1,1}> langle_clinit_rangle_ArrayCreate_12(iconst_0, i1, i3, i5, env, static) :|: iconst_0 = 0
langle_clinit_rangle_ArrayCreate_12(iconst_0, i1, i3, i5, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_14(a2, i1, i3, i5, iconst_0, env, static) :|: a2 = 2 && iconst_0 = 0 && 0 < a2
langle_clinit_rangle_FieldAccess_14(a2, i1, i3, i5, iconst_0, env, static) -{1,1}> langle_clinit_rangle_New_16(i1, i3, i5, env, static') :|: 0 <= a2 && iconst_0 = 0 && static' <= static + a2 && 0 <= static && 0 < a2
langle_clinit_rangle_New_16(i1, i3, i5, env, static) -{0,0}> langle_clinit_rangle_New_18(i1, i3, i5, env, static) :|: 0 >= 0
langle_clinit_rangle_New_18(i1, i3, i5, env, static) -{0,0}> langle_clinit_rangle_New_19(i1, i3, i5, env, static) :|: 0 <= static
langle_clinit_rangle_New_19(i1, i3, i5, env, static) -{1,1}> langle_clinit_rangle_Duplicate_20(o2, i1, i3, i5, env, static) :|: 0 < o2 && o2 = 1
langle_clinit_rangle_Duplicate_20(o2, i1, i3, i5, env, static) -{1,1}> langle_clinit_rangle_ConstantStackPush_22(o2, i1, i3, i5, env, static) :|: 0 < o2
langle_clinit_rangle_ConstantStackPush_22(o2, i1, i3, i5, env, static) -{1,1}> langle_clinit_rangle_InvokeMethod_23(o2, NULL, i1, i3, i5, env, static) :|: NULL = 0 && 0 < o2
langle_clinit_rangle_InvokeMethod_23(o2, NULL, i1, i3, i5, env, static) -{1,1}> langle_init_rangle_Load_25(o2, i1, i3, i5, env, static) :|: NULL = 0 && 0 < o2
langle_init_rangle_Load_25(o2, i1, i3, i5, env, static) -{1,1}> langle_init_rangle_InvokeMethod_26(o2, i1, i3, i5, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_26(o2, i1, i3, i5, env, static) -{1,1}> langle_init_rangle_Load_27(o2, i1, i3, i5, env, static) :|: 0 < o2
langle_init_rangle_Load_27(o2, i1, i3, i5, env, static) -{1,1}> langle_init_rangle_InvokeMethod_29(o2, i1, i3, i5, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_29(o2, i1, i3, i5, env, static) -{1,1}> langle_init_rangle_Return_31(o2, i1, i3, i5, env, static) :|: 0 < o2
langle_init_rangle_Return_31(o2, i1, i3, i5, env, static) -{1,1}> langle_init_rangle_Return_33(o2, i1, i3, i5, env, static) :|: 0 < o2
langle_init_rangle_Return_33(o2, i1, i3, i5, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_36(o2, i1, i3, i5, env, static) :|: 0 < o2
langle_clinit_rangle_FieldAccess_36(o2, i1, i3, i5, env, static) -{1,1}> langle_clinit_rangle_Return_38(i1, i3, i5, env, static') :|: 0 < o2 && 0 <= o2 && 0 <= static && static' <= static + o2
langle_clinit_rangle_Return_38(i1, i3, i5, env, static) -{1,1}> main_Load_41(i1, i3, i5, env, static) :|: 0 >= 0
main_Load_41(i1, i3, i5, env, static) -{0,0}> main_Load_42(i1, i3, i5, env, static) :|: 0 >= 0
main_Load_42(i1, i3, i5, env, static) -{0,0}> main_Load_44(i1, i3, i5, env, static) :|: 0 <= static
main_Load_44(i1, i3, i5, env, static) -{0,0}> main_Load_45(i1, i3, i5, env, static) :|: 0 >= 0
main_Load_45(i1, i3, i5, env, static) -{0,0}> main_Load_47(i1, i3, i5, env, static) :|: 0 >= 0
main_Load_47(i1, i3, i5, env, static) -{0,0}> main_Load_181(i1, i3, i5, i1, i3, i5, env, static) :|: 0 >= 0

obtained
main_Load_181(i48, i3, i5, i49, i50, i51, env, static) -{4,4}> main_LT_192(i48, i3, i5, i61', 1, i49, i51, env, static) :|: 0 >= 0 && i50 - i51 = i61'
by chaining
main_Load_181(i48, i3, i5, i49, i50, i51, env, static) -{1,1}> main_Load_183(i48, i3, i5, i50, i49, i51, env, static) :|: 0 >= 0
main_Load_183(i48, i3, i5, i50, i49, i51, env, static) -{1,1}> main_IntArithmetic_184(i48, i3, i5, i50, i51, i49, env, static) :|: 0 >= 0
main_IntArithmetic_184(i48, i3, i5, i50, i51, i49, env, static) -{1,1}> main_ConstantStackPush_185(i48, i3, i5, i61, i49, i51, env, static) :|: i50 - i51 = i61
main_ConstantStackPush_185(i48, i3, i5, i61, i49, i51, env, static) -{1,1}> main_LT_192(i48, i3, i5, i61, iconst_1, i49, i51, env, static) :|: iconst_1 = 1

obtained
main_LT_192(i48, i3, i5, i71, 1, i49, i51, env, static) -{3,3}> main_NE_267(i48, i3, i5, i49, i51, env, static) :|: 0 >= 0 && 1 <= i71
by chaining
main_LT_192(i48, i3, i5, i71, iconst_1, i49, i51, env, static) -{0,0}> main_LT_198(i48, i3, i5, i71, iconst_1, i49, i51, env, static) :|: iconst_1 = 1 && 1 <= i71
main_LT_198(i48, i3, i5, i71, iconst_1, i49, i51, env, static) -{1,1}> main_Load_230(i48, i3, i5, i49, i51, env, static) :|: iconst_1 <= i71 && iconst_1 = 1 && 1 <= i71
main_Load_230(i48, i3, i5, i49, i51, env, static) -{1,1}> main_Load_240(i48, i3, i5, i49, i51, env, static) :|: 0 >= 0
main_Load_240(i48, i3, i5, i49, i51, env, static) -{1,1}> main_NE_267(i48, i3, i5, i49, i51, env, static) :|: 0 >= 0

obtained
main_NE_267(i48, i3, i5, i49, i49, env, static) -{7,7}> main_GE_291(i48, i3, i5, i92', i49, env, static) :|: 0 >= 0 && 0 < 1
by chaining
main_NE_267(i48, i3, i5, i49, i51, env, static) -{0,0}> main_NE_269(i48, i3, i5, i51, env, static) :|: i49 = i51
main_NE_269(i48, i3, i5, i51, env, static) -{1,1}> main_New_278(i48, i3, i5, i51, env, static) :|: i51 = i51
main_New_278(i48, i3, i5, i51, env, static) -{1,1}> main_Duplicate_282(i48, i3, i5, o21, i51, env, static) :|: o21 = 1 && 0 < o21
main_Duplicate_282(i48, i3, i5, o21, i51, env, static) -{1,1}> main_InvokeMethod_283(i48, i3, i5, o21, i51, env, static) :|: 0 < o21
main_InvokeMethod_283(i48, i3, i5, o21, i51, env, static) -{1,1}> main_InvokeMethod_286(i48, i3, i5, o21, i51, env, static) :|: 0 < o21
main_InvokeMethod_286(i48, i3, i5, o21, i51, env, static) -{1,1}> main_Store_288(i48, i3, i5, i92, i51, env, static) :|: 0 < o21
main_Store_288(i48, i3, i5, i92, i51, env, static) -{1,1}> main_Load_290(i48, i3, i5, i51, i92, env, static) :|: 0 >= 0
main_Load_290(i48, i3, i5, i51, i92, env, static) -{1,1}> main_GE_291(i48, i3, i5, i92, i51, env, static) :|: 0 >= 0

obtained
main_GE_291(i48, i3, i5, i99, i51, env, static) -{8,8}> main_Store_325(i48, i3, i5, i102', 10, env, static) :|: i101' + i99 = i102' && 0 <= i99 && i51 + 1 = i101'
by chaining
main_GE_291(i48, i3, i5, i99, i51, env, static) -{0,0}> main_GE_293(i48, i3, i5, i99, i51, env, static) :|: 0 <= i99
main_GE_293(i48, i3, i5, i99, i51, env, static) -{1,1}> main_ConstantStackPush_296(i48, i3, i5, i51, i99, env, static) :|: 0 <= i99
main_ConstantStackPush_296(i48, i3, i5, i51, i99, env, static) -{1,1}> main_Store_298(i48, i3, i5, iconst_10, i51, i99, env, static) :|: iconst_10 = 10 && 0 <= i99
main_Store_298(i48, i3, i5, iconst_10, i51, i99, env, static) -{1,1}> main_Load_300(i48, i3, i5, iconst_10, i51, i99, env, static) :|: iconst_10 = 10 && 0 <= i99
main_Load_300(i48, i3, i5, iconst_10, i51, i99, env, static) -{1,1}> main_ConstantStackPush_302(i48, i3, i5, i51, iconst_10, i99, env, static) :|: iconst_10 = 10 && 0 <= i99
main_ConstantStackPush_302(i48, i3, i5, i51, iconst_10, i99, env, static) -{1,1}> main_IntArithmetic_305(i48, i3, i5, i51, iconst_1, iconst_10, i99, env, static) :|: iconst_1 = 1 && iconst_10 = 10 && 0 <= i99
main_IntArithmetic_305(i48, i3, i5, i51, iconst_1, iconst_10, i99, env, static) -{1,1}> main_Load_308(i48, i3, i5, i101, iconst_10, i99, env, static) :|: i51 + iconst_1 = i101 && iconst_1 = 1 && iconst_10 = 10 && 0 <= i99
main_Load_308(i48, i3, i5, i101, iconst_10, i99, env, static) -{1,1}> main_IntArithmetic_310(i48, i3, i5, i101, i99, iconst_10, env, static) :|: iconst_10 = 10 && 0 <= i99
main_IntArithmetic_310(i48, i3, i5, i101, i99, iconst_10, env, static) -{1,1}> main_Store_312(i48, i3, i5, i102, iconst_10, env, static) :|: iconst_10 = 10 && 0 <= i99 && i101 + i99 = i102
main_Store_312(i48, i3, i5, i102, iconst_10, env, static) -{0,0}> main_Store_325(i48, i3, i5, i102, iconst_10, env, static) :|: iconst_10 = 10

obtained
main_Store_325(i48, i3, i5, i104, 10, env, static) -{4,4}> main_Load_181(i48, i3, i5, i104, 10, i104, env, static) :|: 0 >= 0
by chaining
main_Store_325(i48, i3, i5, i104, iconst_10, env, static) -{1,1}> main_Load_326(i48, i3, i5, iconst_10, i104, env, static) :|: iconst_10 = 10
main_Load_326(i48, i3, i5, iconst_10, i104, env, static) -{1,1}> main_Store_329(i48, i3, i5, i104, iconst_10, env, static) :|: iconst_10 = 10
main_Store_329(i48, i3, i5, i104, iconst_10, env, static) -{1,1}> main_JMP_331(i48, i3, i5, i104, iconst_10, env, static) :|: iconst_10 = 10
main_JMP_331(i48, i3, i5, i104, iconst_10, env, static) -{1,1}> main_Load_334(i48, i3, i5, i104, iconst_10, env, static) :|: iconst_10 = 10
main_Load_334(i48, i3, i5, i104, iconst_10, env, static) -{0,0}> main_Load_181(i48, i3, i5, i104, iconst_10, i104, env, static) :|: iconst_10 = 10

obtained
main_GE_291(i48, i3, i5, i98, i51, env, static) -{11,11}> main_Store_325(i48, i3, i5, i1043, 10, env, static) :|: i98 < 0 && i103' + i100' = i1043 && i98 <= -1 && 1 <= i100' && i51 + 1 = i103' && -i98 = i100'
by chaining
main_GE_291(i48, i3, i5, i98, i51, env, static) -{0,0}> main_GE_292(i48, i3, i5, i98, i51, env, static) :|: i98 <= -1
main_GE_292(i48, i3, i5, i98, i51, env, static) -{1,1}> main_Load_294(i48, i3, i5, i51, i98, env, static) :|: i98 <= -1 && i98 < 0
main_Load_294(i48, i3, i5, i51, i98, env, static) -{1,1}> main_IntArithmetic_297(i48, i3, i5, i98, i51, env, static) :|: i98 <= -1
main_IntArithmetic_297(i48, i3, i5, i98, i51, env, static) -{1,1}> main_Store_299(i48, i3, i5, i100, i51, env, static) :|: i98 <= -1 && -i98 = i100 && 1 <= i100
main_Store_299(i48, i3, i5, i100, i51, env, static) -{1,1}> main_ConstantStackPush_301(i48, i3, i5, i51, i100, env, static) :|: 1 <= i100
main_ConstantStackPush_301(i48, i3, i5, i51, i100, env, static) -{1,1}> main_Store_304(i48, i3, i5, iconst_10, i51, i100, env, static) :|: iconst_10 = 10 && 1 <= i100
main_Store_304(i48, i3, i5, iconst_10, i51, i100, env, static) -{1,1}> main_Load_306(i48, i3, i5, iconst_10, i51, i100, env, static) :|: iconst_10 = 10 && 1 <= i100
main_Load_306(i48, i3, i5, iconst_10, i51, i100, env, static) -{1,1}> main_ConstantStackPush_309(i48, i3, i5, i51, iconst_10, i100, env, static) :|: iconst_10 = 10 && 1 <= i100
main_ConstantStackPush_309(i48, i3, i5, i51, iconst_10, i100, env, static) -{1,1}> main_IntArithmetic_311(i48, i3, i5, i51, iconst_1, iconst_10, i100, env, static) :|: iconst_1 = 1 && iconst_10 = 10 && 1 <= i100
main_IntArithmetic_311(i48, i3, i5, i51, iconst_1, iconst_10, i100, env, static) -{1,1}> main_Load_314(i48, i3, i5, i103, iconst_10, i100, env, static) :|: iconst_1 = 1 && iconst_10 = 10 && i51 + iconst_1 = i103 && 1 <= i100
main_Load_314(i48, i3, i5, i103, iconst_10, i100, env, static) -{1,1}> main_IntArithmetic_317(i48, i3, i5, i103, i100, iconst_10, env, static) :|: iconst_10 = 10 && 1 <= i100
main_IntArithmetic_317(i48, i3, i5, i103, i100, iconst_10, env, static) -{1,1}> main_Store_325(i48, i3, i5, i104, iconst_10, env, static) :|: iconst_10 = 10 && 1 <= i100 && i103 + i100 = i104

(8) Obligation:

IntTrs with 9 rules
Start term: main_Load_1(#0, #1, #2, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_Load_1(i1, i3, i5, env, static) -{15,15}> main_Load_181(i1, i3, i5, i1, i3, i5, 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_Load_181(i48, i3, i5, i49, i50, i51, env, static) -{4,4}> main_LT_192(i48, i3, i5, i61', 1, i49, i51, env, static) :|: 0 >= 0 && i50 - i51 = i61'
main_LT_192(i48, i3, i5, i69, iconst_1, i49, i51, env, static) -{0,0}> main_LT_196(i48, i3, i5, i69, iconst_1, i49, i51, env, static) :|: iconst_1 = 1 && i69 <= 0
main_LT_192(i48, i3, i5, i71, 1, i49, i51, env, static) -{3,3}> main_NE_267(i48, i3, i5, i49, i51, env, static) :|: 0 >= 0 && 1 <= i71
main_NE_267(i48, i3, i5, i49, i51, env, static) -{0,0}> main_NE_268(i48, i3, i5, i49, i51, env, static) :|: !(i49 = i51)
main_NE_267(i48, i3, i5, i49, i49, env, static) -{7,7}> main_GE_291(i48, i3, i5, i92', i49, env, static) :|: 0 >= 0 && 0 < 1
main_GE_291(i48, i3, i5, i99, i51, env, static) -{8,8}> main_Store_325(i48, i3, i5, i102', 10, env, static) :|: i101' + i99 = i102' && 0 <= i99 && i51 + 1 = i101'
main_Store_325(i48, i3, i5, i104, 10, env, static) -{4,4}> main_Load_181(i48, i3, i5, i104, 10, i104, env, static) :|: 0 >= 0
main_GE_291(i48, i3, i5, i98, i51, env, static) -{11,11}> main_Store_325(i48, i3, i5, i1043, 10, env, static) :|: i98 < 0 && i103' + i100' = i1043 && i98 <= -1 && 1 <= i100' && i51 + 1 = i103' && -i98 = i100'

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

Moved arithmethic from lhss to constraints.

main_Store_325(i48, i3, i5, i104, 10, env, static) -{4,4}> main_Load_181(i48, i3, i5, i104, 10, i104, env, static) :|: 0 >= 0
was transformed to
main_Store_325(i48, i3, i5, i104, x, env, static) -{4,4}> main_Load_181(i48, i3, i5, i104, 10, i104, env, static) :|: 0 >= 0 && x = 10

main_LT_192(i48, i3, i5, i71, 1, i49, i51, env, static) -{3,3}> main_NE_267(i48, i3, i5, i49, i51, env, static) :|: 0 >= 0 && 1 <= i71
was transformed to
main_LT_192(i48, i3, i5, i71, x, i49, i51, env, static) -{3,3}> main_NE_267(i48, i3, i5, i49, i51, env, static) :|: 0 >= 0 && 1 <= i71 && x = 1

(10) Obligation:

IntTrs with 9 rules
Start term: main_Load_1(#0, #1, #2, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_GE_291(i48, i3, i5, i99, i51, env, static) -{8,8}> main_Store_325(i48, i3, i5, i102', 10, env, static) :|: i101' + i99 = i102' && 0 <= i99 && i51 + 1 = i101'
main_NE_267(i48, i3, i5, i49, i51, env, static) -{0,0}> main_NE_268(i48, i3, i5, i49, i51, env, static) :|: !(i49 = i51)
main_Load_1(i1, i3, i5, env, static) -{15,15}> main_Load_181(i1, i3, i5, i1, i3, i5, 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_Store_325(i48, i3, i5, i104, x, env, static) -{4,4}> main_Load_181(i48, i3, i5, i104, 10, i104, env, static) :|: 0 >= 0 && x = 10
main_LT_192(i48, i3, i5, i71, x, i49, i51, env, static) -{3,3}> main_NE_267(i48, i3, i5, i49, i51, env, static) :|: 0 >= 0 && 1 <= i71 && x = 1
main_NE_267(i48, i3, i5, i49, i49, env, static) -{7,7}> main_GE_291(i48, i3, i5, i92', i49, env, static) :|: 0 >= 0 && 0 < 1
main_LT_192(i48, i3, i5, i69, iconst_1, i49, i51, env, static) -{0,0}> main_LT_196(i48, i3, i5, i69, iconst_1, i49, i51, env, static) :|: iconst_1 = 1 && i69 <= 0
main_Load_181(i48, i3, i5, i49, i50, i51, env, static) -{4,4}> main_LT_192(i48, i3, i5, i61', 1, i49, i51, env, static) :|: 0 >= 0 && i50 - i51 = i61'
main_GE_291(i48, i3, i5, i98, i51, env, static) -{11,11}> main_Store_325(i48, i3, i5, i1043, 10, env, static) :|: i98 < 0 && i103' + i100' = i1043 && i98 <= -1 && 1 <= i100' && i51 + 1 = i103' && -i98 = i100'

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

Linearized lhss.

main_NE_267(i48, i3, i5, i49, i49, env, static) -{7,7}> main_GE_291(i48, i3, i5, i92', i49, env, static) :|: 0 >= 0 && 0 < 1
was transformed to
main_NE_267(i48, i3, i5, i49, x, env, static) -{7,7}> main_GE_291(i48, i3, i5, i92', i49, env, static) :|: 0 >= 0 && 0 < 1 && x = i49

(12) Obligation:

IntTrs with 9 rules
Start term: main_Load_1(#0, #1, #2, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_NE_267(i48, i3, i5, i49, i51, env, static) -{0,0}> main_NE_268(i48, i3, i5, i49, i51, env, static) :|: !(i49 = i51)
main_GE_291(i48, i3, i5, i99, i51, env, static) -{8,8}> main_Store_325(i48, i3, i5, i102', 10, env, static) :|: i101' + i99 = i102' && 0 <= i99 && i51 + 1 = i101'
main_LT_192(i48, i3, i5, i71, x, i49, i51, env, static) -{3,3}> main_NE_267(i48, i3, i5, i49, i51, env, static) :|: 0 >= 0 && 1 <= i71 && x = 1
main_Load_1(i1, i3, i5, env, static) -{15,15}> main_Load_181(i1, i3, i5, i1, i3, i5, 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_192(i48, i3, i5, i69, iconst_1, i49, i51, env, static) -{0,0}> main_LT_196(i48, i3, i5, i69, iconst_1, i49, i51, env, static) :|: iconst_1 = 1 && i69 <= 0
main_NE_267(i48, i3, i5, i49, x, env, static) -{7,7}> main_GE_291(i48, i3, i5, i92', i49, env, static) :|: 0 >= 0 && 0 < 1 && x = i49
main_Store_325(i48, i3, i5, i104, x, env, static) -{4,4}> main_Load_181(i48, i3, i5, i104, 10, i104, env, static) :|: 0 >= 0 && x = 10
main_Load_181(i48, i3, i5, i49, i50, i51, env, static) -{4,4}> main_LT_192(i48, i3, i5, i61', 1, i49, i51, env, static) :|: 0 >= 0 && i50 - i51 = i61'
main_GE_291(i48, i3, i5, i98, i51, env, static) -{11,11}> main_Store_325(i48, i3, i5, i1043, 10, env, static) :|: i98 < 0 && i103' + i100' = i1043 && i98 <= -1 && 1 <= i100' && i51 + 1 = i103' && -i98 = i100'

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

Removed div and mod.

main_NE_267(i48, i3, i5, i49, i51, env, static) -{0,0}> main_NE_268(i48, i3, i5, i49, i51, env, static) :|: !(i49 = i51)
was transformed to
main_NE_267(i48, i3, i5, i49, i51, env, static) -{0,0}> main_NE_268(i48, i3, i5, i49, i51, env, static) :|: i49 < i51
main_NE_267(i48, i3, i5, i49, i51, env, static) -{0,0}> main_NE_268(i48, i3, i5, i49, i51, env, static) :|: i49 > i51

(14) Obligation:

IntTrs with 10 rules
Start term: main_Load_1(#0, #1, #2, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_GE_291(i48, i3, i5, i99, i51, env, static) -{8,8}> main_Store_325(i48, i3, i5, i102', 10, env, static) :|: i101' + i99 = i102' && 0 <= i99 && i51 + 1 = i101'
main_LT_192(i48, i3, i5, i71, x, i49, i51, env, static) -{3,3}> main_NE_267(i48, i3, i5, i49, i51, env, static) :|: 0 >= 0 && 1 <= i71 && x = 1
main_NE_267(i48, i3, i5, i49, i51, env, static) -{0,0}> main_NE_268(i48, i3, i5, i49, i51, env, static) :|: i49 < i51
main_Load_1(i1, i3, i5, env, static) -{15,15}> main_Load_181(i1, i3, i5, i1, i3, i5, 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_NE_267(i48, i3, i5, i49, i51, env, static) -{0,0}> main_NE_268(i48, i3, i5, i49, i51, env, static) :|: i49 > i51
main_NE_267(i48, i3, i5, i49, x, env, static) -{7,7}> main_GE_291(i48, i3, i5, i92', i49, env, static) :|: 0 >= 0 && 0 < 1 && x = i49
main_Store_325(i48, i3, i5, i104, x, env, static) -{4,4}> main_Load_181(i48, i3, i5, i104, 10, i104, env, static) :|: 0 >= 0 && x = 10
main_LT_192(i48, i3, i5, i69, iconst_1, i49, i51, env, static) -{0,0}> main_LT_196(i48, i3, i5, i69, iconst_1, i49, i51, env, static) :|: iconst_1 = 1 && i69 <= 0
main_Load_181(i48, i3, i5, i49, i50, i51, env, static) -{4,4}> main_LT_192(i48, i3, i5, i61', 1, i49, i51, env, static) :|: 0 >= 0 && i50 - i51 = i61'
main_GE_291(i48, i3, i5, i98, i51, env, static) -{11,11}> main_Store_325(i48, i3, i5, i1043, 10, env, static) :|: i98 < 0 && i103' + i100' = i1043 && i98 <= -1 && 1 <= i100' && i51 + 1 = i103' && -i98 = i100'

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

Moved arithmethic from constraints to rhss.

main_GE_291(i48, i3, i5, i99, i51, env, static) -{8,8}> main_Store_325(i48, i3, i5, i102', 10, env, static) :|: i101' + i99 = i102' && 0 <= i99 && i51 + 1 = i101'
was transformed to
main_GE_291(i48, i3, i5, i99, i51, env, static) -{8,8}> main_Store_325(i48, i3, i5, i101' + i99, 10, env, static) :|: i101' + i99 = i102' && 0 <= i99 && i51 + 1 = i101'

main_LT_192(i48, i3, i5, i69, iconst_1, i49, i51, env, static) -{0,0}> main_LT_196(i48, i3, i5, i69, iconst_1, i49, i51, env, static) :|: iconst_1 = 1 && i69 <= 0
was transformed to
main_LT_192(i48, i3, i5, i69, iconst_1, i49, i51, env, static) -{0,0}> main_LT_196(i48, i3, i5, i69, 1, i49, i51, env, static) :|: iconst_1 = 1 && i69 <= 0

main_Load_181(i48, i3, i5, i49, i50, i51, env, static) -{4,4}> main_LT_192(i48, i3, i5, i61', 1, i49, i51, env, static) :|: 0 >= 0 && i50 - i51 = i61'
was transformed to
main_Load_181(i48, i3, i5, i49, i50, i51, env, static) -{4,4}> main_LT_192(i48, i3, i5, i50 - i51, 1, i49, i51, env, static) :|: 0 >= 0 && i50 - i51 = i61'

main_GE_291(i48, i3, i5, i98, i51, env, static) -{11,11}> main_Store_325(i48, i3, i5, i1043, 10, env, static) :|: i98 < 0 && i103' + i100' = i1043 && i98 <= -1 && 1 <= i100' && i51 + 1 = i103' && -i98 = i100'
was transformed to
main_GE_291(i48, i3, i5, i98, i51, env, static) -{11,11}> main_Store_325(i48, i3, i5, i103' + i100', 10, env, static) :|: i98 < 0 && i103' + i100' = i1043 && i98 <= -1 && 1 <= i100' && i51 + 1 = i103' && -i98 = i100'

(16) Obligation:

IntTrs with 10 rules
Start term: main_Load_1(#0, #1, #2, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_GE_291(i48, i3, i5, i99, i51, env, static) -{8,8}> main_Store_325(i48, i3, i5, i101' + i99, 10, env, static) :|: i101' + i99 = i102' && 0 <= i99 && i51 + 1 = i101'
main_LT_192(i48, i3, i5, i71, x, i49, i51, env, static) -{3,3}> main_NE_267(i48, i3, i5, i49, i51, env, static) :|: 0 >= 0 && 1 <= i71 && x = 1
main_NE_267(i48, i3, i5, i49, i51, env, static) -{0,0}> main_NE_268(i48, i3, i5, i49, i51, env, static) :|: i49 < i51
main_Load_1(i1, i3, i5, env, static) -{15,15}> main_Load_181(i1, i3, i5, i1, i3, i5, 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_NE_267(i48, i3, i5, i49, i51, env, static) -{0,0}> main_NE_268(i48, i3, i5, i49, i51, env, static) :|: i49 > i51
main_NE_267(i48, i3, i5, i49, x, env, static) -{7,7}> main_GE_291(i48, i3, i5, i92', i49, env, static) :|: 0 >= 0 && 0 < 1 && x = i49
main_LT_192(i48, i3, i5, i69, iconst_1, i49, i51, env, static) -{0,0}> main_LT_196(i48, i3, i5, i69, 1, i49, i51, env, static) :|: iconst_1 = 1 && i69 <= 0
main_Store_325(i48, i3, i5, i104, x, env, static) -{4,4}> main_Load_181(i48, i3, i5, i104, 10, i104, env, static) :|: 0 >= 0 && x = 10
main_Load_181(i48, i3, i5, i49, i50, i51, env, static) -{4,4}> main_LT_192(i48, i3, i5, i50 - i51, 1, i49, i51, env, static) :|: 0 >= 0 && i50 - i51 = i61'
main_GE_291(i48, i3, i5, i98, i51, env, static) -{11,11}> main_Store_325(i48, i3, i5, i103' + i100', 10, env, static) :|: i98 < 0 && i103' + i100' = i1043 && i98 <= -1 && 1 <= i100' && i51 + 1 = i103' && -i98 = i100'

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

Simplified expressions.

main_GE_291(i48, i3, i5, i98, i51, env, static) -{11,11}> main_Store_325(i48, i3, i5, i103' + i100', 10, env, static) :|: i98 < 0 && i103' + i100' = i1043 && i98 <= -1 && 1 <= i100' && i51 + 1 = i103' && -i98 = i100'
was transformed to
main_GE_291(i48, i3, i5, i98, i51, env, static) -{11,11}> main_Store_325(i48, i3, i5, i103' + i100', 10, env, static) :|: i98 < 0 && i103' + i100' = i1043 && i98 <= -1 && 1 <= i100' && i51 + 1 = i103' && -1 * i98 = i100'

main_Load_181(i48, i3, i5, i49, i50, i51, env, static) -{4,4}> main_LT_192(i48, i3, i5, i50 - i51, 1, i49, i51, env, static) :|: 0 >= 0 && i50 - i51 = i61'
was transformed to
main_Load_181(i48, i3, i5, i49, i50, i51, env, static) -{4,4}> main_LT_192(i48, i3, i5, i50 + -1 * i51, 1, i49, i51, env, static) :|: i50 + -1 * i51 = i61'

main_LT_192(i48, i3, i5, i71, x, i49, i51, env, static) -{3,3}> main_NE_267(i48, i3, i5, i49, i51, env, static) :|: 0 >= 0 && 1 <= i71 && x = 1
was transformed to
main_LT_192(i48, i3, i5, i71, x, i49, i51, env, static) -{3,3}> main_NE_267(i48, i3, i5, i49, i51, env, static) :|: 1 <= i71 && x = 1

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

main_NE_267(i48, i3, i5, i49, i51, env, static) -{0,0}> main_NE_268(i48, i3, i5, i49, i51, env, static) :|: i49 > i51
was transformed to
main_NE_267(i48, i3, i5, i49, i51, env, static) -{0,0}> main_NE_268(i48, i3, i5, i49, i51, env, static) :|: i51 < i49

main_NE_267(i48, i3, i5, i49, x, env, static) -{7,7}> main_GE_291(i48, i3, i5, i92', i49, env, static) :|: 0 >= 0 && 0 < 1 && x = i49
was transformed to
main_NE_267(i48, i3, i5, i49, x, env, static) -{7,7}> main_GE_291(i48, i3, i5, i92', i49, env, static) :|: x = i49

main_Store_325(i48, i3, i5, i104, x, env, static) -{4,4}> main_Load_181(i48, i3, i5, i104, 10, i104, env, static) :|: 0 >= 0 && x = 10
was transformed to
main_Store_325(i48, i3, i5, i104, x, env, static) -{4,4}> main_Load_181(i48, i3, i5, i104, 10, i104, env, static) :|: x = 10

(18) Obligation:

IntTrs with 10 rules
Start term: main_Load_1(#0, #1, #2, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_GE_291(i48, i3, i5, i98, i51, env, static) -{11,11}> main_Store_325(i48, i3, i5, i103' + i100', 10, env, static) :|: i98 < 0 && i103' + i100' = i1043 && i98 <= -1 && 1 <= i100' && i51 + 1 = i103' && -1 * i98 = i100'
main_NE_267(i48, i3, i5, i49, x, env, static) -{7,7}> main_GE_291(i48, i3, i5, i92', i49, env, static) :|: x = i49
main_LT_192(i48, i3, i5, i71, x, i49, i51, env, static) -{3,3}> main_NE_267(i48, i3, i5, i49, i51, env, static) :|: 1 <= i71 && x = 1
main_NE_267(i48, i3, i5, i49, i51, env, static) -{0,0}> main_NE_268(i48, i3, i5, i49, i51, env, static) :|: i49 < i51
main_NE_267(i48, i3, i5, i49, i51, env, static) -{0,0}> main_NE_268(i48, i3, i5, i49, i51, env, static) :|: i51 < i49
main_Load_181(i48, i3, i5, i49, i50, i51, env, static) -{4,4}> main_LT_192(i48, i3, i5, i50 + -1 * i51, 1, i49, i51, env, static) :|: i50 + -1 * i51 = i61'
main_GE_291(i48, i3, i5, i99, i51, env, static) -{8,8}> main_Store_325(i48, i3, i5, i101' + i99, 10, env, static) :|: i101' + i99 = i102' && 0 <= i99 && i51 + 1 = i101'
main_LT_192(i48, i3, i5, i69, iconst_1, i49, i51, env, static) -{0,0}> main_LT_196(i48, i3, i5, i69, 1, i49, i51, env, static) :|: iconst_1 = 1 && i69 <= 0
main_Load_1(i1, i3, i5, env, static) -{15,15}> main_Load_181(i1, i3, i5, i1, i3, i5, env, static'1) :|: static'1 <= static''' + 1 && 0 <= static''' && static''' <= static + 2 && 0 <= static && 0 <= static'1
main_Store_325(i48, i3, i5, i104, x, env, static) -{4,4}> main_Load_181(i48, i3, i5, i104, 10, i104, env, static) :|: x = 10

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

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

(20) Obligation:

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

(22) Obligation:

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

Moved arithmethic from lhss to constraints.

(24) Obligation:

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

Linearized lhss.

(26) Obligation:

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

Removed div and mod.

(28) Obligation:

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

Moved arithmethic from constraints to rhss.

(30) Obligation:

IntTrs with 10 rules
Start term: main_Load_1(#0, #1, #2, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_GE_291(i48, i3, i5, i99, i51, env, static) -{8,8}> main_Store_325(i48, i3, i5, i101' + i99, 10, env, static) :|: i101' + i99 = i102' && 0 <= i99 && i51 + 1 = i101'
main_LT_192(i48, i3, i5, i71, x, i49, i51, env, static) -{3,3}> main_NE_267(i48, i3, i5, i49, i51, env, static) :|: 0 >= 0 && 1 <= i71 && x = 1
main_NE_267(i48, i3, i5, i49, i51, env, static) -{0,0}> main_NE_268(i48, i3, i5, i49, i51, env, static) :|: i49 < i51
main_Load_1(i1, i3, i5, env, static) -{15,15}> main_Load_181(i1, i3, i5, i1, i3, i5, 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_NE_267(i48, i3, i5, i49, i51, env, static) -{0,0}> main_NE_268(i48, i3, i5, i49, i51, env, static) :|: i49 > i51
main_NE_267(i48, i3, i5, i49, x, env, static) -{7,7}> main_GE_291(i48, i3, i5, i92', i49, env, static) :|: 0 >= 0 && 0 < 1 && x = i49
main_LT_192(i48, i3, i5, i69, iconst_1, i49, i51, env, static) -{0,0}> main_LT_196(i48, i3, i5, i69, 1, i49, i51, env, static) :|: iconst_1 = 1 && i69 <= 0
main_Store_325(i48, i3, i5, i104, x, env, static) -{4,4}> main_Load_181(i48, i3, i5, i104, 10, i104, env, static) :|: 0 >= 0 && x = 10
main_Load_181(i48, i3, i5, i49, i50, i51, env, static) -{4,4}> main_LT_192(i48, i3, i5, i50 - i51, 1, i49, i51, env, static) :|: 0 >= 0 && i50 - i51 = i61'
main_GE_291(i48, i3, i5, i98, i51, env, static) -{11,11}> main_Store_325(i48, i3, i5, i103' + i100', 10, env, static) :|: i98 < 0 && i103' + i100' = i1043 && i98 <= -1 && 1 <= i100' && i51 + 1 = i103' && -i98 = i100'

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

Simplified expressions.

(32) Obligation:

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

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

(34) Obligation:

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

Used field analysis yielded the following read fields:

Considered paths: all paths from start

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

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

(36) Obligation:

IntTrs with 67 rules
Start term: main_Load_1(#0, #1, #2, env, static)
Considered paths: all paths from start
Rules:
main_Load_1(i1, i3, i5, env, static) -{0,0}> main_Load_4(i1, i3, i5, env, static) :|: 0 >= 0
main_Load_4(i1, i3, i5, env, static) -{0,0}> langle_clinit_rangle_ConstantStackPush_6(i1, i3, i5, env, static) :|: 0 >= 0
langle_clinit_rangle_ConstantStackPush_6(i1, i3, i5, env, static) -{1,1}> langle_clinit_rangle_ArrayCreate_12(iconst_0, i1, i3, i5, env, static) :|: iconst_0 = 0
langle_clinit_rangle_ArrayCreate_12(iconst_0, i1, i3, i5, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_14(a2, i1, i3, i5, iconst_0, env, static) :|: a2 = 2 && iconst_0 = 0 && 0 < a2
langle_clinit_rangle_FieldAccess_14(a2, i1, i3, i5, iconst_0, env, static) -{1,1}> langle_clinit_rangle_New_16(i1, i3, i5, env, static') :|: 0 <= a2 && iconst_0 = 0 && static' <= static + a2 && 0 <= static && 0 < a2
langle_clinit_rangle_New_16(i1, i3, i5, env, static) -{0,0}> langle_clinit_rangle_New_18(i1, i3, i5, env, static) :|: 0 >= 0
langle_clinit_rangle_New_18(i1, i3, i5, env, static) -{0,0}> langle_clinit_rangle_New_19(i1, i3, i5, env, static) :|: 0 <= static
langle_clinit_rangle_New_19(i1, i3, i5, env, static) -{1,1}> langle_clinit_rangle_Duplicate_20(o2, i1, i3, i5, env, static) :|: 0 < o2 && o2 = 1
langle_clinit_rangle_Duplicate_20(o2, i1, i3, i5, env, static) -{1,1}> langle_clinit_rangle_ConstantStackPush_22(o2, i1, i3, i5, env, static) :|: 0 < o2
langle_clinit_rangle_ConstantStackPush_22(o2, i1, i3, i5, env, static) -{1,1}> langle_clinit_rangle_InvokeMethod_23(o2, NULL, i1, i3, i5, env, static) :|: NULL = 0 && 0 < o2
langle_clinit_rangle_InvokeMethod_23(o2, NULL, i1, i3, i5, env, static) -{1,1}> langle_init_rangle_Load_25(o2, i1, i3, i5, env, static) :|: NULL = 0 && 0 < o2
langle_init_rangle_Load_25(o2, i1, i3, i5, env, static) -{1,1}> langle_init_rangle_InvokeMethod_26(o2, i1, i3, i5, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_26(o2, i1, i3, i5, env, static) -{1,1}> langle_init_rangle_Load_27(o2, i1, i3, i5, env, static) :|: 0 < o2
langle_init_rangle_Load_27(o2, i1, i3, i5, env, static) -{1,1}> langle_init_rangle_InvokeMethod_29(o2, i1, i3, i5, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_29(o2, i1, i3, i5, env, static) -{1,1}> langle_init_rangle_Return_31(o2, i1, i3, i5, env, static) :|: 0 < o2
langle_init_rangle_Return_31(o2, i1, i3, i5, env, static) -{1,1}> langle_init_rangle_Return_33(o2, i1, i3, i5, env, static) :|: 0 < o2
langle_init_rangle_Return_33(o2, i1, i3, i5, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_36(o2, i1, i3, i5, env, static) :|: 0 < o2
langle_clinit_rangle_FieldAccess_36(o2, i1, i3, i5, env, static) -{1,1}> langle_clinit_rangle_Return_38(i1, i3, i5, env, static') :|: 0 < o2 && 0 <= o2 && 0 <= static && static' <= static + o2
langle_clinit_rangle_Return_38(i1, i3, i5, env, static) -{1,1}> main_Load_41(i1, i3, i5, env, static) :|: 0 >= 0
main_Load_41(i1, i3, i5, env, static) -{0,0}> main_Load_42(i1, i3, i5, env, static) :|: 0 >= 0
main_Load_42(i1, i3, i5, env, static) -{0,0}> main_Load_44(i1, i3, i5, env, static) :|: 0 <= static
main_Load_44(i1, i3, i5, env, static) -{0,0}> main_Load_45(i1, i3, i5, env, static) :|: 0 >= 0
main_Load_45(i1, i3, i5, env, static) -{0,0}> main_Load_47(i1, i3, i5, env, static) :|: 0 >= 0
main_Load_47(i1, i3, i5, env, static) -{0,0}> main_Load_181(i1, i3, i5, i1, i3, i5, env, static) :|: 0 >= 0
main_Load_181(i48, i3, i5, i49, i50, i51, env, static) -{1,1}> main_Load_183(i48, i3, i5, i50, i49, i51, env, static) :|: 0 >= 0
main_Load_183(i48, i3, i5, i50, i49, i51, env, static) -{1,1}> main_IntArithmetic_184(i48, i3, i5, i50, i51, i49, env, static) :|: 0 >= 0
main_IntArithmetic_184(i48, i3, i5, i50, i51, i49, env, static) -{1,1}> main_ConstantStackPush_185(i48, i3, i5, i61, i49, i51, env, static) :|: i50 - i51 = i61
main_ConstantStackPush_185(i48, i3, i5, i61, i49, i51, env, static) -{1,1}> main_LT_192(i48, i3, i5, i61, iconst_1, i49, i51, env, static) :|: iconst_1 = 1
main_LT_192(i48, i3, i5, i71, iconst_1, i49, i51, env, static) -{0,0}> main_LT_198(i48, i3, i5, i71, iconst_1, i49, i51, env, static) :|: iconst_1 = 1 && 1 <= i71
main_LT_198(i48, i3, i5, i71, iconst_1, i49, i51, env, static) -{1,1}> main_Load_230(i48, i3, i5, i49, i51, env, static) :|: iconst_1 <= i71 && iconst_1 = 1 && 1 <= i71
main_Load_230(i48, i3, i5, i49, i51, env, static) -{1,1}> main_Load_240(i48, i3, i5, i49, i51, env, static) :|: 0 >= 0
main_Load_240(i48, i3, i5, i49, i51, env, static) -{1,1}> main_NE_267(i48, i3, i5, i49, i51, env, static) :|: 0 >= 0
main_NE_267(i48, i3, i5, i49, i51, env, static) -{0,0}> main_NE_269(i48, i3, i5, i51, env, static) :|: i49 = i51
main_NE_269(i48, i3, i5, i51, env, static) -{1,1}> main_New_278(i48, i3, i5, i51, env, static) :|: i51 = i51
main_New_278(i48, i3, i5, i51, env, static) -{1,1}> main_Duplicate_282(i48, i3, i5, o21, i51, env, static) :|: o21 = 1 && 0 < o21
main_Duplicate_282(i48, i3, i5, o21, i51, env, static) -{1,1}> main_InvokeMethod_283(i48, i3, i5, o21, i51, env, static) :|: 0 < o21
main_InvokeMethod_283(i48, i3, i5, o21, i51, env, static) -{1,1}> main_InvokeMethod_286(i48, i3, i5, o21, i51, env, static) :|: 0 < o21
main_InvokeMethod_286(i48, i3, i5, o21, i51, env, static) -{1,1}> main_Store_288(i48, i3, i5, i92, i51, env, static) :|: 0 < o21
main_Store_288(i48, i3, i5, i92, i51, env, static) -{1,1}> main_Load_290(i48, i3, i5, i51, i92, env, static) :|: 0 >= 0
main_Load_290(i48, i3, i5, i51, i92, env, static) -{1,1}> main_GE_291(i48, i3, i5, i92, i51, env, static) :|: 0 >= 0
main_GE_291(i48, i3, i5, i98, i51, env, static) -{0,0}> main_GE_292(i48, i3, i5, i98, i51, env, static) :|: i98 <= -1
main_GE_291(i48, i3, i5, i99, i51, env, static) -{0,0}> main_GE_293(i48, i3, i5, i99, i51, env, static) :|: 0 <= i99
main_GE_292(i48, i3, i5, i98, i51, env, static) -{1,1}> main_Load_294(i48, i3, i5, i51, i98, env, static) :|: i98 <= -1 && i98 < 0
main_GE_293(i48, i3, i5, i99, i51, env, static) -{1,1}> main_ConstantStackPush_296(i48, i3, i5, i51, i99, env, static) :|: 0 <= i99
main_Load_294(i48, i3, i5, i51, i98, env, static) -{1,1}> main_IntArithmetic_297(i48, i3, i5, i98, i51, env, static) :|: i98 <= -1
main_ConstantStackPush_296(i48, i3, i5, i51, i99, env, static) -{1,1}> main_Store_298(i48, i3, i5, iconst_10, i51, i99, env, static) :|: iconst_10 = 10 && 0 <= i99
main_IntArithmetic_297(i48, i3, i5, i98, i51, env, static) -{1,1}> main_Store_299(i48, i3, i5, i100, i51, env, static) :|: i98 <= -1 && -i98 = i100 && 1 <= i100
main_Store_298(i48, i3, i5, iconst_10, i51, i99, env, static) -{1,1}> main_Load_300(i48, i3, i5, iconst_10, i51, i99, env, static) :|: iconst_10 = 10 && 0 <= i99
main_Store_299(i48, i3, i5, i100, i51, env, static) -{1,1}> main_ConstantStackPush_301(i48, i3, i5, i51, i100, env, static) :|: 1 <= i100
main_Load_300(i48, i3, i5, iconst_10, i51, i99, env, static) -{1,1}> main_ConstantStackPush_302(i48, i3, i5, i51, iconst_10, i99, env, static) :|: iconst_10 = 10 && 0 <= i99
main_ConstantStackPush_301(i48, i3, i5, i51, i100, env, static) -{1,1}> main_Store_304(i48, i3, i5, iconst_10, i51, i100, env, static) :|: iconst_10 = 10 && 1 <= i100
main_ConstantStackPush_302(i48, i3, i5, i51, iconst_10, i99, env, static) -{1,1}> main_IntArithmetic_305(i48, i3, i5, i51, iconst_1, iconst_10, i99, env, static) :|: iconst_1 = 1 && iconst_10 = 10 && 0 <= i99
main_Store_304(i48, i3, i5, iconst_10, i51, i100, env, static) -{1,1}> main_Load_306(i48, i3, i5, iconst_10, i51, i100, env, static) :|: iconst_10 = 10 && 1 <= i100
main_IntArithmetic_305(i48, i3, i5, i51, iconst_1, iconst_10, i99, env, static) -{1,1}> main_Load_308(i48, i3, i5, i101, iconst_10, i99, env, static) :|: i51 + iconst_1 = i101 && iconst_1 = 1 && iconst_10 = 10 && 0 <= i99
main_Load_306(i48, i3, i5, iconst_10, i51, i100, env, static) -{1,1}> main_ConstantStackPush_309(i48, i3, i5, i51, iconst_10, i100, env, static) :|: iconst_10 = 10 && 1 <= i100
main_Load_308(i48, i3, i5, i101, iconst_10, i99, env, static) -{1,1}> main_IntArithmetic_310(i48, i3, i5, i101, i99, iconst_10, env, static) :|: iconst_10 = 10 && 0 <= i99
main_ConstantStackPush_309(i48, i3, i5, i51, iconst_10, i100, env, static) -{1,1}> main_IntArithmetic_311(i48, i3, i5, i51, iconst_1, iconst_10, i100, env, static) :|: iconst_1 = 1 && iconst_10 = 10 && 1 <= i100
main_IntArithmetic_310(i48, i3, i5, i101, i99, iconst_10, env, static) -{1,1}> main_Store_312(i48, i3, i5, i102, iconst_10, env, static) :|: iconst_10 = 10 && 0 <= i99 && i101 + i99 = i102
main_IntArithmetic_311(i48, i3, i5, i51, iconst_1, iconst_10, i100, env, static) -{1,1}> main_Load_314(i48, i3, i5, i103, iconst_10, i100, env, static) :|: iconst_1 = 1 && iconst_10 = 10 && i51 + iconst_1 = i103 && 1 <= i100
main_Store_312(i48, i3, i5, i102, iconst_10, env, static) -{0,0}> main_Store_325(i48, i3, i5, i102, iconst_10, env, static) :|: iconst_10 = 10
main_Load_314(i48, i3, i5, i103, iconst_10, i100, env, static) -{1,1}> main_IntArithmetic_317(i48, i3, i5, i103, i100, iconst_10, env, static) :|: iconst_10 = 10 && 1 <= i100
main_IntArithmetic_317(i48, i3, i5, i103, i100, iconst_10, env, static) -{1,1}> main_Store_325(i48, i3, i5, i104, iconst_10, env, static) :|: iconst_10 = 10 && 1 <= i100 && i103 + i100 = i104
main_Store_325(i48, i3, i5, i104, iconst_10, env, static) -{1,1}> main_Load_326(i48, i3, i5, iconst_10, i104, env, static) :|: iconst_10 = 10
main_Load_326(i48, i3, i5, iconst_10, i104, env, static) -{1,1}> main_Store_329(i48, i3, i5, i104, iconst_10, env, static) :|: iconst_10 = 10
main_Store_329(i48, i3, i5, i104, iconst_10, env, static) -{1,1}> main_JMP_331(i48, i3, i5, i104, iconst_10, env, static) :|: iconst_10 = 10
main_JMP_331(i48, i3, i5, i104, iconst_10, env, static) -{1,1}> main_Load_334(i48, i3, i5, i104, iconst_10, env, static) :|: iconst_10 = 10
main_Load_334(i48, i3, i5, i104, iconst_10, env, static) -{0,0}> main_Load_181(i48, i3, i5, i104, iconst_10, i104, env, static) :|: iconst_10 = 10

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

obtained
main_Load_181(i48, i3, i5, i49, i50, i49, env, static) -{14,14}> main_GE_291(i48, i3, i5, i92', i49, env, static) :|: 0 >= 0 && i50 - i49 = i61' && 0 < 1 && 1 <= i61'
by chaining
main_Load_181(i48, i3, i5, i49, i50, i51, env, static) -{1,1}> main_Load_183(i48, i3, i5, i50, i49, i51, env, static) :|: 0 >= 0
main_Load_183(i48, i3, i5, i50, i49, i51, env, static) -{1,1}> main_IntArithmetic_184(i48, i3, i5, i50, i51, i49, env, static) :|: 0 >= 0
main_IntArithmetic_184(i48, i3, i5, i50, i51, i49, env, static) -{1,1}> main_ConstantStackPush_185(i48, i3, i5, i61, i49, i51, env, static) :|: i50 - i51 = i61
main_ConstantStackPush_185(i48, i3, i5, i61, i49, i51, env, static) -{1,1}> main_LT_192(i48, i3, i5, i61, iconst_1, i49, i51, env, static) :|: iconst_1 = 1
main_LT_192(i48, i3, i5, i71, iconst_1, i49, i51, env, static) -{0,0}> main_LT_198(i48, i3, i5, i71, iconst_1, i49, i51, env, static) :|: iconst_1 = 1 && 1 <= i71
main_LT_198(i48, i3, i5, i71, iconst_1, i49, i51, env, static) -{1,1}> main_Load_230(i48, i3, i5, i49, i51, env, static) :|: iconst_1 <= i71 && iconst_1 = 1 && 1 <= i71
main_Load_230(i48, i3, i5, i49, i51, env, static) -{1,1}> main_Load_240(i48, i3, i5, i49, i51, env, static) :|: 0 >= 0
main_Load_240(i48, i3, i5, i49, i51, env, static) -{1,1}> main_NE_267(i48, i3, i5, i49, i51, env, static) :|: 0 >= 0
main_NE_267(i48, i3, i5, i49, i51, env, static) -{0,0}> main_NE_269(i48, i3, i5, i51, env, static) :|: i49 = i51
main_NE_269(i48, i3, i5, i51, env, static) -{1,1}> main_New_278(i48, i3, i5, i51, env, static) :|: i51 = i51
main_New_278(i48, i3, i5, i51, env, static) -{1,1}> main_Duplicate_282(i48, i3, i5, o21, i51, env, static) :|: o21 = 1 && 0 < o21
main_Duplicate_282(i48, i3, i5, o21, i51, env, static) -{1,1}> main_InvokeMethod_283(i48, i3, i5, o21, i51, env, static) :|: 0 < o21
main_InvokeMethod_283(i48, i3, i5, o21, i51, env, static) -{1,1}> main_InvokeMethod_286(i48, i3, i5, o21, i51, env, static) :|: 0 < o21
main_InvokeMethod_286(i48, i3, i5, o21, i51, env, static) -{1,1}> main_Store_288(i48, i3, i5, i92, i51, env, static) :|: 0 < o21
main_Store_288(i48, i3, i5, i92, i51, env, static) -{1,1}> main_Load_290(i48, i3, i5, i51, i92, env, static) :|: 0 >= 0
main_Load_290(i48, i3, i5, i51, i92, env, static) -{1,1}> main_GE_291(i48, i3, i5, i92, i51, env, static) :|: 0 >= 0

(38) Obligation:

IntTrs with 5 rules
Start term: main_Load_1(#0, #1, #2, env, static)
Considered paths: all paths from start
Rules:
main_Load_1(i1, i3, i5, env, static) -{15,15}> main_Load_181(i1, i3, i5, i1, i3, i5, 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_Load_181(i48, i3, i5, i49, i50, i49, env, static) -{14,14}> main_GE_291(i48, i3, i5, i92', i49, env, static) :|: 0 >= 0 && i50 - i49 = i61' && 0 < 1 && 1 <= i61'
main_GE_291(i48, i3, i5, i99, i51, env, static) -{8,8}> main_Store_325(i48, i3, i5, i102', 10, env, static) :|: i101' + i99 = i102' && 0 <= i99 && i51 + 1 = i101'
main_Store_325(i48, i3, i5, i104, 10, env, static) -{4,4}> main_Load_181(i48, i3, i5, i104, 10, i104, env, static) :|: 0 >= 0
main_GE_291(i48, i3, i5, i98, i51, env, static) -{11,11}> main_Store_325(i48, i3, i5, i1043, 10, env, static) :|: i98 < 0 && i103' + i100' = i1043 && i98 <= -1 && 1 <= i100' && i51 + 1 = i103' && -i98 = i100'

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

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

main_Load_1(x1, x2, x3, x4, x5) → main_Load_1(x1, x2, x3, x5)
main_Load_181(x1, x2, x3, x4, x5, x6, x7, x8) → main_Load_181(x4, x5, x6)
main_GE_291(x1, x2, x3, x4, x5, x6, x7) → main_GE_291(x4, x5)
main_Store_325(x1, x2, x3, x4, x5, x6, x7) → main_Store_325(x4)

(40) Obligation:

IntTrs with 5 rules
Start term: main_Load_1(#0, #1, #2, static)
Considered paths: all paths from start
Rules:
main_Load_1(i1, i3, i5, static) -{15,15}> main_Load_181(i1, i3, i5) :|: 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_Load_181(i49, i50, i49) -{14,14}> main_GE_291(i92', i49) :|: 0 >= 0 && i50 - i49 = i61' && 0 < 1 && 1 <= i61'
main_GE_291(i99, i51) -{8,8}> main_Store_325(i102') :|: i101' + i99 = i102' && 0 <= i99 && i51 + 1 = i101'
main_Store_325(i104) -{4,4}> main_Load_181(i104, 10, i104) :|: 0 >= 0
main_GE_291(i98, i51) -{11,11}> main_Store_325(i1043) :|: i98 < 0 && i103' + i100' = i1043 && i98 <= -1 && 1 <= i100' && i51 + 1 = i103' && -i98 = i100'

(41) LinearizedLhssProof (BOTH CONCRETE BOUNDS(ID, ID) transformation)

Linearized lhss.

main_Load_181(i49, i50, i49) -{14,14}> main_GE_291(i92', i49) :|: 0 >= 0 && i50 - i49 = i61' && 0 < 1 && 1 <= i61'
was transformed to
main_Load_181(i49, i50, x) -{14,14}> main_GE_291(i92', i49) :|: 0 >= 0 && i50 - i49 = i61' && 0 < 1 && 1 <= i61' && x = i49

(42) Obligation:

IntTrs with 5 rules
Start term: main_Load_1(#0, #1, #2, static)
Considered paths: all paths from start
Rules:
main_Store_325(i104) -{4,4}> main_Load_181(i104, 10, i104) :|: 0 >= 0
main_GE_291(i99, i51) -{8,8}> main_Store_325(i102') :|: i101' + i99 = i102' && 0 <= i99 && i51 + 1 = i101'
main_Load_1(i1, i3, i5, static) -{15,15}> main_Load_181(i1, i3, i5) :|: 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_GE_291(i98, i51) -{11,11}> main_Store_325(i1043) :|: i98 < 0 && i103' + i100' = i1043 && i98 <= -1 && 1 <= i100' && i51 + 1 = i103' && -i98 = i100'
main_Load_181(i49, i50, x) -{14,14}> main_GE_291(i92', i49) :|: 0 >= 0 && i50 - i49 = i61' && 0 < 1 && 1 <= i61' && x = i49

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

Moved arithmethic from constraints to rhss.

main_GE_291(i99, i51) -{8,8}> main_Store_325(i102') :|: i101' + i99 = i102' && 0 <= i99 && i51 + 1 = i101'
was transformed to
main_GE_291(i99, i51) -{8,8}> main_Store_325(i101' + i99) :|: i101' + i99 = i102' && 0 <= i99 && i51 + 1 = i101'

main_GE_291(i98, i51) -{11,11}> main_Store_325(i1043) :|: i98 < 0 && i103' + i100' = i1043 && i98 <= -1 && 1 <= i100' && i51 + 1 = i103' && -i98 = i100'
was transformed to
main_GE_291(i98, i51) -{11,11}> main_Store_325(i103' + i100') :|: i98 < 0 && i103' + i100' = i1043 && i98 <= -1 && 1 <= i100' && i51 + 1 = i103' && -i98 = i100'

(44) Obligation:

IntTrs with 5 rules
Start term: main_Load_1(#0, #1, #2, static)
Considered paths: all paths from start
Rules:
main_GE_291(i99, i51) -{8,8}> main_Store_325(i101' + i99) :|: i101' + i99 = i102' && 0 <= i99 && i51 + 1 = i101'
main_Store_325(i104) -{4,4}> main_Load_181(i104, 10, i104) :|: 0 >= 0
main_Load_181(i49, i50, x) -{14,14}> main_GE_291(i92', i49) :|: 0 >= 0 && i50 - i49 = i61' && 0 < 1 && 1 <= i61' && x = i49
main_Load_1(i1, i3, i5, static) -{15,15}> main_Load_181(i1, i3, i5) :|: 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_GE_291(i98, i51) -{11,11}> main_Store_325(i103' + i100') :|: i98 < 0 && i103' + i100' = i1043 && i98 <= -1 && 1 <= i100' && i51 + 1 = i103' && -i98 = i100'

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

Simplified expressions.

main_GE_291(i98, i51) -{11,11}> main_Store_325(i103' + i100') :|: i98 < 0 && i103' + i100' = i1043 && i98 <= -1 && 1 <= i100' && i51 + 1 = i103' && -i98 = i100'
was transformed to
main_GE_291(i98, i51) -{11,11}> main_Store_325(i103' + i100') :|: i98 < 0 && i103' + i100' = i1043 && i98 <= -1 && 1 <= i100' && i51 + 1 = i103' && -1 * i98 = i100'

main_Load_181(i49, i50, x) -{14,14}> main_GE_291(i92', i49) :|: 0 >= 0 && i50 - i49 = i61' && 0 < 1 && 1 <= i61' && x = i49
was transformed to
main_Load_181(i49, i50, x) -{14,14}> main_GE_291(i92', i49) :|: i50 + -1 * i49 = i61' && 1 <= i61' && x = i49

main_Load_1(i1, i3, i5, static) -{15,15}> main_Load_181(i1, i3, i5) :|: 0 >= 0 && static'1 <= static''' + 1 && 0 <= 2 && 0 <= static''' && static''' <= static + 2 && 0 < 1 && 0 <= 1 && 0 <= static && 0 <= static'1 && 0 < 2
was transformed to
main_Load_1(i1, i3, i5, static) -{15,15}> main_Load_181(i1, i3, i5) :|: static'1 <= static''' + 1 && 0 <= static''' && static''' <= static + 2 && 0 <= static && 0 <= static'1

(46) Obligation:

IntTrs with 5 rules
Start term: main_Load_1(#0, #1, #2, static)
Considered paths: all paths from start
Rules:
main_Store_325(i104) -{4,4}> main_Load_181(i104, 10, i104) :|: 0 >= 0
main_GE_291(i99, i51) -{8,8}> main_Store_325(i101' + i99) :|: i101' + i99 = i102' && 0 <= i99 && i51 + 1 = i101'
main_Load_1(i1, i3, i5, static) -{15,15}> main_Load_181(i1, i3, i5) :|: static'1 <= static''' + 1 && 0 <= static''' && static''' <= static + 2 && 0 <= static && 0 <= static'1
main_GE_291(i98, i51) -{11,11}> main_Store_325(i103' + i100') :|: i98 < 0 && i103' + i100' = i1043 && i98 <= -1 && 1 <= i100' && i51 + 1 = i103' && -1 * i98 = i100'
main_Load_181(i49, i50, x) -{14,14}> main_GE_291(i92', i49) :|: i50 + -1 * i49 = i61' && 1 <= i61' && x = i49

(47) koat Proof (EQUIVALENT transformation)

YES(?, 37*ar_0 + 381)

Initial complexity problem:
1: T:
(Comp: ?, Cost: 4) main_Store_325(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_Load_181(ar_0, 10, ar_0, arityPad)) [ 0 >= 0 ]
(Comp: ?, Cost: 8) main_GE_291(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_Store_325(i101' + ar_0, arityPad, arityPad, arityPad)) [ i101' + ar_0 = i102' /\ 0 <= ar_0 /\ ar_1 + 1 = i101' ]
(Comp: ?, Cost: 15) main_Load_1(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_Load_181(ar_0, ar_1, ar_2, arityPad)) [ static'1 <= static''' + 1 /\ 0 <= static''' /\ static''' <= ar_3 + 2 /\ 0 <= ar_3 /\ 0 <= static'1 ]
(Comp: ?, Cost: 11) main_GE_291(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_Store_325(i103' + i100', arityPad, arityPad, arityPad)) [ ar_0 < 0 /\ i103' + i100' = i1043 /\ ar_0 <= -1 /\ 1 <= i100' /\ ar_1 + 1 = i103' /\ -ar_0 = i100' ]
(Comp: ?, Cost: 14) main_Load_181(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_GE_291(i92', ar_0, arityPad, arityPad)) [ ar_1 - ar_0 = i61' /\ 1 <= i61' /\ ar_2 = ar_0 ]
(Comp: 1, Cost: 0) koat_start(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_Load_1(ar_0, ar_1, ar_2, ar_3)) [ 0 <= 0 ]
start location: koat_start
leaf cost: 0

Repeatedly propagating knowledge in problem 1 produces the following problem:
2: T:
(Comp: ?, Cost: 4) main_Store_325(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_Load_181(ar_0, 10, ar_0, arityPad)) [ 0 >= 0 ]
(Comp: ?, Cost: 8) main_GE_291(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_Store_325(i101' + ar_0, arityPad, arityPad, arityPad)) [ i101' + ar_0 = i102' /\ 0 <= ar_0 /\ ar_1 + 1 = i101' ]
(Comp: 1, Cost: 15) main_Load_1(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_Load_181(ar_0, ar_1, ar_2, arityPad)) [ static'1 <= static''' + 1 /\ 0 <= static''' /\ static''' <= ar_3 + 2 /\ 0 <= ar_3 /\ 0 <= static'1 ]
(Comp: ?, Cost: 11) main_GE_291(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_Store_325(i103' + i100', arityPad, arityPad, arityPad)) [ ar_0 < 0 /\ i103' + i100' = i1043 /\ ar_0 <= -1 /\ 1 <= i100' /\ ar_1 + 1 = i103' /\ -ar_0 = i100' ]
(Comp: ?, Cost: 14) main_Load_181(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_GE_291(i92', ar_0, arityPad, arityPad)) [ ar_1 - ar_0 = i61' /\ 1 <= i61' /\ ar_2 = ar_0 ]
(Comp: 1, Cost: 0) koat_start(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_Load_1(ar_0, ar_1, ar_2, ar_3)) [ 0 <= 0 ]
start location: koat_start
leaf cost: 0

By chaining the transition main_Store_325(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_Load_181(ar_0, 10, ar_0, arityPad)) [ 0 >= 0 ] with all transitions in problem 2, the following new transition is obtained:
main_Store_325(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_GE_291(i92', ar_0, arityPad', arityPad')) [ 0 >= 0 /\ -ar_0 + 10 = i61' /\ 1 <= i61' /\ ar_0 = ar_0 ]
We thus obtain the following problem:
3: T:
(Comp: ?, Cost: 18) main_Store_325(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_GE_291(i92', ar_0, arityPad', arityPad')) [ 0 >= 0 /\ -ar_0 + 10 = i61' /\ 1 <= i61' /\ ar_0 = ar_0 ]
(Comp: ?, Cost: 8) main_GE_291(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_Store_325(i101' + ar_0, arityPad, arityPad, arityPad)) [ i101' + ar_0 = i102' /\ 0 <= ar_0 /\ ar_1 + 1 = i101' ]
(Comp: 1, Cost: 15) main_Load_1(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_Load_181(ar_0, ar_1, ar_2, arityPad)) [ static'1 <= static''' + 1 /\ 0 <= static''' /\ static''' <= ar_3 + 2 /\ 0 <= ar_3 /\ 0 <= static'1 ]
(Comp: ?, Cost: 11) main_GE_291(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_Store_325(i103' + i100', arityPad, arityPad, arityPad)) [ ar_0 < 0 /\ i103' + i100' = i1043 /\ ar_0 <= -1 /\ 1 <= i100' /\ ar_1 + 1 = i103' /\ -ar_0 = i100' ]
(Comp: ?, Cost: 14) main_Load_181(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_GE_291(i92', ar_0, arityPad, arityPad)) [ ar_1 - ar_0 = i61' /\ 1 <= i61' /\ ar_2 = ar_0 ]
(Comp: 1, Cost: 0) koat_start(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_Load_1(ar_0, ar_1, ar_2, ar_3)) [ 0 <= 0 ]
start location: koat_start
leaf cost: 0

Repeatedly propagating knowledge in problem 3 produces the following problem:
4: T:
(Comp: ?, Cost: 18) main_Store_325(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_GE_291(i92', ar_0, arityPad', arityPad')) [ 0 >= 0 /\ -ar_0 + 10 = i61' /\ 1 <= i61' /\ ar_0 = ar_0 ]
(Comp: ?, Cost: 8) main_GE_291(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_Store_325(i101' + ar_0, arityPad, arityPad, arityPad)) [ i101' + ar_0 = i102' /\ 0 <= ar_0 /\ ar_1 + 1 = i101' ]
(Comp: 1, Cost: 15) main_Load_1(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_Load_181(ar_0, ar_1, ar_2, arityPad)) [ static'1 <= static''' + 1 /\ 0 <= static''' /\ static''' <= ar_3 + 2 /\ 0 <= ar_3 /\ 0 <= static'1 ]
(Comp: ?, Cost: 11) main_GE_291(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_Store_325(i103' + i100', arityPad, arityPad, arityPad)) [ ar_0 < 0 /\ i103' + i100' = i1043 /\ ar_0 <= -1 /\ 1 <= i100' /\ ar_1 + 1 = i103' /\ -ar_0 = i100' ]
(Comp: 1, Cost: 14) main_Load_181(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_GE_291(i92', ar_0, arityPad, arityPad)) [ ar_1 - ar_0 = i61' /\ 1 <= i61' /\ ar_2 = ar_0 ]
(Comp: 1, Cost: 0) koat_start(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_Load_1(ar_0, ar_1, ar_2, ar_3)) [ 0 <= 0 ]
start location: koat_start
leaf cost: 0

A polynomial rank function with
Pol(main_Store_325) = -V_1 + 10
Pol(main_GE_291) = -V_2 + 9
Pol(main_Load_1) = -V_1 + 9
Pol(main_Load_181) = -V_1 + 9
Pol(koat_start) = -V_1 + 9
orients all transitions weakly and the transition
main_Store_325(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_GE_291(i92', ar_0, arityPad', arityPad')) [ 0 >= 0 /\ -ar_0 + 10 = i61' /\ 1 <= i61' /\ ar_0 = ar_0 ]
strictly and produces the following problem:
5: T:
(Comp: ar_0 + 9, Cost: 18) main_Store_325(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_GE_291(i92', ar_0, arityPad', arityPad')) [ 0 >= 0 /\ -ar_0 + 10 = i61' /\ 1 <= i61' /\ ar_0 = ar_0 ]
(Comp: ?, Cost: 8) main_GE_291(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_Store_325(i101' + ar_0, arityPad, arityPad, arityPad)) [ i101' + ar_0 = i102' /\ 0 <= ar_0 /\ ar_1 + 1 = i101' ]
(Comp: 1, Cost: 15) main_Load_1(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_Load_181(ar_0, ar_1, ar_2, arityPad)) [ static'1 <= static''' + 1 /\ 0 <= static''' /\ static''' <= ar_3 + 2 /\ 0 <= ar_3 /\ 0 <= static'1 ]
(Comp: ?, Cost: 11) main_GE_291(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_Store_325(i103' + i100', arityPad, arityPad, arityPad)) [ ar_0 < 0 /\ i103' + i100' = i1043 /\ ar_0 <= -1 /\ 1 <= i100' /\ ar_1 + 1 = i103' /\ -ar_0 = i100' ]
(Comp: 1, Cost: 14) main_Load_181(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_GE_291(i92', ar_0, arityPad, arityPad)) [ ar_1 - ar_0 = i61' /\ 1 <= i61' /\ ar_2 = ar_0 ]
(Comp: 1, Cost: 0) koat_start(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_Load_1(ar_0, ar_1, ar_2, ar_3)) [ 0 <= 0 ]
start location: koat_start
leaf cost: 0

Repeatedly propagating knowledge in problem 5 produces the following problem:
6: T:
(Comp: ar_0 + 9, Cost: 18) main_Store_325(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_GE_291(i92', ar_0, arityPad', arityPad')) [ 0 >= 0 /\ -ar_0 + 10 = i61' /\ 1 <= i61' /\ ar_0 = ar_0 ]
(Comp: ar_0 + 10, Cost: 8) main_GE_291(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_Store_325(i101' + ar_0, arityPad, arityPad, arityPad)) [ i101' + ar_0 = i102' /\ 0 <= ar_0 /\ ar_1 + 1 = i101' ]
(Comp: 1, Cost: 15) main_Load_1(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_Load_181(ar_0, ar_1, ar_2, arityPad)) [ static'1 <= static''' + 1 /\ 0 <= static''' /\ static''' <= ar_3 + 2 /\ 0 <= ar_3 /\ 0 <= static'1 ]
(Comp: ar_0 + 10, Cost: 11) main_GE_291(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_Store_325(i103' + i100', arityPad, arityPad, arityPad)) [ ar_0 < 0 /\ i103' + i100' = i1043 /\ ar_0 <= -1 /\ 1 <= i100' /\ ar_1 + 1 = i103' /\ -ar_0 = i100' ]
(Comp: 1, Cost: 14) main_Load_181(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_GE_291(i92', ar_0, arityPad, arityPad)) [ ar_1 - ar_0 = i61' /\ 1 <= i61' /\ ar_2 = ar_0 ]
(Comp: 1, Cost: 0) koat_start(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_Load_1(ar_0, ar_1, ar_2, ar_3)) [ 0 <= 0 ]
start location: koat_start
leaf cost: 0

Complexity upper bound 37*ar_0 + 381

Time: 0.544 sec (SMT: 0.469 sec)

(0) Obligation:

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

(2) Obligation:

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

(4) Obligation:

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

(6) Obligation:

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

(8) Obligation:

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

(10) Obligation:

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

(12) Obligation:

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

(14) Obligation:

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

(16) Obligation:

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

(18) Obligation:

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

(20) Obligation:

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

(22) Obligation:

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

(24) Obligation:

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

(26) Obligation:

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

(34) Obligation:

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

(36) Obligation:

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

(38) Obligation:

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

(40) Obligation:

(41) LinearizedLhssProof (BOTH CONCRETE BOUNDS(ID, ID) transformation)

(42) Obligation:

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

(44) Obligation:

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

(46) Obligation:

(47) koat Proof (EQUIVALENT transformation)

(48) BOUNDS(CONSTANT, 381 + 37 * |#0|)