warning: Ignored call to loop_cont_eval/2 in equation start/2 Inferred cost of eval(A,B,C,D,E): eval(A,B,C,D,E):[10]: 0 with precondition: [C=1,D=A,E=B] eval(A,B,C,D,E):[[8],[9],10]: 0+it1*(1)+it2*(1) Such that:it1=<1*B,it1=<1*B+ -1*E,it2=<1*A,it2=<1*A+1*B with precondition: [C=1,D=0,A>=1,E>=0,B>=E+1] eval(A,B,C,D,E):[[8],10]: 0+it1*(1) Such that:it1=<1*A,it1=<1*A+ -1*D,it1=<1*A+1*B with precondition: [C=1,B=E,D>=0,A>=D+1,B+D>=0] eval(A,B,C,D,E):[[9],10]: 0+it1*(1) Such that:it1=<1*B,it1=<1*A+1*B,it1=<1*B+ -1*E,it1=<1*B+1*D with precondition: [C=1,A=D,0>=A,B>=E+1,A+E>=0] Inferred cost of start(A,B): start(A,B):[12]: 1 with precondition: [] start(A,B):[13]: 1+it1*(1)+it2*(1) Such that:it1=<1*B,it2=<1*A,it2=<1*A+1*B with precondition: [A>=1,B>=1] start(A,B):[14]: 1+it1*(1) Such that:it1=<1*A,it1=<1*A+1*B with precondition: [A>=1,A+B>=1] start(A,B):[15]: 1+it1*(1) Such that:it1=<1*B,it1=<1*A+1*B with precondition: [0>=A,A+B>=1] Solved cost expressions of start(A,B): start(A,B):[12]: 1 with precondition: [] start(A,B):[13]: 1*A+1*B+1 with precondition: [A>=1,B>=1] start(A,B):[14]: nat(min([1*A+1*B,1*A]))+1 with precondition: [A>=1,A+B>=1] start(A,B):[15]: 1*A+1*B+1 with precondition: [0>=A,A+B>=1] Maximum cost of start(A,B): max([1*A+1*B+1,1,nat(min([1*A+1*B,1*A]))+1]) Asymptotic class: n Time statistics: Partial evaluation computed in 3 ms. Invariants computed in 20 ms. ----Backward Invariants 10 ms. ----Transitive Invariants 2 ms. Refinement performed in 11 ms. Termination proved in 4 ms. Upper bounds computed in 46 ms. ----Phase cost structures 8 ms. --------Equation cost structures 6 ms. --------Inductive compression(1) 0 ms. --------Inductive compression(2) 0 ms. --------Black Cost 0 ms. ----Chain cost structures 32 ms. ----Solving cost expressions 2 ms. Compressed phase information: 2 Compressed Chains: 0 Compressed invariants: 0 Total analysis performed in 96 ms.