WORST_CASE(?,O(n^2)) proof of input_wT3w4DauDV.trs # AProVE Commit ID: 5b976082cb74a395683ed8cc7acf94bd611ab29f fuhs 20230524 unpublished The Runtime Complexity (parallel-innermost) of the given CpxTRS could be proven to be BOUNDS(1, n^2). (0) CpxTRS (1) CpxTrsToCdtProof [UPPER BOUND(ID), 0 ms] (2) CdtProblem (3) CdtLeafRemovalProof [BOTH BOUNDS(ID, ID), 0 ms] (4) CdtProblem (5) CdtRhsSimplificationProcessorProof [BOTH BOUNDS(ID, ID), 0 ms] (6) CdtProblem (7) CdtUsableRulesProof [BOTH BOUNDS(ID, ID), 0 ms] (8) CdtProblem (9) CdtToCpxRelTrsProof [BOTH BOUNDS(ID, ID), 0 ms] (10) CpxRelTRS (11) RelTrsToWeightedTrsProof [BOTH BOUNDS(ID, ID), 0 ms] (12) CpxWeightedTrs (13) TypeInferenceProof [BOTH BOUNDS(ID, ID), 0 ms] (14) CpxTypedWeightedTrs (15) CompletionProof [UPPER BOUND(ID), 0 ms] (16) CpxTypedWeightedCompleteTrs (17) CpxTypedWeightedTrsToRntsProof [UPPER BOUND(ID), 0 ms] (18) CpxRNTS (19) CompleteCoflocoProof [FINISHED, 15.7 s] (20) BOUNDS(1, n^2) ---------------------------------------- (0) Obligation: The Runtime Complexity (parallel-innermost) of the given CpxTRS could be proven to be BOUNDS(1, n^2). The TRS R consists of the following rules: cond(true, x, y, z) -> cond(and(gr(x, z), gr(y, z)), p(x), p(y), z) and(true, true) -> true and(x, false) -> false and(false, x) -> false gr(0, 0) -> false gr(0, x) -> false gr(s(x), 0) -> true gr(s(x), s(y)) -> gr(x, y) p(0) -> 0 p(s(x)) -> x S is empty. Rewrite Strategy: PARALLEL_INNERMOST ---------------------------------------- (1) CpxTrsToCdtProof (UPPER BOUND(ID)) Converted Cpx (relative) TRS with rewrite strategy PARALLEL_INNERMOST to CDT ---------------------------------------- (2) Obligation: Complexity Dependency Tuples Problem Rules: cond(true, z0, z1, z2) -> cond(and(gr(z0, z2), gr(z1, z2)), p(z0), p(z1), z2) and(true, true) -> true and(z0, false) -> false and(false, z0) -> false gr(0, 0) -> false gr(0, z0) -> false gr(s(z0), 0) -> true gr(s(z0), s(z1)) -> gr(z0, z1) p(0) -> 0 p(s(z0)) -> z0 Tuples: COND(true, z0, z1, z2) -> c(COND(and(gr(z0, z2), gr(z1, z2)), p(z0), p(z1), z2), AND(gr(z0, z2), gr(z1, z2)), GR(z0, z2)) COND(true, z0, z1, z2) -> c1(COND(and(gr(z0, z2), gr(z1, z2)), p(z0), p(z1), z2), AND(gr(z0, z2), gr(z1, z2)), GR(z1, z2)) COND(true, z0, z1, z2) -> c2(COND(and(gr(z0, z2), gr(z1, z2)), p(z0), p(z1), z2), P(z0)) COND(true, z0, z1, z2) -> c3(COND(and(gr(z0, z2), gr(z1, z2)), p(z0), p(z1), z2), P(z1)) AND(true, true) -> c4 AND(z0, false) -> c5 AND(false, z0) -> c6 GR(0, 0) -> c7 GR(0, z0) -> c8 GR(s(z0), 0) -> c9 GR(s(z0), s(z1)) -> c10(GR(z0, z1)) P(0) -> c11 P(s(z0)) -> c12 S tuples: COND(true, z0, z1, z2) -> c(COND(and(gr(z0, z2), gr(z1, z2)), p(z0), p(z1), z2), AND(gr(z0, z2), gr(z1, z2)), GR(z0, z2)) COND(true, z0, z1, z2) -> c1(COND(and(gr(z0, z2), gr(z1, z2)), p(z0), p(z1), z2), AND(gr(z0, z2), gr(z1, z2)), GR(z1, z2)) COND(true, z0, z1, z2) -> c2(COND(and(gr(z0, z2), gr(z1, z2)), p(z0), p(z1), z2), P(z0)) COND(true, z0, z1, z2) -> c3(COND(and(gr(z0, z2), gr(z1, z2)), p(z0), p(z1), z2), P(z1)) AND(true, true) -> c4 AND(z0, false) -> c5 AND(false, z0) -> c6 GR(0, 0) -> c7 GR(0, z0) -> c8 GR(s(z0), 0) -> c9 GR(s(z0), s(z1)) -> c10(GR(z0, z1)) P(0) -> c11 P(s(z0)) -> c12 K tuples:none Defined Rule Symbols: cond_4, and_2, gr_2, p_1 Defined Pair Symbols: COND_4, AND_2, GR_2, P_1 Compound Symbols: c_3, c1_3, c2_2, c3_2, c4, c5, c6, c7, c8, c9, c10_1, c11, c12 ---------------------------------------- (3) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID)) Removed 8 trailing nodes: AND(z0, false) -> c5 P(0) -> c11 GR(0, 0) -> c7 GR(0, z0) -> c8 AND(true, true) -> c4 AND(false, z0) -> c6 GR(s(z0), 0) -> c9 P(s(z0)) -> c12 ---------------------------------------- (4) Obligation: Complexity Dependency Tuples Problem Rules: cond(true, z0, z1, z2) -> cond(and(gr(z0, z2), gr(z1, z2)), p(z0), p(z1), z2) and(true, true) -> true and(z0, false) -> false and(false, z0) -> false gr(0, 0) -> false gr(0, z0) -> false gr(s(z0), 0) -> true gr(s(z0), s(z1)) -> gr(z0, z1) p(0) -> 0 p(s(z0)) -> z0 Tuples: COND(true, z0, z1, z2) -> c(COND(and(gr(z0, z2), gr(z1, z2)), p(z0), p(z1), z2), AND(gr(z0, z2), gr(z1, z2)), GR(z0, z2)) COND(true, z0, z1, z2) -> c1(COND(and(gr(z0, z2), gr(z1, z2)), p(z0), p(z1), z2), AND(gr(z0, z2), gr(z1, z2)), GR(z1, z2)) COND(true, z0, z1, z2) -> c2(COND(and(gr(z0, z2), gr(z1, z2)), p(z0), p(z1), z2), P(z0)) COND(true, z0, z1, z2) -> c3(COND(and(gr(z0, z2), gr(z1, z2)), p(z0), p(z1), z2), P(z1)) GR(s(z0), s(z1)) -> c10(GR(z0, z1)) S tuples: COND(true, z0, z1, z2) -> c(COND(and(gr(z0, z2), gr(z1, z2)), p(z0), p(z1), z2), AND(gr(z0, z2), gr(z1, z2)), GR(z0, z2)) COND(true, z0, z1, z2) -> c1(COND(and(gr(z0, z2), gr(z1, z2)), p(z0), p(z1), z2), AND(gr(z0, z2), gr(z1, z2)), GR(z1, z2)) COND(true, z0, z1, z2) -> c2(COND(and(gr(z0, z2), gr(z1, z2)), p(z0), p(z1), z2), P(z0)) COND(true, z0, z1, z2) -> c3(COND(and(gr(z0, z2), gr(z1, z2)), p(z0), p(z1), z2), P(z1)) GR(s(z0), s(z1)) -> c10(GR(z0, z1)) K tuples:none Defined Rule Symbols: cond_4, and_2, gr_2, p_1 Defined Pair Symbols: COND_4, GR_2 Compound Symbols: c_3, c1_3, c2_2, c3_2, c10_1 ---------------------------------------- (5) CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID)) Removed 4 trailing tuple parts ---------------------------------------- (6) Obligation: Complexity Dependency Tuples Problem Rules: cond(true, z0, z1, z2) -> cond(and(gr(z0, z2), gr(z1, z2)), p(z0), p(z1), z2) and(true, true) -> true and(z0, false) -> false and(false, z0) -> false gr(0, 0) -> false gr(0, z0) -> false gr(s(z0), 0) -> true gr(s(z0), s(z1)) -> gr(z0, z1) p(0) -> 0 p(s(z0)) -> z0 Tuples: GR(s(z0), s(z1)) -> c10(GR(z0, z1)) COND(true, z0, z1, z2) -> c(COND(and(gr(z0, z2), gr(z1, z2)), p(z0), p(z1), z2), GR(z0, z2)) COND(true, z0, z1, z2) -> c1(COND(and(gr(z0, z2), gr(z1, z2)), p(z0), p(z1), z2), GR(z1, z2)) COND(true, z0, z1, z2) -> c2(COND(and(gr(z0, z2), gr(z1, z2)), p(z0), p(z1), z2)) COND(true, z0, z1, z2) -> c3(COND(and(gr(z0, z2), gr(z1, z2)), p(z0), p(z1), z2)) S tuples: GR(s(z0), s(z1)) -> c10(GR(z0, z1)) COND(true, z0, z1, z2) -> c(COND(and(gr(z0, z2), gr(z1, z2)), p(z0), p(z1), z2), GR(z0, z2)) COND(true, z0, z1, z2) -> c1(COND(and(gr(z0, z2), gr(z1, z2)), p(z0), p(z1), z2), GR(z1, z2)) COND(true, z0, z1, z2) -> c2(COND(and(gr(z0, z2), gr(z1, z2)), p(z0), p(z1), z2)) COND(true, z0, z1, z2) -> c3(COND(and(gr(z0, z2), gr(z1, z2)), p(z0), p(z1), z2)) K tuples:none Defined Rule Symbols: cond_4, and_2, gr_2, p_1 Defined Pair Symbols: GR_2, COND_4 Compound Symbols: c10_1, c_2, c1_2, c2_1, c3_1 ---------------------------------------- (7) CdtUsableRulesProof (BOTH BOUNDS(ID, ID)) The following rules are not usable and were removed: cond(true, z0, z1, z2) -> cond(and(gr(z0, z2), gr(z1, z2)), p(z0), p(z1), z2) ---------------------------------------- (8) Obligation: Complexity Dependency Tuples Problem Rules: and(true, true) -> true and(z0, false) -> false and(false, z0) -> false gr(0, 0) -> false gr(0, z0) -> false gr(s(z0), 0) -> true gr(s(z0), s(z1)) -> gr(z0, z1) p(0) -> 0 p(s(z0)) -> z0 Tuples: GR(s(z0), s(z1)) -> c10(GR(z0, z1)) COND(true, z0, z1, z2) -> c(COND(and(gr(z0, z2), gr(z1, z2)), p(z0), p(z1), z2), GR(z0, z2)) COND(true, z0, z1, z2) -> c1(COND(and(gr(z0, z2), gr(z1, z2)), p(z0), p(z1), z2), GR(z1, z2)) COND(true, z0, z1, z2) -> c2(COND(and(gr(z0, z2), gr(z1, z2)), p(z0), p(z1), z2)) COND(true, z0, z1, z2) -> c3(COND(and(gr(z0, z2), gr(z1, z2)), p(z0), p(z1), z2)) S tuples: GR(s(z0), s(z1)) -> c10(GR(z0, z1)) COND(true, z0, z1, z2) -> c(COND(and(gr(z0, z2), gr(z1, z2)), p(z0), p(z1), z2), GR(z0, z2)) COND(true, z0, z1, z2) -> c1(COND(and(gr(z0, z2), gr(z1, z2)), p(z0), p(z1), z2), GR(z1, z2)) COND(true, z0, z1, z2) -> c2(COND(and(gr(z0, z2), gr(z1, z2)), p(z0), p(z1), z2)) COND(true, z0, z1, z2) -> c3(COND(and(gr(z0, z2), gr(z1, z2)), p(z0), p(z1), z2)) K tuples:none Defined Rule Symbols: and_2, gr_2, p_1 Defined Pair Symbols: GR_2, COND_4 Compound Symbols: c10_1, c_2, c1_2, c2_1, c3_1 ---------------------------------------- (9) CdtToCpxRelTrsProof (BOTH BOUNDS(ID, ID)) Converted S to standard rules, and D \ S as well as R to relative rules. ---------------------------------------- (10) Obligation: The Runtime Complexity (innermost) of the given CpxRelTRS could be proven to be BOUNDS(1, n^2). The TRS R consists of the following rules: GR(s(z0), s(z1)) -> c10(GR(z0, z1)) COND(true, z0, z1, z2) -> c(COND(and(gr(z0, z2), gr(z1, z2)), p(z0), p(z1), z2), GR(z0, z2)) COND(true, z0, z1, z2) -> c1(COND(and(gr(z0, z2), gr(z1, z2)), p(z0), p(z1), z2), GR(z1, z2)) COND(true, z0, z1, z2) -> c2(COND(and(gr(z0, z2), gr(z1, z2)), p(z0), p(z1), z2)) COND(true, z0, z1, z2) -> c3(COND(and(gr(z0, z2), gr(z1, z2)), p(z0), p(z1), z2)) The (relative) TRS S consists of the following rules: and(true, true) -> true and(z0, false) -> false and(false, z0) -> false gr(0, 0) -> false gr(0, z0) -> false gr(s(z0), 0) -> true gr(s(z0), s(z1)) -> gr(z0, z1) p(0) -> 0 p(s(z0)) -> z0 Rewrite Strategy: INNERMOST ---------------------------------------- (11) RelTrsToWeightedTrsProof (BOTH BOUNDS(ID, ID)) Transformed relative TRS to weighted TRS ---------------------------------------- (12) Obligation: The Runtime Complexity (innermost) of the given CpxWeightedTrs could be proven to be BOUNDS(1, n^2). The TRS R consists of the following rules: GR(s(z0), s(z1)) -> c10(GR(z0, z1)) [1] COND(true, z0, z1, z2) -> c(COND(and(gr(z0, z2), gr(z1, z2)), p(z0), p(z1), z2), GR(z0, z2)) [1] COND(true, z0, z1, z2) -> c1(COND(and(gr(z0, z2), gr(z1, z2)), p(z0), p(z1), z2), GR(z1, z2)) [1] COND(true, z0, z1, z2) -> c2(COND(and(gr(z0, z2), gr(z1, z2)), p(z0), p(z1), z2)) [1] COND(true, z0, z1, z2) -> c3(COND(and(gr(z0, z2), gr(z1, z2)), p(z0), p(z1), z2)) [1] and(true, true) -> true [0] and(z0, false) -> false [0] and(false, z0) -> false [0] gr(0, 0) -> false [0] gr(0, z0) -> false [0] gr(s(z0), 0) -> true [0] gr(s(z0), s(z1)) -> gr(z0, z1) [0] p(0) -> 0 [0] p(s(z0)) -> z0 [0] Rewrite Strategy: INNERMOST ---------------------------------------- (13) TypeInferenceProof (BOTH BOUNDS(ID, ID)) Infered types. ---------------------------------------- (14) Obligation: Runtime Complexity Weighted TRS with Types. The TRS R consists of the following rules: GR(s(z0), s(z1)) -> c10(GR(z0, z1)) [1] COND(true, z0, z1, z2) -> c(COND(and(gr(z0, z2), gr(z1, z2)), p(z0), p(z1), z2), GR(z0, z2)) [1] COND(true, z0, z1, z2) -> c1(COND(and(gr(z0, z2), gr(z1, z2)), p(z0), p(z1), z2), GR(z1, z2)) [1] COND(true, z0, z1, z2) -> c2(COND(and(gr(z0, z2), gr(z1, z2)), p(z0), p(z1), z2)) [1] COND(true, z0, z1, z2) -> c3(COND(and(gr(z0, z2), gr(z1, z2)), p(z0), p(z1), z2)) [1] and(true, true) -> true [0] and(z0, false) -> false [0] and(false, z0) -> false [0] gr(0, 0) -> false [0] gr(0, z0) -> false [0] gr(s(z0), 0) -> true [0] gr(s(z0), s(z1)) -> gr(z0, z1) [0] p(0) -> 0 [0] p(s(z0)) -> z0 [0] The TRS has the following type information: GR :: s:0 -> s:0 -> c10 s :: s:0 -> s:0 c10 :: c10 -> c10 COND :: true:false -> s:0 -> s:0 -> s:0 -> c:c1:c2:c3 true :: true:false c :: c:c1:c2:c3 -> c10 -> c:c1:c2:c3 and :: true:false -> true:false -> true:false gr :: s:0 -> s:0 -> true:false p :: s:0 -> s:0 c1 :: c:c1:c2:c3 -> c10 -> c:c1:c2:c3 c2 :: c:c1:c2:c3 -> c:c1:c2:c3 c3 :: c:c1:c2:c3 -> c:c1:c2:c3 false :: true:false 0 :: s:0 Rewrite Strategy: INNERMOST ---------------------------------------- (15) 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: and(v0, v1) -> null_and [0] gr(v0, v1) -> null_gr [0] p(v0) -> null_p [0] GR(v0, v1) -> null_GR [0] COND(v0, v1, v2, v3) -> null_COND [0] And the following fresh constants: null_and, null_gr, null_p, null_GR, null_COND ---------------------------------------- (16) 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: GR(s(z0), s(z1)) -> c10(GR(z0, z1)) [1] COND(true, z0, z1, z2) -> c(COND(and(gr(z0, z2), gr(z1, z2)), p(z0), p(z1), z2), GR(z0, z2)) [1] COND(true, z0, z1, z2) -> c1(COND(and(gr(z0, z2), gr(z1, z2)), p(z0), p(z1), z2), GR(z1, z2)) [1] COND(true, z0, z1, z2) -> c2(COND(and(gr(z0, z2), gr(z1, z2)), p(z0), p(z1), z2)) [1] COND(true, z0, z1, z2) -> c3(COND(and(gr(z0, z2), gr(z1, z2)), p(z0), p(z1), z2)) [1] and(true, true) -> true [0] and(z0, false) -> false [0] and(false, z0) -> false [0] gr(0, 0) -> false [0] gr(0, z0) -> false [0] gr(s(z0), 0) -> true [0] gr(s(z0), s(z1)) -> gr(z0, z1) [0] p(0) -> 0 [0] p(s(z0)) -> z0 [0] and(v0, v1) -> null_and [0] gr(v0, v1) -> null_gr [0] p(v0) -> null_p [0] GR(v0, v1) -> null_GR [0] COND(v0, v1, v2, v3) -> null_COND [0] The TRS has the following type information: GR :: s:0:null_p -> s:0:null_p -> c10:null_GR s :: s:0:null_p -> s:0:null_p c10 :: c10:null_GR -> c10:null_GR COND :: true:false:null_and:null_gr -> s:0:null_p -> s:0:null_p -> s:0:null_p -> c:c1:c2:c3:null_COND true :: true:false:null_and:null_gr c :: c:c1:c2:c3:null_COND -> c10:null_GR -> c:c1:c2:c3:null_COND and :: true:false:null_and:null_gr -> true:false:null_and:null_gr -> true:false:null_and:null_gr gr :: s:0:null_p -> s:0:null_p -> true:false:null_and:null_gr p :: s:0:null_p -> s:0:null_p c1 :: c:c1:c2:c3:null_COND -> c10:null_GR -> c:c1:c2:c3:null_COND c2 :: c:c1:c2:c3:null_COND -> c:c1:c2:c3:null_COND c3 :: c:c1:c2:c3:null_COND -> c:c1:c2:c3:null_COND false :: true:false:null_and:null_gr 0 :: s:0:null_p null_and :: true:false:null_and:null_gr null_gr :: true:false:null_and:null_gr null_p :: s:0:null_p null_GR :: c10:null_GR null_COND :: c:c1:c2:c3:null_COND Rewrite Strategy: INNERMOST ---------------------------------------- (17) CpxTypedWeightedTrsToRntsProof (UPPER BOUND(ID)) Transformed the TRS into an over-approximating RNTS by (improved) Size Abstraction. The constant constructors are abstracted as follows: true => 2 false => 1 0 => 0 null_and => 0 null_gr => 0 null_p => 0 null_GR => 0 null_COND => 0 ---------------------------------------- (18) Obligation: Complexity RNTS consisting of the following rules: COND(z, z', z'', z3) -{ 0 }-> 0 :|: v0 >= 0, z'' = v2, v1 >= 0, z = v0, z' = v1, z3 = v3, v2 >= 0, v3 >= 0 COND(z, z', z'', z3) -{ 1 }-> 1 + COND(and(gr(z0, z2), gr(z1, z2)), p(z0), p(z1), z2) :|: z = 2, z1 >= 0, z0 >= 0, z3 = z2, z' = z0, z2 >= 0, z'' = z1 COND(z, z', z'', z3) -{ 1 }-> 1 + COND(and(gr(z0, z2), gr(z1, z2)), p(z0), p(z1), z2) + GR(z0, z2) :|: z = 2, z1 >= 0, z0 >= 0, z3 = z2, z' = z0, z2 >= 0, z'' = z1 COND(z, z', z'', z3) -{ 1 }-> 1 + COND(and(gr(z0, z2), gr(z1, z2)), p(z0), p(z1), z2) + GR(z1, z2) :|: z = 2, z1 >= 0, z0 >= 0, z3 = z2, z' = z0, z2 >= 0, z'' = z1 GR(z, z') -{ 0 }-> 0 :|: v0 >= 0, v1 >= 0, z = v0, z' = v1 GR(z, z') -{ 1 }-> 1 + GR(z0, z1) :|: z1 >= 0, z = 1 + z0, z0 >= 0, z' = 1 + z1 and(z, z') -{ 0 }-> 2 :|: z = 2, z' = 2 and(z, z') -{ 0 }-> 1 :|: z = z0, z0 >= 0, z' = 1 and(z, z') -{ 0 }-> 1 :|: z = 1, z0 >= 0, z' = z0 and(z, z') -{ 0 }-> 0 :|: v0 >= 0, v1 >= 0, z = v0, z' = v1 gr(z, z') -{ 0 }-> gr(z0, z1) :|: z1 >= 0, z = 1 + z0, z0 >= 0, z' = 1 + z1 gr(z, z') -{ 0 }-> 2 :|: z = 1 + z0, z0 >= 0, z' = 0 gr(z, z') -{ 0 }-> 1 :|: z = 0, z' = 0 gr(z, z') -{ 0 }-> 1 :|: z0 >= 0, z = 0, z' = z0 gr(z, z') -{ 0 }-> 0 :|: v0 >= 0, v1 >= 0, z = v0, z' = v1 p(z) -{ 0 }-> z0 :|: z = 1 + z0, z0 >= 0 p(z) -{ 0 }-> 0 :|: z = 0 p(z) -{ 0 }-> 0 :|: v0 >= 0, z = v0 Only complete derivations are relevant for the runtime complexity. ---------------------------------------- (19) CompleteCoflocoProof (FINISHED) Transformed the RNTS (where only complete derivations are relevant) into cost relations for CoFloCo: eq(start(V1, V, V4, V8),0,[fun(V1, V, Out)],[V1 >= 0,V >= 0]). eq(start(V1, V, V4, V8),0,[fun1(V1, V, V4, V8, Out)],[V1 >= 0,V >= 0,V4 >= 0,V8 >= 0]). eq(start(V1, V, V4, V8),0,[and(V1, V, Out)],[V1 >= 0,V >= 0]). eq(start(V1, V, V4, V8),0,[gr(V1, V, Out)],[V1 >= 0,V >= 0]). eq(start(V1, V, V4, V8),0,[p(V1, Out)],[V1 >= 0]). eq(fun(V1, V, Out),1,[fun(V3, V2, Ret1)],[Out = 1 + Ret1,V2 >= 0,V1 = 1 + V3,V3 >= 0,V = 1 + V2]). eq(fun1(V1, V, V4, V8, Out),1,[gr(V6, V7, Ret0100),gr(V5, V7, Ret0101),and(Ret0100, Ret0101, Ret010),p(V6, Ret011),p(V5, Ret012),fun1(Ret010, Ret011, Ret012, V7, Ret01),fun(V6, V7, Ret11)],[Out = 1 + Ret01 + Ret11,V1 = 2,V5 >= 0,V6 >= 0,V8 = V7,V = V6,V7 >= 0,V4 = V5]). eq(fun1(V1, V, V4, V8, Out),1,[gr(V11, V9, Ret01001),gr(V10, V9, Ret01011),and(Ret01001, Ret01011, Ret0102),p(V11, Ret0111),p(V10, Ret0121),fun1(Ret0102, Ret0111, Ret0121, V9, Ret013),fun(V10, V9, Ret12)],[Out = 1 + Ret013 + Ret12,V1 = 2,V10 >= 0,V11 >= 0,V8 = V9,V = V11,V9 >= 0,V4 = V10]). eq(fun1(V1, V, V4, V8, Out),1,[gr(V12, V13, Ret100),gr(V14, V13, Ret101),and(Ret100, Ret101, Ret10),p(V12, Ret111),p(V14, Ret121),fun1(Ret10, Ret111, Ret121, V13, Ret13)],[Out = 1 + Ret13,V1 = 2,V14 >= 0,V12 >= 0,V8 = V13,V = V12,V13 >= 0,V4 = V14]). eq(and(V1, V, Out),0,[],[Out = 2,V1 = 2,V = 2]). eq(and(V1, V, Out),0,[],[Out = 1,V1 = V15,V15 >= 0,V = 1]). eq(and(V1, V, Out),0,[],[Out = 1,V1 = 1,V16 >= 0,V = V16]). eq(gr(V1, V, Out),0,[],[Out = 1,V1 = 0,V = 0]). eq(gr(V1, V, Out),0,[],[Out = 1,V17 >= 0,V1 = 0,V = V17]). eq(gr(V1, V, Out),0,[],[Out = 2,V1 = 1 + V18,V18 >= 0,V = 0]). eq(gr(V1, V, Out),0,[gr(V20, V19, Ret)],[Out = Ret,V19 >= 0,V1 = 1 + V20,V20 >= 0,V = 1 + V19]). eq(p(V1, Out),0,[],[Out = 0,V1 = 0]). eq(p(V1, Out),0,[],[Out = V21,V1 = 1 + V21,V21 >= 0]). eq(and(V1, V, Out),0,[],[Out = 0,V23 >= 0,V22 >= 0,V1 = V23,V = V22]). eq(gr(V1, V, Out),0,[],[Out = 0,V25 >= 0,V24 >= 0,V1 = V25,V = V24]). eq(p(V1, Out),0,[],[Out = 0,V26 >= 0,V1 = V26]). eq(fun(V1, V, Out),0,[],[Out = 0,V27 >= 0,V28 >= 0,V1 = V27,V = V28]). eq(fun1(V1, V, V4, V8, Out),0,[],[Out = 0,V29 >= 0,V4 = V32,V30 >= 0,V1 = V29,V = V30,V8 = V31,V32 >= 0,V31 >= 0]). input_output_vars(fun(V1,V,Out),[V1,V],[Out]). input_output_vars(fun1(V1,V,V4,V8,Out),[V1,V,V4,V8],[Out]). input_output_vars(and(V1,V,Out),[V1,V],[Out]). input_output_vars(gr(V1,V,Out),[V1,V],[Out]). input_output_vars(p(V1,Out),[V1],[Out]). CoFloCo proof output: Preprocessing Cost Relations ===================================== #### Computed strongly connected components 0. non_recursive : [and/3] 1. recursive : [fun/3] 2. recursive : [gr/3] 3. non_recursive : [p/2] 4. recursive [non_tail] : [fun1/5] 5. non_recursive : [start/4] #### Obtained direct recursion through partial evaluation 0. SCC is partially evaluated into and/3 1. SCC is partially evaluated into fun/3 2. SCC is partially evaluated into gr/3 3. SCC is partially evaluated into p/2 4. SCC is partially evaluated into fun1/5 5. SCC is partially evaluated into start/4 Control-Flow Refinement of Cost Relations ===================================== ### Specialization of cost equations and/3 * CE 15 is refined into CE [22] * CE 13 is refined into CE [23] * CE 12 is refined into CE [24] * CE 14 is refined into CE [25] ### Cost equations --> "Loop" of and/3 * CEs [22] --> Loop 16 * CEs [23] --> Loop 17 * CEs [24] --> Loop 18 * CEs [25] --> Loop 19 ### Ranking functions of CR and(V1,V,Out) #### Partial ranking functions of CR and(V1,V,Out) ### Specialization of cost equations fun/3 * CE 7 is refined into CE [26] * CE 6 is refined into CE [27] ### Cost equations --> "Loop" of fun/3 * CEs [27] --> Loop 20 * CEs [26] --> Loop 21 ### Ranking functions of CR fun(V1,V,Out) * RF of phase [20]: [V,V1] #### Partial ranking functions of CR fun(V1,V,Out) * Partial RF of phase [20]: - RF of loop [20:1]: V V1 ### Specialization of cost equations gr/3 * CE 19 is refined into CE [28] * CE 17 is refined into CE [29] * CE 16 is refined into CE [30] * CE 18 is refined into CE [31] ### Cost equations --> "Loop" of gr/3 * CEs [31] --> Loop 22 * CEs [28] --> Loop 23 * CEs [29] --> Loop 24 * CEs [30] --> Loop 25 ### Ranking functions of CR gr(V1,V,Out) * RF of phase [22]: [V,V1] #### Partial ranking functions of CR gr(V1,V,Out) * Partial RF of phase [22]: - RF of loop [22:1]: V V1 ### Specialization of cost equations p/2 * CE 21 is refined into CE [32] * CE 20 is refined into CE [33] ### Cost equations --> "Loop" of p/2 * CEs [32] --> Loop 26 * CEs [33] --> Loop 27 ### Ranking functions of CR p(V1,Out) #### Partial ranking functions of CR p(V1,Out) ### Specialization of cost equations fun1/5 * CE 11 is refined into CE [34] * CE 8 is refined into CE [35,36,37,38,39,40,41,42,43,44,45,46,47,48,49,50,51,52,53,54,55,56,57,58,59,60,61,62,63,64,65,66,67,68,69,70,71,72,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,125,126,127,128,129,130,131,132,133,134,135,136,137,138,139,140,141,142,143,144,145,146,147,148,149,150,151,152,153,154,155,156,157,158,159,160,161,162,163,164,165,166,167,168,169,170,171,172,173,174,175,176,177,178,179,180,181,182,183,184,185,186,187,188,189,190,191,192,193,194,195,196,197,198,199,200,201,202,203,204,205,206,207,208,209,210,211,212,213,214,215,216,217,218,219,220,221,222,223,224,225,226,227,228,229,230,231] * CE 9 is refined into CE [232,233,234,235,236,237,238,239,240,241,242,243,244,245,246,247,248,249,250,251,252,253,254,255,256,257,258,259,260,261,262,263,264,265,266,267,268,269,270,271,272,273,274,275,276,277,278,279,280,281,282,283,284,285,286,287,288,289,290,291,292,293,294,295,296,297,298,299,300,301,302,303,304,305,306,307,308,309,310,311,312,313,314,315,316,317,318,319,320,321,322,323,324,325,326,327,328,329,330,331,332,333,334,335,336,337,338,339,340,341,342,343,344,345,346,347,348,349,350,351,352,353,354,355,356,357,358,359,360,361,362,363,364,365,366,367,368,369,370,371,372,373,374,375,376,377,378,379,380,381,382,383,384,385,386,387,388,389,390,391,392,393,394,395,396,397,398,399,400,401,402,403,404,405,406,407,408,409,410,411,412,413,414,415,416,417,418,419,420,421,422,423,424,425,426,427,428] * CE 10 is refined into CE [429,430,431,432,433,434,435,436,437,438,439,440,441,442,443,444,445,446,447,448,449,450,451,452,453,454,455,456,457,458,459,460,461,462,463,464,465,466,467,468,469,470,471,472,473,474,475,476,477,478,479,480,481,482,483,484,485,486,487,488,489,490,491,492,493,494,495,496,497,498,499,500,501,502,503,504,505,506,507,508,509,510,511,512,513,514,515,516,517,518,519,520,521,522,523,524,525,526,527,528,529,530,531,532,533,534,535,536,537,538,539,540,541,542,543,544,545,546,547] ### Cost equations --> "Loop" of fun1/5 * CEs [223,420] --> Loop 28 * CEs [222,419,543] --> Loop 29 * CEs [221,418] --> Loop 30 * CEs [220,417,542] --> Loop 31 * CEs [219,416] --> Loop 32 * CEs [218,415,541] --> Loop 33 * CEs [217,414] --> Loop 34 * CEs [216,413,540] --> Loop 35 * CEs [336,376] --> Loop 36 * CEs [99,207] --> Loop 37 * CEs [135,151,159,175] --> Loop 38 * CEs [306,352,360,404] --> Loop 39 * CEs [98,206,305,403,481,535] --> Loop 40 * CEs [134,150,158,174,335,351,359,375,499,507,511,519] --> Loop 41 * CEs [97,205] --> Loop 42 * CEs [334,374] --> Loop 43 * CEs [304,350,358,402] --> Loop 44 * CEs [133,149,157,173] --> Loop 45 * CEs [96,204,303,401,480,534] --> Loop 46 * CEs [132,148,156,172,333,349,357,373,498,506,510,518] --> Loop 47 * CEs [332,372] --> Loop 48 * CEs [95,203] --> Loop 49 * CEs [131,147,155,171] --> Loop 50 * CEs [302,348,356,400] --> Loop 51 * CEs [130,170,331,371,497,517] --> Loop 52 * CEs [94,146,154,202,301,347,355,399,479,505,509,533] --> Loop 53 * CEs [93,201] --> Loop 54 * CEs [129,145,153] --> Loop 55 * CEs [169,330,370] --> Loop 56 * CEs [300,346,354,398] --> Loop 57 * CEs [128,168,329,369,496,516] --> Loop 58 * CEs [92,144,152,200,299,345,353,397,478,504,508,532] --> Loop 59 * CEs [199,215] --> Loop 60 * CEs [322] --> Loop 61 * CEs [91,107,143,167] --> Loop 62 * CEs [115,183,231,298,314,344,368,384,396,412,428] --> Loop 63 * CEs [320] --> Loop 64 * CEs [296,312,342,366,382] --> Loop 65 * CEs [141] --> Loop 66 * CEs [195,211] --> Loop 67 * CEs [87,103,139,163] --> Loop 68 * CEs [310,408] --> Loop 69 * CEs [137] --> Loop 70 * CEs [308] --> Loop 71 * CEs [63,274,457] --> Loop 72 * CEs [62,273,456] --> Loop 73 * CEs [61,272,455] --> Loop 74 * CEs [60,271,454] --> Loop 75 * CEs [67,71,83,90,106,114,142,166,182,198,214,230,278,282,290,297,313,321,343,367,383,395,411,427,461,465,473,477,485,489,503,515,523,531,539,547] --> Loop 76 * CEs [66,70,82,277,281,289,460,464,472] --> Loop 77 * CEs [65,69,81,276,280,288,459,463,471] --> Loop 78 * CEs [68,279,462] --> Loop 79 * CEs [187] --> Loop 80 * CEs [75,119,123] --> Loop 81 * CEs [185] --> Loop 82 * CEs [73,117,121] --> Loop 83 * CEs [191,197] --> Loop 84 * CEs [79,89,105,113,127,165,181,213,229,394,410,426] --> Loop 85 * CEs [189,193] --> Loop 86 * CEs [77,85,101,125,161,209] --> Loop 87 * CEs [57,74,118,122,186,268,284,324,326,386,451,467,491,493,525] --> Loop 88 * CEs [56,72,116,120,184,267,283,323,325,385,450,466,490,492,524] --> Loop 89 * CEs [59,78,88,104,112,126,140,164,180,190,196,212,228,270,286,295,311,319,328,341,365,381,388,393,409,425,453,469,476,484,488,495,502,514,522,527,530,538,546] --> Loop 90 * CEs [58,76,124,188,269,285,327,387,452,468,494,526] --> Loop 91 * CEs [262] --> Loop 92 * CEs [242,250,254] --> Loop 93 * CEs [260] --> Loop 94 * CEs [240,248,252] --> Loop 95 * CEs [266,318] --> Loop 96 * CEs [111,179,227,246,258,294,340,364,380,392,424] --> Loop 97 * CEs [264,316] --> Loop 98 * CEs [109,177,225,244,256,292,338,362,378,390,406,422] --> Loop 99 * CEs [39,43,47,49,53,236,241,249,253,261,433,437,441,443,447] --> Loop 100 * CEs [38,235,432] --> Loop 101 * CEs [41,45,51,55,86,102,110,138,162,178,194,210,226,238,245,257,265,293,309,317,339,363,379,391,407,423,435,439,445,449,475,483,487,501,513,521,529,537,545] --> Loop 102 * CEs [40,64,80,237,275,287,434,458,470] --> Loop 103 * CEs [35,36,42,46,48,52,232,233,239,247,251,259,429,430,436,440,442,446] --> Loop 104 * CEs [37,44,50,54,84,100,108,136,160,176,192,208,224,234,243,255,263,291,307,315,337,361,377,389,405,421,431,438,444,448,474,482,486,500,512,520,528,536,544] --> Loop 105 * CEs [34] --> Loop 106 ### Ranking functions of CR fun1(V1,V,V4,V8,Out) * RF of phase [28,29]: [V-1,V-V8,V4-1,V4-V8] * RF of phase [72]: [V,V4] #### Partial ranking functions of CR fun1(V1,V,V4,V8,Out) * Partial RF of phase [28,29]: - RF of loop [28:1,29:1]: V-1 V-V8 V4-1 V4-V8 * Partial RF of phase [72]: - RF of loop [72:1]: V V4 ### Specialization of cost equations start/4 * CE 1 is refined into CE [548,549] * CE 2 is refined into CE [550,551,552,553,554,555,556,557,558,559,560,561,562,563,564,565,566,567,568] * CE 3 is refined into CE [569,570,571,572] * CE 4 is refined into CE [573,574,575,576,577] * CE 5 is refined into CE [578,579] ### Cost equations --> "Loop" of start/4 * CEs [571] --> Loop 107 * CEs [574] --> Loop 108 * CEs [563] --> Loop 109 * CEs [564,565] --> Loop 110 * CEs [557] --> Loop 111 * CEs [552,555,556,558,559] --> Loop 112 * CEs [550,551,553,554,560,561,562,566,567] --> Loop 113 * CEs [570] --> Loop 114 * CEs [569] --> Loop 115 * CEs [548,549,568,572,573,575,576,577,578,579] --> Loop 116 ### Ranking functions of CR start(V1,V,V4,V8) #### Partial ranking functions of CR start(V1,V,V4,V8) Computing Bounds ===================================== #### Cost of chains of and(V1,V,Out): * Chain [19]: 0 with precondition: [V1=1,Out=1,V>=0] * Chain [18]: 0 with precondition: [V1=2,V=2,Out=2] * Chain [17]: 0 with precondition: [V=1,Out=1,V1>=0] * Chain [16]: 0 with precondition: [Out=0,V1>=0,V>=0] #### Cost of chains of fun(V1,V,Out): * Chain [[20],21]: 1*it(20)+0 Such that:it(20) =< Out with precondition: [Out>=1,V1>=Out,V>=Out] * Chain [21]: 0 with precondition: [Out=0,V1>=0,V>=0] #### Cost of chains of gr(V1,V,Out): * Chain [[22],25]: 0 with precondition: [Out=1,V1>=1,V>=V1] * Chain [[22],24]: 0 with precondition: [Out=2,V>=1,V1>=V+1] * Chain [[22],23]: 0 with precondition: [Out=0,V1>=1,V>=1] * Chain [25]: 0 with precondition: [V1=0,Out=1,V>=0] * Chain [24]: 0 with precondition: [V=0,Out=2,V1>=1] * Chain [23]: 0 with precondition: [Out=0,V1>=0,V>=0] #### Cost of chains of p(V1,Out): * Chain [27]: 0 with precondition: [Out=0,V1>=0] * Chain [26]: 0 with precondition: [V1=Out+1,V1>=1] #### Cost of chains of fun1(V1,V,V4,V8,Out): * Chain [[72],106]: 1*it(72)+0 Such that:it(72) =< Out with precondition: [V1=2,V8=0,Out>=1,V>=Out,V4>=Out] * Chain [[72],105,106]: 1*it(72)+1 Such that:it(72) =< Out with precondition: [V1=2,V8=0,Out>=2,V+1>=Out,V4+1>=Out] * Chain [[72],104,106]: 1*it(72)+1 Such that:it(72) =< Out with precondition: [V1=2,V8=0,V+1=Out,V>=1,V4>=V] * Chain [[72],103,106]: 1*it(72)+1 Such that:it(72) =< Out with precondition: [V1=2,V8=0,Out>=2,V+1>=Out,V4>=Out] * Chain [[72],102,106]: 1*it(72)+1 Such that:it(72) =< Out with precondition: [V1=2,V8=0,Out>=2,V+1>=Out,V4>=Out] * Chain [[72],101,106]: 1*it(72)+1 Such that:it(72) =< Out with precondition: [V1=2,V8=0,V+1=Out,V>=1,V4>=V+1] * Chain [[72],100,106]: 1*it(72)+1 Such that:it(72) =< Out with precondition: [V1=2,V8=0,V+1=Out,V>=1,V4>=V+1] * Chain [[72],91,106]: 1*it(72)+1 Such that:it(72) =< Out with precondition: [V1=2,V8=0,V4+1=Out,V4>=1,V>=V4] * Chain [[72],90,106]: 1*it(72)+1 Such that:it(72) =< Out with precondition: [V1=2,V8=0,Out>=2,V>=Out,V4+1>=Out] * Chain [[72],89,106]: 1*it(72)+1 Such that:it(72) =< Out with precondition: [V1=2,V8=0,V4+1=Out,V4>=1,V>=V4] * Chain [[72],88,106]: 1*it(72)+1 Such that:it(72) =< Out with precondition: [V1=2,V8=0,V4+1=Out,V4>=1,V>=V4+1] * Chain [[72],79,106]: 1*it(72)+1 Such that:it(72) =< Out with precondition: [V1=2,V8=0,Out>=2,V>=Out,V4+1>=Out] * Chain [[72],78,106]: 1*it(72)+1 Such that:it(72) =< Out with precondition: [V1=2,V8=0,Out>=2,V+1>=Out,V4>=Out] * Chain [[72],77,106]: 1*it(72)+1 Such that:it(72) =< Out with precondition: [V1=2,V8=0,Out>=2,V>=Out,V4+1>=Out] * Chain [[72],76,106]: 1*it(72)+1 Such that:it(72) =< Out with precondition: [V1=2,V8=0,Out>=2,V>=Out,V4>=Out] * Chain [[72],75,106]: 1*it(72)+1 Such that:it(72) =< Out with precondition: [V1=2,V8=0,Out>=2,V>=Out,V4>=Out] * Chain [[72],75,105,106]: 1*it(72)+2 Such that:it(72) =< Out with precondition: [V1=2,V8=0,Out>=3,V+1>=Out,V4+1>=Out] * Chain [[72],75,104,106]: 1*it(72)+2 Such that:it(72) =< Out with precondition: [V1=2,V8=0,Out>=3,V+1>=Out,V4+1>=Out] * Chain [[72],75,91,106]: 1*it(72)+2 Such that:it(72) =< Out with precondition: [V1=2,V8=0,Out>=3,V+1>=Out,V4+1>=Out] * Chain [[72],75,89,106]: 1*it(72)+2 Such that:it(72) =< Out with precondition: [V1=2,V8=0,Out>=3,V+1>=Out,V4+1>=Out] * Chain [[72],74,106]: 1*it(72)+1 Such that:it(72) =< Out with precondition: [V1=2,V8=0,Out>=2,V>=Out,V4>=Out] * Chain [[72],74,105,106]: 1*it(72)+2 Such that:it(72) =< Out with precondition: [V1=2,V8=0,Out>=3,V+1>=Out,V4+1>=Out] * Chain [[72],74,104,106]: 1*it(72)+2 Such that:it(72) =< Out with precondition: [V1=2,V8=0,Out>=3,V+1>=Out,V4+1>=Out] * Chain [[72],74,103,106]: 1*it(72)+2 Such that:it(72) =< Out with precondition: [V1=2,V8=0,Out>=3,V+1>=Out,V4>=Out] * Chain [[72],74,102,106]: 1*it(72)+2 Such that:it(72) =< Out with precondition: [V1=2,V8=0,Out>=3,V+1>=Out,V4>=Out] * Chain [[72],74,101,106]: 1*it(72)+2 Such that:it(72) =< Out with precondition: [V1=2,V8=0,Out>=3,V+1>=Out,V4>=Out] * Chain [[72],74,100,106]: 1*it(72)+2 Such that:it(72) =< Out with precondition: [V1=2,V8=0,Out>=3,V+1>=Out,V4>=Out] * Chain [[72],74,91,106]: 1*it(72)+2 Such that:it(72) =< Out with precondition: [V1=2,V8=0,V4+1=Out,V4>=2,V>=V4] * Chain [[72],74,89,106]: 1*it(72)+2 Such that:it(72) =< Out with precondition: [V1=2,V8=0,V4+1=Out,V4>=2,V>=V4] * Chain [[72],74,78,106]: 1*it(72)+2 Such that:it(72) =< Out with precondition: [V1=2,V8=0,Out>=3,V+1>=Out,V4>=Out] * Chain [[72],73,106]: 1*it(72)+1 Such that:it(72) =< Out with precondition: [V1=2,V8=0,Out>=2,V>=Out,V4>=Out] * Chain [[72],73,105,106]: 1*it(72)+2 Such that:it(72) =< Out with precondition: [V1=2,V8=0,Out>=3,V+1>=Out,V4+1>=Out] * Chain [[72],73,104,106]: 1*it(72)+2 Such that:it(72) =< Out with precondition: [V1=2,V8=0,V+1=Out,V>=2,V4>=V] * Chain [[72],73,91,106]: 1*it(72)+2 Such that:it(72) =< Out with precondition: [V1=2,V8=0,Out>=3,V+1>=Out,V4+1>=Out] * Chain [[72],73,90,106]: 1*it(72)+2 Such that:it(72) =< Out with precondition: [V1=2,V8=0,Out>=3,V>=Out,V4+1>=Out] * Chain [[72],73,89,106]: 1*it(72)+2 Such that:it(72) =< Out with precondition: [V1=2,V8=0,Out>=3,V+1>=Out,V4+1>=Out] * Chain [[72],73,88,106]: 1*it(72)+2 Such that:it(72) =< Out with precondition: [V1=2,V8=0,Out>=3,V>=Out,V4+1>=Out] * Chain [[72],73,79,106]: 1*it(72)+2 Such that:it(72) =< Out with precondition: [V1=2,V8=0,Out>=3,V>=Out,V4+1>=Out] * Chain [[72],73,77,106]: 1*it(72)+2 Such that:it(72) =< Out with precondition: [V1=2,V8=0,Out>=3,V>=Out,V4+1>=Out] * Chain [[28,29],106]: 2*it(28)+2*s(5)+0 Such that:aux(3) =< V aux(4) =< V-V8 aux(7) =< V4 aux(2) =< V8 aux(11) =< V4-V8 it(28) =< aux(3) it(28) =< aux(4) it(28) =< aux(11) it(28) =< aux(7) s(6) =< it(28)*aux(2) s(5) =< s(6) with precondition: [V1=2,V8>=1,Out>=1,V>=V8+1,V4>=V8+1] * Chain [[28,29],105,106]: 2*it(28)+2*s(5)+1 Such that:aux(3) =< V aux(4) =< V-V8 aux(7) =< V4 aux(2) =< V8 aux(12) =< V4-V8 it(28) =< aux(3) it(28) =< aux(4) it(28) =< aux(12) it(28) =< aux(7) s(6) =< it(28)*aux(2) s(5) =< s(6) with precondition: [V1=2,V8>=1,Out>=2,V>=V8+1,V4>=V8+1] * Chain [[28,29],102,106]: 2*it(28)+2*s(5)+1 Such that:aux(3) =< V aux(4) =< V-V8 aux(7) =< V4 aux(2) =< V8 aux(13) =< V4-V8 it(28) =< aux(3) it(28) =< aux(4) it(28) =< aux(13) it(28) =< aux(7) s(6) =< it(28)*aux(2) s(5) =< s(6) with precondition: [V1=2,V8>=1,Out>=2,V>=V8+1,V4>=V8+1] * Chain [[28,29],99,106]: 2*it(28)+2*s(5)+2*s(7)+3*s(9)+7*s(10)+1 Such that:aux(4) =< V-V8 aux(8) =< V4-V8 aux(17) =< V aux(18) =< V4 aux(19) =< V8 s(7) =< aux(17) s(10) =< aux(18) s(9) =< aux(19) it(28) =< aux(17) it(28) =< aux(4) it(28) =< aux(18) it(28) =< aux(8) s(6) =< it(28)*aux(19) s(5) =< s(6) with precondition: [V1=2,V8>=1,Out>=3,V>=V8+1,V4>=V8+1] * Chain [[28,29],98,106]: 2*it(28)+2*s(5)+2*s(19)+1 Such that:aux(3) =< V aux(7) =< V4 aux(8) =< V4-V8 aux(21) =< V-V8 aux(22) =< V8 s(19) =< aux(22) it(28) =< aux(3) it(28) =< aux(21) it(28) =< aux(7) it(28) =< aux(8) s(6) =< it(28)*aux(22) s(5) =< s(6) with precondition: [V1=2,V8>=1,Out>=3,V>=V8+1,V4>=V8+2] * Chain [[28,29],97,106]: 2*it(28)+2*s(5)+2*s(21)+5*s(23)+4*s(25)+1 Such that:aux(4) =< V-V8 aux(8) =< V4-V8 aux(27) =< V aux(28) =< V4 aux(29) =< V8 s(25) =< aux(28) s(21) =< aux(27) s(23) =< aux(29) it(28) =< aux(27) it(28) =< aux(4) it(28) =< aux(28) it(28) =< aux(8) s(6) =< it(28)*aux(29) s(5) =< s(6) with precondition: [V1=2,V8>=1,Out>=3,V>=V8+1,V4>=V8+1] * Chain [[28,29],96,106]: 2*it(28)+2*s(5)+2*s(32)+1 Such that:aux(3) =< V aux(7) =< V4 aux(8) =< V4-V8 aux(31) =< V-V8 aux(32) =< V8 s(32) =< aux(32) it(28) =< aux(3) it(28) =< aux(31) it(28) =< aux(7) it(28) =< aux(8) s(6) =< it(28)*aux(32) s(5) =< s(6) with precondition: [V1=2,V8>=1,Out>=3,V>=V8+1,V4>=V8+2] * Chain [[28,29],90,106]: 2*it(28)+2*s(5)+1 Such that:aux(3) =< V aux(4) =< V-V8 aux(7) =< V4 aux(2) =< V8 aux(33) =< V4-V8 it(28) =< aux(3) it(28) =< aux(4) it(28) =< aux(33) it(28) =< aux(7) s(6) =< it(28)*aux(2) s(5) =< s(6) with precondition: [V1=2,V8>=1,Out>=2,V>=V8+1,V4>=V8+1] * Chain [[28,29],87,106]: 2*it(28)+2*s(5)+5*s(34)+1*s(39)+1 Such that:aux(4) =< V-V8 aux(7) =< V4 aux(8) =< V4-V8 aux(35) =< V aux(36) =< V8 s(39) =< aux(36) s(34) =< aux(35) it(28) =< aux(35) it(28) =< aux(4) it(28) =< aux(7) it(28) =< aux(8) s(6) =< it(28)*aux(36) s(5) =< s(6) with precondition: [V1=2,V8>=1,Out>=3,V>=V8+1,V4>=V8+1] * Chain [[28,29],86,106]: 2*it(28)+2*s(5)+2*s(40)+1 Such that:aux(3) =< V aux(7) =< V4 aux(8) =< V4-V8 aux(38) =< V-V8 aux(39) =< V8 s(40) =< aux(39) it(28) =< aux(3) it(28) =< aux(38) it(28) =< aux(7) it(28) =< aux(8) s(6) =< it(28)*aux(39) s(5) =< s(6) with precondition: [V1=2,V8>=1,Out>=3,V>=V8+2,V4>=V8+1] * Chain [[28,29],85,106]: 2*it(28)+2*s(5)+7*s(42)+3*s(49)+2*s(51)+1 Such that:aux(4) =< V-V8 aux(8) =< V4-V8 aux(45) =< V aux(46) =< V4 aux(47) =< V8 s(42) =< aux(45) s(51) =< aux(46) s(49) =< aux(47) it(28) =< aux(45) it(28) =< aux(4) it(28) =< aux(46) it(28) =< aux(8) s(6) =< it(28)*aux(47) s(5) =< s(6) with precondition: [V1=2,V8>=1,Out>=3,V>=V8+1,V4>=V8+1] * Chain [[28,29],84,106]: 2*it(28)+2*s(5)+2*s(54)+1 Such that:aux(3) =< V aux(7) =< V4 aux(8) =< V4-V8 aux(49) =< V-V8 aux(50) =< V8 s(54) =< aux(50) it(28) =< aux(3) it(28) =< aux(49) it(28) =< aux(7) it(28) =< aux(8) s(6) =< it(28)*aux(50) s(5) =< s(6) with precondition: [V1=2,V8>=1,Out>=3,V>=V8+2,V4>=V8+1] * Chain [[28,29],76,106]: 2*it(28)+2*s(5)+1 Such that:aux(3) =< V aux(4) =< V-V8 aux(7) =< V4 aux(2) =< V8 aux(51) =< V4-V8 it(28) =< aux(3) it(28) =< aux(4) it(28) =< aux(51) it(28) =< aux(7) s(6) =< it(28)*aux(2) s(5) =< s(6) with precondition: [V1=2,V8>=1,Out>=2,V>=V8+1,V4>=V8+1] * Chain [[28,29],71,106]: 2*it(28)+2*s(5)+1*s(56)+1 Such that:aux(3) =< V aux(4) =< V-V8 aux(7) =< V4 aux(52) =< V4-V8 aux(53) =< V8 s(56) =< aux(53) it(28) =< aux(3) it(28) =< aux(4) it(28) =< aux(52) it(28) =< aux(7) s(6) =< it(28)*aux(53) s(5) =< s(6) with precondition: [V1=2,V8>=1,V>=V4,V4>=V8+1,Out+V8>=V4+2] * Chain [[28,29],70,106]: 2*it(28)+2*s(5)+1*s(57)+1 Such that:aux(3) =< V aux(7) =< V4 aux(8) =< V4-V8 aux(54) =< V-V8 aux(55) =< V8 s(57) =< aux(55) it(28) =< aux(3) it(28) =< aux(54) it(28) =< aux(7) it(28) =< aux(8) s(6) =< it(28)*aux(55) s(5) =< s(6) with precondition: [V1=2,V8>=1,V4>=V,V>=V8+1,Out+V8>=V+2] * Chain [[28,29],69,106]: 2*it(28)+2*s(5)+2*s(58)+1 Such that:aux(3) =< V aux(4) =< V-V8 aux(7) =< V4 aux(57) =< V4-V8 aux(58) =< V8 s(58) =< aux(58) it(28) =< aux(3) it(28) =< aux(4) it(28) =< aux(57) it(28) =< aux(7) s(6) =< it(28)*aux(58) s(5) =< s(6) with precondition: [V1=2,V8>=1,V>=V4,V4>=V8+1,Out+V8>=V4+2] * Chain [[28,29],68,106]: 2*it(28)+2*s(5)+4*s(60)+1 Such that:aux(4) =< V-V8 aux(7) =< V4 aux(8) =< V4-V8 aux(2) =< V8 aux(60) =< V s(60) =< aux(60) it(28) =< aux(60) it(28) =< aux(4) it(28) =< aux(7) it(28) =< aux(8) s(6) =< it(28)*aux(2) s(5) =< s(6) with precondition: [V1=2,V8>=1,Out>=3,V>=V8+1,V4>=V8+1] * Chain [[28,29],67,106]: 2*it(28)+2*s(5)+2*s(64)+1 Such that:aux(3) =< V aux(7) =< V4 aux(8) =< V4-V8 aux(62) =< V-V8 aux(63) =< V8 s(64) =< aux(63) it(28) =< aux(3) it(28) =< aux(62) it(28) =< aux(7) it(28) =< aux(8) s(6) =< it(28)*aux(63) s(5) =< s(6) with precondition: [V1=2,V8>=1,Out>=3,V>=V8+2,V4>=V8+1] * Chain [[28,29],66,106]: 2*it(28)+2*s(5)+1*s(66)+1 Such that:aux(3) =< V aux(7) =< V4 aux(8) =< V4-V8 aux(64) =< V-V8 aux(65) =< V8 s(66) =< aux(65) it(28) =< aux(3) it(28) =< aux(64) it(28) =< aux(7) it(28) =< aux(8) s(6) =< it(28)*aux(65) s(5) =< s(6) with precondition: [V1=2,V8>=1,V4>=V,V>=V8+1,Out+V8>=V+2] * Chain [[28,29],65,106]: 2*it(28)+2*s(5)+4*s(67)+1*s(71)+1 Such that:aux(3) =< V aux(4) =< V-V8 aux(8) =< V4-V8 aux(67) =< V4 aux(68) =< V8 s(71) =< aux(68) s(67) =< aux(67) it(28) =< aux(3) it(28) =< aux(4) it(28) =< aux(67) it(28) =< aux(8) s(6) =< it(28)*aux(68) s(5) =< s(6) with precondition: [V1=2,V8>=1,Out>=3,V>=V8+1,V4>=V8+1] * Chain [[28,29],64,106]: 2*it(28)+2*s(5)+1*s(72)+1 Such that:aux(3) =< V aux(7) =< V4 aux(8) =< V4-V8 aux(69) =< V-V8 aux(70) =< V8 s(72) =< aux(70) it(28) =< aux(3) it(28) =< aux(69) it(28) =< aux(7) it(28) =< aux(8) s(6) =< it(28)*aux(70) s(5) =< s(6) with precondition: [V1=2,V8>=1,Out>=3,V>=V8+1,V4>=V8+2] * Chain [[28,29],63,106]: 2*it(28)+2*s(5)+2*s(73)+4*s(75)+5*s(77)+1 Such that:aux(4) =< V-V8 aux(8) =< V4-V8 aux(75) =< V aux(76) =< V4 aux(77) =< V8 s(77) =< aux(76) s(73) =< aux(75) s(75) =< aux(77) it(28) =< aux(75) it(28) =< aux(4) it(28) =< aux(76) it(28) =< aux(8) s(6) =< it(28)*aux(77) s(5) =< s(6) with precondition: [V1=2,V8>=1,Out>=3,V>=V8+1,V4>=V8+1] * Chain [[28,29],62,106]: 2*it(28)+2*s(5)+1*s(84)+3*s(85)+1 Such that:aux(4) =< V-V8 aux(7) =< V4 aux(8) =< V4-V8 aux(79) =< V aux(80) =< V8 s(84) =< aux(80) s(85) =< aux(79) it(28) =< aux(79) it(28) =< aux(4) it(28) =< aux(7) it(28) =< aux(8) s(6) =< it(28)*aux(80) s(5) =< s(6) with precondition: [V1=2,V8>=1,Out>=3,V>=V8+1,V4>=V8+1] * Chain [[28,29],61,106]: 2*it(28)+2*s(5)+1*s(88)+1 Such that:aux(3) =< V aux(7) =< V4 aux(8) =< V4-V8 aux(81) =< V-V8 aux(82) =< V8 s(88) =< aux(82) it(28) =< aux(3) it(28) =< aux(81) it(28) =< aux(7) it(28) =< aux(8) s(6) =< it(28)*aux(82) s(5) =< s(6) with precondition: [V1=2,V8>=1,Out>=3,V>=V8+1,V4>=V8+2] * Chain [[28,29],60,106]: 2*it(28)+2*s(5)+2*s(89)+1 Such that:aux(3) =< V aux(7) =< V4 aux(8) =< V4-V8 aux(84) =< V-V8 aux(85) =< V8 s(89) =< aux(85) it(28) =< aux(3) it(28) =< aux(84) it(28) =< aux(7) it(28) =< aux(8) s(6) =< it(28)*aux(85) s(5) =< s(6) with precondition: [V1=2,V8>=1,Out>=3,V>=V8+2,V4>=V8+1] * Chain [[28,29],59,106]: 2*it(28)+2*s(5)+1 Such that:aux(3) =< V aux(4) =< V-V8 aux(7) =< V4 aux(2) =< V8 aux(86) =< V4-V8 it(28) =< aux(3) it(28) =< aux(4) it(28) =< aux(86) it(28) =< aux(7) s(6) =< it(28)*aux(2) s(5) =< s(6) with precondition: [V1=2,V8>=1,V>=V4,V4>=V8+1,Out+V8>=V4+1] * Chain [[28,29],58,106]: 2*it(28)+2*s(5)+1 Such that:aux(3) =< V aux(7) =< V4 aux(8) =< V4-V8 aux(2) =< V8 aux(87) =< V-V8 it(28) =< aux(3) it(28) =< aux(87) it(28) =< aux(7) it(28) =< aux(8) s(6) =< it(28)*aux(2) s(5) =< s(6) with precondition: [V1=2,V8>=1,V4>=V,V>=V8+1,Out+V8>=V+1] * Chain [[28,29],57,106]: 2*it(28)+2*s(5)+4*s(91)+1 Such that:aux(3) =< V aux(4) =< V-V8 aux(7) =< V4 aux(89) =< V4-V8 aux(90) =< V8 s(91) =< aux(90) it(28) =< aux(3) it(28) =< aux(4) it(28) =< aux(89) it(28) =< aux(7) s(6) =< it(28)*aux(90) s(5) =< s(6) with precondition: [V1=2,V8>=1,V>=V4,V4>=V8+1,Out+V8>=V4+2] * Chain [[28,29],56,106]: 2*it(28)+2*s(5)+2*s(95)+1*s(96)+1 Such that:s(96) =< -V+V4+V8 aux(3) =< V aux(7) =< V4 aux(8) =< V4-V8 aux(91) =< V-V8 aux(92) =< V8 s(95) =< aux(92) it(28) =< aux(3) it(28) =< aux(91) it(28) =< aux(7) it(28) =< aux(8) s(6) =< it(28)*aux(92) s(5) =< s(6) with precondition: [V1=2,V8>=1,V4>=V,V>=V8+1,Out+V8>=V+2] * Chain [[28,29],55,106]: 2*it(28)+2*s(5)+3*s(98)+1 Such that:aux(3) =< V aux(7) =< V4 aux(8) =< V4-V8 aux(94) =< V-V8 aux(95) =< V8 s(98) =< aux(95) it(28) =< aux(3) it(28) =< aux(94) it(28) =< aux(7) it(28) =< aux(8) s(6) =< it(28)*aux(95) s(5) =< s(6) with precondition: [V1=2,V8>=1,V4>=V,V>=V8+1,Out+V8>=V+2] * Chain [[28,29],54,106]: 2*it(28)+2*s(5)+1*s(101)+1*s(102)+1 Such that:aux(3) =< V s(101) =< V-V4+V8 aux(4) =< V-V8 aux(7) =< V4 aux(96) =< V4-V8 aux(97) =< V8 s(102) =< aux(97) it(28) =< aux(3) it(28) =< aux(4) it(28) =< aux(96) it(28) =< aux(7) s(6) =< it(28)*aux(97) s(5) =< s(6) with precondition: [V1=2,V8>=1,V>=V4,V4>=V8+1,Out+V8>=V4+2] * Chain [[28,29],53,106]: 2*it(28)+2*s(5)+1 Such that:aux(3) =< V aux(4) =< V-V8 aux(7) =< V4 aux(2) =< V8 aux(98) =< V4-V8 it(28) =< aux(3) it(28) =< aux(4) it(28) =< aux(98) it(28) =< aux(7) s(6) =< it(28)*aux(2) s(5) =< s(6) with precondition: [V1=2,V8>=1,V>=V4,V4>=V8+1,Out+V8>=V4+1] * Chain [[28,29],52,106]: 2*it(28)+2*s(5)+1 Such that:aux(3) =< V aux(7) =< V4 aux(8) =< V4-V8 aux(2) =< V8 aux(99) =< V-V8 it(28) =< aux(3) it(28) =< aux(99) it(28) =< aux(7) it(28) =< aux(8) s(6) =< it(28)*aux(2) s(5) =< s(6) with precondition: [V1=2,V8>=1,V4>=V,V>=V8+1,Out+V8>=V+1] * Chain [[28,29],51,106]: 2*it(28)+2*s(5)+4*s(103)+1 Such that:aux(3) =< V aux(4) =< V-V8 aux(7) =< V4 aux(101) =< V4-V8 aux(102) =< V8 s(103) =< aux(102) it(28) =< aux(3) it(28) =< aux(4) it(28) =< aux(101) it(28) =< aux(7) s(6) =< it(28)*aux(102) s(5) =< s(6) with precondition: [V1=2,V8>=1,V>=V4,V4>=V8+1,Out+V8>=V4+2] * Chain [[28,29],50,106]: 2*it(28)+2*s(5)+4*s(107)+1 Such that:aux(3) =< V aux(7) =< V4 aux(8) =< V4-V8 aux(104) =< V-V8 aux(105) =< V8 s(107) =< aux(105) it(28) =< aux(3) it(28) =< aux(104) it(28) =< aux(7) it(28) =< aux(8) s(6) =< it(28)*aux(105) s(5) =< s(6) with precondition: [V1=2,V8>=1,V4>=V,V>=V8+1,Out+V8>=V+2] * Chain [[28,29],49,106]: 2*it(28)+2*s(5)+1*s(111)+1*s(112)+1 Such that:aux(3) =< V s(111) =< V-V4+V8 aux(4) =< V-V8 aux(7) =< V4 aux(106) =< V4-V8 aux(107) =< V8 s(112) =< aux(107) it(28) =< aux(3) it(28) =< aux(4) it(28) =< aux(106) it(28) =< aux(7) s(6) =< it(28)*aux(107) s(5) =< s(6) with precondition: [V1=2,V8>=1,V>=V4,V4>=V8+1,Out+V8>=V4+2] * Chain [[28,29],48,106]: 2*it(28)+2*s(5)+1*s(113)+1*s(114)+1 Such that:s(113) =< -V+V4+V8 aux(3) =< V aux(7) =< V4 aux(8) =< V4-V8 aux(108) =< V-V8 aux(109) =< V8 s(114) =< aux(109) it(28) =< aux(3) it(28) =< aux(108) it(28) =< aux(7) it(28) =< aux(8) s(6) =< it(28)*aux(109) s(5) =< s(6) with precondition: [V1=2,V8>=1,V4>=V,V>=V8+1,Out+V8>=V+2] * Chain [[28,29],47,106]: 2*it(28)+2*s(5)+1 Such that:aux(3) =< V aux(7) =< V4 aux(8) =< V4-V8 aux(2) =< V8 aux(110) =< V-V8 it(28) =< aux(3) it(28) =< aux(110) it(28) =< aux(7) it(28) =< aux(8) s(6) =< it(28)*aux(2) s(5) =< s(6) with precondition: [V1=2,V8>=1,V4>=V,V>=V8+1,Out+V8>=V+1] * Chain [[28,29],46,106]: 2*it(28)+2*s(5)+1 Such that:aux(3) =< V aux(4) =< V-V8 aux(7) =< V4 aux(2) =< V8 aux(111) =< V4-V8 it(28) =< aux(3) it(28) =< aux(4) it(28) =< aux(111) it(28) =< aux(7) s(6) =< it(28)*aux(2) s(5) =< s(6) with precondition: [V1=2,V8>=1,V>=V4,V4>=V8+1,Out+V8>=V4+1] * Chain [[28,29],45,106]: 2*it(28)+2*s(5)+4*s(115)+1 Such that:aux(3) =< V aux(7) =< V4 aux(8) =< V4-V8 aux(114) =< V-V8 aux(115) =< V8 s(115) =< aux(115) it(28) =< aux(3) it(28) =< aux(114) it(28) =< aux(7) it(28) =< aux(8) s(6) =< it(28)*aux(115) s(5) =< s(6) with precondition: [V1=2,V8>=1,V4>=V,V>=V8+1,Out+V8>=V+2] * Chain [[28,29],44,106]: 2*it(28)+2*s(5)+4*s(119)+1 Such that:aux(3) =< V aux(4) =< V-V8 aux(7) =< V4 aux(117) =< V4-V8 aux(118) =< V8 s(119) =< aux(118) it(28) =< aux(3) it(28) =< aux(4) it(28) =< aux(117) it(28) =< aux(7) s(6) =< it(28)*aux(118) s(5) =< s(6) with precondition: [V1=2,V8>=1,V>=V4,V4>=V8+1,Out+V8>=V4+2] * Chain [[28,29],43,106]: 2*it(28)+2*s(5)+1*s(123)+1*s(124)+1 Such that:s(123) =< -V+V4+V8 aux(3) =< V aux(7) =< V4 aux(8) =< V4-V8 aux(119) =< V-V8 aux(120) =< V8 s(124) =< aux(120) it(28) =< aux(3) it(28) =< aux(119) it(28) =< aux(7) it(28) =< aux(8) s(6) =< it(28)*aux(120) s(5) =< s(6) with precondition: [V1=2,V8>=1,V4>=V,V>=V8+1,Out+V8>=V+2] * Chain [[28,29],42,106]: 2*it(28)+2*s(5)+1*s(125)+1*s(126)+1 Such that:aux(3) =< V s(125) =< V-V4+V8 aux(4) =< V-V8 aux(7) =< V4 aux(121) =< V4-V8 aux(122) =< V8 s(126) =< aux(122) it(28) =< aux(3) it(28) =< aux(4) it(28) =< aux(121) it(28) =< aux(7) s(6) =< it(28)*aux(122) s(5) =< s(6) with precondition: [V1=2,V8>=1,V>=V4,V4>=V8+1,Out+V8>=V4+2] * Chain [[28,29],41,106]: 2*it(28)+2*s(5)+1 Such that:aux(3) =< V aux(7) =< V4 aux(8) =< V4-V8 aux(2) =< V8 aux(123) =< V-V8 it(28) =< aux(3) it(28) =< aux(123) it(28) =< aux(7) it(28) =< aux(8) s(6) =< it(28)*aux(2) s(5) =< s(6) with precondition: [V1=2,V8>=1,V4>=V,V>=V8+1,Out+V8>=V+1] * Chain [[28,29],40,106]: 2*it(28)+2*s(5)+1 Such that:aux(3) =< V aux(4) =< V-V8 aux(7) =< V4 aux(2) =< V8 aux(124) =< V4-V8 it(28) =< aux(3) it(28) =< aux(4) it(28) =< aux(124) it(28) =< aux(7) s(6) =< it(28)*aux(2) s(5) =< s(6) with precondition: [V1=2,V8>=1,V>=V4,V4>=V8+1,Out+V8>=V4+1] * Chain [[28,29],39,106]: 2*it(28)+2*s(5)+4*s(127)+1 Such that:aux(3) =< V aux(4) =< V-V8 aux(7) =< V4 aux(126) =< V4-V8 aux(127) =< V8 s(127) =< aux(127) it(28) =< aux(3) it(28) =< aux(4) it(28) =< aux(126) it(28) =< aux(7) s(6) =< it(28)*aux(127) s(5) =< s(6) with precondition: [V1=2,V8>=1,V>=V4,V4>=V8+1,Out+V8>=V4+2] * Chain [[28,29],38,106]: 2*it(28)+2*s(5)+4*s(131)+1 Such that:aux(3) =< V aux(7) =< V4 aux(8) =< V4-V8 aux(129) =< V-V8 aux(130) =< V8 s(131) =< aux(130) it(28) =< aux(3) it(28) =< aux(129) it(28) =< aux(7) it(28) =< aux(8) s(6) =< it(28)*aux(130) s(5) =< s(6) with precondition: [V1=2,V8>=1,V4>=V,V>=V8+1,Out+V8>=V+2] * Chain [[28,29],37,106]: 2*it(28)+2*s(5)+1*s(135)+1*s(136)+1 Such that:aux(3) =< V s(135) =< V-V4+V8 aux(4) =< V-V8 aux(7) =< V4 aux(131) =< V4-V8 aux(132) =< V8 s(136) =< aux(132) it(28) =< aux(3) it(28) =< aux(4) it(28) =< aux(131) it(28) =< aux(7) s(6) =< it(28)*aux(132) s(5) =< s(6) with precondition: [V1=2,V8>=1,V>=V4,V4>=V8+1,Out+V8>=V4+2] * Chain [[28,29],36,106]: 2*it(28)+2*s(5)+1*s(137)+1*s(138)+1 Such that:s(137) =< -V+V4+V8 aux(3) =< V aux(7) =< V4 aux(8) =< V4-V8 aux(133) =< V-V8 aux(134) =< V8 s(138) =< aux(134) it(28) =< aux(3) it(28) =< aux(133) it(28) =< aux(7) it(28) =< aux(8) s(6) =< it(28)*aux(134) s(5) =< s(6) with precondition: [V1=2,V8>=1,V4>=V,V>=V8+1,Out+V8>=V+2] * Chain [[28,29],35,106]: 2*it(28)+2*s(5)+1 Such that:aux(3) =< V aux(4) =< V-V8 aux(7) =< V4 aux(2) =< V8 aux(135) =< V4-V8 it(28) =< aux(3) it(28) =< aux(4) it(28) =< aux(135) it(28) =< aux(7) s(6) =< it(28)*aux(2) s(5) =< s(6) with precondition: [V1=2,V8>=1,Out>=2,V>=V8+2,V4>=V8+2] * Chain [[28,29],35,105,106]: 2*it(28)+2*s(5)+2 Such that:aux(3) =< V aux(4) =< V-V8 aux(7) =< V4 aux(2) =< V8 aux(136) =< V4-V8 it(28) =< aux(3) it(28) =< aux(4) it(28) =< aux(136) it(28) =< aux(7) s(6) =< it(28)*aux(2) s(5) =< s(6) with precondition: [V1=2,V8>=1,Out>=3,V>=V8+2,V4>=V8+2] * Chain [[28,29],35,104,106]: 2*it(28)+2*s(5)+2 Such that:aux(3) =< V aux(4) =< V-V8 aux(7) =< V4 aux(2) =< V8 aux(137) =< V4-V8 it(28) =< aux(3) it(28) =< aux(4) it(28) =< aux(137) it(28) =< aux(7) s(6) =< it(28)*aux(2) s(5) =< s(6) with precondition: [V1=2,V8>=1,Out>=3,V>=V8+2,V4>=V8+2] * Chain [[28,29],35,91,106]: 2*it(28)+2*s(5)+2 Such that:aux(3) =< V aux(4) =< V-V8 aux(7) =< V4 aux(2) =< V8 aux(138) =< V4-V8 it(28) =< aux(3) it(28) =< aux(4) it(28) =< aux(138) it(28) =< aux(7) s(6) =< it(28)*aux(2) s(5) =< s(6) with precondition: [V1=2,V8>=1,Out>=3,V>=V8+2,V4>=V8+2] * Chain [[28,29],35,89,106]: 2*it(28)+2*s(5)+2 Such that:aux(3) =< V aux(4) =< V-V8 aux(7) =< V4 aux(2) =< V8 aux(139) =< V4-V8 it(28) =< aux(3) it(28) =< aux(4) it(28) =< aux(139) it(28) =< aux(7) s(6) =< it(28)*aux(2) s(5) =< s(6) with precondition: [V1=2,V8>=1,Out>=3,V>=V8+2,V4>=V8+2] * Chain [[28,29],34,106]: 2*it(28)+2*s(5)+2*s(139)+1 Such that:aux(3) =< V aux(7) =< V4 aux(8) =< V4-V8 aux(141) =< V-V8 aux(142) =< V8 s(139) =< aux(142) it(28) =< aux(3) it(28) =< aux(141) it(28) =< aux(7) it(28) =< aux(8) s(6) =< it(28)*aux(142) s(5) =< s(6) with precondition: [V1=2,V8>=1,Out>=3,V>=V8+2,V4>=V8+2] * Chain [[28,29],34,105,106]: 2*it(28)+2*s(5)+2*s(139)+2 Such that:aux(3) =< V aux(7) =< V4 aux(8) =< V4-V8 aux(143) =< V-V8 aux(144) =< V8 s(139) =< aux(144) it(28) =< aux(3) it(28) =< aux(143) it(28) =< aux(7) it(28) =< aux(8) s(6) =< it(28)*aux(144) s(5) =< s(6) with precondition: [V1=2,V8>=1,Out>=4,V>=V8+2,V4>=V8+2] * Chain [[28,29],34,104,106]: 2*it(28)+2*s(5)+2*s(139)+2 Such that:aux(3) =< V aux(7) =< V4 aux(8) =< V4-V8 aux(145) =< V-V8 aux(146) =< V8 s(139) =< aux(146) it(28) =< aux(3) it(28) =< aux(145) it(28) =< aux(7) it(28) =< aux(8) s(6) =< it(28)*aux(146) s(5) =< s(6) with precondition: [V1=2,V8>=1,Out>=4,V>=V8+2,V4>=V8+2] * Chain [[28,29],34,91,106]: 2*it(28)+2*s(5)+2*s(139)+2 Such that:aux(3) =< V aux(7) =< V4 aux(8) =< V4-V8 aux(147) =< V-V8 aux(148) =< V8 s(139) =< aux(148) it(28) =< aux(3) it(28) =< aux(147) it(28) =< aux(7) it(28) =< aux(8) s(6) =< it(28)*aux(148) s(5) =< s(6) with precondition: [V1=2,V8>=1,Out>=4,V>=V8+2,V4>=V8+2] * Chain [[28,29],34,89,106]: 2*it(28)+2*s(5)+2*s(139)+2 Such that:aux(3) =< V aux(7) =< V4 aux(8) =< V4-V8 aux(149) =< V-V8 aux(150) =< V8 s(139) =< aux(150) it(28) =< aux(3) it(28) =< aux(149) it(28) =< aux(7) it(28) =< aux(8) s(6) =< it(28)*aux(150) s(5) =< s(6) with precondition: [V1=2,V8>=1,Out>=4,V>=V8+2,V4>=V8+2] * Chain [[28,29],33,106]: 2*it(28)+2*s(5)+1 Such that:aux(3) =< V aux(4) =< V-V8 aux(7) =< V4 aux(2) =< V8 aux(151) =< V4-V8 it(28) =< aux(3) it(28) =< aux(4) it(28) =< aux(151) it(28) =< aux(7) s(6) =< it(28)*aux(2) s(5) =< s(6) with precondition: [V1=2,V8>=1,Out>=2,V>=V8+2,V4>=V8+2] * Chain [[28,29],33,105,106]: 2*it(28)+2*s(5)+2 Such that:aux(3) =< V aux(4) =< V-V8 aux(7) =< V4 aux(2) =< V8 aux(152) =< V4-V8 it(28) =< aux(3) it(28) =< aux(4) it(28) =< aux(152) it(28) =< aux(7) s(6) =< it(28)*aux(2) s(5) =< s(6) with precondition: [V1=2,V8>=1,Out>=3,V>=V8+2,V4>=V8+2] * Chain [[28,29],33,104,106]: 2*it(28)+2*s(5)+2 Such that:aux(3) =< V aux(4) =< V-V8 aux(7) =< V4 aux(2) =< V8 aux(153) =< V4-V8 it(28) =< aux(3) it(28) =< aux(4) it(28) =< aux(153) it(28) =< aux(7) s(6) =< it(28)*aux(2) s(5) =< s(6) with precondition: [V1=2,V8>=1,Out>=3,V>=V8+2,V4>=V8+2] * Chain [[28,29],33,102,106]: 2*it(28)+2*s(5)+2 Such that:aux(3) =< V aux(4) =< V-V8 aux(7) =< V4 aux(2) =< V8 aux(154) =< V4-V8 it(28) =< aux(3) it(28) =< aux(4) it(28) =< aux(154) it(28) =< aux(7) s(6) =< it(28)*aux(2) s(5) =< s(6) with precondition: [V1=2,V8>=1,Out>=3,V>=V8+2,V4>=V8+2] * Chain [[28,29],33,100,106]: 2*it(28)+2*s(5)+2 Such that:aux(3) =< V aux(4) =< V-V8 aux(7) =< V4 aux(2) =< V8 aux(155) =< V4-V8 it(28) =< aux(3) it(28) =< aux(4) it(28) =< aux(155) it(28) =< aux(7) s(6) =< it(28)*aux(2) s(5) =< s(6) with precondition: [V1=2,V8>=1,Out>=3,V>=V8+2,V4>=V8+2] * Chain [[28,29],33,99,106]: 2*it(28)+2*s(5)+3*s(9)+7*s(10)+2 Such that:aux(3) =< V aux(4) =< V-V8 aux(8) =< V4-V8 aux(156) =< V4 aux(157) =< V8 s(10) =< aux(156) s(9) =< aux(157) it(28) =< aux(3) it(28) =< aux(4) it(28) =< aux(156) it(28) =< aux(8) s(6) =< it(28)*aux(157) s(5) =< s(6) with precondition: [V1=2,V8>=1,Out>=4,V>=V8+2,V4>=V8+2] * Chain [[28,29],33,98,106]: 2*it(28)+2*s(5)+2*s(19)+2 Such that:aux(3) =< V aux(7) =< V4 aux(8) =< V4-V8 aux(158) =< V-V8 aux(159) =< V8 s(19) =< aux(159) it(28) =< aux(3) it(28) =< aux(158) it(28) =< aux(7) it(28) =< aux(8) s(6) =< it(28)*aux(159) s(5) =< s(6) with precondition: [V1=2,V8>=1,Out>=4,V>=V8+2,V4>=V8+3] * Chain [[28,29],33,97,106]: 2*it(28)+2*s(5)+5*s(23)+4*s(25)+2 Such that:aux(3) =< V aux(4) =< V-V8 aux(8) =< V4-V8 aux(160) =< V4 aux(161) =< V8 s(25) =< aux(160) s(23) =< aux(161) it(28) =< aux(3) it(28) =< aux(4) it(28) =< aux(160) it(28) =< aux(8) s(6) =< it(28)*aux(161) s(5) =< s(6) with precondition: [V1=2,V8>=1,Out>=4,V>=V8+2,V4>=V8+2] * Chain [[28,29],33,96,106]: 2*it(28)+2*s(5)+2*s(32)+2 Such that:aux(3) =< V aux(7) =< V4 aux(8) =< V4-V8 aux(162) =< V-V8 aux(163) =< V8 s(32) =< aux(163) it(28) =< aux(3) it(28) =< aux(162) it(28) =< aux(7) it(28) =< aux(8) s(6) =< it(28)*aux(163) s(5) =< s(6) with precondition: [V1=2,V8>=1,Out>=4,V>=V8+2,V4>=V8+3] * Chain [[28,29],33,95,106]: 2*it(28)+2*s(5)+3*s(141)+2 Such that:aux(3) =< V aux(4) =< V-V8 aux(8) =< V4-V8 aux(2) =< V8 aux(165) =< V4 s(141) =< aux(165) it(28) =< aux(3) it(28) =< aux(4) it(28) =< aux(165) it(28) =< aux(8) s(6) =< it(28)*aux(2) s(5) =< s(6) with precondition: [V1=2,V8>=1,Out>=4,V>=V8+2,V4>=V8+2] * Chain [[28,29],33,94,106]: 2*it(28)+2*s(5)+1*s(144)+2 Such that:aux(3) =< V aux(7) =< V4 aux(8) =< V4-V8 aux(166) =< V-V8 aux(167) =< V8 s(144) =< aux(167) it(28) =< aux(3) it(28) =< aux(166) it(28) =< aux(7) it(28) =< aux(8) s(6) =< it(28)*aux(167) s(5) =< s(6) with precondition: [V1=2,V8>=1,Out>=4,V>=V8+2,V4>=V8+3] * Chain [[28,29],33,93,106]: 2*it(28)+2*s(5)+1*s(145)+2*s(146)+2 Such that:aux(3) =< V aux(4) =< V-V8 aux(8) =< V4-V8 aux(169) =< V4 aux(170) =< V8 s(145) =< aux(170) s(146) =< aux(169) it(28) =< aux(3) it(28) =< aux(4) it(28) =< aux(169) it(28) =< aux(8) s(6) =< it(28)*aux(170) s(5) =< s(6) with precondition: [V1=2,V8>=1,Out>=4,V>=V8+2,V4>=V8+2] * Chain [[28,29],33,92,106]: 2*it(28)+2*s(5)+1*s(148)+2 Such that:aux(3) =< V aux(7) =< V4 aux(8) =< V4-V8 aux(171) =< V-V8 aux(172) =< V8 s(148) =< aux(172) it(28) =< aux(3) it(28) =< aux(171) it(28) =< aux(7) it(28) =< aux(8) s(6) =< it(28)*aux(172) s(5) =< s(6) with precondition: [V1=2,V8>=1,Out>=4,V>=V8+2,V4>=V8+3] * Chain [[28,29],33,71,106]: 2*it(28)+2*s(5)+1*s(56)+2 Such that:aux(3) =< V aux(4) =< V-V8 aux(7) =< V4 aux(173) =< V4-V8 aux(174) =< V8 s(56) =< aux(174) it(28) =< aux(3) it(28) =< aux(4) it(28) =< aux(173) it(28) =< aux(7) s(6) =< it(28)*aux(174) s(5) =< s(6) with precondition: [V1=2,V8>=1,V>=V4,V4>=V8+2,Out+V8>=V4+2] * Chain [[28,29],33,69,106]: 2*it(28)+2*s(5)+2*s(58)+2 Such that:aux(3) =< V aux(4) =< V-V8 aux(7) =< V4 aux(175) =< V4-V8 aux(176) =< V8 s(58) =< aux(176) it(28) =< aux(3) it(28) =< aux(4) it(28) =< aux(175) it(28) =< aux(7) s(6) =< it(28)*aux(176) s(5) =< s(6) with precondition: [V1=2,V8>=1,V>=V4,V4>=V8+2,Out+V8>=V4+2] * Chain [[28,29],33,59,106]: 2*it(28)+2*s(5)+2 Such that:aux(3) =< V aux(4) =< V-V8 aux(7) =< V4 aux(2) =< V8 aux(177) =< V4-V8 it(28) =< aux(3) it(28) =< aux(4) it(28) =< aux(177) it(28) =< aux(7) s(6) =< it(28)*aux(2) s(5) =< s(6) with precondition: [V1=2,V8>=1,V>=V4,V4>=V8+2,Out+V8>=V4+1] * Chain [[28,29],33,57,106]: 2*it(28)+2*s(5)+4*s(91)+2 Such that:aux(3) =< V aux(4) =< V-V8 aux(7) =< V4 aux(178) =< V4-V8 aux(179) =< V8 s(91) =< aux(179) it(28) =< aux(3) it(28) =< aux(4) it(28) =< aux(178) it(28) =< aux(7) s(6) =< it(28)*aux(179) s(5) =< s(6) with precondition: [V1=2,V8>=1,V>=V4,V4>=V8+2,Out+V8>=V4+2] * Chain [[28,29],33,53,106]: 2*it(28)+2*s(5)+2 Such that:aux(3) =< V aux(4) =< V-V8 aux(7) =< V4 aux(2) =< V8 aux(180) =< V4-V8 it(28) =< aux(3) it(28) =< aux(4) it(28) =< aux(180) it(28) =< aux(7) s(6) =< it(28)*aux(2) s(5) =< s(6) with precondition: [V1=2,V8>=1,V>=V4,V4>=V8+2,Out+V8>=V4+1] * Chain [[28,29],33,51,106]: 2*it(28)+2*s(5)+4*s(103)+2 Such that:aux(3) =< V aux(4) =< V-V8 aux(7) =< V4 aux(181) =< V4-V8 aux(182) =< V8 s(103) =< aux(182) it(28) =< aux(3) it(28) =< aux(4) it(28) =< aux(181) it(28) =< aux(7) s(6) =< it(28)*aux(182) s(5) =< s(6) with precondition: [V1=2,V8>=1,V>=V4,V4>=V8+2,Out+V8>=V4+2] * Chain [[28,29],32,106]: 2*it(28)+2*s(5)+2*s(149)+1 Such that:aux(3) =< V aux(7) =< V4 aux(8) =< V4-V8 aux(184) =< V-V8 aux(185) =< V8 s(149) =< aux(185) it(28) =< aux(3) it(28) =< aux(184) it(28) =< aux(7) it(28) =< aux(8) s(6) =< it(28)*aux(185) s(5) =< s(6) with precondition: [V1=2,V8>=1,Out>=3,V>=V8+2,V4>=V8+2] * Chain [[28,29],32,105,106]: 2*it(28)+2*s(5)+2*s(149)+2 Such that:aux(3) =< V aux(7) =< V4 aux(8) =< V4-V8 aux(186) =< V-V8 aux(187) =< V8 s(149) =< aux(187) it(28) =< aux(3) it(28) =< aux(186) it(28) =< aux(7) it(28) =< aux(8) s(6) =< it(28)*aux(187) s(5) =< s(6) with precondition: [V1=2,V8>=1,Out>=4,V>=V8+2,V4>=V8+2] * Chain [[28,29],32,104,106]: 2*it(28)+2*s(5)+2*s(149)+2 Such that:aux(3) =< V aux(7) =< V4 aux(8) =< V4-V8 aux(188) =< V-V8 aux(189) =< V8 s(149) =< aux(189) it(28) =< aux(3) it(28) =< aux(188) it(28) =< aux(7) it(28) =< aux(8) s(6) =< it(28)*aux(189) s(5) =< s(6) with precondition: [V1=2,V8>=1,Out>=4,V>=V8+2,V4>=V8+2] * Chain [[28,29],32,102,106]: 2*it(28)+2*s(5)+2*s(149)+2 Such that:aux(3) =< V aux(7) =< V4 aux(8) =< V4-V8 aux(190) =< V-V8 aux(191) =< V8 s(149) =< aux(191) it(28) =< aux(3) it(28) =< aux(190) it(28) =< aux(7) it(28) =< aux(8) s(6) =< it(28)*aux(191) s(5) =< s(6) with precondition: [V1=2,V8>=1,Out>=4,V>=V8+2,V4>=V8+2] * Chain [[28,29],32,100,106]: 2*it(28)+2*s(5)+2*s(149)+2 Such that:aux(3) =< V aux(7) =< V4 aux(8) =< V4-V8 aux(192) =< V-V8 aux(193) =< V8 s(149) =< aux(193) it(28) =< aux(3) it(28) =< aux(192) it(28) =< aux(7) it(28) =< aux(8) s(6) =< it(28)*aux(193) s(5) =< s(6) with precondition: [V1=2,V8>=1,Out>=4,V>=V8+2,V4>=V8+2] * Chain [[28,29],32,99,106]: 2*it(28)+2*s(5)+5*s(9)+7*s(10)+2 Such that:aux(3) =< V aux(4) =< V-V8 aux(8) =< V4-V8 aux(195) =< V4 aux(196) =< V8 s(10) =< aux(195) s(9) =< aux(196) it(28) =< aux(3) it(28) =< aux(4) it(28) =< aux(195) it(28) =< aux(8) s(6) =< it(28)*aux(196) s(5) =< s(6) with precondition: [V1=2,V8>=1,Out>=5,V>=V8+2,V4>=V8+2] * Chain [[28,29],32,98,106]: 2*it(28)+2*s(5)+4*s(19)+2 Such that:aux(3) =< V aux(7) =< V4 aux(8) =< V4-V8 aux(198) =< V-V8 aux(199) =< V8 s(19) =< aux(199) it(28) =< aux(3) it(28) =< aux(198) it(28) =< aux(7) it(28) =< aux(8) s(6) =< it(28)*aux(199) s(5) =< s(6) with precondition: [V1=2,V8>=1,Out>=5,V>=V8+2,V4>=V8+3] * Chain [[28,29],32,97,106]: 2*it(28)+2*s(5)+7*s(23)+4*s(25)+2 Such that:aux(3) =< V aux(4) =< V-V8 aux(8) =< V4-V8 aux(201) =< V4 aux(202) =< V8 s(25) =< aux(201) s(23) =< aux(202) it(28) =< aux(3) it(28) =< aux(4) it(28) =< aux(201) it(28) =< aux(8) s(6) =< it(28)*aux(202) s(5) =< s(6) with precondition: [V1=2,V8>=1,Out>=5,V>=V8+2,V4>=V8+2] * Chain [[28,29],32,96,106]: 2*it(28)+2*s(5)+4*s(32)+2 Such that:aux(3) =< V aux(7) =< V4 aux(8) =< V4-V8 aux(204) =< V-V8 aux(205) =< V8 s(32) =< aux(205) it(28) =< aux(3) it(28) =< aux(204) it(28) =< aux(7) it(28) =< aux(8) s(6) =< it(28)*aux(205) s(5) =< s(6) with precondition: [V1=2,V8>=1,Out>=5,V>=V8+2,V4>=V8+3] * Chain [[28,29],32,95,106]: 2*it(28)+2*s(5)+3*s(141)+2*s(149)+2 Such that:aux(3) =< V aux(4) =< V-V8 aux(8) =< V4-V8 aux(206) =< V4 aux(207) =< V8 s(141) =< aux(206) s(149) =< aux(207) it(28) =< aux(3) it(28) =< aux(4) it(28) =< aux(206) it(28) =< aux(8) s(6) =< it(28)*aux(207) s(5) =< s(6) with precondition: [V1=2,V8>=1,Out>=5,V>=V8+2,V4>=V8+2] * Chain [[28,29],32,94,106]: 2*it(28)+2*s(5)+3*s(144)+2 Such that:aux(3) =< V aux(7) =< V4 aux(8) =< V4-V8 aux(209) =< V-V8 aux(210) =< V8 s(144) =< aux(210) it(28) =< aux(3) it(28) =< aux(209) it(28) =< aux(7) it(28) =< aux(8) s(6) =< it(28)*aux(210) s(5) =< s(6) with precondition: [V1=2,V8>=1,Out>=5,V>=V8+2,V4>=V8+3] * Chain [[28,29],32,93,106]: 2*it(28)+2*s(5)+3*s(145)+2*s(146)+2 Such that:aux(3) =< V aux(4) =< V-V8 aux(8) =< V4-V8 aux(212) =< V4 aux(213) =< V8 s(145) =< aux(213) s(146) =< aux(212) it(28) =< aux(3) it(28) =< aux(4) it(28) =< aux(212) it(28) =< aux(8) s(6) =< it(28)*aux(213) s(5) =< s(6) with precondition: [V1=2,V8>=1,Out>=5,V>=V8+2,V4>=V8+2] * Chain [[28,29],32,92,106]: 2*it(28)+2*s(5)+3*s(148)+2 Such that:aux(3) =< V aux(7) =< V4 aux(8) =< V4-V8 aux(215) =< V-V8 aux(216) =< V8 s(148) =< aux(216) it(28) =< aux(3) it(28) =< aux(215) it(28) =< aux(7) it(28) =< aux(8) s(6) =< it(28)*aux(216) s(5) =< s(6) with precondition: [V1=2,V8>=1,Out>=5,V>=V8+2,V4>=V8+3] * Chain [[28,29],32,71,106]: 2*it(28)+2*s(5)+3*s(56)+2 Such that:aux(3) =< V aux(4) =< V-V8 aux(7) =< V4 aux(218) =< V4-V8 aux(219) =< V8 s(56) =< aux(219) it(28) =< aux(3) it(28) =< aux(4) it(28) =< aux(218) it(28) =< aux(7) s(6) =< it(28)*aux(219) s(5) =< s(6) with precondition: [V1=2,V8>=1,V>=V4,V4>=V8+2,Out+V8>=V4+3] * Chain [[28,29],32,69,106]: 2*it(28)+2*s(5)+4*s(58)+2 Such that:aux(3) =< V aux(4) =< V-V8 aux(7) =< V4 aux(221) =< V4-V8 aux(222) =< V8 s(58) =< aux(222) it(28) =< aux(3) it(28) =< aux(4) it(28) =< aux(221) it(28) =< aux(7) s(6) =< it(28)*aux(222) s(5) =< s(6) with precondition: [V1=2,V8>=1,V>=V4,V4>=V8+2,Out+V8>=V4+3] * Chain [[28,29],32,59,106]: 2*it(28)+2*s(5)+2*s(149)+2 Such that:aux(3) =< V aux(4) =< V-V8 aux(7) =< V4 aux(223) =< V4-V8 aux(224) =< V8 s(149) =< aux(224) it(28) =< aux(3) it(28) =< aux(4) it(28) =< aux(223) it(28) =< aux(7) s(6) =< it(28)*aux(224) s(5) =< s(6) with precondition: [V1=2,V8>=1,V>=V4,V4>=V8+2,Out+V8>=V4+2] * Chain [[28,29],32,57,106]: 2*it(28)+2*s(5)+6*s(91)+2 Such that:aux(3) =< V aux(4) =< V-V8 aux(7) =< V4 aux(226) =< V4-V8 aux(227) =< V8 s(91) =< aux(227) it(28) =< aux(3) it(28) =< aux(4) it(28) =< aux(226) it(28) =< aux(7) s(6) =< it(28)*aux(227) s(5) =< s(6) with precondition: [V1=2,V8>=1,V>=V4,V4>=V8+2,Out+V8>=V4+3] * Chain [[28,29],32,53,106]: 2*it(28)+2*s(5)+2*s(149)+2 Such that:aux(3) =< V aux(4) =< V-V8 aux(7) =< V4 aux(228) =< V4-V8 aux(229) =< V8 s(149) =< aux(229) it(28) =< aux(3) it(28) =< aux(4) it(28) =< aux(228) it(28) =< aux(7) s(6) =< it(28)*aux(229) s(5) =< s(6) with precondition: [V1=2,V8>=1,V>=V4,V4>=V8+2,Out+V8>=V4+2] * Chain [[28,29],32,51,106]: 2*it(28)+2*s(5)+6*s(103)+2 Such that:aux(3) =< V aux(4) =< V-V8 aux(7) =< V4 aux(231) =< V4-V8 aux(232) =< V8 s(103) =< aux(232) it(28) =< aux(3) it(28) =< aux(4) it(28) =< aux(231) it(28) =< aux(7) s(6) =< it(28)*aux(232) s(5) =< s(6) with precondition: [V1=2,V8>=1,V>=V4,V4>=V8+2,Out+V8>=V4+3] * Chain [[28,29],31,106]: 2*it(28)+2*s(5)+1 Such that:aux(3) =< V aux(4) =< V-V8 aux(7) =< V4 aux(2) =< V8 aux(233) =< V4-V8 it(28) =< aux(3) it(28) =< aux(4) it(28) =< aux(233) it(28) =< aux(7) s(6) =< it(28)*aux(2) s(5) =< s(6) with precondition: [V1=2,V8>=1,Out>=2,V>=V8+2,V4>=V8+2] * Chain [[28,29],31,105,106]: 2*it(28)+2*s(5)+2 Such that:aux(3) =< V aux(4) =< V-V8 aux(7) =< V4 aux(2) =< V8 aux(234) =< V4-V8 it(28) =< aux(3) it(28) =< aux(4) it(28) =< aux(234) it(28) =< aux(7) s(6) =< it(28)*aux(2) s(5) =< s(6) with precondition: [V1=2,V8>=1,Out>=3,V>=V8+2,V4>=V8+2] * Chain [[28,29],31,91,106]: 2*it(28)+2*s(5)+2 Such that:aux(3) =< V aux(4) =< V-V8 aux(7) =< V4 aux(2) =< V8 aux(235) =< V4-V8 it(28) =< aux(3) it(28) =< aux(4) it(28) =< aux(235) it(28) =< aux(7) s(6) =< it(28)*aux(2) s(5) =< s(6) with precondition: [V1=2,V8>=1,Out>=3,V>=V8+2,V4>=V8+2] * Chain [[28,29],31,90,106]: 2*it(28)+2*s(5)+2 Such that:aux(3) =< V aux(4) =< V-V8 aux(7) =< V4 aux(2) =< V8 aux(236) =< V4-V8 it(28) =< aux(3) it(28) =< aux(4) it(28) =< aux(236) it(28) =< aux(7) s(6) =< it(28)*aux(2) s(5) =< s(6) with precondition: [V1=2,V8>=1,Out>=3,V>=V8+2,V4>=V8+2] * Chain [[28,29],31,89,106]: 2*it(28)+2*s(5)+2 Such that:aux(3) =< V aux(4) =< V-V8 aux(7) =< V4 aux(2) =< V8 aux(237) =< V4-V8 it(28) =< aux(3) it(28) =< aux(4) it(28) =< aux(237) it(28) =< aux(7) s(6) =< it(28)*aux(2) s(5) =< s(6) with precondition: [V1=2,V8>=1,Out>=3,V>=V8+2,V4>=V8+2] * Chain [[28,29],31,88,106]: 2*it(28)+2*s(5)+2 Such that:aux(3) =< V aux(4) =< V-V8 aux(7) =< V4 aux(2) =< V8 aux(238) =< V4-V8 it(28) =< aux(3) it(28) =< aux(4) it(28) =< aux(238) it(28) =< aux(7) s(6) =< it(28)*aux(2) s(5) =< s(6) with precondition: [V1=2,V8>=1,Out>=3,V>=V8+2,V4>=V8+2] * Chain [[28,29],31,87,106]: 2*it(28)+2*s(5)+5*s(34)+1*s(39)+2 Such that:aux(4) =< V-V8 aux(7) =< V4 aux(8) =< V4-V8 aux(239) =< V aux(240) =< V8 s(39) =< aux(240) s(34) =< aux(239) it(28) =< aux(239) it(28) =< aux(4) it(28) =< aux(7) it(28) =< aux(8) s(6) =< it(28)*aux(240) s(5) =< s(6) with precondition: [V1=2,V8>=1,Out>=4,V>=V8+2,V4>=V8+2] * Chain [[28,29],31,86,106]: 2*it(28)+2*s(5)+2*s(40)+2 Such that:aux(3) =< V aux(7) =< V4 aux(8) =< V4-V8 aux(241) =< V-V8 aux(242) =< V8 s(40) =< aux(242) it(28) =< aux(3) it(28) =< aux(241) it(28) =< aux(7) it(28) =< aux(8) s(6) =< it(28)*aux(242) s(5) =< s(6) with precondition: [V1=2,V8>=1,Out>=4,V>=V8+3,V4>=V8+2] * Chain [[28,29],31,85,106]: 2*it(28)+2*s(5)+7*s(42)+3*s(49)+2 Such that:aux(4) =< V-V8 aux(7) =< V4 aux(8) =< V4-V8 aux(243) =< V aux(244) =< V8 s(42) =< aux(243) s(49) =< aux(244) it(28) =< aux(243) it(28) =< aux(4) it(28) =< aux(7) it(28) =< aux(8) s(6) =< it(28)*aux(244) s(5) =< s(6) with precondition: [V1=2,V8>=1,Out>=4,V>=V8+2,V4>=V8+2] * Chain [[28,29],31,84,106]: 2*it(28)+2*s(5)+2*s(54)+2 Such that:aux(3) =< V aux(7) =< V4 aux(8) =< V4-V8 aux(245) =< V-V8 aux(246) =< V8 s(54) =< aux(246) it(28) =< aux(3) it(28) =< aux(245) it(28) =< aux(7) it(28) =< aux(8) s(6) =< it(28)*aux(246) s(5) =< s(6) with precondition: [V1=2,V8>=1,Out>=4,V>=V8+3,V4>=V8+2] * Chain [[28,29],31,83,106]: 2*it(28)+2*s(5)+3*s(151)+2 Such that:aux(4) =< V-V8 aux(7) =< V4 aux(8) =< V4-V8 aux(2) =< V8 aux(248) =< V s(151) =< aux(248) it(28) =< aux(248) it(28) =< aux(4) it(28) =< aux(7) it(28) =< aux(8) s(6) =< it(28)*aux(2) s(5) =< s(6) with precondition: [V1=2,V8>=1,Out>=4,V>=V8+2,V4>=V8+2] * Chain [[28,29],31,82,106]: 2*it(28)+2*s(5)+1*s(154)+2 Such that:aux(3) =< V aux(7) =< V4 aux(8) =< V4-V8 aux(249) =< V-V8 aux(250) =< V8 s(154) =< aux(250) it(28) =< aux(3) it(28) =< aux(249) it(28) =< aux(7) it(28) =< aux(8) s(6) =< it(28)*aux(250) s(5) =< s(6) with precondition: [V1=2,V8>=1,Out>=4,V>=V8+3,V4>=V8+2] * Chain [[28,29],31,81,106]: 2*it(28)+2*s(5)+3*s(155)+2 Such that:aux(4) =< V-V8 aux(7) =< V4 aux(8) =< V4-V8 aux(2) =< V8 aux(252) =< V s(155) =< aux(252) it(28) =< aux(252) it(28) =< aux(4) it(28) =< aux(7) it(28) =< aux(8) s(6) =< it(28)*aux(2) s(5) =< s(6) with precondition: [V1=2,V8>=1,Out>=4,V>=V8+2,V4>=V8+2] * Chain [[28,29],31,80,106]: 2*it(28)+2*s(5)+1*s(158)+2 Such that:aux(3) =< V aux(7) =< V4 aux(8) =< V4-V8 aux(253) =< V-V8 aux(254) =< V8 s(158) =< aux(254) it(28) =< aux(3) it(28) =< aux(253) it(28) =< aux(7) it(28) =< aux(8) s(6) =< it(28)*aux(254) s(5) =< s(6) with precondition: [V1=2,V8>=1,Out>=4,V>=V8+3,V4>=V8+2] * Chain [[28,29],31,70,106]: 2*it(28)+2*s(5)+1*s(57)+2 Such that:aux(3) =< V aux(7) =< V4 aux(8) =< V4-V8 aux(2) =< V8 s(57) =< V8+1 aux(255) =< V-V8 it(28) =< aux(3) it(28) =< aux(255) it(28) =< aux(7) it(28) =< aux(8) s(6) =< it(28)*aux(2) s(5) =< s(6) with precondition: [V1=2,V8>=1,V4>=V,V>=V8+2,Out+V8>=V+2] * Chain [[28,29],31,66,106]: 2*it(28)+2*s(5)+1*s(66)+2 Such that:aux(3) =< V aux(7) =< V4 aux(8) =< V4-V8 aux(2) =< V8 s(66) =< V8+1 aux(256) =< V-V8 it(28) =< aux(3) it(28) =< aux(256) it(28) =< aux(7) it(28) =< aux(8) s(6) =< it(28)*aux(2) s(5) =< s(6) with precondition: [V1=2,V8>=1,V4>=V,V>=V8+2,Out+V8>=V+2] * Chain [[28,29],31,58,106]: 2*it(28)+2*s(5)+2 Such that:aux(3) =< V aux(7) =< V4 aux(8) =< V4-V8 aux(2) =< V8 aux(257) =< V-V8 it(28) =< aux(3) it(28) =< aux(257) it(28) =< aux(7) it(28) =< aux(8) s(6) =< it(28)*aux(2) s(5) =< s(6) with precondition: [V1=2,V8>=1,V4>=V,V>=V8+2,Out+V8>=V+1] * Chain [[28,29],31,55,106]: 2*it(28)+2*s(5)+3*s(98)+2 Such that:aux(3) =< V aux(7) =< V4 aux(8) =< V4-V8 aux(2) =< V8 aux(93) =< V8+1 aux(258) =< V-V8 s(98) =< aux(93) it(28) =< aux(3) it(28) =< aux(258) it(28) =< aux(7) it(28) =< aux(8) s(6) =< it(28)*aux(2) s(5) =< s(6) with precondition: [V1=2,V8>=1,V4>=V,V>=V8+2,Out+V8>=V+2] * Chain [[28,29],31,47,106]: 2*it(28)+2*s(5)+2 Such that:aux(3) =< V aux(7) =< V4 aux(8) =< V4-V8 aux(2) =< V8 aux(259) =< V-V8 it(28) =< aux(3) it(28) =< aux(259) it(28) =< aux(7) it(28) =< aux(8) s(6) =< it(28)*aux(2) s(5) =< s(6) with precondition: [V1=2,V8>=1,V4>=V,V>=V8+2,Out+V8>=V+1] * Chain [[28,29],31,45,106]: 2*it(28)+2*s(5)+4*s(115)+2 Such that:aux(3) =< V aux(7) =< V4 aux(8) =< V4-V8 aux(2) =< V8 aux(113) =< V8+1 aux(260) =< V-V8 s(115) =< aux(113) it(28) =< aux(3) it(28) =< aux(260) it(28) =< aux(7) it(28) =< aux(8) s(6) =< it(28)*aux(2) s(5) =< s(6) with precondition: [V1=2,V8>=1,V4>=V,V>=V8+2,Out+V8>=V+2] * Chain [[28,29],30,106]: 2*it(28)+2*s(5)+2*s(159)+1 Such that:aux(3) =< V aux(7) =< V4 aux(8) =< V4-V8 aux(262) =< V-V8 aux(263) =< V8 s(159) =< aux(263) it(28) =< aux(3) it(28) =< aux(262) it(28) =< aux(7) it(28) =< aux(8) s(6) =< it(28)*aux(263) s(5) =< s(6) with precondition: [V1=2,V8>=1,Out>=3,V>=V8+2,V4>=V8+2] * Chain [[28,29],30,105,106]: 2*it(28)+2*s(5)+2*s(159)+2 Such that:aux(3) =< V aux(7) =< V4 aux(8) =< V4-V8 aux(264) =< V-V8 aux(265) =< V8 s(159) =< aux(265) it(28) =< aux(3) it(28) =< aux(264) it(28) =< aux(7) it(28) =< aux(8) s(6) =< it(28)*aux(265) s(5) =< s(6) with precondition: [V1=2,V8>=1,Out>=4,V>=V8+2,V4>=V8+2] * Chain [[28,29],30,91,106]: 2*it(28)+2*s(5)+2*s(159)+2 Such that:aux(3) =< V aux(7) =< V4 aux(8) =< V4-V8 aux(266) =< V-V8 aux(267) =< V8 s(159) =< aux(267) it(28) =< aux(3) it(28) =< aux(266) it(28) =< aux(7) it(28) =< aux(8) s(6) =< it(28)*aux(267) s(5) =< s(6) with precondition: [V1=2,V8>=1,Out>=4,V>=V8+2,V4>=V8+2] * Chain [[28,29],30,90,106]: 2*it(28)+2*s(5)+2*s(159)+2 Such that:aux(3) =< V aux(7) =< V4 aux(8) =< V4-V8 aux(268) =< V-V8 aux(269) =< V8 s(159) =< aux(269) it(28) =< aux(3) it(28) =< aux(268) it(28) =< aux(7) it(28) =< aux(8) s(6) =< it(28)*aux(269) s(5) =< s(6) with precondition: [V1=2,V8>=1,Out>=4,V>=V8+2,V4>=V8+2] * Chain [[28,29],30,89,106]: 2*it(28)+2*s(5)+2*s(159)+2 Such that:aux(3) =< V aux(7) =< V4 aux(8) =< V4-V8 aux(270) =< V-V8 aux(271) =< V8 s(159) =< aux(271) it(28) =< aux(3) it(28) =< aux(270) it(28) =< aux(7) it(28) =< aux(8) s(6) =< it(28)*aux(271) s(5) =< s(6) with precondition: [V1=2,V8>=1,Out>=4,V>=V8+2,V4>=V8+2] * Chain [[28,29],30,88,106]: 2*it(28)+2*s(5)+2*s(159)+2 Such that:aux(3) =< V aux(7) =< V4 aux(8) =< V4-V8 aux(272) =< V-V8 aux(273) =< V8 s(159) =< aux(273) it(28) =< aux(3) it(28) =< aux(272) it(28) =< aux(7) it(28) =< aux(8) s(6) =< it(28)*aux(273) s(5) =< s(6) with precondition: [V1=2,V8>=1,Out>=4,V>=V8+2,V4>=V8+2] * Chain [[28,29],30,87,106]: 2*it(28)+2*s(5)+5*s(34)+3*s(39)+2 Such that:aux(4) =< V-V8 aux(7) =< V4 aux(8) =< V4-V8 aux(275) =< V aux(276) =< V8 s(39) =< aux(276) s(34) =< aux(275) it(28) =< aux(275) it(28) =< aux(4) it(28) =< aux(7) it(28) =< aux(8) s(6) =< it(28)*aux(276) s(5) =< s(6) with precondition: [V1=2,V8>=1,Out>=5,V>=V8+2,V4>=V8+2] * Chain [[28,29],30,86,106]: 2*it(28)+2*s(5)+4*s(40)+2 Such that:aux(3) =< V aux(7) =< V4 aux(8) =< V4-V8 aux(278) =< V-V8 aux(279) =< V8 s(40) =< aux(279) it(28) =< aux(3) it(28) =< aux(278) it(28) =< aux(7) it(28) =< aux(8) s(6) =< it(28)*aux(279) s(5) =< s(6) with precondition: [V1=2,V8>=1,Out>=5,V>=V8+3,V4>=V8+2] * Chain [[28,29],30,85,106]: 2*it(28)+2*s(5)+7*s(42)+5*s(49)+2 Such that:aux(4) =< V-V8 aux(7) =< V4 aux(8) =< V4-V8 aux(281) =< V aux(282) =< V8 s(42) =< aux(281) s(49) =< aux(282) it(28) =< aux(281) it(28) =< aux(4) it(28) =< aux(7) it(28) =< aux(8) s(6) =< it(28)*aux(282) s(5) =< s(6) with precondition: [V1=2,V8>=1,Out>=5,V>=V8+2,V4>=V8+2] * Chain [[28,29],30,84,106]: 2*it(28)+2*s(5)+4*s(54)+2 Such that:aux(3) =< V aux(7) =< V4 aux(8) =< V4-V8 aux(284) =< V-V8 aux(285) =< V8 s(54) =< aux(285) it(28) =< aux(3) it(28) =< aux(284) it(28) =< aux(7) it(28) =< aux(8) s(6) =< it(28)*aux(285) s(5) =< s(6) with precondition: [V1=2,V8>=1,Out>=5,V>=V8+3,V4>=V8+2] * Chain [[28,29],30,83,106]: 2*it(28)+2*s(5)+3*s(151)+2*s(159)+2 Such that:aux(4) =< V-V8 aux(7) =< V4 aux(8) =< V4-V8 aux(286) =< V aux(287) =< V8 s(151) =< aux(286) s(159) =< aux(287) it(28) =< aux(286) it(28) =< aux(4) it(28) =< aux(7) it(28) =< aux(8) s(6) =< it(28)*aux(287) s(5) =< s(6) with precondition: [V1=2,V8>=1,Out>=5,V>=V8+2,V4>=V8+2] * Chain [[28,29],30,82,106]: 2*it(28)+2*s(5)+3*s(154)+2 Such that:aux(3) =< V aux(7) =< V4 aux(8) =< V4-V8 aux(289) =< V-V8 aux(290) =< V8 s(154) =< aux(290) it(28) =< aux(3) it(28) =< aux(289) it(28) =< aux(7) it(28) =< aux(8) s(6) =< it(28)*aux(290) s(5) =< s(6) with precondition: [V1=2,V8>=1,Out>=5,V>=V8+3,V4>=V8+2] * Chain [[28,29],30,81,106]: 2*it(28)+2*s(5)+3*s(155)+2*s(159)+2 Such that:aux(4) =< V-V8 aux(7) =< V4 aux(8) =< V4-V8 aux(291) =< V aux(292) =< V8 s(155) =< aux(291) s(159) =< aux(292) it(28) =< aux(291) it(28) =< aux(4) it(28) =< aux(7) it(28) =< aux(8) s(6) =< it(28)*aux(292) s(5) =< s(6) with precondition: [V1=2,V8>=1,Out>=5,V>=V8+2,V4>=V8+2] * Chain [[28,29],30,80,106]: 2*it(28)+2*s(5)+3*s(158)+2 Such that:aux(3) =< V aux(7) =< V4 aux(8) =< V4-V8 aux(294) =< V-V8 aux(295) =< V8 s(158) =< aux(295) it(28) =< aux(3) it(28) =< aux(294) it(28) =< aux(7) it(28) =< aux(8) s(6) =< it(28)*aux(295) s(5) =< s(6) with precondition: [V1=2,V8>=1,Out>=5,V>=V8+3,V4>=V8+2] * Chain [[28,29],30,70,106]: 2*it(28)+2*s(5)+3*s(57)+2 Such that:aux(3) =< V aux(7) =< V4 aux(8) =< V4-V8 aux(297) =< V-V8 aux(298) =< V8 s(57) =< aux(298) it(28) =< aux(3) it(28) =< aux(297) it(28) =< aux(7) it(28) =< aux(8) s(6) =< it(28)*aux(298) s(5) =< s(6) with precondition: [V1=2,V8>=1,V4>=V,V>=V8+2,Out+V8>=V+3] * Chain [[28,29],30,66,106]: 2*it(28)+2*s(5)+3*s(66)+2 Such that:aux(3) =< V aux(7) =< V4 aux(8) =< V4-V8 aux(300) =< V-V8 aux(301) =< V8 s(66) =< aux(301) it(28) =< aux(3) it(28) =< aux(300) it(28) =< aux(7) it(28) =< aux(8) s(6) =< it(28)*aux(301) s(5) =< s(6) with precondition: [V1=2,V8>=1,V4>=V,V>=V8+2,Out+V8>=V+3] * Chain [[28,29],30,58,106]: 2*it(28)+2*s(5)+2*s(159)+2 Such that:aux(3) =< V aux(7) =< V4 aux(8) =< V4-V8 aux(2) =< V8 aux(261) =< V8+1 aux(302) =< V-V8 s(159) =< aux(261) it(28) =< aux(3) it(28) =< aux(302) it(28) =< aux(7) it(28) =< aux(8) s(6) =< it(28)*aux(2) s(5) =< s(6) with precondition: [V1=2,V8>=1,V4>=V,V>=V8+2,Out+V8>=V+2] * Chain [[28,29],30,55,106]: 2*it(28)+2*s(5)+5*s(98)+2 Such that:aux(3) =< V aux(7) =< V4 aux(8) =< V4-V8 aux(304) =< V-V8 aux(305) =< V8 s(98) =< aux(305) it(28) =< aux(3) it(28) =< aux(304) it(28) =< aux(7) it(28) =< aux(8) s(6) =< it(28)*aux(305) s(5) =< s(6) with precondition: [V1=2,V8>=1,V4>=V,V>=V8+2,Out+V8>=V+3] * Chain [[28,29],30,47,106]: 2*it(28)+2*s(5)+2*s(159)+2 Such that:aux(3) =< V aux(7) =< V4 aux(8) =< V4-V8 aux(2) =< V8 aux(261) =< V8+1 aux(306) =< V-V8 s(159) =< aux(261) it(28) =< aux(3) it(28) =< aux(306) it(28) =< aux(7) it(28) =< aux(8) s(6) =< it(28)*aux(2) s(5) =< s(6) with precondition: [V1=2,V8>=1,V4>=V,V>=V8+2,Out+V8>=V+2] * Chain [[28,29],30,45,106]: 2*it(28)+2*s(5)+6*s(115)+2 Such that:aux(3) =< V aux(7) =< V4 aux(8) =< V4-V8 aux(308) =< V-V8 aux(309) =< V8 s(115) =< aux(309) it(28) =< aux(3) it(28) =< aux(308) it(28) =< aux(7) it(28) =< aux(8) s(6) =< it(28)*aux(309) s(5) =< s(6) with precondition: [V1=2,V8>=1,V4>=V,V>=V8+2,Out+V8>=V+3] * Chain [106]: 0 with precondition: [Out=0,V1>=0,V>=0,V4>=0,V8>=0] * Chain [105,106]: 1 with precondition: [V1=2,Out=1,V>=0,V4>=0,V8>=0] * Chain [104,106]: 1 with precondition: [V1=2,V=0,Out=1,V4>=0,V8>=0] * Chain [103,106]: 1 with precondition: [V1=2,V8=0,Out=1,V>=0,V4>=1] * Chain [102,106]: 1 with precondition: [V1=2,Out=1,V>=0,V4>=1,V8>=0] * Chain [101,106]: 1 with precondition: [V1=2,V=0,V8=0,Out=1,V4>=1] * Chain [100,106]: 1 with precondition: [V1=2,V=0,Out=1,V4>=1,V8>=0] * Chain [99,106]: 2*s(7)+3*s(9)+7*s(10)+1 Such that:aux(14) =< V aux(15) =< V4 aux(16) =< V8 s(7) =< aux(14) s(10) =< aux(15) s(9) =< aux(16) with precondition: [V1=2,V>=0,Out>=2,V4+1>=Out,V8+1>=Out] * Chain [98,106]: 2*s(19)+1 Such that:aux(20) =< V8 s(19) =< aux(20) with precondition: [V1=2,V>=0,Out>=2,V4>=V8+1,V8+1>=Out] * Chain [97,106]: 2*s(21)+5*s(23)+4*s(25)+1 Such that:aux(23) =< V aux(25) =< V8 aux(26) =< V4 s(25) =< aux(26) s(21) =< aux(23) s(23) =< aux(25) with precondition: [V1=2,V>=0,Out>=2,V4+1>=Out,V8+1>=Out] * Chain [96,106]: 2*s(32)+1 Such that:aux(30) =< V8 s(32) =< aux(30) with precondition: [V1=2,V>=0,Out>=2,V4>=V8+1,V8+1>=Out] * Chain [95,106]: 3*s(141)+1 Such that:aux(164) =< V4 s(141) =< aux(164) with precondition: [V1=2,V=0,Out>=2,V4+1>=Out,V8+1>=Out] * Chain [94,106]: 1*s(144)+1 Such that:s(144) =< V8 with precondition: [V1=2,V=0,Out>=2,V4>=V8+1,V8+1>=Out] * Chain [93,106]: 1*s(145)+2*s(146)+1 Such that:aux(168) =< V4 s(145) =< V8 s(146) =< aux(168) with precondition: [V1=2,V=0,Out>=2,V4+1>=Out,V8+1>=Out] * Chain [92,106]: 1*s(148)+1 Such that:s(148) =< V8 with precondition: [V1=2,V=0,Out>=2,V4>=V8+1,V8+1>=Out] * Chain [91,106]: 1 with precondition: [V1=2,V4=0,Out=1,V>=0,V8>=0] * Chain [90,106]: 1 with precondition: [V1=2,Out=1,V>=1,V4>=0,V8>=0] * Chain [89,106]: 1 with precondition: [V1=2,V4=0,Out=1,V>=0,V8>=0] * Chain [88,106]: 1 with precondition: [V1=2,V4=0,Out=1,V>=1,V8>=0] * Chain [87,106]: 5*s(34)+1*s(39)+1 Such that:aux(34) =< V s(39) =< V8 s(34) =< aux(34) with precondition: [V1=2,V4>=0,Out>=2,V+1>=Out,V8+1>=Out] * Chain [86,106]: 2*s(40)+1 Such that:aux(37) =< V8 s(40) =< aux(37) with precondition: [V1=2,V4>=0,Out>=2,V>=V8+1,V8+1>=Out] * Chain [85,106]: 7*s(42)+3*s(49)+2*s(51)+1 Such that:aux(41) =< V4 aux(43) =< V8 aux(44) =< V s(42) =< aux(44) s(51) =< aux(41) s(49) =< aux(43) with precondition: [V1=2,V4>=0,Out>=2,V+1>=Out,V8+1>=Out] * Chain [84,106]: 2*s(54)+1 Such that:aux(48) =< V8 s(54) =< aux(48) with precondition: [V1=2,V4>=0,Out>=2,V>=V8+1,V8+1>=Out] * Chain [83,106]: 3*s(151)+1 Such that:aux(247) =< V s(151) =< aux(247) with precondition: [V1=2,V4=0,Out>=2,V+1>=Out,V8+1>=Out] * Chain [82,106]: 1*s(154)+1 Such that:s(154) =< V8 with precondition: [V1=2,V4=0,Out>=2,V>=V8+1,V8+1>=Out] * Chain [81,106]: 3*s(155)+1 Such that:aux(251) =< V s(155) =< aux(251) with precondition: [V1=2,V4=0,Out>=2,V+1>=Out,V8+1>=Out] * Chain [80,106]: 1*s(158)+1 Such that:s(158) =< V8 with precondition: [V1=2,V4=0,Out>=2,V>=V8+1,V8+1>=Out] * Chain [79,106]: 1 with precondition: [V1=2,V8=0,Out=1,V>=1,V4>=0] * Chain [78,106]: 1 with precondition: [V1=2,V8=0,Out=1,V>=0,V4>=1] * Chain [77,106]: 1 with precondition: [V1=2,V8=0,Out=1,V>=1,V4>=0] * Chain [76,106]: 1 with precondition: [V1=2,Out=1,V>=1,V4>=1,V8>=0] * Chain [75,106]: 1 with precondition: [V1=2,V8=0,Out=1,V>=1,V4>=1] * Chain [75,105,106]: 2 with precondition: [V1=2,V8=0,Out=2,V>=1,V4>=1] * Chain [75,104,106]: 2 with precondition: [V1=2,V8=0,Out=2,V>=1,V4>=1] * Chain [75,91,106]: 2 with precondition: [V1=2,V8=0,Out=2,V>=1,V4>=1] * Chain [75,89,106]: 2 with precondition: [V1=2,V8=0,Out=2,V>=1,V4>=1] * Chain [74,106]: 1 with precondition: [V1=2,V8=0,Out=1,V>=1,V4>=1] * Chain [74,105,106]: 2 with precondition: [V1=2,V8=0,Out=2,V>=1,V4>=1] * Chain [74,104,106]: 2 with precondition: [V1=2,V8=0,Out=2,V>=1,V4>=1] * Chain [74,103,106]: 2 with precondition: [V1=2,V8=0,Out=2,V>=1,V4>=2] * Chain [74,102,106]: 2 with precondition: [V1=2,V8=0,Out=2,V>=1,V4>=2] * Chain [74,101,106]: 2 with precondition: [V1=2,V8=0,Out=2,V>=1,V4>=2] * Chain [74,100,106]: 2 with precondition: [V1=2,V8=0,Out=2,V>=1,V4>=2] * Chain [74,91,106]: 2 with precondition: [V1=2,V4=1,V8=0,Out=2,V>=1] * Chain [74,89,106]: 2 with precondition: [V1=2,V4=1,V8=0,Out=2,V>=1] * Chain [74,78,106]: 2 with precondition: [V1=2,V8=0,Out=2,V>=1,V4>=2] * Chain [73,106]: 1 with precondition: [V1=2,V8=0,Out=1,V>=1,V4>=1] * Chain [73,105,106]: 2 with precondition: [V1=2,V8=0,Out=2,V>=1,V4>=1] * Chain [73,104,106]: 2 with precondition: [V1=2,V=1,V8=0,Out=2,V4>=1] * Chain [73,91,106]: 2 with precondition: [V1=2,V8=0,Out=2,V>=1,V4>=1] * Chain [73,90,106]: 2 with precondition: [V1=2,V8=0,Out=2,V>=2,V4>=1] * Chain [73,89,106]: 2 with precondition: [V1=2,V8=0,Out=2,V>=1,V4>=1] * Chain [73,88,106]: 2 with precondition: [V1=2,V8=0,Out=2,V>=2,V4>=1] * Chain [73,79,106]: 2 with precondition: [V1=2,V8=0,Out=2,V>=2,V4>=1] * Chain [73,77,106]: 2 with precondition: [V1=2,V8=0,Out=2,V>=2,V4>=1] * Chain [71,106]: 1*s(56)+1 Such that:s(56) =< V4 with precondition: [V1=2,V>=0,Out>=2,V8>=V4,V4+1>=Out] * Chain [70,106]: 1*s(57)+1 Such that:s(57) =< V with precondition: [V1=2,V4>=0,Out>=2,V8>=V,V+1>=Out] * Chain [69,106]: 2*s(58)+1 Such that:aux(56) =< V4 s(58) =< aux(56) with precondition: [V1=2,V>=0,Out>=2,V8>=V4,V4+1>=Out] * Chain [68,106]: 4*s(60)+1 Such that:aux(59) =< V s(60) =< aux(59) with precondition: [V1=2,V4>=1,Out>=2,V+1>=Out,V8+1>=Out] * Chain [67,106]: 2*s(64)+1 Such that:aux(61) =< V8 s(64) =< aux(61) with precondition: [V1=2,V4>=1,Out>=2,V>=V8+1,V8+1>=Out] * Chain [66,106]: 1*s(66)+1 Such that:s(66) =< V with precondition: [V1=2,V4>=0,Out>=2,V8>=V,V+1>=Out] * Chain [65,106]: 4*s(67)+1*s(71)+1 Such that:aux(66) =< V4 s(71) =< V8 s(67) =< aux(66) with precondition: [V1=2,V>=1,Out>=2,V4+1>=Out,V8+1>=Out] * Chain [64,106]: 1*s(72)+1 Such that:s(72) =< V8 with precondition: [V1=2,V>=1,Out>=2,V4>=V8+1,V8+1>=Out] * Chain [63,106]: 2*s(73)+4*s(75)+5*s(77)+1 Such that:aux(71) =< V aux(73) =< V8 aux(74) =< V4 s(77) =< aux(74) s(73) =< aux(71) s(75) =< aux(73) with precondition: [V1=2,V>=1,Out>=2,V4+1>=Out,V8+1>=Out] * Chain [62,106]: 1*s(84)+3*s(85)+1 Such that:aux(78) =< V s(84) =< V8 s(85) =< aux(78) with precondition: [V1=2,V4>=1,Out>=2,V+1>=Out,V8+1>=Out] * Chain [61,106]: 1*s(88)+1 Such that:s(88) =< V8 with precondition: [V1=2,V>=1,Out>=2,V4>=V8+1,V8+1>=Out] * Chain [60,106]: 2*s(89)+1 Such that:aux(83) =< V8 s(89) =< aux(83) with precondition: [V1=2,V4>=1,Out>=2,V>=V8+1,V8+1>=Out] * Chain [59,106]: 1 with precondition: [V1=2,Out=1,V>=0,V4>=1,V8>=V4] * Chain [58,106]: 1 with precondition: [V1=2,Out=1,V>=1,V4>=0,V8>=V] * Chain [57,106]: 4*s(91)+1 Such that:aux(88) =< V4 s(91) =< aux(88) with precondition: [V1=2,V>=0,Out>=2,V8>=V4,V4+1>=Out] * Chain [56,106]: 1*s(95)+1*s(96)+1*s(97)+1 Such that:s(95) =< V s(96) =< V4 s(97) =< V8 with precondition: [V1=2,V>=1,Out>=2,V8>=V,V4+1>=Out,V8+1>=Out] * Chain [55,106]: 3*s(98)+1 Such that:aux(93) =< V s(98) =< aux(93) with precondition: [V1=2,V4>=0,Out>=2,V8>=V,V+1>=Out] * Chain [54,106]: 1*s(101)+1*s(102)+1 Such that:s(101) =< V s(102) =< V8 with precondition: [V1=2,V4>=1,Out>=2,V8>=V4,V+1>=Out,V8+1>=Out] * Chain [53,106]: 1 with precondition: [V1=2,Out=1,V>=0,V4>=1,V8>=V4] * Chain [52,106]: 1 with precondition: [V1=2,Out=1,V>=1,V4>=1,V8>=V] * Chain [51,106]: 4*s(103)+1 Such that:aux(100) =< V4 s(103) =< aux(100) with precondition: [V1=2,V>=0,Out>=2,V8>=V4,V4+1>=Out] * Chain [50,106]: 4*s(107)+1 Such that:aux(103) =< V s(107) =< aux(103) with precondition: [V1=2,V4>=1,Out>=2,V8>=V,V+1>=Out] * Chain [49,106]: 1*s(111)+1*s(112)+1 Such that:s(111) =< V s(112) =< V8 with precondition: [V1=2,V4>=1,Out>=2,V8>=V4,V+1>=Out,V8+1>=Out] * Chain [48,106]: 1*s(113)+1*s(114)+1 Such that:s(113) =< V4 s(114) =< V8 with precondition: [V1=2,V>=1,Out>=2,V8>=V,V4+1>=Out,V8+1>=Out] * Chain [47,106]: 1 with precondition: [V1=2,Out=1,V>=1,V4>=0,V8>=V] * Chain [46,106]: 1 with precondition: [V1=2,Out=1,V>=1,V4>=1,V8>=V4] * Chain [45,106]: 4*s(115)+1 Such that:aux(113) =< V s(115) =< aux(113) with precondition: [V1=2,V4>=0,Out>=2,V8>=V,V+1>=Out] * Chain [44,106]: 4*s(119)+1 Such that:aux(116) =< V4 s(119) =< aux(116) with precondition: [V1=2,V>=1,Out>=2,V8>=V4,V4+1>=Out] * Chain [43,106]: 1*s(123)+1*s(124)+1 Such that:s(123) =< V4 s(124) =< V8 with precondition: [V1=2,V>=1,Out>=2,V8>=V,V4+1>=Out,V8+1>=Out] * Chain [42,106]: 1*s(125)+1*s(126)+1 Such that:s(125) =< V s(126) =< V8 with precondition: [V1=2,V4>=1,Out>=2,V8>=V4,V+1>=Out,V8+1>=Out] * Chain [41,106]: 1 with precondition: [V1=2,Out=1,V>=1,V4>=1,V8>=V] * Chain [40,106]: 1 with precondition: [V1=2,Out=1,V>=1,V4>=1,V8>=V4] * Chain [39,106]: 4*s(127)+1 Such that:aux(125) =< V4 s(127) =< aux(125) with precondition: [V1=2,V>=1,Out>=2,V8>=V4,V4+1>=Out] * Chain [38,106]: 4*s(131)+1 Such that:aux(128) =< V s(131) =< aux(128) with precondition: [V1=2,V4>=1,Out>=2,V8>=V,V+1>=Out] * Chain [37,106]: 1*s(135)+1*s(136)+1 Such that:s(135) =< V s(136) =< V8 with precondition: [V1=2,V4>=1,Out>=2,V8>=V4,V+1>=Out,V8+1>=Out] * Chain [36,106]: 1*s(137)+1*s(138)+1 Such that:s(137) =< V4 s(138) =< V8 with precondition: [V1=2,V>=1,Out>=2,V8>=V,V4+1>=Out,V8+1>=Out] * Chain [35,106]: 1 with precondition: [V1=2,Out=1,V8>=1,V>=V8+1,V4>=V8+1] * Chain [35,105,106]: 2 with precondition: [V1=2,Out=2,V8>=1,V>=V8+1,V4>=V8+1] * Chain [35,104,106]: 2 with precondition: [V1=2,Out=2,V8>=1,V>=V8+1,V4>=V8+1] * Chain [35,91,106]: 2 with precondition: [V1=2,Out=2,V8>=1,V>=V8+1,V4>=V8+1] * Chain [35,89,106]: 2 with precondition: [V1=2,Out=2,V8>=1,V>=V8+1,V4>=V8+1] * Chain [34,106]: 2*s(139)+1 Such that:aux(140) =< V8 s(139) =< aux(140) with precondition: [V1=2,Out>=2,V>=V8+1,V4>=V8+1,V8+1>=Out] * Chain [34,105,106]: 2*s(139)+2 Such that:aux(140) =< V8 s(139) =< aux(140) with precondition: [V1=2,Out>=3,V>=V8+1,V4>=V8+1,V8+2>=Out] * Chain [34,104,106]: 2*s(139)+2 Such that:aux(140) =< V8 s(139) =< aux(140) with precondition: [V1=2,Out>=3,V>=V8+1,V4>=V8+1,V8+2>=Out] * Chain [34,91,106]: 2*s(139)+2 Such that:aux(140) =< V8 s(139) =< aux(140) with precondition: [V1=2,Out>=3,V>=V8+1,V4>=V8+1,V8+2>=Out] * Chain [34,89,106]: 2*s(139)+2 Such that:aux(140) =< V8 s(139) =< aux(140) with precondition: [V1=2,Out>=3,V>=V8+1,V4>=V8+1,V8+2>=Out] * Chain [33,106]: 1 with precondition: [V1=2,Out=1,V8>=1,V>=V8+1,V4>=V8+1] * Chain [33,105,106]: 2 with precondition: [V1=2,Out=2,V8>=1,V>=V8+1,V4>=V8+1] * Chain [33,104,106]: 2 with precondition: [V1=2,Out=2,V8>=1,V>=V8+1,V4>=V8+1] * Chain [33,102,106]: 2 with precondition: [V1=2,Out=2,V8>=1,V>=V8+1,V4>=V8+1] * Chain [33,100,106]: 2 with precondition: [V1=2,Out=2,V8>=1,V>=V8+1,V4>=V8+1] * Chain [33,99,106]: 3*s(9)+7*s(10)+2 Such that:aux(15) =< V4 aux(16) =< V8 s(10) =< aux(15) s(9) =< aux(16) with precondition: [V1=2,Out>=3,V>=V8+1,V4>=V8+1,V8+2>=Out] * Chain [33,98,106]: 2*s(19)+2 Such that:aux(20) =< V8 s(19) =< aux(20) with precondition: [V1=2,Out>=3,V>=V8+1,V4>=V8+2,V8+2>=Out] * Chain [33,97,106]: 5*s(23)+4*s(25)+2 Such that:aux(26) =< V4 aux(25) =< V8 s(25) =< aux(26) s(23) =< aux(25) with precondition: [V1=2,Out>=3,V>=V8+1,V4>=V8+1,V8+2>=Out] * Chain [33,96,106]: 2*s(32)+2 Such that:aux(30) =< V8 s(32) =< aux(30) with precondition: [V1=2,Out>=3,V>=V8+1,V4>=V8+2,V8+2>=Out] * Chain [33,95,106]: 3*s(141)+2 Such that:aux(164) =< V4 s(141) =< aux(164) with precondition: [V1=2,Out>=3,V>=V8+1,V4>=V8+1,V8+2>=Out] * Chain [33,94,106]: 1*s(144)+2 Such that:s(144) =< V8 with precondition: [V1=2,Out>=3,V>=V8+1,V4>=V8+2,V8+2>=Out] * Chain [33,93,106]: 1*s(145)+2*s(146)+2 Such that:aux(168) =< V4 s(145) =< V8 s(146) =< aux(168) with precondition: [V1=2,Out>=3,V>=V8+1,V4>=V8+1,V8+2>=Out] * Chain [33,92,106]: 1*s(148)+2 Such that:s(148) =< V8 with precondition: [V1=2,Out>=3,V>=V8+1,V4>=V8+2,V8+2>=Out] * Chain [33,71,106]: 1*s(56)+2 Such that:s(56) =< V8 with precondition: [V1=2,V4=V8+1,Out>=3,V>=V4,V4+1>=Out] * Chain [33,69,106]: 2*s(58)+2 Such that:aux(56) =< V8 s(58) =< aux(56) with precondition: [V1=2,V4=V8+1,Out>=3,V>=V4,V4+1>=Out] * Chain [33,59,106]: 2 with precondition: [V1=2,Out=2,V8+1=V4,V8>=1,V>=V8+1] * Chain [33,57,106]: 4*s(91)+2 Such that:aux(88) =< V8 s(91) =< aux(88) with precondition: [V1=2,V4=V8+1,Out>=3,V>=V4,V4+1>=Out] * Chain [33,53,106]: 2 with precondition: [V1=2,Out=2,V8+1=V4,V8>=1,V>=V8+1] * Chain [33,51,106]: 4*s(103)+2 Such that:aux(100) =< V8 s(103) =< aux(100) with precondition: [V1=2,V4=V8+1,Out>=3,V>=V4,V4+1>=Out] * Chain [32,106]: 2*s(149)+1 Such that:aux(183) =< V8 s(149) =< aux(183) with precondition: [V1=2,Out>=2,V>=V8+1,V4>=V8+1,V8+1>=Out] * Chain [32,105,106]: 2*s(149)+2 Such that:aux(183) =< V8 s(149) =< aux(183) with precondition: [V1=2,Out>=3,V>=V8+1,V4>=V8+1,V8+2>=Out] * Chain [32,104,106]: 2*s(149)+2 Such that:aux(183) =< V8 s(149) =< aux(183) with precondition: [V1=2,Out>=3,V>=V8+1,V4>=V8+1,V8+2>=Out] * Chain [32,102,106]: 2*s(149)+2 Such that:aux(183) =< V8 s(149) =< aux(183) with precondition: [V1=2,Out>=3,V>=V8+1,V4>=V8+1,V8+2>=Out] * Chain [32,100,106]: 2*s(149)+2 Such that:aux(183) =< V8 s(149) =< aux(183) with precondition: [V1=2,Out>=3,V>=V8+1,V4>=V8+1,V8+2>=Out] * Chain [32,99,106]: 5*s(9)+7*s(10)+2 Such that:aux(15) =< V4 aux(194) =< V8 s(10) =< aux(15) s(9) =< aux(194) with precondition: [V1=2,Out>=4,V>=V8+1,V4>=V8+1,2*V8+2>=Out] * Chain [32,98,106]: 4*s(19)+2 Such that:aux(197) =< V8 s(19) =< aux(197) with precondition: [V1=2,Out>=4,V>=V8+1,V4>=V8+2,2*V8+2>=Out] * Chain [32,97,106]: 7*s(23)+4*s(25)+2 Such that:aux(26) =< V4 aux(200) =< V8 s(25) =< aux(26) s(23) =< aux(200) with precondition: [V1=2,Out>=4,V>=V8+1,V4>=V8+1,2*V8+2>=Out] * Chain [32,96,106]: 4*s(32)+2 Such that:aux(203) =< V8 s(32) =< aux(203) with precondition: [V1=2,Out>=4,V>=V8+1,V4>=V8+2,2*V8+2>=Out] * Chain [32,95,106]: 3*s(141)+2*s(149)+2 Such that:aux(164) =< V4 aux(183) =< V8 s(141) =< aux(164) s(149) =< aux(183) with precondition: [V1=2,Out>=4,V>=V8+1,V4>=V8+1,2*V8+2>=Out] * Chain [32,94,106]: 3*s(144)+2 Such that:aux(208) =< V8 s(144) =< aux(208) with precondition: [V1=2,Out>=4,V>=V8+1,V4>=V8+2,2*V8+2>=Out] * Chain [32,93,106]: 3*s(145)+2*s(146)+2 Such that:aux(168) =< V4 aux(211) =< V8 s(145) =< aux(211) s(146) =< aux(168) with precondition: [V1=2,Out>=4,V>=V8+1,V4>=V8+1,2*V8+2>=Out] * Chain [32,92,106]: 3*s(148)+2 Such that:aux(214) =< V8 s(148) =< aux(214) with precondition: [V1=2,Out>=4,V>=V8+1,V4>=V8+2,2*V8+2>=Out] * Chain [32,71,106]: 3*s(56)+2 Such that:aux(217) =< V8 s(56) =< aux(217) with precondition: [V1=2,V4=V8+1,Out>=4,V>=V4,2*V4>=Out] * Chain [32,69,106]: 4*s(58)+2 Such that:aux(220) =< V8 s(58) =< aux(220) with precondition: [V1=2,V4=V8+1,Out>=4,V>=V4,2*V4>=Out] * Chain [32,59,106]: 2*s(149)+2 Such that:aux(183) =< V8 s(149) =< aux(183) with precondition: [V1=2,V4=V8+1,Out>=3,V>=V4,V4+1>=Out] * Chain [32,57,106]: 6*s(91)+2 Such that:aux(225) =< V8 s(91) =< aux(225) with precondition: [V1=2,V4=V8+1,Out>=4,V>=V4,2*V4>=Out] * Chain [32,53,106]: 2*s(149)+2 Such that:aux(183) =< V8 s(149) =< aux(183) with precondition: [V1=2,V4=V8+1,Out>=3,V>=V4,V4+1>=Out] * Chain [32,51,106]: 6*s(103)+2 Such that:aux(230) =< V8 s(103) =< aux(230) with precondition: [V1=2,V4=V8+1,Out>=4,V>=V4,2*V4>=Out] * Chain [31,106]: 1 with precondition: [V1=2,Out=1,V8>=1,V>=V8+1,V4>=V8+1] * Chain [31,105,106]: 2 with precondition: [V1=2,Out=2,V8>=1,V>=V8+1,V4>=V8+1] * Chain [31,91,106]: 2 with precondition: [V1=2,Out=2,V8>=1,V>=V8+1,V4>=V8+1] * Chain [31,90,106]: 2 with precondition: [V1=2,Out=2,V8>=1,V>=V8+1,V4>=V8+1] * Chain [31,89,106]: 2 with precondition: [V1=2,Out=2,V8>=1,V>=V8+1,V4>=V8+1] * Chain [31,88,106]: 2 with precondition: [V1=2,Out=2,V8>=1,V>=V8+1,V4>=V8+1] * Chain [31,87,106]: 5*s(34)+1*s(39)+2 Such that:aux(34) =< V s(39) =< V8 s(34) =< aux(34) with precondition: [V1=2,Out>=3,V>=V8+1,V4>=V8+1,V8+2>=Out] * Chain [31,86,106]: 2*s(40)+2 Such that:aux(37) =< V8 s(40) =< aux(37) with precondition: [V1=2,Out>=3,V>=V8+2,V4>=V8+1,V8+2>=Out] * Chain [31,85,106]: 7*s(42)+3*s(49)+2 Such that:aux(44) =< V aux(43) =< V8 s(42) =< aux(44) s(49) =< aux(43) with precondition: [V1=2,Out>=3,V>=V8+1,V4>=V8+1,V8+2>=Out] * Chain [31,84,106]: 2*s(54)+2 Such that:aux(48) =< V8 s(54) =< aux(48) with precondition: [V1=2,Out>=3,V>=V8+2,V4>=V8+1,V8+2>=Out] * Chain [31,83,106]: 3*s(151)+2 Such that:aux(247) =< V s(151) =< aux(247) with precondition: [V1=2,Out>=3,V>=V8+1,V4>=V8+1,V8+2>=Out] * Chain [31,82,106]: 1*s(154)+2 Such that:s(154) =< V8 with precondition: [V1=2,Out>=3,V>=V8+2,V4>=V8+1,V8+2>=Out] * Chain [31,81,106]: 3*s(155)+2 Such that:aux(251) =< V s(155) =< aux(251) with precondition: [V1=2,Out>=3,V>=V8+1,V4>=V8+1,V8+2>=Out] * Chain [31,80,106]: 1*s(158)+2 Such that:s(158) =< V8 with precondition: [V1=2,Out>=3,V>=V8+2,V4>=V8+1,V8+2>=Out] * Chain [31,70,106]: 1*s(57)+2 Such that:s(57) =< V with precondition: [V1=2,V=V8+1,Out>=3,V4>=V,V+1>=Out] * Chain [31,66,106]: 1*s(66)+2 Such that:s(66) =< V with precondition: [V1=2,V=V8+1,Out>=3,V4>=V,V+1>=Out] * Chain [31,58,106]: 2 with precondition: [V1=2,Out=2,V=V8+1,V>=2,V4>=V] * Chain [31,55,106]: 3*s(98)+2 Such that:aux(93) =< V s(98) =< aux(93) with precondition: [V1=2,V=V8+1,Out>=3,V4>=V,V+1>=Out] * Chain [31,47,106]: 2 with precondition: [V1=2,Out=2,V=V8+1,V>=2,V4>=V] * Chain [31,45,106]: 4*s(115)+2 Such that:aux(113) =< V s(115) =< aux(113) with precondition: [V1=2,V=V8+1,Out>=3,V4>=V,V+1>=Out] * Chain [30,106]: 2*s(159)+1 Such that:aux(261) =< V8 s(159) =< aux(261) with precondition: [V1=2,Out>=2,V>=V8+1,V4>=V8+1,V8+1>=Out] * Chain [30,105,106]: 2*s(159)+2 Such that:aux(261) =< V8 s(159) =< aux(261) with precondition: [V1=2,Out>=3,V>=V8+1,V4>=V8+1,V8+2>=Out] * Chain [30,91,106]: 2*s(159)+2 Such that:aux(261) =< V8 s(159) =< aux(261) with precondition: [V1=2,Out>=3,V>=V8+1,V4>=V8+1,V8+2>=Out] * Chain [30,90,106]: 2*s(159)+2 Such that:aux(261) =< V8 s(159) =< aux(261) with precondition: [V1=2,Out>=3,V>=V8+1,V4>=V8+1,V8+2>=Out] * Chain [30,89,106]: 2*s(159)+2 Such that:aux(261) =< V8 s(159) =< aux(261) with precondition: [V1=2,Out>=3,V>=V8+1,V4>=V8+1,V8+2>=Out] * Chain [30,88,106]: 2*s(159)+2 Such that:aux(261) =< V8 s(159) =< aux(261) with precondition: [V1=2,Out>=3,V>=V8+1,V4>=V8+1,V8+2>=Out] * Chain [30,87,106]: 5*s(34)+3*s(39)+2 Such that:aux(34) =< V aux(274) =< V8 s(39) =< aux(274) s(34) =< aux(34) with precondition: [V1=2,Out>=4,V>=V8+1,V4>=V8+1,2*V8+2>=Out] * Chain [30,86,106]: 4*s(40)+2 Such that:aux(277) =< V8 s(40) =< aux(277) with precondition: [V1=2,Out>=4,V>=V8+2,V4>=V8+1,2*V8+2>=Out] * Chain [30,85,106]: 7*s(42)+5*s(49)+2 Such that:aux(44) =< V aux(280) =< V8 s(42) =< aux(44) s(49) =< aux(280) with precondition: [V1=2,Out>=4,V>=V8+1,V4>=V8+1,2*V8+2>=Out] * Chain [30,84,106]: 4*s(54)+2 Such that:aux(283) =< V8 s(54) =< aux(283) with precondition: [V1=2,Out>=4,V>=V8+2,V4>=V8+1,2*V8+2>=Out] * Chain [30,83,106]: 3*s(151)+2*s(159)+2 Such that:aux(247) =< V aux(261) =< V8 s(151) =< aux(247) s(159) =< aux(261) with precondition: [V1=2,Out>=4,V>=V8+1,V4>=V8+1,2*V8+2>=Out] * Chain [30,82,106]: 3*s(154)+2 Such that:aux(288) =< V8 s(154) =< aux(288) with precondition: [V1=2,Out>=4,V>=V8+2,V4>=V8+1,2*V8+2>=Out] * Chain [30,81,106]: 3*s(155)+2*s(159)+2 Such that:aux(251) =< V aux(261) =< V8 s(155) =< aux(251) s(159) =< aux(261) with precondition: [V1=2,Out>=4,V>=V8+1,V4>=V8+1,2*V8+2>=Out] * Chain [30,80,106]: 3*s(158)+2 Such that:aux(293) =< V8 s(158) =< aux(293) with precondition: [V1=2,Out>=4,V>=V8+2,V4>=V8+1,2*V8+2>=Out] * Chain [30,70,106]: 3*s(57)+2 Such that:aux(296) =< V8 s(57) =< aux(296) with precondition: [V1=2,V=V8+1,Out>=4,V4>=V,2*V>=Out] * Chain [30,66,106]: 3*s(66)+2 Such that:aux(299) =< V8 s(66) =< aux(299) with precondition: [V1=2,V=V8+1,Out>=4,V4>=V,2*V>=Out] * Chain [30,58,106]: 2*s(159)+2 Such that:aux(261) =< V s(159) =< aux(261) with precondition: [V1=2,V=V8+1,Out>=3,V4>=V,V+1>=Out] * Chain [30,55,106]: 5*s(98)+2 Such that:aux(303) =< V8 s(98) =< aux(303) with precondition: [V1=2,V=V8+1,Out>=4,V4>=V,2*V>=Out] * Chain [30,47,106]: 2*s(159)+2 Such that:aux(261) =< V s(159) =< aux(261) with precondition: [V1=2,V=V8+1,Out>=3,V4>=V,V+1>=Out] * Chain [30,45,106]: 6*s(115)+2 Such that:aux(307) =< V8 s(115) =< aux(307) with precondition: [V1=2,V=V8+1,Out>=4,V4>=V,2*V>=Out] #### Cost of chains of start(V1,V,V4,V8): * Chain [116]: 1*s(1688)+0 Such that:s(1688) =< V with precondition: [V1>=0] * Chain [115]: 0 with precondition: [V1=1,V>=0] * Chain [114]: 0 with precondition: [V1=2,V=2] * Chain [113]: 163*s(1692)+136*s(1693)+401*s(1694)+4*s(1713)+4*s(1715)+13*s(1717)+274*s(1718)+274*s(1720)+2 Such that:s(1705) =< -V+V4+V8 s(1707) =< V-V4+V8 s(1708) =< V-V8 s(1710) =< V4-V8 s(1712) =< V8+1 aux(333) =< V aux(334) =< V4 aux(335) =< V8 s(1713) =< s(1705) s(1692) =< aux(333) s(1715) =< s(1707) s(1694) =< aux(335) s(1717) =< s(1712) s(1718) =< aux(333) s(1718) =< s(1708) s(1718) =< aux(334) s(1718) =< s(1710) s(1719) =< s(1718)*aux(335) s(1720) =< s(1719) s(1693) =< aux(334) with precondition: [V1=2,V>=0,V4>=0,V8>=0] * Chain [112]: 34*s(1727)+4*s(1731)+1*s(1732)+2 Such that:s(1730) =< V+1 s(1732) =< V4 aux(336) =< V4+1 s(1731) =< s(1730) s(1727) =< aux(336) with precondition: [V1=2,V8=0,V>=0,V4>=1] * Chain [111]: 1 with precondition: [V1=2,V8=0,V>=1,V4>=0] * Chain [110]: 34*s(1734)+2 Such that:aux(337) =< V8 s(1734) =< aux(337) with precondition: [V1=2,V4=V8+1,V4>=2,V>=V4] * Chain [109]: 17*s(1738)+2 Such that:s(1737) =< V8 s(1738) =< s(1737) with precondition: [V1=2,V=V8+1,V>=2,V4>=V] * Chain [108]: 0 with precondition: [V=0,V1>=1] * Chain [107]: 0 with precondition: [V=1,V1>=0] Closed-form bounds of start(V1,V,V4,V8): ------------------------------------- * Chain [116] with precondition: [V1>=0] - Upper bound: nat(V) - Complexity: n * Chain [115] with precondition: [V1=1,V>=0] - Upper bound: 0 - Complexity: constant * Chain [114] with precondition: [V1=2,V=2] - Upper bound: 0 - Complexity: constant * Chain [113] with precondition: [V1=2,V>=0,V4>=0,V8>=0] - Upper bound: 437*V+2+274*V*V8+136*V4+401*V8+(13*V8+13)+nat(-V+V4+V8)*4+nat(V-V4+V8)*4 - Complexity: n^2 * Chain [112] with precondition: [V1=2,V8=0,V>=0,V4>=1] - Upper bound: 4*V+35*V4+40 - Complexity: n * Chain [111] with precondition: [V1=2,V8=0,V>=1,V4>=0] - Upper bound: 1 - Complexity: constant * Chain [110] with precondition: [V1=2,V4=V8+1,V4>=2,V>=V4] - Upper bound: 34*V8+2 - Complexity: n * Chain [109] with precondition: [V1=2,V=V8+1,V>=2,V4>=V] - Upper bound: 17*V8+2 - Complexity: n * Chain [108] with precondition: [V=0,V1>=1] - Upper bound: 0 - Complexity: constant * Chain [107] with precondition: [V=1,V1>=0] - Upper bound: 0 - Complexity: constant ### Maximum cost of start(V1,V,V4,V8): max([max([1,nat(V),nat(V4)+2+nat(V+1)*4+nat(V4+1)*34]),nat(V)*274*nat(V8)+nat(V)*437+nat(V4)*136+nat(V8)*367+nat(V8+1)*13+nat(-V+V4+V8)*4+nat(V-V4+V8)*4+nat(V8)*17+(nat(V8)*17+2)]) Asymptotic class: n^2 * Total analysis performed in 15005 ms. ---------------------------------------- (20) BOUNDS(1, n^2)