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 1 ms.
sabu_memo_table_1(case_0,[A,B,C],[1*C=1,1*B=1],0,0)
sabu_memo_table_1(case_1,[A,B,C,D,E],[1*E=1,1*A=1],0,0)
sabu_memo_table_1(take_l,[A,B,C],[1*B=1,1*C=1],0,0)
sabu_memo_table_1(case_0,[A,B,C],[1*B>=1,1*C=1],1,1)
sabu_memo_table_1(case_1,[A,B,C,D,E],[1*E>=1,1*A>=1],1,1)
sabu_memo_table_1(case_0,[A,B,C],[1*B>=1,1*C>=1],2,2)
sabu_memo_table_1(take_l,[A,B,C],[1*C>=1,1*B>=1],3,1)
sabu_memo_table_1(start,[A,B],[],0,0)
:- dynamic sabu_memo_table_1/5.

sabu_memo_table_1(case_1, [B, _, _, _, A], [1*A>=1, 1*B>=1], 1, 1).
sabu_memo_table_1(case_0, [_, A, B], [1*A>=1, 1*B>=1], 2, 2).
sabu_memo_table_1(take_l, [_, B, A], [1*A>=1, 1*B>=1], 3, 1).
sabu_memo_table_1(start, [_, _], [], 0, 0).


Size analysis performed in 2 ms.

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

Generated 31 equations 

Cost relation system solved by PUBS in 14 ms.

Method start terminates?: UNKOWN

UB for start(n) = c(maximize_failed)+c(failed(no_rf,[scc=1,cr=zeros/0]))


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

#### Computed strongly connected components 
0. recursive  : [case_0/2,case_1/4,take_l/2]
1. recursive  : [zeros/0]
2. non_recursive  : [start/1]
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 partially evaluated into take_l/2
1. SCC is partially evaluated into zeros/0
2. SCC is partially evaluated into start/1

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

### Specialization of cost equations take_l/2 
* CE 4 is refined into CE [7] 
* CE 6 is refined into CE [8] 
* CE 5 is refined into CE [9] 


#### Refined cost equations take_l/2 
* CE 7: take_l(A,B) = 3
     [B=1] 
* CE 8: take_l(A,B) = 6
     [B>=2,A=1] 
* CE 9: take_l(A,B) = 8+ take_l(C,D)
     [B>=D+1,B>=2,A>=2,A=C+1] 

### Cost equations --> "Loop" of take_l/2 
* CEs [9] --> Loop 7 
* CEs [7] --> Loop 8 
* CEs [8] --> Loop 9 

#### Loops of take_l/2 
* Loop 7: take_l(A,B)->  take_l(A',B')
                  [B>=B'+1,B>=2,A>=2,A=A'+1] 
* Loop 8: take_l(A,B) [B=1] 
* Loop 9: take_l(A,B) [B>=2,A=1] 

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

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


### Resulting Chains:take_l(A,B) 
* [[7],9]
* [[7],8]
* [9]
* [8]


### Specialization of cost equations zeros/0 
* CE 3 is refined into CE [10] 


#### Refined cost equations zeros/0 
* CE 10: zeros = 3+ zeros
     [] 

### Cost equations --> "Loop" of zeros/0 
* CEs [10] --> Loop 10 

#### Loops of zeros/0 
* Loop 10: zeros->  zeros
                  [] 

### Ranking functions of CR zeros 

#### Partial ranking functions of CR zeros 

Warning: no base case found for predicate

### Resulting Chains:zeros 
* [[10]]...


### Specialization of cost equations start/1 
* CE 2 is refined into CE [11] 
* CE 1 is refined into CE [12,13,14,15] 


#### Refined cost equations start/1 
* CE 11: start(A) = 1
     [] 
* CE 12: start(A) = 2+ zeros:[[10]]+ take_l(A,B):[[7],9]
     [B>=A+1,A>=2] 
* CE 13: start(A) = 2+ zeros:[[10]]+ take_l(A,B):[[7],8]
     [B>=2,A>=2] 
* CE 14: start(A) = 2+ zeros:[[10]]+ take_l(B,C):[9]
     [C>=2,B=1,A=1] 
* CE 15: start(A) = 2+ zeros:[[10]]+ take_l(A,B):[8]
     [B=1] 

### Cost equations --> "Loop" of start/1 
* CEs [13] --> Loop 11 
* CEs [12] --> Loop 12 
* CEs [14] --> Loop 13 
* CEs [15] --> Loop 14 
* CEs [11] --> Loop 15 

#### Loops of start/1 
* Loop 11: start(A) [A>=2] 
* Loop 12: start(A) [A>=2] 
* Loop 13: start(A) [A=1] 
* Loop 14: start(A) [] 
* Loop 15: start(A) [] 

### Ranking functions of CR start(A) 

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


### Resulting Chains:start(A) 
* [15]
* [14]...
* [13]...
* [12]...
* [11]...


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

#### Cost of loops [7] 

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

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

#### Cost of chains of take_l(A,B):
* Chain [[7],9]: 8*it(7)+6
  Such that:it(7) =< A-1
it(7) >= A-1

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

* Chain [[7],8]: 8*it(7)+3
  Such that:it(7) =< B-1
it(7) >= 1

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

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

* Chain [8]: 3
  with precondition: [B=1] 


#### Cost of loops [10] 

 * loop 10:zeros -> [zeros] 
3
#### Cost of phase [10]:zeros -> [zeros] 
3*it(10)+0
#### Cost of chains of zeros:
* Chain [[10]]...: 3*it(10)+0
  with precondition: [] 


#### Cost of chains of start(A):
* Chain [15]: 1
  with precondition: [] 

* Chain [14]...: 3*s(1)+5
  with precondition: [] 

* Chain [13]...: 3*s(2)+8
  with precondition: [A=1] 

* Chain [12]...: 3*s(3)+8*s(4)+8
  Such that:s(4) =< A-1
s(4) >= A-1

  with precondition: [A>=2] 

* Chain [11]...: 3*s(5)+8*s(6)+5
  Such that:s(6) >= 1

  with precondition: [A>=2] 


Closed-form bounds of start(A): 
-------------------------------------
* Chain [15] with precondition: [] 
    - Lower bound: 1 
    - Complexity: constant
 * Chain [14]... with precondition: [] 
    - Lower bound: 5 
    - Complexity: constant
 * Chain [13]... with precondition: [A=1] 
    - Lower bound: 8 
    - Complexity: constant
 * Chain [12]... with precondition: [A>=2] 
    - Lower bound: 8*A 
    - Complexity: n
 * Chain [11]... with precondition: [A>=2] 
    - Lower bound: 13 
    - Complexity: constant
 
### Partitioned lower bound of start(A): 
* 1 
 if []
Possible lower bounds : [1]
Maximum lower bound complexity: constant
* Total analysis performed in 33 ms.