warning: Ignored call to loop_cont_f300/4 in equation f2/4 Inferred cost of f300(A,B,C,D,E,F,G,H,I): f300(A,B,C,D,E,F,G,H,I):[12]: 1 with precondition: [E=1,H=C,A=F,B=G,A>=B] f300(A,B,C,D,E,F,G,H,I):[[9,10,11],12]: 1+it1*(1) Such that:it1=<1*B+ -1*A with precondition: [E=1,F=G,B>=A+1,F>=A,B>=F] Inferred cost of f2(A,B,C,D): f2(A,B,C,D):[14]: 2 with precondition: [A>=B] f2(A,B,C,D):[15]: 2+it1*(1) Such that:it1=<1*B+ -1*A with precondition: [B>=A+1] Solved cost expressions of f2(A,B,C,D): f2(A,B,C,D):[14]: 2 with precondition: [A>=B] f2(A,B,C,D):[15]: -1*A+1*B+2 with precondition: [B>=A+1] Maximum cost of f2(A,B,C,D): max([-1*A+1*B+2,2]) Asymptotic class: n Time statistics: Partial evaluation computed in 5 ms. Invariants computed in 15 ms. ----Backward Invariants 6 ms. ----Transitive Invariants 3 ms. Refinement performed in 19 ms. Termination proved in 7 ms. Upper bounds computed in 13 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 6 ms. ----Solving cost expressions 1 ms. Compressed phase information: 0 Compressed Chains: 0 Compressed invariants: 0 Total analysis performed in 71 ms.