WORST_CASE(Omega(n^1),O(n^2))
proof of input_Jh7FHEH39D.trs
# AProVE Commit ID: aff8ecad908e01718a4c36e68d2e55d5e0f16e15 fuhs 20220216 unpublished


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

(0) CpxTRS
(1) CpxTrsToCdtProof [UPPER BOUND(ID), 0 ms]
(2) CdtProblem
    (3) CdtLeafRemovalProof [ComplexityIfPolyImplication, 0 ms]
    (4) CdtProblem
    (5) CdtUsableRulesProof [BOTH BOUNDS(ID, ID), 0 ms]
    (6) CdtProblem
    (7) CdtToCpxRelTrsProof [BOTH BOUNDS(ID, ID), 0 ms]
    (8) CpxRelTRS
    (9) RelTrsToWeightedTrsProof [BOTH BOUNDS(ID, ID), 0 ms]
    (10) CpxWeightedTrs
    (11) TypeInferenceProof [BOTH BOUNDS(ID, ID), 0 ms]
    (12) CpxTypedWeightedTrs
    (13) CompletionProof [UPPER BOUND(ID), 0 ms]
    (14) CpxTypedWeightedCompleteTrs
    (15) CpxTypedWeightedTrsToRntsProof [UPPER BOUND(ID), 0 ms]
    (16) CpxRNTS
    (17) CompleteCoflocoProof [FINISHED, 4300 ms]
    (18) BOUNDS(1, n^2)
(19) CpxTrsToCdtProof [BOTH BOUNDS(ID, ID), 0 ms]
(20) CdtProblem
    (21) CdtToCpxRelTrsProof [BOTH BOUNDS(ID, ID), 0 ms]
    (22) CpxRelTRS
    (23) RenamingProof [BOTH BOUNDS(ID, ID), 0 ms]
    (24) CpxRelTRS
    (25) TypeInferenceProof [BOTH BOUNDS(ID, ID), 0 ms]
    (26) typed CpxTrs
    (27) OrderProof [LOWER BOUND(ID), 11 ms]
    (28) typed CpxTrs
    (29) RewriteLemmaProof [LOWER BOUND(ID), 396 ms]
    (30) BEST
        (31) proven lower bound
            (32) LowerBoundPropagationProof [FINISHED, 0 ms]
            (33) BOUNDS(n^1, INF)
        (34) typed CpxTrs
            (35) RewriteLemmaProof [LOWER BOUND(ID), 83 ms]
            (36) typed CpxTrs


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

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


The TRS R consists of the following rules:

   le(0, y) -> true
   le(s(x), 0) -> false
   le(s(x), s(y)) -> le(x, y)
   quot(x, 0) -> quotZeroErro
   quot(x, s(y)) -> quotIter(x, s(y), 0, 0, 0)
   quotIter(x, s(y), z, u, v) -> if(le(x, z), x, s(y), z, u, v)
   if(true, x, y, z, u, v) -> v
   if(false, x, y, z, u, v) -> if2(le(y, s(u)), x, y, s(z), s(u), v)
   if2(false, x, y, z, u, v) -> quotIter(x, y, z, u, v)
   if2(true, x, y, z, u, v) -> quotIter(x, y, z, 0, s(v))

S is empty.
Rewrite Strategy: PARALLEL_INNERMOST
----------------------------------------

(1) CpxTrsToCdtProof (UPPER BOUND(ID))
Converted Cpx (relative) TRS with rewrite strategy PARALLEL_INNERMOST to CDT
----------------------------------------

(2)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   le(0, z0) -> true
   le(s(z0), 0) -> false
   le(s(z0), s(z1)) -> le(z0, z1)
   quot(z0, 0) -> quotZeroErro
   quot(z0, s(z1)) -> quotIter(z0, s(z1), 0, 0, 0)
   quotIter(z0, s(z1), z2, z3, z4) -> if(le(z0, z2), z0, s(z1), z2, z3, z4)
   if(true, z0, z1, z2, z3, z4) -> z4
   if(false, z0, z1, z2, z3, z4) -> if2(le(z1, s(z3)), z0, z1, s(z2), s(z3), z4)
   if2(false, z0, z1, z2, z3, z4) -> quotIter(z0, z1, z2, z3, z4)
   if2(true, z0, z1, z2, z3, z4) -> quotIter(z0, z1, z2, 0, s(z4))
Tuples:
   LE(0, z0) -> c
   LE(s(z0), 0) -> c1
   LE(s(z0), s(z1)) -> c2(LE(z0, z1))
   QUOT(z0, 0) -> c3
   QUOT(z0, s(z1)) -> c4(QUOTITER(z0, s(z1), 0, 0, 0))
   QUOTITER(z0, s(z1), z2, z3, z4) -> c5(IF(le(z0, z2), z0, s(z1), z2, z3, z4), LE(z0, z2))
   IF(true, z0, z1, z2, z3, z4) -> c6
   IF(false, z0, z1, z2, z3, z4) -> c7(IF2(le(z1, s(z3)), z0, z1, s(z2), s(z3), z4), LE(z1, s(z3)))
   IF2(false, z0, z1, z2, z3, z4) -> c8(QUOTITER(z0, z1, z2, z3, z4))
   IF2(true, z0, z1, z2, z3, z4) -> c9(QUOTITER(z0, z1, z2, 0, s(z4)))
S tuples:
   LE(0, z0) -> c
   LE(s(z0), 0) -> c1
   LE(s(z0), s(z1)) -> c2(LE(z0, z1))
   QUOT(z0, 0) -> c3
   QUOT(z0, s(z1)) -> c4(QUOTITER(z0, s(z1), 0, 0, 0))
   QUOTITER(z0, s(z1), z2, z3, z4) -> c5(IF(le(z0, z2), z0, s(z1), z2, z3, z4), LE(z0, z2))
   IF(true, z0, z1, z2, z3, z4) -> c6
   IF(false, z0, z1, z2, z3, z4) -> c7(IF2(le(z1, s(z3)), z0, z1, s(z2), s(z3), z4), LE(z1, s(z3)))
   IF2(false, z0, z1, z2, z3, z4) -> c8(QUOTITER(z0, z1, z2, z3, z4))
   IF2(true, z0, z1, z2, z3, z4) -> c9(QUOTITER(z0, z1, z2, 0, s(z4)))
K tuples:none
Defined Rule Symbols:   le_2, quot_2, quotIter_5, if_6, if2_6

Defined Pair Symbols:   LE_2, QUOT_2, QUOTITER_5, IF_6, IF2_6

Compound Symbols:   c, c1, c2_1, c3, c4_1, c5_2, c6, c7_2, c8_1, c9_1


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

(3) CdtLeafRemovalProof (ComplexityIfPolyImplication)
Removed 1 leading nodes:
   QUOT(z0, s(z1)) -> c4(QUOTITER(z0, s(z1), 0, 0, 0))
Removed 4 trailing nodes:
   LE(0, z0) -> c
   QUOT(z0, 0) -> c3
   IF(true, z0, z1, z2, z3, z4) -> c6
   LE(s(z0), 0) -> c1

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

(4)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   le(0, z0) -> true
   le(s(z0), 0) -> false
   le(s(z0), s(z1)) -> le(z0, z1)
   quot(z0, 0) -> quotZeroErro
   quot(z0, s(z1)) -> quotIter(z0, s(z1), 0, 0, 0)
   quotIter(z0, s(z1), z2, z3, z4) -> if(le(z0, z2), z0, s(z1), z2, z3, z4)
   if(true, z0, z1, z2, z3, z4) -> z4
   if(false, z0, z1, z2, z3, z4) -> if2(le(z1, s(z3)), z0, z1, s(z2), s(z3), z4)
   if2(false, z0, z1, z2, z3, z4) -> quotIter(z0, z1, z2, z3, z4)
   if2(true, z0, z1, z2, z3, z4) -> quotIter(z0, z1, z2, 0, s(z4))
Tuples:
   LE(s(z0), s(z1)) -> c2(LE(z0, z1))
   QUOTITER(z0, s(z1), z2, z3, z4) -> c5(IF(le(z0, z2), z0, s(z1), z2, z3, z4), LE(z0, z2))
   IF(false, z0, z1, z2, z3, z4) -> c7(IF2(le(z1, s(z3)), z0, z1, s(z2), s(z3), z4), LE(z1, s(z3)))
   IF2(false, z0, z1, z2, z3, z4) -> c8(QUOTITER(z0, z1, z2, z3, z4))
   IF2(true, z0, z1, z2, z3, z4) -> c9(QUOTITER(z0, z1, z2, 0, s(z4)))
S tuples:
   LE(s(z0), s(z1)) -> c2(LE(z0, z1))
   QUOTITER(z0, s(z1), z2, z3, z4) -> c5(IF(le(z0, z2), z0, s(z1), z2, z3, z4), LE(z0, z2))
   IF(false, z0, z1, z2, z3, z4) -> c7(IF2(le(z1, s(z3)), z0, z1, s(z2), s(z3), z4), LE(z1, s(z3)))
   IF2(false, z0, z1, z2, z3, z4) -> c8(QUOTITER(z0, z1, z2, z3, z4))
   IF2(true, z0, z1, z2, z3, z4) -> c9(QUOTITER(z0, z1, z2, 0, s(z4)))
K tuples:none
Defined Rule Symbols:   le_2, quot_2, quotIter_5, if_6, if2_6

Defined Pair Symbols:   LE_2, QUOTITER_5, IF_6, IF2_6

Compound Symbols:   c2_1, c5_2, c7_2, c8_1, c9_1


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

(5) CdtUsableRulesProof (BOTH BOUNDS(ID, ID))
The following rules are not usable and were removed:
   quot(z0, 0) -> quotZeroErro
   quot(z0, s(z1)) -> quotIter(z0, s(z1), 0, 0, 0)
   quotIter(z0, s(z1), z2, z3, z4) -> if(le(z0, z2), z0, s(z1), z2, z3, z4)
   if(true, z0, z1, z2, z3, z4) -> z4
   if(false, z0, z1, z2, z3, z4) -> if2(le(z1, s(z3)), z0, z1, s(z2), s(z3), z4)
   if2(false, z0, z1, z2, z3, z4) -> quotIter(z0, z1, z2, z3, z4)
   if2(true, z0, z1, z2, z3, z4) -> quotIter(z0, z1, z2, 0, s(z4))

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

(6)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   le(0, z0) -> true
   le(s(z0), 0) -> false
   le(s(z0), s(z1)) -> le(z0, z1)
Tuples:
   LE(s(z0), s(z1)) -> c2(LE(z0, z1))
   QUOTITER(z0, s(z1), z2, z3, z4) -> c5(IF(le(z0, z2), z0, s(z1), z2, z3, z4), LE(z0, z2))
   IF(false, z0, z1, z2, z3, z4) -> c7(IF2(le(z1, s(z3)), z0, z1, s(z2), s(z3), z4), LE(z1, s(z3)))
   IF2(false, z0, z1, z2, z3, z4) -> c8(QUOTITER(z0, z1, z2, z3, z4))
   IF2(true, z0, z1, z2, z3, z4) -> c9(QUOTITER(z0, z1, z2, 0, s(z4)))
S tuples:
   LE(s(z0), s(z1)) -> c2(LE(z0, z1))
   QUOTITER(z0, s(z1), z2, z3, z4) -> c5(IF(le(z0, z2), z0, s(z1), z2, z3, z4), LE(z0, z2))
   IF(false, z0, z1, z2, z3, z4) -> c7(IF2(le(z1, s(z3)), z0, z1, s(z2), s(z3), z4), LE(z1, s(z3)))
   IF2(false, z0, z1, z2, z3, z4) -> c8(QUOTITER(z0, z1, z2, z3, z4))
   IF2(true, z0, z1, z2, z3, z4) -> c9(QUOTITER(z0, z1, z2, 0, s(z4)))
K tuples:none
Defined Rule Symbols:   le_2

Defined Pair Symbols:   LE_2, QUOTITER_5, IF_6, IF2_6

Compound Symbols:   c2_1, c5_2, c7_2, c8_1, c9_1


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

(7) CdtToCpxRelTrsProof (BOTH BOUNDS(ID, ID))
Converted S to standard rules, and D \ S as well as R to relative rules.
----------------------------------------

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


The TRS R consists of the following rules:

   LE(s(z0), s(z1)) -> c2(LE(z0, z1))
   QUOTITER(z0, s(z1), z2, z3, z4) -> c5(IF(le(z0, z2), z0, s(z1), z2, z3, z4), LE(z0, z2))
   IF(false, z0, z1, z2, z3, z4) -> c7(IF2(le(z1, s(z3)), z0, z1, s(z2), s(z3), z4), LE(z1, s(z3)))
   IF2(false, z0, z1, z2, z3, z4) -> c8(QUOTITER(z0, z1, z2, z3, z4))
   IF2(true, z0, z1, z2, z3, z4) -> c9(QUOTITER(z0, z1, z2, 0, s(z4)))

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

   le(0, z0) -> true
   le(s(z0), 0) -> false
   le(s(z0), s(z1)) -> le(z0, z1)

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

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

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

   LE(s(z0), s(z1)) -> c2(LE(z0, z1)) [1]
   QUOTITER(z0, s(z1), z2, z3, z4) -> c5(IF(le(z0, z2), z0, s(z1), z2, z3, z4), LE(z0, z2)) [1]
   IF(false, z0, z1, z2, z3, z4) -> c7(IF2(le(z1, s(z3)), z0, z1, s(z2), s(z3), z4), LE(z1, s(z3))) [1]
   IF2(false, z0, z1, z2, z3, z4) -> c8(QUOTITER(z0, z1, z2, z3, z4)) [1]
   IF2(true, z0, z1, z2, z3, z4) -> c9(QUOTITER(z0, z1, z2, 0, s(z4))) [1]
   le(0, z0) -> true [0]
   le(s(z0), 0) -> false [0]
   le(s(z0), s(z1)) -> le(z0, z1) [0]

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

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

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

   LE(s(z0), s(z1)) -> c2(LE(z0, z1)) [1]
   QUOTITER(z0, s(z1), z2, z3, z4) -> c5(IF(le(z0, z2), z0, s(z1), z2, z3, z4), LE(z0, z2)) [1]
   IF(false, z0, z1, z2, z3, z4) -> c7(IF2(le(z1, s(z3)), z0, z1, s(z2), s(z3), z4), LE(z1, s(z3))) [1]
   IF2(false, z0, z1, z2, z3, z4) -> c8(QUOTITER(z0, z1, z2, z3, z4)) [1]
   IF2(true, z0, z1, z2, z3, z4) -> c9(QUOTITER(z0, z1, z2, 0, s(z4))) [1]
   le(0, z0) -> true [0]
   le(s(z0), 0) -> false [0]
   le(s(z0), s(z1)) -> le(z0, z1) [0]

The TRS has the following type information:
LE :: s:0 -> s:0 -> c2
s :: s:0 -> s:0
c2 :: c2 -> c2
QUOTITER :: s:0 -> s:0 -> s:0 -> s:0 -> s:0 -> c5
c5 :: c7 -> c2 -> c5
IF :: false:true -> s:0 -> s:0 -> s:0 -> s:0 -> s:0 -> c7
le :: s:0 -> s:0 -> false:true
false :: false:true
c7 :: c8:c9 -> c2 -> c7
IF2 :: false:true -> s:0 -> s:0 -> s:0 -> s:0 -> s:0 -> c8:c9
c8 :: c5 -> c8:c9
true :: false:true
c9 :: c5 -> c8:c9
0 :: s:0

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

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

   le(v0, v1) -> null_le [0]
   LE(v0, v1) -> null_LE [0]
   QUOTITER(v0, v1, v2, v3, v4) -> null_QUOTITER [0]
   IF(v0, v1, v2, v3, v4, v5) -> null_IF [0]
   IF2(v0, v1, v2, v3, v4, v5) -> null_IF2 [0]

And the following fresh constants:    null_le, null_LE, null_QUOTITER, null_IF, null_IF2

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

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

   LE(s(z0), s(z1)) -> c2(LE(z0, z1)) [1]
   QUOTITER(z0, s(z1), z2, z3, z4) -> c5(IF(le(z0, z2), z0, s(z1), z2, z3, z4), LE(z0, z2)) [1]
   IF(false, z0, z1, z2, z3, z4) -> c7(IF2(le(z1, s(z3)), z0, z1, s(z2), s(z3), z4), LE(z1, s(z3))) [1]
   IF2(false, z0, z1, z2, z3, z4) -> c8(QUOTITER(z0, z1, z2, z3, z4)) [1]
   IF2(true, z0, z1, z2, z3, z4) -> c9(QUOTITER(z0, z1, z2, 0, s(z4))) [1]
   le(0, z0) -> true [0]
   le(s(z0), 0) -> false [0]
   le(s(z0), s(z1)) -> le(z0, z1) [0]
   le(v0, v1) -> null_le [0]
   LE(v0, v1) -> null_LE [0]
   QUOTITER(v0, v1, v2, v3, v4) -> null_QUOTITER [0]
   IF(v0, v1, v2, v3, v4, v5) -> null_IF [0]
   IF2(v0, v1, v2, v3, v4, v5) -> null_IF2 [0]

