Abs program loaded in 3 ms.

Rule based representation generated in 0 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 3 ms.
sabu_memo_table_1(case_2,[A,B,C,D],[1*A+ -1*C=0,1*B+ -1*D=0],0,0)
sabu_memo_table_1(case_2,[A,B,C,D],[-1*A+1*C>=0],0,1)
sabu_memo_table_1(case_2,[A,B,C,D],[],0,2)
sabu_memo_table_1(case_1,[A,B,C,D,E,F],[1*A+ -1*E=0,1*B+ -1*F=0],0,0)
sabu_memo_table_1(case_1,[A,B,C,D,E,F],[-1*A+1*E>=0],0,1)
sabu_memo_table_1(case_1,[A,B,C,D,E,F],[],0,2)
sabu_memo_table_1(not,[A,B],[1*B=1,1*A=0],0,0)
sabu_memo_table_1(not,[A,B],[1*B>=0,-1*B>= -1,1*A+1*B=1],0,1)
sabu_memo_table_1(case_0,[A,B,C,D,E,F,G],[1*F=1],0,0)
sabu_memo_table_1(eval2,[A,B,C,D,E,F,G],[1*F>=0,1*F=1],0,0)
sabu_memo_table_1(case_0,[A,B,C,D,E,F,G],[1*F>=1,-1*F>= -2],1,1)
sabu_memo_table_1(eval2,[A,B,C,D,E,F,G],[-1*F>= -2,1*F>=1],2,1)
sabu_memo_table_1(case_0,[A,B,C,D,E,F,G],[1*F>=1,-1*F>= -3],3,2)
sabu_memo_table_1(eval2,[A,B,C,D,E,F,G],[-1*F>= -3,1*F>=1],4,2)
sabu_memo_table_1(case_0,[A,B,C,D,E,F,G],[1*F>=1,-1*F>= -4],5,3)
sabu_memo_table_1(eval2,[A,B,C,D,E,F,G],[-1*F>= -4,1*F>=1],6,3)
sabu_memo_table_1(case_0,[A,B,C,D,E,F,G],[1*F>=1],7,0)
sabu_memo_table_1(eval2,[A,B,C,D,E,F,G],[1*F>=1],8,0)
sabu_memo_table_1(start,[A,B,C,D,E,F],[1*F>=0,1*F>=1],0,0)
sabu_memo_table_1(start,[],[],0,0)
:- dynamic sabu_memo_table_1/5.

sabu_memo_table_1(case_2, [_, _, _, _], [], 0, 2).
sabu_memo_table_1(case_1, [_, _, _, _, _, _], [], 0, 2).
sabu_memo_table_1(not, [B, A], [1*A>=0, -1*A>= -1, 1*B+1*A=1], 0, 1).
sabu_memo_table_1(case_0, [_, _, _, _, _, A, _], [1*A>=1], 7, 0).
sabu_memo_table_1(eval2, [_, _, _, _, _, A, _], [1*A>=1], 8, 0).
sabu_memo_table_1(start, [_, _, _, _, _, A], [1*A>=0, 1*A>=1], 0, 0).
sabu_memo_table_1(start, [], [], 0, 0).


Size analysis performed in 5 ms.

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

Generated 36 equations 

Cost relation system solved by PUBS in 178 ms.

Method start terminates?: YES

 - a_1: size of a wrt. Rat
 - valA_1: size of valA wrt. Bool
 - b_1: size of b wrt. Rat
 - valB_1: size of valB wrt. Bool
 - expr_1: size of expr wrt. Rat
 - expr_2: size of expr wrt. BoolExpr
UB for start(a_1,valA_1,b_1,valB_1,expr_1,expr_2) = pow(2,nat(expr_2))


Method start terminates?: YES

 - a_1: size of a wrt. Rat
 - valA_1: size of valA wrt. Bool
 - b_1: size of b wrt. Rat
 - valB_1: size of valB wrt. Bool
 - expr_1: size of expr wrt. Rat
 - expr_2: size of expr wrt. BoolExpr
UB for start(a_1,valA_1,b_1,valB_1,expr_1,expr_2) = pow(2,nat(expr_2))


Method start terminates?: YES

UB for start(a_1,valA_1,b_1,valB_1,expr_1,expr_2) = pow(2,nat(expr_2))


Method start terminates?: YES

UB for start(a_1,valA_1,b_1,valB_1,expr_1,expr_2) = pow(2,nat(expr_2))

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

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

#### Computed strongly connected components 
0. non_recursive  : [case_2/3]
1. non_recursive  : [case_1/5]
2. non_recursive  : [neg/1]
3. non_recursive  : [not/1]
4. recursive [non_tail,multiple] : [case_0/6,eval2/6]
6. non_recursive  : [start/6]
* The entry case_0/6 is not a cutpoint so it becomes a new SCC 6
Warning: the following predicates are never called:[and_op/2,eq/2,geq/2,gt/2,leq/2,lt/2,maxNorm/2,neq/2,or/2,start/0]

#### Obtained direct recursion through partial evaluation 
0. SCC is partially evaluated into case_2/3
1. SCC is partially evaluated into case_1/5
2. SCC is partially evaluated into neg/1
3. SCC is completely evaluated into other SCCs
4. SCC is partially evaluated into eval2/6
6. SCC is partially evaluated into case_0/6

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

### Specialization of cost equations case_2/3 
* CE 14 is refined into CE [17] 
* CE 15 is refined into CE [18] 
* CE 16 is refined into CE [19] 


#### Refined cost equations case_2/3 
* CE 17: case_2(A,B,C) = 2
     [A>=C+1] 
* CE 18: case_2(A,B,C) = 2
     [C>=A+1] 
* CE 19: case_2(A,B,A) = 1
     [] 

### Cost equations --> "Loop" of case_2/3 
* CEs [17] --> Loop 17 
* CEs [18] --> Loop 18 
* CEs [19] --> Loop 19 

#### Loops of case_2/3 
* Loop 17: case_2(A,B,C) [A>=C+1] 
* Loop 18: case_2(A,B,C) [C>=A+1] 
* Loop 19: case_2(A,B,A) [] 

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

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


### Resulting Chains:case_2(A,B,C) 
* [19]
* [18]
* [17]


### Specialization of cost equations case_1/5 
* CE 11 is refined into CE [20,21,22] 
* CE 12 is refined into CE [23,24,25] 
* CE 13 is refined into CE [26] 


#### Refined cost equations case_1/5 
* CE 20: case_1(A,B,C,D,C) = 2+ case_2(C,D,C):[19]
     [A>=C+1] 
* CE 21: case_1(A,B,C,D,E) = 2+ case_2(C,D,E):[18]
     [A>=E+1,E>=C+1] 
* CE 22: case_1(A,B,C,D,E) = 2+ case_2(C,D,E):[17]
     [C>=E+1,A>=E+1] 
* CE 23: case_1(A,B,C,D,C) = 2+ case_2(C,D,C):[19]
     [C>=A+1] 
* CE 24: case_1(A,B,C,D,E) = 2+ case_2(C,D,E):[18]
     [E>=C+1,E>=A+1] 
* CE 25: case_1(A,B,C,D,E) = 2+ case_2(C,D,E):[17]
     [C>=E+1,E>=A+1] 
* CE 26: case_1(A,B,C,D,A) = 1
     [] 

### Cost equations --> "Loop" of case_1/5 
* CEs [22] --> Loop 20 
* CEs [21] --> Loop 21 
* CEs [25] --> Loop 22 
* CEs [24] --> Loop 23 
* CEs [20] --> Loop 24 
* CEs [23] --> Loop 25 
* CEs [26] --> Loop 26 

#### Loops of case_1/5 
* Loop 20: case_1(A,B,C,D,E) [C>=E+1,A>=E+1] 
* Loop 21: case_1(A,B,C,D,E) [A>=E+1,E>=C+1] 
* Loop 22: case_1(A,B,C,D,E) [C>=E+1,E>=A+1] 
* Loop 23: case_1(A,B,C,D,E) [E>=C+1,E>=A+1] 
* Loop 24: case_1(A,B,C,D,C) [A>=C+1] 
* Loop 25: case_1(A,B,C,D,C) [C>=A+1] 
* Loop 26: case_1(A,B,C,D,A) [] 

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

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


### Resulting Chains:case_1(A,B,C,D,E) 
* [26]
* [25]
* [24]
* [23]
* [22]
* [21]
* [20]


### Specialization of cost equations neg/1 
* CE 9 is refined into CE [27] 
* CE 10 is refined into CE [28] 


#### Refined cost equations neg/1 
* CE 27: neg(A) = 0
     [A=1] 
* CE 28: neg(A) = 0
     [A=0] 

### Cost equations --> "Loop" of neg/1 
* CEs [27] --> Loop 27 
* CEs [28] --> Loop 28 

#### Loops of neg/1 
* Loop 27: neg(A) [A=1] 
* Loop 28: neg(A) [A=0] 

### Ranking functions of CR neg(A) 

#### Partial ranking functions of CR neg(A) 


### Resulting Chains:neg(A) 
* [28]
* [27]


### Specialization of cost equations eval2/6 
* CE 8 is refined into CE [29,30,31,32,33,34,35] 
* CE 7 is refined into CE [36,37] 
* CE 6 is refined into CE [38] 
* CE 5 is refined into CE [39] 


#### Refined cost equations eval2/6 
* CE 29: eval2(A,B,C,D,A,E) = 3+ case_1(A,B,C,D,A):[26]
     [E=1] 
* CE 30: eval2(A,B,C,D,C,E) = 3+ case_1(A,B,C,D,C):[25]
     [C>=A+1,E=1] 
* CE 31: eval2(A,B,C,D,C,E) = 3+ case_1(A,B,C,D,C):[24]
     [A>=C+1,E=1] 
* CE 32: eval2(A,B,C,D,E,F) = 3+ case_1(A,B,C,D,E):[23]
     [E>=C+1,E>=A+1,F=1] 
* CE 33: eval2(A,B,C,D,E,F) = 3+ case_1(A,B,C,D,E):[22]
     [C>=E+1,E>=A+1,F=1] 
* CE 34: eval2(A,B,C,D,E,F) = 3+ case_1(A,B,C,D,E):[21]
     [A>=E+1,E>=C+1,F=1] 
* CE 35: eval2(A,B,C,D,E,F) = 3+ case_1(A,B,C,D,E):[20]
     [C>=E+1,A>=E+1,F=1] 
* CE 36: eval2(A,B,C,D,E,F) = 6+ eval2(A,B,C,D,E,G)+ neg(H):[28]
     [G>=1,G+1=F,H=0] 
* CE 37: eval2(A,B,C,D,E,F) = 6+ eval2(A,B,C,D,E,G)+ neg(H):[27]
     [G>=1,G+1=F,H=1] 
* CE 38: eval2(A,B,C,D,E,F) = 7+ eval2(A,B,C,D,G,H)+ eval2(A,B,C,D,I,J)
     [E>=I,E>=G,J>=1,H>=1,H+J+1=F] 
* CE 39: eval2(A,B,C,D,E,F) = 8+ eval2(A,B,C,D,G,H)+ eval2(A,B,C,D,I,J)
     [E>=I,E>=G,J>=1,H>=1,H+J+1=F] 

### Cost equations --> "Loop" of eval2/6 
* CEs [39] --> Loop 29 
* CEs [38] --> Loop 30 
* CEs [37] --> Loop 31 
* CEs [36] --> Loop 32 
* CEs [35] --> Loop 33 
* CEs [34] --> Loop 34 
* CEs [33] --> Loop 35 
* CEs [32] --> Loop 36 
* CEs [31] --> Loop 37 
* CEs [30] --> Loop 38 
* CEs [29] --> Loop 39 

#### Loops of eval2/6 
* Loop 29: eval2(A,B,C,D,E,F)->  eval2(A,B,C,D,E',F')  eval2(A,B,C,D,E'2,F'2)
                  [E>=E'2,E>=E',F'2>=1,F'>=1,F'+F'2+1=F] 
* Loop 30: eval2(A,B,C,D,E,F)->  eval2(A,B,C,D,E',F')  eval2(A,B,C,D,E'2,F'2)
                  [E>=E'2,E>=E',F'2>=1,F'>=1,F'+F'2+1=F] 
