WORST_CASE(Omega(n^1),O(n^2))
proof of /export/starexec/sandbox/benchmark/theBenchmark.trs
# AProVE Commit ID: c69e44bd14796315568835c1ffa2502984884775 mhark 20210624 unpublished


The Runtime Complexity (innermost) of the given CpxRelTRS could be proven to be BOUNDS(n^1, n^2).

(0) CpxRelTRS
(1) SInnermostTerminationProof [BOTH CONCRETE BOUNDS(ID, ID), 6390 ms]
(2) CpxRelTRS
(3) RelTrsToWeightedTrsProof [BOTH BOUNDS(ID, ID), 0 ms]
(4) CpxWeightedTrs
    (5) TypeInferenceProof [BOTH BOUNDS(ID, ID), 0 ms]
    (6) CpxTypedWeightedTrs
    (7) CompletionProof [UPPER BOUND(ID), 0 ms]
    (8) CpxTypedWeightedCompleteTrs
    (9) CpxTypedWeightedTrsToRntsProof [UPPER BOUND(ID), 0 ms]
    (10) CpxRNTS
    (11) CompleteCoflocoProof [FINISHED, 38.1 s]
    (12) BOUNDS(1, n^2)
(13) RelTrsToDecreasingLoopProblemProof [LOWER BOUND(ID), 0 ms]
(14) TRS for Loop Detection
    (15) DecreasingLoopProof [LOWER BOUND(ID), 0 ms]
    (16) BEST
        (17) proven lower bound
            (18) LowerBoundPropagationProof [FINISHED, 0 ms]
            (19) BOUNDS(n^1, INF)
        (20) TRS for Loop Detection


----------------------------------------

(0)
Obligation:
The Runtime Complexity (innermost) of the given CpxRelTRS could be proven to be BOUNDS(n^1, n^2).


The TRS R consists of the following rules:

   P(s(z0)) -> c
   P(0) -> c1
   LE(0, z0) -> c2
   LE(s(z0), 0) -> c3
   LE(s(z0), s(z1)) -> c4(LE(z0, z1))
   AVERAGE(z0, z1) -> c5(IF(le(z0, 0), le(z1, 0), le(z1, s(0)), le(z1, s(s(0))), z0, z1), LE(z0, 0))
   AVERAGE(z0, z1) -> c6(IF(le(z0, 0), le(z1, 0), le(z1, s(0)), le(z1, s(s(0))), z0, z1), LE(z1, 0))
   AVERAGE(z0, z1) -> c7(IF(le(z0, 0), le(z1, 0), le(z1, s(0)), le(z1, s(s(0))), z0, z1), LE(z1, s(0)))
   AVERAGE(z0, z1) -> c8(IF(le(z0, 0), le(z1, 0), le(z1, s(0)), le(z1, s(s(0))), z0, z1), LE(z1, s(s(0))))
   IF(true, z0, z1, z2, z3, z4) -> c9(IF2(z0, z1, z2, z3, z4))
   IF(false, z0, z1, z2, z3, z4) -> c10(AVERAGE(p(z3), s(z4)), P(z3))
   IF2(true, z0, z1, z2, z3) -> c11
   IF2(false, z0, z1, z2, z3) -> c12(IF3(z0, z1, z2, z3))
   IF3(true, z0, z1, z2) -> c13
   IF3(false, z0, z1, z2) -> c14(IF4(z0, z1, z2))
   IF4(true, z0, z1) -> c15
   IF4(false, z0, z1) -> c16(AVERAGE(s(z0), p(p(z1))), P(p(z1)), P(z1))

The (relative) TRS S consists of the following rules:

   p(s(z0)) -> z0
   p(0) -> 0
   le(0, z0) -> true
   le(s(z0), 0) -> false
   le(s(z0), s(z1)) -> le(z0, z1)
   average(z0, z1) -> if(le(z0, 0), le(z1, 0), le(z1, s(0)), le(z1, s(s(0))), z0, z1)
   if(true, z0, z1, z2, z3, z4) -> if2(z0, z1, z2, z3, z4)
   if(false, z0, z1, z2, z3, z4) -> average(p(z3), s(z4))
   if2(true, z0, z1, z2, z3) -> 0
   if2(false, z0, z1, z2, z3) -> if3(z0, z1, z2, z3)
   if3(true, z0, z1, z2) -> 0
   if3(false, z0, z1, z2) -> if4(z0, z1, z2)
   if4(true, z0, z1) -> s(0)
   if4(false, z0, z1) -> average(s(z0), p(p(z1)))

Rewrite Strategy: INNERMOST
----------------------------------------

(1) SInnermostTerminationProof (BOTH CONCRETE BOUNDS(ID, ID))
proved innermost termination of relative rules
----------------------------------------

(2)
Obligation:
The Runtime Complexity (innermost) of the given CpxRelTRS could be proven to be BOUNDS(n^1, n^2).


The TRS R consists of the following rules:

   P(s(z0)) -> c
   P(0) -> c1
   LE(0, z0) -> c2
   LE(s(z0), 0) -> c3
   LE(s(z0), s(z1)) -> c4(LE(z0, z1))
   AVERAGE(z0, z1) -> c5(IF(le(z0, 0), le(z1, 0), le(z1, s(0)), le(z1, s(s(0))), z0, z1), LE(z0, 0))
   AVERAGE(z0, z1) -> c6(IF(le(z0, 0), le(z1, 0), le(z1, s(0)), le(z1, s(s(0))), z0, z1), LE(z1, 0))
   AVERAGE(z0, z1) -> c7(IF(le(z0, 0), le(z1, 0), le(z1, s(0)), le(z1, s(s(0))), z0, z1), LE(z1, s(0)))
   AVERAGE(z0, z1) -> c8(IF(le(z0, 0), le(z1, 0), le(z1, s(0)), le(z1, s(s(0))), z0, z1), LE(z1, s(s(0))))
   IF(true, z0, z1, z2, z3, z4) -> c9(IF2(z0, z1, z2, z3, z4))
   IF(false, z0, z1, z2, z3, z4) -> c10(AVERAGE(p(z3), s(z4)), P(z3))
   IF2(true, z0, z1, z2, z3) -> c11
   IF2(false, z0, z1, z2, z3) -> c12(IF3(z0, z1, z2, z3))
   IF3(true, z0, z1, z2) -> c13
   IF3(false, z0, z1, z2) -> c14(IF4(z0, z1, z2))
   IF4(true, z0, z1) -> c15
   IF4(false, z0, z1) -> c16(AVERAGE(s(z0), p(p(z1))), P(p(z1)), P(z1))

The (relative) TRS S consists of the following rules:

   p(s(z0)) -> z0
   p(0) -> 0
   le(0, z0) -> true
   le(s(z0), 0) -> false
   le(s(z0), s(z1)) -> le(z0, z1)
   average(z0, z1) -> if(le(z0, 0), le(z1, 0), le(z1, s(0)), le(z1, s(s(0))), z0, z1)
   if(true, z0, z1, z2, z3, z4) -> if2(z0, z1, z2, z3, z4)
   if(false, z0, z1, z2, z3, z4) -> average(p(z3), s(z4))
   if2(true, z0, z1, z2, z3) -> 0
   if2(false, z0, z1, z2, z3) -> if3(z0, z1, z2, z3)
   if3(true, z0, z1, z2) -> 0
   if3(false, z0, z1, z2) -> if4(z0, z1, z2)
   if4(true, z0, z1) -> s(0)
   if4(false, z0, z1) -> average(s(z0), p(p(z1)))

Rewrite Strategy: INNERMOST
----------------------------------------

(3) RelTrsToWeightedTrsProof (BOTH BOUNDS(ID, ID))
Transformed relative TRS to weighted TRS
----------------------------------------

(4)
Obligation:
The Runtime Complexity (innermost) of the given CpxWeightedTrs could be proven to be BOUNDS(1, n^2).


The TRS R consists of the following rules:

   P(s(z0)) -> c [1]
   P(0) -> c1 [1]
   LE(0, z0) -> c2 [1]
   LE(s(z0), 0) -> c3 [1]
   LE(s(z0), s(z1)) -> c4(LE(z0, z1)) [1]
   AVERAGE(z0, z1) -> c5(IF(le(z0, 0), le(z1, 0), le(z1, s(0)), le(z1, s(s(0))), z0, z1), LE(z0, 0)) [1]
   AVERAGE(z0, z1) -> c6(IF(le(z0, 0), le(z1, 0), le(z1, s(0)), le(z1, s(s(0))), z0, z1), LE(z1, 0)) [1]
   AVERAGE(z0, z1) -> c7(IF(le(z0, 0), le(z1, 0), le(z1, s(0)), le(z1, s(s(0))), z0, z1), LE(z1, s(0))) [1]
   AVERAGE(z0, z1) -> c8(IF(le(z0, 0), le(z1, 0), le(z1, s(0)), le(z1, s(s(0))), z0, z1), LE(z1, s(s(0)))) [1]
   IF(true, z0, z1, z2, z3, z4) -> c9(IF2(z0, z1, z2, z3, z4)) [1]
   IF(false, z0, z1, z2, z3, z4) -> c10(AVERAGE(p(z3), s(z4)), P(z3)) [1]
   IF2(true, z0, z1, z2, z3) -> c11 [1]
   IF2(false, z0, z1, z2, z3) -> c12(IF3(z0, z1, z2, z3)) [1]
   IF3(true, z0, z1, z2) -> c13 [1]
   IF3(false, z0, z1, z2) -> c14(IF4(z0, z1, z2)) [1]
   IF4(true, z0, z1) -> c15 [1]
   IF4(false, z0, z1) -> c16(AVERAGE(s(z0), p(p(z1))), P(p(z1)), P(z1)) [1]
   p(s(z0)) -> z0 [0]
   p(0) -> 0 [0]
   le(0, z0) -> true [0]
   le(s(z0), 0) -> false [0]
   le(s(z0), s(z1)) -> le(z0, z1) [0]
   average(z0, z1) -> if(le(z0, 0), le(z1, 0), le(z1, s(0)), le(z1, s(s(0))), z0, z1) [0]
   if(true, z0, z1, z2, z3, z4) -> if2(z0, z1, z2, z3, z4) [0]
   if(false, z0, z1, z2, z3, z4) -> average(p(z3), s(z4)) [0]
   if2(true, z0, z1, z2, z3) -> 0 [0]
   if2(false, z0, z1, z2, z3) -> if3(z0, z1, z2, z3) [0]
   if3(true, z0, z1, z2) -> 0 [0]
   if3(false, z0, z1, z2) -> if4(z0, z1, z2) [0]
   if4(true, z0, z1) -> s(0) [0]
   if4(false, z0, z1) -> average(s(z0), p(p(z1))) [0]

Rewrite Strategy: INNERMOST
----------------------------------------

(5) TypeInferenceProof (BOTH BOUNDS(ID, ID))
Infered types.
----------------------------------------

(6)
Obligation:
Runtime Complexity Weighted TRS with Types.
The TRS R consists of the following rules:

   P(s(z0)) -> c [1]
   P(0) -> c1 [1]
   LE(0, z0) -> c2 [1]
   LE(s(z0), 0) -> c3 [1]
   LE(s(z0), s(z1)) -> c4(LE(z0, z1)) [1]
   AVERAGE(z0, z1) -> c5(IF(le(z0, 0), le(z1, 0), le(z1, s(0)), le(z1, s(s(0))), z0, z1), LE(z0, 0)) [1]
   AVERAGE(z0, z1) -> c6(IF(le(z0, 0), le(z1, 0), le(z1, s(0)), le(z1, s(s(0))), z0, z1), LE(z1, 0)) [1]
   AVERAGE(z0, z1) -> c7(IF(le(z0, 0), le(z1, 0), le(z1, s(0)), le(z1, s(s(0))), z0, z1), LE(z1, s(0))) [1]
   AVERAGE(z0, z1) -> c8(IF(le(z0, 0), le(z1, 0), le(z1, s(0)), le(z1, s(s(0))), z0, z1), LE(z1, s(s(0)))) [1]
   IF(true, z0, z1, z2, z3, z4) -> c9(IF2(z0, z1, z2, z3, z4)) [1]
   IF(false, z0, z1, z2, z3, z4) -> c10(AVERAGE(p(z3), s(z4)), P(z3)) [1]
   IF2(true, z0, z1, z2, z3) -> c11 [1]
   IF2(false, z0, z1, z2, z3) -> c12(IF3(z0, z1, z2, z3)) [1]
   IF3(true, z0, z1, z2) -> c13 [1]
   IF3(false, z0, z1, z2) -> c14(IF4(z0, z1, z2)) [1]
   IF4(true, z0, z1) -> c15 [1]
   IF4(false, z0, z1) -> c16(AVERAGE(s(z0), p(p(z1))), P(p(z1)), P(z1)) [1]
   p(s(z0)) -> z0 [0]
   p(0) -> 0 [0]
   le(0, z0) -> true [0]
   le(s(z0), 0) -> false [0]
   le(s(z0), s(z1)) -> le(z0, z1) [0]
   average(z0, z1) -> if(le(z0, 0), le(z1, 0), le(z1, s(0)), le(z1, s(s(0))), z0, z1) [0]
   if(true, z0, z1, z2, z3, z4) -> if2(z0, z1, z2, z3, z4) [0]
   if(false, z0, z1, z2, z3, z4) -> average(p(z3), s(z4)) [0]
   if2(true, z0, z1, z2, z3) -> 0 [0]
   if2(false, z0, z1, z2, z3) -> if3(z0, z1, z2, z3) [0]
   if3(true, z0, z1, z2) -> 0 [0]
   if3(false, z0, z1, z2) -> if4(z0, z1, z2) [0]
   if4(true, z0, z1) -> s(0) [0]
   if4(false, z0, z1) -> average(s(z0), p(p(z1))) [0]

The TRS has the following type information:
P :: s:0 -> c:c1
s :: s:0 -> s:0
c :: c:c1
0 :: s:0
c1 :: c:c1
LE :: s:0 -> s:0 -> c2:c3:c4
c2 :: c2:c3:c4
c3 :: c2:c3:c4
c4 :: c2:c3:c4 -> c2:c3:c4
AVERAGE :: s:0 -> s:0 -> c5:c6:c7:c8
c5 :: c9:c10 -> c2:c3:c4 -> c5:c6:c7:c8
IF :: true:false -> true:false -> true:false -> true:false -> s:0 -> s:0 -> c9:c10
le :: s:0 -> s:0 -> true:false
c6 :: c9:c10 -> c2:c3:c4 -> c5:c6:c7:c8
c7 :: c9:c10 -> c2:c3:c4 -> c5:c6:c7:c8
c8 :: c9:c10 -> c2:c3:c4 -> c5:c6:c7:c8
true :: true:false
c9 :: c11:c12 -> c9:c10
IF2 :: true:false -> true:false -> true:false -> s:0 -> s:0 -> c11:c12
false :: true:false
c10 :: c5:c6:c7:c8 -> c:c1 -> c9:c10
p :: s:0 -> s:0
c11 :: c11:c12
c12 :: c13:c14 -> c11:c12
IF3 :: true:false -> true:false -> s:0 -> s:0 -> c13:c14
c13 :: c13:c14
c14 :: c15:c16 -> c13:c14
IF4 :: true:false -> s:0 -> s:0 -> c15:c16
c15 :: c15:c16
c16 :: c5:c6:c7:c8 -> c:c1 -> c:c1 -> c15:c16
average :: s:0 -> s:0 -> s:0
if :: true:false -> true:false -> true:false -> true:false -> s:0 -> s:0 -> s:0
if2 :: true:false -> true:false -> true:false -> s:0 -> s:0 -> s:0
if3 :: true:false -> true:false -> s:0 -> s:0 -> s:0
if4 :: true:false -> s:0 -> s:0 -> s:0

Rewrite Strategy: INNERMOST
----------------------------------------

(7) CompletionProof (UPPER BOUND(ID))
The TRS is a completely defined constructor system, as every type has a constant constructor and the following rules were added:

   p(v0) -> null_p [0]
   le(v0, v1) -> null_le [0]
   average(v0, v1) -> null_average [0]
   if(v0, v1, v2, v3, v4, v5) -> null_if [0]
   if2(v0, v1, v2, v3, v4) -> null_if2 [0]
   if3(v0, v1, v2, v3) -> null_if3 [0]
   if4(v0, v1, v2) -> null_if4 [0]
   P(v0) -> null_P [0]
   LE(v0, v1) -> null_LE [0]
   IF(v0, v1, v2, v3, v4, v5) -> null_IF [0]
   IF2(v0, v1, v2, v3, v4) -> null_IF2 [0]
   IF3(v0, v1, v2, v3) -> null_IF3 [0]
   IF4(v0, v1, v2) -> null_IF4 [0]

And the following fresh constants:    null_p, null_le, null_average, null_if, null_if2, null_if3, null_if4, null_P, null_LE, null_IF, null_IF2, null_IF3, null_IF4, const

----------------------------------------

(8)
Obligation:
Runtime Complexity Weighted TRS where all functions are completely defined. The underlying TRS is:

Runtime Complexity Weighted TRS with Types.
The TRS R consists of the following rules:

   P(s(z0)) -> c [1]
   P(0) -> c1 [1]
   LE(0, z0) -> c2 [1]
   LE(s(z0), 0) -> c3 [1]
   LE(s(z0), s(z1)) -> c4(LE(z0, z1)) [1]
   AVERAGE(z0, z1) -> c5(IF(le(z0, 0), le(z1, 0), le(z1, s(0)), le(z1, s(s(0))), z0, z1), LE(z0, 0)) [1]
   AVERAGE(z0, z1) -> c6(IF(le(z0, 0), le(z1, 0), le(z1, s(0)), le(z1, s(s(0))), z0, z1), LE(z1, 0)) [1]
   AVERAGE(z0, z1) -> c7(IF(le(z0, 0), le(z1, 0), le(z1, s(0)), le(z1, s(s(0))), z0, z1), LE(z1, s(0))) [1]
   AVERAGE(z0, z1) -> c8(IF(le(z0, 0), le(z1, 0), le(z1, s(0)), le(z1, s(s(0))), z0, z1), LE(z1, s(s(0)))) [1]
   IF(true, z0, z1, z2, z3, z4) -> c9(IF2(z0, z1, z2, z3, z4)) [1]
   IF(false, z0, z1, z2, z3, z4) -> c10(AVERAGE(p(z3), s(z4)), P(z3)) [1]
   IF2(true, z0, z1, z2, z3) -> c11 [1]
   IF2(false, z0, z1, z2, z3) -> c12(IF3(z0, z1, z2, z3)) [1]
   IF3(true, z0, z1, z2) -> c13 [1]
   IF3(false, z0, z1, z2) -> c14(IF4(z0, z1, z2)) [1]
   IF4(true, z0, z1) -> c15 [1]
   IF4(false, z0, z1) -> c16(AVERAGE(s(z0), p(p(z1))), P(p(z1)), P(z1)) [1]
   p(s(z0)) -> z0 [0]
   p(0) -> 0 [0]
   le(0, z0) -> true [0]
   le(s(z0), 0) -> false [0]
   le(s(z0), s(z1)) -> le(z0, z1) [0]
   average(z0, z1) -> if(le(z0, 0), le(z1, 0), le(z1, s(0)), le(z1, s(s(0))), z0, z1) [0]
   if(true, z0, z1, z2, z3, z4) -> if2(z0, z1, z2, z3, z4) [0]
   if(false, z0, z1, z2, z3, z4) -> average(p(z3), s(z4)) [0]
   if2(true, z0, z1, z2, z3) -> 0 [0]
   if2(false, z0, z1, z2, z3) -> if3(z0, z1, z2, z3) [0]
   if3(true, z0, z1, z2) -> 0 [0]
   if3(false, z0, z1, z2) -> if4(z0, z1, z2) [0]
   if4(true, z0, z1) -> s(0) [0]
   if4(false, z0, z1) -> average(s(z0), p(p(z1))) [0]
   p(v0) -> null_p [0]
   le(v0, v1) -> null_le [0]
   average(v0, v1) -> null_average [0]
   if(v0, v1, v2, v3, v4, v5) -> null_if [0]
   if2(v0, v1, v2, v3, v4) -> null_if2 [0]
   if3(v0, v1, v2, v3) -> null_if3 [0]
   if4(v0, v1, v2) -> null_if4 [0]
   P(v0) -> null_P [0]
   LE(v0, v1) -> null_LE [0]
   IF(v0, v1, v2, v3, v4, v5) -> null_IF [0]
   IF2(v0, v1, v2, v3, v4) -> null_IF2 [0]
   IF3(v0, v1, v2, v3) -> null_IF3 [0]
   IF4(v0, v1, v2) -> null_IF4 [0]

