WORST_CASE(Omega(n^1),O(n^2)) proof of /export/starexec/sandbox/benchmark/theBenchmark.trs # AProVE Commit ID: c69e44bd14796315568835c1ffa2502984884775 mhark 20210624 unpublished The Runtime Complexity (innermost) of the given CpxRelTRS could be proven to be BOUNDS(n^1, n^2). (0) CpxRelTRS (1) SInnermostTerminationProof [BOTH CONCRETE BOUNDS(ID, ID), 511 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, 14.9 s] (12) BOUNDS(1, n^2) (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^2). The TRS R consists of the following rules: COND(true, z0) -> c(COND(odd(z0), p(p(p(z0)))), ODD(z0)) COND(true, z0) -> c1(COND(odd(z0), p(p(p(z0)))), P(p(p(z0))), P(p(z0)), P(z0)) ODD(0) -> c2 ODD(s(0)) -> c3 ODD(s(s(z0))) -> c4(ODD(z0)) P(0) -> c5 P(s(z0)) -> c6 The (relative) TRS S consists of the following rules: cond(true, z0) -> cond(odd(z0), p(p(p(z0)))) odd(0) -> false odd(s(0)) -> true odd(s(s(z0))) -> odd(z0) 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^2). The TRS R consists of the following rules: COND(true, z0) -> c(COND(odd(z0), p(p(p(z0)))), ODD(z0)) COND(true, z0) -> c1(COND(odd(z0), p(p(p(z0)))), P(p(p(z0))), P(p(z0)), P(z0)) ODD(0) -> c2 ODD(s(0)) -> c3 ODD(s(s(z0))) -> c4(ODD(z0)) P(0) -> c5 P(s(z0)) -> c6 The (relative) TRS S consists of the following rules: cond(true, z0) -> cond(odd(z0), p(p(p(z0)))) odd(0) -> false odd(s(0)) -> true odd(s(s(z0))) -> odd(z0) 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^2). The TRS R consists of the following rules: COND(true, z0) -> c(COND(odd(z0), p(p(p(z0)))), ODD(z0)) [1] COND(true, z0) -> c1(COND(odd(z0), p(p(p(z0)))), P(p(p(z0))), P(p(z0)), P(z0)) [1] ODD(0) -> c2 [1] ODD(s(0)) -> c3 [1] ODD(s(s(z0))) -> c4(ODD(z0)) [1] P(0) -> c5 [1] P(s(z0)) -> c6 [1] cond(true, z0) -> cond(odd(z0), p(p(p(z0)))) [0] odd(0) -> false [0] odd(s(0)) -> true [0] odd(s(s(z0))) -> odd(z0) [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) -> c(COND(odd(z0), p(p(p(z0)))), ODD(z0)) [1] COND(true, z0) -> c1(COND(odd(z0), p(p(p(z0)))), P(p(p(z0))), P(p(z0)), P(z0)) [1] ODD(0) -> c2 [1] ODD(s(0)) -> c3 [1] ODD(s(s(z0))) -> c4(ODD(z0)) [1] P(0) -> c5 [1] P(s(z0)) -> c6 [1] cond(true, z0) -> cond(odd(z0), p(p(p(z0)))) [0] odd(0) -> false [0] odd(s(0)) -> true [0] odd(s(s(z0))) -> odd(z0) [0] p(0) -> 0 [0] p(s(z0)) -> z0 [0] The TRS has the following type information: COND :: true:false -> 0:s -> c:c1 true :: true:false c :: c:c1 -> c2:c3:c4 -> c:c1 odd :: 0:s -> true:false p :: 0:s -> 0:s ODD :: 0:s -> c2:c3:c4 c1 :: c:c1 -> c5:c6 -> c5:c6 -> c5:c6 -> c:c1 P :: 0:s -> c5:c6 0 :: 0:s c2 :: c2:c3:c4 s :: 0:s -> 0:s c3 :: c2:c3:c4 c4 :: c2:c3:c4 -> c2:c3:c4 c5 :: c5:c6 c6 :: c5:c6 cond :: true:false -> 0:s -> cond false :: true:false 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) -> null_cond [0] odd(v0) -> null_odd [0] p(v0) -> null_p [0] COND(v0, v1) -> null_COND [0] ODD(v0) -> null_ODD [0] P(v0) -> null_P [0] And the following fresh constants: null_cond, null_odd, null_p, null_COND, null_ODD, 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) -> c(COND(odd(z0), p(p(p(z0)))), ODD(z0)) [1] COND(true, z0) -> c1(COND(odd(z0), p(p(p(z0)))), P(p(p(z0))), P(p(z0)), P(z0)) [1] ODD(0) -> c2 [1] ODD(s(0)) -> c3 [1] ODD(s(s(z0))) -> c4(ODD(z0)) [1] P(0) -> c5 [1] P(s(z0)) -> c6 [1] cond(true, z0) -> cond(odd(z0), p(p(p(z0)))) [0] odd(0) -> false [0] odd(s(0)) -> true [0] odd(s(s(z0))) -> odd(z0) [0] p(0) -> 0 [0] p(s(z0)) -> z0 [0] cond(v0, v1) -> null_cond [0] odd(v0) -> null_odd [0] p(v0) -> null_p [0] COND(v0, v1) -> null_COND [0] ODD(v0) -> null_ODD [0] P(v0) -> null_P [0] The TRS has the following type information: COND :: true:false:null_odd -> 0:s:null_p -> c:c1:null_COND true :: true:false:null_odd c :: c:c1:null_COND -> c2:c3:c4:null_ODD -> c:c1:null_COND odd :: 0:s:null_p -> true:false:null_odd p :: 0:s:null_p -> 0:s:null_p ODD :: 0:s:null_p -> c2:c3:c4:null_ODD c1 :: c:c1:null_COND -> c5:c6:null_P -> c5:c6:null_P -> c5:c6:null_P -> c:c1:null_COND P :: 0:s:null_p -> c5:c6:null_P 0 :: 0:s:null_p c2 :: c2:c3:c4:null_ODD s :: 0:s:null_p -> 0:s:null_p c3 :: c2:c3:c4:null_ODD c4 :: c2:c3:c4:null_ODD -> c2:c3:c4:null_ODD c5 :: c5:c6:null_P c6 :: c5:c6:null_P cond :: true:false:null_odd -> 0:s:null_p -> null_cond false :: true:false:null_odd null_cond :: null_cond null_odd :: true:false:null_odd null_p :: 0:s:null_p null_COND :: c:c1:null_COND null_ODD :: c2:c3:c4:null_ODD null_P :: c5:c6: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 c2 => 0 c3 => 1 c5 => 1 c6 => 2 false => 1 null_cond => 0 null_odd => 0 null_p => 0 null_COND => 0 null_ODD => 0 null_P => 0 ---------------------------------------- (10) Obligation: Complexity RNTS consisting of the following rules: COND(z, z') -{ 0 }-> 0 :|: v0 >= 0, v1 >= 0, z = v0, z' = v1 COND(z, z') -{ 1 }-> 1 + COND(odd(z0), p(p(p(z0)))) + ODD(z0) :|: z = 2, z0 >= 0, z' = z0 COND(z, z') -{ 1 }-> 1 + COND(odd(z0), p(p(p(z0)))) + P(p(p(z0))) + P(p(z0)) + P(z0) :|: z = 2, z0 >= 0, z' = z0 ODD(z) -{ 1 }-> 1 :|: z = 1 + 0 ODD(z) -{ 1 }-> 0 :|: z = 0 ODD(z) -{ 0 }-> 0 :|: v0 >= 0, z = v0 ODD(z) -{ 1 }-> 1 + ODD(z0) :|: z0 >= 0, z = 1 + (1 + z0) P(z) -{ 1 }-> 2 :|: z = 1 + z0, z0 >= 0 P(z) -{ 1 }-> 1 :|: z = 0 P(z) -{ 0 }-> 0 :|: v0 >= 0, z = v0 cond(z, z') -{ 0 }-> cond(odd(z0), p(p(p(z0)))) :|: z = 2, z0 >= 0, z' = z0 cond(z, z') -{ 0 }-> 0 :|: v0 >= 0, v1 >= 0, z = v0, z' = v1 odd(z) -{ 0 }-> odd(z0) :|: z0 >= 0, z = 1 + (1 + z0) odd(z) -{ 0 }-> 2 :|: z = 1 + 0 odd(z) -{ 0 }-> 1 :|: z = 0 odd(z) -{ 0 }-> 0 :|: v0 >= 0, z = v0 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),0,[fun(V1, V, Out)],[V1 >= 0,V >= 0]). eq(start(V1, V),0,[fun1(V1, Out)],[V1 >= 0]). eq(start(V1, V),0,[fun2(V1, Out)],[V1 >= 0]). eq(start(V1, V),0,[cond(V1, V, Out)],[V1 >= 0,V >= 0]). eq(start(V1, V),0,[odd(V1, Out)],[V1 >= 0]). eq(start(V1, V),0,[p(V1, Out)],[V1 >= 0]). eq(fun(V1, V, Out),1,[odd(V2, Ret010),p(V2, Ret01100),p(Ret01100, Ret0110),p(Ret0110, Ret011),fun(Ret010, Ret011, Ret01),fun1(V2, Ret1)],[Out = 1 + Ret01 + Ret1,V1 = 2,V2 >= 0,V = V2]). eq(fun(V1, V, Out),1,[odd(V3, Ret00010),p(V3, Ret0001100),p(Ret0001100, Ret000110),p(Ret000110, Ret00011),fun(Ret00010, Ret00011, Ret0001),p(V3, Ret00100),p(Ret00100, Ret0010),fun2(Ret0010, Ret001),p(V3, Ret0101),fun2(Ret0101, Ret012),fun2(V3, Ret11)],[Out = 1 + Ret0001 + Ret001 + Ret012 + Ret11,V1 = 2,V3 >= 0,V = V3]). eq(fun1(V1, Out),1,[],[Out = 0,V1 = 0]). eq(fun1(V1, Out),1,[],[Out = 1,V1 = 1]). eq(fun1(V1, Out),1,[fun1(V4, Ret12)],[Out = 1 + Ret12,V4 >= 0,V1 = 2 + V4]). eq(fun2(V1, Out),1,[],[Out = 1,V1 = 0]). eq(fun2(V1, Out),1,[],[Out = 2,V1 = 1 + V5,V5 >= 0]). eq(cond(V1, V, Out),0,[odd(V6, Ret0),p(V6, Ret100),p(Ret100, Ret10),p(Ret10, Ret13),cond(Ret0, Ret13, Ret)],[Out = Ret,V1 = 2,V6 >= 0,V = V6]). eq(odd(V1, Out),0,[],[Out = 1,V1 = 0]). eq(odd(V1, Out),0,[],[Out = 2,V1 = 1]). eq(odd(V1, Out),0,[odd(V7, Ret2)],[Out = Ret2,V7 >= 0,V1 = 2 + V7]). eq(p(V1, Out),0,[],[Out = 0,V1 = 0]). eq(p(V1, Out),0,[],[Out = V8,V1 = 1 + V8,V8 >= 0]). eq(cond(V1, V, Out),0,[],[Out = 0,V10 >= 0,V9 >= 0,V1 = V10,V = V9]). eq(odd(V1, Out),0,[],[Out = 0,V11 >= 0,V1 = V11]). eq(p(V1, Out),0,[],[Out = 0,V12 >= 0,V1 = V12]). eq(fun(V1, V, Out),0,[],[Out = 0,V13 >= 0,V14 >= 0,V1 = V13,V = V14]). eq(fun1(V1, Out),0,[],[Out = 0,V15 >= 0,V1 = V15]). eq(fun2(V1, Out),0,[],[Out = 0,V16 >= 0,V1 = V16]). input_output_vars(fun(V1,V,Out),[V1,V],[Out]). input_output_vars(fun1(V1,Out),[V1],[Out]). input_output_vars(fun2(V1,Out),[V1],[Out]). input_output_vars(cond(V1,V,Out),[V1,V],[Out]). input_output_vars(odd(V1,Out),[V1],[Out]). input_output_vars(p(V1,Out),[V1],[Out]). CoFloCo proof output: Preprocessing Cost Relations ===================================== #### Computed strongly connected components 0. recursive : [odd/2] 1. non_recursive : [p/2] 2. recursive : [cond/3] 3. recursive : [fun1/2] 4. non_recursive : [fun2/2] 5. recursive [non_tail] : [fun/3] 6. non_recursive : [start/2] #### Obtained direct recursion through partial evaluation 0. SCC is partially evaluated into odd/2 1. SCC is partially evaluated into p/2 2. SCC is partially evaluated into cond/3 3. SCC is partially evaluated into fun1/2 4. SCC is partially evaluated into fun2/2 5. SCC is partially evaluated into fun/3 6. SCC is partially evaluated into start/2 Control-Flow Refinement of Cost Relations ===================================== ### Specialization of cost equations odd/2 * CE 22 is refined into CE [25] * CE 20 is refined into CE [26] * CE 19 is refined into CE [27] * CE 21 is refined into CE [28] ### Cost equations --> "Loop" of odd/2 * CEs [28] --> Loop 18 * CEs [25] --> Loop 19 * CEs [26] --> Loop 20 * CEs [27] --> Loop 21 ### Ranking functions of CR odd(V1,Out) * RF of phase [18]: [V1-1] #### Partial ranking functions of CR odd(V1,Out) * Partial RF of phase [18]: - RF of loop [18:1]: V1-1 ### Specialization of cost equations p/2 * CE 24 is refined into CE [29] * CE 23 is refined into CE [30] ### Cost equations --> "Loop" of p/2 * CEs [29] --> Loop 22 * CEs [30] --> Loop 23 ### Ranking functions of CR p(V1,Out) #### Partial ranking functions of CR p(V1,Out) ### Specialization of cost equations cond/3 * CE 18 is refined into CE [31] * CE 17 is refined into CE [32,33,34,35,36,37,38,39,40,41,42,43,44,45,46] ### Cost equations --> "Loop" of cond/3 * CEs [46] --> Loop 24 * CEs [43,44,45] --> Loop 25 * CEs [42] --> Loop 26 * CEs [39,40,41] --> Loop 27 * CEs [38] --> Loop 28 * CEs [35,36,37] --> Loop 29 * CEs [33,34] --> Loop 30 * CEs [32] --> Loop 31 * CEs [31] --> Loop 32 ### Ranking functions of CR cond(V1,V,Out) * RF of phase [24]: [V/3-2/3] #### Partial ranking functions of CR cond(V1,V,Out) * Partial RF of phase [24]: - RF of loop [24:1]: V/3-2/3 ### Specialization of cost equations fun1/2 * CE 11 is refined into CE [47] * CE 10 is refined into CE [48] * CE 13 is refined into CE [49] * CE 12 is refined into CE [50] ### Cost equations --> "Loop" of fun1/2 * CEs [50] --> Loop 33 * CEs [47] --> Loop 34 * CEs [48,49] --> Loop 35 ### Ranking functions of CR fun1(V1,Out) * RF of phase [33]: [V1-1] #### Partial ranking functions of CR fun1(V1,Out) * Partial RF of phase [33]: - RF of loop [33:1]: V1-1 ### Specialization of cost equations fun2/2 * CE 15 is refined into CE [51] * CE 16 is refined into CE [52] * CE 14 is refined into CE [53] ### Cost equations --> "Loop" of fun2/2 * CEs [51] --> Loop 36 * CEs [52] --> Loop 37 * CEs [53] --> Loop 38 ### Ranking functions of CR fun2(V1,Out) #### Partial ranking functions of CR fun2(V1,Out) ### Specialization of cost equations fun/3 * CE 9 is refined into CE [54] * CE 7 is refined into CE [55,56,57,58,59,60,61,62,63,64,65,66,67,68,69,70,71,72,73,74,75,76,77,78,79,80,81,82,83,84,85,86,87,88,89,90,91,92,93,94,95,96,97] * CE 8 is refined into CE [98,99,100,101,102,103,104,105,106,107,108,109,110,111,112,113,114,115,116,117,118,119,120,121,122,123,124,125,126,127,128,129,130,131,132,133,134,135,136,137,138,139,140,141,142,143,144,145,146,147,148,149,150,151,152,153,154,155,156,157,158,159,160,161,162,163,164,165,166,167,168,169,170,171,172,173,174,175,176,177,178,179,180,181,182,183,184,185,186,187,188,189,190,191,192,193,194,195,196,197,198,199,200,201,202,203,204,205,206,207,208,209,210,211,212,213,214,215,216,217,218,219,220,221,222,223,224,225,226,227,228,229,230,231,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,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] ### Cost equations --> "Loop" of fun/3 * CEs [96] --> Loop 39 * CEs [813] --> Loop 40 * CEs [773,789,807] --> Loop 41 * CEs [767,781,783,797,805,809,811,812] --> Loop 42 * CEs [769,771,772,775,785,787,788,791,799,806] --> Loop 43 * CEs [766,777,779,780,782,793,795,796,801,803,804,808,810] --> Loop 44 * CEs [97,768,770,774,784,786,790,798] --> Loop 45 * CEs [95,776,778,792,794,800,802] --> Loop 46 * CEs [87,90,93] --> Loop 47 * CEs [669,717,765] --> Loop 48 * CEs [629,645,663,677,693,711,725,741,759] --> Loop 49 * CEs [623,637,639,653,661,665,667,668,671,685,687,701,709,713,715,716,719,733,735,749,757,761,763,764] --> Loop 50 * CEs [625,627,628,631,641,643,644,647,655,662,673,675,676,679,689,691,692,695,703,710,721,723,724,727,737,739,740,743,751,758] --> Loop 51 * CEs [622,633,635,636,638,649,651,652,657,659,660,664,666,670,681,683,684,686,697,699,700,705,707,708,712,714,718,729,731,732,734,745,747,748,753,755,756,760,762] --> Loop 52 * CEs [88,91,94,624,626,630,640,642,646,654,672,674,678,688,690,694,702,720,722,726,736,738,742,750] --> Loop 53 * CEs [86,89,92,632,634,648,650,656,658,680,682,696,698,704,706,728,730,744,746,752,754] --> Loop 54 * CEs [84] --> Loop 55 * CEs [621] --> Loop 56 * CEs [581,597,615] --> Loop 57 * CEs [575,589,591,605,613,617,619,620] --> Loop 58 * CEs [577,579,580,583,593,595,596,599,607,614] --> Loop 59 * CEs [574,585,587,588,590,601,603,604,609,611,612,616,618] --> Loop 60 * CEs [85,576,578,582,592,594,598,606] --> Loop 61 * CEs [83,584,586,600,602,608,610] --> Loop 62 * CEs [75,78,81] --> Loop 63 * CEs [461,517,573] --> Loop 64 * CEs [74,77,80,416,418,432,434,448,450,472,474,488,490,504,506,528,530,544,546,560,562] --> Loop 65 * CEs [72] --> Loop 66 * CEs [405] --> Loop 67 * CEs [365,381,399] --> Loop 68 * CEs [359,373,375,389,397,401,403,404] --> Loop 69 * CEs [361,363,364,367,377,379,380,383,391,398] --> Loop 70 * CEs [358,369,371,372,374,385,387,388,393,395,396,400,402] --> Loop 71 * CEs [73,360,362,366,376,378,382,390] --> Loop 72 * CEs [71,368,370,384,386,392,394] --> Loop 73 * CEs [62,66,69] --> Loop 74 * CEs [237,301,357] --> Loop 75 * CEs [61,65,68,186,190,206,210,224,226,250,254,270,274,288,290,312,314,328,330,344,346] --> Loop 76 * CEs [413,429,445,455,469,485,501,511,525,541,557,567] --> Loop 77 * CEs [407,421,423,437,439,453,457,459,460,463,477,479,493,495,509,513,515,516,519,533,535,549,551,565,569,571,572] --> Loop 78 * CEs [409,411,412,415,425,427,428,431,441,443,444,447,454,465,467,468,471,481,483,484,487,497,499,500,503,510,521,523,524,527,537,539,540,543,553,555,556,559,566] --> Loop 79 * CEs [406,417,419,420,422,433,435,436,438,449,451,452,456,458,462,473,475,476,478,489,491,492,494,505,507,508,512,514,518,529,531,532,534,545,547,548,550,561,563,564,568,570] --> Loop 80 * CEs [76,79,82,408,410,414,424,426,430,440,442,446,464,466,470,480,482,486,496,498,502,520,522,526,536,538,542,552,554,558] --> Loop 81 * CEs [181,203,221,231,247,267,285,295,309,325,341,351] --> Loop 82 * CEs [215,279,335] --> Loop 83 * CEs [217,219,220,281,283,284,337,339,340] --> Loop 84 * CEs [214,278,334] --> Loop 85 * CEs [63,67,70,216,218,280,282,336,338] --> Loop 86 * CEs [107,111,123,127,139,143,155,159] --> Loop 87 * CEs [109,113,115,119,125,129,131,135,141,145,147,151,157,161,163,167] --> Loop 88 * CEs [106,110,117,121,122,126,133,137,138,142,149,153,154,158,165,169] --> Loop 89 * CEs [56,58,108,112,114,118,124,128,130,134,140,144,146,150,156,160,162,166] --> Loop 90 * CEs [57,59,116,120,132,136,148,152,164,168] --> Loop 91 * CEs [172,177,193,195,199,213,229,233,235,236,239,243,257,259,263,277,293,297,299,300,303,317,319,333,349,353,355,356] --> Loop 92 * CEs [175,179,180,184,189,197,201,202,205,209,223,230,241,245,246,249,253,261,265,266,269,273,287,294,305,307,308,311,321,323,324,327,343,350] --> Loop 93 * CEs [176,198,242,262] --> Loop 94 * CEs [60,64,188,208,252,272] --> Loop 95 * CEs [98] --> Loop 96 * CEs [99,100,102] --> Loop 97 * CEs [101,103,104] --> Loop 98 * CEs [55,105] --> Loop 99 * CEs [170] --> Loop 100 * CEs [171,173,182,187,191,192,194,207,211,212,225,227,228,232,234,238,251,255,256,258,271,275,276,289,291,292,296,298,302,313,315,316,318,329,331,332,345,347,348,352,354] --> Loop 101 * CEs [174,178,183,185,196,200,204,222,240,244,248,260,264,268,286,304,306,310,320,322,326,342] --> Loop 102 * CEs [54] --> Loop 103 ### Ranking functions of CR fun(V1,V,Out) * RF of phase [39,40,41,42,43,44,45,46]: [V/3-2/3] #### Partial ranking functions of CR fun(V1,V,Out) * Partial RF of phase [39,40,41,42,43,44,45,46]: - RF of loop [39:1,40:1,41:1,42:1,43:1,44:1,45:1,46:1]: V/3-2/3 ### Specialization of cost equations start/2 * CE 1 is refined into CE [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] * CE 2 is refined into CE [843,844,845,846] * CE 3 is refined into CE [847,848,849] * CE 4 is refined into CE [850,851] * CE 5 is refined into CE [852,853,854,855,856] * CE 6 is refined into CE [857,858] ### Cost equations --> "Loop" of start/2 * CEs [827,828,829] --> Loop 104 * CEs [818,819,820,823,824,825,826,851] --> Loop 105 * CEs [814,815,816,817,821,822,830,831,832,833,834,835,836,837,838,839,840,841] --> Loop 106 * CEs [843,853] --> Loop 107 * CEs [842,844,845,846,847,848,849,850,852,854,855,856,857,858] --> Loop 108 ### Ranking functions of CR start(V1,V) #### Partial ranking functions of CR start(V1,V) Computing Bounds ===================================== #### Cost of chains of odd(V1,Out): * Chain [[18],21]: 0 with precondition: [Out=1,V1>=2] * Chain [[18],20]: 0 with precondition: [Out=2,V1>=3] * Chain [[18],19]: 0 with precondition: [Out=0,V1>=2] * Chain [21]: 0 with precondition: [V1=0,Out=1] * Chain [20]: 0 with precondition: [V1=1,Out=2] * Chain [19]: 0 with precondition: [Out=0,V1>=0] #### Cost of chains of p(V1,Out): * Chain [23]: 0 with precondition: [Out=0,V1>=0] * Chain [22]: 0 with precondition: [V1=Out+1,V1>=1] #### Cost of chains of cond(V1,V,Out): * Chain [[24],32]: 0 with precondition: [V1=2,Out=0,V>=3] * Chain [[24],31,32]: 0 with precondition: [V1=2,Out=0,V>=3] * Chain [[24],30,32]: 0 with precondition: [V1=2,Out=0,V>=4] * Chain [[24],30,31,32]: 0 with precondition: [V1=2,Out=0,V>=4] * Chain [[24],30,29,32]: 0 with precondition: [V1=2,Out=0,V>=4] * Chain [[24],29,32]: 0 with precondition: [V1=2,Out=0,V>=3] * Chain [[24],28,32]: 0 with precondition: [V1=2,Out=0,V>=6] * Chain [[24],27,32]: 0 with precondition: [V1=2,Out=0,V>=5] * Chain [[24],26,32]: 0 with precondition: [V1=2,Out=0,V>=6] * Chain [[24],25,32]: 0 with precondition: [V1=2,Out=0,V>=6] * Chain [[24],25,31,32]: 0 with precondition: [V1=2,Out=0,V>=6] * Chain [[24],25,29,32]: 0 with precondition: [V1=2,Out=0,V>=6] * Chain [32]: 0 with precondition: [Out=0,V1>=0,V>=0] * Chain [31,32]: 0 with precondition: [V1=2,V=0,Out=0] * Chain [30,32]: 0 with precondition: [V1=2,V=1,Out=0] * Chain [30,31,32]: 0 with precondition: [V1=2,V=1,Out=0] * Chain [30,29,32]: 0 with precondition: [V1=2,V=1,Out=0] * Chain [29,32]: 0 with precondition: [V1=2,Out=0,V>=0] * Chain [28,32]: 0 with precondition: [V1=2,Out=0,V>=3] * Chain [27,32]: 0 with precondition: [V1=2,Out=0,V>=2] * Chain [26,32]: 0 with precondition: [V1=2,Out=0,V>=3] * Chain [25,32]: 0 with precondition: [V1=2,Out=0,V>=3] * Chain [25,31,32]: 0 with precondition: [V1=2,Out=0,V>=3] * Chain [25,29,32]: 0 with precondition: [V1=2,Out=0,V>=3] #### Cost of chains of fun1(V1,Out): * Chain [[33],35]: 1*it(33)+1 Such that:it(33) =< 2*Out with precondition: [Out>=1,V1>=2*Out] * Chain [[33],34]: 1*it(33)+1 Such that:it(33) =< 2*Out with precondition: [V1+1=2*Out,V1>=3] * Chain [35]: 1 with precondition: [Out=0,V1>=0] * Chain [34]: 1 with precondition: [V1=1,Out=1] #### Cost of chains of fun2(V1,Out): * Chain [38]: 1 with precondition: [V1=0,Out=1] * Chain [37]: 0 with precondition: [Out=0,V1>=0] * Chain [36]: 1 with precondition: [Out=2,V1>=1] #### Cost of chains of fun(V1,V,Out): * Chain [[39,40,41,42,43,44,45,46],103]: 24*it(39)+1*s(5)+1*s(6)+0 Such that:aux(1) =< V+1 aux(5) =< V/3 it(39) =< aux(5) aux(2) =< aux(1)-1 s(5) =< it(39)*aux(1) s(6) =< it(39)*aux(2) with precondition: [V1=2,V>=3,Out>=1] * Chain [[39,40,41,42,43,44,45,46],102,103]: 24*it(39)+1*s(5)+1*s(6)+2 Such that:aux(1) =< V+1 aux(6) =< V/3 it(39) =< aux(6) aux(2) =< aux(1)-1 s(5) =< it(39)*aux(1) s(6) =< it(39)*aux(2) with precondition: [V1=2,V>=3,Out>=3] * Chain [[39,40,41,42,43,44,45,46],101,103]: 24*it(39)+1*s(5)+1*s(6)+3 Such that:aux(1) =< V+1 aux(7) =< V/3 it(39) =< aux(7) aux(2) =< aux(1)-1 s(5) =< it(39)*aux(1) s(6) =< it(39)*aux(2) with precondition: [V1=2,V>=3,Out>=4] * Chain [[39,40,41,42,43,44,45,46],100,103]: 24*it(39)+1*s(5)+1*s(6)+4 Such that:aux(1) =< V+1 aux(8) =< V/3 it(39) =< aux(8) aux(2) =< aux(1)-1 s(5) =< it(39)*aux(1) s(6) =< it(39)*aux(2) with precondition: [V1=2,V>=3,3*Out>=V+12] * Chain [[39,40,41,42,43,44,45,46],99,103]: 24*it(39)+1*s(5)+1*s(6)+2 Such that:aux(1) =< V+1 aux(9) =< V/3 it(39) =< aux(9) aux(2) =< aux(1)-1 s(5) =< it(39)*aux(1) s(6) =< it(39)*aux(2) with precondition: [V1=2,V>=3,3*Out>=V+3] * Chain [[39,40,41,42,43,44,45,46],98,103]: 24*it(39)+1*s(5)+1*s(6)+2 Such that:aux(1) =< V+1 aux(10) =< V/3 it(39) =< aux(10) aux(2) =< aux(1)-1 s(5) =< it(39)*aux(1) s(6) =< it(39)*aux(2) with precondition: [V1=2,V>=3,3*Out>=V+6] * Chain [[39,40,41,42,43,44,45,46],97,103]: 24*it(39)+1*s(5)+1*s(6)+3 Such that:aux(1) =< V+1 aux(11) =< V/3 it(39) =< aux(11) aux(2) =< aux(1)-1 s(5) =< it(39)*aux(1) s(6) =< it(39)*aux(2) with precondition: [V1=2,V>=3,3*Out>=V+9] * Chain [[39,40,41,42,43,44,45,46],96,103]: 24*it(39)+1*s(5)+1*s(6)+4 Such that:aux(1) =< V+1 aux(12) =< V/3 it(39) =< aux(12) aux(2) =< aux(1)-1 s(5) =< it(39)*aux(1) s(6) =< it(39)*aux(2) with precondition: [V1=2,V>=3,3*Out>=V+12] * Chain [[39,40,41,42,43,44,45,46],95,103]: 24*it(39)+1*s(5)+1*s(6)+2 Such that:aux(1) =< V+1 aux(13) =< V/3 it(39) =< aux(13) aux(2) =< aux(1)-1 s(5) =< it(39)*aux(1) s(6) =< it(39)*aux(2) with precondition: [V1=2,V>=4,3*Out>=V+5] * Chain [[39,40,41,42,43,44,45,46],94,103]: 24*it(39)+1*s(5)+1*s(6)+3 Such that:aux(1) =< V+1 aux(14) =< V/3 it(39) =< aux(14) aux(2) =< aux(1)-1 s(5) =< it(39)*aux(1) s(6) =< it(39)*aux(2) with precondition: [V1=2,V>=4,3*Out>=V+8] * Chain [[39,40,41,42,43,44,45,46],93,103]: 24*it(39)+1*s(5)+1*s(6)+3 Such that:aux(1) =< V+1 aux(15) =< V/3 it(39) =< aux(15) aux(2) =< aux(1)-1 s(5) =< it(39)*aux(1) s(6) =< it(39)*aux(2) with precondition: [V1=2,V>=4,Out>=5] * Chain [[39,40,41,42,43,44,45,46],92,103]: 24*it(39)+1*s(5)+1*s(6)+4 Such that:aux(1) =< V+1 aux(16) =< V/3 it(39) =< aux(16) aux(2) =< aux(1)-1 s(5) =< it(39)*aux(1) s(6) =< it(39)*aux(2) with precondition: [V1=2,V>=4,Out>=6] * Chain [[39,40,41,42,43,44,45,46],91,103]: 24*it(39)+1*s(5)+1*s(6)+2 Such that:aux(1) =< V+1 aux(17) =< V/3 it(39) =< aux(17) aux(2) =< aux(1)-1 s(5) =< it(39)*aux(1) s(6) =< it(39)*aux(2) with precondition: [V1=2,V>=4,3*Out>=V+2] * Chain [[39,40,41,42,43,44,45,46],91,102,103]: 24*it(39)+1*s(5)+1*s(6)+4 Such that:aux(1) =< V+1 aux(18) =< V/3 it(39) =< aux(18) aux(2) =< aux(1)-1 s(5) =< it(39)*aux(1) s(6) =< it(39)*aux(2) with precondition: [V1=2,V>=4,3*Out>=V+8] * Chain [[39,40,41,42,43,44,45,46],91,101,103]: 24*it(39)+1*s(5)+1*s(6)+5 Such that:aux(1) =< V+1 aux(19) =< V/3 it(39) =< aux(19) aux(2) =< aux(1)-1 s(5) =< it(39)*aux(1) s(6) =< it(39)*aux(2) with precondition: [V1=2,V>=4,3*Out>=V+11] * Chain [[39,40,41,42,43,44,45,46],91,100,103]: 24*it(39)+1*s(5)+1*s(6)+6 Such that:aux(1) =< V+1 aux(20) =< V/3 it(39) =< aux(20) aux(2) =< aux(1)-1 s(5) =< it(39)*aux(1) s(6) =< it(39)*aux(2) with precondition: [V1=2,V>=4,3*Out>=V+14] * Chain [[39,40,41,42,43,44,45,46],91,99,103]: 24*it(39)+1*s(5)+1*s(6)+4 Such that:aux(1) =< V+1 aux(21) =< V/3 it(39) =< aux(21) aux(2) =< aux(1)-1 s(5) =< it(39)*aux(1) s(6) =< it(39)*aux(2) with precondition: [V1=2,V>=4,3*Out>=V+5] * Chain [[39,40,41,42,43,44,45,46],91,98,103]: 24*it(39)+1*s(5)+1*s(6)+4 Such that:aux(1) =< V+1 aux(22) =< V/3 it(39) =< aux(22) aux(2) =< aux(1)-1 s(5) =< it(39)*aux(1) s(6) =< it(39)*aux(2) with precondition: [V1=2,V>=4,3*Out>=V+8] * Chain [[39,40,41,42,43,44,45,46],91,97,103]: 24*it(39)+1*s(5)+1*s(6)+5 Such that:aux(1) =< V+1 aux(23) =< V/3 it(39) =< aux(23) aux(2) =< aux(1)-1 s(5) =< it(39)*aux(1) s(6) =< it(39)*aux(2) with precondition: [V1=2,V>=4,3*Out>=V+11] * Chain [[39,40,41,42,43,44,45,46],91,96,103]: 24*it(39)+1*s(5)+1*s(6)+6 Such that:aux(1) =< V+1 aux(24) =< V/3 it(39) =< aux(24) aux(2) =< aux(1)-1 s(5) =< it(39)*aux(1) s(6) =< it(39)*aux(2) with precondition: [V1=2,V>=4,3*Out>=V+14] * Chain [[39,40,41,42,43,44,45,46],91,76,103]: 24*it(39)+1*s(5)+1*s(6)+4 Such that:aux(1) =< V+1 aux(25) =< V/3 it(39) =< aux(25) aux(2) =< aux(1)-1 s(5) =< it(39)*aux(1) s(6) =< it(39)*aux(2) with precondition: [V1=2,V>=4,3*Out>=V+5] * Chain [[39,40,41,42,43,44,45,46],90,103]: 24*it(39)+1*s(5)+1*s(6)+2 Such that:aux(1) =< V+1 aux(26) =< V/3 it(39) =< aux(26) aux(2) =< aux(1)-1 s(5) =< it(39)*aux(1) s(6) =< it(39)*aux(2) with precondition: [V1=2,V>=4,3*Out>=V+5] * Chain [[39,40,41,42,43,44,45,46],90,102,103]: 24*it(39)+1*s(5)+1*s(6)+4 Such that:aux(1) =< V+1 aux(27) =< V/3 it(39) =< aux(27) aux(2) =< aux(1)-1 s(5) =< it(39)*aux(1) s(6) =< it(39)*aux(2) with precondition: [V1=2,V>=4,3*Out>=V+11] * Chain [[39,40,41,42,43,44,45,46],90,101,103]: 24*it(39)+1*s(5)+1*s(6)+5 Such that:aux(1) =< V+1 aux(28) =< V/3 it(39) =< aux(28) aux(2) =< aux(1)-1 s(5) =< it(39)*aux(1) s(6) =< it(39)*aux(2) with precondition: [V1=2,V>=4,3*Out>=V+14] * Chain [[39,40,41,42,43,44,45,46],90,100,103]: 24*it(39)+1*s(5)+1*s(6)+6 Such that:aux(1) =< V+1 aux(29) =< V/3 it(39) =< aux(29) aux(2) =< aux(1)-1 s(5) =< it(39)*aux(1) s(6) =< it(39)*aux(2) with precondition: [V1=2,V>=4,3*Out>=V+17] * Chain [[39,40,41,42,43,44,45,46],90,99,103]: 24*it(39)+1*s(5)+1*s(6)+4 Such that:aux(1) =< V+1 aux(30) =< V/3 it(39) =< aux(30) aux(2) =< aux(1)-1 s(5) =< it(39)*aux(1) s(6) =< it(39)*aux(2) with precondition: [V1=2,V>=4,3*Out>=V+8] * Chain [[39,40,41,42,43,44,45,46],90,98,103]: 24*it(39)+1*s(5)+1*s(6)+4 Such that:aux(1) =< V+1 aux(31) =< V/3 it(39) =< aux(31) aux(2) =< aux(1)-1 s(5) =< it(39)*aux(1) s(6) =< it(39)*aux(2) with precondition: [V1=2,V>=4,3*Out>=V+11] * Chain [[39,40,41,42,43,44,45,46],90,97,103]: 24*it(39)+1*s(5)+1*s(6)+5 Such that:aux(1) =< V+1 aux(32) =< V/3 it(39) =< aux(32) aux(2) =< aux(1)-1 s(5) =< it(39)*aux(1) s(6) =< it(39)*aux(2) with precondition: [V1=2,V>=4,3*Out>=V+14] * Chain [[39,40,41,42,43,44,45,46],90,96,103]: 24*it(39)+1*s(5)+1*s(6)+6 Such that:aux(1) =< V+1 aux(33) =< V/3 it(39) =< aux(33) aux(2) =< aux(1)-1 s(5) =< it(39)*aux(1) s(6) =< it(39)*aux(2) with precondition: [V1=2,V>=4,3*Out>=V+17] * Chain [[39,40,41,42,43,44,45,46],90,76,103]: 24*it(39)+1*s(5)+1*s(6)+4 Such that:aux(1) =< V+1 aux(34) =< V/3 it(39) =< aux(34) aux(2) =< aux(1)-1 s(5) =< it(39)*aux(1) s(6) =< it(39)*aux(2) with precondition: [V1=2,V>=4,3*Out>=V+8] * Chain [[39,40,41,42,43,44,45,46],89,103]: 24*it(39)+1*s(5)+1*s(6)+3 Such that:aux(1) =< V+1 aux(35) =< V/3 it(39) =< aux(35) aux(2) =< aux(1)-1 s(5) =< it(39)*aux(1) s(6) =< it(39)*aux(2) with precondition: [V1=2,V>=4,3*Out>=V+8] * Chain [[39,40,41,42,43,44,45,46],89,102,103]: 24*it(39)+1*s(5)+1*s(6)+5 Such that:aux(1) =< V+1 aux(36) =< V/3 it(39) =< aux(36) aux(2) =< aux(1)-1 s(5) =< it(39)*aux(1) s(6) =< it(39)*aux(2) with precondition: [V1=2,V>=4,3*Out>=V+14] * Chain [[39,40,41,42,43,44,45,46],89,101,103]: 24*it(39)+1*s(5)+1*s(6)+6 Such that:aux(1) =< V+1 aux(37) =< V/3 it(39) =< aux(37) aux(2) =< aux(1)-1 s(5) =< it(39)*aux(1) s(6) =< it(39)*aux(2) with precondition: [V1=2,V>=4,3*Out>=V+17] * Chain [[39,40,41,42,43,44,45,46],89,100,103]: 24*it(39)+1*s(5)+1*s(6)+7 Such that:aux(1) =< V+1 aux(38) =< V/3 it(39) =< aux(38) aux(2) =< aux(1)-1 s(5) =< it(39)*aux(1) s(6) =< it(39)*aux(2) with precondition: [V1=2,V>=4,3*Out>=V+20] * Chain [[39,40,41,42,43,44,45,46],89,99,103]: 24*it(39)+1*s(5)+1*s(6)+5 Such that:aux(1) =< V+1 aux(39) =< V/3 it(39) =< aux(39) aux(2) =< aux(1)-1 s(5) =< it(39)*aux(1) s(6) =< it(39)*aux(2) with precondition: [V1=2,V>=4,3*Out>=V+11] * Chain [[39,40,41,42,43,44,45,46],89,98,103]: 24*it(39)+1*s(5)+1*s(6)+5 Such that:aux(1) =< V+1 aux(40) =< V/3 it(39) =< aux(40) aux(2) =< aux(1)-1 s(5) =< it(39)*aux(1) s(6) =< it(39)*aux(2) with precondition: [V1=2,V>=4,3*Out>=V+14] * Chain [[39,40,41,42,43,44,45,46],89,97,103]: 24*it(39)+1*s(5)+1*s(6)+6 Such that:aux(1) =< V+1 aux(41) =< V/3 it(39) =< aux(41) aux(2) =< aux(1)-1 s(5) =< it(39)*aux(1) s(6) =< it(39)*aux(2) with precondition: [V1=2,V>=4,3*Out>=V+17] * Chain [[39,40,41,42,43,44,45,46],89,96,103]: 24*it(39)+1*s(5)+1*s(6)+7 Such that:aux(1) =< V+1 aux(42) =< V/3 it(39) =< aux(42) aux(2) =< aux(1)-1 s(5) =< it(39)*aux(1) s(6) =< it(39)*aux(2) with precondition: [V1=2,V>=4,3*Out>=V+20] * Chain [[39,40,41,42,43,44,45,46],89,76,103]: 24*it(39)+1*s(5)+1*s(6)+5 Such that:aux(1) =< V+1 aux(43) =< V/3 it(39) =< aux(43) aux(2) =< aux(1)-1 s(5) =< it(39)*aux(1) s(6) =< it(39)*aux(2) with precondition: [V1=2,V>=4,3*Out>=V+11] * Chain [[39,40,41,42,43,44,45,46],88,103]: 24*it(39)+1*s(5)+1*s(6)+3 Such that:aux(1) =< V+1 aux(44) =< V/3 it(39) =< aux(44) aux(2) =< aux(1)-1 s(5) =< it(39)*aux(1) s(6) =< it(39)*aux(2) with precondition: [V1=2,V>=4,3*Out>=V+11] * Chain [[39,40,41,42,43,44,45,46],88,102,103]: 24*it(39)+1*s(5)+1*s(6)+5 Such that:aux(1) =< V+1 aux(45) =< V/3 it(39) =< aux(45) aux(2) =< aux(1)-1 s(5) =< it(39)*aux(1) s(6) =< it(39)*aux(2) with precondition: [V1=2,V>=4,3*Out>=V+17] * Chain [[39,40,41,42,43,44,45,46],88,101,103]: 24*it(39)+1*s(5)+1*s(6)+6 Such that:aux(1) =< V+1 aux(46) =< V/3 it(39) =< aux(46) aux(2) =< aux(1)-1 s(5) =< it(39)*aux(1) s(6) =< it(39)*aux(2) with precondition: [V1=2,V>=4,3*Out>=V+20] * Chain [[39,40,41,42,43,44,45,46],88,100,103]: 24*it(39)+1*s(5)+1*s(6)+7 Such that:aux(1) =< V+1 aux(47) =< V/3 it(39) =< aux(47) aux(2) =< aux(1)-1 s(5) =< it(39)*aux(1) s(6) =< it(39)*aux(2) with precondition: [V1=2,V>=4,3*Out>=V+23] * Chain [[39,40,41,42,43,44,45,46],88,99,103]: 24*it(39)+1*s(5)+1*s(6)+5 Such that:aux(1) =< V+1 aux(48) =< V/3 it(39) =< aux(48) aux(2) =< aux(1)-1 s(5) =< it(39)*aux(1) s(6) =< it(39)*aux(2) with precondition: [V1=2,V>=4,3*Out>=V+14] * Chain [[39,40,41,42,43,44,45,46],88,98,103]: 24*it(39)+1*s(5)+1*s(6)+5 Such that:aux(1) =< V+1 aux(49) =< V/3 it(39) =< aux(49) aux(2) =< aux(1)-1 s(5) =< it(39)*aux(1) s(6) =< it(39)*aux(2) with precondition: [V1=2,V>=4,3*Out>=V+17] * Chain [[39,40,41,42,43,44,45,46],88,97,103]: 24*it(39)+1*s(5)+1*s(6)+6 Such that:aux(1) =< V+1 aux(50) =< V/3 it(39) =< aux(50) aux(2) =< aux(1)-1 s(5) =< it(39)*aux(1) s(6) =< it(39)*aux(2) with precondition: [V1=2,V>=4,3*Out>=V+20] * Chain [[39,40,41,42,43,44,45,46],88,96,103]: 24*it(39)+1*s(5)+1*s(6)+7 Such that:aux(1) =< V+1 aux(51) =< V/3 it(39) =< aux(51) aux(2) =< aux(1)-1 s(5) =< it(39)*aux(1) s(6) =< it(39)*aux(2) with precondition: [V1=2,V>=4,3*Out>=V+23] * Chain [[39,40,41,42,43,44,45,46],88,76,103]: 24*it(39)+1*s(5)+1*s(6)+5 Such that:aux(1) =< V+1 aux(52) =< V/3 it(39) =< aux(52) aux(2) =< aux(1)-1 s(5) =< it(39)*aux(1) s(6) =< it(39)*aux(2) with precondition: [V1=2,V>=4,3*Out>=V+14] * Chain [[39,40,41,42,43,44,45,46],87,103]: 24*it(39)+1*s(5)+1*s(6)+4 Such that:aux(1) =< V+1 aux(53) =< V/3 it(39) =< aux(53) aux(2) =< aux(1)-1 s(5) =< it(39)*aux(1) s(6) =< it(39)*aux(2) with precondition: [V1=2,V>=4,3*Out>=V+14] * Chain [[39,40,41,42,43,44,45,46],87,102,103]: 24*it(39)+1*s(5)+1*s(6)+6 Such that:aux(1) =< V+1 aux(54) =< V/3 it(39) =< aux(54) aux(2) =< aux(1)-1 s(5) =< it(39)*aux(1) s(6) =< it(39)*aux(2) with precondition: [V1=2,V>=4,3*Out>=V+20] * Chain [[39,40,41,42,43,44,45,46],87,101,103]: 24*it(39)+1*s(5)+1*s(6)+7 Such that:aux(1) =< V+1 aux(55) =< V/3 it(39) =< aux(55) aux(2) =< aux(1)-1 s(5) =< it(39)*aux(1) s(6) =< it(39)*aux(2) with precondition: [V1=2,V>=4,3*Out>=V+23] * Chain [[39,40,41,42,43,44,45,46],87,100,103]: 24*it(39)+1*s(5)+1*s(6)+8 Such that:aux(1) =< V+1 aux(56) =< V/3 it(39) =< aux(56) aux(2) =< aux(1)-1 s(5) =< it(39)*aux(1) s(6) =< it(39)*aux(2) with precondition: [V1=2,V>=4,3*Out>=V+26] * Chain [[39,40,41,42,43,44,45,46],87,99,103]: 24*it(39)+1*s(5)+1*s(6)+6 Such that:aux(1) =< V+1 aux(57) =< V/3 it(39) =< aux(57) aux(2) =< aux(1)-1 s(5) =< it(39)*aux(1) s(6) =< it(39)*aux(2) with precondition: [V1=2,V>=4,3*Out>=V+17] * Chain [[39,40,41,42,43,44,45,46],87,98,103]: 24*it(39)+1*s(5)+1*s(6)+6 Such that:aux(1) =< V+1 aux(58) =< V/3 it(39) =< aux(58) aux(2) =< aux(1)-1 s(5) =< it(39)*aux(1) s(6) =< it(39)*aux(2) with precondition: [V1=2,V>=4,3*Out>=V+20] * Chain [[39,40,41,42,43,44,45,46],87,97,103]: 24*it(39)+1*s(5)+1*s(6)+7 Such that:aux(1) =< V+1 aux(59) =< V/3 it(39) =< aux(59) aux(2) =< aux(1)-1 s(5) =< it(39)*aux(1) s(6) =< it(39)*aux(2) with precondition: [V1=2,V>=4,3*Out>=V+23] * Chain [[39,40,41,42,43,44,45,46],87,96,103]: 24*it(39)+1*s(5)+1*s(6)+8 Such that:aux(1) =< V+1 aux(60) =< V/3 it(39) =< aux(60) aux(2) =< aux(1)-1 s(5) =< it(39)*aux(1) s(6) =< it(39)*aux(2) with precondition: [V1=2,V>=4,3*Out>=V+26] * Chain [[39,40,41,42,43,44,45,46],87,76,103]: 24*it(39)+1*s(5)+1*s(6)+6 Such that:aux(1) =< V+1 aux(61) =< V/3 it(39) =< aux(61) aux(2) =< aux(1)-1 s(5) =< it(39)*aux(1) s(6) =< it(39)*aux(2) with precondition: [V1=2,V>=4,3*Out>=V+17] * Chain [[39,40,41,42,43,44,45,46],86,103]: 24*it(39)+1*s(5)+1*s(6)+3*s(7)+2 Such that:aux(1) =< V+1 aux(3) =< V/3 aux(63) =< V s(7) =< aux(63) it(39) =< aux(3) it(39) =< aux(63) aux(2) =< aux(1)-1 s(5) =< it(39)*aux(1) s(6) =< it(39)*aux(2) with precondition: [V1=2,V>=5,Out>=3] * Chain [[39,40,41,42,43,44,45,46],85,103]: 24*it(39)+1*s(5)+1*s(6)+3 Such that:aux(1) =< V+1 aux(64) =< V/3 it(39) =< aux(64) aux(2) =< aux(1)-1 s(5) =< it(39)*aux(1) s(6) =< it(39)*aux(2) with precondition: [V1=2,V>=5,3*Out>=V+7] * Chain [[39,40,41,42,43,44,45,46],84,103]: 24*it(39)+1*s(5)+1*s(6)+3 Such that:aux(1) =< V+1 aux(65) =< V/3 it(39) =< aux(65) aux(2) =< aux(1)-1 s(5) =< it(39)*aux(1) s(6) =< it(39)*aux(2) with precondition: [V1=2,V>=5,3*Out>=V+10] * Chain [[39,40,41,42,43,44,45,46],83,103]: 24*it(39)+1*s(5)+1*s(6)+4 Such that:aux(1) =< V+1 aux(66) =< V/3 it(39) =< aux(66) aux(2) =< aux(1)-1 s(5) =< it(39)*aux(1) s(6) =< it(39)*aux(2) with precondition: [V1=2,V>=5,3*Out>=V+13] * Chain [[39,40,41,42,43,44,45,46],82,103]: 24*it(39)+1*s(5)+1*s(6)+4 Such that:aux(1) =< V+1 aux(67) =< V/3 it(39) =< aux(67) aux(2) =< aux(1)-1 s(5) =< it(39)*aux(1) s(6) =< it(39)*aux(2) with precondition: [V1=2,V>=5,Out>=7] * Chain [[39,40,41,42,43,44,45,46],81,103]: 24*it(39)+1*s(5)+1*s(6)+3*s(10)+2 Such that:aux(1) =< V+1 aux(3) =< V/3 aux(69) =< V s(10) =< aux(69) it(39) =< aux(3) it(39) =< aux(69) aux(2) =< aux(1)-1 s(5) =< it(39)*aux(1) s(6) =< it(39)*aux(2) with precondition: [V1=2,V>=5,Out>=3] * Chain [[39,40,41,42,43,44,45,46],80,103]: 24*it(39)+1*s(5)+1*s(6)+3 Such that:aux(1) =< V+1 aux(70) =< V/3 it(39) =< aux(70) aux(2) =< aux(1)-1 s(5) =< it(39)*aux(1) s(6) =< it(39)*aux(2) with precondition: [V1=2,V>=5,Out>=4] * Chain [[39,40,41,42,43,44,45,46],79,103]: 24*it(39)+1*s(5)+1*s(6)+3 Such that:aux(1) =< V+1 aux(71) =< V/3 it(39) =< aux(71) aux(2) =< aux(1)-1 s(5) =< it(39)*aux(1) s(6) =< it(39)*aux(2) with precondition: [V1=2,V>=5,Out>=5] * Chain [[39,40,41,42,43,44,45,46],78,103]: 24*it(39)+1*s(5)+1*s(6)+4 Such that:aux(1) =< V+1 aux(72) =< V/3 it(39) =< aux(72) aux(2) =< aux(1)-1 s(5) =< it(39)*aux(1) s(6) =< it(39)*aux(2) with precondition: [V1=2,V>=5,Out>=6] * Chain [[39,40,41,42,43,44,45,46],77,103]: 24*it(39)+1*s(5)+1*s(6)+4 Such that:aux(1) =< V+1 aux(73) =< V/3 it(39) =< aux(73) aux(2) =< aux(1)-1 s(5) =< it(39)*aux(1) s(6) =< it(39)*aux(2) with precondition: [V1=2,V>=5,Out>=7] * Chain [[39,40,41,42,43,44,45,46],76,103]: 24*it(39)+1*s(5)+1*s(6)+2 Such that:aux(1) =< V+1 aux(74) =< V/3 it(39) =< aux(74) aux(2) =< aux(1)-1 s(5) =< it(39)*aux(1) s(6) =< it(39)*aux(2) with precondition: [V1=2,V>=3,Out>=2] * Chain [[39,40,41,42,43,44,45,46],75,103]: 24*it(39)+1*s(5)+1*s(6)+4 Such that:aux(1) =< V+1 aux(75) =< V/3 it(39) =< aux(75) aux(2) =< aux(1)-1 s(5) =< it(39)*aux(1) s(6) =< it(39)*aux(2) with precondition: [V1=2,V>=6,Out>=8] * Chain [[39,40,41,42,43,44,45,46],74,103]: 24*it(39)+1*s(5)+1*s(6)+3*s(13)+2 Such that:aux(1) =< V+1 aux(3) =< V/3 aux(77) =< V+3 s(13) =< aux(77) it(39) =< aux(3) it(39) =< aux(77) aux(2) =< aux(1)-1 s(5) =< it(39)*aux(1) s(6) =< it(39)*aux(2) with precondition: [V1=2,V>=6,3*Out>=V+6] * Chain [[39,40,41,42,43,44,45,46],73,103]: 24*it(39)+1*s(5)+1*s(6)+2 Such that:aux(1) =< V+1 aux(78) =< V/3 it(39) =< aux(78) aux(2) =< aux(1)-1 s(5) =< it(39)*aux(1) s(6) =< it(39)*aux(2) with precondition: [V1=2,V>=6,Out>=2] * Chain [[39,40,41,42,43,44,45,46],72,103]: 24*it(39)+1*s(5)+1*s(6)+1*s(16)+2 Such that:aux(1) =< V+1 aux(3) =< V/3 aux(79) =< V s(16) =< aux(79) it(39) =< aux(3) it(39) =< aux(79) aux(2) =< aux(1)-1 s(5) =< it(39)*aux(1) s(6) =< it(39)*aux(2) with precondition: [V1=2,V>=6,Out>=3] * Chain [[39,40,41,42,43,44,45,46],71,103]: 24*it(39)+1*s(5)+1*s(6)+3 Such that:aux(1) =< V+1 aux(80) =< V/3 it(39) =< aux(80) aux(2) =< aux(1)-1 s(5) =< it(39)*aux(1) s(6) =< it(39)*aux(2) with precondition: [V1=2,V>=6,Out>=4] * Chain [[39,40,41,42,43,44,45,46],70,103]: 24*it(39)+1*s(5)+1*s(6)+3 Such that:aux(1) =< V+1 aux(81) =< V/3 it(39) =< aux(81) aux(2) =< aux(1)-1 s(5) =< it(39)*aux(1) s(6) =< it(39)*aux(2) with precondition: [V1=2,V>=6,Out>=5] * Chain [[39,40,41,42,43,44,45,46],69,103]: 24*it(39)+1*s(5)+1*s(6)+4 Such that:aux(1) =< V+1 aux(82) =< V/3 it(39) =< aux(82) aux(2) =< aux(1)-1 s(5) =< it(39)*aux(1) s(6) =< it(39)*aux(2) with precondition: [V1=2,V>=6,Out>=6] * Chain [[39,40,41,42,43,44,45,46],68,103]: 24*it(39)+1*s(5)+1*s(6)+4 Such that:aux(1) =< V+1 aux(83) =< V/3 it(39) =< aux(83) aux(2) =< aux(1)-1 s(5) =< it(39)*aux(1) s(6) =< it(39)*aux(2) with precondition: [V1=2,V>=6,Out>=7] * Chain [[39,40,41,42,43,44,45,46],67,103]: 24*it(39)+1*s(5)+1*s(6)+4 Such that:aux(1) =< V+1 aux(84) =< V/3 it(39) =< aux(84) aux(2) =< aux(1)-1 s(5) =< it(39)*aux(1) s(6) =< it(39)*aux(2) with precondition: [V1=2,V>=6,Out>=8] * Chain [[39,40,41,42,43,44,45,46],66,103]: 24*it(39)+1*s(5)+1*s(6)+1*s(17)+2 Such that:aux(1) =< V+1 aux(3) =< V/3 aux(85) =< V+3 s(17) =< aux(85) it(39) =< aux(3) it(39) =< aux(85) aux(2) =< aux(1)-1 s(5) =< it(39)*aux(1) s(6) =< it(39)*aux(2) with precondition: [V1=2,V>=6,3*Out>=V+6] * Chain [[39,40,41,42,43,44,45,46],65,103]: 24*it(39)+1*s(5)+1*s(6)+2 Such that:aux(1) =< V+1 aux(86) =< V/3 it(39) =< aux(86) aux(2) =< aux(1)-1 s(5) =< it(39)*aux(1) s(6) =< it(39)*aux(2) with precondition: [V1=2,V>=5,Out>=2] * Chain [[39,40,41,42,43,44,45,46],64,103]: 24*it(39)+1*s(5)+1*s(6)+4 Such that:aux(1) =< V+1 aux(87) =< V/3 it(39) =< aux(87) aux(2) =< aux(1)-1 s(5) =< it(39)*aux(1) s(6) =< it(39)*aux(2) with precondition: [V1=2,V>=6,Out>=8] * Chain [[39,40,41,42,43,44,45,46],63,103]: 24*it(39)+1*s(5)+1*s(6)+3*s(18)+2 Such that:aux(1) =< V+1 aux(3) =< V/3 aux(89) =< V+3 s(18) =< aux(89) it(39) =< aux(3) it(39) =< aux(89) aux(2) =< aux(1)-1 s(5) =< it(39)*aux(1) s(6) =< it(39)*aux(2) with precondition: [V1=2,V>=6,3*Out>=V+6] * Chain [[39,40,41,42,43,44,45,46],62,103]: 24*it(39)+1*s(5)+1*s(6)+2 Such that:aux(1) =< V+1 aux(90) =< V/3 it(39) =< aux(90) aux(2) =< aux(1)-1 s(5) =< it(39)*aux(1) s(6) =< it(39)*aux(2) with precondition: [V1=2,V>=6,Out>=2] * Chain [[39,40,41,42,43,44,45,46],61,103]: 24*it(39)+1*s(5)+1*s(6)+1*s(21)+2 Such that:aux(1) =< V+1 aux(3) =< V/3 aux(91) =< V s(21) =< aux(91) it(39) =< aux(3) it(39) =< aux(91) aux(2) =< aux(1)-1 s(5) =< it(39)*aux(1) s(6) =< it(39)*aux(2) with precondition: [V1=2,V>=6,Out>=3] * Chain [[39,40,41,42,43,44,45,46],60,103]: 24*it(39)+1*s(5)+1*s(6)+3 Such that:aux(1) =< V+1 aux(92) =< V/3 it(39) =< aux(92) aux(2) =< aux(1)-1 s(5) =< it(39)*aux(1) s(6) =< it(39)*aux(2) with precondition: [V1=2,V>=6,Out>=4] * Chain [[39,40,41,42,43,44,45,46],59,103]: 24*it(39)+1*s(5)+1*s(6)+3 Such that:aux(1) =< V+1 aux(93) =< V/3 it(39) =< aux(93) aux(2) =< aux(1)-1 s(5) =< it(39)*aux(1) s(6) =< it(39)*aux(2) with precondition: [V1=2,V>=6,Out>=5] * Chain [[39,40,41,42,43,44,45,46],58,103]: 24*it(39)+1*s(5)+1*s(6)+4 Such that:aux(1) =< V+1 aux(94) =< V/3 it(39) =< aux(94) aux(2) =< aux(1)-1 s(5) =< it(39)*aux(1) s(6) =< it(39)*aux(2) with precondition: [V1=2,V>=6,Out>=6] * Chain [[39,40,41,42,43,44,45,46],57,103]: 24*it(39)+1*s(5)+1*s(6)+4 Such that:aux(1) =< V+1 aux(95) =< V/3 it(39) =< aux(95) aux(2) =< aux(1)-1 s(5) =< it(39)*aux(1) s(6) =< it(39)*aux(2) with precondition: [V1=2,V>=6,Out>=7] * Chain [[39,40,41,42,43,44,45,46],56,103]: 24*it(39)+1*s(5)+1*s(6)+4 Such that:aux(1) =< V+1 aux(96) =< V/3 it(39) =< aux(96) aux(2) =< aux(1)-1 s(5) =< it(39)*aux(1) s(6) =< it(39)*aux(2) with precondition: [V1=2,V>=6,Out>=8] * Chain [[39,40,41,42,43,44,45,46],55,103]: 24*it(39)+1*s(5)+1*s(6)+1*s(22)+2 Such that:aux(1) =< V+1 aux(3) =< V/3 aux(97) =< V+3 s(22) =< aux(97) it(39) =< aux(3) it(39) =< aux(97) aux(2) =< aux(1)-1 s(5) =< it(39)*aux(1) s(6) =< it(39)*aux(2) with precondition: [V1=2,V>=6,3*Out>=V+6] * Chain [[39,40,41,42,43,44,45,46],54,103]: 24*it(39)+1*s(5)+1*s(6)+2 Such that:aux(1) =< V+1 aux(98) =< V/3 it(39) =< aux(98) aux(2) =< aux(1)-1 s(5) =< it(39)*aux(1) s(6) =< it(39)*aux(2) with precondition: [V1=2,V>=6,Out>=2] * Chain [[39,40,41,42,43,44,45,46],54,102,103]: 24*it(39)+1*s(5)+1*s(6)+4 Such that:aux(1) =< V+1 aux(99) =< V/3 it(39) =< aux(99) aux(2) =< aux(1)-1 s(5) =< it(39)*aux(1) s(6) =< it(39)*aux(2) with precondition: [V1=2,V>=6,Out>=4] * Chain [[39,40,41,42,43,44,45,46],54,101,103]: 24*it(39)+1*s(5)+1*s(6)+5 Such that:aux(1) =< V+1 aux(100) =< V/3 it(39) =< aux(100) aux(2) =< aux(1)-1 s(5) =< it(39)*aux(1) s(6) =< it(39)*aux(2) with precondition: [V1=2,V>=6,Out>=5] * Chain [[39,40,41,42,43,44,45,46],54,100,103]: 24*it(39)+1*s(5)+1*s(6)+6 Such that:aux(1) =< V+1 aux(101) =< V/3 it(39) =< aux(101) aux(2) =< aux(1)-1 s(5) =< it(39)*aux(1) s(6) =< it(39)*aux(2) with precondition: [V1=2,V>=6,Out>=6] * Chain [[39,40,41,42,43,44,45,46],54,99,103]: 24*it(39)+1*s(5)+1*s(6)+4 Such that:aux(1) =< V+1 aux(102) =< V/3 it(39) =< aux(102) aux(2) =< aux(1)-1 s(5) =< it(39)*aux(1) s(6) =< it(39)*aux(2) with precondition: [V1=2,V>=6,Out>=3] * Chain [[39,40,41,42,43,44,45,46],54,98,103]: 24*it(39)+1*s(5)+1*s(6)+4 Such that:aux(1) =< V+1 aux(103) =< V/3 it(39) =< aux(103) aux(2) =< aux(1)-1 s(5) =< it(39)*aux(1) s(6) =< it(39)*aux(2) with precondition: [V1=2,V>=6,Out>=4] * Chain [[39,40,41,42,43,44,45,46],54,97,103]: 24*it(39)+1*s(5)+1*s(6)+5 Such that:aux(1) =< V+1 aux(104) =< V/3 it(39) =< aux(104) aux(2) =< aux(1)-1 s(5) =< it(39)*aux(1) s(6) =< it(39)*aux(2) with precondition: [V1=2,V>=6,Out>=5] * Chain [[39,40,41,42,43,44,45,46],54,96,103]: 24*it(39)+1*s(5)+1*s(6)+6 Such that:aux(1) =< V+1 aux(105) =< V/3 it(39) =< aux(105) aux(2) =< aux(1)-1 s(5) =< it(39)*aux(1) s(6) =< it(39)*aux(2) with precondition: [V1=2,V>=6,Out>=6] * Chain [[39,40,41,42,43,44,45,46],54,76,103]: 24*it(39)+1*s(5)+1*s(6)+4 Such that:aux(1) =< V+1 aux(106) =< V/3 it(39) =< aux(106) aux(2) =< aux(1)-1 s(5) =< it(39)*aux(1) s(6) =< it(39)*aux(2) with precondition: [V1=2,V>=6,Out>=3] * Chain [[39,40,41,42,43,44,45,46],53,103]: 24*it(39)+1*s(5)+1*s(6)+3*s(23)+2 Such that:aux(1) =< V+1 aux(3) =< V/3 aux(108) =< V s(23) =< aux(108) it(39) =< aux(3) it(39) =< aux(108) aux(2) =< aux(1)-1 s(5) =< it(39)*aux(1) s(6) =< it(39)*aux(2) with precondition: [V1=2,V>=6,Out>=3] * Chain [[39,40,41,42,43,44,45,46],53,102,103]: 24*it(39)+1*s(5)+1*s(6)+3*s(23)+4 Such that:aux(1) =< V+1 aux(3) =< V/3 aux(109) =< V s(23) =< aux(109) it(39) =< aux(3) it(39) =< aux(109) aux(2) =< aux(1)-1 s(5) =< it(39)*aux(1) s(6) =< it(39)*aux(2) with precondition: [V1=2,V>=6,Out>=5] * Chain [[39,40,41,42,43,44,45,46],53,101,103]: 24*it(39)+1*s(5)+1*s(6)+3*s(23)+5 Such that:aux(1) =< V+1 aux(3) =< V/3 aux(110) =< V s(23) =< aux(110) it(39) =< aux(3) it(39) =< aux(110) aux(2) =< aux(1)-1 s(5) =< it(39)*aux(1) s(6) =< it(39)*aux(2) with precondition: [V1=2,V>=6,Out>=6] * Chain [[39,40,41,42,43,44,45,46],53,100,103]: 24*it(39)+1*s(5)+1*s(6)+3*s(23)+6 Such that:aux(1) =< V+1 aux(3) =< V/3 aux(111) =< V s(23) =< aux(111) it(39) =< aux(3) it(39) =< aux(111) aux(2) =< aux(1)-1 s(5) =< it(39)*aux(1) s(6) =< it(39)*aux(2) with precondition: [V1=2,V>=6,Out>=7] * Chain [[39,40,41,42,43,44,45,46],53,99,103]: 24*it(39)+1*s(5)+1*s(6)+3*s(23)+4 Such that:aux(1) =< V+1 aux(3) =< V/3 aux(112) =< V s(23) =< aux(112) it(39) =< aux(3) it(39) =< aux(112) aux(2) =< aux(1)-1 s(5) =< it(39)*aux(1) s(6) =< it(39)*aux(2) with precondition: [V1=2,V>=6,Out>=4] * Chain [[39,40,41,42,43,44,45,46],53,98,103]: 24*it(39)+1*s(5)+1*s(6)+3*s(23)+4 Such that:aux(1) =< V+1 aux(3) =< V/3 aux(113) =< V s(23) =< aux(113) it(39) =< aux(3) it(39) =< aux(113) aux(2) =< aux(1)-1 s(5) =< it(39)*aux(1) s(6) =< it(39)*aux(2) with precondition: [V1=2,V>=6,Out>=5] * Chain [[39,40,41,42,43,44,45,46],53,97,103]: 24*it(39)+1*s(5)+1*s(6)+3*s(23)+5 Such that:aux(1) =< V+1 aux(3) =< V/3 aux(114) =< V s(23) =< aux(114) it(39) =< aux(3) it(39) =< aux(114) aux(2) =< aux(1)-1 s(5) =< it(39)*aux(1) s(6) =< it(39)*aux(2) with precondition: [V1=2,V>=6,Out>=6] * Chain [[39,40,41,42,43,44,45,46],53,96,103]: 24*it(39)+1*s(5)+1*s(6)+3*s(23)+6 Such that:aux(1) =< V+1 aux(3) =< V/3 aux(115) =< V s(23) =< aux(115) it(39) =< aux(3) it(39) =< aux(115) aux(2) =< aux(1)-1 s(5) =< it(39)*aux(1) s(6) =< it(39)*aux(2) with precondition: [V1=2,V>=6,Out>=7] * Chain [[39,40,41,42,43,44,45,46],53,76,103]: 24*it(39)+1*s(5)+1*s(6)+3*s(23)+4 Such that:aux(1) =< V+1 aux(3) =< V/3 aux(116) =< V s(23) =< aux(116) it(39) =< aux(3) it(39) =< aux(116) aux(2) =< aux(1)-1 s(5) =< it(39)*aux(1) s(6) =< it(39)*aux(2) with precondition: [V1=2,V>=6,Out>=4] * Chain [[39,40,41,42,43,44,45,46],52,103]: 24*it(39)+1*s(5)+1*s(6)+3 Such that:aux(1) =< V+1 aux(117) =< V/3 it(39) =< aux(117) aux(2) =< aux(1)-1 s(5) =< it(39)*aux(1) s(6) =< it(39)*aux(2) with precondition: [V1=2,V>=6,Out>=4] * Chain [[39,40,41,42,43,44,45,46],52,102,103]: 24*it(39)+1*s(5)+1*s(6)+5 Such that:aux(1) =< V+1 aux(118) =< V/3 it(39) =< aux(118) aux(2) =< aux(1)-1 s(5) =< it(39)*aux(1) s(6) =< it(39)*aux(2) with precondition: [V1=2,V>=6,Out>=6] * Chain [[39,40,41,42,43,44,45,46],52,101,103]: 24*it(39)+1*s(5)+1*s(6)+6 Such that:aux(1) =< V+1 aux(119) =< V/3 it(39) =< aux(119) aux(2) =< aux(1)-1 s(5) =< it(39)*aux(1) s(6) =< it(39)*aux(2) with precondition: [V1=2,V>=6,Out>=7] * Chain [[39,40,41,42,43,44,45,46],52,100,103]: 24*it(39)+1*s(5)+1*s(6)+7 Such that:aux(1) =< V+1 aux(120) =< V/3 it(39) =< aux(120) aux(2) =< aux(1)-1 s(5) =< it(39)*aux(1) s(6) =< it(39)*aux(2) with precondition: [V1=2,V>=6,Out>=8] * Chain [[39,40,41,42,43,44,45,46],52,99,103]: 24*it(39)+1*s(5)+1*s(6)+5 Such that:aux(1) =< V+1 aux(121) =< V/3 it(39) =< aux(121) aux(2) =< aux(1)-1 s(5) =< it(39)*aux(1) s(6) =< it(39)*aux(2) with precondition: [V1=2,V>=6,Out>=5] * Chain [[39,40,41,42,43,44,45,46],52,98,103]: 24*it(39)+1*s(5)+1*s(6)+5 Such that:aux(1) =< V+1 aux(122) =< V/3 it(39) =< aux(122) aux(2) =< aux(1)-1 s(5) =< it(39)*aux(1) s(6) =< it(39)*aux(2) with precondition: [V1=2,V>=6,Out>=6] * Chain [[39,40,41,42,43,44,45,46],52,97,103]: 24*it(39)+1*s(5)+1*s(6)+6 Such that:aux(1) =< V+1 aux(123) =< V/3 it(39) =< aux(123) aux(2) =< aux(1)-1 s(5) =< it(39)*aux(1) s(6) =< it(39)*aux(2) with precondition: [V1=2,V>=6,Out>=7] * Chain [[39,40,41,42,43,44,45,46],52,96,103]: 24*it(39)+1*s(5)+1*s(6)+7 Such that:aux(1) =< V+1 aux(124) =< V/3 it(39) =< aux(124) aux(2) =< aux(1)-1 s(5) =< it(39)*aux(1) s(6) =< it(39)*aux(2) with precondition: [V1=2,V>=6,Out>=8] * Chain [[39,40,41,42,43,44,45,46],52,76,103]: 24*it(39)+1*s(5)+1*s(6)+5 Such that:aux(1) =< V+1 aux(125) =< V/3 it(39) =< aux(125) aux(2) =< aux(1)-1 s(5) =< it(39)*aux(1) s(6) =< it(39)*aux(2) with precondition: [V1=2,V>=6,Out>=5] * Chain [[39,40,41,42,43,44,45,46],51,103]: 24*it(39)+1*s(5)+1*s(6)+3 Such that:aux(1) =< V+1 aux(126) =< V/3 it(39) =< aux(126) aux(2) =< aux(1)-1 s(5) =< it(39)*aux(1) s(6) =< it(39)*aux(2) with precondition: [V1=2,V>=6,Out>=5] * Chain [[39,40,41,42,43,44,45,46],51,102,103]: 24*it(39)+1*s(5)+1*s(6)+5 Such that:aux(1) =< V+1 aux(127) =< V/3 it(39) =< aux(127) aux(2) =< aux(1)-1 s(5) =< it(39)*aux(1) s(6) =< it(39)*aux(2) with precondition: [V1=2,V>=6,Out>=7] * Chain [[39,40,41,42,43,44,45,46],51,101,103]: 24*it(39)+1*s(5)+1*s(6)+6 Such that:aux(1) =< V+1 aux(128) =< V/3 it(39) =< aux(128) aux(2) =< aux(1)-1 s(5) =< it(39)*aux(1) s(6) =< it(39)*aux(2) with precondition: [V1=2,V>=6,Out>=8] * Chain [[39,40,41,42,43,44,45,46],51,100,103]: 24*it(39)+1*s(5)+1*s(6)+7 Such that:aux(1) =< V+1 aux(129) =< V/3 it(39) =< aux(129) aux(2) =< aux(1)-1 s(5) =< it(39)*aux(1) s(6) =< it(39)*aux(2) with precondition: [V1=2,V>=6,Out>=9] * Chain [[39,40,41,42,43,44,45,46],51,99,103]: 24*it(39)+1*s(5)+1*s(6)+5 Such that:aux(1) =< V+1 aux(130) =< V/3 it(39) =< aux(130) aux(2) =< aux(1)-1 s(5) =< it(39)*aux(1) s(6) =< it(39)*aux(2) with precondition: [V1=2,V>=6,Out>=6] * Chain [[39,40,41,42,43,44,45,46],51,98,103]: 24*it(39)+1*s(5)+1*s(6)+5 Such that:aux(1) =< V+1 aux(131) =< V/3 it(39) =< aux(131) aux(2) =< aux(1)-1 s(5) =< it(39)*aux(1) s(6) =< it(39)*aux(2) with precondition: [V1=2,V>=6,Out>=7] * Chain [[39,40,41,42,43,44,45,46],51,97,103]: 24*it(39)+1*s(5)+1*s(6)+6 Such that:aux(1) =< V+1 aux(132) =< V/3 it(39) =< aux(132) aux(2) =< aux(1)-1 s(5) =< it(39)*aux(1) s(6) =< it(39)*aux(2) with precondition: [V1=2,V>=6,Out>=8] * Chain [[39,40,41,42,43,44,45,46],51,96,103]: 24*it(39)+1*s(5)+1*s(6)+7 Such that:aux(1) =< V+1 aux(133) =< V/3 it(39) =< aux(133) aux(2) =< aux(1)-1 s(5) =< it(39)*aux(1) s(6) =< it(39)*aux(2) with precondition: [V1=2,V>=6,Out>=9] * Chain [[39,40,41,42,43,44,45,46],51,76,103]: 24*it(39)+1*s(5)+1*s(6)+5 Such that:aux(1) =< V+1 aux(134) =< V/3 it(39) =< aux(134) aux(2) =< aux(1)-1 s(5) =< it(39)*aux(1) s(6) =< it(39)*aux(2) with precondition: [V1=2,V>=6,Out>=6] * Chain [[39,40,41,42,43,44,45,46],50,103]: 24*it(39)+1*s(5)+1*s(6)+4 Such that:aux(1) =< V+1 aux(135) =< V/3 it(39) =< aux(135) aux(2) =< aux(1)-1 s(5) =< it(39)*aux(1) s(6) =< it(39)*aux(2) with precondition: [V1=2,V>=6,Out>=6] * Chain [[39,40,41,42,43,44,45,46],50,102,103]: 24*it(39)+1*s(5)+1*s(6)+6 Such that:aux(1) =< V+1 aux(136) =< V/3 it(39) =< aux(136) aux(2) =< aux(1)-1 s(5) =< it(39)*aux(1) s(6) =< it(39)*aux(2) with precondition: [V1=2,V>=6,Out>=8] * Chain [[39,40,41,42,43,44,45,46],50,101,103]: 24*it(39)+1*s(5)+1*s(6)+7 Such that:aux(1) =< V+1 aux(137) =< V/3 it(39) =< aux(137) aux(2) =< aux(1)-1 s(5) =< it(39)*aux(1) s(6) =< it(39)*aux(2) with precondition: [V1=2,V>=6,Out>=9] * Chain [[39,40,41,42,43,44,45,46],50,100,103]: 24*it(39)+1*s(5)+1*s(6)+8 Such that:aux(1) =< V+1 aux(138) =< V/3 it(39) =< aux(138) aux(2) =< aux(1)-1 s(5) =< it(39)*aux(1) s(6) =< it(39)*aux(2) with precondition: [V1=2,V>=6,Out>=10] * Chain [[39,40,41,42,43,44,45,46],50,99,103]: 24*it(39)+1*s(5)+1*s(6)+6 Such that:aux(1) =< V+1 aux(139) =< V/3 it(39) =< aux(139) aux(2) =< aux(1)-1 s(5) =< it(39)*aux(1) s(6) =< it(39)*aux(2) with precondition: [V1=2,V>=6,Out>=7] * Chain [[39,40,41,42,43,44,45,46],50,98,103]: 24*it(39)+1*s(5)+1*s(6)+6 Such that:aux(1) =< V+1 aux(140) =< V/3 it(39) =< aux(140) aux(2) =< aux(1)-1 s(5) =< it(39)*aux(1) s(6) =< it(39)*aux(2) with precondition: [V1=2,V>=6,Out>=8] * Chain [[39,40,41,42,43,44,45,46],50,97,103]: 24*it(39)+1*s(5)+1*s(6)+7 Such that:aux(1) =< V+1 aux(141) =< V/3 it(39) =< aux(141) aux(2) =< aux(1)-1 s(5) =< it(39)*aux(1) s(6) =< it(39)*aux(2) with precondition: [V1=2,V>=6,Out>=9] * Chain [[39,40,41,42,43,44,45,46],50,96,103]: 24*it(39)+1*s(5)+1*s(6)+8 Such that:aux(1) =< V+1 aux(142) =< V/3 it(39) =< aux(142) aux(2) =< aux(1)-1 s(5) =< it(39)*aux(1) s(6) =< it(39)*aux(2) with precondition: [V1=2,V>=6,Out>=10] * Chain [[39,40,41,42,43,44,45,46],50,76,103]: 24*it(39)+1*s(5)+1*s(6)+6 Such that:aux(1) =< V+1 aux(143) =< V/3 it(39) =< aux(143) aux(2) =< aux(1)-1 s(5) =< it(39)*aux(1) s(6) =< it(39)*aux(2) with precondition: [V1=2,V>=6,Out>=7] * Chain [[39,40,41,42,43,44,45,46],49,103]: 24*it(39)+1*s(5)+1*s(6)+4 Such that:aux(1) =< V+1 aux(144) =< V/3 it(39) =< aux(144) aux(2) =< aux(1)-1 s(5) =< it(39)*aux(1) s(6) =< it(39)*aux(2) with precondition: [V1=2,V>=6,Out>=7] * Chain [[39,40,41,42,43,44,45,46],49,102,103]: 24*it(39)+1*s(5)+1*s(6)+6 Such that:aux(1) =< V+1 aux(145) =< V/3 it(39) =< aux(145) aux(2) =< aux(1)-1 s(5) =< it(39)*aux(1) s(6) =< it(39)*aux(2) with precondition: [V1=2,V>=6,Out>=9] * Chain [[39,40,41,42,43,44,45,46],49,101,103]: 24*it(39)+1*s(5)+1*s(6)+7 Such that:aux(1) =< V+1 aux(146) =< V/3 it(39) =< aux(146) aux(2) =< aux(1)-1 s(5) =< it(39)*aux(1) s(6) =< it(39)*aux(2) with precondition: [V1=2,V>=6,Out>=10] * Chain [[39,40,41,42,43,44,45,46],49,100,103]: 24*it(39)+1*s(5)+1*s(6)+8 Such that:aux(1) =< V+1 aux(147) =< V/3 it(39) =< aux(147) aux(2) =< aux(1)-1 s(5) =< it(39)*aux(1) s(6) =< it(39)*aux(2) with precondition: [V1=2,V>=6,Out>=11] * Chain [[39,40,41,42,43,44,45,46],49,99,103]: 24*it(39)+1*s(5)+1*s(6)+6 Such that:aux(1) =< V+1 aux(148) =< V/3 it(39) =< aux(148) aux(2) =< aux(1)-1 s(5) =< it(39)*aux(1) s(6) =< it(39)*aux(2) with precondition: [V1=2,V>=6,Out>=8] * Chain [[39,40,41,42,43,44,45,46],49,98,103]: 24*it(39)+1*s(5)+1*s(6)+6 Such that:aux(1) =< V+1 aux(149) =< V/3 it(39) =< aux(149) aux(2) =< aux(1)-1 s(5) =< it(39)*aux(1) s(6) =< it(39)*aux(2) with precondition: [V1=2,V>=6,Out>=9] * Chain [[39,40,41,42,43,44,45,46],49,97,103]: 24*it(39)+1*s(5)+1*s(6)+7 Such that:aux(1) =< V+1 aux(150) =< V/3 it(39) =< aux(150) aux(2) =< aux(1)-1 s(5) =< it(39)*aux(1) s(6) =< it(39)*aux(2) with precondition: [V1=2,V>=6,Out>=10] * Chain [[39,40,41,42,43,44,45,46],49,96,103]: 24*it(39)+1*s(5)+1*s(6)+8 Such that:aux(1) =< V+1 aux(151) =< V/3 it(39) =< aux(151) aux(2) =< aux(1)-1 s(5) =< it(39)*aux(1) s(6) =< it(39)*aux(2) with precondition: [V1=2,V>=6,Out>=11] * Chain [[39,40,41,42,43,44,45,46],49,76,103]: 24*it(39)+1*s(5)+1*s(6)+6 Such that:aux(1) =< V+1 aux(152) =< V/3 it(39) =< aux(152) aux(2) =< aux(1)-1 s(5) =< it(39)*aux(1) s(6) =< it(39)*aux(2) with precondition: [V1=2,V>=6,Out>=8] * Chain [[39,40,41,42,43,44,45,46],48,103]: 24*it(39)+1*s(5)+1*s(6)+4 Such that:aux(1) =< V+1 aux(153) =< V/3 it(39) =< aux(153) aux(2) =< aux(1)-1 s(5) =< it(39)*aux(1) s(6) =< it(39)*aux(2) with precondition: [V1=2,V>=6,Out>=8] * Chain [[39,40,41,42,43,44,45,46],48,102,103]: 24*it(39)+1*s(5)+1*s(6)+6 Such that:aux(1) =< V+1 aux(154) =< V/3 it(39) =< aux(154) aux(2) =< aux(1)-1 s(5) =< it(39)*aux(1) s(6) =< it(39)*aux(2) with precondition: [V1=2,V>=6,Out>=10] * Chain [[39,40,41,42,43,44,45,46],48,101,103]: 24*it(39)+1*s(5)+1*s(6)+7 Such that:aux(1) =< V+1 aux(155) =< V/3 it(39) =< aux(155) aux(2) =< aux(1)-1 s(5) =< it(39)*aux(1) s(6) =< it(39)*aux(2) with precondition: [V1=2,V>=6,Out>=11] * Chain [[39,40,41,42,43,44,45,46],48,100,103]: 24*it(39)+1*s(5)+1*s(6)+8 Such that:aux(1) =< V+1 aux(156) =< V/3 it(39) =< aux(156) aux(2) =< aux(1)-1 s(5) =< it(39)*aux(1) s(6) =< it(39)*aux(2) with precondition: [V1=2,V>=6,Out>=12] * Chain [[39,40,41,42,43,44,45,46],48,99,103]: 24*it(39)+1*s(5)+1*s(6)+6 Such that:aux(1) =< V+1 aux(157) =< V/3 it(39) =< aux(157) aux(2) =< aux(1)-1 s(5) =< it(39)*aux(1) s(6) =< it(39)*aux(2) with precondition: [V1=2,V>=6,Out>=9] * Chain [[39,40,41,42,43,44,45,46],48,98,103]: 24*it(39)+1*s(5)+1*s(6)+6 Such that:aux(1) =< V+1 aux(158) =< V/3 it(39) =< aux(158) aux(2) =< aux(1)-1 s(5) =< it(39)*aux(1) s(6) =< it(39)*aux(2) with precondition: [V1=2,V>=6,Out>=10] * Chain [[39,40,41,42,43,44,45,46],48,97,103]: 24*it(39)+1*s(5)+1*s(6)+7 Such that:aux(1) =< V+1 aux(159) =< V/3 it(39) =< aux(159) aux(2) =< aux(1)-1 s(5) =< it(39)*aux(1) s(6) =< it(39)*aux(2) with precondition: [V1=2,V>=6,Out>=11] * Chain [[39,40,41,42,43,44,45,46],48,96,103]: 24*it(39)+1*s(5)+1*s(6)+8 Such that:aux(1) =< V+1 aux(160) =< V/3 it(39) =< aux(160) aux(2) =< aux(1)-1 s(5) =< it(39)*aux(1) s(6) =< it(39)*aux(2) with precondition: [V1=2,V>=6,Out>=12] * Chain [[39,40,41,42,43,44,45,46],48,76,103]: 24*it(39)+1*s(5)+1*s(6)+6 Such that:aux(1) =< V+1 aux(161) =< V/3 it(39) =< aux(161) aux(2) =< aux(1)-1 s(5) =< it(39)*aux(1) s(6) =< it(39)*aux(2) with precondition: [V1=2,V>=6,Out>=9] * Chain [[39,40,41,42,43,44,45,46],47,103]: 24*it(39)+1*s(5)+1*s(6)+3*s(26)+2 Such that:aux(1) =< V+1 aux(3) =< V/3 aux(163) =< V+3 s(26) =< aux(163) it(39) =< aux(3) it(39) =< aux(163) aux(2) =< aux(1)-1 s(5) =< it(39)*aux(1) s(6) =< it(39)*aux(2) with precondition: [V1=2,V>=6,3*Out>=V+6] * Chain [[39,40,41,42,43,44,45,46],47,102,103]: 24*it(39)+1*s(5)+1*s(6)+3*s(26)+4 Such that:aux(1) =< V+1 aux(3) =< V/3 aux(164) =< V+7 s(26) =< aux(164) it(39) =< aux(3) it(39) =< aux(164) aux(2) =< aux(1)-1 s(5) =< it(39)*aux(1) s(6) =< it(39)*aux(2) with precondition: [V1=2,V>=6,3*Out>=V+12] * Chain [[39,40,41,42,43,44,45,46],47,101,103]: 24*it(39)+1*s(5)+1*s(6)+3*s(26)+5 Such that:aux(1) =< V+1 aux(3) =< V/3 aux(165) =< V+9 s(26) =< aux(165) it(39) =< aux(3) it(39) =< aux(165) aux(2) =< aux(1)-1 s(5) =< it(39)*aux(1) s(6) =< it(39)*aux(2) with precondition: [V1=2,V>=6,3*Out>=V+15] * Chain [[39,40,41,42,43,44,45,46],47,100,103]: 24*it(39)+1*s(5)+1*s(6)+3*s(26)+6 Such that:aux(1) =< V+1 aux(3) =< V/3 aux(166) =< V+11 s(26) =< aux(166) it(39) =< aux(3) it(39) =< aux(166) aux(2) =< aux(1)-1 s(5) =< it(39)*aux(1) s(6) =< it(39)*aux(2) with precondition: [V1=2,V>=6,3*Out>=V+18] * Chain [[39,40,41,42,43,44,45,46],47,99,103]: 24*it(39)+1*s(5)+1*s(6)+3*s(26)+4 Such that:aux(1) =< V+1 aux(3) =< V/3 aux(167) =< V+5 s(26) =< aux(167) it(39) =< aux(3) it(39) =< aux(167) aux(2) =< aux(1)-1 s(5) =< it(39)*aux(1) s(6) =< it(39)*aux(2) with precondition: [V1=2,V>=6,3*Out>=V+9] * Chain [[39,40,41,42,43,44,45,46],47,98,103]: 24*it(39)+1*s(5)+1*s(6)+3*s(26)+4 Such that:aux(1) =< V+1 aux(3) =< V/3 aux(168) =< V+7 s(26) =< aux(168) it(39) =< aux(3) it(39) =< aux(168) aux(2) =< aux(1)-1 s(5) =< it(39)*aux(1) s(6) =< it(39)*aux(2) with precondition: [V1=2,V>=6,3*Out>=V+12] * Chain [[39,40,41,42,43,44,45,46],47,97,103]: 24*it(39)+1*s(5)+1*s(6)+3*s(26)+5 Such that:aux(1) =< V+1 aux(3) =< V/3 aux(169) =< V+9 s(26) =< aux(169) it(39) =< aux(3) it(39) =< aux(169) aux(2) =< aux(1)-1 s(5) =< it(39)*aux(1) s(6) =< it(39)*aux(2) with precondition: [V1=2,V>=6,3*Out>=V+15] * Chain [[39,40,41,42,43,44,45,46],47,96,103]: 24*it(39)+1*s(5)+1*s(6)+3*s(26)+6 Such that:aux(1) =< V+1 aux(3) =< V/3 aux(170) =< V+11 s(26) =< aux(170) it(39) =< aux(3) it(39) =< aux(170) aux(2) =< aux(1)-1 s(5) =< it(39)*aux(1) s(6) =< it(39)*aux(2) with precondition: [V1=2,V>=6,3*Out>=V+18] * Chain [[39,40,41,42,43,44,45,46],47,76,103]: 24*it(39)+1*s(5)+1*s(6)+3*s(26)+4 Such that:aux(1) =< V+1 aux(3) =< V/3 aux(171) =< V+5 s(26) =< aux(171) it(39) =< aux(3) it(39) =< aux(171) aux(2) =< aux(1)-1 s(5) =< it(39)*aux(1) s(6) =< it(39)*aux(2) with precondition: [V1=2,V>=6,3*Out>=V+9] * Chain [103]: 0 with precondition: [Out=0,V1>=0,V>=0] * Chain [102,103]: 2 with precondition: [V1=2,Out=2,V>=0] * Chain [101,103]: 3 with precondition: [V1=2,Out=3,V>=0] * Chain [100,103]: 4 with precondition: [V1=2,V=0,Out=4] * Chain [99,103]: 2 with precondition: [V1=2,V=0,Out=1] * Chain [98,103]: 2 with precondition: [V1=2,V=0,Out=2] * Chain [97,103]: 3 with precondition: [V1=2,V=0,Out=3] * Chain [96,103]: 4 with precondition: [V1=2,V=0,Out=4] * Chain [95,103]: 2 with precondition: [V1=2,V=1,Out=2] * Chain [94,103]: 3 with precondition: [V1=2,V=1,Out=3] * Chain [93,103]: 3 with precondition: [V1=2,Out=4,V>=1] * Chain [92,103]: 4 with precondition: [V1=2,Out=5,V>=1] * Chain [91,103]: 2 with precondition: [V1=2,V=1,Out=1] * Chain [91,102,103]: 4 with precondition: [V1=2,V=1,Out=3] * Chain [91,101,103]: 5 with precondition: [V1=2,V=1,Out=4] * Chain [91,100,103]: 6 with precondition: [V1=2,V=1,Out=5] * Chain [91,99,103]: 4 with precondition: [V1=2,V=1,Out=2] * Chain [91,98,103]: 4 with precondition: [V1=2,V=1,Out=3] * Chain [91,97,103]: 5 with precondition: [V1=2,V=1,Out=4] * Chain [91,96,103]: 6 with precondition: [V1=2,V=1,Out=5] * Chain [91,76,103]: 4 with precondition: [V1=2,V=1,Out=2] * Chain [90,103]: 2 with precondition: [V1=2,V=1,Out=2] * Chain [90,102,103]: 4 with precondition: [V1=2,V=1,Out=4] * Chain [90,101,103]: 5 with precondition: [V1=2,V=1,Out=5] * Chain [90,100,103]: 6 with precondition: [V1=2,V=1,Out=6] * Chain [90,99,103]: 4 with precondition: [V1=2,V=1,Out=3] * Chain [90,98,103]: 4 with precondition: [V1=2,V=1,Out=4] * Chain [90,97,103]: 5 with precondition: [V1=2,V=1,Out=5] * Chain [90,96,103]: 6 with precondition: [V1=2,V=1,Out=6] * Chain [90,76,103]: 4 with precondition: [V1=2,V=1,Out=3] * Chain [89,103]: 3 with precondition: [V1=2,V=1,Out=3] * Chain [89,102,103]: 5 with precondition: [V1=2,V=1,Out=5] * Chain [89,101,103]: 6 with precondition: [V1=2,V=1,Out=6] * Chain [89,100,103]: 7 with precondition: [V1=2,V=1,Out=7] * Chain [89,99,103]: 5 with precondition: [V1=2,V=1,Out=4] * Chain [89,98,103]: 5 with precondition: [V1=2,V=1,Out=5] * Chain [89,97,103]: 6 with precondition: [V1=2,V=1,Out=6] * Chain [89,96,103]: 7 with precondition: [V1=2,V=1,Out=7] * Chain [89,76,103]: 5 with precondition: [V1=2,V=1,Out=4] * Chain [88,103]: 3 with precondition: [V1=2,V=1,Out=4] * Chain [88,102,103]: 5 with precondition: [V1=2,V=1,Out=6] * Chain [88,101,103]: 6 with precondition: [V1=2,V=1,Out=7] * Chain [88,100,103]: 7 with precondition: [V1=2,V=1,Out=8] * Chain [88,99,103]: 5 with precondition: [V1=2,V=1,Out=5] * Chain [88,98,103]: 5 with precondition: [V1=2,V=1,Out=6] * Chain [88,97,103]: 6 with precondition: [V1=2,V=1,Out=7] * Chain [88,96,103]: 7 with precondition: [V1=2,V=1,Out=8] * Chain [88,76,103]: 5 with precondition: [V1=2,V=1,Out=5] * Chain [87,103]: 4 with precondition: [V1=2,V=1,Out=5] * Chain [87,102,103]: 6 with precondition: [V1=2,V=1,Out=7] * Chain [87,101,103]: 7 with precondition: [V1=2,V=1,Out=8] * Chain [87,100,103]: 8 with precondition: [V1=2,V=1,Out=9] * Chain [87,99,103]: 6 with precondition: [V1=2,V=1,Out=6] * Chain [87,98,103]: 6 with precondition: [V1=2,V=1,Out=7] * Chain [87,97,103]: 7 with precondition: [V1=2,V=1,Out=8] * Chain [87,96,103]: 8 with precondition: [V1=2,V=1,Out=9] * Chain [87,76,103]: 6 with precondition: [V1=2,V=1,Out=6] * Chain [86,103]: 3*s(7)+2 Such that:aux(62) =< V s(7) =< aux(62) with precondition: [V1=2,Out>=2,V+2>=2*Out] * Chain [85,103]: 3 with precondition: [V1=2,V=2,Out=3] * Chain [84,103]: 3 with precondition: [V1=2,V=2,Out=4] * Chain [83,103]: 4 with precondition: [V1=2,V=2,Out=5] * Chain [82,103]: 4 with precondition: [V1=2,Out=6,V>=2] * Chain [81,103]: 3*s(10)+2 Such that:aux(68) =< V s(10) =< aux(68) with precondition: [V1=2,Out>=2,V+2>=2*Out] * Chain [80,103]: 3 with precondition: [V1=2,Out=3,V>=2] * Chain [79,103]: 3 with precondition: [V1=2,Out=4,V>=2] * Chain [78,103]: 4 with precondition: [V1=2,Out=5,V>=2] * Chain [77,103]: 4 with precondition: [V1=2,Out=6,V>=2] * Chain [76,103]: 2 with precondition: [V1=2,Out=1,V>=0] * Chain [75,103]: 4 with precondition: [V1=2,Out=7,V>=3] * Chain [74,103]: 3*s(13)+2 Such that:aux(76) =< 2*Out s(13) =< aux(76) with precondition: [V1=2,V+3=2*Out,V>=3] * Chain [73,103]: 2 with precondition: [V1=2,Out=1,V>=3] * Chain [72,103]: 1*s(16)+2 Such that:s(16) =< V with precondition: [V1=2,V>=3,Out>=2,V+2>=2*Out] * Chain [71,103]: 3 with precondition: [V1=2,Out=3,V>=3] * Chain [70,103]: 3 with precondition: [V1=2,Out=4,V>=3] * Chain [69,103]: 4 with precondition: [V1=2,Out=5,V>=3] * Chain [68,103]: 4 with precondition: [V1=2,Out=6,V>=3] * Chain [67,103]: 4 with precondition: [V1=2,Out=7,V>=3] * Chain [66,103]: 1*s(17)+2 Such that:s(17) =< 2*Out with precondition: [V1=2,V+3=2*Out,V>=3] * Chain [65,103]: 2 with precondition: [V1=2,Out=1,V>=2] * Chain [64,103]: 4 with precondition: [V1=2,Out=7,V>=3] * Chain [63,103]: 3*s(18)+2 Such that:aux(88) =< 2*Out s(18) =< aux(88) with precondition: [V1=2,V+3=2*Out,V>=3] * Chain [62,103]: 2 with precondition: [V1=2,Out=1,V>=3] * Chain [61,103]: 1*s(21)+2 Such that:s(21) =< V with precondition: [V1=2,V>=3,Out>=2,V+2>=2*Out] * Chain [60,103]: 3 with precondition: [V1=2,Out=3,V>=3] * Chain [59,103]: 3 with precondition: [V1=2,Out=4,V>=3] * Chain [58,103]: 4 with precondition: [V1=2,Out=5,V>=3] * Chain [57,103]: 4 with precondition: [V1=2,Out=6,V>=3] * Chain [56,103]: 4 with precondition: [V1=2,Out=7,V>=3] * Chain [55,103]: 1*s(22)+2 Such that:s(22) =< 2*Out with precondition: [V1=2,V+3=2*Out,V>=3] * Chain [54,103]: 2 with precondition: [V1=2,Out=1,V>=3] * Chain [54,102,103]: 4 with precondition: [V1=2,Out=3,V>=3] * Chain [54,101,103]: 5 with precondition: [V1=2,Out=4,V>=3] * Chain [54,100,103]: 6 with precondition: [V1=2,Out=5,V>=3] * Chain [54,99,103]: 4 with precondition: [V1=2,Out=2,V>=3] * Chain [54,98,103]: 4 with precondition: [V1=2,Out=3,V>=3] * Chain [54,97,103]: 5 with precondition: [V1=2,Out=4,V>=3] * Chain [54,96,103]: 6 with precondition: [V1=2,Out=5,V>=3] * Chain [54,76,103]: 4 with precondition: [V1=2,Out=2,V>=3] * Chain [53,103]: 3*s(23)+2 Such that:aux(107) =< V s(23) =< aux(107) with precondition: [V1=2,V>=3,Out>=2,V+2>=2*Out] * Chain [53,102,103]: 3*s(23)+4 Such that:aux(107) =< V s(23) =< aux(107) with precondition: [V1=2,V>=3,Out>=4,V+6>=2*Out] * Chain [53,101,103]: 3*s(23)+5 Such that:aux(107) =< V s(23) =< aux(107) with precondition: [V1=2,V>=3,Out>=5,V+8>=2*Out] * Chain [53,100,103]: 3*s(23)+6 Such that:aux(107) =< V s(23) =< aux(107) with precondition: [V1=2,V>=3,Out>=6,V+10>=2*Out] * Chain [53,99,103]: 3*s(23)+4 Such that:aux(107) =< V s(23) =< aux(107) with precondition: [V1=2,V>=3,Out>=3,V+4>=2*Out] * Chain [53,98,103]: 3*s(23)+4 Such that:aux(107) =< V s(23) =< aux(107) with precondition: [V1=2,V>=3,Out>=4,V+6>=2*Out] * Chain [53,97,103]: 3*s(23)+5 Such that:aux(107) =< V s(23) =< aux(107) with precondition: [V1=2,V>=3,Out>=5,V+8>=2*Out] * Chain [53,96,103]: 3*s(23)+6 Such that:aux(107) =< V s(23) =< aux(107) with precondition: [V1=2,V>=3,Out>=6,V+10>=2*Out] * Chain [53,76,103]: 3*s(23)+4 Such that:aux(107) =< V s(23) =< aux(107) with precondition: [V1=2,V>=3,Out>=3,V+4>=2*Out] * Chain [52,103]: 3 with precondition: [V1=2,Out=3,V>=3] * Chain [52,102,103]: 5 with precondition: [V1=2,Out=5,V>=3] * Chain [52,101,103]: 6 with precondition: [V1=2,Out=6,V>=3] * Chain [52,100,103]: 7 with precondition: [V1=2,Out=7,V>=3] * Chain [52,99,103]: 5 with precondition: [V1=2,Out=4,V>=3] * Chain [52,98,103]: 5 with precondition: [V1=2,Out=5,V>=3] * Chain [52,97,103]: 6 with precondition: [V1=2,Out=6,V>=3] * Chain [52,96,103]: 7 with precondition: [V1=2,Out=7,V>=3] * Chain [52,76,103]: 5 with precondition: [V1=2,Out=4,V>=3] * Chain [51,103]: 3 with precondition: [V1=2,Out=4,V>=3] * Chain [51,102,103]: 5 with precondition: [V1=2,Out=6,V>=3] * Chain [51,101,103]: 6 with precondition: [V1=2,Out=7,V>=3] * Chain [51,100,103]: 7 with precondition: [V1=2,Out=8,V>=3] * Chain [51,99,103]: 5 with precondition: [V1=2,Out=5,V>=3] * Chain [51,98,103]: 5 with precondition: [V1=2,Out=6,V>=3] * Chain [51,97,103]: 6 with precondition: [V1=2,Out=7,V>=3] * Chain [51,96,103]: 7 with precondition: [V1=2,Out=8,V>=3] * Chain [51,76,103]: 5 with precondition: [V1=2,Out=5,V>=3] * Chain [50,103]: 4 with precondition: [V1=2,Out=5,V>=3] * Chain [50,102,103]: 6 with precondition: [V1=2,Out=7,V>=3] * Chain [50,101,103]: 7 with precondition: [V1=2,Out=8,V>=3] * Chain [50,100,103]: 8 with precondition: [V1=2,Out=9,V>=3] * Chain [50,99,103]: 6 with precondition: [V1=2,Out=6,V>=3] * Chain [50,98,103]: 6 with precondition: [V1=2,Out=7,V>=3] * Chain [50,97,103]: 7 with precondition: [V1=2,Out=8,V>=3] * Chain [50,96,103]: 8 with precondition: [V1=2,Out=9,V>=3] * Chain [50,76,103]: 6 with precondition: [V1=2,Out=6,V>=3] * Chain [49,103]: 4 with precondition: [V1=2,Out=6,V>=3] * Chain [49,102,103]: 6 with precondition: [V1=2,Out=8,V>=3] * Chain [49,101,103]: 7 with precondition: [V1=2,Out=9,V>=3] * Chain [49,100,103]: 8 with precondition: [V1=2,Out=10,V>=3] * Chain [49,99,103]: 6 with precondition: [V1=2,Out=7,V>=3] * Chain [49,98,103]: 6 with precondition: [V1=2,Out=8,V>=3] * Chain [49,97,103]: 7 with precondition: [V1=2,Out=9,V>=3] * Chain [49,96,103]: 8 with precondition: [V1=2,Out=10,V>=3] * Chain [49,76,103]: 6 with precondition: [V1=2,Out=7,V>=3] * Chain [48,103]: 4 with precondition: [V1=2,Out=7,V>=3] * Chain [48,102,103]: 6 with precondition: [V1=2,Out=9,V>=3] * Chain [48,101,103]: 7 with precondition: [V1=2,Out=10,V>=3] * Chain [48,100,103]: 8 with precondition: [V1=2,Out=11,V>=3] * Chain [48,99,103]: 6 with precondition: [V1=2,Out=8,V>=3] * Chain [48,98,103]: 6 with precondition: [V1=2,Out=9,V>=3] * Chain [48,97,103]: 7 with precondition: [V1=2,Out=10,V>=3] * Chain [48,96,103]: 8 with precondition: [V1=2,Out=11,V>=3] * Chain [48,76,103]: 6 with precondition: [V1=2,Out=8,V>=3] * Chain [47,103]: 3*s(26)+2 Such that:aux(162) =< 2*Out s(26) =< aux(162) with precondition: [V1=2,V+3=2*Out,V>=3] * Chain [47,102,103]: 3*s(26)+4 Such that:aux(162) =< 2*Out s(26) =< aux(162) with precondition: [V1=2,V+7=2*Out,V>=3] * Chain [47,101,103]: 3*s(26)+5 Such that:aux(162) =< 2*Out s(26) =< aux(162) with precondition: [V1=2,V+9=2*Out,V>=3] * Chain [47,100,103]: 3*s(26)+6 Such that:aux(162) =< 2*Out s(26) =< aux(162) with precondition: [V1=2,V+11=2*Out,V>=3] * Chain [47,99,103]: 3*s(26)+4 Such that:aux(162) =< 2*Out s(26) =< aux(162) with precondition: [V1=2,V+5=2*Out,V>=3] * Chain [47,98,103]: 3*s(26)+4 Such that:aux(162) =< 2*Out s(26) =< aux(162) with precondition: [V1=2,V+7=2*Out,V>=3] * Chain [47,97,103]: 3*s(26)+5 Such that:aux(162) =< 2*Out s(26) =< aux(162) with precondition: [V1=2,V+9=2*Out,V>=3] * Chain [47,96,103]: 3*s(26)+6 Such that:aux(162) =< 2*Out s(26) =< aux(162) with precondition: [V1=2,V+11=2*Out,V>=3] * Chain [47,76,103]: 3*s(26)+4 Such that:aux(162) =< 2*Out s(26) =< aux(162) with precondition: [V1=2,V+5=2*Out,V>=3] #### Cost of chains of start(V1,V): * Chain [108]: 1*s(1095)+1*s(1096)+1 Such that:s(1096) =< V1 s(1095) =< V1+1 with precondition: [V1>=0] * Chain [107]: 1 with precondition: [V1=1] * Chain [106]: 70*s(1105)+12*s(1106)+48*s(1107)+2*s(1109)+2*s(1110)+12*s(1111)+48*s(1112)+2*s(1113)+2*s(1114)+12*s(1115)+48*s(1116)+2*s(1117)+2*s(1118)+12*s(1119)+48*s(1120)+2*s(1121)+2*s(1122)+22*s(1123)+120*s(1124)+5*s(1125)+5*s(1126)+3240*s(1127)+135*s(1128)+135*s(1129)+312*s(1130)+13*s(1131)+13*s(1132)+8 Such that:s(1098) =< V+1 s(1104) =< V/3 aux(186) =< V aux(187) =< V+3 aux(188) =< V+5 aux(189) =< V+7 aux(190) =< V+9 aux(191) =< V+11 s(1105) =< aux(186) s(1106) =< aux(188) s(1107) =< s(1104) s(1107) =< aux(188) s(1108) =< s(1098)-1 s(1109) =< s(1107)*s(1098) s(1110) =< s(1107)*s(1108) s(1111) =< aux(191) s(1112) =< s(1104) s(1112) =< aux(191) s(1113) =< s(1112)*s(1098) s(1114) =< s(1112)*s(1108) s(1115) =< aux(190) s(1116) =< s(1104) s(1116) =< aux(190) s(1117) =< s(1116)*s(1098) s(1118) =< s(1116)*s(1108) s(1119) =< aux(189) s(1120) =< s(1104) s(1120) =< aux(189) s(1121) =< s(1120)*s(1098) s(1122) =< s(1120)*s(1108) s(1123) =< aux(187) s(1124) =< s(1104) s(1124) =< aux(187) s(1125) =< s(1124)*s(1098) s(1126) =< s(1124)*s(1108) s(1127) =< s(1104) s(1128) =< s(1127)*s(1098) s(1129) =< s(1127)*s(1108) s(1130) =< s(1104) s(1130) =< aux(186) s(1131) =< s(1130)*s(1098) s(1132) =< s(1130)*s(1108) with precondition: [V1=2,V>=0] * Chain [105]: 8 with precondition: [V1=2,V=1] * Chain [104]: 4 with precondition: [V1=2,V=2] Closed-form bounds of start(V1,V): ------------------------------------- * Chain [108] with precondition: [V1>=0] - Upper bound: 2*V1+2 - Complexity: n * Chain [107] with precondition: [V1=1] - Upper bound: 1 - Complexity: constant * Chain [106] with precondition: [V1=2,V>=0] - Upper bound: 70*V+8+V/3*(161*V)+V/3*(161*V+161)+(22*V+66)+(12*V+60)+(12*V+84)+(12*V+108)+(12*V+132)+1288*V - Complexity: n^2 * Chain [105] with precondition: [V1=2,V=1] - Upper bound: 8 - Complexity: constant * Chain [104] with precondition: [V1=2,V=2] - Upper bound: 4 - Complexity: constant ### Maximum cost of start(V1,V): max([2*V1+1,7,nat(V)*70+7+nat(nat(V+1)+ -1)*161*nat(V/3)+nat(V+1)*161*nat(V/3)+nat(V+3)*22+nat(V+5)*12+nat(V+7)*12+nat(V+9)*12+nat(V+11)*12+nat(V/3)*3864])+1 Asymptotic class: n^2 * Total analysis performed in 14020 ms. ---------------------------------------- (12) BOUNDS(1, n^2) ---------------------------------------- (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^2). The TRS R consists of the following rules: COND(true, z0) -> c(COND(odd(z0), p(p(p(z0)))), ODD(z0)) COND(true, z0) -> c1(COND(odd(z0), p(p(p(z0)))), P(p(p(z0))), P(p(z0)), P(z0)) ODD(0) -> c2 ODD(s(0)) -> c3 ODD(s(s(z0))) -> c4(ODD(z0)) P(0) -> c5 P(s(z0)) -> c6 The (relative) TRS S consists of the following rules: cond(true, z0) -> cond(odd(z0), p(p(p(z0)))) odd(0) -> false odd(s(0)) -> true odd(s(s(z0))) -> odd(z0) 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 ODD(s(s(z0))) ->^+ c4(ODD(z0)) gives rise to a decreasing loop by considering the right hand sides subterm at position [0]. The pumping substitution is [z0 / s(s(z0))]. 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^2). The TRS R consists of the following rules: COND(true, z0) -> c(COND(odd(z0), p(p(p(z0)))), ODD(z0)) COND(true, z0) -> c1(COND(odd(z0), p(p(p(z0)))), P(p(p(z0))), P(p(z0)), P(z0)) ODD(0) -> c2 ODD(s(0)) -> c3 ODD(s(s(z0))) -> c4(ODD(z0)) P(0) -> c5 P(s(z0)) -> c6 The (relative) TRS S consists of the following rules: cond(true, z0) -> cond(odd(z0), p(p(p(z0)))) odd(0) -> false odd(s(0)) -> true odd(s(s(z0))) -> odd(z0) 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^2). The TRS R consists of the following rules: COND(true, z0) -> c(COND(odd(z0), p(p(p(z0)))), ODD(z0)) COND(true, z0) -> c1(COND(odd(z0), p(p(p(z0)))), P(p(p(z0))), P(p(z0)), P(z0)) ODD(0) -> c2 ODD(s(0)) -> c3 ODD(s(s(z0))) -> c4(ODD(z0)) P(0) -> c5 P(s(z0)) -> c6 The (relative) TRS S consists of the following rules: cond(true, z0) -> cond(odd(z0), p(p(p(z0)))) odd(0) -> false odd(s(0)) -> true odd(s(s(z0))) -> odd(z0) p(0) -> 0 p(s(z0)) -> z0 Rewrite Strategy: INNERMOST