Termination proof of /tmp/tmp9Wwxg

Termination of the given JBC could be proven:

0 JBC

↳1 JBCToGraph (⇒, 1840 ms)

↳2 JBCTerminationGraph

↳3 TerminationGraphToSCCProof (⇒, 0 ms)

↳4 JBCTerminationSCC

↳5 SCCToIDPv1Proof (⇒, 580 ms)

↳6 IDP

↳7 IDPNonInfProof (⇒, 420 ms)

↳8 AND

    ↳9 IDP

        ↳10 IDependencyGraphProof (⇔, 0 ms)

        ↳11 TRUE

    ↳12 IDP

        ↳13 IDependencyGraphProof (⇔, 0 ms)

        ↳14 TRUE

(0) Obligation:

JBC Problem based on JBC Program:
Manifest-Version: 1.0 Created-By: 1.6.0_20 (Apple Inc.) Main-Class: Test11

public class Test11 {
    public static void main(String[] args) {
	Random.args = args;

	int x = args.length * 100, y = args.length * 200 / 13;

	while (x + y > 0) {
	    if (Random.random() * Random.random() > 9)
		x--;
	    else
		y--;
	}
    }
}

public class Random {
  static String[] args;
  static int index = 0;

  public static int random() {
      if (index >= args.length)
	  return 0;

      String string = args[index];
      index++;
      return string.length();
  }
}

(1) JBCToGraph (SOUND transformation)

Constructed TerminationGraph.

(2) Obligation:

