time complexity proof of /tmp/tmpJuce9X/CyclicList.jar

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

0 JBC problem

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

↳2 JBCTerminationGraph

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

↳4 JBCComplexityEdges

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

    ↳6 WeightedIntTrs

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

        ↳8 WeightedIntTrs

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

        ↳10 WeightedIntTrs

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

        ↳12 WeightedIntTrs

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

        ↳14 WeightedIntTrs

    ↳15 JBCGraphEdgesToCpxIntTrsProof (CONCRETE UPPER BOUND(ID), 201 ms)

    ↳16 WeightedIntTrs

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

        ↳18 WeightedIntTrs

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

        ↳20 WeightedIntTrs

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

        ↳22 WeightedIntTrs

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

        ↳24 WeightedIntTrs

        ↳25 CESProof (⇔, 462 ms)

        ↳26 BOUNDS(CONSTANT, max(31 + 15 * #0, max(39 + 7 * #1, 46) + max(-15 + 15 * #0, 15), 61))

↳27 TerminationGraphToComplexityProof (BOTH CONCRETE BOUNDS(ID, ADD(10)), 7 ms)

↳28 JBCComplexityEdges

    ↳29 JBCGraphEdgesToCpxIntTrsProof (CONCRETE UPPER BOUND(ID), 165 ms)

    ↳30 WeightedIntTrs

    ↳31 StraightLineCodeCompressionProof (BOTH CONCRETE BOUNDS(ID, ID), 80 ms)

    ↳32 WeightedIntTrs

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

    ↳34 WeightedIntTrs

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

    ↳36 WeightedIntTrs

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

    ↳38 WeightedIntTrs

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

    ↳40 WeightedIntTrs

    ↳41 koat Proof (⇔, 393 ms)

    ↳42 BOUNDS(CONSTANT, 116 + 30 * |#0| + 34 * |#1|)

(0) Obligation:

Need to prove time_complexity of the following program:

/**
 * This class represents a list. The function get(n) can be used to access
 * the n-th element.
 * @author Marc Brockschmidt
 */
public class CyclicList {
	/**
	 * A reference to the next list element.
	 */
	private CyclicList next;

    public static void main(int i, int j) {
		CyclicList list = CyclicList.create(i);
		list.get(j);
	}

	/**
	 * Create a new list element.
	 * @param n a reference to the next element.
	 */
	public CyclicList(final CyclicList n) {
		this.next = n;
	}

	/**
	 * Create a new cyclical list of a length l.
	 * @param l some length
	 * @return cyclical list of length max(1, l)
	 */
	public static CyclicList create(int x) {
		CyclicList last, current;
		last = current = new CyclicList(null);
		while (--x > 0)
			current = new CyclicList(current);
		return last.next = current;
	}

	public CyclicList get(int n) {
		CyclicList cur = this;
		while (--n > 0) {
			cur = cur.next;
		}
		return cur;
	}
}

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

Constructed TerminationGraph.

(2) Obligation:

Termination Graph based on JBC Program:
CyclicList.main(II)V: Graph of 133 nodes with 3 SCCs.

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

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

(4) Obligation:

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

Used field analysis yielded the following read fields:
- CyclicList: [next]

Considered paths: nonterm paths and paths from start to sinks

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

Transformed 127 jbc graph edges to a weighted ITS with 127 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 127 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_4(i1, i4, env, static) :|: 0 >= 0
main_Load_4(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_16(iconst_0, i1, i4, env, static) :|: iconst_0 = 0
langle_clinit_rangle_ArrayCreate_16(iconst_0, i1, i4, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_17(a2, i1, i4, iconst_0, env, static) :|: a2 = 2 && iconst_0 = 0 && 0 < a2
langle_clinit_rangle_FieldAccess_17(a2, i1, i4, iconst_0, env, static) -{1,1}> langle_clinit_rangle_New_18(i1, i4, env, static') :|: 0 <= a2 && iconst_0 = 0 && static' <= static + a2 && 0 <= static && 0 < a2
langle_clinit_rangle_New_18(i1, i4, env, static) -{0,0}> langle_clinit_rangle_New_20(i1, i4, env, static) :|: 0 >= 0
langle_clinit_rangle_New_20(i1, i4, env, static) -{0,0}> langle_clinit_rangle_New_22(i1, i4, env, static) :|: 0 <= static
langle_clinit_rangle_New_22(i1, i4, env, static) -{1,1}> langle_clinit_rangle_Duplicate_24(o2, i1, i4, env, static) :|: 0 < o2 && o2 = 1
langle_clinit_rangle_Duplicate_24(o2, i1, i4, env, static) -{1,1}> langle_clinit_rangle_ConstantStackPush_25(o2, i1, i4, env, static) :|: 0 < o2
langle_clinit_rangle_ConstantStackPush_25(o2, i1, i4, env, static) -{1,1}> langle_clinit_rangle_InvokeMethod_28(o2, NULL, i1, i4, env, static) :|: NULL = 0 && 0 < o2
langle_clinit_rangle_InvokeMethod_28(o2, NULL, i1, i4, env, static) -{1,1}> langle_init_rangle_Load_30(o2, i1, i4, env, static) :|: NULL = 0 && 0 < o2
langle_init_rangle_Load_30(o2, i1, i4, env, static) -{1,1}> langle_init_rangle_InvokeMethod_32(o2, i1, i4, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_32(o2, i1, i4, env, static) -{1,1}> langle_init_rangle_Load_34(o2, i1, i4, env, static) :|: 0 < o2
langle_init_rangle_Load_34(o2, i1, i4, env, static) -{1,1}> langle_init_rangle_InvokeMethod_36(o2, i1, i4, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_36(o2, i1, i4, env, static) -{1,1}> langle_init_rangle_Return_37(o2, i1, i4, env, static) :|: 0 < o2
langle_init_rangle_Return_37(o2, i1, i4, env, static) -{1,1}> langle_init_rangle_Return_40(o2, i1, i4, env, static) :|: 0 < o2
langle_init_rangle_Return_40(o2, i1, i4, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_41(o2, i1, i4, env, static) :|: 0 < o2
langle_clinit_rangle_FieldAccess_41(o2, i1, i4, env, static) -{1,1}> langle_clinit_rangle_Return_42(i1, i4, env, static') :|: 0 < o2 && 0 <= o2 && 0 <= static && static' <= static + o2
langle_clinit_rangle_Return_42(i1, i4, env, static) -{1,1}> main_Load_43(i1, i4, env, static) :|: 0 >= 0
main_Load_43(i1, i4, env, static) -{0,0}> main_Load_44(i1, i4, env, static) :|: 0 >= 0
main_Load_44(i1, i4, env, static) -{0,0}> main_Load_47(i1, i4, env, static) :|: 0 <= static
main_Load_47(i1, i4, env, static) -{0,0}> main_Load_48(i1, i4, env, static) :|: 0 >= 0
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) -{1,1}> main_InvokeMethod_51(i1, i4, env, static) :|: 0 >= 0
main_InvokeMethod_51(i1, i4, env, static) -{1,1}> create_New_52(i1, i4, env, static) :|: 0 >= 0
create_New_52(i1, i4, env, static) -{1,1}> create_Duplicate_54(o4, i1, i4, NULL, env, static) :|: NULL = 0 && o4 = 1 && 0 < o4
create_Duplicate_54(o4, i1, i4, NULL, env, static) -{1,1}> create_ConstantStackPush_56(o4, i1, i4, NULL, env, static) :|: NULL = 0 && 0 < o4
create_ConstantStackPush_56(o4, i1, i4, NULL, env, static) -{1,1}> create_InvokeMethod_59(o4, NULL, i1, i4, env, static) :|: NULL = 0 && 0 < o4
create_InvokeMethod_59(o4, NULL, i1, i4, env, static) -{1,1}> langle_init_rangle_Load_60(o4, NULL, i1, i4, env, static) :|: NULL = 0 && 0 < o4
langle_init_rangle_Load_60(o4, NULL, i1, i4, env, static) -{1,1}> langle_init_rangle_InvokeMethod_63(o4, NULL, i1, i4, env, static) :|: NULL = 0 && 0 < o4
langle_init_rangle_InvokeMethod_63(o4, NULL, i1, i4, env, static) -{1,1}> langle_init_rangle_Load_65(o4, NULL, i1, i4, env, static) :|: NULL = 0 && 0 < o4
langle_init_rangle_Load_65(o4, NULL, i1, i4, env, static) -{1,1}> langle_init_rangle_Load_67(o4, NULL, i1, i4, env, static) :|: NULL = 0 && 0 < o4
langle_init_rangle_Load_67(o4, NULL, i1, i4, env, static) -{1,1}> langle_init_rangle_FieldAccess_68(o4, NULL, i1, i4, env, static) :|: NULL = 0 && 0 < o4
langle_init_rangle_FieldAccess_68(o4, NULL, i1, i4, env, static) -{1,1}> langle_init_rangle_Return_70(o4', i1, i4, NULL, env, static) :|: NULL = 0 && o4' = o4 + NULL && 0 < o4 && o4' <= o4 + NULL && 0 < o4'
langle_init_rangle_Return_70(o4, i1, i4, NULL, env, static) -{1,1}> create_Duplicate_72(o4, i1, i4, NULL, env, static) :|: NULL = 0 && 0 < o4
create_Duplicate_72(o4, i1, i4, NULL, env, static) -{1,1}> create_Store_74(o4, i1, i4, NULL, env, static) :|: NULL = 0 && 0 < o4
create_Store_74(o4, i1, i4, NULL, env, static) -{1,1}> create_Store_77(o4, i1, i4, NULL, env, static) :|: NULL = 0 && 0 < o4
create_Store_77(o4, i1, i4, NULL, env, static) -{1,1}> create_Inc_78(i1, o4, i4, NULL, env, static) :|: NULL = 0 && 0 < o4
create_Inc_78(i1, o4, i4, NULL, env, static) -{1,1}> create_Load_79(i6, o4, i1, i4, NULL, env, static) :|: NULL = 0 && 0 < o4 && i1 + -1 = i6
create_Load_79(i6, o4, i1, i4, NULL, env, static) -{1,1}> create_LE_84(i6, o4, i1, i4, NULL, env, static) :|: NULL = 0 && 0 < o4
create_LE_84(i16, o4, i1, i4, NULL, env, static) -{0,0}> create_LE_86(i16, o4, i1, i4, NULL, env, static) :|: NULL = 0 && 0 < o4 && i16 <= 0
create_LE_84(i17, o4, i18, i4, NULL, env, static) -{0,0}> create_LE_87(i17, o4, i18, i4, NULL, env, static) :|: NULL = 0 && 0 < o4 && 1 <= i17 && 2 <= i18
create_LE_86(i16, o4, i1, i4, NULL, env, static) -{1,1}> create_Load_90(o4, i1, i4, NULL, env, static) :|: NULL = 0 && 0 < o4 && i16 <= 0
create_LE_87(i17, o4, i18, i4, NULL, env, static) -{1,1}> create_New_92(i17, o4, i18, i4, NULL, env, static) :|: NULL = 0 && 0 < o4 && 0 < i17 && 1 <= i17 && 2 <= i18
create_Load_90(o4, i1, i4, NULL, env, static) -{1,1}> create_Load_94(o4, i1, i4, NULL, env, static) :|: NULL = 0 && 0 < o4
create_New_92(i17, o4, i18, i4, NULL, env, static) -{1,1}> create_Duplicate_97(o6, i17, o4, i18, i4, NULL, env, static) :|: NULL = 0 && 0 < o6 && 0 < o4 && o6 = 1 && 1 <= i17 && 2 <= i18
create_Load_94(o4, i1, i4, NULL, env, static) -{1,1}> create_Duplicate_99(o4, i1, i4, NULL, env, static) :|: NULL = 0 && 0 < o4
create_Duplicate_97(o6, i17, o4, i18, i4, NULL, env, static) -{0,0}> create_Duplicate_690(o6, i17, o4, o4, i18, i4, NULL, env, static) :|: NULL = 0 && 0 < o6 && 0 < o4 && 1 <= i17 && 2 <= i18
create_Duplicate_99(o4, i1, i4, NULL, env, static) -{1,1}> create_FieldAccess_101(o4, i1, i4, NULL, env, static) :|: NULL = 0 && 0 < o4
create_FieldAccess_101(o4, i1, i4, NULL, env, static) -{1,1}> create_Return_104(o4', i1, i4, env, static) :|: NULL = 0 && 0 < o4 && o4' <= o4 + o4 && o4' = o4 && 0 < o4'
create_Return_104(o4, i1, i4, env, static) -{1,1}> main_Store_108(i1, i4, o4, env, static) :|: 0 < o4
main_Store_108(i1, i4, o4, env, static) -{1,1}> main_Load_110(i1, i4, o4, env, static) :|: 0 < o4
main_Load_110(i1, i4, o4, env, static) -{1,1}> main_Load_119(i1, i4, o4, env, static) :|: 0 < o4
main_Load_119(i1, i4, o4, env, static) -{1,1}> main_InvokeMethod_124(i1, i4, o4, env, static) :|: 0 < o4
main_InvokeMethod_124(i1, i4, o4, env, static) -{1,1}> get_Load_129(o4, i4, i1, env, static) :|: 0 < o4
get_Load_129(o4, i4, i1, env, static) -{1,1}> get_Store_139(o4, i4, i1, env, static) :|: 0 < o4
get_Store_139(o4, i4, i1, env, static) -{1,1}> get_Inc_143(i4, o4, i1, env, static) :|: 0 < o4
get_Inc_143(i4, o4, i1, env, static) -{0,0}> get_Inc_570(i4, o4, i1, i4, env, static) :|: 0 < o4
get_Inc_570(i103, o67, i1, i104, env, static) -{1,1}> get_Load_607(i120, o67, i1, i104, env, static) :|: 0 < o67 && i103 + -1 = i120
get_Load_607(i120, o67, i1, i104, env, static) -{1,1}> get_LE_609(i120, o67, i1, i104, env, static) :|: 0 < o67
get_LE_609(i125, o67, i1, i104, env, static) -{0,0}> get_LE_610(i125, o67, i1, i104, env, static) :|: 0 < o67 && i125 <= 0
get_LE_609(i126, o67, i1, i104, env, static) -{0,0}> get_LE_611(i126, o67, i1, i104, env, static) :|: 0 < o67 && 1 <= i126
get_LE_611(i126, o67, i1, i104, env, static) -{1,1}> get_Load_614(i126, o67, i1, i104, env, static) :|: 0 < o67 && 0 < i126 && 1 <= i126
get_Load_614(i126, o67, i1, i104, env, static) -{1,1}> get_FieldAccess_622(o67, i126, i1, i104, env, static) :|: 0 < o67 && 1 <= i126
get_FieldAccess_622(o67, i126, i1, i104, env, static) -{1,1}> get_Store_630(o67, i126, i1, i104, env, static) :|: 0 < o67 && 1 <= i126
get_Store_630(o67, i126, i1, i104, env, static) -{1,1}> get_JMP_638(i126, o67, i1, i104, env, static) :|: 0 < o67 && 1 <= i126
get_JMP_638(i126, o67, i1, i104, env, static) -{1,1}> get_Inc_654(i126, o67, i1, i104, env, static) :|: 0 < o67 && 1 <= i126
get_Inc_654(i126, o67, i1, i104, env, static) -{0,0}> get_Inc_570(i126, o67, i1, i104, env, static) :|: 0 < o67 && 1 <= i126
create_Duplicate_690(o112, i145, o110, o111, i18, i4, NULL, env, static) -{1,1}> create_Load_693(o112, i145, o110, o111, i18, i4, NULL, env, static) :|: NULL = 0 && 0 < o110 && 0 < o112 && 0 < o111 && 2 <= i18 && 1 <= i145
create_Load_693(o112, i145, o110, o111, i18, i4, NULL, env, static) -{1,1}> create_InvokeMethod_695(o112, o111, i145, o110, i18, i4, NULL, env, static) :|: NULL = 0 && 0 < o110 && 0 < o112 && 0 < o111 && 2 <= i18 && 1 <= i145
create_InvokeMethod_695(o112, o111, i145, o110, i18, i4, NULL, env, static) -{1,1}> langle_init_rangle_Load_697(o112, o111, i145, o110, i18, i4, NULL, env, static) :|: NULL = 0 && 0 < o110 && 0 < o112 && 0 < o111 && 2 <= i18 && 1 <= i145
langle_init_rangle_Load_697(o112, o111, i145, o110, i18, i4, NULL, env, static) -{1,1}> langle_init_rangle_InvokeMethod_698(o112, o111, i145, o110, i18, i4, NULL, env, static) :|: NULL = 0 && 0 < o110 && 0 < o112 && 0 < o111 && 2 <= i18 && 1 <= i145
langle_init_rangle_InvokeMethod_698(o112, o111, i145, o110, i18, i4, NULL, env, static) -{1,1}> langle_init_rangle_Load_699(o112, o111, i145, o110, i18, i4, NULL, env, static) :|: NULL = 0 && 0 < o110 && 0 < o112 && 0 < o111 && 2 <= i18 && 1 <= i145
langle_init_rangle_Load_699(o112, o111, i145, o110, i18, i4, NULL, env, static) -{1,1}> langle_init_rangle_Load_701(o112, o111, i145, o110, i18, i4, NULL, env, static) :|: NULL = 0 && 0 < o110 && 0 < o112 && 0 < o111 && 2 <= i18 && 1 <= i145
langle_init_rangle_Load_701(o112, o111, i145, o110, i18, i4, NULL, env, static) -{1,1}> langle_init_rangle_FieldAccess_703(o112, o111, i145, o110, i18, i4, NULL, env, static) :|: NULL = 0 && 0 < o110 && 0 < o112 && 0 < o111 && 2 <= i18 && 1 <= i145
langle_init_rangle_FieldAccess_703(o112, o111, i145, o110, i18, i4, NULL, env, static) -{1,1}> langle_init_rangle_Return_708(o112', i145, o110, i18, i4, o111, NULL, env, static) :|: NULL = 0 && 0 < o112' && 0 < o110 && o112' = o112 + o111 && 0 < o112 && 0 < o111 && 2 <= i18 && o112' <= o112 + o111 && 1 <= i145
langle_init_rangle_Return_708(o112, i145, o110, i18, i4, o111, NULL, env, static) -{1,1}> create_Store_710(o112, i145, o110, i18, i4, o111, NULL, env, static) :|: NULL = 0 && 0 < o110 && 0 < o112 && 0 < o111 && 2 <= i18 && 1 <= i145
create_Store_710(o112, i145, o110, i18, i4, o111, NULL, env, static) -{1,1}> create_JMP_712(i145, o110, o112, i18, i4, NULL, o111, env, static) :|: NULL = 0 && 0 < o110 && 0 < o112 && 0 < o111 && 2 <= i18 && 1 <= i145
create_JMP_712(i145, o110, o112, i18, i4, NULL, o111, env, static) -{1,1}> create_Inc_715(i145, o110, o112, i18, i4, NULL, o111, env, static) :|: NULL = 0 && 0 < o110 && 0 < o112 && 0 < o111 && 2 <= i18 && 1 <= i145
create_Inc_715(i145, o110, o112, i18, i4, NULL, o111, env, static) -{1,1}> create_Load_718(i151, o110, o112, i18, i4, NULL, o111, env, static) :|: NULL = 0 && 0 < o110 && 0 <= i151 && 0 < o112 && i145 + -1 = i151 && 0 < o111 && 2 <= i18 && 1 <= i145
create_Load_718(i151, o110, o112, i18, i4, NULL, o111, env, static) -{1,1}> create_LE_725(i151, o110, o112, i18, i4, NULL, o111, env, static) :|: NULL = 0 && 0 < o110 && 0 <= i151 && 0 < o112 && 0 < o111 && 2 <= i18
create_LE_725(iconst_0, o110, o112, i18, i4, NULL, o111, env, static) -{0,0}> create_LE_727(iconst_0, o110, o112, i18, i4, NULL, o111, env, static) :|: NULL = 0 && 0 < o110 && 0 <= iconst_0 && iconst_0 = 0 && 0 < o112 && 0 < o111 && 2 <= i18
create_LE_725(i158, o110, o112, i18, i4, NULL, o111, env, static) -{0,0}> create_LE_729(i158, o110, o112, i18, i4, NULL, o111, env, static) :|: NULL = 0 && 0 < o110 && 0 <= i158 && 1 <= i158 && 0 < o112 && 0 < o111 && 2 <= i18
create_LE_727(iconst_0, o110, o112, i18, i4, NULL, o111, env, static) -{1,1}> create_Load_732(o110, o112, i18, i4, NULL, o111, env, static) :|: NULL = 0 && 0 < o110 && iconst_0 <= 0 && iconst_0 = 0 && 0 < o112 && 0 < o111 && 2 <= i18
create_LE_729(i158, o110, o112, i18, i4, NULL, o111, env, static) -{1,1}> create_New_737(i158, o110, o112, i18, i4, NULL, o111, env, static) :|: NULL = 0 && 0 < o110 && 1 <= i158 && 0 < o112 && 0 < o111 && 2 <= i18 && 0 < i158
create_Load_732(o110, o112, i18, i4, NULL, o111, env, static) -{1,1}> create_Load_740(o110, o112, i18, i4, NULL, o111, env, static) :|: NULL = 0 && 0 < o110 && 0 < o112 && 0 < o111 && 2 <= i18
create_New_737(i158, o110, o112, i18, i4, NULL, o111, env, static) -{1,1}> create_Duplicate_743(o150, i158, o110, o112, i18, i4, NULL, o111, env, static) :|: NULL = 0 && 0 < o110 && 1 <= i158 && 0 < o112 && 0 < o150 && 0 < o111 && 2 <= i18 && o150 = 1
create_Load_740(o110, o112, i18, i4, NULL, o111, env, static) -{1,1}> create_Duplicate_746(o110, o112, i18, i4, NULL, o111, env, static) :|: NULL = 0 && 0 < o110 && 0 < o112 && 0 < o111 && 2 <= i18
create_Duplicate_743(o150, i158, o110, o112, i18, i4, NULL, o111, env, static) -{0,0}> create_Duplicate_690(o150, i158, o110, o112, i18, i4, NULL, env, static) :|: NULL = 0 && 0 < o110 && 1 <= i158 && 0 < o150 && 0 < o112 && 0 < o111 && 2 <= i18
create_Duplicate_746(o110, o112, i18, i4, NULL, o111, env, static) -{1,1}> create_FieldAccess_749(o112, o110, i18, i4, o111, NULL, env, static) :|: NULL = 0 && 0 < o110 && 0 < o112 && 0 < o111 && 2 <= i18
create_FieldAccess_749(o112, o110, i18, i4, o111, NULL, env, static) -{0,0}> create_FieldAccess_779(o112, o110, i18, i4, o111, NULL, env, static) :|: NULL = 0 && 0 < o110 && 0 < o112 && 0 < o111 && 2 <= i18
create_FieldAccess_749(o112, o163, i18, i4, o111, NULL, env, static) -{0,0}> create_FieldAccess_780(o112, o163, i18, i4, NULL, env, static) :|: NULL = 0 && 0 < o112 && 0 < o111 && 0 < o163 && 2 <= i18
create_FieldAccess_779(o112, o110, i18, i4, o111, NULL, env, static) -{1,1}> create_Return_797(o112, i18, i4, o111', env, static) :|: NULL = 0 && 0 < o110 && o111' <= o111 + o112 && 0 < o111' && 0 < o112 && 0 < o111 && 2 <= i18
create_FieldAccess_780(o112, o163, i18, i4, NULL, env, static) -{1,1}> create_Return_805(o112', i18, i4, o163', env, static) :|: NULL = 0 && 0 < o112' && o112' <= o112 + o112 && o163' <= o163 + o112 && 0 < o112 && 0 < o163 && 2 <= i18 && 0 < o163' && o163' = o163
create_Return_797(o112, i18, i4, o111, env, static) -{1,1}> main_Store_839(i18, i4, o112, o111, env, static) :|: 0 < o112 && 0 < o111 && 2 <= i18
create_Return_805(o112, i18, i4, o163, env, static) -{1,1}> main_Store_845(i18, i4, o112, o163, env, static) :|: 0 < o112 && 2 <= i18 && 0 < o163
main_Store_839(i18, i4, o112, o111, env, static) -{1,1}> main_Load_848(i18, i4, o112, o111, env, static) :|: 0 < o112 && 0 < o111 && 2 <= i18
main_Store_845(i18, i4, o112, o163, env, static) -{1,1}> main_Load_852(i18, i4, o112, o163, env, static) :|: 0 < o112 && 2 <= i18 && 0 < o163
main_Load_848(i18, i4, o112, o111, env, static) -{1,1}> main_Load_855(i18, i4, o112, o111, env, static) :|: 0 < o112 && 0 < o111 && 2 <= i18
main_Load_852(i18, i4, o112, o163, env, static) -{1,1}> main_Load_860(i18, i4, o112, o163, env, static) :|: 0 < o112 && 2 <= i18 && 0 < o163
main_Load_855(i18, i4, o112, o111, env, static) -{1,1}> main_InvokeMethod_862(i18, i4, o112, o111, env, static) :|: 0 < o112 && 0 < o111 && 2 <= i18
main_Load_860(i18, i4, o112, o163, env, static) -{1,1}> main_InvokeMethod_867(i18, i4, o112, o163, env, static) :|: 0 < o112 && 2 <= i18 && 0 < o163
main_InvokeMethod_862(i18, i4, o112, o111, env, static) -{1,1}> get_Load_869(o112, i4, i18, o111, env, static) :|: 0 < o112 && 0 < o111 && 2 <= i18
main_InvokeMethod_867(i18, i4, o112, o163, env, static) -{1,1}> get_Load_871(o112, i4, i18, o163, env, static) :|: 0 < o112 && 2 <= i18 && 0 < o163
get_Load_869(o112, i4, i18, o111, env, static) -{1,1}> get_Store_874(o112, i4, i18, o111, env, static) :|: 0 < o112 && 0 < o111 && 2 <= i18
get_Load_871(o112, i4, i18, o163, env, static) -{1,1}> get_Store_879(o112, i4, i18, o163, env, static) :|: 0 < o112 && 2 <= i18 && 0 < o163
get_Store_874(o112, i4, i18, o111, env, static) -{1,1}> get_Inc_880(i4, o112, i18, o111, env, static) :|: 0 < o112 && 0 < o111 && 2 <= i18
get_Store_879(o112, i4, i18, o163, env, static) -{1,1}> get_Inc_881(i4, o112, i18, o163, env, static) :|: 0 < o112 && 2 <= i18 && 0 < o163
get_Inc_880(i4, o112, i18, o111, env, static) -{0,0}> get_Inc_957(i4, o112, i18, i4, env, static) :|: 0 < o112 && 0 < o111 && 2 <= i18
get_Inc_881(i4, o112, i18, o163, env, static) -{0,0}> get_Inc_957(i4, o112, i18, i4, env, static) :|: 0 < o112 && 2 <= i18 && 0 < o163
get_Inc_957(i217, o276, i18, i218, env, static) -{1,1}> get_Load_962(i232, o276, i18, i218, env, static) :|: 0 < o276 && i217 + -1 = i232 && 2 <= i18
get_Load_962(i232, o276, i18, i218, env, static) -{1,1}> get_LE_964(i232, o276, i18, i218, env, static) :|: 0 < o276 && 2 <= i18
get_LE_964(i236, o276, i18, i218, env, static) -{0,0}> get_LE_968(i236, o276, i18, i218, env, static) :|: i236 <= 0 && 0 < o276 && 2 <= i18
get_LE_964(i237, o276, i18, i218, env, static) -{0,0}> get_LE_969(i237, o276, i18, i218, env, static) :|: 1 <= i237 && 0 < o276 && 2 <= i18
get_LE_969(i237, o276, i18, i218, env, static) -{1,1}> get_Load_976(i237, o276, i18, i218, env, static) :|: 1 <= i237 && 0 < o276 && 2 <= i18 && 0 < i237
get_Load_976(i237, o276, i18, i218, env, static) -{1,1}> get_FieldAccess_982(o276, i237, i18, i218, env, static) :|: 1 <= i237 && 0 < o276 && 2 <= i18
get_FieldAccess_982(o301, i237, i18, i218, env, static) -{0,0}> get_FieldAccess_993(o301, i237, i18, i218, o302, env, static) :|: 0 < o301 && 1 <= i237 && o302 <= o301 && 0 < o302 && 2 <= i18
get_FieldAccess_993(o301, i237, i18, i218, o302, env, static) -{0,0}> get_FieldAccess_1005(o301, i237, i18, i218, o302, env, static) :|: 0 < o301 && 1 <= i237 && 0 < o302 && 2 <= i18
get_FieldAccess_993(o306, i237, i18, i218, o302, env, static) -{0,0}> get_FieldAccess_1006(o306, i237, i18, i218, env, static) :|: 1 <= i237 && 0 < o306 && 0 < o302 && 2 <= i18
get_FieldAccess_1005(o301, i237, i18, i218, o302, env, static) -{1,1}> get_Store_1011(o302, i237, i18, i218, env, static) :|: 0 < o301 && 1 <= i237 && 0 < o302 && 2 <= i18
get_FieldAccess_1006(o306, i237, i18, i218, env, static) -{1,1}> get_Store_1016(o306, i237, i18, i218, env, static) :|: 1 <= i237 && 0 < o306 && 2 <= i18
get_Store_1011(o302, i237, i18, i218, env, static) -{1,1}> get_JMP_1019(i237, o302, i18, i218, env, static) :|: 1 <= i237 && 0 < o302 && 2 <= i18
get_Store_1016(o306, i237, i18, i218, env, static) -{1,1}> get_JMP_1023(i237, o306, i18, i218, env, static) :|: 1 <= i237 && 0 < o306 && 2 <= i18
get_JMP_1019(i237, o302, i18, i218, env, static) -{1,1}> get_Inc_1030(i237, o302, i18, i218, env, static) :|: 1 <= i237 && 0 < o302 && 2 <= i18
get_JMP_1023(i237, o306, i18, i218, env, static) -{1,1}> get_Inc_1040(i237, o306, i18, i218, env, static) :|: 1 <= i237 && 0 < o306 && 2 <= i18
get_Inc_1030(i237, o302, i18, i218, env, static) -{0,0}> get_Inc_957(i237, o302, i18, i218, env, static) :|: 1 <= i237 && 0 < o302 && 2 <= i18
get_Inc_1040(i237, o306, i18, i218, env, static) -{0,0}> get_Inc_957(i237, o306, i18, i218, env, static) :|: 1 <= i237 && 0 < o306 && 2 <= i18

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

obtained
main_Load_2(i1, i4, env, static) -{32,32}> create_LE_84(i6', o4''', i1, i4, 0, env, static'1) :|: static'1 <= static''' + 1 && 0 < o4''' && 0 <= 2 && o4''' <= 1 + 0 && 0 <= static''' && 0 < 1 && static''' <= static + 2 && o4''' = 1 + 0 && 0 <= 1 && 0 <= static && 0 <= static'1 && 0 >= 0 && 0 < 2 && i1 + -1 = i6'
by chaining
main_Load_2(i1, i4, env, static) -{0,0}> main_Load_4(i1, i4, env, static) :|: 0 >= 0
main_Load_4(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_16(iconst_0, i1, i4, env, static) :|: iconst_0 = 0
langle_clinit_rangle_ArrayCreate_16(iconst_0, i1, i4, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_17(a2, i1, i4, iconst_0, env, static) :|: a2 = 2 && iconst_0 = 0 && 0 < a2
langle_clinit_rangle_FieldAccess_17(a2, i1, i4, iconst_0, env, static) -{1,1}> langle_clinit_rangle_New_18(i1, i4, env, static') :|: 0 <= a2 && iconst_0 = 0 && static' <= static + a2 && 0 <= static && 0 < a2
langle_clinit_rangle_New_18(i1, i4, env, static) -{0,0}> langle_clinit_rangle_New_20(i1, i4, env, static) :|: 0 >= 0
langle_clinit_rangle_New_20(i1, i4, env, static) -{0,0}> langle_clinit_rangle_New_22(i1, i4, env, static) :|: 0 <= static
langle_clinit_rangle_New_22(i1, i4, env, static) -{1,1}> langle_clinit_rangle_Duplicate_24(o2, i1, i4, env, static) :|: 0 < o2 && o2 = 1
langle_clinit_rangle_Duplicate_24(o2, i1, i4, env, static) -{1,1}> langle_clinit_rangle_ConstantStackPush_25(o2, i1, i4, env, static) :|: 0 < o2
langle_clinit_rangle_ConstantStackPush_25(o2, i1, i4, env, static) -{1,1}> langle_clinit_rangle_InvokeMethod_28(o2, NULL, i1, i4, env, static) :|: NULL = 0 && 0 < o2
langle_clinit_rangle_InvokeMethod_28(o2, NULL, i1, i4, env, static) -{1,1}> langle_init_rangle_Load_30(o2, i1, i4, env, static) :|: NULL = 0 && 0 < o2
langle_init_rangle_Load_30(o2, i1, i4, env, static) -{1,1}> langle_init_rangle_InvokeMethod_32(o2, i1, i4, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_32(o2, i1, i4, env, static) -{1,1}> langle_init_rangle_Load_34(o2, i1, i4, env, static) :|: 0 < o2
langle_init_rangle_Load_34(o2, i1, i4, env, static) -{1,1}> langle_init_rangle_InvokeMethod_36(o2, i1, i4, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_36(o2, i1, i4, env, static) -{1,1}> langle_init_rangle_Return_37(o2, i1, i4, env, static) :|: 0 < o2
langle_init_rangle_Return_37(o2, i1, i4, env, static) -{1,1}> langle_init_rangle_Return_40(o2, i1, i4, env, static) :|: 0 < o2
langle_init_rangle_Return_40(o2, i1, i4, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_41(o2, i1, i4, env, static) :|: 0 < o2
langle_clinit_rangle_FieldAccess_41(o2, i1, i4, env, static) -{1,1}> langle_clinit_rangle_Return_42(i1, i4, env, static') :|: 0 < o2 && 0 <= o2 && 0 <= static && static' <= static + o2
langle_clinit_rangle_Return_42(i1, i4, env, static) -{1,1}> main_Load_43(i1, i4, env, static) :|: 0 >= 0
main_Load_43(i1, i4, env, static) -{0,0}> main_Load_44(i1, i4, env, static) :|: 0 >= 0
main_Load_44(i1, i4, env, static) -{0,0}> main_Load_47(i1, i4, env, static) :|: 0 <= static
main_Load_47(i1, i4, env, static) -{0,0}> main_Load_48(i1, i4, env, static) :|: 0 >= 0
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) -{1,1}> main_InvokeMethod_51(i1, i4, env, static) :|: 0 >= 0
main_InvokeMethod_51(i1, i4, env, static) -{1,1}> create_New_52(i1, i4, env, static) :|: 0 >= 0
create_New_52(i1, i4, env, static) -{1,1}> create_Duplicate_54(o4, i1, i4, NULL, env, static) :|: NULL = 0 && o4 = 1 && 0 < o4
create_Duplicate_54(o4, i1, i4, NULL, env, static) -{1,1}> create_ConstantStackPush_56(o4, i1, i4, NULL, env, static) :|: NULL = 0 && 0 < o4
create_ConstantStackPush_56(o4, i1, i4, NULL, env, static) -{1,1}> create_InvokeMethod_59(o4, NULL, i1, i4, env, static) :|: NULL = 0 && 0 < o4
create_InvokeMethod_59(o4, NULL, i1, i4, env, static) -{1,1}> langle_init_rangle_Load_60(o4, NULL, i1, i4, env, static) :|: NULL = 0 && 0 < o4
langle_init_rangle_Load_60(o4, NULL, i1, i4, env, static) -{1,1}> langle_init_rangle_InvokeMethod_63(o4, NULL, i1, i4, env, static) :|: NULL = 0 && 0 < o4
langle_init_rangle_InvokeMethod_63(o4, NULL, i1, i4, env, static) -{1,1}> langle_init_rangle_Load_65(o4, NULL, i1, i4, env, static) :|: NULL = 0 && 0 < o4
langle_init_rangle_Load_65(o4, NULL, i1, i4, env, static) -{1,1}> langle_init_rangle_Load_67(o4, NULL, i1, i4, env, static) :|: NULL = 0 && 0 < o4
langle_init_rangle_Load_67(o4, NULL, i1, i4, env, static) -{1,1}> langle_init_rangle_FieldAccess_68(o4, NULL, i1, i4, env, static) :|: NULL = 0 && 0 < o4
langle_init_rangle_FieldAccess_68(o4, NULL, i1, i4, env, static) -{1,1}> langle_init_rangle_Return_70(o4', i1, i4, NULL, env, static) :|: NULL = 0 && o4' = o4 + NULL && 0 < o4 && o4' <= o4 + NULL && 0 < o4'
langle_init_rangle_Return_70(o4, i1, i4, NULL, env, static) -{1,1}> create_Duplicate_72(o4, i1, i4, NULL, env, static) :|: NULL = 0 && 0 < o4
create_Duplicate_72(o4, i1, i4, NULL, env, static) -{1,1}> create_Store_74(o4, i1, i4, NULL, env, static) :|: NULL = 0 && 0 < o4
create_Store_74(o4, i1, i4, NULL, env, static) -{1,1}> create_Store_77(o4, i1, i4, NULL, env, static) :|: NULL = 0 && 0 < o4
create_Store_77(o4, i1, i4, NULL, env, static) -{1,1}> create_Inc_78(i1, o4, i4, NULL, env, static) :|: NULL = 0 && 0 < o4
create_Inc_78(i1, o4, i4, NULL, env, static) -{1,1}> create_Load_79(i6, o4, i1, i4, NULL, env, static) :|: NULL = 0 && 0 < o4 && i1 + -1 = i6
create_Load_79(i6, o4, i1, i4, NULL, env, static) -{1,1}> create_LE_84(i6, o4, i1, i4, NULL, env, static) :|: NULL = 0 && 0 < o4

obtained
create_LE_84(i17, o4, i18, i4, 0, env, static) -{2,2}> create_Duplicate_690(1, i17, o4, o4, i18, i4, 0, env, static) :|: 0 < 1 && 2 <= i18 && 1 <= i17 && 0 < o4 && 0 < i17
by chaining
create_LE_84(i17, o4, i18, i4, NULL, env, static) -{0,0}> create_LE_87(i17, o4, i18, i4, NULL, env, static) :|: NULL = 0 && 0 < o4 && 1 <= i17 && 2 <= i18
create_LE_87(i17, o4, i18, i4, NULL, env, static) -{1,1}> create_New_92(i17, o4, i18, i4, NULL, env, static) :|: NULL = 0 && 0 < o4 && 0 < i17 && 1 <= i17 && 2 <= i18
create_New_92(i17, o4, i18, i4, NULL, env, static) -{1,1}> create_Duplicate_97(o6, i17, o4, i18, i4, NULL, env, static) :|: NULL = 0 && 0 < o6 && 0 < o4 && o6 = 1 && 1 <= i17 && 2 <= i18
create_Duplicate_97(o6, i17, o4, i18, i4, NULL, env, static) -{0,0}> create_Duplicate_690(o6, i17, o4, o4, i18, i4, NULL, env, static) :|: NULL = 0 && 0 < o6 && 0 < o4 && 1 <= i17 && 2 <= i18

obtained
create_Duplicate_690(o112, i145, o110, o111, i18, i4, 0, env, static) -{13,13}> create_LE_725(i151', o110, o112''', i18, i4, 0, o111, env, static) :|: o112''' = o112 + o111 && 2 <= i18 && 0 <= i151' && 0 < o111 && 0 < o112''' && i145 + -1 = i151' && 0 < o110 && 0 < o112 && o112''' <= o112 + o111 && 1 <= i145
by chaining
create_Duplicate_690(o112, i145, o110, o111, i18, i4, NULL, env, static) -{1,1}> create_Load_693(o112, i145, o110, o111, i18, i4, NULL, env, static) :|: NULL = 0 && 0 < o110 && 0 < o112 && 0 < o111 && 2 <= i18 && 1 <= i145
create_Load_693(o112, i145, o110, o111, i18, i4, NULL, env, static) -{1,1}> create_InvokeMethod_695(o112, o111, i145, o110, i18, i4, NULL, env, static) :|: NULL = 0 && 0 < o110 && 0 < o112 && 0 < o111 && 2 <= i18 && 1 <= i145
create_InvokeMethod_695(o112, o111, i145, o110, i18, i4, NULL, env, static) -{1,1}> langle_init_rangle_Load_697(o112, o111, i145, o110, i18, i4, NULL, env, static) :|: NULL = 0 && 0 < o110 && 0 < o112 && 0 < o111 && 2 <= i18 && 1 <= i145
langle_init_rangle_Load_697(o112, o111, i145, o110, i18, i4, NULL, env, static) -{1,1}> langle_init_rangle_InvokeMethod_698(o112, o111, i145, o110, i18, i4, NULL, env, static) :|: NULL = 0 && 0 < o110 && 0 < o112 && 0 < o111 && 2 <= i18 && 1 <= i145
langle_init_rangle_InvokeMethod_698(o112, o111, i145, o110, i18, i4, NULL, env, static) -{1,1}> langle_init_rangle_Load_699(o112, o111, i145, o110, i18, i4, NULL, env, static) :|: NULL = 0 && 0 < o110 && 0 < o112 && 0 < o111 && 2 <= i18 && 1 <= i145
langle_init_rangle_Load_699(o112, o111, i145, o110, i18, i4, NULL, env, static) -{1,1}> langle_init_rangle_Load_701(o112, o111, i145, o110, i18, i4, NULL, env, static) :|: NULL = 0 && 0 < o110 && 0 < o112 && 0 < o111 && 2 <= i18 && 1 <= i145
langle_init_rangle_Load_701(o112, o111, i145, o110, i18, i4, NULL, env, static) -{1,1}> langle_init_rangle_FieldAccess_703(o112, o111, i145, o110, i18, i4, NULL, env, static) :|: NULL = 0 && 0 < o110 && 0 < o112 && 0 < o111 && 2 <= i18 && 1 <= i145
langle_init_rangle_FieldAccess_703(o112, o111, i145, o110, i18, i4, NULL, env, static) -{1,1}> langle_init_rangle_Return_708(o112', i145, o110, i18, i4, o111, NULL, env, static) :|: NULL = 0 && 0 < o112' && 0 < o110 && o112' = o112 + o111 && 0 < o112 && 0 < o111 && 2 <= i18 && o112' <= o112 + o111 && 1 <= i145
langle_init_rangle_Return_708(o112, i145, o110, i18, i4, o111, NULL, env, static) -{1,1}> create_Store_710(o112, i145, o110, i18, i4, o111, NULL, env, static) :|: NULL = 0 && 0 < o110 && 0 < o112 && 0 < o111 && 2 <= i18 && 1 <= i145
create_Store_710(o112, i145, o110, i18, i4, o111, NULL, env, static) -{1,1}> create_JMP_712(i145, o110, o112, i18, i4, NULL, o111, env, static) :|: NULL = 0 && 0 < o110 && 0 < o112 && 0 < o111 && 2 <= i18 && 1 <= i145
create_JMP_712(i145, o110, o112, i18, i4, NULL, o111, env, static) -{1,1}> create_Inc_715(i145, o110, o112, i18, i4, NULL, o111, env, static) :|: NULL = 0 && 0 < o110 && 0 < o112 && 0 < o111 && 2 <= i18 && 1 <= i145
create_Inc_715(i145, o110, o112, i18, i4, NULL, o111, env, static) -{1,1}> create_Load_718(i151, o110, o112, i18, i4, NULL, o111, env, static) :|: NULL = 0 && 0 < o110 && 0 <= i151 && 0 < o112 && i145 + -1 = i151 && 0 < o111 && 2 <= i18 && 1 <= i145
create_Load_718(i151, o110, o112, i18, i4, NULL, o111, env, static) -{1,1}> create_LE_725(i151, o110, o112, i18, i4, NULL, o111, env, static) :|: NULL = 0 && 0 < o110 && 0 <= i151 && 0 < o112 && 0 < o111 && 2 <= i18

obtained
create_LE_725(i158, o110, o112, i18, i4, 0, o111, env, static) -{2,2}> create_Duplicate_690(1, i158, o110, o112, i18, i4, 0, env, static) :|: 0 < i158 && 2 <= i18 && 0 < 1 && 0 < o111 && 0 < o112 && 1 <= i158 && 0 < o110 && 0 <= i158
by chaining
create_LE_725(i158, o110, o112, i18, i4, NULL, o111, env, static) -{0,0}> create_LE_729(i158, o110, o112, i18, i4, NULL, o111, env, static) :|: NULL = 0 && 0 < o110 && 0 <= i158 && 1 <= i158 && 0 < o112 && 0 < o111 && 2 <= i18
create_LE_729(i158, o110, o112, i18, i4, NULL, o111, env, static) -{1,1}> create_New_737(i158, o110, o112, i18, i4, NULL, o111, env, static) :|: NULL = 0 && 0 < o110 && 1 <= i158 && 0 < o112 && 0 < o111 && 2 <= i18 && 0 < i158
create_New_737(i158, o110, o112, i18, i4, NULL, o111, env, static) -{1,1}> create_Duplicate_743(o150, i158, o110, o112, i18, i4, NULL, o111, env, static) :|: NULL = 0 && 0 < o110 && 1 <= i158 && 0 < o112 && 0 < o150 && 0 < o111 && 2 <= i18 && o150 = 1
create_Duplicate_743(o150, i158, o110, o112, i18, i4, NULL, o111, env, static) -{0,0}> create_Duplicate_690(o150, i158, o110, o112, i18, i4, NULL, env, static) :|: NULL = 0 && 0 < o110 && 1 <= i158 && 0 < o150 && 0 < o112 && 0 < o111 && 2 <= i18

obtained
create_LE_725(0, o110, o112, i18, i4, 0, o111, env, static) -{4,4}> create_FieldAccess_749(o112, o110, i18, i4, o111, 0, env, static) :|: 0 < o110 && 2 <= i18 && 0 <= 0 && 0 < o111 && 0 < o112
by chaining
create_LE_725(iconst_0, o110, o112, i18, i4, NULL, o111, env, static) -{0,0}> create_LE_727(iconst_0, o110, o112, i18, i4, NULL, o111, env, static) :|: NULL = 0 && 0 < o110 && 0 <= iconst_0 && iconst_0 = 0 && 0 < o112 && 0 < o111 && 2 <= i18
create_LE_727(iconst_0, o110, o112, i18, i4, NULL, o111, env, static) -{1,1}> create_Load_732(o110, o112, i18, i4, NULL, o111, env, static) :|: NULL = 0 && 0 < o110 && iconst_0 <= 0 && iconst_0 = 0 && 0 < o112 && 0 < o111 && 2 <= i18
create_Load_732(o110, o112, i18, i4, NULL, o111, env, static) -{1,1}> create_Load_740(o110, o112, i18, i4, NULL, o111, env, static) :|: NULL = 0 && 0 < o110 && 0 < o112 && 0 < o111 && 2 <= i18
create_Load_740(o110, o112, i18, i4, NULL, o111, env, static) -{1,1}> create_Duplicate_746(o110, o112, i18, i4, NULL, o111, env, static) :|: NULL = 0 && 0 < o110 && 0 < o112 && 0 < o111 && 2 <= i18
create_Duplicate_746(o110, o112, i18, i4, NULL, o111, env, static) -{1,1}> create_FieldAccess_749(o112, o110, i18, i4, o111, NULL, env, static) :|: NULL = 0 && 0 < o110 && 0 < o112 && 0 < o111 && 2 <= i18

obtained
create_FieldAccess_749(o112, o163''', i18, i4, o111, 0, env, static) -{8,8}> get_Inc_957(i4, o112'1, i18, i4, env, static) :|: 0 < o111 && 0 < o163''' && 0 < o112 && 0 < o112'1 && 2 <= i18 && o163''' <= o163''' + o112 && o112'1 <= o112 + o112
by chaining
create_FieldAccess_749(o112, o163, i18, i4, o111, NULL, env, static) -{0,0}> create_FieldAccess_780(o112, o163, i18, i4, NULL, env, static) :|: NULL = 0 && 0 < o112 && 0 < o111 && 0 < o163 && 2 <= i18
create_FieldAccess_780(o112, o163, i18, i4, NULL, env, static) -{1,1}> create_Return_805(o112', i18, i4, o163', env, static) :|: NULL = 0 && 0 < o112' && o112' <= o112 + o112 && o163' <= o163 + o112 && 0 < o112 && 0 < o163 && 2 <= i18 && 0 < o163' && o163' = o163
create_Return_805(o112, i18, i4, o163, env, static) -{1,1}> main_Store_845(i18, i4, o112, o163, env, static) :|: 0 < o112 && 2 <= i18 && 0 < o163
main_Store_845(i18, i4, o112, o163, env, static) -{1,1}> main_Load_852(i18, i4, o112, o163, env, static) :|: 0 < o112 && 2 <= i18 && 0 < o163
main_Load_852(i18, i4, o112, o163, env, static) -{1,1}> main_Load_860(i18, i4, o112, o163, env, static) :|: 0 < o112 && 2 <= i18 && 0 < o163
main_Load_860(i18, i4, o112, o163, env, static) -{1,1}> main_InvokeMethod_867(i18, i4, o112, o163, env, static) :|: 0 < o112 && 2 <= i18 && 0 < o163
main_InvokeMethod_867(i18, i4, o112, o163, env, static) -{1,1}> get_Load_871(o112, i4, i18, o163, env, static) :|: 0 < o112 && 2 <= i18 && 0 < o163
get_Load_871(o112, i4, i18, o163, env, static) -{1,1}> get_Store_879(o112, i4, i18, o163, env, static) :|: 0 < o112 && 2 <= i18 && 0 < o163
get_Store_879(o112, i4, i18, o163, env, static) -{1,1}> get_Inc_881(i4, o112, i18, o163, env, static) :|: 0 < o112 && 2 <= i18 && 0 < o163
get_Inc_881(i4, o112, i18, o163, env, static) -{0,0}> get_Inc_957(i4, o112, i18, i4, env, static) :|: 0 < o112 && 2 <= i18 && 0 < o163

obtained
get_Inc_957(i217, o276, i18, i218, env, static) -{2,2}> get_LE_964(i232, o276, i18, i218, env, static) :|: 2 <= i18 && 0 < o276 && i217 + -1 = i232
by chaining
get_Inc_957(i217, o276, i18, i218, env, static) -{1,1}> get_Load_962(i232, o276, i18, i218, env, static) :|: 0 < o276 && i217 + -1 = i232 && 2 <= i18
get_Load_962(i232, o276, i18, i218, env, static) -{1,1}> get_LE_964(i232, o276, i18, i218, env, static) :|: 0 < o276 && 2 <= i18

obtained
get_LE_964(i237, o276, i18, i218, env, static) -{2,2}> get_FieldAccess_993(o276, i237, i18, i218, o302', env, static) :|: 0 < i237 && 2 <= i18 && 1 <= i237 && 0 < o302' && 0 < o276 && o302' <= o276
by chaining
get_LE_964(i237, o276, i18, i218, env, static) -{0,0}> get_LE_969(i237, o276, i18, i218, env, static) :|: 1 <= i237 && 0 < o276 && 2 <= i18
get_LE_969(i237, o276, i18, i218, env, static) -{1,1}> get_Load_976(i237, o276, i18, i218, env, static) :|: 1 <= i237 && 0 < o276 && 2 <= i18 && 0 < i237
get_Load_976(i237, o276, i18, i218, env, static) -{1,1}> get_FieldAccess_982(o276, i237, i18, i218, env, static) :|: 1 <= i237 && 0 < o276 && 2 <= i18
get_FieldAccess_982(o301, i237, i18, i218, env, static) -{0,0}> get_FieldAccess_993(o301, i237, i18, i218, o302, env, static) :|: 0 < o301 && 1 <= i237 && o302 <= o301 && 0 < o302 && 2 <= i18

obtained
get_FieldAccess_993(o306, i237, i18, i218, o302, env, static) -{3,3}> get_Inc_957(i237, o306, i18, i218, env, static) :|: 0 < o306 && 2 <= i18 && 1 <= i237 && 0 < o302
by chaining
get_FieldAccess_993(o306, i237, i18, i218, o302, env, static) -{0,0}> get_FieldAccess_1006(o306, i237, i18, i218, env, static) :|: 1 <= i237 && 0 < o306 && 0 < o302 && 2 <= i18
get_FieldAccess_1006(o306, i237, i18, i218, env, static) -{1,1}> get_Store_1016(o306, i237, i18, i218, env, static) :|: 1 <= i237 && 0 < o306 && 2 <= i18
get_Store_1016(o306, i237, i18, i218, env, static) -{1,1}> get_JMP_1023(i237, o306, i18, i218, env, static) :|: 1 <= i237 && 0 < o306 && 2 <= i18
get_JMP_1023(i237, o306, i18, i218, env, static) -{1,1}> get_Inc_1040(i237, o306, i18, i218, env, static) :|: 1 <= i237 && 0 < o306 && 2 <= i18
get_Inc_1040(i237, o306, i18, i218, env, static) -{0,0}> get_Inc_957(i237, o306, i18, i218, env, static) :|: 1 <= i237 && 0 < o306 && 2 <= i18

obtained
get_FieldAccess_993(o301, i237, i18, i218, o302, env, static) -{3,3}> get_Inc_957(i237, o302, i18, i218, env, static) :|: 1 <= i237 && 2 <= i18 && 0 < o301 && 0 < o302
by chaining
get_FieldAccess_993(o301, i237, i18, i218, o302, env, static) -{0,0}> get_FieldAccess_1005(o301, i237, i18, i218, o302, env, static) :|: 0 < o301 && 1 <= i237 && 0 < o302 && 2 <= i18
get_FieldAccess_1005(o301, i237, i18, i218, o302, env, static) -{1,1}> get_Store_1011(o302, i237, i18, i218, env, static) :|: 0 < o301 && 1 <= i237 && 0 < o302 && 2 <= i18
get_Store_1011(o302, i237, i18, i218, env, static) -{1,1}> get_JMP_1019(i237, o302, i18, i218, env, static) :|: 1 <= i237 && 0 < o302 && 2 <= i18
get_JMP_1019(i237, o302, i18, i218, env, static) -{1,1}> get_Inc_1030(i237, o302, i18, i218, env, static) :|: 1 <= i237 && 0 < o302 && 2 <= i18
get_Inc_1030(i237, o302, i18, i218, env, static) -{0,0}> get_Inc_957(i237, o302, i18, i218, env, static) :|: 1 <= i237 && 0 < o302 && 2 <= i18

obtained
create_FieldAccess_749(o112, o110, i18, i4, o111, 0, env, static) -{8,8}> get_Inc_957(i4, o112, i18, i4, env, static) :|: 0 < o111 && 2 <= i18 && 0 < o110 && 0 < o112 && 0 < o111''' && o111''' <= o111 + o112
by chaining
create_FieldAccess_749(o112, o110, i18, i4, o111, NULL, env, static) -{0,0}> create_FieldAccess_779(o112, o110, i18, i4, o111, NULL, env, static) :|: NULL = 0 && 0 < o110 && 0 < o112 && 0 < o111 && 2 <= i18
create_FieldAccess_779(o112, o110, i18, i4, o111, NULL, env, static) -{1,1}> create_Return_797(o112, i18, i4, o111', env, static) :|: NULL = 0 && 0 < o110 && o111' <= o111 + o112 && 0 < o111' && 0 < o112 && 0 < o111 && 2 <= i18
create_Return_797(o112, i18, i4, o111, env, static) -{1,1}> main_Store_839(i18, i4, o112, o111, env, static) :|: 0 < o112 && 0 < o111 && 2 <= i18
main_Store_839(i18, i4, o112, o111, env, static) -{1,1}> main_Load_848(i18, i4, o112, o111, env, static) :|: 0 < o112 && 0 < o111 && 2 <= i18
main_Load_848(i18, i4, o112, o111, env, static) -{1,1}> main_Load_855(i18, i4, o112, o111, env, static) :|: 0 < o112 && 0 < o111 && 2 <= i18
main_Load_855(i18, i4, o112, o111, env, static) -{1,1}> main_InvokeMethod_862(i18, i4, o112, o111, env, static) :|: 0 < o112 && 0 < o111 && 2 <= i18
main_InvokeMethod_862(i18, i4, o112, o111, env, static) -{1,1}> get_Load_869(o112, i4, i18, o111, env, static) :|: 0 < o112 && 0 < o111 && 2 <= i18
get_Load_869(o112, i4, i18, o111, env, static) -{1,1}> get_Store_874(o112, i4, i18, o111, env, static) :|: 0 < o112 && 0 < o111 && 2 <= i18
get_Store_874(o112, i4, i18, o111, env, static) -{1,1}> get_Inc_880(i4, o112, i18, o111, env, static) :|: 0 < o112 && 0 < o111 && 2 <= i18
get_Inc_880(i4, o112, i18, o111, env, static) -{0,0}> get_Inc_957(i4, o112, i18, i4, env, static) :|: 0 < o112 && 0 < o111 && 2 <= i18

obtained
create_LE_84(i16, o4'1, i1, i4, 0, env, static) -{12,12}> get_Inc_570(i4, o4'1, i1, i4, env, static) :|: 0 < o4'1 && i16 <= 0 && o4'1 <= o4'1 + o4'1
by chaining
create_LE_84(i16, o4, i1, i4, NULL, env, static) -{0,0}> create_LE_86(i16, o4, i1, i4, NULL, env, static) :|: NULL = 0 && 0 < o4 && i16 <= 0
create_LE_86(i16, o4, i1, i4, NULL, env, static) -{1,1}> create_Load_90(o4, i1, i4, NULL, env, static) :|: NULL = 0 && 0 < o4 && i16 <= 0
create_Load_90(o4, i1, i4, NULL, env, static) -{1,1}> create_Load_94(o4, i1, i4, NULL, env, static) :|: NULL = 0 && 0 < o4
create_Load_94(o4, i1, i4, NULL, env, static) -{1,1}> create_Duplicate_99(o4, i1, i4, NULL, env, static) :|: NULL = 0 && 0 < o4
create_Duplicate_99(o4, i1, i4, NULL, env, static) -{1,1}> create_FieldAccess_101(o4, i1, i4, NULL, env, static) :|: NULL = 0 && 0 < o4
create_FieldAccess_101(o4, i1, i4, NULL, env, static) -{1,1}> create_Return_104(o4', i1, i4, env, static) :|: NULL = 0 && 0 < o4 && o4' <= o4 + o4 && o4' = o4 && 0 < o4'
create_Return_104(o4, i1, i4, env, static) -{1,1}> main_Store_108(i1, i4, o4, env, static) :|: 0 < o4
main_Store_108(i1, i4, o4, env, static) -{1,1}> main_Load_110(i1, i4, o4, env, static) :|: 0 < o4
main_Load_110(i1, i4, o4, env, static) -{1,1}> main_Load_119(i1, i4, o4, env, static) :|: 0 < o4
main_Load_119(i1, i4, o4, env, static) -{1,1}> main_InvokeMethod_124(i1, i4, o4, env, static) :|: 0 < o4
main_InvokeMethod_124(i1, i4, o4, env, static) -{1,1}> get_Load_129(o4, i4, i1, env, static) :|: 0 < o4
get_Load_129(o4, i4, i1, env, static) -{1,1}> get_Store_139(o4, i4, i1, env, static) :|: 0 < o4
get_Store_139(o4, i4, i1, env, static) -{1,1}> get_Inc_143(i4, o4, i1, env, static) :|: 0 < o4
get_Inc_143(i4, o4, i1, env, static) -{0,0}> get_Inc_570(i4, o4, i1, i4, env, static) :|: 0 < o4

obtained
get_Inc_570(i103, o67, i1, i104, env, static) -{2,2}> get_LE_609(i120, o67, i1, i104, env, static) :|: 0 < o67 && i103 + -1 = i120
by chaining
get_Inc_570(i103, o67, i1, i104, env, static) -{1,1}> get_Load_607(i120, o67, i1, i104, env, static) :|: 0 < o67 && i103 + -1 = i120
get_Load_607(i120, o67, i1, i104, env, static) -{1,1}> get_LE_609(i120, o67, i1, i104, env, static) :|: 0 < o67

obtained
get_LE_609(i126, o67, i1, i104, env, static) -{5,5}> get_Inc_570(i126, o67, i1, i104, env, static) :|: 0 < i126 && 0 < o67 && 1 <= i126
by chaining
get_LE_609(i126, o67, i1, i104, env, static) -{0,0}> get_LE_611(i126, o67, i1, i104, env, static) :|: 0 < o67 && 1 <= i126
get_LE_611(i126, o67, i1, i104, env, static) -{1,1}> get_Load_614(i126, o67, i1, i104, env, static) :|: 0 < o67 && 0 < i126 && 1 <= i126
get_Load_614(i126, o67, i1, i104, env, static) -{1,1}> get_FieldAccess_622(o67, i126, i1, i104, env, static) :|: 0 < o67 && 1 <= i126
get_FieldAccess_622(o67, i126, i1, i104, env, static) -{1,1}> get_Store_630(o67, i126, i1, i104, env, static) :|: 0 < o67 && 1 <= i126
get_Store_630(o67, i126, i1, i104, env, static) -{1,1}> get_JMP_638(i126, o67, i1, i104, env, static) :|: 0 < o67 && 1 <= i126
get_JMP_638(i126, o67, i1, i104, env, static) -{1,1}> get_Inc_654(i126, o67, i1, i104, env, static) :|: 0 < o67 && 1 <= i126
get_Inc_654(i126, o67, i1, i104, env, static) -{0,0}> get_Inc_570(i126, o67, i1, i104, env, static) :|: 0 < o67 && 1 <= i126

(8) Obligation:

IntTrs with 16 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) -{32,32}> create_LE_84(i6', o4''', i1, i4, 0, env, static'1) :|: static'1 <= static''' + 1 && 0 < o4''' && 0 <= 2 && o4''' <= 1 + 0 && 0 <= static''' && 0 < 1 && static''' <= static + 2 && o4''' = 1 + 0 && 0 <= 1 && 0 <= static && 0 <= static'1 && 0 >= 0 && 0 < 2 && i1 + -1 = i6'
create_LE_84(i17, o4, i18, i4, 0, env, static) -{2,2}> create_Duplicate_690(1, i17, o4, o4, i18, i4, 0, env, static) :|: 0 < 1 && 2 <= i18 && 1 <= i17 && 0 < o4 && 0 < i17
create_Duplicate_690(o112, i145, o110, o111, i18, i4, 0, env, static) -{13,13}> create_LE_725(i151', o110, o112''', i18, i4, 0, o111, env, static) :|: o112''' = o112 + o111 && 2 <= i18 && 0 <= i151' && 0 < o111 && 0 < o112''' && i145 + -1 = i151' && 0 < o110 && 0 < o112 && o112''' <= o112 + o111 && 1 <= i145
create_LE_725(i158, o110, o112, i18, i4, 0, o111, env, static) -{2,2}> create_Duplicate_690(1, i158, o110, o112, i18, i4, 0, env, static) :|: 0 < i158 && 2 <= i18 && 0 < 1 && 0 < o111 && 0 < o112 && 1 <= i158 && 0 < o110 && 0 <= i158
create_LE_725(0, o110, o112, i18, i4, 0, o111, env, static) -{4,4}> create_FieldAccess_749(o112, o110, i18, i4, o111, 0, env, static) :|: 0 < o110 && 2 <= i18 && 0 <= 0 && 0 < o111 && 0 < o112
create_FieldAccess_749(o112, o163''', i18, i4, o111, 0, env, static) -{8,8}> get_Inc_957(i4, o112'1, i18, i4, env, static) :|: 0 < o111 && 0 < o163''' && 0 < o112 && 0 < o112'1 && 2 <= i18 && o163''' <= o163''' + o112 && o112'1 <= o112 + o112
get_Inc_957(i217, o276, i18, i218, env, static) -{2,2}> get_LE_964(i232, o276, i18, i218, env, static) :|: 2 <= i18 && 0 < o276 && i217 + -1 = i232
get_LE_964(i236, o276, i18, i218, env, static) -{0,0}> get_LE_968(i236, o276, i18, i218, env, static) :|: i236 <= 0 && 0 < o276 && 2 <= i18
get_LE_964(i237, o276, i18, i218, env, static) -{2,2}> get_FieldAccess_993(o276, i237, i18, i218, o302', env, static) :|: 0 < i237 && 2 <= i18 && 1 <= i237 && 0 < o302' && 0 < o276 && o302' <= o276
get_FieldAccess_993(o306, i237, i18, i218, o302, env, static) -{3,3}> get_Inc_957(i237, o306, i18, i218, env, static) :|: 0 < o306 && 2 <= i18 && 1 <= i237 && 0 < o302
get_FieldAccess_993(o301, i237, i18, i218, o302, env, static) -{3,3}> get_Inc_957(i237, o302, i18, i218, env, static) :|: 1 <= i237 && 2 <= i18 && 0 < o301 && 0 < o302
create_FieldAccess_749(o112, o110, i18, i4, o111, 0, env, static) -{8,8}> get_Inc_957(i4, o112, i18, i4, env, static) :|: 0 < o111 && 2 <= i18 && 0 < o110 && 0 < o112 && 0 < o111''' && o111''' <= o111 + o112
create_LE_84(i16, o4'1, i1, i4, 0, env, static) -{12,12}> get_Inc_570(i4, o4'1, i1, i4, env, static) :|: 0 < o4'1 && i16 <= 0 && o4'1 <= o4'1 + o4'1
get_Inc_570(i103, o67, i1, i104, env, static) -{2,2}> get_LE_609(i120, o67, i1, i104, env, static) :|: 0 < o67 && i103 + -1 = i120
get_LE_609(i125, o67, i1, i104, env, static) -{0,0}> get_LE_610(i125, o67, i1, i104, env, static) :|: 0 < o67 && i125 <= 0
get_LE_609(i126, o67, i1, i104, env, static) -{5,5}> get_Inc_570(i126, o67, i1, i104, env, static) :|: 0 < i126 && 0 < o67 && 1 <= i126

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

Moved arithmethic from lhss to constraints.

create_LE_725(0, o110, o112, i18, i4, 0, o111, env, static) -{4,4}> create_FieldAccess_749(o112, o110, i18, i4, o111, 0, env, static) :|: 0 < o110 && 2 <= i18 && 0 <= 0 && 0 < o111 && 0 < o112
was transformed to
create_LE_725(x, o110, o112, i18, i4, x', o111, env, static) -{4,4}> create_FieldAccess_749(o112, o110, i18, i4, o111, 0, env, static) :|: 0 < o110 && 2 <= i18 && 0 <= 0 && 0 < o111 && 0 < o112 && x = 0 && x' = 0

create_LE_725(i158, o110, o112, i18, i4, 0, o111, env, static) -{2,2}> create_Duplicate_690(1, i158, o110, o112, i18, i4, 0, env, static) :|: 0 < i158 && 2 <= i18 && 0 < 1 && 0 < o111 && 0 < o112 && 1 <= i158 && 0 < o110 && 0 <= i158
was transformed to
create_LE_725(i158, o110, o112, i18, i4, x, o111, env, static) -{2,2}> create_Duplicate_690(1, i158, o110, o112, i18, i4, 0, env, static) :|: 0 < i158 && 2 <= i18 && 0 < 1 && 0 < o111 && 0 < o112 && 1 <= i158 && 0 < o110 && 0 <= i158 && x = 0

create_FieldAccess_749(o112, o163''', i18, i4, o111, 0, env, static) -{8,8}> get_Inc_957(i4, o112'1, i18, i4, env, static) :|: 0 < o111 && 0 < o163''' && 0 < o112 && 0 < o112'1 && 2 <= i18 && o163''' <= o163''' + o112 && o112'1 <= o112 + o112
was transformed to
create_FieldAccess_749(o112, o163''', i18, i4, o111, x, env, static) -{8,8}> get_Inc_957(i4, o112'1, i18, i4, env, static) :|: 0 < o111 && 0 < o163''' && 0 < o112 && 0 < o112'1 && 2 <= i18 && o163''' <= o163''' + o112 && o112'1 <= o112 + o112 && x = 0

create_Duplicate_690(o112, i145, o110, o111, i18, i4, 0, env, static) -{13,13}> create_LE_725(i151', o110, o112''', i18, i4, 0, o111, env, static) :|: o112''' = o112 + o111 && 2 <= i18 && 0 <= i151' && 0 < o111 && 0 < o112''' && i145 + -1 = i151' && 0 < o110 && 0 < o112 && o112''' <= o112 + o111 && 1 <= i145
was transformed to
create_Duplicate_690(o112, i145, o110, o111, i18, i4, x, env, static) -{13,13}> create_LE_725(i151', o110, o112''', i18, i4, 0, o111, env, static) :|: o112''' = o112 + o111 && 2 <= i18 && 0 <= i151' && 0 < o111 && 0 < o112''' && i145 + -1 = i151' && 0 < o110 && 0 < o112 && o112''' <= o112 + o111 && 1 <= i145 && x = 0

create_FieldAccess_749(o112, o110, i18, i4, o111, 0, env, static) -{8,8}> get_Inc_957(i4, o112, i18, i4, env, static) :|: 0 < o111 && 2 <= i18 && 0 < o110 && 0 < o112 && 0 < o111''' && o111''' <= o111 + o112
was transformed to
create_FieldAccess_749(o112, o110, i18, i4, o111, x, env, static) -{8,8}> get_Inc_957(i4, o112, i18, i4, env, static) :|: 0 < o111 && 2 <= i18 && 0 < o110 && 0 < o112 && 0 < o111''' && o111''' <= o111 + o112 && x = 0

create_LE_84(i16, o4'1, i1, i4, 0, env, static) -{12,12}> get_Inc_570(i4, o4'1, i1, i4, env, static) :|: 0 < o4'1 && i16 <= 0 && o4'1 <= o4'1 + o4'1
was transformed to
create_LE_84(i16, o4'1, i1, i4, x, env, static) -{12,12}> get_Inc_570(i4, o4'1, i1, i4, env, static) :|: 0 < o4'1 && i16 <= 0 && o4'1 <= o4'1 + o4'1 && x = 0

create_LE_84(i17, o4, i18, i4, 0, env, static) -{2,2}> create_Duplicate_690(1, i17, o4, o4, i18, i4, 0, env, static) :|: 0 < 1 && 2 <= i18 && 1 <= i17 && 0 < o4 && 0 < i17
was transformed to
create_LE_84(i17, o4, i18, i4, x, env, static) -{2,2}> create_Duplicate_690(1, i17, o4, o4, i18, i4, 0, env, static) :|: 0 < 1 && 2 <= i18 && 1 <= i17 && 0 < o4 && 0 < i17 && x = 0

(10) Obligation:

IntTrs with 16 rules
Start term: main_Load_2(#0, #1, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
get_Inc_570(i103, o67, i1, i104, env, static) -{2,2}> get_LE_609(i120, o67, i1, i104, env, static) :|: 0 < o67 && i103 + -1 = i120
get_LE_609(i125, o67, i1, i104, env, static) -{0,0}> get_LE_610(i125, o67, i1, i104, env, static) :|: 0 < o67 && i125 <= 0
create_LE_725(x, o110, o112, i18, i4, x', o111, env, static) -{4,4}> create_FieldAccess_749(o112, o110, i18, i4, o111, 0, env, static) :|: 0 < o110 && 2 <= i18 && 0 <= 0 && 0 < o111 && 0 < o112 && x = 0 && x' = 0
create_LE_725(i158, o110, o112, i18, i4, x, o111, env, static) -{2,2}> create_Duplicate_690(1, i158, o110, o112, i18, i4, 0, env, static) :|: 0 < i158 && 2 <= i18 && 0 < 1 && 0 < o111 && 0 < o112 && 1 <= i158 && 0 < o110 && 0 <= i158 && x = 0
create_FieldAccess_749(o112, o163''', i18, i4, o111, x, env, static) -{8,8}> get_Inc_957(i4, o112'1, i18, i4, env, static) :|: 0 < o111 && 0 < o163''' && 0 < o112 && 0 < o112'1 && 2 <= i18 && o163''' <= o163''' + o112 && o112'1 <= o112 + o112 && x = 0
get_Inc_957(i217, o276, i18, i218, env, static) -{2,2}> get_LE_964(i232, o276, i18, i218, env, static) :|: 2 <= i18 && 0 < o276 && i217 + -1 = i232
get_FieldAccess_993(o301, i237, i18, i218, o302, env, static) -{3,3}> get_Inc_957(i237, o302, i18, i218, env, static) :|: 1 <= i237 && 2 <= i18 && 0 < o301 && 0 < o302
main_Load_2(i1, i4, env, static) -{32,32}> create_LE_84(i6', o4''', i1, i4, 0, env, static'1) :|: static'1 <= static''' + 1 && 0 < o4''' && 0 <= 2 && o4''' <= 1 + 0 && 0 <= static''' && 0 < 1 && static''' <= static + 2 && o4''' = 1 + 0 && 0 <= 1 && 0 <= static && 0 <= static'1 && 0 >= 0 && 0 < 2 && i1 + -1 = i6'
get_FieldAccess_993(o306, i237, i18, i218, o302, env, static) -{3,3}> get_Inc_957(i237, o306, i18, i218, env, static) :|: 0 < o306 && 2 <= i18 && 1 <= i237 && 0 < o302
get_LE_964(i237, o276, i18, i218, env, static) -{2,2}> get_FieldAccess_993(o276, i237, i18, i218, o302', env, static) :|: 0 < i237 && 2 <= i18 && 1 <= i237 && 0 < o302' && 0 < o276 && o302' <= o276
get_LE_609(i126, o67, i1, i104, env, static) -{5,5}> get_Inc_570(i126, o67, i1, i104, env, static) :|: 0 < i126 && 0 < o67 && 1 <= i126
create_Duplicate_690(o112, i145, o110, o111, i18, i4, x, env, static) -{13,13}> create_LE_725(i151', o110, o112''', i18, i4, 0, o111, env, static) :|: o112''' = o112 + o111 && 2 <= i18 && 0 <= i151' && 0 < o111 && 0 < o112''' && i145 + -1 = i151' && 0 < o110 && 0 < o112 && o112''' <= o112 + o111 && 1 <= i145 && x = 0
get_LE_964(i236, o276, i18, i218, env, static) -{0,0}> get_LE_968(i236, o276, i18, i218, env, static) :|: i236 <= 0 && 0 < o276 && 2 <= i18
create_FieldAccess_749(o112, o110, i18, i4, o111, x, env, static) -{8,8}> get_Inc_957(i4, o112, i18, i4, env, static) :|: 0 < o111 && 2 <= i18 && 0 < o110 && 0 < o112 && 0 < o111''' && o111''' <= o111 + o112 && x = 0
create_LE_84(i16, o4'1, i1, i4, x, env, static) -{12,12}> get_Inc_570(i4, o4'1, i1, i4, env, static) :|: 0 < o4'1 && i16 <= 0 && o4'1 <= o4'1 + o4'1 && x = 0
create_LE_84(i17, o4, i18, i4, x, env, static) -{2,2}> create_Duplicate_690(1, i17, o4, o4, i18, i4, 0, env, static) :|: 0 < 1 && 2 <= i18 && 1 <= i17 && 0 < o4 && 0 < i17 && x = 0

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

Moved arithmethic from constraints to rhss.

get_Inc_570(i103, o67, i1, i104, env, static) -{2,2}> get_LE_609(i120, o67, i1, i104, env, static) :|: 0 < o67 && i103 + -1 = i120
was transformed to
get_Inc_570(i103, o67, i1, i104, env, static) -{2,2}> get_LE_609(i103 + -1, o67, i1, i104, env, static) :|: 0 < o67 && i103 + -1 = i120

create_Duplicate_690(o112, i145, o110, o111, i18, i4, x, env, static) -{13,13}> create_LE_725(i151', o110, o112''', i18, i4, 0, o111, env, static) :|: o112''' = o112 + o111 && 2 <= i18 && 0 <= i151' && 0 < o111 && 0 < o112''' && i145 + -1 = i151' && 0 < o110 && 0 < o112 && o112''' <= o112 + o111 && 1 <= i145 && x = 0
was transformed to
create_Duplicate_690(o112, i145, o110, o111, i18, i4, x, env, static) -{13,13}> create_LE_725(i145 + -1, o110, o112 + o111, i18, i4, 0, o111, env, static) :|: o112''' = o112 + o111 && 2 <= i18 && 0 <= i151' && 0 < o111 && 0 < o112''' && i145 + -1 = i151' && 0 < o110 && 0 < o112 && o112''' <= o112 + o111 && 1 <= i145 && x = 0

get_Inc_957(i217, o276, i18, i218, env, static) -{2,2}> get_LE_964(i232, o276, i18, i218, env, static) :|: 2 <= i18 && 0 < o276 && i217 + -1 = i232
was transformed to
get_Inc_957(i217, o276, i18, i218, env, static) -{2,2}> get_LE_964(i217 + -1, o276, i18, i218, env, static) :|: 2 <= i18 && 0 < o276 && i217 + -1 = i232

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

(12) Obligation:

IntTrs with 16 rules
Start term: main_Load_2(#0, #1, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
create_LE_84(i16, o4'1, i1, i4, x, env, static) -{12,12}> get_Inc_570(i4, o4'1, i1, i4, env, static) :|: 0 < o4'1 && i16 <= 0 && o4'1 <= o4'1 + o4'1 && x = 0
create_FieldAccess_749(o112, o110, i18, i4, o111, x, env, static) -{8,8}> get_Inc_957(i4, o112, i18, i4, env, static) :|: 0 < o111 && 2 <= i18 && 0 < o110 && 0 < o112 && 0 < o111''' && o111''' <= o111 + o112 && x = 0
create_FieldAccess_749(o112, o163''', i18, i4, o111, x, env, static) -{8,8}> get_Inc_957(i4, o112'1, i18, i4, env, static) :|: 0 < o111 && 0 < o163''' && 0 < o112 && 0 < o112'1 && 2 <= i18 && o163''' <= o163''' + o112 && o112'1 <= o112 + o112 && x = 0
get_Inc_570(i103, o67, i1, i104, env, static) -{2,2}> get_LE_609(i103 + -1, o67, i1, i104, env, static) :|: 0 < o67 && i103 + -1 = i120
get_LE_609(i125, o67, i1, i104, env, static) -{0,0}> get_LE_610(i125, o67, i1, i104, env, static) :|: 0 < o67 && i125 <= 0
create_Duplicate_690(o112, i145, o110, o111, i18, i4, x, env, static) -{13,13}> create_LE_725(i145 + -1, o110, o112 + o111, i18, i4, 0, o111, env, static) :|: o112''' = o112 + o111 && 2 <= i18 && 0 <= i151' && 0 < o111 && 0 < o112''' && i145 + -1 = i151' && 0 < o110 && 0 < o112 && o112''' <= o112 + o111 && 1 <= i145 && x = 0
get_Inc_957(i217, o276, i18, i218, env, static) -{2,2}> get_LE_964(i217 + -1, o276, i18, i218, env, static) :|: 2 <= i18 && 0 < o276 && i217 + -1 = i232
main_Load_2(i1, i4, env, static) -{32,32}> create_LE_84(i1 + -1, 1 + 0, i1, i4, 0, env, static'1) :|: static'1 <= static''' + 1 && 0 < o4''' && 0 <= 2 && o4''' <= 1 + 0 && 0 <= static''' && 0 < 1 && static''' <= static + 2 && o4''' = 1 + 0 && 0 <= 1 && 0 <= static && 0 <= static'1 && 0 >= 0 && 0 < 2 && i1 + -1 = i6'
get_FieldAccess_993(o301, i237, i18, i218, o302, env, static) -{3,3}> get_Inc_957(i237, o302, i18, i218, env, static) :|: 1 <= i237 && 2 <= i18 && 0 < o301 && 0 < o302
create_LE_84(i17, o4, i18, i4, x, env, static) -{2,2}> create_Duplicate_690(1, i17, o4, o4, i18, i4, 0, env, static) :|: 0 < 1 && 2 <= i18 && 1 <= i17 && 0 < o4 && 0 < i17 && x = 0
get_FieldAccess_993(o306, i237, i18, i218, o302, env, static) -{3,3}> get_Inc_957(i237, o306, i18, i218, env, static) :|: 0 < o306 && 2 <= i18 && 1 <= i237 && 0 < o302
get_LE_964(i237, o276, i18, i218, env, static) -{2,2}> get_FieldAccess_993(o276, i237, i18, i218, o302', env, static) :|: 0 < i237 && 2 <= i18 && 1 <= i237 && 0 < o302' && 0 < o276 && o302' <= o276
get_LE_609(i126, o67, i1, i104, env, static) -{5,5}> get_Inc_570(i126, o67, i1, i104, env, static) :|: 0 < i126 && 0 < o67 && 1 <= i126
get_LE_964(i236, o276, i18, i218, env, static) -{0,0}> get_LE_968(i236, o276, i18, i218, env, static) :|: i236 <= 0 && 0 < o276 && 2 <= i18
create_LE_725(i158, o110, o112, i18, i4, x, o111, env, static) -{2,2}> create_Duplicate_690(1, i158, o110, o112, i18, i4, 0, env, static) :|: 0 < i158 && 2 <= i18 && 0 < 1 && 0 < o111 && 0 < o112 && 1 <= i158 && 0 < o110 && 0 <= i158 && x = 0
create_LE_725(x, o110, o112, i18, i4, x', o111, env, static) -{4,4}> create_FieldAccess_749(o112, o110, i18, i4, o111, 0, env, static) :|: 0 < o110 && 2 <= i18 && 0 <= 0 && 0 < o111 && 0 < o112 && x = 0 && x' = 0

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

Simplified expressions.

create_LE_84(i16, o4'1, i1, i4, x, env, static) -{12,12}> get_Inc_570(i4, o4'1, i1, i4, env, static) :|: 0 < o4'1 && i16 <= 0 && o4'1 <= o4'1 + o4'1 && x = 0
was transformed to
create_LE_84(i16, o4'1, i1, i4, x, env, static) -{12,12}> get_Inc_570(i4, o4'1, i1, i4, env, static) :|: 0 < o4'1 && i16 <= 0 && o4'1 <= 2 * o4'1 && x = 0

create_FieldAccess_749(o112, o163''', i18, i4, o111, x, env, static) -{8,8}> get_Inc_957(i4, o112'1, i18, i4, env, static) :|: 0 < o111 && 0 < o163''' && 0 < o112 && 0 < o112'1 && 2 <= i18 && o163''' <= o163''' + o112 && o112'1 <= o112 + o112 && x = 0
was transformed to
create_FieldAccess_749(o112, o163''', i18, i4, o111, x, env, static) -{8,8}> get_Inc_957(i4, o112'1, i18, i4, env, static) :|: 0 < o111 && 0 < o163''' && 0 < o112 && 0 < o112'1 && 2 <= i18 && o163''' <= o163''' + o112 && o112'1 <= 2 * o112 && x = 0

get_Inc_957(i217, o276, i18, i218, env, static) -{2,2}> get_LE_964(i217 + -1, o276, i18, i218, env, static) :|: 2 <= i18 && 0 < o276 && i217 + -1 = i232
was transformed to
get_Inc_957(i217, o276, i18, i218, env, static) -{2,2}> get_LE_964(i217 - 1, o276, i18, i218, env, static) :|: 2 <= i18 && 0 < o276 && i217 - 1 = i232

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

get_Inc_570(i103, o67, i1, i104, env, static) -{2,2}> get_LE_609(i103 + -1, o67, i1, i104, env, static) :|: 0 < o67 && i103 + -1 = i120
was transformed to
get_Inc_570(i103, o67, i1, i104, env, static) -{2,2}> get_LE_609(i103 - 1, o67, i1, i104, env, static) :|: 0 < o67 && i103 - 1 = i120

create_LE_84(i17, o4, i18, i4, x, env, static) -{2,2}> create_Duplicate_690(1, i17, o4, o4, i18, i4, 0, env, static) :|: 0 < 1 && 2 <= i18 && 1 <= i17 && 0 < o4 && 0 < i17 && x = 0
was transformed to
create_LE_84(i17, o4, i18, i4, x, env, static) -{2,2}> create_Duplicate_690(1, i17, o4, o4, i18, i4, 0, env, static) :|: 2 <= i18 && 1 <= i17 && 0 < o4 && 0 < i17 && x = 0

create_Duplicate_690(o112, i145, o110, o111, i18, i4, x, env, static) -{13,13}> create_LE_725(i145 + -1, o110, o112 + o111, i18, i4, 0, o111, env, static) :|: o112''' = o112 + o111 && 2 <= i18 && 0 <= i151' && 0 < o111 && 0 < o112''' && i145 + -1 = i151' && 0 < o110 && 0 < o112 && o112''' <= o112 + o111 && 1 <= i145 && x = 0
was transformed to
create_Duplicate_690(o112, i145, o110, o111, i18, i4, x, env, static) -{13,13}> create_LE_725(i145 - 1, o110, o112 + o111, i18, i4, 0, o111, env, static) :|: o112''' = o112 + o111 && 2 <= i18 && 0 <= i151' && 0 < o111 && 0 < o112''' && i145 - 1 = i151' && 0 < o110 && 0 < o112 && 1 <= i145 && x = 0

create_LE_725(i158, o110, o112, i18, i4, x, o111, env, static) -{2,2}> create_Duplicate_690(1, i158, o110, o112, i18, i4, 0, env, static) :|: 0 < i158 && 2 <= i18 && 0 < 1 && 0 < o111 && 0 < o112 && 1 <= i158 && 0 < o110 && 0 <= i158 && x = 0
was transformed to
create_LE_725(i158, o110, o112, i18, i4, x, o111, env, static) -{2,2}> create_Duplicate_690(1, i158, o110, o112, i18, i4, 0, env, static) :|: 0 < i158 && 2 <= i18 && 0 < o111 && 0 < o112 && 1 <= i158 && 0 < o110 && x = 0

create_LE_725(x, o110, o112, i18, i4, x', o111, env, static) -{4,4}> create_FieldAccess_749(o112, o110, i18, i4, o111, 0, env, static) :|: 0 < o110 && 2 <= i18 && 0 <= 0 && 0 < o111 && 0 < o112 && x = 0 && x' = 0
was transformed to
create_LE_725(x, o110, o112, i18, i4, x', o111, env, static) -{4,4}> create_FieldAccess_749(o112, o110, i18, i4, o111, 0, env, static) :|: 0 < o110 && 2 <= i18 && 0 < o111 && 0 < o112 && x = 0 && x' = 0

(14) Obligation:

IntTrs with 16 rules
Start term: main_Load_2(#0, #1, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
create_FieldAccess_749(o112, o110, i18, i4, o111, x, env, static) -{8,8}> get_Inc_957(i4, o112, i18, i4, env, static) :|: 0 < o111 && 2 <= i18 && 0 < o110 && 0 < o112 && 0 < o111''' && o111''' <= o111 + o112 && x = 0
create_LE_725(i158, o110, o112, i18, i4, x, o111, env, static) -{2,2}> create_Duplicate_690(1, i158, o110, o112, i18, i4, 0, env, static) :|: 0 < i158 && 2 <= i18 && 0 < o111 && 0 < o112 && 1 <= i158 && 0 < o110 && x = 0
get_LE_609(i125, o67, i1, i104, env, static) -{0,0}> get_LE_610(i125, o67, i1, i104, env, static) :|: 0 < o67 && i125 <= 0
create_Duplicate_690(o112, i145, o110, o111, i18, i4, x, env, static) -{13,13}> create_LE_725(i145 - 1, o110, o112 + o111, i18, i4, 0, o111, env, static) :|: o112''' = o112 + o111 && 2 <= i18 && 0 <= i151' && 0 < o111 && 0 < o112''' && i145 - 1 = i151' && 0 < o110 && 0 < o112 && 1 <= i145 && x = 0
main_Load_2(i1, i4, env, static) -{32,32}> create_LE_84(i1 - 1, 1, i1, i4, 0, env, static'1) :|: static'1 <= static''' + 1 && 0 < o4''' && 0 <= static''' && static''' <= static + 2 && o4''' = 1 && 0 <= static && 0 <= static'1 && i1 - 1 = i6'
get_Inc_570(i103, o67, i1, i104, env, static) -{2,2}> get_LE_609(i103 - 1, o67, i1, i104, env, static) :|: 0 < o67 && i103 - 1 = i120
get_FieldAccess_993(o301, i237, i18, i218, o302, env, static) -{3,3}> get_Inc_957(i237, o302, i18, i218, env, static) :|: 1 <= i237 && 2 <= i18 && 0 < o301 && 0 < o302
get_FieldAccess_993(o306, i237, i18, i218, o302, env, static) -{3,3}> get_Inc_957(i237, o306, i18, i218, env, static) :|: 0 < o306 && 2 <= i18 && 1 <= i237 && 0 < o302
create_LE_725(x, o110, o112, i18, i4, x', o111, env, static) -{4,4}> create_FieldAccess_749(o112, o110, i18, i4, o111, 0, env, static) :|: 0 < o110 && 2 <= i18 && 0 < o111 && 0 < o112 && x = 0 && x' = 0
get_LE_964(i237, o276, i18, i218, env, static) -{2,2}> get_FieldAccess_993(o276, i237, i18, i218, o302', env, static) :|: 0 < i237 && 2 <= i18 && 1 <= i237 && 0 < o302' && 0 < o276 && o302' <= o276
get_LE_609(i126, o67, i1, i104, env, static) -{5,5}> get_Inc_570(i126, o67, i1, i104, env, static) :|: 0 < i126 && 0 < o67 && 1 <= i126
create_LE_84(i17, o4, i18, i4, x, env, static) -{2,2}> create_Duplicate_690(1, i17, o4, o4, i18, i4, 0, env, static) :|: 2 <= i18 && 1 <= i17 && 0 < o4 && 0 < i17 && x = 0
get_LE_964(i236, o276, i18, i218, env, static) -{0,0}> get_LE_968(i236, o276, i18, i218, env, static) :|: i236 <= 0 && 0 < o276 && 2 <= i18
create_LE_84(i16, o4'1, i1, i4, x, env, static) -{12,12}> get_Inc_570(i4, o4'1, i1, i4, env, static) :|: 0 < o4'1 && i16 <= 0 && o4'1 <= 2 * o4'1 && x = 0
create_FieldAccess_749(o112, o163''', i18, i4, o111, x, env, static) -{8,8}> get_Inc_957(i4, o112'1, i18, i4, env, static) :|: 0 < o111 && 0 < o163''' && 0 < o112 && 0 < o112'1 && 2 <= i18 && o163''' <= o163''' + o112 && o112'1 <= 2 * o112 && x = 0
get_Inc_957(i217, o276, i18, i218, env, static) -{2,2}> get_LE_964(i217 - 1, o276, i18, i218, env, static) :|: 2 <= i18 && 0 < o276 && i217 - 1 = i232

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

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

(16) Obligation:

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

(18) Obligation:

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

Moved arithmethic from lhss to constraints.

(20) Obligation:

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

Moved arithmethic from constraints to rhss.

(22) Obligation:

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

Simplified expressions.

(24) Obligation:

(25) CESProof (EQUIVALENT transformation)

proved upper bound max(31 + 15 * #0, max(39 + 7 * #1, 46) + max(-15 + 15 * #0, 15), 61) using cofloco

(26) BOUNDS(CONSTANT, max(31 + 15 * #0, max(39 + 7 * #1, 46) + max(-15 + 15 * #0, 15), 61))

(27) TerminationGraphToComplexityProof (BOTH CONCRETE BOUNDS(ID, ADD(10)) transformation)

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

(28) Obligation:

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

Used field analysis yielded the following read fields:
- CyclicList: [next]

Considered paths: all paths from start

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

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

(30) Obligation:

IntTrs with 125 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_4(i1, i4, env, static) :|: 0 >= 0
main_Load_4(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_16(iconst_0, i1, i4, env, static) :|: iconst_0 = 0
langle_clinit_rangle_ArrayCreate_16(iconst_0, i1, i4, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_17(a2, i1, i4, iconst_0, env, static) :|: a2 = 2 && iconst_0 = 0 && 0 < a2
langle_clinit_rangle_FieldAccess_17(a2, i1, i4, iconst_0, env, static) -{1,1}> langle_clinit_rangle_New_18(i1, i4, env, static') :|: 0 <= a2 && iconst_0 = 0 && static' <= static + a2 && 0 <= static && 0 < a2
langle_clinit_rangle_New_18(i1, i4, env, static) -{0,0}> langle_clinit_rangle_New_20(i1, i4, env, static) :|: 0 >= 0
langle_clinit_rangle_New_20(i1, i4, env, static) -{0,0}> langle_clinit_rangle_New_22(i1, i4, env, static) :|: 0 <= static
langle_clinit_rangle_New_22(i1, i4, env, static) -{1,1}> langle_clinit_rangle_Duplicate_24(o2, i1, i4, env, static) :|: 0 < o2 && o2 = 1
langle_clinit_rangle_Duplicate_24(o2, i1, i4, env, static) -{1,1}> langle_clinit_rangle_ConstantStackPush_25(o2, i1, i4, env, static) :|: 0 < o2
langle_clinit_rangle_ConstantStackPush_25(o2, i1, i4, env, static) -{1,1}> langle_clinit_rangle_InvokeMethod_28(o2, NULL, i1, i4, env, static) :|: NULL = 0 && 0 < o2
langle_clinit_rangle_InvokeMethod_28(o2, NULL, i1, i4, env, static) -{1,1}> langle_init_rangle_Load_30(o2, i1, i4, env, static) :|: NULL = 0 && 0 < o2
langle_init_rangle_Load_30(o2, i1, i4, env, static) -{1,1}> langle_init_rangle_InvokeMethod_32(o2, i1, i4, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_32(o2, i1, i4, env, static) -{1,1}> langle_init_rangle_Load_34(o2, i1, i4, env, static) :|: 0 < o2
langle_init_rangle_Load_34(o2, i1, i4, env, static) -{1,1}> langle_init_rangle_InvokeMethod_36(o2, i1, i4, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_36(o2, i1, i4, env, static) -{1,1}> langle_init_rangle_Return_37(o2, i1, i4, env, static) :|: 0 < o2
langle_init_rangle_Return_37(o2, i1, i4, env, static) -{1,1}> langle_init_rangle_Return_40(o2, i1, i4, env, static) :|: 0 < o2
langle_init_rangle_Return_40(o2, i1, i4, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_41(o2, i1, i4, env, static) :|: 0 < o2
langle_clinit_rangle_FieldAccess_41(o2, i1, i4, env, static) -{1,1}> langle_clinit_rangle_Return_42(i1, i4, env, static') :|: 0 < o2 && 0 <= o2 && 0 <= static && static' <= static + o2
langle_clinit_rangle_Return_42(i1, i4, env, static) -{1,1}> main_Load_43(i1, i4, env, static) :|: 0 >= 0
main_Load_43(i1, i4, env, static) -{0,0}> main_Load_44(i1, i4, env, static) :|: 0 >= 0
main_Load_44(i1, i4, env, static) -{0,0}> main_Load_47(i1, i4, env, static) :|: 0 <= static
main_Load_47(i1, i4, env, static) -{0,0}> main_Load_48(i1, i4, env, static) :|: 0 >= 0
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) -{1,1}> main_InvokeMethod_51(i1, i4, env, static) :|: 0 >= 0
main_InvokeMethod_51(i1, i4, env, static) -{1,1}> create_New_52(i1, i4, env, static) :|: 0 >= 0
create_New_52(i1, i4, env, static) -{1,1}> create_Duplicate_54(o4, i1, i4, NULL, env, static) :|: NULL = 0 && o4 = 1 && 0 < o4
create_Duplicate_54(o4, i1, i4, NULL, env, static) -{1,1}> create_ConstantStackPush_56(o4, i1, i4, NULL, env, static) :|: NULL = 0 && 0 < o4
create_ConstantStackPush_56(o4, i1, i4, NULL, env, static) -{1,1}> create_InvokeMethod_59(o4, NULL, i1, i4, env, static) :|: NULL = 0 && 0 < o4
create_InvokeMethod_59(o4, NULL, i1, i4, env, static) -{1,1}> langle_init_rangle_Load_60(o4, NULL, i1, i4, env, static) :|: NULL = 0 && 0 < o4
langle_init_rangle_Load_60(o4, NULL, i1, i4, env, static) -{1,1}> langle_init_rangle_InvokeMethod_63(o4, NULL, i1, i4, env, static) :|: NULL = 0 && 0 < o4
langle_init_rangle_InvokeMethod_63(o4, NULL, i1, i4, env, static) -{1,1}> langle_init_rangle_Load_65(o4, NULL, i1, i4, env, static) :|: NULL = 0 && 0 < o4
langle_init_rangle_Load_65(o4, NULL, i1, i4, env, static) -{1,1}> langle_init_rangle_Load_67(o4, NULL, i1, i4, env, static) :|: NULL = 0 && 0 < o4
langle_init_rangle_Load_67(o4, NULL, i1, i4, env, static) -{1,1}> langle_init_rangle_FieldAccess_68(o4, NULL, i1, i4, env, static) :|: NULL = 0 && 0 < o4
langle_init_rangle_FieldAccess_68(o4, NULL, i1, i4, env, static) -{1,1}> langle_init_rangle_Return_70(o4', i1, i4, NULL, env, static) :|: NULL = 0 && o4' = o4 + NULL && 0 < o4 && o4' <= o4 + NULL && 0 < o4'
langle_init_rangle_Return_70(o4, i1, i4, NULL, env, static) -{1,1}> create_Duplicate_72(o4, i1, i4, NULL, env, static) :|: NULL = 0 && 0 < o4
create_Duplicate_72(o4, i1, i4, NULL, env, static) -{1,1}> create_Store_74(o4, i1, i4, NULL, env, static) :|: NULL = 0 && 0 < o4
create_Store_74(o4, i1, i4, NULL, env, static) -{1,1}> create_Store_77(o4, i1, i4, NULL, env, static) :|: NULL = 0 && 0 < o4
create_Store_77(o4, i1, i4, NULL, env, static) -{1,1}> create_Inc_78(i1, o4, i4, NULL, env, static) :|: NULL = 0 && 0 < o4
create_Inc_78(i1, o4, i4, NULL, env, static) -{1,1}> create_Load_79(i6, o4, i1, i4, NULL, env, static) :|: NULL = 0 && 0 < o4 && i1 + -1 = i6
create_Load_79(i6, o4, i1, i4, NULL, env, static) -{1,1}> create_LE_84(i6, o4, i1, i4, NULL, env, static) :|: NULL = 0 && 0 < o4
create_LE_84(i16, o4, i1, i4, NULL, env, static) -{0,0}> create_LE_86(i16, o4, i1, i4, NULL, env, static) :|: NULL = 0 && 0 < o4 && i16 <= 0
create_LE_84(i17, o4, i18, i4, NULL, env, static) -{0,0}> create_LE_87(i17, o4, i18, i4, NULL, env, static) :|: NULL = 0 && 0 < o4 && 1 <= i17 && 2 <= i18
create_LE_86(i16, o4, i1, i4, NULL, env, static) -{1,1}> create_Load_90(o4, i1, i4, NULL, env, static) :|: NULL = 0 && 0 < o4 && i16 <= 0
create_LE_87(i17, o4, i18, i4, NULL, env, static) -{1,1}> create_New_92(i17, o4, i18, i4, NULL, env, static) :|: NULL = 0 && 0 < o4 && 0 < i17 && 1 <= i17 && 2 <= i18
create_Load_90(o4, i1, i4, NULL, env, static) -{1,1}> create_Load_94(o4, i1, i4, NULL, env, static) :|: NULL = 0 && 0 < o4
create_New_92(i17, o4, i18, i4, NULL, env, static) -{1,1}> create_Duplicate_97(o6, i17, o4, i18, i4, NULL, env, static) :|: NULL = 0 && 0 < o6 && 0 < o4 && o6 = 1 && 1 <= i17 && 2 <= i18
create_Load_94(o4, i1, i4, NULL, env, static) -{1,1}> create_Duplicate_99(o4, i1, i4, NULL, env, static) :|: NULL = 0 && 0 < o4
create_Duplicate_97(o6, i17, o4, i18, i4, NULL, env, static) -{0,0}> create_Duplicate_690(o6, i17, o4, o4, i18, i4, NULL, env, static) :|: NULL = 0 && 0 < o6 && 0 < o4 && 1 <= i17 && 2 <= i18
create_Duplicate_99(o4, i1, i4, NULL, env, static) -{1,1}> create_FieldAccess_101(o4, i1, i4, NULL, env, static) :|: NULL = 0 && 0 < o4
create_FieldAccess_101(o4, i1, i4, NULL, env, static) -{1,1}> create_Return_104(o4', i1, i4, env, static) :|: NULL = 0 && 0 < o4 && o4' <= o4 + o4 && o4' = o4 && 0 < o4'
create_Return_104(o4, i1, i4, env, static) -{1,1}> main_Store_108(i1, i4, o4, env, static) :|: 0 < o4
main_Store_108(i1, i4, o4, env, static) -{1,1}> main_Load_110(i1, i4, o4, env, static) :|: 0 < o4
main_Load_110(i1, i4, o4, env, static) -{1,1}> main_Load_119(i1, i4, o4, env, static) :|: 0 < o4
main_Load_119(i1, i4, o4, env, static) -{1,1}> main_InvokeMethod_124(i1, i4, o4, env, static) :|: 0 < o4
main_InvokeMethod_124(i1, i4, o4, env, static) -{1,1}> get_Load_129(o4, i4, i1, env, static) :|: 0 < o4
get_Load_129(o4, i4, i1, env, static) -{1,1}> get_Store_139(o4, i4, i1, env, static) :|: 0 < o4
get_Store_139(o4, i4, i1, env, static) -{1,1}> get_Inc_143(i4, o4, i1, env, static) :|: 0 < o4
get_Inc_143(i4, o4, i1, env, static) -{0,0}> get_Inc_570(i4, o4, i1, i4, env, static) :|: 0 < o4
get_Inc_570(i103, o67, i1, i104, env, static) -{1,1}> get_Load_607(i120, o67, i1, i104, env, static) :|: 0 < o67 && i103 + -1 = i120
get_Load_607(i120, o67, i1, i104, env, static) -{1,1}> get_LE_609(i120, o67, i1, i104, env, static) :|: 0 < o67
get_LE_609(i126, o67, i1, i104, env, static) -{0,0}> get_LE_611(i126, o67, i1, i104, env, static) :|: 0 < o67 && 1 <= i126
get_LE_611(i126, o67, i1, i104, env, static) -{1,1}> get_Load_614(i126, o67, i1, i104, env, static) :|: 0 < o67 && 0 < i126 && 1 <= i126
get_Load_614(i126, o67, i1, i104, env, static) -{1,1}> get_FieldAccess_622(o67, i126, i1, i104, env, static) :|: 0 < o67 && 1 <= i126
get_FieldAccess_622(o67, i126, i1, i104, env, static) -{1,1}> get_Store_630(o67, i126, i1, i104, env, static) :|: 0 < o67 && 1 <= i126
get_Store_630(o67, i126, i1, i104, env, static) -{1,1}> get_JMP_638(i126, o67, i1, i104, env, static) :|: 0 < o67 && 1 <= i126
get_JMP_638(i126, o67, i1, i104, env, static) -{1,1}> get_Inc_654(i126, o67, i1, i104, env, static) :|: 0 < o67 && 1 <= i126
get_Inc_654(i126, o67, i1, i104, env, static) -{0,0}> get_Inc_570(i126, o67, i1, i104, env, static) :|: 0 < o67 && 1 <= i126
create_Duplicate_690(o112, i145, o110, o111, i18, i4, NULL, env, static) -{1,1}> create_Load_693(o112, i145, o110, o111, i18, i4, NULL, env, static) :|: NULL = 0 && 0 < o110 && 0 < o112 && 0 < o111 && 2 <= i18 && 1 <= i145
create_Load_693(o112, i145, o110, o111, i18, i4, NULL, env, static) -{1,1}> create_InvokeMethod_695(o112, o111, i145, o110, i18, i4, NULL, env, static) :|: NULL = 0 && 0 < o110 && 0 < o112 && 0 < o111 && 2 <= i18 && 1 <= i145
create_InvokeMethod_695(o112, o111, i145, o110, i18, i4, NULL, env, static) -{1,1}> langle_init_rangle_Load_697(o112, o111, i145, o110, i18, i4, NULL, env, static) :|: NULL = 0 && 0 < o110 && 0 < o112 && 0 < o111 && 2 <= i18 && 1 <= i145
langle_init_rangle_Load_697(o112, o111, i145, o110, i18, i4, NULL, env, static) -{1,1}> langle_init_rangle_InvokeMethod_698(o112, o111, i145, o110, i18, i4, NULL, env, static) :|: NULL = 0 && 0 < o110 && 0 < o112 && 0 < o111 && 2 <= i18 && 1 <= i145
langle_init_rangle_InvokeMethod_698(o112, o111, i145, o110, i18, i4, NULL, env, static) -{1,1}> langle_init_rangle_Load_699(o112, o111, i145, o110, i18, i4, NULL, env, static) :|: NULL = 0 && 0 < o110 && 0 < o112 && 0 < o111 && 2 <= i18 && 1 <= i145
langle_init_rangle_Load_699(o112, o111, i145, o110, i18, i4, NULL, env, static) -{1,1}> langle_init_rangle_Load_701(o112, o111, i145, o110, i18, i4, NULL, env, static) :|: NULL = 0 && 0 < o110 && 0 < o112 && 0 < o111 && 2 <= i18 && 1 <= i145
langle_init_rangle_Load_701(o112, o111, i145, o110, i18, i4, NULL, env, static) -{1,1}> langle_init_rangle_FieldAccess_703(o112, o111, i145, o110, i18, i4, NULL, env, static) :|: NULL = 0 && 0 < o110 && 0 < o112 && 0 < o111 && 2 <= i18 && 1 <= i145
langle_init_rangle_FieldAccess_703(o112, o111, i145, o110, i18, i4, NULL, env, static) -{1,1}> langle_init_rangle_Return_708(o112', i145, o110, i18, i4, o111, NULL, env, static) :|: NULL = 0 && 0 < o112' && 0 < o110 && o112' = o112 + o111 && 0 < o112 && 0 < o111 && 2 <= i18 && o112' <= o112 + o111 && 1 <= i145
langle_init_rangle_Return_708(o112, i145, o110, i18, i4, o111, NULL, env, static) -{1,1}> create_Store_710(o112, i145, o110, i18, i4, o111, NULL, env, static) :|: NULL = 0 && 0 < o110 && 0 < o112 && 0 < o111 && 2 <= i18 && 1 <= i145
create_Store_710(o112, i145, o110, i18, i4, o111, NULL, env, static) -{1,1}> create_JMP_712(i145, o110, o112, i18, i4, NULL, o111, env, static) :|: NULL = 0 && 0 < o110 && 0 < o112 && 0 < o111 && 2 <= i18 && 1 <= i145
create_JMP_712(i145, o110, o112, i18, i4, NULL, o111, env, static) -{1,1}> create_Inc_715(i145, o110, o112, i18, i4, NULL, o111, env, static) :|: NULL = 0 && 0 < o110 && 0 < o112 && 0 < o111 && 2 <= i18 && 1 <= i145
create_Inc_715(i145, o110, o112, i18, i4, NULL, o111, env, static) -{1,1}> create_Load_718(i151, o110, o112, i18, i4, NULL, o111, env, static) :|: NULL = 0 && 0 < o110 && 0 <= i151 && 0 < o112 && i145 + -1 = i151 && 0 < o111 && 2 <= i18 && 1 <= i145
create_Load_718(i151, o110, o112, i18, i4, NULL, o111, env, static) -{1,1}> create_LE_725(i151, o110, o112, i18, i4, NULL, o111, env, static) :|: NULL = 0 && 0 < o110 && 0 <= i151 && 0 < o112 && 0 < o111 && 2 <= i18
create_LE_725(iconst_0, o110, o112, i18, i4, NULL, o111, env, static) -{0,0}> create_LE_727(iconst_0, o110, o112, i18, i4, NULL, o111, env, static) :|: NULL = 0 && 0 < o110 && 0 <= iconst_0 && iconst_0 = 0 && 0 < o112 && 0 < o111 && 2 <= i18
create_LE_725(i158, o110, o112, i18, i4, NULL, o111, env, static) -{0,0}> create_LE_729(i158, o110, o112, i18, i4, NULL, o111, env, static) :|: NULL = 0 && 0 < o110 && 0 <= i158 && 1 <= i158 && 0 < o112 && 0 < o111 && 2 <= i18
create_LE_727(iconst_0, o110, o112, i18, i4, NULL, o111, env, static) -{1,1}> create_Load_732(o110, o112, i18, i4, NULL, o111, env, static) :|: NULL = 0 && 0 < o110 && iconst_0 <= 0 && iconst_0 = 0 && 0 < o112 && 0 < o111 && 2 <= i18
create_LE_729(i158, o110, o112, i18, i4, NULL, o111, env, static) -{1,1}> create_New_737(i158, o110, o112, i18, i4, NULL, o111, env, static) :|: NULL = 0 && 0 < o110 && 1 <= i158 && 0 < o112 && 0 < o111 && 2 <= i18 && 0 < i158
create_Load_732(o110, o112, i18, i4, NULL, o111, env, static) -{1,1}> create_Load_740(o110, o112, i18, i4, NULL, o111, env, static) :|: NULL = 0 && 0 < o110 && 0 < o112 && 0 < o111 && 2 <= i18
create_New_737(i158, o110, o112, i18, i4, NULL, o111, env, static) -{1,1}> create_Duplicate_743(o150, i158, o110, o112, i18, i4, NULL, o111, env, static) :|: NULL = 0 && 0 < o110 && 1 <= i158 && 0 < o112 && 0 < o150 && 0 < o111 && 2 <= i18 && o150 = 1
create_Load_740(o110, o112, i18, i4, NULL, o111, env, static) -{1,1}> create_Duplicate_746(o110, o112, i18, i4, NULL, o111, env, static) :|: NULL = 0 && 0 < o110 && 0 < o112 && 0 < o111 && 2 <= i18
create_Duplicate_743(o150, i158, o110, o112, i18, i4, NULL, o111, env, static) -{0,0}> create_Duplicate_690(o150, i158, o110, o112, i18, i4, NULL, env, static) :|: NULL = 0 && 0 < o110 && 1 <= i158 && 0 < o150 && 0 < o112 && 0 < o111 && 2 <= i18
create_Duplicate_746(o110, o112, i18, i4, NULL, o111, env, static) -{1,1}> create_FieldAccess_749(o112, o110, i18, i4, o111, NULL, env, static) :|: NULL = 0 && 0 < o110 && 0 < o112 && 0 < o111 && 2 <= i18
create_FieldAccess_749(o112, o110, i18, i4, o111, NULL, env, static) -{0,0}> create_FieldAccess_779(o112, o110, i18, i4, o111, NULL, env, static) :|: NULL = 0 && 0 < o110 && 0 < o112 && 0 < o111 && 2 <= i18
create_FieldAccess_749(o112, o163, i18, i4, o111, NULL, env, static) -{0,0}> create_FieldAccess_780(o112, o163, i18, i4, NULL, env, static) :|: NULL = 0 && 0 < o112 && 0 < o111 && 0 < o163 && 2 <= i18
create_FieldAccess_779(o112, o110, i18, i4, o111, NULL, env, static) -{1,1}> create_Return_797(o112, i18, i4, o111', env, static) :|: NULL = 0 && 0 < o110 && o111' <= o111 + o112 && 0 < o111' && 0 < o112 && 0 < o111 && 2 <= i18
create_FieldAccess_780(o112, o163, i18, i4, NULL, env, static) -{1,1}> create_Return_805(o112', i18, i4, o163', env, static) :|: NULL = 0 && 0 < o112' && o112' <= o112 + o112 && o163' <= o163 + o112 && 0 < o112 && 0 < o163 && 2 <= i18 && 0 < o163' && o163' = o163
create_Return_797(o112, i18, i4, o111, env, static) -{1,1}> main_Store_839(i18, i4, o112, o111, env, static) :|: 0 < o112 && 0 < o111 && 2 <= i18
create_Return_805(o112, i18, i4, o163, env, static) -{1,1}> main_Store_845(i18, i4, o112, o163, env, static) :|: 0 < o112 && 2 <= i18 && 0 < o163
main_Store_839(i18, i4, o112, o111, env, static) -{1,1}> main_Load_848(i18, i4, o112, o111, env, static) :|: 0 < o112 && 0 < o111 && 2 <= i18
main_Store_845(i18, i4, o112, o163, env, static) -{1,1}> main_Load_852(i18, i4, o112, o163, env, static) :|: 0 < o112 && 2 <= i18 && 0 < o163
main_Load_848(i18, i4, o112, o111, env, static) -{1,1}> main_Load_855(i18, i4, o112, o111, env, static) :|: 0 < o112 && 0 < o111 && 2 <= i18
main_Load_852(i18, i4, o112, o163, env, static) -{1,1}> main_Load_860(i18, i4, o112, o163, env, static) :|: 0 < o112 && 2 <= i18 && 0 < o163
main_Load_855(i18, i4, o112, o111, env, static) -{1,1}> main_InvokeMethod_862(i18, i4, o112, o111, env, static) :|: 0 < o112 && 0 < o111 && 2 <= i18
main_Load_860(i18, i4, o112, o163, env, static) -{1,1}> main_InvokeMethod_867(i18, i4, o112, o163, env, static) :|: 0 < o112 && 2 <= i18 && 0 < o163
main_InvokeMethod_862(i18, i4, o112, o111, env, static) -{1,1}> get_Load_869(o112, i4, i18, o111, env, static) :|: 0 < o112 && 0 < o111 && 2 <= i18
main_InvokeMethod_867(i18, i4, o112, o163, env, static) -{1,1}> get_Load_871(o112, i4, i18, o163, env, static) :|: 0 < o112 && 2 <= i18 && 0 < o163
get_Load_869(o112, i4, i18, o111, env, static) -{1,1}> get_Store_874(o112, i4, i18, o111, env, static) :|: 0 < o112 && 0 < o111 && 2 <= i18
get_Load_871(o112, i4, i18, o163, env, static) -{1,1}> get_Store_879(o112, i4, i18, o163, env, static) :|: 0 < o112 && 2 <= i18 && 0 < o163
get_Store_874(o112, i4, i18, o111, env, static) -{1,1}> get_Inc_880(i4, o112, i18, o111, env, static) :|: 0 < o112 && 0 < o111 && 2 <= i18
get_Store_879(o112, i4, i18, o163, env, static) -{1,1}> get_Inc_881(i4, o112, i18, o163, env, static) :|: 0 < o112 && 2 <= i18 && 0 < o163
get_Inc_880(i4, o112, i18, o111, env, static) -{0,0}> get_Inc_957(i4, o112, i18, i4, env, static) :|: 0 < o112 && 0 < o111 && 2 <= i18
get_Inc_881(i4, o112, i18, o163, env, static) -{0,0}> get_Inc_957(i4, o112, i18, i4, env, static) :|: 0 < o112 && 2 <= i18 && 0 < o163
get_Inc_957(i217, o276, i18, i218, env, static) -{1,1}> get_Load_962(i232, o276, i18, i218, env, static) :|: 0 < o276 && i217 + -1 = i232 && 2 <= i18
get_Load_962(i232, o276, i18, i218, env, static) -{1,1}> get_LE_964(i232, o276, i18, i218, env, static) :|: 0 < o276 && 2 <= i18
get_LE_964(i237, o276, i18, i218, env, static) -{0,0}> get_LE_969(i237, o276, i18, i218, env, static) :|: 1 <= i237 && 0 < o276 && 2 <= i18
get_LE_969(i237, o276, i18, i218, env, static) -{1,1}> get_Load_976(i237, o276, i18, i218, env, static) :|: 1 <= i237 && 0 < o276 && 2 <= i18 && 0 < i237
get_Load_976(i237, o276, i18, i218, env, static) -{1,1}> get_FieldAccess_982(o276, i237, i18, i218, env, static) :|: 1 <= i237 && 0 < o276 && 2 <= i18
get_FieldAccess_982(o301, i237, i18, i218, env, static) -{0,0}> get_FieldAccess_993(o301, i237, i18, i218, o302, env, static) :|: 0 < o301 && 1 <= i237 && o302 <= o301 && 0 < o302 && 2 <= i18
get_FieldAccess_993(o301, i237, i18, i218, o302, env, static) -{0,0}> get_FieldAccess_1005(o301, i237, i18, i218, o302, env, static) :|: 0 < o301 && 1 <= i237 && 0 < o302 && 2 <= i18
get_FieldAccess_993(o306, i237, i18, i218, o302, env, static) -{0,0}> get_FieldAccess_1006(o306, i237, i18, i218, env, static) :|: 1 <= i237 && 0 < o306 && 0 < o302 && 2 <= i18
get_FieldAccess_1005(o301, i237, i18, i218, o302, env, static) -{1,1}> get_Store_1011(o302, i237, i18, i218, env, static) :|: 0 < o301 && 1 <= i237 && 0 < o302 && 2 <= i18
get_FieldAccess_1006(o306, i237, i18, i218, env, static) -{1,1}> get_Store_1016(o306, i237, i18, i218, env, static) :|: 1 <= i237 && 0 < o306 && 2 <= i18
get_Store_1011(o302, i237, i18, i218, env, static) -{1,1}> get_JMP_1019(i237, o302, i18, i218, env, static) :|: 1 <= i237 && 0 < o302 && 2 <= i18
get_Store_1016(o306, i237, i18, i218, env, static) -{1,1}> get_JMP_1023(i237, o306, i18, i218, env, static) :|: 1 <= i237 && 0 < o306 && 2 <= i18
get_JMP_1019(i237, o302, i18, i218, env, static) -{1,1}> get_Inc_1030(i237, o302, i18, i218, env, static) :|: 1 <= i237 && 0 < o302 && 2 <= i18
get_JMP_1023(i237, o306, i18, i218, env, static) -{1,1}> get_Inc_1040(i237, o306, i18, i218, env, static) :|: 1 <= i237 && 0 < o306 && 2 <= i18
get_Inc_1030(i237, o302, i18, i218, env, static) -{0,0}> get_Inc_957(i237, o302, i18, i218, env, static) :|: 1 <= i237 && 0 < o302 && 2 <= i18
get_Inc_1040(i237, o306, i18, i218, env, static) -{0,0}> get_Inc_957(i237, o306, i18, i218, env, static) :|: 1 <= i237 && 0 < o306 && 2 <= i18

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

obtained
get_Inc_957(i217, o276, i18, i218, env, static) -{4,4}> get_FieldAccess_993(o276, i232, i18, i218, o302', env, static) :|: 0 < i232 && 2 <= i18 && 0 < o276 && 0 < o302' && 1 <= i232 && o302' <= o276 && i217 + -1 = i232
by chaining
get_Inc_957(i217, o276, i18, i218, env, static) -{1,1}> get_Load_962(i232, o276, i18, i218, env, static) :|: 0 < o276 && i217 + -1 = i232 && 2 <= i18
get_Load_962(i232, o276, i18, i218, env, static) -{1,1}> get_LE_964(i232, o276, i18, i218, env, static) :|: 0 < o276 && 2 <= i18
get_LE_964(i237, o276, i18, i218, env, static) -{0,0}> get_LE_969(i237, o276, i18, i218, env, static) :|: 1 <= i237 && 0 < o276 && 2 <= i18
get_LE_969(i237, o276, i18, i218, env, static) -{1,1}> get_Load_976(i237, o276, i18, i218, env, static) :|: 1 <= i237 && 0 < o276 && 2 <= i18 && 0 < i237
get_Load_976(i237, o276, i18, i218, env, static) -{1,1}> get_FieldAccess_982(o276, i237, i18, i218, env, static) :|: 1 <= i237 && 0 < o276 && 2 <= i18
get_FieldAccess_982(o301, i237, i18, i218, env, static) -{0,0}> get_FieldAccess_993(o301, i237, i18, i218, o302, env, static) :|: 0 < o301 && 1 <= i237 && o302 <= o301 && 0 < o302 && 2 <= i18

obtained
get_Inc_570(i103, o67, i1, i104, env, static) -{7,7}> get_Inc_570(i120, o67, i1, i104, env, static) :|: 0 < i120 && 0 < o67 && 1 <= i120 && i103 + -1 = i120
by chaining
get_Inc_570(i103, o67, i1, i104, env, static) -{1,1}> get_Load_607(i120, o67, i1, i104, env, static) :|: 0 < o67 && i103 + -1 = i120
get_Load_607(i120, o67, i1, i104, env, static) -{1,1}> get_LE_609(i120, o67, i1, i104, env, static) :|: 0 < o67
get_LE_609(i126, o67, i1, i104, env, static) -{0,0}> get_LE_611(i126, o67, i1, i104, env, static) :|: 0 < o67 && 1 <= i126
get_LE_611(i126, o67, i1, i104, env, static) -{1,1}> get_Load_614(i126, o67, i1, i104, env, static) :|: 0 < o67 && 0 < i126 && 1 <= i126
get_Load_614(i126, o67, i1, i104, env, static) -{1,1}> get_FieldAccess_622(o67, i126, i1, i104, env, static) :|: 0 < o67 && 1 <= i126
get_FieldAccess_622(o67, i126, i1, i104, env, static) -{1,1}> get_Store_630(o67, i126, i1, i104, env, static) :|: 0 < o67 && 1 <= i126
get_Store_630(o67, i126, i1, i104, env, static) -{1,1}> get_JMP_638(i126, o67, i1, i104, env, static) :|: 0 < o67 && 1 <= i126
get_JMP_638(i126, o67, i1, i104, env, static) -{1,1}> get_Inc_654(i126, o67, i1, i104, env, static) :|: 0 < o67 && 1 <= i126
get_Inc_654(i126, o67, i1, i104, env, static) -{0,0}> get_Inc_570(i126, o67, i1, i104, env, static) :|: 0 < o67 && 1 <= i126

(32) Obligation:

IntTrs with 12 rules
Start term: main_Load_2(#0, #1, env, static)
Considered paths: all paths from start
Rules:
main_Load_2(i1, i4, env, static) -{32,32}> create_LE_84(i6', o4''', i1, i4, 0, env, static'1) :|: static'1 <= static''' + 1 && 0 < o4''' && 0 <= 2 && o4''' <= 1 + 0 && 0 <= static''' && 0 < 1 && static''' <= static + 2 && o4''' = 1 + 0 && 0 <= 1 && 0 <= static && 0 <= static'1 && 0 >= 0 && 0 < 2 && i1 + -1 = i6'
create_LE_84(i17, o4, i18, i4, 0, env, static) -{2,2}> create_Duplicate_690(1, i17, o4, o4, i18, i4, 0, env, static) :|: 0 < 1 && 2 <= i18 && 1 <= i17 && 0 < o4 && 0 < i17
create_Duplicate_690(o112, i145, o110, o111, i18, i4, 0, env, static) -{13,13}> create_LE_725(i151', o110, o112''', i18, i4, 0, o111, env, static) :|: o112''' = o112 + o111 && 2 <= i18 && 0 <= i151' && 0 < o111 && 0 < o112''' && i145 + -1 = i151' && 0 < o110 && 0 < o112 && o112''' <= o112 + o111 && 1 <= i145
create_LE_725(i158, o110, o112, i18, i4, 0, o111, env, static) -{2,2}> create_Duplicate_690(1, i158, o110, o112, i18, i4, 0, env, static) :|: 0 < i158 && 2 <= i18 && 0 < 1 && 0 < o111 && 0 < o112 && 1 <= i158 && 0 < o110 && 0 <= i158
create_LE_725(0, o110, o112, i18, i4, 0, o111, env, static) -{4,4}> create_FieldAccess_749(o112, o110, i18, i4, o111, 0, env, static) :|: 0 < o110 && 2 <= i18 && 0 <= 0 && 0 < o111 && 0 < o112
create_FieldAccess_749(o112, o163''', i18, i4, o111, 0, env, static) -{8,8}> get_Inc_957(i4, o112'1, i18, i4, env, static) :|: 0 < o111 && 0 < o163''' && 0 < o112 && 0 < o112'1 && 2 <= i18 && o163''' <= o163''' + o112 && o112'1 <= o112 + o112
get_Inc_957(i217, o276, i18, i218, env, static) -{4,4}> get_FieldAccess_993(o276, i232, i18, i218, o302', env, static) :|: 0 < i232 && 2 <= i18 && 0 < o276 && 0 < o302' && 1 <= i232 && o302' <= o276 && i217 + -1 = i232
get_FieldAccess_993(o306, i237, i18, i218, o302, env, static) -{3,3}> get_Inc_957(i237, o306, i18, i218, env, static) :|: 0 < o306 && 2 <= i18 && 1 <= i237 && 0 < o302
get_FieldAccess_993(o301, i237, i18, i218, o302, env, static) -{3,3}> get_Inc_957(i237, o302, i18, i218, env, static) :|: 1 <= i237 && 2 <= i18 && 0 < o301 && 0 < o302
create_FieldAccess_749(o112, o110, i18, i4, o111, 0, env, static) -{8,8}> get_Inc_957(i4, o112, i18, i4, env, static) :|: 0 < o111 && 2 <= i18 && 0 < o110 && 0 < o112 && 0 < o111''' && o111''' <= o111 + o112
create_LE_84(i16, o4'1, i1, i4, 0, env, static) -{12,12}> get_Inc_570(i4, o4'1, i1, i4, env, static) :|: 0 < o4'1 && i16 <= 0 && o4'1 <= o4'1 + o4'1
get_Inc_570(i103, o67, i1, i104, env, static) -{7,7}> get_Inc_570(i120, o67, i1, i104, env, static) :|: 0 < i120 && 0 < o67 && 1 <= i120 && i103 + -1 = i120

(33) 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)
create_LE_84(x1, x2, x3, x4, x5, x6, x7) → create_LE_84(x1, x2, x3, x4)
create_Duplicate_690(x1, x2, x3, x4, x5, x6, x7, x8, x9) → create_Duplicate_690(x1, x2, x3, x4, x5, x6)
create_LE_725(x1, x2, x3, x4, x5, x6, x7, x8, x9) → create_LE_725(x1, x2, x3, x4, x5, x7)
create_FieldAccess_749(x1, x2, x3, x4, x5, x6, x7, x8) → create_FieldAccess_749(x1, x2, x3, x4, x5)
get_Inc_957(x1, x2, x3, x4, x5, x6) → get_Inc_957(x1, x2, x3)
get_FieldAccess_993(x1, x2, x3, x4, x5, x6, x7) → get_FieldAccess_993(x1, x2, x3, x5)
get_Inc_570(x1, x2, x3, x4, x5, x6) → get_Inc_570(x1, x2)

(34) Obligation:

IntTrs with 12 rules
Start term: main_Load_2(#0, #1, static)
Considered paths: all paths from start
Rules:
main_Load_2(i1, i4, static) -{32,32}> create_LE_84(i6', o4''', i1, i4) :|: static'1 <= static''' + 1 && 0 < o4''' && 0 <= 2 && o4''' <= 1 + 0 && 0 <= static''' && 0 < 1 && static''' <= static + 2 && o4''' = 1 + 0 && 0 <= 1 && 0 <= static && 0 <= static'1 && 0 >= 0 && 0 < 2 && i1 + -1 = i6'
create_LE_84(i17, o4, i18, i4) -{2,2}> create_Duplicate_690(1, i17, o4, o4, i18, i4) :|: 0 < 1 && 2 <= i18 && 1 <= i17 && 0 < o4 && 0 < i17
create_Duplicate_690(o112, i145, o110, o111, i18, i4) -{13,13}> create_LE_725(i151', o110, o112''', i18, i4, o111) :|: o112''' = o112 + o111 && 2 <= i18 && 0 <= i151' && 0 < o111 && 0 < o112''' && i145 + -1 = i151' && 0 < o110 && 0 < o112 && o112''' <= o112 + o111 && 1 <= i145
create_LE_725(i158, o110, o112, i18, i4, o111) -{2,2}> create_Duplicate_690(1, i158, o110, o112, i18, i4) :|: 0 < i158 && 2 <= i18 && 0 < 1 && 0 < o111 && 0 < o112 && 1 <= i158 && 0 < o110 && 0 <= i158
create_LE_725(0, o110, o112, i18, i4, o111) -{4,4}> create_FieldAccess_749(o112, o110, i18, i4, o111) :|: 0 < o110 && 2 <= i18 && 0 <= 0 && 0 < o111 && 0 < o112
create_FieldAccess_749(o112, o163''', i18, i4, o111) -{8,8}> get_Inc_957(i4, o112'1, i18) :|: 0 < o111 && 0 < o163''' && 0 < o112 && 0 < o112'1 && 2 <= i18 && o163''' <= o163''' + o112 && o112'1 <= o112 + o112
get_Inc_957(i217, o276, i18) -{4,4}> get_FieldAccess_993(o276, i232, i18, o302') :|: 0 < i232 && 2 <= i18 && 0 < o276 && 0 < o302' && 1 <= i232 && o302' <= o276 && i217 + -1 = i232
get_FieldAccess_993(o306, i237, i18, o302) -{3,3}> get_Inc_957(i237, o306, i18) :|: 0 < o306 && 2 <= i18 && 1 <= i237 && 0 < o302
get_FieldAccess_993(o301, i237, i18, o302) -{3,3}> get_Inc_957(i237, o302, i18) :|: 1 <= i237 && 2 <= i18 && 0 < o301 && 0 < o302
create_FieldAccess_749(o112, o110, i18, i4, o111) -{8,8}> get_Inc_957(i4, o112, i18) :|: 0 < o111 && 2 <= i18 && 0 < o110 && 0 < o112 && 0 < o111''' && o111''' <= o111 + o112
create_LE_84(i16, o4'1, i1, i4) -{12,12}> get_Inc_570(i4, o4'1) :|: 0 < o4'1 && i16 <= 0 && o4'1 <= o4'1 + o4'1
get_Inc_570(i103, o67) -{7,7}> get_Inc_570(i120, o67) :|: 0 < i120 && 0 < o67 && 1 <= i120 && i103 + -1 = i120

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

Moved arithmethic from lhss to constraints.

create_LE_725(0, o110, o112, i18, i4, o111) -{4,4}> create_FieldAccess_749(o112, o110, i18, i4, o111) :|: 0 < o110 && 2 <= i18 && 0 <= 0 && 0 < o111 && 0 < o112
was transformed to
create_LE_725(x, o110, o112, i18, i4, o111) -{4,4}> create_FieldAccess_749(o112, o110, i18, i4, o111) :|: 0 < o110 && 2 <= i18 && 0 <= 0 && 0 < o111 && 0 < o112 && x = 0

(36) Obligation:

IntTrs with 12 rules
Start term: main_Load_2(#0, #1, static)
Considered paths: all paths from start
Rules:
create_LE_725(i158, o110, o112, i18, i4, o111) -{2,2}> create_Duplicate_690(1, i158, o110, o112, i18, i4) :|: 0 < i158 && 2 <= i18 && 0 < 1 && 0 < o111 && 0 < o112 && 1 <= i158 && 0 < o110 && 0 <= i158
create_LE_84(i17, o4, i18, i4) -{2,2}> create_Duplicate_690(1, i17, o4, o4, i18, i4) :|: 0 < 1 && 2 <= i18 && 1 <= i17 && 0 < o4 && 0 < i17
get_Inc_570(i103, o67) -{7,7}> get_Inc_570(i120, o67) :|: 0 < i120 && 0 < o67 && 1 <= i120 && i103 + -1 = i120
create_Duplicate_690(o112, i145, o110, o111, i18, i4) -{13,13}> create_LE_725(i151', o110, o112''', i18, i4, o111) :|: o112''' = o112 + o111 && 2 <= i18 && 0 <= i151' && 0 < o111 && 0 < o112''' && i145 + -1 = i151' && 0 < o110 && 0 < o112 && o112''' <= o112 + o111 && 1 <= i145
create_LE_84(i16, o4'1, i1, i4) -{12,12}> get_Inc_570(i4, o4'1) :|: 0 < o4'1 && i16 <= 0 && o4'1 <= o4'1 + o4'1
create_FieldAccess_749(o112, o163''', i18, i4, o111) -{8,8}> get_Inc_957(i4, o112'1, i18) :|: 0 < o111 && 0 < o163''' && 0 < o112 && 0 < o112'1 && 2 <= i18 && o163''' <= o163''' + o112 && o112'1 <= o112 + o112
create_LE_725(x, o110, o112, i18, i4, o111) -{4,4}> create_FieldAccess_749(o112, o110, i18, i4, o111) :|: 0 < o110 && 2 <= i18 && 0 <= 0 && 0 < o111 && 0 < o112 && x = 0
main_Load_2(i1, i4, static) -{32,32}> create_LE_84(i6', o4''', i1, i4) :|: static'1 <= static''' + 1 && 0 < o4''' && 0 <= 2 && o4''' <= 1 + 0 && 0 <= static''' && 0 < 1 && static''' <= static + 2 && o4''' = 1 + 0 && 0 <= 1 && 0 <= static && 0 <= static'1 && 0 >= 0 && 0 < 2 && i1 + -1 = i6'
get_Inc_957(i217, o276, i18) -{4,4}> get_FieldAccess_993(o276, i232, i18, o302') :|: 0 < i232 && 2 <= i18 && 0 < o276 && 0 < o302' && 1 <= i232 && o302' <= o276 && i217 + -1 = i232
create_FieldAccess_749(o112, o110, i18, i4, o111) -{8,8}> get_Inc_957(i4, o112, i18) :|: 0 < o111 && 2 <= i18 && 0 < o110 && 0 < o112 && 0 < o111''' && o111''' <= o111 + o112
get_FieldAccess_993(o306, i237, i18, o302) -{3,3}> get_Inc_957(i237, o306, i18) :|: 0 < o306 && 2 <= i18 && 1 <= i237 && 0 < o302
get_FieldAccess_993(o301, i237, i18, o302) -{3,3}> get_Inc_957(i237, o302, i18) :|: 1 <= i237 && 2 <= i18 && 0 < o301 && 0 < o302

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

Moved arithmethic from constraints to rhss.

create_Duplicate_690(o112, i145, o110, o111, i18, i4) -{13,13}> create_LE_725(i151', o110, o112''', i18, i4, o111) :|: o112''' = o112 + o111 && 2 <= i18 && 0 <= i151' && 0 < o111 && 0 < o112''' && i145 + -1 = i151' && 0 < o110 && 0 < o112 && o112''' <= o112 + o111 && 1 <= i145
was transformed to
create_Duplicate_690(o112, i145, o110, o111, i18, i4) -{13,13}> create_LE_725(i145 + -1, o110, o112 + o111, i18, i4, o111) :|: o112''' = o112 + o111 && 2 <= i18 && 0 <= i151' && 0 < o111 && 0 < o112''' && i145 + -1 = i151' && 0 < o110 && 0 < o112 && o112''' <= o112 + o111 && 1 <= i145

get_Inc_570(i103, o67) -{7,7}> get_Inc_570(i120, o67) :|: 0 < i120 && 0 < o67 && 1 <= i120 && i103 + -1 = i120
was transformed to
get_Inc_570(i103, o67) -{7,7}> get_Inc_570(i103 + -1, o67) :|: 0 < i120 && 0 < o67 && 1 <= i120 && i103 + -1 = i120

main_Load_2(i1, i4, static) -{32,32}> create_LE_84(i6', o4''', i1, i4) :|: static'1 <= static''' + 1 && 0 < o4''' && 0 <= 2 && o4''' <= 1 + 0 && 0 <= static''' && 0 < 1 && static''' <= static + 2 && o4''' = 1 + 0 && 0 <= 1 && 0 <= static && 0 <= static'1 && 0 >= 0 && 0 < 2 && i1 + -1 = i6'
was transformed to
main_Load_2(i1, i4, static) -{32,32}> create_LE_84(i1 + -1, 1 + 0, i1, i4) :|: static'1 <= static''' + 1 && 0 < o4''' && 0 <= 2 && o4''' <= 1 + 0 && 0 <= static''' && 0 < 1 && static''' <= static + 2 && o4''' = 1 + 0 && 0 <= 1 && 0 <= static && 0 <= static'1 && 0 >= 0 && 0 < 2 && i1 + -1 = i6'

get_Inc_957(i217, o276, i18) -{4,4}> get_FieldAccess_993(o276, i232, i18, o302') :|: 0 < i232 && 2 <= i18 && 0 < o276 && 0 < o302' && 1 <= i232 && o302' <= o276 && i217 + -1 = i232
was transformed to
get_Inc_957(i217, o276, i18) -{4,4}> get_FieldAccess_993(o276, i217 + -1, i18, o302') :|: 0 < i232 && 2 <= i18 && 0 < o276 && 0 < o302' && 1 <= i232 && o302' <= o276 && i217 + -1 = i232

(38) Obligation:

IntTrs with 12 rules
Start term: main_Load_2(#0, #1, static)
Considered paths: all paths from start
Rules:
create_LE_725(i158, o110, o112, i18, i4, o111) -{2,2}> create_Duplicate_690(1, i158, o110, o112, i18, i4) :|: 0 < i158 && 2 <= i18 && 0 < 1 && 0 < o111 && 0 < o112 && 1 <= i158 && 0 < o110 && 0 <= i158
create_LE_84(i17, o4, i18, i4) -{2,2}> create_Duplicate_690(1, i17, o4, o4, i18, i4) :|: 0 < 1 && 2 <= i18 && 1 <= i17 && 0 < o4 && 0 < i17
create_Duplicate_690(o112, i145, o110, o111, i18, i4) -{13,13}> create_LE_725(i145 + -1, o110, o112 + o111, i18, i4, o111) :|: o112''' = o112 + o111 && 2 <= i18 && 0 <= i151' && 0 < o111 && 0 < o112''' && i145 + -1 = i151' && 0 < o110 && 0 < o112 && o112''' <= o112 + o111 && 1 <= i145
get_Inc_570(i103, o67) -{7,7}> get_Inc_570(i103 + -1, o67) :|: 0 < i120 && 0 < o67 && 1 <= i120 && i103 + -1 = i120
create_LE_84(i16, o4'1, i1, i4) -{12,12}> get_Inc_570(i4, o4'1) :|: 0 < o4'1 && i16 <= 0 && o4'1 <= o4'1 + o4'1
main_Load_2(i1, i4, static) -{32,32}> create_LE_84(i1 + -1, 1 + 0, i1, i4) :|: static'1 <= static''' + 1 && 0 < o4''' && 0 <= 2 && o4''' <= 1 + 0 && 0 <= static''' && 0 < 1 && static''' <= static + 2 && o4''' = 1 + 0 && 0 <= 1 && 0 <= static && 0 <= static'1 && 0 >= 0 && 0 < 2 && i1 + -1 = i6'
create_FieldAccess_749(o112, o163''', i18, i4, o111) -{8,8}> get_Inc_957(i4, o112'1, i18) :|: 0 < o111 && 0 < o163''' && 0 < o112 && 0 < o112'1 && 2 <= i18 && o163''' <= o163''' + o112 && o112'1 <= o112 + o112
get_Inc_957(i217, o276, i18) -{4,4}> get_FieldAccess_993(o276, i217 + -1, i18, o302') :|: 0 < i232 && 2 <= i18 && 0 < o276 && 0 < o302' && 1 <= i232 && o302' <= o276 && i217 + -1 = i232
get_FieldAccess_993(o306, i237, i18, o302) -{3,3}> get_Inc_957(i237, o306, i18) :|: 0 < o306 && 2 <= i18 && 1 <= i237 && 0 < o302
create_FieldAccess_749(o112, o110, i18, i4, o111) -{8,8}> get_Inc_957(i4, o112, i18) :|: 0 < o111 && 2 <= i18 && 0 < o110 && 0 < o112 && 0 < o111''' && o111''' <= o111 + o112
create_LE_725(x, o110, o112, i18, i4, o111) -{4,4}> create_FieldAccess_749(o112, o110, i18, i4, o111) :|: 0 < o110 && 2 <= i18 && 0 <= 0 && 0 < o111 && 0 < o112 && x = 0
get_FieldAccess_993(o301, i237, i18, o302) -{3,3}> get_Inc_957(i237, o302, i18) :|: 1 <= i237 && 2 <= i18 && 0 < o301 && 0 < o302

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

Simplified expressions.

create_LE_725(i158, o110, o112, i18, i4, o111) -{2,2}> create_Duplicate_690(1, i158, o110, o112, i18, i4) :|: 0 < i158 && 2 <= i18 && 0 < 1 && 0 < o111 && 0 < o112 && 1 <= i158 && 0 < o110 && 0 <= i158
was transformed to
create_LE_725(i158, o110, o112, i18, i4, o111) -{2,2}> create_Duplicate_690(1, i158, o110, o112, i18, i4) :|: 0 < i158 && 2 <= i18 && 0 < o111 && 0 < o112 && 1 <= i158 && 0 < o110

create_LE_84(i17, o4, i18, i4) -{2,2}> create_Duplicate_690(1, i17, o4, o4, i18, i4) :|: 0 < 1 && 2 <= i18 && 1 <= i17 && 0 < o4 && 0 < i17
was transformed to
create_LE_84(i17, o4, i18, i4) -{2,2}> create_Duplicate_690(1, i17, o4, o4, i18, i4) :|: 2 <= i18 && 1 <= i17 && 0 < o4 && 0 < i17

get_Inc_570(i103, o67) -{7,7}> get_Inc_570(i103 + -1, o67) :|: 0 < i120 && 0 < o67 && 1 <= i120 && i103 + -1 = i120
was transformed to
get_Inc_570(i103, o67) -{7,7}> get_Inc_570(i103 - 1, o67) :|: 0 < i120 && 0 < o67 && 1 <= i120 && i103 - 1 = i120

create_LE_84(i16, o4'1, i1, i4) -{12,12}> get_Inc_570(i4, o4'1) :|: 0 < o4'1 && i16 <= 0 && o4'1 <= o4'1 + o4'1
was transformed to
create_LE_84(i16, o4'1, i1, i4) -{12,12}> get_Inc_570(i4, o4'1) :|: 0 < o4'1 && i16 <= 0 && o4'1 <= 2 * o4'1

get_Inc_957(i217, o276, i18) -{4,4}> get_FieldAccess_993(o276, i217 + -1, i18, o302') :|: 0 < i232 && 2 <= i18 && 0 < o276 && 0 < o302' && 1 <= i232 && o302' <= o276 && i217 + -1 = i232
was transformed to
get_Inc_957(i217, o276, i18) -{4,4}> get_FieldAccess_993(o276, i217 - 1, i18, o302') :|: 0 < i232 && 2 <= i18 && 0 < o276 && 0 < o302' && 1 <= i232 && o302' <= o276 && i217 - 1 = i232

create_FieldAccess_749(o112, o163''', i18, i4, o111) -{8,8}> get_Inc_957(i4, o112'1, i18) :|: 0 < o111 && 0 < o163''' && 0 < o112 && 0 < o112'1 && 2 <= i18 && o163''' <= o163''' + o112 && o112'1 <= o112 + o112
was transformed to
create_FieldAccess_749(o112, o163''', i18, i4, o111) -{8,8}> get_Inc_957(i4, o112'1, i18) :|: 0 < o111 && 0 < o163''' && 0 < o112 && 0 < o112'1 && 2 <= i18 && o163''' <= o163''' + o112 && o112'1 <= 2 * o112

main_Load_2(i1, i4, static) -{32,32}> create_LE_84(i1 + -1, 1 + 0, i1, i4) :|: static'1 <= static''' + 1 && 0 < o4''' && 0 <= 2 && o4''' <= 1 + 0 && 0 <= static''' && 0 < 1 && static''' <= static + 2 && o4''' = 1 + 0 && 0 <= 1 && 0 <= static && 0 <= static'1 && 0 >= 0 && 0 < 2 && i1 + -1 = i6'
was transformed to
main_Load_2(i1, i4, static) -{32,32}> create_LE_84(i1 - 1, 1, i1, i4) :|: static'1 <= static''' + 1 && 0 < o4''' && 0 <= static''' && static''' <= static + 2 && o4''' = 1 && 0 <= static && 0 <= static'1 && i1 - 1 = i6'

create_LE_725(x, o110, o112, i18, i4, o111) -{4,4}> create_FieldAccess_749(o112, o110, i18, i4, o111) :|: 0 < o110 && 2 <= i18 && 0 <= 0 && 0 < o111 && 0 < o112 && x = 0
was transformed to
create_LE_725(x, o110, o112, i18, i4, o111) -{4,4}> create_FieldAccess_749(o112, o110, i18, i4, o111) :|: 0 < o110 && 2 <= i18 && 0 < o111 && 0 < o112 && x = 0

create_Duplicate_690(o112, i145, o110, o111, i18, i4) -{13,13}> create_LE_725(i145 + -1, o110, o112 + o111, i18, i4, o111) :|: o112''' = o112 + o111 && 2 <= i18 && 0 <= i151' && 0 < o111 && 0 < o112''' && i145 + -1 = i151' && 0 < o110 && 0 < o112 && o112''' <= o112 + o111 && 1 <= i145
was transformed to
create_Duplicate_690(o112, i145, o110, o111, i18, i4) -{13,13}> create_LE_725(i145 - 1, o110, o112 + o111, i18, i4, o111) :|: o112''' = o112 + o111 && 2 <= i18 && 0 <= i151' && 0 < o111 && 0 < o112''' && i145 - 1 = i151' && 0 < o110 && 0 < o112 && 1 <= i145

(40) Obligation:

IntTrs with 12 rules
Start term: main_Load_2(#0, #1, static)
Considered paths: all paths from start
Rules:
create_FieldAccess_749(o112, o163''', i18, i4, o111) -{8,8}> get_Inc_957(i4, o112'1, i18) :|: 0 < o111 && 0 < o163''' && 0 < o112 && 0 < o112'1 && 2 <= i18 && o163''' <= o163''' + o112 && o112'1 <= 2 * o112
create_LE_725(x, o110, o112, i18, i4, o111) -{4,4}> create_FieldAccess_749(o112, o110, i18, i4, o111) :|: 0 < o110 && 2 <= i18 && 0 < o111 && 0 < o112 && x = 0
get_Inc_957(i217, o276, i18) -{4,4}> get_FieldAccess_993(o276, i217 - 1, i18, o302') :|: 0 < i232 && 2 <= i18 && 0 < o276 && 0 < o302' && 1 <= i232 && o302' <= o276 && i217 - 1 = i232
create_Duplicate_690(o112, i145, o110, o111, i18, i4) -{13,13}> create_LE_725(i145 - 1, o110, o112 + o111, i18, i4, o111) :|: o112''' = o112 + o111 && 2 <= i18 && 0 <= i151' && 0 < o111 && 0 < o112''' && i145 - 1 = i151' && 0 < o110 && 0 < o112 && 1 <= i145
create_LE_725(i158, o110, o112, i18, i4, o111) -{2,2}> create_Duplicate_690(1, i158, o110, o112, i18, i4) :|: 0 < i158 && 2 <= i18 && 0 < o111 && 0 < o112 && 1 <= i158 && 0 < o110
main_Load_2(i1, i4, static) -{32,32}> create_LE_84(i1 - 1, 1, i1, i4) :|: static'1 <= static''' + 1 && 0 < o4''' && 0 <= static''' && static''' <= static + 2 && o4''' = 1 && 0 <= static && 0 <= static'1 && i1 - 1 = i6'
create_FieldAccess_749(o112, o110, i18, i4, o111) -{8,8}> get_Inc_957(i4, o112, i18) :|: 0 < o111 && 2 <= i18 && 0 < o110 && 0 < o112 && 0 < o111''' && o111''' <= o111 + o112
get_FieldAccess_993(o306, i237, i18, o302) -{3,3}> get_Inc_957(i237, o306, i18) :|: 0 < o306 && 2 <= i18 && 1 <= i237 && 0 < o302
create_LE_84(i17, o4, i18, i4) -{2,2}> create_Duplicate_690(1, i17, o4, o4, i18, i4) :|: 2 <= i18 && 1 <= i17 && 0 < o4 && 0 < i17
create_LE_84(i16, o4'1, i1, i4) -{12,12}> get_Inc_570(i4, o4'1) :|: 0 < o4'1 && i16 <= 0 && o4'1 <= 2 * o4'1
get_Inc_570(i103, o67) -{7,7}> get_Inc_570(i103 - 1, o67) :|: 0 < i120 && 0 < o67 && 1 <= i120 && i103 - 1 = i120
get_FieldAccess_993(o301, i237, i18, o302) -{3,3}> get_Inc_957(i237, o302, i18) :|: 1 <= i237 && 2 <= i18 && 0 < o301 && 0 < o302

(41) koat Proof (EQUIVALENT transformation)

YES(?, 34*ar_1 + 30*ar_0 + 116)

Initial complexity problem:
1: T:
(Comp: ?, Cost: 8) create_FieldAccess_749(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(get_Inc_957(ar_3, o112'1, ar_2, arityPad, arityPad, arityPad)) [ 0 < ar_4 /\ 0 < ar_1 /\ 0 < ar_0 /\ 0 < o112'1 /\ 2 <= ar_2 /\ ar_1 <= ar_1 + ar_0 /\ o112'1 <= 2*ar_0 ]
(Comp: ?, Cost: 4) create_LE_725(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(create_FieldAccess_749(ar_2, ar_1, ar_3, ar_4, ar_5, arityPad)) [ 0 < ar_1 /\ 2 <= ar_3 /\ 0 < ar_5 /\ 0 < ar_2 /\ ar_0 = 0 ]
(Comp: ?, Cost: 4) get_Inc_957(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(get_FieldAccess_993(ar_1, ar_0 - 1, ar_2, o302', arityPad, arityPad)) [ 0 < i232 /\ 2 <= ar_2 /\ 0 < ar_1 /\ 0 < o302' /\ 1 <= i232 /\ o302' <= ar_1 /\ ar_0 - 1 = i232 ]
(Comp: ?, Cost: 13) create_Duplicate_690(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(create_LE_725(ar_1 - 1, ar_2, ar_0 + ar_3, ar_4, ar_5, ar_3)) [ o112''' = ar_0 + ar_3 /\ 2 <= ar_4 /\ 0 <= i151' /\ 0 < ar_3 /\ 0 < o112''' /\ ar_1 - 1 = i151' /\ 0 < ar_2 /\ 0 < ar_0 /\ 1 <= ar_1 ]
(Comp: ?, Cost: 2) create_LE_725(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(create_Duplicate_690(1, ar_0, ar_1, ar_2, ar_3, ar_4)) [ 0 < ar_0 /\ 2 <= ar_3 /\ 0 < ar_5 /\ 0 < ar_2 /\ 1 <= ar_0 /\ 0 < ar_1 ]
(Comp: ?, Cost: 32) main_Load_2(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(create_LE_84(ar_0 - 1, 1, ar_0, ar_1, arityPad, arityPad)) [ static'1 <= static''' + 1 /\ 0 < o4''' /\ 0 <= static''' /\ static''' <= ar_2 + 2 /\ o4''' = 1 /\ 0 <= ar_2 /\ 0 <= static'1 /\ ar_0 - 1 = i6' ]
(Comp: ?, Cost: 8) create_FieldAccess_749(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(get_Inc_957(ar_3, ar_0, ar_2, arityPad, arityPad, arityPad)) [ 0 < ar_4 /\ 2 <= ar_2 /\ 0 < ar_1 /\ 0 < ar_0 /\ 0 < o111''' /\ o111''' <= ar_4 + ar_0 ]
(Comp: ?, Cost: 3) get_FieldAccess_993(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(get_Inc_957(ar_1, ar_0, ar_2, arityPad, arityPad, arityPad)) [ 0 < ar_0 /\ 2 <= ar_2 /\ 1 <= ar_1 /\ 0 < ar_3 ]
(Comp: ?, Cost: 2) create_LE_84(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(create_Duplicate_690(1, ar_0, ar_1, ar_1, ar_2, ar_3)) [ 2 <= ar_2 /\ 1 <= ar_0 /\ 0 < ar_1 /\ 0 < ar_0 ]
(Comp: ?, Cost: 12) create_LE_84(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(get_Inc_570(ar_3, ar_1, arityPad, arityPad, arityPad, arityPad)) [ 0 < ar_1 /\ ar_0 <= 0 /\ ar_1 <= 2*ar_1 ]
(Comp: ?, Cost: 7) get_Inc_570(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(get_Inc_570(ar_0 - 1, ar_1, arityPad, arityPad, arityPad, arityPad)) [ 0 < i120 /\ 0 < ar_1 /\ 1 <= i120 /\ ar_0 - 1 = i120 ]
(Comp: ?, Cost: 3) get_FieldAccess_993(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(get_Inc_957(ar_1, ar_3, ar_2, arityPad, arityPad, arityPad)) [ 1 <= ar_1 /\ 2 <= ar_2 /\ 0 < ar_0 /\ 0 < ar_3 ]
(Comp: 1, Cost: 0) koat_start(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(main_Load_2(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5)) [ 0 <= 0 ]
start location: koat_start
leaf cost: 0

Repeatedly propagating knowledge in problem 1 produces the following problem:
2: T:
(Comp: ?, Cost: 8) create_FieldAccess_749(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(get_Inc_957(ar_3, o112'1, ar_2, arityPad, arityPad, arityPad)) [ 0 < ar_4 /\ 0 < ar_1 /\ 0 < ar_0 /\ 0 < o112'1 /\ 2 <= ar_2 /\ ar_1 <= ar_1 + ar_0 /\ o112'1 <= 2*ar_0 ]
(Comp: ?, Cost: 4) create_LE_725(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(create_FieldAccess_749(ar_2, ar_1, ar_3, ar_4, ar_5, arityPad)) [ 0 < ar_1 /\ 2 <= ar_3 /\ 0 < ar_5 /\ 0 < ar_2 /\ ar_0 = 0 ]
(Comp: ?, Cost: 4) get_Inc_957(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(get_FieldAccess_993(ar_1, ar_0 - 1, ar_2, o302', arityPad, arityPad)) [ 0 < i232 /\ 2 <= ar_2 /\ 0 < ar_1 /\ 0 < o302' /\ 1 <= i232 /\ o302' <= ar_1 /\ ar_0 - 1 = i232 ]
(Comp: ?, Cost: 13) create_Duplicate_690(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(create_LE_725(ar_1 - 1, ar_2, ar_0 + ar_3, ar_4, ar_5, ar_3)) [ o112''' = ar_0 + ar_3 /\ 2 <= ar_4 /\ 0 <= i151' /\ 0 < ar_3 /\ 0 < o112''' /\ ar_1 - 1 = i151' /\ 0 < ar_2 /\ 0 < ar_0 /\ 1 <= ar_1 ]
(Comp: ?, Cost: 2) create_LE_725(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(create_Duplicate_690(1, ar_0, ar_1, ar_2, ar_3, ar_4)) [ 0 < ar_0 /\ 2 <= ar_3 /\ 0 < ar_5 /\ 0 < ar_2 /\ 1 <= ar_0 /\ 0 < ar_1 ]
(Comp: 1, Cost: 32) main_Load_2(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(create_LE_84(ar_0 - 1, 1, ar_0, ar_1, arityPad, arityPad)) [ static'1 <= static''' + 1 /\ 0 < o4''' /\ 0 <= static''' /\ static''' <= ar_2 + 2 /\ o4''' = 1 /\ 0 <= ar_2 /\ 0 <= static'1 /\ ar_0 - 1 = i6' ]
(Comp: ?, Cost: 8) create_FieldAccess_749(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(get_Inc_957(ar_3, ar_0, ar_2, arityPad, arityPad, arityPad)) [ 0 < ar_4 /\ 2 <= ar_2 /\ 0 < ar_1 /\ 0 < ar_0 /\ 0 < o111''' /\ o111''' <= ar_4 + ar_0 ]
(Comp: ?, Cost: 3) get_FieldAccess_993(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(get_Inc_957(ar_1, ar_0, ar_2, arityPad, arityPad, arityPad)) [ 0 < ar_0 /\ 2 <= ar_2 /\ 1 <= ar_1 /\ 0 < ar_3 ]
(Comp: 1, Cost: 2) create_LE_84(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(create_Duplicate_690(1, ar_0, ar_1, ar_1, ar_2, ar_3)) [ 2 <= ar_2 /\ 1 <= ar_0 /\ 0 < ar_1 /\ 0 < ar_0 ]
(Comp: 1, Cost: 12) create_LE_84(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(get_Inc_570(ar_3, ar_1, arityPad, arityPad, arityPad, arityPad)) [ 0 < ar_1 /\ ar_0 <= 0 /\ ar_1 <= 2*ar_1 ]
(Comp: ?, Cost: 7) get_Inc_570(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(get_Inc_570(ar_0 - 1, ar_1, arityPad, arityPad, arityPad, arityPad)) [ 0 < i120 /\ 0 < ar_1 /\ 1 <= i120 /\ ar_0 - 1 = i120 ]
(Comp: ?, Cost: 3) get_FieldAccess_993(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(get_Inc_957(ar_1, ar_3, ar_2, arityPad, arityPad, arityPad)) [ 1 <= ar_1 /\ 2 <= ar_2 /\ 0 < ar_0 /\ 0 < ar_3 ]
(Comp: 1, Cost: 0) koat_start(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(main_Load_2(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5)) [ 0 <= 0 ]
start location: koat_start
leaf cost: 0

A polynomial rank function with
Pol(create_FieldAccess_749) = 1
Pol(get_Inc_957) = 0
Pol(create_LE_725) = 2
Pol(get_FieldAccess_993) = 0
Pol(create_Duplicate_690) = 2
Pol(main_Load_2) = 2
Pol(create_LE_84) = 2
Pol(get_Inc_570) = 0
Pol(koat_start) = 2
orients all transitions weakly and the transitions
create_LE_725(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(create_FieldAccess_749(ar_2, ar_1, ar_3, ar_4, ar_5, arityPad)) [ 0 < ar_1 /\ 2 <= ar_3 /\ 0 < ar_5 /\ 0 < ar_2 /\ ar_0 = 0 ]
create_FieldAccess_749(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(get_Inc_957(ar_3, o112'1, ar_2, arityPad, arityPad, arityPad)) [ 0 < ar_4 /\ 0 < ar_1 /\ 0 < ar_0 /\ 0 < o112'1 /\ 2 <= ar_2 /\ ar_1 <= ar_1 + ar_0 /\ o112'1 <= 2*ar_0 ]
create_FieldAccess_749(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(get_Inc_957(ar_3, ar_0, ar_2, arityPad, arityPad, arityPad)) [ 0 < ar_4 /\ 2 <= ar_2 /\ 0 < ar_1 /\ 0 < ar_0 /\ 0 < o111''' /\ o111''' <= ar_4 + ar_0 ]
strictly and produces the following problem:
3: T:
(Comp: 2, Cost: 8) create_FieldAccess_749(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(get_Inc_957(ar_3, o112'1, ar_2, arityPad, arityPad, arityPad)) [ 0 < ar_4 /\ 0 < ar_1 /\ 0 < ar_0 /\ 0 < o112'1 /\ 2 <= ar_2 /\ ar_1 <= ar_1 + ar_0 /\ o112'1 <= 2*ar_0 ]
(Comp: 2, Cost: 4) create_LE_725(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(create_FieldAccess_749(ar_2, ar_1, ar_3, ar_4, ar_5, arityPad)) [ 0 < ar_1 /\ 2 <= ar_3 /\ 0 < ar_5 /\ 0 < ar_2 /\ ar_0 = 0 ]
(Comp: ?, Cost: 4) get_Inc_957(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(get_FieldAccess_993(ar_1, ar_0 - 1, ar_2, o302', arityPad, arityPad)) [ 0 < i232 /\ 2 <= ar_2 /\ 0 < ar_1 /\ 0 < o302' /\ 1 <= i232 /\ o302' <= ar_1 /\ ar_0 - 1 = i232 ]
(Comp: ?, Cost: 13) create_Duplicate_690(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(create_LE_725(ar_1 - 1, ar_2, ar_0 + ar_3, ar_4, ar_5, ar_3)) [ o112''' = ar_0 + ar_3 /\ 2 <= ar_4 /\ 0 <= i151' /\ 0 < ar_3 /\ 0 < o112''' /\ ar_1 - 1 = i151' /\ 0 < ar_2 /\ 0 < ar_0 /\ 1 <= ar_1 ]
(Comp: ?, Cost: 2) create_LE_725(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(create_Duplicate_690(1, ar_0, ar_1, ar_2, ar_3, ar_4)) [ 0 < ar_0 /\ 2 <= ar_3 /\ 0 < ar_5 /\ 0 < ar_2 /\ 1 <= ar_0 /\ 0 < ar_1 ]
(Comp: 1, Cost: 32) main_Load_2(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(create_LE_84(ar_0 - 1, 1, ar_0, ar_1, arityPad, arityPad)) [ static'1 <= static''' + 1 /\ 0 < o4''' /\ 0 <= static''' /\ static''' <= ar_2 + 2 /\ o4''' = 1 /\ 0 <= ar_2 /\ 0 <= static'1 /\ ar_0 - 1 = i6' ]
(Comp: 2, Cost: 8) create_FieldAccess_749(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(get_Inc_957(ar_3, ar_0, ar_2, arityPad, arityPad, arityPad)) [ 0 < ar_4 /\ 2 <= ar_2 /\ 0 < ar_1 /\ 0 < ar_0 /\ 0 < o111''' /\ o111''' <= ar_4 + ar_0 ]
(Comp: ?, Cost: 3) get_FieldAccess_993(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(get_Inc_957(ar_1, ar_0, ar_2, arityPad, arityPad, arityPad)) [ 0 < ar_0 /\ 2 <= ar_2 /\ 1 <= ar_1 /\ 0 < ar_3 ]
(Comp: 1, Cost: 2) create_LE_84(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(create_Duplicate_690(1, ar_0, ar_1, ar_1, ar_2, ar_3)) [ 2 <= ar_2 /\ 1 <= ar_0 /\ 0 < ar_1 /\ 0 < ar_0 ]
(Comp: 1, Cost: 12) create_LE_84(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(get_Inc_570(ar_3, ar_1, arityPad, arityPad, arityPad, arityPad)) [ 0 < ar_1 /\ ar_0 <= 0 /\ ar_1 <= 2*ar_1 ]
(Comp: ?, Cost: 7) get_Inc_570(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(get_Inc_570(ar_0 - 1, ar_1, arityPad, arityPad, arityPad, arityPad)) [ 0 < i120 /\ 0 < ar_1 /\ 1 <= i120 /\ ar_0 - 1 = i120 ]
(Comp: ?, Cost: 3) get_FieldAccess_993(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(get_Inc_957(ar_1, ar_3, ar_2, arityPad, arityPad, arityPad)) [ 1 <= ar_1 /\ 2 <= ar_2 /\ 0 < ar_0 /\ 0 < ar_3 ]
(Comp: 1, Cost: 0) koat_start(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(main_Load_2(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5)) [ 0 <= 0 ]
start location: koat_start
leaf cost: 0

A polynomial rank function with
Pol(create_FieldAccess_749) = 2*V_4
Pol(get_Inc_957) = 2*V_1
Pol(create_LE_725) = 2*V_5
Pol(get_FieldAccess_993) = 2*V_2 + 1
Pol(create_Duplicate_690) = 2*V_6
Pol(main_Load_2) = 2*V_2
Pol(create_LE_84) = 2*V_4
Pol(get_Inc_570) = 2*V_1
Pol(koat_start) = 2*V_2
orients all transitions weakly and the transitions
get_Inc_957(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(get_FieldAccess_993(ar_1, ar_0 - 1, ar_2, o302', arityPad, arityPad)) [ 0 < i232 /\ 2 <= ar_2 /\ 0 < ar_1 /\ 0 < o302' /\ 1 <= i232 /\ o302' <= ar_1 /\ ar_0 - 1 = i232 ]
get_Inc_570(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(get_Inc_570(ar_0 - 1, ar_1, arityPad, arityPad, arityPad, arityPad)) [ 0 < i120 /\ 0 < ar_1 /\ 1 <= i120 /\ ar_0 - 1 = i120 ]
get_FieldAccess_993(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(get_Inc_957(ar_1, ar_3, ar_2, arityPad, arityPad, arityPad)) [ 1 <= ar_1 /\ 2 <= ar_2 /\ 0 < ar_0 /\ 0 < ar_3 ]
get_FieldAccess_993(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(get_Inc_957(ar_1, ar_0, ar_2, arityPad, arityPad, arityPad)) [ 0 < ar_0 /\ 2 <= ar_2 /\ 1 <= ar_1 /\ 0 < ar_3 ]
strictly and produces the following problem:
4: T:
(Comp: 2, Cost: 8) create_FieldAccess_749(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(get_Inc_957(ar_3, o112'1, ar_2, arityPad, arityPad, arityPad)) [ 0 < ar_4 /\ 0 < ar_1 /\ 0 < ar_0 /\ 0 < o112'1 /\ 2 <= ar_2 /\ ar_1 <= ar_1 + ar_0 /\ o112'1 <= 2*ar_0 ]
(Comp: 2, Cost: 4) create_LE_725(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(create_FieldAccess_749(ar_2, ar_1, ar_3, ar_4, ar_5, arityPad)) [ 0 < ar_1 /\ 2 <= ar_3 /\ 0 < ar_5 /\ 0 < ar_2 /\ ar_0 = 0 ]
(Comp: 2*ar_1, Cost: 4) get_Inc_957(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(get_FieldAccess_993(ar_1, ar_0 - 1, ar_2, o302', arityPad, arityPad)) [ 0 < i232 /\ 2 <= ar_2 /\ 0 < ar_1 /\ 0 < o302' /\ 1 <= i232 /\ o302' <= ar_1 /\ ar_0 - 1 = i232 ]
(Comp: ?, Cost: 13) create_Duplicate_690(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(create_LE_725(ar_1 - 1, ar_2, ar_0 + ar_3, ar_4, ar_5, ar_3)) [ o112''' = ar_0 + ar_3 /\ 2 <= ar_4 /\ 0 <= i151' /\ 0 < ar_3 /\ 0 < o112''' /\ ar_1 - 1 = i151' /\ 0 < ar_2 /\ 0 < ar_0 /\ 1 <= ar_1 ]
(Comp: ?, Cost: 2) create_LE_725(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(create_Duplicate_690(1, ar_0, ar_1, ar_2, ar_3, ar_4)) [ 0 < ar_0 /\ 2 <= ar_3 /\ 0 < ar_5 /\ 0 < ar_2 /\ 1 <= ar_0 /\ 0 < ar_1 ]
(Comp: 1, Cost: 32) main_Load_2(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(create_LE_84(ar_0 - 1, 1, ar_0, ar_1, arityPad, arityPad)) [ static'1 <= static''' + 1 /\ 0 < o4''' /\ 0 <= static''' /\ static''' <= ar_2 + 2 /\ o4''' = 1 /\ 0 <= ar_2 /\ 0 <= static'1 /\ ar_0 - 1 = i6' ]
(Comp: 2, Cost: 8) create_FieldAccess_749(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(get_Inc_957(ar_3, ar_0, ar_2, arityPad, arityPad, arityPad)) [ 0 < ar_4 /\ 2 <= ar_2 /\ 0 < ar_1 /\ 0 < ar_0 /\ 0 < o111''' /\ o111''' <= ar_4 + ar_0 ]
(Comp: 2*ar_1, Cost: 3) get_FieldAccess_993(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(get_Inc_957(ar_1, ar_0, ar_2, arityPad, arityPad, arityPad)) [ 0 < ar_0 /\ 2 <= ar_2 /\ 1 <= ar_1 /\ 0 < ar_3 ]
(Comp: 1, Cost: 2) create_LE_84(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(create_Duplicate_690(1, ar_0, ar_1, ar_1, ar_2, ar_3)) [ 2 <= ar_2 /\ 1 <= ar_0 /\ 0 < ar_1 /\ 0 < ar_0 ]
(Comp: 1, Cost: 12) create_LE_84(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(get_Inc_570(ar_3, ar_1, arityPad, arityPad, arityPad, arityPad)) [ 0 < ar_1 /\ ar_0 <= 0 /\ ar_1 <= 2*ar_1 ]
(Comp: 2*ar_1, Cost: 7) get_Inc_570(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(get_Inc_570(ar_0 - 1, ar_1, arityPad, arityPad, arityPad, arityPad)) [ 0 < i120 /\ 0 < ar_1 /\ 1 <= i120 /\ ar_0 - 1 = i120 ]
(Comp: 2*ar_1, Cost: 3) get_FieldAccess_993(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(get_Inc_957(ar_1, ar_3, ar_2, arityPad, arityPad, arityPad)) [ 1 <= ar_1 /\ 2 <= ar_2 /\ 0 < ar_0 /\ 0 < ar_3 ]
(Comp: 1, Cost: 0) koat_start(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(main_Load_2(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5)) [ 0 <= 0 ]
start location: koat_start
leaf cost: 0

A polynomial rank function with
Pol(create_LE_725) = 2*V_1 + 1
Pol(create_Duplicate_690) = 2*V_2
and size complexities
S("koat_start(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(main_Load_2(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5)) [ 0 <= 0 ]", 0-0) = ar_0
S("koat_start(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(main_Load_2(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5)) [ 0 <= 0 ]", 0-1) = ar_1
S("koat_start(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(main_Load_2(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5)) [ 0 <= 0 ]", 0-2) = ar_2
S("koat_start(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(main_Load_2(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5)) [ 0 <= 0 ]", 0-3) = ar_3
S("koat_start(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(main_Load_2(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5)) [ 0 <= 0 ]", 0-4) = ar_4
S("koat_start(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(main_Load_2(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5)) [ 0 <= 0 ]", 0-5) = ar_5
S("get_FieldAccess_993(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(get_Inc_957(ar_1, ar_3, ar_2, arityPad, arityPad, arityPad)) [ 1 <= ar_1 /\\ 2 <= ar_2 /\\ 0 < ar_0 /\\ 0 < ar_3 ]", 0-0) = ar_1
S("get_FieldAccess_993(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(get_Inc_957(ar_1, ar_3, ar_2, arityPad, arityPad, arityPad)) [ 1 <= ar_1 /\\ 2 <= ar_2 /\\ 0 < ar_0 /\\ 0 < ar_3 ]", 0-1) = ?
S("get_FieldAccess_993(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(get_Inc_957(ar_1, ar_3, ar_2, arityPad, arityPad, arityPad)) [ 1 <= ar_1 /\\ 2 <= ar_2 /\\ 0 < ar_0 /\\ 0 < ar_3 ]", 0-2) = ar_0
S("get_FieldAccess_993(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(get_Inc_957(ar_1, ar_3, ar_2, arityPad, arityPad, arityPad)) [ 1 <= ar_1 /\\ 2 <= ar_2 /\\ 0 < ar_0 /\\ 0 < ar_3 ]", 0-3) = ?
S("get_FieldAccess_993(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(get_Inc_957(ar_1, ar_3, ar_2, arityPad, arityPad, arityPad)) [ 1 <= ar_1 /\\ 2 <= ar_2 /\\ 0 < ar_0 /\\ 0 < ar_3 ]", 0-4) = ?
S("get_FieldAccess_993(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(get_Inc_957(ar_1, ar_3, ar_2, arityPad, arityPad, arityPad)) [ 1 <= ar_1 /\\ 2 <= ar_2 /\\ 0 < ar_0 /\\ 0 < ar_3 ]", 0-5) = ?
S("get_Inc_570(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(get_Inc_570(ar_0 - 1, ar_1, arityPad, arityPad, arityPad, arityPad)) [ 0 < i120 /\\ 0 < ar_1 /\\ 1 <= i120 /\\ ar_0 - 1 = i120 ]", 0-0) = ar_1
S("get_Inc_570(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(get_Inc_570(ar_0 - 1, ar_1, arityPad, arityPad, arityPad, arityPad)) [ 0 < i120 /\\ 0 < ar_1 /\\ 1 <= i120 /\\ ar_0 - 1 = i120 ]", 0-1) = 1
S("get_Inc_570(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(get_Inc_570(ar_0 - 1, ar_1, arityPad, arityPad, arityPad, arityPad)) [ 0 < i120 /\\ 0 < ar_1 /\\ 1 <= i120 /\\ ar_0 - 1 = i120 ]", 0-2) = ?
S("get_Inc_570(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(get_Inc_570(ar_0 - 1, ar_1, arityPad, arityPad, arityPad, arityPad)) [ 0 < i120 /\\ 0 < ar_1 /\\ 1 <= i120 /\\ ar_0 - 1 = i120 ]", 0-3) = ?
S("get_Inc_570(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(get_Inc_570(ar_0 - 1, ar_1, arityPad, arityPad, arityPad, arityPad)) [ 0 < i120 /\\ 0 < ar_1 /\\ 1 <= i120 /\\ ar_0 - 1 = i120 ]", 0-4) = ?
S("get_Inc_570(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(get_Inc_570(ar_0 - 1, ar_1, arityPad, arityPad, arityPad, arityPad)) [ 0 < i120 /\\ 0 < ar_1 /\\ 1 <= i120 /\\ ar_0 - 1 = i120 ]", 0-5) = ?
S("create_LE_84(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(get_Inc_570(ar_3, ar_1, arityPad, arityPad, arityPad, arityPad)) [ 0 < ar_1 /\\ ar_0 <= 0 /\\ ar_1 <= 2*ar_1 ]", 0-0) = ar_1
S("create_LE_84(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(get_Inc_570(ar_3, ar_1, arityPad, arityPad, arityPad, arityPad)) [ 0 < ar_1 /\\ ar_0 <= 0 /\\ ar_1 <= 2*ar_1 ]", 0-1) = 1
S("create_LE_84(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(get_Inc_570(ar_3, ar_1, arityPad, arityPad, arityPad, arityPad)) [ 0 < ar_1 /\\ ar_0 <= 0 /\\ ar_1 <= 2*ar_1 ]", 0-2) = ?
S("create_LE_84(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(get_Inc_570(ar_3, ar_1, arityPad, arityPad, arityPad, arityPad)) [ 0 < ar_1 /\\ ar_0 <= 0 /\\ ar_1 <= 2*ar_1 ]", 0-3) = ?
S("create_LE_84(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(get_Inc_570(ar_3, ar_1, arityPad, arityPad, arityPad, arityPad)) [ 0 < ar_1 /\\ ar_0 <= 0 /\\ ar_1 <= 2*ar_1 ]", 0-4) = ?
S("create_LE_84(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(get_Inc_570(ar_3, ar_1, arityPad, arityPad, arityPad, arityPad)) [ 0 < ar_1 /\\ ar_0 <= 0 /\\ ar_1 <= 2*ar_1 ]", 0-5) = ?
S("create_LE_84(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(create_Duplicate_690(1, ar_0, ar_1, ar_1, ar_2, ar_3)) [ 2 <= ar_2 /\\ 1 <= ar_0 /\\ 0 < ar_1 /\\ 0 < ar_0 ]", 0-0) = 1
S("create_LE_84(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(create_Duplicate_690(1, ar_0, ar_1, ar_1, ar_2, ar_3)) [ 2 <= ar_2 /\\ 1 <= ar_0 /\\ 0 < ar_1 /\\ 0 < ar_0 ]", 0-1) = ar_0 + 1
S("create_LE_84(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(create_Duplicate_690(1, ar_0, ar_1, ar_1, ar_2, ar_3)) [ 2 <= ar_2 /\\ 1 <= ar_0 /\\ 0 < ar_1 /\\ 0 < ar_0 ]", 0-2) = 1
S("create_LE_84(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(create_Duplicate_690(1, ar_0, ar_1, ar_1, ar_2, ar_3)) [ 2 <= ar_2 /\\ 1 <= ar_0 /\\ 0 < ar_1 /\\ 0 < ar_0 ]", 0-3) = 1
S("create_LE_84(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(create_Duplicate_690(1, ar_0, ar_1, ar_1, ar_2, ar_3)) [ 2 <= ar_2 /\\ 1 <= ar_0 /\\ 0 < ar_1 /\\ 0 < ar_0 ]", 0-4) = ar_0
S("create_LE_84(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(create_Duplicate_690(1, ar_0, ar_1, ar_1, ar_2, ar_3)) [ 2 <= ar_2 /\\ 1 <= ar_0 /\\ 0 < ar_1 /\\ 0 < ar_0 ]", 0-5) = ar_1
S("get_FieldAccess_993(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(get_Inc_957(ar_1, ar_0, ar_2, arityPad, arityPad, arityPad)) [ 0 < ar_0 /\\ 2 <= ar_2 /\\ 1 <= ar_1 /\\ 0 < ar_3 ]", 0-0) = ar_1
S("get_FieldAccess_993(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(get_Inc_957(ar_1, ar_0, ar_2, arityPad, arityPad, arityPad)) [ 0 < ar_0 /\\ 2 <= ar_2 /\\ 1 <= ar_1 /\\ 0 < ar_3 ]", 0-1) = ?
S("get_FieldAccess_993(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(get_Inc_957(ar_1, ar_0, ar_2, arityPad, arityPad, arityPad)) [ 0 < ar_0 /\\ 2 <= ar_2 /\\ 1 <= ar_1 /\\ 0 < ar_3 ]", 0-2) = ar_0
S("get_FieldAccess_993(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(get_Inc_957(ar_1, ar_0, ar_2, arityPad, arityPad, arityPad)) [ 0 < ar_0 /\\ 2 <= ar_2 /\\ 1 <= ar_1 /\\ 0 < ar_3 ]", 0-3) = ?
S("get_FieldAccess_993(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(get_Inc_957(ar_1, ar_0, ar_2, arityPad, arityPad, arityPad)) [ 0 < ar_0 /\\ 2 <= ar_2 /\\ 1 <= ar_1 /\\ 0 < ar_3 ]", 0-4) = ?
S("get_FieldAccess_993(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(get_Inc_957(ar_1, ar_0, ar_2, arityPad, arityPad, arityPad)) [ 0 < ar_0 /\\ 2 <= ar_2 /\\ 1 <= ar_1 /\\ 0 < ar_3 ]", 0-5) = ?
S("create_FieldAccess_749(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(get_Inc_957(ar_3, ar_0, ar_2, arityPad, arityPad, arityPad)) [ 0 < ar_4 /\\ 2 <= ar_2 /\\ 0 < ar_1 /\\ 0 < ar_0 /\\ 0 < o111''' /\\ o111''' <= ar_4 + ar_0 ]", 0-0) = ar_1
S("create_FieldAccess_749(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(get_Inc_957(ar_3, ar_0, ar_2, arityPad, arityPad, arityPad)) [ 0 < ar_4 /\\ 2 <= ar_2 /\\ 0 < ar_1 /\\ 0 < ar_0 /\\ 0 < o111''' /\\ o111''' <= ar_4 + ar_0 ]", 0-1) = ?
S("create_FieldAccess_749(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(get_Inc_957(ar_3, ar_0, ar_2, arityPad, arityPad, arityPad)) [ 0 < ar_4 /\\ 2 <= ar_2 /\\ 0 < ar_1 /\\ 0 < ar_0 /\\ 0 < o111''' /\\ o111''' <= ar_4 + ar_0 ]", 0-2) = ar_0
S("create_FieldAccess_749(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(get_Inc_957(ar_3, ar_0, ar_2, arityPad, arityPad, arityPad)) [ 0 < ar_4 /\\ 2 <= ar_2 /\\ 0 < ar_1 /\\ 0 < ar_0 /\\ 0 < o111''' /\\ o111''' <= ar_4 + ar_0 ]", 0-3) = ?
S("create_FieldAccess_749(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(get_Inc_957(ar_3, ar_0, ar_2, arityPad, arityPad, arityPad)) [ 0 < ar_4 /\\ 2 <= ar_2 /\\ 0 < ar_1 /\\ 0 < ar_0 /\\ 0 < o111''' /\\ o111''' <= ar_4 + ar_0 ]", 0-4) = ?
S("create_FieldAccess_749(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(get_Inc_957(ar_3, ar_0, ar_2, arityPad, arityPad, arityPad)) [ 0 < ar_4 /\\ 2 <= ar_2 /\\ 0 < ar_1 /\\ 0 < ar_0 /\\ 0 < o111''' /\\ o111''' <= ar_4 + ar_0 ]", 0-5) = ?
S("main_Load_2(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(create_LE_84(ar_0 - 1, 1, ar_0, ar_1, arityPad, arityPad)) [ static'1 <= static''' + 1 /\\ 0 < o4''' /\\ 0 <= static''' /\\ static''' <= ar_2 + 2 /\\ o4''' = 1 /\\ 0 <= ar_2 /\\ 0 <= static'1 /\\ ar_0 - 1 = i6' ]", 0-0) = ar_0 + 1
S("main_Load_2(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(create_LE_84(ar_0 - 1, 1, ar_0, ar_1, arityPad, arityPad)) [ static'1 <= static''' + 1 /\\ 0 < o4''' /\\ 0 <= static''' /\\ static''' <= ar_2 + 2 /\\ o4''' = 1 /\\ 0 <= ar_2 /\\ 0 <= static'1 /\\ ar_0 - 1 = i6' ]", 0-1) = 1
S("main_Load_2(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(create_LE_84(ar_0 - 1, 1, ar_0, ar_1, arityPad, arityPad)) [ static'1 <= static''' + 1 /\\ 0 < o4''' /\\ 0 <= static''' /\\ static''' <= ar_2 + 2 /\\ o4''' = 1 /\\ 0 <= ar_2 /\\ 0 <= static'1 /\\ ar_0 - 1 = i6' ]", 0-2) = ar_0
S("main_Load_2(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(create_LE_84(ar_0 - 1, 1, ar_0, ar_1, arityPad, arityPad)) [ static'1 <= static''' + 1 /\\ 0 < o4''' /\\ 0 <= static''' /\\ static''' <= ar_2 + 2 /\\ o4''' = 1 /\\ 0 <= ar_2 /\\ 0 <= static'1 /\\ ar_0 - 1 = i6' ]", 0-3) = ar_1
S("main_Load_2(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(create_LE_84(ar_0 - 1, 1, ar_0, ar_1, arityPad, arityPad)) [ static'1 <= static''' + 1 /\\ 0 < o4''' /\\ 0 <= static''' /\\ static''' <= ar_2 + 2 /\\ o4''' = 1 /\\ 0 <= ar_2 /\\ 0 <= static'1 /\\ ar_0 - 1 = i6' ]", 0-4) = ?
S("main_Load_2(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(create_LE_84(ar_0 - 1, 1, ar_0, ar_1, arityPad, arityPad)) [ static'1 <= static''' + 1 /\\ 0 < o4''' /\\ 0 <= static''' /\\ static''' <= ar_2 + 2 /\\ o4''' = 1 /\\ 0 <= ar_2 /\\ 0 <= static'1 /\\ ar_0 - 1 = i6' ]", 0-5) = ?
S("create_LE_725(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(create_Duplicate_690(1, ar_0, ar_1, ar_2, ar_3, ar_4)) [ 0 < ar_0 /\\ 2 <= ar_3 /\\ 0 < ar_5 /\\ 0 < ar_2 /\\ 1 <= ar_0 /\\ 0 < ar_1 ]", 0-0) = 1
S("create_LE_725(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(create_Duplicate_690(1, ar_0, ar_1, ar_2, ar_3, ar_4)) [ 0 < ar_0 /\\ 2 <= ar_3 /\\ 0 < ar_5 /\\ 0 < ar_2 /\\ 1 <= ar_0 /\\ 0 < ar_1 ]", 0-1) = ar_0 + 1
S("create_LE_725(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(create_Duplicate_690(1, ar_0, ar_1, ar_2, ar_3, ar_4)) [ 0 < ar_0 /\\ 2 <= ar_3 /\\ 0 < ar_5 /\\ 0 < ar_2 /\\ 1 <= ar_0 /\\ 0 < ar_1 ]", 0-2) = 1
S("create_LE_725(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(create_Duplicate_690(1, ar_0, ar_1, ar_2, ar_3, ar_4)) [ 0 < ar_0 /\\ 2 <= ar_3 /\\ 0 < ar_5 /\\ 0 < ar_2 /\\ 1 <= ar_0 /\\ 0 < ar_1 ]", 0-3) = ?
S("create_LE_725(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(create_Duplicate_690(1, ar_0, ar_1, ar_2, ar_3, ar_4)) [ 0 < ar_0 /\\ 2 <= ar_3 /\\ 0 < ar_5 /\\ 0 < ar_2 /\\ 1 <= ar_0 /\\ 0 < ar_1 ]", 0-4) = ar_0
S("create_LE_725(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(create_Duplicate_690(1, ar_0, ar_1, ar_2, ar_3, ar_4)) [ 0 < ar_0 /\\ 2 <= ar_3 /\\ 0 < ar_5 /\\ 0 < ar_2 /\\ 1 <= ar_0 /\\ 0 < ar_1 ]", 0-5) = ar_1
S("create_Duplicate_690(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(create_LE_725(ar_1 - 1, ar_2, ar_0 + ar_3, ar_4, ar_5, ar_3)) [ o112''' = ar_0 + ar_3 /\\ 2 <= ar_4 /\\ 0 <= i151' /\\ 0 < ar_3 /\\ 0 < o112''' /\\ ar_1 - 1 = i151' /\\ 0 < ar_2 /\\ 0 < ar_0 /\\ 1 <= ar_1 ]", 0-0) = ar_0 + 1
S("create_Duplicate_690(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(create_LE_725(ar_1 - 1, ar_2, ar_0 + ar_3, ar_4, ar_5, ar_3)) [ o112''' = ar_0 + ar_3 /\\ 2 <= ar_4 /\\ 0 <= i151' /\\ 0 < ar_3 /\\ 0 < o112''' /\\ ar_1 - 1 = i151' /\\ 0 < ar_2 /\\ 0 < ar_0 /\\ 1 <= ar_1 ]", 0-1) = 1
S("create_Duplicate_690(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(create_LE_725(ar_1 - 1, ar_2, ar_0 + ar_3, ar_4, ar_5, ar_3)) [ o112''' = ar_0 + ar_3 /\\ 2 <= ar_4 /\\ 0 <= i151' /\\ 0 < ar_3 /\\ 0 < o112''' /\\ ar_1 - 1 = i151' /\\ 0 < ar_2 /\\ 0 < ar_0 /\\ 1 <= ar_1 ]", 0-2) = ?
S("create_Duplicate_690(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(create_LE_725(ar_1 - 1, ar_2, ar_0 + ar_3, ar_4, ar_5, ar_3)) [ o112''' = ar_0 + ar_3 /\\ 2 <= ar_4 /\\ 0 <= i151' /\\ 0 < ar_3 /\\ 0 < o112''' /\\ ar_1 - 1 = i151' /\\ 0 < ar_2 /\\ 0 < ar_0 /\\ 1 <= ar_1 ]", 0-3) = ar_0
S("create_Duplicate_690(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(create_LE_725(ar_1 - 1, ar_2, ar_0 + ar_3, ar_4, ar_5, ar_3)) [ o112''' = ar_0 + ar_3 /\\ 2 <= ar_4 /\\ 0 <= i151' /\\ 0 < ar_3 /\\ 0 < o112''' /\\ ar_1 - 1 = i151' /\\ 0 < ar_2 /\\ 0 < ar_0 /\\ 1 <= ar_1 ]", 0-4) = ar_1
S("create_Duplicate_690(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(create_LE_725(ar_1 - 1, ar_2, ar_0 + ar_3, ar_4, ar_5, ar_3)) [ o112''' = ar_0 + ar_3 /\\ 2 <= ar_4 /\\ 0 <= i151' /\\ 0 < ar_3 /\\ 0 < o112''' /\\ ar_1 - 1 = i151' /\\ 0 < ar_2 /\\ 0 < ar_0 /\\ 1 <= ar_1 ]", 0-5) = ?
S("get_Inc_957(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(get_FieldAccess_993(ar_1, ar_0 - 1, ar_2, o302', arityPad, arityPad)) [ 0 < i232 /\\ 2 <= ar_2 /\\ 0 < ar_1 /\\ 0 < o302' /\\ 1 <= i232 /\\ o302' <= ar_1 /\\ ar_0 - 1 = i232 ]", 0-0) = ?
S("get_Inc_957(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(get_FieldAccess_993(ar_1, ar_0 - 1, ar_2, o302', arityPad, arityPad)) [ 0 < i232 /\\ 2 <= ar_2 /\\ 0 < ar_1 /\\ 0 < o302' /\\ 1 <= i232 /\\ o302' <= ar_1 /\\ ar_0 - 1 = i232 ]", 0-1) = ar_1
S("get_Inc_957(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(get_FieldAccess_993(ar_1, ar_0 - 1, ar_2, o302', arityPad, arityPad)) [ 0 < i232 /\\ 2 <= ar_2 /\\ 0 < ar_1 /\\ 0 < o302' /\\ 1 <= i232 /\\ o302' <= ar_1 /\\ ar_0 - 1 = i232 ]", 0-2) = ar_0
S("get_Inc_957(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(get_FieldAccess_993(ar_1, ar_0 - 1, ar_2, o302', arityPad, arityPad)) [ 0 < i232 /\\ 2 <= ar_2 /\\ 0 < ar_1 /\\ 0 < o302' /\\ 1 <= i232 /\\ o302' <= ar_1 /\\ ar_0 - 1 = i232 ]", 0-3) = ?
S("get_Inc_957(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(get_FieldAccess_993(ar_1, ar_0 - 1, ar_2, o302', arityPad, arityPad)) [ 0 < i232 /\\ 2 <= ar_2 /\\ 0 < ar_1 /\\ 0 < o302' /\\ 1 <= i232 /\\ o302' <= ar_1 /\\ ar_0 - 1 = i232 ]", 0-4) = ?
S("get_Inc_957(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(get_FieldAccess_993(ar_1, ar_0 - 1, ar_2, o302', arityPad, arityPad)) [ 0 < i232 /\\ 2 <= ar_2 /\\ 0 < ar_1 /\\ 0 < o302' /\\ 1 <= i232 /\\ o302' <= ar_1 /\\ ar_0 - 1 = i232 ]", 0-5) = ?
S("create_LE_725(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(create_FieldAccess_749(ar_2, ar_1, ar_3, ar_4, ar_5, arityPad)) [ 0 < ar_1 /\\ 2 <= ar_3 /\\ 0 < ar_5 /\\ 0 < ar_2 /\\ ar_0 = 0 ]", 0-0) = ?
S("create_LE_725(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(create_FieldAccess_749(ar_2, ar_1, ar_3, ar_4, ar_5, arityPad)) [ 0 < ar_1 /\\ 2 <= ar_3 /\\ 0 < ar_5 /\\ 0 < ar_2 /\\ ar_0 = 0 ]", 0-1) = 1
S("create_LE_725(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(create_FieldAccess_749(ar_2, ar_1, ar_3, ar_4, ar_5, arityPad)) [ 0 < ar_1 /\\ 2 <= ar_3 /\\ 0 < ar_5 /\\ 0 < ar_2 /\\ ar_0 = 0 ]", 0-2) = ar_0
S("create_LE_725(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(create_FieldAccess_749(ar_2, ar_1, ar_3, ar_4, ar_5, arityPad)) [ 0 < ar_1 /\\ 2 <= ar_3 /\\ 0 < ar_5 /\\ 0 < ar_2 /\\ ar_0 = 0 ]", 0-3) = ar_1
S("create_LE_725(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(create_FieldAccess_749(ar_2, ar_1, ar_3, ar_4, ar_5, arityPad)) [ 0 < ar_1 /\\ 2 <= ar_3 /\\ 0 < ar_5 /\\ 0 < ar_2 /\\ ar_0 = 0 ]", 0-4) = ?
S("create_LE_725(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(create_FieldAccess_749(ar_2, ar_1, ar_3, ar_4, ar_5, arityPad)) [ 0 < ar_1 /\\ 2 <= ar_3 /\\ 0 < ar_5 /\\ 0 < ar_2 /\\ ar_0 = 0 ]", 0-5) = ?
S("create_FieldAccess_749(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(get_Inc_957(ar_3, o112'1, ar_2, arityPad, arityPad, arityPad)) [ 0 < ar_4 /\\ 0 < ar_1 /\\ 0 < ar_0 /\\ 0 < o112'1 /\\ 2 <= ar_2 /\\ ar_1 <= ar_1 + ar_0 /\\ o112'1 <= 2*ar_0 ]", 0-0) = ar_1
S("create_FieldAccess_749(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(get_Inc_957(ar_3, o112'1, ar_2, arityPad, arityPad, arityPad)) [ 0 < ar_4 /\\ 0 < ar_1 /\\ 0 < ar_0 /\\ 0 < o112'1 /\\ 2 <= ar_2 /\\ ar_1 <= ar_1 + ar_0 /\\ o112'1 <= 2*ar_0 ]", 0-1) = ?
S("create_FieldAccess_749(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(get_Inc_957(ar_3, o112'1, ar_2, arityPad, arityPad, arityPad)) [ 0 < ar_4 /\\ 0 < ar_1 /\\ 0 < ar_0 /\\ 0 < o112'1 /\\ 2 <= ar_2 /\\ ar_1 <= ar_1 + ar_0 /\\ o112'1 <= 2*ar_0 ]", 0-2) = ar_0
S("create_FieldAccess_749(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(get_Inc_957(ar_3, o112'1, ar_2, arityPad, arityPad, arityPad)) [ 0 < ar_4 /\\ 0 < ar_1 /\\ 0 < ar_0 /\\ 0 < o112'1 /\\ 2 <= ar_2 /\\ ar_1 <= ar_1 + ar_0 /\\ o112'1 <= 2*ar_0 ]", 0-3) = ?
S("create_FieldAccess_749(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(get_Inc_957(ar_3, o112'1, ar_2, arityPad, arityPad, arityPad)) [ 0 < ar_4 /\\ 0 < ar_1 /\\ 0 < ar_0 /\\ 0 < o112'1 /\\ 2 <= ar_2 /\\ ar_1 <= ar_1 + ar_0 /\\ o112'1 <= 2*ar_0 ]", 0-4) = ?
S("create_FieldAccess_749(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(get_Inc_957(ar_3, o112'1, ar_2, arityPad, arityPad, arityPad)) [ 0 < ar_4 /\\ 0 < ar_1 /\\ 0 < ar_0 /\\ 0 < o112'1 /\\ 2 <= ar_2 /\\ ar_1 <= ar_1 + ar_0 /\\ o112'1 <= 2*ar_0 ]", 0-5) = ?
orients the transitions
create_LE_725(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(create_Duplicate_690(1, ar_0, ar_1, ar_2, ar_3, ar_4)) [ 0 < ar_0 /\ 2 <= ar_3 /\ 0 < ar_5 /\ 0 < ar_2 /\ 1 <= ar_0 /\ 0 < ar_1 ]
create_Duplicate_690(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(create_LE_725(ar_1 - 1, ar_2, ar_0 + ar_3, ar_4, ar_5, ar_3)) [ o112''' = ar_0 + ar_3 /\ 2 <= ar_4 /\ 0 <= i151' /\ 0 < ar_3 /\ 0 < o112''' /\ ar_1 - 1 = i151' /\ 0 < ar_2 /\ 0 < ar_0 /\ 1 <= ar_1 ]
weakly and the transitions
create_LE_725(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(create_Duplicate_690(1, ar_0, ar_1, ar_2, ar_3, ar_4)) [ 0 < ar_0 /\ 2 <= ar_3 /\ 0 < ar_5 /\ 0 < ar_2 /\ 1 <= ar_0 /\ 0 < ar_1 ]
create_Duplicate_690(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(create_LE_725(ar_1 - 1, ar_2, ar_0 + ar_3, ar_4, ar_5, ar_3)) [ o112''' = ar_0 + ar_3 /\ 2 <= ar_4 /\ 0 <= i151' /\ 0 < ar_3 /\ 0 < o112''' /\ ar_1 - 1 = i151' /\ 0 < ar_2 /\ 0 < ar_0 /\ 1 <= ar_1 ]
strictly and produces the following problem:
5: T:
(Comp: 2, Cost: 8) create_FieldAccess_749(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(get_Inc_957(ar_3, o112'1, ar_2, arityPad, arityPad, arityPad)) [ 0 < ar_4 /\ 0 < ar_1 /\ 0 < ar_0 /\ 0 < o112'1 /\ 2 <= ar_2 /\ ar_1 <= ar_1 + ar_0 /\ o112'1 <= 2*ar_0 ]
(Comp: 2, Cost: 4) create_LE_725(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(create_FieldAccess_749(ar_2, ar_1, ar_3, ar_4, ar_5, arityPad)) [ 0 < ar_1 /\ 2 <= ar_3 /\ 0 < ar_5 /\ 0 < ar_2 /\ ar_0 = 0 ]
(Comp: 2*ar_1, Cost: 4) get_Inc_957(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(get_FieldAccess_993(ar_1, ar_0 - 1, ar_2, o302', arityPad, arityPad)) [ 0 < i232 /\ 2 <= ar_2 /\ 0 < ar_1 /\ 0 < o302' /\ 1 <= i232 /\ o302' <= ar_1 /\ ar_0 - 1 = i232 ]
(Comp: 2*ar_0 + 2, Cost: 13) create_Duplicate_690(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(create_LE_725(ar_1 - 1, ar_2, ar_0 + ar_3, ar_4, ar_5, ar_3)) [ o112''' = ar_0 + ar_3 /\ 2 <= ar_4 /\ 0 <= i151' /\ 0 < ar_3 /\ 0 < o112''' /\ ar_1 - 1 = i151' /\ 0 < ar_2 /\ 0 < ar_0 /\ 1 <= ar_1 ]
(Comp: 2*ar_0 + 2, Cost: 2) create_LE_725(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(create_Duplicate_690(1, ar_0, ar_1, ar_2, ar_3, ar_4)) [ 0 < ar_0 /\ 2 <= ar_3 /\ 0 < ar_5 /\ 0 < ar_2 /\ 1 <= ar_0 /\ 0 < ar_1 ]
(Comp: 1, Cost: 32) main_Load_2(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(create_LE_84(ar_0 - 1, 1, ar_0, ar_1, arityPad, arityPad)) [ static'1 <= static''' + 1 /\ 0 < o4''' /\ 0 <= static''' /\ static''' <= ar_2 + 2 /\ o4''' = 1 /\ 0 <= ar_2 /\ 0 <= static'1 /\ ar_0 - 1 = i6' ]
(Comp: 2, Cost: 8) create_FieldAccess_749(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(get_Inc_957(ar_3, ar_0, ar_2, arityPad, arityPad, arityPad)) [ 0 < ar_4 /\ 2 <= ar_2 /\ 0 < ar_1 /\ 0 < ar_0 /\ 0 < o111''' /\ o111''' <= ar_4 + ar_0 ]
(Comp: 2*ar_1, Cost: 3) get_FieldAccess_993(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(get_Inc_957(ar_1, ar_0, ar_2, arityPad, arityPad, arityPad)) [ 0 < ar_0 /\ 2 <= ar_2 /\ 1 <= ar_1 /\ 0 < ar_3 ]
(Comp: 1, Cost: 2) create_LE_84(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(create_Duplicate_690(1, ar_0, ar_1, ar_1, ar_2, ar_3)) [ 2 <= ar_2 /\ 1 <= ar_0 /\ 0 < ar_1 /\ 0 < ar_0 ]
(Comp: 1, Cost: 12) create_LE_84(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(get_Inc_570(ar_3, ar_1, arityPad, arityPad, arityPad, arityPad)) [ 0 < ar_1 /\ ar_0 <= 0 /\ ar_1 <= 2*ar_1 ]
(Comp: 2*ar_1, Cost: 7) get_Inc_570(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(get_Inc_570(ar_0 - 1, ar_1, arityPad, arityPad, arityPad, arityPad)) [ 0 < i120 /\ 0 < ar_1 /\ 1 <= i120 /\ ar_0 - 1 = i120 ]
(Comp: 2*ar_1, Cost: 3) get_FieldAccess_993(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(get_Inc_957(ar_1, ar_3, ar_2, arityPad, arityPad, arityPad)) [ 1 <= ar_1 /\ 2 <= ar_2 /\ 0 < ar_0 /\ 0 < ar_3 ]
(Comp: 1, Cost: 0) koat_start(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(main_Load_2(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5)) [ 0 <= 0 ]
start location: koat_start
leaf cost: 0

Complexity upper bound 34*ar_1 + 30*ar_0 + 116

Time: 0.497 sec (SMT: 0.380 sec)

(0) Obligation:

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

(2) Obligation:

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

(12) Obligation:

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

(14) Obligation:

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

(16) Obligation:

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

(18) Obligation:

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

(20) Obligation:

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

(22) Obligation:

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

(24) Obligation:

(25) CESProof (EQUIVALENT transformation)

(26) BOUNDS(CONSTANT, max(31 + 15 * #0, max(39 + 7 * #1, 46) + max(-15 + 15 * #0, 15), 61))

(27) TerminationGraphToComplexityProof (BOTH CONCRETE BOUNDS(ID, ADD(10)) transformation)

(28) Obligation:

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

(30) Obligation:

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

(32) Obligation:

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

(34) Obligation:

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

(36) Obligation:

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

(38) Obligation:

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

(40) Obligation:

(41) koat Proof (EQUIVALENT transformation)

(42) BOUNDS(CONSTANT, 116 + 30 * |#0| + 34 * |#1|)