warning: Ignored call to loop_cont_f4/3 in equation f6/3 warning: Ignored call to f3/3 in equation f5/3 Warning: the following predicates are never called:[f0/7,f5/3,f5/7] Inferred cost of f3(A,B,C,D,E,F,G): f3(A,B,C,D,E,F,G):[16]: 2 with precondition: [A+1=0,C=0,D=1,E=0,G=1] f3(A,B,C,D,E,F,G):[18]: 1 with precondition: [A=0,C=0,D=1,E=0,G=0] f3(A,B,C,D,E,F,G):[[12],16]: 2+it1*(2) Such that:it1=<-1/2*A+ -1/2 with precondition: [C=0,D=1,E=0,G=1,0>=A+3] f3(A,B,C,D,E,F,G):[[12],18]: 1+it1*(2) Such that:it1=<-1/2*A,it1=<-1/2*A+ -1/2 with precondition: [C=0,D=1,E=0,G=0,0>=A+2] Inferred cost of f6(A,B,C): f6(A,B,C):[20]: 4 with precondition: [A=2] f6(A,B,C):[21]: 3 with precondition: [A=1] f6(A,B,C):[22]: 4+it1*(2) Such that:it1=<1/2*A+ -1 with precondition: [A>=4] f6(A,B,C):[23]: 3+it1*(2) Such that:it1=<1/2*A+ -1,it1=<1/2*A+ -1/2 with precondition: [A>=3] Solved cost expressions of f6(A,B,C): f6(A,B,C):[20]: 4 with precondition: [A=2] f6(A,B,C):[21]: 3 with precondition: [A=1] f6(A,B,C):[22]: 1*A+2 with precondition: [A>=4] f6(A,B,C):[23]: 1*A+1 with precondition: [A>=3] Maximum cost of f6(A,B,C): max([1*A+2,4]) Asymptotic class: n Time statistics: Partial evaluation computed in 13 ms. Invariants computed in 12 ms. ----Backward Invariants 7 ms. ----Transitive Invariants 1 ms. Refinement performed in 21 ms. Termination proved in 3 ms. Upper bounds computed in 14 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 8 ms. ----Solving cost expressions 0 ms. Compressed phase information: 3 Compressed Chains: 0 Compressed invariants: 0 Total analysis performed in 79 ms.