warning: Ignored call to loop_cont_a/1 in equation start/1 warning: Ignored call to loop_cont_a/1 in equation start/1 warning: Ignored call to loop_cont_a/1 in equation start/1 Inferred cost of a(A,B,C): a(A,B,C):[14]: 0 with precondition: [B=1,A=C,A>=1] a(A,B,C):[[12,13],14]: 0+it1*(1) Such that:it1=<1*A+ -1,it1=<1*A+ -1*C with precondition: [B=1,A>=2,2*C>=1,A>=2*C] Inferred cost of start(A): start(A):[16]: 1 with precondition: [A>=1] start(A):[17]: 1+it1*(1) Such that:it1=<1*A+ -1,it1=<1*A+ -1/2 with precondition: [A>=2] start(A):[18]: 1 with precondition: [A>=2] start(A):[19]: 1+it1*(1) Such that:it1=<1*A+ -1,it1=<1*A+ -1/2 with precondition: [A>=2] start(A):[20]: 1 with precondition: [A>=4] start(A):[21]: 1+it1*(1) Such that:it1=<1*A+ -1,it1=<1*A+ -1/2 with precondition: [A>=4] Solved cost expressions of start(A): start(A):[16]: 1 with precondition: [A>=1] start(A):[17]: 1*A with precondition: [A>=2] start(A):[18]: 1 with precondition: [A>=2] start(A):[19]: 1*A with precondition: [A>=2] start(A):[20]: 1 with precondition: [A>=4] start(A):[21]: 1*A with precondition: [A>=4] Maximum cost of start(A): max([1*A,1]) Asymptotic class: n Time statistics: Partial evaluation computed in 3 ms. Invariants computed in 7 ms. ----Backward Invariants 3 ms. ----Transitive Invariants 1 ms. Refinement performed in 9 ms. Termination proved in 2 ms. Upper bounds computed in 14 ms. ----Phase cost structures 4 ms. --------Equation cost structures 3 ms. --------Inductive compression(1) 0 ms. --------Inductive compression(2) 0 ms. --------Black Cost 0 ms. ----Chain cost structures 4 ms. ----Solving cost expressions 1 ms. Compressed phase information: 0 Compressed Chains: 0 Compressed invariants: 0 Total analysis performed in 44 ms.