warning: Ignored call to stop/8 in equation start/8 warning: Ignored call to stop/8 in equation start/8 warning: Ignored call to stop/8 in equation start/8 warning: Ignored call to loop_cont_cut/8 in equation start/8 warning: Ignored call to loop_cont_cut/8 in equation start/8 Inferred cost of cut(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q): cut(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q):[23]: 1 with precondition: [A=2,D=2,G=1,I=1,J=2,M=2,N=0,P=0,K=B,L=C,O=F,Q=H,1>=E,E>=0] cut(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q):[24]: 1 with precondition: [A=2,D=2,E=0,G=1,I=1,J=2,K=0,M=2,N=1,P=0,L=C,O=F,Q=H] cut(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q):[25]: 1 with precondition: [A=2,D=2,E=1,G=1,I=1,J=2,K=1,M=2,N=0,P=0,L=C,O=F,Q=H] cut(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q):[[19,20,21],22]: 1+it1*(1) Such that:it1=<1*A+ -2,it1=<1*D+ -2,it1=<1*G+ -1,it1=<1*J+ -2,it1=<1*M+ -2,it1=<-1*E+1*A+ -1,it1=<-1*E+1*D+ -1,it1=<-1*E+1*J+ -1 with precondition: [I=1,P=0,A=D,A=J,C=L,A=M,F=O,H=Q,E>=0,G>=2,N>=1,A>=G+1,A>=E+G,G+N>=E,E+G>=N+2] cut(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q):[[19,20,21],23]: 1+it1*(1) Such that:it1=<1*A+ -2,it1=<1*D+ -2,it1=<1*G+ -1,it1=<1*J+ -2,it1=<1*M+ -2,it1=<-1*E+1*A+ -1,it1=<-1*E+1*D+ -1,it1=<-1*E+1*J+ -1 with precondition: [I=1,N=0,P=0,A=D,A=J,C=L,A=M,F=O,H=Q,E>=0,G>=2,G>=E,A>=G+1,A>=E+G] cut(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q):[[19,20,21],24]: 1+it1*(1) Such that:it1=<1*A+ -2,it1=<1*D+ -2,it1=<1*G+ -1,it1=<1*J+ -2,it1=<1*M+ -2,it1=<-1*E+1*A+ -1,it1=<-1*E+1*D+ -1,it1=<-1*E+1*J+ -1 with precondition: [I=1,P=0,A=D,A=J,N=K+1,C=L,A=M,F=O,H=Q,E>=0,G>=2,N>=1,A>=G+1,A>=E+G,G+N>=E+2,E+G>=N,2*A>=E+G+N+2] cut(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q):[[19,20,21],25]: 1+it1*(1) Such that:it1=<1*G+ -1,it1=<1*J+ -2,it1=<1*K+ -1,it1=<1*M+ -2,it1=<1*A+ -1*E+ -1,it1=<1*D+ -1*E+ -1,it1=<1*M+ -1*E+ -1 with precondition: [I=1,N=0,P=0,A=D,A=J,A=K+1,C=L,A=M,F=O,H=Q,A=E+G,G>=2,A>=G+1] Inferred cost of start(A,B,C,D,E,F,G,H): start(A,B,C,D,E,F,G,H):[27]: 1 with precondition: [D=A,C=B,F=E,H=G,0>=D] start(A,B,C,D,E,F,G,H):[28]: 1 with precondition: [A=1,D=1,C=B,F=E,H=G] start(A,B,C,D,E,F,G,H):[29]: 1 with precondition: [A=1,D=1,C=B,F=E,H=G] start(A,B,C,D,E,F,G,H):[30]: 2 with precondition: [A=2,D=2,C=B,F=E,H=G] start(A,B,C,D,E,F,G,H):[31]: 2 with precondition: [A=2,D=2,C=B,F=E,H=G] start(A,B,C,D,E,F,G,H):[32]: 2+it1*(1) Such that:it1=<1*A+ -2,it1=<1*A+ -1,it1=<1*D+ -2,it1=<1*D+ -1 with precondition: [D=A,C=B,F=E,H=G,D>=4] start(A,B,C,D,E,F,G,H):[33]: 2+it1*(1) Such that:it1=<1*A+ -2,it1=<1*A+ -1,it1=<1*D+ -2,it1=<1*D+ -1 with precondition: [D=A,C=B,F=E,H=G,D>=3] start(A,B,C,D,E,F,G,H):[34]: 2+it1*(1) Such that:it1=<1*A+ -2,it1=<1*A+ -1,it1=<1*D+ -2,it1=<1*D+ -1 with precondition: [D=A,C=B,F=E,H=G,D>=3] start(A,B,C,D,E,F,G,H):[35]: 2 with precondition: [A=2,D=2,C=B,F=E,H=G] start(A,B,C,D,E,F,G,H):[36]: 2 with precondition: [A=2,D=2,C=B,F=E,H=G] start(A,B,C,D,E,F,G,H):[37]: 2+it1*(1) Such that:it1=<1*A+ -2,it1=<1*D+ -2 with precondition: [D=A,C=B,F=E,H=G,D>=3] start(A,B,C,D,E,F,G,H):[38]: 2+it1*(1) Such that:it1=<1*A+ -2,it1=<1*D+ -2 with precondition: [D=A,C=B,F=E,H=G,D>=3] start(A,B,C,D,E,F,G,H):[39]: 2+it1*(1) Such that:it1=<1*A+ -2,it1=<1*D+ -2 with precondition: [D=A,C=B,F=E,H=G,D>=3] start(A,B,C,D,E,F,G,H):[40]: 2+it1*(1) Such that:it1=<1*A+ -2,it1=<1*D+ -2 with precondition: [D=A,C=B,F=E,H=G,D>=3] Inferred cost of start0(A,B,C,D,E,F,G,H): start0(A,B,C,D,E,F,G,H):[42]: 2 with precondition: [0>=A] start0(A,B,C,D,E,F,G,H):[43]: 2 with precondition: [A=1] start0(A,B,C,D,E,F,G,H):[44]: 2 with precondition: [A=1] start0(A,B,C,D,E,F,G,H):[45]: 3 with precondition: [A=2] start0(A,B,C,D,E,F,G,H):[46]: 3 with precondition: [A=2] start0(A,B,C,D,E,F,G,H):[47]: 3+it1*(1) Such that:it1=<1*A+ -2,it1=<1*A+ -1 with precondition: [A>=4] start0(A,B,C,D,E,F,G,H):[48]: 3+it1*(1) Such that:it1=<1*A+ -2,it1=<1*A+ -1 with precondition: [A>=3] start0(A,B,C,D,E,F,G,H):[49]: 3+it1*(1) Such that:it1=<1*A+ -2,it1=<1*A+ -1 with precondition: [A>=3] start0(A,B,C,D,E,F,G,H):[50]: 3 with precondition: [A=2] start0(A,B,C,D,E,F,G,H):[51]: 3 with precondition: [A=2] start0(A,B,C,D,E,F,G,H):[52]: 3+it1*(1) Such that:it1=<1*A+ -2 with precondition: [A>=3] start0(A,B,C,D,E,F,G,H):[53]: 3+it1*(1) Such that:it1=<1*A+ -2 with precondition: [A>=3] start0(A,B,C,D,E,F,G,H):[54]: 3+it1*(1) Such that:it1=<1*A+ -2 with precondition: [A>=3] start0(A,B,C,D,E,F,G,H):[55]: 3+it1*(1) Such that:it1=<1*A+ -2 with precondition: [A>=3] Solved cost expressions of start0(A,B,C,D,E,F,G,H): start0(A,B,C,D,E,F,G,H):[42]: 2 with precondition: [0>=A] start0(A,B,C,D,E,F,G,H):[43]: 2 with precondition: [A=1] start0(A,B,C,D,E,F,G,H):[44]: 2 with precondition: [A=1] start0(A,B,C,D,E,F,G,H):[45]: 3 with precondition: [A=2] start0(A,B,C,D,E,F,G,H):[46]: 3 with precondition: [A=2] start0(A,B,C,D,E,F,G,H):[47]: 1*A+1 with precondition: [A>=4] start0(A,B,C,D,E,F,G,H):[48]: 1*A+1 with precondition: [A>=3] start0(A,B,C,D,E,F,G,H):[49]: 1*A+1 with precondition: [A>=3] start0(A,B,C,D,E,F,G,H):[50]: 3 with precondition: [A=2] start0(A,B,C,D,E,F,G,H):[51]: 3 with precondition: [A=2] start0(A,B,C,D,E,F,G,H):[52]: 1*A+1 with precondition: [A>=3] start0(A,B,C,D,E,F,G,H):[53]: 1*A+1 with precondition: [A>=3] start0(A,B,C,D,E,F,G,H):[54]: 1*A+1 with precondition: [A>=3] start0(A,B,C,D,E,F,G,H):[55]: 1*A+1 with precondition: [A>=3] Maximum cost of start0(A,B,C,D,E,F,G,H): max([1*A+1,3]) Asymptotic class: n Time statistics: Partial evaluation computed in 17 ms. Invariants computed in 104 ms. ----Backward Invariants 67 ms. ----Transitive Invariants 9 ms. Refinement performed in 109 ms. Termination proved in 26 ms. Upper bounds computed in 147 ms. ----Phase cost structures 74 ms. --------Equation cost structures 72 ms. --------Inductive compression(1) 0 ms. --------Inductive compression(2) 0 ms. --------Black Cost 0 ms. ----Chain cost structures 61 ms. ----Solving cost expressions 2 ms. Compressed phase information: 3 Compressed Chains: 0 Compressed invariants: 0 Total analysis performed in 452 ms.