Termination proof of /tmp/tmpZm2rBl/Test11.jar

Termination of the given JBC could be proven:

0 JBC

↳1 JBCToGraph (⇒, 1180 ms)

↳2 JBCTerminationGraph

↳3 TerminationGraphToSCCProof (⇒, 0 ms)

↳4 JBCTerminationSCC

↳5 SCCToIDPv1Proof (⇒, 600 ms)

↳6 IDP

↳7 IDPNonInfProof (⇒, 410 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:
3897_0_main_Load(EOS(STATIC_3897(i1332)), i1333, i443, i1333) → 3899_0_main_IntArithmetic(EOS(STATIC_3899(i1332)), i1333, i443, i1333, i443)
3899_0_main_IntArithmetic(EOS(STATIC_3899(i1332)), i1333, i443, i1333, i443) → 3900_0_main_LE(EOS(STATIC_3900(i1332)), i1333, i443, +(i1333, i443))
3900_0_main_LE(EOS(STATIC_3900(i1332)), i1333, i443, i1343) → 3902_0_main_LE(EOS(STATIC_3902(i1332)), i1333, i443, i1343)
3902_0_main_LE(EOS(STATIC_3902(i1332)), i1333, i443, i1343) → 3905_0_main_InvokeMethod(EOS(STATIC_3905(i1332)), i1333, i443) | >(i1343, 0)
3905_0_main_InvokeMethod(EOS(STATIC_3905(i1332)), i1333, i443) → 3907_0_random_FieldAccess(EOS(STATIC_3907(i1332)), i1333, i443)
3907_0_random_FieldAccess(EOS(STATIC_3907(i1332)), i1333, i443) → 3909_0_random_FieldAccess(EOS(STATIC_3909(i1332)), i1333, i443, i1332)
3909_0_random_FieldAccess(EOS(STATIC_3909(i1332)), i1333, i443, i1332) → 3910_0_random_ArrayLength(EOS(STATIC_3910(i1332)), i1333, i443, i1332, java.lang.Object(ARRAY(i183)))
3910_0_random_ArrayLength(EOS(STATIC_3910(i1332)), i1333, i443, i1332, java.lang.Object(ARRAY(i183))) → 3911_0_random_LT(EOS(STATIC_3911(i1332)), i1333, i443, i1332, i183) | >=(i183, 0)
3911_0_random_LT(EOS(STATIC_3911(i1332)), i1333, i443, i1332, i183) → 3913_0_random_LT(EOS(STATIC_3913(i1332)), i1333, i443, i1332, i183)
3911_0_random_LT(EOS(STATIC_3911(i1332)), i1333, i443, i1332, i183) → 3914_0_random_LT(EOS(STATIC_3914(i1332)), i1333, i443, i1332, i183)
3913_0_random_LT(EOS(STATIC_3913(i1332)), i1333, i443, i1332, i183) → 3915_0_random_FieldAccess(EOS(STATIC_3915(i1332)), i1333, i443) | <(i1332, i183)
3915_0_random_FieldAccess(EOS(STATIC_3915(i1332)), i1333, i443) → 3917_0_random_FieldAccess(EOS(STATIC_3917(i1332)), i1333, i443, java.lang.Object(ARRAY(i183)))
3917_0_random_FieldAccess(EOS(STATIC_3917(i1332)), i1333, i443, java.lang.Object(ARRAY(i183))) → 3920_0_random_ArrayAccess(EOS(STATIC_3920(i1332)), i1333, i443, java.lang.Object(ARRAY(i183)), i1332)
3920_0_random_ArrayAccess(EOS(STATIC_3920(i1348)), i1333, i443, java.lang.Object(ARRAY(i183)), i1348) → 3923_0_random_ArrayAccess(EOS(STATIC_3923(i1348)), i1333, i443, java.lang.Object(ARRAY(i183)), i1348)
3923_0_random_ArrayAccess(EOS(STATIC_3923(i1348)), i1333, i443, java.lang.Object(ARRAY(i183)), i1348) → 3927_0_random_ArrayAccess(EOS(STATIC_3927(i1348)), i1333, i443, java.lang.Object(ARRAY(i183)), i1348)
3927_0_random_ArrayAccess(EOS(STATIC_3927(i1348)), i1333, i443, java.lang.Object(ARRAY(i183)), i1348) → 3930_0_random_Store(EOS(STATIC_3930(i1348)), i1333, i443, o2532)
3930_0_random_Store(EOS(STATIC_3930(i1348)), i1333, i443, o2532) → 3935_0_random_FieldAccess(EOS(STATIC_3935(i1348)), i1333, i443, o2532)
3935_0_random_FieldAccess(EOS(STATIC_3935(i1348)), i1333, i443, o2532) → 3939_0_random_ConstantStackPush(EOS(STATIC_3939(i1348)), i1333, i443, o2532, i1348)
3939_0_random_ConstantStackPush(EOS(STATIC_3939(i1348)), i1333, i443, o2532, i1348) → 3944_0_random_IntArithmetic(EOS(STATIC_3944(i1348)), i1333, i443, o2532, i1348, 1)
3944_0_random_IntArithmetic(EOS(STATIC_3944(i1348)), i1333, i443, o2532, i1348, matching1) → 3950_0_random_FieldAccess(EOS(STATIC_3950(i1348)), i1333, i443, o2532, +(i1348, 1)) | &&(>=(i1348, 0), =(matching1, 1))
3950_0_random_FieldAccess(EOS(STATIC_3950(i1348)), i1333, i443, o2532, i1350) → 3955_0_random_Load(EOS(STATIC_3955(i1350)), i1333, i443, o2532)
3955_0_random_Load(EOS(STATIC_3955(i1350)), i1333, i443, o2532) → 3961_0_random_InvokeMethod(EOS(STATIC_3961(i1350)), i1333, i443, o2532)
3961_0_random_InvokeMethod(EOS(STATIC_3961(i1350)), i1333, i443, java.lang.Object(o2547sub)) → 3968_0_random_InvokeMethod(EOS(STATIC_3968(i1350)), i1333, i443, java.lang.Object(o2547sub))
3968_0_random_InvokeMethod(EOS(STATIC_3968(i1350)), i1333, i443, java.lang.Object(o2547sub)) → 3976_0_length_Load(EOS(STATIC_3976(i1350)), i1333, i443, java.lang.Object(o2547sub), java.lang.Object(o2547sub))
3976_0_length_Load(EOS(STATIC_3976(i1350)), i1333, i443, java.lang.Object(o2547sub), java.lang.Object(o2547sub)) → 3993_0_length_FieldAccess(EOS(STATIC_3993(i1350)), i1333, i443, java.lang.Object(o2547sub), java.lang.Object(o2547sub))
3993_0_length_FieldAccess(EOS(STATIC_3993(i1350)), i1333, i443, java.lang.Object(java.lang.String(o2562sub, i1370)), java.lang.Object(java.lang.String(o2562sub, i1370))) → 4000_0_length_FieldAccess(EOS(STATIC_4000(i1350)), i1333, i443, java.lang.Object(java.lang.String(o2562sub, i1370)), java.lang.Object(java.lang.String(o2562sub, i1370))) | &&(>=(i1370, 0), >=(i1371, 0))
4000_0_length_FieldAccess(EOS(STATIC_4000(i1350)), i1333, i443, java.lang.Object(java.lang.String(o2562sub, i1370)), java.lang.Object(java.lang.String(o2562sub, i1370))) → 4011_0_length_Return(EOS(STATIC_4011(i1350)), i1333, i443, java.lang.Object(java.lang.String(o2562sub, i1370)), i1370)
4011_0_length_Return(EOS(STATIC_4011(i1350)), i1333, i443, java.lang.Object(java.lang.String(o2562sub, i1370)), i1370) → 4019_0_random_Return(EOS(STATIC_4019(i1350)), i1333, i443, i1370)
4019_0_random_Return(EOS(STATIC_4019(i1350)), i1333, i443, i1370) → 4025_0_main_InvokeMethod(EOS(STATIC_4025(i1350)), i1333, i443, i1370)
4025_0_main_InvokeMethod(EOS(STATIC_4025(i1350)), i1333, i443, i1370) → 4035_0_random_FieldAccess(EOS(STATIC_4035(i1350)), i1333, i443, i1370)
4035_0_random_FieldAccess(EOS(STATIC_4035(i1350)), i1333, i443, i1370) → 4053_0_random_FieldAccess(EOS(STATIC_4053(i1350)), i1333, i443, i1370, i1350)
4053_0_random_FieldAccess(EOS(STATIC_4053(i1350)), i1333, i443, i1370, i1350) → 4065_0_random_ArrayLength(EOS(STATIC_4065(i1350)), i1333, i443, i1370, i1350, java.lang.Object(ARRAY(i183)))
4065_0_random_ArrayLength(EOS(STATIC_4065(i1350)), i1333, i443, i1370, i1350, java.lang.Object(ARRAY(i183))) → 4075_0_random_LT(EOS(STATIC_4075(i1350)), i1333, i443, i1370, i1350, i183) | >=(i183, 0)
4075_0_random_LT(EOS(STATIC_4075(i1350)), i1333, i443, i1370, i1350, i183) → 4083_0_random_LT(EOS(STATIC_4083(i1350)), i1333, i443, i1370, i1350, i183)
4075_0_random_LT(EOS(STATIC_4075(i1350)), i1333, i443, i1370, i1350, i183) → 4084_0_random_LT(EOS(STATIC_4084(i1350)), i1333, i443, i1370, i1350, i183)
4083_0_random_LT(EOS(STATIC_4083(i1350)), i1333, i443, i1370, i1350, i183) → 4097_0_random_FieldAccess(EOS(STATIC_4097(i1350)), i1333, i443, i1370) | <(i1350, i183)
4097_0_random_FieldAccess(EOS(STATIC_4097(i1350)), i1333, i443, i1370) → 4109_0_random_FieldAccess(EOS(STATIC_4109(i1350)), i1333, i443, i1370, java.lang.Object(ARRAY(i183)))
4109_0_random_FieldAccess(EOS(STATIC_4109(i1350)), i1333, i443, i1370, java.lang.Object(ARRAY(i183))) → 4121_0_random_ArrayAccess(EOS(STATIC_4121(i1350)), i1333, i443, i1370, java.lang.Object(ARRAY(i183)), i1350)
4121_0_random_ArrayAccess(EOS(STATIC_4121(i1350)), i1333, i443, i1370, java.lang.Object(ARRAY(i183)), i1350) → 4135_0_random_ArrayAccess(EOS(STATIC_4135(i1350)), i1333, i443, i1370, java.lang.Object(ARRAY(i183)), i1350)
4135_0_random_ArrayAccess(EOS(STATIC_4135(i1350)), i1333, i443, i1370, java.lang.Object(ARRAY(i183)), i1350) → 4153_0_random_Store(EOS(STATIC_4153(i1350)), i1333, i443, i1370, o2708)
4153_0_random_Store(EOS(STATIC_4153(i1350)), i1333, i443, i1370, o2708) → 4166_0_random_FieldAccess(EOS(STATIC_4166(i1350)), i1333, i443, i1370, o2708)
4166_0_random_FieldAccess(EOS(STATIC_4166(i1350)), i1333, i443, i1370, o2708) → 4183_0_random_ConstantStackPush(EOS(STATIC_4183(i1350)), i1333, i443, i1370, o2708, i1350)
4183_0_random_ConstantStackPush(EOS(STATIC_4183(i1350)), i1333, i443, i1370, o2708, i1350) → 4198_0_random_IntArithmetic(EOS(STATIC_4198(i1350)), i1333, i443, i1370, o2708, i1350, 1)
4198_0_random_IntArithmetic(EOS(STATIC_4198(i1350)), i1333, i443, i1370, o2708, i1350, matching1) → 4210_0_random_FieldAccess(EOS(STATIC_4210(i1350)), i1333, i443, i1370, o2708, +(i1350, 1)) | &&(>(i1350, 0), =(matching1, 1))
4210_0_random_FieldAccess(EOS(STATIC_4210(i1350)), i1333, i443, i1370, o2708, i1456) → 4220_0_random_Load(EOS(STATIC_4220(i1456)), i1333, i443, i1370, o2708)
4220_0_random_Load(EOS(STATIC_4220(i1456)), i1333, i443, i1370, o2708) → 4232_0_random_InvokeMethod(EOS(STATIC_4232(i1456)), i1333, i443, i1370, o2708)
4232_0_random_InvokeMethod(EOS(STATIC_4232(i1456)), i1333, i443, i1370, java.lang.Object(o2862sub)) → 4244_0_random_InvokeMethod(EOS(STATIC_4244(i1456)), i1333, i443, i1370, java.lang.Object(o2862sub))
4244_0_random_InvokeMethod(EOS(STATIC_4244(i1456)), i1333, i443, i1370, java.lang.Object(o2862sub)) → 4254_0_length_Load(EOS(STATIC_4254(i1456)), i1333, i443, i1370, java.lang.Object(o2862sub), java.lang.Object(o2862sub))
4254_0_length_Load(EOS(STATIC_4254(i1456)), i1333, i443, i1370, java.lang.Object(o2862sub), java.lang.Object(o2862sub)) → 4278_0_length_FieldAccess(EOS(STATIC_4278(i1456)), i1333, i443, i1370, java.lang.Object(o2862sub), java.lang.Object(o2862sub))
4278_0_length_FieldAccess(EOS(STATIC_4278(i1456)), i1333, i443, i1370, java.lang.Object(java.lang.String(o2951sub, i1514)), java.lang.Object(java.lang.String(o2951sub, i1514))) → 4291_0_length_FieldAccess(EOS(STATIC_4291(i1456)), i1333, i443, i1370, java.lang.Object(java.lang.String(o2951sub, i1514)), java.lang.Object(java.lang.String(o2951sub, i1514))) | &&(>=(i1514, 0), >=(i1515, 0))
4291_0_length_FieldAccess(EOS(STATIC_4291(i1456)), i1333, i443, i1370, java.lang.Object(java.lang.String(o2951sub, i1514)), java.lang.Object(java.lang.String(o2951sub, i1514))) → 4301_0_length_Return(EOS(STATIC_4301(i1456)), i1333, i443, i1370, java.lang.Object(java.lang.String(o2951sub, i1514)), i1514)
4301_0_length_Return(EOS(STATIC_4301(i1456)), i1333, i443, i1370, java.lang.Object(java.lang.String(o2951sub, i1514)), i1514) → 4308_0_random_Return(EOS(STATIC_4308(i1456)), i1333, i443, i1370, i1514)
4308_0_random_Return(EOS(STATIC_4308(i1456)), i1333, i443, i1370, i1514) → 4312_0_main_IntArithmetic(EOS(STATIC_4312(i1456)), i1333, i443, i1370, i1514)
4312_0_main_IntArithmetic(EOS(STATIC_4312(i1456)), i1333, i443, i1370, i1514) → 4320_0_main_ConstantStackPush(EOS(STATIC_4320(i1456)), i1333, i443, *(i1370, i1514))
4320_0_main_ConstantStackPush(EOS(STATIC_4320(i1456)), i1333, i443, i1528) → 4328_0_main_LE(EOS(STATIC_4328(i1456)), i1333, i443, i1528, 9)
4328_0_main_LE(EOS(STATIC_4328(i1456)), i1333, i443, i1541, matching1) → 4333_0_main_LE(EOS(STATIC_4333(i1456)), i1333, i443, i1541, 9) | =(matching1, 9)
4328_0_main_LE(EOS(STATIC_4328(i1456)), i1333, i443, i1542, matching1) → 4334_0_main_LE(EOS(STATIC_4334(i1456)), i1333, i443, i1542, 9) | =(matching1, 9)
4333_0_main_LE(EOS(STATIC_4333(i1456)), i1333, i443, i1541, matching1) → 4341_0_main_Inc(EOS(STATIC_4341(i1456)), i1333, i443) | &&(<=(i1541, 9), =(matching1, 9))
4341_0_main_Inc(EOS(STATIC_4341(i1456)), i1333, i443) → 4348_0_main_JMP(EOS(STATIC_4348(i1456)), i1333, +(i443, -1))
4348_0_main_JMP(EOS(STATIC_4348(i1456)), i1333, i1547) → 4354_0_main_Load(EOS(STATIC_4354(i1456)), i1333, i1547)
4354_0_main_Load(EOS(STATIC_4354(i1456)), i1333, i1547) → 3893_0_main_Load(EOS(STATIC_3893(i1456)), i1333, i1547)
3893_0_main_Load(EOS(STATIC_3893(i1332)), i1333, i443) → 3897_0_main_Load(EOS(STATIC_3897(i1332)), i1333, i443, i1333)
4334_0_main_LE(EOS(STATIC_4334(i1456)), i1333, i443, i1542, matching1) → 4342_0_main_Inc(EOS(STATIC_4342(i1456)), i1333, i443) | &&(>(i1542, 9), =(matching1, 9))
4342_0_main_Inc(EOS(STATIC_4342(i1456)), i1333, i443) → 4350_0_main_JMP(EOS(STATIC_4350(i1456)), +(i1333, -1), i443)
4350_0_main_JMP(EOS(STATIC_4350(i1456)), i1548, i443) → 4356_0_main_Load(EOS(STATIC_4356(i1456)), i1548, i443)
4356_0_main_Load(EOS(STATIC_4356(i1456)), i1548, i443) → 3893_0_main_Load(EOS(STATIC_3893(i1456)), i1548, i443)
4084_0_random_LT(EOS(STATIC_4084(i1350)), i1333, i443, i1370, i1350, i183) → 4098_0_random_ConstantStackPush(EOS(STATIC_4098(i1350)), i1333, i443, i1370) | >=(i1350, i183)
4098_0_random_ConstantStackPush(EOS(STATIC_4098(i1350)), i1333, i443, i1370) → 4110_0_random_Return(EOS(STATIC_4110(i1350)), i1333, i443, i1370)
4110_0_random_Return(EOS(STATIC_4110(i1350)), i1333, i443, i1370) → 4122_0_main_IntArithmetic(EOS(STATIC_4122(i1350)), i1333, i443, i1370)
4122_0_main_IntArithmetic(EOS(STATIC_4122(i1350)), i1333, i443, i1370) → 4138_0_main_ConstantStackPush(EOS(STATIC_4138(i1350)), i1333, i443)
4138_0_main_ConstantStackPush(EOS(STATIC_4138(i1350)), i1333, i443) → 4146_0_main_ConstantStackPush(EOS(STATIC_4146(i1350)), i1333, i443)
4146_0_main_ConstantStackPush(EOS(STATIC_4146(i1377)), i1333, i443) → 4161_0_main_LE(EOS(STATIC_4161(i1377)), i1333, i443)
4161_0_main_LE(EOS(STATIC_4161(i1377)), i1333, i443) → 4176_0_main_Inc(EOS(STATIC_4176(i1377)), i1333, i443)
4176_0_main_Inc(EOS(STATIC_4176(i1377)), i1333, i443) → 4192_0_main_JMP(EOS(STATIC_4192(i1377)), i1333, +(i443, -1))
4192_0_main_JMP(EOS(STATIC_4192(i1377)), i1333, i1448) → 4206_0_main_Load(EOS(STATIC_4206(i1377)), i1333, i1448)
4206_0_main_Load(EOS(STATIC_4206(i1377)), i1333, i1448) → 3893_0_main_Load(EOS(STATIC_3893(i1377)), i1333, i1448)
3914_0_random_LT(EOS(STATIC_3914(i1332)), i1333, i443, i1332, i183) → 3916_0_random_ConstantStackPush(EOS(STATIC_3916(i1332)), i1333, i443) | >=(i1332, i183)
3916_0_random_ConstantStackPush(EOS(STATIC_3916(i1332)), i1333, i443) → 3918_0_random_Return(EOS(STATIC_3918(i1332)), i1333, i443)
3918_0_random_Return(EOS(STATIC_3918(i1332)), i1333, i443) → 3921_0_main_InvokeMethod(EOS(STATIC_3921(i1332)), i1333, i443)
3921_0_main_InvokeMethod(EOS(STATIC_3921(i1332)), i1333, i443) → 3925_0_random_FieldAccess(EOS(STATIC_3925(i1332)), i1333, i443)
3925_0_random_FieldAccess(EOS(STATIC_3925(i1332)), i1333, i443) → 3933_0_random_FieldAccess(EOS(STATIC_3933(i1332)), i1333, i443, i1332)
3933_0_random_FieldAccess(EOS(STATIC_3933(i1332)), i1333, i443, i1332) → 3937_0_random_ArrayLength(EOS(STATIC_3937(i1332)), i1333, i443, i1332, java.lang.Object(ARRAY(i183)))
3937_0_random_ArrayLength(EOS(STATIC_3937(i1332)), i1333, i443, i1332, java.lang.Object(ARRAY(i183))) → 3943_0_random_LT(EOS(STATIC_3943(i1332)), i1333, i443, i1332, i183) | >=(i183, 0)
3943_0_random_LT(EOS(STATIC_3943(i1332)), i1333, i443, i1332, i183) → 3946_0_random_LT(EOS(STATIC_3946(i1332)), i1333, i443, i1332, i183)
3943_0_random_LT(EOS(STATIC_3943(i1332)), i1333, i443, i1332, i183) → 3947_0_random_LT(EOS(STATIC_3947(i1332)), i1333, i443, i1332, i183)
3946_0_random_LT(EOS(STATIC_3946(i1332)), i1333, i443, i1332, i183) → 3951_0_random_FieldAccess(EOS(STATIC_3951(i1332)), i1333, i443) | <(i1332, i183)
3951_0_random_FieldAccess(EOS(STATIC_3951(i1332)), i1333, i443) → 3958_0_random_FieldAccess(EOS(STATIC_3958(i1332)), i1333, i443, java.lang.Object(ARRAY(i183)))
3958_0_random_FieldAccess(EOS(STATIC_3958(i1332)), i1333, i443, java.lang.Object(ARRAY(i183))) → 3964_0_random_ArrayAccess(EOS(STATIC_3964(i1332)), i1333, i443, java.lang.Object(ARRAY(i183)), i1332)
3964_0_random_ArrayAccess(EOS(STATIC_3964(i1355)), i1333, i443, java.lang.Object(ARRAY(i183)), i1355) → 3972_0_random_ArrayAccess(EOS(STATIC_3972(i1355)), i1333, i443, java.lang.Object(ARRAY(i183)), i1355)
3972_0_random_ArrayAccess(EOS(STATIC_3972(i1355)), i1333, i443, java.lang.Object(ARRAY(i183)), i1355) → 3981_0_random_ArrayAccess(EOS(STATIC_3981(i1355)), i1333, i443, java.lang.Object(ARRAY(i183)), i1355)
3981_0_random_ArrayAccess(EOS(STATIC_3981(i1355)), i1333, i443, java.lang.Object(ARRAY(i183)), i1355) → 3988_0_random_Store(EOS(STATIC_3988(i1355)), i1333, i443, o2552)
3988_0_random_Store(EOS(STATIC_3988(i1355)), i1333, i443, o2552) → 3996_0_random_FieldAccess(EOS(STATIC_3996(i1355)), i1333, i443, o2552)
3996_0_random_FieldAccess(EOS(STATIC_3996(i1355)), i1333, i443, o2552) → 4006_0_random_ConstantStackPush(EOS(STATIC_4006(i1355)), i1333, i443, o2552, i1355)
4006_0_random_ConstantStackPush(EOS(STATIC_4006(i1355)), i1333, i443, o2552, i1355) → 4015_0_random_IntArithmetic(EOS(STATIC_4015(i1355)), i1333, i443, o2552, i1355, 1)
4015_0_random_IntArithmetic(EOS(STATIC_4015(i1355)), i1333, i443, o2552, i1355, matching1) → 4022_0_random_FieldAccess(EOS(STATIC_4022(i1355)), i1333, i443, o2552, +(i1355, 1)) | &&(>=(i1355, 0), =(matching1, 1))
4022_0_random_FieldAccess(EOS(STATIC_4022(i1355)), i1333, i443, o2552, i1377) → 4031_0_random_Load(EOS(STATIC_4031(i1377)), i1333, i443, o2552)
4031_0_random_Load(EOS(STATIC_4031(i1377)), i1333, i443, o2552) → 4040_0_random_InvokeMethod(EOS(STATIC_4040(i1377)), i1333, i443, o2552)
4040_0_random_InvokeMethod(EOS(STATIC_4040(i1377)), i1333, i443, java.lang.Object(o2603sub)) → 4048_0_random_InvokeMethod(EOS(STATIC_4048(i1377)), i1333, i443, java.lang.Object(o2603sub))
4048_0_random_InvokeMethod(EOS(STATIC_4048(i1377)), i1333, i443, java.lang.Object(o2603sub)) → 4059_0_length_Load(EOS(STATIC_4059(i1377)), i1333, i443, java.lang.Object(o2603sub), java.lang.Object(o2603sub))
4059_0_length_Load(EOS(STATIC_4059(i1377)), i1333, i443, java.lang.Object(o2603sub), java.lang.Object(o2603sub)) → 4081_0_length_FieldAccess(EOS(STATIC_4081(i1377)), i1333, i443, java.lang.Object(o2603sub), java.lang.Object(o2603sub))
4081_0_length_FieldAccess(EOS(STATIC_4081(i1377)), i1333, i443, java.lang.Object(java.lang.String(o2636sub, i1404)), java.lang.Object(java.lang.String(o2636sub, i1404))) → 4090_0_length_FieldAccess(EOS(STATIC_4090(i1377)), i1333, i443, java.lang.Object(java.lang.String(o2636sub, i1404)), java.lang.Object(java.lang.String(o2636sub, i1404))) | &&(>=(i1404, 0), >=(i1405, 0))
4090_0_length_FieldAccess(EOS(STATIC_4090(i1377)), i1333, i443, java.lang.Object(java.lang.String(o2636sub, i1404)), java.lang.Object(java.lang.String(o2636sub, i1404))) → 4103_0_length_Return(EOS(STATIC_4103(i1377)), i1333, i443, java.lang.Object(java.lang.String(o2636sub, i1404)))
4103_0_length_Return(EOS(STATIC_4103(i1377)), i1333, i443, java.lang.Object(java.lang.String(o2636sub, i1404))) → 4117_0_random_Return(EOS(STATIC_4117(i1377)), i1333, i443)
4117_0_random_Return(EOS(STATIC_4117(i1377)), i1333, i443) → 4129_0_main_IntArithmetic(EOS(STATIC_4129(i1377)), i1333, i443)
4129_0_main_IntArithmetic(EOS(STATIC_4129(i1377)), i1333, i443) → 4146_0_main_ConstantStackPush(EOS(STATIC_4146(i1377)), i1333, i443)
3947_0_random_LT(EOS(STATIC_3947(i1332)), i1333, i443, i1332, i183) → 3953_0_random_ConstantStackPush(EOS(STATIC_3953(i1332)), i1333, i443) | >=(i1332, i183)
3953_0_random_ConstantStackPush(EOS(STATIC_3953(i1332)), i1333, i443) → 3960_0_random_Return(EOS(STATIC_3960(i1332)), i1333, i443)
3960_0_random_Return(EOS(STATIC_3960(i1332)), i1333, i443) → 3966_0_main_IntArithmetic(EOS(STATIC_3966(i1332)), i1333, i443)
3966_0_main_IntArithmetic(EOS(STATIC_3966(i1332)), i1333, i443) → 3973_0_main_ConstantStackPush(EOS(STATIC_3973(i1332)), i1333, i443)
3973_0_main_ConstantStackPush(EOS(STATIC_3973(i1332)), i1333, i443) → 3983_0_main_LE(EOS(STATIC_3983(i1332)), i1333, i443)
3983_0_main_LE(EOS(STATIC_3983(i1332)), i1333, i443) → 3990_0_main_Inc(EOS(STATIC_3990(i1332)), i1333, i443)
3990_0_main_Inc(EOS(STATIC_3990(i1332)), i1333, i443) → 3998_0_main_JMP(EOS(STATIC_3998(i1332)), i1333, +(i443, -1))
3998_0_main_JMP(EOS(STATIC_3998(i1332)), i1333, i1366) → 4009_0_main_Load(EOS(STATIC_4009(i1332)), i1333, i1366)
4009_0_main_Load(EOS(STATIC_4009(i1332)), i1333, i1366) → 3893_0_main_Load(EOS(STATIC_3893(i1332)), i1333, i1366)
R rules:

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

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

Filtered duplicate args:

3897_0_main_Load(x1, x2, x3, x4) → 3897_0_main_Load(x1, x3, x4)
Cond_3897_0_main_Load(x1, x2, x3, x4, x5) → Cond_3897_0_main_Load(x1, x2, x4, x5)
Cond_3897_0_main_Load1(x1, x2, x3, x4, x5) → Cond_3897_0_main_Load1(x1, x2, x4, x5)
Cond_3897_0_main_Load2(x1, x2, x3, x4, x5) → Cond_3897_0_main_Load2(x1, x2, x4, x5)
Cond_3897_0_main_Load3(x1, x2, x3, x4, x5) → Cond_3897_0_main_Load3(x1, x2, x4, x5)

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

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

Performed bisimulation on rules. Used the following equivalence classes: {[Cond_3897_0_main_Load_4, Cond_3897_0_main_Load1_4, Cond_3897_0_main_Load2_4]=Cond_3897_0_main_Load_4}

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

P rules:
3897_0_MAIN_LOAD(EOS(STATIC_3897(x0)), x2, x1) → COND_3897_0_MAIN_LOAD(&&(>(x0, -1), <(0, +(x1, x2))), EOS(STATIC_3897(x0)), x2, x1)
COND_3897_0_MAIN_LOAD(TRUE, EOS(STATIC_3897(x0)), x2, x1) → 3897_0_MAIN_LOAD(EOS(STATIC_3897(+(x0, 2))), +(x2, -1), x1)
COND_3897_0_MAIN_LOAD(TRUE, EOS(STATIC_3897(x0)), x2, x1) → 3897_0_MAIN_LOAD(EOS(STATIC_3897(+(x0, 2))), x2, +(x1, -1))
COND_3897_0_MAIN_LOAD(TRUE, EOS(STATIC_3897(x0)), x2, x1) → 3897_0_MAIN_LOAD(EOS(STATIC_3897(+(x0, 1))), +(x2, -1), x1)
3897_0_MAIN_LOAD(EOS(STATIC_3897(x0)), x2, x1) → COND_3897_0_MAIN_LOAD3(<(0, +(x1, x2)), EOS(STATIC_3897(x0)), x2, x1)
COND_3897_0_MAIN_LOAD3(TRUE, EOS(STATIC_3897(x0)), x2, x1) → 3897_0_MAIN_LOAD(EOS(STATIC_3897(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): 3897_0_MAIN_LOAD(EOS(STATIC_3897(x0[0])), x2[0], x1[0]) → COND_3897_0_MAIN_LOAD(x0[0] > -1 && 0 < x1[0] + x2[0], EOS(STATIC_3897(x0[0])), x2[0], x1[0])
(1): COND_3897_0_MAIN_LOAD(TRUE, EOS(STATIC_3897(x0[1])), x2[1], x1[1]) → 3897_0_MAIN_LOAD(EOS(STATIC_3897(x0[1] + 2)), x2[1] + -1, x1[1])
(2): COND_3897_0_MAIN_LOAD(TRUE, EOS(STATIC_3897(x0[2])), x2[2], x1[2]) → 3897_0_MAIN_LOAD(EOS(STATIC_3897(x0[2] + 2)), x2[2], x1[2] + -1)
(3): COND_3897_0_MAIN_LOAD(TRUE, EOS(STATIC_3897(x0[3])), x2[3], x1[3]) → 3897_0_MAIN_LOAD(EOS(STATIC_3897(x0[3] + 1)), x2[3] + -1, x1[3])
(4): 3897_0_MAIN_LOAD(EOS(STATIC_3897(x0[4])), x2[4], x1[4]) → COND_3897_0_MAIN_LOAD3(0 < x1[4] + x2[4], EOS(STATIC_3897(x0[4])), x2[4], x1[4])
(5): COND_3897_0_MAIN_LOAD3(TRUE, EOS(STATIC_3897(x0[5])), x2[5], x1[5]) → 3897_0_MAIN_LOAD(EOS(STATIC_3897(x0[5])), x2[5] + -1, x1[5])

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

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

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

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

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

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

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

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

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

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

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

(5) -> (4), if (EOS(STATIC_3897(x0[5])) →^* EOS(STATIC_3897(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@2b68c70e 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 3897_0_MAIN_LOAD(EOS(STATIC_3897(x0)), x2, x1) → COND_3897_0_MAIN_LOAD(&&(>(x0, -1), <(0, +(x1, x2))), EOS(STATIC_3897(x0)), x2, x1) the following chains were created:

We consider the chain 3897_0_MAIN_LOAD(EOS(STATIC_3897(x0[0])), x2[0], x1[0]) → COND_3897_0_MAIN_LOAD(&&(>(x0[0], -1), <(0, +(x1[0], x2[0]))), EOS(STATIC_3897(x0[0])), x2[0], x1[0]), COND_3897_0_MAIN_LOAD(TRUE, EOS(STATIC_3897(x0[1])), x2[1], x1[1]) → 3897_0_MAIN_LOAD(EOS(STATIC_3897(+(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_3897(x0[0]))=EOS(STATIC_3897(x0[1]))∧x2[0]=x2[1]∧x1[0]=x1[1] ⇒ 3897_0_MAIN_LOAD(EOS(STATIC_3897(x0[0])), x2[0], x1[0])≥NonInfC∧3897_0_MAIN_LOAD(EOS(STATIC_3897(x0[0])), x2[0], x1[0])≥COND_3897_0_MAIN_LOAD(&&(>(x0[0], -1), <(0, +(x1[0], x2[0]))), EOS(STATIC_3897(x0[0])), x2[0], x1[0])∧(U^Increasing(COND_3897_0_MAIN_LOAD(&&(>(x0[0], -1), <(0, +(x1[0], x2[0]))), EOS(STATIC_3897(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 ⇒ 3897_0_MAIN_LOAD(EOS(STATIC_3897(x0[0])), x2[0], x1[0])≥NonInfC∧3897_0_MAIN_LOAD(EOS(STATIC_3897(x0[0])), x2[0], x1[0])≥COND_3897_0_MAIN_LOAD(&&(>(x0[0], -1), <(0, +(x1[0], x2[0]))), EOS(STATIC_3897(x0[0])), x2[0], x1[0])∧(U^Increasing(COND_3897_0_MAIN_LOAD(&&(>(x0[0], -1), <(0, +(x1[0], x2[0]))), EOS(STATIC_3897(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_3897_0_MAIN_LOAD(&&(>(x0[0], -1), <(0, +(x1[0], x2[0]))), EOS(STATIC_3897(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_3897_0_MAIN_LOAD(&&(>(x0[0], -1), <(0, +(x1[0], x2[0]))), EOS(STATIC_3897(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_3897_0_MAIN_LOAD(&&(>(x0[0], -1), <(0, +(x1[0], x2[0]))), EOS(STATIC_3897(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_3897_0_MAIN_LOAD(&&(>(x0[0], -1), <(0, +(x1[0], x2[0]))), EOS(STATIC_3897(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_3897_0_MAIN_LOAD(&&(>(x0[0], -1), <(0, +(x1[0], x2[0]))), EOS(STATIC_3897(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_3897_0_MAIN_LOAD(&&(>(x0[0], -1), <(0, +(x1[0], x2[0]))), EOS(STATIC_3897(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 3897_0_MAIN_LOAD(EOS(STATIC_3897(x0[0])), x2[0], x1[0]) → COND_3897_0_MAIN_LOAD(&&(>(x0[0], -1), <(0, +(x1[0], x2[0]))), EOS(STATIC_3897(x0[0])), x2[0], x1[0]), COND_3897_0_MAIN_LOAD(TRUE, EOS(STATIC_3897(x0[2])), x2[2], x1[2]) → 3897_0_MAIN_LOAD(EOS(STATIC_3897(+(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_3897(x0[0]))=EOS(STATIC_3897(x0[2]))∧x2[0]=x2[2]∧x1[0]=x1[2] ⇒ 3897_0_MAIN_LOAD(EOS(STATIC_3897(x0[0])), x2[0], x1[0])≥NonInfC∧3897_0_MAIN_LOAD(EOS(STATIC_3897(x0[0])), x2[0], x1[0])≥COND_3897_0_MAIN_LOAD(&&(>(x0[0], -1), <(0, +(x1[0], x2[0]))), EOS(STATIC_3897(x0[0])), x2[0], x1[0])∧(U^Increasing(COND_3897_0_MAIN_LOAD(&&(>(x0[0], -1), <(0, +(x1[0], x2[0]))), EOS(STATIC_3897(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 ⇒ 3897_0_MAIN_LOAD(EOS(STATIC_3897(x0[0])), x2[0], x1[0])≥NonInfC∧3897_0_MAIN_LOAD(EOS(STATIC_3897(x0[0])), x2[0], x1[0])≥COND_3897_0_MAIN_LOAD(&&(>(x0[0], -1), <(0, +(x1[0], x2[0]))), EOS(STATIC_3897(x0[0])), x2[0], x1[0])∧(U^Increasing(COND_3897_0_MAIN_LOAD(&&(>(x0[0], -1), <(0, +(x1[0], x2[0]))), EOS(STATIC_3897(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_3897_0_MAIN_LOAD(&&(>(x0[0], -1), <(0, +(x1[0], x2[0]))), EOS(STATIC_3897(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_3897_0_MAIN_LOAD(&&(>(x0[0], -1), <(0, +(x1[0], x2[0]))), EOS(STATIC_3897(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_3897_0_MAIN_LOAD(&&(>(x0[0], -1), <(0, +(x1[0], x2[0]))), EOS(STATIC_3897(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_3897_0_MAIN_LOAD(&&(>(x0[0], -1), <(0, +(x1[0], x2[0]))), EOS(STATIC_3897(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_3897_0_MAIN_LOAD(&&(>(x0[0], -1), <(0, +(x1[0], x2[0]))), EOS(STATIC_3897(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_3897_0_MAIN_LOAD(&&(>(x0[0], -1), <(0, +(x1[0], x2[0]))), EOS(STATIC_3897(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 3897_0_MAIN_LOAD(EOS(STATIC_3897(x0[0])), x2[0], x1[0]) → COND_3897_0_MAIN_LOAD(&&(>(x0[0], -1), <(0, +(x1[0], x2[0]))), EOS(STATIC_3897(x0[0])), x2[0], x1[0]), COND_3897_0_MAIN_LOAD(TRUE, EOS(STATIC_3897(x0[3])), x2[3], x1[3]) → 3897_0_MAIN_LOAD(EOS(STATIC_3897(+(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_3897(x0[0]))=EOS(STATIC_3897(x0[3]))∧x2[0]=x2[3]∧x1[0]=x1[3] ⇒ 3897_0_MAIN_LOAD(EOS(STATIC_3897(x0[0])), x2[0], x1[0])≥NonInfC∧3897_0_MAIN_LOAD(EOS(STATIC_3897(x0[0])), x2[0], x1[0])≥COND_3897_0_MAIN_LOAD(&&(>(x0[0], -1), <(0, +(x1[0], x2[0]))), EOS(STATIC_3897(x0[0])), x2[0], x1[0])∧(U^Increasing(COND_3897_0_MAIN_LOAD(&&(>(x0[0], -1), <(0, +(x1[0], x2[0]))), EOS(STATIC_3897(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 ⇒ 3897_0_MAIN_LOAD(EOS(STATIC_3897(x0[0])), x2[0], x1[0])≥NonInfC∧3897_0_MAIN_LOAD(EOS(STATIC_3897(x0[0])), x2[0], x1[0])≥COND_3897_0_MAIN_LOAD(&&(>(x0[0], -1), <(0, +(x1[0], x2[0]))), EOS(STATIC_3897(x0[0])), x2[0], x1[0])∧(U^Increasing(COND_3897_0_MAIN_LOAD(&&(>(x0[0], -1), <(0, +(x1[0], x2[0]))), EOS(STATIC_3897(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_3897_0_MAIN_LOAD(&&(>(x0[0], -1), <(0, +(x1[0], x2[0]))), EOS(STATIC_3897(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_3897_0_MAIN_LOAD(&&(>(x0[0], -1), <(0, +(x1[0], x2[0]))), EOS(STATIC_3897(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_3897_0_MAIN_LOAD(&&(>(x0[0], -1), <(0, +(x1[0], x2[0]))), EOS(STATIC_3897(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_3897_0_MAIN_LOAD(&&(>(x0[0], -1), <(0, +(x1[0], x2[0]))), EOS(STATIC_3897(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_3897_0_MAIN_LOAD(&&(>(x0[0], -1), <(0, +(x1[0], x2[0]))), EOS(STATIC_3897(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_3897_0_MAIN_LOAD(&&(>(x0[0], -1), <(0, +(x1[0], x2[0]))), EOS(STATIC_3897(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_3897_0_MAIN_LOAD(TRUE, EOS(STATIC_3897(x0)), x2, x1) → 3897_0_MAIN_LOAD(EOS(STATIC_3897(+(x0, 2))), +(x2, -1), x1) the following chains were created:

We consider the chain COND_3897_0_MAIN_LOAD(TRUE, EOS(STATIC_3897(x0[1])), x2[1], x1[1]) → 3897_0_MAIN_LOAD(EOS(STATIC_3897(+(x0[1], 2))), +(x2[1], -1), x1[1]) which results in the following constraint:
(25)    (COND_3897_0_MAIN_LOAD(TRUE, EOS(STATIC_3897(x0[1])), x2[1], x1[1])≥NonInfC∧COND_3897_0_MAIN_LOAD(TRUE, EOS(STATIC_3897(x0[1])), x2[1], x1[1])≥3897_0_MAIN_LOAD(EOS(STATIC_3897(+(x0[1], 2))), +(x2[1], -1), x1[1])∧(U^Increasing(3897_0_MAIN_LOAD(EOS(STATIC_3897(+(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(3897_0_MAIN_LOAD(EOS(STATIC_3897(+(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(3897_0_MAIN_LOAD(EOS(STATIC_3897(+(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(3897_0_MAIN_LOAD(EOS(STATIC_3897(+(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(3897_0_MAIN_LOAD(EOS(STATIC_3897(+(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_3897_0_MAIN_LOAD(TRUE, EOS(STATIC_3897(x0)), x2, x1) → 3897_0_MAIN_LOAD(EOS(STATIC_3897(+(x0, 2))), x2, +(x1, -1)) the following chains were created:

We consider the chain COND_3897_0_MAIN_LOAD(TRUE, EOS(STATIC_3897(x0[2])), x2[2], x1[2]) → 3897_0_MAIN_LOAD(EOS(STATIC_3897(+(x0[2], 2))), x2[2], +(x1[2], -1)) which results in the following constraint:
(30)    (COND_3897_0_MAIN_LOAD(TRUE, EOS(STATIC_3897(x0[2])), x2[2], x1[2])≥NonInfC∧COND_3897_0_MAIN_LOAD(TRUE, EOS(STATIC_3897(x0[2])), x2[2], x1[2])≥3897_0_MAIN_LOAD(EOS(STATIC_3897(+(x0[2], 2))), x2[2], +(x1[2], -1))∧(U^Increasing(3897_0_MAIN_LOAD(EOS(STATIC_3897(+(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(3897_0_MAIN_LOAD(EOS(STATIC_3897(+(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(3897_0_MAIN_LOAD(EOS(STATIC_3897(+(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(3897_0_MAIN_LOAD(EOS(STATIC_3897(+(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(3897_0_MAIN_LOAD(EOS(STATIC_3897(+(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_3897_0_MAIN_LOAD(TRUE, EOS(STATIC_3897(x0)), x2, x1) → 3897_0_MAIN_LOAD(EOS(STATIC_3897(+(x0, 1))), +(x2, -1), x1) the following chains were created:

We consider the chain COND_3897_0_MAIN_LOAD(TRUE, EOS(STATIC_3897(x0[3])), x2[3], x1[3]) → 3897_0_MAIN_LOAD(EOS(STATIC_3897(+(x0[3], 1))), +(x2[3], -1), x1[3]) which results in the following constraint:
(35)    (COND_3897_0_MAIN_LOAD(TRUE, EOS(STATIC_3897(x0[3])), x2[3], x1[3])≥NonInfC∧COND_3897_0_MAIN_LOAD(TRUE, EOS(STATIC_3897(x0[3])), x2[3], x1[3])≥3897_0_MAIN_LOAD(EOS(STATIC_3897(+(x0[3], 1))), +(x2[3], -1), x1[3])∧(U^Increasing(3897_0_MAIN_LOAD(EOS(STATIC_3897(+(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(3897_0_MAIN_LOAD(EOS(STATIC_3897(+(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(3897_0_MAIN_LOAD(EOS(STATIC_3897(+(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(3897_0_MAIN_LOAD(EOS(STATIC_3897(+(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(3897_0_MAIN_LOAD(EOS(STATIC_3897(+(x0[3], 1))), +(x2[3], -1), x1[3])), ≥)∧[bni_18] = 0∧0 = 0∧0 = 0∧0 = 0∧[1 + (-1)bso_19] ≥ 0)

For Pair 3897_0_MAIN_LOAD(EOS(STATIC_3897(x0)), x2, x1) → COND_3897_0_MAIN_LOAD3(<(0, +(x1, x2)), EOS(STATIC_3897(x0)), x2, x1) the following chains were created:

We consider the chain 3897_0_MAIN_LOAD(EOS(STATIC_3897(x0[4])), x2[4], x1[4]) → COND_3897_0_MAIN_LOAD3(<(0, +(x1[4], x2[4])), EOS(STATIC_3897(x0[4])), x2[4], x1[4]), COND_3897_0_MAIN_LOAD3(TRUE, EOS(STATIC_3897(x0[5])), x2[5], x1[5]) → 3897_0_MAIN_LOAD(EOS(STATIC_3897(x0[5])), +(x2[5], -1), x1[5]) which results in the following constraint:
(40)    (<(0, +(x1[4], x2[4]))=TRUE∧EOS(STATIC_3897(x0[4]))=EOS(STATIC_3897(x0[5]))∧x2[4]=x2[5]∧x1[4]=x1[5] ⇒ 3897_0_MAIN_LOAD(EOS(STATIC_3897(x0[4])), x2[4], x1[4])≥NonInfC∧3897_0_MAIN_LOAD(EOS(STATIC_3897(x0[4])), x2[4], x1[4])≥COND_3897_0_MAIN_LOAD3(<(0, +(x1[4], x2[4])), EOS(STATIC_3897(x0[4])), x2[4], x1[4])∧(U^Increasing(COND_3897_0_MAIN_LOAD3(<(0, +(x1[4], x2[4])), EOS(STATIC_3897(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 ⇒ 3897_0_MAIN_LOAD(EOS(STATIC_3897(x0[4])), x2[4], x1[4])≥NonInfC∧3897_0_MAIN_LOAD(EOS(STATIC_3897(x0[4])), x2[4], x1[4])≥COND_3897_0_MAIN_LOAD3(<(0, +(x1[4], x2[4])), EOS(STATIC_3897(x0[4])), x2[4], x1[4])∧(U^Increasing(COND_3897_0_MAIN_LOAD3(<(0, +(x1[4], x2[4])), EOS(STATIC_3897(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_3897_0_MAIN_LOAD3(<(0, +(x1[4], x2[4])), EOS(STATIC_3897(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_3897_0_MAIN_LOAD3(<(0, +(x1[4], x2[4])), EOS(STATIC_3897(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_3897_0_MAIN_LOAD3(<(0, +(x1[4], x2[4])), EOS(STATIC_3897(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_3897_0_MAIN_LOAD3(<(0, +(x1[4], x2[4])), EOS(STATIC_3897(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_3897_0_MAIN_LOAD3(<(0, +(x1[4], x2[4])), EOS(STATIC_3897(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_3897_0_MAIN_LOAD3(<(0, +(x1[4], x2[4])), EOS(STATIC_3897(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_3897_0_MAIN_LOAD3(<(0, +(x1[4], x2[4])), EOS(STATIC_3897(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_3897_0_MAIN_LOAD3(TRUE, EOS(STATIC_3897(x0)), x2, x1) → 3897_0_MAIN_LOAD(EOS(STATIC_3897(x0)), +(x2, -1), x1) the following chains were created:

We consider the chain COND_3897_0_MAIN_LOAD3(TRUE, EOS(STATIC_3897(x0[5])), x2[5], x1[5]) → 3897_0_MAIN_LOAD(EOS(STATIC_3897(x0[5])), +(x2[5], -1), x1[5]) which results in the following constraint:
(49)    (COND_3897_0_MAIN_LOAD3(TRUE, EOS(STATIC_3897(x0[5])), x2[5], x1[5])≥NonInfC∧COND_3897_0_MAIN_LOAD3(TRUE, EOS(STATIC_3897(x0[5])), x2[5], x1[5])≥3897_0_MAIN_LOAD(EOS(STATIC_3897(x0[5])), +(x2[5], -1), x1[5])∧(U^Increasing(3897_0_MAIN_LOAD(EOS(STATIC_3897(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(3897_0_MAIN_LOAD(EOS(STATIC_3897(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(3897_0_MAIN_LOAD(EOS(STATIC_3897(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(3897_0_MAIN_LOAD(EOS(STATIC_3897(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(3897_0_MAIN_LOAD(EOS(STATIC_3897(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.

3897_0_MAIN_LOAD(EOS(STATIC_3897(x0)), x2, x1) → COND_3897_0_MAIN_LOAD(&&(>(x0, -1), <(0, +(x1, x2))), EOS(STATIC_3897(x0)), x2, x1)
- (x0[0] ≥ 0∧x1[0] ≥ 0∧x2[0] ≥ 0 ⇒ (U^Increasing(COND_3897_0_MAIN_LOAD(&&(>(x0[0], -1), <(0, +(x1[0], x2[0]))), EOS(STATIC_3897(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_3897_0_MAIN_LOAD(&&(>(x0[0], -1), <(0, +(x1[0], x2[0]))), EOS(STATIC_3897(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_3897_0_MAIN_LOAD(&&(>(x0[0], -1), <(0, +(x1[0], x2[0]))), EOS(STATIC_3897(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_3897_0_MAIN_LOAD(&&(>(x0[0], -1), <(0, +(x1[0], x2[0]))), EOS(STATIC_3897(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_3897_0_MAIN_LOAD(&&(>(x0[0], -1), <(0, +(x1[0], x2[0]))), EOS(STATIC_3897(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_3897_0_MAIN_LOAD(&&(>(x0[0], -1), <(0, +(x1[0], x2[0]))), EOS(STATIC_3897(x0[0])), x2[0], x1[0])), ≥)∧[(2)bni_12 + (-1)Bound*bni_12] + [bni_12]x1[0] ≥ 0∧[(-1)bso_13] ≥ 0)
COND_3897_0_MAIN_LOAD(TRUE, EOS(STATIC_3897(x0)), x2, x1) → 3897_0_MAIN_LOAD(EOS(STATIC_3897(+(x0, 2))), +(x2, -1), x1)
- ((U^Increasing(3897_0_MAIN_LOAD(EOS(STATIC_3897(+(x0[1], 2))), +(x2[1], -1), x1[1])), ≥)∧[bni_14] = 0∧0 = 0∧0 = 0∧0 = 0∧[1 + (-1)bso_15] ≥ 0)
COND_3897_0_MAIN_LOAD(TRUE, EOS(STATIC_3897(x0)), x2, x1) → 3897_0_MAIN_LOAD(EOS(STATIC_3897(+(x0, 2))), x2, +(x1, -1))
- ((U^Increasing(3897_0_MAIN_LOAD(EOS(STATIC_3897(+(x0[2], 2))), x2[2], +(x1[2], -1))), ≥)∧[bni_16] = 0∧0 = 0∧0 = 0∧0 = 0∧[1 + (-1)bso_17] ≥ 0)
COND_3897_0_MAIN_LOAD(TRUE, EOS(STATIC_3897(x0)), x2, x1) → 3897_0_MAIN_LOAD(EOS(STATIC_3897(+(x0, 1))), +(x2, -1), x1)
- ((U^Increasing(3897_0_MAIN_LOAD(EOS(STATIC_3897(+(x0[3], 1))), +(x2[3], -1), x1[3])), ≥)∧[bni_18] = 0∧0 = 0∧0 = 0∧0 = 0∧[1 + (-1)bso_19] ≥ 0)
3897_0_MAIN_LOAD(EOS(STATIC_3897(x0)), x2, x1) → COND_3897_0_MAIN_LOAD3(<(0, +(x1, x2)), EOS(STATIC_3897(x0)), x2, x1)
- (x1[4] ≥ 0∧x2[4] ≥ 0 ⇒ (U^Increasing(COND_3897_0_MAIN_LOAD3(<(0, +(x1[4], x2[4])), EOS(STATIC_3897(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_3897_0_MAIN_LOAD3(<(0, +(x1[4], x2[4])), EOS(STATIC_3897(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_3897_0_MAIN_LOAD3(TRUE, EOS(STATIC_3897(x0)), x2, x1) → 3897_0_MAIN_LOAD(EOS(STATIC_3897(x0)), +(x2, -1), x1)
- ((U^Increasing(3897_0_MAIN_LOAD(EOS(STATIC_3897(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(3897_0_MAIN_LOAD(x₁, x₂, x₃)) = [1] + x₃ + x₂
POL(EOS(x₁)) = x₁
POL(STATIC_3897(x₁)) = x₁
POL(COND_3897_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_3897_0_MAIN_LOAD3(x₁, x₂, x₃, x₄)) = [1] + x₄ + x₃

The following pairs are in P_>:

COND_3897_0_MAIN_LOAD(TRUE, EOS(STATIC_3897(x0[1])), x2[1], x1[1]) → 3897_0_MAIN_LOAD(EOS(STATIC_3897(+(x0[1], 2))), +(x2[1], -1), x1[1])
COND_3897_0_MAIN_LOAD(TRUE, EOS(STATIC_3897(x0[2])), x2[2], x1[2]) → 3897_0_MAIN_LOAD(EOS(STATIC_3897(+(x0[2], 2))), x2[2], +(x1[2], -1))
COND_3897_0_MAIN_LOAD(TRUE, EOS(STATIC_3897(x0[3])), x2[3], x1[3]) → 3897_0_MAIN_LOAD(EOS(STATIC_3897(+(x0[3], 1))), +(x2[3], -1), x1[3])
COND_3897_0_MAIN_LOAD3(TRUE, EOS(STATIC_3897(x0[5])), x2[5], x1[5]) → 3897_0_MAIN_LOAD(EOS(STATIC_3897(x0[5])), +(x2[5], -1), x1[5])

The following pairs are in P_bound:

3897_0_MAIN_LOAD(EOS(STATIC_3897(x0[0])), x2[0], x1[0]) → COND_3897_0_MAIN_LOAD(&&(>(x0[0], -1), <(0, +(x1[0], x2[0]))), EOS(STATIC_3897(x0[0])), x2[0], x1[0])
3897_0_MAIN_LOAD(EOS(STATIC_3897(x0[4])), x2[4], x1[4]) → COND_3897_0_MAIN_LOAD3(<(0, +(x1[4], x2[4])), EOS(STATIC_3897(x0[4])), x2[4], x1[4])

The following pairs are in P_≥:

3897_0_MAIN_LOAD(EOS(STATIC_3897(x0[0])), x2[0], x1[0]) → COND_3897_0_MAIN_LOAD(&&(>(x0[0], -1), <(0, +(x1[0], x2[0]))), EOS(STATIC_3897(x0[0])), x2[0], x1[0])
3897_0_MAIN_LOAD(EOS(STATIC_3897(x0[4])), x2[4], x1[4]) → COND_3897_0_MAIN_LOAD3(<(0, +(x1[4], x2[4])), EOS(STATIC_3897(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_3897_0_MAIN_LOAD(TRUE, EOS(STATIC_3897(x0[1])), x2[1], x1[1]) → 3897_0_MAIN_LOAD(EOS(STATIC_3897(x0[1] + 2)), x2[1] + -1, x1[1])
(2): COND_3897_0_MAIN_LOAD(TRUE, EOS(STATIC_3897(x0[2])), x2[2], x1[2]) → 3897_0_MAIN_LOAD(EOS(STATIC_3897(x0[2] + 2)), x2[2], x1[2] + -1)
(3): COND_3897_0_MAIN_LOAD(TRUE, EOS(STATIC_3897(x0[3])), x2[3], x1[3]) → 3897_0_MAIN_LOAD(EOS(STATIC_3897(x0[3] + 1)), x2[3] + -1, x1[3])
(5): COND_3897_0_MAIN_LOAD3(TRUE, EOS(STATIC_3897(x0[5])), x2[5], x1[5]) → 3897_0_MAIN_LOAD(EOS(STATIC_3897(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