Abs program loaded in 4 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 8 ms.
sabu_memo_table_1(case_0,[A,B,C,D,E,F],[1*D>=0,1*C>=0,1*F=0,1*C=0,1*D=1,1*E=0],0,0)
sabu_memo_table_1(case_2,[A,B,C,D,E,F,G,H],[1*D>=0,1*C>=0,1*A+ -1*F=0,1*G+ -1*H=0],0,0)
sabu_memo_table_1(assoc,[A,B,C,D,E,F],[1*D>=0,1*C>=0,1*E=0,1*D=1,1*C=0,1*F=0,1*C>=0,1*D>=0],1,0)
sabu_memo_table_1(case_1,[A,B,C,D,E,F,G,H,I],[1*G>=0,1*F>=0,1*I>=0,1*A+ -1*B=0,1*D+ -1*I=0,1*C=1],1,0)
sabu_memo_table_1(case_0,[A,B,C,D,E,F],[1*C>=0,1*E+ -1*F>=0,1*F>=0,1*D>=1],2,1)
sabu_memo_table_1(case_2,[A,B,C,D,E,F,G,H],[1*D>=0,-1*A+1*F>=0,1*C>=0],2,1)
sabu_memo_table_1(case_2,[A,B,C,D,E,F,G,H],[1*D>=0,1*C>=0],2,2)
sabu_memo_table_1(assoc,[A,B,C,D,E,F],[1*E+ -1*F>=0,1*F>=0,1*D>=1,1*C>=0],3,1)
sabu_memo_table_1(case_1,[A,B,C,D,E,F,G,H,I],[1*D>=0,1*F>=0,1*G>=0,1*C=1],3,1)
sabu_memo_table_1(case_0,[A,B,C,D,E,F],[1*C>=0,1*E>=0,1*D>=1],4,2)
sabu_memo_table_1(assoc,[A,B,C,D,E,F],[1*E>=0,1*D>=1,1*C>=0],5,2)
sabu_memo_table_1(case_3,[A,B,C],[1*B>=0,1*C>=0,1*B=1,1*A+ -1*C=0],0,0)
sabu_memo_table_1(aux,[A,B,C],[1*B>=0,1*A>=0,1*A+ -1*C=0,1*B=1,1*C>=0,1*B>=0],1,0)
sabu_memo_table_1(case_3,[A,B,C],[1*A>=0,1*A+ -1*C>= -1,-1*A+1*C>=0,1*A+1*B+ -1*C=1],2,1)
sabu_memo_table_1(aux,[A,B,C],[1*A>=0,1*A+ -1*C>= -1,-1*A+1*C>=0,1*A+1*B+ -1*C=1],3,1)
sabu_memo_table_1(case_3,[A,B,C],[-1*B>= -3,1*B>=1,1*A>=0,1*A+1*B+ -1*C=1],4,2)
sabu_memo_table_1(aux,[A,B,C],[-1*B>= -3,1*B>=1,1*A>=0,1*A+1*B+ -1*C=1],5,2)
sabu_memo_table_1(case_3,[A,B,C],[-1*B>= -4,1*B>=1,1*A>=0,1*A+1*B+ -1*C=1],6,3)
sabu_memo_table_1(aux,[A,B,C],[-1*B>= -4,1*B>=1,1*A>=0,1*A+1*B+ -1*C=1],7,3)
sabu_memo_table_1(case_3,[A,B,C],[1*A+1*B+ -1*C=1,1*A>=0,1*B>=1],8,0)
sabu_memo_table_1(aux,[A,B,C],[1*A+1*B+ -1*C=1,1*A>=0,1*B>=1],9,0)
sabu_memo_table_1(case_4,[A,B,C],[1*C>=0,1*A>=0,1*A=1,1*B+ -1*C=0],0,0)
sabu_memo_table_1(concat,[A,B,C],[1*B>=0,1*A>=0,1*B+ -1*C=0,1*A=1,1*A>=0,1*C>=0],0,0)
sabu_memo_table_1(case_4,[A,B,C],[1*B>=0,1*B+ -1*C>= -1,-1*B+1*C>=0,1*A+1*B+ -1*C=1],1,1)
sabu_memo_table_1(concat,[A,B,C],[1*B>=0,1*B+ -1*C>= -1,-1*B+1*C>=0,1*A+1*B+ -1*C=1],2,1)
sabu_memo_table_1(case_4,[A,B,C],[-1*A>= -3,1*A>=1,1*B>=0,1*A+1*B+ -1*C=1],3,2)
sabu_memo_table_1(concat,[A,B,C],[-1*A>= -3,1*A>=1,1*B>=0,1*A+1*B+ -1*C=1],4,2)
sabu_memo_table_1(case_4,[A,B,C],[-1*A>= -4,1*A>=1,1*B>=0,1*A+1*B+ -1*C=1],5,3)
sabu_memo_table_1(concat,[A,B,C],[-1*A>= -4,1*A>=1,1*B>=0,1*A+1*B+ -1*C=1],6,3)
sabu_memo_table_1(case_4,[A,B,C],[1*A+1*B+ -1*C=1,1*B>=0,1*A>=1],7,0)
sabu_memo_table_1(concat,[A,B,C],[1*A+1*B+ -1*C=1,1*B>=0,1*A>=1],8,0)
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_5,[A,B,C,D,E,F,G],[1*D>=0,1*C>=1,1*B>=0,1*F=1],0,0)
sabu_memo_table_1(eval,[A,B,C,D,E,F,G],[1*F>=0,1*C>=0,1*B>=0,1*F=1,1*B>=0,1*C>=1,1*D>=0],0,0)
sabu_memo_table_1(rev,[A],[1*A>=1],0,0)
sabu_memo_table_1(case_6,[A,B,C,D,E,F,G,H,I],[1*D>=0,1*C>=1,1*B>=0,1*H=1,1*I=2,1*F=1],0,0)
sabu_memo_table_1(tableMake,[A,B,C,D,E,F,G,H,I],[1*H>=0,1*F>=0,1*C>=0,1*B>=0,1*F=1,1*I=2,1*H=1,1*B>=0,1*C>=1,1*D>=0],0,0)
sabu_memo_table_1(case_6,[A,B,C,D,E,F,G,H,I],[1*B>=0,1*C+1*I>=3,1*D>=0,-1*I>= -3,1*I>=2,1*H=1,1*F+ -1*I= -1],1,1)
sabu_memo_table_1(tableMake,[A,B,C,D,E,F,G,H,I],[1*B>=0,1*C+1*I>=3,1*D>=0,-1*I>= -3,1*I>=2,1*H=1,1*F+ -1*I= -1],2,1)
sabu_memo_table_1(case_6,[A,B,C,D,E,F,G,H,I],[1*C+2*F+ -1*I>=1,1*D>=0,3*F+ -2*I>= -1,1*B>=0,-2*F+1*I>= -1,-1*F+1*I>=1,1*H=1],3,2)
sabu_memo_table_1(tableMake,[A,B,C,D,E,F,G,H,I],[1*C+2*F+ -1*I>=1,1*D>=0,3*F+ -2*I>= -1,1*B>=0,-2*F+1*I>= -1,-1*F+1*I>=1,1*H=1],4,2)
sabu_memo_table_1(case_6,[A,B,C,D,E,F,G,H,I],[-4*F+1*I>= -7,1*C>=0,2*C+3*F+ -1*I>=3,7*F+ -3*I>=1,-1*F+1*I>=1,-2*F+1*I>= -1,1*D>=0,1*B>=0,1*H=1],5,3)
sabu_memo_table_1(tableMake,[A,B,C,D,E,F,G,H,I],[-4*F+1*I>= -7,1*C>=0,2*C+3*F+ -1*I>=3,7*F+ -3*I>=1,-1*F+1*I>=1,-2*F+1*I>= -1,1*D>=0,1*B>=0,1*H=1],6,3)
sabu_memo_table_1(case_6,[A,B,C,D,E,F,G,H,I],[1*H=1,1*B>=0,1*C>=0,1*D>=0,-4*F+1*I>= -7,-2*F+1*I>= -1,-1*F+1*I>=1],7,0)
sabu_memo_table_1(tableMake,[A,B,C,D,E,F,G,H,I],[1*H=1,1*B>=0,1*C>=0,1*D>=0,-4*F+1*I>= -7,-2*F+1*I>= -1,-1*F+1*I>=1],8,0)
sabu_memo_table_1(case_6,[A,B,C,D,E,F,G,H,I],[-1*F+1*I>=0,-2*F+1*I>= -1,-4*F+1*I>= -7,1*B>=0,1*C>=0,1*D>=0,1*H=1],9,1)
sabu_memo_table_1(tableMake,[A,B,C,D,E,F,G,H,I],[-4*F+1*I>= -7,-1*F+1*I>=0,-2*F+1*I>= -1,1*B>=0,1*C>=0,1*D>=0,1*H=1],10,1)
sabu_memo_table_1(case_6,[A,B,C,D,E,F,G,H,I],[-1*F+1*I>= -1,-4*F+1*I>= -7,1*B>=0,1*C>=0,1*D>=0,1*H=1],11,2)
sabu_memo_table_1(tableMake,[A,B,C,D,E,F,G,H,I],[-4*F+1*I>= -7,-1*F+1*I>= -1,1*B>=0,1*C>=0,1*D>=0,1*H=1],12,2)
sabu_memo_table_1(case_6,[A,B,C,D,E,F,G,H,I],[-4*F+1*I>= -11,-1*F+1*I>= -2,1*B>=0,1*C>=0,1*D>=0,1*H=1],13,3)
sabu_memo_table_1(tableMake,[A,B,C,D,E,F,G,H,I],[-4*F+1*I>= -11,-1*F+1*I>= -2,1*B>=0,1*C>=0,1*D>=0,1*H=1],14,3)
sabu_memo_table_1(case_6,[A,B,C,D,E,F,G,H,I],[1*H=1,1*D>=0,1*C>=0,1*B>=0],15,0)
sabu_memo_table_1(tableMake,[A,B,C,D,E,F,G,H,I],[1*H=1,1*D>=0,1*C>=0,1*B>=0],16,0)
sabu_memo_table_1(start,[A,B,C,D,E,F,G,H],[1*H>=0,1*F>=0,1*C>=0,1*B>=0,1*B>=0,1*C>=0,1*D>=0,1*H=1],0,0)
sabu_memo_table_1(start,[],[],0,0)
:- dynamic sabu_memo_table_1/5.

sabu_memo_table_1(case_2, [_, _, B, A, _, _, _, _], [1*A>=0, 1*B>=0], 2, 2).
sabu_memo_table_1(case_1, [_, _, D, A, _, B, C, _, _], [1*A>=0, 1*B>=0, 1*C>=0, 1*D=1], 3, 1).
sabu_memo_table_1(case_0, [_, _, A, C, B, _], [1*A>=0, 1*B>=0, 1*C>=1], 4, 2).
sabu_memo_table_1(assoc, [_, _, C, B, A, _], [1*A>=0, 1*B>=1, 1*C>=0], 5, 2).
sabu_memo_table_1(case_3, [A, B, C], [1*A+1*B+ -1*C=1, 1*A>=0, 1*B>=1], 8, 0).
sabu_memo_table_1(aux, [A, B, C], [1*A+1*B+ -1*C=1, 1*A>=0, 1*B>=1], 9, 0).
sabu_memo_table_1(case_4, [A, B, C], [1*A+1*B+ -1*C=1, 1*B>=0, 1*A>=1], 7, 0).
sabu_memo_table_1(concat, [A, B, C], [1*A+1*B+ -1*C=1, 1*B>=0, 1*A>=1], 8, 0).
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_5, [_, C, B, A, _, D, _], [1*A>=0, 1*B>=1, 1*C>=0, 1*D=1], 0, 0).
sabu_memo_table_1(eval, [_, C, B, D, _, A, _], [1*A>=0, 1*B>=0, 1*C>=0, 1*A=1, 1*C>=0, 1*B>=1, 1*D>=0], 0, 0).
sabu_memo_table_1(rev, [A], [1*A>=1], 0, 0).
sabu_memo_table_1(case_6, [_, D, C, B, _, _, _, A, _], [1*A=1, 1*B>=0, 1*C>=0, 1*D>=0], 15, 0).
sabu_memo_table_1(tableMake, [_, D, C, B, _, _, _, A, _], [1*A=1, 1*B>=0, 1*C>=0, 1*D>=0], 16, 0).
sabu_memo_table_1(start, [_, D, C, E, _, B, _, A], [1*A>=0, 1*B>=0, 1*C>=0, 1*D>=0, 1*D>=0, 1*C>=0, 1*E>=0, 1*A=1], 0, 0).
sabu_memo_table_1(start, [], [], 0, 0).


Size analysis performed in 62 ms.

Cost relation system stored in /tmp/costabs/crs.crs

Generated 47 equations 
removed eval(_G73,_G74,_G75,_G76,_G77,_G78)

Cost relation system solved by PUBS in 300 ms.

Method start terminates?: YES

 - valVars_1: size of valVars wrt. Rat
 - valVars_2: size of valVars wrt. Pair<Rat, Bool>
 - valVars_3: size of valVars wrt. List<Pair<Rat, Bool>>
 - valVars_4: size of valVars wrt. Bool
 - vars_1: size of vars wrt. Rat
 - vars_2: size of vars wrt. List<Rat>
 - expr_1: size of expr wrt. Rat
 - expr_2: size of expr wrt. BoolExpr
UB for start(valVars_1,valVars_2,valVars_3,valVars_4,vars_1,vars_2,expr_1,expr_2) = pow(2,nat(vars_2))*c(maximize_failed)+pow(2,nat(vars_2))*pow(2,log(4,nat(expr_2/2)+3))+pow(2,nat(vars_2))*pow(2,log(4,3+nat(expr_2/2)))*nat(valVars_3+vars_2)


