Abs program loaded in 3 ms.

Rule based representation generated in 1 ms.

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

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

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

Abstract compilation performed in 1 ms.
sabu_memo_table_1(truncate,[A,B],[],0,0)
sabu_memo_table_1(case_0,[A,B],[1*A+ -1*B>=1,1*A+ -1*B=1,1*A>=2],0,0)
sabu_memo_table_1(eval,[A,B],[1*A>=2,1*A+ -1*B=1,1*A+ -1*B>=1],0,0)
sabu_memo_table_1(case_0,[A,B],[2*A+ -1*B>=3,-1*A+1*B>= -1],1,1)
sabu_memo_table_1(case_0,[A,B],[1*A>=2],1,2)
sabu_memo_table_1(eval,[A,B],[1*A>=2],2,1)
sabu_memo_table_1(start,[A,B],[1*A>=2],0,0)
sabu_memo_table_1(start,[A,B],[],0,1)
:- dynamic sabu_memo_table_1/5.

sabu_memo_table_1(truncate, [_, _], [], 0, 0).
sabu_memo_table_1(case_0, [A, _], [1*A>=2], 1, 2).
sabu_memo_table_1(eval, [A, _], [1*A>=2], 2, 1).
sabu_memo_table_1(start, [_, _], [], 0, 1).


Size analysis performed in 3 ms.

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

Generated 33 equations 

Cost relation system solved by PUBS in 34 ms.

Method start terminates?: YES

UB for start(e) = pow(2,nat(e))


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

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

#### Obtained direct recursion through partial evaluation 
0. SCC is completely evaluated into other SCCs
1. SCC is partially evaluated into eval/1
3. SCC is partially evaluated into case_0/1

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

### Specialization of cost equations eval/1 
* CE 14 is refined into CE [15] 
* CE 12 is refined into CE [16] 
* CE 10 is refined into CE [17] 
* CE 8 is refined into CE [18] 
* CE 9 is refined into CE [19] 
* CE 13 is refined into CE [20] 
* CE 11 is refined into CE [21] 


#### Refined cost equations eval/1 
* CE 15: eval(A) = 5
     [A>=2] 
* CE 16: eval(A) = 5+ eval(B)+ eval(C)
     [A>=B+1,B>=2,A=C+1] 
* CE 17: eval(A) = 6+ eval(B)+ eval(C)
     [A>=B+1,B>=2,A=C+1] 
* CE 18: eval(A) = 9+ eval(B)+ eval(C)
     [C>=B,B>=2,C+1=A] 
* CE 19: eval(A) = 9+ eval(B)+ eval(C)
     [B>=C,C>=2,B+1=A] 
* CE 20: eval(A) = 5+ eval(B)+ eval(C)
     [B>=C,B>=2,B+1=A] 
* CE 21: eval(A) = 6+ eval(B)+ eval(C)
     [B>=C,B>=2,B+1=A] 

### Cost equations --> "Loop" of eval/1 
* CEs [17] --> Loop 15 
* CEs [16] --> Loop 16 
* CEs [18] --> Loop 17 
* CEs [19] --> Loop 18 
* CEs [21] --> Loop 19 
* CEs [20] --> Loop 20 
* CEs [15] --> Loop 21 

