warning: Ignored call to stop/14 in equation start/14 warning: Ignored call to loop_cont_lbl53/14 in equation start/14 warning: Ignored call to loop_cont_lbl53/14 in equation start/14 Inferred cost of lbl53(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1): lbl53(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1):[19]: 3 with precondition: [A=2,D=1,J=2,L=0,N=2,O=1,P=2,Q=0,S=1,Y=2,A1=1,C1=2,C=B,T=E,G=F,X=I,Z=K,B1=M,C=R,G=V,H=W,1>=H,H>=0] Inferred cost of start(A,B,C,D,E,F,G,H,I,J,K,L,M,N): start(A,B,C,D,E,F,G,H,I,J,K,L,M,N):[21]: 1 with precondition: [N=A,C=B,E=D,G=F,I=H,K=J,M=L,1>=N] start(A,B,C,D,E,F,G,H,I,J,K,L,M,N):[22]: 4 with precondition: [A=2,N=2,C=B,E=D,G=F,I=H,K=J,M=L] start(A,B,C,D,E,F,G,H,I,J,K,L,M,N):[23]: 4 with precondition: [A=2,N=2,C=B,E=D,G=F,I=H,K=J,M=L] Inferred cost of start0(A,B,C,D,E,F,G,H,I,J,K,L,M,N): start0(A,B,C,D,E,F,G,H,I,J,K,L,M,N):[25]: 2 with precondition: [1>=A] start0(A,B,C,D,E,F,G,H,I,J,K,L,M,N):[26]: 5 with precondition: [A=2] start0(A,B,C,D,E,F,G,H,I,J,K,L,M,N):[27]: 5 with precondition: [A=2] Solved cost expressions of start0(A,B,C,D,E,F,G,H,I,J,K,L,M,N): start0(A,B,C,D,E,F,G,H,I,J,K,L,M,N):[25]: 2 with precondition: [1>=A] start0(A,B,C,D,E,F,G,H,I,J,K,L,M,N):[26]: 5 with precondition: [A=2] start0(A,B,C,D,E,F,G,H,I,J,K,L,M,N):[27]: 5 with precondition: [A=2] Maximum cost of start0(A,B,C,D,E,F,G,H,I,J,K,L,M,N): 5 Asymptotic class: constant Time statistics: Partial evaluation computed in 48 ms. Invariants computed in 7 ms. ----Backward Invariants 5 ms. ----Transitive Invariants 0 ms. Refinement performed in 92 ms. Termination proved in 0 ms. Upper bounds computed in 11 ms. ----Phase cost structures 8 ms. --------Equation cost structures 8 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 221 ms.