warning: Ignored call to loop_cont_f1/4 in equation f3/4 Inferred cost of f1(A,B,C,D,E,F,G,H,I): f1(A,B,C,D,E,F,G,H,I):[9]: 1 with precondition: [A=0,E=1,F=0,B=G,C=H,B>=C] f1(A,B,C,D,E,F,G,H,I):[10]: 1 with precondition: [A=0,E=1,F=1,C=B+1,C=G,C=H] f1(A,B,C,D,E,F,G,H,I):[[8],9]: 1+it1*(1) Such that:it1=<1*C+ -1*G,it1=<1*H+ -1*B,it1=<1*C+ -1*G+ -1/2,it1=<1*G+ -1*B+ -1/2 with precondition: [A=0,E=1,F=0,B+C=2*G,B+C=2*H,C>=B+2] f1(A,B,C,D,E,F,G,H,I):[[8],10]: 1+it1*(1) Such that:it1=<1*C+ -1*G,it1=<1*H+ -1*B+ -1 with precondition: [A=0,E=1,F=1,B+C+1=2*G,B+C+1=2*H,C>=B+3] Inferred cost of f3(A,B,C,D): f3(A,B,C,D):[12]: 2 with precondition: [B>=C] f3(A,B,C,D):[13]: 2 with precondition: [C=B+1] f3(A,B,C,D):[14]: 2+it1*(1) Such that:it1=<1/2*C+ -1/2*B,it1=<1/2*C+ -1/2*B+ -1/2 with precondition: [C>=B+2] f3(A,B,C,D):[15]: 2+it1*(1) Such that:it1=<1/2*C+ -1/2*B+ -1/2 with precondition: [C>=B+3] Solved cost expressions of f3(A,B,C,D): f3(A,B,C,D):[12]: 2 with precondition: [B>=C] f3(A,B,C,D):[13]: 2 with precondition: [C=B+1] f3(A,B,C,D):[14]: -1/2*B+1/2*C+3/2 with precondition: [C>=B+2] f3(A,B,C,D):[15]: -1/2*B+1/2*C+3/2 with precondition: [C>=B+3] Maximum cost of f3(A,B,C,D): max([-1/2*B+1/2*C+3/2,2]) Asymptotic class: n Time statistics: Partial evaluation computed in 3 ms. Invariants computed in 16 ms. ----Backward Invariants 8 ms. ----Transitive Invariants 2 ms. Refinement performed in 13 ms. Termination proved in 4 ms. Upper bounds computed in 24 ms. ----Phase cost structures 7 ms. --------Equation cost structures 5 ms. --------Inductive compression(1) 0 ms. --------Inductive compression(2) 0 ms. --------Black Cost 0 ms. ----Chain cost structures 13 ms. ----Solving cost expressions 1 ms. Compressed phase information: 2 Compressed Chains: 0 Compressed invariants: 0 Total analysis performed in 70 ms.