The TRS has the following type information:
P :: s:0:null_p:null_average:null_if:null_if2:null_if3:null_if4 -> c:c1:null_P
s :: s:0:null_p:null_average:null_if:null_if2:null_if3:null_if4 -> s:0:null_p:null_average:null_if:null_if2:null_if3:null_if4
c :: c:c1:null_P
0 :: s:0:null_p:null_average:null_if:null_if2:null_if3:null_if4
c1 :: c:c1:null_P
LE :: s:0:null_p:null_average:null_if:null_if2:null_if3:null_if4 -> s:0:null_p:null_average:null_if:null_if2:null_if3:null_if4 -> c2:c3:c4:null_LE
c2 :: c2:c3:c4:null_LE
c3 :: c2:c3:c4:null_LE
c4 :: c2:c3:c4:null_LE -> c2:c3:c4:null_LE
AVERAGE :: s:0:null_p:null_average:null_if:null_if2:null_if3:null_if4 -> s:0:null_p:null_average:null_if:null_if2:null_if3:null_if4 -> c5:c6:c7:c8
c5 :: c9:c10:null_IF -> c2:c3:c4:null_LE -> c5:c6:c7:c8
IF :: true:false:null_le -> true:false:null_le -> true:false:null_le -> true:false:null_le -> s:0:null_p:null_average:null_if:null_if2:null_if3:null_if4 -> s:0:null_p:null_average:null_if:null_if2:null_if3:null_if4 -> c9:c10:null_IF
le :: s:0:null_p:null_average:null_if:null_if2:null_if3:null_if4 -> s:0:null_p:null_average:null_if:null_if2:null_if3:null_if4 -> true:false:null_le
c6 :: c9:c10:null_IF -> c2:c3:c4:null_LE -> c5:c6:c7:c8
c7 :: c9:c10:null_IF -> c2:c3:c4:null_LE -> c5:c6:c7:c8
c8 :: c9:c10:null_IF -> c2:c3:c4:null_LE -> c5:c6:c7:c8
true :: true:false:null_le
c9 :: c11:c12:null_IF2 -> c9:c10:null_IF
IF2 :: true:false:null_le -> true:false:null_le -> true:false:null_le -> s:0:null_p:null_average:null_if:null_if2:null_if3:null_if4 -> s:0:null_p:null_average:null_if:null_if2:null_if3:null_if4 -> c11:c12:null_IF2
false :: true:false:null_le
c10 :: c5:c6:c7:c8 -> c:c1:null_P -> c9:c10:null_IF
p :: s:0:null_p:null_average:null_if:null_if2:null_if3:null_if4 -> s:0:null_p:null_average:null_if:null_if2:null_if3:null_if4
c11 :: c11:c12:null_IF2
c12 :: c13:c14:null_IF3 -> c11:c12:null_IF2
IF3 :: true:false:null_le -> true:false:null_le -> s:0:null_p:null_average:null_if:null_if2:null_if3:null_if4 -> s:0:null_p:null_average:null_if:null_if2:null_if3:null_if4 -> c13:c14:null_IF3
c13 :: c13:c14:null_IF3
c14 :: c15:c16:null_IF4 -> c13:c14:null_IF3
IF4 :: true:false:null_le -> s:0:null_p:null_average:null_if:null_if2:null_if3:null_if4 -> s:0:null_p:null_average:null_if:null_if2:null_if3:null_if4 -> c15:c16:null_IF4
c15 :: c15:c16:null_IF4
c16 :: c5:c6:c7:c8 -> c:c1:null_P -> c:c1:null_P -> c15:c16:null_IF4
average :: s:0:null_p:null_average:null_if:null_if2:null_if3:null_if4 -> s:0:null_p:null_average:null_if:null_if2:null_if3:null_if4 -> s:0:null_p:null_average:null_if:null_if2:null_if3:null_if4
if :: true:false:null_le -> true:false:null_le -> true:false:null_le -> true:false:null_le -> s:0:null_p:null_average:null_if:null_if2:null_if3:null_if4 -> s:0:null_p:null_average:null_if:null_if2:null_if3:null_if4 -> s:0:null_p:null_average:null_if:null_if2:null_if3:null_if4
if2 :: true:false:null_le -> true:false:null_le -> true:false:null_le -> s:0:null_p:null_average:null_if:null_if2:null_if3:null_if4 -> s:0:null_p:null_average:null_if:null_if2:null_if3:null_if4 -> s:0:null_p:null_average:null_if:null_if2:null_if3:null_if4
if3 :: true:false:null_le -> true:false:null_le -> s:0:null_p:null_average:null_if:null_if2:null_if3:null_if4 -> s:0:null_p:null_average:null_if:null_if2:null_if3:null_if4 -> s:0:null_p:null_average:null_if:null_if2:null_if3:null_if4
if4 :: true:false:null_le -> s:0:null_p:null_average:null_if:null_if2:null_if3:null_if4 -> s:0:null_p:null_average:null_if:null_if2:null_if3:null_if4 -> s:0:null_p:null_average:null_if:null_if2:null_if3:null_if4
null_p :: s:0:null_p:null_average:null_if:null_if2:null_if3:null_if4
null_le :: true:false:null_le
null_average :: s:0:null_p:null_average:null_if:null_if2:null_if3:null_if4
null_if :: s:0:null_p:null_average:null_if:null_if2:null_if3:null_if4
null_if2 :: s:0:null_p:null_average:null_if:null_if2:null_if3:null_if4
null_if3 :: s:0:null_p:null_average:null_if:null_if2:null_if3:null_if4
null_if4 :: s:0:null_p:null_average:null_if:null_if2:null_if3:null_if4
null_P :: c:c1:null_P
null_LE :: c2:c3:c4:null_LE
null_IF :: c9:c10:null_IF
null_IF2 :: c11:c12:null_IF2
null_IF3 :: c13:c14:null_IF3
null_IF4 :: c15:c16:null_IF4
const :: c5:c6:c7:c8

Rewrite Strategy: INNERMOST
----------------------------------------

(9) CpxTypedWeightedTrsToRntsProof (UPPER BOUND(ID))
Transformed the TRS into an over-approximating RNTS by (improved) Size Abstraction.
The constant constructors are abstracted as follows:

   c => 1
   0 => 0
   c1 => 2
   c2 => 0
   c3 => 1
   true => 2
   false => 1
   c11 => 0
   c13 => 0
   c15 => 0
   null_p => 0
   null_le => 0
   null_average => 0
   null_if => 0
   null_if2 => 0
   null_if3 => 0
   null_if4 => 0
   null_P => 0
   null_LE => 0
   null_IF => 0
   null_IF2 => 0
   null_IF3 => 0
   null_IF4 => 0
   const => 0

----------------------------------------

