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