time complexity proof of /tmp/tmpwosM6W/PastaC5.jar

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

0 JBC problem

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

↳2 JBCTerminationGraph

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

↳4 JBCComplexityEdges

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

    ↳6 WeightedIntTrs

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

        ↳8 WeightedIntTrs

        ↳9 RemoveDivModProof (CONCRETE UPPER BOUND(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), 99 ms)

    ↳16 WeightedIntTrs

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

        ↳18 WeightedIntTrs

        ↳19 RemoveDivModProof (CONCRETE UPPER BOUND(ID), 9 ms)

        ↳20 WeightedIntTrs

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

        ↳22 WeightedIntTrs

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

        ↳24 WeightedIntTrs

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

↳26 JBCComplexityEdges

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

    ↳28 WeightedIntTrs

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

    ↳30 WeightedIntTrs

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

    ↳32 WeightedIntTrs

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

    ↳34 WeightedIntTrs

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

    ↳36 WeightedIntTrs

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

    ↳38 WeightedIntTrs

    ↳39 koat Proof (⇔, 73 ms)

    ↳40 BOUNDS(CONSTANT, 19 + 44 * |#0| + 44 * |#1|)

(0) Obligation:

Need to prove time_complexity of the following program:

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

public class PastaC5 {
    public static void main(int x, int y) {
        if (x > 0 && y > 0) {
            while (x != y) {
                if (x > y) {
                    x = x - y;
                } else {
                    y = y - x;
                }
            }
        }
    }
}

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

Constructed TerminationGraph.

(2) Obligation:

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

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

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

(4) Obligation:

Set of 55 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 55 jbc graph edges to a weighted ITS with 55 rules.
Filtered conditions with variables that do not depend on the variables on the lhs or rhs without taking transitive dependencies into account.
Did no encode lower bounds for putfield and astore.

(6) Obligation:

IntTrs with 55 rules
Start term: main_Load_1(#0, #1, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_Load_1(i1, i3, env, static) -{0,0}> main_Load_4(i1, i3, env, static) :|: 0 >= 0
main_Load_4(i1, i3, env, static) -{0,0}> langle_clinit_rangle_ConstantStackPush_6(i1, i3, env, static) :|: 0 >= 0
langle_clinit_rangle_ConstantStackPush_6(i1, i3, env, static) -{1,1}> langle_clinit_rangle_ArrayCreate_12(iconst_0, i1, i3, env, static) :|: iconst_0 = 0
langle_clinit_rangle_ArrayCreate_12(iconst_0, i1, i3, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_14(a2, i1, i3, iconst_0, env, static) :|: a2 = 2 && iconst_0 = 0 && 0 < a2
langle_clinit_rangle_FieldAccess_14(a2, i1, i3, iconst_0, env, static) -{1,1}> langle_clinit_rangle_New_16(i1, i3, env, static') :|: 0 <= a2 && iconst_0 = 0 && static' <= static + a2 && 0 <= static && 0 < a2
langle_clinit_rangle_New_16(i1, i3, env, static) -{0,0}> langle_clinit_rangle_New_18(i1, i3, env, static) :|: 0 >= 0
langle_clinit_rangle_New_18(i1, i3, env, static) -{0,0}> langle_clinit_rangle_New_19(i1, i3, env, static) :|: 0 <= static
langle_clinit_rangle_New_19(i1, i3, env, static) -{1,1}> langle_clinit_rangle_Duplicate_20(o2, i1, i3, env, static) :|: 0 < o2 && o2 = 1
langle_clinit_rangle_Duplicate_20(o2, i1, i3, env, static) -{1,1}> langle_clinit_rangle_ConstantStackPush_22(o2, i1, i3, env, static) :|: 0 < o2
langle_clinit_rangle_ConstantStackPush_22(o2, i1, i3, env, static) -{1,1}> langle_clinit_rangle_InvokeMethod_23(o2, NULL, i1, i3, env, static) :|: NULL = 0 && 0 < o2
langle_clinit_rangle_InvokeMethod_23(o2, NULL, i1, i3, env, static) -{1,1}> langle_init_rangle_Load_25(o2, i1, i3, env, static) :|: NULL = 0 && 0 < o2
langle_init_rangle_Load_25(o2, i1, i3, env, static) -{1,1}> langle_init_rangle_InvokeMethod_27(o2, i1, i3, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_27(o2, i1, i3, env, static) -{1,1}> langle_init_rangle_Load_29(o2, i1, i3, env, static) :|: 0 < o2
langle_init_rangle_Load_29(o2, i1, i3, env, static) -{1,1}> langle_init_rangle_InvokeMethod_31(o2, i1, i3, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_31(o2, i1, i3, env, static) -{1,1}> langle_init_rangle_Return_34(o2, i1, i3, env, static) :|: 0 < o2
langle_init_rangle_Return_34(o2, i1, i3, env, static) -{1,1}> langle_init_rangle_Return_36(o2, i1, i3, env, static) :|: 0 < o2
langle_init_rangle_Return_36(o2, i1, i3, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_39(o2, i1, i3, env, static) :|: 0 < o2
langle_clinit_rangle_FieldAccess_39(o2, i1, i3, env, static) -{1,1}> langle_clinit_rangle_Return_40(i1, i3, env, static') :|: 0 < o2 && 0 <= o2 && 0 <= static && static' <= static + o2
langle_clinit_rangle_Return_40(i1, i3, env, static) -{1,1}> main_Load_41(i1, i3, env, static) :|: 0 >= 0
main_Load_41(i1, i3, env, static) -{0,0}> main_Load_42(i1, i3, env, static) :|: 0 >= 0
main_Load_42(i1, i3, env, static) -{0,0}> main_Load_44(i1, i3, env, static) :|: 0 <= static
main_Load_44(i1, i3, env, static) -{0,0}> main_Load_46(i1, i3, env, static) :|: 0 >= 0
main_Load_46(i1, i3, env, static) -{0,0}> main_Load_48(i1, i3, env, static) :|: 0 >= 0
main_Load_48(i1, i3, env, static) -{1,1}> main_LE_52(i1, i3, env, static) :|: 0 >= 0
main_LE_52(i11, i3, env, static) -{0,0}> main_LE_53(i11, i3, env, static) :|: i11 <= 0
main_LE_52(i12, i3, env, static) -{0,0}> main_LE_54(i12, i3, env, static) :|: 1 <= i12
main_LE_54(i12, i3, env, static) -{1,1}> main_Load_58(i12, i3, env, static) :|: 0 < i12 && 1 <= i12
main_Load_58(i12, i3, env, static) -{1,1}> main_LE_62(i12, i3, env, static) :|: 1 <= i12
main_LE_62(i12, i19, env, static) -{0,0}> main_LE_63(i12, i19, env, static) :|: i19 <= 0 && 1 <= i12
main_LE_62(i12, i20, env, static) -{0,0}> main_LE_64(i12, i20, env, static) :|: 1 <= i20 && 1 <= i12
main_LE_64(i12, i20, env, static) -{1,1}> main_Load_73(i12, i20, env, static) :|: 0 < i20 && 1 <= i20 && 1 <= i12
main_Load_73(i12, i20, env, static) -{0,0}> main_Load_421(i12, i20, i12, i20, env, static) :|: 1 <= i20 && 1 <= i12
main_Load_421(i158, i159, i160, i175, env, static) -{1,1}> main_Load_424(i158, i159, i160, i175, env, static) :|: 1 <= i160 && 1 <= i159 && 1 <= i175
main_Load_424(i158, i159, i160, i175, env, static) -{1,1}> main_EQ_426(i158, i159, i160, i175, env, static) :|: 1 <= i160 && 1 <= i159 && 1 <= i175
main_EQ_426(i158, i159, i160, i175, env, static) -{0,0}> main_EQ_427(i158, i159, i175, env, static) :|: i160 = i175 && 1 <= i160 && 1 <= i159 && 1 <= i175
main_EQ_426(i158, i159, i160, i175, env, static) -{0,0}> main_EQ_428(i158, i159, i160, i175, env, static) :|: 1 <= i160 && 1 <= i159 && !(i160 = i175) && 1 <= i175
main_EQ_428(i158, i159, i160, i175, env, static) -{1,1}> main_Load_432(i158, i159, i160, i175, env, static) :|: 1 <= i160 && 1 <= i159 && !(i160 = i175) && 1 <= i175
main_Load_432(i158, i159, i160, i175, env, static) -{1,1}> main_Load_434(i158, i159, i160, i175, env, static) :|: 1 <= i160 && 1 <= i159 && 1 <= i175
main_Load_434(i158, i159, i160, i175, env, static) -{1,1}> main_LE_437(i158, i159, i160, i175, env, static) :|: 1 <= i160 && 1 <= i159 && 1 <= i175
main_LE_437(i158, i159, i160, i175, env, static) -{0,0}> main_LE_438(i158, i159, i160, i175, env, static) :|: i160 <= i175 && 1 <= i160 && 1 <= i159 && 1 <= i175
main_LE_437(i158, i159, i160, i175, env, static) -{0,0}> main_LE_439(i158, i159, i160, i175, env, static) :|: 1 <= i160 && 1 <= i159 && i175 < i160 && 1 <= i175
main_LE_438(i158, i159, i160, i175, env, static) -{1,1}> main_Load_440(i158, i159, i160, i175, env, static) :|: 1 <= i160 && 1 <= i159 && i160 < i175 && 2 <= i175 && 1 <= i175
main_LE_439(i158, i159, i160, i175, env, static) -{1,1}> main_Load_441(i158, i159, i160, i175, env, static) :|: 1 <= i160 && 1 <= i159 && i175 < i160 && 2 <= i160 && 1 <= i175
main_Load_440(i158, i159, i160, i175, env, static) -{1,1}> main_Load_442(i158, i159, i175, i160, env, static) :|: 1 <= i160 && 1 <= i159 && 2 <= i175
main_Load_441(i158, i159, i160, i175, env, static) -{1,1}> main_Load_443(i158, i159, i160, i175, env, static) :|: 1 <= i159 && 2 <= i160 && 1 <= i175
main_Load_442(i158, i159, i175, i160, env, static) -{1,1}> main_IntArithmetic_444(i158, i159, i175, i160, env, static) :|: 1 <= i160 && 1 <= i159 && 2 <= i175
main_Load_443(i158, i159, i160, i175, env, static) -{1,1}> main_IntArithmetic_445(i158, i159, i160, i175, env, static) :|: 1 <= i159 && 2 <= i160 && 1 <= i175
main_IntArithmetic_444(i158, i159, i175, i160, env, static) -{1,1}> main_Store_446(i158, i159, i182, i160, env, static) :|: 1 <= i182 && 1 <= i160 && 1 <= i159 && 2 <= i175 && i175 - i160 = i182
main_IntArithmetic_445(i158, i159, i160, i175, env, static) -{1,1}> main_Store_447(i158, i159, i183, i175, env, static) :|: i160 - i175 = i183 && 1 <= i183 && 1 <= i159 && 2 <= i160 && 1 <= i175
main_Store_446(i158, i159, i182, i160, env, static) -{1,1}> main_JMP_448(i158, i159, i160, i182, env, static) :|: 1 <= i182 && 1 <= i160 && 1 <= i159
main_Store_447(i158, i159, i183, i175, env, static) -{1,1}> main_JMP_449(i158, i159, i183, i175, env, static) :|: 1 <= i183 && 1 <= i159 && 1 <= i175
main_JMP_448(i158, i159, i160, i182, env, static) -{1,1}> main_Load_450(i158, i159, i160, i182, env, static) :|: 1 <= i182 && 1 <= i160 && 1 <= i159
main_JMP_449(i158, i159, i183, i175, env, static) -{1,1}> main_Load_453(i158, i159, i183, i175, env, static) :|: 1 <= i183 && 1 <= i159 && 1 <= i175
main_Load_450(i158, i159, i160, i182, env, static) -{0,0}> main_Load_421(i158, i159, i160, i182, env, static) :|: 1 <= i182 && 1 <= i160 && 1 <= i159
main_Load_453(i158, i159, i183, i175, env, static) -{0,0}> main_Load_421(i158, i159, i183, i175, env, static) :|: 1 <= i183 && 1 <= i159 && 1 <= i175

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

obtained
main_Load_1(i1, i3, env, static) -{16,16}> main_LE_52(i1, i3, env, static'1) :|: 0 >= 0 && static'1 <= static''' + 1 && 0 <= 2 && 0 <= static''' && static''' <= static + 2 && 0 < 1 && 0 <= 1 && 0 <= static && 0 <= static'1 && 0 < 2
by chaining
main_Load_1(i1, i3, env, static) -{0,0}> main_Load_4(i1, i3, env, static) :|: 0 >= 0
main_Load_4(i1, i3, env, static) -{0,0}> langle_clinit_rangle_ConstantStackPush_6(i1, i3, env, static) :|: 0 >= 0
langle_clinit_rangle_ConstantStackPush_6(i1, i3, env, static) -{1,1}> langle_clinit_rangle_ArrayCreate_12(iconst_0, i1, i3, env, static) :|: iconst_0 = 0
langle_clinit_rangle_ArrayCreate_12(iconst_0, i1, i3, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_14(a2, i1, i3, iconst_0, env, static) :|: a2 = 2 && iconst_0 = 0 && 0 < a2
langle_clinit_rangle_FieldAccess_14(a2, i1, i3, iconst_0, env, static) -{1,1}> langle_clinit_rangle_New_16(i1, i3, env, static') :|: 0 <= a2 && iconst_0 = 0 && static' <= static + a2 && 0 <= static && 0 < a2
langle_clinit_rangle_New_16(i1, i3, env, static) -{0,0}> langle_clinit_rangle_New_18(i1, i3, env, static) :|: 0 >= 0
langle_clinit_rangle_New_18(i1, i3, env, static) -{0,0}> langle_clinit_rangle_New_19(i1, i3, env, static) :|: 0 <= static
langle_clinit_rangle_New_19(i1, i3, env, static) -{1,1}> langle_clinit_rangle_Duplicate_20(o2, i1, i3, env, static) :|: 0 < o2 && o2 = 1
langle_clinit_rangle_Duplicate_20(o2, i1, i3, env, static) -{1,1}> langle_clinit_rangle_ConstantStackPush_22(o2, i1, i3, env, static) :|: 0 < o2
langle_clinit_rangle_ConstantStackPush_22(o2, i1, i3, env, static) -{1,1}> langle_clinit_rangle_InvokeMethod_23(o2, NULL, i1, i3, env, static) :|: NULL = 0 && 0 < o2
langle_clinit_rangle_InvokeMethod_23(o2, NULL, i1, i3, env, static) -{1,1}> langle_init_rangle_Load_25(o2, i1, i3, env, static) :|: NULL = 0 && 0 < o2
langle_init_rangle_Load_25(o2, i1, i3, env, static) -{1,1}> langle_init_rangle_InvokeMethod_27(o2, i1, i3, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_27(o2, i1, i3, env, static) -{1,1}> langle_init_rangle_Load_29(o2, i1, i3, env, static) :|: 0 < o2
langle_init_rangle_Load_29(o2, i1, i3, env, static) -{1,1}> langle_init_rangle_InvokeMethod_31(o2, i1, i3, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_31(o2, i1, i3, env, static) -{1,1}> langle_init_rangle_Return_34(o2, i1, i3, env, static) :|: 0 < o2
langle_init_rangle_Return_34(o2, i1, i3, env, static) -{1,1}> langle_init_rangle_Return_36(o2, i1, i3, env, static) :|: 0 < o2
langle_init_rangle_Return_36(o2, i1, i3, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_39(o2, i1, i3, env, static) :|: 0 < o2
langle_clinit_rangle_FieldAccess_39(o2, i1, i3, env, static) -{1,1}> langle_clinit_rangle_Return_40(i1, i3, env, static') :|: 0 < o2 && 0 <= o2 && 0 <= static && static' <= static + o2
langle_clinit_rangle_Return_40(i1, i3, env, static) -{1,1}> main_Load_41(i1, i3, env, static) :|: 0 >= 0
main_Load_41(i1, i3, env, static) -{0,0}> main_Load_42(i1, i3, env, static) :|: 0 >= 0
main_Load_42(i1, i3, env, static) -{0,0}> main_Load_44(i1, i3, env, static) :|: 0 <= static
main_Load_44(i1, i3, env, static) -{0,0}> main_Load_46(i1, i3, env, static) :|: 0 >= 0
main_Load_46(i1, i3, env, static) -{0,0}> main_Load_48(i1, i3, env, static) :|: 0 >= 0
main_Load_48(i1, i3, env, static) -{1,1}> main_LE_52(i1, i3, env, static) :|: 0 >= 0

obtained
main_LE_52(i12, i3, env, static) -{2,2}> main_LE_62(i12, i3, env, static) :|: 1 <= i12 && 0 < i12
by chaining
main_LE_52(i12, i3, env, static) -{0,0}> main_LE_54(i12, i3, env, static) :|: 1 <= i12
main_LE_54(i12, i3, env, static) -{1,1}> main_Load_58(i12, i3, env, static) :|: 0 < i12 && 1 <= i12
main_Load_58(i12, i3, env, static) -{1,1}> main_LE_62(i12, i3, env, static) :|: 1 <= i12

obtained
main_LE_62(i12, i20, env, static) -{1,1}> main_Load_421(i12, i20, i12, i20, env, static) :|: 0 < i20 && 1 <= i20 && 1 <= i12
by chaining
main_LE_62(i12, i20, env, static) -{0,0}> main_LE_64(i12, i20, env, static) :|: 1 <= i20 && 1 <= i12
main_LE_64(i12, i20, env, static) -{1,1}> main_Load_73(i12, i20, env, static) :|: 0 < i20 && 1 <= i20 && 1 <= i12
main_Load_73(i12, i20, env, static) -{0,0}> main_Load_421(i12, i20, i12, i20, env, static) :|: 1 <= i20 && 1 <= i12

obtained
main_Load_421(i158, i159, i160, i175, env, static) -{2,2}> main_EQ_426(i158, i159, i160, i175, env, static) :|: 1 <= i175 && 1 <= i160 && 1 <= i159
by chaining
main_Load_421(i158, i159, i160, i175, env, static) -{1,1}> main_Load_424(i158, i159, i160, i175, env, static) :|: 1 <= i160 && 1 <= i159 && 1 <= i175
main_Load_424(i158, i159, i160, i175, env, static) -{1,1}> main_EQ_426(i158, i159, i160, i175, env, static) :|: 1 <= i160 && 1 <= i159 && 1 <= i175

obtained
main_EQ_426(i158, i159, i160, i175, env, static) -{3,3}> main_LE_437(i158, i159, i160, i175, env, static) :|: !(i160 = i175) && 1 <= i175 && 1 <= i160 && 1 <= i159
by chaining
main_EQ_426(i158, i159, i160, i175, env, static) -{0,0}> main_EQ_428(i158, i159, i160, i175, env, static) :|: 1 <= i160 && 1 <= i159 && !(i160 = i175) && 1 <= i175
main_EQ_428(i158, i159, i160, i175, env, static) -{1,1}> main_Load_432(i158, i159, i160, i175, env, static) :|: 1 <= i160 && 1 <= i159 && !(i160 = i175) && 1 <= i175
main_Load_432(i158, i159, i160, i175, env, static) -{1,1}> main_Load_434(i158, i159, i160, i175, env, static) :|: 1 <= i160 && 1 <= i159 && 1 <= i175
main_Load_434(i158, i159, i160, i175, env, static) -{1,1}> main_LE_437(i158, i159, i160, i175, env, static) :|: 1 <= i160 && 1 <= i159 && 1 <= i175

obtained
main_LE_437(i158, i159, i160, i175, env, static) -{6,6}> main_Load_421(i158, i159, i183', i175, env, static) :|: i160 - i175 = i183' && 1 <= i175 && i175 < i160 && 1 <= i183' && 1 <= i159 && 2 <= i160 && 1 <= i160
by chaining
main_LE_437(i158, i159, i160, i175, env, static) -{0,0}> main_LE_439(i158, i159, i160, i175, env, static) :|: 1 <= i160 && 1 <= i159 && i175 < i160 && 1 <= i175
main_LE_439(i158, i159, i160, i175, env, static) -{1,1}> main_Load_441(i158, i159, i160, i175, env, static) :|: 1 <= i160 && 1 <= i159 && i175 < i160 && 2 <= i160 && 1 <= i175
main_Load_441(i158, i159, i160, i175, env, static) -{1,1}> main_Load_443(i158, i159, i160, i175, env, static) :|: 1 <= i159 && 2 <= i160 && 1 <= i175
main_Load_443(i158, i159, i160, i175, env, static) -{1,1}> main_IntArithmetic_445(i158, i159, i160, i175, env, static) :|: 1 <= i159 && 2 <= i160 && 1 <= i175
main_IntArithmetic_445(i158, i159, i160, i175, env, static) -{1,1}> main_Store_447(i158, i159, i183, i175, env, static) :|: i160 - i175 = i183 && 1 <= i183 && 1 <= i159 && 2 <= i160 && 1 <= i175
main_Store_447(i158, i159, i183, i175, env, static) -{1,1}> main_JMP_449(i158, i159, i183, i175, env, static) :|: 1 <= i183 && 1 <= i159 && 1 <= i175
main_JMP_449(i158, i159, i183, i175, env, static) -{1,1}> main_Load_453(i158, i159, i183, i175, env, static) :|: 1 <= i183 && 1 <= i159 && 1 <= i175
main_Load_453(i158, i159, i183, i175, env, static) -{0,0}> main_Load_421(i158, i159, i183, i175, env, static) :|: 1 <= i183 && 1 <= i159 && 1 <= i175

obtained
main_LE_437(i158, i159, i160, i175, env, static) -{6,6}> main_Load_421(i158, i159, i160, i182', env, static) :|: 1 <= i175 && 1 <= i159 && i160 <= i175 && 1 <= i182' && 1 <= i160 && 2 <= i175 && i160 < i175 && i175 - i160 = i182'
by chaining
main_LE_437(i158, i159, i160, i175, env, static) -{0,0}> main_LE_438(i158, i159, i160, i175, env, static) :|: i160 <= i175 && 1 <= i160 && 1 <= i159 && 1 <= i175
main_LE_438(i158, i159, i160, i175, env, static) -{1,1}> main_Load_440(i158, i159, i160, i175, env, static) :|: 1 <= i160 && 1 <= i159 && i160 < i175 && 2 <= i175 && 1 <= i175
main_Load_440(i158, i159, i160, i175, env, static) -{1,1}> main_Load_442(i158, i159, i175, i160, env, static) :|: 1 <= i160 && 1 <= i159 && 2 <= i175
main_Load_442(i158, i159, i175, i160, env, static) -{1,1}> main_IntArithmetic_444(i158, i159, i175, i160, env, static) :|: 1 <= i160 && 1 <= i159 && 2 <= i175
main_IntArithmetic_444(i158, i159, i175, i160, env, static) -{1,1}> main_Store_446(i158, i159, i182, i160, env, static) :|: 1 <= i182 && 1 <= i160 && 1 <= i159 && 2 <= i175 && i175 - i160 = i182
main_Store_446(i158, i159, i182, i160, env, static) -{1,1}> main_JMP_448(i158, i159, i160, i182, env, static) :|: 1 <= i182 && 1 <= i160 && 1 <= i159
main_JMP_448(i158, i159, i160, i182, env, static) -{1,1}> main_Load_450(i158, i159, i160, i182, env, static) :|: 1 <= i182 && 1 <= i160 && 1 <= i159
main_Load_450(i158, i159, i160, i182, env, static) -{0,0}> main_Load_421(i158, i159, i160, i182, env, static) :|: 1 <= i182 && 1 <= i160 && 1 <= i159

(8) Obligation:

IntTrs with 10 rules
Start term: main_Load_1(#0, #1, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_Load_1(i1, i3, env, static) -{16,16}> main_LE_52(i1, i3, env, static'1) :|: 0 >= 0 && static'1 <= static''' + 1 && 0 <= 2 && 0 <= static''' && static''' <= static + 2 && 0 < 1 && 0 <= 1 && 0 <= static && 0 <= static'1 && 0 < 2
main_LE_52(i11, i3, env, static) -{0,0}> main_LE_53(i11, i3, env, static) :|: i11 <= 0
main_LE_52(i12, i3, env, static) -{2,2}> main_LE_62(i12, i3, env, static) :|: 1 <= i12 && 0 < i12
main_LE_62(i12, i19, env, static) -{0,0}> main_LE_63(i12, i19, env, static) :|: i19 <= 0 && 1 <= i12
main_LE_62(i12, i20, env, static) -{1,1}> main_Load_421(i12, i20, i12, i20, env, static) :|: 0 < i20 && 1 <= i20 && 1 <= i12
main_Load_421(i158, i159, i160, i175, env, static) -{2,2}> main_EQ_426(i158, i159, i160, i175, env, static) :|: 1 <= i175 && 1 <= i160 && 1 <= i159
main_EQ_426(i158, i159, i160, i175, env, static) -{0,0}> main_EQ_427(i158, i159, i175, env, static) :|: i160 = i175 && 1 <= i160 && 1 <= i159 && 1 <= i175
main_EQ_426(i158, i159, i160, i175, env, static) -{3,3}> main_LE_437(i158, i159, i160, i175, env, static) :|: !(i160 = i175) && 1 <= i175 && 1 <= i160 && 1 <= i159
main_LE_437(i158, i159, i160, i175, env, static) -{6,6}> main_Load_421(i158, i159, i183', i175, env, static) :|: i160 - i175 = i183' && 1 <= i175 && i175 < i160 && 1 <= i183' && 1 <= i159 && 2 <= i160 && 1 <= i160
main_LE_437(i158, i159, i160, i175, env, static) -{6,6}> main_Load_421(i158, i159, i160, i182', env, static) :|: 1 <= i175 && 1 <= i159 && i160 <= i175 && 1 <= i182' && 1 <= i160 && 2 <= i175 && i160 < i175 && i175 - i160 = i182'

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

Removed div and mod.

main_EQ_426(i158, i159, i160, i175, env, static) -{3,3}> main_LE_437(i158, i159, i160, i175, env, static) :|: !(i160 = i175) && 1 <= i175 && 1 <= i160 && 1 <= i159
was transformed to
main_EQ_426(i158, i159, i160, i175, env, static) -{3,3}> main_LE_437(i158, i159, i160, i175, env, static) :|: i160 < i175 && 1 <= i175 && 1 <= i160 && 1 <= i159
main_EQ_426(i158, i159, i160, i175, env, static) -{3,3}> main_LE_437(i158, i159, i160, i175, env, static) :|: i160 > i175 && 1 <= i175 && 1 <= i160 && 1 <= i159

(10) Obligation:

IntTrs with 11 rules
Start term: main_Load_1(#0, #1, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_LE_437(i158, i159, i160, i175, env, static) -{6,6}> main_Load_421(i158, i159, i160, i182', env, static) :|: 1 <= i175 && 1 <= i159 && i160 <= i175 && 1 <= i182' && 1 <= i160 && 2 <= i175 && i160 < i175 && i175 - i160 = i182'
main_Load_421(i158, i159, i160, i175, env, static) -{2,2}> main_EQ_426(i158, i159, i160, i175, env, static) :|: 1 <= i175 && 1 <= i160 && 1 <= i159
main_LE_62(i12, i20, env, static) -{1,1}> main_Load_421(i12, i20, i12, i20, env, static) :|: 0 < i20 && 1 <= i20 && 1 <= i12
main_EQ_426(i158, i159, i160, i175, env, static) -{0,0}> main_EQ_427(i158, i159, i175, env, static) :|: i160 = i175 && 1 <= i160 && 1 <= i159 && 1 <= i175
main_LE_52(i11, i3, env, static) -{0,0}> main_LE_53(i11, i3, env, static) :|: i11 <= 0
main_Load_1(i1, i3, env, static) -{16,16}> main_LE_52(i1, i3, env, static'1) :|: 0 >= 0 && static'1 <= static''' + 1 && 0 <= 2 && 0 <= static''' && static''' <= static + 2 && 0 < 1 && 0 <= 1 && 0 <= static && 0 <= static'1 && 0 < 2
main_EQ_426(i158, i159, i160, i175, env, static) -{3,3}> main_LE_437(i158, i159, i160, i175, env, static) :|: i160 < i175 && 1 <= i175 && 1 <= i160 && 1 <= i159
main_LE_62(i12, i19, env, static) -{0,0}> main_LE_63(i12, i19, env, static) :|: i19 <= 0 && 1 <= i12
main_EQ_426(i158, i159, i160, i175, env, static) -{3,3}> main_LE_437(i158, i159, i160, i175, env, static) :|: i160 > i175 && 1 <= i175 && 1 <= i160 && 1 <= i159
main_LE_437(i158, i159, i160, i175, env, static) -{6,6}> main_Load_421(i158, i159, i183', i175, env, static) :|: i160 - i175 = i183' && 1 <= i175 && i175 < i160 && 1 <= i183' && 1 <= i159 && 2 <= i160 && 1 <= i160
main_LE_52(i12, i3, env, static) -{2,2}> main_LE_62(i12, i3, env, static) :|: 1 <= i12 && 0 < i12

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

Moved arithmethic from constraints to rhss.

main_LE_437(i158, i159, i160, i175, env, static) -{6,6}> main_Load_421(i158, i159, i160, i182', env, static) :|: 1 <= i175 && 1 <= i159 && i160 <= i175 && 1 <= i182' && 1 <= i160 && 2 <= i175 && i160 < i175 && i175 - i160 = i182'
was transformed to
main_LE_437(i158, i159, i160, i175, env, static) -{6,6}> main_Load_421(i158, i159, i160, i175 - i160, env, static) :|: 1 <= i175 && 1 <= i159 && i160 <= i175 && 1 <= i182' && 1 <= i160 && 2 <= i175 && i160 < i175 && i175 - i160 = i182'

main_LE_437(i158, i159, i160, i175, env, static) -{6,6}> main_Load_421(i158, i159, i183', i175, env, static) :|: i160 - i175 = i183' && 1 <= i175 && i175 < i160 && 1 <= i183' && 1 <= i159 && 2 <= i160 && 1 <= i160
was transformed to
main_LE_437(i158, i159, i160, i175, env, static) -{6,6}> main_Load_421(i158, i159, i160 - i175, i175, env, static) :|: i160 - i175 = i183' && 1 <= i175 && i175 < i160 && 1 <= i183' && 1 <= i159 && 2 <= i160 && 1 <= i160

(12) Obligation:

IntTrs with 11 rules
Start term: main_Load_1(#0, #1, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_LE_62(i12, i20, env, static) -{1,1}> main_Load_421(i12, i20, i12, i20, env, static) :|: 0 < i20 && 1 <= i20 && 1 <= i12
main_Load_421(i158, i159, i160, i175, env, static) -{2,2}> main_EQ_426(i158, i159, i160, i175, env, static) :|: 1 <= i175 && 1 <= i160 && 1 <= i159
main_LE_437(i158, i159, i160, i175, env, static) -{6,6}> main_Load_421(i158, i159, i160, i175 - i160, env, static) :|: 1 <= i175 && 1 <= i159 && i160 <= i175 && 1 <= i182' && 1 <= i160 && 2 <= i175 && i160 < i175 && i175 - i160 = i182'
main_EQ_426(i158, i159, i160, i175, env, static) -{0,0}> main_EQ_427(i158, i159, i175, env, static) :|: i160 = i175 && 1 <= i160 && 1 <= i159 && 1 <= i175
main_EQ_426(i158, i159, i160, i175, env, static) -{3,3}> main_LE_437(i158, i159, i160, i175, env, static) :|: i160 < i175 && 1 <= i175 && 1 <= i160 && 1 <= i159
main_Load_1(i1, i3, env, static) -{16,16}> main_LE_52(i1, i3, env, static'1) :|: 0 >= 0 && static'1 <= static''' + 1 && 0 <= 2 && 0 <= static''' && static''' <= static + 2 && 0 < 1 && 0 <= 1 && 0 <= static && 0 <= static'1 && 0 < 2
main_LE_52(i11, i3, env, static) -{0,0}> main_LE_53(i11, i3, env, static) :|: i11 <= 0
main_LE_62(i12, i19, env, static) -{0,0}> main_LE_63(i12, i19, env, static) :|: i19 <= 0 && 1 <= i12
main_EQ_426(i158, i159, i160, i175, env, static) -{3,3}> main_LE_437(i158, i159, i160, i175, env, static) :|: i160 > i175 && 1 <= i175 && 1 <= i160 && 1 <= i159
main_LE_52(i12, i3, env, static) -{2,2}> main_LE_62(i12, i3, env, static) :|: 1 <= i12 && 0 < i12
main_LE_437(i158, i159, i160, i175, env, static) -{6,6}> main_Load_421(i158, i159, i160 - i175, i175, env, static) :|: i160 - i175 = i183' && 1 <= i175 && i175 < i160 && 1 <= i183' && 1 <= i159 && 2 <= i160 && 1 <= i160

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

Simplified expressions.

main_LE_437(i158, i159, i160, i175, env, static) -{6,6}> main_Load_421(i158, i159, i160 - i175, i175, env, static) :|: i160 - i175 = i183' && 1 <= i175 && i175 < i160 && 1 <= i183' && 1 <= i159 && 2 <= i160 && 1 <= i160
was transformed to
main_LE_437(i158, i159, i160, i175, env, static) -{6,6}> main_Load_421(i158, i159, i160 + -1 * i175, i175, env, static) :|: i160 + -1 * i175 = i183' && 1 <= i175 && i175 < i160 && 1 <= i183' && 1 <= i159 && 2 <= i160 && 1 <= i160

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

main_EQ_426(i158, i159, i160, i175, env, static) -{3,3}> main_LE_437(i158, i159, i160, i175, env, static) :|: i160 > i175 && 1 <= i175 && 1 <= i160 && 1 <= i159
was transformed to
main_EQ_426(i158, i159, i160, i175, env, static) -{3,3}> main_LE_437(i158, i159, i160, i175, env, static) :|: i175 < i160 && 1 <= i175 && 1 <= i160 && 1 <= i159

main_LE_437(i158, i159, i160, i175, env, static) -{6,6}> main_Load_421(i158, i159, i160, i175 - i160, env, static) :|: 1 <= i175 && 1 <= i159 && i160 <= i175 && 1 <= i182' && 1 <= i160 && 2 <= i175 && i160 < i175 && i175 - i160 = i182'
was transformed to
main_LE_437(i158, i159, i160, i175, env, static) -{6,6}> main_Load_421(i158, i159, i160, i175 + -1 * i160, env, static) :|: 1 <= i175 && 1 <= i159 && 1 <= i182' && 1 <= i160 && 2 <= i175 && i160 < i175 && i175 + -1 * i160 = i182'

(14) Obligation:

IntTrs with 11 rules
Start term: main_Load_1(#0, #1, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_Load_421(i158, i159, i160, i175, env, static) -{2,2}> main_EQ_426(i158, i159, i160, i175, env, static) :|: 1 <= i175 && 1 <= i160 && 1 <= i159
main_LE_62(i12, i20, env, static) -{1,1}> main_Load_421(i12, i20, i12, i20, env, static) :|: 0 < i20 && 1 <= i20 && 1 <= i12
main_EQ_426(i158, i159, i160, i175, env, static) -{0,0}> main_EQ_427(i158, i159, i175, env, static) :|: i160 = i175 && 1 <= i160 && 1 <= i159 && 1 <= i175
main_LE_437(i158, i159, i160, i175, env, static) -{6,6}> main_Load_421(i158, i159, i160 + -1 * i175, i175, env, static) :|: i160 + -1 * i175 = i183' && 1 <= i175 && i175 < i160 && 1 <= i183' && 1 <= i159 && 2 <= i160 && 1 <= i160
main_LE_52(i11, i3, env, static) -{0,0}> main_LE_53(i11, i3, env, static) :|: i11 <= 0
main_EQ_426(i158, i159, i160, i175, env, static) -{3,3}> main_LE_437(i158, i159, i160, i175, env, static) :|: i160 < i175 && 1 <= i175 && 1 <= i160 && 1 <= i159
main_EQ_426(i158, i159, i160, i175, env, static) -{3,3}> main_LE_437(i158, i159, i160, i175, env, static) :|: i175 < i160 && 1 <= i175 && 1 <= i160 && 1 <= i159
main_LE_62(i12, i19, env, static) -{0,0}> main_LE_63(i12, i19, env, static) :|: i19 <= 0 && 1 <= i12
main_LE_437(i158, i159, i160, i175, env, static) -{6,6}> main_Load_421(i158, i159, i160, i175 + -1 * i160, env, static) :|: 1 <= i175 && 1 <= i159 && 1 <= i182' && 1 <= i160 && 2 <= i175 && i160 < i175 && i175 + -1 * i160 = i182'
main_Load_1(i1, i3, env, static) -{16,16}> main_LE_52(i1, i3, env, static'1) :|: static'1 <= static''' + 1 && 0 <= static''' && static''' <= static + 2 && 0 <= static && 0 <= static'1
main_LE_52(i12, i3, env, static) -{2,2}> main_LE_62(i12, i3, env, static) :|: 1 <= i12 && 0 < i12

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

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

(16) Obligation:

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

(18) Obligation:

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

Removed div and mod.

(20) Obligation:

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

Moved arithmethic from constraints to rhss.

(22) Obligation:

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

Simplified expressions.

(24) Obligation:

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

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

(26) Obligation:

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

Used field analysis yielded the following read fields:

Considered paths: all paths from start

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

Transformed 52 jbc graph edges to a weighted ITS with 52 rules.
Used simplified encoding of division and modulo.
Filtered conditions with variables that do not depend on the variables on the lhs or rhs without taking transitive dependencies into account.
Filtered fields of type java.lang.Object.
Did no encode lower bounds for putfield and astore.

(28) Obligation:

IntTrs with 52 rules
Start term: main_Load_1(#0, #1, env, static)
Considered paths: all paths from start
Rules:
main_Load_1(i1, i3, env, static) -{0,0}> main_Load_4(i1, i3, env, static) :|: 0 >= 0
main_Load_4(i1, i3, env, static) -{0,0}> langle_clinit_rangle_ConstantStackPush_6(i1, i3, env, static) :|: 0 >= 0
langle_clinit_rangle_ConstantStackPush_6(i1, i3, env, static) -{1,1}> langle_clinit_rangle_ArrayCreate_12(iconst_0, i1, i3, env, static) :|: iconst_0 = 0
langle_clinit_rangle_ArrayCreate_12(iconst_0, i1, i3, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_14(a2, i1, i3, iconst_0, env, static) :|: a2 = 2 && iconst_0 = 0 && 0 < a2
langle_clinit_rangle_FieldAccess_14(a2, i1, i3, iconst_0, env, static) -{1,1}> langle_clinit_rangle_New_16(i1, i3, env, static') :|: 0 <= a2 && iconst_0 = 0 && static' <= static + a2 && 0 <= static && 0 < a2
langle_clinit_rangle_New_16(i1, i3, env, static) -{0,0}> langle_clinit_rangle_New_18(i1, i3, env, static) :|: 0 >= 0
langle_clinit_rangle_New_18(i1, i3, env, static) -{0,0}> langle_clinit_rangle_New_19(i1, i3, env, static) :|: 0 <= static
langle_clinit_rangle_New_19(i1, i3, env, static) -{1,1}> langle_clinit_rangle_Duplicate_20(o2, i1, i3, env, static) :|: 0 < o2 && o2 = 1
langle_clinit_rangle_Duplicate_20(o2, i1, i3, env, static) -{1,1}> langle_clinit_rangle_ConstantStackPush_22(o2, i1, i3, env, static) :|: 0 < o2
langle_clinit_rangle_ConstantStackPush_22(o2, i1, i3, env, static) -{1,1}> langle_clinit_rangle_InvokeMethod_23(o2, NULL, i1, i3, env, static) :|: NULL = 0 && 0 < o2
langle_clinit_rangle_InvokeMethod_23(o2, NULL, i1, i3, env, static) -{1,1}> langle_init_rangle_Load_25(o2, i1, i3, env, static) :|: NULL = 0 && 0 < o2
langle_init_rangle_Load_25(o2, i1, i3, env, static) -{1,1}> langle_init_rangle_InvokeMethod_27(o2, i1, i3, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_27(o2, i1, i3, env, static) -{1,1}> langle_init_rangle_Load_29(o2, i1, i3, env, static) :|: 0 < o2
langle_init_rangle_Load_29(o2, i1, i3, env, static) -{1,1}> langle_init_rangle_InvokeMethod_31(o2, i1, i3, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_31(o2, i1, i3, env, static) -{1,1}> langle_init_rangle_Return_34(o2, i1, i3, env, static) :|: 0 < o2
langle_init_rangle_Return_34(o2, i1, i3, env, static) -{1,1}> langle_init_rangle_Return_36(o2, i1, i3, env, static) :|: 0 < o2
langle_init_rangle_Return_36(o2, i1, i3, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_39(o2, i1, i3, env, static) :|: 0 < o2
langle_clinit_rangle_FieldAccess_39(o2, i1, i3, env, static) -{1,1}> langle_clinit_rangle_Return_40(i1, i3, env, static') :|: 0 < o2 && 0 <= o2 && 0 <= static && static' <= static + o2
langle_clinit_rangle_Return_40(i1, i3, env, static) -{1,1}> main_Load_41(i1, i3, env, static) :|: 0 >= 0
main_Load_41(i1, i3, env, static) -{0,0}> main_Load_42(i1, i3, env, static) :|: 0 >= 0
main_Load_42(i1, i3, env, static) -{0,0}> main_Load_44(i1, i3, env, static) :|: 0 <= static
main_Load_44(i1, i3, env, static) -{0,0}> main_Load_46(i1, i3, env, static) :|: 0 >= 0
main_Load_46(i1, i3, env, static) -{0,0}> main_Load_48(i1, i3, env, static) :|: 0 >= 0
main_Load_48(i1, i3, env, static) -{1,1}> main_LE_52(i1, i3, env, static) :|: 0 >= 0
main_LE_52(i12, i3, env, static) -{0,0}> main_LE_54(i12, i3, env, static) :|: 1 <= i12
main_LE_54(i12, i3, env, static) -{1,1}> main_Load_58(i12, i3, env, static) :|: 0 < i12 && 1 <= i12
main_Load_58(i12, i3, env, static) -{1,1}> main_LE_62(i12, i3, env, static) :|: 1 <= i12
main_LE_62(i12, i20, env, static) -{0,0}> main_LE_64(i12, i20, env, static) :|: 1 <= i20 && 1 <= i12
main_LE_64(i12, i20, env, static) -{1,1}> main_Load_73(i12, i20, env, static) :|: 0 < i20 && 1 <= i20 && 1 <= i12
main_Load_73(i12, i20, env, static) -{0,0}> main_Load_421(i12, i20, i12, i20, env, static) :|: 1 <= i20 && 1 <= i12
main_Load_421(i158, i159, i160, i175, env, static) -{1,1}> main_Load_424(i158, i159, i160, i175, env, static) :|: 1 <= i160 && 1 <= i159 && 1 <= i175
main_Load_424(i158, i159, i160, i175, env, static) -{1,1}> main_EQ_426(i158, i159, i160, i175, env, static) :|: 1 <= i160 && 1 <= i159 && 1 <= i175
main_EQ_426(i158, i159, i160, i175, env, static) -{0,0}> main_EQ_428(i158, i159, i160, i175, env, static) :|: 1 <= i160 && 1 <= i159 && !(i160 = i175) && 1 <= i175
main_EQ_428(i158, i159, i160, i175, env, static) -{1,1}> main_Load_432(i158, i159, i160, i175, env, static) :|: 1 <= i160 && 1 <= i159 && !(i160 = i175) && 1 <= i175
main_Load_432(i158, i159, i160, i175, env, static) -{1,1}> main_Load_434(i158, i159, i160, i175, env, static) :|: 1 <= i160 && 1 <= i159 && 1 <= i175
main_Load_434(i158, i159, i160, i175, env, static) -{1,1}> main_LE_437(i158, i159, i160, i175, env, static) :|: 1 <= i160 && 1 <= i159 && 1 <= i175
main_LE_437(i158, i159, i160, i175, env, static) -{0,0}> main_LE_438(i158, i159, i160, i175, env, static) :|: i160 <= i175 && 1 <= i160 && 1 <= i159 && 1 <= i175
main_LE_437(i158, i159, i160, i175, env, static) -{0,0}> main_LE_439(i158, i159, i160, i175, env, static) :|: 1 <= i160 && 1 <= i159 && i175 < i160 && 1 <= i175
main_LE_438(i158, i159, i160, i175, env, static) -{1,1}> main_Load_440(i158, i159, i160, i175, env, static) :|: 1 <= i160 && 1 <= i159 && i160 < i175 && 2 <= i175 && 1 <= i175
main_LE_439(i158, i159, i160, i175, env, static) -{1,1}> main_Load_441(i158, i159, i160, i175, env, static) :|: 1 <= i160 && 1 <= i159 && i175 < i160 && 2 <= i160 && 1 <= i175
main_Load_440(i158, i159, i160, i175, env, static) -{1,1}> main_Load_442(i158, i159, i175, i160, env, static) :|: 1 <= i160 && 1 <= i159 && 2 <= i175
main_Load_441(i158, i159, i160, i175, env, static) -{1,1}> main_Load_443(i158, i159, i160, i175, env, static) :|: 1 <= i159 && 2 <= i160 && 1 <= i175
main_Load_442(i158, i159, i175, i160, env, static) -{1,1}> main_IntArithmetic_444(i158, i159, i175, i160, env, static) :|: 1 <= i160 && 1 <= i159 && 2 <= i175
main_Load_443(i158, i159, i160, i175, env, static) -{1,1}> main_IntArithmetic_445(i158, i159, i160, i175, env, static) :|: 1 <= i159 && 2 <= i160 && 1 <= i175
main_IntArithmetic_444(i158, i159, i175, i160, env, static) -{1,1}> main_Store_446(i158, i159, i182, i160, env, static) :|: 1 <= i182 && 1 <= i160 && 1 <= i159 && 2 <= i175 && i175 - i160 = i182
main_IntArithmetic_445(i158, i159, i160, i175, env, static) -{1,1}> main_Store_447(i158, i159, i183, i175, env, static) :|: i160 - i175 = i183 && 1 <= i183 && 1 <= i159 && 2 <= i160 && 1 <= i175
main_Store_446(i158, i159, i182, i160, env, static) -{1,1}> main_JMP_448(i158, i159, i160, i182, env, static) :|: 1 <= i182 && 1 <= i160 && 1 <= i159
main_Store_447(i158, i159, i183, i175, env, static) -{1,1}> main_JMP_449(i158, i159, i183, i175, env, static) :|: 1 <= i183 && 1 <= i159 && 1 <= i175
main_JMP_448(i158, i159, i160, i182, env, static) -{1,1}> main_Load_450(i158, i159, i160, i182, env, static) :|: 1 <= i182 && 1 <= i160 && 1 <= i159
main_JMP_449(i158, i159, i183, i175, env, static) -{1,1}> main_Load_453(i158, i159, i183, i175, env, static) :|: 1 <= i183 && 1 <= i159 && 1 <= i175
main_Load_450(i158, i159, i160, i182, env, static) -{0,0}> main_Load_421(i158, i159, i160, i182, env, static) :|: 1 <= i182 && 1 <= i160 && 1 <= i159
main_Load_453(i158, i159, i183, i175, env, static) -{0,0}> main_Load_421(i158, i159, i183, i175, env, static) :|: 1 <= i183 && 1 <= i159 && 1 <= i175

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

obtained
main_Load_1(i1, i3, env, static) -{19,19}> main_Load_421(i1, i3, i1, i3, env, static'1) :|: 0 < i1 && 1 <= i3 && 1 <= i1 && static'1 <= static''' + 1 && 0 >= 0 && 0 <= 2 && 0 <= static''' && static''' <= static + 2 && 0 < 1 && 0 <= 1 && 0 <= static && 0 < i3 && 0 <= static'1 && 0 < 2
by chaining
main_Load_1(i1, i3, env, static) -{0,0}> main_Load_4(i1, i3, env, static) :|: 0 >= 0
main_Load_4(i1, i3, env, static) -{0,0}> langle_clinit_rangle_ConstantStackPush_6(i1, i3, env, static) :|: 0 >= 0
langle_clinit_rangle_ConstantStackPush_6(i1, i3, env, static) -{1,1}> langle_clinit_rangle_ArrayCreate_12(iconst_0, i1, i3, env, static) :|: iconst_0 = 0
langle_clinit_rangle_ArrayCreate_12(iconst_0, i1, i3, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_14(a2, i1, i3, iconst_0, env, static) :|: a2 = 2 && iconst_0 = 0 && 0 < a2
langle_clinit_rangle_FieldAccess_14(a2, i1, i3, iconst_0, env, static) -{1,1}> langle_clinit_rangle_New_16(i1, i3, env, static') :|: 0 <= a2 && iconst_0 = 0 && static' <= static + a2 && 0 <= static && 0 < a2
langle_clinit_rangle_New_16(i1, i3, env, static) -{0,0}> langle_clinit_rangle_New_18(i1, i3, env, static) :|: 0 >= 0
langle_clinit_rangle_New_18(i1, i3, env, static) -{0,0}> langle_clinit_rangle_New_19(i1, i3, env, static) :|: 0 <= static
langle_clinit_rangle_New_19(i1, i3, env, static) -{1,1}> langle_clinit_rangle_Duplicate_20(o2, i1, i3, env, static) :|: 0 < o2 && o2 = 1
langle_clinit_rangle_Duplicate_20(o2, i1, i3, env, static) -{1,1}> langle_clinit_rangle_ConstantStackPush_22(o2, i1, i3, env, static) :|: 0 < o2
langle_clinit_rangle_ConstantStackPush_22(o2, i1, i3, env, static) -{1,1}> langle_clinit_rangle_InvokeMethod_23(o2, NULL, i1, i3, env, static) :|: NULL = 0 && 0 < o2
langle_clinit_rangle_InvokeMethod_23(o2, NULL, i1, i3, env, static) -{1,1}> langle_init_rangle_Load_25(o2, i1, i3, env, static) :|: NULL = 0 && 0 < o2
langle_init_rangle_Load_25(o2, i1, i3, env, static) -{1,1}> langle_init_rangle_InvokeMethod_27(o2, i1, i3, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_27(o2, i1, i3, env, static) -{1,1}> langle_init_rangle_Load_29(o2, i1, i3, env, static) :|: 0 < o2
langle_init_rangle_Load_29(o2, i1, i3, env, static) -{1,1}> langle_init_rangle_InvokeMethod_31(o2, i1, i3, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_31(o2, i1, i3, env, static) -{1,1}> langle_init_rangle_Return_34(o2, i1, i3, env, static) :|: 0 < o2
langle_init_rangle_Return_34(o2, i1, i3, env, static) -{1,1}> langle_init_rangle_Return_36(o2, i1, i3, env, static) :|: 0 < o2
langle_init_rangle_Return_36(o2, i1, i3, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_39(o2, i1, i3, env, static) :|: 0 < o2
langle_clinit_rangle_FieldAccess_39(o2, i1, i3, env, static) -{1,1}> langle_clinit_rangle_Return_40(i1, i3, env, static') :|: 0 < o2 && 0 <= o2 && 0 <= static && static' <= static + o2
langle_clinit_rangle_Return_40(i1, i3, env, static) -{1,1}> main_Load_41(i1, i3, env, static) :|: 0 >= 0
main_Load_41(i1, i3, env, static) -{0,0}> main_Load_42(i1, i3, env, static) :|: 0 >= 0
main_Load_42(i1, i3, env, static) -{0,0}> main_Load_44(i1, i3, env, static) :|: 0 <= static
main_Load_44(i1, i3, env, static) -{0,0}> main_Load_46(i1, i3, env, static) :|: 0 >= 0
main_Load_46(i1, i3, env, static) -{0,0}> main_Load_48(i1, i3, env, static) :|: 0 >= 0
main_Load_48(i1, i3, env, static) -{1,1}> main_LE_52(i1, i3, env, static) :|: 0 >= 0
main_LE_52(i12, i3, env, static) -{0,0}> main_LE_54(i12, i3, env, static) :|: 1 <= i12
main_LE_54(i12, i3, env, static) -{1,1}> main_Load_58(i12, i3, env, static) :|: 0 < i12 && 1 <= i12
main_Load_58(i12, i3, env, static) -{1,1}> main_LE_62(i12, i3, env, static) :|: 1 <= i12
main_LE_62(i12, i20, env, static) -{0,0}> main_LE_64(i12, i20, env, static) :|: 1 <= i20 && 1 <= i12
main_LE_64(i12, i20, env, static) -{1,1}> main_Load_73(i12, i20, env, static) :|: 0 < i20 && 1 <= i20 && 1 <= i12
main_Load_73(i12, i20, env, static) -{0,0}> main_Load_421(i12, i20, i12, i20, env, static) :|: 1 <= i20 && 1 <= i12

obtained
main_Load_421(i158, i159, i160, i175, env, static) -{5,5}> main_LE_437(i158, i159, i160, i175, env, static) :|: !(i160 = i175) && 1 <= i175 && 1 <= i160 && 1 <= i159
by chaining
main_Load_421(i158, i159, i160, i175, env, static) -{1,1}> main_Load_424(i158, i159, i160, i175, env, static) :|: 1 <= i160 && 1 <= i159 && 1 <= i175
main_Load_424(i158, i159, i160, i175, env, static) -{1,1}> main_EQ_426(i158, i159, i160, i175, env, static) :|: 1 <= i160 && 1 <= i159 && 1 <= i175
main_EQ_426(i158, i159, i160, i175, env, static) -{0,0}> main_EQ_428(i158, i159, i160, i175, env, static) :|: 1 <= i160 && 1 <= i159 && !(i160 = i175) && 1 <= i175
main_EQ_428(i158, i159, i160, i175, env, static) -{1,1}> main_Load_432(i158, i159, i160, i175, env, static) :|: 1 <= i160 && 1 <= i159 && !(i160 = i175) && 1 <= i175
main_Load_432(i158, i159, i160, i175, env, static) -{1,1}> main_Load_434(i158, i159, i160, i175, env, static) :|: 1 <= i160 && 1 <= i159 && 1 <= i175
main_Load_434(i158, i159, i160, i175, env, static) -{1,1}> main_LE_437(i158, i159, i160, i175, env, static) :|: 1 <= i160 && 1 <= i159 && 1 <= i175

(30) Obligation:

IntTrs with 4 rules
Start term: main_Load_1(#0, #1, env, static)
Considered paths: all paths from start
Rules:
main_Load_1(i1, i3, env, static) -{19,19}> main_Load_421(i1, i3, i1, i3, env, static'1) :|: 0 < i1 && 1 <= i3 && 1 <= i1 && static'1 <= static''' + 1 && 0 >= 0 && 0 <= 2 && 0 <= static''' && static''' <= static + 2 && 0 < 1 && 0 <= 1 && 0 <= static && 0 < i3 && 0 <= static'1 && 0 < 2
main_Load_421(i158, i159, i160, i175, env, static) -{5,5}> main_LE_437(i158, i159, i160, i175, env, static) :|: !(i160 = i175) && 1 <= i175 && 1 <= i160 && 1 <= i159
main_LE_437(i158, i159, i160, i175, env, static) -{6,6}> main_Load_421(i158, i159, i183', i175, env, static) :|: i160 - i175 = i183' && 1 <= i175 && i175 < i160 && 1 <= i183' && 1 <= i159 && 2 <= i160 && 1 <= i160
main_LE_437(i158, i159, i160, i175, env, static) -{6,6}> main_Load_421(i158, i159, i160, i182', env, static) :|: 1 <= i175 && 1 <= i159 && i160 <= i175 && 1 <= i182' && 1 <= i160 && 2 <= i175 && i160 < i175 && i175 - i160 = i182'

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

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

main_Load_1(x1, x2, x3, x4) → main_Load_1(x1, x2, x4)
main_Load_421(x1, x2, x3, x4, x5, x6) → main_Load_421(x2, x3, x4)
main_LE_437(x1, x2, x3, x4, x5, x6) → main_LE_437(x2, x3, x4)

(32) Obligation:

IntTrs with 4 rules
Start term: main_Load_1(#0, #1, static)
Considered paths: all paths from start
Rules:
main_Load_1(i1, i3, static) -{19,19}> main_Load_421(i3, i1, i3) :|: 0 < i1 && 1 <= i3 && 1 <= i1 && static'1 <= static''' + 1 && 0 >= 0 && 0 <= 2 && 0 <= static''' && static''' <= static + 2 && 0 < 1 && 0 <= 1 && 0 <= static && 0 < i3 && 0 <= static'1 && 0 < 2
main_Load_421(i159, i160, i175) -{5,5}> main_LE_437(i159, i160, i175) :|: !(i160 = i175) && 1 <= i175 && 1 <= i160 && 1 <= i159
main_LE_437(i159, i160, i175) -{6,6}> main_Load_421(i159, i183', i175) :|: i160 - i175 = i183' && 1 <= i175 && i175 < i160 && 1 <= i183' && 1 <= i159 && 2 <= i160 && 1 <= i160
main_LE_437(i159, i160, i175) -{6,6}> main_Load_421(i159, i160, i182') :|: 1 <= i175 && 1 <= i159 && i160 <= i175 && 1 <= i182' && 1 <= i160 && 2 <= i175 && i160 < i175 && i175 - i160 = i182'

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

Removed div and mod.

main_Load_421(i159, i160, i175) -{5,5}> main_LE_437(i159, i160, i175) :|: !(i160 = i175) && 1 <= i175 && 1 <= i160 && 1 <= i159
was transformed to
main_Load_421(i159, i160, i175) -{5,5}> main_LE_437(i159, i160, i175) :|: i160 < i175 && 1 <= i175 && 1 <= i160 && 1 <= i159
main_Load_421(i159, i160, i175) -{5,5}> main_LE_437(i159, i160, i175) :|: i160 > i175 && 1 <= i175 && 1 <= i160 && 1 <= i159

(34) Obligation:

IntTrs with 5 rules
Start term: main_Load_1(#0, #1, static)
Considered paths: all paths from start
Rules:
main_Load_421(i159, i160, i175) -{5,5}> main_LE_437(i159, i160, i175) :|: i160 < i175 && 1 <= i175 && 1 <= i160 && 1 <= i159
main_Load_1(i1, i3, static) -{19,19}> main_Load_421(i3, i1, i3) :|: 0 < i1 && 1 <= i3 && 1 <= i1 && static'1 <= static''' + 1 && 0 >= 0 && 0 <= 2 && 0 <= static''' && static''' <= static + 2 && 0 < 1 && 0 <= 1 && 0 <= static && 0 < i3 && 0 <= static'1 && 0 < 2
main_Load_421(i159, i160, i175) -{5,5}> main_LE_437(i159, i160, i175) :|: i160 > i175 && 1 <= i175 && 1 <= i160 && 1 <= i159
main_LE_437(i159, i160, i175) -{6,6}> main_Load_421(i159, i183', i175) :|: i160 - i175 = i183' && 1 <= i175 && i175 < i160 && 1 <= i183' && 1 <= i159 && 2 <= i160 && 1 <= i160
main_LE_437(i159, i160, i175) -{6,6}> main_Load_421(i159, i160, i182') :|: 1 <= i175 && 1 <= i159 && i160 <= i175 && 1 <= i182' && 1 <= i160 && 2 <= i175 && i160 < i175 && i175 - i160 = i182'

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

Moved arithmethic from constraints to rhss.

main_LE_437(i159, i160, i175) -{6,6}> main_Load_421(i159, i183', i175) :|: i160 - i175 = i183' && 1 <= i175 && i175 < i160 && 1 <= i183' && 1 <= i159 && 2 <= i160 && 1 <= i160
was transformed to
main_LE_437(i159, i160, i175) -{6,6}> main_Load_421(i159, i160 - i175, i175) :|: i160 - i175 = i183' && 1 <= i175 && i175 < i160 && 1 <= i183' && 1 <= i159 && 2 <= i160 && 1 <= i160

main_LE_437(i159, i160, i175) -{6,6}> main_Load_421(i159, i160, i182') :|: 1 <= i175 && 1 <= i159 && i160 <= i175 && 1 <= i182' && 1 <= i160 && 2 <= i175 && i160 < i175 && i175 - i160 = i182'
was transformed to
main_LE_437(i159, i160, i175) -{6,6}> main_Load_421(i159, i160, i175 - i160) :|: 1 <= i175 && 1 <= i159 && i160 <= i175 && 1 <= i182' && 1 <= i160 && 2 <= i175 && i160 < i175 && i175 - i160 = i182'

(36) Obligation:

IntTrs with 5 rules
Start term: main_Load_1(#0, #1, static)
Considered paths: all paths from start
Rules:
main_Load_421(i159, i160, i175) -{5,5}> main_LE_437(i159, i160, i175) :|: i160 < i175 && 1 <= i175 && 1 <= i160 && 1 <= i159
main_Load_1(i1, i3, static) -{19,19}> main_Load_421(i3, i1, i3) :|: 0 < i1 && 1 <= i3 && 1 <= i1 && static'1 <= static''' + 1 && 0 >= 0 && 0 <= 2 && 0 <= static''' && static''' <= static + 2 && 0 < 1 && 0 <= 1 && 0 <= static && 0 < i3 && 0 <= static'1 && 0 < 2
main_Load_421(i159, i160, i175) -{5,5}> main_LE_437(i159, i160, i175) :|: i160 > i175 && 1 <= i175 && 1 <= i160 && 1 <= i159
main_LE_437(i159, i160, i175) -{6,6}> main_Load_421(i159, i160 - i175, i175) :|: i160 - i175 = i183' && 1 <= i175 && i175 < i160 && 1 <= i183' && 1 <= i159 && 2 <= i160 && 1 <= i160
main_LE_437(i159, i160, i175) -{6,6}> main_Load_421(i159, i160, i175 - i160) :|: 1 <= i175 && 1 <= i159 && i160 <= i175 && 1 <= i182' && 1 <= i160 && 2 <= i175 && i160 < i175 && i175 - i160 = i182'

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

Simplified expressions.

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

main_Load_421(i159, i160, i175) -{5,5}> main_LE_437(i159, i160, i175) :|: i160 > i175 && 1 <= i175 && 1 <= i160 && 1 <= i159
was transformed to
main_Load_421(i159, i160, i175) -{5,5}> main_LE_437(i159, i160, i175) :|: i175 < i160 && 1 <= i175 && 1 <= i160 && 1 <= i159

main_LE_437(i159, i160, i175) -{6,6}> main_Load_421(i159, i160, i175 - i160) :|: 1 <= i175 && 1 <= i159 && i160 <= i175 && 1 <= i182' && 1 <= i160 && 2 <= i175 && i160 < i175 && i175 - i160 = i182'
was transformed to
main_LE_437(i159, i160, i175) -{6,6}> main_Load_421(i159, i160, i175 + -1 * i160) :|: 1 <= i175 && 1 <= i159 && 1 <= i182' && 1 <= i160 && 2 <= i175 && i160 < i175 && i175 + -1 * i160 = i182'

main_LE_437(i159, i160, i175) -{6,6}> main_Load_421(i159, i160 - i175, i175) :|: i160 - i175 = i183' && 1 <= i175 && i175 < i160 && 1 <= i183' && 1 <= i159 && 2 <= i160 && 1 <= i160
was transformed to
main_LE_437(i159, i160, i175) -{6,6}> main_Load_421(i159, i160 + -1 * i175, i175) :|: i160 + -1 * i175 = i183' && 1 <= i175 && i175 < i160 && 1 <= i183' && 1 <= i159 && 2 <= i160 && 1 <= i160

(38) Obligation:

IntTrs with 5 rules
Start term: main_Load_1(#0, #1, static)
Considered paths: all paths from start
Rules:
main_Load_421(i159, i160, i175) -{5,5}> main_LE_437(i159, i160, i175) :|: i160 < i175 && 1 <= i175 && 1 <= i160 && 1 <= i159
main_Load_421(i159, i160, i175) -{5,5}> main_LE_437(i159, i160, i175) :|: i175 < i160 && 1 <= i175 && 1 <= i160 && 1 <= i159
main_Load_1(i1, i3, static) -{19,19}> main_Load_421(i3, i1, i3) :|: 0 < i1 && 1 <= i3 && 1 <= i1 && static'1 <= static''' + 1 && 0 <= static''' && static''' <= static + 2 && 0 <= static && 0 < i3 && 0 <= static'1
main_LE_437(i159, i160, i175) -{6,6}> main_Load_421(i159, i160 + -1 * i175, i175) :|: i160 + -1 * i175 = i183' && 1 <= i175 && i175 < i160 && 1 <= i183' && 1 <= i159 && 2 <= i160 && 1 <= i160
main_LE_437(i159, i160, i175) -{6,6}> main_Load_421(i159, i160, i175 + -1 * i160) :|: 1 <= i175 && 1 <= i159 && 1 <= i182' && 1 <= i160 && 2 <= i175 && i160 < i175 && i175 + -1 * i160 = i182'

(39) koat Proof (EQUIVALENT transformation)

YES(?, 44*ar_0 + 44*ar_1 + 19)

Initial complexity problem:
1: T:
(Comp: ?, Cost: 5) main_Load_421(ar_0, ar_1, ar_2) -> Com_1(main_LE_437(ar_0, ar_1, ar_2)) [ ar_1 < ar_2 /\ 1 <= ar_2 /\ 1 <= ar_1 /\ 1 <= ar_0 ]
(Comp: ?, Cost: 5) main_Load_421(ar_0, ar_1, ar_2) -> Com_1(main_LE_437(ar_0, ar_1, ar_2)) [ ar_2 < ar_1 /\ 1 <= ar_2 /\ 1 <= ar_1 /\ 1 <= ar_0 ]
(Comp: ?, Cost: 19) main_Load_1(ar_0, ar_1, ar_2) -> Com_1(main_Load_421(ar_1, ar_0, ar_1)) [ 0 < ar_0 /\ 1 <= ar_1 /\ 1 <= ar_0 /\ static'1 <= static''' + 1 /\ 0 <= static''' /\ static''' <= ar_2 + 2 /\ 0 <= ar_2 /\ 0 < ar_1 /\ 0 <= static'1 ]
(Comp: ?, Cost: 6) main_LE_437(ar_0, ar_1, ar_2) -> Com_1(main_Load_421(ar_0, ar_1 - ar_2, ar_2)) [ ar_1 - ar_2 = i183' /\ 1 <= ar_2 /\ ar_2 < ar_1 /\ 1 <= i183' /\ 1 <= ar_0 /\ 2 <= ar_1 /\ 1 <= ar_1 ]
(Comp: ?, Cost: 6) main_LE_437(ar_0, ar_1, ar_2) -> Com_1(main_Load_421(ar_0, ar_1, ar_2 - ar_1)) [ 1 <= ar_2 /\ 1 <= ar_0 /\ 1 <= i182' /\ 1 <= ar_1 /\ 2 <= ar_2 /\ ar_1 < ar_2 /\ ar_2 - ar_1 = i182' ]
(Comp: 1, Cost: 0) koat_start(ar_0, ar_1, ar_2) -> Com_1(main_Load_1(ar_0, ar_1, ar_2)) [ 0 <= 0 ]
start location: koat_start
leaf cost: 0

Repeatedly propagating knowledge in problem 1 produces the following problem:
2: T:
(Comp: ?, Cost: 5) main_Load_421(ar_0, ar_1, ar_2) -> Com_1(main_LE_437(ar_0, ar_1, ar_2)) [ ar_1 < ar_2 /\ 1 <= ar_2 /\ 1 <= ar_1 /\ 1 <= ar_0 ]
(Comp: ?, Cost: 5) main_Load_421(ar_0, ar_1, ar_2) -> Com_1(main_LE_437(ar_0, ar_1, ar_2)) [ ar_2 < ar_1 /\ 1 <= ar_2 /\ 1 <= ar_1 /\ 1 <= ar_0 ]
(Comp: 1, Cost: 19) main_Load_1(ar_0, ar_1, ar_2) -> Com_1(main_Load_421(ar_1, ar_0, ar_1)) [ 0 < ar_0 /\ 1 <= ar_1 /\ 1 <= ar_0 /\ static'1 <= static''' + 1 /\ 0 <= static''' /\ static''' <= ar_2 + 2 /\ 0 <= ar_2 /\ 0 < ar_1 /\ 0 <= static'1 ]
(Comp: ?, Cost: 6) main_LE_437(ar_0, ar_1, ar_2) -> Com_1(main_Load_421(ar_0, ar_1 - ar_2, ar_2)) [ ar_1 - ar_2 = i183' /\ 1 <= ar_2 /\ ar_2 < ar_1 /\ 1 <= i183' /\ 1 <= ar_0 /\ 2 <= ar_1 /\ 1 <= ar_1 ]
(Comp: ?, Cost: 6) main_LE_437(ar_0, ar_1, ar_2) -> Com_1(main_Load_421(ar_0, ar_1, ar_2 - ar_1)) [ 1 <= ar_2 /\ 1 <= ar_0 /\ 1 <= i182' /\ 1 <= ar_1 /\ 2 <= ar_2 /\ ar_1 < ar_2 /\ ar_2 - ar_1 = i182' ]
(Comp: 1, Cost: 0) koat_start(ar_0, ar_1, ar_2) -> Com_1(main_Load_1(ar_0, ar_1, ar_2)) [ 0 <= 0 ]
start location: koat_start
leaf cost: 0

A polynomial rank function with
Pol(main_Load_421) = 2*V_2 + 2*V_3
Pol(main_LE_437) = 2*V_2 + 2*V_3 - 1
Pol(main_Load_1) = 2*V_1 + 2*V_2
Pol(koat_start) = 2*V_1 + 2*V_2
orients all transitions weakly and the transitions
main_Load_421(ar_0, ar_1, ar_2) -> Com_1(main_LE_437(ar_0, ar_1, ar_2)) [ ar_2 < ar_1 /\ 1 <= ar_2 /\ 1 <= ar_1 /\ 1 <= ar_0 ]
main_Load_421(ar_0, ar_1, ar_2) -> Com_1(main_LE_437(ar_0, ar_1, ar_2)) [ ar_1 < ar_2 /\ 1 <= ar_2 /\ 1 <= ar_1 /\ 1 <= ar_0 ]
main_LE_437(ar_0, ar_1, ar_2) -> Com_1(main_Load_421(ar_0, ar_1 - ar_2, ar_2)) [ ar_1 - ar_2 = i183' /\ 1 <= ar_2 /\ ar_2 < ar_1 /\ 1 <= i183' /\ 1 <= ar_0 /\ 2 <= ar_1 /\ 1 <= ar_1 ]
main_LE_437(ar_0, ar_1, ar_2) -> Com_1(main_Load_421(ar_0, ar_1, ar_2 - ar_1)) [ 1 <= ar_2 /\ 1 <= ar_0 /\ 1 <= i182' /\ 1 <= ar_1 /\ 2 <= ar_2 /\ ar_1 < ar_2 /\ ar_2 - ar_1 = i182' ]
strictly and produces the following problem:
3: T:
(Comp: 2*ar_0 + 2*ar_1, Cost: 5) main_Load_421(ar_0, ar_1, ar_2) -> Com_1(main_LE_437(ar_0, ar_1, ar_2)) [ ar_1 < ar_2 /\ 1 <= ar_2 /\ 1 <= ar_1 /\ 1 <= ar_0 ]
(Comp: 2*ar_0 + 2*ar_1, Cost: 5) main_Load_421(ar_0, ar_1, ar_2) -> Com_1(main_LE_437(ar_0, ar_1, ar_2)) [ ar_2 < ar_1 /\ 1 <= ar_2 /\ 1 <= ar_1 /\ 1 <= ar_0 ]
(Comp: 1, Cost: 19) main_Load_1(ar_0, ar_1, ar_2) -> Com_1(main_Load_421(ar_1, ar_0, ar_1)) [ 0 < ar_0 /\ 1 <= ar_1 /\ 1 <= ar_0 /\ static'1 <= static''' + 1 /\ 0 <= static''' /\ static''' <= ar_2 + 2 /\ 0 <= ar_2 /\ 0 < ar_1 /\ 0 <= static'1 ]
(Comp: 2*ar_0 + 2*ar_1, Cost: 6) main_LE_437(ar_0, ar_1, ar_2) -> Com_1(main_Load_421(ar_0, ar_1 - ar_2, ar_2)) [ ar_1 - ar_2 = i183' /\ 1 <= ar_2 /\ ar_2 < ar_1 /\ 1 <= i183' /\ 1 <= ar_0 /\ 2 <= ar_1 /\ 1 <= ar_1 ]
(Comp: 2*ar_0 + 2*ar_1, Cost: 6) main_LE_437(ar_0, ar_1, ar_2) -> Com_1(main_Load_421(ar_0, ar_1, ar_2 - ar_1)) [ 1 <= ar_2 /\ 1 <= ar_0 /\ 1 <= i182' /\ 1 <= ar_1 /\ 2 <= ar_2 /\ ar_1 < ar_2 /\ ar_2 - ar_1 = i182' ]
(Comp: 1, Cost: 0) koat_start(ar_0, ar_1, ar_2) -> Com_1(main_Load_1(ar_0, ar_1, ar_2)) [ 0 <= 0 ]
start location: koat_start
leaf cost: 0

Complexity upper bound 44*ar_0 + 44*ar_1 + 19

Time: 0.129 sec (SMT: 0.119 sec)

(0) Obligation:

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

(2) Obligation:

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

(4) Obligation:

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

(6) Obligation:

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

(8) Obligation:

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

(10) Obligation:

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

(12) Obligation:

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

(14) Obligation:

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

(16) Obligation:

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

(18) Obligation:

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

(20) Obligation:

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

(22) Obligation:

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

(24) Obligation:

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

(26) Obligation:

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

(28) Obligation:

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

(30) Obligation:

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

(32) Obligation:

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

(34) Obligation:

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

(36) Obligation:

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

(38) Obligation:

(39) koat Proof (EQUIVALENT transformation)

(40) BOUNDS(CONSTANT, 19 + 44 * |#0| + 44 * |#1|)