time complexity proof of /tmp/tmpNfdNsx/Et2.jar

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

0 JBC problem

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

↳2 JBCTerminationGraph

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

↳4 JBCComplexityEdges

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

    ↳6 WeightedIntTrs

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

        ↳8 WeightedIntTrs

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

        ↳10 WeightedIntTrs

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

        ↳12 WeightedIntTrs

    ↳13 JBCGraphEdgesToCpxIntTrsProof (CONCRETE UPPER BOUND(ID), 104 ms)

    ↳14 WeightedIntTrs

        ↳15 StraightLineCodeCompressionProof (BOTH CONCRETE BOUNDS(ID, ID), 44 ms)

        ↳16 WeightedIntTrs

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

        ↳18 WeightedIntTrs

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

        ↳20 WeightedIntTrs

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

↳22 JBCComplexityEdges

    ↳23 JBCGraphEdgesToCpxIntTrsProof (CONCRETE UPPER BOUND(ID), 59 ms)

    ↳24 WeightedIntTrs

    ↳25 StraightLineCodeCompressionProof (BOTH CONCRETE BOUNDS(ID, ID), 10 ms)

    ↳26 WeightedIntTrs

    ↳27 WeightedIntTrsUnneededArgumentFilterProof (CONCRETE UPPER BOUND(ID), 19 ms)

    ↳28 WeightedIntTrs

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

    ↳30 WeightedIntTrs

    ↳31 ExpressionSimplificationProof (BOTH CONCRETE BOUNDS(ID, ID), 2 ms)

    ↳32 WeightedIntTrs

    ↳33 koat Proof (⇔, 604 ms)

    ↳34 BOUNDS(CONSTANT, 23 + 47 * |#0|)

(0) Obligation:

Need to prove time_complexity of the following program:

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

// bin(entry593(C,D),[1*C+ -1*B>=1,1*C+ -1*A>=1,1*D>=1],entry593(A,B))

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

Constructed TerminationGraph.

(2) Obligation:

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

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

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

(4) Obligation:

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

(6) Obligation:

IntTrs with 79 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_3(i1, i3, env, static) :|: 0 >= 0
main_Load_3(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_15(iconst_0, i1, i3, env, static) :|: iconst_0 = 0
langle_clinit_rangle_ArrayCreate_15(iconst_0, i1, i3, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_16(a2, i1, i3, iconst_0, env, static) :|: a2 = 2 && iconst_0 = 0 && 0 < a2
langle_clinit_rangle_FieldAccess_16(a2, i1, i3, iconst_0, env, static) -{1,1}> langle_clinit_rangle_New_18(i1, i3, env, static') :|: 0 <= a2 && iconst_0 = 0 && static' <= static + a2 && 0 <= static && 0 < a2
langle_clinit_rangle_New_18(i1, i3, env, static) -{0,0}> langle_clinit_rangle_New_19(i1, i3, env, static) :|: 0 >= 0
langle_clinit_rangle_New_19(i1, i3, env, static) -{0,0}> langle_clinit_rangle_New_21(i1, i3, env, static) :|: 0 <= static
langle_clinit_rangle_New_21(i1, i3, env, static) -{1,1}> langle_clinit_rangle_Duplicate_23(o2, i1, i3, env, static) :|: 0 < o2 && o2 = 1
langle_clinit_rangle_Duplicate_23(o2, i1, i3, env, static) -{1,1}> langle_clinit_rangle_ConstantStackPush_25(o2, i1, i3, env, static) :|: 0 < o2
langle_clinit_rangle_ConstantStackPush_25(o2, i1, i3, env, static) -{1,1}> langle_clinit_rangle_InvokeMethod_28(o2, NULL, i1, i3, env, static) :|: NULL = 0 && 0 < o2
langle_clinit_rangle_InvokeMethod_28(o2, NULL, i1, i3, env, static) -{1,1}> langle_init_rangle_Load_30(o2, i1, i3, env, static) :|: NULL = 0 && 0 < o2
langle_init_rangle_Load_30(o2, i1, i3, env, static) -{1,1}> langle_init_rangle_InvokeMethod_34(o2, i1, i3, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_34(o2, i1, i3, env, static) -{1,1}> langle_init_rangle_Load_35(o2, i1, i3, env, static) :|: 0 < o2
langle_init_rangle_Load_35(o2, i1, i3, env, static) -{1,1}> langle_init_rangle_InvokeMethod_37(o2, i1, i3, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_37(o2, i1, i3, env, static) -{1,1}> langle_init_rangle_Return_41(o2, i1, i3, env, static) :|: 0 < o2
langle_init_rangle_Return_41(o2, i1, i3, env, static) -{1,1}> langle_init_rangle_Return_42(o2, i1, i3, env, static) :|: 0 < o2
langle_init_rangle_Return_42(o2, i1, i3, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_43(o2, i1, i3, env, static) :|: 0 < o2
langle_clinit_rangle_FieldAccess_43(o2, i1, i3, env, static) -{1,1}> langle_clinit_rangle_Return_44(i1, i3, env, static') :|: 0 < o2 && 0 <= o2 && 0 <= static && static' <= static + o2
langle_clinit_rangle_Return_44(i1, i3, env, static) -{1,1}> main_Load_47(i1, i3, env, static) :|: 0 >= 0
main_Load_47(i1, i3, env, static) -{0,0}> main_Load_48(i1, i3, env, static) :|: 0 >= 0
main_Load_48(i1, i3, env, static) -{0,0}> main_Load_50(i1, i3, env, static) :|: 0 <= static
main_Load_50(i1, i3, env, static) -{0,0}> main_Load_52(i1, i3, env, static) :|: 0 >= 0
main_Load_52(i1, i3, env, static) -{0,0}> main_Load_53(i1, i3, env, static) :|: 0 >= 0
main_Load_53(i1, i3, env, static) -{0,0}> main_Load_190(i1, i3, i1, i3, env, static) :|: 0 >= 0
main_Load_190(i1, i63, i64, i65, env, static) -{0,0}> main_Load_347(i1, i63, i64, i65, env, static) :|: 0 >= 0
main_Load_347(i1, i63, i121, i104, env, static) -{0,0}> main_Load_474(i1, i63, i121, i104, env, static) :|: 0 >= 0
main_Load_474(i1, i63, i186, i175, env, static) -{0,0}> main_Load_587(i1, i63, i186, i175, env, static) :|: 0 >= 0
main_Load_587(i1, i63, i237, i222, env, static) -{0,0}> main_Load_718(i1, i63, i237, i222, env, static) :|: 0 >= 0
main_Load_718(i1, i63, i292, i285, env, static) -{0,0}> main_Load_807(i1, i63, i292, i285, env, static) :|: 0 >= 0
main_Load_807(i1, i63, i332, i322, env, static) -{0,0}> main_Load_932(i1, i63, i332, i322, env, static) :|: 0 >= 0
main_Load_932(i1, i63, i386, i371, env, static) -{0,0}> main_Load_1039(i1, i63, i386, i371, env, static) :|: 0 >= 0
main_Load_1039(i1, i63, i437, i424, env, static) -{0,0}> main_Load_1148(i1, i63, i437, i424, env, static) :|: 0 >= 0
main_Load_1148(i1, i63, i484, i471, env, static) -{0,0}> main_Load_1261(i1, i63, i484, i471, env, static) :|: 0 >= 0
main_Load_1261(i1, i63, i531, i518, env, static) -{0,0}> main_Load_1373(i1, i63, i531, i518, env, static) :|: 0 >= 0
main_Load_1373(i1, i63, i584, i565, env, static) -{0,0}> main_Load_1498(i1, i63, i584, i565, env, static) :|: 0 >= 0
main_Load_1498(i1, i63, i636, i615, env, static) -{0,0}> main_Load_1610(i1, i63, i636, i615, env, static) :|: 0 >= 0
main_Load_1610(i1, i63, i687, i673, env, static) -{1,1}> main_LE_1616(i1, i63, i673, i687, env, static) :|: 0 >= 0
main_LE_1616(i1, i63, i703, i687, env, static) -{0,0}> main_LE_1618(i1, i63, i703, i687, env, static) :|: i703 <= 0
main_LE_1616(i1, i63, i704, i687, env, static) -{0,0}> main_LE_1619(i1, i63, i704, i687, env, static) :|: 1 <= i704
main_LE_1619(i1, i63, i704, i687, env, static) -{1,1}> main_New_1623(i1, i63, i687, env, static) :|: 1 <= i704 && 0 < i704
main_New_1623(i1, i63, i687, env, static) -{1,1}> main_Duplicate_1626(i1, i63, o208, i687, env, static) :|: o208 = 1 && 0 < o208
main_Duplicate_1626(i1, i63, o208, i687, env, static) -{1,1}> main_InvokeMethod_1628(i1, i63, o208, i687, env, static) :|: 0 < o208
main_InvokeMethod_1628(i1, i63, o208, i687, env, static) -{1,1}> main_InvokeMethod_1631(i1, i63, o208, i687, env, static) :|: 0 < o208
main_InvokeMethod_1631(i1, i63, o208, i687, env, static) -{1,1}> main_Store_1633(i1, i63, i709, i687, env, static) :|: 0 < o208
main_Store_1633(i1, i63, i709, i687, env, static) -{1,1}> main_Load_1635(i1, i63, i687, i709, env, static) :|: 0 >= 0
main_Load_1635(i1, i63, i687, i709, env, static) -{1,1}> main_GE_1638(i1, i63, i709, i687, env, static) :|: 0 >= 0
main_GE_1638(i1, i63, i715, i687, env, static) -{0,0}> main_GE_1640(i1, i63, i715, i687, env, static) :|: i715 <= -1
main_GE_1638(i1, i63, i716, i687, env, static) -{0,0}> main_GE_1641(i1, i63, i716, i687, env, static) :|: 0 <= i716
main_GE_1640(i1, i63, i715, i687, env, static) -{1,1}> main_Load_1643(i1, i63, i687, i715, env, static) :|: i715 < 0 && i715 <= -1
main_GE_1641(i1, i63, i716, i687, env, static) -{1,1}> main_Load_1645(i1, i63, i687, i716, env, static) :|: 0 <= i716
main_Load_1643(i1, i63, i687, i715, env, static) -{1,1}> main_IntArithmetic_1647(i1, i63, i715, i687, env, static) :|: i715 <= -1
main_Load_1645(i1, i63, i687, i716, env, static) -{1,1}> main_ConstantStackPush_1649(i1, i63, i687, i716, env, static) :|: 0 <= i716
main_IntArithmetic_1647(i1, i63, i715, i687, env, static) -{1,1}> main_Store_1651(i1, i63, i717, i687, env, static) :|: -i715 = i717 && i715 <= -1 && 1 <= i717
main_ConstantStackPush_1649(i1, i63, i687, i716, env, static) -{1,1}> main_IntArithmetic_1653(i1, i63, i687, iconst_1, i716, env, static) :|: iconst_1 = 1 && 0 <= i716
main_Store_1651(i1, i63, i717, i687, env, static) -{1,1}> main_Load_1658(i1, i63, i687, i717, env, static) :|: 1 <= i717
main_IntArithmetic_1653(i1, i63, i687, iconst_1, i716, env, static) -{1,1}> main_Load_1672(i1, i63, i718, i687, i716, env, static) :|: i687 - iconst_1 = i718 && iconst_1 = 1 && 0 <= i716
main_Load_1658(i1, i63, i687, i717, env, static) -{1,1}> main_ConstantStackPush_1676(i1, i63, i687, i717, env, static) :|: 1 <= i717
main_Load_1672(i1, i63, i718, i687, i716, env, static) -{1,1}> main_IntArithmetic_1678(i1, i63, i718, i716, i687, env, static) :|: 0 <= i716
main_ConstantStackPush_1676(i1, i63, i687, i717, env, static) -{1,1}> main_IntArithmetic_1682(i1, i63, i687, iconst_1, i717, env, static) :|: iconst_1 = 1 && 1 <= i717
main_IntArithmetic_1678(i1, i63, i718, i716, i687, env, static) -{1,1}> main_Store_1683(i1, i63, i720, i687, i716, env, static) :|: i718 - i716 = i720 && 0 <= i716
main_IntArithmetic_1682(i1, i63, i687, iconst_1, i717, env, static) -{1,1}> main_Load_1688(i1, i63, i722, i687, i717, env, static) :|: i687 - iconst_1 = i722 && iconst_1 = 1 && 1 <= i717
main_Store_1683(i1, i63, i720, i687, i716, env, static) -{1,1}> main_Load_1690(i1, i63, i687, i720, i716, env, static) :|: 0 <= i716
main_Load_1688(i1, i63, i722, i687, i717, env, static) -{1,1}> main_IntArithmetic_1693(i1, i63, i722, i717, i687, env, static) :|: 1 <= i717
main_Load_1690(i1, i63, i687, i720, i716, env, static) -{1,1}> main_ConstantStackPush_1695(i1, i63, i687, i720, i716, env, static) :|: 0 <= i716
main_IntArithmetic_1693(i1, i63, i722, i717, i687, env, static) -{1,1}> main_Store_1698(i1, i63, i727, i687, i717, env, static) :|: i722 - i717 = i727 && 1 <= i717
main_ConstantStackPush_1695(i1, i63, i687, i720, i716, env, static) -{1,1}> main_IntArithmetic_1700(i1, i63, i687, iconst_1, i720, i716, env, static) :|: iconst_1 = 1 && 0 <= i716
main_Store_1698(i1, i63, i727, i687, i717, env, static) -{1,1}> main_Load_1703(i1, i63, i687, i727, i717, env, static) :|: 1 <= i717
main_IntArithmetic_1700(i1, i63, i687, iconst_1, i720, i716, env, static) -{1,1}> main_Load_1705(i1, i63, i731, i720, i716, env, static) :|: i687 - iconst_1 = i731 && iconst_1 = 1 && 0 <= i716
main_Load_1703(i1, i63, i687, i727, i717, env, static) -{1,1}> main_ConstantStackPush_1708(i1, i63, i687, i727, i717, env, static) :|: 1 <= i717
main_Load_1705(i1, i63, i731, i720, i716, env, static) -{1,1}> main_IntArithmetic_1710(i1, i63, i731, i716, i720, env, static) :|: 0 <= i716
main_ConstantStackPush_1708(i1, i63, i687, i727, i717, env, static) -{1,1}> main_IntArithmetic_1714(i1, i63, i687, iconst_1, i727, i717, env, static) :|: iconst_1 = 1 && 1 <= i717
main_IntArithmetic_1710(i1, i63, i731, i716, i720, env, static) -{1,1}> main_Store_1716(i1, i63, i737, i720, env, static) :|: i731 - i716 = i737 && 0 <= i716
main_IntArithmetic_1714(i1, i63, i687, iconst_1, i727, i717, env, static) -{1,1}> main_Load_1719(i1, i63, i739, i727, i717, env, static) :|: i687 - iconst_1 = i739 && iconst_1 = 1 && 1 <= i717
main_Store_1716(i1, i63, i737, i720, env, static) -{1,1}> main_JMP_1721(i1, i63, i737, i720, env, static) :|: 0 >= 0
main_Load_1719(i1, i63, i739, i727, i717, env, static) -{1,1}> main_IntArithmetic_1723(i1, i63, i739, i717, i727, env, static) :|: 1 <= i717
main_JMP_1721(i1, i63, i737, i720, env, static) -{1,1}> main_Load_1730(i1, i63, i737, i720, env, static) :|: 0 >= 0
main_IntArithmetic_1723(i1, i63, i739, i717, i727, env, static) -{1,1}> main_Store_1736(i1, i63, i749, i727, env, static) :|: 1 <= i717 && i739 - i717 = i749
main_Load_1730(i1, i63, i737, i720, env, static) -{0,0}> main_Load_1610(i1, i63, i737, i720, env, static) :|: 0 >= 0
main_Store_1736(i1, i63, i749, i727, env, static) -{0,0}> main_Store_1716(i1, i63, i749, i727, env, static) :|: 0 >= 0

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

obtained
main_Load_1(i1, i3, env, static) -{15,15}> main_Load_1610(i1, i3, 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_3(i1, i3, env, static) :|: 0 >= 0
main_Load_3(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_15(iconst_0, i1, i3, env, static) :|: iconst_0 = 0
langle_clinit_rangle_ArrayCreate_15(iconst_0, i1, i3, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_16(a2, i1, i3, iconst_0, env, static) :|: a2 = 2 && iconst_0 = 0 && 0 < a2
langle_clinit_rangle_FieldAccess_16(a2, i1, i3, iconst_0, env, static) -{1,1}> langle_clinit_rangle_New_18(i1, i3, env, static') :|: 0 <= a2 && iconst_0 = 0 && static' <= static + a2 && 0 <= static && 0 < a2
langle_clinit_rangle_New_18(i1, i3, env, static) -{0,0}> langle_clinit_rangle_New_19(i1, i3, env, static) :|: 0 >= 0
langle_clinit_rangle_New_19(i1, i3, env, static) -{0,0}> langle_clinit_rangle_New_21(i1, i3, env, static) :|: 0 <= static
langle_clinit_rangle_New_21(i1, i3, env, static) -{1,1}> langle_clinit_rangle_Duplicate_23(o2, i1, i3, env, static) :|: 0 < o2 && o2 = 1
langle_clinit_rangle_Duplicate_23(o2, i1, i3, env, static) -{1,1}> langle_clinit_rangle_ConstantStackPush_25(o2, i1, i3, env, static) :|: 0 < o2
langle_clinit_rangle_ConstantStackPush_25(o2, i1, i3, env, static) -{1,1}> langle_clinit_rangle_InvokeMethod_28(o2, NULL, i1, i3, env, static) :|: NULL = 0 && 0 < o2
langle_clinit_rangle_InvokeMethod_28(o2, NULL, i1, i3, env, static) -{1,1}> langle_init_rangle_Load_30(o2, i1, i3, env, static) :|: NULL = 0 && 0 < o2
langle_init_rangle_Load_30(o2, i1, i3, env, static) -{1,1}> langle_init_rangle_InvokeMethod_34(o2, i1, i3, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_34(o2, i1, i3, env, static) -{1,1}> langle_init_rangle_Load_35(o2, i1, i3, env, static) :|: 0 < o2
langle_init_rangle_Load_35(o2, i1, i3, env, static) -{1,1}> langle_init_rangle_InvokeMethod_37(o2, i1, i3, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_37(o2, i1, i3, env, static) -{1,1}> langle_init_rangle_Return_41(o2, i1, i3, env, static) :|: 0 < o2
langle_init_rangle_Return_41(o2, i1, i3, env, static) -{1,1}> langle_init_rangle_Return_42(o2, i1, i3, env, static) :|: 0 < o2
langle_init_rangle_Return_42(o2, i1, i3, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_43(o2, i1, i3, env, static) :|: 0 < o2
langle_clinit_rangle_FieldAccess_43(o2, i1, i3, env, static) -{1,1}> langle_clinit_rangle_Return_44(i1, i3, env, static') :|: 0 < o2 && 0 <= o2 && 0 <= static && static' <= static + o2
langle_clinit_rangle_Return_44(i1, i3, env, static) -{1,1}> main_Load_47(i1, i3, env, static) :|: 0 >= 0
main_Load_47(i1, i3, env, static) -{0,0}> main_Load_48(i1, i3, env, static) :|: 0 >= 0
main_Load_48(i1, i3, env, static) -{0,0}> main_Load_50(i1, i3, env, static) :|: 0 <= static
main_Load_50(i1, i3, env, static) -{0,0}> main_Load_52(i1, i3, env, static) :|: 0 >= 0
main_Load_52(i1, i3, env, static) -{0,0}> main_Load_53(i1, i3, env, static) :|: 0 >= 0
main_Load_53(i1, i3, env, static) -{0,0}> main_Load_190(i1, i3, i1, i3, env, static) :|: 0 >= 0
main_Load_190(i1, i63, i64, i65, env, static) -{0,0}> main_Load_347(i1, i63, i64, i65, env, static) :|: 0 >= 0
main_Load_347(i1, i63, i121, i104, env, static) -{0,0}> main_Load_474(i1, i63, i121, i104, env, static) :|: 0 >= 0
main_Load_474(i1, i63, i186, i175, env, static) -{0,0}> main_Load_587(i1, i63, i186, i175, env, static) :|: 0 >= 0
main_Load_587(i1, i63, i237, i222, env, static) -{0,0}> main_Load_718(i1, i63, i237, i222, env, static) :|: 0 >= 0
main_Load_718(i1, i63, i292, i285, env, static) -{0,0}> main_Load_807(i1, i63, i292, i285, env, static) :|: 0 >= 0
main_Load_807(i1, i63, i332, i322, env, static) -{0,0}> main_Load_932(i1, i63, i332, i322, env, static) :|: 0 >= 0
main_Load_932(i1, i63, i386, i371, env, static) -{0,0}> main_Load_1039(i1, i63, i386, i371, env, static) :|: 0 >= 0
main_Load_1039(i1, i63, i437, i424, env, static) -{0,0}> main_Load_1148(i1, i63, i437, i424, env, static) :|: 0 >= 0
main_Load_1148(i1, i63, i484, i471, env, static) -{0,0}> main_Load_1261(i1, i63, i484, i471, env, static) :|: 0 >= 0
main_Load_1261(i1, i63, i531, i518, env, static) -{0,0}> main_Load_1373(i1, i63, i531, i518, env, static) :|: 0 >= 0
main_Load_1373(i1, i63, i584, i565, env, static) -{0,0}> main_Load_1498(i1, i63, i584, i565, env, static) :|: 0 >= 0
main_Load_1498(i1, i63, i636, i615, env, static) -{0,0}> main_Load_1610(i1, i63, i636, i615, env, static) :|: 0 >= 0

obtained
main_LE_1616(i1, i63, i704, i687, env, static) -{7,7}> main_GE_1638(i1, i63, i709', i687, env, static) :|: 0 >= 0 && 1 <= i704 && 0 < 1 && 0 < i704
by chaining
main_LE_1616(i1, i63, i704, i687, env, static) -{0,0}> main_LE_1619(i1, i63, i704, i687, env, static) :|: 1 <= i704
main_LE_1619(i1, i63, i704, i687, env, static) -{1,1}> main_New_1623(i1, i63, i687, env, static) :|: 1 <= i704 && 0 < i704
main_New_1623(i1, i63, i687, env, static) -{1,1}> main_Duplicate_1626(i1, i63, o208, i687, env, static) :|: o208 = 1 && 0 < o208
main_Duplicate_1626(i1, i63, o208, i687, env, static) -{1,1}> main_InvokeMethod_1628(i1, i63, o208, i687, env, static) :|: 0 < o208
main_InvokeMethod_1628(i1, i63, o208, i687, env, static) -{1,1}> main_InvokeMethod_1631(i1, i63, o208, i687, env, static) :|: 0 < o208
main_InvokeMethod_1631(i1, i63, o208, i687, env, static) -{1,1}> main_Store_1633(i1, i63, i709, i687, env, static) :|: 0 < o208
main_Store_1633(i1, i63, i709, i687, env, static) -{1,1}> main_Load_1635(i1, i63, i687, i709, env, static) :|: 0 >= 0
main_Load_1635(i1, i63, i687, i709, env, static) -{1,1}> main_GE_1638(i1, i63, i709, i687, env, static) :|: 0 >= 0

obtained
main_GE_1638(i1, i63, i716, i687, env, static) -{12,12}> main_Store_1716(i1, i63, i737', i720', env, static) :|: i687 - 1 = i718' && i731' - i716 = i737' && 0 <= i716 && i718' - i716 = i720' && i687 - 1 = i731'
by chaining
main_GE_1638(i1, i63, i716, i687, env, static) -{0,0}> main_GE_1641(i1, i63, i716, i687, env, static) :|: 0 <= i716
main_GE_1641(i1, i63, i716, i687, env, static) -{1,1}> main_Load_1645(i1, i63, i687, i716, env, static) :|: 0 <= i716
main_Load_1645(i1, i63, i687, i716, env, static) -{1,1}> main_ConstantStackPush_1649(i1, i63, i687, i716, env, static) :|: 0 <= i716
main_ConstantStackPush_1649(i1, i63, i687, i716, env, static) -{1,1}> main_IntArithmetic_1653(i1, i63, i687, iconst_1, i716, env, static) :|: iconst_1 = 1 && 0 <= i716
main_IntArithmetic_1653(i1, i63, i687, iconst_1, i716, env, static) -{1,1}> main_Load_1672(i1, i63, i718, i687, i716, env, static) :|: i687 - iconst_1 = i718 && iconst_1 = 1 && 0 <= i716
main_Load_1672(i1, i63, i718, i687, i716, env, static) -{1,1}> main_IntArithmetic_1678(i1, i63, i718, i716, i687, env, static) :|: 0 <= i716
main_IntArithmetic_1678(i1, i63, i718, i716, i687, env, static) -{1,1}> main_Store_1683(i1, i63, i720, i687, i716, env, static) :|: i718 - i716 = i720 && 0 <= i716
main_Store_1683(i1, i63, i720, i687, i716, env, static) -{1,1}> main_Load_1690(i1, i63, i687, i720, i716, env, static) :|: 0 <= i716
main_Load_1690(i1, i63, i687, i720, i716, env, static) -{1,1}> main_ConstantStackPush_1695(i1, i63, i687, i720, i716, env, static) :|: 0 <= i716
main_ConstantStackPush_1695(i1, i63, i687, i720, i716, env, static) -{1,1}> main_IntArithmetic_1700(i1, i63, i687, iconst_1, i720, i716, env, static) :|: iconst_1 = 1 && 0 <= i716
main_IntArithmetic_1700(i1, i63, i687, iconst_1, i720, i716, env, static) -{1,1}> main_Load_1705(i1, i63, i731, i720, i716, env, static) :|: i687 - iconst_1 = i731 && iconst_1 = 1 && 0 <= i716
main_Load_1705(i1, i63, i731, i720, i716, env, static) -{1,1}> main_IntArithmetic_1710(i1, i63, i731, i716, i720, env, static) :|: 0 <= i716
main_IntArithmetic_1710(i1, i63, i731, i716, i720, env, static) -{1,1}> main_Store_1716(i1, i63, i737, i720, env, static) :|: i731 - i716 = i737 && 0 <= i716

obtained
main_Store_1716(i1, i63, i737, i720, env, static) -{2,2}> main_Load_1610(i1, i63, i737, i720, env, static) :|: 0 >= 0
by chaining
main_Store_1716(i1, i63, i737, i720, env, static) -{1,1}> main_JMP_1721(i1, i63, i737, i720, env, static) :|: 0 >= 0
main_JMP_1721(i1, i63, i737, i720, env, static) -{1,1}> main_Load_1730(i1, i63, i737, i720, env, static) :|: 0 >= 0
main_Load_1730(i1, i63, i737, i720, env, static) -{0,0}> main_Load_1610(i1, i63, i737, i720, env, static) :|: 0 >= 0

obtained
main_GE_1638(i1, i63, i715, i687, env, static) -{15,15}> main_Store_1716(i1, i63, i749', i727', env, static) :|: 0 >= 0 && -i715 = i717' && i687 - 1 = i722' && i715 <= -1 && i687 - 1 = i739' && i715 < 0 && i739' - i717' = i749' && i722' - i717' = i727' && 1 <= i717'
by chaining
main_GE_1638(i1, i63, i715, i687, env, static) -{0,0}> main_GE_1640(i1, i63, i715, i687, env, static) :|: i715 <= -1
main_GE_1640(i1, i63, i715, i687, env, static) -{1,1}> main_Load_1643(i1, i63, i687, i715, env, static) :|: i715 < 0 && i715 <= -1
main_Load_1643(i1, i63, i687, i715, env, static) -{1,1}> main_IntArithmetic_1647(i1, i63, i715, i687, env, static) :|: i715 <= -1
main_IntArithmetic_1647(i1, i63, i715, i687, env, static) -{1,1}> main_Store_1651(i1, i63, i717, i687, env, static) :|: -i715 = i717 && i715 <= -1 && 1 <= i717
main_Store_1651(i1, i63, i717, i687, env, static) -{1,1}> main_Load_1658(i1, i63, i687, i717, env, static) :|: 1 <= i717
main_Load_1658(i1, i63, i687, i717, env, static) -{1,1}> main_ConstantStackPush_1676(i1, i63, i687, i717, env, static) :|: 1 <= i717
main_ConstantStackPush_1676(i1, i63, i687, i717, env, static) -{1,1}> main_IntArithmetic_1682(i1, i63, i687, iconst_1, i717, env, static) :|: iconst_1 = 1 && 1 <= i717
main_IntArithmetic_1682(i1, i63, i687, iconst_1, i717, env, static) -{1,1}> main_Load_1688(i1, i63, i722, i687, i717, env, static) :|: i687 - iconst_1 = i722 && iconst_1 = 1 && 1 <= i717
main_Load_1688(i1, i63, i722, i687, i717, env, static) -{1,1}> main_IntArithmetic_1693(i1, i63, i722, i717, i687, env, static) :|: 1 <= i717
main_IntArithmetic_1693(i1, i63, i722, i717, i687, env, static) -{1,1}> main_Store_1698(i1, i63, i727, i687, i717, env, static) :|: i722 - i717 = i727 && 1 <= i717
main_Store_1698(i1, i63, i727, i687, i717, env, static) -{1,1}> main_Load_1703(i1, i63, i687, i727, i717, env, static) :|: 1 <= i717
main_Load_1703(i1, i63, i687, i727, i717, env, static) -{1,1}> main_ConstantStackPush_1708(i1, i63, i687, i727, i717, env, static) :|: 1 <= i717
main_ConstantStackPush_1708(i1, i63, i687, i727, i717, env, static) -{1,1}> main_IntArithmetic_1714(i1, i63, i687, iconst_1, i727, i717, env, static) :|: iconst_1 = 1 && 1 <= i717
main_IntArithmetic_1714(i1, i63, i687, iconst_1, i727, i717, env, static) -{1,1}> main_Load_1719(i1, i63, i739, i727, i717, env, static) :|: i687 - iconst_1 = i739 && iconst_1 = 1 && 1 <= i717
main_Load_1719(i1, i63, i739, i727, i717, env, static) -{1,1}> main_IntArithmetic_1723(i1, i63, i739, i717, i727, env, static) :|: 1 <= i717
main_IntArithmetic_1723(i1, i63, i739, i717, i727, env, static) -{1,1}> main_Store_1736(i1, i63, i749, i727, env, static) :|: 1 <= i717 && i739 - i717 = i749
main_Store_1736(i1, i63, i749, i727, env, static) -{0,0}> main_Store_1716(i1, i63, i749, i727, env, static) :|: 0 >= 0

(8) Obligation:

IntTrs with 7 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) -{15,15}> main_Load_1610(i1, i3, 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_Load_1610(i1, i63, i687, i673, env, static) -{1,1}> main_LE_1616(i1, i63, i673, i687, env, static) :|: 0 >= 0
main_LE_1616(i1, i63, i703, i687, env, static) -{0,0}> main_LE_1618(i1, i63, i703, i687, env, static) :|: i703 <= 0
main_LE_1616(i1, i63, i704, i687, env, static) -{7,7}> main_GE_1638(i1, i63, i709', i687, env, static) :|: 0 >= 0 && 1 <= i704 && 0 < 1 && 0 < i704
main_GE_1638(i1, i63, i716, i687, env, static) -{12,12}> main_Store_1716(i1, i63, i737', i720', env, static) :|: i687 - 1 = i718' && i731' - i716 = i737' && 0 <= i716 && i718' - i716 = i720' && i687 - 1 = i731'
main_Store_1716(i1, i63, i737, i720, env, static) -{2,2}> main_Load_1610(i1, i63, i737, i720, env, static) :|: 0 >= 0
main_GE_1638(i1, i63, i715, i687, env, static) -{15,15}> main_Store_1716(i1, i63, i749', i727', env, static) :|: 0 >= 0 && -i715 = i717' && i687 - 1 = i722' && i715 <= -1 && i687 - 1 = i739' && i715 < 0 && i739' - i717' = i749' && i722' - i717' = i727' && 1 <= i717'

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

Moved arithmethic from constraints to rhss.

main_GE_1638(i1, i63, i716, i687, env, static) -{12,12}> main_Store_1716(i1, i63, i737', i720', env, static) :|: i687 - 1 = i718' && i731' - i716 = i737' && 0 <= i716 && i718' - i716 = i720' && i687 - 1 = i731'
was transformed to
main_GE_1638(i1, i63, i716, i687, env, static) -{12,12}> main_Store_1716(i1, i63, i731' - i716, i687 - 1 - i716, env, static) :|: i687 - 1 = i718' && i731' - i716 = i737' && 0 <= i716 && i718' - i716 = i720' && i687 - 1 = i731'

main_GE_1638(i1, i63, i715, i687, env, static) -{15,15}> main_Store_1716(i1, i63, i749', i727', env, static) :|: 0 >= 0 && -i715 = i717' && i687 - 1 = i722' && i715 <= -1 && i687 - 1 = i739' && i715 < 0 && i739' - i717' = i749' && i722' - i717' = i727' && 1 <= i717'
was transformed to
main_GE_1638(i1, i63, i715, i687, env, static) -{15,15}> main_Store_1716(i1, i63, i687 - 1 - -i715, i687 - 1 - -i715, env, static) :|: 0 >= 0 && -i715 = i717' && i687 - 1 = i722' && i715 <= -1 && i687 - 1 = i739' && i715 < 0 && i739' - i717' = i749' && i722' - i717' = i727' && 1 <= i717'

(10) Obligation:

IntTrs with 7 rules
Start term: main_Load_1(#0, #1, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_Store_1716(i1, i63, i737, i720, env, static) -{2,2}> main_Load_1610(i1, i63, i737, i720, env, static) :|: 0 >= 0
main_LE_1616(i1, i63, i704, i687, env, static) -{7,7}> main_GE_1638(i1, i63, i709', i687, env, static) :|: 0 >= 0 && 1 <= i704 && 0 < 1 && 0 < i704
main_GE_1638(i1, i63, i716, i687, env, static) -{12,12}> main_Store_1716(i1, i63, i731' - i716, i687 - 1 - i716, env, static) :|: i687 - 1 = i718' && i731' - i716 = i737' && 0 <= i716 && i718' - i716 = i720' && i687 - 1 = i731'
main_Load_1610(i1, i63, i687, i673, env, static) -{1,1}> main_LE_1616(i1, i63, i673, i687, env, static) :|: 0 >= 0
main_GE_1638(i1, i63, i715, i687, env, static) -{15,15}> main_Store_1716(i1, i63, i687 - 1 - -i715, i687 - 1 - -i715, env, static) :|: 0 >= 0 && -i715 = i717' && i687 - 1 = i722' && i715 <= -1 && i687 - 1 = i739' && i715 < 0 && i739' - i717' = i749' && i722' - i717' = i727' && 1 <= i717'
main_LE_1616(i1, i63, i703, i687, env, static) -{0,0}> main_LE_1618(i1, i63, i703, i687, env, static) :|: i703 <= 0
main_Load_1(i1, i3, env, static) -{15,15}> main_Load_1610(i1, i3, 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

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

Simplified expressions.

main_LE_1616(i1, i63, i704, i687, env, static) -{7,7}> main_GE_1638(i1, i63, i709', i687, env, static) :|: 0 >= 0 && 1 <= i704 && 0 < 1 && 0 < i704
was transformed to
main_LE_1616(i1, i63, i704, i687, env, static) -{7,7}> main_GE_1638(i1, i63, i709', i687, env, static) :|: 1 <= i704 && 0 < i704

main_GE_1638(i1, i63, i716, i687, env, static) -{12,12}> main_Store_1716(i1, i63, i731' - i716, i687 - 1 - i716, env, static) :|: i687 - 1 = i718' && i731' - i716 = i737' && 0 <= i716 && i718' - i716 = i720' && i687 - 1 = i731'
was transformed to
main_GE_1638(i1, i63, i716, i687, env, static) -{12,12}> main_Store_1716(i1, i63, i731' + -1 * i716, i687 - 1 + -1 * i716, env, static) :|: i687 - 1 = i718' && i731' + -1 * i716 = i737' && 0 <= i716 && i718' + -1 * i716 = i720' && i687 - 1 = i731'

main_GE_1638(i1, i63, i715, i687, env, static) -{15,15}> main_Store_1716(i1, i63, i687 - 1 - -i715, i687 - 1 - -i715, env, static) :|: 0 >= 0 && -i715 = i717' && i687 - 1 = i722' && i715 <= -1 && i687 - 1 = i739' && i715 < 0 && i739' - i717' = i749' && i722' - i717' = i727' && 1 <= i717'
was transformed to
main_GE_1638(i1, i63, i715, i687, env, static) -{15,15}> main_Store_1716(i1, i63, i687 - 1 + i715, i687 - 1 + i715, env, static) :|: -1 * i715 = i717' && i687 - 1 = i722' && i715 <= -1 && i687 - 1 = i739' && i715 < 0 && i739' + -1 * i717' = i749' && i722' + -1 * i717' = i727' && 1 <= i717'

main_Load_1(i1, i3, env, static) -{15,15}> main_Load_1610(i1, i3, 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) -{15,15}> main_Load_1610(i1, i3, i1, i3, env, static'1) :|: static'1 <= static''' + 1 && 0 <= static''' && static''' <= static + 2 && 0 <= static && 0 <= static'1

(12) Obligation:

IntTrs with 7 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) -{15,15}> main_Load_1610(i1, i3, i1, i3, env, static'1) :|: static'1 <= static''' + 1 && 0 <= static''' && static''' <= static + 2 && 0 <= static && 0 <= static'1
main_Store_1716(i1, i63, i737, i720, env, static) -{2,2}> main_Load_1610(i1, i63, i737, i720, env, static) :|: 0 >= 0
main_LE_1616(i1, i63, i704, i687, env, static) -{7,7}> main_GE_1638(i1, i63, i709', i687, env, static) :|: 1 <= i704 && 0 < i704
main_GE_1638(i1, i63, i716, i687, env, static) -{12,12}> main_Store_1716(i1, i63, i731' + -1 * i716, i687 - 1 + -1 * i716, env, static) :|: i687 - 1 = i718' && i731' + -1 * i716 = i737' && 0 <= i716 && i718' + -1 * i716 = i720' && i687 - 1 = i731'
main_Load_1610(i1, i63, i687, i673, env, static) -{1,1}> main_LE_1616(i1, i63, i673, i687, env, static) :|: 0 >= 0
main_GE_1638(i1, i63, i715, i687, env, static) -{15,15}> main_Store_1716(i1, i63, i687 - 1 + i715, i687 - 1 + i715, env, static) :|: -1 * i715 = i717' && i687 - 1 = i722' && i715 <= -1 && i687 - 1 = i739' && i715 < 0 && i739' + -1 * i717' = i749' && i722' + -1 * i717' = i727' && 1 <= i717'
main_LE_1616(i1, i63, i703, i687, env, static) -{0,0}> main_LE_1618(i1, i63, i703, i687, env, static) :|: i703 <= 0

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

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

(14) Obligation:

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

(16) Obligation:

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

Moved arithmethic from constraints to rhss.

(18) Obligation:

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

Simplified expressions.

(20) Obligation:

IntTrs with 7 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) -{15,15}> main_Load_1610(i1, i3, i1, i3, env, static'1) :|: static'1 <= static''' + 1 && 0 <= static''' && static''' <= static + 2 && 0 <= static && 0 <= static'1
main_Store_1716(i1, i63, i737, i720, env, static) -{2,2}> main_Load_1610(i1, i63, i737, i720, env, static) :|: 0 >= 0
main_LE_1616(i1, i63, i704, i687, env, static) -{7,7}> main_GE_1638(i1, i63, i709', i687, env, static) :|: 1 <= i704 && 0 < i704
main_GE_1638(i1, i63, i716, i687, env, static) -{12,12}> main_Store_1716(i1, i63, i731' + -1 * i716, i687 - 1 + -1 * i716, env, static) :|: i687 - 1 = i718' && i731' + -1 * i716 = i737' && 0 <= i716 && i718' + -1 * i716 = i720' && i687 - 1 = i731'
main_Load_1610(i1, i63, i687, i673, env, static) -{1,1}> main_LE_1616(i1, i63, i673, i687, env, static) :|: 0 >= 0
main_GE_1638(i1, i63, i715, i687, env, static) -{15,15}> main_Store_1716(i1, i63, i687 - 1 + i715, i687 - 1 + i715, env, static) :|: -1 * i715 = i717' && i687 - 1 = i722' && i715 <= -1 && i687 - 1 = i739' && i715 < 0 && i739' + -1 * i717' = i749' && i722' + -1 * i717' = i727' && 1 <= i717'
main_LE_1616(i1, i63, i703, i687, env, static) -{0,0}> main_LE_1618(i1, i63, i703, i687, env, static) :|: i703 <= 0

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

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

(22) Obligation:

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

Used field analysis yielded the following read fields:

Considered paths: all paths from start

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

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

(24) Obligation:

IntTrs with 78 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_3(i1, i3, env, static) :|: 0 >= 0
main_Load_3(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_15(iconst_0, i1, i3, env, static) :|: iconst_0 = 0
langle_clinit_rangle_ArrayCreate_15(iconst_0, i1, i3, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_16(a2, i1, i3, iconst_0, env, static) :|: a2 = 2 && iconst_0 = 0 && 0 < a2
langle_clinit_rangle_FieldAccess_16(a2, i1, i3, iconst_0, env, static) -{1,1}> langle_clinit_rangle_New_18(i1, i3, env, static') :|: 0 <= a2 && iconst_0 = 0 && static' <= static + a2 && 0 <= static && 0 < a2
langle_clinit_rangle_New_18(i1, i3, env, static) -{0,0}> langle_clinit_rangle_New_19(i1, i3, env, static) :|: 0 >= 0
langle_clinit_rangle_New_19(i1, i3, env, static) -{0,0}> langle_clinit_rangle_New_21(i1, i3, env, static) :|: 0 <= static
langle_clinit_rangle_New_21(i1, i3, env, static) -{1,1}> langle_clinit_rangle_Duplicate_23(o2, i1, i3, env, static) :|: 0 < o2 && o2 = 1
langle_clinit_rangle_Duplicate_23(o2, i1, i3, env, static) -{1,1}> langle_clinit_rangle_ConstantStackPush_25(o2, i1, i3, env, static) :|: 0 < o2
langle_clinit_rangle_ConstantStackPush_25(o2, i1, i3, env, static) -{1,1}> langle_clinit_rangle_InvokeMethod_28(o2, NULL, i1, i3, env, static) :|: NULL = 0 && 0 < o2
langle_clinit_rangle_InvokeMethod_28(o2, NULL, i1, i3, env, static) -{1,1}> langle_init_rangle_Load_30(o2, i1, i3, env, static) :|: NULL = 0 && 0 < o2
langle_init_rangle_Load_30(o2, i1, i3, env, static) -{1,1}> langle_init_rangle_InvokeMethod_34(o2, i1, i3, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_34(o2, i1, i3, env, static) -{1,1}> langle_init_rangle_Load_35(o2, i1, i3, env, static) :|: 0 < o2
langle_init_rangle_Load_35(o2, i1, i3, env, static) -{1,1}> langle_init_rangle_InvokeMethod_37(o2, i1, i3, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_37(o2, i1, i3, env, static) -{1,1}> langle_init_rangle_Return_41(o2, i1, i3, env, static) :|: 0 < o2
langle_init_rangle_Return_41(o2, i1, i3, env, static) -{1,1}> langle_init_rangle_Return_42(o2, i1, i3, env, static) :|: 0 < o2
langle_init_rangle_Return_42(o2, i1, i3, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_43(o2, i1, i3, env, static) :|: 0 < o2
langle_clinit_rangle_FieldAccess_43(o2, i1, i3, env, static) -{1,1}> langle_clinit_rangle_Return_44(i1, i3, env, static') :|: 0 < o2 && 0 <= o2 && 0 <= static && static' <= static + o2
langle_clinit_rangle_Return_44(i1, i3, env, static) -{1,1}> main_Load_47(i1, i3, env, static) :|: 0 >= 0
main_Load_47(i1, i3, env, static) -{0,0}> main_Load_48(i1, i3, env, static) :|: 0 >= 0
main_Load_48(i1, i3, env, static) -{0,0}> main_Load_50(i1, i3, env, static) :|: 0 <= static
main_Load_50(i1, i3, env, static) -{0,0}> main_Load_52(i1, i3, env, static) :|: 0 >= 0
main_Load_52(i1, i3, env, static) -{0,0}> main_Load_53(i1, i3, env, static) :|: 0 >= 0
main_Load_53(i1, i3, env, static) -{0,0}> main_Load_190(i1, i3, i1, i3, env, static) :|: 0 >= 0
main_Load_190(i1, i63, i64, i65, env, static) -{0,0}> main_Load_347(i1, i63, i64, i65, env, static) :|: 0 >= 0
main_Load_347(i1, i63, i121, i104, env, static) -{0,0}> main_Load_474(i1, i63, i121, i104, env, static) :|: 0 >= 0
main_Load_474(i1, i63, i186, i175, env, static) -{0,0}> main_Load_587(i1, i63, i186, i175, env, static) :|: 0 >= 0
main_Load_587(i1, i63, i237, i222, env, static) -{0,0}> main_Load_718(i1, i63, i237, i222, env, static) :|: 0 >= 0
main_Load_718(i1, i63, i292, i285, env, static) -{0,0}> main_Load_807(i1, i63, i292, i285, env, static) :|: 0 >= 0
main_Load_807(i1, i63, i332, i322, env, static) -{0,0}> main_Load_932(i1, i63, i332, i322, env, static) :|: 0 >= 0
main_Load_932(i1, i63, i386, i371, env, static) -{0,0}> main_Load_1039(i1, i63, i386, i371, env, static) :|: 0 >= 0
main_Load_1039(i1, i63, i437, i424, env, static) -{0,0}> main_Load_1148(i1, i63, i437, i424, env, static) :|: 0 >= 0
main_Load_1148(i1, i63, i484, i471, env, static) -{0,0}> main_Load_1261(i1, i63, i484, i471, env, static) :|: 0 >= 0
main_Load_1261(i1, i63, i531, i518, env, static) -{0,0}> main_Load_1373(i1, i63, i531, i518, env, static) :|: 0 >= 0
main_Load_1373(i1, i63, i584, i565, env, static) -{0,0}> main_Load_1498(i1, i63, i584, i565, env, static) :|: 0 >= 0
main_Load_1498(i1, i63, i636, i615, env, static) -{0,0}> main_Load_1610(i1, i63, i636, i615, env, static) :|: 0 >= 0
main_Load_1610(i1, i63, i687, i673, env, static) -{1,1}> main_LE_1616(i1, i63, i673, i687, env, static) :|: 0 >= 0
main_LE_1616(i1, i63, i704, i687, env, static) -{0,0}> main_LE_1619(i1, i63, i704, i687, env, static) :|: 1 <= i704
main_LE_1619(i1, i63, i704, i687, env, static) -{1,1}> main_New_1623(i1, i63, i687, env, static) :|: 1 <= i704 && 0 < i704
main_New_1623(i1, i63, i687, env, static) -{1,1}> main_Duplicate_1626(i1, i63, o208, i687, env, static) :|: o208 = 1 && 0 < o208
main_Duplicate_1626(i1, i63, o208, i687, env, static) -{1,1}> main_InvokeMethod_1628(i1, i63, o208, i687, env, static) :|: 0 < o208
main_InvokeMethod_1628(i1, i63, o208, i687, env, static) -{1,1}> main_InvokeMethod_1631(i1, i63, o208, i687, env, static) :|: 0 < o208
main_InvokeMethod_1631(i1, i63, o208, i687, env, static) -{1,1}> main_Store_1633(i1, i63, i709, i687, env, static) :|: 0 < o208
main_Store_1633(i1, i63, i709, i687, env, static) -{1,1}> main_Load_1635(i1, i63, i687, i709, env, static) :|: 0 >= 0
main_Load_1635(i1, i63, i687, i709, env, static) -{1,1}> main_GE_1638(i1, i63, i709, i687, env, static) :|: 0 >= 0
main_GE_1638(i1, i63, i715, i687, env, static) -{0,0}> main_GE_1640(i1, i63, i715, i687, env, static) :|: i715 <= -1
main_GE_1638(i1, i63, i716, i687, env, static) -{0,0}> main_GE_1641(i1, i63, i716, i687, env, static) :|: 0 <= i716
main_GE_1640(i1, i63, i715, i687, env, static) -{1,1}> main_Load_1643(i1, i63, i687, i715, env, static) :|: i715 < 0 && i715 <= -1
main_GE_1641(i1, i63, i716, i687, env, static) -{1,1}> main_Load_1645(i1, i63, i687, i716, env, static) :|: 0 <= i716
main_Load_1643(i1, i63, i687, i715, env, static) -{1,1}> main_IntArithmetic_1647(i1, i63, i715, i687, env, static) :|: i715 <= -1
main_Load_1645(i1, i63, i687, i716, env, static) -{1,1}> main_ConstantStackPush_1649(i1, i63, i687, i716, env, static) :|: 0 <= i716
main_IntArithmetic_1647(i1, i63, i715, i687, env, static) -{1,1}> main_Store_1651(i1, i63, i717, i687, env, static) :|: -i715 = i717 && i715 <= -1 && 1 <= i717
main_ConstantStackPush_1649(i1, i63, i687, i716, env, static) -{1,1}> main_IntArithmetic_1653(i1, i63, i687, iconst_1, i716, env, static) :|: iconst_1 = 1 && 0 <= i716
main_Store_1651(i1, i63, i717, i687, env, static) -{1,1}> main_Load_1658(i1, i63, i687, i717, env, static) :|: 1 <= i717
main_IntArithmetic_1653(i1, i63, i687, iconst_1, i716, env, static) -{1,1}> main_Load_1672(i1, i63, i718, i687, i716, env, static) :|: i687 - iconst_1 = i718 && iconst_1 = 1 && 0 <= i716
main_Load_1658(i1, i63, i687, i717, env, static) -{1,1}> main_ConstantStackPush_1676(i1, i63, i687, i717, env, static) :|: 1 <= i717
main_Load_1672(i1, i63, i718, i687, i716, env, static) -{1,1}> main_IntArithmetic_1678(i1, i63, i718, i716, i687, env, static) :|: 0 <= i716
main_ConstantStackPush_1676(i1, i63, i687, i717, env, static) -{1,1}> main_IntArithmetic_1682(i1, i63, i687, iconst_1, i717, env, static) :|: iconst_1 = 1 && 1 <= i717
main_IntArithmetic_1678(i1, i63, i718, i716, i687, env, static) -{1,1}> main_Store_1683(i1, i63, i720, i687, i716, env, static) :|: i718 - i716 = i720 && 0 <= i716
main_IntArithmetic_1682(i1, i63, i687, iconst_1, i717, env, static) -{1,1}> main_Load_1688(i1, i63, i722, i687, i717, env, static) :|: i687 - iconst_1 = i722 && iconst_1 = 1 && 1 <= i717
main_Store_1683(i1, i63, i720, i687, i716, env, static) -{1,1}> main_Load_1690(i1, i63, i687, i720, i716, env, static) :|: 0 <= i716
main_Load_1688(i1, i63, i722, i687, i717, env, static) -{1,1}> main_IntArithmetic_1693(i1, i63, i722, i717, i687, env, static) :|: 1 <= i717
main_Load_1690(i1, i63, i687, i720, i716, env, static) -{1,1}> main_ConstantStackPush_1695(i1, i63, i687, i720, i716, env, static) :|: 0 <= i716
main_IntArithmetic_1693(i1, i63, i722, i717, i687, env, static) -{1,1}> main_Store_1698(i1, i63, i727, i687, i717, env, static) :|: i722 - i717 = i727 && 1 <= i717
main_ConstantStackPush_1695(i1, i63, i687, i720, i716, env, static) -{1,1}> main_IntArithmetic_1700(i1, i63, i687, iconst_1, i720, i716, env, static) :|: iconst_1 = 1 && 0 <= i716
main_Store_1698(i1, i63, i727, i687, i717, env, static) -{1,1}> main_Load_1703(i1, i63, i687, i727, i717, env, static) :|: 1 <= i717
main_IntArithmetic_1700(i1, i63, i687, iconst_1, i720, i716, env, static) -{1,1}> main_Load_1705(i1, i63, i731, i720, i716, env, static) :|: i687 - iconst_1 = i731 && iconst_1 = 1 && 0 <= i716
main_Load_1703(i1, i63, i687, i727, i717, env, static) -{1,1}> main_ConstantStackPush_1708(i1, i63, i687, i727, i717, env, static) :|: 1 <= i717
main_Load_1705(i1, i63, i731, i720, i716, env, static) -{1,1}> main_IntArithmetic_1710(i1, i63, i731, i716, i720, env, static) :|: 0 <= i716
main_ConstantStackPush_1708(i1, i63, i687, i727, i717, env, static) -{1,1}> main_IntArithmetic_1714(i1, i63, i687, iconst_1, i727, i717, env, static) :|: iconst_1 = 1 && 1 <= i717
main_IntArithmetic_1710(i1, i63, i731, i716, i720, env, static) -{1,1}> main_Store_1716(i1, i63, i737, i720, env, static) :|: i731 - i716 = i737 && 0 <= i716
main_IntArithmetic_1714(i1, i63, i687, iconst_1, i727, i717, env, static) -{1,1}> main_Load_1719(i1, i63, i739, i727, i717, env, static) :|: i687 - iconst_1 = i739 && iconst_1 = 1 && 1 <= i717
main_Store_1716(i1, i63, i737, i720, env, static) -{1,1}> main_JMP_1721(i1, i63, i737, i720, env, static) :|: 0 >= 0
main_Load_1719(i1, i63, i739, i727, i717, env, static) -{1,1}> main_IntArithmetic_1723(i1, i63, i739, i717, i727, env, static) :|: 1 <= i717
main_JMP_1721(i1, i63, i737, i720, env, static) -{1,1}> main_Load_1730(i1, i63, i737, i720, env, static) :|: 0 >= 0
main_IntArithmetic_1723(i1, i63, i739, i717, i727, env, static) -{1,1}> main_Store_1736(i1, i63, i749, i727, env, static) :|: 1 <= i717 && i739 - i717 = i749
main_Load_1730(i1, i63, i737, i720, env, static) -{0,0}> main_Load_1610(i1, i63, i737, i720, env, static) :|: 0 >= 0
main_Store_1736(i1, i63, i749, i727, env, static) -{0,0}> main_Store_1716(i1, i63, i749, i727, env, static) :|: 0 >= 0

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

obtained
main_Load_1610(i1, i63, i687, i673, env, static) -{8,8}> main_GE_1638(i1, i63, i709', i687, env, static) :|: 0 >= 0 && 1 <= i673 && 0 < 1 && 0 < i673
by chaining
main_Load_1610(i1, i63, i687, i673, env, static) -{1,1}> main_LE_1616(i1, i63, i673, i687, env, static) :|: 0 >= 0
main_LE_1616(i1, i63, i704, i687, env, static) -{0,0}> main_LE_1619(i1, i63, i704, i687, env, static) :|: 1 <= i704
main_LE_1619(i1, i63, i704, i687, env, static) -{1,1}> main_New_1623(i1, i63, i687, env, static) :|: 1 <= i704 && 0 < i704
main_New_1623(i1, i63, i687, env, static) -{1,1}> main_Duplicate_1626(i1, i63, o208, i687, env, static) :|: o208 = 1 && 0 < o208
main_Duplicate_1626(i1, i63, o208, i687, env, static) -{1,1}> main_InvokeMethod_1628(i1, i63, o208, i687, env, static) :|: 0 < o208
main_InvokeMethod_1628(i1, i63, o208, i687, env, static) -{1,1}> main_InvokeMethod_1631(i1, i63, o208, i687, env, static) :|: 0 < o208
main_InvokeMethod_1631(i1, i63, o208, i687, env, static) -{1,1}> main_Store_1633(i1, i63, i709, i687, env, static) :|: 0 < o208
main_Store_1633(i1, i63, i709, i687, env, static) -{1,1}> main_Load_1635(i1, i63, i687, i709, env, static) :|: 0 >= 0
main_Load_1635(i1, i63, i687, i709, env, static) -{1,1}> main_GE_1638(i1, i63, i709, i687, env, static) :|: 0 >= 0

(26) Obligation:

IntTrs with 5 rules
Start term: main_Load_1(#0, #1, env, static)
Considered paths: all paths from start
Rules:
main_Load_1(i1, i3, env, static) -{15,15}> main_Load_1610(i1, i3, 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_Load_1610(i1, i63, i687, i673, env, static) -{8,8}> main_GE_1638(i1, i63, i709', i687, env, static) :|: 0 >= 0 && 1 <= i673 && 0 < 1 && 0 < i673
main_GE_1638(i1, i63, i716, i687, env, static) -{12,12}> main_Store_1716(i1, i63, i737', i720', env, static) :|: i687 - 1 = i718' && i731' - i716 = i737' && 0 <= i716 && i718' - i716 = i720' && i687 - 1 = i731'
main_Store_1716(i1, i63, i737, i720, env, static) -{2,2}> main_Load_1610(i1, i63, i737, i720, env, static) :|: 0 >= 0
main_GE_1638(i1, i63, i715, i687, env, static) -{15,15}> main_Store_1716(i1, i63, i749', i727', env, static) :|: 0 >= 0 && -i715 = i717' && i687 - 1 = i722' && i715 <= -1 && i687 - 1 = i739' && i715 < 0 && i739' - i717' = i749' && i722' - i717' = i727' && 1 <= i717'

(27) 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_1610(x1, x2, x3, x4, x5, x6) → main_Load_1610(x3, x4)
main_GE_1638(x1, x2, x3, x4, x5, x6) → main_GE_1638(x3, x4)
main_Store_1716(x1, x2, x3, x4, x5, x6) → main_Store_1716(x3, x4)

(28) Obligation:

IntTrs with 5 rules
Start term: main_Load_1(#0, #1, static)
Considered paths: all paths from start
Rules:
main_Load_1(i1, i3, static) -{15,15}> main_Load_1610(i1, i3) :|: 0 >= 0 && static'1 <= static''' + 1 && 0 <= 2 && 0 <= static''' && static''' <= static + 2 && 0 < 1 && 0 <= 1 && 0 <= static && 0 <= static'1 && 0 < 2
main_Load_1610(i687, i673) -{8,8}> main_GE_1638(i709', i687) :|: 0 >= 0 && 1 <= i673 && 0 < 1 && 0 < i673
main_GE_1638(i716, i687) -{12,12}> main_Store_1716(i737', i720') :|: i687 - 1 = i718' && i731' - i716 = i737' && 0 <= i716 && i718' - i716 = i720' && i687 - 1 = i731'
main_Store_1716(i737, i720) -{2,2}> main_Load_1610(i737, i720) :|: 0 >= 0
main_GE_1638(i715, i687) -{15,15}> main_Store_1716(i749', i727') :|: 0 >= 0 && -i715 = i717' && i687 - 1 = i722' && i715 <= -1 && i687 - 1 = i739' && i715 < 0 && i739' - i717' = i749' && i722' - i717' = i727' && 1 <= i717'

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

Moved arithmethic from constraints to rhss.

main_GE_1638(i715, i687) -{15,15}> main_Store_1716(i749', i727') :|: 0 >= 0 && -i715 = i717' && i687 - 1 = i722' && i715 <= -1 && i687 - 1 = i739' && i715 < 0 && i739' - i717' = i749' && i722' - i717' = i727' && 1 <= i717'
was transformed to
main_GE_1638(i715, i687) -{15,15}> main_Store_1716(i687 - 1 - -i715, i687 - 1 - -i715) :|: 0 >= 0 && -i715 = i717' && i687 - 1 = i722' && i715 <= -1 && i687 - 1 = i739' && i715 < 0 && i739' - i717' = i749' && i722' - i717' = i727' && 1 <= i717'

main_GE_1638(i716, i687) -{12,12}> main_Store_1716(i737', i720') :|: i687 - 1 = i718' && i731' - i716 = i737' && 0 <= i716 && i718' - i716 = i720' && i687 - 1 = i731'
was transformed to
main_GE_1638(i716, i687) -{12,12}> main_Store_1716(i731' - i716, i687 - 1 - i716) :|: i687 - 1 = i718' && i731' - i716 = i737' && 0 <= i716 && i718' - i716 = i720' && i687 - 1 = i731'

(30) Obligation:

IntTrs with 5 rules
Start term: main_Load_1(#0, #1, static)
Considered paths: all paths from start
Rules:
main_Store_1716(i737, i720) -{2,2}> main_Load_1610(i737, i720) :|: 0 >= 0
main_Load_1(i1, i3, static) -{15,15}> main_Load_1610(i1, i3) :|: 0 >= 0 && static'1 <= static''' + 1 && 0 <= 2 && 0 <= static''' && static''' <= static + 2 && 0 < 1 && 0 <= 1 && 0 <= static && 0 <= static'1 && 0 < 2
main_GE_1638(i715, i687) -{15,15}> main_Store_1716(i687 - 1 - -i715, i687 - 1 - -i715) :|: 0 >= 0 && -i715 = i717' && i687 - 1 = i722' && i715 <= -1 && i687 - 1 = i739' && i715 < 0 && i739' - i717' = i749' && i722' - i717' = i727' && 1 <= i717'
main_GE_1638(i716, i687) -{12,12}> main_Store_1716(i731' - i716, i687 - 1 - i716) :|: i687 - 1 = i718' && i731' - i716 = i737' && 0 <= i716 && i718' - i716 = i720' && i687 - 1 = i731'
main_Load_1610(i687, i673) -{8,8}> main_GE_1638(i709', i687) :|: 0 >= 0 && 1 <= i673 && 0 < 1 && 0 < i673

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

Simplified expressions.

main_Load_1(i1, i3, static) -{15,15}> main_Load_1610(i1, i3) :|: 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, static) -{15,15}> main_Load_1610(i1, i3) :|: static'1 <= static''' + 1 && 0 <= static''' && static''' <= static + 2 && 0 <= static && 0 <= static'1

main_GE_1638(i716, i687) -{12,12}> main_Store_1716(i731' - i716, i687 - 1 - i716) :|: i687 - 1 = i718' && i731' - i716 = i737' && 0 <= i716 && i718' - i716 = i720' && i687 - 1 = i731'
was transformed to
main_GE_1638(i716, i687) -{12,12}> main_Store_1716(i731' + -1 * i716, i687 - 1 + -1 * i716) :|: i687 - 1 = i718' && i731' + -1 * i716 = i737' && 0 <= i716 && i718' + -1 * i716 = i720' && i687 - 1 = i731'

main_Load_1610(i687, i673) -{8,8}> main_GE_1638(i709', i687) :|: 0 >= 0 && 1 <= i673 && 0 < 1 && 0 < i673
was transformed to
main_Load_1610(i687, i673) -{8,8}> main_GE_1638(i709', i687) :|: 1 <= i673 && 0 < i673

main_GE_1638(i715, i687) -{15,15}> main_Store_1716(i687 - 1 - -i715, i687 - 1 - -i715) :|: 0 >= 0 && -i715 = i717' && i687 - 1 = i722' && i715 <= -1 && i687 - 1 = i739' && i715 < 0 && i739' - i717' = i749' && i722' - i717' = i727' && 1 <= i717'
was transformed to
main_GE_1638(i715, i687) -{15,15}> main_Store_1716(i687 - 1 + i715, i687 - 1 + i715) :|: -1 * i715 = i717' && i687 - 1 = i722' && i715 <= -1 && i687 - 1 = i739' && i715 < 0 && i739' + -1 * i717' = i749' && i722' + -1 * i717' = i727' && 1 <= i717'

(32) Obligation:

IntTrs with 5 rules
Start term: main_Load_1(#0, #1, static)
Considered paths: all paths from start
Rules:
main_Store_1716(i737, i720) -{2,2}> main_Load_1610(i737, i720) :|: 0 >= 0
main_Load_1610(i687, i673) -{8,8}> main_GE_1638(i709', i687) :|: 1 <= i673 && 0 < i673
main_GE_1638(i715, i687) -{15,15}> main_Store_1716(i687 - 1 + i715, i687 - 1 + i715) :|: -1 * i715 = i717' && i687 - 1 = i722' && i715 <= -1 && i687 - 1 = i739' && i715 < 0 && i739' + -1 * i717' = i749' && i722' + -1 * i717' = i727' && 1 <= i717'
main_Load_1(i1, i3, static) -{15,15}> main_Load_1610(i1, i3) :|: static'1 <= static''' + 1 && 0 <= static''' && static''' <= static + 2 && 0 <= static && 0 <= static'1
main_GE_1638(i716, i687) -{12,12}> main_Store_1716(i731' + -1 * i716, i687 - 1 + -1 * i716) :|: i687 - 1 = i718' && i731' + -1 * i716 = i737' && 0 <= i716 && i718' + -1 * i716 = i720' && i687 - 1 = i731'

(33) koat Proof (EQUIVALENT transformation)

YES(?, 47*ar_0 + 23)

Initial complexity problem:
1: T:
(Comp: ?, Cost: 2) main_Store_1716(ar_0, ar_1, ar_2) -> Com_1(main_Load_1610(ar_0, ar_1, arityPad)) [ 0 >= 0 ]
(Comp: ?, Cost: 8) main_Load_1610(ar_0, ar_1, ar_2) -> Com_1(main_GE_1638(i709', ar_0, arityPad)) [ 1 <= ar_1 /\ 0 < ar_1 ]
(Comp: ?, Cost: 15) main_GE_1638(ar_0, ar_1, ar_2) -> Com_1(main_Store_1716(ar_1 + ar_0 - 1, ar_1 + ar_0 - 1, arityPad)) [ -ar_0 = i717' /\ ar_1 - 1 = i722' /\ ar_0 <= -1 /\ ar_1 - 1 = i739' /\ ar_0 < 0 /\ i739' - i717' = i749' /\ i722' - i717' = i727' /\ 1 <= i717' ]
(Comp: ?, Cost: 15) main_Load_1(ar_0, ar_1, ar_2) -> Com_1(main_Load_1610(ar_0, ar_1, arityPad)) [ static'1 <= static''' + 1 /\ 0 <= static''' /\ static''' <= ar_2 + 2 /\ 0 <= ar_2 /\ 0 <= static'1 ]
(Comp: ?, Cost: 12) main_GE_1638(ar_0, ar_1, ar_2) -> Com_1(main_Store_1716(i731' - ar_0, ar_1 - ar_0 - 1, arityPad)) [ ar_1 - 1 = i718' /\ i731' - ar_0 = i737' /\ 0 <= ar_0 /\ i718' - ar_0 = i720' /\ ar_1 - 1 = i731' ]
(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: 2) main_Store_1716(ar_0, ar_1, ar_2) -> Com_1(main_Load_1610(ar_0, ar_1, arityPad)) [ 0 >= 0 ]
(Comp: ?, Cost: 8) main_Load_1610(ar_0, ar_1, ar_2) -> Com_1(main_GE_1638(i709', ar_0, arityPad)) [ 1 <= ar_1 /\ 0 < ar_1 ]
(Comp: ?, Cost: 15) main_GE_1638(ar_0, ar_1, ar_2) -> Com_1(main_Store_1716(ar_1 + ar_0 - 1, ar_1 + ar_0 - 1, arityPad)) [ -ar_0 = i717' /\ ar_1 - 1 = i722' /\ ar_0 <= -1 /\ ar_1 - 1 = i739' /\ ar_0 < 0 /\ i739' - i717' = i749' /\ i722' - i717' = i727' /\ 1 <= i717' ]
(Comp: 1, Cost: 15) main_Load_1(ar_0, ar_1, ar_2) -> Com_1(main_Load_1610(ar_0, ar_1, arityPad)) [ static'1 <= static''' + 1 /\ 0 <= static''' /\ static''' <= ar_2 + 2 /\ 0 <= ar_2 /\ 0 <= static'1 ]
(Comp: ?, Cost: 12) main_GE_1638(ar_0, ar_1, ar_2) -> Com_1(main_Store_1716(i731' - ar_0, ar_1 - ar_0 - 1, arityPad)) [ ar_1 - 1 = i718' /\ i731' - ar_0 = i737' /\ 0 <= ar_0 /\ i718' - ar_0 = i720' /\ ar_1 - 1 = i731' ]
(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

By chaining the transition main_Store_1716(ar_0, ar_1, ar_2) -> Com_1(main_Load_1610(ar_0, ar_1, arityPad)) [ 0 >= 0 ] with all transitions in problem 2, the following new transition is obtained:
main_Store_1716(ar_0, ar_1, ar_2) -> Com_1(main_GE_1638(i709', ar_0, arityPad')) [ 0 >= 0 /\ 1 <= ar_1 /\ 0 < ar_1 ]
We thus obtain the following problem:
3: T:
(Comp: ?, Cost: 10) main_Store_1716(ar_0, ar_1, ar_2) -> Com_1(main_GE_1638(i709', ar_0, arityPad')) [ 0 >= 0 /\ 1 <= ar_1 /\ 0 < ar_1 ]
(Comp: ?, Cost: 8) main_Load_1610(ar_0, ar_1, ar_2) -> Com_1(main_GE_1638(i709', ar_0, arityPad)) [ 1 <= ar_1 /\ 0 < ar_1 ]
(Comp: ?, Cost: 15) main_GE_1638(ar_0, ar_1, ar_2) -> Com_1(main_Store_1716(ar_1 + ar_0 - 1, ar_1 + ar_0 - 1, arityPad)) [ -ar_0 = i717' /\ ar_1 - 1 = i722' /\ ar_0 <= -1 /\ ar_1 - 1 = i739' /\ ar_0 < 0 /\ i739' - i717' = i749' /\ i722' - i717' = i727' /\ 1 <= i717' ]
(Comp: 1, Cost: 15) main_Load_1(ar_0, ar_1, ar_2) -> Com_1(main_Load_1610(ar_0, ar_1, arityPad)) [ static'1 <= static''' + 1 /\ 0 <= static''' /\ static''' <= ar_2 + 2 /\ 0 <= ar_2 /\ 0 <= static'1 ]
(Comp: ?, Cost: 12) main_GE_1638(ar_0, ar_1, ar_2) -> Com_1(main_Store_1716(i731' - ar_0, ar_1 - ar_0 - 1, arityPad)) [ ar_1 - 1 = i718' /\ i731' - ar_0 = i737' /\ 0 <= ar_0 /\ i718' - ar_0 = i720' /\ ar_1 - 1 = i731' ]
(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 3 produces the following problem:
4: T:
(Comp: ?, Cost: 10) main_Store_1716(ar_0, ar_1, ar_2) -> Com_1(main_GE_1638(i709', ar_0, arityPad')) [ 0 >= 0 /\ 1 <= ar_1 /\ 0 < ar_1 ]
(Comp: 1, Cost: 8) main_Load_1610(ar_0, ar_1, ar_2) -> Com_1(main_GE_1638(i709', ar_0, arityPad)) [ 1 <= ar_1 /\ 0 < ar_1 ]
(Comp: ?, Cost: 15) main_GE_1638(ar_0, ar_1, ar_2) -> Com_1(main_Store_1716(ar_1 + ar_0 - 1, ar_1 + ar_0 - 1, arityPad)) [ -ar_0 = i717' /\ ar_1 - 1 = i722' /\ ar_0 <= -1 /\ ar_1 - 1 = i739' /\ ar_0 < 0 /\ i739' - i717' = i749' /\ i722' - i717' = i727' /\ 1 <= i717' ]
(Comp: 1, Cost: 15) main_Load_1(ar_0, ar_1, ar_2) -> Com_1(main_Load_1610(ar_0, ar_1, arityPad)) [ static'1 <= static''' + 1 /\ 0 <= static''' /\ static''' <= ar_2 + 2 /\ 0 <= ar_2 /\ 0 <= static'1 ]
(Comp: ?, Cost: 12) main_GE_1638(ar_0, ar_1, ar_2) -> Com_1(main_Store_1716(i731' - ar_0, ar_1 - ar_0 - 1, arityPad)) [ ar_1 - 1 = i718' /\ i731' - ar_0 = i737' /\ 0 <= ar_0 /\ i718' - ar_0 = i720' /\ ar_1 - 1 = i731' ]
(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

By chaining the transition main_GE_1638(ar_0, ar_1, ar_2) -> Com_1(main_Store_1716(ar_1 + ar_0 - 1, ar_1 + ar_0 - 1, arityPad)) [ -ar_0 = i717' /\ ar_1 - 1 = i722' /\ ar_0 <= -1 /\ ar_1 - 1 = i739' /\ ar_0 < 0 /\ i739' - i717' = i749' /\ i722' - i717' = i727' /\ 1 <= i717' ] with all transitions in problem 4, the following new transition is obtained:
main_GE_1638(ar_0, ar_1, ar_2) -> Com_1(main_GE_1638(i709', ar_1 + ar_0 - 1, arityPad')) [ -ar_0 = i717' /\ ar_1 - 1 = i722' /\ ar_0 <= -1 /\ ar_1 - 1 = i739' /\ ar_0 < 0 /\ i739' - i717' = i749' /\ i722' - i717' = i727' /\ 1 <= i717' /\ 0 >= 0 /\ 1 <= ar_1 + ar_0 - 1 /\ 0 < ar_1 + ar_0 - 1 ]
We thus obtain the following problem:
5: T:
(Comp: ?, Cost: 25) main_GE_1638(ar_0, ar_1, ar_2) -> Com_1(main_GE_1638(i709', ar_1 + ar_0 - 1, arityPad')) [ -ar_0 = i717' /\ ar_1 - 1 = i722' /\ ar_0 <= -1 /\ ar_1 - 1 = i739' /\ ar_0 < 0 /\ i739' - i717' = i749' /\ i722' - i717' = i727' /\ 1 <= i717' /\ 0 >= 0 /\ 1 <= ar_1 + ar_0 - 1 /\ 0 < ar_1 + ar_0 - 1 ]
(Comp: ?, Cost: 10) main_Store_1716(ar_0, ar_1, ar_2) -> Com_1(main_GE_1638(i709', ar_0, arityPad')) [ 0 >= 0 /\ 1 <= ar_1 /\ 0 < ar_1 ]
(Comp: 1, Cost: 8) main_Load_1610(ar_0, ar_1, ar_2) -> Com_1(main_GE_1638(i709', ar_0, arityPad)) [ 1 <= ar_1 /\ 0 < ar_1 ]
(Comp: 1, Cost: 15) main_Load_1(ar_0, ar_1, ar_2) -> Com_1(main_Load_1610(ar_0, ar_1, arityPad)) [ static'1 <= static''' + 1 /\ 0 <= static''' /\ static''' <= ar_2 + 2 /\ 0 <= ar_2 /\ 0 <= static'1 ]
(Comp: ?, Cost: 12) main_GE_1638(ar_0, ar_1, ar_2) -> Com_1(main_Store_1716(i731' - ar_0, ar_1 - ar_0 - 1, arityPad)) [ ar_1 - 1 = i718' /\ i731' - ar_0 = i737' /\ 0 <= ar_0 /\ i718' - ar_0 = i720' /\ ar_1 - 1 = i731' ]
(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_GE_1638) = V_2
Pol(main_Store_1716) = V_1 + 1
Pol(main_Load_1610) = V_1
Pol(main_Load_1) = V_1
Pol(koat_start) = V_1
orients all transitions weakly and the transition
main_GE_1638(ar_0, ar_1, ar_2) -> Com_1(main_GE_1638(i709', ar_1 + ar_0 - 1, arityPad')) [ -ar_0 = i717' /\ ar_1 - 1 = i722' /\ ar_0 <= -1 /\ ar_1 - 1 = i739' /\ ar_0 < 0 /\ i739' - i717' = i749' /\ i722' - i717' = i727' /\ 1 <= i717' /\ 0 >= 0 /\ 1 <= ar_1 + ar_0 - 1 /\ 0 < ar_1 + ar_0 - 1 ]
strictly and produces the following problem:
6: T:
(Comp: ar_0, Cost: 25) main_GE_1638(ar_0, ar_1, ar_2) -> Com_1(main_GE_1638(i709', ar_1 + ar_0 - 1, arityPad')) [ -ar_0 = i717' /\ ar_1 - 1 = i722' /\ ar_0 <= -1 /\ ar_1 - 1 = i739' /\ ar_0 < 0 /\ i739' - i717' = i749' /\ i722' - i717' = i727' /\ 1 <= i717' /\ 0 >= 0 /\ 1 <= ar_1 + ar_0 - 1 /\ 0 < ar_1 + ar_0 - 1 ]
(Comp: ?, Cost: 10) main_Store_1716(ar_0, ar_1, ar_2) -> Com_1(main_GE_1638(i709', ar_0, arityPad')) [ 0 >= 0 /\ 1 <= ar_1 /\ 0 < ar_1 ]
(Comp: 1, Cost: 8) main_Load_1610(ar_0, ar_1, ar_2) -> Com_1(main_GE_1638(i709', ar_0, arityPad)) [ 1 <= ar_1 /\ 0 < ar_1 ]
(Comp: 1, Cost: 15) main_Load_1(ar_0, ar_1, ar_2) -> Com_1(main_Load_1610(ar_0, ar_1, arityPad)) [ static'1 <= static''' + 1 /\ 0 <= static''' /\ static''' <= ar_2 + 2 /\ 0 <= ar_2 /\ 0 <= static'1 ]
(Comp: ?, Cost: 12) main_GE_1638(ar_0, ar_1, ar_2) -> Com_1(main_Store_1716(i731' - ar_0, ar_1 - ar_0 - 1, arityPad)) [ ar_1 - 1 = i718' /\ i731' - ar_0 = i737' /\ 0 <= ar_0 /\ i718' - ar_0 = i720' /\ ar_1 - 1 = i731' ]
(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

By chaining the transition main_Load_1(ar_0, ar_1, ar_2) -> Com_1(main_Load_1610(ar_0, ar_1, arityPad)) [ static'1 <= static''' + 1 /\ 0 <= static''' /\ static''' <= ar_2 + 2 /\ 0 <= ar_2 /\ 0 <= static'1 ] with all transitions in problem 6, the following new transition is obtained:
main_Load_1(ar_0, ar_1, ar_2) -> Com_1(main_GE_1638(i709', ar_0, arityPad')) [ static'1 <= static''' + 1 /\ 0 <= static''' /\ static''' <= ar_2 + 2 /\ 0 <= ar_2 /\ 0 <= static'1 /\ 1 <= ar_1 /\ 0 < ar_1 ]
We thus obtain the following problem:
7: T:
(Comp: 1, Cost: 23) main_Load_1(ar_0, ar_1, ar_2) -> Com_1(main_GE_1638(i709', ar_0, arityPad')) [ static'1 <= static''' + 1 /\ 0 <= static''' /\ static''' <= ar_2 + 2 /\ 0 <= ar_2 /\ 0 <= static'1 /\ 1 <= ar_1 /\ 0 < ar_1 ]
(Comp: ar_0, Cost: 25) main_GE_1638(ar_0, ar_1, ar_2) -> Com_1(main_GE_1638(i709', ar_1 + ar_0 - 1, arityPad')) [ -ar_0 = i717' /\ ar_1 - 1 = i722' /\ ar_0 <= -1 /\ ar_1 - 1 = i739' /\ ar_0 < 0 /\ i739' - i717' = i749' /\ i722' - i717' = i727' /\ 1 <= i717' /\ 0 >= 0 /\ 1 <= ar_1 + ar_0 - 1 /\ 0 < ar_1 + ar_0 - 1 ]
(Comp: ?, Cost: 10) main_Store_1716(ar_0, ar_1, ar_2) -> Com_1(main_GE_1638(i709', ar_0, arityPad')) [ 0 >= 0 /\ 1 <= ar_1 /\ 0 < ar_1 ]
(Comp: 1, Cost: 8) main_Load_1610(ar_0, ar_1, ar_2) -> Com_1(main_GE_1638(i709', ar_0, arityPad)) [ 1 <= ar_1 /\ 0 < ar_1 ]
(Comp: ?, Cost: 12) main_GE_1638(ar_0, ar_1, ar_2) -> Com_1(main_Store_1716(i731' - ar_0, ar_1 - ar_0 - 1, arityPad)) [ ar_1 - 1 = i718' /\ i731' - ar_0 = i737' /\ 0 <= ar_0 /\ i718' - ar_0 = i720' /\ ar_1 - 1 = i731' ]
(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

Testing for reachability in the complexity graph removes the following transition from problem 7:
main_Load_1610(ar_0, ar_1, ar_2) -> Com_1(main_GE_1638(i709', ar_0, arityPad)) [ 1 <= ar_1 /\ 0 < ar_1 ]
We thus obtain the following problem:
8: T:
(Comp: ?, Cost: 10) main_Store_1716(ar_0, ar_1, ar_2) -> Com_1(main_GE_1638(i709', ar_0, arityPad')) [ 0 >= 0 /\ 1 <= ar_1 /\ 0 < ar_1 ]
(Comp: ar_0, Cost: 25) main_GE_1638(ar_0, ar_1, ar_2) -> Com_1(main_GE_1638(i709', ar_1 + ar_0 - 1, arityPad')) [ -ar_0 = i717' /\ ar_1 - 1 = i722' /\ ar_0 <= -1 /\ ar_1 - 1 = i739' /\ ar_0 < 0 /\ i739' - i717' = i749' /\ i722' - i717' = i727' /\ 1 <= i717' /\ 0 >= 0 /\ 1 <= ar_1 + ar_0 - 1 /\ 0 < ar_1 + ar_0 - 1 ]
(Comp: ?, Cost: 12) main_GE_1638(ar_0, ar_1, ar_2) -> Com_1(main_Store_1716(i731' - ar_0, ar_1 - ar_0 - 1, arityPad)) [ ar_1 - 1 = i718' /\ i731' - ar_0 = i737' /\ 0 <= ar_0 /\ i718' - ar_0 = i720' /\ ar_1 - 1 = i731' ]
(Comp: 1, Cost: 23) main_Load_1(ar_0, ar_1, ar_2) -> Com_1(main_GE_1638(i709', ar_0, arityPad')) [ static'1 <= static''' + 1 /\ 0 <= static''' /\ static''' <= ar_2 + 2 /\ 0 <= ar_2 /\ 0 <= static'1 /\ 1 <= ar_1 /\ 0 < ar_1 ]
(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

By chaining the transition main_GE_1638(ar_0, ar_1, ar_2) -> Com_1(main_Store_1716(i731' - ar_0, ar_1 - ar_0 - 1, arityPad)) [ ar_1 - 1 = i718' /\ i731' - ar_0 = i737' /\ 0 <= ar_0 /\ i718' - ar_0 = i720' /\ ar_1 - 1 = i731' ] with all transitions in problem 8, the following new transition is obtained:
main_GE_1638(ar_0, ar_1, ar_2) -> Com_1(main_GE_1638(i709', i731' - ar_0, arityPad')) [ ar_1 - 1 = i718' /\ i731' - ar_0 = i737' /\ 0 <= ar_0 /\ i718' - ar_0 = i720' /\ ar_1 - 1 = i731' /\ 0 >= 0 /\ 1 <= ar_1 - ar_0 - 1 /\ 0 < ar_1 - ar_0 - 1 ]
We thus obtain the following problem:
9: T:
(Comp: ?, Cost: 22) main_GE_1638(ar_0, ar_1, ar_2) -> Com_1(main_GE_1638(i709', i731' - ar_0, arityPad')) [ ar_1 - 1 = i718' /\ i731' - ar_0 = i737' /\ 0 <= ar_0 /\ i718' - ar_0 = i720' /\ ar_1 - 1 = i731' /\ 0 >= 0 /\ 1 <= ar_1 - ar_0 - 1 /\ 0 < ar_1 - ar_0 - 1 ]
(Comp: ?, Cost: 10) main_Store_1716(ar_0, ar_1, ar_2) -> Com_1(main_GE_1638(i709', ar_0, arityPad')) [ 0 >= 0 /\ 1 <= ar_1 /\ 0 < ar_1 ]
(Comp: ar_0, Cost: 25) main_GE_1638(ar_0, ar_1, ar_2) -> Com_1(main_GE_1638(i709', ar_1 + ar_0 - 1, arityPad')) [ -ar_0 = i717' /\ ar_1 - 1 = i722' /\ ar_0 <= -1 /\ ar_1 - 1 = i739' /\ ar_0 < 0 /\ i739' - i717' = i749' /\ i722' - i717' = i727' /\ 1 <= i717' /\ 0 >= 0 /\ 1 <= ar_1 + ar_0 - 1 /\ 0 < ar_1 + ar_0 - 1 ]
(Comp: 1, Cost: 23) main_Load_1(ar_0, ar_1, ar_2) -> Com_1(main_GE_1638(i709', ar_0, arityPad')) [ static'1 <= static''' + 1 /\ 0 <= static''' /\ static''' <= ar_2 + 2 /\ 0 <= ar_2 /\ 0 <= static'1 /\ 1 <= ar_1 /\ 0 < ar_1 ]
(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

Testing for reachability in the complexity graph removes the following transition from problem 9:
main_Store_1716(ar_0, ar_1, ar_2) -> Com_1(main_GE_1638(i709', ar_0, arityPad')) [ 0 >= 0 /\ 1 <= ar_1 /\ 0 < ar_1 ]
We thus obtain the following problem:
10: T:
(Comp: ?, Cost: 22) main_GE_1638(ar_0, ar_1, ar_2) -> Com_1(main_GE_1638(i709', i731' - ar_0, arityPad')) [ ar_1 - 1 = i718' /\ i731' - ar_0 = i737' /\ 0 <= ar_0 /\ i718' - ar_0 = i720' /\ ar_1 - 1 = i731' /\ 0 >= 0 /\ 1 <= ar_1 - ar_0 - 1 /\ 0 < ar_1 - ar_0 - 1 ]
(Comp: ar_0, Cost: 25) main_GE_1638(ar_0, ar_1, ar_2) -> Com_1(main_GE_1638(i709', ar_1 + ar_0 - 1, arityPad')) [ -ar_0 = i717' /\ ar_1 - 1 = i722' /\ ar_0 <= -1 /\ ar_1 - 1 = i739' /\ ar_0 < 0 /\ i739' - i717' = i749' /\ i722' - i717' = i727' /\ 1 <= i717' /\ 0 >= 0 /\ 1 <= ar_1 + ar_0 - 1 /\ 0 < ar_1 + ar_0 - 1 ]
(Comp: 1, Cost: 23) main_Load_1(ar_0, ar_1, ar_2) -> Com_1(main_GE_1638(i709', ar_0, arityPad')) [ static'1 <= static''' + 1 /\ 0 <= static''' /\ static''' <= ar_2 + 2 /\ 0 <= ar_2 /\ 0 <= static'1 /\ 1 <= ar_1 /\ 0 < ar_1 ]
(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_GE_1638) = V_2
Pol(main_Load_1) = V_1
Pol(koat_start) = V_1
orients all transitions weakly and the transition
main_GE_1638(ar_0, ar_1, ar_2) -> Com_1(main_GE_1638(i709', i731' - ar_0, arityPad')) [ ar_1 - 1 = i718' /\ i731' - ar_0 = i737' /\ 0 <= ar_0 /\ i718' - ar_0 = i720' /\ ar_1 - 1 = i731' /\ 0 >= 0 /\ 1 <= ar_1 - ar_0 - 1 /\ 0 < ar_1 - ar_0 - 1 ]
strictly and produces the following problem:
11: T:
(Comp: ar_0, Cost: 22) main_GE_1638(ar_0, ar_1, ar_2) -> Com_1(main_GE_1638(i709', i731' - ar_0, arityPad')) [ ar_1 - 1 = i718' /\ i731' - ar_0 = i737' /\ 0 <= ar_0 /\ i718' - ar_0 = i720' /\ ar_1 - 1 = i731' /\ 0 >= 0 /\ 1 <= ar_1 - ar_0 - 1 /\ 0 < ar_1 - ar_0 - 1 ]
(Comp: ar_0, Cost: 25) main_GE_1638(ar_0, ar_1, ar_2) -> Com_1(main_GE_1638(i709', ar_1 + ar_0 - 1, arityPad')) [ -ar_0 = i717' /\ ar_1 - 1 = i722' /\ ar_0 <= -1 /\ ar_1 - 1 = i739' /\ ar_0 < 0 /\ i739' - i717' = i749' /\ i722' - i717' = i727' /\ 1 <= i717' /\ 0 >= 0 /\ 1 <= ar_1 + ar_0 - 1 /\ 0 < ar_1 + ar_0 - 1 ]
(Comp: 1, Cost: 23) main_Load_1(ar_0, ar_1, ar_2) -> Com_1(main_GE_1638(i709', ar_0, arityPad')) [ static'1 <= static''' + 1 /\ 0 <= static''' /\ static''' <= ar_2 + 2 /\ 0 <= ar_2 /\ 0 <= static'1 /\ 1 <= ar_1 /\ 0 < ar_1 ]
(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 47*ar_0 + 23

Time: 0.652 sec (SMT: 0.532 sec)

(0) Obligation:

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

(2) Obligation:

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

(4) Obligation:

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

(6) Obligation:

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

(8) Obligation:

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

(10) Obligation:

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

(12) Obligation:

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

(14) Obligation:

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

(16) Obligation:

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

(18) Obligation:

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

(20) Obligation:

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

(22) Obligation:

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

(24) Obligation:

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

(26) Obligation:

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

(28) Obligation:

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

(30) Obligation:

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

(32) Obligation:

(33) koat Proof (EQUIVALENT transformation)

(34) BOUNDS(CONSTANT, 23 + 47 * |#0|)