Method start terminates?: YES

 - valVars_1: size of valVars wrt. Rat
 - valVars_2: size of valVars wrt. Pair<Rat, Bool>
 - valVars_3: size of valVars wrt. List<Pair<Rat, Bool>>
 - valVars_4: size of valVars wrt. Bool
 - vars_1: size of vars wrt. Rat
 - vars_2: size of vars wrt. List<Rat>
 - expr_1: size of expr wrt. Rat
 - expr_2: size of expr wrt. BoolExpr
UB for start(valVars_1,valVars_2,valVars_3,valVars_4,vars_1,vars_2,expr_1,expr_2) = pow(2,nat(vars_2))*c(maximize_failed)+pow(2,nat(vars_2))*pow(2,log(4,nat(expr_2/2)+3))+pow(2,nat(vars_2))*pow(2,log(4,3+nat(expr_2/2)))*nat(valVars_3+vars_2)


Method start terminates?: YES

UB for start(valVars_1,valVars_2,valVars_3,valVars_4,vars_1,vars_2,expr_1,expr_2) = pow(2,nat(vars_2))*c(maximize_failed)+pow(2,nat(vars_2))*pow(2,log(4,nat(expr_2/2)+3))+pow(2,nat(vars_2))*pow(2,log(4,3+nat(expr_2/2)))*nat(valVars_3+vars_2)


Method start terminates?: YES

UB for start(valVars_1,valVars_2,valVars_3,valVars_4,vars_1,vars_2,expr_1,expr_2) = pow(2,nat(vars_2))*c(maximize_failed)+pow(2,nat(vars_2))*pow(2,log(4,nat(expr_2/2)+3))+pow(2,nat(vars_2))*pow(2,log(4,3+nat(expr_2/2)))*nat(valVars_3+vars_2)

Warning: Ignored call to or/0 in equation case_5/6 
Warning: Ignored call to and_op/0 in equation case_5/6 

Preprocessing Cost Relations
=====================================

#### Computed strongly connected components 
0. recursive  : [case_4/2,concat/2]
1. recursive  : [assoc/5,case_0/5,case_1/8,case_2/7]
2. non_recursive  : [neg/1]
3. non_recursive  : [not/1]
4. recursive [non_tail,multiple] : [case_5/6,eval/6]
5. non_recursive  : [maxNorm/2]
6. recursive  : [aux/2,case_3/2]
7. non_recursive  : [rev/1]
8. recursive [non_tail,multiple] : [case_6/8,tableMake/8]
10. non_recursive  : [start/8]
* The entry case_6/8 is not a cutpoint so it becomes a new SCC 10
Warning: the following predicates are never called:[and_op/2,eq/2,geq/2,gt/2,leq/2,lt/2,neg/1,neq/2,or/2,start/0]

#### Obtained direct recursion through partial evaluation 
0. SCC is partially evaluated into concat/2
1. SCC is partially evaluated into assoc/5
2. SCC is partially evaluated into neg/1
3. SCC is completely evaluated into other SCCs
4. SCC is partially evaluated into eval/6
5. SCC is partially evaluated into maxNorm/2
6. SCC is partially evaluated into aux/2
7. SCC is completely evaluated into other SCCs
8. SCC is partially evaluated into tableMake/8
10. SCC is partially evaluated into case_6/8

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

### Specialization of cost equations concat/2 
* CE 8 is refined into CE [17] 
* CE 7 is refined into CE [18] 


#### Refined cost equations concat/2 
* CE 17: concat(A,B) = 5+ concat(C,B)
     [C>=0,B>=0,C+1=A] 
* CE 18: concat(A,B) = 2
     [B>=0,A=1] 

### Cost equations --> "Loop" of concat/2 
* CEs [18] --> Loop 17 
* CEs [17] --> Loop 18 

