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 4 ms.
sabu_memo_table_1(case_0,[A,B,C],[1*C>=0,1*C=1],0,0)
sabu_memo_table_1(case_1,[A,B,C,D],[1*D>=0,1*A+ -1*B=0],0,0)
sabu_memo_table_1(anyEq,[A,B,C],[1*C>=0,1*C=1,1*C>=0],1,0)
sabu_memo_table_1(case_0,[A,B,C],[1*C>=1],1,1)
sabu_memo_table_1(anyEq,[A,B,C],[1*C>=1],2,1)
sabu_memo_table_1(case_1,[A,B,C,D],[1*D>=0,1*A+ -1*B>=0],3,1)
sabu_memo_table_1(case_1,[A,B,C,D],[1*D>=0],3,2)
sabu_memo_table_1(case_2,[A,B,C,D],[1*C>=1,1*D=1],0,0)
sabu_memo_table_1(lookupBTree,[A,B,C,D],[1*D>=0,1*C>=0,1*D=1,1*C>=1],0,0)
sabu_memo_table_1(case_5,[A,B,C,D,E,F,G,H,I,J],[1*J>=0,1*I>=0,1*G>=0,1*F>=0,1*D>=0,-1*A+1*B>=0,1*F>=1,1*G=1,1*F>=0,1*G>=0],1,0)
sabu_memo_table_1(case_5,[A,B,C,D,E,F,G,H,I,J],[1*G>=0,1*F>=0,1*D+1*F>=1,1*D+1*G>=1,1*D>=0,1*J>=0,1*I>=0],1,1)
sabu_memo_table_1(case_5,[A,B,C,D,E,F,G,H,I,J],[1*D+1*F+1*I>=1,1*D+1*G+1*I>=1,1*I>=0,1*D>=0,1*F>=0,1*G>=0,1*J>=0],1,2)
sabu_memo_table_1(case_4,[A,B,C,D,E,F,G],[2*C+1*G>=1,1*C+1*D+1*G>=2,1*D>=1,1*C>=0,1*G>=0],2,0)
sabu_memo_table_1(case_3,[A,B,C,D,E,F],[1*C+1*E+1*F>=3,1*C+2*E>=2,1*E>=0,1*F>=1,1*C>=1],3,0)
sabu_memo_table_1(case_2,[A,B,C,D],[1*D>=1,1*C>=1],4,1)
sabu_memo_table_1(lookupBTree,[A,B,C,D],[1*C>=1,1*D>=1],5,1)
sabu_memo_table_1(start,[A,B,C,D],[1*D>=0,1*C>=0,1*D>=1,1*C>=1],0,0)
sabu_memo_table_1(start,[],[],0,0)
:- dynamic sabu_memo_table_1/5.

sabu_memo_table_1(case_0, [_, _, A], [1*A>=1], 1, 1).
sabu_memo_table_1(anyEq, [_, _, A], [1*A>=1], 2, 1).
sabu_memo_table_1(case_1, [_, _, _, A], [1*A>=0], 3, 2).
sabu_memo_table_1(case_5, [_, _, _, A, _, B, D, _, C, E], [1*A+1*B+1*C>=1, 1*A+1*D+1*C>=1, 1*C>=0, 1*A>=0, 1*B>=0, 1*D>=0, 1*E>=0], 1, 2).
sabu_memo_table_1(case_4, [_, _, A, C, _, _, B], [2*A+1*B>=1, 1*A+1*C+1*B>=2, 1*C>=1, 1*A>=0, 1*B>=0], 2, 0).
sabu_memo_table_1(case_3, [_, _, A, _, B, C], [1*A+1*B+1*C>=3, 1*A+2*B>=2, 1*B>=0, 1*C>=1, 1*A>=1], 3, 0).
sabu_memo_table_1(case_2, [_, _, B, A], [1*A>=1, 1*B>=1], 4, 1).
sabu_memo_table_1(lookupBTree, [_, _, A, B], [1*A>=1, 1*B>=1], 5, 1).
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 6 ms.

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

Generated 37 equations 

Cost relation system solved by PUBS in 44 ms.

Method start terminates?: YES

 - n_1: size of n wrt. Rat
 - node_1: size of node wrt. Rat
 - node_2: size of node wrt. List<Rat>
 - node_3: size of node wrt. [Tree,List<Tree>]
UB for start(n_1,node_1,node_2,node_3) = nat(node_3)+c(maximize_failed)


Method start terminates?: YES

 - n_1: size of n wrt. Rat
 - node_1: size of node wrt. Rat
 - node_2: size of node wrt. List<Rat>
 - node_3: size of node wrt. [Tree,List<Tree>]
UB for start(n_1,node_1,node_2,node_3) = nat(node_3)+c(maximize_failed)


Method start terminates?: YES

UB for start(n_1,node_1,node_2,node_3) = nat(node_3)+c(maximize_failed)