#### Loops of eval/1 
* Loop 15: eval(A)->  eval(A')  eval(A'2)
                  [A>=A'+1,A'>=2,A=A'2+1] 
* Loop 16: eval(A)->  eval(A')  eval(A'2)
                  [A>=A'+1,A'>=2,A=A'2+1] 
* Loop 17: eval(A)->  eval(A')  eval(A'2)
                  [A'2>=A',A'>=2,A'2+1=A] 
* Loop 18: eval(A)->  eval(A')  eval(A'2)
                  [A'>=A'2,A'2>=2,A'+1=A] 
* Loop 19: eval(A)->  eval(A')  eval(A'2)
                  [A'>=A'2,A'>=2,A'+1=A] 
* Loop 20: eval(A)->  eval(A')  eval(A'2)
                  [A'>=A'2,A'>=2,A'+1=A] 
* Loop 21: eval(A) [A>=2] 

### Ranking functions of CR eval(A) 
* RF of phase [15,16,17,18,19,20]: [A-2]

#### Partial ranking functions of CR eval(A) 
* Partial RF of phase [15,16,17,18,19,20]:
  - RF of loop [15:1,15:2,16:1,16:2,17:1,17:2,18:1,18:2,19:1,19:2,20:1,20:2]:
    A-2


### Resulting Chains:eval(A) 
* [21]
* [multiple([15,16,17,18,19,20],[[21]])]


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


#### Refined cost equations case_0/1 
* CE 22: case_0(A) = 4+ eval(B):[21]+ eval(C):[21]
     [B>=C,C>=2,B+1=A] 
* CE 23: case_0(A) = 4+ eval(B):[21]+ eval(C):[multiple([15,16,17,18,19,20],[[21]])]
     [B>=C,C>=3,B+1=A] 
* CE 24: case_0(A) = 4+ eval(B):[multiple([15,16,17,18,19,20],[[21]])]+ eval(C):[21]
     [B>=C,C>=2,B>=3,B+1=A] 
* CE 25: case_0(A) = 4+ eval(B):[multiple([15,16,17,18,19,20],[[21]])]+ eval(C):[multiple([15,16,17,18,19,20],[[21]])]
     [B>=C,C>=3,B+1=A] 
* CE 26: case_0(A) = 4+ eval(B):[21]+ eval(C):[21]
     [C>=B,B>=2,C+1=A] 
* CE 27: case_0(A) = 4+ eval(B):[21]+ eval(C):[multiple([15,16,17,18,19,20],[[21]])]
     [C>=B,C>=3,B>=2,C+1=A] 
* CE 28: case_0(A) = 4+ eval(B):[multiple([15,16,17,18,19,20],[[21]])]+ eval(C):[21]
     [C>=B,B>=3,C+1=A] 
* CE 29: case_0(A) = 4+ eval(B):[multiple([15,16,17,18,19,20],[[21]])]+ eval(C):[multiple([15,16,17,18,19,20],[[21]])]
     [C>=B,B>=3,C+1=A] 
* CE 30: case_0(A) = 5+ eval(B):[21]+ eval(C):[21]
     [B>=C,C>=2,B+1=A] 
* CE 31: case_0(A) = 5+ eval(B):[21]+ eval(C):[multiple([15,16,17,18,19,20],[[21]])]
     [B>=C,C>=3,B+1=A] 
* CE 32: case_0(A) = 5+ eval(B):[multiple([15,16,17,18,19,20],[[21]])]+ eval(C):[21]
     [B>=C,C>=2,B>=3,B+1=A] 
* CE 33: case_0(A) = 5+ eval(B):[multiple([15,16,17,18,19,20],[[21]])]+ eval(C):[multiple([15,16,17,18,19,20],[[21]])]
     [B>=C,C>=3,B+1=A] 
* CE 34: case_0(A) = 5+ eval(B):[21]+ eval(C):[21]
     [C>=B,B>=2,C+1=A] 
* CE 35: case_0(A) = 5+ eval(B):[21]+ eval(C):[multiple([15,16,17,18,19,20],[[21]])]
     [C>=B,C>=3,B>=2,C+1=A] 
* CE 36: case_0(A) = 5+ eval(B):[multiple([15,16,17,18,19,20],[[21]])]+ eval(C):[21]
     [C>=B,B>=3,C+1=A] 
* CE 37: case_0(A) = 5+ eval(B):[multiple([15,16,17,18,19,20],[[21]])]+ eval(C):[multiple([15,16,17,18,19,20],[[21]])]
     [C>=B,B>=3,C+1=A] 
* CE 38: case_0(A) = 8+ eval(B):[21]+ eval(C):[21]
     [B>=C,C>=2,B+1=A] 
* CE 39: case_0(A) = 8+ eval(B):[21]+ eval(C):[multiple([15,16,17,18,19,20],[[21]])]
     [B>=C,C>=3,B+1=A] 
* CE 40: case_0(A) = 8+ eval(B):[multiple([15,16,17,18,19,20],[[21]])]+ eval(C):[21]
     [B>=C,C>=2,B>=3,B+1=A] 
* CE 41: case_0(A) = 8+ eval(B):[multiple([15,16,17,18,19,20],[[21]])]+ eval(C):[multiple([15,16,17,18,19,20],[[21]])]
     [B>=C,C>=3,B+1=A] 
* CE 42: case_0(A) = 8+ eval(B):[21]+ eval(C):[21]
     [C>=B,B>=2,C+1=A] 
* CE 43: case_0(A) = 8+ eval(B):[21]+ eval(C):[multiple([15,16,17,18,19,20],[[21]])]
     [C>=B,C>=3,B>=2,C+1=A] 
* CE 44: case_0(A) = 8+ eval(B):[multiple([15,16,17,18,19,20],[[21]])]+ eval(C):[21]
     [C>=B,B>=3,C+1=A] 
* CE 45: case_0(A) = 8+ eval(B):[multiple([15,16,17,18,19,20],[[21]])]+ eval(C):[multiple([15,16,17,18,19,20],[[21]])]
     [C>=B,B>=3,C+1=A] 
* CE 46: case_0(A) = 4
     [A>=2] 

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

#### Loops of case_0/1 
* Loop 22: case_0(A) [A>=4] 
* Loop 23: case_0(A) [A>=4] 
* Loop 24: case_0(A) [A>=4] 
* Loop 25: case_0(A) [A>=4] 
* Loop 26: case_0(A) [A>=4] 
* Loop 27: case_0(A) [A>=4] 
* Loop 28: case_0(A) [A>=4] 
* Loop 29: case_0(A) [A>=4] 
* Loop 30: case_0(A) [A>=4] 
* Loop 31: case_0(A) [A>=4] 
* Loop 32: case_0(A) [A>=4] 
* Loop 33: case_0(A) [A>=4] 
* Loop 34: case_0(A) [A>=4] 
* Loop 35: case_0(A) [A>=4] 
* Loop 36: case_0(A) [A>=4] 
* Loop 37: case_0(A) [A>=4] 
* Loop 38: case_0(A) [A>=4] 
* Loop 39: case_0(A) [A>=4] 
* Loop 40: case_0(A) [A>=3] 
* Loop 41: case_0(A) [A>=3] 
* Loop 42: case_0(A) [A>=3] 
* Loop 43: case_0(A) [A>=3] 
* Loop 44: case_0(A) [A>=3] 
* Loop 45: case_0(A) [A>=3] 
* Loop 46: case_0(A) [A>=2] 

### Ranking functions of CR case_0(A) 

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


### Resulting Chains:case_0(A) 
* [46]
* [45]
* [44]
* [43]
* [42]
* [41]
* [40]
* [39]
* [38]
* [37]
* [36]
* [35]
* [34]
* [33]
* [32]
* [31]
* [30]
* [29]
* [28]
* [27]
* [26]
* [25]
* [24]
* [23]
* [22]


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

#### Cost of loops [15,16,17,18,19,20] 

 * loop 15:eval(A) -> [eval(A'),eval(A'2)] 
6
 * loop 16:eval(A) -> [eval(A'),eval(A'2)] 
5
 * loop 17:eval(A) -> [eval(A'),eval(A'2)] 
9
 * loop 18:eval(A) -> [eval(A'),eval(A'2)] 
9
 * loop 19:eval(A) -> [eval(A'),eval(A'2)] 
6
 * loop 20:eval(A) -> [eval(A'),eval(A'2)] 
5
#### Cost of phase [15,16,17,18,19,20]:eval(A) -> [] 
40*it(15)+5*it([21])+0
#### Cost of chains of eval(A):
* Chain [21]: 5
  with precondition: [A>=2] 

* Chain [multiple([15,16,17,18,19,20],[[21]])]: 40*it(15)+5*it([21])+0
  with precondition: [A>=3] 


#### Cost of chains of case_0(A):
* Chain [46]: 4
  with precondition: [A>=2] 

* Chain [45]: 14
  with precondition: [A>=3] 

* Chain [44]: 14
  with precondition: [A>=3] 

* Chain [43]: 15
  with precondition: [A>=3] 

* Chain [42]: 15
  with precondition: [A>=3] 

* Chain [41]: 18
  with precondition: [A>=3] 

* Chain [40]: 18
  with precondition: [A>=3] 

* Chain [39]: 45*s(1)+9
  with precondition: [A>=4] 

* Chain [38]: 45*s(3)+9
  with precondition: [A>=4] 

* Chain [37]: 90*s(5)+4
  with precondition: [A>=4] 

* Chain [36]: 45*s(9)+9
  with precondition: [A>=4] 

* Chain [35]: 45*s(11)+9
  with precondition: [A>=4] 

* Chain [34]: 90*s(13)+4
  with precondition: [A>=4] 

* Chain [33]: 45*s(17)+10
  with precondition: [A>=4] 

* Chain [32]: 45*s(19)+10
  with precondition: [A>=4] 

* Chain [31]: 90*s(21)+5
  with precondition: [A>=4] 

* Chain [30]: 45*s(25)+10
  with precondition: [A>=4] 

* Chain [29]: 45*s(27)+10
  with precondition: [A>=4] 

* Chain [28]: 90*s(29)+5
  with precondition: [A>=4] 

* Chain [27]: 45*s(33)+13
  with precondition: [A>=4] 

* Chain [26]: 45*s(35)+13
  with precondition: [A>=4] 

* Chain [25]: 90*s(37)+8
  with precondition: [A>=4] 

* Chain [24]: 45*s(41)+13
  with precondition: [A>=4] 

* Chain [23]: 45*s(43)+13
  with precondition: [A>=4] 

* Chain [22]: 90*s(45)+8
  with precondition: [A>=4] 


Closed-form bounds of case_0(A): 
-------------------------------------
* Chain [46] with precondition: [A>=2] 
    - Lower bound: 4 
    - Complexity: constant
 * Chain [45] with precondition: [A>=3] 
    - Lower bound: 14 
    - Complexity: constant
 * Chain [44] with precondition: [A>=3] 
    - Lower bound: 14 
    - Complexity: constant
 * Chain [43] with precondition: [A>=3] 
    - Lower bound: 15 
    - Complexity: constant
 * Chain [42] with precondition: [A>=3] 
    - Lower bound: 15 
    - Complexity: constant
 * Chain [41] with precondition: [A>=3] 
    - Lower bound: 18 
    - Complexity: constant
 * Chain [40] with precondition: [A>=3] 
    - Lower bound: 18 
    - Complexity: constant
 * Chain [39] with precondition: [A>=4] 
    - Lower bound: 9 
    - Complexity: constant
 * Chain [38] with precondition: [A>=4] 
    - Lower bound: 9 
    - Complexity: constant
 * Chain [37] with precondition: [A>=4] 
    - Lower bound: 4 
    - Complexity: constant
 * Chain [36] with precondition: [A>=4] 
    - Lower bound: 9 
    - Complexity: constant
 * Chain [35] with precondition: [A>=4] 
    - Lower bound: 9 
    - Complexity: constant
 * Chain [34] with precondition: [A>=4] 
    - Lower bound: 4 
    - Complexity: constant
 * Chain [33] with precondition: [A>=4] 
    - Lower bound: 10 
    - Complexity: constant
 * Chain [32] with precondition: [A>=4] 
    - Lower bound: 10 
    - Complexity: constant
 * Chain [31] with precondition: [A>=4] 
    - Lower bound: 5 
    - Complexity: constant
 * Chain [30] with precondition: [A>=4] 
    - Lower bound: 10 
    - Complexity: constant
 * Chain [29] with precondition: [A>=4] 
    - Lower bound: 10 
    - Complexity: constant
 * Chain [28] with precondition: [A>=4] 
    - Lower bound: 5 
    - Complexity: constant
 * Chain [27] with precondition: [A>=4] 
    - Lower bound: 13 
    - Complexity: constant
 * Chain [26] with precondition: [A>=4] 
    - Lower bound: 13 
    - Complexity: constant
 * Chain [25] with precondition: [A>=4] 
    - Lower bound: 8 
    - Complexity: constant
 * Chain [24] with precondition: [A>=4] 
    - Lower bound: 13 
    - Complexity: constant
 * Chain [23] with precondition: [A>=4] 
    - Lower bound: 13 
    - Complexity: constant
 * Chain [22] with precondition: [A>=4] 
    - Lower bound: 8 
    - Complexity: constant
 
### Partitioned lower bound of case_0(A): 
* 4 
 if [A>=2]
Possible lower bounds : [4]
Maximum lower bound complexity: constant
* Total analysis performed in 92 ms.