(10)
Obligation:
Complexity RNTS consisting of the following rules:

   AVERAGE(z, z') -{ 1 }-> 1 + IF(le(z0, 0), le(z1, 0), le(z1, 1 + 0), le(z1, 1 + (1 + 0)), z0, z1) + LE(z0, 0) :|: z = z0, z1 >= 0, z' = z1, z0 >= 0
   AVERAGE(z, z') -{ 1 }-> 1 + IF(le(z0, 0), le(z1, 0), le(z1, 1 + 0), le(z1, 1 + (1 + 0)), z0, z1) + LE(z1, 0) :|: z = z0, z1 >= 0, z' = z1, z0 >= 0
   AVERAGE(z, z') -{ 1 }-> 1 + IF(le(z0, 0), le(z1, 0), le(z1, 1 + 0), le(z1, 1 + (1 + 0)), z0, z1) + LE(z1, 1 + 0) :|: z = z0, z1 >= 0, z' = z1, z0 >= 0
   AVERAGE(z, z') -{ 1 }-> 1 + IF(le(z0, 0), le(z1, 0), le(z1, 1 + 0), le(z1, 1 + (1 + 0)), z0, z1) + LE(z1, 1 + (1 + 0)) :|: z = z0, z1 >= 0, z' = z1, z0 >= 0
   IF(z, z', z'', z5, z6, z7) -{ 0 }-> 0 :|: z5 = v3, v0 >= 0, v4 >= 0, z7 = v5, z6 = v4, z'' = v2, v1 >= 0, v5 >= 0, z = v0, z' = v1, v2 >= 0, v3 >= 0
   IF(z, z', z'', z5, z6, z7) -{ 1 }-> 1 + IF2(z0, z1, z2, z3, z4) :|: z = 2, z1 >= 0, z6 = z3, z7 = z4, z0 >= 0, z4 >= 0, z5 = z2, z' = z0, z2 >= 0, z3 >= 0, z'' = z1
   IF(z, z', z'', z5, z6, z7) -{ 1 }-> 1 + AVERAGE(p(z3), 1 + z4) + P(z3) :|: z1 >= 0, z = 1, z6 = z3, z7 = z4, z0 >= 0, z4 >= 0, z5 = z2, z' = z0, z2 >= 0, z3 >= 0, z'' = z1
   IF2(z, z', z'', z5, z6) -{ 1 }-> 0 :|: z = 2, z1 >= 0, z6 = z3, z0 >= 0, z5 = z2, z' = z0, z2 >= 0, z3 >= 0, z'' = z1
   IF2(z, z', z'', z5, z6) -{ 0 }-> 0 :|: z5 = v3, v0 >= 0, v4 >= 0, z6 = v4, z'' = v2, v1 >= 0, z = v0, z' = v1, v2 >= 0, v3 >= 0
   IF2(z, z', z'', z5, z6) -{ 1 }-> 1 + IF3(z0, z1, z2, z3) :|: z1 >= 0, z = 1, z6 = z3, z0 >= 0, z5 = z2, z' = z0, z2 >= 0, z3 >= 0, z'' = z1
   IF3(z, z', z'', z5) -{ 1 }-> 0 :|: z = 2, z1 >= 0, z0 >= 0, z5 = z2, z' = z0, z2 >= 0, z'' = z1
   IF3(z, z', z'', z5) -{ 0 }-> 0 :|: z5 = v3, v0 >= 0, z'' = v2, v1 >= 0, z = v0, z' = v1, v2 >= 0, v3 >= 0
   IF3(z, z', z'', z5) -{ 1 }-> 1 + IF4(z0, z1, z2) :|: z1 >= 0, z = 1, z0 >= 0, z5 = z2, z' = z0, z2 >= 0, z'' = z1
   IF4(z, z', z'') -{ 1 }-> 0 :|: z = 2, z1 >= 0, z0 >= 0, z' = z0, z'' = z1
   IF4(z, z', z'') -{ 0 }-> 0 :|: v0 >= 0, z'' = v2, v1 >= 0, z = v0, z' = v1, v2 >= 0
   IF4(z, z', z'') -{ 1 }-> 1 + AVERAGE(1 + z0, p(p(z1))) + P(p(z1)) + P(z1) :|: z1 >= 0, z = 1, z0 >= 0, z' = z0, z'' = z1
   LE(z, z') -{ 1 }-> 1 :|: z = 1 + z0, z0 >= 0, z' = 0
   LE(z, z') -{ 1 }-> 0 :|: z0 >= 0, z = 0, z' = z0
   LE(z, z') -{ 0 }-> 0 :|: v0 >= 0, v1 >= 0, z = v0, z' = v1
   LE(z, z') -{ 1 }-> 1 + LE(z0, z1) :|: z1 >= 0, z = 1 + z0, z0 >= 0, z' = 1 + z1
   P(z) -{ 1 }-> 2 :|: z = 0
   P(z) -{ 1 }-> 1 :|: z = 1 + z0, z0 >= 0
   P(z) -{ 0 }-> 0 :|: v0 >= 0, z = v0
   average(z, z') -{ 0 }-> if(le(z0, 0), le(z1, 0), le(z1, 1 + 0), le(z1, 1 + (1 + 0)), z0, z1) :|: z = z0, z1 >= 0, z' = z1, z0 >= 0
   average(z, z') -{ 0 }-> 0 :|: v0 >= 0, v1 >= 0, z = v0, z' = v1
   if(z, z', z'', z5, z6, z7) -{ 0 }-> if2(z0, z1, z2, z3, z4) :|: z = 2, z1 >= 0, z6 = z3, z7 = z4, z0 >= 0, z4 >= 0, z5 = z2, z' = z0, z2 >= 0, z3 >= 0, z'' = z1
   if(z, z', z'', z5, z6, z7) -{ 0 }-> average(p(z3), 1 + z4) :|: z1 >= 0, z = 1, z6 = z3, z7 = z4, z0 >= 0, z4 >= 0, z5 = z2, z' = z0, z2 >= 0, z3 >= 0, z'' = z1
   if(z, z', z'', z5, z6, z7) -{ 0 }-> 0 :|: z5 = v3, v0 >= 0, v4 >= 0, z7 = v5, z6 = v4, z'' = v2, v1 >= 0, v5 >= 0, z = v0, z' = v1, v2 >= 0, v3 >= 0
   if2(z, z', z'', z5, z6) -{ 0 }-> if3(z0, z1, z2, z3) :|: z1 >= 0, z = 1, z6 = z3, z0 >= 0, z5 = z2, z' = z0, z2 >= 0, z3 >= 0, z'' = z1
   if2(z, z', z'', z5, z6) -{ 0 }-> 0 :|: z = 2, z1 >= 0, z6 = z3, z0 >= 0, z5 = z2, z' = z0, z2 >= 0, z3 >= 0, z'' = z1
   if2(z, z', z'', z5, z6) -{ 0 }-> 0 :|: z5 = v3, v0 >= 0, v4 >= 0, z6 = v4, z'' = v2, v1 >= 0, z = v0, z' = v1, v2 >= 0, v3 >= 0
   if3(z, z', z'', z5) -{ 0 }-> if4(z0, z1, z2) :|: z1 >= 0, z = 1, z0 >= 0, z5 = z2, z' = z0, z2 >= 0, z'' = z1
   if3(z, z', z'', z5) -{ 0 }-> 0 :|: z = 2, z1 >= 0, z0 >= 0, z5 = z2, z' = z0, z2 >= 0, z'' = z1
   if3(z, z', z'', z5) -{ 0 }-> 0 :|: z5 = v3, v0 >= 0, z'' = v2, v1 >= 0, z = v0, z' = v1, v2 >= 0, v3 >= 0
   if4(z, z', z'') -{ 0 }-> average(1 + z0, p(p(z1))) :|: z1 >= 0, z = 1, z0 >= 0, z' = z0, z'' = z1
   if4(z, z', z'') -{ 0 }-> 0 :|: v0 >= 0, z'' = v2, v1 >= 0, z = v0, z' = v1, v2 >= 0
   if4(z, z', z'') -{ 0 }-> 1 + 0 :|: z = 2, z1 >= 0, z0 >= 0, z' = z0, z'' = z1
   le(z, z') -{ 0 }-> le(z0, z1) :|: z1 >= 0, z = 1 + z0, z0 >= 0, z' = 1 + z1
   le(z, z') -{ 0 }-> 2 :|: z0 >= 0, z = 0, z' = z0
   le(z, z') -{ 0 }-> 1 :|: z = 1 + z0, z0 >= 0, z' = 0
   le(z, z') -{ 0 }-> 0 :|: v0 >= 0, v1 >= 0, z = v0, z' = v1
   p(z) -{ 0 }-> z0 :|: z = 1 + z0, z0 >= 0
   p(z) -{ 0 }-> 0 :|: z = 0
   p(z) -{ 0 }-> 0 :|: v0 >= 0, z = v0

Only complete derivations are relevant for the runtime complexity.

----------------------------------------

(11) CompleteCoflocoProof (FINISHED)
Transformed the RNTS (where only complete derivations are relevant) into cost relations for CoFloCo:

eq(start(V, V2, V19, V18, V15, V16),0,[fun(V, Out)],[V >= 0]).
eq(start(V, V2, V19, V18, V15, V16),0,[fun1(V, V2, Out)],[V >= 0,V2 >= 0]).
eq(start(V, V2, V19, V18, V15, V16),0,[fun2(V, V2, Out)],[V >= 0,V2 >= 0]).
eq(start(V, V2, V19, V18, V15, V16),0,[fun3(V, V2, V19, V18, V15, V16, Out)],[V >= 0,V2 >= 0,V19 >= 0,V18 >= 0,V15 >= 0,V16 >= 0]).
eq(start(V, V2, V19, V18, V15, V16),0,[fun4(V, V2, V19, V18, V15, Out)],[V >= 0,V2 >= 0,V19 >= 0,V18 >= 0,V15 >= 0]).
eq(start(V, V2, V19, V18, V15, V16),0,[fun5(V, V2, V19, V18, Out)],[V >= 0,V2 >= 0,V19 >= 0,V18 >= 0]).
eq(start(V, V2, V19, V18, V15, V16),0,[fun6(V, V2, V19, Out)],[V >= 0,V2 >= 0,V19 >= 0]).
eq(start(V, V2, V19, V18, V15, V16),0,[p(V, Out)],[V >= 0]).
eq(start(V, V2, V19, V18, V15, V16),0,[le(V, V2, Out)],[V >= 0,V2 >= 0]).
eq(start(V, V2, V19, V18, V15, V16),0,[average(V, V2, Out)],[V >= 0,V2 >= 0]).
eq(start(V, V2, V19, V18, V15, V16),0,[if(V, V2, V19, V18, V15, V16, Out)],[V >= 0,V2 >= 0,V19 >= 0,V18 >= 0,V15 >= 0,V16 >= 0]).
eq(start(V, V2, V19, V18, V15, V16),0,[if2(V, V2, V19, V18, V15, Out)],[V >= 0,V2 >= 0,V19 >= 0,V18 >= 0,V15 >= 0]).
eq(start(V, V2, V19, V18, V15, V16),0,[if3(V, V2, V19, V18, Out)],[V >= 0,V2 >= 0,V19 >= 0,V18 >= 0]).
eq(start(V, V2, V19, V18, V15, V16),0,[if4(V, V2, V19, Out)],[V >= 0,V2 >= 0,V19 >= 0]).
eq(fun(V, Out),1,[],[Out = 1,V = 1 + V1,V1 >= 0]).
eq(fun(V, Out),1,[],[Out = 2,V = 0]).
eq(fun1(V, V2, Out),1,[],[Out = 0,V3 >= 0,V = 0,V2 = V3]).
eq(fun1(V, V2, Out),1,[],[Out = 1,V = 1 + V4,V4 >= 0,V2 = 0]).
eq(fun1(V, V2, Out),1,[fun1(V5, V6, Ret1)],[Out = 1 + Ret1,V6 >= 0,V = 1 + V5,V5 >= 0,V2 = 1 + V6]).
eq(fun2(V, V2, Out),1,[le(V7, 0, Ret010),le(V8, 0, Ret011),le(V8, 1 + 0, Ret012),le(V8, 1 + (1 + 0), Ret013),fun3(Ret010, Ret011, Ret012, Ret013, V7, V8, Ret01),fun1(V7, 0, Ret11)],[Out = 1 + Ret01 + Ret11,V = V7,V8 >= 0,V2 = V8,V7 >= 0]).
eq(fun2(V, V2, Out),1,[le(V9, 0, Ret0101),le(V10, 0, Ret0111),le(V10, 1 + 0, Ret0121),le(V10, 1 + (1 + 0), Ret0131),fun3(Ret0101, Ret0111, Ret0121, Ret0131, V9, V10, Ret014),fun1(V10, 0, Ret12)],[Out = 1 + Ret014 + Ret12,V = V9,V10 >= 0,V2 = V10,V9 >= 0]).
eq(fun2(V, V2, Out),1,[le(V11, 0, Ret0102),le(V12, 0, Ret0112),le(V12, 1 + 0, Ret0122),le(V12, 1 + (1 + 0), Ret0132),fun3(Ret0102, Ret0112, Ret0122, Ret0132, V11, V12, Ret015),fun1(V12, 1 + 0, Ret13)],[Out = 1 + Ret015 + Ret13,V = V11,V12 >= 0,V2 = V12,V11 >= 0]).
eq(fun2(V, V2, Out),1,[le(V14, 0, Ret0103),le(V13, 0, Ret0113),le(V13, 1 + 0, Ret0123),le(V13, 1 + (1 + 0), Ret0133),fun3(Ret0103, Ret0113, Ret0123, Ret0133, V14, V13, Ret016),fun1(V13, 1 + (1 + 0), Ret14)],[Out = 1 + Ret016 + Ret14,V = V14,V13 >= 0,V2 = V13,V14 >= 0]).
eq(fun3(V, V2, V19, V18, V15, V16, Out),1,[fun4(V23, V17, V22, V21, V20, Ret15)],[Out = 1 + Ret15,V = 2,V17 >= 0,V15 = V21,V16 = V20,V23 >= 0,V20 >= 0,V18 = V22,V2 = V23,V22 >= 0,V21 >= 0,V19 = V17]).
eq(fun3(V, V2, V19, V18, V15, V16, Out),1,[p(V28, Ret0104),fun2(Ret0104, 1 + V27, Ret017),fun(V28, Ret16)],[Out = 1 + Ret017 + Ret16,V25 >= 0,V = 1,V15 = V28,V16 = V27,V24 >= 0,V27 >= 0,V18 = V26,V2 = V24,V26 >= 0,V28 >= 0,V19 = V25]).
eq(fun4(V, V2, V19, V18, V15, Out),1,[],[Out = 0,V = 2,V29 >= 0,V15 = V30,V32 >= 0,V18 = V31,V2 = V32,V31 >= 0,V30 >= 0,V19 = V29]).
eq(fun4(V, V2, V19, V18, V15, Out),1,[fun5(V35, V36, V34, V33, Ret17)],[Out = 1 + Ret17,V36 >= 0,V = 1,V15 = V33,V35 >= 0,V18 = V34,V2 = V35,V34 >= 0,V33 >= 0,V19 = V36]).
eq(fun5(V, V2, V19, V18, Out),1,[],[Out = 0,V = 2,V38 >= 0,V37 >= 0,V18 = V39,V2 = V37,V39 >= 0,V19 = V38]).
eq(fun5(V, V2, V19, V18, Out),1,[fun6(V41, V42, V40, Ret18)],[Out = 1 + Ret18,V42 >= 0,V = 1,V41 >= 0,V18 = V40,V2 = V41,V40 >= 0,V19 = V42]).
eq(fun6(V, V2, V19, Out),1,[],[Out = 0,V = 2,V43 >= 0,V44 >= 0,V2 = V44,V19 = V43]).
eq(fun6(V, V2, V19, Out),1,[p(V45, Ret00110),p(Ret00110, Ret0011),fun2(1 + V46, Ret0011, Ret001),p(V45, Ret0105),fun(Ret0105, Ret018),fun(V45, Ret19)],[Out = 1 + Ret001 + Ret018 + Ret19,V45 >= 0,V = 1,V46 >= 0,V2 = V46,V19 = V45]).
eq(p(V, Out),0,[],[Out = V47,V = 1 + V47,V47 >= 0]).
eq(p(V, Out),0,[],[Out = 0,V = 0]).
eq(le(V, V2, Out),0,[],[Out = 2,V48 >= 0,V = 0,V2 = V48]).
eq(le(V, V2, Out),0,[],[Out = 1,V = 1 + V49,V49 >= 0,V2 = 0]).
eq(le(V, V2, Out),0,[le(V50, V51, Ret)],[Out = Ret,V51 >= 0,V = 1 + V50,V50 >= 0,V2 = 1 + V51]).
eq(average(V, V2, Out),0,[le(V52, 0, Ret0),le(V53, 0, Ret110),le(V53, 1 + 0, Ret2),le(V53, 1 + (1 + 0), Ret3),if(Ret0, Ret110, Ret2, Ret3, V52, V53, Ret4)],[Out = Ret4,V = V52,V53 >= 0,V2 = V53,V52 >= 0]).
eq(if(V, V2, V19, V18, V15, V16, Out),0,[if2(V55, V57, V54, V56, V58, Ret5)],[Out = Ret5,V = 2,V57 >= 0,V15 = V56,V16 = V58,V55 >= 0,V58 >= 0,V18 = V54,V2 = V55,V54 >= 0,V56 >= 0,V19 = V57]).
eq(if(V, V2, V19, V18, V15, V16, Out),0,[p(V61, Ret02),average(Ret02, 1 + V60, Ret6)],[Out = Ret6,V63 >= 0,V = 1,V15 = V61,V16 = V60,V62 >= 0,V60 >= 0,V18 = V59,V2 = V62,V59 >= 0,V61 >= 0,V19 = V63]).
eq(if2(V, V2, V19, V18, V15, Out),0,[],[Out = 0,V = 2,V67 >= 0,V15 = V64,V66 >= 0,V18 = V65,V2 = V66,V65 >= 0,V64 >= 0,V19 = V67]).
eq(if2(V, V2, V19, V18, V15, Out),0,[if3(V69, V71, V70, V68, Ret7)],[Out = Ret7,V71 >= 0,V = 1,V15 = V68,V69 >= 0,V18 = V70,V2 = V69,V70 >= 0,V68 >= 0,V19 = V71]).
eq(if3(V, V2, V19, V18, Out),0,[],[Out = 0,V = 2,V72 >= 0,V74 >= 0,V18 = V73,V2 = V74,V73 >= 0,V19 = V72]).
eq(if3(V, V2, V19, V18, Out),0,[if4(V77, V76, V75, Ret8)],[Out = Ret8,V76 >= 0,V = 1,V77 >= 0,V18 = V75,V2 = V77,V75 >= 0,V19 = V76]).
eq(if4(V, V2, V19, Out),0,[],[Out = 1,V = 2,V78 >= 0,V79 >= 0,V2 = V79,V19 = V78]).
eq(if4(V, V2, V19, Out),0,[p(V80, Ret10),p(Ret10, Ret111),average(1 + V81, Ret111, Ret9)],[Out = Ret9,V80 >= 0,V = 1,V81 >= 0,V2 = V81,V19 = V80]).
eq(p(V, Out),0,[],[Out = 0,V82 >= 0,V = V82]).
eq(le(V, V2, Out),0,[],[Out = 0,V84 >= 0,V83 >= 0,V = V84,V2 = V83]).
eq(average(V, V2, Out),0,[],[Out = 0,V86 >= 0,V85 >= 0,V = V86,V2 = V85]).
eq(if(V, V2, V19, V18, V15, V16, Out),0,[],[Out = 0,V18 = V91,V87 >= 0,V90 >= 0,V16 = V89,V15 = V90,V19 = V92,V88 >= 0,V89 >= 0,V = V87,V2 = V88,V92 >= 0,V91 >= 0]).
eq(if2(V, V2, V19, V18, V15, Out),0,[],[Out = 0,V18 = V97,V93 >= 0,V96 >= 0,V15 = V96,V19 = V94,V95 >= 0,V = V93,V2 = V95,V94 >= 0,V97 >= 0]).
eq(if3(V, V2, V19, V18, Out),0,[],[Out = 0,V18 = V100,V99 >= 0,V19 = V101,V98 >= 0,V = V99,V2 = V98,V101 >= 0,V100 >= 0]).
eq(if4(V, V2, V19, Out),0,[],[Out = 0,V103 >= 0,V19 = V104,V102 >= 0,V = V103,V2 = V102,V104 >= 0]).
eq(fun(V, Out),0,[],[Out = 0,V105 >= 0,V = V105]).
eq(fun1(V, V2, Out),0,[],[Out = 0,V106 >= 0,V107 >= 0,V = V106,V2 = V107]).
eq(fun3(V, V2, V19, V18, V15, V16, Out),0,[],[Out = 0,V18 = V110,V108 >= 0,V113 >= 0,V16 = V112,V15 = V113,V19 = V111,V109 >= 0,V112 >= 0,V = V108,V2 = V109,V111 >= 0,V110 >= 0]).
eq(fun4(V, V2, V19, V18, V15, Out),0,[],[Out = 0,V18 = V118,V116 >= 0,V117 >= 0,V15 = V117,V19 = V115,V114 >= 0,V = V116,V2 = V114,V115 >= 0,V118 >= 0]).
eq(fun5(V, V2, V19, V18, Out),0,[],[Out = 0,V18 = V122,V121 >= 0,V19 = V119,V120 >= 0,V = V121,V2 = V120,V119 >= 0,V122 >= 0]).
eq(fun6(V, V2, V19, Out),0,[],[Out = 0,V125 >= 0,V19 = V123,V124 >= 0,V = V125,V2 = V124,V123 >= 0]).
input_output_vars(fun(V,Out),[V],[Out]).
input_output_vars(fun1(V,V2,Out),[V,V2],[Out]).
input_output_vars(fun2(V,V2,Out),[V,V2],[Out]).
input_output_vars(fun3(V,V2,V19,V18,V15,V16,Out),[V,V2,V19,V18,V15,V16],[Out]).
input_output_vars(fun4(V,V2,V19,V18,V15,Out),[V,V2,V19,V18,V15],[Out]).
input_output_vars(fun5(V,V2,V19,V18,Out),[V,V2,V19,V18],[Out]).
input_output_vars(fun6(V,V2,V19,Out),[V,V2,V19],[Out]).
input_output_vars(p(V,Out),[V],[Out]).
input_output_vars(le(V,V2,Out),[V,V2],[Out]).
input_output_vars(average(V,V2,Out),[V,V2],[Out]).
input_output_vars(if(V,V2,V19,V18,V15,V16,Out),[V,V2,V19,V18,V15,V16],[Out]).
input_output_vars(if2(V,V2,V19,V18,V15,Out),[V,V2,V19,V18,V15],[Out]).
input_output_vars(if3(V,V2,V19,V18,Out),[V,V2,V19,V18],[Out]).
input_output_vars(if4(V,V2,V19,Out),[V,V2,V19],[Out]).


CoFloCo proof output:
Preprocessing Cost Relations
=====================================

#### Computed strongly connected components 
0. non_recursive  : [p/2]
1. recursive  : [le/3]
2. recursive  : [average/3,if/7,if2/6,if3/5,if4/4]
3. non_recursive  : [fun/2]
4. recursive  : [fun1/3]
5. recursive [non_tail] : [fun2/3,fun3/7,fun4/6,fun5/5,fun6/4]
6. non_recursive  : [start/6]

#### Obtained direct recursion through partial evaluation 
0. SCC is partially evaluated into p/2
1. SCC is partially evaluated into le/3
2. SCC is partially evaluated into average/3
3. SCC is partially evaluated into fun/2
4. SCC is partially evaluated into fun1/3
5. SCC is partially evaluated into fun2/3
6. SCC is partially evaluated into start/6

Control-Flow Refinement of Cost Relations
=====================================

### Specialization of cost equations p/2 
* CE 28 is refined into CE [82] 
* CE 29 is refined into CE [83] 


### Cost equations --> "Loop" of p/2 
* CEs [82] --> Loop 27 
* CEs [83] --> Loop 28 

### Ranking functions of CR p(V,Out) 

#### Partial ranking functions of CR p(V,Out) 


### Specialization of cost equations le/3 
* CE 81 is refined into CE [84] 
* CE 79 is refined into CE [85] 
* CE 78 is refined into CE [86] 
* CE 80 is refined into CE [87] 


### Cost equations --> "Loop" of le/3 
* CEs [87] --> Loop 29 
* CEs [84] --> Loop 30 
* CEs [85] --> Loop 31 
* CEs [86] --> Loop 32 

### Ranking functions of CR le(V,V2,Out) 
* RF of phase [29]: [V,V2]

#### Partial ranking functions of CR le(V,V2,Out) 
* Partial RF of phase [29]:
  - RF of loop [29:1]:
    V
    V2


### Specialization of cost equations average/3 
* CE 71 is refined into CE [88] 
* CE 69 is refined into CE [89,90,91,92,93,94,95,96,97,98,99,100,101,102,103,104,105,106,107,108,109,110,111,112,113,114,115,116,117,118,119,120,121,122,123,124,125,126,127,128,129,130,131,132,133,134,135,136,137,138,139,140,141,142,143,144,145,146,147,148,149,150,151,152,153,154,155,156,157] 
* CE 73 is refined into CE [158] 
* CE 72 is refined into CE [159,160,161,162,163,164,165,166,167,168,169,170,171,172,173,174,175,176,177,178,179,180,181,182,183,184,185,186,187,188,189,190,191,192,193,194,195,196,197,198,199,200,201,202,203,204] 
* CE 70 is refined into CE [205,206,207] 


### Cost equations --> "Loop" of average/3 
* CEs [178,200] --> Loop 33 
* CEs [177,199] --> Loop 34 
* CEs [172,180,182,194,202,204] --> Loop 35 
* CEs [171,179,181,193,201,203] --> Loop 36 
* CEs [160,162,164,166,168,170,174,176,184,186,188,190,192,196,198] --> Loop 37 
* CEs [159,161,163,165,167,169,173,175,183,185,187,189,191,195,197] --> Loop 38 
* CEs [207] --> Loop 39 
* CEs [205,206] --> Loop 40 
* CEs [122,123,133,134,145,146,156,157] --> Loop 41 
* CEs [112,113,114,115,124,125,126,135,136,137,138,147,148,149] --> Loop 42 
* CEs [88] --> Loop 43 
* CEs [98,109,121,132,144,155] --> Loop 44 
* CEs [95,99,100,106,110,111,118,129,141,152] --> Loop 45 
* CEs [89,90,91,92,93,94,96,97,101,102,103,104,105,107,108,116,117,119,120,127,128,130,131,139,140,142,143,150,151,153,154,158] --> Loop 46 

### Ranking functions of CR average(V,V2,Out) 
* RF of phase [33,34,35,36,37,38,39,40]: [3*V+2*V2-2,9*V+8*V2-8]

#### Partial ranking functions of CR average(V,V2,Out) 
* Partial RF of phase [33,34,35,36,37,38,39,40]:
  - RF of loop [33:1,34:1,35:1,36:1]:
    -V2+3 depends on loops [39:1,40:1] 
  - RF of loop [33:1,34:1,35:1,36:1,37:1,38:1]:
    V depends on loops [39:1,40:1] 
  - RF of loop [39:1]:
    V2/2-1 depends on loops [33:1,34:1,35:1,36:1,37:1,38:1] 
  - RF of loop [39:1,40:1]:
    -V+1 depends on loops [33:1,34:1,35:1,36:1,37:1,38:1] 
  - RF of loop [40:1]:
    V2/3-2/3 depends on loops [33:1,34:1,35:1,36:1,37:1,38:1] 


### Specialization of cost equations fun/2 
* CE 66 is refined into CE [208] 
* CE 68 is refined into CE [209] 
* CE 67 is refined into CE [210] 


### Cost equations --> "Loop" of fun/2 
* CEs [208] --> Loop 47 
* CEs [209] --> Loop 48 
* CEs [210] --> Loop 49 

### Ranking functions of CR fun(V,Out) 

#### Partial ranking functions of CR fun(V,Out) 


### Specialization of cost equations fun1/3 
* CE 75 is refined into CE [211] 
* CE 74 is refined into CE [212] 
* CE 77 is refined into CE [213] 
* CE 76 is refined into CE [214] 


### Cost equations --> "Loop" of fun1/3 
* CEs [214] --> Loop 50 
* CEs [211] --> Loop 51 
* CEs [212,213] --> Loop 52 

### Ranking functions of CR fun1(V,V2,Out) 
* RF of phase [50]: [V,V2]

#### Partial ranking functions of CR fun1(V,V2,Out) 
* Partial RF of phase [50]:
  - RF of loop [50:1]:
    V
    V2


### Specialization of cost equations fun2/3 
* CE 62 is refined into CE [215,216,217,218,219,220,221,222,223,224,225,226,227,228,229,230,231,232,233,234,235,236,237,238,239,240,241,242,243,244,245,246,247,248,249,250,251,252,253,254,255,256,257,258,259,260,261,262,263,264,265,266,267,268,269,270,271,272,273,274,275,276,277,278,279,280,281,282,283,284,285,286,287,288,289,290,291,292,293,294,295,296,297,298,299,300,301,302,303,304,305,306,307,308,309,310,311,312,313,314,315,316,317,318,319,320,321,322,323,324,325,326,327,328,329,330,331,332,333,334,335,336,337,338,339,340,341,342,343,344,345,346,347,348,349,350,351,352,353,354,355,356,357,358,359,360,361,362,363,364,365,366,367,368,369,370,371,372,373,374,375,376,377,378,379,380,381,382,383,384,385,386,387,388,389,390,391,392,393,394,395,396,397,398,399,400,401,402] 
* CE 63 is refined into CE [403,404,405,406,407,408,409,410,411,412,413,414,415,416,417,418,419,420,421,422,423,424,425,426,427,428,429,430,431,432,433,434,435,436,437,438,439,440,441,442,443,444,445,446,447,448,449,450,451,452,453,454,455,456,457,458,459,460,461,462,463,464,465,466,467,468,469,470,471,472,473,474,475,476,477,478,479,480,481,482,483,484,485,486,487,488,489,490,491,492,493,494,495,496,497,498,499,500,501,502,503,504,505,506,507,508,509,510,511,512,513,514,515,516,517,518,519,520,521,522,523,524,525,526,527,528,529,530,531,532,533,534,535,536,537,538,539,540,541,542,543,544,545,546,547,548,549,550,551,552,553,554,555,556,557,558,559,560,561,562,563,564,565,566,567,568,569,570,571,572,573,574,575,576,577,578,579,580,581,582,583,584,585,586,587,588,589,590,591,592,593,594,595,596,597,598,599,600,601,602,603,604,605,606] 
* CE 64 is refined into CE [607,608,609,610,611,612,613,614,615,616,617,618,619,620,621,622,623,624,625,626,627,628,629,630,631,632,633,634,635,636,637,638,639,640,641,642,643,644,645,646,647,648,649,650,651,652,653,654,655,656,657,658,659,660,661,662,663,664,665,666,667,668,669,670,671,672,673,674,675,676,677,678,679,680,681,682,683,684,685,686,687,688,689,690,691,692,693,694,695,696,697,698,699,700,701,702,703,704,705,706,707,708,709,710,711,712,713,714,715,716,717,718,719,720,721,722,723,724,725,726,727,728,729,730,731,732,733,734,735,736,737,738,739,740,741,742,743,744,745,746,747,748,749,750,751,752,753,754,755,756,757,758,759,760,761,762] 
* CE 65 is refined into CE [763,764,765,766,767,768,769,770,771,772,773,774,775,776,777,778,779,780,781,782,783,784,785,786,787,788,789,790,791,792,793,794,795,796,797,798,799,800,801,802,803,804,805,806,807,808,809,810,811,812,813,814,815,816,817,818,819,820,821,822,823,824,825,826,827,828,829,830,831,832,833,834,835,836,837,838,839,840,841,842,843,844,845,846,847,848,849,850,851,852,853,854,855,856,857,858,859,860,861,862,863,864,865,866,867,868,869,870,871,872,873,874,875,876,877,878,879,880,881,882,883,884,885,886,887,888,889,890,891,892,893,894,895,896,897,898,899,900,901,902,903,904,905,906,907,908,909,910,911,912,913,914,915,916,917,918,919,920,921,922,923,924,925,926,927,928,929,930,931,932,933,934,935,936,937,938,939,940,941,942,943,944,945,946] 
* CE 34 is refined into CE [947,948,949,950,951,952,953,954,955,956,957,958,959,960,961,962,963,964,965,966,967,968,969,970,971,972,973,974,975,976,977,978,979,980,981,982,983,984,985,986,987,988,989,990,991,992,993,994,995,996,997,998,999,1000,1001,1002,1003,1004,1005,1006,1007,1008,1009,1010,1011,1012,1013,1014,1015,1016,1017,1018] 
* CE 35 is refined into CE [1019,1020,1021,1022,1023,1024,1025,1026,1027,1028,1029,1030,1031,1032,1033,1034,1035,1036,1037,1038,1039,1040,1041,1042,1043,1044,1045,1046,1047,1048,1049,1050,1051,1052,1053,1054,1055,1056,1057,1058,1059,1060,1061,1062,1063,1064,1065,1066,1067,1068,1069,1070,1071,1072,1073,1074,1075,1076,1077,1078,1079,1080,1081,1082,1083,1084,1085,1086,1087,1088,1089,1090] 
* CE 36 is refined into CE [1091,1092,1093,1094,1095,1096,1097,1098,1099,1100,1101,1102,1103,1104,1105,1106,1107,1108,1109,1110,1111,1112,1113,1114,1115,1116,1117,1118,1119,1120,1121,1122,1123,1124,1125,1126,1127,1128,1129,1130,1131,1132,1133,1134,1135,1136,1137,1138] 
* CE 37 is refined into CE [1139,1140,1141,1142,1143,1144,1145,1146,1147,1148,1149,1150,1151,1152,1153,1154,1155,1156,1157,1158,1159,1160,1161,1162] 
* CE 30 is refined into CE [1163,1164,1165,1166,1167,1168,1169,1170] 
* CE 31 is refined into CE [1171,1172,1173,1174,1175,1176,1177,1178,1179] 
* CE 32 is refined into CE [1180,1181,1182,1183,1184,1185] 
* CE 33 is refined into CE [1186,1187,1188] 
* CE 38 is refined into CE [1189,1190] 
* CE 39 is refined into CE [1191,1192,1193] 
* CE 40 is refined into CE [1194,1195] 
* CE 41 is refined into CE [1196] 
* CE 42 is refined into CE [1197,1198,1199,1200,1201,1202,1203,1204,1205,1206,1207,1208,1209,1210,1211,1212,1213,1214,1215,1216] 
* CE 43 is refined into CE [1217,1218,1219,1220,1221,1222,1223,1224,1225,1226,1227,1228,1229,1230,1231,1232,1233,1234,1235,1236,1237,1238] 
* CE 44 is refined into CE [1239,1240,1241,1242,1243,1244,1245,1246,1247,1248,1249,1250,1251,1252,1253,1254] 
* CE 45 is refined into CE [1255,1256,1257,1258,1259,1260,1261,1262] 
* CE 46 is refined into CE [1263,1264,1265,1266] 
* CE 47 is refined into CE [1267,1268,1269,1270] 
* CE 48 is refined into CE [1271,1272,1273,1274] 
* CE 49 is refined into CE [1275,1276] 
* CE 50 is refined into CE [1277,1278,1279,1280,1281,1282,1283,1284,1285,1286,1287,1288,1289,1290,1291,1292,1293,1294,1295,1296,1297,1298,1299,1300,1301,1302,1303,1304,1305,1306,1307,1308,1309,1310,1311,1312,1313,1314,1315,1316,1317,1318,1319,1320,1321,1322,1323] 
* CE 51 is refined into CE [1324,1325,1326,1327,1328,1329,1330,1331,1332,1333,1334,1335,1336,1337,1338,1339,1340,1341,1342,1343,1344,1345,1346,1347,1348,1349,1350,1351,1352,1353,1354,1355,1356,1357,1358,1359,1360,1361,1362,1363,1364,1365,1366,1367,1368,1369,1370,1371,1372,1373,1374] 
* CE 52 is refined into CE [1375,1376,1377,1378,1379,1380,1381,1382,1383,1384,1385,1386,1387,1388,1389,1390,1391,1392,1393,1394,1395,1396,1397,1398,1399,1400,1401,1402,1403,1404,1405,1406,1407,1408,1409,1410,1411,1412,1413] 
* CE 53 is refined into CE [1414,1415,1416,1417,1418,1419,1420,1421,1422,1423,1424,1425,1426,1427,1428,1429,1430,1431,1432,1433,1434,1435,1436] 
* CE 54 is refined into CE [1437,1438,1439,1440] 
* CE 55 is refined into CE [1441,1442,1443,1444] 
* CE 56 is refined into CE [1445,1446,1447,1448] 
* CE 57 is refined into CE [1449,1450,1451,1452] 
* CE 58 is refined into CE [1453,1454,1455,1456,1457,1458,1459,1460,1461,1462,1463,1464,1465,1466,1467,1468,1469,1470,1471,1472,1473,1474,1475,1476,1477,1478,1479,1480,1481,1482,1483,1484,1485,1486,1487,1488,1489,1490,1491,1492,1493,1494,1495,1496,1497,1498,1499,1500,1501,1502,1503,1504,1505,1506,1507,1508,1509,1510,1511,1512,1513,1514,1515,1516,1517,1518,1519,1520,1521,1522,1523,1524,1525,1526,1527,1528,1529,1530,1531,1532,1533,1534,1535,1536,1537,1538,1539,1540,1541,1542,1543,1544,1545,1546,1547,1548,1549,1550,1551,1552,1553,1554,1555,1556,1557,1558,1559,1560,1561,1562,1563,1564,1565,1566,1567,1568,1569,1570,1571,1572,1573,1574,1575,1576,1577,1578,1579,1580,1581,1582,1583,1584,1585,1586,1587,1588,1589,1590,1591,1592,1593] 
* CE 59 is refined into CE [1594,1595,1596,1597,1598,1599,1600,1601,1602,1603,1604,1605,1606,1607,1608,1609,1610,1611,1612,1613,1614,1615,1616,1617,1618,1619,1620,1621,1622,1623,1624,1625,1626,1627,1628,1629,1630,1631,1632,1633,1634,1635,1636,1637,1638,1639,1640,1641,1642,1643,1644,1645,1646,1647,1648,1649,1650,1651,1652,1653,1654,1655,1656,1657,1658,1659,1660,1661,1662,1663,1664,1665,1666,1667,1668,1669,1670,1671,1672,1673,1674,1675,1676,1677,1678,1679,1680,1681,1682,1683,1684,1685,1686,1687,1688,1689,1690,1691,1692,1693,1694,1695,1696,1697,1698,1699,1700,1701,1702,1703,1704,1705,1706,1707,1708,1709,1710,1711,1712,1713,1714,1715,1716,1717,1718,1719,1720,1721,1722,1723,1724,1725,1726,1727,1728,1729,1730,1731,1732,1733,1734,1735,1736,1737,1738,1739,1740,1741,1742,1743,1744,1745,1746] 
* CE 60 is refined into CE [1747,1748,1749,1750,1751,1752,1753,1754,1755,1756,1757,1758,1759,1760,1761,1762,1763,1764,1765,1766,1767,1768,1769,1770,1771,1772,1773,1774,1775,1776,1777,1778,1779,1780,1781,1782,1783,1784,1785,1786,1787,1788,1789,1790,1791,1792,1793,1794,1795,1796,1797,1798,1799,1800,1801,1802,1803,1804,1805,1806,1807,1808,1809,1810,1811,1812,1813,1814,1815,1816,1817,1818,1819,1820,1821,1822,1823,1824,1825,1826,1827,1828,1829,1830,1831,1832,1833,1834,1835,1836,1837,1838,1839,1840,1841,1842,1843,1844,1845,1846,1847,1848,1849,1850,1851,1852,1853,1854,1855,1856,1857,1858,1859,1860,1861,1862,1863] 
* CE 61 is refined into CE [1864,1865,1866,1867,1868,1869,1870,1871,1872,1873,1874,1875,1876,1877,1878,1879,1880,1881,1882,1883,1884,1885,1886,1887,1888,1889,1890,1891,1892,1893,1894,1895,1896,1897,1898,1899,1900,1901,1902,1903,1904,1905,1906,1907,1908,1909,1910,1911,1912,1913,1914,1915,1916,1917,1918,1919,1920,1921,1922,1923,1924,1925,1926,1927,1928,1929,1930,1931,1932,1933,1934,1935,1936,1937,1938,1939,1940,1941,1942,1943,1944,1945,1946,1947,1948,1949,1950,1951,1952,1953,1954,1955,1956,1957,1958,1959,1960,1961,1962,1963,1964,1965,1966,1967,1968,1969,1970,1971,1972,1973,1974,1975,1976,1977,1978] 


### Cost equations --> "Loop" of fun2/3 
* CEs [1505,1508,1513,1516,1528,1531,1536,1539,1552,1555,1560,1563,1575,1578,1583,1586] --> Loop 53 
* CEs [1650,1653,1656,1659,1662,1665,1675,1678,1681,1684,1687,1690,1701,1704,1707,1710,1713,1716,1726,1729,1732,1735,1738,1741] --> Loop 54 
* CEs [1511,1519,1534,1542,1558,1566,1581,1589,1666,1691,1717,1742,1800,1819,1839,1858,1905,1927,1951,1973] --> Loop 55 
* CEs [1521,1523,1544,1546,1568,1570,1591,1593,1657,1668,1670,1682,1693,1695,1702,1705,1708,1711,1714,1719,1721,1727,1730,1733,1736,1739,1744,1746,1794,1802,1804,1813,1821,1823,1829,1831,1833,1835,1837,1841,1843,1848,1850,1852,1854,1856,1860,1862,1899,1907,1909,1921,1929,1931,1945,1953,1955,1967,1975,1977] --> Loop 56 
* CEs [1520,1522,1543,1545,1567,1569,1590,1592,1667,1669,1692,1694,1718,1720,1743,1745,1803,1805,1822,1824,1842,1844,1861,1863,1908,1910,1930,1932,1954,1956,1976,1978] --> Loop 57 
* CEs [1651,1654,1660,1663,1676,1679,1685,1688,1790,1792,1796,1798,1809,1811,1815,1817,1887,1889,1891,1893,1895,1897,1901,1903,1911,1913,1915,1917,1919,1923,1925,1933,1935,1937,1939,1941,1943,1947,1949,1957,1959,1961,1963,1965,1969,1971] --> Loop 58 
* CEs [1500,1501,1502,1503,1524,1525,1526,1547,1548,1549,1550,1571,1572,1573,1645,1646,1647,1648,1671,1672,1673,1696,1697,1698,1699,1722,1723,1724,1786,1787,1788,1789,1806,1807,1808,1825,1826,1827,1828,1845,1846,1847,1888,1890,1892,1894,1912,1914,1916,1934,1936,1938,1940,1958,1960,1962] --> Loop 59 
* CEs [1286,1291,1294,1309,1314,1317] --> Loop 60 
* CEs [1164,1167] --> Loop 61 
* CEs [1173,1176,1180,1182,1202,1207,1210,1218,1221,1227,1230,1282,1285,1290,1293,1305,1308,1313,1316] --> Loop 62 
* CEs [1172,1175,1178,1192,1198,1201,1206,1209] --> Loop 63 
* CEs [1165,1168,1170,1179,1184,1190,1193,1194,1224,1233] --> Loop 64 
* CEs [1169,1177,1185,1188,1189,1191,1195,1196,1204,1212,1234,1249,1335,1344,1360,1369] --> Loop 65 
* CEs [1211,1232,1250,1260,1288,1296,1311,1319,1345,1370,1389,1408,1605,1614,1630,1639] --> Loop 66 
* CEs [1295,1318,1343,1368,1390,1409,1423,1434,1462,1467,1470,1472,1485,1490,1493,1495,1556,1561,1564,1579,1584,1587,1615,1640,1761,1780] --> Loop 67 
* CEs [1471,1494,1518,1541,1565,1588,1613,1638,1664,1689,1715,1740,1762,1781,1801,1820,1840,1859,1873,1884,1906,1928,1952,1974] --> Loop 68 
* CEs [1163,1166,1171,1174,1181,1183,1186,1187,1199,1214,1216,1219,1222,1225,1228,1231,1236,1238,1239,1241,1243,1245,1247,1251,1253,1264,1266,1268,1270,1271,1273,1329,1332,1338,1341,1354,1357,1363,1366,1458,1461,1466,1469,1481,1484,1489,1492] --> Loop 69 
* CEs [1197,1200,1203,1205,1208,1213,1215,1217,1220,1223,1226,1229,1235,1237,1240,1242,1244,1246,1248,1252,1254,1255,1256,1257,1258,1259,1261,1262,1263,1265,1267,1269,1272,1274,1275,1276,1283,1298,1300,1306,1321,1323,1330,1333,1336,1339,1342,1347,1349,1355,1358,1361,1364,1367,1372,1374,1379,1381,1383,1385,1387,1391,1393,1398,1400,1402,1404,1406,1410,1412,1599,1602,1608,1611,1624,1627,1633,1636] --> Loop 70 
* CEs [1287,1297,1299,1310,1320,1322,1334,1346,1348,1359,1371,1373,1384,1392,1394,1403,1411,1413,1420,1424,1425,1431,1435,1436,1459,1464,1474,1476,1482,1487,1497,1499,1506,1509,1514,1517,1529,1532,1537,1540,1553,1576,1606,1617,1619,1631,1642,1644,1755,1763,1765,1774,1782,1784] --> Loop 71 
* CEs [1463,1473,1475,1486,1496,1498,1510,1533,1557,1580,1604,1616,1618,1629,1641,1643,1655,1680,1706,1731,1756,1764,1766,1775,1783,1785,1795,1814,1834,1853,1870,1874,1875,1881,1885,1886,1900,1922,1946,1968] --> Loop 72 
* CEs [1277,1278,1279,1280,1281,1284,1289,1292,1301,1302,1303,1304,1307,1312,1315,1324,1325,1326,1327,1328,1331,1337,1340,1350,1351,1352,1353,1356,1362,1365,1375,1376,1377,1378,1380,1382,1386,1388,1395,1396,1397,1399,1401,1405,1407,1414,1415,1416,1417,1418,1419,1421,1422,1426,1427,1428,1429,1430,1432,1433,1437,1438,1439,1440,1441,1442,1443,1444,1445,1446,1447,1448,1449,1450,1451,1452,1600,1603,1609,1612,1625,1628,1634,1637,1751,1753,1757,1759,1770,1772,1776,1778] --> Loop 73 
* CEs [1453,1454,1455,1456,1457,1460,1465,1468,1477,1478,1479,1480,1483,1488,1491,1504,1507,1512,1515,1527,1530,1535,1538,1551,1554,1559,1562,1574,1577,1582,1585,1594,1595,1596,1597,1598,1601,1607,1610,1620,1621,1622,1623,1626,1632,1635,1649,1652,1658,1661,1674,1677,1683,1686,1700,1703,1709,1712,1725,1728,1734,1737,1747,1748,1749,1750,1752,1754,1758,1760,1767,1768,1769,1771,1773,1777,1779,1791,1793,1797,1799,1810,1812,1816,1818,1830,1832,1836,1838,1849,1851,1855,1857,1864,1865,1866,1867,1868,1869,1871,1872,1876,1877,1878,1879,1880,1882,1883,1896,1898,1902,1904,1918,1920,1924,1926,1942,1944,1948,1950,1964,1966,1970,1972] --> Loop 74 
* CEs [241,253,273,285,333,345,365,377] --> Loop 75 
* CEs [235,247,267,279,327,339,359,371] --> Loop 76 
* CEs [238,250,270,282,330,342,362,374,429,441,453,465,477,489,529,541,553,565,577,589] --> Loop 77 
* CEs [254,274,286,294,346,366,378,386,450,486,490,550,586,590,669,745,841,929] --> Loop 78 
* CEs [251,271,283,292,293,343,363,375,384,385,487,488,587,588,667,670,743,746,839,842,927,930] --> Loop 79 
* CEs [291,383,485,585,668,744,840,928] --> Loop 80 
* CEs [232,244,264,276,324,336,356,368,423,435,447,459,471,483,523,535,547,559,571,583] --> Loop 81 
* CEs [248,268,280,290,340,360,372,382,444,480,484,544,580,584,665,741,837,925] --> Loop 82 
* CEs [245,265,277,288,289,337,357,369,380,381,481,482,581,582,663,666,739,742,835,838,923,926] --> Loop 83 
* CEs [287,379,479,579,664,740,836,924] --> Loop 84 
* CEs [242,262,302,310,334,354,394,402,454,498,506,554,598,606,645,677,685,721,753,761,817,849,857,905,937,945] --> Loop 85 
* CEs [239,260,261,300,301,308,309,331,352,353,392,393,400,401,451,452,496,497,504,505,551,552,596,597,604,605,643,646,675,678,683,686,719,722,751,754,759,762,815,818,847,850,855,858,903,906,935,938,943,946] --> Loop 86 
* CEs [259,299,307,351,391,399,449,495,503,549,595,603,644,676,684,720,752,760,816,848,856,904,936,944] --> Loop 87 
* CEs [236,258,298,306,328,350,390,398,448,494,502,548,594,602,641,673,681,717,749,757,813,845,853,901,933,941] --> Loop 88 
* CEs [233,256,257,296,297,304,305,325,348,349,388,389,396,397,445,446,492,493,500,501,545,546,592,593,600,601,639,642,671,674,679,682,715,718,747,750,755,758,811,814,843,846,851,854,899,902,931,934,939,942] --> Loop 89 
* CEs [255,295,303,347,387,395,443,491,499,543,591,599,640,672,680,716,748,756,812,844,852,900,932,940] --> Loop 90 
* CEs [426,430,438,442,462,466,474,478,526,530,538,542,562,566,574,578,629,637,653,661,705,713,729,737,769,777,785,793,801,809,825,833,865,873,881,889,897,913,921] --> Loop 91 
* CEs [218,222,226,230,240,252,272,284,314,318,322,332,344,364,376,406,410,414,418,427,428,439,440,463,464,475,476,510,514,518,527,528,539,540,563,564,575,576,610,614,618,622,627,630,635,638,651,654,659,662,690,694,698,703,706,711,714,727,730,735,738,767,770,775,778,783,786,791,794,799,802,807,810,823,826,831,834,863,866,871,874,879,882,887,890,895,898,911,914,919,922] --> Loop 92 
* CEs [217,221,225,229,237,249,269,281,313,317,321,329,341,361,373,405,409,413,417,425,437,461,473,509,513,517,525,537,561,573,609,613,617,621,628,636,652,660,689,693,697,704,712,728,736,768,776,784,792,800,808,824,832,864,872,880,888,896,912,920] --> Loop 93 
* CEs [420,424,432,436,456,460,468,472,520,524,532,536,556,560,568,572,625,633,649,657,701,709,725,733,765,773,781,789,797,805,821,829,861,869,877,885,893,909,917] --> Loop 94 
* CEs [216,220,224,228,234,246,266,278,312,316,320,326,338,358,370,404,408,412,416,421,422,433,434,457,458,469,470,508,512,516,521,522,533,534,557,558,569,570,608,612,616,620,623,626,631,634,647,650,655,658,688,692,696,699,702,707,710,723,726,731,734,763,766,771,774,779,782,787,790,795,798,803,806,819,822,827,830,859,862,867,870,875,878,883,886,891,894,907,910,915,918] --> Loop 95 
* CEs [215,219,223,227,231,243,263,275,311,315,319,323,335,355,367,403,407,411,415,419,431,455,467,507,511,515,519,531,555,567,607,611,615,619,624,632,648,656,687,691,695,700,708,724,732,764,772,780,788,796,804,820,828,860,868,876,884,892,908,916] --> Loop 96 
* CEs [999] --> Loop 97 
* CEs [996,1017,1071] --> Loop 98 
* CEs [1000,1005,1011,1014,1068,1072,1089,1125] --> Loop 99 
* CEs [997,998,1002,1008,1018,1069,1070,1077,1083,1086,1090,1123,1126,1137,1156] --> Loop 100 
* CEs [995,1006,1012,1015,1016,1067,1074,1078,1080,1084,1087,1088,1124,1129,1133,1135,1138,1155,1162] --> Loop 101 
* CEs [1003,1004,1009,1010,1013,1075,1076,1081,1082,1085,1127,1130,1131,1134,1136,1158,1160,1161] --> Loop 102 
* CEs [1001,1007,1073,1079,1128,1132,1157,1159] --> Loop 103 
* CEs [951,975] --> Loop 104 
* CEs [948,969,972,993,1023,1047] --> Loop 105 
* CEs [952,957,963,966,976,981,987,990,1020,1024,1041,1044,1048,1065,1093,1109] --> Loop 106 
* CEs [949,950,954,960,970,973,974,978,984,994,1021,1022,1029,1035,1038,1042,1045,1046,1053,1059,1062,1066,1091,1094,1105,1107,1110,1121,1140,1148] --> Loop 107 
* CEs [947,958,964,967,968,971,982,988,991,992,1019,1026,1030,1032,1036,1039,1040,1043,1050,1054,1056,1060,1063,1064,1092,1097,1101,1103,1106,1108,1113,1117,1119,1122,1139,1146,1147,1154] --> Loop 108 
* CEs [955,956,961,962,965,979,980,985,986,989,1027,1028,1033,1034,1037,1051,1052,1057,1058,1061,1095,1098,1099,1102,1104,1111,1114,1115,1118,1120,1142,1144,1145,1150,1152,1153] --> Loop 109 
* CEs [953,959,977,983,1025,1031,1049,1055,1096,1100,1112,1116,1141,1143,1149,1151] --> Loop 110 

### Ranking functions of CR fun2(V,V2,Out) 
* RF of phase [75,76,77,78,79,80,81,82,83,84,85,86,87,88,89,90,91,92,93,94,95,96,97,98,99,100,101,102,103,104,105,106,107,108,109,110]: [3*V+2*V2-2,9*V+8*V2-8]

#### Partial ranking functions of CR fun2(V,V2,Out) 
* Partial RF of phase [75,76,77,78,79,80,81,82,83,84,85,86,87,88,89,90,91,92,93,94,95,96,97,98,99,100,101,102,103,104,105,106,107,108,109,110]:
  - RF of loop [75:1,76:1,77:1,78:1,79:1,80:1,81:1,82:1,83:1,84:1,85:1,86:1,87:1,88:1,89:1,90:1,91:1,92:1,93:1,94:1,95:1,96:1]:
    V depends on loops [97:1,98:1,99:1,100:1,101:1,102:1,103:1,104:1,105:1,106:1,107:1,108:1,109:1,110:1] 
  - RF of loop [80:1,84:1,87:1,90:1]:
    -V2+3 depends on loops [97:1,98:1,99:1,100:1,101:1,102:1,103:1,104:1,105:1,106:1,107:1,108:1,109:1,110:1] 
  - RF of loop [97:1,98:1,99:1,100:1,101:1,102:1,103:1]:
    V2/2-1 depends on loops [75:1,76:1,77:1,78:1,79:1,80:1,81:1,82:1,83:1,84:1,85:1,86:1,87:1,88:1,89:1,90:1,91:1,92:1,93:1,94:1,95:1,96:1] 
  - RF of loop [97:1,98:1,99:1,100:1,101:1,102:1,103:1,104:1,105:1,106:1,107:1,108:1,109:1,110:1]:
    -V+1 depends on loops [75:1,76:1,77:1,78:1,79:1,80:1,81:1,82:1,83:1,84:1,85:1,86:1,87:1,88:1,89:1,90:1,91:1,92:1,93:1,94:1,95:1,96:1] 
  - RF of loop [104:1,105:1,106:1,107:1,108:1,109:1,110:1]:
    V2/3-2/3 depends on loops [75:1,76:1,77:1,78:1,79:1,80:1,81:1,82:1,83:1,84:1,85:1,86:1,87:1,88:1,89:1,90:1,91:1,92:1,93:1,94:1,95:1,96:1] 


### Specialization of cost equations start/6 
* CE 15 is refined into CE [1979] 
* CE 14 is refined into CE [1980] 
* CE 9 is refined into CE [1981] 
* CE 1 is refined into CE [1982] 
* CE 5 is refined into CE [1983,1984,1985,1986,1987,1988,1989,1990,1991,1992,1993,1994,1995,1996,1997,1998,1999,2000,2001,2002,2003,2004,2005,2006,2007,2008,2009,2010,2011,2012,2013,2014,2015,2016,2017,2018,2019,2020,2021,2022,2023,2024,2025,2026,2027,2028,2029,2030,2031,2032,2033,2034,2035,2036,2037,2038,2039,2040,2041,2042,2043,2044,2045,2046,2047,2048,2049,2050,2051,2052,2053,2054,2055,2056,2057,2058,2059,2060,2061,2062,2063,2064,2065,2066,2067,2068,2069,2070,2071,2072,2073,2074,2075,2076,2077,2078,2079,2080,2081,2082,2083,2084,2085,2086,2087,2088,2089,2090,2091,2092,2093,2094,2095,2096,2097,2098,2099,2100,2101,2102,2103,2104,2105,2106,2107,2108,2109,2110,2111,2112,2113,2114,2115,2116,2117,2118,2119,2120] 
* CE 12 is refined into CE [2121] 
* CE 13 is refined into CE [2122] 
* CE 17 is refined into CE [2123,2124,2125,2126,2127,2128,2129,2130] 
* CE 11 is refined into CE [2131] 
* CE 10 is refined into CE [2132] 
* CE 2 is refined into CE [2133] 
* CE 3 is refined into CE [2134] 
* CE 4 is refined into CE [2135] 
* CE 6 is refined into CE [2136,2137,2138,2139,2140,2141,2142,2143,2144,2145,2146,2147,2148,2149,2150,2151,2152,2153,2154,2155,2156,2157,2158,2159,2160,2161,2162,2163,2164,2165,2166,2167,2168,2169,2170,2171,2172,2173,2174,2175,2176,2177,2178,2179,2180,2181,2182,2183,2184,2185,2186,2187,2188,2189,2190,2191,2192,2193,2194,2195,2196,2197,2198,2199,2200,2201,2202,2203,2204,2205,2206,2207,2208,2209,2210,2211,2212,2213,2214,2215,2216,2217,2218,2219,2220,2221,2222,2223,2224,2225,2226,2227,2228,2229,2230,2231,2232,2233,2234,2235,2236,2237,2238,2239,2240,2241,2242,2243,2244,2245,2246,2247,2248,2249,2250,2251,2252,2253,2254,2255,2256,2257,2258,2259,2260,2261,2262,2263,2264,2265,2266,2267,2268,2269,2270,2271,2272,2273] 
* CE 7 is refined into CE [2274,2275,2276,2277,2278,2279,2280,2281,2282,2283,2284,2285,2286,2287,2288,2289,2290,2291,2292,2293,2294,2295,2296,2297,2298,2299,2300,2301,2302,2303,2304,2305,2306,2307,2308,2309,2310,2311,2312,2313,2314,2315,2316,2317,2318,2319,2320,2321,2322,2323,2324,2325,2326,2327,2328,2329,2330,2331,2332,2333,2334,2335,2336,2337,2338,2339,2340,2341,2342,2343,2344,2345,2346,2347,2348,2349,2350,2351,2352,2353,2354,2355,2356,2357,2358,2359,2360,2361,2362,2363,2364,2365,2366,2367,2368,2369,2370,2371,2372,2373,2374,2375,2376,2377,2378,2379,2380,2381,2382,2383,2384,2385,2386,2387,2388,2389,2390,2391,2392,2393,2394,2395,2396,2397,2398,2399,2400,2401,2402,2403,2404,2405,2406,2407,2408,2409,2410,2411] 
* CE 8 is refined into CE [2412,2413,2414,2415,2416,2417,2418,2419,2420,2421,2422,2423,2424,2425,2426,2427,2428,2429,2430,2431,2432,2433,2434,2435,2436,2437,2438,2439,2440,2441,2442,2443,2444,2445,2446,2447,2448,2449,2450,2451,2452,2453,2454,2455,2456,2457,2458,2459,2460,2461,2462,2463,2464,2465,2466,2467,2468,2469,2470,2471,2472,2473,2474,2475,2476,2477,2478,2479,2480,2481,2482,2483,2484,2485,2486,2487,2488,2489,2490,2491,2492,2493,2494,2495,2496,2497,2498,2499,2500,2501,2502,2503,2504,2505,2506,2507,2508,2509,2510,2511,2512,2513,2514,2515,2516,2517,2518,2519,2520,2521,2522,2523,2524,2525,2526,2527,2528,2529,2530,2531,2532,2533,2534,2535,2536,2537,2538,2539,2540,2541,2542,2543,2544,2545,2546,2547,2548,2549] 
* CE 16 is refined into CE [2550,2551,2552,2553,2554,2555,2556,2557,2558,2559,2560,2561,2562,2563,2564,2565,2566,2567,2568,2569,2570,2571,2572,2573,2574,2575,2576,2577,2578,2579,2580,2581,2582,2583,2584,2585,2586,2587,2588,2589,2590,2591,2592,2593,2594,2595,2596,2597,2598,2599,2600,2601,2602,2603,2604,2605,2606,2607,2608,2609,2610,2611,2612,2613,2614,2615,2616,2617,2618,2619,2620,2621] 
* CE 18 is refined into CE [2622,2623,2624,2625,2626,2627,2628,2629] 
* CE 19 is refined into CE [2630,2631,2632,2633,2634,2635,2636,2637] 
* CE 20 is refined into CE [2638,2639,2640,2641,2642,2643,2644,2645] 
* CE 21 is refined into CE [2646,2647,2648,2649,2650,2651,2652,2653,2654,2655] 
* CE 22 is refined into CE [2656,2657,2658] 
* CE 23 is refined into CE [2659,2660,2661,2662] 
* CE 24 is refined into CE [2663,2664,2665,2666,2667,2668,2669,2670,2671,2672,2673,2674,2675,2676,2677] 
* CE 25 is refined into CE [2678,2679] 
* CE 26 is refined into CE [2680,2681,2682,2683,2684] 
* CE 27 is refined into CE [2685,2686,2687,2688,2689] 


### Cost equations --> "Loop" of start/6 
* CEs [2659,2681] --> Loop 111 
* CEs [1979] --> Loop 112 
* CEs [1980] --> Loop 113 
* CEs [1981] --> Loop 114 
* CEs [2065,2066,2067,2068,2069,2070,2071,2072,2073,2074,2075,2076,2077,2078,2079,2080,2113,2114,2115,2116,2117,2118,2119,2120,2128,2129] --> Loop 115 
* CEs [1989,1990,2001,2002,2013,2014,2023,2024,2033,2034,2043,2044] --> Loop 116 
* CEs [1982,1983,1984,1985,1986,1987,1988,1991,1992,1993,1994,1995,1996,1997,1998,1999,2000,2003,2004,2005,2006,2007,2008,2009,2010,2011,2012,2015,2016,2017,2018,2019,2020,2021,2022,2025,2026,2027,2028,2029,2030,2031,2032,2035,2036,2037,2038,2039,2040,2041,2042,2045,2046,2047,2048,2049,2050,2051,2052,2053,2054,2055,2056,2057,2058,2059,2060,2061,2062,2063,2064,2081,2082,2083,2084,2085,2086,2087,2088,2089,2090,2091,2092,2093,2094,2095,2096,2097,2098,2099,2100,2101,2102,2103,2104,2105,2106,2107,2108,2109,2110,2111,2112,2121,2122,2123,2124,2125,2126,2127,2130] --> Loop 117 
* CEs [2575,2576,2578,2579,2590,2591,2608,2609,2610,2611,2620,2621,2646,2648,2649,2653,2654] --> Loop 118 
* CEs [2592,2593,2594,2595,2598,2599,2600,2601,2602,2603,2604,2605,2651] --> Loop 119 
* CEs [2550,2553,2556,2559,2562,2565,2568,2571,2574,2577,2580,2583,2586,2589] --> Loop 120 
* CEs [2494,2495,2496,2497,2498,2499,2500,2501,2502,2503,2504,2505,2506,2507,2508,2509,2542,2543,2544,2545,2546,2547,2548,2549,2643,2644] --> Loop 121 
* CEs [2412,2415,2424,2427,2436,2439] --> Loop 122 
* CEs [2131,2672,2688] --> Loop 123 
* CEs [2356,2357,2358,2359,2360,2361,2362,2363,2364,2365,2366,2367,2368,2369,2370,2371,2404,2405,2406,2407,2408,2409,2410,2411,2635,2636] --> Loop 124 
* CEs [2280,2281,2292,2293,2304,2305,2314,2315,2324,2325,2334,2335] --> Loop 125 
* CEs [2274,2277,2286,2289,2298,2301] --> Loop 126 
* CEs [2132] --> Loop 127 
* CEs [2218,2219,2220,2221,2222,2223,2224,2225,2226,2227,2228,2229,2230,2231,2232,2233,2266,2267,2268,2269,2270,2271,2272,2273,2627,2628,2671,2677,2687] --> Loop 128 
* CEs [2142,2143,2154,2155,2166,2167,2176,2177,2186,2187,2196,2197,2418,2419,2430,2431,2442,2443,2452,2453,2462,2463,2472,2473] --> Loop 129 
* CEs [2133,2134,2136,2137,2138,2139,2140,2141,2144,2145,2146,2147,2148,2149,2150,2151,2152,2153,2156,2157,2158,2159,2160,2161,2162,2163,2164,2165,2168,2169,2170,2171,2172,2173,2174,2175,2178,2179,2180,2181,2182,2183,2184,2185,2188,2189,2190,2191,2192,2193,2194,2195,2198,2199,2200,2201,2202,2203,2204,2205,2206,2207,2208,2209,2210,2211,2212,2213,2214,2215,2216,2217,2234,2235,2236,2237,2238,2239,2240,2241,2242,2243,2244,2245,2246,2247,2248,2249,2250,2251,2252,2253,2254,2255,2256,2257,2258,2259,2260,2261,2262,2263,2264,2265,2275,2276,2278,2279,2282,2283,2284,2285,2287,2288,2290,2291,2294,2295,2296,2297,2299,2300,2302,2303,2306,2307,2308,2309,2310,2311,2312,2313,2316,2317,2318,2319,2320,2321,2322,2323,2326,2327,2328,2329,2330,2331,2332,2333,2336,2337,2338,2339,2340,2341,2342,2343,2344,2345,2346,2347,2348,2349,2350,2351,2352,2353,2354,2355,2372,2373,2374,2375,2376,2377,2378,2379,2380,2381,2382,2383,2384,2385,2386,2387,2388,2389,2390,2391,2392,2393,2394,2395,2396,2397,2398,2399,2400,2401,2402,2403,2413,2414,2416,2417,2420,2421,2422,2423,2425,2426,2428,2429,2432,2433,2434,2435,2437,2438,2440,2441,2444,2445,2446,2447,2448,2449,2450,2451,2454,2455,2456,2457,2458,2459,2460,2461,2464,2465,2466,2467,2468,2469,2470,2471,2474,2475,2476,2477,2478,2479,2480,2481,2482,2483,2484,2485,2486,2487,2488,2489,2490,2491,2492,2493,2510,2511,2512,2513,2514,2515,2516,2517,2518,2519,2520,2521,2522,2523,2524,2525,2526,2527,2528,2529,2530,2531,2532,2533,2534,2535,2536,2537,2538,2539,2540,2541,2551,2552,2554,2555,2557,2558,2560,2561,2563,2564,2566,2567,2569,2570,2572,2573,2581,2582,2584,2585,2587,2588,2596,2597,2606,2607,2612,2613,2614,2615,2616,2617,2618,2619,2622,2623,2624,2625,2626,2629,2630,2631,2632,2633,2634,2637,2638,2639,2640,2641,2642,2645,2647,2650,2652,2655] --> Loop 130 
* CEs [2135,2656,2657,2658,2660,2661,2662,2663,2664,2665,2666,2667,2668,2669,2670,2673,2674,2675,2676,2678,2679,2680,2682,2683,2684,2685,2686,2689] --> Loop 131 

### Ranking functions of CR start(V,V2,V19,V18,V15,V16) 

#### Partial ranking functions of CR start(V,V2,V19,V18,V15,V16) 


Computing Bounds
=====================================

#### Cost of chains of p(V,Out):
* Chain [28]: 0
  with precondition: [Out=0,V>=0] 

* Chain [27]: 0
  with precondition: [V=Out+1,V>=1] 


#### Cost of chains of le(V,V2,Out):
* Chain [[29],32]: 0
  with precondition: [Out=2,V>=1,V2>=V] 

* Chain [[29],31]: 0
  with precondition: [Out=1,V2>=1,V>=V2+1] 

* Chain [[29],30]: 0
  with precondition: [Out=0,V>=1,V2>=1] 

* Chain [32]: 0
  with precondition: [V=0,Out=2,V2>=0] 

* Chain [31]: 0
  with precondition: [V2=0,Out=1,V>=1] 

* Chain [30]: 0
  with precondition: [Out=0,V>=0,V2>=0] 


#### Cost of chains of average(V,V2,Out):
* Chain [[33,34,35,36,37,38,39,40],46]: 0
  with precondition: [Out=0,V>=0,V2>=0,V2+3*V>=3] 

* Chain [[33,34,35,36,37,38,39,40],45]: 0
  with precondition: [Out=0,V>=0,V2>=0,V2+3*V>=3] 

* Chain [[33,34,35,36,37,38,39,40],44]: 0
  with precondition: [Out=0,V>=0,V2>=0,V+V2>=2,V2+2*V>=3] 

* Chain [[33,34,35,36,37,38,39,40],43]: 0
  with precondition: [Out=1,V>=0,V2>=0,V+V2>=2,V2+2*V>=3] 

* Chain [[33,34,35,36,37,38,39,40],42]: 0
  with precondition: [Out=0,V>=0,V2>=0,V+V2>=3] 

* Chain [[33,34,35,36,37,38,39,40],41]: 0
  with precondition: [Out=0,V>=0,V2>=0,V2+3*V>=3] 

* Chain [46]: 0
  with precondition: [Out=0,V>=0,V2>=0] 

* Chain [45]: 0
  with precondition: [Out=0,2>=V2,V>=0,V2>=1] 

* Chain [44]: 0
  with precondition: [V2=2,Out=0,V>=0] 

* Chain [43]: 0
  with precondition: [V=0,V2=2,Out=1] 

* Chain [42]: 0
  with precondition: [V2=0,Out=0,V>=0] 

* Chain [41]: 0
  with precondition: [V2=1,Out=0,V>=0] 


#### Cost of chains of fun(V,Out):
* Chain [49]: 1
  with precondition: [V=0,Out=2] 

* Chain [48]: 0
  with precondition: [Out=0,V>=0] 

* Chain [47]: 1
  with precondition: [Out=1,V>=1] 


#### Cost of chains of fun1(V,V2,Out):
* Chain [[50],52]: 1*it(50)+1
  Such that:it(50) =< Out

  with precondition: [Out>=1,V>=Out,V2>=Out] 

* Chain [[50],51]: 1*it(50)+1
  Such that:it(50) =< Out

  with precondition: [V2+1=Out,V2>=1,V>=V2+1] 

* Chain [52]: 1
  with precondition: [Out=0,V>=0,V2>=0] 

* Chain [51]: 1
  with precondition: [V2=0,Out=1,V>=1] 


#### Cost of chains of fun2(V,V2,Out):
* Chain [[75,76,77,78,79,80,81,82,83,84,85,86,87,88,89,90,91,92,93,94,95,96,97,98,99,100,101,102,103,104,105,106,107,108,109,110],74]: 673*it(75)+8*s(330)+2*s(331)+40*s(332)+6*s(337)+1*s(354)+2
  Such that:aux(127) =< V+V2
aux(245) =< 3*V+2*V2
aux(246) =< 9*V+8*V2
aux(125) =< aux(245)
it(75) =< aux(245)
aux(125) =< aux(246)
it(75) =< aux(246)
aux(132) =< aux(127)
s(354) =< aux(125)*3
s(339) =< it(75)*aux(132)
s(334) =< aux(125)*2
s(333) =< it(75)*aux(127)
s(332) =< aux(125)
s(330) =< s(334)
s(337) =< s(339)
s(331) =< s(333)

  with precondition: [V>=0,V2>=0,Out>=3,V2+3*V>=3,Out+3*V>=6] 

* Chain [[75,76,77,78,79,80,81,82,83,84,85,86,87,88,89,90,91,92,93,94,95,96,97,98,99,100,101,102,103,104,105,106,107,108,109,110],73]: 673*it(75)+8*s(330)+2*s(331)+40*s(332)+6*s(337)+1*s(354)+12
  Such that:aux(127) =< V+V2
aux(248) =< 3*V+2*V2
aux(249) =< 9*V+8*V2
aux(125) =< aux(248)
it(75) =< aux(248)
aux(125) =< aux(249)
it(75) =< aux(249)
aux(132) =< aux(127)
s(354) =< aux(125)*3
s(339) =< it(75)*aux(132)
s(334) =< aux(125)*2
s(333) =< it(75)*aux(127)
s(332) =< aux(125)
s(330) =< s(334)
s(337) =< s(339)
s(331) =< s(333)

  with precondition: [V>=0,V2>=0,Out>=4,V2+3*V>=3,Out+5*V>=9] 

* Chain [[75,76,77,78,79,80,81,82,83,84,85,86,87,88,89,90,91,92,93,94,95,96,97,98,99,100,101,102,103,104,105,106,107,108,109,110],72]: 673*it(75)+8*s(330)+2*s(331)+40*s(332)+6*s(337)+1*s(354)+2
  Such that:aux(127) =< V+V2
aux(250) =< 3*V+2*V2
aux(251) =< 9*V+8*V2
aux(125) =< aux(250)
it(75) =< aux(250)
aux(125) =< aux(251)
it(75) =< aux(251)
aux(132) =< aux(127)
s(354) =< aux(125)*3
s(339) =< it(75)*aux(132)
s(334) =< aux(125)*2
s(333) =< it(75)*aux(127)
s(332) =< aux(125)
s(330) =< s(334)
s(337) =< s(339)
s(331) =< s(333)

  with precondition: [V>=0,V2>=0,Out>=3,V2+3*V>=3,Out+3*V>=6] 

* Chain [[75,76,77,78,79,80,81,82,83,84,85,86,87,88,89,90,91,92,93,94,95,96,97,98,99,100,101,102,103,104,105,106,107,108,109,110],71]: 673*it(75)+8*s(330)+2*s(331)+40*s(332)+6*s(337)+1*s(354)+12*s(363)+2*s(364)+10*s(365)+3
  Such that:aux(252) =< 1
aux(253) =< 2
aux(127) =< V+V2
aux(255) =< 3*V+2*V2
aux(256) =< 9*V+8*V2
s(365) =< aux(252)
s(363) =< aux(253)
s(364) =< aux(255)
aux(125) =< aux(255)
it(75) =< aux(255)
aux(125) =< aux(256)
it(75) =< aux(256)
aux(132) =< aux(127)
s(354) =< aux(125)*3
s(339) =< it(75)*aux(132)
s(334) =< aux(125)*2
s(333) =< it(75)*aux(127)
s(332) =< aux(125)
s(330) =< s(334)
s(337) =< s(339)
s(331) =< s(333)

  with precondition: [V>=0,V2>=0,Out>=4,V2+3*V>=3,Out+3*V>=7] 

* Chain [[75,76,77,78,79,80,81,82,83,84,85,86,87,88,89,90,91,92,93,94,95,96,97,98,99,100,101,102,103,104,105,106,107,108,109,110],70]: 673*it(75)+8*s(330)+2*s(331)+40*s(332)+6*s(337)+1*s(354)+43
  Such that:aux(127) =< V+V2
aux(259) =< 3*V+2*V2
aux(260) =< 9*V+8*V2
aux(125) =< aux(259)
it(75) =< aux(259)
aux(125) =< aux(260)
it(75) =< aux(260)
aux(132) =< aux(127)
s(354) =< aux(125)*3
s(339) =< it(75)*aux(132)
s(334) =< aux(125)*2
s(333) =< it(75)*aux(127)
s(332) =< aux(125)
s(330) =< s(334)
s(337) =< s(339)
s(331) =< s(333)

  with precondition: [V>=0,V2>=0,Out>=5,V2+3*V>=3,Out+5*V>=10] 

* Chain [[75,76,77,78,79,80,81,82,83,84,85,86,87,88,89,90,91,92,93,94,95,96,97,98,99,100,101,102,103,104,105,106,107,108,109,110],69]: 673*it(75)+8*s(330)+2*s(331)+40*s(332)+6*s(337)+1*s(354)+60
  Such that:aux(127) =< V+V2
aux(264) =< 3*V+2*V2
aux(265) =< 9*V+8*V2
aux(125) =< aux(264)
it(75) =< aux(264)
aux(125) =< aux(265)
it(75) =< aux(265)
aux(132) =< aux(127)
s(354) =< aux(125)*3
s(339) =< it(75)*aux(132)
s(334) =< aux(125)*2
s(333) =< it(75)*aux(127)
s(332) =< aux(125)
s(330) =< s(334)
s(337) =< s(339)
s(331) =< s(333)

  with precondition: [V>=0,V2>=0,Out>=6,V2+3*V>=3,Out+5*V>=11] 

* Chain [[75,76,77,78,79,80,81,82,83,84,85,86,87,88,89,90,91,92,93,94,95,96,97,98,99,100,101,102,103,104,105,106,107,108,109,110],68]: 673*it(75)+8*s(330)+2*s(331)+40*s(332)+6*s(337)+1*s(354)+2
  Such that:aux(127) =< V+V2
aux(266) =< 3*V+2*V2
aux(267) =< 9*V+8*V2
aux(125) =< aux(266)
it(75) =< aux(266)
aux(125) =< aux(267)
it(75) =< aux(267)
aux(132) =< aux(127)
s(354) =< aux(125)*3
s(339) =< it(75)*aux(132)
s(334) =< aux(125)*2
s(333) =< it(75)*aux(127)
s(332) =< aux(125)
s(330) =< s(334)
s(337) =< s(339)
s(331) =< s(333)

  with precondition: [V>=0,V2>=0,2*Out+8>=5*V2,Out>=V2+2,V+V2>=2,V2+2*V>=3,Out+2*V2>=5,Out+2*V2+9*V>=14] 

* Chain [[75,76,77,78,79,80,81,82,83,84,85,86,87,88,89,90,91,92,93,94,95,96,97,98,99,100,101,102,103,104,105,106,107,108,109,110],67]: 673*it(75)+8*s(330)+2*s(331)+40*s(332)+6*s(337)+1*s(354)+33
  Such that:aux(127) =< V+V2
aux(270) =< 3*V+2*V2
aux(271) =< 9*V+8*V2
aux(125) =< aux(270)
it(75) =< aux(270)
aux(125) =< aux(271)
it(75) =< aux(271)
aux(132) =< aux(127)
s(354) =< aux(125)*3
s(339) =< it(75)*aux(132)
s(334) =< aux(125)*2
s(333) =< it(75)*aux(127)
s(332) =< aux(125)
s(330) =< s(334)
s(337) =< s(339)
s(331) =< s(333)

  with precondition: [V>=0,V2>=0,Out>=4,V+V2>=2,V2+2*V>=3,Out+2*V2>=6,Out+3*V>=7,Out+2*V2+9*V>=15] 

* Chain [[75,76,77,78,79,80,81,82,83,84,85,86,87,88,89,90,91,92,93,94,95,96,97,98,99,100,101,102,103,104,105,106,107,108,109,110],66]: 673*it(75)+8*s(330)+2*s(331)+40*s(332)+6*s(337)+1*s(354)+2*s(461)+6*s(462)+2*s(465)+4
  Such that:aux(272) =< 1
aux(273) =< 2
aux(127) =< V+V2
aux(275) =< 3*V+2*V2
aux(276) =< 9*V+8*V2
s(465) =< aux(272)
s(462) =< aux(273)
s(461) =< aux(275)
aux(125) =< aux(275)
it(75) =< aux(275)
aux(125) =< aux(276)
it(75) =< aux(276)
aux(132) =< aux(127)
s(354) =< aux(125)*3
s(339) =< it(75)*aux(132)
s(334) =< aux(125)*2
s(333) =< it(75)*aux(127)
s(332) =< aux(125)
s(330) =< s(334)
s(337) =< s(339)
s(331) =< s(333)

  with precondition: [V>=0,V2>=0,Out>=5,V2+3*V>=3,Out+5*V>=10] 

* Chain [[75,76,77,78,79,80,81,82,83,84,85,86,87,88,89,90,91,92,93,94,95,96,97,98,99,100,101,102,103,104,105,106,107,108,109,110],65]: 673*it(75)+8*s(330)+2*s(331)+40*s(332)+6*s(337)+1*s(354)+1*s(471)+5*s(472)+1*s(473)+6
  Such that:s(473) =< 1
aux(277) =< 2
aux(127) =< V+V2
aux(278) =< 3*V+2*V2
aux(279) =< 9*V+8*V2
s(471) =< aux(278)
s(472) =< aux(277)
aux(125) =< aux(278)
it(75) =< aux(278)
aux(125) =< aux(279)
it(75) =< aux(279)
aux(132) =< aux(127)
s(354) =< aux(125)*3
s(339) =< it(75)*aux(132)
s(334) =< aux(125)*2
s(333) =< it(75)*aux(127)
s(332) =< aux(125)
s(330) =< s(334)
s(337) =< s(339)
s(331) =< s(333)

  with precondition: [V>=0,V2>=0,Out>=6,V2+3*V>=3,Out+5*V>=11] 

* Chain [[75,76,77,78,79,80,81,82,83,84,85,86,87,88,89,90,91,92,93,94,95,96,97,98,99,100,101,102,103,104,105,106,107,108,109,110],64]: 673*it(75)+8*s(330)+2*s(331)+40*s(332)+6*s(337)+1*s(354)+20
  Such that:aux(127) =< V+V2
aux(282) =< 3*V+2*V2
aux(283) =< 9*V+8*V2
aux(125) =< aux(282)
it(75) =< aux(282)
aux(125) =< aux(283)
it(75) =< aux(283)
aux(132) =< aux(127)
s(354) =< aux(125)*3
s(339) =< it(75)*aux(132)
s(334) =< aux(125)*2
s(333) =< it(75)*aux(127)
s(332) =< aux(125)
s(330) =< s(334)
s(337) =< s(339)
s(331) =< s(333)

  with precondition: [V>=0,V2>=0,Out>=7,V+V2>=2,V2+2*V>=3,Out+2*V2>=9,Out+5*V>=12] 

* Chain [[75,76,77,78,79,80,81,82,83,84,85,86,87,88,89,90,91,92,93,94,95,96,97,98,99,100,101,102,103,104,105,106,107,108,109,110],63]: 673*it(75)+8*s(330)+2*s(331)+40*s(332)+6*s(337)+1*s(354)+26
  Such that:aux(127) =< V+V2
aux(286) =< 3*V+2*V2
aux(287) =< 9*V+8*V2
aux(125) =< aux(286)
it(75) =< aux(286)
aux(125) =< aux(287)
it(75) =< aux(287)
aux(132) =< aux(127)
s(354) =< aux(125)*3
s(339) =< it(75)*aux(132)
s(334) =< aux(125)*2
s(333) =< it(75)*aux(127)
s(332) =< aux(125)
s(330) =< s(334)
s(337) =< s(339)
s(331) =< s(333)

  with precondition: [V>=0,V2>=0,Out>=8,V+V2>=2,V2+2*V>=3,Out+2*V2>=10,Out+5*V>=13] 

* Chain [[75,76,77,78,79,80,81,82,83,84,85,86,87,88,89,90,91,92,93,94,95,96,97,98,99,100,101,102,103,104,105,106,107,108,109,110],62]: 673*it(75)+8*s(330)+2*s(331)+40*s(332)+6*s(337)+1*s(354)+45
  Such that:aux(127) =< V+V2
aux(291) =< 3*V+2*V2
aux(292) =< 9*V+8*V2
aux(125) =< aux(291)
it(75) =< aux(291)
aux(125) =< aux(292)
it(75) =< aux(292)
aux(132) =< aux(127)
s(354) =< aux(125)*3
s(339) =< it(75)*aux(132)
s(334) =< aux(125)*2
s(333) =< it(75)*aux(127)
s(332) =< aux(125)
s(330) =< s(334)
s(337) =< s(339)
s(331) =< s(333)

  with precondition: [V>=0,V2>=0,Out>=6,V+V2>=2,V2+2*V>=3,Out+2*V2>=8,Out+5*V>=11] 

* Chain [[75,76,77,78,79,80,81,82,83,84,85,86,87,88,89,90,91,92,93,94,95,96,97,98,99,100,101,102,103,104,105,106,107,108,109,110],61]: 673*it(75)+8*s(330)+2*s(331)+40*s(332)+6*s(337)+1*s(354)+11
  Such that:aux(127) =< V+V2
aux(294) =< 3*V+2*V2
aux(295) =< 9*V+8*V2
aux(125) =< aux(294)
it(75) =< aux(294)
aux(125) =< aux(295)
it(75) =< aux(295)
aux(132) =< aux(127)
s(354) =< aux(125)*3
s(339) =< it(75)*aux(132)
s(334) =< aux(125)*2
s(333) =< it(75)*aux(127)
s(332) =< aux(125)
s(330) =< s(334)
s(337) =< s(339)
s(331) =< s(333)

  with precondition: [V>=0,V2>=0,Out>=9,V+V2>=3,V2+2*V>=4,Out+2*V2>=13,Out+5*V>=14] 

* Chain [[75,76,77,78,79,80,81,82,83,84,85,86,87,88,89,90,91,92,93,94,95,96,97,98,99,100,101,102,103,104,105,106,107,108,109,110],60]: 673*it(75)+8*s(330)+2*s(331)+40*s(332)+6*s(337)+1*s(354)+15
  Such that:aux(127) =< V+V2
aux(297) =< 3*V+2*V2
aux(298) =< 9*V+8*V2
aux(125) =< aux(297)
it(75) =< aux(297)
aux(125) =< aux(298)
it(75) =< aux(298)
aux(132) =< aux(127)
s(354) =< aux(125)*3
s(339) =< it(75)*aux(132)
s(334) =< aux(125)*2
s(333) =< it(75)*aux(127)
s(332) =< aux(125)
s(330) =< s(334)
s(337) =< s(339)
s(331) =< s(333)

  with precondition: [V>=0,V2>=0,Out>=5,V+V2>=2,V2+2*V>=3,Out+2*V2>=7,Out+5*V>=10] 

* Chain [[75,76,77,78,79,80,81,82,83,84,85,86,87,88,89,90,91,92,93,94,95,96,97,98,99,100,101,102,103,104,105,106,107,108,109,110],59]: 673*it(75)+8*s(330)+2*s(331)+40*s(332)+6*s(337)+1*s(354)+2
  Such that:aux(127) =< V+V2
aux(299) =< 3*V+2*V2
aux(300) =< 9*V+8*V2
aux(125) =< aux(299)
it(75) =< aux(299)
aux(125) =< aux(300)
it(75) =< aux(300)
aux(132) =< aux(127)
s(354) =< aux(125)*3
s(339) =< it(75)*aux(132)
s(334) =< aux(125)*2
s(333) =< it(75)*aux(127)
s(332) =< aux(125)
s(330) =< s(334)
s(337) =< s(339)
s(331) =< s(333)

  with precondition: [V>=0,V2>=0,Out>=6,V+V2>=3,Out+2*V2>=12] 

* Chain [[75,76,77,78,79,80,81,82,83,84,85,86,87,88,89,90,91,92,93,94,95,96,97,98,99,100,101,102,103,104,105,106,107,108,109,110],58]: 673*it(75)+8*s(330)+2*s(331)+40*s(332)+6*s(337)+1*s(354)+10
  Such that:aux(127) =< V+V2
aux(302) =< 3*V+2*V2
aux(303) =< 9*V+8*V2
aux(125) =< aux(302)
it(75) =< aux(302)
aux(125) =< aux(303)
it(75) =< aux(303)
aux(132) =< aux(127)
s(354) =< aux(125)*3
s(339) =< it(75)*aux(132)
s(334) =< aux(125)*2
s(333) =< it(75)*aux(127)
s(332) =< aux(125)
s(330) =< s(334)
s(337) =< s(339)
s(331) =< s(333)

  with precondition: [V>=0,V2>=0,Out>=4,2*V2+3*V>=6,2*Out+3*V>=14,53*V2+69*V>=3*Out+120,17*V2+23*V>=Out+38] 

* Chain [[75,76,77,78,79,80,81,82,83,84,85,86,87,88,89,90,91,92,93,94,95,96,97,98,99,100,101,102,103,104,105,106,107,108,109,110],57]: 673*it(75)+8*s(330)+2*s(331)+40*s(332)+6*s(337)+1*s(354)+2
  Such that:aux(127) =< V+V2
aux(304) =< 3*V+2*V2
aux(305) =< 9*V+8*V2
aux(125) =< aux(304)
it(75) =< aux(304)
aux(125) =< aux(305)
it(75) =< aux(305)
aux(132) =< aux(127)
s(354) =< aux(125)*3
s(339) =< it(75)*aux(132)
s(334) =< aux(125)*2
s(333) =< it(75)*aux(127)
s(332) =< aux(125)
s(330) =< s(334)
s(337) =< s(339)
s(331) =< s(333)

  with precondition: [V>=0,V2>=0,Out>=3,V2+3*V>=3,Out+3*V>=6] 

* Chain [[75,76,77,78,79,80,81,82,83,84,85,86,87,88,89,90,91,92,93,94,95,96,97,98,99,100,101,102,103,104,105,106,107,108,109,110],56]: 673*it(75)+8*s(330)+2*s(331)+40*s(332)+6*s(337)+1*s(354)+30
  Such that:aux(127) =< V+V2
aux(307) =< 3*V+2*V2
aux(308) =< 9*V+8*V2
aux(125) =< aux(307)
it(75) =< aux(307)
aux(125) =< aux(308)
it(75) =< aux(308)
aux(132) =< aux(127)
s(354) =< aux(125)*3
s(339) =< it(75)*aux(132)
s(334) =< aux(125)*2
s(333) =< it(75)*aux(127)
s(332) =< aux(125)
s(330) =< s(334)
s(337) =< s(339)
s(331) =< s(333)

  with precondition: [V>=0,V2>=0,Out>=4,V2+3*V>=3,Out+3*V>=7] 

* Chain [[75,76,77,78,79,80,81,82,83,84,85,86,87,88,89,90,91,92,93,94,95,96,97,98,99,100,101,102,103,104,105,106,107,108,109,110],55]: 673*it(75)+8*s(330)+2*s(331)+40*s(332)+6*s(337)+1*s(354)+4*s(555)+4*s(556)+4*s(563)+2
  Such that:aux(309) =< 1
aux(310) =< 2
aux(127) =< V+V2
aux(312) =< 3*V+2*V2
aux(313) =< 9*V+8*V2
s(563) =< aux(309)
s(556) =< aux(310)
s(555) =< aux(313)
aux(125) =< aux(312)
it(75) =< aux(312)
aux(125) =< aux(313)
it(75) =< aux(313)
aux(132) =< aux(127)
s(354) =< aux(125)*3
s(339) =< it(75)*aux(132)
s(334) =< aux(125)*2
s(333) =< it(75)*aux(127)
s(332) =< aux(125)
s(330) =< s(334)
s(337) =< s(339)
s(331) =< s(333)

  with precondition: [V>=0,V2>=0,Out>=4,V2+3*V>=3,Out+3*V>=7] 

* Chain [[75,76,77,78,79,80,81,82,83,84,85,86,87,88,89,90,91,92,93,94,95,96,97,98,99,100,101,102,103,104,105,106,107,108,109,110],54]: 673*it(75)+8*s(330)+2*s(331)+40*s(332)+6*s(337)+1*s(354)+50
  Such that:aux(127) =< V+V2
aux(315) =< 3*V+2*V2
aux(316) =< 9*V+8*V2
aux(125) =< aux(315)
it(75) =< aux(315)
aux(125) =< aux(316)
it(75) =< aux(316)
aux(132) =< aux(127)
s(354) =< aux(125)*3
s(339) =< it(75)*aux(132)
s(334) =< aux(125)*2
s(333) =< it(75)*aux(127)
s(332) =< aux(125)
s(330) =< s(334)
s(337) =< s(339)
s(331) =< s(333)

  with precondition: [V>=0,V2>=0,Out>=5,V+V2>=2,V2+2*V>=3,Out+2*V2>=7,Out+3*V>=8,Out+2*V2+9*V>=16] 

* Chain [[75,76,77,78,79,80,81,82,83,84,85,86,87,88,89,90,91,92,93,94,95,96,97,98,99,100,101,102,103,104,105,106,107,108,109,110],53]: 673*it(75)+8*s(330)+2*s(331)+40*s(332)+6*s(337)+1*s(354)+50
  Such that:aux(127) =< V+V2
aux(318) =< 3*V+2*V2
aux(319) =< 9*V+8*V2
aux(125) =< aux(318)
it(75) =< aux(318)
aux(125) =< aux(319)
it(75) =< aux(319)
aux(132) =< aux(127)
s(354) =< aux(125)*3
s(339) =< it(75)*aux(132)
s(334) =< aux(125)*2
s(333) =< it(75)*aux(127)
s(332) =< aux(125)
s(330) =< s(334)
s(337) =< s(339)
s(331) =< s(333)

  with precondition: [V>=0,V2>=0,Out>=6,V+V2>=3,V2+2*V>=4,Out+2*V2>=10,Out+3*V>=9,Out+2*V2+9*V>=19] 

* Chain [74]: 2
  with precondition: [Out=1,V>=0,V2>=0] 

* Chain [73]: 12
  with precondition: [V=0,Out=2,V2>=0] 

* Chain [72]: 2
  with precondition: [Out=1,2>=V2,V>=0,V2>=1] 

* Chain [71]: 12*s(363)+2*s(364)+10*s(365)+3
  Such that:aux(252) =< 1
aux(253) =< 2
aux(254) =< V2
s(365) =< aux(252)
s(363) =< aux(253)
s(364) =< aux(254)

  with precondition: [3>=Out,V>=0,Out>=2,V2+1>=Out] 

* Chain [70]: 43
  with precondition: [V=0,4>=Out,Out>=3,V2+2>=Out] 

* Chain [69]: 60
  with precondition: [V=0,5>=Out,Out>=4,V2+3>=Out] 

* Chain [68]: 2
  with precondition: [V2=2,Out=1,V>=0] 

* Chain [67]: 33
  with precondition: [3>=Out,V>=0,V2>=2,Out>=2] 

* Chain [66]: 2*s(461)+6*s(462)+2*s(465)+4
  Such that:aux(272) =< 1
aux(273) =< 2
aux(274) =< V2
s(465) =< aux(272)
s(462) =< aux(273)
s(461) =< aux(274)

  with precondition: [V=0,2>=V2,Out>=3,V2+2>=Out] 

* Chain [65]: 1*s(471)+5*s(472)+1*s(473)+6
  Such that:s(473) =< 1
s(471) =< V2
aux(277) =< 2
s(472) =< aux(277)

  with precondition: [V=0,2>=V2,Out>=4,V2+3>=Out] 

* Chain [64]: 20
  with precondition: [V=0,6>=Out,V2>=2,Out>=5] 

* Chain [63]: 26
  with precondition: [V=0,Out=6,V2>=2] 

* Chain [62]: 45
  with precondition: [V=0,5>=Out,V2>=2,Out>=4] 

* Chain [61]: 11
  with precondition: [V=0,Out=7,V2>=3] 

* Chain [60]: 15
  with precondition: [V=0,4>=Out,V2>=2,Out>=3] 

* Chain [59]: 2
  with precondition: [V2=0,Out=1,V>=0] 

* Chain [58]: 10
  with precondition: [Out=2,V>=1,V2>=0] 

* Chain [57]: 2
  with precondition: [V2=1,Out=1,V>=0] 

* Chain [56]: 30
  with precondition: [Out=2,V>=0,V2>=1] 

* Chain [55]: 4*s(555)+4*s(556)+4*s(563)+2
  Such that:aux(309) =< 1
aux(310) =< 2
aux(311) =< V2
s(563) =< aux(309)
s(556) =< aux(310)
s(555) =< aux(311)

  with precondition: [2>=V2,V>=0,Out>=2,V2+1>=Out] 

* Chain [54]: 50
  with precondition: [Out=3,V>=0,V2>=2] 

* Chain [53]: 50
  with precondition: [Out=4,V>=0,V2>=3] 


#### Cost of chains of start(V,V2,V19,V18,V15,V16):
* Chain [131]: 1*s(950)+6*s(951)+30*s(957)+50*s(958)+4*s(959)+14806*s(961)+22*s(963)+880*s(967)+176*s(968)+132*s(969)+44*s(970)+5*s(971)+60
  Such that:s(954) =< V+V2
s(955) =< 3*V+2*V2
s(956) =< 9*V+8*V2
s(950) =< V2+1
aux(325) =< 1
aux(326) =< 2
aux(327) =< V2
s(957) =< aux(325)
s(951) =< aux(327)
s(958) =< aux(326)
s(959) =< s(956)
s(960) =< s(955)
s(961) =< s(955)
s(960) =< s(956)
s(961) =< s(956)
s(962) =< s(954)
s(963) =< s(960)*3
s(964) =< s(961)*s(962)
s(965) =< s(960)*2
s(966) =< s(961)*s(954)
s(967) =< s(960)
s(968) =< s(965)
s(969) =< s(964)
s(970) =< s(966)
s(971) =< s(955)

  with precondition: [V>=0] 

* Chain [130]: 1612*s(993)+2464*s(994)+72*s(995)+266508*s(997)+396*s(999)+15840*s(1003)+3168*s(1004)+2376*s(1005)+792*s(1006)+90*s(1007)+32*s(1355)+118448*s(1357)+176*s(1359)+7040*s(1363)+1408*s(1364)+1056*s(1365)+352*s(1366)+40*s(1367)+16*s(1513)+64*s(1563)+236896*s(1565)+352*s(1567)+14080*s(1571)+2816*s(1572)+2112*s(1573)+704*s(1574)+80*s(1575)+32*s(1883)+118448*s(1885)+176*s(1887)+7040*s(1891)+1408*s(1892)+1056*s(1893)+352*s(1894)+40*s(1895)+16*s(2041)+64*s(2091)+236896*s(2093)+352*s(2095)+14080*s(2099)+2816*s(2100)+2112*s(2101)+704*s(2102)+80*s(2103)+32*s(2411)+118448*s(2413)+176*s(2415)+7040*s(2419)+1408*s(2420)+1056*s(2421)+352*s(2422)+40*s(2423)+16*s(2569)+8*s(2619)+29612*s(2621)+44*s(2623)+1760*s(2627)+352*s(2628)+264*s(2629)+88*s(2630)+10*s(2631)+14*s(2657)+8*s(2691)+29612*s(2693)+44*s(2695)+1760*s(2699)+352*s(2700)+264*s(2701)+88*s(2702)+10*s(2703)+65
  Such that:aux(328) =< 1
aux(329) =< 2
aux(330) =< V2+1
aux(331) =< V2+V19
aux(332) =< 3*V2+3
aux(333) =< 3*V2+2*V19
aux(334) =< 9*V2+9
aux(335) =< 9*V2+8*V19
aux(336) =< V19
aux(337) =< V19+1
aux(338) =< V19+V18
aux(339) =< 3*V19+3
aux(340) =< 3*V19+2*V18
aux(341) =< 9*V19+9
aux(342) =< 9*V19+8*V18
aux(343) =< V18
aux(344) =< V18+1
aux(345) =< V18+V15
aux(346) =< 3*V18+3
aux(347) =< 3*V18+2*V15
aux(348) =< 9*V18+9
aux(349) =< 9*V18+8*V15
aux(350) =< V15
aux(351) =< V15+V16
aux(352) =< 3*V15+2*V16
aux(353) =< 9*V15+8*V16
aux(354) =< V16+1
aux(355) =< 2*V16+2
aux(356) =< 8*V16+8
s(993) =< aux(328)
s(2657) =< aux(354)
s(994) =< aux(329)
s(995) =< aux(348)
s(996) =< aux(346)
s(997) =< aux(346)
s(996) =< aux(348)
s(997) =< aux(348)
s(998) =< aux(344)
s(999) =< s(996)*3
s(1000) =< s(997)*s(998)
s(1001) =< s(996)*2
s(1002) =< s(997)*aux(344)
s(1003) =< s(996)
s(1004) =< s(1001)
s(1005) =< s(1000)
s(1006) =< s(1002)
s(1007) =< aux(346)
s(1355) =< aux(349)
s(1356) =< aux(347)
s(1357) =< aux(347)
s(1356) =< aux(349)
s(1357) =< aux(349)
s(1358) =< aux(345)
s(1359) =< s(1356)*3
s(1360) =< s(1357)*s(1358)
s(1361) =< s(1356)*2
s(1362) =< s(1357)*aux(345)
s(1363) =< s(1356)
s(1364) =< s(1361)
s(1365) =< s(1360)
s(1366) =< s(1362)
s(1367) =< aux(347)
s(1513) =< aux(350)
s(1563) =< aux(341)
s(1564) =< aux(339)
s(1565) =< aux(339)
s(1564) =< aux(341)
s(1565) =< aux(341)
s(1566) =< aux(337)
s(1567) =< s(1564)*3
s(1568) =< s(1565)*s(1566)
s(1569) =< s(1564)*2
s(1570) =< s(1565)*aux(337)
s(1571) =< s(1564)
s(1572) =< s(1569)
s(1573) =< s(1568)
s(1574) =< s(1570)
s(1575) =< aux(339)
s(1883) =< aux(342)
s(1884) =< aux(340)
s(1885) =< aux(340)
s(1884) =< aux(342)
s(1885) =< aux(342)
s(1886) =< aux(338)
s(1887) =< s(1884)*3
s(1888) =< s(1885)*s(1886)
s(1889) =< s(1884)*2
s(1890) =< s(1885)*aux(338)
s(1891) =< s(1884)
s(1892) =< s(1889)
s(1893) =< s(1888)
s(1894) =< s(1890)
s(1895) =< aux(340)
s(2041) =< aux(343)
s(2091) =< aux(334)
s(2092) =< aux(332)
s(2093) =< aux(332)
s(2092) =< aux(334)
s(2093) =< aux(334)
s(2094) =< aux(330)
s(2095) =< s(2092)*3
s(2096) =< s(2093)*s(2094)
s(2097) =< s(2092)*2
s(2098) =< s(2093)*aux(330)
s(2099) =< s(2092)
s(2100) =< s(2097)
s(2101) =< s(2096)
s(2102) =< s(2098)
s(2103) =< aux(332)
s(2411) =< aux(335)
s(2412) =< aux(333)
s(2413) =< aux(333)
s(2412) =< aux(335)
s(2413) =< aux(335)
s(2414) =< aux(331)
s(2415) =< s(2412)*3
s(2416) =< s(2413)*s(2414)
s(2417) =< s(2412)*2
s(2418) =< s(2413)*aux(331)
s(2419) =< s(2412)
s(2420) =< s(2417)
s(2421) =< s(2416)
s(2422) =< s(2418)
s(2423) =< aux(333)
s(2569) =< aux(336)
s(2619) =< aux(356)
s(2620) =< aux(355)
s(2621) =< aux(355)
s(2620) =< aux(356)
s(2621) =< aux(356)
s(2622) =< aux(354)
s(2623) =< s(2620)*3
s(2624) =< s(2621)*s(2622)
s(2625) =< s(2620)*2
s(2626) =< s(2621)*aux(354)
s(2627) =< s(2620)
s(2628) =< s(2625)
s(2629) =< s(2624)
s(2630) =< s(2626)
s(2631) =< aux(355)
s(2691) =< aux(353)
s(2692) =< aux(352)
s(2693) =< aux(352)
s(2692) =< aux(353)
s(2693) =< aux(353)
s(2694) =< aux(351)
s(2695) =< s(2692)*3
s(2696) =< s(2693)*s(2694)
s(2697) =< s(2692)*2
s(2698) =< s(2693)*aux(351)
s(2699) =< s(2692)
s(2700) =< s(2697)
s(2701) =< s(2696)
s(2702) =< s(2698)
s(2703) =< aux(352)

  with precondition: [V=1,V2>=0,V19>=0] 

* Chain [129]: 136*s(2741)+216*s(2742)+16*s(2743)+59224*s(2745)+88*s(2747)+3520*s(2751)+704*s(2752)+528*s(2753)+176*s(2754)+20*s(2755)+16*s(2823)+59224*s(2825)+88*s(2827)+3520*s(2831)+704*s(2832)+528*s(2833)+176*s(2834)+20*s(2835)+65
  Such that:aux(357) =< 1
aux(358) =< 2
aux(359) =< V2+1
aux(360) =< 3*V2+3
aux(361) =< 9*V2+9
aux(362) =< V18+1
aux(363) =< 3*V18+3
aux(364) =< 9*V18+9
s(2741) =< aux(357)
s(2742) =< aux(358)
s(2743) =< aux(364)
s(2744) =< aux(363)
s(2745) =< aux(363)
s(2744) =< aux(364)
s(2745) =< aux(364)
s(2746) =< aux(362)
s(2747) =< s(2744)*3
s(2748) =< s(2745)*s(2746)
s(2749) =< s(2744)*2
s(2750) =< s(2745)*aux(362)
s(2751) =< s(2744)
s(2752) =< s(2749)
s(2753) =< s(2748)
s(2754) =< s(2750)
s(2755) =< aux(363)
s(2823) =< aux(361)
s(2824) =< aux(360)
s(2825) =< aux(360)
s(2824) =< aux(361)
s(2825) =< aux(361)
s(2826) =< aux(359)
s(2827) =< s(2824)*3
s(2828) =< s(2825)*s(2826)
s(2829) =< s(2824)*2
s(2830) =< s(2825)*aux(359)
s(2831) =< s(2824)
s(2832) =< s(2829)
s(2833) =< s(2828)
s(2834) =< s(2830)
s(2835) =< aux(360)

  with precondition: [V=1,V19=1,V2>=0] 

* Chain [128]: 36*s(2899)+36*s(2900)+32*s(2901)+4*s(2949)+7
  Such that:s(2946) =< V2
aux(365) =< 1
aux(366) =< 2
aux(367) =< V15
s(2899) =< aux(365)
s(2900) =< aux(366)
s(2901) =< aux(367)
s(2949) =< s(2946)

  with precondition: [2>=V2,V>=0,V2>=1] 

* Chain [127]: 3
  with precondition: [V=1,V2=1,V19=2,V18>=0,V15>=0] 

* Chain [126]: 34*s(2955)+54*s(2956)+8*s(2957)+29612*s(2959)+44*s(2961)+1760*s(2965)+352*s(2966)+264*s(2967)+88*s(2968)+10*s(2969)+64
  Such that:aux(368) =< 1
aux(369) =< 2
aux(370) =< V19+1
aux(371) =< 3*V19+3
aux(372) =< 9*V19+9
s(2955) =< aux(368)
s(2956) =< aux(369)
s(2957) =< aux(372)
s(2958) =< aux(371)
s(2959) =< aux(371)
s(2958) =< aux(372)
s(2959) =< aux(372)
s(2960) =< aux(370)
s(2961) =< s(2958)*3
s(2962) =< s(2959)*s(2960)
s(2963) =< s(2958)*2
s(2964) =< s(2959)*aux(370)
s(2965) =< s(2958)
s(2966) =< s(2963)
s(2967) =< s(2962)
s(2968) =< s(2964)
s(2969) =< aux(371)

  with precondition: [V=1,V2=1,V18=0,V19>=0] 

* Chain [125]: 68*s(2995)+108*s(2996)+16*s(2997)+59224*s(2999)+88*s(3001)+3520*s(3005)+704*s(3006)+528*s(3007)+176*s(3008)+20*s(3009)+64
  Such that:aux(373) =< 1
aux(374) =< 2
aux(375) =< V19+1
aux(376) =< 3*V19+3
aux(377) =< 9*V19+9
s(2995) =< aux(373)
s(2996) =< aux(374)
s(2997) =< aux(377)
s(2998) =< aux(376)
s(2999) =< aux(376)
s(2998) =< aux(377)
s(2999) =< aux(377)
s(3000) =< aux(375)
s(3001) =< s(2998)*3
s(3002) =< s(2999)*s(3000)
s(3003) =< s(2998)*2
s(3004) =< s(2999)*aux(375)
s(3005) =< s(2998)
s(3006) =< s(3003)
s(3007) =< s(3002)
s(3008) =< s(3004)
s(3009) =< aux(376)

  with precondition: [V=1,V2=1,V18=1,V19>=0] 

* Chain [124]: 32*s(3073)+32*s(3074)+32*s(3075)+6
  Such that:aux(378) =< 1
aux(379) =< 2
aux(380) =< V18
s(3073) =< aux(378)
s(3074) =< aux(379)
s(3075) =< aux(380)

  with precondition: [V=1,V2=1,4>=V18,V19>=0,V18>=3] 

* Chain [123]: 2
  with precondition: [V2=2,V>=0] 

* Chain [122]: 34*s(3123)+54*s(3124)+8*s(3125)+29612*s(3127)+44*s(3129)+1760*s(3133)+352*s(3134)+264*s(3135)+88*s(3136)+10*s(3137)+63
  Such that:aux(381) =< 1
aux(382) =< 2
aux(383) =< V2+1
aux(384) =< 3*V2+3
aux(385) =< 9*V2+9
s(3123) =< aux(381)
s(3124) =< aux(382)
s(3125) =< aux(385)
s(3126) =< aux(384)
s(3127) =< aux(384)
s(3126) =< aux(385)
s(3127) =< aux(385)
s(3128) =< aux(383)
s(3129) =< s(3126)*3
s(3130) =< s(3127)*s(3128)
s(3131) =< s(3126)*2
s(3132) =< s(3127)*aux(383)
s(3133) =< s(3126)
s(3134) =< s(3131)
s(3135) =< s(3130)
s(3136) =< s(3132)
s(3137) =< aux(384)

  with precondition: [V=1,V19=0,V2>=0] 

* Chain [121]: 32*s(3161)+32*s(3162)+32*s(3163)+5
  Such that:aux(386) =< 1
aux(387) =< 2
aux(388) =< V19
s(3161) =< aux(386)
s(3162) =< aux(387)
s(3163) =< aux(388)

  with precondition: [V=1,4>=V19,V2>=0,V19>=3] 

* Chain [120]: 34*s(3211)+54*s(3212)+4*s(3213)+14806*s(3215)+22*s(3217)+880*s(3221)+176*s(3222)+132*s(3223)+44*s(3224)+5*s(3225)+9*s(3231)+62
  Such that:s(3209) =< 2*V16+2
s(3210) =< 8*V16+8
aux(389) =< 1
aux(390) =< 2
aux(391) =< V16+1
s(3211) =< aux(389)
s(3231) =< aux(391)
s(3212) =< aux(390)
s(3213) =< s(3210)
s(3214) =< s(3209)
s(3215) =< s(3209)
s(3214) =< s(3210)
s(3215) =< s(3210)
s(3216) =< aux(391)
s(3217) =< s(3214)*3
s(3218) =< s(3215)*s(3216)
s(3219) =< s(3214)*2
s(3220) =< s(3215)*aux(391)
s(3221) =< s(3214)
s(3222) =< s(3219)
s(3223) =< s(3218)
s(3224) =< s(3220)
s(3225) =< s(3209)

  with precondition: [V=1,V15=0,V2>=0,V19>=0,V18>=0,V16>=0] 

* Chain [119]: 6*s(3251)+22*s(3252)+6*s(3253)+62
  Such that:aux(392) =< 1
aux(393) =< 2
aux(394) =< V16+1
s(3251) =< aux(392)
s(3253) =< aux(394)
s(3252) =< aux(393)

  with precondition: [V=1,V15=1,V2>=0,V19>=0,V18>=0,V16>=0] 

* Chain [118]: 16*s(3271)+16*s(3272)+16*s(3273)+4
  Such that:aux(395) =< 1
aux(396) =< 2
aux(397) =< V16+1
s(3271) =< aux(395)
s(3272) =< aux(396)
s(3273) =< aux(397)

  with precondition: [V=1,1>=V16,V2>=0,V19>=0,V18>=0,V15>=0,V16>=0] 

* Chain [117]: 522*s(3297)+798*s(3298)+72*s(3299)+266508*s(3301)+396*s(3303)+15840*s(3307)+3168*s(3308)+2376*s(3309)+792*s(3310)+90*s(3311)+32*s(3659)+118448*s(3661)+176*s(3663)+7040*s(3667)+1408*s(3668)+1056*s(3669)+352*s(3670)+40*s(3671)+16*s(3817)+66
  Such that:aux(398) =< 1
aux(399) =< 2
aux(400) =< V15+1
aux(401) =< V15+V16
aux(402) =< 3*V15+3
aux(403) =< 3*V15+2*V16
aux(404) =< 9*V15+9
aux(405) =< 9*V15+8*V16
aux(406) =< V16
s(3297) =< aux(398)
s(3298) =< aux(399)
s(3299) =< aux(404)
s(3300) =< aux(402)
s(3301) =< aux(402)
s(3300) =< aux(404)
s(3301) =< aux(404)
s(3302) =< aux(400)
s(3303) =< s(3300)*3
s(3304) =< s(3301)*s(3302)
s(3305) =< s(3300)*2
s(3306) =< s(3301)*aux(400)
s(3307) =< s(3300)
s(3308) =< s(3305)
s(3309) =< s(3304)
s(3310) =< s(3306)
s(3311) =< aux(402)
s(3659) =< aux(405)
s(3660) =< aux(403)
s(3661) =< aux(403)
s(3660) =< aux(405)
s(3661) =< aux(405)
s(3662) =< aux(401)
s(3663) =< s(3660)*3
s(3664) =< s(3661)*s(3662)
s(3665) =< s(3660)*2
s(3666) =< s(3661)*aux(401)
s(3667) =< s(3660)
s(3668) =< s(3665)
s(3669) =< s(3664)
s(3670) =< s(3666)
s(3671) =< aux(403)
s(3817) =< aux(406)

  with precondition: [V=2,V2>=0,V19>=0] 

* Chain [116]: 68*s(3865)+108*s(3866)+16*s(3867)+59224*s(3869)+88*s(3871)+3520*s(3875)+704*s(3876)+528*s(3877)+176*s(3878)+20*s(3879)+66
  Such that:aux(407) =< 1
aux(408) =< 2
aux(409) =< V15+1
aux(410) =< 3*V15+3
aux(411) =< 9*V15+9
s(3865) =< aux(407)
s(3866) =< aux(408)
s(3867) =< aux(411)
s(3868) =< aux(410)
s(3869) =< aux(410)
s(3868) =< aux(411)
s(3869) =< aux(411)
s(3870) =< aux(409)
s(3871) =< s(3868)*3
s(3872) =< s(3869)*s(3870)
s(3873) =< s(3868)*2
s(3874) =< s(3869)*aux(409)
s(3875) =< s(3868)
s(3876) =< s(3873)
s(3877) =< s(3872)
s(3878) =< s(3874)
s(3879) =< aux(410)

  with precondition: [V=2,V2=1,V19=1,V18=1,V16=1,V15>=0] 

* Chain [115]: 32*s(3943)+32*s(3944)+32*s(3945)+8
  Such that:aux(412) =< 1
aux(413) =< 2
aux(414) =< V16
s(3943) =< aux(412)
s(3944) =< aux(413)
s(3945) =< aux(414)

  with precondition: [V=2,V2=1,V19=1,V18=1,4>=V16,V15>=0,V16>=3] 

* Chain [114]: 4
  with precondition: [V=2,V2=1,V19=1,V18=2,V15>=0,V16>=0] 

* Chain [113]: 3
  with precondition: [V=2,V2=1,V19=2,V18>=0,V15>=0,V16>=0] 

* Chain [112]: 2
  with precondition: [V=2,V2=2,V19>=0,V18>=0,V15>=0,V16>=0] 

* Chain [111]: 1
  with precondition: [V2=0,V>=1] 


Closed-form bounds of start(V,V2,V19,V18,V15,V16): 
-------------------------------------
* Chain [131] with precondition: [V>=0] 
    - Upper bound: nat(V2)*6+190+nat(V+V2)*176*nat(3*V+2*V2)+nat(V2+1)+nat(3*V+2*V2)*16109+nat(9*V+8*V2)*4 
    - Complexity: n^2 
* Chain [130] with precondition: [V=1,V2>=0,V19>=0] 
    - Upper bound: 16*V19+6605+nat(V18)*16+nat(V15)*16+(1408*V2+1408*V19)*(3*V2+2*V19)+(2816*V2+2816)*(3*V2+3)+nat(V19+V18)*1408*nat(3*V19+2*V18)+(2816*V19+2816)*(3*V19+3)+nat(V18+V15)*1408*nat(3*V18+2*V15)+nat(V18+1)*3168*nat(3*V18+3)+nat(V15+V16)*352*nat(3*V15+2*V16)+nat(V16+1)*14+nat(V16+1)*352*nat(2*V16+2)+nat(2*V16+2)*32218+(773232*V2+773232)+(386616*V2+257744*V19)+(773232*V19+773232)+nat(3*V19+2*V18)*128872+nat(3*V18+3)*289962+nat(3*V18+2*V15)*128872+nat(3*V15+2*V16)*32218+nat(8*V16+8)*8+(576*V2+576)+(288*V2+256*V19)+(576*V19+576)+nat(9*V19+8*V18)*32+nat(9*V18+9)*72+nat(9*V18+8*V15)*32+nat(9*V15+8*V16)*8 
    - Complexity: n^2 
* Chain [129] with precondition: [V=1,V19=1,V2>=0] 
    - Upper bound: (704*V2+704)*(3*V2+3)+633+nat(V18+1)*704*nat(3*V18+3)+(193308*V2+193308)+nat(3*V18+3)*64436+(144*V2+144)+nat(9*V18+9)*16 
    - Complexity: n^2 
* Chain [128] with precondition: [2>=V2,V>=0,V2>=1] 
    - Upper bound: 4*V2+115+nat(V15)*32 
    - Complexity: n 
* Chain [127] with precondition: [V=1,V2=1,V19=2,V18>=0,V15>=0] 
    - Upper bound: 3 
    - Complexity: constant 
* Chain [126] with precondition: [V=1,V2=1,V18=0,V19>=0] 
    - Upper bound: (352*V19+352)*(3*V19+3)+206+(96654*V19+96654)+(72*V19+72) 
    - Complexity: n^2 
* Chain [125] with precondition: [V=1,V2=1,V18=1,V19>=0] 
    - Upper bound: (704*V19+704)*(3*V19+3)+348+(193308*V19+193308)+(144*V19+144) 
    - Complexity: n^2 
* Chain [124] with precondition: [V=1,V2=1,4>=V18,V19>=0,V18>=3] 
    - Upper bound: 32*V18+102 
    - Complexity: n 
* Chain [123] with precondition: [V2=2,V>=0] 
    - Upper bound: 2 
    - Complexity: constant 
* Chain [122] with precondition: [V=1,V19=0,V2>=0] 
    - Upper bound: (352*V2+352)*(3*V2+3)+205+(96654*V2+96654)+(72*V2+72) 
    - Complexity: n^2 
* Chain [121] with precondition: [V=1,4>=V19,V2>=0,V19>=3] 
    - Upper bound: 32*V19+101 
    - Complexity: n 
* Chain [120] with precondition: [V=1,V15=0,V2>=0,V19>=0,V18>=0,V16>=0] 
    - Upper bound: 9*V16+213+(176*V16+176)*(2*V16+2)+(32218*V16+32218)+(32*V16+32) 
    - Complexity: n^2 
* Chain [119] with precondition: [V=1,V15=1,V2>=0,V19>=0,V18>=0,V16>=0] 
    - Upper bound: 6*V16+118 
    - Complexity: n 
* Chain [118] with precondition: [V=1,1>=V16,V2>=0,V19>=0,V18>=0,V15>=0,V16>=0] 
    - Upper bound: 16*V16+68 
    - Complexity: n 
* Chain [117] with precondition: [V=2,V2>=0,V19>=0] 
    - Upper bound: nat(V16)*16+2184+nat(V15+V16)*1408*nat(3*V15+2*V16)+nat(V15+1)*3168*nat(3*V15+3)+nat(3*V15+3)*289962+nat(3*V15+2*V16)*128872+nat(9*V15+9)*72+nat(9*V15+8*V16)*32 
    - Complexity: n^2 
* Chain [116] with precondition: [V=2,V2=1,V19=1,V18=1,V16=1,V15>=0] 
    - Upper bound: (704*V15+704)*(3*V15+3)+350+(193308*V15+193308)+(144*V15+144) 
    - Complexity: n^2 
* Chain [115] with precondition: [V=2,V2=1,V19=1,V18=1,4>=V16,V15>=0,V16>=3] 
    - Upper bound: 32*V16+104 
    - Complexity: n 
* Chain [114] with precondition: [V=2,V2=1,V19=1,V18=2,V15>=0,V16>=0] 
    - Upper bound: 4 
    - Complexity: constant 
* Chain [113] with precondition: [V=2,V2=1,V19=2,V18>=0,V15>=0,V16>=0] 
    - Upper bound: 3 
    - Complexity: constant 
* Chain [112] with precondition: [V=2,V2=2,V19>=0,V18>=0,V15>=0,V16>=0] 
    - Upper bound: 2 
    - Complexity: constant 
* Chain [111] with precondition: [V2=0,V>=1] 
    - Upper bound: 1 
    - Complexity: constant 

### Maximum cost of start(V,V2,V19,V18,V15,V16): max([max([max([max([max([max([3,nat(V19)*32+100,nat(V18)*32+101,nat(V15+1)*704*nat(3*V15+3)+349+nat(3*V15+3)*64436+nat(9*V15+9)*16]),nat(V19+1)*352*nat(3*V19+3)+205+nat(3*V19+3)*32218+nat(9*V19+9)*8+(nat(V19+1)*352*nat(3*V19+3)+142+nat(3*V19+3)*32218+nat(9*V19+9)*8)]),nat(V2+1)*352*nat(3*V2+3)+428+nat(V18+1)*704*nat(3*V18+3)+nat(3*V2+3)*32218+nat(3*V18+3)*64436+nat(9*V2+9)*8+nat(9*V18+9)*16+(nat(V2+1)*352*nat(3*V2+3)+204+nat(3*V2+3)*32218+nat(9*V2+9)*8)]),nat(V16)*16+103+max([nat(V16)*16,nat(V15+V16)*1408*nat(3*V15+2*V16)+2080+nat(V15+1)*3168*nat(3*V15+3)+nat(3*V15+3)*289962+nat(3*V15+2*V16)*128872+nat(9*V15+9)*72+nat(9*V15+8*V16)*32])]),nat(V2)*4+114+max([nat(V15)*32,nat(V2)*2+75+nat(V+V2)*176*nat(3*V+2*V2)+nat(V2+1)+nat(3*V+2*V2)*16109+nat(9*V+8*V2)*4])]),nat(V16+1)*6+51+max([60,nat(V16+1)*3+max([nat(V16+1)*5+max([nat(V16+1)*2,nat(V19)*16+6553+nat(V18)*16+nat(V15)*16+nat(V2+V19)*1408*nat(3*V2+2*V19)+nat(V2+1)*2816*nat(3*V2+3)+nat(V19+V18)*1408*nat(3*V19+2*V18)+nat(V19+1)*2816*nat(3*V19+3)+nat(V18+V15)*1408*nat(3*V18+2*V15)+nat(V18+1)*3168*nat(3*V18+3)+nat(V15+V16)*352*nat(3*V15+2*V16)+nat(V16+1)*352*nat(2*V16+2)+nat(2*V16+2)*32218+nat(3*V2+3)*257744+nat(3*V2+2*V19)*128872+nat(3*V19+3)*257744+nat(3*V19+2*V18)*128872+nat(3*V18+3)*289962+nat(3*V18+2*V15)*128872+nat(3*V15+2*V16)*32218+nat(8*V16+8)*8+nat(9*V2+9)*64+nat(9*V2+8*V19)*32+nat(9*V19+9)*64+nat(9*V19+8*V18)*32+nat(9*V18+9)*72+nat(9*V18+8*V15)*32+nat(9*V15+8*V16)*8]),nat(V16+1)*176*nat(2*V16+2)+152+nat(2*V16+2)*16109+nat(8*V16+8)*4])])])+1 
Asymptotic class: n^2 
* Total analysis performed in 36022 ms.


----------------------------------------

(12)
BOUNDS(1, n^2)

----------------------------------------

(13) RelTrsToDecreasingLoopProblemProof (LOWER BOUND(ID))
Transformed a relative TRS into a decreasing-loop problem.
----------------------------------------

(14)
Obligation:
Analyzing the following TRS for decreasing loops:

The Runtime Complexity (innermost) of the given CpxRelTRS could be proven to be BOUNDS(n^1, n^2).


The TRS R consists of the following rules:

   P(s(z0)) -> c
   P(0) -> c1
   LE(0, z0) -> c2
   LE(s(z0), 0) -> c3
   LE(s(z0), s(z1)) -> c4(LE(z0, z1))
   AVERAGE(z0, z1) -> c5(IF(le(z0, 0), le(z1, 0), le(z1, s(0)), le(z1, s(s(0))), z0, z1), LE(z0, 0))
   AVERAGE(z0, z1) -> c6(IF(le(z0, 0), le(z1, 0), le(z1, s(0)), le(z1, s(s(0))), z0, z1), LE(z1, 0))
   AVERAGE(z0, z1) -> c7(IF(le(z0, 0), le(z1, 0), le(z1, s(0)), le(z1, s(s(0))), z0, z1), LE(z1, s(0)))
   AVERAGE(z0, z1) -> c8(IF(le(z0, 0), le(z1, 0), le(z1, s(0)), le(z1, s(s(0))), z0, z1), LE(z1, s(s(0))))
   IF(true, z0, z1, z2, z3, z4) -> c9(IF2(z0, z1, z2, z3, z4))
   IF(false, z0, z1, z2, z3, z4) -> c10(AVERAGE(p(z3), s(z4)), P(z3))
   IF2(true, z0, z1, z2, z3) -> c11
   IF2(false, z0, z1, z2, z3) -> c12(IF3(z0, z1, z2, z3))
   IF3(true, z0, z1, z2) -> c13
   IF3(false, z0, z1, z2) -> c14(IF4(z0, z1, z2))
   IF4(true, z0, z1) -> c15
   IF4(false, z0, z1) -> c16(AVERAGE(s(z0), p(p(z1))), P(p(z1)), P(z1))

The (relative) TRS S consists of the following rules:

   p(s(z0)) -> z0
   p(0) -> 0
   le(0, z0) -> true
   le(s(z0), 0) -> false
   le(s(z0), s(z1)) -> le(z0, z1)
   average(z0, z1) -> if(le(z0, 0), le(z1, 0), le(z1, s(0)), le(z1, s(s(0))), z0, z1)
   if(true, z0, z1, z2, z3, z4) -> if2(z0, z1, z2, z3, z4)
   if(false, z0, z1, z2, z3, z4) -> average(p(z3), s(z4))
   if2(true, z0, z1, z2, z3) -> 0
   if2(false, z0, z1, z2, z3) -> if3(z0, z1, z2, z3)
   if3(true, z0, z1, z2) -> 0
   if3(false, z0, z1, z2) -> if4(z0, z1, z2)
   if4(true, z0, z1) -> s(0)
   if4(false, z0, z1) -> average(s(z0), p(p(z1)))

Rewrite Strategy: INNERMOST
----------------------------------------

(15) DecreasingLoopProof (LOWER BOUND(ID))
The following loop(s) give(s) rise to the lower bound Omega(n^1):

The rewrite sequence

LE(s(z0), s(z1)) ->^+ c4(LE(z0, z1))

gives rise to a decreasing loop by considering the right hand sides subterm at position [0].

The pumping substitution is [z0 / s(z0), z1 / s(z1)].

The result substitution is [ ].




----------------------------------------

(16)
Complex Obligation (BEST)

----------------------------------------

(17)
Obligation:
Proved the lower bound n^1 for the following obligation:

The Runtime Complexity (innermost) of the given CpxRelTRS could be proven to be BOUNDS(n^1, n^2).


The TRS R consists of the following rules:

   P(s(z0)) -> c
   P(0) -> c1
   LE(0, z0) -> c2
   LE(s(z0), 0) -> c3
   LE(s(z0), s(z1)) -> c4(LE(z0, z1))
   AVERAGE(z0, z1) -> c5(IF(le(z0, 0), le(z1, 0), le(z1, s(0)), le(z1, s(s(0))), z0, z1), LE(z0, 0))
   AVERAGE(z0, z1) -> c6(IF(le(z0, 0), le(z1, 0), le(z1, s(0)), le(z1, s(s(0))), z0, z1), LE(z1, 0))
   AVERAGE(z0, z1) -> c7(IF(le(z0, 0), le(z1, 0), le(z1, s(0)), le(z1, s(s(0))), z0, z1), LE(z1, s(0)))
   AVERAGE(z0, z1) -> c8(IF(le(z0, 0), le(z1, 0), le(z1, s(0)), le(z1, s(s(0))), z0, z1), LE(z1, s(s(0))))
   IF(true, z0, z1, z2, z3, z4) -> c9(IF2(z0, z1, z2, z3, z4))
   IF(false, z0, z1, z2, z3, z4) -> c10(AVERAGE(p(z3), s(z4)), P(z3))
   IF2(true, z0, z1, z2, z3) -> c11
   IF2(false, z0, z1, z2, z3) -> c12(IF3(z0, z1, z2, z3))
   IF3(true, z0, z1, z2) -> c13
   IF3(false, z0, z1, z2) -> c14(IF4(z0, z1, z2))
   IF4(true, z0, z1) -> c15
   IF4(false, z0, z1) -> c16(AVERAGE(s(z0), p(p(z1))), P(p(z1)), P(z1))

The (relative) TRS S consists of the following rules:

   p(s(z0)) -> z0
   p(0) -> 0
   le(0, z0) -> true
   le(s(z0), 0) -> false
   le(s(z0), s(z1)) -> le(z0, z1)
   average(z0, z1) -> if(le(z0, 0), le(z1, 0), le(z1, s(0)), le(z1, s(s(0))), z0, z1)
   if(true, z0, z1, z2, z3, z4) -> if2(z0, z1, z2, z3, z4)
   if(false, z0, z1, z2, z3, z4) -> average(p(z3), s(z4))
   if2(true, z0, z1, z2, z3) -> 0
   if2(false, z0, z1, z2, z3) -> if3(z0, z1, z2, z3)
   if3(true, z0, z1, z2) -> 0
   if3(false, z0, z1, z2) -> if4(z0, z1, z2)
   if4(true, z0, z1) -> s(0)
   if4(false, z0, z1) -> average(s(z0), p(p(z1)))

Rewrite Strategy: INNERMOST
----------------------------------------

(18) LowerBoundPropagationProof (FINISHED)
Propagated lower bound.
----------------------------------------

(19)
BOUNDS(n^1, INF)

----------------------------------------

(20)
Obligation:
Analyzing the following TRS for decreasing loops:

The Runtime Complexity (innermost) of the given CpxRelTRS could be proven to be BOUNDS(n^1, n^2).


The TRS R consists of the following rules:

   P(s(z0)) -> c
   P(0) -> c1
   LE(0, z0) -> c2
   LE(s(z0), 0) -> c3
   LE(s(z0), s(z1)) -> c4(LE(z0, z1))
   AVERAGE(z0, z1) -> c5(IF(le(z0, 0), le(z1, 0), le(z1, s(0)), le(z1, s(s(0))), z0, z1), LE(z0, 0))
   AVERAGE(z0, z1) -> c6(IF(le(z0, 0), le(z1, 0), le(z1, s(0)), le(z1, s(s(0))), z0, z1), LE(z1, 0))
   AVERAGE(z0, z1) -> c7(IF(le(z0, 0), le(z1, 0), le(z1, s(0)), le(z1, s(s(0))), z0, z1), LE(z1, s(0)))
   AVERAGE(z0, z1) -> c8(IF(le(z0, 0), le(z1, 0), le(z1, s(0)), le(z1, s(s(0))), z0, z1), LE(z1, s(s(0))))
   IF(true, z0, z1, z2, z3, z4) -> c9(IF2(z0, z1, z2, z3, z4))
   IF(false, z0, z1, z2, z3, z4) -> c10(AVERAGE(p(z3), s(z4)), P(z3))
   IF2(true, z0, z1, z2, z3) -> c11
   IF2(false, z0, z1, z2, z3) -> c12(IF3(z0, z1, z2, z3))
   IF3(true, z0, z1, z2) -> c13
   IF3(false, z0, z1, z2) -> c14(IF4(z0, z1, z2))
   IF4(true, z0, z1) -> c15
   IF4(false, z0, z1) -> c16(AVERAGE(s(z0), p(p(z1))), P(p(z1)), P(z1))

The (relative) TRS S consists of the following rules:

   p(s(z0)) -> z0
   p(0) -> 0
   le(0, z0) -> true
   le(s(z0), 0) -> false
   le(s(z0), s(z1)) -> le(z0, z1)
   average(z0, z1) -> if(le(z0, 0), le(z1, 0), le(z1, s(0)), le(z1, s(s(0))), z0, z1)
   if(true, z0, z1, z2, z3, z4) -> if2(z0, z1, z2, z3, z4)
   if(false, z0, z1, z2, z3, z4) -> average(p(z3), s(z4))
   if2(true, z0, z1, z2, z3) -> 0
   if2(false, z0, z1, z2, z3) -> if3(z0, z1, z2, z3)
   if3(true, z0, z1, z2) -> 0
   if3(false, z0, z1, z2) -> if4(z0, z1, z2)
   if4(true, z0, z1) -> s(0)
   if4(false, z0, z1) -> average(s(z0), p(p(z1)))

Rewrite Strategy: INNERMOST