Abs program loaded in 7 ms. Rule based representation generated in 1 ms. Rule based representation stored in /tmp/costabs/rbr.rbr RBR properties stored in /tmp/costabs/rbr.properties Class invariants generated and loaded in 0 ms. Size abstraction not supported for native Abstract compilation performed in 2 ms. sabu_memo_table_1(case_2,[A,B,C,D,E,F,G],[1*C+ -1*F=0,1*D+ -1*G=0],0,0) sabu_memo_table_1(case_2,[A,B,C,D,E,F,G],[-1*C+1*F>=0],0,1) sabu_memo_table_1(case_2,[A,B,C,D,E,F,G],[],0,2) sabu_memo_table_1(case_1,[A,B,C,D,E,F,G],[1*A+ -1*F=0,1*B+ -1*G=0],0,0) sabu_memo_table_1(case_1,[A,B,C,D,E,F,G],[-1*A+1*F>=0],0,1) sabu_memo_table_1(case_1,[A,B,C,D,E,F,G],[],0,2) sabu_memo_table_1(not,[A,B],[1*B=1,1*A=0],0,0) sabu_memo_table_1(not,[A,B],[1*B>=0,-1*B>= -1,1*A+1*B=1],0,1) sabu_memo_table_1(case_0,[A,B,C,D,E,F],[1*E>=2],0,0) sabu_memo_table_1(eval2,[A,B,C,D,E,F],[1*E>=2],0,0) sabu_memo_table_1(start,[A,B,C,D,E,F],[1*E>=2],0,0) sabu_memo_table_1(start,[A,B],[],0,0) :- dynamic sabu_memo_table_1/5. sabu_memo_table_1(case_2, [_, _, _, _, _, _, _], [], 0, 2). sabu_memo_table_1(case_1, [_, _, _, _, _, _, _], [], 0, 2). sabu_memo_table_1(not, [B, A], [1*A>=0, -1*A>= -1, 1*B+1*A=1], 0, 1). sabu_memo_table_1(case_0, [_, _, _, _, A, _], [1*A>=2], 0, 0). sabu_memo_table_1(eval2, [_, _, _, _, A, _], [1*A>=2], 0, 0). sabu_memo_table_1(start, [_, _, _, _, A, _], [1*A>=2], 0, 0). sabu_memo_table_1(start, [_, _], [], 0, 0). Size analysis performed in 10 ms. Cost relation system stored in /tmp/costabs/crs.crs Generated 38 equations Cost relation system solved by PUBS in 530 ms. Method start terminates?: YES UB for start(a,valA,b,valB,expr) = pow(2,nat(expr)) Preprocessing Cost Relations ===================================== #### Computed strongly connected components 0. non_recursive : [and_op/2] 1. non_recursive : [case_2/6] 2. non_recursive : [case_1/6] 3. non_recursive : [neg/1] 4. non_recursive : [not/1] 5. non_recursive : [or/2] 6. recursive [non_tail,multiple] : [case_0/5,eval2/5] 8. non_recursive : [start/5] * The entry case_0/5 is not a cutpoint so it becomes a new SCC 8 Warning: the following predicates are never called:[eq/2,geq/2,gt/2,leq/2,lt/2,maxNorm/2,neq/2,start/1] #### Obtained direct recursion through partial evaluation 0. SCC is partially evaluated into and_op/2 1. SCC is partially evaluated into case_2/6 2. SCC is partially evaluated into case_1/6 3. SCC is partially evaluated into neg/1 4. SCC is completely evaluated into other SCCs 5. SCC is partially evaluated into or/2 6. SCC is partially evaluated into eval2/5 8. SCC is partially evaluated into case_0/5 Control-Flow Refinement of Cost Relations ===================================== ### Specialization of cost equations and_op/2 * CE 15 is refined into CE [25] * CE 16 is refined into CE [26] #### Refined cost equations and_op/2 * CE 25: and_op(A,B) = 0 [A=1] * CE 26: and_op(A,B) = 0 [A=0] ### Cost equations --> "Loop" of and_op/2 * CEs [25] --> Loop 25 * CEs [26] --> Loop 26 #### Loops of and_op/2 * Loop 25: and_op(A,B) [A=1] * Loop 26: and_op(A,B) [A=0] ### Ranking functions of CR and_op(A,B) #### Partial ranking functions of CR and_op(A,B) ### Resulting Chains:and_op(A,B) * [26] * [25] ### Specialization of cost equations case_2/6 * CE 22 is refined into CE [27] * CE 23 is refined into CE [28] * CE 24 is refined into CE [29] #### Refined cost equations case_2/6 * CE 27: case_2(A,B,C,D,E,F) = 2 [C>=F+1,F>=1,F+1=E] * CE 28: case_2(A,B,C,D,E,F) = 2 [F>=C+1,F>=1,F+1=E] * CE 29: case_2(A,B,C,D,E,C) = 1 [C>=1,C+1=E] ### Cost equations --> "Loop" of case_2/6 * CEs [27] --> Loop 27 * CEs [28] --> Loop 28 * CEs [29] --> Loop 29 #### Loops of case_2/6 * Loop 27: case_2(A,B,C,D,E,F) [C>=F+1,F>=1,F+1=E] * Loop 28: case_2(A,B,C,D,E,F) [F>=C+1,F>=1,F+1=E] * Loop 29: case_2(A,B,C,D,E,C) [C>=1,C+1=E] ### Ranking functions of CR case_2(A,B,C,D,E,F) #### Partial ranking functions of CR case_2(A,B,C,D,E,F) ### Resulting Chains:case_2(A,B,C,D,E,F) * [29] * [28] * [27] ### Specialization of cost equations case_1/6 * CE 19 is refined into CE [30,31,32] * CE 20 is refined into CE [33,34,35] * CE 21 is refined into CE [36] #### Refined cost equations case_1/6 * CE 30: case_1(A,B,C,D,E,C) = 2+ case_2(A,B,C,D,F,C):[29] [A>=C+1,C>=1,C+1=F,C+1=E] * CE 31: case_1(A,B,C,D,E,F) = 2+ case_2(A,B,C,D,G,F):[28] [A>=F+1,F>=C+1,F>=1,F+1=G,F+1=E] * CE 32: case_1(A,B,C,D,E,F) = 2+ case_2(A,B,C,D,G,F):[27] [C>=F+1,A>=F+1,F>=1,F+1=G,F+1=E] * CE 33: case_1(A,B,C,D,E,C) = 2+ case_2(A,B,C,D,F,C):[29] [C>=A+1,C>=1,C+1=F,C+1=E] * CE 34: case_1(A,B,C,D,E,F) = 2+ case_2(A,B,C,D,G,F):[28] [F>=C+1,F>=A+1,F>=1,F+1=G,F+1=E] * CE 35: case_1(A,B,C,D,E,F) = 2+ case_2(A,B,C,D,G,F):[27] [C>=F+1,F>=A+1,F>=1,F+1=G,F+1=E] * CE 36: case_1(A,B,C,D,E,A) = 1 [A>=1,A+1=E] ### Cost equations --> "Loop" of case_1/6 * CEs [32] --> Loop 30 * CEs [31] --> Loop 31 * CEs [35] --> Loop 32 * CEs [34] --> Loop 33 * CEs [30] --> Loop 34 * CEs [33] --> Loop 35 * CEs [36] --> Loop 36 #### Loops of case_1/6 * Loop 30: case_1(A,B,C,D,E,F) [C>=E,A>=E,E>=2,E=F+1] * Loop 31: case_1(A,B,C,D,E,F) [A>=E,E>=C+2,E>=2,E=F+1] * Loop 32: case_1(A,B,C,D,E,F) [C>=E,E>=A+2,E>=2,E=F+1] * Loop 33: case_1(A,B,C,D,E,F) [E>=C+2,E>=A+2,E>=2,E=F+1] * Loop 34: case_1(A,B,C,D,E,C) [A>=C+1,C>=1,C+1=E] * Loop 35: case_1(A,B,C,D,E,C) [C>=A+1,C>=1,C+1=E] * Loop 36: case_1(A,B,C,D,E,A) [A>=1,A+1=E] ### Ranking functions of CR case_1(A,B,C,D,E,F) #### Partial ranking functions of CR case_1(A,B,C,D,E,F) ### Resulting Chains:case_1(A,B,C,D,E,F) * [36] * [35] * [34] * [33] * [32] * [31] * [30] ### Specialization of cost equations neg/1 * CE 17 is refined into CE [37] * CE 18 is refined into CE [38] #### Refined cost equations neg/1 * CE 37: neg(A) = 0 [A=1] * CE 38: neg(A) = 0 [A=0] ### Cost equations --> "Loop" of neg/1 * CEs [37] --> Loop 37 * CEs [38] --> Loop 38 #### Loops of neg/1 * Loop 37: neg(A) [A=1] * Loop 38: neg(A) [A=0] ### Ranking functions of CR neg(A) #### Partial ranking functions of CR neg(A) ### Resulting Chains:neg(A) * [38] * [37] ### Specialization of cost equations or/2 * CE 14 is refined into CE [39] * CE 13 is refined into CE [40] #### Refined cost equations or/2 * CE 39: or(A,B) = 0 [A=1] * CE 40: or(A,B) = 0 [A=0] ### Cost equations --> "Loop" of or/2 * CEs [39] --> Loop 39 * CEs [40] --> Loop 40 #### Loops of or/2 * Loop 39: or(A,B) [A=1] * Loop 40: or(A,B) [A=0] ### Ranking functions of CR or(A,B) #### Partial ranking functions of CR or(A,B) ### Resulting Chains:or(A,B) * [40] * [39] ### Specialization of cost equations eval2/5 * CE 12 is refined into CE [41,42,43,44,45,46,47] * CE 11 is refined into CE [48,49] * CE 9 is refined into CE [50,51] * CE 7 is refined into CE [52,53] * CE 10 is refined into CE [54,55] * CE 8 is refined into CE [56,57] #### Refined cost equations eval2/5 * CE 41: eval2(A,B,C,D,E) = 3+ case_1(A,B,C,D,F,A):[36] [A>=1,A+1=F,A+1=E] * CE 42: eval2(A,B,C,D,E) = 3+ case_1(A,B,C,D,F,C):[35] [C>=A+1,C>=1,C+1=F,C+1=E] * CE 43: eval2(A,B,C,D,E) = 3+ case_1(A,B,C,D,F,C):[34] [A>=C+1,C>=1,C+1=F,C+1=E] * CE 44: eval2(A,B,C,D,E) = 3+ case_1(A,B,C,D,E,F):[33] [E>=C+2,E>=A+2,E>=2,E=F+1] * CE 45: eval2(A,B,C,D,E) = 3+ case_1(A,B,C,D,E,F):[32] [C>=E,E>=A+2,E>=2,E=F+1] * CE 46: eval2(A,B,C,D,E) = 3+ case_1(A,B,C,D,E,F):[31] [A>=E,E>=C+2,E>=2,E=F+1] * CE 47: eval2(A,B,C,D,E) = 3+ case_1(A,B,C,D,E,F):[30] [C>=E,A>=E,E>=2,E=F+1] * CE 48: eval2(A,B,C,D,E) = 6+ eval2(A,B,C,D,F)+ neg(G):[38] [F>=2,F+1=E,G=0] * CE 49: eval2(A,B,C,D,E) = 6+ eval2(A,B,C,D,F)+ neg(G):[37] [F>=2,F+1=E,G=1] * CE 50: eval2(A,B,C,D,E) = 7+ eval2(A,B,C,D,F)+ eval2(A,B,C,D,G)+ and_op(H,I):[26] [G>=F,F>=2,G+1=E,H=0] * CE 51: eval2(A,B,C,D,E) = 7+ eval2(A,B,C,D,F)+ eval2(A,B,C,D,G)+ and_op(H,I):[25] [G>=F,F>=2,G+1=E,H=1] * CE 52: eval2(A,B,C,D,E) = 8+ eval2(A,B,C,D,F)+ eval2(A,B,C,D,G)+ or(H,I):[40] [G>=F,F>=2,G+1=E,H=0] * CE 53: eval2(A,B,C,D,E) = 8+ eval2(A,B,C,D,F)+ eval2(A,B,C,D,G)+ or(H,I):[39] [G>=F,F>=2,G+1=E,H=1] * CE 54: eval2(A,B,C,D,E) = 7+ eval2(A,B,C,D,F)+ eval2(A,B,C,D,G)+ and_op(H,I):[26] [F>=G,G>=2,F+1=E,H=0] * CE 55: eval2(A,B,C,D,E) = 7+ eval2(A,B,C,D,F)+ eval2(A,B,C,D,G)+ and_op(H,I):[25] [F>=G,G>=2,F+1=E,H=1] * CE 56: eval2(A,B,C,D,E) = 8+ eval2(A,B,C,D,F)+ eval2(A,B,C,D,G)+ or(H,I):[40] [F>=G,G>=2,F+1=E,H=0] * CE 57: eval2(A,B,C,D,E) = 8+ eval2(A,B,C,D,F)+ eval2(A,B,C,D,G)+ or(H,I):[39] [F>=G,G>=2,F+1=E,H=1] ### Cost equations --> "Loop" of eval2/5 * CEs [53] --> Loop 41 * CEs [52] --> Loop 42 * CEs [51] --> Loop 43 * CEs [50] --> Loop 44 * CEs [57] --> Loop 45 * CEs [56] --> Loop 46 * CEs [55] --> Loop 47 * CEs [54] --> Loop 48 * CEs [49] --> Loop 49 * CEs [48] --> Loop 50 * CEs [47] --> Loop 51 * CEs [46] --> Loop 52 * CEs [45] --> Loop 53 * CEs [44] --> Loop 54 * CEs [42] --> Loop 55 * CEs [41] --> Loop 56 * CEs [43] --> Loop 57 #### Loops of eval2/5 * Loop 41: eval2(A,B,C,D,E)-> eval2(A,B,C,D,E') eval2(A,B,C,D,E'2) [E'2>=E',E'>=2,E'2+1=E] * Loop 42: eval2(A,B,C,D,E)-> eval2(A,B,C,D,E') eval2(A,B,C,D,E'2) [E'2>=E',E'>=2,E'2+1=E] * Loop 43: eval2(A,B,C,D,E)-> eval2(A,B,C,D,E') eval2(A,B,C,D,E'2) [E'2>=E',E'>=2,E'2+1=E] * Loop 44: eval2(A,B,C,D,E)-> eval2(A,B,C,D,E') eval2(A,B,C,D,E'2) [E'2>=E',E'>=2,E'2+1=E] * Loop 45: eval2(A,B,C,D,E)-> eval2(A,B,C,D,E') eval2(A,B,C,D,E'2) [E'>=E'2,E'2>=2,E'+1=E] * Loop 46: eval2(A,B,C,D,E)-> eval2(A,B,C,D,E') eval2(A,B,C,D,E'2) [E'>=E'2,E'2>=2,E'+1=E] * Loop 47: eval2(A,B,C,D,E)-> eval2(A,B,C,D,E') eval2(A,B,C,D,E'2) [E'>=E'2,E'2>=2,E'+1=E] * Loop 48: eval2(A,B,C,D,E)-> eval2(A,B,C,D,E') eval2(A,B,C,D,E'2) [E'>=E'2,E'2>=2,E'+1=E] * Loop 49: eval2(A,B,C,D,E)-> eval2(A,B,C,D,E') [E'>=2,E'+1=E] * Loop 50: eval2(A,B,C,D,E)-> eval2(A,B,C,D,E') [E'>=2,E'+1=E] * Loop 51: eval2(A,B,C,D,E) [C>=E,A>=E,E>=2] * Loop 52: eval2(A,B,C,D,E) [A>=E,E>=C+2,E>=2] * Loop 53: eval2(A,B,C,D,E) [C>=E,E>=A+2,E>=2] * Loop 54: eval2(A,B,C,D,E) [E>=C+2,E>=A+2,E>=2] * Loop 55: eval2(A,B,C,D,E) [C>=A+1,C>=1,C+1=E] * Loop 56: eval2(A,B,C,D,E) [A>=1,A+1=E] * Loop 57: eval2(A,B,C,D,E) [A>=E,E>=2,E=C+1] ### Ranking functions of CR eval2(A,B,C,D,E) * RF of phase [41,42,43,44,45,46,47,48,49,50]: [E-2] #### Partial ranking functions of CR eval2(A,B,C,D,E) * Partial RF of phase [41,42,43,44,45,46,47,48,49,50]: - RF of loop [41:1,41:2,42:1,42:2,43:1,43:2,44:1,44:2,45:1,45:2,46:1,46:2,47:1,47:2,48:1,48:2,49:1,50:1]: E-2 ### Resulting Chains:eval2(A,B,C,D,E) * [57] * [56] * [55] * [54] * [53] * [52] * [51] * [multiple([41,42,43,44,45,46,47,48,49,50],[[57],[56],[55],[54],[53],[52],[51]])] ### Specialization of cost equations case_0/5 * CE 5 is refined into CE [58,59,60,61,62,63,64,65,66,67,68,69,70,71,72,73] * CE 4 is refined into CE [74,75,76,77,78,79,80,81,82,83,84,85,86,87,88,89,90,91,92,93,94,95,96,97,98,99,100,101,102,103,104,105,106,107,108,109,110,111,112,113,114,115,116,117,118,119,120,121,122,123,124,125,126,127,128,129,130,131,132,133,134,135,136,137,138,139,140,141,142,143,144,145,146,147,148,149,150,151] * CE 3 is refined into CE [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] * CE 2 is refined into CE [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] * CE 1 is refined into CE [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] * CE 6 is refined into CE [386,387,388,389,390,391,392] #### Refined cost equations case_0/5 * CE 58: case_0(A,B,C,D,E) = 5+ eval2(A,B,C,D,F):[57]+ neg(G):[38] [A>=C+1,C>=1,C+1=F,C+2=E,G=0] * CE 59: case_0(A,B,C,D,E) = 5+ eval2(A,B,C,D,F):[57]+ neg(G):[37] [A>=C+1,C>=1,C+1=F,C+2=E,G=1] * CE 60: case_0(A,B,C,D,E) = 5+ eval2(A,B,C,D,F):[56]+ neg(G):[38] [A>=1,A+1=F,A+2=E,G=0] * CE 61: case_0(A,B,C,D,E) = 5+ eval2(A,B,C,D,F):[56]+ neg(G):[37] [A>=1,A+1=F,A+2=E,G=1] * CE 62: case_0(A,B,C,D,E) = 5+ eval2(A,B,C,D,F):[55]+ neg(G):[38] [C>=A+1,C>=1,C+1=F,C+2=E,G=0] * CE 63: case_0(A,B,C,D,E) = 5+ eval2(A,B,C,D,F):[55]+ neg(G):[37] [C>=A+1,C>=1,C+1=F,C+2=E,G=1] * CE 64: case_0(A,B,C,D,E) = 5+ eval2(A,B,C,D,F):[54]+ neg(G):[38] [F>=C+2,F>=A+2,F>=2,F+1=E,G=0] * CE 65: case_0(A,B,C,D,E) = 5+ eval2(A,B,C,D,F):[54]+ neg(G):[37] [F>=C+2,F>=A+2,F>=2,F+1=E,G=1] * CE 66: case_0(A,B,C,D,E) = 5+ eval2(A,B,C,D,F):[53]+ neg(G):[38] [C>=F,F>=A+2,F>=2,F+1=E,G=0] * CE 67: case_0(A,B,C,D,E) = 5+ eval2(A,B,C,D,F):[53]+ neg(G):[37] [C>=F,F>=A+2,F>=2,F+1=E,G=1] * CE 68: case_0(A,B,C,D,E) = 5+ eval2(A,B,C,D,F):[52]+ neg(G):[38] [A>=F,F>=C+2,F>=2,F+1=E,G=0] * CE 69: case_0(A,B,C,D,E) = 5+ eval2(A,B,C,D,F):[52]+ neg(G):[37] [A>=F,F>=C+2,F>=2,F+1=E,G=1] * CE 70: case_0(A,B,C,D,E) = 5+ eval2(A,B,C,D,F):[51]+ neg(G):[38] [C>=F,A>=F,F>=2,F+1=E,G=0] * CE 71: case_0(A,B,C,D,E) = 5+ eval2(A,B,C,D,F):[51]+ neg(G):[37] [C>=F,A>=F,F>=2,F+1=E,G=1] * CE 72: case_0(A,B,C,D,E) = 5+ eval2(A,B,C,D,F):[multiple([41,42,43,44,45,46,47,48,49,50],[[57],[56],[55],[54],[53],[52],[51]])]+ neg(G):[38] [F>=3,F+1=E,G=0] * CE 73: case_0(A,B,C,D,E) = 5+ eval2(A,B,C,D,F):[multiple([41,42,43,44,45,46,47,48,49,50],[[57],[56],[55],[54],[53],[52],[51]])]+ neg(G):[37] [F>=3,F+1=E,G=1] * CE 74: case_0(A,B,C,D,E) = 6+ eval2(A,B,C,D,F):[57]+ eval2(A,B,C,D,G):[57]+ and_op(H,I):[26] [A>=C+1,C>=1,C+1=G,C+1=F,C+2=E,H=0] * CE 75: case_0(A,B,C,D,E) = 6+ eval2(A,B,C,D,F):[57]+ eval2(A,B,C,D,G):[57]+ and_op(H,I):[25] [A>=C+1,C>=1,C+1=G,C+1=F,C+2=E,H=1] * CE 76: case_0(A,B,C,D,E) = 6+ eval2(A,B,C,D,F):[57]+ eval2(A,B,C,D,G):[51]+ and_op(H,I):[26] [C>=G,A>=C+1,G>=2,C+1=F,C+2=E,H=0] * CE 77: case_0(A,B,C,D,E) = 6+ eval2(A,B,C,D,F):[57]+ eval2(A,B,C,D,G):[51]+ and_op(H,I):[25] [C>=G,A>=C+1,G>=2,C+1=F,C+2=E,H=1] * CE 78: case_0(A,B,C,D,E) = 6+ eval2(A,B,C,D,F):[57]+ eval2(A,B,C,D,G):[multiple([41,42,43,44,45,46,47,48,49,50],[[57],[56],[55],[54],[53],[52],[51]])]+ and_op(H,I):[26] [C+1>=G,A>=C+1,G>=3,C+1=F,C+2=E,H=0] * CE 79: case_0(A,B,C,D,E) = 6+ eval2(A,B,C,D,F):[57]+ eval2(A,B,C,D,G):[multiple([41,42,43,44,45,46,47,48,49,50],[[57],[56],[55],[54],[53],[52],[51]])]+ and_op(H,I):[25] [C+1>=G,A>=C+1,G>=3,C+1=F,C+2=E,H=1] * CE 80: case_0(A,B,C,D,E) = 6+ eval2(A,B,C,D,F):[56]+ eval2(A,B,C,D,G):[57]+ and_op(H,I):[26] [A>=C+1,C>=1,C+1=G,A+1=F,A+2=E,H=0] * CE 81: case_0(A,B,C,D,E) = 6+ eval2(A,B,C,D,F):[56]+ eval2(A,B,C,D,G):[57]+ and_op(H,I):[25] [A>=C+1,C>=1,C+1=G,A+1=F,A+2=E,H=1] * CE 82: case_0(A,B,C,D,E) = 6+ eval2(A,B,C,D,F):[56]+ eval2(A,B,C,D,G):[56]+ and_op(H,I):[26] [A>=1,A+1=G,A+1=F,A+2=E,H=0] * CE 83: case_0(A,B,C,D,E) = 6+ eval2(A,B,C,D,F):[56]+ eval2(A,B,C,D,G):[56]+ and_op(H,I):[25] [A>=1,A+1=G,A+1=F,A+2=E,H=1] * CE 84: case_0(A,B,C,D,E) = 6+ eval2(A,B,C,D,F):[56]+ eval2(A,B,C,D,G):[52]+ and_op(H,I):[26] [A>=G,G>=C+2,G>=2,A+1=F,A+2=E,H=0] * CE 85: case_0(A,B,C,D,E) = 6+ eval2(A,B,C,D,F):[56]+ eval2(A,B,C,D,G):[52]+ and_op(H,I):[25] [A>=G,G>=C+2,G>=2,A+1=F,A+2=E,H=1] * CE 86: case_0(A,B,C,D,E) = 6+ eval2(A,B,C,D,F):[56]+ eval2(A,B,C,D,G):[51]+ and_op(H,I):[26] [C>=G,A>=G,G>=2,A+1=F,A+2=E,H=0] * CE 87: case_0(A,B,C,D,E) = 6+ eval2(A,B,C,D,F):[56]+ eval2(A,B,C,D,G):[51]+ and_op(H,I):[25] [C>=G,A>=G,G>=2,A+1=F,A+2=E,H=1] * CE 88: case_0(A,B,C,D,E) = 6+ eval2(A,B,C,D,F):[56]+ eval2(A,B,C,D,G):[multiple([41,42,43,44,45,46,47,48,49,50],[[57],[56],[55],[54],[53],[52],[51]])]+ and_op(H,I):[26] [A+1>=G,G>=3,A+1=F,A+2=E,H=0] * CE 89: case_0(A,B,C,D,E) = 6+ eval2(A,B,C,D,F):[56]+ eval2(A,B,C,D,G):[multiple([41,42,43,44,45,46,47,48,49,50],[[57],[56],[55],[54],[53],[52],[51]])]+ and_op(H,I):[25] [A+1>=G,G>=3,A+1=F,A+2=E,H=1] * CE 90: case_0(A,B,C,D,E) = 6+ eval2(A,B,C,D,F):[55]+ eval2(A,B,C,D,G):[56]+ and_op(H,I):[26] [C>=A+1,A>=1,A+1=G,C+1=F,C+2=E,H=0] * CE 91: case_0(A,B,C,D,E) = 6+ eval2(A,B,C,D,F):[55]+ eval2(A,B,C,D,G):[56]+ and_op(H,I):[25] [C>=A+1,A>=1,A+1=G,C+1=F,C+2=E,H=1] * CE 92: case_0(A,B,C,D,E) = 6+ eval2(A,B,C,D,F):[55]+ eval2(A,B,C,D,G):[55]+ and_op(H,I):[26] [C>=A+1,C>=1,C+1=G,C+1=F,C+2=E,H=0] * CE 93: case_0(A,B,C,D,E) = 6+ eval2(A,B,C,D,F):[55]+ eval2(A,B,C,D,G):[55]+ and_op(H,I):[25] [C>=A+1,C>=1,C+1=G,C+1=F,C+2=E,H=1] * CE 94: case_0(A,B,C,D,E) = 6+ eval2(A,B,C,D,F):[55]+ eval2(A,B,C,D,G):[53]+ and_op(H,I):[26] [C>=G,G>=A+2,G>=2,C+1=F,C+2=E,H=0] * CE 95: case_0(A,B,C,D,E) = 6+ eval2(A,B,C,D,F):[55]+ eval2(A,B,C,D,G):[53]+ and_op(H,I):[25] [C>=G,G>=A+2,G>=2,C+1=F,C+2=E,H=1] * CE 96: case_0(A,B,C,D,E) = 6+ eval2(A,B,C,D,F):[55]+ eval2(A,B,C,D,G):[51]+ and_op(H,I):[26] [A>=G,C>=A+1,G>=2,C+1=F,C+2=E,H=0] * CE 97: case_0(A,B,C,D,E) = 6+ eval2(A,B,C,D,F):[55]+ eval2(A,B,C,D,G):[51]+ and_op(H,I):[25] [A>=G,C>=A+1,G>=2,C+1=F,C+2=E,H=1] * CE 98: case_0(A,B,C,D,E) = 6+ eval2(A,B,C,D,F):[55]+ eval2(A,B,C,D,G):[multiple([41,42,43,44,45,46,47,48,49,50],[[57],[56],[55],[54],[53],[52],[51]])]+ and_op(H,I):[26] [C+1>=G,C>=A+1,G>=3,C+1=F,C+2=E,H=0] * CE 99: case_0(A,B,C,D,E) = 6+ eval2(A,B,C,D,F):[55]+ eval2(A,B,C,D,G):[multiple([41,42,43,44,45,46,47,48,49,50],[[57],[56],[55],[54],[53],[52],[51]])]+ and_op(H,I):[25] [C+1>=G,C>=A+1,G>=3,C+1=F,C+2=E,H=1] * CE 100: case_0(A,B,C,D,E) = 6+ eval2(A,B,C,D,F):[54]+ eval2(A,B,C,D,G):[57]+ and_op(H,I):[26] [A>=C+1,F>=A+2,C>=1,C+1=G,F+1=E,H=0] * CE 101: case_0(A,B,C,D,E) = 6+ eval2(A,B,C,D,F):[54]+ eval2(A,B,C,D,G):[57]+ and_op(H,I):[25] [A>=C+1,F>=A+2,C>=1,C+1=G,F+1=E,H=1] * CE 102: case_0(A,B,C,D,E) = 6+ eval2(A,B,C,D,F):[54]+ eval2(A,B,C,D,G):[56]+ and_op(H,I):[26] [F>=A+2,F>=C+2,A>=1,A+1=G,F+1=E,H=0] * CE 103: case_0(A,B,C,D,E) = 6+ eval2(A,B,C,D,F):[54]+ eval2(A,B,C,D,G):[56]+ and_op(H,I):[25] [F>=A+2,F>=C+2,A>=1,A+1=G,F+1=E,H=1] * CE 104: case_0(A,B,C,D,E) = 6+ eval2(A,B,C,D,F):[54]+ eval2(A,B,C,D,G):[55]+ and_op(H,I):[26] [F>=C+2,C>=A+1,C>=1,C+1=G,F+1=E,H=0] * CE 105: case_0(A,B,C,D,E) = 6+ eval2(A,B,C,D,F):[54]+ eval2(A,B,C,D,G):[55]+ and_op(H,I):[25] [F>=C+2,C>=A+1,C>=1,C+1=G,F+1=E,H=1] * CE 106: case_0(A,B,C,D,E) = 6+ eval2(A,B,C,D,F):[54]+ eval2(A,B,C,D,G):[54]+ and_op(H,I):[26] [F>=G,G>=C+2,G>=A+2,G>=2,F+1=E,H=0] * CE 107: case_0(A,B,C,D,E) = 6+ eval2(A,B,C,D,F):[54]+ eval2(A,B,C,D,G):[54]+ and_op(H,I):[25] [F>=G,G>=C+2,G>=A+2,G>=2,F+1=E,H=1] * CE 108: case_0(A,B,C,D,E) = 6+ eval2(A,B,C,D,F):[54]+ eval2(A,B,C,D,G):[53]+ and_op(H,I):[26] [C>=G,F>=C+2,G>=A+2,G>=2,F+1=E,H=0] * CE 109: case_0(A,B,C,D,E) = 6+ eval2(A,B,C,D,F):[54]+ eval2(A,B,C,D,G):[53]+ and_op(H,I):[25] [C>=G,F>=C+2,G>=A+2,G>=2,F+1=E,H=1] * CE 110: case_0(A,B,C,D,E) = 6+ eval2(A,B,C,D,F):[54]+ eval2(A,B,C,D,G):[52]+ and_op(H,I):[26] [A>=G,G>=C+2,F>=A+2,G>=2,F+1=E,H=0] * CE 111: case_0(A,B,C,D,E) = 6+ eval2(A,B,C,D,F):[54]+ eval2(A,B,C,D,G):[52]+ and_op(H,I):[25] [A>=G,G>=C+2,F>=A+2,G>=2,F+1=E,H=1] * CE 112: case_0(A,B,C,D,E) = 6+ eval2(A,B,C,D,F):[54]+ eval2(A,B,C,D,G):[51]+ and_op(H,I):[26] [C>=G,A>=G,F>=C+2,F>=A+2,G>=2,F+1=E,H=0] * CE 113: case_0(A,B,C,D,E) = 6+ eval2(A,B,C,D,F):[54]+ eval2(A,B,C,D,G):[51]+ and_op(H,I):[25] [C>=G,A>=G,F>=C+2,F>=A+2,G>=2,F+1=E,H=1] * CE 114: case_0(A,B,C,D,E) = 6+ eval2(A,B,C,D,F):[54]+ eval2(A,B,C,D,G):[multiple([41,42,43,44,45,46,47,48,49,50],[[57],[56],[55],[54],[53],[52],[51]])]+ and_op(H,I):[26] [F>=G,F>=C+2,F>=A+2,G>=3,F+1=E,H=0] * CE 115: case_0(A,B,C,D,E) = 6+ eval2(A,B,C,D,F):[54]+ eval2(A,B,C,D,G):[multiple([41,42,43,44,45,46,47,48,49,50],[[57],[56],[55],[54],[53],[52],[51]])]+ and_op(H,I):[25] [F>=G,F>=C+2,F>=A+2,G>=3,F+1=E,H=1] * CE 116: case_0(A,B,C,D,E) = 6+ eval2(A,B,C,D,F):[53]+ eval2(A,B,C,D,G):[56]+ and_op(H,I):[26] [F>=A+2,C>=F,A>=1,A+1=G,F+1=E,H=0] * CE 117: case_0(A,B,C,D,E) = 6+ eval2(A,B,C,D,F):[53]+ eval2(A,B,C,D,G):[56]+ and_op(H,I):[25] [F>=A+2,C>=F,A>=1,A+1=G,F+1=E,H=1] * CE 118: case_0(A,B,C,D,E) = 6+ eval2(A,B,C,D,F):[53]+ eval2(A,B,C,D,G):[53]+ and_op(H,I):[26] [F>=G,G>=A+2,C>=F,G>=2,F+1=E,H=0] * CE 119: case_0(A,B,C,D,E) = 6+ eval2(A,B,C,D,F):[53]+ eval2(A,B,C,D,G):[53]+ and_op(H,I):[25] [F>=G,G>=A+2,C>=F,G>=2,F+1=E,H=1] * CE 120: case_0(A,B,C,D,E) = 6+ eval2(A,B,C,D,F):[53]+ eval2(A,B,C,D,G):[51]+ and_op(H,I):[26] [A>=G,F>=A+2,C>=F,G>=2,F+1=E,H=0] * CE 121: case_0(A,B,C,D,E) = 6+ eval2(A,B,C,D,F):[53]+ eval2(A,B,C,D,G):[51]+ and_op(H,I):[25] [A>=G,F>=A+2,C>=F,G>=2,F+1=E,H=1] * CE 122: case_0(A,B,C,D,E) = 6+ eval2(A,B,C,D,F):[53]+ eval2(A,B,C,D,G):[multiple([41,42,43,44,45,46,47,48,49,50],[[57],[56],[55],[54],[53],[52],[51]])]+ and_op(H,I):[26] [F>=G,C>=F,F>=A+2,G>=3,F+1=E,H=0] * CE 123: case_0(A,B,C,D,E) = 6+ eval2(A,B,C,D,F):[53]+ eval2(A,B,C,D,G):[multiple([41,42,43,44,45,46,47,48,49,50],[[57],[56],[55],[54],[53],[52],[51]])]+ and_op(H,I):[25] [F>=G,C>=F,F>=A+2,G>=3,F+1=E,H=1] * CE 124: case_0(A,B,C,D,E) = 6+ eval2(A,B,C,D,F):[52]+ eval2(A,B,C,D,G):[57]+ and_op(H,I):[26] [F>=C+2,A>=F,C>=1,C+1=G,F+1=E,H=0] * CE 125: case_0(A,B,C,D,E) = 6+ eval2(A,B,C,D,F):[52]+ eval2(A,B,C,D,G):[57]+ and_op(H,I):[25] [F>=C+2,A>=F,C>=1,C+1=G,F+1=E,H=1] * CE 126: case_0(A,B,C,D,E) = 6+ eval2(A,B,C,D,F):[52]+ eval2(A,B,C,D,G):[52]+ and_op(H,I):[26] [F>=G,G>=C+2,A>=F,G>=2,F+1=E,H=0] * CE 127: case_0(A,B,C,D,E) = 6+ eval2(A,B,C,D,F):[52]+ eval2(A,B,C,D,G):[52]+ and_op(H,I):[25] [F>=G,G>=C+2,A>=F,G>=2,F+1=E,H=1] * CE 128: case_0(A,B,C,D,E) = 6+ eval2(A,B,C,D,F):[52]+ eval2(A,B,C,D,G):[51]+ and_op(H,I):[26] [C>=G,F>=C+2,A>=F,G>=2,F+1=E,H=0] * CE 129: case_0(A,B,C,D,E) = 6+ eval2(A,B,C,D,F):[52]+ eval2(A,B,C,D,G):[51]+ and_op(H,I):[25] [C>=G,F>=C+2,A>=F,G>=2,F+1=E,H=1] * CE 130: case_0(A,B,C,D,E) = 6+ eval2(A,B,C,D,F):[52]+ eval2(A,B,C,D,G):[multiple([41,42,43,44,45,46,47,48,49,50],[[57],[56],[55],[54],[53],[52],[51]])]+ and_op(H,I):[26] [F>=G,A>=F,F>=C+2,G>=3,F+1=E,H=0] * CE 131: case_0(A,B,C,D,E) = 6+ eval2(A,B,C,D,F):[52]+ eval2(A,B,C,D,G):[multiple([41,42,43,44,45,46,47,48,49,50],[[57],[56],[55],[54],[53],[52],[51]])]+ and_op(H,I):[25] [F>=G,A>=F,F>=C+2,G>=3,F+1=E,H=1] * CE 132: case_0(A,B,C,D,E) = 6+ eval2(A,B,C,D,F):[51]+ eval2(A,B,C,D,G):[51]+ and_op(H,I):[26] [F>=G,C>=F,A>=F,G>=2,F+1=E,H=0] * CE 133: case_0(A,B,C,D,E) = 6+ eval2(A,B,C,D,F):[51]+ eval2(A,B,C,D,G):[51]+ and_op(H,I):[25] [F>=G,C>=F,A>=F,G>=2,F+1=E,H=1] * CE 134: case_0(A,B,C,D,E) = 6+ eval2(A,B,C,D,F):[51]+ eval2(A,B,C,D,G):[multiple([41,42,43,44,45,46,47,48,49,50],[[57],[56],[55],[54],[53],[52],[51]])]+ and_op(H,I):[26] [F>=G,C>=F,A>=F,G>=3,F+1=E,H=0] * CE 135: case_0(A,B,C,D,E) = 6+ eval2(A,B,C,D,F):[51]+ eval2(A,B,C,D,G):[multiple([41,42,43,44,45,46,47,48,49,50],[[57],[56],[55],[54],[53],[52],[51]])]+ and_op(H,I):[25] [F>=G,C>=F,A>=F,G>=3,F+1=E,H=1] * CE 136: case_0(A,B,C,D,E) = 6+ eval2(A,B,C,D,F):[multiple([41,42,43,44,45,46,47,48,49,50],[[57],[56],[55],[54],[53],[52],[51]])]+ eval2(A,B,C,D,G):[57]+ and_op(H,I):[26] [A>=C+1,F>=C+1,C>=1,F>=3,C+1=G,F+1=E,H=0] * CE 137: case_0(A,B,C,D,E) = 6+ eval2(A,B,C,D,F):[multiple([41,42,43,44,45,46,47,48,49,50],[[57],[56],[55],[54],[53],[52],[51]])]+ eval2(A,B,C,D,G):[57]+ and_op(H,I):[25] [A>=C+1,F>=C+1,C>=1,F>=3,C+1=G,F+1=E,H=1] * CE 138: case_0(A,B,C,D,E) = 6+ eval2(A,B,C,D,F):[multiple([41,42,43,44,45,46,47,48,49,50],[[57],[56],[55],[54],[53],[52],[51]])]+ eval2(A,B,C,D,G):[56]+ and_op(H,I):[26] [F>=A+1,A>=1,F>=3,A+1=G,F+1=E,H=0] * CE 139: case_0(A,B,C,D,E) = 6+ eval2(A,B,C,D,F):[multiple([41,42,43,44,45,46,47,48,49,50],[[57],[56],[55],[54],[53],[52],[51]])]+ eval2(A,B,C,D,G):[56]+ and_op(H,I):[25] [F>=A+1,A>=1,F>=3,A+1=G,F+1=E,H=1] * CE 140: case_0(A,B,C,D,E) = 6+ eval2(A,B,C,D,F):[multiple([41,42,43,44,45,46,47,48,49,50],[[57],[56],[55],[54],[53],[52],[51]])]+ eval2(A,B,C,D,G):[55]+ and_op(H,I):[26] [F>=C+1,C>=A+1,C>=1,F>=3,C+1=G,F+1=E,H=0] * CE 141: case_0(A,B,C,D,E) = 6+ eval2(A,B,C,D,F):[multiple([41,42,43,44,45,46,47,48,49,50],[[57],[56],[55],[54],[53],[52],[51]])]+ eval2(A,B,C,D,G):[55]+ and_op(H,I):[25] [F>=C+1,C>=A+1,C>=1,F>=3,C+1=G,F+1=E,H=1] * CE 142: case_0(A,B,C,D,E) = 6+ eval2(A,B,C,D,F):[multiple([41,42,43,44,45,46,47,48,49,50],[[57],[56],[55],[54],[53],[52],[51]])]+ eval2(A,B,C,D,G):[54]+ and_op(H,I):[26] [F>=G,G>=C+2,G>=A+2,G>=2,F>=3,F+1=E,H=0] * CE 143: case_0(A,B,C,D,E) = 6+ eval2(A,B,C,D,F):[multiple([41,42,43,44,45,46,47,48,49,50],[[57],[56],[55],[54],[53],[52],[51]])]+ eval2(A,B,C,D,G):[54]+ and_op(H,I):[25] [F>=G,G>=C+2,G>=A+2,G>=2,F>=3,F+1=E,H=1] * CE 144: case_0(A,B,C,D,E) = 6+ eval2(A,B,C,D,F):[multiple([41,42,43,44,45,46,47,48,49,50],[[57],[56],[55],[54],[53],[52],[51]])]+ eval2(A,B,C,D,G):[53]+ and_op(H,I):[26] [C>=G,F>=G,G>=A+2,G>=2,F>=3,F+1=E,H=0] * CE 145: case_0(A,B,C,D,E) = 6+ eval2(A,B,C,D,F):[multiple([41,42,43,44,45,46,47,48,49,50],[[57],[56],[55],[54],[53],[52],[51]])]+ eval2(A,B,C,D,G):[53]+ and_op(H,I):[25] [C>=G,F>=G,G>=A+2,G>=2,F>=3,F+1=E,H=1] * CE 146: case_0(A,B,C,D,E) = 6+ eval2(A,B,C,D,F):[multiple([41,42,43,44,45,46,47,48,49,50],[[57],[56],[55],[54],[53],[52],[51]])]+ eval2(A,B,C,D,G):[52]+ and_op(H,I):[26] [A>=G,F>=G,G>=C+2,G>=2,F>=3,F+1=E,H=0] * CE 147: case_0(A,B,C,D,E) = 6+ eval2(A,B,C,D,F):[multiple([41,42,43,44,45,46,47,48,49,50],[[57],[56],[55],[54],[53],[52],[51]])]+ eval2(A,B,C,D,G):[52]+ and_op(H,I):[25] [A>=G,F>=G,G>=C+2,G>=2,F>=3,F+1=E,H=1] * CE 148: case_0(A,B,C,D,E) = 6+ eval2(A,B,C,D,F):[multiple([41,42,43,44,45,46,47,48,49,50],[[57],[56],[55],[54],[53],[52],[51]])]+ eval2(A,B,C,D,G):[51]+ and_op(H,I):[26] [C>=G,A>=G,F>=G,G>=2,F>=3,F+1=E,H=0] * CE 149: case_0(A,B,C,D,E) = 6+ eval2(A,B,C,D,F):[multiple([41,42,43,44,45,46,47,48,49,50],[[57],[56],[55],[54],[53],[52],[51]])]+ eval2(A,B,C,D,G):[51]+ and_op(H,I):[25] [C>=G,A>=G,F>=G,G>=2,F>=3,F+1=E,H=1] * CE 150: case_0(A,B,C,D,E) = 6+ eval2(A,B,C,D,F):[multiple([41,42,43,44,45,46,47,48,49,50],[[57],[56],[55],[54],[53],[52],[51]])]+ eval2(A,B,C,D,G):[multiple([41,42,43,44,45,46,47,48,49,50],[[57],[56],[55],[54],[53],[52],[51]])]+ and_op(H,I):[26] [F>=G,G>=3,F+1=E,H=0] * CE 151: case_0(A,B,C,D,E) = 6+ eval2(A,B,C,D,F):[multiple([41,42,43,44,45,46,47,48,49,50],[[57],[56],[55],[54],[53],[52],[51]])]+ eval2(A,B,C,D,G):[multiple([41,42,43,44,45,46,47,48,49,50],[[57],[56],[55],[54],[53],[52],[51]])]+ and_op(H,I):[25] [F>=G,G>=3,F+1=E,H=1] * CE 152: case_0(A,B,C,D,E) = 6+ eval2(A,B,C,D,F):[57]+ eval2(A,B,C,D,G):[57]+ and_op(H,I):[26] [A>=C+1,C>=1,C+1=G,C+1=F,C+2=E,H=0] * CE 153: case_0(A,B,C,D,E) = 6+ eval2(A,B,C,D,F):[57]+ eval2(A,B,C,D,G):[57]+ and_op(H,I):[25] [A>=C+1,C>=1,C+1=G,C+1=F,C+2=E,H=1] * CE 154: case_0(A,B,C,D,E) = 6+ eval2(A,B,C,D,F):[57]+ eval2(A,B,C,D,G):[56]+ and_op(H,I):[26] [A>=C+1,C>=1,A+1=G,C+1=F,A+2=E,H=0] * CE 155: case_0(A,B,C,D,E) = 6+ eval2(A,B,C,D,F):[57]+ eval2(A,B,C,D,G):[56]+ and_op(H,I):[25] [A>=C+1,C>=1,A+1=G,C+1=F,A+2=E,H=1] * CE 156: case_0(A,B,C,D,E) = 6+ eval2(A,B,C,D,F):[57]+ eval2(A,B,C,D,G):[54]+ and_op(H,I):[26] [A>=C+1,G>=A+2,C>=1,C+1=F,G+1=E,H=0] * CE 157: case_0(A,B,C,D,E) = 6+ eval2(A,B,C,D,F):[57]+ eval2(A,B,C,D,G):[54]+ and_op(H,I):[25] [A>=C+1,G>=A+2,C>=1,C+1=F,G+1=E,H=1] * CE 158: case_0(A,B,C,D,E) = 6+ eval2(A,B,C,D,F):[57]+ eval2(A,B,C,D,G):[52]+ and_op(H,I):[26] [A>=G,G>=C+2,C>=1,C+1=F,G+1=E,H=0] * CE 159: case_0(A,B,C,D,E) = 6+ eval2(A,B,C,D,F):[57]+ eval2(A,B,C,D,G):[52]+ and_op(H,I):[25] [A>=G,G>=C+2,C>=1,C+1=F,G+1=E,H=1] * CE 160: case_0(A,B,C,D,E) = 6+ eval2(A,B,C,D,F):[57]+ eval2(A,B,C,D,G):[multiple([41,42,43,44,45,46,47,48,49,50],[[57],[56],[55],[54],[53],[52],[51]])]+ and_op(H,I):[26] [G>=C+1,A>=C+1,G>=3,C>=1,C+1=F,G+1=E,H=0] * CE 161: case_0(A,B,C,D,E) = 6+ eval2(A,B,C,D,F):[57]+ eval2(A,B,C,D,G):[multiple([41,42,43,44,45,46,47,48,49,50],[[57],[56],[55],[54],[53],[52],[51]])]+ and_op(H,I):[25] [G>=C+1,A>=C+1,G>=3,C>=1,C+1=F,G+1=E,H=1] * CE 162: case_0(A,B,C,D,E) = 6+ eval2(A,B,C,D,F):[56]+ eval2(A,B,C,D,G):[56]+ and_op(H,I):[26] [A>=1,A+1=G,A+1=F,A+2=E,H=0] * CE 163: case_0(A,B,C,D,E) = 6+ eval2(A,B,C,D,F):[56]+ eval2(A,B,C,D,G):[56]+ and_op(H,I):[25] [A>=1,A+1=G,A+1=F,A+2=E,H=1] * CE 164: case_0(A,B,C,D,E) = 6+ eval2(A,B,C,D,F):[56]+ eval2(A,B,C,D,G):[55]+ and_op(H,I):[26] [C>=A+1,A>=1,C+1=G,A+1=F,C+2=E,H=0] * CE 165: case_0(A,B,C,D,E) = 6+ eval2(A,B,C,D,F):[56]+ eval2(A,B,C,D,G):[55]+ and_op(H,I):[25] [C>=A+1,A>=1,C+1=G,A+1=F,C+2=E,H=1] * CE 166: case_0(A,B,C,D,E) = 6+ eval2(A,B,C,D,F):[56]+ eval2(A,B,C,D,G):[54]+ and_op(H,I):[26] [G>=C+2,G>=A+2,A>=1,A+1=F,G+1=E,H=0] * CE 167: case_0(A,B,C,D,E) = 6+ eval2(A,B,C,D,F):[56]+ eval2(A,B,C,D,G):[54]+ and_op(H,I):[25] [G>=C+2,G>=A+2,A>=1,A+1=F,G+1=E,H=1] * CE 168: case_0(A,B,C,D,E) = 6+ eval2(A,B,C,D,F):[56]+ eval2(A,B,C,D,G):[53]+ and_op(H,I):[26] [C>=G,G>=A+2,A>=1,A+1=F,G+1=E,H=0] * CE 169: case_0(A,B,C,D,E) = 6+ eval2(A,B,C,D,F):[56]+ eval2(A,B,C,D,G):[53]+ and_op(H,I):[25] [C>=G,G>=A+2,A>=1,A+1=F,G+1=E,H=1] * CE 170: case_0(A,B,C,D,E) = 6+ eval2(A,B,C,D,F):[56]+ eval2(A,B,C,D,G):[multiple([41,42,43,44,45,46,47,48,49,50],[[57],[56],[55],[54],[53],[52],[51]])]+ and_op(H,I):[26] [G>=A+1,G>=3,A>=1,A+1=F,G+1=E,H=0] * CE 171: case_0(A,B,C,D,E) = 6+ eval2(A,B,C,D,F):[56]+ eval2(A,B,C,D,G):[multiple([41,42,43,44,45,46,47,48,49,50],[[57],[56],[55],[54],[53],[52],[51]])]+ and_op(H,I):[25] [G>=A+1,G>=3,A>=1,A+1=F,G+1=E,H=1] * CE 172: case_0(A,B,C,D,E) = 6+ eval2(A,B,C,D,F):[55]+ eval2(A,B,C,D,G):[55]+ and_op(H,I):[26] [C>=A+1,C>=1,C+1=G,C+1=F,C+2=E,H=0] * CE 173: case_0(A,B,C,D,E) = 6+ eval2(A,B,C,D,F):[55]+ eval2(A,B,C,D,G):[55]+ and_op(H,I):[25] [C>=A+1,C>=1,C+1=G,C+1=F,C+2=E,H=1] * CE 174: case_0(A,B,C,D,E) = 6+ eval2(A,B,C,D,F):[55]+ eval2(A,B,C,D,G):[54]+ and_op(H,I):[26] [G>=C+2,C>=A+1,C>=1,C+1=F,G+1=E,H=0] * CE 175: case_0(A,B,C,D,E) = 6+ eval2(A,B,C,D,F):[55]+ eval2(A,B,C,D,G):[54]+ and_op(H,I):[25] [G>=C+2,C>=A+1,C>=1,C+1=F,G+1=E,H=1] * CE 176: case_0(A,B,C,D,E) = 6+ eval2(A,B,C,D,F):[55]+ eval2(A,B,C,D,G):[multiple([41,42,43,44,45,46,47,48,49,50],[[57],[56],[55],[54],[53],[52],[51]])]+ and_op(H,I):[26] [G>=C+1,C>=A+1,G>=3,C>=1,C+1=F,G+1=E,H=0] * CE 177: case_0(A,B,C,D,E) = 6+ eval2(A,B,C,D,F):[55]+ eval2(A,B,C,D,G):[multiple([41,42,43,44,45,46,47,48,49,50],[[57],[56],[55],[54],[53],[52],[51]])]+ and_op(H,I):[25] [G>=C+1,C>=A+1,G>=3,C>=1,C+1=F,G+1=E,H=1] * CE 178: case_0(A,B,C,D,E) = 6+ eval2(A,B,C,D,F):[54]+ eval2(A,B,C,D,G):[54]+ and_op(H,I):[26] [F>=C+2,F>=A+2,G>=F,F>=2,G+1=E,H=0] * CE 179: case_0(A,B,C,D,E) = 6+ eval2(A,B,C,D,F):[54]+ eval2(A,B,C,D,G):[54]+ and_op(H,I):[25] [F>=C+2,F>=A+2,G>=F,F>=2,G+1=E,H=1] * CE 180: case_0(A,B,C,D,E) = 6+ eval2(A,B,C,D,F):[54]+ eval2(A,B,C,D,G):[multiple([41,42,43,44,45,46,47,48,49,50],[[57],[56],[55],[54],[53],[52],[51]])]+ and_op(H,I):[26] [G>=F,F>=C+2,F>=A+2,G>=3,F>=2,G+1=E,H=0] * CE 181: case_0(A,B,C,D,E) = 6+ eval2(A,B,C,D,F):[54]+ eval2(A,B,C,D,G):[multiple([41,42,43,44,45,46,47,48,49,50],[[57],[56],[55],[54],[53],[52],[51]])]+ and_op(H,I):[25] [G>=F,F>=C+2,F>=A+2,G>=3,F>=2,G+1=E,H=1] * CE 182: case_0(A,B,C,D,E) = 6+ eval2(A,B,C,D,F):[53]+ eval2(A,B,C,D,G):[55]+ and_op(H,I):[26] [F>=A+2,C>=F,F>=2,C+1=G,C+2=E,H=0] * CE 183: case_0(A,B,C,D,E) = 6+ eval2(A,B,C,D,F):[53]+ eval2(A,B,C,D,G):[55]+ and_op(H,I):[25] [F>=A+2,C>=F,F>=2,C+1=G,C+2=E,H=1] * CE 184: case_0(A,B,C,D,E) = 6+ eval2(A,B,C,D,F):[53]+ eval2(A,B,C,D,G):[54]+ and_op(H,I):[26] [G>=C+2,F>=A+2,C>=F,F>=2,G+1=E,H=0] * CE 185: case_0(A,B,C,D,E) = 6+ eval2(A,B,C,D,F):[53]+ eval2(A,B,C,D,G):[54]+ and_op(H,I):[25] [G>=C+2,F>=A+2,C>=F,F>=2,G+1=E,H=1] * CE 186: case_0(A,B,C,D,E) = 6+ eval2(A,B,C,D,F):[53]+ eval2(A,B,C,D,G):[53]+ and_op(H,I):[26] [C>=G,F>=A+2,G>=F,F>=2,G+1=E,H=0] * CE 187: case_0(A,B,C,D,E) = 6+ eval2(A,B,C,D,F):[53]+ eval2(A,B,C,D,G):[53]+ and_op(H,I):[25] [C>=G,F>=A+2,G>=F,F>=2,G+1=E,H=1] * CE 188: case_0(A,B,C,D,E) = 6+ eval2(A,B,C,D,F):[53]+ eval2(A,B,C,D,G):[multiple([41,42,43,44,45,46,47,48,49,50],[[57],[56],[55],[54],[53],[52],[51]])]+ and_op(H,I):[26] [G>=F,C>=F,F>=A+2,G>=3,F>=2,G+1=E,H=0] * CE 189: case_0(A,B,C,D,E) = 6+ eval2(A,B,C,D,F):[53]+ eval2(A,B,C,D,G):[multiple([41,42,43,44,45,46,47,48,49,50],[[57],[56],[55],[54],[53],[52],[51]])]+ and_op(H,I):[25] [G>=F,C>=F,F>=A+2,G>=3,F>=2,G+1=E,H=1] * CE 190: case_0(A,B,C,D,E) = 6+ eval2(A,B,C,D,F):[52]+ eval2(A,B,C,D,G):[56]+ and_op(H,I):[26] [A>=F,F>=C+2,F>=2,A+1=G,A+2=E,H=0] * CE 191: case_0(A,B,C,D,E) = 6+ eval2(A,B,C,D,F):[52]+ eval2(A,B,C,D,G):[56]+ and_op(H,I):[25] [A>=F,F>=C+2,F>=2,A+1=G,A+2=E,H=1] * CE 192: case_0(A,B,C,D,E) = 6+ eval2(A,B,C,D,F):[52]+ eval2(A,B,C,D,G):[54]+ and_op(H,I):[26] [F>=C+2,G>=A+2,A>=F,F>=2,G+1=E,H=0] * CE 193: case_0(A,B,C,D,E) = 6+ eval2(A,B,C,D,F):[52]+ eval2(A,B,C,D,G):[54]+ and_op(H,I):[25] [F>=C+2,G>=A+2,A>=F,F>=2,G+1=E,H=1] * CE 194: case_0(A,B,C,D,E) = 6+ eval2(A,B,C,D,F):[52]+ eval2(A,B,C,D,G):[52]+ and_op(H,I):[26] [A>=G,F>=C+2,G>=F,F>=2,G+1=E,H=0] * CE 195: case_0(A,B,C,D,E) = 6+ eval2(A,B,C,D,F):[52]+ eval2(A,B,C,D,G):[52]+ and_op(H,I):[25] [A>=G,F>=C+2,G>=F,F>=2,G+1=E,H=1] * CE 196: case_0(A,B,C,D,E) = 6+ eval2(A,B,C,D,F):[52]+ eval2(A,B,C,D,G):[multiple([41,42,43,44,45,46,47,48,49,50],[[57],[56],[55],[54],[53],[52],[51]])]+ and_op(H,I):[26] [G>=F,A>=F,F>=C+2,G>=3,F>=2,G+1=E,H=0] * CE 197: case_0(A,B,C,D,E) = 6+ eval2(A,B,C,D,F):[52]+ eval2(A,B,C,D,G):[multiple([41,42,43,44,45,46,47,48,49,50],[[57],[56],[55],[54],[53],[52],[51]])]+ and_op(H,I):[25] [G>=F,A>=F,F>=C+2,G>=3,F>=2,G+1=E,H=1] * CE 198: case_0(A,B,C,D,E) = 6+ eval2(A,B,C,D,F):[51]+ eval2(A,B,C,D,G):[57]+ and_op(H,I):[26] [A>=C+1,C>=F,F>=2,C+1=G,C+2=E,H=0] * CE 199: case_0(A,B,C,D,E) = 6+ eval2(A,B,C,D,F):[51]+ eval2(A,B,C,D,G):[57]+ and_op(H,I):[25] [A>=C+1,C>=F,F>=2,C+1=G,C+2=E,H=1] * CE 200: case_0(A,B,C,D,E) = 6+ eval2(A,B,C,D,F):[51]+ eval2(A,B,C,D,G):[56]+ and_op(H,I):[26] [A>=F,C>=F,F>=2,A+1=G,A+2=E,H=0] * CE 201: case_0(A,B,C,D,E) = 6+ eval2(A,B,C,D,F):[51]+ eval2(A,B,C,D,G):[56]+ and_op(H,I):[25] [A>=F,C>=F,F>=2,A+1=G,A+2=E,H=1] * CE 202: case_0(A,B,C,D,E) = 6+ eval2(A,B,C,D,F):[51]+ eval2(A,B,C,D,G):[55]+ and_op(H,I):[26] [C>=A+1,A>=F,F>=2,C+1=G,C+2=E,H=0] * CE 203: case_0(A,B,C,D,E) = 6+ eval2(A,B,C,D,F):[51]+ eval2(A,B,C,D,G):[55]+ and_op(H,I):[25] [C>=A+1,A>=F,F>=2,C+1=G,C+2=E,H=1] * CE 204: case_0(A,B,C,D,E) = 6+ eval2(A,B,C,D,F):[51]+ eval2(A,B,C,D,G):[54]+ and_op(H,I):[26] [G>=C+2,G>=A+2,C>=F,A>=F,F>=2,G+1=E,H=0] * CE 205: case_0(A,B,C,D,E) = 6+ eval2(A,B,C,D,F):[51]+ eval2(A,B,C,D,G):[54]+ and_op(H,I):[25] [G>=C+2,G>=A+2,C>=F,A>=F,F>=2,G+1=E,H=1] * CE 206: case_0(A,B,C,D,E) = 6+ eval2(A,B,C,D,F):[51]+ eval2(A,B,C,D,G):[53]+ and_op(H,I):[26] [C>=G,G>=A+2,A>=F,F>=2,G+1=E,H=0] * CE 207: case_0(A,B,C,D,E) = 6+ eval2(A,B,C,D,F):[51]+ eval2(A,B,C,D,G):[53]+ and_op(H,I):[25] [C>=G,G>=A+2,A>=F,F>=2,G+1=E,H=1] * CE 208: case_0(A,B,C,D,E) = 6+ eval2(A,B,C,D,F):[51]+ eval2(A,B,C,D,G):[52]+ and_op(H,I):[26] [A>=G,G>=C+2,C>=F,F>=2,G+1=E,H=0] * CE 209: case_0(A,B,C,D,E) = 6+ eval2(A,B,C,D,F):[51]+ eval2(A,B,C,D,G):[52]+ and_op(H,I):[25] [A>=G,G>=C+2,C>=F,F>=2,G+1=E,H=1] * CE 210: case_0(A,B,C,D,E) = 6+ eval2(A,B,C,D,F):[51]+ eval2(A,B,C,D,G):[51]+ and_op(H,I):[26] [C>=G,A>=G,G>=F,F>=2,G+1=E,H=0] * CE 211: case_0(A,B,C,D,E) = 6+ eval2(A,B,C,D,F):[51]+ eval2(A,B,C,D,G):[51]+ and_op(H,I):[25] [C>=G,A>=G,G>=F,F>=2,G+1=E,H=1] * CE 212: case_0(A,B,C,D,E) = 6+ eval2(A,B,C,D,F):[51]+ eval2(A,B,C,D,G):[multiple([41,42,43,44,45,46,47,48,49,50],[[57],[56],[55],[54],[53],[52],[51]])]+ and_op(H,I):[26] [G>=F,C>=F,A>=F,G>=3,F>=2,G+1=E,H=0] * CE 213: case_0(A,B,C,D,E) = 6+ eval2(A,B,C,D,F):[51]+ eval2(A,B,C,D,G):[multiple([41,42,43,44,45,46,47,48,49,50],[[57],[56],[55],[54],[53],[52],[51]])]+ and_op(H,I):[25] [G>=F,C>=F,A>=F,G>=3,F>=2,G+1=E,H=1] * CE 214: case_0(A,B,C,D,E) = 6+ eval2(A,B,C,D,F):[multiple([41,42,43,44,45,46,47,48,49,50],[[57],[56],[55],[54],[53],[52],[51]])]+ eval2(A,B,C,D,G):[57]+ and_op(H,I):[26] [A>=C+1,C+1>=F,F>=3,C+1=G,C+2=E,H=0] * CE 215: case_0(A,B,C,D,E) = 6+ eval2(A,B,C,D,F):[multiple([41,42,43,44,45,46,47,48,49,50],[[57],[56],[55],[54],[53],[52],[51]])]+ eval2(A,B,C,D,G):[57]+ and_op(H,I):[25] [A>=C+1,C+1>=F,F>=3,C+1=G,C+2=E,H=1] * CE 216: case_0(A,B,C,D,E) = 6+ eval2(A,B,C,D,F):[multiple([41,42,43,44,45,46,47,48,49,50],[[57],[56],[55],[54],[53],[52],[51]])]+ eval2(A,B,C,D,G):[56]+ and_op(H,I):[26] [A+1>=F,F>=3,A+1=G,A+2=E,H=0] * CE 217: case_0(A,B,C,D,E) = 6+ eval2(A,B,C,D,F):[multiple([41,42,43,44,45,46,47,48,49,50],[[57],[56],[55],[54],[53],[52],[51]])]+ eval2(A,B,C,D,G):[56]+ and_op(H,I):[25] [A+1>=F,F>=3,A+1=G,A+2=E,H=1] * CE 218: case_0(A,B,C,D,E) = 6+ eval2(A,B,C,D,F):[multiple([41,42,43,44,45,46,47,48,49,50],[[57],[56],[55],[54],[53],[52],[51]])]+ eval2(A,B,C,D,G):[55]+ and_op(H,I):[26] [C>=A+1,C+1>=F,F>=3,C+1=G,C+2=E,H=0] * CE 219: case_0(A,B,C,D,E) = 6+ eval2(A,B,C,D,F):[multiple([41,42,43,44,45,46,47,48,49,50],[[57],[56],[55],[54],[53],[52],[51]])]+ eval2(A,B,C,D,G):[55]+ and_op(H,I):[25] [C>=A+1,C+1>=F,F>=3,C+1=G,C+2=E,H=1] * CE 220: case_0(A,B,C,D,E) = 6+ eval2(A,B,C,D,F):[multiple([41,42,43,44,45,46,47,48,49,50],[[57],[56],[55],[54],[53],[52],[51]])]+ eval2(A,B,C,D,G):[54]+ and_op(H,I):[26] [G>=C+2,G>=A+2,G>=F,F>=3,G+1=E,H=0] * CE 221: case_0(A,B,C,D,E) = 6+ eval2(A,B,C,D,F):[multiple([41,42,43,44,45,46,47,48,49,50],[[57],[56],[55],[54],[53],[52],[51]])]+ eval2(A,B,C,D,G):[54]+ and_op(H,I):[25] [G>=C+2,G>=A+2,G>=F,F>=3,G+1=E,H=1] * CE 222: case_0(A,B,C,D,E) = 6+ eval2(A,B,C,D,F):[multiple([41,42,43,44,45,46,47,48,49,50],[[57],[56],[55],[54],[53],[52],[51]])]+ eval2(A,B,C,D,G):[53]+ and_op(H,I):[26] [C>=G,G>=A+2,G>=F,F>=3,G+1=E,H=0] * CE 223: case_0(A,B,C,D,E) = 6+ eval2(A,B,C,D,F):[multiple([41,42,43,44,45,46,47,48,49,50],[[57],[56],[55],[54],[53],[52],[51]])]+ eval2(A,B,C,D,G):[53]+ and_op(H,I):[25] [C>=G,G>=A+2,G>=F,F>=3,G+1=E,H=1] * CE 224: case_0(A,B,C,D,E) = 6+ eval2(A,B,C,D,F):[multiple([41,42,43,44,45,46,47,48,49,50],[[57],[56],[55],[54],[53],[52],[51]])]+ eval2(A,B,C,D,G):[52]+ and_op(H,I):[26] [A>=G,G>=C+2,G>=F,F>=3,G+1=E,H=0] * CE 225: case_0(A,B,C,D,E) = 6+ eval2(A,B,C,D,F):[multiple([41,42,43,44,45,46,47,48,49,50],[[57],[56],[55],[54],[53],[52],[51]])]+ eval2(A,B,C,D,G):[52]+ and_op(H,I):[25] [A>=G,G>=C+2,G>=F,F>=3,G+1=E,H=1] * CE 226: case_0(A,B,C,D,E) = 6+ eval2(A,B,C,D,F):[multiple([41,42,43,44,45,46,47,48,49,50],[[57],[56],[55],[54],[53],[52],[51]])]+ eval2(A,B,C,D,G):[51]+ and_op(H,I):[26] [C>=G,A>=G,G>=F,F>=3,G+1=E,H=0] * CE 227: case_0(A,B,C,D,E) = 6+ eval2(A,B,C,D,F):[multiple([41,42,43,44,45,46,47,48,49,50],[[57],[56],[55],[54],[53],[52],[51]])]+ eval2(A,B,C,D,G):[51]+ and_op(H,I):[25] [C>=G,A>=G,G>=F,F>=3,G+1=E,H=1] * CE 228: case_0(A,B,C,D,E) = 6+ eval2(A,B,C,D,F):[multiple([41,42,43,44,45,46,47,48,49,50],[[57],[56],[55],[54],[53],[52],[51]])]+ eval2(A,B,C,D,G):[multiple([41,42,43,44,45,46,47,48,49,50],[[57],[56],[55],[54],[53],[52],[51]])]+ and_op(H,I):[26] [G>=F,F>=3,G+1=E,H=0] * CE 229: case_0(A,B,C,D,E) = 6+ eval2(A,B,C,D,F):[multiple([41,42,43,44,45,46,47,48,49,50],[[57],[56],[55],[54],[53],[52],[51]])]+ eval2(A,B,C,D,G):[multiple([41,42,43,44,45,46,47,48,49,50],[[57],[56],[55],[54],[53],[52],[51]])]+ and_op(H,I):[25] [G>=F,F>=3,G+1=E,H=1] * CE 230: case_0(A,B,C,D,E) = 7+ eval2(A,B,C,D,F):[57]+ eval2(A,B,C,D,G):[57]+ or(H,I):[40] [A>=C+1,C>=1,C+1=G,C+1=F,C+2=E,H=0] * CE 231: case_0(A,B,C,D,E) = 7+ eval2(A,B,C,D,F):[57]+ eval2(A,B,C,D,G):[57]+ or(H,I):[39] [A>=C+1,C>=1,C+1=G,C+1=F,C+2=E,H=1] * CE 232: case_0(A,B,C,D,E) = 7+ eval2(A,B,C,D,F):[57]+ eval2(A,B,C,D,G):[51]+ or(H,I):[40] [C>=G,A>=C+1,G>=2,C+1=F,C+2=E,H=0] * CE 233: case_0(A,B,C,D,E) = 7+ eval2(A,B,C,D,F):[57]+ eval2(A,B,C,D,G):[51]+ or(H,I):[39] [C>=G,A>=C+1,G>=2,C+1=F,C+2=E,H=1] * CE 234: case_0(A,B,C,D,E) = 7+ eval2(A,B,C,D,F):[57]+ eval2(A,B,C,D,G):[multiple([41,42,43,44,45,46,47,48,49,50],[[57],[56],[55],[54],[53],[52],[51]])]+ or(H,I):[40] [C+1>=G,A>=C+1,G>=3,C+1=F,C+2=E,H=0] * CE 235: case_0(A,B,C,D,E) = 7+ eval2(A,B,C,D,F):[57]+ eval2(A,B,C,D,G):[multiple([41,42,43,44,45,46,47,48,49,50],[[57],[56],[55],[54],[53],[52],[51]])]+ or(H,I):[39] [C+1>=G,A>=C+1,G>=3,C+1=F,C+2=E,H=1] * CE 236: case_0(A,B,C,D,E) = 7+ eval2(A,B,C,D,F):[56]+ eval2(A,B,C,D,G):[57]+ or(H,I):[40] [A>=C+1,C>=1,C+1=G,A+1=F,A+2=E,H=0] * CE 237: case_0(A,B,C,D,E) = 7+ eval2(A,B,C,D,F):[56]+ eval2(A,B,C,D,G):[57]+ or(H,I):[39] [A>=C+1,C>=1,C+1=G,A+1=F,A+2=E,H=1] * CE 238: case_0(A,B,C,D,E) = 7+ eval2(A,B,C,D,F):[56]+ eval2(A,B,C,D,G):[56]+ or(H,I):[40] [A>=1,A+1=G,A+1=F,A+2=E,H=0] * CE 239: case_0(A,B,C,D,E) = 7+ eval2(A,B,C,D,F):[56]+ eval2(A,B,C,D,G):[56]+ or(H,I):[39] [A>=1,A+1=G,A+1=F,A+2=E,H=1] * CE 240: case_0(A,B,C,D,E) = 7+ eval2(A,B,C,D,F):[56]+ eval2(A,B,C,D,G):[52]+ or(H,I):[40] [A>=G,G>=C+2,G>=2,A+1=F,A+2=E,H=0] * CE 241: case_0(A,B,C,D,E) = 7+ eval2(A,B,C,D,F):[56]+ eval2(A,B,C,D,G):[52]+ or(H,I):[39] [A>=G,G>=C+2,G>=2,A+1=F,A+2=E,H=1] * CE 242: case_0(A,B,C,D,E) = 7+ eval2(A,B,C,D,F):[56]+ eval2(A,B,C,D,G):[51]+ or(H,I):[40] [C>=G,A>=G,G>=2,A+1=F,A+2=E,H=0] * CE 243: case_0(A,B,C,D,E) = 7+ eval2(A,B,C,D,F):[56]+ eval2(A,B,C,D,G):[51]+ or(H,I):[39] [C>=G,A>=G,G>=2,A+1=F,A+2=E,H=1] * CE 244: case_0(A,B,C,D,E) = 7+ eval2(A,B,C,D,F):[56]+ eval2(A,B,C,D,G):[multiple([41,42,43,44,45,46,47,48,49,50],[[57],[56],[55],[54],[53],[52],[51]])]+ or(H,I):[40] [A+1>=G,G>=3,A+1=F,A+2=E,H=0] * CE 245: case_0(A,B,C,D,E) = 7+ eval2(A,B,C,D,F):[56]+ eval2(A,B,C,D,G):[multiple([41,42,43,44,45,46,47,48,49,50],[[57],[56],[55],[54],[53],[52],[51]])]+ or(H,I):[39] [A+1>=G,G>=3,A+1=F,A+2=E,H=1] * CE 246: case_0(A,B,C,D,E) = 7+ eval2(A,B,C,D,F):[55]+ eval2(A,B,C,D,G):[56]+ or(H,I):[40] [C>=A+1,A>=1,A+1=G,C+1=F,C+2=E,H=0] * CE 247: case_0(A,B,C,D,E) = 7+ eval2(A,B,C,D,F):[55]+ eval2(A,B,C,D,G):[56]+ or(H,I):[39] [C>=A+1,A>=1,A+1=G,C+1=F,C+2=E,H=1] * CE 248: case_0(A,B,C,D,E) = 7+ eval2(A,B,C,D,F):[55]+ eval2(A,B,C,D,G):[55]+ or(H,I):[40] [C>=A+1,C>=1,C+1=G,C+1=F,C+2=E,H=0] * CE 249: case_0(A,B,C,D,E) = 7+ eval2(A,B,C,D,F):[55]+ eval2(A,B,C,D,G):[55]+ or(H,I):[39] [C>=A+1,C>=1,C+1=G,C+1=F,C+2=E,H=1] * CE 250: case_0(A,B,C,D,E) = 7+ eval2(A,B,C,D,F):[55]+ eval2(A,B,C,D,G):[53]+ or(H,I):[40] [C>=G,G>=A+2,G>=2,C+1=F,C+2=E,H=0] * CE 251: case_0(A,B,C,D,E) = 7+ eval2(A,B,C,D,F):[55]+ eval2(A,B,C,D,G):[53]+ or(H,I):[39] [C>=G,G>=A+2,G>=2,C+1=F,C+2=E,H=1] * CE 252: case_0(A,B,C,D,E) = 7+ eval2(A,B,C,D,F):[55]+ eval2(A,B,C,D,G):[51]+ or(H,I):[40] [A>=G,C>=A+1,G>=2,C+1=F,C+2=E,H=0] * CE 253: case_0(A,B,C,D,E) = 7+ eval2(A,B,C,D,F):[55]+ eval2(A,B,C,D,G):[51]+ or(H,I):[39] [A>=G,C>=A+1,G>=2,C+1=F,C+2=E,H=1] * CE 254: case_0(A,B,C,D,E) = 7+ eval2(A,B,C,D,F):[55]+ eval2(A,B,C,D,G):[multiple([41,42,43,44,45,46,47,48,49,50],[[57],[56],[55],[54],[53],[52],[51]])]+ or(H,I):[40] [C+1>=G,C>=A+1,G>=3,C+1=F,C+2=E,H=0] * CE 255: case_0(A,B,C,D,E) = 7+ eval2(A,B,C,D,F):[55]+ eval2(A,B,C,D,G):[multiple([41,42,43,44,45,46,47,48,49,50],[[57],[56],[55],[54],[53],[52],[51]])]+ or(H,I):[39] [C+1>=G,C>=A+1,G>=3,C+1=F,C+2=E,H=1] * CE 256: case_0(A,B,C,D,E) = 7+ eval2(A,B,C,D,F):[54]+ eval2(A,B,C,D,G):[57]+ or(H,I):[40] [A>=C+1,F>=A+2,C>=1,C+1=G,F+1=E,H=0] * CE 257: case_0(A,B,C,D,E) = 7+ eval2(A,B,C,D,F):[54]+ eval2(A,B,C,D,G):[57]+ or(H,I):[39] [A>=C+1,F>=A+2,C>=1,C+1=G,F+1=E,H=1] * CE 258: case_0(A,B,C,D,E) = 7+ eval2(A,B,C,D,F):[54]+ eval2(A,B,C,D,G):[56]+ or(H,I):[40] [F>=A+2,F>=C+2,A>=1,A+1=G,F+1=E,H=0] * CE 259: case_0(A,B,C,D,E) = 7+ eval2(A,B,C,D,F):[54]+ eval2(A,B,C,D,G):[56]+ or(H,I):[39] [F>=A+2,F>=C+2,A>=1,A+1=G,F+1=E,H=1] * CE 260: case_0(A,B,C,D,E) = 7+ eval2(A,B,C,D,F):[54]+ eval2(A,B,C,D,G):[55]+ or(H,I):[40] [F>=C+2,C>=A+1,C>=1,C+1=G,F+1=E,H=0] * CE 261: case_0(A,B,C,D,E) = 7+ eval2(A,B,C,D,F):[54]+ eval2(A,B,C,D,G):[55]+ or(H,I):[39] [F>=C+2,C>=A+1,C>=1,C+1=G,F+1=E,H=1] * CE 262: case_0(A,B,C,D,E) = 7+ eval2(A,B,C,D,F):[54]+ eval2(A,B,C,D,G):[54]+ or(H,I):[40] [F>=G,G>=C+2,G>=A+2,G>=2,F+1=E,H=0] * CE 263: case_0(A,B,C,D,E) = 7+ eval2(A,B,C,D,F):[54]+ eval2(A,B,C,D,G):[54]+ or(H,I):[39] [F>=G,G>=C+2,G>=A+2,G>=2,F+1=E,H=1] * CE 264: case_0(A,B,C,D,E) = 7+ eval2(A,B,C,D,F):[54]+ eval2(A,B,C,D,G):[53]+ or(H,I):[40] [C>=G,F>=C+2,G>=A+2,G>=2,F+1=E,H=0] * CE 265: case_0(A,B,C,D,E) = 7+ eval2(A,B,C,D,F):[54]+ eval2(A,B,C,D,G):[53]+ or(H,I):[39] [C>=G,F>=C+2,G>=A+2,G>=2,F+1=E,H=1] * CE 266: case_0(A,B,C,D,E) = 7+ eval2(A,B,C,D,F):[54]+ eval2(A,B,C,D,G):[52]+ or(H,I):[40] [A>=G,G>=C+2,F>=A+2,G>=2,F+1=E,H=0] * CE 267: case_0(A,B,C,D,E) = 7+ eval2(A,B,C,D,F):[54]+ eval2(A,B,C,D,G):[52]+ or(H,I):[39] [A>=G,G>=C+2,F>=A+2,G>=2,F+1=E,H=1] * CE 268: case_0(A,B,C,D,E) = 7+ eval2(A,B,C,D,F):[54]+ eval2(A,B,C,D,G):[51]+ or(H,I):[40] [C>=G,A>=G,F>=C+2,F>=A+2,G>=2,F+1=E,H=0] * CE 269: case_0(A,B,C,D,E) = 7+ eval2(A,B,C,D,F):[54]+ eval2(A,B,C,D,G):[51]+ or(H,I):[39] [C>=G,A>=G,F>=C+2,F>=A+2,G>=2,F+1=E,H=1] * CE 270: case_0(A,B,C,D,E) = 7+ eval2(A,B,C,D,F):[54]+ eval2(A,B,C,D,G):[multiple([41,42,43,44,45,46,47,48,49,50],[[57],[56],[55],[54],[53],[52],[51]])]+ or(H,I):[40] [F>=G,F>=C+2,F>=A+2,G>=3,F+1=E,H=0] * CE 271: case_0(A,B,C,D,E) = 7+ eval2(A,B,C,D,F):[54]+ eval2(A,B,C,D,G):[multiple([41,42,43,44,45,46,47,48,49,50],[[57],[56],[55],[54],[53],[52],[51]])]+ or(H,I):[39] [F>=G,F>=C+2,F>=A+2,G>=3,F+1=E,H=1] * CE 272: case_0(A,B,C,D,E) = 7+ eval2(A,B,C,D,F):[53]+ eval2(A,B,C,D,G):[56]+ or(H,I):[40] [F>=A+2,C>=F,A>=1,A+1=G,F+1=E,H=0] * CE 273: case_0(A,B,C,D,E) = 7+ eval2(A,B,C,D,F):[53]+ eval2(A,B,C,D,G):[56]+ or(H,I):[39] [F>=A+2,C>=F,A>=1,A+1=G,F+1=E,H=1] * CE 274: case_0(A,B,C,D,E) = 7+ eval2(A,B,C,D,F):[53]+ eval2(A,B,C,D,G):[53]+ or(H,I):[40] [F>=G,G>=A+2,C>=F,G>=2,F+1=E,H=0] * CE 275: case_0(A,B,C,D,E) = 7+ eval2(A,B,C,D,F):[53]+ eval2(A,B,C,D,G):[53]+ or(H,I):[39] [F>=G,G>=A+2,C>=F,G>=2,F+1=E,H=1] * CE 276: case_0(A,B,C,D,E) = 7+ eval2(A,B,C,D,F):[53]+ eval2(A,B,C,D,G):[51]+ or(H,I):[40] [A>=G,F>=A+2,C>=F,G>=2,F+1=E,H=0] * CE 277: case_0(A,B,C,D,E) = 7+ eval2(A,B,C,D,F):[53]+ eval2(A,B,C,D,G):[51]+ or(H,I):[39] [A>=G,F>=A+2,C>=F,G>=2,F+1=E,H=1] * CE 278: case_0(A,B,C,D,E) = 7+ eval2(A,B,C,D,F):[53]+ eval2(A,B,C,D,G):[multiple([41,42,43,44,45,46,47,48,49,50],[[57],[56],[55],[54],[53],[52],[51]])]+ or(H,I):[40] [F>=G,C>=F,F>=A+2,G>=3,F+1=E,H=0] * CE 279: case_0(A,B,C,D,E) = 7+ eval2(A,B,C,D,F):[53]+ eval2(A,B,C,D,G):[multiple([41,42,43,44,45,46,47,48,49,50],[[57],[56],[55],[54],[53],[52],[51]])]+ or(H,I):[39] [F>=G,C>=F,F>=A+2,G>=3,F+1=E,H=1] * CE 280: case_0(A,B,C,D,E) = 7+ eval2(A,B,C,D,F):[52]+ eval2(A,B,C,D,G):[57]+ or(H,I):[40] [F>=C+2,A>=F,C>=1,C+1=G,F+1=E,H=0] * CE 281: case_0(A,B,C,D,E) = 7+ eval2(A,B,C,D,F):[52]+ eval2(A,B,C,D,G):[57]+ or(H,I):[39] [F>=C+2,A>=F,C>=1,C+1=G,F+1=E,H=1] * CE 282: case_0(A,B,C,D,E) = 7+ eval2(A,B,C,D,F):[52]+ eval2(A,B,C,D,G):[52]+ or(H,I):[40] [F>=G,G>=C+2,A>=F,G>=2,F+1=E,H=0] * CE 283: case_0(A,B,C,D,E) = 7+ eval2(A,B,C,D,F):[52]+ eval2(A,B,C,D,G):[52]+ or(H,I):[39] [F>=G,G>=C+2,A>=F,G>=2,F+1=E,H=1] * CE 284: case_0(A,B,C,D,E) = 7+ eval2(A,B,C,D,F):[52]+ eval2(A,B,C,D,G):[51]+ or(H,I):[40] [C>=G,F>=C+2,A>=F,G>=2,F+1=E,H=0] * CE 285: case_0(A,B,C,D,E) = 7+ eval2(A,B,C,D,F):[52]+ eval2(A,B,C,D,G):[51]+ or(H,I):[39] [C>=G,F>=C+2,A>=F,G>=2,F+1=E,H=1] * CE 286: case_0(A,B,C,D,E) = 7+ eval2(A,B,C,D,F):[52]+ eval2(A,B,C,D,G):[multiple([41,42,43,44,45,46,47,48,49,50],[[57],[56],[55],[54],[53],[52],[51]])]+ or(H,I):[40] [F>=G,A>=F,F>=C+2,G>=3,F+1=E,H=0] * CE 287: case_0(A,B,C,D,E) = 7+ eval2(A,B,C,D,F):[52]+ eval2(A,B,C,D,G):[multiple([41,42,43,44,45,46,47,48,49,50],[[57],[56],[55],[54],[53],[52],[51]])]+ or(H,I):[39] [F>=G,A>=F,F>=C+2,G>=3,F+1=E,H=1] * CE 288: case_0(A,B,C,D,E) = 7+ eval2(A,B,C,D,F):[51]+ eval2(A,B,C,D,G):[51]+ or(H,I):[40] [F>=G,C>=F,A>=F,G>=2,F+1=E,H=0] * CE 289: case_0(A,B,C,D,E) = 7+ eval2(A,B,C,D,F):[51]+ eval2(A,B,C,D,G):[51]+ or(H,I):[39] [F>=G,C>=F,A>=F,G>=2,F+1=E,H=1] * CE 290: case_0(A,B,C,D,E) = 7+ eval2(A,B,C,D,F):[51]+ eval2(A,B,C,D,G):[multiple([41,42,43,44,45,46,47,48,49,50],[[57],[56],[55],[54],[53],[52],[51]])]+ or(H,I):[40] [F>=G,C>=F,A>=F,G>=3,F+1=E,H=0] * CE 291: case_0(A,B,C,D,E) = 7+ eval2(A,B,C,D,F):[51]+ eval2(A,B,C,D,G):[multiple([41,42,43,44,45,46,47,48,49,50],[[57],[56],[55],[54],[53],[52],[51]])]+ or(H,I):[39] [F>=G,C>=F,A>=F,G>=3,F+1=E,H=1] * CE 292: case_0(A,B,C,D,E) = 7+ eval2(A,B,C,D,F):[multiple([41,42,43,44,45,46,47,48,49,50],[[57],[56],[55],[54],[53],[52],[51]])]+ eval2(A,B,C,D,G):[57]+ or(H,I):[40] [A>=C+1,F>=C+1,C>=1,F>=3,C+1=G,F+1=E,H=0] * CE 293: case_0(A,B,C,D,E) = 7+ eval2(A,B,C,D,F):[multiple([41,42,43,44,45,46,47,48,49,50],[[57],[56],[55],[54],[53],[52],[51]])]+ eval2(A,B,C,D,G):[57]+ or(H,I):[39] [A>=C+1,F>=C+1,C>=1,F>=3,C+1=G,F+1=E,H=1] * CE 294: case_0(A,B,C,D,E) = 7+ eval2(A,B,C,D,F):[multiple([41,42,43,44,45,46,47,48,49,50],[[57],[56],[55],[54],[53],[52],[51]])]+ eval2(A,B,C,D,G):[56]+ or(H,I):[40] [F>=A+1,A>=1,F>=3,A+1=G,F+1=E,H=0] * CE 295: case_0(A,B,C,D,E) = 7+ eval2(A,B,C,D,F):[multiple([41,42,43,44,45,46,47,48,49,50],[[57],[56],[55],[54],[53],[52],[51]])]+ eval2(A,B,C,D,G):[56]+ or(H,I):[39] [F>=A+1,A>=1,F>=3,A+1=G,F+1=E,H=1] * CE 296: case_0(A,B,C,D,E) = 7+ eval2(A,B,C,D,F):[multiple([41,42,43,44,45,46,47,48,49,50],[[57],[56],[55],[54],[53],[52],[51]])]+ eval2(A,B,C,D,G):[55]+ or(H,I):[40] [F>=C+1,C>=A+1,C>=1,F>=3,C+1=G,F+1=E,H=0] * CE 297: case_0(A,B,C,D,E) = 7+ eval2(A,B,C,D,F):[multiple([41,42,43,44,45,46,47,48,49,50],[[57],[56],[55],[54],[53],[52],[51]])]+ eval2(A,B,C,D,G):[55]+ or(H,I):[39] [F>=C+1,C>=A+1,C>=1,F>=3,C+1=G,F+1=E,H=1] * CE 298: case_0(A,B,C,D,E) = 7+ eval2(A,B,C,D,F):[multiple([41,42,43,44,45,46,47,48,49,50],[[57],[56],[55],[54],[53],[52],[51]])]+ eval2(A,B,C,D,G):[54]+ or(H,I):[40] [F>=G,G>=C+2,G>=A+2,G>=2,F>=3,F+1=E,H=0] * CE 299: case_0(A,B,C,D,E) = 7+ eval2(A,B,C,D,F):[multiple([41,42,43,44,45,46,47,48,49,50],[[57],[56],[55],[54],[53],[52],[51]])]+ eval2(A,B,C,D,G):[54]+ or(H,I):[39] [F>=G,G>=C+2,G>=A+2,G>=2,F>=3,F+1=E,H=1] * CE 300: case_0(A,B,C,D,E) = 7+ eval2(A,B,C,D,F):[multiple([41,42,43,44,45,46,47,48,49,50],[[57],[56],[55],[54],[53],[52],[51]])]+ eval2(A,B,C,D,G):[53]+ or(H,I):[40] [C>=G,F>=G,G>=A+2,G>=2,F>=3,F+1=E,H=0] * CE 301: case_0(A,B,C,D,E) = 7+ eval2(A,B,C,D,F):[multiple([41,42,43,44,45,46,47,48,49,50],[[57],[56],[55],[54],[53],[52],[51]])]+ eval2(A,B,C,D,G):[53]+ or(H,I):[39] [C>=G,F>=G,G>=A+2,G>=2,F>=3,F+1=E,H=1] * CE 302: case_0(A,B,C,D,E) = 7+ eval2(A,B,C,D,F):[multiple([41,42,43,44,45,46,47,48,49,50],[[57],[56],[55],[54],[53],[52],[51]])]+ eval2(A,B,C,D,G):[52]+ or(H,I):[40] [A>=G,F>=G,G>=C+2,G>=2,F>=3,F+1=E,H=0] * CE 303: case_0(A,B,C,D,E) = 7+ eval2(A,B,C,D,F):[multiple([41,42,43,44,45,46,47,48,49,50],[[57],[56],[55],[54],[53],[52],[51]])]+ eval2(A,B,C,D,G):[52]+ or(H,I):[39] [A>=G,F>=G,G>=C+2,G>=2,F>=3,F+1=E,H=1] * CE 304: case_0(A,B,C,D,E) = 7+ eval2(A,B,C,D,F):[multiple([41,42,43,44,45,46,47,48,49,50],[[57],[56],[55],[54],[53],[52],[51]])]+ eval2(A,B,C,D,G):[51]+ or(H,I):[40] [C>=G,A>=G,F>=G,G>=2,F>=3,F+1=E,H=0] * CE 305: case_0(A,B,C,D,E) = 7+ eval2(A,B,C,D,F):[multiple([41,42,43,44,45,46,47,48,49,50],[[57],[56],[55],[54],[53],[52],[51]])]+ eval2(A,B,C,D,G):[51]+ or(H,I):[39] [C>=G,A>=G,F>=G,G>=2,F>=3,F+1=E,H=1] * CE 306: case_0(A,B,C,D,E) = 7+ eval2(A,B,C,D,F):[multiple([41,42,43,44,45,46,47,48,49,50],[[57],[56],[55],[54],[53],[52],[51]])]+ eval2(A,B,C,D,G):[multiple([41,42,43,44,45,46,47,48,49,50],[[57],[56],[55],[54],[53],[52],[51]])]+ or(H,I):[40] [F>=G,G>=3,F+1=E,H=0] * CE 307: case_0(A,B,C,D,E) = 7+ eval2(A,B,C,D,F):[multiple([41,42,43,44,45,46,47,48,49,50],[[57],[56],[55],[54],[53],[52],[51]])]+ eval2(A,B,C,D,G):[multiple([41,42,43,44,45,46,47,48,49,50],[[57],[56],[55],[54],[53],[52],[51]])]+ or(H,I):[39] [F>=G,G>=3,F+1=E,H=1] * CE 308: case_0(A,B,C,D,E) = 7+ eval2(A,B,C,D,F):[57]+ eval2(A,B,C,D,G):[57]+ or(H,I):[40] [A>=C+1,C>=1,C+1=G,C+1=F,C+2=E,H=0] * CE 309: case_0(A,B,C,D,E) = 7+ eval2(A,B,C,D,F):[57]+ eval2(A,B,C,D,G):[57]+ or(H,I):[39] [A>=C+1,C>=1,C+1=G,C+1=F,C+2=E,H=1] * CE 310: case_0(A,B,C,D,E) = 7+ eval2(A,B,C,D,F):[57]+ eval2(A,B,C,D,G):[56]+ or(H,I):[40] [A>=C+1,C>=1,A+1=G,C+1=F,A+2=E,H=0] * CE 311: case_0(A,B,C,D,E) = 7+ eval2(A,B,C,D,F):[57]+ eval2(A,B,C,D,G):[56]+ or(H,I):[39] [A>=C+1,C>=1,A+1=G,C+1=F,A+2=E,H=1] * CE 312: case_0(A,B,C,D,E) = 7+ eval2(A,B,C,D,F):[57]+ eval2(A,B,C,D,G):[54]+ or(H,I):[40] [A>=C+1,G>=A+2,C>=1,C+1=F,G+1=E,H=0] * CE 313: case_0(A,B,C,D,E) = 7+ eval2(A,B,C,D,F):[57]+ eval2(A,B,C,D,G):[54]+ or(H,I):[39] [A>=C+1,G>=A+2,C>=1,C+1=F,G+1=E,H=1] * CE 314: case_0(A,B,C,D,E) = 7+ eval2(A,B,C,D,F):[57]+ eval2(A,B,C,D,G):[52]+ or(H,I):[40] [A>=G,G>=C+2,C>=1,C+1=F,G+1=E,H=0] * CE 315: case_0(A,B,C,D,E) = 7+ eval2(A,B,C,D,F):[57]+ eval2(A,B,C,D,G):[52]+ or(H,I):[39] [A>=G,G>=C+2,C>=1,C+1=F,G+1=E,H=1] * CE 316: case_0(A,B,C,D,E) = 7+ eval2(A,B,C,D,F):[57]+ eval2(A,B,C,D,G):[multiple([41,42,43,44,45,46,47,48,49,50],[[57],[56],[55],[54],[53],[52],[51]])]+ or(H,I):[40] [G>=C+1,A>=C+1,G>=3,C>=1,C+1=F,G+1=E,H=0] * CE 317: case_0(A,B,C,D,E) = 7+ eval2(A,B,C,D,F):[57]+ eval2(A,B,C,D,G):[multiple([41,42,43,44,45,46,47,48,49,50],[[57],[56],[55],[54],[53],[52],[51]])]+ or(H,I):[39] [G>=C+1,A>=C+1,G>=3,C>=1,C+1=F,G+1=E,H=1] * CE 318: case_0(A,B,C,D,E) = 7+ eval2(A,B,C,D,F):[56]+ eval2(A,B,C,D,G):[56]+ or(H,I):[40] [A>=1,A+1=G,A+1=F,A+2=E,H=0] * CE 319: case_0(A,B,C,D,E) = 7+ eval2(A,B,C,D,F):[56]+ eval2(A,B,C,D,G):[56]+ or(H,I):[39] [A>=1,A+1=G,A+1=F,A+2=E,H=1] * CE 320: case_0(A,B,C,D,E) = 7+ eval2(A,B,C,D,F):[56]+ eval2(A,B,C,D,G):[55]+ or(H,I):[40] [C>=A+1,A>=1,C+1=G,A+1=F,C+2=E,H=0] * CE 321: case_0(A,B,C,D,E) = 7+ eval2(A,B,C,D,F):[56]+ eval2(A,B,C,D,G):[55]+ or(H,I):[39] [C>=A+1,A>=1,C+1=G,A+1=F,C+2=E,H=1] * CE 322: case_0(A,B,C,D,E) = 7+ eval2(A,B,C,D,F):[56]+ eval2(A,B,C,D,G):[54]+ or(H,I):[40] [G>=C+2,G>=A+2,A>=1,A+1=F,G+1=E,H=0] * CE 323: case_0(A,B,C,D,E) = 7+ eval2(A,B,C,D,F):[56]+ eval2(A,B,C,D,G):[54]+ or(H,I):[39] [G>=C+2,G>=A+2,A>=1,A+1=F,G+1=E,H=1] * CE 324: case_0(A,B,C,D,E) = 7+ eval2(A,B,C,D,F):[56]+ eval2(A,B,C,D,G):[53]+ or(H,I):[40] [C>=G,G>=A+2,A>=1,A+1=F,G+1=E,H=0] * CE 325: case_0(A,B,C,D,E) = 7+ eval2(A,B,C,D,F):[56]+ eval2(A,B,C,D,G):[53]+ or(H,I):[39] [C>=G,G>=A+2,A>=1,A+1=F,G+1=E,H=1] * CE 326: case_0(A,B,C,D,E) = 7+ eval2(A,B,C,D,F):[56]+ eval2(A,B,C,D,G):[multiple([41,42,43,44,45,46,47,48,49,50],[[57],[56],[55],[54],[53],[52],[51]])]+ or(H,I):[40] [G>=A+1,G>=3,A>=1,A+1=F,G+1=E,H=0] * CE 327: case_0(A,B,C,D,E) = 7+ eval2(A,B,C,D,F):[56]+ eval2(A,B,C,D,G):[multiple([41,42,43,44,45,46,47,48,49,50],[[57],[56],[55],[54],[53],[52],[51]])]+ or(H,I):[39] [G>=A+1,G>=3,A>=1,A+1=F,G+1=E,H=1] * CE 328: case_0(A,B,C,D,E) = 7+ eval2(A,B,C,D,F):[55]+ eval2(A,B,C,D,G):[55]+ or(H,I):[40] [C>=A+1,C>=1,C+1=G,C+1=F,C+2=E,H=0] * CE 329: case_0(A,B,C,D,E) = 7+ eval2(A,B,C,D,F):[55]+ eval2(A,B,C,D,G):[55]+ or(H,I):[39] [C>=A+1,C>=1,C+1=G,C+1=F,C+2=E,H=1] * CE 330: case_0(A,B,C,D,E) = 7+ eval2(A,B,C,D,F):[55]+ eval2(A,B,C,D,G):[54]+ or(H,I):[40] [G>=C+2,C>=A+1,C>=1,C+1=F,G+1=E,H=0] * CE 331: case_0(A,B,C,D,E) = 7+ eval2(A,B,C,D,F):[55]+ eval2(A,B,C,D,G):[54]+ or(H,I):[39] [G>=C+2,C>=A+1,C>=1,C+1=F,G+1=E,H=1] * CE 332: case_0(A,B,C,D,E) = 7+ eval2(A,B,C,D,F):[55]+ eval2(A,B,C,D,G):[multiple([41,42,43,44,45,46,47,48,49,50],[[57],[56],[55],[54],[53],[52],[51]])]+ or(H,I):[40] [G>=C+1,C>=A+1,G>=3,C>=1,C+1=F,G+1=E,H=0] * CE 333: case_0(A,B,C,D,E) = 7+ eval2(A,B,C,D,F):[55]+ eval2(A,B,C,D,G):[multiple([41,42,43,44,45,46,47,48,49,50],[[57],[56],[55],[54],[53],[52],[51]])]+ or(H,I):[39] [G>=C+1,C>=A+1,G>=3,C>=1,C+1=F,G+1=E,H=1] * CE 334: case_0(A,B,C,D,E) = 7+ eval2(A,B,C,D,F):[54]+ eval2(A,B,C,D,G):[54]+ or(H,I):[40] [F>=C+2,F>=A+2,G>=F,F>=2,G+1=E,H=0] * CE 335: case_0(A,B,C,D,E) = 7+ eval2(A,B,C,D,F):[54]+ eval2(A,B,C,D,G):[54]+ or(H,I):[39] [F>=C+2,F>=A+2,G>=F,F>=2,G+1=E,H=1] * CE 336: case_0(A,B,C,D,E) = 7+ eval2(A,B,C,D,F):[54]+ eval2(A,B,C,D,G):[multiple([41,42,43,44,45,46,47,48,49,50],[[57],[56],[55],[54],[53],[52],[51]])]+ or(H,I):[40] [G>=F,F>=C+2,F>=A+2,G>=3,F>=2,G+1=E,H=0] * CE 337: case_0(A,B,C,D,E) = 7+ eval2(A,B,C,D,F):[54]+ eval2(A,B,C,D,G):[multiple([41,42,43,44,45,46,47,48,49,50],[[57],[56],[55],[54],[53],[52],[51]])]+ or(H,I):[39] [G>=F,F>=C+2,F>=A+2,G>=3,F>=2,G+1=E,H=1] * CE 338: case_0(A,B,C,D,E) = 7+ eval2(A,B,C,D,F):[53]+ eval2(A,B,C,D,G):[55]+ or(H,I):[40] [F>=A+2,C>=F,F>=2,C+1=G,C+2=E,H=0] * CE 339: case_0(A,B,C,D,E) = 7+ eval2(A,B,C,D,F):[53]+ eval2(A,B,C,D,G):[55]+ or(H,I):[39] [F>=A+2,C>=F,F>=2,C+1=G,C+2=E,H=1] * CE 340: case_0(A,B,C,D,E) = 7+ eval2(A,B,C,D,F):[53]+ eval2(A,B,C,D,G):[54]+ or(H,I):[40] [G>=C+2,F>=A+2,C>=F,F>=2,G+1=E,H=0] * CE 341: case_0(A,B,C,D,E) = 7+ eval2(A,B,C,D,F):[53]+ eval2(A,B,C,D,G):[54]+ or(H,I):[39] [G>=C+2,F>=A+2,C>=F,F>=2,G+1=E,H=1] * CE 342: case_0(A,B,C,D,E) = 7+ eval2(A,B,C,D,F):[53]+ eval2(A,B,C,D,G):[53]+ or(H,I):[40] [C>=G,F>=A+2,G>=F,F>=2,G+1=E,H=0] * CE 343: case_0(A,B,C,D,E) = 7+ eval2(A,B,C,D,F):[53]+ eval2(A,B,C,D,G):[53]+ or(H,I):[39] [C>=G,F>=A+2,G>=F,F>=2,G+1=E,H=1] * CE 344: case_0(A,B,C,D,E) = 7+ eval2(A,B,C,D,F):[53]+ eval2(A,B,C,D,G):[multiple([41,42,43,44,45,46,47,48,49,50],[[57],[56],[55],[54],[53],[52],[51]])]+ or(H,I):[40] [G>=F,C>=F,F>=A+2,G>=3,F>=2,G+1=E,H=0] * CE 345: case_0(A,B,C,D,E) = 7+ eval2(A,B,C,D,F):[53]+ eval2(A,B,C,D,G):[multiple([41,42,43,44,45,46,47,48,49,50],[[57],[56],[55],[54],[53],[52],[51]])]+ or(H,I):[39] [G>=F,C>=F,F>=A+2,G>=3,F>=2,G+1=E,H=1] * CE 346: case_0(A,B,C,D,E) = 7+ eval2(A,B,C,D,F):[52]+ eval2(A,B,C,D,G):[56]+ or(H,I):[40] [A>=F,F>=C+2,F>=2,A+1=G,A+2=E,H=0] * CE 347: case_0(A,B,C,D,E) = 7+ eval2(A,B,C,D,F):[52]+ eval2(A,B,C,D,G):[56]+ or(H,I):[39] [A>=F,F>=C+2,F>=2,A+1=G,A+2=E,H=1] * CE 348: case_0(A,B,C,D,E) = 7+ eval2(A,B,C,D,F):[52]+ eval2(A,B,C,D,G):[54]+ or(H,I):[40] [F>=C+2,G>=A+2,A>=F,F>=2,G+1=E,H=0] * CE 349: case_0(A,B,C,D,E) = 7+ eval2(A,B,C,D,F):[52]+ eval2(A,B,C,D,G):[54]+ or(H,I):[39] [F>=C+2,G>=A+2,A>=F,F>=2,G+1=E,H=1] * CE 350: case_0(A,B,C,D,E) = 7+ eval2(A,B,C,D,F):[52]+ eval2(A,B,C,D,G):[52]+ or(H,I):[40] [A>=G,F>=C+2,G>=F,F>=2,G+1=E,H=0] * CE 351: case_0(A,B,C,D,E) = 7+ eval2(A,B,C,D,F):[52]+ eval2(A,B,C,D,G):[52]+ or(H,I):[39] [A>=G,F>=C+2,G>=F,F>=2,G+1=E,H=1] * CE 352: case_0(A,B,C,D,E) = 7+ eval2(A,B,C,D,F):[52]+ eval2(A,B,C,D,G):[multiple([41,42,43,44,45,46,47,48,49,50],[[57],[56],[55],[54],[53],[52],[51]])]+ or(H,I):[40] [G>=F,A>=F,F>=C+2,G>=3,F>=2,G+1=E,H=0] * CE 353: case_0(A,B,C,D,E) = 7+ eval2(A,B,C,D,F):[52]+ eval2(A,B,C,D,G):[multiple([41,42,43,44,45,46,47,48,49,50],[[57],[56],[55],[54],[53],[52],[51]])]+ or(H,I):[39] [G>=F,A>=F,F>=C+2,G>=3,F>=2,G+1=E,H=1] * CE 354: case_0(A,B,C,D,E) = 7+ eval2(A,B,C,D,F):[51]+ eval2(A,B,C,D,G):[57]+ or(H,I):[40] [A>=C+1,C>=F,F>=2,C+1=G,C+2=E,H=0] * CE 355: case_0(A,B,C,D,E) = 7+ eval2(A,B,C,D,F):[51]+ eval2(A,B,C,D,G):[57]+ or(H,I):[39] [A>=C+1,C>=F,F>=2,C+1=G,C+2=E,H=1] * CE 356: case_0(A,B,C,D,E) = 7+ eval2(A,B,C,D,F):[51]+ eval2(A,B,C,D,G):[56]+ or(H,I):[40] [A>=F,C>=F,F>=2,A+1=G,A+2=E,H=0] * CE 357: case_0(A,B,C,D,E) = 7+ eval2(A,B,C,D,F):[51]+ eval2(A,B,C,D,G):[56]+ or(H,I):[39] [A>=F,C>=F,F>=2,A+1=G,A+2=E,H=1] * CE 358: case_0(A,B,C,D,E) = 7+ eval2(A,B,C,D,F):[51]+ eval2(A,B,C,D,G):[55]+ or(H,I):[40] [C>=A+1,A>=F,F>=2,C+1=G,C+2=E,H=0] * CE 359: case_0(A,B,C,D,E) = 7+ eval2(A,B,C,D,F):[51]+ eval2(A,B,C,D,G):[55]+ or(H,I):[39] [C>=A+1,A>=F,F>=2,C+1=G,C+2=E,H=1] * CE 360: case_0(A,B,C,D,E) = 7+ eval2(A,B,C,D,F):[51]+ eval2(A,B,C,D,G):[54]+ or(H,I):[40] [G>=C+2,G>=A+2,C>=F,A>=F,F>=2,G+1=E,H=0] * CE 361: case_0(A,B,C,D,E) = 7+ eval2(A,B,C,D,F):[51]+ eval2(A,B,C,D,G):[54]+ or(H,I):[39] [G>=C+2,G>=A+2,C>=F,A>=F,F>=2,G+1=E,H=1] * CE 362: case_0(A,B,C,D,E) = 7+ eval2(A,B,C,D,F):[51]+ eval2(A,B,C,D,G):[53]+ or(H,I):[40] [C>=G,G>=A+2,A>=F,F>=2,G+1=E,H=0] * CE 363: case_0(A,B,C,D,E) = 7+ eval2(A,B,C,D,F):[51]+ eval2(A,B,C,D,G):[53]+ or(H,I):[39] [C>=G,G>=A+2,A>=F,F>=2,G+1=E,H=1] * CE 364: case_0(A,B,C,D,E) = 7+ eval2(A,B,C,D,F):[51]+ eval2(A,B,C,D,G):[52]+ or(H,I):[40] [A>=G,G>=C+2,C>=F,F>=2,G+1=E,H=0] * CE 365: case_0(A,B,C,D,E) = 7+ eval2(A,B,C,D,F):[51]+ eval2(A,B,C,D,G):[52]+ or(H,I):[39] [A>=G,G>=C+2,C>=F,F>=2,G+1=E,H=1] * CE 366: case_0(A,B,C,D,E) = 7+ eval2(A,B,C,D,F):[51]+ eval2(A,B,C,D,G):[51]+ or(H,I):[40] [C>=G,A>=G,G>=F,F>=2,G+1=E,H=0] * CE 367: case_0(A,B,C,D,E) = 7+ eval2(A,B,C,D,F):[51]+ eval2(A,B,C,D,G):[51]+ or(H,I):[39] [C>=G,A>=G,G>=F,F>=2,G+1=E,H=1] * CE 368: case_0(A,B,C,D,E) = 7+ eval2(A,B,C,D,F):[51]+ eval2(A,B,C,D,G):[multiple([41,42,43,44,45,46,47,48,49,50],[[57],[56],[55],[54],[53],[52],[51]])]+ or(H,I):[40] [G>=F,C>=F,A>=F,G>=3,F>=2,G+1=E,H=0] * CE 369: case_0(A,B,C,D,E) = 7+ eval2(A,B,C,D,F):[51]+ eval2(A,B,C,D,G):[multiple([41,42,43,44,45,46,47,48,49,50],[[57],[56],[55],[54],[53],[52],[51]])]+ or(H,I):[39] [G>=F,C>=F,A>=F,G>=3,F>=2,G+1=E,H=1] * CE 370: case_0(A,B,C,D,E) = 7+ eval2(A,B,C,D,F):[multiple([41,42,43,44,45,46,47,48,49,50],[[57],[56],[55],[54],[53],[52],[51]])]+ eval2(A,B,C,D,G):[57]+ or(H,I):[40] [A>=C+1,C+1>=F,F>=3,C+1=G,C+2=E,H=0] * CE 371: case_0(A,B,C,D,E) = 7+ eval2(A,B,C,D,F):[multiple([41,42,43,44,45,46,47,48,49,50],[[57],[56],[55],[54],[53],[52],[51]])]+ eval2(A,B,C,D,G):[57]+ or(H,I):[39] [A>=C+1,C+1>=F,F>=3,C+1=G,C+2=E,H=1] * CE 372: case_0(A,B,C,D,E) = 7+ eval2(A,B,C,D,F):[multiple([41,42,43,44,45,46,47,48,49,50],[[57],[56],[55],[54],[53],[52],[51]])]+ eval2(A,B,C,D,G):[56]+ or(H,I):[40] [A+1>=F,F>=3,A+1=G,A+2=E,H=0] * CE 373: case_0(A,B,C,D,E) = 7+ eval2(A,B,C,D,F):[multiple([41,42,43,44,45,46,47,48,49,50],[[57],[56],[55],[54],[53],[52],[51]])]+ eval2(A,B,C,D,G):[56]+ or(H,I):[39] [A+1>=F,F>=3,A+1=G,A+2=E,H=1] * CE 374: case_0(A,B,C,D,E) = 7+ eval2(A,B,C,D,F):[multiple([41,42,43,44,45,46,47,48,49,50],[[57],[56],[55],[54],[53],[52],[51]])]+ eval2(A,B,C,D,G):[55]+ or(H,I):[40] [C>=A+1,C+1>=F,F>=3,C+1=G,C+2=E,H=0] * CE 375: case_0(A,B,C,D,E) = 7+ eval2(A,B,C,D,F):[multiple([41,42,43,44,45,46,47,48,49,50],[[57],[56],[55],[54],[53],[52],[51]])]+ eval2(A,B,C,D,G):[55]+ or(H,I):[39] [C>=A+1,C+1>=F,F>=3,C+1=G,C+2=E,H=1] * CE 376: case_0(A,B,C,D,E) = 7+ eval2(A,B,C,D,F):[multiple([41,42,43,44,45,46,47,48,49,50],[[57],[56],[55],[54],[53],[52],[51]])]+ eval2(A,B,C,D,G):[54]+ or(H,I):[40] [G>=C+2,G>=A+2,G>=F,F>=3,G+1=E,H=0] * CE 377: case_0(A,B,C,D,E) = 7+ eval2(A,B,C,D,F):[multiple([41,42,43,44,45,46,47,48,49,50],[[57],[56],[55],[54],[53],[52],[51]])]+ eval2(A,B,C,D,G):[54]+ or(H,I):[39] [G>=C+2,G>=A+2,G>=F,F>=3,G+1=E,H=1] * CE 378: case_0(A,B,C,D,E) = 7+ eval2(A,B,C,D,F):[multiple([41,42,43,44,45,46,47,48,49,50],[[57],[56],[55],[54],[53],[52],[51]])]+ eval2(A,B,C,D,G):[53]+ or(H,I):[40] [C>=G,G>=A+2,G>=F,F>=3,G+1=E,H=0] * CE 379: case_0(A,B,C,D,E) = 7+ eval2(A,B,C,D,F):[multiple([41,42,43,44,45,46,47,48,49,50],[[57],[56],[55],[54],[53],[52],[51]])]+ eval2(A,B,C,D,G):[53]+ or(H,I):[39] [C>=G,G>=A+2,G>=F,F>=3,G+1=E,H=1] * CE 380: case_0(A,B,C,D,E) = 7+ eval2(A,B,C,D,F):[multiple([41,42,43,44,45,46,47,48,49,50],[[57],[56],[55],[54],[53],[52],[51]])]+ eval2(A,B,C,D,G):[52]+ or(H,I):[40] [A>=G,G>=C+2,G>=F,F>=3,G+1=E,H=0] * CE 381: case_0(A,B,C,D,E) = 7+ eval2(A,B,C,D,F):[multiple([41,42,43,44,45,46,47,48,49,50],[[57],[56],[55],[54],[53],[52],[51]])]+ eval2(A,B,C,D,G):[52]+ or(H,I):[39] [A>=G,G>=C+2,G>=F,F>=3,G+1=E,H=1] * CE 382: case_0(A,B,C,D,E) = 7+ eval2(A,B,C,D,F):[multiple([41,42,43,44,45,46,47,48,49,50],[[57],[56],[55],[54],[53],[52],[51]])]+ eval2(A,B,C,D,G):[51]+ or(H,I):[40] [C>=G,A>=G,G>=F,F>=3,G+1=E,H=0] * CE 383: case_0(A,B,C,D,E) = 7+ eval2(A,B,C,D,F):[multiple([41,42,43,44,45,46,47,48,49,50],[[57],[56],[55],[54],[53],[52],[51]])]+ eval2(A,B,C,D,G):[51]+ or(H,I):[39] [C>=G,A>=G,G>=F,F>=3,G+1=E,H=1] * CE 384: case_0(A,B,C,D,E) = 7+ eval2(A,B,C,D,F):[multiple([41,42,43,44,45,46,47,48,49,50],[[57],[56],[55],[54],[53],[52],[51]])]+ eval2(A,B,C,D,G):[multiple([41,42,43,44,45,46,47,48,49,50],[[57],[56],[55],[54],[53],[52],[51]])]+ or(H,I):[40] [G>=F,F>=3,G+1=E,H=0] * CE 385: case_0(A,B,C,D,E) = 7+ eval2(A,B,C,D,F):[multiple([41,42,43,44,45,46,47,48,49,50],[[57],[56],[55],[54],[53],[52],[51]])]+ eval2(A,B,C,D,G):[multiple([41,42,43,44,45,46,47,48,49,50],[[57],[56],[55],[54],[53],[52],[51]])]+ or(H,I):[39] [G>=F,F>=3,G+1=E,H=1] * CE 386: case_0(A,B,C,D,E) = 2+ case_1(A,B,C,D,F,A):[36] [A>=1,A+1=F,A+1=E] * CE 387: case_0(A,B,C,D,E) = 2+ case_1(A,B,C,D,F,C):[35] [C>=A+1,C>=1,C+1=F,C+1=E] * CE 388: case_0(A,B,C,D,E) = 2+ case_1(A,B,C,D,F,C):[34] [A>=C+1,C>=1,C+1=F,C+1=E] * CE 389: case_0(A,B,C,D,E) = 2+ case_1(A,B,C,D,E,F):[33] [E>=C+2,E>=A+2,E>=2,E=F+1] * CE 390: case_0(A,B,C,D,E) = 2+ case_1(A,B,C,D,E,F):[32] [C>=E,E>=A+2,E>=2,E=F+1] * CE 391: case_0(A,B,C,D,E) = 2+ case_1(A,B,C,D,E,F):[31] [A>=E,E>=C+2,E>=2,E=F+1] * CE 392: case_0(A,B,C,D,E) = 2+ case_1(A,B,C,D,E,F):[30] [C>=E,A>=E,E>=2,E=F+1] ### Cost equations --> "Loop" of case_0/5 * CEs [383] --> Loop 58 * CEs [382] --> Loop 59 * CEs [291] --> Loop 60 * CEs [290] --> Loop 61 * CEs [227] --> Loop 62 * CEs [226] --> Loop 63 * CEs [135] --> Loop 64 * CEs [134] --> Loop 65 * CEs [381] --> Loop 66 * CEs [380] --> Loop 67 * CEs [287] --> Loop 68 * CEs [286] --> Loop 69 * CEs [225] --> Loop 70 * CEs [224] --> Loop 71 * CEs [131] --> Loop 72 * CEs [130] --> Loop 73 * CEs [379] --> Loop 74 * CEs [378] --> Loop 75 * CEs [279] --> Loop 76 * CEs [278] --> Loop 77 * CEs [223] --> Loop 78 * CEs [222] --> Loop 79 * CEs [123] --> Loop 80 * CEs [122] --> Loop 81 * CEs [377] --> Loop 82 * CEs [376] --> Loop 83 * CEs [337] --> Loop 84 * CEs [336] --> Loop 85 * CEs [299] --> Loop 86 * CEs [298] --> Loop 87 * CEs [271] --> Loop 88 * CEs [270] --> Loop 89 * CEs [221] --> Loop 90 * CEs [220] --> Loop 91 * CEs [181] --> Loop 92 * CEs [180] --> Loop 93 * CEs [143] --> Loop 94 * CEs [142] --> Loop 95 * CEs [115] --> Loop 96 * CEs [114] --> Loop 97 * CEs [385] --> Loop 98 * CEs [384] --> Loop 99 * CEs [307] --> Loop 100 * CEs [306] --> Loop 101 * CEs [229] --> Loop 102 * CEs [228] --> Loop 103 * CEs [151] --> Loop 104 * CEs [150] --> Loop 105 * CEs [73] --> Loop 106 * CEs [72] --> Loop 107 * CEs [367] --> Loop 108 * CEs [366] --> Loop 109 * CEs [289] --> Loop 110 * CEs [288] --> Loop 111 * CEs [211] --> Loop 112 * CEs [210] --> Loop 113 * CEs [133] --> Loop 114 * CEs [132] --> Loop 115 * CEs [71] --> Loop 116 * CEs [70] --> Loop 117 * CEs [351] --> Loop 118 * CEs [350] --> Loop 119 * CEs [283] --> Loop 120 * CEs [282] --> Loop 121 * CEs [195] --> Loop 122 * CEs [194] --> Loop 123 * CEs [127] --> Loop 124 * CEs [126] --> Loop 125 * CEs [69] --> Loop 126 * CEs [68] --> Loop 127 * CEs [343] --> Loop 128 * CEs [342] --> Loop 129 * CEs [275] --> Loop 130 * CEs [274] --> Loop 131 * CEs [187] --> Loop 132 * CEs [186] --> Loop 133 * CEs [119] --> Loop 134 * CEs [118] --> Loop 135 * CEs [67] --> Loop 136 * CEs [66] --> Loop 137 * CEs [335] --> Loop 138 * CEs [334] --> Loop 139 * CEs [263] --> Loop 140 * CEs [262] --> Loop 141 * CEs [179] --> Loop 142 * CEs [178] --> Loop 143 * CEs [107] --> Loop 144 * CEs [106] --> Loop 145 * CEs [65] --> Loop 146 * CEs [64] --> Loop 147 * CEs [392] --> Loop 148 * CEs [391] --> Loop 149 * CEs [390] --> Loop 150 * CEs [389] --> Loop 151 * CEs [365] --> Loop 152 * CEs [364] --> Loop 153 * CEs [285] --> Loop 154 * CEs [284] --> Loop 155 * CEs [209] --> Loop 156 * CEs [208] --> Loop 157 * CEs [129] --> Loop 158 * CEs [128] --> Loop 159 * CEs [341] --> Loop 160 * CEs [340] --> Loop 161 * CEs [265] --> Loop 162 * CEs [264] --> Loop 163 * CEs [185] --> Loop 164 * CEs [184] --> Loop 165 * CEs [109] --> Loop 166 * CEs [108] --> Loop 167 * CEs [345] --> Loop 168 * CEs [344] --> Loop 169 * CEs [301] --> Loop 170 * CEs [300] --> Loop 171 * CEs [189] --> Loop 172 * CEs [188] --> Loop 173 * CEs [145] --> Loop 174 * CEs [144] --> Loop 175 * CEs [315] --> Loop 176 * CEs [314] --> Loop 177 * CEs [281] --> Loop 178 * CEs [280] --> Loop 179 * CEs [159] --> Loop 180 * CEs [158] --> Loop 181 * CEs [125] --> Loop 182 * CEs [124] --> Loop 183 * CEs [313] --> Loop 184 * CEs [312] --> Loop 185 * CEs [257] --> Loop 186 * CEs [256] --> Loop 187 * CEs [157] --> Loop 188 * CEs [156] --> Loop 189 * CEs [101] --> Loop 190 * CEs [100] --> Loop 191 * CEs [331] --> Loop 192 * CEs [330] --> Loop 193 * CEs [261] --> Loop 194 * CEs [260] --> Loop 195 * CEs [175] --> Loop 196 * CEs [174] --> Loop 197 * CEs [105] --> Loop 198 * CEs [104] --> Loop 199 * CEs [317] --> Loop 200 * CEs [316] --> Loop 201 * CEs [293] --> Loop 202 * CEs [292] --> Loop 203 * CEs [161] --> Loop 204 * CEs [160] --> Loop 205 * CEs [137] --> Loop 206 * CEs [136] --> Loop 207 * CEs [333] --> Loop 208 * CEs [332] --> Loop 209 * CEs [297] --> Loop 210 * CEs [296] --> Loop 211 * CEs [177] --> Loop 212 * CEs [176] --> Loop 213 * CEs [141] --> Loop 214 * CEs [140] --> Loop 215 * CEs [363] --> Loop 216 * CEs [362] --> Loop 217 * CEs [277] --> Loop 218 * CEs [276] --> Loop 219 * CEs [207] --> Loop 220 * CEs [206] --> Loop 221 * CEs [121] --> Loop 222 * CEs [120] --> Loop 223 * CEs [349] --> Loop 224 * CEs [348] --> Loop 225 * CEs [267] --> Loop 226 * CEs [266] --> Loop 227 * CEs [193] --> Loop 228 * CEs [192] --> Loop 229 * CEs [111] --> Loop 230 * CEs [110] --> Loop 231 * CEs [353] --> Loop 232 * CEs [352] --> Loop 233 * CEs [303] --> Loop 234 * CEs [302] --> Loop 235 * CEs [197] --> Loop 236 * CEs [196] --> Loop 237 * CEs [147] --> Loop 238 * CEs [146] --> Loop 239 * CEs [361] --> Loop 240 * CEs [360] --> Loop 241 * CEs [269] --> Loop 242 * CEs [268] --> Loop 243 * CEs [205] --> Loop 244 * CEs [204] --> Loop 245 * CEs [113] --> Loop 246 * CEs [112] --> Loop 247 * CEs [369] --> Loop 248 * CEs [368] --> Loop 249 * CEs [305] --> Loop 250 * CEs [304] --> Loop 251 * CEs [213] --> Loop 252 * CEs [212] --> Loop 253 * CEs [149] --> Loop 254 * CEs [148] --> Loop 255 * CEs [325] --> Loop 256 * CEs [324] --> Loop 257 * CEs [273] --> Loop 258 * CEs [272] --> Loop 259 * CEs [169] --> Loop 260 * CEs [168] --> Loop 261 * CEs [117] --> Loop 262 * CEs [116] --> Loop 263 * CEs [323] --> Loop 264 * CEs [322] --> Loop 265 * CEs [259] --> Loop 266 * CEs [258] --> Loop 267 * CEs [167] --> Loop 268 * CEs [166] --> Loop 269 * CEs [103] --> Loop 270 * CEs [102] --> Loop 271 * CEs [327] --> Loop 272 * CEs [326] --> Loop 273 * CEs [295] --> Loop 274 * CEs [294] --> Loop 275 * CEs [171] --> Loop 276 * CEs [170] --> Loop 277 * CEs [139] --> Loop 278 * CEs [138] --> Loop 279 * CEs [387] --> Loop 280 * CEs [329] --> Loop 281 * CEs [328] --> Loop 282 * CEs [249] --> Loop 283 * CEs [248] --> Loop 284 * CEs [173] --> Loop 285 * CEs [172] --> Loop 286 * CEs [93] --> Loop 287 * CEs [92] --> Loop 288 * CEs [63] --> Loop 289 * CEs [62] --> Loop 290 * CEs [359] --> Loop 291 * CEs [358] --> Loop 292 * CEs [253] --> Loop 293 * CEs [252] --> Loop 294 * CEs [203] --> Loop 295 * CEs [202] --> Loop 296 * CEs [97] --> Loop 297 * CEs [96] --> Loop 298 * CEs [321] --> Loop 299 * CEs [320] --> Loop 300 * CEs [247] --> Loop 301 * CEs [246] --> Loop 302 * CEs [165] --> Loop 303 * CEs [164] --> Loop 304 * CEs [91] --> Loop 305 * CEs [90] --> Loop 306 * CEs [386] --> Loop 307 * CEs [311] --> Loop 308 * CEs [310] --> Loop 309 * CEs [237] --> Loop 310 * CEs [236] --> Loop 311 * CEs [155] --> Loop 312 * CEs [154] --> Loop 313 * CEs [81] --> Loop 314 * CEs [80] --> Loop 315 * CEs [347] --> Loop 316 * CEs [346] --> Loop 317 * CEs [241] --> Loop 318 * CEs [240] --> Loop 319 * CEs [191] --> Loop 320 * CEs [190] --> Loop 321 * CEs [85] --> Loop 322 * CEs [84] --> Loop 323 * CEs [357] --> Loop 324 * CEs [356] --> Loop 325 * CEs [243] --> Loop 326 * CEs [242] --> Loop 327 * CEs [201] --> Loop 328 * CEs [200] --> Loop 329 * CEs [87] --> Loop 330 * CEs [86] --> Loop 331 * CEs [373] --> Loop 332 * CEs [372] --> Loop 333 * CEs [245] --> Loop 334 * CEs [244] --> Loop 335 * CEs [217] --> Loop 336 * CEs [216] --> Loop 337 * CEs [89] --> Loop 338 * CEs [88] --> Loop 339 * CEs [319] --> Loop 340 * CEs [318] --> Loop 341 * CEs [239] --> Loop 342 * CEs [238] --> Loop 343 * CEs [163] --> Loop 344 * CEs [162] --> Loop 345 * CEs [83] --> Loop 346 * CEs [82] --> Loop 347 * CEs [61] --> Loop 348 * CEs [60] --> Loop 349 * CEs [371] --> Loop 350 * CEs [370] --> Loop 351 * CEs [355] --> Loop 352 * CEs [354] --> Loop 353 * CEs [235] --> Loop 354 * CEs [234] --> Loop 355 * CEs [233] --> Loop 356 * CEs [232] --> Loop 357 * CEs [215] --> Loop 358 * CEs [214] --> Loop 359 * CEs [199] --> Loop 360 * CEs [198] --> Loop 361 * CEs [79] --> Loop 362 * CEs [78] --> Loop 363 * CEs [77] --> Loop 364 * CEs [76] --> Loop 365 * CEs [339] --> Loop 366 * CEs [338] --> Loop 367 * CEs [251] --> Loop 368 * CEs [250] --> Loop 369 * CEs [183] --> Loop 370 * CEs [182] --> Loop 371 * CEs [95] --> Loop 372 * CEs [94] --> Loop 373 * CEs [375] --> Loop 374 * CEs [374] --> Loop 375 * CEs [255] --> Loop 376 * CEs [254] --> Loop 377 * CEs [219] --> Loop 378 * CEs [218] --> Loop 379 * CEs [99] --> Loop 380 * CEs [98] --> Loop 381 * CEs [309] --> Loop 382 * CEs [308] --> Loop 383 * CEs [231] --> Loop 384 * CEs [230] --> Loop 385 * CEs [153] --> Loop 386 * CEs [152] --> Loop 387 * CEs [75] --> Loop 388 * CEs [74] --> Loop 389 * CEs [59] --> Loop 390 * CEs [58] --> Loop 391 * CEs [388] --> Loop 392 #### Loops of case_0/5 * Loop 58: case_0(A,B,C,D,E) [C+1>=E,A+1>=E,E>=4] * Loop 59: case_0(A,B,C,D,E) [C+1>=E,A+1>=E,E>=4] * Loop 60: case_0(A,B,C,D,E) [C+1>=E,A+1>=E,E>=4] * Loop 61: case_0(A,B,C,D,E) [C+1>=E,A+1>=E,E>=4] * Loop 62: case_0(A,B,C,D,E) [C+1>=E,A+1>=E,E>=4] * Loop 63: case_0(A,B,C,D,E) [C+1>=E,A+1>=E,E>=4] * Loop 64: case_0(A,B,C,D,E) [C+1>=E,A+1>=E,E>=4] * Loop 65: case_0(A,B,C,D,E) [C+1>=E,A+1>=E,E>=4] * Loop 66: case_0(A,B,C,D,E) [A+1>=E,E>=C+3,E>=4] * Loop 67: case_0(A,B,C,D,E) [A+1>=E,E>=C+3,E>=4] * Loop 68: case_0(A,B,C,D,E) [A+1>=E,E>=C+3,E>=4] * Loop 69: case_0(A,B,C,D,E) [A+1>=E,E>=C+3,E>=4] * Loop 70: case_0(A,B,C,D,E) [A+1>=E,E>=C+3,E>=4] * Loop 71: case_0(A,B,C,D,E) [A+1>=E,E>=C+3,E>=4] * Loop 72: case_0(A,B,C,D,E) [A+1>=E,E>=C+3,E>=4] * Loop 73: case_0(A,B,C,D,E) [A+1>=E,E>=C+3,E>=4] * Loop 74: case_0(A,B,C,D,E) [C+1>=E,E>=A+3,E>=4] * Loop 75: case_0(A,B,C,D,E) [C+1>=E,E>=A+3,E>=4] * Loop 76: case_0(A,B,C,D,E) [C+1>=E,E>=A+3,E>=4] * Loop 77: case_0(A,B,C,D,E) [C+1>=E,E>=A+3,E>=4] * Loop 78: case_0(A,B,C,D,E) [C+1>=E,E>=A+3,E>=4] * Loop 79: case_0(A,B,C,D,E) [C+1>=E,E>=A+3,E>=4] * Loop 80: case_0(A,B,C,D,E) [C+1>=E,E>=A+3,E>=4] * Loop 81: case_0(A,B,C,D,E) [C+1>=E,E>=A+3,E>=4] * Loop 82: case_0(A,B,C,D,E) [E>=C+3,E>=A+3,E>=4] * Loop 83: case_0(A,B,C,D,E) [E>=C+3,E>=A+3,E>=4] * Loop 84: case_0(A,B,C,D,E) [E>=C+3,E>=A+3,E>=4] * Loop 85: case_0(A,B,C,D,E) [E>=C+3,E>=A+3,E>=4] * Loop 86: case_0(A,B,C,D,E) [E>=C+3,E>=A+3,E>=4] * Loop 87: case_0(A,B,C,D,E) [E>=C+3,E>=A+3,E>=4] * Loop 88: case_0(A,B,C,D,E) [E>=C+3,E>=A+3,E>=4] * Loop 89: case_0(A,B,C,D,E) [E>=C+3,E>=A+3,E>=4] * Loop 90: case_0(A,B,C,D,E) [E>=C+3,E>=A+3,E>=4] * Loop 91: case_0(A,B,C,D,E) [E>=C+3,E>=A+3,E>=4] * Loop 92: case_0(A,B,C,D,E) [E>=C+3,E>=A+3,E>=4] * Loop 93: case_0(A,B,C,D,E) [E>=C+3,E>=A+3,E>=4] * Loop 94: case_0(A,B,C,D,E) [E>=C+3,E>=A+3,E>=4] * Loop 95: case_0(A,B,C,D,E) [E>=C+3,E>=A+3,E>=4] * Loop 96: case_0(A,B,C,D,E) [E>=C+3,E>=A+3,E>=4] * Loop 97: case_0(A,B,C,D,E) [E>=C+3,E>=A+3,E>=4] * Loop 98: case_0(A,B,C,D,E) [E>=4] * Loop 99: case_0(A,B,C,D,E) [E>=4] * Loop 100: case_0(A,B,C,D,E) [E>=4] * Loop 101: case_0(A,B,C,D,E) [E>=4] * Loop 102: case_0(A,B,C,D,E) [E>=4] * Loop 103: case_0(A,B,C,D,E) [E>=4] * Loop 104: case_0(A,B,C,D,E) [E>=4] * Loop 105: case_0(A,B,C,D,E) [E>=4] * Loop 106: case_0(A,B,C,D,E) [E>=4] * Loop 107: case_0(A,B,C,D,E) [E>=4] * Loop 108: case_0(A,B,C,D,E) [C+1>=E,A+1>=E,E>=3] * Loop 109: case_0(A,B,C,D,E) [C+1>=E,A+1>=E,E>=3] * Loop 110: case_0(A,B,C,D,E) [C+1>=E,A+1>=E,E>=3] * Loop 111: case_0(A,B,C,D,E) [C+1>=E,A+1>=E,E>=3] * Loop 112: case_0(A,B,C,D,E) [C+1>=E,A+1>=E,E>=3] * Loop 113: case_0(A,B,C,D,E) [C+1>=E,A+1>=E,E>=3] * Loop 114: case_0(A,B,C,D,E) [C+1>=E,A+1>=E,E>=3] * Loop 115: case_0(A,B,C,D,E) [C+1>=E,A+1>=E,E>=3] * Loop 116: case_0(A,B,C,D,E) [C+1>=E,A+1>=E,E>=3] * Loop 117: case_0(A,B,C,D,E) [C+1>=E,A+1>=E,E>=3] * Loop 118: case_0(A,B,C,D,E) [A+1>=E,E>=C+3,E>=3] * Loop 119: case_0(A,B,C,D,E) [A+1>=E,E>=C+3,E>=3] * Loop 120: case_0(A,B,C,D,E) [A+1>=E,E>=C+3,E>=3] * Loop 121: case_0(A,B,C,D,E) [A+1>=E,E>=C+3,E>=3] * Loop 122: case_0(A,B,C,D,E) [A+1>=E,E>=C+3,E>=3] * Loop 123: case_0(A,B,C,D,E) [A+1>=E,E>=C+3,E>=3] * Loop 124: case_0(A,B,C,D,E) [A+1>=E,E>=C+3,E>=3] * Loop 125: case_0(A,B,C,D,E) [A+1>=E,E>=C+3,E>=3] * Loop 126: case_0(A,B,C,D,E) [A+1>=E,E>=C+3,E>=3] * Loop 127: case_0(A,B,C,D,E) [A+1>=E,E>=C+3,E>=3] * Loop 128: case_0(A,B,C,D,E) [C+1>=E,E>=A+3,E>=3] * Loop 129: case_0(A,B,C,D,E) [C+1>=E,E>=A+3,E>=3] * Loop 130: case_0(A,B,C,D,E) [C+1>=E,E>=A+3,E>=3] * Loop 131: case_0(A,B,C,D,E) [C+1>=E,E>=A+3,E>=3] * Loop 132: case_0(A,B,C,D,E) [C+1>=E,E>=A+3,E>=3] * Loop 133: case_0(A,B,C,D,E) [C+1>=E,E>=A+3,E>=3] * Loop 134: case_0(A,B,C,D,E) [C+1>=E,E>=A+3,E>=3] * Loop 135: case_0(A,B,C,D,E) [C+1>=E,E>=A+3,E>=3] * Loop 136: case_0(A,B,C,D,E) [C+1>=E,E>=A+3,E>=3] * Loop 137: case_0(A,B,C,D,E) [C+1>=E,E>=A+3,E>=3] * Loop 138: case_0(A,B,C,D,E) [E>=C+3,E>=A+3,E>=3] * Loop 139: case_0(A,B,C,D,E) [E>=C+3,E>=A+3,E>=3] * Loop 140: case_0(A,B,C,D,E) [E>=C+3,E>=A+3,E>=3] * Loop 141: case_0(A,B,C,D,E) [E>=C+3,E>=A+3,E>=3] * Loop 142: case_0(A,B,C,D,E) [E>=C+3,E>=A+3,E>=3] * Loop 143: case_0(A,B,C,D,E) [E>=C+3,E>=A+3,E>=3] * Loop 144: case_0(A,B,C,D,E) [E>=C+3,E>=A+3,E>=3] * Loop 145: case_0(A,B,C,D,E) [E>=C+3,E>=A+3,E>=3] * Loop 146: case_0(A,B,C,D,E) [E>=C+3,E>=A+3,E>=3] * Loop 147: case_0(A,B,C,D,E) [E>=C+3,E>=A+3,E>=3] * Loop 148: case_0(A,B,C,D,E) [C>=E,A>=E,E>=2] * Loop 149: case_0(A,B,C,D,E) [A>=E,E>=C+2,E>=2] * Loop 150: case_0(A,B,C,D,E) [C>=E,E>=A+2,E>=2] * Loop 151: case_0(A,B,C,D,E) [E>=C+2,E>=A+2,E>=2] * Loop 152: case_0(A,B,C,D,E) [A+1>=E,E>=C+3,C>=2] * Loop 153: case_0(A,B,C,D,E) [A+1>=E,E>=C+3,C>=2] * Loop 154: case_0(A,B,C,D,E) [A+1>=E,E>=C+3,C>=2] * Loop 155: case_0(A,B,C,D,E) [A+1>=E,E>=C+3,C>=2] * Loop 156: case_0(A,B,C,D,E) [A+1>=E,E>=C+3,C>=2] * Loop 157: case_0(A,B,C,D,E) [A+1>=E,E>=C+3,C>=2] * Loop 158: case_0(A,B,C,D,E) [A+1>=E,E>=C+3,C>=2] * Loop 159: case_0(A,B,C,D,E) [A+1>=E,E>=C+3,C>=2] * Loop 160: case_0(A,B,C,D,E) [E>=C+3,C>=A+2,C>=2] * Loop 161: case_0(A,B,C,D,E) [E>=C+3,C>=A+2,C>=2] * Loop 162: case_0(A,B,C,D,E) [E>=C+3,C>=A+2,C>=2] * Loop 163: case_0(A,B,C,D,E) [E>=C+3,C>=A+2,C>=2] * Loop 164: case_0(A,B,C,D,E) [E>=C+3,C>=A+2,C>=2] * Loop 165: case_0(A,B,C,D,E) [E>=C+3,C>=A+2,C>=2] * Loop 166: case_0(A,B,C,D,E) [E>=C+3,C>=A+2,C>=2] * Loop 167: case_0(A,B,C,D,E) [E>=C+3,C>=A+2,C>=2] * Loop 168: case_0(A,B,C,D,E) [E>=A+3,C>=A+2,E>=4,C>=2] * Loop 169: case_0(A,B,C,D,E) [E>=A+3,C>=A+2,E>=4,C>=2] * Loop 170: case_0(A,B,C,D,E) [E>=A+3,C>=A+2,E>=4,C>=2] * Loop 171: case_0(A,B,C,D,E) [E>=A+3,C>=A+2,E>=4,C>=2] * Loop 172: case_0(A,B,C,D,E) [E>=A+3,C>=A+2,E>=4,C>=2] * Loop 173: case_0(A,B,C,D,E) [E>=A+3,C>=A+2,E>=4,C>=2] * Loop 174: case_0(A,B,C,D,E) [E>=A+3,C>=A+2,E>=4,C>=2] * Loop 175: case_0(A,B,C,D,E) [E>=A+3,C>=A+2,E>=4,C>=2] * Loop 176: case_0(A,B,C,D,E) [A+1>=E,E>=C+3,C>=1] * Loop 177: case_0(A,B,C,D,E) [A+1>=E,E>=C+3,C>=1] * Loop 178: case_0(A,B,C,D,E) [A+1>=E,E>=C+3,C>=1] * Loop 179: case_0(A,B,C,D,E) [A+1>=E,E>=C+3,C>=1] * Loop 180: case_0(A,B,C,D,E) [A+1>=E,E>=C+3,C>=1] * Loop 181: case_0(A,B,C,D,E) [A+1>=E,E>=C+3,C>=1] * Loop 182: case_0(A,B,C,D,E) [A+1>=E,E>=C+3,C>=1] * Loop 183: case_0(A,B,C,D,E) [A+1>=E,E>=C+3,C>=1] * Loop 184: case_0(A,B,C,D,E) [A>=C+1,E>=A+3,C>=1] * Loop 185: case_0(A,B,C,D,E) [A>=C+1,E>=A+3,C>=1] * Loop 186: case_0(A,B,C,D,E) [A>=C+1,E>=A+3,C>=1] * Loop 187: case_0(A,B,C,D,E) [A>=C+1,E>=A+3,C>=1] * Loop 188: case_0(A,B,C,D,E) [A>=C+1,E>=A+3,C>=1] * Loop 189: case_0(A,B,C,D,E) [A>=C+1,E>=A+3,C>=1] * Loop 190: case_0(A,B,C,D,E) [A>=C+1,E>=A+3,C>=1] * Loop 191: case_0(A,B,C,D,E) [A>=C+1,E>=A+3,C>=1] * Loop 192: case_0(A,B,C,D,E) [E>=C+3,C>=A+1,C>=1] * Loop 193: case_0(A,B,C,D,E) [E>=C+3,C>=A+1,C>=1] * Loop 194: case_0(A,B,C,D,E) [E>=C+3,C>=A+1,C>=1] * Loop 195: case_0(A,B,C,D,E) [E>=C+3,C>=A+1,C>=1] * Loop 196: case_0(A,B,C,D,E) [E>=C+3,C>=A+1,C>=1] * Loop 197: case_0(A,B,C,D,E) [E>=C+3,C>=A+1,C>=1] * Loop 198: case_0(A,B,C,D,E) [E>=C+3,C>=A+1,C>=1] * Loop 199: case_0(A,B,C,D,E) [E>=C+3,C>=A+1,C>=1] * Loop 200: case_0(A,B,C,D,E) [E>=C+2,A>=C+1,E>=4,C>=1] * Loop 201: case_0(A,B,C,D,E) [E>=C+2,A>=C+1,E>=4,C>=1] * Loop 202: case_0(A,B,C,D,E) [E>=C+2,A>=C+1,E>=4,C>=1] * Loop 203: case_0(A,B,C,D,E) [E>=C+2,A>=C+1,E>=4,C>=1] * Loop 204: case_0(A,B,C,D,E) [E>=C+2,A>=C+1,E>=4,C>=1] * Loop 205: case_0(A,B,C,D,E) [E>=C+2,A>=C+1,E>=4,C>=1] * Loop 206: case_0(A,B,C,D,E) [E>=C+2,A>=C+1,E>=4,C>=1] * Loop 207: case_0(A,B,C,D,E) [E>=C+2,A>=C+1,E>=4,C>=1] * Loop 208: case_0(A,B,C,D,E) [E>=C+2,C>=A+1,E>=4,C>=1] * Loop 209: case_0(A,B,C,D,E) [E>=C+2,C>=A+1,E>=4,C>=1] * Loop 210: case_0(A,B,C,D,E) [E>=C+2,C>=A+1,E>=4,C>=1] * Loop 211: case_0(A,B,C,D,E) [E>=C+2,C>=A+1,E>=4,C>=1] * Loop 212: case_0(A,B,C,D,E) [E>=C+2,C>=A+1,E>=4,C>=1] * Loop 213: case_0(A,B,C,D,E) [E>=C+2,C>=A+1,E>=4,C>=1] * Loop 214: case_0(A,B,C,D,E) [E>=C+2,C>=A+1,E>=4,C>=1] * Loop 215: case_0(A,B,C,D,E) [E>=C+2,C>=A+1,E>=4,C>=1] * Loop 216: case_0(A,B,C,D,E) [C+1>=E,E>=A+3,A>=2] * Loop 217: case_0(A,B,C,D,E) [C+1>=E,E>=A+3,A>=2] * Loop 218: case_0(A,B,C,D,E) [C+1>=E,E>=A+3,A>=2] * Loop 219: case_0(A,B,C,D,E) [C+1>=E,E>=A+3,A>=2] * Loop 220: case_0(A,B,C,D,E) [C+1>=E,E>=A+3,A>=2] * Loop 221: case_0(A,B,C,D,E) [C+1>=E,E>=A+3,A>=2] * Loop 222: case_0(A,B,C,D,E) [C+1>=E,E>=A+3,A>=2] * Loop 223: case_0(A,B,C,D,E) [C+1>=E,E>=A+3,A>=2] * Loop 224: case_0(A,B,C,D,E) [A>=C+2,E>=A+3,A>=2] * Loop 225: case_0(A,B,C,D,E) [A>=C+2,E>=A+3,A>=2] * Loop 226: case_0(A,B,C,D,E) [A>=C+2,E>=A+3,A>=2] * Loop 227: case_0(A,B,C,D,E) [A>=C+2,E>=A+3,A>=2] * Loop 228: case_0(A,B,C,D,E) [A>=C+2,E>=A+3,A>=2] * Loop 229: case_0(A,B,C,D,E) [A>=C+2,E>=A+3,A>=2] * Loop 230: case_0(A,B,C,D,E) [A>=C+2,E>=A+3,A>=2] * Loop 231: case_0(A,B,C,D,E) [A>=C+2,E>=A+3,A>=2] * Loop 232: case_0(A,B,C,D,E) [E>=C+3,A>=C+2,E>=4,A>=2] * Loop 233: case_0(A,B,C,D,E) [E>=C+3,A>=C+2,E>=4,A>=2] * Loop 234: case_0(A,B,C,D,E) [E>=C+3,A>=C+2,E>=4,A>=2] * Loop 235: case_0(A,B,C,D,E) [E>=C+3,A>=C+2,E>=4,A>=2] * Loop 236: case_0(A,B,C,D,E) [E>=C+3,A>=C+2,E>=4,A>=2] * Loop 237: case_0(A,B,C,D,E) [E>=C+3,A>=C+2,E>=4,A>=2] * Loop 238: case_0(A,B,C,D,E) [E>=C+3,A>=C+2,E>=4,A>=2] * Loop 239: case_0(A,B,C,D,E) [E>=C+3,A>=C+2,E>=4,A>=2] * Loop 240: case_0(A,B,C,D,E) [E>=C+3,E>=A+3,C>=2,A>=2] * Loop 241: case_0(A,B,C,D,E) [E>=C+3,E>=A+3,C>=2,A>=2] * Loop 242: case_0(A,B,C,D,E) [E>=C+3,E>=A+3,C>=2,A>=2] * Loop 243: case_0(A,B,C,D,E) [E>=C+3,E>=A+3,C>=2,A>=2] * Loop 244: case_0(A,B,C,D,E) [E>=C+3,E>=A+3,C>=2,A>=2] * Loop 245: case_0(A,B,C,D,E) [E>=C+3,E>=A+3,C>=2,A>=2] * Loop 246: case_0(A,B,C,D,E) [E>=C+3,E>=A+3,C>=2,A>=2] * Loop 247: case_0(A,B,C,D,E) [E>=C+3,E>=A+3,C>=2,A>=2] * Loop 248: case_0(A,B,C,D,E) [E>=4,C>=2,A>=2] * Loop 249: case_0(A,B,C,D,E) [E>=4,C>=2,A>=2] * Loop 250: case_0(A,B,C,D,E) [E>=4,C>=2,A>=2] * Loop 251: case_0(A,B,C,D,E) [E>=4,C>=2,A>=2] * Loop 252: case_0(A,B,C,D,E) [E>=4,C>=2,A>=2] * Loop 253: case_0(A,B,C,D,E) [E>=4,C>=2,A>=2] * Loop 254: case_0(A,B,C,D,E) [E>=4,C>=2,A>=2] * Loop 255: case_0(A,B,C,D,E) [E>=4,C>=2,A>=2] * Loop 256: case_0(A,B,C,D,E) [C+1>=E,E>=A+3,A>=1] * Loop 257: case_0(A,B,C,D,E) [C+1>=E,E>=A+3,A>=1] * Loop 258: case_0(A,B,C,D,E) [C+1>=E,E>=A+3,A>=1] * Loop 259: case_0(A,B,C,D,E) [C+1>=E,E>=A+3,A>=1] * Loop 260: case_0(A,B,C,D,E) [C+1>=E,E>=A+3,A>=1] * Loop 261: case_0(A,B,C,D,E) [C+1>=E,E>=A+3,A>=1] * Loop 262: case_0(A,B,C,D,E) [C+1>=E,E>=A+3,A>=1] * Loop 263: case_0(A,B,C,D,E) [C+1>=E,E>=A+3,A>=1] * Loop 264: case_0(A,B,C,D,E) [E>=C+3,E>=A+3,A>=1] * Loop 265: case_0(A,B,C,D,E) [E>=C+3,E>=A+3,A>=1] * Loop 266: case_0(A,B,C,D,E) [E>=C+3,E>=A+3,A>=1] * Loop 267: case_0(A,B,C,D,E) [E>=C+3,E>=A+3,A>=1] * Loop 268: case_0(A,B,C,D,E) [E>=C+3,E>=A+3,A>=1] * Loop 269: case_0(A,B,C,D,E) [E>=C+3,E>=A+3,A>=1] * Loop 270: case_0(A,B,C,D,E) [E>=C+3,E>=A+3,A>=1] * Loop 271: case_0(A,B,C,D,E) [E>=C+3,E>=A+3,A>=1] * Loop 272: case_0(A,B,C,D,E) [E>=A+2,E>=4,A>=1] * Loop 273: case_0(A,B,C,D,E) [E>=A+2,E>=4,A>=1] * Loop 274: case_0(A,B,C,D,E) [E>=A+2,E>=4,A>=1] * Loop 275: case_0(A,B,C,D,E) [E>=A+2,E>=4,A>=1] * Loop 276: case_0(A,B,C,D,E) [E>=A+2,E>=4,A>=1] * Loop 277: case_0(A,B,C,D,E) [E>=A+2,E>=4,A>=1] * Loop 278: case_0(A,B,C,D,E) [E>=A+2,E>=4,A>=1] * Loop 279: case_0(A,B,C,D,E) [E>=A+2,E>=4,A>=1] * Loop 280: case_0(A,B,C,D,E) [C>=A+1,C>=1,C+1=E] * Loop 281: case_0(A,B,C,D,E) [C>=A+1,C>=1,C+2=E] * Loop 282: case_0(A,B,C,D,E) [C>=A+1,C>=1,C+2=E] * Loop 283: case_0(A,B,C,D,E) [C>=A+1,C>=1,C+2=E] * Loop 284: case_0(A,B,C,D,E) [C>=A+1,C>=1,C+2=E] * Loop 285: case_0(A,B,C,D,E) [C>=A+1,C>=1,C+2=E] * Loop 286: case_0(A,B,C,D,E) [C>=A+1,C>=1,C+2=E] * Loop 287: case_0(A,B,C,D,E) [C>=A+1,C>=1,C+2=E] * Loop 288: case_0(A,B,C,D,E) [C>=A+1,C>=1,C+2=E] * Loop 289: case_0(A,B,C,D,E) [C>=A+1,C>=1,C+2=E] * Loop 290: case_0(A,B,C,D,E) [C>=A+1,C>=1,C+2=E] * Loop 291: case_0(A,B,C,D,E) [C>=A+1,A>=2,C+2=E] * Loop 292: case_0(A,B,C,D,E) [C>=A+1,A>=2,C+2=E] * Loop 293: case_0(A,B,C,D,E) [C>=A+1,A>=2,C+2=E] * Loop 294: case_0(A,B,C,D,E) [C>=A+1,A>=2,C+2=E] * Loop 295: case_0(A,B,C,D,E) [C>=A+1,A>=2,C+2=E] * Loop 296: case_0(A,B,C,D,E) [C>=A+1,A>=2,C+2=E] * Loop 297: case_0(A,B,C,D,E) [C>=A+1,A>=2,C+2=E] * Loop 298: case_0(A,B,C,D,E) [C>=A+1,A>=2,C+2=E] * Loop 299: case_0(A,B,C,D,E) [C>=A+1,A>=1,C+2=E] * Loop 300: case_0(A,B,C,D,E) [C>=A+1,A>=1,C+2=E] * Loop 301: case_0(A,B,C,D,E) [C>=A+1,A>=1,C+2=E] * Loop 302: case_0(A,B,C,D,E) [C>=A+1,A>=1,C+2=E] * Loop 303: case_0(A,B,C,D,E) [C>=A+1,A>=1,C+2=E] * Loop 304: case_0(A,B,C,D,E) [C>=A+1,A>=1,C+2=E] * Loop 305: case_0(A,B,C,D,E) [C>=A+1,A>=1,C+2=E] * Loop 306: case_0(A,B,C,D,E) [C>=A+1,A>=1,C+2=E] * Loop 307: case_0(A,B,C,D,E) [A>=1,A+1=E] * Loop 308: case_0(A,B,C,D,E) [A>=C+1,C>=1,A+2=E] * Loop 309: case_0(A,B,C,D,E) [A>=C+1,C>=1,A+2=E] * Loop 310: case_0(A,B,C,D,E) [A>=C+1,C>=1,A+2=E] * Loop 311: case_0(A,B,C,D,E) [A>=C+1,C>=1,A+2=E] * Loop 312: case_0(A,B,C,D,E) [A>=C+1,C>=1,A+2=E] * Loop 313: case_0(A,B,C,D,E) [A>=C+1,C>=1,A+2=E] * Loop 314: case_0(A,B,C,D,E) [A>=C+1,C>=1,A+2=E] * Loop 315: case_0(A,B,C,D,E) [A>=C+1,C>=1,A+2=E] * Loop 316: case_0(A,B,C,D,E) [A>=C+2,A>=2,A+2=E] * Loop 317: case_0(A,B,C,D,E) [A>=C+2,A>=2,A+2=E] * Loop 318: case_0(A,B,C,D,E) [A>=C+2,A>=2,A+2=E] * Loop 319: case_0(A,B,C,D,E) [A>=C+2,A>=2,A+2=E] * Loop 320: case_0(A,B,C,D,E) [A>=C+2,A>=2,A+2=E] * Loop 321: case_0(A,B,C,D,E) [A>=C+2,A>=2,A+2=E] * Loop 322: case_0(A,B,C,D,E) [A>=C+2,A>=2,A+2=E] * Loop 323: case_0(A,B,C,D,E) [A>=C+2,A>=2,A+2=E] * Loop 324: case_0(A,B,C,D,E) [C>=2,A>=2,A+2=E] * Loop 325: case_0(A,B,C,D,E) [C>=2,A>=2,A+2=E] * Loop 326: case_0(A,B,C,D,E) [C>=2,A>=2,A+2=E] * Loop 327: case_0(A,B,C,D,E) [C>=2,A>=2,A+2=E] * Loop 328: case_0(A,B,C,D,E) [C>=2,A>=2,A+2=E] * Loop 329: case_0(A,B,C,D,E) [C>=2,A>=2,A+2=E] * Loop 330: case_0(A,B,C,D,E) [C>=2,A>=2,A+2=E] * Loop 331: case_0(A,B,C,D,E) [C>=2,A>=2,A+2=E] * Loop 332: case_0(A,B,C,D,E) [A>=2,A+2=E] * Loop 333: case_0(A,B,C,D,E) [A>=2,A+2=E] * Loop 334: case_0(A,B,C,D,E) [A>=2,A+2=E] * Loop 335: case_0(A,B,C,D,E) [A>=2,A+2=E] * Loop 336: case_0(A,B,C,D,E) [A>=2,A+2=E] * Loop 337: case_0(A,B,C,D,E) [A>=2,A+2=E] * Loop 338: case_0(A,B,C,D,E) [A>=2,A+2=E] * Loop 339: case_0(A,B,C,D,E) [A>=2,A+2=E] * Loop 340: case_0(A,B,C,D,E) [A>=1,A+2=E] * Loop 341: case_0(A,B,C,D,E) [A>=1,A+2=E] * Loop 342: case_0(A,B,C,D,E) [A>=1,A+2=E] * Loop 343: case_0(A,B,C,D,E) [A>=1,A+2=E] * Loop 344: case_0(A,B,C,D,E) [A>=1,A+2=E] * Loop 345: case_0(A,B,C,D,E) [A>=1,A+2=E] * Loop 346: case_0(A,B,C,D,E) [A>=1,A+2=E] * Loop 347: case_0(A,B,C,D,E) [A>=1,A+2=E] * Loop 348: case_0(A,B,C,D,E) [A>=1,A+2=E] * Loop 349: case_0(A,B,C,D,E) [A>=1,A+2=E] * Loop 350: case_0(A,B,C,D,E) [A+1>=E,E>=4,E=C+2] * Loop 351: case_0(A,B,C,D,E) [A+1>=E,E>=4,E=C+2] * Loop 352: case_0(A,B,C,D,E) [A+1>=E,E>=4,E=C+2] * Loop 353: case_0(A,B,C,D,E) [A+1>=E,E>=4,E=C+2] * Loop 354: case_0(A,B,C,D,E) [A+1>=E,E>=4,E=C+2] * Loop 355: case_0(A,B,C,D,E) [A+1>=E,E>=4,E=C+2] * Loop 356: case_0(A,B,C,D,E) [A+1>=E,E>=4,E=C+2] * Loop 357: case_0(A,B,C,D,E) [A+1>=E,E>=4,E=C+2] * Loop 358: case_0(A,B,C,D,E) [A+1>=E,E>=4,E=C+2] * Loop 359: case_0(A,B,C,D,E) [A+1>=E,E>=4,E=C+2] * Loop 360: case_0(A,B,C,D,E) [A+1>=E,E>=4,E=C+2] * Loop 361: case_0(A,B,C,D,E) [A+1>=E,E>=4,E=C+2] * Loop 362: case_0(A,B,C,D,E) [A+1>=E,E>=4,E=C+2] * Loop 363: case_0(A,B,C,D,E) [A+1>=E,E>=4,E=C+2] * Loop 364: case_0(A,B,C,D,E) [A+1>=E,E>=4,E=C+2] * Loop 365: case_0(A,B,C,D,E) [A+1>=E,E>=4,E=C+2] * Loop 366: case_0(A,B,C,D,E) [E>=A+4,E>=4,E=C+2] * Loop 367: case_0(A,B,C,D,E) [E>=A+4,E>=4,E=C+2] * Loop 368: case_0(A,B,C,D,E) [E>=A+4,E>=4,E=C+2] * Loop 369: case_0(A,B,C,D,E) [E>=A+4,E>=4,E=C+2] * Loop 370: case_0(A,B,C,D,E) [E>=A+4,E>=4,E=C+2] * Loop 371: case_0(A,B,C,D,E) [E>=A+4,E>=4,E=C+2] * Loop 372: case_0(A,B,C,D,E) [E>=A+4,E>=4,E=C+2] * Loop 373: case_0(A,B,C,D,E) [E>=A+4,E>=4,E=C+2] * Loop 374: case_0(A,B,C,D,E) [E>=A+3,E>=4,E=C+2] * Loop 375: case_0(A,B,C,D,E) [E>=A+3,E>=4,E=C+2] * Loop 376: case_0(A,B,C,D,E) [E>=A+3,E>=4,E=C+2] * Loop 377: case_0(A,B,C,D,E) [E>=A+3,E>=4,E=C+2] * Loop 378: case_0(A,B,C,D,E) [E>=A+3,E>=4,E=C+2] * Loop 379: case_0(A,B,C,D,E) [E>=A+3,E>=4,E=C+2] * Loop 380: case_0(A,B,C,D,E) [E>=A+3,E>=4,E=C+2] * Loop 381: case_0(A,B,C,D,E) [E>=A+3,E>=4,E=C+2] * Loop 382: case_0(A,B,C,D,E) [A+1>=E,E>=3,E=C+2] * Loop 383: case_0(A,B,C,D,E) [A+1>=E,E>=3,E=C+2] * Loop 384: case_0(A,B,C,D,E) [A+1>=E,E>=3,E=C+2] * Loop 385: case_0(A,B,C,D,E) [A+1>=E,E>=3,E=C+2] * Loop 386: case_0(A,B,C,D,E) [A+1>=E,E>=3,E=C+2] * Loop 387: case_0(A,B,C,D,E) [A+1>=E,E>=3,E=C+2] * Loop 388: case_0(A,B,C,D,E) [A+1>=E,E>=3,E=C+2] * Loop 389: case_0(A,B,C,D,E) [A+1>=E,E>=3,E=C+2] * Loop 390: case_0(A,B,C,D,E) [A+1>=E,E>=3,E=C+2] * Loop 391: case_0(A,B,C,D,E) [A+1>=E,E>=3,E=C+2] * Loop 392: case_0(A,B,C,D,E) [A>=E,E>=2,E=C+1] ### Ranking functions of CR case_0(A,B,C,D,E) #### Partial ranking functions of CR case_0(A,B,C,D,E) ### Resulting Chains:case_0(A,B,C,D,E) * [392] * [391] * [390] * [389] * [388] * [387] * [386] * [385] * [384] * [383] * [382] * [381] * [380] * [379] * [378] * [377] * [376] * [375] * [374] * [373] * [372] * [371] * [370] * [369] * [368] * [367] * [366] * [365] * [364] * [363] * [362] * [361] * [360] * [359] * [358] * [357] * [356] * [355] * [354] * [353] * [352] * [351] * [350] * [349] * [348] * [347] * [346] * [345] * [344] * [343] * [342] * [341] * [340] * [339] * [338] * [337] * [336] * [335] * [334] * [333] * [332] * [331] * [330] * [329] * [328] * [327] * [326] * [325] * [324] * [323] * [322] * [321] * [320] * [319] * [318] * [317] * [316] * [315] * [314] * [313] * [312] * [311] * [310] * [309] * [308] * [307] * [306] * [305] * [304] * [303] * [302] * [301] * [300] * [299] * [298] * [297] * [296] * [295] * [294] * [293] * [292] * [291] * [290] * [289] * [288] * [287] * [286] * [285] * [284] * [283] * [282] * [281] * [280] * [279] * [278] * [277] * [276] * [275] * [274] * [273] * [272] * [271] * [270] * [269] * [268] * [267] * [266] * [265] * [264] * [263] * [262] * [261] * [260] * [259] * [258] * [257] * [256] * [255] * [254] * [253] * [252] * [251] * [250] * [249] * [248] * [247] * [246] * [245] * [244] * [243] * [242] * [241] * [240] * [239] * [238] * [237] * [236] * [235] * [234] * [233] * [232] * [231] * [230] * [229] * [228] * [227] * [226] * [225] * [224] * [223] * [222] * [221] * [220] * [219] * [218] * [217] * [216] * [215] * [214] * [213] * [212] * [211] * [210] * [209] * [208] * [207] * [206] * [205] * [204] * [203] * [202] * [201] * [200] * [199] * [198] * [197] * [196] * [195] * [194] * [193] * [192] * [191] * [190] * [189] * [188] * [187] * [186] * [185] * [184] * [183] * [182] * [181] * [180] * [179] * [178] * [177] * [176] * [175] * [174] * [173] * [172] * [171] * [170] * [169] * [168] * [167] * [166] * [165] * [164] * [163] * [162] * [161] * [160] * [159] * [158] * [157] * [156] * [155] * [154] * [153] * [152] * [151] * [150] * [149] * [148] * [147] * [146] * [145] * [144] * [143] * [142] * [141] * [140] * [139] * [138] * [137] * [136] * [135] * [134] * [133] * [132] * [131] * [130] * [129] * [128] * [127] * [126] * [125] * [124] * [123] * [122] * [121] * [120] * [119] * [118] * [117] * [116] * [115] * [114] * [113] * [112] * [111] * [110] * [109] * [108] * [107] * [106] * [105] * [104] * [103] * [102] * [101] * [100] * [99] * [98] * [97] * [96] * [95] * [94] * [93] * [92] * [91] * [90] * [89] * [88] * [87] * [86] * [85] * [84] * [83] * [82] * [81] * [80] * [79] * [78] * [77] * [76] * [75] * [74] * [73] * [72] * [71] * [70] * [69] * [68] * [67] * [66] * [65] * [64] * [63] * [62] * [61] * [60] * [59] * [58] Computing Bounds ===================================== #### Cost of chains of and_op(A,B): * Chain [26]: 0 with precondition: [A=0] * Chain [25]: 0 with precondition: [A=1] #### Cost of chains of case_2(A,B,C,D,E,F): * Chain [29]: 1 with precondition: [E=C+1,E=F+1,E>=2] * Chain [28]: 2 with precondition: [E=F+1,E>=2,E>=C+2] * Chain [27]: 2 with precondition: [E=F+1,E>=2,C>=E] #### Cost of chains of case_1(A,B,C,D,E,F): * Chain [36]: 1 with precondition: [E=A+1,E=F+1,E>=2] * Chain [35]: 3 with precondition: [E=C+1,E=F+1,E>=2,E>=A+2] * Chain [34]: 3 with precondition: [E=C+1,E=F+1,E>=2,A>=E] * Chain [33]: 4 with precondition: [F+1=E,F>=1,F>=A+1,F>=C+1] * Chain [32]: 4 with precondition: [F+1=E,F>=1,F>=A+1,C>=F+1] * Chain [31]: 4 with precondition: [F+1=E,F>=1,F>=C+1,A>=F+1] * Chain [30]: 4 with precondition: [F+1=E,F>=1,A>=F+1,C>=F+1] #### Cost of chains of neg(A): * Chain [38]: 0 with precondition: [A=0] * Chain [37]: 0 with precondition: [A=1] #### Cost of chains of or(A,B): * Chain [40]: 0 with precondition: [A=0] * Chain [39]: 0 with precondition: [A=1] #### Cost of loops [41,42,43,44,45,46,47,48,49,50] * loop 41:eval2(A,B,C,D,E) -> [eval2(A',B',C',D',E'),eval2(A'2,B'2,C'2,D'2,E'2)] 8 * loop 42:eval2(A,B,C,D,E) -> [eval2(A',B',C',D',E'),eval2(A'2,B'2,C'2,D'2,E'2)] 8 * loop 43:eval2(A,B,C,D,E) -> [eval2(A',B',C',D',E'),eval2(A'2,B'2,C'2,D'2,E'2)] 7 * loop 44:eval2(A,B,C,D,E) -> [eval2(A',B',C',D',E'),eval2(A'2,B'2,C'2,D'2,E'2)] 7 * loop 45:eval2(A,B,C,D,E) -> [eval2(A',B',C',D',E'),eval2(A'2,B'2,C'2,D'2,E'2)] 8 * loop 46:eval2(A,B,C,D,E) -> [eval2(A',B',C',D',E'),eval2(A'2,B'2,C'2,D'2,E'2)] 8 * loop 47:eval2(A,B,C,D,E) -> [eval2(A',B',C',D',E'),eval2(A'2,B'2,C'2,D'2,E'2)] 7 * loop 48:eval2(A,B,C,D,E) -> [eval2(A',B',C',D',E'),eval2(A'2,B'2,C'2,D'2,E'2)] 7 * loop 49:eval2(A,B,C,D,E) -> [eval2(A',B',C',D',E')] 6 * loop 50:eval2(A,B,C,D,E) -> [eval2(A',B',C',D',E')] 6 #### Cost of phase [41,42,43,44,45,46,47,48,49,50]:eval2(A,B,C,D,E) -> [] 60*it(41)+6*it(49)+6*it(50)+7*it([51])+7*it([52])+7*it([53])+7*it([54])+6*it([55])+4*it([56])+6*it([57])+0 #### Cost of chains of eval2(A,B,C,D,E): * Chain [57]: 6 with precondition: [E=C+1,E>=2,A>=E] * Chain [56]: 4 with precondition: [E=A+1,E>=2] * Chain [55]: 6 with precondition: [E=C+1,E>=2,E>=A+2] * Chain [54]: 7 with precondition: [E>=2,E>=A+2,E>=C+2] * Chain [53]: 7 with precondition: [E>=2,E>=A+2,C>=E] * Chain [52]: 7 with precondition: [E>=2,E>=C+2,A>=E] * Chain [51]: 7 with precondition: [E>=2,A>=E,C>=E] * Chain [multiple([41,42,43,44,45,46,47,48,49,50],[[57],[56],[55],[54],[53],[52],[51]])]: 60*it(41)+6*it(49)+6*it(50)+7*it([51])+7*it([52])+7*it([53])+7*it([54])+6*it([55])+4*it([56])+6*it([57])+0 with precondition: [E>=3] #### Cost of chains of case_0(A,B,C,D,E): * Chain [392]: 5 with precondition: [E=C+1,E>=2,A>=E] * Chain [391]: 11 with precondition: [E=C+2,E>=3,A+1>=E] * Chain [390]: 11 with precondition: [E=C+2,E>=3,A+1>=E] * Chain [389]: 18 with precondition: [E=C+2,E>=3,A+1>=E] * Chain [388]: 18 with precondition: [E=C+2,E>=3,A+1>=E] * Chain [387]: 18 with precondition: [E=C+2,E>=3,A+1>=E] * Chain [386]: 18 with precondition: [E=C+2,E>=3,A+1>=E] * Chain [385]: 19 with precondition: [E=C+2,E>=3,A+1>=E] * Chain [384]: 19 with precondition: [E=C+2,E>=3,A+1>=E] * Chain [383]: 19 with precondition: [E=C+2,E>=3,A+1>=E] * Chain [382]: 19 with precondition: [E=C+2,E>=3,A+1>=E] * Chain [381]: 116*s(1)+12 with precondition: [E=C+2,E>=4,E>=A+3] * Chain [380]: 116*s(11)+12 with precondition: [E=C+2,E>=4,E>=A+3] * Chain [379]: 116*s(21)+12 with precondition: [E=C+2,E>=4,E>=A+3] * Chain [378]: 116*s(31)+12 with precondition: [E=C+2,E>=4,E>=A+3] * Chain [377]: 116*s(41)+13 with precondition: [E=C+2,E>=4,E>=A+3] * Chain [376]: 116*s(51)+13 with precondition: [E=C+2,E>=4,E>=A+3] * Chain [375]: 116*s(61)+13 with precondition: [E=C+2,E>=4,E>=A+3] * Chain [374]: 116*s(71)+13 with precondition: [E=C+2,E>=4,E>=A+3] * Chain [373]: 19 with precondition: [E=C+2,E>=4,E>=A+4] * Chain [372]: 19 with precondition: [E=C+2,E>=4,E>=A+4] * Chain [371]: 19 with precondition: [E=C+2,E>=4,E>=A+4] * Chain [370]: 19 with precondition: [E=C+2,E>=4,E>=A+4] * Chain [369]: 20 with precondition: [E=C+2,E>=4,E>=A+4] * Chain [368]: 20 with precondition: [E=C+2,E>=4,E>=A+4] * Chain [367]: 20 with precondition: [E=C+2,E>=4,E>=A+4] * Chain [366]: 20 with precondition: [E=C+2,E>=4,E>=A+4] * Chain [365]: 19 with precondition: [E=C+2,E>=4,A+1>=E] * Chain [364]: 19 with precondition: [E=C+2,E>=4,A+1>=E] * Chain [363]: 116*s(81)+12 with precondition: [E=C+2,E>=4,A+1>=E] * Chain [362]: 116*s(91)+12 with precondition: [E=C+2,E>=4,A+1>=E] * Chain [361]: 19 with precondition: [E=C+2,E>=4,A+1>=E] * Chain [360]: 19 with precondition: [E=C+2,E>=4,A+1>=E] * Chain [359]: 116*s(101)+12 with precondition: [E=C+2,E>=4,A+1>=E] * Chain [358]: 116*s(111)+12 with precondition: [E=C+2,E>=4,A+1>=E] * Chain [357]: 20 with precondition: [E=C+2,E>=4,A+1>=E] * Chain [356]: 20 with precondition: [E=C+2,E>=4,A+1>=E] * Chain [355]: 116*s(121)+13 with precondition: [E=C+2,E>=4,A+1>=E] * Chain [354]: 116*s(131)+13 with precondition: [E=C+2,E>=4,A+1>=E] * Chain [353]: 20 with precondition: [E=C+2,E>=4,A+1>=E] * Chain [352]: 20 with precondition: [E=C+2,E>=4,A+1>=E] * Chain [351]: 116*s(141)+13 with precondition: [E=C+2,E>=4,A+1>=E] * Chain [350]: 116*s(151)+13 with precondition: [E=C+2,E>=4,A+1>=E] * Chain [349]: 9 with precondition: [A+2=E,A>=1] * Chain [348]: 9 with precondition: [A+2=E,A>=1] * Chain [347]: 14 with precondition: [A+2=E,A>=1] * Chain [346]: 14 with precondition: [A+2=E,A>=1] * Chain [345]: 14 with precondition: [A+2=E,A>=1] * Chain [344]: 14 with precondition: [A+2=E,A>=1] * Chain [343]: 15 with precondition: [A+2=E,A>=1] * Chain [342]: 15 with precondition: [A+2=E,A>=1] * Chain [341]: 15 with precondition: [A+2=E,A>=1] * Chain [340]: 15 with precondition: [A+2=E,A>=1] * Chain [339]: 116*s(161)+10 with precondition: [A+2=E,A>=2] * Chain [338]: 116*s(171)+10 with precondition: [A+2=E,A>=2] * Chain [337]: 116*s(181)+10 with precondition: [A+2=E,A>=2] * Chain [336]: 116*s(191)+10 with precondition: [A+2=E,A>=2] * Chain [335]: 116*s(201)+11 with precondition: [A+2=E,A>=2] * Chain [334]: 116*s(211)+11 with precondition: [A+2=E,A>=2] * Chain [333]: 116*s(221)+11 with precondition: [A+2=E,A>=2] * Chain [332]: 116*s(231)+11 with precondition: [A+2=E,A>=2] * Chain [331]: 17 with precondition: [A+2=E,A>=2,C>=2] * Chain [330]: 17 with precondition: [A+2=E,A>=2,C>=2] * Chain [329]: 17 with precondition: [A+2=E,A>=2,C>=2] * Chain [328]: 17 with precondition: [A+2=E,A>=2,C>=2] * Chain [327]: 18 with precondition: [A+2=E,A>=2,C>=2] * Chain [326]: 18 with precondition: [A+2=E,A>=2,C>=2] * Chain [325]: 18 with precondition: [A+2=E,A>=2,C>=2] * Chain [324]: 18 with precondition: [A+2=E,A>=2,C>=2] * Chain [323]: 17 with precondition: [A+2=E,A>=2,A>=C+2] * Chain [322]: 17 with precondition: [A+2=E,A>=2,A>=C+2] * Chain [321]: 17 with precondition: [A+2=E,A>=2,A>=C+2] * Chain [320]: 17 with precondition: [A+2=E,A>=2,A>=C+2] * Chain [319]: 18 with precondition: [A+2=E,A>=2,A>=C+2] * Chain [318]: 18 with precondition: [A+2=E,A>=2,A>=C+2] * Chain [317]: 18 with precondition: [A+2=E,A>=2,A>=C+2] * Chain [316]: 18 with precondition: [A+2=E,A>=2,A>=C+2] * Chain [315]: 16 with precondition: [A+2=E,C>=1,A>=C+1] * Chain [314]: 16 with precondition: [A+2=E,C>=1,A>=C+1] * Chain [313]: 16 with precondition: [A+2=E,C>=1,A>=C+1] * Chain [312]: 16 with precondition: [A+2=E,C>=1,A>=C+1] * Chain [311]: 17 with precondition: [A+2=E,C>=1,A>=C+1] * Chain [310]: 17 with precondition: [A+2=E,C>=1,A>=C+1] * Chain [309]: 17 with precondition: [A+2=E,C>=1,A>=C+1] * Chain [308]: 17 with precondition: [A+2=E,C>=1,A>=C+1] * Chain [307]: 3 with precondition: [A+1=E,A>=1] * Chain [306]: 16 with precondition: [C+2=E,A>=1,C>=A+1] * Chain [305]: 16 with precondition: [C+2=E,A>=1,C>=A+1] * Chain [304]: 16 with precondition: [C+2=E,A>=1,C>=A+1] * Chain [303]: 16 with precondition: [C+2=E,A>=1,C>=A+1] * Chain [302]: 17 with precondition: [C+2=E,A>=1,C>=A+1] * Chain [301]: 17 with precondition: [C+2=E,A>=1,C>=A+1] * Chain [300]: 17 with precondition: [C+2=E,A>=1,C>=A+1] * Chain [299]: 17 with precondition: [C+2=E,A>=1,C>=A+1] * Chain [298]: 19 with precondition: [C+2=E,A>=2,C>=A+1] * Chain [297]: 19 with precondition: [C+2=E,A>=2,C>=A+1] * Chain [296]: 19 with precondition: [C+2=E,A>=2,C>=A+1] * Chain [295]: 19 with precondition: [C+2=E,A>=2,C>=A+1] * Chain [294]: 20 with precondition: [C+2=E,A>=2,C>=A+1] * Chain [293]: 20 with precondition: [C+2=E,A>=2,C>=A+1] * Chain [292]: 20 with precondition: [C+2=E,A>=2,C>=A+1] * Chain [291]: 20 with precondition: [C+2=E,A>=2,C>=A+1] * Chain [290]: 11 with precondition: [C+2=E,C>=1,C>=A+1] * Chain [289]: 11 with precondition: [C+2=E,C>=1,C>=A+1] * Chain [288]: 18 with precondition: [C+2=E,C>=1,C>=A+1] * Chain [287]: 18 with precondition: [C+2=E,C>=1,C>=A+1] * Chain [286]: 18 with precondition: [C+2=E,C>=1,C>=A+1] * Chain [285]: 18 with precondition: [C+2=E,C>=1,C>=A+1] * Chain [284]: 19 with precondition: [C+2=E,C>=1,C>=A+1] * Chain [283]: 19 with precondition: [C+2=E,C>=1,C>=A+1] * Chain [282]: 19 with precondition: [C+2=E,C>=1,C>=A+1] * Chain [281]: 19 with precondition: [C+2=E,C>=1,C>=A+1] * Chain [280]: 5 with precondition: [C+1=E,C>=1,C>=A+1] * Chain [279]: 116*s(241)+10 with precondition: [A>=1,E>=4,E>=A+2] * Chain [278]: 116*s(251)+10 with precondition: [A>=1,E>=4,E>=A+2] * Chain [277]: 116*s(261)+10 with precondition: [A>=1,E>=4,E>=A+2] * Chain [276]: 116*s(271)+10 with precondition: [A>=1,E>=4,E>=A+2] * Chain [275]: 116*s(281)+11 with precondition: [A>=1,E>=4,E>=A+2] * Chain [274]: 116*s(291)+11 with precondition: [A>=1,E>=4,E>=A+2] * Chain [273]: 116*s(301)+11 with precondition: [A>=1,E>=4,E>=A+2] * Chain [272]: 116*s(311)+11 with precondition: [A>=1,E>=4,E>=A+2] * Chain [271]: 17 with precondition: [A>=1,E>=A+3,E>=C+3] * Chain [270]: 17 with precondition: [A>=1,E>=A+3,E>=C+3] * Chain [269]: 17 with precondition: [A>=1,E>=A+3,E>=C+3] * Chain [268]: 17 with precondition: [A>=1,E>=A+3,E>=C+3] * Chain [267]: 18 with precondition: [A>=1,E>=A+3,E>=C+3] * Chain [266]: 18 with precondition: [A>=1,E>=A+3,E>=C+3] * Chain [265]: 18 with precondition: [A>=1,E>=A+3,E>=C+3] * Chain [264]: 18 with precondition: [A>=1,E>=A+3,E>=C+3] * Chain [263]: 17 with precondition: [A>=1,E>=A+3,C+1>=E] * Chain [262]: 17 with precondition: [A>=1,E>=A+3,C+1>=E] * Chain [261]: 17 with precondition: [A>=1,E>=A+3,C+1>=E] * Chain [260]: 17 with precondition: [A>=1,E>=A+3,C+1>=E] * Chain [259]: 18 with precondition: [A>=1,E>=A+3,C+1>=E] * Chain [258]: 18 with precondition: [A>=1,E>=A+3,C+1>=E] * Chain [257]: 18 with precondition: [A>=1,E>=A+3,C+1>=E] * Chain [256]: 18 with precondition: [A>=1,E>=A+3,C+1>=E] * Chain [255]: 116*s(321)+13 with precondition: [A>=2,C>=2,E>=4] * Chain [254]: 116*s(331)+13 with precondition: [A>=2,C>=2,E>=4] * Chain [253]: 116*s(341)+13 with precondition: [A>=2,C>=2,E>=4] * Chain [252]: 116*s(351)+13 with precondition: [A>=2,C>=2,E>=4] * Chain [251]: 116*s(361)+14 with precondition: [A>=2,C>=2,E>=4] * Chain [250]: 116*s(371)+14 with precondition: [A>=2,C>=2,E>=4] * Chain [249]: 116*s(381)+14 with precondition: [A>=2,C>=2,E>=4] * Chain [248]: 116*s(391)+14 with precondition: [A>=2,C>=2,E>=4] * Chain [247]: 20 with precondition: [A>=2,C>=2,E>=A+3,E>=C+3] * Chain [246]: 20 with precondition: [A>=2,C>=2,E>=A+3,E>=C+3] * Chain [245]: 20 with precondition: [A>=2,C>=2,E>=A+3,E>=C+3] * Chain [244]: 20 with precondition: [A>=2,C>=2,E>=A+3,E>=C+3] * Chain [243]: 21 with precondition: [A>=2,C>=2,E>=A+3,E>=C+3] * Chain [242]: 21 with precondition: [A>=2,C>=2,E>=A+3,E>=C+3] * Chain [241]: 21 with precondition: [A>=2,C>=2,E>=A+3,E>=C+3] * Chain [240]: 21 with precondition: [A>=2,C>=2,E>=A+3,E>=C+3] * Chain [239]: 116*s(401)+13 with precondition: [A>=2,E>=4,A>=C+2,E>=C+3] * Chain [238]: 116*s(411)+13 with precondition: [A>=2,E>=4,A>=C+2,E>=C+3] * Chain [237]: 116*s(421)+13 with precondition: [A>=2,E>=4,A>=C+2,E>=C+3] * Chain [236]: 116*s(431)+13 with precondition: [A>=2,E>=4,A>=C+2,E>=C+3] * Chain [235]: 116*s(441)+14 with precondition: [A>=2,E>=4,A>=C+2,E>=C+3] * Chain [234]: 116*s(451)+14 with precondition: [A>=2,E>=4,A>=C+2,E>=C+3] * Chain [233]: 116*s(461)+14 with precondition: [A>=2,E>=4,A>=C+2,E>=C+3] * Chain [232]: 116*s(471)+14 with precondition: [A>=2,E>=4,A>=C+2,E>=C+3] * Chain [231]: 20 with precondition: [A>=2,E>=A+3,A>=C+2] * Chain [230]: 20 with precondition: [A>=2,E>=A+3,A>=C+2] * Chain [229]: 20 with precondition: [A>=2,E>=A+3,A>=C+2] * Chain [228]: 20 with precondition: [A>=2,E>=A+3,A>=C+2] * Chain [227]: 21 with precondition: [A>=2,E>=A+3,A>=C+2] * Chain [226]: 21 with precondition: [A>=2,E>=A+3,A>=C+2] * Chain [225]: 21 with precondition: [A>=2,E>=A+3,A>=C+2] * Chain [224]: 21 with precondition: [A>=2,E>=A+3,A>=C+2] * Chain [223]: 20 with precondition: [A>=2,E>=A+3,C+1>=E] * Chain [222]: 20 with precondition: [A>=2,E>=A+3,C+1>=E] * Chain [221]: 20 with precondition: [A>=2,E>=A+3,C+1>=E] * Chain [220]: 20 with precondition: [A>=2,E>=A+3,C+1>=E] * Chain [219]: 21 with precondition: [A>=2,E>=A+3,C+1>=E] * Chain [218]: 21 with precondition: [A>=2,E>=A+3,C+1>=E] * Chain [217]: 21 with precondition: [A>=2,E>=A+3,C+1>=E] * Chain [216]: 21 with precondition: [A>=2,E>=A+3,C+1>=E] * Chain [215]: 116*s(481)+12 with precondition: [C>=1,E>=4,C>=A+1,E>=C+2] * Chain [214]: 116*s(491)+12 with precondition: [C>=1,E>=4,C>=A+1,E>=C+2] * Chain [213]: 116*s(501)+12 with precondition: [C>=1,E>=4,C>=A+1,E>=C+2] * Chain [212]: 116*s(511)+12 with precondition: [C>=1,E>=4,C>=A+1,E>=C+2] * Chain [211]: 116*s(521)+13 with precondition: [C>=1,E>=4,C>=A+1,E>=C+2] * Chain [210]: 116*s(531)+13 with precondition: [C>=1,E>=4,C>=A+1,E>=C+2] * Chain [209]: 116*s(541)+13 with precondition: [C>=1,E>=4,C>=A+1,E>=C+2] * Chain [208]: 116*s(551)+13 with precondition: [C>=1,E>=4,C>=A+1,E>=C+2] * Chain [207]: 116*s(561)+12 with precondition: [C>=1,E>=4,A>=C+1,E>=C+2] * Chain [206]: 116*s(571)+12 with precondition: [C>=1,E>=4,A>=C+1,E>=C+2] * Chain [205]: 116*s(581)+12 with precondition: [C>=1,E>=4,A>=C+1,E>=C+2] * Chain [204]: 116*s(591)+12 with precondition: [C>=1,E>=4,A>=C+1,E>=C+2] * Chain [203]: 116*s(601)+13 with precondition: [C>=1,E>=4,A>=C+1,E>=C+2] * Chain [202]: 116*s(611)+13 with precondition: [C>=1,E>=4,A>=C+1,E>=C+2] * Chain [201]: 116*s(621)+13 with precondition: [C>=1,E>=4,A>=C+1,E>=C+2] * Chain [200]: 116*s(631)+13 with precondition: [C>=1,E>=4,A>=C+1,E>=C+2] * Chain [199]: 19 with precondition: [C>=1,C>=A+1,E>=C+3] * Chain [198]: 19 with precondition: [C>=1,C>=A+1,E>=C+3] * Chain [197]: 19 with precondition: [C>=1,C>=A+1,E>=C+3] * Chain [196]: 19 with precondition: [C>=1,C>=A+1,E>=C+3] * Chain [195]: 20 with precondition: [C>=1,C>=A+1,E>=C+3] * Chain [194]: 20 with precondition: [C>=1,C>=A+1,E>=C+3] * Chain [193]: 20 with precondition: [C>=1,C>=A+1,E>=C+3] * Chain [192]: 20 with precondition: [C>=1,C>=A+1,E>=C+3] * Chain [191]: 19 with precondition: [C>=1,E>=A+3,A>=C+1] * Chain [190]: 19 with precondition: [C>=1,E>=A+3,A>=C+1] * Chain [189]: 19 with precondition: [C>=1,E>=A+3,A>=C+1] * Chain [188]: 19 with precondition: [C>=1,E>=A+3,A>=C+1] * Chain [187]: 20 with precondition: [C>=1,E>=A+3,A>=C+1] * Chain [186]: 20 with precondition: [C>=1,E>=A+3,A>=C+1] * Chain [185]: 20 with precondition: [C>=1,E>=A+3,A>=C+1] * Chain [184]: 20 with precondition: [C>=1,E>=A+3,A>=C+1] * Chain [183]: 19 with precondition: [C>=1,E>=C+3,A+1>=E] * Chain [182]: 19 with precondition: [C>=1,E>=C+3,A+1>=E] * Chain [181]: 19 with precondition: [C>=1,E>=C+3,A+1>=E] * Chain [180]: 19 with precondition: [C>=1,E>=C+3,A+1>=E] * Chain [179]: 20 with precondition: [C>=1,E>=C+3,A+1>=E] * Chain [178]: 20 with precondition: [C>=1,E>=C+3,A+1>=E] * Chain [177]: 20 with precondition: [C>=1,E>=C+3,A+1>=E] * Chain [176]: 20 with precondition: [C>=1,E>=C+3,A+1>=E] * Chain [175]: 116*s(641)+13 with precondition: [C>=2,E>=4,C>=A+2,E>=A+3] * Chain [174]: 116*s(651)+13 with precondition: [C>=2,E>=4,C>=A+2,E>=A+3] * Chain [173]: 116*s(661)+13 with precondition: [C>=2,E>=4,C>=A+2,E>=A+3] * Chain [172]: 116*s(671)+13 with precondition: [C>=2,E>=4,C>=A+2,E>=A+3] * Chain [171]: 116*s(681)+14 with precondition: [C>=2,E>=4,C>=A+2,E>=A+3] * Chain [170]: 116*s(691)+14 with precondition: [C>=2,E>=4,C>=A+2,E>=A+3] * Chain [169]: 116*s(701)+14 with precondition: [C>=2,E>=4,C>=A+2,E>=A+3] * Chain [168]: 116*s(711)+14 with precondition: [C>=2,E>=4,C>=A+2,E>=A+3] * Chain [167]: 20 with precondition: [C>=2,C>=A+2,E>=C+3] * Chain [166]: 20 with precondition: [C>=2,C>=A+2,E>=C+3] * Chain [165]: 20 with precondition: [C>=2,C>=A+2,E>=C+3] * Chain [164]: 20 with precondition: [C>=2,C>=A+2,E>=C+3] * Chain [163]: 21 with precondition: [C>=2,C>=A+2,E>=C+3] * Chain [162]: 21 with precondition: [C>=2,C>=A+2,E>=C+3] * Chain [161]: 21 with precondition: [C>=2,C>=A+2,E>=C+3] * Chain [160]: 21 with precondition: [C>=2,C>=A+2,E>=C+3] * Chain [159]: 20 with precondition: [C>=2,E>=C+3,A+1>=E] * Chain [158]: 20 with precondition: [C>=2,E>=C+3,A+1>=E] * Chain [157]: 20 with precondition: [C>=2,E>=C+3,A+1>=E] * Chain [156]: 20 with precondition: [C>=2,E>=C+3,A+1>=E] * Chain [155]: 21 with precondition: [C>=2,E>=C+3,A+1>=E] * Chain [154]: 21 with precondition: [C>=2,E>=C+3,A+1>=E] * Chain [153]: 21 with precondition: [C>=2,E>=C+3,A+1>=E] * Chain [152]: 21 with precondition: [C>=2,E>=C+3,A+1>=E] * Chain [151]: 6 with precondition: [E>=2,E>=A+2,E>=C+2] * Chain [150]: 6 with precondition: [E>=2,E>=A+2,C>=E] * Chain [149]: 6 with precondition: [E>=2,E>=C+2,A>=E] * Chain [148]: 6 with precondition: [E>=2,A>=E,C>=E] * Chain [147]: 12 with precondition: [E>=3,E>=A+3,E>=C+3] * Chain [146]: 12 with precondition: [E>=3,E>=A+3,E>=C+3] * Chain [145]: 20 with precondition: [E>=3,E>=A+3,E>=C+3] * Chain [144]: 20 with precondition: [E>=3,E>=A+3,E>=C+3] * Chain [143]: 20 with precondition: [E>=3,E>=A+3,E>=C+3] * Chain [142]: 20 with precondition: [E>=3,E>=A+3,E>=C+3] * Chain [141]: 21 with precondition: [E>=3,E>=A+3,E>=C+3] * Chain [140]: 21 with precondition: [E>=3,E>=A+3,E>=C+3] * Chain [139]: 21 with precondition: [E>=3,E>=A+3,E>=C+3] * Chain [138]: 21 with precondition: [E>=3,E>=A+3,E>=C+3] * Chain [137]: 12 with precondition: [E>=3,E>=A+3,C+1>=E] * Chain [136]: 12 with precondition: [E>=3,E>=A+3,C+1>=E] * Chain [135]: 20 with precondition: [E>=3,E>=A+3,C+1>=E] * Chain [134]: 20 with precondition: [E>=3,E>=A+3,C+1>=E] * Chain [133]: 20 with precondition: [E>=3,E>=A+3,C+1>=E] * Chain [132]: 20 with precondition: [E>=3,E>=A+3,C+1>=E] * Chain [131]: 21 with precondition: [E>=3,E>=A+3,C+1>=E] * Chain [130]: 21 with precondition: [E>=3,E>=A+3,C+1>=E] * Chain [129]: 21 with precondition: [E>=3,E>=A+3,C+1>=E] * Chain [128]: 21 with precondition: [E>=3,E>=A+3,C+1>=E] * Chain [127]: 12 with precondition: [E>=3,E>=C+3,A+1>=E] * Chain [126]: 12 with precondition: [E>=3,E>=C+3,A+1>=E] * Chain [125]: 20 with precondition: [E>=3,E>=C+3,A+1>=E] * Chain [124]: 20 with precondition: [E>=3,E>=C+3,A+1>=E] * Chain [123]: 20 with precondition: [E>=3,E>=C+3,A+1>=E] * Chain [122]: 20 with precondition: [E>=3,E>=C+3,A+1>=E] * Chain [121]: 21 with precondition: [E>=3,E>=C+3,A+1>=E] * Chain [120]: 21 with precondition: [E>=3,E>=C+3,A+1>=E] * Chain [119]: 21 with precondition: [E>=3,E>=C+3,A+1>=E] * Chain [118]: 21 with precondition: [E>=3,E>=C+3,A+1>=E] * Chain [117]: 12 with precondition: [E>=3,A+1>=E,C+1>=E] * Chain [116]: 12 with precondition: [E>=3,A+1>=E,C+1>=E] * Chain [115]: 20 with precondition: [E>=3,A+1>=E,C+1>=E] * Chain [114]: 20 with precondition: [E>=3,A+1>=E,C+1>=E] * Chain [113]: 20 with precondition: [E>=3,A+1>=E,C+1>=E] * Chain [112]: 20 with precondition: [E>=3,A+1>=E,C+1>=E] * Chain [111]: 21 with precondition: [E>=3,A+1>=E,C+1>=E] * Chain [110]: 21 with precondition: [E>=3,A+1>=E,C+1>=E] * Chain [109]: 21 with precondition: [E>=3,A+1>=E,C+1>=E] * Chain [108]: 21 with precondition: [E>=3,A+1>=E,C+1>=E] * Chain [107]: 116*s(721)+5 with precondition: [E>=4] * Chain [106]: 116*s(731)+5 with precondition: [E>=4] * Chain [105]: 232*s(741)+6 with precondition: [E>=4] * Chain [104]: 232*s(761)+6 with precondition: [E>=4] * Chain [103]: 232*s(781)+6 with precondition: [E>=4] * Chain [102]: 232*s(801)+6 with precondition: [E>=4] * Chain [101]: 232*s(821)+7 with precondition: [E>=4] * Chain [100]: 232*s(841)+7 with precondition: [E>=4] * Chain [99]: 232*s(861)+7 with precondition: [E>=4] * Chain [98]: 232*s(881)+7 with precondition: [E>=4] * Chain [97]: 116*s(901)+13 with precondition: [E>=4,E>=A+3,E>=C+3] * Chain [96]: 116*s(911)+13 with precondition: [E>=4,E>=A+3,E>=C+3] * Chain [95]: 116*s(921)+13 with precondition: [E>=4,E>=A+3,E>=C+3] * Chain [94]: 116*s(931)+13 with precondition: [E>=4,E>=A+3,E>=C+3] * Chain [93]: 116*s(941)+13 with precondition: [E>=4,E>=A+3,E>=C+3] * Chain [92]: 116*s(951)+13 with precondition: [E>=4,E>=A+3,E>=C+3] * Chain [91]: 116*s(961)+13 with precondition: [E>=4,E>=A+3,E>=C+3] * Chain [90]: 116*s(971)+13 with precondition: [E>=4,E>=A+3,E>=C+3] * Chain [89]: 116*s(981)+14 with precondition: [E>=4,E>=A+3,E>=C+3] * Chain [88]: 116*s(991)+14 with precondition: [E>=4,E>=A+3,E>=C+3] * Chain [87]: 116*s(1001)+14 with precondition: [E>=4,E>=A+3,E>=C+3] * Chain [86]: 116*s(1011)+14 with precondition: [E>=4,E>=A+3,E>=C+3] * Chain [85]: 116*s(1021)+14 with precondition: [E>=4,E>=A+3,E>=C+3] * Chain [84]: 116*s(1031)+14 with precondition: [E>=4,E>=A+3,E>=C+3] * Chain [83]: 116*s(1041)+14 with precondition: [E>=4,E>=A+3,E>=C+3] * Chain [82]: 116*s(1051)+14 with precondition: [E>=4,E>=A+3,E>=C+3] * Chain [81]: 116*s(1061)+13 with precondition: [E>=4,E>=A+3,C+1>=E] * Chain [80]: 116*s(1071)+13 with precondition: [E>=4,E>=A+3,C+1>=E] * Chain [79]: 116*s(1081)+13 with precondition: [E>=4,E>=A+3,C+1>=E] * Chain [78]: 116*s(1091)+13 with precondition: [E>=4,E>=A+3,C+1>=E] * Chain [77]: 116*s(1101)+14 with precondition: [E>=4,E>=A+3,C+1>=E] * Chain [76]: 116*s(1111)+14 with precondition: [E>=4,E>=A+3,C+1>=E] * Chain [75]: 116*s(1121)+14 with precondition: [E>=4,E>=A+3,C+1>=E] * Chain [74]: 116*s(1131)+14 with precondition: [E>=4,E>=A+3,C+1>=E] * Chain [73]: 116*s(1141)+13 with precondition: [E>=4,E>=C+3,A+1>=E] * Chain [72]: 116*s(1151)+13 with precondition: [E>=4,E>=C+3,A+1>=E] * Chain [71]: 116*s(1161)+13 with precondition: [E>=4,E>=C+3,A+1>=E] * Chain [70]: 116*s(1171)+13 with precondition: [E>=4,E>=C+3,A+1>=E] * Chain [69]: 116*s(1181)+14 with precondition: [E>=4,E>=C+3,A+1>=E] * Chain [68]: 116*s(1191)+14 with precondition: [E>=4,E>=C+3,A+1>=E] * Chain [67]: 116*s(1201)+14 with precondition: [E>=4,E>=C+3,A+1>=E] * Chain [66]: 116*s(1211)+14 with precondition: [E>=4,E>=C+3,A+1>=E] * Chain [65]: 116*s(1221)+13 with precondition: [E>=4,A+1>=E,C+1>=E] * Chain [64]: 116*s(1231)+13 with precondition: [E>=4,A+1>=E,C+1>=E] * Chain [63]: 116*s(1241)+13 with precondition: [E>=4,A+1>=E,C+1>=E] * Chain [62]: 116*s(1251)+13 with precondition: [E>=4,A+1>=E,C+1>=E] * Chain [61]: 116*s(1261)+14 with precondition: [E>=4,A+1>=E,C+1>=E] * Chain [60]: 116*s(1271)+14 with precondition: [E>=4,A+1>=E,C+1>=E] * Chain [59]: 116*s(1281)+14 with precondition: [E>=4,A+1>=E,C+1>=E] * Chain [58]: 116*s(1291)+14 with precondition: [E>=4,A+1>=E,C+1>=E] Closed-form bounds of case_0(A,B,C,D,E): ------------------------------------- * Chain [392] with precondition: [E=C+1,E>=2,A>=E] - Lower bound: 5 - Complexity: constant * Chain [391] with precondition: [E=C+2,E>=3,A+1>=E] - Lower bound: 11 - Complexity: constant * Chain [390] with precondition: [E=C+2,E>=3,A+1>=E] - Lower bound: 11 - Complexity: constant * Chain [389] with precondition: [E=C+2,E>=3,A+1>=E] - Lower bound: 18 - Complexity: constant * Chain [388] with precondition: [E=C+2,E>=3,A+1>=E] - Lower bound: 18 - Complexity: constant * Chain [387] with precondition: [E=C+2,E>=3,A+1>=E] - Lower bound: 18 - Complexity: constant * Chain [386] with precondition: [E=C+2,E>=3,A+1>=E] - Lower bound: 18 - Complexity: constant * Chain [385] with precondition: [E=C+2,E>=3,A+1>=E] - Lower bound: 19 - Complexity: constant * Chain [384] with precondition: [E=C+2,E>=3,A+1>=E] - Lower bound: 19 - Complexity: constant * Chain [383] with precondition: [E=C+2,E>=3,A+1>=E] - Lower bound: 19 - Complexity: constant * Chain [382] with precondition: [E=C+2,E>=3,A+1>=E] - Lower bound: 19 - Complexity: constant * Chain [381] with precondition: [E=C+2,E>=4,E>=A+3] - Lower bound: 12 - Complexity: constant * Chain [380] with precondition: [E=C+2,E>=4,E>=A+3] - Lower bound: 12 - Complexity: constant * Chain [379] with precondition: [E=C+2,E>=4,E>=A+3] - Lower bound: 12 - Complexity: constant * Chain [378] with precondition: [E=C+2,E>=4,E>=A+3] - Lower bound: 12 - Complexity: constant * Chain [377] with precondition: [E=C+2,E>=4,E>=A+3] - Lower bound: 13 - Complexity: constant * Chain [376] with precondition: [E=C+2,E>=4,E>=A+3] - Lower bound: 13 - Complexity: constant * Chain [375] with precondition: [E=C+2,E>=4,E>=A+3] - Lower bound: 13 - Complexity: constant * Chain [374] with precondition: [E=C+2,E>=4,E>=A+3] - Lower bound: 13 - Complexity: constant * Chain [373] with precondition: [E=C+2,E>=4,E>=A+4] - Lower bound: 19 - Complexity: constant * Chain [372] with precondition: [E=C+2,E>=4,E>=A+4] - Lower bound: 19 - Complexity: constant * Chain [371] with precondition: [E=C+2,E>=4,E>=A+4] - Lower bound: 19 - Complexity: constant * Chain [370] with precondition: [E=C+2,E>=4,E>=A+4] - Lower bound: 19 - Complexity: constant * Chain [369] with precondition: [E=C+2,E>=4,E>=A+4] - Lower bound: 20 - Complexity: constant * Chain [368] with precondition: [E=C+2,E>=4,E>=A+4] - Lower bound: 20 - Complexity: constant * Chain [367] with precondition: [E=C+2,E>=4,E>=A+4] - Lower bound: 20 - Complexity: constant * Chain [366] with precondition: [E=C+2,E>=4,E>=A+4] - Lower bound: 20 - Complexity: constant * Chain [365] with precondition: [E=C+2,E>=4,A+1>=E] - Lower bound: 19 - Complexity: constant * Chain [364] with precondition: [E=C+2,E>=4,A+1>=E] - Lower bound: 19 - Complexity: constant * Chain [363] with precondition: [E=C+2,E>=4,A+1>=E] - Lower bound: 12 - Complexity: constant * Chain [362] with precondition: [E=C+2,E>=4,A+1>=E] - Lower bound: 12 - Complexity: constant * Chain [361] with precondition: [E=C+2,E>=4,A+1>=E] - Lower bound: 19 - Complexity: constant * Chain [360] with precondition: [E=C+2,E>=4,A+1>=E] - Lower bound: 19 - Complexity: constant * Chain [359] with precondition: [E=C+2,E>=4,A+1>=E] - Lower bound: 12 - Complexity: constant * Chain [358] with precondition: [E=C+2,E>=4,A+1>=E] - Lower bound: 12 - Complexity: constant * Chain [357] with precondition: [E=C+2,E>=4,A+1>=E] - Lower bound: 20 - Complexity: constant * Chain [356] with precondition: [E=C+2,E>=4,A+1>=E] - Lower bound: 20 - Complexity: constant * Chain [355] with precondition: [E=C+2,E>=4,A+1>=E] - Lower bound: 13 - Complexity: constant * Chain [354] with precondition: [E=C+2,E>=4,A+1>=E] - Lower bound: 13 - Complexity: constant * Chain [353] with precondition: [E=C+2,E>=4,A+1>=E] - Lower bound: 20 - Complexity: constant * Chain [352] with precondition: [E=C+2,E>=4,A+1>=E] - Lower bound: 20 - Complexity: constant * Chain [351] with precondition: [E=C+2,E>=4,A+1>=E] - Lower bound: 13 - Complexity: constant * Chain [350] with precondition: [E=C+2,E>=4,A+1>=E] - Lower bound: 13 - Complexity: constant * Chain [349] with precondition: [A+2=E,A>=1] - Lower bound: 9 - Complexity: constant * Chain [348] with precondition: [A+2=E,A>=1] - Lower bound: 9 - Complexity: constant * Chain [347] with precondition: [A+2=E,A>=1] - Lower bound: 14 - Complexity: constant * Chain [346] with precondition: [A+2=E,A>=1] - Lower bound: 14 - Complexity: constant * Chain [345] with precondition: [A+2=E,A>=1] - Lower bound: 14 - Complexity: constant * Chain [344] with precondition: [A+2=E,A>=1] - Lower bound: 14 - Complexity: constant * Chain [343] with precondition: [A+2=E,A>=1] - Lower bound: 15 - Complexity: constant * Chain [342] with precondition: [A+2=E,A>=1] - Lower bound: 15 - Complexity: constant * Chain [341] with precondition: [A+2=E,A>=1] - Lower bound: 15 - Complexity: constant * Chain [340] with precondition: [A+2=E,A>=1] - Lower bound: 15 - Complexity: constant * Chain [339] with precondition: [A+2=E,A>=2] - Lower bound: 10 - Complexity: constant * Chain [338] with precondition: [A+2=E,A>=2] - Lower bound: 10 - Complexity: constant * Chain [337] with precondition: [A+2=E,A>=2] - Lower bound: 10 - Complexity: constant * Chain [336] with precondition: [A+2=E,A>=2] - Lower bound: 10 - Complexity: constant * Chain [335] with precondition: [A+2=E,A>=2] - Lower bound: 11 - Complexity: constant * Chain [334] with precondition: [A+2=E,A>=2] - Lower bound: 11 - Complexity: constant * Chain [333] with precondition: [A+2=E,A>=2] - Lower bound: 11 - Complexity: constant * Chain [332] with precondition: [A+2=E,A>=2] - Lower bound: 11 - Complexity: constant * Chain [331] with precondition: [A+2=E,A>=2,C>=2] - Lower bound: 17 - Complexity: constant * Chain [330] with precondition: [A+2=E,A>=2,C>=2] - Lower bound: 17 - Complexity: constant * Chain [329] with precondition: [A+2=E,A>=2,C>=2] - Lower bound: 17 - Complexity: constant * Chain [328] with precondition: [A+2=E,A>=2,C>=2] - Lower bound: 17 - Complexity: constant * Chain [327] with precondition: [A+2=E,A>=2,C>=2] - Lower bound: 18 - Complexity: constant * Chain [326] with precondition: [A+2=E,A>=2,C>=2] - Lower bound: 18 - Complexity: constant * Chain [325] with precondition: [A+2=E,A>=2,C>=2] - Lower bound: 18 - Complexity: constant * Chain [324] with precondition: [A+2=E,A>=2,C>=2] - Lower bound: 18 - Complexity: constant * Chain [323] with precondition: [A+2=E,A>=2,A>=C+2] - Lower bound: 17 - Complexity: constant * Chain [322] with precondition: [A+2=E,A>=2,A>=C+2] - Lower bound: 17 - Complexity: constant * Chain [321] with precondition: [A+2=E,A>=2,A>=C+2] - Lower bound: 17 - Complexity: constant * Chain [320] with precondition: [A+2=E,A>=2,A>=C+2] - Lower bound: 17 - Complexity: constant * Chain [319] with precondition: [A+2=E,A>=2,A>=C+2] - Lower bound: 18 - Complexity: constant * Chain [318] with precondition: [A+2=E,A>=2,A>=C+2] - Lower bound: 18 - Complexity: constant * Chain [317] with precondition: [A+2=E,A>=2,A>=C+2] - Lower bound: 18 - Complexity: constant * Chain [316] with precondition: [A+2=E,A>=2,A>=C+2] - Lower bound: 18 - Complexity: constant * Chain [315] with precondition: [A+2=E,C>=1,A>=C+1] - Lower bound: 16 - Complexity: constant * Chain [314] with precondition: [A+2=E,C>=1,A>=C+1] - Lower bound: 16 - Complexity: constant * Chain [313] with precondition: [A+2=E,C>=1,A>=C+1] - Lower bound: 16 - Complexity: constant * Chain [312] with precondition: [A+2=E,C>=1,A>=C+1] - Lower bound: 16 - Complexity: constant * Chain [311] with precondition: [A+2=E,C>=1,A>=C+1] - Lower bound: 17 - Complexity: constant * Chain [310] with precondition: [A+2=E,C>=1,A>=C+1] - Lower bound: 17 - Complexity: constant * Chain [309] with precondition: [A+2=E,C>=1,A>=C+1] - Lower bound: 17 - Complexity: constant * Chain [308] with precondition: [A+2=E,C>=1,A>=C+1] - Lower bound: 17 - Complexity: constant * Chain [307] with precondition: [A+1=E,A>=1] - Lower bound: 3 - Complexity: constant * Chain [306] with precondition: [C+2=E,A>=1,C>=A+1] - Lower bound: 16 - Complexity: constant * Chain [305] with precondition: [C+2=E,A>=1,C>=A+1] - Lower bound: 16 - Complexity: constant * Chain [304] with precondition: [C+2=E,A>=1,C>=A+1] - Lower bound: 16 - Complexity: constant * Chain [303] with precondition: [C+2=E,A>=1,C>=A+1] - Lower bound: 16 - Complexity: constant * Chain [302] with precondition: [C+2=E,A>=1,C>=A+1] - Lower bound: 17 - Complexity: constant * Chain [301] with precondition: [C+2=E,A>=1,C>=A+1] - Lower bound: 17 - Complexity: constant * Chain [300] with precondition: [C+2=E,A>=1,C>=A+1] - Lower bound: 17 - Complexity: constant * Chain [299] with precondition: [C+2=E,A>=1,C>=A+1] - Lower bound: 17 - Complexity: constant * Chain [298] with precondition: [C+2=E,A>=2,C>=A+1] - Lower bound: 19 - Complexity: constant * Chain [297] with precondition: [C+2=E,A>=2,C>=A+1] - Lower bound: 19 - Complexity: constant * Chain [296] with precondition: [C+2=E,A>=2,C>=A+1] - Lower bound: 19 - Complexity: constant * Chain [295] with precondition: [C+2=E,A>=2,C>=A+1] - Lower bound: 19 - Complexity: constant * Chain [294] with precondition: [C+2=E,A>=2,C>=A+1] - Lower bound: 20 - Complexity: constant * Chain [293] with precondition: [C+2=E,A>=2,C>=A+1] - Lower bound: 20 - Complexity: constant * Chain [292] with precondition: [C+2=E,A>=2,C>=A+1] - Lower bound: 20 - Complexity: constant * Chain [291] with precondition: [C+2=E,A>=2,C>=A+1] - Lower bound: 20 - Complexity: constant * Chain [290] with precondition: [C+2=E,C>=1,C>=A+1] - Lower bound: 11 - Complexity: constant * Chain [289] with precondition: [C+2=E,C>=1,C>=A+1] - Lower bound: 11 - Complexity: constant * Chain [288] with precondition: [C+2=E,C>=1,C>=A+1] - Lower bound: 18 - Complexity: constant * Chain [287] with precondition: [C+2=E,C>=1,C>=A+1] - Lower bound: 18 - Complexity: constant * Chain [286] with precondition: [C+2=E,C>=1,C>=A+1] - Lower bound: 18 - Complexity: constant * Chain [285] with precondition: [C+2=E,C>=1,C>=A+1] - Lower bound: 18 - Complexity: constant * Chain [284] with precondition: [C+2=E,C>=1,C>=A+1] - Lower bound: 19 - Complexity: constant * Chain [283] with precondition: [C+2=E,C>=1,C>=A+1] - Lower bound: 19 - Complexity: constant * Chain [282] with precondition: [C+2=E,C>=1,C>=A+1] - Lower bound: 19 - Complexity: constant * Chain [281] with precondition: [C+2=E,C>=1,C>=A+1] - Lower bound: 19 - Complexity: constant * Chain [280] with precondition: [C+1=E,C>=1,C>=A+1] - Lower bound: 5 - Complexity: constant * Chain [279] with precondition: [A>=1,E>=4,E>=A+2] - Lower bound: 10 - Complexity: constant * Chain [278] with precondition: [A>=1,E>=4,E>=A+2] - Lower bound: 10 - Complexity: constant * Chain [277] with precondition: [A>=1,E>=4,E>=A+2] - Lower bound: 10 - Complexity: constant * Chain [276] with precondition: [A>=1,E>=4,E>=A+2] - Lower bound: 10 - Complexity: constant * Chain [275] with precondition: [A>=1,E>=4,E>=A+2] - Lower bound: 11 - Complexity: constant * Chain [274] with precondition: [A>=1,E>=4,E>=A+2] - Lower bound: 11 - Complexity: constant * Chain [273] with precondition: [A>=1,E>=4,E>=A+2] - Lower bound: 11 - Complexity: constant * Chain [272] with precondition: [A>=1,E>=4,E>=A+2] - Lower bound: 11 - Complexity: constant * Chain [271] with precondition: [A>=1,E>=A+3,E>=C+3] - Lower bound: 17 - Complexity: constant * Chain [270] with precondition: [A>=1,E>=A+3,E>=C+3] - Lower bound: 17 - Complexity: constant * Chain [269] with precondition: [A>=1,E>=A+3,E>=C+3] - Lower bound: 17 - Complexity: constant * Chain [268] with precondition: [A>=1,E>=A+3,E>=C+3] - Lower bound: 17 - Complexity: constant * Chain [267] with precondition: [A>=1,E>=A+3,E>=C+3] - Lower bound: 18 - Complexity: constant * Chain [266] with precondition: [A>=1,E>=A+3,E>=C+3] - Lower bound: 18 - Complexity: constant * Chain [265] with precondition: [A>=1,E>=A+3,E>=C+3] - Lower bound: 18 - Complexity: constant * Chain [264] with precondition: [A>=1,E>=A+3,E>=C+3] - Lower bound: 18 - Complexity: constant * Chain [263] with precondition: [A>=1,E>=A+3,C+1>=E] - Lower bound: 17 - Complexity: constant * Chain [262] with precondition: [A>=1,E>=A+3,C+1>=E] - Lower bound: 17 - Complexity: constant * Chain [261] with precondition: [A>=1,E>=A+3,C+1>=E] - Lower bound: 17 - Complexity: constant * Chain [260] with precondition: [A>=1,E>=A+3,C+1>=E] - Lower bound: 17 - Complexity: constant * Chain [259] with precondition: [A>=1,E>=A+3,C+1>=E] - Lower bound: 18 - Complexity: constant * Chain [258] with precondition: [A>=1,E>=A+3,C+1>=E] - Lower bound: 18 - Complexity: constant * Chain [257] with precondition: [A>=1,E>=A+3,C+1>=E] - Lower bound: 18 - Complexity: constant * Chain [256] with precondition: [A>=1,E>=A+3,C+1>=E] - Lower bound: 18 - Complexity: constant * Chain [255] with precondition: [A>=2,C>=2,E>=4] - Lower bound: 13 - Complexity: constant * Chain [254] with precondition: [A>=2,C>=2,E>=4] - Lower bound: 13 - Complexity: constant * Chain [253] with precondition: [A>=2,C>=2,E>=4] - Lower bound: 13 - Complexity: constant * Chain [252] with precondition: [A>=2,C>=2,E>=4] - Lower bound: 13 - Complexity: constant * Chain [251] with precondition: [A>=2,C>=2,E>=4] - Lower bound: 14 - Complexity: constant * Chain [250] with precondition: [A>=2,C>=2,E>=4] - Lower bound: 14 - Complexity: constant * Chain [249] with precondition: [A>=2,C>=2,E>=4] - Lower bound: 14 - Complexity: constant * Chain [248] with precondition: [A>=2,C>=2,E>=4] - Lower bound: 14 - Complexity: constant * Chain [247] with precondition: [A>=2,C>=2,E>=A+3,E>=C+3] - Lower bound: 20 - Complexity: constant * Chain [246] with precondition: [A>=2,C>=2,E>=A+3,E>=C+3] - Lower bound: 20 - Complexity: constant * Chain [245] with precondition: [A>=2,C>=2,E>=A+3,E>=C+3] - Lower bound: 20 - Complexity: constant * Chain [244] with precondition: [A>=2,C>=2,E>=A+3,E>=C+3] - Lower bound: 20 - Complexity: constant * Chain [243] with precondition: [A>=2,C>=2,E>=A+3,E>=C+3] - Lower bound: 21 - Complexity: constant * Chain [242] with precondition: [A>=2,C>=2,E>=A+3,E>=C+3] - Lower bound: 21 - Complexity: constant * Chain [241] with precondition: [A>=2,C>=2,E>=A+3,E>=C+3] - Lower bound: 21 - Complexity: constant * Chain [240] with precondition: [A>=2,C>=2,E>=A+3,E>=C+3] - Lower bound: 21 - Complexity: constant * Chain [239] with precondition: [A>=2,E>=4,A>=C+2,E>=C+3] - Lower bound: 13 - Complexity: constant * Chain [238] with precondition: [A>=2,E>=4,A>=C+2,E>=C+3] - Lower bound: 13 - Complexity: constant * Chain [237] with precondition: [A>=2,E>=4,A>=C+2,E>=C+3] - Lower bound: 13 - Complexity: constant * Chain [236] with precondition: [A>=2,E>=4,A>=C+2,E>=C+3] - Lower bound: 13 - Complexity: constant * Chain [235] with precondition: [A>=2,E>=4,A>=C+2,E>=C+3] - Lower bound: 14 - Complexity: constant * Chain [234] with precondition: [A>=2,E>=4,A>=C+2,E>=C+3] - Lower bound: 14 - Complexity: constant * Chain [233] with precondition: [A>=2,E>=4,A>=C+2,E>=C+3] - Lower bound: 14 - Complexity: constant * Chain [232] with precondition: [A>=2,E>=4,A>=C+2,E>=C+3] - Lower bound: 14 - Complexity: constant * Chain [231] with precondition: [A>=2,E>=A+3,A>=C+2] - Lower bound: 20 - Complexity: constant * Chain [230] with precondition: [A>=2,E>=A+3,A>=C+2] - Lower bound: 20 - Complexity: constant * Chain [229] with precondition: [A>=2,E>=A+3,A>=C+2] - Lower bound: 20 - Complexity: constant * Chain [228] with precondition: [A>=2,E>=A+3,A>=C+2] - Lower bound: 20 - Complexity: constant * Chain [227] with precondition: [A>=2,E>=A+3,A>=C+2] - Lower bound: 21 - Complexity: constant * Chain [226] with precondition: [A>=2,E>=A+3,A>=C+2] - Lower bound: 21 - Complexity: constant * Chain [225] with precondition: [A>=2,E>=A+3,A>=C+2] - Lower bound: 21 - Complexity: constant * Chain [224] with precondition: [A>=2,E>=A+3,A>=C+2] - Lower bound: 21 - Complexity: constant * Chain [223] with precondition: [A>=2,E>=A+3,C+1>=E] - Lower bound: 20 - Complexity: constant * Chain [222] with precondition: [A>=2,E>=A+3,C+1>=E] - Lower bound: 20 - Complexity: constant * Chain [221] with precondition: [A>=2,E>=A+3,C+1>=E] - Lower bound: 20 - Complexity: constant * Chain [220] with precondition: [A>=2,E>=A+3,C+1>=E] - Lower bound: 20 - Complexity: constant * Chain [219] with precondition: [A>=2,E>=A+3,C+1>=E] - Lower bound: 21 - Complexity: constant * Chain [218] with precondition: [A>=2,E>=A+3,C+1>=E] - Lower bound: 21 - Complexity: constant * Chain [217] with precondition: [A>=2,E>=A+3,C+1>=E] - Lower bound: 21 - Complexity: constant * Chain [216] with precondition: [A>=2,E>=A+3,C+1>=E] - Lower bound: 21 - Complexity: constant * Chain [215] with precondition: [C>=1,E>=4,C>=A+1,E>=C+2] - Lower bound: 12 - Complexity: constant * Chain [214] with precondition: [C>=1,E>=4,C>=A+1,E>=C+2] - Lower bound: 12 - Complexity: constant * Chain [213] with precondition: [C>=1,E>=4,C>=A+1,E>=C+2] - Lower bound: 12 - Complexity: constant * Chain [212] with precondition: [C>=1,E>=4,C>=A+1,E>=C+2] - Lower bound: 12 - Complexity: constant * Chain [211] with precondition: [C>=1,E>=4,C>=A+1,E>=C+2] - Lower bound: 13 - Complexity: constant * Chain [210] with precondition: [C>=1,E>=4,C>=A+1,E>=C+2] - Lower bound: 13 - Complexity: constant * Chain [209] with precondition: [C>=1,E>=4,C>=A+1,E>=C+2] - Lower bound: 13 - Complexity: constant * Chain [208] with precondition: [C>=1,E>=4,C>=A+1,E>=C+2] - Lower bound: 13 - Complexity: constant * Chain [207] with precondition: [C>=1,E>=4,A>=C+1,E>=C+2] - Lower bound: 12 - Complexity: constant * Chain [206] with precondition: [C>=1,E>=4,A>=C+1,E>=C+2] - Lower bound: 12 - Complexity: constant * Chain [205] with precondition: [C>=1,E>=4,A>=C+1,E>=C+2] - Lower bound: 12 - Complexity: constant * Chain [204] with precondition: [C>=1,E>=4,A>=C+1,E>=C+2] - Lower bound: 12 - Complexity: constant * Chain [203] with precondition: [C>=1,E>=4,A>=C+1,E>=C+2] - Lower bound: 13 - Complexity: constant * Chain [202] with precondition: [C>=1,E>=4,A>=C+1,E>=C+2] - Lower bound: 13 - Complexity: constant * Chain [201] with precondition: [C>=1,E>=4,A>=C+1,E>=C+2] - Lower bound: 13 - Complexity: constant * Chain [200] with precondition: [C>=1,E>=4,A>=C+1,E>=C+2] - Lower bound: 13 - Complexity: constant * Chain [199] with precondition: [C>=1,C>=A+1,E>=C+3] - Lower bound: 19 - Complexity: constant * Chain [198] with precondition: [C>=1,C>=A+1,E>=C+3] - Lower bound: 19 - Complexity: constant * Chain [197] with precondition: [C>=1,C>=A+1,E>=C+3] - Lower bound: 19 - Complexity: constant * Chain [196] with precondition: [C>=1,C>=A+1,E>=C+3] - Lower bound: 19 - Complexity: constant * Chain [195] with precondition: [C>=1,C>=A+1,E>=C+3] - Lower bound: 20 - Complexity: constant * Chain [194] with precondition: [C>=1,C>=A+1,E>=C+3] - Lower bound: 20 - Complexity: constant * Chain [193] with precondition: [C>=1,C>=A+1,E>=C+3] - Lower bound: 20 - Complexity: constant * Chain [192] with precondition: [C>=1,C>=A+1,E>=C+3] - Lower bound: 20 - Complexity: constant * Chain [191] with precondition: [C>=1,E>=A+3,A>=C+1] - Lower bound: 19 - Complexity: constant * Chain [190] with precondition: [C>=1,E>=A+3,A>=C+1] - Lower bound: 19 - Complexity: constant * Chain [189] with precondition: [C>=1,E>=A+3,A>=C+1] - Lower bound: 19 - Complexity: constant * Chain [188] with precondition: [C>=1,E>=A+3,A>=C+1] - Lower bound: 19 - Complexity: constant * Chain [187] with precondition: [C>=1,E>=A+3,A>=C+1] - Lower bound: 20 - Complexity: constant * Chain [186] with precondition: [C>=1,E>=A+3,A>=C+1] - Lower bound: 20 - Complexity: constant * Chain [185] with precondition: [C>=1,E>=A+3,A>=C+1] - Lower bound: 20 - Complexity: constant * Chain [184] with precondition: [C>=1,E>=A+3,A>=C+1] - Lower bound: 20 - Complexity: constant * Chain [183] with precondition: [C>=1,E>=C+3,A+1>=E] - Lower bound: 19 - Complexity: constant * Chain [182] with precondition: [C>=1,E>=C+3,A+1>=E] - Lower bound: 19 - Complexity: constant * Chain [181] with precondition: [C>=1,E>=C+3,A+1>=E] - Lower bound: 19 - Complexity: constant * Chain [180] with precondition: [C>=1,E>=C+3,A+1>=E] - Lower bound: 19 - Complexity: constant * Chain [179] with precondition: [C>=1,E>=C+3,A+1>=E] - Lower bound: 20 - Complexity: constant * Chain [178] with precondition: [C>=1,E>=C+3,A+1>=E] - Lower bound: 20 - Complexity: constant * Chain [177] with precondition: [C>=1,E>=C+3,A+1>=E] - Lower bound: 20 - Complexity: constant * Chain [176] with precondition: [C>=1,E>=C+3,A+1>=E] - Lower bound: 20 - Complexity: constant * Chain [175] with precondition: [C>=2,E>=4,C>=A+2,E>=A+3] - Lower bound: 13 - Complexity: constant * Chain [174] with precondition: [C>=2,E>=4,C>=A+2,E>=A+3] - Lower bound: 13 - Complexity: constant * Chain [173] with precondition: [C>=2,E>=4,C>=A+2,E>=A+3] - Lower bound: 13 - Complexity: constant * Chain [172] with precondition: [C>=2,E>=4,C>=A+2,E>=A+3] - Lower bound: 13 - Complexity: constant * Chain [171] with precondition: [C>=2,E>=4,C>=A+2,E>=A+3] - Lower bound: 14 - Complexity: constant * Chain [170] with precondition: [C>=2,E>=4,C>=A+2,E>=A+3] - Lower bound: 14 - Complexity: constant * Chain [169] with precondition: [C>=2,E>=4,C>=A+2,E>=A+3] - Lower bound: 14 - Complexity: constant * Chain [168] with precondition: [C>=2,E>=4,C>=A+2,E>=A+3] - Lower bound: 14 - Complexity: constant * Chain [167] with precondition: [C>=2,C>=A+2,E>=C+3] - Lower bound: 20 - Complexity: constant * Chain [166] with precondition: [C>=2,C>=A+2,E>=C+3] - Lower bound: 20 - Complexity: constant * Chain [165] with precondition: [C>=2,C>=A+2,E>=C+3] - Lower bound: 20 - Complexity: constant * Chain [164] with precondition: [C>=2,C>=A+2,E>=C+3] - Lower bound: 20 - Complexity: constant * Chain [163] with precondition: [C>=2,C>=A+2,E>=C+3] - Lower bound: 21 - Complexity: constant * Chain [162] with precondition: [C>=2,C>=A+2,E>=C+3] - Lower bound: 21 - Complexity: constant * Chain [161] with precondition: [C>=2,C>=A+2,E>=C+3] - Lower bound: 21 - Complexity: constant * Chain [160] with precondition: [C>=2,C>=A+2,E>=C+3] - Lower bound: 21 - Complexity: constant * Chain [159] with precondition: [C>=2,E>=C+3,A+1>=E] - Lower bound: 20 - Complexity: constant * Chain [158] with precondition: [C>=2,E>=C+3,A+1>=E] - Lower bound: 20 - Complexity: constant * Chain [157] with precondition: [C>=2,E>=C+3,A+1>=E] - Lower bound: 20 - Complexity: constant * Chain [156] with precondition: [C>=2,E>=C+3,A+1>=E] - Lower bound: 20 - Complexity: constant * Chain [155] with precondition: [C>=2,E>=C+3,A+1>=E] - Lower bound: 21 - Complexity: constant * Chain [154] with precondition: [C>=2,E>=C+3,A+1>=E] - Lower bound: 21 - Complexity: constant * Chain [153] with precondition: [C>=2,E>=C+3,A+1>=E] - Lower bound: 21 - Complexity: constant * Chain [152] with precondition: [C>=2,E>=C+3,A+1>=E] - Lower bound: 21 - Complexity: constant * Chain [151] with precondition: [E>=2,E>=A+2,E>=C+2] - Lower bound: 6 - Complexity: constant * Chain [150] with precondition: [E>=2,E>=A+2,C>=E] - Lower bound: 6 - Complexity: constant * Chain [149] with precondition: [E>=2,E>=C+2,A>=E] - Lower bound: 6 - Complexity: constant * Chain [148] with precondition: [E>=2,A>=E,C>=E] - Lower bound: 6 - Complexity: constant * Chain [147] with precondition: [E>=3,E>=A+3,E>=C+3] - Lower bound: 12 - Complexity: constant * Chain [146] with precondition: [E>=3,E>=A+3,E>=C+3] - Lower bound: 12 - Complexity: constant * Chain [145] with precondition: [E>=3,E>=A+3,E>=C+3] - Lower bound: 20 - Complexity: constant * Chain [144] with precondition: [E>=3,E>=A+3,E>=C+3] - Lower bound: 20 - Complexity: constant * Chain [143] with precondition: [E>=3,E>=A+3,E>=C+3] - Lower bound: 20 - Complexity: constant * Chain [142] with precondition: [E>=3,E>=A+3,E>=C+3] - Lower bound: 20 - Complexity: constant * Chain [141] with precondition: [E>=3,E>=A+3,E>=C+3] - Lower bound: 21 - Complexity: constant * Chain [140] with precondition: [E>=3,E>=A+3,E>=C+3] - Lower bound: 21 - Complexity: constant * Chain [139] with precondition: [E>=3,E>=A+3,E>=C+3] - Lower bound: 21 - Complexity: constant * Chain [138] with precondition: [E>=3,E>=A+3,E>=C+3] - Lower bound: 21 - Complexity: constant * Chain [137] with precondition: [E>=3,E>=A+3,C+1>=E] - Lower bound: 12 - Complexity: constant * Chain [136] with precondition: [E>=3,E>=A+3,C+1>=E] - Lower bound: 12 - Complexity: constant * Chain [135] with precondition: [E>=3,E>=A+3,C+1>=E] - Lower bound: 20 - Complexity: constant * Chain [134] with precondition: [E>=3,E>=A+3,C+1>=E] - Lower bound: 20 - Complexity: constant * Chain [133] with precondition: [E>=3,E>=A+3,C+1>=E] - Lower bound: 20 - Complexity: constant * Chain [132] with precondition: [E>=3,E>=A+3,C+1>=E] - Lower bound: 20 - Complexity: constant * Chain [131] with precondition: [E>=3,E>=A+3,C+1>=E] - Lower bound: 21 - Complexity: constant * Chain [130] with precondition: [E>=3,E>=A+3,C+1>=E] - Lower bound: 21 - Complexity: constant * Chain [129] with precondition: [E>=3,E>=A+3,C+1>=E] - Lower bound: 21 - Complexity: constant * Chain [128] with precondition: [E>=3,E>=A+3,C+1>=E] - Lower bound: 21 - Complexity: constant * Chain [127] with precondition: [E>=3,E>=C+3,A+1>=E] - Lower bound: 12 - Complexity: constant * Chain [126] with precondition: [E>=3,E>=C+3,A+1>=E] - Lower bound: 12 - Complexity: constant * Chain [125] with precondition: [E>=3,E>=C+3,A+1>=E] - Lower bound: 20 - Complexity: constant * Chain [124] with precondition: [E>=3,E>=C+3,A+1>=E] - Lower bound: 20 - Complexity: constant * Chain [123] with precondition: [E>=3,E>=C+3,A+1>=E] - Lower bound: 20 - Complexity: constant * Chain [122] with precondition: [E>=3,E>=C+3,A+1>=E] - Lower bound: 20 - Complexity: constant * Chain [121] with precondition: [E>=3,E>=C+3,A+1>=E] - Lower bound: 21 - Complexity: constant * Chain [120] with precondition: [E>=3,E>=C+3,A+1>=E] - Lower bound: 21 - Complexity: constant * Chain [119] with precondition: [E>=3,E>=C+3,A+1>=E] - Lower bound: 21 - Complexity: constant * Chain [118] with precondition: [E>=3,E>=C+3,A+1>=E] - Lower bound: 21 - Complexity: constant * Chain [117] with precondition: [E>=3,A+1>=E,C+1>=E] - Lower bound: 12 - Complexity: constant * Chain [116] with precondition: [E>=3,A+1>=E,C+1>=E] - Lower bound: 12 - Complexity: constant * Chain [115] with precondition: [E>=3,A+1>=E,C+1>=E] - Lower bound: 20 - Complexity: constant * Chain [114] with precondition: [E>=3,A+1>=E,C+1>=E] - Lower bound: 20 - Complexity: constant * Chain [113] with precondition: [E>=3,A+1>=E,C+1>=E] - Lower bound: 20 - Complexity: constant * Chain [112] with precondition: [E>=3,A+1>=E,C+1>=E] - Lower bound: 20 - Complexity: constant * Chain [111] with precondition: [E>=3,A+1>=E,C+1>=E] - Lower bound: 21 - Complexity: constant * Chain [110] with precondition: [E>=3,A+1>=E,C+1>=E] - Lower bound: 21 - Complexity: constant * Chain [109] with precondition: [E>=3,A+1>=E,C+1>=E] - Lower bound: 21 - Complexity: constant * Chain [108] with precondition: [E>=3,A+1>=E,C+1>=E] - Lower bound: 21 - Complexity: constant * Chain [107] with precondition: [E>=4] - Lower bound: 5 - Complexity: constant * Chain [106] with precondition: [E>=4] - Lower bound: 5 - Complexity: constant * Chain [105] with precondition: [E>=4] - Lower bound: 6 - Complexity: constant * Chain [104] with precondition: [E>=4] - Lower bound: 6 - Complexity: constant * Chain [103] with precondition: [E>=4] - Lower bound: 6 - Complexity: constant * Chain [102] with precondition: [E>=4] - Lower bound: 6 - Complexity: constant * Chain [101] with precondition: [E>=4] - Lower bound: 7 - Complexity: constant * Chain [100] with precondition: [E>=4] - Lower bound: 7 - Complexity: constant * Chain [99] with precondition: [E>=4] - Lower bound: 7 - Complexity: constant * Chain [98] with precondition: [E>=4] - Lower bound: 7 - Complexity: constant * Chain [97] with precondition: [E>=4,E>=A+3,E>=C+3] - Lower bound: 13 - Complexity: constant * Chain [96] with precondition: [E>=4,E>=A+3,E>=C+3] - Lower bound: 13 - Complexity: constant * Chain [95] with precondition: [E>=4,E>=A+3,E>=C+3] - Lower bound: 13 - Complexity: constant * Chain [94] with precondition: [E>=4,E>=A+3,E>=C+3] - Lower bound: 13 - Complexity: constant * Chain [93] with precondition: [E>=4,E>=A+3,E>=C+3] - Lower bound: 13 - Complexity: constant * Chain [92] with precondition: [E>=4,E>=A+3,E>=C+3] - Lower bound: 13 - Complexity: constant * Chain [91] with precondition: [E>=4,E>=A+3,E>=C+3] - Lower bound: 13 - Complexity: constant * Chain [90] with precondition: [E>=4,E>=A+3,E>=C+3] - Lower bound: 13 - Complexity: constant * Chain [89] with precondition: [E>=4,E>=A+3,E>=C+3] - Lower bound: 14 - Complexity: constant * Chain [88] with precondition: [E>=4,E>=A+3,E>=C+3] - Lower bound: 14 - Complexity: constant * Chain [87] with precondition: [E>=4,E>=A+3,E>=C+3] - Lower bound: 14 - Complexity: constant * Chain [86] with precondition: [E>=4,E>=A+3,E>=C+3] - Lower bound: 14 - Complexity: constant * Chain [85] with precondition: [E>=4,E>=A+3,E>=C+3] - Lower bound: 14 - Complexity: constant * Chain [84] with precondition: [E>=4,E>=A+3,E>=C+3] - Lower bound: 14 - Complexity: constant * Chain [83] with precondition: [E>=4,E>=A+3,E>=C+3] - Lower bound: 14 - Complexity: constant * Chain [82] with precondition: [E>=4,E>=A+3,E>=C+3] - Lower bound: 14 - Complexity: constant * Chain [81] with precondition: [E>=4,E>=A+3,C+1>=E] - Lower bound: 13 - Complexity: constant * Chain [80] with precondition: [E>=4,E>=A+3,C+1>=E] - Lower bound: 13 - Complexity: constant * Chain [79] with precondition: [E>=4,E>=A+3,C+1>=E] - Lower bound: 13 - Complexity: constant * Chain [78] with precondition: [E>=4,E>=A+3,C+1>=E] - Lower bound: 13 - Complexity: constant * Chain [77] with precondition: [E>=4,E>=A+3,C+1>=E] - Lower bound: 14 - Complexity: constant * Chain [76] with precondition: [E>=4,E>=A+3,C+1>=E] - Lower bound: 14 - Complexity: constant * Chain [75] with precondition: [E>=4,E>=A+3,C+1>=E] - Lower bound: 14 - Complexity: constant * Chain [74] with precondition: [E>=4,E>=A+3,C+1>=E] - Lower bound: 14 - Complexity: constant * Chain [73] with precondition: [E>=4,E>=C+3,A+1>=E] - Lower bound: 13 - Complexity: constant * Chain [72] with precondition: [E>=4,E>=C+3,A+1>=E] - Lower bound: 13 - Complexity: constant * Chain [71] with precondition: [E>=4,E>=C+3,A+1>=E] - Lower bound: 13 - Complexity: constant * Chain [70] with precondition: [E>=4,E>=C+3,A+1>=E] - Lower bound: 13 - Complexity: constant * Chain [69] with precondition: [E>=4,E>=C+3,A+1>=E] - Lower bound: 14 - Complexity: constant * Chain [68] with precondition: [E>=4,E>=C+3,A+1>=E] - Lower bound: 14 - Complexity: constant * Chain [67] with precondition: [E>=4,E>=C+3,A+1>=E] - Lower bound: 14 - Complexity: constant * Chain [66] with precondition: [E>=4,E>=C+3,A+1>=E] - Lower bound: 14 - Complexity: constant * Chain [65] with precondition: [E>=4,A+1>=E,C+1>=E] - Lower bound: 13 - Complexity: constant * Chain [64] with precondition: [E>=4,A+1>=E,C+1>=E] - Lower bound: 13 - Complexity: constant * Chain [63] with precondition: [E>=4,A+1>=E,C+1>=E] - Lower bound: 13 - Complexity: constant * Chain [62] with precondition: [E>=4,A+1>=E,C+1>=E] - Lower bound: 13 - Complexity: constant * Chain [61] with precondition: [E>=4,A+1>=E,C+1>=E] - Lower bound: 14 - Complexity: constant * Chain [60] with precondition: [E>=4,A+1>=E,C+1>=E] - Lower bound: 14 - Complexity: constant * Chain [59] with precondition: [E>=4,A+1>=E,C+1>=E] - Lower bound: 14 - Complexity: constant * Chain [58] with precondition: [E>=4,A+1>=E,C+1>=E] - Lower bound: 14 - Complexity: constant ### Partitioned lower bound of case_0(A,B,C,D,E): * 3 if [E=A+1,C>=2,E>=C+3] or [E=A+1,E>=4,C+1>=E] or [E=A+1,1>=C,E>=4] or [C+1=A,C+2=E,C>=2] or [A=1,E=2] or [A=2,E=3] * 5 if [E=A+2,C>=2,E>=C+4] or [A>=2,E>=A+3,C+1>=E] or [E>=4,A>=E,C>=E] or [A>=2,C>=A+2,E>=C+2] or [C+2=E,C>=2,A>=C+2] or [A+1=C,A>=2,E>=A+4] or [A=C+1,A>=3,E>=A+3] or [0>=C,A>=2,E>=A+3] or [A=C,A>=2,E>=A+3] or [E=A+2,E=C+3,E>=5] or [C=1,E=A+2,E>=5] or [1>=A,E>=4,C+1>=E] or [0>=C,E>=4,C>=A+1] or [1>=C,E>=4,A>=E] or [0>=A,E>=4,A>=C] or [E=A+2,0>=C,E>=4] or [E=A+2,E>=4,C+2>=E] or [C+1=E,C>=3,A>=C+1] or [C=A+1,C+2=E,C>=3] or [A=1,C>=3,E>=C+2] or [C>=2,E>=C+3,A>=E] or [C>=2,E>=A+3,A>=C+2] or [0>=A,C>=2,E>=C+2] or [C=1,A>=3,E>=A+3] or [C=2,E=3,A>=3] or [C=1,E=2,A>=2] or [A=1,1>=C,E>=4] or [C=1,0>=A,E>=4] or [C=2,E=3,0>=A] or [A=2,C=1,E>=4] or [C=1,E=2,0>=A] or [A=1,C=2,E>=3] * 6 if [E=3,A>=3,C>=3] or [E=2,A>=2,C>=2] or [E=2,0>=C+1,C>=A+1] or [E=2,0>=C,A>=2] or [E=3,0>=C,C>=A+1] or [E=3,1>=C,A>=3] or [A=0,E=2,0>=C] or [A=1,E=3,1>=C] or [E=2,0>=A+1,A>=C] or [E=2,0>=A,C>=2] or [C=0,E=2,0>=A+1] or [E=3,0>=A,A>=C] or [E=3,1>=A,C>=3] or [C=1,E=3,0>=A] Possible lower bounds : [3,5,6] Maximum lower bound complexity: constant * Total analysis performed in 2882 ms.