The TRS has the following type information:
LE :: s:0 -> s:0 -> c2:null_LE
s :: s:0 -> s:0
c2 :: c2:null_LE -> c2:null_LE
QUOTITER :: s:0 -> s:0 -> s:0 -> s:0 -> s:0 -> c5:null_QUOTITER
c5 :: c7:null_IF -> c2:null_LE -> c5:null_QUOTITER
IF :: false:true:null_le -> s:0 -> s:0 -> s:0 -> s:0 -> s:0 -> c7:null_IF
le :: s:0 -> s:0 -> false:true:null_le
false :: false:true:null_le
c7 :: c8:c9:null_IF2 -> c2:null_LE -> c7:null_IF
IF2 :: false:true:null_le -> s:0 -> s:0 -> s:0 -> s:0 -> s:0 -> c8:c9:null_IF2
c8 :: c5:null_QUOTITER -> c8:c9:null_IF2
true :: false:true:null_le
c9 :: c5:null_QUOTITER -> c8:c9:null_IF2
0 :: s:0
null_le :: false:true:null_le
null_LE :: c2:null_LE
null_QUOTITER :: c5:null_QUOTITER
null_IF :: c7:null_IF
null_IF2 :: c8:c9:null_IF2

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

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

   false => 1
   true => 2
   0 => 0
   null_le => 0
   null_LE => 0
   null_QUOTITER => 0
   null_IF => 0
   null_IF2 => 0

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

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

   IF(z, z', z'', z5, z6, z7) -{ 0 }-> 0 :|: z5 = v3, v0 >= 0, v4 >= 0, z7 = v5, z6 = v4, z'' = v2, v1 >= 0, v5 >= 0, z = v0, z' = v1, v2 >= 0, v3 >= 0
   IF(z, z', z'', z5, z6, z7) -{ 1 }-> 1 + IF2(le(z1, 1 + z3), z0, z1, 1 + z2, 1 + z3, z4) + LE(z1, 1 + z3) :|: z1 >= 0, z = 1, z6 = z3, z7 = z4, z0 >= 0, z4 >= 0, z5 = z2, z' = z0, z2 >= 0, z3 >= 0, z'' = z1
   IF2(z, z', z'', z5, z6, z7) -{ 0 }-> 0 :|: z5 = v3, v0 >= 0, v4 >= 0, z7 = v5, z6 = v4, z'' = v2, v1 >= 0, v5 >= 0, z = v0, z' = v1, v2 >= 0, v3 >= 0
   IF2(z, z', z'', z5, z6, z7) -{ 1 }-> 1 + QUOTITER(z0, z1, z2, z3, z4) :|: z1 >= 0, z = 1, z6 = z3, z7 = z4, z0 >= 0, z4 >= 0, z5 = z2, z' = z0, z2 >= 0, z3 >= 0, z'' = z1
   IF2(z, z', z'', z5, z6, z7) -{ 1 }-> 1 + QUOTITER(z0, z1, z2, 0, 1 + z4) :|: z = 2, z1 >= 0, z6 = z3, z7 = z4, z0 >= 0, z4 >= 0, z5 = z2, z' = z0, z2 >= 0, z3 >= 0, z'' = z1
   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
   QUOTITER(z, z', z'', z5, z6) -{ 0 }-> 0 :|: z5 = v3, v0 >= 0, v4 >= 0, z6 = v4, z'' = v2, v1 >= 0, z = v0, z' = v1, v2 >= 0, v3 >= 0
   QUOTITER(z, z', z'', z5, z6) -{ 1 }-> 1 + IF(le(z0, z2), z0, 1 + z1, z2, z3, z4) + LE(z0, z2) :|: z'' = z2, z = z0, z1 >= 0, z6 = z4, z0 >= 0, z5 = z3, z4 >= 0, z' = 1 + z1, z2 >= 0, z3 >= 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

Only complete derivations are relevant for the runtime complexity.

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

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

eq(start(V1, V, V6, V5, V4, V12),0,[fun(V1, V, Out)],[V1 >= 0,V >= 0]).
eq(start(V1, V, V6, V5, V4, V12),0,[fun1(V1, V, V6, V5, V4, Out)],[V1 >= 0,V >= 0,V6 >= 0,V5 >= 0,V4 >= 0]).
eq(start(V1, V, V6, V5, V4, V12),0,[fun2(V1, V, V6, V5, V4, V12, Out)],[V1 >= 0,V >= 0,V6 >= 0,V5 >= 0,V4 >= 0,V12 >= 0]).
eq(start(V1, V, V6, V5, V4, V12),0,[fun3(V1, V, V6, V5, V4, V12, Out)],[V1 >= 0,V >= 0,V6 >= 0,V5 >= 0,V4 >= 0,V12 >= 0]).
eq(start(V1, V, V6, V5, V4, V12),0,[le(V1, V, Out)],[V1 >= 0,V >= 0]).
eq(fun(V1, V, Out),1,[fun(V3, V2, Ret1)],[Out = 1 + Ret1,V2 >= 0,V1 = 1 + V3,V3 >= 0,V = 1 + V2]).
eq(fun1(V1, V, V6, V5, V4, Out),1,[le(V8, V11, Ret010),fun2(Ret010, V8, 1 + V7, V11, V10, V9, Ret01),fun(V8, V11, Ret11)],[Out = 1 + Ret01 + Ret11,V6 = V11,V1 = V8,V7 >= 0,V4 = V9,V8 >= 0,V5 = V10,V9 >= 0,V = 1 + V7,V11 >= 0,V10 >= 0]).
eq(fun2(V1, V, V6, V5, V4, V12, Out),1,[le(V14, 1 + V17, Ret0101),fun3(Ret0101, V15, V14, 1 + V13, 1 + V17, V16, Ret011),fun(V14, 1 + V17, Ret12)],[Out = 1 + Ret011 + Ret12,V14 >= 0,V1 = 1,V4 = V17,V12 = V16,V15 >= 0,V16 >= 0,V5 = V13,V = V15,V13 >= 0,V17 >= 0,V6 = V14]).
eq(fun3(V1, V, V6, V5, V4, V12, Out),1,[fun1(V18, V21, V20, V19, V22, Ret13)],[Out = 1 + Ret13,V21 >= 0,V1 = 1,V4 = V19,V12 = V22,V18 >= 0,V22 >= 0,V5 = V20,V = V18,V20 >= 0,V19 >= 0,V6 = V21]).
eq(fun3(V1, V, V6, V5, V4, V12, Out),1,[fun1(V24, V23, V27, 0, 1 + V25, Ret14)],[Out = 1 + Ret14,V1 = 2,V23 >= 0,V4 = V26,V12 = V25,V24 >= 0,V25 >= 0,V5 = V27,V = V24,V27 >= 0,V26 >= 0,V6 = V23]).
eq(le(V1, V, Out),0,[],[Out = 2,V28 >= 0,V1 = 0,V = V28]).
eq(le(V1, V, Out),0,[],[Out = 1,V1 = 1 + V29,V29 >= 0,V = 0]).
eq(le(V1, V, Out),0,[le(V31, V30, Ret)],[Out = Ret,V30 >= 0,V1 = 1 + V31,V31 >= 0,V = 1 + V30]).
eq(le(V1, V, Out),0,[],[Out = 0,V33 >= 0,V32 >= 0,V1 = V33,V = V32]).
eq(fun(V1, V, Out),0,[],[Out = 0,V35 >= 0,V34 >= 0,V1 = V35,V = V34]).
eq(fun1(V1, V, V6, V5, V4, Out),0,[],[Out = 0,V5 = V39,V37 >= 0,V38 >= 0,V4 = V38,V6 = V40,V36 >= 0,V1 = V37,V = V36,V40 >= 0,V39 >= 0]).
eq(fun2(V1, V, V6, V5, V4, V12, Out),0,[],[Out = 0,V5 = V46,V41 >= 0,V45 >= 0,V12 = V44,V4 = V45,V6 = V42,V43 >= 0,V44 >= 0,V1 = V41,V = V43,V42 >= 0,V46 >= 0]).
eq(fun3(V1, V, V6, V5, V4, V12, Out),0,[],[Out = 0,V5 = V49,V48 >= 0,V52 >= 0,V12 = V51,V4 = V52,V6 = V50,V47 >= 0,V51 >= 0,V1 = V48,V = V47,V50 >= 0,V49 >= 0]).
input_output_vars(fun(V1,V,Out),[V1,V],[Out]).
input_output_vars(fun1(V1,V,V6,V5,V4,Out),[V1,V,V6,V5,V4],[Out]).
input_output_vars(fun2(V1,V,V6,V5,V4,V12,Out),[V1,V,V6,V5,V4,V12],[Out]).
input_output_vars(fun3(V1,V,V6,V5,V4,V12,Out),[V1,V,V6,V5,V4,V12],[Out]).
input_output_vars(le(V1,V,Out),[V1,V],[Out]).


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

#### Computed strongly connected components 
0. recursive  : [fun/3]
1. recursive  : [le/3]
2. recursive [non_tail] : [fun1/6,fun2/7,fun3/7]
3. non_recursive  : [start/6]

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

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

### Specialization of cost equations fun/3 
* CE 15 is refined into CE [21] 
* CE 14 is refined into CE [22] 


### Cost equations --> "Loop" of fun/3 
* CEs [22] --> Loop 13 
* CEs [21] --> Loop 14 

### Ranking functions of CR fun(V1,V,Out) 
* RF of phase [13]: [V,V1]

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


### Specialization of cost equations le/3 
* CE 13 is refined into CE [23] 
* CE 11 is refined into CE [24] 
* CE 10 is refined into CE [25] 
* CE 12 is refined into CE [26] 


### Cost equations --> "Loop" of le/3 
* CEs [26] --> Loop 15 
* CEs [23] --> Loop 16 
* CEs [24] --> Loop 17 
* CEs [25] --> Loop 18 

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

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


### Specialization of cost equations fun1/6 
* CE 16 is refined into CE [27,28,29,30,31,32,33,34,35,36,37,38,39,40,41,42,43,44] 
* CE 19 is refined into CE [45,46,47,48,49,50,51,52] 
* CE 20 is refined into CE [53] 
* CE 18 is refined into CE [54,55,56,57,58,59] 
* CE 17 is refined into CE [60,61,62,63,64,65] 


### Cost equations --> "Loop" of fun1/6 
* CEs [58] --> Loop 19 
* CEs [56] --> Loop 20 
* CEs [57] --> Loop 21 
* CEs [59] --> Loop 22 
* CEs [64] --> Loop 23 
* CEs [65] --> Loop 24 
* CEs [62] --> Loop 25 
* CEs [63] --> Loop 26 
* CEs [55] --> Loop 27 
* CEs [54] --> Loop 28 
* CEs [61] --> Loop 29 
* CEs [60] --> Loop 30 
* CEs [39] --> Loop 31 
* CEs [35,43] --> Loop 32 
* CEs [34,38,42] --> Loop 33 
* CEs [52] --> Loop 34 
* CEs [36,40,44] --> Loop 35 
* CEs [33,37,41,48,50] --> Loop 36 
* CEs [53] --> Loop 37 
* CEs [30] --> Loop 38 
* CEs [28,32] --> Loop 39 
* CEs [27,29,31] --> Loop 40 
* CEs [46] --> Loop 41 
* CEs [45,47,49,51] --> Loop 42 

### Ranking functions of CR fun1(V1,V,V6,V5,V4,Out) 
* RF of phase [19,20,21,22,23,24,25,26]: [V1-V6]

#### Partial ranking functions of CR fun1(V1,V,V6,V5,V4,Out) 
* Partial RF of phase [19,20,21,22,23,24,25,26]:
  - RF of loop [19:1,20:1,21:1,22:1]:
    V-V5-1 depends on loops [23:1,24:1,25:1,26:1] 
  - RF of loop [19:1,20:1,21:1,22:1,23:1,24:1,25:1,26:1]:
    V1-V6


### Specialization of cost equations start/6 
* CE 4 is refined into CE [66,67,68,69,70,71,72,73,74,75,76,77,78,79,80,81] 
* CE 1 is refined into CE [82,83,84,85,86,87,88] 
* CE 2 is refined into CE [89] 
* CE 3 is refined into CE [90,91,92,93,94,95,96,97,98] 
* CE 5 is refined into CE [99,100,101,102,103,104,105,106] 
* CE 6 is refined into CE [107,108,109,110,111,112,113,114,115,116,117,118,119,120,121,122] 
* CE 7 is refined into CE [123,124] 
* CE 8 is refined into CE [125,126,127,128,129,130,131,132,133,134,135,136,137,138,139,140] 
* CE 9 is refined into CE [141,142,143,144,145] 


### Cost equations --> "Loop" of start/6 
* CEs [125,126,127,128,130,131,132,133,134,135,136,137] --> Loop 43 
* CEs [142] --> Loop 44 
* CEs [66,67,68,69,70,71,72,73,74,75,76,77,78,79,80,81] --> Loop 45 
* CEs [107,108,109,110,112,113,114,115,116,117,118,119] --> Loop 46 
* CEs [82,83,84,85,86,87,88,90,91,92,93,94,95,96,97,98,99,100,101,102,103,104,105,106,111,120,121,122] --> Loop 47 
* CEs [89,123,124,129,138,139,140,141,143,144,145] --> Loop 48 

### Ranking functions of CR start(V1,V,V6,V5,V4,V12) 

#### Partial ranking functions of CR start(V1,V,V6,V5,V4,V12) 


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

#### Cost of chains of fun(V1,V,Out):
* Chain [[13],14]: 1*it(13)+0
  Such that:it(13) =< Out

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

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


#### Cost of chains of le(V1,V,Out):
* Chain [[15],18]: 0
  with precondition: [Out=2,V1>=1,V>=V1] 

* Chain [[15],17]: 0
  with precondition: [Out=1,V>=1,V1>=V+1] 

* Chain [[15],16]: 0
  with precondition: [Out=0,V1>=1,V>=1] 

* Chain [18]: 0
  with precondition: [V1=0,Out=2,V>=0] 

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

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


#### Cost of chains of fun1(V1,V,V6,V5,V4,Out):
* Chain [[19,20,21,22,23,24,25,26],42]: 15*it(19)+3*it(24)+6*it(25)+1*s(17)+1*s(18)+1*s(19)+1*s(20)+1*s(21)+1*s(22)+1*s(23)+1*s(24)+1
  Such that:aux(9) =< V1
aux(27) =< V1+V-V6+V5
aux(31) =< 2*V1+V-V6+V5
aux(34) =< V+V5
aux(36) =< V1-V6
aux(37) =< V1-V6+V5
it(24) =< aux(27)
it(25) =< aux(27)
s(21) =< aux(27)
it(24) =< aux(37)
it(25) =< aux(37)
s(21) =< aux(37)
it(19) =< aux(36)
it(24) =< aux(36)
it(25) =< aux(36)
it(25) =< aux(31)
s(22) =< aux(31)
s(22) =< aux(37)
aux(23) =< aux(9)-1
aux(11) =< aux(9)
aux(12) =< aux(34)
s(24) =< it(25)*aux(23)
s(23) =< it(24)*aux(11)
s(19) =< it(19)*aux(12)
s(20) =< it(19)*aux(11)
s(18) =< it(19)*aux(9)
s(17) =< it(19)*aux(34)

  with precondition: [V>=1,V6>=1,V5>=0,V4>=0,Out>=4,V1>=V6+1] 

* Chain [[19,20,21,22,23,24,25,26],37]: 15*it(19)+3*it(24)+6*it(25)+1*s(17)+1*s(18)+1*s(19)+1*s(20)+1*s(21)+1*s(22)+1*s(23)+1*s(24)+0
  Such that:aux(9) =< V1
aux(27) =< V1+V-V6+V5
aux(31) =< 2*V1+V-V6+V5
aux(34) =< V+V5
aux(38) =< V1-V6
aux(39) =< V1-V6+V5
it(24) =< aux(27)
it(25) =< aux(27)
s(21) =< aux(27)
it(24) =< aux(39)
it(25) =< aux(39)
s(21) =< aux(39)
it(19) =< aux(38)
it(24) =< aux(38)
it(25) =< aux(38)
it(25) =< aux(31)
s(22) =< aux(31)
s(22) =< aux(39)
aux(23) =< aux(9)-1
aux(11) =< aux(9)
aux(12) =< aux(34)
s(24) =< it(25)*aux(23)
s(23) =< it(24)*aux(11)
s(19) =< it(19)*aux(12)
s(20) =< it(19)*aux(11)
s(18) =< it(19)*aux(9)
s(17) =< it(19)*aux(34)

  with precondition: [V>=1,V6>=1,V5>=0,V4>=0,Out>=3,V1>=V6+1] 

* Chain [[19,20,21,22,23,24,25,26],36]: 15*it(19)+3*it(24)+6*it(25)+1*s(17)+1*s(18)+1*s(19)+1*s(20)+1*s(21)+1*s(22)+1*s(23)+1*s(24)+2*s(25)+2
  Such that:aux(27) =< V1+V-V6+V5
aux(31) =< 2*V1+V-V6+V5
aux(34) =< V+V5
aux(41) =< V1
aux(42) =< V1-V6
aux(43) =< V1-V6+V5
s(25) =< aux(41)
it(24) =< aux(27)
it(25) =< aux(27)
s(21) =< aux(27)
it(24) =< aux(43)
it(25) =< aux(43)
s(21) =< aux(43)
it(19) =< aux(42)
it(24) =< aux(42)
it(25) =< aux(42)
it(25) =< aux(31)
s(22) =< aux(31)
s(22) =< aux(43)
aux(23) =< aux(41)-1
aux(11) =< aux(41)
aux(12) =< aux(34)
s(24) =< it(25)*aux(23)
s(23) =< it(24)*aux(11)
s(19) =< it(19)*aux(12)
s(20) =< it(19)*aux(11)
s(18) =< it(19)*aux(41)
s(17) =< it(19)*aux(34)

  with precondition: [V>=1,V6>=1,V5>=0,V4>=0,Out>=5,V1>=V6+1] 

* Chain [[19,20,21,22,23,24,25,26],35]: 15*it(19)+3*it(24)+6*it(25)+1*s(17)+1*s(18)+1*s(19)+1*s(20)+1*s(21)+1*s(22)+1*s(23)+1*s(24)+2*s(27)+3*s(28)+1*s(29)+2
  Such that:aux(27) =< V1+V-V6+V5
aux(31) =< 2*V1+V-V6+V5
aux(44) =< V
aux(34) =< V+V5
aux(46) =< V1
aux(47) =< V1-V6
aux(48) =< V1-V6+V5
s(29) =< aux(48)
s(27) =< aux(44)
s(28) =< aux(46)
it(24) =< aux(27)
it(25) =< aux(27)
s(21) =< aux(27)
it(24) =< aux(48)
it(25) =< aux(48)
s(21) =< aux(48)
it(19) =< aux(47)
it(24) =< aux(47)
it(25) =< aux(47)
it(25) =< aux(31)
s(22) =< aux(31)
s(22) =< aux(48)
aux(23) =< aux(46)-1
aux(11) =< aux(46)
aux(12) =< aux(34)
s(24) =< it(25)*aux(23)
s(23) =< it(24)*aux(11)
s(19) =< it(19)*aux(12)
s(20) =< it(19)*aux(11)
s(18) =< it(19)*aux(46)
s(17) =< it(19)*aux(34)

  with precondition: [V>=1,V6>=1,V5>=0,V4>=0,Out>=7,V1>=V6+2] 

* Chain [[19,20,21,22,23,24,25,26],34]: 15*it(19)+3*it(24)+6*it(25)+1*s(17)+1*s(18)+1*s(19)+1*s(20)+1*s(21)+1*s(22)+1*s(23)+1*s(24)+1*s(33)+1
  Such that:aux(27) =< V1+V-V6+V5
aux(31) =< 2*V1+V-V6+V5
aux(34) =< V+V5
aux(49) =< V1
aux(50) =< V1-V6
aux(51) =< V1-V6+V5
s(33) =< aux(49)
it(24) =< aux(27)
it(25) =< aux(27)
s(21) =< aux(27)
it(24) =< aux(51)
it(25) =< aux(51)
s(21) =< aux(51)
it(19) =< aux(50)
it(24) =< aux(50)
it(25) =< aux(50)
it(25) =< aux(31)
s(22) =< aux(31)
s(22) =< aux(51)
aux(23) =< aux(49)-1
aux(11) =< aux(49)
aux(12) =< aux(34)
s(24) =< it(25)*aux(23)
s(23) =< it(24)*aux(11)
s(19) =< it(19)*aux(12)
s(20) =< it(19)*aux(11)
s(18) =< it(19)*aux(49)
s(17) =< it(19)*aux(34)

  with precondition: [V>=1,V6>=1,V5>=0,V4>=0,V1>=V6+1,Out+3*V6>=3*V1+2] 

* Chain [[19,20,21,22,23,24,25,26],33]: 15*it(19)+3*it(24)+6*it(25)+1*s(17)+1*s(18)+1*s(19)+1*s(20)+1*s(21)+1*s(22)+1*s(23)+1*s(24)+3*s(34)+2
  Such that:aux(27) =< V1+V-V6+V5
aux(31) =< 2*V1+V-V6+V5
aux(34) =< V+V5
aux(53) =< V1
aux(54) =< V1-V6
aux(55) =< V1-V6+V5
s(34) =< aux(53)
it(24) =< aux(27)
it(25) =< aux(27)
s(21) =< aux(27)
it(24) =< aux(55)
it(25) =< aux(55)
s(21) =< aux(55)
it(19) =< aux(54)
it(24) =< aux(54)
it(25) =< aux(54)
it(25) =< aux(31)
s(22) =< aux(31)
s(22) =< aux(55)
aux(23) =< aux(53)-1
aux(11) =< aux(53)
aux(12) =< aux(34)
s(24) =< it(25)*aux(23)
s(23) =< it(24)*aux(11)
s(19) =< it(19)*aux(12)
s(20) =< it(19)*aux(11)
s(18) =< it(19)*aux(53)
s(17) =< it(19)*aux(34)

  with precondition: [V>=1,V6>=1,V5>=0,V4>=0,Out>=6,V1>=V6+2] 

* Chain [[19,20,21,22,23,24,25,26],32]: 15*it(19)+3*it(24)+6*it(25)+1*s(17)+1*s(18)+1*s(19)+1*s(20)+1*s(21)+1*s(22)+1*s(23)+1*s(24)+2*s(37)+2
  Such that:aux(9) =< V1
aux(27) =< V1+V-V6+V5
aux(31) =< 2*V1+V-V6+V5
aux(56) =< V
aux(34) =< V+V5
aux(57) =< V1-V6
aux(58) =< V1-V6+V5
s(37) =< aux(56)
it(24) =< aux(27)
it(25) =< aux(27)
s(21) =< aux(27)
it(24) =< aux(58)
it(25) =< aux(58)
s(21) =< aux(58)
it(19) =< aux(57)
it(24) =< aux(57)
it(25) =< aux(57)
it(25) =< aux(31)
s(22) =< aux(31)
s(22) =< aux(58)
aux(23) =< aux(9)-1
aux(11) =< aux(9)
aux(12) =< aux(34)
s(24) =< it(25)*aux(23)
s(23) =< it(24)*aux(11)
s(19) =< it(19)*aux(12)
s(20) =< it(19)*aux(11)
s(18) =< it(19)*aux(9)
s(17) =< it(19)*aux(34)

  with precondition: [V>=1,V6>=1,V5>=0,V4>=0,Out>=6,V1>=V6+2] 

* Chain [[19,20,21,22,23,24,25,26],31]: 15*it(19)+3*it(24)+6*it(25)+1*s(17)+1*s(18)+1*s(19)+1*s(20)+1*s(21)+1*s(22)+1*s(23)+1*s(24)+1*s(39)+2
  Such that:aux(9) =< V1
aux(27) =< V1+V-V6+V5
aux(31) =< 2*V1+V-V6+V5
aux(34) =< V+V5
aux(59) =< V1-V6
aux(60) =< V1-V6+V5
s(39) =< aux(60)
it(24) =< aux(27)
it(25) =< aux(27)
s(21) =< aux(27)
it(24) =< aux(60)
it(25) =< aux(60)
s(21) =< aux(60)
it(19) =< aux(59)
it(24) =< aux(59)
it(25) =< aux(59)
it(25) =< aux(31)
s(22) =< aux(31)
s(22) =< aux(60)
aux(23) =< aux(9)-1
aux(11) =< aux(9)
aux(12) =< aux(34)
s(24) =< it(25)*aux(23)
s(23) =< it(24)*aux(11)
s(19) =< it(19)*aux(12)
s(20) =< it(19)*aux(11)
s(18) =< it(19)*aux(9)
s(17) =< it(19)*aux(34)

  with precondition: [V>=2,V6>=1,V5>=0,V4>=0,Out>=6,V1>=V6+2,Out+3*V+3*V5>=15,V+V1+V5>=V6+5] 

* Chain [42]: 1
  with precondition: [Out=1,V1>=0,V>=1,V6>=0,V5>=0,V4>=0] 

* Chain [41]: 1
  with precondition: [V6=0,Out=1,V1>=1,V>=1,V5>=0,V4>=0] 

* Chain [40]: 2
  with precondition: [V6=0,Out=2,V1>=1,V>=1,V5>=0,V4>=0] 

* Chain [39]: 2*s(40)+2
  Such that:aux(61) =< V
s(40) =< aux(61)

  with precondition: [V6=0,V1>=1,V4>=0,Out>=3,V+2>=Out,V5+3>=Out] 

* Chain [38]: 1*s(42)+2
  Such that:s(42) =< V5+1

  with precondition: [V6=0,V1>=1,V4>=0,Out>=3,V>=V5+2,V5+3>=Out] 

* Chain [37]: 0
  with precondition: [Out=0,V1>=0,V>=0,V6>=0,V5>=0,V4>=0] 

* Chain [36]: 2*s(25)+2
  Such that:aux(40) =< V6
s(25) =< aux(40)

  with precondition: [V>=1,V5>=0,V4>=0,Out>=2,V1+1>=Out,V6+1>=Out] 

* Chain [35]: 2*s(27)+3*s(28)+1*s(29)+2
  Such that:s(29) =< V5+1
aux(44) =< V
aux(45) =< V6
s(27) =< aux(44)
s(28) =< aux(45)

  with precondition: [V>=1,V6>=1,V5>=0,V4>=0,Out>=4,V1>=V6+1,V+V6+2>=Out,V5+V6+3>=Out] 

* Chain [34]: 1*s(33)+1
  Such that:s(33) =< V1

  with precondition: [V>=1,V5>=0,V4>=0,Out>=2,V6>=V1,V1+1>=Out] 

* Chain [33]: 3*s(34)+2
  Such that:aux(52) =< V6
s(34) =< aux(52)

  with precondition: [V>=1,V5>=0,V4>=0,Out>=3,V1>=V6+1,V6+2>=Out] 

* Chain [32]: 2*s(37)+2
  Such that:aux(56) =< V
s(37) =< aux(56)

  with precondition: [V6>=1,V4>=0,Out>=3,V1>=V6+1,V+2>=Out,V5+3>=Out] 

* Chain [31]: 1*s(39)+2
  Such that:s(39) =< V5+1

  with precondition: [V6>=1,V4>=0,Out>=3,V1>=V6+1,V>=V5+2,V5+3>=Out] 

* Chain [30,[19,20,21,22,23,24,25,26],42]: 15*it(19)+4*it(24)+6*it(25)+1*s(17)+1*s(18)+1*s(19)+1*s(20)+1*s(22)+1*s(23)+1*s(24)+4
  Such that:aux(27) =< V1+V
aux(31) =< 2*V1+V
aux(34) =< V
aux(62) =< V1
it(24) =< aux(27)
it(25) =< aux(27)
it(24) =< aux(62)
it(25) =< aux(62)
it(19) =< aux(62)
it(25) =< aux(31)
s(22) =< aux(31)
s(22) =< aux(62)
aux(23) =< aux(62)-1
aux(11) =< aux(62)
aux(12) =< aux(34)
s(24) =< it(25)*aux(23)
s(23) =< it(24)*aux(11)
s(19) =< it(19)*aux(12)
s(20) =< it(19)*aux(11)
s(18) =< it(19)*aux(62)
s(17) =< it(19)*aux(34)

  with precondition: [V6=0,V1>=2,V>=1,V4>=0,Out>=7,V5+1>=V] 

* Chain [30,[19,20,21,22,23,24,25,26],37]: 15*it(19)+4*it(24)+6*it(25)+1*s(17)+1*s(18)+1*s(19)+1*s(20)+1*s(22)+1*s(23)+1*s(24)+3
  Such that:aux(27) =< V1+V
aux(31) =< 2*V1+V
aux(34) =< V
aux(63) =< V1
it(24) =< aux(27)
it(25) =< aux(27)
it(24) =< aux(63)
it(25) =< aux(63)
it(19) =< aux(63)
it(25) =< aux(31)
s(22) =< aux(31)
s(22) =< aux(63)
aux(23) =< aux(63)-1
aux(11) =< aux(63)
aux(12) =< aux(34)
s(24) =< it(25)*aux(23)
s(23) =< it(24)*aux(11)
s(19) =< it(19)*aux(12)
s(20) =< it(19)*aux(11)
s(18) =< it(19)*aux(63)
s(17) =< it(19)*aux(34)

  with precondition: [V6=0,V1>=2,V>=1,V4>=0,Out>=6,V5+1>=V] 

* Chain [30,[19,20,21,22,23,24,25,26],36]: 17*it(19)+4*it(24)+6*it(25)+1*s(17)+1*s(18)+1*s(19)+1*s(20)+1*s(22)+1*s(23)+1*s(24)+5
  Such that:aux(27) =< V1+V
aux(31) =< 2*V1+V
aux(34) =< V
aux(64) =< V1
it(19) =< aux(64)
it(24) =< aux(27)
it(25) =< aux(27)
it(24) =< aux(64)
it(25) =< aux(64)
it(25) =< aux(31)
s(22) =< aux(31)
s(22) =< aux(64)
aux(23) =< aux(64)-1
aux(11) =< aux(64)
aux(12) =< aux(34)
s(24) =< it(25)*aux(23)
s(23) =< it(24)*aux(11)
s(19) =< it(19)*aux(12)
s(20) =< it(19)*aux(11)
s(18) =< it(19)*aux(64)
s(17) =< it(19)*aux(34)

  with precondition: [V6=0,V1>=2,V>=1,V4>=0,Out>=8,V5+1>=V] 

* Chain [30,[19,20,21,22,23,24,25,26],35]: 19*it(19)+4*it(24)+6*it(25)+1*s(17)+1*s(18)+1*s(19)+1*s(20)+1*s(22)+1*s(23)+1*s(24)+2*s(27)+5
  Such that:aux(27) =< V1+V
aux(31) =< 2*V1+V
aux(65) =< V1
aux(66) =< V
it(19) =< aux(65)
s(27) =< aux(66)
it(24) =< aux(27)
it(25) =< aux(27)
it(24) =< aux(65)
it(25) =< aux(65)
it(25) =< aux(31)
s(22) =< aux(31)
s(22) =< aux(65)
aux(23) =< aux(65)-1
aux(11) =< aux(65)
aux(12) =< aux(66)
s(24) =< it(25)*aux(23)
s(23) =< it(24)*aux(11)
s(19) =< it(19)*aux(12)
s(20) =< it(19)*aux(11)
s(18) =< it(19)*aux(65)
s(17) =< it(19)*aux(66)

  with precondition: [V6=0,V1>=3,V>=1,V4>=0,Out>=10,V5+1>=V] 

* Chain [30,[19,20,21,22,23,24,25,26],34]: 16*it(19)+4*it(24)+6*it(25)+1*s(17)+1*s(18)+1*s(19)+1*s(20)+1*s(22)+1*s(23)+1*s(24)+4
  Such that:aux(27) =< V1+V
aux(31) =< 2*V1+V
aux(34) =< V
aux(67) =< V1
it(19) =< aux(67)
it(24) =< aux(27)
it(25) =< aux(27)
it(24) =< aux(67)
it(25) =< aux(67)
it(25) =< aux(31)
s(22) =< aux(31)
s(22) =< aux(67)
aux(23) =< aux(67)-1
aux(11) =< aux(67)
aux(12) =< aux(34)
s(24) =< it(25)*aux(23)
s(23) =< it(24)*aux(11)
s(19) =< it(19)*aux(12)
s(20) =< it(19)*aux(11)
s(18) =< it(19)*aux(67)
s(17) =< it(19)*aux(34)

  with precondition: [V6=0,V1>=2,V>=1,V4>=0,Out>=3*V1+2,V5+1>=V] 

* Chain [30,[19,20,21,22,23,24,25,26],33]: 18*it(19)+4*it(24)+6*it(25)+1*s(17)+1*s(18)+1*s(19)+1*s(20)+1*s(22)+1*s(23)+1*s(24)+5
  Such that:aux(27) =< V1+V
aux(31) =< 2*V1+V
aux(34) =< V
aux(68) =< V1
it(19) =< aux(68)
it(24) =< aux(27)
it(25) =< aux(27)
it(24) =< aux(68)
it(25) =< aux(68)
it(25) =< aux(31)
s(22) =< aux(31)
s(22) =< aux(68)
aux(23) =< aux(68)-1
aux(11) =< aux(68)
aux(12) =< aux(34)
s(24) =< it(25)*aux(23)
s(23) =< it(24)*aux(11)
s(19) =< it(19)*aux(12)
s(20) =< it(19)*aux(11)
s(18) =< it(19)*aux(68)
s(17) =< it(19)*aux(34)

  with precondition: [V6=0,V1>=3,V>=1,V4>=0,Out>=9,V5+1>=V] 

* Chain [30,[19,20,21,22,23,24,25,26],32]: 15*it(19)+4*it(24)+6*it(25)+1*s(17)+1*s(18)+1*s(19)+1*s(20)+1*s(22)+1*s(23)+1*s(24)+2*s(37)+5
  Such that:aux(27) =< V1+V
aux(31) =< 2*V1+V
aux(69) =< V1
aux(70) =< V
s(37) =< aux(70)
it(24) =< aux(27)
it(25) =< aux(27)
it(24) =< aux(69)
it(25) =< aux(69)
it(19) =< aux(69)
it(25) =< aux(31)
s(22) =< aux(31)
s(22) =< aux(69)
aux(23) =< aux(69)-1
aux(11) =< aux(69)
aux(12) =< aux(70)
s(24) =< it(25)*aux(23)
s(23) =< it(24)*aux(11)
s(19) =< it(19)*aux(12)
s(20) =< it(19)*aux(11)
s(18) =< it(19)*aux(69)
s(17) =< it(19)*aux(70)

  with precondition: [V6=0,V1>=3,V>=1,V4>=0,Out>=9,V5+1>=V] 

* Chain [30,[19,20,21,22,23,24,25,26],31]: 16*it(19)+4*it(24)+6*it(25)+1*s(17)+1*s(18)+1*s(19)+1*s(20)+1*s(22)+1*s(23)+1*s(24)+5
  Such that:aux(27) =< V1+V
aux(31) =< 2*V1+V
aux(34) =< V
aux(71) =< V1
it(19) =< aux(71)
it(24) =< aux(27)
it(25) =< aux(27)
it(24) =< aux(71)
it(25) =< aux(71)
it(25) =< aux(31)
s(22) =< aux(31)
s(22) =< aux(71)
aux(23) =< aux(71)-1
aux(11) =< aux(71)
aux(12) =< aux(34)
s(24) =< it(25)*aux(23)
s(23) =< it(24)*aux(11)
s(19) =< it(19)*aux(12)
s(20) =< it(19)*aux(11)
s(18) =< it(19)*aux(71)
s(17) =< it(19)*aux(34)

  with precondition: [V6=0,V1>=3,V>=2,V4>=0,Out>=9,V5+1>=V,V+V1>=6,Out+3*V>=18] 

* Chain [30,42]: 4
  with precondition: [V6=0,Out=4,V1>=1,V>=1,V4>=0,V5+1>=V] 

* Chain [30,37]: 3
  with precondition: [V6=0,Out=3,V1>=1,V>=1,V4>=0,V5+1>=V] 

* Chain [30,36]: 2*s(25)+5
  Such that:aux(40) =< 1
s(25) =< aux(40)

  with precondition: [V6=0,Out=5,V1>=1,V>=1,V4>=0,V5+1>=V] 

* Chain [30,35]: 2*s(27)+4*s(28)+5
  Such that:aux(44) =< V
aux(72) =< 1
s(28) =< aux(72)
s(27) =< aux(44)

  with precondition: [V6=0,Out=7,V1>=2,V>=1,V4>=0,V5+1>=V] 

* Chain [30,34]: 1*s(33)+4
  Such that:s(33) =< 1

  with precondition: [V1=1,V6=0,Out=5,V>=1,V4>=0,V5+1>=V] 

* Chain [30,33]: 3*s(34)+5
  Such that:aux(52) =< 1
s(34) =< aux(52)

  with precondition: [V6=0,Out=6,V1>=2,V>=1,V4>=0,V5+1>=V] 

* Chain [30,32]: 2*s(37)+5
  Such that:aux(56) =< V
s(37) =< aux(56)

  with precondition: [V6=0,Out=6,V1>=2,V>=1,V4>=0,V5+1>=V] 

* Chain [30,31]: 1*s(39)+5
  Such that:s(39) =< 1

  with precondition: [V6=0,Out=6,V1>=2,V>=2,V4>=0,V5+1>=V] 

* Chain [29,[19,20,21,22,23,24,25,26],42]: 15*it(19)+4*it(24)+6*it(25)+1*s(17)+1*s(18)+1*s(19)+1*s(20)+1*s(22)+1*s(23)+1*s(24)+1*s(43)+4
  Such that:aux(27) =< V1+V
aux(31) =< 2*V1+V
aux(73) =< V1
aux(74) =< V
s(43) =< aux(74)
it(24) =< aux(27)
it(25) =< aux(27)
it(24) =< aux(73)
it(25) =< aux(73)
it(19) =< aux(73)
it(25) =< aux(31)
s(22) =< aux(31)
s(22) =< aux(73)
aux(23) =< aux(73)-1
aux(11) =< aux(73)
aux(12) =< aux(74)
s(24) =< it(25)*aux(23)
s(23) =< it(24)*aux(11)
s(19) =< it(19)*aux(12)
s(20) =< it(19)*aux(11)
s(18) =< it(19)*aux(73)
s(17) =< it(19)*aux(74)

  with precondition: [V6=0,V1>=2,V>=1,V4>=0,Out>=8,V5+1>=V] 

* Chain [29,[19,20,21,22,23,24,25,26],37]: 15*it(19)+4*it(24)+6*it(25)+1*s(17)+1*s(18)+1*s(19)+1*s(20)+1*s(22)+1*s(23)+1*s(24)+1*s(43)+3
  Such that:aux(27) =< V1+V
aux(31) =< 2*V1+V
aux(75) =< V1
aux(76) =< V
s(43) =< aux(76)
it(24) =< aux(27)
it(25) =< aux(27)
it(24) =< aux(75)
it(25) =< aux(75)
it(19) =< aux(75)
it(25) =< aux(31)
s(22) =< aux(31)
s(22) =< aux(75)
aux(23) =< aux(75)-1
aux(11) =< aux(75)
aux(12) =< aux(76)
s(24) =< it(25)*aux(23)
s(23) =< it(24)*aux(11)
s(19) =< it(19)*aux(12)
s(20) =< it(19)*aux(11)
s(18) =< it(19)*aux(75)
s(17) =< it(19)*aux(76)

  with precondition: [V6=0,V1>=2,V>=1,V4>=0,Out>=7,V5+1>=V] 

* Chain [29,[19,20,21,22,23,24,25,26],36]: 17*it(19)+4*it(24)+6*it(25)+1*s(17)+1*s(18)+1*s(19)+1*s(20)+1*s(22)+1*s(23)+1*s(24)+1*s(43)+5
  Such that:aux(27) =< V1+V
aux(31) =< 2*V1+V
aux(77) =< V1
aux(78) =< V
s(43) =< aux(78)
it(19) =< aux(77)
it(24) =< aux(27)
it(25) =< aux(27)
it(24) =< aux(77)
it(25) =< aux(77)
it(25) =< aux(31)
s(22) =< aux(31)
s(22) =< aux(77)
aux(23) =< aux(77)-1
aux(11) =< aux(77)
aux(12) =< aux(78)
s(24) =< it(25)*aux(23)
s(23) =< it(24)*aux(11)
s(19) =< it(19)*aux(12)
s(20) =< it(19)*aux(11)
s(18) =< it(19)*aux(77)
s(17) =< it(19)*aux(78)

  with precondition: [V6=0,V1>=2,V>=1,V4>=0,Out>=9,V5+1>=V] 

* Chain [29,[19,20,21,22,23,24,25,26],35]: 19*it(19)+4*it(24)+6*it(25)+1*s(17)+1*s(18)+1*s(19)+1*s(20)+1*s(22)+1*s(23)+1*s(24)+3*s(27)+5
  Such that:aux(27) =< V1+V
aux(31) =< 2*V1+V
aux(79) =< V1
aux(80) =< V
s(27) =< aux(80)
it(19) =< aux(79)
it(24) =< aux(27)
it(25) =< aux(27)
it(24) =< aux(79)
it(25) =< aux(79)
it(25) =< aux(31)
s(22) =< aux(31)
s(22) =< aux(79)
aux(23) =< aux(79)-1
aux(11) =< aux(79)
aux(12) =< aux(80)
s(24) =< it(25)*aux(23)
s(23) =< it(24)*aux(11)
s(19) =< it(19)*aux(12)
s(20) =< it(19)*aux(11)
s(18) =< it(19)*aux(79)
s(17) =< it(19)*aux(80)

  with precondition: [V6=0,V1>=3,V>=1,V4>=0,Out>=11,V5+1>=V] 

* Chain [29,[19,20,21,22,23,24,25,26],34]: 16*it(19)+4*it(24)+6*it(25)+1*s(17)+1*s(18)+1*s(19)+1*s(20)+1*s(22)+1*s(23)+1*s(24)+1*s(43)+4
  Such that:aux(27) =< V1+V
aux(31) =< 2*V1+V
aux(81) =< V1
aux(82) =< V
s(43) =< aux(82)
it(19) =< aux(81)
it(24) =< aux(27)
it(25) =< aux(27)
it(24) =< aux(81)
it(25) =< aux(81)
it(25) =< aux(31)
s(22) =< aux(31)
s(22) =< aux(81)
aux(23) =< aux(81)-1
aux(11) =< aux(81)
aux(12) =< aux(82)
s(24) =< it(25)*aux(23)
s(23) =< it(24)*aux(11)
s(19) =< it(19)*aux(12)
s(20) =< it(19)*aux(11)
s(18) =< it(19)*aux(81)
s(17) =< it(19)*aux(82)

  with precondition: [V6=0,V1>=2,V>=1,V4>=0,Out>=3*V1+3,V5+1>=V] 

* Chain [29,[19,20,21,22,23,24,25,26],33]: 18*it(19)+4*it(24)+6*it(25)+1*s(17)+1*s(18)+1*s(19)+1*s(20)+1*s(22)+1*s(23)+1*s(24)+1*s(43)+5
  Such that:aux(27) =< V1+V
aux(31) =< 2*V1+V
aux(83) =< V1
aux(84) =< V
s(43) =< aux(84)
it(19) =< aux(83)
it(24) =< aux(27)
it(25) =< aux(27)
it(24) =< aux(83)
it(25) =< aux(83)
it(25) =< aux(31)
s(22) =< aux(31)
s(22) =< aux(83)
aux(23) =< aux(83)-1
aux(11) =< aux(83)
aux(12) =< aux(84)
s(24) =< it(25)*aux(23)
s(23) =< it(24)*aux(11)
s(19) =< it(19)*aux(12)
s(20) =< it(19)*aux(11)
s(18) =< it(19)*aux(83)
s(17) =< it(19)*aux(84)

  with precondition: [V6=0,V1>=3,V>=1,V4>=0,Out>=10,V5+1>=V] 

* Chain [29,[19,20,21,22,23,24,25,26],32]: 15*it(19)+4*it(24)+6*it(25)+1*s(17)+1*s(18)+1*s(19)+1*s(20)+1*s(22)+1*s(23)+1*s(24)+3*s(37)+5
  Such that:aux(27) =< V1+V
aux(31) =< 2*V1+V
aux(85) =< V1
aux(86) =< V
s(37) =< aux(86)
it(24) =< aux(27)
it(25) =< aux(27)
it(24) =< aux(85)
it(25) =< aux(85)
it(19) =< aux(85)
it(25) =< aux(31)
s(22) =< aux(31)
s(22) =< aux(85)
aux(23) =< aux(85)-1
aux(11) =< aux(85)
aux(12) =< aux(86)
s(24) =< it(25)*aux(23)
s(23) =< it(24)*aux(11)
s(19) =< it(19)*aux(12)
s(20) =< it(19)*aux(11)
s(18) =< it(19)*aux(85)
s(17) =< it(19)*aux(86)

  with precondition: [V6=0,V1>=3,V>=1,V4>=0,Out>=10,V5+1>=V] 

* Chain [29,[19,20,21,22,23,24,25,26],31]: 16*it(19)+4*it(24)+6*it(25)+1*s(17)+1*s(18)+1*s(19)+1*s(20)+1*s(22)+1*s(23)+1*s(24)+1*s(43)+5
  Such that:aux(27) =< V1+V
aux(31) =< 2*V1+V
aux(87) =< V1
aux(88) =< V
s(43) =< aux(88)
it(19) =< aux(87)
it(24) =< aux(27)
it(25) =< aux(27)
it(24) =< aux(87)
it(25) =< aux(87)
it(25) =< aux(31)
s(22) =< aux(31)
s(22) =< aux(87)
aux(23) =< aux(87)-1
aux(11) =< aux(87)
aux(12) =< aux(88)
s(24) =< it(25)*aux(23)
s(23) =< it(24)*aux(11)
s(19) =< it(19)*aux(12)
s(20) =< it(19)*aux(11)
s(18) =< it(19)*aux(87)
s(17) =< it(19)*aux(88)

  with precondition: [V6=0,V1>=3,V>=2,V4>=0,Out>=10,V5+1>=V,V+V1>=6,Out+3*V>=19] 

* Chain [29,42]: 1*s(43)+4
  Such that:s(43) =< V

  with precondition: [V6=0,V1>=1,V4>=0,Out>=5,V5+1>=V,V+4>=Out] 

* Chain [29,37]: 1*s(43)+3
  Such that:s(43) =< V

  with precondition: [V6=0,V1>=1,V4>=0,Out>=4,V5+1>=V,V+3>=Out] 

* Chain [29,36]: 2*s(25)+1*s(43)+5
  Such that:aux(40) =< 1
s(43) =< V
s(25) =< aux(40)

  with precondition: [V6=0,V1>=1,V4>=0,Out>=6,V5+1>=V,V+5>=Out] 

* Chain [29,35]: 3*s(27)+4*s(28)+5
  Such that:aux(89) =< 1
aux(90) =< V
s(28) =< aux(89)
s(27) =< aux(90)

  with precondition: [V6=0,V1>=2,V4>=0,Out>=8,V5+1>=V,V+7>=Out] 

* Chain [29,34]: 1*s(33)+1*s(43)+4
  Such that:s(33) =< 1
s(43) =< V

  with precondition: [V1=1,V6=0,V4>=0,Out>=6,V5+1>=V,V+5>=Out] 

* Chain [29,33]: 3*s(34)+1*s(43)+5
  Such that:aux(52) =< 1
s(43) =< V
s(34) =< aux(52)

  with precondition: [V6=0,V1>=2,V4>=0,Out>=7,V5+1>=V,V+6>=Out] 

* Chain [29,32]: 3*s(37)+5
  Such that:aux(91) =< V
s(37) =< aux(91)

  with precondition: [V6=0,V1>=2,V4>=0,Out>=7,V5+1>=V,V+6>=Out] 

* Chain [29,31]: 1*s(39)+1*s(43)+5
  Such that:s(39) =< 1
s(43) =< V

  with precondition: [V6=0,V1>=2,V>=2,V4>=0,Out>=7,V5+1>=V,V+6>=Out] 

* Chain [28,[19,20,21,22,23,24,25,26],42]: 15*it(19)+3*it(24)+6*it(25)+1*s(17)+1*s(18)+1*s(19)+1*s(20)+1*s(21)+1*s(22)+1*s(23)+1*s(24)+4
  Such that:aux(27) =< V1+V+V5
aux(37) =< V1+V5
aux(31) =< 2*V1+V+V5
aux(34) =< V+V5+1
aux(92) =< V1
it(24) =< aux(27)
it(25) =< aux(27)
s(21) =< aux(27)
it(24) =< aux(37)
it(25) =< aux(37)
s(21) =< aux(37)
it(19) =< aux(92)
it(24) =< aux(92)
it(25) =< aux(92)
it(25) =< aux(31)
s(22) =< aux(31)
s(22) =< aux(37)
aux(23) =< aux(92)-1
aux(11) =< aux(92)
aux(12) =< aux(34)
s(24) =< it(25)*aux(23)
s(23) =< it(24)*aux(11)
s(19) =< it(19)*aux(12)
s(20) =< it(19)*aux(11)
s(18) =< it(19)*aux(92)
s(17) =< it(19)*aux(34)

  with precondition: [V6=0,V1>=2,V5>=0,V4>=0,Out>=7,V>=V5+2] 

* Chain [28,[19,20,21,22,23,24,25,26],37]: 15*it(19)+3*it(24)+6*it(25)+1*s(17)+1*s(18)+1*s(19)+1*s(20)+1*s(21)+1*s(22)+1*s(23)+1*s(24)+3
  Such that:aux(27) =< V1+V+V5
aux(39) =< V1+V5
aux(31) =< 2*V1+V+V5
aux(34) =< V+V5+1
aux(93) =< V1
it(24) =< aux(27)
it(25) =< aux(27)
s(21) =< aux(27)
it(24) =< aux(39)
it(25) =< aux(39)
s(21) =< aux(39)
it(19) =< aux(93)
it(24) =< aux(93)
it(25) =< aux(93)
it(25) =< aux(31)
s(22) =< aux(31)
s(22) =< aux(39)
aux(23) =< aux(93)-1
aux(11) =< aux(93)
aux(12) =< aux(34)
s(24) =< it(25)*aux(23)
s(23) =< it(24)*aux(11)
s(19) =< it(19)*aux(12)
s(20) =< it(19)*aux(11)
s(18) =< it(19)*aux(93)
s(17) =< it(19)*aux(34)

  with precondition: [V6=0,V1>=2,V5>=0,V4>=0,Out>=6,V>=V5+2] 

* Chain [28,[19,20,21,22,23,24,25,26],36]: 17*it(19)+3*it(24)+6*it(25)+1*s(17)+1*s(18)+1*s(19)+1*s(20)+1*s(21)+1*s(22)+1*s(23)+1*s(24)+5
  Such that:aux(27) =< V1+V+V5
aux(43) =< V1+V5
aux(31) =< 2*V1+V+V5
aux(34) =< V+V5+1
aux(94) =< V1
it(19) =< aux(94)
it(24) =< aux(27)
it(25) =< aux(27)
s(21) =< aux(27)
it(24) =< aux(43)
it(25) =< aux(43)
s(21) =< aux(43)
it(24) =< aux(94)
it(25) =< aux(94)
it(25) =< aux(31)
s(22) =< aux(31)
s(22) =< aux(43)
aux(23) =< aux(94)-1
aux(11) =< aux(94)
aux(12) =< aux(34)
s(24) =< it(25)*aux(23)
s(23) =< it(24)*aux(11)
s(19) =< it(19)*aux(12)
s(20) =< it(19)*aux(11)
s(18) =< it(19)*aux(94)
s(17) =< it(19)*aux(34)

  with precondition: [V6=0,V1>=2,V5>=0,V4>=0,Out>=8,V>=V5+2] 

* Chain [28,[19,20,21,22,23,24,25,26],35]: 18*it(19)+3*it(24)+6*it(25)+1*s(17)+1*s(18)+1*s(19)+1*s(20)+1*s(21)+1*s(22)+1*s(23)+1*s(24)+2*s(27)+1*s(29)+5
  Such that:aux(27) =< V1+V+V5
aux(48) =< V1+V5
aux(31) =< 2*V1+V+V5
aux(44) =< V
aux(34) =< V+V5+1
aux(95) =< V1
s(29) =< aux(48)
s(27) =< aux(44)
it(19) =< aux(95)
it(24) =< aux(27)
it(25) =< aux(27)
s(21) =< aux(27)
it(24) =< aux(48)
it(25) =< aux(48)
s(21) =< aux(48)
it(24) =< aux(95)
it(25) =< aux(95)
it(25) =< aux(31)
s(22) =< aux(31)
s(22) =< aux(48)
aux(23) =< aux(95)-1
aux(11) =< aux(95)
aux(12) =< aux(34)
s(24) =< it(25)*aux(23)
s(23) =< it(24)*aux(11)
s(19) =< it(19)*aux(12)
s(20) =< it(19)*aux(11)
s(18) =< it(19)*aux(95)
s(17) =< it(19)*aux(34)

  with precondition: [V6=0,V1>=3,V5>=0,V4>=0,Out>=10,V>=V5+2] 

* Chain [28,[19,20,21,22,23,24,25,26],34]: 16*it(19)+3*it(24)+6*it(25)+1*s(17)+1*s(18)+1*s(19)+1*s(20)+1*s(21)+1*s(22)+1*s(23)+1*s(24)+4
  Such that:aux(27) =< V1+V+V5
aux(51) =< V1+V5
aux(31) =< 2*V1+V+V5
aux(34) =< V+V5+1
aux(96) =< V1
it(19) =< aux(96)
it(24) =< aux(27)
it(25) =< aux(27)
s(21) =< aux(27)
it(24) =< aux(51)
it(25) =< aux(51)
s(21) =< aux(51)
it(24) =< aux(96)
it(25) =< aux(96)
it(25) =< aux(31)
s(22) =< aux(31)
s(22) =< aux(51)
aux(23) =< aux(96)-1
aux(11) =< aux(96)
aux(12) =< aux(34)
s(24) =< it(25)*aux(23)
s(23) =< it(24)*aux(11)
s(19) =< it(19)*aux(12)
s(20) =< it(19)*aux(11)
s(18) =< it(19)*aux(96)
s(17) =< it(19)*aux(34)

  with precondition: [V6=0,V1>=2,V5>=0,V4>=0,Out>=3*V1+2,V>=V5+2] 

* Chain [28,[19,20,21,22,23,24,25,26],33]: 18*it(19)+3*it(24)+6*it(25)+1*s(17)+1*s(18)+1*s(19)+1*s(20)+1*s(21)+1*s(22)+1*s(23)+1*s(24)+5
  Such that:aux(27) =< V1+V+V5
aux(55) =< V1+V5
aux(31) =< 2*V1+V+V5
aux(34) =< V+V5+1
aux(97) =< V1
it(19) =< aux(97)
it(24) =< aux(27)
it(25) =< aux(27)
s(21) =< aux(27)
it(24) =< aux(55)
it(25) =< aux(55)
s(21) =< aux(55)
it(24) =< aux(97)
it(25) =< aux(97)
it(25) =< aux(31)
s(22) =< aux(31)
s(22) =< aux(55)
aux(23) =< aux(97)-1
aux(11) =< aux(97)
aux(12) =< aux(34)
s(24) =< it(25)*aux(23)
s(23) =< it(24)*aux(11)
s(19) =< it(19)*aux(12)
s(20) =< it(19)*aux(11)
s(18) =< it(19)*aux(97)
s(17) =< it(19)*aux(34)

  with precondition: [V6=0,V1>=3,V5>=0,V4>=0,Out>=9,V>=V5+2] 

* Chain [28,[19,20,21,22,23,24,25,26],32]: 15*it(19)+3*it(24)+6*it(25)+1*s(17)+1*s(18)+1*s(19)+1*s(20)+1*s(21)+1*s(22)+1*s(23)+1*s(24)+2*s(37)+5
  Such that:aux(27) =< V1+V+V5
aux(58) =< V1+V5
aux(31) =< 2*V1+V+V5
aux(56) =< V
aux(34) =< V+V5+1
aux(98) =< V1
s(37) =< aux(56)
it(24) =< aux(27)
it(25) =< aux(27)
s(21) =< aux(27)
it(24) =< aux(58)
it(25) =< aux(58)
s(21) =< aux(58)
it(19) =< aux(98)
it(24) =< aux(98)
it(25) =< aux(98)
it(25) =< aux(31)
s(22) =< aux(31)
s(22) =< aux(58)
aux(23) =< aux(98)-1
aux(11) =< aux(98)
aux(12) =< aux(34)
s(24) =< it(25)*aux(23)
s(23) =< it(24)*aux(11)
s(19) =< it(19)*aux(12)
s(20) =< it(19)*aux(11)
s(18) =< it(19)*aux(98)
s(17) =< it(19)*aux(34)

  with precondition: [V6=0,V1>=3,V5>=0,V4>=0,Out>=9,V>=V5+2] 

* Chain [28,[19,20,21,22,23,24,25,26],31]: 15*it(19)+3*it(24)+6*it(25)+1*s(17)+1*s(18)+1*s(19)+1*s(20)+1*s(21)+1*s(22)+1*s(23)+1*s(24)+1*s(39)+5
  Such that:aux(27) =< V1+V+V5
aux(60) =< V1+V5
aux(31) =< 2*V1+V+V5
aux(34) =< V+V5+1
aux(99) =< V1
s(39) =< aux(60)
it(24) =< aux(27)
it(25) =< aux(27)
s(21) =< aux(27)
it(24) =< aux(60)
it(25) =< aux(60)
s(21) =< aux(60)
it(19) =< aux(99)
it(24) =< aux(99)
it(25) =< aux(99)
it(25) =< aux(31)
s(22) =< aux(31)
s(22) =< aux(60)
aux(23) =< aux(99)-1
aux(11) =< aux(99)
aux(12) =< aux(34)
s(24) =< it(25)*aux(23)
s(23) =< it(24)*aux(11)
s(19) =< it(19)*aux(12)
s(20) =< it(19)*aux(11)
s(18) =< it(19)*aux(99)
s(17) =< it(19)*aux(34)

  with precondition: [V6=0,V1>=3,V5>=0,V4>=0,Out>=9,V>=V5+2] 

* Chain [28,42]: 4
  with precondition: [V6=0,Out=4,V1>=1,V5>=0,V4>=0,V>=V5+2] 

* Chain [28,37]: 3
  with precondition: [V6=0,Out=3,V1>=1,V5>=0,V4>=0,V>=V5+2] 

* Chain [28,36]: 2*s(25)+5
  Such that:aux(40) =< 1
s(25) =< aux(40)

  with precondition: [V6=0,Out=5,V1>=1,V5>=0,V4>=0,V>=V5+2] 

* Chain [28,35]: 2*s(27)+3*s(28)+1*s(29)+5
  Such that:aux(45) =< 1
aux(44) =< V
s(29) =< V5+2
s(27) =< aux(44)
s(28) =< aux(45)

  with precondition: [V6=0,V1>=2,V5>=0,V4>=0,Out>=7,V>=V5+2,V5+8>=Out] 

* Chain [28,34]: 1*s(33)+4
  Such that:s(33) =< 1

  with precondition: [V1=1,V6=0,Out=5,V5>=0,V4>=0,V>=V5+2] 

* Chain [28,33]: 3*s(34)+5
  Such that:aux(52) =< 1
s(34) =< aux(52)

  with precondition: [V6=0,Out=6,V1>=2,V5>=0,V4>=0,V>=V5+2] 

* Chain [28,32]: 2*s(37)+5
  Such that:aux(56) =< V
s(37) =< aux(56)

  with precondition: [V6=0,V1>=2,V5>=0,V4>=0,Out>=6,V>=V5+2,V5+7>=Out] 

* Chain [28,31]: 1*s(39)+5
  Such that:s(39) =< V5+2

  with precondition: [V6=0,V1>=2,V5>=0,V4>=0,Out>=6,V>=V5+3,V5+7>=Out] 

* Chain [27,[19,20,21,22,23,24,25,26],42]: 15*it(19)+3*it(24)+6*it(25)+1*s(17)+1*s(18)+1*s(19)+1*s(20)+1*s(21)+1*s(22)+1*s(23)+1*s(24)+1*s(44)+4
  Such that:aux(27) =< V1+V+V5
aux(37) =< V1+V5
aux(31) =< 2*V1+V+V5
aux(34) =< V+V5+1
s(44) =< V5+1
aux(100) =< V1
it(24) =< aux(27)
it(25) =< aux(27)
s(21) =< aux(27)
it(24) =< aux(37)
it(25) =< aux(37)
s(21) =< aux(37)
it(19) =< aux(100)
it(24) =< aux(100)
it(25) =< aux(100)
it(25) =< aux(31)
s(22) =< aux(31)
s(22) =< aux(37)
aux(23) =< aux(100)-1
aux(11) =< aux(100)
aux(12) =< aux(34)
s(24) =< it(25)*aux(23)
s(23) =< it(24)*aux(11)
s(19) =< it(19)*aux(12)
s(20) =< it(19)*aux(11)
s(18) =< it(19)*aux(100)
s(17) =< it(19)*aux(34)

  with precondition: [V6=0,V1>=2,V5>=0,V4>=0,Out>=8,V>=V5+2] 

* Chain [27,[19,20,21,22,23,24,25,26],37]: 15*it(19)+3*it(24)+6*it(25)+1*s(17)+1*s(18)+1*s(19)+1*s(20)+1*s(21)+1*s(22)+1*s(23)+1*s(24)+1*s(44)+3
  Such that:aux(27) =< V1+V+V5
aux(39) =< V1+V5
aux(31) =< 2*V1+V+V5
aux(34) =< V+V5+1
s(44) =< V5+1
aux(101) =< V1
it(24) =< aux(27)
it(25) =< aux(27)
s(21) =< aux(27)
it(24) =< aux(39)
it(25) =< aux(39)
s(21) =< aux(39)
it(19) =< aux(101)
it(24) =< aux(101)
it(25) =< aux(101)
it(25) =< aux(31)
s(22) =< aux(31)
s(22) =< aux(39)
aux(23) =< aux(101)-1
aux(11) =< aux(101)
aux(12) =< aux(34)
s(24) =< it(25)*aux(23)
s(23) =< it(24)*aux(11)
s(19) =< it(19)*aux(12)
s(20) =< it(19)*aux(11)
s(18) =< it(19)*aux(101)
s(17) =< it(19)*aux(34)

  with precondition: [V6=0,V1>=2,V5>=0,V4>=0,Out>=7,V>=V5+2] 

* Chain [27,[19,20,21,22,23,24,25,26],36]: 17*it(19)+3*it(24)+6*it(25)+1*s(17)+1*s(18)+1*s(19)+1*s(20)+1*s(21)+1*s(22)+1*s(23)+1*s(24)+1*s(44)+5
  Such that:aux(27) =< V1+V+V5
aux(43) =< V1+V5
aux(31) =< 2*V1+V+V5
aux(34) =< V+V5+1
s(44) =< V5+1
aux(102) =< V1
it(19) =< aux(102)
it(24) =< aux(27)
it(25) =< aux(27)
s(21) =< aux(27)
it(24) =< aux(43)
it(25) =< aux(43)
s(21) =< aux(43)
it(24) =< aux(102)
it(25) =< aux(102)
it(25) =< aux(31)
s(22) =< aux(31)
s(22) =< aux(43)
aux(23) =< aux(102)-1
aux(11) =< aux(102)
aux(12) =< aux(34)
s(24) =< it(25)*aux(23)
s(23) =< it(24)*aux(11)
s(19) =< it(19)*aux(12)
s(20) =< it(19)*aux(11)
s(18) =< it(19)*aux(102)
s(17) =< it(19)*aux(34)

  with precondition: [V6=0,V1>=2,V5>=0,V4>=0,Out>=9,V>=V5+2] 

* Chain [27,[19,20,21,22,23,24,25,26],35]: 18*it(19)+3*it(24)+6*it(25)+1*s(17)+1*s(18)+1*s(19)+1*s(20)+1*s(21)+1*s(22)+1*s(23)+1*s(24)+2*s(27)+1*s(29)+1*s(44)+5
  Such that:aux(27) =< V1+V+V5
aux(48) =< V1+V5
aux(31) =< 2*V1+V+V5
aux(44) =< V
aux(34) =< V+V5+1
s(44) =< V5+1
aux(103) =< V1
s(29) =< aux(48)
s(27) =< aux(44)
it(19) =< aux(103)
it(24) =< aux(27)
it(25) =< aux(27)
s(21) =< aux(27)
it(24) =< aux(48)
it(25) =< aux(48)
s(21) =< aux(48)
it(24) =< aux(103)
it(25) =< aux(103)
it(25) =< aux(31)
s(22) =< aux(31)
s(22) =< aux(48)
aux(23) =< aux(103)-1
aux(11) =< aux(103)
aux(12) =< aux(34)
s(24) =< it(25)*aux(23)
s(23) =< it(24)*aux(11)
s(19) =< it(19)*aux(12)
s(20) =< it(19)*aux(11)
s(18) =< it(19)*aux(103)
s(17) =< it(19)*aux(34)

  with precondition: [V6=0,V1>=3,V5>=0,V4>=0,Out>=11,V>=V5+2] 

* Chain [27,[19,20,21,22,23,24,25,26],34]: 16*it(19)+3*it(24)+6*it(25)+1*s(17)+1*s(18)+1*s(19)+1*s(20)+1*s(21)+1*s(22)+1*s(23)+1*s(24)+1*s(44)+4
  Such that:aux(27) =< V1+V+V5
aux(51) =< V1+V5
aux(31) =< 2*V1+V+V5
aux(34) =< V+V5+1
s(44) =< V5+1
aux(104) =< V1
it(19) =< aux(104)
it(24) =< aux(27)
it(25) =< aux(27)
s(21) =< aux(27)
it(24) =< aux(51)
it(25) =< aux(51)
s(21) =< aux(51)
it(24) =< aux(104)
it(25) =< aux(104)
it(25) =< aux(31)
s(22) =< aux(31)
s(22) =< aux(51)
aux(23) =< aux(104)-1
aux(11) =< aux(104)
aux(12) =< aux(34)
s(24) =< it(25)*aux(23)
s(23) =< it(24)*aux(11)
s(19) =< it(19)*aux(12)
s(20) =< it(19)*aux(11)
s(18) =< it(19)*aux(104)
s(17) =< it(19)*aux(34)

  with precondition: [V6=0,V1>=2,V5>=0,V4>=0,Out>=3*V1+3,V>=V5+2] 

* Chain [27,[19,20,21,22,23,24,25,26],33]: 18*it(19)+3*it(24)+6*it(25)+1*s(17)+1*s(18)+1*s(19)+1*s(20)+1*s(21)+1*s(22)+1*s(23)+1*s(24)+1*s(44)+5
  Such that:aux(27) =< V1+V+V5
aux(55) =< V1+V5
aux(31) =< 2*V1+V+V5
aux(34) =< V+V5+1
s(44) =< V5+1
aux(105) =< V1
it(19) =< aux(105)
it(24) =< aux(27)
it(25) =< aux(27)
s(21) =< aux(27)
it(24) =< aux(55)
it(25) =< aux(55)
s(21) =< aux(55)
it(24) =< aux(105)
it(25) =< aux(105)
it(25) =< aux(31)
s(22) =< aux(31)
s(22) =< aux(55)
aux(23) =< aux(105)-1
aux(11) =< aux(105)
aux(12) =< aux(34)
s(24) =< it(25)*aux(23)
s(23) =< it(24)*aux(11)
s(19) =< it(19)*aux(12)
s(20) =< it(19)*aux(11)
s(18) =< it(19)*aux(105)
s(17) =< it(19)*aux(34)

  with precondition: [V6=0,V1>=3,V5>=0,V4>=0,Out>=10,V>=V5+2] 

* Chain [27,[19,20,21,22,23,24,25,26],32]: 15*it(19)+3*it(24)+6*it(25)+1*s(17)+1*s(18)+1*s(19)+1*s(20)+1*s(21)+1*s(22)+1*s(23)+1*s(24)+2*s(37)+1*s(44)+5
  Such that:aux(27) =< V1+V+V5
aux(58) =< V1+V5
aux(31) =< 2*V1+V+V5
aux(56) =< V
aux(34) =< V+V5+1
s(44) =< V5+1
aux(106) =< V1
s(37) =< aux(56)
it(24) =< aux(27)
it(25) =< aux(27)
s(21) =< aux(27)
it(24) =< aux(58)
it(25) =< aux(58)
s(21) =< aux(58)
it(19) =< aux(106)
it(24) =< aux(106)
it(25) =< aux(106)
it(25) =< aux(31)
s(22) =< aux(31)
s(22) =< aux(58)
aux(23) =< aux(106)-1
aux(11) =< aux(106)
aux(12) =< aux(34)
s(24) =< it(25)*aux(23)
s(23) =< it(24)*aux(11)
s(19) =< it(19)*aux(12)
s(20) =< it(19)*aux(11)
s(18) =< it(19)*aux(106)
s(17) =< it(19)*aux(34)

  with precondition: [V6=0,V1>=3,V5>=0,V4>=0,Out>=10,V>=V5+2] 

* Chain [27,[19,20,21,22,23,24,25,26],31]: 15*it(19)+3*it(24)+6*it(25)+1*s(17)+1*s(18)+1*s(19)+1*s(20)+1*s(21)+1*s(22)+1*s(23)+1*s(24)+1*s(39)+1*s(44)+5
  Such that:aux(27) =< V1+V+V5
aux(60) =< V1+V5
aux(31) =< 2*V1+V+V5
aux(34) =< V+V5+1
s(44) =< V5+1
aux(107) =< V1
s(39) =< aux(60)
it(24) =< aux(27)
it(25) =< aux(27)
s(21) =< aux(27)
it(24) =< aux(60)
it(25) =< aux(60)
s(21) =< aux(60)
it(19) =< aux(107)
it(24) =< aux(107)
it(25) =< aux(107)
it(25) =< aux(31)
s(22) =< aux(31)
s(22) =< aux(60)
aux(23) =< aux(107)-1
aux(11) =< aux(107)
aux(12) =< aux(34)
s(24) =< it(25)*aux(23)
s(23) =< it(24)*aux(11)
s(19) =< it(19)*aux(12)
s(20) =< it(19)*aux(11)
s(18) =< it(19)*aux(107)
s(17) =< it(19)*aux(34)

  with precondition: [V6=0,V1>=3,V5>=0,V4>=0,Out>=10,V>=V5+2] 

* Chain [27,42]: 1*s(44)+4
  Such that:s(44) =< V5+1

  with precondition: [V6=0,V1>=1,V4>=0,Out>=5,V>=V5+2,V5+5>=Out] 

* Chain [27,37]: 1*s(44)+3
  Such that:s(44) =< V5+1

  with precondition: [V6=0,V1>=1,V4>=0,Out>=4,V>=V5+2,V5+4>=Out] 

* Chain [27,36]: 2*s(25)+1*s(44)+5
  Such that:aux(40) =< 1
s(44) =< V5+1
s(25) =< aux(40)

  with precondition: [V6=0,V1>=1,V4>=0,Out>=6,V>=V5+2,V5+6>=Out] 

* Chain [27,35]: 2*s(27)+3*s(28)+1*s(29)+1*s(44)+5
  Such that:aux(45) =< 1
aux(44) =< V
s(44) =< V5+1
s(29) =< V5+2
s(27) =< aux(44)
s(28) =< aux(45)

  with precondition: [V6=0,V1>=2,V5>=0,V4>=0,Out>=8,V>=V5+2,2*V5+9>=Out] 

* Chain [27,34]: 1*s(33)+1*s(44)+4
  Such that:s(33) =< 1
s(44) =< V5+1

  with precondition: [V1=1,V6=0,V4>=0,Out>=6,V>=V5+2,V5+6>=Out] 

* Chain [27,33]: 3*s(34)+1*s(44)+5
  Such that:aux(52) =< 1
s(44) =< V5+1
s(34) =< aux(52)

  with precondition: [V6=0,V1>=2,V4>=0,Out>=7,V>=V5+2,V5+7>=Out] 

* Chain [27,32]: 2*s(37)+1*s(44)+5
  Such that:aux(56) =< V
s(44) =< V5+1
s(37) =< aux(56)

  with precondition: [V6=0,V1>=2,V5>=0,V4>=0,Out>=7,V>=V5+2,2*V5+8>=Out] 

* Chain [27,31]: 1*s(39)+1*s(44)+5
  Such that:s(44) =< V5+1
s(39) =< V5+2

  with precondition: [V6=0,V1>=2,V5>=0,V4>=0,Out>=7,V>=V5+3,2*V5+8>=Out] 


#### Cost of chains of start(V1,V,V6,V5,V4,V12):
* Chain [48]: 9*s(897)+2*s(907)+2*s(908)+24*s(909)+48*s(910)+8*s(911)+120*s(912)+8*s(913)+8*s(917)+8*s(918)+8*s(919)+8*s(920)+8*s(921)+8*s(922)+10*s(924)+8*s(925)+2
  Such that:s(899) =< V1+V-V6+V5
s(900) =< V1-V6
s(901) =< V1-V6+V5
s(902) =< 2*V1+V-V6+V5
s(904) =< V+V5
s(906) =< V5+1
aux(137) =< V1
aux(138) =< V
aux(139) =< V6
s(924) =< aux(137)
s(897) =< aux(138)
s(907) =< s(906)
s(908) =< s(901)
s(909) =< s(899)
s(910) =< s(899)
s(911) =< s(899)
s(909) =< s(901)
s(910) =< s(901)
s(911) =< s(901)
s(912) =< s(900)
s(909) =< s(900)
s(910) =< s(900)
s(910) =< s(902)
s(913) =< s(902)
s(913) =< s(901)
s(914) =< aux(137)-1
s(915) =< aux(137)
s(916) =< s(904)
s(917) =< s(910)*s(914)
s(918) =< s(909)*s(915)
s(919) =< s(912)*s(916)
s(920) =< s(912)*s(915)
s(921) =< s(912)*aux(137)
s(922) =< s(912)*s(904)
s(925) =< aux(139)

  with precondition: [V1>=0,V>=0] 

* Chain [47]: 46*s(929)+7*s(930)+4*s(943)+604*s(944)+64*s(945)+96*s(946)+16*s(949)+16*s(953)+16*s(954)+16*s(955)+40*s(956)+40*s(957)+16*s(958)+50*s(960)+32*s(961)+4*s(1009)+6*s(1010)+72*s(1011)+144*s(1012)+24*s(1013)+24*s(1015)+24*s(1019)+24*s(1020)+16*s(1021)+16*s(1024)+8*s(1085)+8*s(1088)+8*s(1091)+4
  Such that:s(1070) =< V6+V4
aux(144) =< 1
aux(145) =< V
aux(146) =< V+V6-V5
aux(147) =< V+V6-V5+V4
aux(148) =< V-V5
aux(149) =< V-V5+V4
aux(150) =< 2*V+V6-V5
aux(151) =< 2*V+V6-V5+V4
aux(152) =< V6
aux(153) =< V6+V4+1
aux(154) =< V5
aux(155) =< V5+1
aux(156) =< V4+1
aux(157) =< V4+2
s(960) =< aux(145)
s(929) =< aux(152)
s(930) =< aux(156)
s(943) =< aux(144)
s(944) =< aux(148)
s(945) =< aux(146)
s(946) =< aux(146)
s(945) =< aux(148)
s(946) =< aux(148)
s(946) =< aux(150)
s(949) =< aux(150)
s(949) =< aux(148)
s(950) =< aux(145)-1
s(951) =< aux(145)
s(952) =< aux(152)
s(953) =< s(946)*s(950)
s(954) =< s(945)*s(951)
s(955) =< s(944)*s(952)
s(956) =< s(944)*s(951)
s(957) =< s(944)*aux(145)
s(958) =< s(944)*aux(152)
s(961) =< aux(155)
s(1009) =< aux(157)
s(1010) =< aux(149)
s(1011) =< aux(147)
s(1012) =< aux(147)
s(1013) =< aux(147)
s(1011) =< aux(149)
s(1012) =< aux(149)
s(1013) =< aux(149)
s(1011) =< aux(148)
s(1012) =< aux(148)
s(1012) =< aux(151)
s(1015) =< aux(151)
s(1015) =< aux(149)
s(1018) =< aux(153)
s(1019) =< s(1012)*s(950)
s(1020) =< s(1011)*s(951)
s(1021) =< s(944)*s(1018)
s(1024) =< s(944)*aux(153)
s(1082) =< s(1070)
s(1085) =< s(944)*s(1082)
s(1088) =< s(944)*s(1070)
s(1091) =< aux(154)

  with precondition: [V1=1,V>=0,V6>=0,V5>=0,V4>=0,V12>=0] 

* Chain [46]: 50*s(1095)+40*s(1097)+17*s(1098)+520*s(1121)+64*s(1122)+96*s(1123)+16*s(1124)+16*s(1128)+16*s(1129)+16*s(1130)+32*s(1131)+32*s(1132)+16*s(1133)+4*s(1144)+4*s(1147)+48*s(1148)+96*s(1149)+16*s(1150)+16*s(1152)+16*s(1156)+16*s(1157)+16*s(1158)+16*s(1161)+6
  Such that:s(1116) =< V+V6
s(1136) =< V+V6+V4
s(1137) =< V+V4
s(1117) =< 2*V+V6
s(1138) =< 2*V+V6+V4
s(1140) =< V6+V4+1
s(1142) =< V4+2
aux(158) =< 1
aux(159) =< V
aux(160) =< V6
aux(161) =< V4+1
s(1095) =< aux(160)
s(1098) =< aux(161)
s(1097) =< aux(158)
s(1121) =< aux(159)
s(1122) =< s(1116)
s(1123) =< s(1116)
s(1122) =< aux(159)
s(1123) =< aux(159)
s(1123) =< s(1117)
s(1124) =< s(1117)
s(1124) =< aux(159)
s(1125) =< aux(159)-1
s(1126) =< aux(159)
s(1127) =< aux(160)
s(1128) =< s(1123)*s(1125)
s(1129) =< s(1122)*s(1126)
s(1130) =< s(1121)*s(1127)
s(1131) =< s(1121)*s(1126)
s(1132) =< s(1121)*aux(159)
s(1133) =< s(1121)*aux(160)
s(1144) =< s(1142)
s(1147) =< s(1137)
s(1148) =< s(1136)
s(1149) =< s(1136)
s(1150) =< s(1136)
s(1148) =< s(1137)
s(1149) =< s(1137)
s(1150) =< s(1137)
s(1148) =< aux(159)
s(1149) =< aux(159)
s(1149) =< s(1138)
s(1152) =< s(1138)
s(1152) =< s(1137)
s(1155) =< s(1140)
s(1156) =< s(1149)*s(1125)
s(1157) =< s(1148)*s(1126)
s(1158) =< s(1121)*s(1155)
s(1161) =< s(1121)*s(1140)

  with precondition: [V1=1,V5=0,V>=1,V6>=1,V4>=0,V12>=0] 

* Chain [45]: 91*s(1166)+26*s(1181)+534*s(1192)+64*s(1193)+96*s(1194)+16*s(1195)+16*s(1199)+16*s(1200)+16*s(1201)+32*s(1202)+32*s(1203)+16*s(1204)+4*s(1215)+64*s(1219)+96*s(1220)+16*s(1223)+16*s(1227)+16*s(1228)+16*s(1229)+16*s(1232)+122*s(1247)+32*s(1248)+48*s(1249)+8*s(1252)+8*s(1256)+8*s(1257)+8*s(1258)+8*s(1259)+8*s(1260)+8*s(1261)+8*s(1264)+6
  Such that:s(1213) =< 2
s(1187) =< V+1
s(1207) =< V+V6
s(1238) =< V+V6-V5
aux(170) =< V-V5
s(1188) =< 2*V+1
s(1209) =< 2*V+V6
s(1241) =< 2*V+V6-V5
s(1211) =< V6+1
aux(172) =< 1
aux(173) =< V
aux(174) =< V6
aux(175) =< V5
s(1166) =< aux(172)
s(1192) =< aux(173)
s(1247) =< aux(170)
s(1248) =< s(1238)
s(1249) =< s(1238)
s(1248) =< aux(170)
s(1249) =< aux(170)
s(1249) =< s(1241)
s(1252) =< s(1241)
s(1252) =< aux(170)
s(1196) =< aux(173)-1
s(1197) =< aux(173)
s(1255) =< aux(174)
s(1256) =< s(1249)*s(1196)
s(1257) =< s(1248)*s(1197)
s(1258) =< s(1247)*s(1255)
s(1259) =< s(1247)*s(1197)
s(1260) =< s(1247)*aux(173)
s(1261) =< s(1247)*aux(174)
s(1181) =< aux(174)
s(1264) =< aux(175)
s(1215) =< s(1213)
s(1219) =< s(1207)
s(1220) =< s(1207)
s(1219) =< aux(173)
s(1220) =< aux(173)
s(1220) =< s(1209)
s(1223) =< s(1209)
s(1223) =< aux(173)
s(1226) =< s(1211)
s(1227) =< s(1220)*s(1196)
s(1228) =< s(1219)*s(1197)
s(1229) =< s(1192)*s(1226)
s(1202) =< s(1192)*s(1197)
s(1203) =< s(1192)*aux(173)
s(1232) =< s(1192)*s(1211)
s(1193) =< s(1187)
s(1194) =< s(1187)
s(1193) =< aux(173)
s(1194) =< aux(173)
s(1194) =< s(1188)
s(1195) =< s(1188)
s(1195) =< aux(173)
s(1198) =< aux(172)
s(1199) =< s(1194)*s(1196)
s(1200) =< s(1193)*s(1197)
s(1201) =< s(1192)*s(1198)
s(1204) =< s(1192)*aux(172)

  with precondition: [V1=2,V>=0,V6>=0,V5>=0,V4>=0,V12>=0] 

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

* Chain [43]: 50*s(1268)+40*s(1270)+17*s(1271)+520*s(1294)+64*s(1295)+96*s(1296)+16*s(1297)+16*s(1301)+16*s(1302)+16*s(1303)+32*s(1304)+32*s(1305)+16*s(1306)+4*s(1317)+4*s(1320)+48*s(1321)+96*s(1322)+16*s(1323)+16*s(1325)+16*s(1329)+16*s(1330)+16*s(1331)+16*s(1334)+5
  Such that:s(1289) =< V1+V
s(1309) =< V1+V+V5
s(1310) =< V1+V5
s(1290) =< 2*V1+V
s(1311) =< 2*V1+V+V5
s(1313) =< V+V5+1
s(1315) =< V5+2
aux(176) =< 1
aux(177) =< V1
aux(178) =< V
aux(179) =< V5+1
s(1268) =< aux(178)
s(1271) =< aux(179)
s(1270) =< aux(176)
s(1294) =< aux(177)
s(1295) =< s(1289)
s(1296) =< s(1289)
s(1295) =< aux(177)
s(1296) =< aux(177)
s(1296) =< s(1290)
s(1297) =< s(1290)
s(1297) =< aux(177)
s(1298) =< aux(177)-1
s(1299) =< aux(177)
s(1300) =< aux(178)
s(1301) =< s(1296)*s(1298)
s(1302) =< s(1295)*s(1299)
s(1303) =< s(1294)*s(1300)
s(1304) =< s(1294)*s(1299)
s(1305) =< s(1294)*aux(177)
s(1306) =< s(1294)*aux(178)
s(1317) =< s(1315)
s(1320) =< s(1310)
s(1321) =< s(1309)
s(1322) =< s(1309)
s(1323) =< s(1309)
s(1321) =< s(1310)
s(1322) =< s(1310)
s(1323) =< s(1310)
s(1321) =< aux(177)
s(1322) =< aux(177)
s(1322) =< s(1311)
s(1325) =< s(1311)
s(1325) =< s(1310)
s(1328) =< s(1313)
s(1329) =< s(1322)*s(1298)
s(1330) =< s(1321)*s(1299)
s(1331) =< s(1294)*s(1328)
s(1334) =< s(1294)*s(1313)

  with precondition: [V6=0,V1>=1,V>=1,V5>=0,V4>=0] 


Closed-form bounds of start(V1,V,V6,V5,V4,V12): 
-------------------------------------
* Chain [48] with precondition: [V1>=0,V>=0] 
    - Upper bound: 10*V1+2+8*V1*nat(V1+V-V6+V5)+16*V1*nat(V1-V6)+9*V+nat(V6)*8+nat(V1-1)*8*nat(V1+V-V6+V5)+nat(V+V5)*16*nat(V1-V6)+nat(V5+1)*2+nat(V1-V6+V5)*2+nat(V1+V-V6+V5)*80+nat(2*V1+V-V6+V5)*8+nat(V1-V6)*120 
    - Complexity: n^2 
* Chain [47] with precondition: [V1=1,V>=0,V6>=0,V5>=0,V4>=0,V12>=0] 
    - Upper bound: 50*V+8+24*V*nat(V+V6-V5+V4)+80*V*nat(V-V5)+16*V*nat(V+V6-V5)+46*V6+32*V6*nat(V-V5)+8*V5+nat(V-1)*24*nat(V+V6-V5+V4)+nat(V-1)*16*nat(V+V6-V5)+(16*V6+16*V4)*nat(V-V5)+(32*V5+32)+(7*V4+7)+(4*V4+8)+(32*V6+32*V4+32)*nat(V-V5)+nat(V-V5+V4)*6+nat(V+V6-V5+V4)*240+nat(2*V+V6-V5+V4)*24+nat(V-V5)*604+nat(V+V6-V5)*160+nat(2*V+V6-V5)*16 
    - Complexity: n^2 
* Chain [46] with precondition: [V1=1,V5=0,V>=1,V6>=1,V4>=0,V12>=0] 
    - Upper bound: 520*V+46+64*V*V+32*V*V6+(V+V6)*(16*V)+(V+V6+V4)*(16*V)+(V6+V4+1)*(32*V)+50*V6+(16*V-16)*(V+V6)+(16*V-16)*(V+V6+V4)+(160*V+160*V6)+(4*V+4*V4)+(17*V4+17)+(4*V4+8)+(32*V+16*V6)+(160*V+160*V6+160*V4)+(32*V+16*V6+16*V4) 
    - Complexity: n^2 
* Chain [45] with precondition: [V1=2,V>=0,V6>=0,V5>=0,V4>=0,V12>=0] 
    - Upper bound: 566*V+105+64*V*V+(V+V6)*(16*V)+(V+1)*(16*V)+(V6+1)*(32*V)+16*V*nat(V-V5)+8*V*nat(V+V6-V5)+26*V6+16*V6*nat(V-V5)+8*V5+(V+V6)*(nat(V-1)*16)+(V+1)*(nat(V-1)*16)+nat(V-1)*8*nat(V+V6-V5)+(160*V+160*V6)+(160*V+160)+(32*V+16*V6)+(32*V+16)+nat(V-V5)*122+nat(V+V6-V5)*80+nat(2*V+V6-V5)*8 
    - Complexity: n^2 
* Chain [44] with precondition: [V=0,V1>=1] 
    - Upper bound: 0 
    - Complexity: constant 
* Chain [43] with precondition: [V6=0,V1>=1,V>=1,V5>=0,V4>=0] 
    - Upper bound: 520*V1+45+64*V1*V1+32*V1*V+(V1+V)*(16*V1)+(V1+V+V5)*(16*V1)+(V+V5+1)*(32*V1)+50*V+(16*V1-16)*(V1+V)+(16*V1-16)*(V1+V+V5)+(160*V1+160*V)+(4*V1+4*V5)+(17*V5+17)+(4*V5+8)+(32*V1+16*V)+(160*V1+160*V+160*V5)+(32*V1+16*V+16*V5) 
    - Complexity: n^2 

### Maximum cost of start(V1,V,V6,V5,V4,V12): 9*V+2+max([41*V+6+max([nat(V6)*26+max([470*V+38+64*V*V+16*V*nat(V+V6)+nat(V-1)*16*nat(V+V6)+nat(V+V6)*160+nat(2*V+V6)*16+max([32*V*nat(V6)+16*V*nat(V+V6+V4)+32*V*nat(V6+V4+1)+nat(V6)*24+nat(V-1)*16*nat(V+V6+V4)+nat(V+V4)*4+nat(V4+1)*17+nat(V4+2)*4+nat(V+V6+V4)*160+nat(2*V+V6+V4)*16,46*V+59+(V+1)*(16*V)+32*V*nat(V6+1)+16*V*nat(V-V5)+8*V*nat(V+V6-V5)+nat(V6)*16*nat(V-V5)+nat(V5)*8+(V+1)*(nat(V-1)*16)+nat(V-1)*8*nat(V+V6-V5)+(160*V+160)+(32*V+16)+nat(V-V5)*122+nat(V+V6-V5)*80+nat(2*V+V6-V5)*8]),80*V*nat(V-V5)+24*V*nat(V+V6-V5+V4)+16*V*nat(V+V6-V5)+nat(V6)*20+nat(V6)*32*nat(V-V5)+nat(V5)*8+nat(V-1)*24*nat(V+V6-V5+V4)+nat(V-1)*16*nat(V+V6-V5)+nat(V6+V4)*16*nat(V-V5)+nat(V5+1)*32+nat(V4+1)*7+nat(V4+2)*4+nat(V6+V4+1)*32*nat(V-V5)+nat(V-V5+V4)*6+nat(V+V6-V5+V4)*240+nat(2*V+V6-V5+V4)*24+nat(V-V5)*604+nat(V+V6-V5)*160+nat(2*V+V6-V5)*16]),520*V1+37+64*V1*V1+32*V1*V+(V1+V)*(16*V1)+16*V1*nat(V1+V+V5)+32*V1*nat(V+V5+1)+(V1+V)*(nat(V1-1)*16)+nat(V1-1)*16*nat(V1+V+V5)+(160*V1+160*V)+nat(V1+V5)*4+nat(V5+1)*17+nat(V5+2)*4+(32*V1+16*V)+nat(V1+V+V5)*160+nat(2*V1+V+V5)*16]),8*V1*nat(V1+V-V6+V5)+10*V1+16*V1*nat(V1-V6)+nat(V6)*8+nat(V1-1)*8*nat(V1+V-V6+V5)+nat(V+V5)*16*nat(V1-V6)+nat(V5+1)*2+nat(V1-V6+V5)*2+nat(V1+V-V6+V5)*80+nat(2*V1+V-V6+V5)*8+nat(V1-V6)*120]) 
Asymptotic class: n^2 
* Total analysis performed in 4026 ms.


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

(18)
BOUNDS(1, n^2)

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

(19) CpxTrsToCdtProof (BOTH BOUNDS(ID, ID))
Converted Cpx (relative) TRS with rewrite strategy PARALLEL_INNERMOST to CDT
----------------------------------------

(20)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   le(0, z0) -> true
   le(s(z0), 0) -> false
   le(s(z0), s(z1)) -> le(z0, z1)
   quot(z0, 0) -> quotZeroErro
   quot(z0, s(z1)) -> quotIter(z0, s(z1), 0, 0, 0)
   quotIter(z0, s(z1), z2, z3, z4) -> if(le(z0, z2), z0, s(z1), z2, z3, z4)
   if(true, z0, z1, z2, z3, z4) -> z4
   if(false, z0, z1, z2, z3, z4) -> if2(le(z1, s(z3)), z0, z1, s(z2), s(z3), z4)
   if2(false, z0, z1, z2, z3, z4) -> quotIter(z0, z1, z2, z3, z4)
   if2(true, z0, z1, z2, z3, z4) -> quotIter(z0, z1, z2, 0, s(z4))
Tuples:
   LE(0, z0) -> c
   LE(s(z0), 0) -> c1
   LE(s(z0), s(z1)) -> c2(LE(z0, z1))
   QUOT(z0, 0) -> c3
   QUOT(z0, s(z1)) -> c4(QUOTITER(z0, s(z1), 0, 0, 0))
   QUOTITER(z0, s(z1), z2, z3, z4) -> c5(IF(le(z0, z2), z0, s(z1), z2, z3, z4), LE(z0, z2))
   IF(true, z0, z1, z2, z3, z4) -> c6
   IF(false, z0, z1, z2, z3, z4) -> c7(IF2(le(z1, s(z3)), z0, z1, s(z2), s(z3), z4), LE(z1, s(z3)))
   IF2(false, z0, z1, z2, z3, z4) -> c8(QUOTITER(z0, z1, z2, z3, z4))
   IF2(true, z0, z1, z2, z3, z4) -> c9(QUOTITER(z0, z1, z2, 0, s(z4)))
S tuples:
   LE(0, z0) -> c
   LE(s(z0), 0) -> c1
   LE(s(z0), s(z1)) -> c2(LE(z0, z1))
   QUOT(z0, 0) -> c3
   QUOT(z0, s(z1)) -> c4(QUOTITER(z0, s(z1), 0, 0, 0))
   QUOTITER(z0, s(z1), z2, z3, z4) -> c5(IF(le(z0, z2), z0, s(z1), z2, z3, z4), LE(z0, z2))
   IF(true, z0, z1, z2, z3, z4) -> c6
   IF(false, z0, z1, z2, z3, z4) -> c7(IF2(le(z1, s(z3)), z0, z1, s(z2), s(z3), z4), LE(z1, s(z3)))
   IF2(false, z0, z1, z2, z3, z4) -> c8(QUOTITER(z0, z1, z2, z3, z4))
   IF2(true, z0, z1, z2, z3, z4) -> c9(QUOTITER(z0, z1, z2, 0, s(z4)))
K tuples:none
Defined Rule Symbols:   le_2, quot_2, quotIter_5, if_6, if2_6

Defined Pair Symbols:   LE_2, QUOT_2, QUOTITER_5, IF_6, IF2_6

Compound Symbols:   c, c1, c2_1, c3, c4_1, c5_2, c6, c7_2, c8_1, c9_1


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

(21) CdtToCpxRelTrsProof (BOTH BOUNDS(ID, ID))
Converted S to standard rules, and D \ S as well as R to relative rules.
----------------------------------------

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

   LE(0, z0) -> c
   LE(s(z0), 0) -> c1
   LE(s(z0), s(z1)) -> c2(LE(z0, z1))
   QUOT(z0, 0) -> c3
   QUOT(z0, s(z1)) -> c4(QUOTITER(z0, s(z1), 0, 0, 0))
   QUOTITER(z0, s(z1), z2, z3, z4) -> c5(IF(le(z0, z2), z0, s(z1), z2, z3, z4), LE(z0, z2))
   IF(true, z0, z1, z2, z3, z4) -> c6
   IF(false, z0, z1, z2, z3, z4) -> c7(IF2(le(z1, s(z3)), z0, z1, s(z2), s(z3), z4), LE(z1, s(z3)))
   IF2(false, z0, z1, z2, z3, z4) -> c8(QUOTITER(z0, z1, z2, z3, z4))
   IF2(true, z0, z1, z2, z3, z4) -> c9(QUOTITER(z0, z1, z2, 0, s(z4)))

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

   le(0, z0) -> true
   le(s(z0), 0) -> false
   le(s(z0), s(z1)) -> le(z0, z1)
   quot(z0, 0) -> quotZeroErro
   quot(z0, s(z1)) -> quotIter(z0, s(z1), 0, 0, 0)
   quotIter(z0, s(z1), z2, z3, z4) -> if(le(z0, z2), z0, s(z1), z2, z3, z4)
   if(true, z0, z1, z2, z3, z4) -> z4
   if(false, z0, z1, z2, z3, z4) -> if2(le(z1, s(z3)), z0, z1, s(z2), s(z3), z4)
   if2(false, z0, z1, z2, z3, z4) -> quotIter(z0, z1, z2, z3, z4)
   if2(true, z0, z1, z2, z3, z4) -> quotIter(z0, z1, z2, 0, s(z4))

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

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

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

   LE(0', z0) -> c
   LE(s(z0), 0') -> c1
   LE(s(z0), s(z1)) -> c2(LE(z0, z1))
   QUOT(z0, 0') -> c3
   QUOT(z0, s(z1)) -> c4(QUOTITER(z0, s(z1), 0', 0', 0'))
   QUOTITER(z0, s(z1), z2, z3, z4) -> c5(IF(le(z0, z2), z0, s(z1), z2, z3, z4), LE(z0, z2))
   IF(true, z0, z1, z2, z3, z4) -> c6
   IF(false, z0, z1, z2, z3, z4) -> c7(IF2(le(z1, s(z3)), z0, z1, s(z2), s(z3), z4), LE(z1, s(z3)))
   IF2(false, z0, z1, z2, z3, z4) -> c8(QUOTITER(z0, z1, z2, z3, z4))
   IF2(true, z0, z1, z2, z3, z4) -> c9(QUOTITER(z0, z1, z2, 0', s(z4)))

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

   le(0', z0) -> true
   le(s(z0), 0') -> false
   le(s(z0), s(z1)) -> le(z0, z1)
   quot(z0, 0') -> quotZeroErro
   quot(z0, s(z1)) -> quotIter(z0, s(z1), 0', 0', 0')
   quotIter(z0, s(z1), z2, z3, z4) -> if(le(z0, z2), z0, s(z1), z2, z3, z4)
   if(true, z0, z1, z2, z3, z4) -> z4
   if(false, z0, z1, z2, z3, z4) -> if2(le(z1, s(z3)), z0, z1, s(z2), s(z3), z4)
   if2(false, z0, z1, z2, z3, z4) -> quotIter(z0, z1, z2, z3, z4)
   if2(true, z0, z1, z2, z3, z4) -> quotIter(z0, z1, z2, 0', s(z4))

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

(25) TypeInferenceProof (BOTH BOUNDS(ID, ID))
Inferred types.
----------------------------------------

(26)
Obligation:
Innermost TRS:
Rules:
LE(0', z0) -> c
LE(s(z0), 0') -> c1
LE(s(z0), s(z1)) -> c2(LE(z0, z1))
QUOT(z0, 0') -> c3
QUOT(z0, s(z1)) -> c4(QUOTITER(z0, s(z1), 0', 0', 0'))
QUOTITER(z0, s(z1), z2, z3, z4) -> c5(IF(le(z0, z2), z0, s(z1), z2, z3, z4), LE(z0, z2))
IF(true, z0, z1, z2, z3, z4) -> c6
IF(false, z0, z1, z2, z3, z4) -> c7(IF2(le(z1, s(z3)), z0, z1, s(z2), s(z3), z4), LE(z1, s(z3)))
IF2(false, z0, z1, z2, z3, z4) -> c8(QUOTITER(z0, z1, z2, z3, z4))
IF2(true, z0, z1, z2, z3, z4) -> c9(QUOTITER(z0, z1, z2, 0', s(z4)))
le(0', z0) -> true
le(s(z0), 0') -> false
le(s(z0), s(z1)) -> le(z0, z1)
quot(z0, 0') -> quotZeroErro
quot(z0, s(z1)) -> quotIter(z0, s(z1), 0', 0', 0')
quotIter(z0, s(z1), z2, z3, z4) -> if(le(z0, z2), z0, s(z1), z2, z3, z4)
if(true, z0, z1, z2, z3, z4) -> z4
if(false, z0, z1, z2, z3, z4) -> if2(le(z1, s(z3)), z0, z1, s(z2), s(z3), z4)
if2(false, z0, z1, z2, z3, z4) -> quotIter(z0, z1, z2, z3, z4)
if2(true, z0, z1, z2, z3, z4) -> quotIter(z0, z1, z2, 0', s(z4))

Types:
LE :: 0':s:quotZeroErro -> 0':s:quotZeroErro -> c:c1:c2
0' :: 0':s:quotZeroErro
c :: c:c1:c2
s :: 0':s:quotZeroErro -> 0':s:quotZeroErro
c1 :: c:c1:c2
c2 :: c:c1:c2 -> c:c1:c2
QUOT :: 0':s:quotZeroErro -> 0':s:quotZeroErro -> c3:c4
c3 :: c3:c4
c4 :: c5 -> c3:c4
QUOTITER :: 0':s:quotZeroErro -> 0':s:quotZeroErro -> 0':s:quotZeroErro -> 0':s:quotZeroErro -> 0':s:quotZeroErro -> c5
c5 :: c6:c7 -> c:c1:c2 -> c5
IF :: true:false -> 0':s:quotZeroErro -> 0':s:quotZeroErro -> 0':s:quotZeroErro -> 0':s:quotZeroErro -> 0':s:quotZeroErro -> c6:c7
le :: 0':s:quotZeroErro -> 0':s:quotZeroErro -> true:false
true :: true:false
c6 :: c6:c7
false :: true:false
c7 :: c8:c9 -> c:c1:c2 -> c6:c7
IF2 :: true:false -> 0':s:quotZeroErro -> 0':s:quotZeroErro -> 0':s:quotZeroErro -> 0':s:quotZeroErro -> 0':s:quotZeroErro -> c8:c9
c8 :: c5 -> c8:c9
c9 :: c5 -> c8:c9
quot :: 0':s:quotZeroErro -> 0':s:quotZeroErro -> 0':s:quotZeroErro
quotZeroErro :: 0':s:quotZeroErro
quotIter :: 0':s:quotZeroErro -> 0':s:quotZeroErro -> 0':s:quotZeroErro -> 0':s:quotZeroErro -> 0':s:quotZeroErro -> 0':s:quotZeroErro
if :: true:false -> 0':s:quotZeroErro -> 0':s:quotZeroErro -> 0':s:quotZeroErro -> 0':s:quotZeroErro -> 0':s:quotZeroErro -> 0':s:quotZeroErro
if2 :: true:false -> 0':s:quotZeroErro -> 0':s:quotZeroErro -> 0':s:quotZeroErro -> 0':s:quotZeroErro -> 0':s:quotZeroErro -> 0':s:quotZeroErro
hole_c:c1:c21_10 :: c:c1:c2
hole_0':s:quotZeroErro2_10 :: 0':s:quotZeroErro
hole_c3:c43_10 :: c3:c4
hole_c54_10 :: c5
hole_c6:c75_10 :: c6:c7
hole_true:false6_10 :: true:false
hole_c8:c97_10 :: c8:c9
gen_c:c1:c28_10 :: Nat -> c:c1:c2
gen_0':s:quotZeroErro9_10 :: Nat -> 0':s:quotZeroErro

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

(27) OrderProof (LOWER BOUND(ID))
Heuristically decided to analyse the following defined symbols:
LE, QUOTITER, le, quotIter

They will be analysed ascendingly in the following order:
LE < QUOTITER
le < QUOTITER
le < quotIter

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

(28)
Obligation:
Innermost TRS:
Rules:
LE(0', z0) -> c
LE(s(z0), 0') -> c1
LE(s(z0), s(z1)) -> c2(LE(z0, z1))
QUOT(z0, 0') -> c3
QUOT(z0, s(z1)) -> c4(QUOTITER(z0, s(z1), 0', 0', 0'))
QUOTITER(z0, s(z1), z2, z3, z4) -> c5(IF(le(z0, z2), z0, s(z1), z2, z3, z4), LE(z0, z2))
IF(true, z0, z1, z2, z3, z4) -> c6
IF(false, z0, z1, z2, z3, z4) -> c7(IF2(le(z1, s(z3)), z0, z1, s(z2), s(z3), z4), LE(z1, s(z3)))
IF2(false, z0, z1, z2, z3, z4) -> c8(QUOTITER(z0, z1, z2, z3, z4))
IF2(true, z0, z1, z2, z3, z4) -> c9(QUOTITER(z0, z1, z2, 0', s(z4)))
le(0', z0) -> true
le(s(z0), 0') -> false
le(s(z0), s(z1)) -> le(z0, z1)
quot(z0, 0') -> quotZeroErro
quot(z0, s(z1)) -> quotIter(z0, s(z1), 0', 0', 0')
quotIter(z0, s(z1), z2, z3, z4) -> if(le(z0, z2), z0, s(z1), z2, z3, z4)
if(true, z0, z1, z2, z3, z4) -> z4
if(false, z0, z1, z2, z3, z4) -> if2(le(z1, s(z3)), z0, z1, s(z2), s(z3), z4)
if2(false, z0, z1, z2, z3, z4) -> quotIter(z0, z1, z2, z3, z4)
if2(true, z0, z1, z2, z3, z4) -> quotIter(z0, z1, z2, 0', s(z4))

Types:
LE :: 0':s:quotZeroErro -> 0':s:quotZeroErro -> c:c1:c2
0' :: 0':s:quotZeroErro
c :: c:c1:c2
s :: 0':s:quotZeroErro -> 0':s:quotZeroErro
c1 :: c:c1:c2
c2 :: c:c1:c2 -> c:c1:c2
QUOT :: 0':s:quotZeroErro -> 0':s:quotZeroErro -> c3:c4
c3 :: c3:c4
c4 :: c5 -> c3:c4
QUOTITER :: 0':s:quotZeroErro -> 0':s:quotZeroErro -> 0':s:quotZeroErro -> 0':s:quotZeroErro -> 0':s:quotZeroErro -> c5
c5 :: c6:c7 -> c:c1:c2 -> c5
IF :: true:false -> 0':s:quotZeroErro -> 0':s:quotZeroErro -> 0':s:quotZeroErro -> 0':s:quotZeroErro -> 0':s:quotZeroErro -> c6:c7
le :: 0':s:quotZeroErro -> 0':s:quotZeroErro -> true:false
true :: true:false
c6 :: c6:c7
false :: true:false
c7 :: c8:c9 -> c:c1:c2 -> c6:c7
IF2 :: true:false -> 0':s:quotZeroErro -> 0':s:quotZeroErro -> 0':s:quotZeroErro -> 0':s:quotZeroErro -> 0':s:quotZeroErro -> c8:c9
c8 :: c5 -> c8:c9
c9 :: c5 -> c8:c9
quot :: 0':s:quotZeroErro -> 0':s:quotZeroErro -> 0':s:quotZeroErro
quotZeroErro :: 0':s:quotZeroErro
quotIter :: 0':s:quotZeroErro -> 0':s:quotZeroErro -> 0':s:quotZeroErro -> 0':s:quotZeroErro -> 0':s:quotZeroErro -> 0':s:quotZeroErro
if :: true:false -> 0':s:quotZeroErro -> 0':s:quotZeroErro -> 0':s:quotZeroErro -> 0':s:quotZeroErro -> 0':s:quotZeroErro -> 0':s:quotZeroErro
if2 :: true:false -> 0':s:quotZeroErro -> 0':s:quotZeroErro -> 0':s:quotZeroErro -> 0':s:quotZeroErro -> 0':s:quotZeroErro -> 0':s:quotZeroErro
hole_c:c1:c21_10 :: c:c1:c2
hole_0':s:quotZeroErro2_10 :: 0':s:quotZeroErro
hole_c3:c43_10 :: c3:c4
hole_c54_10 :: c5
hole_c6:c75_10 :: c6:c7
hole_true:false6_10 :: true:false
hole_c8:c97_10 :: c8:c9
gen_c:c1:c28_10 :: Nat -> c:c1:c2
gen_0':s:quotZeroErro9_10 :: Nat -> 0':s:quotZeroErro


Generator Equations:
gen_c:c1:c28_10(0) <=> c
gen_c:c1:c28_10(+(x, 1)) <=> c2(gen_c:c1:c28_10(x))
gen_0':s:quotZeroErro9_10(0) <=> 0'
gen_0':s:quotZeroErro9_10(+(x, 1)) <=> s(gen_0':s:quotZeroErro9_10(x))


The following defined symbols remain to be analysed:
LE, QUOTITER, le, quotIter

They will be analysed ascendingly in the following order:
LE < QUOTITER
le < QUOTITER
le < quotIter

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

(29) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
LE(gen_0':s:quotZeroErro9_10(n11_10), gen_0':s:quotZeroErro9_10(n11_10)) -> gen_c:c1:c28_10(n11_10), rt in Omega(1 + n11_10)

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

Induction Step:
LE(gen_0':s:quotZeroErro9_10(+(n11_10, 1)), gen_0':s:quotZeroErro9_10(+(n11_10, 1))) ->_R^Omega(1)
c2(LE(gen_0':s:quotZeroErro9_10(n11_10), gen_0':s:quotZeroErro9_10(n11_10))) ->_IH
c2(gen_c:c1:c28_10(c12_10))

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

(30)
Complex Obligation (BEST)

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

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

Innermost TRS:
Rules:
LE(0', z0) -> c
LE(s(z0), 0') -> c1
LE(s(z0), s(z1)) -> c2(LE(z0, z1))
QUOT(z0, 0') -> c3
QUOT(z0, s(z1)) -> c4(QUOTITER(z0, s(z1), 0', 0', 0'))
QUOTITER(z0, s(z1), z2, z3, z4) -> c5(IF(le(z0, z2), z0, s(z1), z2, z3, z4), LE(z0, z2))
IF(true, z0, z1, z2, z3, z4) -> c6
IF(false, z0, z1, z2, z3, z4) -> c7(IF2(le(z1, s(z3)), z0, z1, s(z2), s(z3), z4), LE(z1, s(z3)))
IF2(false, z0, z1, z2, z3, z4) -> c8(QUOTITER(z0, z1, z2, z3, z4))
IF2(true, z0, z1, z2, z3, z4) -> c9(QUOTITER(z0, z1, z2, 0', s(z4)))
le(0', z0) -> true
le(s(z0), 0') -> false
le(s(z0), s(z1)) -> le(z0, z1)
quot(z0, 0') -> quotZeroErro
quot(z0, s(z1)) -> quotIter(z0, s(z1), 0', 0', 0')
quotIter(z0, s(z1), z2, z3, z4) -> if(le(z0, z2), z0, s(z1), z2, z3, z4)
if(true, z0, z1, z2, z3, z4) -> z4
if(false, z0, z1, z2, z3, z4) -> if2(le(z1, s(z3)), z0, z1, s(z2), s(z3), z4)
if2(false, z0, z1, z2, z3, z4) -> quotIter(z0, z1, z2, z3, z4)
if2(true, z0, z1, z2, z3, z4) -> quotIter(z0, z1, z2, 0', s(z4))

Types:
LE :: 0':s:quotZeroErro -> 0':s:quotZeroErro -> c:c1:c2
0' :: 0':s:quotZeroErro
c :: c:c1:c2
s :: 0':s:quotZeroErro -> 0':s:quotZeroErro
c1 :: c:c1:c2
c2 :: c:c1:c2 -> c:c1:c2
QUOT :: 0':s:quotZeroErro -> 0':s:quotZeroErro -> c3:c4
c3 :: c3:c4
c4 :: c5 -> c3:c4
QUOTITER :: 0':s:quotZeroErro -> 0':s:quotZeroErro -> 0':s:quotZeroErro -> 0':s:quotZeroErro -> 0':s:quotZeroErro -> c5
c5 :: c6:c7 -> c:c1:c2 -> c5
IF :: true:false -> 0':s:quotZeroErro -> 0':s:quotZeroErro -> 0':s:quotZeroErro -> 0':s:quotZeroErro -> 0':s:quotZeroErro -> c6:c7
le :: 0':s:quotZeroErro -> 0':s:quotZeroErro -> true:false
true :: true:false
c6 :: c6:c7
false :: true:false
c7 :: c8:c9 -> c:c1:c2 -> c6:c7
IF2 :: true:false -> 0':s:quotZeroErro -> 0':s:quotZeroErro -> 0':s:quotZeroErro -> 0':s:quotZeroErro -> 0':s:quotZeroErro -> c8:c9
c8 :: c5 -> c8:c9
c9 :: c5 -> c8:c9
quot :: 0':s:quotZeroErro -> 0':s:quotZeroErro -> 0':s:quotZeroErro
quotZeroErro :: 0':s:quotZeroErro
quotIter :: 0':s:quotZeroErro -> 0':s:quotZeroErro -> 0':s:quotZeroErro -> 0':s:quotZeroErro -> 0':s:quotZeroErro -> 0':s:quotZeroErro
if :: true:false -> 0':s:quotZeroErro -> 0':s:quotZeroErro -> 0':s:quotZeroErro -> 0':s:quotZeroErro -> 0':s:quotZeroErro -> 0':s:quotZeroErro
if2 :: true:false -> 0':s:quotZeroErro -> 0':s:quotZeroErro -> 0':s:quotZeroErro -> 0':s:quotZeroErro -> 0':s:quotZeroErro -> 0':s:quotZeroErro
hole_c:c1:c21_10 :: c:c1:c2
hole_0':s:quotZeroErro2_10 :: 0':s:quotZeroErro
hole_c3:c43_10 :: c3:c4
hole_c54_10 :: c5
hole_c6:c75_10 :: c6:c7
hole_true:false6_10 :: true:false
hole_c8:c97_10 :: c8:c9
gen_c:c1:c28_10 :: Nat -> c:c1:c2
gen_0':s:quotZeroErro9_10 :: Nat -> 0':s:quotZeroErro


Generator Equations:
gen_c:c1:c28_10(0) <=> c
gen_c:c1:c28_10(+(x, 1)) <=> c2(gen_c:c1:c28_10(x))
gen_0':s:quotZeroErro9_10(0) <=> 0'
gen_0':s:quotZeroErro9_10(+(x, 1)) <=> s(gen_0':s:quotZeroErro9_10(x))


The following defined symbols remain to be analysed:
LE, QUOTITER, le, quotIter

They will be analysed ascendingly in the following order:
LE < QUOTITER
le < QUOTITER
le < quotIter

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

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

(33)
BOUNDS(n^1, INF)

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

(34)
Obligation:
Innermost TRS:
Rules:
LE(0', z0) -> c
LE(s(z0), 0') -> c1
LE(s(z0), s(z1)) -> c2(LE(z0, z1))
QUOT(z0, 0') -> c3
QUOT(z0, s(z1)) -> c4(QUOTITER(z0, s(z1), 0', 0', 0'))
QUOTITER(z0, s(z1), z2, z3, z4) -> c5(IF(le(z0, z2), z0, s(z1), z2, z3, z4), LE(z0, z2))
IF(true, z0, z1, z2, z3, z4) -> c6
IF(false, z0, z1, z2, z3, z4) -> c7(IF2(le(z1, s(z3)), z0, z1, s(z2), s(z3), z4), LE(z1, s(z3)))
IF2(false, z0, z1, z2, z3, z4) -> c8(QUOTITER(z0, z1, z2, z3, z4))
IF2(true, z0, z1, z2, z3, z4) -> c9(QUOTITER(z0, z1, z2, 0', s(z4)))
le(0', z0) -> true
le(s(z0), 0') -> false
le(s(z0), s(z1)) -> le(z0, z1)
quot(z0, 0') -> quotZeroErro
quot(z0, s(z1)) -> quotIter(z0, s(z1), 0', 0', 0')
quotIter(z0, s(z1), z2, z3, z4) -> if(le(z0, z2), z0, s(z1), z2, z3, z4)
if(true, z0, z1, z2, z3, z4) -> z4
if(false, z0, z1, z2, z3, z4) -> if2(le(z1, s(z3)), z0, z1, s(z2), s(z3), z4)
if2(false, z0, z1, z2, z3, z4) -> quotIter(z0, z1, z2, z3, z4)
if2(true, z0, z1, z2, z3, z4) -> quotIter(z0, z1, z2, 0', s(z4))

Types:
LE :: 0':s:quotZeroErro -> 0':s:quotZeroErro -> c:c1:c2
0' :: 0':s:quotZeroErro
c :: c:c1:c2
s :: 0':s:quotZeroErro -> 0':s:quotZeroErro
c1 :: c:c1:c2
c2 :: c:c1:c2 -> c:c1:c2
QUOT :: 0':s:quotZeroErro -> 0':s:quotZeroErro -> c3:c4
c3 :: c3:c4
c4 :: c5 -> c3:c4
QUOTITER :: 0':s:quotZeroErro -> 0':s:quotZeroErro -> 0':s:quotZeroErro -> 0':s:quotZeroErro -> 0':s:quotZeroErro -> c5
c5 :: c6:c7 -> c:c1:c2 -> c5
IF :: true:false -> 0':s:quotZeroErro -> 0':s:quotZeroErro -> 0':s:quotZeroErro -> 0':s:quotZeroErro -> 0':s:quotZeroErro -> c6:c7
le :: 0':s:quotZeroErro -> 0':s:quotZeroErro -> true:false
true :: true:false
c6 :: c6:c7
false :: true:false
c7 :: c8:c9 -> c:c1:c2 -> c6:c7
IF2 :: true:false -> 0':s:quotZeroErro -> 0':s:quotZeroErro -> 0':s:quotZeroErro -> 0':s:quotZeroErro -> 0':s:quotZeroErro -> c8:c9
c8 :: c5 -> c8:c9
c9 :: c5 -> c8:c9
quot :: 0':s:quotZeroErro -> 0':s:quotZeroErro -> 0':s:quotZeroErro
quotZeroErro :: 0':s:quotZeroErro
quotIter :: 0':s:quotZeroErro -> 0':s:quotZeroErro -> 0':s:quotZeroErro -> 0':s:quotZeroErro -> 0':s:quotZeroErro -> 0':s:quotZeroErro
if :: true:false -> 0':s:quotZeroErro -> 0':s:quotZeroErro -> 0':s:quotZeroErro -> 0':s:quotZeroErro -> 0':s:quotZeroErro -> 0':s:quotZeroErro
if2 :: true:false -> 0':s:quotZeroErro -> 0':s:quotZeroErro -> 0':s:quotZeroErro -> 0':s:quotZeroErro -> 0':s:quotZeroErro -> 0':s:quotZeroErro
hole_c:c1:c21_10 :: c:c1:c2
hole_0':s:quotZeroErro2_10 :: 0':s:quotZeroErro
hole_c3:c43_10 :: c3:c4
hole_c54_10 :: c5
hole_c6:c75_10 :: c6:c7
hole_true:false6_10 :: true:false
hole_c8:c97_10 :: c8:c9
gen_c:c1:c28_10 :: Nat -> c:c1:c2
gen_0':s:quotZeroErro9_10 :: Nat -> 0':s:quotZeroErro


Lemmas:
LE(gen_0':s:quotZeroErro9_10(n11_10), gen_0':s:quotZeroErro9_10(n11_10)) -> gen_c:c1:c28_10(n11_10), rt in Omega(1 + n11_10)


Generator Equations:
gen_c:c1:c28_10(0) <=> c
gen_c:c1:c28_10(+(x, 1)) <=> c2(gen_c:c1:c28_10(x))
gen_0':s:quotZeroErro9_10(0) <=> 0'
gen_0':s:quotZeroErro9_10(+(x, 1)) <=> s(gen_0':s:quotZeroErro9_10(x))


The following defined symbols remain to be analysed:
le, QUOTITER, quotIter

They will be analysed ascendingly in the following order:
le < QUOTITER
le < quotIter

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

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

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

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

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

(36)
Obligation:
Innermost TRS:
Rules:
LE(0', z0) -> c
LE(s(z0), 0') -> c1
LE(s(z0), s(z1)) -> c2(LE(z0, z1))
QUOT(z0, 0') -> c3
QUOT(z0, s(z1)) -> c4(QUOTITER(z0, s(z1), 0', 0', 0'))
QUOTITER(z0, s(z1), z2, z3, z4) -> c5(IF(le(z0, z2), z0, s(z1), z2, z3, z4), LE(z0, z2))
IF(true, z0, z1, z2, z3, z4) -> c6
IF(false, z0, z1, z2, z3, z4) -> c7(IF2(le(z1, s(z3)), z0, z1, s(z2), s(z3), z4), LE(z1, s(z3)))
IF2(false, z0, z1, z2, z3, z4) -> c8(QUOTITER(z0, z1, z2, z3, z4))
IF2(true, z0, z1, z2, z3, z4) -> c9(QUOTITER(z0, z1, z2, 0', s(z4)))
le(0', z0) -> true
le(s(z0), 0') -> false
le(s(z0), s(z1)) -> le(z0, z1)
quot(z0, 0') -> quotZeroErro
quot(z0, s(z1)) -> quotIter(z0, s(z1), 0', 0', 0')
quotIter(z0, s(z1), z2, z3, z4) -> if(le(z0, z2), z0, s(z1), z2, z3, z4)
if(true, z0, z1, z2, z3, z4) -> z4
if(false, z0, z1, z2, z3, z4) -> if2(le(z1, s(z3)), z0, z1, s(z2), s(z3), z4)
if2(false, z0, z1, z2, z3, z4) -> quotIter(z0, z1, z2, z3, z4)
if2(true, z0, z1, z2, z3, z4) -> quotIter(z0, z1, z2, 0', s(z4))

Types:
LE :: 0':s:quotZeroErro -> 0':s:quotZeroErro -> c:c1:c2
0' :: 0':s:quotZeroErro
c :: c:c1:c2
s :: 0':s:quotZeroErro -> 0':s:quotZeroErro
c1 :: c:c1:c2
c2 :: c:c1:c2 -> c:c1:c2
QUOT :: 0':s:quotZeroErro -> 0':s:quotZeroErro -> c3:c4
c3 :: c3:c4
c4 :: c5 -> c3:c4
QUOTITER :: 0':s:quotZeroErro -> 0':s:quotZeroErro -> 0':s:quotZeroErro -> 0':s:quotZeroErro -> 0':s:quotZeroErro -> c5
c5 :: c6:c7 -> c:c1:c2 -> c5
IF :: true:false -> 0':s:quotZeroErro -> 0':s:quotZeroErro -> 0':s:quotZeroErro -> 0':s:quotZeroErro -> 0':s:quotZeroErro -> c6:c7
le :: 0':s:quotZeroErro -> 0':s:quotZeroErro -> true:false
true :: true:false
c6 :: c6:c7
false :: true:false
c7 :: c8:c9 -> c:c1:c2 -> c6:c7
IF2 :: true:false -> 0':s:quotZeroErro -> 0':s:quotZeroErro -> 0':s:quotZeroErro -> 0':s:quotZeroErro -> 0':s:quotZeroErro -> c8:c9
c8 :: c5 -> c8:c9
c9 :: c5 -> c8:c9
quot :: 0':s:quotZeroErro -> 0':s:quotZeroErro -> 0':s:quotZeroErro
quotZeroErro :: 0':s:quotZeroErro
quotIter :: 0':s:quotZeroErro -> 0':s:quotZeroErro -> 0':s:quotZeroErro -> 0':s:quotZeroErro -> 0':s:quotZeroErro -> 0':s:quotZeroErro
if :: true:false -> 0':s:quotZeroErro -> 0':s:quotZeroErro -> 0':s:quotZeroErro -> 0':s:quotZeroErro -> 0':s:quotZeroErro -> 0':s:quotZeroErro
if2 :: true:false -> 0':s:quotZeroErro -> 0':s:quotZeroErro -> 0':s:quotZeroErro -> 0':s:quotZeroErro -> 0':s:quotZeroErro -> 0':s:quotZeroErro
hole_c:c1:c21_10 :: c:c1:c2
hole_0':s:quotZeroErro2_10 :: 0':s:quotZeroErro
hole_c3:c43_10 :: c3:c4
hole_c54_10 :: c5
hole_c6:c75_10 :: c6:c7
hole_true:false6_10 :: true:false
hole_c8:c97_10 :: c8:c9
gen_c:c1:c28_10 :: Nat -> c:c1:c2
gen_0':s:quotZeroErro9_10 :: Nat -> 0':s:quotZeroErro


Lemmas:
LE(gen_0':s:quotZeroErro9_10(n11_10), gen_0':s:quotZeroErro9_10(n11_10)) -> gen_c:c1:c28_10(n11_10), rt in Omega(1 + n11_10)
le(gen_0':s:quotZeroErro9_10(n579_10), gen_0':s:quotZeroErro9_10(n579_10)) -> true, rt in Omega(0)


Generator Equations:
gen_c:c1:c28_10(0) <=> c
gen_c:c1:c28_10(+(x, 1)) <=> c2(gen_c:c1:c28_10(x))
gen_0':s:quotZeroErro9_10(0) <=> 0'
gen_0':s:quotZeroErro9_10(+(x, 1)) <=> s(gen_0':s:quotZeroErro9_10(x))


The following defined symbols remain to be analysed:
QUOTITER, quotIter