WORST_CASE(Omega(n^1),O(n^1))
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^1).

(0) CpxRelTRS
(1) SInnermostTerminationProof [BOTH CONCRETE BOUNDS(ID, ID), 752 ms]
(2) CpxRelTRS
(3) RelTrsToWeightedTrsProof [BOTH BOUNDS(ID, ID), 0 ms]
(4) CpxWeightedTrs
    (5) CpxWeightedTrsRenamingProof [BOTH BOUNDS(ID, ID), 0 ms]
    (6) CpxWeightedTrs
    (7) TypeInferenceProof [BOTH BOUNDS(ID, ID), 0 ms]
    (8) CpxTypedWeightedTrs
    (9) CompletionProof [UPPER BOUND(ID), 0 ms]
    (10) CpxTypedWeightedCompleteTrs
    (11) CpxTypedWeightedTrsToRntsProof [UPPER BOUND(ID), 0 ms]
    (12) CpxRNTS
    (13) CompleteCoflocoProof [FINISHED, 7492 ms]
    (14) BOUNDS(1, n^1)
(15) RenamingProof [BOTH BOUNDS(ID, ID), 0 ms]
(16) CpxRelTRS
    (17) SlicingProof [LOWER BOUND(ID), 0 ms]
    (18) CpxRelTRS
    (19) TypeInferenceProof [BOTH BOUNDS(ID, ID), 0 ms]
    (20) typed CpxTrs
    (21) OrderProof [LOWER BOUND(ID), 0 ms]
    (22) typed CpxTrs
    (23) RewriteLemmaProof [LOWER BOUND(ID), 273 ms]
    (24) BEST
        (25) proven lower bound
            (26) LowerBoundPropagationProof [FINISHED, 0 ms]
            (27) BOUNDS(n^1, INF)
        (28) typed CpxTrs
            (29) RewriteLemmaProof [LOWER BOUND(ID), 79 ms]
            (30) typed CpxTrs
            (31) RewriteLemmaProof [LOWER BOUND(ID), 30 ms]
            (32) typed CpxTrs
            (33) RewriteLemmaProof [LOWER BOUND(ID), 48 ms]
            (34) typed CpxTrs


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

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


The TRS R consists of the following rules:

   LEQ(0, z0) -> c
   LEQ(s(z0), 0) -> c1
   LEQ(s(z0), s(z1)) -> c2(LEQ(z0, z1))
   IF(true, z0, z1) -> c3
   IF(false, z0, z1) -> c4
   -'(z0, 0) -> c5
   -'(s(z0), s(z1)) -> c6(-'(z0, z1))
   MOD(0, z0) -> c7
   MOD(s(z0), 0) -> c8
   MOD(s(z0), s(z1)) -> c9(IF(leq(z1, z0), mod(-(s(z0), s(z1)), s(z1)), s(z0)), LEQ(z1, z0))
   MOD(s(z0), s(z1)) -> c10(IF(leq(z1, z0), mod(-(s(z0), s(z1)), s(z1)), s(z0)), MOD(-(s(z0), s(z1)), s(z1)), -'(s(z0), s(z1)))

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

   leq(0, z0) -> true
   leq(s(z0), 0) -> false
   leq(s(z0), s(z1)) -> leq(z0, z1)
   if(true, z0, z1) -> z0
   if(false, z0, z1) -> z1
   -(z0, 0) -> z0
   -(s(z0), s(z1)) -> -(z0, z1)
   mod(0, z0) -> 0
   mod(s(z0), 0) -> 0
   mod(s(z0), s(z1)) -> if(leq(z1, z0), mod(-(s(z0), s(z1)), s(z1)), s(z0))

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^1).


The TRS R consists of the following rules:

   LEQ(0, z0) -> c
   LEQ(s(z0), 0) -> c1
   LEQ(s(z0), s(z1)) -> c2(LEQ(z0, z1))
   IF(true, z0, z1) -> c3
   IF(false, z0, z1) -> c4
   -'(z0, 0) -> c5
   -'(s(z0), s(z1)) -> c6(-'(z0, z1))
   MOD(0, z0) -> c7
   MOD(s(z0), 0) -> c8
   MOD(s(z0), s(z1)) -> c9(IF(leq(z1, z0), mod(-(s(z0), s(z1)), s(z1)), s(z0)), LEQ(z1, z0))
   MOD(s(z0), s(z1)) -> c10(IF(leq(z1, z0), mod(-(s(z0), s(z1)), s(z1)), s(z0)), MOD(-(s(z0), s(z1)), s(z1)), -'(s(z0), s(z1)))

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

   leq(0, z0) -> true
   leq(s(z0), 0) -> false
   leq(s(z0), s(z1)) -> leq(z0, z1)
   if(true, z0, z1) -> z0
   if(false, z0, z1) -> z1
   -(z0, 0) -> z0
   -(s(z0), s(z1)) -> -(z0, z1)
   mod(0, z0) -> 0
   mod(s(z0), 0) -> 0
   mod(s(z0), s(z1)) -> if(leq(z1, z0), mod(-(s(z0), s(z1)), s(z1)), s(z0))

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^1).


