warning: Ignored call to loop_cont_f2/3 in equation f1/3 Inferred cost of f2(A,B,C,D,E,F,G): f2(A,B,C,D,E,F,G):[14]: 0 with precondition: [D=1,B+1=C,A=E,B=F,B+1=G,B>=1,A>=B] f2(A,B,C,D,E,F,G):[[13],12,[11],14]: 2+it1*(2)+it2*(2) Such that:it1=<1*A,it1=<1*B,it1=<1*E,it1=<1*F,it1=<1*G,it1=<1*A+ -1,it1=<1*C+ -1,it1=<1*E+ -1,it2=<-1*B+1*E,it2=<-1*F+1*E,it2=<1*A+ -1*C+1,it2=<1*E+ -1*C+1 with precondition: [D=1,A=E,B=F,G>=1,C>=B+1,A>=C,B>=G] f2(A,B,C,D,E,F,G):[[13],12,14]: 2+it1*(2) Such that:it1=<-1*B+1*E,it1=<-1*F+1*E,it1=<1*A+ -1*C+1,it1=<1*E+ -1*C+1 with precondition: [D=1,G=0,A=E,B=F,B>=1,C>=B+1,A>=C] f2(A,B,C,D,E,F,G):[[13],14]: 0+it1*(2) Such that:it1=<-1*B+1*E,it1=<-1*F+1*E,it1=<1*A+ -1,it1=<1*E+ -1,it1=<1*G+ -2,it1=<1*G+ -1*C,it1=<-1*B+1*G+ -1,it1=<-1*F+1*G+ -1,it1=<1*A+ -1*C+1,it1=<1*E+ -1*C+1 with precondition: [D=1,A=E,B=F,B>=1,C>=B+1,G>=C+1,A+1>=G] f2(A,B,C,D,E,F,G):[12,[11],14]: 2+it1*(2) Such that:it1=<1*A,it1=<1*B,it1=<1*E,it1=<1*F,it1=<1*G,it1=<1*C+ -1 with precondition: [D=1,A=B,A+1=C,A=E,A=F,G>=1,A>=G] f2(A,B,C,D,E,F,G):[12,14]: 2 with precondition: [D=1,G=0,A=B,A+1=C,A=E,A=F,A>=1] Inferred cost of f1(A,B,C): f1(A,B,C):[16]: 1 with precondition: [B>=1,A>=B] f1(A,B,C):[17]: 3+it1*(2)+it2*(2) Such that:it1=<1*A,it1=<1*B,it1=<1*A+ -1,it2=<1*A+ -1*B with precondition: [B>=1,A>=B+1] f1(A,B,C):[18]: 3+it1*(2) Such that:it1=<1*A+ -1*B with precondition: [B>=1,A>=B+1] f1(A,B,C):[19]: 1+it1*(2) Such that:it1=<-1*B+1*A,it1=<1*A+ -1,it1=<1*A+ -1*B with precondition: [B>=1,A>=B+1] f1(A,B,C):[20]: 3+it1*(2) Such that:it1=<1*A,it1=<1*B with precondition: [A=B,A>=1] f1(A,B,C):[21]: 3 with precondition: [A=B,A>=1] Solved cost expressions of f1(A,B,C): f1(A,B,C):[16]: 1 with precondition: [B>=1,A>=B] f1(A,B,C):[17]: 2*A+3 with precondition: [B>=1,A>=B+1] f1(A,B,C):[18]: 2*A+ -2*B+3 with precondition: [B>=1,A>=B+1] f1(A,B,C):[19]: 2*A+ -2*B+1 with precondition: [B>=1,A>=B+1] f1(A,B,C):[20]: 2*A+3 with precondition: [A=B,A>=1] f1(A,B,C):[21]: 3 with precondition: [A=B,A>=1] Maximum cost of f1(A,B,C): max([2*A+ -2*B+3,2*A+3,3]) Asymptotic class: n Time statistics: Partial evaluation computed in 9 ms. Invariants computed in 56 ms. ----Backward Invariants 28 ms. ----Transitive Invariants 3 ms. Refinement performed in 29 ms. Termination proved in 7 ms. Upper bounds computed in 161 ms. ----Phase cost structures 27 ms. --------Equation cost structures 26 ms. --------Inductive compression(1) 0 ms. --------Inductive compression(2) 0 ms. --------Black Cost 0 ms. ----Chain cost structures 127 ms. ----Solving cost expressions 2 ms. Compressed phase information: 4 Compressed Chains: 0 Compressed invariants: 0 Total analysis performed in 283 ms.