warning: Ignored call to loop_cont_f2/11 in equation f1/11 Inferred cost of f2(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W): f2(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W):[12]: 1 with precondition: [L=1,Q=E,R=F,K=H,J=I,A=M,B=N,K=T,J=U,J=V,K=W,A>=B] f2(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W):[[9,10,11],13]...: inf with precondition: [I=J,H=K,1>=L,L>=0,B>=A+1] Inferred cost of f1(A,B,C,D,E,F,G,H,I,J,K): f1(A,B,C,D,E,F,G,H,I,J,K):[14]: 2 with precondition: [A>=B] f1(A,B,C,D,E,F,G,H,I,J,K):[15]...: inf with precondition: [B>=A+1] f1(A,B,C,D,E,F,G,H,I,J,K):[16]...: inf with precondition: [B>=A+1] Solved cost expressions of f1(A,B,C,D,E,F,G,H,I,J,K): f1(A,B,C,D,E,F,G,H,I,J,K):[14]: 2 with precondition: [A>=B] f1(A,B,C,D,E,F,G,H,I,J,K):[15]...: inf with precondition: [B>=A+1] f1(A,B,C,D,E,F,G,H,I,J,K):[16]...: inf with precondition: [B>=A+1] Maximum cost of f1(A,B,C,D,E,F,G,H,I,J,K): inf Asymptotic class: infinity Time statistics: Partial evaluation computed in 11 ms. Invariants computed in 39 ms. ----Backward Invariants 14 ms. ----Transitive Invariants 8 ms. Refinement performed in 52 ms. Termination proved in 18 ms. Upper bounds computed in 15 ms. ----Phase cost structures 7 ms. --------Equation cost structures 7 ms. --------Inductive compression(1) 0 ms. --------Inductive compression(2) 0 ms. --------Black Cost 0 ms. ----Chain cost structures 6 ms. ----Solving cost expressions 0 ms. Compressed phase information: 0 Compressed Chains: 0 Compressed invariants: 0 Total analysis performed in 163 ms.