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), 5885 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), 16 ms]
    (10) CpxRNTS
    (11) CompleteCoflocoProof [FINISHED, 16.2 s]
    (12) BOUNDS(1, n^2)
(13) RenamingProof [BOTH BOUNDS(ID, ID), 0 ms]
(14) CpxRelTRS
    (15) TypeInferenceProof [BOTH BOUNDS(ID, ID), 0 ms]
    (16) typed CpxTrs
    (17) OrderProof [LOWER BOUND(ID), 5 ms]
    (18) typed CpxTrs
    (19) RewriteLemmaProof [LOWER BOUND(ID), 299 ms]
    (20) BEST
        (21) proven lower bound
            (22) LowerBoundPropagationProof [FINISHED, 0 ms]
            (23) BOUNDS(n^1, INF)
        (24) typed CpxTrs
            (25) RewriteLemmaProof [LOWER BOUND(ID), 130 ms]
            (26) typed CpxTrs
            (27) RewriteLemmaProof [LOWER BOUND(ID), 34 ms]
            (28) typed CpxTrs
            (29) RewriteLemmaProof [LOWER BOUND(ID), 41 ms]
            (30) typed CpxTrs
            (31) RewriteLemmaProof [LOWER BOUND(ID), 58 ms]
            (32) typed CpxTrs
            (33) RewriteLemmaProof [LOWER BOUND(ID), 45 ms]
            (34) typed CpxTrs


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