Termination Graph based on JBC Program:
Test11.main([Ljava/lang/String;)V: Graph of 360 nodes with 1 SCC.

(3) TerminationGraphToSCCProof (SOUND transformation)

Splitted TerminationGraph to 1 SCCs.

(4) Obligation:

SCC of termination graph based on JBC Program.
SCC contains nodes from the following methods: Test11.main([Ljava/lang/String;)V
SCC calls the following helper methods:
Performed SCC analyses: UsedFieldsAnalysis

(5) SCCToIDPv1Proof (SOUND transformation)

Transformed FIGraph SCCs to IDPs. Log:

Generated 114 rules for P and 0 rules for R.

P rules:
4674_0_main_Load(EOS(STATIC_4674(i2231)), i2232, i825, i2232) → 4675_0_main_IntArithmetic(EOS(STATIC_4675(i2231)), i2232, i825, i2232, i825)
4675_0_main_IntArithmetic(EOS(STATIC_4675(i2231)), i2232, i825, i2232, i825) → 4676_0_main_LE(EOS(STATIC_4676(i2231)), i2232, i825, +(i2232, i825))
4676_0_main_LE(EOS(STATIC_4676(i2231)), i2232, i825, i2379) → 4678_0_main_LE(EOS(STATIC_4678(i2231)), i2232, i825, i2379)
4678_0_main_LE(EOS(STATIC_4678(i2231)), i2232, i825, i2379) → 4681_0_main_InvokeMethod(EOS(STATIC_4681(i2231)), i2232, i825) | >(i2379, 0)
4681_0_main_InvokeMethod(EOS(STATIC_4681(i2231)), i2232, i825) → 4683_0_random_FieldAccess(EOS(STATIC_4683(i2231)), i2232, i825)
4683_0_random_FieldAccess(EOS(STATIC_4683(i2231)), i2232, i825) → 4684_0_random_FieldAccess(EOS(STATIC_4684(i2231)), i2232, i825, i2231)
4684_0_random_FieldAccess(EOS(STATIC_4684(i2231)), i2232, i825, i2231) → 4686_0_random_ArrayLength(EOS(STATIC_4686(i2231)), i2232, i825, i2231, java.lang.Object(ARRAY(i303)))
4686_0_random_ArrayLength(EOS(STATIC_4686(i2231)), i2232, i825, i2231, java.lang.Object(ARRAY(i303))) → 4687_0_random_LT(EOS(STATIC_4687(i2231)), i2232, i825, i2231, i303) | >=(i303, 0)
4687_0_random_LT(EOS(STATIC_4687(i2231)), i2232, i825, i2231, i303) → 4688_0_random_LT(EOS(STATIC_4688(i2231)), i2232, i825, i2231, i303)
4687_0_random_LT(EOS(STATIC_4687(i2231)), i2232, i825, i2231, i303) → 4689_0_random_LT(EOS(STATIC_4689(i2231)), i2232, i825, i2231, i303)
4688_0_random_LT(EOS(STATIC_4688(i2231)), i2232, i825, i2231, i303) → 4690_0_random_FieldAccess(EOS(STATIC_4690(i2231)), i2232, i825) | <(i2231, i303)
4690_0_random_FieldAccess(EOS(STATIC_4690(i2231)), i2232, i825) → 4693_0_random_FieldAccess(EOS(STATIC_4693(i2231)), i2232, i825, java.lang.Object(ARRAY(i303)))
4693_0_random_FieldAccess(EOS(STATIC_4693(i2231)), i2232, i825, java.lang.Object(ARRAY(i303))) → 4695_0_random_ArrayAccess(EOS(STATIC_4695(i2231)), i2232, i825, java.lang.Object(ARRAY(i303)), i2231)
4695_0_random_ArrayAccess(EOS(STATIC_4695(i2383)), i2232, i825, java.lang.Object(ARRAY(i303)), i2383) → 4699_0_random_ArrayAccess(EOS(STATIC_4699(i2383)), i2232, i825, java.lang.Object(ARRAY(i303)), i2383)
4699_0_random_ArrayAccess(EOS(STATIC_4699(i2383)), i2232, i825, java.lang.Object(ARRAY(i303)), i2383) → 4703_0_random_ArrayAccess(EOS(STATIC_4703(i2383)), i2232, i825, java.lang.Object(ARRAY(i303)), i2383)
4703_0_random_ArrayAccess(EOS(STATIC_4703(i2383)), i2232, i825, java.lang.Object(ARRAY(i303)), i2383) → 4705_0_random_Store(EOS(STATIC_4705(i2383)), i2232, i825, o3209)
4705_0_random_Store(EOS(STATIC_4705(i2383)), i2232, i825, o3209) → 4711_0_random_FieldAccess(EOS(STATIC_4711(i2383)), i2232, i825, o3209)
4711_0_random_FieldAccess(EOS(STATIC_4711(i2383)), i2232, i825, o3209) → 4715_0_random_ConstantStackPush(EOS(STATIC_4715(i2383)), i2232, i825, o3209, i2383)
4715_0_random_ConstantStackPush(EOS(STATIC_4715(i2383)), i2232, i825, o3209, i2383) → 4719_0_random_IntArithmetic(EOS(STATIC_4719(i2383)), i2232, i825, o3209, i2383, 1)
4719_0_random_IntArithmetic(EOS(STATIC_4719(i2383)), i2232, i825, o3209, i2383, matching1) → 4725_0_random_FieldAccess(EOS(STATIC_4725(i2383)), i2232, i825, o3209, +(i2383, 1)) | &&(>=(i2383, 0), =(matching1, 1))
4725_0_random_FieldAccess(EOS(STATIC_4725(i2383)), i2232, i825, o3209, i2384) → 4730_0_random_Load(EOS(STATIC_4730(i2384)), i2232, i825, o3209)
4730_0_random_Load(EOS(STATIC_4730(i2384)), i2232, i825, o3209) → 4735_0_random_InvokeMethod(EOS(STATIC_4735(i2384)), i2232, i825, o3209)
4735_0_random_InvokeMethod(EOS(STATIC_4735(i2384)), i2232, i825, java.lang.Object(o3224sub)) → 4741_0_random_InvokeMethod(EOS(STATIC_4741(i2384)), i2232, i825, java.lang.Object(o3224sub))
4741_0_random_InvokeMethod(EOS(STATIC_4741(i2384)), i2232, i825, java.lang.Object(o3224sub)) → 4749_0_length_Load(EOS(STATIC_4749(i2384)), i2232, i825, java.lang.Object(o3224sub), java.lang.Object(o3224sub))
4749_0_length_Load(EOS(STATIC_4749(i2384)), i2232, i825, java.lang.Object(o3224sub), java.lang.Object(o3224sub)) → 4765_0_length_FieldAccess(EOS(STATIC_4765(i2384)), i2232, i825, java.lang.Object(o3224sub), java.lang.Object(o3224sub))
4765_0_length_FieldAccess(EOS(STATIC_4765(i2384)), i2232, i825, java.lang.Object(java.lang.String(o3239sub, i2403)), java.lang.Object(java.lang.String(o3239sub, i2403))) → 4773_0_length_FieldAccess(EOS(STATIC_4773(i2384)), i2232, i825, java.lang.Object(java.lang.String(o3239sub, i2403)), java.lang.Object(java.lang.String(o3239sub, i2403))) | &&(>=(i2403, 0), >=(i2404, 0))
4773_0_length_FieldAccess(EOS(STATIC_4773(i2384)), i2232, i825, java.lang.Object(java.lang.String(o3239sub, i2403)), java.lang.Object(java.lang.String(o3239sub, i2403))) → 4782_0_length_Return(EOS(STATIC_4782(i2384)), i2232, i825, java.lang.Object(java.lang.String(o3239sub, i2403)), i2403)
4782_0_length_Return(EOS(STATIC_4782(i2384)), i2232, i825, java.lang.Object(java.lang.String(o3239sub, i2403)), i2403) → 4836_0_random_Return(EOS(STATIC_4836(i2384)), i2232, i825, i2403)
4836_0_random_Return(EOS(STATIC_4836(i2384)), i2232, i825, i2403) → 4842_0_main_InvokeMethod(EOS(STATIC_4842(i2384)), i2232, i825, i2403)
4842_0_main_InvokeMethod(EOS(STATIC_4842(i2384)), i2232, i825, i2403) → 4851_0_random_FieldAccess(EOS(STATIC_4851(i2384)), i2232, i825, i2403)
4851_0_random_FieldAccess(EOS(STATIC_4851(i2384)), i2232, i825, i2403) → 4867_0_random_FieldAccess(EOS(STATIC_4867(i2384)), i2232, i825, i2403, i2384)
4867_0_random_FieldAccess(EOS(STATIC_4867(i2384)), i2232, i825, i2403, i2384) → 4878_0_random_ArrayLength(EOS(STATIC_4878(i2384)), i2232, i825, i2403, i2384, java.lang.Object(ARRAY(i303)))
4878_0_random_ArrayLength(EOS(STATIC_4878(i2384)), i2232, i825, i2403, i2384, java.lang.Object(ARRAY(i303))) → 4887_0_random_LT(EOS(STATIC_4887(i2384)), i2232, i825, i2403, i2384, i303) | >=(i303, 0)
4887_0_random_LT(EOS(STATIC_4887(i2384)), i2232, i825, i2403, i2384, i303) → 4895_0_random_LT(EOS(STATIC_4895(i2384)), i2232, i825, i2403, i2384, i303)
4887_0_random_LT(EOS(STATIC_4887(i2384)), i2232, i825, i2403, i2384, i303) → 4896_0_random_LT(EOS(STATIC_4896(i2384)), i2232, i825, i2403, i2384, i303)
4895_0_random_LT(EOS(STATIC_4895(i2384)), i2232, i825, i2403, i2384, i303) → 4907_0_random_FieldAccess(EOS(STATIC_4907(i2384)), i2232, i825, i2403) | <(i2384, i303)
4907_0_random_FieldAccess(EOS(STATIC_4907(i2384)), i2232, i825, i2403) → 4917_0_random_FieldAccess(EOS(STATIC_4917(i2384)), i2232, i825, i2403, java.lang.Object(ARRAY(i303)))
4917_0_random_FieldAccess(EOS(STATIC_4917(i2384)), i2232, i825, i2403, java.lang.Object(ARRAY(i303))) → 4928_0_random_ArrayAccess(EOS(STATIC_4928(i2384)), i2232, i825, i2403, java.lang.Object(ARRAY(i303)), i2384)
4928_0_random_ArrayAccess(EOS(STATIC_4928(i2384)), i2232, i825, i2403, java.lang.Object(ARRAY(i303)), i2384) → 4941_0_random_ArrayAccess(EOS(STATIC_4941(i2384)), i2232, i825, i2403, java.lang.Object(ARRAY(i303)), i2384)
4941_0_random_ArrayAccess(EOS(STATIC_4941(i2384)), i2232, i825, i2403, java.lang.Object(ARRAY(i303)), i2384) → 4956_0_random_Store(EOS(STATIC_4956(i2384)), i2232, i825, i2403, o3459)
4956_0_random_Store(EOS(STATIC_4956(i2384)), i2232, i825, i2403, o3459) → 4968_0_random_FieldAccess(EOS(STATIC_4968(i2384)), i2232, i825, i2403, o3459)
4968_0_random_FieldAccess(EOS(STATIC_4968(i2384)), i2232, i825, i2403, o3459) → 4980_0_random_ConstantStackPush(EOS(STATIC_4980(i2384)), i2232, i825, i2403, o3459, i2384)
4980_0_random_ConstantStackPush(EOS(STATIC_4980(i2384)), i2232, i825, i2403, o3459, i2384) → 4992_0_random_IntArithmetic(EOS(STATIC_4992(i2384)), i2232, i825, i2403, o3459, i2384, 1)
4992_0_random_IntArithmetic(EOS(STATIC_4992(i2384)), i2232, i825, i2403, o3459, i2384, matching1) → 5003_0_random_FieldAccess(EOS(STATIC_5003(i2384)), i2232, i825, i2403, o3459, +(i2384, 1)) | &&(>(i2384, 0), =(matching1, 1))
5003_0_random_FieldAccess(EOS(STATIC_5003(i2384)), i2232, i825, i2403, o3459, i2646) → 5065_0_random_Load(EOS(STATIC_5065(i2646)), i2232, i825, i2403, o3459)
5065_0_random_Load(EOS(STATIC_5065(i2646)), i2232, i825, i2403, o3459) → 5074_0_random_InvokeMethod(EOS(STATIC_5074(i2646)), i2232, i825, i2403, o3459)
5074_0_random_InvokeMethod(EOS(STATIC_5074(i2646)), i2232, i825, i2403, java.lang.Object(o3643sub)) → 5083_0_random_InvokeMethod(EOS(STATIC_5083(i2646)), i2232, i825, i2403, java.lang.Object(o3643sub))
5083_0_random_InvokeMethod(EOS(STATIC_5083(i2646)), i2232, i825, i2403, java.lang.Object(o3643sub)) → 5092_0_length_Load(EOS(STATIC_5092(i2646)), i2232, i825, i2403, java.lang.Object(o3643sub), java.lang.Object(o3643sub))
5092_0_length_Load(EOS(STATIC_5092(i2646)), i2232, i825, i2403, java.lang.Object(o3643sub), java.lang.Object(o3643sub)) → 5111_0_length_FieldAccess(EOS(STATIC_5111(i2646)), i2232, i825, i2403, java.lang.Object(o3643sub), java.lang.Object(o3643sub))
5111_0_length_FieldAccess(EOS(STATIC_5111(i2646)), i2232, i825, i2403, java.lang.Object(java.lang.String(o3732sub, i2703)), java.lang.Object(java.lang.String(o3732sub, i2703))) → 5119_0_length_FieldAccess(EOS(STATIC_5119(i2646)), i2232, i825, i2403, java.lang.Object(java.lang.String(o3732sub, i2703)), java.lang.Object(java.lang.String(o3732sub, i2703))) | &&(>=(i2703, 0), >=(i2704, 0))
5119_0_length_FieldAccess(EOS(STATIC_5119(i2646)), i2232, i825, i2403, java.lang.Object(java.lang.String(o3732sub, i2703)), java.lang.Object(java.lang.String(o3732sub, i2703))) → 5127_0_length_Return(EOS(STATIC_5127(i2646)), i2232, i825, i2403, java.lang.Object(java.lang.String(o3732sub, i2703)), i2703)
5127_0_length_Return(EOS(STATIC_5127(i2646)), i2232, i825, i2403, java.lang.Object(java.lang.String(o3732sub, i2703)), i2703) → 5134_0_random_Return(EOS(STATIC_5134(i2646)), i2232, i825, i2403, i2703)
5134_0_random_Return(EOS(STATIC_5134(i2646)), i2232, i825, i2403, i2703) → 5137_0_main_IntArithmetic(EOS(STATIC_5137(i2646)), i2232, i825, i2403, i2703)
5137_0_main_IntArithmetic(EOS(STATIC_5137(i2646)), i2232, i825, i2403, i2703) → 5143_0_main_ConstantStackPush(EOS(STATIC_5143(i2646)), i2232, i825, *(i2403, i2703))
5143_0_main_ConstantStackPush(EOS(STATIC_5143(i2646)), i2232, i825, i2713) → 5150_0_main_LE(EOS(STATIC_5150(i2646)), i2232, i825, i2713, 9)
5150_0_main_LE(EOS(STATIC_5150(i2646)), i2232, i825, i2726, matching1) → 5155_0_main_LE(EOS(STATIC_5155(i2646)), i2232, i825, i2726, 9) | =(matching1, 9)
5150_0_main_LE(EOS(STATIC_5150(i2646)), i2232, i825, i2727, matching1) → 5156_0_main_LE(EOS(STATIC_5156(i2646)), i2232, i825, i2727, 9) | =(matching1, 9)
5155_0_main_LE(EOS(STATIC_5155(i2646)), i2232, i825, i2726, matching1) → 5162_0_main_Inc(EOS(STATIC_5162(i2646)), i2232, i825) | &&(<=(i2726, 9), =(matching1, 9))
5162_0_main_Inc(EOS(STATIC_5162(i2646)), i2232, i825) → 5168_0_main_JMP(EOS(STATIC_5168(i2646)), i2232, +(i825, -1))
5168_0_main_JMP(EOS(STATIC_5168(i2646)), i2232, i2730) → 5173_0_main_Load(EOS(STATIC_5173(i2646)), i2232, i2730)
5173_0_main_Load(EOS(STATIC_5173(i2646)), i2232, i2730) → 4649_0_main_Load(EOS(STATIC_4649(i2646)), i2232, i2730)
4649_0_main_Load(EOS(STATIC_4649(i2231)), i2232, i825) → 4674_0_main_Load(EOS(STATIC_4674(i2231)), i2232, i825, i2232)
5156_0_main_LE(EOS(STATIC_5156(i2646)), i2232, i825, i2727, matching1) → 5163_0_main_Inc(EOS(STATIC_5163(i2646)), i2232, i825) | &&(>(i2727, 9), =(matching1, 9))
5163_0_main_Inc(EOS(STATIC_5163(i2646)), i2232, i825) → 5169_0_main_JMP(EOS(STATIC_5169(i2646)), +(i2232, -1), i825)
5169_0_main_JMP(EOS(STATIC_5169(i2646)), i2731, i825) → 5174_0_main_Load(EOS(STATIC_5174(i2646)), i2731, i825)
5174_0_main_Load(EOS(STATIC_5174(i2646)), i2731, i825) → 4649_0_main_Load(EOS(STATIC_4649(i2646)), i2731, i825)
4896_0_random_LT(EOS(STATIC_4896(i2384)), i2232, i825, i2403, i2384, i303) → 4908_0_random_ConstantStackPush(EOS(STATIC_4908(i2384)), i2232, i825, i2403) | >=(i2384, i303)
4908_0_random_ConstantStackPush(EOS(STATIC_4908(i2384)), i2232, i825, i2403) → 4919_0_random_Return(EOS(STATIC_4919(i2384)), i2232, i825, i2403)
4919_0_random_Return(EOS(STATIC_4919(i2384)), i2232, i825, i2403) → 4929_0_main_IntArithmetic(EOS(STATIC_4929(i2384)), i2232, i825, i2403)
4929_0_main_IntArithmetic(EOS(STATIC_4929(i2384)), i2232, i825, i2403) → 4943_0_main_ConstantStackPush(EOS(STATIC_4943(i2384)), i2232, i825)
4943_0_main_ConstantStackPush(EOS(STATIC_4943(i2384)), i2232, i825) → 4950_0_main_ConstantStackPush(EOS(STATIC_4950(i2384)), i2232, i825)
4950_0_main_ConstantStackPush(EOS(STATIC_4950(i2564)), i2232, i825) → 4963_0_main_LE(EOS(STATIC_4963(i2564)), i2232, i825)
4963_0_main_LE(EOS(STATIC_4963(i2564)), i2232, i825) → 4975_0_main_Inc(EOS(STATIC_4975(i2564)), i2232, i825)
4975_0_main_Inc(EOS(STATIC_4975(i2564)), i2232, i825) → 4988_0_main_JMP(EOS(STATIC_4988(i2564)), i2232, +(i825, -1))
4988_0_main_JMP(EOS(STATIC_4988(i2564)), i2232, i2637) → 4999_0_main_Load(EOS(STATIC_4999(i2564)), i2232, i2637)
4999_0_main_Load(EOS(STATIC_4999(i2564)), i2232, i2637) → 4649_0_main_Load(EOS(STATIC_4649(i2564)), i2232, i2637)
4689_0_random_LT(EOS(STATIC_4689(i2231)), i2232, i825, i2231, i303) → 4692_0_random_ConstantStackPush(EOS(STATIC_4692(i2231)), i2232, i825) | >=(i2231, i303)
4692_0_random_ConstantStackPush(EOS(STATIC_4692(i2231)), i2232, i825) → 4694_0_random_Return(EOS(STATIC_4694(i2231)), i2232, i825)
4694_0_random_Return(EOS(STATIC_4694(i2231)), i2232, i825) → 4697_0_main_InvokeMethod(EOS(STATIC_4697(i2231)), i2232, i825)
4697_0_main_InvokeMethod(EOS(STATIC_4697(i2231)), i2232, i825) → 4700_0_random_FieldAccess(EOS(STATIC_4700(i2231)), i2232, i825)
4700_0_random_FieldAccess(EOS(STATIC_4700(i2231)), i2232, i825) → 4708_0_random_FieldAccess(EOS(STATIC_4708(i2231)), i2232, i825, i2231)
4708_0_random_FieldAccess(EOS(STATIC_4708(i2231)), i2232, i825, i2231) → 4712_0_random_ArrayLength(EOS(STATIC_4712(i2231)), i2232, i825, i2231, java.lang.Object(ARRAY(i303)))
4712_0_random_ArrayLength(EOS(STATIC_4712(i2231)), i2232, i825, i2231, java.lang.Object(ARRAY(i303))) → 4718_0_random_LT(EOS(STATIC_4718(i2231)), i2232, i825, i2231, i303) | >=(i303, 0)
4718_0_random_LT(EOS(STATIC_4718(i2231)), i2232, i825, i2231, i303) → 4721_0_random_LT(EOS(STATIC_4721(i2231)), i2232, i825, i2231, i303)
4718_0_random_LT(EOS(STATIC_4718(i2231)), i2232, i825, i2231, i303) → 4722_0_random_LT(EOS(STATIC_4722(i2231)), i2232, i825, i2231, i303)
4721_0_random_LT(EOS(STATIC_4721(i2231)), i2232, i825, i2231, i303) → 4726_0_random_FieldAccess(EOS(STATIC_4726(i2231)), i2232, i825) | <(i2231, i303)
4726_0_random_FieldAccess(EOS(STATIC_4726(i2231)), i2232, i825) → 4732_0_random_FieldAccess(EOS(STATIC_4732(i2231)), i2232, i825, java.lang.Object(ARRAY(i303)))
4732_0_random_FieldAccess(EOS(STATIC_4732(i2231)), i2232, i825, java.lang.Object(ARRAY(i303))) → 4738_0_random_ArrayAccess(EOS(STATIC_4738(i2231)), i2232, i825, java.lang.Object(ARRAY(i303)), i2231)
4738_0_random_ArrayAccess(EOS(STATIC_4738(i2390)), i2232, i825, java.lang.Object(ARRAY(i303)), i2390) → 4745_0_random_ArrayAccess(EOS(STATIC_4745(i2390)), i2232, i825, java.lang.Object(ARRAY(i303)), i2390)
4745_0_random_ArrayAccess(EOS(STATIC_4745(i2390)), i2232, i825, java.lang.Object(ARRAY(i303)), i2390) → 4754_0_random_ArrayAccess(EOS(STATIC_4754(i2390)), i2232, i825, java.lang.Object(ARRAY(i303)), i2390)
4754_0_random_ArrayAccess(EOS(STATIC_4754(i2390)), i2232, i825, java.lang.Object(ARRAY(i303)), i2390) → 4760_0_random_Store(EOS(STATIC_4760(i2390)), i2232, i825, o3229)
4760_0_random_Store(EOS(STATIC_4760(i2390)), i2232, i825, o3229) → 4769_0_random_FieldAccess(EOS(STATIC_4769(i2390)), i2232, i825, o3229)
4769_0_random_FieldAccess(EOS(STATIC_4769(i2390)), i2232, i825, o3229) → 4778_0_random_ConstantStackPush(EOS(STATIC_4778(i2390)), i2232, i825, o3229, i2390)
4778_0_random_ConstantStackPush(EOS(STATIC_4778(i2390)), i2232, i825, o3229, i2390) → 4786_0_random_IntArithmetic(EOS(STATIC_4786(i2390)), i2232, i825, o3229, i2390, 1)
4786_0_random_IntArithmetic(EOS(STATIC_4786(i2390)), i2232, i825, o3229, i2390, matching1) → 4840_0_random_FieldAccess(EOS(STATIC_4840(i2390)), i2232, i825, o3229, +(i2390, 1)) | &&(>=(i2390, 0), =(matching1, 1))
4840_0_random_FieldAccess(EOS(STATIC_4840(i2390)), i2232, i825, o3229, i2564) → 4847_0_random_Load(EOS(STATIC_4847(i2564)), i2232, i825, o3229)
4847_0_random_Load(EOS(STATIC_4847(i2564)), i2232, i825, o3229) → 4856_0_random_InvokeMethod(EOS(STATIC_4856(i2564)), i2232, i825, o3229)
4856_0_random_InvokeMethod(EOS(STATIC_4856(i2564)), i2232, i825, java.lang.Object(o3354sub)) → 4863_0_random_InvokeMethod(EOS(STATIC_4863(i2564)), i2232, i825, java.lang.Object(o3354sub))
4863_0_random_InvokeMethod(EOS(STATIC_4863(i2564)), i2232, i825, java.lang.Object(o3354sub)) → 4872_0_length_Load(EOS(STATIC_4872(i2564)), i2232, i825, java.lang.Object(o3354sub), java.lang.Object(o3354sub))
4872_0_length_Load(EOS(STATIC_4872(i2564)), i2232, i825, java.lang.Object(o3354sub), java.lang.Object(o3354sub)) → 4892_0_length_FieldAccess(EOS(STATIC_4892(i2564)), i2232, i825, java.lang.Object(o3354sub), java.lang.Object(o3354sub))
4892_0_length_FieldAccess(EOS(STATIC_4892(i2564)), i2232, i825, java.lang.Object(java.lang.String(o3387sub, i2592)), java.lang.Object(java.lang.String(o3387sub, i2592))) → 4901_0_length_FieldAccess(EOS(STATIC_4901(i2564)), i2232, i825, java.lang.Object(java.lang.String(o3387sub, i2592)), java.lang.Object(java.lang.String(o3387sub, i2592))) | &&(>=(i2592, 0), >=(i2593, 0))
4901_0_length_FieldAccess(EOS(STATIC_4901(i2564)), i2232, i825, java.lang.Object(java.lang.String(o3387sub, i2592)), java.lang.Object(java.lang.String(o3387sub, i2592))) → 4912_0_length_Return(EOS(STATIC_4912(i2564)), i2232, i825, java.lang.Object(java.lang.String(o3387sub, i2592)))
4912_0_length_Return(EOS(STATIC_4912(i2564)), i2232, i825, java.lang.Object(java.lang.String(o3387sub, i2592))) → 4925_0_random_Return(EOS(STATIC_4925(i2564)), i2232, i825)
4925_0_random_Return(EOS(STATIC_4925(i2564)), i2232, i825) → 4935_0_main_IntArithmetic(EOS(STATIC_4935(i2564)), i2232, i825)
4935_0_main_IntArithmetic(EOS(STATIC_4935(i2564)), i2232, i825) → 4950_0_main_ConstantStackPush(EOS(STATIC_4950(i2564)), i2232, i825)
4722_0_random_LT(EOS(STATIC_4722(i2231)), i2232, i825, i2231, i303) → 4728_0_random_ConstantStackPush(EOS(STATIC_4728(i2231)), i2232, i825) | >=(i2231, i303)
4728_0_random_ConstantStackPush(EOS(STATIC_4728(i2231)), i2232, i825) → 4734_0_random_Return(EOS(STATIC_4734(i2231)), i2232, i825)
4734_0_random_Return(EOS(STATIC_4734(i2231)), i2232, i825) → 4739_0_main_IntArithmetic(EOS(STATIC_4739(i2231)), i2232, i825)
4739_0_main_IntArithmetic(EOS(STATIC_4739(i2231)), i2232, i825) → 4746_0_main_ConstantStackPush(EOS(STATIC_4746(i2231)), i2232, i825)
4746_0_main_ConstantStackPush(EOS(STATIC_4746(i2231)), i2232, i825) → 4756_0_main_LE(EOS(STATIC_4756(i2231)), i2232, i825)
4756_0_main_LE(EOS(STATIC_4756(i2231)), i2232, i825) → 4763_0_main_Inc(EOS(STATIC_4763(i2231)), i2232, i825)
4763_0_main_Inc(EOS(STATIC_4763(i2231)), i2232, i825) → 4770_0_main_JMP(EOS(STATIC_4770(i2231)), i2232, +(i825, -1))
4770_0_main_JMP(EOS(STATIC_4770(i2231)), i2232, i2399) → 4781_0_main_Load(EOS(STATIC_4781(i2231)), i2232, i2399)
4781_0_main_Load(EOS(STATIC_4781(i2231)), i2232, i2399) → 4649_0_main_Load(EOS(STATIC_4649(i2231)), i2232, i2399)
R rules:

Combined rules. Obtained 4 conditional rules for P and 0 conditional rules for R.

P rules:
4674_0_main_Load(EOS(STATIC_4674(x0)), x1, x2, x1) → 4674_0_main_Load(EOS(STATIC_4674(+(x0, 2))), x1, +(x2, -1), x1) | &&(>(+(x0, 1), 0), <(0, +(x1, x2)))
4674_0_main_Load(EOS(STATIC_4674(x0)), x1, x2, x1) → 4674_0_main_Load(EOS(STATIC_4674(+(x0, 2))), +(x1, -1), x2, +(x1, -1)) | &&(>(+(x0, 1), 0), <(0, +(x1, x2)))
4674_0_main_Load(EOS(STATIC_4674(x0)), x1, x2, x1) → 4674_0_main_Load(EOS(STATIC_4674(+(x0, 1))), x1, +(x2, -1), x1) | &&(>(+(x0, 1), 0), <(0, +(x1, x2)))
4674_0_main_Load(EOS(STATIC_4674(x0)), x1, x2, x1) → 4674_0_main_Load(EOS(STATIC_4674(x0)), x1, +(x2, -1), x1) | <(0, +(x1, x2))
R rules:

Filtered duplicate args:

4674_0_main_Load(x1, x2, x3, x4) → 4674_0_main_Load(x1, x3, x4)
Cond_4674_0_main_Load(x1, x2, x3, x4, x5) → Cond_4674_0_main_Load(x1, x2, x4, x5)
Cond_4674_0_main_Load1(x1, x2, x3, x4, x5) → Cond_4674_0_main_Load1(x1, x2, x4, x5)
Cond_4674_0_main_Load2(x1, x2, x3, x4, x5) → Cond_4674_0_main_Load2(x1, x2, x4, x5)
Cond_4674_0_main_Load3(x1, x2, x3, x4, x5) → Cond_4674_0_main_Load3(x1, x2, x4, x5)

Combined rules. Obtained 4 conditional rules for P and 0 conditional rules for R.

P rules:
4674_0_main_Load(EOS(STATIC_4674(x0)), x2, x1) → 4674_0_main_Load(EOS(STATIC_4674(+(x0, 2))), +(x2, -1), x1) | &&(>(x0, -1), <(0, +(x1, x2)))
4674_0_main_Load(EOS(STATIC_4674(x0)), x2, x1) → 4674_0_main_Load(EOS(STATIC_4674(+(x0, 2))), x2, +(x1, -1)) | &&(>(x0, -1), <(0, +(x1, x2)))
4674_0_main_Load(EOS(STATIC_4674(x0)), x2, x1) → 4674_0_main_Load(EOS(STATIC_4674(+(x0, 1))), +(x2, -1), x1) | &&(>(x0, -1), <(0, +(x1, x2)))
4674_0_main_Load(EOS(STATIC_4674(x0)), x2, x1) → 4674_0_main_Load(EOS(STATIC_4674(x0)), +(x2, -1), x1) | <(0, +(x1, x2))
R rules:

Performed bisimulation on rules. Used the following equivalence classes: {[Cond_4674_0_main_Load_4, Cond_4674_0_main_Load1_4, Cond_4674_0_main_Load2_4]=Cond_4674_0_main_Load_4}

Finished conversion. Obtained 6 rules for P and 0 rules for R. System has predefined symbols.

P rules:
4674_0_MAIN_LOAD(EOS(STATIC_4674(x0)), x2, x1) → COND_4674_0_MAIN_LOAD(&&(>(x0, -1), <(0, +(x1, x2))), EOS(STATIC_4674(x0)), x2, x1)
COND_4674_0_MAIN_LOAD(TRUE, EOS(STATIC_4674(x0)), x2, x1) → 4674_0_MAIN_LOAD(EOS(STATIC_4674(+(x0, 2))), +(x2, -1), x1)
COND_4674_0_MAIN_LOAD(TRUE, EOS(STATIC_4674(x0)), x2, x1) → 4674_0_MAIN_LOAD(EOS(STATIC_4674(+(x0, 2))), x2, +(x1, -1))
COND_4674_0_MAIN_LOAD(TRUE, EOS(STATIC_4674(x0)), x2, x1) → 4674_0_MAIN_LOAD(EOS(STATIC_4674(+(x0, 1))), +(x2, -1), x1)
4674_0_MAIN_LOAD(EOS(STATIC_4674(x0)), x2, x1) → COND_4674_0_MAIN_LOAD3(<(0, +(x1, x2)), EOS(STATIC_4674(x0)), x2, x1)
COND_4674_0_MAIN_LOAD3(TRUE, EOS(STATIC_4674(x0)), x2, x1) → 4674_0_MAIN_LOAD(EOS(STATIC_4674(x0)), +(x2, -1), x1)
R rules:

(6) Obligation:

IDP problem:
The following function symbols are pre-defined:

!=	~	Neq: (Integer, Integer) -> Boolean
*	~	Mul: (Integer, Integer) -> Integer
>=	~	Ge: (Integer, Integer) -> Boolean
-1	~	UnaryMinus: (Integer) -> Integer
\|	~	Bwor: (Integer, Integer) -> Integer
/	~	Div: (Integer, Integer) -> Integer
=	~	Eq: (Integer, Integer) -> Boolean
	~	Bwxor: (Integer, Integer) -> Integer
\|\|	~	Lor: (Boolean, Boolean) -> Boolean
!	~	Lnot: (Boolean) -> Boolean
<	~	Lt: (Integer, Integer) -> Boolean
-	~	Sub: (Integer, Integer) -> Integer
<=	~	Le: (Integer, Integer) -> Boolean
>	~	Gt: (Integer, Integer) -> Boolean
~	~	Bwnot: (Integer) -> Integer
%	~	Mod: (Integer, Integer) -> Integer
&	~	Bwand: (Integer, Integer) -> Integer
+	~	Add: (Integer, Integer) -> Integer
&&	~	Land: (Boolean, Boolean) -> Boolean

The following domains are used:

Boolean, Integer

R is empty.

The integer pair graph contains the following rules and edges:
(0): 4674_0_MAIN_LOAD(EOS(STATIC_4674(x0[0])), x2[0], x1[0]) → COND_4674_0_MAIN_LOAD(x0[0] > -1 && 0 < x1[0] + x2[0], EOS(STATIC_4674(x0[0])), x2[0], x1[0])
(1): COND_4674_0_MAIN_LOAD(TRUE, EOS(STATIC_4674(x0[1])), x2[1], x1[1]) → 4674_0_MAIN_LOAD(EOS(STATIC_4674(x0[1] + 2)), x2[1] + -1, x1[1])
(2): COND_4674_0_MAIN_LOAD(TRUE, EOS(STATIC_4674(x0[2])), x2[2], x1[2]) → 4674_0_MAIN_LOAD(EOS(STATIC_4674(x0[2] + 2)), x2[2], x1[2] + -1)
(3): COND_4674_0_MAIN_LOAD(TRUE, EOS(STATIC_4674(x0[3])), x2[3], x1[3]) → 4674_0_MAIN_LOAD(EOS(STATIC_4674(x0[3] + 1)), x2[3] + -1, x1[3])
(4): 4674_0_MAIN_LOAD(EOS(STATIC_4674(x0[4])), x2[4], x1[4]) → COND_4674_0_MAIN_LOAD3(0 < x1[4] + x2[4], EOS(STATIC_4674(x0[4])), x2[4], x1[4])
(5): COND_4674_0_MAIN_LOAD3(TRUE, EOS(STATIC_4674(x0[5])), x2[5], x1[5]) → 4674_0_MAIN_LOAD(EOS(STATIC_4674(x0[5])), x2[5] + -1, x1[5])

(0) -> (1), if (x0[0] > -1 && 0 < x1[0] + x2[0] ∧EOS(STATIC_4674(x0[0])) →^* EOS(STATIC_4674(x0[1]))∧x2[0] →^* x2[1]∧x1[0] →^* x1[1])

(0) -> (2), if (x0[0] > -1 && 0 < x1[0] + x2[0] ∧EOS(STATIC_4674(x0[0])) →^* EOS(STATIC_4674(x0[2]))∧x2[0] →^* x2[2]∧x1[0] →^* x1[2])

(0) -> (3), if (x0[0] > -1 && 0 < x1[0] + x2[0] ∧EOS(STATIC_4674(x0[0])) →^* EOS(STATIC_4674(x0[3]))∧x2[0] →^* x2[3]∧x1[0] →^* x1[3])

(1) -> (0), if (EOS(STATIC_4674(x0[1] + 2)) →^* EOS(STATIC_4674(x0[0]))∧x2[1] + -1 →^* x2[0]∧x1[1] →^* x1[0])

(1) -> (4), if (EOS(STATIC_4674(x0[1] + 2)) →^* EOS(STATIC_4674(x0[4]))∧x2[1] + -1 →^* x2[4]∧x1[1] →^* x1[4])

(2) -> (0), if (EOS(STATIC_4674(x0[2] + 2)) →^* EOS(STATIC_4674(x0[0]))∧x2[2] →^* x2[0]∧x1[2] + -1 →^* x1[0])

(2) -> (4), if (EOS(STATIC_4674(x0[2] + 2)) →^* EOS(STATIC_4674(x0[4]))∧x2[2] →^* x2[4]∧x1[2] + -1 →^* x1[4])

(3) -> (0), if (EOS(STATIC_4674(x0[3] + 1)) →^* EOS(STATIC_4674(x0[0]))∧x2[3] + -1 →^* x2[0]∧x1[3] →^* x1[0])

(3) -> (4), if (EOS(STATIC_4674(x0[3] + 1)) →^* EOS(STATIC_4674(x0[4]))∧x2[3] + -1 →^* x2[4]∧x1[3] →^* x1[4])

(4) -> (5), if (0 < x1[4] + x2[4] ∧EOS(STATIC_4674(x0[4])) →^* EOS(STATIC_4674(x0[5]))∧x2[4] →^* x2[5]∧x1[4] →^* x1[5])

(5) -> (0), if (EOS(STATIC_4674(x0[5])) →^* EOS(STATIC_4674(x0[0]))∧x2[5] + -1 →^* x2[0]∧x1[5] →^* x1[0])

(5) -> (4), if (EOS(STATIC_4674(x0[5])) →^* EOS(STATIC_4674(x0[4]))∧x2[5] + -1 →^* x2[4]∧x1[5] →^* x1[4])

The set Q is empty.

(7) IDPNonInfProof (SOUND transformation)

Used the following options for this NonInfProof:
IDPGPoloSolver: Range: [(-1,2)] IsNat: false Interpretation Shape Heuristic: aprove.DPFramework.IDPProblem.Processors.nonInf.poly.IdpCand1ShapeHeuristic@4289e37 Constraint Generator: NonInfConstraintGenerator: PathGenerator: MetricPathGenerator: Max Left Steps: 0 Max Right Steps: 0

The constraints were generated the following way:
The DP Problem is simplified using the Induction Calculus [NONINF] with the following steps:
Note that final constraints are written in bold face.

For Pair 4674_0_MAIN_LOAD(EOS(STATIC_4674(x0)), x2, x1) → COND_4674_0_MAIN_LOAD(&&(>(x0, -1), <(0, +(x1, x2))), EOS(STATIC_4674(x0)), x2, x1) the following chains were created:

We consider the chain 4674_0_MAIN_LOAD(EOS(STATIC_4674(x0[0])), x2[0], x1[0]) → COND_4674_0_MAIN_LOAD(&&(>(x0[0], -1), <(0, +(x1[0], x2[0]))), EOS(STATIC_4674(x0[0])), x2[0], x1[0]), COND_4674_0_MAIN_LOAD(TRUE, EOS(STATIC_4674(x0[1])), x2[1], x1[1]) → 4674_0_MAIN_LOAD(EOS(STATIC_4674(+(x0[1], 2))), +(x2[1], -1), x1[1]) which results in the following constraint:
(1)    (&&(>(x0[0], -1), <(0, +(x1[0], x2[0])))=TRUE∧EOS(STATIC_4674(x0[0]))=EOS(STATIC_4674(x0[1]))∧x2[0]=x2[1]∧x1[0]=x1[1] ⇒ 4674_0_MAIN_LOAD(EOS(STATIC_4674(x0[0])), x2[0], x1[0])≥NonInfC∧4674_0_MAIN_LOAD(EOS(STATIC_4674(x0[0])), x2[0], x1[0])≥COND_4674_0_MAIN_LOAD(&&(>(x0[0], -1), <(0, +(x1[0], x2[0]))), EOS(STATIC_4674(x0[0])), x2[0], x1[0])∧(U^Increasing(COND_4674_0_MAIN_LOAD(&&(>(x0[0], -1), <(0, +(x1[0], x2[0]))), EOS(STATIC_4674(x0[0])), x2[0], x1[0])), ≥))

We simplified constraint (1) using rules (I), (II), (IV), (IDP_BOOLEAN) which results in the following new constraint:
(2)    (>(x0[0], -1)=TRUE∧<(0, +(x1[0], x2[0]))=TRUE ⇒ 4674_0_MAIN_LOAD(EOS(STATIC_4674(x0[0])), x2[0], x1[0])≥NonInfC∧4674_0_MAIN_LOAD(EOS(STATIC_4674(x0[0])), x2[0], x1[0])≥COND_4674_0_MAIN_LOAD(&&(>(x0[0], -1), <(0, +(x1[0], x2[0]))), EOS(STATIC_4674(x0[0])), x2[0], x1[0])∧(U^Increasing(COND_4674_0_MAIN_LOAD(&&(>(x0[0], -1), <(0, +(x1[0], x2[0]))), EOS(STATIC_4674(x0[0])), x2[0], x1[0])), ≥))

We simplified constraint (2) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(3)    (x0[0] ≥ 0∧x1[0] + [-1] + x2[0] ≥ 0 ⇒ (U^Increasing(COND_4674_0_MAIN_LOAD(&&(>(x0[0], -1), <(0, +(x1[0], x2[0]))), EOS(STATIC_4674(x0[0])), x2[0], x1[0])), ≥)∧[bni_12 + (-1)Bound*bni_12] + [bni_12]x1[0] + [bni_12]x2[0] ≥ 0∧[(-1)bso_13] ≥ 0)

We simplified constraint (3) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(4)    (x0[0] ≥ 0∧x1[0] + [-1] + x2[0] ≥ 0 ⇒ (U^Increasing(COND_4674_0_MAIN_LOAD(&&(>(x0[0], -1), <(0, +(x1[0], x2[0]))), EOS(STATIC_4674(x0[0])), x2[0], x1[0])), ≥)∧[bni_12 + (-1)Bound*bni_12] + [bni_12]x1[0] + [bni_12]x2[0] ≥ 0∧[(-1)bso_13] ≥ 0)

We simplified constraint (4) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(5)    (x0[0] ≥ 0∧x1[0] + [-1] + x2[0] ≥ 0 ⇒ (U^Increasing(COND_4674_0_MAIN_LOAD(&&(>(x0[0], -1), <(0, +(x1[0], x2[0]))), EOS(STATIC_4674(x0[0])), x2[0], x1[0])), ≥)∧[bni_12 + (-1)Bound*bni_12] + [bni_12]x1[0] + [bni_12]x2[0] ≥ 0∧[(-1)bso_13] ≥ 0)

We simplified constraint (5) using rule (IDP_SMT_SPLIT) which results in the following new constraint:
(6)    (x0[0] ≥ 0∧x1[0] ≥ 0 ⇒ (U^Increasing(COND_4674_0_MAIN_LOAD(&&(>(x0[0], -1), <(0, +(x1[0], x2[0]))), EOS(STATIC_4674(x0[0])), x2[0], x1[0])), ≥)∧[(2)bni_12 + (-1)Bound*bni_12] + [bni_12]x1[0] ≥ 0∧[(-1)bso_13] ≥ 0)

We simplified constraint (6) using rule (IDP_SMT_SPLIT) which results in the following new constraints:
(7)    (x0[0] ≥ 0∧x1[0] ≥ 0∧x2[0] ≥ 0 ⇒ (U^Increasing(COND_4674_0_MAIN_LOAD(&&(>(x0[0], -1), <(0, +(x1[0], x2[0]))), EOS(STATIC_4674(x0[0])), x2[0], x1[0])), ≥)∧[(2)bni_12 + (-1)Bound*bni_12] + [bni_12]x1[0] ≥ 0∧[(-1)bso_13] ≥ 0)

(8)    (x0[0] ≥ 0∧x1[0] ≥ 0∧x2[0] ≥ 0 ⇒ (U^Increasing(COND_4674_0_MAIN_LOAD(&&(>(x0[0], -1), <(0, +(x1[0], x2[0]))), EOS(STATIC_4674(x0[0])), x2[0], x1[0])), ≥)∧[(2)bni_12 + (-1)Bound*bni_12] + [bni_12]x1[0] ≥ 0∧[(-1)bso_13] ≥ 0)
We consider the chain 4674_0_MAIN_LOAD(EOS(STATIC_4674(x0[0])), x2[0], x1[0]) → COND_4674_0_MAIN_LOAD(&&(>(x0[0], -1), <(0, +(x1[0], x2[0]))), EOS(STATIC_4674(x0[0])), x2[0], x1[0]), COND_4674_0_MAIN_LOAD(TRUE, EOS(STATIC_4674(x0[2])), x2[2], x1[2]) → 4674_0_MAIN_LOAD(EOS(STATIC_4674(+(x0[2], 2))), x2[2], +(x1[2], -1)) which results in the following constraint:
(9)    (&&(>(x0[0], -1), <(0, +(x1[0], x2[0])))=TRUE∧EOS(STATIC_4674(x0[0]))=EOS(STATIC_4674(x0[2]))∧x2[0]=x2[2]∧x1[0]=x1[2] ⇒ 4674_0_MAIN_LOAD(EOS(STATIC_4674(x0[0])), x2[0], x1[0])≥NonInfC∧4674_0_MAIN_LOAD(EOS(STATIC_4674(x0[0])), x2[0], x1[0])≥COND_4674_0_MAIN_LOAD(&&(>(x0[0], -1), <(0, +(x1[0], x2[0]))), EOS(STATIC_4674(x0[0])), x2[0], x1[0])∧(U^Increasing(COND_4674_0_MAIN_LOAD(&&(>(x0[0], -1), <(0, +(x1[0], x2[0]))), EOS(STATIC_4674(x0[0])), x2[0], x1[0])), ≥))

We simplified constraint (9) using rules (I), (II), (IV), (IDP_BOOLEAN) which results in the following new constraint:
(10)    (>(x0[0], -1)=TRUE∧<(0, +(x1[0], x2[0]))=TRUE ⇒ 4674_0_MAIN_LOAD(EOS(STATIC_4674(x0[0])), x2[0], x1[0])≥NonInfC∧4674_0_MAIN_LOAD(EOS(STATIC_4674(x0[0])), x2[0], x1[0])≥COND_4674_0_MAIN_LOAD(&&(>(x0[0], -1), <(0, +(x1[0], x2[0]))), EOS(STATIC_4674(x0[0])), x2[0], x1[0])∧(U^Increasing(COND_4674_0_MAIN_LOAD(&&(>(x0[0], -1), <(0, +(x1[0], x2[0]))), EOS(STATIC_4674(x0[0])), x2[0], x1[0])), ≥))

We simplified constraint (10) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(11)    (x0[0] ≥ 0∧x1[0] + [-1] + x2[0] ≥ 0 ⇒ (U^Increasing(COND_4674_0_MAIN_LOAD(&&(>(x0[0], -1), <(0, +(x1[0], x2[0]))), EOS(STATIC_4674(x0[0])), x2[0], x1[0])), ≥)∧[bni_12 + (-1)Bound*bni_12] + [bni_12]x1[0] + [bni_12]x2[0] ≥ 0∧[(-1)bso_13] ≥ 0)

We simplified constraint (11) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(12)    (x0[0] ≥ 0∧x1[0] + [-1] + x2[0] ≥ 0 ⇒ (U^Increasing(COND_4674_0_MAIN_LOAD(&&(>(x0[0], -1), <(0, +(x1[0], x2[0]))), EOS(STATIC_4674(x0[0])), x2[0], x1[0])), ≥)∧[bni_12 + (-1)Bound*bni_12] + [bni_12]x1[0] + [bni_12]x2[0] ≥ 0∧[(-1)bso_13] ≥ 0)

We simplified constraint (12) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(13)    (x0[0] ≥ 0∧x1[0] + [-1] + x2[0] ≥ 0 ⇒ (U^Increasing(COND_4674_0_MAIN_LOAD(&&(>(x0[0], -1), <(0, +(x1[0], x2[0]))), EOS(STATIC_4674(x0[0])), x2[0], x1[0])), ≥)∧[bni_12 + (-1)Bound*bni_12] + [bni_12]x1[0] + [bni_12]x2[0] ≥ 0∧[(-1)bso_13] ≥ 0)

We simplified constraint (13) using rule (IDP_SMT_SPLIT) which results in the following new constraint:
(14)    (x0[0] ≥ 0∧x1[0] ≥ 0 ⇒ (U^Increasing(COND_4674_0_MAIN_LOAD(&&(>(x0[0], -1), <(0, +(x1[0], x2[0]))), EOS(STATIC_4674(x0[0])), x2[0], x1[0])), ≥)∧[(2)bni_12 + (-1)Bound*bni_12] + [bni_12]x1[0] ≥ 0∧[(-1)bso_13] ≥ 0)

We simplified constraint (14) using rule (IDP_SMT_SPLIT) which results in the following new constraints:
(15)    (x0[0] ≥ 0∧x1[0] ≥ 0∧x2[0] ≥ 0 ⇒ (U^Increasing(COND_4674_0_MAIN_LOAD(&&(>(x0[0], -1), <(0, +(x1[0], x2[0]))), EOS(STATIC_4674(x0[0])), x2[0], x1[0])), ≥)∧[(2)bni_12 + (-1)Bound*bni_12] + [bni_12]x1[0] ≥ 0∧[(-1)bso_13] ≥ 0)

(16)    (x0[0] ≥ 0∧x1[0] ≥ 0∧x2[0] ≥ 0 ⇒ (U^Increasing(COND_4674_0_MAIN_LOAD(&&(>(x0[0], -1), <(0, +(x1[0], x2[0]))), EOS(STATIC_4674(x0[0])), x2[0], x1[0])), ≥)∧[(2)bni_12 + (-1)Bound*bni_12] + [bni_12]x1[0] ≥ 0∧[(-1)bso_13] ≥ 0)
We consider the chain 4674_0_MAIN_LOAD(EOS(STATIC_4674(x0[0])), x2[0], x1[0]) → COND_4674_0_MAIN_LOAD(&&(>(x0[0], -1), <(0, +(x1[0], x2[0]))), EOS(STATIC_4674(x0[0])), x2[0], x1[0]), COND_4674_0_MAIN_LOAD(TRUE, EOS(STATIC_4674(x0[3])), x2[3], x1[3]) → 4674_0_MAIN_LOAD(EOS(STATIC_4674(+(x0[3], 1))), +(x2[3], -1), x1[3]) which results in the following constraint:
(17)    (&&(>(x0[0], -1), <(0, +(x1[0], x2[0])))=TRUE∧EOS(STATIC_4674(x0[0]))=EOS(STATIC_4674(x0[3]))∧x2[0]=x2[3]∧x1[0]=x1[3] ⇒ 4674_0_MAIN_LOAD(EOS(STATIC_4674(x0[0])), x2[0], x1[0])≥NonInfC∧4674_0_MAIN_LOAD(EOS(STATIC_4674(x0[0])), x2[0], x1[0])≥COND_4674_0_MAIN_LOAD(&&(>(x0[0], -1), <(0, +(x1[0], x2[0]))), EOS(STATIC_4674(x0[0])), x2[0], x1[0])∧(U^Increasing(COND_4674_0_MAIN_LOAD(&&(>(x0[0], -1), <(0, +(x1[0], x2[0]))), EOS(STATIC_4674(x0[0])), x2[0], x1[0])), ≥))

We simplified constraint (17) using rules (I), (II), (IV), (IDP_BOOLEAN) which results in the following new constraint:
(18)    (>(x0[0], -1)=TRUE∧<(0, +(x1[0], x2[0]))=TRUE ⇒ 4674_0_MAIN_LOAD(EOS(STATIC_4674(x0[0])), x2[0], x1[0])≥NonInfC∧4674_0_MAIN_LOAD(EOS(STATIC_4674(x0[0])), x2[0], x1[0])≥COND_4674_0_MAIN_LOAD(&&(>(x0[0], -1), <(0, +(x1[0], x2[0]))), EOS(STATIC_4674(x0[0])), x2[0], x1[0])∧(U^Increasing(COND_4674_0_MAIN_LOAD(&&(>(x0[0], -1), <(0, +(x1[0], x2[0]))), EOS(STATIC_4674(x0[0])), x2[0], x1[0])), ≥))

We simplified constraint (18) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(19)    (x0[0] ≥ 0∧x1[0] + [-1] + x2[0] ≥ 0 ⇒ (U^Increasing(COND_4674_0_MAIN_LOAD(&&(>(x0[0], -1), <(0, +(x1[0], x2[0]))), EOS(STATIC_4674(x0[0])), x2[0], x1[0])), ≥)∧[bni_12 + (-1)Bound*bni_12] + [bni_12]x1[0] + [bni_12]x2[0] ≥ 0∧[(-1)bso_13] ≥ 0)

We simplified constraint (19) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(20)    (x0[0] ≥ 0∧x1[0] + [-1] + x2[0] ≥ 0 ⇒ (U^Increasing(COND_4674_0_MAIN_LOAD(&&(>(x0[0], -1), <(0, +(x1[0], x2[0]))), EOS(STATIC_4674(x0[0])), x2[0], x1[0])), ≥)∧[bni_12 + (-1)Bound*bni_12] + [bni_12]x1[0] + [bni_12]x2[0] ≥ 0∧[(-1)bso_13] ≥ 0)

We simplified constraint (20) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(21)    (x0[0] ≥ 0∧x1[0] + [-1] + x2[0] ≥ 0 ⇒ (U^Increasing(COND_4674_0_MAIN_LOAD(&&(>(x0[0], -1), <(0, +(x1[0], x2[0]))), EOS(STATIC_4674(x0[0])), x2[0], x1[0])), ≥)∧[bni_12 + (-1)Bound*bni_12] + [bni_12]x1[0] + [bni_12]x2[0] ≥ 0∧[(-1)bso_13] ≥ 0)

We simplified constraint (21) using rule (IDP_SMT_SPLIT) which results in the following new constraint:
(22)    (x0[0] ≥ 0∧x1[0] ≥ 0 ⇒ (U^Increasing(COND_4674_0_MAIN_LOAD(&&(>(x0[0], -1), <(0, +(x1[0], x2[0]))), EOS(STATIC_4674(x0[0])), x2[0], x1[0])), ≥)∧[(2)bni_12 + (-1)Bound*bni_12] + [bni_12]x1[0] ≥ 0∧[(-1)bso_13] ≥ 0)

We simplified constraint (22) using rule (IDP_SMT_SPLIT) which results in the following new constraints:
(23)    (x0[0] ≥ 0∧x1[0] ≥ 0∧x2[0] ≥ 0 ⇒ (U^Increasing(COND_4674_0_MAIN_LOAD(&&(>(x0[0], -1), <(0, +(x1[0], x2[0]))), EOS(STATIC_4674(x0[0])), x2[0], x1[0])), ≥)∧[(2)bni_12 + (-1)Bound*bni_12] + [bni_12]x1[0] ≥ 0∧[(-1)bso_13] ≥ 0)

(24)    (x0[0] ≥ 0∧x1[0] ≥ 0∧x2[0] ≥ 0 ⇒ (U^Increasing(COND_4674_0_MAIN_LOAD(&&(>(x0[0], -1), <(0, +(x1[0], x2[0]))), EOS(STATIC_4674(x0[0])), x2[0], x1[0])), ≥)∧[(2)bni_12 + (-1)Bound*bni_12] + [bni_12]x1[0] ≥ 0∧[(-1)bso_13] ≥ 0)

For Pair COND_4674_0_MAIN_LOAD(TRUE, EOS(STATIC_4674(x0)), x2, x1) → 4674_0_MAIN_LOAD(EOS(STATIC_4674(+(x0, 2))), +(x2, -1), x1) the following chains were created:

We consider the chain COND_4674_0_MAIN_LOAD(TRUE, EOS(STATIC_4674(x0[1])), x2[1], x1[1]) → 4674_0_MAIN_LOAD(EOS(STATIC_4674(+(x0[1], 2))), +(x2[1], -1), x1[1]) which results in the following constraint:
(25)    (COND_4674_0_MAIN_LOAD(TRUE, EOS(STATIC_4674(x0[1])), x2[1], x1[1])≥NonInfC∧COND_4674_0_MAIN_LOAD(TRUE, EOS(STATIC_4674(x0[1])), x2[1], x1[1])≥4674_0_MAIN_LOAD(EOS(STATIC_4674(+(x0[1], 2))), +(x2[1], -1), x1[1])∧(U^Increasing(4674_0_MAIN_LOAD(EOS(STATIC_4674(+(x0[1], 2))), +(x2[1], -1), x1[1])), ≥))

We simplified constraint (25) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(26)    ((U^Increasing(4674_0_MAIN_LOAD(EOS(STATIC_4674(+(x0[1], 2))), +(x2[1], -1), x1[1])), ≥)∧[bni_14] = 0∧[1 + (-1)bso_15] ≥ 0)

We simplified constraint (26) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(27)    ((U^Increasing(4674_0_MAIN_LOAD(EOS(STATIC_4674(+(x0[1], 2))), +(x2[1], -1), x1[1])), ≥)∧[bni_14] = 0∧[1 + (-1)bso_15] ≥ 0)

We simplified constraint (27) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(28)    ((U^Increasing(4674_0_MAIN_LOAD(EOS(STATIC_4674(+(x0[1], 2))), +(x2[1], -1), x1[1])), ≥)∧[bni_14] = 0∧[1 + (-1)bso_15] ≥ 0)

We simplified constraint (28) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:
(29)    ((U^Increasing(4674_0_MAIN_LOAD(EOS(STATIC_4674(+(x0[1], 2))), +(x2[1], -1), x1[1])), ≥)∧[bni_14] = 0∧0 = 0∧0 = 0∧0 = 0∧[1 + (-1)bso_15] ≥ 0)

For Pair COND_4674_0_MAIN_LOAD(TRUE, EOS(STATIC_4674(x0)), x2, x1) → 4674_0_MAIN_LOAD(EOS(STATIC_4674(+(x0, 2))), x2, +(x1, -1)) the following chains were created:

We consider the chain COND_4674_0_MAIN_LOAD(TRUE, EOS(STATIC_4674(x0[2])), x2[2], x1[2]) → 4674_0_MAIN_LOAD(EOS(STATIC_4674(+(x0[2], 2))), x2[2], +(x1[2], -1)) which results in the following constraint:
(30)    (COND_4674_0_MAIN_LOAD(TRUE, EOS(STATIC_4674(x0[2])), x2[2], x1[2])≥NonInfC∧COND_4674_0_MAIN_LOAD(TRUE, EOS(STATIC_4674(x0[2])), x2[2], x1[2])≥4674_0_MAIN_LOAD(EOS(STATIC_4674(+(x0[2], 2))), x2[2], +(x1[2], -1))∧(U^Increasing(4674_0_MAIN_LOAD(EOS(STATIC_4674(+(x0[2], 2))), x2[2], +(x1[2], -1))), ≥))

We simplified constraint (30) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(31)    ((U^Increasing(4674_0_MAIN_LOAD(EOS(STATIC_4674(+(x0[2], 2))), x2[2], +(x1[2], -1))), ≥)∧[bni_16] = 0∧[1 + (-1)bso_17] ≥ 0)

We simplified constraint (31) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(32)    ((U^Increasing(4674_0_MAIN_LOAD(EOS(STATIC_4674(+(x0[2], 2))), x2[2], +(x1[2], -1))), ≥)∧[bni_16] = 0∧[1 + (-1)bso_17] ≥ 0)

We simplified constraint (32) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(33)    ((U^Increasing(4674_0_MAIN_LOAD(EOS(STATIC_4674(+(x0[2], 2))), x2[2], +(x1[2], -1))), ≥)∧[bni_16] = 0∧[1 + (-1)bso_17] ≥ 0)

We simplified constraint (33) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:
(34)    ((U^Increasing(4674_0_MAIN_LOAD(EOS(STATIC_4674(+(x0[2], 2))), x2[2], +(x1[2], -1))), ≥)∧[bni_16] = 0∧0 = 0∧0 = 0∧0 = 0∧[1 + (-1)bso_17] ≥ 0)

For Pair COND_4674_0_MAIN_LOAD(TRUE, EOS(STATIC_4674(x0)), x2, x1) → 4674_0_MAIN_LOAD(EOS(STATIC_4674(+(x0, 1))), +(x2, -1), x1) the following chains were created:

We consider the chain COND_4674_0_MAIN_LOAD(TRUE, EOS(STATIC_4674(x0[3])), x2[3], x1[3]) → 4674_0_MAIN_LOAD(EOS(STATIC_4674(+(x0[3], 1))), +(x2[3], -1), x1[3]) which results in the following constraint:
(35)    (COND_4674_0_MAIN_LOAD(TRUE, EOS(STATIC_4674(x0[3])), x2[3], x1[3])≥NonInfC∧COND_4674_0_MAIN_LOAD(TRUE, EOS(STATIC_4674(x0[3])), x2[3], x1[3])≥4674_0_MAIN_LOAD(EOS(STATIC_4674(+(x0[3], 1))), +(x2[3], -1), x1[3])∧(U^Increasing(4674_0_MAIN_LOAD(EOS(STATIC_4674(+(x0[3], 1))), +(x2[3], -1), x1[3])), ≥))

We simplified constraint (35) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(36)    ((U^Increasing(4674_0_MAIN_LOAD(EOS(STATIC_4674(+(x0[3], 1))), +(x2[3], -1), x1[3])), ≥)∧[bni_18] = 0∧[1 + (-1)bso_19] ≥ 0)

We simplified constraint (36) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(37)    ((U^Increasing(4674_0_MAIN_LOAD(EOS(STATIC_4674(+(x0[3], 1))), +(x2[3], -1), x1[3])), ≥)∧[bni_18] = 0∧[1 + (-1)bso_19] ≥ 0)

We simplified constraint (37) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(38)    ((U^Increasing(4674_0_MAIN_LOAD(EOS(STATIC_4674(+(x0[3], 1))), +(x2[3], -1), x1[3])), ≥)∧[bni_18] = 0∧[1 + (-1)bso_19] ≥ 0)

We simplified constraint (38) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:
(39)    ((U^Increasing(4674_0_MAIN_LOAD(EOS(STATIC_4674(+(x0[3], 1))), +(x2[3], -1), x1[3])), ≥)∧[bni_18] = 0∧0 = 0∧0 = 0∧0 = 0∧[1 + (-1)bso_19] ≥ 0)

For Pair 4674_0_MAIN_LOAD(EOS(STATIC_4674(x0)), x2, x1) → COND_4674_0_MAIN_LOAD3(<(0, +(x1, x2)), EOS(STATIC_4674(x0)), x2, x1) the following chains were created:

We consider the chain 4674_0_MAIN_LOAD(EOS(STATIC_4674(x0[4])), x2[4], x1[4]) → COND_4674_0_MAIN_LOAD3(<(0, +(x1[4], x2[4])), EOS(STATIC_4674(x0[4])), x2[4], x1[4]), COND_4674_0_MAIN_LOAD3(TRUE, EOS(STATIC_4674(x0[5])), x2[5], x1[5]) → 4674_0_MAIN_LOAD(EOS(STATIC_4674(x0[5])), +(x2[5], -1), x1[5]) which results in the following constraint:
(40)    (<(0, +(x1[4], x2[4]))=TRUE∧EOS(STATIC_4674(x0[4]))=EOS(STATIC_4674(x0[5]))∧x2[4]=x2[5]∧x1[4]=x1[5] ⇒ 4674_0_MAIN_LOAD(EOS(STATIC_4674(x0[4])), x2[4], x1[4])≥NonInfC∧4674_0_MAIN_LOAD(EOS(STATIC_4674(x0[4])), x2[4], x1[4])≥COND_4674_0_MAIN_LOAD3(<(0, +(x1[4], x2[4])), EOS(STATIC_4674(x0[4])), x2[4], x1[4])∧(U^Increasing(COND_4674_0_MAIN_LOAD3(<(0, +(x1[4], x2[4])), EOS(STATIC_4674(x0[4])), x2[4], x1[4])), ≥))

We simplified constraint (40) using rules (I), (II), (IV) which results in the following new constraint:
(41)    (<(0, +(x1[4], x2[4]))=TRUE ⇒ 4674_0_MAIN_LOAD(EOS(STATIC_4674(x0[4])), x2[4], x1[4])≥NonInfC∧4674_0_MAIN_LOAD(EOS(STATIC_4674(x0[4])), x2[4], x1[4])≥COND_4674_0_MAIN_LOAD3(<(0, +(x1[4], x2[4])), EOS(STATIC_4674(x0[4])), x2[4], x1[4])∧(U^Increasing(COND_4674_0_MAIN_LOAD3(<(0, +(x1[4], x2[4])), EOS(STATIC_4674(x0[4])), x2[4], x1[4])), ≥))

We simplified constraint (41) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(42)    (x1[4] + [-1] + x2[4] ≥ 0 ⇒ (U^Increasing(COND_4674_0_MAIN_LOAD3(<(0, +(x1[4], x2[4])), EOS(STATIC_4674(x0[4])), x2[4], x1[4])), ≥)∧[bni_20 + (-1)Bound*bni_20] + [bni_20]x1[4] + [bni_20]x2[4] ≥ 0∧[(-1)bso_21] ≥ 0)

We simplified constraint (42) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(43)    (x1[4] + [-1] + x2[4] ≥ 0 ⇒ (U^Increasing(COND_4674_0_MAIN_LOAD3(<(0, +(x1[4], x2[4])), EOS(STATIC_4674(x0[4])), x2[4], x1[4])), ≥)∧[bni_20 + (-1)Bound*bni_20] + [bni_20]x1[4] + [bni_20]x2[4] ≥ 0∧[(-1)bso_21] ≥ 0)

We simplified constraint (43) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(44)    (x1[4] + [-1] + x2[4] ≥ 0 ⇒ (U^Increasing(COND_4674_0_MAIN_LOAD3(<(0, +(x1[4], x2[4])), EOS(STATIC_4674(x0[4])), x2[4], x1[4])), ≥)∧[bni_20 + (-1)Bound*bni_20] + [bni_20]x1[4] + [bni_20]x2[4] ≥ 0∧[(-1)bso_21] ≥ 0)

We simplified constraint (44) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:
(45)    (x1[4] + [-1] + x2[4] ≥ 0 ⇒ (U^Increasing(COND_4674_0_MAIN_LOAD3(<(0, +(x1[4], x2[4])), EOS(STATIC_4674(x0[4])), x2[4], x1[4])), ≥)∧0 = 0∧[bni_20 + (-1)Bound*bni_20] + [bni_20]x1[4] + [bni_20]x2[4] ≥ 0∧0 = 0∧[(-1)bso_21] ≥ 0)

We simplified constraint (45) using rule (IDP_SMT_SPLIT) which results in the following new constraint:
(46)    (x1[4] ≥ 0 ⇒ (U^Increasing(COND_4674_0_MAIN_LOAD3(<(0, +(x1[4], x2[4])), EOS(STATIC_4674(x0[4])), x2[4], x1[4])), ≥)∧0 = 0∧[(2)bni_20 + (-1)Bound*bni_20] + [bni_20]x1[4] ≥ 0∧0 = 0∧[(-1)bso_21] ≥ 0)

We simplified constraint (46) using rule (IDP_SMT_SPLIT) which results in the following new constraints:
(47)    (x1[4] ≥ 0∧x2[4] ≥ 0 ⇒ (U^Increasing(COND_4674_0_MAIN_LOAD3(<(0, +(x1[4], x2[4])), EOS(STATIC_4674(x0[4])), x2[4], x1[4])), ≥)∧0 = 0∧[(2)bni_20 + (-1)Bound*bni_20] + [bni_20]x1[4] ≥ 0∧0 = 0∧[(-1)bso_21] ≥ 0)

(48)    (x1[4] ≥ 0∧x2[4] ≥ 0 ⇒ (U^Increasing(COND_4674_0_MAIN_LOAD3(<(0, +(x1[4], x2[4])), EOS(STATIC_4674(x0[4])), x2[4], x1[4])), ≥)∧0 = 0∧[(2)bni_20 + (-1)Bound*bni_20] + [bni_20]x1[4] ≥ 0∧0 = 0∧[(-1)bso_21] ≥ 0)

For Pair COND_4674_0_MAIN_LOAD3(TRUE, EOS(STATIC_4674(x0)), x2, x1) → 4674_0_MAIN_LOAD(EOS(STATIC_4674(x0)), +(x2, -1), x1) the following chains were created:

We consider the chain COND_4674_0_MAIN_LOAD3(TRUE, EOS(STATIC_4674(x0[5])), x2[5], x1[5]) → 4674_0_MAIN_LOAD(EOS(STATIC_4674(x0[5])), +(x2[5], -1), x1[5]) which results in the following constraint:
(49)    (COND_4674_0_MAIN_LOAD3(TRUE, EOS(STATIC_4674(x0[5])), x2[5], x1[5])≥NonInfC∧COND_4674_0_MAIN_LOAD3(TRUE, EOS(STATIC_4674(x0[5])), x2[5], x1[5])≥4674_0_MAIN_LOAD(EOS(STATIC_4674(x0[5])), +(x2[5], -1), x1[5])∧(U^Increasing(4674_0_MAIN_LOAD(EOS(STATIC_4674(x0[5])), +(x2[5], -1), x1[5])), ≥))

We simplified constraint (49) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(50)    ((U^Increasing(4674_0_MAIN_LOAD(EOS(STATIC_4674(x0[5])), +(x2[5], -1), x1[5])), ≥)∧[bni_22] = 0∧[1 + (-1)bso_23] ≥ 0)

We simplified constraint (50) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(51)    ((U^Increasing(4674_0_MAIN_LOAD(EOS(STATIC_4674(x0[5])), +(x2[5], -1), x1[5])), ≥)∧[bni_22] = 0∧[1 + (-1)bso_23] ≥ 0)

We simplified constraint (51) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(52)    ((U^Increasing(4674_0_MAIN_LOAD(EOS(STATIC_4674(x0[5])), +(x2[5], -1), x1[5])), ≥)∧[bni_22] = 0∧[1 + (-1)bso_23] ≥ 0)

We simplified constraint (52) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:
(53)    ((U^Increasing(4674_0_MAIN_LOAD(EOS(STATIC_4674(x0[5])), +(x2[5], -1), x1[5])), ≥)∧[bni_22] = 0∧0 = 0∧0 = 0∧0 = 0∧[1 + (-1)bso_23] ≥ 0)

To summarize, we get the following constraints P_≥ for the following pairs.

4674_0_MAIN_LOAD(EOS(STATIC_4674(x0)), x2, x1) → COND_4674_0_MAIN_LOAD(&&(>(x0, -1), <(0, +(x1, x2))), EOS(STATIC_4674(x0)), x2, x1)
- (x0[0] ≥ 0∧x1[0] ≥ 0∧x2[0] ≥ 0 ⇒ (U^Increasing(COND_4674_0_MAIN_LOAD(&&(>(x0[0], -1), <(0, +(x1[0], x2[0]))), EOS(STATIC_4674(x0[0])), x2[0], x1[0])), ≥)∧[(2)bni_12 + (-1)Bound*bni_12] + [bni_12]x1[0] ≥ 0∧[(-1)bso_13] ≥ 0)
- (x0[0] ≥ 0∧x1[0] ≥ 0∧x2[0] ≥ 0 ⇒ (U^Increasing(COND_4674_0_MAIN_LOAD(&&(>(x0[0], -1), <(0, +(x1[0], x2[0]))), EOS(STATIC_4674(x0[0])), x2[0], x1[0])), ≥)∧[(2)bni_12 + (-1)Bound*bni_12] + [bni_12]x1[0] ≥ 0∧[(-1)bso_13] ≥ 0)
- (x0[0] ≥ 0∧x1[0] ≥ 0∧x2[0] ≥ 0 ⇒ (U^Increasing(COND_4674_0_MAIN_LOAD(&&(>(x0[0], -1), <(0, +(x1[0], x2[0]))), EOS(STATIC_4674(x0[0])), x2[0], x1[0])), ≥)∧[(2)bni_12 + (-1)Bound*bni_12] + [bni_12]x1[0] ≥ 0∧[(-1)bso_13] ≥ 0)
- (x0[0] ≥ 0∧x1[0] ≥ 0∧x2[0] ≥ 0 ⇒ (U^Increasing(COND_4674_0_MAIN_LOAD(&&(>(x0[0], -1), <(0, +(x1[0], x2[0]))), EOS(STATIC_4674(x0[0])), x2[0], x1[0])), ≥)∧[(2)bni_12 + (-1)Bound*bni_12] + [bni_12]x1[0] ≥ 0∧[(-1)bso_13] ≥ 0)
- (x0[0] ≥ 0∧x1[0] ≥ 0∧x2[0] ≥ 0 ⇒ (U^Increasing(COND_4674_0_MAIN_LOAD(&&(>(x0[0], -1), <(0, +(x1[0], x2[0]))), EOS(STATIC_4674(x0[0])), x2[0], x1[0])), ≥)∧[(2)bni_12 + (-1)Bound*bni_12] + [bni_12]x1[0] ≥ 0∧[(-1)bso_13] ≥ 0)
- (x0[0] ≥ 0∧x1[0] ≥ 0∧x2[0] ≥ 0 ⇒ (U^Increasing(COND_4674_0_MAIN_LOAD(&&(>(x0[0], -1), <(0, +(x1[0], x2[0]))), EOS(STATIC_4674(x0[0])), x2[0], x1[0])), ≥)∧[(2)bni_12 + (-1)Bound*bni_12] + [bni_12]x1[0] ≥ 0∧[(-1)bso_13] ≥ 0)
COND_4674_0_MAIN_LOAD(TRUE, EOS(STATIC_4674(x0)), x2, x1) → 4674_0_MAIN_LOAD(EOS(STATIC_4674(+(x0, 2))), +(x2, -1), x1)
- ((U^Increasing(4674_0_MAIN_LOAD(EOS(STATIC_4674(+(x0[1], 2))), +(x2[1], -1), x1[1])), ≥)∧[bni_14] = 0∧0 = 0∧0 = 0∧0 = 0∧[1 + (-1)bso_15] ≥ 0)
COND_4674_0_MAIN_LOAD(TRUE, EOS(STATIC_4674(x0)), x2, x1) → 4674_0_MAIN_LOAD(EOS(STATIC_4674(+(x0, 2))), x2, +(x1, -1))
- ((U^Increasing(4674_0_MAIN_LOAD(EOS(STATIC_4674(+(x0[2], 2))), x2[2], +(x1[2], -1))), ≥)∧[bni_16] = 0∧0 = 0∧0 = 0∧0 = 0∧[1 + (-1)bso_17] ≥ 0)
COND_4674_0_MAIN_LOAD(TRUE, EOS(STATIC_4674(x0)), x2, x1) → 4674_0_MAIN_LOAD(EOS(STATIC_4674(+(x0, 1))), +(x2, -1), x1)
- ((U^Increasing(4674_0_MAIN_LOAD(EOS(STATIC_4674(+(x0[3], 1))), +(x2[3], -1), x1[3])), ≥)∧[bni_18] = 0∧0 = 0∧0 = 0∧0 = 0∧[1 + (-1)bso_19] ≥ 0)
4674_0_MAIN_LOAD(EOS(STATIC_4674(x0)), x2, x1) → COND_4674_0_MAIN_LOAD3(<(0, +(x1, x2)), EOS(STATIC_4674(x0)), x2, x1)
- (x1[4] ≥ 0∧x2[4] ≥ 0 ⇒ (U^Increasing(COND_4674_0_MAIN_LOAD3(<(0, +(x1[4], x2[4])), EOS(STATIC_4674(x0[4])), x2[4], x1[4])), ≥)∧0 = 0∧[(2)bni_20 + (-1)Bound*bni_20] + [bni_20]x1[4] ≥ 0∧0 = 0∧[(-1)bso_21] ≥ 0)
- (x1[4] ≥ 0∧x2[4] ≥ 0 ⇒ (U^Increasing(COND_4674_0_MAIN_LOAD3(<(0, +(x1[4], x2[4])), EOS(STATIC_4674(x0[4])), x2[4], x1[4])), ≥)∧0 = 0∧[(2)bni_20 + (-1)Bound*bni_20] + [bni_20]x1[4] ≥ 0∧0 = 0∧[(-1)bso_21] ≥ 0)
COND_4674_0_MAIN_LOAD3(TRUE, EOS(STATIC_4674(x0)), x2, x1) → 4674_0_MAIN_LOAD(EOS(STATIC_4674(x0)), +(x2, -1), x1)
- ((U^Increasing(4674_0_MAIN_LOAD(EOS(STATIC_4674(x0[5])), +(x2[5], -1), x1[5])), ≥)∧[bni_22] = 0∧0 = 0∧0 = 0∧0 = 0∧[1 + (-1)bso_23] ≥ 0)

The constraints for P_> respective P_bound are constructed from P_≥ where we just replace every occurence of "t ≥ s" in P_≥ by "t > s" respective "t ≥ c". Here c stands for the fresh constant used for P_bound.
Using the following integer polynomial ordering the resulting constraints can be solved
Polynomial interpretation over integers[POLO]:

POL(TRUE) = 0
POL(FALSE) = 0
POL(4674_0_MAIN_LOAD(x₁, x₂, x₃)) = [1] + x₃ + x₂
POL(EOS(x₁)) = x₁
POL(STATIC_4674(x₁)) = x₁
POL(COND_4674_0_MAIN_LOAD(x₁, x₂, x₃, x₄)) = [1] + x₄ + x₃
POL(&&(x₁, x₂)) = [-1]
POL(>(x₁, x₂)) = [-1]
POL(-1) = [-1]
POL(<(x₁, x₂)) = [-1]
POL(0) = 0
POL(+(x₁, x₂)) = x₁ + x₂
POL(2) = [2]
POL(1) = [1]
POL(COND_4674_0_MAIN_LOAD3(x₁, x₂, x₃, x₄)) = [1] + x₄ + x₃

The following pairs are in P_>:

COND_4674_0_MAIN_LOAD(TRUE, EOS(STATIC_4674(x0[1])), x2[1], x1[1]) → 4674_0_MAIN_LOAD(EOS(STATIC_4674(+(x0[1], 2))), +(x2[1], -1), x1[1])
COND_4674_0_MAIN_LOAD(TRUE, EOS(STATIC_4674(x0[2])), x2[2], x1[2]) → 4674_0_MAIN_LOAD(EOS(STATIC_4674(+(x0[2], 2))), x2[2], +(x1[2], -1))
COND_4674_0_MAIN_LOAD(TRUE, EOS(STATIC_4674(x0[3])), x2[3], x1[3]) → 4674_0_MAIN_LOAD(EOS(STATIC_4674(+(x0[3], 1))), +(x2[3], -1), x1[3])
COND_4674_0_MAIN_LOAD3(TRUE, EOS(STATIC_4674(x0[5])), x2[5], x1[5]) → 4674_0_MAIN_LOAD(EOS(STATIC_4674(x0[5])), +(x2[5], -1), x1[5])

The following pairs are in P_bound:

4674_0_MAIN_LOAD(EOS(STATIC_4674(x0[0])), x2[0], x1[0]) → COND_4674_0_MAIN_LOAD(&&(>(x0[0], -1), <(0, +(x1[0], x2[0]))), EOS(STATIC_4674(x0[0])), x2[0], x1[0])
4674_0_MAIN_LOAD(EOS(STATIC_4674(x0[4])), x2[4], x1[4]) → COND_4674_0_MAIN_LOAD3(<(0, +(x1[4], x2[4])), EOS(STATIC_4674(x0[4])), x2[4], x1[4])

The following pairs are in P_≥:

4674_0_MAIN_LOAD(EOS(STATIC_4674(x0[0])), x2[0], x1[0]) → COND_4674_0_MAIN_LOAD(&&(>(x0[0], -1), <(0, +(x1[0], x2[0]))), EOS(STATIC_4674(x0[0])), x2[0], x1[0])
4674_0_MAIN_LOAD(EOS(STATIC_4674(x0[4])), x2[4], x1[4]) → COND_4674_0_MAIN_LOAD3(<(0, +(x1[4], x2[4])), EOS(STATIC_4674(x0[4])), x2[4], x1[4])

There are no usable rules.

(8) Complex Obligation (AND)

(9) Obligation:

IDP problem:
The following function symbols are pre-defined:

!=	~	Neq: (Integer, Integer) -> Boolean
*	~	Mul: (Integer, Integer) -> Integer
>=	~	Ge: (Integer, Integer) -> Boolean
-1	~	UnaryMinus: (Integer) -> Integer
\|	~	Bwor: (Integer, Integer) -> Integer
/	~	Div: (Integer, Integer) -> Integer
=	~	Eq: (Integer, Integer) -> Boolean
	~	Bwxor: (Integer, Integer) -> Integer
\|\|	~	Lor: (Boolean, Boolean) -> Boolean
!	~	Lnot: (Boolean) -> Boolean
<	~	Lt: (Integer, Integer) -> Boolean
-	~	Sub: (Integer, Integer) -> Integer
<=	~	Le: (Integer, Integer) -> Boolean
>	~	Gt: (Integer, Integer) -> Boolean
~	~	Bwnot: (Integer) -> Integer
%	~	Mod: (Integer, Integer) -> Integer
&	~	Bwand: (Integer, Integer) -> Integer
+	~	Add: (Integer, Integer) -> Integer
&&	~	Land: (Boolean, Boolean) -> Boolean

The following domains are used:

Boolean, Integer

(10) IDependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 0 SCCs with 2 less nodes.

(11) TRUE

(12) Obligation:

IDP problem:
The following function symbols are pre-defined:

!=	~	Neq: (Integer, Integer) -> Boolean
*	~	Mul: (Integer, Integer) -> Integer
>=	~	Ge: (Integer, Integer) -> Boolean
-1	~	UnaryMinus: (Integer) -> Integer
\|	~	Bwor: (Integer, Integer) -> Integer
/	~	Div: (Integer, Integer) -> Integer
=	~	Eq: (Integer, Integer) -> Boolean
	~	Bwxor: (Integer, Integer) -> Integer
\|\|	~	Lor: (Boolean, Boolean) -> Boolean
!	~	Lnot: (Boolean) -> Boolean
<	~	Lt: (Integer, Integer) -> Boolean
-	~	Sub: (Integer, Integer) -> Integer
<=	~	Le: (Integer, Integer) -> Boolean
>	~	Gt: (Integer, Integer) -> Boolean
~	~	Bwnot: (Integer) -> Integer
%	~	Mod: (Integer, Integer) -> Integer
&	~	Bwand: (Integer, Integer) -> Integer
+	~	Add: (Integer, Integer) -> Integer
&&	~	Land: (Boolean, Boolean) -> Boolean

The following domains are used:

Integer

R is empty.

The integer pair graph contains the following rules and edges:
(1): COND_4674_0_MAIN_LOAD(TRUE, EOS(STATIC_4674(x0[1])), x2[1], x1[1]) → 4674_0_MAIN_LOAD(EOS(STATIC_4674(x0[1] + 2)), x2[1] + -1, x1[1])
(2): COND_4674_0_MAIN_LOAD(TRUE, EOS(STATIC_4674(x0[2])), x2[2], x1[2]) → 4674_0_MAIN_LOAD(EOS(STATIC_4674(x0[2] + 2)), x2[2], x1[2] + -1)
(3): COND_4674_0_MAIN_LOAD(TRUE, EOS(STATIC_4674(x0[3])), x2[3], x1[3]) → 4674_0_MAIN_LOAD(EOS(STATIC_4674(x0[3] + 1)), x2[3] + -1, x1[3])
(5): COND_4674_0_MAIN_LOAD3(TRUE, EOS(STATIC_4674(x0[5])), x2[5], x1[5]) → 4674_0_MAIN_LOAD(EOS(STATIC_4674(x0[5])), x2[5] + -1, x1[5])

The set Q is empty.

(13) IDependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 0 SCCs with 4 less nodes.

(0) Obligation:

(1) JBCToGraph (SOUND transformation)

(2) Obligation:

(3) TerminationGraphToSCCProof (SOUND transformation)

(4) Obligation:

(5) SCCToIDPv1Proof (SOUND transformation)

(6) Obligation:

(7) IDPNonInfProof (SOUND transformation)

(8) Complex Obligation (AND)

(9) Obligation:

(10) IDependencyGraphProof (EQUIVALENT transformation)

(11) TRUE

(12) Obligation:

(13) IDependencyGraphProof (EQUIVALENT transformation)

(14) TRUE