time complexity proof of /tmp/tmpwiCBiB/costa09-example

The time complexity of the given JBC problem could be proven to be BOUNDS(CONSTANT, 126270).

0 JBC problem

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

↳2 JBCTerminationGraph

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

↳4 JBCComplexityEdges

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

    ↳6 WeightedIntTrs

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

    ↳16 WeightedIntTrs

        ↳17 StraightLineCodeCompressionProof (BOTH CONCRETE BOUNDS(ID, ID), 90 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 TerminationGraphToComplexityProof (BOTH CONCRETE BOUNDS(ID, ADD(5)), 0 ms)

↳26 JBCComplexityEdges

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

    ↳28 WeightedIntTrs

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

    ↳30 WeightedIntTrs

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

    ↳32 WeightedIntTrs

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

    ↳34 WeightedIntTrs

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

    ↳36 WeightedIntTrs

    ↳37 koat Proof (⇔, 254 ms)

    ↳38 BOUNDS(CONSTANT, 126265)

(0) Obligation:

Need to prove time_complexity of the following program:

package example_1;

public class A {

	int incr(int i) {
		return i=i+1;
	}
}


package example_1;

public class B extends A {
	int incr(int i) {
		return i = i+2;
	}
}



package example_1;

public class C extends B {
	int incr(int i) {
		return i=i+3;
	}
}


package example_1;

public class Test {

	public int add(int n,A o){
		int res=0;
		int i=0;
		while (i<=n){
			res=res+i;
			i=o.incr(i);
		}
		return res;
	}

	public static void main() {
		int test = 1000;
		Test testClass = new Test();
		A a = new A();
		int result1 = testClass.add(test,a);
		a = new B();
		int result2 = testClass.add(test,a);
		a = new C();
		int result3 = testClass.add(test,a);
		// System.out.println("Result: "+result1 + result2 + result3);
	}
}

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

Constructed TerminationGraph.

(2) Obligation:

Termination Graph based on JBC Program:
example_1.Test.main()V: Graph of 172 nodes with 3 SCCs.

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

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

(4) Obligation:

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

Used field analysis yielded the following read fields:

Considered paths: nonterm paths and paths from start to sinks

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

Transformed 169 jbc graph edges to a weighted ITS with 169 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 169 rules
Start term: main_ConstantStackPush_2(env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_ConstantStackPush_2(env, static) -{0,0}> main_ConstantStackPush_4(env, static) :|: 0 >= 0
main_ConstantStackPush_4(env, static) -{0,0}> langle_clinit_rangle_ConstantStackPush_6(env, static) :|: 0 >= 0
langle_clinit_rangle_ConstantStackPush_6(env, static) -{1,1}> langle_clinit_rangle_ArrayCreate_13(iconst_0, env, static) :|: iconst_0 = 0
langle_clinit_rangle_ArrayCreate_13(iconst_0, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_16(a2, iconst_0, env, static) :|: a2 = 2 && iconst_0 = 0 && 0 < a2
langle_clinit_rangle_FieldAccess_16(a2, iconst_0, env, static) -{1,1}> langle_clinit_rangle_New_17(env, static') :|: 0 <= a2 && iconst_0 = 0 && static' <= static + a2 && 0 <= static && 0 < a2
langle_clinit_rangle_New_17(env, static) -{0,0}> langle_clinit_rangle_New_18(env, static) :|: 0 >= 0
langle_clinit_rangle_New_18(env, static) -{0,0}> langle_clinit_rangle_New_20(env, static) :|: 0 <= static
langle_clinit_rangle_New_20(env, static) -{1,1}> langle_clinit_rangle_Duplicate_21(o2, env, static) :|: 0 < o2 && o2 = 1
langle_clinit_rangle_Duplicate_21(o2, env, static) -{1,1}> langle_clinit_rangle_ConstantStackPush_23(o2, env, static) :|: 0 < o2
langle_clinit_rangle_ConstantStackPush_23(o2, env, static) -{1,1}> langle_clinit_rangle_InvokeMethod_25(o2, NULL, env, static) :|: NULL = 0 && 0 < o2
langle_clinit_rangle_InvokeMethod_25(o2, NULL, env, static) -{1,1}> langle_init_rangle_Load_27(o2, env, static) :|: NULL = 0 && 0 < o2
langle_init_rangle_Load_27(o2, env, static) -{1,1}> langle_init_rangle_InvokeMethod_29(o2, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_29(o2, env, static) -{1,1}> langle_init_rangle_Load_31(o2, env, static) :|: 0 < o2
langle_init_rangle_Load_31(o2, env, static) -{1,1}> langle_init_rangle_InvokeMethod_33(o2, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_33(o2, env, static) -{1,1}> langle_init_rangle_Return_36(o2, env, static) :|: 0 < o2
langle_init_rangle_Return_36(o2, env, static) -{1,1}> langle_init_rangle_Return_38(o2, env, static) :|: 0 < o2
langle_init_rangle_Return_38(o2, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_39(o2, env, static) :|: 0 < o2
langle_clinit_rangle_FieldAccess_39(o2, env, static) -{1,1}> langle_clinit_rangle_Return_40(env, static') :|: 0 < o2 && 0 <= o2 && 0 <= static && static' <= static + o2
langle_clinit_rangle_Return_40(env, static) -{1,1}> main_ConstantStackPush_48(env, static) :|: 0 >= 0
main_ConstantStackPush_48(env, static) -{0,0}> main_ConstantStackPush_49(env, static) :|: 0 >= 0
main_ConstantStackPush_49(env, static) -{0,0}> main_ConstantStackPush_52(env, static) :|: 0 <= static
main_ConstantStackPush_52(env, static) -{0,0}> main_ConstantStackPush_53(env, static) :|: 0 >= 0
main_ConstantStackPush_53(env, static) -{0,0}> main_ConstantStackPush_55(env, static) :|: 0 >= 0
main_ConstantStackPush_55(env, static) -{1,1}> main_Store_57(iconst_1000, env, static) :|: iconst_1000 = 1000
main_Store_57(iconst_1000, env, static) -{1,1}> main_New_59(iconst_1000, env, static) :|: iconst_1000 = 1000
main_New_59(iconst_1000, env, static) -{1,1}> main_Duplicate_61(o4, iconst_1000, env, static) :|: o4 = 1 && 0 < o4 && iconst_1000 = 1000
main_Duplicate_61(o4, iconst_1000, env, static) -{1,1}> main_InvokeMethod_63(o4, iconst_1000, env, static) :|: 0 < o4 && iconst_1000 = 1000
main_InvokeMethod_63(o4, iconst_1000, env, static) -{1,1}> langle_init_rangle_Load_65(o4, iconst_1000, env, static) :|: 0 < o4 && iconst_1000 = 1000
langle_init_rangle_Load_65(o4, iconst_1000, env, static) -{1,1}> langle_init_rangle_InvokeMethod_68(o4, iconst_1000, env, static) :|: 0 < o4 && iconst_1000 = 1000
langle_init_rangle_InvokeMethod_68(o4, iconst_1000, env, static) -{1,1}> langle_init_rangle_Return_70(o4, iconst_1000, env, static) :|: 0 < o4 && iconst_1000 = 1000
langle_init_rangle_Return_70(o4, iconst_1000, env, static) -{1,1}> main_Store_72(o4, iconst_1000, env, static) :|: 0 < o4 && iconst_1000 = 1000
main_Store_72(o4, iconst_1000, env, static) -{1,1}> main_New_75(iconst_1000, o4, env, static) :|: 0 < o4 && iconst_1000 = 1000
main_New_75(iconst_1000, o4, env, static) -{0,0}> main_New_77(iconst_1000, o4, env, static) :|: 0 < o4 && iconst_1000 = 1000
main_New_77(iconst_1000, o4, env, static) -{1,1}> main_Duplicate_79(o6, iconst_1000, o4, env, static) :|: 0 < o6 && 0 < o4 && o6 = 1 && iconst_1000 = 1000
main_Duplicate_79(o6, iconst_1000, o4, env, static) -{1,1}> main_InvokeMethod_80(o6, iconst_1000, o4, env, static) :|: 0 < o6 && 0 < o4 && iconst_1000 = 1000
main_InvokeMethod_80(o6, iconst_1000, o4, env, static) -{1,1}> langle_init_rangle_Load_82(o6, iconst_1000, o4, env, static) :|: 0 < o6 && 0 < o4 && iconst_1000 = 1000
langle_init_rangle_Load_82(o6, iconst_1000, o4, env, static) -{1,1}> langle_init_rangle_InvokeMethod_84(o6, iconst_1000, o4, env, static) :|: 0 < o6 && 0 < o4 && iconst_1000 = 1000
langle_init_rangle_InvokeMethod_84(o6, iconst_1000, o4, env, static) -{1,1}> langle_init_rangle_Return_86(o6, iconst_1000, o4, env, static) :|: 0 < o6 && 0 < o4 && iconst_1000 = 1000
langle_init_rangle_Return_86(o6, iconst_1000, o4, env, static) -{1,1}> main_Store_89(o6, iconst_1000, o4, env, static) :|: 0 < o6 && 0 < o4 && iconst_1000 = 1000
main_Store_89(o6, iconst_1000, o4, env, static) -{1,1}> main_Load_91(iconst_1000, o4, o6, env, static) :|: 0 < o6 && 0 < o4 && iconst_1000 = 1000
main_Load_91(iconst_1000, o4, o6, env, static) -{1,1}> main_Load_93(o4, iconst_1000, o6, env, static) :|: 0 < o6 && 0 < o4 && iconst_1000 = 1000
main_Load_93(o4, iconst_1000, o6, env, static) -{1,1}> main_Load_94(o4, iconst_1000, o6, env, static) :|: 0 < o6 && 0 < o4 && iconst_1000 = 1000
main_Load_94(o4, iconst_1000, o6, env, static) -{1,1}> main_InvokeMethod_95(o4, iconst_1000, o6, env, static) :|: 0 < o6 && 0 < o4 && iconst_1000 = 1000
main_InvokeMethod_95(o4, iconst_1000, o6, env, static) -{1,1}> add_ConstantStackPush_96(iconst_1000, o6, o4, env, static) :|: 0 < o6 && 0 < o4 && iconst_1000 = 1000
add_ConstantStackPush_96(iconst_1000, o6, o4, env, static) -{1,1}> add_Store_97(iconst_0, iconst_1000, o6, o4, env, static) :|: 0 < o6 && 0 < o4 && iconst_0 = 0 && iconst_1000 = 1000
add_Store_97(iconst_0, iconst_1000, o6, o4, env, static) -{1,1}> add_ConstantStackPush_98(iconst_1000, o6, iconst_0, o4, env, static) :|: 0 < o6 && 0 < o4 && iconst_0 = 0 && iconst_1000 = 1000
add_ConstantStackPush_98(iconst_1000, o6, iconst_0, o4, env, static) -{1,1}> add_Store_99(iconst_0, iconst_1000, o6, o4, env, static) :|: 0 < o6 && 0 < o4 && iconst_0 = 0 && iconst_1000 = 1000
add_Store_99(iconst_0, iconst_1000, o6, o4, env, static) -{1,1}> add_Load_100(iconst_1000, o6, iconst_0, o4, env, static) :|: 0 < o6 && 0 < o4 && iconst_0 = 0 && iconst_1000 = 1000
add_Load_100(iconst_1000, o6, iconst_0, o4, env, static) -{0,0}> add_Load_156(iconst_1000, o6, iconst_0, iconst_0, o4, env, static) :|: 0 <= iconst_0 && 0 < o6 && 0 < o4 && iconst_0 <= 1 && iconst_0 = 0 && iconst_1000 = 1000
add_Load_156(iconst_1000, o10, iconst_0, i1, o11, env, static) -{0,0}> add_Load_228(iconst_1000, o10, iconst_0, i1, o11, env, static) :|: 0 <= iconst_0 && 0 <= i1 && i1 <= 1 && iconst_0 <= 1 && iconst_0 = 0 && 0 < o11 && iconst_1000 = 1000 && 0 < o10 && i1 <= 2
add_Load_228(iconst_1000, o20, i4, i5, o21, env, static) -{0,0}> add_Load_283(iconst_1000, o20, i4, i5, o21, env, static) :|: 0 < o20 && i5 <= 2 && 0 <= i4 && 0 < o21 && iconst_1000 = 1000 && 0 <= i5 && i4 <= 1
add_Load_283(iconst_1000, o30, i10, i11, o31, env, static) -{1,1}> add_Load_286(i11, iconst_1000, o30, i10, o31, env, static) :|: 0 <= i10 && 0 < o30 && 0 <= i11 && 0 < o31 && iconst_1000 = 1000
add_Load_286(i11, iconst_1000, o30, i10, o31, env, static) -{1,1}> add_GT_299(i11, iconst_1000, o30, i10, o31, env, static) :|: 0 <= i10 && 0 < o30 && 0 <= i11 && 0 < o31 && iconst_1000 = 1000
add_GT_299(i18, iconst_1000, o30, i10, o31, env, static) -{0,0}> add_GT_304(i18, iconst_1000, o30, i10, o31, env, static) :|: 0 <= i10 && 0 <= i18 && i18 <= 1000 && 0 < o30 && 0 < o31 && iconst_1000 = 1000
add_GT_299(i19, iconst_1000, o30, i10, o31, env, static) -{0,0}> add_GT_305(i19, iconst_1000, o30, i10, o31, env, static) :|: 0 <= i10 && 0 < o30 && 0 < o31 && 1001 <= i19 && iconst_1000 = 1000 && 0 <= i19
add_GT_304(i18, iconst_1000, o30, i10, o31, env, static) -{1,1}> add_Load_309(iconst_1000, o30, i10, i18, o31, env, static) :|: 0 <= i10 && 0 <= i18 && i18 <= 1000 && 0 < o30 && i18 <= iconst_1000 && 0 < o31 && iconst_1000 = 1000
add_GT_305(i19, iconst_1000, o30, i10, o31, env, static) -{1,1}> add_Load_317(i10, iconst_1000, o31, env, static) :|: 0 <= i10 && 0 < o30 && 0 < o31 && 1001 <= i19 && iconst_1000 < i19 && iconst_1000 = 1000
add_Load_309(iconst_1000, o30, i10, i18, o31, env, static) -{1,1}> add_Load_319(i10, iconst_1000, o30, i18, o31, env, static) :|: 0 <= i10 && 0 <= i18 && i18 <= 1000 && 0 < o30 && 0 < o31 && iconst_1000 = 1000
add_Load_317(i10, iconst_1000, o31, env, static) -{1,1}> add_Return_321(i10, iconst_1000, o31, env, static) :|: 0 <= i10 && 0 < o31 && iconst_1000 = 1000
add_Load_319(i10, iconst_1000, o30, i18, o31, env, static) -{1,1}> add_IntArithmetic_323(i10, i18, iconst_1000, o30, o31, env, static) :|: 0 <= i10 && 0 <= i18 && i18 <= 1000 && 0 < o30 && 0 < o31 && iconst_1000 = 1000
add_Return_321(i10, iconst_1000, o31, env, static) -{1,1}> main_Store_325(i10, iconst_1000, o31, env, static) :|: 0 <= i10 && 0 < o31 && iconst_1000 = 1000
add_IntArithmetic_323(i10, i18, iconst_1000, o30, o31, env, static) -{1,1}> add_Store_328(i20, iconst_1000, o30, i18, o31, env, static) :|: 0 <= i10 && 0 <= i18 && i18 <= 1000 && 0 <= i20 && 0 < o30 && 0 < o31 && iconst_1000 = 1000 && i10 + i18 = i20
main_Store_325(i10, iconst_1000, o31, env, static) -{1,1}> main_New_331(iconst_1000, o31, env, static) :|: 0 <= i10 && 0 < o31 && iconst_1000 = 1000
add_Store_328(i20, iconst_1000, o30, i18, o31, env, static) -{1,1}> add_Load_332(iconst_1000, o30, i20, i18, o31, env, static) :|: 0 <= i18 && 0 <= i20 && i18 <= 1000 && 0 < o30 && 0 < o31 && iconst_1000 = 1000
main_New_331(iconst_1000, o31, env, static) -{0,0}> main_New_333(iconst_1000, o31, env, static) :|: 0 < o31 && iconst_1000 = 1000
add_Load_332(iconst_1000, o30, i20, i18, o31, env, static) -{1,1}> add_Load_334(o30, iconst_1000, i20, i18, o31, env, static) :|: 0 <= i18 && 0 <= i20 && i18 <= 1000 && 0 < o30 && 0 < o31 && iconst_1000 = 1000
main_New_333(iconst_1000, o31, env, static) -{1,1}> main_Duplicate_335(o37, iconst_1000, o31, env, static) :|: 0 < o37 && 0 < o31 && o37 = 1 && iconst_1000 = 1000
add_Load_334(o30, iconst_1000, i20, i18, o31, env, static) -{1,1}> add_InvokeMethod_336(o30, i18, iconst_1000, i20, o31, env, static) :|: 0 <= i18 && 0 <= i20 && i18 <= 1000 && 0 < o30 && 0 < o31 && iconst_1000 = 1000
main_Duplicate_335(o37, iconst_1000, o31, env, static) -{1,1}> main_InvokeMethod_337(o37, iconst_1000, o31, env, static) :|: 0 < o37 && 0 < o31 && iconst_1000 = 1000
add_InvokeMethod_336(o30, i18, iconst_1000, i20, o31, env, static) -{1,1}> incr_Load_338(i18, iconst_1000, o30, i20, o31, env, static) :|: 0 <= i18 && i18 <= 1000 && 0 <= i20 && 0 < o30 && 0 < o31 && iconst_1000 = 1000
main_InvokeMethod_337(o37, iconst_1000, o31, env, static) -{1,1}> langle_init_rangle_Load_339(o37, iconst_1000, o31, env, static) :|: 0 < o37 && 0 < o31 && iconst_1000 = 1000
incr_Load_338(i18, iconst_1000, o30, i20, o31, env, static) -{1,1}> incr_ConstantStackPush_340(i18, iconst_1000, o30, i20, o31, env, static) :|: 0 <= i18 && i18 <= 1000 && 0 <= i20 && 0 < o30 && 0 < o31 && iconst_1000 = 1000
langle_init_rangle_Load_339(o37, iconst_1000, o31, env, static) -{1,1}> langle_init_rangle_InvokeMethod_341(o37, iconst_1000, o31, env, static) :|: 0 < o37 && 0 < o31 && iconst_1000 = 1000
incr_ConstantStackPush_340(i18, iconst_1000, o30, i20, o31, env, static) -{1,1}> incr_IntArithmetic_343(i18, iconst_1, iconst_1000, o30, i20, o31, env, static) :|: 0 <= i18 && i18 <= 1000 && 0 <= i20 && 0 < o30 && 0 < o31 && iconst_1 = 1 && iconst_1000 = 1000
langle_init_rangle_InvokeMethod_341(o37, iconst_1000, o31, env, static) -{1,1}> langle_init_rangle_Load_344(o37, iconst_1000, o31, env, static) :|: 0 < o37 && 0 < o31 && iconst_1000 = 1000
incr_IntArithmetic_343(i18, iconst_1, iconst_1000, o30, i20, o31, env, static) -{1,1}> incr_Duplicate_346(i21, iconst_1000, o30, i20, o31, env, static) :|: 1 <= i21 && 0 <= i18 && i18 <= 1000 && 0 <= i20 && 0 < o30 && 0 < o31 && i21 <= 1001 && iconst_1 = 1 && i18 + iconst_1 = i21 && iconst_1000 = 1000
langle_init_rangle_Load_344(o37, iconst_1000, o31, env, static) -{1,1}> langle_init_rangle_InvokeMethod_351(o37, iconst_1000, o31, env, static) :|: 0 < o37 && 0 < o31 && iconst_1000 = 1000
incr_Duplicate_346(i21, iconst_1000, o30, i20, o31, env, static) -{1,1}> incr_Store_348(i21, iconst_1000, o30, i20, o31, env, static) :|: 1 <= i21 && 0 <= i20 && 0 < o30 && 0 < o31 && i21 <= 1001 && iconst_1000 = 1000
incr_Store_348(i21, iconst_1000, o30, i20, o31, env, static) -{1,1}> incr_Return_353(i21, iconst_1000, o30, i20, o31, env, static) :|: 1 <= i21 && 0 <= i20 && 0 < o30 && 0 < o31 && i21 <= 1001 && iconst_1000 = 1000
langle_init_rangle_InvokeMethod_351(o37, iconst_1000, o31, env, static) -{1,1}> langle_init_rangle_Return_357(o37, iconst_1000, o31, env, static) :|: 0 < o37 && 0 < o31 && iconst_1000 = 1000
incr_Return_353(i21, iconst_1000, o30, i20, o31, env, static) -{1,1}> add_Store_359(i21, iconst_1000, o30, i20, o31, env, static) :|: 1 <= i21 && 0 <= i20 && 0 < o30 && 0 < o31 && i21 <= 1001 && iconst_1000 = 1000
langle_init_rangle_Return_357(o37, iconst_1000, o31, env, static) -{1,1}> langle_init_rangle_Return_361(o37, iconst_1000, o31, env, static) :|: 0 < o37 && 0 < o31 && iconst_1000 = 1000
add_Store_359(i21, iconst_1000, o30, i20, o31, env, static) -{1,1}> add_JMP_363(iconst_1000, o30, i20, i21, o31, env, static) :|: 1 <= i21 && 0 <= i20 && 0 < o30 && 0 < o31 && i21 <= 1001 && iconst_1000 = 1000
langle_init_rangle_Return_361(o37, iconst_1000, o31, env, static) -{1,1}> main_Store_365(o37, iconst_1000, o31, env, static) :|: 0 < o37 && 0 < o31 && iconst_1000 = 1000
add_JMP_363(iconst_1000, o30, i20, i21, o31, env, static) -{1,1}> add_Load_370(iconst_1000, o30, i20, i21, o31, env, static) :|: 1 <= i21 && 0 <= i20 && 0 < o30 && 0 < o31 && i21 <= 1001 && iconst_1000 = 1000
main_Store_365(o37, iconst_1000, o31, env, static) -{1,1}> main_Load_372(iconst_1000, o31, o37, env, static) :|: 0 < o37 && 0 < o31 && iconst_1000 = 1000
add_Load_370(iconst_1000, o30, i20, i21, o31, env, static) -{0,0}> add_Load_283(iconst_1000, o30, i20, i21, o31, env, static) :|: 1 <= i21 && 0 <= i20 && 0 < o30 && 0 <= i21 && 0 < o31 && i21 <= 1001 && iconst_1000 = 1000
main_Load_372(iconst_1000, o31, o37, env, static) -{1,1}> main_Load_373(o31, iconst_1000, o37, env, static) :|: 0 < o37 && 0 < o31 && iconst_1000 = 1000
main_Load_373(o31, iconst_1000, o37, env, static) -{1,1}> main_Load_374(o31, iconst_1000, o37, env, static) :|: 0 < o37 && 0 < o31 && iconst_1000 = 1000
main_Load_374(o31, iconst_1000, o37, env, static) -{1,1}> main_InvokeMethod_375(o31, iconst_1000, o37, env, static) :|: 0 < o37 && 0 < o31 && iconst_1000 = 1000
main_InvokeMethod_375(o31, iconst_1000, o37, env, static) -{1,1}> add_ConstantStackPush_376(iconst_1000, o37, o31, env, static) :|: 0 < o37 && 0 < o31 && iconst_1000 = 1000
add_ConstantStackPush_376(iconst_1000, o37, o31, env, static) -{1,1}> add_Store_378(iconst_0, iconst_1000, o37, o31, env, static) :|: 0 < o37 && 0 < o31 && iconst_0 = 0 && iconst_1000 = 1000
add_Store_378(iconst_0, iconst_1000, o37, o31, env, static) -{1,1}> add_ConstantStackPush_383(iconst_1000, o37, iconst_0, o31, env, static) :|: 0 < o37 && 0 < o31 && iconst_0 = 0 && iconst_1000 = 1000
add_ConstantStackPush_383(iconst_1000, o37, iconst_0, o31, env, static) -{1,1}> add_Store_389(iconst_0, iconst_1000, o37, o31, env, static) :|: 0 < o37 && 0 < o31 && iconst_0 = 0 && iconst_1000 = 1000
add_Store_389(iconst_0, iconst_1000, o37, o31, env, static) -{1,1}> add_Load_394(iconst_1000, o37, iconst_0, o31, env, static) :|: 0 < o37 && 0 < o31 && iconst_0 = 0 && iconst_1000 = 1000
add_Load_394(iconst_1000, o37, iconst_0, o31, env, static) -{0,0}> add_Load_453(iconst_1000, o37, iconst_0, iconst_0, o31, env, static) :|: 0 < o37 && 0 <= iconst_0 && iconst_0 <= 2 && 0 < o31 && iconst_0 = 0 && iconst_1000 = 1000
add_Load_453(iconst_1000, o111, iconst_0, i48, o112, env, static) -{0,0}> add_Load_522(iconst_1000, o111, iconst_0, i48, o112, env, static) :|: 0 <= iconst_0 && iconst_0 <= 2 && 0 <= i48 && i48 <= 4 && iconst_0 = 0 && 0 < o112 && iconst_1000 = 1000 && 0 < o111 && i48 <= 2
add_Load_522(iconst_1000, o169, i74, i75, o170, env, static) -{0,0}> add_Load_599(iconst_1000, o169, i74, i75, o170, env, static) :|: i74 <= 2 && i75 <= 4 && iconst_1000 = 1000 && 0 < o170 && 0 <= i75 && 0 < o169 && 0 <= i74
add_Load_599(iconst_1000, o227, i104, i105, o228, env, static) -{1,1}> add_Load_600(i105, iconst_1000, o227, i104, o228, env, static) :|: 0 < o227 && 0 <= i105 && 0 <= i104 && iconst_1000 = 1000 && 0 < o228
add_Load_600(i105, iconst_1000, o227, i104, o228, env, static) -{1,1}> add_GT_602(i105, iconst_1000, o227, i104, o228, env, static) :|: 0 < o227 && 0 <= i105 && 0 <= i104 && iconst_1000 = 1000 && 0 < o228
add_GT_602(i112, iconst_1000, o227, i104, o228, env, static) -{0,0}> add_GT_607(i112, iconst_1000, o227, i104, o228, env, static) :|: 0 < o227 && 0 <= i112 && 0 <= i104 && iconst_1000 = 1000 && 0 < o228 && i112 <= 1000
add_GT_602(i113, iconst_1000, o227, i104, o228, env, static) -{0,0}> add_GT_608(i113, iconst_1000, o227, i104, o228, env, static) :|: 0 < o227 && 1001 <= i113 && 0 <= i113 && 0 <= i104 && iconst_1000 = 1000 && 0 < o228
add_GT_607(i112, iconst_1000, o227, i104, o228, env, static) -{1,1}> add_Load_621(iconst_1000, o227, i104, i112, o228, env, static) :|: 0 < o227 && 0 <= i112 && i112 <= iconst_1000 && 0 <= i104 && iconst_1000 = 1000 && 0 < o228 && i112 <= 1000
add_GT_608(i113, iconst_1000, o227, i104, o228, env, static) -{1,1}> add_Load_624(i104, iconst_1000, o228, env, static) :|: 0 < o227 && 1001 <= i113 && iconst_1000 < i113 && 0 <= i104 && iconst_1000 = 1000 && 0 < o228
add_Load_621(iconst_1000, o227, i104, i112, o228, env, static) -{1,1}> add_Load_627(i104, iconst_1000, o227, i112, o228, env, static) :|: 0 < o227 && 0 <= i112 && 0 <= i104 && iconst_1000 = 1000 && 0 < o228 && i112 <= 1000
add_Load_624(i104, iconst_1000, o228, env, static) -{1,1}> add_Return_631(i104, iconst_1000, o228, env, static) :|: 0 <= i104 && iconst_1000 = 1000 && 0 < o228
add_Load_627(i104, iconst_1000, o227, i112, o228, env, static) -{1,1}> add_IntArithmetic_636(i104, i112, iconst_1000, o227, o228, env, static) :|: 0 < o227 && 0 <= i112 && 0 <= i104 && iconst_1000 = 1000 && 0 < o228 && i112 <= 1000
add_Return_631(i104, iconst_1000, o228, env, static) -{1,1}> main_Store_637(i104, iconst_1000, o228, env, static) :|: 0 <= i104 && iconst_1000 = 1000 && 0 < o228
add_IntArithmetic_636(i104, i112, iconst_1000, o227, o228, env, static) -{1,1}> add_Store_643(i126, iconst_1000, o227, i112, o228, env, static) :|: 0 < o227 && 0 <= i112 && 0 <= i104 && iconst_1000 = 1000 && 0 < o228 && i112 <= 1000 && 0 <= i126 && i104 + i112 = i126
main_Store_637(i104, iconst_1000, o228, env, static) -{1,1}> main_New_645(iconst_1000, o228, env, static) :|: 0 <= i104 && iconst_1000 = 1000 && 0 < o228
add_Store_643(i126, iconst_1000, o227, i112, o228, env, static) -{1,1}> add_Load_648(iconst_1000, o227, i126, i112, o228, env, static) :|: 0 < o227 && 0 <= i112 && iconst_1000 = 1000 && 0 < o228 && 0 <= i126 && i112 <= 1000
main_New_645(iconst_1000, o228, env, static) -{0,0}> main_New_649(iconst_1000, o228, env, static) :|: iconst_1000 = 1000 && 0 < o228
add_Load_648(iconst_1000, o227, i126, i112, o228, env, static) -{1,1}> add_Load_650(o227, iconst_1000, i126, i112, o228, env, static) :|: 0 < o227 && 0 <= i112 && iconst_1000 = 1000 && 0 < o228 && 0 <= i126 && i112 <= 1000
main_New_649(iconst_1000, o228, env, static) -{1,1}> main_Duplicate_651(o275, iconst_1000, o228, env, static) :|: 0 < o275 && o275 = 1 && iconst_1000 = 1000 && 0 < o228
add_Load_650(o227, iconst_1000, i126, i112, o228, env, static) -{1,1}> add_InvokeMethod_653(o227, i112, iconst_1000, i126, o228, env, static) :|: 0 < o227 && 0 <= i112 && iconst_1000 = 1000 && 0 < o228 && 0 <= i126 && i112 <= 1000
main_Duplicate_651(o275, iconst_1000, o228, env, static) -{1,1}> main_InvokeMethod_654(o275, iconst_1000, o228, env, static) :|: 0 < o275 && iconst_1000 = 1000 && 0 < o228
add_InvokeMethod_653(o227, i112, iconst_1000, i126, o228, env, static) -{1,1}> incr_Load_655(i112, iconst_1000, o227, i126, o228, env, static) :|: 0 < o227 && 0 <= i112 && iconst_1000 = 1000 && 0 < o228 && i112 <= 1000 && 0 <= i126
main_InvokeMethod_654(o275, iconst_1000, o228, env, static) -{1,1}> langle_init_rangle_Load_656(o275, iconst_1000, o228, env, static) :|: 0 < o275 && iconst_1000 = 1000 && 0 < o228
incr_Load_655(i112, iconst_1000, o227, i126, o228, env, static) -{1,1}> incr_ConstantStackPush_658(i112, iconst_1000, o227, i126, o228, env, static) :|: 0 < o227 && 0 <= i112 && iconst_1000 = 1000 && 0 < o228 && i112 <= 1000 && 0 <= i126
langle_init_rangle_Load_656(o275, iconst_1000, o228, env, static) -{1,1}> langle_init_rangle_InvokeMethod_659(o275, iconst_1000, o228, env, static) :|: 0 < o275 && iconst_1000 = 1000 && 0 < o228
incr_ConstantStackPush_658(i112, iconst_1000, o227, i126, o228, env, static) -{1,1}> incr_IntArithmetic_660(i112, iconst_2, iconst_1000, o227, i126, o228, env, static) :|: 0 < o227 && 0 <= i112 && iconst_1000 = 1000 && 0 < o228 && i112 <= 1000 && 0 <= i126 && iconst_2 = 2
langle_init_rangle_InvokeMethod_659(o275, iconst_1000, o228, env, static) -{1,1}> langle_init_rangle_Load_661(o275, iconst_1000, o228, env, static) :|: 0 < o275 && iconst_1000 = 1000 && 0 < o228
incr_IntArithmetic_660(i112, iconst_2, iconst_1000, o227, i126, o228, env, static) -{1,1}> incr_Duplicate_662(i135, iconst_1000, o227, i126, o228, env, static) :|: i112 + iconst_2 = i135 && 0 < o227 && i135 <= 1002 && 0 <= i112 && 2 <= i135 && iconst_1000 = 1000 && 0 < o228 && i112 <= 1000 && 0 <= i126 && iconst_2 = 2
langle_init_rangle_Load_661(o275, iconst_1000, o228, env, static) -{1,1}> langle_init_rangle_InvokeMethod_664(o275, iconst_1000, o228, env, static) :|: 0 < o275 && iconst_1000 = 1000 && 0 < o228
incr_Duplicate_662(i135, iconst_1000, o227, i126, o228, env, static) -{1,1}> incr_Store_663(i135, iconst_1000, o227, i126, o228, env, static) :|: i135 <= 1002 && 0 < o227 && 2 <= i135 && iconst_1000 = 1000 && 0 < o228 && 0 <= i126
incr_Store_663(i135, iconst_1000, o227, i126, o228, env, static) -{1,1}> incr_Return_665(i135, iconst_1000, o227, i126, o228, env, static) :|: i135 <= 1002 && 0 < o227 && 2 <= i135 && iconst_1000 = 1000 && 0 < o228 && 0 <= i126
langle_init_rangle_InvokeMethod_664(o275, iconst_1000, o228, env, static) -{1,1}> langle_init_rangle_Load_666(o275, iconst_1000, o228, env, static) :|: 0 < o275 && iconst_1000 = 1000 && 0 < o228
incr_Return_665(i135, iconst_1000, o227, i126, o228, env, static) -{1,1}> add_Store_667(i135, iconst_1000, o227, i126, o228, env, static) :|: i135 <= 1002 && 0 < o227 && 2 <= i135 && iconst_1000 = 1000 && 0 < o228 && 0 <= i126
langle_init_rangle_Load_666(o275, iconst_1000, o228, env, static) -{1,1}> langle_init_rangle_InvokeMethod_673(o275, iconst_1000, o228, env, static) :|: 0 < o275 && iconst_1000 = 1000 && 0 < o228
add_Store_667(i135, iconst_1000, o227, i126, o228, env, static) -{1,1}> add_JMP_668(iconst_1000, o227, i126, i135, o228, env, static) :|: i135 <= 1002 && 0 < o227 && 2 <= i135 && iconst_1000 = 1000 && 0 < o228 && 0 <= i126
add_JMP_668(iconst_1000, o227, i126, i135, o228, env, static) -{1,1}> add_Load_678(iconst_1000, o227, i126, i135, o228, env, static) :|: 0 < o227 && i135 <= 1002 && 2 <= i135 && iconst_1000 = 1000 && 0 < o228 && 0 <= i126
langle_init_rangle_InvokeMethod_673(o275, iconst_1000, o228, env, static) -{1,1}> langle_init_rangle_Return_684(o275, iconst_1000, o228, env, static) :|: 0 < o275 && iconst_1000 = 1000 && 0 < o228
add_Load_678(iconst_1000, o227, i126, i135, o228, env, static) -{0,0}> add_Load_599(iconst_1000, o227, i126, i135, o228, env, static) :|: 0 < o227 && i135 <= 1002 && 2 <= i135 && iconst_1000 = 1000 && 0 <= i135 && 0 < o228 && 0 <= i126
langle_init_rangle_Return_684(o275, iconst_1000, o228, env, static) -{1,1}> langle_init_rangle_Return_688(o275, iconst_1000, o228, env, static) :|: 0 < o275 && iconst_1000 = 1000 && 0 < o228
langle_init_rangle_Return_688(o275, iconst_1000, o228, env, static) -{1,1}> langle_init_rangle_Return_689(o275, iconst_1000, o228, env, static) :|: 0 < o275 && iconst_1000 = 1000 && 0 < o228
langle_init_rangle_Return_689(o275, iconst_1000, o228, env, static) -{1,1}> main_Store_690(o275, iconst_1000, o228, env, static) :|: 0 < o275 && iconst_1000 = 1000 && 0 < o228
main_Store_690(o275, iconst_1000, o228, env, static) -{1,1}> main_Load_691(iconst_1000, o228, o275, env, static) :|: 0 < o275 && iconst_1000 = 1000 && 0 < o228
main_Load_691(iconst_1000, o228, o275, env, static) -{1,1}> main_Load_692(o228, iconst_1000, o275, env, static) :|: 0 < o275 && iconst_1000 = 1000 && 0 < o228
main_Load_692(o228, iconst_1000, o275, env, static) -{1,1}> main_Load_693(o228, iconst_1000, o275, env, static) :|: 0 < o275 && iconst_1000 = 1000 && 0 < o228
main_Load_693(o228, iconst_1000, o275, env, static) -{1,1}> main_InvokeMethod_694(o228, iconst_1000, o275, env, static) :|: 0 < o275 && iconst_1000 = 1000 && 0 < o228
main_InvokeMethod_694(o228, iconst_1000, o275, env, static) -{1,1}> add_ConstantStackPush_695(iconst_1000, o275, env, static) :|: 0 < o275 && iconst_1000 = 1000 && 0 < o228
add_ConstantStackPush_695(iconst_1000, o275, env, static) -{1,1}> add_Store_702(iconst_0, iconst_1000, o275, env, static) :|: 0 < o275 && iconst_0 = 0 && iconst_1000 = 1000
add_Store_702(iconst_0, iconst_1000, o275, env, static) -{1,1}> add_ConstantStackPush_709(iconst_1000, o275, iconst_0, env, static) :|: 0 < o275 && iconst_0 = 0 && iconst_1000 = 1000
add_ConstantStackPush_709(iconst_1000, o275, iconst_0, env, static) -{1,1}> add_Store_715(iconst_0, iconst_1000, o275, env, static) :|: 0 < o275 && iconst_0 = 0 && iconst_1000 = 1000
add_Store_715(iconst_0, iconst_1000, o275, env, static) -{1,1}> add_Load_717(iconst_1000, o275, iconst_0, env, static) :|: 0 < o275 && iconst_0 = 0 && iconst_1000 = 1000
add_Load_717(iconst_1000, o275, iconst_0, env, static) -{0,0}> add_Load_808(iconst_1000, o275, iconst_0, iconst_0, env, static) :|: 0 <= iconst_0 && 0 < o275 && iconst_0 = 0 && iconst_1000 = 1000 && iconst_0 <= 3
add_Load_808(iconst_1000, o438, iconst_0, i194, env, static) -{0,0}> add_Load_889(iconst_1000, o438, iconst_0, i194, env, static) :|: i194 <= 3 && 0 <= iconst_0 && iconst_0 = 0 && iconst_1000 = 1000 && 0 <= i194 && 0 < o438 && iconst_0 <= 3 && i194 <= 6
add_Load_889(iconst_1000, o538, i241, i242, env, static) -{0,0}> add_Load_954(iconst_1000, o538, i241, i242, env, static) :|: i242 <= 6 && 0 < o538 && 0 <= i242 && 0 <= i241 && iconst_1000 = 1000 && i241 <= 3
add_Load_954(iconst_1000, o644, i296, i297, env, static) -{1,1}> add_Load_955(i297, iconst_1000, o644, i296, env, static) :|: 0 <= i297 && iconst_1000 = 1000 && 0 <= i296 && 0 < o644
add_Load_955(i297, iconst_1000, o644, i296, env, static) -{1,1}> add_GT_956(i297, iconst_1000, o644, i296, env, static) :|: 0 <= i297 && iconst_1000 = 1000 && 0 <= i296 && 0 < o644
add_GT_956(i308, iconst_1000, o644, i296, env, static) -{0,0}> add_GT_957(i308, iconst_1000, o644, i296, env, static) :|: i308 <= 1000 && 0 <= i308 && iconst_1000 = 1000 && 0 <= i296 && 0 < o644
add_GT_956(i309, iconst_1000, o644, i296, env, static) -{0,0}> add_GT_958(i309, iconst_1000, o644, i296, env, static) :|: 1001 <= i309 && 0 <= i309 && iconst_1000 = 1000 && 0 <= i296 && 0 < o644
add_GT_957(i308, iconst_1000, o644, i296, env, static) -{1,1}> add_Load_959(iconst_1000, o644, i296, i308, env, static) :|: i308 <= 1000 && i308 <= iconst_1000 && 0 <= i308 && iconst_1000 = 1000 && 0 <= i296 && 0 < o644
add_Load_959(iconst_1000, o644, i296, i308, env, static) -{1,1}> add_Load_963(i296, iconst_1000, o644, i308, env, static) :|: i308 <= 1000 && 0 <= i308 && iconst_1000 = 1000 && 0 <= i296 && 0 < o644
add_Load_963(i296, iconst_1000, o644, i308, env, static) -{1,1}> add_IntArithmetic_973(i296, i308, iconst_1000, o644, env, static) :|: i308 <= 1000 && 0 <= i308 && iconst_1000 = 1000 && 0 <= i296 && 0 < o644
add_IntArithmetic_973(i296, i308, iconst_1000, o644, env, static) -{1,1}> add_Store_981(i334, iconst_1000, o644, i308, env, static) :|: i308 <= 1000 && 0 <= i308 && iconst_1000 = 1000 && 0 <= i296 && 0 <= i334 && 0 < o644 && i296 + i308 = i334
add_Store_981(i334, iconst_1000, o644, i308, env, static) -{1,1}> add_Load_985(iconst_1000, o644, i334, i308, env, static) :|: i308 <= 1000 && 0 <= i308 && iconst_1000 = 1000 && 0 <= i334 && 0 < o644
add_Load_985(iconst_1000, o644, i334, i308, env, static) -{1,1}> add_Load_993(o644, iconst_1000, i334, i308, env, static) :|: i308 <= 1000 && 0 <= i308 && iconst_1000 = 1000 && 0 <= i334 && 0 < o644
add_Load_993(o644, iconst_1000, i334, i308, env, static) -{1,1}> add_InvokeMethod_999(o644, i308, iconst_1000, i334, env, static) :|: i308 <= 1000 && 0 <= i308 && iconst_1000 = 1000 && 0 <= i334 && 0 < o644
add_InvokeMethod_999(o644, i308, iconst_1000, i334, env, static) -{1,1}> incr_Load_1001(i308, iconst_1000, o644, i334, env, static) :|: i308 <= 1000 && 0 <= i308 && iconst_1000 = 1000 && 0 <= i334 && 0 < o644
incr_Load_1001(i308, iconst_1000, o644, i334, env, static) -{1,1}> incr_ConstantStackPush_1004(i308, iconst_1000, o644, i334, env, static) :|: i308 <= 1000 && 0 <= i308 && iconst_1000 = 1000 && 0 <= i334 && 0 < o644
incr_ConstantStackPush_1004(i308, iconst_1000, o644, i334, env, static) -{1,1}> incr_IntArithmetic_1006(i308, iconst_3, iconst_1000, o644, i334, env, static) :|: i308 <= 1000 && iconst_3 = 3 && 0 <= i308 && iconst_1000 = 1000 && 0 <= i334 && 0 < o644
incr_IntArithmetic_1006(i308, iconst_3, iconst_1000, o644, i334, env, static) -{1,1}> incr_Duplicate_1008(i351, iconst_1000, o644, i334, env, static) :|: i308 <= 1000 && i308 + iconst_3 = i351 && i351 <= 1003 && iconst_3 = 3 && 0 <= i308 && iconst_1000 = 1000 && 3 <= i351 && 0 <= i334 && 0 < o644
incr_Duplicate_1008(i351, iconst_1000, o644, i334, env, static) -{1,1}> incr_Store_1010(i351, iconst_1000, o644, i334, env, static) :|: i351 <= 1003 && iconst_1000 = 1000 && 3 <= i351 && 0 <= i334 && 0 < o644
incr_Store_1010(i351, iconst_1000, o644, i334, env, static) -{1,1}> incr_Return_1012(i351, iconst_1000, o644, i334, env, static) :|: i351 <= 1003 && iconst_1000 = 1000 && 3 <= i351 && 0 <= i334 && 0 < o644
incr_Return_1012(i351, iconst_1000, o644, i334, env, static) -{1,1}> add_Store_1013(i351, iconst_1000, o644, i334, env, static) :|: i351 <= 1003 && iconst_1000 = 1000 && 3 <= i351 && 0 <= i334 && 0 < o644
add_Store_1013(i351, iconst_1000, o644, i334, env, static) -{1,1}> add_JMP_1017(iconst_1000, o644, i334, i351, env, static) :|: i351 <= 1003 && iconst_1000 = 1000 && 3 <= i351 && 0 <= i334 && 0 < o644
add_JMP_1017(iconst_1000, o644, i334, i351, env, static) -{1,1}> add_Load_1021(iconst_1000, o644, i334, i351, env, static) :|: i351 <= 1003 && iconst_1000 = 1000 && 3 <= i351 && 0 <= i334 && 0 < o644
add_Load_1021(iconst_1000, o644, i334, i351, env, static) -{0,0}> add_Load_954(iconst_1000, o644, i334, i351, env, static) :|: i351 <= 1003 && 0 <= i351 && iconst_1000 = 1000 && 3 <= i351 && 0 <= i334 && 0 < o644

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

obtained
main_ConstantStackPush_2(env, static) -{39,39}> add_Load_283(1000, 1, 0, 0, 1, env, static'1) :|: 0 >= 0 && 0 <= 1 && 0 < 2 && 0 <= 0 && 0 <= static'1 && 0 <= static && 0 < 1 && 0 <= 2 && static''' <= static + 2 && 0 <= static''' && static'1 <= static''' + 1
by chaining
main_ConstantStackPush_2(env, static) -{0,0}> main_ConstantStackPush_4(env, static) :|: 0 >= 0
main_ConstantStackPush_4(env, static) -{0,0}> langle_clinit_rangle_ConstantStackPush_6(env, static) :|: 0 >= 0
langle_clinit_rangle_ConstantStackPush_6(env, static) -{1,1}> langle_clinit_rangle_ArrayCreate_13(iconst_0, env, static) :|: iconst_0 = 0
langle_clinit_rangle_ArrayCreate_13(iconst_0, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_16(a2, iconst_0, env, static) :|: a2 = 2 && iconst_0 = 0 && 0 < a2
langle_clinit_rangle_FieldAccess_16(a2, iconst_0, env, static) -{1,1}> langle_clinit_rangle_New_17(env, static') :|: 0 <= a2 && iconst_0 = 0 && static' <= static + a2 && 0 <= static && 0 < a2
langle_clinit_rangle_New_17(env, static) -{0,0}> langle_clinit_rangle_New_18(env, static) :|: 0 >= 0
langle_clinit_rangle_New_18(env, static) -{0,0}> langle_clinit_rangle_New_20(env, static) :|: 0 <= static
langle_clinit_rangle_New_20(env, static) -{1,1}> langle_clinit_rangle_Duplicate_21(o2, env, static) :|: 0 < o2 && o2 = 1
langle_clinit_rangle_Duplicate_21(o2, env, static) -{1,1}> langle_clinit_rangle_ConstantStackPush_23(o2, env, static) :|: 0 < o2
langle_clinit_rangle_ConstantStackPush_23(o2, env, static) -{1,1}> langle_clinit_rangle_InvokeMethod_25(o2, NULL, env, static) :|: NULL = 0 && 0 < o2
langle_clinit_rangle_InvokeMethod_25(o2, NULL, env, static) -{1,1}> langle_init_rangle_Load_27(o2, env, static) :|: NULL = 0 && 0 < o2
langle_init_rangle_Load_27(o2, env, static) -{1,1}> langle_init_rangle_InvokeMethod_29(o2, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_29(o2, env, static) -{1,1}> langle_init_rangle_Load_31(o2, env, static) :|: 0 < o2
langle_init_rangle_Load_31(o2, env, static) -{1,1}> langle_init_rangle_InvokeMethod_33(o2, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_33(o2, env, static) -{1,1}> langle_init_rangle_Return_36(o2, env, static) :|: 0 < o2
langle_init_rangle_Return_36(o2, env, static) -{1,1}> langle_init_rangle_Return_38(o2, env, static) :|: 0 < o2
langle_init_rangle_Return_38(o2, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_39(o2, env, static) :|: 0 < o2
langle_clinit_rangle_FieldAccess_39(o2, env, static) -{1,1}> langle_clinit_rangle_Return_40(env, static') :|: 0 < o2 && 0 <= o2 && 0 <= static && static' <= static + o2
langle_clinit_rangle_Return_40(env, static) -{1,1}> main_ConstantStackPush_48(env, static) :|: 0 >= 0
main_ConstantStackPush_48(env, static) -{0,0}> main_ConstantStackPush_49(env, static) :|: 0 >= 0
main_ConstantStackPush_49(env, static) -{0,0}> main_ConstantStackPush_52(env, static) :|: 0 <= static
main_ConstantStackPush_52(env, static) -{0,0}> main_ConstantStackPush_53(env, static) :|: 0 >= 0
main_ConstantStackPush_53(env, static) -{0,0}> main_ConstantStackPush_55(env, static) :|: 0 >= 0
main_ConstantStackPush_55(env, static) -{1,1}> main_Store_57(iconst_1000, env, static) :|: iconst_1000 = 1000
main_Store_57(iconst_1000, env, static) -{1,1}> main_New_59(iconst_1000, env, static) :|: iconst_1000 = 1000
main_New_59(iconst_1000, env, static) -{1,1}> main_Duplicate_61(o4, iconst_1000, env, static) :|: o4 = 1 && 0 < o4 && iconst_1000 = 1000
main_Duplicate_61(o4, iconst_1000, env, static) -{1,1}> main_InvokeMethod_63(o4, iconst_1000, env, static) :|: 0 < o4 && iconst_1000 = 1000
main_InvokeMethod_63(o4, iconst_1000, env, static) -{1,1}> langle_init_rangle_Load_65(o4, iconst_1000, env, static) :|: 0 < o4 && iconst_1000 = 1000
langle_init_rangle_Load_65(o4, iconst_1000, env, static) -{1,1}> langle_init_rangle_InvokeMethod_68(o4, iconst_1000, env, static) :|: 0 < o4 && iconst_1000 = 1000
langle_init_rangle_InvokeMethod_68(o4, iconst_1000, env, static) -{1,1}> langle_init_rangle_Return_70(o4, iconst_1000, env, static) :|: 0 < o4 && iconst_1000 = 1000
langle_init_rangle_Return_70(o4, iconst_1000, env, static) -{1,1}> main_Store_72(o4, iconst_1000, env, static) :|: 0 < o4 && iconst_1000 = 1000
main_Store_72(o4, iconst_1000, env, static) -{1,1}> main_New_75(iconst_1000, o4, env, static) :|: 0 < o4 && iconst_1000 = 1000
main_New_75(iconst_1000, o4, env, static) -{0,0}> main_New_77(iconst_1000, o4, env, static) :|: 0 < o4 && iconst_1000 = 1000
main_New_77(iconst_1000, o4, env, static) -{1,1}> main_Duplicate_79(o6, iconst_1000, o4, env, static) :|: 0 < o6 && 0 < o4 && o6 = 1 && iconst_1000 = 1000
main_Duplicate_79(o6, iconst_1000, o4, env, static) -{1,1}> main_InvokeMethod_80(o6, iconst_1000, o4, env, static) :|: 0 < o6 && 0 < o4 && iconst_1000 = 1000
main_InvokeMethod_80(o6, iconst_1000, o4, env, static) -{1,1}> langle_init_rangle_Load_82(o6, iconst_1000, o4, env, static) :|: 0 < o6 && 0 < o4 && iconst_1000 = 1000
langle_init_rangle_Load_82(o6, iconst_1000, o4, env, static) -{1,1}> langle_init_rangle_InvokeMethod_84(o6, iconst_1000, o4, env, static) :|: 0 < o6 && 0 < o4 && iconst_1000 = 1000
langle_init_rangle_InvokeMethod_84(o6, iconst_1000, o4, env, static) -{1,1}> langle_init_rangle_Return_86(o6, iconst_1000, o4, env, static) :|: 0 < o6 && 0 < o4 && iconst_1000 = 1000
langle_init_rangle_Return_86(o6, iconst_1000, o4, env, static) -{1,1}> main_Store_89(o6, iconst_1000, o4, env, static) :|: 0 < o6 && 0 < o4 && iconst_1000 = 1000
main_Store_89(o6, iconst_1000, o4, env, static) -{1,1}> main_Load_91(iconst_1000, o4, o6, env, static) :|: 0 < o6 && 0 < o4 && iconst_1000 = 1000
main_Load_91(iconst_1000, o4, o6, env, static) -{1,1}> main_Load_93(o4, iconst_1000, o6, env, static) :|: 0 < o6 && 0 < o4 && iconst_1000 = 1000
main_Load_93(o4, iconst_1000, o6, env, static) -{1,1}> main_Load_94(o4, iconst_1000, o6, env, static) :|: 0 < o6 && 0 < o4 && iconst_1000 = 1000
main_Load_94(o4, iconst_1000, o6, env, static) -{1,1}> main_InvokeMethod_95(o4, iconst_1000, o6, env, static) :|: 0 < o6 && 0 < o4 && iconst_1000 = 1000
main_InvokeMethod_95(o4, iconst_1000, o6, env, static) -{1,1}> add_ConstantStackPush_96(iconst_1000, o6, o4, env, static) :|: 0 < o6 && 0 < o4 && iconst_1000 = 1000
add_ConstantStackPush_96(iconst_1000, o6, o4, env, static) -{1,1}> add_Store_97(iconst_0, iconst_1000, o6, o4, env, static) :|: 0 < o6 && 0 < o4 && iconst_0 = 0 && iconst_1000 = 1000
add_Store_97(iconst_0, iconst_1000, o6, o4, env, static) -{1,1}> add_ConstantStackPush_98(iconst_1000, o6, iconst_0, o4, env, static) :|: 0 < o6 && 0 < o4 && iconst_0 = 0 && iconst_1000 = 1000
add_ConstantStackPush_98(iconst_1000, o6, iconst_0, o4, env, static) -{1,1}> add_Store_99(iconst_0, iconst_1000, o6, o4, env, static) :|: 0 < o6 && 0 < o4 && iconst_0 = 0 && iconst_1000 = 1000
add_Store_99(iconst_0, iconst_1000, o6, o4, env, static) -{1,1}> add_Load_100(iconst_1000, o6, iconst_0, o4, env, static) :|: 0 < o6 && 0 < o4 && iconst_0 = 0 && iconst_1000 = 1000
add_Load_100(iconst_1000, o6, iconst_0, o4, env, static) -{0,0}> add_Load_156(iconst_1000, o6, iconst_0, iconst_0, o4, env, static) :|: 0 <= iconst_0 && 0 < o6 && 0 < o4 && iconst_0 <= 1 && iconst_0 = 0 && iconst_1000 = 1000
add_Load_156(iconst_1000, o10, iconst_0, i1, o11, env, static) -{0,0}> add_Load_228(iconst_1000, o10, iconst_0, i1, o11, env, static) :|: 0 <= iconst_0 && 0 <= i1 && i1 <= 1 && iconst_0 <= 1 && iconst_0 = 0 && 0 < o11 && iconst_1000 = 1000 && 0 < o10 && i1 <= 2
add_Load_228(iconst_1000, o20, i4, i5, o21, env, static) -{0,0}> add_Load_283(iconst_1000, o20, i4, i5, o21, env, static) :|: 0 < o20 && i5 <= 2 && 0 <= i4 && 0 < o21 && iconst_1000 = 1000 && 0 <= i5 && i4 <= 1

obtained
add_Load_283(1000, o30, i10, i11, o31, env, static) -{2,2}> add_GT_299(i11, 1000, o30, i10, o31, env, static) :|: 0 < o31 && 0 <= i11 && 0 <= i10 && 0 < o30
by chaining
add_Load_283(iconst_1000, o30, i10, i11, o31, env, static) -{1,1}> add_Load_286(i11, iconst_1000, o30, i10, o31, env, static) :|: 0 <= i10 && 0 < o30 && 0 <= i11 && 0 < o31 && iconst_1000 = 1000
add_Load_286(i11, iconst_1000, o30, i10, o31, env, static) -{1,1}> add_GT_299(i11, iconst_1000, o30, i10, o31, env, static) :|: 0 <= i10 && 0 < o30 && 0 <= i11 && 0 < o31 && iconst_1000 = 1000

obtained
add_GT_299(i19, 1000, o30, i10, o31, env, static) -{22,22}> add_Load_599(1000, 1, 0, 0, o31, env, static) :|: 1001 <= i19 && 0 <= 0 && 0 < o30 && 0 < 1 && 0 <= i10 && 0 <= 4 && 0 < o31 && 0 <= 2 && 0 <= i19 && 1000 < i19
by chaining
add_GT_299(i19, iconst_1000, o30, i10, o31, env, static) -{0,0}> add_GT_305(i19, iconst_1000, o30, i10, o31, env, static) :|: 0 <= i10 && 0 < o30 && 0 < o31 && 1001 <= i19 && iconst_1000 = 1000 && 0 <= i19
add_GT_305(i19, iconst_1000, o30, i10, o31, env, static) -{1,1}> add_Load_317(i10, iconst_1000, o31, env, static) :|: 0 <= i10 && 0 < o30 && 0 < o31 && 1001 <= i19 && iconst_1000 < i19 && iconst_1000 = 1000
add_Load_317(i10, iconst_1000, o31, env, static) -{1,1}> add_Return_321(i10, iconst_1000, o31, env, static) :|: 0 <= i10 && 0 < o31 && iconst_1000 = 1000
add_Return_321(i10, iconst_1000, o31, env, static) -{1,1}> main_Store_325(i10, iconst_1000, o31, env, static) :|: 0 <= i10 && 0 < o31 && iconst_1000 = 1000
main_Store_325(i10, iconst_1000, o31, env, static) -{1,1}> main_New_331(iconst_1000, o31, env, static) :|: 0 <= i10 && 0 < o31 && iconst_1000 = 1000
main_New_331(iconst_1000, o31, env, static) -{0,0}> main_New_333(iconst_1000, o31, env, static) :|: 0 < o31 && iconst_1000 = 1000
main_New_333(iconst_1000, o31, env, static) -{1,1}> main_Duplicate_335(o37, iconst_1000, o31, env, static) :|: 0 < o37 && 0 < o31 && o37 = 1 && iconst_1000 = 1000
main_Duplicate_335(o37, iconst_1000, o31, env, static) -{1,1}> main_InvokeMethod_337(o37, iconst_1000, o31, env, static) :|: 0 < o37 && 0 < o31 && iconst_1000 = 1000
main_InvokeMethod_337(o37, iconst_1000, o31, env, static) -{1,1}> langle_init_rangle_Load_339(o37, iconst_1000, o31, env, static) :|: 0 < o37 && 0 < o31 && iconst_1000 = 1000
langle_init_rangle_Load_339(o37, iconst_1000, o31, env, static) -{1,1}> langle_init_rangle_InvokeMethod_341(o37, iconst_1000, o31, env, static) :|: 0 < o37 && 0 < o31 && iconst_1000 = 1000
langle_init_rangle_InvokeMethod_341(o37, iconst_1000, o31, env, static) -{1,1}> langle_init_rangle_Load_344(o37, iconst_1000, o31, env, static) :|: 0 < o37 && 0 < o31 && iconst_1000 = 1000
langle_init_rangle_Load_344(o37, iconst_1000, o31, env, static) -{1,1}> langle_init_rangle_InvokeMethod_351(o37, iconst_1000, o31, env, static) :|: 0 < o37 && 0 < o31 && iconst_1000 = 1000
langle_init_rangle_InvokeMethod_351(o37, iconst_1000, o31, env, static) -{1,1}> langle_init_rangle_Return_357(o37, iconst_1000, o31, env, static) :|: 0 < o37 && 0 < o31 && iconst_1000 = 1000
langle_init_rangle_Return_357(o37, iconst_1000, o31, env, static) -{1,1}> langle_init_rangle_Return_361(o37, iconst_1000, o31, env, static) :|: 0 < o37 && 0 < o31 && iconst_1000 = 1000
langle_init_rangle_Return_361(o37, iconst_1000, o31, env, static) -{1,1}> main_Store_365(o37, iconst_1000, o31, env, static) :|: 0 < o37 && 0 < o31 && iconst_1000 = 1000
main_Store_365(o37, iconst_1000, o31, env, static) -{1,1}> main_Load_372(iconst_1000, o31, o37, env, static) :|: 0 < o37 && 0 < o31 && iconst_1000 = 1000
main_Load_372(iconst_1000, o31, o37, env, static) -{1,1}> main_Load_373(o31, iconst_1000, o37, env, static) :|: 0 < o37 && 0 < o31 && iconst_1000 = 1000
main_Load_373(o31, iconst_1000, o37, env, static) -{1,1}> main_Load_374(o31, iconst_1000, o37, env, static) :|: 0 < o37 && 0 < o31 && iconst_1000 = 1000
main_Load_374(o31, iconst_1000, o37, env, static) -{1,1}> main_InvokeMethod_375(o31, iconst_1000, o37, env, static) :|: 0 < o37 && 0 < o31 && iconst_1000 = 1000
main_InvokeMethod_375(o31, iconst_1000, o37, env, static) -{1,1}> add_ConstantStackPush_376(iconst_1000, o37, o31, env, static) :|: 0 < o37 && 0 < o31 && iconst_1000 = 1000
add_ConstantStackPush_376(iconst_1000, o37, o31, env, static) -{1,1}> add_Store_378(iconst_0, iconst_1000, o37, o31, env, static) :|: 0 < o37 && 0 < o31 && iconst_0 = 0 && iconst_1000 = 1000
add_Store_378(iconst_0, iconst_1000, o37, o31, env, static) -{1,1}> add_ConstantStackPush_383(iconst_1000, o37, iconst_0, o31, env, static) :|: 0 < o37 && 0 < o31 && iconst_0 = 0 && iconst_1000 = 1000
add_ConstantStackPush_383(iconst_1000, o37, iconst_0, o31, env, static) -{1,1}> add_Store_389(iconst_0, iconst_1000, o37, o31, env, static) :|: 0 < o37 && 0 < o31 && iconst_0 = 0 && iconst_1000 = 1000
add_Store_389(iconst_0, iconst_1000, o37, o31, env, static) -{1,1}> add_Load_394(iconst_1000, o37, iconst_0, o31, env, static) :|: 0 < o37 && 0 < o31 && iconst_0 = 0 && iconst_1000 = 1000
add_Load_394(iconst_1000, o37, iconst_0, o31, env, static) -{0,0}> add_Load_453(iconst_1000, o37, iconst_0, iconst_0, o31, env, static) :|: 0 < o37 && 0 <= iconst_0 && iconst_0 <= 2 && 0 < o31 && iconst_0 = 0 && iconst_1000 = 1000
add_Load_453(iconst_1000, o111, iconst_0, i48, o112, env, static) -{0,0}> add_Load_522(iconst_1000, o111, iconst_0, i48, o112, env, static) :|: 0 <= iconst_0 && iconst_0 <= 2 && 0 <= i48 && i48 <= 4 && iconst_0 = 0 && 0 < o112 && iconst_1000 = 1000 && 0 < o111 && i48 <= 2
add_Load_522(iconst_1000, o169, i74, i75, o170, env, static) -{0,0}> add_Load_599(iconst_1000, o169, i74, i75, o170, env, static) :|: i74 <= 2 && i75 <= 4 && iconst_1000 = 1000 && 0 < o170 && 0 <= i75 && 0 < o169 && 0 <= i74

obtained
add_Load_599(1000, o227, i104, i105, o228, env, static) -{2,2}> add_GT_602(i105, 1000, o227, i104, o228, env, static) :|: 0 < o228 && 0 <= i104 && 0 < o227 && 0 <= i105
by chaining
add_Load_599(iconst_1000, o227, i104, i105, o228, env, static) -{1,1}> add_Load_600(i105, iconst_1000, o227, i104, o228, env, static) :|: 0 < o227 && 0 <= i105 && 0 <= i104 && iconst_1000 = 1000 && 0 < o228
add_Load_600(i105, iconst_1000, o227, i104, o228, env, static) -{1,1}> add_GT_602(i105, iconst_1000, o227, i104, o228, env, static) :|: 0 < o227 && 0 <= i105 && 0 <= i104 && iconst_1000 = 1000 && 0 < o228

obtained
add_GT_602(i113, 1000, o227, i104, o228, env, static) -{25,25}> add_Load_954(1000, 1, 0, 0, env, static) :|: 0 <= i113 && 0 <= 3 && 1000 < i113 && 0 <= i104 && 0 <= 0 && 0 < o227 && 0 <= 6 && 0 < 1 && 1001 <= i113 && 0 < o228
by chaining
add_GT_602(i113, iconst_1000, o227, i104, o228, env, static) -{0,0}> add_GT_608(i113, iconst_1000, o227, i104, o228, env, static) :|: 0 < o227 && 1001 <= i113 && 0 <= i113 && 0 <= i104 && iconst_1000 = 1000 && 0 < o228
add_GT_608(i113, iconst_1000, o227, i104, o228, env, static) -{1,1}> add_Load_624(i104, iconst_1000, o228, env, static) :|: 0 < o227 && 1001 <= i113 && iconst_1000 < i113 && 0 <= i104 && iconst_1000 = 1000 && 0 < o228
add_Load_624(i104, iconst_1000, o228, env, static) -{1,1}> add_Return_631(i104, iconst_1000, o228, env, static) :|: 0 <= i104 && iconst_1000 = 1000 && 0 < o228
add_Return_631(i104, iconst_1000, o228, env, static) -{1,1}> main_Store_637(i104, iconst_1000, o228, env, static) :|: 0 <= i104 && iconst_1000 = 1000 && 0 < o228
main_Store_637(i104, iconst_1000, o228, env, static) -{1,1}> main_New_645(iconst_1000, o228, env, static) :|: 0 <= i104 && iconst_1000 = 1000 && 0 < o228
main_New_645(iconst_1000, o228, env, static) -{0,0}> main_New_649(iconst_1000, o228, env, static) :|: iconst_1000 = 1000 && 0 < o228
main_New_649(iconst_1000, o228, env, static) -{1,1}> main_Duplicate_651(o275, iconst_1000, o228, env, static) :|: 0 < o275 && o275 = 1 && iconst_1000 = 1000 && 0 < o228
main_Duplicate_651(o275, iconst_1000, o228, env, static) -{1,1}> main_InvokeMethod_654(o275, iconst_1000, o228, env, static) :|: 0 < o275 && iconst_1000 = 1000 && 0 < o228
main_InvokeMethod_654(o275, iconst_1000, o228, env, static) -{1,1}> langle_init_rangle_Load_656(o275, iconst_1000, o228, env, static) :|: 0 < o275 && iconst_1000 = 1000 && 0 < o228
langle_init_rangle_Load_656(o275, iconst_1000, o228, env, static) -{1,1}> langle_init_rangle_InvokeMethod_659(o275, iconst_1000, o228, env, static) :|: 0 < o275 && iconst_1000 = 1000 && 0 < o228
langle_init_rangle_InvokeMethod_659(o275, iconst_1000, o228, env, static) -{1,1}> langle_init_rangle_Load_661(o275, iconst_1000, o228, env, static) :|: 0 < o275 && iconst_1000 = 1000 && 0 < o228
langle_init_rangle_Load_661(o275, iconst_1000, o228, env, static) -{1,1}> langle_init_rangle_InvokeMethod_664(o275, iconst_1000, o228, env, static) :|: 0 < o275 && iconst_1000 = 1000 && 0 < o228
langle_init_rangle_InvokeMethod_664(o275, iconst_1000, o228, env, static) -{1,1}> langle_init_rangle_Load_666(o275, iconst_1000, o228, env, static) :|: 0 < o275 && iconst_1000 = 1000 && 0 < o228
langle_init_rangle_Load_666(o275, iconst_1000, o228, env, static) -{1,1}> langle_init_rangle_InvokeMethod_673(o275, iconst_1000, o228, env, static) :|: 0 < o275 && iconst_1000 = 1000 && 0 < o228
langle_init_rangle_InvokeMethod_673(o275, iconst_1000, o228, env, static) -{1,1}> langle_init_rangle_Return_684(o275, iconst_1000, o228, env, static) :|: 0 < o275 && iconst_1000 = 1000 && 0 < o228
langle_init_rangle_Return_684(o275, iconst_1000, o228, env, static) -{1,1}> langle_init_rangle_Return_688(o275, iconst_1000, o228, env, static) :|: 0 < o275 && iconst_1000 = 1000 && 0 < o228
langle_init_rangle_Return_688(o275, iconst_1000, o228, env, static) -{1,1}> langle_init_rangle_Return_689(o275, iconst_1000, o228, env, static) :|: 0 < o275 && iconst_1000 = 1000 && 0 < o228
langle_init_rangle_Return_689(o275, iconst_1000, o228, env, static) -{1,1}> main_Store_690(o275, iconst_1000, o228, env, static) :|: 0 < o275 && iconst_1000 = 1000 && 0 < o228
main_Store_690(o275, iconst_1000, o228, env, static) -{1,1}> main_Load_691(iconst_1000, o228, o275, env, static) :|: 0 < o275 && iconst_1000 = 1000 && 0 < o228
main_Load_691(iconst_1000, o228, o275, env, static) -{1,1}> main_Load_692(o228, iconst_1000, o275, env, static) :|: 0 < o275 && iconst_1000 = 1000 && 0 < o228
main_Load_692(o228, iconst_1000, o275, env, static) -{1,1}> main_Load_693(o228, iconst_1000, o275, env, static) :|: 0 < o275 && iconst_1000 = 1000 && 0 < o228
main_Load_693(o228, iconst_1000, o275, env, static) -{1,1}> main_InvokeMethod_694(o228, iconst_1000, o275, env, static) :|: 0 < o275 && iconst_1000 = 1000 && 0 < o228
main_InvokeMethod_694(o228, iconst_1000, o275, env, static) -{1,1}> add_ConstantStackPush_695(iconst_1000, o275, env, static) :|: 0 < o275 && iconst_1000 = 1000 && 0 < o228
add_ConstantStackPush_695(iconst_1000, o275, env, static) -{1,1}> add_Store_702(iconst_0, iconst_1000, o275, env, static) :|: 0 < o275 && iconst_0 = 0 && iconst_1000 = 1000
add_Store_702(iconst_0, iconst_1000, o275, env, static) -{1,1}> add_ConstantStackPush_709(iconst_1000, o275, iconst_0, env, static) :|: 0 < o275 && iconst_0 = 0 && iconst_1000 = 1000
add_ConstantStackPush_709(iconst_1000, o275, iconst_0, env, static) -{1,1}> add_Store_715(iconst_0, iconst_1000, o275, env, static) :|: 0 < o275 && iconst_0 = 0 && iconst_1000 = 1000
add_Store_715(iconst_0, iconst_1000, o275, env, static) -{1,1}> add_Load_717(iconst_1000, o275, iconst_0, env, static) :|: 0 < o275 && iconst_0 = 0 && iconst_1000 = 1000
add_Load_717(iconst_1000, o275, iconst_0, env, static) -{0,0}> add_Load_808(iconst_1000, o275, iconst_0, iconst_0, env, static) :|: 0 <= iconst_0 && 0 < o275 && iconst_0 = 0 && iconst_1000 = 1000 && iconst_0 <= 3
add_Load_808(iconst_1000, o438, iconst_0, i194, env, static) -{0,0}> add_Load_889(iconst_1000, o438, iconst_0, i194, env, static) :|: i194 <= 3 && 0 <= iconst_0 && iconst_0 = 0 && iconst_1000 = 1000 && 0 <= i194 && 0 < o438 && iconst_0 <= 3 && i194 <= 6
add_Load_889(iconst_1000, o538, i241, i242, env, static) -{0,0}> add_Load_954(iconst_1000, o538, i241, i242, env, static) :|: i242 <= 6 && 0 < o538 && 0 <= i242 && 0 <= i241 && iconst_1000 = 1000 && i241 <= 3

obtained
add_Load_954(1000, o644, i296, i297, env, static) -{2,2}> add_GT_956(i297, 1000, o644, i296, env, static) :|: 0 < o644 && 0 <= i296 && 0 <= i297
by chaining
add_Load_954(iconst_1000, o644, i296, i297, env, static) -{1,1}> add_Load_955(i297, iconst_1000, o644, i296, env, static) :|: 0 <= i297 && iconst_1000 = 1000 && 0 <= i296 && 0 < o644
add_Load_955(i297, iconst_1000, o644, i296, env, static) -{1,1}> add_GT_956(i297, iconst_1000, o644, i296, env, static) :|: 0 <= i297 && iconst_1000 = 1000 && 0 <= i296 && 0 < o644

obtained
add_GT_956(i308, 1000, o644, i296, env, static) -{16,16}> add_Load_954(1000, o644, i334', i351', env, static) :|: 0 <= i296 && 0 < o644 && 0 <= i308 && 0 <= i334' && i308 <= 1000 && 3 <= i351' && i351' <= 1003 && 0 <= i351' && i296 + i308 = i334' && i308 + 3 = i351'
by chaining
add_GT_956(i308, iconst_1000, o644, i296, env, static) -{0,0}> add_GT_957(i308, iconst_1000, o644, i296, env, static) :|: i308 <= 1000 && 0 <= i308 && iconst_1000 = 1000 && 0 <= i296 && 0 < o644
add_GT_957(i308, iconst_1000, o644, i296, env, static) -{1,1}> add_Load_959(iconst_1000, o644, i296, i308, env, static) :|: i308 <= 1000 && i308 <= iconst_1000 && 0 <= i308 && iconst_1000 = 1000 && 0 <= i296 && 0 < o644
add_Load_959(iconst_1000, o644, i296, i308, env, static) -{1,1}> add_Load_963(i296, iconst_1000, o644, i308, env, static) :|: i308 <= 1000 && 0 <= i308 && iconst_1000 = 1000 && 0 <= i296 && 0 < o644
add_Load_963(i296, iconst_1000, o644, i308, env, static) -{1,1}> add_IntArithmetic_973(i296, i308, iconst_1000, o644, env, static) :|: i308 <= 1000 && 0 <= i308 && iconst_1000 = 1000 && 0 <= i296 && 0 < o644
add_IntArithmetic_973(i296, i308, iconst_1000, o644, env, static) -{1,1}> add_Store_981(i334, iconst_1000, o644, i308, env, static) :|: i308 <= 1000 && 0 <= i308 && iconst_1000 = 1000 && 0 <= i296 && 0 <= i334 && 0 < o644 && i296 + i308 = i334
add_Store_981(i334, iconst_1000, o644, i308, env, static) -{1,1}> add_Load_985(iconst_1000, o644, i334, i308, env, static) :|: i308 <= 1000 && 0 <= i308 && iconst_1000 = 1000 && 0 <= i334 && 0 < o644
add_Load_985(iconst_1000, o644, i334, i308, env, static) -{1,1}> add_Load_993(o644, iconst_1000, i334, i308, env, static) :|: i308 <= 1000 && 0 <= i308 && iconst_1000 = 1000 && 0 <= i334 && 0 < o644
add_Load_993(o644, iconst_1000, i334, i308, env, static) -{1,1}> add_InvokeMethod_999(o644, i308, iconst_1000, i334, env, static) :|: i308 <= 1000 && 0 <= i308 && iconst_1000 = 1000 && 0 <= i334 && 0 < o644
add_InvokeMethod_999(o644, i308, iconst_1000, i334, env, static) -{1,1}> incr_Load_1001(i308, iconst_1000, o644, i334, env, static) :|: i308 <= 1000 && 0 <= i308 && iconst_1000 = 1000 && 0 <= i334 && 0 < o644
incr_Load_1001(i308, iconst_1000, o644, i334, env, static) -{1,1}> incr_ConstantStackPush_1004(i308, iconst_1000, o644, i334, env, static) :|: i308 <= 1000 && 0 <= i308 && iconst_1000 = 1000 && 0 <= i334 && 0 < o644
incr_ConstantStackPush_1004(i308, iconst_1000, o644, i334, env, static) -{1,1}> incr_IntArithmetic_1006(i308, iconst_3, iconst_1000, o644, i334, env, static) :|: i308 <= 1000 && iconst_3 = 3 && 0 <= i308 && iconst_1000 = 1000 && 0 <= i334 && 0 < o644
incr_IntArithmetic_1006(i308, iconst_3, iconst_1000, o644, i334, env, static) -{1,1}> incr_Duplicate_1008(i351, iconst_1000, o644, i334, env, static) :|: i308 <= 1000 && i308 + iconst_3 = i351 && i351 <= 1003 && iconst_3 = 3 && 0 <= i308 && iconst_1000 = 1000 && 3 <= i351 && 0 <= i334 && 0 < o644
incr_Duplicate_1008(i351, iconst_1000, o644, i334, env, static) -{1,1}> incr_Store_1010(i351, iconst_1000, o644, i334, env, static) :|: i351 <= 1003 && iconst_1000 = 1000 && 3 <= i351 && 0 <= i334 && 0 < o644
incr_Store_1010(i351, iconst_1000, o644, i334, env, static) -{1,1}> incr_Return_1012(i351, iconst_1000, o644, i334, env, static) :|: i351 <= 1003 && iconst_1000 = 1000 && 3 <= i351 && 0 <= i334 && 0 < o644
incr_Return_1012(i351, iconst_1000, o644, i334, env, static) -{1,1}> add_Store_1013(i351, iconst_1000, o644, i334, env, static) :|: i351 <= 1003 && iconst_1000 = 1000 && 3 <= i351 && 0 <= i334 && 0 < o644
add_Store_1013(i351, iconst_1000, o644, i334, env, static) -{1,1}> add_JMP_1017(iconst_1000, o644, i334, i351, env, static) :|: i351 <= 1003 && iconst_1000 = 1000 && 3 <= i351 && 0 <= i334 && 0 < o644
add_JMP_1017(iconst_1000, o644, i334, i351, env, static) -{1,1}> add_Load_1021(iconst_1000, o644, i334, i351, env, static) :|: i351 <= 1003 && iconst_1000 = 1000 && 3 <= i351 && 0 <= i334 && 0 < o644
add_Load_1021(iconst_1000, o644, i334, i351, env, static) -{0,0}> add_Load_954(iconst_1000, o644, i334, i351, env, static) :|: i351 <= 1003 && 0 <= i351 && iconst_1000 = 1000 && 3 <= i351 && 0 <= i334 && 0 < o644

obtained
add_GT_602(i112, 1000, o227, i104, o228, env, static) -{16,16}> add_Load_599(1000, o227, i126', i135', o228, env, static) :|: 0 <= i104 && 0 <= i126' && i112 <= 1000 && 0 < o228 && 0 < o227 && 0 <= i135' && i104 + i112 = i126' && 2 <= i135' && i135' <= 1002 && 0 <= i112 && i112 + 2 = i135'
by chaining
add_GT_602(i112, iconst_1000, o227, i104, o228, env, static) -{0,0}> add_GT_607(i112, iconst_1000, o227, i104, o228, env, static) :|: 0 < o227 && 0 <= i112 && 0 <= i104 && iconst_1000 = 1000 && 0 < o228 && i112 <= 1000
add_GT_607(i112, iconst_1000, o227, i104, o228, env, static) -{1,1}> add_Load_621(iconst_1000, o227, i104, i112, o228, env, static) :|: 0 < o227 && 0 <= i112 && i112 <= iconst_1000 && 0 <= i104 && iconst_1000 = 1000 && 0 < o228 && i112 <= 1000
add_Load_621(iconst_1000, o227, i104, i112, o228, env, static) -{1,1}> add_Load_627(i104, iconst_1000, o227, i112, o228, env, static) :|: 0 < o227 && 0 <= i112 && 0 <= i104 && iconst_1000 = 1000 && 0 < o228 && i112 <= 1000
add_Load_627(i104, iconst_1000, o227, i112, o228, env, static) -{1,1}> add_IntArithmetic_636(i104, i112, iconst_1000, o227, o228, env, static) :|: 0 < o227 && 0 <= i112 && 0 <= i104 && iconst_1000 = 1000 && 0 < o228 && i112 <= 1000
add_IntArithmetic_636(i104, i112, iconst_1000, o227, o228, env, static) -{1,1}> add_Store_643(i126, iconst_1000, o227, i112, o228, env, static) :|: 0 < o227 && 0 <= i112 && 0 <= i104 && iconst_1000 = 1000 && 0 < o228 && i112 <= 1000 && 0 <= i126 && i104 + i112 = i126
add_Store_643(i126, iconst_1000, o227, i112, o228, env, static) -{1,1}> add_Load_648(iconst_1000, o227, i126, i112, o228, env, static) :|: 0 < o227 && 0 <= i112 && iconst_1000 = 1000 && 0 < o228 && 0 <= i126 && i112 <= 1000
add_Load_648(iconst_1000, o227, i126, i112, o228, env, static) -{1,1}> add_Load_650(o227, iconst_1000, i126, i112, o228, env, static) :|: 0 < o227 && 0 <= i112 && iconst_1000 = 1000 && 0 < o228 && 0 <= i126 && i112 <= 1000
add_Load_650(o227, iconst_1000, i126, i112, o228, env, static) -{1,1}> add_InvokeMethod_653(o227, i112, iconst_1000, i126, o228, env, static) :|: 0 < o227 && 0 <= i112 && iconst_1000 = 1000 && 0 < o228 && 0 <= i126 && i112 <= 1000
add_InvokeMethod_653(o227, i112, iconst_1000, i126, o228, env, static) -{1,1}> incr_Load_655(i112, iconst_1000, o227, i126, o228, env, static) :|: 0 < o227 && 0 <= i112 && iconst_1000 = 1000 && 0 < o228 && i112 <= 1000 && 0 <= i126
incr_Load_655(i112, iconst_1000, o227, i126, o228, env, static) -{1,1}> incr_ConstantStackPush_658(i112, iconst_1000, o227, i126, o228, env, static) :|: 0 < o227 && 0 <= i112 && iconst_1000 = 1000 && 0 < o228 && i112 <= 1000 && 0 <= i126
incr_ConstantStackPush_658(i112, iconst_1000, o227, i126, o228, env, static) -{1,1}> incr_IntArithmetic_660(i112, iconst_2, iconst_1000, o227, i126, o228, env, static) :|: 0 < o227 && 0 <= i112 && iconst_1000 = 1000 && 0 < o228 && i112 <= 1000 && 0 <= i126 && iconst_2 = 2
incr_IntArithmetic_660(i112, iconst_2, iconst_1000, o227, i126, o228, env, static) -{1,1}> incr_Duplicate_662(i135, iconst_1000, o227, i126, o228, env, static) :|: i112 + iconst_2 = i135 && 0 < o227 && i135 <= 1002 && 0 <= i112 && 2 <= i135 && iconst_1000 = 1000 && 0 < o228 && i112 <= 1000 && 0 <= i126 && iconst_2 = 2
incr_Duplicate_662(i135, iconst_1000, o227, i126, o228, env, static) -{1,1}> incr_Store_663(i135, iconst_1000, o227, i126, o228, env, static) :|: i135 <= 1002 && 0 < o227 && 2 <= i135 && iconst_1000 = 1000 && 0 < o228 && 0 <= i126
incr_Store_663(i135, iconst_1000, o227, i126, o228, env, static) -{1,1}> incr_Return_665(i135, iconst_1000, o227, i126, o228, env, static) :|: i135 <= 1002 && 0 < o227 && 2 <= i135 && iconst_1000 = 1000 && 0 < o228 && 0 <= i126
incr_Return_665(i135, iconst_1000, o227, i126, o228, env, static) -{1,1}> add_Store_667(i135, iconst_1000, o227, i126, o228, env, static) :|: i135 <= 1002 && 0 < o227 && 2 <= i135 && iconst_1000 = 1000 && 0 < o228 && 0 <= i126
add_Store_667(i135, iconst_1000, o227, i126, o228, env, static) -{1,1}> add_JMP_668(iconst_1000, o227, i126, i135, o228, env, static) :|: i135 <= 1002 && 0 < o227 && 2 <= i135 && iconst_1000 = 1000 && 0 < o228 && 0 <= i126
add_JMP_668(iconst_1000, o227, i126, i135, o228, env, static) -{1,1}> add_Load_678(iconst_1000, o227, i126, i135, o228, env, static) :|: 0 < o227 && i135 <= 1002 && 2 <= i135 && iconst_1000 = 1000 && 0 < o228 && 0 <= i126
add_Load_678(iconst_1000, o227, i126, i135, o228, env, static) -{0,0}> add_Load_599(iconst_1000, o227, i126, i135, o228, env, static) :|: 0 < o227 && i135 <= 1002 && 2 <= i135 && iconst_1000 = 1000 && 0 <= i135 && 0 < o228 && 0 <= i126

obtained
add_GT_299(i18, 1000, o30, i10, o31, env, static) -{16,16}> add_Load_283(1000, o30, i20', i21', o31, env, static) :|: i18 <= 1000 && i18 + 1 = i21' && i21' <= 1001 && 0 <= i20' && 0 < o31 && 0 < o30 && 0 <= i21' && 0 <= i18 && 1 <= i21' && i10 + i18 = i20' && 0 <= i10
by chaining
add_GT_299(i18, iconst_1000, o30, i10, o31, env, static) -{0,0}> add_GT_304(i18, iconst_1000, o30, i10, o31, env, static) :|: 0 <= i10 && 0 <= i18 && i18 <= 1000 && 0 < o30 && 0 < o31 && iconst_1000 = 1000
add_GT_304(i18, iconst_1000, o30, i10, o31, env, static) -{1,1}> add_Load_309(iconst_1000, o30, i10, i18, o31, env, static) :|: 0 <= i10 && 0 <= i18 && i18 <= 1000 && 0 < o30 && i18 <= iconst_1000 && 0 < o31 && iconst_1000 = 1000
add_Load_309(iconst_1000, o30, i10, i18, o31, env, static) -{1,1}> add_Load_319(i10, iconst_1000, o30, i18, o31, env, static) :|: 0 <= i10 && 0 <= i18 && i18 <= 1000 && 0 < o30 && 0 < o31 && iconst_1000 = 1000
add_Load_319(i10, iconst_1000, o30, i18, o31, env, static) -{1,1}> add_IntArithmetic_323(i10, i18, iconst_1000, o30, o31, env, static) :|: 0 <= i10 && 0 <= i18 && i18 <= 1000 && 0 < o30 && 0 < o31 && iconst_1000 = 1000
add_IntArithmetic_323(i10, i18, iconst_1000, o30, o31, env, static) -{1,1}> add_Store_328(i20, iconst_1000, o30, i18, o31, env, static) :|: 0 <= i10 && 0 <= i18 && i18 <= 1000 && 0 <= i20 && 0 < o30 && 0 < o31 && iconst_1000 = 1000 && i10 + i18 = i20
add_Store_328(i20, iconst_1000, o30, i18, o31, env, static) -{1,1}> add_Load_332(iconst_1000, o30, i20, i18, o31, env, static) :|: 0 <= i18 && 0 <= i20 && i18 <= 1000 && 0 < o30 && 0 < o31 && iconst_1000 = 1000
add_Load_332(iconst_1000, o30, i20, i18, o31, env, static) -{1,1}> add_Load_334(o30, iconst_1000, i20, i18, o31, env, static) :|: 0 <= i18 && 0 <= i20 && i18 <= 1000 && 0 < o30 && 0 < o31 && iconst_1000 = 1000
add_Load_334(o30, iconst_1000, i20, i18, o31, env, static) -{1,1}> add_InvokeMethod_336(o30, i18, iconst_1000, i20, o31, env, static) :|: 0 <= i18 && 0 <= i20 && i18 <= 1000 && 0 < o30 && 0 < o31 && iconst_1000 = 1000
add_InvokeMethod_336(o30, i18, iconst_1000, i20, o31, env, static) -{1,1}> incr_Load_338(i18, iconst_1000, o30, i20, o31, env, static) :|: 0 <= i18 && i18 <= 1000 && 0 <= i20 && 0 < o30 && 0 < o31 && iconst_1000 = 1000
incr_Load_338(i18, iconst_1000, o30, i20, o31, env, static) -{1,1}> incr_ConstantStackPush_340(i18, iconst_1000, o30, i20, o31, env, static) :|: 0 <= i18 && i18 <= 1000 && 0 <= i20 && 0 < o30 && 0 < o31 && iconst_1000 = 1000
incr_ConstantStackPush_340(i18, iconst_1000, o30, i20, o31, env, static) -{1,1}> incr_IntArithmetic_343(i18, iconst_1, iconst_1000, o30, i20, o31, env, static) :|: 0 <= i18 && i18 <= 1000 && 0 <= i20 && 0 < o30 && 0 < o31 && iconst_1 = 1 && iconst_1000 = 1000
incr_IntArithmetic_343(i18, iconst_1, iconst_1000, o30, i20, o31, env, static) -{1,1}> incr_Duplicate_346(i21, iconst_1000, o30, i20, o31, env, static) :|: 1 <= i21 && 0 <= i18 && i18 <= 1000 && 0 <= i20 && 0 < o30 && 0 < o31 && i21 <= 1001 && iconst_1 = 1 && i18 + iconst_1 = i21 && iconst_1000 = 1000
incr_Duplicate_346(i21, iconst_1000, o30, i20, o31, env, static) -{1,1}> incr_Store_348(i21, iconst_1000, o30, i20, o31, env, static) :|: 1 <= i21 && 0 <= i20 && 0 < o30 && 0 < o31 && i21 <= 1001 && iconst_1000 = 1000
incr_Store_348(i21, iconst_1000, o30, i20, o31, env, static) -{1,1}> incr_Return_353(i21, iconst_1000, o30, i20, o31, env, static) :|: 1 <= i21 && 0 <= i20 && 0 < o30 && 0 < o31 && i21 <= 1001 && iconst_1000 = 1000
incr_Return_353(i21, iconst_1000, o30, i20, o31, env, static) -{1,1}> add_Store_359(i21, iconst_1000, o30, i20, o31, env, static) :|: 1 <= i21 && 0 <= i20 && 0 < o30 && 0 < o31 && i21 <= 1001 && iconst_1000 = 1000
add_Store_359(i21, iconst_1000, o30, i20, o31, env, static) -{1,1}> add_JMP_363(iconst_1000, o30, i20, i21, o31, env, static) :|: 1 <= i21 && 0 <= i20 && 0 < o30 && 0 < o31 && i21 <= 1001 && iconst_1000 = 1000
add_JMP_363(iconst_1000, o30, i20, i21, o31, env, static) -{1,1}> add_Load_370(iconst_1000, o30, i20, i21, o31, env, static) :|: 1 <= i21 && 0 <= i20 && 0 < o30 && 0 < o31 && i21 <= 1001 && iconst_1000 = 1000
add_Load_370(iconst_1000, o30, i20, i21, o31, env, static) -{0,0}> add_Load_283(iconst_1000, o30, i20, i21, o31, env, static) :|: 1 <= i21 && 0 <= i20 && 0 < o30 && 0 <= i21 && 0 < o31 && i21 <= 1001 && iconst_1000 = 1000

(8) Obligation:

IntTrs with 10 rules
Start term: main_ConstantStackPush_2(env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_ConstantStackPush_2(env, static) -{39,39}> add_Load_283(1000, 1, 0, 0, 1, env, static'1) :|: 0 >= 0 && 0 <= 1 && 0 < 2 && 0 <= 0 && 0 <= static'1 && 0 <= static && 0 < 1 && 0 <= 2 && static''' <= static + 2 && 0 <= static''' && static'1 <= static''' + 1
add_Load_283(1000, o30, i10, i11, o31, env, static) -{2,2}> add_GT_299(i11, 1000, o30, i10, o31, env, static) :|: 0 < o31 && 0 <= i11 && 0 <= i10 && 0 < o30
add_GT_299(i19, 1000, o30, i10, o31, env, static) -{22,22}> add_Load_599(1000, 1, 0, 0, o31, env, static) :|: 1001 <= i19 && 0 <= 0 && 0 < o30 && 0 < 1 && 0 <= i10 && 0 <= 4 && 0 < o31 && 0 <= 2 && 0 <= i19 && 1000 < i19
add_Load_599(1000, o227, i104, i105, o228, env, static) -{2,2}> add_GT_602(i105, 1000, o227, i104, o228, env, static) :|: 0 < o228 && 0 <= i104 && 0 < o227 && 0 <= i105
add_GT_602(i113, 1000, o227, i104, o228, env, static) -{25,25}> add_Load_954(1000, 1, 0, 0, env, static) :|: 0 <= i113 && 0 <= 3 && 1000 < i113 && 0 <= i104 && 0 <= 0 && 0 < o227 && 0 <= 6 && 0 < 1 && 1001 <= i113 && 0 < o228
add_Load_954(1000, o644, i296, i297, env, static) -{2,2}> add_GT_956(i297, 1000, o644, i296, env, static) :|: 0 < o644 && 0 <= i296 && 0 <= i297
add_GT_956(i309, iconst_1000, o644, i296, env, static) -{0,0}> add_GT_958(i309, iconst_1000, o644, i296, env, static) :|: 1001 <= i309 && 0 <= i309 && iconst_1000 = 1000 && 0 <= i296 && 0 < o644
add_GT_956(i308, 1000, o644, i296, env, static) -{16,16}> add_Load_954(1000, o644, i334', i351', env, static) :|: 0 <= i296 && 0 < o644 && 0 <= i308 && 0 <= i334' && i308 <= 1000 && 3 <= i351' && i351' <= 1003 && 0 <= i351' && i296 + i308 = i334' && i308 + 3 = i351'
add_GT_602(i112, 1000, o227, i104, o228, env, static) -{16,16}> add_Load_599(1000, o227, i126', i135', o228, env, static) :|: 0 <= i104 && 0 <= i126' && i112 <= 1000 && 0 < o228 && 0 < o227 && 0 <= i135' && i104 + i112 = i126' && 2 <= i135' && i135' <= 1002 && 0 <= i112 && i112 + 2 = i135'
add_GT_299(i18, 1000, o30, i10, o31, env, static) -{16,16}> add_Load_283(1000, o30, i20', i21', o31, env, static) :|: i18 <= 1000 && i18 + 1 = i21' && i21' <= 1001 && 0 <= i20' && 0 < o31 && 0 < o30 && 0 <= i21' && 0 <= i18 && 1 <= i21' && i10 + i18 = i20' && 0 <= i10

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

Moved arithmethic from lhss to constraints.

add_GT_602(i113, 1000, o227, i104, o228, env, static) -{25,25}> add_Load_954(1000, 1, 0, 0, env, static) :|: 0 <= i113 && 0 <= 3 && 1000 < i113 && 0 <= i104 && 0 <= 0 && 0 < o227 && 0 <= 6 && 0 < 1 && 1001 <= i113 && 0 < o228
was transformed to
add_GT_602(i113, x, o227, i104, o228, env, static) -{25,25}> add_Load_954(1000, 1, 0, 0, env, static) :|: 0 <= i113 && 0 <= 3 && 1000 < i113 && 0 <= i104 && 0 <= 0 && 0 < o227 && 0 <= 6 && 0 < 1 && 1001 <= i113 && 0 < o228 && x = 1000

add_GT_299(i18, 1000, o30, i10, o31, env, static) -{16,16}> add_Load_283(1000, o30, i20', i21', o31, env, static) :|: i18 <= 1000 && i18 + 1 = i21' && i21' <= 1001 && 0 <= i20' && 0 < o31 && 0 < o30 && 0 <= i21' && 0 <= i18 && 1 <= i21' && i10 + i18 = i20' && 0 <= i10
was transformed to
add_GT_299(i18, x, o30, i10, o31, env, static) -{16,16}> add_Load_283(1000, o30, i20', i21', o31, env, static) :|: i18 <= 1000 && i18 + 1 = i21' && i21' <= 1001 && 0 <= i20' && 0 < o31 && 0 < o30 && 0 <= i21' && 0 <= i18 && 1 <= i21' && i10 + i18 = i20' && 0 <= i10 && x = 1000

add_Load_599(1000, o227, i104, i105, o228, env, static) -{2,2}> add_GT_602(i105, 1000, o227, i104, o228, env, static) :|: 0 < o228 && 0 <= i104 && 0 < o227 && 0 <= i105
was transformed to
add_Load_599(x, o227, i104, i105, o228, env, static) -{2,2}> add_GT_602(i105, 1000, o227, i104, o228, env, static) :|: 0 < o228 && 0 <= i104 && 0 < o227 && 0 <= i105 && x = 1000

add_GT_299(i19, 1000, o30, i10, o31, env, static) -{22,22}> add_Load_599(1000, 1, 0, 0, o31, env, static) :|: 1001 <= i19 && 0 <= 0 && 0 < o30 && 0 < 1 && 0 <= i10 && 0 <= 4 && 0 < o31 && 0 <= 2 && 0 <= i19 && 1000 < i19
was transformed to
add_GT_299(i19, x, o30, i10, o31, env, static) -{22,22}> add_Load_599(1000, 1, 0, 0, o31, env, static) :|: 1001 <= i19 && 0 <= 0 && 0 < o30 && 0 < 1 && 0 <= i10 && 0 <= 4 && 0 < o31 && 0 <= 2 && 0 <= i19 && 1000 < i19 && x = 1000

add_Load_283(1000, o30, i10, i11, o31, env, static) -{2,2}> add_GT_299(i11, 1000, o30, i10, o31, env, static) :|: 0 < o31 && 0 <= i11 && 0 <= i10 && 0 < o30
was transformed to
add_Load_283(x, o30, i10, i11, o31, env, static) -{2,2}> add_GT_299(i11, 1000, o30, i10, o31, env, static) :|: 0 < o31 && 0 <= i11 && 0 <= i10 && 0 < o30 && x = 1000

add_GT_602(i112, 1000, o227, i104, o228, env, static) -{16,16}> add_Load_599(1000, o227, i126', i135', o228, env, static) :|: 0 <= i104 && 0 <= i126' && i112 <= 1000 && 0 < o228 && 0 < o227 && 0 <= i135' && i104 + i112 = i126' && 2 <= i135' && i135' <= 1002 && 0 <= i112 && i112 + 2 = i135'
was transformed to
add_GT_602(i112, x, o227, i104, o228, env, static) -{16,16}> add_Load_599(1000, o227, i126', i135', o228, env, static) :|: 0 <= i104 && 0 <= i126' && i112 <= 1000 && 0 < o228 && 0 < o227 && 0 <= i135' && i104 + i112 = i126' && 2 <= i135' && i135' <= 1002 && 0 <= i112 && i112 + 2 = i135' && x = 1000

add_GT_956(i308, 1000, o644, i296, env, static) -{16,16}> add_Load_954(1000, o644, i334', i351', env, static) :|: 0 <= i296 && 0 < o644 && 0 <= i308 && 0 <= i334' && i308 <= 1000 && 3 <= i351' && i351' <= 1003 && 0 <= i351' && i296 + i308 = i334' && i308 + 3 = i351'
was transformed to
add_GT_956(i308, x, o644, i296, env, static) -{16,16}> add_Load_954(1000, o644, i334', i351', env, static) :|: 0 <= i296 && 0 < o644 && 0 <= i308 && 0 <= i334' && i308 <= 1000 && 3 <= i351' && i351' <= 1003 && 0 <= i351' && i296 + i308 = i334' && i308 + 3 = i351' && x = 1000

add_Load_954(1000, o644, i296, i297, env, static) -{2,2}> add_GT_956(i297, 1000, o644, i296, env, static) :|: 0 < o644 && 0 <= i296 && 0 <= i297
was transformed to
add_Load_954(x, o644, i296, i297, env, static) -{2,2}> add_GT_956(i297, 1000, o644, i296, env, static) :|: 0 < o644 && 0 <= i296 && 0 <= i297 && x = 1000

(10) Obligation:

IntTrs with 10 rules
Start term: main_ConstantStackPush_2(env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
add_GT_602(i113, x, o227, i104, o228, env, static) -{25,25}> add_Load_954(1000, 1, 0, 0, env, static) :|: 0 <= i113 && 0 <= 3 && 1000 < i113 && 0 <= i104 && 0 <= 0 && 0 < o227 && 0 <= 6 && 0 < 1 && 1001 <= i113 && 0 < o228 && x = 1000
add_GT_299(i18, x, o30, i10, o31, env, static) -{16,16}> add_Load_283(1000, o30, i20', i21', o31, env, static) :|: i18 <= 1000 && i18 + 1 = i21' && i21' <= 1001 && 0 <= i20' && 0 < o31 && 0 < o30 && 0 <= i21' && 0 <= i18 && 1 <= i21' && i10 + i18 = i20' && 0 <= i10 && x = 1000
main_ConstantStackPush_2(env, static) -{39,39}> add_Load_283(1000, 1, 0, 0, 1, env, static'1) :|: 0 >= 0 && 0 <= 1 && 0 < 2 && 0 <= 0 && 0 <= static'1 && 0 <= static && 0 < 1 && 0 <= 2 && static''' <= static + 2 && 0 <= static''' && static'1 <= static''' + 1
add_Load_599(x, o227, i104, i105, o228, env, static) -{2,2}> add_GT_602(i105, 1000, o227, i104, o228, env, static) :|: 0 < o228 && 0 <= i104 && 0 < o227 && 0 <= i105 && x = 1000
add_GT_299(i19, x, o30, i10, o31, env, static) -{22,22}> add_Load_599(1000, 1, 0, 0, o31, env, static) :|: 1001 <= i19 && 0 <= 0 && 0 < o30 && 0 < 1 && 0 <= i10 && 0 <= 4 && 0 < o31 && 0 <= 2 && 0 <= i19 && 1000 < i19 && x = 1000
add_Load_283(x, o30, i10, i11, o31, env, static) -{2,2}> add_GT_299(i11, 1000, o30, i10, o31, env, static) :|: 0 < o31 && 0 <= i11 && 0 <= i10 && 0 < o30 && x = 1000
add_GT_602(i112, x, o227, i104, o228, env, static) -{16,16}> add_Load_599(1000, o227, i126', i135', o228, env, static) :|: 0 <= i104 && 0 <= i126' && i112 <= 1000 && 0 < o228 && 0 < o227 && 0 <= i135' && i104 + i112 = i126' && 2 <= i135' && i135' <= 1002 && 0 <= i112 && i112 + 2 = i135' && x = 1000
add_GT_956(i308, x, o644, i296, env, static) -{16,16}> add_Load_954(1000, o644, i334', i351', env, static) :|: 0 <= i296 && 0 < o644 && 0 <= i308 && 0 <= i334' && i308 <= 1000 && 3 <= i351' && i351' <= 1003 && 0 <= i351' && i296 + i308 = i334' && i308 + 3 = i351' && x = 1000
add_GT_956(i309, iconst_1000, o644, i296, env, static) -{0,0}> add_GT_958(i309, iconst_1000, o644, i296, env, static) :|: 1001 <= i309 && 0 <= i309 && iconst_1000 = 1000 && 0 <= i296 && 0 < o644
add_Load_954(x, o644, i296, i297, env, static) -{2,2}> add_GT_956(i297, 1000, o644, i296, env, static) :|: 0 < o644 && 0 <= i296 && 0 <= i297 && x = 1000

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

Moved arithmethic from constraints to rhss.

add_GT_299(i18, x, o30, i10, o31, env, static) -{16,16}> add_Load_283(1000, o30, i20', i21', o31, env, static) :|: i18 <= 1000 && i18 + 1 = i21' && i21' <= 1001 && 0 <= i20' && 0 < o31 && 0 < o30 && 0 <= i21' && 0 <= i18 && 1 <= i21' && i10 + i18 = i20' && 0 <= i10 && x = 1000
was transformed to
add_GT_299(i18, x, o30, i10, o31, env, static) -{16,16}> add_Load_283(1000, o30, i10 + i18, i18 + 1, o31, env, static) :|: i18 <= 1000 && i18 + 1 = i21' && i21' <= 1001 && 0 <= i20' && 0 < o31 && 0 < o30 && 0 <= i21' && 0 <= i18 && 1 <= i21' && i10 + i18 = i20' && 0 <= i10 && x = 1000

add_GT_602(i112, x, o227, i104, o228, env, static) -{16,16}> add_Load_599(1000, o227, i126', i135', o228, env, static) :|: 0 <= i104 && 0 <= i126' && i112 <= 1000 && 0 < o228 && 0 < o227 && 0 <= i135' && i104 + i112 = i126' && 2 <= i135' && i135' <= 1002 && 0 <= i112 && i112 + 2 = i135' && x = 1000
was transformed to
add_GT_602(i112, x, o227, i104, o228, env, static) -{16,16}> add_Load_599(1000, o227, i104 + i112, i112 + 2, o228, env, static) :|: 0 <= i104 && 0 <= i126' && i112 <= 1000 && 0 < o228 && 0 < o227 && 0 <= i135' && i104 + i112 = i126' && 2 <= i135' && i135' <= 1002 && 0 <= i112 && i112 + 2 = i135' && x = 1000

add_GT_956(i309, iconst_1000, o644, i296, env, static) -{0,0}> add_GT_958(i309, iconst_1000, o644, i296, env, static) :|: 1001 <= i309 && 0 <= i309 && iconst_1000 = 1000 && 0 <= i296 && 0 < o644
was transformed to
add_GT_956(i309, iconst_1000, o644, i296, env, static) -{0,0}> add_GT_958(i309, 1000, o644, i296, env, static) :|: 1001 <= i309 && 0 <= i309 && iconst_1000 = 1000 && 0 <= i296 && 0 < o644

add_GT_956(i308, x, o644, i296, env, static) -{16,16}> add_Load_954(1000, o644, i334', i351', env, static) :|: 0 <= i296 && 0 < o644 && 0 <= i308 && 0 <= i334' && i308 <= 1000 && 3 <= i351' && i351' <= 1003 && 0 <= i351' && i296 + i308 = i334' && i308 + 3 = i351' && x = 1000
was transformed to
add_GT_956(i308, x, o644, i296, env, static) -{16,16}> add_Load_954(1000, o644, i296 + i308, i308 + 3, env, static) :|: 0 <= i296 && 0 < o644 && 0 <= i308 && 0 <= i334' && i308 <= 1000 && 3 <= i351' && i351' <= 1003 && 0 <= i351' && i296 + i308 = i334' && i308 + 3 = i351' && x = 1000

(12) Obligation:

IntTrs with 10 rules
Start term: main_ConstantStackPush_2(env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
add_Load_954(x, o644, i296, i297, env, static) -{2,2}> add_GT_956(i297, 1000, o644, i296, env, static) :|: 0 < o644 && 0 <= i296 && 0 <= i297 && x = 1000
add_GT_299(i18, x, o30, i10, o31, env, static) -{16,16}> add_Load_283(1000, o30, i10 + i18, i18 + 1, o31, env, static) :|: i18 <= 1000 && i18 + 1 = i21' && i21' <= 1001 && 0 <= i20' && 0 < o31 && 0 < o30 && 0 <= i21' && 0 <= i18 && 1 <= i21' && i10 + i18 = i20' && 0 <= i10 && x = 1000
main_ConstantStackPush_2(env, static) -{39,39}> add_Load_283(1000, 1, 0, 0, 1, env, static'1) :|: 0 >= 0 && 0 <= 1 && 0 < 2 && 0 <= 0 && 0 <= static'1 && 0 <= static && 0 < 1 && 0 <= 2 && static''' <= static + 2 && 0 <= static''' && static'1 <= static''' + 1
add_GT_602(i112, x, o227, i104, o228, env, static) -{16,16}> add_Load_599(1000, o227, i104 + i112, i112 + 2, o228, env, static) :|: 0 <= i104 && 0 <= i126' && i112 <= 1000 && 0 < o228 && 0 < o227 && 0 <= i135' && i104 + i112 = i126' && 2 <= i135' && i135' <= 1002 && 0 <= i112 && i112 + 2 = i135' && x = 1000
add_Load_599(x, o227, i104, i105, o228, env, static) -{2,2}> add_GT_602(i105, 1000, o227, i104, o228, env, static) :|: 0 < o228 && 0 <= i104 && 0 < o227 && 0 <= i105 && x = 1000
add_GT_602(i113, x, o227, i104, o228, env, static) -{25,25}> add_Load_954(1000, 1, 0, 0, env, static) :|: 0 <= i113 && 0 <= 3 && 1000 < i113 && 0 <= i104 && 0 <= 0 && 0 < o227 && 0 <= 6 && 0 < 1 && 1001 <= i113 && 0 < o228 && x = 1000
add_GT_299(i19, x, o30, i10, o31, env, static) -{22,22}> add_Load_599(1000, 1, 0, 0, o31, env, static) :|: 1001 <= i19 && 0 <= 0 && 0 < o30 && 0 < 1 && 0 <= i10 && 0 <= 4 && 0 < o31 && 0 <= 2 && 0 <= i19 && 1000 < i19 && x = 1000
add_GT_956(i309, iconst_1000, o644, i296, env, static) -{0,0}> add_GT_958(i309, 1000, o644, i296, env, static) :|: 1001 <= i309 && 0 <= i309 && iconst_1000 = 1000 && 0 <= i296 && 0 < o644
add_GT_956(i308, x, o644, i296, env, static) -{16,16}> add_Load_954(1000, o644, i296 + i308, i308 + 3, env, static) :|: 0 <= i296 && 0 < o644 && 0 <= i308 && 0 <= i334' && i308 <= 1000 && 3 <= i351' && i351' <= 1003 && 0 <= i351' && i296 + i308 = i334' && i308 + 3 = i351' && x = 1000
add_Load_283(x, o30, i10, i11, o31, env, static) -{2,2}> add_GT_299(i11, 1000, o30, i10, o31, env, static) :|: 0 < o31 && 0 <= i11 && 0 <= i10 && 0 < o30 && x = 1000

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

Simplified expressions.

main_ConstantStackPush_2(env, static) -{39,39}> add_Load_283(1000, 1, 0, 0, 1, env, static'1) :|: 0 >= 0 && 0 <= 1 && 0 < 2 && 0 <= 0 && 0 <= static'1 && 0 <= static && 0 < 1 && 0 <= 2 && static''' <= static + 2 && 0 <= static''' && static'1 <= static''' + 1
was transformed to
main_ConstantStackPush_2(env, static) -{39,39}> add_Load_283(1000, 1, 0, 0, 1, env, static'1) :|: 0 <= static'1 && 0 <= static && static''' <= static + 2 && 0 <= static''' && static'1 <= static''' + 1

add_GT_602(i113, x, o227, i104, o228, env, static) -{25,25}> add_Load_954(1000, 1, 0, 0, env, static) :|: 0 <= i113 && 0 <= 3 && 1000 < i113 && 0 <= i104 && 0 <= 0 && 0 < o227 && 0 <= 6 && 0 < 1 && 1001 <= i113 && 0 < o228 && x = 1000
was transformed to
add_GT_602(i113, x, o227, i104, o228, env, static) -{25,25}> add_Load_954(1000, 1, 0, 0, env, static) :|: 0 <= i113 && 1000 < i113 && 0 <= i104 && 0 < o227 && 1001 <= i113 && 0 < o228 && x = 1000

add_GT_299(i19, x, o30, i10, o31, env, static) -{22,22}> add_Load_599(1000, 1, 0, 0, o31, env, static) :|: 1001 <= i19 && 0 <= 0 && 0 < o30 && 0 < 1 && 0 <= i10 && 0 <= 4 && 0 < o31 && 0 <= 2 && 0 <= i19 && 1000 < i19 && x = 1000
was transformed to
add_GT_299(i19, x, o30, i10, o31, env, static) -{22,22}> add_Load_599(1000, 1, 0, 0, o31, env, static) :|: 1001 <= i19 && 0 < o30 && 0 <= i10 && 0 < o31 && 0 <= i19 && 1000 < i19 && x = 1000

(14) Obligation:

IntTrs with 10 rules
Start term: main_ConstantStackPush_2(env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
add_GT_299(i18, x, o30, i10, o31, env, static) -{16,16}> add_Load_283(1000, o30, i10 + i18, i18 + 1, o31, env, static) :|: i18 <= 1000 && i18 + 1 = i21' && i21' <= 1001 && 0 <= i20' && 0 < o31 && 0 < o30 && 0 <= i21' && 0 <= i18 && 1 <= i21' && i10 + i18 = i20' && 0 <= i10 && x = 1000
add_Load_954(x, o644, i296, i297, env, static) -{2,2}> add_GT_956(i297, 1000, o644, i296, env, static) :|: 0 < o644 && 0 <= i296 && 0 <= i297 && x = 1000
main_ConstantStackPush_2(env, static) -{39,39}> add_Load_283(1000, 1, 0, 0, 1, env, static'1) :|: 0 <= static'1 && 0 <= static && static''' <= static + 2 && 0 <= static''' && static'1 <= static''' + 1
add_GT_602(i113, x, o227, i104, o228, env, static) -{25,25}> add_Load_954(1000, 1, 0, 0, env, static) :|: 0 <= i113 && 1000 < i113 && 0 <= i104 && 0 < o227 && 1001 <= i113 && 0 < o228 && x = 1000
add_GT_602(i112, x, o227, i104, o228, env, static) -{16,16}> add_Load_599(1000, o227, i104 + i112, i112 + 2, o228, env, static) :|: 0 <= i104 && 0 <= i126' && i112 <= 1000 && 0 < o228 && 0 < o227 && 0 <= i135' && i104 + i112 = i126' && 2 <= i135' && i135' <= 1002 && 0 <= i112 && i112 + 2 = i135' && x = 1000
add_Load_599(x, o227, i104, i105, o228, env, static) -{2,2}> add_GT_602(i105, 1000, o227, i104, o228, env, static) :|: 0 < o228 && 0 <= i104 && 0 < o227 && 0 <= i105 && x = 1000
add_GT_956(i309, iconst_1000, o644, i296, env, static) -{0,0}> add_GT_958(i309, 1000, o644, i296, env, static) :|: 1001 <= i309 && 0 <= i309 && iconst_1000 = 1000 && 0 <= i296 && 0 < o644
add_GT_299(i19, x, o30, i10, o31, env, static) -{22,22}> add_Load_599(1000, 1, 0, 0, o31, env, static) :|: 1001 <= i19 && 0 < o30 && 0 <= i10 && 0 < o31 && 0 <= i19 && 1000 < i19 && x = 1000
add_Load_283(x, o30, i10, i11, o31, env, static) -{2,2}> add_GT_299(i11, 1000, o30, i10, o31, env, static) :|: 0 < o31 && 0 <= i11 && 0 <= i10 && 0 < o30 && x = 1000
add_GT_956(i308, x, o644, i296, env, static) -{16,16}> add_Load_954(1000, o644, i296 + i308, i308 + 3, env, static) :|: 0 <= i296 && 0 < o644 && 0 <= i308 && 0 <= i334' && i308 <= 1000 && 3 <= i351' && i351' <= 1003 && 0 <= i351' && i296 + i308 = i334' && i308 + 3 = i351' && x = 1000

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

Transformed 169 jbc graph edges to a weighted ITS with 169 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) TerminationGraphToComplexityProof (BOTH CONCRETE BOUNDS(ID, ADD(5)) transformation)

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

(26) Obligation:

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

Used field analysis yielded the following read fields:

Considered paths: all paths from start

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

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

(28) Obligation:

IntTrs with 168 rules
Start term: main_ConstantStackPush_2(env, static)
Considered paths: all paths from start
Rules:
main_ConstantStackPush_2(env, static) -{0,0}> main_ConstantStackPush_4(env, static) :|: 0 >= 0
main_ConstantStackPush_4(env, static) -{0,0}> langle_clinit_rangle_ConstantStackPush_6(env, static) :|: 0 >= 0
langle_clinit_rangle_ConstantStackPush_6(env, static) -{1,1}> langle_clinit_rangle_ArrayCreate_13(iconst_0, env, static) :|: iconst_0 = 0
langle_clinit_rangle_ArrayCreate_13(iconst_0, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_16(a2, iconst_0, env, static) :|: a2 = 2 && iconst_0 = 0 && 0 < a2
langle_clinit_rangle_FieldAccess_16(a2, iconst_0, env, static) -{1,1}> langle_clinit_rangle_New_17(env, static') :|: 0 <= a2 && iconst_0 = 0 && static' <= static + a2 && 0 <= static && 0 < a2
langle_clinit_rangle_New_17(env, static) -{0,0}> langle_clinit_rangle_New_18(env, static) :|: 0 >= 0
langle_clinit_rangle_New_18(env, static) -{0,0}> langle_clinit_rangle_New_20(env, static) :|: 0 <= static
langle_clinit_rangle_New_20(env, static) -{1,1}> langle_clinit_rangle_Duplicate_21(o2, env, static) :|: 0 < o2 && o2 = 1
langle_clinit_rangle_Duplicate_21(o2, env, static) -{1,1}> langle_clinit_rangle_ConstantStackPush_23(o2, env, static) :|: 0 < o2
langle_clinit_rangle_ConstantStackPush_23(o2, env, static) -{1,1}> langle_clinit_rangle_InvokeMethod_25(o2, NULL, env, static) :|: NULL = 0 && 0 < o2
langle_clinit_rangle_InvokeMethod_25(o2, NULL, env, static) -{1,1}> langle_init_rangle_Load_27(o2, env, static) :|: NULL = 0 && 0 < o2
langle_init_rangle_Load_27(o2, env, static) -{1,1}> langle_init_rangle_InvokeMethod_29(o2, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_29(o2, env, static) -{1,1}> langle_init_rangle_Load_31(o2, env, static) :|: 0 < o2
langle_init_rangle_Load_31(o2, env, static) -{1,1}> langle_init_rangle_InvokeMethod_33(o2, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_33(o2, env, static) -{1,1}> langle_init_rangle_Return_36(o2, env, static) :|: 0 < o2
langle_init_rangle_Return_36(o2, env, static) -{1,1}> langle_init_rangle_Return_38(o2, env, static) :|: 0 < o2
langle_init_rangle_Return_38(o2, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_39(o2, env, static) :|: 0 < o2
langle_clinit_rangle_FieldAccess_39(o2, env, static) -{1,1}> langle_clinit_rangle_Return_40(env, static') :|: 0 < o2 && 0 <= o2 && 0 <= static && static' <= static + o2
langle_clinit_rangle_Return_40(env, static) -{1,1}> main_ConstantStackPush_48(env, static) :|: 0 >= 0
main_ConstantStackPush_48(env, static) -{0,0}> main_ConstantStackPush_49(env, static) :|: 0 >= 0
main_ConstantStackPush_49(env, static) -{0,0}> main_ConstantStackPush_52(env, static) :|: 0 <= static
main_ConstantStackPush_52(env, static) -{0,0}> main_ConstantStackPush_53(env, static) :|: 0 >= 0
main_ConstantStackPush_53(env, static) -{0,0}> main_ConstantStackPush_55(env, static) :|: 0 >= 0
main_ConstantStackPush_55(env, static) -{1,1}> main_Store_57(iconst_1000, env, static) :|: iconst_1000 = 1000
main_Store_57(iconst_1000, env, static) -{1,1}> main_New_59(iconst_1000, env, static) :|: iconst_1000 = 1000
main_New_59(iconst_1000, env, static) -{1,1}> main_Duplicate_61(o4, iconst_1000, env, static) :|: o4 = 1 && 0 < o4 && iconst_1000 = 1000
main_Duplicate_61(o4, iconst_1000, env, static) -{1,1}> main_InvokeMethod_63(o4, iconst_1000, env, static) :|: 0 < o4 && iconst_1000 = 1000
main_InvokeMethod_63(o4, iconst_1000, env, static) -{1,1}> langle_init_rangle_Load_65(o4, iconst_1000, env, static) :|: 0 < o4 && iconst_1000 = 1000
langle_init_rangle_Load_65(o4, iconst_1000, env, static) -{1,1}> langle_init_rangle_InvokeMethod_68(o4, iconst_1000, env, static) :|: 0 < o4 && iconst_1000 = 1000
langle_init_rangle_InvokeMethod_68(o4, iconst_1000, env, static) -{1,1}> langle_init_rangle_Return_70(o4, iconst_1000, env, static) :|: 0 < o4 && iconst_1000 = 1000
langle_init_rangle_Return_70(o4, iconst_1000, env, static) -{1,1}> main_Store_72(o4, iconst_1000, env, static) :|: 0 < o4 && iconst_1000 = 1000
main_Store_72(o4, iconst_1000, env, static) -{1,1}> main_New_75(iconst_1000, o4, env, static) :|: 0 < o4 && iconst_1000 = 1000
main_New_75(iconst_1000, o4, env, static) -{0,0}> main_New_77(iconst_1000, o4, env, static) :|: 0 < o4 && iconst_1000 = 1000
main_New_77(iconst_1000, o4, env, static) -{1,1}> main_Duplicate_79(o6, iconst_1000, o4, env, static) :|: 0 < o6 && 0 < o4 && o6 = 1 && iconst_1000 = 1000
main_Duplicate_79(o6, iconst_1000, o4, env, static) -{1,1}> main_InvokeMethod_80(o6, iconst_1000, o4, env, static) :|: 0 < o6 && 0 < o4 && iconst_1000 = 1000
main_InvokeMethod_80(o6, iconst_1000, o4, env, static) -{1,1}> langle_init_rangle_Load_82(o6, iconst_1000, o4, env, static) :|: 0 < o6 && 0 < o4 && iconst_1000 = 1000
langle_init_rangle_Load_82(o6, iconst_1000, o4, env, static) -{1,1}> langle_init_rangle_InvokeMethod_84(o6, iconst_1000, o4, env, static) :|: 0 < o6 && 0 < o4 && iconst_1000 = 1000
langle_init_rangle_InvokeMethod_84(o6, iconst_1000, o4, env, static) -{1,1}> langle_init_rangle_Return_86(o6, iconst_1000, o4, env, static) :|: 0 < o6 && 0 < o4 && iconst_1000 = 1000
langle_init_rangle_Return_86(o6, iconst_1000, o4, env, static) -{1,1}> main_Store_89(o6, iconst_1000, o4, env, static) :|: 0 < o6 && 0 < o4 && iconst_1000 = 1000
main_Store_89(o6, iconst_1000, o4, env, static) -{1,1}> main_Load_91(iconst_1000, o4, o6, env, static) :|: 0 < o6 && 0 < o4 && iconst_1000 = 1000
main_Load_91(iconst_1000, o4, o6, env, static) -{1,1}> main_Load_93(o4, iconst_1000, o6, env, static) :|: 0 < o6 && 0 < o4 && iconst_1000 = 1000
main_Load_93(o4, iconst_1000, o6, env, static) -{1,1}> main_Load_94(o4, iconst_1000, o6, env, static) :|: 0 < o6 && 0 < o4 && iconst_1000 = 1000
main_Load_94(o4, iconst_1000, o6, env, static) -{1,1}> main_InvokeMethod_95(o4, iconst_1000, o6, env, static) :|: 0 < o6 && 0 < o4 && iconst_1000 = 1000
main_InvokeMethod_95(o4, iconst_1000, o6, env, static) -{1,1}> add_ConstantStackPush_96(iconst_1000, o6, o4, env, static) :|: 0 < o6 && 0 < o4 && iconst_1000 = 1000
add_ConstantStackPush_96(iconst_1000, o6, o4, env, static) -{1,1}> add_Store_97(iconst_0, iconst_1000, o6, o4, env, static) :|: 0 < o6 && 0 < o4 && iconst_0 = 0 && iconst_1000 = 1000
add_Store_97(iconst_0, iconst_1000, o6, o4, env, static) -{1,1}> add_ConstantStackPush_98(iconst_1000, o6, iconst_0, o4, env, static) :|: 0 < o6 && 0 < o4 && iconst_0 = 0 && iconst_1000 = 1000
add_ConstantStackPush_98(iconst_1000, o6, iconst_0, o4, env, static) -{1,1}> add_Store_99(iconst_0, iconst_1000, o6, o4, env, static) :|: 0 < o6 && 0 < o4 && iconst_0 = 0 && iconst_1000 = 1000
add_Store_99(iconst_0, iconst_1000, o6, o4, env, static) -{1,1}> add_Load_100(iconst_1000, o6, iconst_0, o4, env, static) :|: 0 < o6 && 0 < o4 && iconst_0 = 0 && iconst_1000 = 1000
add_Load_100(iconst_1000, o6, iconst_0, o4, env, static) -{0,0}> add_Load_156(iconst_1000, o6, iconst_0, iconst_0, o4, env, static) :|: 0 <= iconst_0 && 0 < o6 && 0 < o4 && iconst_0 <= 1 && iconst_0 = 0 && iconst_1000 = 1000
add_Load_156(iconst_1000, o10, iconst_0, i1, o11, env, static) -{0,0}> add_Load_228(iconst_1000, o10, iconst_0, i1, o11, env, static) :|: 0 <= iconst_0 && 0 <= i1 && i1 <= 1 && iconst_0 <= 1 && iconst_0 = 0 && 0 < o11 && iconst_1000 = 1000 && 0 < o10 && i1 <= 2
add_Load_228(iconst_1000, o20, i4, i5, o21, env, static) -{0,0}> add_Load_283(iconst_1000, o20, i4, i5, o21, env, static) :|: 0 < o20 && i5 <= 2 && 0 <= i4 && 0 < o21 && iconst_1000 = 1000 && 0 <= i5 && i4 <= 1
add_Load_283(iconst_1000, o30, i10, i11, o31, env, static) -{1,1}> add_Load_286(i11, iconst_1000, o30, i10, o31, env, static) :|: 0 <= i10 && 0 < o30 && 0 <= i11 && 0 < o31 && iconst_1000 = 1000
add_Load_286(i11, iconst_1000, o30, i10, o31, env, static) -{1,1}> add_GT_299(i11, iconst_1000, o30, i10, o31, env, static) :|: 0 <= i10 && 0 < o30 && 0 <= i11 && 0 < o31 && iconst_1000 = 1000
add_GT_299(i18, iconst_1000, o30, i10, o31, env, static) -{0,0}> add_GT_304(i18, iconst_1000, o30, i10, o31, env, static) :|: 0 <= i10 && 0 <= i18 && i18 <= 1000 && 0 < o30 && 0 < o31 && iconst_1000 = 1000
add_GT_299(i19, iconst_1000, o30, i10, o31, env, static) -{0,0}> add_GT_305(i19, iconst_1000, o30, i10, o31, env, static) :|: 0 <= i10 && 0 < o30 && 0 < o31 && 1001 <= i19 && iconst_1000 = 1000 && 0 <= i19
add_GT_304(i18, iconst_1000, o30, i10, o31, env, static) -{1,1}> add_Load_309(iconst_1000, o30, i10, i18, o31, env, static) :|: 0 <= i10 && 0 <= i18 && i18 <= 1000 && 0 < o30 && i18 <= iconst_1000 && 0 < o31 && iconst_1000 = 1000
add_GT_305(i19, iconst_1000, o30, i10, o31, env, static) -{1,1}> add_Load_317(i10, iconst_1000, o31, env, static) :|: 0 <= i10 && 0 < o30 && 0 < o31 && 1001 <= i19 && iconst_1000 < i19 && iconst_1000 = 1000
add_Load_309(iconst_1000, o30, i10, i18, o31, env, static) -{1,1}> add_Load_319(i10, iconst_1000, o30, i18, o31, env, static) :|: 0 <= i10 && 0 <= i18 && i18 <= 1000 && 0 < o30 && 0 < o31 && iconst_1000 = 1000
add_Load_317(i10, iconst_1000, o31, env, static) -{1,1}> add_Return_321(i10, iconst_1000, o31, env, static) :|: 0 <= i10 && 0 < o31 && iconst_1000 = 1000
add_Load_319(i10, iconst_1000, o30, i18, o31, env, static) -{1,1}> add_IntArithmetic_323(i10, i18, iconst_1000, o30, o31, env, static) :|: 0 <= i10 && 0 <= i18 && i18 <= 1000 && 0 < o30 && 0 < o31 && iconst_1000 = 1000
add_Return_321(i10, iconst_1000, o31, env, static) -{1,1}> main_Store_325(i10, iconst_1000, o31, env, static) :|: 0 <= i10 && 0 < o31 && iconst_1000 = 1000
add_IntArithmetic_323(i10, i18, iconst_1000, o30, o31, env, static) -{1,1}> add_Store_328(i20, iconst_1000, o30, i18, o31, env, static) :|: 0 <= i10 && 0 <= i18 && i18 <= 1000 && 0 <= i20 && 0 < o30 && 0 < o31 && iconst_1000 = 1000 && i10 + i18 = i20
main_Store_325(i10, iconst_1000, o31, env, static) -{1,1}> main_New_331(iconst_1000, o31, env, static) :|: 0 <= i10 && 0 < o31 && iconst_1000 = 1000
add_Store_328(i20, iconst_1000, o30, i18, o31, env, static) -{1,1}> add_Load_332(iconst_1000, o30, i20, i18, o31, env, static) :|: 0 <= i18 && 0 <= i20 && i18 <= 1000 && 0 < o30 && 0 < o31 && iconst_1000 = 1000
main_New_331(iconst_1000, o31, env, static) -{0,0}> main_New_333(iconst_1000, o31, env, static) :|: 0 < o31 && iconst_1000 = 1000
add_Load_332(iconst_1000, o30, i20, i18, o31, env, static) -{1,1}> add_Load_334(o30, iconst_1000, i20, i18, o31, env, static) :|: 0 <= i18 && 0 <= i20 && i18 <= 1000 && 0 < o30 && 0 < o31 && iconst_1000 = 1000
main_New_333(iconst_1000, o31, env, static) -{1,1}> main_Duplicate_335(o37, iconst_1000, o31, env, static) :|: 0 < o37 && 0 < o31 && o37 = 1 && iconst_1000 = 1000
add_Load_334(o30, iconst_1000, i20, i18, o31, env, static) -{1,1}> add_InvokeMethod_336(o30, i18, iconst_1000, i20, o31, env, static) :|: 0 <= i18 && 0 <= i20 && i18 <= 1000 && 0 < o30 && 0 < o31 && iconst_1000 = 1000
main_Duplicate_335(o37, iconst_1000, o31, env, static) -{1,1}> main_InvokeMethod_337(o37, iconst_1000, o31, env, static) :|: 0 < o37 && 0 < o31 && iconst_1000 = 1000
add_InvokeMethod_336(o30, i18, iconst_1000, i20, o31, env, static) -{1,1}> incr_Load_338(i18, iconst_1000, o30, i20, o31, env, static) :|: 0 <= i18 && i18 <= 1000 && 0 <= i20 && 0 < o30 && 0 < o31 && iconst_1000 = 1000
main_InvokeMethod_337(o37, iconst_1000, o31, env, static) -{1,1}> langle_init_rangle_Load_339(o37, iconst_1000, o31, env, static) :|: 0 < o37 && 0 < o31 && iconst_1000 = 1000
incr_Load_338(i18, iconst_1000, o30, i20, o31, env, static) -{1,1}> incr_ConstantStackPush_340(i18, iconst_1000, o30, i20, o31, env, static) :|: 0 <= i18 && i18 <= 1000 && 0 <= i20 && 0 < o30 && 0 < o31 && iconst_1000 = 1000
langle_init_rangle_Load_339(o37, iconst_1000, o31, env, static) -{1,1}> langle_init_rangle_InvokeMethod_341(o37, iconst_1000, o31, env, static) :|: 0 < o37 && 0 < o31 && iconst_1000 = 1000
incr_ConstantStackPush_340(i18, iconst_1000, o30, i20, o31, env, static) -{1,1}> incr_IntArithmetic_343(i18, iconst_1, iconst_1000, o30, i20, o31, env, static) :|: 0 <= i18 && i18 <= 1000 && 0 <= i20 && 0 < o30 && 0 < o31 && iconst_1 = 1 && iconst_1000 = 1000
langle_init_rangle_InvokeMethod_341(o37, iconst_1000, o31, env, static) -{1,1}> langle_init_rangle_Load_344(o37, iconst_1000, o31, env, static) :|: 0 < o37 && 0 < o31 && iconst_1000 = 1000
incr_IntArithmetic_343(i18, iconst_1, iconst_1000, o30, i20, o31, env, static) -{1,1}> incr_Duplicate_346(i21, iconst_1000, o30, i20, o31, env, static) :|: 1 <= i21 && 0 <= i18 && i18 <= 1000 && 0 <= i20 && 0 < o30 && 0 < o31 && i21 <= 1001 && iconst_1 = 1 && i18 + iconst_1 = i21 && iconst_1000 = 1000
langle_init_rangle_Load_344(o37, iconst_1000, o31, env, static) -{1,1}> langle_init_rangle_InvokeMethod_351(o37, iconst_1000, o31, env, static) :|: 0 < o37 && 0 < o31 && iconst_1000 = 1000
incr_Duplicate_346(i21, iconst_1000, o30, i20, o31, env, static) -{1,1}> incr_Store_348(i21, iconst_1000, o30, i20, o31, env, static) :|: 1 <= i21 && 0 <= i20 && 0 < o30 && 0 < o31 && i21 <= 1001 && iconst_1000 = 1000
incr_Store_348(i21, iconst_1000, o30, i20, o31, env, static) -{1,1}> incr_Return_353(i21, iconst_1000, o30, i20, o31, env, static) :|: 1 <= i21 && 0 <= i20 && 0 < o30 && 0 < o31 && i21 <= 1001 && iconst_1000 = 1000
langle_init_rangle_InvokeMethod_351(o37, iconst_1000, o31, env, static) -{1,1}> langle_init_rangle_Return_357(o37, iconst_1000, o31, env, static) :|: 0 < o37 && 0 < o31 && iconst_1000 = 1000
incr_Return_353(i21, iconst_1000, o30, i20, o31, env, static) -{1,1}> add_Store_359(i21, iconst_1000, o30, i20, o31, env, static) :|: 1 <= i21 && 0 <= i20 && 0 < o30 && 0 < o31 && i21 <= 1001 && iconst_1000 = 1000
langle_init_rangle_Return_357(o37, iconst_1000, o31, env, static) -{1,1}> langle_init_rangle_Return_361(o37, iconst_1000, o31, env, static) :|: 0 < o37 && 0 < o31 && iconst_1000 = 1000
add_Store_359(i21, iconst_1000, o30, i20, o31, env, static) -{1,1}> add_JMP_363(iconst_1000, o30, i20, i21, o31, env, static) :|: 1 <= i21 && 0 <= i20 && 0 < o30 && 0 < o31 && i21 <= 1001 && iconst_1000 = 1000
langle_init_rangle_Return_361(o37, iconst_1000, o31, env, static) -{1,1}> main_Store_365(o37, iconst_1000, o31, env, static) :|: 0 < o37 && 0 < o31 && iconst_1000 = 1000
add_JMP_363(iconst_1000, o30, i20, i21, o31, env, static) -{1,1}> add_Load_370(iconst_1000, o30, i20, i21, o31, env, static) :|: 1 <= i21 && 0 <= i20 && 0 < o30 && 0 < o31 && i21 <= 1001 && iconst_1000 = 1000
main_Store_365(o37, iconst_1000, o31, env, static) -{1,1}> main_Load_372(iconst_1000, o31, o37, env, static) :|: 0 < o37 && 0 < o31 && iconst_1000 = 1000
add_Load_370(iconst_1000, o30, i20, i21, o31, env, static) -{0,0}> add_Load_283(iconst_1000, o30, i20, i21, o31, env, static) :|: 1 <= i21 && 0 <= i20 && 0 < o30 && 0 <= i21 && 0 < o31 && i21 <= 1001 && iconst_1000 = 1000
main_Load_372(iconst_1000, o31, o37, env, static) -{1,1}> main_Load_373(o31, iconst_1000, o37, env, static) :|: 0 < o37 && 0 < o31 && iconst_1000 = 1000
main_Load_373(o31, iconst_1000, o37, env, static) -{1,1}> main_Load_374(o31, iconst_1000, o37, env, static) :|: 0 < o37 && 0 < o31 && iconst_1000 = 1000
main_Load_374(o31, iconst_1000, o37, env, static) -{1,1}> main_InvokeMethod_375(o31, iconst_1000, o37, env, static) :|: 0 < o37 && 0 < o31 && iconst_1000 = 1000
main_InvokeMethod_375(o31, iconst_1000, o37, env, static) -{1,1}> add_ConstantStackPush_376(iconst_1000, o37, o31, env, static) :|: 0 < o37 && 0 < o31 && iconst_1000 = 1000
add_ConstantStackPush_376(iconst_1000, o37, o31, env, static) -{1,1}> add_Store_378(iconst_0, iconst_1000, o37, o31, env, static) :|: 0 < o37 && 0 < o31 && iconst_0 = 0 && iconst_1000 = 1000
add_Store_378(iconst_0, iconst_1000, o37, o31, env, static) -{1,1}> add_ConstantStackPush_383(iconst_1000, o37, iconst_0, o31, env, static) :|: 0 < o37 && 0 < o31 && iconst_0 = 0 && iconst_1000 = 1000
add_ConstantStackPush_383(iconst_1000, o37, iconst_0, o31, env, static) -{1,1}> add_Store_389(iconst_0, iconst_1000, o37, o31, env, static) :|: 0 < o37 && 0 < o31 && iconst_0 = 0 && iconst_1000 = 1000
add_Store_389(iconst_0, iconst_1000, o37, o31, env, static) -{1,1}> add_Load_394(iconst_1000, o37, iconst_0, o31, env, static) :|: 0 < o37 && 0 < o31 && iconst_0 = 0 && iconst_1000 = 1000
add_Load_394(iconst_1000, o37, iconst_0, o31, env, static) -{0,0}> add_Load_453(iconst_1000, o37, iconst_0, iconst_0, o31, env, static) :|: 0 < o37 && 0 <= iconst_0 && iconst_0 <= 2 && 0 < o31 && iconst_0 = 0 && iconst_1000 = 1000
add_Load_453(iconst_1000, o111, iconst_0, i48, o112, env, static) -{0,0}> add_Load_522(iconst_1000, o111, iconst_0, i48, o112, env, static) :|: 0 <= iconst_0 && iconst_0 <= 2 && 0 <= i48 && i48 <= 4 && iconst_0 = 0 && 0 < o112 && iconst_1000 = 1000 && 0 < o111 && i48 <= 2
add_Load_522(iconst_1000, o169, i74, i75, o170, env, static) -{0,0}> add_Load_599(iconst_1000, o169, i74, i75, o170, env, static) :|: i74 <= 2 && i75 <= 4 && iconst_1000 = 1000 && 0 < o170 && 0 <= i75 && 0 < o169 && 0 <= i74
add_Load_599(iconst_1000, o227, i104, i105, o228, env, static) -{1,1}> add_Load_600(i105, iconst_1000, o227, i104, o228, env, static) :|: 0 < o227 && 0 <= i105 && 0 <= i104 && iconst_1000 = 1000 && 0 < o228
add_Load_600(i105, iconst_1000, o227, i104, o228, env, static) -{1,1}> add_GT_602(i105, iconst_1000, o227, i104, o228, env, static) :|: 0 < o227 && 0 <= i105 && 0 <= i104 && iconst_1000 = 1000 && 0 < o228
add_GT_602(i112, iconst_1000, o227, i104, o228, env, static) -{0,0}> add_GT_607(i112, iconst_1000, o227, i104, o228, env, static) :|: 0 < o227 && 0 <= i112 && 0 <= i104 && iconst_1000 = 1000 && 0 < o228 && i112 <= 1000
add_GT_602(i113, iconst_1000, o227, i104, o228, env, static) -{0,0}> add_GT_608(i113, iconst_1000, o227, i104, o228, env, static) :|: 0 < o227 && 1001 <= i113 && 0 <= i113 && 0 <= i104 && iconst_1000 = 1000 && 0 < o228
add_GT_607(i112, iconst_1000, o227, i104, o228, env, static) -{1,1}> add_Load_621(iconst_1000, o227, i104, i112, o228, env, static) :|: 0 < o227 && 0 <= i112 && i112 <= iconst_1000 && 0 <= i104 && iconst_1000 = 1000 && 0 < o228 && i112 <= 1000
add_GT_608(i113, iconst_1000, o227, i104, o228, env, static) -{1,1}> add_Load_624(i104, iconst_1000, o228, env, static) :|: 0 < o227 && 1001 <= i113 && iconst_1000 < i113 && 0 <= i104 && iconst_1000 = 1000 && 0 < o228
add_Load_621(iconst_1000, o227, i104, i112, o228, env, static) -{1,1}> add_Load_627(i104, iconst_1000, o227, i112, o228, env, static) :|: 0 < o227 && 0 <= i112 && 0 <= i104 && iconst_1000 = 1000 && 0 < o228 && i112 <= 1000
add_Load_624(i104, iconst_1000, o228, env, static) -{1,1}> add_Return_631(i104, iconst_1000, o228, env, static) :|: 0 <= i104 && iconst_1000 = 1000 && 0 < o228
add_Load_627(i104, iconst_1000, o227, i112, o228, env, static) -{1,1}> add_IntArithmetic_636(i104, i112, iconst_1000, o227, o228, env, static) :|: 0 < o227 && 0 <= i112 && 0 <= i104 && iconst_1000 = 1000 && 0 < o228 && i112 <= 1000
add_Return_631(i104, iconst_1000, o228, env, static) -{1,1}> main_Store_637(i104, iconst_1000, o228, env, static) :|: 0 <= i104 && iconst_1000 = 1000 && 0 < o228
add_IntArithmetic_636(i104, i112, iconst_1000, o227, o228, env, static) -{1,1}> add_Store_643(i126, iconst_1000, o227, i112, o228, env, static) :|: 0 < o227 && 0 <= i112 && 0 <= i104 && iconst_1000 = 1000 && 0 < o228 && i112 <= 1000 && 0 <= i126 && i104 + i112 = i126
main_Store_637(i104, iconst_1000, o228, env, static) -{1,1}> main_New_645(iconst_1000, o228, env, static) :|: 0 <= i104 && iconst_1000 = 1000 && 0 < o228
add_Store_643(i126, iconst_1000, o227, i112, o228, env, static) -{1,1}> add_Load_648(iconst_1000, o227, i126, i112, o228, env, static) :|: 0 < o227 && 0 <= i112 && iconst_1000 = 1000 && 0 < o228 && 0 <= i126 && i112 <= 1000
main_New_645(iconst_1000, o228, env, static) -{0,0}> main_New_649(iconst_1000, o228, env, static) :|: iconst_1000 = 1000 && 0 < o228
add_Load_648(iconst_1000, o227, i126, i112, o228, env, static) -{1,1}> add_Load_650(o227, iconst_1000, i126, i112, o228, env, static) :|: 0 < o227 && 0 <= i112 && iconst_1000 = 1000 && 0 < o228 && 0 <= i126 && i112 <= 1000
main_New_649(iconst_1000, o228, env, static) -{1,1}> main_Duplicate_651(o275, iconst_1000, o228, env, static) :|: 0 < o275 && o275 = 1 && iconst_1000 = 1000 && 0 < o228
add_Load_650(o227, iconst_1000, i126, i112, o228, env, static) -{1,1}> add_InvokeMethod_653(o227, i112, iconst_1000, i126, o228, env, static) :|: 0 < o227 && 0 <= i112 && iconst_1000 = 1000 && 0 < o228 && 0 <= i126 && i112 <= 1000
main_Duplicate_651(o275, iconst_1000, o228, env, static) -{1,1}> main_InvokeMethod_654(o275, iconst_1000, o228, env, static) :|: 0 < o275 && iconst_1000 = 1000 && 0 < o228
add_InvokeMethod_653(o227, i112, iconst_1000, i126, o228, env, static) -{1,1}> incr_Load_655(i112, iconst_1000, o227, i126, o228, env, static) :|: 0 < o227 && 0 <= i112 && iconst_1000 = 1000 && 0 < o228 && i112 <= 1000 && 0 <= i126
main_InvokeMethod_654(o275, iconst_1000, o228, env, static) -{1,1}> langle_init_rangle_Load_656(o275, iconst_1000, o228, env, static) :|: 0 < o275 && iconst_1000 = 1000 && 0 < o228
incr_Load_655(i112, iconst_1000, o227, i126, o228, env, static) -{1,1}> incr_ConstantStackPush_658(i112, iconst_1000, o227, i126, o228, env, static) :|: 0 < o227 && 0 <= i112 && iconst_1000 = 1000 && 0 < o228 && i112 <= 1000 && 0 <= i126
langle_init_rangle_Load_656(o275, iconst_1000, o228, env, static) -{1,1}> langle_init_rangle_InvokeMethod_659(o275, iconst_1000, o228, env, static) :|: 0 < o275 && iconst_1000 = 1000 && 0 < o228
incr_ConstantStackPush_658(i112, iconst_1000, o227, i126, o228, env, static) -{1,1}> incr_IntArithmetic_660(i112, iconst_2, iconst_1000, o227, i126, o228, env, static) :|: 0 < o227 && 0 <= i112 && iconst_1000 = 1000 && 0 < o228 && i112 <= 1000 && 0 <= i126 && iconst_2 = 2
langle_init_rangle_InvokeMethod_659(o275, iconst_1000, o228, env, static) -{1,1}> langle_init_rangle_Load_661(o275, iconst_1000, o228, env, static) :|: 0 < o275 && iconst_1000 = 1000 && 0 < o228
incr_IntArithmetic_660(i112, iconst_2, iconst_1000, o227, i126, o228, env, static) -{1,1}> incr_Duplicate_662(i135, iconst_1000, o227, i126, o228, env, static) :|: i112 + iconst_2 = i135 && 0 < o227 && i135 <= 1002 && 0 <= i112 && 2 <= i135 && iconst_1000 = 1000 && 0 < o228 && i112 <= 1000 && 0 <= i126 && iconst_2 = 2
langle_init_rangle_Load_661(o275, iconst_1000, o228, env, static) -{1,1}> langle_init_rangle_InvokeMethod_664(o275, iconst_1000, o228, env, static) :|: 0 < o275 && iconst_1000 = 1000 && 0 < o228
incr_Duplicate_662(i135, iconst_1000, o227, i126, o228, env, static) -{1,1}> incr_Store_663(i135, iconst_1000, o227, i126, o228, env, static) :|: i135 <= 1002 && 0 < o227 && 2 <= i135 && iconst_1000 = 1000 && 0 < o228 && 0 <= i126
incr_Store_663(i135, iconst_1000, o227, i126, o228, env, static) -{1,1}> incr_Return_665(i135, iconst_1000, o227, i126, o228, env, static) :|: i135 <= 1002 && 0 < o227 && 2 <= i135 && iconst_1000 = 1000 && 0 < o228 && 0 <= i126
langle_init_rangle_InvokeMethod_664(o275, iconst_1000, o228, env, static) -{1,1}> langle_init_rangle_Load_666(o275, iconst_1000, o228, env, static) :|: 0 < o275 && iconst_1000 = 1000 && 0 < o228
incr_Return_665(i135, iconst_1000, o227, i126, o228, env, static) -{1,1}> add_Store_667(i135, iconst_1000, o227, i126, o228, env, static) :|: i135 <= 1002 && 0 < o227 && 2 <= i135 && iconst_1000 = 1000 && 0 < o228 && 0 <= i126
langle_init_rangle_Load_666(o275, iconst_1000, o228, env, static) -{1,1}> langle_init_rangle_InvokeMethod_673(o275, iconst_1000, o228, env, static) :|: 0 < o275 && iconst_1000 = 1000 && 0 < o228
add_Store_667(i135, iconst_1000, o227, i126, o228, env, static) -{1,1}> add_JMP_668(iconst_1000, o227, i126, i135, o228, env, static) :|: i135 <= 1002 && 0 < o227 && 2 <= i135 && iconst_1000 = 1000 && 0 < o228 && 0 <= i126
add_JMP_668(iconst_1000, o227, i126, i135, o228, env, static) -{1,1}> add_Load_678(iconst_1000, o227, i126, i135, o228, env, static) :|: 0 < o227 && i135 <= 1002 && 2 <= i135 && iconst_1000 = 1000 && 0 < o228 && 0 <= i126
langle_init_rangle_InvokeMethod_673(o275, iconst_1000, o228, env, static) -{1,1}> langle_init_rangle_Return_684(o275, iconst_1000, o228, env, static) :|: 0 < o275 && iconst_1000 = 1000 && 0 < o228
add_Load_678(iconst_1000, o227, i126, i135, o228, env, static) -{0,0}> add_Load_599(iconst_1000, o227, i126, i135, o228, env, static) :|: 0 < o227 && i135 <= 1002 && 2 <= i135 && iconst_1000 = 1000 && 0 <= i135 && 0 < o228 && 0 <= i126
langle_init_rangle_Return_684(o275, iconst_1000, o228, env, static) -{1,1}> langle_init_rangle_Return_688(o275, iconst_1000, o228, env, static) :|: 0 < o275 && iconst_1000 = 1000 && 0 < o228
langle_init_rangle_Return_688(o275, iconst_1000, o228, env, static) -{1,1}> langle_init_rangle_Return_689(o275, iconst_1000, o228, env, static) :|: 0 < o275 && iconst_1000 = 1000 && 0 < o228
langle_init_rangle_Return_689(o275, iconst_1000, o228, env, static) -{1,1}> main_Store_690(o275, iconst_1000, o228, env, static) :|: 0 < o275 && iconst_1000 = 1000 && 0 < o228
main_Store_690(o275, iconst_1000, o228, env, static) -{1,1}> main_Load_691(iconst_1000, o228, o275, env, static) :|: 0 < o275 && iconst_1000 = 1000 && 0 < o228
main_Load_691(iconst_1000, o228, o275, env, static) -{1,1}> main_Load_692(o228, iconst_1000, o275, env, static) :|: 0 < o275 && iconst_1000 = 1000 && 0 < o228
main_Load_692(o228, iconst_1000, o275, env, static) -{1,1}> main_Load_693(o228, iconst_1000, o275, env, static) :|: 0 < o275 && iconst_1000 = 1000 && 0 < o228
main_Load_693(o228, iconst_1000, o275, env, static) -{1,1}> main_InvokeMethod_694(o228, iconst_1000, o275, env, static) :|: 0 < o275 && iconst_1000 = 1000 && 0 < o228
main_InvokeMethod_694(o228, iconst_1000, o275, env, static) -{1,1}> add_ConstantStackPush_695(iconst_1000, o275, env, static) :|: 0 < o275 && iconst_1000 = 1000 && 0 < o228
add_ConstantStackPush_695(iconst_1000, o275, env, static) -{1,1}> add_Store_702(iconst_0, iconst_1000, o275, env, static) :|: 0 < o275 && iconst_0 = 0 && iconst_1000 = 1000
add_Store_702(iconst_0, iconst_1000, o275, env, static) -{1,1}> add_ConstantStackPush_709(iconst_1000, o275, iconst_0, env, static) :|: 0 < o275 && iconst_0 = 0 && iconst_1000 = 1000
add_ConstantStackPush_709(iconst_1000, o275, iconst_0, env, static) -{1,1}> add_Store_715(iconst_0, iconst_1000, o275, env, static) :|: 0 < o275 && iconst_0 = 0 && iconst_1000 = 1000
add_Store_715(iconst_0, iconst_1000, o275, env, static) -{1,1}> add_Load_717(iconst_1000, o275, iconst_0, env, static) :|: 0 < o275 && iconst_0 = 0 && iconst_1000 = 1000
add_Load_717(iconst_1000, o275, iconst_0, env, static) -{0,0}> add_Load_808(iconst_1000, o275, iconst_0, iconst_0, env, static) :|: 0 <= iconst_0 && 0 < o275 && iconst_0 = 0 && iconst_1000 = 1000 && iconst_0 <= 3
add_Load_808(iconst_1000, o438, iconst_0, i194, env, static) -{0,0}> add_Load_889(iconst_1000, o438, iconst_0, i194, env, static) :|: i194 <= 3 && 0 <= iconst_0 && iconst_0 = 0 && iconst_1000 = 1000 && 0 <= i194 && 0 < o438 && iconst_0 <= 3 && i194 <= 6
add_Load_889(iconst_1000, o538, i241, i242, env, static) -{0,0}> add_Load_954(iconst_1000, o538, i241, i242, env, static) :|: i242 <= 6 && 0 < o538 && 0 <= i242 && 0 <= i241 && iconst_1000 = 1000 && i241 <= 3
add_Load_954(iconst_1000, o644, i296, i297, env, static) -{1,1}> add_Load_955(i297, iconst_1000, o644, i296, env, static) :|: 0 <= i297 && iconst_1000 = 1000 && 0 <= i296 && 0 < o644
add_Load_955(i297, iconst_1000, o644, i296, env, static) -{1,1}> add_GT_956(i297, iconst_1000, o644, i296, env, static) :|: 0 <= i297 && iconst_1000 = 1000 && 0 <= i296 && 0 < o644
add_GT_956(i308, iconst_1000, o644, i296, env, static) -{0,0}> add_GT_957(i308, iconst_1000, o644, i296, env, static) :|: i308 <= 1000 && 0 <= i308 && iconst_1000 = 1000 && 0 <= i296 && 0 < o644
add_GT_957(i308, iconst_1000, o644, i296, env, static) -{1,1}> add_Load_959(iconst_1000, o644, i296, i308, env, static) :|: i308 <= 1000 && i308 <= iconst_1000 && 0 <= i308 && iconst_1000 = 1000 && 0 <= i296 && 0 < o644
add_Load_959(iconst_1000, o644, i296, i308, env, static) -{1,1}> add_Load_963(i296, iconst_1000, o644, i308, env, static) :|: i308 <= 1000 && 0 <= i308 && iconst_1000 = 1000 && 0 <= i296 && 0 < o644
add_Load_963(i296, iconst_1000, o644, i308, env, static) -{1,1}> add_IntArithmetic_973(i296, i308, iconst_1000, o644, env, static) :|: i308 <= 1000 && 0 <= i308 && iconst_1000 = 1000 && 0 <= i296 && 0 < o644
add_IntArithmetic_973(i296, i308, iconst_1000, o644, env, static) -{1,1}> add_Store_981(i334, iconst_1000, o644, i308, env, static) :|: i308 <= 1000 && 0 <= i308 && iconst_1000 = 1000 && 0 <= i296 && 0 <= i334 && 0 < o644 && i296 + i308 = i334
add_Store_981(i334, iconst_1000, o644, i308, env, static) -{1,1}> add_Load_985(iconst_1000, o644, i334, i308, env, static) :|: i308 <= 1000 && 0 <= i308 && iconst_1000 = 1000 && 0 <= i334 && 0 < o644
add_Load_985(iconst_1000, o644, i334, i308, env, static) -{1,1}> add_Load_993(o644, iconst_1000, i334, i308, env, static) :|: i308 <= 1000 && 0 <= i308 && iconst_1000 = 1000 && 0 <= i334 && 0 < o644
add_Load_993(o644, iconst_1000, i334, i308, env, static) -{1,1}> add_InvokeMethod_999(o644, i308, iconst_1000, i334, env, static) :|: i308 <= 1000 && 0 <= i308 && iconst_1000 = 1000 && 0 <= i334 && 0 < o644
add_InvokeMethod_999(o644, i308, iconst_1000, i334, env, static) -{1,1}> incr_Load_1001(i308, iconst_1000, o644, i334, env, static) :|: i308 <= 1000 && 0 <= i308 && iconst_1000 = 1000 && 0 <= i334 && 0 < o644
incr_Load_1001(i308, iconst_1000, o644, i334, env, static) -{1,1}> incr_ConstantStackPush_1004(i308, iconst_1000, o644, i334, env, static) :|: i308 <= 1000 && 0 <= i308 && iconst_1000 = 1000 && 0 <= i334 && 0 < o644
incr_ConstantStackPush_1004(i308, iconst_1000, o644, i334, env, static) -{1,1}> incr_IntArithmetic_1006(i308, iconst_3, iconst_1000, o644, i334, env, static) :|: i308 <= 1000 && iconst_3 = 3 && 0 <= i308 && iconst_1000 = 1000 && 0 <= i334 && 0 < o644
incr_IntArithmetic_1006(i308, iconst_3, iconst_1000, o644, i334, env, static) -{1,1}> incr_Duplicate_1008(i351, iconst_1000, o644, i334, env, static) :|: i308 <= 1000 && i308 + iconst_3 = i351 && i351 <= 1003 && iconst_3 = 3 && 0 <= i308 && iconst_1000 = 1000 && 3 <= i351 && 0 <= i334 && 0 < o644
incr_Duplicate_1008(i351, iconst_1000, o644, i334, env, static) -{1,1}> incr_Store_1010(i351, iconst_1000, o644, i334, env, static) :|: i351 <= 1003 && iconst_1000 = 1000 && 3 <= i351 && 0 <= i334 && 0 < o644
incr_Store_1010(i351, iconst_1000, o644, i334, env, static) -{1,1}> incr_Return_1012(i351, iconst_1000, o644, i334, env, static) :|: i351 <= 1003 && iconst_1000 = 1000 && 3 <= i351 && 0 <= i334 && 0 < o644
incr_Return_1012(i351, iconst_1000, o644, i334, env, static) -{1,1}> add_Store_1013(i351, iconst_1000, o644, i334, env, static) :|: i351 <= 1003 && iconst_1000 = 1000 && 3 <= i351 && 0 <= i334 && 0 < o644
add_Store_1013(i351, iconst_1000, o644, i334, env, static) -{1,1}> add_JMP_1017(iconst_1000, o644, i334, i351, env, static) :|: i351 <= 1003 && iconst_1000 = 1000 && 3 <= i351 && 0 <= i334 && 0 < o644
add_JMP_1017(iconst_1000, o644, i334, i351, env, static) -{1,1}> add_Load_1021(iconst_1000, o644, i334, i351, env, static) :|: i351 <= 1003 && iconst_1000 = 1000 && 3 <= i351 && 0 <= i334 && 0 < o644
add_Load_1021(iconst_1000, o644, i334, i351, env, static) -{0,0}> add_Load_954(iconst_1000, o644, i334, i351, env, static) :|: i351 <= 1003 && 0 <= i351 && iconst_1000 = 1000 && 3 <= i351 && 0 <= i334 && 0 < o644

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

obtained
add_Load_954(1000, o644, i296, i297, env, static) -{18,18}> add_Load_954(1000, o644, i334', i351', env, static) :|: i297 <= 1000 && 0 < o644 && 0 <= i296 && 0 <= i334' && 0 <= i297 && 3 <= i351' && i351' <= 1003 && 0 <= i351' && i296 + i297 = i334' && i297 + 3 = i351'
by chaining
add_Load_954(iconst_1000, o644, i296, i297, env, static) -{1,1}> add_Load_955(i297, iconst_1000, o644, i296, env, static) :|: 0 <= i297 && iconst_1000 = 1000 && 0 <= i296 && 0 < o644
add_Load_955(i297, iconst_1000, o644, i296, env, static) -{1,1}> add_GT_956(i297, iconst_1000, o644, i296, env, static) :|: 0 <= i297 && iconst_1000 = 1000 && 0 <= i296 && 0 < o644
add_GT_956(i308, iconst_1000, o644, i296, env, static) -{0,0}> add_GT_957(i308, iconst_1000, o644, i296, env, static) :|: i308 <= 1000 && 0 <= i308 && iconst_1000 = 1000 && 0 <= i296 && 0 < o644
add_GT_957(i308, iconst_1000, o644, i296, env, static) -{1,1}> add_Load_959(iconst_1000, o644, i296, i308, env, static) :|: i308 <= 1000 && i308 <= iconst_1000 && 0 <= i308 && iconst_1000 = 1000 && 0 <= i296 && 0 < o644
add_Load_959(iconst_1000, o644, i296, i308, env, static) -{1,1}> add_Load_963(i296, iconst_1000, o644, i308, env, static) :|: i308 <= 1000 && 0 <= i308 && iconst_1000 = 1000 && 0 <= i296 && 0 < o644
add_Load_963(i296, iconst_1000, o644, i308, env, static) -{1,1}> add_IntArithmetic_973(i296, i308, iconst_1000, o644, env, static) :|: i308 <= 1000 && 0 <= i308 && iconst_1000 = 1000 && 0 <= i296 && 0 < o644
add_IntArithmetic_973(i296, i308, iconst_1000, o644, env, static) -{1,1}> add_Store_981(i334, iconst_1000, o644, i308, env, static) :|: i308 <= 1000 && 0 <= i308 && iconst_1000 = 1000 && 0 <= i296 && 0 <= i334 && 0 < o644 && i296 + i308 = i334
add_Store_981(i334, iconst_1000, o644, i308, env, static) -{1,1}> add_Load_985(iconst_1000, o644, i334, i308, env, static) :|: i308 <= 1000 && 0 <= i308 && iconst_1000 = 1000 && 0 <= i334 && 0 < o644
add_Load_985(iconst_1000, o644, i334, i308, env, static) -{1,1}> add_Load_993(o644, iconst_1000, i334, i308, env, static) :|: i308 <= 1000 && 0 <= i308 && iconst_1000 = 1000 && 0 <= i334 && 0 < o644
add_Load_993(o644, iconst_1000, i334, i308, env, static) -{1,1}> add_InvokeMethod_999(o644, i308, iconst_1000, i334, env, static) :|: i308 <= 1000 && 0 <= i308 && iconst_1000 = 1000 && 0 <= i334 && 0 < o644
add_InvokeMethod_999(o644, i308, iconst_1000, i334, env, static) -{1,1}> incr_Load_1001(i308, iconst_1000, o644, i334, env, static) :|: i308 <= 1000 && 0 <= i308 && iconst_1000 = 1000 && 0 <= i334 && 0 < o644
incr_Load_1001(i308, iconst_1000, o644, i334, env, static) -{1,1}> incr_ConstantStackPush_1004(i308, iconst_1000, o644, i334, env, static) :|: i308 <= 1000 && 0 <= i308 && iconst_1000 = 1000 && 0 <= i334 && 0 < o644
incr_ConstantStackPush_1004(i308, iconst_1000, o644, i334, env, static) -{1,1}> incr_IntArithmetic_1006(i308, iconst_3, iconst_1000, o644, i334, env, static) :|: i308 <= 1000 && iconst_3 = 3 && 0 <= i308 && iconst_1000 = 1000 && 0 <= i334 && 0 < o644
incr_IntArithmetic_1006(i308, iconst_3, iconst_1000, o644, i334, env, static) -{1,1}> incr_Duplicate_1008(i351, iconst_1000, o644, i334, env, static) :|: i308 <= 1000 && i308 + iconst_3 = i351 && i351 <= 1003 && iconst_3 = 3 && 0 <= i308 && iconst_1000 = 1000 && 3 <= i351 && 0 <= i334 && 0 < o644
incr_Duplicate_1008(i351, iconst_1000, o644, i334, env, static) -{1,1}> incr_Store_1010(i351, iconst_1000, o644, i334, env, static) :|: i351 <= 1003 && iconst_1000 = 1000 && 3 <= i351 && 0 <= i334 && 0 < o644
incr_Store_1010(i351, iconst_1000, o644, i334, env, static) -{1,1}> incr_Return_1012(i351, iconst_1000, o644, i334, env, static) :|: i351 <= 1003 && iconst_1000 = 1000 && 3 <= i351 && 0 <= i334 && 0 < o644
incr_Return_1012(i351, iconst_1000, o644, i334, env, static) -{1,1}> add_Store_1013(i351, iconst_1000, o644, i334, env, static) :|: i351 <= 1003 && iconst_1000 = 1000 && 3 <= i351 && 0 <= i334 && 0 < o644
add_Store_1013(i351, iconst_1000, o644, i334, env, static) -{1,1}> add_JMP_1017(iconst_1000, o644, i334, i351, env, static) :|: i351 <= 1003 && iconst_1000 = 1000 && 3 <= i351 && 0 <= i334 && 0 < o644
add_JMP_1017(iconst_1000, o644, i334, i351, env, static) -{1,1}> add_Load_1021(iconst_1000, o644, i334, i351, env, static) :|: i351 <= 1003 && iconst_1000 = 1000 && 3 <= i351 && 0 <= i334 && 0 < o644
add_Load_1021(iconst_1000, o644, i334, i351, env, static) -{0,0}> add_Load_954(iconst_1000, o644, i334, i351, env, static) :|: i351 <= 1003 && 0 <= i351 && iconst_1000 = 1000 && 3 <= i351 && 0 <= i334 && 0 < o644

(30) Obligation:

IntTrs with 8 rules
Start term: main_ConstantStackPush_2(env, static)
Considered paths: all paths from start
Rules:
main_ConstantStackPush_2(env, static) -{39,39}> add_Load_283(1000, 1, 0, 0, 1, env, static'1) :|: 0 >= 0 && 0 <= 1 && 0 < 2 && 0 <= 0 && 0 <= static'1 && 0 <= static && 0 < 1 && 0 <= 2 && static''' <= static + 2 && 0 <= static''' && static'1 <= static''' + 1
add_Load_283(1000, o30, i10, i11, o31, env, static) -{2,2}> add_GT_299(i11, 1000, o30, i10, o31, env, static) :|: 0 < o31 && 0 <= i11 && 0 <= i10 && 0 < o30
add_GT_299(i19, 1000, o30, i10, o31, env, static) -{22,22}> add_Load_599(1000, 1, 0, 0, o31, env, static) :|: 1001 <= i19 && 0 <= 0 && 0 < o30 && 0 < 1 && 0 <= i10 && 0 <= 4 && 0 < o31 && 0 <= 2 && 0 <= i19 && 1000 < i19
add_Load_599(1000, o227, i104, i105, o228, env, static) -{2,2}> add_GT_602(i105, 1000, o227, i104, o228, env, static) :|: 0 < o228 && 0 <= i104 && 0 < o227 && 0 <= i105
add_GT_602(i113, 1000, o227, i104, o228, env, static) -{25,25}> add_Load_954(1000, 1, 0, 0, env, static) :|: 0 <= i113 && 0 <= 3 && 1000 < i113 && 0 <= i104 && 0 <= 0 && 0 < o227 && 0 <= 6 && 0 < 1 && 1001 <= i113 && 0 < o228
add_Load_954(1000, o644, i296, i297, env, static) -{18,18}> add_Load_954(1000, o644, i334', i351', env, static) :|: i297 <= 1000 && 0 < o644 && 0 <= i296 && 0 <= i334' && 0 <= i297 && 3 <= i351' && i351' <= 1003 && 0 <= i351' && i296 + i297 = i334' && i297 + 3 = i351'
add_GT_602(i112, 1000, o227, i104, o228, env, static) -{16,16}> add_Load_599(1000, o227, i126', i135', o228, env, static) :|: 0 <= i104 && 0 <= i126' && i112 <= 1000 && 0 < o228 && 0 < o227 && 0 <= i135' && i104 + i112 = i126' && 2 <= i135' && i135' <= 1002 && 0 <= i112 && i112 + 2 = i135'
add_GT_299(i18, 1000, o30, i10, o31, env, static) -{16,16}> add_Load_283(1000, o30, i20', i21', o31, env, static) :|: i18 <= 1000 && i18 + 1 = i21' && i21' <= 1001 && 0 <= i20' && 0 < o31 && 0 < o30 && 0 <= i21' && 0 <= i18 && 1 <= i21' && i10 + i18 = i20' && 0 <= i10

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

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

main_ConstantStackPush_2(x1, x2) → main_ConstantStackPush_2(x2)
add_Load_283(x1, x2, x3, x4, x5, x6, x7) → add_Load_283(x2, x3, x4, x5)
add_GT_299(x1, x2, x3, x4, x5, x6, x7) → add_GT_299(x1, x3, x4, x5)
add_Load_599(x1, x2, x3, x4, x5, x6, x7) → add_Load_599(x2, x3, x4, x5)
add_GT_602(x1, x2, x3, x4, x5, x6, x7) → add_GT_602(x1, x3, x4, x5)
add_Load_954(x1, x2, x3, x4, x5, x6) → add_Load_954(x2, x3, x4)

(32) Obligation:

IntTrs with 8 rules
Start term: main_ConstantStackPush_2(static)
Considered paths: all paths from start
Rules:
main_ConstantStackPush_2(static) -{39,39}> add_Load_283(1, 0, 0, 1) :|: 0 >= 0 && 0 <= 1 && 0 < 2 && 0 <= 0 && 0 <= static'1 && 0 <= static && 0 < 1 && 0 <= 2 && static''' <= static + 2 && 0 <= static''' && static'1 <= static''' + 1
add_Load_283(o30, i10, i11, o31) -{2,2}> add_GT_299(i11, o30, i10, o31) :|: 0 < o31 && 0 <= i11 && 0 <= i10 && 0 < o30
add_GT_299(i19, o30, i10, o31) -{22,22}> add_Load_599(1, 0, 0, o31) :|: 1001 <= i19 && 0 <= 0 && 0 < o30 && 0 < 1 && 0 <= i10 && 0 <= 4 && 0 < o31 && 0 <= 2 && 0 <= i19 && 1000 < i19
add_Load_599(o227, i104, i105, o228) -{2,2}> add_GT_602(i105, o227, i104, o228) :|: 0 < o228 && 0 <= i104 && 0 < o227 && 0 <= i105
add_GT_602(i113, o227, i104, o228) -{25,25}> add_Load_954(1, 0, 0) :|: 0 <= i113 && 0 <= 3 && 1000 < i113 && 0 <= i104 && 0 <= 0 && 0 < o227 && 0 <= 6 && 0 < 1 && 1001 <= i113 && 0 < o228
add_Load_954(o644, i296, i297) -{18,18}> add_Load_954(o644, i334', i351') :|: i297 <= 1000 && 0 < o644 && 0 <= i296 && 0 <= i334' && 0 <= i297 && 3 <= i351' && i351' <= 1003 && 0 <= i351' && i296 + i297 = i334' && i297 + 3 = i351'
add_GT_602(i112, o227, i104, o228) -{16,16}> add_Load_599(o227, i126', i135', o228) :|: 0 <= i104 && 0 <= i126' && i112 <= 1000 && 0 < o228 && 0 < o227 && 0 <= i135' && i104 + i112 = i126' && 2 <= i135' && i135' <= 1002 && 0 <= i112 && i112 + 2 = i135'
add_GT_299(i18, o30, i10, o31) -{16,16}> add_Load_283(o30, i20', i21', o31) :|: i18 <= 1000 && i18 + 1 = i21' && i21' <= 1001 && 0 <= i20' && 0 < o31 && 0 < o30 && 0 <= i21' && 0 <= i18 && 1 <= i21' && i10 + i18 = i20' && 0 <= i10

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

Moved arithmethic from constraints to rhss.

add_GT_602(i112, o227, i104, o228) -{16,16}> add_Load_599(o227, i126', i135', o228) :|: 0 <= i104 && 0 <= i126' && i112 <= 1000 && 0 < o228 && 0 < o227 && 0 <= i135' && i104 + i112 = i126' && 2 <= i135' && i135' <= 1002 && 0 <= i112 && i112 + 2 = i135'
was transformed to
add_GT_602(i112, o227, i104, o228) -{16,16}> add_Load_599(o227, i104 + i112, i112 + 2, o228) :|: 0 <= i104 && 0 <= i126' && i112 <= 1000 && 0 < o228 && 0 < o227 && 0 <= i135' && i104 + i112 = i126' && 2 <= i135' && i135' <= 1002 && 0 <= i112 && i112 + 2 = i135'

add_GT_299(i18, o30, i10, o31) -{16,16}> add_Load_283(o30, i20', i21', o31) :|: i18 <= 1000 && i18 + 1 = i21' && i21' <= 1001 && 0 <= i20' && 0 < o31 && 0 < o30 && 0 <= i21' && 0 <= i18 && 1 <= i21' && i10 + i18 = i20' && 0 <= i10
was transformed to
add_GT_299(i18, o30, i10, o31) -{16,16}> add_Load_283(o30, i10 + i18, i18 + 1, o31) :|: i18 <= 1000 && i18 + 1 = i21' && i21' <= 1001 && 0 <= i20' && 0 < o31 && 0 < o30 && 0 <= i21' && 0 <= i18 && 1 <= i21' && i10 + i18 = i20' && 0 <= i10

add_Load_954(o644, i296, i297) -{18,18}> add_Load_954(o644, i334', i351') :|: i297 <= 1000 && 0 < o644 && 0 <= i296 && 0 <= i334' && 0 <= i297 && 3 <= i351' && i351' <= 1003 && 0 <= i351' && i296 + i297 = i334' && i297 + 3 = i351'
was transformed to
add_Load_954(o644, i296, i297) -{18,18}> add_Load_954(o644, i296 + i297, i297 + 3) :|: i297 <= 1000 && 0 < o644 && 0 <= i296 && 0 <= i334' && 0 <= i297 && 3 <= i351' && i351' <= 1003 && 0 <= i351' && i296 + i297 = i334' && i297 + 3 = i351'

(34) Obligation:

IntTrs with 8 rules
Start term: main_ConstantStackPush_2(static)
Considered paths: all paths from start
Rules:
add_GT_602(i113, o227, i104, o228) -{25,25}> add_Load_954(1, 0, 0) :|: 0 <= i113 && 0 <= 3 && 1000 < i113 && 0 <= i104 && 0 <= 0 && 0 < o227 && 0 <= 6 && 0 < 1 && 1001 <= i113 && 0 < o228
add_GT_602(i112, o227, i104, o228) -{16,16}> add_Load_599(o227, i104 + i112, i112 + 2, o228) :|: 0 <= i104 && 0 <= i126' && i112 <= 1000 && 0 < o228 && 0 < o227 && 0 <= i135' && i104 + i112 = i126' && 2 <= i135' && i135' <= 1002 && 0 <= i112 && i112 + 2 = i135'
add_GT_299(i19, o30, i10, o31) -{22,22}> add_Load_599(1, 0, 0, o31) :|: 1001 <= i19 && 0 <= 0 && 0 < o30 && 0 < 1 && 0 <= i10 && 0 <= 4 && 0 < o31 && 0 <= 2 && 0 <= i19 && 1000 < i19
main_ConstantStackPush_2(static) -{39,39}> add_Load_283(1, 0, 0, 1) :|: 0 >= 0 && 0 <= 1 && 0 < 2 && 0 <= 0 && 0 <= static'1 && 0 <= static && 0 < 1 && 0 <= 2 && static''' <= static + 2 && 0 <= static''' && static'1 <= static''' + 1
add_GT_299(i18, o30, i10, o31) -{16,16}> add_Load_283(o30, i10 + i18, i18 + 1, o31) :|: i18 <= 1000 && i18 + 1 = i21' && i21' <= 1001 && 0 <= i20' && 0 < o31 && 0 < o30 && 0 <= i21' && 0 <= i18 && 1 <= i21' && i10 + i18 = i20' && 0 <= i10
add_Load_954(o644, i296, i297) -{18,18}> add_Load_954(o644, i296 + i297, i297 + 3) :|: i297 <= 1000 && 0 < o644 && 0 <= i296 && 0 <= i334' && 0 <= i297 && 3 <= i351' && i351' <= 1003 && 0 <= i351' && i296 + i297 = i334' && i297 + 3 = i351'
add_Load_599(o227, i104, i105, o228) -{2,2}> add_GT_602(i105, o227, i104, o228) :|: 0 < o228 && 0 <= i104 && 0 < o227 && 0 <= i105
add_Load_283(o30, i10, i11, o31) -{2,2}> add_GT_299(i11, o30, i10, o31) :|: 0 < o31 && 0 <= i11 && 0 <= i10 && 0 < o30

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

Simplified expressions.

add_GT_602(i113, o227, i104, o228) -{25,25}> add_Load_954(1, 0, 0) :|: 0 <= i113 && 0 <= 3 && 1000 < i113 && 0 <= i104 && 0 <= 0 && 0 < o227 && 0 <= 6 && 0 < 1 && 1001 <= i113 && 0 < o228
was transformed to
add_GT_602(i113, o227, i104, o228) -{25,25}> add_Load_954(1, 0, 0) :|: 0 <= i113 && 1000 < i113 && 0 <= i104 && 0 < o227 && 1001 <= i113 && 0 < o228

add_GT_299(i19, o30, i10, o31) -{22,22}> add_Load_599(1, 0, 0, o31) :|: 1001 <= i19 && 0 <= 0 && 0 < o30 && 0 < 1 && 0 <= i10 && 0 <= 4 && 0 < o31 && 0 <= 2 && 0 <= i19 && 1000 < i19
was transformed to
add_GT_299(i19, o30, i10, o31) -{22,22}> add_Load_599(1, 0, 0, o31) :|: 1001 <= i19 && 0 < o30 && 0 <= i10 && 0 < o31 && 0 <= i19 && 1000 < i19

main_ConstantStackPush_2(static) -{39,39}> add_Load_283(1, 0, 0, 1) :|: 0 >= 0 && 0 <= 1 && 0 < 2 && 0 <= 0 && 0 <= static'1 && 0 <= static && 0 < 1 && 0 <= 2 && static''' <= static + 2 && 0 <= static''' && static'1 <= static''' + 1
was transformed to
main_ConstantStackPush_2(static) -{39,39}> add_Load_283(1, 0, 0, 1) :|: 0 <= static'1 && 0 <= static && static''' <= static + 2 && 0 <= static''' && static'1 <= static''' + 1

(36) Obligation:

IntTrs with 8 rules
Start term: main_ConstantStackPush_2(static)
Considered paths: all paths from start
Rules:
add_GT_602(i112, o227, i104, o228) -{16,16}> add_Load_599(o227, i104 + i112, i112 + 2, o228) :|: 0 <= i104 && 0 <= i126' && i112 <= 1000 && 0 < o228 && 0 < o227 && 0 <= i135' && i104 + i112 = i126' && 2 <= i135' && i135' <= 1002 && 0 <= i112 && i112 + 2 = i135'
add_Load_599(o227, i104, i105, o228) -{2,2}> add_GT_602(i105, o227, i104, o228) :|: 0 < o228 && 0 <= i104 && 0 < o227 && 0 <= i105
add_Load_283(o30, i10, i11, o31) -{2,2}> add_GT_299(i11, o30, i10, o31) :|: 0 < o31 && 0 <= i11 && 0 <= i10 && 0 < o30
add_Load_954(o644, i296, i297) -{18,18}> add_Load_954(o644, i296 + i297, i297 + 3) :|: i297 <= 1000 && 0 < o644 && 0 <= i296 && 0 <= i334' && 0 <= i297 && 3 <= i351' && i351' <= 1003 && 0 <= i351' && i296 + i297 = i334' && i297 + 3 = i351'
main_ConstantStackPush_2(static) -{39,39}> add_Load_283(1, 0, 0, 1) :|: 0 <= static'1 && 0 <= static && static''' <= static + 2 && 0 <= static''' && static'1 <= static''' + 1
add_GT_602(i113, o227, i104, o228) -{25,25}> add_Load_954(1, 0, 0) :|: 0 <= i113 && 1000 < i113 && 0 <= i104 && 0 < o227 && 1001 <= i113 && 0 < o228
add_GT_299(i19, o30, i10, o31) -{22,22}> add_Load_599(1, 0, 0, o31) :|: 1001 <= i19 && 0 < o30 && 0 <= i10 && 0 < o31 && 0 <= i19 && 1000 < i19
add_GT_299(i18, o30, i10, o31) -{16,16}> add_Load_283(o30, i10 + i18, i18 + 1, o31) :|: i18 <= 1000 && i18 + 1 = i21' && i21' <= 1001 && 0 <= i20' && 0 < o31 && 0 < o30 && 0 <= i21' && 0 <= i18 && 1 <= i21' && i10 + i18 = i20' && 0 <= i10

(37) koat Proof (EQUIVALENT transformation)

YES(?, 126265)

Initial complexity problem:
1: T:
(Comp: ?, Cost: 16) add_GT_602(ar_0, ar_1, ar_2, ar_3) -> Com_1(add_Load_599(ar_1, ar_2 + ar_0, ar_0 + 2, ar_3)) [ 0 <= ar_2 /\ 0 <= i126' /\ ar_0 <= 1000 /\ 0 < ar_3 /\ 0 < ar_1 /\ 0 <= i135' /\ ar_2 + ar_0 = i126' /\ 2 <= i135' /\ i135' <= 1002 /\ 0 <= ar_0 /\ ar_0 + 2 = i135' ]
(Comp: ?, Cost: 2) add_Load_599(ar_0, ar_1, ar_2, ar_3) -> Com_1(add_GT_602(ar_2, ar_0, ar_1, ar_3)) [ 0 < ar_3 /\ 0 <= ar_1 /\ 0 < ar_0 /\ 0 <= ar_2 ]
(Comp: ?, Cost: 2) add_Load_283(ar_0, ar_1, ar_2, ar_3) -> Com_1(add_GT_299(ar_2, ar_0, ar_1, ar_3)) [ 0 < ar_3 /\ 0 <= ar_2 /\ 0 <= ar_1 /\ 0 < ar_0 ]
(Comp: ?, Cost: 18) add_Load_954(ar_0, ar_1, ar_2, ar_3) -> Com_1(add_Load_954(ar_0, ar_1 + ar_2, ar_2 + 3, arityPad)) [ ar_2 <= 1000 /\ 0 < ar_0 /\ 0 <= ar_1 /\ 0 <= i334' /\ 0 <= ar_2 /\ 3 <= i351' /\ i351' <= 1003 /\ 0 <= i351' /\ ar_1 + ar_2 = i334' /\ ar_2 + 3 = i351' ]
(Comp: ?, Cost: 39) main_ConstantStackPush_2(ar_0, ar_1, ar_2, ar_3) -> Com_1(add_Load_283(1, 0, 0, 1)) [ 0 <= static'1 /\ 0 <= ar_0 /\ static''' <= ar_0 + 2 /\ 0 <= static''' /\ static'1 <= static''' + 1 ]
(Comp: ?, Cost: 25) add_GT_602(ar_0, ar_1, ar_2, ar_3) -> Com_1(add_Load_954(1, 0, 0, arityPad)) [ 0 <= ar_0 /\ 1000 < ar_0 /\ 0 <= ar_2 /\ 0 < ar_1 /\ 1001 <= ar_0 /\ 0 < ar_3 ]
(Comp: ?, Cost: 22) add_GT_299(ar_0, ar_1, ar_2, ar_3) -> Com_1(add_Load_599(1, 0, 0, ar_3)) [ 1001 <= ar_0 /\ 0 < ar_1 /\ 0 <= ar_2 /\ 0 < ar_3 /\ 0 <= ar_0 /\ 1000 < ar_0 ]
(Comp: ?, Cost: 16) add_GT_299(ar_0, ar_1, ar_2, ar_3) -> Com_1(add_Load_283(ar_1, ar_2 + ar_0, ar_0 + 1, ar_3)) [ ar_0 <= 1000 /\ ar_0 + 1 = i21' /\ i21' <= 1001 /\ 0 <= i20' /\ 0 < ar_3 /\ 0 < ar_1 /\ 0 <= i21' /\ 0 <= ar_0 /\ 1 <= i21' /\ ar_2 + ar_0 = i20' /\ 0 <= ar_2 ]
(Comp: 1, Cost: 0) koat_start(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_ConstantStackPush_2(ar_0, ar_1, ar_2, ar_3)) [ 0 <= 0 ]
start location: koat_start
leaf cost: 0

Repeatedly propagating knowledge in problem 1 produces the following problem:
2: T:
(Comp: ?, Cost: 16) add_GT_602(ar_0, ar_1, ar_2, ar_3) -> Com_1(add_Load_599(ar_1, ar_2 + ar_0, ar_0 + 2, ar_3)) [ 0 <= ar_2 /\ 0 <= i126' /\ ar_0 <= 1000 /\ 0 < ar_3 /\ 0 < ar_1 /\ 0 <= i135' /\ ar_2 + ar_0 = i126' /\ 2 <= i135' /\ i135' <= 1002 /\ 0 <= ar_0 /\ ar_0 + 2 = i135' ]
(Comp: ?, Cost: 2) add_Load_599(ar_0, ar_1, ar_2, ar_3) -> Com_1(add_GT_602(ar_2, ar_0, ar_1, ar_3)) [ 0 < ar_3 /\ 0 <= ar_1 /\ 0 < ar_0 /\ 0 <= ar_2 ]
(Comp: ?, Cost: 2) add_Load_283(ar_0, ar_1, ar_2, ar_3) -> Com_1(add_GT_299(ar_2, ar_0, ar_1, ar_3)) [ 0 < ar_3 /\ 0 <= ar_2 /\ 0 <= ar_1 /\ 0 < ar_0 ]
(Comp: ?, Cost: 18) add_Load_954(ar_0, ar_1, ar_2, ar_3) -> Com_1(add_Load_954(ar_0, ar_1 + ar_2, ar_2 + 3, arityPad)) [ ar_2 <= 1000 /\ 0 < ar_0 /\ 0 <= ar_1 /\ 0 <= i334' /\ 0 <= ar_2 /\ 3 <= i351' /\ i351' <= 1003 /\ 0 <= i351' /\ ar_1 + ar_2 = i334' /\ ar_2 + 3 = i351' ]
(Comp: 1, Cost: 39) main_ConstantStackPush_2(ar_0, ar_1, ar_2, ar_3) -> Com_1(add_Load_283(1, 0, 0, 1)) [ 0 <= static'1 /\ 0 <= ar_0 /\ static''' <= ar_0 + 2 /\ 0 <= static''' /\ static'1 <= static''' + 1 ]
(Comp: ?, Cost: 25) add_GT_602(ar_0, ar_1, ar_2, ar_3) -> Com_1(add_Load_954(1, 0, 0, arityPad)) [ 0 <= ar_0 /\ 1000 < ar_0 /\ 0 <= ar_2 /\ 0 < ar_1 /\ 1001 <= ar_0 /\ 0 < ar_3 ]
(Comp: ?, Cost: 22) add_GT_299(ar_0, ar_1, ar_2, ar_3) -> Com_1(add_Load_599(1, 0, 0, ar_3)) [ 1001 <= ar_0 /\ 0 < ar_1 /\ 0 <= ar_2 /\ 0 < ar_3 /\ 0 <= ar_0 /\ 1000 < ar_0 ]
(Comp: ?, Cost: 16) add_GT_299(ar_0, ar_1, ar_2, ar_3) -> Com_1(add_Load_283(ar_1, ar_2 + ar_0, ar_0 + 1, ar_3)) [ ar_0 <= 1000 /\ ar_0 + 1 = i21' /\ i21' <= 1001 /\ 0 <= i20' /\ 0 < ar_3 /\ 0 < ar_1 /\ 0 <= i21' /\ 0 <= ar_0 /\ 1 <= i21' /\ ar_2 + ar_0 = i20' /\ 0 <= ar_2 ]
(Comp: 1, Cost: 0) koat_start(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_ConstantStackPush_2(ar_0, ar_1, ar_2, ar_3)) [ 0 <= 0 ]
start location: koat_start
leaf cost: 0

A polynomial rank function with
Pol(add_GT_602) = 1
Pol(add_Load_599) = 1
Pol(add_Load_283) = 2
Pol(add_GT_299) = 2
Pol(add_Load_954) = 0
Pol(main_ConstantStackPush_2) = 2
Pol(koat_start) = 2
orients all transitions weakly and the transitions
add_GT_602(ar_0, ar_1, ar_2, ar_3) -> Com_1(add_Load_954(1, 0, 0, arityPad)) [ 0 <= ar_0 /\ 1000 < ar_0 /\ 0 <= ar_2 /\ 0 < ar_1 /\ 1001 <= ar_0 /\ 0 < ar_3 ]
add_GT_299(ar_0, ar_1, ar_2, ar_3) -> Com_1(add_Load_599(1, 0, 0, ar_3)) [ 1001 <= ar_0 /\ 0 < ar_1 /\ 0 <= ar_2 /\ 0 < ar_3 /\ 0 <= ar_0 /\ 1000 < ar_0 ]
strictly and produces the following problem:
3: T:
(Comp: ?, Cost: 16) add_GT_602(ar_0, ar_1, ar_2, ar_3) -> Com_1(add_Load_599(ar_1, ar_2 + ar_0, ar_0 + 2, ar_3)) [ 0 <= ar_2 /\ 0 <= i126' /\ ar_0 <= 1000 /\ 0 < ar_3 /\ 0 < ar_1 /\ 0 <= i135' /\ ar_2 + ar_0 = i126' /\ 2 <= i135' /\ i135' <= 1002 /\ 0 <= ar_0 /\ ar_0 + 2 = i135' ]
(Comp: ?, Cost: 2) add_Load_599(ar_0, ar_1, ar_2, ar_3) -> Com_1(add_GT_602(ar_2, ar_0, ar_1, ar_3)) [ 0 < ar_3 /\ 0 <= ar_1 /\ 0 < ar_0 /\ 0 <= ar_2 ]
(Comp: ?, Cost: 2) add_Load_283(ar_0, ar_1, ar_2, ar_3) -> Com_1(add_GT_299(ar_2, ar_0, ar_1, ar_3)) [ 0 < ar_3 /\ 0 <= ar_2 /\ 0 <= ar_1 /\ 0 < ar_0 ]
(Comp: ?, Cost: 18) add_Load_954(ar_0, ar_1, ar_2, ar_3) -> Com_1(add_Load_954(ar_0, ar_1 + ar_2, ar_2 + 3, arityPad)) [ ar_2 <= 1000 /\ 0 < ar_0 /\ 0 <= ar_1 /\ 0 <= i334' /\ 0 <= ar_2 /\ 3 <= i351' /\ i351' <= 1003 /\ 0 <= i351' /\ ar_1 + ar_2 = i334' /\ ar_2 + 3 = i351' ]
(Comp: 1, Cost: 39) main_ConstantStackPush_2(ar_0, ar_1, ar_2, ar_3) -> Com_1(add_Load_283(1, 0, 0, 1)) [ 0 <= static'1 /\ 0 <= ar_0 /\ static''' <= ar_0 + 2 /\ 0 <= static''' /\ static'1 <= static''' + 1 ]
(Comp: 2, Cost: 25) add_GT_602(ar_0, ar_1, ar_2, ar_3) -> Com_1(add_Load_954(1, 0, 0, arityPad)) [ 0 <= ar_0 /\ 1000 < ar_0 /\ 0 <= ar_2 /\ 0 < ar_1 /\ 1001 <= ar_0 /\ 0 < ar_3 ]
(Comp: 2, Cost: 22) add_GT_299(ar_0, ar_1, ar_2, ar_3) -> Com_1(add_Load_599(1, 0, 0, ar_3)) [ 1001 <= ar_0 /\ 0 < ar_1 /\ 0 <= ar_2 /\ 0 < ar_3 /\ 0 <= ar_0 /\ 1000 < ar_0 ]
(Comp: ?, Cost: 16) add_GT_299(ar_0, ar_1, ar_2, ar_3) -> Com_1(add_Load_283(ar_1, ar_2 + ar_0, ar_0 + 1, ar_3)) [ ar_0 <= 1000 /\ ar_0 + 1 = i21' /\ i21' <= 1001 /\ 0 <= i20' /\ 0 < ar_3 /\ 0 < ar_1 /\ 0 <= i21' /\ 0 <= ar_0 /\ 1 <= i21' /\ ar_2 + ar_0 = i20' /\ 0 <= ar_2 ]
(Comp: 1, Cost: 0) koat_start(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_ConstantStackPush_2(ar_0, ar_1, ar_2, ar_3)) [ 0 <= 0 ]
start location: koat_start
leaf cost: 0

A polynomial rank function with
Pol(add_GT_602) = 1001*V_4
Pol(add_Load_599) = 1001*V_4
Pol(add_Load_283) = 1001*V_4
Pol(add_GT_299) = 1001*V_4
Pol(add_Load_954) = -V_3 + 1001
Pol(main_ConstantStackPush_2) = 1001
Pol(koat_start) = 1001
orients all transitions weakly and the transition
add_Load_954(ar_0, ar_1, ar_2, ar_3) -> Com_1(add_Load_954(ar_0, ar_1 + ar_2, ar_2 + 3, arityPad)) [ ar_2 <= 1000 /\ 0 < ar_0 /\ 0 <= ar_1 /\ 0 <= i334' /\ 0 <= ar_2 /\ 3 <= i351' /\ i351' <= 1003 /\ 0 <= i351' /\ ar_1 + ar_2 = i334' /\ ar_2 + 3 = i351' ]
strictly and produces the following problem:
4: T:
(Comp: ?, Cost: 16) add_GT_602(ar_0, ar_1, ar_2, ar_3) -> Com_1(add_Load_599(ar_1, ar_2 + ar_0, ar_0 + 2, ar_3)) [ 0 <= ar_2 /\ 0 <= i126' /\ ar_0 <= 1000 /\ 0 < ar_3 /\ 0 < ar_1 /\ 0 <= i135' /\ ar_2 + ar_0 = i126' /\ 2 <= i135' /\ i135' <= 1002 /\ 0 <= ar_0 /\ ar_0 + 2 = i135' ]
(Comp: ?, Cost: 2) add_Load_599(ar_0, ar_1, ar_2, ar_3) -> Com_1(add_GT_602(ar_2, ar_0, ar_1, ar_3)) [ 0 < ar_3 /\ 0 <= ar_1 /\ 0 < ar_0 /\ 0 <= ar_2 ]
(Comp: ?, Cost: 2) add_Load_283(ar_0, ar_1, ar_2, ar_3) -> Com_1(add_GT_299(ar_2, ar_0, ar_1, ar_3)) [ 0 < ar_3 /\ 0 <= ar_2 /\ 0 <= ar_1 /\ 0 < ar_0 ]
(Comp: 1001, Cost: 18) add_Load_954(ar_0, ar_1, ar_2, ar_3) -> Com_1(add_Load_954(ar_0, ar_1 + ar_2, ar_2 + 3, arityPad)) [ ar_2 <= 1000 /\ 0 < ar_0 /\ 0 <= ar_1 /\ 0 <= i334' /\ 0 <= ar_2 /\ 3 <= i351' /\ i351' <= 1003 /\ 0 <= i351' /\ ar_1 + ar_2 = i334' /\ ar_2 + 3 = i351' ]
(Comp: 1, Cost: 39) main_ConstantStackPush_2(ar_0, ar_1, ar_2, ar_3) -> Com_1(add_Load_283(1, 0, 0, 1)) [ 0 <= static'1 /\ 0 <= ar_0 /\ static''' <= ar_0 + 2 /\ 0 <= static''' /\ static'1 <= static''' + 1 ]
(Comp: 2, Cost: 25) add_GT_602(ar_0, ar_1, ar_2, ar_3) -> Com_1(add_Load_954(1, 0, 0, arityPad)) [ 0 <= ar_0 /\ 1000 < ar_0 /\ 0 <= ar_2 /\ 0 < ar_1 /\ 1001 <= ar_0 /\ 0 < ar_3 ]
(Comp: 2, Cost: 22) add_GT_299(ar_0, ar_1, ar_2, ar_3) -> Com_1(add_Load_599(1, 0, 0, ar_3)) [ 1001 <= ar_0 /\ 0 < ar_1 /\ 0 <= ar_2 /\ 0 < ar_3 /\ 0 <= ar_0 /\ 1000 < ar_0 ]
(Comp: ?, Cost: 16) add_GT_299(ar_0, ar_1, ar_2, ar_3) -> Com_1(add_Load_283(ar_1, ar_2 + ar_0, ar_0 + 1, ar_3)) [ ar_0 <= 1000 /\ ar_0 + 1 = i21' /\ i21' <= 1001 /\ 0 <= i20' /\ 0 < ar_3 /\ 0 < ar_1 /\ 0 <= i21' /\ 0 <= ar_0 /\ 1 <= i21' /\ ar_2 + ar_0 = i20' /\ 0 <= ar_2 ]
(Comp: 1, Cost: 0) koat_start(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_ConstantStackPush_2(ar_0, ar_1, ar_2, ar_3)) [ 0 <= 0 ]
start location: koat_start
leaf cost: 0

A polynomial rank function with
Pol(add_Load_599) = -V_3 + 1001
Pol(add_GT_602) = -V_1 + 1001
Pol(add_Load_283) = -V_3 + 1001
Pol(add_GT_299) = -V_1 + 1001
and size complexities
S("koat_start(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_ConstantStackPush_2(ar_0, ar_1, ar_2, ar_3)) [ 0 <= 0 ]", 0-0) = ar_0
S("koat_start(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_ConstantStackPush_2(ar_0, ar_1, ar_2, ar_3)) [ 0 <= 0 ]", 0-1) = ar_1
S("koat_start(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_ConstantStackPush_2(ar_0, ar_1, ar_2, ar_3)) [ 0 <= 0 ]", 0-2) = ar_2
S("koat_start(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_ConstantStackPush_2(ar_0, ar_1, ar_2, ar_3)) [ 0 <= 0 ]", 0-3) = ar_3
S("add_GT_299(ar_0, ar_1, ar_2, ar_3) -> Com_1(add_Load_283(ar_1, ar_2 + ar_0, ar_0 + 1, ar_3)) [ ar_0 <= 1000 /\\ ar_0 + 1 = i21' /\\ i21' <= 1001 /\\ 0 <= i20' /\\ 0 < ar_3 /\\ 0 < ar_1 /\\ 0 <= i21' /\\ 0 <= ar_0 /\\ 1 <= i21' /\\ ar_2 + ar_0 = i20' /\\ 0 <= ar_2 ]", 0-0) = 1
S("add_GT_299(ar_0, ar_1, ar_2, ar_3) -> Com_1(add_Load_283(ar_1, ar_2 + ar_0, ar_0 + 1, ar_3)) [ ar_0 <= 1000 /\\ ar_0 + 1 = i21' /\\ i21' <= 1001 /\\ 0 <= i20' /\\ 0 < ar_3 /\\ 0 < ar_1 /\\ 0 <= i21' /\\ 0 <= ar_0 /\\ 1 <= i21' /\\ ar_2 + ar_0 = i20' /\\ 0 <= ar_2 ]", 0-1) = ?
S("add_GT_299(ar_0, ar_1, ar_2, ar_3) -> Com_1(add_Load_283(ar_1, ar_2 + ar_0, ar_0 + 1, ar_3)) [ ar_0 <= 1000 /\\ ar_0 + 1 = i21' /\\ i21' <= 1001 /\\ 0 <= i20' /\\ 0 < ar_3 /\\ 0 < ar_1 /\\ 0 <= i21' /\\ 0 <= ar_0 /\\ 1 <= i21' /\\ ar_2 + ar_0 = i20' /\\ 0 <= ar_2 ]", 0-2) = 1001
S("add_GT_299(ar_0, ar_1, ar_2, ar_3) -> Com_1(add_Load_283(ar_1, ar_2 + ar_0, ar_0 + 1, ar_3)) [ ar_0 <= 1000 /\\ ar_0 + 1 = i21' /\\ i21' <= 1001 /\\ 0 <= i20' /\\ 0 < ar_3 /\\ 0 < ar_1 /\\ 0 <= i21' /\\ 0 <= ar_0 /\\ 1 <= i21' /\\ ar_2 + ar_0 = i20' /\\ 0 <= ar_2 ]", 0-3) = 1
S("add_GT_299(ar_0, ar_1, ar_2, ar_3) -> Com_1(add_Load_599(1, 0, 0, ar_3)) [ 1001 <= ar_0 /\\ 0 < ar_1 /\\ 0 <= ar_2 /\\ 0 < ar_3 /\\ 0 <= ar_0 /\\ 1000 < ar_0 ]", 0-0) = 1
S("add_GT_299(ar_0, ar_1, ar_2, ar_3) -> Com_1(add_Load_599(1, 0, 0, ar_3)) [ 1001 <= ar_0 /\\ 0 < ar_1 /\\ 0 <= ar_2 /\\ 0 < ar_3 /\\ 0 <= ar_0 /\\ 1000 < ar_0 ]", 0-1) = 0
S("add_GT_299(ar_0, ar_1, ar_2, ar_3) -> Com_1(add_Load_599(1, 0, 0, ar_3)) [ 1001 <= ar_0 /\\ 0 < ar_1 /\\ 0 <= ar_2 /\\ 0 < ar_3 /\\ 0 <= ar_0 /\\ 1000 < ar_0 ]", 0-2) = 0
S("add_GT_299(ar_0, ar_1, ar_2, ar_3) -> Com_1(add_Load_599(1, 0, 0, ar_3)) [ 1001 <= ar_0 /\\ 0 < ar_1 /\\ 0 <= ar_2 /\\ 0 < ar_3 /\\ 0 <= ar_0 /\\ 1000 < ar_0 ]", 0-3) = 1
S("add_GT_602(ar_0, ar_1, ar_2, ar_3) -> Com_1(add_Load_954(1, 0, 0, arityPad)) [ 0 <= ar_0 /\\ 1000 < ar_0 /\\ 0 <= ar_2 /\\ 0 < ar_1 /\\ 1001 <= ar_0 /\\ 0 < ar_3 ]", 0-0) = 1
S("add_GT_602(ar_0, ar_1, ar_2, ar_3) -> Com_1(add_Load_954(1, 0, 0, arityPad)) [ 0 <= ar_0 /\\ 1000 < ar_0 /\\ 0 <= ar_2 /\\ 0 < ar_1 /\\ 1001 <= ar_0 /\\ 0 < ar_3 ]", 0-1) = 0
S("add_GT_602(ar_0, ar_1, ar_2, ar_3) -> Com_1(add_Load_954(1, 0, 0, arityPad)) [ 0 <= ar_0 /\\ 1000 < ar_0 /\\ 0 <= ar_2 /\\ 0 < ar_1 /\\ 1001 <= ar_0 /\\ 0 < ar_3 ]", 0-2) = 0
S("add_GT_602(ar_0, ar_1, ar_2, ar_3) -> Com_1(add_Load_954(1, 0, 0, arityPad)) [ 0 <= ar_0 /\\ 1000 < ar_0 /\\ 0 <= ar_2 /\\ 0 < ar_1 /\\ 1001 <= ar_0 /\\ 0 < ar_3 ]", 0-3) = ?
S("main_ConstantStackPush_2(ar_0, ar_1, ar_2, ar_3) -> Com_1(add_Load_283(1, 0, 0, 1)) [ 0 <= static'1 /\\ 0 <= ar_0 /\\ static''' <= ar_0 + 2 /\\ 0 <= static''' /\\ static'1 <= static''' + 1 ]", 0-0) = 1
S("main_ConstantStackPush_2(ar_0, ar_1, ar_2, ar_3) -> Com_1(add_Load_283(1, 0, 0, 1)) [ 0 <= static'1 /\\ 0 <= ar_0 /\\ static''' <= ar_0 + 2 /\\ 0 <= static''' /\\ static'1 <= static''' + 1 ]", 0-1) = 0
S("main_ConstantStackPush_2(ar_0, ar_1, ar_2, ar_3) -> Com_1(add_Load_283(1, 0, 0, 1)) [ 0 <= static'1 /\\ 0 <= ar_0 /\\ static''' <= ar_0 + 2 /\\ 0 <= static''' /\\ static'1 <= static''' + 1 ]", 0-2) = 0
S("main_ConstantStackPush_2(ar_0, ar_1, ar_2, ar_3) -> Com_1(add_Load_283(1, 0, 0, 1)) [ 0 <= static'1 /\\ 0 <= ar_0 /\\ static''' <= ar_0 + 2 /\\ 0 <= static''' /\\ static'1 <= static''' + 1 ]", 0-3) = 1
S("add_Load_954(ar_0, ar_1, ar_2, ar_3) -> Com_1(add_Load_954(ar_0, ar_1 + ar_2, ar_2 + 3, arityPad)) [ ar_2 <= 1000 /\\ 0 < ar_0 /\\ 0 <= ar_1 /\\ 0 <= i334' /\\ 0 <= ar_2 /\\ 3 <= i351' /\\ i351' <= 1003 /\\ 0 <= i351' /\\ ar_1 + ar_2 = i334' /\\ ar_2 + 3 = i351' ]", 0-0) = 1
S("add_Load_954(ar_0, ar_1, ar_2, ar_3) -> Com_1(add_Load_954(ar_0, ar_1 + ar_2, ar_2 + 3, arityPad)) [ ar_2 <= 1000 /\\ 0 < ar_0 /\\ 0 <= ar_1 /\\ 0 <= i334' /\\ 0 <= ar_2 /\\ 3 <= i351' /\\ i351' <= 1003 /\\ 0 <= i351' /\\ ar_1 + ar_2 = i334' /\\ ar_2 + 3 = i351' ]", 0-1) = 1001000
S("add_Load_954(ar_0, ar_1, ar_2, ar_3) -> Com_1(add_Load_954(ar_0, ar_1 + ar_2, ar_2 + 3, arityPad)) [ ar_2 <= 1000 /\\ 0 < ar_0 /\\ 0 <= ar_1 /\\ 0 <= i334' /\\ 0 <= ar_2 /\\ 3 <= i351' /\\ i351' <= 1003 /\\ 0 <= i351' /\\ ar_1 + ar_2 = i334' /\\ ar_2 + 3 = i351' ]", 0-2) = 1003
S("add_Load_954(ar_0, ar_1, ar_2, ar_3) -> Com_1(add_Load_954(ar_0, ar_1 + ar_2, ar_2 + 3, arityPad)) [ ar_2 <= 1000 /\\ 0 < ar_0 /\\ 0 <= ar_1 /\\ 0 <= i334' /\\ 0 <= ar_2 /\\ 3 <= i351' /\\ i351' <= 1003 /\\ 0 <= i351' /\\ ar_1 + ar_2 = i334' /\\ ar_2 + 3 = i351' ]", 0-3) = ?
S("add_Load_283(ar_0, ar_1, ar_2, ar_3) -> Com_1(add_GT_299(ar_2, ar_0, ar_1, ar_3)) [ 0 < ar_3 /\\ 0 <= ar_2 /\\ 0 <= ar_1 /\\ 0 < ar_0 ]", 0-0) = 1001
S("add_Load_283(ar_0, ar_1, ar_2, ar_3) -> Com_1(add_GT_299(ar_2, ar_0, ar_1, ar_3)) [ 0 < ar_3 /\\ 0 <= ar_2 /\\ 0 <= ar_1 /\\ 0 < ar_0 ]", 0-1) = 1
S("add_Load_283(ar_0, ar_1, ar_2, ar_3) -> Com_1(add_GT_299(ar_2, ar_0, ar_1, ar_3)) [ 0 < ar_3 /\\ 0 <= ar_2 /\\ 0 <= ar_1 /\\ 0 < ar_0 ]", 0-2) = ?
S("add_Load_283(ar_0, ar_1, ar_2, ar_3) -> Com_1(add_GT_299(ar_2, ar_0, ar_1, ar_3)) [ 0 < ar_3 /\\ 0 <= ar_2 /\\ 0 <= ar_1 /\\ 0 < ar_0 ]", 0-3) = 1
S("add_Load_599(ar_0, ar_1, ar_2, ar_3) -> Com_1(add_GT_602(ar_2, ar_0, ar_1, ar_3)) [ 0 < ar_3 /\\ 0 <= ar_1 /\\ 0 < ar_0 /\\ 0 <= ar_2 ]", 0-0) = 1002
S("add_Load_599(ar_0, ar_1, ar_2, ar_3) -> Com_1(add_GT_602(ar_2, ar_0, ar_1, ar_3)) [ 0 < ar_3 /\\ 0 <= ar_1 /\\ 0 < ar_0 /\\ 0 <= ar_2 ]", 0-1) = 1
S("add_Load_599(ar_0, ar_1, ar_2, ar_3) -> Com_1(add_GT_602(ar_2, ar_0, ar_1, ar_3)) [ 0 < ar_3 /\\ 0 <= ar_1 /\\ 0 < ar_0 /\\ 0 <= ar_2 ]", 0-2) = ?
S("add_Load_599(ar_0, ar_1, ar_2, ar_3) -> Com_1(add_GT_602(ar_2, ar_0, ar_1, ar_3)) [ 0 < ar_3 /\\ 0 <= ar_1 /\\ 0 < ar_0 /\\ 0 <= ar_2 ]", 0-3) = 1
S("add_GT_602(ar_0, ar_1, ar_2, ar_3) -> Com_1(add_Load_599(ar_1, ar_2 + ar_0, ar_0 + 2, ar_3)) [ 0 <= ar_2 /\\ 0 <= i126' /\\ ar_0 <= 1000 /\\ 0 < ar_3 /\\ 0 < ar_1 /\\ 0 <= i135' /\\ ar_2 + ar_0 = i126' /\\ 2 <= i135' /\\ i135' <= 1002 /\\ 0 <= ar_0 /\\ ar_0 + 2 = i135' ]", 0-0) = 1
S("add_GT_602(ar_0, ar_1, ar_2, ar_3) -> Com_1(add_Load_599(ar_1, ar_2 + ar_0, ar_0 + 2, ar_3)) [ 0 <= ar_2 /\\ 0 <= i126' /\\ ar_0 <= 1000 /\\ 0 < ar_3 /\\ 0 < ar_1 /\\ 0 <= i135' /\\ ar_2 + ar_0 = i126' /\\ 2 <= i135' /\\ i135' <= 1002 /\\ 0 <= ar_0 /\\ ar_0 + 2 = i135' ]", 0-1) = ?
S("add_GT_602(ar_0, ar_1, ar_2, ar_3) -> Com_1(add_Load_599(ar_1, ar_2 + ar_0, ar_0 + 2, ar_3)) [ 0 <= ar_2 /\\ 0 <= i126' /\\ ar_0 <= 1000 /\\ 0 < ar_3 /\\ 0 < ar_1 /\\ 0 <= i135' /\\ ar_2 + ar_0 = i126' /\\ 2 <= i135' /\\ i135' <= 1002 /\\ 0 <= ar_0 /\\ ar_0 + 2 = i135' ]", 0-2) = 1002
S("add_GT_602(ar_0, ar_1, ar_2, ar_3) -> Com_1(add_Load_599(ar_1, ar_2 + ar_0, ar_0 + 2, ar_3)) [ 0 <= ar_2 /\\ 0 <= i126' /\\ ar_0 <= 1000 /\\ 0 < ar_3 /\\ 0 < ar_1 /\\ 0 <= i135' /\\ ar_2 + ar_0 = i126' /\\ 2 <= i135' /\\ i135' <= 1002 /\\ 0 <= ar_0 /\\ ar_0 + 2 = i135' ]", 0-3) = 1
orients the transitions
add_Load_599(ar_0, ar_1, ar_2, ar_3) -> Com_1(add_GT_602(ar_2, ar_0, ar_1, ar_3)) [ 0 < ar_3 /\ 0 <= ar_1 /\ 0 < ar_0 /\ 0 <= ar_2 ]
add_Load_283(ar_0, ar_1, ar_2, ar_3) -> Com_1(add_GT_299(ar_2, ar_0, ar_1, ar_3)) [ 0 < ar_3 /\ 0 <= ar_2 /\ 0 <= ar_1 /\ 0 < ar_0 ]
add_GT_602(ar_0, ar_1, ar_2, ar_3) -> Com_1(add_Load_599(ar_1, ar_2 + ar_0, ar_0 + 2, ar_3)) [ 0 <= ar_2 /\ 0 <= i126' /\ ar_0 <= 1000 /\ 0 < ar_3 /\ 0 < ar_1 /\ 0 <= i135' /\ ar_2 + ar_0 = i126' /\ 2 <= i135' /\ i135' <= 1002 /\ 0 <= ar_0 /\ ar_0 + 2 = i135' ]
add_GT_299(ar_0, ar_1, ar_2, ar_3) -> Com_1(add_Load_283(ar_1, ar_2 + ar_0, ar_0 + 1, ar_3)) [ ar_0 <= 1000 /\ ar_0 + 1 = i21' /\ i21' <= 1001 /\ 0 <= i20' /\ 0 < ar_3 /\ 0 < ar_1 /\ 0 <= i21' /\ 0 <= ar_0 /\ 1 <= i21' /\ ar_2 + ar_0 = i20' /\ 0 <= ar_2 ]
weakly and the transitions
add_GT_602(ar_0, ar_1, ar_2, ar_3) -> Com_1(add_Load_599(ar_1, ar_2 + ar_0, ar_0 + 2, ar_3)) [ 0 <= ar_2 /\ 0 <= i126' /\ ar_0 <= 1000 /\ 0 < ar_3 /\ 0 < ar_1 /\ 0 <= i135' /\ ar_2 + ar_0 = i126' /\ 2 <= i135' /\ i135' <= 1002 /\ 0 <= ar_0 /\ ar_0 + 2 = i135' ]
add_GT_299(ar_0, ar_1, ar_2, ar_3) -> Com_1(add_Load_283(ar_1, ar_2 + ar_0, ar_0 + 1, ar_3)) [ ar_0 <= 1000 /\ ar_0 + 1 = i21' /\ i21' <= 1001 /\ 0 <= i20' /\ 0 < ar_3 /\ 0 < ar_1 /\ 0 <= i21' /\ 0 <= ar_0 /\ 1 <= i21' /\ ar_2 + ar_0 = i20' /\ 0 <= ar_2 ]
strictly and produces the following problem:
5: T:
(Comp: 3003, Cost: 16) add_GT_602(ar_0, ar_1, ar_2, ar_3) -> Com_1(add_Load_599(ar_1, ar_2 + ar_0, ar_0 + 2, ar_3)) [ 0 <= ar_2 /\ 0 <= i126' /\ ar_0 <= 1000 /\ 0 < ar_3 /\ 0 < ar_1 /\ 0 <= i135' /\ ar_2 + ar_0 = i126' /\ 2 <= i135' /\ i135' <= 1002 /\ 0 <= ar_0 /\ ar_0 + 2 = i135' ]
(Comp: ?, Cost: 2) add_Load_599(ar_0, ar_1, ar_2, ar_3) -> Com_1(add_GT_602(ar_2, ar_0, ar_1, ar_3)) [ 0 < ar_3 /\ 0 <= ar_1 /\ 0 < ar_0 /\ 0 <= ar_2 ]
(Comp: ?, Cost: 2) add_Load_283(ar_0, ar_1, ar_2, ar_3) -> Com_1(add_GT_299(ar_2, ar_0, ar_1, ar_3)) [ 0 < ar_3 /\ 0 <= ar_2 /\ 0 <= ar_1 /\ 0 < ar_0 ]
(Comp: 1001, Cost: 18) add_Load_954(ar_0, ar_1, ar_2, ar_3) -> Com_1(add_Load_954(ar_0, ar_1 + ar_2, ar_2 + 3, arityPad)) [ ar_2 <= 1000 /\ 0 < ar_0 /\ 0 <= ar_1 /\ 0 <= i334' /\ 0 <= ar_2 /\ 3 <= i351' /\ i351' <= 1003 /\ 0 <= i351' /\ ar_1 + ar_2 = i334' /\ ar_2 + 3 = i351' ]
(Comp: 1, Cost: 39) main_ConstantStackPush_2(ar_0, ar_1, ar_2, ar_3) -> Com_1(add_Load_283(1, 0, 0, 1)) [ 0 <= static'1 /\ 0 <= ar_0 /\ static''' <= ar_0 + 2 /\ 0 <= static''' /\ static'1 <= static''' + 1 ]
(Comp: 2, Cost: 25) add_GT_602(ar_0, ar_1, ar_2, ar_3) -> Com_1(add_Load_954(1, 0, 0, arityPad)) [ 0 <= ar_0 /\ 1000 < ar_0 /\ 0 <= ar_2 /\ 0 < ar_1 /\ 1001 <= ar_0 /\ 0 < ar_3 ]
(Comp: 2, Cost: 22) add_GT_299(ar_0, ar_1, ar_2, ar_3) -> Com_1(add_Load_599(1, 0, 0, ar_3)) [ 1001 <= ar_0 /\ 0 < ar_1 /\ 0 <= ar_2 /\ 0 < ar_3 /\ 0 <= ar_0 /\ 1000 < ar_0 ]
(Comp: 3003, Cost: 16) add_GT_299(ar_0, ar_1, ar_2, ar_3) -> Com_1(add_Load_283(ar_1, ar_2 + ar_0, ar_0 + 1, ar_3)) [ ar_0 <= 1000 /\ ar_0 + 1 = i21' /\ i21' <= 1001 /\ 0 <= i20' /\ 0 < ar_3 /\ 0 < ar_1 /\ 0 <= i21' /\ 0 <= ar_0 /\ 1 <= i21' /\ ar_2 + ar_0 = i20' /\ 0 <= ar_2 ]
(Comp: 1, Cost: 0) koat_start(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_ConstantStackPush_2(ar_0, ar_1, ar_2, ar_3)) [ 0 <= 0 ]
start location: koat_start
leaf cost: 0

Repeatedly propagating knowledge in problem 5 produces the following problem:
6: T:
(Comp: 3003, Cost: 16) add_GT_602(ar_0, ar_1, ar_2, ar_3) -> Com_1(add_Load_599(ar_1, ar_2 + ar_0, ar_0 + 2, ar_3)) [ 0 <= ar_2 /\ 0 <= i126' /\ ar_0 <= 1000 /\ 0 < ar_3 /\ 0 < ar_1 /\ 0 <= i135' /\ ar_2 + ar_0 = i126' /\ 2 <= i135' /\ i135' <= 1002 /\ 0 <= ar_0 /\ ar_0 + 2 = i135' ]
(Comp: 3005, Cost: 2) add_Load_599(ar_0, ar_1, ar_2, ar_3) -> Com_1(add_GT_602(ar_2, ar_0, ar_1, ar_3)) [ 0 < ar_3 /\ 0 <= ar_1 /\ 0 < ar_0 /\ 0 <= ar_2 ]
(Comp: 3004, Cost: 2) add_Load_283(ar_0, ar_1, ar_2, ar_3) -> Com_1(add_GT_299(ar_2, ar_0, ar_1, ar_3)) [ 0 < ar_3 /\ 0 <= ar_2 /\ 0 <= ar_1 /\ 0 < ar_0 ]
(Comp: 1001, Cost: 18) add_Load_954(ar_0, ar_1, ar_2, ar_3) -> Com_1(add_Load_954(ar_0, ar_1 + ar_2, ar_2 + 3, arityPad)) [ ar_2 <= 1000 /\ 0 < ar_0 /\ 0 <= ar_1 /\ 0 <= i334' /\ 0 <= ar_2 /\ 3 <= i351' /\ i351' <= 1003 /\ 0 <= i351' /\ ar_1 + ar_2 = i334' /\ ar_2 + 3 = i351' ]
(Comp: 1, Cost: 39) main_ConstantStackPush_2(ar_0, ar_1, ar_2, ar_3) -> Com_1(add_Load_283(1, 0, 0, 1)) [ 0 <= static'1 /\ 0 <= ar_0 /\ static''' <= ar_0 + 2 /\ 0 <= static''' /\ static'1 <= static''' + 1 ]
(Comp: 2, Cost: 25) add_GT_602(ar_0, ar_1, ar_2, ar_3) -> Com_1(add_Load_954(1, 0, 0, arityPad)) [ 0 <= ar_0 /\ 1000 < ar_0 /\ 0 <= ar_2 /\ 0 < ar_1 /\ 1001 <= ar_0 /\ 0 < ar_3 ]
(Comp: 2, Cost: 22) add_GT_299(ar_0, ar_1, ar_2, ar_3) -> Com_1(add_Load_599(1, 0, 0, ar_3)) [ 1001 <= ar_0 /\ 0 < ar_1 /\ 0 <= ar_2 /\ 0 < ar_3 /\ 0 <= ar_0 /\ 1000 < ar_0 ]
(Comp: 3003, Cost: 16) add_GT_299(ar_0, ar_1, ar_2, ar_3) -> Com_1(add_Load_283(ar_1, ar_2 + ar_0, ar_0 + 1, ar_3)) [ ar_0 <= 1000 /\ ar_0 + 1 = i21' /\ i21' <= 1001 /\ 0 <= i20' /\ 0 < ar_3 /\ 0 < ar_1 /\ 0 <= i21' /\ 0 <= ar_0 /\ 1 <= i21' /\ ar_2 + ar_0 = i20' /\ 0 <= ar_2 ]
(Comp: 1, Cost: 0) koat_start(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_ConstantStackPush_2(ar_0, ar_1, ar_2, ar_3)) [ 0 <= 0 ]
start location: koat_start
leaf cost: 0

Complexity upper bound 126265

Time: 0.330 sec (SMT: 0.287 sec)

(0) Obligation:

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

(2) Obligation:

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

(4) Obligation:

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

(6) Obligation:

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

(8) Obligation:

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

(10) Obligation:

(11) 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) TerminationGraphToComplexityProof (BOTH CONCRETE BOUNDS(ID, ADD(5)) transformation)

(26) Obligation:

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

(28) Obligation:

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

(30) Obligation:

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

(32) Obligation:

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

(34) Obligation:

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

(36) Obligation:

(37) koat Proof (EQUIVALENT transformation)

(38) BOUNDS(CONSTANT, 126265)