time complexity proof of /tmp/tmpo76WNE/PastaB14.jar

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

0 JBC problem

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

↳2 JBCTerminationGraph

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

↳4 JBCComplexityEdges

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

    ↳6 WeightedIntTrs

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

        ↳8 WeightedIntTrs

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

        ↳10 WeightedIntTrs

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

        ↳12 WeightedIntTrs

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

        ↳14 WeightedIntTrs

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

        ↳16 WeightedIntTrs

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

        ↳18 WeightedIntTrs

        ↳19 koat Proof (⇔, 193 ms)

        ↳20 BOUNDS(CONSTANT, 30 + 15 * |#1|)

    ↳21 JBCGraphEdgesToCpxIntTrsProof (CONCRETE UPPER BOUND(ID), 89 ms)

    ↳22 WeightedIntTrs

        ↳23 StraightLineCodeCompressionProof (BOTH CONCRETE BOUNDS(ID, ID), 26 ms)

        ↳24 WeightedIntTrs

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

        ↳26 WeightedIntTrs

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

        ↳28 WeightedIntTrs

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

        ↳30 WeightedIntTrs

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

        ↳32 WeightedIntTrs

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

        ↳34 WeightedIntTrs

↳35 TerminationGraphToComplexityProof (BOTH CONCRETE BOUNDS(ID, ADD(5)), 11 ms)

↳36 JBCComplexityEdges

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

    ↳38 WeightedIntTrs

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

    ↳40 WeightedIntTrs

    ↳41 WeightedIntTrsUnneededArgumentFilterProof (CONCRETE UPPER BOUND(ID), 41 ms)

    ↳42 WeightedIntTrs

    ↳43 WeightedIntTrsDuplicateArgumentFilterProof (CONCRETE UPPER BOUND(ID), 0 ms)

    ↳44 WeightedIntTrs

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

    ↳46 WeightedIntTrs

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

    ↳48 WeightedIntTrs

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

    ↳50 WeightedIntTrs

    ↳51 koat Proof (⇔, 22 ms)

    ↳52 BOUNDS(CONSTANT, 25 + 15 * |#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 PastaB14 {
    public static void main(int x, int y) {
        while (x == y && x > 0) {
            while (y > 0) {
                x--;
                y--;
            }
        }
    }
}

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

Constructed TerminationGraph.

(2) Obligation:

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

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

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

(4) Obligation:

Set of 52 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 52 jbc graph edges to a weighted ITS with 52 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 52 rules
Start term: main_Load_2(#0, #1, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_Load_2(i1, i4, env, static) -{0,0}> main_Load_3(i1, i4, env, static) :|: 0 >= 0
main_Load_3(i1, i4, env, static) -{0,0}> langle_clinit_rangle_ConstantStackPush_6(i1, i4, env, static) :|: 0 >= 0
langle_clinit_rangle_ConstantStackPush_6(i1, i4, env, static) -{1,1}> langle_clinit_rangle_ArrayCreate_12(iconst_0, i1, i4, env, static) :|: iconst_0 = 0
langle_clinit_rangle_ArrayCreate_12(iconst_0, i1, i4, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_13(a2, i1, i4, iconst_0, env, static) :|: a2 = 2 && iconst_0 = 0 && 0 < a2
langle_clinit_rangle_FieldAccess_13(a2, i1, i4, iconst_0, env, static) -{1,1}> langle_clinit_rangle_New_14(i1, i4, env, static') :|: 0 <= a2 && iconst_0 = 0 && static' <= static + a2 && 0 <= static && 0 < a2
langle_clinit_rangle_New_14(i1, i4, env, static) -{0,0}> langle_clinit_rangle_New_16(i1, i4, env, static) :|: 0 >= 0
langle_clinit_rangle_New_16(i1, i4, env, static) -{0,0}> langle_clinit_rangle_New_17(i1, i4, env, static) :|: 0 <= static
langle_clinit_rangle_New_17(i1, i4, env, static) -{1,1}> langle_clinit_rangle_Duplicate_19(o2, i1, i4, env, static) :|: 0 < o2 && o2 = 1
langle_clinit_rangle_Duplicate_19(o2, i1, i4, env, static) -{1,1}> langle_clinit_rangle_ConstantStackPush_21(o2, i1, i4, env, static) :|: 0 < o2
langle_clinit_rangle_ConstantStackPush_21(o2, i1, i4, env, static) -{1,1}> langle_clinit_rangle_InvokeMethod_22(o2, NULL, i1, i4, env, static) :|: NULL = 0 && 0 < o2
langle_clinit_rangle_InvokeMethod_22(o2, NULL, i1, i4, env, static) -{1,1}> langle_init_rangle_Load_24(o2, i1, i4, env, static) :|: NULL = 0 && 0 < o2
langle_init_rangle_Load_24(o2, i1, i4, env, static) -{1,1}> langle_init_rangle_InvokeMethod_26(o2, i1, i4, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_26(o2, i1, i4, env, static) -{1,1}> langle_init_rangle_Load_28(o2, i1, i4, env, static) :|: 0 < o2
langle_init_rangle_Load_28(o2, i1, i4, env, static) -{1,1}> langle_init_rangle_InvokeMethod_30(o2, i1, i4, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_30(o2, i1, i4, env, static) -{1,1}> langle_init_rangle_Return_31(o2, i1, i4, env, static) :|: 0 < o2
langle_init_rangle_Return_31(o2, i1, i4, env, static) -{1,1}> langle_init_rangle_Return_32(o2, i1, i4, env, static) :|: 0 < o2
langle_init_rangle_Return_32(o2, i1, i4, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_34(o2, i1, i4, env, static) :|: 0 < o2
langle_clinit_rangle_FieldAccess_34(o2, i1, i4, env, static) -{1,1}> langle_clinit_rangle_Return_35(i1, i4, env, static') :|: 0 < o2 && 0 <= o2 && 0 <= static && static' <= static + o2
langle_clinit_rangle_Return_35(i1, i4, env, static) -{1,1}> main_Load_40(i1, i4, env, static) :|: 0 >= 0
main_Load_40(i1, i4, env, static) -{0,0}> main_Load_42(i1, i4, env, static) :|: 0 >= 0
main_Load_42(i1, i4, env, static) -{0,0}> main_Load_48(i1, i4, env, static) :|: 0 <= static
main_Load_48(i1, i4, env, static) -{0,0}> main_Load_49(i1, i4, env, static) :|: 0 >= 0
main_Load_49(i1, i4, env, static) -{0,0}> main_Load_50(i1, i4, env, static) :|: 0 >= 0
main_Load_50(i1, i4, env, static) -{1,1}> main_Load_51(i1, i4, env, static) :|: 0 >= 0
main_Load_51(i1, i4, env, static) -{1,1}> main_NE_65(i1, i4, env, static) :|: 0 >= 0
main_NE_65(i1, i4, env, static) -{0,0}> main_NE_66(i1, i4, env, static) :|: !(i1 = i4)
main_NE_65(i1, i4, env, static) -{0,0}> main_NE_67(i4, env, static) :|: i1 = i4
main_NE_67(i4, env, static) -{1,1}> main_Load_70(i4, env, static) :|: i4 = i4
main_Load_70(i4, env, static) -{1,1}> main_LE_72(i4, env, static) :|: 0 >= 0
main_LE_72(i4, env, static) -{0,0}> main_LE_518(i4, i4, env, static) :|: 0 >= 0
main_LE_518(i269, i276, env, static) -{0,0}> main_LE_521(i269, i276, env, static) :|: i276 <= 0
main_LE_518(i269, i277, env, static) -{0,0}> main_LE_522(i269, i277, env, static) :|: 1 <= i277
main_LE_522(i269, i277, env, static) -{1,1}> main_Load_527(i269, i277, env, static) :|: 1 <= i277 && 0 < i277
main_Load_527(i269, i277, env, static) -{0,0}> main_Load_548(i269, i277, i277, env, static) :|: 1 <= i277 && 0 <= i277
main_Load_548(i269, i283, i284, env, static) -{0,0}> main_Load_584(i269, i283, i284, env, static) :|: 0 <= i284 && -1 <= i283 && 0 <= i283
main_Load_584(i269, i313, i314, env, static) -{0,0}> main_Load_602(i269, i313, i314, env, static) :|: 0 <= i314 && -1 <= i313
main_Load_602(i269, i343, i344, env, static) -{1,1}> main_LE_604(i269, i344, i343, env, static) :|: 0 <= i344
main_LE_604(i269, iconst_0, i343, env, static) -{0,0}> main_LE_605(i269, iconst_0, i343, env, static) :|: 0 <= iconst_0 && iconst_0 = 0
main_LE_604(i269, i349, i343, env, static) -{0,0}> main_LE_606(i269, i349, i343, env, static) :|: 0 <= i349 && 1 <= i349
main_LE_605(i269, iconst_0, i343, env, static) -{1,1}> main_Load_607(i269, i343, iconst_0, env, static) :|: iconst_0 <= 0 && iconst_0 = 0
main_LE_606(i269, i349, i343, env, static) -{1,1}> main_Inc_608(i269, i343, i349, env, static) :|: 0 < i349 && 1 <= i349
main_Load_607(i269, i343, iconst_0, env, static) -{1,1}> main_Load_609(i269, i343, iconst_0, env, static) :|: iconst_0 = 0
main_Inc_608(i269, i343, i349, env, static) -{1,1}> main_Inc_610(i269, i356, i349, env, static) :|: i343 + -1 = i356 && 1 <= i349
main_Load_609(i269, i343, iconst_0, env, static) -{1,1}> main_NE_611(i269, i343, iconst_0, env, static) :|: iconst_0 = 0
main_Inc_610(i269, i356, i349, env, static) -{1,1}> main_JMP_612(i269, i356, i370, env, static) :|: 0 <= i370 && i349 + -1 = i370 && 1 <= i349
main_NE_611(i269, i371, iconst_0, env, static) -{0,0}> main_NE_613(i269, i371, iconst_0, env, static) :|: iconst_0 = 0
main_NE_611(i269, iconst_0, iconst_0, env, static) -{0,0}> main_NE_614(i269, iconst_0, env, static) :|: iconst_0 = 0
main_JMP_612(i269, i356, i370, env, static) -{1,1}> main_Load_615(i269, i356, i370, env, static) :|: 0 <= i370
main_NE_614(i269, iconst_0, env, static) -{1,1}> main_Load_627(i269, iconst_0, env, static) :|: iconst_0 = 0
main_Load_615(i269, i356, i370, env, static) -{0,0}> main_Load_602(i269, i356, i370, env, static) :|: 0 <= i370
main_Load_627(i269, iconst_0, env, static) -{1,1}> main_LE_629(i269, iconst_0, env, static) :|: iconst_0 = 0
main_LE_629(i269, iconst_0, env, static) -{0,0}> main_LE_518(i269, iconst_0, env, static) :|: iconst_0 = 0

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

obtained
main_Load_2(i1, i4, env, static) -{17,17}> main_NE_65(i1, i4, env, static'1) :|: 0 >= 0 && 0 < 2 && 0 <= static'1 && 0 <= static && 0 <= 1 && 0 < 1 && static''' <= static + 2 && 0 <= static''' && 0 <= 2 && static'1 <= static''' + 1
by chaining
main_Load_2(i1, i4, env, static) -{0,0}> main_Load_3(i1, i4, env, static) :|: 0 >= 0
main_Load_3(i1, i4, env, static) -{0,0}> langle_clinit_rangle_ConstantStackPush_6(i1, i4, env, static) :|: 0 >= 0
langle_clinit_rangle_ConstantStackPush_6(i1, i4, env, static) -{1,1}> langle_clinit_rangle_ArrayCreate_12(iconst_0, i1, i4, env, static) :|: iconst_0 = 0
langle_clinit_rangle_ArrayCreate_12(iconst_0, i1, i4, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_13(a2, i1, i4, iconst_0, env, static) :|: a2 = 2 && iconst_0 = 0 && 0 < a2
langle_clinit_rangle_FieldAccess_13(a2, i1, i4, iconst_0, env, static) -{1,1}> langle_clinit_rangle_New_14(i1, i4, env, static') :|: 0 <= a2 && iconst_0 = 0 && static' <= static + a2 && 0 <= static && 0 < a2
langle_clinit_rangle_New_14(i1, i4, env, static) -{0,0}> langle_clinit_rangle_New_16(i1, i4, env, static) :|: 0 >= 0
langle_clinit_rangle_New_16(i1, i4, env, static) -{0,0}> langle_clinit_rangle_New_17(i1, i4, env, static) :|: 0 <= static
langle_clinit_rangle_New_17(i1, i4, env, static) -{1,1}> langle_clinit_rangle_Duplicate_19(o2, i1, i4, env, static) :|: 0 < o2 && o2 = 1
langle_clinit_rangle_Duplicate_19(o2, i1, i4, env, static) -{1,1}> langle_clinit_rangle_ConstantStackPush_21(o2, i1, i4, env, static) :|: 0 < o2
langle_clinit_rangle_ConstantStackPush_21(o2, i1, i4, env, static) -{1,1}> langle_clinit_rangle_InvokeMethod_22(o2, NULL, i1, i4, env, static) :|: NULL = 0 && 0 < o2
langle_clinit_rangle_InvokeMethod_22(o2, NULL, i1, i4, env, static) -{1,1}> langle_init_rangle_Load_24(o2, i1, i4, env, static) :|: NULL = 0 && 0 < o2
langle_init_rangle_Load_24(o2, i1, i4, env, static) -{1,1}> langle_init_rangle_InvokeMethod_26(o2, i1, i4, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_26(o2, i1, i4, env, static) -{1,1}> langle_init_rangle_Load_28(o2, i1, i4, env, static) :|: 0 < o2
langle_init_rangle_Load_28(o2, i1, i4, env, static) -{1,1}> langle_init_rangle_InvokeMethod_30(o2, i1, i4, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_30(o2, i1, i4, env, static) -{1,1}> langle_init_rangle_Return_31(o2, i1, i4, env, static) :|: 0 < o2
langle_init_rangle_Return_31(o2, i1, i4, env, static) -{1,1}> langle_init_rangle_Return_32(o2, i1, i4, env, static) :|: 0 < o2
langle_init_rangle_Return_32(o2, i1, i4, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_34(o2, i1, i4, env, static) :|: 0 < o2
langle_clinit_rangle_FieldAccess_34(o2, i1, i4, env, static) -{1,1}> langle_clinit_rangle_Return_35(i1, i4, env, static') :|: 0 < o2 && 0 <= o2 && 0 <= static && static' <= static + o2
langle_clinit_rangle_Return_35(i1, i4, env, static) -{1,1}> main_Load_40(i1, i4, env, static) :|: 0 >= 0
main_Load_40(i1, i4, env, static) -{0,0}> main_Load_42(i1, i4, env, static) :|: 0 >= 0
main_Load_42(i1, i4, env, static) -{0,0}> main_Load_48(i1, i4, env, static) :|: 0 <= static
main_Load_48(i1, i4, env, static) -{0,0}> main_Load_49(i1, i4, env, static) :|: 0 >= 0
main_Load_49(i1, i4, env, static) -{0,0}> main_Load_50(i1, i4, env, static) :|: 0 >= 0
main_Load_50(i1, i4, env, static) -{1,1}> main_Load_51(i1, i4, env, static) :|: 0 >= 0
main_Load_51(i1, i4, env, static) -{1,1}> main_NE_65(i1, i4, env, static) :|: 0 >= 0

obtained
main_NE_65(i1, i1, env, static) -{2,2}> main_LE_518(i1, i1, env, static) :|: 0 >= 0
by chaining
main_NE_65(i1, i4, env, static) -{0,0}> main_NE_67(i4, env, static) :|: i1 = i4
main_NE_67(i4, env, static) -{1,1}> main_Load_70(i4, env, static) :|: i4 = i4
main_Load_70(i4, env, static) -{1,1}> main_LE_72(i4, env, static) :|: 0 >= 0
main_LE_72(i4, env, static) -{0,0}> main_LE_518(i4, i4, env, static) :|: 0 >= 0

obtained
main_LE_518(i269, i277, env, static) -{1,1}> main_Load_602(i269, i277, i277, env, static) :|: -1 <= i277 && 0 <= i277 && 0 < i277 && 1 <= i277
by chaining
main_LE_518(i269, i277, env, static) -{0,0}> main_LE_522(i269, i277, env, static) :|: 1 <= i277
main_LE_522(i269, i277, env, static) -{1,1}> main_Load_527(i269, i277, env, static) :|: 1 <= i277 && 0 < i277
main_Load_527(i269, i277, env, static) -{0,0}> main_Load_548(i269, i277, i277, env, static) :|: 1 <= i277 && 0 <= i277
main_Load_548(i269, i283, i284, env, static) -{0,0}> main_Load_584(i269, i283, i284, env, static) :|: 0 <= i284 && -1 <= i283 && 0 <= i283
main_Load_584(i269, i313, i314, env, static) -{0,0}> main_Load_602(i269, i313, i314, env, static) :|: 0 <= i314 && -1 <= i313

obtained
main_LE_604(i269, i349, i343, env, static) -{4,4}> main_Load_602(i269, i356', i370', env, static) :|: 0 <= i370' && 1 <= i349 && 0 <= i349 && i349 + -1 = i370' && 0 < i349 && i343 + -1 = i356'
by chaining
main_LE_604(i269, i349, i343, env, static) -{0,0}> main_LE_606(i269, i349, i343, env, static) :|: 0 <= i349 && 1 <= i349
main_LE_606(i269, i349, i343, env, static) -{1,1}> main_Inc_608(i269, i343, i349, env, static) :|: 0 < i349 && 1 <= i349
main_Inc_608(i269, i343, i349, env, static) -{1,1}> main_Inc_610(i269, i356, i349, env, static) :|: i343 + -1 = i356 && 1 <= i349
main_Inc_610(i269, i356, i349, env, static) -{1,1}> main_JMP_612(i269, i356, i370, env, static) :|: 0 <= i370 && i349 + -1 = i370 && 1 <= i349
main_JMP_612(i269, i356, i370, env, static) -{1,1}> main_Load_615(i269, i356, i370, env, static) :|: 0 <= i370
main_Load_615(i269, i356, i370, env, static) -{0,0}> main_Load_602(i269, i356, i370, env, static) :|: 0 <= i370

obtained
main_LE_604(i269, 0, i343, env, static) -{3,3}> main_NE_611(i269, i343, 0, env, static) :|: 0 <= 0
by chaining
main_LE_604(i269, iconst_0, i343, env, static) -{0,0}> main_LE_605(i269, iconst_0, i343, env, static) :|: 0 <= iconst_0 && iconst_0 = 0
main_LE_605(i269, iconst_0, i343, env, static) -{1,1}> main_Load_607(i269, i343, iconst_0, env, static) :|: iconst_0 <= 0 && iconst_0 = 0
main_Load_607(i269, i343, iconst_0, env, static) -{1,1}> main_Load_609(i269, i343, iconst_0, env, static) :|: iconst_0 = 0
main_Load_609(i269, i343, iconst_0, env, static) -{1,1}> main_NE_611(i269, i343, iconst_0, env, static) :|: iconst_0 = 0

obtained
main_NE_611(i269, 0, 0, env, static) -{2,2}> main_LE_518(i269, 0, env, static) :|: 0 >= 0
by chaining
main_NE_611(i269, iconst_0, iconst_0, env, static) -{0,0}> main_NE_614(i269, iconst_0, env, static) :|: iconst_0 = 0
main_NE_614(i269, iconst_0, env, static) -{1,1}> main_Load_627(i269, iconst_0, env, static) :|: iconst_0 = 0
main_Load_627(i269, iconst_0, env, static) -{1,1}> main_LE_629(i269, iconst_0, env, static) :|: iconst_0 = 0
main_LE_629(i269, iconst_0, env, static) -{0,0}> main_LE_518(i269, iconst_0, env, static) :|: iconst_0 = 0

(8) Obligation:

IntTrs with 10 rules
Start term: main_Load_2(#0, #1, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_Load_2(i1, i4, env, static) -{17,17}> main_NE_65(i1, i4, env, static'1) :|: 0 >= 0 && 0 < 2 && 0 <= static'1 && 0 <= static && 0 <= 1 && 0 < 1 && static''' <= static + 2 && 0 <= static''' && 0 <= 2 && static'1 <= static''' + 1
main_NE_65(i1, i4, env, static) -{0,0}> main_NE_66(i1, i4, env, static) :|: !(i1 = i4)
main_NE_65(i1, i1, env, static) -{2,2}> main_LE_518(i1, i1, env, static) :|: 0 >= 0
main_LE_518(i269, i276, env, static) -{0,0}> main_LE_521(i269, i276, env, static) :|: i276 <= 0
main_LE_518(i269, i277, env, static) -{1,1}> main_Load_602(i269, i277, i277, env, static) :|: -1 <= i277 && 0 <= i277 && 0 < i277 && 1 <= i277
main_Load_602(i269, i343, i344, env, static) -{1,1}> main_LE_604(i269, i344, i343, env, static) :|: 0 <= i344
main_LE_604(i269, i349, i343, env, static) -{4,4}> main_Load_602(i269, i356', i370', env, static) :|: 0 <= i370' && 1 <= i349 && 0 <= i349 && i349 + -1 = i370' && 0 < i349 && i343 + -1 = i356'
main_LE_604(i269, 0, i343, env, static) -{3,3}> main_NE_611(i269, i343, 0, env, static) :|: 0 <= 0
main_NE_611(i269, i371, iconst_0, env, static) -{0,0}> main_NE_613(i269, i371, iconst_0, env, static) :|: iconst_0 = 0
main_NE_611(i269, 0, 0, env, static) -{2,2}> main_LE_518(i269, 0, env, static) :|: 0 >= 0

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

Moved arithmethic from lhss to constraints.

main_NE_611(i269, 0, 0, env, static) -{2,2}> main_LE_518(i269, 0, env, static) :|: 0 >= 0
was transformed to
main_NE_611(i269, x, x', env, static) -{2,2}> main_LE_518(i269, 0, env, static) :|: 0 >= 0 && x = 0 && x' = 0

main_LE_604(i269, 0, i343, env, static) -{3,3}> main_NE_611(i269, i343, 0, env, static) :|: 0 <= 0
was transformed to
main_LE_604(i269, x, i343, env, static) -{3,3}> main_NE_611(i269, i343, 0, env, static) :|: 0 <= 0 && x = 0

(10) Obligation:

IntTrs with 10 rules
Start term: main_Load_2(#0, #1, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_LE_604(i269, i349, i343, env, static) -{4,4}> main_Load_602(i269, i356', i370', env, static) :|: 0 <= i370' && 1 <= i349 && 0 <= i349 && i349 + -1 = i370' && 0 < i349 && i343 + -1 = i356'
main_Load_2(i1, i4, env, static) -{17,17}> main_NE_65(i1, i4, env, static'1) :|: 0 >= 0 && 0 < 2 && 0 <= static'1 && 0 <= static && 0 <= 1 && 0 < 1 && static''' <= static + 2 && 0 <= static''' && 0 <= 2 && static'1 <= static''' + 1
main_LE_518(i269, i276, env, static) -{0,0}> main_LE_521(i269, i276, env, static) :|: i276 <= 0
main_NE_65(i1, i1, env, static) -{2,2}> main_LE_518(i1, i1, env, static) :|: 0 >= 0
main_NE_611(i269, i371, iconst_0, env, static) -{0,0}> main_NE_613(i269, i371, iconst_0, env, static) :|: iconst_0 = 0
main_NE_65(i1, i4, env, static) -{0,0}> main_NE_66(i1, i4, env, static) :|: !(i1 = i4)
main_LE_518(i269, i277, env, static) -{1,1}> main_Load_602(i269, i277, i277, env, static) :|: -1 <= i277 && 0 <= i277 && 0 < i277 && 1 <= i277
main_Load_602(i269, i343, i344, env, static) -{1,1}> main_LE_604(i269, i344, i343, env, static) :|: 0 <= i344
main_NE_611(i269, x, x', env, static) -{2,2}> main_LE_518(i269, 0, env, static) :|: 0 >= 0 && x = 0 && x' = 0
main_LE_604(i269, x, i343, env, static) -{3,3}> main_NE_611(i269, i343, 0, env, static) :|: 0 <= 0 && x = 0

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

Linearized lhss.

main_NE_65(i1, i1, env, static) -{2,2}> main_LE_518(i1, i1, env, static) :|: 0 >= 0
was transformed to
main_NE_65(i1, x, env, static) -{2,2}> main_LE_518(i1, i1, env, static) :|: 0 >= 0 && x = i1

(12) Obligation:

IntTrs with 10 rules
Start term: main_Load_2(#0, #1, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_Load_2(i1, i4, env, static) -{17,17}> main_NE_65(i1, i4, env, static'1) :|: 0 >= 0 && 0 < 2 && 0 <= static'1 && 0 <= static && 0 <= 1 && 0 < 1 && static''' <= static + 2 && 0 <= static''' && 0 <= 2 && static'1 <= static''' + 1
main_LE_604(i269, i349, i343, env, static) -{4,4}> main_Load_602(i269, i356', i370', env, static) :|: 0 <= i370' && 1 <= i349 && 0 <= i349 && i349 + -1 = i370' && 0 < i349 && i343 + -1 = i356'
main_NE_65(i1, x, env, static) -{2,2}> main_LE_518(i1, i1, env, static) :|: 0 >= 0 && x = i1
main_LE_518(i269, i276, env, static) -{0,0}> main_LE_521(i269, i276, env, static) :|: i276 <= 0
main_NE_611(i269, i371, iconst_0, env, static) -{0,0}> main_NE_613(i269, i371, iconst_0, env, static) :|: iconst_0 = 0
main_NE_611(i269, x, x', env, static) -{2,2}> main_LE_518(i269, 0, env, static) :|: 0 >= 0 && x = 0 && x' = 0
main_NE_65(i1, i4, env, static) -{0,0}> main_NE_66(i1, i4, env, static) :|: !(i1 = i4)
main_LE_518(i269, i277, env, static) -{1,1}> main_Load_602(i269, i277, i277, env, static) :|: -1 <= i277 && 0 <= i277 && 0 < i277 && 1 <= i277
main_Load_602(i269, i343, i344, env, static) -{1,1}> main_LE_604(i269, i344, i343, env, static) :|: 0 <= i344
main_LE_604(i269, x, i343, env, static) -{3,3}> main_NE_611(i269, i343, 0, env, static) :|: 0 <= 0 && x = 0

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

Removed div and mod.

main_NE_65(i1, i4, env, static) -{0,0}> main_NE_66(i1, i4, env, static) :|: !(i1 = i4)
was transformed to
main_NE_65(i1, i4, env, static) -{0,0}> main_NE_66(i1, i4, env, static) :|: i1 < i4
main_NE_65(i1, i4, env, static) -{0,0}> main_NE_66(i1, i4, env, static) :|: i1 > i4

(14) Obligation:

IntTrs with 11 rules
Start term: main_Load_2(#0, #1, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_LE_604(i269, i349, i343, env, static) -{4,4}> main_Load_602(i269, i356', i370', env, static) :|: 0 <= i370' && 1 <= i349 && 0 <= i349 && i349 + -1 = i370' && 0 < i349 && i343 + -1 = i356'
main_Load_2(i1, i4, env, static) -{17,17}> main_NE_65(i1, i4, env, static'1) :|: 0 >= 0 && 0 < 2 && 0 <= static'1 && 0 <= static && 0 <= 1 && 0 < 1 && static''' <= static + 2 && 0 <= static''' && 0 <= 2 && static'1 <= static''' + 1
main_NE_65(i1, x, env, static) -{2,2}> main_LE_518(i1, i1, env, static) :|: 0 >= 0 && x = i1
main_LE_518(i269, i276, env, static) -{0,0}> main_LE_521(i269, i276, env, static) :|: i276 <= 0
main_NE_611(i269, i371, iconst_0, env, static) -{0,0}> main_NE_613(i269, i371, iconst_0, env, static) :|: iconst_0 = 0
main_NE_611(i269, x, x', env, static) -{2,2}> main_LE_518(i269, 0, env, static) :|: 0 >= 0 && x = 0 && x' = 0
main_NE_65(i1, i4, env, static) -{0,0}> main_NE_66(i1, i4, env, static) :|: i1 < i4
main_LE_518(i269, i277, env, static) -{1,1}> main_Load_602(i269, i277, i277, env, static) :|: -1 <= i277 && 0 <= i277 && 0 < i277 && 1 <= i277
main_Load_602(i269, i343, i344, env, static) -{1,1}> main_LE_604(i269, i344, i343, env, static) :|: 0 <= i344
main_NE_65(i1, i4, env, static) -{0,0}> main_NE_66(i1, i4, env, static) :|: i1 > i4
main_LE_604(i269, x, i343, env, static) -{3,3}> main_NE_611(i269, i343, 0, env, static) :|: 0 <= 0 && x = 0

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

Moved arithmethic from constraints to rhss.

main_LE_604(i269, i349, i343, env, static) -{4,4}> main_Load_602(i269, i356', i370', env, static) :|: 0 <= i370' && 1 <= i349 && 0 <= i349 && i349 + -1 = i370' && 0 < i349 && i343 + -1 = i356'
was transformed to
main_LE_604(i269, i349, i343, env, static) -{4,4}> main_Load_602(i269, i343 + -1, i349 + -1, env, static) :|: 0 <= i370' && 1 <= i349 && 0 <= i349 && i349 + -1 = i370' && 0 < i349 && i343 + -1 = i356'

main_NE_611(i269, i371, iconst_0, env, static) -{0,0}> main_NE_613(i269, i371, iconst_0, env, static) :|: iconst_0 = 0
was transformed to
main_NE_611(i269, i371, iconst_0, env, static) -{0,0}> main_NE_613(i269, i371, 0, env, static) :|: iconst_0 = 0

(16) Obligation:

IntTrs with 11 rules
Start term: main_Load_2(#0, #1, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_Load_2(i1, i4, env, static) -{17,17}> main_NE_65(i1, i4, env, static'1) :|: 0 >= 0 && 0 < 2 && 0 <= static'1 && 0 <= static && 0 <= 1 && 0 < 1 && static''' <= static + 2 && 0 <= static''' && 0 <= 2 && static'1 <= static''' + 1
main_LE_604(i269, i349, i343, env, static) -{4,4}> main_Load_602(i269, i343 + -1, i349 + -1, env, static) :|: 0 <= i370' && 1 <= i349 && 0 <= i349 && i349 + -1 = i370' && 0 < i349 && i343 + -1 = i356'
main_NE_65(i1, x, env, static) -{2,2}> main_LE_518(i1, i1, env, static) :|: 0 >= 0 && x = i1
main_LE_518(i269, i276, env, static) -{0,0}> main_LE_521(i269, i276, env, static) :|: i276 <= 0
main_NE_611(i269, i371, iconst_0, env, static) -{0,0}> main_NE_613(i269, i371, 0, env, static) :|: iconst_0 = 0
main_NE_65(i1, i4, env, static) -{0,0}> main_NE_66(i1, i4, env, static) :|: i1 < i4
main_NE_611(i269, x, x', env, static) -{2,2}> main_LE_518(i269, 0, env, static) :|: 0 >= 0 && x = 0 && x' = 0
main_LE_518(i269, i277, env, static) -{1,1}> main_Load_602(i269, i277, i277, env, static) :|: -1 <= i277 && 0 <= i277 && 0 < i277 && 1 <= i277
main_Load_602(i269, i343, i344, env, static) -{1,1}> main_LE_604(i269, i344, i343, env, static) :|: 0 <= i344
main_LE_604(i269, x, i343, env, static) -{3,3}> main_NE_611(i269, i343, 0, env, static) :|: 0 <= 0 && x = 0
main_NE_65(i1, i4, env, static) -{0,0}> main_NE_66(i1, i4, env, static) :|: i1 > i4

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

Simplified expressions.

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

main_NE_65(i1, x, env, static) -{2,2}> main_LE_518(i1, i1, env, static) :|: 0 >= 0 && x = i1
was transformed to
main_NE_65(i1, x, env, static) -{2,2}> main_LE_518(i1, i1, env, static) :|: x = i1

main_LE_604(i269, i349, i343, env, static) -{4,4}> main_Load_602(i269, i343 + -1, i349 + -1, env, static) :|: 0 <= i370' && 1 <= i349 && 0 <= i349 && i349 + -1 = i370' && 0 < i349 && i343 + -1 = i356'
was transformed to
main_LE_604(i269, i349, i343, env, static) -{4,4}> main_Load_602(i269, i343 - 1, i349 - 1, env, static) :|: 0 <= i370' && 1 <= i349 && i349 - 1 = i370' && 0 < i349 && i343 - 1 = i356'

main_NE_611(i269, x, x', env, static) -{2,2}> main_LE_518(i269, 0, env, static) :|: 0 >= 0 && x = 0 && x' = 0
was transformed to
main_NE_611(i269, x, x', env, static) -{2,2}> main_LE_518(i269, 0, env, static) :|: x = 0 && x' = 0

main_LE_518(i269, i277, env, static) -{1,1}> main_Load_602(i269, i277, i277, env, static) :|: -1 <= i277 && 0 <= i277 && 0 < i277 && 1 <= i277
was transformed to
main_LE_518(i269, i277, env, static) -{1,1}> main_Load_602(i269, i277, i277, env, static) :|: -1 <= i277 && 0 < i277 && 1 <= i277

main_NE_65(i1, i4, env, static) -{0,0}> main_NE_66(i1, i4, env, static) :|: i1 > i4
was transformed to
main_NE_65(i1, i4, env, static) -{0,0}> main_NE_66(i1, i4, env, static) :|: i4 < i1

main_LE_604(i269, x, i343, env, static) -{3,3}> main_NE_611(i269, i343, 0, env, static) :|: 0 <= 0 && x = 0
was transformed to
main_LE_604(i269, x, i343, env, static) -{3,3}> main_NE_611(i269, i343, 0, env, static) :|: x = 0

(18) Obligation:

IntTrs with 11 rules
Start term: main_Load_2(#0, #1, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_NE_611(i269, i371, iconst_0, env, static) -{0,0}> main_NE_613(i269, i371, 0, env, static) :|: iconst_0 = 0
main_LE_518(i269, i276, env, static) -{0,0}> main_LE_521(i269, i276, env, static) :|: i276 <= 0
main_LE_604(i269, i349, i343, env, static) -{4,4}> main_Load_602(i269, i343 - 1, i349 - 1, env, static) :|: 0 <= i370' && 1 <= i349 && i349 - 1 = i370' && 0 < i349 && i343 - 1 = i356'
main_NE_65(i1, i4, env, static) -{0,0}> main_NE_66(i1, i4, env, static) :|: i1 < i4
main_NE_65(i1, i4, env, static) -{0,0}> main_NE_66(i1, i4, env, static) :|: i4 < i1
main_LE_604(i269, x, i343, env, static) -{3,3}> main_NE_611(i269, i343, 0, env, static) :|: x = 0
main_Load_602(i269, i343, i344, env, static) -{1,1}> main_LE_604(i269, i344, i343, env, static) :|: 0 <= i344
main_Load_2(i1, i4, env, static) -{17,17}> main_NE_65(i1, i4, env, static'1) :|: 0 <= static'1 && 0 <= static && static''' <= static + 2 && 0 <= static''' && static'1 <= static''' + 1
main_NE_65(i1, x, env, static) -{2,2}> main_LE_518(i1, i1, env, static) :|: x = i1
main_NE_611(i269, x, x', env, static) -{2,2}> main_LE_518(i269, 0, env, static) :|: x = 0 && x' = 0
main_LE_518(i269, i277, env, static) -{1,1}> main_Load_602(i269, i277, i277, env, static) :|: -1 <= i277 && 0 < i277 && 1 <= i277

(19) koat Proof (EQUIVALENT transformation)

YES(?, 15*ar_1 + 30)

Initial complexity problem:
1: T:
(Comp: ?, Cost: 0) main_NE_611(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_NE_613(ar_0, ar_1, 0, ar_3, ar_4)) [ ar_2 = 0 ]
(Comp: ?, Cost: 0) main_LE_518(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_LE_521(ar_0, ar_1, ar_2, ar_3, arityPad)) [ ar_1 <= 0 ]
(Comp: ?, Cost: 4) main_LE_604(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_Load_602(ar_0, ar_2 - 1, ar_1 - 1, ar_3, ar_4)) [ 0 <= i370' /\ 1 <= ar_1 /\ ar_1 - 1 = i370' /\ 0 < ar_1 /\ ar_2 - 1 = i356' ]
(Comp: ?, Cost: 0) main_NE_65(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_NE_66(ar_0, ar_1, ar_2, ar_3, arityPad)) [ ar_0 < ar_1 ]
(Comp: ?, Cost: 0) main_NE_65(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_NE_66(ar_0, ar_1, ar_2, ar_3, arityPad)) [ ar_1 < ar_0 ]
(Comp: ?, Cost: 3) main_LE_604(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_NE_611(ar_0, ar_2, 0, ar_3, ar_4)) [ ar_1 = 0 ]
(Comp: ?, Cost: 1) main_Load_602(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_LE_604(ar_0, ar_2, ar_1, ar_3, ar_4)) [ 0 <= ar_2 ]
(Comp: ?, Cost: 17) main_Load_2(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_NE_65(ar_0, ar_1, ar_2, static'1, arityPad)) [ 0 <= static'1 /\ 0 <= ar_3 /\ static''' <= ar_3 + 2 /\ 0 <= static''' /\ static'1 <= static''' + 1 ]
(Comp: ?, Cost: 2) main_NE_65(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_LE_518(ar_0, ar_0, ar_2, ar_3, arityPad)) [ ar_1 = ar_0 ]
(Comp: ?, Cost: 2) main_NE_611(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_LE_518(ar_0, 0, ar_3, ar_4, arityPad)) [ ar_1 = 0 /\ ar_2 = 0 ]
(Comp: ?, Cost: 1) main_LE_518(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_Load_602(ar_0, ar_1, ar_1, ar_2, ar_3)) [ -1 <= ar_1 /\ 0 < ar_1 /\ 1 <= ar_1 ]
(Comp: 1, Cost: 0) koat_start(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_Load_2(ar_0, ar_1, ar_2, ar_3, ar_4)) [ 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_NE_611(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_NE_613(ar_0, ar_1, 0, ar_3, ar_4)) [ ar_2 = 0 ]
(Comp: ?, Cost: 0) main_LE_518(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_LE_521(ar_0, ar_1, ar_2, ar_3, arityPad)) [ ar_1 <= 0 ]
(Comp: ?, Cost: 4) main_LE_604(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_Load_602(ar_0, ar_2 - 1, ar_1 - 1, ar_3, ar_4)) [ 0 <= i370' /\ 1 <= ar_1 /\ ar_1 - 1 = i370' /\ 0 < ar_1 /\ ar_2 - 1 = i356' ]
(Comp: 1, Cost: 0) main_NE_65(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_NE_66(ar_0, ar_1, ar_2, ar_3, arityPad)) [ ar_0 < ar_1 ]
(Comp: 1, Cost: 0) main_NE_65(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_NE_66(ar_0, ar_1, ar_2, ar_3, arityPad)) [ ar_1 < ar_0 ]
(Comp: ?, Cost: 3) main_LE_604(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_NE_611(ar_0, ar_2, 0, ar_3, ar_4)) [ ar_1 = 0 ]
(Comp: ?, Cost: 1) main_Load_602(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_LE_604(ar_0, ar_2, ar_1, ar_3, ar_4)) [ 0 <= ar_2 ]
(Comp: 1, Cost: 17) main_Load_2(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_NE_65(ar_0, ar_1, ar_2, static'1, arityPad)) [ 0 <= static'1 /\ 0 <= ar_3 /\ static''' <= ar_3 + 2 /\ 0 <= static''' /\ static'1 <= static''' + 1 ]
(Comp: 1, Cost: 2) main_NE_65(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_LE_518(ar_0, ar_0, ar_2, ar_3, arityPad)) [ ar_1 = ar_0 ]
(Comp: ?, Cost: 2) main_NE_611(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_LE_518(ar_0, 0, ar_3, ar_4, arityPad)) [ ar_1 = 0 /\ ar_2 = 0 ]
(Comp: 1, Cost: 1) main_LE_518(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_Load_602(ar_0, ar_1, ar_1, ar_2, ar_3)) [ -1 <= ar_1 /\ 0 < ar_1 /\ 1 <= ar_1 ]
(Comp: 1, Cost: 0) koat_start(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_Load_2(ar_0, ar_1, ar_2, ar_3, ar_4)) [ 0 <= 0 ]
start location: koat_start
leaf cost: 0

A polynomial rank function with
Pol(main_NE_611) = 1
Pol(main_NE_613) = 0
Pol(main_LE_518) = 1
Pol(main_LE_521) = 0
Pol(main_LE_604) = 1
Pol(main_Load_602) = 1
Pol(main_NE_65) = 1
Pol(main_NE_66) = 0
Pol(main_Load_2) = 1
Pol(koat_start) = 1
orients all transitions weakly and the transitions
main_NE_611(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_NE_613(ar_0, ar_1, 0, ar_3, ar_4)) [ ar_2 = 0 ]
main_LE_518(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_LE_521(ar_0, ar_1, ar_2, ar_3, arityPad)) [ ar_1 <= 0 ]
strictly and produces the following problem:
3: T:
(Comp: 1, Cost: 0) main_NE_611(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_NE_613(ar_0, ar_1, 0, ar_3, ar_4)) [ ar_2 = 0 ]
(Comp: 1, Cost: 0) main_LE_518(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_LE_521(ar_0, ar_1, ar_2, ar_3, arityPad)) [ ar_1 <= 0 ]
(Comp: ?, Cost: 4) main_LE_604(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_Load_602(ar_0, ar_2 - 1, ar_1 - 1, ar_3, ar_4)) [ 0 <= i370' /\ 1 <= ar_1 /\ ar_1 - 1 = i370' /\ 0 < ar_1 /\ ar_2 - 1 = i356' ]
(Comp: 1, Cost: 0) main_NE_65(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_NE_66(ar_0, ar_1, ar_2, ar_3, arityPad)) [ ar_0 < ar_1 ]
(Comp: 1, Cost: 0) main_NE_65(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_NE_66(ar_0, ar_1, ar_2, ar_3, arityPad)) [ ar_1 < ar_0 ]
(Comp: ?, Cost: 3) main_LE_604(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_NE_611(ar_0, ar_2, 0, ar_3, ar_4)) [ ar_1 = 0 ]
(Comp: ?, Cost: 1) main_Load_602(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_LE_604(ar_0, ar_2, ar_1, ar_3, ar_4)) [ 0 <= ar_2 ]
(Comp: 1, Cost: 17) main_Load_2(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_NE_65(ar_0, ar_1, ar_2, static'1, arityPad)) [ 0 <= static'1 /\ 0 <= ar_3 /\ static''' <= ar_3 + 2 /\ 0 <= static''' /\ static'1 <= static''' + 1 ]
(Comp: 1, Cost: 2) main_NE_65(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_LE_518(ar_0, ar_0, ar_2, ar_3, arityPad)) [ ar_1 = ar_0 ]
(Comp: ?, Cost: 2) main_NE_611(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_LE_518(ar_0, 0, ar_3, ar_4, arityPad)) [ ar_1 = 0 /\ ar_2 = 0 ]
(Comp: 1, Cost: 1) main_LE_518(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_Load_602(ar_0, ar_1, ar_1, ar_2, ar_3)) [ -1 <= ar_1 /\ 0 < ar_1 /\ 1 <= ar_1 ]
(Comp: 1, Cost: 0) koat_start(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_Load_2(ar_0, ar_1, ar_2, ar_3, ar_4)) [ 0 <= 0 ]
start location: koat_start
leaf cost: 0

A polynomial rank function with
Pol(main_NE_611) = 1
Pol(main_LE_518) = 0
Pol(main_Load_602) = 2
Pol(main_LE_604) = 2
and size complexities
S("koat_start(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_Load_2(ar_0, ar_1, ar_2, ar_3, ar_4)) [ 0 <= 0 ]", 0-0) = ar_0
S("koat_start(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_Load_2(ar_0, ar_1, ar_2, ar_3, ar_4)) [ 0 <= 0 ]", 0-1) = ar_1
S("koat_start(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_Load_2(ar_0, ar_1, ar_2, ar_3, ar_4)) [ 0 <= 0 ]", 0-2) = ar_2
S("koat_start(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_Load_2(ar_0, ar_1, ar_2, ar_3, ar_4)) [ 0 <= 0 ]", 0-3) = ar_3
S("koat_start(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_Load_2(ar_0, ar_1, ar_2, ar_3, ar_4)) [ 0 <= 0 ]", 0-4) = ar_4
S("main_LE_518(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_Load_602(ar_0, ar_1, ar_1, ar_2, ar_3)) [ -1 <= ar_1 /\\ 0 < ar_1 /\\ 1 <= ar_1 ]", 0-0) = ar_0
S("main_LE_518(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_Load_602(ar_0, ar_1, ar_1, ar_2, ar_3)) [ -1 <= ar_1 /\\ 0 < ar_1 /\\ 1 <= ar_1 ]", 0-1) = ar_0
S("main_LE_518(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_Load_602(ar_0, ar_1, ar_1, ar_2, ar_3)) [ -1 <= ar_1 /\\ 0 < ar_1 /\\ 1 <= ar_1 ]", 0-2) = ar_0
S("main_LE_518(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_Load_602(ar_0, ar_1, ar_1, ar_2, ar_3)) [ -1 <= ar_1 /\\ 0 < ar_1 /\\ 1 <= ar_1 ]", 0-3) = ar_2
S("main_LE_518(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_Load_602(ar_0, ar_1, ar_1, ar_2, ar_3)) [ -1 <= ar_1 /\\ 0 < ar_1 /\\ 1 <= ar_1 ]", 0-4) = ar_3 + 3
S("main_NE_611(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_LE_518(ar_0, 0, ar_3, ar_4, arityPad)) [ ar_1 = 0 /\\ ar_2 = 0 ]", 0-0) = ar_0
S("main_NE_611(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_LE_518(ar_0, 0, ar_3, ar_4, arityPad)) [ ar_1 = 0 /\\ ar_2 = 0 ]", 0-1) = 0
S("main_NE_611(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_LE_518(ar_0, 0, ar_3, ar_4, arityPad)) [ ar_1 = 0 /\\ ar_2 = 0 ]", 0-2) = ar_2
S("main_NE_611(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_LE_518(ar_0, 0, ar_3, ar_4, arityPad)) [ ar_1 = 0 /\\ ar_2 = 0 ]", 0-3) = ar_3 + 3
S("main_NE_611(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_LE_518(ar_0, 0, ar_3, ar_4, arityPad)) [ ar_1 = 0 /\\ ar_2 = 0 ]", 0-4) = ?
S("main_NE_65(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_LE_518(ar_0, ar_0, ar_2, ar_3, arityPad)) [ ar_1 = ar_0 ]", 0-0) = ar_0
S("main_NE_65(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_LE_518(ar_0, ar_0, ar_2, ar_3, arityPad)) [ ar_1 = ar_0 ]", 0-1) = ar_0
S("main_NE_65(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_LE_518(ar_0, ar_0, ar_2, ar_3, arityPad)) [ ar_1 = ar_0 ]", 0-2) = ar_2
S("main_NE_65(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_LE_518(ar_0, ar_0, ar_2, ar_3, arityPad)) [ ar_1 = ar_0 ]", 0-3) = ar_3 + 3
S("main_NE_65(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_LE_518(ar_0, ar_0, ar_2, ar_3, arityPad)) [ ar_1 = ar_0 ]", 0-4) = ?
S("main_Load_2(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_NE_65(ar_0, ar_1, ar_2, static'1, arityPad)) [ 0 <= static'1 /\\ 0 <= ar_3 /\\ static''' <= ar_3 + 2 /\\ 0 <= static''' /\\ static'1 <= static''' + 1 ]", 0-0) = ar_0
S("main_Load_2(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_NE_65(ar_0, ar_1, ar_2, static'1, arityPad)) [ 0 <= static'1 /\\ 0 <= ar_3 /\\ static''' <= ar_3 + 2 /\\ 0 <= static''' /\\ static'1 <= static''' + 1 ]", 0-1) = ar_1
S("main_Load_2(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_NE_65(ar_0, ar_1, ar_2, static'1, arityPad)) [ 0 <= static'1 /\\ 0 <= ar_3 /\\ static''' <= ar_3 + 2 /\\ 0 <= static''' /\\ static'1 <= static''' + 1 ]", 0-2) = ar_2
S("main_Load_2(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_NE_65(ar_0, ar_1, ar_2, static'1, arityPad)) [ 0 <= static'1 /\\ 0 <= ar_3 /\\ static''' <= ar_3 + 2 /\\ 0 <= static''' /\\ static'1 <= static''' + 1 ]", 0-3) = ar_3 + 3
S("main_Load_2(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_NE_65(ar_0, ar_1, ar_2, static'1, arityPad)) [ 0 <= static'1 /\\ 0 <= ar_3 /\\ static''' <= ar_3 + 2 /\\ 0 <= static''' /\\ static'1 <= static''' + 1 ]", 0-4) = ?
S("main_Load_602(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_LE_604(ar_0, ar_2, ar_1, ar_3, ar_4)) [ 0 <= ar_2 ]", 0-0) = ar_0
S("main_Load_602(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_LE_604(ar_0, ar_2, ar_1, ar_3, ar_4)) [ 0 <= ar_2 ]", 0-1) = ar_0
S("main_Load_602(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_LE_604(ar_0, ar_2, ar_1, ar_3, ar_4)) [ 0 <= ar_2 ]", 0-2) = ?
S("main_Load_602(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_LE_604(ar_0, ar_2, ar_1, ar_3, ar_4)) [ 0 <= ar_2 ]", 0-3) = ar_2
S("main_Load_602(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_LE_604(ar_0, ar_2, ar_1, ar_3, ar_4)) [ 0 <= ar_2 ]", 0-4) = ar_3 + 3
S("main_LE_604(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_NE_611(ar_0, ar_2, 0, ar_3, ar_4)) [ ar_1 = 0 ]", 0-0) = ar_0
S("main_LE_604(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_NE_611(ar_0, ar_2, 0, ar_3, ar_4)) [ ar_1 = 0 ]", 0-1) = ?
S("main_LE_604(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_NE_611(ar_0, ar_2, 0, ar_3, ar_4)) [ ar_1 = 0 ]", 0-2) = 0
S("main_LE_604(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_NE_611(ar_0, ar_2, 0, ar_3, ar_4)) [ ar_1 = 0 ]", 0-3) = ar_2
S("main_LE_604(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_NE_611(ar_0, ar_2, 0, ar_3, ar_4)) [ ar_1 = 0 ]", 0-4) = ar_3 + 3
S("main_NE_65(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_NE_66(ar_0, ar_1, ar_2, ar_3, arityPad)) [ ar_1 < ar_0 ]", 0-0) = ar_0
S("main_NE_65(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_NE_66(ar_0, ar_1, ar_2, ar_3, arityPad)) [ ar_1 < ar_0 ]", 0-1) = ar_1
S("main_NE_65(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_NE_66(ar_0, ar_1, ar_2, ar_3, arityPad)) [ ar_1 < ar_0 ]", 0-2) = ar_2
S("main_NE_65(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_NE_66(ar_0, ar_1, ar_2, ar_3, arityPad)) [ ar_1 < ar_0 ]", 0-3) = ar_3 + 3
S("main_NE_65(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_NE_66(ar_0, ar_1, ar_2, ar_3, arityPad)) [ ar_1 < ar_0 ]", 0-4) = ?
S("main_NE_65(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_NE_66(ar_0, ar_1, ar_2, ar_3, arityPad)) [ ar_0 < ar_1 ]", 0-0) = ar_0
S("main_NE_65(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_NE_66(ar_0, ar_1, ar_2, ar_3, arityPad)) [ ar_0 < ar_1 ]", 0-1) = ar_1
S("main_NE_65(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_NE_66(ar_0, ar_1, ar_2, ar_3, arityPad)) [ ar_0 < ar_1 ]", 0-2) = ar_2
S("main_NE_65(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_NE_66(ar_0, ar_1, ar_2, ar_3, arityPad)) [ ar_0 < ar_1 ]", 0-3) = ar_3 + 3
S("main_NE_65(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_NE_66(ar_0, ar_1, ar_2, ar_3, arityPad)) [ ar_0 < ar_1 ]", 0-4) = ?
S("main_LE_604(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_Load_602(ar_0, ar_2 - 1, ar_1 - 1, ar_3, ar_4)) [ 0 <= i370' /\\ 1 <= ar_1 /\\ ar_1 - 1 = i370' /\\ 0 < ar_1 /\\ ar_2 - 1 = i356' ]", 0-0) = ar_0
S("main_LE_604(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_Load_602(ar_0, ar_2 - 1, ar_1 - 1, ar_3, ar_4)) [ 0 <= i370' /\\ 1 <= ar_1 /\\ ar_1 - 1 = i370' /\\ 0 < ar_1 /\\ ar_2 - 1 = i356' ]", 0-1) = ?
S("main_LE_604(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_Load_602(ar_0, ar_2 - 1, ar_1 - 1, ar_3, ar_4)) [ 0 <= i370' /\\ 1 <= ar_1 /\\ ar_1 - 1 = i370' /\\ 0 < ar_1 /\\ ar_2 - 1 = i356' ]", 0-2) = ar_0
S("main_LE_604(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_Load_602(ar_0, ar_2 - 1, ar_1 - 1, ar_3, ar_4)) [ 0 <= i370' /\\ 1 <= ar_1 /\\ ar_1 - 1 = i370' /\\ 0 < ar_1 /\\ ar_2 - 1 = i356' ]", 0-3) = ar_2
S("main_LE_604(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_Load_602(ar_0, ar_2 - 1, ar_1 - 1, ar_3, ar_4)) [ 0 <= i370' /\\ 1 <= ar_1 /\\ ar_1 - 1 = i370' /\\ 0 < ar_1 /\\ ar_2 - 1 = i356' ]", 0-4) = ar_3 + 3
S("main_LE_518(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_LE_521(ar_0, ar_1, ar_2, ar_3, arityPad)) [ ar_1 <= 0 ]", 0-0) = ar_0
S("main_LE_518(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_LE_521(ar_0, ar_1, ar_2, ar_3, arityPad)) [ ar_1 <= 0 ]", 0-1) = ar_0
S("main_LE_518(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_LE_521(ar_0, ar_1, ar_2, ar_3, arityPad)) [ ar_1 <= 0 ]", 0-2) = ar_2
S("main_LE_518(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_LE_521(ar_0, ar_1, ar_2, ar_3, arityPad)) [ ar_1 <= 0 ]", 0-3) = ar_3 + 3
S("main_LE_518(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_LE_521(ar_0, ar_1, ar_2, ar_3, arityPad)) [ ar_1 <= 0 ]", 0-4) = ?
S("main_NE_611(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_NE_613(ar_0, ar_1, 0, ar_3, ar_4)) [ ar_2 = 0 ]", 0-0) = ar_0
S("main_NE_611(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_NE_613(ar_0, ar_1, 0, ar_3, ar_4)) [ ar_2 = 0 ]", 0-1) = ?
S("main_NE_611(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_NE_613(ar_0, ar_1, 0, ar_3, ar_4)) [ ar_2 = 0 ]", 0-2) = 0
S("main_NE_611(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_NE_613(ar_0, ar_1, 0, ar_3, ar_4)) [ ar_2 = 0 ]", 0-3) = ar_2
S("main_NE_611(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_NE_613(ar_0, ar_1, 0, ar_3, ar_4)) [ ar_2 = 0 ]", 0-4) = ar_3 + 3
orients the transitions
main_NE_611(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_LE_518(ar_0, 0, ar_3, ar_4, arityPad)) [ ar_1 = 0 /\ ar_2 = 0 ]
main_Load_602(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_LE_604(ar_0, ar_2, ar_1, ar_3, ar_4)) [ 0 <= ar_2 ]
main_LE_604(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_NE_611(ar_0, ar_2, 0, ar_3, ar_4)) [ ar_1 = 0 ]
main_LE_604(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_Load_602(ar_0, ar_2 - 1, ar_1 - 1, ar_3, ar_4)) [ 0 <= i370' /\ 1 <= ar_1 /\ ar_1 - 1 = i370' /\ 0 < ar_1 /\ ar_2 - 1 = i356' ]
weakly and the transitions
main_NE_611(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_LE_518(ar_0, 0, ar_3, ar_4, arityPad)) [ ar_1 = 0 /\ ar_2 = 0 ]
main_LE_604(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_NE_611(ar_0, ar_2, 0, ar_3, ar_4)) [ ar_1 = 0 ]
strictly and produces the following problem:
4: T:
(Comp: 1, Cost: 0) main_NE_611(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_NE_613(ar_0, ar_1, 0, ar_3, ar_4)) [ ar_2 = 0 ]
(Comp: 1, Cost: 0) main_LE_518(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_LE_521(ar_0, ar_1, ar_2, ar_3, arityPad)) [ ar_1 <= 0 ]
(Comp: ?, Cost: 4) main_LE_604(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_Load_602(ar_0, ar_2 - 1, ar_1 - 1, ar_3, ar_4)) [ 0 <= i370' /\ 1 <= ar_1 /\ ar_1 - 1 = i370' /\ 0 < ar_1 /\ ar_2 - 1 = i356' ]
(Comp: 1, Cost: 0) main_NE_65(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_NE_66(ar_0, ar_1, ar_2, ar_3, arityPad)) [ ar_0 < ar_1 ]
(Comp: 1, Cost: 0) main_NE_65(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_NE_66(ar_0, ar_1, ar_2, ar_3, arityPad)) [ ar_1 < ar_0 ]
(Comp: 2, Cost: 3) main_LE_604(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_NE_611(ar_0, ar_2, 0, ar_3, ar_4)) [ ar_1 = 0 ]
(Comp: ?, Cost: 1) main_Load_602(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_LE_604(ar_0, ar_2, ar_1, ar_3, ar_4)) [ 0 <= ar_2 ]
(Comp: 1, Cost: 17) main_Load_2(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_NE_65(ar_0, ar_1, ar_2, static'1, arityPad)) [ 0 <= static'1 /\ 0 <= ar_3 /\ static''' <= ar_3 + 2 /\ 0 <= static''' /\ static'1 <= static''' + 1 ]
(Comp: 1, Cost: 2) main_NE_65(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_LE_518(ar_0, ar_0, ar_2, ar_3, arityPad)) [ ar_1 = ar_0 ]
(Comp: 2, Cost: 2) main_NE_611(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_LE_518(ar_0, 0, ar_3, ar_4, arityPad)) [ ar_1 = 0 /\ ar_2 = 0 ]
(Comp: 1, Cost: 1) main_LE_518(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_Load_602(ar_0, ar_1, ar_1, ar_2, ar_3)) [ -1 <= ar_1 /\ 0 < ar_1 /\ 1 <= ar_1 ]
(Comp: 1, Cost: 0) koat_start(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_Load_2(ar_0, ar_1, ar_2, ar_3, ar_4)) [ 0 <= 0 ]
start location: koat_start
leaf cost: 0

A polynomial rank function with
Pol(main_NE_611) = 0
Pol(main_NE_613) = 0
Pol(main_LE_518) = 3*V_2
Pol(main_LE_521) = 3*V_2
Pol(main_LE_604) = 2*V_2
Pol(main_Load_602) = 2*V_3 + 1
Pol(main_NE_65) = 3*V_2
Pol(main_NE_66) = 3*V_2
Pol(main_Load_2) = 3*V_2
Pol(koat_start) = 3*V_2
orients all transitions weakly and the transitions
main_Load_602(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_LE_604(ar_0, ar_2, ar_1, ar_3, ar_4)) [ 0 <= ar_2 ]
main_LE_604(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_Load_602(ar_0, ar_2 - 1, ar_1 - 1, ar_3, ar_4)) [ 0 <= i370' /\ 1 <= ar_1 /\ ar_1 - 1 = i370' /\ 0 < ar_1 /\ ar_2 - 1 = i356' ]
strictly and produces the following problem:
5: T:
(Comp: 1, Cost: 0) main_NE_611(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_NE_613(ar_0, ar_1, 0, ar_3, ar_4)) [ ar_2 = 0 ]
(Comp: 1, Cost: 0) main_LE_518(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_LE_521(ar_0, ar_1, ar_2, ar_3, arityPad)) [ ar_1 <= 0 ]
(Comp: 3*ar_1, Cost: 4) main_LE_604(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_Load_602(ar_0, ar_2 - 1, ar_1 - 1, ar_3, ar_4)) [ 0 <= i370' /\ 1 <= ar_1 /\ ar_1 - 1 = i370' /\ 0 < ar_1 /\ ar_2 - 1 = i356' ]
(Comp: 1, Cost: 0) main_NE_65(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_NE_66(ar_0, ar_1, ar_2, ar_3, arityPad)) [ ar_0 < ar_1 ]
(Comp: 1, Cost: 0) main_NE_65(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_NE_66(ar_0, ar_1, ar_2, ar_3, arityPad)) [ ar_1 < ar_0 ]
(Comp: 2, Cost: 3) main_LE_604(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_NE_611(ar_0, ar_2, 0, ar_3, ar_4)) [ ar_1 = 0 ]
(Comp: 3*ar_1, Cost: 1) main_Load_602(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_LE_604(ar_0, ar_2, ar_1, ar_3, ar_4)) [ 0 <= ar_2 ]
(Comp: 1, Cost: 17) main_Load_2(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_NE_65(ar_0, ar_1, ar_2, static'1, arityPad)) [ 0 <= static'1 /\ 0 <= ar_3 /\ static''' <= ar_3 + 2 /\ 0 <= static''' /\ static'1 <= static''' + 1 ]
(Comp: 1, Cost: 2) main_NE_65(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_LE_518(ar_0, ar_0, ar_2, ar_3, arityPad)) [ ar_1 = ar_0 ]
(Comp: 2, Cost: 2) main_NE_611(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_LE_518(ar_0, 0, ar_3, ar_4, arityPad)) [ ar_1 = 0 /\ ar_2 = 0 ]
(Comp: 1, Cost: 1) main_LE_518(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_Load_602(ar_0, ar_1, ar_1, ar_2, ar_3)) [ -1 <= ar_1 /\ 0 < ar_1 /\ 1 <= ar_1 ]
(Comp: 1, Cost: 0) koat_start(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_Load_2(ar_0, ar_1, ar_2, ar_3, ar_4)) [ 0 <= 0 ]
start location: koat_start
leaf cost: 0

Complexity upper bound 15*ar_1 + 30

Time: 0.265 sec (SMT: 0.229 sec)

(20) BOUNDS(CONSTANT, 30 + 15 * |#1|)

(21) 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.
Did no encode lower bounds for putfield and astore.

(22) Obligation:

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

(24) Obligation:

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

Moved arithmethic from lhss to constraints.

(26) Obligation:

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

Linearized lhss.

main_NE_65(i1, i1, env, static) -{2,2}> main_LE_518(i1, i1, env, static) :|: 0 >= 0
was transformed to
main_NE_65(i1, x, env, static) -{2,2}> main_LE_518(i1, i1, env, static) :|: 0 >= 0 && x = i1

(28) Obligation:

IntTrs with 10 rules
Start term: main_Load_2(#0, #1, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_Load_2(i1, i4, env, static) -{17,17}> main_NE_65(i1, i4, env, static'1) :|: 0 >= 0 && 0 < 2 && 0 <= static'1 && 0 <= static && 0 <= 1 && 0 < 1 && static''' <= static + 2 && 0 <= static''' && 0 <= 2 && static'1 <= static''' + 1
main_LE_604(i269, i349, i343, env, static) -{4,4}> main_Load_602(i269, i356', i370', env, static) :|: 0 <= i370' && 1 <= i349 && 0 <= i349 && i349 + -1 = i370' && 0 < i349 && i343 + -1 = i356'
main_NE_65(i1, x, env, static) -{2,2}> main_LE_518(i1, i1, env, static) :|: 0 >= 0 && x = i1
main_LE_518(i269, i276, env, static) -{0,0}> main_LE_521(i269, i276, env, static) :|: i276 <= 0
main_NE_611(i269, i371, iconst_0, env, static) -{0,0}> main_NE_613(i269, i371, iconst_0, env, static) :|: iconst_0 = 0
main_NE_611(i269, x, x', env, static) -{2,2}> main_LE_518(i269, 0, env, static) :|: 0 >= 0 && x = 0 && x' = 0
main_NE_65(i1, i4, env, static) -{0,0}> main_NE_66(i1, i4, env, static) :|: !(i1 = i4)
main_LE_518(i269, i277, env, static) -{1,1}> main_Load_602(i269, i277, i277, env, static) :|: -1 <= i277 && 0 <= i277 && 0 < i277 && 1 <= i277
main_Load_602(i269, i343, i344, env, static) -{1,1}> main_LE_604(i269, i344, i343, env, static) :|: 0 <= i344
main_LE_604(i269, x, i343, env, static) -{3,3}> main_NE_611(i269, i343, 0, env, static) :|: 0 <= 0 && x = 0

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

Removed div and mod.

(30) Obligation:

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

Moved arithmethic from constraints to rhss.

(32) Obligation:

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

Simplified expressions.

main_NE_65(i1, x, env, static) -{2,2}> main_LE_518(i1, i1, env, static) :|: 0 >= 0 && x = i1
was transformed to
main_NE_65(i1, x, env, static) -{2,2}> main_LE_518(i1, i1, env, static) :|: x = i1

main_NE_65(i1, i4, env, static) -{0,0}> main_NE_66(i1, i4, env, static) :|: i1 > i4
was transformed to
main_NE_65(i1, i4, env, static) -{0,0}> main_NE_66(i1, i4, env, static) :|: i4 < i1

(34) Obligation:

(35) TerminationGraphToComplexityProof (BOTH CONCRETE BOUNDS(ID, ADD(5)) transformation)

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

(36) Obligation:

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

Used field analysis yielded the following read fields:

Considered paths: all paths from start

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

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

(38) Obligation:

IntTrs with 49 rules
Start term: main_Load_2(#0, #1, env, static)
Considered paths: all paths from start
Rules:
main_Load_2(i1, i4, env, static) -{0,0}> main_Load_3(i1, i4, env, static) :|: 0 >= 0
main_Load_3(i1, i4, env, static) -{0,0}> langle_clinit_rangle_ConstantStackPush_6(i1, i4, env, static) :|: 0 >= 0
langle_clinit_rangle_ConstantStackPush_6(i1, i4, env, static) -{1,1}> langle_clinit_rangle_ArrayCreate_12(iconst_0, i1, i4, env, static) :|: iconst_0 = 0
langle_clinit_rangle_ArrayCreate_12(iconst_0, i1, i4, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_13(a2, i1, i4, iconst_0, env, static) :|: a2 = 2 && iconst_0 = 0 && 0 < a2
langle_clinit_rangle_FieldAccess_13(a2, i1, i4, iconst_0, env, static) -{1,1}> langle_clinit_rangle_New_14(i1, i4, env, static') :|: 0 <= a2 && iconst_0 = 0 && static' <= static + a2 && 0 <= static && 0 < a2
langle_clinit_rangle_New_14(i1, i4, env, static) -{0,0}> langle_clinit_rangle_New_16(i1, i4, env, static) :|: 0 >= 0
langle_clinit_rangle_New_16(i1, i4, env, static) -{0,0}> langle_clinit_rangle_New_17(i1, i4, env, static) :|: 0 <= static
langle_clinit_rangle_New_17(i1, i4, env, static) -{1,1}> langle_clinit_rangle_Duplicate_19(o2, i1, i4, env, static) :|: 0 < o2 && o2 = 1
langle_clinit_rangle_Duplicate_19(o2, i1, i4, env, static) -{1,1}> langle_clinit_rangle_ConstantStackPush_21(o2, i1, i4, env, static) :|: 0 < o2
langle_clinit_rangle_ConstantStackPush_21(o2, i1, i4, env, static) -{1,1}> langle_clinit_rangle_InvokeMethod_22(o2, NULL, i1, i4, env, static) :|: NULL = 0 && 0 < o2
langle_clinit_rangle_InvokeMethod_22(o2, NULL, i1, i4, env, static) -{1,1}> langle_init_rangle_Load_24(o2, i1, i4, env, static) :|: NULL = 0 && 0 < o2
langle_init_rangle_Load_24(o2, i1, i4, env, static) -{1,1}> langle_init_rangle_InvokeMethod_26(o2, i1, i4, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_26(o2, i1, i4, env, static) -{1,1}> langle_init_rangle_Load_28(o2, i1, i4, env, static) :|: 0 < o2
langle_init_rangle_Load_28(o2, i1, i4, env, static) -{1,1}> langle_init_rangle_InvokeMethod_30(o2, i1, i4, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_30(o2, i1, i4, env, static) -{1,1}> langle_init_rangle_Return_31(o2, i1, i4, env, static) :|: 0 < o2
langle_init_rangle_Return_31(o2, i1, i4, env, static) -{1,1}> langle_init_rangle_Return_32(o2, i1, i4, env, static) :|: 0 < o2
langle_init_rangle_Return_32(o2, i1, i4, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_34(o2, i1, i4, env, static) :|: 0 < o2
langle_clinit_rangle_FieldAccess_34(o2, i1, i4, env, static) -{1,1}> langle_clinit_rangle_Return_35(i1, i4, env, static') :|: 0 < o2 && 0 <= o2 && 0 <= static && static' <= static + o2
langle_clinit_rangle_Return_35(i1, i4, env, static) -{1,1}> main_Load_40(i1, i4, env, static) :|: 0 >= 0
main_Load_40(i1, i4, env, static) -{0,0}> main_Load_42(i1, i4, env, static) :|: 0 >= 0
main_Load_42(i1, i4, env, static) -{0,0}> main_Load_48(i1, i4, env, static) :|: 0 <= static
main_Load_48(i1, i4, env, static) -{0,0}> main_Load_49(i1, i4, env, static) :|: 0 >= 0
main_Load_49(i1, i4, env, static) -{0,0}> main_Load_50(i1, i4, env, static) :|: 0 >= 0
main_Load_50(i1, i4, env, static) -{1,1}> main_Load_51(i1, i4, env, static) :|: 0 >= 0
main_Load_51(i1, i4, env, static) -{1,1}> main_NE_65(i1, i4, env, static) :|: 0 >= 0
main_NE_65(i1, i4, env, static) -{0,0}> main_NE_67(i4, env, static) :|: i1 = i4
main_NE_67(i4, env, static) -{1,1}> main_Load_70(i4, env, static) :|: i4 = i4
main_Load_70(i4, env, static) -{1,1}> main_LE_72(i4, env, static) :|: 0 >= 0
main_LE_72(i4, env, static) -{0,0}> main_LE_518(i4, i4, env, static) :|: 0 >= 0
main_LE_518(i269, i277, env, static) -{0,0}> main_LE_522(i269, i277, env, static) :|: 1 <= i277
main_LE_522(i269, i277, env, static) -{1,1}> main_Load_527(i269, i277, env, static) :|: 1 <= i277 && 0 < i277
main_Load_527(i269, i277, env, static) -{0,0}> main_Load_548(i269, i277, i277, env, static) :|: 1 <= i277 && 0 <= i277
main_Load_548(i269, i283, i284, env, static) -{0,0}> main_Load_584(i269, i283, i284, env, static) :|: 0 <= i284 && -1 <= i283 && 0 <= i283
main_Load_584(i269, i313, i314, env, static) -{0,0}> main_Load_602(i269, i313, i314, env, static) :|: 0 <= i314 && -1 <= i313
main_Load_602(i269, i343, i344, env, static) -{1,1}> main_LE_604(i269, i344, i343, env, static) :|: 0 <= i344
main_LE_604(i269, iconst_0, i343, env, static) -{0,0}> main_LE_605(i269, iconst_0, i343, env, static) :|: 0 <= iconst_0 && iconst_0 = 0
main_LE_604(i269, i349, i343, env, static) -{0,0}> main_LE_606(i269, i349, i343, env, static) :|: 0 <= i349 && 1 <= i349
main_LE_605(i269, iconst_0, i343, env, static) -{1,1}> main_Load_607(i269, i343, iconst_0, env, static) :|: iconst_0 <= 0 && iconst_0 = 0
main_LE_606(i269, i349, i343, env, static) -{1,1}> main_Inc_608(i269, i343, i349, env, static) :|: 0 < i349 && 1 <= i349
main_Load_607(i269, i343, iconst_0, env, static) -{1,1}> main_Load_609(i269, i343, iconst_0, env, static) :|: iconst_0 = 0
main_Inc_608(i269, i343, i349, env, static) -{1,1}> main_Inc_610(i269, i356, i349, env, static) :|: i343 + -1 = i356 && 1 <= i349
main_Load_609(i269, i343, iconst_0, env, static) -{1,1}> main_NE_611(i269, i343, iconst_0, env, static) :|: iconst_0 = 0
main_Inc_610(i269, i356, i349, env, static) -{1,1}> main_JMP_612(i269, i356, i370, env, static) :|: 0 <= i370 && i349 + -1 = i370 && 1 <= i349
main_NE_611(i269, iconst_0, iconst_0, env, static) -{0,0}> main_NE_614(i269, iconst_0, env, static) :|: iconst_0 = 0
main_JMP_612(i269, i356, i370, env, static) -{1,1}> main_Load_615(i269, i356, i370, env, static) :|: 0 <= i370
main_NE_614(i269, iconst_0, env, static) -{1,1}> main_Load_627(i269, iconst_0, env, static) :|: iconst_0 = 0
main_Load_615(i269, i356, i370, env, static) -{0,0}> main_Load_602(i269, i356, i370, env, static) :|: 0 <= i370
main_Load_627(i269, iconst_0, env, static) -{1,1}> main_LE_629(i269, iconst_0, env, static) :|: iconst_0 = 0
main_LE_629(i269, iconst_0, env, static) -{0,0}> main_LE_518(i269, iconst_0, env, static) :|: iconst_0 = 0

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

obtained
main_Load_2(i1, i1, env, static) -{19,19}> main_LE_518(i1, i1, env, static'1) :|: 0 >= 0 && 0 < 2 && 0 <= static'1 && 0 <= static && 0 <= 1 && 0 < 1 && static''' <= static + 2 && 0 <= static''' && static'1 <= static''' + 1 && 0 <= 2
by chaining
main_Load_2(i1, i4, env, static) -{0,0}> main_Load_3(i1, i4, env, static) :|: 0 >= 0
main_Load_3(i1, i4, env, static) -{0,0}> langle_clinit_rangle_ConstantStackPush_6(i1, i4, env, static) :|: 0 >= 0
langle_clinit_rangle_ConstantStackPush_6(i1, i4, env, static) -{1,1}> langle_clinit_rangle_ArrayCreate_12(iconst_0, i1, i4, env, static) :|: iconst_0 = 0
langle_clinit_rangle_ArrayCreate_12(iconst_0, i1, i4, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_13(a2, i1, i4, iconst_0, env, static) :|: a2 = 2 && iconst_0 = 0 && 0 < a2
langle_clinit_rangle_FieldAccess_13(a2, i1, i4, iconst_0, env, static) -{1,1}> langle_clinit_rangle_New_14(i1, i4, env, static') :|: 0 <= a2 && iconst_0 = 0 && static' <= static + a2 && 0 <= static && 0 < a2
langle_clinit_rangle_New_14(i1, i4, env, static) -{0,0}> langle_clinit_rangle_New_16(i1, i4, env, static) :|: 0 >= 0
langle_clinit_rangle_New_16(i1, i4, env, static) -{0,0}> langle_clinit_rangle_New_17(i1, i4, env, static) :|: 0 <= static
langle_clinit_rangle_New_17(i1, i4, env, static) -{1,1}> langle_clinit_rangle_Duplicate_19(o2, i1, i4, env, static) :|: 0 < o2 && o2 = 1
langle_clinit_rangle_Duplicate_19(o2, i1, i4, env, static) -{1,1}> langle_clinit_rangle_ConstantStackPush_21(o2, i1, i4, env, static) :|: 0 < o2
langle_clinit_rangle_ConstantStackPush_21(o2, i1, i4, env, static) -{1,1}> langle_clinit_rangle_InvokeMethod_22(o2, NULL, i1, i4, env, static) :|: NULL = 0 && 0 < o2
langle_clinit_rangle_InvokeMethod_22(o2, NULL, i1, i4, env, static) -{1,1}> langle_init_rangle_Load_24(o2, i1, i4, env, static) :|: NULL = 0 && 0 < o2
langle_init_rangle_Load_24(o2, i1, i4, env, static) -{1,1}> langle_init_rangle_InvokeMethod_26(o2, i1, i4, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_26(o2, i1, i4, env, static) -{1,1}> langle_init_rangle_Load_28(o2, i1, i4, env, static) :|: 0 < o2
langle_init_rangle_Load_28(o2, i1, i4, env, static) -{1,1}> langle_init_rangle_InvokeMethod_30(o2, i1, i4, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_30(o2, i1, i4, env, static) -{1,1}> langle_init_rangle_Return_31(o2, i1, i4, env, static) :|: 0 < o2
langle_init_rangle_Return_31(o2, i1, i4, env, static) -{1,1}> langle_init_rangle_Return_32(o2, i1, i4, env, static) :|: 0 < o2
langle_init_rangle_Return_32(o2, i1, i4, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_34(o2, i1, i4, env, static) :|: 0 < o2
langle_clinit_rangle_FieldAccess_34(o2, i1, i4, env, static) -{1,1}> langle_clinit_rangle_Return_35(i1, i4, env, static') :|: 0 < o2 && 0 <= o2 && 0 <= static && static' <= static + o2
langle_clinit_rangle_Return_35(i1, i4, env, static) -{1,1}> main_Load_40(i1, i4, env, static) :|: 0 >= 0
main_Load_40(i1, i4, env, static) -{0,0}> main_Load_42(i1, i4, env, static) :|: 0 >= 0
main_Load_42(i1, i4, env, static) -{0,0}> main_Load_48(i1, i4, env, static) :|: 0 <= static
main_Load_48(i1, i4, env, static) -{0,0}> main_Load_49(i1, i4, env, static) :|: 0 >= 0
main_Load_49(i1, i4, env, static) -{0,0}> main_Load_50(i1, i4, env, static) :|: 0 >= 0
main_Load_50(i1, i4, env, static) -{1,1}> main_Load_51(i1, i4, env, static) :|: 0 >= 0
main_Load_51(i1, i4, env, static) -{1,1}> main_NE_65(i1, i4, env, static) :|: 0 >= 0
main_NE_65(i1, i4, env, static) -{0,0}> main_NE_67(i4, env, static) :|: i1 = i4
main_NE_67(i4, env, static) -{1,1}> main_Load_70(i4, env, static) :|: i4 = i4
main_Load_70(i4, env, static) -{1,1}> main_LE_72(i4, env, static) :|: 0 >= 0
main_LE_72(i4, env, static) -{0,0}> main_LE_518(i4, i4, env, static) :|: 0 >= 0

obtained
main_LE_604(i269, 0, 0, env, static) -{5,5}> main_LE_518(i269, 0, env, static) :|: 0 <= 0
by chaining
main_LE_604(i269, iconst_0, i343, env, static) -{0,0}> main_LE_605(i269, iconst_0, i343, env, static) :|: 0 <= iconst_0 && iconst_0 = 0
main_LE_605(i269, iconst_0, i343, env, static) -{1,1}> main_Load_607(i269, i343, iconst_0, env, static) :|: iconst_0 <= 0 && iconst_0 = 0
main_Load_607(i269, i343, iconst_0, env, static) -{1,1}> main_Load_609(i269, i343, iconst_0, env, static) :|: iconst_0 = 0
main_Load_609(i269, i343, iconst_0, env, static) -{1,1}> main_NE_611(i269, i343, iconst_0, env, static) :|: iconst_0 = 0
main_NE_611(i269, iconst_0, iconst_0, env, static) -{0,0}> main_NE_614(i269, iconst_0, env, static) :|: iconst_0 = 0
main_NE_614(i269, iconst_0, env, static) -{1,1}> main_Load_627(i269, iconst_0, env, static) :|: iconst_0 = 0
main_Load_627(i269, iconst_0, env, static) -{1,1}> main_LE_629(i269, iconst_0, env, static) :|: iconst_0 = 0
main_LE_629(i269, iconst_0, env, static) -{0,0}> main_LE_518(i269, iconst_0, env, static) :|: iconst_0 = 0

(40) Obligation:

IntTrs with 5 rules
Start term: main_Load_2(#0, #1, env, static)
Considered paths: all paths from start
Rules:
main_Load_2(i1, i1, env, static) -{19,19}> main_LE_518(i1, i1, env, static'1) :|: 0 >= 0 && 0 < 2 && 0 <= static'1 && 0 <= static && 0 <= 1 && 0 < 1 && static''' <= static + 2 && 0 <= static''' && static'1 <= static''' + 1 && 0 <= 2
main_LE_518(i269, i277, env, static) -{1,1}> main_Load_602(i269, i277, i277, env, static) :|: -1 <= i277 && 0 <= i277 && 0 < i277 && 1 <= i277
main_Load_602(i269, i343, i344, env, static) -{1,1}> main_LE_604(i269, i344, i343, env, static) :|: 0 <= i344
main_LE_604(i269, i349, i343, env, static) -{4,4}> main_Load_602(i269, i356', i370', env, static) :|: 0 <= i370' && 1 <= i349 && 0 <= i349 && i349 + -1 = i370' && 0 < i349 && i343 + -1 = i356'
main_LE_604(i269, 0, 0, env, static) -{5,5}> main_LE_518(i269, 0, env, static) :|: 0 <= 0

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

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

main_Load_2(x1, x2, x3, x4) → main_Load_2(x1, x2, x4)
main_LE_518(x1, x2, x3, x4) → main_LE_518(x2)
main_Load_602(x1, x2, x3, x4, x5) → main_Load_602(x2, x3)
main_LE_604(x1, x2, x3, x4, x5) → main_LE_604(x2, x3)

(42) Obligation:

IntTrs with 5 rules
Start term: main_Load_2(#0, #1, static)
Considered paths: all paths from start
Rules:
main_Load_2(i1, i1, static) -{19,19}> main_LE_518(i1) :|: 0 >= 0 && 0 < 2 && 0 <= static'1 && 0 <= static && 0 <= 1 && 0 < 1 && static''' <= static + 2 && 0 <= static''' && static'1 <= static''' + 1 && 0 <= 2
main_LE_518(i277) -{1,1}> main_Load_602(i277, i277) :|: -1 <= i277 && 0 <= i277 && 0 < i277 && 1 <= i277
main_Load_602(i343, i344) -{1,1}> main_LE_604(i344, i343) :|: 0 <= i344
main_LE_604(i349, i343) -{4,4}> main_Load_602(i356', i370') :|: 0 <= i370' && 1 <= i349 && 0 <= i349 && i349 + -1 = i370' && 0 < i349 && i343 + -1 = i356'
main_LE_604(0, 0) -{5,5}> main_LE_518(0) :|: 0 <= 0

(43) WeightedIntTrsDuplicateArgumentFilterProof (CONCRETE UPPER BOUND(ID) transformation)

Some arguments are removed because they are duplicates. We removed arguments according to the following replacements:

main_Load_2(x1, x2, x3) → main_Load_2(x2, x3)

(44) Obligation:

IntTrs with 5 rules
Start term: main_Load_2(#1, static)
Considered paths: all paths from start
Rules:
main_Load_2(i1, static) -{19,19}> main_LE_518(i1) :|: 0 >= 0 && 0 < 2 && 0 <= static'1 && 0 <= static && 0 <= 1 && 0 < 1 && static''' <= static + 2 && 0 <= static''' && static'1 <= static''' + 1 && 0 <= 2
main_LE_518(i277) -{1,1}> main_Load_602(i277, i277) :|: -1 <= i277 && 0 <= i277 && 0 < i277 && 1 <= i277
main_Load_602(i343, i344) -{1,1}> main_LE_604(i344, i343) :|: 0 <= i344
main_LE_604(i349, i343) -{4,4}> main_Load_602(i356', i370') :|: 0 <= i370' && 1 <= i349 && 0 <= i349 && i349 + -1 = i370' && 0 < i349 && i343 + -1 = i356'
main_LE_604(0, 0) -{5,5}> main_LE_518(0) :|: 0 <= 0

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

Moved arithmethic from lhss to constraints.

main_LE_604(0, 0) -{5,5}> main_LE_518(0) :|: 0 <= 0
was transformed to
main_LE_604(x, x') -{5,5}> main_LE_518(0) :|: 0 <= 0 && x = 0 && x' = 0

(46) Obligation:

IntTrs with 5 rules
Start term: main_Load_2(#1, static)
Considered paths: all paths from start
Rules:
main_LE_604(i349, i343) -{4,4}> main_Load_602(i356', i370') :|: 0 <= i370' && 1 <= i349 && 0 <= i349 && i349 + -1 = i370' && 0 < i349 && i343 + -1 = i356'
main_Load_2(i1, static) -{19,19}> main_LE_518(i1) :|: 0 >= 0 && 0 < 2 && 0 <= static'1 && 0 <= static && 0 <= 1 && 0 < 1 && static''' <= static + 2 && 0 <= static''' && static'1 <= static''' + 1 && 0 <= 2
main_LE_604(x, x') -{5,5}> main_LE_518(0) :|: 0 <= 0 && x = 0 && x' = 0
main_Load_602(i343, i344) -{1,1}> main_LE_604(i344, i343) :|: 0 <= i344
main_LE_518(i277) -{1,1}> main_Load_602(i277, i277) :|: -1 <= i277 && 0 <= i277 && 0 < i277 && 1 <= i277

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

Moved arithmethic from constraints to rhss.

main_LE_604(i349, i343) -{4,4}> main_Load_602(i356', i370') :|: 0 <= i370' && 1 <= i349 && 0 <= i349 && i349 + -1 = i370' && 0 < i349 && i343 + -1 = i356'
was transformed to
main_LE_604(i349, i343) -{4,4}> main_Load_602(i343 + -1, i349 + -1) :|: 0 <= i370' && 1 <= i349 && 0 <= i349 && i349 + -1 = i370' && 0 < i349 && i343 + -1 = i356'

(48) Obligation:

IntTrs with 5 rules
Start term: main_Load_2(#1, static)
Considered paths: all paths from start
Rules:
main_Load_2(i1, static) -{19,19}> main_LE_518(i1) :|: 0 >= 0 && 0 < 2 && 0 <= static'1 && 0 <= static && 0 <= 1 && 0 < 1 && static''' <= static + 2 && 0 <= static''' && static'1 <= static''' + 1 && 0 <= 2
main_LE_604(i349, i343) -{4,4}> main_Load_602(i343 + -1, i349 + -1) :|: 0 <= i370' && 1 <= i349 && 0 <= i349 && i349 + -1 = i370' && 0 < i349 && i343 + -1 = i356'
main_LE_604(x, x') -{5,5}> main_LE_518(0) :|: 0 <= 0 && x = 0 && x' = 0
main_Load_602(i343, i344) -{1,1}> main_LE_604(i344, i343) :|: 0 <= i344
main_LE_518(i277) -{1,1}> main_Load_602(i277, i277) :|: -1 <= i277 && 0 <= i277 && 0 < i277 && 1 <= i277

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

Simplified expressions.

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

main_LE_604(x, x') -{5,5}> main_LE_518(0) :|: 0 <= 0 && x = 0 && x' = 0
was transformed to
main_LE_604(x, x') -{5,5}> main_LE_518(0) :|: x = 0 && x' = 0

main_LE_604(i349, i343) -{4,4}> main_Load_602(i343 + -1, i349 + -1) :|: 0 <= i370' && 1 <= i349 && 0 <= i349 && i349 + -1 = i370' && 0 < i349 && i343 + -1 = i356'
was transformed to
main_LE_604(i349, i343) -{4,4}> main_Load_602(i343 - 1, i349 - 1) :|: 0 <= i370' && 1 <= i349 && i349 - 1 = i370' && 0 < i349 && i343 - 1 = i356'

main_LE_518(i277) -{1,1}> main_Load_602(i277, i277) :|: -1 <= i277 && 0 <= i277 && 0 < i277 && 1 <= i277
was transformed to
main_LE_518(i277) -{1,1}> main_Load_602(i277, i277) :|: -1 <= i277 && 0 < i277 && 1 <= i277

(50) Obligation:

IntTrs with 5 rules
Start term: main_Load_2(#1, static)
Considered paths: all paths from start
Rules:
main_Load_2(i1, static) -{19,19}> main_LE_518(i1) :|: 0 <= static'1 && 0 <= static && static''' <= static + 2 && 0 <= static''' && static'1 <= static''' + 1
main_LE_604(x, x') -{5,5}> main_LE_518(0) :|: x = 0 && x' = 0
main_LE_604(i349, i343) -{4,4}> main_Load_602(i343 - 1, i349 - 1) :|: 0 <= i370' && 1 <= i349 && i349 - 1 = i370' && 0 < i349 && i343 - 1 = i356'
main_Load_602(i343, i344) -{1,1}> main_LE_604(i344, i343) :|: 0 <= i344
main_LE_518(i277) -{1,1}> main_Load_602(i277, i277) :|: -1 <= i277 && 0 < i277 && 1 <= i277

(51) koat Proof (EQUIVALENT transformation)

YES(?, 15*ar_0 + 25)

Initial complexity problem:
1: T:
(Comp: ?, Cost: 19) main_Load_2(ar_0, ar_1) -> Com_1(main_LE_518(ar_0, arityPad)) [ 0 <= static'1 /\ 0 <= ar_1 /\ static''' <= ar_1 + 2 /\ 0 <= static''' /\ static'1 <= static''' + 1 ]
(Comp: ?, Cost: 5) main_LE_604(ar_0, ar_1) -> Com_1(main_LE_518(0, arityPad)) [ ar_0 = 0 /\ ar_1 = 0 ]
(Comp: ?, Cost: 4) main_LE_604(ar_0, ar_1) -> Com_1(main_Load_602(ar_1 - 1, ar_0 - 1)) [ 0 <= i370' /\ 1 <= ar_0 /\ ar_0 - 1 = i370' /\ 0 < ar_0 /\ ar_1 - 1 = i356' ]
(Comp: ?, Cost: 1) main_Load_602(ar_0, ar_1) -> Com_1(main_LE_604(ar_1, ar_0)) [ 0 <= ar_1 ]
(Comp: ?, Cost: 1) main_LE_518(ar_0, ar_1) -> Com_1(main_Load_602(ar_0, ar_0)) [ -1 <= ar_0 /\ 0 < ar_0 /\ 1 <= ar_0 ]
(Comp: 1, Cost: 0) koat_start(ar_0, ar_1) -> Com_1(main_Load_2(ar_0, ar_1)) [ 0 <= 0 ]
start location: koat_start
leaf cost: 0

Repeatedly propagating knowledge in problem 1 produces the following problem:
2: T:
(Comp: 1, Cost: 19) main_Load_2(ar_0, ar_1) -> Com_1(main_LE_518(ar_0, arityPad)) [ 0 <= static'1 /\ 0 <= ar_1 /\ static''' <= ar_1 + 2 /\ 0 <= static''' /\ static'1 <= static''' + 1 ]
(Comp: ?, Cost: 5) main_LE_604(ar_0, ar_1) -> Com_1(main_LE_518(0, arityPad)) [ ar_0 = 0 /\ ar_1 = 0 ]
(Comp: ?, Cost: 4) main_LE_604(ar_0, ar_1) -> Com_1(main_Load_602(ar_1 - 1, ar_0 - 1)) [ 0 <= i370' /\ 1 <= ar_0 /\ ar_0 - 1 = i370' /\ 0 < ar_0 /\ ar_1 - 1 = i356' ]
(Comp: ?, Cost: 1) main_Load_602(ar_0, ar_1) -> Com_1(main_LE_604(ar_1, ar_0)) [ 0 <= ar_1 ]
(Comp: 1, Cost: 1) main_LE_518(ar_0, ar_1) -> Com_1(main_Load_602(ar_0, ar_0)) [ -1 <= ar_0 /\ 0 < ar_0 /\ 1 <= ar_0 ]
(Comp: 1, Cost: 0) koat_start(ar_0, ar_1) -> Com_1(main_Load_2(ar_0, ar_1)) [ 0 <= 0 ]
start location: koat_start
leaf cost: 0

A polynomial rank function with
Pol(main_Load_602) = 1
Pol(main_LE_604) = 1
Pol(main_LE_518) = 0
and size complexities
S("koat_start(ar_0, ar_1) -> Com_1(main_Load_2(ar_0, ar_1)) [ 0 <= 0 ]", 0-0) = ar_0
S("koat_start(ar_0, ar_1) -> Com_1(main_Load_2(ar_0, ar_1)) [ 0 <= 0 ]", 0-1) = ar_1
S("main_LE_518(ar_0, ar_1) -> Com_1(main_Load_602(ar_0, ar_0)) [ -1 <= ar_0 /\\ 0 < ar_0 /\\ 1 <= ar_0 ]", 0-0) = ar_0
S("main_LE_518(ar_0, ar_1) -> Com_1(main_Load_602(ar_0, ar_0)) [ -1 <= ar_0 /\\ 0 < ar_0 /\\ 1 <= ar_0 ]", 0-1) = ar_0
S("main_Load_602(ar_0, ar_1) -> Com_1(main_LE_604(ar_1, ar_0)) [ 0 <= ar_1 ]", 0-0) = ar_0
S("main_Load_602(ar_0, ar_1) -> Com_1(main_LE_604(ar_1, ar_0)) [ 0 <= ar_1 ]", 0-1) = ?
S("main_LE_604(ar_0, ar_1) -> Com_1(main_Load_602(ar_1 - 1, ar_0 - 1)) [ 0 <= i370' /\\ 1 <= ar_0 /\\ ar_0 - 1 = i370' /\\ 0 < ar_0 /\\ ar_1 - 1 = i356' ]", 0-0) = ?
S("main_LE_604(ar_0, ar_1) -> Com_1(main_Load_602(ar_1 - 1, ar_0 - 1)) [ 0 <= i370' /\\ 1 <= ar_0 /\\ ar_0 - 1 = i370' /\\ 0 < ar_0 /\\ ar_1 - 1 = i356' ]", 0-1) = ar_0
S("main_LE_604(ar_0, ar_1) -> Com_1(main_LE_518(0, arityPad)) [ ar_0 = 0 /\\ ar_1 = 0 ]", 0-0) = 0
S("main_LE_604(ar_0, ar_1) -> Com_1(main_LE_518(0, arityPad)) [ ar_0 = 0 /\\ ar_1 = 0 ]", 0-1) = ?
S("main_Load_2(ar_0, ar_1) -> Com_1(main_LE_518(ar_0, arityPad)) [ 0 <= static'1 /\\ 0 <= ar_1 /\\ static''' <= ar_1 + 2 /\\ 0 <= static''' /\\ static'1 <= static''' + 1 ]", 0-0) = ar_0
S("main_Load_2(ar_0, ar_1) -> Com_1(main_LE_518(ar_0, arityPad)) [ 0 <= static'1 /\\ 0 <= ar_1 /\\ static''' <= ar_1 + 2 /\\ 0 <= static''' /\\ static'1 <= static''' + 1 ]", 0-1) = ?
orients the transitions
main_Load_602(ar_0, ar_1) -> Com_1(main_LE_604(ar_1, ar_0)) [ 0 <= ar_1 ]
main_LE_604(ar_0, ar_1) -> Com_1(main_Load_602(ar_1 - 1, ar_0 - 1)) [ 0 <= i370' /\ 1 <= ar_0 /\ ar_0 - 1 = i370' /\ 0 < ar_0 /\ ar_1 - 1 = i356' ]
main_LE_604(ar_0, ar_1) -> Com_1(main_LE_518(0, arityPad)) [ ar_0 = 0 /\ ar_1 = 0 ]
weakly and the transition
main_LE_604(ar_0, ar_1) -> Com_1(main_LE_518(0, arityPad)) [ ar_0 = 0 /\ ar_1 = 0 ]
strictly and produces the following problem:
3: T:
(Comp: 1, Cost: 19) main_Load_2(ar_0, ar_1) -> Com_1(main_LE_518(ar_0, arityPad)) [ 0 <= static'1 /\ 0 <= ar_1 /\ static''' <= ar_1 + 2 /\ 0 <= static''' /\ static'1 <= static''' + 1 ]
(Comp: 1, Cost: 5) main_LE_604(ar_0, ar_1) -> Com_1(main_LE_518(0, arityPad)) [ ar_0 = 0 /\ ar_1 = 0 ]
(Comp: ?, Cost: 4) main_LE_604(ar_0, ar_1) -> Com_1(main_Load_602(ar_1 - 1, ar_0 - 1)) [ 0 <= i370' /\ 1 <= ar_0 /\ ar_0 - 1 = i370' /\ 0 < ar_0 /\ ar_1 - 1 = i356' ]
(Comp: ?, Cost: 1) main_Load_602(ar_0, ar_1) -> Com_1(main_LE_604(ar_1, ar_0)) [ 0 <= ar_1 ]
(Comp: 1, Cost: 1) main_LE_518(ar_0, ar_1) -> Com_1(main_Load_602(ar_0, ar_0)) [ -1 <= ar_0 /\ 0 < ar_0 /\ 1 <= ar_0 ]
(Comp: 1, Cost: 0) koat_start(ar_0, ar_1) -> Com_1(main_Load_2(ar_0, ar_1)) [ 0 <= 0 ]
start location: koat_start
leaf cost: 0

A polynomial rank function with
Pol(main_Load_2) = 3*V_1
Pol(main_LE_518) = 3*V_1
Pol(main_LE_604) = 2*V_1
Pol(main_Load_602) = 2*V_2 + 1
Pol(koat_start) = 3*V_1
orients all transitions weakly and the transitions
main_Load_602(ar_0, ar_1) -> Com_1(main_LE_604(ar_1, ar_0)) [ 0 <= ar_1 ]
main_LE_604(ar_0, ar_1) -> Com_1(main_Load_602(ar_1 - 1, ar_0 - 1)) [ 0 <= i370' /\ 1 <= ar_0 /\ ar_0 - 1 = i370' /\ 0 < ar_0 /\ ar_1 - 1 = i356' ]
strictly and produces the following problem:
4: T:
(Comp: 1, Cost: 19) main_Load_2(ar_0, ar_1) -> Com_1(main_LE_518(ar_0, arityPad)) [ 0 <= static'1 /\ 0 <= ar_1 /\ static''' <= ar_1 + 2 /\ 0 <= static''' /\ static'1 <= static''' + 1 ]
(Comp: 1, Cost: 5) main_LE_604(ar_0, ar_1) -> Com_1(main_LE_518(0, arityPad)) [ ar_0 = 0 /\ ar_1 = 0 ]
(Comp: 3*ar_0, Cost: 4) main_LE_604(ar_0, ar_1) -> Com_1(main_Load_602(ar_1 - 1, ar_0 - 1)) [ 0 <= i370' /\ 1 <= ar_0 /\ ar_0 - 1 = i370' /\ 0 < ar_0 /\ ar_1 - 1 = i356' ]
(Comp: 3*ar_0, Cost: 1) main_Load_602(ar_0, ar_1) -> Com_1(main_LE_604(ar_1, ar_0)) [ 0 <= ar_1 ]
(Comp: 1, Cost: 1) main_LE_518(ar_0, ar_1) -> Com_1(main_Load_602(ar_0, ar_0)) [ -1 <= ar_0 /\ 0 < ar_0 /\ 1 <= ar_0 ]
(Comp: 1, Cost: 0) koat_start(ar_0, ar_1) -> Com_1(main_Load_2(ar_0, ar_1)) [ 0 <= 0 ]
start location: koat_start
leaf cost: 0

Complexity upper bound 15*ar_0 + 25

Time: 0.098 sec (SMT: 0.089 sec)

(0) Obligation:

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

(2) Obligation:

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

(4) Obligation:

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

(6) Obligation:

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

(8) Obligation:

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

(10) Obligation:

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

(12) Obligation:

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

(14) Obligation:

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

(16) Obligation:

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

(18) Obligation:

(19) koat Proof (EQUIVALENT transformation)

(20) BOUNDS(CONSTANT, 30 + 15 * |#1|)

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

(22) Obligation:

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

(24) Obligation:

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

(26) Obligation:

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

(28) Obligation:

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

(30) Obligation:

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

(32) Obligation:

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

(34) Obligation:

(35) TerminationGraphToComplexityProof (BOTH CONCRETE BOUNDS(ID, ADD(5)) transformation)

(36) Obligation:

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

(38) Obligation:

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

(40) Obligation:

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

(42) Obligation:

(43) WeightedIntTrsDuplicateArgumentFilterProof (CONCRETE UPPER BOUND(ID) transformation)

(44) Obligation:

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

(46) Obligation:

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

(48) Obligation:

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

(50) Obligation:

(51) koat Proof (EQUIVALENT transformation)

(52) BOUNDS(CONSTANT, 25 + 15 * |#1|)