time complexity proof of /tmp/tmpAQgaZI/Convert.jar

The time complexity of the given JBC problem could be proven to be BOUNDS(CONSTANT, 46 + 263 * |#0| + 150 * |#0|^2).

0 JBC problem

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

↳2 JBCTerminationGraph

↳3 TerminationGraphToComplexityProof (BOTH CONCRETE BOUNDS(ID, ADD(11)), 17 ms)

↳4 JBCComplexityEdges

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

    ↳6 WeightedIntTrs

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

        ↳8 WeightedIntTrs

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

        ↳10 WeightedIntTrs

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

        ↳12 WeightedIntTrs

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

        ↳14 WeightedIntTrs

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

    ↳16 WeightedIntTrs

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

        ↳18 WeightedIntTrs

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

        ↳20 WeightedIntTrs

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

        ↳22 WeightedIntTrs

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

        ↳24 WeightedIntTrs

↳25 TerminationGraphToComplexityProof (BOTH CONCRETE BOUNDS(ID, ADD(11)), 12 ms)

↳26 JBCComplexityEdges

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

    ↳28 WeightedIntTrs

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

    ↳30 WeightedIntTrs

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

    ↳32 WeightedIntTrs

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

    ↳34 WeightedIntTrs

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

    ↳36 WeightedIntTrs

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

    ↳38 WeightedIntTrs

    ↳39 koat Proof (⇔, 813 ms)

    ↳40 BOUNDS(CONSTANT, 35 + 263 * |#0| + 150 * |#0|^2)

(0) Obligation:

Need to prove time_complexity of the following program:

public class Convert{

  // adapted from [Giesl, 95]
  // converts a number to decimal notation

  public static void main(int i, int b) {
    IntList l = IntList.createIntList(i);

    int res = 0;

    while (l != null) {

      if (l.value <= 0) {
        l = l.next;
        if (l != null) res = res * b;
      }
      else {
        l.value--;
        res++;
      }
    }
  }
}

class IntList {
  int value;
  IntList next;

  public IntList(int value, IntList next) {
    this.value = value;
    this.next = next;
  }

  public static IntList createIntList(int i) {

    IntList l = null;

    while (i > 0) {
      l = new IntList(i, l);
      i--;
    }

    return l;
  }
}

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

Constructed TerminationGraph.

(2) Obligation:

Termination Graph based on JBC Program:
Convert.main(II)V: Graph of 117 nodes with 2 SCCs.

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

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

(4) Obligation:

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

Used field analysis yielded the following read fields:
- IntList: [value, next]

Considered paths: nonterm paths and paths from start to sinks

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

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

(6) Obligation:

IntTrs with 109 rules
Start term: main_Load_1(#0, #1, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_Load_1(i2, i4, env, static) -{0,0}> main_Load_3(i2, i4, env, static) :|: 0 >= 0
main_Load_3(i2, i4, env, static) -{0,0}> langle_clinit_rangle_ConstantStackPush_5(i2, i4, env, static) :|: 0 >= 0
langle_clinit_rangle_ConstantStackPush_5(i2, i4, env, static) -{1,1}> langle_clinit_rangle_ArrayCreate_12(iconst_0, i2, i4, env, static) :|: iconst_0 = 0
langle_clinit_rangle_ArrayCreate_12(iconst_0, i2, i4, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_13(a2, i2, i4, iconst_0, env, static) :|: a2 = 2 && iconst_0 = 0 && 0 < a2
langle_clinit_rangle_FieldAccess_13(a2, i2, i4, iconst_0, env, static) -{1,1}> langle_clinit_rangle_New_14(i2, i4, env, static') :|: 0 <= a2 && iconst_0 = 0 && static' <= static + a2 && 0 <= static && 0 < a2
langle_clinit_rangle_New_14(i2, i4, env, static) -{0,0}> langle_clinit_rangle_New_16(i2, i4, env, static) :|: 0 >= 0
langle_clinit_rangle_New_16(i2, i4, env, static) -{0,0}> langle_clinit_rangle_New_17(i2, i4, env, static) :|: 0 <= static
langle_clinit_rangle_New_17(i2, i4, env, static) -{1,1}> langle_clinit_rangle_Duplicate_19(o2, i2, i4, env, static) :|: 0 < o2 && o2 = 1
langle_clinit_rangle_Duplicate_19(o2, i2, i4, env, static) -{1,1}> langle_clinit_rangle_ConstantStackPush_21(o2, i2, i4, env, static) :|: 0 < o2
langle_clinit_rangle_ConstantStackPush_21(o2, i2, i4, env, static) -{1,1}> langle_clinit_rangle_InvokeMethod_22(o2, NULL, i2, i4, env, static) :|: NULL = 0 && 0 < o2
langle_clinit_rangle_InvokeMethod_22(o2, NULL, i2, i4, env, static) -{1,1}> langle_init_rangle_Load_24(o2, i2, i4, env, static) :|: NULL = 0 && 0 < o2
langle_init_rangle_Load_24(o2, i2, i4, env, static) -{1,1}> langle_init_rangle_InvokeMethod_29(o2, i2, i4, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_29(o2, i2, i4, env, static) -{1,1}> langle_init_rangle_Load_30(o2, i2, i4, env, static) :|: 0 < o2
langle_init_rangle_Load_30(o2, i2, i4, env, static) -{1,1}> langle_init_rangle_InvokeMethod_33(o2, i2, i4, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_33(o2, i2, i4, env, static) -{1,1}> langle_init_rangle_Return_35(o2, i2, i4, env, static) :|: 0 < o2
langle_init_rangle_Return_35(o2, i2, i4, env, static) -{1,1}> langle_init_rangle_Return_38(o2, i2, i4, env, static) :|: 0 < o2
langle_init_rangle_Return_38(o2, i2, i4, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_39(o2, i2, i4, env, static) :|: 0 < o2
langle_clinit_rangle_FieldAccess_39(o2, i2, i4, env, static) -{1,1}> langle_clinit_rangle_Return_40(i2, i4, env, static') :|: 0 < o2 && 0 <= o2 && 0 <= static && static' <= static + o2
langle_clinit_rangle_Return_40(i2, i4, env, static) -{1,1}> main_Load_46(i2, i4, env, static) :|: 0 >= 0
main_Load_46(i2, i4, env, static) -{0,0}> main_Load_47(i2, i4, env, static) :|: 0 >= 0
main_Load_47(i2, i4, env, static) -{0,0}> main_Load_50(i2, i4, env, static) :|: 0 <= static
main_Load_50(i2, i4, env, static) -{0,0}> main_Load_51(i2, i4, env, static) :|: 0 >= 0
main_Load_51(i2, i4, env, static) -{0,0}> main_Load_52(i2, i4, env, static) :|: 0 >= 0
main_Load_52(i2, i4, env, static) -{1,1}> main_InvokeMethod_55(i2, i4, env, static) :|: 0 >= 0
main_InvokeMethod_55(i2, i4, env, static) -{0,0}> main_InvokeMethod_56(i2, i4, env, static) :|: 0 >= 0
main_InvokeMethod_56(i2, i4, env, static) -{1,1}> createIntList_ConstantStackPush_57(i2, i4, env, static) :|: 0 >= 0
createIntList_ConstantStackPush_57(i2, i4, env, static) -{1,1}> createIntList_Store_58(NULL, i2, i4, env, static) :|: NULL = 0
createIntList_Store_58(NULL, i2, i4, env, static) -{1,1}> createIntList_Load_59(i2, NULL, i4, env, static) :|: NULL = 0
createIntList_Load_59(i2, NULL, i4, env, static) -{1,1}> createIntList_LE_62(i2, NULL, i4, env, static) :|: NULL = 0
createIntList_LE_62(i11, NULL, i4, env, static) -{0,0}> createIntList_LE_63(i11, NULL, i4, env, static) :|: NULL = 0 && i11 <= 0
createIntList_LE_62(i12, NULL, i4, env, static) -{0,0}> createIntList_LE_64(i12, NULL, i4, env, static) :|: NULL = 0 && 1 <= i12
createIntList_LE_64(i12, NULL, i4, env, static) -{1,1}> createIntList_New_66(i12, NULL, i4, env, static) :|: NULL = 0 && 0 < i12 && 1 <= i12
createIntList_New_66(i12, NULL, i4, env, static) -{1,1}> createIntList_Duplicate_75(o3, i12, NULL, i4, iconst_0, env, static) :|: NULL = 0 && o3 = 1 && 0 < o3 && iconst_0 = 0 && 1 <= i12
createIntList_Duplicate_75(o3, i12, NULL, i4, iconst_0, env, static) -{1,1}> createIntList_Load_80(o3, i12, NULL, i4, iconst_0, env, static) :|: NULL = 0 && 0 < o3 && iconst_0 = 0 && 1 <= i12
createIntList_Load_80(o3, i12, NULL, i4, iconst_0, env, static) -{1,1}> createIntList_Load_84(o3, i12, NULL, i4, iconst_0, env, static) :|: NULL = 0 && 0 < o3 && iconst_0 = 0 && 1 <= i12
createIntList_Load_84(o3, i12, NULL, i4, iconst_0, env, static) -{1,1}> createIntList_InvokeMethod_89(o3, i12, NULL, i4, iconst_0, env, static) :|: NULL = 0 && 0 < o3 && iconst_0 = 0 && 1 <= i12
createIntList_InvokeMethod_89(o3, i12, NULL, i4, iconst_0, env, static) -{1,1}> langle_init_rangle_Load_92(o3, i12, NULL, i4, iconst_0, env, static) :|: NULL = 0 && 0 < o3 && iconst_0 = 0 && 1 <= i12
langle_init_rangle_Load_92(o3, i12, NULL, i4, iconst_0, env, static) -{1,1}> langle_init_rangle_InvokeMethod_98(o3, i12, NULL, i4, iconst_0, env, static) :|: NULL = 0 && 0 < o3 && iconst_0 = 0 && 1 <= i12
langle_init_rangle_InvokeMethod_98(o3, i12, NULL, i4, iconst_0, env, static) -{1,1}> langle_init_rangle_Load_100(o3, i12, NULL, i4, iconst_0, env, static) :|: NULL = 0 && 0 < o3 && iconst_0 = 0 && 1 <= i12
langle_init_rangle_Load_100(o3, i12, NULL, i4, iconst_0, env, static) -{1,1}> langle_init_rangle_Load_101(o3, i12, NULL, i4, iconst_0, env, static) :|: NULL = 0 && 0 < o3 && iconst_0 = 0 && 1 <= i12
langle_init_rangle_Load_101(o3, i12, NULL, i4, iconst_0, env, static) -{0,0}> langle_init_rangle_Load_313(o3, i12, NULL, i12, i4, NULL, iconst_0, env, static) :|: NULL = 0 && 0 < o3 && iconst_0 = 0 && 0 <= NULL && 1 <= i12
langle_init_rangle_Load_313(o90, i66, o91, i67, i4, NULL, iconst_0, env, static) -{1,1}> langle_init_rangle_FieldAccess_317(o90, i66, o91, i67, i4, NULL, iconst_0, env, static) :|: NULL = 0 && 0 <= o91 && 1 <= i67 && 1 <= i66 && iconst_0 = 0 && 0 < o90
langle_init_rangle_FieldAccess_317(o90, i66, o91, i67, i4, NULL, iconst_0, env, static) -{1,1}> langle_init_rangle_Load_320(o90', o91, i66, i67, i4, NULL, env, static) :|: NULL = 0 && 0 <= o91 && 0 < o90' && 1 <= i67 && 1 <= i66 && iconst_0 = 0 && 0 < o90 && o90' <= o90 + i66 && o90 < o90'
langle_init_rangle_Load_320(o90, o91, i66, i67, i4, NULL, env, static) -{1,1}> langle_init_rangle_Load_322(o90, o91, i66, i67, i4, NULL, env, static) :|: NULL = 0 && 0 <= o91 && 1 <= i67 && 1 <= i66 && 0 < o90
langle_init_rangle_Load_322(o90, o91, i66, i67, i4, NULL, env, static) -{1,1}> langle_init_rangle_FieldAccess_324(o90, o91, i66, i67, i4, NULL, env, static) :|: NULL = 0 && 0 <= o91 && 1 <= i67 && 1 <= i66 && 0 < o90
langle_init_rangle_FieldAccess_324(o90, o91, i66, i67, i4, NULL, env, static) -{1,1}> langle_init_rangle_Return_329(o90', i66, i67, i4, o91, env, static) :|: NULL = 0 && 0 <= o91 && 0 < o90' && 1 <= i67 && o90' <= o90 + o91 && 1 <= i66 && o90' = o90 + o91 && 0 < o90
langle_init_rangle_Return_329(o90, i66, i67, i4, o91, env, static) -{1,1}> createIntList_Store_331(o90, i66, i67, i4, o91, env, static) :|: 0 <= o91 && 1 <= i67 && 1 <= i66 && 0 < o90
createIntList_Store_331(o90, i66, i67, i4, o91, env, static) -{1,1}> createIntList_Inc_333(i66, o90, i67, i4, o91, env, static) :|: 0 <= o91 && 1 <= i67 && 1 <= i66 && 0 < o90
createIntList_Inc_333(i66, o90, i67, i4, o91, env, static) -{1,1}> createIntList_JMP_335(i73, o90, i67, i4, o91, i66, env, static) :|: i66 + -1 = i73 && 0 <= o91 && 1 <= i67 && 1 <= i66 && 0 < o90 && 0 <= i73
createIntList_JMP_335(i73, o90, i67, i4, o91, i66, env, static) -{1,1}> createIntList_Load_338(i73, o90, i67, i4, o91, i66, env, static) :|: 0 <= o91 && 1 <= i67 && 1 <= i66 && 0 < o90 && 0 <= i73
createIntList_Load_338(i73, o90, i67, i4, o91, i66, env, static) -{1,1}> createIntList_LE_346(i73, o90, i67, i4, o91, i66, env, static) :|: 0 <= o91 && 1 <= i67 && 1 <= i66 && 0 < o90 && 0 <= i73
createIntList_LE_346(iconst_0, o90, i67, i4, o91, i66, env, static) -{0,0}> createIntList_LE_348(iconst_0, o90, i67, i4, o91, i66, env, static) :|: 0 <= o91 && 0 <= iconst_0 && 1 <= i67 && 1 <= i66 && iconst_0 = 0 && 0 < o90
createIntList_LE_346(i80, o90, i67, i4, o91, i81, env, static) -{0,0}> createIntList_LE_350(i80, o90, i67, i4, o91, i81, env, static) :|: 1 <= i80 && 0 <= o91 && 2 <= i81 && 1 <= i67 && 0 <= i80 && 0 < o90 && 1 <= i81
createIntList_LE_348(iconst_0, o90, i67, i4, o91, i66, env, static) -{1,1}> createIntList_Load_353(o90, i67, i4, o91, i66, env, static) :|: 0 <= o91 && iconst_0 <= 0 && 1 <= i67 && 1 <= i66 && iconst_0 = 0 && 0 < o90
createIntList_LE_350(i80, o90, i67, i4, o91, i81, env, static) -{1,1}> createIntList_New_356(i80, o90, i67, i4, o91, i81, env, static) :|: 1 <= i80 && 0 <= o91 && 2 <= i81 && 1 <= i67 && 0 < i80 && 0 < o90
createIntList_Load_353(o90, i67, i4, o91, i66, env, static) -{1,1}> createIntList_Return_359(o90, i67, i4, o91, i66, env, static) :|: 0 <= o91 && 1 <= i67 && 1 <= i66 && 0 < o90
createIntList_New_356(i80, o90, i67, i4, o91, i81, env, static) -{1,1}> createIntList_Duplicate_362(o111, i80, o90, i67, i4, NULL, iconst_0, o91, i81, env, static) :|: NULL = 0 && 1 <= i80 && o111 = 1 && 0 <= o91 && 2 <= i81 && 1 <= i67 && iconst_0 = 0 && 0 < o90 && 0 < o111
createIntList_Return_359(o90, i67, i4, o91, i66, env, static) -{1,1}> main_Store_364(i67, i4, o90, o91, i66, env, static) :|: 0 <= o91 && 1 <= i67 && 1 <= i66 && 0 < o90
createIntList_Duplicate_362(o111, i80, o90, i67, i4, NULL, iconst_0, o91, i81, env, static) -{1,1}> createIntList_Load_365(o111, i80, o90, i67, i4, NULL, iconst_0, o91, i81, env, static) :|: NULL = 0 && 1 <= i80 && 0 <= o91 && 2 <= i81 && 1 <= i67 && iconst_0 = 0 && 0 < o90 && 0 < o111
main_Store_364(i67, i4, o90, o91, i66, env, static) -{1,1}> main_ConstantStackPush_366(i67, i4, o90, o91, i66, env, static) :|: 0 <= o91 && 1 <= i67 && 1 <= i66 && 0 < o90
createIntList_Load_365(o111, i80, o90, i67, i4, NULL, iconst_0, o91, i81, env, static) -{1,1}> createIntList_Load_367(o111, i80, o90, i67, i4, NULL, iconst_0, o91, i81, env, static) :|: NULL = 0 && 1 <= i80 && 0 <= o91 && 2 <= i81 && 1 <= i67 && iconst_0 = 0 && 0 < o90 && 0 < o111
main_ConstantStackPush_366(i67, i4, o90, o91, i66, env, static) -{1,1}> main_Store_369(i67, i4, iconst_0, o90, o91, i66, env, static) :|: 0 <= o91 && 1 <= i67 && 1 <= i66 && iconst_0 = 0 && 0 < o90
createIntList_Load_367(o111, i80, o90, i67, i4, NULL, iconst_0, o91, i81, env, static) -{1,1}> createIntList_InvokeMethod_372(o111, i80, o90, i67, i4, NULL, iconst_0, o91, i81, env, static) :|: NULL = 0 && 1 <= i80 && 0 <= o91 && 2 <= i81 && 1 <= i67 && iconst_0 = 0 && 0 < o90 && 0 < o111
main_Store_369(i67, i4, iconst_0, o90, o91, i66, env, static) -{1,1}> main_Load_375(i67, i4, o90, iconst_0, o91, i66, env, static) :|: 0 <= o91 && 1 <= i67 && 1 <= i66 && iconst_0 = 0 && 0 < o90
createIntList_InvokeMethod_372(o111, i80, o90, i67, i4, NULL, iconst_0, o91, i81, env, static) -{1,1}> langle_init_rangle_Load_376(o111, i80, o90, i67, i4, NULL, iconst_0, o91, i81, env, static) :|: NULL = 0 && 1 <= i80 && 0 <= o91 && 2 <= i81 && 1 <= i67 && iconst_0 = 0 && 0 < o90 && 0 < o111
main_Load_375(i67, i4, o90, iconst_0, o91, i66, env, static) -{0,0}> main_Load_437(i67, i4, o90, iconst_0, o91, i66, env, static) :|: 0 <= o91 && 0 <= i66 && 1 <= i67 && 0 <= iconst_0 && 1 <= i66 && iconst_0 <= 1 && iconst_0 = 0 && 0 < o90
langle_init_rangle_Load_376(o111, i80, o90, i67, i4, NULL, iconst_0, o91, i81, env, static) -{1,1}> langle_init_rangle_InvokeMethod_382(o111, i80, o90, i67, i4, NULL, iconst_0, o91, i81, env, static) :|: NULL = 0 && 1 <= i80 && 0 <= o91 && 2 <= i81 && 1 <= i67 && iconst_0 = 0 && 0 < o90 && 0 < o111
langle_init_rangle_InvokeMethod_382(o111, i80, o90, i67, i4, NULL, iconst_0, o91, i81, env, static) -{1,1}> langle_init_rangle_Load_384(o111, i80, o90, i67, i4, NULL, iconst_0, o91, i81, env, static) :|: NULL = 0 && 1 <= i80 && 0 <= o91 && 2 <= i81 && 1 <= i67 && iconst_0 = 0 && 0 < o90 && 0 < o111
langle_init_rangle_Load_384(o111, i80, o90, i67, i4, NULL, iconst_0, o91, i81, env, static) -{1,1}> langle_init_rangle_Load_388(o111, i80, o90, i67, i4, NULL, iconst_0, o91, i81, env, static) :|: NULL = 0 && 1 <= i80 && 0 <= o91 && 2 <= i81 && 1 <= i67 && iconst_0 = 0 && 0 < o90 && 0 < o111
langle_init_rangle_Load_388(o111, i80, o90, i67, i4, NULL, iconst_0, o91, i81, env, static) -{0,0}> langle_init_rangle_Load_313(o111, i80, o90, i67, i4, NULL, iconst_0, env, static) :|: NULL = 0 && 1 <= i80 && 0 <= o91 && 2 <= i81 && 1 <= i67 && 0 <= o90 && iconst_0 = 0 && 0 < o90 && 0 < o111
main_Load_437(i67, i4, o139, i97, o140, i96, env, static) -{0,0}> main_Load_487(i67, i4, o139, i97, env, static) :|: 0 <= o140 && 0 < o139 && 1 <= i67 && 0 <= i97 && 0 <= o139 && 0 <= i96 && i97 <= 1
main_Load_487(i67, i4, o156, i97, env, static) -{0,0}> main_Load_546(i67, i4, o156, i97, env, static) :|: 1 <= i67 && 0 <= i97 && 0 <= o156 && i97 <= 1 && i97 <= 2
main_Load_546(i67, i4, o176, i118, env, static) -{0,0}> main_Load_601(i67, i4, o176, i118, env, static) :|: 1 <= i67 && 0 <= o176 && i118 <= 2 && 0 <= i118
main_Load_601(i67, i4, o195, i127, env, static) -{0,0}> main_Load_653(i67, i4, o195, i127, env, static) :|: 1 <= i67 && 0 <= o195 && 0 <= i127
main_Load_653(i67, i4, o217, i137, env, static) -{1,1}> main_NULL_656(i67, i4, o217, i137, env, static) :|: 1 <= i67 && 0 <= o217
main_NULL_656(i67, i4, o226, i137, env, static) -{0,0}> main_NULL_658(i67, i4, o226, i137, env, static) :|: 0 <= o226 && 1 <= i67 && 0 < o226
main_NULL_656(i67, i4, NULL, i137, env, static) -{0,0}> main_NULL_659(i67, i4, NULL, i137, env, static) :|: NULL = 0 && 1 <= i67 && 0 <= NULL
main_NULL_658(i67, i4, o226, i137, env, static) -{1,1}> main_Load_661(i67, i4, o226, i137, env, static) :|: 1 <= i67 && 0 < o226
main_Load_661(i67, i4, o226, i137, env, static) -{1,1}> main_FieldAccess_665(i67, i4, o226, i137, env, static) :|: 1 <= i67 && 0 < o226
main_FieldAccess_665(i67, i4, o228, i137, env, static) -{0,0}> main_FieldAccess_668(i67, i4, o228, i137, o229, i142, env, static) :|: 0 <= o229 && 1 <= i67 && o229 < o228 && -1 * o228 < i142 && 0 < o228 && i142 < o228
main_FieldAccess_668(i67, i4, o228, i137, o229, i142, env, static) -{1,1}> main_GT_671(i67, i4, i142, o228, i137, o229, env, static) :|: 0 <= o229 && 1 <= i67 && 0 < o228
main_GT_671(i67, i4, i143, o228, i137, o229, env, static) -{0,0}> main_GT_672(i67, i4, i143, o228, i137, o229, env, static) :|: 0 <= o229 && 1 <= i67 && i143 <= 0 && 0 < o228
main_GT_671(i67, i4, i144, o228, i137, o229, env, static) -{0,0}> main_GT_673(i67, i4, i144, o228, i137, o229, env, static) :|: 1 <= i144 && 0 <= o229 && 1 <= i67 && 0 < o228
main_GT_672(i67, i4, i143, o228, i137, o229, env, static) -{1,1}> main_Load_675(i67, i4, o228, i137, o229, i143, env, static) :|: 0 <= o229 && 1 <= i67 && i143 <= 0 && 0 < o228
main_GT_673(i67, i4, i144, o228, i137, o229, env, static) -{1,1}> main_Load_677(i67, i4, o228, i137, o229, i144, env, static) :|: 1 <= i144 && 0 <= o229 && 1 <= i67 && 0 < i144 && 0 < o228
main_Load_675(i67, i4, o228, i137, o229, i143, env, static) -{1,1}> main_FieldAccess_679(i67, i4, o228, i137, o229, i143, env, static) :|: 0 <= o229 && 1 <= i67 && i143 <= 0 && 0 < o228
main_Load_677(i67, i4, o228, i137, o229, i144, env, static) -{1,1}> main_Duplicate_680(i67, i4, o228, i137, o229, i144, env, static) :|: 1 <= i144 && 0 <= o229 && 1 <= i67 && 0 < o228
main_FieldAccess_679(i67, i4, o228, i137, o229, i143, env, static) -{1,1}> main_Store_682(i67, i4, o229, i137, env, static) :|: 0 <= o229 && 1 <= i67 && i143 <= 0 && 0 < o228
main_Duplicate_680(i67, i4, o228, i137, o229, i144, env, static) -{1,1}> main_FieldAccess_684(i67, i4, o228, i137, o229, i144, env, static) :|: 1 <= i144 && 0 <= o229 && 1 <= i67 && 0 < o228
main_Store_682(i67, i4, o229, i137, env, static) -{1,1}> main_Load_685(i67, i4, o229, i137, env, static) :|: 0 <= o229 && 1 <= i67
main_FieldAccess_684(i67, i4, o228, i137, o229, i144, env, static) -{1,1}> main_ConstantStackPush_687(i67, i4, o228, i144, i137, o229, env, static) :|: 1 <= i144 && 0 <= o229 && 1 <= i67 && 0 < o228
main_Load_685(i67, i4, o229, i137, env, static) -{1,1}> main_NULL_689(i67, i4, o229, i137, env, static) :|: 0 <= o229 && 1 <= i67
main_ConstantStackPush_687(i67, i4, o228, i144, i137, o229, env, static) -{1,1}> main_IntArithmetic_691(i67, i4, o228, i144, iconst_1, i137, o229, env, static) :|: 1 <= i144 && 0 <= o229 && 1 <= i67 && iconst_1 = 1 && 0 < o228
main_NULL_689(i67, i4, o230, i137, env, static) -{0,0}> main_NULL_693(i67, i4, o230, i137, env, static) :|: 0 < o230 && 1 <= i67 && 0 <= o230
main_NULL_689(i67, i4, NULL, i137, env, static) -{0,0}> main_NULL_694(i67, i4, NULL, i137, env, static) :|: NULL = 0 && 1 <= i67 && 0 <= NULL
main_IntArithmetic_691(i67, i4, o228, i144, iconst_1, i137, o229, env, static) -{1,1}> main_FieldAccess_697(i67, i4, o228, i146, i137, o229, i144, env, static) :|: 1 <= i144 && 0 <= o229 && 1 <= i67 && iconst_1 = 1 && 0 <= i146 && i144 - iconst_1 = i146 && 0 < o228
main_NULL_693(i67, i4, o230, i137, env, static) -{1,1}> main_Load_699(i67, i4, o230, i137, env, static) :|: 0 < o230 && 1 <= i67
main_NULL_694(i67, i4, NULL, i137, env, static) -{1,1}> main_Load_707(i67, i4, NULL, i137, env, static) :|: NULL = 0 && 1 <= i67
main_FieldAccess_697(i67, i4, o228, i146, i137, o229, i144, env, static) -{1,1}> main_Inc_710(i67, i4, o228', i137, o229, i146, env, static) :|: 0 < o228' && 1 <= i144 && 0 <= o229 && 1 <= i67 && o228' <= o228 + i146 && 0 <= i146 && o228' < o228 && 0 < o228
main_Load_699(i67, i4, o230, i137, env, static) -{1,1}> main_Load_712(i67, i4, i137, o230, env, static) :|: 0 < o230 && 1 <= i67
main_Load_707(i67, i4, NULL, i137, env, static) -{0,0}> main_Load_653(i67, i4, NULL, i137, env, static) :|: NULL = 0 && 1 <= i67 && 0 <= NULL
main_Inc_710(i67, i4, o228, i137, o229, i146, env, static) -{1,1}> main_JMP_715(i67, i4, o228, i148, o229, i146, env, static) :|: i137 + 1 = i148 && 0 <= o229 && 1 <= i67 && 0 <= i146 && 0 < o228
main_Load_712(i67, i4, i137, o230, env, static) -{1,1}> main_IntArithmetic_717(i67, i4, i137, o230, env, static) :|: 0 < o230 && 1 <= i67
main_JMP_715(i67, i4, o228, i148, o229, i146, env, static) -{1,1}> main_Load_722(i67, i4, o228, i148, o229, i146, env, static) :|: 0 <= o229 && 1 <= i67 && 0 <= i146 && 0 < o228
main_IntArithmetic_717(i67, i4, i137, o230, env, static) -{1,1}> main_Store_724(i67, i4, i150, o230, env, static) :|: 0 < o230 && 1 <= i67 && i137 * i4 = i150
main_Load_722(i67, i4, o228, i148, o229, i146, env, static) -{0,0}> main_Load_653(i67, i4, o228, i148, env, static) :|: 0 <= o229 && 1 <= i67 && 0 <= i146 && 0 < o228 && 0 <= o228
main_Store_724(i67, i4, i150, o230, env, static) -{1,1}> main_JMP_726(i67, i4, o230, i150, env, static) :|: 0 < o230 && 1 <= i67
main_JMP_726(i67, i4, o230, i150, env, static) -{1,1}> main_Load_732(i67, i4, o230, i150, env, static) :|: 0 < o230 && 1 <= i67
main_Load_732(i67, i4, o230, i150, env, static) -{0,0}> main_Load_653(i67, i4, o230, i150, env, static) :|: 0 < o230 && 1 <= i67 && 0 <= o230

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

obtained
main_Load_1(i2, i4, env, static) -{20,20}> createIntList_LE_62(i2, 0, i4, env, static'1) :|: 0 <= static'1 && 0 < 2 && 0 <= static && 0 <= 1 && 0 < 1 && static''' <= static + 2 && 0 <= static''' && 0 <= 2 && static'1 <= static''' + 1 && 0 >= 0
by chaining
main_Load_1(i2, i4, env, static) -{0,0}> main_Load_3(i2, i4, env, static) :|: 0 >= 0
main_Load_3(i2, i4, env, static) -{0,0}> langle_clinit_rangle_ConstantStackPush_5(i2, i4, env, static) :|: 0 >= 0
langle_clinit_rangle_ConstantStackPush_5(i2, i4, env, static) -{1,1}> langle_clinit_rangle_ArrayCreate_12(iconst_0, i2, i4, env, static) :|: iconst_0 = 0
langle_clinit_rangle_ArrayCreate_12(iconst_0, i2, i4, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_13(a2, i2, i4, iconst_0, env, static) :|: a2 = 2 && iconst_0 = 0 && 0 < a2
langle_clinit_rangle_FieldAccess_13(a2, i2, i4, iconst_0, env, static) -{1,1}> langle_clinit_rangle_New_14(i2, i4, env, static') :|: 0 <= a2 && iconst_0 = 0 && static' <= static + a2 && 0 <= static && 0 < a2
langle_clinit_rangle_New_14(i2, i4, env, static) -{0,0}> langle_clinit_rangle_New_16(i2, i4, env, static) :|: 0 >= 0
langle_clinit_rangle_New_16(i2, i4, env, static) -{0,0}> langle_clinit_rangle_New_17(i2, i4, env, static) :|: 0 <= static
langle_clinit_rangle_New_17(i2, i4, env, static) -{1,1}> langle_clinit_rangle_Duplicate_19(o2, i2, i4, env, static) :|: 0 < o2 && o2 = 1
langle_clinit_rangle_Duplicate_19(o2, i2, i4, env, static) -{1,1}> langle_clinit_rangle_ConstantStackPush_21(o2, i2, i4, env, static) :|: 0 < o2
langle_clinit_rangle_ConstantStackPush_21(o2, i2, i4, env, static) -{1,1}> langle_clinit_rangle_InvokeMethod_22(o2, NULL, i2, i4, env, static) :|: NULL = 0 && 0 < o2
langle_clinit_rangle_InvokeMethod_22(o2, NULL, i2, i4, env, static) -{1,1}> langle_init_rangle_Load_24(o2, i2, i4, env, static) :|: NULL = 0 && 0 < o2
langle_init_rangle_Load_24(o2, i2, i4, env, static) -{1,1}> langle_init_rangle_InvokeMethod_29(o2, i2, i4, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_29(o2, i2, i4, env, static) -{1,1}> langle_init_rangle_Load_30(o2, i2, i4, env, static) :|: 0 < o2
langle_init_rangle_Load_30(o2, i2, i4, env, static) -{1,1}> langle_init_rangle_InvokeMethod_33(o2, i2, i4, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_33(o2, i2, i4, env, static) -{1,1}> langle_init_rangle_Return_35(o2, i2, i4, env, static) :|: 0 < o2
langle_init_rangle_Return_35(o2, i2, i4, env, static) -{1,1}> langle_init_rangle_Return_38(o2, i2, i4, env, static) :|: 0 < o2
langle_init_rangle_Return_38(o2, i2, i4, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_39(o2, i2, i4, env, static) :|: 0 < o2
langle_clinit_rangle_FieldAccess_39(o2, i2, i4, env, static) -{1,1}> langle_clinit_rangle_Return_40(i2, i4, env, static') :|: 0 < o2 && 0 <= o2 && 0 <= static && static' <= static + o2
langle_clinit_rangle_Return_40(i2, i4, env, static) -{1,1}> main_Load_46(i2, i4, env, static) :|: 0 >= 0
main_Load_46(i2, i4, env, static) -{0,0}> main_Load_47(i2, i4, env, static) :|: 0 >= 0
main_Load_47(i2, i4, env, static) -{0,0}> main_Load_50(i2, i4, env, static) :|: 0 <= static
main_Load_50(i2, i4, env, static) -{0,0}> main_Load_51(i2, i4, env, static) :|: 0 >= 0
main_Load_51(i2, i4, env, static) -{0,0}> main_Load_52(i2, i4, env, static) :|: 0 >= 0
main_Load_52(i2, i4, env, static) -{1,1}> main_InvokeMethod_55(i2, i4, env, static) :|: 0 >= 0
main_InvokeMethod_55(i2, i4, env, static) -{0,0}> main_InvokeMethod_56(i2, i4, env, static) :|: 0 >= 0
main_InvokeMethod_56(i2, i4, env, static) -{1,1}> createIntList_ConstantStackPush_57(i2, i4, env, static) :|: 0 >= 0
createIntList_ConstantStackPush_57(i2, i4, env, static) -{1,1}> createIntList_Store_58(NULL, i2, i4, env, static) :|: NULL = 0
createIntList_Store_58(NULL, i2, i4, env, static) -{1,1}> createIntList_Load_59(i2, NULL, i4, env, static) :|: NULL = 0
createIntList_Load_59(i2, NULL, i4, env, static) -{1,1}> createIntList_LE_62(i2, NULL, i4, env, static) :|: NULL = 0

obtained
createIntList_LE_62(i12, 0, i4, env, static) -{9,9}> langle_init_rangle_Load_313(1, i12, 0, i12, i4, 0, 0, env, static) :|: 0 < i12 && 1 <= i12 && 0 < 1 && 0 <= 0
by chaining
createIntList_LE_62(i12, NULL, i4, env, static) -{0,0}> createIntList_LE_64(i12, NULL, i4, env, static) :|: NULL = 0 && 1 <= i12
createIntList_LE_64(i12, NULL, i4, env, static) -{1,1}> createIntList_New_66(i12, NULL, i4, env, static) :|: NULL = 0 && 0 < i12 && 1 <= i12
createIntList_New_66(i12, NULL, i4, env, static) -{1,1}> createIntList_Duplicate_75(o3, i12, NULL, i4, iconst_0, env, static) :|: NULL = 0 && o3 = 1 && 0 < o3 && iconst_0 = 0 && 1 <= i12
createIntList_Duplicate_75(o3, i12, NULL, i4, iconst_0, env, static) -{1,1}> createIntList_Load_80(o3, i12, NULL, i4, iconst_0, env, static) :|: NULL = 0 && 0 < o3 && iconst_0 = 0 && 1 <= i12
createIntList_Load_80(o3, i12, NULL, i4, iconst_0, env, static) -{1,1}> createIntList_Load_84(o3, i12, NULL, i4, iconst_0, env, static) :|: NULL = 0 && 0 < o3 && iconst_0 = 0 && 1 <= i12
createIntList_Load_84(o3, i12, NULL, i4, iconst_0, env, static) -{1,1}> createIntList_InvokeMethod_89(o3, i12, NULL, i4, iconst_0, env, static) :|: NULL = 0 && 0 < o3 && iconst_0 = 0 && 1 <= i12
createIntList_InvokeMethod_89(o3, i12, NULL, i4, iconst_0, env, static) -{1,1}> langle_init_rangle_Load_92(o3, i12, NULL, i4, iconst_0, env, static) :|: NULL = 0 && 0 < o3 && iconst_0 = 0 && 1 <= i12
langle_init_rangle_Load_92(o3, i12, NULL, i4, iconst_0, env, static) -{1,1}> langle_init_rangle_InvokeMethod_98(o3, i12, NULL, i4, iconst_0, env, static) :|: NULL = 0 && 0 < o3 && iconst_0 = 0 && 1 <= i12
langle_init_rangle_InvokeMethod_98(o3, i12, NULL, i4, iconst_0, env, static) -{1,1}> langle_init_rangle_Load_100(o3, i12, NULL, i4, iconst_0, env, static) :|: NULL = 0 && 0 < o3 && iconst_0 = 0 && 1 <= i12
langle_init_rangle_Load_100(o3, i12, NULL, i4, iconst_0, env, static) -{1,1}> langle_init_rangle_Load_101(o3, i12, NULL, i4, iconst_0, env, static) :|: NULL = 0 && 0 < o3 && iconst_0 = 0 && 1 <= i12
langle_init_rangle_Load_101(o3, i12, NULL, i4, iconst_0, env, static) -{0,0}> langle_init_rangle_Load_313(o3, i12, NULL, i12, i4, NULL, iconst_0, env, static) :|: NULL = 0 && 0 < o3 && iconst_0 = 0 && 0 <= NULL && 1 <= i12

obtained
langle_init_rangle_Load_313(o90, i66, o91, i67, i4, 0, 0, env, static) -{10,10}> createIntList_LE_346(i73', o90'1, i67, i4, o91, i66, env, static) :|: o90 < o90''' && 0 <= i73' && 0 < o90 && 0 < o90'1 && o90'1 <= o90''' + o91 && 1 <= i66 && 1 <= i67 && 0 <= o91 && i66 + -1 = i73' && o90''' <= o90 + i66 && o90'1 = o90''' + o91 && 0 < o90'''
by chaining
langle_init_rangle_Load_313(o90, i66, o91, i67, i4, NULL, iconst_0, env, static) -{1,1}> langle_init_rangle_FieldAccess_317(o90, i66, o91, i67, i4, NULL, iconst_0, env, static) :|: NULL = 0 && 0 <= o91 && 1 <= i67 && 1 <= i66 && iconst_0 = 0 && 0 < o90
langle_init_rangle_FieldAccess_317(o90, i66, o91, i67, i4, NULL, iconst_0, env, static) -{1,1}> langle_init_rangle_Load_320(o90', o91, i66, i67, i4, NULL, env, static) :|: NULL = 0 && 0 <= o91 && 0 < o90' && 1 <= i67 && 1 <= i66 && iconst_0 = 0 && 0 < o90 && o90' <= o90 + i66 && o90 < o90'
langle_init_rangle_Load_320(o90, o91, i66, i67, i4, NULL, env, static) -{1,1}> langle_init_rangle_Load_322(o90, o91, i66, i67, i4, NULL, env, static) :|: NULL = 0 && 0 <= o91 && 1 <= i67 && 1 <= i66 && 0 < o90
langle_init_rangle_Load_322(o90, o91, i66, i67, i4, NULL, env, static) -{1,1}> langle_init_rangle_FieldAccess_324(o90, o91, i66, i67, i4, NULL, env, static) :|: NULL = 0 && 0 <= o91 && 1 <= i67 && 1 <= i66 && 0 < o90
langle_init_rangle_FieldAccess_324(o90, o91, i66, i67, i4, NULL, env, static) -{1,1}> langle_init_rangle_Return_329(o90', i66, i67, i4, o91, env, static) :|: NULL = 0 && 0 <= o91 && 0 < o90' && 1 <= i67 && o90' <= o90 + o91 && 1 <= i66 && o90' = o90 + o91 && 0 < o90
langle_init_rangle_Return_329(o90, i66, i67, i4, o91, env, static) -{1,1}> createIntList_Store_331(o90, i66, i67, i4, o91, env, static) :|: 0 <= o91 && 1 <= i67 && 1 <= i66 && 0 < o90
createIntList_Store_331(o90, i66, i67, i4, o91, env, static) -{1,1}> createIntList_Inc_333(i66, o90, i67, i4, o91, env, static) :|: 0 <= o91 && 1 <= i67 && 1 <= i66 && 0 < o90
createIntList_Inc_333(i66, o90, i67, i4, o91, env, static) -{1,1}> createIntList_JMP_335(i73, o90, i67, i4, o91, i66, env, static) :|: i66 + -1 = i73 && 0 <= o91 && 1 <= i67 && 1 <= i66 && 0 < o90 && 0 <= i73
createIntList_JMP_335(i73, o90, i67, i4, o91, i66, env, static) -{1,1}> createIntList_Load_338(i73, o90, i67, i4, o91, i66, env, static) :|: 0 <= o91 && 1 <= i67 && 1 <= i66 && 0 < o90 && 0 <= i73
createIntList_Load_338(i73, o90, i67, i4, o91, i66, env, static) -{1,1}> createIntList_LE_346(i73, o90, i67, i4, o91, i66, env, static) :|: 0 <= o91 && 1 <= i67 && 1 <= i66 && 0 < o90 && 0 <= i73

obtained
createIntList_LE_346(i80, o90, i67, i4, o91, i81, env, static) -{9,9}> langle_init_rangle_Load_313(1, i80, o90, i67, i4, 0, 0, env, static) :|: 1 <= i80 && 0 < 1 && 0 <= o91 && 0 < o90 && 2 <= i81 && 1 <= i67 && 0 <= o90 && 0 <= i80 && 0 < i80 && 1 <= i81
by chaining
createIntList_LE_346(i80, o90, i67, i4, o91, i81, env, static) -{0,0}> createIntList_LE_350(i80, o90, i67, i4, o91, i81, env, static) :|: 1 <= i80 && 0 <= o91 && 2 <= i81 && 1 <= i67 && 0 <= i80 && 0 < o90 && 1 <= i81
createIntList_LE_350(i80, o90, i67, i4, o91, i81, env, static) -{1,1}> createIntList_New_356(i80, o90, i67, i4, o91, i81, env, static) :|: 1 <= i80 && 0 <= o91 && 2 <= i81 && 1 <= i67 && 0 < i80 && 0 < o90
createIntList_New_356(i80, o90, i67, i4, o91, i81, env, static) -{1,1}> createIntList_Duplicate_362(o111, i80, o90, i67, i4, NULL, iconst_0, o91, i81, env, static) :|: NULL = 0 && 1 <= i80 && o111 = 1 && 0 <= o91 && 2 <= i81 && 1 <= i67 && iconst_0 = 0 && 0 < o90 && 0 < o111
createIntList_Duplicate_362(o111, i80, o90, i67, i4, NULL, iconst_0, o91, i81, env, static) -{1,1}> createIntList_Load_365(o111, i80, o90, i67, i4, NULL, iconst_0, o91, i81, env, static) :|: NULL = 0 && 1 <= i80 && 0 <= o91 && 2 <= i81 && 1 <= i67 && iconst_0 = 0 && 0 < o90 && 0 < o111
createIntList_Load_365(o111, i80, o90, i67, i4, NULL, iconst_0, o91, i81, env, static) -{1,1}> createIntList_Load_367(o111, i80, o90, i67, i4, NULL, iconst_0, o91, i81, env, static) :|: NULL = 0 && 1 <= i80 && 0 <= o91 && 2 <= i81 && 1 <= i67 && iconst_0 = 0 && 0 < o90 && 0 < o111
createIntList_Load_367(o111, i80, o90, i67, i4, NULL, iconst_0, o91, i81, env, static) -{1,1}> createIntList_InvokeMethod_372(o111, i80, o90, i67, i4, NULL, iconst_0, o91, i81, env, static) :|: NULL = 0 && 1 <= i80 && 0 <= o91 && 2 <= i81 && 1 <= i67 && iconst_0 = 0 && 0 < o90 && 0 < o111
createIntList_InvokeMethod_372(o111, i80, o90, i67, i4, NULL, iconst_0, o91, i81, env, static) -{1,1}> langle_init_rangle_Load_376(o111, i80, o90, i67, i4, NULL, iconst_0, o91, i81, env, static) :|: NULL = 0 && 1 <= i80 && 0 <= o91 && 2 <= i81 && 1 <= i67 && iconst_0 = 0 && 0 < o90 && 0 < o111
langle_init_rangle_Load_376(o111, i80, o90, i67, i4, NULL, iconst_0, o91, i81, env, static) -{1,1}> langle_init_rangle_InvokeMethod_382(o111, i80, o90, i67, i4, NULL, iconst_0, o91, i81, env, static) :|: NULL = 0 && 1 <= i80 && 0 <= o91 && 2 <= i81 && 1 <= i67 && iconst_0 = 0 && 0 < o90 && 0 < o111
langle_init_rangle_InvokeMethod_382(o111, i80, o90, i67, i4, NULL, iconst_0, o91, i81, env, static) -{1,1}> langle_init_rangle_Load_384(o111, i80, o90, i67, i4, NULL, iconst_0, o91, i81, env, static) :|: NULL = 0 && 1 <= i80 && 0 <= o91 && 2 <= i81 && 1 <= i67 && iconst_0 = 0 && 0 < o90 && 0 < o111
langle_init_rangle_Load_384(o111, i80, o90, i67, i4, NULL, iconst_0, o91, i81, env, static) -{1,1}> langle_init_rangle_Load_388(o111, i80, o90, i67, i4, NULL, iconst_0, o91, i81, env, static) :|: NULL = 0 && 1 <= i80 && 0 <= o91 && 2 <= i81 && 1 <= i67 && iconst_0 = 0 && 0 < o90 && 0 < o111
langle_init_rangle_Load_388(o111, i80, o90, i67, i4, NULL, iconst_0, o91, i81, env, static) -{0,0}> langle_init_rangle_Load_313(o111, i80, o90, i67, i4, NULL, iconst_0, env, static) :|: NULL = 0 && 1 <= i80 && 0 <= o91 && 2 <= i81 && 1 <= i67 && 0 <= o90 && iconst_0 = 0 && 0 < o90 && 0 < o111

obtained
createIntList_LE_346(0, o90, i67, i4, o91, i66, env, static) -{6,6}> main_Load_653(i67, i4, o90, 0, env, static) :|: 0 < o90 && 0 <= 0 && 0 <= 1 && 1 <= i67 && 0 <= o90 && 0 <= o91 && 1 <= i66 && 0 <= 2 && 0 <= i66
by chaining
createIntList_LE_346(iconst_0, o90, i67, i4, o91, i66, env, static) -{0,0}> createIntList_LE_348(iconst_0, o90, i67, i4, o91, i66, env, static) :|: 0 <= o91 && 0 <= iconst_0 && 1 <= i67 && 1 <= i66 && iconst_0 = 0 && 0 < o90
createIntList_LE_348(iconst_0, o90, i67, i4, o91, i66, env, static) -{1,1}> createIntList_Load_353(o90, i67, i4, o91, i66, env, static) :|: 0 <= o91 && iconst_0 <= 0 && 1 <= i67 && 1 <= i66 && iconst_0 = 0 && 0 < o90
createIntList_Load_353(o90, i67, i4, o91, i66, env, static) -{1,1}> createIntList_Return_359(o90, i67, i4, o91, i66, env, static) :|: 0 <= o91 && 1 <= i67 && 1 <= i66 && 0 < o90
createIntList_Return_359(o90, i67, i4, o91, i66, env, static) -{1,1}> main_Store_364(i67, i4, o90, o91, i66, env, static) :|: 0 <= o91 && 1 <= i67 && 1 <= i66 && 0 < o90
main_Store_364(i67, i4, o90, o91, i66, env, static) -{1,1}> main_ConstantStackPush_366(i67, i4, o90, o91, i66, env, static) :|: 0 <= o91 && 1 <= i67 && 1 <= i66 && 0 < o90
main_ConstantStackPush_366(i67, i4, o90, o91, i66, env, static) -{1,1}> main_Store_369(i67, i4, iconst_0, o90, o91, i66, env, static) :|: 0 <= o91 && 1 <= i67 && 1 <= i66 && iconst_0 = 0 && 0 < o90
main_Store_369(i67, i4, iconst_0, o90, o91, i66, env, static) -{1,1}> main_Load_375(i67, i4, o90, iconst_0, o91, i66, env, static) :|: 0 <= o91 && 1 <= i67 && 1 <= i66 && iconst_0 = 0 && 0 < o90
main_Load_375(i67, i4, o90, iconst_0, o91, i66, env, static) -{0,0}> main_Load_437(i67, i4, o90, iconst_0, o91, i66, env, static) :|: 0 <= o91 && 0 <= i66 && 1 <= i67 && 0 <= iconst_0 && 1 <= i66 && iconst_0 <= 1 && iconst_0 = 0 && 0 < o90
main_Load_437(i67, i4, o139, i97, o140, i96, env, static) -{0,0}> main_Load_487(i67, i4, o139, i97, env, static) :|: 0 <= o140 && 0 < o139 && 1 <= i67 && 0 <= i97 && 0 <= o139 && 0 <= i96 && i97 <= 1
main_Load_487(i67, i4, o156, i97, env, static) -{0,0}> main_Load_546(i67, i4, o156, i97, env, static) :|: 1 <= i67 && 0 <= i97 && 0 <= o156 && i97 <= 1 && i97 <= 2
main_Load_546(i67, i4, o176, i118, env, static) -{0,0}> main_Load_601(i67, i4, o176, i118, env, static) :|: 1 <= i67 && 0 <= o176 && i118 <= 2 && 0 <= i118
main_Load_601(i67, i4, o195, i127, env, static) -{0,0}> main_Load_653(i67, i4, o195, i127, env, static) :|: 1 <= i67 && 0 <= o195 && 0 <= i127

obtained
main_NULL_656(i67, i4, o226, i137, env, static) -{3,3}> main_GT_671(i67, i4, i142', o226, i137, o229', env, static) :|: 0 <= o229' && 0 < o226 && o229' < o226 && 1 <= i67 && -1 * o226 < i142' && 0 <= o226 && i142' < o226
by chaining
main_NULL_656(i67, i4, o226, i137, env, static) -{0,0}> main_NULL_658(i67, i4, o226, i137, env, static) :|: 0 <= o226 && 1 <= i67 && 0 < o226
main_NULL_658(i67, i4, o226, i137, env, static) -{1,1}> main_Load_661(i67, i4, o226, i137, env, static) :|: 1 <= i67 && 0 < o226
main_Load_661(i67, i4, o226, i137, env, static) -{1,1}> main_FieldAccess_665(i67, i4, o226, i137, env, static) :|: 1 <= i67 && 0 < o226
main_FieldAccess_665(i67, i4, o228, i137, env, static) -{0,0}> main_FieldAccess_668(i67, i4, o228, i137, o229, i142, env, static) :|: 0 <= o229 && 1 <= i67 && o229 < o228 && -1 * o228 < i142 && 0 < o228 && i142 < o228
main_FieldAccess_668(i67, i4, o228, i137, o229, i142, env, static) -{1,1}> main_GT_671(i67, i4, i142, o228, i137, o229, env, static) :|: 0 <= o229 && 1 <= i67 && 0 < o228

obtained
main_GT_671(i67, i4, i144, o228, i137, o229, env, static) -{9,9}> main_Load_653(i67, i4, o228''', i148', env, static) :|: 1 <= i144 && 0 <= o228''' && o228''' <= o228 + i146' && 0 < o228''' && i137 + 1 = i148' && 0 <= i146' && i144 - 1 = i146' && 0 <= o229 && 1 <= i67 && o228''' < o228 && 0 < i144 && 0 < o228
by chaining
main_GT_671(i67, i4, i144, o228, i137, o229, env, static) -{0,0}> main_GT_673(i67, i4, i144, o228, i137, o229, env, static) :|: 1 <= i144 && 0 <= o229 && 1 <= i67 && 0 < o228
main_GT_673(i67, i4, i144, o228, i137, o229, env, static) -{1,1}> main_Load_677(i67, i4, o228, i137, o229, i144, env, static) :|: 1 <= i144 && 0 <= o229 && 1 <= i67 && 0 < i144 && 0 < o228
main_Load_677(i67, i4, o228, i137, o229, i144, env, static) -{1,1}> main_Duplicate_680(i67, i4, o228, i137, o229, i144, env, static) :|: 1 <= i144 && 0 <= o229 && 1 <= i67 && 0 < o228
main_Duplicate_680(i67, i4, o228, i137, o229, i144, env, static) -{1,1}> main_FieldAccess_684(i67, i4, o228, i137, o229, i144, env, static) :|: 1 <= i144 && 0 <= o229 && 1 <= i67 && 0 < o228
main_FieldAccess_684(i67, i4, o228, i137, o229, i144, env, static) -{1,1}> main_ConstantStackPush_687(i67, i4, o228, i144, i137, o229, env, static) :|: 1 <= i144 && 0 <= o229 && 1 <= i67 && 0 < o228
main_ConstantStackPush_687(i67, i4, o228, i144, i137, o229, env, static) -{1,1}> main_IntArithmetic_691(i67, i4, o228, i144, iconst_1, i137, o229, env, static) :|: 1 <= i144 && 0 <= o229 && 1 <= i67 && iconst_1 = 1 && 0 < o228
main_IntArithmetic_691(i67, i4, o228, i144, iconst_1, i137, o229, env, static) -{1,1}> main_FieldAccess_697(i67, i4, o228, i146, i137, o229, i144, env, static) :|: 1 <= i144 && 0 <= o229 && 1 <= i67 && iconst_1 = 1 && 0 <= i146 && i144 - iconst_1 = i146 && 0 < o228
main_FieldAccess_697(i67, i4, o228, i146, i137, o229, i144, env, static) -{1,1}> main_Inc_710(i67, i4, o228', i137, o229, i146, env, static) :|: 0 < o228' && 1 <= i144 && 0 <= o229 && 1 <= i67 && o228' <= o228 + i146 && 0 <= i146 && o228' < o228 && 0 < o228
main_Inc_710(i67, i4, o228, i137, o229, i146, env, static) -{1,1}> main_JMP_715(i67, i4, o228, i148, o229, i146, env, static) :|: i137 + 1 = i148 && 0 <= o229 && 1 <= i67 && 0 <= i146 && 0 < o228
main_JMP_715(i67, i4, o228, i148, o229, i146, env, static) -{1,1}> main_Load_722(i67, i4, o228, i148, o229, i146, env, static) :|: 0 <= o229 && 1 <= i67 && 0 <= i146 && 0 < o228
main_Load_722(i67, i4, o228, i148, o229, i146, env, static) -{0,0}> main_Load_653(i67, i4, o228, i148, env, static) :|: 0 <= o229 && 1 <= i67 && 0 <= i146 && 0 < o228 && 0 <= o228

obtained
main_GT_671(i67, i4, i143, o228, i137, o229, env, static) -{5,5}> main_NULL_689(i67, i4, o229, i137, env, static) :|: 0 < o228 && 0 <= o229 && 1 <= i67 && i143 <= 0
by chaining
main_GT_671(i67, i4, i143, o228, i137, o229, env, static) -{0,0}> main_GT_672(i67, i4, i143, o228, i137, o229, env, static) :|: 0 <= o229 && 1 <= i67 && i143 <= 0 && 0 < o228
main_GT_672(i67, i4, i143, o228, i137, o229, env, static) -{1,1}> main_Load_675(i67, i4, o228, i137, o229, i143, env, static) :|: 0 <= o229 && 1 <= i67 && i143 <= 0 && 0 < o228
main_Load_675(i67, i4, o228, i137, o229, i143, env, static) -{1,1}> main_FieldAccess_679(i67, i4, o228, i137, o229, i143, env, static) :|: 0 <= o229 && 1 <= i67 && i143 <= 0 && 0 < o228
main_FieldAccess_679(i67, i4, o228, i137, o229, i143, env, static) -{1,1}> main_Store_682(i67, i4, o229, i137, env, static) :|: 0 <= o229 && 1 <= i67 && i143 <= 0 && 0 < o228
main_Store_682(i67, i4, o229, i137, env, static) -{1,1}> main_Load_685(i67, i4, o229, i137, env, static) :|: 0 <= o229 && 1 <= i67
main_Load_685(i67, i4, o229, i137, env, static) -{1,1}> main_NULL_689(i67, i4, o229, i137, env, static) :|: 0 <= o229 && 1 <= i67

obtained
main_NULL_689(i67, i4, 0, i137, env, static) -{1,1}> main_Load_653(i67, i4, 0, i137, env, static) :|: 0 <= 0 && 1 <= i67
by chaining
main_NULL_689(i67, i4, NULL, i137, env, static) -{0,0}> main_NULL_694(i67, i4, NULL, i137, env, static) :|: NULL = 0 && 1 <= i67 && 0 <= NULL
main_NULL_694(i67, i4, NULL, i137, env, static) -{1,1}> main_Load_707(i67, i4, NULL, i137, env, static) :|: NULL = 0 && 1 <= i67
main_Load_707(i67, i4, NULL, i137, env, static) -{0,0}> main_Load_653(i67, i4, NULL, i137, env, static) :|: NULL = 0 && 1 <= i67 && 0 <= NULL

obtained
main_NULL_689(i67, i4, o230, i137, env, static) -{6,6}> main_Load_653(i67, i4, o230, i150', env, static) :|: 0 <= o230 && 1 <= i67 && 0 < o230 && i137 * i4 = i150'
by chaining
main_NULL_689(i67, i4, o230, i137, env, static) -{0,0}> main_NULL_693(i67, i4, o230, i137, env, static) :|: 0 < o230 && 1 <= i67 && 0 <= o230
main_NULL_693(i67, i4, o230, i137, env, static) -{1,1}> main_Load_699(i67, i4, o230, i137, env, static) :|: 0 < o230 && 1 <= i67
main_Load_699(i67, i4, o230, i137, env, static) -{1,1}> main_Load_712(i67, i4, i137, o230, env, static) :|: 0 < o230 && 1 <= i67
main_Load_712(i67, i4, i137, o230, env, static) -{1,1}> main_IntArithmetic_717(i67, i4, i137, o230, env, static) :|: 0 < o230 && 1 <= i67
main_IntArithmetic_717(i67, i4, i137, o230, env, static) -{1,1}> main_Store_724(i67, i4, i150, o230, env, static) :|: 0 < o230 && 1 <= i67 && i137 * i4 = i150
main_Store_724(i67, i4, i150, o230, env, static) -{1,1}> main_JMP_726(i67, i4, o230, i150, env, static) :|: 0 < o230 && 1 <= i67
main_JMP_726(i67, i4, o230, i150, env, static) -{1,1}> main_Load_732(i67, i4, o230, i150, env, static) :|: 0 < o230 && 1 <= i67
main_Load_732(i67, i4, o230, i150, env, static) -{0,0}> main_Load_653(i67, i4, o230, i150, env, static) :|: 0 < o230 && 1 <= i67 && 0 <= o230

(8) Obligation:

IntTrs with 13 rules
Start term: main_Load_1(#0, #1, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_Load_1(i2, i4, env, static) -{20,20}> createIntList_LE_62(i2, 0, i4, env, static'1) :|: 0 <= static'1 && 0 < 2 && 0 <= static && 0 <= 1 && 0 < 1 && static''' <= static + 2 && 0 <= static''' && 0 <= 2 && static'1 <= static''' + 1 && 0 >= 0
createIntList_LE_62(i11, NULL, i4, env, static) -{0,0}> createIntList_LE_63(i11, NULL, i4, env, static) :|: NULL = 0 && i11 <= 0
createIntList_LE_62(i12, 0, i4, env, static) -{9,9}> langle_init_rangle_Load_313(1, i12, 0, i12, i4, 0, 0, env, static) :|: 0 < i12 && 1 <= i12 && 0 < 1 && 0 <= 0
langle_init_rangle_Load_313(o90, i66, o91, i67, i4, 0, 0, env, static) -{10,10}> createIntList_LE_346(i73', o90'1, i67, i4, o91, i66, env, static) :|: o90 < o90''' && 0 <= i73' && 0 < o90 && 0 < o90'1 && o90'1 <= o90''' + o91 && 1 <= i66 && 1 <= i67 && 0 <= o91 && i66 + -1 = i73' && o90''' <= o90 + i66 && o90'1 = o90''' + o91 && 0 < o90'''
createIntList_LE_346(i80, o90, i67, i4, o91, i81, env, static) -{9,9}> langle_init_rangle_Load_313(1, i80, o90, i67, i4, 0, 0, env, static) :|: 1 <= i80 && 0 < 1 && 0 <= o91 && 0 < o90 && 2 <= i81 && 1 <= i67 && 0 <= o90 && 0 <= i80 && 0 < i80 && 1 <= i81
createIntList_LE_346(0, o90, i67, i4, o91, i66, env, static) -{6,6}> main_Load_653(i67, i4, o90, 0, env, static) :|: 0 < o90 && 0 <= 0 && 0 <= 1 && 1 <= i67 && 0 <= o90 && 0 <= o91 && 1 <= i66 && 0 <= 2 && 0 <= i66
main_Load_653(i67, i4, o217, i137, env, static) -{1,1}> main_NULL_656(i67, i4, o217, i137, env, static) :|: 1 <= i67 && 0 <= o217
main_NULL_656(i67, i4, NULL, i137, env, static) -{0,0}> main_NULL_659(i67, i4, NULL, i137, env, static) :|: NULL = 0 && 1 <= i67 && 0 <= NULL
main_NULL_656(i67, i4, o226, i137, env, static) -{3,3}> main_GT_671(i67, i4, i142', o226, i137, o229', env, static) :|: 0 <= o229' && 0 < o226 && o229' < o226 && 1 <= i67 && -1 * o226 < i142' && 0 <= o226 && i142' < o226
main_GT_671(i67, i4, i144, o228, i137, o229, env, static) -{9,9}> main_Load_653(i67, i4, o228''', i148', env, static) :|: 1 <= i144 && 0 <= o228''' && o228''' <= o228 + i146' && 0 < o228''' && i137 + 1 = i148' && 0 <= i146' && i144 - 1 = i146' && 0 <= o229 && 1 <= i67 && o228''' < o228 && 0 < i144 && 0 < o228
main_GT_671(i67, i4, i143, o228, i137, o229, env, static) -{5,5}> main_NULL_689(i67, i4, o229, i137, env, static) :|: 0 < o228 && 0 <= o229 && 1 <= i67 && i143 <= 0
main_NULL_689(i67, i4, 0, i137, env, static) -{1,1}> main_Load_653(i67, i4, 0, i137, env, static) :|: 0 <= 0 && 1 <= i67
main_NULL_689(i67, i4, o230, i137, env, static) -{6,6}> main_Load_653(i67, i4, o230, i150', env, static) :|: 0 <= o230 && 1 <= i67 && 0 < o230 && i137 * i4 = i150'

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

Moved arithmethic from lhss to constraints.

createIntList_LE_62(i12, 0, i4, env, static) -{9,9}> langle_init_rangle_Load_313(1, i12, 0, i12, i4, 0, 0, env, static) :|: 0 < i12 && 1 <= i12 && 0 < 1 && 0 <= 0
was transformed to
createIntList_LE_62(i12, x, i4, env, static) -{9,9}> langle_init_rangle_Load_313(1, i12, 0, i12, i4, 0, 0, env, static) :|: 0 < i12 && 1 <= i12 && 0 < 1 && 0 <= 0 && x = 0

main_NULL_689(i67, i4, 0, i137, env, static) -{1,1}> main_Load_653(i67, i4, 0, i137, env, static) :|: 0 <= 0 && 1 <= i67
was transformed to
main_NULL_689(i67, i4, x, i137, env, static) -{1,1}> main_Load_653(i67, i4, 0, i137, env, static) :|: 0 <= 0 && 1 <= i67 && x = 0

createIntList_LE_346(0, o90, i67, i4, o91, i66, env, static) -{6,6}> main_Load_653(i67, i4, o90, 0, env, static) :|: 0 < o90 && 0 <= 0 && 0 <= 1 && 1 <= i67 && 0 <= o90 && 0 <= o91 && 1 <= i66 && 0 <= 2 && 0 <= i66
was transformed to
createIntList_LE_346(x, o90, i67, i4, o91, i66, env, static) -{6,6}> main_Load_653(i67, i4, o90, 0, env, static) :|: 0 < o90 && 0 <= 0 && 0 <= 1 && 1 <= i67 && 0 <= o90 && 0 <= o91 && 1 <= i66 && 0 <= 2 && 0 <= i66 && x = 0

langle_init_rangle_Load_313(o90, i66, o91, i67, i4, 0, 0, env, static) -{10,10}> createIntList_LE_346(i73', o90'1, i67, i4, o91, i66, env, static) :|: o90 < o90''' && 0 <= i73' && 0 < o90 && 0 < o90'1 && o90'1 <= o90''' + o91 && 1 <= i66 && 1 <= i67 && 0 <= o91 && i66 + -1 = i73' && o90''' <= o90 + i66 && o90'1 = o90''' + o91 && 0 < o90'''
was transformed to
langle_init_rangle_Load_313(o90, i66, o91, i67, i4, x, x', env, static) -{10,10}> createIntList_LE_346(i73', o90'1, i67, i4, o91, i66, env, static) :|: o90 < o90''' && 0 <= i73' && 0 < o90 && 0 < o90'1 && o90'1 <= o90''' + o91 && 1 <= i66 && 1 <= i67 && 0 <= o91 && i66 + -1 = i73' && o90''' <= o90 + i66 && o90'1 = o90''' + o91 && 0 < o90''' && x = 0 && x' = 0

(10) Obligation:

IntTrs with 13 rules
Start term: main_Load_1(#0, #1, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_GT_671(i67, i4, i143, o228, i137, o229, env, static) -{5,5}> main_NULL_689(i67, i4, o229, i137, env, static) :|: 0 < o228 && 0 <= o229 && 1 <= i67 && i143 <= 0
main_Load_653(i67, i4, o217, i137, env, static) -{1,1}> main_NULL_656(i67, i4, o217, i137, env, static) :|: 1 <= i67 && 0 <= o217
createIntList_LE_62(i12, x, i4, env, static) -{9,9}> langle_init_rangle_Load_313(1, i12, 0, i12, i4, 0, 0, env, static) :|: 0 < i12 && 1 <= i12 && 0 < 1 && 0 <= 0 && x = 0
main_NULL_656(i67, i4, o226, i137, env, static) -{3,3}> main_GT_671(i67, i4, i142', o226, i137, o229', env, static) :|: 0 <= o229' && 0 < o226 && o229' < o226 && 1 <= i67 && -1 * o226 < i142' && 0 <= o226 && i142' < o226
main_GT_671(i67, i4, i144, o228, i137, o229, env, static) -{9,9}> main_Load_653(i67, i4, o228''', i148', env, static) :|: 1 <= i144 && 0 <= o228''' && o228''' <= o228 + i146' && 0 < o228''' && i137 + 1 = i148' && 0 <= i146' && i144 - 1 = i146' && 0 <= o229 && 1 <= i67 && o228''' < o228 && 0 < i144 && 0 < o228
main_NULL_689(i67, i4, x, i137, env, static) -{1,1}> main_Load_653(i67, i4, 0, i137, env, static) :|: 0 <= 0 && 1 <= i67 && x = 0
main_NULL_656(i67, i4, NULL, i137, env, static) -{0,0}> main_NULL_659(i67, i4, NULL, i137, env, static) :|: NULL = 0 && 1 <= i67 && 0 <= NULL
createIntList_LE_346(x, o90, i67, i4, o91, i66, env, static) -{6,6}> main_Load_653(i67, i4, o90, 0, env, static) :|: 0 < o90 && 0 <= 0 && 0 <= 1 && 1 <= i67 && 0 <= o90 && 0 <= o91 && 1 <= i66 && 0 <= 2 && 0 <= i66 && x = 0
createIntList_LE_346(i80, o90, i67, i4, o91, i81, env, static) -{9,9}> langle_init_rangle_Load_313(1, i80, o90, i67, i4, 0, 0, env, static) :|: 1 <= i80 && 0 < 1 && 0 <= o91 && 0 < o90 && 2 <= i81 && 1 <= i67 && 0 <= o90 && 0 <= i80 && 0 < i80 && 1 <= i81
langle_init_rangle_Load_313(o90, i66, o91, i67, i4, x, x', env, static) -{10,10}> createIntList_LE_346(i73', o90'1, i67, i4, o91, i66, env, static) :|: o90 < o90''' && 0 <= i73' && 0 < o90 && 0 < o90'1 && o90'1 <= o90''' + o91 && 1 <= i66 && 1 <= i67 && 0 <= o91 && i66 + -1 = i73' && o90''' <= o90 + i66 && o90'1 = o90''' + o91 && 0 < o90''' && x = 0 && x' = 0
main_Load_1(i2, i4, env, static) -{20,20}> createIntList_LE_62(i2, 0, i4, env, static'1) :|: 0 <= static'1 && 0 < 2 && 0 <= static && 0 <= 1 && 0 < 1 && static''' <= static + 2 && 0 <= static''' && 0 <= 2 && static'1 <= static''' + 1 && 0 >= 0
createIntList_LE_62(i11, NULL, i4, env, static) -{0,0}> createIntList_LE_63(i11, NULL, i4, env, static) :|: NULL = 0 && i11 <= 0
main_NULL_689(i67, i4, o230, i137, env, static) -{6,6}> main_Load_653(i67, i4, o230, i150', env, static) :|: 0 <= o230 && 1 <= i67 && 0 < o230 && i137 * i4 = i150'

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

Moved arithmethic from constraints to rhss.

langle_init_rangle_Load_313(o90, i66, o91, i67, i4, x, x', env, static) -{10,10}> createIntList_LE_346(i73', o90'1, i67, i4, o91, i66, env, static) :|: o90 < o90''' && 0 <= i73' && 0 < o90 && 0 < o90'1 && o90'1 <= o90''' + o91 && 1 <= i66 && 1 <= i67 && 0 <= o91 && i66 + -1 = i73' && o90''' <= o90 + i66 && o90'1 = o90''' + o91 && 0 < o90''' && x = 0 && x' = 0
was transformed to
langle_init_rangle_Load_313(o90, i66, o91, i67, i4, x, x', env, static) -{10,10}> createIntList_LE_346(i66 + -1, o90''' + o91, i67, i4, o91, i66, env, static) :|: o90 < o90''' && 0 <= i73' && 0 < o90 && 0 < o90'1 && o90'1 <= o90''' + o91 && 1 <= i66 && 1 <= i67 && 0 <= o91 && i66 + -1 = i73' && o90''' <= o90 + i66 && o90'1 = o90''' + o91 && 0 < o90''' && x = 0 && x' = 0

main_GT_671(i67, i4, i144, o228, i137, o229, env, static) -{9,9}> main_Load_653(i67, i4, o228''', i148', env, static) :|: 1 <= i144 && 0 <= o228''' && o228''' <= o228 + i146' && 0 < o228''' && i137 + 1 = i148' && 0 <= i146' && i144 - 1 = i146' && 0 <= o229 && 1 <= i67 && o228''' < o228 && 0 < i144 && 0 < o228
was transformed to
main_GT_671(i67, i4, i144, o228, i137, o229, env, static) -{9,9}> main_Load_653(i67, i4, o228''', i137 + 1, env, static) :|: 1 <= i144 && 0 <= o228''' && o228''' <= o228 + i146' && 0 < o228''' && i137 + 1 = i148' && 0 <= i146' && i144 - 1 = i146' && 0 <= o229 && 1 <= i67 && o228''' < o228 && 0 < i144 && 0 < o228

main_NULL_656(i67, i4, NULL, i137, env, static) -{0,0}> main_NULL_659(i67, i4, NULL, i137, env, static) :|: NULL = 0 && 1 <= i67 && 0 <= NULL
was transformed to
main_NULL_656(i67, i4, NULL, i137, env, static) -{0,0}> main_NULL_659(i67, i4, 0, i137, env, static) :|: NULL = 0 && 1 <= i67 && 0 <= NULL

createIntList_LE_62(i11, NULL, i4, env, static) -{0,0}> createIntList_LE_63(i11, NULL, i4, env, static) :|: NULL = 0 && i11 <= 0
was transformed to
createIntList_LE_62(i11, NULL, i4, env, static) -{0,0}> createIntList_LE_63(i11, 0, i4, env, static) :|: NULL = 0 && i11 <= 0

main_NULL_689(i67, i4, o230, i137, env, static) -{6,6}> main_Load_653(i67, i4, o230, i150', env, static) :|: 0 <= o230 && 1 <= i67 && 0 < o230 && i137 * i4 = i150'
was transformed to
main_NULL_689(i67, i4, o230, i137, env, static) -{6,6}> main_Load_653(i67, i4, o230, i137 * i4, env, static) :|: 0 <= o230 && 1 <= i67 && 0 < o230 && i137 * i4 = i150'

(12) Obligation:

IntTrs with 13 rules
Start term: main_Load_1(#0, #1, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
langle_init_rangle_Load_313(o90, i66, o91, i67, i4, x, x', env, static) -{10,10}> createIntList_LE_346(i66 + -1, o90''' + o91, i67, i4, o91, i66, env, static) :|: o90 < o90''' && 0 <= i73' && 0 < o90 && 0 < o90'1 && o90'1 <= o90''' + o91 && 1 <= i66 && 1 <= i67 && 0 <= o91 && i66 + -1 = i73' && o90''' <= o90 + i66 && o90'1 = o90''' + o91 && 0 < o90''' && x = 0 && x' = 0
main_GT_671(i67, i4, i143, o228, i137, o229, env, static) -{5,5}> main_NULL_689(i67, i4, o229, i137, env, static) :|: 0 < o228 && 0 <= o229 && 1 <= i67 && i143 <= 0
main_Load_653(i67, i4, o217, i137, env, static) -{1,1}> main_NULL_656(i67, i4, o217, i137, env, static) :|: 1 <= i67 && 0 <= o217
main_NULL_656(i67, i4, o226, i137, env, static) -{3,3}> main_GT_671(i67, i4, i142', o226, i137, o229', env, static) :|: 0 <= o229' && 0 < o226 && o229' < o226 && 1 <= i67 && -1 * o226 < i142' && 0 <= o226 && i142' < o226
main_GT_671(i67, i4, i144, o228, i137, o229, env, static) -{9,9}> main_Load_653(i67, i4, o228''', i137 + 1, env, static) :|: 1 <= i144 && 0 <= o228''' && o228''' <= o228 + i146' && 0 < o228''' && i137 + 1 = i148' && 0 <= i146' && i144 - 1 = i146' && 0 <= o229 && 1 <= i67 && o228''' < o228 && 0 < i144 && 0 < o228
main_NULL_689(i67, i4, x, i137, env, static) -{1,1}> main_Load_653(i67, i4, 0, i137, env, static) :|: 0 <= 0 && 1 <= i67 && x = 0
createIntList_LE_346(i80, o90, i67, i4, o91, i81, env, static) -{9,9}> langle_init_rangle_Load_313(1, i80, o90, i67, i4, 0, 0, env, static) :|: 1 <= i80 && 0 < 1 && 0 <= o91 && 0 < o90 && 2 <= i81 && 1 <= i67 && 0 <= o90 && 0 <= i80 && 0 < i80 && 1 <= i81
main_NULL_656(i67, i4, NULL, i137, env, static) -{0,0}> main_NULL_659(i67, i4, 0, i137, env, static) :|: NULL = 0 && 1 <= i67 && 0 <= NULL
createIntList_LE_62(i12, x, i4, env, static) -{9,9}> langle_init_rangle_Load_313(1, i12, 0, i12, i4, 0, 0, env, static) :|: 0 < i12 && 1 <= i12 && 0 < 1 && 0 <= 0 && x = 0
main_Load_1(i2, i4, env, static) -{20,20}> createIntList_LE_62(i2, 0, i4, env, static'1) :|: 0 <= static'1 && 0 < 2 && 0 <= static && 0 <= 1 && 0 < 1 && static''' <= static + 2 && 0 <= static''' && 0 <= 2 && static'1 <= static''' + 1 && 0 >= 0
createIntList_LE_62(i11, NULL, i4, env, static) -{0,0}> createIntList_LE_63(i11, 0, i4, env, static) :|: NULL = 0 && i11 <= 0
createIntList_LE_346(x, o90, i67, i4, o91, i66, env, static) -{6,6}> main_Load_653(i67, i4, o90, 0, env, static) :|: 0 < o90 && 0 <= 0 && 0 <= 1 && 1 <= i67 && 0 <= o90 && 0 <= o91 && 1 <= i66 && 0 <= 2 && 0 <= i66 && x = 0
main_NULL_689(i67, i4, o230, i137, env, static) -{6,6}> main_Load_653(i67, i4, o230, i137 * i4, env, static) :|: 0 <= o230 && 1 <= i67 && 0 < o230 && i137 * i4 = i150'

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

Simplified expressions.

main_GT_671(i67, i4, i144, o228, i137, o229, env, static) -{9,9}> main_Load_653(i67, i4, o228''', i137 + 1, env, static) :|: 1 <= i144 && 0 <= o228''' && o228''' <= o228 + i146' && 0 < o228''' && i137 + 1 = i148' && 0 <= i146' && i144 - 1 = i146' && 0 <= o229 && 1 <= i67 && o228''' < o228 && 0 < i144 && 0 < o228
was transformed to
main_GT_671(i67, i4, i144, o228, i137, o229, env, static) -{9,9}> main_Load_653(i67, i4, o228''', i137 + 1, env, static) :|: 1 <= i144 && o228''' <= o228 + i146' && 0 < o228''' && i137 + 1 = i148' && 0 <= i146' && i144 - 1 = i146' && 0 <= o229 && 1 <= i67 && o228''' < o228 && 0 < i144 && 0 < o228

main_NULL_689(i67, i4, o230, i137, env, static) -{6,6}> main_Load_653(i67, i4, o230, i137 * i4, env, static) :|: 0 <= o230 && 1 <= i67 && 0 < o230 && i137 * i4 = i150'
was transformed to
main_NULL_689(i67, i4, o230, i137, env, static) -{6,6}> main_Load_653(i67, i4, o230, i137 * i4, env, static) :|: 1 <= i67 && 0 < o230 && i137 * i4 = i150'

main_NULL_656(i67, i4, o226, i137, env, static) -{3,3}> main_GT_671(i67, i4, i142', o226, i137, o229', env, static) :|: 0 <= o229' && 0 < o226 && o229' < o226 && 1 <= i67 && -1 * o226 < i142' && 0 <= o226 && i142' < o226
was transformed to
main_NULL_656(i67, i4, o226, i137, env, static) -{3,3}> main_GT_671(i67, i4, i142', o226, i137, o229', env, static) :|: 0 <= o229' && 0 < o226 && o229' < o226 && 1 <= i67 && -1 * o226 < i142' && i142' < o226

langle_init_rangle_Load_313(o90, i66, o91, i67, i4, x, x', env, static) -{10,10}> createIntList_LE_346(i66 + -1, o90''' + o91, i67, i4, o91, i66, env, static) :|: o90 < o90''' && 0 <= i73' && 0 < o90 && 0 < o90'1 && o90'1 <= o90''' + o91 && 1 <= i66 && 1 <= i67 && 0 <= o91 && i66 + -1 = i73' && o90''' <= o90 + i66 && o90'1 = o90''' + o91 && 0 < o90''' && x = 0 && x' = 0
was transformed to
langle_init_rangle_Load_313(o90, i66, o91, i67, i4, x, x', env, static) -{10,10}> createIntList_LE_346(i66 - 1, o90''' + o91, i67, i4, o91, i66, env, static) :|: o90 < o90''' && 0 <= i73' && 0 < o90 && 0 < o90'1 && 1 <= i66 && 1 <= i67 && 0 <= o91 && i66 - 1 = i73' && o90''' <= o90 + i66 && o90'1 = o90''' + o91 && 0 < o90''' && x = 0 && x' = 0

main_NULL_689(i67, i4, x, i137, env, static) -{1,1}> main_Load_653(i67, i4, 0, i137, env, static) :|: 0 <= 0 && 1 <= i67 && x = 0
was transformed to
main_NULL_689(i67, i4, x, i137, env, static) -{1,1}> main_Load_653(i67, i4, 0, i137, env, static) :|: 1 <= i67 && x = 0

createIntList_LE_62(i12, x, i4, env, static) -{9,9}> langle_init_rangle_Load_313(1, i12, 0, i12, i4, 0, 0, env, static) :|: 0 < i12 && 1 <= i12 && 0 < 1 && 0 <= 0 && x = 0
was transformed to
createIntList_LE_62(i12, x, i4, env, static) -{9,9}> langle_init_rangle_Load_313(1, i12, 0, i12, i4, 0, 0, env, static) :|: 0 < i12 && 1 <= i12 && x = 0

createIntList_LE_346(i80, o90, i67, i4, o91, i81, env, static) -{9,9}> langle_init_rangle_Load_313(1, i80, o90, i67, i4, 0, 0, env, static) :|: 1 <= i80 && 0 < 1 && 0 <= o91 && 0 < o90 && 2 <= i81 && 1 <= i67 && 0 <= o90 && 0 <= i80 && 0 < i80 && 1 <= i81
was transformed to
createIntList_LE_346(i80, o90, i67, i4, o91, i81, env, static) -{9,9}> langle_init_rangle_Load_313(1, i80, o90, i67, i4, 0, 0, env, static) :|: 1 <= i80 && 0 <= o91 && 0 < o90 && 2 <= i81 && 1 <= i67 && 0 < i80 && 1 <= i81

main_Load_1(i2, i4, env, static) -{20,20}> createIntList_LE_62(i2, 0, i4, env, static'1) :|: 0 <= static'1 && 0 < 2 && 0 <= static && 0 <= 1 && 0 < 1 && static''' <= static + 2 && 0 <= static''' && 0 <= 2 && static'1 <= static''' + 1 && 0 >= 0
was transformed to
main_Load_1(i2, i4, env, static) -{20,20}> createIntList_LE_62(i2, 0, i4, env, static'1) :|: 0 <= static'1 && 0 <= static && static''' <= static + 2 && 0 <= static''' && static'1 <= static''' + 1

createIntList_LE_346(x, o90, i67, i4, o91, i66, env, static) -{6,6}> main_Load_653(i67, i4, o90, 0, env, static) :|: 0 < o90 && 0 <= 0 && 0 <= 1 && 1 <= i67 && 0 <= o90 && 0 <= o91 && 1 <= i66 && 0 <= 2 && 0 <= i66 && x = 0
was transformed to
createIntList_LE_346(x, o90, i67, i4, o91, i66, env, static) -{6,6}> main_Load_653(i67, i4, o90, 0, env, static) :|: 0 < o90 && 1 <= i67 && 0 <= o91 && 1 <= i66 && 0 <= i66 && x = 0

(14) Obligation:

IntTrs with 13 rules
Start term: main_Load_1(#0, #1, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_GT_671(i67, i4, i143, o228, i137, o229, env, static) -{5,5}> main_NULL_689(i67, i4, o229, i137, env, static) :|: 0 < o228 && 0 <= o229 && 1 <= i67 && i143 <= 0
main_Load_653(i67, i4, o217, i137, env, static) -{1,1}> main_NULL_656(i67, i4, o217, i137, env, static) :|: 1 <= i67 && 0 <= o217
main_NULL_689(i67, i4, o230, i137, env, static) -{6,6}> main_Load_653(i67, i4, o230, i137 * i4, env, static) :|: 1 <= i67 && 0 < o230 && i137 * i4 = i150'
main_Load_1(i2, i4, env, static) -{20,20}> createIntList_LE_62(i2, 0, i4, env, static'1) :|: 0 <= static'1 && 0 <= static && static''' <= static + 2 && 0 <= static''' && static'1 <= static''' + 1
main_NULL_689(i67, i4, x, i137, env, static) -{1,1}> main_Load_653(i67, i4, 0, i137, env, static) :|: 1 <= i67 && x = 0
main_GT_671(i67, i4, i144, o228, i137, o229, env, static) -{9,9}> main_Load_653(i67, i4, o228''', i137 + 1, env, static) :|: 1 <= i144 && o228''' <= o228 + i146' && 0 < o228''' && i137 + 1 = i148' && 0 <= i146' && i144 - 1 = i146' && 0 <= o229 && 1 <= i67 && o228''' < o228 && 0 < i144 && 0 < o228
main_NULL_656(i67, i4, NULL, i137, env, static) -{0,0}> main_NULL_659(i67, i4, 0, i137, env, static) :|: NULL = 0 && 1 <= i67 && 0 <= NULL
createIntList_LE_62(i12, x, i4, env, static) -{9,9}> langle_init_rangle_Load_313(1, i12, 0, i12, i4, 0, 0, env, static) :|: 0 < i12 && 1 <= i12 && x = 0
createIntList_LE_346(x, o90, i67, i4, o91, i66, env, static) -{6,6}> main_Load_653(i67, i4, o90, 0, env, static) :|: 0 < o90 && 1 <= i67 && 0 <= o91 && 1 <= i66 && 0 <= i66 && x = 0
langle_init_rangle_Load_313(o90, i66, o91, i67, i4, x, x', env, static) -{10,10}> createIntList_LE_346(i66 - 1, o90''' + o91, i67, i4, o91, i66, env, static) :|: o90 < o90''' && 0 <= i73' && 0 < o90 && 0 < o90'1 && 1 <= i66 && 1 <= i67 && 0 <= o91 && i66 - 1 = i73' && o90''' <= o90 + i66 && o90'1 = o90''' + o91 && 0 < o90''' && x = 0 && x' = 0
createIntList_LE_346(i80, o90, i67, i4, o91, i81, env, static) -{9,9}> langle_init_rangle_Load_313(1, i80, o90, i67, i4, 0, 0, env, static) :|: 1 <= i80 && 0 <= o91 && 0 < o90 && 2 <= i81 && 1 <= i67 && 0 < i80 && 1 <= i81
createIntList_LE_62(i11, NULL, i4, env, static) -{0,0}> createIntList_LE_63(i11, 0, i4, env, static) :|: NULL = 0 && i11 <= 0
main_NULL_656(i67, i4, o226, i137, env, static) -{3,3}> main_GT_671(i67, i4, i142', o226, i137, o229', env, static) :|: 0 <= o229' && 0 < o226 && o229' < o226 && 1 <= i67 && -1 * o226 < i142' && i142' < o226

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

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

(16) Obligation:

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

(18) Obligation:

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

Moved arithmethic from lhss to constraints.

(20) Obligation:

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

Moved arithmethic from constraints to rhss.

(22) Obligation:

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

Simplified expressions.

(24) Obligation:

IntTrs with 13 rules
Start term: main_Load_1(#0, #1, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_GT_671(i67, i4, i143, o228, i137, o229, env, static) -{5,5}> main_NULL_689(i67, i4, o229, i137, env, static) :|: 0 < o228 && 0 <= o229 && 1 <= i67 && i143 <= 0
main_Load_653(i67, i4, o217, i137, env, static) -{1,1}> main_NULL_656(i67, i4, o217, i137, env, static) :|: 1 <= i67 && 0 <= o217
main_NULL_689(i67, i4, o230, i137, env, static) -{6,6}> main_Load_653(i67, i4, o230, i137 * i4, env, static) :|: 1 <= i67 && 0 < o230 && i137 * i4 = i150'
main_Load_1(i2, i4, env, static) -{20,20}> createIntList_LE_62(i2, 0, i4, env, static'1) :|: 0 <= static'1 && 0 <= static && static''' <= static + 2 && 0 <= static''' && static'1 <= static''' + 1
main_NULL_689(i67, i4, x, i137, env, static) -{1,1}> main_Load_653(i67, i4, 0, i137, env, static) :|: 1 <= i67 && x = 0
main_GT_671(i67, i4, i144, o228, i137, o229, env, static) -{9,9}> main_Load_653(i67, i4, o228''', i137 + 1, env, static) :|: 1 <= i144 && o228''' <= o228 + i146' && 0 < o228''' && i137 + 1 = i148' && 0 <= i146' && i144 - 1 = i146' && 0 <= o229 && 1 <= i67 && o228''' < o228 && 0 < i144 && 0 < o228
main_NULL_656(i67, i4, NULL, i137, env, static) -{0,0}> main_NULL_659(i67, i4, 0, i137, env, static) :|: NULL = 0 && 1 <= i67 && 0 <= NULL
createIntList_LE_62(i12, x, i4, env, static) -{9,9}> langle_init_rangle_Load_313(1, i12, 0, i12, i4, 0, 0, env, static) :|: 0 < i12 && 1 <= i12 && x = 0
createIntList_LE_346(x, o90, i67, i4, o91, i66, env, static) -{6,6}> main_Load_653(i67, i4, o90, 0, env, static) :|: 0 < o90 && 1 <= i67 && 0 <= o91 && 1 <= i66 && 0 <= i66 && x = 0
langle_init_rangle_Load_313(o90, i66, o91, i67, i4, x, x', env, static) -{10,10}> createIntList_LE_346(i66 - 1, o90''' + o91, i67, i4, o91, i66, env, static) :|: o90 < o90''' && 0 <= i73' && 0 < o90 && 0 < o90'1 && 1 <= i66 && 1 <= i67 && 0 <= o91 && i66 - 1 = i73' && o90''' <= o90 + i66 && o90'1 = o90''' + o91 && 0 < o90''' && x = 0 && x' = 0
createIntList_LE_346(i80, o90, i67, i4, o91, i81, env, static) -{9,9}> langle_init_rangle_Load_313(1, i80, o90, i67, i4, 0, 0, env, static) :|: 1 <= i80 && 0 <= o91 && 0 < o90 && 2 <= i81 && 1 <= i67 && 0 < i80 && 1 <= i81
createIntList_LE_62(i11, NULL, i4, env, static) -{0,0}> createIntList_LE_63(i11, 0, i4, env, static) :|: NULL = 0 && i11 <= 0
main_NULL_656(i67, i4, o226, i137, env, static) -{3,3}> main_GT_671(i67, i4, i142', o226, i137, o229', env, static) :|: 0 <= o229' && 0 < o226 && o229' < o226 && 1 <= i67 && -1 * o226 < i142' && i142' < o226

(25) TerminationGraphToComplexityProof (BOTH CONCRETE BOUNDS(ID, ADD(11)) transformation)

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

(26) Obligation:

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

Used field analysis yielded the following read fields:
- IntList: [value, next]

Considered paths: all paths from start

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

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

(28) Obligation:

IntTrs with 107 rules
Start term: main_Load_1(#0, #1, env, static)
Considered paths: all paths from start
Rules:
main_Load_1(i2, i4, env, static) -{0,0}> main_Load_3(i2, i4, env, static) :|: 0 >= 0
main_Load_3(i2, i4, env, static) -{0,0}> langle_clinit_rangle_ConstantStackPush_5(i2, i4, env, static) :|: 0 >= 0
langle_clinit_rangle_ConstantStackPush_5(i2, i4, env, static) -{1,1}> langle_clinit_rangle_ArrayCreate_12(iconst_0, i2, i4, env, static) :|: iconst_0 = 0
langle_clinit_rangle_ArrayCreate_12(iconst_0, i2, i4, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_13(a2, i2, i4, iconst_0, env, static) :|: a2 = 2 && iconst_0 = 0 && 0 < a2
langle_clinit_rangle_FieldAccess_13(a2, i2, i4, iconst_0, env, static) -{1,1}> langle_clinit_rangle_New_14(i2, i4, env, static') :|: 0 <= a2 && iconst_0 = 0 && static' <= static + a2 && 0 <= static && 0 < a2
langle_clinit_rangle_New_14(i2, i4, env, static) -{0,0}> langle_clinit_rangle_New_16(i2, i4, env, static) :|: 0 >= 0
langle_clinit_rangle_New_16(i2, i4, env, static) -{0,0}> langle_clinit_rangle_New_17(i2, i4, env, static) :|: 0 <= static
langle_clinit_rangle_New_17(i2, i4, env, static) -{1,1}> langle_clinit_rangle_Duplicate_19(o2, i2, i4, env, static) :|: 0 < o2 && o2 = 1
langle_clinit_rangle_Duplicate_19(o2, i2, i4, env, static) -{1,1}> langle_clinit_rangle_ConstantStackPush_21(o2, i2, i4, env, static) :|: 0 < o2
langle_clinit_rangle_ConstantStackPush_21(o2, i2, i4, env, static) -{1,1}> langle_clinit_rangle_InvokeMethod_22(o2, NULL, i2, i4, env, static) :|: NULL = 0 && 0 < o2
langle_clinit_rangle_InvokeMethod_22(o2, NULL, i2, i4, env, static) -{1,1}> langle_init_rangle_Load_24(o2, i2, i4, env, static) :|: NULL = 0 && 0 < o2
langle_init_rangle_Load_24(o2, i2, i4, env, static) -{1,1}> langle_init_rangle_InvokeMethod_29(o2, i2, i4, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_29(o2, i2, i4, env, static) -{1,1}> langle_init_rangle_Load_30(o2, i2, i4, env, static) :|: 0 < o2
langle_init_rangle_Load_30(o2, i2, i4, env, static) -{1,1}> langle_init_rangle_InvokeMethod_33(o2, i2, i4, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_33(o2, i2, i4, env, static) -{1,1}> langle_init_rangle_Return_35(o2, i2, i4, env, static) :|: 0 < o2
langle_init_rangle_Return_35(o2, i2, i4, env, static) -{1,1}> langle_init_rangle_Return_38(o2, i2, i4, env, static) :|: 0 < o2
langle_init_rangle_Return_38(o2, i2, i4, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_39(o2, i2, i4, env, static) :|: 0 < o2
langle_clinit_rangle_FieldAccess_39(o2, i2, i4, env, static) -{1,1}> langle_clinit_rangle_Return_40(i2, i4, env, static') :|: 0 < o2 && 0 <= o2 && 0 <= static && static' <= static + o2
langle_clinit_rangle_Return_40(i2, i4, env, static) -{1,1}> main_Load_46(i2, i4, env, static) :|: 0 >= 0
main_Load_46(i2, i4, env, static) -{0,0}> main_Load_47(i2, i4, env, static) :|: 0 >= 0
main_Load_47(i2, i4, env, static) -{0,0}> main_Load_50(i2, i4, env, static) :|: 0 <= static
main_Load_50(i2, i4, env, static) -{0,0}> main_Load_51(i2, i4, env, static) :|: 0 >= 0
main_Load_51(i2, i4, env, static) -{0,0}> main_Load_52(i2, i4, env, static) :|: 0 >= 0
main_Load_52(i2, i4, env, static) -{1,1}> main_InvokeMethod_55(i2, i4, env, static) :|: 0 >= 0
main_InvokeMethod_55(i2, i4, env, static) -{0,0}> main_InvokeMethod_56(i2, i4, env, static) :|: 0 >= 0
main_InvokeMethod_56(i2, i4, env, static) -{1,1}> createIntList_ConstantStackPush_57(i2, i4, env, static) :|: 0 >= 0
createIntList_ConstantStackPush_57(i2, i4, env, static) -{1,1}> createIntList_Store_58(NULL, i2, i4, env, static) :|: NULL = 0
createIntList_Store_58(NULL, i2, i4, env, static) -{1,1}> createIntList_Load_59(i2, NULL, i4, env, static) :|: NULL = 0
createIntList_Load_59(i2, NULL, i4, env, static) -{1,1}> createIntList_LE_62(i2, NULL, i4, env, static) :|: NULL = 0
createIntList_LE_62(i12, NULL, i4, env, static) -{0,0}> createIntList_LE_64(i12, NULL, i4, env, static) :|: NULL = 0 && 1 <= i12
createIntList_LE_64(i12, NULL, i4, env, static) -{1,1}> createIntList_New_66(i12, NULL, i4, env, static) :|: NULL = 0 && 0 < i12 && 1 <= i12
createIntList_New_66(i12, NULL, i4, env, static) -{1,1}> createIntList_Duplicate_75(o3, i12, NULL, i4, iconst_0, env, static) :|: NULL = 0 && o3 = 1 && 0 < o3 && iconst_0 = 0 && 1 <= i12
createIntList_Duplicate_75(o3, i12, NULL, i4, iconst_0, env, static) -{1,1}> createIntList_Load_80(o3, i12, NULL, i4, iconst_0, env, static) :|: NULL = 0 && 0 < o3 && iconst_0 = 0 && 1 <= i12
createIntList_Load_80(o3, i12, NULL, i4, iconst_0, env, static) -{1,1}> createIntList_Load_84(o3, i12, NULL, i4, iconst_0, env, static) :|: NULL = 0 && 0 < o3 && iconst_0 = 0 && 1 <= i12
createIntList_Load_84(o3, i12, NULL, i4, iconst_0, env, static) -{1,1}> createIntList_InvokeMethod_89(o3, i12, NULL, i4, iconst_0, env, static) :|: NULL = 0 && 0 < o3 && iconst_0 = 0 && 1 <= i12
createIntList_InvokeMethod_89(o3, i12, NULL, i4, iconst_0, env, static) -{1,1}> langle_init_rangle_Load_92(o3, i12, NULL, i4, iconst_0, env, static) :|: NULL = 0 && 0 < o3 && iconst_0 = 0 && 1 <= i12
langle_init_rangle_Load_92(o3, i12, NULL, i4, iconst_0, env, static) -{1,1}> langle_init_rangle_InvokeMethod_98(o3, i12, NULL, i4, iconst_0, env, static) :|: NULL = 0 && 0 < o3 && iconst_0 = 0 && 1 <= i12
langle_init_rangle_InvokeMethod_98(o3, i12, NULL, i4, iconst_0, env, static) -{1,1}> langle_init_rangle_Load_100(o3, i12, NULL, i4, iconst_0, env, static) :|: NULL = 0 && 0 < o3 && iconst_0 = 0 && 1 <= i12
langle_init_rangle_Load_100(o3, i12, NULL, i4, iconst_0, env, static) -{1,1}> langle_init_rangle_Load_101(o3, i12, NULL, i4, iconst_0, env, static) :|: NULL = 0 && 0 < o3 && iconst_0 = 0 && 1 <= i12
langle_init_rangle_Load_101(o3, i12, NULL, i4, iconst_0, env, static) -{0,0}> langle_init_rangle_Load_313(o3, i12, NULL, i12, i4, NULL, iconst_0, env, static) :|: NULL = 0 && 0 < o3 && iconst_0 = 0 && 0 <= NULL && 1 <= i12
langle_init_rangle_Load_313(o90, i66, o91, i67, i4, NULL, iconst_0, env, static) -{1,1}> langle_init_rangle_FieldAccess_317(o90, i66, o91, i67, i4, NULL, iconst_0, env, static) :|: NULL = 0 && 0 <= o91 && 1 <= i67 && 1 <= i66 && iconst_0 = 0 && 0 < o90
langle_init_rangle_FieldAccess_317(o90, i66, o91, i67, i4, NULL, iconst_0, env, static) -{1,1}> langle_init_rangle_Load_320(o90', o91, i66, i67, i4, NULL, env, static) :|: NULL = 0 && 0 <= o91 && 0 < o90' && 1 <= i67 && 1 <= i66 && iconst_0 = 0 && 0 < o90 && o90' <= o90 + i66 && o90 < o90'
langle_init_rangle_Load_320(o90, o91, i66, i67, i4, NULL, env, static) -{1,1}> langle_init_rangle_Load_322(o90, o91, i66, i67, i4, NULL, env, static) :|: NULL = 0 && 0 <= o91 && 1 <= i67 && 1 <= i66 && 0 < o90
langle_init_rangle_Load_322(o90, o91, i66, i67, i4, NULL, env, static) -{1,1}> langle_init_rangle_FieldAccess_324(o90, o91, i66, i67, i4, NULL, env, static) :|: NULL = 0 && 0 <= o91 && 1 <= i67 && 1 <= i66 && 0 < o90
langle_init_rangle_FieldAccess_324(o90, o91, i66, i67, i4, NULL, env, static) -{1,1}> langle_init_rangle_Return_329(o90', i66, i67, i4, o91, env, static) :|: NULL = 0 && 0 <= o91 && 0 < o90' && 1 <= i67 && o90' <= o90 + o91 && 1 <= i66 && o90' = o90 + o91 && 0 < o90
langle_init_rangle_Return_329(o90, i66, i67, i4, o91, env, static) -{1,1}> createIntList_Store_331(o90, i66, i67, i4, o91, env, static) :|: 0 <= o91 && 1 <= i67 && 1 <= i66 && 0 < o90
createIntList_Store_331(o90, i66, i67, i4, o91, env, static) -{1,1}> createIntList_Inc_333(i66, o90, i67, i4, o91, env, static) :|: 0 <= o91 && 1 <= i67 && 1 <= i66 && 0 < o90
createIntList_Inc_333(i66, o90, i67, i4, o91, env, static) -{1,1}> createIntList_JMP_335(i73, o90, i67, i4, o91, i66, env, static) :|: i66 + -1 = i73 && 0 <= o91 && 1 <= i67 && 1 <= i66 && 0 < o90 && 0 <= i73
createIntList_JMP_335(i73, o90, i67, i4, o91, i66, env, static) -{1,1}> createIntList_Load_338(i73, o90, i67, i4, o91, i66, env, static) :|: 0 <= o91 && 1 <= i67 && 1 <= i66 && 0 < o90 && 0 <= i73
createIntList_Load_338(i73, o90, i67, i4, o91, i66, env, static) -{1,1}> createIntList_LE_346(i73, o90, i67, i4, o91, i66, env, static) :|: 0 <= o91 && 1 <= i67 && 1 <= i66 && 0 < o90 && 0 <= i73
createIntList_LE_346(iconst_0, o90, i67, i4, o91, i66, env, static) -{0,0}> createIntList_LE_348(iconst_0, o90, i67, i4, o91, i66, env, static) :|: 0 <= o91 && 0 <= iconst_0 && 1 <= i67 && 1 <= i66 && iconst_0 = 0 && 0 < o90
createIntList_LE_346(i80, o90, i67, i4, o91, i81, env, static) -{0,0}> createIntList_LE_350(i80, o90, i67, i4, o91, i81, env, static) :|: 1 <= i80 && 0 <= o91 && 2 <= i81 && 1 <= i67 && 0 <= i80 && 0 < o90 && 1 <= i81
createIntList_LE_348(iconst_0, o90, i67, i4, o91, i66, env, static) -{1,1}> createIntList_Load_353(o90, i67, i4, o91, i66, env, static) :|: 0 <= o91 && iconst_0 <= 0 && 1 <= i67 && 1 <= i66 && iconst_0 = 0 && 0 < o90
createIntList_LE_350(i80, o90, i67, i4, o91, i81, env, static) -{1,1}> createIntList_New_356(i80, o90, i67, i4, o91, i81, env, static) :|: 1 <= i80 && 0 <= o91 && 2 <= i81 && 1 <= i67 && 0 < i80 && 0 < o90
createIntList_Load_353(o90, i67, i4, o91, i66, env, static) -{1,1}> createIntList_Return_359(o90, i67, i4, o91, i66, env, static) :|: 0 <= o91 && 1 <= i67 && 1 <= i66 && 0 < o90
createIntList_New_356(i80, o90, i67, i4, o91, i81, env, static) -{1,1}> createIntList_Duplicate_362(o111, i80, o90, i67, i4, NULL, iconst_0, o91, i81, env, static) :|: NULL = 0 && 1 <= i80 && o111 = 1 && 0 <= o91 && 2 <= i81 && 1 <= i67 && iconst_0 = 0 && 0 < o90 && 0 < o111
createIntList_Return_359(o90, i67, i4, o91, i66, env, static) -{1,1}> main_Store_364(i67, i4, o90, o91, i66, env, static) :|: 0 <= o91 && 1 <= i67 && 1 <= i66 && 0 < o90
createIntList_Duplicate_362(o111, i80, o90, i67, i4, NULL, iconst_0, o91, i81, env, static) -{1,1}> createIntList_Load_365(o111, i80, o90, i67, i4, NULL, iconst_0, o91, i81, env, static) :|: NULL = 0 && 1 <= i80 && 0 <= o91 && 2 <= i81 && 1 <= i67 && iconst_0 = 0 && 0 < o90 && 0 < o111
main_Store_364(i67, i4, o90, o91, i66, env, static) -{1,1}> main_ConstantStackPush_366(i67, i4, o90, o91, i66, env, static) :|: 0 <= o91 && 1 <= i67 && 1 <= i66 && 0 < o90
createIntList_Load_365(o111, i80, o90, i67, i4, NULL, iconst_0, o91, i81, env, static) -{1,1}> createIntList_Load_367(o111, i80, o90, i67, i4, NULL, iconst_0, o91, i81, env, static) :|: NULL = 0 && 1 <= i80 && 0 <= o91 && 2 <= i81 && 1 <= i67 && iconst_0 = 0 && 0 < o90 && 0 < o111
main_ConstantStackPush_366(i67, i4, o90, o91, i66, env, static) -{1,1}> main_Store_369(i67, i4, iconst_0, o90, o91, i66, env, static) :|: 0 <= o91 && 1 <= i67 && 1 <= i66 && iconst_0 = 0 && 0 < o90
createIntList_Load_367(o111, i80, o90, i67, i4, NULL, iconst_0, o91, i81, env, static) -{1,1}> createIntList_InvokeMethod_372(o111, i80, o90, i67, i4, NULL, iconst_0, o91, i81, env, static) :|: NULL = 0 && 1 <= i80 && 0 <= o91 && 2 <= i81 && 1 <= i67 && iconst_0 = 0 && 0 < o90 && 0 < o111
main_Store_369(i67, i4, iconst_0, o90, o91, i66, env, static) -{1,1}> main_Load_375(i67, i4, o90, iconst_0, o91, i66, env, static) :|: 0 <= o91 && 1 <= i67 && 1 <= i66 && iconst_0 = 0 && 0 < o90
createIntList_InvokeMethod_372(o111, i80, o90, i67, i4, NULL, iconst_0, o91, i81, env, static) -{1,1}> langle_init_rangle_Load_376(o111, i80, o90, i67, i4, NULL, iconst_0, o91, i81, env, static) :|: NULL = 0 && 1 <= i80 && 0 <= o91 && 2 <= i81 && 1 <= i67 && iconst_0 = 0 && 0 < o90 && 0 < o111
main_Load_375(i67, i4, o90, iconst_0, o91, i66, env, static) -{0,0}> main_Load_437(i67, i4, o90, iconst_0, o91, i66, env, static) :|: 0 <= o91 && 0 <= i66 && 1 <= i67 && 0 <= iconst_0 && 1 <= i66 && iconst_0 <= 1 && iconst_0 = 0 && 0 < o90
langle_init_rangle_Load_376(o111, i80, o90, i67, i4, NULL, iconst_0, o91, i81, env, static) -{1,1}> langle_init_rangle_InvokeMethod_382(o111, i80, o90, i67, i4, NULL, iconst_0, o91, i81, env, static) :|: NULL = 0 && 1 <= i80 && 0 <= o91 && 2 <= i81 && 1 <= i67 && iconst_0 = 0 && 0 < o90 && 0 < o111
langle_init_rangle_InvokeMethod_382(o111, i80, o90, i67, i4, NULL, iconst_0, o91, i81, env, static) -{1,1}> langle_init_rangle_Load_384(o111, i80, o90, i67, i4, NULL, iconst_0, o91, i81, env, static) :|: NULL = 0 && 1 <= i80 && 0 <= o91 && 2 <= i81 && 1 <= i67 && iconst_0 = 0 && 0 < o90 && 0 < o111
langle_init_rangle_Load_384(o111, i80, o90, i67, i4, NULL, iconst_0, o91, i81, env, static) -{1,1}> langle_init_rangle_Load_388(o111, i80, o90, i67, i4, NULL, iconst_0, o91, i81, env, static) :|: NULL = 0 && 1 <= i80 && 0 <= o91 && 2 <= i81 && 1 <= i67 && iconst_0 = 0 && 0 < o90 && 0 < o111
langle_init_rangle_Load_388(o111, i80, o90, i67, i4, NULL, iconst_0, o91, i81, env, static) -{0,0}> langle_init_rangle_Load_313(o111, i80, o90, i67, i4, NULL, iconst_0, env, static) :|: NULL = 0 && 1 <= i80 && 0 <= o91 && 2 <= i81 && 1 <= i67 && 0 <= o90 && iconst_0 = 0 && 0 < o90 && 0 < o111
main_Load_437(i67, i4, o139, i97, o140, i96, env, static) -{0,0}> main_Load_487(i67, i4, o139, i97, env, static) :|: 0 <= o140 && 0 < o139 && 1 <= i67 && 0 <= i97 && 0 <= o139 && 0 <= i96 && i97 <= 1
main_Load_487(i67, i4, o156, i97, env, static) -{0,0}> main_Load_546(i67, i4, o156, i97, env, static) :|: 1 <= i67 && 0 <= i97 && 0 <= o156 && i97 <= 1 && i97 <= 2
main_Load_546(i67, i4, o176, i118, env, static) -{0,0}> main_Load_601(i67, i4, o176, i118, env, static) :|: 1 <= i67 && 0 <= o176 && i118 <= 2 && 0 <= i118
main_Load_601(i67, i4, o195, i127, env, static) -{0,0}> main_Load_653(i67, i4, o195, i127, env, static) :|: 1 <= i67 && 0 <= o195 && 0 <= i127
main_Load_653(i67, i4, o217, i137, env, static) -{1,1}> main_NULL_656(i67, i4, o217, i137, env, static) :|: 1 <= i67 && 0 <= o217
main_NULL_656(i67, i4, o226, i137, env, static) -{0,0}> main_NULL_658(i67, i4, o226, i137, env, static) :|: 0 <= o226 && 1 <= i67 && 0 < o226
main_NULL_658(i67, i4, o226, i137, env, static) -{1,1}> main_Load_661(i67, i4, o226, i137, env, static) :|: 1 <= i67 && 0 < o226
main_Load_661(i67, i4, o226, i137, env, static) -{1,1}> main_FieldAccess_665(i67, i4, o226, i137, env, static) :|: 1 <= i67 && 0 < o226
main_FieldAccess_665(i67, i4, o228, i137, env, static) -{0,0}> main_FieldAccess_668(i67, i4, o228, i137, o229, i142, env, static) :|: 0 <= o229 && 1 <= i67 && o229 < o228 && -1 * o228 < i142 && 0 < o228 && i142 < o228
main_FieldAccess_668(i67, i4, o228, i137, o229, i142, env, static) -{1,1}> main_GT_671(i67, i4, i142, o228, i137, o229, env, static) :|: 0 <= o229 && 1 <= i67 && 0 < o228
main_GT_671(i67, i4, i143, o228, i137, o229, env, static) -{0,0}> main_GT_672(i67, i4, i143, o228, i137, o229, env, static) :|: 0 <= o229 && 1 <= i67 && i143 <= 0 && 0 < o228
main_GT_671(i67, i4, i144, o228, i137, o229, env, static) -{0,0}> main_GT_673(i67, i4, i144, o228, i137, o229, env, static) :|: 1 <= i144 && 0 <= o229 && 1 <= i67 && 0 < o228
main_GT_672(i67, i4, i143, o228, i137, o229, env, static) -{1,1}> main_Load_675(i67, i4, o228, i137, o229, i143, env, static) :|: 0 <= o229 && 1 <= i67 && i143 <= 0 && 0 < o228
main_GT_673(i67, i4, i144, o228, i137, o229, env, static) -{1,1}> main_Load_677(i67, i4, o228, i137, o229, i144, env, static) :|: 1 <= i144 && 0 <= o229 && 1 <= i67 && 0 < i144 && 0 < o228
main_Load_675(i67, i4, o228, i137, o229, i143, env, static) -{1,1}> main_FieldAccess_679(i67, i4, o228, i137, o229, i143, env, static) :|: 0 <= o229 && 1 <= i67 && i143 <= 0 && 0 < o228
main_Load_677(i67, i4, o228, i137, o229, i144, env, static) -{1,1}> main_Duplicate_680(i67, i4, o228, i137, o229, i144, env, static) :|: 1 <= i144 && 0 <= o229 && 1 <= i67 && 0 < o228
main_FieldAccess_679(i67, i4, o228, i137, o229, i143, env, static) -{1,1}> main_Store_682(i67, i4, o229, i137, env, static) :|: 0 <= o229 && 1 <= i67 && i143 <= 0 && 0 < o228
main_Duplicate_680(i67, i4, o228, i137, o229, i144, env, static) -{1,1}> main_FieldAccess_684(i67, i4, o228, i137, o229, i144, env, static) :|: 1 <= i144 && 0 <= o229 && 1 <= i67 && 0 < o228
main_Store_682(i67, i4, o229, i137, env, static) -{1,1}> main_Load_685(i67, i4, o229, i137, env, static) :|: 0 <= o229 && 1 <= i67
main_FieldAccess_684(i67, i4, o228, i137, o229, i144, env, static) -{1,1}> main_ConstantStackPush_687(i67, i4, o228, i144, i137, o229, env, static) :|: 1 <= i144 && 0 <= o229 && 1 <= i67 && 0 < o228
main_Load_685(i67, i4, o229, i137, env, static) -{1,1}> main_NULL_689(i67, i4, o229, i137, env, static) :|: 0 <= o229 && 1 <= i67
main_ConstantStackPush_687(i67, i4, o228, i144, i137, o229, env, static) -{1,1}> main_IntArithmetic_691(i67, i4, o228, i144, iconst_1, i137, o229, env, static) :|: 1 <= i144 && 0 <= o229 && 1 <= i67 && iconst_1 = 1 && 0 < o228
main_NULL_689(i67, i4, o230, i137, env, static) -{0,0}> main_NULL_693(i67, i4, o230, i137, env, static) :|: 0 < o230 && 1 <= i67 && 0 <= o230
main_NULL_689(i67, i4, NULL, i137, env, static) -{0,0}> main_NULL_694(i67, i4, NULL, i137, env, static) :|: NULL = 0 && 1 <= i67 && 0 <= NULL
main_IntArithmetic_691(i67, i4, o228, i144, iconst_1, i137, o229, env, static) -{1,1}> main_FieldAccess_697(i67, i4, o228, i146, i137, o229, i144, env, static) :|: 1 <= i144 && 0 <= o229 && 1 <= i67 && iconst_1 = 1 && 0 <= i146 && i144 - iconst_1 = i146 && 0 < o228
main_NULL_693(i67, i4, o230, i137, env, static) -{1,1}> main_Load_699(i67, i4, o230, i137, env, static) :|: 0 < o230 && 1 <= i67
main_NULL_694(i67, i4, NULL, i137, env, static) -{1,1}> main_Load_707(i67, i4, NULL, i137, env, static) :|: NULL = 0 && 1 <= i67
main_FieldAccess_697(i67, i4, o228, i146, i137, o229, i144, env, static) -{1,1}> main_Inc_710(i67, i4, o228', i137, o229, i146, env, static) :|: 0 < o228' && 1 <= i144 && 0 <= o229 && 1 <= i67 && o228' <= o228 + i146 && 0 <= i146 && o228' < o228 && 0 < o228
main_Load_699(i67, i4, o230, i137, env, static) -{1,1}> main_Load_712(i67, i4, i137, o230, env, static) :|: 0 < o230 && 1 <= i67
main_Load_707(i67, i4, NULL, i137, env, static) -{0,0}> main_Load_653(i67, i4, NULL, i137, env, static) :|: NULL = 0 && 1 <= i67 && 0 <= NULL
main_Inc_710(i67, i4, o228, i137, o229, i146, env, static) -{1,1}> main_JMP_715(i67, i4, o228, i148, o229, i146, env, static) :|: i137 + 1 = i148 && 0 <= o229 && 1 <= i67 && 0 <= i146 && 0 < o228
main_Load_712(i67, i4, i137, o230, env, static) -{1,1}> main_IntArithmetic_717(i67, i4, i137, o230, env, static) :|: 0 < o230 && 1 <= i67
main_JMP_715(i67, i4, o228, i148, o229, i146, env, static) -{1,1}> main_Load_722(i67, i4, o228, i148, o229, i146, env, static) :|: 0 <= o229 && 1 <= i67 && 0 <= i146 && 0 < o228
main_IntArithmetic_717(i67, i4, i137, o230, env, static) -{1,1}> main_Store_724(i67, i4, i150, o230, env, static) :|: 0 < o230 && 1 <= i67 && i137 * i4 = i150
main_Load_722(i67, i4, o228, i148, o229, i146, env, static) -{0,0}> main_Load_653(i67, i4, o228, i148, env, static) :|: 0 <= o229 && 1 <= i67 && 0 <= i146 && 0 < o228 && 0 <= o228
main_Store_724(i67, i4, i150, o230, env, static) -{1,1}> main_JMP_726(i67, i4, o230, i150, env, static) :|: 0 < o230 && 1 <= i67
main_JMP_726(i67, i4, o230, i150, env, static) -{1,1}> main_Load_732(i67, i4, o230, i150, env, static) :|: 0 < o230 && 1 <= i67
main_Load_732(i67, i4, o230, i150, env, static) -{0,0}> main_Load_653(i67, i4, o230, i150, env, static) :|: 0 < o230 && 1 <= i67 && 0 <= o230

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

obtained
main_Load_1(i2, i4, env, static) -{29,29}> langle_init_rangle_Load_313(1, i2, 0, i2, i4, 0, 0, env, static'1) :|: 0 >= 0 && 1 <= i2 && static'1 <= static''' + 1 && 0 <= 0 && 0 <= 2 && 0 <= static''' && 0 < 1 && static''' <= static + 2 && 0 <= 1 && 0 <= static && 0 < i2 && 0 <= static'1 && 0 < 2
by chaining
main_Load_1(i2, i4, env, static) -{0,0}> main_Load_3(i2, i4, env, static) :|: 0 >= 0
main_Load_3(i2, i4, env, static) -{0,0}> langle_clinit_rangle_ConstantStackPush_5(i2, i4, env, static) :|: 0 >= 0
langle_clinit_rangle_ConstantStackPush_5(i2, i4, env, static) -{1,1}> langle_clinit_rangle_ArrayCreate_12(iconst_0, i2, i4, env, static) :|: iconst_0 = 0
langle_clinit_rangle_ArrayCreate_12(iconst_0, i2, i4, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_13(a2, i2, i4, iconst_0, env, static) :|: a2 = 2 && iconst_0 = 0 && 0 < a2
langle_clinit_rangle_FieldAccess_13(a2, i2, i4, iconst_0, env, static) -{1,1}> langle_clinit_rangle_New_14(i2, i4, env, static') :|: 0 <= a2 && iconst_0 = 0 && static' <= static + a2 && 0 <= static && 0 < a2
langle_clinit_rangle_New_14(i2, i4, env, static) -{0,0}> langle_clinit_rangle_New_16(i2, i4, env, static) :|: 0 >= 0
langle_clinit_rangle_New_16(i2, i4, env, static) -{0,0}> langle_clinit_rangle_New_17(i2, i4, env, static) :|: 0 <= static
langle_clinit_rangle_New_17(i2, i4, env, static) -{1,1}> langle_clinit_rangle_Duplicate_19(o2, i2, i4, env, static) :|: 0 < o2 && o2 = 1
langle_clinit_rangle_Duplicate_19(o2, i2, i4, env, static) -{1,1}> langle_clinit_rangle_ConstantStackPush_21(o2, i2, i4, env, static) :|: 0 < o2
langle_clinit_rangle_ConstantStackPush_21(o2, i2, i4, env, static) -{1,1}> langle_clinit_rangle_InvokeMethod_22(o2, NULL, i2, i4, env, static) :|: NULL = 0 && 0 < o2
langle_clinit_rangle_InvokeMethod_22(o2, NULL, i2, i4, env, static) -{1,1}> langle_init_rangle_Load_24(o2, i2, i4, env, static) :|: NULL = 0 && 0 < o2
langle_init_rangle_Load_24(o2, i2, i4, env, static) -{1,1}> langle_init_rangle_InvokeMethod_29(o2, i2, i4, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_29(o2, i2, i4, env, static) -{1,1}> langle_init_rangle_Load_30(o2, i2, i4, env, static) :|: 0 < o2
langle_init_rangle_Load_30(o2, i2, i4, env, static) -{1,1}> langle_init_rangle_InvokeMethod_33(o2, i2, i4, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_33(o2, i2, i4, env, static) -{1,1}> langle_init_rangle_Return_35(o2, i2, i4, env, static) :|: 0 < o2
langle_init_rangle_Return_35(o2, i2, i4, env, static) -{1,1}> langle_init_rangle_Return_38(o2, i2, i4, env, static) :|: 0 < o2
langle_init_rangle_Return_38(o2, i2, i4, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_39(o2, i2, i4, env, static) :|: 0 < o2
langle_clinit_rangle_FieldAccess_39(o2, i2, i4, env, static) -{1,1}> langle_clinit_rangle_Return_40(i2, i4, env, static') :|: 0 < o2 && 0 <= o2 && 0 <= static && static' <= static + o2
langle_clinit_rangle_Return_40(i2, i4, env, static) -{1,1}> main_Load_46(i2, i4, env, static) :|: 0 >= 0
main_Load_46(i2, i4, env, static) -{0,0}> main_Load_47(i2, i4, env, static) :|: 0 >= 0
main_Load_47(i2, i4, env, static) -{0,0}> main_Load_50(i2, i4, env, static) :|: 0 <= static
main_Load_50(i2, i4, env, static) -{0,0}> main_Load_51(i2, i4, env, static) :|: 0 >= 0
main_Load_51(i2, i4, env, static) -{0,0}> main_Load_52(i2, i4, env, static) :|: 0 >= 0
main_Load_52(i2, i4, env, static) -{1,1}> main_InvokeMethod_55(i2, i4, env, static) :|: 0 >= 0
main_InvokeMethod_55(i2, i4, env, static) -{0,0}> main_InvokeMethod_56(i2, i4, env, static) :|: 0 >= 0
main_InvokeMethod_56(i2, i4, env, static) -{1,1}> createIntList_ConstantStackPush_57(i2, i4, env, static) :|: 0 >= 0
createIntList_ConstantStackPush_57(i2, i4, env, static) -{1,1}> createIntList_Store_58(NULL, i2, i4, env, static) :|: NULL = 0
createIntList_Store_58(NULL, i2, i4, env, static) -{1,1}> createIntList_Load_59(i2, NULL, i4, env, static) :|: NULL = 0
createIntList_Load_59(i2, NULL, i4, env, static) -{1,1}> createIntList_LE_62(i2, NULL, i4, env, static) :|: NULL = 0
createIntList_LE_62(i12, NULL, i4, env, static) -{0,0}> createIntList_LE_64(i12, NULL, i4, env, static) :|: NULL = 0 && 1 <= i12
createIntList_LE_64(i12, NULL, i4, env, static) -{1,1}> createIntList_New_66(i12, NULL, i4, env, static) :|: NULL = 0 && 0 < i12 && 1 <= i12
createIntList_New_66(i12, NULL, i4, env, static) -{1,1}> createIntList_Duplicate_75(o3, i12, NULL, i4, iconst_0, env, static) :|: NULL = 0 && o3 = 1 && 0 < o3 && iconst_0 = 0 && 1 <= i12
createIntList_Duplicate_75(o3, i12, NULL, i4, iconst_0, env, static) -{1,1}> createIntList_Load_80(o3, i12, NULL, i4, iconst_0, env, static) :|: NULL = 0 && 0 < o3 && iconst_0 = 0 && 1 <= i12
createIntList_Load_80(o3, i12, NULL, i4, iconst_0, env, static) -{1,1}> createIntList_Load_84(o3, i12, NULL, i4, iconst_0, env, static) :|: NULL = 0 && 0 < o3 && iconst_0 = 0 && 1 <= i12
createIntList_Load_84(o3, i12, NULL, i4, iconst_0, env, static) -{1,1}> createIntList_InvokeMethod_89(o3, i12, NULL, i4, iconst_0, env, static) :|: NULL = 0 && 0 < o3 && iconst_0 = 0 && 1 <= i12
createIntList_InvokeMethod_89(o3, i12, NULL, i4, iconst_0, env, static) -{1,1}> langle_init_rangle_Load_92(o3, i12, NULL, i4, iconst_0, env, static) :|: NULL = 0 && 0 < o3 && iconst_0 = 0 && 1 <= i12
langle_init_rangle_Load_92(o3, i12, NULL, i4, iconst_0, env, static) -{1,1}> langle_init_rangle_InvokeMethod_98(o3, i12, NULL, i4, iconst_0, env, static) :|: NULL = 0 && 0 < o3 && iconst_0 = 0 && 1 <= i12
langle_init_rangle_InvokeMethod_98(o3, i12, NULL, i4, iconst_0, env, static) -{1,1}> langle_init_rangle_Load_100(o3, i12, NULL, i4, iconst_0, env, static) :|: NULL = 0 && 0 < o3 && iconst_0 = 0 && 1 <= i12
langle_init_rangle_Load_100(o3, i12, NULL, i4, iconst_0, env, static) -{1,1}> langle_init_rangle_Load_101(o3, i12, NULL, i4, iconst_0, env, static) :|: NULL = 0 && 0 < o3 && iconst_0 = 0 && 1 <= i12
langle_init_rangle_Load_101(o3, i12, NULL, i4, iconst_0, env, static) -{0,0}> langle_init_rangle_Load_313(o3, i12, NULL, i12, i4, NULL, iconst_0, env, static) :|: NULL = 0 && 0 < o3 && iconst_0 = 0 && 0 <= NULL && 1 <= i12

obtained
main_Load_653(i67, i4, o217, i137, env, static) -{4,4}> main_GT_671(i67, i4, i142', o217, i137, o229', env, static) :|: 0 <= o229' && 0 < o217 && o229' < o217 && 1 <= i67 && -1 * o217 < i142' && 0 <= o217 && i142' < o217
by chaining
main_Load_653(i67, i4, o217, i137, env, static) -{1,1}> main_NULL_656(i67, i4, o217, i137, env, static) :|: 1 <= i67 && 0 <= o217
main_NULL_656(i67, i4, o226, i137, env, static) -{0,0}> main_NULL_658(i67, i4, o226, i137, env, static) :|: 0 <= o226 && 1 <= i67 && 0 < o226
main_NULL_658(i67, i4, o226, i137, env, static) -{1,1}> main_Load_661(i67, i4, o226, i137, env, static) :|: 1 <= i67 && 0 < o226
main_Load_661(i67, i4, o226, i137, env, static) -{1,1}> main_FieldAccess_665(i67, i4, o226, i137, env, static) :|: 1 <= i67 && 0 < o226
main_FieldAccess_665(i67, i4, o228, i137, env, static) -{0,0}> main_FieldAccess_668(i67, i4, o228, i137, o229, i142, env, static) :|: 0 <= o229 && 1 <= i67 && o229 < o228 && -1 * o228 < i142 && 0 < o228 && i142 < o228
main_FieldAccess_668(i67, i4, o228, i137, o229, i142, env, static) -{1,1}> main_GT_671(i67, i4, i142, o228, i137, o229, env, static) :|: 0 <= o229 && 1 <= i67 && 0 < o228

(30) Obligation:

IntTrs with 9 rules
Start term: main_Load_1(#0, #1, env, static)
Considered paths: all paths from start
Rules:
main_Load_1(i2, i4, env, static) -{29,29}> langle_init_rangle_Load_313(1, i2, 0, i2, i4, 0, 0, env, static'1) :|: 0 >= 0 && 1 <= i2 && static'1 <= static''' + 1 && 0 <= 0 && 0 <= 2 && 0 <= static''' && 0 < 1 && static''' <= static + 2 && 0 <= 1 && 0 <= static && 0 < i2 && 0 <= static'1 && 0 < 2
langle_init_rangle_Load_313(o90, i66, o91, i67, i4, 0, 0, env, static) -{10,10}> createIntList_LE_346(i73', o90'1, i67, i4, o91, i66, env, static) :|: o90 < o90''' && 0 <= i73' && 0 < o90 && 0 < o90'1 && o90'1 <= o90''' + o91 && 1 <= i66 && 1 <= i67 && 0 <= o91 && i66 + -1 = i73' && o90''' <= o90 + i66 && o90'1 = o90''' + o91 && 0 < o90'''
createIntList_LE_346(i80, o90, i67, i4, o91, i81, env, static) -{9,9}> langle_init_rangle_Load_313(1, i80, o90, i67, i4, 0, 0, env, static) :|: 1 <= i80 && 0 < 1 && 0 <= o91 && 0 < o90 && 2 <= i81 && 1 <= i67 && 0 <= o90 && 0 <= i80 && 0 < i80 && 1 <= i81
createIntList_LE_346(0, o90, i67, i4, o91, i66, env, static) -{6,6}> main_Load_653(i67, i4, o90, 0, env, static) :|: 0 < o90 && 0 <= 0 && 0 <= 1 && 1 <= i67 && 0 <= o90 && 0 <= o91 && 1 <= i66 && 0 <= 2 && 0 <= i66
main_Load_653(i67, i4, o217, i137, env, static) -{4,4}> main_GT_671(i67, i4, i142', o217, i137, o229', env, static) :|: 0 <= o229' && 0 < o217 && o229' < o217 && 1 <= i67 && -1 * o217 < i142' && 0 <= o217 && i142' < o217
main_GT_671(i67, i4, i144, o228, i137, o229, env, static) -{9,9}> main_Load_653(i67, i4, o228''', i148', env, static) :|: 1 <= i144 && 0 <= o228''' && o228''' <= o228 + i146' && 0 < o228''' && i137 + 1 = i148' && 0 <= i146' && i144 - 1 = i146' && 0 <= o229 && 1 <= i67 && o228''' < o228 && 0 < i144 && 0 < o228
main_GT_671(i67, i4, i143, o228, i137, o229, env, static) -{5,5}> main_NULL_689(i67, i4, o229, i137, env, static) :|: 0 < o228 && 0 <= o229 && 1 <= i67 && i143 <= 0
main_NULL_689(i67, i4, 0, i137, env, static) -{1,1}> main_Load_653(i67, i4, 0, i137, env, static) :|: 0 <= 0 && 1 <= i67
main_NULL_689(i67, i4, o230, i137, env, static) -{6,6}> main_Load_653(i67, i4, o230, i150', env, static) :|: 0 <= o230 && 1 <= i67 && 0 < o230 && i137 * i4 = i150'

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

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

main_Load_1(x1, x2, x3, x4) → main_Load_1(x1, x2, x4)
langle_init_rangle_Load_313(x1, x2, x3, x4, x5, x6, x7, x8, x9) → langle_init_rangle_Load_313(x1, x2, x3, x4, x5)
createIntList_LE_346(x1, x2, x3, x4, x5, x6, x7, x8) → createIntList_LE_346(x1, x2, x3, x4, x5, x6)
main_Load_653(x1, x2, x3, x4, x5, x6) → main_Load_653(x1, x2, x3, x4)
main_GT_671(x1, x2, x3, x4, x5, x6, x7, x8) → main_GT_671(x1, x2, x3, x4, x5, x6)
main_NULL_689(x1, x2, x3, x4, x5, x6) → main_NULL_689(x1, x2, x3, x4)

(32) Obligation:

IntTrs with 9 rules
Start term: main_Load_1(#0, #1, static)
Considered paths: all paths from start
Rules:
main_Load_1(i2, i4, static) -{29,29}> langle_init_rangle_Load_313(1, i2, 0, i2, i4) :|: 0 >= 0 && 1 <= i2 && static'1 <= static''' + 1 && 0 <= 0 && 0 <= 2 && 0 <= static''' && 0 < 1 && static''' <= static + 2 && 0 <= 1 && 0 <= static && 0 < i2 && 0 <= static'1 && 0 < 2
langle_init_rangle_Load_313(o90, i66, o91, i67, i4) -{10,10}> createIntList_LE_346(i73', o90'1, i67, i4, o91, i66) :|: o90 < o90''' && 0 <= i73' && 0 < o90 && 0 < o90'1 && o90'1 <= o90''' + o91 && 1 <= i66 && 1 <= i67 && 0 <= o91 && i66 + -1 = i73' && o90''' <= o90 + i66 && o90'1 = o90''' + o91 && 0 < o90'''
createIntList_LE_346(i80, o90, i67, i4, o91, i81) -{9,9}> langle_init_rangle_Load_313(1, i80, o90, i67, i4) :|: 1 <= i80 && 0 < 1 && 0 <= o91 && 0 < o90 && 2 <= i81 && 1 <= i67 && 0 <= o90 && 0 <= i80 && 0 < i80 && 1 <= i81
createIntList_LE_346(0, o90, i67, i4, o91, i66) -{6,6}> main_Load_653(i67, i4, o90, 0) :|: 0 < o90 && 0 <= 0 && 0 <= 1 && 1 <= i67 && 0 <= o90 && 0 <= o91 && 1 <= i66 && 0 <= 2 && 0 <= i66
main_Load_653(i67, i4, o217, i137) -{4,4}> main_GT_671(i67, i4, i142', o217, i137, o229') :|: 0 <= o229' && 0 < o217 && o229' < o217 && 1 <= i67 && -1 * o217 < i142' && 0 <= o217 && i142' < o217
main_GT_671(i67, i4, i144, o228, i137, o229) -{9,9}> main_Load_653(i67, i4, o228''', i148') :|: 1 <= i144 && 0 <= o228''' && o228''' <= o228 + i146' && 0 < o228''' && i137 + 1 = i148' && 0 <= i146' && i144 - 1 = i146' && 0 <= o229 && 1 <= i67 && o228''' < o228 && 0 < i144 && 0 < o228
main_GT_671(i67, i4, i143, o228, i137, o229) -{5,5}> main_NULL_689(i67, i4, o229, i137) :|: 0 < o228 && 0 <= o229 && 1 <= i67 && i143 <= 0
main_NULL_689(i67, i4, 0, i137) -{1,1}> main_Load_653(i67, i4, 0, i137) :|: 0 <= 0 && 1 <= i67
main_NULL_689(i67, i4, o230, i137) -{6,6}> main_Load_653(i67, i4, o230, i150') :|: 0 <= o230 && 1 <= i67 && 0 < o230 && i137 * i4 = i150'

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

Moved arithmethic from lhss to constraints.

main_NULL_689(i67, i4, 0, i137) -{1,1}> main_Load_653(i67, i4, 0, i137) :|: 0 <= 0 && 1 <= i67
was transformed to
main_NULL_689(i67, i4, x, i137) -{1,1}> main_Load_653(i67, i4, 0, i137) :|: 0 <= 0 && 1 <= i67 && x = 0

createIntList_LE_346(0, o90, i67, i4, o91, i66) -{6,6}> main_Load_653(i67, i4, o90, 0) :|: 0 < o90 && 0 <= 0 && 0 <= 1 && 1 <= i67 && 0 <= o90 && 0 <= o91 && 1 <= i66 && 0 <= 2 && 0 <= i66
was transformed to
createIntList_LE_346(x, o90, i67, i4, o91, i66) -{6,6}> main_Load_653(i67, i4, o90, 0) :|: 0 < o90 && 0 <= 0 && 0 <= 1 && 1 <= i67 && 0 <= o90 && 0 <= o91 && 1 <= i66 && 0 <= 2 && 0 <= i66 && x = 0

(34) Obligation:

IntTrs with 9 rules
Start term: main_Load_1(#0, #1, static)
Considered paths: all paths from start
Rules:
createIntList_LE_346(i80, o90, i67, i4, o91, i81) -{9,9}> langle_init_rangle_Load_313(1, i80, o90, i67, i4) :|: 1 <= i80 && 0 < 1 && 0 <= o91 && 0 < o90 && 2 <= i81 && 1 <= i67 && 0 <= o90 && 0 <= i80 && 0 < i80 && 1 <= i81
main_Load_1(i2, i4, static) -{29,29}> langle_init_rangle_Load_313(1, i2, 0, i2, i4) :|: 0 >= 0 && 1 <= i2 && static'1 <= static''' + 1 && 0 <= 0 && 0 <= 2 && 0 <= static''' && 0 < 1 && static''' <= static + 2 && 0 <= 1 && 0 <= static && 0 < i2 && 0 <= static'1 && 0 < 2
main_GT_671(i67, i4, i144, o228, i137, o229) -{9,9}> main_Load_653(i67, i4, o228''', i148') :|: 1 <= i144 && 0 <= o228''' && o228''' <= o228 + i146' && 0 < o228''' && i137 + 1 = i148' && 0 <= i146' && i144 - 1 = i146' && 0 <= o229 && 1 <= i67 && o228''' < o228 && 0 < i144 && 0 < o228
main_GT_671(i67, i4, i143, o228, i137, o229) -{5,5}> main_NULL_689(i67, i4, o229, i137) :|: 0 < o228 && 0 <= o229 && 1 <= i67 && i143 <= 0
main_Load_653(i67, i4, o217, i137) -{4,4}> main_GT_671(i67, i4, i142', o217, i137, o229') :|: 0 <= o229' && 0 < o217 && o229' < o217 && 1 <= i67 && -1 * o217 < i142' && 0 <= o217 && i142' < o217
main_NULL_689(i67, i4, o230, i137) -{6,6}> main_Load_653(i67, i4, o230, i150') :|: 0 <= o230 && 1 <= i67 && 0 < o230 && i137 * i4 = i150'
main_NULL_689(i67, i4, x, i137) -{1,1}> main_Load_653(i67, i4, 0, i137) :|: 0 <= 0 && 1 <= i67 && x = 0
createIntList_LE_346(x, o90, i67, i4, o91, i66) -{6,6}> main_Load_653(i67, i4, o90, 0) :|: 0 < o90 && 0 <= 0 && 0 <= 1 && 1 <= i67 && 0 <= o90 && 0 <= o91 && 1 <= i66 && 0 <= 2 && 0 <= i66 && x = 0
langle_init_rangle_Load_313(o90, i66, o91, i67, i4) -{10,10}> createIntList_LE_346(i73', o90'1, i67, i4, o91, i66) :|: o90 < o90''' && 0 <= i73' && 0 < o90 && 0 < o90'1 && o90'1 <= o90''' + o91 && 1 <= i66 && 1 <= i67 && 0 <= o91 && i66 + -1 = i73' && o90''' <= o90 + i66 && o90'1 = o90''' + o91 && 0 < o90'''

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

Moved arithmethic from constraints to rhss.

main_GT_671(i67, i4, i144, o228, i137, o229) -{9,9}> main_Load_653(i67, i4, o228''', i148') :|: 1 <= i144 && 0 <= o228''' && o228''' <= o228 + i146' && 0 < o228''' && i137 + 1 = i148' && 0 <= i146' && i144 - 1 = i146' && 0 <= o229 && 1 <= i67 && o228''' < o228 && 0 < i144 && 0 < o228
was transformed to
main_GT_671(i67, i4, i144, o228, i137, o229) -{9,9}> main_Load_653(i67, i4, o228''', i137 + 1) :|: 1 <= i144 && 0 <= o228''' && o228''' <= o228 + i146' && 0 < o228''' && i137 + 1 = i148' && 0 <= i146' && i144 - 1 = i146' && 0 <= o229 && 1 <= i67 && o228''' < o228 && 0 < i144 && 0 < o228

langle_init_rangle_Load_313(o90, i66, o91, i67, i4) -{10,10}> createIntList_LE_346(i73', o90'1, i67, i4, o91, i66) :|: o90 < o90''' && 0 <= i73' && 0 < o90 && 0 < o90'1 && o90'1 <= o90''' + o91 && 1 <= i66 && 1 <= i67 && 0 <= o91 && i66 + -1 = i73' && o90''' <= o90 + i66 && o90'1 = o90''' + o91 && 0 < o90'''
was transformed to
langle_init_rangle_Load_313(o90, i66, o91, i67, i4) -{10,10}> createIntList_LE_346(i66 + -1, o90''' + o91, i67, i4, o91, i66) :|: o90 < o90''' && 0 <= i73' && 0 < o90 && 0 < o90'1 && o90'1 <= o90''' + o91 && 1 <= i66 && 1 <= i67 && 0 <= o91 && i66 + -1 = i73' && o90''' <= o90 + i66 && o90'1 = o90''' + o91 && 0 < o90'''

main_NULL_689(i67, i4, o230, i137) -{6,6}> main_Load_653(i67, i4, o230, i150') :|: 0 <= o230 && 1 <= i67 && 0 < o230 && i137 * i4 = i150'
was transformed to
main_NULL_689(i67, i4, o230, i137) -{6,6}> main_Load_653(i67, i4, o230, i137 * i4) :|: 0 <= o230 && 1 <= i67 && 0 < o230 && i137 * i4 = i150'

(36) Obligation:

IntTrs with 9 rules
Start term: main_Load_1(#0, #1, static)
Considered paths: all paths from start
Rules:
createIntList_LE_346(i80, o90, i67, i4, o91, i81) -{9,9}> langle_init_rangle_Load_313(1, i80, o90, i67, i4) :|: 1 <= i80 && 0 < 1 && 0 <= o91 && 0 < o90 && 2 <= i81 && 1 <= i67 && 0 <= o90 && 0 <= i80 && 0 < i80 && 1 <= i81
main_Load_1(i2, i4, static) -{29,29}> langle_init_rangle_Load_313(1, i2, 0, i2, i4) :|: 0 >= 0 && 1 <= i2 && static'1 <= static''' + 1 && 0 <= 0 && 0 <= 2 && 0 <= static''' && 0 < 1 && static''' <= static + 2 && 0 <= 1 && 0 <= static && 0 < i2 && 0 <= static'1 && 0 < 2
main_NULL_689(i67, i4, x, i137) -{1,1}> main_Load_653(i67, i4, 0, i137) :|: 0 <= 0 && 1 <= i67 && x = 0
createIntList_LE_346(x, o90, i67, i4, o91, i66) -{6,6}> main_Load_653(i67, i4, o90, 0) :|: 0 < o90 && 0 <= 0 && 0 <= 1 && 1 <= i67 && 0 <= o90 && 0 <= o91 && 1 <= i66 && 0 <= 2 && 0 <= i66 && x = 0
main_GT_671(i67, i4, i144, o228, i137, o229) -{9,9}> main_Load_653(i67, i4, o228''', i137 + 1) :|: 1 <= i144 && 0 <= o228''' && o228''' <= o228 + i146' && 0 < o228''' && i137 + 1 = i148' && 0 <= i146' && i144 - 1 = i146' && 0 <= o229 && 1 <= i67 && o228''' < o228 && 0 < i144 && 0 < o228
main_GT_671(i67, i4, i143, o228, i137, o229) -{5,5}> main_NULL_689(i67, i4, o229, i137) :|: 0 < o228 && 0 <= o229 && 1 <= i67 && i143 <= 0
main_Load_653(i67, i4, o217, i137) -{4,4}> main_GT_671(i67, i4, i142', o217, i137, o229') :|: 0 <= o229' && 0 < o217 && o229' < o217 && 1 <= i67 && -1 * o217 < i142' && 0 <= o217 && i142' < o217
langle_init_rangle_Load_313(o90, i66, o91, i67, i4) -{10,10}> createIntList_LE_346(i66 + -1, o90''' + o91, i67, i4, o91, i66) :|: o90 < o90''' && 0 <= i73' && 0 < o90 && 0 < o90'1 && o90'1 <= o90''' + o91 && 1 <= i66 && 1 <= i67 && 0 <= o91 && i66 + -1 = i73' && o90''' <= o90 + i66 && o90'1 = o90''' + o91 && 0 < o90'''
main_NULL_689(i67, i4, o230, i137) -{6,6}> main_Load_653(i67, i4, o230, i137 * i4) :|: 0 <= o230 && 1 <= i67 && 0 < o230 && i137 * i4 = i150'

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

Simplified expressions.

createIntList_LE_346(i80, o90, i67, i4, o91, i81) -{9,9}> langle_init_rangle_Load_313(1, i80, o90, i67, i4) :|: 1 <= i80 && 0 < 1 && 0 <= o91 && 0 < o90 && 2 <= i81 && 1 <= i67 && 0 <= o90 && 0 <= i80 && 0 < i80 && 1 <= i81
was transformed to
createIntList_LE_346(i80, o90, i67, i4, o91, i81) -{9,9}> langle_init_rangle_Load_313(1, i80, o90, i67, i4) :|: 1 <= i80 && 0 <= o91 && 0 < o90 && 2 <= i81 && 1 <= i67 && 0 < i80 && 1 <= i81

main_Load_1(i2, i4, static) -{29,29}> langle_init_rangle_Load_313(1, i2, 0, i2, i4) :|: 0 >= 0 && 1 <= i2 && static'1 <= static''' + 1 && 0 <= 0 && 0 <= 2 && 0 <= static''' && 0 < 1 && static''' <= static + 2 && 0 <= 1 && 0 <= static && 0 < i2 && 0 <= static'1 && 0 < 2
was transformed to
main_Load_1(i2, i4, static) -{29,29}> langle_init_rangle_Load_313(1, i2, 0, i2, i4) :|: 1 <= i2 && static'1 <= static''' + 1 && 0 <= static''' && static''' <= static + 2 && 0 <= static && 0 < i2 && 0 <= static'1

main_NULL_689(i67, i4, x, i137) -{1,1}> main_Load_653(i67, i4, 0, i137) :|: 0 <= 0 && 1 <= i67 && x = 0
was transformed to
main_NULL_689(i67, i4, x, i137) -{1,1}> main_Load_653(i67, i4, 0, i137) :|: 1 <= i67 && x = 0

createIntList_LE_346(x, o90, i67, i4, o91, i66) -{6,6}> main_Load_653(i67, i4, o90, 0) :|: 0 < o90 && 0 <= 0 && 0 <= 1 && 1 <= i67 && 0 <= o90 && 0 <= o91 && 1 <= i66 && 0 <= 2 && 0 <= i66 && x = 0
was transformed to
createIntList_LE_346(x, o90, i67, i4, o91, i66) -{6,6}> main_Load_653(i67, i4, o90, 0) :|: 0 < o90 && 1 <= i67 && 0 <= o91 && 1 <= i66 && 0 <= i66 && x = 0

langle_init_rangle_Load_313(o90, i66, o91, i67, i4) -{10,10}> createIntList_LE_346(i66 + -1, o90''' + o91, i67, i4, o91, i66) :|: o90 < o90''' && 0 <= i73' && 0 < o90 && 0 < o90'1 && o90'1 <= o90''' + o91 && 1 <= i66 && 1 <= i67 && 0 <= o91 && i66 + -1 = i73' && o90''' <= o90 + i66 && o90'1 = o90''' + o91 && 0 < o90'''
was transformed to
langle_init_rangle_Load_313(o90, i66, o91, i67, i4) -{10,10}> createIntList_LE_346(i66 - 1, o90''' + o91, i67, i4, o91, i66) :|: o90 < o90''' && 0 <= i73' && 0 < o90 && 0 < o90'1 && 1 <= i66 && 1 <= i67 && 0 <= o91 && i66 - 1 = i73' && o90''' <= o90 + i66 && o90'1 = o90''' + o91 && 0 < o90'''

main_Load_653(i67, i4, o217, i137) -{4,4}> main_GT_671(i67, i4, i142', o217, i137, o229') :|: 0 <= o229' && 0 < o217 && o229' < o217 && 1 <= i67 && -1 * o217 < i142' && 0 <= o217 && i142' < o217
was transformed to
main_Load_653(i67, i4, o217, i137) -{4,4}> main_GT_671(i67, i4, i142', o217, i137, o229') :|: 0 <= o229' && 0 < o217 && o229' < o217 && 1 <= i67 && -1 * o217 < i142' && i142' < o217

main_GT_671(i67, i4, i144, o228, i137, o229) -{9,9}> main_Load_653(i67, i4, o228''', i137 + 1) :|: 1 <= i144 && 0 <= o228''' && o228''' <= o228 + i146' && 0 < o228''' && i137 + 1 = i148' && 0 <= i146' && i144 - 1 = i146' && 0 <= o229 && 1 <= i67 && o228''' < o228 && 0 < i144 && 0 < o228
was transformed to
main_GT_671(i67, i4, i144, o228, i137, o229) -{9,9}> main_Load_653(i67, i4, o228''', i137 + 1) :|: 1 <= i144 && o228''' <= o228 + i146' && 0 < o228''' && i137 + 1 = i148' && 0 <= i146' && i144 - 1 = i146' && 0 <= o229 && 1 <= i67 && o228''' < o228 && 0 < i144 && 0 < o228

main_NULL_689(i67, i4, o230, i137) -{6,6}> main_Load_653(i67, i4, o230, i137 * i4) :|: 0 <= o230 && 1 <= i67 && 0 < o230 && i137 * i4 = i150'
was transformed to
main_NULL_689(i67, i4, o230, i137) -{6,6}> main_Load_653(i67, i4, o230, i137 * i4) :|: 1 <= i67 && 0 < o230 && i137 * i4 = i150'

(38) Obligation:

IntTrs with 9 rules
Start term: main_Load_1(#0, #1, static)
Considered paths: all paths from start
Rules:
main_Load_1(i2, i4, static) -{29,29}> langle_init_rangle_Load_313(1, i2, 0, i2, i4) :|: 1 <= i2 && static'1 <= static''' + 1 && 0 <= static''' && static''' <= static + 2 && 0 <= static && 0 < i2 && 0 <= static'1
createIntList_LE_346(i80, o90, i67, i4, o91, i81) -{9,9}> langle_init_rangle_Load_313(1, i80, o90, i67, i4) :|: 1 <= i80 && 0 <= o91 && 0 < o90 && 2 <= i81 && 1 <= i67 && 0 < i80 && 1 <= i81
main_NULL_689(i67, i4, o230, i137) -{6,6}> main_Load_653(i67, i4, o230, i137 * i4) :|: 1 <= i67 && 0 < o230 && i137 * i4 = i150'
createIntList_LE_346(x, o90, i67, i4, o91, i66) -{6,6}> main_Load_653(i67, i4, o90, 0) :|: 0 < o90 && 1 <= i67 && 0 <= o91 && 1 <= i66 && 0 <= i66 && x = 0
main_GT_671(i67, i4, i143, o228, i137, o229) -{5,5}> main_NULL_689(i67, i4, o229, i137) :|: 0 < o228 && 0 <= o229 && 1 <= i67 && i143 <= 0
main_Load_653(i67, i4, o217, i137) -{4,4}> main_GT_671(i67, i4, i142', o217, i137, o229') :|: 0 <= o229' && 0 < o217 && o229' < o217 && 1 <= i67 && -1 * o217 < i142' && i142' < o217
main_NULL_689(i67, i4, x, i137) -{1,1}> main_Load_653(i67, i4, 0, i137) :|: 1 <= i67 && x = 0
langle_init_rangle_Load_313(o90, i66, o91, i67, i4) -{10,10}> createIntList_LE_346(i66 - 1, o90''' + o91, i67, i4, o91, i66) :|: o90 < o90''' && 0 <= i73' && 0 < o90 && 0 < o90'1 && 1 <= i66 && 1 <= i67 && 0 <= o91 && i66 - 1 = i73' && o90''' <= o90 + i66 && o90'1 = o90''' + o91 && 0 < o90'''
main_GT_671(i67, i4, i144, o228, i137, o229) -{9,9}> main_Load_653(i67, i4, o228''', i137 + 1) :|: 1 <= i144 && o228''' <= o228 + i146' && 0 < o228''' && i137 + 1 = i148' && 0 <= i146' && i144 - 1 = i146' && 0 <= o229 && 1 <= i67 && o228''' < o228 && 0 < i144 && 0 < o228

(39) koat Proof (EQUIVALENT transformation)

YES(?, 263*ar_0 + 150*ar_0^2 + 35)

Initial complexity problem:
1: T:
(Comp: ?, Cost: 29) main_Load_1(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(langle_init_rangle_Load_313(1, ar_0, 0, ar_0, ar_1, arityPad)) [ 1 <= ar_0 /\ static'1 <= static''' + 1 /\ 0 <= static''' /\ static''' <= ar_2 + 2 /\ 0 <= ar_2 /\ 0 < ar_0 /\ 0 <= static'1 ]
(Comp: ?, Cost: 9) createIntList_LE_346(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(langle_init_rangle_Load_313(1, ar_0, ar_1, ar_2, ar_3, arityPad)) [ 1 <= ar_0 /\ 0 <= ar_4 /\ 0 < ar_1 /\ 2 <= ar_5 /\ 1 <= ar_2 /\ 0 < ar_0 /\ 1 <= ar_5 ]
(Comp: ?, Cost: 6) main_NULL_689(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(main_Load_653(ar_0, ar_1, ar_2, ar_1*ar_3, arityPad, arityPad)) [ 1 <= ar_0 /\ 0 < ar_2 /\ ar_1*ar_3 = i150' ]
(Comp: ?, Cost: 6) createIntList_LE_346(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(main_Load_653(ar_2, ar_3, ar_1, 0, arityPad, arityPad)) [ 0 < ar_1 /\ 1 <= ar_2 /\ 0 <= ar_4 /\ 1 <= ar_5 /\ 0 <= ar_5 /\ ar_0 = 0 ]
(Comp: ?, Cost: 5) main_GT_671(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(main_NULL_689(ar_0, ar_1, ar_5, ar_4, arityPad, arityPad)) [ 0 < ar_3 /\ 0 <= ar_5 /\ 1 <= ar_0 /\ ar_2 <= 0 ]
(Comp: ?, Cost: 4) main_Load_653(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(main_GT_671(ar_0, ar_1, i142', ar_2, ar_3, o229')) [ 0 <= o229' /\ 0 < ar_2 /\ o229' < ar_2 /\ 1 <= ar_0 /\ -ar_2 < i142' /\ i142' < ar_2 ]
(Comp: ?, Cost: 1) main_NULL_689(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(main_Load_653(ar_0, ar_1, 0, ar_3, arityPad, arityPad)) [ 1 <= ar_0 /\ ar_2 = 0 ]
(Comp: ?, Cost: 10) langle_init_rangle_Load_313(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(createIntList_LE_346(ar_1 - 1, o90''' + ar_2, ar_3, ar_4, ar_2, ar_1)) [ ar_0 < o90''' /\ 0 <= i73' /\ 0 < ar_0 /\ 0 < o90'1 /\ 1 <= ar_1 /\ 1 <= ar_3 /\ 0 <= ar_2 /\ ar_1 - 1 = i73' /\ o90''' <= ar_0 + ar_1 /\ o90'1 = o90''' + ar_2 /\ 0 < o90''' ]
(Comp: ?, Cost: 9) main_GT_671(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(main_Load_653(ar_0, ar_1, o228''', ar_4 + 1, arityPad, arityPad)) [ 1 <= ar_2 /\ o228''' <= ar_3 + i146' /\ 0 < o228''' /\ ar_4 + 1 = i148' /\ 0 <= i146' /\ ar_2 - 1 = i146' /\ 0 <= ar_5 /\ 1 <= ar_0 /\ o228''' < ar_3 /\ 0 < ar_2 /\ 0 < ar_3 ]
(Comp: 1, Cost: 0) koat_start(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(main_Load_1(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5)) [ 0 <= 0 ]
start location: koat_start
leaf cost: 0

Repeatedly propagating knowledge in problem 1 produces the following problem:
2: T:
(Comp: 1, Cost: 29) main_Load_1(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(langle_init_rangle_Load_313(1, ar_0, 0, ar_0, ar_1, arityPad)) [ 1 <= ar_0 /\ static'1 <= static''' + 1 /\ 0 <= static''' /\ static''' <= ar_2 + 2 /\ 0 <= ar_2 /\ 0 < ar_0 /\ 0 <= static'1 ]
(Comp: ?, Cost: 9) createIntList_LE_346(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(langle_init_rangle_Load_313(1, ar_0, ar_1, ar_2, ar_3, arityPad)) [ 1 <= ar_0 /\ 0 <= ar_4 /\ 0 < ar_1 /\ 2 <= ar_5 /\ 1 <= ar_2 /\ 0 < ar_0 /\ 1 <= ar_5 ]
(Comp: ?, Cost: 6) main_NULL_689(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(main_Load_653(ar_0, ar_1, ar_2, ar_1*ar_3, arityPad, arityPad)) [ 1 <= ar_0 /\ 0 < ar_2 /\ ar_1*ar_3 = i150' ]
(Comp: ?, Cost: 6) createIntList_LE_346(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(main_Load_653(ar_2, ar_3, ar_1, 0, arityPad, arityPad)) [ 0 < ar_1 /\ 1 <= ar_2 /\ 0 <= ar_4 /\ 1 <= ar_5 /\ 0 <= ar_5 /\ ar_0 = 0 ]
(Comp: ?, Cost: 5) main_GT_671(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(main_NULL_689(ar_0, ar_1, ar_5, ar_4, arityPad, arityPad)) [ 0 < ar_3 /\ 0 <= ar_5 /\ 1 <= ar_0 /\ ar_2 <= 0 ]
(Comp: ?, Cost: 4) main_Load_653(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(main_GT_671(ar_0, ar_1, i142', ar_2, ar_3, o229')) [ 0 <= o229' /\ 0 < ar_2 /\ o229' < ar_2 /\ 1 <= ar_0 /\ -ar_2 < i142' /\ i142' < ar_2 ]
(Comp: ?, Cost: 1) main_NULL_689(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(main_Load_653(ar_0, ar_1, 0, ar_3, arityPad, arityPad)) [ 1 <= ar_0 /\ ar_2 = 0 ]
(Comp: ?, Cost: 10) langle_init_rangle_Load_313(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(createIntList_LE_346(ar_1 - 1, o90''' + ar_2, ar_3, ar_4, ar_2, ar_1)) [ ar_0 < o90''' /\ 0 <= i73' /\ 0 < ar_0 /\ 0 < o90'1 /\ 1 <= ar_1 /\ 1 <= ar_3 /\ 0 <= ar_2 /\ ar_1 - 1 = i73' /\ o90''' <= ar_0 + ar_1 /\ o90'1 = o90''' + ar_2 /\ 0 < o90''' ]
(Comp: ?, Cost: 9) main_GT_671(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(main_Load_653(ar_0, ar_1, o228''', ar_4 + 1, arityPad, arityPad)) [ 1 <= ar_2 /\ o228''' <= ar_3 + i146' /\ 0 < o228''' /\ ar_4 + 1 = i148' /\ 0 <= i146' /\ ar_2 - 1 = i146' /\ 0 <= ar_5 /\ 1 <= ar_0 /\ o228''' < ar_3 /\ 0 < ar_2 /\ 0 < ar_3 ]
(Comp: 1, Cost: 0) koat_start(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(main_Load_1(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5)) [ 0 <= 0 ]
start location: koat_start
leaf cost: 0

A polynomial rank function with
Pol(main_Load_1) = 1
Pol(langle_init_rangle_Load_313) = 1
Pol(createIntList_LE_346) = 1
Pol(main_NULL_689) = 0
Pol(main_Load_653) = 0
Pol(main_GT_671) = 0
Pol(koat_start) = 1
orients all transitions weakly and the transition
createIntList_LE_346(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(main_Load_653(ar_2, ar_3, ar_1, 0, arityPad, arityPad)) [ 0 < ar_1 /\ 1 <= ar_2 /\ 0 <= ar_4 /\ 1 <= ar_5 /\ 0 <= ar_5 /\ ar_0 = 0 ]
strictly and produces the following problem:
3: T:
(Comp: 1, Cost: 29) main_Load_1(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(langle_init_rangle_Load_313(1, ar_0, 0, ar_0, ar_1, arityPad)) [ 1 <= ar_0 /\ static'1 <= static''' + 1 /\ 0 <= static''' /\ static''' <= ar_2 + 2 /\ 0 <= ar_2 /\ 0 < ar_0 /\ 0 <= static'1 ]
(Comp: ?, Cost: 9) createIntList_LE_346(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(langle_init_rangle_Load_313(1, ar_0, ar_1, ar_2, ar_3, arityPad)) [ 1 <= ar_0 /\ 0 <= ar_4 /\ 0 < ar_1 /\ 2 <= ar_5 /\ 1 <= ar_2 /\ 0 < ar_0 /\ 1 <= ar_5 ]
(Comp: ?, Cost: 6) main_NULL_689(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(main_Load_653(ar_0, ar_1, ar_2, ar_1*ar_3, arityPad, arityPad)) [ 1 <= ar_0 /\ 0 < ar_2 /\ ar_1*ar_3 = i150' ]
(Comp: 1, Cost: 6) createIntList_LE_346(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(main_Load_653(ar_2, ar_3, ar_1, 0, arityPad, arityPad)) [ 0 < ar_1 /\ 1 <= ar_2 /\ 0 <= ar_4 /\ 1 <= ar_5 /\ 0 <= ar_5 /\ ar_0 = 0 ]
(Comp: ?, Cost: 5) main_GT_671(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(main_NULL_689(ar_0, ar_1, ar_5, ar_4, arityPad, arityPad)) [ 0 < ar_3 /\ 0 <= ar_5 /\ 1 <= ar_0 /\ ar_2 <= 0 ]
(Comp: ?, Cost: 4) main_Load_653(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(main_GT_671(ar_0, ar_1, i142', ar_2, ar_3, o229')) [ 0 <= o229' /\ 0 < ar_2 /\ o229' < ar_2 /\ 1 <= ar_0 /\ -ar_2 < i142' /\ i142' < ar_2 ]
(Comp: ?, Cost: 1) main_NULL_689(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(main_Load_653(ar_0, ar_1, 0, ar_3, arityPad, arityPad)) [ 1 <= ar_0 /\ ar_2 = 0 ]
(Comp: ?, Cost: 10) langle_init_rangle_Load_313(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(createIntList_LE_346(ar_1 - 1, o90''' + ar_2, ar_3, ar_4, ar_2, ar_1)) [ ar_0 < o90''' /\ 0 <= i73' /\ 0 < ar_0 /\ 0 < o90'1 /\ 1 <= ar_1 /\ 1 <= ar_3 /\ 0 <= ar_2 /\ ar_1 - 1 = i73' /\ o90''' <= ar_0 + ar_1 /\ o90'1 = o90''' + ar_2 /\ 0 < o90''' ]
(Comp: ?, Cost: 9) main_GT_671(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(main_Load_653(ar_0, ar_1, o228''', ar_4 + 1, arityPad, arityPad)) [ 1 <= ar_2 /\ o228''' <= ar_3 + i146' /\ 0 < o228''' /\ ar_4 + 1 = i148' /\ 0 <= i146' /\ ar_2 - 1 = i146' /\ 0 <= ar_5 /\ 1 <= ar_0 /\ o228''' < ar_3 /\ 0 < ar_2 /\ 0 < ar_3 ]
(Comp: 1, Cost: 0) koat_start(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(main_Load_1(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5)) [ 0 <= 0 ]
start location: koat_start
leaf cost: 0

A polynomial rank function with
Pol(main_Load_1) = 2*V_1
Pol(langle_init_rangle_Load_313) = 2*V_2 - 1
Pol(createIntList_LE_346) = 2*V_1
Pol(main_NULL_689) = 0
Pol(main_Load_653) = 0
Pol(main_GT_671) = 0
Pol(koat_start) = 2*V_1
orients all transitions weakly and the transitions
langle_init_rangle_Load_313(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(createIntList_LE_346(ar_1 - 1, o90''' + ar_2, ar_3, ar_4, ar_2, ar_1)) [ ar_0 < o90''' /\ 0 <= i73' /\ 0 < ar_0 /\ 0 < o90'1 /\ 1 <= ar_1 /\ 1 <= ar_3 /\ 0 <= ar_2 /\ ar_1 - 1 = i73' /\ o90''' <= ar_0 + ar_1 /\ o90'1 = o90''' + ar_2 /\ 0 < o90''' ]
createIntList_LE_346(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(langle_init_rangle_Load_313(1, ar_0, ar_1, ar_2, ar_3, arityPad)) [ 1 <= ar_0 /\ 0 <= ar_4 /\ 0 < ar_1 /\ 2 <= ar_5 /\ 1 <= ar_2 /\ 0 < ar_0 /\ 1 <= ar_5 ]
strictly and produces the following problem:
4: T:
(Comp: 1, Cost: 29) main_Load_1(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(langle_init_rangle_Load_313(1, ar_0, 0, ar_0, ar_1, arityPad)) [ 1 <= ar_0 /\ static'1 <= static''' + 1 /\ 0 <= static''' /\ static''' <= ar_2 + 2 /\ 0 <= ar_2 /\ 0 < ar_0 /\ 0 <= static'1 ]
(Comp: 2*ar_0, Cost: 9) createIntList_LE_346(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(langle_init_rangle_Load_313(1, ar_0, ar_1, ar_2, ar_3, arityPad)) [ 1 <= ar_0 /\ 0 <= ar_4 /\ 0 < ar_1 /\ 2 <= ar_5 /\ 1 <= ar_2 /\ 0 < ar_0 /\ 1 <= ar_5 ]
(Comp: ?, Cost: 6) main_NULL_689(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(main_Load_653(ar_0, ar_1, ar_2, ar_1*ar_3, arityPad, arityPad)) [ 1 <= ar_0 /\ 0 < ar_2 /\ ar_1*ar_3 = i150' ]
(Comp: 1, Cost: 6) createIntList_LE_346(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(main_Load_653(ar_2, ar_3, ar_1, 0, arityPad, arityPad)) [ 0 < ar_1 /\ 1 <= ar_2 /\ 0 <= ar_4 /\ 1 <= ar_5 /\ 0 <= ar_5 /\ ar_0 = 0 ]
(Comp: ?, Cost: 5) main_GT_671(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(main_NULL_689(ar_0, ar_1, ar_5, ar_4, arityPad, arityPad)) [ 0 < ar_3 /\ 0 <= ar_5 /\ 1 <= ar_0 /\ ar_2 <= 0 ]
(Comp: ?, Cost: 4) main_Load_653(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(main_GT_671(ar_0, ar_1, i142', ar_2, ar_3, o229')) [ 0 <= o229' /\ 0 < ar_2 /\ o229' < ar_2 /\ 1 <= ar_0 /\ -ar_2 < i142' /\ i142' < ar_2 ]
(Comp: ?, Cost: 1) main_NULL_689(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(main_Load_653(ar_0, ar_1, 0, ar_3, arityPad, arityPad)) [ 1 <= ar_0 /\ ar_2 = 0 ]
(Comp: 2*ar_0, Cost: 10) langle_init_rangle_Load_313(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(createIntList_LE_346(ar_1 - 1, o90''' + ar_2, ar_3, ar_4, ar_2, ar_1)) [ ar_0 < o90''' /\ 0 <= i73' /\ 0 < ar_0 /\ 0 < o90'1 /\ 1 <= ar_1 /\ 1 <= ar_3 /\ 0 <= ar_2 /\ ar_1 - 1 = i73' /\ o90''' <= ar_0 + ar_1 /\ o90'1 = o90''' + ar_2 /\ 0 < o90''' ]
(Comp: ?, Cost: 9) main_GT_671(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(main_Load_653(ar_0, ar_1, o228''', ar_4 + 1, arityPad, arityPad)) [ 1 <= ar_2 /\ o228''' <= ar_3 + i146' /\ 0 < o228''' /\ ar_4 + 1 = i148' /\ 0 <= i146' /\ ar_2 - 1 = i146' /\ 0 <= ar_5 /\ 1 <= ar_0 /\ o228''' < ar_3 /\ 0 < ar_2 /\ 0 < ar_3 ]
(Comp: 1, Cost: 0) koat_start(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(main_Load_1(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5)) [ 0 <= 0 ]
start location: koat_start
leaf cost: 0

Applied AI with 'oct' on problem 4 to obtain the following invariants:
For symbol createIntList_LE_346: X_3 - X_6 >= 0 /\ X_1 - X_6 + 1 >= 0 /\ X_6 - 1 >= 0 /\ X_5 + X_6 - 1 >= 0 /\ X_3 + X_6 - 2 >= 0 /\ X_2 + X_6 - 3 >= 0 /\ X_1 + X_6 - 1 >= 0 /\ -X_1 + X_6 - 1 >= 0 /\ X_2 - X_5 - 2 >= 0 /\ X_5 >= 0 /\ X_3 + X_5 - 1 >= 0 /\ X_2 + X_5 - 2 >= 0 /\ X_1 + X_5 >= 0 /\ X_3 - 1 >= 0 /\ X_2 + X_3 - 3 >= 0 /\ X_1 + X_3 - 1 >= 0 /\ -X_1 + X_3 - 1 >= 0 /\ X_2 - 2 >= 0 /\ X_1 + X_2 - 2 >= 0 /\ X_1 >= 0
For symbol langle_init_rangle_Load_313: X_4 - 1 >= 0 /\ X_3 + X_4 - 1 >= 0 /\ X_2 + X_4 - 2 >= 0 /\ -X_2 + X_4 >= 0 /\ X_1 + X_4 - 2 >= 0 /\ -X_1 + X_4 >= 0 /\ X_3 >= 0 /\ X_2 + X_3 - 1 >= 0 /\ X_1 + X_3 - 1 >= 0 /\ -X_1 + X_3 + 1 >= 0 /\ X_2 - 1 >= 0 /\ X_1 + X_2 - 2 >= 0 /\ -X_1 + X_2 >= 0 /\ -X_1 + 1 >= 0 /\ X_1 - 1 >= 0
For symbol main_GT_671: X_4 - X_6 - 1 >= 0 /\ X_6 >= 0 /\ X_4 + X_6 - 1 >= 0 /\ X_1 + X_6 - 1 >= 0 /\ X_4 - 1 >= 0 /\ X_3 + X_4 - 1 >= 0 /\ -X_3 + X_4 - 1 >= 0 /\ X_1 + X_4 - 2 >= 0 /\ X_1 - 1 >= 0
For symbol main_Load_653: X_1 - 1 >= 0
For symbol main_NULL_689: X_3 >= 0 /\ X_1 + X_3 - 1 >= 0 /\ X_1 - 1 >= 0

This yielded the following problem:
5: T:
(Comp: 1, Cost: 0) koat_start(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(main_Load_1(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5)) [ 0 <= 0 ]
(Comp: ?, Cost: 9) main_GT_671(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(main_Load_653(ar_0, ar_1, o228''', ar_4 + 1, arityPad, arityPad)) [ ar_3 - ar_5 - 1 >= 0 /\ ar_5 >= 0 /\ ar_3 + ar_5 - 1 >= 0 /\ ar_0 + ar_5 - 1 >= 0 /\ ar_3 - 1 >= 0 /\ ar_2 + ar_3 - 1 >= 0 /\ -ar_2 + ar_3 - 1 >= 0 /\ ar_0 + ar_3 - 2 >= 0 /\ ar_0 - 1 >= 0 /\ 1 <= ar_2 /\ o228''' <= ar_3 + i146' /\ 0 < o228''' /\ ar_4 + 1 = i148' /\ 0 <= i146' /\ ar_2 - 1 = i146' /\ 0 <= ar_5 /\ 1 <= ar_0 /\ o228''' < ar_3 /\ 0 < ar_2 /\ 0 < ar_3 ]
(Comp: 2*ar_0, Cost: 10) langle_init_rangle_Load_313(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(createIntList_LE_346(ar_1 - 1, o90''' + ar_2, ar_3, ar_4, ar_2, ar_1)) [ ar_3 - 1 >= 0 /\ ar_2 + ar_3 - 1 >= 0 /\ ar_1 + ar_3 - 2 >= 0 /\ -ar_1 + ar_3 >= 0 /\ ar_0 + ar_3 - 2 >= 0 /\ -ar_0 + ar_3 >= 0 /\ ar_2 >= 0 /\ ar_1 + ar_2 - 1 >= 0 /\ ar_0 + ar_2 - 1 >= 0 /\ -ar_0 + ar_2 + 1 >= 0 /\ ar_1 - 1 >= 0 /\ ar_0 + ar_1 - 2 >= 0 /\ -ar_0 + ar_1 >= 0 /\ -ar_0 + 1 >= 0 /\ ar_0 - 1 >= 0 /\ ar_0 < o90''' /\ 0 <= i73' /\ 0 < ar_0 /\ 0 < o90'1 /\ 1 <= ar_1 /\ 1 <= ar_3 /\ 0 <= ar_2 /\ ar_1 - 1 = i73' /\ o90''' <= ar_0 + ar_1 /\ o90'1 = o90''' + ar_2 /\ 0 < o90''' ]
(Comp: ?, Cost: 1) main_NULL_689(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(main_Load_653(ar_0, ar_1, 0, ar_3, arityPad, arityPad)) [ ar_2 >= 0 /\ ar_0 + ar_2 - 1 >= 0 /\ ar_0 - 1 >= 0 /\ 1 <= ar_0 /\ ar_2 = 0 ]
(Comp: ?, Cost: 4) main_Load_653(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(main_GT_671(ar_0, ar_1, i142', ar_2, ar_3, o229')) [ ar_0 - 1 >= 0 /\ 0 <= o229' /\ 0 < ar_2 /\ o229' < ar_2 /\ 1 <= ar_0 /\ -ar_2 < i142' /\ i142' < ar_2 ]
(Comp: ?, Cost: 5) main_GT_671(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(main_NULL_689(ar_0, ar_1, ar_5, ar_4, arityPad, arityPad)) [ ar_3 - ar_5 - 1 >= 0 /\ ar_5 >= 0 /\ ar_3 + ar_5 - 1 >= 0 /\ ar_0 + ar_5 - 1 >= 0 /\ ar_3 - 1 >= 0 /\ ar_2 + ar_3 - 1 >= 0 /\ -ar_2 + ar_3 - 1 >= 0 /\ ar_0 + ar_3 - 2 >= 0 /\ ar_0 - 1 >= 0 /\ 0 < ar_3 /\ 0 <= ar_5 /\ 1 <= ar_0 /\ ar_2 <= 0 ]
(Comp: 1, Cost: 6) createIntList_LE_346(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(main_Load_653(ar_2, ar_3, ar_1, 0, arityPad, arityPad)) [ ar_2 - ar_5 >= 0 /\ ar_0 - ar_5 + 1 >= 0 /\ ar_5 - 1 >= 0 /\ ar_4 + ar_5 - 1 >= 0 /\ ar_2 + ar_5 - 2 >= 0 /\ ar_1 + ar_5 - 3 >= 0 /\ ar_0 + ar_5 - 1 >= 0 /\ -ar_0 + ar_5 - 1 >= 0 /\ ar_1 - ar_4 - 2 >= 0 /\ ar_4 >= 0 /\ ar_2 + ar_4 - 1 >= 0 /\ ar_1 + ar_4 - 2 >= 0 /\ ar_0 + ar_4 >= 0 /\ ar_2 - 1 >= 0 /\ ar_1 + ar_2 - 3 >= 0 /\ ar_0 + ar_2 - 1 >= 0 /\ -ar_0 + ar_2 - 1 >= 0 /\ ar_1 - 2 >= 0 /\ ar_0 + ar_1 - 2 >= 0 /\ ar_0 >= 0 /\ 0 < ar_1 /\ 1 <= ar_2 /\ 0 <= ar_4 /\ 1 <= ar_5 /\ 0 <= ar_5 /\ ar_0 = 0 ]
(Comp: ?, Cost: 6) main_NULL_689(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(main_Load_653(ar_0, ar_1, ar_2, ar_1*ar_3, arityPad, arityPad)) [ ar_2 >= 0 /\ ar_0 + ar_2 - 1 >= 0 /\ ar_0 - 1 >= 0 /\ 1 <= ar_0 /\ 0 < ar_2 /\ ar_1*ar_3 = i150' ]
(Comp: 2*ar_0, Cost: 9) createIntList_LE_346(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(langle_init_rangle_Load_313(1, ar_0, ar_1, ar_2, ar_3, arityPad)) [ ar_2 - ar_5 >= 0 /\ ar_0 - ar_5 + 1 >= 0 /\ ar_5 - 1 >= 0 /\ ar_4 + ar_5 - 1 >= 0 /\ ar_2 + ar_5 - 2 >= 0 /\ ar_1 + ar_5 - 3 >= 0 /\ ar_0 + ar_5 - 1 >= 0 /\ -ar_0 + ar_5 - 1 >= 0 /\ ar_1 - ar_4 - 2 >= 0 /\ ar_4 >= 0 /\ ar_2 + ar_4 - 1 >= 0 /\ ar_1 + ar_4 - 2 >= 0 /\ ar_0 + ar_4 >= 0 /\ ar_2 - 1 >= 0 /\ ar_1 + ar_2 - 3 >= 0 /\ ar_0 + ar_2 - 1 >= 0 /\ -ar_0 + ar_2 - 1 >= 0 /\ ar_1 - 2 >= 0 /\ ar_0 + ar_1 - 2 >= 0 /\ ar_0 >= 0 /\ 1 <= ar_0 /\ 0 <= ar_4 /\ 0 < ar_1 /\ 2 <= ar_5 /\ 1 <= ar_2 /\ 0 < ar_0 /\ 1 <= ar_5 ]
(Comp: 1, Cost: 29) main_Load_1(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(langle_init_rangle_Load_313(1, ar_0, 0, ar_0, ar_1, arityPad)) [ 1 <= ar_0 /\ static'1 <= static''' + 1 /\ 0 <= static''' /\ static''' <= ar_2 + 2 /\ 0 <= ar_2 /\ 0 < ar_0 /\ 0 <= static'1 ]
start location: koat_start
leaf cost: 0

A polynomial rank function with
Pol(main_NULL_689) = 3*V_3 + 1
Pol(main_Load_653) = 3*V_3
Pol(main_GT_671) = 3*V_4 - 1
and size complexities
S("main_Load_1(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(langle_init_rangle_Load_313(1, ar_0, 0, ar_0, ar_1, arityPad)) [ 1 <= ar_0 /\\ static'1 <= static''' + 1 /\\ 0 <= static''' /\\ static''' <= ar_2 + 2 /\\ 0 <= ar_2 /\\ 0 < ar_0 /\\ 0 <= static'1 ]", 0-0) = 1
S("main_Load_1(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(langle_init_rangle_Load_313(1, ar_0, 0, ar_0, ar_1, arityPad)) [ 1 <= ar_0 /\\ static'1 <= static''' + 1 /\\ 0 <= static''' /\\ static''' <= ar_2 + 2 /\\ 0 <= ar_2 /\\ 0 < ar_0 /\\ 0 <= static'1 ]", 0-1) = ar_0
S("main_Load_1(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(langle_init_rangle_Load_313(1, ar_0, 0, ar_0, ar_1, arityPad)) [ 1 <= ar_0 /\\ static'1 <= static''' + 1 /\\ 0 <= static''' /\\ static''' <= ar_2 + 2 /\\ 0 <= ar_2 /\\ 0 < ar_0 /\\ 0 <= static'1 ]", 0-2) = 0
S("main_Load_1(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(langle_init_rangle_Load_313(1, ar_0, 0, ar_0, ar_1, arityPad)) [ 1 <= ar_0 /\\ static'1 <= static''' + 1 /\\ 0 <= static''' /\\ static''' <= ar_2 + 2 /\\ 0 <= ar_2 /\\ 0 < ar_0 /\\ 0 <= static'1 ]", 0-3) = ar_0
S("main_Load_1(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(langle_init_rangle_Load_313(1, ar_0, 0, ar_0, ar_1, arityPad)) [ 1 <= ar_0 /\\ static'1 <= static''' + 1 /\\ 0 <= static''' /\\ static''' <= ar_2 + 2 /\\ 0 <= ar_2 /\\ 0 < ar_0 /\\ 0 <= static'1 ]", 0-4) = ar_1
S("main_Load_1(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(langle_init_rangle_Load_313(1, ar_0, 0, ar_0, ar_1, arityPad)) [ 1 <= ar_0 /\\ static'1 <= static''' + 1 /\\ 0 <= static''' /\\ static''' <= ar_2 + 2 /\\ 0 <= ar_2 /\\ 0 < ar_0 /\\ 0 <= static'1 ]", 0-5) = ?
S("createIntList_LE_346(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(langle_init_rangle_Load_313(1, ar_0, ar_1, ar_2, ar_3, arityPad)) [ ar_2 - ar_5 >= 0 /\\ ar_0 - ar_5 + 1 >= 0 /\\ ar_5 - 1 >= 0 /\\ ar_4 + ar_5 - 1 >= 0 /\\ ar_2 + ar_5 - 2 >= 0 /\\ ar_1 + ar_5 - 3 >= 0 /\\ ar_0 + ar_5 - 1 >= 0 /\\ -ar_0 + ar_5 - 1 >= 0 /\\ ar_1 - ar_4 - 2 >= 0 /\\ ar_4 >= 0 /\\ ar_2 + ar_4 - 1 >= 0 /\\ ar_1 + ar_4 - 2 >= 0 /\\ ar_0 + ar_4 >= 0 /\\ ar_2 - 1 >= 0 /\\ ar_1 + ar_2 - 3 >= 0 /\\ ar_0 + ar_2 - 1 >= 0 /\\ -ar_0 + ar_2 - 1 >= 0 /\\ ar_1 - 2 >= 0 /\\ ar_0 + ar_1 - 2 >= 0 /\\ ar_0 >= 0 /\\ 1 <= ar_0 /\\ 0 <= ar_4 /\\ 0 < ar_1 /\\ 2 <= ar_5 /\\ 1 <= ar_2 /\\ 0 < ar_0 /\\ 1 <= ar_5 ]", 0-0) = 1
S("createIntList_LE_346(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(langle_init_rangle_Load_313(1, ar_0, ar_1, ar_2, ar_3, arityPad)) [ ar_2 - ar_5 >= 0 /\\ ar_0 - ar_5 + 1 >= 0 /\\ ar_5 - 1 >= 0 /\\ ar_4 + ar_5 - 1 >= 0 /\\ ar_2 + ar_5 - 2 >= 0 /\\ ar_1 + ar_5 - 3 >= 0 /\\ ar_0 + ar_5 - 1 >= 0 /\\ -ar_0 + ar_5 - 1 >= 0 /\\ ar_1 - ar_4 - 2 >= 0 /\\ ar_4 >= 0 /\\ ar_2 + ar_4 - 1 >= 0 /\\ ar_1 + ar_4 - 2 >= 0 /\\ ar_0 + ar_4 >= 0 /\\ ar_2 - 1 >= 0 /\\ ar_1 + ar_2 - 3 >= 0 /\\ ar_0 + ar_2 - 1 >= 0 /\\ -ar_0 + ar_2 - 1 >= 0 /\\ ar_1 - 2 >= 0 /\\ ar_0 + ar_1 - 2 >= 0 /\\ ar_0 >= 0 /\\ 1 <= ar_0 /\\ 0 <= ar_4 /\\ 0 < ar_1 /\\ 2 <= ar_5 /\\ 1 <= ar_2 /\\ 0 < ar_0 /\\ 1 <= ar_5 ]", 0-1) = ar_0
S("createIntList_LE_346(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(langle_init_rangle_Load_313(1, ar_0, ar_1, ar_2, ar_3, arityPad)) [ ar_2 - ar_5 >= 0 /\\ ar_0 - ar_5 + 1 >= 0 /\\ ar_5 - 1 >= 0 /\\ ar_4 + ar_5 - 1 >= 0 /\\ ar_2 + ar_5 - 2 >= 0 /\\ ar_1 + ar_5 - 3 >= 0 /\\ ar_0 + ar_5 - 1 >= 0 /\\ -ar_0 + ar_5 - 1 >= 0 /\\ ar_1 - ar_4 - 2 >= 0 /\\ ar_4 >= 0 /\\ ar_2 + ar_4 - 1 >= 0 /\\ ar_1 + ar_4 - 2 >= 0 /\\ ar_0 + ar_4 >= 0 /\\ ar_2 - 1 >= 0 /\\ ar_1 + ar_2 - 3 >= 0 /\\ ar_0 + ar_2 - 1 >= 0 /\\ -ar_0 + ar_2 - 1 >= 0 /\\ ar_1 - 2 >= 0 /\\ ar_0 + ar_1 - 2 >= 0 /\\ ar_0 >= 0 /\\ 1 <= ar_0 /\\ 0 <= ar_4 /\\ 0 < ar_1 /\\ 2 <= ar_5 /\\ 1 <= ar_2 /\\ 0 < ar_0 /\\ 1 <= ar_5 ]", 0-2) = 3*ar_0 + 2*ar_0^2
S("createIntList_LE_346(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(langle_init_rangle_Load_313(1, ar_0, ar_1, ar_2, ar_3, arityPad)) [ ar_2 - ar_5 >= 0 /\\ ar_0 - ar_5 + 1 >= 0 /\\ ar_5 - 1 >= 0 /\\ ar_4 + ar_5 - 1 >= 0 /\\ ar_2 + ar_5 - 2 >= 0 /\\ ar_1 + ar_5 - 3 >= 0 /\\ ar_0 + ar_5 - 1 >= 0 /\\ -ar_0 + ar_5 - 1 >= 0 /\\ ar_1 - ar_4 - 2 >= 0 /\\ ar_4 >= 0 /\\ ar_2 + ar_4 - 1 >= 0 /\\ ar_1 + ar_4 - 2 >= 0 /\\ ar_0 + ar_4 >= 0 /\\ ar_2 - 1 >= 0 /\\ ar_1 + ar_2 - 3 >= 0 /\\ ar_0 + ar_2 - 1 >= 0 /\\ -ar_0 + ar_2 - 1 >= 0 /\\ ar_1 - 2 >= 0 /\\ ar_0 + ar_1 - 2 >= 0 /\\ ar_0 >= 0 /\\ 1 <= ar_0 /\\ 0 <= ar_4 /\\ 0 < ar_1 /\\ 2 <= ar_5 /\\ 1 <= ar_2 /\\ 0 < ar_0 /\\ 1 <= ar_5 ]", 0-3) = ar_0
S("createIntList_LE_346(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(langle_init_rangle_Load_313(1, ar_0, ar_1, ar_2, ar_3, arityPad)) [ ar_2 - ar_5 >= 0 /\\ ar_0 - ar_5 + 1 >= 0 /\\ ar_5 - 1 >= 0 /\\ ar_4 + ar_5 - 1 >= 0 /\\ ar_2 + ar_5 - 2 >= 0 /\\ ar_1 + ar_5 - 3 >= 0 /\\ ar_0 + ar_5 - 1 >= 0 /\\ -ar_0 + ar_5 - 1 >= 0 /\\ ar_1 - ar_4 - 2 >= 0 /\\ ar_4 >= 0 /\\ ar_2 + ar_4 - 1 >= 0 /\\ ar_1 + ar_4 - 2 >= 0 /\\ ar_0 + ar_4 >= 0 /\\ ar_2 - 1 >= 0 /\\ ar_1 + ar_2 - 3 >= 0 /\\ ar_0 + ar_2 - 1 >= 0 /\\ -ar_0 + ar_2 - 1 >= 0 /\\ ar_1 - 2 >= 0 /\\ ar_0 + ar_1 - 2 >= 0 /\\ ar_0 >= 0 /\\ 1 <= ar_0 /\\ 0 <= ar_4 /\\ 0 < ar_1 /\\ 2 <= ar_5 /\\ 1 <= ar_2 /\\ 0 < ar_0 /\\ 1 <= ar_5 ]", 0-4) = ar_1
S("createIntList_LE_346(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(langle_init_rangle_Load_313(1, ar_0, ar_1, ar_2, ar_3, arityPad)) [ ar_2 - ar_5 >= 0 /\\ ar_0 - ar_5 + 1 >= 0 /\\ ar_5 - 1 >= 0 /\\ ar_4 + ar_5 - 1 >= 0 /\\ ar_2 + ar_5 - 2 >= 0 /\\ ar_1 + ar_5 - 3 >= 0 /\\ ar_0 + ar_5 - 1 >= 0 /\\ -ar_0 + ar_5 - 1 >= 0 /\\ ar_1 - ar_4 - 2 >= 0 /\\ ar_4 >= 0 /\\ ar_2 + ar_4 - 1 >= 0 /\\ ar_1 + ar_4 - 2 >= 0 /\\ ar_0 + ar_4 >= 0 /\\ ar_2 - 1 >= 0 /\\ ar_1 + ar_2 - 3 >= 0 /\\ ar_0 + ar_2 - 1 >= 0 /\\ -ar_0 + ar_2 - 1 >= 0 /\\ ar_1 - 2 >= 0 /\\ ar_0 + ar_1 - 2 >= 0 /\\ ar_0 >= 0 /\\ 1 <= ar_0 /\\ 0 <= ar_4 /\\ 0 < ar_1 /\\ 2 <= ar_5 /\\ 1 <= ar_2 /\\ 0 < ar_0 /\\ 1 <= ar_5 ]", 0-5) = ?
S("main_NULL_689(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(main_Load_653(ar_0, ar_1, ar_2, ar_1*ar_3, arityPad, arityPad)) [ ar_2 >= 0 /\\ ar_0 + ar_2 - 1 >= 0 /\\ ar_0 - 1 >= 0 /\\ 1 <= ar_0 /\\ 0 < ar_2 /\\ ar_1*ar_3 = i150' ]", 0-0) = ar_0
S("main_NULL_689(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(main_Load_653(ar_0, ar_1, ar_2, ar_1*ar_3, arityPad, arityPad)) [ ar_2 >= 0 /\\ ar_0 + ar_2 - 1 >= 0 /\\ ar_0 - 1 >= 0 /\\ 1 <= ar_0 /\\ 0 < ar_2 /\\ ar_1*ar_3 = i150' ]", 0-1) = ar_1
S("main_NULL_689(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(main_Load_653(ar_0, ar_1, ar_2, ar_1*ar_3, arityPad, arityPad)) [ ar_2 >= 0 /\\ ar_0 + ar_2 - 1 >= 0 /\\ ar_0 - 1 >= 0 /\\ 1 <= ar_0 /\\ 0 < ar_2 /\\ ar_1*ar_3 = i150' ]", 0-2) = 3*ar_0 + 2*ar_0^2
S("main_NULL_689(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(main_Load_653(ar_0, ar_1, ar_2, ar_1*ar_3, arityPad, arityPad)) [ ar_2 >= 0 /\\ ar_0 + ar_2 - 1 >= 0 /\\ ar_0 - 1 >= 0 /\\ 1 <= ar_0 /\\ 0 < ar_2 /\\ ar_1*ar_3 = i150' ]", 0-3) = ?
S("main_NULL_689(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(main_Load_653(ar_0, ar_1, ar_2, ar_1*ar_3, arityPad, arityPad)) [ ar_2 >= 0 /\\ ar_0 + ar_2 - 1 >= 0 /\\ ar_0 - 1 >= 0 /\\ 1 <= ar_0 /\\ 0 < ar_2 /\\ ar_1*ar_3 = i150' ]", 0-4) = ?
S("main_NULL_689(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(main_Load_653(ar_0, ar_1, ar_2, ar_1*ar_3, arityPad, arityPad)) [ ar_2 >= 0 /\\ ar_0 + ar_2 - 1 >= 0 /\\ ar_0 - 1 >= 0 /\\ 1 <= ar_0 /\\ 0 < ar_2 /\\ ar_1*ar_3 = i150' ]", 0-5) = ?
S("createIntList_LE_346(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(main_Load_653(ar_2, ar_3, ar_1, 0, arityPad, arityPad)) [ ar_2 - ar_5 >= 0 /\\ ar_0 - ar_5 + 1 >= 0 /\\ ar_5 - 1 >= 0 /\\ ar_4 + ar_5 - 1 >= 0 /\\ ar_2 + ar_5 - 2 >= 0 /\\ ar_1 + ar_5 - 3 >= 0 /\\ ar_0 + ar_5 - 1 >= 0 /\\ -ar_0 + ar_5 - 1 >= 0 /\\ ar_1 - ar_4 - 2 >= 0 /\\ ar_4 >= 0 /\\ ar_2 + ar_4 - 1 >= 0 /\\ ar_1 + ar_4 - 2 >= 0 /\\ ar_0 + ar_4 >= 0 /\\ ar_2 - 1 >= 0 /\\ ar_1 + ar_2 - 3 >= 0 /\\ ar_0 + ar_2 - 1 >= 0 /\\ -ar_0 + ar_2 - 1 >= 0 /\\ ar_1 - 2 >= 0 /\\ ar_0 + ar_1 - 2 >= 0 /\\ ar_0 >= 0 /\\ 0 < ar_1 /\\ 1 <= ar_2 /\\ 0 <= ar_4 /\\ 1 <= ar_5 /\\ 0 <= ar_5 /\\ ar_0 = 0 ]", 0-0) = ar_0
S("createIntList_LE_346(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(main_Load_653(ar_2, ar_3, ar_1, 0, arityPad, arityPad)) [ ar_2 - ar_5 >= 0 /\\ ar_0 - ar_5 + 1 >= 0 /\\ ar_5 - 1 >= 0 /\\ ar_4 + ar_5 - 1 >= 0 /\\ ar_2 + ar_5 - 2 >= 0 /\\ ar_1 + ar_5 - 3 >= 0 /\\ ar_0 + ar_5 - 1 >= 0 /\\ -ar_0 + ar_5 - 1 >= 0 /\\ ar_1 - ar_4 - 2 >= 0 /\\ ar_4 >= 0 /\\ ar_2 + ar_4 - 1 >= 0 /\\ ar_1 + ar_4 - 2 >= 0 /\\ ar_0 + ar_4 >= 0 /\\ ar_2 - 1 >= 0 /\\ ar_1 + ar_2 - 3 >= 0 /\\ ar_0 + ar_2 - 1 >= 0 /\\ -ar_0 + ar_2 - 1 >= 0 /\\ ar_1 - 2 >= 0 /\\ ar_0 + ar_1 - 2 >= 0 /\\ ar_0 >= 0 /\\ 0 < ar_1 /\\ 1 <= ar_2 /\\ 0 <= ar_4 /\\ 1 <= ar_5 /\\ 0 <= ar_5 /\\ ar_0 = 0 ]", 0-1) = ar_1
S("createIntList_LE_346(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(main_Load_653(ar_2, ar_3, ar_1, 0, arityPad, arityPad)) [ ar_2 - ar_5 >= 0 /\\ ar_0 - ar_5 + 1 >= 0 /\\ ar_5 - 1 >= 0 /\\ ar_4 + ar_5 - 1 >= 0 /\\ ar_2 + ar_5 - 2 >= 0 /\\ ar_1 + ar_5 - 3 >= 0 /\\ ar_0 + ar_5 - 1 >= 0 /\\ -ar_0 + ar_5 - 1 >= 0 /\\ ar_1 - ar_4 - 2 >= 0 /\\ ar_4 >= 0 /\\ ar_2 + ar_4 - 1 >= 0 /\\ ar_1 + ar_4 - 2 >= 0 /\\ ar_0 + ar_4 >= 0 /\\ ar_2 - 1 >= 0 /\\ ar_1 + ar_2 - 3 >= 0 /\\ ar_0 + ar_2 - 1 >= 0 /\\ -ar_0 + ar_2 - 1 >= 0 /\\ ar_1 - 2 >= 0 /\\ ar_0 + ar_1 - 2 >= 0 /\\ ar_0 >= 0 /\\ 0 < ar_1 /\\ 1 <= ar_2 /\\ 0 <= ar_4 /\\ 1 <= ar_5 /\\ 0 <= ar_5 /\\ ar_0 = 0 ]", 0-2) = 3*ar_0 + 2*ar_0^2
S("createIntList_LE_346(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(main_Load_653(ar_2, ar_3, ar_1, 0, arityPad, arityPad)) [ ar_2 - ar_5 >= 0 /\\ ar_0 - ar_5 + 1 >= 0 /\\ ar_5 - 1 >= 0 /\\ ar_4 + ar_5 - 1 >= 0 /\\ ar_2 + ar_5 - 2 >= 0 /\\ ar_1 + ar_5 - 3 >= 0 /\\ ar_0 + ar_5 - 1 >= 0 /\\ -ar_0 + ar_5 - 1 >= 0 /\\ ar_1 - ar_4 - 2 >= 0 /\\ ar_4 >= 0 /\\ ar_2 + ar_4 - 1 >= 0 /\\ ar_1 + ar_4 - 2 >= 0 /\\ ar_0 + ar_4 >= 0 /\\ ar_2 - 1 >= 0 /\\ ar_1 + ar_2 - 3 >= 0 /\\ ar_0 + ar_2 - 1 >= 0 /\\ -ar_0 + ar_2 - 1 >= 0 /\\ ar_1 - 2 >= 0 /\\ ar_0 + ar_1 - 2 >= 0 /\\ ar_0 >= 0 /\\ 0 < ar_1 /\\ 1 <= ar_2 /\\ 0 <= ar_4 /\\ 1 <= ar_5 /\\ 0 <= ar_5 /\\ ar_0 = 0 ]", 0-3) = 0
S("createIntList_LE_346(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(main_Load_653(ar_2, ar_3, ar_1, 0, arityPad, arityPad)) [ ar_2 - ar_5 >= 0 /\\ ar_0 - ar_5 + 1 >= 0 /\\ ar_5 - 1 >= 0 /\\ ar_4 + ar_5 - 1 >= 0 /\\ ar_2 + ar_5 - 2 >= 0 /\\ ar_1 + ar_5 - 3 >= 0 /\\ ar_0 + ar_5 - 1 >= 0 /\\ -ar_0 + ar_5 - 1 >= 0 /\\ ar_1 - ar_4 - 2 >= 0 /\\ ar_4 >= 0 /\\ ar_2 + ar_4 - 1 >= 0 /\\ ar_1 + ar_4 - 2 >= 0 /\\ ar_0 + ar_4 >= 0 /\\ ar_2 - 1 >= 0 /\\ ar_1 + ar_2 - 3 >= 0 /\\ ar_0 + ar_2 - 1 >= 0 /\\ -ar_0 + ar_2 - 1 >= 0 /\\ ar_1 - 2 >= 0 /\\ ar_0 + ar_1 - 2 >= 0 /\\ ar_0 >= 0 /\\ 0 < ar_1 /\\ 1 <= ar_2 /\\ 0 <= ar_4 /\\ 1 <= ar_5 /\\ 0 <= ar_5 /\\ ar_0 = 0 ]", 0-4) = ?
S("createIntList_LE_346(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(main_Load_653(ar_2, ar_3, ar_1, 0, arityPad, arityPad)) [ ar_2 - ar_5 >= 0 /\\ ar_0 - ar_5 + 1 >= 0 /\\ ar_5 - 1 >= 0 /\\ ar_4 + ar_5 - 1 >= 0 /\\ ar_2 + ar_5 - 2 >= 0 /\\ ar_1 + ar_5 - 3 >= 0 /\\ ar_0 + ar_5 - 1 >= 0 /\\ -ar_0 + ar_5 - 1 >= 0 /\\ ar_1 - ar_4 - 2 >= 0 /\\ ar_4 >= 0 /\\ ar_2 + ar_4 - 1 >= 0 /\\ ar_1 + ar_4 - 2 >= 0 /\\ ar_0 + ar_4 >= 0 /\\ ar_2 - 1 >= 0 /\\ ar_1 + ar_2 - 3 >= 0 /\\ ar_0 + ar_2 - 1 >= 0 /\\ -ar_0 + ar_2 - 1 >= 0 /\\ ar_1 - 2 >= 0 /\\ ar_0 + ar_1 - 2 >= 0 /\\ ar_0 >= 0 /\\ 0 < ar_1 /\\ 1 <= ar_2 /\\ 0 <= ar_4 /\\ 1 <= ar_5 /\\ 0 <= ar_5 /\\ ar_0 = 0 ]", 0-5) = ?
S("main_GT_671(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(main_NULL_689(ar_0, ar_1, ar_5, ar_4, arityPad, arityPad)) [ ar_3 - ar_5 - 1 >= 0 /\\ ar_5 >= 0 /\\ ar_3 + ar_5 - 1 >= 0 /\\ ar_0 + ar_5 - 1 >= 0 /\\ ar_3 - 1 >= 0 /\\ ar_2 + ar_3 - 1 >= 0 /\\ -ar_2 + ar_3 - 1 >= 0 /\\ ar_0 + ar_3 - 2 >= 0 /\\ ar_0 - 1 >= 0 /\\ 0 < ar_3 /\\ 0 <= ar_5 /\\ 1 <= ar_0 /\\ ar_2 <= 0 ]", 0-0) = ar_0
S("main_GT_671(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(main_NULL_689(ar_0, ar_1, ar_5, ar_4, arityPad, arityPad)) [ ar_3 - ar_5 - 1 >= 0 /\\ ar_5 >= 0 /\\ ar_3 + ar_5 - 1 >= 0 /\\ ar_0 + ar_5 - 1 >= 0 /\\ ar_3 - 1 >= 0 /\\ ar_2 + ar_3 - 1 >= 0 /\\ -ar_2 + ar_3 - 1 >= 0 /\\ ar_0 + ar_3 - 2 >= 0 /\\ ar_0 - 1 >= 0 /\\ 0 < ar_3 /\\ 0 <= ar_5 /\\ 1 <= ar_0 /\\ ar_2 <= 0 ]", 0-1) = ar_1
S("main_GT_671(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(main_NULL_689(ar_0, ar_1, ar_5, ar_4, arityPad, arityPad)) [ ar_3 - ar_5 - 1 >= 0 /\\ ar_5 >= 0 /\\ ar_3 + ar_5 - 1 >= 0 /\\ ar_0 + ar_5 - 1 >= 0 /\\ ar_3 - 1 >= 0 /\\ ar_2 + ar_3 - 1 >= 0 /\\ -ar_2 + ar_3 - 1 >= 0 /\\ ar_0 + ar_3 - 2 >= 0 /\\ ar_0 - 1 >= 0 /\\ 0 < ar_3 /\\ 0 <= ar_5 /\\ 1 <= ar_0 /\\ ar_2 <= 0 ]", 0-2) = 3*ar_0 + 2*ar_0^2
S("main_GT_671(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(main_NULL_689(ar_0, ar_1, ar_5, ar_4, arityPad, arityPad)) [ ar_3 - ar_5 - 1 >= 0 /\\ ar_5 >= 0 /\\ ar_3 + ar_5 - 1 >= 0 /\\ ar_0 + ar_5 - 1 >= 0 /\\ ar_3 - 1 >= 0 /\\ ar_2 + ar_3 - 1 >= 0 /\\ -ar_2 + ar_3 - 1 >= 0 /\\ ar_0 + ar_3 - 2 >= 0 /\\ ar_0 - 1 >= 0 /\\ 0 < ar_3 /\\ 0 <= ar_5 /\\ 1 <= ar_0 /\\ ar_2 <= 0 ]", 0-3) = ?
S("main_GT_671(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(main_NULL_689(ar_0, ar_1, ar_5, ar_4, arityPad, arityPad)) [ ar_3 - ar_5 - 1 >= 0 /\\ ar_5 >= 0 /\\ ar_3 + ar_5 - 1 >= 0 /\\ ar_0 + ar_5 - 1 >= 0 /\\ ar_3 - 1 >= 0 /\\ ar_2 + ar_3 - 1 >= 0 /\\ -ar_2 + ar_3 - 1 >= 0 /\\ ar_0 + ar_3 - 2 >= 0 /\\ ar_0 - 1 >= 0 /\\ 0 < ar_3 /\\ 0 <= ar_5 /\\ 1 <= ar_0 /\\ ar_2 <= 0 ]", 0-4) = ?
S("main_GT_671(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(main_NULL_689(ar_0, ar_1, ar_5, ar_4, arityPad, arityPad)) [ ar_3 - ar_5 - 1 >= 0 /\\ ar_5 >= 0 /\\ ar_3 + ar_5 - 1 >= 0 /\\ ar_0 + ar_5 - 1 >= 0 /\\ ar_3 - 1 >= 0 /\\ ar_2 + ar_3 - 1 >= 0 /\\ -ar_2 + ar_3 - 1 >= 0 /\\ ar_0 + ar_3 - 2 >= 0 /\\ ar_0 - 1 >= 0 /\\ 0 < ar_3 /\\ 0 <= ar_5 /\\ 1 <= ar_0 /\\ ar_2 <= 0 ]", 0-5) = ?
S("main_Load_653(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(main_GT_671(ar_0, ar_1, i142', ar_2, ar_3, o229')) [ ar_0 - 1 >= 0 /\\ 0 <= o229' /\\ 0 < ar_2 /\\ o229' < ar_2 /\\ 1 <= ar_0 /\\ -ar_2 < i142' /\\ i142' < ar_2 ]", 0-0) = ar_0
S("main_Load_653(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(main_GT_671(ar_0, ar_1, i142', ar_2, ar_3, o229')) [ ar_0 - 1 >= 0 /\\ 0 <= o229' /\\ 0 < ar_2 /\\ o229' < ar_2 /\\ 1 <= ar_0 /\\ -ar_2 < i142' /\\ i142' < ar_2 ]", 0-1) = ar_1
S("main_Load_653(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(main_GT_671(ar_0, ar_1, i142', ar_2, ar_3, o229')) [ ar_0 - 1 >= 0 /\\ 0 <= o229' /\\ 0 < ar_2 /\\ o229' < ar_2 /\\ 1 <= ar_0 /\\ -ar_2 < i142' /\\ i142' < ar_2 ]", 0-2) = 3*ar_0 + 2*ar_0^2
S("main_Load_653(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(main_GT_671(ar_0, ar_1, i142', ar_2, ar_3, o229')) [ ar_0 - 1 >= 0 /\\ 0 <= o229' /\\ 0 < ar_2 /\\ o229' < ar_2 /\\ 1 <= ar_0 /\\ -ar_2 < i142' /\\ i142' < ar_2 ]", 0-3) = 3*ar_0 + 2*ar_0^2
S("main_Load_653(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(main_GT_671(ar_0, ar_1, i142', ar_2, ar_3, o229')) [ ar_0 - 1 >= 0 /\\ 0 <= o229' /\\ 0 < ar_2 /\\ o229' < ar_2 /\\ 1 <= ar_0 /\\ -ar_2 < i142' /\\ i142' < ar_2 ]", 0-4) = ?
S("main_Load_653(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(main_GT_671(ar_0, ar_1, i142', ar_2, ar_3, o229')) [ ar_0 - 1 >= 0 /\\ 0 <= o229' /\\ 0 < ar_2 /\\ o229' < ar_2 /\\ 1 <= ar_0 /\\ -ar_2 < i142' /\\ i142' < ar_2 ]", 0-5) = 3*ar_0 + 2*ar_0^2
S("main_NULL_689(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(main_Load_653(ar_0, ar_1, 0, ar_3, arityPad, arityPad)) [ ar_2 >= 0 /\\ ar_0 + ar_2 - 1 >= 0 /\\ ar_0 - 1 >= 0 /\\ 1 <= ar_0 /\\ ar_2 = 0 ]", 0-0) = ar_0
S("main_NULL_689(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(main_Load_653(ar_0, ar_1, 0, ar_3, arityPad, arityPad)) [ ar_2 >= 0 /\\ ar_0 + ar_2 - 1 >= 0 /\\ ar_0 - 1 >= 0 /\\ 1 <= ar_0 /\\ ar_2 = 0 ]", 0-1) = ar_1
S("main_NULL_689(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(main_Load_653(ar_0, ar_1, 0, ar_3, arityPad, arityPad)) [ ar_2 >= 0 /\\ ar_0 + ar_2 - 1 >= 0 /\\ ar_0 - 1 >= 0 /\\ 1 <= ar_0 /\\ ar_2 = 0 ]", 0-2) = 0
S("main_NULL_689(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(main_Load_653(ar_0, ar_1, 0, ar_3, arityPad, arityPad)) [ ar_2 >= 0 /\\ ar_0 + ar_2 - 1 >= 0 /\\ ar_0 - 1 >= 0 /\\ 1 <= ar_0 /\\ ar_2 = 0 ]", 0-3) = ?
S("main_NULL_689(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(main_Load_653(ar_0, ar_1, 0, ar_3, arityPad, arityPad)) [ ar_2 >= 0 /\\ ar_0 + ar_2 - 1 >= 0 /\\ ar_0 - 1 >= 0 /\\ 1 <= ar_0 /\\ ar_2 = 0 ]", 0-4) = ?
S("main_NULL_689(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(main_Load_653(ar_0, ar_1, 0, ar_3, arityPad, arityPad)) [ ar_2 >= 0 /\\ ar_0 + ar_2 - 1 >= 0 /\\ ar_0 - 1 >= 0 /\\ 1 <= ar_0 /\\ ar_2 = 0 ]", 0-5) = ?
S("langle_init_rangle_Load_313(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(createIntList_LE_346(ar_1 - 1, o90''' + ar_2, ar_3, ar_4, ar_2, ar_1)) [ ar_3 - 1 >= 0 /\\ ar_2 + ar_3 - 1 >= 0 /\\ ar_1 + ar_3 - 2 >= 0 /\\ -ar_1 + ar_3 >= 0 /\\ ar_0 + ar_3 - 2 >= 0 /\\ -ar_0 + ar_3 >= 0 /\\ ar_2 >= 0 /\\ ar_1 + ar_2 - 1 >= 0 /\\ ar_0 + ar_2 - 1 >= 0 /\\ -ar_0 + ar_2 + 1 >= 0 /\\ ar_1 - 1 >= 0 /\\ ar_0 + ar_1 - 2 >= 0 /\\ -ar_0 + ar_1 >= 0 /\\ -ar_0 + 1 >= 0 /\\ ar_0 - 1 >= 0 /\\ ar_0 < o90''' /\\ 0 <= i73' /\\ 0 < ar_0 /\\ 0 < o90'1 /\\ 1 <= ar_1 /\\ 1 <= ar_3 /\\ 0 <= ar_2 /\\ ar_1 - 1 = i73' /\\ o90''' <= ar_0 + ar_1 /\\ o90'1 = o90''' + ar_2 /\\ 0 < o90''' ]", 0-0) = ar_0
S("langle_init_rangle_Load_313(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(createIntList_LE_346(ar_1 - 1, o90''' + ar_2, ar_3, ar_4, ar_2, ar_1)) [ ar_3 - 1 >= 0 /\\ ar_2 + ar_3 - 1 >= 0 /\\ ar_1 + ar_3 - 2 >= 0 /\\ -ar_1 + ar_3 >= 0 /\\ ar_0 + ar_3 - 2 >= 0 /\\ -ar_0 + ar_3 >= 0 /\\ ar_2 >= 0 /\\ ar_1 + ar_2 - 1 >= 0 /\\ ar_0 + ar_2 - 1 >= 0 /\\ -ar_0 + ar_2 + 1 >= 0 /\\ ar_1 - 1 >= 0 /\\ ar_0 + ar_1 - 2 >= 0 /\\ -ar_0 + ar_1 >= 0 /\\ -ar_0 + 1 >= 0 /\\ ar_0 - 1 >= 0 /\\ ar_0 < o90''' /\\ 0 <= i73' /\\ 0 < ar_0 /\\ 0 < o90'1 /\\ 1 <= ar_1 /\\ 1 <= ar_3 /\\ 0 <= ar_2 /\\ ar_1 - 1 = i73' /\\ o90''' <= ar_0 + ar_1 /\\ o90'1 = o90''' + ar_2 /\\ 0 < o90''' ]", 0-1) = 3*ar_0 + 2*ar_0^2
S("langle_init_rangle_Load_313(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(createIntList_LE_346(ar_1 - 1, o90''' + ar_2, ar_3, ar_4, ar_2, ar_1)) [ ar_3 - 1 >= 0 /\\ ar_2 + ar_3 - 1 >= 0 /\\ ar_1 + ar_3 - 2 >= 0 /\\ -ar_1 + ar_3 >= 0 /\\ ar_0 + ar_3 - 2 >= 0 /\\ -ar_0 + ar_3 >= 0 /\\ ar_2 >= 0 /\\ ar_1 + ar_2 - 1 >= 0 /\\ ar_0 + ar_2 - 1 >= 0 /\\ -ar_0 + ar_2 + 1 >= 0 /\\ ar_1 - 1 >= 0 /\\ ar_0 + ar_1 - 2 >= 0 /\\ -ar_0 + ar_1 >= 0 /\\ -ar_0 + 1 >= 0 /\\ ar_0 - 1 >= 0 /\\ ar_0 < o90''' /\\ 0 <= i73' /\\ 0 < ar_0 /\\ 0 < o90'1 /\\ 1 <= ar_1 /\\ 1 <= ar_3 /\\ 0 <= ar_2 /\\ ar_1 - 1 = i73' /\\ o90''' <= ar_0 + ar_1 /\\ o90'1 = o90''' + ar_2 /\\ 0 < o90''' ]", 0-2) = ar_0
S("langle_init_rangle_Load_313(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(createIntList_LE_346(ar_1 - 1, o90''' + ar_2, ar_3, ar_4, ar_2, ar_1)) [ ar_3 - 1 >= 0 /\\ ar_2 + ar_3 - 1 >= 0 /\\ ar_1 + ar_3 - 2 >= 0 /\\ -ar_1 + ar_3 >= 0 /\\ ar_0 + ar_3 - 2 >= 0 /\\ -ar_0 + ar_3 >= 0 /\\ ar_2 >= 0 /\\ ar_1 + ar_2 - 1 >= 0 /\\ ar_0 + ar_2 - 1 >= 0 /\\ -ar_0 + ar_2 + 1 >= 0 /\\ ar_1 - 1 >= 0 /\\ ar_0 + ar_1 - 2 >= 0 /\\ -ar_0 + ar_1 >= 0 /\\ -ar_0 + 1 >= 0 /\\ ar_0 - 1 >= 0 /\\ ar_0 < o90''' /\\ 0 <= i73' /\\ 0 < ar_0 /\\ 0 < o90'1 /\\ 1 <= ar_1 /\\ 1 <= ar_3 /\\ 0 <= ar_2 /\\ ar_1 - 1 = i73' /\\ o90''' <= ar_0 + ar_1 /\\ o90'1 = o90''' + ar_2 /\\ 0 < o90''' ]", 0-3) = ar_1
S("langle_init_rangle_Load_313(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(createIntList_LE_346(ar_1 - 1, o90''' + ar_2, ar_3, ar_4, ar_2, ar_1)) [ ar_3 - 1 >= 0 /\\ ar_2 + ar_3 - 1 >= 0 /\\ ar_1 + ar_3 - 2 >= 0 /\\ -ar_1 + ar_3 >= 0 /\\ ar_0 + ar_3 - 2 >= 0 /\\ -ar_0 + ar_3 >= 0 /\\ ar_2 >= 0 /\\ ar_1 + ar_2 - 1 >= 0 /\\ ar_0 + ar_2 - 1 >= 0 /\\ -ar_0 + ar_2 + 1 >= 0 /\\ ar_1 - 1 >= 0 /\\ ar_0 + ar_1 - 2 >= 0 /\\ -ar_0 + ar_1 >= 0 /\\ -ar_0 + 1 >= 0 /\\ ar_0 - 1 >= 0 /\\ ar_0 < o90''' /\\ 0 <= i73' /\\ 0 < ar_0 /\\ 0 < o90'1 /\\ 1 <= ar_1 /\\ 1 <= ar_3 /\\ 0 <= ar_2 /\\ ar_1 - 1 = i73' /\\ o90''' <= ar_0 + ar_1 /\\ o90'1 = o90''' + ar_2 /\\ 0 < o90''' ]", 0-4) = 3*ar_0 + 2*ar_0^2
S("langle_init_rangle_Load_313(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(createIntList_LE_346(ar_1 - 1, o90''' + ar_2, ar_3, ar_4, ar_2, ar_1)) [ ar_3 - 1 >= 0 /\\ ar_2 + ar_3 - 1 >= 0 /\\ ar_1 + ar_3 - 2 >= 0 /\\ -ar_1 + ar_3 >= 0 /\\ ar_0 + ar_3 - 2 >= 0 /\\ -ar_0 + ar_3 >= 0 /\\ ar_2 >= 0 /\\ ar_1 + ar_2 - 1 >= 0 /\\ ar_0 + ar_2 - 1 >= 0 /\\ -ar_0 + ar_2 + 1 >= 0 /\\ ar_1 - 1 >= 0 /\\ ar_0 + ar_1 - 2 >= 0 /\\ -ar_0 + ar_1 >= 0 /\\ -ar_0 + 1 >= 0 /\\ ar_0 - 1 >= 0 /\\ ar_0 < o90''' /\\ 0 <= i73' /\\ 0 < ar_0 /\\ 0 < o90'1 /\\ 1 <= ar_1 /\\ 1 <= ar_3 /\\ 0 <= ar_2 /\\ ar_1 - 1 = i73' /\\ o90''' <= ar_0 + ar_1 /\\ o90'1 = o90''' + ar_2 /\\ 0 < o90''' ]", 0-5) = ar_0
S("main_GT_671(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(main_Load_653(ar_0, ar_1, o228''', ar_4 + 1, arityPad, arityPad)) [ ar_3 - ar_5 - 1 >= 0 /\\ ar_5 >= 0 /\\ ar_3 + ar_5 - 1 >= 0 /\\ ar_0 + ar_5 - 1 >= 0 /\\ ar_3 - 1 >= 0 /\\ ar_2 + ar_3 - 1 >= 0 /\\ -ar_2 + ar_3 - 1 >= 0 /\\ ar_0 + ar_3 - 2 >= 0 /\\ ar_0 - 1 >= 0 /\\ 1 <= ar_2 /\\ o228''' <= ar_3 + i146' /\\ 0 < o228''' /\\ ar_4 + 1 = i148' /\\ 0 <= i146' /\\ ar_2 - 1 = i146' /\\ 0 <= ar_5 /\\ 1 <= ar_0 /\\ o228''' < ar_3 /\\ 0 < ar_2 /\\ 0 < ar_3 ]", 0-0) = ar_0
S("main_GT_671(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(main_Load_653(ar_0, ar_1, o228''', ar_4 + 1, arityPad, arityPad)) [ ar_3 - ar_5 - 1 >= 0 /\\ ar_5 >= 0 /\\ ar_3 + ar_5 - 1 >= 0 /\\ ar_0 + ar_5 - 1 >= 0 /\\ ar_3 - 1 >= 0 /\\ ar_2 + ar_3 - 1 >= 0 /\\ -ar_2 + ar_3 - 1 >= 0 /\\ ar_0 + ar_3 - 2 >= 0 /\\ ar_0 - 1 >= 0 /\\ 1 <= ar_2 /\\ o228''' <= ar_3 + i146' /\\ 0 < o228''' /\\ ar_4 + 1 = i148' /\\ 0 <= i146' /\\ ar_2 - 1 = i146' /\\ 0 <= ar_5 /\\ 1 <= ar_0 /\\ o228''' < ar_3 /\\ 0 < ar_2 /\\ 0 < ar_3 ]", 0-1) = ar_1
S("main_GT_671(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(main_Load_653(ar_0, ar_1, o228''', ar_4 + 1, arityPad, arityPad)) [ ar_3 - ar_5 - 1 >= 0 /\\ ar_5 >= 0 /\\ ar_3 + ar_5 - 1 >= 0 /\\ ar_0 + ar_5 - 1 >= 0 /\\ ar_3 - 1 >= 0 /\\ ar_2 + ar_3 - 1 >= 0 /\\ -ar_2 + ar_3 - 1 >= 0 /\\ ar_0 + ar_3 - 2 >= 0 /\\ ar_0 - 1 >= 0 /\\ 1 <= ar_2 /\\ o228''' <= ar_3 + i146' /\\ 0 < o228''' /\\ ar_4 + 1 = i148' /\\ 0 <= i146' /\\ ar_2 - 1 = i146' /\\ 0 <= ar_5 /\\ 1 <= ar_0 /\\ o228''' < ar_3 /\\ 0 < ar_2 /\\ 0 < ar_3 ]", 0-2) = 3*ar_0 + 2*ar_0^2
S("main_GT_671(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(main_Load_653(ar_0, ar_1, o228''', ar_4 + 1, arityPad, arityPad)) [ ar_3 - ar_5 - 1 >= 0 /\\ ar_5 >= 0 /\\ ar_3 + ar_5 - 1 >= 0 /\\ ar_0 + ar_5 - 1 >= 0 /\\ ar_3 - 1 >= 0 /\\ ar_2 + ar_3 - 1 >= 0 /\\ -ar_2 + ar_3 - 1 >= 0 /\\ ar_0 + ar_3 - 2 >= 0 /\\ ar_0 - 1 >= 0 /\\ 1 <= ar_2 /\\ o228''' <= ar_3 + i146' /\\ 0 < o228''' /\\ ar_4 + 1 = i148' /\\ 0 <= i146' /\\ ar_2 - 1 = i146' /\\ 0 <= ar_5 /\\ 1 <= ar_0 /\\ o228''' < ar_3 /\\ 0 < ar_2 /\\ 0 < ar_3 ]", 0-3) = ?
S("main_GT_671(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(main_Load_653(ar_0, ar_1, o228''', ar_4 + 1, arityPad, arityPad)) [ ar_3 - ar_5 - 1 >= 0 /\\ ar_5 >= 0 /\\ ar_3 + ar_5 - 1 >= 0 /\\ ar_0 + ar_5 - 1 >= 0 /\\ ar_3 - 1 >= 0 /\\ ar_2 + ar_3 - 1 >= 0 /\\ -ar_2 + ar_3 - 1 >= 0 /\\ ar_0 + ar_3 - 2 >= 0 /\\ ar_0 - 1 >= 0 /\\ 1 <= ar_2 /\\ o228''' <= ar_3 + i146' /\\ 0 < o228''' /\\ ar_4 + 1 = i148' /\\ 0 <= i146' /\\ ar_2 - 1 = i146' /\\ 0 <= ar_5 /\\ 1 <= ar_0 /\\ o228''' < ar_3 /\\ 0 < ar_2 /\\ 0 < ar_3 ]", 0-4) = ?
S("main_GT_671(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(main_Load_653(ar_0, ar_1, o228''', ar_4 + 1, arityPad, arityPad)) [ ar_3 - ar_5 - 1 >= 0 /\\ ar_5 >= 0 /\\ ar_3 + ar_5 - 1 >= 0 /\\ ar_0 + ar_5 - 1 >= 0 /\\ ar_3 - 1 >= 0 /\\ ar_2 + ar_3 - 1 >= 0 /\\ -ar_2 + ar_3 - 1 >= 0 /\\ ar_0 + ar_3 - 2 >= 0 /\\ ar_0 - 1 >= 0 /\\ 1 <= ar_2 /\\ o228''' <= ar_3 + i146' /\\ 0 < o228''' /\\ ar_4 + 1 = i148' /\\ 0 <= i146' /\\ ar_2 - 1 = i146' /\\ 0 <= ar_5 /\\ 1 <= ar_0 /\\ o228''' < ar_3 /\\ 0 < ar_2 /\\ 0 < ar_3 ]", 0-5) = ?
S("koat_start(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(main_Load_1(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5)) [ 0 <= 0 ]", 0-0) = ar_0
S("koat_start(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(main_Load_1(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5)) [ 0 <= 0 ]", 0-1) = ar_1
S("koat_start(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(main_Load_1(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5)) [ 0 <= 0 ]", 0-2) = ar_2
S("koat_start(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(main_Load_1(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5)) [ 0 <= 0 ]", 0-3) = ar_3
S("koat_start(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(main_Load_1(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5)) [ 0 <= 0 ]", 0-4) = ar_4
S("koat_start(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(main_Load_1(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5)) [ 0 <= 0 ]", 0-5) = ar_5
orients the transitions
main_NULL_689(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(main_Load_653(ar_0, ar_1, ar_2, ar_1*ar_3, arityPad, arityPad)) [ ar_2 >= 0 /\ ar_0 + ar_2 - 1 >= 0 /\ ar_0 - 1 >= 0 /\ 1 <= ar_0 /\ 0 < ar_2 /\ ar_1*ar_3 = i150' ]
main_NULL_689(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(main_Load_653(ar_0, ar_1, 0, ar_3, arityPad, arityPad)) [ ar_2 >= 0 /\ ar_0 + ar_2 - 1 >= 0 /\ ar_0 - 1 >= 0 /\ 1 <= ar_0 /\ ar_2 = 0 ]
main_Load_653(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(main_GT_671(ar_0, ar_1, i142', ar_2, ar_3, o229')) [ ar_0 - 1 >= 0 /\ 0 <= o229' /\ 0 < ar_2 /\ o229' < ar_2 /\ 1 <= ar_0 /\ -ar_2 < i142' /\ i142' < ar_2 ]
main_GT_671(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(main_NULL_689(ar_0, ar_1, ar_5, ar_4, arityPad, arityPad)) [ ar_3 - ar_5 - 1 >= 0 /\ ar_5 >= 0 /\ ar_3 + ar_5 - 1 >= 0 /\ ar_0 + ar_5 - 1 >= 0 /\ ar_3 - 1 >= 0 /\ ar_2 + ar_3 - 1 >= 0 /\ -ar_2 + ar_3 - 1 >= 0 /\ ar_0 + ar_3 - 2 >= 0 /\ ar_0 - 1 >= 0 /\ 0 < ar_3 /\ 0 <= ar_5 /\ 1 <= ar_0 /\ ar_2 <= 0 ]
main_GT_671(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(main_Load_653(ar_0, ar_1, o228''', ar_4 + 1, arityPad, arityPad)) [ ar_3 - ar_5 - 1 >= 0 /\ ar_5 >= 0 /\ ar_3 + ar_5 - 1 >= 0 /\ ar_0 + ar_5 - 1 >= 0 /\ ar_3 - 1 >= 0 /\ ar_2 + ar_3 - 1 >= 0 /\ -ar_2 + ar_3 - 1 >= 0 /\ ar_0 + ar_3 - 2 >= 0 /\ ar_0 - 1 >= 0 /\ 1 <= ar_2 /\ o228''' <= ar_3 + i146' /\ 0 < o228''' /\ ar_4 + 1 = i148' /\ 0 <= i146' /\ ar_2 - 1 = i146' /\ 0 <= ar_5 /\ 1 <= ar_0 /\ o228''' < ar_3 /\ 0 < ar_2 /\ 0 < ar_3 ]
weakly and the transitions
main_NULL_689(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(main_Load_653(ar_0, ar_1, ar_2, ar_1*ar_3, arityPad, arityPad)) [ ar_2 >= 0 /\ ar_0 + ar_2 - 1 >= 0 /\ ar_0 - 1 >= 0 /\ 1 <= ar_0 /\ 0 < ar_2 /\ ar_1*ar_3 = i150' ]
main_NULL_689(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(main_Load_653(ar_0, ar_1, 0, ar_3, arityPad, arityPad)) [ ar_2 >= 0 /\ ar_0 + ar_2 - 1 >= 0 /\ ar_0 - 1 >= 0 /\ 1 <= ar_0 /\ ar_2 = 0 ]
main_Load_653(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(main_GT_671(ar_0, ar_1, i142', ar_2, ar_3, o229')) [ ar_0 - 1 >= 0 /\ 0 <= o229' /\ 0 < ar_2 /\ o229' < ar_2 /\ 1 <= ar_0 /\ -ar_2 < i142' /\ i142' < ar_2 ]
main_GT_671(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(main_NULL_689(ar_0, ar_1, ar_5, ar_4, arityPad, arityPad)) [ ar_3 - ar_5 - 1 >= 0 /\ ar_5 >= 0 /\ ar_3 + ar_5 - 1 >= 0 /\ ar_0 + ar_5 - 1 >= 0 /\ ar_3 - 1 >= 0 /\ ar_2 + ar_3 - 1 >= 0 /\ -ar_2 + ar_3 - 1 >= 0 /\ ar_0 + ar_3 - 2 >= 0 /\ ar_0 - 1 >= 0 /\ 0 < ar_3 /\ 0 <= ar_5 /\ 1 <= ar_0 /\ ar_2 <= 0 ]
main_GT_671(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(main_Load_653(ar_0, ar_1, o228''', ar_4 + 1, arityPad, arityPad)) [ ar_3 - ar_5 - 1 >= 0 /\ ar_5 >= 0 /\ ar_3 + ar_5 - 1 >= 0 /\ ar_0 + ar_5 - 1 >= 0 /\ ar_3 - 1 >= 0 /\ ar_2 + ar_3 - 1 >= 0 /\ -ar_2 + ar_3 - 1 >= 0 /\ ar_0 + ar_3 - 2 >= 0 /\ ar_0 - 1 >= 0 /\ 1 <= ar_2 /\ o228''' <= ar_3 + i146' /\ 0 < o228''' /\ ar_4 + 1 = i148' /\ 0 <= i146' /\ ar_2 - 1 = i146' /\ 0 <= ar_5 /\ 1 <= ar_0 /\ o228''' < ar_3 /\ 0 < ar_2 /\ 0 < ar_3 ]
strictly and produces the following problem:
6: T:
(Comp: 1, Cost: 0) koat_start(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(main_Load_1(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5)) [ 0 <= 0 ]
(Comp: 9*ar_0 + 6*ar_0^2, Cost: 9) main_GT_671(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(main_Load_653(ar_0, ar_1, o228''', ar_4 + 1, arityPad, arityPad)) [ ar_3 - ar_5 - 1 >= 0 /\ ar_5 >= 0 /\ ar_3 + ar_5 - 1 >= 0 /\ ar_0 + ar_5 - 1 >= 0 /\ ar_3 - 1 >= 0 /\ ar_2 + ar_3 - 1 >= 0 /\ -ar_2 + ar_3 - 1 >= 0 /\ ar_0 + ar_3 - 2 >= 0 /\ ar_0 - 1 >= 0 /\ 1 <= ar_2 /\ o228''' <= ar_3 + i146' /\ 0 < o228''' /\ ar_4 + 1 = i148' /\ 0 <= i146' /\ ar_2 - 1 = i146' /\ 0 <= ar_5 /\ 1 <= ar_0 /\ o228''' < ar_3 /\ 0 < ar_2 /\ 0 < ar_3 ]
(Comp: 2*ar_0, Cost: 10) langle_init_rangle_Load_313(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(createIntList_LE_346(ar_1 - 1, o90''' + ar_2, ar_3, ar_4, ar_2, ar_1)) [ ar_3 - 1 >= 0 /\ ar_2 + ar_3 - 1 >= 0 /\ ar_1 + ar_3 - 2 >= 0 /\ -ar_1 + ar_3 >= 0 /\ ar_0 + ar_3 - 2 >= 0 /\ -ar_0 + ar_3 >= 0 /\ ar_2 >= 0 /\ ar_1 + ar_2 - 1 >= 0 /\ ar_0 + ar_2 - 1 >= 0 /\ -ar_0 + ar_2 + 1 >= 0 /\ ar_1 - 1 >= 0 /\ ar_0 + ar_1 - 2 >= 0 /\ -ar_0 + ar_1 >= 0 /\ -ar_0 + 1 >= 0 /\ ar_0 - 1 >= 0 /\ ar_0 < o90''' /\ 0 <= i73' /\ 0 < ar_0 /\ 0 < o90'1 /\ 1 <= ar_1 /\ 1 <= ar_3 /\ 0 <= ar_2 /\ ar_1 - 1 = i73' /\ o90''' <= ar_0 + ar_1 /\ o90'1 = o90''' + ar_2 /\ 0 < o90''' ]
(Comp: 9*ar_0 + 6*ar_0^2, Cost: 1) main_NULL_689(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(main_Load_653(ar_0, ar_1, 0, ar_3, arityPad, arityPad)) [ ar_2 >= 0 /\ ar_0 + ar_2 - 1 >= 0 /\ ar_0 - 1 >= 0 /\ 1 <= ar_0 /\ ar_2 = 0 ]
(Comp: 9*ar_0 + 6*ar_0^2, Cost: 4) main_Load_653(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(main_GT_671(ar_0, ar_1, i142', ar_2, ar_3, o229')) [ ar_0 - 1 >= 0 /\ 0 <= o229' /\ 0 < ar_2 /\ o229' < ar_2 /\ 1 <= ar_0 /\ -ar_2 < i142' /\ i142' < ar_2 ]
(Comp: 9*ar_0 + 6*ar_0^2, Cost: 5) main_GT_671(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(main_NULL_689(ar_0, ar_1, ar_5, ar_4, arityPad, arityPad)) [ ar_3 - ar_5 - 1 >= 0 /\ ar_5 >= 0 /\ ar_3 + ar_5 - 1 >= 0 /\ ar_0 + ar_5 - 1 >= 0 /\ ar_3 - 1 >= 0 /\ ar_2 + ar_3 - 1 >= 0 /\ -ar_2 + ar_3 - 1 >= 0 /\ ar_0 + ar_3 - 2 >= 0 /\ ar_0 - 1 >= 0 /\ 0 < ar_3 /\ 0 <= ar_5 /\ 1 <= ar_0 /\ ar_2 <= 0 ]
(Comp: 1, Cost: 6) createIntList_LE_346(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(main_Load_653(ar_2, ar_3, ar_1, 0, arityPad, arityPad)) [ ar_2 - ar_5 >= 0 /\ ar_0 - ar_5 + 1 >= 0 /\ ar_5 - 1 >= 0 /\ ar_4 + ar_5 - 1 >= 0 /\ ar_2 + ar_5 - 2 >= 0 /\ ar_1 + ar_5 - 3 >= 0 /\ ar_0 + ar_5 - 1 >= 0 /\ -ar_0 + ar_5 - 1 >= 0 /\ ar_1 - ar_4 - 2 >= 0 /\ ar_4 >= 0 /\ ar_2 + ar_4 - 1 >= 0 /\ ar_1 + ar_4 - 2 >= 0 /\ ar_0 + ar_4 >= 0 /\ ar_2 - 1 >= 0 /\ ar_1 + ar_2 - 3 >= 0 /\ ar_0 + ar_2 - 1 >= 0 /\ -ar_0 + ar_2 - 1 >= 0 /\ ar_1 - 2 >= 0 /\ ar_0 + ar_1 - 2 >= 0 /\ ar_0 >= 0 /\ 0 < ar_1 /\ 1 <= ar_2 /\ 0 <= ar_4 /\ 1 <= ar_5 /\ 0 <= ar_5 /\ ar_0 = 0 ]
(Comp: 9*ar_0 + 6*ar_0^2, Cost: 6) main_NULL_689(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(main_Load_653(ar_0, ar_1, ar_2, ar_1*ar_3, arityPad, arityPad)) [ ar_2 >= 0 /\ ar_0 + ar_2 - 1 >= 0 /\ ar_0 - 1 >= 0 /\ 1 <= ar_0 /\ 0 < ar_2 /\ ar_1*ar_3 = i150' ]
(Comp: 2*ar_0, Cost: 9) createIntList_LE_346(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(langle_init_rangle_Load_313(1, ar_0, ar_1, ar_2, ar_3, arityPad)) [ ar_2 - ar_5 >= 0 /\ ar_0 - ar_5 + 1 >= 0 /\ ar_5 - 1 >= 0 /\ ar_4 + ar_5 - 1 >= 0 /\ ar_2 + ar_5 - 2 >= 0 /\ ar_1 + ar_5 - 3 >= 0 /\ ar_0 + ar_5 - 1 >= 0 /\ -ar_0 + ar_5 - 1 >= 0 /\ ar_1 - ar_4 - 2 >= 0 /\ ar_4 >= 0 /\ ar_2 + ar_4 - 1 >= 0 /\ ar_1 + ar_4 - 2 >= 0 /\ ar_0 + ar_4 >= 0 /\ ar_2 - 1 >= 0 /\ ar_1 + ar_2 - 3 >= 0 /\ ar_0 + ar_2 - 1 >= 0 /\ -ar_0 + ar_2 - 1 >= 0 /\ ar_1 - 2 >= 0 /\ ar_0 + ar_1 - 2 >= 0 /\ ar_0 >= 0 /\ 1 <= ar_0 /\ 0 <= ar_4 /\ 0 < ar_1 /\ 2 <= ar_5 /\ 1 <= ar_2 /\ 0 < ar_0 /\ 1 <= ar_5 ]
(Comp: 1, Cost: 29) main_Load_1(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(langle_init_rangle_Load_313(1, ar_0, 0, ar_0, ar_1, arityPad)) [ 1 <= ar_0 /\ static'1 <= static''' + 1 /\ 0 <= static''' /\ static''' <= ar_2 + 2 /\ 0 <= ar_2 /\ 0 < ar_0 /\ 0 <= static'1 ]
start location: koat_start
leaf cost: 0

Complexity upper bound 263*ar_0 + 150*ar_0^2 + 35

Time: 0.846 sec (SMT: 0.681 sec)

(0) Obligation:

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

(2) Obligation:

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

(4) Obligation:

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

(6) Obligation:

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

(8) Obligation:

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

(10) Obligation:

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

(12) Obligation:

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

(14) Obligation:

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

(16) Obligation:

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

(18) Obligation:

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

(20) Obligation:

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

(22) Obligation:

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

(24) Obligation:

(25) TerminationGraphToComplexityProof (BOTH CONCRETE BOUNDS(ID, ADD(11)) transformation)

(26) Obligation:

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

(28) Obligation:

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

(30) Obligation:

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

(32) Obligation:

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

(34) Obligation:

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

(36) Obligation:

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

(38) Obligation:

(39) koat Proof (EQUIVALENT transformation)

(40) BOUNDS(CONSTANT, 35 + 263 * |#0| + 150 * |#0|^2)