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 2 ms.
sabu_memo_table_1(case_0,[A,B,C],[1*C=0,1*B=1],0,0)
sabu_memo_table_1(case_2,[A,B,C,D,E,F,G],[1*A+ -1*E=0,1*F+ -1*G=0],0,0)
sabu_memo_table_1(assoc,[A,B,C],[1*B=1,1*C=0],1,0)
sabu_memo_table_1(case_1,[A,B,C,D,E],[1*A+ -1*E>=0,1*A>=1,1*A+ -1*C= -1],1,0)
sabu_memo_table_1(case_1,[A,B,C,D,E],[1*C>=2,1*C+ -1*E>=1,-1*A+1*C>=1],1,1)
sabu_memo_table_1(case_0,[A,B,C],[1*B+ -1*C>=1,1*B>=1],2,1)
sabu_memo_table_1(case_2,[A,B,C,D,E,F,G],[-1*A+1*E>=0],2,1)
sabu_memo_table_1(case_2,[A,B,C,D,E,F,G],[],2,2)
sabu_memo_table_1(assoc,[A,B,C],[1*B+ -1*C>=1,1*B>=1],3,1)
sabu_memo_table_1(case_1,[A,B,C,D,E],[1*C>=2],3,2)
sabu_memo_table_1(case_0,[A,B,C],[1*B>=1],4,2)
sabu_memo_table_1(assoc,[A,B,C],[1*B>=1],5,2)
sabu_memo_table_1(case_3,[A,B,C],[1*B=1,1*A+ -1*C=0],0,0)
sabu_memo_table_1(aux,[A,B,C],[1*A+ -1*C=0,1*B=1],1,0)
sabu_memo_table_1(case_3,[A,B,C],[-1*A+1*C>=0,1*B>=1],2,1)
sabu_memo_table_1(aux,[A,B,C],[-1*A+1*C>=0,1*B>=1],3,1)
sabu_memo_table_1(case_4,[A,B,C],[1*A=1,1*B+ -1*C=0],0,0)
sabu_memo_table_1(concat,[A,B,C],[1*B+ -1*C=0,1*A=1],0,0)
sabu_memo_table_1(case_4,[A,B,C],[-1*B+1*C>=0,1*A>=1],1,1)
sabu_memo_table_1(concat,[A,B,C],[-1*B+1*C>=0,1*A>=1],2,1)
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],[1*B>=2,1*A>=1],0,0)
sabu_memo_table_1(eval,[A,B,C],[1*A>=1,1*B>=2],0,0)
sabu_memo_table_1(rev,[A,B],[1*B>=1,1*A>=1],0,0)
sabu_memo_table_1(case_6,[A,B,C,D],[1*D>=3,1*C>=2,1*A>=1,1*B=1],0,0)
sabu_memo_table_1(tableMake,[A,B,C,D],[1*B=1,1*A>=1,1*C>=2,1*D>=3],0,0)
sabu_memo_table_1(case_6,[A,B,C,D],[1*B>=1,1*C>=2,1*D>=3],1,1)
sabu_memo_table_1(tableMake,[A,B,C,D],[1*C>=2,1*D>=3,1*B>=1],2,1)
sabu_memo_table_1(start,[A,B,C,D],[1*B>=1,1*D>=3,1*C>=2],0,0)
sabu_memo_table_1(start,[A,B],[],0,0)
:- dynamic sabu_memo_table_1/5.

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


Size analysis performed in 12 ms.

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

Generated 54 equations 
removed eval(_G68,_G69)

Cost relation system solved by PUBS in 177 ms.

Method start terminates?: YES

UB for start(valVars,vars,expr) = pow(2,nat(vars))*pow(2,nat(expr))*c(maximize_failed)


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

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

#### Obtained direct recursion through partial evaluation 
0. SCC is partially evaluated into concat/2
1. SCC is partially evaluated into and_op/2
2. SCC is partially evaluated into assoc/2
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 eval/2
7. SCC is partially evaluated into aux/2
8. SCC is completely evaluated into other SCCs
9. SCC is partially evaluated into tableMake/3
11. SCC is partially evaluated into case_6/3

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

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


#### Refined cost equations concat/2 
* CE 24: concat(A,B) = 5+ concat(C,B)
     [A>=C+1,B>=3,A>=2] 
* CE 25: concat(A,B) = 2
     [B>=3,A=1] 

### Cost equations --> "Loop" of concat/2 
* CEs [25] --> Loop 24 
* CEs [24] --> Loop 25 

