Abs program loaded in 3 ms.

Rule based representation generated in 2 ms.

Rule based representation stored in /tmp/costabs/rbr.rbr

RBR properties stored in /tmp/costabs/rbr.properties

Class invariants generated and loaded in 0 ms.
Size abstraction not supported for native

Abstract compilation performed in 8 ms.
sabu_memo_table_1(case_0,[A,B,C],[1*A>=0,1*C=1,1*A=1],0,0)
sabu_memo_table_1(firstline,[A,B,C],[1*A>=0,1*A=1,1*C=1,1*A>=0],0,0)
sabu_memo_table_1(case_0,[A,B,C],[-1*C>= -2,1*C>=1,1*A+ -1*C=0],1,1)
sabu_memo_table_1(firstline,[A,B,C],[-1*C>= -2,1*C>=1,1*A+ -1*C=0],2,1)
sabu_memo_table_1(case_0,[A,B,C],[-1*A>= -3,1*A>=1,1*A+ -1*C=0],3,2)
sabu_memo_table_1(firstline,[A,B,C],[-1*A>= -3,1*A>=1,1*A+ -1*C=0],4,2)
sabu_memo_table_1(case_0,[A,B,C],[-1*A>= -4,1*A>=1,1*A+ -1*C=0],5,3)
sabu_memo_table_1(firstline,[A,B,C],[-1*A>= -4,1*A>=1,1*A+ -1*C=0],6,3)
sabu_memo_table_1(case_0,[A,B,C],[1*A+ -1*C=0,1*A>=1],7,0)
sabu_memo_table_1(firstline,[A,B,C],[1*A+ -1*C=0,1*A>=1],8,0)
sabu_memo_table_1(case_1,[A,B,C],[1*B>=0,1*C=0,1*B=1],0,0)
sabu_memo_table_1(case_1,[A,B,C],[1*B>=1],0,1)
sabu_memo_table_1(case_9,[A,B,C],[-1*B+1*C>=1,1*A+ -1*C=0],0,0)
sabu_memo_table_1(case_9,[A,B,C],[-1*B+1*C>=0,-1*A+1*C>=0],0,1)
sabu_memo_table_1(max,[A,B,C],[-1*A+1*C>=0,-1*B+1*C>=0],0,0)
sabu_memo_table_1(case_4,[A,B,C,D,E,F],[1*A+ -1*F= -1,1*C+ -1*D=0],0,0)
sabu_memo_table_1(case_4,[A,B,C,D,E,F],[-1*C+1*D>=0],0,1)
sabu_memo_table_1(case_4,[A,B,C,D,E,F],[],0,2)
sabu_memo_table_1(head_or_zero,[A,B,C],[1*B>=0,1*B>=1],0,0)
sabu_memo_table_1(case_2,[A,B,C,D,E,F,G],[1*E>=0,1*C>=0,1*G=1,1*E=1],0,0)
sabu_memo_table_1(case_3,[A,B,C,D,E,F,G,H],[1*F>=0,1*C>=0,1*H=1,1*C=1],0,0)
sabu_memo_table_1(newline,[A,B,C,D,E,F,G],[1*E>=0,1*C>=0,1*E=1,1*G=1,1*C>=0,1*E>=0],0,0)
sabu_memo_table_1(case_2,[A,B,C,D,E,F,G],[1*C>=0,1*E>=1,1*G=1],1,1)
sabu_memo_table_1(case_3,[A,B,C,D,E,F,G,H],[1*F+ -1*H>= -1,-1*H>= -2,1*C+ -1*H>=0,1*H>=1],1,1)
sabu_memo_table_1(case_2,[A,B,C,D,E,F,G],[1*C+ -2*G>= -2,-1*G>= -2,1*E+ -1*G>=0,1*G>=1],2,2)
sabu_memo_table_1(newline,[A,B,C,D,E,F,G],[1*C+ -2*G>= -2,-1*G>= -2,1*E+ -1*G>=0,1*G>=1],3,1)
sabu_memo_table_1(case_3,[A,B,C,D,E,F,G,H],[1*C+ -2*H>= -3,3*C+ -2*H>=1,1*H>=1,-1*H>= -3,1*F+ -1*H>= -1],4,2)
sabu_memo_table_1(case_2,[A,B,C,D,E,F,G],[3*C+ -4*G>= -4,1*C+ -2*G>= -3,-1*G>= -3,1*G>=1,1*E+ -1*G>=0],5,3)
sabu_memo_table_1(newline,[A,B,C,D,E,F,G],[3*C+ -4*G>= -4,1*C+ -2*G>= -3,-1*G>= -3,1*G>=1,1*E+ -1*G>=0],6,2)
sabu_memo_table_1(case_3,[A,B,C,D,E,F,G,H],[3*C+ -4*H>= -5,7*C+ -4*H>=3,-1*H>= -4,1*H>=1,1*C+ -2*H>= -4,1*F+ -1*H>= -1],7,3)
sabu_memo_table_1(case_2,[A,B,C,D,E,F,G],[1*E+ -1*G>=0,1*G>=1],8,0)
sabu_memo_table_1(newline,[A,B,C,D,E,F,G],[1*C>=0,1*G>=1,1*E+ -1*G>=0],9,3)
sabu_memo_table_1(case_3,[A,B,C,D,E,F,G,H],[1*F+ -1*H>= -1,1*H>=1],10,0)
sabu_memo_table_1(case_6,[A,B,C,D,E,F,G,H,I],[1*E>=0,1*C>=0,1*B>=0,1*H=0,1*I=1,1*B=0,1*C=1],0,0)
sabu_memo_table_1(case_6,[A,B,C,D,E,F,G,H,I],[1*E+ -1*H>=0,1*C+ -1*I>= -1,2*C+1*H+ -2*I>=0,1*C>=1,1*B+1*C+ -1*I>=0,-1*C+1*I>=0],0,1)
sabu_memo_table_1(case_6,[A,B,C,D,E,F,G,H,I],[1*C+1*E+ -1*I>=0,1*C+1*H+ -1*I>=0,-1*C+1*I>=0,1*B+1*C+1*E+ -1*H+ -1*I>=0,1*B+1*C+ -1*I>=0,1*C>=1,1*C+ -1*I>= -1],0,2)
sabu_memo_table_1(case_6,[A,B,C,D,E,F,G,H,I],[1*B>=0,1*B+1*E+ -1*H>=0,-1*C+1*I>=0,1*C+1*H+ -1*I>=0,1*C>=1,1*C+ -1*I>= -1,1*C+1*E+ -1*I>=0],0,3)
sabu_memo_table_1(case_5,[A,B,C,D,E,F,G],[1*F>=1,1*B=1,1*G=2,1*D+ -1*F=0],0,0)
sabu_memo_table_1(lcstable,[A,B,C,D,E,F,G],[1*D>=0,1*B>=0,1*D+ -1*F=0,1*G=2,1*B=1,1*F>=1],0,0)
sabu_memo_table_1(case_5,[A,B,C,D,E,F,G],[1*B+2*D+ -1*F>=2,1*G>=2,1*B+1*F+ -1*G>=0,1*D>=1,1*B+ -1*G>= -1,-1*B>= -2],1,1)
sabu_memo_table_1(lcstable,[A,B,C,D,E,F,G],[1*B+2*D+ -1*F>=2,1*G>=2,1*B+1*F+ -1*G>=0,1*D>=1,1*B+ -1*G>= -1,-1*B>= -2],2,1)
sabu_memo_table_1(case_5,[A,B,C,D,E,F,G],[1*F>=0,1*G>=2,1*B+1*F+ -1*G>=0,1*B+ -1*G>= -1,1*B+3*D+ -1*F>=3,-1*B>= -3,1*D>=1],3,2)
sabu_memo_table_1(lcstable,[A,B,C,D,E,F,G],[1*F>=0,1*G>=2,1*B+1*F+ -1*G>=0,1*B+ -1*G>= -1,1*B+3*D+ -1*F>=3,-1*B>= -3,1*D>=1],4,2)
sabu_memo_table_1(case_5,[A,B,C,D,E,F,G],[1*G>=2,1*B+1*F+ -1*G>=0,1*F>=0,1*B+ -1*G>= -1,1*B+4*D+ -1*F>=4,-1*B>= -4,1*D>=1],5,3)
sabu_memo_table_1(lcstable,[A,B,C,D,E,F,G],[1*G>=2,1*B+1*F+ -1*G>=0,1*F>=0,1*B+ -1*G>= -1,1*B+4*D+ -1*F>=4,-1*B>= -4,1*D>=1],6,3)
sabu_memo_table_1(case_5,[A,B,C,D,E,F,G],[1*D>=1,1*B+ -1*G>= -1,1*F>=0,1*B+1*F+ -1*G>=0,1*G>=2],7,0)
sabu_memo_table_1(lcstable,[A,B,C,D,E,F,G],[1*F>=0,1*D>=1,1*B+ -1*G>= -1,1*B+1*F+ -1*G>=0,1*G>=2],8,0)
sabu_memo_table_1(case_8,[A,B],[1*B>=0,1*B>=0,1*B=1,1*A+ -1*B=0],0,0)
sabu_memo_table_1(case_8,[A,B],[1*B>=1,1*A+ -1*B=0],0,1)
sabu_memo_table_1(case_7,[A,B,C],[1*C>=0,1*B>=0,1*A>=0,1*A=0,1*B=1],0,0)
sabu_memo_table_1(case_7,[A,B,C],[1*C>=0,1*A>=0,1*B>=1],0,1)
sabu_memo_table_1(lcs,[A,B,C,D],[1*B>=1,1*D>=1],0,0)
sabu_memo_table_1(start,[A,B,C,D],[1*D>=0,1*B>=0,1*D>=1,1*B>=1],0,0)
sabu_memo_table_1(start,[],[],0,0)
:- dynamic sabu_memo_table_1/5.