Method start terminates?: YES

UB for start(n_1,node_1,node_2,node_3) = nat(node_3)+c(maximize_failed)


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

#### Computed strongly connected components 
0. recursive  : [anyEq/3,case_0/3,case_1/4]
1. non_recursive  : [maxNorm/2]
2. recursive  : [case_2/4,case_3/6,case_4/7,case_5/10,lookupBTree/4]
4. non_recursive  : [start/4]
* The entry case_5/10 is not a cutpoint so it becomes a new SCC 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 anyEq/3
1. SCC is partially evaluated into maxNorm/2
2. SCC is partially evaluated into lookupBTree/4
4. SCC is partially evaluated into case_5/10

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

### Specialization of cost equations anyEq/3 
* CE 8 is refined into CE [11] 
* CE 10 is refined into CE [12] 
* CE 9 is refined into CE [13] 


#### Refined cost equations anyEq/3 
* CE 11: anyEq(A,B,C) = 6
     [B>=A,C>=1] 
* CE 12: anyEq(A,B,C) = 3
     [C=1] 
* CE 13: anyEq(A,B,C) = 6+ anyEq(A,D,E)
     [B>=D,E>=0,E+1=C] 

### Cost equations --> "Loop" of anyEq/3 
* CEs [13] --> Loop 11 
* CEs [11] --> Loop 12 
* CEs [12] --> Loop 13 

#### Loops of anyEq/3 
* Loop 11: anyEq(A,B,C)->  anyEq(A,B',C')
                  [B>=B',C'>=0,C'+1=C] 
* Loop 12: anyEq(A,B,C) [B>=A,C>=1] 
* Loop 13: anyEq(A,B,C) [C=1] 

### Ranking functions of CR anyEq(A,B,C) 
* RF of phase [11]: [C]

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


### Resulting Chains:anyEq(A,B,C) 
* [[11],13]
* [[11],12]
* [13]
* [12]


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


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

### Cost equations --> "Loop" of maxNorm/2 
* CEs [14] --> Loop 14 
* CEs [15] --> Loop 15 

#### Loops of maxNorm/2 
* Loop 14: maxNorm(A,B) [A>=B+1,B>=0] 
* Loop 15: 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) 
* [15]
* [14]


### Specialization of cost equations lookupBTree/4 
* CE 6 is refined into CE [16,17] 
* CE 7 is refined into CE [18] 
* CE 5 is refined into CE [19,20,21,22] 


#### Refined cost equations lookupBTree/4 
* CE 16: lookupBTree(A,B,C,D) = 11+ maxNorm(E,F):[15]+ lookupBTree(A,G,H,I)
     [D>=I+1,C>=F,F>=E,C>=E+1,I>=1,E>=0] 
* CE 17: lookupBTree(A,B,C,D) = 11+ maxNorm(E,F):[14]+ lookupBTree(A,G,H,I)
     [D>=I+1,E>=F+1,C>=E+1,I>=1,F>=0] 
* CE 18: lookupBTree(A,B,C,D) = 10+ lookupBTree(A,E,F,G)
     [D>=G+2,C>=F,B>=E,B>=A,G>=0,F>=0,C>=1] 
* CE 19: lookupBTree(A,B,C,D) = 3+ anyEq(A,B,C):[[11],13]
     [C>=2,D=1] 
* CE 20: lookupBTree(A,B,C,D) = 3+ anyEq(A,B,C):[[11],12]
     [B>=A,C>=2,D=1] 
* CE 21: lookupBTree(A,B,C,D) = 3+ anyEq(A,B,E):[13]
     [E=1,D=1,C=1] 
* CE 22: lookupBTree(A,B,C,D) = 3+ anyEq(A,B,C):[12]
     [B>=A,C>=1,D=1] 

### Cost equations --> "Loop" of lookupBTree/4 
* CEs [20] --> Loop 16 
* CEs [19] --> Loop 17 
* CEs [22] --> Loop 18 
* CEs [21] --> Loop 19 
* CEs [17] --> Loop 20 
* CEs [16] --> Loop 21 
* CEs [18] --> Loop 22 