The TRS R consists of the following rules:

   LEQ(0, z0) -> c [1]
   LEQ(s(z0), 0) -> c1 [1]
   LEQ(s(z0), s(z1)) -> c2(LEQ(z0, z1)) [1]
   IF(true, z0, z1) -> c3 [1]
   IF(false, z0, z1) -> c4 [1]
   -'(z0, 0) -> c5 [1]
   -'(s(z0), s(z1)) -> c6(-'(z0, z1)) [1]
   MOD(0, z0) -> c7 [1]
   MOD(s(z0), 0) -> c8 [1]
   MOD(s(z0), s(z1)) -> c9(IF(leq(z1, z0), mod(-(s(z0), s(z1)), s(z1)), s(z0)), LEQ(z1, z0)) [1]
   MOD(s(z0), s(z1)) -> c10(IF(leq(z1, z0), mod(-(s(z0), s(z1)), s(z1)), s(z0)), MOD(-(s(z0), s(z1)), s(z1)), -'(s(z0), s(z1))) [1]
   leq(0, z0) -> true [0]
   leq(s(z0), 0) -> false [0]
   leq(s(z0), s(z1)) -> leq(z0, z1) [0]
   if(true, z0, z1) -> z0 [0]
   if(false, z0, z1) -> z1 [0]
   -(z0, 0) -> z0 [0]
   -(s(z0), s(z1)) -> -(z0, z1) [0]
   mod(0, z0) -> 0 [0]
   mod(s(z0), 0) -> 0 [0]
   mod(s(z0), s(z1)) -> if(leq(z1, z0), mod(-(s(z0), s(z1)), s(z1)), s(z0)) [0]

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

(5) CpxWeightedTrsRenamingProof (BOTH BOUNDS(ID, ID))
Renamed defined symbols to avoid conflicts with arithmetic symbols:

- => minus

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

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


The TRS R consists of the following rules:

   LEQ(0, z0) -> c [1]
   LEQ(s(z0), 0) -> c1 [1]
   LEQ(s(z0), s(z1)) -> c2(LEQ(z0, z1)) [1]
   IF(true, z0, z1) -> c3 [1]
   IF(false, z0, z1) -> c4 [1]
   -'(z0, 0) -> c5 [1]
   -'(s(z0), s(z1)) -> c6(-'(z0, z1)) [1]
   MOD(0, z0) -> c7 [1]
   MOD(s(z0), 0) -> c8 [1]
   MOD(s(z0), s(z1)) -> c9(IF(leq(z1, z0), mod(minus(s(z0), s(z1)), s(z1)), s(z0)), LEQ(z1, z0)) [1]
   MOD(s(z0), s(z1)) -> c10(IF(leq(z1, z0), mod(minus(s(z0), s(z1)), s(z1)), s(z0)), MOD(minus(s(z0), s(z1)), s(z1)), -'(s(z0), s(z1))) [1]
   leq(0, z0) -> true [0]
   leq(s(z0), 0) -> false [0]
   leq(s(z0), s(z1)) -> leq(z0, z1) [0]
   if(true, z0, z1) -> z0 [0]
   if(false, z0, z1) -> z1 [0]
   minus(z0, 0) -> z0 [0]
   minus(s(z0), s(z1)) -> minus(z0, z1) [0]
   mod(0, z0) -> 0 [0]
   mod(s(z0), 0) -> 0 [0]
   mod(s(z0), s(z1)) -> if(leq(z1, z0), mod(minus(s(z0), s(z1)), s(z1)), s(z0)) [0]

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

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

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

   LEQ(0, z0) -> c [1]
   LEQ(s(z0), 0) -> c1 [1]
   LEQ(s(z0), s(z1)) -> c2(LEQ(z0, z1)) [1]
   IF(true, z0, z1) -> c3 [1]
   IF(false, z0, z1) -> c4 [1]
   -'(z0, 0) -> c5 [1]
   -'(s(z0), s(z1)) -> c6(-'(z0, z1)) [1]
   MOD(0, z0) -> c7 [1]
   MOD(s(z0), 0) -> c8 [1]
   MOD(s(z0), s(z1)) -> c9(IF(leq(z1, z0), mod(minus(s(z0), s(z1)), s(z1)), s(z0)), LEQ(z1, z0)) [1]
   MOD(s(z0), s(z1)) -> c10(IF(leq(z1, z0), mod(minus(s(z0), s(z1)), s(z1)), s(z0)), MOD(minus(s(z0), s(z1)), s(z1)), -'(s(z0), s(z1))) [1]
   leq(0, z0) -> true [0]
   leq(s(z0), 0) -> false [0]
   leq(s(z0), s(z1)) -> leq(z0, z1) [0]
   if(true, z0, z1) -> z0 [0]
   if(false, z0, z1) -> z1 [0]
   minus(z0, 0) -> z0 [0]
   minus(s(z0), s(z1)) -> minus(z0, z1) [0]
   mod(0, z0) -> 0 [0]
   mod(s(z0), 0) -> 0 [0]
   mod(s(z0), s(z1)) -> if(leq(z1, z0), mod(minus(s(z0), s(z1)), s(z1)), s(z0)) [0]

The TRS has the following type information:
LEQ :: 0:s -> 0:s -> c:c1:c2
0 :: 0:s
c :: c:c1:c2
s :: 0:s -> 0:s
c1 :: c:c1:c2
c2 :: c:c1:c2 -> c:c1:c2
IF :: true:false -> 0:s -> 0:s -> c3:c4
true :: true:false
c3 :: c3:c4
false :: true:false
c4 :: c3:c4
-' :: 0:s -> 0:s -> c5:c6
c5 :: c5:c6
c6 :: c5:c6 -> c5:c6
MOD :: 0:s -> 0:s -> c7:c8:c9:c10
c7 :: c7:c8:c9:c10
c8 :: c7:c8:c9:c10
c9 :: c3:c4 -> c:c1:c2 -> c7:c8:c9:c10
leq :: 0:s -> 0:s -> true:false
mod :: 0:s -> 0:s -> 0:s
minus :: 0:s -> 0:s -> 0:s
c10 :: c3:c4 -> c7:c8:c9:c10 -> c5:c6 -> c7:c8:c9:c10
if :: true:false -> 0:s -> 0:s -> 0:s

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

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

   leq(v0, v1) -> null_leq [0]
   if(v0, v1, v2) -> null_if [0]
   minus(v0, v1) -> null_minus [0]
   mod(v0, v1) -> null_mod [0]
   LEQ(v0, v1) -> null_LEQ [0]
   IF(v0, v1, v2) -> null_IF [0]
   -'(v0, v1) -> null_-' [0]
   MOD(v0, v1) -> null_MOD [0]

And the following fresh constants:    null_leq, null_if, null_minus, null_mod, null_LEQ, null_IF, null_-', null_MOD

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

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

   LEQ(0, z0) -> c [1]
   LEQ(s(z0), 0) -> c1 [1]
   LEQ(s(z0), s(z1)) -> c2(LEQ(z0, z1)) [1]
   IF(true, z0, z1) -> c3 [1]
   IF(false, z0, z1) -> c4 [1]
   -'(z0, 0) -> c5 [1]
   -'(s(z0), s(z1)) -> c6(-'(z0, z1)) [1]
   MOD(0, z0) -> c7 [1]
   MOD(s(z0), 0) -> c8 [1]
   MOD(s(z0), s(z1)) -> c9(IF(leq(z1, z0), mod(minus(s(z0), s(z1)), s(z1)), s(z0)), LEQ(z1, z0)) [1]
   MOD(s(z0), s(z1)) -> c10(IF(leq(z1, z0), mod(minus(s(z0), s(z1)), s(z1)), s(z0)), MOD(minus(s(z0), s(z1)), s(z1)), -'(s(z0), s(z1))) [1]
   leq(0, z0) -> true [0]
   leq(s(z0), 0) -> false [0]
   leq(s(z0), s(z1)) -> leq(z0, z1) [0]
   if(true, z0, z1) -> z0 [0]
   if(false, z0, z1) -> z1 [0]
   minus(z0, 0) -> z0 [0]
   minus(s(z0), s(z1)) -> minus(z0, z1) [0]
   mod(0, z0) -> 0 [0]
   mod(s(z0), 0) -> 0 [0]
   mod(s(z0), s(z1)) -> if(leq(z1, z0), mod(minus(s(z0), s(z1)), s(z1)), s(z0)) [0]
   leq(v0, v1) -> null_leq [0]
   if(v0, v1, v2) -> null_if [0]
   minus(v0, v1) -> null_minus [0]
   mod(v0, v1) -> null_mod [0]
   LEQ(v0, v1) -> null_LEQ [0]
   IF(v0, v1, v2) -> null_IF [0]
   -'(v0, v1) -> null_-' [0]
   MOD(v0, v1) -> null_MOD [0]

The TRS has the following type information:
LEQ :: 0:s:null_if:null_minus:null_mod -> 0:s:null_if:null_minus:null_mod -> c:c1:c2:null_LEQ
0 :: 0:s:null_if:null_minus:null_mod
c :: c:c1:c2:null_LEQ
s :: 0:s:null_if:null_minus:null_mod -> 0:s:null_if:null_minus:null_mod
c1 :: c:c1:c2:null_LEQ
c2 :: c:c1:c2:null_LEQ -> c:c1:c2:null_LEQ
IF :: true:false:null_leq -> 0:s:null_if:null_minus:null_mod -> 0:s:null_if:null_minus:null_mod -> c3:c4:null_IF
true :: true:false:null_leq
c3 :: c3:c4:null_IF
false :: true:false:null_leq
c4 :: c3:c4:null_IF
-' :: 0:s:null_if:null_minus:null_mod -> 0:s:null_if:null_minus:null_mod -> c5:c6:null_-'
c5 :: c5:c6:null_-'
c6 :: c5:c6:null_-' -> c5:c6:null_-'
MOD :: 0:s:null_if:null_minus:null_mod -> 0:s:null_if:null_minus:null_mod -> c7:c8:c9:c10:null_MOD
c7 :: c7:c8:c9:c10:null_MOD
c8 :: c7:c8:c9:c10:null_MOD
c9 :: c3:c4:null_IF -> c:c1:c2:null_LEQ -> c7:c8:c9:c10:null_MOD
leq :: 0:s:null_if:null_minus:null_mod -> 0:s:null_if:null_minus:null_mod -> true:false:null_leq
mod :: 0:s:null_if:null_minus:null_mod -> 0:s:null_if:null_minus:null_mod -> 0:s:null_if:null_minus:null_mod
minus :: 0:s:null_if:null_minus:null_mod -> 0:s:null_if:null_minus:null_mod -> 0:s:null_if:null_minus:null_mod
c10 :: c3:c4:null_IF -> c7:c8:c9:c10:null_MOD -> c5:c6:null_-' -> c7:c8:c9:c10:null_MOD
if :: true:false:null_leq -> 0:s:null_if:null_minus:null_mod -> 0:s:null_if:null_minus:null_mod -> 0:s:null_if:null_minus:null_mod
null_leq :: true:false:null_leq
null_if :: 0:s:null_if:null_minus:null_mod
null_minus :: 0:s:null_if:null_minus:null_mod
null_mod :: 0:s:null_if:null_minus:null_mod
null_LEQ :: c:c1:c2:null_LEQ
null_IF :: c3:c4:null_IF
null_-' :: c5:c6:null_-'
null_MOD :: c7:c8:c9:c10:null_MOD

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

(11) 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
   true => 2
   c3 => 1
   false => 1
   c4 => 2
   c5 => 0
   c7 => 0
   c8 => 1
   null_leq => 0
   null_if => 0
   null_minus => 0
   null_mod => 0
   null_LEQ => 0
   null_IF => 0
   null_-' => 0
   null_MOD => 0

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

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

   -'(z, z') -{ 1 }-> 0 :|: z = z0, z0 >= 0, z' = 0
   -'(z, z') -{ 0 }-> 0 :|: v0 >= 0, v1 >= 0, z = v0, z' = v1
   -'(z, z') -{ 1 }-> 1 + -'(z0, z1) :|: z1 >= 0, z = 1 + z0, z0 >= 0, z' = 1 + z1
   IF(z, z', z'') -{ 1 }-> 2 :|: z1 >= 0, z = 1, z0 >= 0, z' = z0, z'' = z1
   IF(z, z', z'') -{ 1 }-> 1 :|: z = 2, z1 >= 0, z0 >= 0, z' = z0, z'' = z1
   IF(z, z', z'') -{ 0 }-> 0 :|: v0 >= 0, z'' = v2, v1 >= 0, z = v0, z' = v1, v2 >= 0
   LEQ(z, z') -{ 1 }-> 1 :|: z = 1 + z0, z0 >= 0, z' = 0
   LEQ(z, z') -{ 1 }-> 0 :|: z0 >= 0, z = 0, z' = z0
   LEQ(z, z') -{ 0 }-> 0 :|: v0 >= 0, v1 >= 0, z = v0, z' = v1
   LEQ(z, z') -{ 1 }-> 1 + LEQ(z0, z1) :|: z1 >= 0, z = 1 + z0, z0 >= 0, z' = 1 + z1
   MOD(z, z') -{ 1 }-> 1 :|: z = 1 + z0, z0 >= 0, z' = 0
   MOD(z, z') -{ 1 }-> 0 :|: z0 >= 0, z = 0, z' = z0
   MOD(z, z') -{ 0 }-> 0 :|: v0 >= 0, v1 >= 0, z = v0, z' = v1
   MOD(z, z') -{ 1 }-> 1 + IF(leq(z1, z0), mod(minus(1 + z0, 1 + z1), 1 + z1), 1 + z0) + LEQ(z1, z0) :|: z1 >= 0, z = 1 + z0, z0 >= 0, z' = 1 + z1
   MOD(z, z') -{ 1 }-> 1 + IF(leq(z1, z0), mod(minus(1 + z0, 1 + z1), 1 + z1), 1 + z0) + MOD(minus(1 + z0, 1 + z1), 1 + z1) + -'(1 + z0, 1 + z1) :|: z1 >= 0, z = 1 + z0, z0 >= 0, z' = 1 + z1
   if(z, z', z'') -{ 0 }-> z0 :|: z = 2, z1 >= 0, z0 >= 0, z' = z0, z'' = z1
   if(z, z', z'') -{ 0 }-> z1 :|: z1 >= 0, z = 1, z0 >= 0, z' = z0, z'' = z1
   if(z, z', z'') -{ 0 }-> 0 :|: v0 >= 0, z'' = v2, v1 >= 0, z = v0, z' = v1, v2 >= 0
   leq(z, z') -{ 0 }-> leq(z0, z1) :|: z1 >= 0, z = 1 + z0, z0 >= 0, z' = 1 + z1
   leq(z, z') -{ 0 }-> 2 :|: z0 >= 0, z = 0, z' = z0
   leq(z, z') -{ 0 }-> 1 :|: z = 1 + z0, z0 >= 0, z' = 0
   leq(z, z') -{ 0 }-> 0 :|: v0 >= 0, v1 >= 0, z = v0, z' = v1
   minus(z, z') -{ 0 }-> z0 :|: z = z0, z0 >= 0, z' = 0
   minus(z, z') -{ 0 }-> minus(z0, z1) :|: z1 >= 0, z = 1 + z0, z0 >= 0, z' = 1 + z1
   minus(z, z') -{ 0 }-> 0 :|: v0 >= 0, v1 >= 0, z = v0, z' = v1
   mod(z, z') -{ 0 }-> if(leq(z1, z0), mod(minus(1 + z0, 1 + z1), 1 + z1), 1 + z0) :|: z1 >= 0, z = 1 + z0, z0 >= 0, z' = 1 + z1
   mod(z, z') -{ 0 }-> 0 :|: z0 >= 0, z = 0, z' = z0
   mod(z, z') -{ 0 }-> 0 :|: z = 1 + z0, z0 >= 0, z' = 0
   mod(z, z') -{ 0 }-> 0 :|: v0 >= 0, v1 >= 0, z = v0, z' = v1

Only complete derivations are relevant for the runtime complexity.

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

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

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


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

#### Computed strongly connected components 
0. recursive  : [fun/3]
1. non_recursive  : [fun1/4]
2. recursive  : [fun2/3]
3. recursive  : [leq/3]
4. recursive  : [minus/3]
5. non_recursive  : [if/4]
6. recursive [non_tail] : [(mod)/3]
7. recursive [non_tail] : [fun3/3]
8. non_recursive  : [start/3]

#### Obtained direct recursion through partial evaluation 
0. SCC is partially evaluated into fun/3
1. SCC is partially evaluated into fun1/4
2. SCC is partially evaluated into fun2/3
3. SCC is partially evaluated into leq/3
4. SCC is partially evaluated into minus/3
5. SCC is partially evaluated into if/4
6. SCC is partially evaluated into (mod)/3
7. SCC is partially evaluated into fun3/3
8. SCC is partially evaluated into start/3

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

### Specialization of cost equations fun/3 
* CE 10 is refined into CE [37] 
* CE 9 is refined into CE [38] 
* CE 12 is refined into CE [39] 
* CE 11 is refined into CE [40] 


### Cost equations --> "Loop" of fun/3 
* CEs [40] --> Loop 26 
* CEs [37] --> Loop 27 
* CEs [38,39] --> Loop 28 

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

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


### Specialization of cost equations fun1/4 
* CE 15 is refined into CE [41] 
* CE 13 is refined into CE [42] 
* CE 14 is refined into CE [43] 


### Cost equations --> "Loop" of fun1/4 
* CEs [41] --> Loop 29 
* CEs [42] --> Loop 30 
* CEs [43] --> Loop 31 

### Ranking functions of CR fun1(V1,V,V7,Out) 

#### Partial ranking functions of CR fun1(V1,V,V7,Out) 


### Specialization of cost equations fun2/3 
* CE 16 is refined into CE [44] 
* CE 18 is refined into CE [45] 
* CE 17 is refined into CE [46] 


### Cost equations --> "Loop" of fun2/3 
* CEs [46] --> Loop 32 
* CEs [44,45] --> Loop 33 

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

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


### Specialization of cost equations leq/3 
* CE 27 is refined into CE [47] 
* CE 25 is refined into CE [48] 
* CE 24 is refined into CE [49] 
* CE 26 is refined into CE [50] 


### Cost equations --> "Loop" of leq/3 
* CEs [50] --> Loop 34 
* CEs [47] --> Loop 35 
* CEs [48] --> Loop 36 
* CEs [49] --> Loop 37 

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

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


### Specialization of cost equations minus/3 
* CE 33 is refined into CE [51] 
* CE 31 is refined into CE [52] 
* CE 32 is refined into CE [53] 


### Cost equations --> "Loop" of minus/3 
* CEs [53] --> Loop 38 
* CEs [51] --> Loop 39 
* CEs [52] --> Loop 40 

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

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


### Specialization of cost equations if/4 
* CE 30 is refined into CE [54] 
* CE 28 is refined into CE [55] 
* CE 29 is refined into CE [56] 


### Cost equations --> "Loop" of if/4 
* CEs [54] --> Loop 41 
* CEs [55] --> Loop 42 
* CEs [56] --> Loop 43 

### Ranking functions of CR if(V1,V,V7,Out) 

#### Partial ranking functions of CR if(V1,V,V7,Out) 


### Specialization of cost equations (mod)/3 
* CE 34 is refined into CE [57] 
* CE 35 is refined into CE [58] 
* CE 36 is refined into CE [59,60,61,62,63,64,65,66,67,68,69,70,71,72] 


### Cost equations --> "Loop" of (mod)/3 
* CEs [71] --> Loop 44 
* CEs [69] --> Loop 45 
* CEs [67] --> Loop 46 
* CEs [61] --> Loop 47 
* CEs [59] --> Loop 48 
* CEs [62,66,72] --> Loop 49 
* CEs [60] --> Loop 50 
* CEs [63] --> Loop 51 
* CEs [64,65,68,70] --> Loop 52 
* CEs [57,58] --> Loop 53 

### Ranking functions of CR mod(V1,V,Out) 
* RF of phase [44,47,49]: [V1,V1-V+1]

#### Partial ranking functions of CR mod(V1,V,Out) 
* Partial RF of phase [44,47,49]:
  - RF of loop [44:1]:
    V1-1
  - RF of loop [44:1,49:1]:
    V1-V+1
  - RF of loop [47:1,49:1]:
    V1


### Specialization of cost equations fun3/3 
* CE 21 is refined into CE [73,74,75,76,77,78,79,80,81,82,83,84,85,86,87,88,89,90,91,92,93,94,95,96,97,98,99,100,101,102,103,104,105,106,107,108,109,110,111,112,113,114,115,116,117,118,119,120,121,122,123,124] 
* CE 20 is refined into CE [125] 
* CE 19 is refined into CE [126] 
* CE 23 is refined into CE [127] 
* CE 22 is refined into CE [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,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] 


### Cost equations --> "Loop" of fun3/3 
* CEs [211] --> Loop 54 
* CEs [167,215] --> Loop 55 
* CEs [178,194,202,210,218] --> Loop 56 
* CEs [179,187,195,203,219] --> Loop 57 
* CEs [155,163,171,183,186,191,199,207,223] --> Loop 58 
* CEs [154,190] --> Loop 59 
* CEs [209] --> Loop 60 
* CEs [165,213] --> Loop 61 
* CEs [173] --> Loop 62 
* CEs [172,175] --> Loop 63 
* CEs [176,192,200,208,216] --> Loop 64 
* CEs [177,185,193,201,217] --> Loop 65 
* CEs [153,161,169,181,184,189,197,205,221] --> Loop 66 
* CEs [152,188] --> Loop 67 
* CEs [131,139] --> Loop 68 
* CEs [130,135,138,143,151,159] --> Loop 69 
* CEs [134,142,150,158,162,166,170,182,198,206,214,222] --> Loop 70 
* CEs [129,137] --> Loop 71 
* CEs [128,133,136,141,157] --> Loop 72 
* CEs [132,140] --> Loop 73 
* CEs [145] --> Loop 74 
* CEs [144] --> Loop 75 
* CEs [147,149] --> Loop 76 
* CEs [146,148,156,160,164,168,174,180,196,204,212,220] --> Loop 77 
* CEs [97] --> Loop 78 
* CEs [114] --> Loop 79 
* CEs [90,116] --> Loop 80 
* CEs [100] --> Loop 81 
* CEs [118,122] --> Loop 82 
* CEs [94,124] --> Loop 83 
* CEs [83,99] --> Loop 84 
* CEs [96] --> Loop 85 
* CEs [102,106,110] --> Loop 86 
* CEs [86,108] --> Loop 87 
* CEs [95] --> Loop 88 
* CEs [92,117,120] --> Loop 89 
* CEs [84,88,101,104,105,109,112,113,121] --> Loop 90 
* CEs [85,107] --> Loop 91 
* CEs [73,75] --> Loop 92 
* CEs [74,76] --> Loop 93 
* CEs [125] --> Loop 94 
* CEs [77] --> Loop 95 
* CEs [78] --> Loop 96 
* CEs [79,81] --> Loop 97 
* CEs [80,82,87,89,91,93,98,103,111,115,119,123] --> Loop 98 
* CEs [126,127] --> Loop 99 

### Ranking functions of CR fun3(V1,V,Out) 
* RF of phase [54,55,56,57,58,68,69,70]: [V1,V1-V+1]

#### Partial ranking functions of CR fun3(V1,V,Out) 
* Partial RF of phase [54,55,56,57,58,68,69,70]:
  - RF of loop [54:1,55:1]:
    V1/2-2
    V1/2-V
  - RF of loop [56:1,57:1,58:1]:
    V1-1
  - RF of loop [56:1,57:1,58:1,69:1,70:1]:
    V1-V+1
  - RF of loop [68:1,69:1,70:1]:
    V1


### Specialization of cost equations start/3 
* CE 1 is refined into CE [224,225,226,227] 
* CE 2 is refined into CE [228,229,230] 
* CE 3 is refined into CE [231,232] 
* CE 4 is refined into CE [233,234,235,236,237,238,239,240,241,242,243,244,245,246,247,248,249,250,251,252] 
* CE 5 is refined into CE [253,254,255,256,257] 
* CE 6 is refined into CE [258,259,260] 
* CE 7 is refined into CE [261,262,263] 
* CE 8 is refined into CE [264,265,266,267,268] 


### Cost equations --> "Loop" of start/3 
* CEs [244,246,248,250] --> Loop 100 
* CEs [239,240,241,242] --> Loop 101 
* CEs [224,236,254,261] --> Loop 102 
* CEs [229,259] --> Loop 103 
* CEs [234,235,264] --> Loop 104 
* CEs [228,258] --> Loop 105 
* CEs [225,226,227,230,231,232,233,237,238,243,245,247,249,251,252,253,255,256,257,260,262,263,265,266,267,268] --> Loop 106 

### Ranking functions of CR start(V1,V,V7) 

#### Partial ranking functions of CR start(V1,V,V7) 


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

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

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

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

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

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

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


#### Cost of chains of fun1(V1,V,V7,Out):
* Chain [31]: 1
  with precondition: [V1=1,Out=2,V>=0,V7>=0] 

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

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


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

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

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


#### Cost of chains of leq(V1,V,Out):
* Chain [[34],37]: 0
  with precondition: [Out=2,V1>=1,V>=V1] 

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

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

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

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

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


#### Cost of chains of minus(V1,V,Out):
* Chain [[38],40]: 0
  with precondition: [V1=Out+V,V>=1,V1>=V] 

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

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

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


#### Cost of chains of if(V1,V,V7,Out):
* Chain [43]: 0
  with precondition: [V1=1,V7=Out,V>=0,V7>=0] 

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

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


#### Cost of chains of mod(V1,V,Out):
* Chain [[44,47,49],53]: 0
  with precondition: [Out=0,V>=1,V1>=V] 

* Chain [[44,47,49],52,53]: 0
  with precondition: [Out=0,V>=1,V1>=V+1] 

* Chain [[44,47,49],51,53]: 0
  with precondition: [1>=Out,V>=2,Out>=0,V1>=V+1] 

* Chain [[44,47,49],50,53]: 0
  with precondition: [V=1,Out=0,V1>=2] 

* Chain [[44,47,49],48,53]: 0
  with precondition: [V=1,Out=0,V1>=2] 

* Chain [[44,47,49],46,53]: 0
  with precondition: [V>=3,Out>=0,V1>=V+2,V>=Out+1,V1>=Out+V] 

* Chain [[44,47,49],45,53]: 0
  with precondition: [Out=0,V>=2,V1>=2*V] 

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

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

* Chain [51,53]: 0
  with precondition: [V1=1,Out=1,V>=2] 

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

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

* Chain [46,53]: 0
  with precondition: [V1=Out,V1>=2,V>=V1+1] 

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


#### Cost of chains of fun3(V1,V,Out):
* Chain [[54,55,56,57,58,68,69,70],99]: 5*it(54)+6*it(56)+3*it(58)+8*it(68)+2*it(70)+3*s(34)+13*s(37)+2*s(41)+2*s(42)+1
  Such that:aux(13) =< V1+1/3
aux(14) =< V1-V+1
aux(18) =< V1/2-V
aux(23) =< V1
aux(24) =< V1/2
aux(25) =< 6/5*V1
aux(11) =< aux(23)
it(54) =< aux(23)
it(56) =< aux(23)
it(58) =< aux(23)
it(68) =< aux(23)
it(70) =< aux(23)
s(34) =< aux(23)
it(58) =< aux(13)
it(68) =< aux(13)
it(70) =< aux(13)
s(38) =< aux(13)
aux(11) =< aux(14)
it(54) =< aux(14)
it(56) =< aux(14)
it(58) =< aux(14)
it(68) =< aux(14)
it(70) =< aux(14)
s(38) =< aux(23)
it(54) =< aux(24)
it(54) =< aux(18)
it(56) =< aux(24)
it(58) =< aux(24)
it(70) =< aux(25)
s(41) =< aux(11)
s(42) =< aux(25)
s(37) =< s(38)

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

* Chain [[54,55,56,57,58,68,69,70],98]: 5*it(54)+6*it(56)+3*it(58)+8*it(68)+2*it(70)+3*s(34)+13*s(37)+2*s(41)+2*s(42)+2
  Such that:aux(13) =< V1+1/3
aux(14) =< V1-V+1
aux(18) =< V1/2-V
aux(26) =< V1
aux(27) =< V1/2
aux(28) =< 6/5*V1
aux(11) =< aux(26)
it(54) =< aux(26)
it(56) =< aux(26)
it(58) =< aux(26)
it(68) =< aux(26)
it(70) =< aux(26)
s(34) =< aux(26)
it(58) =< aux(13)
it(68) =< aux(13)
it(70) =< aux(13)
s(38) =< aux(13)
aux(11) =< aux(14)
it(54) =< aux(14)
it(56) =< aux(14)
it(58) =< aux(14)
it(68) =< aux(14)
it(70) =< aux(14)
s(38) =< aux(26)
it(54) =< aux(27)
it(54) =< aux(18)
it(56) =< aux(27)
it(58) =< aux(27)
it(70) =< aux(28)
s(41) =< aux(11)
s(42) =< aux(28)
s(37) =< s(38)

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

* Chain [[54,55,56,57,58,68,69,70],97]: 5*it(54)+6*it(56)+3*it(58)+8*it(68)+2*it(70)+3*s(34)+13*s(37)+2*s(41)+2*s(42)+2
  Such that:aux(13) =< V1+1/3
aux(14) =< V1-V+1
aux(18) =< V1/2-V
aux(29) =< V1
aux(30) =< V1/2
aux(31) =< 6/5*V1
aux(11) =< aux(29)
it(54) =< aux(29)
it(56) =< aux(29)
it(58) =< aux(29)
it(68) =< aux(29)
it(70) =< aux(29)
s(34) =< aux(29)
it(58) =< aux(13)
it(68) =< aux(13)
it(70) =< aux(13)
s(38) =< aux(13)
aux(11) =< aux(14)
it(54) =< aux(14)
it(56) =< aux(14)
it(58) =< aux(14)
it(68) =< aux(14)
it(70) =< aux(14)
s(38) =< aux(29)
it(54) =< aux(30)
it(54) =< aux(18)
it(56) =< aux(30)
it(58) =< aux(30)
it(70) =< aux(31)
s(41) =< aux(11)
s(42) =< aux(31)
s(37) =< s(38)

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

* Chain [[54,55,56,57,58,68,69,70],96]: 5*it(54)+6*it(56)+3*it(58)+8*it(68)+2*it(70)+3*s(34)+13*s(37)+2*s(41)+2*s(42)+3
  Such that:aux(13) =< V1+1/3
aux(14) =< V1-V+1
aux(18) =< V1/2-V
aux(32) =< V1
aux(33) =< V1/2
aux(34) =< 6/5*V1
aux(11) =< aux(32)
it(54) =< aux(32)
it(56) =< aux(32)
it(58) =< aux(32)
it(68) =< aux(32)
it(70) =< aux(32)
s(34) =< aux(32)
it(58) =< aux(13)
it(68) =< aux(13)
it(70) =< aux(13)
s(38) =< aux(13)
aux(11) =< aux(14)
it(54) =< aux(14)
it(56) =< aux(14)
it(58) =< aux(14)
it(68) =< aux(14)
it(70) =< aux(14)
s(38) =< aux(32)
it(54) =< aux(33)
it(54) =< aux(18)
it(56) =< aux(33)
it(58) =< aux(33)
it(70) =< aux(34)
s(41) =< aux(11)
s(42) =< aux(34)
s(37) =< s(38)

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

* Chain [[54,55,56,57,58,68,69,70],95]: 5*it(54)+6*it(56)+3*it(58)+8*it(68)+2*it(70)+3*s(34)+13*s(37)+2*s(41)+2*s(42)+3
  Such that:aux(13) =< V1+1/3
aux(14) =< V1-V+1
aux(18) =< V1/2-V
aux(35) =< V1
aux(36) =< V1/2
aux(37) =< 6/5*V1
aux(11) =< aux(35)
it(54) =< aux(35)
it(56) =< aux(35)
it(58) =< aux(35)
it(68) =< aux(35)
it(70) =< aux(35)
s(34) =< aux(35)
it(58) =< aux(13)
it(68) =< aux(13)
it(70) =< aux(13)
s(38) =< aux(13)
aux(11) =< aux(14)
it(54) =< aux(14)
it(56) =< aux(14)
it(58) =< aux(14)
it(68) =< aux(14)
it(70) =< aux(14)
s(38) =< aux(35)
it(54) =< aux(36)
it(54) =< aux(18)
it(56) =< aux(36)
it(58) =< aux(36)
it(70) =< aux(37)
s(41) =< aux(11)
s(42) =< aux(37)
s(37) =< s(38)

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

* Chain [[54,55,56,57,58,68,69,70],93]: 11*it(54)+3*it(58)+8*it(68)+2*it(70)+5*s(34)+13*s(37)+2*s(42)+2
  Such that:aux(13) =< V1+1/3
aux(38) =< V1
aux(39) =< V1/2
aux(40) =< 6/5*V1
it(54) =< aux(38)
it(58) =< aux(38)
it(68) =< aux(38)
it(70) =< aux(38)
s(34) =< aux(38)
it(58) =< aux(13)
it(68) =< aux(13)
it(70) =< aux(13)
s(38) =< aux(13)
s(38) =< aux(38)
it(54) =< aux(39)
it(58) =< aux(39)
it(70) =< aux(40)
s(42) =< aux(40)
s(37) =< s(38)

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

* Chain [[54,55,56,57,58,68,69,70],92]: 11*it(54)+3*it(58)+8*it(68)+2*it(70)+5*s(34)+13*s(37)+2*s(42)+3
  Such that:aux(13) =< V1+1/3
aux(41) =< V1
aux(42) =< V1/2
aux(43) =< 6/5*V1
it(54) =< aux(41)
it(58) =< aux(41)
it(68) =< aux(41)
it(70) =< aux(41)
s(34) =< aux(41)
it(58) =< aux(13)
it(68) =< aux(13)
it(70) =< aux(13)
s(38) =< aux(13)
s(38) =< aux(41)
it(54) =< aux(42)
it(58) =< aux(42)
it(70) =< aux(43)
s(42) =< aux(43)
s(37) =< s(38)

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

* Chain [[54,55,56,57,58,68,69,70],91]: 5*it(54)+6*it(56)+3*it(58)+8*it(68)+2*it(70)+1*s(34)+2*s(35)+13*s(37)+2*s(41)+2*s(42)+2
  Such that:aux(12) =< V1
aux(13) =< V1+1/3
aux(14) =< V1-V+1
aux(17) =< V1/2
aux(18) =< V1/2-V
aux(21) =< 6/5*V1
aux(22) =< 6/5*V1-6/5*V
aux(44) =< V1-V
aux(45) =< V1/2-V/2
aux(11) =< aux(12)
it(54) =< aux(12)
it(56) =< aux(12)
it(58) =< aux(12)
it(68) =< aux(12)
it(70) =< aux(12)
s(34) =< aux(12)
s(36) =< aux(12)
it(58) =< aux(13)
it(68) =< aux(13)
it(70) =< aux(13)
s(38) =< aux(13)
aux(11) =< aux(14)
it(54) =< aux(14)
it(56) =< aux(14)
it(58) =< aux(14)
it(68) =< aux(14)
it(70) =< aux(14)
aux(11) =< aux(44)
it(54) =< aux(44)
it(56) =< aux(44)
it(58) =< aux(44)
it(68) =< aux(44)
it(70) =< aux(44)
s(34) =< aux(44)
s(36) =< aux(44)
s(38) =< aux(44)
it(54) =< aux(17)
it(54) =< aux(18)
it(54) =< aux(45)
it(56) =< aux(45)
it(58) =< aux(45)
it(70) =< aux(21)
s(43) =< aux(21)
it(70) =< aux(22)
s(43) =< aux(22)
s(41) =< aux(11)
s(42) =< s(43)
s(37) =< s(38)
s(35) =< s(36)

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

* Chain [[54,55,56,57,58,68,69,70],90]: 5*it(54)+6*it(56)+3*it(58)+8*it(68)+2*it(70)+3*s(34)+13*s(37)+2*s(41)+2*s(42)+4*s(45)+3
  Such that:aux(13) =< V1+1/3
aux(14) =< V1-V+1
aux(18) =< V1/2-V
aux(46) =< V
aux(47) =< V1
aux(48) =< V1/2
aux(49) =< 6/5*V1
s(45) =< aux(46)
aux(11) =< aux(47)
it(54) =< aux(47)
it(56) =< aux(47)
it(58) =< aux(47)
it(68) =< aux(47)
it(70) =< aux(47)
s(34) =< aux(47)
it(58) =< aux(13)
it(68) =< aux(13)
it(70) =< aux(13)
s(38) =< aux(13)
aux(11) =< aux(14)
it(54) =< aux(14)
it(56) =< aux(14)
it(58) =< aux(14)
it(68) =< aux(14)
it(70) =< aux(14)
s(38) =< aux(47)
it(54) =< aux(48)
it(54) =< aux(18)
it(56) =< aux(48)
it(58) =< aux(48)
it(70) =< aux(49)
s(41) =< aux(11)
s(42) =< aux(49)
s(37) =< s(38)

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

* Chain [[54,55,56,57,58,68,69,70],89]: 5*it(54)+6*it(56)+3*it(58)+8*it(68)+2*it(70)+1*s(34)+2*s(35)+13*s(37)+2*s(41)+2*s(42)+2*s(49)+3
  Such that:aux(12) =< V1
aux(13) =< V1+1/3
aux(14) =< V1-V+1
aux(17) =< V1/2
aux(21) =< 6/5*V1
aux(22) =< 6/5*V1-12/5*V
aux(50) =< V
aux(51) =< V1-2*V
aux(52) =< V1/2-V
s(49) =< aux(50)
aux(11) =< aux(12)
it(54) =< aux(12)
it(56) =< aux(12)
it(58) =< aux(12)
it(68) =< aux(12)
it(70) =< aux(12)
s(34) =< aux(12)
s(36) =< aux(12)
it(58) =< aux(13)
it(68) =< aux(13)
it(70) =< aux(13)
s(38) =< aux(13)
aux(11) =< aux(14)
it(54) =< aux(14)
it(56) =< aux(14)
it(58) =< aux(14)
it(68) =< aux(14)
it(70) =< aux(14)
aux(11) =< aux(51)
it(54) =< aux(51)
it(56) =< aux(51)
it(58) =< aux(51)
it(68) =< aux(51)
it(70) =< aux(51)
s(34) =< aux(51)
s(36) =< aux(51)
s(38) =< aux(51)
it(54) =< aux(17)
it(54) =< aux(52)
it(56) =< aux(52)
it(58) =< aux(52)
it(70) =< aux(21)
s(43) =< aux(21)
it(70) =< aux(22)
s(43) =< aux(22)
s(41) =< aux(11)
s(42) =< s(43)
s(37) =< s(38)
s(35) =< s(36)

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

* Chain [[54,55,56,57,58,68,69,70],88]: 5*it(54)+6*it(56)+3*it(58)+8*it(68)+2*it(70)+3*s(34)+13*s(37)+2*s(41)+2*s(42)+3
  Such that:aux(13) =< V1+1/3
aux(14) =< V1-V+1
aux(18) =< V1/2-V
aux(53) =< V1
aux(54) =< V1/2
aux(55) =< 6/5*V1
aux(11) =< aux(53)
it(54) =< aux(53)
it(56) =< aux(53)
it(58) =< aux(53)
it(68) =< aux(53)
it(70) =< aux(53)
s(34) =< aux(53)
it(58) =< aux(13)
it(68) =< aux(13)
it(70) =< aux(13)
s(38) =< aux(13)
aux(11) =< aux(14)
it(54) =< aux(14)
it(56) =< aux(14)
it(58) =< aux(14)
it(68) =< aux(14)
it(70) =< aux(14)
s(38) =< aux(53)
it(54) =< aux(54)
it(54) =< aux(18)
it(56) =< aux(54)
it(58) =< aux(54)
it(70) =< aux(55)
s(41) =< aux(11)
s(42) =< aux(55)
s(37) =< s(38)

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

* Chain [[54,55,56,57,58,68,69,70],87]: 5*it(54)+6*it(56)+3*it(58)+8*it(68)+2*it(70)+1*s(34)+2*s(35)+13*s(37)+2*s(41)+2*s(42)+2*s(51)+2
  Such that:aux(12) =< V1
aux(13) =< V1+1/3
aux(14) =< V1-V+1
aux(17) =< V1/2
aux(18) =< V1/2-V
aux(21) =< 6/5*V1
aux(22) =< 6/5*V1-6/5*V
aux(56) =< V
aux(57) =< V1-V
aux(58) =< V1/2-V/2
s(51) =< aux(56)
aux(11) =< aux(12)
it(54) =< aux(12)
it(56) =< aux(12)
it(58) =< aux(12)
it(68) =< aux(12)
it(70) =< aux(12)
s(34) =< aux(12)
s(36) =< aux(12)
it(58) =< aux(13)
it(68) =< aux(13)
it(70) =< aux(13)
s(38) =< aux(13)
aux(11) =< aux(14)
it(54) =< aux(14)
it(56) =< aux(14)
it(58) =< aux(14)
it(68) =< aux(14)
it(70) =< aux(14)
aux(11) =< aux(57)
it(54) =< aux(57)
it(56) =< aux(57)
it(58) =< aux(57)
it(68) =< aux(57)
it(70) =< aux(57)
s(34) =< aux(57)
s(36) =< aux(57)
s(38) =< aux(57)
it(54) =< aux(17)
it(54) =< aux(18)
it(54) =< aux(58)
it(56) =< aux(58)
it(58) =< aux(58)
it(70) =< aux(21)
s(43) =< aux(21)
it(70) =< aux(22)
s(43) =< aux(22)
s(41) =< aux(11)
s(42) =< s(43)
s(37) =< s(38)
s(35) =< s(36)

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

* Chain [[54,55,56,57,58,68,69,70],86]: 5*it(54)+6*it(56)+3*it(58)+8*it(68)+2*it(70)+1*s(34)+2*s(35)+13*s(37)+2*s(41)+2*s(42)+3*s(53)+3
  Such that:aux(12) =< V1
aux(13) =< V1+1/3
aux(14) =< V1-V+1
aux(17) =< V1/2
aux(18) =< V1/2-V
aux(21) =< 6/5*V1
aux(22) =< 6/5*V1-6/5*V
aux(59) =< V
aux(60) =< V1-V
aux(61) =< V1/2-V/2
s(53) =< aux(59)
aux(11) =< aux(12)
it(54) =< aux(12)
it(56) =< aux(12)
it(58) =< aux(12)
it(68) =< aux(12)
it(70) =< aux(12)
s(34) =< aux(12)
s(36) =< aux(12)
it(58) =< aux(13)
it(68) =< aux(13)
it(70) =< aux(13)
s(38) =< aux(13)
aux(11) =< aux(14)
it(54) =< aux(14)
it(56) =< aux(14)
it(58) =< aux(14)
it(68) =< aux(14)
it(70) =< aux(14)
aux(11) =< aux(60)
it(54) =< aux(60)
it(56) =< aux(60)
it(58) =< aux(60)
it(68) =< aux(60)
it(70) =< aux(60)
s(34) =< aux(60)
s(36) =< aux(60)
s(38) =< aux(60)
it(54) =< aux(17)
it(54) =< aux(18)
it(54) =< aux(61)
it(56) =< aux(61)
it(58) =< aux(61)
it(70) =< aux(21)
s(43) =< aux(21)
it(70) =< aux(22)
s(43) =< aux(22)
s(41) =< aux(11)
s(42) =< s(43)
s(37) =< s(38)
s(35) =< s(36)

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

* Chain [[54,55,56,57,58,68,69,70],85]: 5*it(54)+6*it(56)+11*it(58)+2*it(70)+4*s(34)+13*s(37)+2*s(41)+2*s(42)+3
  Such that:aux(13) =< V1+1/3
aux(14) =< V1-V+1
aux(22) =< 6*V1
aux(17) =< V1/2
aux(18) =< V1/2-V
aux(21) =< 6/5*V1
aux(62) =< V1
s(34) =< aux(62)
aux(11) =< aux(62)
it(54) =< aux(62)
it(56) =< aux(62)
it(58) =< aux(62)
it(70) =< aux(62)
it(58) =< aux(13)
it(70) =< aux(13)
s(38) =< aux(13)
aux(11) =< aux(14)
it(54) =< aux(14)
it(56) =< aux(14)
it(58) =< aux(14)
it(70) =< aux(14)
s(38) =< aux(62)
it(54) =< aux(17)
it(54) =< aux(18)
it(70) =< aux(21)
s(43) =< aux(21)
it(70) =< aux(22)
s(43) =< aux(22)
s(41) =< aux(11)
s(42) =< s(43)
s(37) =< s(38)

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

* Chain [[54,55,56,57,58,68,69,70],84]: 5*it(54)+6*it(56)+11*it(58)+2*it(70)+5*s(34)+13*s(37)+2*s(41)+2*s(42)+2
  Such that:aux(13) =< V1+1/3
aux(14) =< V1-V+1
aux(22) =< 6*V1
aux(17) =< V1/2
aux(18) =< V1/2-V
aux(21) =< 6/5*V1
aux(64) =< V1
s(34) =< aux(64)
aux(11) =< aux(64)
it(54) =< aux(64)
it(56) =< aux(64)
it(58) =< aux(64)
it(70) =< aux(64)
it(58) =< aux(13)
it(70) =< aux(13)
s(38) =< aux(13)
aux(11) =< aux(14)
it(54) =< aux(14)
it(56) =< aux(14)
it(58) =< aux(14)
it(70) =< aux(14)
s(38) =< aux(64)
it(54) =< aux(17)
it(54) =< aux(18)
it(70) =< aux(21)
s(43) =< aux(21)
it(70) =< aux(22)
s(43) =< aux(22)
s(41) =< aux(11)
s(42) =< s(43)
s(37) =< s(38)

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

* Chain [[54,55,56,57,58,68,69,70],83]: 5*it(54)+6*it(56)+3*it(58)+8*it(68)+2*it(70)+1*s(34)+2*s(35)+13*s(37)+2*s(41)+2*s(42)+2*s(59)+2
  Such that:aux(12) =< V1
aux(13) =< V1+1/3
aux(14) =< V1-V+1
aux(17) =< V1/2
aux(21) =< 6/5*V1
aux(22) =< 6/5*V1-12/5*V
aux(65) =< V
aux(66) =< V1-2*V
aux(67) =< V1/2-V
s(59) =< aux(65)
aux(11) =< aux(12)
it(54) =< aux(12)
it(56) =< aux(12)
it(58) =< aux(12)
it(68) =< aux(12)
it(70) =< aux(12)
s(34) =< aux(12)
s(36) =< aux(12)
it(58) =< aux(13)
it(68) =< aux(13)
it(70) =< aux(13)
s(38) =< aux(13)
aux(11) =< aux(14)
it(54) =< aux(14)
it(56) =< aux(14)
it(58) =< aux(14)
it(68) =< aux(14)
it(70) =< aux(14)
aux(11) =< aux(66)
it(54) =< aux(66)
it(56) =< aux(66)
it(58) =< aux(66)
it(68) =< aux(66)
it(70) =< aux(66)
s(34) =< aux(66)
s(36) =< aux(66)
s(38) =< aux(66)
it(54) =< aux(17)
it(54) =< aux(67)
it(56) =< aux(67)
it(58) =< aux(67)
it(70) =< aux(21)
s(43) =< aux(21)
it(70) =< aux(22)
s(43) =< aux(22)
s(41) =< aux(11)
s(42) =< s(43)
s(37) =< s(38)
s(35) =< s(36)

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

* Chain [[54,55,56,57,58,68,69,70],82]: 5*it(54)+6*it(56)+3*it(58)+8*it(68)+2*it(70)+1*s(34)+2*s(35)+13*s(37)+2*s(41)+2*s(42)+2*s(61)+3
  Such that:aux(12) =< V1
aux(13) =< V1+1/3
aux(14) =< V1-V+1
aux(17) =< V1/2
aux(21) =< 6/5*V1
aux(22) =< 6/5*V1-12/5*V
aux(68) =< V
aux(69) =< V1-2*V
aux(70) =< V1/2-V
s(61) =< aux(68)
aux(11) =< aux(12)
it(54) =< aux(12)
it(56) =< aux(12)
it(58) =< aux(12)
it(68) =< aux(12)
it(70) =< aux(12)
s(34) =< aux(12)
s(36) =< aux(12)
it(58) =< aux(13)
it(68) =< aux(13)
it(70) =< aux(13)
s(38) =< aux(13)
aux(11) =< aux(14)
it(54) =< aux(14)
it(56) =< aux(14)
it(58) =< aux(14)
it(68) =< aux(14)
it(70) =< aux(14)
aux(11) =< aux(69)
it(54) =< aux(69)
it(56) =< aux(69)
it(58) =< aux(69)
it(68) =< aux(69)
it(70) =< aux(69)
s(34) =< aux(69)
s(36) =< aux(69)
s(38) =< aux(69)
it(54) =< aux(17)
it(54) =< aux(70)
it(56) =< aux(70)
it(58) =< aux(70)
it(70) =< aux(21)
s(43) =< aux(21)
it(70) =< aux(22)
s(43) =< aux(22)
s(41) =< aux(11)
s(42) =< s(43)
s(37) =< s(38)
s(35) =< s(36)

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

* Chain [[54,55,56,57,58,68,69,70],81]: 5*it(54)+6*it(56)+11*it(58)+2*it(70)+3*s(34)+13*s(37)+2*s(41)+2*s(42)+1*s(63)+2
  Such that:aux(13) =< V1+1/3
aux(14) =< V1-V+1
aux(17) =< V1/2
aux(18) =< V1/2-V
aux(21) =< 6/5*V1
aux(71) =< V1
aux(72) =< 6*V1
s(63) =< aux(72)
aux(11) =< aux(71)
it(54) =< aux(71)
it(56) =< aux(71)
it(58) =< aux(71)
it(70) =< aux(71)
s(34) =< aux(71)
it(58) =< aux(13)
it(70) =< aux(13)
s(38) =< aux(13)
aux(11) =< aux(14)
it(54) =< aux(14)
it(56) =< aux(14)
it(58) =< aux(14)
it(70) =< aux(14)
s(38) =< aux(71)
it(54) =< aux(17)
it(54) =< aux(18)
it(70) =< aux(21)
s(43) =< aux(21)
it(70) =< aux(72)
s(43) =< aux(72)
s(41) =< aux(11)
s(42) =< s(43)
s(37) =< s(38)

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

* Chain [[54,55,56,57,58,68,69,70],80]: 5*it(54)+6*it(56)+3*it(58)+8*it(68)+2*it(70)+1*s(34)+2*s(35)+13*s(37)+2*s(41)+2*s(42)+2*s(64)+2
  Such that:aux(12) =< V1
aux(13) =< V1+1/3
aux(14) =< V1-V+1
aux(17) =< V1/2
aux(18) =< V1/2-V
aux(21) =< 6/5*V1
aux(22) =< 6/5*V1-6/5*V
aux(73) =< V
aux(74) =< V1-V
aux(75) =< V1/2-V/2
s(64) =< aux(73)
aux(11) =< aux(12)
it(54) =< aux(12)
it(56) =< aux(12)
it(58) =< aux(12)
it(68) =< aux(12)
it(70) =< aux(12)
s(34) =< aux(12)
s(36) =< aux(12)
it(58) =< aux(13)
it(68) =< aux(13)
it(70) =< aux(13)
s(38) =< aux(13)
aux(11) =< aux(14)
it(54) =< aux(14)
it(56) =< aux(14)
it(58) =< aux(14)
it(68) =< aux(14)
it(70) =< aux(14)
aux(11) =< aux(74)
it(54) =< aux(74)
it(56) =< aux(74)
it(58) =< aux(74)
it(68) =< aux(74)
it(70) =< aux(74)
s(34) =< aux(74)
s(36) =< aux(74)
s(38) =< aux(74)
it(54) =< aux(17)
it(54) =< aux(18)
it(54) =< aux(75)
it(56) =< aux(75)
it(58) =< aux(75)
it(70) =< aux(21)
s(43) =< aux(21)
it(70) =< aux(22)
s(43) =< aux(22)
s(41) =< aux(11)
s(42) =< s(43)
s(37) =< s(38)
s(35) =< s(36)

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

* Chain [[54,55,56,57,58,68,69,70],79]: 5*it(54)+6*it(56)+3*it(58)+8*it(68)+2*it(70)+1*s(34)+2*s(35)+13*s(37)+2*s(41)+2*s(42)+1*s(66)+3
  Such that:aux(12) =< V1
aux(13) =< V1+1/3
aux(14) =< V1-V+1
aux(17) =< V1/2
aux(18) =< V1/2-V
aux(21) =< 6/5*V1
aux(22) =< 6/5*V1-6/5*V
s(66) =< V
aux(76) =< V1-V
aux(77) =< V1/2-V/2
aux(11) =< aux(12)
it(54) =< aux(12)
it(56) =< aux(12)
it(58) =< aux(12)
it(68) =< aux(12)
it(70) =< aux(12)
s(34) =< aux(12)
s(36) =< aux(12)
it(58) =< aux(13)
it(68) =< aux(13)
it(70) =< aux(13)
s(38) =< aux(13)
aux(11) =< aux(14)
it(54) =< aux(14)
it(56) =< aux(14)
it(58) =< aux(14)
it(68) =< aux(14)
it(70) =< aux(14)
aux(11) =< aux(76)
it(54) =< aux(76)
it(56) =< aux(76)
it(58) =< aux(76)
it(68) =< aux(76)
it(70) =< aux(76)
s(34) =< aux(76)
s(36) =< aux(76)
s(38) =< aux(76)
it(54) =< aux(17)
it(54) =< aux(18)
it(54) =< aux(77)
it(56) =< aux(77)
it(58) =< aux(77)
it(70) =< aux(21)
s(43) =< aux(21)
it(70) =< aux(22)
s(43) =< aux(22)
s(41) =< aux(11)
s(42) =< s(43)
s(37) =< s(38)
s(35) =< s(36)

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

* Chain [[54,55,56,57,58,68,69,70],78]: 5*it(54)+6*it(56)+11*it(58)+2*it(70)+3*s(34)+13*s(37)+2*s(41)+2*s(42)+1*s(67)+3
  Such that:aux(13) =< V1+1/3
aux(14) =< V1-V+1
aux(17) =< V1/2
aux(18) =< V1/2-V
aux(21) =< 6/5*V1
aux(78) =< V1
aux(79) =< 6*V1
s(67) =< aux(79)
aux(11) =< aux(78)
it(54) =< aux(78)
it(56) =< aux(78)
it(58) =< aux(78)
it(70) =< aux(78)
s(34) =< aux(78)
it(58) =< aux(13)
it(70) =< aux(13)
s(38) =< aux(13)
aux(11) =< aux(14)
it(54) =< aux(14)
it(56) =< aux(14)
it(58) =< aux(14)
it(70) =< aux(14)
s(38) =< aux(78)
it(54) =< aux(17)
it(54) =< aux(18)
it(70) =< aux(21)
s(43) =< aux(21)
it(70) =< aux(79)
s(43) =< aux(79)
s(41) =< aux(11)
s(42) =< s(43)
s(37) =< s(38)

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

* Chain [[54,55,56,57,58,68,69,70],77,99]: 5*it(54)+6*it(56)+3*it(58)+8*it(68)+2*it(70)+3*s(34)+13*s(37)+2*s(41)+2*s(42)+3
  Such that:aux(13) =< V1+1/3
aux(14) =< V1-V+1
aux(18) =< V1/2-V
aux(80) =< V1
aux(81) =< V1/2
aux(82) =< 6/5*V1
aux(11) =< aux(80)
it(54) =< aux(80)
it(56) =< aux(80)
it(58) =< aux(80)
it(68) =< aux(80)
it(70) =< aux(80)
s(34) =< aux(80)
it(58) =< aux(13)
it(68) =< aux(13)
it(70) =< aux(13)
s(38) =< aux(13)
aux(11) =< aux(14)
it(54) =< aux(14)
it(56) =< aux(14)
it(58) =< aux(14)
it(68) =< aux(14)
it(70) =< aux(14)
s(38) =< aux(80)
it(54) =< aux(81)
it(54) =< aux(18)
it(56) =< aux(81)
it(58) =< aux(81)
it(70) =< aux(82)
s(41) =< aux(11)
s(42) =< aux(82)
s(37) =< s(38)

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

* Chain [[54,55,56,57,58,68,69,70],76,99]: 5*it(54)+6*it(56)+11*it(58)+2*it(70)+3*s(34)+13*s(37)+2*s(41)+2*s(42)+1*s(68)+1*s(69)+3
  Such that:s(68) =< 1
aux(13) =< V1+1/3
aux(14) =< V1-V+1
aux(17) =< V1/2
aux(18) =< V1/2-V
aux(21) =< 6/5*V1
aux(83) =< V1
aux(84) =< 6*V1
s(69) =< aux(84)
aux(11) =< aux(83)
it(54) =< aux(83)
it(56) =< aux(83)
it(58) =< aux(83)
it(70) =< aux(83)
s(34) =< aux(83)
it(58) =< aux(13)
it(70) =< aux(13)
s(38) =< aux(13)
aux(11) =< aux(14)
it(54) =< aux(14)
it(56) =< aux(14)
it(58) =< aux(14)
it(70) =< aux(14)
s(38) =< aux(83)
it(54) =< aux(17)
it(54) =< aux(18)
it(70) =< aux(21)
s(43) =< aux(21)
it(70) =< aux(84)
s(43) =< aux(84)
s(41) =< aux(11)
s(42) =< s(43)
s(37) =< s(38)

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

* Chain [[54,55,56,57,58,68,69,70],75,99]: 5*it(54)+6*it(56)+3*it(58)+8*it(68)+2*it(70)+3*s(34)+13*s(37)+2*s(41)+2*s(42)+4
  Such that:aux(13) =< V1+1/3
aux(14) =< V1-V+1
aux(18) =< V1/2-V
aux(85) =< V1
aux(86) =< V1/2
aux(87) =< 6/5*V1
aux(11) =< aux(85)
it(54) =< aux(85)
it(56) =< aux(85)
it(58) =< aux(85)
it(68) =< aux(85)
it(70) =< aux(85)
s(34) =< aux(85)
it(58) =< aux(13)
it(68) =< aux(13)
it(70) =< aux(13)
s(38) =< aux(13)
aux(11) =< aux(14)
it(54) =< aux(14)
it(56) =< aux(14)
it(58) =< aux(14)
it(68) =< aux(14)
it(70) =< aux(14)
s(38) =< aux(85)
it(54) =< aux(86)
it(54) =< aux(18)
it(56) =< aux(86)
it(58) =< aux(86)
it(70) =< aux(87)
s(41) =< aux(11)
s(42) =< aux(87)
s(37) =< s(38)

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

* Chain [[54,55,56,57,58,68,69,70],74,99]: 5*it(54)+6*it(56)+3*it(58)+8*it(68)+2*it(70)+3*s(34)+13*s(37)+2*s(41)+2*s(42)+1*s(70)+4
  Such that:s(70) =< 1
aux(13) =< V1+1/3
aux(14) =< V1-V+1
aux(18) =< V1/2-V
aux(88) =< V1
aux(89) =< V1/2
aux(90) =< 6/5*V1
aux(11) =< aux(88)
it(54) =< aux(88)
it(56) =< aux(88)
it(58) =< aux(88)
it(68) =< aux(88)
it(70) =< aux(88)
s(34) =< aux(88)
it(58) =< aux(13)
it(68) =< aux(13)
it(70) =< aux(13)
s(38) =< aux(13)
aux(11) =< aux(14)
it(54) =< aux(14)
it(56) =< aux(14)
it(58) =< aux(14)
it(68) =< aux(14)
it(70) =< aux(14)
s(38) =< aux(88)
it(54) =< aux(89)
it(54) =< aux(18)
it(56) =< aux(89)
it(58) =< aux(89)
it(70) =< aux(90)
s(41) =< aux(11)
s(42) =< aux(90)
s(37) =< s(38)

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

* Chain [[54,55,56,57,58,68,69,70],73,99]: 11*it(54)+3*it(58)+8*it(68)+2*it(70)+5*s(34)+13*s(37)+2*s(42)+3
  Such that:aux(13) =< V1+1/3
aux(91) =< V1
aux(92) =< V1/2
aux(93) =< 6/5*V1
it(54) =< aux(91)
it(58) =< aux(91)
it(68) =< aux(91)
it(70) =< aux(91)
s(34) =< aux(91)
it(58) =< aux(13)
it(68) =< aux(13)
it(70) =< aux(13)
s(38) =< aux(13)
s(38) =< aux(91)
it(54) =< aux(92)
it(58) =< aux(92)
it(70) =< aux(93)
s(42) =< aux(93)
s(37) =< s(38)

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

* Chain [[54,55,56,57,58,68,69,70],72,99]: 5*it(54)+6*it(56)+3*it(58)+8*it(68)+2*it(70)+1*s(34)+2*s(35)+13*s(37)+2*s(41)+2*s(42)+2*s(71)+1*s(73)+4
  Such that:aux(94) =< 1
aux(12) =< V1
aux(13) =< V1+1/3
aux(14) =< V1-V+1
aux(17) =< V1/2
aux(18) =< V1/2-V
aux(21) =< 6/5*V1
aux(22) =< 6/5*V1-6/5*V
s(73) =< V
aux(95) =< V1-V
aux(96) =< V1/2-V/2
s(71) =< aux(94)
aux(11) =< aux(12)
it(54) =< aux(12)
it(56) =< aux(12)
it(58) =< aux(12)
it(68) =< aux(12)
it(70) =< aux(12)
s(34) =< aux(12)
s(36) =< aux(12)
it(58) =< aux(13)
it(68) =< aux(13)
it(70) =< aux(13)
s(38) =< aux(13)
aux(11) =< aux(14)
it(54) =< aux(14)
it(56) =< aux(14)
it(58) =< aux(14)
it(68) =< aux(14)
it(70) =< aux(14)
aux(11) =< aux(95)
it(54) =< aux(95)
it(56) =< aux(95)
it(58) =< aux(95)
it(68) =< aux(95)
it(70) =< aux(95)
s(34) =< aux(95)
s(36) =< aux(95)
s(38) =< aux(95)
it(54) =< aux(17)
it(54) =< aux(18)
it(54) =< aux(96)
it(56) =< aux(96)
it(58) =< aux(96)
it(70) =< aux(21)
s(43) =< aux(21)
it(70) =< aux(22)
s(43) =< aux(22)
s(41) =< aux(11)
s(42) =< s(43)
s(37) =< s(38)
s(35) =< s(36)

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

* Chain [[54,55,56,57,58,68,69,70],71,99]: 11*it(54)+3*it(58)+8*it(68)+2*it(70)+5*s(34)+13*s(37)+2*s(42)+6
  Such that:aux(13) =< V1+1/3
aux(98) =< V1
aux(99) =< V1/2
aux(100) =< 6/5*V1
it(54) =< aux(98)
it(58) =< aux(98)
it(68) =< aux(98)
it(70) =< aux(98)
s(34) =< aux(98)
it(58) =< aux(13)
it(68) =< aux(13)
it(70) =< aux(13)
s(38) =< aux(13)
s(38) =< aux(98)
it(54) =< aux(99)
it(58) =< aux(99)
it(70) =< aux(100)
s(42) =< aux(100)
s(37) =< s(38)

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

* Chain [[54,55,56,57,58,68,69,70],67,99]: 5*it(54)+6*it(56)+3*it(58)+8*it(68)+2*it(70)+1*s(34)+2*s(35)+13*s(37)+2*s(41)+2*s(42)+3
  Such that:aux(12) =< V1
aux(13) =< V1+1/3
aux(14) =< V1-V+1
aux(17) =< V1/2
aux(18) =< V1/2-V
aux(21) =< 6/5*V1
aux(22) =< 6/5*V1-6/5*V
aux(101) =< V1-V
aux(102) =< V1/2-V/2
aux(11) =< aux(12)
it(54) =< aux(12)
it(56) =< aux(12)
it(58) =< aux(12)
it(68) =< aux(12)
it(70) =< aux(12)
s(34) =< aux(12)
s(36) =< aux(12)
it(58) =< aux(13)
it(68) =< aux(13)
it(70) =< aux(13)
s(38) =< aux(13)
aux(11) =< aux(14)
it(54) =< aux(14)
it(56) =< aux(14)
it(58) =< aux(14)
it(68) =< aux(14)
it(70) =< aux(14)
aux(11) =< aux(101)
it(54) =< aux(101)
it(56) =< aux(101)
it(58) =< aux(101)
it(68) =< aux(101)
it(70) =< aux(101)
s(34) =< aux(101)
s(36) =< aux(101)
s(38) =< aux(101)
it(54) =< aux(17)
it(54) =< aux(18)
it(54) =< aux(102)
it(56) =< aux(102)
it(58) =< aux(102)
it(70) =< aux(21)
s(43) =< aux(21)
it(70) =< aux(22)
s(43) =< aux(22)
s(41) =< aux(11)
s(42) =< s(43)
s(37) =< s(38)
s(35) =< s(36)

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

* Chain [[54,55,56,57,58,68,69,70],66,99]: 5*it(54)+6*it(56)+3*it(58)+8*it(68)+2*it(70)+1*s(34)+2*s(35)+13*s(37)+2*s(41)+2*s(42)+8*s(76)+4
  Such that:aux(12) =< V1
aux(13) =< V1+1/3
aux(14) =< V1-V+1
aux(17) =< V1/2
aux(18) =< V1/2-V
aux(21) =< 6/5*V1
aux(22) =< 6/5*V1-6/5*V
aux(103) =< V
aux(104) =< V1-V
aux(105) =< V1/2-V/2
s(76) =< aux(103)
aux(11) =< aux(12)
it(54) =< aux(12)
it(56) =< aux(12)
it(58) =< aux(12)
it(68) =< aux(12)
it(70) =< aux(12)
s(34) =< aux(12)
s(36) =< aux(12)
it(58) =< aux(13)
it(68) =< aux(13)
it(70) =< aux(13)
s(38) =< aux(13)
aux(11) =< aux(14)
it(54) =< aux(14)
it(56) =< aux(14)
it(58) =< aux(14)
it(68) =< aux(14)
it(70) =< aux(14)
aux(11) =< aux(104)
it(54) =< aux(104)
it(56) =< aux(104)
it(58) =< aux(104)
it(68) =< aux(104)
it(70) =< aux(104)
s(34) =< aux(104)
s(36) =< aux(104)
s(38) =< aux(104)
it(54) =< aux(17)
it(54) =< aux(18)
it(54) =< aux(105)
it(56) =< aux(105)
it(58) =< aux(105)
it(70) =< aux(21)
s(43) =< aux(21)
it(70) =< aux(22)
s(43) =< aux(22)
s(41) =< aux(11)
s(42) =< s(43)
s(37) =< s(38)
s(35) =< s(36)

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

* Chain [[54,55,56,57,58,68,69,70],65,99]: 5*it(54)+6*it(56)+3*it(58)+8*it(68)+2*it(70)+1*s(34)+2*s(35)+13*s(37)+2*s(41)+2*s(42)+5*s(84)+4
  Such that:aux(12) =< V1
aux(13) =< V1+1/3
aux(14) =< V1-V+1
aux(17) =< V1/2
aux(18) =< V1/2-V
aux(21) =< 6/5*V1
aux(22) =< 6/5*V1-6/5*V
aux(106) =< V
aux(107) =< V1-V
aux(108) =< V1/2-V/2
s(84) =< aux(106)
aux(11) =< aux(12)
it(54) =< aux(12)
it(56) =< aux(12)
it(58) =< aux(12)
it(68) =< aux(12)
it(70) =< aux(12)
s(34) =< aux(12)
s(36) =< aux(12)
it(58) =< aux(13)
it(68) =< aux(13)
it(70) =< aux(13)
s(38) =< aux(13)
aux(11) =< aux(14)
it(54) =< aux(14)
it(56) =< aux(14)
it(58) =< aux(14)
it(68) =< aux(14)
it(70) =< aux(14)
aux(11) =< aux(107)
it(54) =< aux(107)
it(56) =< aux(107)
it(58) =< aux(107)
it(68) =< aux(107)
it(70) =< aux(107)
s(34) =< aux(107)
s(36) =< aux(107)
s(38) =< aux(107)
it(54) =< aux(17)
it(54) =< aux(18)
it(54) =< aux(108)
it(56) =< aux(108)
it(58) =< aux(108)
it(70) =< aux(21)
s(43) =< aux(21)
it(70) =< aux(22)
s(43) =< aux(22)
s(41) =< aux(11)
s(42) =< s(43)
s(37) =< s(38)
s(35) =< s(36)

  with precondition: [V>=2,Out>=4,V1>=2*V,2*V1+4>=2*V+Out] 

* Chain [[54,55,56,57,58,68,69,70],64,99]: 5*it(54)+6*it(56)+3*it(58)+8*it(68)+2*it(70)+1*s(34)+2*s(35)+13*s(37)+2*s(41)+2*s(42)+4
  Such that:aux(12) =< V1
aux(13) =< V1+1/3
aux(14) =< V1-V+1
aux(17) =< V1/2
aux(18) =< V1/2-V
aux(21) =< 6/5*V1
aux(22) =< 6/5*V1-6/5*V
aux(109) =< V1-V
aux(110) =< V1/2-V/2
aux(11) =< aux(12)
it(54) =< aux(12)
it(56) =< aux(12)
it(58) =< aux(12)
it(68) =< aux(12)
it(70) =< aux(12)
s(34) =< aux(12)
s(36) =< aux(12)
it(58) =< aux(13)
it(68) =< aux(13)
it(70) =< aux(13)
s(38) =< aux(13)
aux(11) =< aux(14)
it(54) =< aux(14)
it(56) =< aux(14)
it(58) =< aux(14)
it(68) =< aux(14)
it(70) =< aux(14)
aux(11) =< aux(109)
it(54) =< aux(109)
it(56) =< aux(109)
it(58) =< aux(109)
it(68) =< aux(109)
it(70) =< aux(109)
s(34) =< aux(109)
s(36) =< aux(109)
s(38) =< aux(109)
it(54) =< aux(17)
it(54) =< aux(18)
it(54) =< aux(110)
it(56) =< aux(110)
it(58) =< aux(110)
it(70) =< aux(21)
s(43) =< aux(21)
it(70) =< aux(22)
s(43) =< aux(22)
s(41) =< aux(11)
s(42) =< s(43)
s(37) =< s(38)
s(35) =< s(36)

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

* Chain [[54,55,56,57,58,68,69,70],63,99]: 5*it(54)+6*it(56)+11*it(58)+2*it(70)+3*s(34)+13*s(37)+2*s(41)+2*s(42)+1*s(89)+4
  Such that:aux(13) =< V1+1/3
aux(14) =< V1-V+1
aux(17) =< V1/2
aux(18) =< V1/2-V
aux(21) =< 6/5*V1
aux(111) =< V1
aux(112) =< 6*V1
s(89) =< aux(112)
aux(11) =< aux(111)
it(54) =< aux(111)
it(56) =< aux(111)
it(58) =< aux(111)
it(70) =< aux(111)
s(34) =< aux(111)
it(58) =< aux(13)
it(70) =< aux(13)
s(38) =< aux(13)
aux(11) =< aux(14)
it(54) =< aux(14)
it(56) =< aux(14)
it(58) =< aux(14)
it(70) =< aux(14)
s(38) =< aux(111)
it(54) =< aux(17)
it(54) =< aux(18)
it(70) =< aux(21)
s(43) =< aux(21)
it(70) =< aux(112)
s(43) =< aux(112)
s(41) =< aux(11)
s(42) =< s(43)
s(37) =< s(38)

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

* Chain [[54,55,56,57,58,68,69,70],62,99]: 5*it(54)+6*it(56)+11*it(58)+2*it(70)+3*s(34)+13*s(37)+2*s(41)+2*s(42)+1*s(90)+4
  Such that:aux(13) =< V1+1/3
aux(14) =< V1-V+1
aux(17) =< V1/2
aux(18) =< V1/2-V
aux(21) =< 6/5*V1
aux(113) =< V1
aux(114) =< 6*V1
s(90) =< aux(114)
aux(11) =< aux(113)
it(54) =< aux(113)
it(56) =< aux(113)
it(58) =< aux(113)
it(70) =< aux(113)
s(34) =< aux(113)
it(58) =< aux(13)
it(70) =< aux(13)
s(38) =< aux(13)
aux(11) =< aux(14)
it(54) =< aux(14)
it(56) =< aux(14)
it(58) =< aux(14)
it(70) =< aux(14)
s(38) =< aux(113)
it(54) =< aux(17)
it(54) =< aux(18)
it(70) =< aux(21)
s(43) =< aux(21)
it(70) =< aux(114)
s(43) =< aux(114)
s(41) =< aux(11)
s(42) =< s(43)
s(37) =< s(38)

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

* Chain [[54,55,56,57,58,68,69,70],61,99]: 5*it(54)+6*it(56)+3*it(58)+8*it(68)+2*it(70)+1*s(34)+2*s(35)+13*s(37)+2*s(41)+2*s(42)+2*s(91)+3
  Such that:aux(12) =< V1
aux(13) =< V1+1/3
aux(14) =< V1-V+1
aux(17) =< V1/2
aux(21) =< 6/5*V1
aux(22) =< 6/5*V1-12/5*V
aux(115) =< V
aux(116) =< V1-2*V
aux(117) =< V1/2-V
s(91) =< aux(115)
aux(11) =< aux(12)
it(54) =< aux(12)
it(56) =< aux(12)
it(58) =< aux(12)
it(68) =< aux(12)
it(70) =< aux(12)
s(34) =< aux(12)
s(36) =< aux(12)
it(58) =< aux(13)
it(68) =< aux(13)
it(70) =< aux(13)
s(38) =< aux(13)
aux(11) =< aux(14)
it(54) =< aux(14)
it(56) =< aux(14)
it(58) =< aux(14)
it(68) =< aux(14)
it(70) =< aux(14)
aux(11) =< aux(116)
it(54) =< aux(116)
it(56) =< aux(116)
it(58) =< aux(116)
it(68) =< aux(116)
it(70) =< aux(116)
s(34) =< aux(116)
s(36) =< aux(116)
s(38) =< aux(116)
it(54) =< aux(17)
it(54) =< aux(117)
it(56) =< aux(117)
it(58) =< aux(117)
it(70) =< aux(21)
s(43) =< aux(21)
it(70) =< aux(22)
s(43) =< aux(22)
s(41) =< aux(11)
s(42) =< s(43)
s(37) =< s(38)
s(35) =< s(36)

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

* Chain [[54,55,56,57,58,68,69,70],60,99]: 5*it(54)+6*it(56)+3*it(58)+8*it(68)+2*it(70)+1*s(34)+2*s(35)+13*s(37)+2*s(41)+2*s(42)+1*s(93)+4
  Such that:aux(12) =< V1
aux(13) =< V1+1/3
aux(14) =< V1-V+1
aux(17) =< V1/2
aux(21) =< 6/5*V1
aux(22) =< 6/5*V1-12/5*V
s(93) =< V
aux(118) =< V1-2*V
aux(119) =< V1/2-V
aux(11) =< aux(12)
it(54) =< aux(12)
it(56) =< aux(12)
it(58) =< aux(12)
it(68) =< aux(12)
it(70) =< aux(12)
s(34) =< aux(12)
s(36) =< aux(12)
it(58) =< aux(13)
it(68) =< aux(13)
it(70) =< aux(13)
s(38) =< aux(13)
aux(11) =< aux(14)
it(54) =< aux(14)
it(56) =< aux(14)
it(58) =< aux(14)
it(68) =< aux(14)
it(70) =< aux(14)
aux(11) =< aux(118)
it(54) =< aux(118)
it(56) =< aux(118)
it(58) =< aux(118)
it(68) =< aux(118)
it(70) =< aux(118)
s(34) =< aux(118)
s(36) =< aux(118)
s(38) =< aux(118)
it(54) =< aux(17)
it(54) =< aux(119)
it(56) =< aux(119)
it(58) =< aux(119)
it(70) =< aux(21)
s(43) =< aux(21)
it(70) =< aux(22)
s(43) =< aux(22)
s(41) =< aux(11)
s(42) =< s(43)
s(37) =< s(38)
s(35) =< s(36)

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

* Chain [[54,55,56,57,58,68,69,70],59,99]: 5*it(54)+6*it(56)+3*it(58)+8*it(68)+2*it(70)+1*s(34)+2*s(35)+13*s(37)+2*s(41)+2*s(42)+3
  Such that:aux(12) =< V1
aux(13) =< V1+1/3
aux(14) =< V1-V+1
aux(17) =< V1/2
aux(18) =< V1/2-V
aux(21) =< 6/5*V1
aux(22) =< 6/5*V1-6/5*V
aux(120) =< V1-V
aux(121) =< V1/2-V/2
aux(11) =< aux(12)
it(54) =< aux(12)
it(56) =< aux(12)
it(58) =< aux(12)
it(68) =< aux(12)
it(70) =< aux(12)
s(34) =< aux(12)
s(36) =< aux(12)
it(58) =< aux(13)
it(68) =< aux(13)
it(70) =< aux(13)
s(38) =< aux(13)
aux(11) =< aux(14)
it(54) =< aux(14)
it(56) =< aux(14)
it(58) =< aux(14)
it(68) =< aux(14)
it(70) =< aux(14)
aux(11) =< aux(120)
it(54) =< aux(120)
it(56) =< aux(120)
it(58) =< aux(120)
it(68) =< aux(120)
it(70) =< aux(120)
s(34) =< aux(120)
s(36) =< aux(120)
s(38) =< aux(120)
it(54) =< aux(17)
it(54) =< aux(18)
it(54) =< aux(121)
it(56) =< aux(121)
it(58) =< aux(121)
it(70) =< aux(21)
s(43) =< aux(21)
it(70) =< aux(22)
s(43) =< aux(22)
s(41) =< aux(11)
s(42) =< s(43)
s(37) =< s(38)
s(35) =< s(36)

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

* Chain [[54,55,56,57,58,68,69,70],59,98]: 5*it(54)+6*it(56)+3*it(58)+8*it(68)+2*it(70)+1*s(34)+2*s(35)+13*s(37)+2*s(41)+2*s(42)+4
  Such that:aux(12) =< V1
aux(13) =< V1+1/3
aux(14) =< V1-V+1
aux(17) =< V1/2
aux(18) =< V1/2-V
aux(21) =< 6/5*V1
aux(22) =< 6/5*V1-6/5*V
aux(122) =< V1-V
aux(123) =< V1/2-V/2
aux(11) =< aux(12)
it(54) =< aux(12)
it(56) =< aux(12)
it(58) =< aux(12)
it(68) =< aux(12)
it(70) =< aux(12)
s(34) =< aux(12)
s(36) =< aux(12)
it(58) =< aux(13)
it(68) =< aux(13)
it(70) =< aux(13)
s(38) =< aux(13)
aux(11) =< aux(14)
it(54) =< aux(14)
it(56) =< aux(14)
it(58) =< aux(14)
it(68) =< aux(14)
it(70) =< aux(14)
aux(11) =< aux(122)
it(54) =< aux(122)
it(56) =< aux(122)
it(58) =< aux(122)
it(68) =< aux(122)
it(70) =< aux(122)
s(34) =< aux(122)
s(36) =< aux(122)
s(38) =< aux(122)
it(54) =< aux(17)
it(54) =< aux(18)
it(54) =< aux(123)
it(56) =< aux(123)
it(58) =< aux(123)
it(70) =< aux(21)
s(43) =< aux(21)
it(70) =< aux(22)
s(43) =< aux(22)
s(41) =< aux(11)
s(42) =< s(43)
s(37) =< s(38)
s(35) =< s(36)

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

* Chain [[54,55,56,57,58,68,69,70],59,97]: 5*it(54)+6*it(56)+3*it(58)+8*it(68)+2*it(70)+1*s(34)+2*s(35)+13*s(37)+2*s(41)+2*s(42)+4
  Such that:aux(12) =< V1
aux(13) =< V1+1/3
aux(14) =< V1-V+1
aux(17) =< V1/2
aux(18) =< V1/2-V
aux(21) =< 6/5*V1
aux(22) =< 6/5*V1-6/5*V
aux(124) =< V1-V
aux(125) =< V1/2-V/2
aux(11) =< aux(12)
it(54) =< aux(12)
it(56) =< aux(12)
it(58) =< aux(12)
it(68) =< aux(12)
it(70) =< aux(12)
s(34) =< aux(12)
s(36) =< aux(12)
it(58) =< aux(13)
it(68) =< aux(13)
it(70) =< aux(13)
s(38) =< aux(13)
aux(11) =< aux(14)
it(54) =< aux(14)
it(56) =< aux(14)
it(58) =< aux(14)
it(68) =< aux(14)
it(70) =< aux(14)
aux(11) =< aux(124)
it(54) =< aux(124)
it(56) =< aux(124)
it(58) =< aux(124)
it(68) =< aux(124)
it(70) =< aux(124)
s(34) =< aux(124)
s(36) =< aux(124)
s(38) =< aux(124)
it(54) =< aux(17)
it(54) =< aux(18)
it(54) =< aux(125)
it(56) =< aux(125)
it(58) =< aux(125)
it(70) =< aux(21)
s(43) =< aux(21)
it(70) =< aux(22)
s(43) =< aux(22)
s(41) =< aux(11)
s(42) =< s(43)
s(37) =< s(38)
s(35) =< s(36)

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

* Chain [[54,55,56,57,58,68,69,70],59,96]: 5*it(54)+6*it(56)+3*it(58)+8*it(68)+2*it(70)+1*s(34)+2*s(35)+13*s(37)+2*s(41)+2*s(42)+5
  Such that:aux(12) =< V1
aux(13) =< V1+1/3
aux(14) =< V1-V+1
aux(17) =< V1/2
aux(18) =< V1/2-V
aux(21) =< 6/5*V1
aux(22) =< 6/5*V1-6/5*V
aux(126) =< V1-V
aux(127) =< V1/2-V/2
aux(11) =< aux(12)
it(54) =< aux(12)
it(56) =< aux(12)
it(58) =< aux(12)
it(68) =< aux(12)
it(70) =< aux(12)
s(34) =< aux(12)
s(36) =< aux(12)
it(58) =< aux(13)
it(68) =< aux(13)
it(70) =< aux(13)
s(38) =< aux(13)
aux(11) =< aux(14)
it(54) =< aux(14)
it(56) =< aux(14)
it(58) =< aux(14)
it(68) =< aux(14)
it(70) =< aux(14)
aux(11) =< aux(126)
it(54) =< aux(126)
it(56) =< aux(126)
it(58) =< aux(126)
it(68) =< aux(126)
it(70) =< aux(126)
s(34) =< aux(126)
s(36) =< aux(126)
s(38) =< aux(126)
it(54) =< aux(17)
it(54) =< aux(18)
it(54) =< aux(127)
it(56) =< aux(127)
it(58) =< aux(127)
it(70) =< aux(21)
s(43) =< aux(21)
it(70) =< aux(22)
s(43) =< aux(22)
s(41) =< aux(11)
s(42) =< s(43)
s(37) =< s(38)
s(35) =< s(36)

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

* Chain [[54,55,56,57,58,68,69,70],59,95]: 5*it(54)+6*it(56)+3*it(58)+8*it(68)+2*it(70)+1*s(34)+2*s(35)+13*s(37)+2*s(41)+2*s(42)+5
  Such that:aux(12) =< V1
aux(13) =< V1+1/3
aux(14) =< V1-V+1
aux(17) =< V1/2
aux(18) =< V1/2-V
aux(21) =< 6/5*V1
aux(22) =< 6/5*V1-6/5*V
aux(128) =< V1-V
aux(129) =< V1/2-V/2
aux(11) =< aux(12)
it(54) =< aux(12)
it(56) =< aux(12)
it(58) =< aux(12)
it(68) =< aux(12)
it(70) =< aux(12)
s(34) =< aux(12)
s(36) =< aux(12)
it(58) =< aux(13)
it(68) =< aux(13)
it(70) =< aux(13)
s(38) =< aux(13)
aux(11) =< aux(14)
it(54) =< aux(14)
it(56) =< aux(14)
it(58) =< aux(14)
it(68) =< aux(14)
it(70) =< aux(14)
aux(11) =< aux(128)
it(54) =< aux(128)
it(56) =< aux(128)
it(58) =< aux(128)
it(68) =< aux(128)
it(70) =< aux(128)
s(34) =< aux(128)
s(36) =< aux(128)
s(38) =< aux(128)
it(54) =< aux(17)
it(54) =< aux(18)
it(54) =< aux(129)
it(56) =< aux(129)
it(58) =< aux(129)
it(70) =< aux(21)
s(43) =< aux(21)
it(70) =< aux(22)
s(43) =< aux(22)
s(41) =< aux(11)
s(42) =< s(43)
s(37) =< s(38)
s(35) =< s(36)

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

* Chain [[54,55,56,57,58,68,69,70],59,77,99]: 5*it(54)+6*it(56)+3*it(58)+8*it(68)+2*it(70)+1*s(34)+2*s(35)+13*s(37)+2*s(41)+2*s(42)+5
  Such that:aux(12) =< V1
aux(13) =< V1+1/3
aux(14) =< V1-V+1
aux(17) =< V1/2
aux(18) =< V1/2-V
aux(21) =< 6/5*V1
aux(22) =< 6/5*V1-6/5*V
aux(130) =< V1-V
aux(131) =< V1/2-V/2
aux(11) =< aux(12)
it(54) =< aux(12)
it(56) =< aux(12)
it(58) =< aux(12)
it(68) =< aux(12)
it(70) =< aux(12)
s(34) =< aux(12)
s(36) =< aux(12)
it(58) =< aux(13)
it(68) =< aux(13)
it(70) =< aux(13)
s(38) =< aux(13)
aux(11) =< aux(14)
it(54) =< aux(14)
it(56) =< aux(14)
it(58) =< aux(14)
it(68) =< aux(14)
it(70) =< aux(14)
aux(11) =< aux(130)
it(54) =< aux(130)
it(56) =< aux(130)
it(58) =< aux(130)
it(68) =< aux(130)
it(70) =< aux(130)
s(34) =< aux(130)
s(36) =< aux(130)
s(38) =< aux(130)
it(54) =< aux(17)
it(54) =< aux(18)
it(54) =< aux(131)
it(56) =< aux(131)
it(58) =< aux(131)
it(70) =< aux(21)
s(43) =< aux(21)
it(70) =< aux(22)
s(43) =< aux(22)
s(41) =< aux(11)
s(42) =< s(43)
s(37) =< s(38)
s(35) =< s(36)

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

* Chain [[54,55,56,57,58,68,69,70],59,76,99]: 5*it(54)+6*it(56)+3*it(58)+8*it(68)+2*it(70)+1*s(34)+2*s(35)+13*s(37)+2*s(41)+2*s(42)+2*s(68)+5
  Such that:aux(132) =< 1
aux(12) =< V1
aux(13) =< V1+1/3
aux(14) =< V1-V+1
aux(17) =< V1/2
aux(18) =< V1/2-V
aux(21) =< 6/5*V1
aux(22) =< 6/5*V1-6/5*V
aux(133) =< V1-V
aux(134) =< V1/2-V/2
s(68) =< aux(132)
aux(11) =< aux(12)
it(54) =< aux(12)
it(56) =< aux(12)
it(58) =< aux(12)
it(68) =< aux(12)
it(70) =< aux(12)
s(34) =< aux(12)
s(36) =< aux(12)
it(58) =< aux(13)
it(68) =< aux(13)
it(70) =< aux(13)
s(38) =< aux(13)
aux(11) =< aux(14)
it(54) =< aux(14)
it(56) =< aux(14)
it(58) =< aux(14)
it(68) =< aux(14)
it(70) =< aux(14)
aux(11) =< aux(133)
it(54) =< aux(133)
it(56) =< aux(133)
it(58) =< aux(133)
it(68) =< aux(133)
it(70) =< aux(133)
s(34) =< aux(133)
s(36) =< aux(133)
s(38) =< aux(133)
it(54) =< aux(17)
it(54) =< aux(18)
it(54) =< aux(134)
it(56) =< aux(134)
it(58) =< aux(134)
it(70) =< aux(21)
s(43) =< aux(21)
it(70) =< aux(22)
s(43) =< aux(22)
s(41) =< aux(11)
s(42) =< s(43)
s(37) =< s(38)
s(35) =< s(36)

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

* Chain [[54,55,56,57,58,68,69,70],59,75,99]: 5*it(54)+6*it(56)+3*it(58)+8*it(68)+2*it(70)+1*s(34)+2*s(35)+13*s(37)+2*s(41)+2*s(42)+6
  Such that:aux(12) =< V1
aux(13) =< V1+1/3
aux(14) =< V1-V+1
aux(17) =< V1/2
aux(18) =< V1/2-V
aux(21) =< 6/5*V1
aux(22) =< 6/5*V1-6/5*V
aux(135) =< V1-V
aux(136) =< V1/2-V/2
aux(11) =< aux(12)
it(54) =< aux(12)
it(56) =< aux(12)
it(58) =< aux(12)
it(68) =< aux(12)
it(70) =< aux(12)
s(34) =< aux(12)
s(36) =< aux(12)
it(58) =< aux(13)
it(68) =< aux(13)
it(70) =< aux(13)
s(38) =< aux(13)
aux(11) =< aux(14)
it(54) =< aux(14)
it(56) =< aux(14)
it(58) =< aux(14)
it(68) =< aux(14)
it(70) =< aux(14)
aux(11) =< aux(135)
it(54) =< aux(135)
it(56) =< aux(135)
it(58) =< aux(135)
it(68) =< aux(135)
it(70) =< aux(135)
s(34) =< aux(135)
s(36) =< aux(135)
s(38) =< aux(135)
it(54) =< aux(17)
it(54) =< aux(18)
it(54) =< aux(136)
it(56) =< aux(136)
it(58) =< aux(136)
it(70) =< aux(21)
s(43) =< aux(21)
it(70) =< aux(22)
s(43) =< aux(22)
s(41) =< aux(11)
s(42) =< s(43)
s(37) =< s(38)
s(35) =< s(36)

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

* Chain [[54,55,56,57,58,68,69,70],59,74,99]: 5*it(54)+6*it(56)+3*it(58)+8*it(68)+2*it(70)+1*s(34)+2*s(35)+13*s(37)+2*s(41)+2*s(42)+1*s(70)+6
  Such that:s(70) =< 1
aux(12) =< V1
aux(13) =< V1+1/3
aux(14) =< V1-V+1
aux(17) =< V1/2
aux(18) =< V1/2-V
aux(21) =< 6/5*V1
aux(22) =< 6/5*V1-6/5*V
aux(137) =< V1-V
aux(138) =< V1/2-V/2
aux(11) =< aux(12)
it(54) =< aux(12)
it(56) =< aux(12)
it(58) =< aux(12)
it(68) =< aux(12)
it(70) =< aux(12)
s(34) =< aux(12)
s(36) =< aux(12)
it(58) =< aux(13)
it(68) =< aux(13)
it(70) =< aux(13)
s(38) =< aux(13)
aux(11) =< aux(14)
it(54) =< aux(14)
it(56) =< aux(14)
it(58) =< aux(14)
it(68) =< aux(14)
it(70) =< aux(14)
aux(11) =< aux(137)
it(54) =< aux(137)
it(56) =< aux(137)
it(58) =< aux(137)
it(68) =< aux(137)
it(70) =< aux(137)
s(34) =< aux(137)
s(36) =< aux(137)
s(38) =< aux(137)
it(54) =< aux(17)
it(54) =< aux(18)
it(54) =< aux(138)
it(56) =< aux(138)
it(58) =< aux(138)
it(70) =< aux(21)
s(43) =< aux(21)
it(70) =< aux(22)
s(43) =< aux(22)
s(41) =< aux(11)
s(42) =< s(43)
s(37) =< s(38)
s(35) =< s(36)

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

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

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

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

* Chain [96]: 3
  with precondition: [V1=1,Out=3,V>=2] 

* Chain [95]: 3
  with precondition: [V1=1,Out=4,V>=2] 

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

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

* Chain [92]: 3
  with precondition: [V=1,Out=2,V1>=1] 

* Chain [91]: 2
  with precondition: [Out=1,V+1=V1,V>=2] 

* Chain [90]: 4*s(45)+3
  Such that:aux(46) =< V
s(45) =< aux(46)

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

* Chain [89]: 2*s(49)+3
  Such that:aux(50) =< V
s(49) =< aux(50)

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

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

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

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

* Chain [86]: 3*s(53)+3
  Such that:aux(59) =< V
s(53) =< aux(59)

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

* Chain [85]: 1*s(56)+3
  Such that:s(56) =< V1

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

* Chain [84]: 2*s(57)+2
  Such that:aux(63) =< V1
s(57) =< aux(63)

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

* Chain [83]: 2*s(59)+2
  Such that:aux(65) =< V
s(59) =< aux(65)

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

* Chain [82]: 2*s(61)+3
  Such that:aux(68) =< V
s(61) =< aux(68)

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

* Chain [81]: 1*s(63)+2
  Such that:s(63) =< V1

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

* Chain [80]: 2*s(64)+2
  Such that:aux(73) =< V
s(64) =< aux(73)

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

* Chain [79]: 1*s(66)+3
  Such that:s(66) =< V

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

* Chain [78]: 1*s(67)+3
  Such that:s(67) =< V1

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

* Chain [77,99]: 3
  with precondition: [Out=1,V1>=1,V>=1] 

* Chain [76,99]: 1*s(68)+1*s(69)+3
  Such that:s(68) =< 1
s(69) =< V1

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

* Chain [75,99]: 4
  with precondition: [V1=1,Out=3,V>=2] 

* Chain [74,99]: 1*s(70)+4
  Such that:s(70) =< 1

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

* Chain [73,99]: 3
  with precondition: [V=1,Out=1,V1>=1] 

* Chain [72,99]: 2*s(71)+1*s(73)+4
  Such that:aux(94) =< 1
s(73) =< V
s(71) =< aux(94)

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

* Chain [71,99]: 6
  with precondition: [V=1,Out=3,V1>=1] 

* Chain [67,99]: 3
  with precondition: [Out=1,V1=V+1,V1>=3] 

* Chain [66,99]: 8*s(76)+4
  Such that:aux(103) =< V
s(76) =< aux(103)

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

* Chain [65,99]: 5*s(84)+4
  Such that:aux(106) =< V
s(84) =< aux(106)

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

* Chain [64,99]: 4
  with precondition: [Out=2,V>=2,V1>=V] 

* Chain [63,99]: 1*s(89)+4
  Such that:s(89) =< V1

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

* Chain [62,99]: 1*s(90)+4
  Such that:s(90) =< V1

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

* Chain [61,99]: 2*s(91)+3
  Such that:aux(115) =< V
s(91) =< aux(115)

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

* Chain [60,99]: 1*s(93)+4
  Such that:s(93) =< V

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

* Chain [59,99]: 3
  with precondition: [Out=1,V1=V+1,V1>=3] 

* Chain [59,98]: 4
  with precondition: [Out=2,V1=V+1,V1>=3] 

* Chain [59,97]: 4
  with precondition: [Out=3,V1=V+1,V1>=3] 

* Chain [59,96]: 5
  with precondition: [Out=4,V1=V+1,V1>=3] 

* Chain [59,95]: 5
  with precondition: [Out=5,V1=V+1,V1>=3] 

* Chain [59,77,99]: 5
  with precondition: [Out=2,V1=V+1,V1>=3] 

* Chain [59,76,99]: 2*s(68)+5
  Such that:aux(132) =< 1
s(68) =< aux(132)

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

* Chain [59,75,99]: 6
  with precondition: [Out=4,V1=V+1,V1>=3] 

* Chain [59,74,99]: 1*s(70)+6
  Such that:s(70) =< 1

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


#### Cost of chains of start(V1,V,V7):
* Chain [106]: 1*s(1030)+70*s(1031)+11*s(1033)+62*s(1034)+95*s(1054)+114*s(1055)+57*s(1056)+152*s(1057)+38*s(1058)+19*s(1059)+38*s(1063)+38*s(1064)+247*s(1065)+38*s(1066)+5*s(1067)+85*s(1069)+42*s(1070)+157*s(1071)+14*s(1072)+34*s(1076)+14*s(1077)+221*s(1078)+25*s(1080)+30*s(1081)+15*s(1082)+40*s(1083)+10*s(1084)+5*s(1085)+10*s(1089)+10*s(1090)+65*s(1091)+10*s(1092)+60*s(1093)+30*s(1094)+20*s(1095)+20*s(1096)+6
  Such that:s(1040) =< V1-2*V
s(1041) =< V1-V
s(1043) =< 6*V1
s(1046) =< V1/2-V/2
s(1048) =< 6/5*V1-12/5*V
s(1049) =< 6/5*V1-6/5*V
s(1030) =< V+1
aux(167) =< 1
aux(168) =< V1
aux(169) =< V1+1/3
aux(170) =< V1-V+1
aux(171) =< V1/2
aux(172) =< V1/2-V
aux(173) =< 6/5*V1
aux(174) =< V
s(1033) =< aux(167)
s(1034) =< aux(168)
s(1031) =< aux(174)
s(1053) =< aux(168)
s(1054) =< aux(168)
s(1055) =< aux(168)
s(1056) =< aux(168)
s(1057) =< aux(168)
s(1058) =< aux(168)
s(1059) =< aux(168)
s(1060) =< aux(168)
s(1056) =< aux(169)
s(1057) =< aux(169)
s(1058) =< aux(169)
s(1061) =< aux(169)
s(1053) =< aux(170)
s(1054) =< aux(170)
s(1055) =< aux(170)
s(1056) =< aux(170)
s(1057) =< aux(170)
s(1058) =< aux(170)
s(1053) =< s(1041)
s(1054) =< s(1041)
s(1055) =< s(1041)
s(1056) =< s(1041)
s(1057) =< s(1041)
s(1058) =< s(1041)
s(1059) =< s(1041)
s(1060) =< s(1041)
s(1061) =< s(1041)
s(1054) =< aux(171)
s(1054) =< aux(172)
s(1054) =< s(1046)
s(1055) =< s(1046)
s(1056) =< s(1046)
s(1058) =< aux(173)
s(1062) =< aux(173)
s(1058) =< s(1049)
s(1062) =< s(1049)
s(1063) =< s(1053)
s(1064) =< s(1062)
s(1065) =< s(1061)
s(1066) =< s(1060)
s(1067) =< s(1043)
s(1068) =< aux(168)
s(1069) =< aux(168)
s(1070) =< aux(168)
s(1071) =< aux(168)
s(1072) =< aux(168)
s(1071) =< aux(169)
s(1072) =< aux(169)
s(1074) =< aux(169)
s(1068) =< aux(170)
s(1069) =< aux(170)
s(1070) =< aux(170)
s(1071) =< aux(170)
s(1072) =< aux(170)
s(1074) =< aux(168)
s(1069) =< aux(171)
s(1069) =< aux(172)
s(1072) =< aux(173)
s(1075) =< aux(173)
s(1072) =< s(1043)
s(1075) =< s(1043)
s(1076) =< s(1068)
s(1077) =< s(1075)
s(1078) =< s(1074)
s(1079) =< aux(168)
s(1080) =< aux(168)
s(1081) =< aux(168)
s(1082) =< aux(168)
s(1083) =< aux(168)
s(1084) =< aux(168)
s(1085) =< aux(168)
s(1086) =< aux(168)
s(1082) =< aux(169)
s(1083) =< aux(169)
s(1084) =< aux(169)
s(1087) =< aux(169)
s(1079) =< aux(170)
s(1080) =< aux(170)
s(1081) =< aux(170)
s(1082) =< aux(170)
s(1083) =< aux(170)
s(1084) =< aux(170)
s(1079) =< s(1040)
s(1080) =< s(1040)
s(1081) =< s(1040)
s(1082) =< s(1040)
s(1083) =< s(1040)
s(1084) =< s(1040)
s(1085) =< s(1040)
s(1086) =< s(1040)
s(1087) =< s(1040)
s(1080) =< aux(171)
s(1080) =< aux(172)
s(1081) =< aux(172)
s(1082) =< aux(172)
s(1084) =< aux(173)
s(1088) =< aux(173)
s(1084) =< s(1048)
s(1088) =< s(1048)
s(1089) =< s(1079)
s(1090) =< s(1088)
s(1091) =< s(1087)
s(1092) =< s(1086)
s(1093) =< aux(168)
s(1094) =< aux(168)
s(1095) =< aux(168)
s(1094) =< aux(169)
s(1095) =< aux(169)
s(1093) =< aux(170)
s(1094) =< aux(170)
s(1095) =< aux(170)
s(1093) =< aux(171)
s(1094) =< aux(171)
s(1095) =< aux(173)
s(1096) =< aux(173)

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

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

* Chain [104]: 5
  with precondition: [V1=1,V>=2] 

* Chain [103]: 1
  with precondition: [V1=2,V>=0,V7>=0] 

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

* Chain [101]: 44*s(1126)+12*s(1127)+32*s(1128)+8*s(1129)+20*s(1130)+8*s(1132)+52*s(1133)+6
  Such that:aux(175) =< V1
aux(176) =< V1+1/3
aux(177) =< V1/2
aux(178) =< 6/5*V1
s(1126) =< aux(175)
s(1127) =< aux(175)
s(1128) =< aux(175)
s(1129) =< aux(175)
s(1130) =< aux(175)
s(1127) =< aux(176)
s(1128) =< aux(176)
s(1129) =< aux(176)
s(1131) =< aux(176)
s(1131) =< aux(175)
s(1126) =< aux(177)
s(1127) =< aux(177)
s(1129) =< aux(178)
s(1132) =< aux(178)
s(1133) =< s(1131)

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

* Chain [100]: 2*s(1159)+7
  Such that:s(1158) =< V
s(1159) =< s(1158)

  with precondition: [V1=V+1,V1>=3] 


Closed-form bounds of start(V1,V,V7): 
-------------------------------------
* Chain [106] with precondition: [V1>=0,V>=0] 
    - Upper bound: 9307/5*V1+71*V+587/3 
    - Complexity: n 
* Chain [105] with precondition: [V1=1,V>=0,V7>=0] 
    - Upper bound: 1 
    - Complexity: constant 
* Chain [104] with precondition: [V1=1,V>=2] 
    - Upper bound: 5 
    - Complexity: constant 
* Chain [103] with precondition: [V1=2,V>=0,V7>=0] 
    - Upper bound: 1 
    - Complexity: constant 
* Chain [102] with precondition: [V=0,V1>=0] 
    - Upper bound: 1 
    - Complexity: constant 
* Chain [101] with precondition: [V=1,V1>=1] 
    - Upper bound: 888/5*V1+70/3 
    - Complexity: n 
* Chain [100] with precondition: [V1=V+1,V1>=3] 
    - Upper bound: 2*V+7 
    - Complexity: n 

### Maximum cost of start(V1,V,V7): 9307/5*V1+71*V+587/3 
Asymptotic class: n 
* Total analysis performed in 6836 ms.


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

(14)
BOUNDS(1, n^1)

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

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

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

   LEQ(0', z0) -> c
   LEQ(s(z0), 0') -> c1
   LEQ(s(z0), s(z1)) -> c2(LEQ(z0, z1))
   IF(true, z0, z1) -> c3
   IF(false, z0, z1) -> c4
   -'(z0, 0') -> c5
   -'(s(z0), s(z1)) -> c6(-'(z0, z1))
   MOD(0', z0) -> c7
   MOD(s(z0), 0') -> c8
   MOD(s(z0), s(z1)) -> c9(IF(leq(z1, z0), mod(-(s(z0), s(z1)), s(z1)), s(z0)), LEQ(z1, z0))
   MOD(s(z0), s(z1)) -> c10(IF(leq(z1, z0), mod(-(s(z0), s(z1)), s(z1)), s(z0)), MOD(-(s(z0), s(z1)), s(z1)), -'(s(z0), s(z1)))

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

   leq(0', z0) -> true
   leq(s(z0), 0') -> false
   leq(s(z0), s(z1)) -> leq(z0, z1)
   if(true, z0, z1) -> z0
   if(false, z0, z1) -> z1
   -(z0, 0') -> z0
   -(s(z0), s(z1)) -> -(z0, z1)
   mod(0', z0) -> 0'
   mod(s(z0), 0') -> 0'
   mod(s(z0), s(z1)) -> if(leq(z1, z0), mod(-(s(z0), s(z1)), s(z1)), s(z0))

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

(17) SlicingProof (LOWER BOUND(ID))
Sliced the following arguments:
IF/2

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

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

   LEQ(0', z0) -> c
   LEQ(s(z0), 0') -> c1
   LEQ(s(z0), s(z1)) -> c2(LEQ(z0, z1))
   IF(true, z0) -> c3
   IF(false, z0) -> c4
   -'(z0, 0') -> c5
   -'(s(z0), s(z1)) -> c6(-'(z0, z1))
   MOD(0', z0) -> c7
   MOD(s(z0), 0') -> c8
   MOD(s(z0), s(z1)) -> c9(IF(leq(z1, z0), mod(-(s(z0), s(z1)), s(z1))), LEQ(z1, z0))
   MOD(s(z0), s(z1)) -> c10(IF(leq(z1, z0), mod(-(s(z0), s(z1)), s(z1))), MOD(-(s(z0), s(z1)), s(z1)), -'(s(z0), s(z1)))

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

   leq(0', z0) -> true
   leq(s(z0), 0') -> false
   leq(s(z0), s(z1)) -> leq(z0, z1)
   if(true, z0, z1) -> z0
   if(false, z0, z1) -> z1
   -(z0, 0') -> z0
   -(s(z0), s(z1)) -> -(z0, z1)
   mod(0', z0) -> 0'
   mod(s(z0), 0') -> 0'
   mod(s(z0), s(z1)) -> if(leq(z1, z0), mod(-(s(z0), s(z1)), s(z1)), s(z0))

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

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

(20)
Obligation:
Innermost TRS:
Rules:
LEQ(0', z0) -> c
LEQ(s(z0), 0') -> c1
LEQ(s(z0), s(z1)) -> c2(LEQ(z0, z1))
IF(true, z0) -> c3
IF(false, z0) -> c4
-'(z0, 0') -> c5
-'(s(z0), s(z1)) -> c6(-'(z0, z1))
MOD(0', z0) -> c7
MOD(s(z0), 0') -> c8
MOD(s(z0), s(z1)) -> c9(IF(leq(z1, z0), mod(-(s(z0), s(z1)), s(z1))), LEQ(z1, z0))
MOD(s(z0), s(z1)) -> c10(IF(leq(z1, z0), mod(-(s(z0), s(z1)), s(z1))), MOD(-(s(z0), s(z1)), s(z1)), -'(s(z0), s(z1)))
leq(0', z0) -> true
leq(s(z0), 0') -> false
leq(s(z0), s(z1)) -> leq(z0, z1)
if(true, z0, z1) -> z0
if(false, z0, z1) -> z1
-(z0, 0') -> z0
-(s(z0), s(z1)) -> -(z0, z1)
mod(0', z0) -> 0'
mod(s(z0), 0') -> 0'
mod(s(z0), s(z1)) -> if(leq(z1, z0), mod(-(s(z0), s(z1)), s(z1)), s(z0))

Types:
LEQ :: 0':s -> 0':s -> c:c1:c2
0' :: 0':s
c :: c:c1:c2
s :: 0':s -> 0':s
c1 :: c:c1:c2
c2 :: c:c1:c2 -> c:c1:c2
IF :: true:false -> 0':s -> c3:c4
true :: true:false
c3 :: c3:c4
false :: true:false
c4 :: c3:c4
-' :: 0':s -> 0':s -> c5:c6
c5 :: c5:c6
c6 :: c5:c6 -> c5:c6
MOD :: 0':s -> 0':s -> c7:c8:c9:c10
c7 :: c7:c8:c9:c10
c8 :: c7:c8:c9:c10
c9 :: c3:c4 -> c:c1:c2 -> c7:c8:c9:c10
leq :: 0':s -> 0':s -> true:false
mod :: 0':s -> 0':s -> 0':s
- :: 0':s -> 0':s -> 0':s
c10 :: c3:c4 -> c7:c8:c9:c10 -> c5:c6 -> c7:c8:c9:c10
if :: true:false -> 0':s -> 0':s -> 0':s
hole_c:c1:c21_11 :: c:c1:c2
hole_0':s2_11 :: 0':s
hole_c3:c43_11 :: c3:c4
hole_true:false4_11 :: true:false
hole_c5:c65_11 :: c5:c6
hole_c7:c8:c9:c106_11 :: c7:c8:c9:c10
gen_c:c1:c27_11 :: Nat -> c:c1:c2
gen_0':s8_11 :: Nat -> 0':s
gen_c5:c69_11 :: Nat -> c5:c6
gen_c7:c8:c9:c1010_11 :: Nat -> c7:c8:c9:c10

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

(21) OrderProof (LOWER BOUND(ID))
Heuristically decided to analyse the following defined symbols:
LEQ, -', MOD, leq, mod, -

They will be analysed ascendingly in the following order:
LEQ < MOD
-' < MOD
leq < MOD
mod < MOD
- < MOD
leq < mod
- < mod

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

(22)
Obligation:
Innermost TRS:
Rules:
LEQ(0', z0) -> c
LEQ(s(z0), 0') -> c1
LEQ(s(z0), s(z1)) -> c2(LEQ(z0, z1))
IF(true, z0) -> c3
IF(false, z0) -> c4
-'(z0, 0') -> c5
-'(s(z0), s(z1)) -> c6(-'(z0, z1))
MOD(0', z0) -> c7
MOD(s(z0), 0') -> c8
MOD(s(z0), s(z1)) -> c9(IF(leq(z1, z0), mod(-(s(z0), s(z1)), s(z1))), LEQ(z1, z0))
MOD(s(z0), s(z1)) -> c10(IF(leq(z1, z0), mod(-(s(z0), s(z1)), s(z1))), MOD(-(s(z0), s(z1)), s(z1)), -'(s(z0), s(z1)))
leq(0', z0) -> true
leq(s(z0), 0') -> false
leq(s(z0), s(z1)) -> leq(z0, z1)
if(true, z0, z1) -> z0
if(false, z0, z1) -> z1
-(z0, 0') -> z0
-(s(z0), s(z1)) -> -(z0, z1)
mod(0', z0) -> 0'
mod(s(z0), 0') -> 0'
mod(s(z0), s(z1)) -> if(leq(z1, z0), mod(-(s(z0), s(z1)), s(z1)), s(z0))

Types:
LEQ :: 0':s -> 0':s -> c:c1:c2
0' :: 0':s
c :: c:c1:c2
s :: 0':s -> 0':s
c1 :: c:c1:c2
c2 :: c:c1:c2 -> c:c1:c2
IF :: true:false -> 0':s -> c3:c4
true :: true:false
c3 :: c3:c4
false :: true:false
c4 :: c3:c4
-' :: 0':s -> 0':s -> c5:c6
c5 :: c5:c6
c6 :: c5:c6 -> c5:c6
MOD :: 0':s -> 0':s -> c7:c8:c9:c10
c7 :: c7:c8:c9:c10
c8 :: c7:c8:c9:c10
c9 :: c3:c4 -> c:c1:c2 -> c7:c8:c9:c10
leq :: 0':s -> 0':s -> true:false
mod :: 0':s -> 0':s -> 0':s
- :: 0':s -> 0':s -> 0':s
c10 :: c3:c4 -> c7:c8:c9:c10 -> c5:c6 -> c7:c8:c9:c10
if :: true:false -> 0':s -> 0':s -> 0':s
hole_c:c1:c21_11 :: c:c1:c2
hole_0':s2_11 :: 0':s
hole_c3:c43_11 :: c3:c4
hole_true:false4_11 :: true:false
hole_c5:c65_11 :: c5:c6
hole_c7:c8:c9:c106_11 :: c7:c8:c9:c10
gen_c:c1:c27_11 :: Nat -> c:c1:c2
gen_0':s8_11 :: Nat -> 0':s
gen_c5:c69_11 :: Nat -> c5:c6
gen_c7:c8:c9:c1010_11 :: Nat -> c7:c8:c9:c10


Generator Equations:
gen_c:c1:c27_11(0) <=> c
gen_c:c1:c27_11(+(x, 1)) <=> c2(gen_c:c1:c27_11(x))
gen_0':s8_11(0) <=> 0'
gen_0':s8_11(+(x, 1)) <=> s(gen_0':s8_11(x))
gen_c5:c69_11(0) <=> c5
gen_c5:c69_11(+(x, 1)) <=> c6(gen_c5:c69_11(x))
gen_c7:c8:c9:c1010_11(0) <=> c7
gen_c7:c8:c9:c1010_11(+(x, 1)) <=> c10(c3, gen_c7:c8:c9:c1010_11(x), c5)


The following defined symbols remain to be analysed:
LEQ, -', MOD, leq, mod, -

They will be analysed ascendingly in the following order:
LEQ < MOD
-' < MOD
leq < MOD
mod < MOD
- < MOD
leq < mod
- < mod

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

(23) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
LEQ(gen_0':s8_11(n12_11), gen_0':s8_11(n12_11)) -> gen_c:c1:c27_11(n12_11), rt in Omega(1 + n12_11)

Induction Base:
LEQ(gen_0':s8_11(0), gen_0':s8_11(0)) ->_R^Omega(1)
c

Induction Step:
LEQ(gen_0':s8_11(+(n12_11, 1)), gen_0':s8_11(+(n12_11, 1))) ->_R^Omega(1)
c2(LEQ(gen_0':s8_11(n12_11), gen_0':s8_11(n12_11))) ->_IH
c2(gen_c:c1:c27_11(c13_11))

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

(24)
Complex Obligation (BEST)

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

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

Innermost TRS:
Rules:
LEQ(0', z0) -> c
LEQ(s(z0), 0') -> c1
LEQ(s(z0), s(z1)) -> c2(LEQ(z0, z1))
IF(true, z0) -> c3
IF(false, z0) -> c4
-'(z0, 0') -> c5
-'(s(z0), s(z1)) -> c6(-'(z0, z1))
MOD(0', z0) -> c7
MOD(s(z0), 0') -> c8
MOD(s(z0), s(z1)) -> c9(IF(leq(z1, z0), mod(-(s(z0), s(z1)), s(z1))), LEQ(z1, z0))
MOD(s(z0), s(z1)) -> c10(IF(leq(z1, z0), mod(-(s(z0), s(z1)), s(z1))), MOD(-(s(z0), s(z1)), s(z1)), -'(s(z0), s(z1)))
leq(0', z0) -> true
leq(s(z0), 0') -> false
leq(s(z0), s(z1)) -> leq(z0, z1)
if(true, z0, z1) -> z0
if(false, z0, z1) -> z1
-(z0, 0') -> z0
-(s(z0), s(z1)) -> -(z0, z1)
mod(0', z0) -> 0'
mod(s(z0), 0') -> 0'
mod(s(z0), s(z1)) -> if(leq(z1, z0), mod(-(s(z0), s(z1)), s(z1)), s(z0))

Types:
LEQ :: 0':s -> 0':s -> c:c1:c2
0' :: 0':s
c :: c:c1:c2
s :: 0':s -> 0':s
c1 :: c:c1:c2
c2 :: c:c1:c2 -> c:c1:c2
IF :: true:false -> 0':s -> c3:c4
true :: true:false
c3 :: c3:c4
false :: true:false
c4 :: c3:c4
-' :: 0':s -> 0':s -> c5:c6
c5 :: c5:c6
c6 :: c5:c6 -> c5:c6
MOD :: 0':s -> 0':s -> c7:c8:c9:c10
c7 :: c7:c8:c9:c10
c8 :: c7:c8:c9:c10
c9 :: c3:c4 -> c:c1:c2 -> c7:c8:c9:c10
leq :: 0':s -> 0':s -> true:false
mod :: 0':s -> 0':s -> 0':s
- :: 0':s -> 0':s -> 0':s
c10 :: c3:c4 -> c7:c8:c9:c10 -> c5:c6 -> c7:c8:c9:c10
if :: true:false -> 0':s -> 0':s -> 0':s
hole_c:c1:c21_11 :: c:c1:c2
hole_0':s2_11 :: 0':s
hole_c3:c43_11 :: c3:c4
hole_true:false4_11 :: true:false
hole_c5:c65_11 :: c5:c6
hole_c7:c8:c9:c106_11 :: c7:c8:c9:c10
gen_c:c1:c27_11 :: Nat -> c:c1:c2
gen_0':s8_11 :: Nat -> 0':s
gen_c5:c69_11 :: Nat -> c5:c6
gen_c7:c8:c9:c1010_11 :: Nat -> c7:c8:c9:c10


Generator Equations:
gen_c:c1:c27_11(0) <=> c
gen_c:c1:c27_11(+(x, 1)) <=> c2(gen_c:c1:c27_11(x))
gen_0':s8_11(0) <=> 0'
gen_0':s8_11(+(x, 1)) <=> s(gen_0':s8_11(x))
gen_c5:c69_11(0) <=> c5
gen_c5:c69_11(+(x, 1)) <=> c6(gen_c5:c69_11(x))
gen_c7:c8:c9:c1010_11(0) <=> c7
gen_c7:c8:c9:c1010_11(+(x, 1)) <=> c10(c3, gen_c7:c8:c9:c1010_11(x), c5)


The following defined symbols remain to be analysed:
LEQ, -', MOD, leq, mod, -

They will be analysed ascendingly in the following order:
LEQ < MOD
-' < MOD
leq < MOD
mod < MOD
- < MOD
leq < mod
- < mod

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

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

(27)
BOUNDS(n^1, INF)

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

(28)
Obligation:
Innermost TRS:
Rules:
LEQ(0', z0) -> c
LEQ(s(z0), 0') -> c1
LEQ(s(z0), s(z1)) -> c2(LEQ(z0, z1))
IF(true, z0) -> c3
IF(false, z0) -> c4
-'(z0, 0') -> c5
-'(s(z0), s(z1)) -> c6(-'(z0, z1))
MOD(0', z0) -> c7
MOD(s(z0), 0') -> c8
MOD(s(z0), s(z1)) -> c9(IF(leq(z1, z0), mod(-(s(z0), s(z1)), s(z1))), LEQ(z1, z0))
MOD(s(z0), s(z1)) -> c10(IF(leq(z1, z0), mod(-(s(z0), s(z1)), s(z1))), MOD(-(s(z0), s(z1)), s(z1)), -'(s(z0), s(z1)))
leq(0', z0) -> true
leq(s(z0), 0') -> false
leq(s(z0), s(z1)) -> leq(z0, z1)
if(true, z0, z1) -> z0
if(false, z0, z1) -> z1
-(z0, 0') -> z0
-(s(z0), s(z1)) -> -(z0, z1)
mod(0', z0) -> 0'
mod(s(z0), 0') -> 0'
mod(s(z0), s(z1)) -> if(leq(z1, z0), mod(-(s(z0), s(z1)), s(z1)), s(z0))

Types:
LEQ :: 0':s -> 0':s -> c:c1:c2
0' :: 0':s
c :: c:c1:c2
s :: 0':s -> 0':s
c1 :: c:c1:c2
c2 :: c:c1:c2 -> c:c1:c2
IF :: true:false -> 0':s -> c3:c4
true :: true:false
c3 :: c3:c4
false :: true:false
c4 :: c3:c4
-' :: 0':s -> 0':s -> c5:c6
c5 :: c5:c6
c6 :: c5:c6 -> c5:c6
MOD :: 0':s -> 0':s -> c7:c8:c9:c10
c7 :: c7:c8:c9:c10
c8 :: c7:c8:c9:c10
c9 :: c3:c4 -> c:c1:c2 -> c7:c8:c9:c10
leq :: 0':s -> 0':s -> true:false
mod :: 0':s -> 0':s -> 0':s
- :: 0':s -> 0':s -> 0':s
c10 :: c3:c4 -> c7:c8:c9:c10 -> c5:c6 -> c7:c8:c9:c10
if :: true:false -> 0':s -> 0':s -> 0':s
hole_c:c1:c21_11 :: c:c1:c2
hole_0':s2_11 :: 0':s
hole_c3:c43_11 :: c3:c4
hole_true:false4_11 :: true:false
hole_c5:c65_11 :: c5:c6
hole_c7:c8:c9:c106_11 :: c7:c8:c9:c10
gen_c:c1:c27_11 :: Nat -> c:c1:c2
gen_0':s8_11 :: Nat -> 0':s
gen_c5:c69_11 :: Nat -> c5:c6
gen_c7:c8:c9:c1010_11 :: Nat -> c7:c8:c9:c10


Lemmas:
LEQ(gen_0':s8_11(n12_11), gen_0':s8_11(n12_11)) -> gen_c:c1:c27_11(n12_11), rt in Omega(1 + n12_11)


Generator Equations:
gen_c:c1:c27_11(0) <=> c
gen_c:c1:c27_11(+(x, 1)) <=> c2(gen_c:c1:c27_11(x))
gen_0':s8_11(0) <=> 0'
gen_0':s8_11(+(x, 1)) <=> s(gen_0':s8_11(x))
gen_c5:c69_11(0) <=> c5
gen_c5:c69_11(+(x, 1)) <=> c6(gen_c5:c69_11(x))
gen_c7:c8:c9:c1010_11(0) <=> c7
gen_c7:c8:c9:c1010_11(+(x, 1)) <=> c10(c3, gen_c7:c8:c9:c1010_11(x), c5)


The following defined symbols remain to be analysed:
-', MOD, leq, mod, -

They will be analysed ascendingly in the following order:
-' < MOD
leq < MOD
mod < MOD
- < MOD
leq < mod
- < mod

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

(29) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
-'(gen_0':s8_11(n607_11), gen_0':s8_11(n607_11)) -> gen_c5:c69_11(n607_11), rt in Omega(1 + n607_11)

Induction Base:
-'(gen_0':s8_11(0), gen_0':s8_11(0)) ->_R^Omega(1)
c5

Induction Step:
-'(gen_0':s8_11(+(n607_11, 1)), gen_0':s8_11(+(n607_11, 1))) ->_R^Omega(1)
c6(-'(gen_0':s8_11(n607_11), gen_0':s8_11(n607_11))) ->_IH
c6(gen_c5:c69_11(c608_11))

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

(30)
Obligation:
Innermost TRS:
Rules:
LEQ(0', z0) -> c
LEQ(s(z0), 0') -> c1
LEQ(s(z0), s(z1)) -> c2(LEQ(z0, z1))
IF(true, z0) -> c3
IF(false, z0) -> c4
-'(z0, 0') -> c5
-'(s(z0), s(z1)) -> c6(-'(z0, z1))
MOD(0', z0) -> c7
MOD(s(z0), 0') -> c8
MOD(s(z0), s(z1)) -> c9(IF(leq(z1, z0), mod(-(s(z0), s(z1)), s(z1))), LEQ(z1, z0))
MOD(s(z0), s(z1)) -> c10(IF(leq(z1, z0), mod(-(s(z0), s(z1)), s(z1))), MOD(-(s(z0), s(z1)), s(z1)), -'(s(z0), s(z1)))
leq(0', z0) -> true
leq(s(z0), 0') -> false
leq(s(z0), s(z1)) -> leq(z0, z1)
if(true, z0, z1) -> z0
if(false, z0, z1) -> z1
-(z0, 0') -> z0
-(s(z0), s(z1)) -> -(z0, z1)
mod(0', z0) -> 0'
mod(s(z0), 0') -> 0'
mod(s(z0), s(z1)) -> if(leq(z1, z0), mod(-(s(z0), s(z1)), s(z1)), s(z0))

Types:
LEQ :: 0':s -> 0':s -> c:c1:c2
0' :: 0':s
c :: c:c1:c2
s :: 0':s -> 0':s
c1 :: c:c1:c2
c2 :: c:c1:c2 -> c:c1:c2
IF :: true:false -> 0':s -> c3:c4
true :: true:false
c3 :: c3:c4
false :: true:false
c4 :: c3:c4
-' :: 0':s -> 0':s -> c5:c6
c5 :: c5:c6
c6 :: c5:c6 -> c5:c6
MOD :: 0':s -> 0':s -> c7:c8:c9:c10
c7 :: c7:c8:c9:c10
c8 :: c7:c8:c9:c10
c9 :: c3:c4 -> c:c1:c2 -> c7:c8:c9:c10
leq :: 0':s -> 0':s -> true:false
mod :: 0':s -> 0':s -> 0':s
- :: 0':s -> 0':s -> 0':s
c10 :: c3:c4 -> c7:c8:c9:c10 -> c5:c6 -> c7:c8:c9:c10
if :: true:false -> 0':s -> 0':s -> 0':s
hole_c:c1:c21_11 :: c:c1:c2
hole_0':s2_11 :: 0':s
hole_c3:c43_11 :: c3:c4
hole_true:false4_11 :: true:false
hole_c5:c65_11 :: c5:c6
hole_c7:c8:c9:c106_11 :: c7:c8:c9:c10
gen_c:c1:c27_11 :: Nat -> c:c1:c2
gen_0':s8_11 :: Nat -> 0':s
gen_c5:c69_11 :: Nat -> c5:c6
gen_c7:c8:c9:c1010_11 :: Nat -> c7:c8:c9:c10


Lemmas:
LEQ(gen_0':s8_11(n12_11), gen_0':s8_11(n12_11)) -> gen_c:c1:c27_11(n12_11), rt in Omega(1 + n12_11)
-'(gen_0':s8_11(n607_11), gen_0':s8_11(n607_11)) -> gen_c5:c69_11(n607_11), rt in Omega(1 + n607_11)


Generator Equations:
gen_c:c1:c27_11(0) <=> c
gen_c:c1:c27_11(+(x, 1)) <=> c2(gen_c:c1:c27_11(x))
gen_0':s8_11(0) <=> 0'
gen_0':s8_11(+(x, 1)) <=> s(gen_0':s8_11(x))
gen_c5:c69_11(0) <=> c5
gen_c5:c69_11(+(x, 1)) <=> c6(gen_c5:c69_11(x))
gen_c7:c8:c9:c1010_11(0) <=> c7
gen_c7:c8:c9:c1010_11(+(x, 1)) <=> c10(c3, gen_c7:c8:c9:c1010_11(x), c5)


The following defined symbols remain to be analysed:
leq, MOD, mod, -

They will be analysed ascendingly in the following order:
leq < MOD
mod < MOD
- < MOD
leq < mod
- < mod

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

(31) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
leq(gen_0':s8_11(n1092_11), gen_0':s8_11(n1092_11)) -> true, rt in Omega(0)

Induction Base:
leq(gen_0':s8_11(0), gen_0':s8_11(0)) ->_R^Omega(0)
true

Induction Step:
leq(gen_0':s8_11(+(n1092_11, 1)), gen_0':s8_11(+(n1092_11, 1))) ->_R^Omega(0)
leq(gen_0':s8_11(n1092_11), gen_0':s8_11(n1092_11)) ->_IH
true

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:
LEQ(0', z0) -> c
LEQ(s(z0), 0') -> c1
LEQ(s(z0), s(z1)) -> c2(LEQ(z0, z1))
IF(true, z0) -> c3
IF(false, z0) -> c4
-'(z0, 0') -> c5
-'(s(z0), s(z1)) -> c6(-'(z0, z1))
MOD(0', z0) -> c7
MOD(s(z0), 0') -> c8
MOD(s(z0), s(z1)) -> c9(IF(leq(z1, z0), mod(-(s(z0), s(z1)), s(z1))), LEQ(z1, z0))
MOD(s(z0), s(z1)) -> c10(IF(leq(z1, z0), mod(-(s(z0), s(z1)), s(z1))), MOD(-(s(z0), s(z1)), s(z1)), -'(s(z0), s(z1)))
leq(0', z0) -> true
leq(s(z0), 0') -> false
leq(s(z0), s(z1)) -> leq(z0, z1)
if(true, z0, z1) -> z0
if(false, z0, z1) -> z1
-(z0, 0') -> z0
-(s(z0), s(z1)) -> -(z0, z1)
mod(0', z0) -> 0'
mod(s(z0), 0') -> 0'
mod(s(z0), s(z1)) -> if(leq(z1, z0), mod(-(s(z0), s(z1)), s(z1)), s(z0))

Types:
LEQ :: 0':s -> 0':s -> c:c1:c2
0' :: 0':s
c :: c:c1:c2
s :: 0':s -> 0':s
c1 :: c:c1:c2
c2 :: c:c1:c2 -> c:c1:c2
IF :: true:false -> 0':s -> c3:c4
true :: true:false
c3 :: c3:c4
false :: true:false
c4 :: c3:c4
-' :: 0':s -> 0':s -> c5:c6
c5 :: c5:c6
c6 :: c5:c6 -> c5:c6
MOD :: 0':s -> 0':s -> c7:c8:c9:c10
c7 :: c7:c8:c9:c10
c8 :: c7:c8:c9:c10
c9 :: c3:c4 -> c:c1:c2 -> c7:c8:c9:c10
leq :: 0':s -> 0':s -> true:false
mod :: 0':s -> 0':s -> 0':s
- :: 0':s -> 0':s -> 0':s
c10 :: c3:c4 -> c7:c8:c9:c10 -> c5:c6 -> c7:c8:c9:c10
if :: true:false -> 0':s -> 0':s -> 0':s
hole_c:c1:c21_11 :: c:c1:c2
hole_0':s2_11 :: 0':s
hole_c3:c43_11 :: c3:c4
hole_true:false4_11 :: true:false
hole_c5:c65_11 :: c5:c6
hole_c7:c8:c9:c106_11 :: c7:c8:c9:c10
gen_c:c1:c27_11 :: Nat -> c:c1:c2
gen_0':s8_11 :: Nat -> 0':s
gen_c5:c69_11 :: Nat -> c5:c6
gen_c7:c8:c9:c1010_11 :: Nat -> c7:c8:c9:c10


Lemmas:
LEQ(gen_0':s8_11(n12_11), gen_0':s8_11(n12_11)) -> gen_c:c1:c27_11(n12_11), rt in Omega(1 + n12_11)
-'(gen_0':s8_11(n607_11), gen_0':s8_11(n607_11)) -> gen_c5:c69_11(n607_11), rt in Omega(1 + n607_11)
leq(gen_0':s8_11(n1092_11), gen_0':s8_11(n1092_11)) -> true, rt in Omega(0)


Generator Equations:
gen_c:c1:c27_11(0) <=> c
gen_c:c1:c27_11(+(x, 1)) <=> c2(gen_c:c1:c27_11(x))
gen_0':s8_11(0) <=> 0'
gen_0':s8_11(+(x, 1)) <=> s(gen_0':s8_11(x))
gen_c5:c69_11(0) <=> c5
gen_c5:c69_11(+(x, 1)) <=> c6(gen_c5:c69_11(x))
gen_c7:c8:c9:c1010_11(0) <=> c7
gen_c7:c8:c9:c1010_11(+(x, 1)) <=> c10(c3, gen_c7:c8:c9:c1010_11(x), c5)


The following defined symbols remain to be analysed:
-, MOD, mod

They will be analysed ascendingly in the following order:
mod < MOD
- < MOD
- < mod

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

(33) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
-(gen_0':s8_11(n1471_11), gen_0':s8_11(n1471_11)) -> gen_0':s8_11(0), rt in Omega(0)

Induction Base:
-(gen_0':s8_11(0), gen_0':s8_11(0)) ->_R^Omega(0)
gen_0':s8_11(0)

Induction Step:
-(gen_0':s8_11(+(n1471_11, 1)), gen_0':s8_11(+(n1471_11, 1))) ->_R^Omega(0)
-(gen_0':s8_11(n1471_11), gen_0':s8_11(n1471_11)) ->_IH
gen_0':s8_11(0)

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:
LEQ(0', z0) -> c
LEQ(s(z0), 0') -> c1
LEQ(s(z0), s(z1)) -> c2(LEQ(z0, z1))
IF(true, z0) -> c3
IF(false, z0) -> c4
-'(z0, 0') -> c5
-'(s(z0), s(z1)) -> c6(-'(z0, z1))
MOD(0', z0) -> c7
MOD(s(z0), 0') -> c8
MOD(s(z0), s(z1)) -> c9(IF(leq(z1, z0), mod(-(s(z0), s(z1)), s(z1))), LEQ(z1, z0))
MOD(s(z0), s(z1)) -> c10(IF(leq(z1, z0), mod(-(s(z0), s(z1)), s(z1))), MOD(-(s(z0), s(z1)), s(z1)), -'(s(z0), s(z1)))
leq(0', z0) -> true
leq(s(z0), 0') -> false
leq(s(z0), s(z1)) -> leq(z0, z1)
if(true, z0, z1) -> z0
if(false, z0, z1) -> z1
-(z0, 0') -> z0
-(s(z0), s(z1)) -> -(z0, z1)
mod(0', z0) -> 0'
mod(s(z0), 0') -> 0'
mod(s(z0), s(z1)) -> if(leq(z1, z0), mod(-(s(z0), s(z1)), s(z1)), s(z0))

Types:
LEQ :: 0':s -> 0':s -> c:c1:c2
0' :: 0':s
c :: c:c1:c2
s :: 0':s -> 0':s
c1 :: c:c1:c2
c2 :: c:c1:c2 -> c:c1:c2
IF :: true:false -> 0':s -> c3:c4
true :: true:false
c3 :: c3:c4
false :: true:false
c4 :: c3:c4
-' :: 0':s -> 0':s -> c5:c6
c5 :: c5:c6
c6 :: c5:c6 -> c5:c6
MOD :: 0':s -> 0':s -> c7:c8:c9:c10
c7 :: c7:c8:c9:c10
c8 :: c7:c8:c9:c10
c9 :: c3:c4 -> c:c1:c2 -> c7:c8:c9:c10
leq :: 0':s -> 0':s -> true:false
mod :: 0':s -> 0':s -> 0':s
- :: 0':s -> 0':s -> 0':s
c10 :: c3:c4 -> c7:c8:c9:c10 -> c5:c6 -> c7:c8:c9:c10
if :: true:false -> 0':s -> 0':s -> 0':s
hole_c:c1:c21_11 :: c:c1:c2
hole_0':s2_11 :: 0':s
hole_c3:c43_11 :: c3:c4
hole_true:false4_11 :: true:false
hole_c5:c65_11 :: c5:c6
hole_c7:c8:c9:c106_11 :: c7:c8:c9:c10
gen_c:c1:c27_11 :: Nat -> c:c1:c2
gen_0':s8_11 :: Nat -> 0':s
gen_c5:c69_11 :: Nat -> c5:c6
gen_c7:c8:c9:c1010_11 :: Nat -> c7:c8:c9:c10


Lemmas:
LEQ(gen_0':s8_11(n12_11), gen_0':s8_11(n12_11)) -> gen_c:c1:c27_11(n12_11), rt in Omega(1 + n12_11)
-'(gen_0':s8_11(n607_11), gen_0':s8_11(n607_11)) -> gen_c5:c69_11(n607_11), rt in Omega(1 + n607_11)
leq(gen_0':s8_11(n1092_11), gen_0':s8_11(n1092_11)) -> true, rt in Omega(0)
-(gen_0':s8_11(n1471_11), gen_0':s8_11(n1471_11)) -> gen_0':s8_11(0), rt in Omega(0)


Generator Equations:
gen_c:c1:c27_11(0) <=> c
gen_c:c1:c27_11(+(x, 1)) <=> c2(gen_c:c1:c27_11(x))
gen_0':s8_11(0) <=> 0'
gen_0':s8_11(+(x, 1)) <=> s(gen_0':s8_11(x))
gen_c5:c69_11(0) <=> c5
gen_c5:c69_11(+(x, 1)) <=> c6(gen_c5:c69_11(x))
gen_c7:c8:c9:c1010_11(0) <=> c7
gen_c7:c8:c9:c1010_11(+(x, 1)) <=> c10(c3, gen_c7:c8:c9:c1010_11(x), c5)


The following defined symbols remain to be analysed:
mod, MOD

They will be analysed ascendingly in the following order:
mod < MOD