#### Loops of concat/2 
* Loop 24: concat(A,B) [B>=3,A=1] 
* Loop 25: concat(A,B)->  concat(A',B)
                  [A>=A'+1,B>=3,A>=2] 

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

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


### Resulting Chains:concat(A,B) 
* [[25],24]


### Specialization of cost equations and_op/2 
* CE 20 is refined into CE [26] 
* CE 21 is refined into CE [27] 


#### Refined cost equations and_op/2 
* CE 26: and_op(A,B) = 0
     [A=1] 
* CE 27: and_op(A,B) = 0
     [A=0] 

### Cost equations --> "Loop" of and_op/2 
* CEs [26] --> Loop 26 
* CEs [27] --> Loop 27 

#### Loops of and_op/2 
* Loop 26: and_op(A,B) [A=1] 
* Loop 27: 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) 
* [27]
* [26]


### Specialization of cost equations assoc/2 
* CE 19 is refined into CE [28] 
* CE 17 is refined into CE [29] 
* CE 18 is refined into CE [30] 


#### Refined cost equations assoc/2 
* CE 28: assoc(A,B) = 7
     [B>=A+2,A>=1] 
* CE 29: assoc(A,B) = 3
     [A>=1,B=1] 
* CE 30: assoc(A,B) = 8+ assoc(A,C)
     [B>=C+1,B>=3,A>=1] 

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

#### Loops of assoc/2 
* Loop 28: assoc(A,B)->  assoc(A,B')
                  [B>=B'+1,B>=3,A>=1] 
* Loop 29: assoc(A,B) [B>=A+2,A>=1] 
* Loop 30: assoc(A,B) [A>=1,B=1] 

### Ranking functions of CR assoc(A,B) 
* RF of phase [28]: [B-2]

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


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


### Specialization of cost equations or/2 
* CE 23 is refined into CE [31] 
* CE 22 is refined into CE [32] 


#### Refined cost equations or/2 
* CE 31: or(A,B) = 0
     [A=1] 
* CE 32: or(A,B) = 0
     [A=0] 

### Cost equations --> "Loop" of or/2 
* CEs [31] --> Loop 31 
* CEs [32] --> Loop 32 

#### Loops of or/2 
* Loop 31: or(A,B) [A=1] 
* Loop 32: 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) 
* [32]
* [31]


### Specialization of cost equations eval/2 
* CE 16 is refined into CE [33,34] 
* CE 14 is refined into CE [35,36] 
* CE 15 is refined into CE [37,38] 
* CE 13 is refined into CE [39,40] 
* CE 12 is refined into CE [41,42,43,44] 


#### Refined cost equations eval/2 
* CE 33: eval(A,B) = 8+ eval(A,C)+ eval(A,D)+ or(E,F):[32]
     [D>=C,C>=2,A>=1,D+1=B,E=0] 
* CE 34: eval(A,B) = 8+ eval(A,C)+ eval(A,D)+ or(E,F):[31]
     [D>=C,C>=2,A>=1,D+1=B,E=1] 
* CE 35: eval(A,B) = 7+ eval(A,C)+ eval(A,D)+ and_op(E,F):[27]
     [D>=C,C>=2,A>=1,D+1=B,E=0] 
* CE 36: eval(A,B) = 7+ eval(A,C)+ eval(A,D)+ and_op(E,F):[26]
     [D>=C,C>=2,A>=1,D+1=B,E=1] 
* CE 37: eval(A,B) = 8+ eval(A,C)+ eval(A,D)+ or(E,F):[32]
     [C>=D,D>=2,A>=1,C+1=B,E=0] 
* CE 38: eval(A,B) = 8+ eval(A,C)+ eval(A,D)+ or(E,F):[31]
     [C>=D,D>=2,A>=1,C+1=B,E=1] 
* CE 39: eval(A,B) = 7+ eval(A,C)+ eval(A,D)+ and_op(E,F):[27]
     [C>=D,D>=2,A>=1,C+1=B,E=0] 
* CE 40: eval(A,B) = 7+ eval(A,C)+ eval(A,D)+ and_op(E,F):[26]
     [C>=D,D>=2,A>=1,C+1=B,E=1] 
* CE 41: eval(A,B) = 3+ assoc(C,A):[[28],30]
     [A>=3,C>=1,C+1=B] 
* CE 42: eval(A,B) = 3+ assoc(C,A):[[28],29]
     [A>=C+3,C>=1,C+1=B] 
* CE 43: eval(A,B) = 3+ assoc(C,D):[30]
     [C>=1,C+1=B,D=1,A=1] 
* CE 44: eval(A,B) = 3+ assoc(C,A):[29]
     [A>=C+2,C>=1,C+1=B] 

### Cost equations --> "Loop" of eval/2 
* CEs [42] --> Loop 33 
* CEs [44] --> Loop 34 
* CEs [41] --> Loop 35 
* CEs [43] --> Loop 36 
* CEs [36] --> Loop 37 
* CEs [35] --> Loop 38 
* CEs [34] --> Loop 39 
* CEs [33] --> Loop 40 
* CEs [40] --> Loop 41 
* CEs [39] --> Loop 42 
* CEs [38] --> Loop 43 
* CEs [37] --> Loop 44 

#### Loops of eval/2 
* Loop 33: eval(A,B) [A>=B+2,B>=2] 
* Loop 34: eval(A,B) [A>=B+1,B>=2] 
* Loop 35: eval(A,B) [B>=2,A>=3] 
* Loop 36: eval(A,B) [B>=2,A=1] 
* Loop 37: eval(A,B)->  eval(A,B')  eval(A,B'2)
                  [B'2>=B',B'>=2,A>=1,B'2+1=B] 
* Loop 38: eval(A,B)->  eval(A,B')  eval(A,B'2)
                  [B'2>=B',B'>=2,A>=1,B'2+1=B] 
* Loop 39: eval(A,B)->  eval(A,B')  eval(A,B'2)
                  [B'2>=B',B'>=2,A>=1,B'2+1=B] 
* Loop 40: eval(A,B)->  eval(A,B')  eval(A,B'2)
                  [B'2>=B',B'>=2,A>=1,B'2+1=B] 
* Loop 41: eval(A,B)->  eval(A,B')  eval(A,B'2)
                  [B'>=B'2,B'2>=2,A>=1,B'+1=B] 
* Loop 42: eval(A,B)->  eval(A,B')  eval(A,B'2)
                  [B'>=B'2,B'2>=2,A>=1,B'+1=B] 
* Loop 43: eval(A,B)->  eval(A,B')  eval(A,B'2)
                  [B'>=B'2,B'2>=2,A>=1,B'+1=B] 
* Loop 44: eval(A,B)->  eval(A,B')  eval(A,B'2)
                  [B'>=B'2,B'2>=2,A>=1,B'+1=B] 

### Ranking functions of CR eval(A,B) 
* RF of phase [37,38,39,40,41,42,43,44]: [B-2]

#### Partial ranking functions of CR eval(A,B) 
* Partial RF of phase [37,38,39,40,41,42,43,44]:
  - RF of loop [37:1,37:2,38:1,38:2,39:1,39:2,40:1,40:2,41:1,41:2,42:1,42:2,43:1,43:2,44:1,44:2]:
    B-2


### Resulting Chains:eval(A,B) 
* [36]
* [35]
* [34]
* [33]
* [multiple([37,38,39,40,41,42,43,44],[[36],[35],[34],[33]])]


### Specialization of cost equations aux/2 
* CE 10 is refined into CE [45] 
* CE 11 is refined into CE [46] 
* CE 9 is refined into CE [47] 


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

### Cost equations --> "Loop" of aux/2 
* CEs [47] --> Loop 45 
* CEs [45] --> Loop 46 
* CEs [46] --> Loop 47 

#### Loops of aux/2 
* Loop 45: aux(A,B) [A>=1,B=1] 
* Loop 46: aux(A,B)->  aux(A',B')
                  [B>=B'+1,A'>=B,A'>=A+1,B>=2,A>=1] 
* Loop 47: aux(A,B)->  aux(A',B')
                  [A'>=A+1,B'>=1,A>=1,B'+1=B] 

### Ranking functions of CR aux(A,B) 
* RF of phase [46,47]: [B-1]

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


### Resulting Chains:aux(A,B) 
* [[46,47],45]
* [45]


### Specialization of cost equations tableMake/3 
* CE 6 is refined into CE [48,49,50,51] 
* CE 5 is refined into CE [52] 
* CE 4 is refined into CE [53] 


#### Refined cost equations tableMake/3 
* CE 48: tableMake(A,B,C) = 9+ aux(D,A):[[46,47],45]+ eval(A,C):[35]
     [C>=2,A>=3,D=1,B=1] 
* CE 49: tableMake(A,B,C) = 9+ aux(D,A):[[46,47],45]+ eval(A,C):[34]
     [A>=C+1,C>=2,D=1,B=1] 
* CE 50: tableMake(A,B,C) = 9+ aux(D,A):[[46,47],45]+ eval(A,C):[33]
     [A>=C+2,C>=2,D=1,B=1] 
* CE 51: tableMake(A,B,C) = 9+ aux(D,A):[[46,47],45]+ eval(A,C):[multiple([37,38,39,40,41,42,43,44],[[36],[35],[34],[33]])]
     [C>=3,A>=3,D=1,B=1] 
* CE 52: tableMake(A,B,C) = 12+ tableMake(D,E,C)+ tableMake(F,E,C)+ concat(G,H):[[25],24]
     [B>=E+1,F>=B+1,D>=B+1,F>=A+1,D>=A+1,E>=1,H>=3,G>=3,C>=2,A>=3] 
* CE 53: tableMake(A,B,C) = 12+ tableMake(D,E,C)+ tableMake(F,E,C)+ concat(G,H):[[25],24]
     [F>=A+1,D>=A+1,E>=1,H>=3,G>=3,C>=2,A>=3,E+1=B] 

### Cost equations --> "Loop" of tableMake/3 
* CEs [52] --> Loop 48 
* CEs [53] --> Loop 49 
* CEs [50] --> Loop 50 
* CEs [49] --> Loop 51 
* CEs [51] --> Loop 52 
* CEs [48] --> Loop 53 

#### Loops of tableMake/3 
* Loop 48: tableMake(A,B,C)->  tableMake(A',B',C)  tableMake(A'2,B',C)
                  [B>=B'+1,A'2>=B+1,A'>=B+1,A'2>=A+1,A'>=A+1,B'>=1,C>=2,A>=3] 
* Loop 49: tableMake(A,B,C)->  tableMake(A',B',C)  tableMake(A'2,B',C)
                  [A'2>=A+1,A'>=A+1,B'>=1,C>=2,A>=3,B'+1=B] 
* Loop 50: tableMake(A,B,C) [A>=C+2,C>=2,B=1] 
* Loop 51: tableMake(A,B,C) [A>=C+1,C>=2,B=1] 
* Loop 52: tableMake(A,B,C) [C>=3,A>=3,B=1] 
* Loop 53: tableMake(A,B,C) [C>=2,A>=3,B=1] 

### Ranking functions of CR tableMake(A,B,C) 
* RF of phase [48,49]: [B-1]

#### Partial ranking functions of CR tableMake(A,B,C) 
* Partial RF of phase [48,49]:
  - RF of loop [48:1,48:2,49:1,49:2]:
    B-1


### Resulting Chains:tableMake(A,B,C) 
* [53]
* [52]
* [51]
* [50]
* [multiple([48,49],[[53],[52],[51],[50]])]


### Specialization of cost equations case_6/3 
* CE 2 is refined into CE [54,55,56,57,58,59,60,61,62,63,64,65,66,67,68,69,70] 
* CE 1 is refined into CE [71,72,73,74,75,76,77,78,79,80,81,82,83,84,85,86,87] 
* CE 3 is refined into CE [88,89,90,91,92,93] 


#### Refined cost equations case_6/3 
* CE 54: case_6(A,B,C) = 11+ tableMake(D,E,C):[53]+ tableMake(F,G,C):[53]+ concat(H,I):[[25],24]
     [F>=B+1,D>=B+1,F>=A+1,D>=A+1,I>=3,H>=3,C>=2,B>=2,G=1,E=1] 
* CE 55: case_6(A,B,C) = 11+ tableMake(D,E,C):[53]+ tableMake(F,G,C):[52]+ concat(H,I):[[25],24]
     [F>=B+1,D>=B+1,F>=A+1,D>=A+1,I>=3,H>=3,C>=3,B>=2,G=1,E=1] 
* CE 56: case_6(A,B,C) = 11+ tableMake(D,E,C):[53]+ tableMake(F,G,C):[51]+ concat(H,I):[[25],24]
     [F>=C+1,F>=B+1,D>=B+1,F>=A+1,D>=A+1,I>=3,H>=3,C>=2,B>=2,G=1,E=1] 
* CE 57: case_6(A,B,C) = 11+ tableMake(D,E,C):[53]+ tableMake(F,G,C):[50]+ concat(H,I):[[25],24]
     [F>=C+2,F>=B+1,D>=B+1,F>=A+1,D>=A+1,I>=3,H>=3,C>=2,B>=2,G=1,E=1] 
* CE 58: case_6(A,B,C) = 11+ tableMake(D,E,C):[52]+ tableMake(F,G,C):[53]+ concat(H,I):[[25],24]
     [F>=B+1,D>=B+1,F>=A+1,D>=A+1,I>=3,H>=3,C>=3,B>=2,G=1,E=1] 
* CE 59: case_6(A,B,C) = 11+ tableMake(D,E,C):[52]+ tableMake(F,G,C):[52]+ concat(H,I):[[25],24]
     [F>=B+1,D>=B+1,F>=A+1,D>=A+1,I>=3,H>=3,C>=3,B>=2,G=1,E=1] 
* CE 60: case_6(A,B,C) = 11+ tableMake(D,E,C):[52]+ tableMake(F,G,C):[51]+ concat(H,I):[[25],24]
     [F>=C+1,F>=B+1,D>=B+1,F>=A+1,D>=A+1,I>=3,H>=3,C>=3,B>=2,G=1,E=1] 
* CE 61: case_6(A,B,C) = 11+ tableMake(D,E,C):[52]+ tableMake(F,G,C):[50]+ concat(H,I):[[25],24]
     [F>=C+2,F>=B+1,D>=B+1,F>=A+1,D>=A+1,I>=3,H>=3,C>=3,B>=2,G=1,E=1] 
* CE 62: case_6(A,B,C) = 11+ tableMake(D,E,C):[51]+ tableMake(F,G,C):[53]+ concat(H,I):[[25],24]
     [D>=C+1,F>=B+1,D>=B+1,F>=A+1,D>=A+1,I>=3,H>=3,C>=2,B>=2,G=1,E=1] 
* CE 63: case_6(A,B,C) = 11+ tableMake(D,E,C):[51]+ tableMake(F,G,C):[52]+ concat(H,I):[[25],24]
     [D>=C+1,F>=B+1,D>=B+1,F>=A+1,D>=A+1,I>=3,H>=3,C>=3,B>=2,G=1,E=1] 
* CE 64: case_6(A,B,C) = 11+ tableMake(D,E,C):[51]+ tableMake(F,G,C):[51]+ concat(H,I):[[25],24]
     [F>=C+1,D>=C+1,F>=B+1,D>=B+1,F>=A+1,D>=A+1,I>=3,H>=3,C>=2,B>=2,G=1,E=1] 
* CE 65: case_6(A,B,C) = 11+ tableMake(D,E,C):[51]+ tableMake(F,G,C):[50]+ concat(H,I):[[25],24]
     [F>=C+2,D>=C+1,F>=B+1,D>=B+1,F>=A+1,D>=A+1,I>=3,H>=3,C>=2,B>=2,G=1,E=1] 
* CE 66: case_6(A,B,C) = 11+ tableMake(D,E,C):[50]+ tableMake(F,G,C):[53]+ concat(H,I):[[25],24]
     [D>=C+2,F>=B+1,D>=B+1,F>=A+1,D>=A+1,I>=3,H>=3,C>=2,B>=2,G=1,E=1] 
* CE 67: case_6(A,B,C) = 11+ tableMake(D,E,C):[50]+ tableMake(F,G,C):[52]+ concat(H,I):[[25],24]
     [D>=C+2,F>=B+1,D>=B+1,F>=A+1,D>=A+1,I>=3,H>=3,C>=3,B>=2,G=1,E=1] 
* CE 68: case_6(A,B,C) = 11+ tableMake(D,E,C):[50]+ tableMake(F,G,C):[51]+ concat(H,I):[[25],24]
     [F>=C+1,D>=C+2,F>=B+1,D>=B+1,F>=A+1,D>=A+1,I>=3,H>=3,C>=2,B>=2,G=1,E=1] 
* CE 69: case_6(A,B,C) = 11+ tableMake(D,E,C):[50]+ tableMake(F,G,C):[50]+ concat(H,I):[[25],24]
     [F>=C+2,D>=C+2,F>=B+1,D>=B+1,F>=A+1,D>=A+1,I>=3,H>=3,C>=2,B>=2,G=1,E=1] 
* CE 70: case_6(A,B,C) = 11+ tableMake(D,E,C):[multiple([48,49],[[53],[52],[51],[50]])]+ tableMake(F,E,C):[multiple([48,49],[[53],[52],[51],[50]])]+ concat(G,H):[[25],24]
     [B>=E+1,F>=B+1,D>=B+1,F>=A+1,D>=A+1,H>=3,G>=3,C>=2,E>=2] 
* CE 71: case_6(A,B,C) = 11+ tableMake(D,E,C):[53]+ tableMake(F,G,C):[53]+ concat(H,I):[[25],24]
     [F>=A+1,D>=A+1,I>=3,H>=3,C>=2,F>=3,D>=3,G=1,E=1,B=2] 
* CE 72: case_6(A,B,C) = 11+ tableMake(D,E,C):[53]+ tableMake(F,G,C):[52]+ concat(H,I):[[25],24]
     [F>=A+1,D>=A+1,I>=3,H>=3,C>=3,F>=3,D>=3,G=1,E=1,B=2] 
* CE 73: case_6(A,B,C) = 11+ tableMake(D,E,C):[53]+ tableMake(F,G,C):[51]+ concat(H,I):[[25],24]
     [F>=C+1,F>=A+1,D>=A+1,I>=3,H>=3,C>=2,D>=3,G=1,E=1,B=2] 
* CE 74: case_6(A,B,C) = 11+ tableMake(D,E,C):[53]+ tableMake(F,G,C):[50]+ concat(H,I):[[25],24]
     [F>=C+2,F>=A+1,D>=A+1,I>=3,H>=3,C>=2,D>=3,G=1,E=1,B=2] 
* CE 75: case_6(A,B,C) = 11+ tableMake(D,E,C):[52]+ tableMake(F,G,C):[53]+ concat(H,I):[[25],24]
     [F>=A+1,D>=A+1,I>=3,H>=3,C>=3,F>=3,D>=3,G=1,E=1,B=2] 
* CE 76: case_6(A,B,C) = 11+ tableMake(D,E,C):[52]+ tableMake(F,G,C):[52]+ concat(H,I):[[25],24]
     [F>=A+1,D>=A+1,I>=3,H>=3,C>=3,F>=3,D>=3,G=1,E=1,B=2] 
* CE 77: case_6(A,B,C) = 11+ tableMake(D,E,C):[52]+ tableMake(F,G,C):[51]+ concat(H,I):[[25],24]
     [F>=C+1,F>=A+1,D>=A+1,I>=3,H>=3,C>=3,D>=3,G=1,E=1,B=2] 
* CE 78: case_6(A,B,C) = 11+ tableMake(D,E,C):[52]+ tableMake(F,G,C):[50]+ concat(H,I):[[25],24]
     [F>=C+2,F>=A+1,D>=A+1,I>=3,H>=3,C>=3,D>=3,G=1,E=1,B=2] 
* CE 79: case_6(A,B,C) = 11+ tableMake(D,E,C):[51]+ tableMake(F,G,C):[53]+ concat(H,I):[[25],24]
     [D>=C+1,F>=A+1,D>=A+1,I>=3,H>=3,C>=2,F>=3,G=1,E=1,B=2] 
* CE 80: case_6(A,B,C) = 11+ tableMake(D,E,C):[51]+ tableMake(F,G,C):[52]+ concat(H,I):[[25],24]
     [D>=C+1,F>=A+1,D>=A+1,I>=3,H>=3,C>=3,F>=3,G=1,E=1,B=2] 
* CE 81: case_6(A,B,C) = 11+ tableMake(D,E,C):[51]+ tableMake(F,G,C):[51]+ concat(H,I):[[25],24]
     [F>=C+1,D>=C+1,F>=A+1,D>=A+1,I>=3,H>=3,C>=2,G=1,E=1,B=2] 
* CE 82: case_6(A,B,C) = 11+ tableMake(D,E,C):[51]+ tableMake(F,G,C):[50]+ concat(H,I):[[25],24]
     [F>=C+2,D>=C+1,F>=A+1,D>=A+1,I>=3,H>=3,C>=2,G=1,E=1,B=2] 
* CE 83: case_6(A,B,C) = 11+ tableMake(D,E,C):[50]+ tableMake(F,G,C):[53]+ concat(H,I):[[25],24]
     [D>=C+2,F>=A+1,D>=A+1,I>=3,H>=3,C>=2,F>=3,G=1,E=1,B=2] 
* CE 84: case_6(A,B,C) = 11+ tableMake(D,E,C):[50]+ tableMake(F,G,C):[52]+ concat(H,I):[[25],24]
     [D>=C+2,F>=A+1,D>=A+1,I>=3,H>=3,C>=3,F>=3,G=1,E=1,B=2] 
* CE 85: case_6(A,B,C) = 11+ tableMake(D,E,C):[50]+ tableMake(F,G,C):[51]+ concat(H,I):[[25],24]
     [F>=C+1,D>=C+2,F>=A+1,D>=A+1,I>=3,H>=3,C>=2,G=1,E=1,B=2] 
* CE 86: case_6(A,B,C) = 11+ tableMake(D,E,C):[50]+ tableMake(F,G,C):[50]+ concat(H,I):[[25],24]
     [F>=C+2,D>=C+2,F>=A+1,D>=A+1,I>=3,H>=3,C>=2,G=1,E=1,B=2] 
* CE 87: case_6(A,B,C) = 11+ tableMake(D,E,C):[multiple([48,49],[[53],[52],[51],[50]])]+ tableMake(F,E,C):[multiple([48,49],[[53],[52],[51],[50]])]+ concat(G,H):[[25],24]
     [F>=A+1,D>=A+1,H>=3,G>=3,C>=2,E>=2,F>=3,D>=3,E+1=B] 
* CE 88: case_6(A,B,C) = 8+ aux(D,A):[[46,47],45]+ eval(A,C):[35]
     [C>=2,A>=3,D=1,B=1] 
* CE 89: case_6(A,B,C) = 8+ aux(D,A):[[46,47],45]+ eval(A,C):[34]
     [A>=C+1,C>=2,D=1,B=1] 
* CE 90: case_6(A,B,C) = 8+ aux(D,A):[[46,47],45]+ eval(A,C):[33]
     [A>=C+2,C>=2,D=1,B=1] 
* CE 91: case_6(A,B,C) = 8+ aux(D,A):[[46,47],45]+ eval(A,C):[multiple([37,38,39,40,41,42,43,44],[[36],[35],[34],[33]])]
     [C>=3,A>=2,D=1,B=1] 
* CE 92: case_6(A,B,C) = 8+ aux(D,E):[45]+ eval(F,C):[36]
     [C>=2,F=1,E=1,D=1,B=1,A=1] 
* CE 93: case_6(A,B,C) = 8+ aux(D,E):[45]+ eval(F,C):[multiple([37,38,39,40,41,42,43,44],[[36],[35],[34],[33]])]
     [C>=3,F=1,E=1,D=1,B=1,A=1] 

### Cost equations --> "Loop" of case_6/3 
* CEs [87] --> Loop 54 
* CEs [70] --> Loop 55 
* CEs [67] --> Loop 56 
* CEs [63] --> Loop 57 
* CEs [61] --> Loop 58 
* CEs [60] --> Loop 59 
* CEs [59] --> Loop 60 
* CEs [58] --> Loop 61 
* CEs [55] --> Loop 62 
* CEs [69] --> Loop 63 
* CEs [68] --> Loop 64 
* CEs [66] --> Loop 65 
* CEs [65] --> Loop 66 
* CEs [64] --> Loop 67 
* CEs [62] --> Loop 68 
* CEs [57] --> Loop 69 
* CEs [56] --> Loop 70 
* CEs [54] --> Loop 71 
* CEs [84] --> Loop 72 
* CEs [80] --> Loop 73 
* CEs [78] --> Loop 74 
* CEs [77] --> Loop 75 
* CEs [76] --> Loop 76 
* CEs [75] --> Loop 77 
* CEs [72] --> Loop 78 
* CEs [86] --> Loop 79 
* CEs [85] --> Loop 80 
* CEs [83] --> Loop 81 
* CEs [82] --> Loop 82 
* CEs [81] --> Loop 83 
* CEs [79] --> Loop 84 
* CEs [74] --> Loop 85 
* CEs [73] --> Loop 86 
* CEs [71] --> Loop 87 
* CEs [90] --> Loop 88 
* CEs [89] --> Loop 89 
* CEs [88] --> Loop 90 
* CEs [91] --> Loop 91 
* CEs [93] --> Loop 92 
* CEs [92] --> Loop 93 

#### Loops of case_6/3 
* Loop 54: case_6(A,B,C) [C>=2,B>=3] 
* Loop 55: case_6(A,B,C) [C>=2,B>=3] 
* Loop 56: case_6(A,B,C) [C>=3,B>=2] 
* Loop 57: case_6(A,B,C) [C>=3,B>=2] 
* Loop 58: case_6(A,B,C) [C>=3,B>=2] 
* Loop 59: case_6(A,B,C) [C>=3,B>=2] 
* Loop 60: case_6(A,B,C) [C>=3,B>=2] 
* Loop 61: case_6(A,B,C) [C>=3,B>=2] 
* Loop 62: case_6(A,B,C) [C>=3,B>=2] 
* Loop 63: case_6(A,B,C) [C>=2,B>=2] 
* Loop 64: case_6(A,B,C) [C>=2,B>=2] 
* Loop 65: case_6(A,B,C) [C>=2,B>=2] 
* Loop 66: case_6(A,B,C) [C>=2,B>=2] 
* Loop 67: case_6(A,B,C) [C>=2,B>=2] 
* Loop 68: case_6(A,B,C) [C>=2,B>=2] 
* Loop 69: case_6(A,B,C) [C>=2,B>=2] 
* Loop 70: case_6(A,B,C) [C>=2,B>=2] 
* Loop 71: case_6(A,B,C) [C>=2,B>=2] 
* Loop 72: case_6(A,B,C) [C>=3,B=2] 
* Loop 73: case_6(A,B,C) [C>=3,B=2] 
* Loop 74: case_6(A,B,C) [C>=3,B=2] 
* Loop 75: case_6(A,B,C) [C>=3,B=2] 
* Loop 76: case_6(A,B,C) [C>=3,B=2] 
* Loop 77: case_6(A,B,C) [C>=3,B=2] 
* Loop 78: case_6(A,B,C) [C>=3,B=2] 
* Loop 79: case_6(A,B,C) [C>=2,B=2] 
* Loop 80: case_6(A,B,C) [C>=2,B=2] 
* Loop 81: case_6(A,B,C) [C>=2,B=2] 
* Loop 82: case_6(A,B,C) [C>=2,B=2] 
* Loop 83: case_6(A,B,C) [C>=2,B=2] 
* Loop 84: case_6(A,B,C) [C>=2,B=2] 
* Loop 85: case_6(A,B,C) [C>=2,B=2] 
* Loop 86: case_6(A,B,C) [C>=2,B=2] 
* Loop 87: case_6(A,B,C) [C>=2,B=2] 
* Loop 88: case_6(A,B,C) [A>=C+2,C>=2,B=1] 
* Loop 89: case_6(A,B,C) [A>=C+1,C>=2,B=1] 
* Loop 90: case_6(A,B,C) [C>=2,A>=3,B=1] 
* Loop 91: case_6(A,B,C) [C>=3,A>=2,B=1] 
* Loop 92: case_6(A,B,C) [C>=3,B=1,A=1] 
* Loop 93: case_6(A,B,C) [C>=2,B=1,A=1] 

### Ranking functions of CR case_6(A,B,C) 

#### Partial ranking functions of CR case_6(A,B,C) 


### Resulting Chains:case_6(A,B,C) 
* [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]


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

#### Cost of loops [25] 

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

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

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


#### Cost of chains of and_op(A,B):
* Chain [27]: 0
  with precondition: [A=0] 

* Chain [26]: 0
  with precondition: [A=1] 


#### Cost of loops [28] 

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

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

#### Cost of chains of assoc(A,B):
* Chain [[28],30]: 8*it(28)+3
  Such that:it(28) =< B-2

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

* Chain [[28],29]: 8*it(28)+7
  Such that:it(28) =< -A+B-2

  with precondition: [A>=1,B>=A+3] 

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

* Chain [29]: 7
  with precondition: [A>=1,B>=A+2] 


#### Cost of chains of or(A,B):
* Chain [32]: 0
  with precondition: [A=0] 

* Chain [31]: 0
  with precondition: [A=1] 


#### Cost of loops [37,38,39,40,41,42,43,44] 

 * loop 37:eval(A,B) -> [eval(A',B'),eval(A'2,B'2)] 
7
 * loop 38:eval(A,B) -> [eval(A',B'),eval(A'2,B'2)] 
7
 * loop 39:eval(A,B) -> [eval(A',B'),eval(A'2,B'2)] 
8
 * loop 40:eval(A,B) -> [eval(A',B'),eval(A'2,B'2)] 
8
 * loop 41:eval(A,B) -> [eval(A',B'),eval(A'2,B'2)] 
7
 * loop 42:eval(A,B) -> [eval(A',B'),eval(A'2,B'2)] 
7
 * loop 43:eval(A,B) -> [eval(A',B'),eval(A'2,B'2)] 
8
 * loop 44:eval(A,B) -> [eval(A',B'),eval(A'2,B'2)] 
8
#### Cost of phase [37,38,39,40,41,42,43,44]:eval(A,B) -> [] 
60*it(37)+10*it([33])+10*it([34])+6*it([35])+6*it([36])+8*s(3)+8*s(4)+0
#### Cost of chains of eval(A,B):
* Chain [36]: 6
  with precondition: [A=1,B>=2] 

* Chain [35]: 8*s(1)+6
  Such that:s(1) =< A-2

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

* Chain [34]: 10
  with precondition: [B>=2,A>=B+1] 

* Chain [33]: 8*s(2)+10
  Such that:s(2) =< A-B-1

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

* Chain [multiple([37,38,39,40,41,42,43,44],[[36],[35],[34],[33]])]: 60*it(37)+10*it([33])+10*it([34])+6*it([35])+6*it([36])+8*s(3)+8*s(4)+0
  with precondition: [A>=1,B>=3] 


#### Cost of loops [46,47] 

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

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

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

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


#### Cost of loops [48,49] 

 * loop 48:tableMake(A,B,C) -> [tableMake(A',B',C'),tableMake(A'2,B'2,C'2)] 
5*s(23)+14
 * loop 49:tableMake(A,B,C) -> [tableMake(A',B',C'),tableMake(A'2,B'2,C'2)] 
5*s(25)+14
#### Cost of phase [48,49]:tableMake(A,B,C) -> [] 
14*it(48)+14*it(49)+21*it([50])+21*it([51])+11*it([52])+17*it([53])+118*s(26)+5*s(28)+5*s(29)+8*s(30)+5*s(31)+5*s(32)+5*s(34)+5*s(35)+5*s(36)+5*s(37)+8*s(38)+0
#### Cost of chains of tableMake(A,B,C):
* Chain [53]: 5*s(5)+5*s(6)+8*s(7)+17
  Such that:s(7) =< A-2
s(5)+s(6) =< A-1

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

* Chain [52]: 5*s(8)+5*s(9)+108*s(10)+11
  Such that:s(8)+s(9) =< A-1

  with precondition: [B=1,A>=3,C>=3] 

* Chain [51]: 5*s(17)+5*s(18)+21
  Such that:s(17)+s(18) =< A-1

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

* Chain [50]: 5*s(19)+5*s(20)+8*s(21)+21
  Such that:s(19)+s(20) =< A-1
s(21) =< A-C-1

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

* Chain [multiple([48,49],[[53],[52],[51],[50]])]: 14*it(48)+14*it(49)+21*it([50])+21*it([51])+11*it([52])+17*it([53])+118*s(26)+5*s(28)+5*s(29)+8*s(30)+5*s(31)+5*s(32)+5*s(34)+5*s(35)+5*s(36)+5*s(37)+8*s(38)+0
  with precondition: [A>=3,B>=2,C>=2] 


#### Cost of chains of case_6(A,B,C):
* Chain [93]: 16
  with precondition: [A=1,B=1,C>=2] 

* Chain [92]: 108*s(39)+10
  with precondition: [A=1,B=1,C>=3] 

* Chain [91]: 5*s(46)+5*s(47)+108*s(48)+10
  Such that:s(46)+s(47) =< A-1

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

* Chain [90]: 5*s(55)+5*s(56)+8*s(57)+16
  Such that:s(57) =< A-2
s(55)+s(56) =< A-1

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

* Chain [89]: 5*s(58)+5*s(59)+20
  Such that:s(58)+s(59) =< A-1

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

* Chain [88]: 5*s(60)+5*s(61)+8*s(62)+20
  Such that:s(60)+s(61) =< A-1
s(62) =< A-C-1

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

* Chain [87]: 41*s(63)+47
  with precondition: [B=2,C>=2] 

* Chain [86]: 33*s(70)+51
  with precondition: [B=2,C>=2] 

* Chain [85]: 41*s(76)+51
  with precondition: [B=2,C>=2] 

* Chain [84]: 33*s(83)+51
  with precondition: [B=2,C>=2] 

* Chain [83]: 25*s(89)+55
  with precondition: [B=2,C>=2] 

* Chain [82]: 33*s(94)+55
  with precondition: [B=2,C>=2] 

* Chain [81]: 41*s(100)+51
  with precondition: [B=2,C>=2] 

* Chain [80]: 33*s(107)+55
  with precondition: [B=2,C>=2] 

* Chain [79]: 41*s(113)+55
  with precondition: [B=2,C>=2] 

* Chain [78]: 141*s(120)+41
  with precondition: [B=2,C>=3] 

* Chain [77]: 141*s(127)+41
  with precondition: [B=2,C>=3] 

* Chain [76]: 241*s(134)+35
  with precondition: [B=2,C>=3] 

* Chain [75]: 133*s(141)+45
  with precondition: [B=2,C>=3] 

* Chain [74]: 141*s(147)+45
  with precondition: [B=2,C>=3] 

* Chain [73]: 133*s(154)+45
  with precondition: [B=2,C>=3] 

* Chain [72]: 141*s(160)+45
  with precondition: [B=2,C>=3] 

* Chain [71]: 41*s(167)+47
  with precondition: [B>=2,C>=2] 

* Chain [70]: 33*s(174)+51
  with precondition: [B>=2,C>=2] 

* Chain [69]: 41*s(180)+51
  with precondition: [B>=2,C>=2] 

* Chain [68]: 33*s(187)+51
  with precondition: [B>=2,C>=2] 

* Chain [67]: 25*s(193)+55
  with precondition: [B>=2,C>=2] 

* Chain [66]: 33*s(198)+55
  with precondition: [B>=2,C>=2] 

* Chain [65]: 41*s(204)+51
  with precondition: [B>=2,C>=2] 

* Chain [64]: 33*s(211)+55
  with precondition: [B>=2,C>=2] 

* Chain [63]: 41*s(217)+55
  with precondition: [B>=2,C>=2] 

* Chain [62]: 141*s(224)+41
  with precondition: [B>=2,C>=3] 

* Chain [61]: 141*s(231)+41
  with precondition: [B>=2,C>=3] 

* Chain [60]: 241*s(238)+35
  with precondition: [B>=2,C>=3] 

* Chain [59]: 133*s(245)+45
  with precondition: [B>=2,C>=3] 

* Chain [58]: 141*s(251)+45
  with precondition: [B>=2,C>=3] 

* Chain [57]: 133*s(258)+45
  with precondition: [B>=2,C>=3] 

* Chain [56]: 141*s(264)+45
  with precondition: [B>=2,C>=3] 

* Chain [55]: 549*s(271)+13
  with precondition: [B>=3,C>=2] 

* Chain [54]: 549*s(306)+13
  with precondition: [B>=3,C>=2] 


Closed-form bounds of case_6(A,B,C): 
-------------------------------------
* Chain [93] with precondition: [A=1,B=1,C>=2] 
    - Lower bound: 16 
    - Complexity: constant
 * Chain [92] with precondition: [A=1,B=1,C>=3] 
    - Lower bound: 10 
    - Complexity: constant
 * Chain [91] with precondition: [B=1,A>=2,C>=3] 
    - Lower bound: 10 
    - Complexity: constant
 * Chain [90] with precondition: [B=1,A>=3,C>=2] 
    - Lower bound: 16 
    - Complexity: constant
 * Chain [89] with precondition: [B=1,C>=2,A>=C+1] 
    - Lower bound: 20 
    - Complexity: constant
 * Chain [88] with precondition: [B=1,C>=2,A>=C+2] 
    - Lower bound: 20 
    - Complexity: constant
 * Chain [87] with precondition: [B=2,C>=2] 
    - Lower bound: 47 
    - Complexity: constant
 * Chain [86] with precondition: [B=2,C>=2] 
    - Lower bound: 51 
    - Complexity: constant
 * Chain [85] with precondition: [B=2,C>=2] 
    - Lower bound: 51 
    - Complexity: constant
 * Chain [84] with precondition: [B=2,C>=2] 
    - Lower bound: 51 
    - Complexity: constant
 * Chain [83] with precondition: [B=2,C>=2] 
    - Lower bound: 55 
    - Complexity: constant
 * Chain [82] with precondition: [B=2,C>=2] 
    - Lower bound: 55 
    - Complexity: constant
 * Chain [81] with precondition: [B=2,C>=2] 
    - Lower bound: 51 
    - Complexity: constant
 * Chain [80] with precondition: [B=2,C>=2] 
    - Lower bound: 55 
    - Complexity: constant
 * Chain [79] with precondition: [B=2,C>=2] 
    - Lower bound: 55 
    - Complexity: constant
 * Chain [78] with precondition: [B=2,C>=3] 
    - Lower bound: 41 
    - Complexity: constant
 * Chain [77] with precondition: [B=2,C>=3] 
    - Lower bound: 41 
    - Complexity: constant
 * Chain [76] with precondition: [B=2,C>=3] 
    - Lower bound: 35 
    - Complexity: constant
 * Chain [75] with precondition: [B=2,C>=3] 
    - Lower bound: 45 
    - Complexity: constant
 * Chain [74] with precondition: [B=2,C>=3] 
    - Lower bound: 45 
    - Complexity: constant
 * Chain [73] with precondition: [B=2,C>=3] 
    - Lower bound: 45 
    - Complexity: constant
 * Chain [72] with precondition: [B=2,C>=3] 
    - Lower bound: 45 
    - Complexity: constant
 * Chain [71] with precondition: [B>=2,C>=2] 
    - Lower bound: 47 
    - Complexity: constant
 * Chain [70] with precondition: [B>=2,C>=2] 
    - Lower bound: 51 
    - Complexity: constant
 * Chain [69] with precondition: [B>=2,C>=2] 
    - Lower bound: 51 
    - Complexity: constant
 * Chain [68] with precondition: [B>=2,C>=2] 
    - Lower bound: 51 
    - Complexity: constant
 * Chain [67] with precondition: [B>=2,C>=2] 
    - Lower bound: 55 
    - Complexity: constant
 * Chain [66] with precondition: [B>=2,C>=2] 
    - Lower bound: 55 
    - Complexity: constant
 * Chain [65] with precondition: [B>=2,C>=2] 
    - Lower bound: 51 
    - Complexity: constant
 * Chain [64] with precondition: [B>=2,C>=2] 
    - Lower bound: 55 
    - Complexity: constant
 * Chain [63] with precondition: [B>=2,C>=2] 
    - Lower bound: 55 
    - Complexity: constant
 * Chain [62] with precondition: [B>=2,C>=3] 
    - Lower bound: 41 
    - Complexity: constant
 * Chain [61] with precondition: [B>=2,C>=3] 
    - Lower bound: 41 
    - Complexity: constant
 * Chain [60] with precondition: [B>=2,C>=3] 
    - Lower bound: 35 
    - Complexity: constant
 * Chain [59] with precondition: [B>=2,C>=3] 
    - Lower bound: 45 
    - Complexity: constant
 * Chain [58] with precondition: [B>=2,C>=3] 
    - Lower bound: 45 
    - Complexity: constant
 * Chain [57] with precondition: [B>=2,C>=3] 
    - Lower bound: 45 
    - Complexity: constant
 * Chain [56] with precondition: [B>=2,C>=3] 
    - Lower bound: 45 
    - Complexity: constant
 * Chain [55] with precondition: [B>=3,C>=2] 
    - Lower bound: 13 
    - Complexity: constant
 * Chain [54] with precondition: [B>=3,C>=2] 
    - Lower bound: 13 
    - Complexity: constant
 
### Partitioned lower bound of case_6(A,B,C): 
* 10 
 if [B=1,C>=3,A>=C+2]
 or [A=2,B=1,C>=3]
 or [A=1,B=1,C>=3]
 or [B=1,A=C+1,A>=4]
 or [B=1,A>=3,C>=A]
* 13 
 if [B>=3,C>=2]
* 16 
 if [B=1,C=2,A>=3]
 or [A=1,B=1,C=2]
* 35 
 if [B=2,C>=3]
* 47 
 if [B=2,C=2]
Possible lower bounds : [10,13,16,35,47]
Maximum lower bound complexity: constant
* Total analysis performed in 558 ms.