#### Loops of lookupBTree/4 
* Loop 16: lookupBTree(A,B,C,D) [B>=A,C>=2,D=1] 
* Loop 17: lookupBTree(A,B,C,D) [C>=2,D=1] 
* Loop 18: lookupBTree(A,B,C,D) [B>=A,C>=1,D=1] 
* Loop 19: lookupBTree(A,B,C,D) [D=1,C=1] 
* Loop 20: lookupBTree(A,B,C,D)->  lookupBTree(A,B',C',D')
                  [D>=D'+1,D'>=1,C>=2] 
* Loop 21: lookupBTree(A,B,C,D)->  lookupBTree(A,B',C',D')
                  [D>=D'+1,D'>=1,C>=1] 
* Loop 22: lookupBTree(A,B,C,D)->  lookupBTree(A,B',C',D')
                  [D>=D'+2,C>=C',B>=B',B>=A,D'>=0,C'>=0,C>=1] 

### Ranking functions of CR lookupBTree(A,B,C,D) 
* RF of phase [20,21,22]: [D-1]

#### Partial ranking functions of CR lookupBTree(A,B,C,D) 
* Partial RF of phase [20,21,22]:
  - RF of loop [20:1,21:1]:
    D-1
  - RF of loop [22:1]:
    D/2-1/2


### Resulting Chains:lookupBTree(A,B,C,D) 
* [[20,21,22],19]
* [[20,21,22],18]
* [[20,21,22],17]
* [[20,21,22],16]
* [19]
* [18]
* [17]
* [16]


### Specialization of cost equations case_5/10 
* CE 1 is refined into CE [23,24,25,26,27,28,29,30,31,32,33,34,35,36,37,38] 
* CE 2 is refined into CE [39,40,41,42,43,44,45,46] 


#### Refined cost equations case_5/10 
* CE 23: case_5(A,B,C,D,E,F,G,H,I,J) = 3+ maxNorm(D,I):[15]+ lookupBTree(A,K,L,M):[[20,21,22],19]
     [I>=D,K>=H,K>=C,A>=B+1,M>=2,L>=1,D>=0,G>=0,F>=0,M=J+1] 
* CE 24: case_5(A,B,C,D,E,F,G,H,I,J) = 3+ maxNorm(D,I):[15]+ lookupBTree(A,K,L,M):[[20,21,22],18]
     [I>=D,K>=H,K>=C,A>=B+1,M>=2,L>=1,D>=0,G>=0,F>=0,M=J+1] 
* CE 25: case_5(A,B,C,D,E,F,G,H,I,J) = 3+ maxNorm(D,I):[15]+ lookupBTree(A,K,L,M):[[20,21,22],17]
     [I>=D,K>=H,K>=C,A>=B+1,M>=2,L>=1,D>=0,G>=0,F>=0,M=J+1] 
* CE 26: case_5(A,B,C,D,E,F,G,H,I,J) = 3+ maxNorm(D,I):[15]+ lookupBTree(A,K,L,M):[[20,21,22],16]
     [I>=D,K>=H,K>=C,A>=B+1,M>=2,L>=1,D>=0,G>=0,F>=0,M=J+1] 
* CE 27: case_5(A,B,C,D,E,F,G,H,I,J) = 3+ maxNorm(D,I):[15]+ lookupBTree(A,K,L,M):[19]
     [I>=D,K>=H,K>=C,A>=B+1,D>=0,G>=0,F>=0,M=1,L=1,J=0] 
* CE 28: case_5(A,B,C,D,E,F,G,H,I,J) = 3+ maxNorm(D,I):[15]+ lookupBTree(A,K,L,M):[18]
     [K>=A,I>=D,K>=H,K>=C,A>=B+1,L>=1,D>=0,G>=0,F>=0,M=1,J=0] 
* CE 29: case_5(A,B,C,D,E,F,G,H,I,J) = 3+ maxNorm(D,I):[15]+ lookupBTree(A,K,L,M):[17]
     [I>=D,K>=H,K>=C,A>=B+1,L>=2,D>=0,G>=0,F>=0,M=1,J=0] 
* CE 30: case_5(A,B,C,D,E,F,G,H,I,J) = 3+ maxNorm(D,I):[15]+ lookupBTree(A,K,L,M):[16]
     [K>=A,I>=D,K>=H,K>=C,A>=B+1,L>=2,D>=0,G>=0,F>=0,M=1,J=0] 
* CE 31: case_5(A,B,C,D,E,F,G,H,I,J) = 3+ maxNorm(D,I):[14]+ lookupBTree(A,K,L,M):[[20,21,22],19]
     [D>=I+1,K>=H,K>=C,A>=B+1,M>=2,L>=1,I>=0,G>=0,F>=0,M=J+1] 
* CE 32: case_5(A,B,C,D,E,F,G,H,I,J) = 3+ maxNorm(D,I):[14]+ lookupBTree(A,K,L,M):[[20,21,22],18]
     [D>=I+1,K>=H,K>=C,A>=B+1,M>=2,L>=1,I>=0,G>=0,F>=0,M=J+1] 
* CE 33: case_5(A,B,C,D,E,F,G,H,I,J) = 3+ maxNorm(D,I):[14]+ lookupBTree(A,K,L,M):[[20,21,22],17]
     [D>=I+1,K>=H,K>=C,A>=B+1,M>=2,L>=1,I>=0,G>=0,F>=0,M=J+1] 
* CE 34: case_5(A,B,C,D,E,F,G,H,I,J) = 3+ maxNorm(D,I):[14]+ lookupBTree(A,K,L,M):[[20,21,22],16]
     [D>=I+1,K>=H,K>=C,A>=B+1,M>=2,L>=1,I>=0,G>=0,F>=0,M=J+1] 
* CE 35: case_5(A,B,C,D,E,F,G,H,I,J) = 3+ maxNorm(D,I):[14]+ lookupBTree(A,K,L,M):[19]
     [D>=I+1,K>=H,K>=C,A>=B+1,I>=0,G>=0,F>=0,M=1,L=1,J=0] 
* CE 36: case_5(A,B,C,D,E,F,G,H,I,J) = 3+ maxNorm(D,I):[14]+ lookupBTree(A,K,L,M):[18]
     [K>=A,D>=I+1,K>=H,K>=C,A>=B+1,L>=1,I>=0,G>=0,F>=0,M=1,J=0] 
* CE 37: case_5(A,B,C,D,E,F,G,H,I,J) = 3+ maxNorm(D,I):[14]+ lookupBTree(A,K,L,M):[17]
     [D>=I+1,K>=H,K>=C,A>=B+1,L>=2,I>=0,G>=0,F>=0,M=1,J=0] 
* CE 38: case_5(A,B,C,D,E,F,G,H,I,J) = 3+ maxNorm(D,I):[14]+ lookupBTree(A,K,L,M):[16]
     [K>=A,D>=I+1,K>=H,K>=C,A>=B+1,L>=2,I>=0,G>=0,F>=0,M=1,J=0] 
* CE 39: case_5(A,B,C,D,E,F,G,H,I,J) = 2+ lookupBTree(A,E,F,G):[[20,21,22],19]
     [B>=A,G>=2,F>=1,J>=0,I>=0,D>=0] 
* CE 40: case_5(A,B,C,D,E,F,G,H,I,J) = 2+ lookupBTree(A,E,F,G):[[20,21,22],18]
     [B>=A,G>=2,F>=1,J>=0,I>=0,D>=0] 
* CE 41: case_5(A,B,C,D,E,F,G,H,I,J) = 2+ lookupBTree(A,E,F,G):[[20,21,22],17]
     [B>=A,G>=2,F>=1,J>=0,I>=0,D>=0] 
* CE 42: case_5(A,B,C,D,E,F,G,H,I,J) = 2+ lookupBTree(A,E,F,G):[[20,21,22],16]
     [B>=A,G>=2,F>=1,J>=0,I>=0,D>=0] 
* CE 43: case_5(A,B,C,D,E,F,G,H,I,J) = 2+ lookupBTree(A,E,K,L):[19]
     [B>=A,J>=0,I>=0,D>=0,L=1,K=1,G=1,F=1] 
* CE 44: case_5(A,B,C,D,E,F,G,H,I,J) = 2+ lookupBTree(A,E,F,K):[18]
     [E>=A,B>=A,F>=1,J>=0,I>=0,D>=0,K=1,G=1] 
* CE 45: case_5(A,B,C,D,E,F,G,H,I,J) = 2+ lookupBTree(A,E,F,K):[17]
     [B>=A,F>=2,J>=0,I>=0,D>=0,K=1,G=1] 
* CE 46: case_5(A,B,C,D,E,F,G,H,I,J) = 2+ lookupBTree(A,E,F,K):[16]
     [E>=A,B>=A,F>=2,J>=0,I>=0,D>=0,K=1,G=1] 

### Cost equations --> "Loop" of case_5/10 
* CEs [34] --> Loop 23 
* CEs [33] --> Loop 24 
* CEs [32] --> Loop 25 
* CEs [31] --> Loop 26 
* CEs [42] --> Loop 27 
* CEs [41] --> Loop 28 
* CEs [40] --> Loop 29 
* CEs [39] --> Loop 30 
* CEs [26] --> Loop 31 
* CEs [25] --> Loop 32 
* CEs [24] --> Loop 33 
* CEs [23] --> Loop 34 
* CEs [38] --> Loop 35 
* CEs [37] --> Loop 36 
* CEs [36] --> Loop 37 
* CEs [35] --> Loop 38 
* CEs [30] --> Loop 39 
* CEs [29] --> Loop 40 
* CEs [28] --> Loop 41 
* CEs [27] --> Loop 42 
* CEs [46] --> Loop 43 
* CEs [45] --> Loop 44 
* CEs [44] --> Loop 45 
* CEs [43] --> Loop 46 

#### Loops of case_5/10 
* Loop 23: case_5(A,B,C,D,E,F,G,H,I,J) [D>=I+1,A>=B+1,J>=1,I>=0,G>=0,F>=0] 
* Loop 24: case_5(A,B,C,D,E,F,G,H,I,J) [D>=I+1,A>=B+1,J>=1,I>=0,G>=0,F>=0] 
* Loop 25: case_5(A,B,C,D,E,F,G,H,I,J) [D>=I+1,A>=B+1,J>=1,I>=0,G>=0,F>=0] 
* Loop 26: case_5(A,B,C,D,E,F,G,H,I,J) [D>=I+1,A>=B+1,J>=1,I>=0,G>=0,F>=0] 
* Loop 27: case_5(A,B,C,D,E,F,G,H,I,J) [B>=A,J>=0,I>=0,G>=2,F>=1,D>=0] 
* Loop 28: case_5(A,B,C,D,E,F,G,H,I,J) [B>=A,J>=0,I>=0,G>=2,F>=1,D>=0] 
* Loop 29: case_5(A,B,C,D,E,F,G,H,I,J) [B>=A,J>=0,I>=0,G>=2,F>=1,D>=0] 
* Loop 30: case_5(A,B,C,D,E,F,G,H,I,J) [B>=A,J>=0,I>=0,G>=2,F>=1,D>=0] 
* Loop 31: case_5(A,B,C,D,E,F,G,H,I,J) [I>=D,A>=B+1,J>=1,G>=0,F>=0,D>=0] 
* Loop 32: case_5(A,B,C,D,E,F,G,H,I,J) [I>=D,A>=B+1,J>=1,G>=0,F>=0,D>=0] 
* Loop 33: case_5(A,B,C,D,E,F,G,H,I,J) [I>=D,A>=B+1,J>=1,G>=0,F>=0,D>=0] 
* Loop 34: case_5(A,B,C,D,E,F,G,H,I,J) [I>=D,A>=B+1,J>=1,G>=0,F>=0,D>=0] 
* Loop 35: case_5(A,B,C,D,E,F,G,H,I,J) [D>=I+1,A>=B+1,I>=0,G>=0,F>=0,J=0] 
* Loop 36: case_5(A,B,C,D,E,F,G,H,I,J) [D>=I+1,A>=B+1,I>=0,G>=0,F>=0,J=0] 
* Loop 37: case_5(A,B,C,D,E,F,G,H,I,J) [D>=I+1,A>=B+1,I>=0,G>=0,F>=0,J=0] 
* Loop 38: case_5(A,B,C,D,E,F,G,H,I,J) [D>=I+1,A>=B+1,I>=0,G>=0,F>=0,J=0] 
* Loop 39: case_5(A,B,C,D,E,F,G,H,I,J) [I>=D,A>=B+1,G>=0,F>=0,D>=0,J=0] 
* Loop 40: case_5(A,B,C,D,E,F,G,H,I,J) [I>=D,A>=B+1,G>=0,F>=0,D>=0,J=0] 
* Loop 41: case_5(A,B,C,D,E,F,G,H,I,J) [I>=D,A>=B+1,G>=0,F>=0,D>=0,J=0] 
* Loop 42: case_5(A,B,C,D,E,F,G,H,I,J) [I>=D,A>=B+1,G>=0,F>=0,D>=0,J=0] 
* Loop 43: case_5(A,B,C,D,E,F,G,H,I,J) [E>=A,B>=A,J>=0,I>=0,F>=2,D>=0,G=1] 
* Loop 44: case_5(A,B,C,D,E,F,G,H,I,J) [B>=A,J>=0,I>=0,F>=2,D>=0,G=1] 
* Loop 45: case_5(A,B,C,D,E,F,G,H,I,J) [E>=A,B>=A,J>=0,I>=0,F>=1,D>=0,G=1] 
* Loop 46: case_5(A,B,C,D,E,F,G,H,I,J) [B>=A,J>=0,I>=0,D>=0,G=1,F=1] 

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

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


### Resulting Chains:case_5(A,B,C,D,E,F,G,H,I,J) 
* [46]
* [45]
* [44]
* [43]
* [42]
* [41]
* [40]
* [39]
* [38]
* [37]
* [36]
* [35]
* [34]
* [33]
* [32]
* [31]
* [30]
* [29]
* [28]
* [27]
* [26]
* [25]
* [24]
* [23]


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

#### Cost of loops [11] 

 * loop 11:anyEq(A,B,C) -> [anyEq(A',B',C')] 
6
#### Cost of phase [11]:anyEq(A,B,C) -> [anyEq(A',B',C')] 
6*it(11)+0
  Such that:it(11) =< C
it(11) =< C-C'
it(11) >= C-C'

#### Cost of phase [11]:anyEq(A,B,C) -> [anyEq(A',B',C')] 
6*it(11)+0
  Such that:it(11) =< C
it(11) =< C-C'
it(11) >= C-C'

#### Cost of chains of anyEq(A,B,C):
* Chain [[11],13]: 6*it(11)+3
  Such that:it(11) =< C-1
it(11) >= C-1

  with precondition: [C>=2] 

* Chain [[11],12]: 6*it(11)+6
  Such that:it(11) =< C-1
it(11) >= 1

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

* Chain [13]: 3
  with precondition: [C=1] 

* Chain [12]: 6
  with precondition: [C>=1,B>=A] 


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

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


#### Cost of loops [20,21,22] 

 * loop 20:lookupBTree(A,B,C,D) -> [lookupBTree(A',B',C',D')] 
11
 * loop 21:lookupBTree(A,B,C,D) -> [lookupBTree(A',B',C',D')] 
11
 * loop 22:lookupBTree(A,B,C,D) -> [lookupBTree(A',B',C',D')] 
10
#### Cost of phase [20,21,22]:lookupBTree(A,B,C,D) -> [lookupBTree(A',B',C',D')] 
11*it(20)+11*it(21)+10*it(22)+0
  Such that:it(20)+it(21)+it(22) =< D-1
it(20)+it(21)+it(22) =< D-D'
it(22) =< D/2-1/2
it(22) =< D/2-D'/2

#### Cost of phase [20,21,22]:lookupBTree(A,B,C,D) -> [lookupBTree(A',B',C',D')] 
11*it(20)+11*it(21)+10*it(22)+0
  Such that:it(20)+it(21)+it(22) =< D-1
it(20)+it(21)+it(22) =< D-D'
it(22) =< D/2-1/2
it(22) =< D/2-D'/2

#### Cost of phase [20,21,22]:lookupBTree(A,B,C,D) -> [lookupBTree(A',B',C',D')] 
11*it(20)+11*it(21)+10*it(22)+0
  Such that:it(20)+it(21)+it(22) =< D-1
it(20)+it(21)+it(22) =< D-D'
it(22) =< D/2-1/2
it(22) =< D/2-D'/2

#### Cost of loops [20,21,22] 

 * loop 20:lookupBTree(A,B,C,D) -> [lookupBTree(A',B',C',D')] 
11
 * loop 21:lookupBTree(A,B,C,D) -> [lookupBTree(A',B',C',D')] 
11
 * loop 22:lookupBTree(A,B,C,D) -> [lookupBTree(A',B',C',D')] 
10
#### Cost of phase [20,21,22]:lookupBTree(A,B,C,D) -> [] 
11*it(20)+11*it(21)+10*it(22)+6*it([17])+6*s(2)+0
  Such that:it([17]) =< 1
it(20)+it(21)+it(22) =< D-1
it(22) =< D/2-1/2

#### Cost of phase [20,21,22]:lookupBTree(A,B,C,D) -> [lookupBTree(A',B',C',D')] 
11*it(20)+11*it(21)+10*it(22)+0
  Such that:it(20)+it(21)+it(22) =< D-1
it(20)+it(21)+it(22) =< D-D'
it(22) =< D/2-1/2
it(22) =< D/2-D'/2

#### Cost of loops [20,21,22] 

 * loop 20:lookupBTree(A,B,C,D) -> [lookupBTree(A',B',C',D')] 
11
 * loop 21:lookupBTree(A,B,C,D) -> [lookupBTree(A',B',C',D')] 
11
 * loop 22:lookupBTree(A,B,C,D) -> [lookupBTree(A',B',C',D')] 
10
#### Cost of phase [20,21,22]:lookupBTree(A,B,C,D) -> [] 
11*it(20)+11*it(21)+10*it(22)+9*it([16])+6*s(4)+0
  Such that:it([16]) =< 1
it(20)+it(21)+it(22) =< D-1
it(22) =< D/2-1/2

#### Cost of chains of lookupBTree(A,B,C,D):
* Chain [[20,21,22],19]: 11*it(20)+11*it(21)+10*it(22)+6
  Such that:it(20)+it(21)+it(22) =< D-1

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

* Chain [[20,21,22],18]: 11*it(20)+11*it(21)+10*it(22)+9
  Such that:it(20)+it(21)+it(22) =< D-1

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

* Chain [[20,21,22],17]: 11*it(20)+11*it(21)+10*it(22)+6*it([17])+6*s(2)+0
  Such that:it([17]) =< 1
it(20)+it(21)+it(22) =< D-1
it(22) =< D/2-1/2

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

* Chain [[20,21,22],16]: 11*it(20)+11*it(21)+10*it(22)+9*it([16])+6*s(4)+0
  Such that:it([16]) =< 1
it(20)+it(21)+it(22) =< D-1
it(22) =< D/2-1/2

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

* Chain [19]: 6
  with precondition: [C=1,D=1] 

* Chain [18]: 9
  with precondition: [D=1,C>=1,B>=A] 

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

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

* Chain [16]: 6*s(3)+9
  Such that:s(3) =< C-1
s(3) >= 1

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


#### Cost of chains of case_5(A,B,C,D,E,F,G,H,I,J):
* Chain [46]: 8
  with precondition: [F=1,G=1,D>=0,I>=0,J>=0,B>=A] 

* Chain [45]: 11
  with precondition: [G=1,D>=0,F>=1,I>=0,J>=0,B>=A,E>=A] 

* Chain [44]: 6*s(5)+8
  Such that:s(5) =< F-1
s(5) >= F-1

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

* Chain [43]: 6*s(6)+11
  Such that:s(6) =< F-1
s(6) >= 1

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

* Chain [42]: 9
  with precondition: [J=0,D>=0,F>=0,G>=0,A>=B+1,I>=D] 

* Chain [41]: 12
  with precondition: [J=0,D>=0,F>=0,G>=0,A>=B+1,I>=D] 

* Chain [40]: 6*s(7)+9
  Such that:s(7) >= 1

  with precondition: [J=0,D>=0,F>=0,G>=0,A>=B+1,I>=D] 

* Chain [39]: 6*s(8)+12
  Such that:s(8) >= 1

  with precondition: [J=0,D>=0,F>=0,G>=0,A>=B+1,I>=D] 

* Chain [38]: 9
  with precondition: [J=0,F>=0,G>=0,I>=0,A>=B+1,D>=I+1] 

* Chain [37]: 12
  with precondition: [J=0,F>=0,G>=0,I>=0,A>=B+1,D>=I+1] 

* Chain [36]: 6*s(9)+9
  Such that:s(9) >= 1

  with precondition: [J=0,F>=0,G>=0,I>=0,A>=B+1,D>=I+1] 

* Chain [35]: 6*s(10)+12
  Such that:s(10) >= 1

  with precondition: [J=0,F>=0,G>=0,I>=0,A>=B+1,D>=I+1] 

* Chain [34]: 11*s(11)+11*s(12)+10*s(13)+9
  Such that:s(11)+s(12)+s(13) =< J

  with precondition: [D>=0,F>=0,G>=0,J>=1,A>=B+1,I>=D] 

* Chain [33]: 11*s(14)+11*s(15)+10*s(16)+12
  Such that:s(14)+s(15)+s(16) =< J

  with precondition: [D>=0,F>=0,G>=0,J>=1,A>=B+1,I>=D] 

* Chain [32]: 6*s(17)+11*s(18)+11*s(19)+10*s(20)+6*s(21)+3
  Such that:s(17) =< 1
s(18)+s(19)+s(20) =< J

  with precondition: [D>=0,F>=0,G>=0,J>=1,A>=B+1,I>=D] 

* Chain [31]: 9*s(22)+11*s(23)+11*s(24)+10*s(25)+6*s(26)+3
  Such that:s(22) =< 1
s(23)+s(24)+s(25) =< J

  with precondition: [D>=0,F>=0,G>=0,J>=1,A>=B+1,I>=D] 

* Chain [30]: 11*s(27)+11*s(28)+10*s(29)+8
  Such that:s(27)+s(28)+s(29) =< G-1

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

* Chain [29]: 11*s(30)+11*s(31)+10*s(32)+11
  Such that:s(30)+s(31)+s(32) =< G-1

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

* Chain [28]: 6*s(33)+11*s(34)+11*s(35)+10*s(36)+6*s(37)+2
  Such that:s(33) =< 1
s(34)+s(35)+s(36) =< G-1

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

* Chain [27]: 9*s(38)+11*s(39)+11*s(40)+10*s(41)+6*s(42)+2
  Such that:s(38) =< 1
s(39)+s(40)+s(41) =< G-1

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

* Chain [26]: 11*s(43)+11*s(44)+10*s(45)+9
  Such that:s(43)+s(44)+s(45) =< J

  with precondition: [F>=0,G>=0,I>=0,J>=1,A>=B+1,D>=I+1] 

* Chain [25]: 11*s(46)+11*s(47)+10*s(48)+12
  Such that:s(46)+s(47)+s(48) =< J

  with precondition: [F>=0,G>=0,I>=0,J>=1,A>=B+1,D>=I+1] 

* Chain [24]: 6*s(49)+11*s(50)+11*s(51)+10*s(52)+6*s(53)+3
  Such that:s(49) =< 1
s(50)+s(51)+s(52) =< J

  with precondition: [F>=0,G>=0,I>=0,J>=1,A>=B+1,D>=I+1] 

* Chain [23]: 9*s(54)+11*s(55)+11*s(56)+10*s(57)+6*s(58)+3
  Such that:s(54) =< 1
s(55)+s(56)+s(57) =< J

  with precondition: [F>=0,G>=0,I>=0,J>=1,A>=B+1,D>=I+1] 


Closed-form bounds of case_5(A,B,C,D,E,F,G,H,I,J): 
-------------------------------------
* Chain [46] with precondition: [F=1,G=1,D>=0,I>=0,J>=0,B>=A] 
    - Lower bound: 8 
    - Complexity: constant
 * Chain [45] with precondition: [G=1,D>=0,F>=1,I>=0,J>=0,B>=A,E>=A] 
    - Lower bound: 11 
    - Complexity: constant
 * Chain [44] with precondition: [G=1,D>=0,F>=2,I>=0,J>=0,B>=A] 
    - Lower bound: 6*F+2 
    - Complexity: n
 * Chain [43] with precondition: [G=1,D>=0,F>=2,I>=0,J>=0,B>=A,E>=A] 
    - Lower bound: 17 
    - Complexity: constant
 * Chain [42] with precondition: [J=0,D>=0,F>=0,G>=0,A>=B+1,I>=D] 
    - Lower bound: 9 
    - Complexity: constant
 * Chain [41] with precondition: [J=0,D>=0,F>=0,G>=0,A>=B+1,I>=D] 
    - Lower bound: 12 
    - Complexity: constant
 * Chain [40] with precondition: [J=0,D>=0,F>=0,G>=0,A>=B+1,I>=D] 
    - Lower bound: 15 
    - Complexity: constant
 * Chain [39] with precondition: [J=0,D>=0,F>=0,G>=0,A>=B+1,I>=D] 
    - Lower bound: 18 
    - Complexity: constant
 * Chain [38] with precondition: [J=0,F>=0,G>=0,I>=0,A>=B+1,D>=I+1] 
    - Lower bound: 9 
    - Complexity: constant
 * Chain [37] with precondition: [J=0,F>=0,G>=0,I>=0,A>=B+1,D>=I+1] 
    - Lower bound: 12 
    - Complexity: constant
 * Chain [36] with precondition: [J=0,F>=0,G>=0,I>=0,A>=B+1,D>=I+1] 
    - Lower bound: 15 
    - Complexity: constant
 * Chain [35] with precondition: [J=0,F>=0,G>=0,I>=0,A>=B+1,D>=I+1] 
    - Lower bound: 18 
    - Complexity: constant
 * Chain [34] with precondition: [D>=0,F>=0,G>=0,J>=1,A>=B+1,I>=D] 
    - Lower bound: 9 
    - Complexity: constant
 * Chain [33] with precondition: [D>=0,F>=0,G>=0,J>=1,A>=B+1,I>=D] 
    - Lower bound: 12 
    - Complexity: constant
 * Chain [32] with precondition: [D>=0,F>=0,G>=0,J>=1,A>=B+1,I>=D] 
    - Lower bound: 3 
    - Complexity: constant
 * Chain [31] with precondition: [D>=0,F>=0,G>=0,J>=1,A>=B+1,I>=D] 
    - Lower bound: 3 
    - Complexity: constant
 * Chain [30] with precondition: [D>=0,F>=1,G>=2,I>=0,J>=0,B>=A] 
    - Lower bound: 8 
    - Complexity: constant
 * Chain [29] with precondition: [D>=0,F>=1,G>=2,I>=0,J>=0,B>=A] 
    - Lower bound: 11 
    - Complexity: constant
 * Chain [28] with precondition: [D>=0,F>=1,G>=2,I>=0,J>=0,B>=A] 
    - Lower bound: 2 
    - Complexity: constant
 * Chain [27] with precondition: [D>=0,F>=1,G>=2,I>=0,J>=0,B>=A] 
    - Lower bound: 2 
    - Complexity: constant
 * Chain [26] with precondition: [F>=0,G>=0,I>=0,J>=1,A>=B+1,D>=I+1] 
    - Lower bound: 9 
    - Complexity: constant
 * Chain [25] with precondition: [F>=0,G>=0,I>=0,J>=1,A>=B+1,D>=I+1] 
    - Lower bound: 12 
    - Complexity: constant
 * Chain [24] with precondition: [F>=0,G>=0,I>=0,J>=1,A>=B+1,D>=I+1] 
    - Lower bound: 3 
    - Complexity: constant
 * Chain [23] with precondition: [F>=0,G>=0,I>=0,J>=1,A>=B+1,D>=I+1] 
    - Lower bound: 3 
    - Complexity: constant
 
### Partitioned lower bound of case_5(A,B,C,D,E,F,G,H,I,J): 
* 2 
 if [D>=0,F>=1,G>=2,I>=0,J>=0,B>=A]
* 3 
 if [F>=0,G>=0,I>=0,J>=1,A>=B+1,D>=I+1]
 or [D>=0,F>=0,G>=0,J>=1,A>=B+1,I>=D]
* 8 
 if [F=1,G=1,D>=0,I>=0,J>=0,B>=A]
* 9 
 if [J=0,F>=0,G>=0,I>=0,A>=B+1,D>=I+1]
 or [J=0,D>=0,F>=0,G>=0,A>=B+1,I>=D]
* 11 
 if [G=1,D>=0,F>=2,I>=0,J>=0,B>=A,E>=A]
* 6*F+2 
 if [G=1,D>=0,F>=2,I>=0,J>=0,B>=A,A>=E+1]
Possible lower bounds : [2,3,8,9,11,6*F+2]
Maximum lower bound complexity: n
* Total analysis performed in 254 ms.