#### Loops of concat/2 
* Loop 17: concat(A,B) [B>=0,A=1] 
* Loop 18: concat(A,B)->  concat(A',B)
                  [A'>=0,B>=0,A'+1=A] 

### Ranking functions of CR concat(A,B) 
* RF of phase [18]: [A]

#### Partial ranking functions of CR concat(A,B) 
* Partial RF of phase [18]:
  - RF of loop [18:1]:
    A


### Resulting Chains:concat(A,B) 
* [[18],17]
* [17]


### Specialization of cost equations assoc/5 
* CE 14 is refined into CE [19] 
* CE 16 is refined into CE [20] 
* CE 15 is refined into CE [21] 


#### Refined cost equations assoc/5 
* CE 19: assoc(A,B,C,D,E) = 7
     [B>=A,E>=0,D>=1,C>=1] 
* CE 20: assoc(A,B,C,D,E) = 3
     [E=0,D=1,C=0] 
* CE 21: assoc(A,B,C,D,E) = 8+ assoc(A,F,G,H,I)
     [E>=I,C>=G,B>=F,I>=0,H>=0,G>=0,C>=1,H+1=D] 

### Cost equations --> "Loop" of assoc/5 
* CEs [21] --> Loop 19 
* CEs [19] --> Loop 20 
* CEs [20] --> Loop 21 

#### Loops of assoc/5 
* Loop 19: assoc(A,B,C,D,E)->  assoc(A,B',C',D',E')
                  [E>=E',C>=C',B>=B',E'>=0,D'>=0,C'>=0,C>=1,D'+1=D] 
* Loop 20: assoc(A,B,C,D,E) [B>=A,E>=0,D>=1,C>=1] 
* Loop 21: assoc(A,B,C,D,E) [E=0,D=1,C=0] 

### Ranking functions of CR assoc(A,B,C,D,E) 
* RF of phase [19]: [D]

#### Partial ranking functions of CR assoc(A,B,C,D,E) 
* Partial RF of phase [19]:
  - RF of loop [19:1]:
    D


### Resulting Chains:assoc(A,B,C,D,E) 
* [[19],21]
* [[19],20]
* [21]
* [20]


### Specialization of cost equations eval/6 
* CE 13 is refined into CE [22] 
* CE 12 is refined into CE [23] 
* CE 11 is refined into CE [24,25,26,27] 


#### Refined cost equations eval/6 
* CE 22: eval(A,B,C,D,E,F) = 8+ eval(A,B,C,D,G,H)+ eval(A,B,C,D,I,J)
     [E>=I,E>=G,D>=0,C>=1,B>=0,J=1,H=1,F=3] 
* CE 23: eval(A,B,C,D,E,F) = 7+ eval(A,B,C,D,G,H)+ eval(A,B,C,D,I,J)
     [E>=I,E>=G,D>=0,C>=1,B>=0,J=1,H=1,F=3] 
* CE 24: eval(A,B,C,D,E,F) = 3+ assoc(E,A,B,C,D):[[19],21]
     [D>=0,C>=2,B>=1,F=1] 
* CE 25: eval(A,B,C,D,E,F) = 3+ assoc(E,A,B,C,D):[[19],20]
     [A>=E,D>=0,C>=2,B>=1,F=1] 
* CE 26: eval(A,B,C,D,E,F) = 3+ assoc(E,A,G,H,I):[21]
     [I=0,H=1,G=0,F=1,D=0,C=1,B=0] 
* CE 27: eval(A,B,C,D,E,F) = 3+ assoc(E,A,B,C,D):[20]
     [A>=E,D>=0,C>=1,B>=1,F=1] 

### Cost equations --> "Loop" of eval/6 
* CEs [25] --> Loop 22 
* CEs [24] --> Loop 23 
* CEs [27] --> Loop 24 
* CEs [26] --> Loop 25 
* CEs [23] --> Loop 26 
* CEs [22] --> Loop 27 

#### Loops of eval/6 
* Loop 22: eval(A,B,C,D,E,F) [A>=E,D>=0,C>=2,B>=1,F=1] 
* Loop 23: eval(A,B,C,D,E,F) [D>=0,C>=2,B>=1,F=1] 
* Loop 24: eval(A,B,C,D,E,F) [A>=E,D>=0,C>=1,B>=1,F=1] 
* Loop 25: eval(A,B,C,D,E,F) [F=1,D=0,C=1,B=0] 
* Loop 26: eval(A,B,C,D,E,F)->  eval(A,B,C,D,E',F')  eval(A,B,C,D,E'2,F'2)
                  [E>=E'2,E>=E',D>=0,C>=1,B>=0,F'2=1,F'=1,F=3] 
* Loop 27: eval(A,B,C,D,E,F)->  eval(A,B,C,D,E',F')  eval(A,B,C,D,E'2,F'2)
                  [E>=E'2,E>=E',D>=0,C>=1,B>=0,F'2=1,F'=1,F=3] 

### Ranking functions of CR eval(A,B,C,D,E,F) 

#### Partial ranking functions of CR eval(A,B,C,D,E,F) 


### Resulting Chains:eval(A,B,C,D,E,F) 
* [multiple(27,[[25],[24],[23],[22]])]
* [multiple(26,[[25],[24],[23],[22]])]
* [25]
* [24]
* [23]
* [22]


### Specialization of cost equations maxNorm/2 
* CE 4 is refined into CE [28] 
* CE 3 is refined into CE [29] 


#### Refined cost equations maxNorm/2 
* CE 28: maxNorm(A,B) = 0
     [B=0,A=1] 
* CE 29: maxNorm(A,B) = 0
     [B>=1,A=1] 

### Cost equations --> "Loop" of maxNorm/2 
* CEs [29] --> Loop 28 
* CEs [28] --> Loop 29 

#### Loops of maxNorm/2 
* Loop 28: maxNorm(A,B) [B>=1,A=1] 
* Loop 29: maxNorm(A,B) [B=0,A=1] 

### Ranking functions of CR maxNorm(A,B) 

#### Partial ranking functions of CR maxNorm(A,B) 


### Resulting Chains:maxNorm(A,B) 
* [29]
* [28]


### Specialization of cost equations aux/2 
* CE 10 is refined into CE [30] 
* CE 9 is refined into CE [31] 


#### Refined cost equations aux/2 
* CE 30: aux(A,B) = 5+ aux(C,D)
     [D>=0,A>=1,A+1=C,D+1=B] 
* CE 31: aux(A,B) = 2
     [A>=1,B=1] 

### Cost equations --> "Loop" of aux/2 
* CEs [31] --> Loop 30 
* CEs [30] --> Loop 31 

#### Loops of aux/2 
* Loop 30: aux(A,B) [A>=1,B=1] 
* Loop 31: aux(A,B)->  aux(A',B')
                  [B'>=0,A>=1,A+1=A',B'+1=B] 

### Ranking functions of CR aux(A,B) 
* RF of phase [31]: [B]

#### Partial ranking functions of CR aux(A,B) 
* Partial RF of phase [31]:
  - RF of loop [31:1]:
    B


### Resulting Chains:aux(A,B) 
* [[31],30]
* [30]


### Specialization of cost equations tableMake/8 
* CE 6 is refined into CE [32,33,34,35,36] 
* CE 5 is refined into CE [37,38,39,40] 


#### Refined cost equations tableMake/8 
* CE 32: tableMake(A,B,C,D,E,F,G,H) = 9+ aux(I,C):[[31],30]+ eval(A,B,C,D,G,J):[24]
     [A>=G,D>=0,C>=2,B>=1,J=1,I=1,H=1,F=1] 
* CE 33: tableMake(A,B,C,D,E,F,G,H) = 9+ aux(I,C):[[31],30]+ eval(A,B,C,D,G,J):[23]
     [D>=0,C>=2,B>=1,J=1,I=1,H=1,F=1] 
* CE 34: tableMake(A,B,C,D,E,F,G,H) = 9+ aux(I,C):[[31],30]+ eval(A,B,C,D,G,J):[22]
     [A>=G,D>=0,C>=2,B>=1,J=1,I=1,H=1,F=1] 
* CE 35: tableMake(A,B,C,D,E,F,G,H) = 9+ aux(I,J):[30]+ eval(A,K,L,M,G,N):[25]
     [N=1,M=0,L=1,K=0,J=1,I=1,H=1,F=1,D=0,C=1,B=0] 
* CE 36: tableMake(A,B,C,D,E,F,G,H) = 9+ aux(I,J):[30]+ eval(A,B,K,D,G,L):[24]
     [A>=G,D>=0,B>=1,L=1,K=1,J=1,I=1,H=1,F=1,C=1] 
* CE 37: tableMake(A,B,C,D,E,F,G,H) = 12+ maxNorm(I,J):[29]+ tableMake(K,L,M,N,O,P,G,Q)+ maxNorm(R,S):[29]+ tableMake(T,U,M,V,O,P,G,W)+ concat(X,Y):[[18],17]
     [E>=O,V>=D,N>=D,T>=A,K>=A,U>=0,P>=0,N>=1,M>=2,L>=0,Y>=0,X>=2,D>=0,P+1=F,M=C+1,W=1,Q=1,S=0,R=1,J=0,I=1,H=1,B=0] 
* CE 38: tableMake(A,B,C,D,E,F,G,H) = 12+ maxNorm(I,J):[29]+ tableMake(K,L,M,N,O,P,G,Q)+ maxNorm(R,S):[29]+ tableMake(T,U,M,V,O,P,G,W)+ concat(X,Y):[17]
     [E>=O,V>=D,N>=D,T>=A,K>=A,U>=0,P>=0,N>=1,M>=2,L>=0,Y>=0,D>=0,P+1=F,M=C+1,W=1,Q=1,X=1,S=0,R=1,J=0,I=1,H=1,B=0] 
* CE 39: tableMake(A,B,C,D,E,F,G,H) = 12+ maxNorm(I,B):[28]+ tableMake(J,K,L,M,N,O,G,P)+ maxNorm(Q,B):[28]+ tableMake(R,S,L,T,N,O,G,U)+ concat(V,W):[[18],17]
     [E>=N,T>=D,M>=D,R>=A,J>=A,S>=0,O>=0,M>=1,L>=2,K>=0,W>=0,V>=2,B>=1,D>=0,O+1=F,L=C+1,U=1,P=1,Q=1,I=1,H=1] 
* CE 40: tableMake(A,B,C,D,E,F,G,H) = 12+ maxNorm(I,B):[28]+ tableMake(J,K,L,M,N,O,G,P)+ maxNorm(Q,B):[28]+ tableMake(R,S,L,T,N,O,G,U)+ concat(V,W):[17]
     [E>=N,T>=D,M>=D,R>=A,J>=A,S>=0,O>=0,M>=1,L>=2,K>=0,W>=0,B>=1,D>=0,O+1=F,L=C+1,U=1,P=1,V=1,Q=1,I=1,H=1] 

### Cost equations --> "Loop" of tableMake/8 
* CEs [40] --> Loop 32 
* CEs [39] --> Loop 33 
* CEs [38] --> Loop 34 
* CEs [37] --> Loop 35 
* CEs [34] --> Loop 36 
* CEs [32] --> Loop 37 
* CEs [33] --> Loop 38 
* CEs [36] --> Loop 39 
* CEs [35] --> Loop 40 

#### Loops of tableMake/8 
* Loop 32: tableMake(A,B,C,D,E,F,G,H)->  tableMake(A',B',C',D',E',F',G,H')  tableMake(A'2,B'2,C',C'2,E',F',G,D'2)
                  [E>=E',C'2>=D,D'>=D,A'2>=A,A'>=A,B'2>=0,F'>=0,D'>=1,C'>=2,B'>=0,D>=0,B>=1,F'+1=F,C'=C+1,D'2=1,H'=1,H=1] 
* Loop 33: tableMake(A,B,C,D,E,F,G,H)->  tableMake(A',B',C',D',E',F',G,H')  tableMake(A'2,B'2,C',C'2,E',F',G,D'2)
                  [E>=E',C'2>=D,D'>=D,A'2>=A,A'>=A,B'2>=0,F'>=0,D'>=1,C'>=2,B'>=0,D>=0,B>=1,F'+1=F,C'=C+1,D'2=1,H'=1,H=1] 
* Loop 34: tableMake(A,B,C,D,E,F,G,H)->  tableMake(A',B',C',D',E',F',G,H')  tableMake(A'2,B'2,C',C'2,E',F',G,D'2)
                  [E>=E',C'2>=D,D'>=D,A'2>=A,A'>=A,B'2>=0,F'>=0,D'>=1,C'>=2,B'>=0,D>=0,F'+1=F,C'=C+1,D'2=1,H'=1,H=1,B=0] 
* Loop 35: tableMake(A,B,C,D,E,F,G,H)->  tableMake(A',B',C',D',E',F',G,H')  tableMake(A'2,B'2,C',C'2,E',F',G,D'2)
                  [E>=E',C'2>=D,D'>=D,A'2>=A,A'>=A,B'2>=0,F'>=0,D'>=1,C'>=2,B'>=0,D>=0,F'+1=F,C'=C+1,D'2=1,H'=1,H=1,B=0] 
* Loop 36: tableMake(A,B,C,D,E,F,G,H) [A>=G,D>=0,C>=2,B>=1,H=1,F=1] 
* Loop 37: tableMake(A,B,C,D,E,F,G,H) [A>=G,D>=0,C>=2,B>=1,H=1,F=1] 
* Loop 38: tableMake(A,B,C,D,E,F,G,H) [D>=0,C>=2,B>=1,H=1,F=1] 
* Loop 39: tableMake(A,B,C,D,E,F,G,H) [A>=G,D>=0,B>=1,H=1,F=1,C=1] 
* Loop 40: tableMake(A,B,C,D,E,F,G,H) [H=1,F=1,D=0,C=1,B=0] 

### Ranking functions of CR tableMake(A,B,C,D,E,F,G,H) 
* RF of phase [32,33,34,35]: [F]

#### Partial ranking functions of CR tableMake(A,B,C,D,E,F,G,H) 
* Partial RF of phase [32,33,34,35]:
  - RF of loop [32:1,32:2,33:1,33:2,34:1,34:2,35:1,35:2]:
    F


### Resulting Chains:tableMake(A,B,C,D,E,F,G,H) 
* [40]
* [39]
* [38]
* [37]
* [36]
* [multiple([32,33,34,35],[[38],[37],[36]])]


### Specialization of cost equations case_6/8 
* CE 1 is refined into CE [41,42,43,44,45,46,47,48,49,50,51,52,53,54,55,56,57,58,59,60,61,62,63,64,65,66,67,68,69,70,71,72,73,74,75,76,77,78,79,80,81,82,83,84,85,86,87,88] 
* CE 2 is refined into CE [89,90,91,92,93,94,95,96,97] 


#### Refined cost equations case_6/8 
* CE 41: case_6(A,B,C,D,E,F,G,H) = 11+ maxNorm(I,J):[29]+ tableMake(K,L,M,N,O,P,G,Q):[39]+ maxNorm(R,S):[29]+ tableMake(T,U,V,W,O,X,G,Y):[40]+ concat(Z,A1):[[18],17]
     [K>=G,E>=O,T>=A,K>=A,A1>=0,Z>=2,N>=1,L>=1,Y=1,X=1,W=0,V=1,U=0,S=0,R=1,Q=1,P=1,M=1,J=0,I=1,H=1,F=2,D=0,C=0,B=0] 
* CE 42: case_6(A,B,C,D,E,F,G,H) = 11+ maxNorm(I,J):[29]+ tableMake(K,L,M,N,O,P,G,Q):[39]+ maxNorm(R,S):[29]+ tableMake(T,U,V,W,O,X,G,Y):[40]+ concat(Z,A1):[17]
     [K>=G,E>=O,T>=A,K>=A,A1>=0,N>=1,L>=1,Z=1,Y=1,X=1,W=0,V=1,U=0,S=0,R=1,Q=1,P=1,M=1,J=0,I=1,H=1,F=2,D=0,C=0,B=0] 
* CE 43: case_6(A,B,C,D,E,F,G,H) = 11+ maxNorm(I,J):[29]+ tableMake(K,L,M,N,O,P,G,Q):[39]+ maxNorm(R,S):[29]+ tableMake(T,U,V,W,O,X,G,Y):[39]+ concat(Z,A1):[[18],17]
     [T>=G,K>=G,E>=O,W>=D,N>=D,T>=A,K>=A,A1>=0,Z>=2,U>=1,N>=1,L>=1,D>=0,Y=1,X=1,V=1,S=0,R=1,Q=1,P=1,M=1,J=0,I=1,H=1,F=2,C=0,B=0] 
* CE 44: case_6(A,B,C,D,E,F,G,H) = 11+ maxNorm(I,J):[29]+ tableMake(K,L,M,N,O,P,G,Q):[39]+ maxNorm(R,S):[29]+ tableMake(T,U,V,W,O,X,G,Y):[39]+ concat(Z,A1):[17]
     [T>=G,K>=G,E>=O,W>=D,N>=D,T>=A,K>=A,A1>=0,U>=1,N>=1,L>=1,D>=0,Z=1,Y=1,X=1,V=1,S=0,R=1,Q=1,P=1,M=1,J=0,I=1,H=1,F=2,C=0,B=0] 
* CE 45: case_6(A,B,C,D,E,F,G,H) = 11+ maxNorm(I,J):[29]+ tableMake(K,L,M,N,O,P,G,Q):[38]+ maxNorm(R,S):[29]+ tableMake(T,U,M,V,O,W,G,X):[38]+ concat(Y,Z):[[18],17]
     [E>=O,V>=D,N>=D,T>=A,K>=A,Z>=0,Y>=2,M>=2,U>=1,N>=1,L>=1,D>=0,M=C+1,X=1,W=1,S=0,R=1,Q=1,P=1,J=0,I=1,H=1,F=2,B=0] 
* CE 46: case_6(A,B,C,D,E,F,G,H) = 11+ maxNorm(I,J):[29]+ tableMake(K,L,M,N,O,P,G,Q):[38]+ maxNorm(R,S):[29]+ tableMake(T,U,M,V,O,W,G,X):[38]+ concat(Y,Z):[17]
     [E>=O,V>=D,N>=D,T>=A,K>=A,Z>=0,M>=2,U>=1,N>=1,L>=1,D>=0,M=C+1,Y=1,X=1,W=1,S=0,R=1,Q=1,P=1,J=0,I=1,H=1,F=2,B=0] 
* CE 47: case_6(A,B,C,D,E,F,G,H) = 11+ maxNorm(I,J):[29]+ tableMake(K,L,M,N,O,P,G,Q):[38]+ maxNorm(R,S):[29]+ tableMake(T,U,M,V,O,W,G,X):[37]+ concat(Y,Z):[[18],17]
     [T>=G,E>=O,V>=D,N>=D,T>=A,K>=A,Z>=0,Y>=2,M>=2,U>=1,N>=1,L>=1,D>=0,M=C+1,X=1,W=1,S=0,R=1,Q=1,P=1,J=0,I=1,H=1,F=2,B=0] 
* CE 48: case_6(A,B,C,D,E,F,G,H) = 11+ maxNorm(I,J):[29]+ tableMake(K,L,M,N,O,P,G,Q):[38]+ maxNorm(R,S):[29]+ tableMake(T,U,M,V,O,W,G,X):[37]+ concat(Y,Z):[17]
     [T>=G,E>=O,V>=D,N>=D,T>=A,K>=A,Z>=0,M>=2,U>=1,N>=1,L>=1,D>=0,M=C+1,Y=1,X=1,W=1,S=0,R=1,Q=1,P=1,J=0,I=1,H=1,F=2,B=0] 
* CE 49: case_6(A,B,C,D,E,F,G,H) = 11+ maxNorm(I,J):[29]+ tableMake(K,L,M,N,O,P,G,Q):[38]+ maxNorm(R,S):[29]+ tableMake(T,U,M,V,O,W,G,X):[36]+ concat(Y,Z):[[18],17]
     [T>=G,E>=O,V>=D,N>=D,T>=A,K>=A,Z>=0,Y>=2,M>=2,U>=1,N>=1,L>=1,D>=0,M=C+1,X=1,W=1,S=0,R=1,Q=1,P=1,J=0,I=1,H=1,F=2,B=0] 
* CE 50: case_6(A,B,C,D,E,F,G,H) = 11+ maxNorm(I,J):[29]+ tableMake(K,L,M,N,O,P,G,Q):[38]+ maxNorm(R,S):[29]+ tableMake(T,U,M,V,O,W,G,X):[36]+ concat(Y,Z):[17]
     [T>=G,E>=O,V>=D,N>=D,T>=A,K>=A,Z>=0,M>=2,U>=1,N>=1,L>=1,D>=0,M=C+1,Y=1,X=1,W=1,S=0,R=1,Q=1,P=1,J=0,I=1,H=1,F=2,B=0] 
* CE 51: case_6(A,B,C,D,E,F,G,H) = 11+ maxNorm(I,J):[29]+ tableMake(K,L,M,N,O,P,G,Q):[37]+ maxNorm(R,S):[29]+ tableMake(T,U,M,V,O,W,G,X):[38]+ concat(Y,Z):[[18],17]
     [K>=G,E>=O,V>=D,N>=D,T>=A,K>=A,Z>=0,Y>=2,M>=2,U>=1,N>=1,L>=1,D>=0,M=C+1,X=1,W=1,S=0,R=1,Q=1,P=1,J=0,I=1,H=1,F=2,B=0] 
* CE 52: case_6(A,B,C,D,E,F,G,H) = 11+ maxNorm(I,J):[29]+ tableMake(K,L,M,N,O,P,G,Q):[37]+ maxNorm(R,S):[29]+ tableMake(T,U,M,V,O,W,G,X):[38]+ concat(Y,Z):[17]
     [K>=G,E>=O,V>=D,N>=D,T>=A,K>=A,Z>=0,M>=2,U>=1,N>=1,L>=1,D>=0,M=C+1,Y=1,X=1,W=1,S=0,R=1,Q=1,P=1,J=0,I=1,H=1,F=2,B=0] 
* CE 53: case_6(A,B,C,D,E,F,G,H) = 11+ maxNorm(I,J):[29]+ tableMake(K,L,M,N,O,P,G,Q):[37]+ maxNorm(R,S):[29]+ tableMake(T,U,M,V,O,W,G,X):[37]+ concat(Y,Z):[[18],17]
     [T>=G,K>=G,E>=O,V>=D,N>=D,T>=A,K>=A,Z>=0,Y>=2,M>=2,U>=1,N>=1,L>=1,D>=0,M=C+1,X=1,W=1,S=0,R=1,Q=1,P=1,J=0,I=1,H=1,F=2,B=0] 
* CE 54: case_6(A,B,C,D,E,F,G,H) = 11+ maxNorm(I,J):[29]+ tableMake(K,L,M,N,O,P,G,Q):[37]+ maxNorm(R,S):[29]+ tableMake(T,U,M,V,O,W,G,X):[37]+ concat(Y,Z):[17]
     [T>=G,K>=G,E>=O,V>=D,N>=D,T>=A,K>=A,Z>=0,M>=2,U>=1,N>=1,L>=1,D>=0,M=C+1,Y=1,X=1,W=1,S=0,R=1,Q=1,P=1,J=0,I=1,H=1,F=2,B=0] 
* CE 55: case_6(A,B,C,D,E,F,G,H) = 11+ maxNorm(I,J):[29]+ tableMake(K,L,M,N,O,P,G,Q):[37]+ maxNorm(R,S):[29]+ tableMake(T,U,M,V,O,W,G,X):[36]+ concat(Y,Z):[[18],17]
     [T>=G,K>=G,E>=O,V>=D,N>=D,T>=A,K>=A,Z>=0,Y>=2,M>=2,U>=1,N>=1,L>=1,D>=0,M=C+1,X=1,W=1,S=0,R=1,Q=1,P=1,J=0,I=1,H=1,F=2,B=0] 
* CE 56: case_6(A,B,C,D,E,F,G,H) = 11+ maxNorm(I,J):[29]+ tableMake(K,L,M,N,O,P,G,Q):[37]+ maxNorm(R,S):[29]+ tableMake(T,U,M,V,O,W,G,X):[36]+ concat(Y,Z):[17]
     [T>=G,K>=G,E>=O,V>=D,N>=D,T>=A,K>=A,Z>=0,M>=2,U>=1,N>=1,L>=1,D>=0,M=C+1,Y=1,X=1,W=1,S=0,R=1,Q=1,P=1,J=0,I=1,H=1,F=2,B=0] 
* CE 57: case_6(A,B,C,D,E,F,G,H) = 11+ maxNorm(I,J):[29]+ tableMake(K,L,M,N,O,P,G,Q):[36]+ maxNorm(R,S):[29]+ tableMake(T,U,M,V,O,W,G,X):[38]+ concat(Y,Z):[[18],17]
     [K>=G,E>=O,V>=D,N>=D,T>=A,K>=A,Z>=0,Y>=2,M>=2,U>=1,N>=1,L>=1,D>=0,M=C+1,X=1,W=1,S=0,R=1,Q=1,P=1,J=0,I=1,H=1,F=2,B=0] 
* CE 58: case_6(A,B,C,D,E,F,G,H) = 11+ maxNorm(I,J):[29]+ tableMake(K,L,M,N,O,P,G,Q):[36]+ maxNorm(R,S):[29]+ tableMake(T,U,M,V,O,W,G,X):[38]+ concat(Y,Z):[17]
     [K>=G,E>=O,V>=D,N>=D,T>=A,K>=A,Z>=0,M>=2,U>=1,N>=1,L>=1,D>=0,M=C+1,Y=1,X=1,W=1,S=0,R=1,Q=1,P=1,J=0,I=1,H=1,F=2,B=0] 
* CE 59: case_6(A,B,C,D,E,F,G,H) = 11+ maxNorm(I,J):[29]+ tableMake(K,L,M,N,O,P,G,Q):[36]+ maxNorm(R,S):[29]+ tableMake(T,U,M,V,O,W,G,X):[37]+ concat(Y,Z):[[18],17]
     [T>=G,K>=G,E>=O,V>=D,N>=D,T>=A,K>=A,Z>=0,Y>=2,M>=2,U>=1,N>=1,L>=1,D>=0,M=C+1,X=1,W=1,S=0,R=1,Q=1,P=1,J=0,I=1,H=1,F=2,B=0] 
* CE 60: case_6(A,B,C,D,E,F,G,H) = 11+ maxNorm(I,J):[29]+ tableMake(K,L,M,N,O,P,G,Q):[36]+ maxNorm(R,S):[29]+ tableMake(T,U,M,V,O,W,G,X):[37]+ concat(Y,Z):[17]
     [T>=G,K>=G,E>=O,V>=D,N>=D,T>=A,K>=A,Z>=0,M>=2,U>=1,N>=1,L>=1,D>=0,M=C+1,Y=1,X=1,W=1,S=0,R=1,Q=1,P=1,J=0,I=1,H=1,F=2,B=0] 
* CE 61: case_6(A,B,C,D,E,F,G,H) = 11+ maxNorm(I,J):[29]+ tableMake(K,L,M,N,O,P,G,Q):[36]+ maxNorm(R,S):[29]+ tableMake(T,U,M,V,O,W,G,X):[36]+ concat(Y,Z):[[18],17]
     [T>=G,K>=G,E>=O,V>=D,N>=D,T>=A,K>=A,Z>=0,Y>=2,M>=2,U>=1,N>=1,L>=1,D>=0,M=C+1,X=1,W=1,S=0,R=1,Q=1,P=1,J=0,I=1,H=1,F=2,B=0] 
* CE 62: case_6(A,B,C,D,E,F,G,H) = 11+ maxNorm(I,J):[29]+ tableMake(K,L,M,N,O,P,G,Q):[36]+ maxNorm(R,S):[29]+ tableMake(T,U,M,V,O,W,G,X):[36]+ concat(Y,Z):[17]
     [T>=G,K>=G,E>=O,V>=D,N>=D,T>=A,K>=A,Z>=0,M>=2,U>=1,N>=1,L>=1,D>=0,M=C+1,Y=1,X=1,W=1,S=0,R=1,Q=1,P=1,J=0,I=1,H=1,F=2,B=0] 
* CE 63: case_6(A,B,C,D,E,F,G,H) = 11+ maxNorm(I,J):[29]+ tableMake(K,L,M,N,O,P,G,Q):[multiple([32,33,34,35],[[38],[37],[36]])]+ maxNorm(R,S):[29]+ tableMake(T,U,M,V,O,P,G,W):[multiple([32,33,34,35],[[38],[37],[36]])]+ concat(X,Y):[[18],17]
     [E>=O,V>=D,N>=D,T>=A,K>=A,Y>=0,X>=2,P>=2,M>=1,U>=0,N>=1,L>=0,D>=0,P+1=F,M=C+1,W=1,S=0,R=1,Q=1,J=0,I=1,H=1,B=0] 
* CE 64: case_6(A,B,C,D,E,F,G,H) = 11+ maxNorm(I,J):[29]+ tableMake(K,L,M,N,O,P,G,Q):[multiple([32,33,34,35],[[38],[37],[36]])]+ maxNorm(R,S):[29]+ tableMake(T,U,M,V,O,P,G,W):[multiple([32,33,34,35],[[38],[37],[36]])]+ concat(X,Y):[17]
     [E>=O,V>=D,N>=D,T>=A,K>=A,Y>=0,P>=2,M>=1,U>=0,N>=1,L>=0,D>=0,P+1=F,M=C+1,X=1,W=1,S=0,R=1,Q=1,J=0,I=1,H=1,B=0] 
* CE 65: case_6(A,B,C,D,E,F,G,H) = 11+ maxNorm(I,B):[28]+ tableMake(J,K,L,M,N,O,G,P):[39]+ maxNorm(Q,B):[28]+ tableMake(R,S,T,U,N,V,G,W):[40]+ concat(X,Y):[[18],17]
     [J>=G,E>=N,R>=A,J>=A,Y>=0,X>=2,B>=1,M>=1,K>=1,W=1,V=1,U=0,T=1,S=0,Q=1,P=1,O=1,L=1,I=1,H=1,F=2,D=0,C=0] 
* CE 66: case_6(A,B,C,D,E,F,G,H) = 11+ maxNorm(I,B):[28]+ tableMake(J,K,L,M,N,O,G,P):[39]+ maxNorm(Q,B):[28]+ tableMake(R,S,T,U,N,V,G,W):[40]+ concat(X,Y):[17]
     [J>=G,E>=N,R>=A,J>=A,Y>=0,B>=1,M>=1,K>=1,X=1,W=1,V=1,U=0,T=1,S=0,Q=1,P=1,O=1,L=1,I=1,H=1,F=2,D=0,C=0] 
* CE 67: case_6(A,B,C,D,E,F,G,H) = 11+ maxNorm(I,B):[28]+ tableMake(J,K,L,M,N,O,G,P):[39]+ maxNorm(Q,B):[28]+ tableMake(R,S,T,U,N,V,G,W):[39]+ concat(X,Y):[[18],17]
     [R>=G,J>=G,E>=N,U>=D,M>=D,R>=A,J>=A,Y>=0,X>=2,S>=1,B>=1,M>=1,K>=1,D>=0,W=1,V=1,T=1,Q=1,P=1,O=1,L=1,I=1,H=1,F=2,C=0] 
* CE 68: case_6(A,B,C,D,E,F,G,H) = 11+ maxNorm(I,B):[28]+ tableMake(J,K,L,M,N,O,G,P):[39]+ maxNorm(Q,B):[28]+ tableMake(R,S,T,U,N,V,G,W):[39]+ concat(X,Y):[17]
     [R>=G,J>=G,E>=N,U>=D,M>=D,R>=A,J>=A,Y>=0,S>=1,B>=1,M>=1,K>=1,D>=0,X=1,W=1,V=1,T=1,Q=1,P=1,O=1,L=1,I=1,H=1,F=2,C=0] 
* CE 69: case_6(A,B,C,D,E,F,G,H) = 11+ maxNorm(I,B):[28]+ tableMake(J,K,L,M,N,O,G,P):[38]+ maxNorm(Q,B):[28]+ tableMake(R,S,L,T,N,U,G,V):[38]+ concat(W,X):[[18],17]
     [E>=N,T>=D,M>=D,R>=A,J>=A,X>=0,W>=2,L>=2,S>=1,B>=1,M>=1,K>=1,D>=0,L=C+1,V=1,U=1,Q=1,P=1,O=1,I=1,H=1,F=2] 
* CE 70: case_6(A,B,C,D,E,F,G,H) = 11+ maxNorm(I,B):[28]+ tableMake(J,K,L,M,N,O,G,P):[38]+ maxNorm(Q,B):[28]+ tableMake(R,S,L,T,N,U,G,V):[38]+ concat(W,X):[17]
     [E>=N,T>=D,M>=D,R>=A,J>=A,X>=0,L>=2,S>=1,B>=1,M>=1,K>=1,D>=0,L=C+1,W=1,V=1,U=1,Q=1,P=1,O=1,I=1,H=1,F=2] 
* CE 71: case_6(A,B,C,D,E,F,G,H) = 11+ maxNorm(I,B):[28]+ tableMake(J,K,L,M,N,O,G,P):[38]+ maxNorm(Q,B):[28]+ tableMake(R,S,L,T,N,U,G,V):[37]+ concat(W,X):[[18],17]
     [R>=G,E>=N,T>=D,M>=D,R>=A,J>=A,X>=0,W>=2,L>=2,S>=1,B>=1,M>=1,K>=1,D>=0,L=C+1,V=1,U=1,Q=1,P=1,O=1,I=1,H=1,F=2] 
* CE 72: case_6(A,B,C,D,E,F,G,H) = 11+ maxNorm(I,B):[28]+ tableMake(J,K,L,M,N,O,G,P):[38]+ maxNorm(Q,B):[28]+ tableMake(R,S,L,T,N,U,G,V):[37]+ concat(W,X):[17]
     [R>=G,E>=N,T>=D,M>=D,R>=A,J>=A,X>=0,L>=2,S>=1,B>=1,M>=1,K>=1,D>=0,L=C+1,W=1,V=1,U=1,Q=1,P=1,O=1,I=1,H=1,F=2] 
* CE 73: case_6(A,B,C,D,E,F,G,H) = 11+ maxNorm(I,B):[28]+ tableMake(J,K,L,M,N,O,G,P):[38]+ maxNorm(Q,B):[28]+ tableMake(R,S,L,T,N,U,G,V):[36]+ concat(W,X):[[18],17]
     [R>=G,E>=N,T>=D,M>=D,R>=A,J>=A,X>=0,W>=2,L>=2,S>=1,B>=1,M>=1,K>=1,D>=0,L=C+1,V=1,U=1,Q=1,P=1,O=1,I=1,H=1,F=2] 
* CE 74: case_6(A,B,C,D,E,F,G,H) = 11+ maxNorm(I,B):[28]+ tableMake(J,K,L,M,N,O,G,P):[38]+ maxNorm(Q,B):[28]+ tableMake(R,S,L,T,N,U,G,V):[36]+ concat(W,X):[17]
     [R>=G,E>=N,T>=D,M>=D,R>=A,J>=A,X>=0,L>=2,S>=1,B>=1,M>=1,K>=1,D>=0,L=C+1,W=1,V=1,U=1,Q=1,P=1,O=1,I=1,H=1,F=2] 
* CE 75: case_6(A,B,C,D,E,F,G,H) = 11+ maxNorm(I,B):[28]+ tableMake(J,K,L,M,N,O,G,P):[37]+ maxNorm(Q,B):[28]+ tableMake(R,S,L,T,N,U,G,V):[38]+ concat(W,X):[[18],17]
     [J>=G,E>=N,T>=D,M>=D,R>=A,J>=A,X>=0,W>=2,L>=2,S>=1,B>=1,M>=1,K>=1,D>=0,L=C+1,V=1,U=1,Q=1,P=1,O=1,I=1,H=1,F=2] 
* CE 76: case_6(A,B,C,D,E,F,G,H) = 11+ maxNorm(I,B):[28]+ tableMake(J,K,L,M,N,O,G,P):[37]+ maxNorm(Q,B):[28]+ tableMake(R,S,L,T,N,U,G,V):[38]+ concat(W,X):[17]
     [J>=G,E>=N,T>=D,M>=D,R>=A,J>=A,X>=0,L>=2,S>=1,B>=1,M>=1,K>=1,D>=0,L=C+1,W=1,V=1,U=1,Q=1,P=1,O=1,I=1,H=1,F=2] 
* CE 77: case_6(A,B,C,D,E,F,G,H) = 11+ maxNorm(I,B):[28]+ tableMake(J,K,L,M,N,O,G,P):[37]+ maxNorm(Q,B):[28]+ tableMake(R,S,L,T,N,U,G,V):[37]+ concat(W,X):[[18],17]
     [R>=G,J>=G,E>=N,T>=D,M>=D,R>=A,J>=A,X>=0,W>=2,L>=2,S>=1,B>=1,M>=1,K>=1,D>=0,L=C+1,V=1,U=1,Q=1,P=1,O=1,I=1,H=1,F=2] 
* CE 78: case_6(A,B,C,D,E,F,G,H) = 11+ maxNorm(I,B):[28]+ tableMake(J,K,L,M,N,O,G,P):[37]+ maxNorm(Q,B):[28]+ tableMake(R,S,L,T,N,U,G,V):[37]+ concat(W,X):[17]
     [R>=G,J>=G,E>=N,T>=D,M>=D,R>=A,J>=A,X>=0,L>=2,S>=1,B>=1,M>=1,K>=1,D>=0,L=C+1,W=1,V=1,U=1,Q=1,P=1,O=1,I=1,H=1,F=2] 
* CE 79: case_6(A,B,C,D,E,F,G,H) = 11+ maxNorm(I,B):[28]+ tableMake(J,K,L,M,N,O,G,P):[37]+ maxNorm(Q,B):[28]+ tableMake(R,S,L,T,N,U,G,V):[36]+ concat(W,X):[[18],17]
     [R>=G,J>=G,E>=N,T>=D,M>=D,R>=A,J>=A,X>=0,W>=2,L>=2,S>=1,B>=1,M>=1,K>=1,D>=0,L=C+1,V=1,U=1,Q=1,P=1,O=1,I=1,H=1,F=2] 
* CE 80: case_6(A,B,C,D,E,F,G,H) = 11+ maxNorm(I,B):[28]+ tableMake(J,K,L,M,N,O,G,P):[37]+ maxNorm(Q,B):[28]+ tableMake(R,S,L,T,N,U,G,V):[36]+ concat(W,X):[17]
     [R>=G,J>=G,E>=N,T>=D,M>=D,R>=A,J>=A,X>=0,L>=2,S>=1,B>=1,M>=1,K>=1,D>=0,L=C+1,W=1,V=1,U=1,Q=1,P=1,O=1,I=1,H=1,F=2] 
* CE 81: case_6(A,B,C,D,E,F,G,H) = 11+ maxNorm(I,B):[28]+ tableMake(J,K,L,M,N,O,G,P):[36]+ maxNorm(Q,B):[28]+ tableMake(R,S,L,T,N,U,G,V):[38]+ concat(W,X):[[18],17]
     [J>=G,E>=N,T>=D,M>=D,R>=A,J>=A,X>=0,W>=2,L>=2,S>=1,B>=1,M>=1,K>=1,D>=0,L=C+1,V=1,U=1,Q=1,P=1,O=1,I=1,H=1,F=2] 
* CE 82: case_6(A,B,C,D,E,F,G,H) = 11+ maxNorm(I,B):[28]+ tableMake(J,K,L,M,N,O,G,P):[36]+ maxNorm(Q,B):[28]+ tableMake(R,S,L,T,N,U,G,V):[38]+ concat(W,X):[17]
     [J>=G,E>=N,T>=D,M>=D,R>=A,J>=A,X>=0,L>=2,S>=1,B>=1,M>=1,K>=1,D>=0,L=C+1,W=1,V=1,U=1,Q=1,P=1,O=1,I=1,H=1,F=2] 
* CE 83: case_6(A,B,C,D,E,F,G,H) = 11+ maxNorm(I,B):[28]+ tableMake(J,K,L,M,N,O,G,P):[36]+ maxNorm(Q,B):[28]+ tableMake(R,S,L,T,N,U,G,V):[37]+ concat(W,X):[[18],17]
     [R>=G,J>=G,E>=N,T>=D,M>=D,R>=A,J>=A,X>=0,W>=2,L>=2,S>=1,B>=1,M>=1,K>=1,D>=0,L=C+1,V=1,U=1,Q=1,P=1,O=1,I=1,H=1,F=2] 
* CE 84: case_6(A,B,C,D,E,F,G,H) = 11+ maxNorm(I,B):[28]+ tableMake(J,K,L,M,N,O,G,P):[36]+ maxNorm(Q,B):[28]+ tableMake(R,S,L,T,N,U,G,V):[37]+ concat(W,X):[17]
     [R>=G,J>=G,E>=N,T>=D,M>=D,R>=A,J>=A,X>=0,L>=2,S>=1,B>=1,M>=1,K>=1,D>=0,L=C+1,W=1,V=1,U=1,Q=1,P=1,O=1,I=1,H=1,F=2] 
* CE 85: case_6(A,B,C,D,E,F,G,H) = 11+ maxNorm(I,B):[28]+ tableMake(J,K,L,M,N,O,G,P):[36]+ maxNorm(Q,B):[28]+ tableMake(R,S,L,T,N,U,G,V):[36]+ concat(W,X):[[18],17]
     [R>=G,J>=G,E>=N,T>=D,M>=D,R>=A,J>=A,X>=0,W>=2,L>=2,S>=1,B>=1,M>=1,K>=1,D>=0,L=C+1,V=1,U=1,Q=1,P=1,O=1,I=1,H=1,F=2] 
* CE 86: case_6(A,B,C,D,E,F,G,H) = 11+ maxNorm(I,B):[28]+ tableMake(J,K,L,M,N,O,G,P):[36]+ maxNorm(Q,B):[28]+ tableMake(R,S,L,T,N,U,G,V):[36]+ concat(W,X):[17]
     [R>=G,J>=G,E>=N,T>=D,M>=D,R>=A,J>=A,X>=0,L>=2,S>=1,B>=1,M>=1,K>=1,D>=0,L=C+1,W=1,V=1,U=1,Q=1,P=1,O=1,I=1,H=1,F=2] 
* CE 87: case_6(A,B,C,D,E,F,G,H) = 11+ maxNorm(I,B):[28]+ tableMake(J,K,L,M,N,O,G,P):[multiple([32,33,34,35],[[38],[37],[36]])]+ maxNorm(Q,B):[28]+ tableMake(R,S,L,T,N,O,G,U):[multiple([32,33,34,35],[[38],[37],[36]])]+ concat(V,W):[[18],17]
     [E>=N,T>=D,M>=D,R>=A,J>=A,W>=0,V>=2,O>=2,L>=1,S>=0,B>=1,M>=1,K>=0,D>=0,O+1=F,L=C+1,U=1,Q=1,P=1,I=1,H=1] 
* CE 88: case_6(A,B,C,D,E,F,G,H) = 11+ maxNorm(I,B):[28]+ tableMake(J,K,L,M,N,O,G,P):[multiple([32,33,34,35],[[38],[37],[36]])]+ maxNorm(Q,B):[28]+ tableMake(R,S,L,T,N,O,G,U):[multiple([32,33,34,35],[[38],[37],[36]])]+ concat(V,W):[17]
     [E>=N,T>=D,M>=D,R>=A,J>=A,W>=0,O>=2,L>=1,S>=0,B>=1,M>=1,K>=0,D>=0,O+1=F,L=C+1,V=1,U=1,Q=1,P=1,I=1,H=1] 
* CE 89: case_6(A,B,C,D,E,F,G,H) = 8+ aux(I,C):[[31],30]+ eval(A,B,C,D,G,J):[multiple(27,[[25],[24],[23],[22]])]
     [D>=0,C>=2,B>=0,J=3,I=1,H=3,F=1] 
* CE 90: case_6(A,B,C,D,E,F,G,H) = 8+ aux(I,C):[[31],30]+ eval(A,B,C,D,G,J):[multiple(26,[[25],[24],[23],[22]])]
     [D>=0,C>=2,B>=0,J=3,I=1,H=3,F=1] 
* CE 91: case_6(A,B,C,D,E,F,G,H) = 8+ aux(I,C):[[31],30]+ eval(A,B,C,D,G,J):[24]
     [A>=G,D>=0,C>=2,B>=1,J=1,I=1,H=1,F=1] 
* CE 92: case_6(A,B,C,D,E,F,G,H) = 8+ aux(I,C):[[31],30]+ eval(A,B,C,D,G,J):[23]
     [D>=0,C>=2,B>=1,J=1,I=1,H=1,F=1] 
* CE 93: case_6(A,B,C,D,E,F,G,H) = 8+ aux(I,C):[[31],30]+ eval(A,B,C,D,G,J):[22]
     [A>=G,D>=0,C>=2,B>=1,J=1,I=1,H=1,F=1] 
* CE 94: case_6(A,B,C,D,E,F,G,H) = 8+ aux(I,J):[30]+ eval(A,B,K,D,G,L):[multiple(27,[[25],[24],[23],[22]])]
     [D>=0,B>=0,L=3,K=1,J=1,I=1,H=3,F=1,C=1] 
* CE 95: case_6(A,B,C,D,E,F,G,H) = 8+ aux(I,J):[30]+ eval(A,B,K,D,G,L):[multiple(26,[[25],[24],[23],[22]])]
     [D>=0,B>=0,L=3,K=1,J=1,I=1,H=3,F=1,C=1] 
* CE 96: case_6(A,B,C,D,E,F,G,H) = 8+ aux(I,J):[30]+ eval(A,K,L,M,G,N):[25]
     [N=1,M=0,L=1,K=0,J=1,I=1,H=1,F=1,D=0,C=1,B=0] 
* CE 97: case_6(A,B,C,D,E,F,G,H) = 8+ aux(I,J):[30]+ eval(A,B,K,D,G,L):[24]
     [A>=G,D>=0,B>=1,L=1,K=1,J=1,I=1,H=1,F=1,C=1] 

### Cost equations --> "Loop" of case_6/8 
* CEs [88] --> Loop 41 
* CEs [87] --> Loop 42 
* CEs [86] --> Loop 43 
* CEs [85] --> Loop 44 
* CEs [84] --> Loop 45 
* CEs [83] --> Loop 46 
* CEs [82] --> Loop 47 
* CEs [81] --> Loop 48 
* CEs [80] --> Loop 49 
* CEs [79] --> Loop 50 
* CEs [78] --> Loop 51 
* CEs [77] --> Loop 52 
* CEs [76] --> Loop 53 
* CEs [75] --> Loop 54 
* CEs [74] --> Loop 55 
* CEs [73] --> Loop 56 
* CEs [72] --> Loop 57 
* CEs [71] --> Loop 58 
* CEs [70] --> Loop 59 
* CEs [69] --> Loop 60 
* CEs [90] --> Loop 61 
* CEs [89] --> Loop 62 
* CEs [93] --> Loop 63 
* CEs [91] --> Loop 64 
* CEs [92] --> Loop 65 
* CEs [95] --> Loop 66 
* CEs [94] --> Loop 67 
* CEs [97] --> Loop 68 
* CEs [68] --> Loop 69 
* CEs [67] --> Loop 70 
* CEs [66] --> Loop 71 
* CEs [65] --> Loop 72 
* CEs [64] --> Loop 73 
* CEs [63] --> Loop 74 
* CEs [62] --> Loop 75 
* CEs [61] --> Loop 76 
* CEs [60] --> Loop 77 
* CEs [59] --> Loop 78 
* CEs [58] --> Loop 79 
* CEs [57] --> Loop 80 
* CEs [56] --> Loop 81 
* CEs [55] --> Loop 82 
* CEs [54] --> Loop 83 
* CEs [53] --> Loop 84 
* CEs [52] --> Loop 85 
* CEs [51] --> Loop 86 
* CEs [50] --> Loop 87 
* CEs [49] --> Loop 88 
* CEs [48] --> Loop 89 
* CEs [47] --> Loop 90 
* CEs [46] --> Loop 91 
* CEs [45] --> Loop 92 
* CEs [96] --> Loop 93 
* CEs [44] --> Loop 94 
* CEs [43] --> Loop 95 
* CEs [42] --> Loop 96 
* CEs [41] --> Loop 97 

#### Loops of case_6/8 
* Loop 41: case_6(A,B,C,D,E,F,G,H) [F>=3,D>=0,C>=0,B>=1,H=1] 
* Loop 42: case_6(A,B,C,D,E,F,G,H) [F>=3,D>=0,C>=0,B>=1,H=1] 
* Loop 43: case_6(A,B,C,D,E,F,G,H) [D>=0,C>=1,B>=1,H=1,F=2] 
* Loop 44: case_6(A,B,C,D,E,F,G,H) [D>=0,C>=1,B>=1,H=1,F=2] 
* Loop 45: case_6(A,B,C,D,E,F,G,H) [D>=0,C>=1,B>=1,H=1,F=2] 
* Loop 46: case_6(A,B,C,D,E,F,G,H) [D>=0,C>=1,B>=1,H=1,F=2] 
* Loop 47: case_6(A,B,C,D,E,F,G,H) [D>=0,C>=1,B>=1,H=1,F=2] 
* Loop 48: case_6(A,B,C,D,E,F,G,H) [D>=0,C>=1,B>=1,H=1,F=2] 
* Loop 49: case_6(A,B,C,D,E,F,G,H) [D>=0,C>=1,B>=1,H=1,F=2] 
* Loop 50: case_6(A,B,C,D,E,F,G,H) [D>=0,C>=1,B>=1,H=1,F=2] 
* Loop 51: case_6(A,B,C,D,E,F,G,H) [D>=0,C>=1,B>=1,H=1,F=2] 
* Loop 52: case_6(A,B,C,D,E,F,G,H) [D>=0,C>=1,B>=1,H=1,F=2] 
* Loop 53: case_6(A,B,C,D,E,F,G,H) [D>=0,C>=1,B>=1,H=1,F=2] 
* Loop 54: case_6(A,B,C,D,E,F,G,H) [D>=0,C>=1,B>=1,H=1,F=2] 
* Loop 55: case_6(A,B,C,D,E,F,G,H) [D>=0,C>=1,B>=1,H=1,F=2] 
* Loop 56: case_6(A,B,C,D,E,F,G,H) [D>=0,C>=1,B>=1,H=1,F=2] 
* Loop 57: case_6(A,B,C,D,E,F,G,H) [D>=0,C>=1,B>=1,H=1,F=2] 
* Loop 58: case_6(A,B,C,D,E,F,G,H) [D>=0,C>=1,B>=1,H=1,F=2] 
* Loop 59: case_6(A,B,C,D,E,F,G,H) [D>=0,C>=1,B>=1,H=1,F=2] 
* Loop 60: case_6(A,B,C,D,E,F,G,H) [D>=0,C>=1,B>=1,H=1,F=2] 
* Loop 61: case_6(A,B,C,D,E,F,G,H) [D>=0,C>=2,B>=0,H=3,F=1] 
* Loop 62: case_6(A,B,C,D,E,F,G,H) [D>=0,C>=2,B>=0,H=3,F=1] 
* Loop 63: case_6(A,B,C,D,E,F,G,H) [A>=G,D>=0,C>=2,B>=1,H=1,F=1] 
* Loop 64: case_6(A,B,C,D,E,F,G,H) [A>=G,D>=0,C>=2,B>=1,H=1,F=1] 
* Loop 65: case_6(A,B,C,D,E,F,G,H) [D>=0,C>=2,B>=1,H=1,F=1] 
* Loop 66: case_6(A,B,C,D,E,F,G,H) [D>=0,B>=0,H=3,F=1,C=1] 
* Loop 67: case_6(A,B,C,D,E,F,G,H) [D>=0,B>=0,H=3,F=1,C=1] 
* Loop 68: case_6(A,B,C,D,E,F,G,H) [A>=G,D>=0,B>=1,H=1,F=1,C=1] 
* Loop 69: case_6(A,B,C,D,E,F,G,H) [D>=0,B>=1,H=1,F=2,C=0] 
* Loop 70: case_6(A,B,C,D,E,F,G,H) [D>=0,B>=1,H=1,F=2,C=0] 
* Loop 71: case_6(A,B,C,D,E,F,G,H) [B>=1,H=1,F=2,D=0,C=0] 
* Loop 72: case_6(A,B,C,D,E,F,G,H) [B>=1,H=1,F=2,D=0,C=0] 
* Loop 73: case_6(A,B,C,D,E,F,G,H) [F>=3,D>=0,C>=0,H=1,B=0] 
* Loop 74: case_6(A,B,C,D,E,F,G,H) [F>=3,D>=0,C>=0,H=1,B=0] 
* Loop 75: case_6(A,B,C,D,E,F,G,H) [D>=0,C>=1,H=1,F=2,B=0] 
* Loop 76: case_6(A,B,C,D,E,F,G,H) [D>=0,C>=1,H=1,F=2,B=0] 
* Loop 77: case_6(A,B,C,D,E,F,G,H) [D>=0,C>=1,H=1,F=2,B=0] 
* Loop 78: case_6(A,B,C,D,E,F,G,H) [D>=0,C>=1,H=1,F=2,B=0] 
* Loop 79: case_6(A,B,C,D,E,F,G,H) [D>=0,C>=1,H=1,F=2,B=0] 
* Loop 80: case_6(A,B,C,D,E,F,G,H) [D>=0,C>=1,H=1,F=2,B=0] 
* Loop 81: case_6(A,B,C,D,E,F,G,H) [D>=0,C>=1,H=1,F=2,B=0] 
* Loop 82: case_6(A,B,C,D,E,F,G,H) [D>=0,C>=1,H=1,F=2,B=0] 
* Loop 83: case_6(A,B,C,D,E,F,G,H) [D>=0,C>=1,H=1,F=2,B=0] 
* Loop 84: case_6(A,B,C,D,E,F,G,H) [D>=0,C>=1,H=1,F=2,B=0] 
* Loop 85: case_6(A,B,C,D,E,F,G,H) [D>=0,C>=1,H=1,F=2,B=0] 
* Loop 86: case_6(A,B,C,D,E,F,G,H) [D>=0,C>=1,H=1,F=2,B=0] 
* Loop 87: case_6(A,B,C,D,E,F,G,H) [D>=0,C>=1,H=1,F=2,B=0] 
* Loop 88: case_6(A,B,C,D,E,F,G,H) [D>=0,C>=1,H=1,F=2,B=0] 
* Loop 89: case_6(A,B,C,D,E,F,G,H) [D>=0,C>=1,H=1,F=2,B=0] 
* Loop 90: case_6(A,B,C,D,E,F,G,H) [D>=0,C>=1,H=1,F=2,B=0] 
* Loop 91: case_6(A,B,C,D,E,F,G,H) [D>=0,C>=1,H=1,F=2,B=0] 
* Loop 92: case_6(A,B,C,D,E,F,G,H) [D>=0,C>=1,H=1,F=2,B=0] 
* Loop 93: case_6(A,B,C,D,E,F,G,H) [H=1,F=1,D=0,C=1,B=0] 
* Loop 94: case_6(A,B,C,D,E,F,G,H) [D>=0,H=1,F=2,C=0,B=0] 
* Loop 95: case_6(A,B,C,D,E,F,G,H) [D>=0,H=1,F=2,C=0,B=0] 
* Loop 96: case_6(A,B,C,D,E,F,G,H) [H=1,F=2,D=0,C=0,B=0] 
* Loop 97: case_6(A,B,C,D,E,F,G,H) [H=1,F=2,D=0,C=0,B=0] 

### Ranking functions of CR case_6(A,B,C,D,E,F,G,H) 

#### Partial ranking functions of CR case_6(A,B,C,D,E,F,G,H) 


### Resulting Chains:case_6(A,B,C,D,E,F,G,H) 
* [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]
* [57]
* [56]
* [55]
* [54]
* [53]
* [52]
* [51]
* [50]
* [49]
* [48]
* [47]
* [46]
* [45]
* [44]
* [43]
* [42]
* [41]


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

#### Cost of loops [18] 

 * loop 18:concat(A,B) -> [concat(A',B')] 
5
#### Cost of phase [18]:concat(A,B) -> [concat(A',B')] 
5*it(18)+0
  Such that:it(18) =< A
it(18) =< A-A'
it(18) >= A-A'

#### Cost of chains of concat(A,B):
* Chain [[18],17]: 5*it(18)+2
  Such that:it(18) =< A-1
it(18) >= A-1

  with precondition: [A>=2,B>=0] 

* Chain [17]: 2
  with precondition: [A=1,B>=0] 


#### Cost of loops [19] 

 * loop 19:assoc(A,B,C,D,E) -> [assoc(A',B',C',D',E')] 
8
#### Cost of phase [19]:assoc(A,B,C,D,E) -> [assoc(A',B',C',D',E')] 
8*it(19)+0
  Such that:it(19) =< D
it(19) =< D-D'
it(19) >= D-D'

#### Cost of phase [19]:assoc(A,B,C,D,E) -> [assoc(A',B',C',D',E')] 
8*it(19)+0
  Such that:it(19) =< D
it(19) =< D-D'
it(19) >= D-D'

#### Cost of chains of assoc(A,B,C,D,E):
* Chain [[19],21]: 8*it(19)+3
  Such that:it(19) =< D-1
it(19) >= D-1

  with precondition: [C>=1,D>=2,E>=0] 

* Chain [[19],20]: 8*it(19)+7
  Such that:it(19) =< D-1
it(19) >= 1

  with precondition: [C>=1,D>=2,E>=0,B>=A] 

* Chain [21]: 3
  with precondition: [C=0,D=1,E=0] 

* Chain [20]: 7
  with precondition: [C>=1,D>=1,E>=0,B>=A] 


#### Cost of chains of eval(A,B,C,D,E,F):
* Chain [multiple(27,[[25],[24],[23],[22]])]: 1*aux(9)+8
  Such that:aux(5)+aux(6)+aux(7)+aux(8) =< 1
aux(1) =< 6
aux(2) =< 10
aux(10) =< C-1
s(1) =< aux(10)
s(2) =< aux(10)
aux(3) =< 6+s(1)*8
aux(4) =< 10+s(2)*8
aux(9) =< aux(4)*aux(5)+aux(3)*aux(6)+aux(2)*aux(7)+aux(1)*aux(8)
s(1) =< aux(10)
s(2) =< aux(10)
aux(3) =< 6+s(1)*8
aux(4) =< 10+s(2)*8
aux(9) =< aux(4)*aux(5)+aux(3)*aux(6)+aux(2)*aux(7)+aux(1)*aux(8)
aux(11) >= 1
aux(1) >= 6
aux(2) >= 10
s(1) >= C-1
aux(5)+aux(6)+aux(7)+aux(8) >= aux(11)
s(2) >= aux(11)
aux(3) >= 6+s(1)*8
aux(4) >= 10+s(2)*8
aux(9) >= aux(4)*aux(5)+aux(3)*aux(6)+aux(2)*aux(7)+aux(1)*aux(8)
aux(5)+aux(6)+aux(7)+aux(8) >= aux(11)
s(2) >= aux(11)
aux(3) >= 6+s(1)*8
aux(4) >= 10+s(2)*8
aux(9) >= aux(4)*aux(5)+aux(3)*aux(6)+aux(2)*aux(7)+aux(1)*aux(8)

  with precondition: [F=3,B>=0,C>=1,D>=0] 

* Chain [multiple(26,[[25],[24],[23],[22]])]: 1*aux(20)+7
  Such that:aux(16)+aux(17)+aux(18)+aux(19) =< 1
aux(12) =< 6
aux(13) =< 10
aux(21) =< C-1
s(1) =< aux(21)
s(2) =< aux(21)
aux(14) =< 6+s(1)*8
aux(15) =< 10+s(2)*8
aux(20) =< aux(15)*aux(16)+aux(14)*aux(17)+aux(13)*aux(18)+aux(12)*aux(19)
s(1) =< aux(21)
s(2) =< aux(21)
aux(14) =< 6+s(1)*8
aux(15) =< 10+s(2)*8
aux(20) =< aux(15)*aux(16)+aux(14)*aux(17)+aux(13)*aux(18)+aux(12)*aux(19)
aux(22) >= 1
aux(12) >= 6
aux(13) >= 10
s(1) >= C-1
aux(16)+aux(17)+aux(18)+aux(19) >= aux(22)
s(2) >= aux(22)
aux(14) >= 6+s(1)*8
aux(15) >= 10+s(2)*8
aux(20) >= aux(15)*aux(16)+aux(14)*aux(17)+aux(13)*aux(18)+aux(12)*aux(19)
aux(16)+aux(17)+aux(18)+aux(19) >= aux(22)
s(2) >= aux(22)
aux(14) >= 6+s(1)*8
aux(15) >= 10+s(2)*8
aux(20) >= aux(15)*aux(16)+aux(14)*aux(17)+aux(13)*aux(18)+aux(12)*aux(19)

  with precondition: [F=3,B>=0,C>=1,D>=0] 

* Chain [25]: 6
  with precondition: [B=0,C=1,D=0,F=1] 

* Chain [24]: 10
  with precondition: [F=1,B>=1,C>=1,D>=0,A>=E] 

* Chain [23]: 8*s(1)+6
  Such that:s(1) =< C-1
s(1) >= C-1

  with precondition: [F=1,B>=1,C>=2,D>=0] 

* Chain [22]: 8*s(2)+10
  Such that:s(2) =< C-1
s(2) >= 1

  with precondition: [F=1,B>=1,C>=2,D>=0,A>=E] 


#### Cost of chains of maxNorm(A,B):
* Chain [29]: 0
  with precondition: [A=1,B=0] 

* Chain [28]: 0
  with precondition: [A=1,B>=1] 


#### Cost of loops [31] 

 * loop 31:aux(A,B) -> [aux(A',B')] 
5
#### Cost of phase [31]:aux(A,B) -> [aux(A',B')] 
5*it(31)+0
  Such that:it(31) =< B
it(31) =< B-B'
it(31) >= B-B'

#### Cost of chains of aux(A,B):
* Chain [[31],30]: 5*it(31)+2
  Such that:it(31) =< B-1
it(31) >= B-1

  with precondition: [A>=1,B>=2] 

* Chain [30]: 2
  with precondition: [B=1,A>=1] 


#### Cost of loops [32,33,34,35] 

 * loop 32:tableMake(A,B,C,D,E,F,G,H) -> [tableMake(A',B',C',D',E',F',G',H'),tableMake(A'2,B'2,C'2,D'2,E'2,F'2,G'2,H'2)] 
14
 * loop 33:tableMake(A,B,C,D,E,F,G,H) -> [tableMake(A',B',C',D',E',F',G',H'),tableMake(A'2,B'2,C'2,D'2,E'2,F'2,G'2,H'2)] 
5*s(9)+14
  Such that:s(9) >= 1

 * loop 34:tableMake(A,B,C,D,E,F,G,H) -> [tableMake(A',B',C',D',E',F',G',H'),tableMake(A'2,B'2,C'2,D'2,E'2,F'2,G'2,H'2)] 
14
 * loop 35:tableMake(A,B,C,D,E,F,G,H) -> [tableMake(A',B',C',D',E',F',G',H'),tableMake(A'2,B'2,C'2,D'2,E'2,F'2,G'2,H'2)] 
5*s(11)+14
  Such that:s(11) >= 1

#### Cost of phase [32,33,34,35]:tableMake(A,B,C,D,E,F,G,H) -> [] 
66*it(32)+21*it([36])+21*it([37])+17*it([38])+13*s(14)+5*s(17)+13*s(18)+0
#### Cost of chains of tableMake(A,B,C,D,E,F,G,H):
* Chain [40]: 17
  with precondition: [B=0,C=1,D=0,F=1,H=1] 

* Chain [39]: 21
  with precondition: [C=1,F=1,H=1,B>=1,D>=0,A>=G] 

* Chain [38]: 13*s(3)+17
  Such that:aux(23) =< C-1
s(3) =< aux(23)
aux(24) >= C-1
s(3) >= aux(24)

  with precondition: [F=1,H=1,B>=1,C>=2,D>=0] 

* Chain [37]: 5*s(5)+21
  Such that:s(5) =< C-1
s(5) >= C-1

  with precondition: [F=1,H=1,B>=1,C>=2,D>=0,A>=G] 

* Chain [36]: 5*s(6)+8*s(7)+21
  Such that:aux(25) =< C-1
s(6) =< aux(25)
s(7) =< aux(25)
s(7) >= 1
s(6) >= C-1

  with precondition: [F=1,H=1,B>=1,C>=2,D>=0,A>=G] 

* Chain [multiple([32,33,34,35],[[38],[37],[36]])]: 66*it(32)+21*it([36])+21*it([37])+17*it([38])+13*s(14)+5*s(17)+13*s(18)+0
  with precondition: [H=1,B>=0,C>=1,D>=0,F>=2] 


#### Cost of chains of case_6(A,B,C,D,E,F,G,H):
* Chain [97]: 5*s(21)+51
  Such that:s(21) >= 1

  with precondition: [B=0,C=0,D=0,F=2,H=1] 

* Chain [96]: 51
  with precondition: [B=0,C=0,D=0,F=2,H=1] 

* Chain [95]: 5*s(22)+55
  Such that:s(22) >= 1

  with precondition: [B=0,C=0,F=2,H=1,D>=0] 

* Chain [94]: 55
  with precondition: [B=0,C=0,F=2,H=1,D>=0] 

* Chain [93]: 16
  with precondition: [B=0,C=1,D=0,F=1,H=1] 

* Chain [92]: 26*s(25)+5*s(29)+47
  Such that:aux(84) =< C
s(25) =< aux(84)
s(29) >= 1
aux(85) >= C
aux(85) >= aux(85)
s(25) >= aux(85)

  with precondition: [B=0,F=2,H=1,C>=1,D>=0] 

* Chain [91]: 26*s(32)+47
  Such that:aux(86) =< C
s(32) =< aux(86)
aux(87) >= C
aux(87) >= aux(87)
s(32) >= aux(87)

  with precondition: [B=0,F=2,H=1,C>=1,D>=0] 

* Chain [90]: 18*s(38)+5*s(40)+51
  Such that:aux(88) =< C
s(38) =< aux(88)
s(40) >= 1
aux(89) >= C
aux(89) >= aux(89)
s(38) >= aux(89)

  with precondition: [B=0,F=2,H=1,C>=1,D>=0] 

* Chain [89]: 18*s(43)+51
  Such that:aux(90) =< C
s(43) =< aux(90)
aux(91) >= C
aux(91) >= aux(91)
s(43) >= aux(91)

  with precondition: [B=0,F=2,H=1,C>=1,D>=0] 

* Chain [88]: 18*s(47)+8*s(49)+5*s(51)+51
  Such that:aux(92) =< C
s(47) =< aux(92)
s(49) =< aux(92)
aux(93) >= 1
aux(94) >= C
s(49) >= aux(93)
s(51) >= aux(93)
aux(94) >= aux(94)
s(47) >= aux(94)

  with precondition: [B=0,F=2,H=1,C>=1,D>=0] 

* Chain [87]: 18*s(54)+8*s(56)+51
  Such that:aux(95) =< C
s(54) =< aux(95)
s(56) =< aux(95)
s(56) >= 1
aux(96) >= C
aux(96) >= aux(96)
s(54) >= aux(96)

  with precondition: [B=0,F=2,H=1,C>=1,D>=0] 

* Chain [86]: 18*s(58)+5*s(62)+51
  Such that:aux(97) =< C
s(58) =< aux(97)
s(62) >= 1
aux(98) >= C
s(58) >= aux(98)

  with precondition: [B=0,F=2,H=1,C>=1,D>=0] 

* Chain [85]: 18*s(63)+51
  Such that:aux(99) =< C
s(63) =< aux(99)
aux(100) >= C
s(63) >= aux(100)

  with precondition: [B=0,F=2,H=1,C>=1,D>=0] 

* Chain [84]: 10*s(67)+5*s(69)+55
  Such that:aux(101) =< C
s(67) =< aux(101)
s(69) >= 1
aux(102) >= C
s(67) >= aux(102)

  with precondition: [B=0,F=2,H=1,C>=1,D>=0] 

* Chain [83]: 10*s(70)+55
  Such that:aux(103) =< C
s(70) =< aux(103)
aux(104) >= C
s(70) >= aux(104)

  with precondition: [B=0,F=2,H=1,C>=1,D>=0] 

* Chain [82]: 10*s(72)+8*s(74)+5*s(76)+55
  Such that:aux(105) =< C
s(72) =< aux(105)
s(74) =< aux(105)
aux(106) >= 1
aux(107) >= C
s(74) >= aux(106)
s(76) >= aux(106)
s(72) >= aux(107)

  with precondition: [B=0,F=2,H=1,C>=1,D>=0] 

* Chain [81]: 10*s(77)+8*s(79)+55
  Such that:aux(108) =< C
s(77) =< aux(108)
s(79) =< aux(108)
s(79) >= 1
aux(109) >= C
s(77) >= aux(109)

  with precondition: [B=0,F=2,H=1,C>=1,D>=0] 

* Chain [80]: 8*s(82)+18*s(83)+5*s(87)+51
  Such that:aux(110) =< C
s(83) =< aux(110)
s(82) =< aux(110)
aux(111) >= 1
aux(112) >= C
s(82) >= aux(111)
s(87) >= aux(111)
s(83) >= aux(112)

  with precondition: [B=0,F=2,H=1,C>=1,D>=0] 

* Chain [79]: 8*s(89)+18*s(90)+51
  Such that:aux(113) =< C
s(90) =< aux(113)
s(89) =< aux(113)
s(89) >= 1
aux(114) >= C
s(90) >= aux(114)

  with precondition: [B=0,F=2,H=1,C>=1,D>=0] 

* Chain [78]: 8*s(95)+10*s(96)+5*s(98)+55
  Such that:aux(115) =< C
s(96) =< aux(115)
s(95) =< aux(115)
aux(116) >= 1
aux(117) >= C
s(95) >= aux(116)
s(98) >= aux(116)
s(96) >= aux(117)

  with precondition: [B=0,F=2,H=1,C>=1,D>=0] 

* Chain [77]: 8*s(100)+10*s(101)+55
  Such that:aux(118) =< C
s(101) =< aux(118)
s(100) =< aux(118)
s(100) >= 1
aux(119) >= C
s(101) >= aux(119)

  with precondition: [B=0,F=2,H=1,C>=1,D>=0] 

* Chain [76]: 16*s(104)+10*s(105)+5*s(109)+55
  Such that:aux(120) =< C
s(105) =< aux(120)
s(104) =< aux(120)
aux(121) >= 1
aux(122) >= C
s(104) >= aux(121)
s(109) >= aux(121)
s(105) >= aux(122)

  with precondition: [B=0,F=2,H=1,C>=1,D>=0] 

* Chain [75]: 16*s(111)+10*s(112)+55
  Such that:aux(123) =< C
s(112) =< aux(123)
s(111) =< aux(123)
aux(124) >= 1
aux(125) >= C
s(111) >= aux(124)
s(112) >= aux(125)

  with precondition: [B=0,F=2,H=1,C>=1,D>=0] 

* Chain [74]: 312*s(116)+5*s(130)+13
  Such that:s(130) >= 1

  with precondition: [B=0,H=1,C>=0,D>=0,F>=3] 

* Chain [73]: 312*s(131)+13
  with precondition: [B=0,H=1,C>=0,D>=0,F>=3] 

* Chain [72]: 5*s(145)+51
  Such that:s(145) >= 1

  with precondition: [C=0,D=0,F=2,H=1,B>=1] 

* Chain [71]: 51
  with precondition: [C=0,D=0,F=2,H=1,B>=1] 

* Chain [70]: 5*s(146)+55
  Such that:s(146) >= 1

  with precondition: [C=0,F=2,H=1,B>=1,D>=0] 

* Chain [69]: 55
  with precondition: [C=0,F=2,H=1,B>=1,D>=0] 

* Chain [68]: 20
  with precondition: [C=1,F=1,H=1,B>=1,D>=0,A>=G] 

* Chain [67]: 1*s(159)+18
  Such that:s(147)+s(148)+s(149)+s(150) =< 1
s(151) =< 6
s(152) =< 10
s(157) =< 6
s(158) =< 10
s(159) =< s(158)*s(147)+s(157)*s(148)+s(152)*s(149)+s(151)*s(150)
s(157) =< 6
s(158) =< 10
s(159) =< s(158)*s(147)+s(157)*s(148)+s(152)*s(149)+s(151)*s(150)
s(154) >= 1
s(151) >= 6
s(152) >= 10
s(147)+s(148)+s(149)+s(150) >= s(154)
s(157) >= 6
s(158) >= 10
s(159) >= s(158)*s(147)+s(157)*s(148)+s(152)*s(149)+s(151)*s(150)
s(147)+s(148)+s(149)+s(150) >= s(154)
s(157) >= 6
s(158) >= 10
s(159) >= s(158)*s(147)+s(157)*s(148)+s(152)*s(149)+s(151)*s(150)

  with precondition: [C=1,F=1,H=3,B>=0,D>=0] 

* Chain [66]: 1*s(172)+17
  Such that:s(160)+s(161)+s(162)+s(163) =< 1
s(164) =< 6
s(165) =< 10
s(170) =< 6
s(171) =< 10
s(172) =< s(171)*s(160)+s(170)*s(161)+s(165)*s(162)+s(164)*s(163)
s(170) =< 6
s(171) =< 10
s(172) =< s(171)*s(160)+s(170)*s(161)+s(165)*s(162)+s(164)*s(163)
s(167) >= 1
s(164) >= 6
s(165) >= 10
s(160)+s(161)+s(162)+s(163) >= s(167)
s(170) >= 6
s(171) >= 10
s(172) >= s(171)*s(160)+s(170)*s(161)+s(165)*s(162)+s(164)*s(163)
s(160)+s(161)+s(162)+s(163) >= s(167)
s(170) >= 6
s(171) >= 10
s(172) >= s(171)*s(160)+s(170)*s(161)+s(165)*s(162)+s(164)*s(163)

  with precondition: [C=1,F=1,H=3,B>=0,D>=0] 

* Chain [65]: 13*s(173)+16
  Such that:aux(126) =< C-1
s(173) =< aux(126)
aux(127) >= C-1
s(173) >= aux(127)

  with precondition: [F=1,H=1,B>=1,C>=2,D>=0] 

* Chain [64]: 5*s(175)+20
  Such that:s(175) =< C-1
s(175) >= C-1

  with precondition: [F=1,H=1,B>=1,C>=2,D>=0,A>=G] 

* Chain [63]: 5*s(176)+8*s(177)+20
  Such that:aux(128) =< C-1
s(176) =< aux(128)
s(177) =< aux(128)
s(177) >= 1
s(176) >= C-1

  with precondition: [F=1,H=1,B>=1,C>=2,D>=0,A>=G] 

* Chain [62]: 5*s(178)+1*s(191)+18
  Such that:s(179)+s(180)+s(181)+s(182) =< 1
s(183) =< 6
s(184) =< 10
aux(129) =< C-1
s(178) =< aux(129)
s(187) =< aux(129)
s(188) =< aux(129)
s(189) =< 6+s(187)*8
s(190) =< 10+s(188)*8
s(191) =< s(190)*s(179)+s(189)*s(180)+s(184)*s(181)+s(183)*s(182)
s(186) >= 1
s(183) >= 6
s(184) >= 10
aux(130) >= C-1
s(178) >= aux(130)
s(187) >= aux(130)
s(179)+s(180)+s(181)+s(182) >= s(186)
s(188) >= s(186)
s(189) >= 6+s(187)*8
s(190) >= 10+s(188)*8
s(191) >= s(190)*s(179)+s(189)*s(180)+s(184)*s(181)+s(183)*s(182)

  with precondition: [F=1,H=3,B>=0,C>=2,D>=0] 

* Chain [61]: 5*s(192)+1*s(205)+17
  Such that:s(193)+s(194)+s(195)+s(196) =< 1
s(197) =< 6
s(198) =< 10
aux(131) =< C-1
s(192) =< aux(131)
s(201) =< aux(131)
s(202) =< aux(131)
s(203) =< 6+s(201)*8
s(204) =< 10+s(202)*8
s(205) =< s(204)*s(193)+s(203)*s(194)+s(198)*s(195)+s(197)*s(196)
s(200) >= 1
s(197) >= 6
s(198) >= 10
aux(132) >= C-1
s(192) >= aux(132)
s(201) >= aux(132)
s(193)+s(194)+s(195)+s(196) >= s(200)
s(202) >= s(200)
s(203) >= 6+s(201)*8
s(204) >= 10+s(202)*8
s(205) >= s(204)*s(193)+s(203)*s(194)+s(198)*s(195)+s(197)*s(196)

  with precondition: [F=1,H=3,B>=0,C>=2,D>=0] 

* Chain [60]: 26*s(208)+5*s(212)+47
  Such that:aux(133) =< C
s(208) =< aux(133)
s(212) >= 1
aux(134) >= C
aux(134) >= aux(134)
s(208) >= aux(134)

  with precondition: [F=2,H=1,B>=1,C>=1,D>=0] 

* Chain [59]: 26*s(215)+47
  Such that:aux(135) =< C
s(215) =< aux(135)
aux(136) >= C
aux(136) >= aux(136)
s(215) >= aux(136)

  with precondition: [F=2,H=1,B>=1,C>=1,D>=0] 

* Chain [58]: 18*s(221)+5*s(223)+51
  Such that:aux(137) =< C
s(221) =< aux(137)
s(223) >= 1
aux(138) >= C
aux(138) >= aux(138)
s(221) >= aux(138)

  with precondition: [F=2,H=1,B>=1,C>=1,D>=0] 

* Chain [57]: 18*s(226)+51
  Such that:aux(139) =< C
s(226) =< aux(139)
aux(140) >= C
aux(140) >= aux(140)
s(226) >= aux(140)

  with precondition: [F=2,H=1,B>=1,C>=1,D>=0] 

* Chain [56]: 18*s(230)+8*s(232)+5*s(234)+51
  Such that:aux(141) =< C
s(230) =< aux(141)
s(232) =< aux(141)
aux(142) >= 1
aux(143) >= C
s(232) >= aux(142)
s(234) >= aux(142)
aux(143) >= aux(143)
s(230) >= aux(143)

  with precondition: [F=2,H=1,B>=1,C>=1,D>=0] 

* Chain [55]: 18*s(237)+8*s(239)+51
  Such that:aux(144) =< C
s(237) =< aux(144)
s(239) =< aux(144)
s(239) >= 1
aux(145) >= C
aux(145) >= aux(145)
s(237) >= aux(145)

  with precondition: [F=2,H=1,B>=1,C>=1,D>=0] 

* Chain [54]: 18*s(241)+5*s(245)+51
  Such that:aux(146) =< C
s(241) =< aux(146)
s(245) >= 1
aux(147) >= C
s(241) >= aux(147)

  with precondition: [F=2,H=1,B>=1,C>=1,D>=0] 

* Chain [53]: 18*s(246)+51
  Such that:aux(148) =< C
s(246) =< aux(148)
aux(149) >= C
s(246) >= aux(149)

  with precondition: [F=2,H=1,B>=1,C>=1,D>=0] 

* Chain [52]: 10*s(250)+5*s(252)+55
  Such that:aux(150) =< C
s(250) =< aux(150)
s(252) >= 1
aux(151) >= C
s(250) >= aux(151)

  with precondition: [F=2,H=1,B>=1,C>=1,D>=0] 

* Chain [51]: 10*s(253)+55
  Such that:aux(152) =< C
s(253) =< aux(152)
aux(153) >= C
s(253) >= aux(153)

  with precondition: [F=2,H=1,B>=1,C>=1,D>=0] 

* Chain [50]: 10*s(255)+8*s(257)+5*s(259)+55
  Such that:aux(154) =< C
s(255) =< aux(154)
s(257) =< aux(154)
aux(155) >= 1
aux(156) >= C
s(257) >= aux(155)
s(259) >= aux(155)
s(255) >= aux(156)

  with precondition: [F=2,H=1,B>=1,C>=1,D>=0] 

* Chain [49]: 10*s(260)+8*s(262)+55
  Such that:aux(157) =< C
s(260) =< aux(157)
s(262) =< aux(157)
s(262) >= 1
aux(158) >= C
s(260) >= aux(158)

  with precondition: [F=2,H=1,B>=1,C>=1,D>=0] 

* Chain [48]: 8*s(265)+18*s(266)+5*s(270)+51
  Such that:aux(159) =< C
s(266) =< aux(159)
s(265) =< aux(159)
aux(160) >= 1
aux(161) >= C
s(265) >= aux(160)
s(270) >= aux(160)
s(266) >= aux(161)

  with precondition: [F=2,H=1,B>=1,C>=1,D>=0] 

* Chain [47]: 8*s(272)+18*s(273)+51
  Such that:aux(162) =< C
s(273) =< aux(162)
s(272) =< aux(162)
s(272) >= 1
aux(163) >= C
s(273) >= aux(163)

  with precondition: [F=2,H=1,B>=1,C>=1,D>=0] 

* Chain [46]: 8*s(278)+10*s(279)+5*s(281)+55
  Such that:aux(164) =< C
s(279) =< aux(164)
s(278) =< aux(164)
aux(165) >= 1
aux(166) >= C
s(278) >= aux(165)
s(281) >= aux(165)
s(279) >= aux(166)

  with precondition: [F=2,H=1,B>=1,C>=1,D>=0] 

* Chain [45]: 8*s(283)+10*s(284)+55
  Such that:aux(167) =< C
s(284) =< aux(167)
s(283) =< aux(167)
s(283) >= 1
aux(168) >= C
s(284) >= aux(168)

  with precondition: [F=2,H=1,B>=1,C>=1,D>=0] 

* Chain [44]: 16*s(287)+10*s(288)+5*s(292)+55
  Such that:aux(169) =< C
s(288) =< aux(169)
s(287) =< aux(169)
aux(170) >= 1
aux(171) >= C
s(287) >= aux(170)
s(292) >= aux(170)
s(288) >= aux(171)

  with precondition: [F=2,H=1,B>=1,C>=1,D>=0] 

* Chain [43]: 16*s(294)+10*s(295)+55
  Such that:aux(172) =< C
s(295) =< aux(172)
s(294) =< aux(172)
aux(173) >= 1
aux(174) >= C
s(294) >= aux(173)
s(295) >= aux(174)

  with precondition: [F=2,H=1,B>=1,C>=1,D>=0] 

* Chain [42]: 312*s(299)+5*s(313)+13
  Such that:s(313) >= 1

  with precondition: [H=1,B>=1,C>=0,D>=0,F>=3] 

* Chain [41]: 312*s(314)+13
  with precondition: [H=1,B>=1,C>=0,D>=0,F>=3] 


Closed-form bounds of case_6(A,B,C,D,E,F,G,H): 
-------------------------------------
* Chain [97] with precondition: [B=0,C=0,D=0,F=2,H=1] 
    - Lower bound: 56 
    - Complexity: constant
 * Chain [96] with precondition: [B=0,C=0,D=0,F=2,H=1] 
    - Lower bound: 51 
    - Complexity: constant
 * Chain [95] with precondition: [B=0,C=0,F=2,H=1,D>=0] 
    - Lower bound: 60 
    - Complexity: constant
 * Chain [94] with precondition: [B=0,C=0,F=2,H=1,D>=0] 
    - Lower bound: 55 
    - Complexity: constant
 * Chain [93] with precondition: [B=0,C=1,D=0,F=1,H=1] 
    - Lower bound: 16 
    - Complexity: constant
 * Chain [92] with precondition: [B=0,F=2,H=1,C>=1,D>=0] 
    - Lower bound: 26*C+52 
    - Complexity: n
 * Chain [91] with precondition: [B=0,F=2,H=1,C>=1,D>=0] 
    - Lower bound: 26*C+47 
    - Complexity: n
 * Chain [90] with precondition: [B=0,F=2,H=1,C>=1,D>=0] 
    - Lower bound: 18*C+56 
    - Complexity: n
 * Chain [89] with precondition: [B=0,F=2,H=1,C>=1,D>=0] 
    - Lower bound: 18*C+51 
    - Complexity: n
 * Chain [88] with precondition: [B=0,F=2,H=1,C>=1,D>=0] 
    - Lower bound: 18*C+64 
    - Complexity: n
 * Chain [87] with precondition: [B=0,F=2,H=1,C>=1,D>=0] 
    - Lower bound: 18*C+59 
    - Complexity: n
 * Chain [86] with precondition: [B=0,F=2,H=1,C>=1,D>=0] 
    - Lower bound: 18*C+56 
    - Complexity: n
 * Chain [85] with precondition: [B=0,F=2,H=1,C>=1,D>=0] 
    - Lower bound: 18*C+51 
    - Complexity: n
 * Chain [84] with precondition: [B=0,F=2,H=1,C>=1,D>=0] 
    - Lower bound: 10*C+60 
    - Complexity: n
 * Chain [83] with precondition: [B=0,F=2,H=1,C>=1,D>=0] 
    - Lower bound: 10*C+55 
    - Complexity: n
 * Chain [82] with precondition: [B=0,F=2,H=1,C>=1,D>=0] 
    - Lower bound: 10*C+68 
    - Complexity: n
 * Chain [81] with precondition: [B=0,F=2,H=1,C>=1,D>=0] 
    - Lower bound: 10*C+63 
    - Complexity: n
 * Chain [80] with precondition: [B=0,F=2,H=1,C>=1,D>=0] 
    - Lower bound: 18*C+64 
    - Complexity: n
 * Chain [79] with precondition: [B=0,F=2,H=1,C>=1,D>=0] 
    - Lower bound: 18*C+59 
    - Complexity: n
 * Chain [78] with precondition: [B=0,F=2,H=1,C>=1,D>=0] 
    - Lower bound: 10*C+68 
    - Complexity: n
 * Chain [77] with precondition: [B=0,F=2,H=1,C>=1,D>=0] 
    - Lower bound: 10*C+63 
    - Complexity: n
 * Chain [76] with precondition: [B=0,F=2,H=1,C>=1,D>=0] 
    - Lower bound: 10*C+76 
    - Complexity: n
 * Chain [75] with precondition: [B=0,F=2,H=1,C>=1,D>=0] 
    - Lower bound: 10*C+71 
    - Complexity: n
 * Chain [74] with precondition: [B=0,H=1,C>=0,D>=0,F>=3] 
    - Lower bound: 18 
    - Complexity: constant
 * Chain [73] with precondition: [B=0,H=1,C>=0,D>=0,F>=3] 
    - Lower bound: 13 
    - Complexity: constant
 * Chain [72] with precondition: [C=0,D=0,F=2,H=1,B>=1] 
    - Lower bound: 56 
    - Complexity: constant
 * Chain [71] with precondition: [C=0,D=0,F=2,H=1,B>=1] 
    - Lower bound: 51 
    - Complexity: constant
 * Chain [70] with precondition: [C=0,F=2,H=1,B>=1,D>=0] 
    - Lower bound: 60 
    - Complexity: constant
 * Chain [69] with precondition: [C=0,F=2,H=1,B>=1,D>=0] 
    - Lower bound: 55 
    - Complexity: constant
 * Chain [68] with precondition: [C=1,F=1,H=1,B>=1,D>=0,A>=G] 
    - Lower bound: 20 
    - Complexity: constant
 * Chain [67] with precondition: [C=1,F=1,H=3,B>=0,D>=0] 
    - Lower bound: 24 
    - Complexity: constant
 * Chain [66] with precondition: [C=1,F=1,H=3,B>=0,D>=0] 
    - Lower bound: 23 
    - Complexity: constant
 * Chain [65] with precondition: [F=1,H=1,B>=1,C>=2,D>=0] 
    - Lower bound: 13*C+3 
    - Complexity: n
 * Chain [64] with precondition: [F=1,H=1,B>=1,C>=2,D>=0,A>=G] 
    - Lower bound: 5*C+15 
    - Complexity: n
 * Chain [63] with precondition: [F=1,H=1,B>=1,C>=2,D>=0,A>=G] 
    - Lower bound: 5*C+23 
    - Complexity: n
 * Chain [62] with precondition: [F=1,H=3,B>=0,C>=2,D>=0] 
    - Lower bound: 5*C+19 
    - Complexity: n
 * Chain [61] with precondition: [F=1,H=3,B>=0,C>=2,D>=0] 
    - Lower bound: 5*C+18 
    - Complexity: n
 * Chain [60] with precondition: [F=2,H=1,B>=1,C>=1,D>=0] 
    - Lower bound: 26*C+52 
    - Complexity: n
 * Chain [59] with precondition: [F=2,H=1,B>=1,C>=1,D>=0] 
    - Lower bound: 26*C+47 
    - Complexity: n
 * Chain [58] with precondition: [F=2,H=1,B>=1,C>=1,D>=0] 
    - Lower bound: 18*C+56 
    - Complexity: n
 * Chain [57] with precondition: [F=2,H=1,B>=1,C>=1,D>=0] 
    - Lower bound: 18*C+51 
    - Complexity: n
 * Chain [56] with precondition: [F=2,H=1,B>=1,C>=1,D>=0] 
    - Lower bound: 18*C+64 
    - Complexity: n
 * Chain [55] with precondition: [F=2,H=1,B>=1,C>=1,D>=0] 
    - Lower bound: 18*C+59 
    - Complexity: n
 * Chain [54] with precondition: [F=2,H=1,B>=1,C>=1,D>=0] 
    - Lower bound: 18*C+56 
    - Complexity: n
 * Chain [53] with precondition: [F=2,H=1,B>=1,C>=1,D>=0] 
    - Lower bound: 18*C+51 
    - Complexity: n
 * Chain [52] with precondition: [F=2,H=1,B>=1,C>=1,D>=0] 
    - Lower bound: 10*C+60 
    - Complexity: n
 * Chain [51] with precondition: [F=2,H=1,B>=1,C>=1,D>=0] 
    - Lower bound: 10*C+55 
    - Complexity: n
 * Chain [50] with precondition: [F=2,H=1,B>=1,C>=1,D>=0] 
    - Lower bound: 10*C+68 
    - Complexity: n
 * Chain [49] with precondition: [F=2,H=1,B>=1,C>=1,D>=0] 
    - Lower bound: 10*C+63 
    - Complexity: n
 * Chain [48] with precondition: [F=2,H=1,B>=1,C>=1,D>=0] 
    - Lower bound: 18*C+64 
    - Complexity: n
 * Chain [47] with precondition: [F=2,H=1,B>=1,C>=1,D>=0] 
    - Lower bound: 18*C+59 
    - Complexity: n
 * Chain [46] with precondition: [F=2,H=1,B>=1,C>=1,D>=0] 
    - Lower bound: 10*C+68 
    - Complexity: n
 * Chain [45] with precondition: [F=2,H=1,B>=1,C>=1,D>=0] 
    - Lower bound: 10*C+63 
    - Complexity: n
 * Chain [44] with precondition: [F=2,H=1,B>=1,C>=1,D>=0] 
    - Lower bound: 10*C+76 
    - Complexity: n
 * Chain [43] with precondition: [F=2,H=1,B>=1,C>=1,D>=0] 
    - Lower bound: 10*C+71 
    - Complexity: n
 * Chain [42] with precondition: [H=1,B>=1,C>=0,D>=0,F>=3] 
    - Lower bound: 18 
    - Complexity: constant
 * Chain [41] with precondition: [H=1,B>=1,C>=0,D>=0,F>=3] 
    - Lower bound: 13 
    - Complexity: constant
 
### Partitioned lower bound of case_6(A,B,C,D,E,F,G,H): 
* 13 
 if [H=1,B>=0,C>=0,D>=0,F>=3]
* 16 
 if [B=0,C=1,D=0,F=1,H=1]
* 20 
 if [C=1,F=1,H=1,B>=1,D>=0,A>=G]
* 23 
 if [C=1,F=1,H=3,B>=0,D>=0]
* 51 
 if [C=0,D=0,F=2,H=1,B>=0]
* 55 
 if [C=0,F=2,H=1,B>=0,D>=1]
* 5*C+15 
 if [F=1,H=1,B>=1,C>=2,D>=0,A>=G]
* 5*C+18 
 if [F=1,H=3,B>=0,C>=2,D>=0]
* 10*C+55 
 if [F=2,H=1,B>=0,C>=1,D>=0]
* 13*C+3 
 if [F=1,H=1,B>=1,C>=2,D>=0,G>=A+1]
Possible lower bounds : [13,16,20,23,51,55,5*C+15,5*C+18,10*C+55,13*C+3]
Maximum lower bound complexity: n
* Total analysis performed in 1103 ms.