sabu_memo_table_1(case_0, [A, _, B], [1*A+ -1*B=0, 1*A>=1], 7, 0).
sabu_memo_table_1(firstline, [A, _, B], [1*A+ -1*B=0, 1*A>=1], 8, 0).
sabu_memo_table_1(case_1, [_, A, _], [1*A>=1], 0, 1).
sabu_memo_table_1(case_9, [C, A, B], [-1*A+1*B>=0, -1*C+1*B>=0], 0, 1).
sabu_memo_table_1(max, [A, C, B], [-1*A+1*B>=0, -1*C+1*B>=0], 0, 0).
sabu_memo_table_1(case_4, [_, _, _, _, _, _], [], 0, 2).
sabu_memo_table_1(head_or_zero, [_, A, _], [1*A>=0, 1*A>=1], 0, 0).
sabu_memo_table_1(case_2, [_, _, _, _, A, _, B], [1*A+ -1*B>=0, 1*B>=1], 8, 0).
sabu_memo_table_1(newline, [_, _, A, _, C, _, B], [1*A>=0, 1*B>=1, 1*C+ -1*B>=0], 9, 3).
sabu_memo_table_1(case_3, [_, _, _, _, _, A, _, B], [1*A+ -1*B>= -1, 1*B>=1], 10, 0).
sabu_memo_table_1(case_6, [_, A, D, _, B, _, _, C, E], [1*A>=0, 1*A+1*B+ -1*C>=0, -1*D+1*E>=0, 1*D+1*C+ -1*E>=0, 1*D>=1, 1*D+ -1*E>= -1, 1*D+1*B+ -1*E>=0], 0, 3).
sabu_memo_table_1(case_5, [_, B, _, A, _, D, C], [1*A>=1, 1*B+ -1*C>= -1, 1*D>=0, 1*B+1*D+ -1*C>=0, 1*C>=2], 7, 0).
sabu_memo_table_1(lcstable, [_, C, _, B, _, A, D], [1*A>=0, 1*B>=1, 1*C+ -1*D>= -1, 1*C+1*A+ -1*D>=0, 1*D>=2], 8, 0).
sabu_memo_table_1(case_8, [B, A], [1*A>=1, 1*B+ -1*A=0], 0, 1).
sabu_memo_table_1(case_7, [B, C, A], [1*A>=0, 1*B>=0, 1*C>=1], 0, 1).
sabu_memo_table_1(lcs, [_, A, _, B], [1*A>=1, 1*B>=1], 0, 0).
sabu_memo_table_1(start, [_, B, _, A], [1*A>=0, 1*B>=0, 1*A>=1, 1*B>=1], 0, 0).
sabu_memo_table_1(start, [], [], 0, 0).


Size analysis performed in 28 ms.

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

Generated 51 equations 

Cost relation system solved by PUBS in 67 ms.

Method start terminates?: YES

 - l1_1: size of l1 wrt. Rat
 - l1_2: size of l1 wrt. List<Rat>
 - l2_1: size of l2 wrt. Rat
 - l2_2: size of l2 wrt. List<Rat>
UB for start(l1_1,l1_2,l2_1,l2_2) = nat(l2_2)*nat(l1_2)


Method start terminates?: YES

 - l1_1: size of l1 wrt. Rat
 - l1_2: size of l1 wrt. List<Rat>
 - l2_1: size of l2 wrt. Rat
 - l2_2: size of l2 wrt. List<Rat>
UB for start(l1_1,l1_2,l2_1,l2_2) = nat(l2_2)*nat(l1_2)


Method start terminates?: YES

UB for start(l1_1,l1_2,l2_1,l2_2) = nat(l2_2)*nat(l1_2)


Method start terminates?: YES

UB for start(l1_1,l1_2,l2_1,l2_2) = nat(l2_2)*nat(l1_2)


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

#### Computed strongly connected components 
0. non_recursive  : [case_8/2]
1. non_recursive  : [case_7/3]
2. non_recursive  : [maxNorm/2]
3. non_recursive  : [case_9/2]
4. non_recursive  : [max/2]
5. non_recursive  : [case_4/5]
6. non_recursive  : [case_1/2]
7. non_recursive  : [head_or_zero/2]
8. recursive [non_tail] : [case_2/5,case_3/6,newline/5]
9. non_recursive  : [case_6/6]
10. recursive  : [case_0/1,firstline/1]
11. recursive [non_tail] : [case_5/4,lcstable/4]
12. non_recursive  : [lcs/4]
14. non_recursive  : [start/4]
Warning: the following predicates are never called:[and_op/2,eq/2,geq/2,gt/2,leq/2,lt/2,neg/1,neq/2,or/2,start/0]

#### Obtained direct recursion through partial evaluation 
0. SCC is partially evaluated into case_8/2
1. SCC is partially evaluated into case_7/3
2. SCC is partially evaluated into maxNorm/2
3. SCC is partially evaluated into case_9/2
4. SCC is completely evaluated into other SCCs
5. SCC is partially evaluated into case_4/5
6. SCC is partially evaluated into case_1/2
7. SCC is completely evaluated into other SCCs
8. SCC is partially evaluated into newline/5
9. SCC is partially evaluated into case_6/6
10. SCC is partially evaluated into firstline/1
11. SCC is partially evaluated into lcstable/4
12. SCC is partially evaluated into lcs/4

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

### Specialization of cost equations case_8/2 
* CE 12 is refined into CE [23] 
* CE 13 is refined into CE [24] 


#### Refined cost equations case_8/2 
* CE 23: case_8(A,A) = 2
     [A>=2] 
* CE 24: case_8(A,C) = 2
     [C=1,A=1] 

### Cost equations --> "Loop" of case_8/2 
* CEs [23] --> Loop 23 
* CEs [24] --> Loop 24 

#### Loops of case_8/2 
* Loop 23: case_8(A,A) [A>=2] 
* Loop 24: case_8(A,C) [C=1,A=1] 

### Ranking functions of CR case_8(A,C) 

#### Partial ranking functions of CR case_8(A,C) 


### Resulting Chains:case_8(A,C) 
* [24]
* [23]


### Specialization of cost equations case_7/3 
* CE 4 is refined into CE [25,26] 
* CE 5 is discarded (unfeasible) 


#### Refined cost equations case_7/3 
* CE 25: case_7(A,B,C) = 3+ case_8(D,E):[24]
     [A>=1,E=1,D=1,C=1,B=2] 
* CE 26: case_7(A,B,C) = 3+ case_8(C,C):[23]
     [A>=C,C+1>=B,C>=2,B>=2] 

### Cost equations --> "Loop" of case_7/3 
* CEs [26] --> Loop 25 
* CEs [25] --> Loop 26 

#### Loops of case_7/3 
* Loop 25: case_7(A,B,C) [A>=C,C+1>=B,C>=2,B>=2] 
* Loop 26: case_7(A,B,C) [A>=1,C=1,B=2] 

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

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


### Resulting Chains:case_7(A,B,C) 
* [26]
* [25]


### Specialization of cost equations maxNorm/2 
* CE 9 is refined into CE [27] 
* CE 8 is refined into CE [28] 


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

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

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

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

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


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


### Specialization of cost equations case_9/2 
* CE 22 is refined into CE [29] 
* CE 21 is refined into CE [30] 


#### Refined cost equations case_9/2 
* CE 29: case_9(A,B) = 1
     [A>=B+1] 
* CE 30: case_9(A,B) = 1
     [B>=A] 

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

#### Loops of case_9/2 
* Loop 29: case_9(A,B) [A>=B+1] 
* Loop 30: case_9(A,B) [B>=A] 

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

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


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


### Specialization of cost equations case_4/5 
* CE 18 is refined into CE [31,32] 
* CE 19 is refined into CE [33,34] 
* CE 20 is refined into CE [35] 


#### Refined cost equations case_4/5 
* CE 31: case_4(A,B,C,D,E) = 3+ case_9(E,B):[30]
     [B>=E,C>=D+1] 
* CE 32: case_4(A,B,C,D,E) = 3+ case_9(E,B):[29]
     [E>=B+1,C>=D+1] 
* CE 33: case_4(A,B,C,D,E) = 3+ case_9(E,B):[30]
     [B>=E,D>=C+1] 
* CE 34: case_4(A,B,C,D,E) = 3+ case_9(E,B):[29]
     [E>=B+1,D>=C+1] 
* CE 35: case_4(A,B,C,C,D) = 3
     [] 

### Cost equations --> "Loop" of case_4/5 
* CEs [31] --> Loop 31 
* CEs [33] --> Loop 32 
* CEs [32] --> Loop 33 
* CEs [34] --> Loop 34 
* CEs [35] --> Loop 35 

#### Loops of case_4/5 
* Loop 31: case_4(A,B,C,D,E) [B>=E,C>=D+1] 
* Loop 32: case_4(A,B,C,D,E) [B>=E,D>=C+1] 
* Loop 33: case_4(A,B,C,D,E) [C>=D+1,E>=B+1] 
* Loop 34: case_4(A,B,C,D,E) [D>=C+1,E>=B+1] 
* Loop 35: case_4(A,B,C,C,D) [] 

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

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


### Resulting Chains:case_4(A,B,C,D,E) 
* [35]
* [34]
* [33]
* [32]
* [31]


### Specialization of cost equations case_1/2 
* CE 17 is refined into CE [36] 


#### Refined cost equations case_1/2 
* CE 36: case_1(A,B) = 2
     [B>=1] 

### Cost equations --> "Loop" of case_1/2 
* CEs [36] --> Loop 36 

#### Loops of case_1/2 
* Loop 36: case_1(A,B) [B>=1] 

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

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


### Resulting Chains:case_1(A,B) 
* [36]


### Specialization of cost equations newline/5 
* CE 14 is refined into CE [37] 
* CE 16 is refined into CE [38] 
* CE 15 is refined into CE [39,40,41,42,43] 


#### Refined cost equations newline/5 
* CE 37: newline(A,B,C,D,E) = 3
     [C>=0,E=1] 
