WORST_CASE(Omega(n^1),O(n^1)) proof of /export/starexec/sandbox/benchmark/theBenchmark.trs # AProVE Commit ID: c69e44bd14796315568835c1ffa2502984884775 mhark 20210624 unpublished The Runtime Complexity (innermost) of the given CpxRelTRS could be proven to be BOUNDS(n^1, n^1). (0) CpxRelTRS (1) SInnermostTerminationProof [BOTH CONCRETE BOUNDS(ID, ID), 370 ms] (2) CpxRelTRS (3) RelTrsToWeightedTrsProof [BOTH BOUNDS(ID, ID), 0 ms] (4) CpxWeightedTrs (5) TypeInferenceProof [BOTH BOUNDS(ID, ID), 0 ms] (6) CpxTypedWeightedTrs (7) CompletionProof [UPPER BOUND(ID), 0 ms] (8) CpxTypedWeightedCompleteTrs (9) CpxTypedWeightedTrsToRntsProof [UPPER BOUND(ID), 0 ms] (10) CpxRNTS (11) CompleteCoflocoProof [FINISHED, 29.0 s] (12) BOUNDS(1, n^1) (13) RelTrsToDecreasingLoopProblemProof [LOWER BOUND(ID), 0 ms] (14) TRS for Loop Detection (15) DecreasingLoopProof [LOWER BOUND(ID), 0 ms] (16) BEST (17) proven lower bound (18) LowerBoundPropagationProof [FINISHED, 0 ms] (19) BOUNDS(n^1, INF) (20) TRS for Loop Detection ---------------------------------------- (0) Obligation: The Runtime Complexity (innermost) of the given CpxRelTRS could be proven to be BOUNDS(n^1, n^1). The TRS R consists of the following rules: COND(true, z0, z1) -> c(COND(and(gr(z0, 0), gr(z1, 0)), p(z0), p(z1)), AND(gr(z0, 0), gr(z1, 0)), GR(z0, 0)) COND(true, z0, z1) -> c1(COND(and(gr(z0, 0), gr(z1, 0)), p(z0), p(z1)), AND(gr(z0, 0), gr(z1, 0)), GR(z1, 0)) COND(true, z0, z1) -> c2(COND(and(gr(z0, 0), gr(z1, 0)), p(z0), p(z1)), P(z0)) COND(true, z0, z1) -> c3(COND(and(gr(z0, 0), gr(z1, 0)), p(z0), p(z1)), 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 The (relative) TRS S consists of the following rules: cond(true, z0, z1) -> cond(and(gr(z0, 0), gr(z1, 0)), p(z0), p(z1)) 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 ---------------------------------------- (1) SInnermostTerminationProof (BOTH CONCRETE BOUNDS(ID, ID)) proved innermost termination of relative rules ---------------------------------------- (2) Obligation: The Runtime Complexity (innermost) of the given CpxRelTRS could be proven to be BOUNDS(n^1, n^1). The TRS R consists of the following rules: COND(true, z0, z1) -> c(COND(and(gr(z0, 0), gr(z1, 0)), p(z0), p(z1)), AND(gr(z0, 0), gr(z1, 0)), GR(z0, 0)) COND(true, z0, z1) -> c1(COND(and(gr(z0, 0), gr(z1, 0)), p(z0), p(z1)), AND(gr(z0, 0), gr(z1, 0)), GR(z1, 0)) COND(true, z0, z1) -> c2(COND(and(gr(z0, 0), gr(z1, 0)), p(z0), p(z1)), P(z0)) COND(true, z0, z1) -> c3(COND(and(gr(z0, 0), gr(z1, 0)), p(z0), p(z1)), 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 The (relative) TRS S consists of the following rules: cond(true, z0, z1) -> cond(and(gr(z0, 0), gr(z1, 0)), p(z0), p(z1)) 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 ---------------------------------------- (3) RelTrsToWeightedTrsProof (BOTH BOUNDS(ID, ID)) Transformed relative TRS to weighted TRS ---------------------------------------- (4) Obligation: The Runtime Complexity (innermost) of the given CpxWeightedTrs could be proven to be BOUNDS(1, n^1). The TRS R consists of the following rules: COND(true, z0, z1) -> c(COND(and(gr(z0, 0), gr(z1, 0)), p(z0), p(z1)), AND(gr(z0, 0), gr(z1, 0)), GR(z0, 0)) [1] COND(true, z0, z1) -> c1(COND(and(gr(z0, 0), gr(z1, 0)), p(z0), p(z1)), AND(gr(z0, 0), gr(z1, 0)), GR(z1, 0)) [1] COND(true, z0, z1) -> c2(COND(and(gr(z0, 0), gr(z1, 0)), p(z0), p(z1)), P(z0)) [1] COND(true, z0, z1) -> c3(COND(and(gr(z0, 0), gr(z1, 0)), p(z0), p(z1)), P(z1)) [1] AND(true, true) -> c4 [1] AND(z0, false) -> c5 [1] AND(false, z0) -> c6 [1] GR(0, 0) -> c7 [1] GR(0, z0) -> c8 [1] GR(s(z0), 0) -> c9 [1] GR(s(z0), s(z1)) -> c10(GR(z0, z1)) [1] P(0) -> c11 [1] P(s(z0)) -> c12 [1] cond(true, z0, z1) -> cond(and(gr(z0, 0), gr(z1, 0)), p(z0), p(z1)) [0] 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 ---------------------------------------- (5) TypeInferenceProof (BOTH BOUNDS(ID, ID)) Infered types. ---------------------------------------- (6) Obligation: Runtime Complexity Weighted TRS with Types. The TRS R consists of the following rules: COND(true, z0, z1) -> c(COND(and(gr(z0, 0), gr(z1, 0)), p(z0), p(z1)), AND(gr(z0, 0), gr(z1, 0)), GR(z0, 0)) [1] COND(true, z0, z1) -> c1(COND(and(gr(z0, 0), gr(z1, 0)), p(z0), p(z1)), AND(gr(z0, 0), gr(z1, 0)), GR(z1, 0)) [1] COND(true, z0, z1) -> c2(COND(and(gr(z0, 0), gr(z1, 0)), p(z0), p(z1)), P(z0)) [1] COND(true, z0, z1) -> c3(COND(and(gr(z0, 0), gr(z1, 0)), p(z0), p(z1)), P(z1)) [1] AND(true, true) -> c4 [1] AND(z0, false) -> c5 [1] AND(false, z0) -> c6 [1] GR(0, 0) -> c7 [1] GR(0, z0) -> c8 [1] GR(s(z0), 0) -> c9 [1] GR(s(z0), s(z1)) -> c10(GR(z0, z1)) [1] P(0) -> c11 [1] P(s(z0)) -> c12 [1] cond(true, z0, z1) -> cond(and(gr(z0, 0), gr(z1, 0)), p(z0), p(z1)) [0] 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: COND :: true:false -> 0:s -> 0:s -> c:c1:c2:c3 true :: true:false c :: c:c1:c2:c3 -> c4:c5:c6 -> c7:c8:c9:c10 -> c:c1:c2:c3 and :: true:false -> true:false -> true:false gr :: 0:s -> 0:s -> true:false 0 :: 0:s p :: 0:s -> 0:s AND :: true:false -> true:false -> c4:c5:c6 GR :: 0:s -> 0:s -> c7:c8:c9:c10 c1 :: c:c1:c2:c3 -> c4:c5:c6 -> c7:c8:c9:c10 -> c:c1:c2:c3 c2 :: c:c1:c2:c3 -> c11:c12 -> c:c1:c2:c3 P :: 0:s -> c11:c12 c3 :: c:c1:c2:c3 -> c11:c12 -> c:c1:c2:c3 c4 :: c4:c5:c6 false :: true:false c5 :: c4:c5:c6 c6 :: c4:c5:c6 c7 :: c7:c8:c9:c10 c8 :: c7:c8:c9:c10 s :: 0:s -> 0:s c9 :: c7:c8:c9:c10 c10 :: c7:c8:c9:c10 -> c7:c8:c9:c10 c11 :: c11:c12 c12 :: c11:c12 cond :: true:false -> 0:s -> 0:s -> cond Rewrite Strategy: INNERMOST ---------------------------------------- (7) CompletionProof (UPPER BOUND(ID)) The TRS is a completely defined constructor system, as every type has a constant constructor and the following rules were added: cond(v0, v1, v2) -> null_cond [0] and(v0, v1) -> null_and [0] gr(v0, v1) -> null_gr [0] p(v0) -> null_p [0] COND(v0, v1, v2) -> null_COND [0] AND(v0, v1) -> null_AND [0] GR(v0, v1) -> null_GR [0] P(v0) -> null_P [0] And the following fresh constants: null_cond, null_and, null_gr, null_p, null_COND, null_AND, null_GR, null_P ---------------------------------------- (8) Obligation: Runtime Complexity Weighted TRS where all functions are completely defined. The underlying TRS is: Runtime Complexity Weighted TRS with Types. The TRS R consists of the following rules: COND(true, z0, z1) -> c(COND(and(gr(z0, 0), gr(z1, 0)), p(z0), p(z1)), AND(gr(z0, 0), gr(z1, 0)), GR(z0, 0)) [1] COND(true, z0, z1) -> c1(COND(and(gr(z0, 0), gr(z1, 0)), p(z0), p(z1)), AND(gr(z0, 0), gr(z1, 0)), GR(z1, 0)) [1] COND(true, z0, z1) -> c2(COND(and(gr(z0, 0), gr(z1, 0)), p(z0), p(z1)), P(z0)) [1] COND(true, z0, z1) -> c3(COND(and(gr(z0, 0), gr(z1, 0)), p(z0), p(z1)), P(z1)) [1] AND(true, true) -> c4 [1] AND(z0, false) -> c5 [1] AND(false, z0) -> c6 [1] GR(0, 0) -> c7 [1] GR(0, z0) -> c8 [1] GR(s(z0), 0) -> c9 [1] GR(s(z0), s(z1)) -> c10(GR(z0, z1)) [1] P(0) -> c11 [1] P(s(z0)) -> c12 [1] cond(true, z0, z1) -> cond(and(gr(z0, 0), gr(z1, 0)), p(z0), p(z1)) [0] 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] cond(v0, v1, v2) -> null_cond [0] and(v0, v1) -> null_and [0] gr(v0, v1) -> null_gr [0] p(v0) -> null_p [0] COND(v0, v1, v2) -> null_COND [0] AND(v0, v1) -> null_AND [0] GR(v0, v1) -> null_GR [0] P(v0) -> null_P [0] The TRS has the following type information: COND :: true:false:null_and:null_gr -> 0:s:null_p -> 0:s:null_p -> c:c1:c2:c3:null_COND true :: true:false:null_and:null_gr c :: c:c1:c2:c3:null_COND -> c4:c5:c6:null_AND -> c7:c8:c9: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 :: 0:s:null_p -> 0:s:null_p -> true:false:null_and:null_gr 0 :: 0:s:null_p p :: 0:s:null_p -> 0:s:null_p AND :: true:false:null_and:null_gr -> true:false:null_and:null_gr -> c4:c5:c6:null_AND GR :: 0:s:null_p -> 0:s:null_p -> c7:c8:c9:c10:null_GR c1 :: c:c1:c2:c3:null_COND -> c4:c5:c6:null_AND -> c7:c8:c9:c10:null_GR -> c:c1:c2:c3:null_COND c2 :: c:c1:c2:c3:null_COND -> c11:c12:null_P -> c:c1:c2:c3:null_COND P :: 0:s:null_p -> c11:c12:null_P c3 :: c:c1:c2:c3:null_COND -> c11:c12:null_P -> c:c1:c2:c3:null_COND c4 :: c4:c5:c6:null_AND false :: true:false:null_and:null_gr c5 :: c4:c5:c6:null_AND c6 :: c4:c5:c6:null_AND c7 :: c7:c8:c9:c10:null_GR c8 :: c7:c8:c9:c10:null_GR s :: 0:s:null_p -> 0:s:null_p c9 :: c7:c8:c9:c10:null_GR c10 :: c7:c8:c9:c10:null_GR -> c7:c8:c9:c10:null_GR c11 :: c11:c12:null_P c12 :: c11:c12:null_P cond :: true:false:null_and:null_gr -> 0:s:null_p -> 0:s:null_p -> null_cond null_cond :: null_cond null_and :: true:false:null_and:null_gr null_gr :: true:false:null_and:null_gr null_p :: 0:s:null_p null_COND :: c:c1:c2:c3:null_COND null_AND :: c4:c5:c6:null_AND null_GR :: c7:c8:c9:c10:null_GR null_P :: c11:c12:null_P Rewrite Strategy: INNERMOST ---------------------------------------- (9) CpxTypedWeightedTrsToRntsProof (UPPER BOUND(ID)) Transformed the TRS into an over-approximating RNTS by (improved) Size Abstraction. The constant constructors are abstracted as follows: true => 2 0 => 0 c4 => 1 false => 1 c5 => 2 c6 => 3 c7 => 0 c8 => 1 c9 => 2 c11 => 1 c12 => 2 null_cond => 0 null_and => 0 null_gr => 0 null_p => 0 null_COND => 0 null_AND => 0 null_GR => 0 null_P => 0 ---------------------------------------- (10) Obligation: Complexity RNTS consisting of the following rules: AND(z, z') -{ 1 }-> 3 :|: z = 1, z0 >= 0, z' = z0 AND(z, z') -{ 1 }-> 2 :|: z = z0, z0 >= 0, z' = 1 AND(z, z') -{ 1 }-> 1 :|: z = 2, z' = 2 AND(z, z') -{ 0 }-> 0 :|: v0 >= 0, v1 >= 0, z = v0, z' = v1 COND(z, z', z'') -{ 0 }-> 0 :|: v0 >= 0, z'' = v2, v1 >= 0, z = v0, z' = v1, v2 >= 0 COND(z, z', z'') -{ 1 }-> 1 + COND(and(gr(z0, 0), gr(z1, 0)), p(z0), p(z1)) + P(z0) :|: z = 2, z1 >= 0, z0 >= 0, z' = z0, z'' = z1 COND(z, z', z'') -{ 1 }-> 1 + COND(and(gr(z0, 0), gr(z1, 0)), p(z0), p(z1)) + P(z1) :|: z = 2, z1 >= 0, z0 >= 0, z' = z0, z'' = z1 COND(z, z', z'') -{ 1 }-> 1 + COND(and(gr(z0, 0), gr(z1, 0)), p(z0), p(z1)) + AND(gr(z0, 0), gr(z1, 0)) + GR(z0, 0) :|: z = 2, z1 >= 0, z0 >= 0, z' = z0, z'' = z1 COND(z, z', z'') -{ 1 }-> 1 + COND(and(gr(z0, 0), gr(z1, 0)), p(z0), p(z1)) + AND(gr(z0, 0), gr(z1, 0)) + GR(z1, 0) :|: z = 2, z1 >= 0, z0 >= 0, z' = z0, z'' = z1 GR(z, z') -{ 1 }-> 2 :|: z = 1 + z0, z0 >= 0, z' = 0 GR(z, z') -{ 1 }-> 1 :|: z0 >= 0, z = 0, z' = z0 GR(z, z') -{ 1 }-> 0 :|: z = 0, z' = 0 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 P(z) -{ 1 }-> 2 :|: z = 1 + z0, z0 >= 0 P(z) -{ 1 }-> 1 :|: z = 0 P(z) -{ 0 }-> 0 :|: v0 >= 0, z = v0 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 cond(z, z', z'') -{ 0 }-> cond(and(gr(z0, 0), gr(z1, 0)), p(z0), p(z1)) :|: z = 2, z1 >= 0, z0 >= 0, z' = z0, z'' = z1 cond(z, z', z'') -{ 0 }-> 0 :|: v0 >= 0, z'' = v2, v1 >= 0, z = v0, z' = v1, v2 >= 0 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. ---------------------------------------- (11) CompleteCoflocoProof (FINISHED) Transformed the RNTS (where only complete derivations are relevant) into cost relations for CoFloCo: eq(start(V1, V, V2),0,[fun(V1, V, V2, Out)],[V1 >= 0,V >= 0,V2 >= 0]). eq(start(V1, V, V2),0,[fun1(V1, V, Out)],[V1 >= 0,V >= 0]). eq(start(V1, V, V2),0,[fun2(V1, V, Out)],[V1 >= 0,V >= 0]). eq(start(V1, V, V2),0,[fun3(V1, Out)],[V1 >= 0]). eq(start(V1, V, V2),0,[cond(V1, V, V2, Out)],[V1 >= 0,V >= 0,V2 >= 0]). eq(start(V1, V, V2),0,[and(V1, V, Out)],[V1 >= 0,V >= 0]). eq(start(V1, V, V2),0,[gr(V1, V, Out)],[V1 >= 0,V >= 0]). eq(start(V1, V, V2),0,[p(V1, Out)],[V1 >= 0]). eq(fun(V1, V, V2, Out),1,[gr(V4, 0, Ret00100),gr(V3, 0, Ret00101),and(Ret00100, Ret00101, Ret0010),p(V4, Ret0011),p(V3, Ret0012),fun(Ret0010, Ret0011, Ret0012, Ret001),gr(V4, 0, Ret010),gr(V3, 0, Ret011),fun1(Ret010, Ret011, Ret01),fun2(V4, 0, Ret1)],[Out = 1 + Ret001 + Ret01 + Ret1,V1 = 2,V3 >= 0,V4 >= 0,V = V4,V2 = V3]). eq(fun(V1, V, V2, Out),1,[gr(V6, 0, Ret001001),gr(V5, 0, Ret001011),and(Ret001001, Ret001011, Ret00102),p(V6, Ret00111),p(V5, Ret00121),fun(Ret00102, Ret00111, Ret00121, Ret0013),gr(V6, 0, Ret0101),gr(V5, 0, Ret0111),fun1(Ret0101, Ret0111, Ret012),fun2(V5, 0, Ret11)],[Out = 1 + Ret0013 + Ret012 + Ret11,V1 = 2,V5 >= 0,V6 >= 0,V = V6,V2 = V5]). eq(fun(V1, V, V2, Out),1,[gr(V8, 0, Ret0100),gr(V7, 0, Ret01011),and(Ret0100, Ret01011, Ret0102),p(V8, Ret0112),p(V7, Ret0121),fun(Ret0102, Ret0112, Ret0121, Ret013),fun3(V8, Ret12)],[Out = 1 + Ret013 + Ret12,V1 = 2,V7 >= 0,V8 >= 0,V = V8,V2 = V7]). eq(fun(V1, V, V2, Out),1,[gr(V9, 0, Ret01001),gr(V10, 0, Ret01012),and(Ret01001, Ret01012, Ret0103),p(V9, Ret0113),p(V10, Ret0122),fun(Ret0103, Ret0113, Ret0122, Ret014),fun3(V10, Ret13)],[Out = 1 + Ret014 + Ret13,V1 = 2,V10 >= 0,V9 >= 0,V = V9,V2 = V10]). eq(fun1(V1, V, Out),1,[],[Out = 1,V1 = 2,V = 2]). eq(fun1(V1, V, Out),1,[],[Out = 2,V1 = V11,V11 >= 0,V = 1]). eq(fun1(V1, V, Out),1,[],[Out = 3,V1 = 1,V12 >= 0,V = V12]). eq(fun2(V1, V, Out),1,[],[Out = 0,V1 = 0,V = 0]). eq(fun2(V1, V, Out),1,[],[Out = 1,V13 >= 0,V1 = 0,V = V13]). eq(fun2(V1, V, Out),1,[],[Out = 2,V1 = 1 + V14,V14 >= 0,V = 0]). eq(fun2(V1, V, Out),1,[fun2(V16, V15, Ret14)],[Out = 1 + Ret14,V15 >= 0,V1 = 1 + V16,V16 >= 0,V = 1 + V15]). eq(fun3(V1, Out),1,[],[Out = 1,V1 = 0]). eq(fun3(V1, Out),1,[],[Out = 2,V1 = 1 + V17,V17 >= 0]). eq(cond(V1, V, V2, Out),0,[gr(V19, 0, Ret00),gr(V18, 0, Ret015),and(Ret00, Ret015, Ret0),p(V19, Ret15),p(V18, Ret2),cond(Ret0, Ret15, Ret2, Ret)],[Out = Ret,V1 = 2,V18 >= 0,V19 >= 0,V = V19,V2 = V18]). eq(and(V1, V, Out),0,[],[Out = 2,V1 = 2,V = 2]). eq(and(V1, V, Out),0,[],[Out = 1,V1 = V20,V20 >= 0,V = 1]). eq(and(V1, V, Out),0,[],[Out = 1,V1 = 1,V21 >= 0,V = V21]). eq(gr(V1, V, Out),0,[],[Out = 1,V1 = 0,V = 0]). eq(gr(V1, V, Out),0,[],[Out = 1,V22 >= 0,V1 = 0,V = V22]). eq(gr(V1, V, Out),0,[],[Out = 2,V1 = 1 + V23,V23 >= 0,V = 0]). eq(gr(V1, V, Out),0,[gr(V25, V24, Ret3)],[Out = Ret3,V24 >= 0,V1 = 1 + V25,V25 >= 0,V = 1 + V24]). eq(p(V1, Out),0,[],[Out = 0,V1 = 0]). eq(p(V1, Out),0,[],[Out = V26,V1 = 1 + V26,V26 >= 0]). eq(cond(V1, V, V2, Out),0,[],[Out = 0,V28 >= 0,V2 = V29,V27 >= 0,V1 = V28,V = V27,V29 >= 0]). eq(and(V1, V, Out),0,[],[Out = 0,V31 >= 0,V30 >= 0,V1 = V31,V = V30]). eq(gr(V1, V, Out),0,[],[Out = 0,V33 >= 0,V32 >= 0,V1 = V33,V = V32]). eq(p(V1, Out),0,[],[Out = 0,V34 >= 0,V1 = V34]). eq(fun(V1, V, V2, Out),0,[],[Out = 0,V35 >= 0,V2 = V36,V37 >= 0,V1 = V35,V = V37,V36 >= 0]). eq(fun1(V1, V, Out),0,[],[Out = 0,V39 >= 0,V38 >= 0,V1 = V39,V = V38]). eq(fun2(V1, V, Out),0,[],[Out = 0,V41 >= 0,V40 >= 0,V1 = V41,V = V40]). eq(fun3(V1, Out),0,[],[Out = 0,V42 >= 0,V1 = V42]). input_output_vars(fun(V1,V,V2,Out),[V1,V,V2],[Out]). input_output_vars(fun1(V1,V,Out),[V1,V],[Out]). input_output_vars(fun2(V1,V,Out),[V1,V],[Out]). input_output_vars(fun3(V1,Out),[V1],[Out]). input_output_vars(cond(V1,V,V2,Out),[V1,V,V2],[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 : [gr/3] 2. non_recursive : [p/2] 3. recursive : [cond/4] 4. non_recursive : [fun1/3] 5. recursive : [fun2/3] 6. non_recursive : [fun3/2] 7. recursive [non_tail] : [fun/4] 8. non_recursive : [start/3] #### Obtained direct recursion through partial evaluation 0. SCC is partially evaluated into and/3 1. SCC is partially evaluated into gr/3 2. SCC is partially evaluated into p/2 3. SCC is partially evaluated into cond/4 4. SCC is partially evaluated into fun1/3 5. SCC is partially evaluated into fun2/3 6. SCC is partially evaluated into fun3/2 7. SCC is partially evaluated into fun/4 8. SCC is partially evaluated into start/3 Control-Flow Refinement of Cost Relations ===================================== ### Specialization of cost equations and/3 * CE 31 is refined into CE [38] * CE 29 is refined into CE [39] * CE 28 is refined into CE [40] * CE 30 is refined into CE [41] ### Cost equations --> "Loop" of and/3 * CEs [38] --> Loop 27 * CEs [39] --> Loop 28 * CEs [40] --> Loop 29 * CEs [41] --> Loop 30 ### Ranking functions of CR and(V1,V,Out) #### Partial ranking functions of CR and(V1,V,Out) ### Specialization of cost equations gr/3 * CE 35 is refined into CE [42] * CE 33 is refined into CE [43] * CE 32 is refined into CE [44] * CE 34 is refined into CE [45] ### Cost equations --> "Loop" of gr/3 * CEs [45] --> Loop 31 * CEs [42] --> Loop 32 * CEs [43] --> Loop 33 * CEs [44] --> Loop 34 ### Ranking functions of CR gr(V1,V,Out) * RF of phase [31]: [V,V1] #### Partial ranking functions of CR gr(V1,V,Out) * Partial RF of phase [31]: - RF of loop [31:1]: V V1 ### Specialization of cost equations p/2 * CE 37 is refined into CE [46] * CE 36 is refined into CE [47] ### Cost equations --> "Loop" of p/2 * CEs [46] --> Loop 35 * CEs [47] --> Loop 36 ### Ranking functions of CR p(V1,Out) #### Partial ranking functions of CR p(V1,Out) ### Specialization of cost equations cond/4 * CE 27 is refined into CE [48] * CE 26 is refined into CE [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] ### Cost equations --> "Loop" of cond/4 * CEs [67] --> Loop 37 * CEs [66] --> Loop 38 * CEs [65] --> Loop 39 * CEs [64] --> Loop 40 * CEs [71,75,83,87] --> Loop 41 * CEs [61,77] --> Loop 42 * CEs [60,76] --> Loop 43 * CEs [63,70,74,79,82,86] --> Loop 44 * CEs [62,78] --> Loop 45 * CEs [53,57] --> Loop 46 * CEs [55,59,69,73,81,85] --> Loop 47 * CEs [49,50,52,56] --> Loop 48 * CEs [51,54,58,68,72,80,84] --> Loop 49 * CEs [48] --> Loop 50 ### Ranking functions of CR cond(V1,V,V2,Out) * RF of phase [37]: [V,V2] #### Partial ranking functions of CR cond(V1,V,V2,Out) * Partial RF of phase [37]: - RF of loop [37:1]: V V2 ### Specialization of cost equations fun1/3 * CE 17 is refined into CE [88] * CE 15 is refined into CE [89] * CE 14 is refined into CE [90] * CE 16 is refined into CE [91] ### Cost equations --> "Loop" of fun1/3 * CEs [88] --> Loop 51 * CEs [89] --> Loop 52 * CEs [90] --> Loop 53 * CEs [91] --> Loop 54 ### Ranking functions of CR fun1(V1,V,Out) #### Partial ranking functions of CR fun1(V1,V,Out) ### Specialization of cost equations fun2/3 * CE 20 is refined into CE [92] * CE 19 is refined into CE [93] * CE 18 is refined into CE [94] * CE 22 is refined into CE [95] * CE 21 is refined into CE [96] ### Cost equations --> "Loop" of fun2/3 * CEs [96] --> Loop 55 * CEs [92] --> Loop 56 * CEs [93] --> Loop 57 * CEs [94,95] --> Loop 58 ### Ranking functions of CR fun2(V1,V,Out) * RF of phase [55]: [V,V1] #### Partial ranking functions of CR fun2(V1,V,Out) * Partial RF of phase [55]: - RF of loop [55:1]: V V1 ### Specialization of cost equations fun3/2 * CE 24 is refined into CE [97] * CE 25 is refined into CE [98] * CE 23 is refined into CE [99] ### Cost equations --> "Loop" of fun3/2 * CEs [97] --> Loop 59 * CEs [98] --> Loop 60 * CEs [99] --> Loop 61 ### Ranking functions of CR fun3(V1,Out) #### Partial ranking functions of CR fun3(V1,Out) ### Specialization of cost equations fun/4 * CE 13 is refined into CE [100] * CE 9 is refined into CE [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,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,429,430,431,432,433,434,435,436,437,438,439,440,441,442,443,444,445,446,447,448,449,450,451,452,453,454,455,456,457,458,459,460,461,462,463,464,465,466,467,468,469,470,471,472,473,474,475,476,477,478,479,480,481,482,483,484,485,486,487,488,489,490,491,492,493,494,495,496,497,498,499,500,501,502,503,504,505,506,507,508,509,510,511,512,513,514,515,516,517,518,519,520,521,522,523,524,525,526,527,528,529,530,531,532,533,534,535,536,537,538,539,540,541,542,543,544,545,546,547,548,549,550,551,552,553,554,555,556,557,558,559,560,561,562,563,564,565,566,567,568,569,570,571,572,573,574,575,576,577,578,579,580,581,582,583,584,585,586,587,588,589,590,591,592,593,594,595,596,597,598,599,600,601,602,603,604,605,606,607,608,609,610,611,612,613,614,615,616,617,618,619,620,621,622,623,624,625,626,627,628,629,630,631,632,633,634,635,636,637,638,639,640,641,642,643,644,645,646,647,648,649,650,651,652,653,654,655,656,657,658,659,660,661,662,663,664,665,666] * CE 10 is refined into CE [667,668,669,670,671,672,673,674,675,676,677,678,679,680,681,682,683,684,685,686,687,688,689,690,691,692,693,694,695,696,697,698,699,700,701,702,703,704,705,706,707,708,709,710,711,712,713,714,715,716,717,718,719,720,721,722,723,724,725,726,727,728,729,730,731,732,733,734,735,736,737,738,739,740,741,742,743,744,745,746,747,748,749,750,751,752,753,754,755,756,757,758,759,760,761,762,763,764,765,766,767,768,769,770,771,772,773,774,775,776,777,778,779,780,781,782,783,784,785,786,787,788,789,790,791,792,793,794,795,796,797,798,799,800,801,802,803,804,805,806,807,808,809,810,811,812,813,814,815,816,817,818,819,820,821,822,823,824,825,826,827,828,829,830,831,832,833,834,835,836,837,838,839,840,841,842,843,844,845,846,847,848,849,850,851,852,853,854,855,856,857,858,859,860,861,862,863,864,865,866,867,868,869,870,871,872,873,874,875,876,877,878,879,880,881,882,883,884,885,886,887,888,889,890,891,892,893,894,895,896,897,898,899,900,901,902,903,904,905,906,907,908,909,910,911,912,913,914,915,916,917,918,919,920,921,922,923,924,925,926,927,928,929,930,931,932,933,934,935,936,937,938,939,940,941,942,943,944,945,946,947,948,949,950,951,952,953,954,955,956,957,958,959,960,961,962,963,964,965,966,967,968,969,970,971,972,973,974,975,976,977,978,979,980,981,982,983,984,985,986,987,988,989,990,991,992,993,994,995,996,997,998,999,1000,1001,1002,1003,1004,1005,1006,1007,1008,1009,1010,1011,1012,1013,1014,1015,1016,1017,1018,1019,1020,1021,1022,1023,1024,1025,1026,1027,1028,1029,1030,1031,1032,1033,1034,1035,1036,1037,1038,1039,1040,1041,1042,1043,1044,1045,1046,1047,1048,1049,1050,1051,1052,1053,1054,1055,1056,1057,1058,1059,1060,1061,1062,1063,1064,1065,1066,1067,1068,1069,1070,1071,1072,1073,1074,1075,1076,1077,1078,1079,1080,1081,1082,1083,1084,1085,1086,1087,1088,1089,1090,1091,1092,1093,1094,1095,1096,1097,1098,1099,1100,1101,1102,1103,1104,1105,1106,1107,1108,1109,1110,1111,1112,1113,1114,1115,1116,1117,1118,1119,1120,1121,1122,1123,1124,1125,1126,1127,1128,1129,1130,1131,1132,1133,1134,1135,1136,1137,1138,1139,1140,1141,1142,1143,1144,1145,1146,1147,1148,1149,1150,1151,1152,1153,1154,1155,1156,1157,1158,1159,1160,1161,1162,1163,1164,1165,1166,1167,1168,1169,1170,1171,1172,1173,1174,1175,1176,1177,1178,1179,1180,1181,1182,1183,1184,1185,1186,1187,1188,1189,1190,1191,1192,1193,1194,1195,1196,1197,1198,1199,1200,1201,1202,1203,1204,1205,1206,1207,1208,1209,1210,1211,1212,1213,1214,1215,1216,1217,1218,1219,1220,1221,1222,1223,1224,1225,1226,1227,1228,1229,1230,1231,1232] * CE 11 is refined into CE [1233,1234,1235,1236,1237,1238,1239,1240,1241,1242,1243,1244,1245,1246,1247,1248,1249,1250,1251,1252,1253,1254,1255,1256,1257,1258,1259,1260,1261,1262,1263,1264,1265,1266,1267,1268,1269,1270,1271,1272,1273,1274,1275,1276,1277,1278,1279,1280,1281,1282,1283,1284,1285,1286,1287,1288,1289,1290,1291,1292,1293,1294,1295,1296,1297,1298,1299,1300,1301,1302,1303,1304,1305,1306,1307,1308,1309,1310,1311,1312,1313,1314,1315,1316] * CE 12 is refined into CE [1317,1318,1319,1320,1321,1322,1323,1324,1325,1326,1327,1328,1329,1330,1331,1332,1333,1334,1335,1336,1337,1338,1339,1340,1341,1342,1343,1344,1345,1346,1347,1348,1349,1350,1351,1352,1353,1354,1355,1356,1357,1358,1359,1360,1361,1362,1363,1364,1365,1366,1367,1368,1369,1370,1371,1372,1373,1374,1375,1376,1377,1378,1379,1380,1381,1382,1383,1384,1385,1386,1387,1388,1389,1390,1391,1392,1393,1394,1395,1396,1397,1398,1399,1400] ### Cost equations --> "Loop" of fun/4 * CEs [343,915] --> Loop 62 * CEs [345,347,349,351,917,919,921,923,1270,1356] --> Loop 63 * CEs [344,916] --> Loop 64 * CEs [346,348,350,352,918,920,922,924,1269,1355] --> Loop 65 * CEs [333,905] --> Loop 66 * CEs [335,337,339,341,907,909,911,913,1268,1354] --> Loop 67 * CEs [334,906] --> Loop 68 * CEs [336,338,340,342,908,910,912,914,1267,1353] --> Loop 69 * CEs [323,895] --> Loop 70 * CEs [325,327,329,331,897,899,901,903,1266,1352] --> Loop 71 * CEs [324,896] --> Loop 72 * CEs [326,328,330,332,898,900,902,904,1265,1351] --> Loop 73 * CEs [313,885] --> Loop 74 * CEs [315,317,319,321,887,889,891,893,1264,1350] --> Loop 75 * CEs [314,886] --> Loop 76 * CEs [316,318,320,322,888,890,892,894,1263,1349] --> Loop 77 * CEs [383,439,573,657,955,1015,1139,1223] --> Loop 78 * CEs [385,387,389,391,441,443,445,447,575,577,579,581,659,661,663,665,957,959,961,963,1017,1019,1021,1023,1141,1143,1145,1147,1225,1227,1229,1231,1278,1286,1306,1316,1364,1374,1390,1400] --> Loop 79 * CEs [384,440,574,658,956,1016,1140,1224] --> Loop 80 * CEs [386,388,390,392,442,444,446,448,576,578,580,582,660,662,664,666,958,960,962,964,1018,1020,1022,1024,1142,1144,1146,1148,1226,1228,1230,1232,1277,1285,1305,1315,1363,1373,1389,1399] --> Loop 81 * CEs [373,425,563,643,945,999,1129,1207] --> Loop 82 * CEs [374,426,564,644,946,1000,1130,1208] --> Loop 83 * CEs [363,411,551,627,935,985,1119,1193] --> Loop 84 * CEs [364,412,552,628,936,986,1120,1194] --> Loop 85 * CEs [353,397,531,601,925,969,1101,1169] --> Loop 86 * CEs [401,409,605,617,1280,1309] --> Loop 87 * CEs [354,398,532,602,926,970,1102,1170] --> Loop 88 * CEs [277,283,474,480] --> Loop 89 * CEs [849,855,1047,1053] --> Loop 90 * CEs [278,279,281,284,285,287,475,476,478,481,482,484,850,856,1048,1054,1258,1291] --> Loop 91 * CEs [851,853,857,859,1049,1051,1055,1057,1343,1377] --> Loop 92 * CEs [280,282,286,288,477,479,483,485,852,854,858,860,1050,1052,1056,1058,1257,1290,1344,1378] --> Loop 93 * CEs [265,271,459,466] --> Loop 94 * CEs [837,843,1035,1041] --> Loop 95 * CEs [839,841,845,847,1037,1039,1043,1045,1341,1375] --> Loop 96 * CEs [268,270,274,276,462,464,470,473,840,842,846,848,1038,1040,1044,1046,1255,1288,1342,1376] --> Loop 97 * CEs [301,307,421,431,511,517,639,649] --> Loop 98 * CEs [873,879,995,1006,1081,1087,1203,1214] --> Loop 99 * CEs [302,303,305,308,309,311,375,377,379,381,422,423,427,429,432,433,435,437,512,513,515,518,519,521,565,567,569,571,640,641,645,647,650,651,653,655,874,880,947,949,951,953,996,1001,1004,1007,1010,1013,1082,1088,1131,1133,1135,1137,1204,1209,1212,1215,1218,1221,1262,1276,1284,1296,1304,1314,1362,1372,1388,1398] --> Loop 100 * CEs [875,877,881,883,997,1003,1008,1012,1083,1085,1089,1091,1205,1211,1216,1220,1347,1370,1381,1396] --> Loop 101 * CEs [304,306,310,312,376,378,380,382,424,428,430,434,436,438,514,516,520,522,566,568,570,572,642,646,648,652,654,656,876,878,882,884,948,950,952,954,998,1002,1005,1009,1011,1014,1084,1086,1090,1092,1132,1134,1136,1138,1206,1210,1213,1217,1219,1222,1261,1275,1283,1295,1303,1313,1348,1361,1371,1382,1387,1397] --> Loop 102 * CEs [289,295,393,403,496,503,597,608] --> Loop 103 * CEs [861,867,965,976,1069,1075,1165,1176] --> Loop 104 * CEs [863,865,869,871,967,973,978,982,1071,1073,1077,1079,1167,1173,1178,1182,1345,1365,1379,1391] --> Loop 105 * CEs [292,294,298,300,396,406,499,501,507,510,600,612,864,866,870,872,968,979,1072,1074,1078,1080,1168,1179,1259,1293,1346,1380] --> Loop 106 * CEs [727,731,788,792] --> Loop 107 * CEs [161,165,219,223] --> Loop 108 * CEs [162,166,220,224,728,732,789,793] --> Loop 109 * CEs [729,733,735,737,790,794,796,798,1326,1335] --> Loop 110 * CEs [163,167,169,171,221,225,227,229,1241,1249] --> Loop 111 * CEs [164,168,170,172,222,226,228,230,730,734,736,738,791,795,797,799,1242,1250,1325,1334] --> Loop 112 * CEs [715,719,769,774] --> Loop 113 * CEs [717,721,723,725,771,777,783,786,1324,1333] --> Loop 114 * CEs [751,755,825,829,1111,1115,1185,1189] --> Loop 115 * CEs [185,189,253,257,543,547,619,623] --> Loop 116 * CEs [186,190,254,258,544,548,620,624,752,756,826,830,1112,1116,1186,1190] --> Loop 117 * CEs [365,367,369,371,413,415,417,419,553,555,558,561,629,631,634,637,753,757,759,761,827,831,833,835,937,939,941,943,987,989,991,993,1113,1117,1121,1123,1125,1127,1187,1191,1195,1197,1199,1201,1274,1282,1302,1312,1330,1340,1360,1369,1386,1395] --> Loop 118 * CEs [187,191,193,195,255,259,261,263,545,549,557,560,621,625,633,636,1245,1253,1300,1310] --> Loop 119 * CEs [188,192,194,196,256,260,262,264,366,368,370,372,414,416,418,420,546,550,554,556,559,562,622,626,630,632,635,638,754,758,760,762,828,832,834,836,938,940,942,944,988,990,992,994,1114,1118,1122,1124,1126,1128,1188,1192,1196,1198,1200,1202,1246,1254,1273,1281,1301,1311,1329,1339,1359,1368,1385,1394] --> Loop 120 * CEs [739,743,806,811,1093,1097,1155,1160] --> Loop 121 * CEs [355,357,359,361,399,407,533,535,538,541,603,614,741,745,747,749,808,814,820,823,927,929,931,933,971,974,980,983,1095,1099,1103,1105,1107,1109,1157,1163,1171,1174,1180,1183,1272,1299,1328,1338,1358,1367,1384,1393] --> Loop 122 * CEs [101,107,117,123,149,153,197,203,207,449,455,667,673,683,689,763,773,1025,1031] --> Loop 123 * CEs [102,103,108,111,118,119,124,127,150,154,198,199,204,208,211,450,451,456,465,668,669,674,677,684,685,690,693,716,720,764,765,770,775,779,1026,1027,1032] --> Loop 124 * CEs [104,112,120,128,200,212,266,267,269,272,273,275,452,460,461,463,467,469,472,670,678,686,694,766,780,838,844,1028,1036,1042,1256,1289] --> Loop 125 * CEs [105,109,113,115,121,125,129,131,151,155,157,159,201,205,209,213,215,217,453,457,468,471,671,675,679,681,687,691,695,697,767,776,781,785,1029,1033,1233,1235,1239,1247,1287,1317,1319,1331] --> Loop 126 * CEs [106,110,114,116,122,126,130,132,152,156,158,160,202,206,210,214,216,218,454,458,672,676,680,682,688,692,696,698,718,722,724,726,768,772,778,782,784,787,1030,1034,1234,1236,1240,1248,1318,1320,1323,1332] --> Loop 127 * CEs [133,139,173,177,231,237,241,486,492,523,527,583,589,593,699,705,800,810,1059,1065,1149,1159] --> Loop 128 * CEs [134,135,140,143,174,178,232,233,238,242,245,487,488,493,502,524,528,584,585,590,594,607,700,701,706,709,740,744,801,802,807,812,816,1060,1061,1066,1094,1098,1150,1151,1156,1161] --> Loop 129 * CEs [136,144,234,246,290,291,293,296,297,299,394,395,404,405,489,497,498,500,504,506,509,586,598,599,609,611,702,710,803,817,862,868,966,977,1062,1070,1076,1152,1166,1177,1260,1294] --> Loop 130 * CEs [137,141,145,147,175,179,181,183,235,239,243,247,249,251,490,494,505,508,525,529,537,540,587,591,595,610,613,616,703,707,711,713,804,813,818,822,1063,1067,1153,1162,1237,1243,1251,1292,1297,1307,1321,1336] --> Loop 131 * CEs [138,142,146,148,176,180,182,184,236,240,244,248,250,252,356,358,360,362,400,402,408,410,491,495,526,530,534,536,539,542,588,592,596,604,606,615,618,704,708,712,714,742,746,748,750,805,809,815,819,821,824,928,930,932,934,972,975,981,984,1064,1068,1096,1100,1104,1106,1108,1110,1154,1158,1164,1172,1175,1181,1184,1238,1244,1252,1271,1279,1298,1308,1322,1327,1337,1357,1366,1383,1392] --> Loop 132 * CEs [100] --> Loop 133 ### Ranking functions of CR fun(V1,V,V2,Out) * RF of phase [62,63,64,65]: [V,V2] #### Partial ranking functions of CR fun(V1,V,V2,Out) * Partial RF of phase [62,63,64,65]: - RF of loop [62:1,63:1,64:1,65:1]: V V2 ### Specialization of cost equations start/3 * CE 1 is refined into CE [1401,1402,1403,1404,1405,1406,1407,1408,1409,1410,1411,1412,1413,1414,1415,1416,1417,1418,1419,1420,1421,1422,1423,1424,1425,1426,1427,1428,1429,1430,1431,1432,1433,1434,1435,1436,1437,1438,1439,1440] * CE 2 is refined into CE [1441,1442,1443,1444] * CE 3 is refined into CE [1445,1446,1447,1448,1449,1450] * CE 4 is refined into CE [1451,1452,1453] * CE 5 is refined into CE [1454,1455,1456,1457] * CE 6 is refined into CE [1458,1459,1460,1461] * CE 7 is refined into CE [1462,1463,1464,1465,1466] * CE 8 is refined into CE [1467,1468] ### Cost equations --> "Loop" of start/3 * CEs [1446,1463] --> Loop 134 * CEs [1420,1424,1425,1426,1457] --> Loop 135 * CEs [1415,1416,1417,1418,1419,1456] --> Loop 136 * CEs [1442,1459] --> Loop 137 * CEs [1443,1455,1460] --> Loop 138 * CEs [1401,1402,1403,1404,1405,1406,1407,1408,1409,1410,1411,1412,1413,1414,1421,1422,1423,1427,1428,1429,1430,1431,1432,1433,1434,1435,1436,1437,1438,1439] --> Loop 139 * CEs [1441,1458] --> Loop 140 * CEs [1440,1444,1445,1447,1448,1449,1450,1451,1452,1453,1454,1461,1462,1464,1465,1466,1467,1468] --> Loop 141 ### Ranking functions of CR start(V1,V,V2) #### Partial ranking functions of CR start(V1,V,V2) Computing Bounds ===================================== #### Cost of chains of and(V1,V,Out): * Chain [30]: 0 with precondition: [V1=1,Out=1,V>=0] * Chain [29]: 0 with precondition: [V1=2,V=2,Out=2] * Chain [28]: 0 with precondition: [V=1,Out=1,V1>=0] * Chain [27]: 0 with precondition: [Out=0,V1>=0,V>=0] #### Cost of chains of gr(V1,V,Out): * Chain [[31],34]: 0 with precondition: [Out=1,V1>=1,V>=V1] * Chain [[31],33]: 0 with precondition: [Out=2,V>=1,V1>=V+1] * Chain [[31],32]: 0 with precondition: [Out=0,V1>=1,V>=1] * Chain [34]: 0 with precondition: [V1=0,Out=1,V>=0] * Chain [33]: 0 with precondition: [V=0,Out=2,V1>=1] * Chain [32]: 0 with precondition: [Out=0,V1>=0,V>=0] #### Cost of chains of p(V1,Out): * Chain [36]: 0 with precondition: [Out=0,V1>=0] * Chain [35]: 0 with precondition: [V1=Out+1,V1>=1] #### Cost of chains of cond(V1,V,V2,Out): * Chain [[37],50]: 0 with precondition: [V1=2,Out=0,V>=1,V2>=1] * Chain [[37],49,50]: 0 with precondition: [V1=2,Out=0,V>=1,V2>=1] * Chain [[37],48,50]: 0 with precondition: [V1=2,Out=0,V>=1,V2>=V] * Chain [[37],47,50]: 0 with precondition: [V1=2,Out=0,V>=1,V2>=2] * Chain [[37],46,50]: 0 with precondition: [V1=2,Out=0,V>=1,V2>=V+1] * Chain [[37],45,50]: 0 with precondition: [V1=2,Out=0,V2>=1,V>=V2] * Chain [[37],44,50]: 0 with precondition: [V1=2,Out=0,V>=2,V2>=1] * Chain [[37],43,50]: 0 with precondition: [V1=2,Out=0,V2>=1,V>=V2] * Chain [[37],42,50]: 0 with precondition: [V1=2,Out=0,V2>=1,V>=V2+1] * Chain [[37],41,50]: 0 with precondition: [V1=2,Out=0,V>=2,V2>=2] * Chain [[37],40,50]: 0 with precondition: [V1=2,Out=0,V>=2,V2>=2] * Chain [[37],40,49,50]: 0 with precondition: [V1=2,Out=0,V>=2,V2>=2] * Chain [[37],40,48,50]: 0 with precondition: [V1=2,Out=0,V>=2,V2>=2] * Chain [[37],40,45,50]: 0 with precondition: [V1=2,Out=0,V>=2,V2>=2] * Chain [[37],40,43,50]: 0 with precondition: [V1=2,Out=0,V>=2,V2>=2] * Chain [[37],39,50]: 0 with precondition: [V1=2,Out=0,V>=2,V2>=2] * Chain [[37],39,49,50]: 0 with precondition: [V1=2,Out=0,V>=2,V2>=2] * Chain [[37],39,48,50]: 0 with precondition: [V1=2,Out=0,V>=2,V2>=2] * Chain [[37],39,47,50]: 0 with precondition: [V1=2,Out=0,V>=2,V2>=3] * Chain [[37],39,46,50]: 0 with precondition: [V1=2,Out=0,V>=2,V2>=3] * Chain [[37],39,45,50]: 0 with precondition: [V1=2,Out=0,V2>=2,V>=V2] * Chain [[37],39,43,50]: 0 with precondition: [V1=2,Out=0,V2>=2,V>=V2] * Chain [[37],38,50]: 0 with precondition: [V1=2,Out=0,V>=2,V2>=2] * Chain [[37],38,49,50]: 0 with precondition: [V1=2,Out=0,V>=2,V2>=2] * Chain [[37],38,48,50]: 0 with precondition: [V1=2,Out=0,V>=2,V2>=V] * Chain [[37],38,45,50]: 0 with precondition: [V1=2,Out=0,V>=2,V2>=2] * Chain [[37],38,44,50]: 0 with precondition: [V1=2,Out=0,V>=3,V2>=2] * Chain [[37],38,43,50]: 0 with precondition: [V1=2,Out=0,V>=2,V2>=2] * Chain [[37],38,42,50]: 0 with precondition: [V1=2,Out=0,V>=3,V2>=2] * Chain [50]: 0 with precondition: [Out=0,V1>=0,V>=0,V2>=0] * Chain [49,50]: 0 with precondition: [V1=2,Out=0,V>=0,V2>=0] * Chain [48,50]: 0 with precondition: [V1=2,V=0,Out=0,V2>=0] * Chain [47,50]: 0 with precondition: [V1=2,Out=0,V>=0,V2>=1] * Chain [46,50]: 0 with precondition: [V1=2,V=0,Out=0,V2>=1] * Chain [45,50]: 0 with precondition: [V1=2,V2=0,Out=0,V>=0] * Chain [44,50]: 0 with precondition: [V1=2,Out=0,V>=1,V2>=0] * Chain [43,50]: 0 with precondition: [V1=2,V2=0,Out=0,V>=0] * Chain [42,50]: 0 with precondition: [V1=2,V2=0,Out=0,V>=1] * Chain [41,50]: 0 with precondition: [V1=2,Out=0,V>=1,V2>=1] * Chain [40,50]: 0 with precondition: [V1=2,Out=0,V>=1,V2>=1] * Chain [40,49,50]: 0 with precondition: [V1=2,Out=0,V>=1,V2>=1] * Chain [40,48,50]: 0 with precondition: [V1=2,Out=0,V>=1,V2>=1] * Chain [40,45,50]: 0 with precondition: [V1=2,Out=0,V>=1,V2>=1] * Chain [40,43,50]: 0 with precondition: [V1=2,Out=0,V>=1,V2>=1] * Chain [39,50]: 0 with precondition: [V1=2,Out=0,V>=1,V2>=1] * Chain [39,49,50]: 0 with precondition: [V1=2,Out=0,V>=1,V2>=1] * Chain [39,48,50]: 0 with precondition: [V1=2,Out=0,V>=1,V2>=1] * Chain [39,47,50]: 0 with precondition: [V1=2,Out=0,V>=1,V2>=2] * Chain [39,46,50]: 0 with precondition: [V1=2,Out=0,V>=1,V2>=2] * Chain [39,45,50]: 0 with precondition: [V1=2,V2=1,Out=0,V>=1] * Chain [39,43,50]: 0 with precondition: [V1=2,V2=1,Out=0,V>=1] * Chain [38,50]: 0 with precondition: [V1=2,Out=0,V>=1,V2>=1] * Chain [38,49,50]: 0 with precondition: [V1=2,Out=0,V>=1,V2>=1] * Chain [38,48,50]: 0 with precondition: [V1=2,V=1,Out=0,V2>=1] * Chain [38,45,50]: 0 with precondition: [V1=2,Out=0,V>=1,V2>=1] * Chain [38,44,50]: 0 with precondition: [V1=2,Out=0,V>=2,V2>=1] * Chain [38,43,50]: 0 with precondition: [V1=2,Out=0,V>=1,V2>=1] * Chain [38,42,50]: 0 with precondition: [V1=2,Out=0,V>=2,V2>=1] #### Cost of chains of fun1(V1,V,Out): * Chain [54]: 1 with precondition: [V1=1,Out=3,V>=0] * Chain [53]: 1 with precondition: [V1=2,V=2,Out=1] * Chain [52]: 1 with precondition: [V=1,Out=2,V1>=0] * Chain [51]: 0 with precondition: [Out=0,V1>=0,V>=0] #### Cost of chains of fun2(V1,V,Out): * Chain [[55],58]: 1*it(55)+1 Such that:it(55) =< Out with precondition: [Out>=1,V1>=Out,V>=Out] * Chain [[55],57]: 1*it(55)+1 Such that:it(55) =< Out with precondition: [V1+1=Out,V1>=1,V>=V1] * Chain [[55],56]: 1*it(55)+1 Such that:it(55) =< Out with precondition: [V+2=Out,V>=1,V1>=V+1] * Chain [58]: 1 with precondition: [Out=0,V1>=0,V>=0] * Chain [57]: 1 with precondition: [V1=0,Out=1,V>=0] * Chain [56]: 1 with precondition: [V=0,Out=2,V1>=1] #### Cost of chains of fun3(V1,Out): * Chain [61]: 1 with precondition: [V1=0,Out=1] * Chain [60]: 0 with precondition: [Out=0,V1>=0] * Chain [59]: 1 with precondition: [Out=2,V1>=1] #### Cost of chains of fun(V1,V,V2,Out): * Chain [[62,63,64,65],133]: 10*it(62)+0 Such that:aux(5) =< V aux(6) =< V2 it(62) =< aux(5) it(62) =< aux(6) with precondition: [V1=2,V>=1,V2>=1,Out>=1,4*V>=Out,4*V2>=Out] * Chain [[62,63,64,65],132,133]: 10*it(62)+2 Such that:aux(7) =< V aux(8) =< V2 it(62) =< aux(7) it(62) =< aux(8) with precondition: [V1=2,V>=1,V2>=1,Out>=2,4*V+1>=Out,4*V2+1>=Out] * Chain [[62,63,64,65],131,133]: 10*it(62)+2 Such that:aux(3) =< V2 aux(9) =< V it(62) =< aux(9) it(62) =< aux(3) with precondition: [V1=2,V>=1,V2>=V,Out>=V+2,4*V+2>=Out] * Chain [[62,63,64,65],130,133]: 10*it(62)+3 Such that:aux(1) =< V aux(10) =< V2 it(62) =< aux(1) it(62) =< aux(10) with precondition: [V1=2,V2>=1,V>=V2,Out>=V2+3,4*V2+3>=Out] * Chain [[62,63,64,65],129,133]: 10*it(62)+3 Such that:aux(3) =< V2 aux(11) =< V it(62) =< aux(11) it(62) =< aux(3) with precondition: [V1=2,V>=1,V2>=V,Out>=V+4,4*V+4>=Out] * Chain [[62,63,64,65],128,133]: 10*it(62)+3 Such that:aux(3) =< V2 aux(12) =< V it(62) =< aux(12) it(62) =< aux(3) with precondition: [V1=2,V>=1,V2>=V,Out>=V+5,4*V+5>=Out] * Chain [[62,63,64,65],127,133]: 10*it(62)+2 Such that:aux(3) =< V2 aux(13) =< V it(62) =< aux(13) it(62) =< aux(3) with precondition: [V1=2,V>=1,V2>=V,Out>=V+1,4*V+1>=Out] * Chain [[62,63,64,65],126,133]: 10*it(62)+2 Such that:aux(3) =< V2 aux(14) =< V it(62) =< aux(14) it(62) =< aux(3) with precondition: [V1=2,V>=1,V2>=V,Out>=V+2,4*V+2>=Out] * Chain [[62,63,64,65],125,133]: 10*it(62)+3 Such that:aux(1) =< V aux(15) =< V2 it(62) =< aux(1) it(62) =< aux(15) with precondition: [V1=2,V2>=1,V>=V2,Out>=V2+3,4*V2+3>=Out] * Chain [[62,63,64,65],124,133]: 10*it(62)+3 Such that:aux(3) =< V2 aux(16) =< V it(62) =< aux(16) it(62) =< aux(3) with precondition: [V1=2,V>=1,V2>=V,Out>=V+4,4*V+4>=Out] * Chain [[62,63,64,65],123,133]: 10*it(62)+3 Such that:aux(3) =< V2 aux(17) =< V it(62) =< aux(17) it(62) =< aux(3) with precondition: [V1=2,V>=1,V2>=V,Out>=V+5,4*V+5>=Out] * Chain [[62,63,64,65],122,133]: 10*it(62)+2 Such that:aux(18) =< V aux(19) =< V2 it(62) =< aux(18) it(62) =< aux(19) with precondition: [V1=2,V>=1,V2>=2,Out>=4,4*V+3>=Out,4*V2>=Out+1] * Chain [[62,63,64,65],121,133]: 10*it(62)+3 Such that:aux(3) =< V2 aux(20) =< V it(62) =< aux(20) it(62) =< aux(3) with precondition: [V1=2,V>=1,V2>=V+1,Out>=V+6,4*V+6>=Out] * Chain [[62,63,64,65],120,133]: 10*it(62)+2 Such that:aux(21) =< V aux(22) =< V2 it(62) =< aux(21) it(62) =< aux(22) with precondition: [V1=2,V>=1,V2>=2,Out>=2,4*V+1>=Out,4*V2>=Out+3] * Chain [[62,63,64,65],119,133]: 10*it(62)+2 Such that:aux(3) =< V2 aux(23) =< V it(62) =< aux(23) it(62) =< aux(3) with precondition: [V1=2,V>=1,V2>=V+1,Out>=V+2,4*V+2>=Out] * Chain [[62,63,64,65],118,133]: 10*it(62)+2 Such that:aux(24) =< V aux(25) =< V2 it(62) =< aux(24) it(62) =< aux(25) with precondition: [V1=2,V>=1,V2>=2,Out>=4,4*V+3>=Out,4*V2>=Out+1] * Chain [[62,63,64,65],117,133]: 10*it(62)+3 Such that:aux(3) =< V2 aux(26) =< V it(62) =< aux(26) it(62) =< aux(3) with precondition: [V1=2,V>=1,V2>=V+1,Out>=V+4,4*V+4>=Out] * Chain [[62,63,64,65],116,133]: 10*it(62)+3 Such that:aux(3) =< V2 aux(27) =< V it(62) =< aux(27) it(62) =< aux(3) with precondition: [V1=2,V>=1,V2>=V+1,Out>=V+5,4*V+5>=Out] * Chain [[62,63,64,65],115,133]: 10*it(62)+3 Such that:aux(3) =< V2 aux(28) =< V it(62) =< aux(28) it(62) =< aux(3) with precondition: [V1=2,V>=1,V2>=V+1,Out>=V+6,4*V+6>=Out] * Chain [[62,63,64,65],114,133]: 10*it(62)+2 Such that:aux(3) =< V2 aux(29) =< V it(62) =< aux(29) it(62) =< aux(3) with precondition: [V1=2,V>=1,V2>=V+1,Out>=V+3,4*V+3>=Out] * Chain [[62,63,64,65],113,133]: 10*it(62)+3 Such that:aux(3) =< V2 aux(30) =< V it(62) =< aux(30) it(62) =< aux(3) with precondition: [V1=2,V>=1,V2>=V+1,Out>=V+6,4*V+6>=Out] * Chain [[62,63,64,65],112,133]: 10*it(62)+2 Such that:aux(3) =< V2 aux(31) =< V it(62) =< aux(31) it(62) =< aux(3) with precondition: [V1=2,V>=1,V2>=V+1,Out>=V+1,4*V+1>=Out] * Chain [[62,63,64,65],111,133]: 10*it(62)+2 Such that:aux(3) =< V2 aux(32) =< V it(62) =< aux(32) it(62) =< aux(3) with precondition: [V1=2,V>=1,V2>=V+1,Out>=V+2,4*V+2>=Out] * Chain [[62,63,64,65],110,133]: 10*it(62)+2 Such that:aux(3) =< V2 aux(33) =< V it(62) =< aux(33) it(62) =< aux(3) with precondition: [V1=2,V>=1,V2>=V+1,Out>=V+3,4*V+3>=Out] * Chain [[62,63,64,65],109,133]: 10*it(62)+3 Such that:aux(3) =< V2 aux(34) =< V it(62) =< aux(34) it(62) =< aux(3) with precondition: [V1=2,V>=1,V2>=V+1,Out>=V+4,4*V+4>=Out] * Chain [[62,63,64,65],108,133]: 10*it(62)+3 Such that:aux(3) =< V2 aux(35) =< V it(62) =< aux(35) it(62) =< aux(3) with precondition: [V1=2,V>=1,V2>=V+1,Out>=V+5,4*V+5>=Out] * Chain [[62,63,64,65],107,133]: 10*it(62)+3 Such that:aux(3) =< V2 aux(36) =< V it(62) =< aux(36) it(62) =< aux(3) with precondition: [V1=2,V>=1,V2>=V+1,Out>=V+6,4*V+6>=Out] * Chain [[62,63,64,65],106,133]: 10*it(62)+2 Such that:aux(1) =< V aux(37) =< V2 it(62) =< aux(1) it(62) =< aux(37) with precondition: [V1=2,V2>=1,V>=V2,Out>=V2+1,4*V2+1>=Out] * Chain [[62,63,64,65],105,133]: 10*it(62)+2 Such that:aux(1) =< V aux(38) =< V2 it(62) =< aux(1) it(62) =< aux(38) with precondition: [V1=2,V2>=1,V>=V2,Out>=V2+2,4*V2+2>=Out] * Chain [[62,63,64,65],104,133]: 10*it(62)+3 Such that:aux(1) =< V aux(39) =< V2 it(62) =< aux(1) it(62) =< aux(39) with precondition: [V1=2,V2>=1,V>=V2,Out>=V2+4,4*V2+4>=Out] * Chain [[62,63,64,65],103,133]: 10*it(62)+3 Such that:aux(1) =< V aux(40) =< V2 it(62) =< aux(1) it(62) =< aux(40) with precondition: [V1=2,V2>=1,V>=V2+1,Out>=V2+5,4*V2+5>=Out] * Chain [[62,63,64,65],102,133]: 10*it(62)+2 Such that:aux(41) =< V aux(42) =< V2 it(62) =< aux(41) it(62) =< aux(42) with precondition: [V1=2,V>=2,V2>=1,Out>=2,4*V>=Out+3,4*V2+1>=Out] * Chain [[62,63,64,65],101,133]: 10*it(62)+2 Such that:aux(1) =< V aux(43) =< V2 it(62) =< aux(1) it(62) =< aux(43) with precondition: [V1=2,V2>=1,V>=V2+1,Out>=V2+2,4*V2+2>=Out] * Chain [[62,63,64,65],100,133]: 10*it(62)+3 Such that:aux(44) =< V aux(45) =< V2 it(62) =< aux(44) it(62) =< aux(45) with precondition: [V1=2,V>=2,V2>=1,Out>=4,4*V>=Out+1,4*V2+3>=Out] * Chain [[62,63,64,65],99,133]: 10*it(62)+3 Such that:aux(1) =< V aux(46) =< V2 it(62) =< aux(1) it(62) =< aux(46) with precondition: [V1=2,V2>=1,V>=V2+1,Out>=V2+4,4*V2+4>=Out] * Chain [[62,63,64,65],98,133]: 10*it(62)+3 Such that:aux(1) =< V aux(47) =< V2 it(62) =< aux(1) it(62) =< aux(47) with precondition: [V1=2,V2>=1,V>=V2+1,Out>=V2+5,4*V2+5>=Out] * Chain [[62,63,64,65],97,133]: 10*it(62)+2 Such that:aux(1) =< V aux(48) =< V2 it(62) =< aux(1) it(62) =< aux(48) with precondition: [V1=2,V2>=1,V>=V2,Out>=V2+1,4*V2+1>=Out] * Chain [[62,63,64,65],96,133]: 10*it(62)+2 Such that:aux(1) =< V aux(49) =< V2 it(62) =< aux(1) it(62) =< aux(49) with precondition: [V1=2,V2>=1,V>=V2,Out>=V2+2,4*V2+2>=Out] * Chain [[62,63,64,65],95,133]: 10*it(62)+3 Such that:aux(1) =< V aux(50) =< V2 it(62) =< aux(1) it(62) =< aux(50) with precondition: [V1=2,V2>=1,V>=V2,Out>=V2+4,4*V2+4>=Out] * Chain [[62,63,64,65],94,133]: 10*it(62)+3 Such that:aux(1) =< V aux(51) =< V2 it(62) =< aux(1) it(62) =< aux(51) with precondition: [V1=2,V2>=1,V>=V2+1,Out>=V2+5,4*V2+5>=Out] * Chain [[62,63,64,65],93,133]: 10*it(62)+2 Such that:aux(1) =< V aux(52) =< V2 it(62) =< aux(1) it(62) =< aux(52) with precondition: [V1=2,V2>=1,V>=V2+1,Out>=V2+1,4*V2+1>=Out] * Chain [[62,63,64,65],92,133]: 10*it(62)+2 Such that:aux(1) =< V aux(53) =< V2 it(62) =< aux(1) it(62) =< aux(53) with precondition: [V1=2,V2>=1,V>=V2+1,Out>=V2+2,4*V2+2>=Out] * Chain [[62,63,64,65],91,133]: 10*it(62)+3 Such that:aux(1) =< V aux(54) =< V2 it(62) =< aux(1) it(62) =< aux(54) with precondition: [V1=2,V2>=1,V>=V2+1,Out>=V2+3,4*V2+3>=Out] * Chain [[62,63,64,65],90,133]: 10*it(62)+3 Such that:aux(1) =< V aux(55) =< V2 it(62) =< aux(1) it(62) =< aux(55) with precondition: [V1=2,V2>=1,V>=V2+1,Out>=V2+4,4*V2+4>=Out] * Chain [[62,63,64,65],89,133]: 10*it(62)+3 Such that:aux(1) =< V aux(56) =< V2 it(62) =< aux(1) it(62) =< aux(56) with precondition: [V1=2,V2>=1,V>=V2+1,Out>=V2+5,4*V2+5>=Out] * Chain [[62,63,64,65],88,133]: 10*it(62)+3 Such that:aux(57) =< V aux(58) =< V2 it(62) =< aux(57) it(62) =< aux(58) with precondition: [V1=2,V>=2,V2>=2,Out>=3,4*V>=Out+2,4*V2>=Out+2] * Chain [[62,63,64,65],87,133]: 10*it(62)+2 Such that:aux(59) =< V aux(60) =< V2 it(62) =< aux(59) it(62) =< aux(60) with precondition: [V1=2,V>=2,V2>=1,Out>=4,4*V>=Out+1,4*V2+3>=Out] * Chain [[62,63,64,65],86,133]: 10*it(62)+3 Such that:aux(61) =< V aux(62) =< V2 it(62) =< aux(61) it(62) =< aux(62) with precondition: [V1=2,V>=2,V2>=2,Out>=5,4*V>=Out,4*V2>=Out] * Chain [[62,63,64,65],85,133]: 10*it(62)+3 Such that:aux(63) =< V aux(64) =< V2 it(62) =< aux(63) it(62) =< aux(64) with precondition: [V1=2,V>=2,V2>=2,Out>=3,4*V>=Out+2,4*V2>=Out+2] * Chain [[62,63,64,65],84,133]: 10*it(62)+3 Such that:aux(65) =< V aux(66) =< V2 it(62) =< aux(65) it(62) =< aux(66) with precondition: [V1=2,V>=2,V2>=2,Out>=5,4*V>=Out,4*V2>=Out] * Chain [[62,63,64,65],83,133]: 10*it(62)+3 Such that:aux(67) =< V aux(68) =< V2 it(62) =< aux(67) it(62) =< aux(68) with precondition: [V1=2,V>=2,V2>=2,Out>=3,4*V>=Out+2,4*V2>=Out+2] * Chain [[62,63,64,65],82,133]: 10*it(62)+3 Such that:aux(69) =< V aux(70) =< V2 it(62) =< aux(69) it(62) =< aux(70) with precondition: [V1=2,V>=2,V2>=2,Out>=5,4*V>=Out,4*V2>=Out] * Chain [[62,63,64,65],81,133]: 10*it(62)+2 Such that:aux(71) =< V aux(72) =< V2 it(62) =< aux(71) it(62) =< aux(72) with precondition: [V1=2,V>=2,V2>=2,Out>=2,4*V>=Out+3,4*V2>=Out+3] * Chain [[62,63,64,65],80,133]: 10*it(62)+3 Such that:aux(73) =< V aux(74) =< V2 it(62) =< aux(73) it(62) =< aux(74) with precondition: [V1=2,V>=2,V2>=2,Out>=3,4*V>=Out+2,4*V2>=Out+2] * Chain [[62,63,64,65],79,133]: 10*it(62)+2 Such that:aux(75) =< V aux(76) =< V2 it(62) =< aux(75) it(62) =< aux(76) with precondition: [V1=2,V>=2,V2>=2,Out>=4,4*V>=Out+1,4*V2>=Out+1] * Chain [[62,63,64,65],78,133]: 10*it(62)+3 Such that:aux(77) =< V aux(78) =< V2 it(62) =< aux(77) it(62) =< aux(78) with precondition: [V1=2,V>=2,V2>=2,Out>=5,4*V>=Out,4*V2>=Out] * Chain [[62,63,64,65],77,133]: 10*it(62)+2 Such that:aux(79) =< V aux(80) =< V2 it(62) =< aux(79) it(62) =< aux(80) with precondition: [V1=2,V>=2,V2>=2,Out>=2,4*V>=Out+3,4*V2>=Out+3] * Chain [[62,63,64,65],77,132,133]: 10*it(62)+4 Such that:aux(81) =< V aux(82) =< V2 it(62) =< aux(81) it(62) =< aux(82) with precondition: [V1=2,V>=2,V2>=2,Out>=3,4*V>=Out+2,4*V2>=Out+2] * Chain [[62,63,64,65],77,131,133]: 10*it(62)+4 Such that:aux(83) =< V aux(84) =< V2 it(62) =< aux(83) it(62) =< aux(84) with precondition: [V1=2,V>=2,V2>=2,Out>=4,4*V>=Out+1,4*V2>=Out+1] * Chain [[62,63,64,65],77,130,133]: 10*it(62)+5 Such that:aux(85) =< V aux(86) =< V2 it(62) =< aux(85) it(62) =< aux(86) with precondition: [V1=2,V>=2,V2>=2,Out>=5,4*V>=Out,4*V2>=Out] * Chain [[62,63,64,65],77,129,133]: 10*it(62)+5 Such that:aux(87) =< V aux(88) =< V2 it(62) =< aux(87) it(62) =< aux(88) with precondition: [V1=2,V>=2,V2>=2,Out>=6,4*V+1>=Out,4*V2+1>=Out] * Chain [[62,63,64,65],77,128,133]: 10*it(62)+5 Such that:aux(89) =< V aux(90) =< V2 it(62) =< aux(89) it(62) =< aux(90) with precondition: [V1=2,V>=2,V2>=2,Out>=7,4*V+2>=Out,4*V2+2>=Out] * Chain [[62,63,64,65],77,127,133]: 10*it(62)+4 Such that:aux(91) =< V aux(92) =< V2 it(62) =< aux(91) it(62) =< aux(92) with precondition: [V1=2,V>=2,V2>=2,Out>=3,4*V>=Out+2,4*V2>=Out+2] * Chain [[62,63,64,65],77,126,133]: 10*it(62)+4 Such that:aux(93) =< V aux(94) =< V2 it(62) =< aux(93) it(62) =< aux(94) with precondition: [V1=2,V>=2,V2>=2,Out>=4,4*V>=Out+1,4*V2>=Out+1] * Chain [[62,63,64,65],77,125,133]: 10*it(62)+5 Such that:aux(95) =< V aux(96) =< V2 it(62) =< aux(95) it(62) =< aux(96) with precondition: [V1=2,V>=2,V2>=2,Out>=5,4*V>=Out,4*V2>=Out] * Chain [[62,63,64,65],77,124,133]: 10*it(62)+5 Such that:aux(97) =< V aux(98) =< V2 it(62) =< aux(97) it(62) =< aux(98) with precondition: [V1=2,V>=2,V2>=2,Out>=6,4*V+1>=Out,4*V2+1>=Out] * Chain [[62,63,64,65],77,123,133]: 10*it(62)+5 Such that:aux(99) =< V aux(100) =< V2 it(62) =< aux(99) it(62) =< aux(100) with precondition: [V1=2,V>=2,V2>=2,Out>=7,4*V+2>=Out,4*V2+2>=Out] * Chain [[62,63,64,65],77,106,133]: 10*it(62)+4 Such that:aux(101) =< V aux(102) =< V2 it(62) =< aux(101) it(62) =< aux(102) with precondition: [V1=2,V>=2,V2>=2,Out>=3,4*V>=Out+2,4*V2>=Out+2] * Chain [[62,63,64,65],77,105,133]: 10*it(62)+4 Such that:aux(103) =< V aux(104) =< V2 it(62) =< aux(103) it(62) =< aux(104) with precondition: [V1=2,V>=2,V2>=2,Out>=4,4*V>=Out+1,4*V2>=Out+1] * Chain [[62,63,64,65],77,104,133]: 10*it(62)+5 Such that:aux(105) =< V aux(106) =< V2 it(62) =< aux(105) it(62) =< aux(106) with precondition: [V1=2,V>=2,V2>=2,Out>=6,4*V+1>=Out,4*V2+1>=Out] * Chain [[62,63,64,65],77,97,133]: 10*it(62)+4 Such that:aux(107) =< V aux(108) =< V2 it(62) =< aux(107) it(62) =< aux(108) with precondition: [V1=2,V>=2,V2>=2,Out>=3,4*V>=Out+2,4*V2>=Out+2] * Chain [[62,63,64,65],77,96,133]: 10*it(62)+4 Such that:aux(109) =< V aux(110) =< V2 it(62) =< aux(109) it(62) =< aux(110) with precondition: [V1=2,V>=2,V2>=2,Out>=4,4*V>=Out+1,4*V2>=Out+1] * Chain [[62,63,64,65],77,95,133]: 10*it(62)+5 Such that:aux(111) =< V aux(112) =< V2 it(62) =< aux(111) it(62) =< aux(112) with precondition: [V1=2,V>=2,V2>=2,Out>=6,4*V+1>=Out,4*V2+1>=Out] * Chain [[62,63,64,65],76,133]: 10*it(62)+3 Such that:aux(113) =< V aux(114) =< V2 it(62) =< aux(113) it(62) =< aux(114) with precondition: [V1=2,V>=2,V2>=2,Out>=3,4*V>=Out+2,4*V2>=Out+2] * Chain [[62,63,64,65],76,132,133]: 10*it(62)+5 Such that:aux(115) =< V aux(116) =< V2 it(62) =< aux(115) it(62) =< aux(116) with precondition: [V1=2,V>=2,V2>=2,Out>=4,4*V>=Out+1,4*V2>=Out+1] * Chain [[62,63,64,65],76,131,133]: 10*it(62)+5 Such that:aux(117) =< V aux(118) =< V2 it(62) =< aux(117) it(62) =< aux(118) with precondition: [V1=2,V>=2,V2>=2,Out>=5,4*V>=Out,4*V2>=Out] * Chain [[62,63,64,65],76,130,133]: 10*it(62)+6 Such that:aux(119) =< V aux(120) =< V2 it(62) =< aux(119) it(62) =< aux(120) with precondition: [V1=2,V>=2,V2>=2,Out>=6,4*V+1>=Out,4*V2+1>=Out] * Chain [[62,63,64,65],76,129,133]: 10*it(62)+6 Such that:aux(121) =< V aux(122) =< V2 it(62) =< aux(121) it(62) =< aux(122) with precondition: [V1=2,V>=2,V2>=2,Out>=7,4*V+2>=Out,4*V2+2>=Out] * Chain [[62,63,64,65],76,128,133]: 10*it(62)+6 Such that:aux(123) =< V aux(124) =< V2 it(62) =< aux(123) it(62) =< aux(124) with precondition: [V1=2,V>=2,V2>=2,Out>=8,4*V+3>=Out,4*V2+3>=Out] * Chain [[62,63,64,65],76,127,133]: 10*it(62)+5 Such that:aux(125) =< V aux(126) =< V2 it(62) =< aux(125) it(62) =< aux(126) with precondition: [V1=2,V>=2,V2>=2,Out>=4,4*V>=Out+1,4*V2>=Out+1] * Chain [[62,63,64,65],76,126,133]: 10*it(62)+5 Such that:aux(127) =< V aux(128) =< V2 it(62) =< aux(127) it(62) =< aux(128) with precondition: [V1=2,V>=2,V2>=2,Out>=5,4*V>=Out,4*V2>=Out] * Chain [[62,63,64,65],76,125,133]: 10*it(62)+6 Such that:aux(129) =< V aux(130) =< V2 it(62) =< aux(129) it(62) =< aux(130) with precondition: [V1=2,V>=2,V2>=2,Out>=6,4*V+1>=Out,4*V2+1>=Out] * Chain [[62,63,64,65],76,124,133]: 10*it(62)+6 Such that:aux(131) =< V aux(132) =< V2 it(62) =< aux(131) it(62) =< aux(132) with precondition: [V1=2,V>=2,V2>=2,Out>=7,4*V+2>=Out,4*V2+2>=Out] * Chain [[62,63,64,65],76,123,133]: 10*it(62)+6 Such that:aux(133) =< V aux(134) =< V2 it(62) =< aux(133) it(62) =< aux(134) with precondition: [V1=2,V>=2,V2>=2,Out>=8,4*V+3>=Out,4*V2+3>=Out] * Chain [[62,63,64,65],76,106,133]: 10*it(62)+5 Such that:aux(135) =< V aux(136) =< V2 it(62) =< aux(135) it(62) =< aux(136) with precondition: [V1=2,V>=2,V2>=2,Out>=4,4*V>=Out+1,4*V2>=Out+1] * Chain [[62,63,64,65],76,105,133]: 10*it(62)+5 Such that:aux(137) =< V aux(138) =< V2 it(62) =< aux(137) it(62) =< aux(138) with precondition: [V1=2,V>=2,V2>=2,Out>=5,4*V>=Out,4*V2>=Out] * Chain [[62,63,64,65],76,104,133]: 10*it(62)+6 Such that:aux(139) =< V aux(140) =< V2 it(62) =< aux(139) it(62) =< aux(140) with precondition: [V1=2,V>=2,V2>=2,Out>=7,4*V+2>=Out,4*V2+2>=Out] * Chain [[62,63,64,65],76,97,133]: 10*it(62)+5 Such that:aux(141) =< V aux(142) =< V2 it(62) =< aux(141) it(62) =< aux(142) with precondition: [V1=2,V>=2,V2>=2,Out>=4,4*V>=Out+1,4*V2>=Out+1] * Chain [[62,63,64,65],76,96,133]: 10*it(62)+5 Such that:aux(143) =< V aux(144) =< V2 it(62) =< aux(143) it(62) =< aux(144) with precondition: [V1=2,V>=2,V2>=2,Out>=5,4*V>=Out,4*V2>=Out] * Chain [[62,63,64,65],76,95,133]: 10*it(62)+6 Such that:aux(145) =< V aux(146) =< V2 it(62) =< aux(145) it(62) =< aux(146) with precondition: [V1=2,V>=2,V2>=2,Out>=7,4*V+2>=Out,4*V2+2>=Out] * Chain [[62,63,64,65],75,133]: 10*it(62)+2 Such that:aux(147) =< V aux(148) =< V2 it(62) =< aux(147) it(62) =< aux(148) with precondition: [V1=2,V>=2,V2>=2,Out>=4,4*V>=Out+1,4*V2>=Out+1] * Chain [[62,63,64,65],75,132,133]: 10*it(62)+4 Such that:aux(149) =< V aux(150) =< V2 it(62) =< aux(149) it(62) =< aux(150) with precondition: [V1=2,V>=2,V2>=2,Out>=5,4*V>=Out,4*V2>=Out] * Chain [[62,63,64,65],75,131,133]: 10*it(62)+4 Such that:aux(151) =< V aux(152) =< V2 it(62) =< aux(151) it(62) =< aux(152) with precondition: [V1=2,V>=2,V2>=2,Out>=6,4*V+1>=Out,4*V2+1>=Out] * Chain [[62,63,64,65],75,130,133]: 10*it(62)+5 Such that:aux(153) =< V aux(154) =< V2 it(62) =< aux(153) it(62) =< aux(154) with precondition: [V1=2,V>=2,V2>=2,Out>=7,4*V+2>=Out,4*V2+2>=Out] * Chain [[62,63,64,65],75,129,133]: 10*it(62)+5 Such that:aux(155) =< V aux(156) =< V2 it(62) =< aux(155) it(62) =< aux(156) with precondition: [V1=2,V>=2,V2>=2,Out>=8,4*V+3>=Out,4*V2+3>=Out] * Chain [[62,63,64,65],75,128,133]: 10*it(62)+5 Such that:aux(157) =< V aux(158) =< V2 it(62) =< aux(157) it(62) =< aux(158) with precondition: [V1=2,V>=2,V2>=2,Out>=9,4*V+4>=Out,4*V2+4>=Out] * Chain [[62,63,64,65],75,127,133]: 10*it(62)+4 Such that:aux(159) =< V aux(160) =< V2 it(62) =< aux(159) it(62) =< aux(160) with precondition: [V1=2,V>=2,V2>=2,Out>=5,4*V>=Out,4*V2>=Out] * Chain [[62,63,64,65],75,126,133]: 10*it(62)+4 Such that:aux(161) =< V aux(162) =< V2 it(62) =< aux(161) it(62) =< aux(162) with precondition: [V1=2,V>=2,V2>=2,Out>=6,4*V+1>=Out,4*V2+1>=Out] * Chain [[62,63,64,65],75,125,133]: 10*it(62)+5 Such that:aux(163) =< V aux(164) =< V2 it(62) =< aux(163) it(62) =< aux(164) with precondition: [V1=2,V>=2,V2>=2,Out>=7,4*V+2>=Out,4*V2+2>=Out] * Chain [[62,63,64,65],75,124,133]: 10*it(62)+5 Such that:aux(165) =< V aux(166) =< V2 it(62) =< aux(165) it(62) =< aux(166) with precondition: [V1=2,V>=2,V2>=2,Out>=8,4*V+3>=Out,4*V2+3>=Out] * Chain [[62,63,64,65],75,123,133]: 10*it(62)+5 Such that:aux(167) =< V aux(168) =< V2 it(62) =< aux(167) it(62) =< aux(168) with precondition: [V1=2,V>=2,V2>=2,Out>=9,4*V+4>=Out,4*V2+4>=Out] * Chain [[62,63,64,65],75,106,133]: 10*it(62)+4 Such that:aux(169) =< V aux(170) =< V2 it(62) =< aux(169) it(62) =< aux(170) with precondition: [V1=2,V>=2,V2>=2,Out>=5,4*V>=Out,4*V2>=Out] * Chain [[62,63,64,65],75,105,133]: 10*it(62)+4 Such that:aux(171) =< V aux(172) =< V2 it(62) =< aux(171) it(62) =< aux(172) with precondition: [V1=2,V>=2,V2>=2,Out>=6,4*V+1>=Out,4*V2+1>=Out] * Chain [[62,63,64,65],75,104,133]: 10*it(62)+5 Such that:aux(173) =< V aux(174) =< V2 it(62) =< aux(173) it(62) =< aux(174) with precondition: [V1=2,V>=2,V2>=2,Out>=8,4*V+3>=Out,4*V2+3>=Out] * Chain [[62,63,64,65],75,97,133]: 10*it(62)+4 Such that:aux(175) =< V aux(176) =< V2 it(62) =< aux(175) it(62) =< aux(176) with precondition: [V1=2,V>=2,V2>=2,Out>=5,4*V>=Out,4*V2>=Out] * Chain [[62,63,64,65],75,96,133]: 10*it(62)+4 Such that:aux(177) =< V aux(178) =< V2 it(62) =< aux(177) it(62) =< aux(178) with precondition: [V1=2,V>=2,V2>=2,Out>=6,4*V+1>=Out,4*V2+1>=Out] * Chain [[62,63,64,65],75,95,133]: 10*it(62)+5 Such that:aux(179) =< V aux(180) =< V2 it(62) =< aux(179) it(62) =< aux(180) with precondition: [V1=2,V>=2,V2>=2,Out>=8,4*V+3>=Out,4*V2+3>=Out] * Chain [[62,63,64,65],74,133]: 10*it(62)+3 Such that:aux(181) =< V aux(182) =< V2 it(62) =< aux(181) it(62) =< aux(182) with precondition: [V1=2,V>=2,V2>=2,Out>=5,4*V>=Out,4*V2>=Out] * Chain [[62,63,64,65],74,132,133]: 10*it(62)+5 Such that:aux(183) =< V aux(184) =< V2 it(62) =< aux(183) it(62) =< aux(184) with precondition: [V1=2,V>=2,V2>=2,Out>=6,4*V+1>=Out,4*V2+1>=Out] * Chain [[62,63,64,65],74,131,133]: 10*it(62)+5 Such that:aux(185) =< V aux(186) =< V2 it(62) =< aux(185) it(62) =< aux(186) with precondition: [V1=2,V>=2,V2>=2,Out>=7,4*V+2>=Out,4*V2+2>=Out] * Chain [[62,63,64,65],74,130,133]: 10*it(62)+6 Such that:aux(187) =< V aux(188) =< V2 it(62) =< aux(187) it(62) =< aux(188) with precondition: [V1=2,V>=2,V2>=2,Out>=8,4*V+3>=Out,4*V2+3>=Out] * Chain [[62,63,64,65],74,129,133]: 10*it(62)+6 Such that:aux(189) =< V aux(190) =< V2 it(62) =< aux(189) it(62) =< aux(190) with precondition: [V1=2,V>=2,V2>=2,Out>=9,4*V+4>=Out,4*V2+4>=Out] * Chain [[62,63,64,65],74,128,133]: 10*it(62)+6 Such that:aux(191) =< V aux(192) =< V2 it(62) =< aux(191) it(62) =< aux(192) with precondition: [V1=2,V>=2,V2>=2,Out>=10,4*V+5>=Out,4*V2+5>=Out] * Chain [[62,63,64,65],74,127,133]: 10*it(62)+5 Such that:aux(193) =< V aux(194) =< V2 it(62) =< aux(193) it(62) =< aux(194) with precondition: [V1=2,V>=2,V2>=2,Out>=6,4*V+1>=Out,4*V2+1>=Out] * Chain [[62,63,64,65],74,126,133]: 10*it(62)+5 Such that:aux(195) =< V aux(196) =< V2 it(62) =< aux(195) it(62) =< aux(196) with precondition: [V1=2,V>=2,V2>=2,Out>=7,4*V+2>=Out,4*V2+2>=Out] * Chain [[62,63,64,65],74,125,133]: 10*it(62)+6 Such that:aux(197) =< V aux(198) =< V2 it(62) =< aux(197) it(62) =< aux(198) with precondition: [V1=2,V>=2,V2>=2,Out>=8,4*V+3>=Out,4*V2+3>=Out] * Chain [[62,63,64,65],74,124,133]: 10*it(62)+6 Such that:aux(199) =< V aux(200) =< V2 it(62) =< aux(199) it(62) =< aux(200) with precondition: [V1=2,V>=2,V2>=2,Out>=9,4*V+4>=Out,4*V2+4>=Out] * Chain [[62,63,64,65],74,123,133]: 10*it(62)+6 Such that:aux(201) =< V aux(202) =< V2 it(62) =< aux(201) it(62) =< aux(202) with precondition: [V1=2,V>=2,V2>=2,Out>=10,4*V+5>=Out,4*V2+5>=Out] * Chain [[62,63,64,65],74,106,133]: 10*it(62)+5 Such that:aux(203) =< V aux(204) =< V2 it(62) =< aux(203) it(62) =< aux(204) with precondition: [V1=2,V>=2,V2>=2,Out>=6,4*V+1>=Out,4*V2+1>=Out] * Chain [[62,63,64,65],74,105,133]: 10*it(62)+5 Such that:aux(205) =< V aux(206) =< V2 it(62) =< aux(205) it(62) =< aux(206) with precondition: [V1=2,V>=2,V2>=2,Out>=7,4*V+2>=Out,4*V2+2>=Out] * Chain [[62,63,64,65],74,104,133]: 10*it(62)+6 Such that:aux(207) =< V aux(208) =< V2 it(62) =< aux(207) it(62) =< aux(208) with precondition: [V1=2,V>=2,V2>=2,Out>=9,4*V+4>=Out,4*V2+4>=Out] * Chain [[62,63,64,65],74,97,133]: 10*it(62)+5 Such that:aux(209) =< V aux(210) =< V2 it(62) =< aux(209) it(62) =< aux(210) with precondition: [V1=2,V>=2,V2>=2,Out>=6,4*V+1>=Out,4*V2+1>=Out] * Chain [[62,63,64,65],74,96,133]: 10*it(62)+5 Such that:aux(211) =< V aux(212) =< V2 it(62) =< aux(211) it(62) =< aux(212) with precondition: [V1=2,V>=2,V2>=2,Out>=7,4*V+2>=Out,4*V2+2>=Out] * Chain [[62,63,64,65],74,95,133]: 10*it(62)+6 Such that:aux(213) =< V aux(214) =< V2 it(62) =< aux(213) it(62) =< aux(214) with precondition: [V1=2,V>=2,V2>=2,Out>=9,4*V+4>=Out,4*V2+4>=Out] * Chain [[62,63,64,65],73,133]: 10*it(62)+2 Such that:aux(215) =< V aux(216) =< V2 it(62) =< aux(215) it(62) =< aux(216) with precondition: [V1=2,V>=2,V2>=2,Out>=2,4*V>=Out+3,4*V2>=Out+3] * Chain [[62,63,64,65],73,132,133]: 10*it(62)+4 Such that:aux(217) =< V aux(218) =< V2 it(62) =< aux(217) it(62) =< aux(218) with precondition: [V1=2,V>=2,V2>=2,Out>=3,4*V>=Out+2,4*V2>=Out+2] * Chain [[62,63,64,65],73,131,133]: 10*it(62)+4 Such that:aux(219) =< V aux(220) =< V2 it(62) =< aux(219) it(62) =< aux(220) with precondition: [V1=2,V>=2,V2>=2,Out>=4,4*V>=Out+1,4*V2>=Out+1] * Chain [[62,63,64,65],73,130,133]: 10*it(62)+5 Such that:aux(1) =< V aux(221) =< V2 it(62) =< aux(1) it(62) =< aux(221) with precondition: [V1=2,V2>=2,V>=V2,Out>=V2+3,4*V2>=Out] * Chain [[62,63,64,65],73,129,133]: 10*it(62)+5 Such that:aux(222) =< V aux(223) =< V2 it(62) =< aux(222) it(62) =< aux(223) with precondition: [V1=2,V>=2,V2>=2,Out>=6,4*V+1>=Out,4*V2+1>=Out] * Chain [[62,63,64,65],73,128,133]: 10*it(62)+5 Such that:aux(224) =< V aux(225) =< V2 it(62) =< aux(224) it(62) =< aux(225) with precondition: [V1=2,V>=2,V2>=2,Out>=7,4*V+2>=Out,4*V2+2>=Out] * Chain [[62,63,64,65],73,127,133]: 10*it(62)+4 Such that:aux(226) =< V aux(227) =< V2 it(62) =< aux(226) it(62) =< aux(227) with precondition: [V1=2,V>=2,V2>=2,Out>=3,4*V>=Out+2,4*V2>=Out+2] * Chain [[62,63,64,65],73,126,133]: 10*it(62)+4 Such that:aux(228) =< V aux(229) =< V2 it(62) =< aux(228) it(62) =< aux(229) with precondition: [V1=2,V>=2,V2>=2,Out>=4,4*V>=Out+1,4*V2>=Out+1] * Chain [[62,63,64,65],73,125,133]: 10*it(62)+5 Such that:aux(1) =< V aux(230) =< V2 it(62) =< aux(1) it(62) =< aux(230) with precondition: [V1=2,V2>=2,V>=V2,Out>=V2+3,4*V2>=Out] * Chain [[62,63,64,65],73,124,133]: 10*it(62)+5 Such that:aux(231) =< V aux(232) =< V2 it(62) =< aux(231) it(62) =< aux(232) with precondition: [V1=2,V>=2,V2>=2,Out>=6,4*V+1>=Out,4*V2+1>=Out] * Chain [[62,63,64,65],73,123,133]: 10*it(62)+5 Such that:aux(233) =< V aux(234) =< V2 it(62) =< aux(233) it(62) =< aux(234) with precondition: [V1=2,V>=2,V2>=2,Out>=7,4*V+2>=Out,4*V2+2>=Out] * Chain [[62,63,64,65],73,122,133]: 10*it(62)+4 Such that:aux(235) =< V aux(236) =< V2 it(62) =< aux(235) it(62) =< aux(236) with precondition: [V1=2,V>=2,V2>=3,Out>=5,4*V>=Out,4*V2>=Out+4] * Chain [[62,63,64,65],73,121,133]: 10*it(62)+5 Such that:aux(237) =< V aux(238) =< V2 it(62) =< aux(237) it(62) =< aux(238) with precondition: [V1=2,V>=2,V2>=3,Out>=8,4*V+3>=Out,4*V2>=Out+1] * Chain [[62,63,64,65],73,120,133]: 10*it(62)+4 Such that:aux(239) =< V aux(240) =< V2 it(62) =< aux(239) it(62) =< aux(240) with precondition: [V1=2,V>=2,V2>=3,Out>=3,4*V>=Out+2,4*V2>=Out+6] * Chain [[62,63,64,65],73,119,133]: 10*it(62)+4 Such that:aux(241) =< V aux(242) =< V2 it(62) =< aux(241) it(62) =< aux(242) with precondition: [V1=2,V>=2,V2>=3,Out>=4,4*V>=Out+1,4*V2>=Out+5] * Chain [[62,63,64,65],73,118,133]: 10*it(62)+4 Such that:aux(243) =< V aux(244) =< V2 it(62) =< aux(243) it(62) =< aux(244) with precondition: [V1=2,V>=2,V2>=3,Out>=5,4*V>=Out,4*V2>=Out+4] * Chain [[62,63,64,65],73,117,133]: 10*it(62)+5 Such that:aux(245) =< V aux(246) =< V2 it(62) =< aux(245) it(62) =< aux(246) with precondition: [V1=2,V>=2,V2>=3,Out>=6,4*V+1>=Out,4*V2>=Out+3] * Chain [[62,63,64,65],73,116,133]: 10*it(62)+5 Such that:aux(247) =< V aux(248) =< V2 it(62) =< aux(247) it(62) =< aux(248) with precondition: [V1=2,V>=2,V2>=3,Out>=7,4*V+2>=Out,4*V2>=Out+2] * Chain [[62,63,64,65],73,115,133]: 10*it(62)+5 Such that:aux(249) =< V aux(250) =< V2 it(62) =< aux(249) it(62) =< aux(250) with precondition: [V1=2,V>=2,V2>=3,Out>=8,4*V+3>=Out,4*V2>=Out+1] * Chain [[62,63,64,65],73,114,133]: 10*it(62)+4 Such that:aux(251) =< V aux(252) =< V2 it(62) =< aux(251) it(62) =< aux(252) with precondition: [V1=2,V>=2,V2>=3,Out>=5,4*V>=Out,4*V2>=Out+4] * Chain [[62,63,64,65],73,113,133]: 10*it(62)+5 Such that:aux(253) =< V aux(254) =< V2 it(62) =< aux(253) it(62) =< aux(254) with precondition: [V1=2,V>=2,V2>=3,Out>=8,4*V+3>=Out,4*V2>=Out+1] * Chain [[62,63,64,65],73,112,133]: 10*it(62)+4 Such that:aux(255) =< V aux(256) =< V2 it(62) =< aux(255) it(62) =< aux(256) with precondition: [V1=2,V>=2,V2>=3,Out>=3,4*V>=Out+2,4*V2>=Out+6] * Chain [[62,63,64,65],73,111,133]: 10*it(62)+4 Such that:aux(257) =< V aux(258) =< V2 it(62) =< aux(257) it(62) =< aux(258) with precondition: [V1=2,V>=2,V2>=3,Out>=4,4*V>=Out+1,4*V2>=Out+5] * Chain [[62,63,64,65],73,110,133]: 10*it(62)+4 Such that:aux(259) =< V aux(260) =< V2 it(62) =< aux(259) it(62) =< aux(260) with precondition: [V1=2,V>=2,V2>=3,Out>=5,4*V>=Out,4*V2>=Out+4] * Chain [[62,63,64,65],73,109,133]: 10*it(62)+5 Such that:aux(261) =< V aux(262) =< V2 it(62) =< aux(261) it(62) =< aux(262) with precondition: [V1=2,V>=2,V2>=3,Out>=6,4*V+1>=Out,4*V2>=Out+3] * Chain [[62,63,64,65],73,108,133]: 10*it(62)+5 Such that:aux(263) =< V aux(264) =< V2 it(62) =< aux(263) it(62) =< aux(264) with precondition: [V1=2,V>=2,V2>=3,Out>=7,4*V+2>=Out,4*V2>=Out+2] * Chain [[62,63,64,65],73,107,133]: 10*it(62)+5 Such that:aux(265) =< V aux(266) =< V2 it(62) =< aux(265) it(62) =< aux(266) with precondition: [V1=2,V>=2,V2>=3,Out>=8,4*V+3>=Out,4*V2>=Out+1] * Chain [[62,63,64,65],73,106,133]: 10*it(62)+4 Such that:aux(1) =< V aux(267) =< V2 it(62) =< aux(1) it(62) =< aux(267) with precondition: [V1=2,V2>=2,V>=V2,Out>=V2+1,4*V2>=Out+2] * Chain [[62,63,64,65],73,105,133]: 10*it(62)+4 Such that:aux(1) =< V aux(268) =< V2 it(62) =< aux(1) it(62) =< aux(268) with precondition: [V1=2,V2>=2,V>=V2,Out>=V2+2,4*V2>=Out+1] * Chain [[62,63,64,65],73,104,133]: 10*it(62)+5 Such that:aux(1) =< V aux(269) =< V2 it(62) =< aux(1) it(62) =< aux(269) with precondition: [V1=2,V2>=2,V>=V2,Out>=V2+4,4*V2+1>=Out] * Chain [[62,63,64,65],73,97,133]: 10*it(62)+4 Such that:aux(1) =< V aux(270) =< V2 it(62) =< aux(1) it(62) =< aux(270) with precondition: [V1=2,V2>=2,V>=V2,Out>=V2+1,4*V2>=Out+2] * Chain [[62,63,64,65],73,96,133]: 10*it(62)+4 Such that:aux(1) =< V aux(271) =< V2 it(62) =< aux(1) it(62) =< aux(271) with precondition: [V1=2,V2>=2,V>=V2,Out>=V2+2,4*V2>=Out+1] * Chain [[62,63,64,65],73,95,133]: 10*it(62)+5 Such that:aux(1) =< V aux(272) =< V2 it(62) =< aux(1) it(62) =< aux(272) with precondition: [V1=2,V2>=2,V>=V2,Out>=V2+4,4*V2+1>=Out] * Chain [[62,63,64,65],72,133]: 10*it(62)+3 Such that:aux(273) =< V aux(274) =< V2 it(62) =< aux(273) it(62) =< aux(274) with precondition: [V1=2,V>=2,V2>=2,Out>=3,4*V>=Out+2,4*V2>=Out+2] * Chain [[62,63,64,65],72,132,133]: 10*it(62)+5 Such that:aux(275) =< V aux(276) =< V2 it(62) =< aux(275) it(62) =< aux(276) with precondition: [V1=2,V>=2,V2>=2,Out>=4,4*V>=Out+1,4*V2>=Out+1] * Chain [[62,63,64,65],72,131,133]: 10*it(62)+5 Such that:aux(277) =< V aux(278) =< V2 it(62) =< aux(277) it(62) =< aux(278) with precondition: [V1=2,V>=2,V2>=2,Out>=5,4*V>=Out,4*V2>=Out] * Chain [[62,63,64,65],72,130,133]: 10*it(62)+6 Such that:aux(1) =< V aux(279) =< V2 it(62) =< aux(1) it(62) =< aux(279) with precondition: [V1=2,V2>=2,V>=V2,Out>=V2+4,4*V2+1>=Out] * Chain [[62,63,64,65],72,129,133]: 10*it(62)+6 Such that:aux(280) =< V aux(281) =< V2 it(62) =< aux(280) it(62) =< aux(281) with precondition: [V1=2,V>=2,V2>=2,Out>=7,4*V+2>=Out,4*V2+2>=Out] * Chain [[62,63,64,65],72,128,133]: 10*it(62)+6 Such that:aux(282) =< V aux(283) =< V2 it(62) =< aux(282) it(62) =< aux(283) with precondition: [V1=2,V>=2,V2>=2,Out>=8,4*V+3>=Out,4*V2+3>=Out] * Chain [[62,63,64,65],72,127,133]: 10*it(62)+5 Such that:aux(284) =< V aux(285) =< V2 it(62) =< aux(284) it(62) =< aux(285) with precondition: [V1=2,V>=2,V2>=2,Out>=4,4*V>=Out+1,4*V2>=Out+1] * Chain [[62,63,64,65],72,126,133]: 10*it(62)+5 Such that:aux(286) =< V aux(287) =< V2 it(62) =< aux(286) it(62) =< aux(287) with precondition: [V1=2,V>=2,V2>=2,Out>=5,4*V>=Out,4*V2>=Out] * Chain [[62,63,64,65],72,125,133]: 10*it(62)+6 Such that:aux(1) =< V aux(288) =< V2 it(62) =< aux(1) it(62) =< aux(288) with precondition: [V1=2,V2>=2,V>=V2,Out>=V2+4,4*V2+1>=Out] * Chain [[62,63,64,65],72,124,133]: 10*it(62)+6 Such that:aux(289) =< V aux(290) =< V2 it(62) =< aux(289) it(62) =< aux(290) with precondition: [V1=2,V>=2,V2>=2,Out>=7,4*V+2>=Out,4*V2+2>=Out] * Chain [[62,63,64,65],72,123,133]: 10*it(62)+6 Such that:aux(291) =< V aux(292) =< V2 it(62) =< aux(291) it(62) =< aux(292) with precondition: [V1=2,V>=2,V2>=2,Out>=8,4*V+3>=Out,4*V2+3>=Out] * Chain [[62,63,64,65],72,122,133]: 10*it(62)+5 Such that:aux(293) =< V aux(294) =< V2 it(62) =< aux(293) it(62) =< aux(294) with precondition: [V1=2,V>=2,V2>=3,Out>=6,4*V+1>=Out,4*V2>=Out+3] * Chain [[62,63,64,65],72,121,133]: 10*it(62)+6 Such that:aux(295) =< V aux(296) =< V2 it(62) =< aux(295) it(62) =< aux(296) with precondition: [V1=2,V>=2,V2>=3,Out>=9,4*V+4>=Out,4*V2>=Out] * Chain [[62,63,64,65],72,120,133]: 10*it(62)+5 Such that:aux(297) =< V aux(298) =< V2 it(62) =< aux(297) it(62) =< aux(298) with precondition: [V1=2,V>=2,V2>=3,Out>=4,4*V>=Out+1,4*V2>=Out+5] * Chain [[62,63,64,65],72,119,133]: 10*it(62)+5 Such that:aux(299) =< V aux(300) =< V2 it(62) =< aux(299) it(62) =< aux(300) with precondition: [V1=2,V>=2,V2>=3,Out>=5,4*V>=Out,4*V2>=Out+4] * Chain [[62,63,64,65],72,118,133]: 10*it(62)+5 Such that:aux(301) =< V aux(302) =< V2 it(62) =< aux(301) it(62) =< aux(302) with precondition: [V1=2,V>=2,V2>=3,Out>=6,4*V+1>=Out,4*V2>=Out+3] * Chain [[62,63,64,65],72,117,133]: 10*it(62)+6 Such that:aux(303) =< V aux(304) =< V2 it(62) =< aux(303) it(62) =< aux(304) with precondition: [V1=2,V>=2,V2>=3,Out>=7,4*V+2>=Out,4*V2>=Out+2] * Chain [[62,63,64,65],72,116,133]: 10*it(62)+6 Such that:aux(305) =< V aux(306) =< V2 it(62) =< aux(305) it(62) =< aux(306) with precondition: [V1=2,V>=2,V2>=3,Out>=8,4*V+3>=Out,4*V2>=Out+1] * Chain [[62,63,64,65],72,115,133]: 10*it(62)+6 Such that:aux(307) =< V aux(308) =< V2 it(62) =< aux(307) it(62) =< aux(308) with precondition: [V1=2,V>=2,V2>=3,Out>=9,4*V+4>=Out,4*V2>=Out] * Chain [[62,63,64,65],72,114,133]: 10*it(62)+5 Such that:aux(309) =< V aux(310) =< V2 it(62) =< aux(309) it(62) =< aux(310) with precondition: [V1=2,V>=2,V2>=3,Out>=6,4*V+1>=Out,4*V2>=Out+3] * Chain [[62,63,64,65],72,113,133]: 10*it(62)+6 Such that:aux(311) =< V aux(312) =< V2 it(62) =< aux(311) it(62) =< aux(312) with precondition: [V1=2,V>=2,V2>=3,Out>=9,4*V+4>=Out,4*V2>=Out] * Chain [[62,63,64,65],72,112,133]: 10*it(62)+5 Such that:aux(313) =< V aux(314) =< V2 it(62) =< aux(313) it(62) =< aux(314) with precondition: [V1=2,V>=2,V2>=3,Out>=4,4*V>=Out+1,4*V2>=Out+5] * Chain [[62,63,64,65],72,111,133]: 10*it(62)+5 Such that:aux(315) =< V aux(316) =< V2 it(62) =< aux(315) it(62) =< aux(316) with precondition: [V1=2,V>=2,V2>=3,Out>=5,4*V>=Out,4*V2>=Out+4] * Chain [[62,63,64,65],72,110,133]: 10*it(62)+5 Such that:aux(317) =< V aux(318) =< V2 it(62) =< aux(317) it(62) =< aux(318) with precondition: [V1=2,V>=2,V2>=3,Out>=6,4*V+1>=Out,4*V2>=Out+3] * Chain [[62,63,64,65],72,109,133]: 10*it(62)+6 Such that:aux(319) =< V aux(320) =< V2 it(62) =< aux(319) it(62) =< aux(320) with precondition: [V1=2,V>=2,V2>=3,Out>=7,4*V+2>=Out,4*V2>=Out+2] * Chain [[62,63,64,65],72,108,133]: 10*it(62)+6 Such that:aux(321) =< V aux(322) =< V2 it(62) =< aux(321) it(62) =< aux(322) with precondition: [V1=2,V>=2,V2>=3,Out>=8,4*V+3>=Out,4*V2>=Out+1] * Chain [[62,63,64,65],72,107,133]: 10*it(62)+6 Such that:aux(323) =< V aux(324) =< V2 it(62) =< aux(323) it(62) =< aux(324) with precondition: [V1=2,V>=2,V2>=3,Out>=9,4*V+4>=Out,4*V2>=Out] * Chain [[62,63,64,65],72,106,133]: 10*it(62)+5 Such that:aux(1) =< V aux(325) =< V2 it(62) =< aux(1) it(62) =< aux(325) with precondition: [V1=2,V2>=2,V>=V2,Out>=V2+2,4*V2>=Out+1] * Chain [[62,63,64,65],72,105,133]: 10*it(62)+5 Such that:aux(1) =< V aux(326) =< V2 it(62) =< aux(1) it(62) =< aux(326) with precondition: [V1=2,V2>=2,V>=V2,Out>=V2+3,4*V2>=Out] * Chain [[62,63,64,65],72,104,133]: 10*it(62)+6 Such that:aux(1) =< V aux(327) =< V2 it(62) =< aux(1) it(62) =< aux(327) with precondition: [V1=2,V2>=2,V>=V2,Out>=V2+5,4*V2+2>=Out] * Chain [[62,63,64,65],72,97,133]: 10*it(62)+5 Such that:aux(1) =< V aux(328) =< V2 it(62) =< aux(1) it(62) =< aux(328) with precondition: [V1=2,V2>=2,V>=V2,Out>=V2+2,4*V2>=Out+1] * Chain [[62,63,64,65],72,96,133]: 10*it(62)+5 Such that:aux(1) =< V aux(329) =< V2 it(62) =< aux(1) it(62) =< aux(329) with precondition: [V1=2,V2>=2,V>=V2,Out>=V2+3,4*V2>=Out] * Chain [[62,63,64,65],72,95,133]: 10*it(62)+6 Such that:aux(1) =< V aux(330) =< V2 it(62) =< aux(1) it(62) =< aux(330) with precondition: [V1=2,V2>=2,V>=V2,Out>=V2+5,4*V2+2>=Out] * Chain [[62,63,64,65],71,133]: 10*it(62)+2 Such that:aux(331) =< V aux(332) =< V2 it(62) =< aux(331) it(62) =< aux(332) with precondition: [V1=2,V>=2,V2>=2,Out>=4,4*V>=Out+1,4*V2>=Out+1] * Chain [[62,63,64,65],71,132,133]: 10*it(62)+4 Such that:aux(333) =< V aux(334) =< V2 it(62) =< aux(333) it(62) =< aux(334) with precondition: [V1=2,V>=2,V2>=2,Out>=5,4*V>=Out,4*V2>=Out] * Chain [[62,63,64,65],71,131,133]: 10*it(62)+4 Such that:aux(335) =< V aux(336) =< V2 it(62) =< aux(335) it(62) =< aux(336) with precondition: [V1=2,V>=2,V2>=2,Out>=6,4*V+1>=Out,4*V2+1>=Out] * Chain [[62,63,64,65],71,130,133]: 10*it(62)+5 Such that:aux(1) =< V aux(337) =< V2 it(62) =< aux(1) it(62) =< aux(337) with precondition: [V1=2,V2>=2,V>=V2,Out>=V2+5,4*V2+2>=Out] * Chain [[62,63,64,65],71,129,133]: 10*it(62)+5 Such that:aux(338) =< V aux(339) =< V2 it(62) =< aux(338) it(62) =< aux(339) with precondition: [V1=2,V>=2,V2>=2,Out>=8,4*V+3>=Out,4*V2+3>=Out] * Chain [[62,63,64,65],71,128,133]: 10*it(62)+5 Such that:aux(340) =< V aux(341) =< V2 it(62) =< aux(340) it(62) =< aux(341) with precondition: [V1=2,V>=2,V2>=2,Out>=9,4*V+4>=Out,4*V2+4>=Out] * Chain [[62,63,64,65],71,127,133]: 10*it(62)+4 Such that:aux(342) =< V aux(343) =< V2 it(62) =< aux(342) it(62) =< aux(343) with precondition: [V1=2,V>=2,V2>=2,Out>=5,4*V>=Out,4*V2>=Out] * Chain [[62,63,64,65],71,126,133]: 10*it(62)+4 Such that:aux(344) =< V aux(345) =< V2 it(62) =< aux(344) it(62) =< aux(345) with precondition: [V1=2,V>=2,V2>=2,Out>=6,4*V+1>=Out,4*V2+1>=Out] * Chain [[62,63,64,65],71,125,133]: 10*it(62)+5 Such that:aux(1) =< V aux(346) =< V2 it(62) =< aux(1) it(62) =< aux(346) with precondition: [V1=2,V2>=2,V>=V2,Out>=V2+5,4*V2+2>=Out] * Chain [[62,63,64,65],71,124,133]: 10*it(62)+5 Such that:aux(347) =< V aux(348) =< V2 it(62) =< aux(347) it(62) =< aux(348) with precondition: [V1=2,V>=2,V2>=2,Out>=8,4*V+3>=Out,4*V2+3>=Out] * Chain [[62,63,64,65],71,123,133]: 10*it(62)+5 Such that:aux(349) =< V aux(350) =< V2 it(62) =< aux(349) it(62) =< aux(350) with precondition: [V1=2,V>=2,V2>=2,Out>=9,4*V+4>=Out,4*V2+4>=Out] * Chain [[62,63,64,65],71,122,133]: 10*it(62)+4 Such that:aux(351) =< V aux(352) =< V2 it(62) =< aux(351) it(62) =< aux(352) with precondition: [V1=2,V>=2,V2>=3,Out>=7,4*V+2>=Out,4*V2>=Out+2] * Chain [[62,63,64,65],71,121,133]: 10*it(62)+5 Such that:aux(353) =< V aux(354) =< V2 it(62) =< aux(353) it(62) =< aux(354) with precondition: [V1=2,V>=2,V2>=3,Out>=10,4*V+5>=Out,4*V2+1>=Out] * Chain [[62,63,64,65],71,120,133]: 10*it(62)+4 Such that:aux(355) =< V aux(356) =< V2 it(62) =< aux(355) it(62) =< aux(356) with precondition: [V1=2,V>=2,V2>=3,Out>=5,4*V>=Out,4*V2>=Out+4] * Chain [[62,63,64,65],71,119,133]: 10*it(62)+4 Such that:aux(357) =< V aux(358) =< V2 it(62) =< aux(357) it(62) =< aux(358) with precondition: [V1=2,V>=2,V2>=3,Out>=6,4*V+1>=Out,4*V2>=Out+3] * Chain [[62,63,64,65],71,118,133]: 10*it(62)+4 Such that:aux(359) =< V aux(360) =< V2 it(62) =< aux(359) it(62) =< aux(360) with precondition: [V1=2,V>=2,V2>=3,Out>=7,4*V+2>=Out,4*V2>=Out+2] * Chain [[62,63,64,65],71,117,133]: 10*it(62)+5 Such that:aux(361) =< V aux(362) =< V2 it(62) =< aux(361) it(62) =< aux(362) with precondition: [V1=2,V>=2,V2>=3,Out>=8,4*V+3>=Out,4*V2>=Out+1] * Chain [[62,63,64,65],71,116,133]: 10*it(62)+5 Such that:aux(363) =< V aux(364) =< V2 it(62) =< aux(363) it(62) =< aux(364) with precondition: [V1=2,V>=2,V2>=3,Out>=9,4*V+4>=Out,4*V2>=Out] * Chain [[62,63,64,65],71,115,133]: 10*it(62)+5 Such that:aux(365) =< V aux(366) =< V2 it(62) =< aux(365) it(62) =< aux(366) with precondition: [V1=2,V>=2,V2>=3,Out>=10,4*V+5>=Out,4*V2+1>=Out] * Chain [[62,63,64,65],71,114,133]: 10*it(62)+4 Such that:aux(367) =< V aux(368) =< V2 it(62) =< aux(367) it(62) =< aux(368) with precondition: [V1=2,V>=2,V2>=3,Out>=7,4*V+2>=Out,4*V2>=Out+2] * Chain [[62,63,64,65],71,113,133]: 10*it(62)+5 Such that:aux(369) =< V aux(370) =< V2 it(62) =< aux(369) it(62) =< aux(370) with precondition: [V1=2,V>=2,V2>=3,Out>=10,4*V+5>=Out,4*V2+1>=Out] * Chain [[62,63,64,65],71,112,133]: 10*it(62)+4 Such that:aux(371) =< V aux(372) =< V2 it(62) =< aux(371) it(62) =< aux(372) with precondition: [V1=2,V>=2,V2>=3,Out>=5,4*V>=Out,4*V2>=Out+4] * Chain [[62,63,64,65],71,111,133]: 10*it(62)+4 Such that:aux(373) =< V aux(374) =< V2 it(62) =< aux(373) it(62) =< aux(374) with precondition: [V1=2,V>=2,V2>=3,Out>=6,4*V+1>=Out,4*V2>=Out+3] * Chain [[62,63,64,65],71,110,133]: 10*it(62)+4 Such that:aux(375) =< V aux(376) =< V2 it(62) =< aux(375) it(62) =< aux(376) with precondition: [V1=2,V>=2,V2>=3,Out>=7,4*V+2>=Out,4*V2>=Out+2] * Chain [[62,63,64,65],71,109,133]: 10*it(62)+5 Such that:aux(377) =< V aux(378) =< V2 it(62) =< aux(377) it(62) =< aux(378) with precondition: [V1=2,V>=2,V2>=3,Out>=8,4*V+3>=Out,4*V2>=Out+1] * Chain [[62,63,64,65],71,108,133]: 10*it(62)+5 Such that:aux(379) =< V aux(380) =< V2 it(62) =< aux(379) it(62) =< aux(380) with precondition: [V1=2,V>=2,V2>=3,Out>=9,4*V+4>=Out,4*V2>=Out] * Chain [[62,63,64,65],71,107,133]: 10*it(62)+5 Such that:aux(381) =< V aux(382) =< V2 it(62) =< aux(381) it(62) =< aux(382) with precondition: [V1=2,V>=2,V2>=3,Out>=10,4*V+5>=Out,4*V2+1>=Out] * Chain [[62,63,64,65],71,106,133]: 10*it(62)+4 Such that:aux(1) =< V aux(383) =< V2 it(62) =< aux(1) it(62) =< aux(383) with precondition: [V1=2,V2>=2,V>=V2,Out>=V2+3,4*V2>=Out] * Chain [[62,63,64,65],71,105,133]: 10*it(62)+4 Such that:aux(1) =< V aux(384) =< V2 it(62) =< aux(1) it(62) =< aux(384) with precondition: [V1=2,V2>=2,V>=V2,Out>=V2+4,4*V2+1>=Out] * Chain [[62,63,64,65],71,104,133]: 10*it(62)+5 Such that:aux(1) =< V aux(385) =< V2 it(62) =< aux(1) it(62) =< aux(385) with precondition: [V1=2,V2>=2,V>=V2,Out>=V2+6,4*V2+3>=Out] * Chain [[62,63,64,65],71,97,133]: 10*it(62)+4 Such that:aux(1) =< V aux(386) =< V2 it(62) =< aux(1) it(62) =< aux(386) with precondition: [V1=2,V2>=2,V>=V2,Out>=V2+3,4*V2>=Out] * Chain [[62,63,64,65],71,96,133]: 10*it(62)+4 Such that:aux(1) =< V aux(387) =< V2 it(62) =< aux(1) it(62) =< aux(387) with precondition: [V1=2,V2>=2,V>=V2,Out>=V2+4,4*V2+1>=Out] * Chain [[62,63,64,65],71,95,133]: 10*it(62)+5 Such that:aux(1) =< V aux(388) =< V2 it(62) =< aux(1) it(62) =< aux(388) with precondition: [V1=2,V2>=2,V>=V2,Out>=V2+6,4*V2+3>=Out] * Chain [[62,63,64,65],70,133]: 10*it(62)+3 Such that:aux(389) =< V aux(390) =< V2 it(62) =< aux(389) it(62) =< aux(390) with precondition: [V1=2,V>=2,V2>=2,Out>=5,4*V>=Out,4*V2>=Out] * Chain [[62,63,64,65],70,132,133]: 10*it(62)+5 Such that:aux(391) =< V aux(392) =< V2 it(62) =< aux(391) it(62) =< aux(392) with precondition: [V1=2,V>=2,V2>=2,Out>=6,4*V+1>=Out,4*V2+1>=Out] * Chain [[62,63,64,65],70,131,133]: 10*it(62)+5 Such that:aux(393) =< V aux(394) =< V2 it(62) =< aux(393) it(62) =< aux(394) with precondition: [V1=2,V>=2,V2>=2,Out>=7,4*V+2>=Out,4*V2+2>=Out] * Chain [[62,63,64,65],70,130,133]: 10*it(62)+6 Such that:aux(1) =< V aux(395) =< V2 it(62) =< aux(1) it(62) =< aux(395) with precondition: [V1=2,V2>=2,V>=V2,Out>=V2+6,4*V2+3>=Out] * Chain [[62,63,64,65],70,129,133]: 10*it(62)+6 Such that:aux(396) =< V aux(397) =< V2 it(62) =< aux(396) it(62) =< aux(397) with precondition: [V1=2,V>=2,V2>=2,Out>=9,4*V+4>=Out,4*V2+4>=Out] * Chain [[62,63,64,65],70,128,133]: 10*it(62)+6 Such that:aux(398) =< V aux(399) =< V2 it(62) =< aux(398) it(62) =< aux(399) with precondition: [V1=2,V>=2,V2>=2,Out>=10,4*V+5>=Out,4*V2+5>=Out] * Chain [[62,63,64,65],70,127,133]: 10*it(62)+5 Such that:aux(400) =< V aux(401) =< V2 it(62) =< aux(400) it(62) =< aux(401) with precondition: [V1=2,V>=2,V2>=2,Out>=6,4*V+1>=Out,4*V2+1>=Out] * Chain [[62,63,64,65],70,126,133]: 10*it(62)+5 Such that:aux(402) =< V aux(403) =< V2 it(62) =< aux(402) it(62) =< aux(403) with precondition: [V1=2,V>=2,V2>=2,Out>=7,4*V+2>=Out,4*V2+2>=Out] * Chain [[62,63,64,65],70,125,133]: 10*it(62)+6 Such that:aux(1) =< V aux(404) =< V2 it(62) =< aux(1) it(62) =< aux(404) with precondition: [V1=2,V2>=2,V>=V2,Out>=V2+6,4*V2+3>=Out] * Chain [[62,63,64,65],70,124,133]: 10*it(62)+6 Such that:aux(405) =< V aux(406) =< V2 it(62) =< aux(405) it(62) =< aux(406) with precondition: [V1=2,V>=2,V2>=2,Out>=9,4*V+4>=Out,4*V2+4>=Out] * Chain [[62,63,64,65],70,123,133]: 10*it(62)+6 Such that:aux(407) =< V aux(408) =< V2 it(62) =< aux(407) it(62) =< aux(408) with precondition: [V1=2,V>=2,V2>=2,Out>=10,4*V+5>=Out,4*V2+5>=Out] * Chain [[62,63,64,65],70,122,133]: 10*it(62)+5 Such that:aux(409) =< V aux(410) =< V2 it(62) =< aux(409) it(62) =< aux(410) with precondition: [V1=2,V>=2,V2>=3,Out>=8,4*V+3>=Out,4*V2>=Out+1] * Chain [[62,63,64,65],70,121,133]: 10*it(62)+6 Such that:aux(411) =< V aux(412) =< V2 it(62) =< aux(411) it(62) =< aux(412) with precondition: [V1=2,V>=2,V2>=3,Out>=11,4*V+6>=Out,4*V2+2>=Out] * Chain [[62,63,64,65],70,120,133]: 10*it(62)+5 Such that:aux(413) =< V aux(414) =< V2 it(62) =< aux(413) it(62) =< aux(414) with precondition: [V1=2,V>=2,V2>=3,Out>=6,4*V+1>=Out,4*V2>=Out+3] * Chain [[62,63,64,65],70,119,133]: 10*it(62)+5 Such that:aux(415) =< V aux(416) =< V2 it(62) =< aux(415) it(62) =< aux(416) with precondition: [V1=2,V>=2,V2>=3,Out>=7,4*V+2>=Out,4*V2>=Out+2] * Chain [[62,63,64,65],70,118,133]: 10*it(62)+5 Such that:aux(417) =< V aux(418) =< V2 it(62) =< aux(417) it(62) =< aux(418) with precondition: [V1=2,V>=2,V2>=3,Out>=8,4*V+3>=Out,4*V2>=Out+1] * Chain [[62,63,64,65],70,117,133]: 10*it(62)+6 Such that:aux(419) =< V aux(420) =< V2 it(62) =< aux(419) it(62) =< aux(420) with precondition: [V1=2,V>=2,V2>=3,Out>=9,4*V+4>=Out,4*V2>=Out] * Chain [[62,63,64,65],70,116,133]: 10*it(62)+6 Such that:aux(421) =< V aux(422) =< V2 it(62) =< aux(421) it(62) =< aux(422) with precondition: [V1=2,V>=2,V2>=3,Out>=10,4*V+5>=Out,4*V2+1>=Out] * Chain [[62,63,64,65],70,115,133]: 10*it(62)+6 Such that:aux(423) =< V aux(424) =< V2 it(62) =< aux(423) it(62) =< aux(424) with precondition: [V1=2,V>=2,V2>=3,Out>=11,4*V+6>=Out,4*V2+2>=Out] * Chain [[62,63,64,65],70,114,133]: 10*it(62)+5 Such that:aux(425) =< V aux(426) =< V2 it(62) =< aux(425) it(62) =< aux(426) with precondition: [V1=2,V>=2,V2>=3,Out>=8,4*V+3>=Out,4*V2>=Out+1] * Chain [[62,63,64,65],70,113,133]: 10*it(62)+6 Such that:aux(427) =< V aux(428) =< V2 it(62) =< aux(427) it(62) =< aux(428) with precondition: [V1=2,V>=2,V2>=3,Out>=11,4*V+6>=Out,4*V2+2>=Out] * Chain [[62,63,64,65],70,112,133]: 10*it(62)+5 Such that:aux(429) =< V aux(430) =< V2 it(62) =< aux(429) it(62) =< aux(430) with precondition: [V1=2,V>=2,V2>=3,Out>=6,4*V+1>=Out,4*V2>=Out+3] * Chain [[62,63,64,65],70,111,133]: 10*it(62)+5 Such that:aux(431) =< V aux(432) =< V2 it(62) =< aux(431) it(62) =< aux(432) with precondition: [V1=2,V>=2,V2>=3,Out>=7,4*V+2>=Out,4*V2>=Out+2] * Chain [[62,63,64,65],70,110,133]: 10*it(62)+5 Such that:aux(433) =< V aux(434) =< V2 it(62) =< aux(433) it(62) =< aux(434) with precondition: [V1=2,V>=2,V2>=3,Out>=8,4*V+3>=Out,4*V2>=Out+1] * Chain [[62,63,64,65],70,109,133]: 10*it(62)+6 Such that:aux(435) =< V aux(436) =< V2 it(62) =< aux(435) it(62) =< aux(436) with precondition: [V1=2,V>=2,V2>=3,Out>=9,4*V+4>=Out,4*V2>=Out] * Chain [[62,63,64,65],70,108,133]: 10*it(62)+6 Such that:aux(437) =< V aux(438) =< V2 it(62) =< aux(437) it(62) =< aux(438) with precondition: [V1=2,V>=2,V2>=3,Out>=10,4*V+5>=Out,4*V2+1>=Out] * Chain [[62,63,64,65],70,107,133]: 10*it(62)+6 Such that:aux(439) =< V aux(440) =< V2 it(62) =< aux(439) it(62) =< aux(440) with precondition: [V1=2,V>=2,V2>=3,Out>=11,4*V+6>=Out,4*V2+2>=Out] * Chain [[62,63,64,65],70,106,133]: 10*it(62)+5 Such that:aux(1) =< V aux(441) =< V2 it(62) =< aux(1) it(62) =< aux(441) with precondition: [V1=2,V2>=2,V>=V2,Out>=V2+4,4*V2+1>=Out] * Chain [[62,63,64,65],70,105,133]: 10*it(62)+5 Such that:aux(1) =< V aux(442) =< V2 it(62) =< aux(1) it(62) =< aux(442) with precondition: [V1=2,V2>=2,V>=V2,Out>=V2+5,4*V2+2>=Out] * Chain [[62,63,64,65],70,104,133]: 10*it(62)+6 Such that:aux(1) =< V aux(443) =< V2 it(62) =< aux(1) it(62) =< aux(443) with precondition: [V1=2,V2>=2,V>=V2,Out>=V2+7,4*V2+4>=Out] * Chain [[62,63,64,65],70,97,133]: 10*it(62)+5 Such that:aux(1) =< V aux(444) =< V2 it(62) =< aux(1) it(62) =< aux(444) with precondition: [V1=2,V2>=2,V>=V2,Out>=V2+4,4*V2+1>=Out] * Chain [[62,63,64,65],70,96,133]: 10*it(62)+5 Such that:aux(1) =< V aux(445) =< V2 it(62) =< aux(1) it(62) =< aux(445) with precondition: [V1=2,V2>=2,V>=V2,Out>=V2+5,4*V2+2>=Out] * Chain [[62,63,64,65],70,95,133]: 10*it(62)+6 Such that:aux(1) =< V aux(446) =< V2 it(62) =< aux(1) it(62) =< aux(446) with precondition: [V1=2,V2>=2,V>=V2,Out>=V2+7,4*V2+4>=Out] * Chain [[62,63,64,65],69,133]: 10*it(62)+2 Such that:aux(447) =< V aux(448) =< V2 it(62) =< aux(447) it(62) =< aux(448) with precondition: [V1=2,V>=2,V2>=2,Out>=2,4*V>=Out+3,4*V2>=Out+3] * Chain [[62,63,64,65],69,132,133]: 10*it(62)+4 Such that:aux(449) =< V aux(450) =< V2 it(62) =< aux(449) it(62) =< aux(450) with precondition: [V1=2,V>=2,V2>=2,Out>=3,4*V>=Out+2,4*V2>=Out+2] * Chain [[62,63,64,65],69,131,133]: 10*it(62)+4 Such that:aux(3) =< V2 aux(451) =< V it(62) =< aux(451) it(62) =< aux(3) with precondition: [V1=2,V>=2,V2>=V,Out>=V+2,4*V>=Out+1] * Chain [[62,63,64,65],69,130,133]: 10*it(62)+5 Such that:aux(452) =< V aux(453) =< V2 it(62) =< aux(452) it(62) =< aux(453) with precondition: [V1=2,V>=2,V2>=2,Out>=5,4*V>=Out,4*V2>=Out] * Chain [[62,63,64,65],69,129,133]: 10*it(62)+5 Such that:aux(3) =< V2 aux(454) =< V it(62) =< aux(454) it(62) =< aux(3) with precondition: [V1=2,V>=2,V2>=V,Out>=V+4,4*V+1>=Out] * Chain [[62,63,64,65],69,128,133]: 10*it(62)+5 Such that:aux(3) =< V2 aux(455) =< V it(62) =< aux(455) it(62) =< aux(3) with precondition: [V1=2,V>=2,V2>=V,Out>=V+5,4*V+2>=Out] * Chain [[62,63,64,65],69,127,133]: 10*it(62)+4 Such that:aux(3) =< V2 aux(456) =< V it(62) =< aux(456) it(62) =< aux(3) with precondition: [V1=2,V>=2,V2>=V,Out>=V+1,4*V>=Out+2] * Chain [[62,63,64,65],69,126,133]: 10*it(62)+4 Such that:aux(3) =< V2 aux(457) =< V it(62) =< aux(457) it(62) =< aux(3) with precondition: [V1=2,V>=2,V2>=V,Out>=V+2,4*V>=Out+1] * Chain [[62,63,64,65],69,125,133]: 10*it(62)+5 Such that:aux(458) =< V aux(459) =< V2 it(62) =< aux(458) it(62) =< aux(459) with precondition: [V1=2,V>=2,V2>=2,Out>=5,4*V>=Out,4*V2>=Out] * Chain [[62,63,64,65],69,124,133]: 10*it(62)+5 Such that:aux(3) =< V2 aux(460) =< V it(62) =< aux(460) it(62) =< aux(3) with precondition: [V1=2,V>=2,V2>=V,Out>=V+4,4*V+1>=Out] * Chain [[62,63,64,65],69,123,133]: 10*it(62)+5 Such that:aux(3) =< V2 aux(461) =< V it(62) =< aux(461) it(62) =< aux(3) with precondition: [V1=2,V>=2,V2>=V,Out>=V+5,4*V+2>=Out] * Chain [[62,63,64,65],69,106,133]: 10*it(62)+4 Such that:aux(462) =< V aux(463) =< V2 it(62) =< aux(462) it(62) =< aux(463) with precondition: [V1=2,V>=2,V2>=2,Out>=3,4*V>=Out+2,4*V2>=Out+2] * Chain [[62,63,64,65],69,105,133]: 10*it(62)+4 Such that:aux(464) =< V aux(465) =< V2 it(62) =< aux(464) it(62) =< aux(465) with precondition: [V1=2,V>=2,V2>=2,Out>=4,4*V>=Out+1,4*V2>=Out+1] * Chain [[62,63,64,65],69,104,133]: 10*it(62)+5 Such that:aux(466) =< V aux(467) =< V2 it(62) =< aux(466) it(62) =< aux(467) with precondition: [V1=2,V>=2,V2>=2,Out>=6,4*V+1>=Out,4*V2+1>=Out] * Chain [[62,63,64,65],69,103,133]: 10*it(62)+5 Such that:aux(468) =< V aux(469) =< V2 it(62) =< aux(468) it(62) =< aux(469) with precondition: [V1=2,V>=3,V2>=2,Out>=7,4*V>=Out+2,4*V2+2>=Out] * Chain [[62,63,64,65],69,102,133]: 10*it(62)+4 Such that:aux(470) =< V aux(471) =< V2 it(62) =< aux(470) it(62) =< aux(471) with precondition: [V1=2,V>=3,V2>=2,Out>=3,4*V>=Out+6,4*V2>=Out+2] * Chain [[62,63,64,65],69,101,133]: 10*it(62)+4 Such that:aux(472) =< V aux(473) =< V2 it(62) =< aux(472) it(62) =< aux(473) with precondition: [V1=2,V>=3,V2>=2,Out>=4,4*V>=Out+5,4*V2>=Out+1] * Chain [[62,63,64,65],69,100,133]: 10*it(62)+5 Such that:aux(474) =< V aux(475) =< V2 it(62) =< aux(474) it(62) =< aux(475) with precondition: [V1=2,V>=3,V2>=2,Out>=5,4*V>=Out+4,4*V2>=Out] * Chain [[62,63,64,65],69,99,133]: 10*it(62)+5 Such that:aux(476) =< V aux(477) =< V2 it(62) =< aux(476) it(62) =< aux(477) with precondition: [V1=2,V>=3,V2>=2,Out>=6,4*V>=Out+3,4*V2+1>=Out] * Chain [[62,63,64,65],69,98,133]: 10*it(62)+5 Such that:aux(478) =< V aux(479) =< V2 it(62) =< aux(478) it(62) =< aux(479) with precondition: [V1=2,V>=3,V2>=2,Out>=7,4*V>=Out+2,4*V2+2>=Out] * Chain [[62,63,64,65],69,97,133]: 10*it(62)+4 Such that:aux(480) =< V aux(481) =< V2 it(62) =< aux(480) it(62) =< aux(481) with precondition: [V1=2,V>=2,V2>=2,Out>=3,4*V>=Out+2,4*V2>=Out+2] * Chain [[62,63,64,65],69,96,133]: 10*it(62)+4 Such that:aux(482) =< V aux(483) =< V2 it(62) =< aux(482) it(62) =< aux(483) with precondition: [V1=2,V>=2,V2>=2,Out>=4,4*V>=Out+1,4*V2>=Out+1] * Chain [[62,63,64,65],69,95,133]: 10*it(62)+5 Such that:aux(484) =< V aux(485) =< V2 it(62) =< aux(484) it(62) =< aux(485) with precondition: [V1=2,V>=2,V2>=2,Out>=6,4*V+1>=Out,4*V2+1>=Out] * Chain [[62,63,64,65],69,94,133]: 10*it(62)+5 Such that:aux(486) =< V aux(487) =< V2 it(62) =< aux(486) it(62) =< aux(487) with precondition: [V1=2,V>=3,V2>=2,Out>=7,4*V>=Out+2,4*V2+2>=Out] * Chain [[62,63,64,65],69,93,133]: 10*it(62)+4 Such that:aux(488) =< V aux(489) =< V2 it(62) =< aux(488) it(62) =< aux(489) with precondition: [V1=2,V>=3,V2>=2,Out>=3,4*V>=Out+6,4*V2>=Out+2] * Chain [[62,63,64,65],69,92,133]: 10*it(62)+4 Such that:aux(490) =< V aux(491) =< V2 it(62) =< aux(490) it(62) =< aux(491) with precondition: [V1=2,V>=3,V2>=2,Out>=4,4*V>=Out+5,4*V2>=Out+1] * Chain [[62,63,64,65],69,91,133]: 10*it(62)+5 Such that:aux(492) =< V aux(493) =< V2 it(62) =< aux(492) it(62) =< aux(493) with precondition: [V1=2,V>=3,V2>=2,Out>=5,4*V>=Out+4,4*V2>=Out] * Chain [[62,63,64,65],69,90,133]: 10*it(62)+5 Such that:aux(494) =< V aux(495) =< V2 it(62) =< aux(494) it(62) =< aux(495) with precondition: [V1=2,V>=3,V2>=2,Out>=6,4*V>=Out+3,4*V2+1>=Out] * Chain [[62,63,64,65],69,89,133]: 10*it(62)+5 Such that:aux(496) =< V aux(497) =< V2 it(62) =< aux(496) it(62) =< aux(497) with precondition: [V1=2,V>=3,V2>=2,Out>=7,4*V>=Out+2,4*V2+2>=Out] * Chain [[62,63,64,65],69,87,133]: 10*it(62)+4 Such that:aux(498) =< V aux(499) =< V2 it(62) =< aux(498) it(62) =< aux(499) with precondition: [V1=2,V>=3,V2>=2,Out>=5,4*V>=Out+4,4*V2>=Out] * Chain [[62,63,64,65],68,133]: 10*it(62)+3 Such that:aux(500) =< V aux(501) =< V2 it(62) =< aux(500) it(62) =< aux(501) with precondition: [V1=2,V>=2,V2>=2,Out>=3,4*V>=Out+2,4*V2>=Out+2] * Chain [[62,63,64,65],68,132,133]: 10*it(62)+5 Such that:aux(502) =< V aux(503) =< V2 it(62) =< aux(502) it(62) =< aux(503) with precondition: [V1=2,V>=2,V2>=2,Out>=4,4*V>=Out+1,4*V2>=Out+1] * Chain [[62,63,64,65],68,131,133]: 10*it(62)+5 Such that:aux(3) =< V2 aux(504) =< V it(62) =< aux(504) it(62) =< aux(3) with precondition: [V1=2,V>=2,V2>=V,Out>=V+3,4*V>=Out] * Chain [[62,63,64,65],68,130,133]: 10*it(62)+6 Such that:aux(505) =< V aux(506) =< V2 it(62) =< aux(505) it(62) =< aux(506) with precondition: [V1=2,V>=2,V2>=2,Out>=6,4*V+1>=Out,4*V2+1>=Out] * Chain [[62,63,64,65],68,129,133]: 10*it(62)+6 Such that:aux(3) =< V2 aux(507) =< V it(62) =< aux(507) it(62) =< aux(3) with precondition: [V1=2,V>=2,V2>=V,Out>=V+5,4*V+2>=Out] * Chain [[62,63,64,65],68,128,133]: 10*it(62)+6 Such that:aux(3) =< V2 aux(508) =< V it(62) =< aux(508) it(62) =< aux(3) with precondition: [V1=2,V>=2,V2>=V,Out>=V+6,4*V+3>=Out] * Chain [[62,63,64,65],68,127,133]: 10*it(62)+5 Such that:aux(3) =< V2 aux(509) =< V it(62) =< aux(509) it(62) =< aux(3) with precondition: [V1=2,V>=2,V2>=V,Out>=V+2,4*V>=Out+1] * Chain [[62,63,64,65],68,126,133]: 10*it(62)+5 Such that:aux(3) =< V2 aux(510) =< V it(62) =< aux(510) it(62) =< aux(3) with precondition: [V1=2,V>=2,V2>=V,Out>=V+3,4*V>=Out] * Chain [[62,63,64,65],68,125,133]: 10*it(62)+6 Such that:aux(511) =< V aux(512) =< V2 it(62) =< aux(511) it(62) =< aux(512) with precondition: [V1=2,V>=2,V2>=2,Out>=6,4*V+1>=Out,4*V2+1>=Out] * Chain [[62,63,64,65],68,124,133]: 10*it(62)+6 Such that:aux(3) =< V2 aux(513) =< V it(62) =< aux(513) it(62) =< aux(3) with precondition: [V1=2,V>=2,V2>=V,Out>=V+5,4*V+2>=Out] * Chain [[62,63,64,65],68,123,133]: 10*it(62)+6 Such that:aux(3) =< V2 aux(514) =< V it(62) =< aux(514) it(62) =< aux(3) with precondition: [V1=2,V>=2,V2>=V,Out>=V+6,4*V+3>=Out] * Chain [[62,63,64,65],68,106,133]: 10*it(62)+5 Such that:aux(515) =< V aux(516) =< V2 it(62) =< aux(515) it(62) =< aux(516) with precondition: [V1=2,V>=2,V2>=2,Out>=4,4*V>=Out+1,4*V2>=Out+1] * Chain [[62,63,64,65],68,105,133]: 10*it(62)+5 Such that:aux(517) =< V aux(518) =< V2 it(62) =< aux(517) it(62) =< aux(518) with precondition: [V1=2,V>=2,V2>=2,Out>=5,4*V>=Out,4*V2>=Out] * Chain [[62,63,64,65],68,104,133]: 10*it(62)+6 Such that:aux(519) =< V aux(520) =< V2 it(62) =< aux(519) it(62) =< aux(520) with precondition: [V1=2,V>=2,V2>=2,Out>=7,4*V+2>=Out,4*V2+2>=Out] * Chain [[62,63,64,65],68,103,133]: 10*it(62)+6 Such that:aux(521) =< V aux(522) =< V2 it(62) =< aux(521) it(62) =< aux(522) with precondition: [V1=2,V>=3,V2>=2,Out>=8,4*V>=Out+1,4*V2+3>=Out] * Chain [[62,63,64,65],68,102,133]: 10*it(62)+5 Such that:aux(523) =< V aux(524) =< V2 it(62) =< aux(523) it(62) =< aux(524) with precondition: [V1=2,V>=3,V2>=2,Out>=4,4*V>=Out+5,4*V2>=Out+1] * Chain [[62,63,64,65],68,101,133]: 10*it(62)+5 Such that:aux(525) =< V aux(526) =< V2 it(62) =< aux(525) it(62) =< aux(526) with precondition: [V1=2,V>=3,V2>=2,Out>=5,4*V>=Out+4,4*V2>=Out] * Chain [[62,63,64,65],68,100,133]: 10*it(62)+6 Such that:aux(527) =< V aux(528) =< V2 it(62) =< aux(527) it(62) =< aux(528) with precondition: [V1=2,V>=3,V2>=2,Out>=6,4*V>=Out+3,4*V2+1>=Out] * Chain [[62,63,64,65],68,99,133]: 10*it(62)+6 Such that:aux(529) =< V aux(530) =< V2 it(62) =< aux(529) it(62) =< aux(530) with precondition: [V1=2,V>=3,V2>=2,Out>=7,4*V>=Out+2,4*V2+2>=Out] * Chain [[62,63,64,65],68,98,133]: 10*it(62)+6 Such that:aux(531) =< V aux(532) =< V2 it(62) =< aux(531) it(62) =< aux(532) with precondition: [V1=2,V>=3,V2>=2,Out>=8,4*V>=Out+1,4*V2+3>=Out] * Chain [[62,63,64,65],68,97,133]: 10*it(62)+5 Such that:aux(533) =< V aux(534) =< V2 it(62) =< aux(533) it(62) =< aux(534) with precondition: [V1=2,V>=2,V2>=2,Out>=4,4*V>=Out+1,4*V2>=Out+1] * Chain [[62,63,64,65],68,96,133]: 10*it(62)+5 Such that:aux(535) =< V aux(536) =< V2 it(62) =< aux(535) it(62) =< aux(536) with precondition: [V1=2,V>=2,V2>=2,Out>=5,4*V>=Out,4*V2>=Out] * Chain [[62,63,64,65],68,95,133]: 10*it(62)+6 Such that:aux(537) =< V aux(538) =< V2 it(62) =< aux(537) it(62) =< aux(538) with precondition: [V1=2,V>=2,V2>=2,Out>=7,4*V+2>=Out,4*V2+2>=Out] * Chain [[62,63,64,65],68,94,133]: 10*it(62)+6 Such that:aux(539) =< V aux(540) =< V2 it(62) =< aux(539) it(62) =< aux(540) with precondition: [V1=2,V>=3,V2>=2,Out>=8,4*V>=Out+1,4*V2+3>=Out] * Chain [[62,63,64,65],68,93,133]: 10*it(62)+5 Such that:aux(541) =< V aux(542) =< V2 it(62) =< aux(541) it(62) =< aux(542) with precondition: [V1=2,V>=3,V2>=2,Out>=4,4*V>=Out+5,4*V2>=Out+1] * Chain [[62,63,64,65],68,92,133]: 10*it(62)+5 Such that:aux(543) =< V aux(544) =< V2 it(62) =< aux(543) it(62) =< aux(544) with precondition: [V1=2,V>=3,V2>=2,Out>=5,4*V>=Out+4,4*V2>=Out] * Chain [[62,63,64,65],68,91,133]: 10*it(62)+6 Such that:aux(545) =< V aux(546) =< V2 it(62) =< aux(545) it(62) =< aux(546) with precondition: [V1=2,V>=3,V2>=2,Out>=6,4*V>=Out+3,4*V2+1>=Out] * Chain [[62,63,64,65],68,90,133]: 10*it(62)+6 Such that:aux(547) =< V aux(548) =< V2 it(62) =< aux(547) it(62) =< aux(548) with precondition: [V1=2,V>=3,V2>=2,Out>=7,4*V>=Out+2,4*V2+2>=Out] * Chain [[62,63,64,65],68,89,133]: 10*it(62)+6 Such that:aux(549) =< V aux(550) =< V2 it(62) =< aux(549) it(62) =< aux(550) with precondition: [V1=2,V>=3,V2>=2,Out>=8,4*V>=Out+1,4*V2+3>=Out] * Chain [[62,63,64,65],68,87,133]: 10*it(62)+5 Such that:aux(551) =< V aux(552) =< V2 it(62) =< aux(551) it(62) =< aux(552) with precondition: [V1=2,V>=3,V2>=2,Out>=6,4*V>=Out+3,4*V2+1>=Out] * Chain [[62,63,64,65],67,133]: 10*it(62)+2 Such that:aux(553) =< V aux(554) =< V2 it(62) =< aux(553) it(62) =< aux(554) with precondition: [V1=2,V>=2,V2>=2,Out>=4,4*V>=Out+1,4*V2>=Out+1] * Chain [[62,63,64,65],67,132,133]: 10*it(62)+4 Such that:aux(555) =< V aux(556) =< V2 it(62) =< aux(555) it(62) =< aux(556) with precondition: [V1=2,V>=2,V2>=2,Out>=5,4*V>=Out,4*V2>=Out] * Chain [[62,63,64,65],67,131,133]: 10*it(62)+4 Such that:aux(3) =< V2 aux(557) =< V it(62) =< aux(557) it(62) =< aux(3) with precondition: [V1=2,V>=2,V2>=V,Out>=V+4,4*V+1>=Out] * Chain [[62,63,64,65],67,130,133]: 10*it(62)+5 Such that:aux(558) =< V aux(559) =< V2 it(62) =< aux(558) it(62) =< aux(559) with precondition: [V1=2,V>=2,V2>=2,Out>=7,4*V+2>=Out,4*V2+2>=Out] * Chain [[62,63,64,65],67,129,133]: 10*it(62)+5 Such that:aux(3) =< V2 aux(560) =< V it(62) =< aux(560) it(62) =< aux(3) with precondition: [V1=2,V>=2,V2>=V,Out>=V+6,4*V+3>=Out] * Chain [[62,63,64,65],67,128,133]: 10*it(62)+5 Such that:aux(3) =< V2 aux(561) =< V it(62) =< aux(561) it(62) =< aux(3) with precondition: [V1=2,V>=2,V2>=V,Out>=V+7,4*V+4>=Out] * Chain [[62,63,64,65],67,127,133]: 10*it(62)+4 Such that:aux(3) =< V2 aux(562) =< V it(62) =< aux(562) it(62) =< aux(3) with precondition: [V1=2,V>=2,V2>=V,Out>=V+3,4*V>=Out] * Chain [[62,63,64,65],67,126,133]: 10*it(62)+4 Such that:aux(3) =< V2 aux(563) =< V it(62) =< aux(563) it(62) =< aux(3) with precondition: [V1=2,V>=2,V2>=V,Out>=V+4,4*V+1>=Out] * Chain [[62,63,64,65],67,125,133]: 10*it(62)+5 Such that:aux(564) =< V aux(565) =< V2 it(62) =< aux(564) it(62) =< aux(565) with precondition: [V1=2,V>=2,V2>=2,Out>=7,4*V+2>=Out,4*V2+2>=Out] * Chain [[62,63,64,65],67,124,133]: 10*it(62)+5 Such that:aux(3) =< V2 aux(566) =< V it(62) =< aux(566) it(62) =< aux(3) with precondition: [V1=2,V>=2,V2>=V,Out>=V+6,4*V+3>=Out] * Chain [[62,63,64,65],67,123,133]: 10*it(62)+5 Such that:aux(3) =< V2 aux(567) =< V it(62) =< aux(567) it(62) =< aux(3) with precondition: [V1=2,V>=2,V2>=V,Out>=V+7,4*V+4>=Out] * Chain [[62,63,64,65],67,106,133]: 10*it(62)+4 Such that:aux(568) =< V aux(569) =< V2 it(62) =< aux(568) it(62) =< aux(569) with precondition: [V1=2,V>=2,V2>=2,Out>=5,4*V>=Out,4*V2>=Out] * Chain [[62,63,64,65],67,105,133]: 10*it(62)+4 Such that:aux(570) =< V aux(571) =< V2 it(62) =< aux(570) it(62) =< aux(571) with precondition: [V1=2,V>=2,V2>=2,Out>=6,4*V+1>=Out,4*V2+1>=Out] * Chain [[62,63,64,65],67,104,133]: 10*it(62)+5 Such that:aux(572) =< V aux(573) =< V2 it(62) =< aux(572) it(62) =< aux(573) with precondition: [V1=2,V>=2,V2>=2,Out>=8,4*V+3>=Out,4*V2+3>=Out] * Chain [[62,63,64,65],67,103,133]: 10*it(62)+5 Such that:aux(574) =< V aux(575) =< V2 it(62) =< aux(574) it(62) =< aux(575) with precondition: [V1=2,V>=3,V2>=2,Out>=9,4*V>=Out,4*V2+4>=Out] * Chain [[62,63,64,65],67,102,133]: 10*it(62)+4 Such that:aux(576) =< V aux(577) =< V2 it(62) =< aux(576) it(62) =< aux(577) with precondition: [V1=2,V>=3,V2>=2,Out>=5,4*V>=Out+4,4*V2>=Out] * Chain [[62,63,64,65],67,101,133]: 10*it(62)+4 Such that:aux(578) =< V aux(579) =< V2 it(62) =< aux(578) it(62) =< aux(579) with precondition: [V1=2,V>=3,V2>=2,Out>=6,4*V>=Out+3,4*V2+1>=Out] * Chain [[62,63,64,65],67,100,133]: 10*it(62)+5 Such that:aux(580) =< V aux(581) =< V2 it(62) =< aux(580) it(62) =< aux(581) with precondition: [V1=2,V>=3,V2>=2,Out>=7,4*V>=Out+2,4*V2+2>=Out] * Chain [[62,63,64,65],67,99,133]: 10*it(62)+5 Such that:aux(582) =< V aux(583) =< V2 it(62) =< aux(582) it(62) =< aux(583) with precondition: [V1=2,V>=3,V2>=2,Out>=8,4*V>=Out+1,4*V2+3>=Out] * Chain [[62,63,64,65],67,98,133]: 10*it(62)+5 Such that:aux(584) =< V aux(585) =< V2 it(62) =< aux(584) it(62) =< aux(585) with precondition: [V1=2,V>=3,V2>=2,Out>=9,4*V>=Out,4*V2+4>=Out] * Chain [[62,63,64,65],67,97,133]: 10*it(62)+4 Such that:aux(586) =< V aux(587) =< V2 it(62) =< aux(586) it(62) =< aux(587) with precondition: [V1=2,V>=2,V2>=2,Out>=5,4*V>=Out,4*V2>=Out] * Chain [[62,63,64,65],67,96,133]: 10*it(62)+4 Such that:aux(588) =< V aux(589) =< V2 it(62) =< aux(588) it(62) =< aux(589) with precondition: [V1=2,V>=2,V2>=2,Out>=6,4*V+1>=Out,4*V2+1>=Out] * Chain [[62,63,64,65],67,95,133]: 10*it(62)+5 Such that:aux(590) =< V aux(591) =< V2 it(62) =< aux(590) it(62) =< aux(591) with precondition: [V1=2,V>=2,V2>=2,Out>=8,4*V+3>=Out,4*V2+3>=Out] * Chain [[62,63,64,65],67,94,133]: 10*it(62)+5 Such that:aux(592) =< V aux(593) =< V2 it(62) =< aux(592) it(62) =< aux(593) with precondition: [V1=2,V>=3,V2>=2,Out>=9,4*V>=Out,4*V2+4>=Out] * Chain [[62,63,64,65],67,93,133]: 10*it(62)+4 Such that:aux(594) =< V aux(595) =< V2 it(62) =< aux(594) it(62) =< aux(595) with precondition: [V1=2,V>=3,V2>=2,Out>=5,4*V>=Out+4,4*V2>=Out] * Chain [[62,63,64,65],67,92,133]: 10*it(62)+4 Such that:aux(596) =< V aux(597) =< V2 it(62) =< aux(596) it(62) =< aux(597) with precondition: [V1=2,V>=3,V2>=2,Out>=6,4*V>=Out+3,4*V2+1>=Out] * Chain [[62,63,64,65],67,91,133]: 10*it(62)+5 Such that:aux(598) =< V aux(599) =< V2 it(62) =< aux(598) it(62) =< aux(599) with precondition: [V1=2,V>=3,V2>=2,Out>=7,4*V>=Out+2,4*V2+2>=Out] * Chain [[62,63,64,65],67,90,133]: 10*it(62)+5 Such that:aux(600) =< V aux(601) =< V2 it(62) =< aux(600) it(62) =< aux(601) with precondition: [V1=2,V>=3,V2>=2,Out>=8,4*V>=Out+1,4*V2+3>=Out] * Chain [[62,63,64,65],67,89,133]: 10*it(62)+5 Such that:aux(602) =< V aux(603) =< V2 it(62) =< aux(602) it(62) =< aux(603) with precondition: [V1=2,V>=3,V2>=2,Out>=9,4*V>=Out,4*V2+4>=Out] * Chain [[62,63,64,65],67,87,133]: 10*it(62)+4 Such that:aux(604) =< V aux(605) =< V2 it(62) =< aux(604) it(62) =< aux(605) with precondition: [V1=2,V>=3,V2>=2,Out>=7,4*V>=Out+2,4*V2+2>=Out] * Chain [[62,63,64,65],66,133]: 10*it(62)+3 Such that:aux(606) =< V aux(607) =< V2 it(62) =< aux(606) it(62) =< aux(607) with precondition: [V1=2,V>=2,V2>=2,Out>=5,4*V>=Out,4*V2>=Out] * Chain [[62,63,64,65],66,132,133]: 10*it(62)+5 Such that:aux(608) =< V aux(609) =< V2 it(62) =< aux(608) it(62) =< aux(609) with precondition: [V1=2,V>=2,V2>=2,Out>=6,4*V+1>=Out,4*V2+1>=Out] * Chain [[62,63,64,65],66,131,133]: 10*it(62)+5 Such that:aux(3) =< V2 aux(610) =< V it(62) =< aux(610) it(62) =< aux(3) with precondition: [V1=2,V>=2,V2>=V,Out>=V+5,4*V+2>=Out] * Chain [[62,63,64,65],66,130,133]: 10*it(62)+6 Such that:aux(611) =< V aux(612) =< V2 it(62) =< aux(611) it(62) =< aux(612) with precondition: [V1=2,V>=2,V2>=2,Out>=8,4*V+3>=Out,4*V2+3>=Out] * Chain [[62,63,64,65],66,129,133]: 10*it(62)+6 Such that:aux(3) =< V2 aux(613) =< V it(62) =< aux(613) it(62) =< aux(3) with precondition: [V1=2,V>=2,V2>=V,Out>=V+7,4*V+4>=Out] * Chain [[62,63,64,65],66,128,133]: 10*it(62)+6 Such that:aux(3) =< V2 aux(614) =< V it(62) =< aux(614) it(62) =< aux(3) with precondition: [V1=2,V>=2,V2>=V,Out>=V+8,4*V+5>=Out] * Chain [[62,63,64,65],66,127,133]: 10*it(62)+5 Such that:aux(3) =< V2 aux(615) =< V it(62) =< aux(615) it(62) =< aux(3) with precondition: [V1=2,V>=2,V2>=V,Out>=V+4,4*V+1>=Out] * Chain [[62,63,64,65],66,126,133]: 10*it(62)+5 Such that:aux(3) =< V2 aux(616) =< V it(62) =< aux(616) it(62) =< aux(3) with precondition: [V1=2,V>=2,V2>=V,Out>=V+5,4*V+2>=Out] * Chain [[62,63,64,65],66,125,133]: 10*it(62)+6 Such that:aux(617) =< V aux(618) =< V2 it(62) =< aux(617) it(62) =< aux(618) with precondition: [V1=2,V>=2,V2>=2,Out>=8,4*V+3>=Out,4*V2+3>=Out] * Chain [[62,63,64,65],66,124,133]: 10*it(62)+6 Such that:aux(3) =< V2 aux(619) =< V it(62) =< aux(619) it(62) =< aux(3) with precondition: [V1=2,V>=2,V2>=V,Out>=V+7,4*V+4>=Out] * Chain [[62,63,64,65],66,123,133]: 10*it(62)+6 Such that:aux(3) =< V2 aux(620) =< V it(62) =< aux(620) it(62) =< aux(3) with precondition: [V1=2,V>=2,V2>=V,Out>=V+8,4*V+5>=Out] * Chain [[62,63,64,65],66,106,133]: 10*it(62)+5 Such that:aux(621) =< V aux(622) =< V2 it(62) =< aux(621) it(62) =< aux(622) with precondition: [V1=2,V>=2,V2>=2,Out>=6,4*V+1>=Out,4*V2+1>=Out] * Chain [[62,63,64,65],66,105,133]: 10*it(62)+5 Such that:aux(623) =< V aux(624) =< V2 it(62) =< aux(623) it(62) =< aux(624) with precondition: [V1=2,V>=2,V2>=2,Out>=7,4*V+2>=Out,4*V2+2>=Out] * Chain [[62,63,64,65],66,104,133]: 10*it(62)+6 Such that:aux(625) =< V aux(626) =< V2 it(62) =< aux(625) it(62) =< aux(626) with precondition: [V1=2,V>=2,V2>=2,Out>=9,4*V+4>=Out,4*V2+4>=Out] * Chain [[62,63,64,65],66,103,133]: 10*it(62)+6 Such that:aux(627) =< V aux(628) =< V2 it(62) =< aux(627) it(62) =< aux(628) with precondition: [V1=2,V>=3,V2>=2,Out>=10,4*V+1>=Out,4*V2+5>=Out] * Chain [[62,63,64,65],66,102,133]: 10*it(62)+5 Such that:aux(629) =< V aux(630) =< V2 it(62) =< aux(629) it(62) =< aux(630) with precondition: [V1=2,V>=3,V2>=2,Out>=6,4*V>=Out+3,4*V2+1>=Out] * Chain [[62,63,64,65],66,101,133]: 10*it(62)+5 Such that:aux(631) =< V aux(632) =< V2 it(62) =< aux(631) it(62) =< aux(632) with precondition: [V1=2,V>=3,V2>=2,Out>=7,4*V>=Out+2,4*V2+2>=Out] * Chain [[62,63,64,65],66,100,133]: 10*it(62)+6 Such that:aux(633) =< V aux(634) =< V2 it(62) =< aux(633) it(62) =< aux(634) with precondition: [V1=2,V>=3,V2>=2,Out>=8,4*V>=Out+1,4*V2+3>=Out] * Chain [[62,63,64,65],66,99,133]: 10*it(62)+6 Such that:aux(635) =< V aux(636) =< V2 it(62) =< aux(635) it(62) =< aux(636) with precondition: [V1=2,V>=3,V2>=2,Out>=9,4*V>=Out,4*V2+4>=Out] * Chain [[62,63,64,65],66,98,133]: 10*it(62)+6 Such that:aux(637) =< V aux(638) =< V2 it(62) =< aux(637) it(62) =< aux(638) with precondition: [V1=2,V>=3,V2>=2,Out>=10,4*V+1>=Out,4*V2+5>=Out] * Chain [[62,63,64,65],66,97,133]: 10*it(62)+5 Such that:aux(639) =< V aux(640) =< V2 it(62) =< aux(639) it(62) =< aux(640) with precondition: [V1=2,V>=2,V2>=2,Out>=6,4*V+1>=Out,4*V2+1>=Out] * Chain [[62,63,64,65],66,96,133]: 10*it(62)+5 Such that:aux(641) =< V aux(642) =< V2 it(62) =< aux(641) it(62) =< aux(642) with precondition: [V1=2,V>=2,V2>=2,Out>=7,4*V+2>=Out,4*V2+2>=Out] * Chain [[62,63,64,65],66,95,133]: 10*it(62)+6 Such that:aux(643) =< V aux(644) =< V2 it(62) =< aux(643) it(62) =< aux(644) with precondition: [V1=2,V>=2,V2>=2,Out>=9,4*V+4>=Out,4*V2+4>=Out] * Chain [[62,63,64,65],66,94,133]: 10*it(62)+6 Such that:aux(645) =< V aux(646) =< V2 it(62) =< aux(645) it(62) =< aux(646) with precondition: [V1=2,V>=3,V2>=2,Out>=10,4*V+1>=Out,4*V2+5>=Out] * Chain [[62,63,64,65],66,93,133]: 10*it(62)+5 Such that:aux(647) =< V aux(648) =< V2 it(62) =< aux(647) it(62) =< aux(648) with precondition: [V1=2,V>=3,V2>=2,Out>=6,4*V>=Out+3,4*V2+1>=Out] * Chain [[62,63,64,65],66,92,133]: 10*it(62)+5 Such that:aux(649) =< V aux(650) =< V2 it(62) =< aux(649) it(62) =< aux(650) with precondition: [V1=2,V>=3,V2>=2,Out>=7,4*V>=Out+2,4*V2+2>=Out] * Chain [[62,63,64,65],66,91,133]: 10*it(62)+6 Such that:aux(651) =< V aux(652) =< V2 it(62) =< aux(651) it(62) =< aux(652) with precondition: [V1=2,V>=3,V2>=2,Out>=8,4*V>=Out+1,4*V2+3>=Out] * Chain [[62,63,64,65],66,90,133]: 10*it(62)+6 Such that:aux(653) =< V aux(654) =< V2 it(62) =< aux(653) it(62) =< aux(654) with precondition: [V1=2,V>=3,V2>=2,Out>=9,4*V>=Out,4*V2+4>=Out] * Chain [[62,63,64,65],66,89,133]: 10*it(62)+6 Such that:aux(655) =< V aux(656) =< V2 it(62) =< aux(655) it(62) =< aux(656) with precondition: [V1=2,V>=3,V2>=2,Out>=10,4*V+1>=Out,4*V2+5>=Out] * Chain [[62,63,64,65],66,87,133]: 10*it(62)+5 Such that:aux(657) =< V aux(658) =< V2 it(62) =< aux(657) it(62) =< aux(658) with precondition: [V1=2,V>=3,V2>=2,Out>=8,4*V>=Out+1,4*V2+3>=Out] * Chain [133]: 0 with precondition: [Out=0,V1>=0,V>=0,V2>=0] * Chain [132,133]: 2 with precondition: [V1=2,Out=1,V>=0,V2>=0] * Chain [131,133]: 2 with precondition: [V1=2,V=0,Out=2,V2>=0] * Chain [130,133]: 3 with precondition: [V1=2,V2=0,Out=3,V>=0] * Chain [129,133]: 3 with precondition: [V1=2,V=0,Out=4,V2>=0] * Chain [128,133]: 3 with precondition: [V1=2,V=0,Out=5,V2>=0] * Chain [127,133]: 2 with precondition: [V1=2,V=0,Out=1,V2>=0] * Chain [126,133]: 2 with precondition: [V1=2,V=0,Out=2,V2>=0] * Chain [125,133]: 3 with precondition: [V1=2,V2=0,Out=3,V>=0] * Chain [124,133]: 3 with precondition: [V1=2,V=0,Out=4,V2>=0] * Chain [123,133]: 3 with precondition: [V1=2,V=0,Out=5,V2>=0] * Chain [122,133]: 2 with precondition: [V1=2,Out=3,V>=0,V2>=1] * Chain [121,133]: 3 with precondition: [V1=2,V=0,Out=6,V2>=1] * Chain [120,133]: 2 with precondition: [V1=2,Out=1,V>=0,V2>=1] * Chain [119,133]: 2 with precondition: [V1=2,V=0,Out=2,V2>=1] * Chain [118,133]: 2 with precondition: [V1=2,Out=3,V>=0,V2>=1] * Chain [117,133]: 3 with precondition: [V1=2,V=0,Out=4,V2>=1] * Chain [116,133]: 3 with precondition: [V1=2,V=0,Out=5,V2>=1] * Chain [115,133]: 3 with precondition: [V1=2,V=0,Out=6,V2>=1] * Chain [114,133]: 2 with precondition: [V1=2,V=0,Out=3,V2>=1] * Chain [113,133]: 3 with precondition: [V1=2,V=0,Out=6,V2>=1] * Chain [112,133]: 2 with precondition: [V1=2,V=0,Out=1,V2>=1] * Chain [111,133]: 2 with precondition: [V1=2,V=0,Out=2,V2>=1] * Chain [110,133]: 2 with precondition: [V1=2,V=0,Out=3,V2>=1] * Chain [109,133]: 3 with precondition: [V1=2,V=0,Out=4,V2>=1] * Chain [108,133]: 3 with precondition: [V1=2,V=0,Out=5,V2>=1] * Chain [107,133]: 3 with precondition: [V1=2,V=0,Out=6,V2>=1] * Chain [106,133]: 2 with precondition: [V1=2,V2=0,Out=1,V>=0] * Chain [105,133]: 2 with precondition: [V1=2,V2=0,Out=2,V>=0] * Chain [104,133]: 3 with precondition: [V1=2,V2=0,Out=4,V>=0] * Chain [103,133]: 3 with precondition: [V1=2,V2=0,Out=5,V>=1] * Chain [102,133]: 2 with precondition: [V1=2,Out=1,V>=1,V2>=0] * Chain [101,133]: 2 with precondition: [V1=2,V2=0,Out=2,V>=1] * Chain [100,133]: 3 with precondition: [V1=2,Out=3,V>=1,V2>=0] * Chain [99,133]: 3 with precondition: [V1=2,V2=0,Out=4,V>=1] * Chain [98,133]: 3 with precondition: [V1=2,V2=0,Out=5,V>=1] * Chain [97,133]: 2 with precondition: [V1=2,V2=0,Out=1,V>=0] * Chain [96,133]: 2 with precondition: [V1=2,V2=0,Out=2,V>=0] * Chain [95,133]: 3 with precondition: [V1=2,V2=0,Out=4,V>=0] * Chain [94,133]: 3 with precondition: [V1=2,V2=0,Out=5,V>=1] * Chain [93,133]: 2 with precondition: [V1=2,V2=0,Out=1,V>=1] * Chain [92,133]: 2 with precondition: [V1=2,V2=0,Out=2,V>=1] * Chain [91,133]: 3 with precondition: [V1=2,V2=0,Out=3,V>=1] * Chain [90,133]: 3 with precondition: [V1=2,V2=0,Out=4,V>=1] * Chain [89,133]: 3 with precondition: [V1=2,V2=0,Out=5,V>=1] * Chain [88,133]: 3 with precondition: [V1=2,Out=2,V>=1,V2>=1] * Chain [87,133]: 2 with precondition: [V1=2,Out=3,V>=1,V2>=0] * Chain [86,133]: 3 with precondition: [V1=2,Out=4,V>=1,V2>=1] * Chain [85,133]: 3 with precondition: [V1=2,Out=2,V>=1,V2>=1] * Chain [84,133]: 3 with precondition: [V1=2,Out=4,V>=1,V2>=1] * Chain [83,133]: 3 with precondition: [V1=2,Out=2,V>=1,V2>=1] * Chain [82,133]: 3 with precondition: [V1=2,Out=4,V>=1,V2>=1] * Chain [81,133]: 2 with precondition: [V1=2,Out=1,V>=1,V2>=1] * Chain [80,133]: 3 with precondition: [V1=2,Out=2,V>=1,V2>=1] * Chain [79,133]: 2 with precondition: [V1=2,Out=3,V>=1,V2>=1] * Chain [78,133]: 3 with precondition: [V1=2,Out=4,V>=1,V2>=1] * Chain [77,133]: 2 with precondition: [V1=2,Out=1,V>=1,V2>=1] * Chain [77,132,133]: 4 with precondition: [V1=2,Out=2,V>=1,V2>=1] * Chain [77,131,133]: 4 with precondition: [V1=2,Out=3,V>=1,V2>=1] * Chain [77,130,133]: 5 with precondition: [V1=2,Out=4,V>=1,V2>=1] * Chain [77,129,133]: 5 with precondition: [V1=2,Out=5,V>=1,V2>=1] * Chain [77,128,133]: 5 with precondition: [V1=2,Out=6,V>=1,V2>=1] * Chain [77,127,133]: 4 with precondition: [V1=2,Out=2,V>=1,V2>=1] * Chain [77,126,133]: 4 with precondition: [V1=2,Out=3,V>=1,V2>=1] * Chain [77,125,133]: 5 with precondition: [V1=2,Out=4,V>=1,V2>=1] * Chain [77,124,133]: 5 with precondition: [V1=2,Out=5,V>=1,V2>=1] * Chain [77,123,133]: 5 with precondition: [V1=2,Out=6,V>=1,V2>=1] * Chain [77,106,133]: 4 with precondition: [V1=2,Out=2,V>=1,V2>=1] * Chain [77,105,133]: 4 with precondition: [V1=2,Out=3,V>=1,V2>=1] * Chain [77,104,133]: 5 with precondition: [V1=2,Out=5,V>=1,V2>=1] * Chain [77,97,133]: 4 with precondition: [V1=2,Out=2,V>=1,V2>=1] * Chain [77,96,133]: 4 with precondition: [V1=2,Out=3,V>=1,V2>=1] * Chain [77,95,133]: 5 with precondition: [V1=2,Out=5,V>=1,V2>=1] * Chain [76,133]: 3 with precondition: [V1=2,Out=2,V>=1,V2>=1] * Chain [76,132,133]: 5 with precondition: [V1=2,Out=3,V>=1,V2>=1] * Chain [76,131,133]: 5 with precondition: [V1=2,Out=4,V>=1,V2>=1] * Chain [76,130,133]: 6 with precondition: [V1=2,Out=5,V>=1,V2>=1] * Chain [76,129,133]: 6 with precondition: [V1=2,Out=6,V>=1,V2>=1] * Chain [76,128,133]: 6 with precondition: [V1=2,Out=7,V>=1,V2>=1] * Chain [76,127,133]: 5 with precondition: [V1=2,Out=3,V>=1,V2>=1] * Chain [76,126,133]: 5 with precondition: [V1=2,Out=4,V>=1,V2>=1] * Chain [76,125,133]: 6 with precondition: [V1=2,Out=5,V>=1,V2>=1] * Chain [76,124,133]: 6 with precondition: [V1=2,Out=6,V>=1,V2>=1] * Chain [76,123,133]: 6 with precondition: [V1=2,Out=7,V>=1,V2>=1] * Chain [76,106,133]: 5 with precondition: [V1=2,Out=3,V>=1,V2>=1] * Chain [76,105,133]: 5 with precondition: [V1=2,Out=4,V>=1,V2>=1] * Chain [76,104,133]: 6 with precondition: [V1=2,Out=6,V>=1,V2>=1] * Chain [76,97,133]: 5 with precondition: [V1=2,Out=3,V>=1,V2>=1] * Chain [76,96,133]: 5 with precondition: [V1=2,Out=4,V>=1,V2>=1] * Chain [76,95,133]: 6 with precondition: [V1=2,Out=6,V>=1,V2>=1] * Chain [75,133]: 2 with precondition: [V1=2,Out=3,V>=1,V2>=1] * Chain [75,132,133]: 4 with precondition: [V1=2,Out=4,V>=1,V2>=1] * Chain [75,131,133]: 4 with precondition: [V1=2,Out=5,V>=1,V2>=1] * Chain [75,130,133]: 5 with precondition: [V1=2,Out=6,V>=1,V2>=1] * Chain [75,129,133]: 5 with precondition: [V1=2,Out=7,V>=1,V2>=1] * Chain [75,128,133]: 5 with precondition: [V1=2,Out=8,V>=1,V2>=1] * Chain [75,127,133]: 4 with precondition: [V1=2,Out=4,V>=1,V2>=1] * Chain [75,126,133]: 4 with precondition: [V1=2,Out=5,V>=1,V2>=1] * Chain [75,125,133]: 5 with precondition: [V1=2,Out=6,V>=1,V2>=1] * Chain [75,124,133]: 5 with precondition: [V1=2,Out=7,V>=1,V2>=1] * Chain [75,123,133]: 5 with precondition: [V1=2,Out=8,V>=1,V2>=1] * Chain [75,106,133]: 4 with precondition: [V1=2,Out=4,V>=1,V2>=1] * Chain [75,105,133]: 4 with precondition: [V1=2,Out=5,V>=1,V2>=1] * Chain [75,104,133]: 5 with precondition: [V1=2,Out=7,V>=1,V2>=1] * Chain [75,97,133]: 4 with precondition: [V1=2,Out=4,V>=1,V2>=1] * Chain [75,96,133]: 4 with precondition: [V1=2,Out=5,V>=1,V2>=1] * Chain [75,95,133]: 5 with precondition: [V1=2,Out=7,V>=1,V2>=1] * Chain [74,133]: 3 with precondition: [V1=2,Out=4,V>=1,V2>=1] * Chain [74,132,133]: 5 with precondition: [V1=2,Out=5,V>=1,V2>=1] * Chain [74,131,133]: 5 with precondition: [V1=2,Out=6,V>=1,V2>=1] * Chain [74,130,133]: 6 with precondition: [V1=2,Out=7,V>=1,V2>=1] * Chain [74,129,133]: 6 with precondition: [V1=2,Out=8,V>=1,V2>=1] * Chain [74,128,133]: 6 with precondition: [V1=2,Out=9,V>=1,V2>=1] * Chain [74,127,133]: 5 with precondition: [V1=2,Out=5,V>=1,V2>=1] * Chain [74,126,133]: 5 with precondition: [V1=2,Out=6,V>=1,V2>=1] * Chain [74,125,133]: 6 with precondition: [V1=2,Out=7,V>=1,V2>=1] * Chain [74,124,133]: 6 with precondition: [V1=2,Out=8,V>=1,V2>=1] * Chain [74,123,133]: 6 with precondition: [V1=2,Out=9,V>=1,V2>=1] * Chain [74,106,133]: 5 with precondition: [V1=2,Out=5,V>=1,V2>=1] * Chain [74,105,133]: 5 with precondition: [V1=2,Out=6,V>=1,V2>=1] * Chain [74,104,133]: 6 with precondition: [V1=2,Out=8,V>=1,V2>=1] * Chain [74,97,133]: 5 with precondition: [V1=2,Out=5,V>=1,V2>=1] * Chain [74,96,133]: 5 with precondition: [V1=2,Out=6,V>=1,V2>=1] * Chain [74,95,133]: 6 with precondition: [V1=2,Out=8,V>=1,V2>=1] * Chain [73,133]: 2 with precondition: [V1=2,Out=1,V>=1,V2>=1] * Chain [73,132,133]: 4 with precondition: [V1=2,Out=2,V>=1,V2>=1] * Chain [73,131,133]: 4 with precondition: [V1=2,Out=3,V>=1,V2>=1] * Chain [73,130,133]: 5 with precondition: [V1=2,V2=1,Out=4,V>=1] * Chain [73,129,133]: 5 with precondition: [V1=2,Out=5,V>=1,V2>=1] * Chain [73,128,133]: 5 with precondition: [V1=2,Out=6,V>=1,V2>=1] * Chain [73,127,133]: 4 with precondition: [V1=2,Out=2,V>=1,V2>=1] * Chain [73,126,133]: 4 with precondition: [V1=2,Out=3,V>=1,V2>=1] * Chain [73,125,133]: 5 with precondition: [V1=2,V2=1,Out=4,V>=1] * Chain [73,124,133]: 5 with precondition: [V1=2,Out=5,V>=1,V2>=1] * Chain [73,123,133]: 5 with precondition: [V1=2,Out=6,V>=1,V2>=1] * Chain [73,122,133]: 4 with precondition: [V1=2,Out=4,V>=1,V2>=2] * Chain [73,121,133]: 5 with precondition: [V1=2,Out=7,V>=1,V2>=2] * Chain [73,120,133]: 4 with precondition: [V1=2,Out=2,V>=1,V2>=2] * Chain [73,119,133]: 4 with precondition: [V1=2,Out=3,V>=1,V2>=2] * Chain [73,118,133]: 4 with precondition: [V1=2,Out=4,V>=1,V2>=2] * Chain [73,117,133]: 5 with precondition: [V1=2,Out=5,V>=1,V2>=2] * Chain [73,116,133]: 5 with precondition: [V1=2,Out=6,V>=1,V2>=2] * Chain [73,115,133]: 5 with precondition: [V1=2,Out=7,V>=1,V2>=2] * Chain [73,114,133]: 4 with precondition: [V1=2,Out=4,V>=1,V2>=2] * Chain [73,113,133]: 5 with precondition: [V1=2,Out=7,V>=1,V2>=2] * Chain [73,112,133]: 4 with precondition: [V1=2,Out=2,V>=1,V2>=2] * Chain [73,111,133]: 4 with precondition: [V1=2,Out=3,V>=1,V2>=2] * Chain [73,110,133]: 4 with precondition: [V1=2,Out=4,V>=1,V2>=2] * Chain [73,109,133]: 5 with precondition: [V1=2,Out=5,V>=1,V2>=2] * Chain [73,108,133]: 5 with precondition: [V1=2,Out=6,V>=1,V2>=2] * Chain [73,107,133]: 5 with precondition: [V1=2,Out=7,V>=1,V2>=2] * Chain [73,106,133]: 4 with precondition: [V1=2,V2=1,Out=2,V>=1] * Chain [73,105,133]: 4 with precondition: [V1=2,V2=1,Out=3,V>=1] * Chain [73,104,133]: 5 with precondition: [V1=2,V2=1,Out=5,V>=1] * Chain [73,97,133]: 4 with precondition: [V1=2,V2=1,Out=2,V>=1] * Chain [73,96,133]: 4 with precondition: [V1=2,V2=1,Out=3,V>=1] * Chain [73,95,133]: 5 with precondition: [V1=2,V2=1,Out=5,V>=1] * Chain [72,133]: 3 with precondition: [V1=2,Out=2,V>=1,V2>=1] * Chain [72,132,133]: 5 with precondition: [V1=2,Out=3,V>=1,V2>=1] * Chain [72,131,133]: 5 with precondition: [V1=2,Out=4,V>=1,V2>=1] * Chain [72,130,133]: 6 with precondition: [V1=2,V2=1,Out=5,V>=1] * Chain [72,129,133]: 6 with precondition: [V1=2,Out=6,V>=1,V2>=1] * Chain [72,128,133]: 6 with precondition: [V1=2,Out=7,V>=1,V2>=1] * Chain [72,127,133]: 5 with precondition: [V1=2,Out=3,V>=1,V2>=1] * Chain [72,126,133]: 5 with precondition: [V1=2,Out=4,V>=1,V2>=1] * Chain [72,125,133]: 6 with precondition: [V1=2,V2=1,Out=5,V>=1] * Chain [72,124,133]: 6 with precondition: [V1=2,Out=6,V>=1,V2>=1] * Chain [72,123,133]: 6 with precondition: [V1=2,Out=7,V>=1,V2>=1] * Chain [72,122,133]: 5 with precondition: [V1=2,Out=5,V>=1,V2>=2] * Chain [72,121,133]: 6 with precondition: [V1=2,Out=8,V>=1,V2>=2] * Chain [72,120,133]: 5 with precondition: [V1=2,Out=3,V>=1,V2>=2] * Chain [72,119,133]: 5 with precondition: [V1=2,Out=4,V>=1,V2>=2] * Chain [72,118,133]: 5 with precondition: [V1=2,Out=5,V>=1,V2>=2] * Chain [72,117,133]: 6 with precondition: [V1=2,Out=6,V>=1,V2>=2] * Chain [72,116,133]: 6 with precondition: [V1=2,Out=7,V>=1,V2>=2] * Chain [72,115,133]: 6 with precondition: [V1=2,Out=8,V>=1,V2>=2] * Chain [72,114,133]: 5 with precondition: [V1=2,Out=5,V>=1,V2>=2] * Chain [72,113,133]: 6 with precondition: [V1=2,Out=8,V>=1,V2>=2] * Chain [72,112,133]: 5 with precondition: [V1=2,Out=3,V>=1,V2>=2] * Chain [72,111,133]: 5 with precondition: [V1=2,Out=4,V>=1,V2>=2] * Chain [72,110,133]: 5 with precondition: [V1=2,Out=5,V>=1,V2>=2] * Chain [72,109,133]: 6 with precondition: [V1=2,Out=6,V>=1,V2>=2] * Chain [72,108,133]: 6 with precondition: [V1=2,Out=7,V>=1,V2>=2] * Chain [72,107,133]: 6 with precondition: [V1=2,Out=8,V>=1,V2>=2] * Chain [72,106,133]: 5 with precondition: [V1=2,V2=1,Out=3,V>=1] * Chain [72,105,133]: 5 with precondition: [V1=2,V2=1,Out=4,V>=1] * Chain [72,104,133]: 6 with precondition: [V1=2,V2=1,Out=6,V>=1] * Chain [72,97,133]: 5 with precondition: [V1=2,V2=1,Out=3,V>=1] * Chain [72,96,133]: 5 with precondition: [V1=2,V2=1,Out=4,V>=1] * Chain [72,95,133]: 6 with precondition: [V1=2,V2=1,Out=6,V>=1] * Chain [71,133]: 2 with precondition: [V1=2,Out=3,V>=1,V2>=1] * Chain [71,132,133]: 4 with precondition: [V1=2,Out=4,V>=1,V2>=1] * Chain [71,131,133]: 4 with precondition: [V1=2,Out=5,V>=1,V2>=1] * Chain [71,130,133]: 5 with precondition: [V1=2,V2=1,Out=6,V>=1] * Chain [71,129,133]: 5 with precondition: [V1=2,Out=7,V>=1,V2>=1] * Chain [71,128,133]: 5 with precondition: [V1=2,Out=8,V>=1,V2>=1] * Chain [71,127,133]: 4 with precondition: [V1=2,Out=4,V>=1,V2>=1] * Chain [71,126,133]: 4 with precondition: [V1=2,Out=5,V>=1,V2>=1] * Chain [71,125,133]: 5 with precondition: [V1=2,V2=1,Out=6,V>=1] * Chain [71,124,133]: 5 with precondition: [V1=2,Out=7,V>=1,V2>=1] * Chain [71,123,133]: 5 with precondition: [V1=2,Out=8,V>=1,V2>=1] * Chain [71,122,133]: 4 with precondition: [V1=2,Out=6,V>=1,V2>=2] * Chain [71,121,133]: 5 with precondition: [V1=2,Out=9,V>=1,V2>=2] * Chain [71,120,133]: 4 with precondition: [V1=2,Out=4,V>=1,V2>=2] * Chain [71,119,133]: 4 with precondition: [V1=2,Out=5,V>=1,V2>=2] * Chain [71,118,133]: 4 with precondition: [V1=2,Out=6,V>=1,V2>=2] * Chain [71,117,133]: 5 with precondition: [V1=2,Out=7,V>=1,V2>=2] * Chain [71,116,133]: 5 with precondition: [V1=2,Out=8,V>=1,V2>=2] * Chain [71,115,133]: 5 with precondition: [V1=2,Out=9,V>=1,V2>=2] * Chain [71,114,133]: 4 with precondition: [V1=2,Out=6,V>=1,V2>=2] * Chain [71,113,133]: 5 with precondition: [V1=2,Out=9,V>=1,V2>=2] * Chain [71,112,133]: 4 with precondition: [V1=2,Out=4,V>=1,V2>=2] * Chain [71,111,133]: 4 with precondition: [V1=2,Out=5,V>=1,V2>=2] * Chain [71,110,133]: 4 with precondition: [V1=2,Out=6,V>=1,V2>=2] * Chain [71,109,133]: 5 with precondition: [V1=2,Out=7,V>=1,V2>=2] * Chain [71,108,133]: 5 with precondition: [V1=2,Out=8,V>=1,V2>=2] * Chain [71,107,133]: 5 with precondition: [V1=2,Out=9,V>=1,V2>=2] * Chain [71,106,133]: 4 with precondition: [V1=2,V2=1,Out=4,V>=1] * Chain [71,105,133]: 4 with precondition: [V1=2,V2=1,Out=5,V>=1] * Chain [71,104,133]: 5 with precondition: [V1=2,V2=1,Out=7,V>=1] * Chain [71,97,133]: 4 with precondition: [V1=2,V2=1,Out=4,V>=1] * Chain [71,96,133]: 4 with precondition: [V1=2,V2=1,Out=5,V>=1] * Chain [71,95,133]: 5 with precondition: [V1=2,V2=1,Out=7,V>=1] * Chain [70,133]: 3 with precondition: [V1=2,Out=4,V>=1,V2>=1] * Chain [70,132,133]: 5 with precondition: [V1=2,Out=5,V>=1,V2>=1] * Chain [70,131,133]: 5 with precondition: [V1=2,Out=6,V>=1,V2>=1] * Chain [70,130,133]: 6 with precondition: [V1=2,V2=1,Out=7,V>=1] * Chain [70,129,133]: 6 with precondition: [V1=2,Out=8,V>=1,V2>=1] * Chain [70,128,133]: 6 with precondition: [V1=2,Out=9,V>=1,V2>=1] * Chain [70,127,133]: 5 with precondition: [V1=2,Out=5,V>=1,V2>=1] * Chain [70,126,133]: 5 with precondition: [V1=2,Out=6,V>=1,V2>=1] * Chain [70,125,133]: 6 with precondition: [V1=2,V2=1,Out=7,V>=1] * Chain [70,124,133]: 6 with precondition: [V1=2,Out=8,V>=1,V2>=1] * Chain [70,123,133]: 6 with precondition: [V1=2,Out=9,V>=1,V2>=1] * Chain [70,122,133]: 5 with precondition: [V1=2,Out=7,V>=1,V2>=2] * Chain [70,121,133]: 6 with precondition: [V1=2,Out=10,V>=1,V2>=2] * Chain [70,120,133]: 5 with precondition: [V1=2,Out=5,V>=1,V2>=2] * Chain [70,119,133]: 5 with precondition: [V1=2,Out=6,V>=1,V2>=2] * Chain [70,118,133]: 5 with precondition: [V1=2,Out=7,V>=1,V2>=2] * Chain [70,117,133]: 6 with precondition: [V1=2,Out=8,V>=1,V2>=2] * Chain [70,116,133]: 6 with precondition: [V1=2,Out=9,V>=1,V2>=2] * Chain [70,115,133]: 6 with precondition: [V1=2,Out=10,V>=1,V2>=2] * Chain [70,114,133]: 5 with precondition: [V1=2,Out=7,V>=1,V2>=2] * Chain [70,113,133]: 6 with precondition: [V1=2,Out=10,V>=1,V2>=2] * Chain [70,112,133]: 5 with precondition: [V1=2,Out=5,V>=1,V2>=2] * Chain [70,111,133]: 5 with precondition: [V1=2,Out=6,V>=1,V2>=2] * Chain [70,110,133]: 5 with precondition: [V1=2,Out=7,V>=1,V2>=2] * Chain [70,109,133]: 6 with precondition: [V1=2,Out=8,V>=1,V2>=2] * Chain [70,108,133]: 6 with precondition: [V1=2,Out=9,V>=1,V2>=2] * Chain [70,107,133]: 6 with precondition: [V1=2,Out=10,V>=1,V2>=2] * Chain [70,106,133]: 5 with precondition: [V1=2,V2=1,Out=5,V>=1] * Chain [70,105,133]: 5 with precondition: [V1=2,V2=1,Out=6,V>=1] * Chain [70,104,133]: 6 with precondition: [V1=2,V2=1,Out=8,V>=1] * Chain [70,97,133]: 5 with precondition: [V1=2,V2=1,Out=5,V>=1] * Chain [70,96,133]: 5 with precondition: [V1=2,V2=1,Out=6,V>=1] * Chain [70,95,133]: 6 with precondition: [V1=2,V2=1,Out=8,V>=1] * Chain [69,133]: 2 with precondition: [V1=2,Out=1,V>=1,V2>=1] * Chain [69,132,133]: 4 with precondition: [V1=2,Out=2,V>=1,V2>=1] * Chain [69,131,133]: 4 with precondition: [V1=2,V=1,Out=3,V2>=1] * Chain [69,130,133]: 5 with precondition: [V1=2,Out=4,V>=1,V2>=1] * Chain [69,129,133]: 5 with precondition: [V1=2,V=1,Out=5,V2>=1] * Chain [69,128,133]: 5 with precondition: [V1=2,V=1,Out=6,V2>=1] * Chain [69,127,133]: 4 with precondition: [V1=2,V=1,Out=2,V2>=1] * Chain [69,126,133]: 4 with precondition: [V1=2,V=1,Out=3,V2>=1] * Chain [69,125,133]: 5 with precondition: [V1=2,Out=4,V>=1,V2>=1] * Chain [69,124,133]: 5 with precondition: [V1=2,V=1,Out=5,V2>=1] * Chain [69,123,133]: 5 with precondition: [V1=2,V=1,Out=6,V2>=1] * Chain [69,106,133]: 4 with precondition: [V1=2,Out=2,V>=1,V2>=1] * Chain [69,105,133]: 4 with precondition: [V1=2,Out=3,V>=1,V2>=1] * Chain [69,104,133]: 5 with precondition: [V1=2,Out=5,V>=1,V2>=1] * Chain [69,103,133]: 5 with precondition: [V1=2,Out=6,V>=2,V2>=1] * Chain [69,102,133]: 4 with precondition: [V1=2,Out=2,V>=2,V2>=1] * Chain [69,101,133]: 4 with precondition: [V1=2,Out=3,V>=2,V2>=1] * Chain [69,100,133]: 5 with precondition: [V1=2,Out=4,V>=2,V2>=1] * Chain [69,99,133]: 5 with precondition: [V1=2,Out=5,V>=2,V2>=1] * Chain [69,98,133]: 5 with precondition: [V1=2,Out=6,V>=2,V2>=1] * Chain [69,97,133]: 4 with precondition: [V1=2,Out=2,V>=1,V2>=1] * Chain [69,96,133]: 4 with precondition: [V1=2,Out=3,V>=1,V2>=1] * Chain [69,95,133]: 5 with precondition: [V1=2,Out=5,V>=1,V2>=1] * Chain [69,94,133]: 5 with precondition: [V1=2,Out=6,V>=2,V2>=1] * Chain [69,93,133]: 4 with precondition: [V1=2,Out=2,V>=2,V2>=1] * Chain [69,92,133]: 4 with precondition: [V1=2,Out=3,V>=2,V2>=1] * Chain [69,91,133]: 5 with precondition: [V1=2,Out=4,V>=2,V2>=1] * Chain [69,90,133]: 5 with precondition: [V1=2,Out=5,V>=2,V2>=1] * Chain [69,89,133]: 5 with precondition: [V1=2,Out=6,V>=2,V2>=1] * Chain [69,87,133]: 4 with precondition: [V1=2,Out=4,V>=2,V2>=1] * Chain [68,133]: 3 with precondition: [V1=2,Out=2,V>=1,V2>=1] * Chain [68,132,133]: 5 with precondition: [V1=2,Out=3,V>=1,V2>=1] * Chain [68,131,133]: 5 with precondition: [V1=2,V=1,Out=4,V2>=1] * Chain [68,130,133]: 6 with precondition: [V1=2,Out=5,V>=1,V2>=1] * Chain [68,129,133]: 6 with precondition: [V1=2,V=1,Out=6,V2>=1] * Chain [68,128,133]: 6 with precondition: [V1=2,V=1,Out=7,V2>=1] * Chain [68,127,133]: 5 with precondition: [V1=2,V=1,Out=3,V2>=1] * Chain [68,126,133]: 5 with precondition: [V1=2,V=1,Out=4,V2>=1] * Chain [68,125,133]: 6 with precondition: [V1=2,Out=5,V>=1,V2>=1] * Chain [68,124,133]: 6 with precondition: [V1=2,V=1,Out=6,V2>=1] * Chain [68,123,133]: 6 with precondition: [V1=2,V=1,Out=7,V2>=1] * Chain [68,106,133]: 5 with precondition: [V1=2,Out=3,V>=1,V2>=1] * Chain [68,105,133]: 5 with precondition: [V1=2,Out=4,V>=1,V2>=1] * Chain [68,104,133]: 6 with precondition: [V1=2,Out=6,V>=1,V2>=1] * Chain [68,103,133]: 6 with precondition: [V1=2,Out=7,V>=2,V2>=1] * Chain [68,102,133]: 5 with precondition: [V1=2,Out=3,V>=2,V2>=1] * Chain [68,101,133]: 5 with precondition: [V1=2,Out=4,V>=2,V2>=1] * Chain [68,100,133]: 6 with precondition: [V1=2,Out=5,V>=2,V2>=1] * Chain [68,99,133]: 6 with precondition: [V1=2,Out=6,V>=2,V2>=1] * Chain [68,98,133]: 6 with precondition: [V1=2,Out=7,V>=2,V2>=1] * Chain [68,97,133]: 5 with precondition: [V1=2,Out=3,V>=1,V2>=1] * Chain [68,96,133]: 5 with precondition: [V1=2,Out=4,V>=1,V2>=1] * Chain [68,95,133]: 6 with precondition: [V1=2,Out=6,V>=1,V2>=1] * Chain [68,94,133]: 6 with precondition: [V1=2,Out=7,V>=2,V2>=1] * Chain [68,93,133]: 5 with precondition: [V1=2,Out=3,V>=2,V2>=1] * Chain [68,92,133]: 5 with precondition: [V1=2,Out=4,V>=2,V2>=1] * Chain [68,91,133]: 6 with precondition: [V1=2,Out=5,V>=2,V2>=1] * Chain [68,90,133]: 6 with precondition: [V1=2,Out=6,V>=2,V2>=1] * Chain [68,89,133]: 6 with precondition: [V1=2,Out=7,V>=2,V2>=1] * Chain [68,87,133]: 5 with precondition: [V1=2,Out=5,V>=2,V2>=1] * Chain [67,133]: 2 with precondition: [V1=2,Out=3,V>=1,V2>=1] * Chain [67,132,133]: 4 with precondition: [V1=2,Out=4,V>=1,V2>=1] * Chain [67,131,133]: 4 with precondition: [V1=2,V=1,Out=5,V2>=1] * Chain [67,130,133]: 5 with precondition: [V1=2,Out=6,V>=1,V2>=1] * Chain [67,129,133]: 5 with precondition: [V1=2,V=1,Out=7,V2>=1] * Chain [67,128,133]: 5 with precondition: [V1=2,V=1,Out=8,V2>=1] * Chain [67,127,133]: 4 with precondition: [V1=2,V=1,Out=4,V2>=1] * Chain [67,126,133]: 4 with precondition: [V1=2,V=1,Out=5,V2>=1] * Chain [67,125,133]: 5 with precondition: [V1=2,Out=6,V>=1,V2>=1] * Chain [67,124,133]: 5 with precondition: [V1=2,V=1,Out=7,V2>=1] * Chain [67,123,133]: 5 with precondition: [V1=2,V=1,Out=8,V2>=1] * Chain [67,106,133]: 4 with precondition: [V1=2,Out=4,V>=1,V2>=1] * Chain [67,105,133]: 4 with precondition: [V1=2,Out=5,V>=1,V2>=1] * Chain [67,104,133]: 5 with precondition: [V1=2,Out=7,V>=1,V2>=1] * Chain [67,103,133]: 5 with precondition: [V1=2,Out=8,V>=2,V2>=1] * Chain [67,102,133]: 4 with precondition: [V1=2,Out=4,V>=2,V2>=1] * Chain [67,101,133]: 4 with precondition: [V1=2,Out=5,V>=2,V2>=1] * Chain [67,100,133]: 5 with precondition: [V1=2,Out=6,V>=2,V2>=1] * Chain [67,99,133]: 5 with precondition: [V1=2,Out=7,V>=2,V2>=1] * Chain [67,98,133]: 5 with precondition: [V1=2,Out=8,V>=2,V2>=1] * Chain [67,97,133]: 4 with precondition: [V1=2,Out=4,V>=1,V2>=1] * Chain [67,96,133]: 4 with precondition: [V1=2,Out=5,V>=1,V2>=1] * Chain [67,95,133]: 5 with precondition: [V1=2,Out=7,V>=1,V2>=1] * Chain [67,94,133]: 5 with precondition: [V1=2,Out=8,V>=2,V2>=1] * Chain [67,93,133]: 4 with precondition: [V1=2,Out=4,V>=2,V2>=1] * Chain [67,92,133]: 4 with precondition: [V1=2,Out=5,V>=2,V2>=1] * Chain [67,91,133]: 5 with precondition: [V1=2,Out=6,V>=2,V2>=1] * Chain [67,90,133]: 5 with precondition: [V1=2,Out=7,V>=2,V2>=1] * Chain [67,89,133]: 5 with precondition: [V1=2,Out=8,V>=2,V2>=1] * Chain [67,87,133]: 4 with precondition: [V1=2,Out=6,V>=2,V2>=1] * Chain [66,133]: 3 with precondition: [V1=2,Out=4,V>=1,V2>=1] * Chain [66,132,133]: 5 with precondition: [V1=2,Out=5,V>=1,V2>=1] * Chain [66,131,133]: 5 with precondition: [V1=2,V=1,Out=6,V2>=1] * Chain [66,130,133]: 6 with precondition: [V1=2,Out=7,V>=1,V2>=1] * Chain [66,129,133]: 6 with precondition: [V1=2,V=1,Out=8,V2>=1] * Chain [66,128,133]: 6 with precondition: [V1=2,V=1,Out=9,V2>=1] * Chain [66,127,133]: 5 with precondition: [V1=2,V=1,Out=5,V2>=1] * Chain [66,126,133]: 5 with precondition: [V1=2,V=1,Out=6,V2>=1] * Chain [66,125,133]: 6 with precondition: [V1=2,Out=7,V>=1,V2>=1] * Chain [66,124,133]: 6 with precondition: [V1=2,V=1,Out=8,V2>=1] * Chain [66,123,133]: 6 with precondition: [V1=2,V=1,Out=9,V2>=1] * Chain [66,106,133]: 5 with precondition: [V1=2,Out=5,V>=1,V2>=1] * Chain [66,105,133]: 5 with precondition: [V1=2,Out=6,V>=1,V2>=1] * Chain [66,104,133]: 6 with precondition: [V1=2,Out=8,V>=1,V2>=1] * Chain [66,103,133]: 6 with precondition: [V1=2,Out=9,V>=2,V2>=1] * Chain [66,102,133]: 5 with precondition: [V1=2,Out=5,V>=2,V2>=1] * Chain [66,101,133]: 5 with precondition: [V1=2,Out=6,V>=2,V2>=1] * Chain [66,100,133]: 6 with precondition: [V1=2,Out=7,V>=2,V2>=1] * Chain [66,99,133]: 6 with precondition: [V1=2,Out=8,V>=2,V2>=1] * Chain [66,98,133]: 6 with precondition: [V1=2,Out=9,V>=2,V2>=1] * Chain [66,97,133]: 5 with precondition: [V1=2,Out=5,V>=1,V2>=1] * Chain [66,96,133]: 5 with precondition: [V1=2,Out=6,V>=1,V2>=1] * Chain [66,95,133]: 6 with precondition: [V1=2,Out=8,V>=1,V2>=1] * Chain [66,94,133]: 6 with precondition: [V1=2,Out=9,V>=2,V2>=1] * Chain [66,93,133]: 5 with precondition: [V1=2,Out=5,V>=2,V2>=1] * Chain [66,92,133]: 5 with precondition: [V1=2,Out=6,V>=2,V2>=1] * Chain [66,91,133]: 6 with precondition: [V1=2,Out=7,V>=2,V2>=1] * Chain [66,90,133]: 6 with precondition: [V1=2,Out=8,V>=2,V2>=1] * Chain [66,89,133]: 6 with precondition: [V1=2,Out=9,V>=2,V2>=1] * Chain [66,87,133]: 5 with precondition: [V1=2,Out=7,V>=2,V2>=1] #### Cost of chains of start(V1,V,V2): * Chain [141]: 1*s(1129)+1*s(1130)+1*s(1131)+1 Such that:s(1129) =< V1+1 s(1131) =< V s(1130) =< V+2 with precondition: [V1>=0] * Chain [140]: 1 with precondition: [V1=1,V>=0] * Chain [139]: 3760*s(1134)+6 Such that:aux(693) =< V aux(694) =< V2 s(1134) =< aux(693) s(1134) =< aux(694) with precondition: [V1=2,V>=0,V2>=0] * Chain [138]: 1 with precondition: [V=1,V1>=0] * Chain [137]: 1 with precondition: [V1=2,V=2] * Chain [136]: 3 with precondition: [V1=2,V2=0,V>=0] * Chain [135]: 6 with precondition: [V1=2,V2=1,V>=1] * Chain [134]: 1 with precondition: [V=0,V1>=1] Closed-form bounds of start(V1,V,V2): ------------------------------------- * Chain [141] with precondition: [V1>=0] - Upper bound: nat(V)+1+(V1+1)+nat(V+2) - Complexity: n * Chain [140] with precondition: [V1=1,V>=0] - Upper bound: 1 - Complexity: constant * Chain [139] with precondition: [V1=2,V>=0,V2>=0] - Upper bound: 3760*V+6 - Complexity: n * Chain [138] with precondition: [V=1,V1>=0] - Upper bound: 1 - Complexity: constant * Chain [137] with precondition: [V1=2,V=2] - Upper bound: 1 - Complexity: constant * Chain [136] with precondition: [V1=2,V2=0,V>=0] - Upper bound: 3 - Complexity: constant * Chain [135] with precondition: [V1=2,V2=1,V>=1] - Upper bound: 6 - Complexity: constant * Chain [134] with precondition: [V=0,V1>=1] - Upper bound: 1 - Complexity: constant ### Maximum cost of start(V1,V,V2): max([5,nat(V)+max([nat(V)*3759+5,V1+1+nat(V+2)])])+1 Asymptotic class: n * Total analysis performed in 28384 ms. ---------------------------------------- (12) BOUNDS(1, n^1) ---------------------------------------- (13) RelTrsToDecreasingLoopProblemProof (LOWER BOUND(ID)) Transformed a relative TRS into a decreasing-loop problem. ---------------------------------------- (14) Obligation: Analyzing the following TRS for decreasing loops: The Runtime Complexity (innermost) of the given CpxRelTRS could be proven to be BOUNDS(n^1, n^1). The TRS R consists of the following rules: COND(true, z0, z1) -> c(COND(and(gr(z0, 0), gr(z1, 0)), p(z0), p(z1)), AND(gr(z0, 0), gr(z1, 0)), GR(z0, 0)) COND(true, z0, z1) -> c1(COND(and(gr(z0, 0), gr(z1, 0)), p(z0), p(z1)), AND(gr(z0, 0), gr(z1, 0)), GR(z1, 0)) COND(true, z0, z1) -> c2(COND(and(gr(z0, 0), gr(z1, 0)), p(z0), p(z1)), P(z0)) COND(true, z0, z1) -> c3(COND(and(gr(z0, 0), gr(z1, 0)), p(z0), p(z1)), 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 The (relative) TRS S consists of the following rules: cond(true, z0, z1) -> cond(and(gr(z0, 0), gr(z1, 0)), p(z0), p(z1)) 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 ---------------------------------------- (15) DecreasingLoopProof (LOWER BOUND(ID)) The following loop(s) give(s) rise to the lower bound Omega(n^1): The rewrite sequence GR(s(z0), s(z1)) ->^+ c10(GR(z0, z1)) gives rise to a decreasing loop by considering the right hand sides subterm at position [0]. The pumping substitution is [z0 / s(z0), z1 / s(z1)]. The result substitution is [ ]. ---------------------------------------- (16) Complex Obligation (BEST) ---------------------------------------- (17) Obligation: Proved the lower bound n^1 for the following obligation: The Runtime Complexity (innermost) of the given CpxRelTRS could be proven to be BOUNDS(n^1, n^1). The TRS R consists of the following rules: COND(true, z0, z1) -> c(COND(and(gr(z0, 0), gr(z1, 0)), p(z0), p(z1)), AND(gr(z0, 0), gr(z1, 0)), GR(z0, 0)) COND(true, z0, z1) -> c1(COND(and(gr(z0, 0), gr(z1, 0)), p(z0), p(z1)), AND(gr(z0, 0), gr(z1, 0)), GR(z1, 0)) COND(true, z0, z1) -> c2(COND(and(gr(z0, 0), gr(z1, 0)), p(z0), p(z1)), P(z0)) COND(true, z0, z1) -> c3(COND(and(gr(z0, 0), gr(z1, 0)), p(z0), p(z1)), 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 The (relative) TRS S consists of the following rules: cond(true, z0, z1) -> cond(and(gr(z0, 0), gr(z1, 0)), p(z0), p(z1)) 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 ---------------------------------------- (18) LowerBoundPropagationProof (FINISHED) Propagated lower bound. ---------------------------------------- (19) BOUNDS(n^1, INF) ---------------------------------------- (20) Obligation: Analyzing the following TRS for decreasing loops: The Runtime Complexity (innermost) of the given CpxRelTRS could be proven to be BOUNDS(n^1, n^1). The TRS R consists of the following rules: COND(true, z0, z1) -> c(COND(and(gr(z0, 0), gr(z1, 0)), p(z0), p(z1)), AND(gr(z0, 0), gr(z1, 0)), GR(z0, 0)) COND(true, z0, z1) -> c1(COND(and(gr(z0, 0), gr(z1, 0)), p(z0), p(z1)), AND(gr(z0, 0), gr(z1, 0)), GR(z1, 0)) COND(true, z0, z1) -> c2(COND(and(gr(z0, 0), gr(z1, 0)), p(z0), p(z1)), P(z0)) COND(true, z0, z1) -> c3(COND(and(gr(z0, 0), gr(z1, 0)), p(z0), p(z1)), 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 The (relative) TRS S consists of the following rules: cond(true, z0, z1) -> cond(and(gr(z0, 0), gr(z1, 0)), p(z0), p(z1)) 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