warning: Ignored call to loop_cont_f9/2 in equation f0/2 warning: Ignored call to f30/2 in equation f28/2 Warning: the following predicates are never called:[f2/2,f26/2,f28/2] Inferred cost of f20(A,B,C,D,E): f20(A,B,C,D,E):[14]: 1 with precondition: [C=0,E=B,A=D,2>=A] f20(A,B,C,D,E):[[13],14]: 1+it1*(1) Such that:it1=<1*A+ -2 with precondition: [C=0,D=2,B=E,A>=3] Inferred cost of f9(A,B,C,D,E): f9(A,B,C,D,E):[21]: 0 with precondition: [C=1,D=A,E=B] f9(A,B,C,D,E):[[16,17,18,19,20],21]: inf with precondition: [C=1,6>=D] f9(A,B,C,D,E):[[16,17,18,19,20],22]...: inf with precondition: [1>=C,C>=0] Inferred cost of f0(A,B): f0(A,B):[23]: 1 with precondition: [] f0(A,B):[24]: inf with precondition: [] f0(A,B):[25]...: inf with precondition: [] f0(A,B):[26]...: inf with precondition: [] Solved cost expressions of f0(A,B): f0(A,B):[23]: 1 with precondition: [] f0(A,B):[24]: inf with precondition: [] f0(A,B):[25]...: inf with precondition: [] f0(A,B):[26]...: inf with precondition: [] Maximum cost of f0(A,B): inf Asymptotic class: infinity Time statistics: Partial evaluation computed in 7 ms. Invariants computed in 19 ms. ----Backward Invariants 9 ms. ----Transitive Invariants 3 ms. Refinement performed in 22 ms. Termination proved in 9 ms. Upper bounds computed in 18 ms. ----Phase cost structures 8 ms. --------Equation cost structures 6 ms. --------Inductive compression(1) 2 ms. --------Inductive compression(2) 0 ms. --------Black Cost 0 ms. ----Chain cost structures 6 ms. ----Solving cost expressions 0 ms. Compressed phase information: 1 Compressed Chains: 0 Compressed invariants: 0 Total analysis performed in 89 ms.