* CE 38: newline(A,B,C,D,E) = 6
     [E>=1,C=1] 
* CE 39: newline(A,B,C,D,E) = 21+ newline(A,F,G,H,I)+ case_1(J,K):[36]+ case_1(F,G):[36]+ case_4(L,M,A,A,N):[35]
     [D>=H,B>=F,B>=N,D>=A,E>=K+1,G>=1,K>=1,E=I+1,G+1=C] 
* CE 40: newline(A,B,C,D,E) = 21+ newline(A,F,G,H,I)+ case_1(J,K):[36]+ case_1(F,G):[36]+ case_4(L,M,A,N,O):[34]
     [D>=H,B>=F,B>=O,D>=N,N>=A+1,O>=M+1,E>=K+1,G>=1,K>=1,E=I+1,G+1=C] 
* CE 41: newline(A,B,C,D,E) = 21+ newline(A,F,G,H,I)+ case_1(J,K):[36]+ case_1(F,G):[36]+ case_4(L,M,A,N,O):[33]
     [D>=H,B>=F,B>=O,A>=N+1,D>=N,O>=M+1,E>=K+1,G>=1,K>=1,E=I+1,G+1=C] 
* CE 42: newline(A,B,C,D,E) = 21+ newline(A,F,G,H,I)+ case_1(J,K):[36]+ case_1(F,G):[36]+ case_4(L,M,A,N,O):[32]
     [D>=H,B>=F,M>=O,B>=O,D>=N,N>=A+1,E>=K+1,G>=1,K>=1,E=I+1,G+1=C] 
* CE 43: newline(A,B,C,D,E) = 21+ newline(A,F,G,H,I)+ case_1(J,K):[36]+ case_1(F,G):[36]+ case_4(L,M,A,N,O):[31]
     [D>=H,B>=F,M>=O,B>=O,A>=N+1,D>=N,E>=K+1,G>=1,K>=1,E=I+1,G+1=C] 

### Cost equations --> "Loop" of newline/5 
* CEs [43] --> Loop 37 
* CEs [41] --> Loop 38 
* CEs [42] --> Loop 39 
* CEs [40] --> Loop 40 
* CEs [39] --> Loop 41 
* CEs [37] --> Loop 42 
* CEs [38] --> Loop 43 

