WARNING: Excluded non-linear constraints:[E=A*D] warning: Ignored call to loop_cont_a/1 in equation start/1 warning: Ignored call to loop_cont_a/1 in equation start/1 warning: Ignored call to loop_cont_a/1 in equation start/1 Inferred cost of a(A,B,C): a(A,B,C):[10]: 0 with precondition: [B=1,A=C,A>=1] Inferred cost of start(A): start(A):[12]: 1 with precondition: [A>=1] start(A):[13]: 1 with precondition: [A>=2] start(A):[14]: 1 with precondition: [A>=4] Solved cost expressions of start(A): start(A):[12]: 1 with precondition: [A>=1] start(A):[13]: 1 with precondition: [A>=2] start(A):[14]: 1 with precondition: [A>=4] Maximum cost of start(A): 1 Asymptotic class: constant Time statistics: Partial evaluation computed in 2 ms. Invariants computed in 0 ms. ----Backward Invariants 0 ms. ----Transitive Invariants 0 ms. Refinement performed in 4 ms. Termination proved in 1 ms. Upper bounds computed in 3 ms. ----Phase cost structures 2 ms. --------Equation cost structures 2 ms. --------Inductive compression(1) 0 ms. --------Inductive compression(2) 0 ms. --------Black Cost 0 ms. ----Chain cost structures 0 ms. ----Solving cost expressions 0 ms. Compressed phase information: 0 Compressed Chains: 0 Compressed invariants: 0 Total analysis performed in 15 ms.