time complexity proof of /tmp/tmpgpGLWL/GCD.jar

The time complexity of the given JBC problem could be proven to be BOUNDS(CONSTANT, 303 + 300 * |#0| + 1059 * |#0| * |#1| + 828 * |#0| * |#1|^2 + 276 * |#0|^2 + 276 * |#0|^2 * |#1| + 894 * |#1| + 1083 * |#1|^2 + 552 * |#1|^3).

0 JBC problem

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

↳2 JBCTerminationGraph

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

↳4 JBCComplexityEdges

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

    ↳6 WeightedIntTrs

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

        ↳8 WeightedIntTrs

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

        ↳10 WeightedIntTrs

        ↳11 RemoveDivModProof (CONCRETE UPPER BOUND(ID), 0 ms)

        ↳12 WeightedIntTrs

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

        ↳14 WeightedIntTrs

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

        ↳16 WeightedIntTrs

    ↳17 JBCGraphEdgesToCpxIntTrsProof (CONCRETE UPPER BOUND(ID), 144 ms)

    ↳18 WeightedIntTrs

        ↳19 StraightLineCodeCompressionProof (BOTH CONCRETE BOUNDS(ID, ID), 37 ms)

        ↳20 WeightedIntTrs

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

        ↳22 WeightedIntTrs

        ↳23 RemoveDivModProof (CONCRETE UPPER BOUND(ID), 0 ms)

        ↳24 WeightedIntTrs

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

        ↳26 WeightedIntTrs

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

        ↳28 WeightedIntTrs

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

↳30 JBCComplexityEdges

    ↳31 JBCGraphEdgesToCpxIntTrsProof (CONCRETE UPPER BOUND(ID), 74 ms)

    ↳32 WeightedIntTrs

    ↳33 StraightLineCodeCompressionProof (BOTH CONCRETE BOUNDS(ID, ID), 49 ms)

    ↳34 WeightedIntTrs

    ↳35 WeightedIntTrsUnneededArgumentFilterProof (CONCRETE UPPER BOUND(ID), 35 ms)

    ↳36 WeightedIntTrs

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

    ↳38 WeightedIntTrs

    ↳39 RemoveDivModProof (CONCRETE UPPER BOUND(ID), 0 ms)

    ↳40 WeightedIntTrs

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

    ↳42 WeightedIntTrs

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

    ↳44 WeightedIntTrs

    ↳45 koat Proof (⇔, 1043 ms)

    ↳46 BOUNDS(CONSTANT, 300 + 300 * |#0| + 1059 * |#0| * |#1| + 828 * |#0| * |#1|^2 + 276 * |#0|^2 + 276 * |#0|^2 * |#1| + 894 * |#1| + 1083 * |#1|^2 + 552 * |#1|^3)

(0) Obligation:

Need to prove time_complexity of the following program:

public class GCD {
  public static int mod(int a, int b) {
    if(a <= 0 || b <= 0)
      return 0;
    if (a == b) {
      return 0;
    }
    while(a>b) {
      a -= b;
    }
    return a;
  }

  public static int gcd(int a, int b) {
    int tmp;
    while(b != 0) {
      tmp = b;
      b = mod(a, b);
      a = tmp;
    }
    return a;
  }

}

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

Constructed TerminationGraph.

(2) Obligation:

Termination Graph based on JBC Program:
GCD.gcd(II)I: Graph of 82 nodes with 1 SCC.

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

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

(4) Obligation:

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

Used field analysis yielded the following read fields:

Considered paths: nonterm paths and paths from start to sinks

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

Transformed 83 jbc graph edges to a weighted ITS with 83 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 83 rules
Start term: gcd_Load_2(#0, #1, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
gcd_Load_2(i1, i4, env, static) -{0,0}> gcd_Load_4(i1, i4, env, static) :|: 0 >= 0
gcd_Load_4(i1, i4, env, static) -{0,0}> langle_clinit_rangle_ConstantStackPush_6(i1, i4, env, static) :|: 0 >= 0
langle_clinit_rangle_ConstantStackPush_6(i1, i4, env, static) -{1,1}> langle_clinit_rangle_ArrayCreate_12(iconst_0, i1, i4, env, static) :|: iconst_0 = 0
langle_clinit_rangle_ArrayCreate_12(iconst_0, i1, i4, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_14(a2, i1, i4, iconst_0, env, static) :|: a2 = 2 && iconst_0 = 0 && 0 < a2
langle_clinit_rangle_FieldAccess_14(a2, i1, i4, iconst_0, env, static) -{1,1}> langle_clinit_rangle_New_16(i1, i4, env, static') :|: 0 <= a2 && iconst_0 = 0 && static' <= static + a2 && 0 <= static && 0 < a2
langle_clinit_rangle_New_16(i1, i4, env, static) -{0,0}> langle_clinit_rangle_New_17(i1, i4, env, static) :|: 0 >= 0
langle_clinit_rangle_New_17(i1, i4, env, static) -{0,0}> langle_clinit_rangle_New_19(i1, i4, env, static) :|: 0 <= static
langle_clinit_rangle_New_19(i1, i4, env, static) -{1,1}> langle_clinit_rangle_Duplicate_20(o2, i1, i4, env, static) :|: 0 < o2 && o2 = 1
langle_clinit_rangle_Duplicate_20(o2, i1, i4, env, static) -{1,1}> langle_clinit_rangle_ConstantStackPush_22(o2, i1, i4, env, static) :|: 0 < o2
langle_clinit_rangle_ConstantStackPush_22(o2, i1, i4, env, static) -{1,1}> langle_clinit_rangle_InvokeMethod_23(o2, NULL, i1, i4, env, static) :|: NULL = 0 && 0 < o2
langle_clinit_rangle_InvokeMethod_23(o2, NULL, i1, i4, env, static) -{1,1}> langle_init_rangle_Load_24(o2, i1, i4, env, static) :|: NULL = 0 && 0 < o2
langle_init_rangle_Load_24(o2, i1, i4, env, static) -{1,1}> langle_init_rangle_InvokeMethod_25(o2, i1, i4, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_25(o2, i1, i4, env, static) -{1,1}> langle_init_rangle_Load_26(o2, i1, i4, env, static) :|: 0 < o2
langle_init_rangle_Load_26(o2, i1, i4, env, static) -{1,1}> langle_init_rangle_InvokeMethod_28(o2, i1, i4, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_28(o2, i1, i4, env, static) -{1,1}> langle_init_rangle_Return_31(o2, i1, i4, env, static) :|: 0 < o2
langle_init_rangle_Return_31(o2, i1, i4, env, static) -{1,1}> langle_init_rangle_Return_33(o2, i1, i4, env, static) :|: 0 < o2
langle_init_rangle_Return_33(o2, i1, i4, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_35(o2, i1, i4, env, static) :|: 0 < o2
langle_clinit_rangle_FieldAccess_35(o2, i1, i4, env, static) -{1,1}> langle_clinit_rangle_Return_38(i1, i4, env, static') :|: 0 < o2 && 0 <= o2 && 0 <= static && static' <= static + o2
langle_clinit_rangle_Return_38(i1, i4, env, static) -{1,1}> gcd_Load_41(i1, i4, env, static) :|: 0 >= 0
gcd_Load_41(i1, i4, env, static) -{0,0}> gcd_Load_42(i1, i4, env, static) :|: 0 >= 0
gcd_Load_42(i1, i4, env, static) -{0,0}> gcd_Load_49(i1, i4, env, static) :|: 0 <= static
gcd_Load_49(i1, i4, env, static) -{0,0}> gcd_Load_50(i1, i4, env, static) :|: 0 >= 0
gcd_Load_50(i1, i4, env, static) -{0,0}> gcd_Load_51(i1, i4, env, static) :|: 0 >= 0
gcd_Load_51(i1, i4, env, static) -{0,0}> gcd_Load_314(i1, i4, i1, i4, env, static) :|: 0 >= 0
gcd_Load_314(i92, i93, i94, i95, env, static) -{1,1}> gcd_EQ_316(i92, i93, i95, i94, env, static) :|: 0 >= 0
gcd_EQ_316(i92, i93, i107, i94, env, static) -{0,0}> gcd_EQ_318(i92, i93, i107, i94, env, static) :|: 0 >= 0
gcd_EQ_316(i92, i93, iconst_0, i94, env, static) -{0,0}> gcd_EQ_319(i92, i93, iconst_0, i94, env, static) :|: iconst_0 = 0
gcd_EQ_318(i92, i93, i107, i94, env, static) -{1,1}> gcd_Load_320(i92, i93, i94, i107, env, static) :|: !(i107 = 0)
gcd_Load_320(i92, i93, i94, i107, env, static) -{1,1}> gcd_Store_322(i92, i93, i107, i94, env, static) :|: 0 >= 0
gcd_Store_322(i92, i93, i107, i94, env, static) -{1,1}> gcd_Load_326(i92, i93, i94, i107, env, static) :|: 0 >= 0
gcd_Load_326(i92, i93, i94, i107, env, static) -{1,1}> gcd_Load_330(i92, i93, i94, i107, env, static) :|: 0 >= 0
gcd_Load_330(i92, i93, i94, i107, env, static) -{1,1}> gcd_InvokeMethod_332(i92, i93, i94, i107, env, static) :|: 0 >= 0
gcd_InvokeMethod_332(i92, i93, i94, i107, env, static) -{1,1}> mod_Load_334(i94, i107, i92, i93, env, static) :|: 0 >= 0
mod_Load_334(i94, i107, i92, i93, env, static) -{1,1}> mod_LE_338(i94, i107, i92, i93, env, static) :|: 0 >= 0
mod_LE_338(i112, i107, i92, i93, env, static) -{0,0}> mod_LE_340(i112, i107, i92, i93, env, static) :|: i112 <= 0
mod_LE_338(i113, i107, i92, i93, env, static) -{0,0}> mod_LE_341(i113, i107, i92, i93, env, static) :|: 1 <= i113
mod_LE_340(i112, i107, i92, i93, env, static) -{1,1}> mod_ConstantStackPush_343(i92, i93, i107, env, static) :|: i112 <= 0
mod_LE_341(i113, i107, i92, i93, env, static) -{1,1}> mod_Load_346(i113, i107, i92, i93, env, static) :|: 1 <= i113 && 0 < i113
mod_ConstantStackPush_343(i92, i93, i107, env, static) -{1,1}> mod_Return_348(iconst_0, i92, i93, i107, env, static) :|: iconst_0 = 0
mod_Load_346(i113, i107, i92, i93, env, static) -{1,1}> mod_GT_350(i107, i113, i92, i93, env, static) :|: 1 <= i113
mod_Return_348(iconst_0, i92, i93, i107, env, static) -{1,1}> gcd_Store_351(i92, i93, iconst_0, i107, env, static) :|: iconst_0 = 0
mod_GT_350(i118, i113, i92, i93, env, static) -{0,0}> mod_GT_352(i118, i113, i92, i93, env, static) :|: 1 <= i113 && i118 <= -1
mod_GT_350(i119, i113, i92, i93, env, static) -{0,0}> mod_GT_353(i119, i113, i92, i93, env, static) :|: 1 <= i113 && 1 <= i119
gcd_Store_351(i92, i93, iconst_0, i107, env, static) -{1,1}> gcd_Load_354(i92, i93, iconst_0, i107, env, static) :|: iconst_0 = 0
mod_GT_352(i118, i113, i92, i93, env, static) -{1,1}> mod_ConstantStackPush_355(i92, i93, i118, env, static) :|: 1 <= i113 && i118 <= -1 && i118 <= 0
mod_GT_353(i119, i113, i92, i93, env, static) -{1,1}> mod_Load_356(i113, i119, i92, i93, env, static) :|: 1 <= i113 && 1 <= i119 && 0 < i119
gcd_Load_354(i92, i93, iconst_0, i107, env, static) -{0,0}> gcd_Load_463(i92, i93, iconst_0, i107, env, static) :|: iconst_0 = 0
mod_ConstantStackPush_355(i92, i93, i118, env, static) -{1,1}> mod_Return_358(iconst_0, i92, i93, i118, env, static) :|: i118 <= -1 && iconst_0 = 0
mod_Load_356(i113, i119, i92, i93, env, static) -{1,1}> mod_Load_361(i113, i119, i92, i93, env, static) :|: 1 <= i113 && 1 <= i119
mod_Return_358(iconst_0, i92, i93, i118, env, static) -{1,1}> gcd_Store_363(i92, i93, iconst_0, i118, env, static) :|: i118 <= -1 && iconst_0 = 0
mod_Load_361(i113, i119, i92, i93, env, static) -{1,1}> mod_NE_369(i113, i119, i92, i93, env, static) :|: 1 <= i113 && 1 <= i119
gcd_Store_363(i92, i93, iconst_0, i118, env, static) -{1,1}> gcd_Load_372(i92, i93, iconst_0, i118, env, static) :|: i118 <= -1 && iconst_0 = 0
mod_NE_369(i113, i119, i92, i93, env, static) -{0,0}> mod_NE_374(i113, i119, i92, i93, env, static) :|: 1 <= i113 && !(i113 = i119) && 1 <= i119
mod_NE_369(i113, i119, i92, i93, env, static) -{0,0}> mod_NE_376(i119, i92, i93, env, static) :|: 1 <= i113 && i113 = i119 && 1 <= i119
gcd_Load_372(i92, i93, iconst_0, i118, env, static) -{0,0}> gcd_Load_463(i92, i93, iconst_0, i118, env, static) :|: i118 <= -1 && iconst_0 = 0
mod_NE_374(i113, i119, i92, i93, env, static) -{1,1}> mod_Load_382(i113, i119, i92, i93, env, static) :|: 1 <= i113 && !(i113 = i119) && 1 <= i119
mod_NE_376(i119, i92, i93, env, static) -{1,1}> mod_ConstantStackPush_385(i92, i93, i119, env, static) :|: i119 = i119 && 1 <= i119
mod_Load_382(i113, i119, i92, i93, env, static) -{0,0}> mod_Load_470(i113, i119, i92, i93, env, static) :|: 1 <= i113 && 1 <= i119
mod_ConstantStackPush_385(i92, i93, i119, env, static) -{1,1}> mod_Return_390(iconst_0, i92, i93, i119, env, static) :|: 1 <= i119 && iconst_0 = 0
mod_Return_390(iconst_0, i92, i93, i119, env, static) -{1,1}> gcd_Store_405(i92, i93, iconst_0, i119, env, static) :|: 1 <= i119 && iconst_0 = 0
gcd_Store_405(i92, i93, iconst_0, i119, env, static) -{0,0}> gcd_Store_445(i92, i93, iconst_0, i119, env, static) :|: 1 <= i119 && iconst_0 = 0
gcd_Store_445(i92, i93, i130, i129, env, static) -{0,0}> gcd_Store_509(i92, i93, i130, i129, env, static) :|: 0 >= 0
gcd_Load_463(i92, i93, i142, i143, env, static) -{1,1}> gcd_Store_467(i92, i93, i143, i142, env, static) :|: 0 >= 0
gcd_Store_467(i92, i93, i143, i142, env, static) -{1,1}> gcd_JMP_469(i92, i93, i143, i142, env, static) :|: 0 >= 0
gcd_JMP_469(i92, i93, i143, i142, env, static) -{1,1}> gcd_Load_471(i92, i93, i143, i142, env, static) :|: 0 >= 0
mod_Load_470(i150, i119, i92, i93, env, static) -{1,1}> mod_Load_474(i150, i119, i92, i93, env, static) :|: 1 <= i150 && 1 <= i119
gcd_Load_471(i92, i93, i143, i142, env, static) -{0,0}> gcd_Load_314(i92, i93, i143, i142, env, static) :|: 0 >= 0
mod_Load_474(i150, i119, i92, i93, env, static) -{1,1}> mod_LE_475(i150, i119, i92, i93, env, static) :|: 1 <= i150 && 1 <= i119
mod_LE_475(i150, i119, i92, i93, env, static) -{0,0}> mod_LE_476(i150, i119, i92, i93, env, static) :|: 1 <= i150 && 1 <= i119 && i150 <= i119
mod_LE_475(i150, i119, i92, i93, env, static) -{0,0}> mod_LE_477(i150, i119, i92, i93, env, static) :|: 1 <= i150 && 1 <= i119 && i119 < i150
mod_LE_476(i150, i119, i92, i93, env, static) -{1,1}> mod_Load_481(i150, i92, i93, i119, env, static) :|: 1 <= i150 && 1 <= i119 && i150 <= i119
mod_LE_477(i150, i119, i92, i93, env, static) -{1,1}> mod_Load_485(i150, i119, i92, i93, env, static) :|: 1 <= i150 && 2 <= i150 && 1 <= i119 && i119 < i150
mod_Load_481(i150, i92, i93, i119, env, static) -{1,1}> mod_Return_486(i150, i92, i93, i119, env, static) :|: 1 <= i150 && 1 <= i119
mod_Load_485(i150, i119, i92, i93, env, static) -{1,1}> mod_Load_487(i150, i119, i92, i93, env, static) :|: 2 <= i150 && 1 <= i119
mod_Return_486(i150, i92, i93, i119, env, static) -{1,1}> gcd_Store_508(i92, i93, i150, i119, env, static) :|: 1 <= i150 && 1 <= i119
mod_Load_487(i150, i119, i92, i93, env, static) -{1,1}> mod_IntArithmetic_510(i150, i119, i92, i93, env, static) :|: 2 <= i150 && 1 <= i119
gcd_Store_508(i92, i93, i150, i119, env, static) -{0,0}> gcd_Store_509(i92, i93, i150, i119, env, static) :|: 1 <= i150 && 1 <= i119
gcd_Store_509(i92, i93, i160, i159, env, static) -{1,1}> gcd_Load_516(i92, i93, i160, i159, env, static) :|: 0 >= 0
mod_IntArithmetic_510(i150, i119, i92, i93, env, static) -{1,1}> mod_Store_521(i172, i119, i92, i93, env, static) :|: 1 <= i172 && 2 <= i150 && 1 <= i119 && i150 - i119 = i172
gcd_Load_516(i92, i93, i160, i159, env, static) -{0,0}> gcd_Load_463(i92, i93, i160, i159, env, static) :|: 0 >= 0
mod_Store_521(i172, i119, i92, i93, env, static) -{1,1}> mod_JMP_530(i172, i119, i92, i93, env, static) :|: 1 <= i172 && 1 <= i119
mod_JMP_530(i172, i119, i92, i93, env, static) -{1,1}> mod_Load_539(i172, i119, i92, i93, env, static) :|: 1 <= i172 && 1 <= i119
mod_Load_539(i172, i119, i92, i93, env, static) -{0,0}> mod_Load_470(i172, i119, i92, i93, env, static) :|: 1 <= i172 && 1 <= i119

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

obtained
gcd_Load_2(i1, i4, env, static) -{15,15}> gcd_Load_314(i1, i4, i1, i4, env, static'1) :|: 0 >= 0 && static'1 <= static''' + 1 && 0 <= 2 && 0 <= static''' && static''' <= static + 2 && 0 < 1 && 0 <= 1 && 0 <= static && 0 <= static'1 && 0 < 2
by chaining
gcd_Load_2(i1, i4, env, static) -{0,0}> gcd_Load_4(i1, i4, env, static) :|: 0 >= 0
gcd_Load_4(i1, i4, env, static) -{0,0}> langle_clinit_rangle_ConstantStackPush_6(i1, i4, env, static) :|: 0 >= 0
langle_clinit_rangle_ConstantStackPush_6(i1, i4, env, static) -{1,1}> langle_clinit_rangle_ArrayCreate_12(iconst_0, i1, i4, env, static) :|: iconst_0 = 0
langle_clinit_rangle_ArrayCreate_12(iconst_0, i1, i4, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_14(a2, i1, i4, iconst_0, env, static) :|: a2 = 2 && iconst_0 = 0 && 0 < a2
langle_clinit_rangle_FieldAccess_14(a2, i1, i4, iconst_0, env, static) -{1,1}> langle_clinit_rangle_New_16(i1, i4, env, static') :|: 0 <= a2 && iconst_0 = 0 && static' <= static + a2 && 0 <= static && 0 < a2
langle_clinit_rangle_New_16(i1, i4, env, static) -{0,0}> langle_clinit_rangle_New_17(i1, i4, env, static) :|: 0 >= 0
langle_clinit_rangle_New_17(i1, i4, env, static) -{0,0}> langle_clinit_rangle_New_19(i1, i4, env, static) :|: 0 <= static
langle_clinit_rangle_New_19(i1, i4, env, static) -{1,1}> langle_clinit_rangle_Duplicate_20(o2, i1, i4, env, static) :|: 0 < o2 && o2 = 1
langle_clinit_rangle_Duplicate_20(o2, i1, i4, env, static) -{1,1}> langle_clinit_rangle_ConstantStackPush_22(o2, i1, i4, env, static) :|: 0 < o2
langle_clinit_rangle_ConstantStackPush_22(o2, i1, i4, env, static) -{1,1}> langle_clinit_rangle_InvokeMethod_23(o2, NULL, i1, i4, env, static) :|: NULL = 0 && 0 < o2
langle_clinit_rangle_InvokeMethod_23(o2, NULL, i1, i4, env, static) -{1,1}> langle_init_rangle_Load_24(o2, i1, i4, env, static) :|: NULL = 0 && 0 < o2
langle_init_rangle_Load_24(o2, i1, i4, env, static) -{1,1}> langle_init_rangle_InvokeMethod_25(o2, i1, i4, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_25(o2, i1, i4, env, static) -{1,1}> langle_init_rangle_Load_26(o2, i1, i4, env, static) :|: 0 < o2
langle_init_rangle_Load_26(o2, i1, i4, env, static) -{1,1}> langle_init_rangle_InvokeMethod_28(o2, i1, i4, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_28(o2, i1, i4, env, static) -{1,1}> langle_init_rangle_Return_31(o2, i1, i4, env, static) :|: 0 < o2
langle_init_rangle_Return_31(o2, i1, i4, env, static) -{1,1}> langle_init_rangle_Return_33(o2, i1, i4, env, static) :|: 0 < o2
langle_init_rangle_Return_33(o2, i1, i4, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_35(o2, i1, i4, env, static) :|: 0 < o2
langle_clinit_rangle_FieldAccess_35(o2, i1, i4, env, static) -{1,1}> langle_clinit_rangle_Return_38(i1, i4, env, static') :|: 0 < o2 && 0 <= o2 && 0 <= static && static' <= static + o2
langle_clinit_rangle_Return_38(i1, i4, env, static) -{1,1}> gcd_Load_41(i1, i4, env, static) :|: 0 >= 0
gcd_Load_41(i1, i4, env, static) -{0,0}> gcd_Load_42(i1, i4, env, static) :|: 0 >= 0
gcd_Load_42(i1, i4, env, static) -{0,0}> gcd_Load_49(i1, i4, env, static) :|: 0 <= static
gcd_Load_49(i1, i4, env, static) -{0,0}> gcd_Load_50(i1, i4, env, static) :|: 0 >= 0
gcd_Load_50(i1, i4, env, static) -{0,0}> gcd_Load_51(i1, i4, env, static) :|: 0 >= 0
gcd_Load_51(i1, i4, env, static) -{0,0}> gcd_Load_314(i1, i4, i1, i4, env, static) :|: 0 >= 0

obtained
gcd_EQ_316(i92, i93, i107, i94, env, static) -{7,7}> mod_LE_338(i94, i107, i92, i93, env, static) :|: 0 >= 0 && !(i107 = 0)
by chaining
gcd_EQ_316(i92, i93, i107, i94, env, static) -{0,0}> gcd_EQ_318(i92, i93, i107, i94, env, static) :|: 0 >= 0
gcd_EQ_318(i92, i93, i107, i94, env, static) -{1,1}> gcd_Load_320(i92, i93, i94, i107, env, static) :|: !(i107 = 0)
gcd_Load_320(i92, i93, i94, i107, env, static) -{1,1}> gcd_Store_322(i92, i93, i107, i94, env, static) :|: 0 >= 0
gcd_Store_322(i92, i93, i107, i94, env, static) -{1,1}> gcd_Load_326(i92, i93, i94, i107, env, static) :|: 0 >= 0
gcd_Load_326(i92, i93, i94, i107, env, static) -{1,1}> gcd_Load_330(i92, i93, i94, i107, env, static) :|: 0 >= 0
gcd_Load_330(i92, i93, i94, i107, env, static) -{1,1}> gcd_InvokeMethod_332(i92, i93, i94, i107, env, static) :|: 0 >= 0
gcd_InvokeMethod_332(i92, i93, i94, i107, env, static) -{1,1}> mod_Load_334(i94, i107, i92, i93, env, static) :|: 0 >= 0
mod_Load_334(i94, i107, i92, i93, env, static) -{1,1}> mod_LE_338(i94, i107, i92, i93, env, static) :|: 0 >= 0

obtained
mod_LE_338(i113, i107, i92, i93, env, static) -{2,2}> mod_GT_350(i107, i113, i92, i93, env, static) :|: 1 <= i113 && 0 < i113
by chaining
mod_LE_338(i113, i107, i92, i93, env, static) -{0,0}> mod_LE_341(i113, i107, i92, i93, env, static) :|: 1 <= i113
mod_LE_341(i113, i107, i92, i93, env, static) -{1,1}> mod_Load_346(i113, i107, i92, i93, env, static) :|: 1 <= i113 && 0 < i113
mod_Load_346(i113, i107, i92, i93, env, static) -{1,1}> mod_GT_350(i107, i113, i92, i93, env, static) :|: 1 <= i113

obtained
mod_GT_350(i119, i113, i92, i93, env, static) -{3,3}> mod_NE_369(i113, i119, i92, i93, env, static) :|: 1 <= i119 && 1 <= i113 && 0 < i119
by chaining
mod_GT_350(i119, i113, i92, i93, env, static) -{0,0}> mod_GT_353(i119, i113, i92, i93, env, static) :|: 1 <= i113 && 1 <= i119
mod_GT_353(i119, i113, i92, i93, env, static) -{1,1}> mod_Load_356(i113, i119, i92, i93, env, static) :|: 1 <= i113 && 1 <= i119 && 0 < i119
mod_Load_356(i113, i119, i92, i93, env, static) -{1,1}> mod_Load_361(i113, i119, i92, i93, env, static) :|: 1 <= i113 && 1 <= i119
mod_Load_361(i113, i119, i92, i93, env, static) -{1,1}> mod_NE_369(i113, i119, i92, i93, env, static) :|: 1 <= i113 && 1 <= i119

obtained
mod_NE_369(i113, i113, i92, i93, env, static) -{3,3}> gcd_Store_509(i92, i93, 0, i113, env, static) :|: 1 <= i113 && 0 >= 0
by chaining
mod_NE_369(i113, i119, i92, i93, env, static) -{0,0}> mod_NE_376(i119, i92, i93, env, static) :|: 1 <= i113 && i113 = i119 && 1 <= i119
mod_NE_376(i119, i92, i93, env, static) -{1,1}> mod_ConstantStackPush_385(i92, i93, i119, env, static) :|: i119 = i119 && 1 <= i119
mod_ConstantStackPush_385(i92, i93, i119, env, static) -{1,1}> mod_Return_390(iconst_0, i92, i93, i119, env, static) :|: 1 <= i119 && iconst_0 = 0
mod_Return_390(iconst_0, i92, i93, i119, env, static) -{1,1}> gcd_Store_405(i92, i93, iconst_0, i119, env, static) :|: 1 <= i119 && iconst_0 = 0
gcd_Store_405(i92, i93, iconst_0, i119, env, static) -{0,0}> gcd_Store_445(i92, i93, iconst_0, i119, env, static) :|: 1 <= i119 && iconst_0 = 0
gcd_Store_445(i92, i93, i130, i129, env, static) -{0,0}> gcd_Store_509(i92, i93, i130, i129, env, static) :|: 0 >= 0

obtained
gcd_Store_509(i92, i93, i160, i159, env, static) -{1,1}> gcd_Load_463(i92, i93, i160, i159, env, static) :|: 0 >= 0
by chaining
gcd_Store_509(i92, i93, i160, i159, env, static) -{1,1}> gcd_Load_516(i92, i93, i160, i159, env, static) :|: 0 >= 0
gcd_Load_516(i92, i93, i160, i159, env, static) -{0,0}> gcd_Load_463(i92, i93, i160, i159, env, static) :|: 0 >= 0

obtained
gcd_Load_463(i92, i93, i142, i143, env, static) -{3,3}> gcd_Load_314(i92, i93, i143, i142, env, static) :|: 0 >= 0
by chaining
gcd_Load_463(i92, i93, i142, i143, env, static) -{1,1}> gcd_Store_467(i92, i93, i143, i142, env, static) :|: 0 >= 0
gcd_Store_467(i92, i93, i143, i142, env, static) -{1,1}> gcd_JMP_469(i92, i93, i143, i142, env, static) :|: 0 >= 0
gcd_JMP_469(i92, i93, i143, i142, env, static) -{1,1}> gcd_Load_471(i92, i93, i143, i142, env, static) :|: 0 >= 0
gcd_Load_471(i92, i93, i143, i142, env, static) -{0,0}> gcd_Load_314(i92, i93, i143, i142, env, static) :|: 0 >= 0

obtained
mod_NE_369(i113, i119, i92, i93, env, static) -{1,1}> mod_Load_470(i113, i119, i92, i93, env, static) :|: !(i113 = i119) && 1 <= i113 && 1 <= i119
by chaining
mod_NE_369(i113, i119, i92, i93, env, static) -{0,0}> mod_NE_374(i113, i119, i92, i93, env, static) :|: 1 <= i113 && !(i113 = i119) && 1 <= i119
mod_NE_374(i113, i119, i92, i93, env, static) -{1,1}> mod_Load_382(i113, i119, i92, i93, env, static) :|: 1 <= i113 && !(i113 = i119) && 1 <= i119
mod_Load_382(i113, i119, i92, i93, env, static) -{0,0}> mod_Load_470(i113, i119, i92, i93, env, static) :|: 1 <= i113 && 1 <= i119

obtained
mod_Load_470(i150, i119, i92, i93, env, static) -{2,2}> mod_LE_475(i150, i119, i92, i93, env, static) :|: 1 <= i150 && 1 <= i119
by chaining
mod_Load_470(i150, i119, i92, i93, env, static) -{1,1}> mod_Load_474(i150, i119, i92, i93, env, static) :|: 1 <= i150 && 1 <= i119
mod_Load_474(i150, i119, i92, i93, env, static) -{1,1}> mod_LE_475(i150, i119, i92, i93, env, static) :|: 1 <= i150 && 1 <= i119

obtained
mod_LE_475(i150, i119, i92, i93, env, static) -{6,6}> mod_Load_470(i172', i119, i92, i93, env, static) :|: 2 <= i150 && 1 <= i172' && 1 <= i119 && 1 <= i150 && i119 < i150 && i150 - i119 = i172'
by chaining
mod_LE_475(i150, i119, i92, i93, env, static) -{0,0}> mod_LE_477(i150, i119, i92, i93, env, static) :|: 1 <= i150 && 1 <= i119 && i119 < i150
mod_LE_477(i150, i119, i92, i93, env, static) -{1,1}> mod_Load_485(i150, i119, i92, i93, env, static) :|: 1 <= i150 && 2 <= i150 && 1 <= i119 && i119 < i150
mod_Load_485(i150, i119, i92, i93, env, static) -{1,1}> mod_Load_487(i150, i119, i92, i93, env, static) :|: 2 <= i150 && 1 <= i119
mod_Load_487(i150, i119, i92, i93, env, static) -{1,1}> mod_IntArithmetic_510(i150, i119, i92, i93, env, static) :|: 2 <= i150 && 1 <= i119
mod_IntArithmetic_510(i150, i119, i92, i93, env, static) -{1,1}> mod_Store_521(i172, i119, i92, i93, env, static) :|: 1 <= i172 && 2 <= i150 && 1 <= i119 && i150 - i119 = i172
mod_Store_521(i172, i119, i92, i93, env, static) -{1,1}> mod_JMP_530(i172, i119, i92, i93, env, static) :|: 1 <= i172 && 1 <= i119
mod_JMP_530(i172, i119, i92, i93, env, static) -{1,1}> mod_Load_539(i172, i119, i92, i93, env, static) :|: 1 <= i172 && 1 <= i119
mod_Load_539(i172, i119, i92, i93, env, static) -{0,0}> mod_Load_470(i172, i119, i92, i93, env, static) :|: 1 <= i172 && 1 <= i119

obtained
mod_LE_475(i150, i119, i92, i93, env, static) -{3,3}> gcd_Store_509(i92, i93, i150, i119, env, static) :|: 1 <= i119 && 1 <= i150 && i150 <= i119
by chaining
mod_LE_475(i150, i119, i92, i93, env, static) -{0,0}> mod_LE_476(i150, i119, i92, i93, env, static) :|: 1 <= i150 && 1 <= i119 && i150 <= i119
mod_LE_476(i150, i119, i92, i93, env, static) -{1,1}> mod_Load_481(i150, i92, i93, i119, env, static) :|: 1 <= i150 && 1 <= i119 && i150 <= i119
mod_Load_481(i150, i92, i93, i119, env, static) -{1,1}> mod_Return_486(i150, i92, i93, i119, env, static) :|: 1 <= i150 && 1 <= i119
mod_Return_486(i150, i92, i93, i119, env, static) -{1,1}> gcd_Store_508(i92, i93, i150, i119, env, static) :|: 1 <= i150 && 1 <= i119
gcd_Store_508(i92, i93, i150, i119, env, static) -{0,0}> gcd_Store_509(i92, i93, i150, i119, env, static) :|: 1 <= i150 && 1 <= i119

obtained
mod_GT_350(i118, i113, i92, i93, env, static) -{4,4}> gcd_Load_463(i92, i93, 0, i118, env, static) :|: 1 <= i113 && i118 <= -1 && i118 <= 0
by chaining
mod_GT_350(i118, i113, i92, i93, env, static) -{0,0}> mod_GT_352(i118, i113, i92, i93, env, static) :|: 1 <= i113 && i118 <= -1
mod_GT_352(i118, i113, i92, i93, env, static) -{1,1}> mod_ConstantStackPush_355(i92, i93, i118, env, static) :|: 1 <= i113 && i118 <= -1 && i118 <= 0
mod_ConstantStackPush_355(i92, i93, i118, env, static) -{1,1}> mod_Return_358(iconst_0, i92, i93, i118, env, static) :|: i118 <= -1 && iconst_0 = 0
mod_Return_358(iconst_0, i92, i93, i118, env, static) -{1,1}> gcd_Store_363(i92, i93, iconst_0, i118, env, static) :|: i118 <= -1 && iconst_0 = 0
gcd_Store_363(i92, i93, iconst_0, i118, env, static) -{1,1}> gcd_Load_372(i92, i93, iconst_0, i118, env, static) :|: i118 <= -1 && iconst_0 = 0
gcd_Load_372(i92, i93, iconst_0, i118, env, static) -{0,0}> gcd_Load_463(i92, i93, iconst_0, i118, env, static) :|: i118 <= -1 && iconst_0 = 0

obtained
mod_LE_338(i112, i107, i92, i93, env, static) -{4,4}> gcd_Load_463(i92, i93, 0, i107, env, static) :|: i112 <= 0
by chaining
mod_LE_338(i112, i107, i92, i93, env, static) -{0,0}> mod_LE_340(i112, i107, i92, i93, env, static) :|: i112 <= 0
mod_LE_340(i112, i107, i92, i93, env, static) -{1,1}> mod_ConstantStackPush_343(i92, i93, i107, env, static) :|: i112 <= 0
mod_ConstantStackPush_343(i92, i93, i107, env, static) -{1,1}> mod_Return_348(iconst_0, i92, i93, i107, env, static) :|: iconst_0 = 0
mod_Return_348(iconst_0, i92, i93, i107, env, static) -{1,1}> gcd_Store_351(i92, i93, iconst_0, i107, env, static) :|: iconst_0 = 0
gcd_Store_351(i92, i93, iconst_0, i107, env, static) -{1,1}> gcd_Load_354(i92, i93, iconst_0, i107, env, static) :|: iconst_0 = 0
gcd_Load_354(i92, i93, iconst_0, i107, env, static) -{0,0}> gcd_Load_463(i92, i93, iconst_0, i107, env, static) :|: iconst_0 = 0

(8) Obligation:

IntTrs with 15 rules
Start term: gcd_Load_2(#0, #1, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
gcd_Load_2(i1, i4, env, static) -{15,15}> gcd_Load_314(i1, i4, i1, i4, env, static'1) :|: 0 >= 0 && static'1 <= static''' + 1 && 0 <= 2 && 0 <= static''' && static''' <= static + 2 && 0 < 1 && 0 <= 1 && 0 <= static && 0 <= static'1 && 0 < 2
gcd_Load_314(i92, i93, i94, i95, env, static) -{1,1}> gcd_EQ_316(i92, i93, i95, i94, env, static) :|: 0 >= 0
gcd_EQ_316(i92, i93, iconst_0, i94, env, static) -{0,0}> gcd_EQ_319(i92, i93, iconst_0, i94, env, static) :|: iconst_0 = 0
gcd_EQ_316(i92, i93, i107, i94, env, static) -{7,7}> mod_LE_338(i94, i107, i92, i93, env, static) :|: 0 >= 0 && !(i107 = 0)
mod_LE_338(i113, i107, i92, i93, env, static) -{2,2}> mod_GT_350(i107, i113, i92, i93, env, static) :|: 1 <= i113 && 0 < i113
mod_GT_350(i119, i113, i92, i93, env, static) -{3,3}> mod_NE_369(i113, i119, i92, i93, env, static) :|: 1 <= i119 && 1 <= i113 && 0 < i119
mod_NE_369(i113, i113, i92, i93, env, static) -{3,3}> gcd_Store_509(i92, i93, 0, i113, env, static) :|: 1 <= i113 && 0 >= 0
gcd_Store_509(i92, i93, i160, i159, env, static) -{1,1}> gcd_Load_463(i92, i93, i160, i159, env, static) :|: 0 >= 0
gcd_Load_463(i92, i93, i142, i143, env, static) -{3,3}> gcd_Load_314(i92, i93, i143, i142, env, static) :|: 0 >= 0
mod_NE_369(i113, i119, i92, i93, env, static) -{1,1}> mod_Load_470(i113, i119, i92, i93, env, static) :|: !(i113 = i119) && 1 <= i113 && 1 <= i119
mod_Load_470(i150, i119, i92, i93, env, static) -{2,2}> mod_LE_475(i150, i119, i92, i93, env, static) :|: 1 <= i150 && 1 <= i119
mod_LE_475(i150, i119, i92, i93, env, static) -{6,6}> mod_Load_470(i172', i119, i92, i93, env, static) :|: 2 <= i150 && 1 <= i172' && 1 <= i119 && 1 <= i150 && i119 < i150 && i150 - i119 = i172'
mod_LE_475(i150, i119, i92, i93, env, static) -{3,3}> gcd_Store_509(i92, i93, i150, i119, env, static) :|: 1 <= i119 && 1 <= i150 && i150 <= i119
mod_GT_350(i118, i113, i92, i93, env, static) -{4,4}> gcd_Load_463(i92, i93, 0, i118, env, static) :|: 1 <= i113 && i118 <= -1 && i118 <= 0
mod_LE_338(i112, i107, i92, i93, env, static) -{4,4}> gcd_Load_463(i92, i93, 0, i107, env, static) :|: i112 <= 0

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

Linearized lhss.

mod_NE_369(i113, i113, i92, i93, env, static) -{3,3}> gcd_Store_509(i92, i93, 0, i113, env, static) :|: 1 <= i113 && 0 >= 0
was transformed to
mod_NE_369(i113, x, i92, i93, env, static) -{3,3}> gcd_Store_509(i92, i93, 0, i113, env, static) :|: 1 <= i113 && 0 >= 0 && x = i113

(10) Obligation:

IntTrs with 15 rules
Start term: gcd_Load_2(#0, #1, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
mod_Load_470(i150, i119, i92, i93, env, static) -{2,2}> mod_LE_475(i150, i119, i92, i93, env, static) :|: 1 <= i150 && 1 <= i119
gcd_EQ_316(i92, i93, i107, i94, env, static) -{7,7}> mod_LE_338(i94, i107, i92, i93, env, static) :|: 0 >= 0 && !(i107 = 0)
mod_LE_475(i150, i119, i92, i93, env, static) -{6,6}> mod_Load_470(i172', i119, i92, i93, env, static) :|: 2 <= i150 && 1 <= i172' && 1 <= i119 && 1 <= i150 && i119 < i150 && i150 - i119 = i172'
gcd_EQ_316(i92, i93, iconst_0, i94, env, static) -{0,0}> gcd_EQ_319(i92, i93, iconst_0, i94, env, static) :|: iconst_0 = 0
gcd_Load_463(i92, i93, i142, i143, env, static) -{3,3}> gcd_Load_314(i92, i93, i143, i142, env, static) :|: 0 >= 0
mod_LE_338(i113, i107, i92, i93, env, static) -{2,2}> mod_GT_350(i107, i113, i92, i93, env, static) :|: 1 <= i113 && 0 < i113
gcd_Load_2(i1, i4, env, static) -{15,15}> gcd_Load_314(i1, i4, i1, i4, env, static'1) :|: 0 >= 0 && static'1 <= static''' + 1 && 0 <= 2 && 0 <= static''' && static''' <= static + 2 && 0 < 1 && 0 <= 1 && 0 <= static && 0 <= static'1 && 0 < 2
gcd_Store_509(i92, i93, i160, i159, env, static) -{1,1}> gcd_Load_463(i92, i93, i160, i159, env, static) :|: 0 >= 0
mod_LE_338(i112, i107, i92, i93, env, static) -{4,4}> gcd_Load_463(i92, i93, 0, i107, env, static) :|: i112 <= 0
mod_GT_350(i118, i113, i92, i93, env, static) -{4,4}> gcd_Load_463(i92, i93, 0, i118, env, static) :|: 1 <= i113 && i118 <= -1 && i118 <= 0
gcd_Load_314(i92, i93, i94, i95, env, static) -{1,1}> gcd_EQ_316(i92, i93, i95, i94, env, static) :|: 0 >= 0
mod_LE_475(i150, i119, i92, i93, env, static) -{3,3}> gcd_Store_509(i92, i93, i150, i119, env, static) :|: 1 <= i119 && 1 <= i150 && i150 <= i119
mod_NE_369(i113, i119, i92, i93, env, static) -{1,1}> mod_Load_470(i113, i119, i92, i93, env, static) :|: !(i113 = i119) && 1 <= i113 && 1 <= i119
mod_NE_369(i113, x, i92, i93, env, static) -{3,3}> gcd_Store_509(i92, i93, 0, i113, env, static) :|: 1 <= i113 && 0 >= 0 && x = i113
mod_GT_350(i119, i113, i92, i93, env, static) -{3,3}> mod_NE_369(i113, i119, i92, i93, env, static) :|: 1 <= i119 && 1 <= i113 && 0 < i119

(11) RemoveDivModProof (CONCRETE UPPER BOUND(ID) transformation)

Removed div and mod.

gcd_EQ_316(i92, i93, i107, i94, env, static) -{7,7}> mod_LE_338(i94, i107, i92, i93, env, static) :|: 0 >= 0 && !(i107 = 0)
was transformed to
gcd_EQ_316(i92, i93, i107, i94, env, static) -{7,7}> mod_LE_338(i94, i107, i92, i93, env, static) :|: 0 >= 0 && i107 < 0
gcd_EQ_316(i92, i93, i107, i94, env, static) -{7,7}> mod_LE_338(i94, i107, i92, i93, env, static) :|: 0 >= 0 && i107 > 0

mod_NE_369(i113, i119, i92, i93, env, static) -{1,1}> mod_Load_470(i113, i119, i92, i93, env, static) :|: !(i113 = i119) && 1 <= i113 && 1 <= i119
was transformed to
mod_NE_369(i113, i119, i92, i93, env, static) -{1,1}> mod_Load_470(i113, i119, i92, i93, env, static) :|: i113 < i119 && 1 <= i113 && 1 <= i119
mod_NE_369(i113, i119, i92, i93, env, static) -{1,1}> mod_Load_470(i113, i119, i92, i93, env, static) :|: i113 > i119 && 1 <= i113 && 1 <= i119

(12) Obligation:

IntTrs with 17 rules
Start term: gcd_Load_2(#0, #1, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
mod_Load_470(i150, i119, i92, i93, env, static) -{2,2}> mod_LE_475(i150, i119, i92, i93, env, static) :|: 1 <= i150 && 1 <= i119
mod_LE_475(i150, i119, i92, i93, env, static) -{6,6}> mod_Load_470(i172', i119, i92, i93, env, static) :|: 2 <= i150 && 1 <= i172' && 1 <= i119 && 1 <= i150 && i119 < i150 && i150 - i119 = i172'
mod_NE_369(i113, i119, i92, i93, env, static) -{1,1}> mod_Load_470(i113, i119, i92, i93, env, static) :|: i113 < i119 && 1 <= i113 && 1 <= i119
gcd_EQ_316(i92, i93, iconst_0, i94, env, static) -{0,0}> gcd_EQ_319(i92, i93, iconst_0, i94, env, static) :|: iconst_0 = 0
gcd_Load_463(i92, i93, i142, i143, env, static) -{3,3}> gcd_Load_314(i92, i93, i143, i142, env, static) :|: 0 >= 0
mod_LE_338(i113, i107, i92, i93, env, static) -{2,2}> mod_GT_350(i107, i113, i92, i93, env, static) :|: 1 <= i113 && 0 < i113
gcd_Load_2(i1, i4, env, static) -{15,15}> gcd_Load_314(i1, i4, i1, i4, env, static'1) :|: 0 >= 0 && static'1 <= static''' + 1 && 0 <= 2 && 0 <= static''' && static''' <= static + 2 && 0 < 1 && 0 <= 1 && 0 <= static && 0 <= static'1 && 0 < 2
gcd_Store_509(i92, i93, i160, i159, env, static) -{1,1}> gcd_Load_463(i92, i93, i160, i159, env, static) :|: 0 >= 0
mod_LE_338(i112, i107, i92, i93, env, static) -{4,4}> gcd_Load_463(i92, i93, 0, i107, env, static) :|: i112 <= 0
mod_GT_350(i118, i113, i92, i93, env, static) -{4,4}> gcd_Load_463(i92, i93, 0, i118, env, static) :|: 1 <= i113 && i118 <= -1 && i118 <= 0
gcd_Load_314(i92, i93, i94, i95, env, static) -{1,1}> gcd_EQ_316(i92, i93, i95, i94, env, static) :|: 0 >= 0
mod_NE_369(i113, x, i92, i93, env, static) -{3,3}> gcd_Store_509(i92, i93, 0, i113, env, static) :|: 1 <= i113 && 0 >= 0 && x = i113
mod_LE_475(i150, i119, i92, i93, env, static) -{3,3}> gcd_Store_509(i92, i93, i150, i119, env, static) :|: 1 <= i119 && 1 <= i150 && i150 <= i119
gcd_EQ_316(i92, i93, i107, i94, env, static) -{7,7}> mod_LE_338(i94, i107, i92, i93, env, static) :|: 0 >= 0 && i107 < 0
gcd_EQ_316(i92, i93, i107, i94, env, static) -{7,7}> mod_LE_338(i94, i107, i92, i93, env, static) :|: 0 >= 0 && i107 > 0
mod_GT_350(i119, i113, i92, i93, env, static) -{3,3}> mod_NE_369(i113, i119, i92, i93, env, static) :|: 1 <= i119 && 1 <= i113 && 0 < i119
mod_NE_369(i113, i119, i92, i93, env, static) -{1,1}> mod_Load_470(i113, i119, i92, i93, env, static) :|: i113 > i119 && 1 <= i113 && 1 <= i119

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

Moved arithmethic from constraints to rhss.

mod_LE_475(i150, i119, i92, i93, env, static) -{6,6}> mod_Load_470(i172', i119, i92, i93, env, static) :|: 2 <= i150 && 1 <= i172' && 1 <= i119 && 1 <= i150 && i119 < i150 && i150 - i119 = i172'
was transformed to
mod_LE_475(i150, i119, i92, i93, env, static) -{6,6}> mod_Load_470(i150 - i119, i119, i92, i93, env, static) :|: 2 <= i150 && 1 <= i172' && 1 <= i119 && 1 <= i150 && i119 < i150 && i150 - i119 = i172'

gcd_EQ_316(i92, i93, iconst_0, i94, env, static) -{0,0}> gcd_EQ_319(i92, i93, iconst_0, i94, env, static) :|: iconst_0 = 0
was transformed to
gcd_EQ_316(i92, i93, iconst_0, i94, env, static) -{0,0}> gcd_EQ_319(i92, i93, 0, i94, env, static) :|: iconst_0 = 0

(14) Obligation:

IntTrs with 17 rules
Start term: gcd_Load_2(#0, #1, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
mod_Load_470(i150, i119, i92, i93, env, static) -{2,2}> mod_LE_475(i150, i119, i92, i93, env, static) :|: 1 <= i150 && 1 <= i119
mod_LE_475(i150, i119, i92, i93, env, static) -{6,6}> mod_Load_470(i150 - i119, i119, i92, i93, env, static) :|: 2 <= i150 && 1 <= i172' && 1 <= i119 && 1 <= i150 && i119 < i150 && i150 - i119 = i172'
mod_NE_369(i113, i119, i92, i93, env, static) -{1,1}> mod_Load_470(i113, i119, i92, i93, env, static) :|: i113 < i119 && 1 <= i113 && 1 <= i119
gcd_EQ_316(i92, i93, iconst_0, i94, env, static) -{0,0}> gcd_EQ_319(i92, i93, 0, i94, env, static) :|: iconst_0 = 0
gcd_Load_463(i92, i93, i142, i143, env, static) -{3,3}> gcd_Load_314(i92, i93, i143, i142, env, static) :|: 0 >= 0
mod_LE_338(i113, i107, i92, i93, env, static) -{2,2}> mod_GT_350(i107, i113, i92, i93, env, static) :|: 1 <= i113 && 0 < i113
gcd_Load_2(i1, i4, env, static) -{15,15}> gcd_Load_314(i1, i4, i1, i4, env, static'1) :|: 0 >= 0 && static'1 <= static''' + 1 && 0 <= 2 && 0 <= static''' && static''' <= static + 2 && 0 < 1 && 0 <= 1 && 0 <= static && 0 <= static'1 && 0 < 2
gcd_Store_509(i92, i93, i160, i159, env, static) -{1,1}> gcd_Load_463(i92, i93, i160, i159, env, static) :|: 0 >= 0
mod_LE_338(i112, i107, i92, i93, env, static) -{4,4}> gcd_Load_463(i92, i93, 0, i107, env, static) :|: i112 <= 0
mod_GT_350(i118, i113, i92, i93, env, static) -{4,4}> gcd_Load_463(i92, i93, 0, i118, env, static) :|: 1 <= i113 && i118 <= -1 && i118 <= 0
gcd_Load_314(i92, i93, i94, i95, env, static) -{1,1}> gcd_EQ_316(i92, i93, i95, i94, env, static) :|: 0 >= 0
mod_LE_475(i150, i119, i92, i93, env, static) -{3,3}> gcd_Store_509(i92, i93, i150, i119, env, static) :|: 1 <= i119 && 1 <= i150 && i150 <= i119
mod_NE_369(i113, x, i92, i93, env, static) -{3,3}> gcd_Store_509(i92, i93, 0, i113, env, static) :|: 1 <= i113 && 0 >= 0 && x = i113
gcd_EQ_316(i92, i93, i107, i94, env, static) -{7,7}> mod_LE_338(i94, i107, i92, i93, env, static) :|: 0 >= 0 && i107 > 0
gcd_EQ_316(i92, i93, i107, i94, env, static) -{7,7}> mod_LE_338(i94, i107, i92, i93, env, static) :|: 0 >= 0 && i107 < 0
mod_GT_350(i119, i113, i92, i93, env, static) -{3,3}> mod_NE_369(i113, i119, i92, i93, env, static) :|: 1 <= i119 && 1 <= i113 && 0 < i119
mod_NE_369(i113, i119, i92, i93, env, static) -{1,1}> mod_Load_470(i113, i119, i92, i93, env, static) :|: i113 > i119 && 1 <= i113 && 1 <= i119

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

Simplified expressions.

gcd_Load_2(i1, i4, env, static) -{15,15}> gcd_Load_314(i1, i4, i1, i4, env, static'1) :|: 0 >= 0 && static'1 <= static''' + 1 && 0 <= 2 && 0 <= static''' && static''' <= static + 2 && 0 < 1 && 0 <= 1 && 0 <= static && 0 <= static'1 && 0 < 2
was transformed to
gcd_Load_2(i1, i4, env, static) -{15,15}> gcd_Load_314(i1, i4, i1, i4, env, static'1) :|: static'1 <= static''' + 1 && 0 <= static''' && static''' <= static + 2 && 0 <= static && 0 <= static'1

mod_NE_369(i113, x, i92, i93, env, static) -{3,3}> gcd_Store_509(i92, i93, 0, i113, env, static) :|: 1 <= i113 && 0 >= 0 && x = i113
was transformed to
mod_NE_369(i113, x, i92, i93, env, static) -{3,3}> gcd_Store_509(i92, i93, 0, i113, env, static) :|: 1 <= i113 && x = i113

mod_LE_475(i150, i119, i92, i93, env, static) -{6,6}> mod_Load_470(i150 - i119, i119, i92, i93, env, static) :|: 2 <= i150 && 1 <= i172' && 1 <= i119 && 1 <= i150 && i119 < i150 && i150 - i119 = i172'
was transformed to
mod_LE_475(i150, i119, i92, i93, env, static) -{6,6}> mod_Load_470(i150 + -1 * i119, i119, i92, i93, env, static) :|: 2 <= i150 && 1 <= i172' && 1 <= i119 && 1 <= i150 && i119 < i150 && i150 + -1 * i119 = i172'

gcd_EQ_316(i92, i93, i107, i94, env, static) -{7,7}> mod_LE_338(i94, i107, i92, i93, env, static) :|: 0 >= 0 && i107 < 0
was transformed to
gcd_EQ_316(i92, i93, i107, i94, env, static) -{7,7}> mod_LE_338(i94, i107, i92, i93, env, static) :|: i107 < 0

gcd_EQ_316(i92, i93, i107, i94, env, static) -{7,7}> mod_LE_338(i94, i107, i92, i93, env, static) :|: 0 >= 0 && i107 > 0
was transformed to
gcd_EQ_316(i92, i93, i107, i94, env, static) -{7,7}> mod_LE_338(i94, i107, i92, i93, env, static) :|: 0 < i107

mod_NE_369(i113, i119, i92, i93, env, static) -{1,1}> mod_Load_470(i113, i119, i92, i93, env, static) :|: i113 > i119 && 1 <= i113 && 1 <= i119
was transformed to
mod_NE_369(i113, i119, i92, i93, env, static) -{1,1}> mod_Load_470(i113, i119, i92, i93, env, static) :|: i119 < i113 && 1 <= i113 && 1 <= i119

(16) Obligation:

IntTrs with 17 rules
Start term: gcd_Load_2(#0, #1, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
gcd_Load_2(i1, i4, env, static) -{15,15}> gcd_Load_314(i1, i4, i1, i4, env, static'1) :|: static'1 <= static''' + 1 && 0 <= static''' && static''' <= static + 2 && 0 <= static && 0 <= static'1
gcd_EQ_316(i92, i93, i107, i94, env, static) -{7,7}> mod_LE_338(i94, i107, i92, i93, env, static) :|: i107 < 0
gcd_EQ_316(i92, i93, i107, i94, env, static) -{7,7}> mod_LE_338(i94, i107, i92, i93, env, static) :|: 0 < i107
mod_Load_470(i150, i119, i92, i93, env, static) -{2,2}> mod_LE_475(i150, i119, i92, i93, env, static) :|: 1 <= i150 && 1 <= i119
mod_NE_369(i113, i119, i92, i93, env, static) -{1,1}> mod_Load_470(i113, i119, i92, i93, env, static) :|: i113 < i119 && 1 <= i113 && 1 <= i119
mod_NE_369(i113, i119, i92, i93, env, static) -{1,1}> mod_Load_470(i113, i119, i92, i93, env, static) :|: i119 < i113 && 1 <= i113 && 1 <= i119
gcd_Load_463(i92, i93, i142, i143, env, static) -{3,3}> gcd_Load_314(i92, i93, i143, i142, env, static) :|: 0 >= 0
mod_LE_475(i150, i119, i92, i93, env, static) -{6,6}> mod_Load_470(i150 + -1 * i119, i119, i92, i93, env, static) :|: 2 <= i150 && 1 <= i172' && 1 <= i119 && 1 <= i150 && i119 < i150 && i150 + -1 * i119 = i172'
mod_LE_338(i113, i107, i92, i93, env, static) -{2,2}> mod_GT_350(i107, i113, i92, i93, env, static) :|: 1 <= i113 && 0 < i113
gcd_Store_509(i92, i93, i160, i159, env, static) -{1,1}> gcd_Load_463(i92, i93, i160, i159, env, static) :|: 0 >= 0
mod_LE_338(i112, i107, i92, i93, env, static) -{4,4}> gcd_Load_463(i92, i93, 0, i107, env, static) :|: i112 <= 0
mod_GT_350(i118, i113, i92, i93, env, static) -{4,4}> gcd_Load_463(i92, i93, 0, i118, env, static) :|: 1 <= i113 && i118 <= -1 && i118 <= 0
gcd_Load_314(i92, i93, i94, i95, env, static) -{1,1}> gcd_EQ_316(i92, i93, i95, i94, env, static) :|: 0 >= 0
gcd_EQ_316(i92, i93, iconst_0, i94, env, static) -{0,0}> gcd_EQ_319(i92, i93, 0, i94, env, static) :|: iconst_0 = 0
mod_NE_369(i113, x, i92, i93, env, static) -{3,3}> gcd_Store_509(i92, i93, 0, i113, env, static) :|: 1 <= i113 && x = i113
mod_LE_475(i150, i119, i92, i93, env, static) -{3,3}> gcd_Store_509(i92, i93, i150, i119, env, static) :|: 1 <= i119 && 1 <= i150 && i150 <= i119
mod_GT_350(i119, i113, i92, i93, env, static) -{3,3}> mod_NE_369(i113, i119, i92, i93, env, static) :|: 1 <= i119 && 1 <= i113 && 0 < i119

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

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

(18) Obligation:

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

(20) Obligation:

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

Linearized lhss.

(22) Obligation:

(23) RemoveDivModProof (CONCRETE UPPER BOUND(ID) transformation)

Removed div and mod.

(24) Obligation:

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

Moved arithmethic from constraints to rhss.

(26) Obligation:

IntTrs with 17 rules
Start term: gcd_Load_2(#0, #1, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
mod_Load_470(i150, i119, i92, i93, env, static) -{2,2}> mod_LE_475(i150, i119, i92, i93, env, static) :|: 1 <= i150 && 1 <= i119
mod_LE_475(i150, i119, i92, i93, env, static) -{6,6}> mod_Load_470(i150 - i119, i119, i92, i93, env, static) :|: 2 <= i150 && 1 <= i172' && 1 <= i119 && 1 <= i150 && i119 < i150 && i150 - i119 = i172'
mod_NE_369(i113, i119, i92, i93, env, static) -{1,1}> mod_Load_470(i113, i119, i92, i93, env, static) :|: i113 < i119 && 1 <= i113 && 1 <= i119
gcd_EQ_316(i92, i93, iconst_0, i94, env, static) -{0,0}> gcd_EQ_319(i92, i93, 0, i94, env, static) :|: iconst_0 = 0
gcd_Load_463(i92, i93, i142, i143, env, static) -{3,3}> gcd_Load_314(i92, i93, i143, i142, env, static) :|: 0 >= 0
mod_LE_338(i113, i107, i92, i93, env, static) -{2,2}> mod_GT_350(i107, i113, i92, i93, env, static) :|: 1 <= i113 && 0 < i113
gcd_Load_2(i1, i4, env, static) -{15,15}> gcd_Load_314(i1, i4, i1, i4, env, static'1) :|: 0 >= 0 && static'1 <= static''' + 1 && 0 <= 2 && 0 <= static''' && static''' <= static + 2 && 0 < 1 && 0 <= 1 && 0 <= static && 0 <= static'1 && 0 < 2
gcd_Store_509(i92, i93, i160, i159, env, static) -{1,1}> gcd_Load_463(i92, i93, i160, i159, env, static) :|: 0 >= 0
mod_LE_338(i112, i107, i92, i93, env, static) -{4,4}> gcd_Load_463(i92, i93, 0, i107, env, static) :|: i112 <= 0
mod_GT_350(i118, i113, i92, i93, env, static) -{4,4}> gcd_Load_463(i92, i93, 0, i118, env, static) :|: 1 <= i113 && i118 <= -1 && i118 <= 0
gcd_Load_314(i92, i93, i94, i95, env, static) -{1,1}> gcd_EQ_316(i92, i93, i95, i94, env, static) :|: 0 >= 0
mod_LE_475(i150, i119, i92, i93, env, static) -{3,3}> gcd_Store_509(i92, i93, i150, i119, env, static) :|: 1 <= i119 && 1 <= i150 && i150 <= i119
mod_NE_369(i113, x, i92, i93, env, static) -{3,3}> gcd_Store_509(i92, i93, 0, i113, env, static) :|: 1 <= i113 && 0 >= 0 && x = i113
gcd_EQ_316(i92, i93, i107, i94, env, static) -{7,7}> mod_LE_338(i94, i107, i92, i93, env, static) :|: 0 >= 0 && i107 > 0
gcd_EQ_316(i92, i93, i107, i94, env, static) -{7,7}> mod_LE_338(i94, i107, i92, i93, env, static) :|: 0 >= 0 && i107 < 0
mod_GT_350(i119, i113, i92, i93, env, static) -{3,3}> mod_NE_369(i113, i119, i92, i93, env, static) :|: 1 <= i119 && 1 <= i113 && 0 < i119
mod_NE_369(i113, i119, i92, i93, env, static) -{1,1}> mod_Load_470(i113, i119, i92, i93, env, static) :|: i113 > i119 && 1 <= i113 && 1 <= i119

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

Simplified expressions.

(28) Obligation:

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

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

(30) Obligation:

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

Used field analysis yielded the following read fields:

Considered paths: all paths from start

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

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

(32) Obligation:

IntTrs with 82 rules
Start term: gcd_Load_2(#0, #1, env, static)
Considered paths: all paths from start
Rules:
gcd_Load_2(i1, i4, env, static) -{0,0}> gcd_Load_4(i1, i4, env, static) :|: 0 >= 0
gcd_Load_4(i1, i4, env, static) -{0,0}> langle_clinit_rangle_ConstantStackPush_6(i1, i4, env, static) :|: 0 >= 0
langle_clinit_rangle_ConstantStackPush_6(i1, i4, env, static) -{1,1}> langle_clinit_rangle_ArrayCreate_12(iconst_0, i1, i4, env, static) :|: iconst_0 = 0
langle_clinit_rangle_ArrayCreate_12(iconst_0, i1, i4, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_14(a2, i1, i4, iconst_0, env, static) :|: a2 = 2 && iconst_0 = 0 && 0 < a2
langle_clinit_rangle_FieldAccess_14(a2, i1, i4, iconst_0, env, static) -{1,1}> langle_clinit_rangle_New_16(i1, i4, env, static') :|: 0 <= a2 && iconst_0 = 0 && static' <= static + a2 && 0 <= static && 0 < a2
langle_clinit_rangle_New_16(i1, i4, env, static) -{0,0}> langle_clinit_rangle_New_17(i1, i4, env, static) :|: 0 >= 0
langle_clinit_rangle_New_17(i1, i4, env, static) -{0,0}> langle_clinit_rangle_New_19(i1, i4, env, static) :|: 0 <= static
langle_clinit_rangle_New_19(i1, i4, env, static) -{1,1}> langle_clinit_rangle_Duplicate_20(o2, i1, i4, env, static) :|: 0 < o2 && o2 = 1
langle_clinit_rangle_Duplicate_20(o2, i1, i4, env, static) -{1,1}> langle_clinit_rangle_ConstantStackPush_22(o2, i1, i4, env, static) :|: 0 < o2
langle_clinit_rangle_ConstantStackPush_22(o2, i1, i4, env, static) -{1,1}> langle_clinit_rangle_InvokeMethod_23(o2, NULL, i1, i4, env, static) :|: NULL = 0 && 0 < o2
langle_clinit_rangle_InvokeMethod_23(o2, NULL, i1, i4, env, static) -{1,1}> langle_init_rangle_Load_24(o2, i1, i4, env, static) :|: NULL = 0 && 0 < o2
langle_init_rangle_Load_24(o2, i1, i4, env, static) -{1,1}> langle_init_rangle_InvokeMethod_25(o2, i1, i4, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_25(o2, i1, i4, env, static) -{1,1}> langle_init_rangle_Load_26(o2, i1, i4, env, static) :|: 0 < o2
langle_init_rangle_Load_26(o2, i1, i4, env, static) -{1,1}> langle_init_rangle_InvokeMethod_28(o2, i1, i4, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_28(o2, i1, i4, env, static) -{1,1}> langle_init_rangle_Return_31(o2, i1, i4, env, static) :|: 0 < o2
langle_init_rangle_Return_31(o2, i1, i4, env, static) -{1,1}> langle_init_rangle_Return_33(o2, i1, i4, env, static) :|: 0 < o2
langle_init_rangle_Return_33(o2, i1, i4, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_35(o2, i1, i4, env, static) :|: 0 < o2
langle_clinit_rangle_FieldAccess_35(o2, i1, i4, env, static) -{1,1}> langle_clinit_rangle_Return_38(i1, i4, env, static') :|: 0 < o2 && 0 <= o2 && 0 <= static && static' <= static + o2
langle_clinit_rangle_Return_38(i1, i4, env, static) -{1,1}> gcd_Load_41(i1, i4, env, static) :|: 0 >= 0
gcd_Load_41(i1, i4, env, static) -{0,0}> gcd_Load_42(i1, i4, env, static) :|: 0 >= 0
gcd_Load_42(i1, i4, env, static) -{0,0}> gcd_Load_49(i1, i4, env, static) :|: 0 <= static
gcd_Load_49(i1, i4, env, static) -{0,0}> gcd_Load_50(i1, i4, env, static) :|: 0 >= 0
gcd_Load_50(i1, i4, env, static) -{0,0}> gcd_Load_51(i1, i4, env, static) :|: 0 >= 0
gcd_Load_51(i1, i4, env, static) -{0,0}> gcd_Load_314(i1, i4, i1, i4, env, static) :|: 0 >= 0
gcd_Load_314(i92, i93, i94, i95, env, static) -{1,1}> gcd_EQ_316(i92, i93, i95, i94, env, static) :|: 0 >= 0
gcd_EQ_316(i92, i93, i107, i94, env, static) -{0,0}> gcd_EQ_318(i92, i93, i107, i94, env, static) :|: 0 >= 0
gcd_EQ_318(i92, i93, i107, i94, env, static) -{1,1}> gcd_Load_320(i92, i93, i94, i107, env, static) :|: !(i107 = 0)
gcd_Load_320(i92, i93, i94, i107, env, static) -{1,1}> gcd_Store_322(i92, i93, i107, i94, env, static) :|: 0 >= 0
gcd_Store_322(i92, i93, i107, i94, env, static) -{1,1}> gcd_Load_326(i92, i93, i94, i107, env, static) :|: 0 >= 0
gcd_Load_326(i92, i93, i94, i107, env, static) -{1,1}> gcd_Load_330(i92, i93, i94, i107, env, static) :|: 0 >= 0
gcd_Load_330(i92, i93, i94, i107, env, static) -{1,1}> gcd_InvokeMethod_332(i92, i93, i94, i107, env, static) :|: 0 >= 0
gcd_InvokeMethod_332(i92, i93, i94, i107, env, static) -{1,1}> mod_Load_334(i94, i107, i92, i93, env, static) :|: 0 >= 0
mod_Load_334(i94, i107, i92, i93, env, static) -{1,1}> mod_LE_338(i94, i107, i92, i93, env, static) :|: 0 >= 0
mod_LE_338(i112, i107, i92, i93, env, static) -{0,0}> mod_LE_340(i112, i107, i92, i93, env, static) :|: i112 <= 0
mod_LE_338(i113, i107, i92, i93, env, static) -{0,0}> mod_LE_341(i113, i107, i92, i93, env, static) :|: 1 <= i113
mod_LE_340(i112, i107, i92, i93, env, static) -{1,1}> mod_ConstantStackPush_343(i92, i93, i107, env, static) :|: i112 <= 0
mod_LE_341(i113, i107, i92, i93, env, static) -{1,1}> mod_Load_346(i113, i107, i92, i93, env, static) :|: 1 <= i113 && 0 < i113
mod_ConstantStackPush_343(i92, i93, i107, env, static) -{1,1}> mod_Return_348(iconst_0, i92, i93, i107, env, static) :|: iconst_0 = 0
mod_Load_346(i113, i107, i92, i93, env, static) -{1,1}> mod_GT_350(i107, i113, i92, i93, env, static) :|: 1 <= i113
mod_Return_348(iconst_0, i92, i93, i107, env, static) -{1,1}> gcd_Store_351(i92, i93, iconst_0, i107, env, static) :|: iconst_0 = 0
mod_GT_350(i118, i113, i92, i93, env, static) -{0,0}> mod_GT_352(i118, i113, i92, i93, env, static) :|: 1 <= i113 && i118 <= -1
mod_GT_350(i119, i113, i92, i93, env, static) -{0,0}> mod_GT_353(i119, i113, i92, i93, env, static) :|: 1 <= i113 && 1 <= i119
gcd_Store_351(i92, i93, iconst_0, i107, env, static) -{1,1}> gcd_Load_354(i92, i93, iconst_0, i107, env, static) :|: iconst_0 = 0
mod_GT_352(i118, i113, i92, i93, env, static) -{1,1}> mod_ConstantStackPush_355(i92, i93, i118, env, static) :|: 1 <= i113 && i118 <= -1 && i118 <= 0
mod_GT_353(i119, i113, i92, i93, env, static) -{1,1}> mod_Load_356(i113, i119, i92, i93, env, static) :|: 1 <= i113 && 1 <= i119 && 0 < i119
gcd_Load_354(i92, i93, iconst_0, i107, env, static) -{0,0}> gcd_Load_463(i92, i93, iconst_0, i107, env, static) :|: iconst_0 = 0
mod_ConstantStackPush_355(i92, i93, i118, env, static) -{1,1}> mod_Return_358(iconst_0, i92, i93, i118, env, static) :|: i118 <= -1 && iconst_0 = 0
mod_Load_356(i113, i119, i92, i93, env, static) -{1,1}> mod_Load_361(i113, i119, i92, i93, env, static) :|: 1 <= i113 && 1 <= i119
mod_Return_358(iconst_0, i92, i93, i118, env, static) -{1,1}> gcd_Store_363(i92, i93, iconst_0, i118, env, static) :|: i118 <= -1 && iconst_0 = 0
mod_Load_361(i113, i119, i92, i93, env, static) -{1,1}> mod_NE_369(i113, i119, i92, i93, env, static) :|: 1 <= i113 && 1 <= i119
gcd_Store_363(i92, i93, iconst_0, i118, env, static) -{1,1}> gcd_Load_372(i92, i93, iconst_0, i118, env, static) :|: i118 <= -1 && iconst_0 = 0
mod_NE_369(i113, i119, i92, i93, env, static) -{0,0}> mod_NE_374(i113, i119, i92, i93, env, static) :|: 1 <= i113 && !(i113 = i119) && 1 <= i119
mod_NE_369(i113, i119, i92, i93, env, static) -{0,0}> mod_NE_376(i119, i92, i93, env, static) :|: 1 <= i113 && i113 = i119 && 1 <= i119
gcd_Load_372(i92, i93, iconst_0, i118, env, static) -{0,0}> gcd_Load_463(i92, i93, iconst_0, i118, env, static) :|: i118 <= -1 && iconst_0 = 0
mod_NE_374(i113, i119, i92, i93, env, static) -{1,1}> mod_Load_382(i113, i119, i92, i93, env, static) :|: 1 <= i113 && !(i113 = i119) && 1 <= i119
mod_NE_376(i119, i92, i93, env, static) -{1,1}> mod_ConstantStackPush_385(i92, i93, i119, env, static) :|: i119 = i119 && 1 <= i119
mod_Load_382(i113, i119, i92, i93, env, static) -{0,0}> mod_Load_470(i113, i119, i92, i93, env, static) :|: 1 <= i113 && 1 <= i119
mod_ConstantStackPush_385(i92, i93, i119, env, static) -{1,1}> mod_Return_390(iconst_0, i92, i93, i119, env, static) :|: 1 <= i119 && iconst_0 = 0
mod_Return_390(iconst_0, i92, i93, i119, env, static) -{1,1}> gcd_Store_405(i92, i93, iconst_0, i119, env, static) :|: 1 <= i119 && iconst_0 = 0
gcd_Store_405(i92, i93, iconst_0, i119, env, static) -{0,0}> gcd_Store_445(i92, i93, iconst_0, i119, env, static) :|: 1 <= i119 && iconst_0 = 0
gcd_Store_445(i92, i93, i130, i129, env, static) -{0,0}> gcd_Store_509(i92, i93, i130, i129, env, static) :|: 0 >= 0
gcd_Load_463(i92, i93, i142, i143, env, static) -{1,1}> gcd_Store_467(i92, i93, i143, i142, env, static) :|: 0 >= 0
gcd_Store_467(i92, i93, i143, i142, env, static) -{1,1}> gcd_JMP_469(i92, i93, i143, i142, env, static) :|: 0 >= 0
gcd_JMP_469(i92, i93, i143, i142, env, static) -{1,1}> gcd_Load_471(i92, i93, i143, i142, env, static) :|: 0 >= 0
mod_Load_470(i150, i119, i92, i93, env, static) -{1,1}> mod_Load_474(i150, i119, i92, i93, env, static) :|: 1 <= i150 && 1 <= i119
gcd_Load_471(i92, i93, i143, i142, env, static) -{0,0}> gcd_Load_314(i92, i93, i143, i142, env, static) :|: 0 >= 0
mod_Load_474(i150, i119, i92, i93, env, static) -{1,1}> mod_LE_475(i150, i119, i92, i93, env, static) :|: 1 <= i150 && 1 <= i119
mod_LE_475(i150, i119, i92, i93, env, static) -{0,0}> mod_LE_476(i150, i119, i92, i93, env, static) :|: 1 <= i150 && 1 <= i119 && i150 <= i119
mod_LE_475(i150, i119, i92, i93, env, static) -{0,0}> mod_LE_477(i150, i119, i92, i93, env, static) :|: 1 <= i150 && 1 <= i119 && i119 < i150
mod_LE_476(i150, i119, i92, i93, env, static) -{1,1}> mod_Load_481(i150, i92, i93, i119, env, static) :|: 1 <= i150 && 1 <= i119 && i150 <= i119
mod_LE_477(i150, i119, i92, i93, env, static) -{1,1}> mod_Load_485(i150, i119, i92, i93, env, static) :|: 1 <= i150 && 2 <= i150 && 1 <= i119 && i119 < i150
mod_Load_481(i150, i92, i93, i119, env, static) -{1,1}> mod_Return_486(i150, i92, i93, i119, env, static) :|: 1 <= i150 && 1 <= i119
mod_Load_485(i150, i119, i92, i93, env, static) -{1,1}> mod_Load_487(i150, i119, i92, i93, env, static) :|: 2 <= i150 && 1 <= i119
mod_Return_486(i150, i92, i93, i119, env, static) -{1,1}> gcd_Store_508(i92, i93, i150, i119, env, static) :|: 1 <= i150 && 1 <= i119
mod_Load_487(i150, i119, i92, i93, env, static) -{1,1}> mod_IntArithmetic_510(i150, i119, i92, i93, env, static) :|: 2 <= i150 && 1 <= i119
gcd_Store_508(i92, i93, i150, i119, env, static) -{0,0}> gcd_Store_509(i92, i93, i150, i119, env, static) :|: 1 <= i150 && 1 <= i119
gcd_Store_509(i92, i93, i160, i159, env, static) -{1,1}> gcd_Load_516(i92, i93, i160, i159, env, static) :|: 0 >= 0
mod_IntArithmetic_510(i150, i119, i92, i93, env, static) -{1,1}> mod_Store_521(i172, i119, i92, i93, env, static) :|: 1 <= i172 && 2 <= i150 && 1 <= i119 && i150 - i119 = i172
gcd_Load_516(i92, i93, i160, i159, env, static) -{0,0}> gcd_Load_463(i92, i93, i160, i159, env, static) :|: 0 >= 0
mod_Store_521(i172, i119, i92, i93, env, static) -{1,1}> mod_JMP_530(i172, i119, i92, i93, env, static) :|: 1 <= i172 && 1 <= i119
mod_JMP_530(i172, i119, i92, i93, env, static) -{1,1}> mod_Load_539(i172, i119, i92, i93, env, static) :|: 1 <= i172 && 1 <= i119
mod_Load_539(i172, i119, i92, i93, env, static) -{0,0}> mod_Load_470(i172, i119, i92, i93, env, static) :|: 1 <= i172 && 1 <= i119

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

obtained
gcd_Load_314(i92, i93, i94, i95, env, static) -{8,8}> mod_LE_338(i94, i95, i92, i93, env, static) :|: 0 >= 0 && !(i95 = 0)
by chaining
gcd_Load_314(i92, i93, i94, i95, env, static) -{1,1}> gcd_EQ_316(i92, i93, i95, i94, env, static) :|: 0 >= 0
gcd_EQ_316(i92, i93, i107, i94, env, static) -{0,0}> gcd_EQ_318(i92, i93, i107, i94, env, static) :|: 0 >= 0
gcd_EQ_318(i92, i93, i107, i94, env, static) -{1,1}> gcd_Load_320(i92, i93, i94, i107, env, static) :|: !(i107 = 0)
gcd_Load_320(i92, i93, i94, i107, env, static) -{1,1}> gcd_Store_322(i92, i93, i107, i94, env, static) :|: 0 >= 0
gcd_Store_322(i92, i93, i107, i94, env, static) -{1,1}> gcd_Load_326(i92, i93, i94, i107, env, static) :|: 0 >= 0
gcd_Load_326(i92, i93, i94, i107, env, static) -{1,1}> gcd_Load_330(i92, i93, i94, i107, env, static) :|: 0 >= 0
gcd_Load_330(i92, i93, i94, i107, env, static) -{1,1}> gcd_InvokeMethod_332(i92, i93, i94, i107, env, static) :|: 0 >= 0
gcd_InvokeMethod_332(i92, i93, i94, i107, env, static) -{1,1}> mod_Load_334(i94, i107, i92, i93, env, static) :|: 0 >= 0
mod_Load_334(i94, i107, i92, i93, env, static) -{1,1}> mod_LE_338(i94, i107, i92, i93, env, static) :|: 0 >= 0

(34) Obligation:

IntTrs with 13 rules
Start term: gcd_Load_2(#0, #1, env, static)
Considered paths: all paths from start
Rules:
gcd_Load_2(i1, i4, env, static) -{15,15}> gcd_Load_314(i1, i4, i1, i4, env, static'1) :|: 0 >= 0 && static'1 <= static''' + 1 && 0 <= 2 && 0 <= static''' && static''' <= static + 2 && 0 < 1 && 0 <= 1 && 0 <= static && 0 <= static'1 && 0 < 2
gcd_Load_314(i92, i93, i94, i95, env, static) -{8,8}> mod_LE_338(i94, i95, i92, i93, env, static) :|: 0 >= 0 && !(i95 = 0)
mod_LE_338(i113, i107, i92, i93, env, static) -{2,2}> mod_GT_350(i107, i113, i92, i93, env, static) :|: 1 <= i113 && 0 < i113
mod_GT_350(i119, i113, i92, i93, env, static) -{3,3}> mod_NE_369(i113, i119, i92, i93, env, static) :|: 1 <= i119 && 1 <= i113 && 0 < i119
mod_NE_369(i113, i113, i92, i93, env, static) -{3,3}> gcd_Store_509(i92, i93, 0, i113, env, static) :|: 1 <= i113 && 0 >= 0
gcd_Store_509(i92, i93, i160, i159, env, static) -{1,1}> gcd_Load_463(i92, i93, i160, i159, env, static) :|: 0 >= 0
gcd_Load_463(i92, i93, i142, i143, env, static) -{3,3}> gcd_Load_314(i92, i93, i143, i142, env, static) :|: 0 >= 0
mod_NE_369(i113, i119, i92, i93, env, static) -{1,1}> mod_Load_470(i113, i119, i92, i93, env, static) :|: !(i113 = i119) && 1 <= i113 && 1 <= i119
mod_Load_470(i150, i119, i92, i93, env, static) -{2,2}> mod_LE_475(i150, i119, i92, i93, env, static) :|: 1 <= i150 && 1 <= i119
mod_LE_475(i150, i119, i92, i93, env, static) -{6,6}> mod_Load_470(i172', i119, i92, i93, env, static) :|: 2 <= i150 && 1 <= i172' && 1 <= i119 && 1 <= i150 && i119 < i150 && i150 - i119 = i172'
mod_LE_475(i150, i119, i92, i93, env, static) -{3,3}> gcd_Store_509(i92, i93, i150, i119, env, static) :|: 1 <= i119 && 1 <= i150 && i150 <= i119
mod_GT_350(i118, i113, i92, i93, env, static) -{4,4}> gcd_Load_463(i92, i93, 0, i118, env, static) :|: 1 <= i113 && i118 <= -1 && i118 <= 0
mod_LE_338(i112, i107, i92, i93, env, static) -{4,4}> gcd_Load_463(i92, i93, 0, i107, env, static) :|: i112 <= 0

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

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

gcd_Load_2(x1, x2, x3, x4) → gcd_Load_2(x1, x2, x4)
gcd_Load_314(x1, x2, x3, x4, x5, x6) → gcd_Load_314(x3, x4)
mod_LE_338(x1, x2, x3, x4, x5, x6) → mod_LE_338(x1, x2)
mod_GT_350(x1, x2, x3, x4, x5, x6) → mod_GT_350(x1, x2)
mod_NE_369(x1, x2, x3, x4, x5, x6) → mod_NE_369(x1, x2)
gcd_Load_463(x1, x2, x3, x4, x5, x6) → gcd_Load_463(x3, x4)
mod_Load_470(x1, x2, x3, x4, x5, x6) → mod_Load_470(x1, x2)
mod_LE_475(x1, x2, x3, x4, x5, x6) → mod_LE_475(x1, x2)
gcd_Store_509(x1, x2, x3, x4, x5, x6) → gcd_Store_509(x3, x4)

(36) Obligation:

IntTrs with 13 rules
Start term: gcd_Load_2(#0, #1, static)
Considered paths: all paths from start
Rules:
gcd_Load_2(i1, i4, static) -{15,15}> gcd_Load_314(i1, i4) :|: 0 >= 0 && static'1 <= static''' + 1 && 0 <= 2 && 0 <= static''' && static''' <= static + 2 && 0 < 1 && 0 <= 1 && 0 <= static && 0 <= static'1 && 0 < 2
gcd_Load_314(i94, i95) -{8,8}> mod_LE_338(i94, i95) :|: 0 >= 0 && !(i95 = 0)
mod_LE_338(i113, i107) -{2,2}> mod_GT_350(i107, i113) :|: 1 <= i113 && 0 < i113
mod_GT_350(i119, i113) -{3,3}> mod_NE_369(i113, i119) :|: 1 <= i119 && 1 <= i113 && 0 < i119
mod_NE_369(i113, i113) -{3,3}> gcd_Store_509(0, i113) :|: 1 <= i113 && 0 >= 0
gcd_Store_509(i160, i159) -{1,1}> gcd_Load_463(i160, i159) :|: 0 >= 0
gcd_Load_463(i142, i143) -{3,3}> gcd_Load_314(i143, i142) :|: 0 >= 0
mod_NE_369(i113, i119) -{1,1}> mod_Load_470(i113, i119) :|: !(i113 = i119) && 1 <= i113 && 1 <= i119
mod_Load_470(i150, i119) -{2,2}> mod_LE_475(i150, i119) :|: 1 <= i150 && 1 <= i119
mod_LE_475(i150, i119) -{6,6}> mod_Load_470(i172', i119) :|: 2 <= i150 && 1 <= i172' && 1 <= i119 && 1 <= i150 && i119 < i150 && i150 - i119 = i172'
mod_LE_475(i150, i119) -{3,3}> gcd_Store_509(i150, i119) :|: 1 <= i119 && 1 <= i150 && i150 <= i119
mod_GT_350(i118, i113) -{4,4}> gcd_Load_463(0, i118) :|: 1 <= i113 && i118 <= -1 && i118 <= 0
mod_LE_338(i112, i107) -{4,4}> gcd_Load_463(0, i107) :|: i112 <= 0

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

Linearized lhss.

mod_NE_369(i113, i113) -{3,3}> gcd_Store_509(0, i113) :|: 1 <= i113 && 0 >= 0
was transformed to
mod_NE_369(i113, x) -{3,3}> gcd_Store_509(0, i113) :|: 1 <= i113 && 0 >= 0 && x = i113

(38) Obligation:

IntTrs with 13 rules
Start term: gcd_Load_2(#0, #1, static)
Considered paths: all paths from start
Rules:
mod_Load_470(i150, i119) -{2,2}> mod_LE_475(i150, i119) :|: 1 <= i150 && 1 <= i119
gcd_Load_2(i1, i4, static) -{15,15}> gcd_Load_314(i1, i4) :|: 0 >= 0 && static'1 <= static''' + 1 && 0 <= 2 && 0 <= static''' && static''' <= static + 2 && 0 < 1 && 0 <= 1 && 0 <= static && 0 <= static'1 && 0 < 2
mod_LE_475(i150, i119) -{3,3}> gcd_Store_509(i150, i119) :|: 1 <= i119 && 1 <= i150 && i150 <= i119
mod_GT_350(i119, i113) -{3,3}> mod_NE_369(i113, i119) :|: 1 <= i119 && 1 <= i113 && 0 < i119
gcd_Load_314(i94, i95) -{8,8}> mod_LE_338(i94, i95) :|: 0 >= 0 && !(i95 = 0)
gcd_Store_509(i160, i159) -{1,1}> gcd_Load_463(i160, i159) :|: 0 >= 0
mod_NE_369(i113, i119) -{1,1}> mod_Load_470(i113, i119) :|: !(i113 = i119) && 1 <= i113 && 1 <= i119
mod_LE_338(i113, i107) -{2,2}> mod_GT_350(i107, i113) :|: 1 <= i113 && 0 < i113
mod_GT_350(i118, i113) -{4,4}> gcd_Load_463(0, i118) :|: 1 <= i113 && i118 <= -1 && i118 <= 0
gcd_Load_463(i142, i143) -{3,3}> gcd_Load_314(i143, i142) :|: 0 >= 0
mod_NE_369(i113, x) -{3,3}> gcd_Store_509(0, i113) :|: 1 <= i113 && 0 >= 0 && x = i113
mod_LE_338(i112, i107) -{4,4}> gcd_Load_463(0, i107) :|: i112 <= 0
mod_LE_475(i150, i119) -{6,6}> mod_Load_470(i172', i119) :|: 2 <= i150 && 1 <= i172' && 1 <= i119 && 1 <= i150 && i119 < i150 && i150 - i119 = i172'

(39) RemoveDivModProof (CONCRETE UPPER BOUND(ID) transformation)

Removed div and mod.

gcd_Load_314(i94, i95) -{8,8}> mod_LE_338(i94, i95) :|: 0 >= 0 && !(i95 = 0)
was transformed to
gcd_Load_314(i94, i95) -{8,8}> mod_LE_338(i94, i95) :|: 0 >= 0 && i95 < 0
gcd_Load_314(i94, i95) -{8,8}> mod_LE_338(i94, i95) :|: 0 >= 0 && i95 > 0

mod_NE_369(i113, i119) -{1,1}> mod_Load_470(i113, i119) :|: !(i113 = i119) && 1 <= i113 && 1 <= i119
was transformed to
mod_NE_369(i113, i119) -{1,1}> mod_Load_470(i113, i119) :|: i113 > i119 && 1 <= i113 && 1 <= i119
mod_NE_369(i113, i119) -{1,1}> mod_Load_470(i113, i119) :|: i113 < i119 && 1 <= i113 && 1 <= i119

(40) Obligation:

IntTrs with 15 rules
Start term: gcd_Load_2(#0, #1, static)
Considered paths: all paths from start
Rules:
gcd_Load_2(i1, i4, static) -{15,15}> gcd_Load_314(i1, i4) :|: 0 >= 0 && static'1 <= static''' + 1 && 0 <= 2 && 0 <= static''' && static''' <= static + 2 && 0 < 1 && 0 <= 1 && 0 <= static && 0 <= static'1 && 0 < 2
mod_LE_475(i150, i119) -{3,3}> gcd_Store_509(i150, i119) :|: 1 <= i119 && 1 <= i150 && i150 <= i119
gcd_Store_509(i160, i159) -{1,1}> gcd_Load_463(i160, i159) :|: 0 >= 0
mod_LE_338(i113, i107) -{2,2}> mod_GT_350(i107, i113) :|: 1 <= i113 && 0 < i113
mod_NE_369(i113, i119) -{1,1}> mod_Load_470(i113, i119) :|: i113 > i119 && 1 <= i113 && 1 <= i119
gcd_Load_314(i94, i95) -{8,8}> mod_LE_338(i94, i95) :|: 0 >= 0 && i95 > 0
mod_NE_369(i113, i119) -{1,1}> mod_Load_470(i113, i119) :|: i113 < i119 && 1 <= i113 && 1 <= i119
mod_LE_475(i150, i119) -{6,6}> mod_Load_470(i172', i119) :|: 2 <= i150 && 1 <= i172' && 1 <= i119 && 1 <= i150 && i119 < i150 && i150 - i119 = i172'
mod_NE_369(i113, x) -{3,3}> gcd_Store_509(0, i113) :|: 1 <= i113 && 0 >= 0 && x = i113
mod_Load_470(i150, i119) -{2,2}> mod_LE_475(i150, i119) :|: 1 <= i150 && 1 <= i119
mod_GT_350(i119, i113) -{3,3}> mod_NE_369(i113, i119) :|: 1 <= i119 && 1 <= i113 && 0 < i119
gcd_Load_314(i94, i95) -{8,8}> mod_LE_338(i94, i95) :|: 0 >= 0 && i95 < 0
mod_GT_350(i118, i113) -{4,4}> gcd_Load_463(0, i118) :|: 1 <= i113 && i118 <= -1 && i118 <= 0
gcd_Load_463(i142, i143) -{3,3}> gcd_Load_314(i143, i142) :|: 0 >= 0
mod_LE_338(i112, i107) -{4,4}> gcd_Load_463(0, i107) :|: i112 <= 0

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

Moved arithmethic from constraints to rhss.

mod_LE_475(i150, i119) -{6,6}> mod_Load_470(i172', i119) :|: 2 <= i150 && 1 <= i172' && 1 <= i119 && 1 <= i150 && i119 < i150 && i150 - i119 = i172'
was transformed to
mod_LE_475(i150, i119) -{6,6}> mod_Load_470(i150 - i119, i119) :|: 2 <= i150 && 1 <= i172' && 1 <= i119 && 1 <= i150 && i119 < i150 && i150 - i119 = i172'

(42) Obligation:

IntTrs with 15 rules
Start term: gcd_Load_2(#0, #1, static)
Considered paths: all paths from start
Rules:
gcd_Load_2(i1, i4, static) -{15,15}> gcd_Load_314(i1, i4) :|: 0 >= 0 && static'1 <= static''' + 1 && 0 <= 2 && 0 <= static''' && static''' <= static + 2 && 0 < 1 && 0 <= 1 && 0 <= static && 0 <= static'1 && 0 < 2
mod_LE_475(i150, i119) -{3,3}> gcd_Store_509(i150, i119) :|: 1 <= i119 && 1 <= i150 && i150 <= i119
gcd_Store_509(i160, i159) -{1,1}> gcd_Load_463(i160, i159) :|: 0 >= 0
mod_LE_338(i113, i107) -{2,2}> mod_GT_350(i107, i113) :|: 1 <= i113 && 0 < i113
mod_NE_369(i113, i119) -{1,1}> mod_Load_470(i113, i119) :|: i113 > i119 && 1 <= i113 && 1 <= i119
gcd_Load_314(i94, i95) -{8,8}> mod_LE_338(i94, i95) :|: 0 >= 0 && i95 > 0
mod_NE_369(i113, i119) -{1,1}> mod_Load_470(i113, i119) :|: i113 < i119 && 1 <= i113 && 1 <= i119
mod_NE_369(i113, x) -{3,3}> gcd_Store_509(0, i113) :|: 1 <= i113 && 0 >= 0 && x = i113
mod_LE_475(i150, i119) -{6,6}> mod_Load_470(i150 - i119, i119) :|: 2 <= i150 && 1 <= i172' && 1 <= i119 && 1 <= i150 && i119 < i150 && i150 - i119 = i172'
mod_Load_470(i150, i119) -{2,2}> mod_LE_475(i150, i119) :|: 1 <= i150 && 1 <= i119
mod_GT_350(i119, i113) -{3,3}> mod_NE_369(i113, i119) :|: 1 <= i119 && 1 <= i113 && 0 < i119
gcd_Load_314(i94, i95) -{8,8}> mod_LE_338(i94, i95) :|: 0 >= 0 && i95 < 0
mod_GT_350(i118, i113) -{4,4}> gcd_Load_463(0, i118) :|: 1 <= i113 && i118 <= -1 && i118 <= 0
gcd_Load_463(i142, i143) -{3,3}> gcd_Load_314(i143, i142) :|: 0 >= 0
mod_LE_338(i112, i107) -{4,4}> gcd_Load_463(0, i107) :|: i112 <= 0

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

Simplified expressions.

gcd_Load_2(i1, i4, static) -{15,15}> gcd_Load_314(i1, i4) :|: 0 >= 0 && static'1 <= static''' + 1 && 0 <= 2 && 0 <= static''' && static''' <= static + 2 && 0 < 1 && 0 <= 1 && 0 <= static && 0 <= static'1 && 0 < 2
was transformed to
gcd_Load_2(i1, i4, static) -{15,15}> gcd_Load_314(i1, i4) :|: static'1 <= static''' + 1 && 0 <= static''' && static''' <= static + 2 && 0 <= static && 0 <= static'1

mod_LE_475(i150, i119) -{6,6}> mod_Load_470(i150 - i119, i119) :|: 2 <= i150 && 1 <= i172' && 1 <= i119 && 1 <= i150 && i119 < i150 && i150 - i119 = i172'
was transformed to
mod_LE_475(i150, i119) -{6,6}> mod_Load_470(i150 + -1 * i119, i119) :|: 2 <= i150 && 1 <= i172' && 1 <= i119 && 1 <= i150 && i119 < i150 && i150 + -1 * i119 = i172'

mod_NE_369(i113, i119) -{1,1}> mod_Load_470(i113, i119) :|: i113 > i119 && 1 <= i113 && 1 <= i119
was transformed to
mod_NE_369(i113, i119) -{1,1}> mod_Load_470(i113, i119) :|: i119 < i113 && 1 <= i113 && 1 <= i119

gcd_Load_314(i94, i95) -{8,8}> mod_LE_338(i94, i95) :|: 0 >= 0 && i95 > 0
was transformed to
gcd_Load_314(i94, i95) -{8,8}> mod_LE_338(i94, i95) :|: 0 < i95

mod_NE_369(i113, x) -{3,3}> gcd_Store_509(0, i113) :|: 1 <= i113 && 0 >= 0 && x = i113
was transformed to
mod_NE_369(i113, x) -{3,3}> gcd_Store_509(0, i113) :|: 1 <= i113 && x = i113

gcd_Load_314(i94, i95) -{8,8}> mod_LE_338(i94, i95) :|: 0 >= 0 && i95 < 0
was transformed to
gcd_Load_314(i94, i95) -{8,8}> mod_LE_338(i94, i95) :|: i95 < 0

(44) Obligation:

IntTrs with 15 rules
Start term: gcd_Load_2(#0, #1, static)
Considered paths: all paths from start
Rules:
mod_LE_475(i150, i119) -{3,3}> gcd_Store_509(i150, i119) :|: 1 <= i119 && 1 <= i150 && i150 <= i119
gcd_Store_509(i160, i159) -{1,1}> gcd_Load_463(i160, i159) :|: 0 >= 0
mod_LE_338(i113, i107) -{2,2}> mod_GT_350(i107, i113) :|: 1 <= i113 && 0 < i113
mod_NE_369(i113, i119) -{1,1}> mod_Load_470(i113, i119) :|: i119 < i113 && 1 <= i113 && 1 <= i119
mod_NE_369(i113, i119) -{1,1}> mod_Load_470(i113, i119) :|: i113 < i119 && 1 <= i113 && 1 <= i119
mod_Load_470(i150, i119) -{2,2}> mod_LE_475(i150, i119) :|: 1 <= i150 && 1 <= i119
mod_GT_350(i119, i113) -{3,3}> mod_NE_369(i113, i119) :|: 1 <= i119 && 1 <= i113 && 0 < i119
gcd_Load_2(i1, i4, static) -{15,15}> gcd_Load_314(i1, i4) :|: static'1 <= static''' + 1 && 0 <= static''' && static''' <= static + 2 && 0 <= static && 0 <= static'1
mod_LE_475(i150, i119) -{6,6}> mod_Load_470(i150 + -1 * i119, i119) :|: 2 <= i150 && 1 <= i172' && 1 <= i119 && 1 <= i150 && i119 < i150 && i150 + -1 * i119 = i172'
gcd_Load_314(i94, i95) -{8,8}> mod_LE_338(i94, i95) :|: 0 < i95
gcd_Load_314(i94, i95) -{8,8}> mod_LE_338(i94, i95) :|: i95 < 0
mod_NE_369(i113, x) -{3,3}> gcd_Store_509(0, i113) :|: 1 <= i113 && x = i113
mod_GT_350(i118, i113) -{4,4}> gcd_Load_463(0, i118) :|: 1 <= i113 && i118 <= -1 && i118 <= 0
gcd_Load_463(i142, i143) -{3,3}> gcd_Load_314(i143, i142) :|: 0 >= 0
mod_LE_338(i112, i107) -{4,4}> gcd_Load_463(0, i107) :|: i112 <= 0

(45) koat Proof (EQUIVALENT transformation)

YES(?, 1059*ar_0*ar_1 + 1083*ar_1^2 + 300*ar_0 + 894*ar_1 + 276*ar_0^2*ar_1 + 828*ar_0*ar_1^2 + 276*ar_0^2 + 552*ar_1^3 + 300)

Initial complexity problem:
1: T:
(Comp: ?, Cost: 3) mod_LE_475(ar_0, ar_1, ar_2) -> Com_1(gcd_Store_509(ar_0, ar_1, arityPad)) [ 1 <= ar_1 /\ 1 <= ar_0 /\ ar_0 <= ar_1 ]
(Comp: ?, Cost: 1) gcd_Store_509(ar_0, ar_1, ar_2) -> Com_1(gcd_Load_463(ar_0, ar_1, arityPad)) [ 0 >= 0 ]
(Comp: ?, Cost: 2) mod_LE_338(ar_0, ar_1, ar_2) -> Com_1(mod_GT_350(ar_1, ar_0, arityPad)) [ 1 <= ar_0 /\ 0 < ar_0 ]
(Comp: ?, Cost: 1) mod_NE_369(ar_0, ar_1, ar_2) -> Com_1(mod_Load_470(ar_0, ar_1, arityPad)) [ ar_1 < ar_0 /\ 1 <= ar_0 /\ 1 <= ar_1 ]
(Comp: ?, Cost: 1) mod_NE_369(ar_0, ar_1, ar_2) -> Com_1(mod_Load_470(ar_0, ar_1, arityPad)) [ ar_0 < ar_1 /\ 1 <= ar_0 /\ 1 <= ar_1 ]
(Comp: ?, Cost: 2) mod_Load_470(ar_0, ar_1, ar_2) -> Com_1(mod_LE_475(ar_0, ar_1, arityPad)) [ 1 <= ar_0 /\ 1 <= ar_1 ]
(Comp: ?, Cost: 3) mod_GT_350(ar_0, ar_1, ar_2) -> Com_1(mod_NE_369(ar_1, ar_0, arityPad)) [ 1 <= ar_0 /\ 1 <= ar_1 /\ 0 < ar_0 ]
(Comp: ?, Cost: 15) gcd_Load_2(ar_0, ar_1, ar_2) -> Com_1(gcd_Load_314(ar_0, ar_1, arityPad)) [ static'1 <= static''' + 1 /\ 0 <= static''' /\ static''' <= ar_2 + 2 /\ 0 <= ar_2 /\ 0 <= static'1 ]
(Comp: ?, Cost: 6) mod_LE_475(ar_0, ar_1, ar_2) -> Com_1(mod_Load_470(ar_0 - ar_1, ar_1, arityPad)) [ 2 <= ar_0 /\ 1 <= i172' /\ 1 <= ar_1 /\ 1 <= ar_0 /\ ar_1 < ar_0 /\ ar_0 - ar_1 = i172' ]
(Comp: ?, Cost: 8) gcd_Load_314(ar_0, ar_1, ar_2) -> Com_1(mod_LE_338(ar_0, ar_1, arityPad)) [ 0 < ar_1 ]
(Comp: ?, Cost: 8) gcd_Load_314(ar_0, ar_1, ar_2) -> Com_1(mod_LE_338(ar_0, ar_1, arityPad)) [ ar_1 < 0 ]
(Comp: ?, Cost: 3) mod_NE_369(ar_0, ar_1, ar_2) -> Com_1(gcd_Store_509(0, ar_0, arityPad)) [ 1 <= ar_0 /\ ar_1 = ar_0 ]
(Comp: ?, Cost: 4) mod_GT_350(ar_0, ar_1, ar_2) -> Com_1(gcd_Load_463(0, ar_0, arityPad)) [ 1 <= ar_1 /\ ar_0 <= -1 /\ ar_0 <= 0 ]
(Comp: ?, Cost: 3) gcd_Load_463(ar_0, ar_1, ar_2) -> Com_1(gcd_Load_314(ar_1, ar_0, arityPad)) [ 0 >= 0 ]
(Comp: ?, Cost: 4) mod_LE_338(ar_0, ar_1, ar_2) -> Com_1(gcd_Load_463(0, ar_1, arityPad)) [ ar_0 <= 0 ]
(Comp: 1, Cost: 0) koat_start(ar_0, ar_1, ar_2) -> Com_1(gcd_Load_2(ar_0, ar_1, ar_2)) [ 0 <= 0 ]
start location: koat_start
leaf cost: 0

Repeatedly propagating knowledge in problem 1 produces the following problem:
2: T:
(Comp: ?, Cost: 3) mod_LE_475(ar_0, ar_1, ar_2) -> Com_1(gcd_Store_509(ar_0, ar_1, arityPad)) [ 1 <= ar_1 /\ 1 <= ar_0 /\ ar_0 <= ar_1 ]
(Comp: ?, Cost: 1) gcd_Store_509(ar_0, ar_1, ar_2) -> Com_1(gcd_Load_463(ar_0, ar_1, arityPad)) [ 0 >= 0 ]
(Comp: ?, Cost: 2) mod_LE_338(ar_0, ar_1, ar_2) -> Com_1(mod_GT_350(ar_1, ar_0, arityPad)) [ 1 <= ar_0 /\ 0 < ar_0 ]
(Comp: ?, Cost: 1) mod_NE_369(ar_0, ar_1, ar_2) -> Com_1(mod_Load_470(ar_0, ar_1, arityPad)) [ ar_1 < ar_0 /\ 1 <= ar_0 /\ 1 <= ar_1 ]
(Comp: ?, Cost: 1) mod_NE_369(ar_0, ar_1, ar_2) -> Com_1(mod_Load_470(ar_0, ar_1, arityPad)) [ ar_0 < ar_1 /\ 1 <= ar_0 /\ 1 <= ar_1 ]
(Comp: ?, Cost: 2) mod_Load_470(ar_0, ar_1, ar_2) -> Com_1(mod_LE_475(ar_0, ar_1, arityPad)) [ 1 <= ar_0 /\ 1 <= ar_1 ]
(Comp: ?, Cost: 3) mod_GT_350(ar_0, ar_1, ar_2) -> Com_1(mod_NE_369(ar_1, ar_0, arityPad)) [ 1 <= ar_0 /\ 1 <= ar_1 /\ 0 < ar_0 ]
(Comp: 1, Cost: 15) gcd_Load_2(ar_0, ar_1, ar_2) -> Com_1(gcd_Load_314(ar_0, ar_1, arityPad)) [ static'1 <= static''' + 1 /\ 0 <= static''' /\ static''' <= ar_2 + 2 /\ 0 <= ar_2 /\ 0 <= static'1 ]
(Comp: ?, Cost: 6) mod_LE_475(ar_0, ar_1, ar_2) -> Com_1(mod_Load_470(ar_0 - ar_1, ar_1, arityPad)) [ 2 <= ar_0 /\ 1 <= i172' /\ 1 <= ar_1 /\ 1 <= ar_0 /\ ar_1 < ar_0 /\ ar_0 - ar_1 = i172' ]
(Comp: ?, Cost: 8) gcd_Load_314(ar_0, ar_1, ar_2) -> Com_1(mod_LE_338(ar_0, ar_1, arityPad)) [ 0 < ar_1 ]
(Comp: ?, Cost: 8) gcd_Load_314(ar_0, ar_1, ar_2) -> Com_1(mod_LE_338(ar_0, ar_1, arityPad)) [ ar_1 < 0 ]
(Comp: ?, Cost: 3) mod_NE_369(ar_0, ar_1, ar_2) -> Com_1(gcd_Store_509(0, ar_0, arityPad)) [ 1 <= ar_0 /\ ar_1 = ar_0 ]
(Comp: ?, Cost: 4) mod_GT_350(ar_0, ar_1, ar_2) -> Com_1(gcd_Load_463(0, ar_0, arityPad)) [ 1 <= ar_1 /\ ar_0 <= -1 /\ ar_0 <= 0 ]
(Comp: ?, Cost: 3) gcd_Load_463(ar_0, ar_1, ar_2) -> Com_1(gcd_Load_314(ar_1, ar_0, arityPad)) [ 0 >= 0 ]
(Comp: ?, Cost: 4) mod_LE_338(ar_0, ar_1, ar_2) -> Com_1(gcd_Load_463(0, ar_1, arityPad)) [ ar_0 <= 0 ]
(Comp: 1, Cost: 0) koat_start(ar_0, ar_1, ar_2) -> Com_1(gcd_Load_2(ar_0, ar_1, ar_2)) [ 0 <= 0 ]
start location: koat_start
leaf cost: 0

Applied AI with 'oct' on problem 2 to obtain the following invariants:
For symbol gcd_Load_463: X_1 >= 0
For symbol gcd_Store_509: X_2 - 1 >= 0 /\ X_1 + X_2 - 1 >= 0 /\ -X_1 + X_2 >= 0 /\ X_1 >= 0
For symbol mod_GT_350: X_2 - 1 >= 0
For symbol mod_LE_475: X_2 - 1 >= 0 /\ X_1 + X_2 - 2 >= 0 /\ X_1 - 1 >= 0
For symbol mod_Load_470: X_2 - 1 >= 0
For symbol mod_NE_369: X_2 - 1 >= 0 /\ X_1 + X_2 - 2 >= 0 /\ X_1 - 1 >= 0

This yielded the following problem:
3: T:
(Comp: 1, Cost: 0) koat_start(ar_0, ar_1, ar_2) -> Com_1(gcd_Load_2(ar_0, ar_1, ar_2)) [ 0 <= 0 ]
(Comp: ?, Cost: 4) mod_LE_338(ar_0, ar_1, ar_2) -> Com_1(gcd_Load_463(0, ar_1, arityPad)) [ ar_0 <= 0 ]
(Comp: ?, Cost: 3) gcd_Load_463(ar_0, ar_1, ar_2) -> Com_1(gcd_Load_314(ar_1, ar_0, arityPad)) [ ar_0 >= 0 /\ 0 >= 0 ]
(Comp: ?, Cost: 4) mod_GT_350(ar_0, ar_1, ar_2) -> Com_1(gcd_Load_463(0, ar_0, arityPad)) [ ar_1 - 1 >= 0 /\ 1 <= ar_1 /\ ar_0 <= -1 /\ ar_0 <= 0 ]
(Comp: ?, Cost: 3) mod_NE_369(ar_0, ar_1, ar_2) -> Com_1(gcd_Store_509(0, ar_0, arityPad)) [ ar_1 - 1 >= 0 /\ ar_0 + ar_1 - 2 >= 0 /\ ar_0 - 1 >= 0 /\ 1 <= ar_0 /\ ar_1 = ar_0 ]
(Comp: ?, Cost: 8) gcd_Load_314(ar_0, ar_1, ar_2) -> Com_1(mod_LE_338(ar_0, ar_1, arityPad)) [ ar_1 < 0 ]
(Comp: ?, Cost: 8) gcd_Load_314(ar_0, ar_1, ar_2) -> Com_1(mod_LE_338(ar_0, ar_1, arityPad)) [ 0 < ar_1 ]
(Comp: ?, Cost: 6) mod_LE_475(ar_0, ar_1, ar_2) -> Com_1(mod_Load_470(ar_0 - ar_1, ar_1, arityPad)) [ ar_1 - 1 >= 0 /\ ar_0 + ar_1 - 2 >= 0 /\ ar_0 - 1 >= 0 /\ 2 <= ar_0 /\ 1 <= i172' /\ 1 <= ar_1 /\ 1 <= ar_0 /\ ar_1 < ar_0 /\ ar_0 - ar_1 = i172' ]
(Comp: 1, Cost: 15) gcd_Load_2(ar_0, ar_1, ar_2) -> Com_1(gcd_Load_314(ar_0, ar_1, arityPad)) [ static'1 <= static''' + 1 /\ 0 <= static''' /\ static''' <= ar_2 + 2 /\ 0 <= ar_2 /\ 0 <= static'1 ]
(Comp: ?, Cost: 3) mod_GT_350(ar_0, ar_1, ar_2) -> Com_1(mod_NE_369(ar_1, ar_0, arityPad)) [ ar_1 - 1 >= 0 /\ 1 <= ar_0 /\ 1 <= ar_1 /\ 0 < ar_0 ]
(Comp: ?, Cost: 2) mod_Load_470(ar_0, ar_1, ar_2) -> Com_1(mod_LE_475(ar_0, ar_1, arityPad)) [ ar_1 - 1 >= 0 /\ 1 <= ar_0 /\ 1 <= ar_1 ]
(Comp: ?, Cost: 1) mod_NE_369(ar_0, ar_1, ar_2) -> Com_1(mod_Load_470(ar_0, ar_1, arityPad)) [ ar_1 - 1 >= 0 /\ ar_0 + ar_1 - 2 >= 0 /\ ar_0 - 1 >= 0 /\ ar_0 < ar_1 /\ 1 <= ar_0 /\ 1 <= ar_1 ]
(Comp: ?, Cost: 1) mod_NE_369(ar_0, ar_1, ar_2) -> Com_1(mod_Load_470(ar_0, ar_1, arityPad)) [ ar_1 - 1 >= 0 /\ ar_0 + ar_1 - 2 >= 0 /\ ar_0 - 1 >= 0 /\ ar_1 < ar_0 /\ 1 <= ar_0 /\ 1 <= ar_1 ]
(Comp: ?, Cost: 2) mod_LE_338(ar_0, ar_1, ar_2) -> Com_1(mod_GT_350(ar_1, ar_0, arityPad)) [ 1 <= ar_0 /\ 0 < ar_0 ]
(Comp: ?, Cost: 1) gcd_Store_509(ar_0, ar_1, ar_2) -> Com_1(gcd_Load_463(ar_0, ar_1, arityPad)) [ ar_1 - 1 >= 0 /\ ar_0 + ar_1 - 1 >= 0 /\ -ar_0 + ar_1 >= 0 /\ ar_0 >= 0 /\ 0 >= 0 ]
(Comp: ?, Cost: 3) mod_LE_475(ar_0, ar_1, ar_2) -> Com_1(gcd_Store_509(ar_0, ar_1, arityPad)) [ ar_1 - 1 >= 0 /\ ar_0 + ar_1 - 2 >= 0 /\ ar_0 - 1 >= 0 /\ 1 <= ar_1 /\ 1 <= ar_0 /\ ar_0 <= ar_1 ]
start location: koat_start
leaf cost: 0

Repeatedly propagating knowledge in problem 3 produces the following problem:
4: T:
(Comp: 1, Cost: 0) koat_start(ar_0, ar_1, ar_2) -> Com_1(gcd_Load_2(ar_0, ar_1, ar_2)) [ 0 <= 0 ]
(Comp: ?, Cost: 4) mod_LE_338(ar_0, ar_1, ar_2) -> Com_1(gcd_Load_463(0, ar_1, arityPad)) [ ar_0 <= 0 ]
(Comp: ?, Cost: 3) gcd_Load_463(ar_0, ar_1, ar_2) -> Com_1(gcd_Load_314(ar_1, ar_0, arityPad)) [ ar_0 >= 0 /\ 0 >= 0 ]
(Comp: ?, Cost: 4) mod_GT_350(ar_0, ar_1, ar_2) -> Com_1(gcd_Load_463(0, ar_0, arityPad)) [ ar_1 - 1 >= 0 /\ 1 <= ar_1 /\ ar_0 <= -1 /\ ar_0 <= 0 ]
(Comp: ?, Cost: 3) mod_NE_369(ar_0, ar_1, ar_2) -> Com_1(gcd_Store_509(0, ar_0, arityPad)) [ ar_1 - 1 >= 0 /\ ar_0 + ar_1 - 2 >= 0 /\ ar_0 - 1 >= 0 /\ 1 <= ar_0 /\ ar_1 = ar_0 ]
(Comp: 1, Cost: 8) gcd_Load_314(ar_0, ar_1, ar_2) -> Com_1(mod_LE_338(ar_0, ar_1, arityPad)) [ ar_1 < 0 ]
(Comp: ?, Cost: 8) gcd_Load_314(ar_0, ar_1, ar_2) -> Com_1(mod_LE_338(ar_0, ar_1, arityPad)) [ 0 < ar_1 ]
(Comp: ?, Cost: 6) mod_LE_475(ar_0, ar_1, ar_2) -> Com_1(mod_Load_470(ar_0 - ar_1, ar_1, arityPad)) [ ar_1 - 1 >= 0 /\ ar_0 + ar_1 - 2 >= 0 /\ ar_0 - 1 >= 0 /\ 2 <= ar_0 /\ 1 <= i172' /\ 1 <= ar_1 /\ 1 <= ar_0 /\ ar_1 < ar_0 /\ ar_0 - ar_1 = i172' ]
(Comp: 1, Cost: 15) gcd_Load_2(ar_0, ar_1, ar_2) -> Com_1(gcd_Load_314(ar_0, ar_1, arityPad)) [ static'1 <= static''' + 1 /\ 0 <= static''' /\ static''' <= ar_2 + 2 /\ 0 <= ar_2 /\ 0 <= static'1 ]
(Comp: ?, Cost: 3) mod_GT_350(ar_0, ar_1, ar_2) -> Com_1(mod_NE_369(ar_1, ar_0, arityPad)) [ ar_1 - 1 >= 0 /\ 1 <= ar_0 /\ 1 <= ar_1 /\ 0 < ar_0 ]
(Comp: ?, Cost: 2) mod_Load_470(ar_0, ar_1, ar_2) -> Com_1(mod_LE_475(ar_0, ar_1, arityPad)) [ ar_1 - 1 >= 0 /\ 1 <= ar_0 /\ 1 <= ar_1 ]
(Comp: ?, Cost: 1) mod_NE_369(ar_0, ar_1, ar_2) -> Com_1(mod_Load_470(ar_0, ar_1, arityPad)) [ ar_1 - 1 >= 0 /\ ar_0 + ar_1 - 2 >= 0 /\ ar_0 - 1 >= 0 /\ ar_0 < ar_1 /\ 1 <= ar_0 /\ 1 <= ar_1 ]
(Comp: ?, Cost: 1) mod_NE_369(ar_0, ar_1, ar_2) -> Com_1(mod_Load_470(ar_0, ar_1, arityPad)) [ ar_1 - 1 >= 0 /\ ar_0 + ar_1 - 2 >= 0 /\ ar_0 - 1 >= 0 /\ ar_1 < ar_0 /\ 1 <= ar_0 /\ 1 <= ar_1 ]
(Comp: ?, Cost: 2) mod_LE_338(ar_0, ar_1, ar_2) -> Com_1(mod_GT_350(ar_1, ar_0, arityPad)) [ 1 <= ar_0 /\ 0 < ar_0 ]
(Comp: ?, Cost: 1) gcd_Store_509(ar_0, ar_1, ar_2) -> Com_1(gcd_Load_463(ar_0, ar_1, arityPad)) [ ar_1 - 1 >= 0 /\ ar_0 + ar_1 - 1 >= 0 /\ -ar_0 + ar_1 >= 0 /\ ar_0 >= 0 /\ 0 >= 0 ]
(Comp: ?, Cost: 3) mod_LE_475(ar_0, ar_1, ar_2) -> Com_1(gcd_Store_509(ar_0, ar_1, arityPad)) [ ar_1 - 1 >= 0 /\ ar_0 + ar_1 - 2 >= 0 /\ ar_0 - 1 >= 0 /\ 1 <= ar_1 /\ 1 <= ar_0 /\ ar_0 <= ar_1 ]
start location: koat_start
leaf cost: 0

By chaining the transition koat_start(ar_0, ar_1, ar_2) -> Com_1(gcd_Load_2(ar_0, ar_1, ar_2)) [ 0 <= 0 ] with all transitions in problem 4, the following new transition is obtained:
koat_start(ar_0, ar_1, ar_2) -> Com_1(gcd_Load_314(ar_0, ar_1, arityPad)) [ 0 <= 0 /\ static'1 <= static''' + 1 /\ 0 <= static''' /\ static''' <= ar_2 + 2 /\ 0 <= ar_2 /\ 0 <= static'1 ]
We thus obtain the following problem:
5: T:
(Comp: 1, Cost: 15) koat_start(ar_0, ar_1, ar_2) -> Com_1(gcd_Load_314(ar_0, ar_1, arityPad)) [ 0 <= 0 /\ static'1 <= static''' + 1 /\ 0 <= static''' /\ static''' <= ar_2 + 2 /\ 0 <= ar_2 /\ 0 <= static'1 ]
(Comp: ?, Cost: 4) mod_LE_338(ar_0, ar_1, ar_2) -> Com_1(gcd_Load_463(0, ar_1, arityPad)) [ ar_0 <= 0 ]
(Comp: ?, Cost: 3) gcd_Load_463(ar_0, ar_1, ar_2) -> Com_1(gcd_Load_314(ar_1, ar_0, arityPad)) [ ar_0 >= 0 /\ 0 >= 0 ]
(Comp: ?, Cost: 4) mod_GT_350(ar_0, ar_1, ar_2) -> Com_1(gcd_Load_463(0, ar_0, arityPad)) [ ar_1 - 1 >= 0 /\ 1 <= ar_1 /\ ar_0 <= -1 /\ ar_0 <= 0 ]
(Comp: ?, Cost: 3) mod_NE_369(ar_0, ar_1, ar_2) -> Com_1(gcd_Store_509(0, ar_0, arityPad)) [ ar_1 - 1 >= 0 /\ ar_0 + ar_1 - 2 >= 0 /\ ar_0 - 1 >= 0 /\ 1 <= ar_0 /\ ar_1 = ar_0 ]
(Comp: 1, Cost: 8) gcd_Load_314(ar_0, ar_1, ar_2) -> Com_1(mod_LE_338(ar_0, ar_1, arityPad)) [ ar_1 < 0 ]
(Comp: ?, Cost: 8) gcd_Load_314(ar_0, ar_1, ar_2) -> Com_1(mod_LE_338(ar_0, ar_1, arityPad)) [ 0 < ar_1 ]
(Comp: ?, Cost: 6) mod_LE_475(ar_0, ar_1, ar_2) -> Com_1(mod_Load_470(ar_0 - ar_1, ar_1, arityPad)) [ ar_1 - 1 >= 0 /\ ar_0 + ar_1 - 2 >= 0 /\ ar_0 - 1 >= 0 /\ 2 <= ar_0 /\ 1 <= i172' /\ 1 <= ar_1 /\ 1 <= ar_0 /\ ar_1 < ar_0 /\ ar_0 - ar_1 = i172' ]
(Comp: 1, Cost: 15) gcd_Load_2(ar_0, ar_1, ar_2) -> Com_1(gcd_Load_314(ar_0, ar_1, arityPad)) [ static'1 <= static''' + 1 /\ 0 <= static''' /\ static''' <= ar_2 + 2 /\ 0 <= ar_2 /\ 0 <= static'1 ]
(Comp: ?, Cost: 3) mod_GT_350(ar_0, ar_1, ar_2) -> Com_1(mod_NE_369(ar_1, ar_0, arityPad)) [ ar_1 - 1 >= 0 /\ 1 <= ar_0 /\ 1 <= ar_1 /\ 0 < ar_0 ]
(Comp: ?, Cost: 2) mod_Load_470(ar_0, ar_1, ar_2) -> Com_1(mod_LE_475(ar_0, ar_1, arityPad)) [ ar_1 - 1 >= 0 /\ 1 <= ar_0 /\ 1 <= ar_1 ]
(Comp: ?, Cost: 1) mod_NE_369(ar_0, ar_1, ar_2) -> Com_1(mod_Load_470(ar_0, ar_1, arityPad)) [ ar_1 - 1 >= 0 /\ ar_0 + ar_1 - 2 >= 0 /\ ar_0 - 1 >= 0 /\ ar_0 < ar_1 /\ 1 <= ar_0 /\ 1 <= ar_1 ]
(Comp: ?, Cost: 1) mod_NE_369(ar_0, ar_1, ar_2) -> Com_1(mod_Load_470(ar_0, ar_1, arityPad)) [ ar_1 - 1 >= 0 /\ ar_0 + ar_1 - 2 >= 0 /\ ar_0 - 1 >= 0 /\ ar_1 < ar_0 /\ 1 <= ar_0 /\ 1 <= ar_1 ]
(Comp: ?, Cost: 2) mod_LE_338(ar_0, ar_1, ar_2) -> Com_1(mod_GT_350(ar_1, ar_0, arityPad)) [ 1 <= ar_0 /\ 0 < ar_0 ]
(Comp: ?, Cost: 1) gcd_Store_509(ar_0, ar_1, ar_2) -> Com_1(gcd_Load_463(ar_0, ar_1, arityPad)) [ ar_1 - 1 >= 0 /\ ar_0 + ar_1 - 1 >= 0 /\ -ar_0 + ar_1 >= 0 /\ ar_0 >= 0 /\ 0 >= 0 ]
(Comp: ?, Cost: 3) mod_LE_475(ar_0, ar_1, ar_2) -> Com_1(gcd_Store_509(ar_0, ar_1, arityPad)) [ ar_1 - 1 >= 0 /\ ar_0 + ar_1 - 2 >= 0 /\ ar_0 - 1 >= 0 /\ 1 <= ar_1 /\ 1 <= ar_0 /\ ar_0 <= ar_1 ]
start location: koat_start
leaf cost: 0

Testing for reachability in the complexity graph removes the following transition from problem 5:
gcd_Load_2(ar_0, ar_1, ar_2) -> Com_1(gcd_Load_314(ar_0, ar_1, arityPad)) [ static'1 <= static''' + 1 /\ 0 <= static''' /\ static''' <= ar_2 + 2 /\ 0 <= ar_2 /\ 0 <= static'1 ]
We thus obtain the following problem:
6: T:
(Comp: ?, Cost: 3) mod_LE_475(ar_0, ar_1, ar_2) -> Com_1(gcd_Store_509(ar_0, ar_1, arityPad)) [ ar_1 - 1 >= 0 /\ ar_0 + ar_1 - 2 >= 0 /\ ar_0 - 1 >= 0 /\ 1 <= ar_1 /\ 1 <= ar_0 /\ ar_0 <= ar_1 ]
(Comp: ?, Cost: 6) mod_LE_475(ar_0, ar_1, ar_2) -> Com_1(mod_Load_470(ar_0 - ar_1, ar_1, arityPad)) [ ar_1 - 1 >= 0 /\ ar_0 + ar_1 - 2 >= 0 /\ ar_0 - 1 >= 0 /\ 2 <= ar_0 /\ 1 <= i172' /\ 1 <= ar_1 /\ 1 <= ar_0 /\ ar_1 < ar_0 /\ ar_0 - ar_1 = i172' ]
(Comp: ?, Cost: 2) mod_Load_470(ar_0, ar_1, ar_2) -> Com_1(mod_LE_475(ar_0, ar_1, arityPad)) [ ar_1 - 1 >= 0 /\ 1 <= ar_0 /\ 1 <= ar_1 ]
(Comp: ?, Cost: 1) gcd_Store_509(ar_0, ar_1, ar_2) -> Com_1(gcd_Load_463(ar_0, ar_1, arityPad)) [ ar_1 - 1 >= 0 /\ ar_0 + ar_1 - 1 >= 0 /\ -ar_0 + ar_1 >= 0 /\ ar_0 >= 0 /\ 0 >= 0 ]
(Comp: ?, Cost: 1) mod_NE_369(ar_0, ar_1, ar_2) -> Com_1(mod_Load_470(ar_0, ar_1, arityPad)) [ ar_1 - 1 >= 0 /\ ar_0 + ar_1 - 2 >= 0 /\ ar_0 - 1 >= 0 /\ ar_1 < ar_0 /\ 1 <= ar_0 /\ 1 <= ar_1 ]
(Comp: ?, Cost: 1) mod_NE_369(ar_0, ar_1, ar_2) -> Com_1(mod_Load_470(ar_0, ar_1, arityPad)) [ ar_1 - 1 >= 0 /\ ar_0 + ar_1 - 2 >= 0 /\ ar_0 - 1 >= 0 /\ ar_0 < ar_1 /\ 1 <= ar_0 /\ 1 <= ar_1 ]
(Comp: ?, Cost: 3) mod_NE_369(ar_0, ar_1, ar_2) -> Com_1(gcd_Store_509(0, ar_0, arityPad)) [ ar_1 - 1 >= 0 /\ ar_0 + ar_1 - 2 >= 0 /\ ar_0 - 1 >= 0 /\ 1 <= ar_0 /\ ar_1 = ar_0 ]
(Comp: ?, Cost: 3) mod_GT_350(ar_0, ar_1, ar_2) -> Com_1(mod_NE_369(ar_1, ar_0, arityPad)) [ ar_1 - 1 >= 0 /\ 1 <= ar_0 /\ 1 <= ar_1 /\ 0 < ar_0 ]
(Comp: ?, Cost: 4) mod_GT_350(ar_0, ar_1, ar_2) -> Com_1(gcd_Load_463(0, ar_0, arityPad)) [ ar_1 - 1 >= 0 /\ 1 <= ar_1 /\ ar_0 <= -1 /\ ar_0 <= 0 ]
(Comp: ?, Cost: 3) gcd_Load_463(ar_0, ar_1, ar_2) -> Com_1(gcd_Load_314(ar_1, ar_0, arityPad)) [ ar_0 >= 0 /\ 0 >= 0 ]
(Comp: ?, Cost: 2) mod_LE_338(ar_0, ar_1, ar_2) -> Com_1(mod_GT_350(ar_1, ar_0, arityPad)) [ 1 <= ar_0 /\ 0 < ar_0 ]
(Comp: ?, Cost: 4) mod_LE_338(ar_0, ar_1, ar_2) -> Com_1(gcd_Load_463(0, ar_1, arityPad)) [ ar_0 <= 0 ]
(Comp: ?, Cost: 8) gcd_Load_314(ar_0, ar_1, ar_2) -> Com_1(mod_LE_338(ar_0, ar_1, arityPad)) [ 0 < ar_1 ]
(Comp: 1, Cost: 8) gcd_Load_314(ar_0, ar_1, ar_2) -> Com_1(mod_LE_338(ar_0, ar_1, arityPad)) [ ar_1 < 0 ]
(Comp: 1, Cost: 15) koat_start(ar_0, ar_1, ar_2) -> Com_1(gcd_Load_314(ar_0, ar_1, arityPad)) [ 0 <= 0 /\ static'1 <= static''' + 1 /\ 0 <= static''' /\ static''' <= ar_2 + 2 /\ 0 <= ar_2 /\ 0 <= static'1 ]
start location: koat_start
leaf cost: 0

By chaining the transition mod_LE_475(ar_0, ar_1, ar_2) -> Com_1(gcd_Store_509(ar_0, ar_1, arityPad)) [ ar_1 - 1 >= 0 /\ ar_0 + ar_1 - 2 >= 0 /\ ar_0 - 1 >= 0 /\ 1 <= ar_1 /\ 1 <= ar_0 /\ ar_0 <= ar_1 ] with all transitions in problem 6, the following new transition is obtained:
mod_LE_475(ar_0, ar_1, ar_2) -> Com_1(gcd_Load_463(ar_0, ar_1, arityPad')) [ ar_1 - 1 >= 0 /\ ar_0 + ar_1 - 2 >= 0 /\ ar_0 - 1 >= 0 /\ 1 <= ar_1 /\ 1 <= ar_0 /\ ar_0 <= ar_1 /\ ar_0 + ar_1 - 1 >= 0 /\ -ar_0 + ar_1 >= 0 /\ ar_0 >= 0 /\ 0 >= 0 ]
We thus obtain the following problem:
7: T:
(Comp: ?, Cost: 4) mod_LE_475(ar_0, ar_1, ar_2) -> Com_1(gcd_Load_463(ar_0, ar_1, arityPad')) [ ar_1 - 1 >= 0 /\ ar_0 + ar_1 - 2 >= 0 /\ ar_0 - 1 >= 0 /\ 1 <= ar_1 /\ 1 <= ar_0 /\ ar_0 <= ar_1 /\ ar_0 + ar_1 - 1 >= 0 /\ -ar_0 + ar_1 >= 0 /\ ar_0 >= 0 /\ 0 >= 0 ]
(Comp: ?, Cost: 6) mod_LE_475(ar_0, ar_1, ar_2) -> Com_1(mod_Load_470(ar_0 - ar_1, ar_1, arityPad)) [ ar_1 - 1 >= 0 /\ ar_0 + ar_1 - 2 >= 0 /\ ar_0 - 1 >= 0 /\ 2 <= ar_0 /\ 1 <= i172' /\ 1 <= ar_1 /\ 1 <= ar_0 /\ ar_1 < ar_0 /\ ar_0 - ar_1 = i172' ]
(Comp: ?, Cost: 2) mod_Load_470(ar_0, ar_1, ar_2) -> Com_1(mod_LE_475(ar_0, ar_1, arityPad)) [ ar_1 - 1 >= 0 /\ 1 <= ar_0 /\ 1 <= ar_1 ]
(Comp: ?, Cost: 1) gcd_Store_509(ar_0, ar_1, ar_2) -> Com_1(gcd_Load_463(ar_0, ar_1, arityPad)) [ ar_1 - 1 >= 0 /\ ar_0 + ar_1 - 1 >= 0 /\ -ar_0 + ar_1 >= 0 /\ ar_0 >= 0 /\ 0 >= 0 ]
(Comp: ?, Cost: 1) mod_NE_369(ar_0, ar_1, ar_2) -> Com_1(mod_Load_470(ar_0, ar_1, arityPad)) [ ar_1 - 1 >= 0 /\ ar_0 + ar_1 - 2 >= 0 /\ ar_0 - 1 >= 0 /\ ar_1 < ar_0 /\ 1 <= ar_0 /\ 1 <= ar_1 ]
(Comp: ?, Cost: 1) mod_NE_369(ar_0, ar_1, ar_2) -> Com_1(mod_Load_470(ar_0, ar_1, arityPad)) [ ar_1 - 1 >= 0 /\ ar_0 + ar_1 - 2 >= 0 /\ ar_0 - 1 >= 0 /\ ar_0 < ar_1 /\ 1 <= ar_0 /\ 1 <= ar_1 ]
(Comp: ?, Cost: 3) mod_NE_369(ar_0, ar_1, ar_2) -> Com_1(gcd_Store_509(0, ar_0, arityPad)) [ ar_1 - 1 >= 0 /\ ar_0 + ar_1 - 2 >= 0 /\ ar_0 - 1 >= 0 /\ 1 <= ar_0 /\ ar_1 = ar_0 ]
(Comp: ?, Cost: 3) mod_GT_350(ar_0, ar_1, ar_2) -> Com_1(mod_NE_369(ar_1, ar_0, arityPad)) [ ar_1 - 1 >= 0 /\ 1 <= ar_0 /\ 1 <= ar_1 /\ 0 < ar_0 ]
(Comp: ?, Cost: 4) mod_GT_350(ar_0, ar_1, ar_2) -> Com_1(gcd_Load_463(0, ar_0, arityPad)) [ ar_1 - 1 >= 0 /\ 1 <= ar_1 /\ ar_0 <= -1 /\ ar_0 <= 0 ]
(Comp: ?, Cost: 3) gcd_Load_463(ar_0, ar_1, ar_2) -> Com_1(gcd_Load_314(ar_1, ar_0, arityPad)) [ ar_0 >= 0 /\ 0 >= 0 ]
(Comp: ?, Cost: 2) mod_LE_338(ar_0, ar_1, ar_2) -> Com_1(mod_GT_350(ar_1, ar_0, arityPad)) [ 1 <= ar_0 /\ 0 < ar_0 ]
(Comp: ?, Cost: 4) mod_LE_338(ar_0, ar_1, ar_2) -> Com_1(gcd_Load_463(0, ar_1, arityPad)) [ ar_0 <= 0 ]
(Comp: ?, Cost: 8) gcd_Load_314(ar_0, ar_1, ar_2) -> Com_1(mod_LE_338(ar_0, ar_1, arityPad)) [ 0 < ar_1 ]
(Comp: 1, Cost: 8) gcd_Load_314(ar_0, ar_1, ar_2) -> Com_1(mod_LE_338(ar_0, ar_1, arityPad)) [ ar_1 < 0 ]
(Comp: 1, Cost: 15) koat_start(ar_0, ar_1, ar_2) -> Com_1(gcd_Load_314(ar_0, ar_1, arityPad)) [ 0 <= 0 /\ static'1 <= static''' + 1 /\ 0 <= static''' /\ static''' <= ar_2 + 2 /\ 0 <= ar_2 /\ 0 <= static'1 ]
start location: koat_start
leaf cost: 0

By chaining the transition mod_LE_475(ar_0, ar_1, ar_2) -> Com_1(gcd_Load_463(ar_0, ar_1, arityPad')) [ ar_1 - 1 >= 0 /\ ar_0 + ar_1 - 2 >= 0 /\ ar_0 - 1 >= 0 /\ 1 <= ar_1 /\ 1 <= ar_0 /\ ar_0 <= ar_1 /\ ar_0 + ar_1 - 1 >= 0 /\ -ar_0 + ar_1 >= 0 /\ ar_0 >= 0 /\ 0 >= 0 ] with all transitions in problem 7, the following new transition is obtained:
mod_LE_475(ar_0, ar_1, ar_2) -> Com_1(gcd_Load_314(ar_1, ar_0, arityPad)) [ ar_1 - 1 >= 0 /\ ar_0 + ar_1 - 2 >= 0 /\ ar_0 - 1 >= 0 /\ 1 <= ar_1 /\ 1 <= ar_0 /\ ar_0 <= ar_1 /\ ar_0 + ar_1 - 1 >= 0 /\ -ar_0 + ar_1 >= 0 /\ ar_0 >= 0 /\ 0 >= 0 ]
We thus obtain the following problem:
8: T:
(Comp: ?, Cost: 7) mod_LE_475(ar_0, ar_1, ar_2) -> Com_1(gcd_Load_314(ar_1, ar_0, arityPad)) [ ar_1 - 1 >= 0 /\ ar_0 + ar_1 - 2 >= 0 /\ ar_0 - 1 >= 0 /\ 1 <= ar_1 /\ 1 <= ar_0 /\ ar_0 <= ar_1 /\ ar_0 + ar_1 - 1 >= 0 /\ -ar_0 + ar_1 >= 0 /\ ar_0 >= 0 /\ 0 >= 0 ]
(Comp: ?, Cost: 6) mod_LE_475(ar_0, ar_1, ar_2) -> Com_1(mod_Load_470(ar_0 - ar_1, ar_1, arityPad)) [ ar_1 - 1 >= 0 /\ ar_0 + ar_1 - 2 >= 0 /\ ar_0 - 1 >= 0 /\ 2 <= ar_0 /\ 1 <= i172' /\ 1 <= ar_1 /\ 1 <= ar_0 /\ ar_1 < ar_0 /\ ar_0 - ar_1 = i172' ]
(Comp: ?, Cost: 2) mod_Load_470(ar_0, ar_1, ar_2) -> Com_1(mod_LE_475(ar_0, ar_1, arityPad)) [ ar_1 - 1 >= 0 /\ 1 <= ar_0 /\ 1 <= ar_1 ]
(Comp: ?, Cost: 1) gcd_Store_509(ar_0, ar_1, ar_2) -> Com_1(gcd_Load_463(ar_0, ar_1, arityPad)) [ ar_1 - 1 >= 0 /\ ar_0 + ar_1 - 1 >= 0 /\ -ar_0 + ar_1 >= 0 /\ ar_0 >= 0 /\ 0 >= 0 ]
(Comp: ?, Cost: 1) mod_NE_369(ar_0, ar_1, ar_2) -> Com_1(mod_Load_470(ar_0, ar_1, arityPad)) [ ar_1 - 1 >= 0 /\ ar_0 + ar_1 - 2 >= 0 /\ ar_0 - 1 >= 0 /\ ar_1 < ar_0 /\ 1 <= ar_0 /\ 1 <= ar_1 ]
(Comp: ?, Cost: 1) mod_NE_369(ar_0, ar_1, ar_2) -> Com_1(mod_Load_470(ar_0, ar_1, arityPad)) [ ar_1 - 1 >= 0 /\ ar_0 + ar_1 - 2 >= 0 /\ ar_0 - 1 >= 0 /\ ar_0 < ar_1 /\ 1 <= ar_0 /\ 1 <= ar_1 ]
(Comp: ?, Cost: 3) mod_NE_369(ar_0, ar_1, ar_2) -> Com_1(gcd_Store_509(0, ar_0, arityPad)) [ ar_1 - 1 >= 0 /\ ar_0 + ar_1 - 2 >= 0 /\ ar_0 - 1 >= 0 /\ 1 <= ar_0 /\ ar_1 = ar_0 ]
(Comp: ?, Cost: 3) mod_GT_350(ar_0, ar_1, ar_2) -> Com_1(mod_NE_369(ar_1, ar_0, arityPad)) [ ar_1 - 1 >= 0 /\ 1 <= ar_0 /\ 1 <= ar_1 /\ 0 < ar_0 ]
(Comp: ?, Cost: 4) mod_GT_350(ar_0, ar_1, ar_2) -> Com_1(gcd_Load_463(0, ar_0, arityPad)) [ ar_1 - 1 >= 0 /\ 1 <= ar_1 /\ ar_0 <= -1 /\ ar_0 <= 0 ]
(Comp: ?, Cost: 3) gcd_Load_463(ar_0, ar_1, ar_2) -> Com_1(gcd_Load_314(ar_1, ar_0, arityPad)) [ ar_0 >= 0 /\ 0 >= 0 ]
(Comp: ?, Cost: 2) mod_LE_338(ar_0, ar_1, ar_2) -> Com_1(mod_GT_350(ar_1, ar_0, arityPad)) [ 1 <= ar_0 /\ 0 < ar_0 ]
(Comp: ?, Cost: 4) mod_LE_338(ar_0, ar_1, ar_2) -> Com_1(gcd_Load_463(0, ar_1, arityPad)) [ ar_0 <= 0 ]
(Comp: ?, Cost: 8) gcd_Load_314(ar_0, ar_1, ar_2) -> Com_1(mod_LE_338(ar_0, ar_1, arityPad)) [ 0 < ar_1 ]
(Comp: 1, Cost: 8) gcd_Load_314(ar_0, ar_1, ar_2) -> Com_1(mod_LE_338(ar_0, ar_1, arityPad)) [ ar_1 < 0 ]
(Comp: 1, Cost: 15) koat_start(ar_0, ar_1, ar_2) -> Com_1(gcd_Load_314(ar_0, ar_1, arityPad)) [ 0 <= 0 /\ static'1 <= static''' + 1 /\ 0 <= static''' /\ static''' <= ar_2 + 2 /\ 0 <= ar_2 /\ 0 <= static'1 ]
start location: koat_start
leaf cost: 0

By chaining the transition mod_LE_475(ar_0, ar_1, ar_2) -> Com_1(gcd_Load_314(ar_1, ar_0, arityPad)) [ ar_1 - 1 >= 0 /\ ar_0 + ar_1 - 2 >= 0 /\ ar_0 - 1 >= 0 /\ 1 <= ar_1 /\ 1 <= ar_0 /\ ar_0 <= ar_1 /\ ar_0 + ar_1 - 1 >= 0 /\ -ar_0 + ar_1 >= 0 /\ ar_0 >= 0 /\ 0 >= 0 ] with all transitions in problem 8, the following new transition is obtained:
mod_LE_475(ar_0, ar_1, ar_2) -> Com_1(mod_LE_338(ar_1, ar_0, arityPad')) [ ar_1 - 1 >= 0 /\ ar_0 + ar_1 - 2 >= 0 /\ ar_0 - 1 >= 0 /\ 1 <= ar_1 /\ 1 <= ar_0 /\ ar_0 <= ar_1 /\ ar_0 + ar_1 - 1 >= 0 /\ -ar_0 + ar_1 >= 0 /\ ar_0 >= 0 /\ 0 >= 0 /\ 0 < ar_0 ]
We thus obtain the following problem:
9: T:
(Comp: ?, Cost: 15) mod_LE_475(ar_0, ar_1, ar_2) -> Com_1(mod_LE_338(ar_1, ar_0, arityPad')) [ ar_1 - 1 >= 0 /\ ar_0 + ar_1 - 2 >= 0 /\ ar_0 - 1 >= 0 /\ 1 <= ar_1 /\ 1 <= ar_0 /\ ar_0 <= ar_1 /\ ar_0 + ar_1 - 1 >= 0 /\ -ar_0 + ar_1 >= 0 /\ ar_0 >= 0 /\ 0 >= 0 /\ 0 < ar_0 ]
(Comp: ?, Cost: 6) mod_LE_475(ar_0, ar_1, ar_2) -> Com_1(mod_Load_470(ar_0 - ar_1, ar_1, arityPad)) [ ar_1 - 1 >= 0 /\ ar_0 + ar_1 - 2 >= 0 /\ ar_0 - 1 >= 0 /\ 2 <= ar_0 /\ 1 <= i172' /\ 1 <= ar_1 /\ 1 <= ar_0 /\ ar_1 < ar_0 /\ ar_0 - ar_1 = i172' ]
(Comp: ?, Cost: 2) mod_Load_470(ar_0, ar_1, ar_2) -> Com_1(mod_LE_475(ar_0, ar_1, arityPad)) [ ar_1 - 1 >= 0 /\ 1 <= ar_0 /\ 1 <= ar_1 ]
(Comp: ?, Cost: 1) gcd_Store_509(ar_0, ar_1, ar_2) -> Com_1(gcd_Load_463(ar_0, ar_1, arityPad)) [ ar_1 - 1 >= 0 /\ ar_0 + ar_1 - 1 >= 0 /\ -ar_0 + ar_1 >= 0 /\ ar_0 >= 0 /\ 0 >= 0 ]
(Comp: ?, Cost: 1) mod_NE_369(ar_0, ar_1, ar_2) -> Com_1(mod_Load_470(ar_0, ar_1, arityPad)) [ ar_1 - 1 >= 0 /\ ar_0 + ar_1 - 2 >= 0 /\ ar_0 - 1 >= 0 /\ ar_1 < ar_0 /\ 1 <= ar_0 /\ 1 <= ar_1 ]
(Comp: ?, Cost: 1) mod_NE_369(ar_0, ar_1, ar_2) -> Com_1(mod_Load_470(ar_0, ar_1, arityPad)) [ ar_1 - 1 >= 0 /\ ar_0 + ar_1 - 2 >= 0 /\ ar_0 - 1 >= 0 /\ ar_0 < ar_1 /\ 1 <= ar_0 /\ 1 <= ar_1 ]
(Comp: ?, Cost: 3) mod_NE_369(ar_0, ar_1, ar_2) -> Com_1(gcd_Store_509(0, ar_0, arityPad)) [ ar_1 - 1 >= 0 /\ ar_0 + ar_1 - 2 >= 0 /\ ar_0 - 1 >= 0 /\ 1 <= ar_0 /\ ar_1 = ar_0 ]
(Comp: ?, Cost: 3) mod_GT_350(ar_0, ar_1, ar_2) -> Com_1(mod_NE_369(ar_1, ar_0, arityPad)) [ ar_1 - 1 >= 0 /\ 1 <= ar_0 /\ 1 <= ar_1 /\ 0 < ar_0 ]
(Comp: ?, Cost: 4) mod_GT_350(ar_0, ar_1, ar_2) -> Com_1(gcd_Load_463(0, ar_0, arityPad)) [ ar_1 - 1 >= 0 /\ 1 <= ar_1 /\ ar_0 <= -1 /\ ar_0 <= 0 ]
(Comp: ?, Cost: 3) gcd_Load_463(ar_0, ar_1, ar_2) -> Com_1(gcd_Load_314(ar_1, ar_0, arityPad)) [ ar_0 >= 0 /\ 0 >= 0 ]
(Comp: ?, Cost: 2) mod_LE_338(ar_0, ar_1, ar_2) -> Com_1(mod_GT_350(ar_1, ar_0, arityPad)) [ 1 <= ar_0 /\ 0 < ar_0 ]
(Comp: ?, Cost: 4) mod_LE_338(ar_0, ar_1, ar_2) -> Com_1(gcd_Load_463(0, ar_1, arityPad)) [ ar_0 <= 0 ]
(Comp: ?, Cost: 8) gcd_Load_314(ar_0, ar_1, ar_2) -> Com_1(mod_LE_338(ar_0, ar_1, arityPad)) [ 0 < ar_1 ]
(Comp: 1, Cost: 8) gcd_Load_314(ar_0, ar_1, ar_2) -> Com_1(mod_LE_338(ar_0, ar_1, arityPad)) [ ar_1 < 0 ]
(Comp: 1, Cost: 15) koat_start(ar_0, ar_1, ar_2) -> Com_1(gcd_Load_314(ar_0, ar_1, arityPad)) [ 0 <= 0 /\ static'1 <= static''' + 1 /\ 0 <= static''' /\ static''' <= ar_2 + 2 /\ 0 <= ar_2 /\ 0 <= static'1 ]
start location: koat_start
leaf cost: 0

A polynomial rank function with
Pol(mod_NE_369) = 3
Pol(mod_Load_470) = 3
Pol(gcd_Store_509) = 4*V_1 + 2
Pol(mod_LE_475) = 3
Pol(mod_LE_338) = 3
Pol(mod_GT_350) = 3
Pol(gcd_Load_463) = 4*V_1 + 1
Pol(gcd_Load_314) = 4*V_2
and size complexities
S("koat_start(ar_0, ar_1, ar_2) -> Com_1(gcd_Load_314(ar_0, ar_1, arityPad)) [ 0 <= 0 /\\ static'1 <= static''' + 1 /\\ 0 <= static''' /\\ static''' <= ar_2 + 2 /\\ 0 <= ar_2 /\\ 0 <= static'1 ]", 0-0) = ar_0
S("koat_start(ar_0, ar_1, ar_2) -> Com_1(gcd_Load_314(ar_0, ar_1, arityPad)) [ 0 <= 0 /\\ static'1 <= static''' + 1 /\\ 0 <= static''' /\\ static''' <= ar_2 + 2 /\\ 0 <= ar_2 /\\ 0 <= static'1 ]", 0-1) = ar_1
S("koat_start(ar_0, ar_1, ar_2) -> Com_1(gcd_Load_314(ar_0, ar_1, arityPad)) [ 0 <= 0 /\\ static'1 <= static''' + 1 /\\ 0 <= static''' /\\ static''' <= ar_2 + 2 /\\ 0 <= ar_2 /\\ 0 <= static'1 ]", 0-2) = ?
S("gcd_Load_314(ar_0, ar_1, ar_2) -> Com_1(mod_LE_338(ar_0, ar_1, arityPad)) [ ar_1 < 0 ]", 0-0) = ar_0
S("gcd_Load_314(ar_0, ar_1, ar_2) -> Com_1(mod_LE_338(ar_0, ar_1, arityPad)) [ ar_1 < 0 ]", 0-1) = ar_1
S("gcd_Load_314(ar_0, ar_1, ar_2) -> Com_1(mod_LE_338(ar_0, ar_1, arityPad)) [ ar_1 < 0 ]", 0-2) = ?
S("gcd_Load_314(ar_0, ar_1, ar_2) -> Com_1(mod_LE_338(ar_0, ar_1, arityPad)) [ 0 < ar_1 ]", 0-0) = ar_0 + ar_1
S("gcd_Load_314(ar_0, ar_1, ar_2) -> Com_1(mod_LE_338(ar_0, ar_1, arityPad)) [ 0 < ar_1 ]", 0-1) = ar_1
S("gcd_Load_314(ar_0, ar_1, ar_2) -> Com_1(mod_LE_338(ar_0, ar_1, arityPad)) [ 0 < ar_1 ]", 0-2) = ?
S("mod_LE_338(ar_0, ar_1, ar_2) -> Com_1(gcd_Load_463(0, ar_1, arityPad)) [ ar_0 <= 0 ]", 0-0) = 0
S("mod_LE_338(ar_0, ar_1, ar_2) -> Com_1(gcd_Load_463(0, ar_1, arityPad)) [ ar_0 <= 0 ]", 0-1) = ar_1
S("mod_LE_338(ar_0, ar_1, ar_2) -> Com_1(gcd_Load_463(0, ar_1, arityPad)) [ ar_0 <= 0 ]", 0-2) = ?
S("mod_LE_338(ar_0, ar_1, ar_2) -> Com_1(mod_GT_350(ar_1, ar_0, arityPad)) [ 1 <= ar_0 /\\ 0 < ar_0 ]", 0-0) = ar_0 + ar_1
S("mod_LE_338(ar_0, ar_1, ar_2) -> Com_1(mod_GT_350(ar_1, ar_0, arityPad)) [ 1 <= ar_0 /\\ 0 < ar_0 ]", 0-1) = ar_0 + ar_1
S("mod_LE_338(ar_0, ar_1, ar_2) -> Com_1(mod_GT_350(ar_1, ar_0, arityPad)) [ 1 <= ar_0 /\\ 0 < ar_0 ]", 0-2) = ?
S("gcd_Load_463(ar_0, ar_1, ar_2) -> Com_1(gcd_Load_314(ar_1, ar_0, arityPad)) [ ar_0 >= 0 /\\ 0 >= 0 ]", 0-0) = ar_0 + ar_1
S("gcd_Load_463(ar_0, ar_1, ar_2) -> Com_1(gcd_Load_314(ar_1, ar_0, arityPad)) [ ar_0 >= 0 /\\ 0 >= 0 ]", 0-1) = 0
S("gcd_Load_463(ar_0, ar_1, ar_2) -> Com_1(gcd_Load_314(ar_1, ar_0, arityPad)) [ ar_0 >= 0 /\\ 0 >= 0 ]", 0-2) = ?
S("mod_GT_350(ar_0, ar_1, ar_2) -> Com_1(gcd_Load_463(0, ar_0, arityPad)) [ ar_1 - 1 >= 0 /\\ 1 <= ar_1 /\\ ar_0 <= -1 /\\ ar_0 <= 0 ]", 0-0) = 0
S("mod_GT_350(ar_0, ar_1, ar_2) -> Com_1(gcd_Load_463(0, ar_0, arityPad)) [ ar_1 - 1 >= 0 /\\ 1 <= ar_1 /\\ ar_0 <= -1 /\\ ar_0 <= 0 ]", 0-1) = ar_0 + ar_1
S("mod_GT_350(ar_0, ar_1, ar_2) -> Com_1(gcd_Load_463(0, ar_0, arityPad)) [ ar_1 - 1 >= 0 /\\ 1 <= ar_1 /\\ ar_0 <= -1 /\\ ar_0 <= 0 ]", 0-2) = ?
S("mod_GT_350(ar_0, ar_1, ar_2) -> Com_1(mod_NE_369(ar_1, ar_0, arityPad)) [ ar_1 - 1 >= 0 /\\ 1 <= ar_0 /\\ 1 <= ar_1 /\\ 0 < ar_0 ]", 0-0) = ar_0 + ar_1
S("mod_GT_350(ar_0, ar_1, ar_2) -> Com_1(mod_NE_369(ar_1, ar_0, arityPad)) [ ar_1 - 1 >= 0 /\\ 1 <= ar_0 /\\ 1 <= ar_1 /\\ 0 < ar_0 ]", 0-1) = ar_0 + ar_1
S("mod_GT_350(ar_0, ar_1, ar_2) -> Com_1(mod_NE_369(ar_1, ar_0, arityPad)) [ ar_1 - 1 >= 0 /\\ 1 <= ar_0 /\\ 1 <= ar_1 /\\ 0 < ar_0 ]", 0-2) = ?
S("mod_NE_369(ar_0, ar_1, ar_2) -> Com_1(gcd_Store_509(0, ar_0, arityPad)) [ ar_1 - 1 >= 0 /\\ ar_0 + ar_1 - 2 >= 0 /\\ ar_0 - 1 >= 0 /\\ 1 <= ar_0 /\\ ar_1 = ar_0 ]", 0-0) = 0
S("mod_NE_369(ar_0, ar_1, ar_2) -> Com_1(gcd_Store_509(0, ar_0, arityPad)) [ ar_1 - 1 >= 0 /\\ ar_0 + ar_1 - 2 >= 0 /\\ ar_0 - 1 >= 0 /\\ 1 <= ar_0 /\\ ar_1 = ar_0 ]", 0-1) = ar_0 + ar_1
S("mod_NE_369(ar_0, ar_1, ar_2) -> Com_1(gcd_Store_509(0, ar_0, arityPad)) [ ar_1 - 1 >= 0 /\\ ar_0 + ar_1 - 2 >= 0 /\\ ar_0 - 1 >= 0 /\\ 1 <= ar_0 /\\ ar_1 = ar_0 ]", 0-2) = ?
S("mod_NE_369(ar_0, ar_1, ar_2) -> Com_1(mod_Load_470(ar_0, ar_1, arityPad)) [ ar_1 - 1 >= 0 /\\ ar_0 + ar_1 - 2 >= 0 /\\ ar_0 - 1 >= 0 /\\ ar_0 < ar_1 /\\ 1 <= ar_0 /\\ 1 <= ar_1 ]", 0-0) = ar_0 + ar_1
S("mod_NE_369(ar_0, ar_1, ar_2) -> Com_1(mod_Load_470(ar_0, ar_1, arityPad)) [ ar_1 - 1 >= 0 /\\ ar_0 + ar_1 - 2 >= 0 /\\ ar_0 - 1 >= 0 /\\ ar_0 < ar_1 /\\ 1 <= ar_0 /\\ 1 <= ar_1 ]", 0-1) = ar_0 + ar_1
S("mod_NE_369(ar_0, ar_1, ar_2) -> Com_1(mod_Load_470(ar_0, ar_1, arityPad)) [ ar_1 - 1 >= 0 /\\ ar_0 + ar_1 - 2 >= 0 /\\ ar_0 - 1 >= 0 /\\ ar_0 < ar_1 /\\ 1 <= ar_0 /\\ 1 <= ar_1 ]", 0-2) = ?
S("mod_NE_369(ar_0, ar_1, ar_2) -> Com_1(mod_Load_470(ar_0, ar_1, arityPad)) [ ar_1 - 1 >= 0 /\\ ar_0 + ar_1 - 2 >= 0 /\\ ar_0 - 1 >= 0 /\\ ar_1 < ar_0 /\\ 1 <= ar_0 /\\ 1 <= ar_1 ]", 0-0) = ar_0 + ar_1
S("mod_NE_369(ar_0, ar_1, ar_2) -> Com_1(mod_Load_470(ar_0, ar_1, arityPad)) [ ar_1 - 1 >= 0 /\\ ar_0 + ar_1 - 2 >= 0 /\\ ar_0 - 1 >= 0 /\\ ar_1 < ar_0 /\\ 1 <= ar_0 /\\ 1 <= ar_1 ]", 0-1) = ar_0 + ar_1
S("mod_NE_369(ar_0, ar_1, ar_2) -> Com_1(mod_Load_470(ar_0, ar_1, arityPad)) [ ar_1 - 1 >= 0 /\\ ar_0 + ar_1 - 2 >= 0 /\\ ar_0 - 1 >= 0 /\\ ar_1 < ar_0 /\\ 1 <= ar_0 /\\ 1 <= ar_1 ]", 0-2) = ?
S("gcd_Store_509(ar_0, ar_1, ar_2) -> Com_1(gcd_Load_463(ar_0, ar_1, arityPad)) [ ar_1 - 1 >= 0 /\\ ar_0 + ar_1 - 1 >= 0 /\\ -ar_0 + ar_1 >= 0 /\\ ar_0 >= 0 /\\ 0 >= 0 ]", 0-0) = 0
S("gcd_Store_509(ar_0, ar_1, ar_2) -> Com_1(gcd_Load_463(ar_0, ar_1, arityPad)) [ ar_1 - 1 >= 0 /\\ ar_0 + ar_1 - 1 >= 0 /\\ -ar_0 + ar_1 >= 0 /\\ ar_0 >= 0 /\\ 0 >= 0 ]", 0-1) = ar_0 + ar_1
S("gcd_Store_509(ar_0, ar_1, ar_2) -> Com_1(gcd_Load_463(ar_0, ar_1, arityPad)) [ ar_1 - 1 >= 0 /\\ ar_0 + ar_1 - 1 >= 0 /\\ -ar_0 + ar_1 >= 0 /\\ ar_0 >= 0 /\\ 0 >= 0 ]", 0-2) = ?
S("mod_Load_470(ar_0, ar_1, ar_2) -> Com_1(mod_LE_475(ar_0, ar_1, arityPad)) [ ar_1 - 1 >= 0 /\\ 1 <= ar_0 /\\ 1 <= ar_1 ]", 0-0) = ar_0 + ar_1
S("mod_Load_470(ar_0, ar_1, ar_2) -> Com_1(mod_LE_475(ar_0, ar_1, arityPad)) [ ar_1 - 1 >= 0 /\\ 1 <= ar_0 /\\ 1 <= ar_1 ]", 0-1) = ar_0 + ar_1
S("mod_Load_470(ar_0, ar_1, ar_2) -> Com_1(mod_LE_475(ar_0, ar_1, arityPad)) [ ar_1 - 1 >= 0 /\\ 1 <= ar_0 /\\ 1 <= ar_1 ]", 0-2) = ?
S("mod_LE_475(ar_0, ar_1, ar_2) -> Com_1(mod_Load_470(ar_0 - ar_1, ar_1, arityPad)) [ ar_1 - 1 >= 0 /\\ ar_0 + ar_1 - 2 >= 0 /\\ ar_0 - 1 >= 0 /\\ 2 <= ar_0 /\\ 1 <= i172' /\\ 1 <= ar_1 /\\ 1 <= ar_0 /\\ ar_1 < ar_0 /\\ ar_0 - ar_1 = i172' ]", 0-0) = ar_0 + ar_1
S("mod_LE_475(ar_0, ar_1, ar_2) -> Com_1(mod_Load_470(ar_0 - ar_1, ar_1, arityPad)) [ ar_1 - 1 >= 0 /\\ ar_0 + ar_1 - 2 >= 0 /\\ ar_0 - 1 >= 0 /\\ 2 <= ar_0 /\\ 1 <= i172' /\\ 1 <= ar_1 /\\ 1 <= ar_0 /\\ ar_1 < ar_0 /\\ ar_0 - ar_1 = i172' ]", 0-1) = ar_0 + ar_1
S("mod_LE_475(ar_0, ar_1, ar_2) -> Com_1(mod_Load_470(ar_0 - ar_1, ar_1, arityPad)) [ ar_1 - 1 >= 0 /\\ ar_0 + ar_1 - 2 >= 0 /\\ ar_0 - 1 >= 0 /\\ 2 <= ar_0 /\\ 1 <= i172' /\\ 1 <= ar_1 /\\ 1 <= ar_0 /\\ ar_1 < ar_0 /\\ ar_0 - ar_1 = i172' ]", 0-2) = ?
S("mod_LE_475(ar_0, ar_1, ar_2) -> Com_1(mod_LE_338(ar_1, ar_0, arityPad')) [ ar_1 - 1 >= 0 /\\ ar_0 + ar_1 - 2 >= 0 /\\ ar_0 - 1 >= 0 /\\ 1 <= ar_1 /\\ 1 <= ar_0 /\\ ar_0 <= ar_1 /\\ ar_0 + ar_1 - 1 >= 0 /\\ -ar_0 + ar_1 >= 0 /\\ ar_0 >= 0 /\\ 0 >= 0 /\\ 0 < ar_0 ]", 0-0) = ar_0 + ar_1
S("mod_LE_475(ar_0, ar_1, ar_2) -> Com_1(mod_LE_338(ar_1, ar_0, arityPad')) [ ar_1 - 1 >= 0 /\\ ar_0 + ar_1 - 2 >= 0 /\\ ar_0 - 1 >= 0 /\\ 1 <= ar_1 /\\ 1 <= ar_0 /\\ ar_0 <= ar_1 /\\ ar_0 + ar_1 - 1 >= 0 /\\ -ar_0 + ar_1 >= 0 /\\ ar_0 >= 0 /\\ 0 >= 0 /\\ 0 < ar_0 ]", 0-1) = ar_0 + ar_1
S("mod_LE_475(ar_0, ar_1, ar_2) -> Com_1(mod_LE_338(ar_1, ar_0, arityPad')) [ ar_1 - 1 >= 0 /\\ ar_0 + ar_1 - 2 >= 0 /\\ ar_0 - 1 >= 0 /\\ 1 <= ar_1 /\\ 1 <= ar_0 /\\ ar_0 <= ar_1 /\\ ar_0 + ar_1 - 1 >= 0 /\\ -ar_0 + ar_1 >= 0 /\\ ar_0 >= 0 /\\ 0 >= 0 /\\ 0 < ar_0 ]", 0-2) = ?
orients the transitions
mod_NE_369(ar_0, ar_1, ar_2) -> Com_1(mod_Load_470(ar_0, ar_1, arityPad)) [ ar_1 - 1 >= 0 /\ ar_0 + ar_1 - 2 >= 0 /\ ar_0 - 1 >= 0 /\ ar_1 < ar_0 /\ 1 <= ar_0 /\ 1 <= ar_1 ]
mod_NE_369(ar_0, ar_1, ar_2) -> Com_1(mod_Load_470(ar_0, ar_1, arityPad)) [ ar_1 - 1 >= 0 /\ ar_0 + ar_1 - 2 >= 0 /\ ar_0 - 1 >= 0 /\ ar_0 < ar_1 /\ 1 <= ar_0 /\ 1 <= ar_1 ]
mod_NE_369(ar_0, ar_1, ar_2) -> Com_1(gcd_Store_509(0, ar_0, arityPad)) [ ar_1 - 1 >= 0 /\ ar_0 + ar_1 - 2 >= 0 /\ ar_0 - 1 >= 0 /\ 1 <= ar_0 /\ ar_1 = ar_0 ]
mod_Load_470(ar_0, ar_1, ar_2) -> Com_1(mod_LE_475(ar_0, ar_1, arityPad)) [ ar_1 - 1 >= 0 /\ 1 <= ar_0 /\ 1 <= ar_1 ]
mod_LE_475(ar_0, ar_1, ar_2) -> Com_1(mod_Load_470(ar_0 - ar_1, ar_1, arityPad)) [ ar_1 - 1 >= 0 /\ ar_0 + ar_1 - 2 >= 0 /\ ar_0 - 1 >= 0 /\ 2 <= ar_0 /\ 1 <= i172' /\ 1 <= ar_1 /\ 1 <= ar_0 /\ ar_1 < ar_0 /\ ar_0 - ar_1 = i172' ]
mod_LE_475(ar_0, ar_1, ar_2) -> Com_1(mod_LE_338(ar_1, ar_0, arityPad')) [ ar_1 - 1 >= 0 /\ ar_0 + ar_1 - 2 >= 0 /\ ar_0 - 1 >= 0 /\ 1 <= ar_1 /\ 1 <= ar_0 /\ ar_0 <= ar_1 /\ ar_0 + ar_1 - 1 >= 0 /\ -ar_0 + ar_1 >= 0 /\ ar_0 >= 0 /\ 0 >= 0 /\ 0 < ar_0 ]
mod_LE_338(ar_0, ar_1, ar_2) -> Com_1(mod_GT_350(ar_1, ar_0, arityPad)) [ 1 <= ar_0 /\ 0 < ar_0 ]
mod_LE_338(ar_0, ar_1, ar_2) -> Com_1(gcd_Load_463(0, ar_1, arityPad)) [ ar_0 <= 0 ]
mod_GT_350(ar_0, ar_1, ar_2) -> Com_1(mod_NE_369(ar_1, ar_0, arityPad)) [ ar_1 - 1 >= 0 /\ 1 <= ar_0 /\ 1 <= ar_1 /\ 0 < ar_0 ]
mod_GT_350(ar_0, ar_1, ar_2) -> Com_1(gcd_Load_463(0, ar_0, arityPad)) [ ar_1 - 1 >= 0 /\ 1 <= ar_1 /\ ar_0 <= -1 /\ ar_0 <= 0 ]
gcd_Store_509(ar_0, ar_1, ar_2) -> Com_1(gcd_Load_463(ar_0, ar_1, arityPad)) [ ar_1 - 1 >= 0 /\ ar_0 + ar_1 - 1 >= 0 /\ -ar_0 + ar_1 >= 0 /\ ar_0 >= 0 /\ 0 >= 0 ]
gcd_Load_463(ar_0, ar_1, ar_2) -> Com_1(gcd_Load_314(ar_1, ar_0, arityPad)) [ ar_0 >= 0 /\ 0 >= 0 ]
gcd_Load_314(ar_0, ar_1, ar_2) -> Com_1(mod_LE_338(ar_0, ar_1, arityPad)) [ 0 < ar_1 ]
weakly and the transitions
mod_NE_369(ar_0, ar_1, ar_2) -> Com_1(gcd_Store_509(0, ar_0, arityPad)) [ ar_1 - 1 >= 0 /\ ar_0 + ar_1 - 2 >= 0 /\ ar_0 - 1 >= 0 /\ 1 <= ar_0 /\ ar_1 = ar_0 ]
mod_LE_338(ar_0, ar_1, ar_2) -> Com_1(gcd_Load_463(0, ar_1, arityPad)) [ ar_0 <= 0 ]
mod_GT_350(ar_0, ar_1, ar_2) -> Com_1(gcd_Load_463(0, ar_0, arityPad)) [ ar_1 - 1 >= 0 /\ 1 <= ar_1 /\ ar_0 <= -1 /\ ar_0 <= 0 ]
gcd_Store_509(ar_0, ar_1, ar_2) -> Com_1(gcd_Load_463(ar_0, ar_1, arityPad)) [ ar_1 - 1 >= 0 /\ ar_0 + ar_1 - 1 >= 0 /\ -ar_0 + ar_1 >= 0 /\ ar_0 >= 0 /\ 0 >= 0 ]
gcd_Load_463(ar_0, ar_1, ar_2) -> Com_1(gcd_Load_314(ar_1, ar_0, arityPad)) [ ar_0 >= 0 /\ 0 >= 0 ]
gcd_Load_314(ar_0, ar_1, ar_2) -> Com_1(mod_LE_338(ar_0, ar_1, arityPad)) [ 0 < ar_1 ]
strictly and produces the following problem:
10: T:
(Comp: ?, Cost: 15) mod_LE_475(ar_0, ar_1, ar_2) -> Com_1(mod_LE_338(ar_1, ar_0, arityPad')) [ ar_1 - 1 >= 0 /\ ar_0 + ar_1 - 2 >= 0 /\ ar_0 - 1 >= 0 /\ 1 <= ar_1 /\ 1 <= ar_0 /\ ar_0 <= ar_1 /\ ar_0 + ar_1 - 1 >= 0 /\ -ar_0 + ar_1 >= 0 /\ ar_0 >= 0 /\ 0 >= 0 /\ 0 < ar_0 ]
(Comp: ?, Cost: 6) mod_LE_475(ar_0, ar_1, ar_2) -> Com_1(mod_Load_470(ar_0 - ar_1, ar_1, arityPad)) [ ar_1 - 1 >= 0 /\ ar_0 + ar_1 - 2 >= 0 /\ ar_0 - 1 >= 0 /\ 2 <= ar_0 /\ 1 <= i172' /\ 1 <= ar_1 /\ 1 <= ar_0 /\ ar_1 < ar_0 /\ ar_0 - ar_1 = i172' ]
(Comp: ?, Cost: 2) mod_Load_470(ar_0, ar_1, ar_2) -> Com_1(mod_LE_475(ar_0, ar_1, arityPad)) [ ar_1 - 1 >= 0 /\ 1 <= ar_0 /\ 1 <= ar_1 ]
(Comp: 4*ar_1 + 3, Cost: 1) gcd_Store_509(ar_0, ar_1, ar_2) -> Com_1(gcd_Load_463(ar_0, ar_1, arityPad)) [ ar_1 - 1 >= 0 /\ ar_0 + ar_1 - 1 >= 0 /\ -ar_0 + ar_1 >= 0 /\ ar_0 >= 0 /\ 0 >= 0 ]
(Comp: ?, Cost: 1) mod_NE_369(ar_0, ar_1, ar_2) -> Com_1(mod_Load_470(ar_0, ar_1, arityPad)) [ ar_1 - 1 >= 0 /\ ar_0 + ar_1 - 2 >= 0 /\ ar_0 - 1 >= 0 /\ ar_1 < ar_0 /\ 1 <= ar_0 /\ 1 <= ar_1 ]
(Comp: ?, Cost: 1) mod_NE_369(ar_0, ar_1, ar_2) -> Com_1(mod_Load_470(ar_0, ar_1, arityPad)) [ ar_1 - 1 >= 0 /\ ar_0 + ar_1 - 2 >= 0 /\ ar_0 - 1 >= 0 /\ ar_0 < ar_1 /\ 1 <= ar_0 /\ 1 <= ar_1 ]
(Comp: 4*ar_1 + 3, Cost: 3) mod_NE_369(ar_0, ar_1, ar_2) -> Com_1(gcd_Store_509(0, ar_0, arityPad)) [ ar_1 - 1 >= 0 /\ ar_0 + ar_1 - 2 >= 0 /\ ar_0 - 1 >= 0 /\ 1 <= ar_0 /\ ar_1 = ar_0 ]
(Comp: ?, Cost: 3) mod_GT_350(ar_0, ar_1, ar_2) -> Com_1(mod_NE_369(ar_1, ar_0, arityPad)) [ ar_1 - 1 >= 0 /\ 1 <= ar_0 /\ 1 <= ar_1 /\ 0 < ar_0 ]
(Comp: 4*ar_1 + 3, Cost: 4) mod_GT_350(ar_0, ar_1, ar_2) -> Com_1(gcd_Load_463(0, ar_0, arityPad)) [ ar_1 - 1 >= 0 /\ 1 <= ar_1 /\ ar_0 <= -1 /\ ar_0 <= 0 ]
(Comp: 4*ar_1 + 3, Cost: 3) gcd_Load_463(ar_0, ar_1, ar_2) -> Com_1(gcd_Load_314(ar_1, ar_0, arityPad)) [ ar_0 >= 0 /\ 0 >= 0 ]
(Comp: ?, Cost: 2) mod_LE_338(ar_0, ar_1, ar_2) -> Com_1(mod_GT_350(ar_1, ar_0, arityPad)) [ 1 <= ar_0 /\ 0 < ar_0 ]
(Comp: 4*ar_1 + 3, Cost: 4) mod_LE_338(ar_0, ar_1, ar_2) -> Com_1(gcd_Load_463(0, ar_1, arityPad)) [ ar_0 <= 0 ]
(Comp: 4*ar_1 + 3, Cost: 8) gcd_Load_314(ar_0, ar_1, ar_2) -> Com_1(mod_LE_338(ar_0, ar_1, arityPad)) [ 0 < ar_1 ]
(Comp: 1, Cost: 8) gcd_Load_314(ar_0, ar_1, ar_2) -> Com_1(mod_LE_338(ar_0, ar_1, arityPad)) [ ar_1 < 0 ]
(Comp: 1, Cost: 15) koat_start(ar_0, ar_1, ar_2) -> Com_1(gcd_Load_314(ar_0, ar_1, arityPad)) [ 0 <= 0 /\ static'1 <= static''' + 1 /\ 0 <= static''' /\ static''' <= ar_2 + 2 /\ 0 <= ar_2 /\ 0 <= static'1 ]
start location: koat_start
leaf cost: 0

A polynomial rank function with
Pol(mod_NE_369) = V_1 + V_2
Pol(mod_Load_470) = V_1 + V_2
Pol(mod_LE_475) = V_1 + V_2
Pol(mod_LE_338) = V_1 + V_2
Pol(mod_GT_350) = V_1 + V_2
and size complexities
S("koat_start(ar_0, ar_1, ar_2) -> Com_1(gcd_Load_314(ar_0, ar_1, arityPad)) [ 0 <= 0 /\\ static'1 <= static''' + 1 /\\ 0 <= static''' /\\ static''' <= ar_2 + 2 /\\ 0 <= ar_2 /\\ 0 <= static'1 ]", 0-0) = ar_0
S("koat_start(ar_0, ar_1, ar_2) -> Com_1(gcd_Load_314(ar_0, ar_1, arityPad)) [ 0 <= 0 /\\ static'1 <= static''' + 1 /\\ 0 <= static''' /\\ static''' <= ar_2 + 2 /\\ 0 <= ar_2 /\\ 0 <= static'1 ]", 0-1) = ar_1
S("koat_start(ar_0, ar_1, ar_2) -> Com_1(gcd_Load_314(ar_0, ar_1, arityPad)) [ 0 <= 0 /\\ static'1 <= static''' + 1 /\\ 0 <= static''' /\\ static''' <= ar_2 + 2 /\\ 0 <= ar_2 /\\ 0 <= static'1 ]", 0-2) = ?
S("gcd_Load_314(ar_0, ar_1, ar_2) -> Com_1(mod_LE_338(ar_0, ar_1, arityPad)) [ ar_1 < 0 ]", 0-0) = ar_0
S("gcd_Load_314(ar_0, ar_1, ar_2) -> Com_1(mod_LE_338(ar_0, ar_1, arityPad)) [ ar_1 < 0 ]", 0-1) = ar_1
S("gcd_Load_314(ar_0, ar_1, ar_2) -> Com_1(mod_LE_338(ar_0, ar_1, arityPad)) [ ar_1 < 0 ]", 0-2) = ?
S("gcd_Load_314(ar_0, ar_1, ar_2) -> Com_1(mod_LE_338(ar_0, ar_1, arityPad)) [ 0 < ar_1 ]", 0-0) = ar_0 + ar_1
S("gcd_Load_314(ar_0, ar_1, ar_2) -> Com_1(mod_LE_338(ar_0, ar_1, arityPad)) [ 0 < ar_1 ]", 0-1) = ar_1
S("gcd_Load_314(ar_0, ar_1, ar_2) -> Com_1(mod_LE_338(ar_0, ar_1, arityPad)) [ 0 < ar_1 ]", 0-2) = ?
S("mod_LE_338(ar_0, ar_1, ar_2) -> Com_1(gcd_Load_463(0, ar_1, arityPad)) [ ar_0 <= 0 ]", 0-0) = 0
S("mod_LE_338(ar_0, ar_1, ar_2) -> Com_1(gcd_Load_463(0, ar_1, arityPad)) [ ar_0 <= 0 ]", 0-1) = ar_1
S("mod_LE_338(ar_0, ar_1, ar_2) -> Com_1(gcd_Load_463(0, ar_1, arityPad)) [ ar_0 <= 0 ]", 0-2) = ?
S("mod_LE_338(ar_0, ar_1, ar_2) -> Com_1(mod_GT_350(ar_1, ar_0, arityPad)) [ 1 <= ar_0 /\\ 0 < ar_0 ]", 0-0) = ar_0 + ar_1
S("mod_LE_338(ar_0, ar_1, ar_2) -> Com_1(mod_GT_350(ar_1, ar_0, arityPad)) [ 1 <= ar_0 /\\ 0 < ar_0 ]", 0-1) = ar_0 + ar_1
S("mod_LE_338(ar_0, ar_1, ar_2) -> Com_1(mod_GT_350(ar_1, ar_0, arityPad)) [ 1 <= ar_0 /\\ 0 < ar_0 ]", 0-2) = ?
S("gcd_Load_463(ar_0, ar_1, ar_2) -> Com_1(gcd_Load_314(ar_1, ar_0, arityPad)) [ ar_0 >= 0 /\\ 0 >= 0 ]", 0-0) = ar_0 + ar_1
S("gcd_Load_463(ar_0, ar_1, ar_2) -> Com_1(gcd_Load_314(ar_1, ar_0, arityPad)) [ ar_0 >= 0 /\\ 0 >= 0 ]", 0-1) = 0
S("gcd_Load_463(ar_0, ar_1, ar_2) -> Com_1(gcd_Load_314(ar_1, ar_0, arityPad)) [ ar_0 >= 0 /\\ 0 >= 0 ]", 0-2) = ?
S("mod_GT_350(ar_0, ar_1, ar_2) -> Com_1(gcd_Load_463(0, ar_0, arityPad)) [ ar_1 - 1 >= 0 /\\ 1 <= ar_1 /\\ ar_0 <= -1 /\\ ar_0 <= 0 ]", 0-0) = 0
S("mod_GT_350(ar_0, ar_1, ar_2) -> Com_1(gcd_Load_463(0, ar_0, arityPad)) [ ar_1 - 1 >= 0 /\\ 1 <= ar_1 /\\ ar_0 <= -1 /\\ ar_0 <= 0 ]", 0-1) = ar_0 + ar_1
S("mod_GT_350(ar_0, ar_1, ar_2) -> Com_1(gcd_Load_463(0, ar_0, arityPad)) [ ar_1 - 1 >= 0 /\\ 1 <= ar_1 /\\ ar_0 <= -1 /\\ ar_0 <= 0 ]", 0-2) = ?
S("mod_GT_350(ar_0, ar_1, ar_2) -> Com_1(mod_NE_369(ar_1, ar_0, arityPad)) [ ar_1 - 1 >= 0 /\\ 1 <= ar_0 /\\ 1 <= ar_1 /\\ 0 < ar_0 ]", 0-0) = ar_0 + ar_1
S("mod_GT_350(ar_0, ar_1, ar_2) -> Com_1(mod_NE_369(ar_1, ar_0, arityPad)) [ ar_1 - 1 >= 0 /\\ 1 <= ar_0 /\\ 1 <= ar_1 /\\ 0 < ar_0 ]", 0-1) = ar_0 + ar_1
S("mod_GT_350(ar_0, ar_1, ar_2) -> Com_1(mod_NE_369(ar_1, ar_0, arityPad)) [ ar_1 - 1 >= 0 /\\ 1 <= ar_0 /\\ 1 <= ar_1 /\\ 0 < ar_0 ]", 0-2) = ?
S("mod_NE_369(ar_0, ar_1, ar_2) -> Com_1(gcd_Store_509(0, ar_0, arityPad)) [ ar_1 - 1 >= 0 /\\ ar_0 + ar_1 - 2 >= 0 /\\ ar_0 - 1 >= 0 /\\ 1 <= ar_0 /\\ ar_1 = ar_0 ]", 0-0) = 0
S("mod_NE_369(ar_0, ar_1, ar_2) -> Com_1(gcd_Store_509(0, ar_0, arityPad)) [ ar_1 - 1 >= 0 /\\ ar_0 + ar_1 - 2 >= 0 /\\ ar_0 - 1 >= 0 /\\ 1 <= ar_0 /\\ ar_1 = ar_0 ]", 0-1) = ar_0 + ar_1
S("mod_NE_369(ar_0, ar_1, ar_2) -> Com_1(gcd_Store_509(0, ar_0, arityPad)) [ ar_1 - 1 >= 0 /\\ ar_0 + ar_1 - 2 >= 0 /\\ ar_0 - 1 >= 0 /\\ 1 <= ar_0 /\\ ar_1 = ar_0 ]", 0-2) = ?
S("mod_NE_369(ar_0, ar_1, ar_2) -> Com_1(mod_Load_470(ar_0, ar_1, arityPad)) [ ar_1 - 1 >= 0 /\\ ar_0 + ar_1 - 2 >= 0 /\\ ar_0 - 1 >= 0 /\\ ar_0 < ar_1 /\\ 1 <= ar_0 /\\ 1 <= ar_1 ]", 0-0) = ar_0 + ar_1
S("mod_NE_369(ar_0, ar_1, ar_2) -> Com_1(mod_Load_470(ar_0, ar_1, arityPad)) [ ar_1 - 1 >= 0 /\\ ar_0 + ar_1 - 2 >= 0 /\\ ar_0 - 1 >= 0 /\\ ar_0 < ar_1 /\\ 1 <= ar_0 /\\ 1 <= ar_1 ]", 0-1) = ar_0 + ar_1
S("mod_NE_369(ar_0, ar_1, ar_2) -> Com_1(mod_Load_470(ar_0, ar_1, arityPad)) [ ar_1 - 1 >= 0 /\\ ar_0 + ar_1 - 2 >= 0 /\\ ar_0 - 1 >= 0 /\\ ar_0 < ar_1 /\\ 1 <= ar_0 /\\ 1 <= ar_1 ]", 0-2) = ?
S("mod_NE_369(ar_0, ar_1, ar_2) -> Com_1(mod_Load_470(ar_0, ar_1, arityPad)) [ ar_1 - 1 >= 0 /\\ ar_0 + ar_1 - 2 >= 0 /\\ ar_0 - 1 >= 0 /\\ ar_1 < ar_0 /\\ 1 <= ar_0 /\\ 1 <= ar_1 ]", 0-0) = ar_0 + ar_1
S("mod_NE_369(ar_0, ar_1, ar_2) -> Com_1(mod_Load_470(ar_0, ar_1, arityPad)) [ ar_1 - 1 >= 0 /\\ ar_0 + ar_1 - 2 >= 0 /\\ ar_0 - 1 >= 0 /\\ ar_1 < ar_0 /\\ 1 <= ar_0 /\\ 1 <= ar_1 ]", 0-1) = ar_0 + ar_1
S("mod_NE_369(ar_0, ar_1, ar_2) -> Com_1(mod_Load_470(ar_0, ar_1, arityPad)) [ ar_1 - 1 >= 0 /\\ ar_0 + ar_1 - 2 >= 0 /\\ ar_0 - 1 >= 0 /\\ ar_1 < ar_0 /\\ 1 <= ar_0 /\\ 1 <= ar_1 ]", 0-2) = ?
S("gcd_Store_509(ar_0, ar_1, ar_2) -> Com_1(gcd_Load_463(ar_0, ar_1, arityPad)) [ ar_1 - 1 >= 0 /\\ ar_0 + ar_1 - 1 >= 0 /\\ -ar_0 + ar_1 >= 0 /\\ ar_0 >= 0 /\\ 0 >= 0 ]", 0-0) = 0
S("gcd_Store_509(ar_0, ar_1, ar_2) -> Com_1(gcd_Load_463(ar_0, ar_1, arityPad)) [ ar_1 - 1 >= 0 /\\ ar_0 + ar_1 - 1 >= 0 /\\ -ar_0 + ar_1 >= 0 /\\ ar_0 >= 0 /\\ 0 >= 0 ]", 0-1) = ar_0 + ar_1
S("gcd_Store_509(ar_0, ar_1, ar_2) -> Com_1(gcd_Load_463(ar_0, ar_1, arityPad)) [ ar_1 - 1 >= 0 /\\ ar_0 + ar_1 - 1 >= 0 /\\ -ar_0 + ar_1 >= 0 /\\ ar_0 >= 0 /\\ 0 >= 0 ]", 0-2) = ?
S("mod_Load_470(ar_0, ar_1, ar_2) -> Com_1(mod_LE_475(ar_0, ar_1, arityPad)) [ ar_1 - 1 >= 0 /\\ 1 <= ar_0 /\\ 1 <= ar_1 ]", 0-0) = ar_0 + ar_1
S("mod_Load_470(ar_0, ar_1, ar_2) -> Com_1(mod_LE_475(ar_0, ar_1, arityPad)) [ ar_1 - 1 >= 0 /\\ 1 <= ar_0 /\\ 1 <= ar_1 ]", 0-1) = ar_0 + ar_1
S("mod_Load_470(ar_0, ar_1, ar_2) -> Com_1(mod_LE_475(ar_0, ar_1, arityPad)) [ ar_1 - 1 >= 0 /\\ 1 <= ar_0 /\\ 1 <= ar_1 ]", 0-2) = ?
S("mod_LE_475(ar_0, ar_1, ar_2) -> Com_1(mod_Load_470(ar_0 - ar_1, ar_1, arityPad)) [ ar_1 - 1 >= 0 /\\ ar_0 + ar_1 - 2 >= 0 /\\ ar_0 - 1 >= 0 /\\ 2 <= ar_0 /\\ 1 <= i172' /\\ 1 <= ar_1 /\\ 1 <= ar_0 /\\ ar_1 < ar_0 /\\ ar_0 - ar_1 = i172' ]", 0-0) = ar_0 + ar_1
S("mod_LE_475(ar_0, ar_1, ar_2) -> Com_1(mod_Load_470(ar_0 - ar_1, ar_1, arityPad)) [ ar_1 - 1 >= 0 /\\ ar_0 + ar_1 - 2 >= 0 /\\ ar_0 - 1 >= 0 /\\ 2 <= ar_0 /\\ 1 <= i172' /\\ 1 <= ar_1 /\\ 1 <= ar_0 /\\ ar_1 < ar_0 /\\ ar_0 - ar_1 = i172' ]", 0-1) = ar_0 + ar_1
S("mod_LE_475(ar_0, ar_1, ar_2) -> Com_1(mod_Load_470(ar_0 - ar_1, ar_1, arityPad)) [ ar_1 - 1 >= 0 /\\ ar_0 + ar_1 - 2 >= 0 /\\ ar_0 - 1 >= 0 /\\ 2 <= ar_0 /\\ 1 <= i172' /\\ 1 <= ar_1 /\\ 1 <= ar_0 /\\ ar_1 < ar_0 /\\ ar_0 - ar_1 = i172' ]", 0-2) = ?
S("mod_LE_475(ar_0, ar_1, ar_2) -> Com_1(mod_LE_338(ar_1, ar_0, arityPad')) [ ar_1 - 1 >= 0 /\\ ar_0 + ar_1 - 2 >= 0 /\\ ar_0 - 1 >= 0 /\\ 1 <= ar_1 /\\ 1 <= ar_0 /\\ ar_0 <= ar_1 /\\ ar_0 + ar_1 - 1 >= 0 /\\ -ar_0 + ar_1 >= 0 /\\ ar_0 >= 0 /\\ 0 >= 0 /\\ 0 < ar_0 ]", 0-0) = ar_0 + ar_1
S("mod_LE_475(ar_0, ar_1, ar_2) -> Com_1(mod_LE_338(ar_1, ar_0, arityPad')) [ ar_1 - 1 >= 0 /\\ ar_0 + ar_1 - 2 >= 0 /\\ ar_0 - 1 >= 0 /\\ 1 <= ar_1 /\\ 1 <= ar_0 /\\ ar_0 <= ar_1 /\\ ar_0 + ar_1 - 1 >= 0 /\\ -ar_0 + ar_1 >= 0 /\\ ar_0 >= 0 /\\ 0 >= 0 /\\ 0 < ar_0 ]", 0-1) = ar_0 + ar_1
S("mod_LE_475(ar_0, ar_1, ar_2) -> Com_1(mod_LE_338(ar_1, ar_0, arityPad')) [ ar_1 - 1 >= 0 /\\ ar_0 + ar_1 - 2 >= 0 /\\ ar_0 - 1 >= 0 /\\ 1 <= ar_1 /\\ 1 <= ar_0 /\\ ar_0 <= ar_1 /\\ ar_0 + ar_1 - 1 >= 0 /\\ -ar_0 + ar_1 >= 0 /\\ ar_0 >= 0 /\\ 0 >= 0 /\\ 0 < ar_0 ]", 0-2) = ?
orients the transitions
mod_NE_369(ar_0, ar_1, ar_2) -> Com_1(mod_Load_470(ar_0, ar_1, arityPad)) [ ar_1 - 1 >= 0 /\ ar_0 + ar_1 - 2 >= 0 /\ ar_0 - 1 >= 0 /\ ar_1 < ar_0 /\ 1 <= ar_0 /\ 1 <= ar_1 ]
mod_NE_369(ar_0, ar_1, ar_2) -> Com_1(mod_Load_470(ar_0, ar_1, arityPad)) [ ar_1 - 1 >= 0 /\ ar_0 + ar_1 - 2 >= 0 /\ ar_0 - 1 >= 0 /\ ar_0 < ar_1 /\ 1 <= ar_0 /\ 1 <= ar_1 ]
mod_Load_470(ar_0, ar_1, ar_2) -> Com_1(mod_LE_475(ar_0, ar_1, arityPad)) [ ar_1 - 1 >= 0 /\ 1 <= ar_0 /\ 1 <= ar_1 ]
mod_LE_475(ar_0, ar_1, ar_2) -> Com_1(mod_Load_470(ar_0 - ar_1, ar_1, arityPad)) [ ar_1 - 1 >= 0 /\ ar_0 + ar_1 - 2 >= 0 /\ ar_0 - 1 >= 0 /\ 2 <= ar_0 /\ 1 <= i172' /\ 1 <= ar_1 /\ 1 <= ar_0 /\ ar_1 < ar_0 /\ ar_0 - ar_1 = i172' ]
mod_LE_475(ar_0, ar_1, ar_2) -> Com_1(mod_LE_338(ar_1, ar_0, arityPad')) [ ar_1 - 1 >= 0 /\ ar_0 + ar_1 - 2 >= 0 /\ ar_0 - 1 >= 0 /\ 1 <= ar_1 /\ 1 <= ar_0 /\ ar_0 <= ar_1 /\ ar_0 + ar_1 - 1 >= 0 /\ -ar_0 + ar_1 >= 0 /\ ar_0 >= 0 /\ 0 >= 0 /\ 0 < ar_0 ]
mod_LE_338(ar_0, ar_1, ar_2) -> Com_1(mod_GT_350(ar_1, ar_0, arityPad)) [ 1 <= ar_0 /\ 0 < ar_0 ]
mod_GT_350(ar_0, ar_1, ar_2) -> Com_1(mod_NE_369(ar_1, ar_0, arityPad)) [ ar_1 - 1 >= 0 /\ 1 <= ar_0 /\ 1 <= ar_1 /\ 0 < ar_0 ]
weakly and the transition
mod_LE_475(ar_0, ar_1, ar_2) -> Com_1(mod_Load_470(ar_0 - ar_1, ar_1, arityPad)) [ ar_1 - 1 >= 0 /\ ar_0 + ar_1 - 2 >= 0 /\ ar_0 - 1 >= 0 /\ 2 <= ar_0 /\ 1 <= i172' /\ 1 <= ar_1 /\ 1 <= ar_0 /\ ar_1 < ar_0 /\ ar_0 - ar_1 = i172' ]
strictly and produces the following problem:
11: T:
(Comp: ?, Cost: 15) mod_LE_475(ar_0, ar_1, ar_2) -> Com_1(mod_LE_338(ar_1, ar_0, arityPad')) [ ar_1 - 1 >= 0 /\ ar_0 + ar_1 - 2 >= 0 /\ ar_0 - 1 >= 0 /\ 1 <= ar_1 /\ 1 <= ar_0 /\ ar_0 <= ar_1 /\ ar_0 + ar_1 - 1 >= 0 /\ -ar_0 + ar_1 >= 0 /\ ar_0 >= 0 /\ 0 >= 0 /\ 0 < ar_0 ]
(Comp: 4*ar_0*ar_1 + 8*ar_1^2 + 4*ar_0 + 7*ar_1, Cost: 6) mod_LE_475(ar_0, ar_1, ar_2) -> Com_1(mod_Load_470(ar_0 - ar_1, ar_1, arityPad)) [ ar_1 - 1 >= 0 /\ ar_0 + ar_1 - 2 >= 0 /\ ar_0 - 1 >= 0 /\ 2 <= ar_0 /\ 1 <= i172' /\ 1 <= ar_1 /\ 1 <= ar_0 /\ ar_1 < ar_0 /\ ar_0 - ar_1 = i172' ]
(Comp: ?, Cost: 2) mod_Load_470(ar_0, ar_1, ar_2) -> Com_1(mod_LE_475(ar_0, ar_1, arityPad)) [ ar_1 - 1 >= 0 /\ 1 <= ar_0 /\ 1 <= ar_1 ]
(Comp: 4*ar_1 + 3, Cost: 1) gcd_Store_509(ar_0, ar_1, ar_2) -> Com_1(gcd_Load_463(ar_0, ar_1, arityPad)) [ ar_1 - 1 >= 0 /\ ar_0 + ar_1 - 1 >= 0 /\ -ar_0 + ar_1 >= 0 /\ ar_0 >= 0 /\ 0 >= 0 ]
(Comp: ?, Cost: 1) mod_NE_369(ar_0, ar_1, ar_2) -> Com_1(mod_Load_470(ar_0, ar_1, arityPad)) [ ar_1 - 1 >= 0 /\ ar_0 + ar_1 - 2 >= 0 /\ ar_0 - 1 >= 0 /\ ar_1 < ar_0 /\ 1 <= ar_0 /\ 1 <= ar_1 ]
(Comp: ?, Cost: 1) mod_NE_369(ar_0, ar_1, ar_2) -> Com_1(mod_Load_470(ar_0, ar_1, arityPad)) [ ar_1 - 1 >= 0 /\ ar_0 + ar_1 - 2 >= 0 /\ ar_0 - 1 >= 0 /\ ar_0 < ar_1 /\ 1 <= ar_0 /\ 1 <= ar_1 ]
(Comp: 4*ar_1 + 3, Cost: 3) mod_NE_369(ar_0, ar_1, ar_2) -> Com_1(gcd_Store_509(0, ar_0, arityPad)) [ ar_1 - 1 >= 0 /\ ar_0 + ar_1 - 2 >= 0 /\ ar_0 - 1 >= 0 /\ 1 <= ar_0 /\ ar_1 = ar_0 ]
(Comp: ?, Cost: 3) mod_GT_350(ar_0, ar_1, ar_2) -> Com_1(mod_NE_369(ar_1, ar_0, arityPad)) [ ar_1 - 1 >= 0 /\ 1 <= ar_0 /\ 1 <= ar_1 /\ 0 < ar_0 ]
(Comp: 4*ar_1 + 3, Cost: 4) mod_GT_350(ar_0, ar_1, ar_2) -> Com_1(gcd_Load_463(0, ar_0, arityPad)) [ ar_1 - 1 >= 0 /\ 1 <= ar_1 /\ ar_0 <= -1 /\ ar_0 <= 0 ]
(Comp: 4*ar_1 + 3, Cost: 3) gcd_Load_463(ar_0, ar_1, ar_2) -> Com_1(gcd_Load_314(ar_1, ar_0, arityPad)) [ ar_0 >= 0 /\ 0 >= 0 ]
(Comp: ?, Cost: 2) mod_LE_338(ar_0, ar_1, ar_2) -> Com_1(mod_GT_350(ar_1, ar_0, arityPad)) [ 1 <= ar_0 /\ 0 < ar_0 ]
(Comp: 4*ar_1 + 3, Cost: 4) mod_LE_338(ar_0, ar_1, ar_2) -> Com_1(gcd_Load_463(0, ar_1, arityPad)) [ ar_0 <= 0 ]
(Comp: 4*ar_1 + 3, Cost: 8) gcd_Load_314(ar_0, ar_1, ar_2) -> Com_1(mod_LE_338(ar_0, ar_1, arityPad)) [ 0 < ar_1 ]
(Comp: 1, Cost: 8) gcd_Load_314(ar_0, ar_1, ar_2) -> Com_1(mod_LE_338(ar_0, ar_1, arityPad)) [ ar_1 < 0 ]
(Comp: 1, Cost: 15) koat_start(ar_0, ar_1, ar_2) -> Com_1(gcd_Load_314(ar_0, ar_1, arityPad)) [ 0 <= 0 /\ static'1 <= static''' + 1 /\ 0 <= static''' /\ static''' <= ar_2 + 2 /\ 0 <= ar_2 /\ 0 <= static'1 ]
start location: koat_start
leaf cost: 0

By chaining the transition mod_LE_475(ar_0, ar_1, ar_2) -> Com_1(mod_LE_338(ar_1, ar_0, arityPad')) [ ar_1 - 1 >= 0 /\ ar_0 + ar_1 - 2 >= 0 /\ ar_0 - 1 >= 0 /\ 1 <= ar_1 /\ 1 <= ar_0 /\ ar_0 <= ar_1 /\ ar_0 + ar_1 - 1 >= 0 /\ -ar_0 + ar_1 >= 0 /\ ar_0 >= 0 /\ 0 >= 0 /\ 0 < ar_0 ] with all transitions in problem 11, the following new transition is obtained:
mod_LE_475(ar_0, ar_1, ar_2) -> Com_1(mod_GT_350(ar_0, ar_1, arityPad)) [ ar_1 - 1 >= 0 /\ ar_0 + ar_1 - 2 >= 0 /\ ar_0 - 1 >= 0 /\ 1 <= ar_1 /\ 1 <= ar_0 /\ ar_0 <= ar_1 /\ ar_0 + ar_1 - 1 >= 0 /\ -ar_0 + ar_1 >= 0 /\ ar_0 >= 0 /\ 0 >= 0 /\ 0 < ar_0 /\ 0 < ar_1 ]
We thus obtain the following problem:
12: T:
(Comp: ?, Cost: 17) mod_LE_475(ar_0, ar_1, ar_2) -> Com_1(mod_GT_350(ar_0, ar_1, arityPad)) [ ar_1 - 1 >= 0 /\ ar_0 + ar_1 - 2 >= 0 /\ ar_0 - 1 >= 0 /\ 1 <= ar_1 /\ 1 <= ar_0 /\ ar_0 <= ar_1 /\ ar_0 + ar_1 - 1 >= 0 /\ -ar_0 + ar_1 >= 0 /\ ar_0 >= 0 /\ 0 >= 0 /\ 0 < ar_0 /\ 0 < ar_1 ]
(Comp: 4*ar_0*ar_1 + 8*ar_1^2 + 4*ar_0 + 7*ar_1, Cost: 6) mod_LE_475(ar_0, ar_1, ar_2) -> Com_1(mod_Load_470(ar_0 - ar_1, ar_1, arityPad)) [ ar_1 - 1 >= 0 /\ ar_0 + ar_1 - 2 >= 0 /\ ar_0 - 1 >= 0 /\ 2 <= ar_0 /\ 1 <= i172' /\ 1 <= ar_1 /\ 1 <= ar_0 /\ ar_1 < ar_0 /\ ar_0 - ar_1 = i172' ]
(Comp: ?, Cost: 2) mod_Load_470(ar_0, ar_1, ar_2) -> Com_1(mod_LE_475(ar_0, ar_1, arityPad)) [ ar_1 - 1 >= 0 /\ 1 <= ar_0 /\ 1 <= ar_1 ]
(Comp: 4*ar_1 + 3, Cost: 1) gcd_Store_509(ar_0, ar_1, ar_2) -> Com_1(gcd_Load_463(ar_0, ar_1, arityPad)) [ ar_1 - 1 >= 0 /\ ar_0 + ar_1 - 1 >= 0 /\ -ar_0 + ar_1 >= 0 /\ ar_0 >= 0 /\ 0 >= 0 ]
(Comp: ?, Cost: 1) mod_NE_369(ar_0, ar_1, ar_2) -> Com_1(mod_Load_470(ar_0, ar_1, arityPad)) [ ar_1 - 1 >= 0 /\ ar_0 + ar_1 - 2 >= 0 /\ ar_0 - 1 >= 0 /\ ar_1 < ar_0 /\ 1 <= ar_0 /\ 1 <= ar_1 ]
(Comp: ?, Cost: 1) mod_NE_369(ar_0, ar_1, ar_2) -> Com_1(mod_Load_470(ar_0, ar_1, arityPad)) [ ar_1 - 1 >= 0 /\ ar_0 + ar_1 - 2 >= 0 /\ ar_0 - 1 >= 0 /\ ar_0 < ar_1 /\ 1 <= ar_0 /\ 1 <= ar_1 ]
(Comp: 4*ar_1 + 3, Cost: 3) mod_NE_369(ar_0, ar_1, ar_2) -> Com_1(gcd_Store_509(0, ar_0, arityPad)) [ ar_1 - 1 >= 0 /\ ar_0 + ar_1 - 2 >= 0 /\ ar_0 - 1 >= 0 /\ 1 <= ar_0 /\ ar_1 = ar_0 ]
(Comp: ?, Cost: 3) mod_GT_350(ar_0, ar_1, ar_2) -> Com_1(mod_NE_369(ar_1, ar_0, arityPad)) [ ar_1 - 1 >= 0 /\ 1 <= ar_0 /\ 1 <= ar_1 /\ 0 < ar_0 ]
(Comp: 4*ar_1 + 3, Cost: 4) mod_GT_350(ar_0, ar_1, ar_2) -> Com_1(gcd_Load_463(0, ar_0, arityPad)) [ ar_1 - 1 >= 0 /\ 1 <= ar_1 /\ ar_0 <= -1 /\ ar_0 <= 0 ]
(Comp: 4*ar_1 + 3, Cost: 3) gcd_Load_463(ar_0, ar_1, ar_2) -> Com_1(gcd_Load_314(ar_1, ar_0, arityPad)) [ ar_0 >= 0 /\ 0 >= 0 ]
(Comp: ?, Cost: 2) mod_LE_338(ar_0, ar_1, ar_2) -> Com_1(mod_GT_350(ar_1, ar_0, arityPad)) [ 1 <= ar_0 /\ 0 < ar_0 ]
(Comp: 4*ar_1 + 3, Cost: 4) mod_LE_338(ar_0, ar_1, ar_2) -> Com_1(gcd_Load_463(0, ar_1, arityPad)) [ ar_0 <= 0 ]
(Comp: 4*ar_1 + 3, Cost: 8) gcd_Load_314(ar_0, ar_1, ar_2) -> Com_1(mod_LE_338(ar_0, ar_1, arityPad)) [ 0 < ar_1 ]
(Comp: 1, Cost: 8) gcd_Load_314(ar_0, ar_1, ar_2) -> Com_1(mod_LE_338(ar_0, ar_1, arityPad)) [ ar_1 < 0 ]
(Comp: 1, Cost: 15) koat_start(ar_0, ar_1, ar_2) -> Com_1(gcd_Load_314(ar_0, ar_1, arityPad)) [ 0 <= 0 /\ static'1 <= static''' + 1 /\ 0 <= static''' /\ static''' <= ar_2 + 2 /\ 0 <= ar_2 /\ 0 <= static'1 ]
start location: koat_start
leaf cost: 0

Repeatedly propagating knowledge in problem 12 produces the following problem:
13: T:
(Comp: ?, Cost: 17) mod_LE_475(ar_0, ar_1, ar_2) -> Com_1(mod_GT_350(ar_0, ar_1, arityPad)) [ ar_1 - 1 >= 0 /\ ar_0 + ar_1 - 2 >= 0 /\ ar_0 - 1 >= 0 /\ 1 <= ar_1 /\ 1 <= ar_0 /\ ar_0 <= ar_1 /\ ar_0 + ar_1 - 1 >= 0 /\ -ar_0 + ar_1 >= 0 /\ ar_0 >= 0 /\ 0 >= 0 /\ 0 < ar_0 /\ 0 < ar_1 ]
(Comp: 4*ar_0*ar_1 + 8*ar_1^2 + 4*ar_0 + 7*ar_1, Cost: 6) mod_LE_475(ar_0, ar_1, ar_2) -> Com_1(mod_Load_470(ar_0 - ar_1, ar_1, arityPad)) [ ar_1 - 1 >= 0 /\ ar_0 + ar_1 - 2 >= 0 /\ ar_0 - 1 >= 0 /\ 2 <= ar_0 /\ 1 <= i172' /\ 1 <= ar_1 /\ 1 <= ar_0 /\ ar_1 < ar_0 /\ ar_0 - ar_1 = i172' ]
(Comp: ?, Cost: 2) mod_Load_470(ar_0, ar_1, ar_2) -> Com_1(mod_LE_475(ar_0, ar_1, arityPad)) [ ar_1 - 1 >= 0 /\ 1 <= ar_0 /\ 1 <= ar_1 ]
(Comp: 4*ar_1 + 3, Cost: 1) gcd_Store_509(ar_0, ar_1, ar_2) -> Com_1(gcd_Load_463(ar_0, ar_1, arityPad)) [ ar_1 - 1 >= 0 /\ ar_0 + ar_1 - 1 >= 0 /\ -ar_0 + ar_1 >= 0 /\ ar_0 >= 0 /\ 0 >= 0 ]
(Comp: ?, Cost: 1) mod_NE_369(ar_0, ar_1, ar_2) -> Com_1(mod_Load_470(ar_0, ar_1, arityPad)) [ ar_1 - 1 >= 0 /\ ar_0 + ar_1 - 2 >= 0 /\ ar_0 - 1 >= 0 /\ ar_1 < ar_0 /\ 1 <= ar_0 /\ 1 <= ar_1 ]
(Comp: ?, Cost: 1) mod_NE_369(ar_0, ar_1, ar_2) -> Com_1(mod_Load_470(ar_0, ar_1, arityPad)) [ ar_1 - 1 >= 0 /\ ar_0 + ar_1 - 2 >= 0 /\ ar_0 - 1 >= 0 /\ ar_0 < ar_1 /\ 1 <= ar_0 /\ 1 <= ar_1 ]
(Comp: 4*ar_1 + 3, Cost: 3) mod_NE_369(ar_0, ar_1, ar_2) -> Com_1(gcd_Store_509(0, ar_0, arityPad)) [ ar_1 - 1 >= 0 /\ ar_0 + ar_1 - 2 >= 0 /\ ar_0 - 1 >= 0 /\ 1 <= ar_0 /\ ar_1 = ar_0 ]
(Comp: ?, Cost: 3) mod_GT_350(ar_0, ar_1, ar_2) -> Com_1(mod_NE_369(ar_1, ar_0, arityPad)) [ ar_1 - 1 >= 0 /\ 1 <= ar_0 /\ 1 <= ar_1 /\ 0 < ar_0 ]
(Comp: 4*ar_1 + 3, Cost: 4) mod_GT_350(ar_0, ar_1, ar_2) -> Com_1(gcd_Load_463(0, ar_0, arityPad)) [ ar_1 - 1 >= 0 /\ 1 <= ar_1 /\ ar_0 <= -1 /\ ar_0 <= 0 ]
(Comp: 4*ar_1 + 3, Cost: 3) gcd_Load_463(ar_0, ar_1, ar_2) -> Com_1(gcd_Load_314(ar_1, ar_0, arityPad)) [ ar_0 >= 0 /\ 0 >= 0 ]
(Comp: 4*ar_1 + 4, Cost: 2) mod_LE_338(ar_0, ar_1, ar_2) -> Com_1(mod_GT_350(ar_1, ar_0, arityPad)) [ 1 <= ar_0 /\ 0 < ar_0 ]
(Comp: 4*ar_1 + 3, Cost: 4) mod_LE_338(ar_0, ar_1, ar_2) -> Com_1(gcd_Load_463(0, ar_1, arityPad)) [ ar_0 <= 0 ]
(Comp: 4*ar_1 + 3, Cost: 8) gcd_Load_314(ar_0, ar_1, ar_2) -> Com_1(mod_LE_338(ar_0, ar_1, arityPad)) [ 0 < ar_1 ]
(Comp: 1, Cost: 8) gcd_Load_314(ar_0, ar_1, ar_2) -> Com_1(mod_LE_338(ar_0, ar_1, arityPad)) [ ar_1 < 0 ]
(Comp: 1, Cost: 15) koat_start(ar_0, ar_1, ar_2) -> Com_1(gcd_Load_314(ar_0, ar_1, arityPad)) [ 0 <= 0 /\ static'1 <= static''' + 1 /\ 0 <= static''' /\ static''' <= ar_2 + 2 /\ 0 <= ar_2 /\ 0 <= static'1 ]
start location: koat_start
leaf cost: 0

By chaining the transition mod_LE_475(ar_0, ar_1, ar_2) -> Com_1(mod_GT_350(ar_0, ar_1, arityPad)) [ ar_1 - 1 >= 0 /\ ar_0 + ar_1 - 2 >= 0 /\ ar_0 - 1 >= 0 /\ 1 <= ar_1 /\ 1 <= ar_0 /\ ar_0 <= ar_1 /\ ar_0 + ar_1 - 1 >= 0 /\ -ar_0 + ar_1 >= 0 /\ ar_0 >= 0 /\ 0 >= 0 /\ 0 < ar_0 /\ 0 < ar_1 ] with all transitions in problem 13, the following new transition is obtained:
mod_LE_475(ar_0, ar_1, ar_2) -> Com_1(mod_NE_369(ar_1, ar_0, arityPad')) [ ar_1 - 1 >= 0 /\ ar_0 + ar_1 - 2 >= 0 /\ ar_0 - 1 >= 0 /\ 1 <= ar_1 /\ 1 <= ar_0 /\ ar_0 <= ar_1 /\ ar_0 + ar_1 - 1 >= 0 /\ -ar_0 + ar_1 >= 0 /\ ar_0 >= 0 /\ 0 >= 0 /\ 0 < ar_0 /\ 0 < ar_1 ]
We thus obtain the following problem:
14: T:
(Comp: ?, Cost: 20) mod_LE_475(ar_0, ar_1, ar_2) -> Com_1(mod_NE_369(ar_1, ar_0, arityPad')) [ ar_1 - 1 >= 0 /\ ar_0 + ar_1 - 2 >= 0 /\ ar_0 - 1 >= 0 /\ 1 <= ar_1 /\ 1 <= ar_0 /\ ar_0 <= ar_1 /\ ar_0 + ar_1 - 1 >= 0 /\ -ar_0 + ar_1 >= 0 /\ ar_0 >= 0 /\ 0 >= 0 /\ 0 < ar_0 /\ 0 < ar_1 ]
(Comp: 4*ar_0*ar_1 + 8*ar_1^2 + 4*ar_0 + 7*ar_1, Cost: 6) mod_LE_475(ar_0, ar_1, ar_2) -> Com_1(mod_Load_470(ar_0 - ar_1, ar_1, arityPad)) [ ar_1 - 1 >= 0 /\ ar_0 + ar_1 - 2 >= 0 /\ ar_0 - 1 >= 0 /\ 2 <= ar_0 /\ 1 <= i172' /\ 1 <= ar_1 /\ 1 <= ar_0 /\ ar_1 < ar_0 /\ ar_0 - ar_1 = i172' ]
(Comp: ?, Cost: 2) mod_Load_470(ar_0, ar_1, ar_2) -> Com_1(mod_LE_475(ar_0, ar_1, arityPad)) [ ar_1 - 1 >= 0 /\ 1 <= ar_0 /\ 1 <= ar_1 ]
(Comp: 4*ar_1 + 3, Cost: 1) gcd_Store_509(ar_0, ar_1, ar_2) -> Com_1(gcd_Load_463(ar_0, ar_1, arityPad)) [ ar_1 - 1 >= 0 /\ ar_0 + ar_1 - 1 >= 0 /\ -ar_0 + ar_1 >= 0 /\ ar_0 >= 0 /\ 0 >= 0 ]
(Comp: ?, Cost: 1) mod_NE_369(ar_0, ar_1, ar_2) -> Com_1(mod_Load_470(ar_0, ar_1, arityPad)) [ ar_1 - 1 >= 0 /\ ar_0 + ar_1 - 2 >= 0 /\ ar_0 - 1 >= 0 /\ ar_1 < ar_0 /\ 1 <= ar_0 /\ 1 <= ar_1 ]
(Comp: ?, Cost: 1) mod_NE_369(ar_0, ar_1, ar_2) -> Com_1(mod_Load_470(ar_0, ar_1, arityPad)) [ ar_1 - 1 >= 0 /\ ar_0 + ar_1 - 2 >= 0 /\ ar_0 - 1 >= 0 /\ ar_0 < ar_1 /\ 1 <= ar_0 /\ 1 <= ar_1 ]
(Comp: 4*ar_1 + 3, Cost: 3) mod_NE_369(ar_0, ar_1, ar_2) -> Com_1(gcd_Store_509(0, ar_0, arityPad)) [ ar_1 - 1 >= 0 /\ ar_0 + ar_1 - 2 >= 0 /\ ar_0 - 1 >= 0 /\ 1 <= ar_0 /\ ar_1 = ar_0 ]
(Comp: ?, Cost: 3) mod_GT_350(ar_0, ar_1, ar_2) -> Com_1(mod_NE_369(ar_1, ar_0, arityPad)) [ ar_1 - 1 >= 0 /\ 1 <= ar_0 /\ 1 <= ar_1 /\ 0 < ar_0 ]
(Comp: 4*ar_1 + 3, Cost: 4) mod_GT_350(ar_0, ar_1, ar_2) -> Com_1(gcd_Load_463(0, ar_0, arityPad)) [ ar_1 - 1 >= 0 /\ 1 <= ar_1 /\ ar_0 <= -1 /\ ar_0 <= 0 ]
(Comp: 4*ar_1 + 3, Cost: 3) gcd_Load_463(ar_0, ar_1, ar_2) -> Com_1(gcd_Load_314(ar_1, ar_0, arityPad)) [ ar_0 >= 0 /\ 0 >= 0 ]
(Comp: 4*ar_1 + 4, Cost: 2) mod_LE_338(ar_0, ar_1, ar_2) -> Com_1(mod_GT_350(ar_1, ar_0, arityPad)) [ 1 <= ar_0 /\ 0 < ar_0 ]
(Comp: 4*ar_1 + 3, Cost: 4) mod_LE_338(ar_0, ar_1, ar_2) -> Com_1(gcd_Load_463(0, ar_1, arityPad)) [ ar_0 <= 0 ]
(Comp: 4*ar_1 + 3, Cost: 8) gcd_Load_314(ar_0, ar_1, ar_2) -> Com_1(mod_LE_338(ar_0, ar_1, arityPad)) [ 0 < ar_1 ]
(Comp: 1, Cost: 8) gcd_Load_314(ar_0, ar_1, ar_2) -> Com_1(mod_LE_338(ar_0, ar_1, arityPad)) [ ar_1 < 0 ]
(Comp: 1, Cost: 15) koat_start(ar_0, ar_1, ar_2) -> Com_1(gcd_Load_314(ar_0, ar_1, arityPad)) [ 0 <= 0 /\ static'1 <= static''' + 1 /\ 0 <= static''' /\ static''' <= ar_2 + 2 /\ 0 <= ar_2 /\ 0 <= static'1 ]
start location: koat_start
leaf cost: 0

Repeatedly propagating knowledge in problem 14 produces the following problem:
15: T:
(Comp: ?, Cost: 20) mod_LE_475(ar_0, ar_1, ar_2) -> Com_1(mod_NE_369(ar_1, ar_0, arityPad')) [ ar_1 - 1 >= 0 /\ ar_0 + ar_1 - 2 >= 0 /\ ar_0 - 1 >= 0 /\ 1 <= ar_1 /\ 1 <= ar_0 /\ ar_0 <= ar_1 /\ ar_0 + ar_1 - 1 >= 0 /\ -ar_0 + ar_1 >= 0 /\ ar_0 >= 0 /\ 0 >= 0 /\ 0 < ar_0 /\ 0 < ar_1 ]
(Comp: 4*ar_0*ar_1 + 8*ar_1^2 + 4*ar_0 + 7*ar_1, Cost: 6) mod_LE_475(ar_0, ar_1, ar_2) -> Com_1(mod_Load_470(ar_0 - ar_1, ar_1, arityPad)) [ ar_1 - 1 >= 0 /\ ar_0 + ar_1 - 2 >= 0 /\ ar_0 - 1 >= 0 /\ 2 <= ar_0 /\ 1 <= i172' /\ 1 <= ar_1 /\ 1 <= ar_0 /\ ar_1 < ar_0 /\ ar_0 - ar_1 = i172' ]
(Comp: ?, Cost: 2) mod_Load_470(ar_0, ar_1, ar_2) -> Com_1(mod_LE_475(ar_0, ar_1, arityPad)) [ ar_1 - 1 >= 0 /\ 1 <= ar_0 /\ 1 <= ar_1 ]
(Comp: 4*ar_1 + 3, Cost: 1) gcd_Store_509(ar_0, ar_1, ar_2) -> Com_1(gcd_Load_463(ar_0, ar_1, arityPad)) [ ar_1 - 1 >= 0 /\ ar_0 + ar_1 - 1 >= 0 /\ -ar_0 + ar_1 >= 0 /\ ar_0 >= 0 /\ 0 >= 0 ]
(Comp: ?, Cost: 1) mod_NE_369(ar_0, ar_1, ar_2) -> Com_1(mod_Load_470(ar_0, ar_1, arityPad)) [ ar_1 - 1 >= 0 /\ ar_0 + ar_1 - 2 >= 0 /\ ar_0 - 1 >= 0 /\ ar_1 < ar_0 /\ 1 <= ar_0 /\ 1 <= ar_1 ]
(Comp: 4*ar_1 + 4, Cost: 1) mod_NE_369(ar_0, ar_1, ar_2) -> Com_1(mod_Load_470(ar_0, ar_1, arityPad)) [ ar_1 - 1 >= 0 /\ ar_0 + ar_1 - 2 >= 0 /\ ar_0 - 1 >= 0 /\ ar_0 < ar_1 /\ 1 <= ar_0 /\ 1 <= ar_1 ]
(Comp: 4*ar_1 + 3, Cost: 3) mod_NE_369(ar_0, ar_1, ar_2) -> Com_1(gcd_Store_509(0, ar_0, arityPad)) [ ar_1 - 1 >= 0 /\ ar_0 + ar_1 - 2 >= 0 /\ ar_0 - 1 >= 0 /\ 1 <= ar_0 /\ ar_1 = ar_0 ]
(Comp: 4*ar_1 + 4, Cost: 3) mod_GT_350(ar_0, ar_1, ar_2) -> Com_1(mod_NE_369(ar_1, ar_0, arityPad)) [ ar_1 - 1 >= 0 /\ 1 <= ar_0 /\ 1 <= ar_1 /\ 0 < ar_0 ]
(Comp: 4*ar_1 + 3, Cost: 4) mod_GT_350(ar_0, ar_1, ar_2) -> Com_1(gcd_Load_463(0, ar_0, arityPad)) [ ar_1 - 1 >= 0 /\ 1 <= ar_1 /\ ar_0 <= -1 /\ ar_0 <= 0 ]
(Comp: 4*ar_1 + 3, Cost: 3) gcd_Load_463(ar_0, ar_1, ar_2) -> Com_1(gcd_Load_314(ar_1, ar_0, arityPad)) [ ar_0 >= 0 /\ 0 >= 0 ]
(Comp: 4*ar_1 + 4, Cost: 2) mod_LE_338(ar_0, ar_1, ar_2) -> Com_1(mod_GT_350(ar_1, ar_0, arityPad)) [ 1 <= ar_0 /\ 0 < ar_0 ]
(Comp: 4*ar_1 + 3, Cost: 4) mod_LE_338(ar_0, ar_1, ar_2) -> Com_1(gcd_Load_463(0, ar_1, arityPad)) [ ar_0 <= 0 ]
(Comp: 4*ar_1 + 3, Cost: 8) gcd_Load_314(ar_0, ar_1, ar_2) -> Com_1(mod_LE_338(ar_0, ar_1, arityPad)) [ 0 < ar_1 ]
(Comp: 1, Cost: 8) gcd_Load_314(ar_0, ar_1, ar_2) -> Com_1(mod_LE_338(ar_0, ar_1, arityPad)) [ ar_1 < 0 ]
(Comp: 1, Cost: 15) koat_start(ar_0, ar_1, ar_2) -> Com_1(gcd_Load_314(ar_0, ar_1, arityPad)) [ 0 <= 0 /\ static'1 <= static''' + 1 /\ 0 <= static''' /\ static''' <= ar_2 + 2 /\ 0 <= ar_2 /\ 0 <= static'1 ]
start location: koat_start
leaf cost: 0

A polynomial rank function with
Pol(mod_NE_369) = 3*V_1 - 2
Pol(mod_Load_470) = 3*V_2
Pol(mod_LE_475) = 3*V_2 - 1
and size complexities
S("koat_start(ar_0, ar_1, ar_2) -> Com_1(gcd_Load_314(ar_0, ar_1, arityPad)) [ 0 <= 0 /\\ static'1 <= static''' + 1 /\\ 0 <= static''' /\\ static''' <= ar_2 + 2 /\\ 0 <= ar_2 /\\ 0 <= static'1 ]", 0-0) = ar_0
S("koat_start(ar_0, ar_1, ar_2) -> Com_1(gcd_Load_314(ar_0, ar_1, arityPad)) [ 0 <= 0 /\\ static'1 <= static''' + 1 /\\ 0 <= static''' /\\ static''' <= ar_2 + 2 /\\ 0 <= ar_2 /\\ 0 <= static'1 ]", 0-1) = ar_1
S("koat_start(ar_0, ar_1, ar_2) -> Com_1(gcd_Load_314(ar_0, ar_1, arityPad)) [ 0 <= 0 /\\ static'1 <= static''' + 1 /\\ 0 <= static''' /\\ static''' <= ar_2 + 2 /\\ 0 <= ar_2 /\\ 0 <= static'1 ]", 0-2) = ?
S("gcd_Load_314(ar_0, ar_1, ar_2) -> Com_1(mod_LE_338(ar_0, ar_1, arityPad)) [ ar_1 < 0 ]", 0-0) = ar_0
S("gcd_Load_314(ar_0, ar_1, ar_2) -> Com_1(mod_LE_338(ar_0, ar_1, arityPad)) [ ar_1 < 0 ]", 0-1) = ar_1
S("gcd_Load_314(ar_0, ar_1, ar_2) -> Com_1(mod_LE_338(ar_0, ar_1, arityPad)) [ ar_1 < 0 ]", 0-2) = ?
S("gcd_Load_314(ar_0, ar_1, ar_2) -> Com_1(mod_LE_338(ar_0, ar_1, arityPad)) [ 0 < ar_1 ]", 0-0) = ar_0 + ar_1
S("gcd_Load_314(ar_0, ar_1, ar_2) -> Com_1(mod_LE_338(ar_0, ar_1, arityPad)) [ 0 < ar_1 ]", 0-1) = ar_1
S("gcd_Load_314(ar_0, ar_1, ar_2) -> Com_1(mod_LE_338(ar_0, ar_1, arityPad)) [ 0 < ar_1 ]", 0-2) = ?
S("mod_LE_338(ar_0, ar_1, ar_2) -> Com_1(gcd_Load_463(0, ar_1, arityPad)) [ ar_0 <= 0 ]", 0-0) = 0
S("mod_LE_338(ar_0, ar_1, ar_2) -> Com_1(gcd_Load_463(0, ar_1, arityPad)) [ ar_0 <= 0 ]", 0-1) = ar_1
S("mod_LE_338(ar_0, ar_1, ar_2) -> Com_1(gcd_Load_463(0, ar_1, arityPad)) [ ar_0 <= 0 ]", 0-2) = ?
S("mod_LE_338(ar_0, ar_1, ar_2) -> Com_1(mod_GT_350(ar_1, ar_0, arityPad)) [ 1 <= ar_0 /\\ 0 < ar_0 ]", 0-0) = ar_1
S("mod_LE_338(ar_0, ar_1, ar_2) -> Com_1(mod_GT_350(ar_1, ar_0, arityPad)) [ 1 <= ar_0 /\\ 0 < ar_0 ]", 0-1) = ar_0 + ar_1
S("mod_LE_338(ar_0, ar_1, ar_2) -> Com_1(mod_GT_350(ar_1, ar_0, arityPad)) [ 1 <= ar_0 /\\ 0 < ar_0 ]", 0-2) = ?
S("gcd_Load_463(ar_0, ar_1, ar_2) -> Com_1(gcd_Load_314(ar_1, ar_0, arityPad)) [ ar_0 >= 0 /\\ 0 >= 0 ]", 0-0) = ar_0 + ar_1
S("gcd_Load_463(ar_0, ar_1, ar_2) -> Com_1(gcd_Load_314(ar_1, ar_0, arityPad)) [ ar_0 >= 0 /\\ 0 >= 0 ]", 0-1) = 0
S("gcd_Load_463(ar_0, ar_1, ar_2) -> Com_1(gcd_Load_314(ar_1, ar_0, arityPad)) [ ar_0 >= 0 /\\ 0 >= 0 ]", 0-2) = ?
S("mod_GT_350(ar_0, ar_1, ar_2) -> Com_1(gcd_Load_463(0, ar_0, arityPad)) [ ar_1 - 1 >= 0 /\\ 1 <= ar_1 /\\ ar_0 <= -1 /\\ ar_0 <= 0 ]", 0-0) = 0
S("mod_GT_350(ar_0, ar_1, ar_2) -> Com_1(gcd_Load_463(0, ar_0, arityPad)) [ ar_1 - 1 >= 0 /\\ 1 <= ar_1 /\\ ar_0 <= -1 /\\ ar_0 <= 0 ]", 0-1) = ar_1
S("mod_GT_350(ar_0, ar_1, ar_2) -> Com_1(gcd_Load_463(0, ar_0, arityPad)) [ ar_1 - 1 >= 0 /\\ 1 <= ar_1 /\\ ar_0 <= -1 /\\ ar_0 <= 0 ]", 0-2) = ?
S("mod_GT_350(ar_0, ar_1, ar_2) -> Com_1(mod_NE_369(ar_1, ar_0, arityPad)) [ ar_1 - 1 >= 0 /\\ 1 <= ar_0 /\\ 1 <= ar_1 /\\ 0 < ar_0 ]", 0-0) = ar_0 + ar_1
S("mod_GT_350(ar_0, ar_1, ar_2) -> Com_1(mod_NE_369(ar_1, ar_0, arityPad)) [ ar_1 - 1 >= 0 /\\ 1 <= ar_0 /\\ 1 <= ar_1 /\\ 0 < ar_0 ]", 0-1) = ar_1
S("mod_GT_350(ar_0, ar_1, ar_2) -> Com_1(mod_NE_369(ar_1, ar_0, arityPad)) [ ar_1 - 1 >= 0 /\\ 1 <= ar_0 /\\ 1 <= ar_1 /\\ 0 < ar_0 ]", 0-2) = ?
S("mod_NE_369(ar_0, ar_1, ar_2) -> Com_1(gcd_Store_509(0, ar_0, arityPad)) [ ar_1 - 1 >= 0 /\\ ar_0 + ar_1 - 2 >= 0 /\\ ar_0 - 1 >= 0 /\\ 1 <= ar_0 /\\ ar_1 = ar_0 ]", 0-0) = 0
S("mod_NE_369(ar_0, ar_1, ar_2) -> Com_1(gcd_Store_509(0, ar_0, arityPad)) [ ar_1 - 1 >= 0 /\\ ar_0 + ar_1 - 2 >= 0 /\\ ar_0 - 1 >= 0 /\\ 1 <= ar_0 /\\ ar_1 = ar_0 ]", 0-1) = ar_0 + ar_1
S("mod_NE_369(ar_0, ar_1, ar_2) -> Com_1(gcd_Store_509(0, ar_0, arityPad)) [ ar_1 - 1 >= 0 /\\ ar_0 + ar_1 - 2 >= 0 /\\ ar_0 - 1 >= 0 /\\ 1 <= ar_0 /\\ ar_1 = ar_0 ]", 0-2) = ?
S("mod_NE_369(ar_0, ar_1, ar_2) -> Com_1(mod_Load_470(ar_0, ar_1, arityPad)) [ ar_1 - 1 >= 0 /\\ ar_0 + ar_1 - 2 >= 0 /\\ ar_0 - 1 >= 0 /\\ ar_0 < ar_1 /\\ 1 <= ar_0 /\\ 1 <= ar_1 ]", 0-0) = ar_0 + ar_1
S("mod_NE_369(ar_0, ar_1, ar_2) -> Com_1(mod_Load_470(ar_0, ar_1, arityPad)) [ ar_1 - 1 >= 0 /\\ ar_0 + ar_1 - 2 >= 0 /\\ ar_0 - 1 >= 0 /\\ ar_0 < ar_1 /\\ 1 <= ar_0 /\\ 1 <= ar_1 ]", 0-1) = ar_1
S("mod_NE_369(ar_0, ar_1, ar_2) -> Com_1(mod_Load_470(ar_0, ar_1, arityPad)) [ ar_1 - 1 >= 0 /\\ ar_0 + ar_1 - 2 >= 0 /\\ ar_0 - 1 >= 0 /\\ ar_0 < ar_1 /\\ 1 <= ar_0 /\\ 1 <= ar_1 ]", 0-2) = ?
S("mod_NE_369(ar_0, ar_1, ar_2) -> Com_1(mod_Load_470(ar_0, ar_1, arityPad)) [ ar_1 - 1 >= 0 /\\ ar_0 + ar_1 - 2 >= 0 /\\ ar_0 - 1 >= 0 /\\ ar_1 < ar_0 /\\ 1 <= ar_0 /\\ 1 <= ar_1 ]", 0-0) = ar_0 + ar_1
S("mod_NE_369(ar_0, ar_1, ar_2) -> Com_1(mod_Load_470(ar_0, ar_1, arityPad)) [ ar_1 - 1 >= 0 /\\ ar_0 + ar_1 - 2 >= 0 /\\ ar_0 - 1 >= 0 /\\ ar_1 < ar_0 /\\ 1 <= ar_0 /\\ 1 <= ar_1 ]", 0-1) = ar_0 + ar_1
S("mod_NE_369(ar_0, ar_1, ar_2) -> Com_1(mod_Load_470(ar_0, ar_1, arityPad)) [ ar_1 - 1 >= 0 /\\ ar_0 + ar_1 - 2 >= 0 /\\ ar_0 - 1 >= 0 /\\ ar_1 < ar_0 /\\ 1 <= ar_0 /\\ 1 <= ar_1 ]", 0-2) = ?
S("gcd_Store_509(ar_0, ar_1, ar_2) -> Com_1(gcd_Load_463(ar_0, ar_1, arityPad)) [ ar_1 - 1 >= 0 /\\ ar_0 + ar_1 - 1 >= 0 /\\ -ar_0 + ar_1 >= 0 /\\ ar_0 >= 0 /\\ 0 >= 0 ]", 0-0) = 0
S("gcd_Store_509(ar_0, ar_1, ar_2) -> Com_1(gcd_Load_463(ar_0, ar_1, arityPad)) [ ar_1 - 1 >= 0 /\\ ar_0 + ar_1 - 1 >= 0 /\\ -ar_0 + ar_1 >= 0 /\\ ar_0 >= 0 /\\ 0 >= 0 ]", 0-1) = ar_0 + ar_1
S("gcd_Store_509(ar_0, ar_1, ar_2) -> Com_1(gcd_Load_463(ar_0, ar_1, arityPad)) [ ar_1 - 1 >= 0 /\\ ar_0 + ar_1 - 1 >= 0 /\\ -ar_0 + ar_1 >= 0 /\\ ar_0 >= 0 /\\ 0 >= 0 ]", 0-2) = ?
S("mod_Load_470(ar_0, ar_1, ar_2) -> Com_1(mod_LE_475(ar_0, ar_1, arityPad)) [ ar_1 - 1 >= 0 /\\ 1 <= ar_0 /\\ 1 <= ar_1 ]", 0-0) = ar_0 + ar_1
S("mod_Load_470(ar_0, ar_1, ar_2) -> Com_1(mod_LE_475(ar_0, ar_1, arityPad)) [ ar_1 - 1 >= 0 /\\ 1 <= ar_0 /\\ 1 <= ar_1 ]", 0-1) = ar_0 + ar_1
S("mod_Load_470(ar_0, ar_1, ar_2) -> Com_1(mod_LE_475(ar_0, ar_1, arityPad)) [ ar_1 - 1 >= 0 /\\ 1 <= ar_0 /\\ 1 <= ar_1 ]", 0-2) = ?
S("mod_LE_475(ar_0, ar_1, ar_2) -> Com_1(mod_Load_470(ar_0 - ar_1, ar_1, arityPad)) [ ar_1 - 1 >= 0 /\\ ar_0 + ar_1 - 2 >= 0 /\\ ar_0 - 1 >= 0 /\\ 2 <= ar_0 /\\ 1 <= i172' /\\ 1 <= ar_1 /\\ 1 <= ar_0 /\\ ar_1 < ar_0 /\\ ar_0 - ar_1 = i172' ]", 0-0) = ar_0 + ar_1
S("mod_LE_475(ar_0, ar_1, ar_2) -> Com_1(mod_Load_470(ar_0 - ar_1, ar_1, arityPad)) [ ar_1 - 1 >= 0 /\\ ar_0 + ar_1 - 2 >= 0 /\\ ar_0 - 1 >= 0 /\\ 2 <= ar_0 /\\ 1 <= i172' /\\ 1 <= ar_1 /\\ 1 <= ar_0 /\\ ar_1 < ar_0 /\\ ar_0 - ar_1 = i172' ]", 0-1) = ar_0 + ar_1
S("mod_LE_475(ar_0, ar_1, ar_2) -> Com_1(mod_Load_470(ar_0 - ar_1, ar_1, arityPad)) [ ar_1 - 1 >= 0 /\\ ar_0 + ar_1 - 2 >= 0 /\\ ar_0 - 1 >= 0 /\\ 2 <= ar_0 /\\ 1 <= i172' /\\ 1 <= ar_1 /\\ 1 <= ar_0 /\\ ar_1 < ar_0 /\\ ar_0 - ar_1 = i172' ]", 0-2) = ?
S("mod_LE_475(ar_0, ar_1, ar_2) -> Com_1(mod_NE_369(ar_1, ar_0, arityPad')) [ ar_1 - 1 >= 0 /\\ ar_0 + ar_1 - 2 >= 0 /\\ ar_0 - 1 >= 0 /\\ 1 <= ar_1 /\\ 1 <= ar_0 /\\ ar_0 <= ar_1 /\\ ar_0 + ar_1 - 1 >= 0 /\\ -ar_0 + ar_1 >= 0 /\\ ar_0 >= 0 /\\ 0 >= 0 /\\ 0 < ar_0 /\\ 0 < ar_1 ]", 0-0) = ar_0 + ar_1
S("mod_LE_475(ar_0, ar_1, ar_2) -> Com_1(mod_NE_369(ar_1, ar_0, arityPad')) [ ar_1 - 1 >= 0 /\\ ar_0 + ar_1 - 2 >= 0 /\\ ar_0 - 1 >= 0 /\\ 1 <= ar_1 /\\ 1 <= ar_0 /\\ ar_0 <= ar_1 /\\ ar_0 + ar_1 - 1 >= 0 /\\ -ar_0 + ar_1 >= 0 /\\ ar_0 >= 0 /\\ 0 >= 0 /\\ 0 < ar_0 /\\ 0 < ar_1 ]", 0-1) = ar_0 + ar_1
S("mod_LE_475(ar_0, ar_1, ar_2) -> Com_1(mod_NE_369(ar_1, ar_0, arityPad')) [ ar_1 - 1 >= 0 /\\ ar_0 + ar_1 - 2 >= 0 /\\ ar_0 - 1 >= 0 /\\ 1 <= ar_1 /\\ 1 <= ar_0 /\\ ar_0 <= ar_1 /\\ ar_0 + ar_1 - 1 >= 0 /\\ -ar_0 + ar_1 >= 0 /\\ ar_0 >= 0 /\\ 0 >= 0 /\\ 0 < ar_0 /\\ 0 < ar_1 ]", 0-2) = ?
orients the transitions
mod_NE_369(ar_0, ar_1, ar_2) -> Com_1(mod_Load_470(ar_0, ar_1, arityPad)) [ ar_1 - 1 >= 0 /\ ar_0 + ar_1 - 2 >= 0 /\ ar_0 - 1 >= 0 /\ ar_1 < ar_0 /\ 1 <= ar_0 /\ 1 <= ar_1 ]
mod_Load_470(ar_0, ar_1, ar_2) -> Com_1(mod_LE_475(ar_0, ar_1, arityPad)) [ ar_1 - 1 >= 0 /\ 1 <= ar_0 /\ 1 <= ar_1 ]
mod_LE_475(ar_0, ar_1, ar_2) -> Com_1(mod_NE_369(ar_1, ar_0, arityPad')) [ ar_1 - 1 >= 0 /\ ar_0 + ar_1 - 2 >= 0 /\ ar_0 - 1 >= 0 /\ 1 <= ar_1 /\ 1 <= ar_0 /\ ar_0 <= ar_1 /\ ar_0 + ar_1 - 1 >= 0 /\ -ar_0 + ar_1 >= 0 /\ ar_0 >= 0 /\ 0 >= 0 /\ 0 < ar_0 /\ 0 < ar_1 ]
weakly and the transitions
mod_NE_369(ar_0, ar_1, ar_2) -> Com_1(mod_Load_470(ar_0, ar_1, arityPad)) [ ar_1 - 1 >= 0 /\ ar_0 + ar_1 - 2 >= 0 /\ ar_0 - 1 >= 0 /\ ar_1 < ar_0 /\ 1 <= ar_0 /\ 1 <= ar_1 ]
mod_Load_470(ar_0, ar_1, ar_2) -> Com_1(mod_LE_475(ar_0, ar_1, arityPad)) [ ar_1 - 1 >= 0 /\ 1 <= ar_0 /\ 1 <= ar_1 ]
mod_LE_475(ar_0, ar_1, ar_2) -> Com_1(mod_NE_369(ar_1, ar_0, arityPad')) [ ar_1 - 1 >= 0 /\ ar_0 + ar_1 - 2 >= 0 /\ ar_0 - 1 >= 0 /\ 1 <= ar_1 /\ 1 <= ar_0 /\ ar_0 <= ar_1 /\ ar_0 + ar_1 - 1 >= 0 /\ -ar_0 + ar_1 >= 0 /\ ar_0 >= 0 /\ 0 >= 0 /\ 0 < ar_0 /\ 0 < ar_1 ]
strictly and produces the following problem:
16: T:
(Comp: 45*ar_0*ar_1 + 45*ar_1^2 + 12*ar_0 + 32*ar_1 + 12*ar_0^2*ar_1 + 36*ar_0*ar_1^2 + 12*ar_0^2 + 24*ar_1^3 + 8, Cost: 20) mod_LE_475(ar_0, ar_1, ar_2) -> Com_1(mod_NE_369(ar_1, ar_0, arityPad')) [ ar_1 - 1 >= 0 /\ ar_0 + ar_1 - 2 >= 0 /\ ar_0 - 1 >= 0 /\ 1 <= ar_1 /\ 1 <= ar_0 /\ ar_0 <= ar_1 /\ ar_0 + ar_1 - 1 >= 0 /\ -ar_0 + ar_1 >= 0 /\ ar_0 >= 0 /\ 0 >= 0 /\ 0 < ar_0 /\ 0 < ar_1 ]
(Comp: 4*ar_0*ar_1 + 8*ar_1^2 + 4*ar_0 + 7*ar_1, Cost: 6) mod_LE_475(ar_0, ar_1, ar_2) -> Com_1(mod_Load_470(ar_0 - ar_1, ar_1, arityPad)) [ ar_1 - 1 >= 0 /\ ar_0 + ar_1 - 2 >= 0 /\ ar_0 - 1 >= 0 /\ 2 <= ar_0 /\ 1 <= i172' /\ 1 <= ar_1 /\ 1 <= ar_0 /\ ar_1 < ar_0 /\ ar_0 - ar_1 = i172' ]
(Comp: 45*ar_0*ar_1 + 45*ar_1^2 + 12*ar_0 + 32*ar_1 + 12*ar_0^2*ar_1 + 36*ar_0*ar_1^2 + 12*ar_0^2 + 24*ar_1^3 + 8, Cost: 2) mod_Load_470(ar_0, ar_1, ar_2) -> Com_1(mod_LE_475(ar_0, ar_1, arityPad)) [ ar_1 - 1 >= 0 /\ 1 <= ar_0 /\ 1 <= ar_1 ]
(Comp: 4*ar_1 + 3, Cost: 1) gcd_Store_509(ar_0, ar_1, ar_2) -> Com_1(gcd_Load_463(ar_0, ar_1, arityPad)) [ ar_1 - 1 >= 0 /\ ar_0 + ar_1 - 1 >= 0 /\ -ar_0 + ar_1 >= 0 /\ ar_0 >= 0 /\ 0 >= 0 ]
(Comp: 45*ar_0*ar_1 + 45*ar_1^2 + 12*ar_0 + 32*ar_1 + 12*ar_0^2*ar_1 + 36*ar_0*ar_1^2 + 12*ar_0^2 + 24*ar_1^3 + 8, Cost: 1) mod_NE_369(ar_0, ar_1, ar_2) -> Com_1(mod_Load_470(ar_0, ar_1, arityPad)) [ ar_1 - 1 >= 0 /\ ar_0 + ar_1 - 2 >= 0 /\ ar_0 - 1 >= 0 /\ ar_1 < ar_0 /\ 1 <= ar_0 /\ 1 <= ar_1 ]
(Comp: 4*ar_1 + 4, Cost: 1) mod_NE_369(ar_0, ar_1, ar_2) -> Com_1(mod_Load_470(ar_0, ar_1, arityPad)) [ ar_1 - 1 >= 0 /\ ar_0 + ar_1 - 2 >= 0 /\ ar_0 - 1 >= 0 /\ ar_0 < ar_1 /\ 1 <= ar_0 /\ 1 <= ar_1 ]
(Comp: 4*ar_1 + 3, Cost: 3) mod_NE_369(ar_0, ar_1, ar_2) -> Com_1(gcd_Store_509(0, ar_0, arityPad)) [ ar_1 - 1 >= 0 /\ ar_0 + ar_1 - 2 >= 0 /\ ar_0 - 1 >= 0 /\ 1 <= ar_0 /\ ar_1 = ar_0 ]
(Comp: 4*ar_1 + 4, Cost: 3) mod_GT_350(ar_0, ar_1, ar_2) -> Com_1(mod_NE_369(ar_1, ar_0, arityPad)) [ ar_1 - 1 >= 0 /\ 1 <= ar_0 /\ 1 <= ar_1 /\ 0 < ar_0 ]
(Comp: 4*ar_1 + 3, Cost: 4) mod_GT_350(ar_0, ar_1, ar_2) -> Com_1(gcd_Load_463(0, ar_0, arityPad)) [ ar_1 - 1 >= 0 /\ 1 <= ar_1 /\ ar_0 <= -1 /\ ar_0 <= 0 ]
(Comp: 4*ar_1 + 3, Cost: 3) gcd_Load_463(ar_0, ar_1, ar_2) -> Com_1(gcd_Load_314(ar_1, ar_0, arityPad)) [ ar_0 >= 0 /\ 0 >= 0 ]
(Comp: 4*ar_1 + 4, Cost: 2) mod_LE_338(ar_0, ar_1, ar_2) -> Com_1(mod_GT_350(ar_1, ar_0, arityPad)) [ 1 <= ar_0 /\ 0 < ar_0 ]
(Comp: 4*ar_1 + 3, Cost: 4) mod_LE_338(ar_0, ar_1, ar_2) -> Com_1(gcd_Load_463(0, ar_1, arityPad)) [ ar_0 <= 0 ]
(Comp: 4*ar_1 + 3, Cost: 8) gcd_Load_314(ar_0, ar_1, ar_2) -> Com_1(mod_LE_338(ar_0, ar_1, arityPad)) [ 0 < ar_1 ]
(Comp: 1, Cost: 8) gcd_Load_314(ar_0, ar_1, ar_2) -> Com_1(mod_LE_338(ar_0, ar_1, arityPad)) [ ar_1 < 0 ]
(Comp: 1, Cost: 15) koat_start(ar_0, ar_1, ar_2) -> Com_1(gcd_Load_314(ar_0, ar_1, arityPad)) [ 0 <= 0 /\ static'1 <= static''' + 1 /\ 0 <= static''' /\ static''' <= ar_2 + 2 /\ 0 <= ar_2 /\ 0 <= static'1 ]
start location: koat_start
leaf cost: 0

Complexity upper bound 1059*ar_0*ar_1 + 1083*ar_1^2 + 300*ar_0 + 894*ar_1 + 276*ar_0^2*ar_1 + 828*ar_0*ar_1^2 + 276*ar_0^2 + 552*ar_1^3 + 300

Time: 1.129 sec (SMT: 0.897 sec)

(46) BOUNDS(CONSTANT, 300 + 300 * |#0| + 1059 * |#0| * |#1| + 828 * |#0| * |#1|^2 + 276 * |#0|^2 + 276 * |#0|^2 * |#1| + 894 * |#1| + 1083 * |#1|^2 + 552 * |#1|^3)