time complexity proof of /tmp/tmpI5nW57/Test11.jar

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

0 JBC problem

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

↳2 JBCTerminationGraph

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

↳4 JBCComplexityEdges

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

    ↳6 WeightedIntTrs

        ↳7 StraightLineCodeCompressionProof (BOTH CONCRETE BOUNDS(ID, ID), 55 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), 93 ms)

    ↳16 WeightedIntTrs

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

        ↳18 WeightedIntTrs

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

        ↳20 WeightedIntTrs

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

        ↳22 WeightedIntTrs

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

        ↳24 WeightedIntTrs

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

        ↳26 WeightedIntTrs

        ↳27 koat Proof (⇔, 2308 ms)

        ↳28 BOUNDS(CONSTANT, 484 + 51000 * |#0|)

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

↳30 JBCComplexityEdges

    ↳31 JBCGraphEdgesToCpxIntTrsProof (CONCRETE UPPER BOUND(ID), 84 ms)

    ↳32 WeightedIntTrs

    ↳33 StraightLineCodeCompressionProof (BOTH CONCRETE BOUNDS(ID, ID), 33 ms)

    ↳34 WeightedIntTrs

    ↳35 WeightedIntTrsUnneededArgumentFilterProof (CONCRETE UPPER BOUND(ID), 24 ms)

    ↳36 WeightedIntTrs

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

    ↳38 WeightedIntTrs

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

    ↳40 WeightedIntTrs

(0) Obligation:

Need to prove time_complexity of the following program:

public class Test11 {
    public static void main(int l) {
	int x = l * 100, y = l * 200 / 13;

	while (x + y > 0) {
	    if (new Object().hashCode() * new Object().hashCode() > 9)
		x--;
	    else
		y--;
	}
    }
}

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

Constructed TerminationGraph.

(2) Obligation:

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

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

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

(4) Obligation:

Set of 60 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 60 jbc graph edges to a weighted ITS with 60 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 60 rules
Start term: main_Load_1(#0, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_Load_1(i1, env, static) -{0,0}> main_Load_3(i1, env, static) :|: 0 >= 0
main_Load_3(i1, env, static) -{0,0}> langle_clinit_rangle_ConstantStackPush_6(i1, env, static) :|: 0 >= 0
langle_clinit_rangle_ConstantStackPush_6(i1, env, static) -{1,1}> langle_clinit_rangle_ArrayCreate_12(iconst_0, i1, env, static) :|: iconst_0 = 0
langle_clinit_rangle_ArrayCreate_12(iconst_0, i1, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_14(a2, i1, iconst_0, env, static) :|: a2 = 2 && iconst_0 = 0 && 0 < a2
langle_clinit_rangle_FieldAccess_14(a2, i1, iconst_0, env, static) -{1,1}> langle_clinit_rangle_New_16(i1, env, static') :|: 0 <= a2 && iconst_0 = 0 && static' <= static + a2 && 0 <= static && 0 < a2
langle_clinit_rangle_New_16(i1, env, static) -{0,0}> langle_clinit_rangle_New_17(i1, env, static) :|: 0 >= 0
langle_clinit_rangle_New_17(i1, env, static) -{0,0}> langle_clinit_rangle_New_19(i1, env, static) :|: 0 <= static
langle_clinit_rangle_New_19(i1, env, static) -{1,1}> langle_clinit_rangle_Duplicate_20(o2, i1, env, static) :|: 0 < o2 && o2 = 1
langle_clinit_rangle_Duplicate_20(o2, i1, env, static) -{1,1}> langle_clinit_rangle_ConstantStackPush_22(o2, i1, env, static) :|: 0 < o2
langle_clinit_rangle_ConstantStackPush_22(o2, i1, env, static) -{1,1}> langle_clinit_rangle_InvokeMethod_23(o2, NULL, i1, env, static) :|: NULL = 0 && 0 < o2
langle_clinit_rangle_InvokeMethod_23(o2, NULL, i1, env, static) -{1,1}> langle_init_rangle_Load_24(o2, i1, env, static) :|: NULL = 0 && 0 < o2
langle_init_rangle_Load_24(o2, i1, env, static) -{1,1}> langle_init_rangle_InvokeMethod_27(o2, i1, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_27(o2, i1, env, static) -{1,1}> langle_init_rangle_Load_28(o2, i1, env, static) :|: 0 < o2
langle_init_rangle_Load_28(o2, i1, env, static) -{1,1}> langle_init_rangle_InvokeMethod_30(o2, i1, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_30(o2, i1, env, static) -{1,1}> langle_init_rangle_Return_33(o2, i1, env, static) :|: 0 < o2
langle_init_rangle_Return_33(o2, i1, env, static) -{1,1}> langle_init_rangle_Return_35(o2, i1, env, static) :|: 0 < o2
langle_init_rangle_Return_35(o2, i1, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_38(o2, i1, env, static) :|: 0 < o2
langle_clinit_rangle_FieldAccess_38(o2, i1, env, static) -{1,1}> langle_clinit_rangle_Return_40(i1, env, static') :|: 0 < o2 && 0 <= o2 && 0 <= static && static' <= static + o2
langle_clinit_rangle_Return_40(i1, env, static) -{1,1}> main_Load_41(i1, env, static) :|: 0 >= 0
main_Load_41(i1, env, static) -{0,0}> main_Load_42(i1, env, static) :|: 0 >= 0
main_Load_42(i1, env, static) -{0,0}> main_Load_44(i1, env, static) :|: 0 <= static
main_Load_44(i1, env, static) -{0,0}> main_Load_46(i1, env, static) :|: 0 >= 0
main_Load_46(i1, env, static) -{0,0}> main_Load_48(i1, env, static) :|: 0 >= 0
main_Load_48(i1, env, static) -{1,1}> main_ConstantStackPush_50(i1, env, static) :|: 0 >= 0
main_ConstantStackPush_50(i1, env, static) -{1,1}> main_IntArithmetic_52(i1, iconst_100, env, static) :|: iconst_100 = 100
main_IntArithmetic_52(i1, iconst_100, env, static) -{1,1}> main_Store_54(i1, i4, env, static) :|: i1 * iconst_100 = i4 && iconst_100 = 100
main_Store_54(i1, i4, env, static) -{1,1}> main_Load_56(i1, i4, env, static) :|: 0 >= 0
main_Load_56(i1, i4, env, static) -{1,1}> main_ConstantStackPush_58(i1, i4, env, static) :|: 0 >= 0
main_ConstantStackPush_58(i1, i4, env, static) -{1,1}> main_IntArithmetic_60(i1, iconst_200, i4, env, static) :|: iconst_200 = 200
main_IntArithmetic_60(i1, iconst_200, i4, env, static) -{1,1}> main_ConstantStackPush_63(i1, i6, i4, env, static) :|: i1 * iconst_200 = i6 && iconst_200 = 200
main_ConstantStackPush_63(i1, i6, i4, env, static) -{1,1}> main_IntArithmetic_65(i1, i6, iconst_13, i4, env, static) :|: iconst_13 = 13
main_IntArithmetic_65(i1, i6, iconst_13, i4, env, static) -{1,1}> main_Store_67(i1, i8, i4, env, static) :|: iconst_13 = 13
main_Store_67(i1, i8, i4, env, static) -{1,1}> main_Load_70(i1, i4, i8, env, static) :|: 0 >= 0
main_Load_70(i1, i4, i8, env, static) -{0,0}> main_Load_142(i1, i4, i8, env, static) :|: 0 >= 0
main_Load_142(i1, i4, i33, env, static) -{1,1}> main_Load_148(i1, i4, i33, env, static) :|: 0 >= 0
main_Load_148(i1, i4, i33, env, static) -{1,1}> main_IntArithmetic_150(i1, i4, i33, env, static) :|: 0 >= 0
main_IntArithmetic_150(i1, i4, i33, env, static) -{1,1}> main_LE_153(i1, i46, i4, i33, env, static) :|: i4 + i33 = i46
main_LE_153(i1, i53, i4, i33, env, static) -{0,0}> main_LE_155(i1, i53, i4, i33, env, static) :|: i53 <= 0
main_LE_153(i1, i54, i4, i33, env, static) -{0,0}> main_LE_156(i1, i54, i4, i33, env, static) :|: 1 <= i54
main_LE_156(i1, i54, i4, i33, env, static) -{1,1}> main_New_161(i1, i4, i33, env, static) :|: 1 <= i54 && 0 < i54
main_New_161(i1, i4, i33, env, static) -{1,1}> main_Duplicate_164(i1, o12, i4, i33, env, static) :|: 0 < o12 && o12 = 1
main_Duplicate_164(i1, o12, i4, i33, env, static) -{1,1}> main_InvokeMethod_165(i1, o12, i4, i33, env, static) :|: 0 < o12
main_InvokeMethod_165(i1, o12, i4, i33, env, static) -{1,1}> main_InvokeMethod_166(i1, o12, i4, i33, env, static) :|: 0 < o12
main_InvokeMethod_166(i1, o12, i4, i33, env, static) -{1,1}> main_New_169(i1, i59, i4, i33, env, static) :|: 0 < o12
main_New_169(i1, i59, i4, i33, env, static) -{1,1}> main_Duplicate_170(i1, i59, o13, i4, i33, env, static) :|: 0 < o13 && o13 = 1
main_Duplicate_170(i1, i59, o13, i4, i33, env, static) -{1,1}> main_InvokeMethod_171(i1, i59, o13, i4, i33, env, static) :|: 0 < o13
main_InvokeMethod_171(i1, i59, o13, i4, i33, env, static) -{1,1}> main_InvokeMethod_174(i1, i59, o13, i4, i33, env, static) :|: 0 < o13
main_InvokeMethod_174(i1, i59, o13, i4, i33, env, static) -{1,1}> main_IntArithmetic_175(i1, i59, i62, i4, i33, env, static) :|: 0 < o13
main_IntArithmetic_175(i1, i59, i62, i4, i33, env, static) -{1,1}> main_ConstantStackPush_176(i1, i63, i4, i33, env, static) :|: i59 * i62 = i63
main_ConstantStackPush_176(i1, i63, i4, i33, env, static) -{1,1}> main_LE_178(i1, i63, iconst_9, i4, i33, env, static) :|: iconst_9 = 9
main_LE_178(i1, i68, iconst_9, i4, i33, env, static) -{0,0}> main_LE_179(i1, i68, iconst_9, i4, i33, env, static) :|: i68 <= 9 && iconst_9 = 9
main_LE_178(i1, i69, iconst_9, i4, i33, env, static) -{0,0}> main_LE_180(i1, i69, iconst_9, i4, i33, env, static) :|: 10 <= i69 && iconst_9 = 9
main_LE_179(i1, i68, iconst_9, i4, i33, env, static) -{1,1}> main_Inc_183(i1, i4, i33, env, static) :|: i68 <= iconst_9 && i68 <= 9 && iconst_9 = 9
main_LE_180(i1, i69, iconst_9, i4, i33, env, static) -{1,1}> main_Inc_186(i1, i4, i33, env, static) :|: iconst_9 < i69 && 10 <= i69 && iconst_9 = 9
main_Inc_183(i1, i4, i33, env, static) -{1,1}> main_JMP_190(i1, i4, i73, env, static) :|: i33 + -1 = i73
main_Inc_186(i1, i4, i33, env, static) -{1,1}> main_JMP_193(i1, i75, i33, env, static) :|: i4 + -1 = i75
main_JMP_190(i1, i4, i73, env, static) -{1,1}> main_Load_200(i1, i4, i73, env, static) :|: 0 >= 0
main_JMP_193(i1, i75, i33, env, static) -{1,1}> main_Load_207(i1, i75, i33, env, static) :|: 0 >= 0
main_Load_200(i1, i4, i73, env, static) -{0,0}> main_Load_142(i1, i4, i73, env, static) :|: 0 >= 0
main_Load_207(i1, i75, i33, env, static) -{0,0}> main_Load_142(i1, i75, i33, env, static) :|: 0 >= 0

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

obtained
main_Load_1(i1, env, static) -{25,25}> main_Load_142(i1, i4', i8', env, static'1) :|: 0 >= 0 && i1 * 100 = i4' && i1 * 200 = i6' && static'1 <= static''' + 1 && 0 <= 2 && 0 <= static''' && static''' <= static + 2 && 0 < 1 && 0 <= 1 && 0 <= static && 0 < 2 && 0 <= static'1
by chaining
main_Load_1(i1, env, static) -{0,0}> main_Load_3(i1, env, static) :|: 0 >= 0
main_Load_3(i1, env, static) -{0,0}> langle_clinit_rangle_ConstantStackPush_6(i1, env, static) :|: 0 >= 0
langle_clinit_rangle_ConstantStackPush_6(i1, env, static) -{1,1}> langle_clinit_rangle_ArrayCreate_12(iconst_0, i1, env, static) :|: iconst_0 = 0
langle_clinit_rangle_ArrayCreate_12(iconst_0, i1, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_14(a2, i1, iconst_0, env, static) :|: a2 = 2 && iconst_0 = 0 && 0 < a2
langle_clinit_rangle_FieldAccess_14(a2, i1, iconst_0, env, static) -{1,1}> langle_clinit_rangle_New_16(i1, env, static') :|: 0 <= a2 && iconst_0 = 0 && static' <= static + a2 && 0 <= static && 0 < a2
langle_clinit_rangle_New_16(i1, env, static) -{0,0}> langle_clinit_rangle_New_17(i1, env, static) :|: 0 >= 0
langle_clinit_rangle_New_17(i1, env, static) -{0,0}> langle_clinit_rangle_New_19(i1, env, static) :|: 0 <= static
langle_clinit_rangle_New_19(i1, env, static) -{1,1}> langle_clinit_rangle_Duplicate_20(o2, i1, env, static) :|: 0 < o2 && o2 = 1
langle_clinit_rangle_Duplicate_20(o2, i1, env, static) -{1,1}> langle_clinit_rangle_ConstantStackPush_22(o2, i1, env, static) :|: 0 < o2
langle_clinit_rangle_ConstantStackPush_22(o2, i1, env, static) -{1,1}> langle_clinit_rangle_InvokeMethod_23(o2, NULL, i1, env, static) :|: NULL = 0 && 0 < o2
langle_clinit_rangle_InvokeMethod_23(o2, NULL, i1, env, static) -{1,1}> langle_init_rangle_Load_24(o2, i1, env, static) :|: NULL = 0 && 0 < o2
langle_init_rangle_Load_24(o2, i1, env, static) -{1,1}> langle_init_rangle_InvokeMethod_27(o2, i1, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_27(o2, i1, env, static) -{1,1}> langle_init_rangle_Load_28(o2, i1, env, static) :|: 0 < o2
langle_init_rangle_Load_28(o2, i1, env, static) -{1,1}> langle_init_rangle_InvokeMethod_30(o2, i1, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_30(o2, i1, env, static) -{1,1}> langle_init_rangle_Return_33(o2, i1, env, static) :|: 0 < o2
langle_init_rangle_Return_33(o2, i1, env, static) -{1,1}> langle_init_rangle_Return_35(o2, i1, env, static) :|: 0 < o2
langle_init_rangle_Return_35(o2, i1, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_38(o2, i1, env, static) :|: 0 < o2
langle_clinit_rangle_FieldAccess_38(o2, i1, env, static) -{1,1}> langle_clinit_rangle_Return_40(i1, env, static') :|: 0 < o2 && 0 <= o2 && 0 <= static && static' <= static + o2
langle_clinit_rangle_Return_40(i1, env, static) -{1,1}> main_Load_41(i1, env, static) :|: 0 >= 0
main_Load_41(i1, env, static) -{0,0}> main_Load_42(i1, env, static) :|: 0 >= 0
main_Load_42(i1, env, static) -{0,0}> main_Load_44(i1, env, static) :|: 0 <= static
main_Load_44(i1, env, static) -{0,0}> main_Load_46(i1, env, static) :|: 0 >= 0
main_Load_46(i1, env, static) -{0,0}> main_Load_48(i1, env, static) :|: 0 >= 0
main_Load_48(i1, env, static) -{1,1}> main_ConstantStackPush_50(i1, env, static) :|: 0 >= 0
main_ConstantStackPush_50(i1, env, static) -{1,1}> main_IntArithmetic_52(i1, iconst_100, env, static) :|: iconst_100 = 100
main_IntArithmetic_52(i1, iconst_100, env, static) -{1,1}> main_Store_54(i1, i4, env, static) :|: i1 * iconst_100 = i4 && iconst_100 = 100
main_Store_54(i1, i4, env, static) -{1,1}> main_Load_56(i1, i4, env, static) :|: 0 >= 0
main_Load_56(i1, i4, env, static) -{1,1}> main_ConstantStackPush_58(i1, i4, env, static) :|: 0 >= 0
main_ConstantStackPush_58(i1, i4, env, static) -{1,1}> main_IntArithmetic_60(i1, iconst_200, i4, env, static) :|: iconst_200 = 200
main_IntArithmetic_60(i1, iconst_200, i4, env, static) -{1,1}> main_ConstantStackPush_63(i1, i6, i4, env, static) :|: i1 * iconst_200 = i6 && iconst_200 = 200
main_ConstantStackPush_63(i1, i6, i4, env, static) -{1,1}> main_IntArithmetic_65(i1, i6, iconst_13, i4, env, static) :|: iconst_13 = 13
main_IntArithmetic_65(i1, i6, iconst_13, i4, env, static) -{1,1}> main_Store_67(i1, i8, i4, env, static) :|: iconst_13 = 13
main_Store_67(i1, i8, i4, env, static) -{1,1}> main_Load_70(i1, i4, i8, env, static) :|: 0 >= 0
main_Load_70(i1, i4, i8, env, static) -{0,0}> main_Load_142(i1, i4, i8, env, static) :|: 0 >= 0

obtained
main_Load_142(i1, i4, i33, env, static) -{3,3}> main_LE_153(i1, i46', i4, i33, env, static) :|: 0 >= 0 && i4 + i33 = i46'
by chaining
main_Load_142(i1, i4, i33, env, static) -{1,1}> main_Load_148(i1, i4, i33, env, static) :|: 0 >= 0
main_Load_148(i1, i4, i33, env, static) -{1,1}> main_IntArithmetic_150(i1, i4, i33, env, static) :|: 0 >= 0
main_IntArithmetic_150(i1, i4, i33, env, static) -{1,1}> main_LE_153(i1, i46, i4, i33, env, static) :|: i4 + i33 = i46

obtained
main_LE_153(i1, i54, i4, i33, env, static) -{11,11}> main_LE_178(i1, i63', 9, i4, i33, env, static) :|: 1 <= i54 && 0 < 1 && i59' * i62' = i63' && 0 < i54
by chaining
main_LE_153(i1, i54, i4, i33, env, static) -{0,0}> main_LE_156(i1, i54, i4, i33, env, static) :|: 1 <= i54
main_LE_156(i1, i54, i4, i33, env, static) -{1,1}> main_New_161(i1, i4, i33, env, static) :|: 1 <= i54 && 0 < i54
main_New_161(i1, i4, i33, env, static) -{1,1}> main_Duplicate_164(i1, o12, i4, i33, env, static) :|: 0 < o12 && o12 = 1
main_Duplicate_164(i1, o12, i4, i33, env, static) -{1,1}> main_InvokeMethod_165(i1, o12, i4, i33, env, static) :|: 0 < o12
main_InvokeMethod_165(i1, o12, i4, i33, env, static) -{1,1}> main_InvokeMethod_166(i1, o12, i4, i33, env, static) :|: 0 < o12
main_InvokeMethod_166(i1, o12, i4, i33, env, static) -{1,1}> main_New_169(i1, i59, i4, i33, env, static) :|: 0 < o12
main_New_169(i1, i59, i4, i33, env, static) -{1,1}> main_Duplicate_170(i1, i59, o13, i4, i33, env, static) :|: 0 < o13 && o13 = 1
main_Duplicate_170(i1, i59, o13, i4, i33, env, static) -{1,1}> main_InvokeMethod_171(i1, i59, o13, i4, i33, env, static) :|: 0 < o13
main_InvokeMethod_171(i1, i59, o13, i4, i33, env, static) -{1,1}> main_InvokeMethod_174(i1, i59, o13, i4, i33, env, static) :|: 0 < o13
main_InvokeMethod_174(i1, i59, o13, i4, i33, env, static) -{1,1}> main_IntArithmetic_175(i1, i59, i62, i4, i33, env, static) :|: 0 < o13
main_IntArithmetic_175(i1, i59, i62, i4, i33, env, static) -{1,1}> main_ConstantStackPush_176(i1, i63, i4, i33, env, static) :|: i59 * i62 = i63
main_ConstantStackPush_176(i1, i63, i4, i33, env, static) -{1,1}> main_LE_178(i1, i63, iconst_9, i4, i33, env, static) :|: iconst_9 = 9

obtained
main_LE_178(i1, i69, 9, i4, i33, env, static) -{3,3}> main_Load_142(i1, i75', i33, env, static) :|: 0 >= 0 && 10 <= i69 && i4 + -1 = i75' && 9 < i69
by chaining
main_LE_178(i1, i69, iconst_9, i4, i33, env, static) -{0,0}> main_LE_180(i1, i69, iconst_9, i4, i33, env, static) :|: 10 <= i69 && iconst_9 = 9
main_LE_180(i1, i69, iconst_9, i4, i33, env, static) -{1,1}> main_Inc_186(i1, i4, i33, env, static) :|: iconst_9 < i69 && 10 <= i69 && iconst_9 = 9
main_Inc_186(i1, i4, i33, env, static) -{1,1}> main_JMP_193(i1, i75, i33, env, static) :|: i4 + -1 = i75
main_JMP_193(i1, i75, i33, env, static) -{1,1}> main_Load_207(i1, i75, i33, env, static) :|: 0 >= 0
main_Load_207(i1, i75, i33, env, static) -{0,0}> main_Load_142(i1, i75, i33, env, static) :|: 0 >= 0

obtained
main_LE_178(i1, i68, 9, i4, i33, env, static) -{3,3}> main_Load_142(i1, i4, i73', env, static) :|: 0 >= 0 && i68 <= 9 && i33 + -1 = i73'
by chaining
main_LE_178(i1, i68, iconst_9, i4, i33, env, static) -{0,0}> main_LE_179(i1, i68, iconst_9, i4, i33, env, static) :|: i68 <= 9 && iconst_9 = 9
main_LE_179(i1, i68, iconst_9, i4, i33, env, static) -{1,1}> main_Inc_183(i1, i4, i33, env, static) :|: i68 <= iconst_9 && i68 <= 9 && iconst_9 = 9
main_Inc_183(i1, i4, i33, env, static) -{1,1}> main_JMP_190(i1, i4, i73, env, static) :|: i33 + -1 = i73
main_JMP_190(i1, i4, i73, env, static) -{1,1}> main_Load_200(i1, i4, i73, env, static) :|: 0 >= 0
main_Load_200(i1, i4, i73, env, static) -{0,0}> main_Load_142(i1, i4, i73, env, static) :|: 0 >= 0

(8) Obligation:

IntTrs with 6 rules
Start term: main_Load_1(#0, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_Load_1(i1, env, static) -{25,25}> main_Load_142(i1, i4', i8', env, static'1) :|: 0 >= 0 && i1 * 100 = i4' && i1 * 200 = i6' && static'1 <= static''' + 1 && 0 <= 2 && 0 <= static''' && static''' <= static + 2 && 0 < 1 && 0 <= 1 && 0 <= static && 0 < 2 && 0 <= static'1
main_Load_142(i1, i4, i33, env, static) -{3,3}> main_LE_153(i1, i46', i4, i33, env, static) :|: 0 >= 0 && i4 + i33 = i46'
main_LE_153(i1, i53, i4, i33, env, static) -{0,0}> main_LE_155(i1, i53, i4, i33, env, static) :|: i53 <= 0
main_LE_153(i1, i54, i4, i33, env, static) -{11,11}> main_LE_178(i1, i63', 9, i4, i33, env, static) :|: 1 <= i54 && 0 < 1 && i59' * i62' = i63' && 0 < i54
main_LE_178(i1, i69, 9, i4, i33, env, static) -{3,3}> main_Load_142(i1, i75', i33, env, static) :|: 0 >= 0 && 10 <= i69 && i4 + -1 = i75' && 9 < i69
main_LE_178(i1, i68, 9, i4, i33, env, static) -{3,3}> main_Load_142(i1, i4, i73', env, static) :|: 0 >= 0 && i68 <= 9 && i33 + -1 = i73'

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

Moved arithmethic from lhss to constraints.

main_LE_178(i1, i68, 9, i4, i33, env, static) -{3,3}> main_Load_142(i1, i4, i73', env, static) :|: 0 >= 0 && i68 <= 9 && i33 + -1 = i73'
was transformed to
main_LE_178(i1, i68, x, i4, i33, env, static) -{3,3}> main_Load_142(i1, i4, i73', env, static) :|: 0 >= 0 && i68 <= 9 && i33 + -1 = i73' && x = 9

main_LE_178(i1, i69, 9, i4, i33, env, static) -{3,3}> main_Load_142(i1, i75', i33, env, static) :|: 0 >= 0 && 10 <= i69 && i4 + -1 = i75' && 9 < i69
was transformed to
main_LE_178(i1, i69, x, i4, i33, env, static) -{3,3}> main_Load_142(i1, i75', i33, env, static) :|: 0 >= 0 && 10 <= i69 && i4 + -1 = i75' && 9 < i69 && x = 9

(10) Obligation:

IntTrs with 6 rules
Start term: main_Load_1(#0, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_LE_153(i1, i53, i4, i33, env, static) -{0,0}> main_LE_155(i1, i53, i4, i33, env, static) :|: i53 <= 0
main_Load_142(i1, i4, i33, env, static) -{3,3}> main_LE_153(i1, i46', i4, i33, env, static) :|: 0 >= 0 && i4 + i33 = i46'
main_Load_1(i1, env, static) -{25,25}> main_Load_142(i1, i4', i8', env, static'1) :|: 0 >= 0 && i1 * 100 = i4' && i1 * 200 = i6' && static'1 <= static''' + 1 && 0 <= 2 && 0 <= static''' && static''' <= static + 2 && 0 < 1 && 0 <= 1 && 0 <= static && 0 < 2 && 0 <= static'1
main_LE_178(i1, i68, x, i4, i33, env, static) -{3,3}> main_Load_142(i1, i4, i73', env, static) :|: 0 >= 0 && i68 <= 9 && i33 + -1 = i73' && x = 9
main_LE_178(i1, i69, x, i4, i33, env, static) -{3,3}> main_Load_142(i1, i75', i33, env, static) :|: 0 >= 0 && 10 <= i69 && i4 + -1 = i75' && 9 < i69 && x = 9
main_LE_153(i1, i54, i4, i33, env, static) -{11,11}> main_LE_178(i1, i63', 9, i4, i33, env, static) :|: 1 <= i54 && 0 < 1 && i59' * i62' = i63' && 0 < i54

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

Moved arithmethic from constraints to rhss.

main_Load_142(i1, i4, i33, env, static) -{3,3}> main_LE_153(i1, i46', i4, i33, env, static) :|: 0 >= 0 && i4 + i33 = i46'
was transformed to
main_Load_142(i1, i4, i33, env, static) -{3,3}> main_LE_153(i1, i4 + i33, i4, i33, env, static) :|: 0 >= 0 && i4 + i33 = i46'

main_LE_178(i1, i68, x, i4, i33, env, static) -{3,3}> main_Load_142(i1, i4, i73', env, static) :|: 0 >= 0 && i68 <= 9 && i33 + -1 = i73' && x = 9
was transformed to
main_LE_178(i1, i68, x, i4, i33, env, static) -{3,3}> main_Load_142(i1, i4, i33 + -1, env, static) :|: 0 >= 0 && i68 <= 9 && i33 + -1 = i73' && x = 9

main_Load_1(i1, env, static) -{25,25}> main_Load_142(i1, i4', i8', env, static'1) :|: 0 >= 0 && i1 * 100 = i4' && i1 * 200 = i6' && static'1 <= static''' + 1 && 0 <= 2 && 0 <= static''' && static''' <= static + 2 && 0 < 1 && 0 <= 1 && 0 <= static && 0 < 2 && 0 <= static'1
was transformed to
main_Load_1(i1, env, static) -{25,25}> main_Load_142(i1, i1 * 100, i8', env, static'1) :|: 0 >= 0 && i1 * 100 = i4' && i1 * 200 = i6' && static'1 <= static''' + 1 && 0 <= 2 && 0 <= static''' && static''' <= static + 2 && 0 < 1 && 0 <= 1 && 0 <= static && 0 < 2 && 0 <= static'1

main_LE_153(i1, i54, i4, i33, env, static) -{11,11}> main_LE_178(i1, i63', 9, i4, i33, env, static) :|: 1 <= i54 && 0 < 1 && i59' * i62' = i63' && 0 < i54
was transformed to
main_LE_153(i1, i54, i4, i33, env, static) -{11,11}> main_LE_178(i1, i59' * i62', 9, i4, i33, env, static) :|: 1 <= i54 && 0 < 1 && i59' * i62' = i63' && 0 < i54

main_LE_178(i1, i69, x, i4, i33, env, static) -{3,3}> main_Load_142(i1, i75', i33, env, static) :|: 0 >= 0 && 10 <= i69 && i4 + -1 = i75' && 9 < i69 && x = 9
was transformed to
main_LE_178(i1, i69, x, i4, i33, env, static) -{3,3}> main_Load_142(i1, i4 + -1, i33, env, static) :|: 0 >= 0 && 10 <= i69 && i4 + -1 = i75' && 9 < i69 && x = 9

(12) Obligation:

IntTrs with 6 rules
Start term: main_Load_1(#0, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_LE_153(i1, i53, i4, i33, env, static) -{0,0}> main_LE_155(i1, i53, i4, i33, env, static) :|: i53 <= 0
main_Load_142(i1, i4, i33, env, static) -{3,3}> main_LE_153(i1, i4 + i33, i4, i33, env, static) :|: 0 >= 0 && i4 + i33 = i46'
main_LE_178(i1, i68, x, i4, i33, env, static) -{3,3}> main_Load_142(i1, i4, i33 + -1, env, static) :|: 0 >= 0 && i68 <= 9 && i33 + -1 = i73' && x = 9
main_Load_1(i1, env, static) -{25,25}> main_Load_142(i1, i1 * 100, i8', env, static'1) :|: 0 >= 0 && i1 * 100 = i4' && i1 * 200 = i6' && static'1 <= static''' + 1 && 0 <= 2 && 0 <= static''' && static''' <= static + 2 && 0 < 1 && 0 <= 1 && 0 <= static && 0 < 2 && 0 <= static'1
main_LE_153(i1, i54, i4, i33, env, static) -{11,11}> main_LE_178(i1, i59' * i62', 9, i4, i33, env, static) :|: 1 <= i54 && 0 < 1 && i59' * i62' = i63' && 0 < i54
main_LE_178(i1, i69, x, i4, i33, env, static) -{3,3}> main_Load_142(i1, i4 + -1, i33, env, static) :|: 0 >= 0 && 10 <= i69 && i4 + -1 = i75' && 9 < i69 && x = 9

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

Simplified expressions.

main_LE_178(i1, i69, x, i4, i33, env, static) -{3,3}> main_Load_142(i1, i4 + -1, i33, env, static) :|: 0 >= 0 && 10 <= i69 && i4 + -1 = i75' && 9 < i69 && x = 9
was transformed to
main_LE_178(i1, i69, x, i4, i33, env, static) -{3,3}> main_Load_142(i1, i4 - 1, i33, env, static) :|: 10 <= i69 && i4 - 1 = i75' && 9 < i69 && x = 9

main_LE_153(i1, i54, i4, i33, env, static) -{11,11}> main_LE_178(i1, i59' * i62', 9, i4, i33, env, static) :|: 1 <= i54 && 0 < 1 && i59' * i62' = i63' && 0 < i54
was transformed to
main_LE_153(i1, i54, i4, i33, env, static) -{11,11}> main_LE_178(i1, i59' * i62', 9, i4, i33, env, static) :|: 1 <= i54 && i59' * i62' = i63' && 0 < i54

main_LE_178(i1, i68, x, i4, i33, env, static) -{3,3}> main_Load_142(i1, i4, i33 + -1, env, static) :|: 0 >= 0 && i68 <= 9 && i33 + -1 = i73' && x = 9
was transformed to
main_LE_178(i1, i68, x, i4, i33, env, static) -{3,3}> main_Load_142(i1, i4, i33 - 1, env, static) :|: i68 <= 9 && i33 - 1 = i73' && x = 9

main_Load_142(i1, i4, i33, env, static) -{3,3}> main_LE_153(i1, i4 + i33, i4, i33, env, static) :|: 0 >= 0 && i4 + i33 = i46'
was transformed to
main_Load_142(i1, i4, i33, env, static) -{3,3}> main_LE_153(i1, i4 + i33, i4, i33, env, static) :|: i4 + i33 = i46'

main_Load_1(i1, env, static) -{25,25}> main_Load_142(i1, i1 * 100, i8', env, static'1) :|: 0 >= 0 && i1 * 100 = i4' && i1 * 200 = i6' && static'1 <= static''' + 1 && 0 <= 2 && 0 <= static''' && static''' <= static + 2 && 0 < 1 && 0 <= 1 && 0 <= static && 0 < 2 && 0 <= static'1
was transformed to
main_Load_1(i1, env, static) -{25,25}> main_Load_142(i1, 100 * i1, i8', env, static'1) :|: 100 * i1 = i4' && 200 * i1 = i6' && static'1 <= static''' + 1 && 0 <= static''' && static''' <= static + 2 && 0 <= static && 0 <= static'1

(14) Obligation:

IntTrs with 6 rules
Start term: main_Load_1(#0, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_LE_153(i1, i53, i4, i33, env, static) -{0,0}> main_LE_155(i1, i53, i4, i33, env, static) :|: i53 <= 0
main_LE_178(i1, i69, x, i4, i33, env, static) -{3,3}> main_Load_142(i1, i4 - 1, i33, env, static) :|: 10 <= i69 && i4 - 1 = i75' && 9 < i69 && x = 9
main_LE_153(i1, i54, i4, i33, env, static) -{11,11}> main_LE_178(i1, i59' * i62', 9, i4, i33, env, static) :|: 1 <= i54 && i59' * i62' = i63' && 0 < i54
main_Load_142(i1, i4, i33, env, static) -{3,3}> main_LE_153(i1, i4 + i33, i4, i33, env, static) :|: i4 + i33 = i46'
main_LE_178(i1, i68, x, i4, i33, env, static) -{3,3}> main_Load_142(i1, i4, i33 - 1, env, static) :|: i68 <= 9 && i33 - 1 = i73' && x = 9
main_Load_1(i1, env, static) -{25,25}> main_Load_142(i1, 100 * i1, i8', env, static'1) :|: 100 * i1 = i4' && 200 * i1 = i6' && static'1 <= static''' + 1 && 0 <= static''' && static''' <= static + 2 && 0 <= static && 0 <= static'1

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

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

IntTrs with 60 rules
Start term: main_Load_1(#0, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_Load_1(i1, env, static) -{0,0}> main_Load_3(i1, env, static) :|: 0 >= 0
main_Load_3(i1, env, static) -{0,0}> langle_clinit_rangle_ConstantStackPush_6(i1, env, static) :|: 0 >= 0
langle_clinit_rangle_ConstantStackPush_6(i1, env, static) -{1,1}> langle_clinit_rangle_ArrayCreate_12(iconst_0, i1, env, static) :|: iconst_0 = 0
langle_clinit_rangle_ArrayCreate_12(iconst_0, i1, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_14(a2, i1, iconst_0, env, static) :|: a2 = 2 && iconst_0 = 0 && 0 < a2
langle_clinit_rangle_FieldAccess_14(a2, i1, iconst_0, env, static) -{1,1}> langle_clinit_rangle_New_16(i1, env, static') :|: 0 <= a2 && iconst_0 = 0 && static' <= static + a2 && 0 <= static && 0 < a2
langle_clinit_rangle_New_16(i1, env, static) -{0,0}> langle_clinit_rangle_New_17(i1, env, static) :|: 0 >= 0
langle_clinit_rangle_New_17(i1, env, static) -{0,0}> langle_clinit_rangle_New_19(i1, env, static) :|: 0 <= static
langle_clinit_rangle_New_19(i1, env, static) -{1,1}> langle_clinit_rangle_Duplicate_20(o2, i1, env, static) :|: 0 < o2 && o2 = 1
langle_clinit_rangle_Duplicate_20(o2, i1, env, static) -{1,1}> langle_clinit_rangle_ConstantStackPush_22(o2, i1, env, static) :|: 0 < o2
langle_clinit_rangle_ConstantStackPush_22(o2, i1, env, static) -{1,1}> langle_clinit_rangle_InvokeMethod_23(o2, NULL, i1, env, static) :|: NULL = 0 && 0 < o2
langle_clinit_rangle_InvokeMethod_23(o2, NULL, i1, env, static) -{1,1}> langle_init_rangle_Load_24(o2, i1, env, static) :|: NULL = 0 && 0 < o2
langle_init_rangle_Load_24(o2, i1, env, static) -{1,1}> langle_init_rangle_InvokeMethod_27(o2, i1, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_27(o2, i1, env, static) -{1,1}> langle_init_rangle_Load_28(o2, i1, env, static) :|: 0 < o2
langle_init_rangle_Load_28(o2, i1, env, static) -{1,1}> langle_init_rangle_InvokeMethod_30(o2, i1, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_30(o2, i1, env, static) -{1,1}> langle_init_rangle_Return_33(o2, i1, env, static) :|: 0 < o2
langle_init_rangle_Return_33(o2, i1, env, static) -{1,1}> langle_init_rangle_Return_35(o2, i1, env, static) :|: 0 < o2
langle_init_rangle_Return_35(o2, i1, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_38(o2, i1, env, static) :|: 0 < o2
langle_clinit_rangle_FieldAccess_38(o2, i1, env, static) -{1,1}> langle_clinit_rangle_Return_40(i1, env, static') :|: 0 < o2 && 0 <= o2 && 0 <= static && static' <= static + o2
langle_clinit_rangle_Return_40(i1, env, static) -{1,1}> main_Load_41(i1, env, static) :|: 0 >= 0
main_Load_41(i1, env, static) -{0,0}> main_Load_42(i1, env, static) :|: 0 >= 0
main_Load_42(i1, env, static) -{0,0}> main_Load_44(i1, env, static) :|: 0 <= static
main_Load_44(i1, env, static) -{0,0}> main_Load_46(i1, env, static) :|: 0 >= 0
main_Load_46(i1, env, static) -{0,0}> main_Load_48(i1, env, static) :|: 0 >= 0
main_Load_48(i1, env, static) -{1,1}> main_ConstantStackPush_50(i1, env, static) :|: 0 >= 0
main_ConstantStackPush_50(i1, env, static) -{1,1}> main_IntArithmetic_52(i1, iconst_100, env, static) :|: iconst_100 = 100
main_IntArithmetic_52(i1, iconst_100, env, static) -{1,1}> main_Store_54(i1, i4, env, static) :|: i1 * iconst_100 = i4 && iconst_100 = 100
main_Store_54(i1, i4, env, static) -{1,1}> main_Load_56(i1, i4, env, static) :|: 0 >= 0
main_Load_56(i1, i4, env, static) -{1,1}> main_ConstantStackPush_58(i1, i4, env, static) :|: 0 >= 0
main_ConstantStackPush_58(i1, i4, env, static) -{1,1}> main_IntArithmetic_60(i1, iconst_200, i4, env, static) :|: iconst_200 = 200
main_IntArithmetic_60(i1, iconst_200, i4, env, static) -{1,1}> main_ConstantStackPush_63(i1, i6, i4, env, static) :|: i1 * iconst_200 = i6 && iconst_200 = 200
main_ConstantStackPush_63(i1, i6, i4, env, static) -{1,1}> main_IntArithmetic_65(i1, i6, iconst_13, i4, env, static) :|: iconst_13 = 13
main_IntArithmetic_65(i1, i6, iconst_13, i4, env, static) -{1,1}> main_Store_67(i1, i8, i4, env, static) :|: i6 / iconst_13 = i8 && iconst_13 = 13
main_Store_67(i1, i8, i4, env, static) -{1,1}> main_Load_70(i1, i4, i8, env, static) :|: 0 >= 0
main_Load_70(i1, i4, i8, env, static) -{0,0}> main_Load_142(i1, i4, i8, env, static) :|: 0 >= 0
main_Load_142(i1, i4, i33, env, static) -{1,1}> main_Load_148(i1, i4, i33, env, static) :|: 0 >= 0
main_Load_148(i1, i4, i33, env, static) -{1,1}> main_IntArithmetic_150(i1, i4, i33, env, static) :|: 0 >= 0
main_IntArithmetic_150(i1, i4, i33, env, static) -{1,1}> main_LE_153(i1, i46, i4, i33, env, static) :|: i4 + i33 = i46
main_LE_153(i1, i53, i4, i33, env, static) -{0,0}> main_LE_155(i1, i53, i4, i33, env, static) :|: i53 <= 0
main_LE_153(i1, i54, i4, i33, env, static) -{0,0}> main_LE_156(i1, i54, i4, i33, env, static) :|: 1 <= i54
main_LE_156(i1, i54, i4, i33, env, static) -{1,1}> main_New_161(i1, i4, i33, env, static) :|: 1 <= i54 && 0 < i54
main_New_161(i1, i4, i33, env, static) -{1,1}> main_Duplicate_164(i1, o12, i4, i33, env, static) :|: 0 < o12 && o12 = 1
main_Duplicate_164(i1, o12, i4, i33, env, static) -{1,1}> main_InvokeMethod_165(i1, o12, i4, i33, env, static) :|: 0 < o12
main_InvokeMethod_165(i1, o12, i4, i33, env, static) -{1,1}> main_InvokeMethod_166(i1, o12, i4, i33, env, static) :|: 0 < o12
main_InvokeMethod_166(i1, o12, i4, i33, env, static) -{1,1}> main_New_169(i1, i59, i4, i33, env, static) :|: 0 < o12
main_New_169(i1, i59, i4, i33, env, static) -{1,1}> main_Duplicate_170(i1, i59, o13, i4, i33, env, static) :|: 0 < o13 && o13 = 1
main_Duplicate_170(i1, i59, o13, i4, i33, env, static) -{1,1}> main_InvokeMethod_171(i1, i59, o13, i4, i33, env, static) :|: 0 < o13
main_InvokeMethod_171(i1, i59, o13, i4, i33, env, static) -{1,1}> main_InvokeMethod_174(i1, i59, o13, i4, i33, env, static) :|: 0 < o13
main_InvokeMethod_174(i1, i59, o13, i4, i33, env, static) -{1,1}> main_IntArithmetic_175(i1, i59, i62, i4, i33, env, static) :|: 0 < o13
main_IntArithmetic_175(i1, i59, i62, i4, i33, env, static) -{1,1}> main_ConstantStackPush_176(i1, i63, i4, i33, env, static) :|: i59 * i62 = i63
main_ConstantStackPush_176(i1, i63, i4, i33, env, static) -{1,1}> main_LE_178(i1, i63, iconst_9, i4, i33, env, static) :|: iconst_9 = 9
main_LE_178(i1, i68, iconst_9, i4, i33, env, static) -{0,0}> main_LE_179(i1, i68, iconst_9, i4, i33, env, static) :|: i68 <= 9 && iconst_9 = 9
main_LE_178(i1, i69, iconst_9, i4, i33, env, static) -{0,0}> main_LE_180(i1, i69, iconst_9, i4, i33, env, static) :|: 10 <= i69 && iconst_9 = 9
main_LE_179(i1, i68, iconst_9, i4, i33, env, static) -{1,1}> main_Inc_183(i1, i4, i33, env, static) :|: i68 <= iconst_9 && i68 <= 9 && iconst_9 = 9
main_LE_180(i1, i69, iconst_9, i4, i33, env, static) -{1,1}> main_Inc_186(i1, i4, i33, env, static) :|: iconst_9 < i69 && 10 <= i69 && iconst_9 = 9
main_Inc_183(i1, i4, i33, env, static) -{1,1}> main_JMP_190(i1, i4, i73, env, static) :|: i33 + -1 = i73
main_Inc_186(i1, i4, i33, env, static) -{1,1}> main_JMP_193(i1, i75, i33, env, static) :|: i4 + -1 = i75
main_JMP_190(i1, i4, i73, env, static) -{1,1}> main_Load_200(i1, i4, i73, env, static) :|: 0 >= 0
main_JMP_193(i1, i75, i33, env, static) -{1,1}> main_Load_207(i1, i75, i33, env, static) :|: 0 >= 0
main_Load_200(i1, i4, i73, env, static) -{0,0}> main_Load_142(i1, i4, i73, env, static) :|: 0 >= 0
main_Load_207(i1, i75, i33, env, static) -{0,0}> main_Load_142(i1, i75, i33, env, static) :|: 0 >= 0

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

obtained
main_Load_1(i1, env, static) -{25,25}> main_Load_142(i1, i4', i8', env, static'1) :|: 0 >= 0 && i6' / 13 = i8' && i1 * 200 = i6' && i1 * 100 = i4' && static'1 <= static''' + 1 && 0 <= 2 && 0 <= static''' && static''' <= static + 2 && 0 < 1 && 0 <= 1 && 0 <= static && 0 < 2 && 0 <= static'1
by chaining
main_Load_1(i1, env, static) -{0,0}> main_Load_3(i1, env, static) :|: 0 >= 0
main_Load_3(i1, env, static) -{0,0}> langle_clinit_rangle_ConstantStackPush_6(i1, env, static) :|: 0 >= 0
langle_clinit_rangle_ConstantStackPush_6(i1, env, static) -{1,1}> langle_clinit_rangle_ArrayCreate_12(iconst_0, i1, env, static) :|: iconst_0 = 0
langle_clinit_rangle_ArrayCreate_12(iconst_0, i1, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_14(a2, i1, iconst_0, env, static) :|: a2 = 2 && iconst_0 = 0 && 0 < a2
langle_clinit_rangle_FieldAccess_14(a2, i1, iconst_0, env, static) -{1,1}> langle_clinit_rangle_New_16(i1, env, static') :|: 0 <= a2 && iconst_0 = 0 && static' <= static + a2 && 0 <= static && 0 < a2
langle_clinit_rangle_New_16(i1, env, static) -{0,0}> langle_clinit_rangle_New_17(i1, env, static) :|: 0 >= 0
langle_clinit_rangle_New_17(i1, env, static) -{0,0}> langle_clinit_rangle_New_19(i1, env, static) :|: 0 <= static
langle_clinit_rangle_New_19(i1, env, static) -{1,1}> langle_clinit_rangle_Duplicate_20(o2, i1, env, static) :|: 0 < o2 && o2 = 1
langle_clinit_rangle_Duplicate_20(o2, i1, env, static) -{1,1}> langle_clinit_rangle_ConstantStackPush_22(o2, i1, env, static) :|: 0 < o2
langle_clinit_rangle_ConstantStackPush_22(o2, i1, env, static) -{1,1}> langle_clinit_rangle_InvokeMethod_23(o2, NULL, i1, env, static) :|: NULL = 0 && 0 < o2
langle_clinit_rangle_InvokeMethod_23(o2, NULL, i1, env, static) -{1,1}> langle_init_rangle_Load_24(o2, i1, env, static) :|: NULL = 0 && 0 < o2
langle_init_rangle_Load_24(o2, i1, env, static) -{1,1}> langle_init_rangle_InvokeMethod_27(o2, i1, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_27(o2, i1, env, static) -{1,1}> langle_init_rangle_Load_28(o2, i1, env, static) :|: 0 < o2
langle_init_rangle_Load_28(o2, i1, env, static) -{1,1}> langle_init_rangle_InvokeMethod_30(o2, i1, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_30(o2, i1, env, static) -{1,1}> langle_init_rangle_Return_33(o2, i1, env, static) :|: 0 < o2
langle_init_rangle_Return_33(o2, i1, env, static) -{1,1}> langle_init_rangle_Return_35(o2, i1, env, static) :|: 0 < o2
langle_init_rangle_Return_35(o2, i1, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_38(o2, i1, env, static) :|: 0 < o2
langle_clinit_rangle_FieldAccess_38(o2, i1, env, static) -{1,1}> langle_clinit_rangle_Return_40(i1, env, static') :|: 0 < o2 && 0 <= o2 && 0 <= static && static' <= static + o2
langle_clinit_rangle_Return_40(i1, env, static) -{1,1}> main_Load_41(i1, env, static) :|: 0 >= 0
main_Load_41(i1, env, static) -{0,0}> main_Load_42(i1, env, static) :|: 0 >= 0
main_Load_42(i1, env, static) -{0,0}> main_Load_44(i1, env, static) :|: 0 <= static
main_Load_44(i1, env, static) -{0,0}> main_Load_46(i1, env, static) :|: 0 >= 0
main_Load_46(i1, env, static) -{0,0}> main_Load_48(i1, env, static) :|: 0 >= 0
main_Load_48(i1, env, static) -{1,1}> main_ConstantStackPush_50(i1, env, static) :|: 0 >= 0
main_ConstantStackPush_50(i1, env, static) -{1,1}> main_IntArithmetic_52(i1, iconst_100, env, static) :|: iconst_100 = 100
main_IntArithmetic_52(i1, iconst_100, env, static) -{1,1}> main_Store_54(i1, i4, env, static) :|: i1 * iconst_100 = i4 && iconst_100 = 100
main_Store_54(i1, i4, env, static) -{1,1}> main_Load_56(i1, i4, env, static) :|: 0 >= 0
main_Load_56(i1, i4, env, static) -{1,1}> main_ConstantStackPush_58(i1, i4, env, static) :|: 0 >= 0
main_ConstantStackPush_58(i1, i4, env, static) -{1,1}> main_IntArithmetic_60(i1, iconst_200, i4, env, static) :|: iconst_200 = 200
main_IntArithmetic_60(i1, iconst_200, i4, env, static) -{1,1}> main_ConstantStackPush_63(i1, i6, i4, env, static) :|: i1 * iconst_200 = i6 && iconst_200 = 200
main_ConstantStackPush_63(i1, i6, i4, env, static) -{1,1}> main_IntArithmetic_65(i1, i6, iconst_13, i4, env, static) :|: iconst_13 = 13
main_IntArithmetic_65(i1, i6, iconst_13, i4, env, static) -{1,1}> main_Store_67(i1, i8, i4, env, static) :|: i6 / iconst_13 = i8 && iconst_13 = 13
main_Store_67(i1, i8, i4, env, static) -{1,1}> main_Load_70(i1, i4, i8, env, static) :|: 0 >= 0
main_Load_70(i1, i4, i8, env, static) -{0,0}> main_Load_142(i1, i4, i8, env, static) :|: 0 >= 0

(18) Obligation:

IntTrs with 6 rules
Start term: main_Load_1(#0, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_Load_1(i1, env, static) -{25,25}> main_Load_142(i1, i4', i8', env, static'1) :|: 0 >= 0 && i6' / 13 = i8' && i1 * 200 = i6' && i1 * 100 = i4' && static'1 <= static''' + 1 && 0 <= 2 && 0 <= static''' && static''' <= static + 2 && 0 < 1 && 0 <= 1 && 0 <= static && 0 < 2 && 0 <= static'1
main_Load_142(i1, i4, i33, env, static) -{3,3}> main_LE_153(i1, i46', i4, i33, env, static) :|: 0 >= 0 && i4 + i33 = i46'
main_LE_153(i1, i53, i4, i33, env, static) -{0,0}> main_LE_155(i1, i53, i4, i33, env, static) :|: i53 <= 0
main_LE_153(i1, i54, i4, i33, env, static) -{11,11}> main_LE_178(i1, i63', 9, i4, i33, env, static) :|: 1 <= i54 && 0 < 1 && i59' * i62' = i63' && 0 < i54
main_LE_178(i1, i69, 9, i4, i33, env, static) -{3,3}> main_Load_142(i1, i75', i33, env, static) :|: 0 >= 0 && 10 <= i69 && i4 + -1 = i75' && 9 < i69
main_LE_178(i1, i68, 9, i4, i33, env, static) -{3,3}> main_Load_142(i1, i4, i73', env, static) :|: 0 >= 0 && i68 <= 9 && i33 + -1 = i73'

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

Moved arithmethic from lhss to constraints.

(20) Obligation:

IntTrs with 6 rules
Start term: main_Load_1(#0, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_LE_153(i1, i53, i4, i33, env, static) -{0,0}> main_LE_155(i1, i53, i4, i33, env, static) :|: i53 <= 0
main_Load_142(i1, i4, i33, env, static) -{3,3}> main_LE_153(i1, i46', i4, i33, env, static) :|: 0 >= 0 && i4 + i33 = i46'
main_Load_1(i1, env, static) -{25,25}> main_Load_142(i1, i4', i8', env, static'1) :|: 0 >= 0 && i6' / 13 = i8' && i1 * 200 = i6' && i1 * 100 = i4' && static'1 <= static''' + 1 && 0 <= 2 && 0 <= static''' && static''' <= static + 2 && 0 < 1 && 0 <= 1 && 0 <= static && 0 < 2 && 0 <= static'1
main_LE_178(i1, i68, x, i4, i33, env, static) -{3,3}> main_Load_142(i1, i4, i73', env, static) :|: 0 >= 0 && i68 <= 9 && i33 + -1 = i73' && x = 9
main_LE_178(i1, i69, x, i4, i33, env, static) -{3,3}> main_Load_142(i1, i75', i33, env, static) :|: 0 >= 0 && 10 <= i69 && i4 + -1 = i75' && 9 < i69 && x = 9
main_LE_153(i1, i54, i4, i33, env, static) -{11,11}> main_LE_178(i1, i63', 9, i4, i33, env, static) :|: 1 <= i54 && 0 < 1 && i59' * i62' = i63' && 0 < i54

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

Removed div and mod.

main_Load_1(i1, env, static) -{25,25}> main_Load_142(i1, i4', i8', env, static'1) :|: 0 >= 0 && i6' / 13 = i8' && i1 * 200 = i6' && i1 * 100 = i4' && static'1 <= static''' + 1 && 0 <= 2 && 0 <= static''' && static''' <= static + 2 && 0 < 1 && 0 <= 1 && 0 <= static && 0 < 2 && 0 <= static'1
was transformed to
main_Load_1'(i1, env, static) -{25,25}> main_Load_142(i1, i4', i8', env, static'1) :|: i6' - 13 * div < 13 && i6' - 13 * div + 13 > 0 && 0 >= 0 && div = i8' && i1 * 200 = i6' && i1 * 100 = i4' && static'1 <= static''' + 1 && 0 <= 2 && 0 <= static''' && static''' <= static + 2 && 0 < 1 && 0 <= 1 && 0 <= static && 0 < 2 && 0 <= static'1
main_Load_1(i1, env, static) -{25,25}> main_Load_1'(i1, env, static) :|: 0 >= 0 && div = i8' && i1 * 200 = i6' && i1 * 100 = i4' && static'1 <= static''' + 1 && 0 <= 2 && 0 <= static''' && static''' <= static + 2 && 0 < 1 && 0 <= 1 && 0 <= static && 0 < 2 && 0 <= static'1

(22) Obligation:

IntTrs with 7 rules
Start term: main_Load_1(#0, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_LE_153(i1, i53, i4, i33, env, static) -{0,0}> main_LE_155(i1, i53, i4, i33, env, static) :|: i53 <= 0
main_Load_142(i1, i4, i33, env, static) -{3,3}> main_LE_153(i1, i46', i4, i33, env, static) :|: 0 >= 0 && i4 + i33 = i46'
main_Load_1'(i1, env, static) -{25,25}> main_Load_142(i1, i4', i8', env, static'1) :|: i6' - 13 * div < 13 && i6' - 13 * div + 13 > 0 && 0 >= 0 && div = i8' && i1 * 200 = i6' && i1 * 100 = i4' && static'1 <= static''' + 1 && 0 <= 2 && 0 <= static''' && static''' <= static + 2 && 0 < 1 && 0 <= 1 && 0 <= static && 0 < 2 && 0 <= static'1
main_LE_178(i1, i68, x, i4, i33, env, static) -{3,3}> main_Load_142(i1, i4, i73', env, static) :|: 0 >= 0 && i68 <= 9 && i33 + -1 = i73' && x = 9
main_Load_1(i1, env, static) -{25,25}> main_Load_1'(i1, env, static) :|: 0 >= 0 && div = i8' && i1 * 200 = i6' && i1 * 100 = i4' && static'1 <= static''' + 1 && 0 <= 2 && 0 <= static''' && static''' <= static + 2 && 0 < 1 && 0 <= 1 && 0 <= static && 0 < 2 && 0 <= static'1
main_LE_153(i1, i54, i4, i33, env, static) -{11,11}> main_LE_178(i1, i63', 9, i4, i33, env, static) :|: 1 <= i54 && 0 < 1 && i59' * i62' = i63' && 0 < i54
main_LE_178(i1, i69, x, i4, i33, env, static) -{3,3}> main_Load_142(i1, i75', i33, env, static) :|: 0 >= 0 && 10 <= i69 && i4 + -1 = i75' && 9 < i69 && x = 9

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

Moved arithmethic from constraints to rhss.

main_Load_1'(i1, env, static) -{25,25}> main_Load_142(i1, i4', i8', env, static'1) :|: i6' - 13 * div < 13 && i6' - 13 * div + 13 > 0 && 0 >= 0 && div = i8' && i1 * 200 = i6' && i1 * 100 = i4' && static'1 <= static''' + 1 && 0 <= 2 && 0 <= static''' && static''' <= static + 2 && 0 < 1 && 0 <= 1 && 0 <= static && 0 < 2 && 0 <= static'1
was transformed to
main_Load_1'(i1, env, static) -{25,25}> main_Load_142(i1, i1 * 100, i8', env, static'1) :|: i6' - 13 * div < 13 && i6' - 13 * div + 13 > 0 && 0 >= 0 && div = i8' && i1 * 200 = i6' && i1 * 100 = i4' && static'1 <= static''' + 1 && 0 <= 2 && 0 <= static''' && static''' <= static + 2 && 0 < 1 && 0 <= 1 && 0 <= static && 0 < 2 && 0 <= static'1

(24) Obligation:

IntTrs with 7 rules
Start term: main_Load_1(#0, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_LE_153(i1, i53, i4, i33, env, static) -{0,0}> main_LE_155(i1, i53, i4, i33, env, static) :|: i53 <= 0
main_Load_142(i1, i4, i33, env, static) -{3,3}> main_LE_153(i1, i4 + i33, i4, i33, env, static) :|: 0 >= 0 && i4 + i33 = i46'
main_Load_1'(i1, env, static) -{25,25}> main_Load_142(i1, i1 * 100, i8', env, static'1) :|: i6' - 13 * div < 13 && i6' - 13 * div + 13 > 0 && 0 >= 0 && div = i8' && i1 * 200 = i6' && i1 * 100 = i4' && static'1 <= static''' + 1 && 0 <= 2 && 0 <= static''' && static''' <= static + 2 && 0 < 1 && 0 <= 1 && 0 <= static && 0 < 2 && 0 <= static'1
main_Load_1(i1, env, static) -{25,25}> main_Load_1'(i1, env, static) :|: 0 >= 0 && div = i8' && i1 * 200 = i6' && i1 * 100 = i4' && static'1 <= static''' + 1 && 0 <= 2 && 0 <= static''' && static''' <= static + 2 && 0 < 1 && 0 <= 1 && 0 <= static && 0 < 2 && 0 <= static'1
main_LE_178(i1, i68, x, i4, i33, env, static) -{3,3}> main_Load_142(i1, i4, i33 + -1, env, static) :|: 0 >= 0 && i68 <= 9 && i33 + -1 = i73' && x = 9
main_LE_178(i1, i69, x, i4, i33, env, static) -{3,3}> main_Load_142(i1, i4 + -1, i33, env, static) :|: 0 >= 0 && 10 <= i69 && i4 + -1 = i75' && 9 < i69 && x = 9
main_LE_153(i1, i54, i4, i33, env, static) -{11,11}> main_LE_178(i1, i59' * i62', 9, i4, i33, env, static) :|: 1 <= i54 && 0 < 1 && i59' * i62' = i63' && 0 < i54

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

Simplified expressions.

main_Load_1(i1, env, static) -{25,25}> main_Load_1'(i1, env, static) :|: 0 >= 0 && div = i8' && i1 * 200 = i6' && i1 * 100 = i4' && static'1 <= static''' + 1 && 0 <= 2 && 0 <= static''' && static''' <= static + 2 && 0 < 1 && 0 <= 1 && 0 <= static && 0 < 2 && 0 <= static'1
was transformed to
main_Load_1(i1, env, static) -{25,25}> main_Load_1'(i1, env, static) :|: div = i8' && 200 * i1 = i6' && 100 * i1 = i4' && static'1 <= static''' + 1 && 0 <= static''' && static''' <= static + 2 && 0 <= static && 0 <= static'1

main_Load_1'(i1, env, static) -{25,25}> main_Load_142(i1, i1 * 100, i8', env, static'1) :|: i6' - 13 * div < 13 && i6' - 13 * div + 13 > 0 && 0 >= 0 && div = i8' && i1 * 200 = i6' && i1 * 100 = i4' && static'1 <= static''' + 1 && 0 <= 2 && 0 <= static''' && static''' <= static + 2 && 0 < 1 && 0 <= 1 && 0 <= static && 0 < 2 && 0 <= static'1
was transformed to
main_Load_1'(i1, env, static) -{25,25}> main_Load_142(i1, 100 * i1, i8', env, static'1) :|: i6' + -13 * div < 13 && 0 < i6' + -13 * div + 13 && div = i8' && 200 * i1 = i6' && 100 * i1 = i4' && static'1 <= static''' + 1 && 0 <= static''' && static''' <= static + 2 && 0 <= static && 0 <= static'1

(26) Obligation:

IntTrs with 7 rules
Start term: main_Load_1(#0, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_LE_153(i1, i53, i4, i33, env, static) -{0,0}> main_LE_155(i1, i53, i4, i33, env, static) :|: i53 <= 0
main_LE_178(i1, i69, x, i4, i33, env, static) -{3,3}> main_Load_142(i1, i4 - 1, i33, env, static) :|: 10 <= i69 && i4 - 1 = i75' && 9 < i69 && x = 9
main_LE_153(i1, i54, i4, i33, env, static) -{11,11}> main_LE_178(i1, i59' * i62', 9, i4, i33, env, static) :|: 1 <= i54 && i59' * i62' = i63' && 0 < i54
main_Load_142(i1, i4, i33, env, static) -{3,3}> main_LE_153(i1, i4 + i33, i4, i33, env, static) :|: i4 + i33 = i46'
main_Load_1(i1, env, static) -{25,25}> main_Load_1'(i1, env, static) :|: div = i8' && 200 * i1 = i6' && 100 * i1 = i4' && static'1 <= static''' + 1 && 0 <= static''' && static''' <= static + 2 && 0 <= static && 0 <= static'1
main_LE_178(i1, i68, x, i4, i33, env, static) -{3,3}> main_Load_142(i1, i4, i33 - 1, env, static) :|: i68 <= 9 && i33 - 1 = i73' && x = 9
main_Load_1'(i1, env, static) -{25,25}> main_Load_142(i1, 100 * i1, i8', env, static'1) :|: i6' + -13 * div < 13 && 0 < i6' + -13 * div + 13 && div = i8' && 200 * i1 = i6' && 100 * i1 = i4' && static'1 <= static''' + 1 && 0 <= static''' && static''' <= static + 2 && 0 <= static && 0 <= static'1

(27) koat Proof (EQUIVALENT transformation)

YES(?, 51000*ar_0 + 484)

Initial complexity problem:
1: T:
(Comp: ?, Cost: 0) main_LE_153(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5, ar_6) -> Com_1(main_LE_155(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5, arityPad)) [ ar_1 <= 0 ]
(Comp: ?, Cost: 3) main_LE_178(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5, ar_6) -> Com_1(main_Load_142(ar_0, ar_3 - 1, ar_4, ar_5, ar_6, arityPad, arityPad)) [ 10 <= ar_1 /\ ar_3 - 1 = i75' /\ 9 < ar_1 /\ ar_2 = 9 ]
(Comp: ?, Cost: 11) main_LE_153(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5, ar_6) -> Com_1(main_LE_178(ar_0, i59'*i62', 9, ar_2, ar_3, ar_4, ar_5)) [ 1 <= ar_1 /\ i59'*i62' = i63' /\ 0 < ar_1 ]
(Comp: ?, Cost: 3) main_Load_142(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5, ar_6) -> Com_1(main_LE_153(ar_0, ar_1 + ar_2, ar_1, ar_2, ar_3, ar_4, arityPad)) [ ar_1 + ar_2 = i46' ]
(Comp: ?, Cost: 25) main_Load_1(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5, ar_6) -> Com_1(main_Load_1'(ar_0, ar_1, ar_2, arityPad, arityPad, arityPad, arityPad)) [ div = i8' /\ 200*ar_0 = i6' /\ 100*ar_0 = i4' /\ static'1 <= static''' + 1 /\ 0 <= static''' /\ static''' <= ar_2 + 2 /\ 0 <= ar_2 /\ 0 <= static'1 ]
(Comp: ?, Cost: 3) main_LE_178(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5, ar_6) -> Com_1(main_Load_142(ar_0, ar_3, ar_4 - 1, ar_5, ar_6, arityPad, arityPad)) [ ar_1 <= 9 /\ ar_4 - 1 = i73' /\ ar_2 = 9 ]
(Comp: ?, Cost: 25) main_Load_1'(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5, ar_6) -> Com_1(main_Load_142(ar_0, 100*ar_0, i8', ar_1, static'1, arityPad, arityPad)) [ i6' - 13*div < 13 /\ 0 < i6' - 13*div + 13 /\ div = i8' /\ 200*ar_0 = i6' /\ 100*ar_0 = i4' /\ static'1 <= static''' + 1 /\ 0 <= static''' /\ static''' <= ar_2 + 2 /\ 0 <= ar_2 /\ 0 <= static'1 ]
(Comp: 1, Cost: 0) koat_start(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5, ar_6) -> Com_1(main_Load_1(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5, ar_6)) [ 0 <= 0 ]
start location: koat_start
leaf cost: 0

Repeatedly propagating knowledge in problem 1 produces the following problem:
2: T:
(Comp: ?, Cost: 0) main_LE_153(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5, ar_6) -> Com_1(main_LE_155(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5, arityPad)) [ ar_1 <= 0 ]
(Comp: ?, Cost: 3) main_LE_178(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5, ar_6) -> Com_1(main_Load_142(ar_0, ar_3 - 1, ar_4, ar_5, ar_6, arityPad, arityPad)) [ 10 <= ar_1 /\ ar_3 - 1 = i75' /\ 9 < ar_1 /\ ar_2 = 9 ]
(Comp: ?, Cost: 11) main_LE_153(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5, ar_6) -> Com_1(main_LE_178(ar_0, i59'*i62', 9, ar_2, ar_3, ar_4, ar_5)) [ 1 <= ar_1 /\ i59'*i62' = i63' /\ 0 < ar_1 ]
(Comp: ?, Cost: 3) main_Load_142(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5, ar_6) -> Com_1(main_LE_153(ar_0, ar_1 + ar_2, ar_1, ar_2, ar_3, ar_4, arityPad)) [ ar_1 + ar_2 = i46' ]
(Comp: 1, Cost: 25) main_Load_1(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5, ar_6) -> Com_1(main_Load_1'(ar_0, ar_1, ar_2, arityPad, arityPad, arityPad, arityPad)) [ div = i8' /\ 200*ar_0 = i6' /\ 100*ar_0 = i4' /\ static'1 <= static''' + 1 /\ 0 <= static''' /\ static''' <= ar_2 + 2 /\ 0 <= ar_2 /\ 0 <= static'1 ]
(Comp: ?, Cost: 3) main_LE_178(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5, ar_6) -> Com_1(main_Load_142(ar_0, ar_3, ar_4 - 1, ar_5, ar_6, arityPad, arityPad)) [ ar_1 <= 9 /\ ar_4 - 1 = i73' /\ ar_2 = 9 ]
(Comp: 1, Cost: 25) main_Load_1'(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5, ar_6) -> Com_1(main_Load_142(ar_0, 100*ar_0, i8', ar_1, static'1, arityPad, arityPad)) [ i6' - 13*div < 13 /\ 0 < i6' - 13*div + 13 /\ div = i8' /\ 200*ar_0 = i6' /\ 100*ar_0 = i4' /\ static'1 <= static''' + 1 /\ 0 <= static''' /\ static''' <= ar_2 + 2 /\ 0 <= ar_2 /\ 0 <= static'1 ]
(Comp: 1, Cost: 0) koat_start(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5, ar_6) -> Com_1(main_Load_1(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5, ar_6)) [ 0 <= 0 ]
start location: koat_start
leaf cost: 0

A polynomial rank function with
Pol(main_LE_153) = 1
Pol(main_LE_155) = 0
Pol(main_LE_178) = 1
Pol(main_Load_142) = 1
Pol(main_Load_1) = 1
Pol(main_Load_1') = 1
Pol(koat_start) = 1
orients all transitions weakly and the transition
main_LE_153(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5, ar_6) -> Com_1(main_LE_155(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5, arityPad)) [ ar_1 <= 0 ]
strictly and produces the following problem:
3: T:
(Comp: 1, Cost: 0) main_LE_153(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5, ar_6) -> Com_1(main_LE_155(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5, arityPad)) [ ar_1 <= 0 ]
(Comp: ?, Cost: 3) main_LE_178(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5, ar_6) -> Com_1(main_Load_142(ar_0, ar_3 - 1, ar_4, ar_5, ar_6, arityPad, arityPad)) [ 10 <= ar_1 /\ ar_3 - 1 = i75' /\ 9 < ar_1 /\ ar_2 = 9 ]
(Comp: ?, Cost: 11) main_LE_153(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5, ar_6) -> Com_1(main_LE_178(ar_0, i59'*i62', 9, ar_2, ar_3, ar_4, ar_5)) [ 1 <= ar_1 /\ i59'*i62' = i63' /\ 0 < ar_1 ]
(Comp: ?, Cost: 3) main_Load_142(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5, ar_6) -> Com_1(main_LE_153(ar_0, ar_1 + ar_2, ar_1, ar_2, ar_3, ar_4, arityPad)) [ ar_1 + ar_2 = i46' ]
(Comp: 1, Cost: 25) main_Load_1(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5, ar_6) -> Com_1(main_Load_1'(ar_0, ar_1, ar_2, arityPad, arityPad, arityPad, arityPad)) [ div = i8' /\ 200*ar_0 = i6' /\ 100*ar_0 = i4' /\ static'1 <= static''' + 1 /\ 0 <= static''' /\ static''' <= ar_2 + 2 /\ 0 <= ar_2 /\ 0 <= static'1 ]
(Comp: ?, Cost: 3) main_LE_178(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5, ar_6) -> Com_1(main_Load_142(ar_0, ar_3, ar_4 - 1, ar_5, ar_6, arityPad, arityPad)) [ ar_1 <= 9 /\ ar_4 - 1 = i73' /\ ar_2 = 9 ]
(Comp: 1, Cost: 25) main_Load_1'(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5, ar_6) -> Com_1(main_Load_142(ar_0, 100*ar_0, i8', ar_1, static'1, arityPad, arityPad)) [ i6' - 13*div < 13 /\ 0 < i6' - 13*div + 13 /\ div = i8' /\ 200*ar_0 = i6' /\ 100*ar_0 = i4' /\ static'1 <= static''' + 1 /\ 0 <= static''' /\ static''' <= ar_2 + 2 /\ 0 <= ar_2 /\ 0 <= static'1 ]
(Comp: 1, Cost: 0) koat_start(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5, ar_6) -> Com_1(main_Load_1(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5, ar_6)) [ 0 <= 0 ]
start location: koat_start
leaf cost: 0

Applied AI with 'oct' on problem 3 to obtain the following invariants:
For symbol main_LE_153: X_6 >= 0
For symbol main_LE_178: X_7 >= 0 /\ X_3 + X_7 - 9 >= 0 /\ -X_3 + X_7 + 9 >= 0 /\ -X_3 + 9 >= 0 /\ X_3 - 9 >= 0
For symbol main_Load_1': X_3 >= 0
For symbol main_Load_142: X_5 >= 0

This yielded the following problem:
4: T:
(Comp: 1, Cost: 0) koat_start(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5, ar_6) -> Com_1(main_Load_1(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5, ar_6)) [ 0 <= 0 ]
(Comp: 1, Cost: 25) main_Load_1'(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5, ar_6) -> Com_1(main_Load_142(ar_0, 100*ar_0, i8', ar_1, static'1, arityPad, arityPad)) [ ar_2 >= 0 /\ i6' - 13*div < 13 /\ 0 < i6' - 13*div + 13 /\ div = i8' /\ 200*ar_0 = i6' /\ 100*ar_0 = i4' /\ static'1 <= static''' + 1 /\ 0 <= static''' /\ static''' <= ar_2 + 2 /\ 0 <= ar_2 /\ 0 <= static'1 ]
(Comp: ?, Cost: 3) main_LE_178(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5, ar_6) -> Com_1(main_Load_142(ar_0, ar_3, ar_4 - 1, ar_5, ar_6, arityPad, arityPad)) [ ar_6 >= 0 /\ ar_2 + ar_6 - 9 >= 0 /\ -ar_2 + ar_6 + 9 >= 0 /\ -ar_2 + 9 >= 0 /\ ar_2 - 9 >= 0 /\ ar_1 <= 9 /\ ar_4 - 1 = i73' /\ ar_2 = 9 ]
(Comp: 1, Cost: 25) main_Load_1(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5, ar_6) -> Com_1(main_Load_1'(ar_0, ar_1, ar_2, arityPad, arityPad, arityPad, arityPad)) [ div = i8' /\ 200*ar_0 = i6' /\ 100*ar_0 = i4' /\ static'1 <= static''' + 1 /\ 0 <= static''' /\ static''' <= ar_2 + 2 /\ 0 <= ar_2 /\ 0 <= static'1 ]
(Comp: ?, Cost: 3) main_Load_142(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5, ar_6) -> Com_1(main_LE_153(ar_0, ar_1 + ar_2, ar_1, ar_2, ar_3, ar_4, arityPad)) [ ar_4 >= 0 /\ ar_1 + ar_2 = i46' ]
(Comp: ?, Cost: 11) main_LE_153(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5, ar_6) -> Com_1(main_LE_178(ar_0, i59'*i62', 9, ar_2, ar_3, ar_4, ar_5)) [ ar_5 >= 0 /\ 1 <= ar_1 /\ i59'*i62' = i63' /\ 0 < ar_1 ]
(Comp: ?, Cost: 3) main_LE_178(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5, ar_6) -> Com_1(main_Load_142(ar_0, ar_3 - 1, ar_4, ar_5, ar_6, arityPad, arityPad)) [ ar_6 >= 0 /\ ar_2 + ar_6 - 9 >= 0 /\ -ar_2 + ar_6 + 9 >= 0 /\ -ar_2 + 9 >= 0 /\ ar_2 - 9 >= 0 /\ 10 <= ar_1 /\ ar_3 - 1 = i75' /\ 9 < ar_1 /\ ar_2 = 9 ]
(Comp: 1, Cost: 0) main_LE_153(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5, ar_6) -> Com_1(main_LE_155(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5, arityPad)) [ ar_5 >= 0 /\ ar_1 <= 0 ]
start location: koat_start
leaf cost: 0

By chaining the transition koat_start(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5, ar_6) -> Com_1(main_Load_1(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5, ar_6)) [ 0 <= 0 ] with all transitions in problem 4, the following new transition is obtained:
koat_start(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5, ar_6) -> Com_1(main_Load_1'(ar_0, ar_1, ar_2, arityPad, arityPad, arityPad, arityPad)) [ 0 <= 0 /\ div = i8' /\ 200*ar_0 = i6' /\ 100*ar_0 = i4' /\ static'1 <= static''' + 1 /\ 0 <= static''' /\ static''' <= ar_2 + 2 /\ 0 <= ar_2 /\ 0 <= static'1 ]
We thus obtain the following problem:
5: T:
(Comp: 1, Cost: 25) koat_start(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5, ar_6) -> Com_1(main_Load_1'(ar_0, ar_1, ar_2, arityPad, arityPad, arityPad, arityPad)) [ 0 <= 0 /\ div = i8' /\ 200*ar_0 = i6' /\ 100*ar_0 = i4' /\ static'1 <= static''' + 1 /\ 0 <= static''' /\ static''' <= ar_2 + 2 /\ 0 <= ar_2 /\ 0 <= static'1 ]
(Comp: 1, Cost: 25) main_Load_1'(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5, ar_6) -> Com_1(main_Load_142(ar_0, 100*ar_0, i8', ar_1, static'1, arityPad, arityPad)) [ ar_2 >= 0 /\ i6' - 13*div < 13 /\ 0 < i6' - 13*div + 13 /\ div = i8' /\ 200*ar_0 = i6' /\ 100*ar_0 = i4' /\ static'1 <= static''' + 1 /\ 0 <= static''' /\ static''' <= ar_2 + 2 /\ 0 <= ar_2 /\ 0 <= static'1 ]
(Comp: ?, Cost: 3) main_LE_178(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5, ar_6) -> Com_1(main_Load_142(ar_0, ar_3, ar_4 - 1, ar_5, ar_6, arityPad, arityPad)) [ ar_6 >= 0 /\ ar_2 + ar_6 - 9 >= 0 /\ -ar_2 + ar_6 + 9 >= 0 /\ -ar_2 + 9 >= 0 /\ ar_2 - 9 >= 0 /\ ar_1 <= 9 /\ ar_4 - 1 = i73' /\ ar_2 = 9 ]
(Comp: 1, Cost: 25) main_Load_1(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5, ar_6) -> Com_1(main_Load_1'(ar_0, ar_1, ar_2, arityPad, arityPad, arityPad, arityPad)) [ div = i8' /\ 200*ar_0 = i6' /\ 100*ar_0 = i4' /\ static'1 <= static''' + 1 /\ 0 <= static''' /\ static''' <= ar_2 + 2 /\ 0 <= ar_2 /\ 0 <= static'1 ]
(Comp: ?, Cost: 3) main_Load_142(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5, ar_6) -> Com_1(main_LE_153(ar_0, ar_1 + ar_2, ar_1, ar_2, ar_3, ar_4, arityPad)) [ ar_4 >= 0 /\ ar_1 + ar_2 = i46' ]
(Comp: ?, Cost: 11) main_LE_153(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5, ar_6) -> Com_1(main_LE_178(ar_0, i59'*i62', 9, ar_2, ar_3, ar_4, ar_5)) [ ar_5 >= 0 /\ 1 <= ar_1 /\ i59'*i62' = i63' /\ 0 < ar_1 ]
(Comp: ?, Cost: 3) main_LE_178(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5, ar_6) -> Com_1(main_Load_142(ar_0, ar_3 - 1, ar_4, ar_5, ar_6, arityPad, arityPad)) [ ar_6 >= 0 /\ ar_2 + ar_6 - 9 >= 0 /\ -ar_2 + ar_6 + 9 >= 0 /\ -ar_2 + 9 >= 0 /\ ar_2 - 9 >= 0 /\ 10 <= ar_1 /\ ar_3 - 1 = i75' /\ 9 < ar_1 /\ ar_2 = 9 ]
(Comp: 1, Cost: 0) main_LE_153(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5, ar_6) -> Com_1(main_LE_155(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5, arityPad)) [ ar_5 >= 0 /\ ar_1 <= 0 ]
start location: koat_start
leaf cost: 0

Testing for reachability in the complexity graph removes the following transition from problem 5:
main_Load_1(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5, ar_6) -> Com_1(main_Load_1'(ar_0, ar_1, ar_2, arityPad, arityPad, arityPad, arityPad)) [ div = i8' /\ 200*ar_0 = i6' /\ 100*ar_0 = i4' /\ static'1 <= static''' + 1 /\ 0 <= static''' /\ static''' <= ar_2 + 2 /\ 0 <= ar_2 /\ 0 <= static'1 ]
We thus obtain the following problem:
6: T:
(Comp: ?, Cost: 3) main_LE_178(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5, ar_6) -> Com_1(main_Load_142(ar_0, ar_3 - 1, ar_4, ar_5, ar_6, arityPad, arityPad)) [ ar_6 >= 0 /\ ar_2 + ar_6 - 9 >= 0 /\ -ar_2 + ar_6 + 9 >= 0 /\ -ar_2 + 9 >= 0 /\ ar_2 - 9 >= 0 /\ 10 <= ar_1 /\ ar_3 - 1 = i75' /\ 9 < ar_1 /\ ar_2 = 9 ]
(Comp: ?, Cost: 3) main_LE_178(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5, ar_6) -> Com_1(main_Load_142(ar_0, ar_3, ar_4 - 1, ar_5, ar_6, arityPad, arityPad)) [ ar_6 >= 0 /\ ar_2 + ar_6 - 9 >= 0 /\ -ar_2 + ar_6 + 9 >= 0 /\ -ar_2 + 9 >= 0 /\ ar_2 - 9 >= 0 /\ ar_1 <= 9 /\ ar_4 - 1 = i73' /\ ar_2 = 9 ]
(Comp: 1, Cost: 0) main_LE_153(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5, ar_6) -> Com_1(main_LE_155(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5, arityPad)) [ ar_5 >= 0 /\ ar_1 <= 0 ]
(Comp: ?, Cost: 11) main_LE_153(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5, ar_6) -> Com_1(main_LE_178(ar_0, i59'*i62', 9, ar_2, ar_3, ar_4, ar_5)) [ ar_5 >= 0 /\ 1 <= ar_1 /\ i59'*i62' = i63' /\ 0 < ar_1 ]
(Comp: ?, Cost: 3) main_Load_142(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5, ar_6) -> Com_1(main_LE_153(ar_0, ar_1 + ar_2, ar_1, ar_2, ar_3, ar_4, arityPad)) [ ar_4 >= 0 /\ ar_1 + ar_2 = i46' ]
(Comp: 1, Cost: 25) main_Load_1'(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5, ar_6) -> Com_1(main_Load_142(ar_0, 100*ar_0, i8', ar_1, static'1, arityPad, arityPad)) [ ar_2 >= 0 /\ i6' - 13*div < 13 /\ 0 < i6' - 13*div + 13 /\ div = i8' /\ 200*ar_0 = i6' /\ 100*ar_0 = i4' /\ static'1 <= static''' + 1 /\ 0 <= static''' /\ static''' <= ar_2 + 2 /\ 0 <= ar_2 /\ 0 <= static'1 ]
(Comp: 1, Cost: 25) koat_start(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5, ar_6) -> Com_1(main_Load_1'(ar_0, ar_1, ar_2, arityPad, arityPad, arityPad, arityPad)) [ 0 <= 0 /\ div = i8' /\ 200*ar_0 = i6' /\ 100*ar_0 = i4' /\ static'1 <= static''' + 1 /\ 0 <= static''' /\ static''' <= ar_2 + 2 /\ 0 <= ar_2 /\ 0 <= static'1 ]
start location: koat_start
leaf cost: 0

By chaining the transition main_LE_178(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5, ar_6) -> Com_1(main_Load_142(ar_0, ar_3 - 1, ar_4, ar_5, ar_6, arityPad, arityPad)) [ ar_6 >= 0 /\ ar_2 + ar_6 - 9 >= 0 /\ -ar_2 + ar_6 + 9 >= 0 /\ -ar_2 + 9 >= 0 /\ ar_2 - 9 >= 0 /\ 10 <= ar_1 /\ ar_3 - 1 = i75' /\ 9 < ar_1 /\ ar_2 = 9 ] with all transitions in problem 6, the following new transition is obtained:
main_LE_178(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5, ar_6) -> Com_1(main_LE_153(ar_0, ar_3 + ar_4 - 1, ar_3 - 1, ar_4, ar_5, ar_6, arityPad')) [ ar_6 >= 0 /\ ar_2 + ar_6 - 9 >= 0 /\ -ar_2 + ar_6 + 9 >= 0 /\ -ar_2 + 9 >= 0 /\ ar_2 - 9 >= 0 /\ 10 <= ar_1 /\ ar_3 - 1 = i75' /\ 9 < ar_1 /\ ar_2 = 9 /\ ar_3 + ar_4 - 1 = i46' ]
We thus obtain the following problem:
7: T:
(Comp: ?, Cost: 6) main_LE_178(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5, ar_6) -> Com_1(main_LE_153(ar_0, ar_3 + ar_4 - 1, ar_3 - 1, ar_4, ar_5, ar_6, arityPad')) [ ar_6 >= 0 /\ ar_2 + ar_6 - 9 >= 0 /\ -ar_2 + ar_6 + 9 >= 0 /\ -ar_2 + 9 >= 0 /\ ar_2 - 9 >= 0 /\ 10 <= ar_1 /\ ar_3 - 1 = i75' /\ 9 < ar_1 /\ ar_2 = 9 /\ ar_3 + ar_4 - 1 = i46' ]
(Comp: ?, Cost: 3) main_LE_178(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5, ar_6) -> Com_1(main_Load_142(ar_0, ar_3, ar_4 - 1, ar_5, ar_6, arityPad, arityPad)) [ ar_6 >= 0 /\ ar_2 + ar_6 - 9 >= 0 /\ -ar_2 + ar_6 + 9 >= 0 /\ -ar_2 + 9 >= 0 /\ ar_2 - 9 >= 0 /\ ar_1 <= 9 /\ ar_4 - 1 = i73' /\ ar_2 = 9 ]
(Comp: 1, Cost: 0) main_LE_153(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5, ar_6) -> Com_1(main_LE_155(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5, arityPad)) [ ar_5 >= 0 /\ ar_1 <= 0 ]
(Comp: ?, Cost: 11) main_LE_153(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5, ar_6) -> Com_1(main_LE_178(ar_0, i59'*i62', 9, ar_2, ar_3, ar_4, ar_5)) [ ar_5 >= 0 /\ 1 <= ar_1 /\ i59'*i62' = i63' /\ 0 < ar_1 ]
(Comp: ?, Cost: 3) main_Load_142(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5, ar_6) -> Com_1(main_LE_153(ar_0, ar_1 + ar_2, ar_1, ar_2, ar_3, ar_4, arityPad)) [ ar_4 >= 0 /\ ar_1 + ar_2 = i46' ]
(Comp: 1, Cost: 25) main_Load_1'(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5, ar_6) -> Com_1(main_Load_142(ar_0, 100*ar_0, i8', ar_1, static'1, arityPad, arityPad)) [ ar_2 >= 0 /\ i6' - 13*div < 13 /\ 0 < i6' - 13*div + 13 /\ div = i8' /\ 200*ar_0 = i6' /\ 100*ar_0 = i4' /\ static'1 <= static''' + 1 /\ 0 <= static''' /\ static''' <= ar_2 + 2 /\ 0 <= ar_2 /\ 0 <= static'1 ]
(Comp: 1, Cost: 25) koat_start(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5, ar_6) -> Com_1(main_Load_1'(ar_0, ar_1, ar_2, arityPad, arityPad, arityPad, arityPad)) [ 0 <= 0 /\ div = i8' /\ 200*ar_0 = i6' /\ 100*ar_0 = i4' /\ static'1 <= static''' + 1 /\ 0 <= static''' /\ static''' <= ar_2 + 2 /\ 0 <= ar_2 /\ 0 <= static'1 ]
start location: koat_start
leaf cost: 0

By chaining the transition main_LE_178(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5, ar_6) -> Com_1(main_Load_142(ar_0, ar_3, ar_4 - 1, ar_5, ar_6, arityPad, arityPad)) [ ar_6 >= 0 /\ ar_2 + ar_6 - 9 >= 0 /\ -ar_2 + ar_6 + 9 >= 0 /\ -ar_2 + 9 >= 0 /\ ar_2 - 9 >= 0 /\ ar_1 <= 9 /\ ar_4 - 1 = i73' /\ ar_2 = 9 ] with all transitions in problem 7, the following new transition is obtained:
main_LE_178(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5, ar_6) -> Com_1(main_LE_153(ar_0, ar_3 + ar_4 - 1, ar_3, ar_4 - 1, ar_5, ar_6, arityPad')) [ ar_6 >= 0 /\ ar_2 + ar_6 - 9 >= 0 /\ -ar_2 + ar_6 + 9 >= 0 /\ -ar_2 + 9 >= 0 /\ ar_2 - 9 >= 0 /\ ar_1 <= 9 /\ ar_4 - 1 = i73' /\ ar_2 = 9 /\ ar_3 + ar_4 - 1 = i46' ]
We thus obtain the following problem:
8: T:
(Comp: ?, Cost: 6) main_LE_178(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5, ar_6) -> Com_1(main_LE_153(ar_0, ar_3 + ar_4 - 1, ar_3, ar_4 - 1, ar_5, ar_6, arityPad')) [ ar_6 >= 0 /\ ar_2 + ar_6 - 9 >= 0 /\ -ar_2 + ar_6 + 9 >= 0 /\ -ar_2 + 9 >= 0 /\ ar_2 - 9 >= 0 /\ ar_1 <= 9 /\ ar_4 - 1 = i73' /\ ar_2 = 9 /\ ar_3 + ar_4 - 1 = i46' ]
(Comp: ?, Cost: 6) main_LE_178(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5, ar_6) -> Com_1(main_LE_153(ar_0, ar_3 + ar_4 - 1, ar_3 - 1, ar_4, ar_5, ar_6, arityPad')) [ ar_6 >= 0 /\ ar_2 + ar_6 - 9 >= 0 /\ -ar_2 + ar_6 + 9 >= 0 /\ -ar_2 + 9 >= 0 /\ ar_2 - 9 >= 0 /\ 10 <= ar_1 /\ ar_3 - 1 = i75' /\ 9 < ar_1 /\ ar_2 = 9 /\ ar_3 + ar_4 - 1 = i46' ]
(Comp: 1, Cost: 0) main_LE_153(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5, ar_6) -> Com_1(main_LE_155(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5, arityPad)) [ ar_5 >= 0 /\ ar_1 <= 0 ]
(Comp: ?, Cost: 11) main_LE_153(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5, ar_6) -> Com_1(main_LE_178(ar_0, i59'*i62', 9, ar_2, ar_3, ar_4, ar_5)) [ ar_5 >= 0 /\ 1 <= ar_1 /\ i59'*i62' = i63' /\ 0 < ar_1 ]
(Comp: ?, Cost: 3) main_Load_142(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5, ar_6) -> Com_1(main_LE_153(ar_0, ar_1 + ar_2, ar_1, ar_2, ar_3, ar_4, arityPad)) [ ar_4 >= 0 /\ ar_1 + ar_2 = i46' ]
(Comp: 1, Cost: 25) main_Load_1'(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5, ar_6) -> Com_1(main_Load_142(ar_0, 100*ar_0, i8', ar_1, static'1, arityPad, arityPad)) [ ar_2 >= 0 /\ i6' - 13*div < 13 /\ 0 < i6' - 13*div + 13 /\ div = i8' /\ 200*ar_0 = i6' /\ 100*ar_0 = i4' /\ static'1 <= static''' + 1 /\ 0 <= static''' /\ static''' <= ar_2 + 2 /\ 0 <= ar_2 /\ 0 <= static'1 ]
(Comp: 1, Cost: 25) koat_start(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5, ar_6) -> Com_1(main_Load_1'(ar_0, ar_1, ar_2, arityPad, arityPad, arityPad, arityPad)) [ 0 <= 0 /\ div = i8' /\ 200*ar_0 = i6' /\ 100*ar_0 = i4' /\ static'1 <= static''' + 1 /\ 0 <= static''' /\ static''' <= ar_2 + 2 /\ 0 <= ar_2 /\ 0 <= static'1 ]
start location: koat_start
leaf cost: 0

Repeatedly propagating knowledge in problem 8 produces the following problem:
9: T:
(Comp: ?, Cost: 6) main_LE_178(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5, ar_6) -> Com_1(main_LE_153(ar_0, ar_3 + ar_4 - 1, ar_3, ar_4 - 1, ar_5, ar_6, arityPad')) [ ar_6 >= 0 /\ ar_2 + ar_6 - 9 >= 0 /\ -ar_2 + ar_6 + 9 >= 0 /\ -ar_2 + 9 >= 0 /\ ar_2 - 9 >= 0 /\ ar_1 <= 9 /\ ar_4 - 1 = i73' /\ ar_2 = 9 /\ ar_3 + ar_4 - 1 = i46' ]
(Comp: ?, Cost: 6) main_LE_178(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5, ar_6) -> Com_1(main_LE_153(ar_0, ar_3 + ar_4 - 1, ar_3 - 1, ar_4, ar_5, ar_6, arityPad')) [ ar_6 >= 0 /\ ar_2 + ar_6 - 9 >= 0 /\ -ar_2 + ar_6 + 9 >= 0 /\ -ar_2 + 9 >= 0 /\ ar_2 - 9 >= 0 /\ 10 <= ar_1 /\ ar_3 - 1 = i75' /\ 9 < ar_1 /\ ar_2 = 9 /\ ar_3 + ar_4 - 1 = i46' ]
(Comp: 1, Cost: 0) main_LE_153(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5, ar_6) -> Com_1(main_LE_155(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5, arityPad)) [ ar_5 >= 0 /\ ar_1 <= 0 ]
(Comp: ?, Cost: 11) main_LE_153(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5, ar_6) -> Com_1(main_LE_178(ar_0, i59'*i62', 9, ar_2, ar_3, ar_4, ar_5)) [ ar_5 >= 0 /\ 1 <= ar_1 /\ i59'*i62' = i63' /\ 0 < ar_1 ]
(Comp: 1, Cost: 3) main_Load_142(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5, ar_6) -> Com_1(main_LE_153(ar_0, ar_1 + ar_2, ar_1, ar_2, ar_3, ar_4, arityPad)) [ ar_4 >= 0 /\ ar_1 + ar_2 = i46' ]
(Comp: 1, Cost: 25) main_Load_1'(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5, ar_6) -> Com_1(main_Load_142(ar_0, 100*ar_0, i8', ar_1, static'1, arityPad, arityPad)) [ ar_2 >= 0 /\ i6' - 13*div < 13 /\ 0 < i6' - 13*div + 13 /\ div = i8' /\ 200*ar_0 = i6' /\ 100*ar_0 = i4' /\ static'1 <= static''' + 1 /\ 0 <= static''' /\ static''' <= ar_2 + 2 /\ 0 <= ar_2 /\ 0 <= static'1 ]
(Comp: 1, Cost: 25) koat_start(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5, ar_6) -> Com_1(main_Load_1'(ar_0, ar_1, ar_2, arityPad, arityPad, arityPad, arityPad)) [ 0 <= 0 /\ div = i8' /\ 200*ar_0 = i6' /\ 100*ar_0 = i4' /\ static'1 <= static''' + 1 /\ 0 <= static''' /\ static''' <= ar_2 + 2 /\ 0 <= ar_2 /\ 0 <= static'1 ]
start location: koat_start
leaf cost: 0

By chaining the transition main_Load_1'(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5, ar_6) -> Com_1(main_Load_142(ar_0, 100*ar_0, i8', ar_1, static'1, arityPad, arityPad)) [ ar_2 >= 0 /\ i6' - 13*div < 13 /\ 0 < i6' - 13*div + 13 /\ div = i8' /\ 200*ar_0 = i6' /\ 100*ar_0 = i4' /\ static'1 <= static''' + 1 /\ 0 <= static''' /\ static''' <= ar_2 + 2 /\ 0 <= ar_2 /\ 0 <= static'1 ] with all transitions in problem 9, the following new transition is obtained:
main_Load_1'(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5, ar_6) -> Com_1(main_LE_153(ar_0, 100*ar_0 + i8', 100*ar_0, i8', ar_1, static'1, arityPad')) [ ar_2 >= 0 /\ i6' - 13*div < 13 /\ 0 < i6' - 13*div + 13 /\ div = i8' /\ 200*ar_0 = i6' /\ 100*ar_0 = i4' /\ static'1 <= static''' + 1 /\ 0 <= static''' /\ static''' <= ar_2 + 2 /\ 0 <= ar_2 /\ 0 <= static'1 /\ static'1 >= 0 /\ 100*ar_0 + i8' = i46' ]
We thus obtain the following problem:
10: T:
(Comp: 1, Cost: 28) main_Load_1'(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5, ar_6) -> Com_1(main_LE_153(ar_0, 100*ar_0 + i8', 100*ar_0, i8', ar_1, static'1, arityPad')) [ ar_2 >= 0 /\ i6' - 13*div < 13 /\ 0 < i6' - 13*div + 13 /\ div = i8' /\ 200*ar_0 = i6' /\ 100*ar_0 = i4' /\ static'1 <= static''' + 1 /\ 0 <= static''' /\ static''' <= ar_2 + 2 /\ 0 <= ar_2 /\ 0 <= static'1 /\ static'1 >= 0 /\ 100*ar_0 + i8' = i46' ]
(Comp: ?, Cost: 6) main_LE_178(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5, ar_6) -> Com_1(main_LE_153(ar_0, ar_3 + ar_4 - 1, ar_3, ar_4 - 1, ar_5, ar_6, arityPad')) [ ar_6 >= 0 /\ ar_2 + ar_6 - 9 >= 0 /\ -ar_2 + ar_6 + 9 >= 0 /\ -ar_2 + 9 >= 0 /\ ar_2 - 9 >= 0 /\ ar_1 <= 9 /\ ar_4 - 1 = i73' /\ ar_2 = 9 /\ ar_3 + ar_4 - 1 = i46' ]
(Comp: ?, Cost: 6) main_LE_178(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5, ar_6) -> Com_1(main_LE_153(ar_0, ar_3 + ar_4 - 1, ar_3 - 1, ar_4, ar_5, ar_6, arityPad')) [ ar_6 >= 0 /\ ar_2 + ar_6 - 9 >= 0 /\ -ar_2 + ar_6 + 9 >= 0 /\ -ar_2 + 9 >= 0 /\ ar_2 - 9 >= 0 /\ 10 <= ar_1 /\ ar_3 - 1 = i75' /\ 9 < ar_1 /\ ar_2 = 9 /\ ar_3 + ar_4 - 1 = i46' ]
(Comp: 1, Cost: 0) main_LE_153(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5, ar_6) -> Com_1(main_LE_155(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5, arityPad)) [ ar_5 >= 0 /\ ar_1 <= 0 ]
(Comp: ?, Cost: 11) main_LE_153(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5, ar_6) -> Com_1(main_LE_178(ar_0, i59'*i62', 9, ar_2, ar_3, ar_4, ar_5)) [ ar_5 >= 0 /\ 1 <= ar_1 /\ i59'*i62' = i63' /\ 0 < ar_1 ]
(Comp: 1, Cost: 3) main_Load_142(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5, ar_6) -> Com_1(main_LE_153(ar_0, ar_1 + ar_2, ar_1, ar_2, ar_3, ar_4, arityPad)) [ ar_4 >= 0 /\ ar_1 + ar_2 = i46' ]
(Comp: 1, Cost: 25) koat_start(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5, ar_6) -> Com_1(main_Load_1'(ar_0, ar_1, ar_2, arityPad, arityPad, arityPad, arityPad)) [ 0 <= 0 /\ div = i8' /\ 200*ar_0 = i6' /\ 100*ar_0 = i4' /\ static'1 <= static''' + 1 /\ 0 <= static''' /\ static''' <= ar_2 + 2 /\ 0 <= ar_2 /\ 0 <= static'1 ]
start location: koat_start
leaf cost: 0

Testing for reachability in the complexity graph removes the following transition from problem 10:
main_Load_142(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5, ar_6) -> Com_1(main_LE_153(ar_0, ar_1 + ar_2, ar_1, ar_2, ar_3, ar_4, arityPad)) [ ar_4 >= 0 /\ ar_1 + ar_2 = i46' ]
We thus obtain the following problem:
11: T:
(Comp: ?, Cost: 6) main_LE_178(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5, ar_6) -> Com_1(main_LE_153(ar_0, ar_3 + ar_4 - 1, ar_3, ar_4 - 1, ar_5, ar_6, arityPad')) [ ar_6 >= 0 /\ ar_2 + ar_6 - 9 >= 0 /\ -ar_2 + ar_6 + 9 >= 0 /\ -ar_2 + 9 >= 0 /\ ar_2 - 9 >= 0 /\ ar_1 <= 9 /\ ar_4 - 1 = i73' /\ ar_2 = 9 /\ ar_3 + ar_4 - 1 = i46' ]
(Comp: ?, Cost: 6) main_LE_178(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5, ar_6) -> Com_1(main_LE_153(ar_0, ar_3 + ar_4 - 1, ar_3 - 1, ar_4, ar_5, ar_6, arityPad')) [ ar_6 >= 0 /\ ar_2 + ar_6 - 9 >= 0 /\ -ar_2 + ar_6 + 9 >= 0 /\ -ar_2 + 9 >= 0 /\ ar_2 - 9 >= 0 /\ 10 <= ar_1 /\ ar_3 - 1 = i75' /\ 9 < ar_1 /\ ar_2 = 9 /\ ar_3 + ar_4 - 1 = i46' ]
(Comp: 1, Cost: 0) main_LE_153(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5, ar_6) -> Com_1(main_LE_155(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5, arityPad)) [ ar_5 >= 0 /\ ar_1 <= 0 ]
(Comp: ?, Cost: 11) main_LE_153(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5, ar_6) -> Com_1(main_LE_178(ar_0, i59'*i62', 9, ar_2, ar_3, ar_4, ar_5)) [ ar_5 >= 0 /\ 1 <= ar_1 /\ i59'*i62' = i63' /\ 0 < ar_1 ]
(Comp: 1, Cost: 28) main_Load_1'(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5, ar_6) -> Com_1(main_LE_153(ar_0, 100*ar_0 + i8', 100*ar_0, i8', ar_1, static'1, arityPad')) [ ar_2 >= 0 /\ i6' - 13*div < 13 /\ 0 < i6' - 13*div + 13 /\ div = i8' /\ 200*ar_0 = i6' /\ 100*ar_0 = i4' /\ static'1 <= static''' + 1 /\ 0 <= static''' /\ static''' <= ar_2 + 2 /\ 0 <= ar_2 /\ 0 <= static'1 /\ static'1 >= 0 /\ 100*ar_0 + i8' = i46' ]
(Comp: 1, Cost: 25) koat_start(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5, ar_6) -> Com_1(main_Load_1'(ar_0, ar_1, ar_2, arityPad, arityPad, arityPad, arityPad)) [ 0 <= 0 /\ div = i8' /\ 200*ar_0 = i6' /\ 100*ar_0 = i4' /\ static'1 <= static''' + 1 /\ 0 <= static''' /\ static''' <= ar_2 + 2 /\ 0 <= ar_2 /\ 0 <= static'1 ]
start location: koat_start
leaf cost: 0

By chaining the transition koat_start(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5, ar_6) -> Com_1(main_Load_1'(ar_0, ar_1, ar_2, arityPad, arityPad, arityPad, arityPad)) [ 0 <= 0 /\ div = i8' /\ 200*ar_0 = i6' /\ 100*ar_0 = i4' /\ static'1 <= static''' + 1 /\ 0 <= static''' /\ static''' <= ar_2 + 2 /\ 0 <= ar_2 /\ 0 <= static'1 ] with all transitions in problem 11, the following new transition is obtained:
koat_start(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5, ar_6) -> Com_1(main_LE_153(ar_0, 100*ar_0 + i8'', 100*ar_0, i8'', ar_1, static'1', arityPad')) [ 0 <= 0 /\ div = i8' /\ 200*ar_0 = i6' /\ 100*ar_0 = i4' /\ static'1 <= static''' + 1 /\ 0 <= static''' /\ static''' <= ar_2 + 2 /\ 0 <= ar_2 /\ 0 <= static'1 /\ ar_2 >= 0 /\ i6'' - 13*div' < 13 /\ 0 < i6'' - 13*div' + 13 /\ div' = i8'' /\ 200*ar_0 = i6'' /\ 100*ar_0 = i4'' /\ static'1' <= static'''' + 1 /\ 0 <= static'''' /\ static'''' <= ar_2 + 2 /\ 0 <= static'1' /\ static'1' >= 0 /\ 100*ar_0 + i8'' = i46' ]
We thus obtain the following problem:
12: T:
(Comp: 1, Cost: 53) koat_start(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5, ar_6) -> Com_1(main_LE_153(ar_0, 100*ar_0 + i8'', 100*ar_0, i8'', ar_1, static'1', arityPad')) [ 0 <= 0 /\ div = i8' /\ 200*ar_0 = i6' /\ 100*ar_0 = i4' /\ static'1 <= static''' + 1 /\ 0 <= static''' /\ static''' <= ar_2 + 2 /\ 0 <= ar_2 /\ 0 <= static'1 /\ ar_2 >= 0 /\ i6'' - 13*div' < 13 /\ 0 < i6'' - 13*div' + 13 /\ div' = i8'' /\ 200*ar_0 = i6'' /\ 100*ar_0 = i4'' /\ static'1' <= static'''' + 1 /\ 0 <= static'''' /\ static'''' <= ar_2 + 2 /\ 0 <= static'1' /\ static'1' >= 0 /\ 100*ar_0 + i8'' = i46' ]
(Comp: ?, Cost: 6) main_LE_178(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5, ar_6) -> Com_1(main_LE_153(ar_0, ar_3 + ar_4 - 1, ar_3, ar_4 - 1, ar_5, ar_6, arityPad')) [ ar_6 >= 0 /\ ar_2 + ar_6 - 9 >= 0 /\ -ar_2 + ar_6 + 9 >= 0 /\ -ar_2 + 9 >= 0 /\ ar_2 - 9 >= 0 /\ ar_1 <= 9 /\ ar_4 - 1 = i73' /\ ar_2 = 9 /\ ar_3 + ar_4 - 1 = i46' ]
(Comp: ?, Cost: 6) main_LE_178(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5, ar_6) -> Com_1(main_LE_153(ar_0, ar_3 + ar_4 - 1, ar_3 - 1, ar_4, ar_5, ar_6, arityPad')) [ ar_6 >= 0 /\ ar_2 + ar_6 - 9 >= 0 /\ -ar_2 + ar_6 + 9 >= 0 /\ -ar_2 + 9 >= 0 /\ ar_2 - 9 >= 0 /\ 10 <= ar_1 /\ ar_3 - 1 = i75' /\ 9 < ar_1 /\ ar_2 = 9 /\ ar_3 + ar_4 - 1 = i46' ]
(Comp: 1, Cost: 0) main_LE_153(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5, ar_6) -> Com_1(main_LE_155(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5, arityPad)) [ ar_5 >= 0 /\ ar_1 <= 0 ]
(Comp: ?, Cost: 11) main_LE_153(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5, ar_6) -> Com_1(main_LE_178(ar_0, i59'*i62', 9, ar_2, ar_3, ar_4, ar_5)) [ ar_5 >= 0 /\ 1 <= ar_1 /\ i59'*i62' = i63' /\ 0 < ar_1 ]
(Comp: 1, Cost: 28) main_Load_1'(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5, ar_6) -> Com_1(main_LE_153(ar_0, 100*ar_0 + i8', 100*ar_0, i8', ar_1, static'1, arityPad')) [ ar_2 >= 0 /\ i6' - 13*div < 13 /\ 0 < i6' - 13*div + 13 /\ div = i8' /\ 200*ar_0 = i6' /\ 100*ar_0 = i4' /\ static'1 <= static''' + 1 /\ 0 <= static''' /\ static''' <= ar_2 + 2 /\ 0 <= ar_2 /\ 0 <= static'1 /\ static'1 >= 0 /\ 100*ar_0 + i8' = i46' ]
start location: koat_start
leaf cost: 0

Testing for reachability in the complexity graph removes the following transition from problem 12:
main_Load_1'(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5, ar_6) -> Com_1(main_LE_153(ar_0, 100*ar_0 + i8', 100*ar_0, i8', ar_1, static'1, arityPad')) [ ar_2 >= 0 /\ i6' - 13*div < 13 /\ 0 < i6' - 13*div + 13 /\ div = i8' /\ 200*ar_0 = i6' /\ 100*ar_0 = i4' /\ static'1 <= static''' + 1 /\ 0 <= static''' /\ static''' <= ar_2 + 2 /\ 0 <= ar_2 /\ 0 <= static'1 /\ static'1 >= 0 /\ 100*ar_0 + i8' = i46' ]
We thus obtain the following problem:
13: T:
(Comp: ?, Cost: 6) main_LE_178(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5, ar_6) -> Com_1(main_LE_153(ar_0, ar_3 + ar_4 - 1, ar_3, ar_4 - 1, ar_5, ar_6, arityPad')) [ ar_6 >= 0 /\ ar_2 + ar_6 - 9 >= 0 /\ -ar_2 + ar_6 + 9 >= 0 /\ -ar_2 + 9 >= 0 /\ ar_2 - 9 >= 0 /\ ar_1 <= 9 /\ ar_4 - 1 = i73' /\ ar_2 = 9 /\ ar_3 + ar_4 - 1 = i46' ]
(Comp: ?, Cost: 6) main_LE_178(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5, ar_6) -> Com_1(main_LE_153(ar_0, ar_3 + ar_4 - 1, ar_3 - 1, ar_4, ar_5, ar_6, arityPad')) [ ar_6 >= 0 /\ ar_2 + ar_6 - 9 >= 0 /\ -ar_2 + ar_6 + 9 >= 0 /\ -ar_2 + 9 >= 0 /\ ar_2 - 9 >= 0 /\ 10 <= ar_1 /\ ar_3 - 1 = i75' /\ 9 < ar_1 /\ ar_2 = 9 /\ ar_3 + ar_4 - 1 = i46' ]
(Comp: 1, Cost: 0) main_LE_153(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5, ar_6) -> Com_1(main_LE_155(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5, arityPad)) [ ar_5 >= 0 /\ ar_1 <= 0 ]
(Comp: ?, Cost: 11) main_LE_153(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5, ar_6) -> Com_1(main_LE_178(ar_0, i59'*i62', 9, ar_2, ar_3, ar_4, ar_5)) [ ar_5 >= 0 /\ 1 <= ar_1 /\ i59'*i62' = i63' /\ 0 < ar_1 ]
(Comp: 1, Cost: 53) koat_start(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5, ar_6) -> Com_1(main_LE_153(ar_0, 100*ar_0 + i8'', 100*ar_0, i8'', ar_1, static'1', arityPad')) [ 0 <= 0 /\ div = i8' /\ 200*ar_0 = i6' /\ 100*ar_0 = i4' /\ static'1 <= static''' + 1 /\ 0 <= static''' /\ static''' <= ar_2 + 2 /\ 0 <= ar_2 /\ 0 <= static'1 /\ ar_2 >= 0 /\ i6'' - 13*div' < 13 /\ 0 < i6'' - 13*div' + 13 /\ div' = i8'' /\ 200*ar_0 = i6'' /\ 100*ar_0 = i4'' /\ static'1' <= static'''' + 1 /\ 0 <= static'''' /\ static'''' <= ar_2 + 2 /\ 0 <= static'1' /\ static'1' >= 0 /\ 100*ar_0 + i8'' = i46' ]
start location: koat_start
leaf cost: 0

By chaining the transition main_LE_178(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5, ar_6) -> Com_1(main_LE_153(ar_0, ar_3 + ar_4 - 1, ar_3, ar_4 - 1, ar_5, ar_6, arityPad')) [ ar_6 >= 0 /\ ar_2 + ar_6 - 9 >= 0 /\ -ar_2 + ar_6 + 9 >= 0 /\ -ar_2 + 9 >= 0 /\ ar_2 - 9 >= 0 /\ ar_1 <= 9 /\ ar_4 - 1 = i73' /\ ar_2 = 9 /\ ar_3 + ar_4 - 1 = i46' ] with all transitions in problem 13, the following new transitions are obtained:
main_LE_178(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5, ar_6) -> Com_1(main_LE_155(ar_0, ar_3 + ar_4 - 1, ar_3, ar_4 - 1, ar_5, ar_6, arityPad)) [ ar_6 >= 0 /\ ar_2 + ar_6 - 9 >= 0 /\ -ar_2 + ar_6 + 9 >= 0 /\ -ar_2 + 9 >= 0 /\ ar_2 - 9 >= 0 /\ ar_1 <= 9 /\ ar_4 - 1 = i73' /\ ar_2 = 9 /\ ar_3 + ar_4 - 1 = i46' /\ ar_3 + ar_4 - 1 <= 0 ]
main_LE_178(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5, ar_6) -> Com_1(main_LE_178(ar_0, i59'*i62', 9, ar_3, ar_4 - 1, ar_5, ar_6)) [ ar_6 >= 0 /\ ar_2 + ar_6 - 9 >= 0 /\ -ar_2 + ar_6 + 9 >= 0 /\ -ar_2 + 9 >= 0 /\ ar_2 - 9 >= 0 /\ ar_1 <= 9 /\ ar_4 - 1 = i73' /\ ar_2 = 9 /\ ar_3 + ar_4 - 1 = i46' /\ 1 <= ar_3 + ar_4 - 1 /\ i59'*i62' = i63' /\ 0 < ar_3 + ar_4 - 1 ]
We thus obtain the following problem:
14: T:
(Comp: ?, Cost: 6) main_LE_178(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5, ar_6) -> Com_1(main_LE_155(ar_0, ar_3 + ar_4 - 1, ar_3, ar_4 - 1, ar_5, ar_6, arityPad)) [ ar_6 >= 0 /\ ar_2 + ar_6 - 9 >= 0 /\ -ar_2 + ar_6 + 9 >= 0 /\ -ar_2 + 9 >= 0 /\ ar_2 - 9 >= 0 /\ ar_1 <= 9 /\ ar_4 - 1 = i73' /\ ar_2 = 9 /\ ar_3 + ar_4 - 1 = i46' /\ ar_3 + ar_4 - 1 <= 0 ]
(Comp: ?, Cost: 17) main_LE_178(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5, ar_6) -> Com_1(main_LE_178(ar_0, i59'*i62', 9, ar_3, ar_4 - 1, ar_5, ar_6)) [ ar_6 >= 0 /\ ar_2 + ar_6 - 9 >= 0 /\ -ar_2 + ar_6 + 9 >= 0 /\ -ar_2 + 9 >= 0 /\ ar_2 - 9 >= 0 /\ ar_1 <= 9 /\ ar_4 - 1 = i73' /\ ar_2 = 9 /\ ar_3 + ar_4 - 1 = i46' /\ 1 <= ar_3 + ar_4 - 1 /\ i59'*i62' = i63' /\ 0 < ar_3 + ar_4 - 1 ]
(Comp: ?, Cost: 6) main_LE_178(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5, ar_6) -> Com_1(main_LE_153(ar_0, ar_3 + ar_4 - 1, ar_3 - 1, ar_4, ar_5, ar_6, arityPad')) [ ar_6 >= 0 /\ ar_2 + ar_6 - 9 >= 0 /\ -ar_2 + ar_6 + 9 >= 0 /\ -ar_2 + 9 >= 0 /\ ar_2 - 9 >= 0 /\ 10 <= ar_1 /\ ar_3 - 1 = i75' /\ 9 < ar_1 /\ ar_2 = 9 /\ ar_3 + ar_4 - 1 = i46' ]
(Comp: 1, Cost: 0) main_LE_153(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5, ar_6) -> Com_1(main_LE_155(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5, arityPad)) [ ar_5 >= 0 /\ ar_1 <= 0 ]
(Comp: ?, Cost: 11) main_LE_153(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5, ar_6) -> Com_1(main_LE_178(ar_0, i59'*i62', 9, ar_2, ar_3, ar_4, ar_5)) [ ar_5 >= 0 /\ 1 <= ar_1 /\ i59'*i62' = i63' /\ 0 < ar_1 ]
(Comp: 1, Cost: 53) koat_start(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5, ar_6) -> Com_1(main_LE_153(ar_0, 100*ar_0 + i8'', 100*ar_0, i8'', ar_1, static'1', arityPad')) [ 0 <= 0 /\ div = i8' /\ 200*ar_0 = i6' /\ 100*ar_0 = i4' /\ static'1 <= static''' + 1 /\ 0 <= static''' /\ static''' <= ar_2 + 2 /\ 0 <= ar_2 /\ 0 <= static'1 /\ ar_2 >= 0 /\ i6'' - 13*div' < 13 /\ 0 < i6'' - 13*div' + 13 /\ div' = i8'' /\ 200*ar_0 = i6'' /\ 100*ar_0 = i4'' /\ static'1' <= static'''' + 1 /\ 0 <= static'''' /\ static'''' <= ar_2 + 2 /\ 0 <= static'1' /\ static'1' >= 0 /\ 100*ar_0 + i8'' = i46' ]
start location: koat_start
leaf cost: 0

A polynomial rank function with
Pol(main_LE_178) = 1
Pol(main_LE_155) = 0
Pol(main_LE_153) = 1
Pol(koat_start) = 1
orients all transitions weakly and the transition
main_LE_178(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5, ar_6) -> Com_1(main_LE_155(ar_0, ar_3 + ar_4 - 1, ar_3, ar_4 - 1, ar_5, ar_6, arityPad)) [ ar_6 >= 0 /\ ar_2 + ar_6 - 9 >= 0 /\ -ar_2 + ar_6 + 9 >= 0 /\ -ar_2 + 9 >= 0 /\ ar_2 - 9 >= 0 /\ ar_1 <= 9 /\ ar_4 - 1 = i73' /\ ar_2 = 9 /\ ar_3 + ar_4 - 1 = i46' /\ ar_3 + ar_4 - 1 <= 0 ]
strictly and produces the following problem:
15: T:
(Comp: 1, Cost: 6) main_LE_178(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5, ar_6) -> Com_1(main_LE_155(ar_0, ar_3 + ar_4 - 1, ar_3, ar_4 - 1, ar_5, ar_6, arityPad)) [ ar_6 >= 0 /\ ar_2 + ar_6 - 9 >= 0 /\ -ar_2 + ar_6 + 9 >= 0 /\ -ar_2 + 9 >= 0 /\ ar_2 - 9 >= 0 /\ ar_1 <= 9 /\ ar_4 - 1 = i73' /\ ar_2 = 9 /\ ar_3 + ar_4 - 1 = i46' /\ ar_3 + ar_4 - 1 <= 0 ]
(Comp: ?, Cost: 17) main_LE_178(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5, ar_6) -> Com_1(main_LE_178(ar_0, i59'*i62', 9, ar_3, ar_4 - 1, ar_5, ar_6)) [ ar_6 >= 0 /\ ar_2 + ar_6 - 9 >= 0 /\ -ar_2 + ar_6 + 9 >= 0 /\ -ar_2 + 9 >= 0 /\ ar_2 - 9 >= 0 /\ ar_1 <= 9 /\ ar_4 - 1 = i73' /\ ar_2 = 9 /\ ar_3 + ar_4 - 1 = i46' /\ 1 <= ar_3 + ar_4 - 1 /\ i59'*i62' = i63' /\ 0 < ar_3 + ar_4 - 1 ]
(Comp: ?, Cost: 6) main_LE_178(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5, ar_6) -> Com_1(main_LE_153(ar_0, ar_3 + ar_4 - 1, ar_3 - 1, ar_4, ar_5, ar_6, arityPad')) [ ar_6 >= 0 /\ ar_2 + ar_6 - 9 >= 0 /\ -ar_2 + ar_6 + 9 >= 0 /\ -ar_2 + 9 >= 0 /\ ar_2 - 9 >= 0 /\ 10 <= ar_1 /\ ar_3 - 1 = i75' /\ 9 < ar_1 /\ ar_2 = 9 /\ ar_3 + ar_4 - 1 = i46' ]
(Comp: 1, Cost: 0) main_LE_153(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5, ar_6) -> Com_1(main_LE_155(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5, arityPad)) [ ar_5 >= 0 /\ ar_1 <= 0 ]
(Comp: ?, Cost: 11) main_LE_153(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5, ar_6) -> Com_1(main_LE_178(ar_0, i59'*i62', 9, ar_2, ar_3, ar_4, ar_5)) [ ar_5 >= 0 /\ 1 <= ar_1 /\ i59'*i62' = i63' /\ 0 < ar_1 ]
(Comp: 1, Cost: 53) koat_start(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5, ar_6) -> Com_1(main_LE_153(ar_0, 100*ar_0 + i8'', 100*ar_0, i8'', ar_1, static'1', arityPad')) [ 0 <= 0 /\ div = i8' /\ 200*ar_0 = i6' /\ 100*ar_0 = i4' /\ static'1 <= static''' + 1 /\ 0 <= static''' /\ static''' <= ar_2 + 2 /\ 0 <= ar_2 /\ 0 <= static'1 /\ ar_2 >= 0 /\ i6'' - 13*div' < 13 /\ 0 < i6'' - 13*div' + 13 /\ div' = i8'' /\ 200*ar_0 = i6'' /\ 100*ar_0 = i4'' /\ static'1' <= static'''' + 1 /\ 0 <= static'''' /\ static'''' <= ar_2 + 2 /\ 0 <= static'1' /\ static'1' >= 0 /\ 100*ar_0 + i8'' = i46' ]
start location: koat_start
leaf cost: 0

A polynomial rank function with
Pol(main_LE_178) = 13*V_4 + 13*V_5 - 13
Pol(main_LE_155) = 13*V_3 + 13*V_4
Pol(main_LE_153) = 13*V_3 + 13*V_4
Pol(koat_start) = 1500*V_1 + 12
orients all transitions weakly and the transition
main_LE_178(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5, ar_6) -> Com_1(main_LE_178(ar_0, i59'*i62', 9, ar_3, ar_4 - 1, ar_5, ar_6)) [ ar_6 >= 0 /\ ar_2 + ar_6 - 9 >= 0 /\ -ar_2 + ar_6 + 9 >= 0 /\ -ar_2 + 9 >= 0 /\ ar_2 - 9 >= 0 /\ ar_1 <= 9 /\ ar_4 - 1 = i73' /\ ar_2 = 9 /\ ar_3 + ar_4 - 1 = i46' /\ 1 <= ar_3 + ar_4 - 1 /\ i59'*i62' = i63' /\ 0 < ar_3 + ar_4 - 1 ]
strictly and produces the following problem:
16: T:
(Comp: 1, Cost: 6) main_LE_178(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5, ar_6) -> Com_1(main_LE_155(ar_0, ar_3 + ar_4 - 1, ar_3, ar_4 - 1, ar_5, ar_6, arityPad)) [ ar_6 >= 0 /\ ar_2 + ar_6 - 9 >= 0 /\ -ar_2 + ar_6 + 9 >= 0 /\ -ar_2 + 9 >= 0 /\ ar_2 - 9 >= 0 /\ ar_1 <= 9 /\ ar_4 - 1 = i73' /\ ar_2 = 9 /\ ar_3 + ar_4 - 1 = i46' /\ ar_3 + ar_4 - 1 <= 0 ]
(Comp: 1500*ar_0 + 12, Cost: 17) main_LE_178(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5, ar_6) -> Com_1(main_LE_178(ar_0, i59'*i62', 9, ar_3, ar_4 - 1, ar_5, ar_6)) [ ar_6 >= 0 /\ ar_2 + ar_6 - 9 >= 0 /\ -ar_2 + ar_6 + 9 >= 0 /\ -ar_2 + 9 >= 0 /\ ar_2 - 9 >= 0 /\ ar_1 <= 9 /\ ar_4 - 1 = i73' /\ ar_2 = 9 /\ ar_3 + ar_4 - 1 = i46' /\ 1 <= ar_3 + ar_4 - 1 /\ i59'*i62' = i63' /\ 0 < ar_3 + ar_4 - 1 ]
(Comp: ?, Cost: 6) main_LE_178(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5, ar_6) -> Com_1(main_LE_153(ar_0, ar_3 + ar_4 - 1, ar_3 - 1, ar_4, ar_5, ar_6, arityPad')) [ ar_6 >= 0 /\ ar_2 + ar_6 - 9 >= 0 /\ -ar_2 + ar_6 + 9 >= 0 /\ -ar_2 + 9 >= 0 /\ ar_2 - 9 >= 0 /\ 10 <= ar_1 /\ ar_3 - 1 = i75' /\ 9 < ar_1 /\ ar_2 = 9 /\ ar_3 + ar_4 - 1 = i46' ]
(Comp: 1, Cost: 0) main_LE_153(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5, ar_6) -> Com_1(main_LE_155(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5, arityPad)) [ ar_5 >= 0 /\ ar_1 <= 0 ]
(Comp: ?, Cost: 11) main_LE_153(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5, ar_6) -> Com_1(main_LE_178(ar_0, i59'*i62', 9, ar_2, ar_3, ar_4, ar_5)) [ ar_5 >= 0 /\ 1 <= ar_1 /\ i59'*i62' = i63' /\ 0 < ar_1 ]
(Comp: 1, Cost: 53) koat_start(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5, ar_6) -> Com_1(main_LE_153(ar_0, 100*ar_0 + i8'', 100*ar_0, i8'', ar_1, static'1', arityPad')) [ 0 <= 0 /\ div = i8' /\ 200*ar_0 = i6' /\ 100*ar_0 = i4' /\ static'1 <= static''' + 1 /\ 0 <= static''' /\ static''' <= ar_2 + 2 /\ 0 <= ar_2 /\ 0 <= static'1 /\ ar_2 >= 0 /\ i6'' - 13*div' < 13 /\ 0 < i6'' - 13*div' + 13 /\ div' = i8'' /\ 200*ar_0 = i6'' /\ 100*ar_0 = i4'' /\ static'1' <= static'''' + 1 /\ 0 <= static'''' /\ static'''' <= ar_2 + 2 /\ 0 <= static'1' /\ static'1' >= 0 /\ 100*ar_0 + i8'' = i46' ]
start location: koat_start
leaf cost: 0

By chaining the transition main_LE_178(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5, ar_6) -> Com_1(main_LE_153(ar_0, ar_3 + ar_4 - 1, ar_3 - 1, ar_4, ar_5, ar_6, arityPad')) [ ar_6 >= 0 /\ ar_2 + ar_6 - 9 >= 0 /\ -ar_2 + ar_6 + 9 >= 0 /\ -ar_2 + 9 >= 0 /\ ar_2 - 9 >= 0 /\ 10 <= ar_1 /\ ar_3 - 1 = i75' /\ 9 < ar_1 /\ ar_2 = 9 /\ ar_3 + ar_4 - 1 = i46' ] with all transitions in problem 16, the following new transitions are obtained:
main_LE_178(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5, ar_6) -> Com_1(main_LE_155(ar_0, ar_3 + ar_4 - 1, ar_3 - 1, ar_4, ar_5, ar_6, arityPad)) [ ar_6 >= 0 /\ ar_2 + ar_6 - 9 >= 0 /\ -ar_2 + ar_6 + 9 >= 0 /\ -ar_2 + 9 >= 0 /\ ar_2 - 9 >= 0 /\ 10 <= ar_1 /\ ar_3 - 1 = i75' /\ 9 < ar_1 /\ ar_2 = 9 /\ ar_3 + ar_4 - 1 = i46' /\ ar_3 + ar_4 - 1 <= 0 ]
main_LE_178(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5, ar_6) -> Com_1(main_LE_178(ar_0, i59'*i62', 9, ar_3 - 1, ar_4, ar_5, ar_6)) [ ar_6 >= 0 /\ ar_2 + ar_6 - 9 >= 0 /\ -ar_2 + ar_6 + 9 >= 0 /\ -ar_2 + 9 >= 0 /\ ar_2 - 9 >= 0 /\ 10 <= ar_1 /\ ar_3 - 1 = i75' /\ 9 < ar_1 /\ ar_2 = 9 /\ ar_3 + ar_4 - 1 = i46' /\ 1 <= ar_3 + ar_4 - 1 /\ i59'*i62' = i63' /\ 0 < ar_3 + ar_4 - 1 ]
We thus obtain the following problem:
17: T:
(Comp: ?, Cost: 6) main_LE_178(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5, ar_6) -> Com_1(main_LE_155(ar_0, ar_3 + ar_4 - 1, ar_3 - 1, ar_4, ar_5, ar_6, arityPad)) [ ar_6 >= 0 /\ ar_2 + ar_6 - 9 >= 0 /\ -ar_2 + ar_6 + 9 >= 0 /\ -ar_2 + 9 >= 0 /\ ar_2 - 9 >= 0 /\ 10 <= ar_1 /\ ar_3 - 1 = i75' /\ 9 < ar_1 /\ ar_2 = 9 /\ ar_3 + ar_4 - 1 = i46' /\ ar_3 + ar_4 - 1 <= 0 ]
(Comp: ?, Cost: 17) main_LE_178(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5, ar_6) -> Com_1(main_LE_178(ar_0, i59'*i62', 9, ar_3 - 1, ar_4, ar_5, ar_6)) [ ar_6 >= 0 /\ ar_2 + ar_6 - 9 >= 0 /\ -ar_2 + ar_6 + 9 >= 0 /\ -ar_2 + 9 >= 0 /\ ar_2 - 9 >= 0 /\ 10 <= ar_1 /\ ar_3 - 1 = i75' /\ 9 < ar_1 /\ ar_2 = 9 /\ ar_3 + ar_4 - 1 = i46' /\ 1 <= ar_3 + ar_4 - 1 /\ i59'*i62' = i63' /\ 0 < ar_3 + ar_4 - 1 ]
(Comp: 1, Cost: 6) main_LE_178(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5, ar_6) -> Com_1(main_LE_155(ar_0, ar_3 + ar_4 - 1, ar_3, ar_4 - 1, ar_5, ar_6, arityPad)) [ ar_6 >= 0 /\ ar_2 + ar_6 - 9 >= 0 /\ -ar_2 + ar_6 + 9 >= 0 /\ -ar_2 + 9 >= 0 /\ ar_2 - 9 >= 0 /\ ar_1 <= 9 /\ ar_4 - 1 = i73' /\ ar_2 = 9 /\ ar_3 + ar_4 - 1 = i46' /\ ar_3 + ar_4 - 1 <= 0 ]
(Comp: 1500*ar_0 + 12, Cost: 17) main_LE_178(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5, ar_6) -> Com_1(main_LE_178(ar_0, i59'*i62', 9, ar_3, ar_4 - 1, ar_5, ar_6)) [ ar_6 >= 0 /\ ar_2 + ar_6 - 9 >= 0 /\ -ar_2 + ar_6 + 9 >= 0 /\ -ar_2 + 9 >= 0 /\ ar_2 - 9 >= 0 /\ ar_1 <= 9 /\ ar_4 - 1 = i73' /\ ar_2 = 9 /\ ar_3 + ar_4 - 1 = i46' /\ 1 <= ar_3 + ar_4 - 1 /\ i59'*i62' = i63' /\ 0 < ar_3 + ar_4 - 1 ]
(Comp: 1, Cost: 0) main_LE_153(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5, ar_6) -> Com_1(main_LE_155(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5, arityPad)) [ ar_5 >= 0 /\ ar_1 <= 0 ]
(Comp: ?, Cost: 11) main_LE_153(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5, ar_6) -> Com_1(main_LE_178(ar_0, i59'*i62', 9, ar_2, ar_3, ar_4, ar_5)) [ ar_5 >= 0 /\ 1 <= ar_1 /\ i59'*i62' = i63' /\ 0 < ar_1 ]
(Comp: 1, Cost: 53) koat_start(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5, ar_6) -> Com_1(main_LE_153(ar_0, 100*ar_0 + i8'', 100*ar_0, i8'', ar_1, static'1', arityPad')) [ 0 <= 0 /\ div = i8' /\ 200*ar_0 = i6' /\ 100*ar_0 = i4' /\ static'1 <= static''' + 1 /\ 0 <= static''' /\ static''' <= ar_2 + 2 /\ 0 <= ar_2 /\ 0 <= static'1 /\ ar_2 >= 0 /\ i6'' - 13*div' < 13 /\ 0 < i6'' - 13*div' + 13 /\ div' = i8'' /\ 200*ar_0 = i6'' /\ 100*ar_0 = i4'' /\ static'1' <= static'''' + 1 /\ 0 <= static'''' /\ static'''' <= ar_2 + 2 /\ 0 <= static'1' /\ static'1' >= 0 /\ 100*ar_0 + i8'' = i46' ]
start location: koat_start
leaf cost: 0

Repeatedly propagating knowledge in problem 17 produces the following problem:
18: T:
(Comp: ?, Cost: 6) main_LE_178(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5, ar_6) -> Com_1(main_LE_155(ar_0, ar_3 + ar_4 - 1, ar_3 - 1, ar_4, ar_5, ar_6, arityPad)) [ ar_6 >= 0 /\ ar_2 + ar_6 - 9 >= 0 /\ -ar_2 + ar_6 + 9 >= 0 /\ -ar_2 + 9 >= 0 /\ ar_2 - 9 >= 0 /\ 10 <= ar_1 /\ ar_3 - 1 = i75' /\ 9 < ar_1 /\ ar_2 = 9 /\ ar_3 + ar_4 - 1 = i46' /\ ar_3 + ar_4 - 1 <= 0 ]
(Comp: ?, Cost: 17) main_LE_178(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5, ar_6) -> Com_1(main_LE_178(ar_0, i59'*i62', 9, ar_3 - 1, ar_4, ar_5, ar_6)) [ ar_6 >= 0 /\ ar_2 + ar_6 - 9 >= 0 /\ -ar_2 + ar_6 + 9 >= 0 /\ -ar_2 + 9 >= 0 /\ ar_2 - 9 >= 0 /\ 10 <= ar_1 /\ ar_3 - 1 = i75' /\ 9 < ar_1 /\ ar_2 = 9 /\ ar_3 + ar_4 - 1 = i46' /\ 1 <= ar_3 + ar_4 - 1 /\ i59'*i62' = i63' /\ 0 < ar_3 + ar_4 - 1 ]
(Comp: 1, Cost: 6) main_LE_178(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5, ar_6) -> Com_1(main_LE_155(ar_0, ar_3 + ar_4 - 1, ar_3, ar_4 - 1, ar_5, ar_6, arityPad)) [ ar_6 >= 0 /\ ar_2 + ar_6 - 9 >= 0 /\ -ar_2 + ar_6 + 9 >= 0 /\ -ar_2 + 9 >= 0 /\ ar_2 - 9 >= 0 /\ ar_1 <= 9 /\ ar_4 - 1 = i73' /\ ar_2 = 9 /\ ar_3 + ar_4 - 1 = i46' /\ ar_3 + ar_4 - 1 <= 0 ]
(Comp: 1500*ar_0 + 12, Cost: 17) main_LE_178(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5, ar_6) -> Com_1(main_LE_178(ar_0, i59'*i62', 9, ar_3, ar_4 - 1, ar_5, ar_6)) [ ar_6 >= 0 /\ ar_2 + ar_6 - 9 >= 0 /\ -ar_2 + ar_6 + 9 >= 0 /\ -ar_2 + 9 >= 0 /\ ar_2 - 9 >= 0 /\ ar_1 <= 9 /\ ar_4 - 1 = i73' /\ ar_2 = 9 /\ ar_3 + ar_4 - 1 = i46' /\ 1 <= ar_3 + ar_4 - 1 /\ i59'*i62' = i63' /\ 0 < ar_3 + ar_4 - 1 ]
(Comp: 1, Cost: 0) main_LE_153(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5, ar_6) -> Com_1(main_LE_155(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5, arityPad)) [ ar_5 >= 0 /\ ar_1 <= 0 ]
(Comp: 1, Cost: 11) main_LE_153(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5, ar_6) -> Com_1(main_LE_178(ar_0, i59'*i62', 9, ar_2, ar_3, ar_4, ar_5)) [ ar_5 >= 0 /\ 1 <= ar_1 /\ i59'*i62' = i63' /\ 0 < ar_1 ]
(Comp: 1, Cost: 53) koat_start(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5, ar_6) -> Com_1(main_LE_153(ar_0, 100*ar_0 + i8'', 100*ar_0, i8'', ar_1, static'1', arityPad')) [ 0 <= 0 /\ div = i8' /\ 200*ar_0 = i6' /\ 100*ar_0 = i4' /\ static'1 <= static''' + 1 /\ 0 <= static''' /\ static''' <= ar_2 + 2 /\ 0 <= ar_2 /\ 0 <= static'1 /\ ar_2 >= 0 /\ i6'' - 13*div' < 13 /\ 0 < i6'' - 13*div' + 13 /\ div' = i8'' /\ 200*ar_0 = i6'' /\ 100*ar_0 = i4'' /\ static'1' <= static'''' + 1 /\ 0 <= static'''' /\ static'''' <= ar_2 + 2 /\ 0 <= static'1' /\ static'1' >= 0 /\ 100*ar_0 + i8'' = i46' ]
start location: koat_start
leaf cost: 0

A polynomial rank function with
Pol(main_LE_178) = 1
Pol(main_LE_155) = 0
Pol(main_LE_153) = 1
Pol(koat_start) = 1
orients all transitions weakly and the transition
main_LE_178(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5, ar_6) -> Com_1(main_LE_155(ar_0, ar_3 + ar_4 - 1, ar_3 - 1, ar_4, ar_5, ar_6, arityPad)) [ ar_6 >= 0 /\ ar_2 + ar_6 - 9 >= 0 /\ -ar_2 + ar_6 + 9 >= 0 /\ -ar_2 + 9 >= 0 /\ ar_2 - 9 >= 0 /\ 10 <= ar_1 /\ ar_3 - 1 = i75' /\ 9 < ar_1 /\ ar_2 = 9 /\ ar_3 + ar_4 - 1 = i46' /\ ar_3 + ar_4 - 1 <= 0 ]
strictly and produces the following problem:
19: T:
(Comp: 1, Cost: 6) main_LE_178(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5, ar_6) -> Com_1(main_LE_155(ar_0, ar_3 + ar_4 - 1, ar_3 - 1, ar_4, ar_5, ar_6, arityPad)) [ ar_6 >= 0 /\ ar_2 + ar_6 - 9 >= 0 /\ -ar_2 + ar_6 + 9 >= 0 /\ -ar_2 + 9 >= 0 /\ ar_2 - 9 >= 0 /\ 10 <= ar_1 /\ ar_3 - 1 = i75' /\ 9 < ar_1 /\ ar_2 = 9 /\ ar_3 + ar_4 - 1 = i46' /\ ar_3 + ar_4 - 1 <= 0 ]
(Comp: ?, Cost: 17) main_LE_178(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5, ar_6) -> Com_1(main_LE_178(ar_0, i59'*i62', 9, ar_3 - 1, ar_4, ar_5, ar_6)) [ ar_6 >= 0 /\ ar_2 + ar_6 - 9 >= 0 /\ -ar_2 + ar_6 + 9 >= 0 /\ -ar_2 + 9 >= 0 /\ ar_2 - 9 >= 0 /\ 10 <= ar_1 /\ ar_3 - 1 = i75' /\ 9 < ar_1 /\ ar_2 = 9 /\ ar_3 + ar_4 - 1 = i46' /\ 1 <= ar_3 + ar_4 - 1 /\ i59'*i62' = i63' /\ 0 < ar_3 + ar_4 - 1 ]
(Comp: 1, Cost: 6) main_LE_178(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5, ar_6) -> Com_1(main_LE_155(ar_0, ar_3 + ar_4 - 1, ar_3, ar_4 - 1, ar_5, ar_6, arityPad)) [ ar_6 >= 0 /\ ar_2 + ar_6 - 9 >= 0 /\ -ar_2 + ar_6 + 9 >= 0 /\ -ar_2 + 9 >= 0 /\ ar_2 - 9 >= 0 /\ ar_1 <= 9 /\ ar_4 - 1 = i73' /\ ar_2 = 9 /\ ar_3 + ar_4 - 1 = i46' /\ ar_3 + ar_4 - 1 <= 0 ]
(Comp: 1500*ar_0 + 12, Cost: 17) main_LE_178(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5, ar_6) -> Com_1(main_LE_178(ar_0, i59'*i62', 9, ar_3, ar_4 - 1, ar_5, ar_6)) [ ar_6 >= 0 /\ ar_2 + ar_6 - 9 >= 0 /\ -ar_2 + ar_6 + 9 >= 0 /\ -ar_2 + 9 >= 0 /\ ar_2 - 9 >= 0 /\ ar_1 <= 9 /\ ar_4 - 1 = i73' /\ ar_2 = 9 /\ ar_3 + ar_4 - 1 = i46' /\ 1 <= ar_3 + ar_4 - 1 /\ i59'*i62' = i63' /\ 0 < ar_3 + ar_4 - 1 ]
(Comp: 1, Cost: 0) main_LE_153(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5, ar_6) -> Com_1(main_LE_155(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5, arityPad)) [ ar_5 >= 0 /\ ar_1 <= 0 ]
(Comp: 1, Cost: 11) main_LE_153(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5, ar_6) -> Com_1(main_LE_178(ar_0, i59'*i62', 9, ar_2, ar_3, ar_4, ar_5)) [ ar_5 >= 0 /\ 1 <= ar_1 /\ i59'*i62' = i63' /\ 0 < ar_1 ]
(Comp: 1, Cost: 53) koat_start(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5, ar_6) -> Com_1(main_LE_153(ar_0, 100*ar_0 + i8'', 100*ar_0, i8'', ar_1, static'1', arityPad')) [ 0 <= 0 /\ div = i8' /\ 200*ar_0 = i6' /\ 100*ar_0 = i4' /\ static'1 <= static''' + 1 /\ 0 <= static''' /\ static''' <= ar_2 + 2 /\ 0 <= ar_2 /\ 0 <= static'1 /\ ar_2 >= 0 /\ i6'' - 13*div' < 13 /\ 0 < i6'' - 13*div' + 13 /\ div' = i8'' /\ 200*ar_0 = i6'' /\ 100*ar_0 = i4'' /\ static'1' <= static'''' + 1 /\ 0 <= static'''' /\ static'''' <= ar_2 + 2 /\ 0 <= static'1' /\ static'1' >= 0 /\ 100*ar_0 + i8'' = i46' ]
start location: koat_start
leaf cost: 0

A polynomial rank function with
Pol(main_LE_178) = 13*V_4 + 13*V_5
Pol(main_LE_155) = 13*V_3 + 13*V_4
Pol(main_LE_153) = 13*V_3 + 13*V_4
Pol(koat_start) = 1500*V_1 + 12
orients all transitions weakly and the transition
main_LE_178(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5, ar_6) -> Com_1(main_LE_178(ar_0, i59'*i62', 9, ar_3 - 1, ar_4, ar_5, ar_6)) [ ar_6 >= 0 /\ ar_2 + ar_6 - 9 >= 0 /\ -ar_2 + ar_6 + 9 >= 0 /\ -ar_2 + 9 >= 0 /\ ar_2 - 9 >= 0 /\ 10 <= ar_1 /\ ar_3 - 1 = i75' /\ 9 < ar_1 /\ ar_2 = 9 /\ ar_3 + ar_4 - 1 = i46' /\ 1 <= ar_3 + ar_4 - 1 /\ i59'*i62' = i63' /\ 0 < ar_3 + ar_4 - 1 ]
strictly and produces the following problem:
20: T:
(Comp: 1, Cost: 6) main_LE_178(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5, ar_6) -> Com_1(main_LE_155(ar_0, ar_3 + ar_4 - 1, ar_3 - 1, ar_4, ar_5, ar_6, arityPad)) [ ar_6 >= 0 /\ ar_2 + ar_6 - 9 >= 0 /\ -ar_2 + ar_6 + 9 >= 0 /\ -ar_2 + 9 >= 0 /\ ar_2 - 9 >= 0 /\ 10 <= ar_1 /\ ar_3 - 1 = i75' /\ 9 < ar_1 /\ ar_2 = 9 /\ ar_3 + ar_4 - 1 = i46' /\ ar_3 + ar_4 - 1 <= 0 ]
(Comp: 1500*ar_0 + 12, Cost: 17) main_LE_178(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5, ar_6) -> Com_1(main_LE_178(ar_0, i59'*i62', 9, ar_3 - 1, ar_4, ar_5, ar_6)) [ ar_6 >= 0 /\ ar_2 + ar_6 - 9 >= 0 /\ -ar_2 + ar_6 + 9 >= 0 /\ -ar_2 + 9 >= 0 /\ ar_2 - 9 >= 0 /\ 10 <= ar_1 /\ ar_3 - 1 = i75' /\ 9 < ar_1 /\ ar_2 = 9 /\ ar_3 + ar_4 - 1 = i46' /\ 1 <= ar_3 + ar_4 - 1 /\ i59'*i62' = i63' /\ 0 < ar_3 + ar_4 - 1 ]
(Comp: 1, Cost: 6) main_LE_178(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5, ar_6) -> Com_1(main_LE_155(ar_0, ar_3 + ar_4 - 1, ar_3, ar_4 - 1, ar_5, ar_6, arityPad)) [ ar_6 >= 0 /\ ar_2 + ar_6 - 9 >= 0 /\ -ar_2 + ar_6 + 9 >= 0 /\ -ar_2 + 9 >= 0 /\ ar_2 - 9 >= 0 /\ ar_1 <= 9 /\ ar_4 - 1 = i73' /\ ar_2 = 9 /\ ar_3 + ar_4 - 1 = i46' /\ ar_3 + ar_4 - 1 <= 0 ]
(Comp: 1500*ar_0 + 12, Cost: 17) main_LE_178(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5, ar_6) -> Com_1(main_LE_178(ar_0, i59'*i62', 9, ar_3, ar_4 - 1, ar_5, ar_6)) [ ar_6 >= 0 /\ ar_2 + ar_6 - 9 >= 0 /\ -ar_2 + ar_6 + 9 >= 0 /\ -ar_2 + 9 >= 0 /\ ar_2 - 9 >= 0 /\ ar_1 <= 9 /\ ar_4 - 1 = i73' /\ ar_2 = 9 /\ ar_3 + ar_4 - 1 = i46' /\ 1 <= ar_3 + ar_4 - 1 /\ i59'*i62' = i63' /\ 0 < ar_3 + ar_4 - 1 ]
(Comp: 1, Cost: 0) main_LE_153(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5, ar_6) -> Com_1(main_LE_155(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5, arityPad)) [ ar_5 >= 0 /\ ar_1 <= 0 ]
(Comp: 1, Cost: 11) main_LE_153(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5, ar_6) -> Com_1(main_LE_178(ar_0, i59'*i62', 9, ar_2, ar_3, ar_4, ar_5)) [ ar_5 >= 0 /\ 1 <= ar_1 /\ i59'*i62' = i63' /\ 0 < ar_1 ]
(Comp: 1, Cost: 53) koat_start(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5, ar_6) -> Com_1(main_LE_153(ar_0, 100*ar_0 + i8'', 100*ar_0, i8'', ar_1, static'1', arityPad')) [ 0 <= 0 /\ div = i8' /\ 200*ar_0 = i6' /\ 100*ar_0 = i4' /\ static'1 <= static''' + 1 /\ 0 <= static''' /\ static''' <= ar_2 + 2 /\ 0 <= ar_2 /\ 0 <= static'1 /\ ar_2 >= 0 /\ i6'' - 13*div' < 13 /\ 0 < i6'' - 13*div' + 13 /\ div' = i8'' /\ 200*ar_0 = i6'' /\ 100*ar_0 = i4'' /\ static'1' <= static'''' + 1 /\ 0 <= static'''' /\ static'''' <= ar_2 + 2 /\ 0 <= static'1' /\ static'1' >= 0 /\ 100*ar_0 + i8'' = i46' ]
start location: koat_start
leaf cost: 0

Complexity upper bound 51000*ar_0 + 484

Time: 2.443 sec (SMT: 2.030 sec)

(28) BOUNDS(CONSTANT, 484 + 51000 * |#0|)

(29) TerminationGraphToComplexityProof (BOTH CONCRETE BOUNDS(ID, ADD(2)) transformation)

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

(30) Obligation:

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

Used field analysis yielded the following read fields:

Considered paths: all paths from start

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

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

(32) Obligation:

IntTrs with 59 rules
Start term: main_Load_1(#0, env, static)
Considered paths: all paths from start
Rules:
main_Load_1(i1, env, static) -{0,0}> main_Load_3(i1, env, static) :|: 0 >= 0
main_Load_3(i1, env, static) -{0,0}> langle_clinit_rangle_ConstantStackPush_6(i1, env, static) :|: 0 >= 0
langle_clinit_rangle_ConstantStackPush_6(i1, env, static) -{1,1}> langle_clinit_rangle_ArrayCreate_12(iconst_0, i1, env, static) :|: iconst_0 = 0
langle_clinit_rangle_ArrayCreate_12(iconst_0, i1, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_14(a2, i1, iconst_0, env, static) :|: a2 = 2 && iconst_0 = 0 && 0 < a2
langle_clinit_rangle_FieldAccess_14(a2, i1, iconst_0, env, static) -{1,1}> langle_clinit_rangle_New_16(i1, env, static') :|: 0 <= a2 && iconst_0 = 0 && static' <= static + a2 && 0 <= static && 0 < a2
langle_clinit_rangle_New_16(i1, env, static) -{0,0}> langle_clinit_rangle_New_17(i1, env, static) :|: 0 >= 0
langle_clinit_rangle_New_17(i1, env, static) -{0,0}> langle_clinit_rangle_New_19(i1, env, static) :|: 0 <= static
langle_clinit_rangle_New_19(i1, env, static) -{1,1}> langle_clinit_rangle_Duplicate_20(o2, i1, env, static) :|: 0 < o2 && o2 = 1
langle_clinit_rangle_Duplicate_20(o2, i1, env, static) -{1,1}> langle_clinit_rangle_ConstantStackPush_22(o2, i1, env, static) :|: 0 < o2
langle_clinit_rangle_ConstantStackPush_22(o2, i1, env, static) -{1,1}> langle_clinit_rangle_InvokeMethod_23(o2, NULL, i1, env, static) :|: NULL = 0 && 0 < o2
langle_clinit_rangle_InvokeMethod_23(o2, NULL, i1, env, static) -{1,1}> langle_init_rangle_Load_24(o2, i1, env, static) :|: NULL = 0 && 0 < o2
langle_init_rangle_Load_24(o2, i1, env, static) -{1,1}> langle_init_rangle_InvokeMethod_27(o2, i1, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_27(o2, i1, env, static) -{1,1}> langle_init_rangle_Load_28(o2, i1, env, static) :|: 0 < o2
langle_init_rangle_Load_28(o2, i1, env, static) -{1,1}> langle_init_rangle_InvokeMethod_30(o2, i1, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_30(o2, i1, env, static) -{1,1}> langle_init_rangle_Return_33(o2, i1, env, static) :|: 0 < o2
langle_init_rangle_Return_33(o2, i1, env, static) -{1,1}> langle_init_rangle_Return_35(o2, i1, env, static) :|: 0 < o2
langle_init_rangle_Return_35(o2, i1, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_38(o2, i1, env, static) :|: 0 < o2
langle_clinit_rangle_FieldAccess_38(o2, i1, env, static) -{1,1}> langle_clinit_rangle_Return_40(i1, env, static') :|: 0 < o2 && 0 <= o2 && 0 <= static && static' <= static + o2
langle_clinit_rangle_Return_40(i1, env, static) -{1,1}> main_Load_41(i1, env, static) :|: 0 >= 0
main_Load_41(i1, env, static) -{0,0}> main_Load_42(i1, env, static) :|: 0 >= 0
main_Load_42(i1, env, static) -{0,0}> main_Load_44(i1, env, static) :|: 0 <= static
main_Load_44(i1, env, static) -{0,0}> main_Load_46(i1, env, static) :|: 0 >= 0
main_Load_46(i1, env, static) -{0,0}> main_Load_48(i1, env, static) :|: 0 >= 0
main_Load_48(i1, env, static) -{1,1}> main_ConstantStackPush_50(i1, env, static) :|: 0 >= 0
main_ConstantStackPush_50(i1, env, static) -{1,1}> main_IntArithmetic_52(i1, iconst_100, env, static) :|: iconst_100 = 100
main_IntArithmetic_52(i1, iconst_100, env, static) -{1,1}> main_Store_54(i1, i4, env, static) :|: i1 * iconst_100 = i4 && iconst_100 = 100
main_Store_54(i1, i4, env, static) -{1,1}> main_Load_56(i1, i4, env, static) :|: 0 >= 0
main_Load_56(i1, i4, env, static) -{1,1}> main_ConstantStackPush_58(i1, i4, env, static) :|: 0 >= 0
main_ConstantStackPush_58(i1, i4, env, static) -{1,1}> main_IntArithmetic_60(i1, iconst_200, i4, env, static) :|: iconst_200 = 200
main_IntArithmetic_60(i1, iconst_200, i4, env, static) -{1,1}> main_ConstantStackPush_63(i1, i6, i4, env, static) :|: i1 * iconst_200 = i6 && iconst_200 = 200
main_ConstantStackPush_63(i1, i6, i4, env, static) -{1,1}> main_IntArithmetic_65(i1, i6, iconst_13, i4, env, static) :|: iconst_13 = 13
main_IntArithmetic_65(i1, i6, iconst_13, i4, env, static) -{1,1}> main_Store_67(i1, i8, i4, env, static) :|: iconst_13 = 13
main_Store_67(i1, i8, i4, env, static) -{1,1}> main_Load_70(i1, i4, i8, env, static) :|: 0 >= 0
main_Load_70(i1, i4, i8, env, static) -{0,0}> main_Load_142(i1, i4, i8, env, static) :|: 0 >= 0
main_Load_142(i1, i4, i33, env, static) -{1,1}> main_Load_148(i1, i4, i33, env, static) :|: 0 >= 0
main_Load_148(i1, i4, i33, env, static) -{1,1}> main_IntArithmetic_150(i1, i4, i33, env, static) :|: 0 >= 0
main_IntArithmetic_150(i1, i4, i33, env, static) -{1,1}> main_LE_153(i1, i46, i4, i33, env, static) :|: i4 + i33 = i46
main_LE_153(i1, i54, i4, i33, env, static) -{0,0}> main_LE_156(i1, i54, i4, i33, env, static) :|: 1 <= i54
main_LE_156(i1, i54, i4, i33, env, static) -{1,1}> main_New_161(i1, i4, i33, env, static) :|: 1 <= i54 && 0 < i54
main_New_161(i1, i4, i33, env, static) -{1,1}> main_Duplicate_164(i1, o12, i4, i33, env, static) :|: 0 < o12 && o12 = 1
main_Duplicate_164(i1, o12, i4, i33, env, static) -{1,1}> main_InvokeMethod_165(i1, o12, i4, i33, env, static) :|: 0 < o12
main_InvokeMethod_165(i1, o12, i4, i33, env, static) -{1,1}> main_InvokeMethod_166(i1, o12, i4, i33, env, static) :|: 0 < o12
main_InvokeMethod_166(i1, o12, i4, i33, env, static) -{1,1}> main_New_169(i1, i59, i4, i33, env, static) :|: 0 < o12
main_New_169(i1, i59, i4, i33, env, static) -{1,1}> main_Duplicate_170(i1, i59, o13, i4, i33, env, static) :|: 0 < o13 && o13 = 1
main_Duplicate_170(i1, i59, o13, i4, i33, env, static) -{1,1}> main_InvokeMethod_171(i1, i59, o13, i4, i33, env, static) :|: 0 < o13
main_InvokeMethod_171(i1, i59, o13, i4, i33, env, static) -{1,1}> main_InvokeMethod_174(i1, i59, o13, i4, i33, env, static) :|: 0 < o13
main_InvokeMethod_174(i1, i59, o13, i4, i33, env, static) -{1,1}> main_IntArithmetic_175(i1, i59, i62, i4, i33, env, static) :|: 0 < o13
main_IntArithmetic_175(i1, i59, i62, i4, i33, env, static) -{1,1}> main_ConstantStackPush_176(i1, i63, i4, i33, env, static) :|: i59 * i62 = i63
main_ConstantStackPush_176(i1, i63, i4, i33, env, static) -{1,1}> main_LE_178(i1, i63, iconst_9, i4, i33, env, static) :|: iconst_9 = 9
main_LE_178(i1, i68, iconst_9, i4, i33, env, static) -{0,0}> main_LE_179(i1, i68, iconst_9, i4, i33, env, static) :|: i68 <= 9 && iconst_9 = 9
main_LE_178(i1, i69, iconst_9, i4, i33, env, static) -{0,0}> main_LE_180(i1, i69, iconst_9, i4, i33, env, static) :|: 10 <= i69 && iconst_9 = 9
main_LE_179(i1, i68, iconst_9, i4, i33, env, static) -{1,1}> main_Inc_183(i1, i4, i33, env, static) :|: i68 <= iconst_9 && i68 <= 9 && iconst_9 = 9
main_LE_180(i1, i69, iconst_9, i4, i33, env, static) -{1,1}> main_Inc_186(i1, i4, i33, env, static) :|: iconst_9 < i69 && 10 <= i69 && iconst_9 = 9
main_Inc_183(i1, i4, i33, env, static) -{1,1}> main_JMP_190(i1, i4, i73, env, static) :|: i33 + -1 = i73
main_Inc_186(i1, i4, i33, env, static) -{1,1}> main_JMP_193(i1, i75, i33, env, static) :|: i4 + -1 = i75
main_JMP_190(i1, i4, i73, env, static) -{1,1}> main_Load_200(i1, i4, i73, env, static) :|: 0 >= 0
main_JMP_193(i1, i75, i33, env, static) -{1,1}> main_Load_207(i1, i75, i33, env, static) :|: 0 >= 0
main_Load_200(i1, i4, i73, env, static) -{0,0}> main_Load_142(i1, i4, i73, env, static) :|: 0 >= 0
main_Load_207(i1, i75, i33, env, static) -{0,0}> main_Load_142(i1, i75, i33, env, static) :|: 0 >= 0

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

obtained
main_Load_142(i1, i4, i33, env, static) -{14,14}> main_LE_178(i1, i63', 9, i4, i33, env, static) :|: 1 <= i46' && 0 < 1 && i4 + i33 = i46' && 0 < i46' && i59' * i62' = i63' && 0 >= 0
by chaining
main_Load_142(i1, i4, i33, env, static) -{1,1}> main_Load_148(i1, i4, i33, env, static) :|: 0 >= 0
main_Load_148(i1, i4, i33, env, static) -{1,1}> main_IntArithmetic_150(i1, i4, i33, env, static) :|: 0 >= 0
main_IntArithmetic_150(i1, i4, i33, env, static) -{1,1}> main_LE_153(i1, i46, i4, i33, env, static) :|: i4 + i33 = i46
main_LE_153(i1, i54, i4, i33, env, static) -{0,0}> main_LE_156(i1, i54, i4, i33, env, static) :|: 1 <= i54
main_LE_156(i1, i54, i4, i33, env, static) -{1,1}> main_New_161(i1, i4, i33, env, static) :|: 1 <= i54 && 0 < i54
main_New_161(i1, i4, i33, env, static) -{1,1}> main_Duplicate_164(i1, o12, i4, i33, env, static) :|: 0 < o12 && o12 = 1
main_Duplicate_164(i1, o12, i4, i33, env, static) -{1,1}> main_InvokeMethod_165(i1, o12, i4, i33, env, static) :|: 0 < o12
main_InvokeMethod_165(i1, o12, i4, i33, env, static) -{1,1}> main_InvokeMethod_166(i1, o12, i4, i33, env, static) :|: 0 < o12
main_InvokeMethod_166(i1, o12, i4, i33, env, static) -{1,1}> main_New_169(i1, i59, i4, i33, env, static) :|: 0 < o12
main_New_169(i1, i59, i4, i33, env, static) -{1,1}> main_Duplicate_170(i1, i59, o13, i4, i33, env, static) :|: 0 < o13 && o13 = 1
main_Duplicate_170(i1, i59, o13, i4, i33, env, static) -{1,1}> main_InvokeMethod_171(i1, i59, o13, i4, i33, env, static) :|: 0 < o13
main_InvokeMethod_171(i1, i59, o13, i4, i33, env, static) -{1,1}> main_InvokeMethod_174(i1, i59, o13, i4, i33, env, static) :|: 0 < o13
main_InvokeMethod_174(i1, i59, o13, i4, i33, env, static) -{1,1}> main_IntArithmetic_175(i1, i59, i62, i4, i33, env, static) :|: 0 < o13
main_IntArithmetic_175(i1, i59, i62, i4, i33, env, static) -{1,1}> main_ConstantStackPush_176(i1, i63, i4, i33, env, static) :|: i59 * i62 = i63
main_ConstantStackPush_176(i1, i63, i4, i33, env, static) -{1,1}> main_LE_178(i1, i63, iconst_9, i4, i33, env, static) :|: iconst_9 = 9

(34) Obligation:

IntTrs with 4 rules
Start term: main_Load_1(#0, env, static)
Considered paths: all paths from start
Rules:
main_Load_1(i1, env, static) -{25,25}> main_Load_142(i1, i4', i8', env, static'1) :|: 0 >= 0 && i1 * 100 = i4' && i1 * 200 = i6' && static'1 <= static''' + 1 && 0 <= 2 && 0 <= static''' && static''' <= static + 2 && 0 < 1 && 0 <= 1 && 0 <= static && 0 < 2 && 0 <= static'1
main_Load_142(i1, i4, i33, env, static) -{14,14}> main_LE_178(i1, i63', 9, i4, i33, env, static) :|: 1 <= i46' && 0 < 1 && i4 + i33 = i46' && 0 < i46' && i59' * i62' = i63' && 0 >= 0
main_LE_178(i1, i69, 9, i4, i33, env, static) -{3,3}> main_Load_142(i1, i75', i33, env, static) :|: 0 >= 0 && 10 <= i69 && i4 + -1 = i75' && 9 < i69
main_LE_178(i1, i68, 9, i4, i33, env, static) -{3,3}> main_Load_142(i1, i4, i73', env, static) :|: 0 >= 0 && i68 <= 9 && i33 + -1 = i73'

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

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

main_Load_1(x1, x2, x3) → main_Load_1(x1, x3)
main_Load_142(x1, x2, x3, x4, x5) → main_Load_142(x1, x2, x3)
main_LE_178(x1, x2, x3, x4, x5, x6, x7) → main_LE_178(x2, x4, x5)

(36) Obligation:

IntTrs with 4 rules
Start term: main_Load_1(#0, static)
Considered paths: all paths from start
Rules:
main_Load_1(i1, static) -{25,25}> main_Load_142(i1, i4', i8') :|: 0 >= 0 && i1 * 100 = i4' && i1 * 200 = i6' && static'1 <= static''' + 1 && 0 <= 2 && 0 <= static''' && static''' <= static + 2 && 0 < 1 && 0 <= 1 && 0 <= static && 0 < 2 && 0 <= static'1
main_Load_142(i1, i4, i33) -{14,14}> main_LE_178(i63', i4, i33) :|: 1 <= i46' && 0 < 1 && i4 + i33 = i46' && 0 < i46' && i59' * i62' = i63' && 0 >= 0
main_LE_178(i69, i4, i33) -{3,3}> main_Load_142(i1, i75', i33) :|: 0 >= 0 && 10 <= i69 && i4 + -1 = i75' && 9 < i69
main_LE_178(i68, i4, i33) -{3,3}> main_Load_142(i1, i4, i73') :|: 0 >= 0 && i68 <= 9 && i33 + -1 = i73'

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

Moved arithmethic from constraints to rhss.

main_Load_142(i1, i4, i33) -{14,14}> main_LE_178(i63', i4, i33) :|: 1 <= i46' && 0 < 1 && i4 + i33 = i46' && 0 < i46' && i59' * i62' = i63' && 0 >= 0
was transformed to
main_Load_142(i1, i4, i33) -{14,14}> main_LE_178(i59' * i62', i4, i33) :|: 1 <= i46' && 0 < 1 && i4 + i33 = i46' && 0 < i46' && i59' * i62' = i63' && 0 >= 0

main_LE_178(i69, i4, i33) -{3,3}> main_Load_142(i1, i75', i33) :|: 0 >= 0 && 10 <= i69 && i4 + -1 = i75' && 9 < i69
was transformed to
main_LE_178(i69, i4, i33) -{3,3}> main_Load_142(i1, i4 + -1, i33) :|: 0 >= 0 && 10 <= i69 && i4 + -1 = i75' && 9 < i69

main_LE_178(i68, i4, i33) -{3,3}> main_Load_142(i1, i4, i73') :|: 0 >= 0 && i68 <= 9 && i33 + -1 = i73'
was transformed to
main_LE_178(i68, i4, i33) -{3,3}> main_Load_142(i1, i4, i33 + -1) :|: 0 >= 0 && i68 <= 9 && i33 + -1 = i73'

main_Load_1(i1, static) -{25,25}> main_Load_142(i1, i4', i8') :|: 0 >= 0 && i1 * 100 = i4' && i1 * 200 = i6' && static'1 <= static''' + 1 && 0 <= 2 && 0 <= static''' && static''' <= static + 2 && 0 < 1 && 0 <= 1 && 0 <= static && 0 < 2 && 0 <= static'1
was transformed to
main_Load_1(i1, static) -{25,25}> main_Load_142(i1, i1 * 100, i8') :|: 0 >= 0 && i1 * 100 = i4' && i1 * 200 = i6' && static'1 <= static''' + 1 && 0 <= 2 && 0 <= static''' && static''' <= static + 2 && 0 < 1 && 0 <= 1 && 0 <= static && 0 < 2 && 0 <= static'1

(38) Obligation:

IntTrs with 4 rules
Start term: main_Load_1(#0, static)
Considered paths: all paths from start
Rules:
main_Load_142(i1, i4, i33) -{14,14}> main_LE_178(i59' * i62', i4, i33) :|: 1 <= i46' && 0 < 1 && i4 + i33 = i46' && 0 < i46' && i59' * i62' = i63' && 0 >= 0
main_LE_178(i69, i4, i33) -{3,3}> main_Load_142(i1, i4 + -1, i33) :|: 0 >= 0 && 10 <= i69 && i4 + -1 = i75' && 9 < i69
main_LE_178(i68, i4, i33) -{3,3}> main_Load_142(i1, i4, i33 + -1) :|: 0 >= 0 && i68 <= 9 && i33 + -1 = i73'
main_Load_1(i1, static) -{25,25}> main_Load_142(i1, i1 * 100, i8') :|: 0 >= 0 && i1 * 100 = i4' && i1 * 200 = i6' && static'1 <= static''' + 1 && 0 <= 2 && 0 <= static''' && static''' <= static + 2 && 0 < 1 && 0 <= 1 && 0 <= static && 0 < 2 && 0 <= static'1

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

Simplified expressions.

main_LE_178(i69, i4, i33) -{3,3}> main_Load_142(i1, i4 + -1, i33) :|: 0 >= 0 && 10 <= i69 && i4 + -1 = i75' && 9 < i69
was transformed to
main_LE_178(i69, i4, i33) -{3,3}> main_Load_142(i1, i4 - 1, i33) :|: 10 <= i69 && i4 - 1 = i75' && 9 < i69

main_LE_178(i68, i4, i33) -{3,3}> main_Load_142(i1, i4, i33 + -1) :|: 0 >= 0 && i68 <= 9 && i33 + -1 = i73'
was transformed to
main_LE_178(i68, i4, i33) -{3,3}> main_Load_142(i1, i4, i33 - 1) :|: i68 <= 9 && i33 - 1 = i73'

main_Load_142(i1, i4, i33) -{14,14}> main_LE_178(i59' * i62', i4, i33) :|: 1 <= i46' && 0 < 1 && i4 + i33 = i46' && 0 < i46' && i59' * i62' = i63' && 0 >= 0
was transformed to
main_Load_142(i1, i4, i33) -{14,14}> main_LE_178(i59' * i62', i4, i33) :|: 1 <= i46' && i4 + i33 = i46' && 0 < i46' && i59' * i62' = i63'

main_Load_1(i1, static) -{25,25}> main_Load_142(i1, i1 * 100, i8') :|: 0 >= 0 && i1 * 100 = i4' && i1 * 200 = i6' && static'1 <= static''' + 1 && 0 <= 2 && 0 <= static''' && static''' <= static + 2 && 0 < 1 && 0 <= 1 && 0 <= static && 0 < 2 && 0 <= static'1
was transformed to
main_Load_1(i1, static) -{25,25}> main_Load_142(i1, 100 * i1, i8') :|: 100 * i1 = i4' && 200 * i1 = i6' && static'1 <= static''' + 1 && 0 <= static''' && static''' <= static + 2 && 0 <= static && 0 <= static'1

(40) Obligation:

IntTrs with 4 rules
Start term: main_Load_1(#0, static)
Considered paths: all paths from start
Rules:
main_LE_178(i69, i4, i33) -{3,3}> main_Load_142(i1, i4 - 1, i33) :|: 10 <= i69 && i4 - 1 = i75' && 9 < i69
main_Load_1(i1, static) -{25,25}> main_Load_142(i1, 100 * i1, i8') :|: 100 * i1 = i4' && 200 * i1 = i6' && static'1 <= static''' + 1 && 0 <= static''' && static''' <= static + 2 && 0 <= static && 0 <= static'1
main_LE_178(i68, i4, i33) -{3,3}> main_Load_142(i1, i4, i33 - 1) :|: i68 <= 9 && i33 - 1 = i73'
main_Load_142(i1, i4, i33) -{14,14}> main_LE_178(i59' * i62', i4, i33) :|: 1 <= i46' && i4 + i33 = i46' && 0 < i46' && i59' * i62' = i63'