* Loop 31: eval2(A,B,C,D,E,F)->  eval2(A,B,C,D,E,F')
                  [F'>=1,F'+1=F] 
* Loop 32: eval2(A,B,C,D,E,F)->  eval2(A,B,C,D,E,F')
                  [F'>=1,F'+1=F] 
* Loop 33: eval2(A,B,C,D,E,F) [C>=E+1,A>=E+1,F=1] 
* Loop 34: eval2(A,B,C,D,E,F) [A>=E+1,E>=C+1,F=1] 
* Loop 35: eval2(A,B,C,D,E,F) [C>=E+1,E>=A+1,F=1] 
* Loop 36: eval2(A,B,C,D,E,F) [E>=C+1,E>=A+1,F=1] 
* Loop 37: eval2(A,B,C,D,C,E) [A>=C+1,E=1] 
* Loop 38: eval2(A,B,C,D,C,E) [C>=A+1,E=1] 
* Loop 39: eval2(A,B,C,D,A,E) [E=1] 

### Ranking functions of CR eval2(A,B,C,D,E,F) 
* RF of phase [29,30,31,32]: [F-1]

#### Partial ranking functions of CR eval2(A,B,C,D,E,F) 
* Partial RF of phase [29,30,31,32]:
  - RF of loop [29:1,29:2,30:1,30:2]:
    F/2-1
  - RF of loop [31:1,32:1]:
    F-1


### Resulting Chains:eval2(A,B,C,D,E,F) 
* [39]
* [38]
* [37]
* [36]
* [35]
* [34]
* [33]
* [multiple([29,30,31,32],[[39],[38],[37],[36],[35],[34],[33]])]


### Specialization of cost equations case_0/6 
* CE 2 is refined into CE [40,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,89,90,91,92,93,94,95] 
* CE 1 is refined into CE [96,97,98,99,100,101,102,103,104,105,106,107,108,109,110,111,112,113,114,115,116,117,118,119,120,121,122,123,124,125,126,127,128,129,130,131,132,133,134,135,136,137,138,139,140,141,142,143,144,145,146,147,148,149,150,151] 
* CE 3 is refined into CE [152,153,154,155,156,157,158,159,160,161,162,163,164,165,166,167] 
* CE 4 is refined into CE [168,169,170,171,172,173,174] 


#### Refined cost equations case_0/6 
* CE 40: case_0(A,B,C,D,E,F) = 6+ eval2(A,B,C,D,A,G):[39]+ eval2(A,B,C,D,A,H):[39]
     [E>=A,H=1,G=1,F=3] 
* CE 41: case_0(A,B,C,D,E,F) = 6+ eval2(A,B,C,D,A,G):[39]+ eval2(A,B,C,D,C,H):[38]
     [E>=C,C>=A+1,H=1,G=1,F=3] 
* CE 42: case_0(A,B,C,D,E,F) = 6+ eval2(A,B,C,D,A,G):[39]+ eval2(A,B,C,D,C,H):[37]
     [A>=C+1,E>=A,H=1,G=1,F=3] 
* CE 43: case_0(A,B,C,D,E,F) = 6+ eval2(A,B,C,D,A,G):[39]+ eval2(A,B,C,D,H,I):[36]
     [E>=H,H>=C+1,H>=A+1,I=1,G=1,F=3] 
* CE 44: case_0(A,B,C,D,E,F) = 6+ eval2(A,B,C,D,A,G):[39]+ eval2(A,B,C,D,H,I):[35]
     [C>=H+1,E>=H,H>=A+1,I=1,G=1,F=3] 
* CE 45: case_0(A,B,C,D,E,F) = 6+ eval2(A,B,C,D,A,G):[39]+ eval2(A,B,C,D,H,I):[34]
     [A>=H+1,H>=C+1,E>=A,I=1,G=1,F=3] 
* CE 46: case_0(A,B,C,D,E,F) = 6+ eval2(A,B,C,D,A,G):[39]+ eval2(A,B,C,D,H,I):[33]
     [C>=H+1,A>=H+1,E>=A,I=1,G=1,F=3] 
* CE 47: case_0(A,B,C,D,E,F) = 6+ eval2(A,B,C,D,A,G):[39]+ eval2(A,B,C,D,H,I):[multiple([29,30,31,32],[[39],[38],[37],[36],[35],[34],[33]])]
     [E>=H,E>=A,I>=2,I+2=F,G=1] 
* CE 48: case_0(A,B,C,D,E,F) = 6+ eval2(A,B,C,D,C,G):[38]+ eval2(A,B,C,D,A,H):[39]
     [C>=A+1,E>=C,H=1,G=1,F=3] 
* CE 49: case_0(A,B,C,D,E,F) = 6+ eval2(A,B,C,D,C,G):[38]+ eval2(A,B,C,D,C,H):[38]
     [E>=C,C>=A+1,H=1,G=1,F=3] 
* CE 50: case_0(A,B,C,D,E,F) = 6+ eval2(A,B,C,D,C,G):[38]+ eval2(A,B,C,D,H,I):[36]
     [E>=H,H>=C+1,C>=A+1,I=1,G=1,F=3] 
* CE 51: case_0(A,B,C,D,E,F) = 6+ eval2(A,B,C,D,C,G):[38]+ eval2(A,B,C,D,H,I):[35]
     [C>=H+1,E>=C,H>=A+1,I=1,G=1,F=3] 
* CE 52: case_0(A,B,C,D,E,F) = 6+ eval2(A,B,C,D,C,G):[38]+ eval2(A,B,C,D,H,I):[33]
     [A>=H+1,E>=C,C>=A+1,I=1,G=1,F=3] 
* CE 53: case_0(A,B,C,D,E,F) = 6+ eval2(A,B,C,D,C,G):[38]+ eval2(A,B,C,D,H,I):[multiple([29,30,31,32],[[39],[38],[37],[36],[35],[34],[33]])]
     [E>=H,E>=C,C>=A+1,I>=2,I+2=F,G=1] 
* CE 54: case_0(A,B,C,D,E,F) = 6+ eval2(A,B,C,D,C,G):[37]+ eval2(A,B,C,D,A,H):[39]
     [E>=A,A>=C+1,H=1,G=1,F=3] 
* CE 55: case_0(A,B,C,D,E,F) = 6+ eval2(A,B,C,D,C,G):[37]+ eval2(A,B,C,D,C,H):[37]
     [A>=C+1,E>=C,H=1,G=1,F=3] 
* CE 56: case_0(A,B,C,D,E,F) = 6+ eval2(A,B,C,D,C,G):[37]+ eval2(A,B,C,D,H,I):[36]
     [E>=H,A>=C+1,H>=A+1,I=1,G=1,F=3] 
* CE 57: case_0(A,B,C,D,E,F) = 6+ eval2(A,B,C,D,C,G):[37]+ eval2(A,B,C,D,H,I):[34]
     [A>=H+1,E>=H,H>=C+1,I=1,G=1,F=3] 
* CE 58: case_0(A,B,C,D,E,F) = 6+ eval2(A,B,C,D,C,G):[37]+ eval2(A,B,C,D,H,I):[33]
     [C>=H+1,A>=C+1,E>=C,I=1,G=1,F=3] 
* CE 59: case_0(A,B,C,D,E,F) = 6+ eval2(A,B,C,D,C,G):[37]+ eval2(A,B,C,D,H,I):[multiple([29,30,31,32],[[39],[38],[37],[36],[35],[34],[33]])]
     [E>=H,A>=C+1,E>=C,I>=2,I+2=F,G=1] 
* CE 60: case_0(A,B,C,D,E,F) = 6+ eval2(A,B,C,D,G,H):[36]+ eval2(A,B,C,D,A,I):[39]
     [G>=A+1,E>=G,G>=C+1,I=1,H=1,F=3] 
* CE 61: case_0(A,B,C,D,E,F) = 6+ eval2(A,B,C,D,G,H):[36]+ eval2(A,B,C,D,C,I):[38]
     [G>=C+1,C>=A+1,E>=G,I=1,H=1,F=3] 
* CE 62: case_0(A,B,C,D,E,F) = 6+ eval2(A,B,C,D,G,H):[36]+ eval2(A,B,C,D,C,I):[37]
     [A>=C+1,G>=A+1,E>=G,I=1,H=1,F=3] 
* CE 63: case_0(A,B,C,D,E,F) = 6+ eval2(A,B,C,D,G,H):[36]+ eval2(A,B,C,D,I,J):[36]
     [E>=I,I>=C+1,G>=C+1,I>=A+1,G>=A+1,E>=G,J=1,H=1,F=3] 
* CE 64: case_0(A,B,C,D,E,F) = 6+ eval2(A,B,C,D,G,H):[36]+ eval2(A,B,C,D,I,J):[35]
     [C>=I+1,G>=C+1,I>=A+1,E>=G,J=1,H=1,F=3] 
* CE 65: case_0(A,B,C,D,E,F) = 6+ eval2(A,B,C,D,G,H):[36]+ eval2(A,B,C,D,I,J):[34]
     [A>=I+1,I>=C+1,G>=A+1,E>=G,J=1,H=1,F=3] 
* CE 66: case_0(A,B,C,D,E,F) = 6+ eval2(A,B,C,D,G,H):[36]+ eval2(A,B,C,D,I,J):[33]
     [C>=I+1,A>=I+1,G>=C+1,G>=A+1,E>=G,J=1,H=1,F=3] 
* CE 67: case_0(A,B,C,D,E,F) = 6+ eval2(A,B,C,D,G,H):[36]+ eval2(A,B,C,D,I,J):[multiple([29,30,31,32],[[39],[38],[37],[36],[35],[34],[33]])]
     [E>=I,E>=G,G>=C+1,G>=A+1,J>=2,J+2=F,H=1] 
* CE 68: case_0(A,B,C,D,E,F) = 6+ eval2(A,B,C,D,G,H):[35]+ eval2(A,B,C,D,A,I):[39]
     [G>=A+1,C>=G+1,E>=G,I=1,H=1,F=3] 
* CE 69: case_0(A,B,C,D,E,F) = 6+ eval2(A,B,C,D,G,H):[35]+ eval2(A,B,C,D,C,I):[38]
     [E>=C,G>=A+1,C>=G+1,I=1,H=1,F=3] 
* CE 70: case_0(A,B,C,D,E,F) = 6+ eval2(A,B,C,D,G,H):[35]+ eval2(A,B,C,D,I,J):[36]
     [E>=I,I>=C+1,G>=A+1,C>=G+1,J=1,H=1,F=3] 
* CE 71: case_0(A,B,C,D,E,F) = 6+ eval2(A,B,C,D,G,H):[35]+ eval2(A,B,C,D,I,J):[35]
     [C>=I+1,E>=I,I>=A+1,G>=A+1,C>=G+1,E>=G,J=1,H=1,F=3] 
* CE 72: case_0(A,B,C,D,E,F) = 6+ eval2(A,B,C,D,G,H):[35]+ eval2(A,B,C,D,I,J):[33]
     [A>=I+1,G>=A+1,C>=G+1,E>=G,J=1,H=1,F=3] 
* CE 73: case_0(A,B,C,D,E,F) = 6+ eval2(A,B,C,D,G,H):[35]+ eval2(A,B,C,D,I,J):[multiple([29,30,31,32],[[39],[38],[37],[36],[35],[34],[33]])]
     [E>=I,C>=G+1,E>=G,G>=A+1,J>=2,J+2=F,H=1] 
* CE 74: case_0(A,B,C,D,E,F) = 6+ eval2(A,B,C,D,G,H):[34]+ eval2(A,B,C,D,A,I):[39]
     [E>=A,A>=G+1,G>=C+1,I=1,H=1,F=3] 
* CE 75: case_0(A,B,C,D,E,F) = 6+ eval2(A,B,C,D,G,H):[34]+ eval2(A,B,C,D,C,I):[37]
     [G>=C+1,A>=G+1,E>=G,I=1,H=1,F=3] 
* CE 76: case_0(A,B,C,D,E,F) = 6+ eval2(A,B,C,D,G,H):[34]+ eval2(A,B,C,D,I,J):[36]
     [E>=I,G>=C+1,I>=A+1,A>=G+1,J=1,H=1,F=3] 
* CE 77: case_0(A,B,C,D,E,F) = 6+ eval2(A,B,C,D,G,H):[34]+ eval2(A,B,C,D,I,J):[34]
     [A>=I+1,E>=I,I>=C+1,G>=C+1,A>=G+1,E>=G,J=1,H=1,F=3] 
* CE 78: case_0(A,B,C,D,E,F) = 6+ eval2(A,B,C,D,G,H):[34]+ eval2(A,B,C,D,I,J):[33]
     [C>=I+1,G>=C+1,A>=G+1,E>=G,J=1,H=1,F=3] 
* CE 79: case_0(A,B,C,D,E,F) = 6+ eval2(A,B,C,D,G,H):[34]+ eval2(A,B,C,D,I,J):[multiple([29,30,31,32],[[39],[38],[37],[36],[35],[34],[33]])]
     [E>=I,A>=G+1,E>=G,G>=C+1,J>=2,J+2=F,H=1] 
* CE 80: case_0(A,B,C,D,E,F) = 6+ eval2(A,B,C,D,G,H):[33]+ eval2(A,B,C,D,A,I):[39]
     [E>=A,A>=G+1,C>=G+1,I=1,H=1,F=3] 
* CE 81: case_0(A,B,C,D,E,F) = 6+ eval2(A,B,C,D,G,H):[33]+ eval2(A,B,C,D,C,I):[38]
     [E>=C,C>=A+1,A>=G+1,I=1,H=1,F=3] 
* CE 82: case_0(A,B,C,D,E,F) = 6+ eval2(A,B,C,D,G,H):[33]+ eval2(A,B,C,D,C,I):[37]
     [A>=C+1,E>=C,C>=G+1,I=1,H=1,F=3] 
* CE 83: case_0(A,B,C,D,E,F) = 6+ eval2(A,B,C,D,G,H):[33]+ eval2(A,B,C,D,I,J):[36]
     [E>=I,I>=C+1,I>=A+1,C>=G+1,A>=G+1,J=1,H=1,F=3] 
* CE 84: case_0(A,B,C,D,E,F) = 6+ eval2(A,B,C,D,G,H):[33]+ eval2(A,B,C,D,I,J):[35]
     [C>=I+1,E>=I,I>=A+1,A>=G+1,J=1,H=1,F=3] 
* CE 85: case_0(A,B,C,D,E,F) = 6+ eval2(A,B,C,D,G,H):[33]+ eval2(A,B,C,D,I,J):[34]
     [A>=I+1,E>=I,I>=C+1,C>=G+1,J=1,H=1,F=3] 
* CE 86: case_0(A,B,C,D,E,F) = 6+ eval2(A,B,C,D,G,H):[33]+ eval2(A,B,C,D,I,J):[33]
     [C>=I+1,A>=I+1,E>=I,C>=G+1,A>=G+1,E>=G,J=1,H=1,F=3] 
* CE 87: case_0(A,B,C,D,E,F) = 6+ eval2(A,B,C,D,G,H):[33]+ eval2(A,B,C,D,I,J):[multiple([29,30,31,32],[[39],[38],[37],[36],[35],[34],[33]])]
     [E>=I,C>=G+1,A>=G+1,E>=G,J>=2,J+2=F,H=1] 
* CE 88: case_0(A,B,C,D,E,F) = 6+ eval2(A,B,C,D,G,H):[multiple([29,30,31,32],[[39],[38],[37],[36],[35],[34],[33]])]+ eval2(A,B,C,D,A,I):[39]
     [E>=A,E>=G,H>=2,H+2=F,I=1] 
* CE 89: case_0(A,B,C,D,E,F) = 6+ eval2(A,B,C,D,G,H):[multiple([29,30,31,32],[[39],[38],[37],[36],[35],[34],[33]])]+ eval2(A,B,C,D,C,I):[38]
     [E>=C,C>=A+1,E>=G,H>=2,H+2=F,I=1] 
* CE 90: case_0(A,B,C,D,E,F) = 6+ eval2(A,B,C,D,G,H):[multiple([29,30,31,32],[[39],[38],[37],[36],[35],[34],[33]])]+ eval2(A,B,C,D,C,I):[37]
     [A>=C+1,E>=C,E>=G,H>=2,H+2=F,I=1] 
* CE 91: case_0(A,B,C,D,E,F) = 6+ eval2(A,B,C,D,G,H):[multiple([29,30,31,32],[[39],[38],[37],[36],[35],[34],[33]])]+ eval2(A,B,C,D,I,J):[36]
     [E>=I,I>=C+1,I>=A+1,E>=G,H>=2,H+2=F,J=1] 
* CE 92: case_0(A,B,C,D,E,F) = 6+ eval2(A,B,C,D,G,H):[multiple([29,30,31,32],[[39],[38],[37],[36],[35],[34],[33]])]+ eval2(A,B,C,D,I,J):[35]
     [C>=I+1,E>=I,I>=A+1,E>=G,H>=2,H+2=F,J=1] 
* CE 93: case_0(A,B,C,D,E,F) = 6+ eval2(A,B,C,D,G,H):[multiple([29,30,31,32],[[39],[38],[37],[36],[35],[34],[33]])]+ eval2(A,B,C,D,I,J):[34]
     [A>=I+1,E>=I,I>=C+1,E>=G,H>=2,H+2=F,J=1] 
* CE 94: case_0(A,B,C,D,E,F) = 6+ eval2(A,B,C,D,G,H):[multiple([29,30,31,32],[[39],[38],[37],[36],[35],[34],[33]])]+ eval2(A,B,C,D,I,J):[33]
     [C>=I+1,A>=I+1,E>=I,E>=G,H>=2,H+2=F,J=1] 
* CE 95: case_0(A,B,C,D,E,F) = 6+ eval2(A,B,C,D,G,H):[multiple([29,30,31,32],[[39],[38],[37],[36],[35],[34],[33]])]+ eval2(A,B,C,D,I,J):[multiple([29,30,31,32],[[39],[38],[37],[36],[35],[34],[33]])]
     [E>=I,E>=G,J>=2,H>=2,H+J+1=F] 
* CE 96: case_0(A,B,C,D,E,F) = 7+ eval2(A,B,C,D,A,G):[39]+ eval2(A,B,C,D,A,H):[39]
     [E>=A,H=1,G=1,F=3] 
* CE 97: case_0(A,B,C,D,E,F) = 7+ eval2(A,B,C,D,A,G):[39]+ eval2(A,B,C,D,C,H):[38]
     [E>=C,C>=A+1,H=1,G=1,F=3] 
* CE 98: case_0(A,B,C,D,E,F) = 7+ eval2(A,B,C,D,A,G):[39]+ eval2(A,B,C,D,C,H):[37]
     [A>=C+1,E>=A,H=1,G=1,F=3] 
* CE 99: case_0(A,B,C,D,E,F) = 7+ eval2(A,B,C,D,A,G):[39]+ eval2(A,B,C,D,H,I):[36]
     [E>=H,H>=C+1,H>=A+1,I=1,G=1,F=3] 
* CE 100: case_0(A,B,C,D,E,F) = 7+ eval2(A,B,C,D,A,G):[39]+ eval2(A,B,C,D,H,I):[35]
     [C>=H+1,E>=H,H>=A+1,I=1,G=1,F=3] 
* CE 101: case_0(A,B,C,D,E,F) = 7+ eval2(A,B,C,D,A,G):[39]+ eval2(A,B,C,D,H,I):[34]
     [A>=H+1,H>=C+1,E>=A,I=1,G=1,F=3] 
* CE 102: case_0(A,B,C,D,E,F) = 7+ eval2(A,B,C,D,A,G):[39]+ eval2(A,B,C,D,H,I):[33]
     [C>=H+1,A>=H+1,E>=A,I=1,G=1,F=3] 
* CE 103: case_0(A,B,C,D,E,F) = 7+ eval2(A,B,C,D,A,G):[39]+ eval2(A,B,C,D,H,I):[multiple([29,30,31,32],[[39],[38],[37],[36],[35],[34],[33]])]
     [E>=H,E>=A,I>=2,I+2=F,G=1] 
* CE 104: case_0(A,B,C,D,E,F) = 7+ eval2(A,B,C,D,C,G):[38]+ eval2(A,B,C,D,A,H):[39]
     [C>=A+1,E>=C,H=1,G=1,F=3] 
* CE 105: case_0(A,B,C,D,E,F) = 7+ eval2(A,B,C,D,C,G):[38]+ eval2(A,B,C,D,C,H):[38]
     [E>=C,C>=A+1,H=1,G=1,F=3] 
* CE 106: case_0(A,B,C,D,E,F) = 7+ eval2(A,B,C,D,C,G):[38]+ eval2(A,B,C,D,H,I):[36]
     [E>=H,H>=C+1,C>=A+1,I=1,G=1,F=3] 
* CE 107: case_0(A,B,C,D,E,F) = 7+ eval2(A,B,C,D,C,G):[38]+ eval2(A,B,C,D,H,I):[35]
     [C>=H+1,E>=C,H>=A+1,I=1,G=1,F=3] 
* CE 108: case_0(A,B,C,D,E,F) = 7+ eval2(A,B,C,D,C,G):[38]+ eval2(A,B,C,D,H,I):[33]
     [A>=H+1,E>=C,C>=A+1,I=1,G=1,F=3] 
* CE 109: case_0(A,B,C,D,E,F) = 7+ eval2(A,B,C,D,C,G):[38]+ eval2(A,B,C,D,H,I):[multiple([29,30,31,32],[[39],[38],[37],[36],[35],[34],[33]])]
     [E>=H,E>=C,C>=A+1,I>=2,I+2=F,G=1] 
* CE 110: case_0(A,B,C,D,E,F) = 7+ eval2(A,B,C,D,C,G):[37]+ eval2(A,B,C,D,A,H):[39]
     [E>=A,A>=C+1,H=1,G=1,F=3] 
* CE 111: case_0(A,B,C,D,E,F) = 7+ eval2(A,B,C,D,C,G):[37]+ eval2(A,B,C,D,C,H):[37]
     [A>=C+1,E>=C,H=1,G=1,F=3] 
* CE 112: case_0(A,B,C,D,E,F) = 7+ eval2(A,B,C,D,C,G):[37]+ eval2(A,B,C,D,H,I):[36]
     [E>=H,A>=C+1,H>=A+1,I=1,G=1,F=3] 
* CE 113: case_0(A,B,C,D,E,F) = 7+ eval2(A,B,C,D,C,G):[37]+ eval2(A,B,C,D,H,I):[34]
     [A>=H+1,E>=H,H>=C+1,I=1,G=1,F=3] 
* CE 114: case_0(A,B,C,D,E,F) = 7+ eval2(A,B,C,D,C,G):[37]+ eval2(A,B,C,D,H,I):[33]
     [C>=H+1,A>=C+1,E>=C,I=1,G=1,F=3] 
* CE 115: case_0(A,B,C,D,E,F) = 7+ eval2(A,B,C,D,C,G):[37]+ eval2(A,B,C,D,H,I):[multiple([29,30,31,32],[[39],[38],[37],[36],[35],[34],[33]])]
     [E>=H,A>=C+1,E>=C,I>=2,I+2=F,G=1] 
* CE 116: case_0(A,B,C,D,E,F) = 7+ eval2(A,B,C,D,G,H):[36]+ eval2(A,B,C,D,A,I):[39]
     [G>=A+1,E>=G,G>=C+1,I=1,H=1,F=3] 
* CE 117: case_0(A,B,C,D,E,F) = 7+ eval2(A,B,C,D,G,H):[36]+ eval2(A,B,C,D,C,I):[38]
     [G>=C+1,C>=A+1,E>=G,I=1,H=1,F=3] 
* CE 118: case_0(A,B,C,D,E,F) = 7+ eval2(A,B,C,D,G,H):[36]+ eval2(A,B,C,D,C,I):[37]
     [A>=C+1,G>=A+1,E>=G,I=1,H=1,F=3] 
* CE 119: case_0(A,B,C,D,E,F) = 7+ eval2(A,B,C,D,G,H):[36]+ eval2(A,B,C,D,I,J):[36]
     [E>=I,I>=C+1,G>=C+1,I>=A+1,G>=A+1,E>=G,J=1,H=1,F=3] 
* CE 120: case_0(A,B,C,D,E,F) = 7+ eval2(A,B,C,D,G,H):[36]+ eval2(A,B,C,D,I,J):[35]
     [C>=I+1,G>=C+1,I>=A+1,E>=G,J=1,H=1,F=3] 
* CE 121: case_0(A,B,C,D,E,F) = 7+ eval2(A,B,C,D,G,H):[36]+ eval2(A,B,C,D,I,J):[34]
     [A>=I+1,I>=C+1,G>=A+1,E>=G,J=1,H=1,F=3] 
* CE 122: case_0(A,B,C,D,E,F) = 7+ eval2(A,B,C,D,G,H):[36]+ eval2(A,B,C,D,I,J):[33]
     [C>=I+1,A>=I+1,G>=C+1,G>=A+1,E>=G,J=1,H=1,F=3] 
* CE 123: case_0(A,B,C,D,E,F) = 7+ eval2(A,B,C,D,G,H):[36]+ eval2(A,B,C,D,I,J):[multiple([29,30,31,32],[[39],[38],[37],[36],[35],[34],[33]])]
     [E>=I,E>=G,G>=C+1,G>=A+1,J>=2,J+2=F,H=1] 
* CE 124: case_0(A,B,C,D,E,F) = 7+ eval2(A,B,C,D,G,H):[35]+ eval2(A,B,C,D,A,I):[39]
     [G>=A+1,C>=G+1,E>=G,I=1,H=1,F=3] 
* CE 125: case_0(A,B,C,D,E,F) = 7+ eval2(A,B,C,D,G,H):[35]+ eval2(A,B,C,D,C,I):[38]
     [E>=C,G>=A+1,C>=G+1,I=1,H=1,F=3] 
* CE 126: case_0(A,B,C,D,E,F) = 7+ eval2(A,B,C,D,G,H):[35]+ eval2(A,B,C,D,I,J):[36]
     [E>=I,I>=C+1,G>=A+1,C>=G+1,J=1,H=1,F=3] 
* CE 127: case_0(A,B,C,D,E,F) = 7+ eval2(A,B,C,D,G,H):[35]+ eval2(A,B,C,D,I,J):[35]
     [C>=I+1,E>=I,I>=A+1,G>=A+1,C>=G+1,E>=G,J=1,H=1,F=3] 
* CE 128: case_0(A,B,C,D,E,F) = 7+ eval2(A,B,C,D,G,H):[35]+ eval2(A,B,C,D,I,J):[33]
     [A>=I+1,G>=A+1,C>=G+1,E>=G,J=1,H=1,F=3] 
* CE 129: case_0(A,B,C,D,E,F) = 7+ eval2(A,B,C,D,G,H):[35]+ eval2(A,B,C,D,I,J):[multiple([29,30,31,32],[[39],[38],[37],[36],[35],[34],[33]])]
     [E>=I,C>=G+1,E>=G,G>=A+1,J>=2,J+2=F,H=1] 
* CE 130: case_0(A,B,C,D,E,F) = 7+ eval2(A,B,C,D,G,H):[34]+ eval2(A,B,C,D,A,I):[39]
     [E>=A,A>=G+1,G>=C+1,I=1,H=1,F=3] 
* CE 131: case_0(A,B,C,D,E,F) = 7+ eval2(A,B,C,D,G,H):[34]+ eval2(A,B,C,D,C,I):[37]
     [G>=C+1,A>=G+1,E>=G,I=1,H=1,F=3] 
* CE 132: case_0(A,B,C,D,E,F) = 7+ eval2(A,B,C,D,G,H):[34]+ eval2(A,B,C,D,I,J):[36]
     [E>=I,G>=C+1,I>=A+1,A>=G+1,J=1,H=1,F=3] 
* CE 133: case_0(A,B,C,D,E,F) = 7+ eval2(A,B,C,D,G,H):[34]+ eval2(A,B,C,D,I,J):[34]
     [A>=I+1,E>=I,I>=C+1,G>=C+1,A>=G+1,E>=G,J=1,H=1,F=3] 
* CE 134: case_0(A,B,C,D,E,F) = 7+ eval2(A,B,C,D,G,H):[34]+ eval2(A,B,C,D,I,J):[33]
     [C>=I+1,G>=C+1,A>=G+1,E>=G,J=1,H=1,F=3] 
* CE 135: case_0(A,B,C,D,E,F) = 7+ eval2(A,B,C,D,G,H):[34]+ eval2(A,B,C,D,I,J):[multiple([29,30,31,32],[[39],[38],[37],[36],[35],[34],[33]])]
     [E>=I,A>=G+1,E>=G,G>=C+1,J>=2,J+2=F,H=1] 
* CE 136: case_0(A,B,C,D,E,F) = 7+ eval2(A,B,C,D,G,H):[33]+ eval2(A,B,C,D,A,I):[39]
     [E>=A,A>=G+1,C>=G+1,I=1,H=1,F=3] 
* CE 137: case_0(A,B,C,D,E,F) = 7+ eval2(A,B,C,D,G,H):[33]+ eval2(A,B,C,D,C,I):[38]
     [E>=C,C>=A+1,A>=G+1,I=1,H=1,F=3] 
* CE 138: case_0(A,B,C,D,E,F) = 7+ eval2(A,B,C,D,G,H):[33]+ eval2(A,B,C,D,C,I):[37]
     [A>=C+1,E>=C,C>=G+1,I=1,H=1,F=3] 
* CE 139: case_0(A,B,C,D,E,F) = 7+ eval2(A,B,C,D,G,H):[33]+ eval2(A,B,C,D,I,J):[36]
     [E>=I,I>=C+1,I>=A+1,C>=G+1,A>=G+1,J=1,H=1,F=3] 
* CE 140: case_0(A,B,C,D,E,F) = 7+ eval2(A,B,C,D,G,H):[33]+ eval2(A,B,C,D,I,J):[35]
     [C>=I+1,E>=I,I>=A+1,A>=G+1,J=1,H=1,F=3] 
* CE 141: case_0(A,B,C,D,E,F) = 7+ eval2(A,B,C,D,G,H):[33]+ eval2(A,B,C,D,I,J):[34]
     [A>=I+1,E>=I,I>=C+1,C>=G+1,J=1,H=1,F=3] 
* CE 142: case_0(A,B,C,D,E,F) = 7+ eval2(A,B,C,D,G,H):[33]+ eval2(A,B,C,D,I,J):[33]
     [C>=I+1,A>=I+1,E>=I,C>=G+1,A>=G+1,E>=G,J=1,H=1,F=3] 
* CE 143: case_0(A,B,C,D,E,F) = 7+ eval2(A,B,C,D,G,H):[33]+ eval2(A,B,C,D,I,J):[multiple([29,30,31,32],[[39],[38],[37],[36],[35],[34],[33]])]
     [E>=I,C>=G+1,A>=G+1,E>=G,J>=2,J+2=F,H=1] 
* CE 144: case_0(A,B,C,D,E,F) = 7+ eval2(A,B,C,D,G,H):[multiple([29,30,31,32],[[39],[38],[37],[36],[35],[34],[33]])]+ eval2(A,B,C,D,A,I):[39]
     [E>=A,E>=G,H>=2,H+2=F,I=1] 
* CE 145: case_0(A,B,C,D,E,F) = 7+ eval2(A,B,C,D,G,H):[multiple([29,30,31,32],[[39],[38],[37],[36],[35],[34],[33]])]+ eval2(A,B,C,D,C,I):[38]
     [E>=C,C>=A+1,E>=G,H>=2,H+2=F,I=1] 
* CE 146: case_0(A,B,C,D,E,F) = 7+ eval2(A,B,C,D,G,H):[multiple([29,30,31,32],[[39],[38],[37],[36],[35],[34],[33]])]+ eval2(A,B,C,D,C,I):[37]
     [A>=C+1,E>=C,E>=G,H>=2,H+2=F,I=1] 
* CE 147: case_0(A,B,C,D,E,F) = 7+ eval2(A,B,C,D,G,H):[multiple([29,30,31,32],[[39],[38],[37],[36],[35],[34],[33]])]+ eval2(A,B,C,D,I,J):[36]
     [E>=I,I>=C+1,I>=A+1,E>=G,H>=2,H+2=F,J=1] 
* CE 148: case_0(A,B,C,D,E,F) = 7+ eval2(A,B,C,D,G,H):[multiple([29,30,31,32],[[39],[38],[37],[36],[35],[34],[33]])]+ eval2(A,B,C,D,I,J):[35]
     [C>=I+1,E>=I,I>=A+1,E>=G,H>=2,H+2=F,J=1] 
* CE 149: case_0(A,B,C,D,E,F) = 7+ eval2(A,B,C,D,G,H):[multiple([29,30,31,32],[[39],[38],[37],[36],[35],[34],[33]])]+ eval2(A,B,C,D,I,J):[34]
     [A>=I+1,E>=I,I>=C+1,E>=G,H>=2,H+2=F,J=1] 
* CE 150: case_0(A,B,C,D,E,F) = 7+ eval2(A,B,C,D,G,H):[multiple([29,30,31,32],[[39],[38],[37],[36],[35],[34],[33]])]+ eval2(A,B,C,D,I,J):[33]
     [C>=I+1,A>=I+1,E>=I,E>=G,H>=2,H+2=F,J=1] 
* CE 151: case_0(A,B,C,D,E,F) = 7+ eval2(A,B,C,D,G,H):[multiple([29,30,31,32],[[39],[38],[37],[36],[35],[34],[33]])]+ eval2(A,B,C,D,I,J):[multiple([29,30,31,32],[[39],[38],[37],[36],[35],[34],[33]])]
     [E>=I,E>=G,J>=2,H>=2,H+J+1=F] 
* CE 152: case_0(A,B,C,D,A,E) = 5+ eval2(A,B,C,D,A,F):[39]+ neg(G):[28]
     [G=0,F=1,E=2] 
* CE 153: case_0(A,B,C,D,A,E) = 5+ eval2(A,B,C,D,A,F):[39]+ neg(G):[27]
     [G=1,F=1,E=2] 
* CE 154: case_0(A,B,C,D,C,E) = 5+ eval2(A,B,C,D,C,F):[38]+ neg(G):[28]
     [C>=A+1,G=0,F=1,E=2] 
* CE 155: case_0(A,B,C,D,C,E) = 5+ eval2(A,B,C,D,C,F):[38]+ neg(G):[27]
     [C>=A+1,G=1,F=1,E=2] 
* CE 156: case_0(A,B,C,D,C,E) = 5+ eval2(A,B,C,D,C,F):[37]+ neg(G):[28]
     [A>=C+1,G=0,F=1,E=2] 
* CE 157: case_0(A,B,C,D,C,E) = 5+ eval2(A,B,C,D,C,F):[37]+ neg(G):[27]
     [A>=C+1,G=1,F=1,E=2] 
* CE 158: case_0(A,B,C,D,E,F) = 5+ eval2(A,B,C,D,E,G):[36]+ neg(H):[28]
     [E>=C+1,E>=A+1,H=0,G=1,F=2] 
* CE 159: case_0(A,B,C,D,E,F) = 5+ eval2(A,B,C,D,E,G):[36]+ neg(H):[27]
     [E>=C+1,E>=A+1,H=1,G=1,F=2] 
* CE 160: case_0(A,B,C,D,E,F) = 5+ eval2(A,B,C,D,E,G):[35]+ neg(H):[28]
     [C>=E+1,E>=A+1,H=0,G=1,F=2] 
* CE 161: case_0(A,B,C,D,E,F) = 5+ eval2(A,B,C,D,E,G):[35]+ neg(H):[27]
     [C>=E+1,E>=A+1,H=1,G=1,F=2] 
* CE 162: case_0(A,B,C,D,E,F) = 5+ eval2(A,B,C,D,E,G):[34]+ neg(H):[28]
     [A>=E+1,E>=C+1,H=0,G=1,F=2] 
* CE 163: case_0(A,B,C,D,E,F) = 5+ eval2(A,B,C,D,E,G):[34]+ neg(H):[27]
     [A>=E+1,E>=C+1,H=1,G=1,F=2] 
* CE 164: case_0(A,B,C,D,E,F) = 5+ eval2(A,B,C,D,E,G):[33]+ neg(H):[28]
     [C>=E+1,A>=E+1,H=0,G=1,F=2] 
* CE 165: case_0(A,B,C,D,E,F) = 5+ eval2(A,B,C,D,E,G):[33]+ neg(H):[27]
     [C>=E+1,A>=E+1,H=1,G=1,F=2] 
* CE 166: case_0(A,B,C,D,E,F) = 5+ eval2(A,B,C,D,E,G):[multiple([29,30,31,32],[[39],[38],[37],[36],[35],[34],[33]])]+ neg(H):[28]
     [G>=2,G+1=F,H=0] 
* CE 167: case_0(A,B,C,D,E,F) = 5+ eval2(A,B,C,D,E,G):[multiple([29,30,31,32],[[39],[38],[37],[36],[35],[34],[33]])]+ neg(H):[27]
     [G>=2,G+1=F,H=1] 
* CE 168: case_0(A,B,C,D,A,E) = 2+ case_1(A,B,C,D,A):[26]
     [E=1] 
* CE 169: case_0(A,B,C,D,C,E) = 2+ case_1(A,B,C,D,C):[25]
     [C>=A+1,E=1] 
* CE 170: case_0(A,B,C,D,C,E) = 2+ case_1(A,B,C,D,C):[24]
     [A>=C+1,E=1] 
* CE 171: case_0(A,B,C,D,E,F) = 2+ case_1(A,B,C,D,E):[23]
     [E>=C+1,E>=A+1,F=1] 
* CE 172: case_0(A,B,C,D,E,F) = 2+ case_1(A,B,C,D,E):[22]
     [C>=E+1,E>=A+1,F=1] 
* CE 173: case_0(A,B,C,D,E,F) = 2+ case_1(A,B,C,D,E):[21]
     [A>=E+1,E>=C+1,F=1] 
* CE 174: case_0(A,B,C,D,E,F) = 2+ case_1(A,B,C,D,E):[20]
     [C>=E+1,A>=E+1,F=1] 

### Cost equations --> "Loop" of case_0/6 
* CEs [151] --> Loop 40 
* CEs [95] --> Loop 41 
* CEs [149] --> Loop 42 
* CEs [135] --> Loop 43 
* CEs [93] --> Loop 44 
* CEs [79] --> Loop 45 
* CEs [146] --> Loop 46 
* CEs [115] --> Loop 47 
* CEs [90] --> Loop 48 
* CEs [59] --> Loop 49 
* CEs [147] --> Loop 50 
* CEs [123] --> Loop 51 
* CEs [91] --> Loop 52 
* CEs [67] --> Loop 53 
* CEs [144] --> Loop 54 
* CEs [103] --> Loop 55 
* CEs [88] --> Loop 56 
* CEs [47] --> Loop 57 
* CEs [148] --> Loop 58 
* CEs [129] --> Loop 59 
* CEs [92] --> Loop 60 
* CEs [73] --> Loop 61 
* CEs [145] --> Loop 62 
* CEs [109] --> Loop 63 
* CEs [89] --> Loop 64 
* CEs [53] --> Loop 65 
* CEs [150] --> Loop 66 
* CEs [143] --> Loop 67 
* CEs [94] --> Loop 68 
* CEs [87] --> Loop 69 
* CEs [167] --> Loop 70 
* CEs [166] --> Loop 71 
* CEs [141] --> Loop 72 
* CEs [134] --> Loop 73 
* CEs [133] --> Loop 74 
* CEs [131] --> Loop 75 
* CEs [113] --> Loop 76 
* CEs [85] --> Loop 77 
* CEs [78] --> Loop 78 
* CEs [77] --> Loop 79 
* CEs [75] --> Loop 80 
* CEs [57] --> Loop 81 
* CEs [138] --> Loop 82 
* CEs [114] --> Loop 83 
* CEs [111] --> Loop 84 
* CEs [82] --> Loop 85 
* CEs [58] --> Loop 86 
* CEs [55] --> Loop 87 
* CEs [139] --> Loop 88 
* CEs [122] --> Loop 89 
* CEs [119] --> Loop 90 
* CEs [116] --> Loop 91 
* CEs [99] --> Loop 92 
* CEs [83] --> Loop 93 
* CEs [66] --> Loop 94 
* CEs [63] --> Loop 95 
* CEs [60] --> Loop 96 
* CEs [43] --> Loop 97 
* CEs [132] --> Loop 98 
* CEs [121] --> Loop 99 
* CEs [76] --> Loop 100 
* CEs [65] --> Loop 101 
* CEs [118] --> Loop 102 
* CEs [112] --> Loop 103 
* CEs [62] --> Loop 104 
* CEs [56] --> Loop 105 
* CEs [130] --> Loop 106 
* CEs [101] --> Loop 107 
* CEs [74] --> Loop 108 
* CEs [45] --> Loop 109 
* CEs [110] --> Loop 110 
* CEs [98] --> Loop 111 
* CEs [54] --> Loop 112 
* CEs [42] --> Loop 113 
* CEs [136] --> Loop 114 
* CEs [102] --> Loop 115 
* CEs [96] --> Loop 116 
* CEs [80] --> Loop 117 
* CEs [46] --> Loop 118 
* CEs [40] --> Loop 119 
* CEs [126] --> Loop 120 
* CEs [120] --> Loop 121 
* CEs [70] --> Loop 122 
* CEs [64] --> Loop 123 
* CEs [125] --> Loop 124 
* CEs [107] --> Loop 125 
* CEs [69] --> Loop 126 
* CEs [51] --> Loop 127 
* CEs [140] --> Loop 128 
* CEs [128] --> Loop 129 
* CEs [127] --> Loop 130 
* CEs [124] --> Loop 131 
* CEs [100] --> Loop 132 
* CEs [84] --> Loop 133 
* CEs [72] --> Loop 134 
* CEs [71] --> Loop 135 
* CEs [68] --> Loop 136 
* CEs [44] --> Loop 137 
* CEs [117] --> Loop 138 
* CEs [106] --> Loop 139 
* CEs [61] --> Loop 140 
* CEs [50] --> Loop 141 
* CEs [137] --> Loop 142 
* CEs [108] --> Loop 143 
* CEs [105] --> Loop 144 
* CEs [104] --> Loop 145 
* CEs [97] --> Loop 146 
* CEs [81] --> Loop 147 
* CEs [52] --> Loop 148 
* CEs [49] --> Loop 149 
* CEs [48] --> Loop 150 
* CEs [41] --> Loop 151 
* CEs [142] --> Loop 152 
* CEs [86] --> Loop 153 
* CEs [165] --> Loop 154 
* CEs [164] --> Loop 155 
* CEs [163] --> Loop 156 
* CEs [162] --> Loop 157 
* CEs [161] --> Loop 158 
* CEs [160] --> Loop 159 
* CEs [159] --> Loop 160 
* CEs [158] --> Loop 161 
* CEs [157] --> Loop 162 
* CEs [156] --> Loop 163 
* CEs [155] --> Loop 164 
* CEs [154] --> Loop 165 
* CEs [153] --> Loop 166 
* CEs [152] --> Loop 167 
* CEs [174] --> Loop 168 
* CEs [173] --> Loop 169 
* CEs [172] --> Loop 170 
* CEs [171] --> Loop 171 
* CEs [170] --> Loop 172 
* CEs [169] --> Loop 173 
* CEs [168] --> Loop 174 

#### Loops of case_0/6 
* Loop 40: case_0(A,B,C,D,E,F) [F>=5] 
* Loop 41: case_0(A,B,C,D,E,F) [F>=5] 
* Loop 42: case_0(A,B,C,D,E,F) [E>=C+1,A>=C+2,F>=4] 
* Loop 43: case_0(A,B,C,D,E,F) [E>=C+1,A>=C+2,F>=4] 
* Loop 44: case_0(A,B,C,D,E,F) [E>=C+1,A>=C+2,F>=4] 
* Loop 45: case_0(A,B,C,D,E,F) [E>=C+1,A>=C+2,F>=4] 
* Loop 46: case_0(A,B,C,D,E,F) [E>=C,A>=C+1,F>=4] 
* Loop 47: case_0(A,B,C,D,E,F) [E>=C,A>=C+1,F>=4] 
* Loop 48: case_0(A,B,C,D,E,F) [E>=C,A>=C+1,F>=4] 
* Loop 49: case_0(A,B,C,D,E,F) [E>=C,A>=C+1,F>=4] 
* Loop 50: case_0(A,B,C,D,E,F) [E>=C+1,E>=A+1,F>=4] 
* Loop 51: case_0(A,B,C,D,E,F) [E>=C+1,E>=A+1,F>=4] 
* Loop 52: case_0(A,B,C,D,E,F) [E>=C+1,E>=A+1,F>=4] 
* Loop 53: case_0(A,B,C,D,E,F) [E>=C+1,E>=A+1,F>=4] 
* Loop 54: case_0(A,B,C,D,E,F) [E>=A,F>=4] 
* Loop 55: case_0(A,B,C,D,E,F) [E>=A,F>=4] 
* Loop 56: case_0(A,B,C,D,E,F) [E>=A,F>=4] 
* Loop 57: case_0(A,B,C,D,E,F) [E>=A,F>=4] 
* Loop 58: case_0(A,B,C,D,E,F) [E>=A+1,C>=A+2,F>=4] 
* Loop 59: case_0(A,B,C,D,E,F) [E>=A+1,C>=A+2,F>=4] 
* Loop 60: case_0(A,B,C,D,E,F) [E>=A+1,C>=A+2,F>=4] 
* Loop 61: case_0(A,B,C,D,E,F) [E>=A+1,C>=A+2,F>=4] 
* Loop 62: case_0(A,B,C,D,E,F) [E>=C,C>=A+1,F>=4] 
* Loop 63: case_0(A,B,C,D,E,F) [E>=C,C>=A+1,F>=4] 
* Loop 64: case_0(A,B,C,D,E,F) [E>=C,C>=A+1,F>=4] 
* Loop 65: case_0(A,B,C,D,E,F) [E>=C,C>=A+1,F>=4] 
* Loop 66: case_0(A,B,C,D,E,F) [F>=4] 
* Loop 67: case_0(A,B,C,D,E,F) [F>=4] 
* Loop 68: case_0(A,B,C,D,E,F) [F>=4] 
* Loop 69: case_0(A,B,C,D,E,F) [F>=4] 
* Loop 70: case_0(A,B,C,D,E,F) [F>=3] 
* Loop 71: case_0(A,B,C,D,E,F) [F>=3] 
* Loop 72: case_0(A,B,C,D,E,F) [E>=C+1,A>=C+2,F=3] 
* Loop 73: case_0(A,B,C,D,E,F) [E>=C+1,A>=C+2,F=3] 
* Loop 74: case_0(A,B,C,D,E,F) [E>=C+1,A>=C+2,F=3] 
* Loop 75: case_0(A,B,C,D,E,F) [E>=C+1,A>=C+2,F=3] 
* Loop 76: case_0(A,B,C,D,E,F) [E>=C+1,A>=C+2,F=3] 
* Loop 77: case_0(A,B,C,D,E,F) [E>=C+1,A>=C+2,F=3] 
* Loop 78: case_0(A,B,C,D,E,F) [E>=C+1,A>=C+2,F=3] 
* Loop 79: case_0(A,B,C,D,E,F) [E>=C+1,A>=C+2,F=3] 
* Loop 80: case_0(A,B,C,D,E,F) [E>=C+1,A>=C+2,F=3] 
* Loop 81: case_0(A,B,C,D,E,F) [E>=C+1,A>=C+2,F=3] 
* Loop 82: case_0(A,B,C,D,E,F) [E>=C,A>=C+1,F=3] 
* Loop 83: case_0(A,B,C,D,E,F) [E>=C,A>=C+1,F=3] 
* Loop 84: case_0(A,B,C,D,E,F) [E>=C,A>=C+1,F=3] 
* Loop 85: case_0(A,B,C,D,E,F) [E>=C,A>=C+1,F=3] 
* Loop 86: case_0(A,B,C,D,E,F) [E>=C,A>=C+1,F=3] 
* Loop 87: case_0(A,B,C,D,E,F) [E>=C,A>=C+1,F=3] 
* Loop 88: case_0(A,B,C,D,E,F) [E>=C+1,E>=A+1,F=3] 
* Loop 89: case_0(A,B,C,D,E,F) [E>=C+1,E>=A+1,F=3] 
* Loop 90: case_0(A,B,C,D,E,F) [E>=C+1,E>=A+1,F=3] 
* Loop 91: case_0(A,B,C,D,E,F) [E>=C+1,E>=A+1,F=3] 
* Loop 92: case_0(A,B,C,D,E,F) [E>=C+1,E>=A+1,F=3] 
* Loop 93: case_0(A,B,C,D,E,F) [E>=C+1,E>=A+1,F=3] 
* Loop 94: case_0(A,B,C,D,E,F) [E>=C+1,E>=A+1,F=3] 
* Loop 95: case_0(A,B,C,D,E,F) [E>=C+1,E>=A+1,F=3] 
* Loop 96: case_0(A,B,C,D,E,F) [E>=C+1,E>=A+1,F=3] 
* Loop 97: case_0(A,B,C,D,E,F) [E>=C+1,E>=A+1,F=3] 
* Loop 98: case_0(A,B,C,D,E,F) [A>=C+2,E>=A+1,F=3] 
* Loop 99: case_0(A,B,C,D,E,F) [A>=C+2,E>=A+1,F=3] 
* Loop 100: case_0(A,B,C,D,E,F) [A>=C+2,E>=A+1,F=3] 
* Loop 101: case_0(A,B,C,D,E,F) [A>=C+2,E>=A+1,F=3] 
* Loop 102: case_0(A,B,C,D,E,F) [A>=C+1,E>=A+1,F=3] 
* Loop 103: case_0(A,B,C,D,E,F) [A>=C+1,E>=A+1,F=3] 
* Loop 104: case_0(A,B,C,D,E,F) [A>=C+1,E>=A+1,F=3] 
* Loop 105: case_0(A,B,C,D,E,F) [A>=C+1,E>=A+1,F=3] 
* Loop 106: case_0(A,B,C,D,E,F) [A>=C+2,E>=A,F=3] 
* Loop 107: case_0(A,B,C,D,E,F) [A>=C+2,E>=A,F=3] 
* Loop 108: case_0(A,B,C,D,E,F) [A>=C+2,E>=A,F=3] 
* Loop 109: case_0(A,B,C,D,E,F) [A>=C+2,E>=A,F=3] 
* Loop 110: case_0(A,B,C,D,E,F) [A>=C+1,E>=A,F=3] 
* Loop 111: case_0(A,B,C,D,E,F) [A>=C+1,E>=A,F=3] 
* Loop 112: case_0(A,B,C,D,E,F) [A>=C+1,E>=A,F=3] 
* Loop 113: case_0(A,B,C,D,E,F) [A>=C+1,E>=A,F=3] 
* Loop 114: case_0(A,B,C,D,E,F) [E>=A,F=3] 
* Loop 115: case_0(A,B,C,D,E,F) [E>=A,F=3] 
* Loop 116: case_0(A,B,C,D,E,F) [E>=A,F=3] 
* Loop 117: case_0(A,B,C,D,E,F) [E>=A,F=3] 
* Loop 118: case_0(A,B,C,D,E,F) [E>=A,F=3] 
* Loop 119: case_0(A,B,C,D,E,F) [E>=A,F=3] 
* Loop 120: case_0(A,B,C,D,E,F) [E>=C+1,C>=A+2,F=3] 
* Loop 121: case_0(A,B,C,D,E,F) [E>=C+1,C>=A+2,F=3] 
* Loop 122: case_0(A,B,C,D,E,F) [E>=C+1,C>=A+2,F=3] 
* Loop 123: case_0(A,B,C,D,E,F) [E>=C+1,C>=A+2,F=3] 
* Loop 124: case_0(A,B,C,D,E,F) [E>=C,C>=A+2,F=3] 
* Loop 125: case_0(A,B,C,D,E,F) [E>=C,C>=A+2,F=3] 
* Loop 126: case_0(A,B,C,D,E,F) [E>=C,C>=A+2,F=3] 
* Loop 127: case_0(A,B,C,D,E,F) [E>=C,C>=A+2,F=3] 
* Loop 128: case_0(A,B,C,D,E,F) [E>=A+1,C>=A+2,F=3] 
* Loop 129: case_0(A,B,C,D,E,F) [E>=A+1,C>=A+2,F=3] 
* Loop 130: case_0(A,B,C,D,E,F) [E>=A+1,C>=A+2,F=3] 
* Loop 131: case_0(A,B,C,D,E,F) [E>=A+1,C>=A+2,F=3] 
* Loop 132: case_0(A,B,C,D,E,F) [E>=A+1,C>=A+2,F=3] 
* Loop 133: case_0(A,B,C,D,E,F) [E>=A+1,C>=A+2,F=3] 
* Loop 134: case_0(A,B,C,D,E,F) [E>=A+1,C>=A+2,F=3] 
* Loop 135: case_0(A,B,C,D,E,F) [E>=A+1,C>=A+2,F=3] 
* Loop 136: case_0(A,B,C,D,E,F) [E>=A+1,C>=A+2,F=3] 
* Loop 137: case_0(A,B,C,D,E,F) [E>=A+1,C>=A+2,F=3] 
* Loop 138: case_0(A,B,C,D,E,F) [E>=C+1,C>=A+1,F=3] 
* Loop 139: case_0(A,B,C,D,E,F) [E>=C+1,C>=A+1,F=3] 
* Loop 140: case_0(A,B,C,D,E,F) [E>=C+1,C>=A+1,F=3] 
* Loop 141: case_0(A,B,C,D,E,F) [E>=C+1,C>=A+1,F=3] 
* Loop 142: case_0(A,B,C,D,E,F) [E>=C,C>=A+1,F=3] 
* Loop 143: case_0(A,B,C,D,E,F) [E>=C,C>=A+1,F=3] 
* Loop 144: case_0(A,B,C,D,E,F) [E>=C,C>=A+1,F=3] 
* Loop 145: case_0(A,B,C,D,E,F) [E>=C,C>=A+1,F=3] 
* Loop 146: case_0(A,B,C,D,E,F) [E>=C,C>=A+1,F=3] 
* Loop 147: case_0(A,B,C,D,E,F) [E>=C,C>=A+1,F=3] 
* Loop 148: case_0(A,B,C,D,E,F) [E>=C,C>=A+1,F=3] 
* Loop 149: case_0(A,B,C,D,E,F) [E>=C,C>=A+1,F=3] 
* Loop 150: case_0(A,B,C,D,E,F) [E>=C,C>=A+1,F=3] 
* Loop 151: case_0(A,B,C,D,E,F) [E>=C,C>=A+1,F=3] 
* Loop 152: case_0(A,B,C,D,E,F) [F=3] 
* Loop 153: case_0(A,B,C,D,E,F) [F=3] 
* Loop 154: case_0(A,B,C,D,E,F) [C>=E+1,A>=E+1,F=2] 
* Loop 155: case_0(A,B,C,D,E,F) [C>=E+1,A>=E+1,F=2] 
* Loop 156: case_0(A,B,C,D,E,F) [A>=E+1,E>=C+1,F=2] 
* Loop 157: case_0(A,B,C,D,E,F) [A>=E+1,E>=C+1,F=2] 
* Loop 158: case_0(A,B,C,D,E,F) [C>=E+1,E>=A+1,F=2] 
* Loop 159: case_0(A,B,C,D,E,F) [C>=E+1,E>=A+1,F=2] 
* Loop 160: case_0(A,B,C,D,E,F) [E>=C+1,E>=A+1,F=2] 
* Loop 161: case_0(A,B,C,D,E,F) [E>=C+1,E>=A+1,F=2] 
* Loop 162: case_0(A,B,C,D,C,E) [A>=C+1,E=2] 
* Loop 163: case_0(A,B,C,D,C,E) [A>=C+1,E=2] 
* Loop 164: case_0(A,B,C,D,C,E) [C>=A+1,E=2] 
* Loop 165: case_0(A,B,C,D,C,E) [C>=A+1,E=2] 
* Loop 166: case_0(A,B,C,D,A,E) [E=2] 
* Loop 167: case_0(A,B,C,D,A,E) [E=2] 
* Loop 168: case_0(A,B,C,D,E,F) [C>=E+1,A>=E+1,F=1] 
* Loop 169: case_0(A,B,C,D,E,F) [A>=E+1,E>=C+1,F=1] 
* Loop 170: case_0(A,B,C,D,E,F) [C>=E+1,E>=A+1,F=1] 
* Loop 171: case_0(A,B,C,D,E,F) [E>=C+1,E>=A+1,F=1] 
* Loop 172: case_0(A,B,C,D,C,E) [A>=C+1,E=1] 
* Loop 173: case_0(A,B,C,D,C,E) [C>=A+1,E=1] 
* Loop 174: case_0(A,B,C,D,A,E) [E=1] 

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

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


### Resulting Chains:case_0(A,B,C,D,E,F) 
* [174]
* [173]
* [172]
* [171]
* [170]
* [169]
* [168]
* [167]
* [166]
* [165]
* [164]
* [163]
* [162]
* [161]
* [160]
* [159]
* [158]
* [157]
* [156]
* [155]
* [154]
* [153]
* [152]
* [151]
* [150]
* [149]
* [148]
* [147]
* [146]
* [145]
* [144]
* [143]
* [142]
* [141]
* [140]
* [139]
* [138]
* [137]
* [136]
* [135]
* [134]
* [133]
* [132]
* [131]
* [130]
* [129]
* [128]
* [127]
* [126]
* [125]
* [124]
* [123]
* [122]
* [121]
* [120]
* [119]
* [118]
* [117]
* [116]
* [115]
* [114]
* [113]
* [112]
* [111]
* [110]
* [109]
* [108]
* [107]
* [106]
* [105]
* [104]
* [103]
* [102]
* [101]
* [100]
* [99]
* [98]
* [97]
* [96]
* [95]
* [94]
* [93]
* [92]
* [91]
* [90]
* [89]
* [88]
* [87]
* [86]
* [85]
* [84]
* [83]
* [82]
* [81]
* [80]
* [79]
* [78]
* [77]
* [76]
* [75]
* [74]
* [73]
* [72]
* [71]
* [70]
* [69]
* [68]
* [67]
* [66]
* [65]
* [64]
* [63]
* [62]
* [61]
* [60]
* [59]
* [58]
* [57]
* [56]
* [55]
* [54]
* [53]
* [52]
* [51]
* [50]
* [49]
* [48]
* [47]
* [46]
* [45]
* [44]
* [43]
* [42]
* [41]
* [40]


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

#### Cost of chains of case_2(A,B,C):
* Chain [19]: 1
  with precondition: [C=A] 

* Chain [18]: 2
  with precondition: [C>=A+1] 

* Chain [17]: 2
  with precondition: [A>=C+1] 


#### Cost of chains of case_1(A,B,C,D,E):
* Chain [26]: 1
  with precondition: [E=A] 

* Chain [25]: 3
  with precondition: [C=E,C>=A+1] 

* Chain [24]: 3
  with precondition: [C=E,A>=C+1] 

* Chain [23]: 4
  with precondition: [E>=A+1,E>=C+1] 

* Chain [22]: 4
  with precondition: [E>=A+1,C>=E+1] 

* Chain [21]: 4
  with precondition: [E>=C+1,A>=E+1] 

* Chain [20]: 4
  with precondition: [A>=E+1,C>=E+1] 


#### Cost of chains of neg(A):
* Chain [28]: 0
  with precondition: [A=0] 

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


#### Cost of loops [29,30,31,32] 

 * loop 29:eval2(A,B,C,D,E,F) -> [eval2(A',B',C',D',E',F'),eval2(A'2,B'2,C'2,D'2,E'2,F'2)] 
8
 * loop 30:eval2(A,B,C,D,E,F) -> [eval2(A',B',C',D',E',F'),eval2(A'2,B'2,C'2,D'2,E'2,F'2)] 
7
 * loop 31:eval2(A,B,C,D,E,F) -> [eval2(A',B',C',D',E',F')] 
6
 * loop 32:eval2(A,B,C,D,E,F) -> [eval2(A',B',C',D',E',F')] 
6
#### Cost of phase [29,30,31,32]:eval2(A,B,C,D,E,F) -> [] 
8*it(29)+7*it(30)+6*it(31)+6*it(32)+7*it([33])+7*it([34])+7*it([35])+7*it([36])+6*it([37])+6*it([38])+4*it([39])+0
  Such that:it(31)+it(32) =< F-1
it(29)+it(30) =< F/2-1/2
it([33])+it([34])+it([35])+it([36])+it([37])+it([38])+it([39]) =< F/2+1/2
it(29)+it(30)+it(31)+it(32)+it([33])+it([34])+it([35])+it([36])+it([37])+it([38])+it([39]) >= F
aux(6) >= 1
aux(6) >= aux(6)
it([33])+it([34])+it([35])+it([36])+it([37])+it([38])+it([39]) >= it(30)+it(29)+aux(6)

#### Cost of chains of eval2(A,B,C,D,E,F):
* Chain [39]: 4
  with precondition: [F=1,E=A] 

* Chain [38]: 6
  with precondition: [F=1,C=E,C>=A+1] 

* Chain [37]: 6
  with precondition: [F=1,C=E,A>=C+1] 

* Chain [36]: 7
  with precondition: [F=1,E>=A+1,E>=C+1] 

* Chain [35]: 7
  with precondition: [F=1,E>=A+1,C>=E+1] 

* Chain [34]: 7
  with precondition: [F=1,E>=C+1,A>=E+1] 

* Chain [33]: 7
  with precondition: [F=1,A>=E+1,C>=E+1] 

* Chain [multiple([29,30,31,32],[[39],[38],[37],[36],[35],[34],[33]])]: 8*it(29)+7*it(30)+6*it(31)+6*it(32)+7*it([33])+7*it([34])+7*it([35])+7*it([36])+6*it([37])+6*it([38])+4*it([39])+0
  Such that:it(31)+it(32) =< F-1
it(29)+it(30) =< F/2-1/2
it([33])+it([34])+it([35])+it([36])+it([37])+it([38])+it([39]) =< F/2+1/2
it(29)+it(30)+it(31)+it(32)+it([33])+it([34])+it([35])+it([36])+it([37])+it([38])+it([39]) >= F
aux(6) >= 1
aux(6) >= aux(6)
it([33])+it([34])+it([35])+it([36])+it([37])+it([38])+it([39]) >= it(30)+it(29)+aux(6)

  with precondition: [F>=2] 


#### Cost of chains of case_0(A,B,C,D,E,F):
* Chain [174]: 3
  with precondition: [F=1,E=A] 

* Chain [173]: 5
  with precondition: [F=1,C=E,C>=A+1] 

* Chain [172]: 5
  with precondition: [F=1,C=E,A>=C+1] 

* Chain [171]: 6
  with precondition: [F=1,E>=A+1,E>=C+1] 

* Chain [170]: 6
  with precondition: [F=1,E>=A+1,C>=E+1] 

* Chain [169]: 6
  with precondition: [F=1,E>=C+1,A>=E+1] 

* Chain [168]: 6
  with precondition: [F=1,A>=E+1,C>=E+1] 

* Chain [167]: 9
  with precondition: [F=2,E=A] 

* Chain [166]: 9
  with precondition: [F=2,E=A] 

* Chain [165]: 11
  with precondition: [F=2,C=E,C>=A+1] 

* Chain [164]: 11
  with precondition: [F=2,C=E,C>=A+1] 

* Chain [163]: 11
  with precondition: [F=2,C=E,A>=C+1] 

* Chain [162]: 11
  with precondition: [F=2,C=E,A>=C+1] 

* Chain [161]: 12
  with precondition: [F=2,E>=A+1,E>=C+1] 

* Chain [160]: 12
  with precondition: [F=2,E>=A+1,E>=C+1] 

* Chain [159]: 12
  with precondition: [F=2,E>=A+1,C>=E+1] 

* Chain [158]: 12
  with precondition: [F=2,E>=A+1,C>=E+1] 

* Chain [157]: 12
  with precondition: [F=2,E>=C+1,A>=E+1] 

* Chain [156]: 12
  with precondition: [F=2,E>=C+1,A>=E+1] 

* Chain [155]: 12
  with precondition: [F=2,A>=E+1,C>=E+1] 

* Chain [154]: 12
  with precondition: [F=2,A>=E+1,C>=E+1] 

* Chain [153]: 20
  with precondition: [F=3] 

* Chain [152]: 21
  with precondition: [F=3] 

* Chain [151]: 16
  with precondition: [F=3,C>=A+1,E>=C] 

* Chain [150]: 16
  with precondition: [F=3,C>=A+1,E>=C] 

* Chain [149]: 18
  with precondition: [F=3,C>=A+1,E>=C] 

* Chain [148]: 19
  with precondition: [F=3,C>=A+1,E>=C] 

* Chain [147]: 19
  with precondition: [F=3,C>=A+1,E>=C] 

* Chain [146]: 17
  with precondition: [F=3,C>=A+1,E>=C] 

* Chain [145]: 17
  with precondition: [F=3,C>=A+1,E>=C] 

* Chain [144]: 19
  with precondition: [F=3,C>=A+1,E>=C] 

* Chain [143]: 20
  with precondition: [F=3,C>=A+1,E>=C] 

* Chain [142]: 20
  with precondition: [F=3,C>=A+1,E>=C] 

* Chain [141]: 19
  with precondition: [F=3,C>=A+1,E>=C+1] 

* Chain [140]: 19
  with precondition: [F=3,C>=A+1,E>=C+1] 

* Chain [139]: 20
  with precondition: [F=3,C>=A+1,E>=C+1] 

* Chain [138]: 20
  with precondition: [F=3,C>=A+1,E>=C+1] 

* Chain [137]: 17
  with precondition: [F=3,C>=A+2,E>=A+1] 

* Chain [136]: 17
  with precondition: [F=3,C>=A+2,E>=A+1] 

* Chain [135]: 20
  with precondition: [F=3,C>=A+2,E>=A+1] 

* Chain [134]: 20
  with precondition: [F=3,C>=A+2,E>=A+1] 

* Chain [133]: 20
  with precondition: [F=3,C>=A+2,E>=A+1] 

* Chain [132]: 18
  with precondition: [F=3,C>=A+2,E>=A+1] 

* Chain [131]: 18
  with precondition: [F=3,C>=A+2,E>=A+1] 

* Chain [130]: 21
  with precondition: [F=3,C>=A+2,E>=A+1] 

* Chain [129]: 21
  with precondition: [F=3,C>=A+2,E>=A+1] 

* Chain [128]: 21
  with precondition: [F=3,C>=A+2,E>=A+1] 

* Chain [127]: 19
  with precondition: [F=3,C>=A+2,E>=C] 

* Chain [126]: 19
  with precondition: [F=3,C>=A+2,E>=C] 

* Chain [125]: 20
  with precondition: [F=3,C>=A+2,E>=C] 

* Chain [124]: 20
  with precondition: [F=3,C>=A+2,E>=C] 

* Chain [123]: 20
  with precondition: [F=3,C>=A+2,E>=C+1] 

* Chain [122]: 20
  with precondition: [F=3,C>=A+2,E>=C+1] 

* Chain [121]: 21
  with precondition: [F=3,C>=A+2,E>=C+1] 

* Chain [120]: 21
  with precondition: [F=3,C>=A+2,E>=C+1] 

* Chain [119]: 14
  with precondition: [F=3,E>=A] 

* Chain [118]: 17
  with precondition: [F=3,E>=A] 

* Chain [117]: 17
  with precondition: [F=3,E>=A] 

* Chain [116]: 15
  with precondition: [F=3,E>=A] 

* Chain [115]: 18
  with precondition: [F=3,E>=A] 

* Chain [114]: 18
  with precondition: [F=3,E>=A] 

* Chain [113]: 16
  with precondition: [F=3,E>=A,A>=C+1] 

* Chain [112]: 16
  with precondition: [F=3,E>=A,A>=C+1] 

* Chain [111]: 17
  with precondition: [F=3,E>=A,A>=C+1] 

* Chain [110]: 17
  with precondition: [F=3,E>=A,A>=C+1] 

* Chain [109]: 17
  with precondition: [F=3,E>=A,A>=C+2] 

* Chain [108]: 17
  with precondition: [F=3,E>=A,A>=C+2] 

* Chain [107]: 18
  with precondition: [F=3,E>=A,A>=C+2] 

* Chain [106]: 18
  with precondition: [F=3,E>=A,A>=C+2] 

* Chain [105]: 19
  with precondition: [F=3,E>=A+1,A>=C+1] 

* Chain [104]: 19
  with precondition: [F=3,E>=A+1,A>=C+1] 

* Chain [103]: 20
  with precondition: [F=3,E>=A+1,A>=C+1] 

* Chain [102]: 20
  with precondition: [F=3,E>=A+1,A>=C+1] 

* Chain [101]: 20
  with precondition: [F=3,E>=A+1,A>=C+2] 

* Chain [100]: 20
  with precondition: [F=3,E>=A+1,A>=C+2] 

* Chain [99]: 21
  with precondition: [F=3,E>=A+1,A>=C+2] 

* Chain [98]: 21
  with precondition: [F=3,E>=A+1,A>=C+2] 

* Chain [97]: 17
  with precondition: [F=3,E>=A+1,E>=C+1] 

* Chain [96]: 17
  with precondition: [F=3,E>=A+1,E>=C+1] 

* Chain [95]: 20
  with precondition: [F=3,E>=A+1,E>=C+1] 

* Chain [94]: 20
  with precondition: [F=3,E>=A+1,E>=C+1] 

* Chain [93]: 20
  with precondition: [F=3,E>=A+1,E>=C+1] 

* Chain [92]: 18
  with precondition: [F=3,E>=A+1,E>=C+1] 

* Chain [91]: 18
  with precondition: [F=3,E>=A+1,E>=C+1] 

* Chain [90]: 21
  with precondition: [F=3,E>=A+1,E>=C+1] 

* Chain [89]: 21
  with precondition: [F=3,E>=A+1,E>=C+1] 

* Chain [88]: 21
  with precondition: [F=3,E>=A+1,E>=C+1] 

* Chain [87]: 18
  with precondition: [F=3,A>=C+1,E>=C] 

* Chain [86]: 19
  with precondition: [F=3,A>=C+1,E>=C] 

* Chain [85]: 19
  with precondition: [F=3,A>=C+1,E>=C] 

* Chain [84]: 19
  with precondition: [F=3,A>=C+1,E>=C] 

* Chain [83]: 20
  with precondition: [F=3,A>=C+1,E>=C] 

* Chain [82]: 20
  with precondition: [F=3,A>=C+1,E>=C] 

* Chain [81]: 19
  with precondition: [F=3,A>=C+2,E>=C+1] 

* Chain [80]: 19
  with precondition: [F=3,A>=C+2,E>=C+1] 

* Chain [79]: 20
  with precondition: [F=3,A>=C+2,E>=C+1] 

* Chain [78]: 20
  with precondition: [F=3,A>=C+2,E>=C+1] 

* Chain [77]: 20
  with precondition: [F=3,A>=C+2,E>=C+1] 

* Chain [76]: 20
  with precondition: [F=3,A>=C+2,E>=C+1] 

* Chain [75]: 20
  with precondition: [F=3,A>=C+2,E>=C+1] 

* Chain [74]: 21
  with precondition: [F=3,A>=C+2,E>=C+1] 

* Chain [73]: 21
  with precondition: [F=3,A>=C+2,E>=C+1] 

* Chain [72]: 21
  with precondition: [F=3,A>=C+2,E>=C+1] 

* Chain [71]: 6*s(1)+6*s(2)+8*s(3)+7*s(4)+7*s(5)+7*s(6)+7*s(7)+7*s(8)+6*s(9)+6*s(10)+4*s(11)+5
  Such that:s(1)+s(2) =< F-2
s(3)+s(4) =< F/2-1
s(5)+s(6)+s(7)+s(8)+s(9)+s(10)+s(11) =< F/2
s(12) >= 1
s(1)+s(2)+s(3)+s(4)+s(5)+s(6)+s(7)+s(8)+s(9)+s(10)+s(11) >= F-1
s(12) >= s(12)
s(5)+s(6)+s(7)+s(8)+s(9)+s(10)+s(11) >= s(4)+s(3)+s(12)

  with precondition: [F>=3] 

* Chain [70]: 6*s(13)+6*s(14)+8*s(15)+7*s(16)+7*s(17)+7*s(18)+7*s(19)+7*s(20)+6*s(21)+6*s(22)+4*s(23)+5
  Such that:s(13)+s(14) =< F-2
s(15)+s(16) =< F/2-1
s(17)+s(18)+s(19)+s(20)+s(21)+s(22)+s(23) =< F/2
s(24) >= 1
s(13)+s(14)+s(15)+s(16)+s(17)+s(18)+s(19)+s(20)+s(21)+s(22)+s(23) >= F-1
s(24) >= s(24)
s(17)+s(18)+s(19)+s(20)+s(21)+s(22)+s(23) >= s(16)+s(15)+s(24)

  with precondition: [F>=3] 

* Chain [69]: 6*s(25)+6*s(26)+8*s(27)+7*s(28)+7*s(29)+7*s(30)+7*s(31)+7*s(32)+6*s(33)+6*s(34)+4*s(35)+13
  Such that:s(25)+s(26) =< F-3
s(27)+s(28) =< F/2-3/2
s(29)+s(30)+s(31)+s(32)+s(33)+s(34)+s(35) =< F/2-1/2
s(36) >= 1
s(25)+s(26)+s(27)+s(28)+s(29)+s(30)+s(31)+s(32)+s(33)+s(34)+s(35) >= F-2
s(36) >= s(36)
s(29)+s(30)+s(31)+s(32)+s(33)+s(34)+s(35) >= s(28)+s(27)+s(36)

  with precondition: [F>=4] 

* Chain [68]: 6*s(37)+6*s(38)+8*s(39)+7*s(40)+7*s(41)+7*s(42)+7*s(43)+7*s(44)+6*s(45)+6*s(46)+4*s(47)+13
  Such that:s(37)+s(38) =< F-3
s(39)+s(40) =< F/2-3/2
s(41)+s(42)+s(43)+s(44)+s(45)+s(46)+s(47) =< F/2-1/2
s(48) >= 1
s(37)+s(38)+s(39)+s(40)+s(41)+s(42)+s(43)+s(44)+s(45)+s(46)+s(47) >= F-2
s(48) >= s(48)
s(41)+s(42)+s(43)+s(44)+s(45)+s(46)+s(47) >= s(40)+s(39)+s(48)

  with precondition: [F>=4] 

* Chain [67]: 6*s(49)+6*s(50)+8*s(51)+7*s(52)+7*s(53)+7*s(54)+7*s(55)+7*s(56)+6*s(57)+6*s(58)+4*s(59)+14
  Such that:s(49)+s(50) =< F-3
s(51)+s(52) =< F/2-3/2
s(53)+s(54)+s(55)+s(56)+s(57)+s(58)+s(59) =< F/2-1/2
s(60) >= 1
s(49)+s(50)+s(51)+s(52)+s(53)+s(54)+s(55)+s(56)+s(57)+s(58)+s(59) >= F-2
s(60) >= s(60)
s(53)+s(54)+s(55)+s(56)+s(57)+s(58)+s(59) >= s(52)+s(51)+s(60)

  with precondition: [F>=4] 

* Chain [66]: 6*s(61)+6*s(62)+8*s(63)+7*s(64)+7*s(65)+7*s(66)+7*s(67)+7*s(68)+6*s(69)+6*s(70)+4*s(71)+14
  Such that:s(61)+s(62) =< F-3
s(63)+s(64) =< F/2-3/2
s(65)+s(66)+s(67)+s(68)+s(69)+s(70)+s(71) =< F/2-1/2
s(72) >= 1
s(61)+s(62)+s(63)+s(64)+s(65)+s(66)+s(67)+s(68)+s(69)+s(70)+s(71) >= F-2
s(72) >= s(72)
s(65)+s(66)+s(67)+s(68)+s(69)+s(70)+s(71) >= s(64)+s(63)+s(72)

  with precondition: [F>=4] 

* Chain [65]: 6*s(73)+6*s(74)+8*s(75)+7*s(76)+7*s(77)+7*s(78)+7*s(79)+7*s(80)+6*s(81)+6*s(82)+4*s(83)+12
  Such that:s(73)+s(74) =< F-3
s(75)+s(76) =< F/2-3/2
s(77)+s(78)+s(79)+s(80)+s(81)+s(82)+s(83) =< F/2-1/2
s(84) >= 1
s(73)+s(74)+s(75)+s(76)+s(77)+s(78)+s(79)+s(80)+s(81)+s(82)+s(83) >= F-2
s(84) >= s(84)
s(77)+s(78)+s(79)+s(80)+s(81)+s(82)+s(83) >= s(76)+s(75)+s(84)

  with precondition: [F>=4,C>=A+1,E>=C] 

* Chain [64]: 6*s(85)+6*s(86)+8*s(87)+7*s(88)+7*s(89)+7*s(90)+7*s(91)+7*s(92)+6*s(93)+6*s(94)+4*s(95)+12
  Such that:s(85)+s(86) =< F-3
s(87)+s(88) =< F/2-3/2
s(89)+s(90)+s(91)+s(92)+s(93)+s(94)+s(95) =< F/2-1/2
s(96) >= 1
s(85)+s(86)+s(87)+s(88)+s(89)+s(90)+s(91)+s(92)+s(93)+s(94)+s(95) >= F-2
s(96) >= s(96)
s(89)+s(90)+s(91)+s(92)+s(93)+s(94)+s(95) >= s(88)+s(87)+s(96)

  with precondition: [F>=4,C>=A+1,E>=C] 

* Chain [63]: 6*s(97)+6*s(98)+8*s(99)+7*s(100)+7*s(101)+7*s(102)+7*s(103)+7*s(104)+6*s(105)+6*s(106)+4*s(107)+13
  Such that:s(97)+s(98) =< F-3
s(99)+s(100) =< F/2-3/2
s(101)+s(102)+s(103)+s(104)+s(105)+s(106)+s(107) =< F/2-1/2
s(108) >= 1
s(97)+s(98)+s(99)+s(100)+s(101)+s(102)+s(103)+s(104)+s(105)+s(106)+s(107) >= F-2
s(108) >= s(108)
s(101)+s(102)+s(103)+s(104)+s(105)+s(106)+s(107) >= s(100)+s(99)+s(108)

  with precondition: [F>=4,C>=A+1,E>=C] 

* Chain [62]: 6*s(109)+6*s(110)+8*s(111)+7*s(112)+7*s(113)+7*s(114)+7*s(115)+7*s(116)+6*s(117)+6*s(118)+4*s(119)+13
  Such that:s(109)+s(110) =< F-3
s(111)+s(112) =< F/2-3/2
s(113)+s(114)+s(115)+s(116)+s(117)+s(118)+s(119) =< F/2-1/2
s(120) >= 1
s(109)+s(110)+s(111)+s(112)+s(113)+s(114)+s(115)+s(116)+s(117)+s(118)+s(119) >= F-2
s(120) >= s(120)
s(113)+s(114)+s(115)+s(116)+s(117)+s(118)+s(119) >= s(112)+s(111)+s(120)

  with precondition: [F>=4,C>=A+1,E>=C] 

* Chain [61]: 6*s(121)+6*s(122)+8*s(123)+7*s(124)+7*s(125)+7*s(126)+7*s(127)+7*s(128)+6*s(129)+6*s(130)+4*s(131)+13
  Such that:s(121)+s(122) =< F-3
s(123)+s(124) =< F/2-3/2
s(125)+s(126)+s(127)+s(128)+s(129)+s(130)+s(131) =< F/2-1/2
s(132) >= 1
s(121)+s(122)+s(123)+s(124)+s(125)+s(126)+s(127)+s(128)+s(129)+s(130)+s(131) >= F-2
s(132) >= s(132)
s(125)+s(126)+s(127)+s(128)+s(129)+s(130)+s(131) >= s(124)+s(123)+s(132)

  with precondition: [F>=4,C>=A+2,E>=A+1] 

* Chain [60]: 6*s(133)+6*s(134)+8*s(135)+7*s(136)+7*s(137)+7*s(138)+7*s(139)+7*s(140)+6*s(141)+6*s(142)+4*s(143)+13
  Such that:s(133)+s(134) =< F-3
s(135)+s(136) =< F/2-3/2
s(137)+s(138)+s(139)+s(140)+s(141)+s(142)+s(143) =< F/2-1/2
s(144) >= 1
s(133)+s(134)+s(135)+s(136)+s(137)+s(138)+s(139)+s(140)+s(141)+s(142)+s(143) >= F-2
s(144) >= s(144)
s(137)+s(138)+s(139)+s(140)+s(141)+s(142)+s(143) >= s(136)+s(135)+s(144)

  with precondition: [F>=4,C>=A+2,E>=A+1] 

* Chain [59]: 6*s(145)+6*s(146)+8*s(147)+7*s(148)+7*s(149)+7*s(150)+7*s(151)+7*s(152)+6*s(153)+6*s(154)+4*s(155)+14
  Such that:s(145)+s(146) =< F-3
s(147)+s(148) =< F/2-3/2
s(149)+s(150)+s(151)+s(152)+s(153)+s(154)+s(155) =< F/2-1/2
s(156) >= 1
s(145)+s(146)+s(147)+s(148)+s(149)+s(150)+s(151)+s(152)+s(153)+s(154)+s(155) >= F-2
s(156) >= s(156)
s(149)+s(150)+s(151)+s(152)+s(153)+s(154)+s(155) >= s(148)+s(147)+s(156)

  with precondition: [F>=4,C>=A+2,E>=A+1] 

* Chain [58]: 6*s(157)+6*s(158)+8*s(159)+7*s(160)+7*s(161)+7*s(162)+7*s(163)+7*s(164)+6*s(165)+6*s(166)+4*s(167)+14
  Such that:s(157)+s(158) =< F-3
s(159)+s(160) =< F/2-3/2
s(161)+s(162)+s(163)+s(164)+s(165)+s(166)+s(167) =< F/2-1/2
s(168) >= 1
s(157)+s(158)+s(159)+s(160)+s(161)+s(162)+s(163)+s(164)+s(165)+s(166)+s(167) >= F-2
s(168) >= s(168)
s(161)+s(162)+s(163)+s(164)+s(165)+s(166)+s(167) >= s(160)+s(159)+s(168)

  with precondition: [F>=4,C>=A+2,E>=A+1] 

* Chain [57]: 6*s(169)+6*s(170)+8*s(171)+7*s(172)+7*s(173)+7*s(174)+7*s(175)+7*s(176)+6*s(177)+6*s(178)+4*s(179)+10
  Such that:s(169)+s(170) =< F-3
s(171)+s(172) =< F/2-3/2
s(173)+s(174)+s(175)+s(176)+s(177)+s(178)+s(179) =< F/2-1/2
s(180) >= 1
s(169)+s(170)+s(171)+s(172)+s(173)+s(174)+s(175)+s(176)+s(177)+s(178)+s(179) >= F-2
s(180) >= s(180)
s(173)+s(174)+s(175)+s(176)+s(177)+s(178)+s(179) >= s(172)+s(171)+s(180)

  with precondition: [F>=4,E>=A] 

* Chain [56]: 6*s(181)+6*s(182)+8*s(183)+7*s(184)+7*s(185)+7*s(186)+7*s(187)+7*s(188)+6*s(189)+6*s(190)+4*s(191)+10
  Such that:s(181)+s(182) =< F-3
s(183)+s(184) =< F/2-3/2
s(185)+s(186)+s(187)+s(188)+s(189)+s(190)+s(191) =< F/2-1/2
s(192) >= 1
s(181)+s(182)+s(183)+s(184)+s(185)+s(186)+s(187)+s(188)+s(189)+s(190)+s(191) >= F-2
s(192) >= s(192)
s(185)+s(186)+s(187)+s(188)+s(189)+s(190)+s(191) >= s(184)+s(183)+s(192)

  with precondition: [F>=4,E>=A] 

* Chain [55]: 6*s(193)+6*s(194)+8*s(195)+7*s(196)+7*s(197)+7*s(198)+7*s(199)+7*s(200)+6*s(201)+6*s(202)+4*s(203)+11
  Such that:s(193)+s(194) =< F-3
s(195)+s(196) =< F/2-3/2
s(197)+s(198)+s(199)+s(200)+s(201)+s(202)+s(203) =< F/2-1/2
s(204) >= 1
s(193)+s(194)+s(195)+s(196)+s(197)+s(198)+s(199)+s(200)+s(201)+s(202)+s(203) >= F-2
s(204) >= s(204)
s(197)+s(198)+s(199)+s(200)+s(201)+s(202)+s(203) >= s(196)+s(195)+s(204)

  with precondition: [F>=4,E>=A] 

* Chain [54]: 6*s(205)+6*s(206)+8*s(207)+7*s(208)+7*s(209)+7*s(210)+7*s(211)+7*s(212)+6*s(213)+6*s(214)+4*s(215)+11
  Such that:s(205)+s(206) =< F-3
s(207)+s(208) =< F/2-3/2
s(209)+s(210)+s(211)+s(212)+s(213)+s(214)+s(215) =< F/2-1/2
s(216) >= 1
s(205)+s(206)+s(207)+s(208)+s(209)+s(210)+s(211)+s(212)+s(213)+s(214)+s(215) >= F-2
s(216) >= s(216)
s(209)+s(210)+s(211)+s(212)+s(213)+s(214)+s(215) >= s(208)+s(207)+s(216)

  with precondition: [F>=4,E>=A] 

* Chain [53]: 6*s(217)+6*s(218)+8*s(219)+7*s(220)+7*s(221)+7*s(222)+7*s(223)+7*s(224)+6*s(225)+6*s(226)+4*s(227)+13
  Such that:s(217)+s(218) =< F-3
s(219)+s(220) =< F/2-3/2
s(221)+s(222)+s(223)+s(224)+s(225)+s(226)+s(227) =< F/2-1/2
s(228) >= 1
s(217)+s(218)+s(219)+s(220)+s(221)+s(222)+s(223)+s(224)+s(225)+s(226)+s(227) >= F-2
s(228) >= s(228)
s(221)+s(222)+s(223)+s(224)+s(225)+s(226)+s(227) >= s(220)+s(219)+s(228)

  with precondition: [F>=4,E>=A+1,E>=C+1] 

* Chain [52]: 6*s(229)+6*s(230)+8*s(231)+7*s(232)+7*s(233)+7*s(234)+7*s(235)+7*s(236)+6*s(237)+6*s(238)+4*s(239)+13
  Such that:s(229)+s(230) =< F-3
s(231)+s(232) =< F/2-3/2
s(233)+s(234)+s(235)+s(236)+s(237)+s(238)+s(239) =< F/2-1/2
s(240) >= 1
s(229)+s(230)+s(231)+s(232)+s(233)+s(234)+s(235)+s(236)+s(237)+s(238)+s(239) >= F-2
s(240) >= s(240)
s(233)+s(234)+s(235)+s(236)+s(237)+s(238)+s(239) >= s(232)+s(231)+s(240)

  with precondition: [F>=4,E>=A+1,E>=C+1] 

* Chain [51]: 6*s(241)+6*s(242)+8*s(243)+7*s(244)+7*s(245)+7*s(246)+7*s(247)+7*s(248)+6*s(249)+6*s(250)+4*s(251)+14
  Such that:s(241)+s(242) =< F-3
s(243)+s(244) =< F/2-3/2
s(245)+s(246)+s(247)+s(248)+s(249)+s(250)+s(251) =< F/2-1/2
s(252) >= 1
s(241)+s(242)+s(243)+s(244)+s(245)+s(246)+s(247)+s(248)+s(249)+s(250)+s(251) >= F-2
s(252) >= s(252)
s(245)+s(246)+s(247)+s(248)+s(249)+s(250)+s(251) >= s(244)+s(243)+s(252)

  with precondition: [F>=4,E>=A+1,E>=C+1] 

* Chain [50]: 6*s(253)+6*s(254)+8*s(255)+7*s(256)+7*s(257)+7*s(258)+7*s(259)+7*s(260)+6*s(261)+6*s(262)+4*s(263)+14
  Such that:s(253)+s(254) =< F-3
s(255)+s(256) =< F/2-3/2
s(257)+s(258)+s(259)+s(260)+s(261)+s(262)+s(263) =< F/2-1/2
s(264) >= 1
s(253)+s(254)+s(255)+s(256)+s(257)+s(258)+s(259)+s(260)+s(261)+s(262)+s(263) >= F-2
s(264) >= s(264)
s(257)+s(258)+s(259)+s(260)+s(261)+s(262)+s(263) >= s(256)+s(255)+s(264)

  with precondition: [F>=4,E>=A+1,E>=C+1] 

* Chain [49]: 6*s(265)+6*s(266)+8*s(267)+7*s(268)+7*s(269)+7*s(270)+7*s(271)+7*s(272)+6*s(273)+6*s(274)+4*s(275)+12
  Such that:s(265)+s(266) =< F-3
s(267)+s(268) =< F/2-3/2
s(269)+s(270)+s(271)+s(272)+s(273)+s(274)+s(275) =< F/2-1/2
s(276) >= 1
s(265)+s(266)+s(267)+s(268)+s(269)+s(270)+s(271)+s(272)+s(273)+s(274)+s(275) >= F-2
s(276) >= s(276)
s(269)+s(270)+s(271)+s(272)+s(273)+s(274)+s(275) >= s(268)+s(267)+s(276)

  with precondition: [F>=4,A>=C+1,E>=C] 

* Chain [48]: 6*s(277)+6*s(278)+8*s(279)+7*s(280)+7*s(281)+7*s(282)+7*s(283)+7*s(284)+6*s(285)+6*s(286)+4*s(287)+12
  Such that:s(277)+s(278) =< F-3
s(279)+s(280) =< F/2-3/2
s(281)+s(282)+s(283)+s(284)+s(285)+s(286)+s(287) =< F/2-1/2
s(288) >= 1
s(277)+s(278)+s(279)+s(280)+s(281)+s(282)+s(283)+s(284)+s(285)+s(286)+s(287) >= F-2
s(288) >= s(288)
s(281)+s(282)+s(283)+s(284)+s(285)+s(286)+s(287) >= s(280)+s(279)+s(288)

  with precondition: [F>=4,A>=C+1,E>=C] 

* Chain [47]: 6*s(289)+6*s(290)+8*s(291)+7*s(292)+7*s(293)+7*s(294)+7*s(295)+7*s(296)+6*s(297)+6*s(298)+4*s(299)+13
  Such that:s(289)+s(290) =< F-3
s(291)+s(292) =< F/2-3/2
s(293)+s(294)+s(295)+s(296)+s(297)+s(298)+s(299) =< F/2-1/2
s(300) >= 1
s(289)+s(290)+s(291)+s(292)+s(293)+s(294)+s(295)+s(296)+s(297)+s(298)+s(299) >= F-2
s(300) >= s(300)
s(293)+s(294)+s(295)+s(296)+s(297)+s(298)+s(299) >= s(292)+s(291)+s(300)

  with precondition: [F>=4,A>=C+1,E>=C] 

* Chain [46]: 6*s(301)+6*s(302)+8*s(303)+7*s(304)+7*s(305)+7*s(306)+7*s(307)+7*s(308)+6*s(309)+6*s(310)+4*s(311)+13
  Such that:s(301)+s(302) =< F-3
s(303)+s(304) =< F/2-3/2
s(305)+s(306)+s(307)+s(308)+s(309)+s(310)+s(311) =< F/2-1/2
s(312) >= 1
s(301)+s(302)+s(303)+s(304)+s(305)+s(306)+s(307)+s(308)+s(309)+s(310)+s(311) >= F-2
s(312) >= s(312)
s(305)+s(306)+s(307)+s(308)+s(309)+s(310)+s(311) >= s(304)+s(303)+s(312)

  with precondition: [F>=4,A>=C+1,E>=C] 

* Chain [45]: 6*s(313)+6*s(314)+8*s(315)+7*s(316)+7*s(317)+7*s(318)+7*s(319)+7*s(320)+6*s(321)+6*s(322)+4*s(323)+13
  Such that:s(313)+s(314) =< F-3
s(315)+s(316) =< F/2-3/2
s(317)+s(318)+s(319)+s(320)+s(321)+s(322)+s(323) =< F/2-1/2
s(324) >= 1
s(313)+s(314)+s(315)+s(316)+s(317)+s(318)+s(319)+s(320)+s(321)+s(322)+s(323) >= F-2
s(324) >= s(324)
s(317)+s(318)+s(319)+s(320)+s(321)+s(322)+s(323) >= s(316)+s(315)+s(324)

  with precondition: [F>=4,A>=C+2,E>=C+1] 

* Chain [44]: 6*s(325)+6*s(326)+8*s(327)+7*s(328)+7*s(329)+7*s(330)+7*s(331)+7*s(332)+6*s(333)+6*s(334)+4*s(335)+13
  Such that:s(325)+s(326) =< F-3
s(327)+s(328) =< F/2-3/2
s(329)+s(330)+s(331)+s(332)+s(333)+s(334)+s(335) =< F/2-1/2
s(336) >= 1
s(325)+s(326)+s(327)+s(328)+s(329)+s(330)+s(331)+s(332)+s(333)+s(334)+s(335) >= F-2
s(336) >= s(336)
s(329)+s(330)+s(331)+s(332)+s(333)+s(334)+s(335) >= s(328)+s(327)+s(336)

  with precondition: [F>=4,A>=C+2,E>=C+1] 

* Chain [43]: 6*s(337)+6*s(338)+8*s(339)+7*s(340)+7*s(341)+7*s(342)+7*s(343)+7*s(344)+6*s(345)+6*s(346)+4*s(347)+14
  Such that:s(337)+s(338) =< F-3
s(339)+s(340) =< F/2-3/2
s(341)+s(342)+s(343)+s(344)+s(345)+s(346)+s(347) =< F/2-1/2
s(348) >= 1
s(337)+s(338)+s(339)+s(340)+s(341)+s(342)+s(343)+s(344)+s(345)+s(346)+s(347) >= F-2
s(348) >= s(348)
s(341)+s(342)+s(343)+s(344)+s(345)+s(346)+s(347) >= s(340)+s(339)+s(348)

  with precondition: [F>=4,A>=C+2,E>=C+1] 

* Chain [42]: 6*s(349)+6*s(350)+8*s(351)+7*s(352)+7*s(353)+7*s(354)+7*s(355)+7*s(356)+6*s(357)+6*s(358)+4*s(359)+14
  Such that:s(349)+s(350) =< F-3
s(351)+s(352) =< F/2-3/2
s(353)+s(354)+s(355)+s(356)+s(357)+s(358)+s(359) =< F/2-1/2
s(360) >= 1
s(349)+s(350)+s(351)+s(352)+s(353)+s(354)+s(355)+s(356)+s(357)+s(358)+s(359) >= F-2
s(360) >= s(360)
s(353)+s(354)+s(355)+s(356)+s(357)+s(358)+s(359) >= s(352)+s(351)+s(360)

  with precondition: [F>=4,A>=C+2,E>=C+1] 

* Chain [41]: 6*s(361)+6*s(362)+8*s(363)+7*s(364)+7*s(365)+7*s(366)+7*s(367)+7*s(368)+6*s(369)+6*s(370)+4*s(371)+6*s(373)+6*s(374)+8*s(375)+7*s(376)+7*s(377)+7*s(378)+7*s(379)+7*s(380)+6*s(381)+6*s(382)+4*s(383)+6
  Such that:s(365)+s(366)+s(367)+s(368)+s(369)+s(370)+s(371)+s(377)+s(378)+s(379)+s(380)+s(381)+s(382)+s(383) =< F/2+1/2
aux(7) =< F-1
aux(8) =< F/2-1/2
s(361)+s(362) =< aux(7)
s(373)+s(374) =< aux(7)
s(363)+s(364) =< aux(8)
s(375)+s(376) =< aux(8)
s(361)+s(362)+s(363)+s(364)+s(365)+s(366)+s(367)+s(368)+s(369)+s(370)+s(371)+s(373)+s(374)+s(375)+s(376)+s(377)+s(378)+s(379)+s(380)+s(381)+s(382)+s(383) >= F-1
aux(9) >= 1
aux(10) >= 2
s(372) >= aux(9)
s(384) >= aux(9)
s(361)+s(362)+s(363)+s(364)+s(365)+s(366)+s(367)+s(368)+s(369)+s(370)+s(371) >= aux(10)
s(373)+s(374)+s(375)+s(376)+s(377)+s(378)+s(379)+s(380)+s(381)+s(382)+s(383) >= aux(10)
s(384) >= s(384)
s(377)+s(378)+s(379)+s(380)+s(381)+s(382)+s(383) >= s(376)+s(375)+s(384)
s(372) >= s(372)
s(365)+s(366)+s(367)+s(368)+s(369)+s(370)+s(371) >= s(364)+s(363)+s(372)

  with precondition: [F>=5] 

* Chain [40]: 6*s(385)+6*s(386)+8*s(387)+7*s(388)+7*s(389)+7*s(390)+7*s(391)+7*s(392)+6*s(393)+6*s(394)+4*s(395)+6*s(397)+6*s(398)+8*s(399)+7*s(400)+7*s(401)+7*s(402)+7*s(403)+7*s(404)+6*s(405)+6*s(406)+4*s(407)+7
  Such that:s(389)+s(390)+s(391)+s(392)+s(393)+s(394)+s(395)+s(401)+s(402)+s(403)+s(404)+s(405)+s(406)+s(407) =< F/2+1/2
aux(11) =< F-1
aux(12) =< F/2-1/2
s(385)+s(386) =< aux(11)
s(397)+s(398) =< aux(11)
s(387)+s(388) =< aux(12)
s(399)+s(400) =< aux(12)
s(385)+s(386)+s(387)+s(388)+s(389)+s(390)+s(391)+s(392)+s(393)+s(394)+s(395)+s(397)+s(398)+s(399)+s(400)+s(401)+s(402)+s(403)+s(404)+s(405)+s(406)+s(407) >= F-1
aux(13) >= 1
aux(14) >= 2
s(396) >= aux(13)
s(408) >= aux(13)
s(385)+s(386)+s(387)+s(388)+s(389)+s(390)+s(391)+s(392)+s(393)+s(394)+s(395) >= aux(14)
s(397)+s(398)+s(399)+s(400)+s(401)+s(402)+s(403)+s(404)+s(405)+s(406)+s(407) >= aux(14)
s(408) >= s(408)
s(401)+s(402)+s(403)+s(404)+s(405)+s(406)+s(407) >= s(400)+s(399)+s(408)
s(396) >= s(396)
s(389)+s(390)+s(391)+s(392)+s(393)+s(394)+s(395) >= s(388)+s(387)+s(396)

  with precondition: [F>=5] 


Closed-form bounds of case_0(A,B,C,D,E,F): 
-------------------------------------
* Chain [174] with precondition: [F=1,E=A] 
    - Lower bound: 3 
    - Complexity: constant
 * Chain [173] with precondition: [F=1,C=E,C>=A+1] 
    - Lower bound: 5 
    - Complexity: constant
 * Chain [172] with precondition: [F=1,C=E,A>=C+1] 
    - Lower bound: 5 
    - Complexity: constant
 * Chain [171] with precondition: [F=1,E>=A+1,E>=C+1] 
    - Lower bound: 6 
    - Complexity: constant
 * Chain [170] with precondition: [F=1,E>=A+1,C>=E+1] 
    - Lower bound: 6 
    - Complexity: constant
 * Chain [169] with precondition: [F=1,E>=C+1,A>=E+1] 
    - Lower bound: 6 
    - Complexity: constant
 * Chain [168] with precondition: [F=1,A>=E+1,C>=E+1] 
    - Lower bound: 6 
    - Complexity: constant
 * Chain [167] with precondition: [F=2,E=A] 
    - Lower bound: 9 
    - Complexity: constant
 * Chain [166] with precondition: [F=2,E=A] 
    - Lower bound: 9 
    - Complexity: constant
 * Chain [165] with precondition: [F=2,C=E,C>=A+1] 
    - Lower bound: 11 
    - Complexity: constant
 * Chain [164] with precondition: [F=2,C=E,C>=A+1] 
    - Lower bound: 11 
    - Complexity: constant
 * Chain [163] with precondition: [F=2,C=E,A>=C+1] 
    - Lower bound: 11 
    - Complexity: constant
 * Chain [162] with precondition: [F=2,C=E,A>=C+1] 
    - Lower bound: 11 
    - Complexity: constant
 * Chain [161] with precondition: [F=2,E>=A+1,E>=C+1] 
    - Lower bound: 12 
    - Complexity: constant
 * Chain [160] with precondition: [F=2,E>=A+1,E>=C+1] 
    - Lower bound: 12 
    - Complexity: constant
 * Chain [159] with precondition: [F=2,E>=A+1,C>=E+1] 
    - Lower bound: 12 
    - Complexity: constant
 * Chain [158] with precondition: [F=2,E>=A+1,C>=E+1] 
    - Lower bound: 12 
    - Complexity: constant
 * Chain [157] with precondition: [F=2,E>=C+1,A>=E+1] 
    - Lower bound: 12 
    - Complexity: constant
 * Chain [156] with precondition: [F=2,E>=C+1,A>=E+1] 
    - Lower bound: 12 
    - Complexity: constant
 * Chain [155] with precondition: [F=2,A>=E+1,C>=E+1] 
    - Lower bound: 12 
    - Complexity: constant
 * Chain [154] with precondition: [F=2,A>=E+1,C>=E+1] 
    - Lower bound: 12 
    - Complexity: constant
 * Chain [153] with precondition: [F=3] 
    - Lower bound: 20 
    - Complexity: constant
 * Chain [152] with precondition: [F=3] 
    - Lower bound: 21 
    - Complexity: constant
 * Chain [151] with precondition: [F=3,C>=A+1,E>=C] 
    - Lower bound: 16 
    - Complexity: constant
 * Chain [150] with precondition: [F=3,C>=A+1,E>=C] 
    - Lower bound: 16 
    - Complexity: constant
 * Chain [149] with precondition: [F=3,C>=A+1,E>=C] 
    - Lower bound: 18 
    - Complexity: constant
 * Chain [148] with precondition: [F=3,C>=A+1,E>=C] 
    - Lower bound: 19 
    - Complexity: constant
 * Chain [147] with precondition: [F=3,C>=A+1,E>=C] 
    - Lower bound: 19 
    - Complexity: constant
 * Chain [146] with precondition: [F=3,C>=A+1,E>=C] 
    - Lower bound: 17 
    - Complexity: constant
 * Chain [145] with precondition: [F=3,C>=A+1,E>=C] 
    - Lower bound: 17 
    - Complexity: constant
 * Chain [144] with precondition: [F=3,C>=A+1,E>=C] 
    - Lower bound: 19 
    - Complexity: constant
 * Chain [143] with precondition: [F=3,C>=A+1,E>=C] 
    - Lower bound: 20 
    - Complexity: constant
 * Chain [142] with precondition: [F=3,C>=A+1,E>=C] 
    - Lower bound: 20 
    - Complexity: constant
 * Chain [141] with precondition: [F=3,C>=A+1,E>=C+1] 
    - Lower bound: 19 
    - Complexity: constant
 * Chain [140] with precondition: [F=3,C>=A+1,E>=C+1] 
    - Lower bound: 19 
    - Complexity: constant
 * Chain [139] with precondition: [F=3,C>=A+1,E>=C+1] 
    - Lower bound: 20 
    - Complexity: constant
 * Chain [138] with precondition: [F=3,C>=A+1,E>=C+1] 
    - Lower bound: 20 
    - Complexity: constant
 * Chain [137] with precondition: [F=3,C>=A+2,E>=A+1] 
    - Lower bound: 17 
    - Complexity: constant
 * Chain [136] with precondition: [F=3,C>=A+2,E>=A+1] 
    - Lower bound: 17 
    - Complexity: constant
 * Chain [135] with precondition: [F=3,C>=A+2,E>=A+1] 
    - Lower bound: 20 
    - Complexity: constant
 * Chain [134] with precondition: [F=3,C>=A+2,E>=A+1] 
    - Lower bound: 20 
    - Complexity: constant
 * Chain [133] with precondition: [F=3,C>=A+2,E>=A+1] 
    - Lower bound: 20 
    - Complexity: constant
 * Chain [132] with precondition: [F=3,C>=A+2,E>=A+1] 
    - Lower bound: 18 
    - Complexity: constant
 * Chain [131] with precondition: [F=3,C>=A+2,E>=A+1] 
    - Lower bound: 18 
    - Complexity: constant
 * Chain [130] with precondition: [F=3,C>=A+2,E>=A+1] 
    - Lower bound: 21 
    - Complexity: constant
 * Chain [129] with precondition: [F=3,C>=A+2,E>=A+1] 
    - Lower bound: 21 
    - Complexity: constant
 * Chain [128] with precondition: [F=3,C>=A+2,E>=A+1] 
    - Lower bound: 21 
    - Complexity: constant
 * Chain [127] with precondition: [F=3,C>=A+2,E>=C] 
    - Lower bound: 19 
    - Complexity: constant
 * Chain [126] with precondition: [F=3,C>=A+2,E>=C] 
    - Lower bound: 19 
    - Complexity: constant
 * Chain [125] with precondition: [F=3,C>=A+2,E>=C] 
    - Lower bound: 20 
    - Complexity: constant
 * Chain [124] with precondition: [F=3,C>=A+2,E>=C] 
    - Lower bound: 20 
    - Complexity: constant
 * Chain [123] with precondition: [F=3,C>=A+2,E>=C+1] 
    - Lower bound: 20 
    - Complexity: constant
 * Chain [122] with precondition: [F=3,C>=A+2,E>=C+1] 
    - Lower bound: 20 
    - Complexity: constant
 * Chain [121] with precondition: [F=3,C>=A+2,E>=C+1] 
    - Lower bound: 21 
    - Complexity: constant
 * Chain [120] with precondition: [F=3,C>=A+2,E>=C+1] 
    - Lower bound: 21 
    - Complexity: constant
 * Chain [119] with precondition: [F=3,E>=A] 
    - Lower bound: 14 
    - Complexity: constant
 * Chain [118] with precondition: [F=3,E>=A] 
    - Lower bound: 17 
    - Complexity: constant
 * Chain [117] with precondition: [F=3,E>=A] 
    - Lower bound: 17 
    - Complexity: constant
 * Chain [116] with precondition: [F=3,E>=A] 
    - Lower bound: 15 
    - Complexity: constant
 * Chain [115] with precondition: [F=3,E>=A] 
    - Lower bound: 18 
    - Complexity: constant
 * Chain [114] with precondition: [F=3,E>=A] 
    - Lower bound: 18 
    - Complexity: constant
 * Chain [113] with precondition: [F=3,E>=A,A>=C+1] 
    - Lower bound: 16 
    - Complexity: constant
 * Chain [112] with precondition: [F=3,E>=A,A>=C+1] 
    - Lower bound: 16 
    - Complexity: constant
 * Chain [111] with precondition: [F=3,E>=A,A>=C+1] 
    - Lower bound: 17 
    - Complexity: constant
 * Chain [110] with precondition: [F=3,E>=A,A>=C+1] 
    - Lower bound: 17 
    - Complexity: constant
 * Chain [109] with precondition: [F=3,E>=A,A>=C+2] 
    - Lower bound: 17 
    - Complexity: constant
 * Chain [108] with precondition: [F=3,E>=A,A>=C+2] 
    - Lower bound: 17 
    - Complexity: constant
 * Chain [107] with precondition: [F=3,E>=A,A>=C+2] 
    - Lower bound: 18 
    - Complexity: constant
 * Chain [106] with precondition: [F=3,E>=A,A>=C+2] 
    - Lower bound: 18 
    - Complexity: constant
 * Chain [105] with precondition: [F=3,E>=A+1,A>=C+1] 
    - Lower bound: 19 
    - Complexity: constant
 * Chain [104] with precondition: [F=3,E>=A+1,A>=C+1] 
    - Lower bound: 19 
    - Complexity: constant
 * Chain [103] with precondition: [F=3,E>=A+1,A>=C+1] 
    - Lower bound: 20 
    - Complexity: constant
 * Chain [102] with precondition: [F=3,E>=A+1,A>=C+1] 
    - Lower bound: 20 
    - Complexity: constant
 * Chain [101] with precondition: [F=3,E>=A+1,A>=C+2] 
    - Lower bound: 20 
    - Complexity: constant
 * Chain [100] with precondition: [F=3,E>=A+1,A>=C+2] 
    - Lower bound: 20 
    - Complexity: constant
 * Chain [99] with precondition: [F=3,E>=A+1,A>=C+2] 
    - Lower bound: 21 
    - Complexity: constant
 * Chain [98] with precondition: [F=3,E>=A+1,A>=C+2] 
    - Lower bound: 21 
    - Complexity: constant
 * Chain [97] with precondition: [F=3,E>=A+1,E>=C+1] 
    - Lower bound: 17 
    - Complexity: constant
 * Chain [96] with precondition: [F=3,E>=A+1,E>=C+1] 
    - Lower bound: 17 
    - Complexity: constant
 * Chain [95] with precondition: [F=3,E>=A+1,E>=C+1] 
    - Lower bound: 20 
    - Complexity: constant
 * Chain [94] with precondition: [F=3,E>=A+1,E>=C+1] 
    - Lower bound: 20 
    - Complexity: constant
 * Chain [93] with precondition: [F=3,E>=A+1,E>=C+1] 
    - Lower bound: 20 
    - Complexity: constant
 * Chain [92] with precondition: [F=3,E>=A+1,E>=C+1] 
    - Lower bound: 18 
    - Complexity: constant
 * Chain [91] with precondition: [F=3,E>=A+1,E>=C+1] 
    - Lower bound: 18 
    - Complexity: constant
 * Chain [90] with precondition: [F=3,E>=A+1,E>=C+1] 
    - Lower bound: 21 
    - Complexity: constant
 * Chain [89] with precondition: [F=3,E>=A+1,E>=C+1] 
    - Lower bound: 21 
    - Complexity: constant
 * Chain [88] with precondition: [F=3,E>=A+1,E>=C+1] 
    - Lower bound: 21 
    - Complexity: constant
 * Chain [87] with precondition: [F=3,A>=C+1,E>=C] 
    - Lower bound: 18 
    - Complexity: constant
 * Chain [86] with precondition: [F=3,A>=C+1,E>=C] 
    - Lower bound: 19 
    - Complexity: constant
 * Chain [85] with precondition: [F=3,A>=C+1,E>=C] 
    - Lower bound: 19 
    - Complexity: constant
 * Chain [84] with precondition: [F=3,A>=C+1,E>=C] 
    - Lower bound: 19 
    - Complexity: constant
 * Chain [83] with precondition: [F=3,A>=C+1,E>=C] 
    - Lower bound: 20 
    - Complexity: constant
 * Chain [82] with precondition: [F=3,A>=C+1,E>=C] 
    - Lower bound: 20 
    - Complexity: constant
 * Chain [81] with precondition: [F=3,A>=C+2,E>=C+1] 
    - Lower bound: 19 
    - Complexity: constant
 * Chain [80] with precondition: [F=3,A>=C+2,E>=C+1] 
    - Lower bound: 19 
    - Complexity: constant
 * Chain [79] with precondition: [F=3,A>=C+2,E>=C+1] 
    - Lower bound: 20 
    - Complexity: constant
 * Chain [78] with precondition: [F=3,A>=C+2,E>=C+1] 
    - Lower bound: 20 
    - Complexity: constant
 * Chain [77] with precondition: [F=3,A>=C+2,E>=C+1] 
    - Lower bound: 20 
    - Complexity: constant
 * Chain [76] with precondition: [F=3,A>=C+2,E>=C+1] 
    - Lower bound: 20 
    - Complexity: constant
 * Chain [75] with precondition: [F=3,A>=C+2,E>=C+1] 
    - Lower bound: 20 
    - Complexity: constant
 * Chain [74] with precondition: [F=3,A>=C+2,E>=C+1] 
    - Lower bound: 21 
    - Complexity: constant
 * Chain [73] with precondition: [F=3,A>=C+2,E>=C+1] 
    - Lower bound: 21 
    - Complexity: constant
 * Chain [72] with precondition: [F=3,A>=C+2,E>=C+1] 
    - Lower bound: 21 
    - Complexity: constant
 * Chain [71] with precondition: [F>=3] 
    - Lower bound: 4*F+1 
    - Complexity: n
 * Chain [70] with precondition: [F>=3] 
    - Lower bound: 4*F+1 
    - Complexity: n
 * Chain [69] with precondition: [F>=4] 
    - Lower bound: 4*F+5 
    - Complexity: n
 * Chain [68] with precondition: [F>=4] 
    - Lower bound: 4*F+5 
    - Complexity: n
 * Chain [67] with precondition: [F>=4] 
    - Lower bound: 4*F+6 
    - Complexity: n
 * Chain [66] with precondition: [F>=4] 
    - Lower bound: 4*F+6 
    - Complexity: n
 * Chain [65] with precondition: [F>=4,C>=A+1,E>=C] 
    - Lower bound: 4*F+4 
    - Complexity: n
 * Chain [64] with precondition: [F>=4,C>=A+1,E>=C] 
    - Lower bound: 4*F+4 
    - Complexity: n
 * Chain [63] with precondition: [F>=4,C>=A+1,E>=C] 
    - Lower bound: 4*F+5 
    - Complexity: n
 * Chain [62] with precondition: [F>=4,C>=A+1,E>=C] 
    - Lower bound: 4*F+5 
    - Complexity: n
 * Chain [61] with precondition: [F>=4,C>=A+2,E>=A+1] 
    - Lower bound: 4*F+5 
    - Complexity: n
 * Chain [60] with precondition: [F>=4,C>=A+2,E>=A+1] 
    - Lower bound: 4*F+5 
    - Complexity: n
 * Chain [59] with precondition: [F>=4,C>=A+2,E>=A+1] 
    - Lower bound: 4*F+6 
    - Complexity: n
 * Chain [58] with precondition: [F>=4,C>=A+2,E>=A+1] 
    - Lower bound: 4*F+6 
    - Complexity: n
 * Chain [57] with precondition: [F>=4,E>=A] 
    - Lower bound: 4*F+2 
    - Complexity: n
 * Chain [56] with precondition: [F>=4,E>=A] 
    - Lower bound: 4*F+2 
    - Complexity: n
 * Chain [55] with precondition: [F>=4,E>=A] 
    - Lower bound: 4*F+3 
    - Complexity: n
 * Chain [54] with precondition: [F>=4,E>=A] 
    - Lower bound: 4*F+3 
    - Complexity: n
 * Chain [53] with precondition: [F>=4,E>=A+1,E>=C+1] 
    - Lower bound: 4*F+5 
    - Complexity: n
 * Chain [52] with precondition: [F>=4,E>=A+1,E>=C+1] 
    - Lower bound: 4*F+5 
    - Complexity: n
 * Chain [51] with precondition: [F>=4,E>=A+1,E>=C+1] 
    - Lower bound: 4*F+6 
    - Complexity: n
 * Chain [50] with precondition: [F>=4,E>=A+1,E>=C+1] 
    - Lower bound: 4*F+6 
    - Complexity: n
 * Chain [49] with precondition: [F>=4,A>=C+1,E>=C] 
    - Lower bound: 4*F+4 
    - Complexity: n
 * Chain [48] with precondition: [F>=4,A>=C+1,E>=C] 
    - Lower bound: 4*F+4 
    - Complexity: n
 * Chain [47] with precondition: [F>=4,A>=C+1,E>=C] 
    - Lower bound: 4*F+5 
    - Complexity: n
 * Chain [46] with precondition: [F>=4,A>=C+1,E>=C] 
    - Lower bound: 4*F+5 
    - Complexity: n
 * Chain [45] with precondition: [F>=4,A>=C+2,E>=C+1] 
    - Lower bound: 4*F+5 
    - Complexity: n
 * Chain [44] with precondition: [F>=4,A>=C+2,E>=C+1] 
    - Lower bound: 4*F+5 
    - Complexity: n
 * Chain [43] with precondition: [F>=4,A>=C+2,E>=C+1] 
    - Lower bound: 4*F+6 
    - Complexity: n
 * Chain [42] with precondition: [F>=4,A>=C+2,E>=C+1] 
    - Lower bound: 4*F+6 
    - Complexity: n
 * Chain [41] with precondition: [F>=5] 
    - Lower bound: 4*F+2 
    - Complexity: n
 * Chain [40] with precondition: [F>=5] 
    - Lower bound: 4*F+3 
    - Complexity: n
 
### Partitioned lower bound of case_0(A,B,C,D,E,F): 
* 3 
 if [F=1,A=E]
* 5 
 if [F=1,E=C,E>=A+1]
 or [F=1,E=C,A>=E+1]
* 6 
 if [F=1,E>=A+1,E>=C+1]
 or [F=1,E>=A+1,C>=E+1]
 or [F=1,A>=E+1,C>=E+1]
 or [F=1,E>=C+1,A>=E+1]
* 9 
 if [F=2,A=E]
* 11 
 if [F=2,E=C,E>=A+1]
 or [F=2,E=C,A>=E+1]
* 12 
 if [F=2,E>=C+1,A>=E+1]
 or [F=2,E>=A+1,E>=C+1]
 or [F=2,E>=A+1,C>=E+1]
 or [F=2,A>=E+1,C>=E+1]
* 4*F+1 
 if [F>=3,E>=A+1,C>=E+1]
 or [F>=3,E>=C+1,A>=E+1]
 or [F>=3,E>=A+1,A>=C+1]
 or [C=E,F>=3,A>=C+1]
 or [A+1=C,F>=3,E>=A]
 or [A=C,F>=3,E>=A]
 or [F>=3,C>=A+2,E>=C]
 or [F>=3,A>=C,C>=E+1]
 or [F>=3,C>=A+1,A>=E+1]
Possible lower bounds : [3,5,6,9,11,12,4*F+1]
Maximum lower bound complexity: n
* Total analysis performed in 998 ms.