#### Loops of newline/5 
* Loop 37: newline(A,B,C,D,E)->  newline(A,B',C',D',E')
                  [D>=D',B>=B',C'>=1,E>=2,E=E'+1,C'+1=C] 
* Loop 38: newline(A,B,C,D,E)->  newline(A,B',C',D',E')
                  [D>=D',B>=B',C'>=1,E>=2,E=E'+1,C'+1=C] 
* Loop 39: newline(A,B,C,D,E)->  newline(A,B',C',D',E')
                  [D>=D',B>=B',D>=A+1,C'>=1,E>=2,E=E'+1,C'+1=C] 
* Loop 40: newline(A,B,C,D,E)->  newline(A,B',C',D',E')
                  [D>=D',B>=B',D>=A+1,C'>=1,E>=2,E=E'+1,C'+1=C] 
* Loop 41: newline(A,B,C,D,E)->  newline(A,B',C',D',E')
                  [D>=D',B>=B',D>=A,C'>=1,E>=2,E=E'+1,C'+1=C] 
* Loop 42: newline(A,B,C,D,E) [C>=0,E=1] 
* Loop 43: newline(A,B,C,D,E) [E>=1,C=1] 

### Ranking functions of CR newline(A,B,C,D,E) 
* RF of phase [37,38,39,40,41]: [C-1,E-1]

#### Partial ranking functions of CR newline(A,B,C,D,E) 
* Partial RF of phase [37,38,39,40,41]:
  - RF of loop [37:1,38:1,39:1,40:1,41:1]:
    C-1
    E-1


### Resulting Chains:newline(A,B,C,D,E) 
* [[37,38,39,40,41],43]
* [[37,38,39,40,41],42]
* [43]
* [42]


### Specialization of cost equations case_6/6 
* CE 10 is refined into CE [44,45,46,47,48,49,50,51,52,53,54,55,56,57,58,59] 
* CE 11 is discarded (unfeasible) 


#### Refined cost equations case_6/6 
* CE 44: case_6(A,B,C,D,E,F) = 5+ newline(F,G,H,D,E):[[37,38,39,40,41],43]+ maxNorm(H,I):[28]+ maxNorm(J,K):[28]
     [K>=J,E>=J,B>=I,I>=H,E>=H,A>=G,J>=1,H>=2,C>=2] 
* CE 45: case_6(A,B,C,D,E,F) = 5+ newline(F,G,H,D,E):[[37,38,39,40,41],43]+ maxNorm(H,I):[28]+ maxNorm(J,K):[27]
     [J>=K+1,E>=J,B>=I,I>=H,E>=H,A>=G,K>=0,H>=2,C>=2] 
* CE 46: case_6(A,B,C,D,E,F) = 5+ newline(F,G,H,D,E):[[37,38,39,40,41],43]+ maxNorm(H,I):[27]+ maxNorm(J,K):[28]
     [K>=J,E>=J,H>=I+1,E>=H,B>=H,A>=G,J>=1,I>=0,H>=2,C>=2] 
* CE 47: case_6(A,B,C,D,E,F) = 5+ newline(F,G,H,D,E):[[37,38,39,40,41],43]+ maxNorm(H,I):[27]+ maxNorm(J,K):[27]
     [J>=K+1,E>=J,H>=I+1,E>=H,B>=H,A>=G,K>=0,I>=0,H>=2,C>=2] 
* CE 48: case_6(A,B,C,D,E,F) = 5+ newline(F,G,H,D,E):[[37,38,39,40,41],42]+ maxNorm(H,I):[28]+ maxNorm(J,K):[28]
     [K>=J,E>=J,B>=I,I>=H,H>=E,A>=G,J>=1,E>=2,C>=2] 
* CE 49: case_6(A,B,C,D,E,F) = 5+ newline(F,G,H,D,E):[[37,38,39,40,41],42]+ maxNorm(H,I):[28]+ maxNorm(J,K):[27]
     [J>=K+1,E>=J,B>=I,I>=H,H>=E,A>=G,K>=0,E>=2,C>=2] 
* CE 50: case_6(A,B,C,D,E,F) = 5+ newline(F,G,H,D,E):[[37,38,39,40,41],42]+ maxNorm(H,I):[27]+ maxNorm(J,K):[28]
     [K>=J,E>=J,H>=I+1,B>=H,H>=E,A>=G,J>=1,I>=0,E>=2,C>=2] 
* CE 51: case_6(A,B,C,D,E,F) = 5+ newline(F,G,H,D,E):[[37,38,39,40,41],42]+ maxNorm(H,I):[27]+ maxNorm(J,K):[27]
     [J>=K+1,E>=J,H>=I+1,B>=H,H>=E,A>=G,K>=0,I>=0,E>=2,C>=2] 
* CE 52: case_6(A,B,C,D,E,F) = 5+ newline(F,G,H,D,E):[43]+ maxNorm(I,J):[28]+ maxNorm(K,L):[28]
     [L>=K,E>=K,B>=J,A>=G,K>=1,J>=1,C>=2,I=1,H=1] 
* CE 53: case_6(A,B,C,D,E,F) = 5+ newline(F,G,H,D,E):[43]+ maxNorm(I,J):[28]+ maxNorm(K,L):[27]
     [K>=L+1,E>=K,B>=J,A>=G,L>=0,J>=1,C>=2,I=1,H=1] 
* CE 54: case_6(A,B,C,D,E,F) = 5+ newline(F,G,H,D,E):[43]+ maxNorm(I,J):[27]+ maxNorm(K,L):[28]
     [L>=K,E>=K,A>=G,K>=1,C>=2,B>=1,J=0,I=1,H=1] 
* CE 55: case_6(A,B,C,D,E,F) = 5+ newline(F,G,H,D,E):[43]+ maxNorm(I,J):[27]+ maxNorm(K,L):[27]
     [K>=L+1,E>=K,A>=G,L>=0,C>=2,B>=1,J=0,I=1,H=1] 
* CE 56: case_6(A,B,C,D,E,F) = 5+ newline(F,G,H,D,I):[42]+ maxNorm(H,J):[28]+ maxNorm(K,L):[28]
     [B>=J,J>=H,A>=G,L>=1,H>=0,C>=2,K=1,I=1,E=1] 
* CE 57: case_6(A,B,C,D,E,F) = 5+ newline(F,G,H,D,I):[42]+ maxNorm(H,J):[28]+ maxNorm(K,L):[27]
     [B>=J,J>=H,A>=G,H>=0,C>=2,L=0,K=1,I=1,E=1] 
* CE 58: case_6(A,B,C,D,E,F) = 5+ newline(F,G,H,D,I):[42]+ maxNorm(H,J):[27]+ maxNorm(K,L):[28]
     [H>=J+1,B>=H,A>=G,L>=1,J>=0,C>=2,K=1,I=1,E=1] 
* CE 59: case_6(A,B,C,D,E,F) = 5+ newline(F,G,H,D,I):[42]+ maxNorm(H,J):[27]+ maxNorm(K,L):[27]
     [H>=J+1,B>=H,A>=G,J>=0,C>=2,L=0,K=1,I=1,E=1] 

### Cost equations --> "Loop" of case_6/6 
* CEs [51] --> Loop 44 
* CEs [50] --> Loop 45 
* CEs [49] --> Loop 46 
* CEs [48] --> Loop 47 
* CEs [47] --> Loop 48 
* CEs [46] --> Loop 49 
* CEs [45] --> Loop 50 
* CEs [44] --> Loop 51 
* CEs [55] --> Loop 52 
* CEs [54] --> Loop 53 
* CEs [53] --> Loop 54 
* CEs [52] --> Loop 55 
* CEs [59] --> Loop 56 
* CEs [58] --> Loop 57 
* CEs [57] --> Loop 58 
* CEs [56] --> Loop 59 

#### Loops of case_6/6 
* Loop 44: case_6(A,B,C,D,E,F) [B>=E,E>=2,C>=2] 
* Loop 45: case_6(A,B,C,D,E,F) [B>=E,E>=2,C>=2] 
* Loop 46: case_6(A,B,C,D,E,F) [B>=E,E>=2,C>=2] 
* Loop 47: case_6(A,B,C,D,E,F) [B>=E,E>=2,C>=2] 
* Loop 48: case_6(A,B,C,D,E,F) [E>=2,C>=2,B>=2] 
* Loop 49: case_6(A,B,C,D,E,F) [E>=2,C>=2,B>=2] 
* Loop 50: case_6(A,B,C,D,E,F) [E>=2,C>=2,B>=2] 
* Loop 51: case_6(A,B,C,D,E,F) [E>=2,C>=2,B>=2] 
* Loop 52: case_6(A,B,C,D,E,F) [E>=1,C>=2,B>=1] 
* Loop 53: case_6(A,B,C,D,E,F) [E>=1,C>=2,B>=1] 
* Loop 54: case_6(A,B,C,D,E,F) [E>=1,C>=2,B>=1] 
* Loop 55: case_6(A,B,C,D,E,F) [E>=1,C>=2,B>=1] 
* Loop 56: case_6(A,B,C,D,E,F) [C>=2,B>=1,E=1] 
* Loop 57: case_6(A,B,C,D,E,F) [C>=2,B>=1,E=1] 
* Loop 58: case_6(A,B,C,D,E,F) [C>=2,B>=0,E=1] 
* Loop 59: case_6(A,B,C,D,E,F) [C>=2,B>=0,E=1] 

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

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


### Resulting Chains:case_6(A,B,C,D,E,F) 
* [59]
* [58]
* [57]
* [56]
* [55]
* [54]
* [53]
* [52]
* [51]
* [50]
* [49]
* [48]
* [47]
* [46]
* [45]
* [44]


### Specialization of cost equations firstline/1 
* CE 7 is refined into CE [60] 
* CE 6 is refined into CE [61] 


#### Refined cost equations firstline/1 
* CE 60: firstline(A) = 6+ firstline(B)
     [B>=0,B+1=A] 
* CE 61: firstline(A) = 3
     [A=1] 

### Cost equations --> "Loop" of firstline/1 
* CEs [61] --> Loop 60 
* CEs [60] --> Loop 61 

#### Loops of firstline/1 
* Loop 60: firstline(A) [A=1] 
* Loop 61: firstline(A)->  firstline(A')
                  [A'>=0,A'+1=A] 

### Ranking functions of CR firstline(A) 
* RF of phase [61]: [A]

#### Partial ranking functions of CR firstline(A) 
* Partial RF of phase [61]:
  - RF of loop [61:1]:
    A


### Resulting Chains:firstline(A) 
* [[61],60]
* [60]


### Specialization of cost equations lcstable/4 
* CE 3 is refined into CE [62,63,64,65,66,67,68,69,70,71,72,73,74,75,76,77] 
* CE 2 is refined into CE [78,79] 


#### Refined cost equations lcstable/4 
* CE 62: lcstable(A,B,C,D) = 7+ lcstable(E,F,C,G)+ case_6(H,I,J,C,K,L):[59]
     [I+F>=J,A>=E,A>=L,F+1>=J,J>=2,I>=0,F+1=B,G=1,K=1,D=1] 
* CE 63: lcstable(A,B,C,D) = 7+ lcstable(E,F,C,G)+ case_6(H,I,J,C,K,L):[58]
     [I+F>=J,A>=E,A>=L,F+1>=J,J>=2,I>=0,F+1=B,G=1,K=1,D=1] 
* CE 64: lcstable(A,B,C,D) = 7+ lcstable(E,F,C,G)+ case_6(H,I,J,C,K,L):[57]
     [A>=E,A>=L,F+1>=J,J>=2,I>=1,F+1=B,G=1,K=1,D=1] 
* CE 65: lcstable(A,B,C,D) = 7+ lcstable(E,F,C,G)+ case_6(H,I,J,C,K,L):[56]
     [A>=E,A>=L,F+1>=J,J>=2,I>=1,F+1=B,G=1,K=1,D=1] 
* CE 66: lcstable(A,B,C,D) = 7+ lcstable(E,F,C,D)+ case_6(G,H,I,C,D,J):[55]
     [A>=E,A>=J,F+1>=I,D>=1,I>=2,H>=1,F+1=B] 
* CE 67: lcstable(A,B,C,D) = 7+ lcstable(E,F,C,D)+ case_6(G,H,I,C,D,J):[54]
     [A>=E,A>=J,F+1>=I,D>=1,I>=2,H>=1,F+1=B] 
* CE 68: lcstable(A,B,C,D) = 7+ lcstable(E,F,C,D)+ case_6(G,H,I,C,D,J):[53]
     [A>=E,A>=J,F+1>=I,D>=1,I>=2,H>=1,F+1=B] 
* CE 69: lcstable(A,B,C,D) = 7+ lcstable(E,F,C,D)+ case_6(G,H,I,C,D,J):[52]
     [A>=E,A>=J,F+1>=I,D>=1,I>=2,H>=1,F+1=B] 
* CE 70: lcstable(A,B,C,D) = 7+ lcstable(E,F,C,D)+ case_6(G,H,I,C,D,J):[51]
     [A>=E,A>=J,F+1>=I,D>=2,I>=2,H>=2,F+1=B] 
* CE 71: lcstable(A,B,C,D) = 7+ lcstable(E,F,C,D)+ case_6(G,H,I,C,D,J):[50]
     [A>=E,A>=J,F+1>=I,D>=2,I>=2,H>=2,F+1=B] 
* CE 72: lcstable(A,B,C,D) = 7+ lcstable(E,F,C,D)+ case_6(G,H,I,C,D,J):[49]
     [A>=E,A>=J,F+1>=I,D>=2,I>=2,H>=2,F+1=B] 
* CE 73: lcstable(A,B,C,D) = 7+ lcstable(E,F,C,D)+ case_6(G,H,I,C,D,J):[48]
     [A>=E,A>=J,F+1>=I,D>=2,I>=2,H>=2,F+1=B] 
* CE 74: lcstable(A,B,C,D) = 7+ lcstable(E,F,C,D)+ case_6(G,H,I,C,D,J):[47]
     [A>=E,A>=J,H>=D,F+1>=I,D>=2,I>=2,F+1=B] 
* CE 75: lcstable(A,B,C,D) = 7+ lcstable(E,F,C,D)+ case_6(G,H,I,C,D,J):[46]
     [A>=E,A>=J,H>=D,F+1>=I,D>=2,I>=2,F+1=B] 
* CE 76: lcstable(A,B,C,D) = 7+ lcstable(E,F,C,D)+ case_6(G,H,I,C,D,J):[45]
     [A>=E,A>=J,H>=D,F+1>=I,D>=2,I>=2,F+1=B] 
* CE 77: lcstable(A,B,C,D) = 7+ lcstable(E,F,C,D)+ case_6(G,H,I,C,D,J):[44]
     [A>=E,A>=J,H>=D,F+1>=I,D>=2,I>=2,F+1=B] 
* CE 78: lcstable(A,B,C,D) = 5+ firstline(D):[[61],60]+ maxNorm(D,E):[27]
     [D>=2,E=0,B=1] 
* CE 79: lcstable(A,B,C,D) = 5+ firstline(E):[60]+ maxNorm(F,G):[27]
     [G=0,F=1,E=1,D=1,B=1] 

### Cost equations --> "Loop" of lcstable/4 
* CEs [78] --> Loop 62 
* CEs [79] --> Loop 63 
* CEs [77] --> Loop 64 
* CEs [76] --> Loop 65 
* CEs [75] --> Loop 66 
* CEs [74] --> Loop 67 
* CEs [73] --> Loop 68 
* CEs [72] --> Loop 69 
* CEs [71] --> Loop 70 
* CEs [70] --> Loop 71 
* CEs [69] --> Loop 72 
* CEs [68] --> Loop 73 
* CEs [67] --> Loop 74 
* CEs [66] --> Loop 75 
* CEs [65] --> Loop 76 
* CEs [64] --> Loop 77 
* CEs [63] --> Loop 78 
* CEs [62] --> Loop 79 

#### Loops of lcstable/4 
* Loop 62: lcstable(A,B,C,D) [D>=2,B=1] 
* Loop 63: lcstable(A,B,C,D) [D=1,B=1] 
* Loop 64: lcstable(A,B,C,D)->  lcstable(A',B',C,D)
                  [A>=A',D>=2,B>=2,B=B'+1] 
* Loop 65: lcstable(A,B,C,D)->  lcstable(A',B',C,D)
                  [A>=A',D>=2,B>=2,B=B'+1] 
* Loop 66: lcstable(A,B,C,D)->  lcstable(A',B',C,D)
                  [A>=A',D>=2,B>=2,B=B'+1] 
* Loop 67: lcstable(A,B,C,D)->  lcstable(A',B',C,D)
                  [A>=A',D>=2,B>=2,B=B'+1] 
* Loop 68: lcstable(A,B,C,D)->  lcstable(A',B',C,D)
                  [A>=A',D>=2,B>=2,B=B'+1] 
* Loop 69: lcstable(A,B,C,D)->  lcstable(A',B',C,D)
                  [A>=A',D>=2,B>=2,B=B'+1] 
* Loop 70: lcstable(A,B,C,D)->  lcstable(A',B',C,D)
                  [A>=A',D>=2,B>=2,B=B'+1] 
* Loop 71: lcstable(A,B,C,D)->  lcstable(A',B',C,D)
                  [A>=A',D>=2,B>=2,B=B'+1] 
* Loop 72: lcstable(A,B,C,D)->  lcstable(A',B',C,D)
                  [A>=A',D>=1,B>=2,B=B'+1] 
* Loop 73: lcstable(A,B,C,D)->  lcstable(A',B',C,D)
                  [A>=A',D>=1,B>=2,B=B'+1] 
* Loop 74: lcstable(A,B,C,D)->  lcstable(A',B',C,D)
                  [A>=A',D>=1,B>=2,B=B'+1] 
* Loop 75: lcstable(A,B,C,D)->  lcstable(A',B',C,D)
                  [A>=A',D>=1,B>=2,B=B'+1] 
* Loop 76: lcstable(A,B,C,D)->  lcstable(A',B',C,D')
                  [A>=A',B>=2,B=B'+1,D'=1,D=1] 
* Loop 77: lcstable(A,B,C,D)->  lcstable(A',B',C,D')
                  [A>=A',B>=2,B=B'+1,D'=1,D=1] 
* Loop 78: lcstable(A,B,C,D)->  lcstable(A',B',C,D')
                  [A>=A',B>=2,B=B'+1,D'=1,D=1] 
* Loop 79: lcstable(A,B,C,D)->  lcstable(A',B',C,D')
                  [A>=A',B>=2,B=B'+1,D'=1,D=1] 

### Ranking functions of CR lcstable(A,B,C,D) 
* RF of phase [64,65,66,67,68,69,70,71,72,73,74,75,76,77,78,79]: [B-1]

#### Partial ranking functions of CR lcstable(A,B,C,D) 
* Partial RF of phase [64,65,66,67,68,69,70,71,72,73,74,75,76,77,78,79]:
  - RF of loop [64:1,65:1,66:1,67:1,68:1,69:1,70:1,71:1,72:1,73:1,74:1,75:1,76:1,77:1,78:1,79:1]:
    B-1


### Resulting Chains:lcstable(A,B,C,D) 
* [[64,65,66,67,68,69,70,71,72,73,74,75,76,77,78,79],63]
* [[64,65,66,67,68,69,70,71,72,73,74,75,76,77,78,79],62]
* [63]
* [62]


### Specialization of cost equations lcs/4 
* CE 1 is refined into CE [80,81,82,83] 


#### Refined cost equations lcs/4 
* CE 80: lcs(A,B,C,D) = 4+ lcstable(A,B,C,E):[[64,65,66,67,68,69,70,71,72,73,74,75,76,77,78,79],63]+ case_7(F,G,B):[25]
     [F>=B,B+1>=G,B>=2,G>=2,E=1,D=1] 
* CE 81: lcs(A,B,C,D) = 4+ lcstable(A,B,C,D):[[64,65,66,67,68,69,70,71,72,73,74,75,76,77,78,79],62]+ case_7(E,F,B):[25]
     [E>=B,B+1>=F,B>=2,F>=2,D>=2] 
* CE 82: lcs(A,B,C,D) = 4+ lcstable(A,E,C,F):[63]+ case_7(G,H,I):[26]
     [G>=1,I=1,H=2,F=1,E=1,D=1,B=1] 
* CE 83: lcs(A,B,C,D) = 4+ lcstable(A,E,C,D):[62]+ case_7(F,G,H):[26]
     [F>=1,D>=2,H=1,G=2,E=1,B=1] 

### Cost equations --> "Loop" of lcs/4 
* CEs [81] --> Loop 80 
* CEs [80] --> Loop 81 
* CEs [83] --> Loop 82 
* CEs [82] --> Loop 83 

#### Loops of lcs/4 
* Loop 80: lcs(A,B,C,D) [D>=2,B>=2] 
* Loop 81: lcs(A,B,C,D) [B>=2,D=1] 
* Loop 82: lcs(A,B,C,D) [D>=2,B=1] 
* Loop 83: lcs(A,B,C,D) [D=1,B=1] 

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

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


### Resulting Chains:lcs(A,B,C,D) 
* [83]
* [82]
* [81]
* [80]


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

#### Cost of chains of case_8(A,C):
* Chain [24]: 2
  with precondition: [A=1,C=1] 

* Chain [23]: 2
  with precondition: [C=A,C>=2] 


#### Cost of chains of case_7(A,B,C):
* Chain [26]: 5
  with precondition: [B=2,C=1,A>=1] 

* Chain [25]: 5
  with precondition: [B>=2,C>=2,C+1>=B,A>=C] 


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

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


#### Cost of chains of case_9(A,B):
* Chain [30]: 1
  with precondition: [B>=A] 

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


#### Cost of chains of case_4(A,B,C,D,E):
* Chain [35]: 3
  with precondition: [D=C] 

* Chain [34]: 4
  with precondition: [E>=B+1,D>=C+1] 

* Chain [33]: 4
  with precondition: [E>=B+1,C>=D+1] 

* Chain [32]: 4
  with precondition: [D>=C+1,B>=E] 

* Chain [31]: 4
  with precondition: [C>=D+1,B>=E] 


#### Cost of chains of case_1(A,B):
* Chain [36]: 2
  with precondition: [B>=1] 


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

 * loop 37:newline(A,B,C,D,E) -> [newline(A',B',C',D',E')] 
29
 * loop 38:newline(A,B,C,D,E) -> [newline(A',B',C',D',E')] 
29
 * loop 39:newline(A,B,C,D,E) -> [newline(A',B',C',D',E')] 
29
 * loop 40:newline(A,B,C,D,E) -> [newline(A',B',C',D',E')] 
29
 * loop 41:newline(A,B,C,D,E) -> [newline(A',B',C',D',E')] 
28
#### Cost of phase [37,38,39,40,41]:newline(A,B,C,D,E) -> [newline(A',B',C',D',E')] 
29*it(37)+29*it(38)+29*it(39)+29*it(40)+28*it(41)+0
  Such that:it(37)+it(38)+it(39)+it(40)+it(41) =< C-1
it(37)+it(38)+it(39)+it(40)+it(41) =< C-C'
it(37)+it(38)+it(39)+it(40)+it(41) =< E-1
it(37)+it(38)+it(39)+it(40)+it(41) =< E-E'
it(37)+it(38)+it(39)+it(40)+it(41) >= C-C'
it(37)+it(38)+it(39)+it(40)+it(41) >= E-E'

#### Cost of phase [37,38,39,40,41]:newline(A,B,C,D,E) -> [newline(A',B',C',D',E')] 
29*it(37)+29*it(38)+29*it(39)+29*it(40)+28*it(41)+0
  Such that:it(37)+it(38)+it(39)+it(40)+it(41) =< C-1
it(37)+it(38)+it(39)+it(40)+it(41) =< C-C'
it(37)+it(38)+it(39)+it(40)+it(41) =< E-1
it(37)+it(38)+it(39)+it(40)+it(41) =< E-E'
it(37)+it(38)+it(39)+it(40)+it(41) >= C-C'
it(37)+it(38)+it(39)+it(40)+it(41) >= E-E'

#### Cost of chains of newline(A,B,C,D,E):
* Chain [[37,38,39,40,41],43]: 29*it(37)+29*it(38)+29*it(39)+29*it(40)+28*it(41)+6
  Such that:it(37)+it(38)+it(39)+it(40)+it(41) =< C-1
it(37)+it(38)+it(39)+it(40)+it(41) >= C-1

  with precondition: [C>=2,E>=C] 

* Chain [[37,38,39,40,41],42]: 29*it(37)+29*it(38)+29*it(39)+29*it(40)+28*it(41)+3
  Such that:it(37)+it(38)+it(39)+it(40)+it(41) =< E-1
it(37)+it(38)+it(39)+it(40)+it(41) >= E-1

  with precondition: [E>=2,C>=E] 

* Chain [43]: 6
  with precondition: [C=1,E>=1] 

* Chain [42]: 3
  with precondition: [E=1,C>=0] 


#### Cost of chains of case_6(A,B,C,D,E,F):
* Chain [59]: 8
  with precondition: [E=1,B>=0,C>=2] 

* Chain [58]: 8
  with precondition: [E=1,B>=0,C>=2] 

* Chain [57]: 8
  with precondition: [E=1,B>=1,C>=2] 

* Chain [56]: 8
  with precondition: [E=1,B>=1,C>=2] 

* Chain [55]: 11
  with precondition: [B>=1,C>=2,E>=1] 

* Chain [54]: 11
  with precondition: [B>=1,C>=2,E>=1] 

* Chain [53]: 11
  with precondition: [B>=1,C>=2,E>=1] 

* Chain [52]: 11
  with precondition: [B>=1,C>=2,E>=1] 

* Chain [51]: 29*s(1)+29*s(2)+29*s(3)+29*s(4)+28*s(5)+11
  Such that:s(1)+s(2)+s(3)+s(4)+s(5) =< E-1
s(1)+s(2)+s(3)+s(4)+s(5) >= 1

  with precondition: [B>=2,C>=2,E>=2] 

* Chain [50]: 29*s(6)+29*s(7)+29*s(8)+29*s(9)+28*s(10)+11
  Such that:s(6)+s(7)+s(8)+s(9)+s(10) =< E-1
s(6)+s(7)+s(8)+s(9)+s(10) >= 1

  with precondition: [B>=2,C>=2,E>=2] 

* Chain [49]: 29*s(11)+29*s(12)+29*s(13)+29*s(14)+28*s(15)+11
  Such that:s(11)+s(12)+s(13)+s(14)+s(15) =< E-1
s(11)+s(12)+s(13)+s(14)+s(15) >= 1

  with precondition: [B>=2,C>=2,E>=2] 

* Chain [48]: 29*s(16)+29*s(17)+29*s(18)+29*s(19)+28*s(20)+11
  Such that:s(16)+s(17)+s(18)+s(19)+s(20) =< E-1
s(16)+s(17)+s(18)+s(19)+s(20) >= 1

  with precondition: [B>=2,C>=2,E>=2] 

* Chain [47]: 29*s(21)+29*s(22)+29*s(23)+29*s(24)+28*s(25)+8
  Such that:s(21)+s(22)+s(23)+s(24)+s(25) =< E-1
s(21)+s(22)+s(23)+s(24)+s(25) >= E-1

  with precondition: [C>=2,E>=2,B>=E] 

* Chain [46]: 29*s(26)+29*s(27)+29*s(28)+29*s(29)+28*s(30)+8
  Such that:s(26)+s(27)+s(28)+s(29)+s(30) =< E-1
s(26)+s(27)+s(28)+s(29)+s(30) >= E-1

  with precondition: [C>=2,E>=2,B>=E] 

* Chain [45]: 29*s(31)+29*s(32)+29*s(33)+29*s(34)+28*s(35)+8
  Such that:s(31)+s(32)+s(33)+s(34)+s(35) =< E-1
s(31)+s(32)+s(33)+s(34)+s(35) >= E-1

  with precondition: [C>=2,E>=2,B>=E] 

* Chain [44]: 29*s(36)+29*s(37)+29*s(38)+29*s(39)+28*s(40)+8
  Such that:s(36)+s(37)+s(38)+s(39)+s(40) =< E-1
s(36)+s(37)+s(38)+s(39)+s(40) >= E-1

  with precondition: [C>=2,E>=2,B>=E] 


#### Cost of loops [61] 

 * loop 61:firstline(A) -> [firstline(A')] 
6
#### Cost of phase [61]:firstline(A) -> [firstline(A')] 
6*it(61)+0
  Such that:it(61) =< A
it(61) =< A-A'
it(61) >= A-A'

#### Cost of chains of firstline(A):
* Chain [[61],60]: 6*it(61)+3
  Such that:it(61) =< A-1
it(61) >= A-1

  with precondition: [A>=2] 

* Chain [60]: 3
  with precondition: [A=1] 


#### Cost of loops [64,65,66,67,68,69,70,71,72,73,74,75,76,77,78,79] 

 * loop 64:lcstable(A,B,C,D) -> [lcstable(A',B',C',D')] 
29*s(46)+29*s(47)+29*s(48)+29*s(49)+28*s(50)+15
  Such that:s(46)+s(47)+s(48)+s(49)+s(50) =< D-1
s(46)+s(47)+s(48)+s(49)+s(50) >= D-1

 * loop 65:lcstable(A,B,C,D) -> [lcstable(A',B',C',D')] 
29*s(56)+29*s(57)+29*s(58)+29*s(59)+28*s(60)+15
  Such that:s(56)+s(57)+s(58)+s(59)+s(60) =< D-1
s(56)+s(57)+s(58)+s(59)+s(60) >= D-1

 * loop 66:lcstable(A,B,C,D) -> [lcstable(A',B',C',D')] 
29*s(66)+29*s(67)+29*s(68)+29*s(69)+28*s(70)+15
  Such that:s(66)+s(67)+s(68)+s(69)+s(70) =< D-1
s(66)+s(67)+s(68)+s(69)+s(70) >= D-1

 * loop 67:lcstable(A,B,C,D) -> [lcstable(A',B',C',D')] 
29*s(76)+29*s(77)+29*s(78)+29*s(79)+28*s(80)+15
  Such that:s(76)+s(77)+s(78)+s(79)+s(80) =< D-1
s(76)+s(77)+s(78)+s(79)+s(80) >= D-1

 * loop 68:lcstable(A,B,C,D) -> [lcstable(A',B',C',D')] 
29*s(86)+29*s(87)+29*s(88)+29*s(89)+28*s(90)+18
  Such that:s(86)+s(87)+s(88)+s(89)+s(90) =< D-1
s(86)+s(87)+s(88)+s(89)+s(90) >= 1

 * loop 69:lcstable(A,B,C,D) -> [lcstable(A',B',C',D')] 
29*s(96)+29*s(97)+29*s(98)+29*s(99)+28*s(100)+18
  Such that:s(96)+s(97)+s(98)+s(99)+s(100) =< D-1
s(96)+s(97)+s(98)+s(99)+s(100) >= 1

 * loop 70:lcstable(A,B,C,D) -> [lcstable(A',B',C',D')] 
29*s(106)+29*s(107)+29*s(108)+29*s(109)+28*s(110)+18
  Such that:s(106)+s(107)+s(108)+s(109)+s(110) =< D-1
s(106)+s(107)+s(108)+s(109)+s(110) >= 1

 * loop 71:lcstable(A,B,C,D) -> [lcstable(A',B',C',D')] 
29*s(116)+29*s(117)+29*s(118)+29*s(119)+28*s(120)+18
  Such that:s(116)+s(117)+s(118)+s(119)+s(120) =< D-1
s(116)+s(117)+s(118)+s(119)+s(120) >= 1

 * loop 72:lcstable(A,B,C,D) -> [lcstable(A',B',C',D')] 
18
 * loop 73:lcstable(A,B,C,D) -> [lcstable(A',B',C',D')] 
18
 * loop 74:lcstable(A,B,C,D) -> [lcstable(A',B',C',D')] 
18
 * loop 75:lcstable(A,B,C,D) -> [lcstable(A',B',C',D')] 
18
 * loop 76:lcstable(A,B,C,D) -> [lcstable(A',B',C',D')] 
15
 * loop 77:lcstable(A,B,C,D) -> [lcstable(A',B',C',D')] 
15
 * loop 78:lcstable(A,B,C,D) -> [lcstable(A',B',C',D')] 
15
 * loop 79:lcstable(A,B,C,D) -> [lcstable(A',B',C',D')] 
15
#### Cost of phase [64,65,66,67,68,69,70,71,72,73,74,75,76,77,78,79]:lcstable(A,B,C,D) -> [lcstable(A',B',C',D')] 
15*it(64)+15*it(65)+15*it(66)+15*it(67)+18*it(68)+18*it(69)+18*it(70)+18*it(71)+18*it(72)+18*it(73)+18*it(74)+18*it(75)+15*it(76)+15*it(77)+15*it(78)+15*it(79)+29*s(121)+29*s(122)+29*s(123)+29*s(124)+28*s(125)+29*s(126)+29*s(127)+29*s(128)+29*s(129)+28*s(130)+29*s(131)+29*s(132)+29*s(133)+29*s(134)+28*s(135)+29*s(136)+29*s(137)+29*s(138)+29*s(139)+28*s(140)+29*s(141)+29*s(142)+29*s(143)+29*s(144)+28*s(145)+29*s(146)+29*s(147)+29*s(148)+29*s(149)+28*s(150)+29*s(151)+29*s(152)+29*s(153)+29*s(154)+28*s(155)+29*s(156)+29*s(157)+29*s(158)+29*s(159)+28*s(160)+0
  Such that:it(64)+it(65)+it(66)+it(67)+it(68)+it(69)+it(70)+it(71)+it(72)+it(73)+it(74)+it(75)+it(76)+it(77)+it(78)+it(79) =< B-1
it(64)+it(65)+it(66)+it(67)+it(68)+it(69)+it(70)+it(71)+it(72)+it(73)+it(74)+it(75)+it(76)+it(77)+it(78)+it(79) =< B-B'
aux(2) =< D-1
aux(4) =< aux(2)
s(121)+s(122)+s(123)+s(124)+s(125) =< it(64)*aux(2)
s(156)+s(157)+s(158)+s(159)+s(160) =< it(71)*aux(4)
s(151)+s(152)+s(153)+s(154)+s(155) =< it(70)*aux(4)
s(146)+s(147)+s(148)+s(149)+s(150) =< it(69)*aux(4)
s(141)+s(142)+s(143)+s(144)+s(145) =< it(68)*aux(4)
s(136)+s(137)+s(138)+s(139)+s(140) =< it(67)*aux(4)
s(131)+s(132)+s(133)+s(134)+s(135) =< it(66)*aux(4)
s(126)+s(127)+s(128)+s(129)+s(130) =< it(65)*aux(4)
aux(1) >= D-1
aux(17) >= B-B'
aux(9)+it(64)+it(65)+it(66)+it(67)+it(69)+it(70)+it(71)+it(72)+it(73)+it(74)+it(75)+it(76)+it(77)+it(78)+it(79) >= aux(17)
aux(11)+it(64)+it(65)+it(66)+it(67)+it(68)+it(70)+it(71)+it(72)+it(73)+it(74)+it(75)+it(76)+it(77)+it(78)+it(79) >= aux(17)
aux(13)+it(64)+it(65)+it(66)+it(67)+it(68)+it(69)+it(71)+it(72)+it(73)+it(74)+it(75)+it(76)+it(77)+it(78)+it(79) >= aux(17)
aux(15)+it(64)+it(65)+it(66)+it(67)+it(68)+it(69)+it(70)+it(72)+it(73)+it(74)+it(75)+it(76)+it(77)+it(78)+it(79) >= aux(17)
it(64)+it(65)+it(66)+it(67)+it(68)+it(69)+it(70)+it(71)+it(72)+it(73)+it(74)+it(75)+it(76)+it(77)+it(78)+it(79) >= aux(17)
it(65)+it(66)+it(67)+it(68)+it(69)+it(70)+it(71)+it(72)+it(73)+it(74)+it(75)+it(76)+it(77)+it(78)+it(79)+s(121)+s(122)+s(123)+s(124)+s(125) >= aux(17)
it(65)+it(66)+it(68)+it(69)+it(70)+it(71)+it(72)+it(73)+it(74)+it(75)+it(76)+it(77)+it(78)+it(79)+s(121)+s(122)+s(123)+s(124)+s(125)+s(136)+s(137)+s(138)+s(139)+s(140) >= aux(17)
it(65)+it(67)+it(68)+it(69)+it(70)+it(71)+it(72)+it(73)+it(74)+it(75)+it(76)+it(77)+it(78)+it(79)+s(121)+s(122)+s(123)+s(124)+s(125)+s(131)+s(132)+s(133)+s(134)+s(135) >= aux(17)
it(66)+it(67)+it(68)+it(69)+it(70)+it(71)+it(72)+it(73)+it(74)+it(75)+it(76)+it(77)+it(78)+it(79)+s(121)+s(122)+s(123)+s(124)+s(125)+s(126)+s(127)+s(128)+s(129)+s(130) >= aux(17)
aux(3) >= aux(1)
s(156)+s(157)+s(158)+s(159)+s(160) >= aux(15)
s(151)+s(152)+s(153)+s(154)+s(155) >= aux(13)
s(146)+s(147)+s(148)+s(149)+s(150) >= aux(11)
s(141)+s(142)+s(143)+s(144)+s(145) >= aux(9)
s(121)+s(122)+s(123)+s(124)+s(125) >= it(64)*aux(1)
s(136)+s(137)+s(138)+s(139)+s(140) >= it(67)*aux(3)
s(131)+s(132)+s(133)+s(134)+s(135) >= it(66)*aux(3)
s(126)+s(127)+s(128)+s(129)+s(130) >= it(65)*aux(3)

#### Cost of phase [64,65,66,67,68,69,70,71,72,73,74,75,76,77,78,79]:lcstable(A,B,C,D) -> [lcstable(A',B',C',D')] 
15*it(64)+15*it(65)+15*it(66)+15*it(67)+18*it(68)+18*it(69)+18*it(70)+18*it(71)+18*it(72)+18*it(73)+18*it(74)+18*it(75)+15*it(76)+15*it(77)+15*it(78)+15*it(79)+29*s(121)+29*s(122)+29*s(123)+29*s(124)+28*s(125)+29*s(126)+29*s(127)+29*s(128)+29*s(129)+28*s(130)+29*s(131)+29*s(132)+29*s(133)+29*s(134)+28*s(135)+29*s(136)+29*s(137)+29*s(138)+29*s(139)+28*s(140)+29*s(141)+29*s(142)+29*s(143)+29*s(144)+28*s(145)+29*s(146)+29*s(147)+29*s(148)+29*s(149)+28*s(150)+29*s(151)+29*s(152)+29*s(153)+29*s(154)+28*s(155)+29*s(156)+29*s(157)+29*s(158)+29*s(159)+28*s(160)+0
  Such that:it(64)+it(65)+it(66)+it(67)+it(68)+it(69)+it(70)+it(71)+it(72)+it(73)+it(74)+it(75)+it(76)+it(77)+it(78)+it(79) =< B-1
it(64)+it(65)+it(66)+it(67)+it(68)+it(69)+it(70)+it(71)+it(72)+it(73)+it(74)+it(75)+it(76)+it(77)+it(78)+it(79) =< B-B'
aux(2) =< D-1
aux(4) =< aux(2)
s(121)+s(122)+s(123)+s(124)+s(125) =< it(64)*aux(2)
s(156)+s(157)+s(158)+s(159)+s(160) =< it(71)*aux(4)
s(151)+s(152)+s(153)+s(154)+s(155) =< it(70)*aux(4)
s(146)+s(147)+s(148)+s(149)+s(150) =< it(69)*aux(4)
s(141)+s(142)+s(143)+s(144)+s(145) =< it(68)*aux(4)
s(136)+s(137)+s(138)+s(139)+s(140) =< it(67)*aux(4)
s(131)+s(132)+s(133)+s(134)+s(135) =< it(66)*aux(4)
s(126)+s(127)+s(128)+s(129)+s(130) =< it(65)*aux(4)
aux(1) >= D-1
aux(17) >= B-B'
aux(9)+it(64)+it(65)+it(66)+it(67)+it(69)+it(70)+it(71)+it(72)+it(73)+it(74)+it(75)+it(76)+it(77)+it(78)+it(79) >= aux(17)
aux(11)+it(64)+it(65)+it(66)+it(67)+it(68)+it(70)+it(71)+it(72)+it(73)+it(74)+it(75)+it(76)+it(77)+it(78)+it(79) >= aux(17)
aux(13)+it(64)+it(65)+it(66)+it(67)+it(68)+it(69)+it(71)+it(72)+it(73)+it(74)+it(75)+it(76)+it(77)+it(78)+it(79) >= aux(17)
aux(15)+it(64)+it(65)+it(66)+it(67)+it(68)+it(69)+it(70)+it(72)+it(73)+it(74)+it(75)+it(76)+it(77)+it(78)+it(79) >= aux(17)
it(64)+it(65)+it(66)+it(67)+it(68)+it(69)+it(70)+it(71)+it(72)+it(73)+it(74)+it(75)+it(76)+it(77)+it(78)+it(79) >= aux(17)
it(65)+it(66)+it(67)+it(68)+it(69)+it(70)+it(71)+it(72)+it(73)+it(74)+it(75)+it(76)+it(77)+it(78)+it(79)+s(121)+s(122)+s(123)+s(124)+s(125) >= aux(17)
it(65)+it(66)+it(68)+it(69)+it(70)+it(71)+it(72)+it(73)+it(74)+it(75)+it(76)+it(77)+it(78)+it(79)+s(121)+s(122)+s(123)+s(124)+s(125)+s(136)+s(137)+s(138)+s(139)+s(140) >= aux(17)
it(65)+it(67)+it(68)+it(69)+it(70)+it(71)+it(72)+it(73)+it(74)+it(75)+it(76)+it(77)+it(78)+it(79)+s(121)+s(122)+s(123)+s(124)+s(125)+s(131)+s(132)+s(133)+s(134)+s(135) >= aux(17)
it(66)+it(67)+it(68)+it(69)+it(70)+it(71)+it(72)+it(73)+it(74)+it(75)+it(76)+it(77)+it(78)+it(79)+s(121)+s(122)+s(123)+s(124)+s(125)+s(126)+s(127)+s(128)+s(129)+s(130) >= aux(17)
aux(3) >= aux(1)
s(156)+s(157)+s(158)+s(159)+s(160) >= aux(15)
s(151)+s(152)+s(153)+s(154)+s(155) >= aux(13)
s(146)+s(147)+s(148)+s(149)+s(150) >= aux(11)
s(141)+s(142)+s(143)+s(144)+s(145) >= aux(9)
s(121)+s(122)+s(123)+s(124)+s(125) >= it(64)*aux(1)
s(136)+s(137)+s(138)+s(139)+s(140) >= it(67)*aux(3)
s(131)+s(132)+s(133)+s(134)+s(135) >= it(66)*aux(3)
s(126)+s(127)+s(128)+s(129)+s(130) >= it(65)*aux(3)

#### Cost of chains of lcstable(A,B,C,D):
* Chain [[64,65,66,67,68,69,70,71,72,73,74,75,76,77,78,79],63]: 15*it(64)+15*it(65)+15*it(66)+15*it(67)+18*it(68)+18*it(69)+18*it(70)+18*it(71)+18*it(72)+18*it(73)+18*it(74)+18*it(75)+15*it(76)+15*it(77)+15*it(78)+15*it(79)+8
  Such that:it(64)+it(65)+it(66)+it(67)+it(68)+it(69)+it(70)+it(71)+it(72)+it(73)+it(74)+it(75)+it(76)+it(77)+it(78)+it(79) =< B-1
aux(17) >= B-1
it(64)+it(65)+it(66)+it(67)+it(68)+it(69)+it(70)+it(71)+it(72)+it(73)+it(74)+it(75)+it(76)+it(77)+it(78)+it(79) >= aux(17)

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

* Chain [[64,65,66,67,68,69,70,71,72,73,74,75,76,77,78,79],62]: 15*it(64)+15*it(65)+15*it(66)+15*it(67)+18*it(68)+18*it(69)+18*it(70)+18*it(71)+18*it(72)+18*it(73)+18*it(74)+18*it(75)+15*it(76)+15*it(77)+15*it(78)+15*it(79)+29*s(121)+29*s(122)+29*s(123)+29*s(124)+28*s(125)+29*s(126)+29*s(127)+29*s(128)+29*s(129)+28*s(130)+29*s(131)+29*s(132)+29*s(133)+29*s(134)+28*s(135)+29*s(136)+29*s(137)+29*s(138)+29*s(139)+28*s(140)+29*s(141)+29*s(142)+29*s(143)+29*s(144)+28*s(145)+29*s(146)+29*s(147)+29*s(148)+29*s(149)+28*s(150)+29*s(151)+29*s(152)+29*s(153)+29*s(154)+28*s(155)+29*s(156)+29*s(157)+29*s(158)+29*s(159)+28*s(160)+6*s(161)+8
  Such that:it(64)+it(65)+it(66)+it(67)+it(68)+it(69)+it(70)+it(71)+it(72)+it(73)+it(74)+it(75)+it(76)+it(77)+it(78)+it(79) =< B-1
aux(18) =< D-1
s(161) =< aux(18)
aux(4) =< aux(18)
s(121)+s(122)+s(123)+s(124)+s(125) =< it(64)*aux(18)
s(156)+s(157)+s(158)+s(159)+s(160) =< it(71)*aux(4)
s(151)+s(152)+s(153)+s(154)+s(155) =< it(70)*aux(4)
s(146)+s(147)+s(148)+s(149)+s(150) =< it(69)*aux(4)
s(141)+s(142)+s(143)+s(144)+s(145) =< it(68)*aux(4)
s(136)+s(137)+s(138)+s(139)+s(140) =< it(67)*aux(4)
s(131)+s(132)+s(133)+s(134)+s(135) =< it(66)*aux(4)
s(126)+s(127)+s(128)+s(129)+s(130) =< it(65)*aux(4)
aux(17) >= B-1
aux(19) >= D-1
aux(19) >= aux(19)
s(161) >= aux(19)
aux(9)+it(64)+it(65)+it(66)+it(67)+it(69)+it(70)+it(71)+it(72)+it(73)+it(74)+it(75)+it(76)+it(77)+it(78)+it(79) >= aux(17)
aux(11)+it(64)+it(65)+it(66)+it(67)+it(68)+it(70)+it(71)+it(72)+it(73)+it(74)+it(75)+it(76)+it(77)+it(78)+it(79) >= aux(17)
aux(13)+it(64)+it(65)+it(66)+it(67)+it(68)+it(69)+it(71)+it(72)+it(73)+it(74)+it(75)+it(76)+it(77)+it(78)+it(79) >= aux(17)
aux(15)+it(64)+it(65)+it(66)+it(67)+it(68)+it(69)+it(70)+it(72)+it(73)+it(74)+it(75)+it(76)+it(77)+it(78)+it(79) >= aux(17)
it(64)+it(65)+it(66)+it(67)+it(68)+it(69)+it(70)+it(71)+it(72)+it(73)+it(74)+it(75)+it(76)+it(77)+it(78)+it(79) >= aux(17)
it(65)+it(66)+it(67)+it(68)+it(69)+it(70)+it(71)+it(72)+it(73)+it(74)+it(75)+it(76)+it(77)+it(78)+it(79)+s(121)+s(122)+s(123)+s(124)+s(125) >= aux(17)
it(65)+it(66)+it(68)+it(69)+it(70)+it(71)+it(72)+it(73)+it(74)+it(75)+it(76)+it(77)+it(78)+it(79)+s(121)+s(122)+s(123)+s(124)+s(125)+s(136)+s(137)+s(138)+s(139)+s(140) >= aux(17)
it(65)+it(67)+it(68)+it(69)+it(70)+it(71)+it(72)+it(73)+it(74)+it(75)+it(76)+it(77)+it(78)+it(79)+s(121)+s(122)+s(123)+s(124)+s(125)+s(131)+s(132)+s(133)+s(134)+s(135) >= aux(17)
it(66)+it(67)+it(68)+it(69)+it(70)+it(71)+it(72)+it(73)+it(74)+it(75)+it(76)+it(77)+it(78)+it(79)+s(121)+s(122)+s(123)+s(124)+s(125)+s(126)+s(127)+s(128)+s(129)+s(130) >= aux(17)
aux(3) >= aux(19)
s(156)+s(157)+s(158)+s(159)+s(160) >= aux(15)
s(151)+s(152)+s(153)+s(154)+s(155) >= aux(13)
s(146)+s(147)+s(148)+s(149)+s(150) >= aux(11)
s(141)+s(142)+s(143)+s(144)+s(145) >= aux(9)
s(121)+s(122)+s(123)+s(124)+s(125) >= it(64)*aux(19)
s(136)+s(137)+s(138)+s(139)+s(140) >= it(67)*aux(3)
s(131)+s(132)+s(133)+s(134)+s(135) >= it(66)*aux(3)
s(126)+s(127)+s(128)+s(129)+s(130) >= it(65)*aux(3)

  with precondition: [B>=2,D>=2] 

* Chain [63]: 8
  with precondition: [B=1,D=1] 

* Chain [62]: 6*s(161)+8
  Such that:s(161) =< D-1
s(161) >= D-1

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


#### Cost of chains of lcs(A,B,C,D):
* Chain [83]: 17
  with precondition: [B=1,D=1] 

* Chain [82]: 6*s(162)+17
  Such that:s(162) =< D-1
s(162) >= D-1

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

* Chain [81]: 15*s(163)+15*s(164)+15*s(165)+15*s(166)+18*s(167)+18*s(168)+18*s(169)+18*s(170)+18*s(171)+18*s(172)+18*s(173)+18*s(174)+15*s(175)+15*s(176)+15*s(177)+15*s(178)+17
  Such that:s(163)+s(164)+s(165)+s(166)+s(167)+s(168)+s(169)+s(170)+s(171)+s(172)+s(173)+s(174)+s(175)+s(176)+s(177)+s(178) =< B-1
s(179) >= B-1
s(163)+s(164)+s(165)+s(166)+s(167)+s(168)+s(169)+s(170)+s(171)+s(172)+s(173)+s(174)+s(175)+s(176)+s(177)+s(178) >= s(179)

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

* Chain [80]: 15*s(180)+15*s(181)+15*s(182)+15*s(183)+18*s(184)+18*s(185)+18*s(186)+18*s(187)+18*s(188)+18*s(189)+18*s(190)+18*s(191)+15*s(192)+15*s(193)+15*s(194)+15*s(195)+6*s(199)+29*s(204)+29*s(205)+29*s(206)+29*s(207)+28*s(208)+29*s(209)+29*s(210)+29*s(211)+29*s(212)+28*s(213)+29*s(214)+29*s(215)+29*s(216)+29*s(217)+28*s(218)+29*s(219)+29*s(220)+29*s(221)+29*s(222)+28*s(223)+29*s(226)+29*s(227)+29*s(228)+29*s(229)+28*s(230)+29*s(231)+29*s(232)+29*s(233)+29*s(234)+28*s(235)+29*s(236)+29*s(237)+29*s(238)+29*s(239)+28*s(240)+29*s(241)+29*s(242)+29*s(243)+29*s(244)+28*s(245)+17
  Such that:s(180)+s(181)+s(182)+s(183)+s(184)+s(185)+s(186)+s(187)+s(188)+s(189)+s(190)+s(191)+s(192)+s(193)+s(194)+s(195) =< B-1
s(196) =< D-1
s(199) =< s(196)
s(224) =< s(196)
s(204)+s(205)+s(206)+s(207)+s(208) =< s(180)*s(196)
s(226)+s(227)+s(228)+s(229)+s(230) =< s(187)*s(224)
s(231)+s(232)+s(233)+s(234)+s(235) =< s(186)*s(224)
s(236)+s(237)+s(238)+s(239)+s(240) =< s(185)*s(224)
s(241)+s(242)+s(243)+s(244)+s(245) =< s(184)*s(224)
s(209)+s(210)+s(211)+s(212)+s(213) =< s(183)*s(224)
s(214)+s(215)+s(216)+s(217)+s(218) =< s(182)*s(224)
s(219)+s(220)+s(221)+s(222)+s(223) =< s(181)*s(224)
s(197) >= B-1
s(198) >= D-1
s(198) >= s(198)
s(199) >= s(198)
s(180)+s(181)+s(182)+s(183)+s(185)+s(186)+s(187)+s(188)+s(189)+s(190)+s(191)+s(192)+s(193)+s(194)+s(195)+s(200) >= s(197)
s(180)+s(181)+s(182)+s(183)+s(184)+s(186)+s(187)+s(188)+s(189)+s(190)+s(191)+s(192)+s(193)+s(194)+s(195)+s(201) >= s(197)
s(180)+s(181)+s(182)+s(183)+s(184)+s(185)+s(187)+s(188)+s(189)+s(190)+s(191)+s(192)+s(193)+s(194)+s(195)+s(202) >= s(197)
s(180)+s(181)+s(182)+s(183)+s(184)+s(185)+s(186)+s(188)+s(189)+s(190)+s(191)+s(192)+s(193)+s(194)+s(195)+s(203) >= s(197)
s(180)+s(181)+s(182)+s(183)+s(184)+s(185)+s(186)+s(187)+s(188)+s(189)+s(190)+s(191)+s(192)+s(193)+s(194)+s(195) >= s(197)
s(181)+s(182)+s(183)+s(184)+s(185)+s(186)+s(187)+s(188)+s(189)+s(190)+s(191)+s(192)+s(193)+s(194)+s(195)+s(204)+s(205)+s(206)+s(207)+s(208) >= s(197)
s(181)+s(182)+s(184)+s(185)+s(186)+s(187)+s(188)+s(189)+s(190)+s(191)+s(192)+s(193)+s(194)+s(195)+s(204)+s(205)+s(206)+s(207)+s(208)+s(209)+s(210)+s(211)+s(212)+s(213) >= s(197)
s(181)+s(183)+s(184)+s(185)+s(186)+s(187)+s(188)+s(189)+s(190)+s(191)+s(192)+s(193)+s(194)+s(195)+s(204)+s(205)+s(206)+s(207)+s(208)+s(214)+s(215)+s(216)+s(217)+s(218) >= s(197)
s(182)+s(183)+s(184)+s(185)+s(186)+s(187)+s(188)+s(189)+s(190)+s(191)+s(192)+s(193)+s(194)+s(195)+s(204)+s(205)+s(206)+s(207)+s(208)+s(219)+s(220)+s(221)+s(222)+s(223) >= s(197)
s(225) >= s(198)
s(226)+s(227)+s(228)+s(229)+s(230) >= s(203)
s(231)+s(232)+s(233)+s(234)+s(235) >= s(202)
s(236)+s(237)+s(238)+s(239)+s(240) >= s(201)
s(241)+s(242)+s(243)+s(244)+s(245) >= s(200)
s(204)+s(205)+s(206)+s(207)+s(208) >= s(180)*s(198)
s(209)+s(210)+s(211)+s(212)+s(213) >= s(183)*s(225)
s(214)+s(215)+s(216)+s(217)+s(218) >= s(182)*s(225)
s(219)+s(220)+s(221)+s(222)+s(223) >= s(181)*s(225)

  with precondition: [B>=2,D>=2] 


Closed-form bounds of lcs(A,B,C,D): 
-------------------------------------
* Chain [83] with precondition: [B=1,D=1] 
    - Lower bound: 17 
    - Complexity: constant
 * Chain [82] with precondition: [B=1,D>=2] 
    - Lower bound: 6*D+11 
    - Complexity: n
 * Chain [81] with precondition: [D=1,B>=2] 
    - Lower bound: 15*B+2 
    - Complexity: n
 * Chain [80] with precondition: [B>=2,D>=2] 
    - Lower bound: 15*B+6*D-4 
    - Complexity: n
 
### Partitioned lower bound of lcs(A,B,C,D): 
* 17 
 if [B=1,D=1]
* 6*D+11 
 if [B=1,D>=2]
* 15*B+2 
 if [D=1,B>=2]
* 15*B+6*D-4 
 if [B>=2,D>=2]
Possible lower bounds : [17,6*D+11,15*B+2,15*B+6*D-4]
Maximum lower bound complexity: n
* Total analysis performed in 788 ms.