warning: Ignored call to loop_cont_l1/4 in equation l0/4 Inferred cost of l2(A,B,C,D,E,F,G,H,I): l2(A,B,C,D,E,F,G,H,I):[[11],12]: 1+it1*(1) Such that:it1=<1*B+ -1*C,it1=<1*H+ -1*C with precondition: [E=0,B=G+1,B=H,A+I=F,B>=C+1] Inferred cost of l1(A,B,C,D,E,F,G,H,I): l1(A,B,C,D,E,F,G,H,I):[15]: 0 with precondition: [A=0,E=1,F=0,G=B,H=C,I=D] l1(A,B,C,D,E,F,G,H,I):[[14],15]: 0+it1*(2+it2*(1)) Such that:it1=<1*B,it1=<1*B+ -1*G it2=<1*B with precondition: [E=1,G+1=H,G>=0,B>=G+1] Inferred cost of l0(A,B,C,D): l0(A,B,C,D):[17]: 1 with precondition: [] l0(A,B,C,D):[18]: 1+it1*(2+it2*(1)) Such that:it1=<1*B it2=<1*B with precondition: [B>=1] Solved cost expressions of l0(A,B,C,D): l0(A,B,C,D):[17]: 1 with precondition: [] l0(A,B,C,D):[18]: (1*B+2)* (1*B)+1 with precondition: [B>=1] Maximum cost of l0(A,B,C,D): max([1, (1*B+2)* (1*B)+1]) Asymptotic class: n^2 Time statistics: Partial evaluation computed in 7 ms. Invariants computed in 20 ms. ----Backward Invariants 7 ms. ----Transitive Invariants 4 ms. Refinement performed in 17 ms. Termination proved in 6 ms. Upper bounds computed in 23 ms. ----Phase cost structures 9 ms. --------Equation cost structures 6 ms. --------Inductive compression(1) 0 ms. --------Inductive compression(2) 0 ms. --------Black Cost 0 ms. ----Chain cost structures 10 ms. ----Solving cost expressions 1 ms. Compressed phase information: 0 Compressed Chains: 0 Compressed invariants: 0 Total analysis performed in 89 ms.