(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:

   HALF(0) -> c
   HALF(s(0)) -> c1
   HALF(s(s(z0))) -> c2(HALF(z0))
   LE(0, z0) -> c3
   LE(s(z0), 0) -> c4
   LE(s(z0), s(z1)) -> c5(LE(z0, z1))
   INC(s(z0)) -> c6(INC(z0))
   INC(0) -> c7
   LOGARITHM(z0) -> c8(LOGITER(z0, 0))
   LOGITER(z0, z1) -> c9(IF(le(s(0), z0), le(s(s(0)), z0), half(z0), inc(z1)), LE(s(0), z0))
   LOGITER(z0, z1) -> c10(IF(le(s(0), z0), le(s(s(0)), z0), half(z0), inc(z1)), LE(s(s(0)), z0))
   LOGITER(z0, z1) -> c11(IF(le(s(0), z0), le(s(s(0)), z0), half(z0), inc(z1)), HALF(z0))
   LOGITER(z0, z1) -> c12(IF(le(s(0), z0), le(s(s(0)), z0), half(z0), inc(z1)), INC(z1))
   IF(false, z0, z1, z2) -> c13
   IF(true, false, z0, s(z1)) -> c14
   IF(true, true, z0, z1) -> c15(LOGITER(z0, z1))
   F -> c16
   F -> c17

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

   half(0) -> 0
   half(s(0)) -> 0
   half(s(s(z0))) -> s(half(z0))
   le(0, z0) -> true
   le(s(z0), 0) -> false
   le(s(z0), s(z1)) -> le(z0, z1)
   inc(s(z0)) -> s(inc(z0))
   inc(0) -> s(0)
   logarithm(z0) -> logIter(z0, 0)
   logIter(z0, z1) -> if(le(s(0), z0), le(s(s(0)), z0), half(z0), inc(z1))
   if(false, z0, z1, z2) -> logZeroError
   if(true, false, z0, s(z1)) -> z1
   if(true, true, z0, z1) -> logIter(z0, z1)
   f -> g
   f -> h

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:

   HALF(0) -> c
   HALF(s(0)) -> c1
   HALF(s(s(z0))) -> c2(HALF(z0))
   LE(0, z0) -> c3
   LE(s(z0), 0) -> c4
   LE(s(z0), s(z1)) -> c5(LE(z0, z1))
   INC(s(z0)) -> c6(INC(z0))
   INC(0) -> c7
   LOGARITHM(z0) -> c8(LOGITER(z0, 0))
   LOGITER(z0, z1) -> c9(IF(le(s(0), z0), le(s(s(0)), z0), half(z0), inc(z1)), LE(s(0), z0))
   LOGITER(z0, z1) -> c10(IF(le(s(0), z0), le(s(s(0)), z0), half(z0), inc(z1)), LE(s(s(0)), z0))
   LOGITER(z0, z1) -> c11(IF(le(s(0), z0), le(s(s(0)), z0), half(z0), inc(z1)), HALF(z0))
   LOGITER(z0, z1) -> c12(IF(le(s(0), z0), le(s(s(0)), z0), half(z0), inc(z1)), INC(z1))
   IF(false, z0, z1, z2) -> c13
   IF(true, false, z0, s(z1)) -> c14
   IF(true, true, z0, z1) -> c15(LOGITER(z0, z1))
   F -> c16
   F -> c17

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

   half(0) -> 0
   half(s(0)) -> 0
   half(s(s(z0))) -> s(half(z0))
   le(0, z0) -> true
   le(s(z0), 0) -> false
   le(s(z0), s(z1)) -> le(z0, z1)
   inc(s(z0)) -> s(inc(z0))
   inc(0) -> s(0)
   logarithm(z0) -> logIter(z0, 0)
   logIter(z0, z1) -> if(le(s(0), z0), le(s(s(0)), z0), half(z0), inc(z1))
   if(false, z0, z1, z2) -> logZeroError
   if(true, false, z0, s(z1)) -> z1
   if(true, true, z0, z1) -> logIter(z0, z1)
   f -> g
   f -> h

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:

   HALF(0) -> c [1]
   HALF(s(0)) -> c1 [1]
   HALF(s(s(z0))) -> c2(HALF(z0)) [1]
   LE(0, z0) -> c3 [1]
   LE(s(z0), 0) -> c4 [1]
   LE(s(z0), s(z1)) -> c5(LE(z0, z1)) [1]
   INC(s(z0)) -> c6(INC(z0)) [1]
   INC(0) -> c7 [1]
   LOGARITHM(z0) -> c8(LOGITER(z0, 0)) [1]
   LOGITER(z0, z1) -> c9(IF(le(s(0), z0), le(s(s(0)), z0), half(z0), inc(z1)), LE(s(0), z0)) [1]
   LOGITER(z0, z1) -> c10(IF(le(s(0), z0), le(s(s(0)), z0), half(z0), inc(z1)), LE(s(s(0)), z0)) [1]
   LOGITER(z0, z1) -> c11(IF(le(s(0), z0), le(s(s(0)), z0), half(z0), inc(z1)), HALF(z0)) [1]
   LOGITER(z0, z1) -> c12(IF(le(s(0), z0), le(s(s(0)), z0), half(z0), inc(z1)), INC(z1)) [1]
   IF(false, z0, z1, z2) -> c13 [1]
   IF(true, false, z0, s(z1)) -> c14 [1]
   IF(true, true, z0, z1) -> c15(LOGITER(z0, z1)) [1]
   F -> c16 [1]
   F -> c17 [1]
   half(0) -> 0 [0]
   half(s(0)) -> 0 [0]
   half(s(s(z0))) -> s(half(z0)) [0]
   le(0, z0) -> true [0]
   le(s(z0), 0) -> false [0]
   le(s(z0), s(z1)) -> le(z0, z1) [0]
   inc(s(z0)) -> s(inc(z0)) [0]
   inc(0) -> s(0) [0]
   logarithm(z0) -> logIter(z0, 0) [0]
   logIter(z0, z1) -> if(le(s(0), z0), le(s(s(0)), z0), half(z0), inc(z1)) [0]
   if(false, z0, z1, z2) -> logZeroError [0]
   if(true, false, z0, s(z1)) -> z1 [0]
   if(true, true, z0, z1) -> logIter(z0, z1) [0]
   f -> g [0]
   f -> h [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:

   HALF(0) -> c [1]
   HALF(s(0)) -> c1 [1]
   HALF(s(s(z0))) -> c2(HALF(z0)) [1]
   LE(0, z0) -> c3 [1]
   LE(s(z0), 0) -> c4 [1]
   LE(s(z0), s(z1)) -> c5(LE(z0, z1)) [1]
   INC(s(z0)) -> c6(INC(z0)) [1]
   INC(0) -> c7 [1]
   LOGARITHM(z0) -> c8(LOGITER(z0, 0)) [1]
   LOGITER(z0, z1) -> c9(IF(le(s(0), z0), le(s(s(0)), z0), half(z0), inc(z1)), LE(s(0), z0)) [1]
   LOGITER(z0, z1) -> c10(IF(le(s(0), z0), le(s(s(0)), z0), half(z0), inc(z1)), LE(s(s(0)), z0)) [1]
   LOGITER(z0, z1) -> c11(IF(le(s(0), z0), le(s(s(0)), z0), half(z0), inc(z1)), HALF(z0)) [1]
   LOGITER(z0, z1) -> c12(IF(le(s(0), z0), le(s(s(0)), z0), half(z0), inc(z1)), INC(z1)) [1]
   IF(false, z0, z1, z2) -> c13 [1]
   IF(true, false, z0, s(z1)) -> c14 [1]
   IF(true, true, z0, z1) -> c15(LOGITER(z0, z1)) [1]
   F -> c16 [1]
   F -> c17 [1]
   half(0) -> 0 [0]
   half(s(0)) -> 0 [0]
   half(s(s(z0))) -> s(half(z0)) [0]
   le(0, z0) -> true [0]
   le(s(z0), 0) -> false [0]
   le(s(z0), s(z1)) -> le(z0, z1) [0]
   inc(s(z0)) -> s(inc(z0)) [0]
   inc(0) -> s(0) [0]
   logarithm(z0) -> logIter(z0, 0) [0]
   logIter(z0, z1) -> if(le(s(0), z0), le(s(s(0)), z0), half(z0), inc(z1)) [0]
   if(false, z0, z1, z2) -> logZeroError [0]
   if(true, false, z0, s(z1)) -> z1 [0]
   if(true, true, z0, z1) -> logIter(z0, z1) [0]
   f -> g [0]
   f -> h [0]

The TRS has the following type information:
HALF :: 0:s:logZeroError -> c:c1:c2
0 :: 0:s:logZeroError
c :: c:c1:c2
s :: 0:s:logZeroError -> 0:s:logZeroError
c1 :: c:c1:c2
c2 :: c:c1:c2 -> c:c1:c2
LE :: 0:s:logZeroError -> 0:s:logZeroError -> c3:c4:c5
c3 :: c3:c4:c5
c4 :: c3:c4:c5
c5 :: c3:c4:c5 -> c3:c4:c5
INC :: 0:s:logZeroError -> c6:c7
c6 :: c6:c7 -> c6:c7
c7 :: c6:c7
LOGARITHM :: 0:s:logZeroError -> c8
c8 :: c9:c10:c11:c12 -> c8
LOGITER :: 0:s:logZeroError -> 0:s:logZeroError -> c9:c10:c11:c12
c9 :: c13:c14:c15 -> c3:c4:c5 -> c9:c10:c11:c12
IF :: false:true -> false:true -> 0:s:logZeroError -> 0:s:logZeroError -> c13:c14:c15
le :: 0:s:logZeroError -> 0:s:logZeroError -> false:true
half :: 0:s:logZeroError -> 0:s:logZeroError
inc :: 0:s:logZeroError -> 0:s:logZeroError
c10 :: c13:c14:c15 -> c3:c4:c5 -> c9:c10:c11:c12
c11 :: c13:c14:c15 -> c:c1:c2 -> c9:c10:c11:c12
c12 :: c13:c14:c15 -> c6:c7 -> c9:c10:c11:c12
false :: false:true
c13 :: c13:c14:c15
true :: false:true
c14 :: c13:c14:c15
c15 :: c9:c10:c11:c12 -> c13:c14:c15
F :: c16:c17
c16 :: c16:c17
c17 :: c16:c17
logarithm :: 0:s:logZeroError -> 0:s:logZeroError
logIter :: 0:s:logZeroError -> 0:s:logZeroError -> 0:s:logZeroError
if :: false:true -> false:true -> 0:s:logZeroError -> 0:s:logZeroError -> 0:s:logZeroError
logZeroError :: 0:s:logZeroError
f :: g:h
g :: g:h
h :: g:h

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:

   half(v0) -> null_half [0]
   le(v0, v1) -> null_le [0]
   inc(v0) -> null_inc [0]
   logarithm(v0) -> null_logarithm [0]
   logIter(v0, v1) -> null_logIter [0]
   if(v0, v1, v2, v3) -> null_if [0]
   f -> null_f [0]
   HALF(v0) -> null_HALF [0]
   LE(v0, v1) -> null_LE [0]
   INC(v0) -> null_INC [0]
   IF(v0, v1, v2, v3) -> null_IF [0]

And the following fresh constants:    null_half, null_le, null_inc, null_logarithm, null_logIter, null_if, null_f, null_HALF, null_LE, null_INC, null_IF, const, const1

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

(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:

   HALF(0) -> c [1]
   HALF(s(0)) -> c1 [1]
   HALF(s(s(z0))) -> c2(HALF(z0)) [1]
   LE(0, z0) -> c3 [1]
   LE(s(z0), 0) -> c4 [1]
   LE(s(z0), s(z1)) -> c5(LE(z0, z1)) [1]
   INC(s(z0)) -> c6(INC(z0)) [1]
   INC(0) -> c7 [1]
   LOGARITHM(z0) -> c8(LOGITER(z0, 0)) [1]
   LOGITER(z0, z1) -> c9(IF(le(s(0), z0), le(s(s(0)), z0), half(z0), inc(z1)), LE(s(0), z0)) [1]
   LOGITER(z0, z1) -> c10(IF(le(s(0), z0), le(s(s(0)), z0), half(z0), inc(z1)), LE(s(s(0)), z0)) [1]
   LOGITER(z0, z1) -> c11(IF(le(s(0), z0), le(s(s(0)), z0), half(z0), inc(z1)), HALF(z0)) [1]
   LOGITER(z0, z1) -> c12(IF(le(s(0), z0), le(s(s(0)), z0), half(z0), inc(z1)), INC(z1)) [1]
   IF(false, z0, z1, z2) -> c13 [1]
   IF(true, false, z0, s(z1)) -> c14 [1]
   IF(true, true, z0, z1) -> c15(LOGITER(z0, z1)) [1]
   F -> c16 [1]
   F -> c17 [1]
   half(0) -> 0 [0]
   half(s(0)) -> 0 [0]
   half(s(s(z0))) -> s(half(z0)) [0]
   le(0, z0) -> true [0]
   le(s(z0), 0) -> false [0]
   le(s(z0), s(z1)) -> le(z0, z1) [0]
   inc(s(z0)) -> s(inc(z0)) [0]
   inc(0) -> s(0) [0]
   logarithm(z0) -> logIter(z0, 0) [0]
   logIter(z0, z1) -> if(le(s(0), z0), le(s(s(0)), z0), half(z0), inc(z1)) [0]
   if(false, z0, z1, z2) -> logZeroError [0]
   if(true, false, z0, s(z1)) -> z1 [0]
   if(true, true, z0, z1) -> logIter(z0, z1) [0]
   f -> g [0]
   f -> h [0]
   half(v0) -> null_half [0]
   le(v0, v1) -> null_le [0]
   inc(v0) -> null_inc [0]
   logarithm(v0) -> null_logarithm [0]
   logIter(v0, v1) -> null_logIter [0]
   if(v0, v1, v2, v3) -> null_if [0]
   f -> null_f [0]
   HALF(v0) -> null_HALF [0]
   LE(v0, v1) -> null_LE [0]
   INC(v0) -> null_INC [0]
   IF(v0, v1, v2, v3) -> null_IF [0]

The TRS has the following type information:
HALF :: 0:s:logZeroError:null_half:null_inc:null_logarithm:null_logIter:null_if -> c:c1:c2:null_HALF
0 :: 0:s:logZeroError:null_half:null_inc:null_logarithm:null_logIter:null_if
c :: c:c1:c2:null_HALF
s :: 0:s:logZeroError:null_half:null_inc:null_logarithm:null_logIter:null_if -> 0:s:logZeroError:null_half:null_inc:null_logarithm:null_logIter:null_if
c1 :: c:c1:c2:null_HALF
c2 :: c:c1:c2:null_HALF -> c:c1:c2:null_HALF
LE :: 0:s:logZeroError:null_half:null_inc:null_logarithm:null_logIter:null_if -> 0:s:logZeroError:null_half:null_inc:null_logarithm:null_logIter:null_if -> c3:c4:c5:null_LE
c3 :: c3:c4:c5:null_LE
c4 :: c3:c4:c5:null_LE
c5 :: c3:c4:c5:null_LE -> c3:c4:c5:null_LE
INC :: 0:s:logZeroError:null_half:null_inc:null_logarithm:null_logIter:null_if -> c6:c7:null_INC
c6 :: c6:c7:null_INC -> c6:c7:null_INC
c7 :: c6:c7:null_INC
LOGARITHM :: 0:s:logZeroError:null_half:null_inc:null_logarithm:null_logIter:null_if -> c8
c8 :: c9:c10:c11:c12 -> c8
LOGITER :: 0:s:logZeroError:null_half:null_inc:null_logarithm:null_logIter:null_if -> 0:s:logZeroError:null_half:null_inc:null_logarithm:null_logIter:null_if -> c9:c10:c11:c12
c9 :: c13:c14:c15:null_IF -> c3:c4:c5:null_LE -> c9:c10:c11:c12
IF :: false:true:null_le -> false:true:null_le -> 0:s:logZeroError:null_half:null_inc:null_logarithm:null_logIter:null_if -> 0:s:logZeroError:null_half:null_inc:null_logarithm:null_logIter:null_if -> c13:c14:c15:null_IF
le :: 0:s:logZeroError:null_half:null_inc:null_logarithm:null_logIter:null_if -> 0:s:logZeroError:null_half:null_inc:null_logarithm:null_logIter:null_if -> false:true:null_le
half :: 0:s:logZeroError:null_half:null_inc:null_logarithm:null_logIter:null_if -> 0:s:logZeroError:null_half:null_inc:null_logarithm:null_logIter:null_if
inc :: 0:s:logZeroError:null_half:null_inc:null_logarithm:null_logIter:null_if -> 0:s:logZeroError:null_half:null_inc:null_logarithm:null_logIter:null_if
c10 :: c13:c14:c15:null_IF -> c3:c4:c5:null_LE -> c9:c10:c11:c12
c11 :: c13:c14:c15:null_IF -> c:c1:c2:null_HALF -> c9:c10:c11:c12
c12 :: c13:c14:c15:null_IF -> c6:c7:null_INC -> c9:c10:c11:c12
false :: false:true:null_le
c13 :: c13:c14:c15:null_IF
true :: false:true:null_le
c14 :: c13:c14:c15:null_IF
c15 :: c9:c10:c11:c12 -> c13:c14:c15:null_IF
F :: c16:c17
c16 :: c16:c17
c17 :: c16:c17
logarithm :: 0:s:logZeroError:null_half:null_inc:null_logarithm:null_logIter:null_if -> 0:s:logZeroError:null_half:null_inc:null_logarithm:null_logIter:null_if
logIter :: 0:s:logZeroError:null_half:null_inc:null_logarithm:null_logIter:null_if -> 0:s:logZeroError:null_half:null_inc:null_logarithm:null_logIter:null_if -> 0:s:logZeroError:null_half:null_inc:null_logarithm:null_logIter:null_if
if :: false:true:null_le -> false:true:null_le -> 0:s:logZeroError:null_half:null_inc:null_logarithm:null_logIter:null_if -> 0:s:logZeroError:null_half:null_inc:null_logarithm:null_logIter:null_if -> 0:s:logZeroError:null_half:null_inc:null_logarithm:null_logIter:null_if
logZeroError :: 0:s:logZeroError:null_half:null_inc:null_logarithm:null_logIter:null_if
f :: g:h:null_f
g :: g:h:null_f
h :: g:h:null_f
null_half :: 0:s:logZeroError:null_half:null_inc:null_logarithm:null_logIter:null_if
null_le :: false:true:null_le
null_inc :: 0:s:logZeroError:null_half:null_inc:null_logarithm:null_logIter:null_if
null_logarithm :: 0:s:logZeroError:null_half:null_inc:null_logarithm:null_logIter:null_if
null_logIter :: 0:s:logZeroError:null_half:null_inc:null_logarithm:null_logIter:null_if
null_if :: 0:s:logZeroError:null_half:null_inc:null_logarithm:null_logIter:null_if
null_f :: g:h:null_f
null_HALF :: c:c1:c2:null_HALF
null_LE :: c3:c4:c5:null_LE
null_INC :: c6:c7:null_INC
null_IF :: c13:c14:c15:null_IF
const :: c8
const1 :: c9:c10:c11:c12

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:

   0 => 0
   c => 0
   c1 => 1
   c3 => 0
   c4 => 1
   c7 => 0
   false => 1
   c13 => 0
   true => 2
   c14 => 1
   c16 => 0
   c17 => 1
   logZeroError => 1
   g => 1
   h => 2
   null_half => 0
   null_le => 0
   null_inc => 0
   null_logarithm => 0
   null_logIter => 0
   null_if => 0
   null_f => 0
   null_HALF => 0
   null_LE => 0
   null_INC => 0
   null_IF => 0
   const => 0
   const1 => 0

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

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

   F -{ 1 }-> 1 :|: 
   F -{ 1 }-> 0 :|: 
   HALF(z) -{ 1 }-> 1 :|: z = 1 + 0
   HALF(z) -{ 1 }-> 0 :|: z = 0
   HALF(z) -{ 0 }-> 0 :|: v0 >= 0, z = v0
   HALF(z) -{ 1 }-> 1 + HALF(z0) :|: z0 >= 0, z = 1 + (1 + z0)
   IF(z, z', z'', z3) -{ 1 }-> 1 :|: z = 2, z3 = 1 + z1, z1 >= 0, z'' = z0, z0 >= 0, z' = 1
   IF(z, z', z'', z3) -{ 1 }-> 0 :|: z1 >= 0, z = 1, z0 >= 0, z3 = z2, z' = z0, z2 >= 0, z'' = z1
   IF(z, z', z'', z3) -{ 0 }-> 0 :|: v0 >= 0, z'' = v2, v1 >= 0, z = v0, z' = v1, z3 = v3, v2 >= 0, v3 >= 0
   IF(z, z', z'', z3) -{ 1 }-> 1 + LOGITER(z0, z1) :|: z = 2, z1 >= 0, z' = 2, z'' = z0, z3 = z1, z0 >= 0
   INC(z) -{ 1 }-> 0 :|: z = 0
   INC(z) -{ 0 }-> 0 :|: v0 >= 0, z = v0
   INC(z) -{ 1 }-> 1 + INC(z0) :|: z = 1 + z0, z0 >= 0
   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
   LOGARITHM(z) -{ 1 }-> 1 + LOGITER(z0, 0) :|: z = z0, z0 >= 0
   LOGITER(z, z') -{ 1 }-> 1 + IF(le(1 + 0, z0), le(1 + (1 + 0), z0), half(z0), inc(z1)) + LE(1 + 0, z0) :|: z = z0, z1 >= 0, z' = z1, z0 >= 0
   LOGITER(z, z') -{ 1 }-> 1 + IF(le(1 + 0, z0), le(1 + (1 + 0), z0), half(z0), inc(z1)) + LE(1 + (1 + 0), z0) :|: z = z0, z1 >= 0, z' = z1, z0 >= 0
   LOGITER(z, z') -{ 1 }-> 1 + IF(le(1 + 0, z0), le(1 + (1 + 0), z0), half(z0), inc(z1)) + INC(z1) :|: z = z0, z1 >= 0, z' = z1, z0 >= 0
   LOGITER(z, z') -{ 1 }-> 1 + IF(le(1 + 0, z0), le(1 + (1 + 0), z0), half(z0), inc(z1)) + HALF(z0) :|: z = z0, z1 >= 0, z' = z1, z0 >= 0
   f -{ 0 }-> 2 :|: 
   f -{ 0 }-> 1 :|: 
   f -{ 0 }-> 0 :|: 
   half(z) -{ 0 }-> 0 :|: z = 0
   half(z) -{ 0 }-> 0 :|: z = 1 + 0
   half(z) -{ 0 }-> 0 :|: v0 >= 0, z = v0
   half(z) -{ 0 }-> 1 + half(z0) :|: z0 >= 0, z = 1 + (1 + z0)
   if(z, z', z'', z3) -{ 0 }-> z1 :|: z = 2, z3 = 1 + z1, z1 >= 0, z'' = z0, z0 >= 0, z' = 1
   if(z, z', z'', z3) -{ 0 }-> logIter(z0, z1) :|: z = 2, z1 >= 0, z' = 2, z'' = z0, z3 = z1, z0 >= 0
   if(z, z', z'', z3) -{ 0 }-> 1 :|: z1 >= 0, z = 1, z0 >= 0, z3 = z2, z' = z0, z2 >= 0, z'' = z1
   if(z, z', z'', z3) -{ 0 }-> 0 :|: v0 >= 0, z'' = v2, v1 >= 0, z = v0, z' = v1, z3 = v3, v2 >= 0, v3 >= 0
   inc(z) -{ 0 }-> 0 :|: v0 >= 0, z = v0
   inc(z) -{ 0 }-> 1 + inc(z0) :|: z = 1 + z0, z0 >= 0
   inc(z) -{ 0 }-> 1 + 0 :|: z = 0
   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
   logIter(z, z') -{ 0 }-> if(le(1 + 0, z0), le(1 + (1 + 0), z0), half(z0), inc(z1)) :|: z = z0, z1 >= 0, z' = z1, z0 >= 0
   logIter(z, z') -{ 0 }-> 0 :|: v0 >= 0, v1 >= 0, z = v0, z' = v1
   logarithm(z) -{ 0 }-> logIter(z0, 0) :|: z = z0, z0 >= 0
   logarithm(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, V18, V21),0,[fun(V, Out)],[V >= 0]).
eq(start(V, V2, V18, V21),0,[fun1(V, V2, Out)],[V >= 0,V2 >= 0]).
eq(start(V, V2, V18, V21),0,[fun2(V, Out)],[V >= 0]).
eq(start(V, V2, V18, V21),0,[fun3(V, Out)],[V >= 0]).
eq(start(V, V2, V18, V21),0,[fun4(V, V2, Out)],[V >= 0,V2 >= 0]).
eq(start(V, V2, V18, V21),0,[fun5(V, V2, V18, V21, Out)],[V >= 0,V2 >= 0,V18 >= 0,V21 >= 0]).
eq(start(V, V2, V18, V21),0,[fun6(Out)],[]).
eq(start(V, V2, V18, V21),0,[half(V, Out)],[V >= 0]).
eq(start(V, V2, V18, V21),0,[le(V, V2, Out)],[V >= 0,V2 >= 0]).
eq(start(V, V2, V18, V21),0,[inc(V, Out)],[V >= 0]).
eq(start(V, V2, V18, V21),0,[logarithm(V, Out)],[V >= 0]).
eq(start(V, V2, V18, V21),0,[logIter(V, V2, Out)],[V >= 0,V2 >= 0]).
eq(start(V, V2, V18, V21),0,[if(V, V2, V18, V21, Out)],[V >= 0,V2 >= 0,V18 >= 0,V21 >= 0]).
eq(start(V, V2, V18, V21),0,[f(Out)],[]).
eq(fun(V, Out),1,[],[Out = 0,V = 0]).
eq(fun(V, Out),1,[],[Out = 1,V = 1]).
eq(fun(V, Out),1,[fun(V1, Ret1)],[Out = 1 + Ret1,V1 >= 0,V = 2 + V1]).
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, Ret11)],[Out = 1 + Ret11,V6 >= 0,V = 1 + V5,V5 >= 0,V2 = 1 + V6]).
eq(fun2(V, Out),1,[fun2(V7, Ret12)],[Out = 1 + Ret12,V = 1 + V7,V7 >= 0]).
eq(fun2(V, Out),1,[],[Out = 0,V = 0]).
eq(fun3(V, Out),1,[fun4(V8, 0, Ret13)],[Out = 1 + Ret13,V = V8,V8 >= 0]).
eq(fun4(V, V2, Out),1,[le(1 + 0, V9, Ret010),le(1 + (1 + 0), V9, Ret011),half(V9, Ret012),inc(V10, Ret013),fun5(Ret010, Ret011, Ret012, Ret013, Ret01),fun1(1 + 0, V9, Ret14)],[Out = 1 + Ret01 + Ret14,V = V9,V10 >= 0,V2 = V10,V9 >= 0]).
eq(fun4(V, V2, Out),1,[le(1 + 0, V12, Ret0101),le(1 + (1 + 0), V12, Ret0111),half(V12, Ret0121),inc(V11, Ret0131),fun5(Ret0101, Ret0111, Ret0121, Ret0131, Ret014),fun1(1 + (1 + 0), V12, Ret15)],[Out = 1 + Ret014 + Ret15,V = V12,V11 >= 0,V2 = V11,V12 >= 0]).
eq(fun4(V, V2, Out),1,[le(1 + 0, V14, Ret0102),le(1 + (1 + 0), V14, Ret0112),half(V14, Ret0122),inc(V13, Ret0132),fun5(Ret0102, Ret0112, Ret0122, Ret0132, Ret015),fun(V14, Ret16)],[Out = 1 + Ret015 + Ret16,V = V14,V13 >= 0,V2 = V13,V14 >= 0]).
eq(fun4(V, V2, Out),1,[le(1 + 0, V16, Ret0103),le(1 + (1 + 0), V16, Ret0113),half(V16, Ret0123),inc(V15, Ret0133),fun5(Ret0103, Ret0113, Ret0123, Ret0133, Ret016),fun2(V15, Ret17)],[Out = 1 + Ret016 + Ret17,V = V16,V15 >= 0,V2 = V15,V16 >= 0]).
eq(fun5(V, V2, V18, V21, Out),1,[],[Out = 0,V17 >= 0,V = 1,V19 >= 0,V21 = V20,V2 = V19,V20 >= 0,V18 = V17]).
eq(fun5(V, V2, V18, V21, Out),1,[],[Out = 1,V = 2,V21 = 1 + V22,V22 >= 0,V18 = V23,V23 >= 0,V2 = 1]).
eq(fun5(V, V2, V18, V21, Out),1,[fun4(V25, V24, Ret18)],[Out = 1 + Ret18,V = 2,V24 >= 0,V2 = 2,V18 = V25,V21 = V24,V25 >= 0]).
eq(fun6(Out),1,[],[Out = 0]).
eq(fun6(Out),1,[],[Out = 1]).
eq(half(V, Out),0,[],[Out = 0,V = 0]).
eq(half(V, Out),0,[],[Out = 0,V = 1]).
eq(half(V, Out),0,[half(V26, Ret19)],[Out = 1 + Ret19,V26 >= 0,V = 2 + V26]).
eq(le(V, V2, Out),0,[],[Out = 2,V27 >= 0,V = 0,V2 = V27]).
eq(le(V, V2, Out),0,[],[Out = 1,V = 1 + V28,V28 >= 0,V2 = 0]).
eq(le(V, V2, Out),0,[le(V29, V30, Ret)],[Out = Ret,V30 >= 0,V = 1 + V29,V29 >= 0,V2 = 1 + V30]).
eq(inc(V, Out),0,[inc(V31, Ret110)],[Out = 1 + Ret110,V = 1 + V31,V31 >= 0]).
eq(inc(V, Out),0,[],[Out = 1,V = 0]).
eq(logarithm(V, Out),0,[logIter(V32, 0, Ret2)],[Out = Ret2,V = V32,V32 >= 0]).
eq(logIter(V, V2, Out),0,[le(1 + 0, V33, Ret0),le(1 + (1 + 0), V33, Ret111),half(V33, Ret21),inc(V34, Ret3),if(Ret0, Ret111, Ret21, Ret3, Ret4)],[Out = Ret4,V = V33,V34 >= 0,V2 = V34,V33 >= 0]).
eq(if(V, V2, V18, V21, Out),0,[],[Out = 1,V37 >= 0,V = 1,V35 >= 0,V21 = V36,V2 = V35,V36 >= 0,V18 = V37]).
eq(if(V, V2, V18, V21, Out),0,[],[Out = V38,V = 2,V21 = 1 + V38,V38 >= 0,V18 = V39,V39 >= 0,V2 = 1]).
eq(if(V, V2, V18, V21, Out),0,[logIter(V41, V40, Ret5)],[Out = Ret5,V = 2,V40 >= 0,V2 = 2,V18 = V41,V21 = V40,V41 >= 0]).
eq(f(Out),0,[],[Out = 1]).
eq(f(Out),0,[],[Out = 2]).
eq(half(V, Out),0,[],[Out = 0,V42 >= 0,V = V42]).
eq(le(V, V2, Out),0,[],[Out = 0,V44 >= 0,V43 >= 0,V = V44,V2 = V43]).
eq(inc(V, Out),0,[],[Out = 0,V45 >= 0,V = V45]).
eq(logarithm(V, Out),0,[],[Out = 0,V46 >= 0,V = V46]).
eq(logIter(V, V2, Out),0,[],[Out = 0,V47 >= 0,V48 >= 0,V = V47,V2 = V48]).
eq(if(V, V2, V18, V21, Out),0,[],[Out = 0,V49 >= 0,V18 = V52,V50 >= 0,V = V49,V2 = V50,V21 = V51,V52 >= 0,V51 >= 0]).
eq(f(Out),0,[],[Out = 0]).
eq(fun(V, Out),0,[],[Out = 0,V53 >= 0,V = V53]).
eq(fun1(V, V2, Out),0,[],[Out = 0,V54 >= 0,V55 >= 0,V = V54,V2 = V55]).
eq(fun2(V, Out),0,[],[Out = 0,V56 >= 0,V = V56]).
eq(fun5(V, V2, V18, V21, Out),0,[],[Out = 0,V58 >= 0,V18 = V59,V57 >= 0,V = V58,V2 = V57,V21 = V60,V59 >= 0,V60 >= 0]).
input_output_vars(fun(V,Out),[V],[Out]).
input_output_vars(fun1(V,V2,Out),[V,V2],[Out]).
input_output_vars(fun2(V,Out),[V],[Out]).
input_output_vars(fun3(V,Out),[V],[Out]).
input_output_vars(fun4(V,V2,Out),[V,V2],[Out]).
input_output_vars(fun5(V,V2,V18,V21,Out),[V,V2,V18,V21],[Out]).
input_output_vars(fun6(Out),[],[Out]).
input_output_vars(half(V,Out),[V],[Out]).
input_output_vars(le(V,V2,Out),[V,V2],[Out]).
input_output_vars(inc(V,Out),[V],[Out]).
input_output_vars(logarithm(V,Out),[V],[Out]).
input_output_vars(logIter(V,V2,Out),[V,V2],[Out]).
input_output_vars(if(V,V2,V18,V21,Out),[V,V2,V18,V21],[Out]).
input_output_vars(f(Out),[],[Out]).


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

#### Computed strongly connected components 
0. non_recursive  : [f/1]
1. recursive  : [fun/2]
2. recursive  : [fun1/3]
3. recursive  : [fun2/2]
4. recursive  : [half/2]
5. recursive  : [inc/2]
6. recursive  : [le/3]
7. recursive [non_tail] : [fun4/3,fun5/5]
8. non_recursive  : [fun3/2]
9. non_recursive  : [fun6/1]
10. recursive  : [if/5,logIter/3]
11. non_recursive  : [logarithm/2]
12. non_recursive  : [start/4]

#### Obtained direct recursion through partial evaluation 
0. SCC is partially evaluated into f/1
1. SCC is partially evaluated into fun/2
2. SCC is partially evaluated into fun1/3
3. SCC is partially evaluated into fun2/2
4. SCC is partially evaluated into half/2
5. SCC is partially evaluated into inc/2
6. SCC is partially evaluated into le/3
7. SCC is partially evaluated into fun4/3
8. SCC is completely evaluated into other SCCs
9. SCC is partially evaluated into fun6/1
10. SCC is partially evaluated into logIter/3
11. SCC is partially evaluated into logarithm/2
12. SCC is partially evaluated into start/4

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

### Specialization of cost equations f/1 
* CE 65 is refined into CE [67] 
* CE 64 is refined into CE [68] 
* CE 66 is refined into CE [69] 


### Cost equations --> "Loop" of f/1 
* CEs [67] --> Loop 30 
* CEs [68] --> Loop 31 
* CEs [69] --> Loop 32 

### Ranking functions of CR f(Out) 

#### Partial ranking functions of CR f(Out) 


### Specialization of cost equations fun/2 
* CE 40 is refined into CE [70] 
* CE 39 is refined into CE [71] 
* CE 42 is refined into CE [72] 
* CE 41 is refined into CE [73] 


### Cost equations --> "Loop" of fun/2 
* CEs [73] --> Loop 33 
* CEs [70] --> Loop 34 
* CEs [71,72] --> Loop 35 

### Ranking functions of CR fun(V,Out) 
* RF of phase [33]: [V-1]

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


### Specialization of cost equations fun1/3 
* CE 44 is refined into CE [74] 
* CE 43 is refined into CE [75] 
* CE 46 is refined into CE [76] 
* CE 45 is refined into CE [77] 


### Cost equations --> "Loop" of fun1/3 
* CEs [77] --> Loop 36 
* CEs [74] --> Loop 37 
* CEs [75,76] --> Loop 38 

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

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


### Specialization of cost equations fun2/2 
* CE 48 is refined into CE [78] 
* CE 49 is refined into CE [79] 
* CE 47 is refined into CE [80] 


### Cost equations --> "Loop" of fun2/2 
* CEs [80] --> Loop 39 
* CEs [78,79] --> Loop 40 

### Ranking functions of CR fun2(V,Out) 
* RF of phase [39]: [V]

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


### Specialization of cost equations half/2 
* CE 52 is refined into CE [81] 
* CE 53 is refined into CE [82] 
* CE 54 is refined into CE [83] 


### Cost equations --> "Loop" of half/2 
* CEs [83] --> Loop 41 
* CEs [81,82] --> Loop 42 

### Ranking functions of CR half(V,Out) 
* RF of phase [41]: [V-1]

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


### Specialization of cost equations inc/2 
* CE 61 is refined into CE [84] 
* CE 60 is refined into CE [85] 
* CE 59 is refined into CE [86] 


### Cost equations --> "Loop" of inc/2 
* CEs [86] --> Loop 43 
* CEs [84] --> Loop 44 
* CEs [85] --> Loop 45 

### Ranking functions of CR inc(V,Out) 
* RF of phase [43]: [V]

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


### Specialization of cost equations le/3 
* CE 58 is refined into CE [87] 
* CE 56 is refined into CE [88] 
* CE 55 is refined into CE [89] 
* CE 57 is refined into CE [90] 


### Cost equations --> "Loop" of le/3 
* CEs [90] --> Loop 46 
* CEs [87] --> Loop 47 
* CEs [88] --> Loop 48 
* CEs [89] --> Loop 49 

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

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


### Specialization of cost equations fun4/3 
* CE 23 is refined into CE [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,158,159,160,161,162,163,164,165,166,167,168,169,170,171,172,173,174,175,176,177,178,179,180,181] 
* CE 24 is refined into CE [182,183,184,185,186,187,188,189,190,191,192,193,194,195,196,197,198,199,200,201,202,203,204,205,206,207,208,209,210,211,212,213,214,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] 
* CE 25 is refined into CE [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,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] 
* CE 26 is refined into CE [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] 
* CE 31 is refined into CE [546,547,548,549,550] 
* CE 32 is refined into CE [551,552,553,554,555,556] 
* CE 33 is refined into CE [557,558,559,560,561,562,563,564,565] 
* CE 34 is refined into CE [566,567,568,569,570,571] 
* CE 35 is refined into CE [572,573,574,575,576,577,578,579,580,581,582,583,584,585] 
* CE 36 is refined into CE [586,587,588,589,590,591,592,593] 
* CE 37 is refined into CE [594,595,596,597,598,599,600,601,602,603,604,605,606,607,608,609] 
* CE 38 is refined into CE [610,611,612,613,614,615,616,617,618,619,620,621,622,623,624,625] 
* CE 27 is refined into CE [626,627,628,629,630,631,632,633,634,635,636,637,638,639] 
* CE 28 is refined into CE [640,641,642,643,644,645,646,647,648,649,650,651,652,653,654,655,656,657,658,659,660,661,662,663] 
* CE 29 is refined into CE [664,665,666,667,668,669,670,671,672,673,674,675,676,677,678,679] 
* CE 30 is refined into CE [680,681,682,683,684,685,686,687,688,689,690,691,692,693,694,695] 


### Cost equations --> "Loop" of fun4/3 
* CEs [639] --> Loop 50 
* CEs [663] --> Loop 51 
* CEs [662] --> Loop 52 
* CEs [679,695] --> Loop 53 
* CEs [638,661,678,694] --> Loop 54 
* CEs [637] --> Loop 55 
* CEs [660] --> Loop 56 
* CEs [659] --> Loop 57 
* CEs [677,693] --> Loop 58 
* CEs [636,658,676,692] --> Loop 59 
* CEs [635] --> Loop 60 
* CEs [657] --> Loop 61 
* CEs [656] --> Loop 62 
* CEs [675,691] --> Loop 63 
* CEs [634,655,674,690] --> Loop 64 
* CEs [651] --> Loop 65 
* CEs [632] --> Loop 66 
* CEs [650] --> Loop 67 
* CEs [671,687] --> Loop 68 
* CEs [631,649,670,686] --> Loop 69 
* CEs [648] --> Loop 70 
* CEs [630] --> Loop 71 
* CEs [647] --> Loop 72 
* CEs [669,685] --> Loop 73 
* CEs [629,646,668,684] --> Loop 74 
* CEs [645] --> Loop 75 
* CEs [628] --> Loop 76 
* CEs [644] --> Loop 77 
* CEs [667,683] --> Loop 78 
* CEs [627,643,666,682] --> Loop 79 
* CEs [654] --> Loop 80 
* CEs [653] --> Loop 81 
* CEs [673,689] --> Loop 82 
* CEs [633,652,672,688] --> Loop 83 
* CEs [642] --> Loop 84 
* CEs [641] --> Loop 85 
* CEs [665,681] --> Loop 86 
* CEs [626,640,664,680] --> Loop 87 
* CEs [197,201,205,209,212,215,218,221,232,235,238,241,244,247,250,253,257,261,265,269,272,275,278,281,292,295,298,301,304,307,310,313] --> Loop 88 
* CEs [355,357,359,361,375,377,379,381,383,385,387,389,403,405,407,409,423,425,427,429,431,433,435,437] --> Loop 89 
* CEs [196,200,204,208,211,214,217,220,231,234,237,240,243,246,249,252,256,260,264,268,271,274,277,280,291,294,297,300,303,306,309,312] --> Loop 90 
* CEs [341,392,464,475,491,499,507,515,531,539] --> Loop 91 
* CEs [112,119,133,140,147,154,168,175,195,210,230,242,255,270,290,302,339,354,374,382,390,402,422,430,463,474,490,498,506,514,530,538] --> Loop 92 
* CEs [548,550] --> Loop 93 
* CEs [128,130,132,163,165,167] --> Loop 94 
* CEs [561,564] --> Loop 95 
* CEs [558] --> Loop 96 
* CEs [340,344,348,352,363,366,369,372,391,394,397,400,411,414,417,420,551,553,555,559,562,565,567,569,571] --> Loop 97 
* CEs [194,198,202,206,222,224,226,228,254,258,262,266,282,284,286,288,345,349,353,364,367,370,373,395,398,401,412,415,418,421,467,470,473,477,479,481,483,485,487,489,493,495,497,501,503,505,509,511,513,517,519,521,523,525,527,529,533,535,537,541,543,545,546,547,549,552,554,556,557,560,563,566,568,570] --> Loop 98 
* CEs [126,127,129,131,161,162,164,166,223,225,227,229,283,285,287,289,362,365,368,371,410,413,416,419,482,484,486,488,522,524,526,528] --> Loop 99 
* CEs [93,95,97,100,102,104,107,109,111,114,116,118,121,123,125,135,137,139,142,144,146,149,151,153,156,158,160,170,172,174,177,179,181,574,576,578,581,583,585] --> Loop 100 
* CEs [314,316,318,320,322,324,326,328,330,332,334,336,338,342,346,350,438,440,442,444,446,448,450,452,454,456,458,460,462,465,468,471,594,596,598,600,602,604,606,608,610,612,614,616,618,620,622,624] --> Loop 101 
* CEs [91,92,94,96,98,99,101,103,105,106,108,110,113,115,117,120,122,124,134,136,138,141,143,145,148,150,152,155,157,159,169,171,173,176,178,180,182,183,184,185,186,187,188,189,190,191,192,193,199,203,207,213,216,219,233,236,239,245,248,251,259,263,267,273,276,279,293,296,299,305,308,311,315,317,319,321,323,325,327,329,331,333,335,337,343,347,351,356,358,360,376,378,380,384,386,388,393,396,399,404,406,408,424,426,428,432,434,436,439,441,443,445,447,449,451,453,455,457,459,461,466,469,472,476,478,480,492,494,496,500,502,504,508,510,512,516,518,520,532,534,536,540,542,544,572,573,575,577,579,580,582,584,586,587,588,589,590,591,592,593,595,597,599,601,603,605,607,609,611,613,615,617,619,621,623,625] --> Loop 102 

### Ranking functions of CR fun4(V,V2,Out) 
* RF of phase [50,51,52,53,54,55,56,57,58,59,60,61,62,63,64,80,81,82,83]: [V-1]

#### Partial ranking functions of CR fun4(V,V2,Out) 
* Partial RF of phase [50,51,52,53,54,55,56,57,58,59,60,61,62,63,64,80,81,82,83]:
  - RF of loop [50:1,51:1,53:1,54:1,55:1,56:1,58:1,59:1,60:1,61:1,63:1,64:1,80:1,82:1,83:1]:
    V-1
  - RF of loop [52:1,57:1,62:1,81:1]:
    V-2
    2/3*V-5/3
  - RF of loop [60:1]:
    V2 depends on loops [55:1,56:1,57:1,58:1,59:1,80:1,81:1,82:1,83:1] 
  - RF of loop [80:1,81:1,82:1,83:1]:
    -V2+1 depends on loops [50:1,51:1,52:1,53:1,54:1,60:1,61:1,62:1,63:1,64:1] 


### Specialization of cost equations fun6/1 
* CE 51 is refined into CE [696] 
* CE 50 is refined into CE [697] 


### Cost equations --> "Loop" of fun6/1 
* CEs [696] --> Loop 103 
* CEs [697] --> Loop 104 

### Ranking functions of CR fun6(Out) 

#### Partial ranking functions of CR fun6(Out) 


### Specialization of cost equations logIter/3 
* CE 21 is refined into CE [698,699,700,701,702,703,704,705] 
* CE 18 is refined into CE [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] 
* CE 20 is refined into CE [758,759,760] 
* CE 22 is refined into CE [761] 
* CE 19 is refined into CE [762,763,764,765,766,767,768,769] 


### Cost equations --> "Loop" of logIter/3 
* CEs [769] --> Loop 105 
* CEs [768] --> Loop 106 
* CEs [767] --> Loop 107 
* CEs [765] --> Loop 108 
* CEs [764] --> Loop 109 
* CEs [763] --> Loop 110 
* CEs [766] --> Loop 111 
* CEs [762] --> Loop 112 
* CEs [718,722,730,734,738,742,750,754] --> Loop 113 
* CEs [760] --> Loop 114 
* CEs [759] --> Loop 115 
* CEs [726,727,728,729,746,747,748,749,758] --> Loop 116 
* CEs [698,699,700,701,702,703,704,705] --> Loop 117 
* CEs [706,707,708,709,710,711,712,713,714,715,716,717,719,720,721,723,724,725,731,732,733,735,736,737,739,740,741,743,744,745,751,752,753,755,756,757,761] --> Loop 118 

### Ranking functions of CR logIter(V,V2,Out) 
* RF of phase [105,106,107,111]: [V-1]

#### Partial ranking functions of CR logIter(V,V2,Out) 
* Partial RF of phase [105,106,107,111]:
  - RF of loop [105:1,106:1,107:1,111:1]:
    V-1
  - RF of loop [111:1]:
    -V2+1 depends on loops [105:1,107:1] 


### Specialization of cost equations logarithm/2 
* CE 62 is refined into CE [770,771,772,773,774] 
* CE 63 is refined into CE [775] 


### Cost equations --> "Loop" of logarithm/2 
* CEs [773] --> Loop 119 
* CEs [774] --> Loop 120 
* CEs [771,772,775] --> Loop 121 
* CEs [770] --> Loop 122 

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

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


### Specialization of cost equations start/4 
* CE 1 is refined into CE [776] 
* CE 2 is refined into CE [777,778,779,780,781,782,783] 
* CE 3 is refined into CE [784,785,786,787,788,789,790,791,792,793,794,795,796,797,798,799,800,801,802] 
* CE 4 is refined into CE [803] 
* CE 5 is refined into CE [804] 
* CE 6 is refined into CE [805,806,807,808] 
* CE 7 is refined into CE [809,810,811,812] 
* CE 8 is refined into CE [813,814] 
* CE 9 is refined into CE [815,816,817,818,819,820,821,822,823,824,825,826,827,828,829,830] 
* CE 10 is refined into CE [831,832,833,834,835,836,837,838,839,840,841,842,843,844,845,846,847,848,849] 
* CE 11 is refined into CE [850,851] 
* CE 12 is refined into CE [852,853] 
* CE 13 is refined into CE [854,855,856,857,858] 
* CE 14 is refined into CE [859,860,861,862] 
* CE 15 is refined into CE [863,864,865,866] 
* CE 16 is refined into CE [867,868,869,870,871,872,873] 
* CE 17 is refined into CE [874,875,876] 


### Cost equations --> "Loop" of start/4 
* CEs [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] --> Loop 123 

### Ranking functions of CR start(V,V2,V18,V21) 

#### Partial ranking functions of CR start(V,V2,V18,V21) 


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

#### Cost of chains of f(Out):
* Chain [32]: 0
  with precondition: [Out=0] 

* Chain [31]: 0
  with precondition: [Out=1] 

* Chain [30]: 0
  with precondition: [Out=2] 


#### Cost of chains of fun(V,Out):
* Chain [[33],35]: 1*it(33)+1
  Such that:it(33) =< 2*Out

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

* Chain [[33],34]: 1*it(33)+1
  Such that:it(33) =< 2*Out

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

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

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


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

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

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

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

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

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


#### Cost of chains of fun2(V,Out):
* Chain [[39],40]: 1*it(39)+1
  Such that:it(39) =< Out

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

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


#### Cost of chains of half(V,Out):
* Chain [[41],42]: 0
  with precondition: [Out>=1,V>=2*Out] 

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


#### Cost of chains of inc(V,Out):
* Chain [[43],45]: 0
  with precondition: [V+1=Out,V>=1] 

* Chain [[43],44]: 0
  with precondition: [Out>=1,V>=Out] 

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

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


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

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

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

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

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

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


#### Cost of chains of fun4(V,V2,Out):
* Chain [[50,51,52,53,54,55,56,57,58,59,60,61,62,63,64,80,81,82,83],102]: 6*it(50)+3*it(52)+51*it(53)+9*it(57)+1*s(31)+4*s(32)+4*s(33)+1*s(34)+1*s(37)+3
  Such that:aux(1) =< V+V2
aux(39) =< V
aux(40) =< 2*V
aux(41) =< 3*V
aux(42) =< 2/3*V
aux(43) =< V2
it(50) =< aux(39)
it(52) =< aux(39)
it(53) =< aux(39)
it(57) =< aux(39)
it(52) =< aux(40)
it(53) =< aux(40)
it(57) =< aux(40)
s(32) =< aux(40)
it(53) =< aux(41)
it(57) =< aux(41)
s(33) =< aux(41)
it(52) =< aux(42)
it(57) =< aux(42)
aux(7) =< aux(1)
aux(2) =< aux(1)+1
s(31) =< it(50)*aux(1)
s(34) =< it(53)*aux(2)
s(37) =< it(53)+it(53)+it(57)+it(53)+it(53)+it(53)+it(57)+it(53)+it(53)+aux(43)
s(37) =< it(53)*aux(7)

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

* Chain [[50,51,52,53,54,55,56,57,58,59,60,61,62,63,64,80,81,82,83],100]: 6*it(50)+3*it(52)+51*it(53)+9*it(57)+1*s(31)+4*s(32)+4*s(33)+1*s(34)+1*s(37)+39*s(42)+3
  Such that:aux(1) =< V+V2
aux(44) =< V/2+V2
aux(45) =< V
aux(46) =< 2*V
aux(47) =< 3*V
aux(48) =< 2/3*V
aux(49) =< V2
s(42) =< aux(44)
it(50) =< aux(45)
it(52) =< aux(45)
it(53) =< aux(45)
it(57) =< aux(45)
it(52) =< aux(46)
it(53) =< aux(46)
it(57) =< aux(46)
s(32) =< aux(46)
it(53) =< aux(47)
it(57) =< aux(47)
s(33) =< aux(47)
it(52) =< aux(48)
it(57) =< aux(48)
aux(7) =< aux(1)
aux(2) =< aux(1)+1
s(31) =< it(50)*aux(1)
s(34) =< it(53)*aux(2)
s(37) =< it(53)+it(53)+it(57)+it(53)+it(53)+it(53)+it(57)+it(53)+it(53)+aux(49)
s(37) =< it(53)*aux(7)

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

* Chain [[50,51,52,53,54,55,56,57,58,59,60,61,62,63,64,80,81,82,83],99]: 6*it(50)+3*it(52)+51*it(53)+9*it(57)+1*s(31)+4*s(32)+4*s(33)+1*s(34)+1*s(37)+2
  Such that:aux(1) =< V+V2
aux(50) =< V
aux(51) =< 2*V
aux(52) =< 3*V
aux(53) =< 2/3*V
aux(54) =< V2
it(50) =< aux(50)
it(52) =< aux(50)
it(53) =< aux(50)
it(57) =< aux(50)
it(52) =< aux(51)
it(53) =< aux(51)
it(57) =< aux(51)
s(32) =< aux(51)
it(53) =< aux(52)
it(57) =< aux(52)
s(33) =< aux(52)
it(52) =< aux(53)
it(57) =< aux(53)
aux(7) =< aux(1)
aux(2) =< aux(1)+1
s(31) =< it(50)*aux(1)
s(34) =< it(53)*aux(2)
s(37) =< it(53)+it(53)+it(57)+it(53)+it(53)+it(53)+it(57)+it(53)+it(53)+aux(54)
s(37) =< it(53)*aux(7)

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

* Chain [[50,51,52,53,54,55,56,57,58,59,60,61,62,63,64,80,81,82,83],98]: 6*it(50)+3*it(52)+51*it(53)+9*it(57)+1*s(31)+10*s(32)+4*s(33)+1*s(34)+1*s(37)+40*s(84)+3
  Such that:aux(55) =< 1
aux(1) =< V+V2
aux(34) =< 2/3*V
aux(57) =< V
aux(58) =< 2*V
aux(59) =< 3*V
aux(60) =< V2
s(84) =< aux(55)
s(32) =< aux(58)
it(50) =< aux(57)
it(52) =< aux(57)
it(53) =< aux(57)
it(57) =< aux(57)
it(52) =< aux(58)
it(53) =< aux(58)
it(57) =< aux(58)
it(53) =< aux(59)
it(57) =< aux(59)
s(33) =< aux(59)
it(52) =< aux(34)
it(57) =< aux(34)
aux(7) =< aux(1)
aux(2) =< aux(1)+1
s(31) =< it(50)*aux(1)
s(34) =< it(53)*aux(2)
s(37) =< it(53)+it(53)+it(57)+it(53)+it(53)+it(53)+it(57)+it(53)+it(53)+aux(60)
s(37) =< it(53)*aux(7)

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

* Chain [[50,51,52,53,54,55,56,57,58,59,60,61,62,63,64,80,81,82,83],97]: 6*it(50)+3*it(52)+51*it(53)+9*it(57)+1*s(31)+4*s(32)+4*s(33)+1*s(34)+1*s(37)+41
  Such that:aux(1) =< V+V2
aux(63) =< V
aux(64) =< 2*V
aux(65) =< 3*V
aux(66) =< 2/3*V
aux(67) =< V2
it(50) =< aux(63)
it(52) =< aux(63)
it(53) =< aux(63)
it(57) =< aux(63)
it(52) =< aux(64)
it(53) =< aux(64)
it(57) =< aux(64)
s(32) =< aux(64)
it(53) =< aux(65)
it(57) =< aux(65)
s(33) =< aux(65)
it(52) =< aux(66)
it(57) =< aux(66)
aux(7) =< aux(1)
aux(2) =< aux(1)+1
s(31) =< it(50)*aux(1)
s(34) =< it(53)*aux(2)
s(37) =< it(53)+it(53)+it(57)+it(53)+it(53)+it(53)+it(57)+it(53)+it(53)+aux(67)
s(37) =< it(53)*aux(7)

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

* Chain [[50,51,52,53,54,55,56,57,58,59,60,61,62,63,64,80,81,82,83],96]: 6*it(50)+3*it(52)+51*it(53)+9*it(57)+1*s(31)+4*s(32)+4*s(33)+1*s(34)+1*s(37)+1*s(149)+3
  Such that:s(149) =< 2
aux(1) =< V+V2
aux(68) =< V
aux(69) =< 2*V
aux(70) =< 3*V
aux(71) =< 2/3*V
aux(72) =< V2
it(50) =< aux(68)
it(52) =< aux(68)
it(53) =< aux(68)
it(57) =< aux(68)
it(52) =< aux(69)
it(53) =< aux(69)
it(57) =< aux(69)
s(32) =< aux(69)
it(53) =< aux(70)
it(57) =< aux(70)
s(33) =< aux(70)
it(52) =< aux(71)
it(57) =< aux(71)
aux(7) =< aux(1)
aux(2) =< aux(1)+1
s(31) =< it(50)*aux(1)
s(34) =< it(53)*aux(2)
s(37) =< it(53)+it(53)+it(57)+it(53)+it(53)+it(53)+it(57)+it(53)+it(53)+aux(72)
s(37) =< it(53)*aux(7)

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

* Chain [[50,51,52,53,54,55,56,57,58,59,60,61,62,63,64,80,81,82,83],95]: 6*it(50)+3*it(52)+51*it(53)+9*it(57)+1*s(31)+4*s(32)+4*s(33)+1*s(34)+1*s(37)+7
  Such that:aux(1) =< V+V2
aux(74) =< V
aux(75) =< 2*V
aux(76) =< 3*V
aux(77) =< 2/3*V
aux(78) =< V2
it(50) =< aux(74)
it(52) =< aux(74)
it(53) =< aux(74)
it(57) =< aux(74)
it(52) =< aux(75)
it(53) =< aux(75)
it(57) =< aux(75)
s(32) =< aux(75)
it(53) =< aux(76)
it(57) =< aux(76)
s(33) =< aux(76)
it(52) =< aux(77)
it(57) =< aux(77)
aux(7) =< aux(1)
aux(2) =< aux(1)+1
s(31) =< it(50)*aux(1)
s(34) =< it(53)*aux(2)
s(37) =< it(53)+it(53)+it(57)+it(53)+it(53)+it(53)+it(57)+it(53)+it(53)+aux(78)
s(37) =< it(53)*aux(7)

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

* Chain [[50,51,52,53,54,55,56,57,58,59,60,61,62,63,64,80,81,82,83],94]: 6*it(50)+3*it(52)+51*it(53)+9*it(57)+1*s(31)+4*s(32)+4*s(33)+1*s(34)+1*s(37)+6*s(152)+2
  Such that:aux(1) =< V+V2
aux(79) =< V/2+V2
aux(80) =< V
aux(81) =< 2*V
aux(82) =< 3*V
aux(83) =< 2/3*V
aux(84) =< V2
s(152) =< aux(79)
it(50) =< aux(80)
it(52) =< aux(80)
it(53) =< aux(80)
it(57) =< aux(80)
it(52) =< aux(81)
it(53) =< aux(81)
it(57) =< aux(81)
s(32) =< aux(81)
it(53) =< aux(82)
it(57) =< aux(82)
s(33) =< aux(82)
it(52) =< aux(83)
it(57) =< aux(83)
aux(7) =< aux(1)
aux(2) =< aux(1)+1
s(31) =< it(50)*aux(1)
s(34) =< it(53)*aux(2)
s(37) =< it(53)+it(53)+it(57)+it(53)+it(53)+it(53)+it(57)+it(53)+it(53)+aux(84)
s(37) =< it(53)*aux(7)

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

* Chain [[50,51,52,53,54,55,56,57,58,59,60,61,62,63,64,80,81,82,83],93]: 6*it(50)+3*it(52)+51*it(53)+9*it(57)+1*s(31)+4*s(32)+4*s(33)+1*s(34)+1*s(37)+2*s(158)+3
  Such that:aux(1) =< V+V2
aux(85) =< V/2+V2
aux(86) =< V
aux(87) =< 2*V
aux(88) =< 3*V
aux(89) =< 2/3*V
aux(90) =< V2
s(158) =< aux(85)
it(50) =< aux(86)
it(52) =< aux(86)
it(53) =< aux(86)
it(57) =< aux(86)
it(52) =< aux(87)
it(53) =< aux(87)
it(57) =< aux(87)
s(32) =< aux(87)
it(53) =< aux(88)
it(57) =< aux(88)
s(33) =< aux(88)
it(52) =< aux(89)
it(57) =< aux(89)
aux(7) =< aux(1)
aux(2) =< aux(1)+1
s(31) =< it(50)*aux(1)
s(34) =< it(53)*aux(2)
s(37) =< it(53)+it(53)+it(57)+it(53)+it(53)+it(53)+it(57)+it(53)+it(53)+aux(90)
s(37) =< it(53)*aux(7)

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

* Chain [[50,51,52,53,54,55,56,57,58,59,60,61,62,63,64,80,81,82,83],92]: 6*it(50)+3*it(52)+51*it(53)+9*it(57)+1*s(31)+4*s(32)+4*s(33)+1*s(34)+1*s(37)+2
  Such that:aux(1) =< V+V2
aux(91) =< V
aux(92) =< 2*V
aux(93) =< 3*V
aux(94) =< 2/3*V
aux(95) =< V2
it(50) =< aux(91)
it(52) =< aux(91)
it(53) =< aux(91)
it(57) =< aux(91)
it(52) =< aux(92)
it(53) =< aux(92)
it(57) =< aux(92)
s(32) =< aux(92)
it(53) =< aux(93)
it(57) =< aux(93)
s(33) =< aux(93)
it(52) =< aux(94)
it(57) =< aux(94)
aux(7) =< aux(1)
aux(2) =< aux(1)+1
s(31) =< it(50)*aux(1)
s(34) =< it(53)*aux(2)
s(37) =< it(53)+it(53)+it(57)+it(53)+it(53)+it(53)+it(57)+it(53)+it(53)+aux(95)
s(37) =< it(53)*aux(7)

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

* Chain [[50,51,52,53,54,55,56,57,58,59,60,61,62,63,64,80,81,82,83],91]: 6*it(50)+3*it(52)+51*it(53)+9*it(57)+1*s(31)+4*s(32)+4*s(33)+1*s(34)+1*s(37)+14
  Such that:aux(1) =< V+V2
aux(98) =< V
aux(99) =< 2*V
aux(100) =< 3*V
aux(101) =< 2/3*V
aux(102) =< V2
it(50) =< aux(98)
it(52) =< aux(98)
it(53) =< aux(98)
it(57) =< aux(98)
it(52) =< aux(99)
it(53) =< aux(99)
it(57) =< aux(99)
s(32) =< aux(99)
it(53) =< aux(100)
it(57) =< aux(100)
s(33) =< aux(100)
it(52) =< aux(101)
it(57) =< aux(101)
aux(7) =< aux(1)
aux(2) =< aux(1)+1
s(31) =< it(50)*aux(1)
s(34) =< it(53)*aux(2)
s(37) =< it(53)+it(53)+it(57)+it(53)+it(53)+it(53)+it(57)+it(53)+it(53)+aux(102)
s(37) =< it(53)*aux(7)

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

* Chain [[50,51,52,53,54,55,56,57,58,59,60,61,62,63,64,80,81,82,83],90]: 6*it(50)+3*it(52)+51*it(53)+9*it(57)+1*s(31)+4*s(32)+4*s(33)+1*s(34)+1*s(37)+32*s(170)+2
  Such that:aux(28) =< V
aux(29) =< V+1
aux(1) =< V+V2
aux(30) =< 2*V
aux(32) =< 3*V
aux(33) =< 3*V+3
aux(34) =< 2/3*V
aux(104) =< 2*V+2
aux(105) =< V2
s(170) =< aux(104)
it(50) =< aux(28)
it(52) =< aux(28)
it(53) =< aux(28)
it(57) =< aux(28)
it(50) =< aux(29)
it(52) =< aux(29)
it(53) =< aux(29)
it(57) =< aux(29)
it(52) =< aux(30)
it(53) =< aux(30)
it(57) =< aux(30)
s(32) =< aux(30)
it(52) =< aux(104)
it(53) =< aux(104)
it(57) =< aux(104)
s(32) =< aux(104)
it(53) =< aux(32)
it(57) =< aux(32)
s(33) =< aux(32)
it(53) =< aux(33)
it(57) =< aux(33)
s(33) =< aux(33)
it(52) =< aux(34)
it(57) =< aux(34)
aux(7) =< aux(1)
aux(2) =< aux(1)+1
s(31) =< it(50)*aux(1)
s(34) =< it(53)*aux(2)
s(37) =< it(53)+it(53)+it(57)+it(53)+it(53)+it(53)+it(57)+it(53)+it(53)+aux(105)
s(37) =< it(53)*aux(7)

  with precondition: [V>=6,V2>=0,Out>=5] 

* Chain [[50,51,52,53,54,55,56,57,58,59,60,61,62,63,64,80,81,82,83],89]: 6*it(50)+3*it(52)+51*it(53)+9*it(57)+1*s(31)+4*s(32)+4*s(33)+1*s(34)+1*s(37)+50
  Such that:aux(1) =< V+V2
aux(107) =< V
aux(108) =< 2*V
aux(109) =< 3*V
aux(110) =< 2/3*V
aux(111) =< V2
it(50) =< aux(107)
it(52) =< aux(107)
it(53) =< aux(107)
it(57) =< aux(107)
it(52) =< aux(108)
it(53) =< aux(108)
it(57) =< aux(108)
s(32) =< aux(108)
it(53) =< aux(109)
it(57) =< aux(109)
s(33) =< aux(109)
it(52) =< aux(110)
it(57) =< aux(110)
aux(7) =< aux(1)
aux(2) =< aux(1)+1
s(31) =< it(50)*aux(1)
s(34) =< it(53)*aux(2)
s(37) =< it(53)+it(53)+it(57)+it(53)+it(53)+it(53)+it(57)+it(53)+it(53)+aux(111)
s(37) =< it(53)*aux(7)

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

* Chain [[50,51,52,53,54,55,56,57,58,59,60,61,62,63,64,80,81,82,83],88]: 6*it(50)+3*it(52)+51*it(53)+9*it(57)+1*s(31)+36*s(32)+4*s(33)+1*s(34)+1*s(37)+2
  Such that:aux(1) =< V+V2
aux(34) =< 2/3*V
aux(113) =< V
aux(114) =< 2*V
aux(115) =< 3*V
aux(116) =< V2
s(32) =< aux(114)
it(50) =< aux(113)
it(52) =< aux(113)
it(53) =< aux(113)
it(57) =< aux(113)
it(52) =< aux(114)
it(53) =< aux(114)
it(57) =< aux(114)
it(53) =< aux(115)
it(57) =< aux(115)
s(33) =< aux(115)
it(52) =< aux(34)
it(57) =< aux(34)
aux(7) =< aux(1)
aux(2) =< aux(1)+1
s(31) =< it(50)*aux(1)
s(34) =< it(53)*aux(2)
s(37) =< it(53)+it(53)+it(57)+it(53)+it(53)+it(53)+it(57)+it(53)+it(53)+aux(116)
s(37) =< it(53)*aux(7)

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

* Chain [[50,51,52,53,54,55,56,57,58,59,60,61,62,63,64,80,81,82,83],87,102]: 6*it(50)+3*it(52)+51*it(53)+9*it(57)+1*s(31)+4*s(32)+4*s(33)+1*s(34)+1*s(37)+6
  Such that:aux(1) =< V+V2
aux(117) =< V
aux(118) =< 2*V
aux(119) =< 3*V
aux(120) =< 2/3*V
aux(121) =< V2
it(50) =< aux(117)
it(52) =< aux(117)
it(53) =< aux(117)
it(57) =< aux(117)
it(52) =< aux(118)
it(53) =< aux(118)
it(57) =< aux(118)
s(32) =< aux(118)
it(53) =< aux(119)
it(57) =< aux(119)
s(33) =< aux(119)
it(52) =< aux(120)
it(57) =< aux(120)
aux(7) =< aux(1)
aux(2) =< aux(1)+1
s(31) =< it(50)*aux(1)
s(34) =< it(53)*aux(2)
s(37) =< it(53)+it(53)+it(57)+it(53)+it(53)+it(53)+it(57)+it(53)+it(53)+aux(121)
s(37) =< it(53)*aux(7)

  with precondition: [V>=4,V2>=0,Out>=5] 

* Chain [[50,51,52,53,54,55,56,57,58,59,60,61,62,63,64,80,81,82,83],87,101]: 6*it(50)+3*it(52)+51*it(53)+9*it(57)+1*s(31)+4*s(32)+4*s(33)+1*s(34)+1*s(37)+6
  Such that:aux(1) =< V+V2
aux(122) =< V
aux(123) =< 2*V
aux(124) =< 3*V
aux(125) =< 2/3*V
aux(126) =< V2
it(50) =< aux(122)
it(52) =< aux(122)
it(53) =< aux(122)
it(57) =< aux(122)
it(52) =< aux(123)
it(53) =< aux(123)
it(57) =< aux(123)
s(32) =< aux(123)
it(53) =< aux(124)
it(57) =< aux(124)
s(33) =< aux(124)
it(52) =< aux(125)
it(57) =< aux(125)
aux(7) =< aux(1)
aux(2) =< aux(1)+1
s(31) =< it(50)*aux(1)
s(34) =< it(53)*aux(2)
s(37) =< it(53)+it(53)+it(57)+it(53)+it(53)+it(53)+it(57)+it(53)+it(53)+aux(126)
s(37) =< it(53)*aux(7)

  with precondition: [V>=4,V2>=0,Out>=6] 

* Chain [[50,51,52,53,54,55,56,57,58,59,60,61,62,63,64,80,81,82,83],87,100]: 6*it(50)+3*it(52)+51*it(53)+9*it(57)+1*s(31)+4*s(32)+4*s(33)+1*s(34)+1*s(37)+39*s(42)+6
  Such that:aux(44) =< 1
aux(1) =< V+V2
aux(127) =< V
aux(128) =< 2*V
aux(129) =< 3*V
aux(130) =< 2/3*V
aux(131) =< V2
s(42) =< aux(44)
it(50) =< aux(127)
it(52) =< aux(127)
it(53) =< aux(127)
it(57) =< aux(127)
it(52) =< aux(128)
it(53) =< aux(128)
it(57) =< aux(128)
s(32) =< aux(128)
it(53) =< aux(129)
it(57) =< aux(129)
s(33) =< aux(129)
it(52) =< aux(130)
it(57) =< aux(130)
aux(7) =< aux(1)
aux(2) =< aux(1)+1
s(31) =< it(50)*aux(1)
s(34) =< it(53)*aux(2)
s(37) =< it(53)+it(53)+it(57)+it(53)+it(53)+it(53)+it(57)+it(53)+it(53)+aux(131)
s(37) =< it(53)*aux(7)

  with precondition: [V>=4,V2>=0,Out>=6] 

* Chain [[50,51,52,53,54,55,56,57,58,59,60,61,62,63,64,80,81,82,83],86,102]: 6*it(50)+3*it(52)+51*it(53)+9*it(57)+1*s(31)+4*s(32)+4*s(33)+1*s(34)+1*s(37)+9
  Such that:aux(1) =< V+V2
aux(132) =< V
aux(133) =< 2*V
aux(134) =< 3*V
aux(135) =< 2/3*V
aux(136) =< V2
it(50) =< aux(132)
it(52) =< aux(132)
it(53) =< aux(132)
it(57) =< aux(132)
it(52) =< aux(133)
it(53) =< aux(133)
it(57) =< aux(133)
s(32) =< aux(133)
it(53) =< aux(134)
it(57) =< aux(134)
s(33) =< aux(134)
it(52) =< aux(135)
it(57) =< aux(135)
aux(7) =< aux(1)
aux(2) =< aux(1)+1
s(31) =< it(50)*aux(1)
s(34) =< it(53)*aux(2)
s(37) =< it(53)+it(53)+it(57)+it(53)+it(53)+it(53)+it(57)+it(53)+it(53)+aux(136)
s(37) =< it(53)*aux(7)

  with precondition: [V>=4,V2>=0,Out>=6] 

* Chain [[50,51,52,53,54,55,56,57,58,59,60,61,62,63,64,80,81,82,83],86,101]: 6*it(50)+3*it(52)+51*it(53)+9*it(57)+1*s(31)+4*s(32)+4*s(33)+1*s(34)+1*s(37)+9
  Such that:aux(1) =< V+V2
aux(137) =< V
aux(138) =< 2*V
aux(139) =< 3*V
aux(140) =< 2/3*V
aux(141) =< V2
it(50) =< aux(137)
it(52) =< aux(137)
it(53) =< aux(137)
it(57) =< aux(137)
it(52) =< aux(138)
it(53) =< aux(138)
it(57) =< aux(138)
s(32) =< aux(138)
it(53) =< aux(139)
it(57) =< aux(139)
s(33) =< aux(139)
it(52) =< aux(140)
it(57) =< aux(140)
aux(7) =< aux(1)
aux(2) =< aux(1)+1
s(31) =< it(50)*aux(1)
s(34) =< it(53)*aux(2)
s(37) =< it(53)+it(53)+it(57)+it(53)+it(53)+it(53)+it(57)+it(53)+it(53)+aux(141)
s(37) =< it(53)*aux(7)

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

* Chain [[50,51,52,53,54,55,56,57,58,59,60,61,62,63,64,80,81,82,83],86,100]: 6*it(50)+3*it(52)+51*it(53)+9*it(57)+1*s(31)+4*s(32)+4*s(33)+1*s(34)+1*s(37)+39*s(42)+9
  Such that:aux(44) =< 1
aux(1) =< V+V2
aux(142) =< V
aux(143) =< 2*V
aux(144) =< 3*V
aux(145) =< 2/3*V
aux(146) =< V2
s(42) =< aux(44)
it(50) =< aux(142)
it(52) =< aux(142)
it(53) =< aux(142)
it(57) =< aux(142)
it(52) =< aux(143)
it(53) =< aux(143)
it(57) =< aux(143)
s(32) =< aux(143)
it(53) =< aux(144)
it(57) =< aux(144)
s(33) =< aux(144)
it(52) =< aux(145)
it(57) =< aux(145)
aux(7) =< aux(1)
aux(2) =< aux(1)+1
s(31) =< it(50)*aux(1)
s(34) =< it(53)*aux(2)
s(37) =< it(53)+it(53)+it(57)+it(53)+it(53)+it(53)+it(57)+it(53)+it(53)+aux(146)
s(37) =< it(53)*aux(7)

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

* Chain [[50,51,52,53,54,55,56,57,58,59,60,61,62,63,64,80,81,82,83],85,102]: 6*it(50)+3*it(52)+51*it(53)+9*it(57)+1*s(31)+4*s(32)+4*s(33)+1*s(34)+1*s(37)+1*s(260)+6
  Such that:aux(28) =< V
aux(29) =< V+7
aux(1) =< V+V2
aux(30) =< 2*V
aux(32) =< 3*V
aux(34) =< 2/3*V
aux(147) =< 2*V+14
aux(148) =< 3*V+21
aux(149) =< V2
s(260) =< aux(148)
it(50) =< aux(28)
it(52) =< aux(28)
it(53) =< aux(28)
it(57) =< aux(28)
it(50) =< aux(29)
it(52) =< aux(29)
it(53) =< aux(29)
it(57) =< aux(29)
it(52) =< aux(30)
it(53) =< aux(30)
it(57) =< aux(30)
s(32) =< aux(30)
it(52) =< aux(147)
it(53) =< aux(147)
it(57) =< aux(147)
s(32) =< aux(147)
it(53) =< aux(32)
it(57) =< aux(32)
s(33) =< aux(32)
it(53) =< aux(148)
it(57) =< aux(148)
s(33) =< aux(148)
it(52) =< aux(34)
it(57) =< aux(34)
aux(7) =< aux(1)
aux(2) =< aux(1)+1
s(31) =< it(50)*aux(1)
s(34) =< it(53)*aux(2)
s(37) =< it(53)+it(53)+it(57)+it(53)+it(53)+it(53)+it(57)+it(53)+it(53)+aux(149)
s(37) =< it(53)*aux(7)

  with precondition: [V>=6,V2>=0,Out>=7] 

* Chain [[50,51,52,53,54,55,56,57,58,59,60,61,62,63,64,80,81,82,83],85,101]: 6*it(50)+3*it(52)+51*it(53)+9*it(57)+1*s(31)+4*s(32)+4*s(33)+1*s(34)+1*s(37)+1*s(260)+6
  Such that:aux(28) =< V
aux(29) =< V+9
aux(1) =< V+V2
aux(30) =< 2*V
aux(32) =< 3*V
aux(34) =< 2/3*V
aux(150) =< 2*V+18
aux(151) =< 3*V+27
aux(152) =< V2
s(260) =< aux(151)
it(50) =< aux(28)
it(52) =< aux(28)
it(53) =< aux(28)
it(57) =< aux(28)
it(50) =< aux(29)
it(52) =< aux(29)
it(53) =< aux(29)
it(57) =< aux(29)
it(52) =< aux(30)
it(53) =< aux(30)
it(57) =< aux(30)
s(32) =< aux(30)
it(52) =< aux(150)
it(53) =< aux(150)
it(57) =< aux(150)
s(32) =< aux(150)
it(53) =< aux(32)
it(57) =< aux(32)
s(33) =< aux(32)
it(53) =< aux(151)
it(57) =< aux(151)
s(33) =< aux(151)
it(52) =< aux(34)
it(57) =< aux(34)
aux(7) =< aux(1)
aux(2) =< aux(1)+1
s(31) =< it(50)*aux(1)
s(34) =< it(53)*aux(2)
s(37) =< it(53)+it(53)+it(57)+it(53)+it(53)+it(53)+it(57)+it(53)+it(53)+aux(152)
s(37) =< it(53)*aux(7)

  with precondition: [V>=6,V2>=0,Out>=8] 

* Chain [[50,51,52,53,54,55,56,57,58,59,60,61,62,63,64,80,81,82,83],85,100]: 6*it(50)+3*it(52)+51*it(53)+9*it(57)+1*s(31)+4*s(32)+4*s(33)+1*s(34)+1*s(37)+39*s(42)+1*s(260)+6
  Such that:aux(44) =< 1
aux(28) =< V
aux(29) =< V+9
aux(1) =< V+V2
aux(30) =< 2*V
aux(32) =< 3*V
aux(34) =< 2/3*V
aux(153) =< 2*V+18
aux(154) =< 3*V+27
aux(155) =< V2
s(260) =< aux(154)
s(42) =< aux(44)
it(50) =< aux(28)
it(52) =< aux(28)
it(53) =< aux(28)
it(57) =< aux(28)
it(50) =< aux(29)
it(52) =< aux(29)
it(53) =< aux(29)
it(57) =< aux(29)
it(52) =< aux(30)
it(53) =< aux(30)
it(57) =< aux(30)
s(32) =< aux(30)
it(52) =< aux(153)
it(53) =< aux(153)
it(57) =< aux(153)
s(32) =< aux(153)
it(53) =< aux(32)
it(57) =< aux(32)
s(33) =< aux(32)
it(53) =< aux(154)
it(57) =< aux(154)
s(33) =< aux(154)
it(52) =< aux(34)
it(57) =< aux(34)
aux(7) =< aux(1)
aux(2) =< aux(1)+1
s(31) =< it(50)*aux(1)
s(34) =< it(53)*aux(2)
s(37) =< it(53)+it(53)+it(57)+it(53)+it(53)+it(53)+it(57)+it(53)+it(53)+aux(155)
s(37) =< it(53)*aux(7)

  with precondition: [V>=6,V2>=0,Out>=8] 

* Chain [[50,51,52,53,54,55,56,57,58,59,60,61,62,63,64,80,81,82,83],84,102]: 6*it(50)+3*it(52)+51*it(53)+9*it(57)+1*s(31)+4*s(32)+5*s(33)+1*s(34)+1*s(37)+6
  Such that:aux(1) =< V+V2
aux(34) =< 2/3*V
aux(156) =< V
aux(157) =< 2*V
aux(158) =< 3*V
aux(159) =< V2
s(33) =< aux(158)
it(50) =< aux(156)
it(52) =< aux(156)
it(53) =< aux(156)
it(57) =< aux(156)
it(52) =< aux(157)
it(53) =< aux(157)
it(57) =< aux(157)
s(32) =< aux(157)
it(53) =< aux(158)
it(57) =< aux(158)
it(52) =< aux(34)
it(57) =< aux(34)
aux(7) =< aux(1)
aux(2) =< aux(1)+1
s(31) =< it(50)*aux(1)
s(34) =< it(53)*aux(2)
s(37) =< it(53)+it(53)+it(57)+it(53)+it(53)+it(53)+it(57)+it(53)+it(53)+aux(159)
s(37) =< it(53)*aux(7)

  with precondition: [V>=4,V2>=0,Out>=6] 

* Chain [[50,51,52,53,54,55,56,57,58,59,60,61,62,63,64,80,81,82,83],84,101]: 6*it(50)+3*it(52)+51*it(53)+9*it(57)+1*s(31)+4*s(32)+5*s(33)+1*s(34)+1*s(37)+6
  Such that:aux(1) =< V+V2
aux(34) =< 2/3*V
aux(160) =< V
aux(161) =< 2*V
aux(162) =< 3*V
aux(163) =< V2
s(33) =< aux(162)
it(50) =< aux(160)
it(52) =< aux(160)
it(53) =< aux(160)
it(57) =< aux(160)
it(52) =< aux(161)
it(53) =< aux(161)
it(57) =< aux(161)
s(32) =< aux(161)
it(53) =< aux(162)
it(57) =< aux(162)
it(52) =< aux(34)
it(57) =< aux(34)
aux(7) =< aux(1)
aux(2) =< aux(1)+1
s(31) =< it(50)*aux(1)
s(34) =< it(53)*aux(2)
s(37) =< it(53)+it(53)+it(57)+it(53)+it(53)+it(53)+it(57)+it(53)+it(53)+aux(163)
s(37) =< it(53)*aux(7)

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

* Chain [[50,51,52,53,54,55,56,57,58,59,60,61,62,63,64,80,81,82,83],84,100]: 6*it(50)+3*it(52)+51*it(53)+9*it(57)+1*s(31)+4*s(32)+5*s(33)+1*s(34)+1*s(37)+39*s(42)+6
  Such that:aux(44) =< 1
aux(1) =< V+V2
aux(34) =< 2/3*V
aux(164) =< V
aux(165) =< 2*V
aux(166) =< 3*V
aux(167) =< V2
s(33) =< aux(166)
s(42) =< aux(44)
it(50) =< aux(164)
it(52) =< aux(164)
it(53) =< aux(164)
it(57) =< aux(164)
it(52) =< aux(165)
it(53) =< aux(165)
it(57) =< aux(165)
s(32) =< aux(165)
it(53) =< aux(166)
it(57) =< aux(166)
it(52) =< aux(34)
it(57) =< aux(34)
aux(7) =< aux(1)
aux(2) =< aux(1)+1
s(31) =< it(50)*aux(1)
s(34) =< it(53)*aux(2)
s(37) =< it(53)+it(53)+it(57)+it(53)+it(53)+it(53)+it(57)+it(53)+it(53)+aux(167)
s(37) =< it(53)*aux(7)

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

* Chain [[50,51,52,53,54,55,56,57,58,59,60,61,62,63,64,80,81,82,83],79,102]: 6*it(50)+3*it(52)+51*it(53)+9*it(57)+1*s(31)+4*s(32)+4*s(33)+1*s(34)+1*s(37)+6
  Such that:aux(1) =< V+V2
aux(168) =< V
aux(169) =< 2*V
aux(170) =< 3*V
aux(171) =< 2/3*V
aux(172) =< V2
it(50) =< aux(168)
it(52) =< aux(168)
it(53) =< aux(168)
it(57) =< aux(168)
it(52) =< aux(169)
it(53) =< aux(169)
it(57) =< aux(169)
s(32) =< aux(169)
it(53) =< aux(170)
it(57) =< aux(170)
s(33) =< aux(170)
it(52) =< aux(171)
it(57) =< aux(171)
aux(7) =< aux(1)
aux(2) =< aux(1)+1
s(31) =< it(50)*aux(1)
s(34) =< it(53)*aux(2)
s(37) =< it(53)+it(53)+it(57)+it(53)+it(53)+it(53)+it(57)+it(53)+it(53)+aux(172)
s(37) =< it(53)*aux(7)

  with precondition: [V>=4,V2>=0,Out>=5] 

* Chain [[50,51,52,53,54,55,56,57,58,59,60,61,62,63,64,80,81,82,83],79,101]: 6*it(50)+3*it(52)+51*it(53)+9*it(57)+1*s(31)+4*s(32)+4*s(33)+1*s(34)+1*s(37)+6
  Such that:aux(1) =< V+V2
aux(173) =< V
aux(174) =< 2*V
aux(175) =< 3*V
aux(176) =< 2/3*V
aux(177) =< V2
it(50) =< aux(173)
it(52) =< aux(173)
it(53) =< aux(173)
it(57) =< aux(173)
it(52) =< aux(174)
it(53) =< aux(174)
it(57) =< aux(174)
s(32) =< aux(174)
it(53) =< aux(175)
it(57) =< aux(175)
s(33) =< aux(175)
it(52) =< aux(176)
it(57) =< aux(176)
aux(7) =< aux(1)
aux(2) =< aux(1)+1
s(31) =< it(50)*aux(1)
s(34) =< it(53)*aux(2)
s(37) =< it(53)+it(53)+it(57)+it(53)+it(53)+it(53)+it(57)+it(53)+it(53)+aux(177)
s(37) =< it(53)*aux(7)

  with precondition: [V>=4,V2>=0,Out>=6] 

* Chain [[50,51,52,53,54,55,56,57,58,59,60,61,62,63,64,80,81,82,83],79,92]: 6*it(50)+3*it(52)+51*it(53)+9*it(57)+1*s(31)+4*s(32)+4*s(33)+1*s(34)+1*s(37)+5
  Such that:aux(1) =< V+V2
aux(178) =< V
aux(179) =< 2*V
aux(180) =< 3*V
aux(181) =< 2/3*V
aux(182) =< V2
it(50) =< aux(178)
it(52) =< aux(178)
it(53) =< aux(178)
it(57) =< aux(178)
it(52) =< aux(179)
it(53) =< aux(179)
it(57) =< aux(179)
s(32) =< aux(179)
it(53) =< aux(180)
it(57) =< aux(180)
s(33) =< aux(180)
it(52) =< aux(181)
it(57) =< aux(181)
aux(7) =< aux(1)
aux(2) =< aux(1)+1
s(31) =< it(50)*aux(1)
s(34) =< it(53)*aux(2)
s(37) =< it(53)+it(53)+it(57)+it(53)+it(53)+it(53)+it(57)+it(53)+it(53)+aux(182)
s(37) =< it(53)*aux(7)

  with precondition: [V>=4,V2>=0,Out>=5] 

* Chain [[50,51,52,53,54,55,56,57,58,59,60,61,62,63,64,80,81,82,83],78,102]: 6*it(50)+3*it(52)+51*it(53)+9*it(57)+1*s(31)+4*s(32)+4*s(33)+1*s(34)+1*s(37)+9
  Such that:aux(1) =< V+V2
aux(183) =< V
aux(184) =< 2*V
aux(185) =< 3*V
aux(186) =< 2/3*V
aux(187) =< V2
it(50) =< aux(183)
it(52) =< aux(183)
it(53) =< aux(183)
it(57) =< aux(183)
it(52) =< aux(184)
it(53) =< aux(184)
it(57) =< aux(184)
s(32) =< aux(184)
it(53) =< aux(185)
it(57) =< aux(185)
s(33) =< aux(185)
it(52) =< aux(186)
it(57) =< aux(186)
aux(7) =< aux(1)
aux(2) =< aux(1)+1
s(31) =< it(50)*aux(1)
s(34) =< it(53)*aux(2)
s(37) =< it(53)+it(53)+it(57)+it(53)+it(53)+it(53)+it(57)+it(53)+it(53)+aux(187)
s(37) =< it(53)*aux(7)

  with precondition: [V>=4,V2>=0,Out>=6] 

* Chain [[50,51,52,53,54,55,56,57,58,59,60,61,62,63,64,80,81,82,83],78,101]: 6*it(50)+3*it(52)+51*it(53)+9*it(57)+1*s(31)+4*s(32)+4*s(33)+1*s(34)+1*s(37)+9
  Such that:aux(1) =< V+V2
aux(188) =< V
aux(189) =< 2*V
aux(190) =< 3*V
aux(191) =< 2/3*V
aux(192) =< V2
it(50) =< aux(188)
it(52) =< aux(188)
it(53) =< aux(188)
it(57) =< aux(188)
it(52) =< aux(189)
it(53) =< aux(189)
it(57) =< aux(189)
s(32) =< aux(189)
it(53) =< aux(190)
it(57) =< aux(190)
s(33) =< aux(190)
it(52) =< aux(191)
it(57) =< aux(191)
aux(7) =< aux(1)
aux(2) =< aux(1)+1
s(31) =< it(50)*aux(1)
s(34) =< it(53)*aux(2)
s(37) =< it(53)+it(53)+it(57)+it(53)+it(53)+it(53)+it(57)+it(53)+it(53)+aux(192)
s(37) =< it(53)*aux(7)

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

* Chain [[50,51,52,53,54,55,56,57,58,59,60,61,62,63,64,80,81,82,83],78,92]: 6*it(50)+3*it(52)+51*it(53)+9*it(57)+1*s(31)+4*s(32)+4*s(33)+1*s(34)+1*s(37)+8
  Such that:aux(1) =< V+V2
aux(193) =< V
aux(194) =< 2*V
aux(195) =< 3*V
aux(196) =< 2/3*V
aux(197) =< V2
it(50) =< aux(193)
it(52) =< aux(193)
it(53) =< aux(193)
it(57) =< aux(193)
it(52) =< aux(194)
it(53) =< aux(194)
it(57) =< aux(194)
s(32) =< aux(194)
it(53) =< aux(195)
it(57) =< aux(195)
s(33) =< aux(195)
it(52) =< aux(196)
it(57) =< aux(196)
aux(7) =< aux(1)
aux(2) =< aux(1)+1
s(31) =< it(50)*aux(1)
s(34) =< it(53)*aux(2)
s(37) =< it(53)+it(53)+it(57)+it(53)+it(53)+it(53)+it(57)+it(53)+it(53)+aux(197)
s(37) =< it(53)*aux(7)

  with precondition: [V>=4,V2>=0,Out>=6] 

* Chain [[50,51,52,53,54,55,56,57,58,59,60,61,62,63,64,80,81,82,83],77,102]: 6*it(50)+3*it(52)+51*it(53)+9*it(57)+1*s(31)+4*s(32)+4*s(33)+1*s(34)+1*s(37)+1*s(264)+6
  Such that:aux(28) =< V
aux(29) =< V+7
aux(1) =< V+V2
aux(30) =< 2*V
aux(32) =< 3*V
aux(33) =< 3*V+21
aux(34) =< 2/3*V
aux(198) =< 2*V+14
aux(199) =< V2
s(264) =< aux(198)
it(50) =< aux(28)
it(52) =< aux(28)
it(53) =< aux(28)
it(57) =< aux(28)
it(50) =< aux(29)
it(52) =< aux(29)
it(53) =< aux(29)
it(57) =< aux(29)
it(52) =< aux(30)
it(53) =< aux(30)
it(57) =< aux(30)
s(32) =< aux(30)
it(52) =< aux(198)
it(53) =< aux(198)
it(57) =< aux(198)
s(32) =< aux(198)
it(53) =< aux(32)
it(57) =< aux(32)
s(33) =< aux(32)
it(53) =< aux(33)
it(57) =< aux(33)
s(33) =< aux(33)
it(52) =< aux(34)
it(57) =< aux(34)
aux(7) =< aux(1)
aux(2) =< aux(1)+1
s(31) =< it(50)*aux(1)
s(34) =< it(53)*aux(2)
s(37) =< it(53)+it(53)+it(57)+it(53)+it(53)+it(53)+it(57)+it(53)+it(53)+aux(199)
s(37) =< it(53)*aux(7)

  with precondition: [V>=6,V2>=0,Out>=7] 

* Chain [[50,51,52,53,54,55,56,57,58,59,60,61,62,63,64,80,81,82,83],77,101]: 6*it(50)+3*it(52)+51*it(53)+9*it(57)+1*s(31)+4*s(32)+4*s(33)+1*s(34)+1*s(37)+1*s(264)+6
  Such that:aux(28) =< V
aux(29) =< V+9
aux(1) =< V+V2
aux(30) =< 2*V
aux(32) =< 3*V
aux(33) =< 3*V+27
aux(34) =< 2/3*V
aux(200) =< 2*V+18
aux(201) =< V2
s(264) =< aux(200)
it(50) =< aux(28)
it(52) =< aux(28)
it(53) =< aux(28)
it(57) =< aux(28)
it(50) =< aux(29)
it(52) =< aux(29)
it(53) =< aux(29)
it(57) =< aux(29)
it(52) =< aux(30)
it(53) =< aux(30)
it(57) =< aux(30)
s(32) =< aux(30)
it(52) =< aux(200)
it(53) =< aux(200)
it(57) =< aux(200)
s(32) =< aux(200)
it(53) =< aux(32)
it(57) =< aux(32)
s(33) =< aux(32)
it(53) =< aux(33)
it(57) =< aux(33)
s(33) =< aux(33)
it(52) =< aux(34)
it(57) =< aux(34)
aux(7) =< aux(1)
aux(2) =< aux(1)+1
s(31) =< it(50)*aux(1)
s(34) =< it(53)*aux(2)
s(37) =< it(53)+it(53)+it(57)+it(53)+it(53)+it(53)+it(57)+it(53)+it(53)+aux(201)
s(37) =< it(53)*aux(7)

  with precondition: [V>=6,V2>=0,Out>=8] 

* Chain [[50,51,52,53,54,55,56,57,58,59,60,61,62,63,64,80,81,82,83],77,92]: 6*it(50)+3*it(52)+51*it(53)+9*it(57)+1*s(31)+4*s(32)+4*s(33)+1*s(34)+1*s(37)+1*s(264)+5
  Such that:aux(28) =< V
aux(29) =< V+7
aux(1) =< V+V2
aux(30) =< 2*V
aux(32) =< 3*V
aux(33) =< 3*V+21
aux(34) =< 2/3*V
aux(202) =< 2*V+14
aux(203) =< V2
s(264) =< aux(202)
it(50) =< aux(28)
it(52) =< aux(28)
it(53) =< aux(28)
it(57) =< aux(28)
it(50) =< aux(29)
it(52) =< aux(29)
it(53) =< aux(29)
it(57) =< aux(29)
it(52) =< aux(30)
it(53) =< aux(30)
it(57) =< aux(30)
s(32) =< aux(30)
it(52) =< aux(202)
it(53) =< aux(202)
it(57) =< aux(202)
s(32) =< aux(202)
it(53) =< aux(32)
it(57) =< aux(32)
s(33) =< aux(32)
it(53) =< aux(33)
it(57) =< aux(33)
s(33) =< aux(33)
it(52) =< aux(34)
it(57) =< aux(34)
aux(7) =< aux(1)
aux(2) =< aux(1)+1
s(31) =< it(50)*aux(1)
s(34) =< it(53)*aux(2)
s(37) =< it(53)+it(53)+it(57)+it(53)+it(53)+it(53)+it(57)+it(53)+it(53)+aux(203)
s(37) =< it(53)*aux(7)

  with precondition: [V>=6,V2>=0,Out>=7] 

* Chain [[50,51,52,53,54,55,56,57,58,59,60,61,62,63,64,80,81,82,83],76,102]: 6*it(50)+3*it(52)+51*it(53)+9*it(57)+1*s(31)+4*s(32)+4*s(33)+1*s(34)+1*s(37)+1*s(265)+6
  Such that:aux(1) =< V+V2
s(265) =< V/2+V2
aux(204) =< V
aux(205) =< 2*V
aux(206) =< 3*V
aux(207) =< 2/3*V
aux(208) =< V2
it(50) =< aux(204)
it(52) =< aux(204)
it(53) =< aux(204)
it(57) =< aux(204)
it(52) =< aux(205)
it(53) =< aux(205)
it(57) =< aux(205)
s(32) =< aux(205)
it(53) =< aux(206)
it(57) =< aux(206)
s(33) =< aux(206)
it(52) =< aux(207)
it(57) =< aux(207)
aux(7) =< aux(1)
aux(2) =< aux(1)+1
s(31) =< it(50)*aux(1)
s(34) =< it(53)*aux(2)
s(37) =< it(53)+it(53)+it(57)+it(53)+it(53)+it(53)+it(57)+it(53)+it(53)+aux(208)
s(37) =< it(53)*aux(7)

  with precondition: [V>=4,V2>=0,Out>=6] 

* Chain [[50,51,52,53,54,55,56,57,58,59,60,61,62,63,64,80,81,82,83],76,101]: 6*it(50)+3*it(52)+51*it(53)+9*it(57)+1*s(31)+4*s(32)+4*s(33)+1*s(34)+1*s(37)+1*s(265)+6
  Such that:aux(1) =< V+V2
s(265) =< V/2+V2
aux(209) =< V
aux(210) =< 2*V
aux(211) =< 3*V
aux(212) =< 2/3*V
aux(213) =< V2
it(50) =< aux(209)
it(52) =< aux(209)
it(53) =< aux(209)
it(57) =< aux(209)
it(52) =< aux(210)
it(53) =< aux(210)
it(57) =< aux(210)
s(32) =< aux(210)
it(53) =< aux(211)
it(57) =< aux(211)
s(33) =< aux(211)
it(52) =< aux(212)
it(57) =< aux(212)
aux(7) =< aux(1)
aux(2) =< aux(1)+1
s(31) =< it(50)*aux(1)
s(34) =< it(53)*aux(2)
s(37) =< it(53)+it(53)+it(57)+it(53)+it(53)+it(53)+it(57)+it(53)+it(53)+aux(213)
s(37) =< it(53)*aux(7)

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

* Chain [[50,51,52,53,54,55,56,57,58,59,60,61,62,63,64,80,81,82,83],76,92]: 6*it(50)+3*it(52)+51*it(53)+9*it(57)+1*s(31)+4*s(32)+4*s(33)+1*s(34)+1*s(37)+1*s(265)+5
  Such that:aux(1) =< V+V2
s(265) =< V/2+V2
aux(214) =< V
aux(215) =< 2*V
aux(216) =< 3*V
aux(217) =< 2/3*V
aux(218) =< V2
it(50) =< aux(214)
it(52) =< aux(214)
it(53) =< aux(214)
it(57) =< aux(214)
it(52) =< aux(215)
it(53) =< aux(215)
it(57) =< aux(215)
s(32) =< aux(215)
it(53) =< aux(216)
it(57) =< aux(216)
s(33) =< aux(216)
it(52) =< aux(217)
it(57) =< aux(217)
aux(7) =< aux(1)
aux(2) =< aux(1)+1
s(31) =< it(50)*aux(1)
s(34) =< it(53)*aux(2)
s(37) =< it(53)+it(53)+it(57)+it(53)+it(53)+it(53)+it(57)+it(53)+it(53)+aux(218)
s(37) =< it(53)*aux(7)

  with precondition: [V>=4,V2>=0,Out>=6] 

* Chain [[50,51,52,53,54,55,56,57,58,59,60,61,62,63,64,80,81,82,83],75,102]: 6*it(50)+3*it(52)+51*it(53)+9*it(57)+1*s(31)+5*s(32)+4*s(33)+1*s(34)+1*s(37)+6
  Such that:aux(1) =< V+V2
aux(34) =< 2/3*V
aux(219) =< V
aux(220) =< 2*V
aux(221) =< 3*V
aux(222) =< V2
s(32) =< aux(220)
it(50) =< aux(219)
it(52) =< aux(219)
it(53) =< aux(219)
it(57) =< aux(219)
it(52) =< aux(220)
it(53) =< aux(220)
it(57) =< aux(220)
it(53) =< aux(221)
it(57) =< aux(221)
s(33) =< aux(221)
it(52) =< aux(34)
it(57) =< aux(34)
aux(7) =< aux(1)
aux(2) =< aux(1)+1
s(31) =< it(50)*aux(1)
s(34) =< it(53)*aux(2)
s(37) =< it(53)+it(53)+it(57)+it(53)+it(53)+it(53)+it(57)+it(53)+it(53)+aux(222)
s(37) =< it(53)*aux(7)

  with precondition: [V>=4,V2>=0,Out>=6] 

* Chain [[50,51,52,53,54,55,56,57,58,59,60,61,62,63,64,80,81,82,83],75,101]: 6*it(50)+3*it(52)+51*it(53)+9*it(57)+1*s(31)+5*s(32)+4*s(33)+1*s(34)+1*s(37)+6
  Such that:aux(1) =< V+V2
aux(34) =< 2/3*V
aux(223) =< V
aux(224) =< 2*V
aux(225) =< 3*V
aux(226) =< V2
s(32) =< aux(224)
it(50) =< aux(223)
it(52) =< aux(223)
it(53) =< aux(223)
it(57) =< aux(223)
it(52) =< aux(224)
it(53) =< aux(224)
it(57) =< aux(224)
it(53) =< aux(225)
it(57) =< aux(225)
s(33) =< aux(225)
it(52) =< aux(34)
it(57) =< aux(34)
aux(7) =< aux(1)
aux(2) =< aux(1)+1
s(31) =< it(50)*aux(1)
s(34) =< it(53)*aux(2)
s(37) =< it(53)+it(53)+it(57)+it(53)+it(53)+it(53)+it(57)+it(53)+it(53)+aux(226)
s(37) =< it(53)*aux(7)

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

* Chain [[50,51,52,53,54,55,56,57,58,59,60,61,62,63,64,80,81,82,83],75,92]: 6*it(50)+3*it(52)+51*it(53)+9*it(57)+1*s(31)+5*s(32)+4*s(33)+1*s(34)+1*s(37)+5
  Such that:aux(1) =< V+V2
aux(34) =< 2/3*V
aux(227) =< V
aux(228) =< 2*V
aux(229) =< 3*V
aux(230) =< V2
s(32) =< aux(228)
it(50) =< aux(227)
it(52) =< aux(227)
it(53) =< aux(227)
it(57) =< aux(227)
it(52) =< aux(228)
it(53) =< aux(228)
it(57) =< aux(228)
it(53) =< aux(229)
it(57) =< aux(229)
s(33) =< aux(229)
it(52) =< aux(34)
it(57) =< aux(34)
aux(7) =< aux(1)
aux(2) =< aux(1)+1
s(31) =< it(50)*aux(1)
s(34) =< it(53)*aux(2)
s(37) =< it(53)+it(53)+it(57)+it(53)+it(53)+it(53)+it(57)+it(53)+it(53)+aux(230)
s(37) =< it(53)*aux(7)

  with precondition: [V>=4,V2>=0,Out>=6] 

* Chain [[50,51,52,53,54,55,56,57,58,59,60,61,62,63,64,80,81,82,83],74,102]: 6*it(50)+3*it(52)+51*it(53)+9*it(57)+1*s(31)+4*s(32)+4*s(33)+1*s(34)+1*s(37)+6
  Such that:aux(1) =< V+V2
aux(231) =< V
aux(232) =< 2*V
aux(233) =< 3*V
aux(234) =< 2/3*V
aux(235) =< V2
it(50) =< aux(231)
it(52) =< aux(231)
it(53) =< aux(231)
it(57) =< aux(231)
it(52) =< aux(232)
it(53) =< aux(232)
it(57) =< aux(232)
s(32) =< aux(232)
it(53) =< aux(233)
it(57) =< aux(233)
s(33) =< aux(233)
it(52) =< aux(234)
it(57) =< aux(234)
aux(7) =< aux(1)
aux(2) =< aux(1)+1
s(31) =< it(50)*aux(1)
s(34) =< it(53)*aux(2)
s(37) =< it(53)+it(53)+it(57)+it(53)+it(53)+it(53)+it(57)+it(53)+it(53)+aux(235)
s(37) =< it(53)*aux(7)

  with precondition: [V>=4,V2>=0,Out>=5] 

* Chain [[50,51,52,53,54,55,56,57,58,59,60,61,62,63,64,80,81,82,83],74,101]: 6*it(50)+3*it(52)+51*it(53)+9*it(57)+1*s(31)+4*s(32)+4*s(33)+1*s(34)+1*s(37)+6
  Such that:aux(1) =< V+V2
aux(236) =< V
aux(237) =< 2*V
aux(238) =< 3*V
aux(239) =< 2/3*V
aux(240) =< V2
it(50) =< aux(236)
it(52) =< aux(236)
it(53) =< aux(236)
it(57) =< aux(236)
it(52) =< aux(237)
it(53) =< aux(237)
it(57) =< aux(237)
s(32) =< aux(237)
it(53) =< aux(238)
it(57) =< aux(238)
s(33) =< aux(238)
it(52) =< aux(239)
it(57) =< aux(239)
aux(7) =< aux(1)
aux(2) =< aux(1)+1
s(31) =< it(50)*aux(1)
s(34) =< it(53)*aux(2)
s(37) =< it(53)+it(53)+it(57)+it(53)+it(53)+it(53)+it(57)+it(53)+it(53)+aux(240)
s(37) =< it(53)*aux(7)

  with precondition: [V>=4,V2>=0,Out>=6] 

* Chain [[50,51,52,53,54,55,56,57,58,59,60,61,62,63,64,80,81,82,83],74,100]: 6*it(50)+3*it(52)+51*it(53)+9*it(57)+1*s(31)+4*s(32)+4*s(33)+1*s(34)+1*s(37)+39*s(42)+6
  Such that:aux(1) =< V+V2
aux(44) =< V/2+V2
aux(241) =< V
aux(242) =< 2*V
aux(243) =< 3*V
aux(244) =< 2/3*V
aux(245) =< V2
s(42) =< aux(44)
it(50) =< aux(241)
it(52) =< aux(241)
it(53) =< aux(241)
it(57) =< aux(241)
it(52) =< aux(242)
it(53) =< aux(242)
it(57) =< aux(242)
s(32) =< aux(242)
it(53) =< aux(243)
it(57) =< aux(243)
s(33) =< aux(243)
it(52) =< aux(244)
it(57) =< aux(244)
aux(7) =< aux(1)
aux(2) =< aux(1)+1
s(31) =< it(50)*aux(1)
s(34) =< it(53)*aux(2)
s(37) =< it(53)+it(53)+it(57)+it(53)+it(53)+it(53)+it(57)+it(53)+it(53)+aux(245)
s(37) =< it(53)*aux(7)

  with precondition: [V>=4,V2>=0,Out>=6] 

* Chain [[50,51,52,53,54,55,56,57,58,59,60,61,62,63,64,80,81,82,83],73,102]: 6*it(50)+3*it(52)+51*it(53)+9*it(57)+1*s(31)+4*s(32)+4*s(33)+1*s(34)+1*s(37)+9
  Such that:aux(1) =< V+V2
aux(246) =< V
aux(247) =< 2*V
aux(248) =< 3*V
aux(249) =< 2/3*V
aux(250) =< V2
it(50) =< aux(246)
it(52) =< aux(246)
it(53) =< aux(246)
it(57) =< aux(246)
it(52) =< aux(247)
it(53) =< aux(247)
it(57) =< aux(247)
s(32) =< aux(247)
it(53) =< aux(248)
it(57) =< aux(248)
s(33) =< aux(248)
it(52) =< aux(249)
it(57) =< aux(249)
aux(7) =< aux(1)
aux(2) =< aux(1)+1
s(31) =< it(50)*aux(1)
s(34) =< it(53)*aux(2)
s(37) =< it(53)+it(53)+it(57)+it(53)+it(53)+it(53)+it(57)+it(53)+it(53)+aux(250)
s(37) =< it(53)*aux(7)

  with precondition: [V>=4,V2>=0,Out>=6] 

* Chain [[50,51,52,53,54,55,56,57,58,59,60,61,62,63,64,80,81,82,83],73,101]: 6*it(50)+3*it(52)+51*it(53)+9*it(57)+1*s(31)+4*s(32)+4*s(33)+1*s(34)+1*s(37)+9
  Such that:aux(1) =< V+V2
aux(251) =< V
aux(252) =< 2*V
aux(253) =< 3*V
aux(254) =< 2/3*V
aux(255) =< V2
it(50) =< aux(251)
it(52) =< aux(251)
it(53) =< aux(251)
it(57) =< aux(251)
it(52) =< aux(252)
it(53) =< aux(252)
it(57) =< aux(252)
s(32) =< aux(252)
it(53) =< aux(253)
it(57) =< aux(253)
s(33) =< aux(253)
it(52) =< aux(254)
it(57) =< aux(254)
aux(7) =< aux(1)
aux(2) =< aux(1)+1
s(31) =< it(50)*aux(1)
s(34) =< it(53)*aux(2)
s(37) =< it(53)+it(53)+it(57)+it(53)+it(53)+it(53)+it(57)+it(53)+it(53)+aux(255)
s(37) =< it(53)*aux(7)

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

* Chain [[50,51,52,53,54,55,56,57,58,59,60,61,62,63,64,80,81,82,83],73,100]: 6*it(50)+3*it(52)+51*it(53)+9*it(57)+1*s(31)+4*s(32)+4*s(33)+1*s(34)+1*s(37)+39*s(42)+9
  Such that:aux(1) =< V+V2
aux(44) =< V/2+V2
aux(256) =< V
aux(257) =< 2*V
aux(258) =< 3*V
aux(259) =< 2/3*V
aux(260) =< V2
s(42) =< aux(44)
it(50) =< aux(256)
it(52) =< aux(256)
it(53) =< aux(256)
it(57) =< aux(256)
it(52) =< aux(257)
it(53) =< aux(257)
it(57) =< aux(257)
s(32) =< aux(257)
it(53) =< aux(258)
it(57) =< aux(258)
s(33) =< aux(258)
it(52) =< aux(259)
it(57) =< aux(259)
aux(7) =< aux(1)
aux(2) =< aux(1)+1
s(31) =< it(50)*aux(1)
s(34) =< it(53)*aux(2)
s(37) =< it(53)+it(53)+it(57)+it(53)+it(53)+it(53)+it(57)+it(53)+it(53)+aux(260)
s(37) =< it(53)*aux(7)

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

* Chain [[50,51,52,53,54,55,56,57,58,59,60,61,62,63,64,80,81,82,83],72,102]: 6*it(50)+3*it(52)+51*it(53)+9*it(57)+1*s(31)+4*s(32)+4*s(33)+1*s(34)+1*s(37)+1*s(269)+6
  Such that:aux(28) =< V
aux(29) =< V+7
aux(1) =< V+V2
aux(30) =< 2*V
aux(32) =< 3*V
aux(33) =< 3*V+21
aux(34) =< 2/3*V
aux(261) =< 2*V+14
aux(262) =< V2
s(269) =< aux(261)
it(50) =< aux(28)
it(52) =< aux(28)
it(53) =< aux(28)
it(57) =< aux(28)
it(50) =< aux(29)
it(52) =< aux(29)
it(53) =< aux(29)
it(57) =< aux(29)
it(52) =< aux(30)
it(53) =< aux(30)
it(57) =< aux(30)
s(32) =< aux(30)
it(52) =< aux(261)
it(53) =< aux(261)
it(57) =< aux(261)
s(32) =< aux(261)
it(53) =< aux(32)
it(57) =< aux(32)
s(33) =< aux(32)
it(53) =< aux(33)
it(57) =< aux(33)
s(33) =< aux(33)
it(52) =< aux(34)
it(57) =< aux(34)
aux(7) =< aux(1)
aux(2) =< aux(1)+1
s(31) =< it(50)*aux(1)
s(34) =< it(53)*aux(2)
s(37) =< it(53)+it(53)+it(57)+it(53)+it(53)+it(53)+it(57)+it(53)+it(53)+aux(262)
s(37) =< it(53)*aux(7)

  with precondition: [V>=6,V2>=0,Out>=7] 

* Chain [[50,51,52,53,54,55,56,57,58,59,60,61,62,63,64,80,81,82,83],72,101]: 6*it(50)+3*it(52)+51*it(53)+9*it(57)+1*s(31)+4*s(32)+4*s(33)+1*s(34)+1*s(37)+1*s(269)+6
  Such that:aux(28) =< V
aux(29) =< V+9
aux(1) =< V+V2
aux(30) =< 2*V
aux(32) =< 3*V
aux(33) =< 3*V+27
aux(34) =< 2/3*V
aux(263) =< 2*V+18
aux(264) =< V2
s(269) =< aux(263)
it(50) =< aux(28)
it(52) =< aux(28)
it(53) =< aux(28)
it(57) =< aux(28)
it(50) =< aux(29)
it(52) =< aux(29)
it(53) =< aux(29)
it(57) =< aux(29)
it(52) =< aux(30)
it(53) =< aux(30)
it(57) =< aux(30)
s(32) =< aux(30)
it(52) =< aux(263)
it(53) =< aux(263)
it(57) =< aux(263)
s(32) =< aux(263)
it(53) =< aux(32)
it(57) =< aux(32)
s(33) =< aux(32)
it(53) =< aux(33)
it(57) =< aux(33)
s(33) =< aux(33)
it(52) =< aux(34)
it(57) =< aux(34)
aux(7) =< aux(1)
aux(2) =< aux(1)+1
s(31) =< it(50)*aux(1)
s(34) =< it(53)*aux(2)
s(37) =< it(53)+it(53)+it(57)+it(53)+it(53)+it(53)+it(57)+it(53)+it(53)+aux(264)
s(37) =< it(53)*aux(7)

  with precondition: [V>=6,V2>=0,Out>=8] 

* Chain [[50,51,52,53,54,55,56,57,58,59,60,61,62,63,64,80,81,82,83],72,100]: 6*it(50)+3*it(52)+51*it(53)+9*it(57)+1*s(31)+4*s(32)+4*s(33)+1*s(34)+1*s(37)+39*s(42)+1*s(269)+6
  Such that:aux(28) =< V
aux(1) =< V+V2
aux(30) =< 2*V
aux(32) =< 3*V
aux(33) =< 3*V+3
aux(44) =< V/2+V2+3
aux(34) =< 2/3*V
aux(265) =< V+1
aux(266) =< 2*V+2
aux(267) =< V2
s(269) =< aux(265)
s(42) =< aux(44)
it(50) =< aux(28)
it(52) =< aux(28)
it(53) =< aux(28)
it(57) =< aux(28)
it(50) =< aux(265)
it(52) =< aux(265)
it(53) =< aux(265)
it(57) =< aux(265)
it(52) =< aux(30)
it(53) =< aux(30)
it(57) =< aux(30)
s(32) =< aux(30)
it(52) =< aux(266)
it(53) =< aux(266)
it(57) =< aux(266)
s(32) =< aux(266)
it(53) =< aux(32)
it(57) =< aux(32)
s(33) =< aux(32)
it(53) =< aux(33)
it(57) =< aux(33)
s(33) =< aux(33)
it(52) =< aux(34)
it(57) =< aux(34)
aux(7) =< aux(1)
aux(2) =< aux(1)+1
s(31) =< it(50)*aux(1)
s(34) =< it(53)*aux(2)
s(37) =< it(53)+it(53)+it(57)+it(53)+it(53)+it(53)+it(57)+it(53)+it(53)+aux(267)
s(37) =< it(53)*aux(7)

  with precondition: [V>=6,V2>=0,Out>=8] 

* Chain [[50,51,52,53,54,55,56,57,58,59,60,61,62,63,64,80,81,82,83],71,102]: 6*it(50)+3*it(52)+51*it(53)+9*it(57)+1*s(31)+4*s(32)+4*s(33)+1*s(34)+1*s(37)+1*s(270)+6
  Such that:aux(1) =< V+V2
s(270) =< V/2+V2
aux(268) =< V
aux(269) =< 2*V
aux(270) =< 3*V
aux(271) =< 2/3*V
aux(272) =< V2
it(50) =< aux(268)
it(52) =< aux(268)
it(53) =< aux(268)
it(57) =< aux(268)
it(52) =< aux(269)
it(53) =< aux(269)
it(57) =< aux(269)
s(32) =< aux(269)
it(53) =< aux(270)
it(57) =< aux(270)
s(33) =< aux(270)
it(52) =< aux(271)
it(57) =< aux(271)
aux(7) =< aux(1)
aux(2) =< aux(1)+1
s(31) =< it(50)*aux(1)
s(34) =< it(53)*aux(2)
s(37) =< it(53)+it(53)+it(57)+it(53)+it(53)+it(53)+it(57)+it(53)+it(53)+aux(272)
s(37) =< it(53)*aux(7)

  with precondition: [V>=4,V2>=0,Out>=6] 

* Chain [[50,51,52,53,54,55,56,57,58,59,60,61,62,63,64,80,81,82,83],71,101]: 6*it(50)+3*it(52)+51*it(53)+9*it(57)+1*s(31)+4*s(32)+4*s(33)+1*s(34)+1*s(37)+1*s(270)+6
  Such that:aux(1) =< V+V2
s(270) =< V/2+V2
aux(273) =< V
aux(274) =< 2*V
aux(275) =< 3*V
aux(276) =< 2/3*V
aux(277) =< V2
it(50) =< aux(273)
it(52) =< aux(273)
it(53) =< aux(273)
it(57) =< aux(273)
it(52) =< aux(274)
it(53) =< aux(274)
it(57) =< aux(274)
s(32) =< aux(274)
it(53) =< aux(275)
it(57) =< aux(275)
s(33) =< aux(275)
it(52) =< aux(276)
it(57) =< aux(276)
aux(7) =< aux(1)
aux(2) =< aux(1)+1
s(31) =< it(50)*aux(1)
s(34) =< it(53)*aux(2)
s(37) =< it(53)+it(53)+it(57)+it(53)+it(53)+it(53)+it(57)+it(53)+it(53)+aux(277)
s(37) =< it(53)*aux(7)

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

* Chain [[50,51,52,53,54,55,56,57,58,59,60,61,62,63,64,80,81,82,83],71,100]: 6*it(50)+3*it(52)+51*it(53)+9*it(57)+1*s(31)+4*s(32)+4*s(33)+1*s(34)+1*s(37)+40*s(42)+6
  Such that:aux(1) =< V+V2
aux(278) =< V/2+V2
aux(279) =< V
aux(280) =< 2*V
aux(281) =< 3*V
aux(282) =< 2/3*V
aux(283) =< V2
s(42) =< aux(278)
it(50) =< aux(279)
it(52) =< aux(279)
it(53) =< aux(279)
it(57) =< aux(279)
it(52) =< aux(280)
it(53) =< aux(280)
it(57) =< aux(280)
s(32) =< aux(280)
it(53) =< aux(281)
it(57) =< aux(281)
s(33) =< aux(281)
it(52) =< aux(282)
it(57) =< aux(282)
aux(7) =< aux(1)
aux(2) =< aux(1)+1
s(31) =< it(50)*aux(1)
s(34) =< it(53)*aux(2)
s(37) =< it(53)+it(53)+it(57)+it(53)+it(53)+it(53)+it(57)+it(53)+it(53)+aux(283)
s(37) =< it(53)*aux(7)

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

* Chain [[50,51,52,53,54,55,56,57,58,59,60,61,62,63,64,80,81,82,83],70,102]: 6*it(50)+3*it(52)+51*it(53)+9*it(57)+1*s(31)+5*s(32)+4*s(33)+1*s(34)+1*s(37)+6
  Such that:aux(1) =< V+V2
aux(34) =< 2/3*V
aux(284) =< V
aux(285) =< 2*V
aux(286) =< 3*V
aux(287) =< V2
s(32) =< aux(285)
it(50) =< aux(284)
it(52) =< aux(284)
it(53) =< aux(284)
it(57) =< aux(284)
it(52) =< aux(285)
it(53) =< aux(285)
it(57) =< aux(285)
it(53) =< aux(286)
it(57) =< aux(286)
s(33) =< aux(286)
it(52) =< aux(34)
it(57) =< aux(34)
aux(7) =< aux(1)
aux(2) =< aux(1)+1
s(31) =< it(50)*aux(1)
s(34) =< it(53)*aux(2)
s(37) =< it(53)+it(53)+it(57)+it(53)+it(53)+it(53)+it(57)+it(53)+it(53)+aux(287)
s(37) =< it(53)*aux(7)

  with precondition: [V>=4,V2>=0,Out>=6] 

* Chain [[50,51,52,53,54,55,56,57,58,59,60,61,62,63,64,80,81,82,83],70,101]: 6*it(50)+3*it(52)+51*it(53)+9*it(57)+1*s(31)+5*s(32)+4*s(33)+1*s(34)+1*s(37)+6
  Such that:aux(1) =< V+V2
aux(34) =< 2/3*V
aux(288) =< V
aux(289) =< 2*V
aux(290) =< 3*V
aux(291) =< V2
s(32) =< aux(289)
it(50) =< aux(288)
it(52) =< aux(288)
it(53) =< aux(288)
it(57) =< aux(288)
it(52) =< aux(289)
it(53) =< aux(289)
it(57) =< aux(289)
it(53) =< aux(290)
it(57) =< aux(290)
s(33) =< aux(290)
it(52) =< aux(34)
it(57) =< aux(34)
aux(7) =< aux(1)
aux(2) =< aux(1)+1
s(31) =< it(50)*aux(1)
s(34) =< it(53)*aux(2)
s(37) =< it(53)+it(53)+it(57)+it(53)+it(53)+it(53)+it(57)+it(53)+it(53)+aux(291)
s(37) =< it(53)*aux(7)

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

* Chain [[50,51,52,53,54,55,56,57,58,59,60,61,62,63,64,80,81,82,83],70,100]: 6*it(50)+3*it(52)+51*it(53)+9*it(57)+1*s(31)+5*s(32)+4*s(33)+1*s(34)+1*s(37)+39*s(42)+6
  Such that:aux(1) =< V+V2
aux(44) =< V/2+V2+2
aux(34) =< 2/3*V
aux(292) =< V
aux(293) =< 2*V
aux(294) =< 3*V
aux(295) =< V2
s(32) =< aux(293)
s(42) =< aux(44)
it(50) =< aux(292)
it(52) =< aux(292)
it(53) =< aux(292)
it(57) =< aux(292)
it(52) =< aux(293)
it(53) =< aux(293)
it(57) =< aux(293)
it(53) =< aux(294)
it(57) =< aux(294)
s(33) =< aux(294)
it(52) =< aux(34)
it(57) =< aux(34)
aux(7) =< aux(1)
aux(2) =< aux(1)+1
s(31) =< it(50)*aux(1)
s(34) =< it(53)*aux(2)
s(37) =< it(53)+it(53)+it(57)+it(53)+it(53)+it(53)+it(57)+it(53)+it(53)+aux(295)
s(37) =< it(53)*aux(7)

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

* Chain [[50,51,52,53,54,55,56,57,58,59,60,61,62,63,64,80,81,82,83],69,102]: 6*it(50)+3*it(52)+51*it(53)+9*it(57)+1*s(31)+4*s(32)+4*s(33)+1*s(34)+1*s(37)+6
  Such that:aux(1) =< V+V2
aux(296) =< V
aux(297) =< 2*V
aux(298) =< 3*V
aux(299) =< 2/3*V
aux(300) =< V2
it(50) =< aux(296)
it(52) =< aux(296)
it(53) =< aux(296)
it(57) =< aux(296)
it(52) =< aux(297)
it(53) =< aux(297)
it(57) =< aux(297)
s(32) =< aux(297)
it(53) =< aux(298)
it(57) =< aux(298)
s(33) =< aux(298)
it(52) =< aux(299)
it(57) =< aux(299)
aux(7) =< aux(1)
aux(2) =< aux(1)+1
s(31) =< it(50)*aux(1)
s(34) =< it(53)*aux(2)
s(37) =< it(53)+it(53)+it(57)+it(53)+it(53)+it(53)+it(57)+it(53)+it(53)+aux(300)
s(37) =< it(53)*aux(7)

  with precondition: [V>=4,V2>=0,Out>=5] 

* Chain [[50,51,52,53,54,55,56,57,58,59,60,61,62,63,64,80,81,82,83],69,101]: 6*it(50)+3*it(52)+51*it(53)+9*it(57)+1*s(31)+4*s(32)+4*s(33)+1*s(34)+1*s(37)+6
  Such that:aux(1) =< V+V2
aux(301) =< V
aux(302) =< 2*V
aux(303) =< 3*V
aux(304) =< 2/3*V
aux(305) =< V2
it(50) =< aux(301)
it(52) =< aux(301)
it(53) =< aux(301)
it(57) =< aux(301)
it(52) =< aux(302)
it(53) =< aux(302)
it(57) =< aux(302)
s(32) =< aux(302)
it(53) =< aux(303)
it(57) =< aux(303)
s(33) =< aux(303)
it(52) =< aux(304)
it(57) =< aux(304)
aux(7) =< aux(1)
aux(2) =< aux(1)+1
s(31) =< it(50)*aux(1)
s(34) =< it(53)*aux(2)
s(37) =< it(53)+it(53)+it(57)+it(53)+it(53)+it(53)+it(57)+it(53)+it(53)+aux(305)
s(37) =< it(53)*aux(7)

  with precondition: [V>=4,V2>=0,Out>=6] 

* Chain [[50,51,52,53,54,55,56,57,58,59,60,61,62,63,64,80,81,82,83],69,100]: 6*it(50)+3*it(52)+51*it(53)+9*it(57)+1*s(31)+4*s(32)+4*s(33)+1*s(34)+1*s(37)+39*s(42)+6
  Such that:aux(1) =< V+V2
aux(44) =< V/2+V2
aux(306) =< V
aux(307) =< 2*V
aux(308) =< 3*V
aux(309) =< 2/3*V
aux(310) =< V2
s(42) =< aux(44)
it(50) =< aux(306)
it(52) =< aux(306)
it(53) =< aux(306)
it(57) =< aux(306)
it(52) =< aux(307)
it(53) =< aux(307)
it(57) =< aux(307)
s(32) =< aux(307)
it(53) =< aux(308)
it(57) =< aux(308)
s(33) =< aux(308)
it(52) =< aux(309)
it(57) =< aux(309)
aux(7) =< aux(1)
aux(2) =< aux(1)+1
s(31) =< it(50)*aux(1)
s(34) =< it(53)*aux(2)
s(37) =< it(53)+it(53)+it(57)+it(53)+it(53)+it(53)+it(57)+it(53)+it(53)+aux(310)
s(37) =< it(53)*aux(7)

  with precondition: [V>=4,V2>=0,Out>=6] 

* Chain [[50,51,52,53,54,55,56,57,58,59,60,61,62,63,64,80,81,82,83],68,102]: 6*it(50)+3*it(52)+51*it(53)+9*it(57)+1*s(31)+4*s(32)+4*s(33)+1*s(34)+1*s(37)+9
  Such that:aux(1) =< V+V2
aux(311) =< V
aux(312) =< 2*V
aux(313) =< 3*V
aux(314) =< 2/3*V
aux(315) =< V2
it(50) =< aux(311)
it(52) =< aux(311)
it(53) =< aux(311)
it(57) =< aux(311)
it(52) =< aux(312)
it(53) =< aux(312)
it(57) =< aux(312)
s(32) =< aux(312)
it(53) =< aux(313)
it(57) =< aux(313)
s(33) =< aux(313)
it(52) =< aux(314)
it(57) =< aux(314)
aux(7) =< aux(1)
aux(2) =< aux(1)+1
s(31) =< it(50)*aux(1)
s(34) =< it(53)*aux(2)
s(37) =< it(53)+it(53)+it(57)+it(53)+it(53)+it(53)+it(57)+it(53)+it(53)+aux(315)
s(37) =< it(53)*aux(7)

  with precondition: [V>=4,V2>=0,Out>=6] 

* Chain [[50,51,52,53,54,55,56,57,58,59,60,61,62,63,64,80,81,82,83],68,101]: 6*it(50)+3*it(52)+51*it(53)+9*it(57)+1*s(31)+4*s(32)+4*s(33)+1*s(34)+1*s(37)+9
  Such that:aux(1) =< V+V2
aux(316) =< V
aux(317) =< 2*V
aux(318) =< 3*V
aux(319) =< 2/3*V
aux(320) =< V2
it(50) =< aux(316)
it(52) =< aux(316)
it(53) =< aux(316)
it(57) =< aux(316)
it(52) =< aux(317)
it(53) =< aux(317)
it(57) =< aux(317)
s(32) =< aux(317)
it(53) =< aux(318)
it(57) =< aux(318)
s(33) =< aux(318)
it(52) =< aux(319)
it(57) =< aux(319)
aux(7) =< aux(1)
aux(2) =< aux(1)+1
s(31) =< it(50)*aux(1)
s(34) =< it(53)*aux(2)
s(37) =< it(53)+it(53)+it(57)+it(53)+it(53)+it(53)+it(57)+it(53)+it(53)+aux(320)
s(37) =< it(53)*aux(7)

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

* Chain [[50,51,52,53,54,55,56,57,58,59,60,61,62,63,64,80,81,82,83],68,100]: 6*it(50)+3*it(52)+51*it(53)+9*it(57)+1*s(31)+4*s(32)+4*s(33)+1*s(34)+1*s(37)+39*s(42)+9
  Such that:aux(1) =< V+V2
aux(44) =< V/2+V2
aux(321) =< V
aux(322) =< 2*V
aux(323) =< 3*V
aux(324) =< 2/3*V
aux(325) =< V2
s(42) =< aux(44)
it(50) =< aux(321)
it(52) =< aux(321)
it(53) =< aux(321)
it(57) =< aux(321)
it(52) =< aux(322)
it(53) =< aux(322)
it(57) =< aux(322)
s(32) =< aux(322)
it(53) =< aux(323)
it(57) =< aux(323)
s(33) =< aux(323)
it(52) =< aux(324)
it(57) =< aux(324)
aux(7) =< aux(1)
aux(2) =< aux(1)+1
s(31) =< it(50)*aux(1)
s(34) =< it(53)*aux(2)
s(37) =< it(53)+it(53)+it(57)+it(53)+it(53)+it(53)+it(57)+it(53)+it(53)+aux(325)
s(37) =< it(53)*aux(7)

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

* Chain [[50,51,52,53,54,55,56,57,58,59,60,61,62,63,64,80,81,82,83],67,102]: 6*it(50)+3*it(52)+51*it(53)+9*it(57)+1*s(31)+4*s(32)+4*s(33)+1*s(34)+1*s(37)+1*s(274)+6
  Such that:aux(28) =< V
aux(29) =< V+7
aux(1) =< V+V2
aux(30) =< 2*V
aux(32) =< 3*V
aux(33) =< 3*V+21
aux(34) =< 2/3*V
aux(326) =< 2*V+14
aux(327) =< V2
s(274) =< aux(326)
it(50) =< aux(28)
it(52) =< aux(28)
it(53) =< aux(28)
it(57) =< aux(28)
it(50) =< aux(29)
it(52) =< aux(29)
it(53) =< aux(29)
it(57) =< aux(29)
it(52) =< aux(30)
it(53) =< aux(30)
it(57) =< aux(30)
s(32) =< aux(30)
it(52) =< aux(326)
it(53) =< aux(326)
it(57) =< aux(326)
s(32) =< aux(326)
it(53) =< aux(32)
it(57) =< aux(32)
s(33) =< aux(32)
it(53) =< aux(33)
it(57) =< aux(33)
s(33) =< aux(33)
it(52) =< aux(34)
it(57) =< aux(34)
aux(7) =< aux(1)
aux(2) =< aux(1)+1
s(31) =< it(50)*aux(1)
s(34) =< it(53)*aux(2)
s(37) =< it(53)+it(53)+it(57)+it(53)+it(53)+it(53)+it(57)+it(53)+it(53)+aux(327)
s(37) =< it(53)*aux(7)

  with precondition: [V>=6,V2>=0,Out>=7] 

* Chain [[50,51,52,53,54,55,56,57,58,59,60,61,62,63,64,80,81,82,83],67,101]: 6*it(50)+3*it(52)+51*it(53)+9*it(57)+1*s(31)+4*s(32)+4*s(33)+1*s(34)+1*s(37)+1*s(274)+6
  Such that:aux(28) =< V
aux(29) =< V+9
aux(1) =< V+V2
aux(30) =< 2*V
aux(32) =< 3*V
aux(33) =< 3*V+27
aux(34) =< 2/3*V
aux(328) =< 2*V+18
aux(329) =< V2
s(274) =< aux(328)
it(50) =< aux(28)
it(52) =< aux(28)
it(53) =< aux(28)
it(57) =< aux(28)
it(50) =< aux(29)
it(52) =< aux(29)
it(53) =< aux(29)
it(57) =< aux(29)
it(52) =< aux(30)
it(53) =< aux(30)
it(57) =< aux(30)
s(32) =< aux(30)
it(52) =< aux(328)
it(53) =< aux(328)
it(57) =< aux(328)
s(32) =< aux(328)
it(53) =< aux(32)
it(57) =< aux(32)
s(33) =< aux(32)
it(53) =< aux(33)
it(57) =< aux(33)
s(33) =< aux(33)
it(52) =< aux(34)
it(57) =< aux(34)
aux(7) =< aux(1)
aux(2) =< aux(1)+1
s(31) =< it(50)*aux(1)
s(34) =< it(53)*aux(2)
s(37) =< it(53)+it(53)+it(57)+it(53)+it(53)+it(53)+it(57)+it(53)+it(53)+aux(329)
s(37) =< it(53)*aux(7)

  with precondition: [V>=6,V2>=0,Out>=8] 

* Chain [[50,51,52,53,54,55,56,57,58,59,60,61,62,63,64,80,81,82,83],67,100]: 6*it(50)+3*it(52)+51*it(53)+9*it(57)+1*s(31)+4*s(32)+4*s(33)+1*s(34)+1*s(37)+39*s(42)+1*s(274)+6
  Such that:aux(28) =< V
aux(29) =< V+1
aux(1) =< V+V2
aux(30) =< 2*V
aux(32) =< 3*V
aux(33) =< 3*V+3
aux(44) =< V/2+V2+2
aux(34) =< 2/3*V
aux(330) =< 2*V+2
aux(331) =< V2
s(274) =< aux(330)
s(42) =< aux(44)
it(50) =< aux(28)
it(52) =< aux(28)
it(53) =< aux(28)
it(57) =< aux(28)
it(50) =< aux(29)
it(52) =< aux(29)
it(53) =< aux(29)
it(57) =< aux(29)
it(52) =< aux(30)
it(53) =< aux(30)
it(57) =< aux(30)
s(32) =< aux(30)
it(52) =< aux(330)
it(53) =< aux(330)
it(57) =< aux(330)
s(32) =< aux(330)
it(53) =< aux(32)
it(57) =< aux(32)
s(33) =< aux(32)
it(53) =< aux(33)
it(57) =< aux(33)
s(33) =< aux(33)
it(52) =< aux(34)
it(57) =< aux(34)
aux(7) =< aux(1)
aux(2) =< aux(1)+1
s(31) =< it(50)*aux(1)
s(34) =< it(53)*aux(2)
s(37) =< it(53)+it(53)+it(57)+it(53)+it(53)+it(53)+it(57)+it(53)+it(53)+aux(331)
s(37) =< it(53)*aux(7)

  with precondition: [V>=6,V2>=0,Out>=8] 

* Chain [[50,51,52,53,54,55,56,57,58,59,60,61,62,63,64,80,81,82,83],66,102]: 6*it(50)+3*it(52)+51*it(53)+9*it(57)+1*s(31)+4*s(32)+4*s(33)+1*s(34)+1*s(37)+1*s(275)+6
  Such that:aux(1) =< V+V2
s(275) =< V/2+V2
aux(332) =< V
aux(333) =< 2*V
aux(334) =< 3*V
aux(335) =< 2/3*V
aux(336) =< V2
it(50) =< aux(332)
it(52) =< aux(332)
it(53) =< aux(332)
it(57) =< aux(332)
it(52) =< aux(333)
it(53) =< aux(333)
it(57) =< aux(333)
s(32) =< aux(333)
it(53) =< aux(334)
it(57) =< aux(334)
s(33) =< aux(334)
it(52) =< aux(335)
it(57) =< aux(335)
aux(7) =< aux(1)
aux(2) =< aux(1)+1
s(31) =< it(50)*aux(1)
s(34) =< it(53)*aux(2)
s(37) =< it(53)+it(53)+it(57)+it(53)+it(53)+it(53)+it(57)+it(53)+it(53)+aux(336)
s(37) =< it(53)*aux(7)

  with precondition: [V>=4,V2>=0,Out>=6] 

* Chain [[50,51,52,53,54,55,56,57,58,59,60,61,62,63,64,80,81,82,83],66,101]: 6*it(50)+3*it(52)+51*it(53)+9*it(57)+1*s(31)+4*s(32)+4*s(33)+1*s(34)+1*s(37)+1*s(275)+6
  Such that:aux(1) =< V+V2
s(275) =< V/2+V2
aux(337) =< V
aux(338) =< 2*V
aux(339) =< 3*V
aux(340) =< 2/3*V
aux(341) =< V2
it(50) =< aux(337)
it(52) =< aux(337)
it(53) =< aux(337)
it(57) =< aux(337)
it(52) =< aux(338)
it(53) =< aux(338)
it(57) =< aux(338)
s(32) =< aux(338)
it(53) =< aux(339)
it(57) =< aux(339)
s(33) =< aux(339)
it(52) =< aux(340)
it(57) =< aux(340)
aux(7) =< aux(1)
aux(2) =< aux(1)+1
s(31) =< it(50)*aux(1)
s(34) =< it(53)*aux(2)
s(37) =< it(53)+it(53)+it(57)+it(53)+it(53)+it(53)+it(57)+it(53)+it(53)+aux(341)
s(37) =< it(53)*aux(7)

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

* Chain [[50,51,52,53,54,55,56,57,58,59,60,61,62,63,64,80,81,82,83],66,100]: 6*it(50)+3*it(52)+51*it(53)+9*it(57)+1*s(31)+4*s(32)+4*s(33)+1*s(34)+1*s(37)+40*s(42)+6
  Such that:aux(1) =< V+V2
aux(342) =< V/2+V2
aux(343) =< V
aux(344) =< 2*V
aux(345) =< 3*V
aux(346) =< 2/3*V
aux(347) =< V2
s(42) =< aux(342)
it(50) =< aux(343)
it(52) =< aux(343)
it(53) =< aux(343)
it(57) =< aux(343)
it(52) =< aux(344)
it(53) =< aux(344)
it(57) =< aux(344)
s(32) =< aux(344)
it(53) =< aux(345)
it(57) =< aux(345)
s(33) =< aux(345)
it(52) =< aux(346)
it(57) =< aux(346)
aux(7) =< aux(1)
aux(2) =< aux(1)+1
s(31) =< it(50)*aux(1)
s(34) =< it(53)*aux(2)
s(37) =< it(53)+it(53)+it(57)+it(53)+it(53)+it(53)+it(57)+it(53)+it(53)+aux(347)
s(37) =< it(53)*aux(7)

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

* Chain [[50,51,52,53,54,55,56,57,58,59,60,61,62,63,64,80,81,82,83],65,102]: 6*it(50)+3*it(52)+51*it(53)+9*it(57)+1*s(31)+5*s(32)+4*s(33)+1*s(34)+1*s(37)+6
  Such that:aux(1) =< V+V2
aux(34) =< 2/3*V
aux(348) =< V
aux(349) =< 2*V
aux(350) =< 3*V
aux(351) =< V2
s(32) =< aux(349)
it(50) =< aux(348)
it(52) =< aux(348)
it(53) =< aux(348)
it(57) =< aux(348)
it(52) =< aux(349)
it(53) =< aux(349)
it(57) =< aux(349)
it(53) =< aux(350)
it(57) =< aux(350)
s(33) =< aux(350)
it(52) =< aux(34)
it(57) =< aux(34)
aux(7) =< aux(1)
aux(2) =< aux(1)+1
s(31) =< it(50)*aux(1)
s(34) =< it(53)*aux(2)
s(37) =< it(53)+it(53)+it(57)+it(53)+it(53)+it(53)+it(57)+it(53)+it(53)+aux(351)
s(37) =< it(53)*aux(7)

  with precondition: [V>=4,V2>=0,Out>=6] 

* Chain [[50,51,52,53,54,55,56,57,58,59,60,61,62,63,64,80,81,82,83],65,101]: 6*it(50)+3*it(52)+51*it(53)+9*it(57)+1*s(31)+5*s(32)+4*s(33)+1*s(34)+1*s(37)+6
  Such that:aux(1) =< V+V2
aux(34) =< 2/3*V
aux(352) =< V
aux(353) =< 2*V
aux(354) =< 3*V
aux(355) =< V2
s(32) =< aux(353)
it(50) =< aux(352)
it(52) =< aux(352)
it(53) =< aux(352)
it(57) =< aux(352)
it(52) =< aux(353)
it(53) =< aux(353)
it(57) =< aux(353)
it(53) =< aux(354)
it(57) =< aux(354)
s(33) =< aux(354)
it(52) =< aux(34)
it(57) =< aux(34)
aux(7) =< aux(1)
aux(2) =< aux(1)+1
s(31) =< it(50)*aux(1)
s(34) =< it(53)*aux(2)
s(37) =< it(53)+it(53)+it(57)+it(53)+it(53)+it(53)+it(57)+it(53)+it(53)+aux(355)
s(37) =< it(53)*aux(7)

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

* Chain [[50,51,52,53,54,55,56,57,58,59,60,61,62,63,64,80,81,82,83],65,100]: 6*it(50)+3*it(52)+51*it(53)+9*it(57)+1*s(31)+5*s(32)+4*s(33)+1*s(34)+1*s(37)+39*s(42)+6
  Such that:aux(1) =< V+V2
aux(44) =< V/2+V2+1
aux(34) =< 2/3*V
aux(356) =< V
aux(357) =< 2*V
aux(358) =< 3*V
aux(359) =< V2
s(32) =< aux(357)
s(42) =< aux(44)
it(50) =< aux(356)
it(52) =< aux(356)
it(53) =< aux(356)
it(57) =< aux(356)
it(52) =< aux(357)
it(53) =< aux(357)
it(57) =< aux(357)
it(53) =< aux(358)
it(57) =< aux(358)
s(33) =< aux(358)
it(52) =< aux(34)
it(57) =< aux(34)
aux(7) =< aux(1)
aux(2) =< aux(1)+1
s(31) =< it(50)*aux(1)
s(34) =< it(53)*aux(2)
s(37) =< it(53)+it(53)+it(57)+it(53)+it(53)+it(53)+it(57)+it(53)+it(53)+aux(359)
s(37) =< it(53)*aux(7)

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

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

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

* Chain [100]: 39*s(42)+3
  Such that:aux(44) =< V2
s(42) =< aux(44)

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

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

* Chain [98]: 6*s(81)+40*s(84)+3
  Such that:aux(55) =< 1
aux(56) =< V
s(84) =< aux(55)
s(81) =< aux(56)

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

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

* Chain [96]: 1*s(149)+3
  Such that:s(149) =< 2

  with precondition: [V=1,V2=0,Out=4] 

* Chain [95]: 7
  with precondition: [V=1,Out=4,V2>=1] 

* Chain [94]: 6*s(152)+2
  Such that:aux(79) =< V2
s(152) =< aux(79)

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

* Chain [93]: 2*s(158)+3
  Such that:aux(85) =< V2
s(158) =< aux(85)

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

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

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

* Chain [90]: 32*s(170)+2
  Such that:aux(103) =< V+1
s(170) =< aux(103)

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

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

* Chain [88]: 32*s(226)+2
  Such that:aux(112) =< V
s(226) =< aux(112)

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

* Chain [87,102]: 6
  with precondition: [V2=0,Out=3,V>=2] 

* Chain [87,101]: 6
  with precondition: [V2=0,Out=4,V>=2] 

* Chain [87,100]: 39*s(42)+6
  Such that:aux(44) =< 1
s(42) =< aux(44)

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

* Chain [86,102]: 9
  with precondition: [V2=0,5>=Out,V>=2,Out>=4] 

* Chain [86,101]: 9
  with precondition: [V2=0,6>=Out,V>=2,Out>=5] 

* Chain [86,100]: 39*s(42)+9
  Such that:aux(44) =< 1
s(42) =< aux(44)

  with precondition: [V2=0,6>=Out,V>=2,Out>=5] 

* Chain [85,102]: 1*s(260)+6
  Such that:s(260) =< 2*Out

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

* Chain [85,101]: 1*s(260)+6
  Such that:s(260) =< 2*Out

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

* Chain [85,100]: 39*s(42)+1*s(260)+6
  Such that:aux(44) =< 1
s(260) =< 2*Out
s(42) =< aux(44)

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

* Chain [84,102]: 1*s(261)+6
  Such that:s(261) =< V

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

* Chain [84,101]: 1*s(261)+6
  Such that:s(261) =< V

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

* Chain [84,100]: 39*s(42)+1*s(261)+6
  Such that:aux(44) =< 1
s(261) =< V
s(42) =< aux(44)

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

* Chain [79,102]: 6
  with precondition: [Out=3,V>=2,V2>=0] 

* Chain [79,101]: 6
  with precondition: [Out=4,V>=2,V2>=0] 

* Chain [79,92]: 5
  with precondition: [Out=3,V>=2,V2>=0] 

* Chain [78,102]: 9
  with precondition: [5>=Out,V>=2,V2>=0,Out>=4] 

* Chain [78,101]: 9
  with precondition: [6>=Out,V>=2,V2>=0,Out>=5] 

* Chain [78,92]: 8
  with precondition: [5>=Out,V>=2,V2>=0,Out>=4] 

* Chain [77,102]: 1*s(264)+6
  Such that:s(264) =< 2*Out

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

* Chain [77,101]: 1*s(264)+6
  Such that:s(264) =< 2*Out

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

* Chain [77,92]: 1*s(264)+5
  Such that:s(264) =< 2*Out

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

* Chain [76,102]: 1*s(265)+6
  Such that:s(265) =< V2

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

* Chain [76,101]: 1*s(265)+6
  Such that:s(265) =< V2

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

* Chain [76,92]: 1*s(265)+5
  Such that:s(265) =< V2

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

* Chain [75,102]: 1*s(266)+6
  Such that:s(266) =< V

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

* Chain [75,101]: 1*s(266)+6
  Such that:s(266) =< V

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

* Chain [75,92]: 1*s(266)+5
  Such that:s(266) =< V

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

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

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

* Chain [74,100]: 39*s(42)+6
  Such that:aux(44) =< V2+1
s(42) =< aux(44)

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

* Chain [73,102]: 9
  with precondition: [5>=Out,V>=2,V2>=1,Out>=4] 

* Chain [73,101]: 9
  with precondition: [6>=Out,V>=2,V2>=1,Out>=5] 

* Chain [73,100]: 39*s(42)+9
  Such that:aux(44) =< V2+1
s(42) =< aux(44)

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

* Chain [72,102]: 1*s(269)+6
  Such that:s(269) =< 2*Out

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

* Chain [72,101]: 1*s(269)+6
  Such that:s(269) =< 2*Out

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

* Chain [72,100]: 39*s(42)+1*s(269)+6
  Such that:s(269) =< V+1
aux(44) =< V2+1
s(42) =< aux(44)

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

* Chain [71,102]: 1*s(270)+6
  Such that:s(270) =< V2+1

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

* Chain [71,101]: 1*s(270)+6
  Such that:s(270) =< V2+1

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

* Chain [71,100]: 40*s(42)+6
  Such that:aux(278) =< V2+1
s(42) =< aux(278)

  with precondition: [V>=2,V2>=1,Out>=5,2*V2+4>=Out] 

* Chain [70,102]: 1*s(271)+6
  Such that:s(271) =< V

  with precondition: [V2>=1,Out>=4,V+6>=2*Out] 

* Chain [70,101]: 1*s(271)+6
  Such that:s(271) =< V

  with precondition: [V2>=1,Out>=5,V+8>=2*Out] 

* Chain [70,100]: 39*s(42)+1*s(271)+6
  Such that:s(271) =< V
aux(44) =< V2+1
s(42) =< aux(44)

  with precondition: [V>=2,V2>=1,Out>=5,V+2*V2+8>=2*Out] 

* Chain [69,102]: 6
  with precondition: [Out=3,V>=2,V2>=1] 

* Chain [69,101]: 6
  with precondition: [Out=4,V>=2,V2>=1] 

* Chain [69,100]: 39*s(42)+6
  Such that:aux(44) =< V2
s(42) =< aux(44)

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

* Chain [68,102]: 9
  with precondition: [5>=Out,V>=2,V2>=1,Out>=4] 

* Chain [68,101]: 9
  with precondition: [6>=Out,V>=2,V2>=1,Out>=5] 

* Chain [68,100]: 39*s(42)+9
  Such that:aux(44) =< V2
s(42) =< aux(44)

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

* Chain [67,102]: 1*s(274)+6
  Such that:s(274) =< 2*Out

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

* Chain [67,101]: 1*s(274)+6
  Such that:s(274) =< 2*Out

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

* Chain [67,100]: 39*s(42)+1*s(274)+6
  Such that:s(274) =< V+1
aux(44) =< V2
s(42) =< aux(44)

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

* Chain [66,102]: 1*s(275)+6
  Such that:s(275) =< V2

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

* Chain [66,101]: 1*s(275)+6
  Such that:s(275) =< V2

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

* Chain [66,100]: 40*s(42)+6
  Such that:aux(342) =< V2
s(42) =< aux(342)

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

* Chain [65,102]: 1*s(276)+6
  Such that:s(276) =< V

  with precondition: [V2>=1,Out>=4,V+6>=2*Out] 

* Chain [65,101]: 1*s(276)+6
  Such that:s(276) =< V

  with precondition: [V2>=1,Out>=5,V+8>=2*Out] 

* Chain [65,100]: 39*s(42)+1*s(276)+6
  Such that:s(276) =< V
aux(44) =< V2
s(42) =< aux(44)

  with precondition: [V>=2,V2>=1,Out>=5,V+2*V2+6>=2*Out] 


#### Cost of chains of fun6(Out):
* Chain [104]: 1
  with precondition: [Out=0] 

* Chain [103]: 1
  with precondition: [Out=1] 


#### Cost of chains of logIter(V,V2,Out):
* Chain [[105,106,107,111],118]: 0
  with precondition: [Out=0,V>=2,V2>=0] 

* Chain [[105,106,107,111],116]: 0
  with precondition: [Out=0,V>=2,V2>=0] 

* Chain [[105,106,107,111],115]: 0
  with precondition: [V>=2,V2>=0,Out>=1,V+2*V2>=2*Out] 

* Chain [[105,106,107,111],114]: 0
  with precondition: [V>=2,V2>=0,Out>=0,V+2*V2>=2*Out+2] 

* Chain [[105,106,107,111],113]: 0
  with precondition: [Out=0,V>=2,V2>=0] 

* Chain [[105,106,107,111],112,118]: 0
  with precondition: [Out=0,V>=4,V2>=0] 

* Chain [[105,106,107,111],112,117]: 0
  with precondition: [Out=1,V>=4,V2>=0] 

* Chain [[105,106,107,111],110,118]: 0
  with precondition: [Out=0,V>=4,V2>=0] 

* Chain [[105,106,107,111],110,117]: 0
  with precondition: [Out=1,V>=4,V2>=0] 

* Chain [[105,106,107,111],110,113]: 0
  with precondition: [Out=0,V>=4,V2>=0] 

* Chain [[105,106,107,111],109,118]: 0
  with precondition: [Out=0,V>=4,V2>=0] 

* Chain [[105,106,107,111],109,117]: 0
  with precondition: [Out=1,V>=4,V2>=0] 

* Chain [[105,106,107,111],108,118]: 0
  with precondition: [Out=0,V>=4,V2>=0] 

* Chain [[105,106,107,111],108,117]: 0
  with precondition: [Out=1,V>=4,V2>=0] 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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


#### Cost of chains of logarithm(V,Out):
* Chain [122]: 0
  with precondition: [V=0,Out=1] 

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

* Chain [120]: 0
  with precondition: [Out>=0,V>=2*Out+2] 

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


#### Cost of chains of start(V,V2,V18,V21):
* Chain [123]: 6*s(1646)+248*s(1648)+1257*s(1653)+398*s(1654)+35*s(1678)+290*s(1679)+198*s(1681)+235*s(1683)+174*s(1684)+2958*s(1685)+522*s(1686)+279*s(1687)+58*s(1690)+58*s(1691)+58*s(1692)+2*s(1693)+30*s(1694)+15*s(1695)+255*s(1696)+45*s(1697)+20*s(1698)+20*s(1699)+5*s(1700)+5*s(1701)+5*s(1702)+33*s(1703)+78*s(1704)+18*s(1705)+9*s(1706)+153*s(1707)+27*s(1708)+12*s(1709)+12*s(1710)+3*s(1711)+3*s(1712)+3*s(1713)+3*s(1714)+4*s(1715)+30*s(1716)+15*s(1717)+255*s(1718)+45*s(1719)+20*s(1720)+20*s(1721)+5*s(1722)+5*s(1723)+5*s(1724)+39*s(1725)+1*s(1726)+39*s(1727)+5*s(1730)+1*s(1733)+4*s(1739)+71*s(1744)+798*s(1745)+199*s(1746)+249*s(1747)+290*s(1778)+470*s(1782)+348*s(1783)+5916*s(1784)+1044*s(1785)+558*s(1786)+58*s(1789)+58*s(1790)+58*s(1791)+4*s(1792)+60*s(1793)+30*s(1794)+510*s(1795)+90*s(1796)+40*s(1797)+40*s(1798)+5*s(1799)+5*s(1800)+5*s(1801)+66*s(1802)+78*s(1803)+36*s(1804)+18*s(1805)+306*s(1806)+54*s(1807)+24*s(1808)+24*s(1809)+3*s(1810)+3*s(1811)+3*s(1812)+6*s(1813)+8*s(1814)+60*s(1815)+30*s(1816)+510*s(1817)+90*s(1818)+40*s(1819)+40*s(1820)+5*s(1821)+5*s(1822)+5*s(1823)+39*s(1824)+2*s(1825)+39*s(1826)+10*s(1829)+2*s(1832)+8*s(1838)+290*s(1876)+58*s(1887)+58*s(1888)+58*s(1889)+5*s(1897)+5*s(1898)+5*s(1899)+78*s(1901)+3*s(1908)+3*s(1909)+3*s(1910)+5*s(1919)+5*s(1920)+5*s(1921)+39*s(1922)+39*s(1924)+51
  Such that:s(1860) =< V+V2
s(1771) =< V/2
s(1755) =< V/2+1
s(1772) =< V/2+2
s(1756) =< V/2+3
s(1869) =< V/2+V2
s(1853) =< V/2+V2+1
s(1870) =< V/2+V2+2
s(1854) =< V/2+V2+3
s(1733) =< V18+8
s(1663) =< V18+V21
s(1664) =< 2*V18
s(1665) =< 2*V18+2
s(1666) =< 2*V18+14
s(1667) =< 2*V18+18
s(1668) =< 3*V18
s(1669) =< 3*V18+3
s(1670) =< 3*V18+21
s(1671) =< 3*V18+27
s(1672) =< V18/2+V21
s(1656) =< V18/2+V21+1
s(1673) =< V18/2+V21+2
s(1657) =< V18/2+V21+3
s(1674) =< 2/3*V18
s(1676) =< V21+1
aux(391) =< 1
aux(392) =< 2
aux(393) =< V
aux(394) =< V+1
aux(395) =< V+7
aux(396) =< V+8
aux(397) =< V+9
aux(398) =< 2*V
aux(399) =< 2*V+2
aux(400) =< 2*V+14
aux(401) =< 2*V+18
aux(402) =< 3*V
aux(403) =< 3*V+3
aux(404) =< 3*V+21
aux(405) =< 3*V+27
aux(406) =< 2/3*V
aux(407) =< V2
aux(408) =< V2+1
aux(409) =< V18
aux(410) =< V18+1
aux(411) =< V18+7
aux(412) =< V18+9
aux(413) =< V21
s(1646) =< aux(392)
s(1745) =< aux(393)
s(1744) =< aux(394)
s(1832) =< aux(396)
s(1747) =< aux(407)
s(1746) =< aux(408)
s(1654) =< aux(409)
s(1653) =< aux(391)
s(1678) =< aux(410)
s(1679) =< s(1672)
s(1648) =< aux(413)
s(1681) =< s(1676)
s(1683) =< s(1668)
s(1684) =< aux(409)
s(1685) =< aux(409)
s(1686) =< aux(409)
s(1684) =< s(1664)
s(1685) =< s(1664)
s(1686) =< s(1664)
s(1687) =< s(1664)
s(1685) =< s(1668)
s(1686) =< s(1668)
s(1684) =< s(1674)
s(1686) =< s(1674)
s(1688) =< s(1663)
s(1689) =< s(1663)+1
s(1690) =< s(1654)*s(1663)
s(1691) =< s(1685)*s(1689)
s(1692) =< s(1685)+s(1685)+s(1686)+s(1685)+s(1685)+s(1685)+s(1686)+s(1685)+s(1685)+aux(413)
s(1692) =< s(1685)*s(1688)
s(1693) =< s(1671)
s(1694) =< aux(409)
s(1695) =< aux(409)
s(1696) =< aux(409)
s(1697) =< aux(409)
s(1694) =< aux(412)
s(1695) =< aux(412)
s(1696) =< aux(412)
s(1697) =< aux(412)
s(1695) =< s(1664)
s(1696) =< s(1664)
s(1697) =< s(1664)
s(1698) =< s(1664)
s(1695) =< s(1667)
s(1696) =< s(1667)
s(1697) =< s(1667)
s(1698) =< s(1667)
s(1696) =< s(1668)
s(1697) =< s(1668)
s(1699) =< s(1668)
s(1696) =< s(1671)
s(1697) =< s(1671)
s(1699) =< s(1671)
s(1695) =< s(1674)
s(1697) =< s(1674)
s(1700) =< s(1694)*s(1663)
s(1701) =< s(1696)*s(1689)
s(1702) =< s(1696)+s(1696)+s(1697)+s(1696)+s(1696)+s(1696)+s(1697)+s(1696)+s(1696)+aux(413)
s(1702) =< s(1696)*s(1688)
s(1703) =< s(1665)
s(1704) =< s(1673)
s(1705) =< aux(409)
s(1706) =< aux(409)
s(1707) =< aux(409)
s(1708) =< aux(409)
s(1705) =< aux(410)
s(1706) =< aux(410)
s(1707) =< aux(410)
s(1708) =< aux(410)
s(1706) =< s(1664)
s(1707) =< s(1664)
s(1708) =< s(1664)
s(1709) =< s(1664)
s(1706) =< s(1665)
s(1707) =< s(1665)
s(1708) =< s(1665)
s(1709) =< s(1665)
s(1707) =< s(1668)
s(1708) =< s(1668)
s(1710) =< s(1668)
s(1707) =< s(1669)
s(1708) =< s(1669)
s(1710) =< s(1669)
s(1706) =< s(1674)
s(1708) =< s(1674)
s(1711) =< s(1705)*s(1663)
s(1712) =< s(1707)*s(1689)
s(1713) =< s(1707)+s(1707)+s(1708)+s(1707)+s(1707)+s(1707)+s(1708)+s(1707)+s(1707)+aux(413)
s(1713) =< s(1707)*s(1688)
s(1714) =< s(1667)
s(1715) =< s(1666)
s(1716) =< aux(409)
s(1717) =< aux(409)
s(1718) =< aux(409)
s(1719) =< aux(409)
s(1716) =< aux(411)
s(1717) =< aux(411)
s(1718) =< aux(411)
s(1719) =< aux(411)
s(1717) =< s(1664)
s(1718) =< s(1664)
s(1719) =< s(1664)
s(1720) =< s(1664)
s(1717) =< s(1666)
s(1718) =< s(1666)
s(1719) =< s(1666)
s(1720) =< s(1666)
s(1718) =< s(1668)
s(1719) =< s(1668)
s(1721) =< s(1668)
s(1718) =< s(1670)
s(1719) =< s(1670)
s(1721) =< s(1670)
s(1717) =< s(1674)
s(1719) =< s(1674)
s(1722) =< s(1716)*s(1663)
s(1723) =< s(1718)*s(1689)
s(1724) =< s(1718)+s(1718)+s(1719)+s(1718)+s(1718)+s(1718)+s(1719)+s(1718)+s(1718)+aux(413)
s(1724) =< s(1718)*s(1688)
s(1725) =< s(1657)
s(1726) =< s(1670)
s(1727) =< s(1656)
s(1730) =< aux(412)
s(1829) =< aux(397)
s(1876) =< s(1869)
s(1782) =< aux(402)
s(1783) =< aux(393)
s(1784) =< aux(393)
s(1785) =< aux(393)
s(1783) =< aux(398)
s(1784) =< aux(398)
s(1785) =< aux(398)
s(1786) =< aux(398)
s(1784) =< aux(402)
s(1785) =< aux(402)
s(1783) =< aux(406)
s(1785) =< aux(406)
s(1885) =< s(1860)
s(1886) =< s(1860)+1
s(1887) =< s(1745)*s(1860)
s(1888) =< s(1784)*s(1886)
s(1889) =< s(1784)+s(1784)+s(1785)+s(1784)+s(1784)+s(1784)+s(1785)+s(1784)+s(1784)+aux(407)
s(1889) =< s(1784)*s(1885)
s(1792) =< aux(405)
s(1793) =< aux(393)
s(1794) =< aux(393)
s(1795) =< aux(393)
s(1796) =< aux(393)
s(1793) =< aux(397)
s(1794) =< aux(397)
s(1795) =< aux(397)
s(1796) =< aux(397)
s(1794) =< aux(398)
s(1795) =< aux(398)
s(1796) =< aux(398)
s(1797) =< aux(398)
s(1794) =< aux(401)
s(1795) =< aux(401)
s(1796) =< aux(401)
s(1797) =< aux(401)
s(1795) =< aux(402)
s(1796) =< aux(402)
s(1798) =< aux(402)
s(1795) =< aux(405)
s(1796) =< aux(405)
s(1798) =< aux(405)
s(1794) =< aux(406)
s(1796) =< aux(406)
s(1897) =< s(1793)*s(1860)
s(1898) =< s(1795)*s(1886)
s(1899) =< s(1795)+s(1795)+s(1796)+s(1795)+s(1795)+s(1795)+s(1796)+s(1795)+s(1795)+aux(407)
s(1899) =< s(1795)*s(1885)
s(1802) =< aux(399)
s(1901) =< s(1870)
s(1804) =< aux(393)
s(1805) =< aux(393)
s(1806) =< aux(393)
s(1807) =< aux(393)
s(1804) =< aux(394)
s(1805) =< aux(394)
s(1806) =< aux(394)
s(1807) =< aux(394)
s(1805) =< aux(398)
s(1806) =< aux(398)
s(1807) =< aux(398)
s(1808) =< aux(398)
s(1805) =< aux(399)
s(1806) =< aux(399)
s(1807) =< aux(399)
s(1808) =< aux(399)
s(1806) =< aux(402)
s(1807) =< aux(402)
s(1809) =< aux(402)
s(1806) =< aux(403)
s(1807) =< aux(403)
s(1809) =< aux(403)
s(1805) =< aux(406)
s(1807) =< aux(406)
s(1908) =< s(1804)*s(1860)
s(1909) =< s(1806)*s(1886)
s(1910) =< s(1806)+s(1806)+s(1807)+s(1806)+s(1806)+s(1806)+s(1807)+s(1806)+s(1806)+aux(407)
s(1910) =< s(1806)*s(1885)
s(1813) =< aux(401)
s(1814) =< aux(400)
s(1815) =< aux(393)
s(1816) =< aux(393)
s(1817) =< aux(393)
s(1818) =< aux(393)
s(1815) =< aux(395)
s(1816) =< aux(395)
s(1817) =< aux(395)
s(1818) =< aux(395)
s(1816) =< aux(398)
s(1817) =< aux(398)
s(1818) =< aux(398)
s(1819) =< aux(398)
s(1816) =< aux(400)
s(1817) =< aux(400)
s(1818) =< aux(400)
s(1819) =< aux(400)
s(1817) =< aux(402)
s(1818) =< aux(402)
s(1820) =< aux(402)
s(1817) =< aux(404)
s(1818) =< aux(404)
s(1820) =< aux(404)
s(1816) =< aux(406)
s(1818) =< aux(406)
s(1919) =< s(1815)*s(1860)
s(1920) =< s(1817)*s(1886)
s(1921) =< s(1817)+s(1817)+s(1818)+s(1817)+s(1817)+s(1817)+s(1818)+s(1817)+s(1817)+aux(407)
s(1921) =< s(1817)*s(1885)
s(1922) =< s(1854)
s(1825) =< aux(404)
s(1924) =< s(1853)
s(1778) =< s(1771)
s(1787) =< aux(393)
s(1788) =< aux(393)+1
s(1789) =< s(1745)*aux(393)
s(1790) =< s(1784)*s(1788)
s(1791) =< s(1784)+s(1784)+s(1785)+s(1784)+s(1784)+s(1784)+s(1785)+s(1784)+s(1784)
s(1791) =< s(1784)*s(1787)
s(1799) =< s(1793)*aux(393)
s(1800) =< s(1795)*s(1788)
s(1801) =< s(1795)+s(1795)+s(1796)+s(1795)+s(1795)+s(1795)+s(1796)+s(1795)+s(1795)
s(1801) =< s(1795)*s(1787)
s(1803) =< s(1772)
s(1810) =< s(1804)*aux(393)
s(1811) =< s(1806)*s(1788)
s(1812) =< s(1806)+s(1806)+s(1807)+s(1806)+s(1806)+s(1806)+s(1807)+s(1806)+s(1806)
s(1812) =< s(1806)*s(1787)
s(1821) =< s(1815)*aux(393)
s(1822) =< s(1817)*s(1788)
s(1823) =< s(1817)+s(1817)+s(1818)+s(1817)+s(1817)+s(1817)+s(1818)+s(1817)+s(1817)
s(1823) =< s(1817)*s(1787)
s(1824) =< s(1756)
s(1826) =< s(1755)
s(1838) =< aux(395)
s(1739) =< aux(411)

  with precondition: [] 


Closed-form bounds of start(V,V2,V18,V21): 
-------------------------------------
* Chain [123] with precondition: [] 
    - Upper bound: nat(V)*11320+1320+nat(V)*142*nat(V)+nat(V)*142*nat(V+V2)+nat(V2)*320+nat(V18)*5659+nat(V18)*142*nat(V18+V21)+nat(V21)*319+nat(2*V)*662+nat(2*V18)*331+nat(3*V)*574+nat(3*V18)*287+nat(V+1)*71+nat(V+7)*8+nat(V+8)*2+nat(V+9)*10+nat(V2+1)*199+nat(V18+1)*35+nat(V18+7)*4+nat(V18+8)+nat(V18+9)*5+nat(V21+1)*198+nat(2*V+2)*66+nat(2*V+14)*8+nat(2*V+18)*6+nat(2*V18+2)*33+nat(2*V18+14)*4+nat(2*V18+18)*3+nat(3*V+21)*2+nat(3*V+27)*4+nat(3*V18+21)+nat(3*V18+27)*2+nat(V/2+V2+1)*39+nat(V/2+V2+2)*78+nat(V/2+V2+3)*39+nat(V18/2+V21+1)*39+nat(V18/2+V21+2)*78+nat(V18/2+V21+3)*39+nat(V/2+V2)*290+nat(V/2+1)*39+nat(V/2+2)*78+nat(V/2+3)*39+nat(V18/2+V21)*290+nat(V/2)*290 
    - Complexity: n^2 

### Maximum cost of start(V,V2,V18,V21): nat(V)*11320+1320+nat(V)*142*nat(V)+nat(V)*142*nat(V+V2)+nat(V2)*320+nat(V18)*5659+nat(V18)*142*nat(V18+V21)+nat(V21)*319+nat(2*V)*662+nat(2*V18)*331+nat(3*V)*574+nat(3*V18)*287+nat(V+1)*71+nat(V+7)*8+nat(V+8)*2+nat(V+9)*10+nat(V2+1)*199+nat(V18+1)*35+nat(V18+7)*4+nat(V18+8)+nat(V18+9)*5+nat(V21+1)*198+nat(2*V+2)*66+nat(2*V+14)*8+nat(2*V+18)*6+nat(2*V18+2)*33+nat(2*V18+14)*4+nat(2*V18+18)*3+nat(3*V+21)*2+nat(3*V+27)*4+nat(3*V18+21)+nat(3*V18+27)*2+nat(V/2+V2+1)*39+nat(V/2+V2+2)*78+nat(V/2+V2+3)*39+nat(V18/2+V21+1)*39+nat(V18/2+V21+2)*78+nat(V18/2+V21+3)*39+nat(V/2+V2)*290+nat(V/2+1)*39+nat(V/2+2)*78+nat(V/2+3)*39+nat(V18/2+V21)*290+nat(V/2)*290 
Asymptotic class: n^2 
* Total analysis performed in 15120 ms.


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

(12)
BOUNDS(1, n^2)

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

(13) RenamingProof (BOTH BOUNDS(ID, ID))
Renamed function symbols to avoid clashes with predefined symbol.
----------------------------------------

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


The TRS R consists of the following rules:

   HALF(0') -> c
   HALF(s(0')) -> c1
   HALF(s(s(z0))) -> c2(HALF(z0))
   LE(0', z0) -> c3
   LE(s(z0), 0') -> c4
   LE(s(z0), s(z1)) -> c5(LE(z0, z1))
   INC(s(z0)) -> c6(INC(z0))
   INC(0') -> c7
   LOGARITHM(z0) -> c8(LOGITER(z0, 0'))
   LOGITER(z0, z1) -> c9(IF(le(s(0'), z0), le(s(s(0')), z0), half(z0), inc(z1)), LE(s(0'), z0))
   LOGITER(z0, z1) -> c10(IF(le(s(0'), z0), le(s(s(0')), z0), half(z0), inc(z1)), LE(s(s(0')), z0))
   LOGITER(z0, z1) -> c11(IF(le(s(0'), z0), le(s(s(0')), z0), half(z0), inc(z1)), HALF(z0))
   LOGITER(z0, z1) -> c12(IF(le(s(0'), z0), le(s(s(0')), z0), half(z0), inc(z1)), INC(z1))
   IF(false, z0, z1, z2) -> c13
   IF(true, false, z0, s(z1)) -> c14
   IF(true, true, z0, z1) -> c15(LOGITER(z0, z1))
   F -> c16
   F -> c17

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

   half(0') -> 0'
   half(s(0')) -> 0'
   half(s(s(z0))) -> s(half(z0))
   le(0', z0) -> true
   le(s(z0), 0') -> false
   le(s(z0), s(z1)) -> le(z0, z1)
   inc(s(z0)) -> s(inc(z0))
   inc(0') -> s(0')
   logarithm(z0) -> logIter(z0, 0')
   logIter(z0, z1) -> if(le(s(0'), z0), le(s(s(0')), z0), half(z0), inc(z1))
   if(false, z0, z1, z2) -> logZeroError
   if(true, false, z0, s(z1)) -> z1
   if(true, true, z0, z1) -> logIter(z0, z1)
   f -> g
   f -> h

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

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

(16)
Obligation:
Innermost TRS:
Rules:
HALF(0') -> c
HALF(s(0')) -> c1
HALF(s(s(z0))) -> c2(HALF(z0))
LE(0', z0) -> c3
LE(s(z0), 0') -> c4
LE(s(z0), s(z1)) -> c5(LE(z0, z1))
INC(s(z0)) -> c6(INC(z0))
INC(0') -> c7
LOGARITHM(z0) -> c8(LOGITER(z0, 0'))
LOGITER(z0, z1) -> c9(IF(le(s(0'), z0), le(s(s(0')), z0), half(z0), inc(z1)), LE(s(0'), z0))
LOGITER(z0, z1) -> c10(IF(le(s(0'), z0), le(s(s(0')), z0), half(z0), inc(z1)), LE(s(s(0')), z0))
LOGITER(z0, z1) -> c11(IF(le(s(0'), z0), le(s(s(0')), z0), half(z0), inc(z1)), HALF(z0))
LOGITER(z0, z1) -> c12(IF(le(s(0'), z0), le(s(s(0')), z0), half(z0), inc(z1)), INC(z1))
IF(false, z0, z1, z2) -> c13
IF(true, false, z0, s(z1)) -> c14
IF(true, true, z0, z1) -> c15(LOGITER(z0, z1))
F -> c16
F -> c17
half(0') -> 0'
half(s(0')) -> 0'
half(s(s(z0))) -> s(half(z0))
le(0', z0) -> true
le(s(z0), 0') -> false
le(s(z0), s(z1)) -> le(z0, z1)
inc(s(z0)) -> s(inc(z0))
inc(0') -> s(0')
logarithm(z0) -> logIter(z0, 0')
logIter(z0, z1) -> if(le(s(0'), z0), le(s(s(0')), z0), half(z0), inc(z1))
if(false, z0, z1, z2) -> logZeroError
if(true, false, z0, s(z1)) -> z1
if(true, true, z0, z1) -> logIter(z0, z1)
f -> g
f -> h

Types:
HALF :: 0':s:logZeroError -> c:c1:c2
0' :: 0':s:logZeroError
c :: c:c1:c2
s :: 0':s:logZeroError -> 0':s:logZeroError
c1 :: c:c1:c2
c2 :: c:c1:c2 -> c:c1:c2
LE :: 0':s:logZeroError -> 0':s:logZeroError -> c3:c4:c5
c3 :: c3:c4:c5
c4 :: c3:c4:c5
c5 :: c3:c4:c5 -> c3:c4:c5
INC :: 0':s:logZeroError -> c6:c7
c6 :: c6:c7 -> c6:c7
c7 :: c6:c7
LOGARITHM :: 0':s:logZeroError -> c8
c8 :: c9:c10:c11:c12 -> c8
LOGITER :: 0':s:logZeroError -> 0':s:logZeroError -> c9:c10:c11:c12
c9 :: c13:c14:c15 -> c3:c4:c5 -> c9:c10:c11:c12
IF :: false:true -> false:true -> 0':s:logZeroError -> 0':s:logZeroError -> c13:c14:c15
le :: 0':s:logZeroError -> 0':s:logZeroError -> false:true
half :: 0':s:logZeroError -> 0':s:logZeroError
inc :: 0':s:logZeroError -> 0':s:logZeroError
c10 :: c13:c14:c15 -> c3:c4:c5 -> c9:c10:c11:c12
c11 :: c13:c14:c15 -> c:c1:c2 -> c9:c10:c11:c12
c12 :: c13:c14:c15 -> c6:c7 -> c9:c10:c11:c12
false :: false:true
c13 :: c13:c14:c15
true :: false:true
c14 :: c13:c14:c15
c15 :: c9:c10:c11:c12 -> c13:c14:c15
F :: c16:c17
c16 :: c16:c17
c17 :: c16:c17
logarithm :: 0':s:logZeroError -> 0':s:logZeroError
logIter :: 0':s:logZeroError -> 0':s:logZeroError -> 0':s:logZeroError
if :: false:true -> false:true -> 0':s:logZeroError -> 0':s:logZeroError -> 0':s:logZeroError
logZeroError :: 0':s:logZeroError
f :: g:h
g :: g:h
h :: g:h
hole_c:c1:c21_18 :: c:c1:c2
hole_0':s:logZeroError2_18 :: 0':s:logZeroError
hole_c3:c4:c53_18 :: c3:c4:c5
hole_c6:c74_18 :: c6:c7
hole_c85_18 :: c8
hole_c9:c10:c11:c126_18 :: c9:c10:c11:c12
hole_c13:c14:c157_18 :: c13:c14:c15
hole_false:true8_18 :: false:true
hole_c16:c179_18 :: c16:c17
hole_g:h10_18 :: g:h
gen_c:c1:c211_18 :: Nat -> c:c1:c2
gen_0':s:logZeroError12_18 :: Nat -> 0':s:logZeroError
gen_c3:c4:c513_18 :: Nat -> c3:c4:c5
gen_c6:c714_18 :: Nat -> c6:c7

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

(17) OrderProof (LOWER BOUND(ID))
Heuristically decided to analyse the following defined symbols:
HALF, LE, INC, LOGITER, le, half, inc, logIter

They will be analysed ascendingly in the following order:
HALF < LOGITER
LE < LOGITER
INC < LOGITER
le < LOGITER
half < LOGITER
inc < LOGITER
le < logIter
half < logIter
inc < logIter

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

(18)
Obligation:
Innermost TRS:
Rules:
HALF(0') -> c
HALF(s(0')) -> c1
HALF(s(s(z0))) -> c2(HALF(z0))
LE(0', z0) -> c3
LE(s(z0), 0') -> c4
LE(s(z0), s(z1)) -> c5(LE(z0, z1))
INC(s(z0)) -> c6(INC(z0))
INC(0') -> c7
LOGARITHM(z0) -> c8(LOGITER(z0, 0'))
LOGITER(z0, z1) -> c9(IF(le(s(0'), z0), le(s(s(0')), z0), half(z0), inc(z1)), LE(s(0'), z0))
LOGITER(z0, z1) -> c10(IF(le(s(0'), z0), le(s(s(0')), z0), half(z0), inc(z1)), LE(s(s(0')), z0))
LOGITER(z0, z1) -> c11(IF(le(s(0'), z0), le(s(s(0')), z0), half(z0), inc(z1)), HALF(z0))
LOGITER(z0, z1) -> c12(IF(le(s(0'), z0), le(s(s(0')), z0), half(z0), inc(z1)), INC(z1))
IF(false, z0, z1, z2) -> c13
IF(true, false, z0, s(z1)) -> c14
IF(true, true, z0, z1) -> c15(LOGITER(z0, z1))
F -> c16
F -> c17
half(0') -> 0'
half(s(0')) -> 0'
half(s(s(z0))) -> s(half(z0))
le(0', z0) -> true
le(s(z0), 0') -> false
le(s(z0), s(z1)) -> le(z0, z1)
inc(s(z0)) -> s(inc(z0))
inc(0') -> s(0')
logarithm(z0) -> logIter(z0, 0')
logIter(z0, z1) -> if(le(s(0'), z0), le(s(s(0')), z0), half(z0), inc(z1))
if(false, z0, z1, z2) -> logZeroError
if(true, false, z0, s(z1)) -> z1
if(true, true, z0, z1) -> logIter(z0, z1)
f -> g
f -> h

Types:
HALF :: 0':s:logZeroError -> c:c1:c2
0' :: 0':s:logZeroError
c :: c:c1:c2
s :: 0':s:logZeroError -> 0':s:logZeroError
c1 :: c:c1:c2
c2 :: c:c1:c2 -> c:c1:c2
LE :: 0':s:logZeroError -> 0':s:logZeroError -> c3:c4:c5
c3 :: c3:c4:c5
c4 :: c3:c4:c5
c5 :: c3:c4:c5 -> c3:c4:c5
INC :: 0':s:logZeroError -> c6:c7
c6 :: c6:c7 -> c6:c7
c7 :: c6:c7
LOGARITHM :: 0':s:logZeroError -> c8
c8 :: c9:c10:c11:c12 -> c8
LOGITER :: 0':s:logZeroError -> 0':s:logZeroError -> c9:c10:c11:c12
c9 :: c13:c14:c15 -> c3:c4:c5 -> c9:c10:c11:c12
IF :: false:true -> false:true -> 0':s:logZeroError -> 0':s:logZeroError -> c13:c14:c15
le :: 0':s:logZeroError -> 0':s:logZeroError -> false:true
half :: 0':s:logZeroError -> 0':s:logZeroError
inc :: 0':s:logZeroError -> 0':s:logZeroError
c10 :: c13:c14:c15 -> c3:c4:c5 -> c9:c10:c11:c12
c11 :: c13:c14:c15 -> c:c1:c2 -> c9:c10:c11:c12
c12 :: c13:c14:c15 -> c6:c7 -> c9:c10:c11:c12
false :: false:true
c13 :: c13:c14:c15
true :: false:true
c14 :: c13:c14:c15
c15 :: c9:c10:c11:c12 -> c13:c14:c15
F :: c16:c17
c16 :: c16:c17
c17 :: c16:c17
logarithm :: 0':s:logZeroError -> 0':s:logZeroError
logIter :: 0':s:logZeroError -> 0':s:logZeroError -> 0':s:logZeroError
if :: false:true -> false:true -> 0':s:logZeroError -> 0':s:logZeroError -> 0':s:logZeroError
logZeroError :: 0':s:logZeroError
f :: g:h
g :: g:h
h :: g:h
hole_c:c1:c21_18 :: c:c1:c2
hole_0':s:logZeroError2_18 :: 0':s:logZeroError
hole_c3:c4:c53_18 :: c3:c4:c5
hole_c6:c74_18 :: c6:c7
hole_c85_18 :: c8
hole_c9:c10:c11:c126_18 :: c9:c10:c11:c12
hole_c13:c14:c157_18 :: c13:c14:c15
hole_false:true8_18 :: false:true
hole_c16:c179_18 :: c16:c17
hole_g:h10_18 :: g:h
gen_c:c1:c211_18 :: Nat -> c:c1:c2
gen_0':s:logZeroError12_18 :: Nat -> 0':s:logZeroError
gen_c3:c4:c513_18 :: Nat -> c3:c4:c5
gen_c6:c714_18 :: Nat -> c6:c7


Generator Equations:
gen_c:c1:c211_18(0) <=> c
gen_c:c1:c211_18(+(x, 1)) <=> c2(gen_c:c1:c211_18(x))
gen_0':s:logZeroError12_18(0) <=> 0'
gen_0':s:logZeroError12_18(+(x, 1)) <=> s(gen_0':s:logZeroError12_18(x))
gen_c3:c4:c513_18(0) <=> c3
gen_c3:c4:c513_18(+(x, 1)) <=> c5(gen_c3:c4:c513_18(x))
gen_c6:c714_18(0) <=> c7
gen_c6:c714_18(+(x, 1)) <=> c6(gen_c6:c714_18(x))


The following defined symbols remain to be analysed:
HALF, LE, INC, LOGITER, le, half, inc, logIter

They will be analysed ascendingly in the following order:
HALF < LOGITER
LE < LOGITER
INC < LOGITER
le < LOGITER
half < LOGITER
inc < LOGITER
le < logIter
half < logIter
inc < logIter

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

(19) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
HALF(gen_0':s:logZeroError12_18(*(2, n16_18))) -> gen_c:c1:c211_18(n16_18), rt in Omega(1 + n16_18)

Induction Base:
HALF(gen_0':s:logZeroError12_18(*(2, 0))) ->_R^Omega(1)
c

Induction Step:
HALF(gen_0':s:logZeroError12_18(*(2, +(n16_18, 1)))) ->_R^Omega(1)
c2(HALF(gen_0':s:logZeroError12_18(*(2, n16_18)))) ->_IH
c2(gen_c:c1:c211_18(c17_18))

We have rt in Omega(n^1) and sz in O(n). Thus, we have irc_R in Omega(n).
----------------------------------------

(20)
Complex Obligation (BEST)

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

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

Innermost TRS:
Rules:
HALF(0') -> c
HALF(s(0')) -> c1
HALF(s(s(z0))) -> c2(HALF(z0))
LE(0', z0) -> c3
LE(s(z0), 0') -> c4
LE(s(z0), s(z1)) -> c5(LE(z0, z1))
INC(s(z0)) -> c6(INC(z0))
INC(0') -> c7
LOGARITHM(z0) -> c8(LOGITER(z0, 0'))
LOGITER(z0, z1) -> c9(IF(le(s(0'), z0), le(s(s(0')), z0), half(z0), inc(z1)), LE(s(0'), z0))
LOGITER(z0, z1) -> c10(IF(le(s(0'), z0), le(s(s(0')), z0), half(z0), inc(z1)), LE(s(s(0')), z0))
LOGITER(z0, z1) -> c11(IF(le(s(0'), z0), le(s(s(0')), z0), half(z0), inc(z1)), HALF(z0))
LOGITER(z0, z1) -> c12(IF(le(s(0'), z0), le(s(s(0')), z0), half(z0), inc(z1)), INC(z1))
IF(false, z0, z1, z2) -> c13
IF(true, false, z0, s(z1)) -> c14
IF(true, true, z0, z1) -> c15(LOGITER(z0, z1))
F -> c16
F -> c17
half(0') -> 0'
half(s(0')) -> 0'
half(s(s(z0))) -> s(half(z0))
le(0', z0) -> true
le(s(z0), 0') -> false
le(s(z0), s(z1)) -> le(z0, z1)
inc(s(z0)) -> s(inc(z0))
inc(0') -> s(0')
logarithm(z0) -> logIter(z0, 0')
logIter(z0, z1) -> if(le(s(0'), z0), le(s(s(0')), z0), half(z0), inc(z1))
if(false, z0, z1, z2) -> logZeroError
if(true, false, z0, s(z1)) -> z1
if(true, true, z0, z1) -> logIter(z0, z1)
f -> g
f -> h

Types:
HALF :: 0':s:logZeroError -> c:c1:c2
0' :: 0':s:logZeroError
c :: c:c1:c2
s :: 0':s:logZeroError -> 0':s:logZeroError
c1 :: c:c1:c2
c2 :: c:c1:c2 -> c:c1:c2
LE :: 0':s:logZeroError -> 0':s:logZeroError -> c3:c4:c5
c3 :: c3:c4:c5
c4 :: c3:c4:c5
c5 :: c3:c4:c5 -> c3:c4:c5
INC :: 0':s:logZeroError -> c6:c7
c6 :: c6:c7 -> c6:c7
c7 :: c6:c7
LOGARITHM :: 0':s:logZeroError -> c8
c8 :: c9:c10:c11:c12 -> c8
LOGITER :: 0':s:logZeroError -> 0':s:logZeroError -> c9:c10:c11:c12
c9 :: c13:c14:c15 -> c3:c4:c5 -> c9:c10:c11:c12
IF :: false:true -> false:true -> 0':s:logZeroError -> 0':s:logZeroError -> c13:c14:c15
le :: 0':s:logZeroError -> 0':s:logZeroError -> false:true
half :: 0':s:logZeroError -> 0':s:logZeroError
inc :: 0':s:logZeroError -> 0':s:logZeroError
c10 :: c13:c14:c15 -> c3:c4:c5 -> c9:c10:c11:c12
c11 :: c13:c14:c15 -> c:c1:c2 -> c9:c10:c11:c12
c12 :: c13:c14:c15 -> c6:c7 -> c9:c10:c11:c12
false :: false:true
c13 :: c13:c14:c15
true :: false:true
c14 :: c13:c14:c15
c15 :: c9:c10:c11:c12 -> c13:c14:c15
F :: c16:c17
c16 :: c16:c17
c17 :: c16:c17
logarithm :: 0':s:logZeroError -> 0':s:logZeroError
logIter :: 0':s:logZeroError -> 0':s:logZeroError -> 0':s:logZeroError
if :: false:true -> false:true -> 0':s:logZeroError -> 0':s:logZeroError -> 0':s:logZeroError
logZeroError :: 0':s:logZeroError
f :: g:h
g :: g:h
h :: g:h
hole_c:c1:c21_18 :: c:c1:c2
hole_0':s:logZeroError2_18 :: 0':s:logZeroError
hole_c3:c4:c53_18 :: c3:c4:c5
hole_c6:c74_18 :: c6:c7
hole_c85_18 :: c8
hole_c9:c10:c11:c126_18 :: c9:c10:c11:c12
hole_c13:c14:c157_18 :: c13:c14:c15
hole_false:true8_18 :: false:true
hole_c16:c179_18 :: c16:c17
hole_g:h10_18 :: g:h
gen_c:c1:c211_18 :: Nat -> c:c1:c2
gen_0':s:logZeroError12_18 :: Nat -> 0':s:logZeroError
gen_c3:c4:c513_18 :: Nat -> c3:c4:c5
gen_c6:c714_18 :: Nat -> c6:c7


Generator Equations:
gen_c:c1:c211_18(0) <=> c
gen_c:c1:c211_18(+(x, 1)) <=> c2(gen_c:c1:c211_18(x))
gen_0':s:logZeroError12_18(0) <=> 0'
gen_0':s:logZeroError12_18(+(x, 1)) <=> s(gen_0':s:logZeroError12_18(x))
gen_c3:c4:c513_18(0) <=> c3
gen_c3:c4:c513_18(+(x, 1)) <=> c5(gen_c3:c4:c513_18(x))
gen_c6:c714_18(0) <=> c7
gen_c6:c714_18(+(x, 1)) <=> c6(gen_c6:c714_18(x))


The following defined symbols remain to be analysed:
HALF, LE, INC, LOGITER, le, half, inc, logIter

They will be analysed ascendingly in the following order:
HALF < LOGITER
LE < LOGITER
INC < LOGITER
le < LOGITER
half < LOGITER
inc < LOGITER
le < logIter
half < logIter
inc < logIter

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

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

(23)
BOUNDS(n^1, INF)

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

(24)
Obligation:
Innermost TRS:
Rules:
HALF(0') -> c
HALF(s(0')) -> c1
HALF(s(s(z0))) -> c2(HALF(z0))
LE(0', z0) -> c3
LE(s(z0), 0') -> c4
LE(s(z0), s(z1)) -> c5(LE(z0, z1))
INC(s(z0)) -> c6(INC(z0))
INC(0') -> c7
LOGARITHM(z0) -> c8(LOGITER(z0, 0'))
LOGITER(z0, z1) -> c9(IF(le(s(0'), z0), le(s(s(0')), z0), half(z0), inc(z1)), LE(s(0'), z0))
LOGITER(z0, z1) -> c10(IF(le(s(0'), z0), le(s(s(0')), z0), half(z0), inc(z1)), LE(s(s(0')), z0))
LOGITER(z0, z1) -> c11(IF(le(s(0'), z0), le(s(s(0')), z0), half(z0), inc(z1)), HALF(z0))
LOGITER(z0, z1) -> c12(IF(le(s(0'), z0), le(s(s(0')), z0), half(z0), inc(z1)), INC(z1))
IF(false, z0, z1, z2) -> c13
IF(true, false, z0, s(z1)) -> c14
IF(true, true, z0, z1) -> c15(LOGITER(z0, z1))
F -> c16
F -> c17
half(0') -> 0'
half(s(0')) -> 0'
half(s(s(z0))) -> s(half(z0))
le(0', z0) -> true
le(s(z0), 0') -> false
le(s(z0), s(z1)) -> le(z0, z1)
inc(s(z0)) -> s(inc(z0))
inc(0') -> s(0')
logarithm(z0) -> logIter(z0, 0')
logIter(z0, z1) -> if(le(s(0'), z0), le(s(s(0')), z0), half(z0), inc(z1))
if(false, z0, z1, z2) -> logZeroError
if(true, false, z0, s(z1)) -> z1
if(true, true, z0, z1) -> logIter(z0, z1)
f -> g
f -> h

Types:
HALF :: 0':s:logZeroError -> c:c1:c2
0' :: 0':s:logZeroError
c :: c:c1:c2
s :: 0':s:logZeroError -> 0':s:logZeroError
c1 :: c:c1:c2
c2 :: c:c1:c2 -> c:c1:c2
LE :: 0':s:logZeroError -> 0':s:logZeroError -> c3:c4:c5
c3 :: c3:c4:c5
c4 :: c3:c4:c5
c5 :: c3:c4:c5 -> c3:c4:c5
INC :: 0':s:logZeroError -> c6:c7
c6 :: c6:c7 -> c6:c7
c7 :: c6:c7
LOGARITHM :: 0':s:logZeroError -> c8
c8 :: c9:c10:c11:c12 -> c8
LOGITER :: 0':s:logZeroError -> 0':s:logZeroError -> c9:c10:c11:c12
c9 :: c13:c14:c15 -> c3:c4:c5 -> c9:c10:c11:c12
IF :: false:true -> false:true -> 0':s:logZeroError -> 0':s:logZeroError -> c13:c14:c15
le :: 0':s:logZeroError -> 0':s:logZeroError -> false:true
half :: 0':s:logZeroError -> 0':s:logZeroError
inc :: 0':s:logZeroError -> 0':s:logZeroError
c10 :: c13:c14:c15 -> c3:c4:c5 -> c9:c10:c11:c12
c11 :: c13:c14:c15 -> c:c1:c2 -> c9:c10:c11:c12
c12 :: c13:c14:c15 -> c6:c7 -> c9:c10:c11:c12
false :: false:true
c13 :: c13:c14:c15
true :: false:true
c14 :: c13:c14:c15
c15 :: c9:c10:c11:c12 -> c13:c14:c15
F :: c16:c17
c16 :: c16:c17
c17 :: c16:c17
logarithm :: 0':s:logZeroError -> 0':s:logZeroError
logIter :: 0':s:logZeroError -> 0':s:logZeroError -> 0':s:logZeroError
if :: false:true -> false:true -> 0':s:logZeroError -> 0':s:logZeroError -> 0':s:logZeroError
logZeroError :: 0':s:logZeroError
f :: g:h
g :: g:h
h :: g:h
hole_c:c1:c21_18 :: c:c1:c2
hole_0':s:logZeroError2_18 :: 0':s:logZeroError
hole_c3:c4:c53_18 :: c3:c4:c5
hole_c6:c74_18 :: c6:c7
hole_c85_18 :: c8
hole_c9:c10:c11:c126_18 :: c9:c10:c11:c12
hole_c13:c14:c157_18 :: c13:c14:c15
hole_false:true8_18 :: false:true
hole_c16:c179_18 :: c16:c17
hole_g:h10_18 :: g:h
gen_c:c1:c211_18 :: Nat -> c:c1:c2
gen_0':s:logZeroError12_18 :: Nat -> 0':s:logZeroError
gen_c3:c4:c513_18 :: Nat -> c3:c4:c5
gen_c6:c714_18 :: Nat -> c6:c7


Lemmas:
HALF(gen_0':s:logZeroError12_18(*(2, n16_18))) -> gen_c:c1:c211_18(n16_18), rt in Omega(1 + n16_18)


Generator Equations:
gen_c:c1:c211_18(0) <=> c
gen_c:c1:c211_18(+(x, 1)) <=> c2(gen_c:c1:c211_18(x))
gen_0':s:logZeroError12_18(0) <=> 0'
gen_0':s:logZeroError12_18(+(x, 1)) <=> s(gen_0':s:logZeroError12_18(x))
gen_c3:c4:c513_18(0) <=> c3
gen_c3:c4:c513_18(+(x, 1)) <=> c5(gen_c3:c4:c513_18(x))
gen_c6:c714_18(0) <=> c7
gen_c6:c714_18(+(x, 1)) <=> c6(gen_c6:c714_18(x))


The following defined symbols remain to be analysed:
LE, INC, LOGITER, le, half, inc, logIter

They will be analysed ascendingly in the following order:
LE < LOGITER
INC < LOGITER
le < LOGITER
half < LOGITER
inc < LOGITER
le < logIter
half < logIter
inc < logIter

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

(25) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
LE(gen_0':s:logZeroError12_18(n502_18), gen_0':s:logZeroError12_18(n502_18)) -> gen_c3:c4:c513_18(n502_18), rt in Omega(1 + n502_18)

Induction Base:
LE(gen_0':s:logZeroError12_18(0), gen_0':s:logZeroError12_18(0)) ->_R^Omega(1)
c3

Induction Step:
LE(gen_0':s:logZeroError12_18(+(n502_18, 1)), gen_0':s:logZeroError12_18(+(n502_18, 1))) ->_R^Omega(1)
c5(LE(gen_0':s:logZeroError12_18(n502_18), gen_0':s:logZeroError12_18(n502_18))) ->_IH
c5(gen_c3:c4:c513_18(c503_18))

We have rt in Omega(n^1) and sz in O(n). Thus, we have irc_R in Omega(n).
----------------------------------------

(26)
Obligation:
Innermost TRS:
Rules:
HALF(0') -> c
HALF(s(0')) -> c1
HALF(s(s(z0))) -> c2(HALF(z0))
LE(0', z0) -> c3
LE(s(z0), 0') -> c4
LE(s(z0), s(z1)) -> c5(LE(z0, z1))
INC(s(z0)) -> c6(INC(z0))
INC(0') -> c7
LOGARITHM(z0) -> c8(LOGITER(z0, 0'))
LOGITER(z0, z1) -> c9(IF(le(s(0'), z0), le(s(s(0')), z0), half(z0), inc(z1)), LE(s(0'), z0))
LOGITER(z0, z1) -> c10(IF(le(s(0'), z0), le(s(s(0')), z0), half(z0), inc(z1)), LE(s(s(0')), z0))
LOGITER(z0, z1) -> c11(IF(le(s(0'), z0), le(s(s(0')), z0), half(z0), inc(z1)), HALF(z0))
LOGITER(z0, z1) -> c12(IF(le(s(0'), z0), le(s(s(0')), z0), half(z0), inc(z1)), INC(z1))
IF(false, z0, z1, z2) -> c13
IF(true, false, z0, s(z1)) -> c14
IF(true, true, z0, z1) -> c15(LOGITER(z0, z1))
F -> c16
F -> c17
half(0') -> 0'
half(s(0')) -> 0'
half(s(s(z0))) -> s(half(z0))
le(0', z0) -> true
le(s(z0), 0') -> false
le(s(z0), s(z1)) -> le(z0, z1)
inc(s(z0)) -> s(inc(z0))
inc(0') -> s(0')
logarithm(z0) -> logIter(z0, 0')
logIter(z0, z1) -> if(le(s(0'), z0), le(s(s(0')), z0), half(z0), inc(z1))
if(false, z0, z1, z2) -> logZeroError
if(true, false, z0, s(z1)) -> z1
if(true, true, z0, z1) -> logIter(z0, z1)
f -> g
f -> h

Types:
HALF :: 0':s:logZeroError -> c:c1:c2
0' :: 0':s:logZeroError
c :: c:c1:c2
s :: 0':s:logZeroError -> 0':s:logZeroError
c1 :: c:c1:c2
c2 :: c:c1:c2 -> c:c1:c2
LE :: 0':s:logZeroError -> 0':s:logZeroError -> c3:c4:c5
c3 :: c3:c4:c5
c4 :: c3:c4:c5
c5 :: c3:c4:c5 -> c3:c4:c5
INC :: 0':s:logZeroError -> c6:c7
c6 :: c6:c7 -> c6:c7
c7 :: c6:c7
LOGARITHM :: 0':s:logZeroError -> c8
c8 :: c9:c10:c11:c12 -> c8
LOGITER :: 0':s:logZeroError -> 0':s:logZeroError -> c9:c10:c11:c12
c9 :: c13:c14:c15 -> c3:c4:c5 -> c9:c10:c11:c12
IF :: false:true -> false:true -> 0':s:logZeroError -> 0':s:logZeroError -> c13:c14:c15
le :: 0':s:logZeroError -> 0':s:logZeroError -> false:true
half :: 0':s:logZeroError -> 0':s:logZeroError
inc :: 0':s:logZeroError -> 0':s:logZeroError
c10 :: c13:c14:c15 -> c3:c4:c5 -> c9:c10:c11:c12
c11 :: c13:c14:c15 -> c:c1:c2 -> c9:c10:c11:c12
c12 :: c13:c14:c15 -> c6:c7 -> c9:c10:c11:c12
false :: false:true
c13 :: c13:c14:c15
true :: false:true
c14 :: c13:c14:c15
c15 :: c9:c10:c11:c12 -> c13:c14:c15
F :: c16:c17
c16 :: c16:c17
c17 :: c16:c17
logarithm :: 0':s:logZeroError -> 0':s:logZeroError
logIter :: 0':s:logZeroError -> 0':s:logZeroError -> 0':s:logZeroError
if :: false:true -> false:true -> 0':s:logZeroError -> 0':s:logZeroError -> 0':s:logZeroError
logZeroError :: 0':s:logZeroError
f :: g:h
g :: g:h
h :: g:h
hole_c:c1:c21_18 :: c:c1:c2
hole_0':s:logZeroError2_18 :: 0':s:logZeroError
hole_c3:c4:c53_18 :: c3:c4:c5
hole_c6:c74_18 :: c6:c7
hole_c85_18 :: c8
hole_c9:c10:c11:c126_18 :: c9:c10:c11:c12
hole_c13:c14:c157_18 :: c13:c14:c15
hole_false:true8_18 :: false:true
hole_c16:c179_18 :: c16:c17
hole_g:h10_18 :: g:h
gen_c:c1:c211_18 :: Nat -> c:c1:c2
gen_0':s:logZeroError12_18 :: Nat -> 0':s:logZeroError
gen_c3:c4:c513_18 :: Nat -> c3:c4:c5
gen_c6:c714_18 :: Nat -> c6:c7


Lemmas:
HALF(gen_0':s:logZeroError12_18(*(2, n16_18))) -> gen_c:c1:c211_18(n16_18), rt in Omega(1 + n16_18)
LE(gen_0':s:logZeroError12_18(n502_18), gen_0':s:logZeroError12_18(n502_18)) -> gen_c3:c4:c513_18(n502_18), rt in Omega(1 + n502_18)


Generator Equations:
gen_c:c1:c211_18(0) <=> c
gen_c:c1:c211_18(+(x, 1)) <=> c2(gen_c:c1:c211_18(x))
gen_0':s:logZeroError12_18(0) <=> 0'
gen_0':s:logZeroError12_18(+(x, 1)) <=> s(gen_0':s:logZeroError12_18(x))
gen_c3:c4:c513_18(0) <=> c3
gen_c3:c4:c513_18(+(x, 1)) <=> c5(gen_c3:c4:c513_18(x))
gen_c6:c714_18(0) <=> c7
gen_c6:c714_18(+(x, 1)) <=> c6(gen_c6:c714_18(x))


The following defined symbols remain to be analysed:
INC, LOGITER, le, half, inc, logIter

They will be analysed ascendingly in the following order:
INC < LOGITER
le < LOGITER
half < LOGITER
inc < LOGITER
le < logIter
half < logIter
inc < logIter

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

(27) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
INC(gen_0':s:logZeroError12_18(n1274_18)) -> gen_c6:c714_18(n1274_18), rt in Omega(1 + n1274_18)

Induction Base:
INC(gen_0':s:logZeroError12_18(0)) ->_R^Omega(1)
c7

Induction Step:
INC(gen_0':s:logZeroError12_18(+(n1274_18, 1))) ->_R^Omega(1)
c6(INC(gen_0':s:logZeroError12_18(n1274_18))) ->_IH
c6(gen_c6:c714_18(c1275_18))

We have rt in Omega(n^1) and sz in O(n). Thus, we have irc_R in Omega(n).
----------------------------------------

(28)
Obligation:
Innermost TRS:
Rules:
HALF(0') -> c
HALF(s(0')) -> c1
HALF(s(s(z0))) -> c2(HALF(z0))
LE(0', z0) -> c3
LE(s(z0), 0') -> c4
LE(s(z0), s(z1)) -> c5(LE(z0, z1))
INC(s(z0)) -> c6(INC(z0))
INC(0') -> c7
LOGARITHM(z0) -> c8(LOGITER(z0, 0'))
LOGITER(z0, z1) -> c9(IF(le(s(0'), z0), le(s(s(0')), z0), half(z0), inc(z1)), LE(s(0'), z0))
LOGITER(z0, z1) -> c10(IF(le(s(0'), z0), le(s(s(0')), z0), half(z0), inc(z1)), LE(s(s(0')), z0))
LOGITER(z0, z1) -> c11(IF(le(s(0'), z0), le(s(s(0')), z0), half(z0), inc(z1)), HALF(z0))
LOGITER(z0, z1) -> c12(IF(le(s(0'), z0), le(s(s(0')), z0), half(z0), inc(z1)), INC(z1))
IF(false, z0, z1, z2) -> c13
IF(true, false, z0, s(z1)) -> c14
IF(true, true, z0, z1) -> c15(LOGITER(z0, z1))
F -> c16
F -> c17
half(0') -> 0'
half(s(0')) -> 0'
half(s(s(z0))) -> s(half(z0))
le(0', z0) -> true
le(s(z0), 0') -> false
le(s(z0), s(z1)) -> le(z0, z1)
inc(s(z0)) -> s(inc(z0))
inc(0') -> s(0')
logarithm(z0) -> logIter(z0, 0')
logIter(z0, z1) -> if(le(s(0'), z0), le(s(s(0')), z0), half(z0), inc(z1))
if(false, z0, z1, z2) -> logZeroError
if(true, false, z0, s(z1)) -> z1
if(true, true, z0, z1) -> logIter(z0, z1)
f -> g
f -> h

Types:
HALF :: 0':s:logZeroError -> c:c1:c2
0' :: 0':s:logZeroError
c :: c:c1:c2
s :: 0':s:logZeroError -> 0':s:logZeroError
c1 :: c:c1:c2
c2 :: c:c1:c2 -> c:c1:c2
LE :: 0':s:logZeroError -> 0':s:logZeroError -> c3:c4:c5
c3 :: c3:c4:c5
c4 :: c3:c4:c5
c5 :: c3:c4:c5 -> c3:c4:c5
INC :: 0':s:logZeroError -> c6:c7
c6 :: c6:c7 -> c6:c7
c7 :: c6:c7
LOGARITHM :: 0':s:logZeroError -> c8
c8 :: c9:c10:c11:c12 -> c8
LOGITER :: 0':s:logZeroError -> 0':s:logZeroError -> c9:c10:c11:c12
c9 :: c13:c14:c15 -> c3:c4:c5 -> c9:c10:c11:c12
IF :: false:true -> false:true -> 0':s:logZeroError -> 0':s:logZeroError -> c13:c14:c15
le :: 0':s:logZeroError -> 0':s:logZeroError -> false:true
half :: 0':s:logZeroError -> 0':s:logZeroError
inc :: 0':s:logZeroError -> 0':s:logZeroError
c10 :: c13:c14:c15 -> c3:c4:c5 -> c9:c10:c11:c12
c11 :: c13:c14:c15 -> c:c1:c2 -> c9:c10:c11:c12
c12 :: c13:c14:c15 -> c6:c7 -> c9:c10:c11:c12
false :: false:true
c13 :: c13:c14:c15
true :: false:true
c14 :: c13:c14:c15
c15 :: c9:c10:c11:c12 -> c13:c14:c15
F :: c16:c17
c16 :: c16:c17
c17 :: c16:c17
logarithm :: 0':s:logZeroError -> 0':s:logZeroError
logIter :: 0':s:logZeroError -> 0':s:logZeroError -> 0':s:logZeroError
if :: false:true -> false:true -> 0':s:logZeroError -> 0':s:logZeroError -> 0':s:logZeroError
logZeroError :: 0':s:logZeroError
f :: g:h
g :: g:h
h :: g:h
hole_c:c1:c21_18 :: c:c1:c2
hole_0':s:logZeroError2_18 :: 0':s:logZeroError
hole_c3:c4:c53_18 :: c3:c4:c5
hole_c6:c74_18 :: c6:c7
hole_c85_18 :: c8
hole_c9:c10:c11:c126_18 :: c9:c10:c11:c12
hole_c13:c14:c157_18 :: c13:c14:c15
hole_false:true8_18 :: false:true
hole_c16:c179_18 :: c16:c17
hole_g:h10_18 :: g:h
gen_c:c1:c211_18 :: Nat -> c:c1:c2
gen_0':s:logZeroError12_18 :: Nat -> 0':s:logZeroError
gen_c3:c4:c513_18 :: Nat -> c3:c4:c5
gen_c6:c714_18 :: Nat -> c6:c7


Lemmas:
HALF(gen_0':s:logZeroError12_18(*(2, n16_18))) -> gen_c:c1:c211_18(n16_18), rt in Omega(1 + n16_18)
LE(gen_0':s:logZeroError12_18(n502_18), gen_0':s:logZeroError12_18(n502_18)) -> gen_c3:c4:c513_18(n502_18), rt in Omega(1 + n502_18)
INC(gen_0':s:logZeroError12_18(n1274_18)) -> gen_c6:c714_18(n1274_18), rt in Omega(1 + n1274_18)


Generator Equations:
gen_c:c1:c211_18(0) <=> c
gen_c:c1:c211_18(+(x, 1)) <=> c2(gen_c:c1:c211_18(x))
gen_0':s:logZeroError12_18(0) <=> 0'
gen_0':s:logZeroError12_18(+(x, 1)) <=> s(gen_0':s:logZeroError12_18(x))
gen_c3:c4:c513_18(0) <=> c3
gen_c3:c4:c513_18(+(x, 1)) <=> c5(gen_c3:c4:c513_18(x))
gen_c6:c714_18(0) <=> c7
gen_c6:c714_18(+(x, 1)) <=> c6(gen_c6:c714_18(x))


The following defined symbols remain to be analysed:
le, LOGITER, half, inc, logIter

They will be analysed ascendingly in the following order:
le < LOGITER
half < LOGITER
inc < LOGITER
le < logIter
half < logIter
inc < logIter

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

(29) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
le(gen_0':s:logZeroError12_18(n1709_18), gen_0':s:logZeroError12_18(n1709_18)) -> true, rt in Omega(0)

Induction Base:
le(gen_0':s:logZeroError12_18(0), gen_0':s:logZeroError12_18(0)) ->_R^Omega(0)
true

Induction Step:
le(gen_0':s:logZeroError12_18(+(n1709_18, 1)), gen_0':s:logZeroError12_18(+(n1709_18, 1))) ->_R^Omega(0)
le(gen_0':s:logZeroError12_18(n1709_18), gen_0':s:logZeroError12_18(n1709_18)) ->_IH
true

We have rt in Omega(1) and sz in O(n). Thus, we have irc_R in Omega(n^0).
----------------------------------------

(30)
Obligation:
Innermost TRS:
Rules:
HALF(0') -> c
HALF(s(0')) -> c1
HALF(s(s(z0))) -> c2(HALF(z0))
LE(0', z0) -> c3
LE(s(z0), 0') -> c4
LE(s(z0), s(z1)) -> c5(LE(z0, z1))
INC(s(z0)) -> c6(INC(z0))
INC(0') -> c7
LOGARITHM(z0) -> c8(LOGITER(z0, 0'))
LOGITER(z0, z1) -> c9(IF(le(s(0'), z0), le(s(s(0')), z0), half(z0), inc(z1)), LE(s(0'), z0))
LOGITER(z0, z1) -> c10(IF(le(s(0'), z0), le(s(s(0')), z0), half(z0), inc(z1)), LE(s(s(0')), z0))
LOGITER(z0, z1) -> c11(IF(le(s(0'), z0), le(s(s(0')), z0), half(z0), inc(z1)), HALF(z0))
LOGITER(z0, z1) -> c12(IF(le(s(0'), z0), le(s(s(0')), z0), half(z0), inc(z1)), INC(z1))
IF(false, z0, z1, z2) -> c13
IF(true, false, z0, s(z1)) -> c14
IF(true, true, z0, z1) -> c15(LOGITER(z0, z1))
F -> c16
F -> c17
half(0') -> 0'
half(s(0')) -> 0'
half(s(s(z0))) -> s(half(z0))
le(0', z0) -> true
le(s(z0), 0') -> false
le(s(z0), s(z1)) -> le(z0, z1)
inc(s(z0)) -> s(inc(z0))
inc(0') -> s(0')
logarithm(z0) -> logIter(z0, 0')
logIter(z0, z1) -> if(le(s(0'), z0), le(s(s(0')), z0), half(z0), inc(z1))
if(false, z0, z1, z2) -> logZeroError
if(true, false, z0, s(z1)) -> z1
if(true, true, z0, z1) -> logIter(z0, z1)
f -> g
f -> h

Types:
HALF :: 0':s:logZeroError -> c:c1:c2
0' :: 0':s:logZeroError
c :: c:c1:c2
s :: 0':s:logZeroError -> 0':s:logZeroError
c1 :: c:c1:c2
c2 :: c:c1:c2 -> c:c1:c2
LE :: 0':s:logZeroError -> 0':s:logZeroError -> c3:c4:c5
c3 :: c3:c4:c5
c4 :: c3:c4:c5
c5 :: c3:c4:c5 -> c3:c4:c5
INC :: 0':s:logZeroError -> c6:c7
c6 :: c6:c7 -> c6:c7
c7 :: c6:c7
LOGARITHM :: 0':s:logZeroError -> c8
c8 :: c9:c10:c11:c12 -> c8
LOGITER :: 0':s:logZeroError -> 0':s:logZeroError -> c9:c10:c11:c12
c9 :: c13:c14:c15 -> c3:c4:c5 -> c9:c10:c11:c12
IF :: false:true -> false:true -> 0':s:logZeroError -> 0':s:logZeroError -> c13:c14:c15
le :: 0':s:logZeroError -> 0':s:logZeroError -> false:true
half :: 0':s:logZeroError -> 0':s:logZeroError
inc :: 0':s:logZeroError -> 0':s:logZeroError
c10 :: c13:c14:c15 -> c3:c4:c5 -> c9:c10:c11:c12
c11 :: c13:c14:c15 -> c:c1:c2 -> c9:c10:c11:c12
c12 :: c13:c14:c15 -> c6:c7 -> c9:c10:c11:c12
false :: false:true
c13 :: c13:c14:c15
true :: false:true
c14 :: c13:c14:c15
c15 :: c9:c10:c11:c12 -> c13:c14:c15
F :: c16:c17
c16 :: c16:c17
c17 :: c16:c17
logarithm :: 0':s:logZeroError -> 0':s:logZeroError
logIter :: 0':s:logZeroError -> 0':s:logZeroError -> 0':s:logZeroError
if :: false:true -> false:true -> 0':s:logZeroError -> 0':s:logZeroError -> 0':s:logZeroError
logZeroError :: 0':s:logZeroError
f :: g:h
g :: g:h
h :: g:h
hole_c:c1:c21_18 :: c:c1:c2
hole_0':s:logZeroError2_18 :: 0':s:logZeroError
hole_c3:c4:c53_18 :: c3:c4:c5
hole_c6:c74_18 :: c6:c7
hole_c85_18 :: c8
hole_c9:c10:c11:c126_18 :: c9:c10:c11:c12
hole_c13:c14:c157_18 :: c13:c14:c15
hole_false:true8_18 :: false:true
hole_c16:c179_18 :: c16:c17
hole_g:h10_18 :: g:h
gen_c:c1:c211_18 :: Nat -> c:c1:c2
gen_0':s:logZeroError12_18 :: Nat -> 0':s:logZeroError
gen_c3:c4:c513_18 :: Nat -> c3:c4:c5
gen_c6:c714_18 :: Nat -> c6:c7


Lemmas:
HALF(gen_0':s:logZeroError12_18(*(2, n16_18))) -> gen_c:c1:c211_18(n16_18), rt in Omega(1 + n16_18)
LE(gen_0':s:logZeroError12_18(n502_18), gen_0':s:logZeroError12_18(n502_18)) -> gen_c3:c4:c513_18(n502_18), rt in Omega(1 + n502_18)
INC(gen_0':s:logZeroError12_18(n1274_18)) -> gen_c6:c714_18(n1274_18), rt in Omega(1 + n1274_18)
le(gen_0':s:logZeroError12_18(n1709_18), gen_0':s:logZeroError12_18(n1709_18)) -> true, rt in Omega(0)


Generator Equations:
gen_c:c1:c211_18(0) <=> c
gen_c:c1:c211_18(+(x, 1)) <=> c2(gen_c:c1:c211_18(x))
gen_0':s:logZeroError12_18(0) <=> 0'
gen_0':s:logZeroError12_18(+(x, 1)) <=> s(gen_0':s:logZeroError12_18(x))
gen_c3:c4:c513_18(0) <=> c3
gen_c3:c4:c513_18(+(x, 1)) <=> c5(gen_c3:c4:c513_18(x))
gen_c6:c714_18(0) <=> c7
gen_c6:c714_18(+(x, 1)) <=> c6(gen_c6:c714_18(x))


The following defined symbols remain to be analysed:
half, LOGITER, inc, logIter

They will be analysed ascendingly in the following order:
half < LOGITER
inc < LOGITER
half < logIter
inc < logIter

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

(31) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
half(gen_0':s:logZeroError12_18(*(2, n2184_18))) -> gen_0':s:logZeroError12_18(n2184_18), rt in Omega(0)

Induction Base:
half(gen_0':s:logZeroError12_18(*(2, 0))) ->_R^Omega(0)
0'

Induction Step:
half(gen_0':s:logZeroError12_18(*(2, +(n2184_18, 1)))) ->_R^Omega(0)
s(half(gen_0':s:logZeroError12_18(*(2, n2184_18)))) ->_IH
s(gen_0':s:logZeroError12_18(c2185_18))

We have rt in Omega(1) and sz in O(n). Thus, we have irc_R in Omega(n^0).
----------------------------------------

(32)
Obligation:
Innermost TRS:
Rules:
HALF(0') -> c
HALF(s(0')) -> c1
HALF(s(s(z0))) -> c2(HALF(z0))
LE(0', z0) -> c3
LE(s(z0), 0') -> c4
LE(s(z0), s(z1)) -> c5(LE(z0, z1))
INC(s(z0)) -> c6(INC(z0))
INC(0') -> c7
LOGARITHM(z0) -> c8(LOGITER(z0, 0'))
LOGITER(z0, z1) -> c9(IF(le(s(0'), z0), le(s(s(0')), z0), half(z0), inc(z1)), LE(s(0'), z0))
LOGITER(z0, z1) -> c10(IF(le(s(0'), z0), le(s(s(0')), z0), half(z0), inc(z1)), LE(s(s(0')), z0))
LOGITER(z0, z1) -> c11(IF(le(s(0'), z0), le(s(s(0')), z0), half(z0), inc(z1)), HALF(z0))
LOGITER(z0, z1) -> c12(IF(le(s(0'), z0), le(s(s(0')), z0), half(z0), inc(z1)), INC(z1))
IF(false, z0, z1, z2) -> c13
IF(true, false, z0, s(z1)) -> c14
IF(true, true, z0, z1) -> c15(LOGITER(z0, z1))
F -> c16
F -> c17
half(0') -> 0'
half(s(0')) -> 0'
half(s(s(z0))) -> s(half(z0))
le(0', z0) -> true
le(s(z0), 0') -> false
le(s(z0), s(z1)) -> le(z0, z1)
inc(s(z0)) -> s(inc(z0))
inc(0') -> s(0')
logarithm(z0) -> logIter(z0, 0')
logIter(z0, z1) -> if(le(s(0'), z0), le(s(s(0')), z0), half(z0), inc(z1))
if(false, z0, z1, z2) -> logZeroError
if(true, false, z0, s(z1)) -> z1
if(true, true, z0, z1) -> logIter(z0, z1)
f -> g
f -> h

Types:
HALF :: 0':s:logZeroError -> c:c1:c2
0' :: 0':s:logZeroError
c :: c:c1:c2
s :: 0':s:logZeroError -> 0':s:logZeroError
c1 :: c:c1:c2
c2 :: c:c1:c2 -> c:c1:c2
LE :: 0':s:logZeroError -> 0':s:logZeroError -> c3:c4:c5
c3 :: c3:c4:c5
c4 :: c3:c4:c5
c5 :: c3:c4:c5 -> c3:c4:c5
INC :: 0':s:logZeroError -> c6:c7
c6 :: c6:c7 -> c6:c7
c7 :: c6:c7
LOGARITHM :: 0':s:logZeroError -> c8
c8 :: c9:c10:c11:c12 -> c8
LOGITER :: 0':s:logZeroError -> 0':s:logZeroError -> c9:c10:c11:c12
c9 :: c13:c14:c15 -> c3:c4:c5 -> c9:c10:c11:c12
IF :: false:true -> false:true -> 0':s:logZeroError -> 0':s:logZeroError -> c13:c14:c15
le :: 0':s:logZeroError -> 0':s:logZeroError -> false:true
half :: 0':s:logZeroError -> 0':s:logZeroError
inc :: 0':s:logZeroError -> 0':s:logZeroError
c10 :: c13:c14:c15 -> c3:c4:c5 -> c9:c10:c11:c12
c11 :: c13:c14:c15 -> c:c1:c2 -> c9:c10:c11:c12
c12 :: c13:c14:c15 -> c6:c7 -> c9:c10:c11:c12
false :: false:true
c13 :: c13:c14:c15
true :: false:true
c14 :: c13:c14:c15
c15 :: c9:c10:c11:c12 -> c13:c14:c15
F :: c16:c17
c16 :: c16:c17
c17 :: c16:c17
logarithm :: 0':s:logZeroError -> 0':s:logZeroError
logIter :: 0':s:logZeroError -> 0':s:logZeroError -> 0':s:logZeroError
if :: false:true -> false:true -> 0':s:logZeroError -> 0':s:logZeroError -> 0':s:logZeroError
logZeroError :: 0':s:logZeroError
f :: g:h
g :: g:h
h :: g:h
hole_c:c1:c21_18 :: c:c1:c2
hole_0':s:logZeroError2_18 :: 0':s:logZeroError
hole_c3:c4:c53_18 :: c3:c4:c5
hole_c6:c74_18 :: c6:c7
hole_c85_18 :: c8
hole_c9:c10:c11:c126_18 :: c9:c10:c11:c12
hole_c13:c14:c157_18 :: c13:c14:c15
hole_false:true8_18 :: false:true
hole_c16:c179_18 :: c16:c17
hole_g:h10_18 :: g:h
gen_c:c1:c211_18 :: Nat -> c:c1:c2
gen_0':s:logZeroError12_18 :: Nat -> 0':s:logZeroError
gen_c3:c4:c513_18 :: Nat -> c3:c4:c5
gen_c6:c714_18 :: Nat -> c6:c7


Lemmas:
HALF(gen_0':s:logZeroError12_18(*(2, n16_18))) -> gen_c:c1:c211_18(n16_18), rt in Omega(1 + n16_18)
LE(gen_0':s:logZeroError12_18(n502_18), gen_0':s:logZeroError12_18(n502_18)) -> gen_c3:c4:c513_18(n502_18), rt in Omega(1 + n502_18)
INC(gen_0':s:logZeroError12_18(n1274_18)) -> gen_c6:c714_18(n1274_18), rt in Omega(1 + n1274_18)
le(gen_0':s:logZeroError12_18(n1709_18), gen_0':s:logZeroError12_18(n1709_18)) -> true, rt in Omega(0)
half(gen_0':s:logZeroError12_18(*(2, n2184_18))) -> gen_0':s:logZeroError12_18(n2184_18), rt in Omega(0)


Generator Equations:
gen_c:c1:c211_18(0) <=> c
gen_c:c1:c211_18(+(x, 1)) <=> c2(gen_c:c1:c211_18(x))
gen_0':s:logZeroError12_18(0) <=> 0'
gen_0':s:logZeroError12_18(+(x, 1)) <=> s(gen_0':s:logZeroError12_18(x))
gen_c3:c4:c513_18(0) <=> c3
gen_c3:c4:c513_18(+(x, 1)) <=> c5(gen_c3:c4:c513_18(x))
gen_c6:c714_18(0) <=> c7
gen_c6:c714_18(+(x, 1)) <=> c6(gen_c6:c714_18(x))


The following defined symbols remain to be analysed:
inc, LOGITER, logIter

They will be analysed ascendingly in the following order:
inc < LOGITER
inc < logIter

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

(33) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
inc(gen_0':s:logZeroError12_18(n2700_18)) -> gen_0':s:logZeroError12_18(+(1, n2700_18)), rt in Omega(0)

Induction Base:
inc(gen_0':s:logZeroError12_18(0)) ->_R^Omega(0)
s(0')

Induction Step:
inc(gen_0':s:logZeroError12_18(+(n2700_18, 1))) ->_R^Omega(0)
s(inc(gen_0':s:logZeroError12_18(n2700_18))) ->_IH
s(gen_0':s:logZeroError12_18(+(1, c2701_18)))

We have rt in Omega(1) and sz in O(n). Thus, we have irc_R in Omega(n^0).
----------------------------------------

(34)
Obligation:
Innermost TRS:
Rules:
HALF(0') -> c
HALF(s(0')) -> c1
HALF(s(s(z0))) -> c2(HALF(z0))
LE(0', z0) -> c3
LE(s(z0), 0') -> c4
LE(s(z0), s(z1)) -> c5(LE(z0, z1))
INC(s(z0)) -> c6(INC(z0))
INC(0') -> c7
LOGARITHM(z0) -> c8(LOGITER(z0, 0'))
LOGITER(z0, z1) -> c9(IF(le(s(0'), z0), le(s(s(0')), z0), half(z0), inc(z1)), LE(s(0'), z0))
LOGITER(z0, z1) -> c10(IF(le(s(0'), z0), le(s(s(0')), z0), half(z0), inc(z1)), LE(s(s(0')), z0))
LOGITER(z0, z1) -> c11(IF(le(s(0'), z0), le(s(s(0')), z0), half(z0), inc(z1)), HALF(z0))
LOGITER(z0, z1) -> c12(IF(le(s(0'), z0), le(s(s(0')), z0), half(z0), inc(z1)), INC(z1))
IF(false, z0, z1, z2) -> c13
IF(true, false, z0, s(z1)) -> c14
IF(true, true, z0, z1) -> c15(LOGITER(z0, z1))
F -> c16
F -> c17
half(0') -> 0'
half(s(0')) -> 0'
half(s(s(z0))) -> s(half(z0))
le(0', z0) -> true
le(s(z0), 0') -> false
le(s(z0), s(z1)) -> le(z0, z1)
inc(s(z0)) -> s(inc(z0))
inc(0') -> s(0')
logarithm(z0) -> logIter(z0, 0')
logIter(z0, z1) -> if(le(s(0'), z0), le(s(s(0')), z0), half(z0), inc(z1))
if(false, z0, z1, z2) -> logZeroError
if(true, false, z0, s(z1)) -> z1
if(true, true, z0, z1) -> logIter(z0, z1)
f -> g
f -> h

Types:
HALF :: 0':s:logZeroError -> c:c1:c2
0' :: 0':s:logZeroError
c :: c:c1:c2
s :: 0':s:logZeroError -> 0':s:logZeroError
c1 :: c:c1:c2
c2 :: c:c1:c2 -> c:c1:c2
LE :: 0':s:logZeroError -> 0':s:logZeroError -> c3:c4:c5
c3 :: c3:c4:c5
c4 :: c3:c4:c5
c5 :: c3:c4:c5 -> c3:c4:c5
INC :: 0':s:logZeroError -> c6:c7
c6 :: c6:c7 -> c6:c7
c7 :: c6:c7
LOGARITHM :: 0':s:logZeroError -> c8
c8 :: c9:c10:c11:c12 -> c8
LOGITER :: 0':s:logZeroError -> 0':s:logZeroError -> c9:c10:c11:c12
c9 :: c13:c14:c15 -> c3:c4:c5 -> c9:c10:c11:c12
IF :: false:true -> false:true -> 0':s:logZeroError -> 0':s:logZeroError -> c13:c14:c15
le :: 0':s:logZeroError -> 0':s:logZeroError -> false:true
half :: 0':s:logZeroError -> 0':s:logZeroError
inc :: 0':s:logZeroError -> 0':s:logZeroError
c10 :: c13:c14:c15 -> c3:c4:c5 -> c9:c10:c11:c12
c11 :: c13:c14:c15 -> c:c1:c2 -> c9:c10:c11:c12
c12 :: c13:c14:c15 -> c6:c7 -> c9:c10:c11:c12
false :: false:true
c13 :: c13:c14:c15
true :: false:true
c14 :: c13:c14:c15
c15 :: c9:c10:c11:c12 -> c13:c14:c15
F :: c16:c17
c16 :: c16:c17
c17 :: c16:c17
logarithm :: 0':s:logZeroError -> 0':s:logZeroError
logIter :: 0':s:logZeroError -> 0':s:logZeroError -> 0':s:logZeroError
if :: false:true -> false:true -> 0':s:logZeroError -> 0':s:logZeroError -> 0':s:logZeroError
logZeroError :: 0':s:logZeroError
f :: g:h
g :: g:h
h :: g:h
hole_c:c1:c21_18 :: c:c1:c2
hole_0':s:logZeroError2_18 :: 0':s:logZeroError
hole_c3:c4:c53_18 :: c3:c4:c5
hole_c6:c74_18 :: c6:c7
hole_c85_18 :: c8
hole_c9:c10:c11:c126_18 :: c9:c10:c11:c12
hole_c13:c14:c157_18 :: c13:c14:c15
hole_false:true8_18 :: false:true
hole_c16:c179_18 :: c16:c17
hole_g:h10_18 :: g:h
gen_c:c1:c211_18 :: Nat -> c:c1:c2
gen_0':s:logZeroError12_18 :: Nat -> 0':s:logZeroError
gen_c3:c4:c513_18 :: Nat -> c3:c4:c5
gen_c6:c714_18 :: Nat -> c6:c7


Lemmas:
HALF(gen_0':s:logZeroError12_18(*(2, n16_18))) -> gen_c:c1:c211_18(n16_18), rt in Omega(1 + n16_18)
LE(gen_0':s:logZeroError12_18(n502_18), gen_0':s:logZeroError12_18(n502_18)) -> gen_c3:c4:c513_18(n502_18), rt in Omega(1 + n502_18)
INC(gen_0':s:logZeroError12_18(n1274_18)) -> gen_c6:c714_18(n1274_18), rt in Omega(1 + n1274_18)
le(gen_0':s:logZeroError12_18(n1709_18), gen_0':s:logZeroError12_18(n1709_18)) -> true, rt in Omega(0)
half(gen_0':s:logZeroError12_18(*(2, n2184_18))) -> gen_0':s:logZeroError12_18(n2184_18), rt in Omega(0)
inc(gen_0':s:logZeroError12_18(n2700_18)) -> gen_0':s:logZeroError12_18(+(1, n2700_18)), rt in Omega(0)


Generator Equations:
gen_c:c1:c211_18(0) <=> c
gen_c:c1:c211_18(+(x, 1)) <=> c2(gen_c:c1:c211_18(x))
gen_0':s:logZeroError12_18(0) <=> 0'
gen_0':s:logZeroError12_18(+(x, 1)) <=> s(gen_0':s:logZeroError12_18(x))
gen_c3:c4:c513_18(0) <=> c3
gen_c3:c4:c513_18(+(x, 1)) <=> c5(gen_c3:c4:c513_18(x))
gen_c6:c714_18(0) <=> c7
gen_c6:c714_18(+(x, 1)) <=> c6(gen_c6:c714_18(x))


The following defined symbols remain to be analysed:
LOGITER, logIter