warning: Ignored call to evalrealshellsortstop/5 in equation evalrealshellsortreturnin/5 Inferred cost of evalrealshellsortbb3in(A,B,C,D,E,F,G,H,I,J,K): evalrealshellsortbb3in(A,B,C,D,E,F,G,H,I,J,K):[30]: 2 with precondition: [F=0,J=D,C=E,A=G,B=H,C=I,C=K,C>=B,A>=C+1] evalrealshellsortbb3in(A,B,C,D,E,F,G,H,I,J,K):[31]: 1 with precondition: [F=1,J=D,C=E,A=G,B=H,C=I,C=K,C>=B,A>=C+1] evalrealshellsortbb3in(A,B,C,D,E,F,G,H,I,J,K):[32]: 1 with precondition: [F=0,J=D,C=E,A=G,B=H,C=I,C=K,A>=C+1,B>=C+1] evalrealshellsortbb3in(A,B,C,D,E,F,G,H,I,J,K):[[29],30]: inf with precondition: [F=0,A=G,B=H,C=I,D=J,E>=B,K>=B,A>=C+1] evalrealshellsortbb3in(A,B,C,D,E,F,G,H,I,J,K):[[29],31]: inf with precondition: [F=1,A=G,B=H,C=I,D=J,E>=B,K>=B,A>=C+1] evalrealshellsortbb3in(A,B,C,D,E,F,G,H,I,J,K):[[29],32]: inf with precondition: [F=0,A=G,B=H,C=I,D=J,K>=0,A>=C+1,B>=K+1,E>=B+K] evalrealshellsortbb3in(A,B,C,D,E,F,G,H,I,J,K):[[29],33]...: inf with precondition: [1>=F,F>=0,E>=B,A>=C+1] Inferred cost of evalrealshellsortbb6in(A,B,C,D,E,F,G,H,I,J,K): evalrealshellsortbb6in(A,B,C,D,E,F,G,H,I,J,K):[40]: 1 with precondition: [C=0,F=0,I=0,J=D,K=E,A=G,B=H,0>=A,B>=1] evalrealshellsortbb6in(A,B,C,D,E,F,G,H,I,J,K):[[35],[34,36,37],38]: 3+it1*(5)+it2*(inf)+it3*(4) Such that:it1+it2=<1*A+ -1*B,it1+it2=<1*A+ -1*B+ -1,it3=<1*A+ -1*C,it3=<1*B+ -1*C,it3=<-1*C+1*A+ -2 with precondition: [F=1,C>=0,A>=B+2,B>=C+1] evalrealshellsortbb6in(A,B,C,D,E,F,G,H,I,J,K):[[35],[34,36,37],39]: inf with precondition: [F=1,C>=0,A>=B+2,B>=C+1] evalrealshellsortbb6in(A,B,C,D,E,F,G,H,I,J,K):[[35],[34,36,37],40]: 1+it1*(5)+it2*(inf)+it3*(4) Such that:it1+it2=<1*A+ -1,it1+it2=<1*A+ -1*B,it1+it2=<1*G+ -1,it1+it2=<1*G+ -1*H,it1+it2=<1*I+ -1,it1+it2=<1*I+ -1*B,it1+it2=<1*I+ -1*H,it1+it2=<-1*C+1*I+ -1,it3=<1*G,it3=<1*H,it3=<1*I,it3=<1*A+ -1,it3=<1*A+ -1*C,it3=<1*B+ -1*C,it3=<1*G+ -1,it3=<1*H+ -1*C,it3=<1*I+ -1,it3=<1*I+ -1*C with precondition: [F=0,A=G,B=H,A=I,C>=0,K>=0,A>=B+1,B>=C+1] evalrealshellsortbb6in(A,B,C,D,E,F,G,H,I,J,K):[[35],[34,36,37],41]...: inf with precondition: [1>=F,C>=0,F>=0,A>=B+2,B>=C+1] evalrealshellsortbb6in(A,B,C,D,E,F,G,H,I,J,K):[[35],[34,36,37],42]...: inf with precondition: [F=1,C>=0,A>=B+2,B>=C+1] evalrealshellsortbb6in(A,B,C,D,E,F,G,H,I,J,K):[[35],38]: 3+it1*(4) Such that:it1=<1*A+ -1*C,it1=<1*B+ -1*C,it1=<-1*C+1*A+ -1 with precondition: [F=1,C>=0,A>=B+1,B>=C+1] evalrealshellsortbb6in(A,B,C,D,E,F,G,H,I,J,K):[[35],39]: inf with precondition: [F=1,C>=0,A>=B+1,B>=C+1] evalrealshellsortbb6in(A,B,C,D,E,F,G,H,I,J,K):[[35],40]: 1+it1*(4) Such that:it1=<1*B,it1=<1*G,it1=<1*H,it1=<1*I,it1=<1*A+ -1*C,it1=<1*H+ -1*C,it1=<1*K+1,it1=<1*K+ -1*C+1 with precondition: [F=0,A=G,B=H,A=I,A=K+1,C>=0,B>=A,A>=C+1] evalrealshellsortbb6in(A,B,C,D,E,F,G,H,I,J,K):[[35],41]...: inf with precondition: [1>=F,C>=0,F>=0,A>=B+1,B>=C+1] evalrealshellsortbb6in(A,B,C,D,E,F,G,H,I,J,K):[[35],42]...: inf with precondition: [F=1,C>=0,A>=B+1,B>=C+1] Inferred cost of evalrealshellsortbb8in(A,B,C,D,E,F,G,H,I,J,K): evalrealshellsortbb8in(A,B,C,D,E,F,G,H,I,J,K):[47]: 4+it1*(5)+it2*(inf)+it3*(4) Such that:it1+it2=<1*B,it1+it2=<1*A+ -1*B,it1+it2=<1*B+1,it1+it2=<1*A+ -1*B+ -1,it3=<1*A,it3=<1*B,it3=<1*A+ -2,it3=<2*B+ -1,it3=<2*B+1,it3=<1/2*A+1/2 with precondition: [F=1,A+1>=2*B,2*B+1>=A,A>=B+2] evalrealshellsortbb8in(A,B,C,D,E,F,G,H,I,J,K):[48]: inf with precondition: [F=1,A+1>=2*B,2*B+1>=A,A>=B+2] evalrealshellsortbb8in(A,B,C,D,E,F,G,H,I,J,K):[49]: 4+it1*(4) Such that:it1=<1*A,it1=<1*B,it1=<2*B,it1=<1*A+ -1,it1=<2*B+1,it1=<1/2*A+1/2 with precondition: [F=1,B>=1,A+1>=2*B,2*B+1>=A,A>=B+1] evalrealshellsortbb8in(A,B,C,D,E,F,G,H,I,J,K):[50]: inf with precondition: [F=1,B>=1,A+1>=2*B,2*B+1>=A,A>=B+1] evalrealshellsortbb8in(A,B,C,D,E,F,G,H,I,J,K):[51]: 1 with precondition: [F=0,I=C,J=D,K=E,A=G,B=H,0>=B,A+1>=2*B,2*B+1>=A] evalrealshellsortbb8in(A,B,C,D,E,F,G,H,I,J,K):[52]...: inf with precondition: [1>=F,F>=0,A+1>=2*B,2*B+1>=A,A>=B+2] evalrealshellsortbb8in(A,B,C,D,E,F,G,H,I,J,K):[53]...: inf with precondition: [1>=F,B>=1,F>=0,A+1>=2*B,2*B+1>=A,A>=B+1] evalrealshellsortbb8in(A,B,C,D,E,F,G,H,I,J,K):[54]...: inf with precondition: [1>=F,F>=0,A+1>=2*B,2*B+1>=A,A>=B+2] evalrealshellsortbb8in(A,B,C,D,E,F,G,H,I,J,K):[55]...: inf with precondition: [1>=F,B>=1,F>=0,A+1>=2*B,2*B+1>=A,A>=B+1] evalrealshellsortbb8in(A,B,C,D,E,F,G,H,I,J,K):[56]...: inf with precondition: [1>=F,F>=0,A+1>=2*B,2*B+1>=A,A>=B+2] evalrealshellsortbb8in(A,B,C,D,E,F,G,H,I,J,K):[57]...: inf with precondition: [1>=F,B>=1,F>=0,A+1>=2*B,2*B+1>=A,A>=B+1] evalrealshellsortbb8in(A,B,C,D,E,F,G,H,I,J,K):[58]...: inf with precondition: [F=1,A+1>=2*B,2*B+1>=A,A>=B+2] evalrealshellsortbb8in(A,B,C,D,E,F,G,H,I,J,K):[59]...: inf with precondition: [F=1,A+1>=2*B,2*B+1>=A,A>=B+2] evalrealshellsortbb8in(A,B,C,D,E,F,G,H,I,J,K):[60]...: inf with precondition: [F=1,B>=1,A+1>=2*B,2*B+1>=A,A>=B+1] evalrealshellsortbb8in(A,B,C,D,E,F,G,H,I,J,K):[61]...: inf with precondition: [F=1,B>=1,A+1>=2*B,2*B+1>=A,A>=B+1] evalrealshellsortbb8in(A,B,C,D,E,F,G,H,I,J,K):[[45],47]: 4+it1*(5)+it2*(inf)+it3*(4)+it4*(3+it5*(5)+it6*(inf)+it7*(4)) Such that:it1+it2=<1*A+ -2,it1+it2=<1*A+ -1,it3=<1*A,it3=<1*A+ -2,it3=<1/4*A+1/4,it3+it4=<1*A,it3+it4=<2*B+ -1,it4=<1*A,it4=<2*B+ -1 it7=<1/2*A+3/2,it7=<1/2*A+1/2,it7=<1*B+1,it7=<1*A+ -1,it7=<1*B,it7=<1*A,it5+it6=<1*A+ -1,it5+it6=<1*A with precondition: [F=1,B>=2,A+1>=2*B] evalrealshellsortbb8in(A,B,C,D,E,F,G,H,I,J,K):[[45],48]: inf with precondition: [F=1,B>=2,A+1>=2*B] evalrealshellsortbb8in(A,B,C,D,E,F,G,H,I,J,K):[[45],49]: 4+it1*(4)+it2*(3+it3*(5)+it4*(inf)+it5*(4)) Such that:it1=<1*A,it1=<1*A+ -1,it1=<1/2*A+1/2,it1+it2=<1*A,it1+it2=<2*B+ -1,it2=<1*A,it2=<2*B+ -1 it5=<1/2*A+3/2,it5=<1/2*A+1/2,it5=<1*B+1,it5=<1*A+ -1,it5=<1*B,it5=<1*A,it3+it4=<1*A+ -1,it3+it4=<1*A with precondition: [F=1,B>=2,A+1>=2*B] evalrealshellsortbb8in(A,B,C,D,E,F,G,H,I,J,K):[[45],50]: inf with precondition: [F=1,B>=2,A+1>=2*B] evalrealshellsortbb8in(A,B,C,D,E,F,G,H,I,J,K):[[45],51]: 1+it1*(3+it2*(5)+it3*(inf)+it4*(4)) Such that:it1=<1*A,it1=<1*G,it1=<1*I,it1=<2*B,it1=<1*A+1,it1=<1*G+1,it1=<1*I+1,it1=<2*A+ -3,it1=<2*A+ -2,it1=<2*B+ -1,it1=<2*G+ -3,it1=<2*G+ -2,it1=<2*I+ -3,it1=<2*I+ -2 it4=<1/2*A+3/2,it4=<1/2*A+1/2,it4=<1*B+1,it4=<1*A+ -1,it4=<1*B,it4=<1*A,it2+it3=<1*A+ -1,it2+it3=<1*A with precondition: [F=0,H=0,A=G,A=I,B>=1,K>=0,A+1>=2*B,A>=B+1] evalrealshellsortbb8in(A,B,C,D,E,F,G,H,I,J,K):[[45],52]...: inf with precondition: [1>=F,B>=2,F>=0,A+1>=2*B] evalrealshellsortbb8in(A,B,C,D,E,F,G,H,I,J,K):[[45],53]...: inf with precondition: [1>=F,B>=2,F>=0,A+1>=2*B] evalrealshellsortbb8in(A,B,C,D,E,F,G,H,I,J,K):[[45],54]...: inf with precondition: [1>=F,B>=2,F>=0,A+1>=2*B] evalrealshellsortbb8in(A,B,C,D,E,F,G,H,I,J,K):[[45],55]...: inf with precondition: [1>=F,B>=2,F>=0,A+1>=2*B] evalrealshellsortbb8in(A,B,C,D,E,F,G,H,I,J,K):[[45],56]...: inf with precondition: [1>=F,B>=2,F>=0,A+1>=2*B] evalrealshellsortbb8in(A,B,C,D,E,F,G,H,I,J,K):[[45],57]...: inf with precondition: [1>=F,B>=2,F>=0,A+1>=2*B] evalrealshellsortbb8in(A,B,C,D,E,F,G,H,I,J,K):[[45],58]...: inf with precondition: [F=1,B>=2,A+1>=2*B] evalrealshellsortbb8in(A,B,C,D,E,F,G,H,I,J,K):[[45],59]...: inf with precondition: [F=1,B>=2,A+1>=2*B] evalrealshellsortbb8in(A,B,C,D,E,F,G,H,I,J,K):[[45],60]...: inf with precondition: [F=1,B>=2,A+1>=2*B] evalrealshellsortbb8in(A,B,C,D,E,F,G,H,I,J,K):[[45],61]...: inf with precondition: [F=1,B>=2,A+1>=2*B] evalrealshellsortbb8in(A,B,C,D,E,F,G,H,I,J,K):[[46],51]: 1+it1*(3+it2*(4)) Such that:it1=<1,it1=<2 it2=<1 with precondition: [A=1,B=1,F=0,G=1,H=0,I=1,K=0] Inferred cost of evalrealshellsortreturnin(A,B,C,D,E): evalrealshellsortreturnin(A,B,C,D,E):[63]: 1 with precondition: [] Inferred cost of loop_cont_evalrealshellsortbb8in(A,B,C,D,E): loop_cont_evalrealshellsortbb8in(A,B,C,D,E):[65]: 1 with precondition: [] Inferred cost of evalrealshellsortentryin(A,B,C,D,E): evalrealshellsortentryin(A,B,C,D,E):[67]: 3 with precondition: [A=0] evalrealshellsortentryin(A,B,C,D,E):[68]: 3 with precondition: [A=1] evalrealshellsortentryin(A,B,C,D,E):[69]: 3+it1*(3+it2*(5)+it3*(inf)+it4*(4)) Such that:it1=<1*A,it1=<1*A+ -1,it1=<1*A+1,it1=<2*A+ -3,it1=<2*A+ -2 it4=<1/2*A+3/2,it4=<1/2*A+1/2,it4=<1/2*A+1,it4=<1*A+ -1,it4=<1/2*A,it4=<1*A,it2+it3=<1*A+ -1,it2+it3=<1*A with precondition: [A>=2] evalrealshellsortentryin(A,B,C,D,E):[70]: 5+it1*(5)+it2*(inf)+it3*(4) Such that:it1+it2=<1/2*A,it1+it2=<1*A+ -2,it1+it2=<1*A+ -1,it1+it2=<1/2*A+1,it1+it2=<1/2*A+ -1/2,it1+it2=<1/2*A+1/2,it3=<1*A,it3=<1/2*A,it3=<1*A+ -2,it3=<1*A+ -1,it3=<1*A+1,it3=<2*A+ -5,it3=<2*A+ -3,it3=<1/2*A+1/2 with precondition: [A>=3] evalrealshellsortentryin(A,B,C,D,E):[71]: inf with precondition: [A>=3] evalrealshellsortentryin(A,B,C,D,E):[72]: 5+it1*(4) Such that:it1=<1*A,it1=<1/2*A,it1=<1*A+ -1,it1=<1*A+1,it1=<1/2*A+1/2 with precondition: [A>=2] evalrealshellsortentryin(A,B,C,D,E):[73]: inf with precondition: [A>=2] evalrealshellsortentryin(A,B,C,D,E):[74]: 5+it1*(5)+it2*(inf)+it3*(4)+it4*(3+it5*(5)+it6*(inf)+it7*(4)) Such that:it1+it2=<1*A+ -2,it1+it2=<1*A+ -1,it3=<1*A,it3=<1*A+ -2,it3=<1/4*A+1/4,it3+it4=<1*A,it3+it4=<1*A+ -1,it4=<1*A,it4=<1*A+ -1 it7=<1/2*A+3/2,it7=<1/2*A+1/2,it7=<1/2*A+1,it7=<1*A+ -1,it7=<1/2*A,it7=<1*A,it5+it6=<1*A+ -1,it5+it6=<1*A with precondition: [A>=4] evalrealshellsortentryin(A,B,C,D,E):[75]: inf with precondition: [A>=4] evalrealshellsortentryin(A,B,C,D,E):[76]: 5+it1*(4)+it2*(3+it3*(5)+it4*(inf)+it5*(4)) Such that:it1=<1*A,it1=<1*A+ -1,it1=<1/2*A+1/2,it1+it2=<1*A,it1+it2=<1*A+ -1,it2=<1*A,it2=<1*A+ -1 it5=<1/2*A+3/2,it5=<1/2*A+1/2,it5=<1/2*A+1,it5=<1*A+ -1,it5=<1/2*A,it5=<1*A,it3+it4=<1*A+ -1,it3+it4=<1*A with precondition: [A>=4] evalrealshellsortentryin(A,B,C,D,E):[77]: inf with precondition: [A>=4] evalrealshellsortentryin(A,B,C,D,E):[78]: 3 with precondition: [0>=A+1] evalrealshellsortentryin(A,B,C,D,E):[79]...: inf with precondition: [A>=3] evalrealshellsortentryin(A,B,C,D,E):[80]...: inf with precondition: [A>=2] evalrealshellsortentryin(A,B,C,D,E):[81]...: inf with precondition: [A>=3] evalrealshellsortentryin(A,B,C,D,E):[82]...: inf with precondition: [A>=2] evalrealshellsortentryin(A,B,C,D,E):[83]...: inf with precondition: [A>=3] evalrealshellsortentryin(A,B,C,D,E):[84]...: inf with precondition: [A>=2] evalrealshellsortentryin(A,B,C,D,E):[85]...: inf with precondition: [A>=4] evalrealshellsortentryin(A,B,C,D,E):[86]...: inf with precondition: [A>=4] evalrealshellsortentryin(A,B,C,D,E):[87]...: inf with precondition: [A>=4] evalrealshellsortentryin(A,B,C,D,E):[88]...: inf with precondition: [A>=4] evalrealshellsortentryin(A,B,C,D,E):[89]...: inf with precondition: [A>=4] evalrealshellsortentryin(A,B,C,D,E):[90]...: inf with precondition: [A>=4] evalrealshellsortentryin(A,B,C,D,E):[91]...: inf with precondition: [A>=3] evalrealshellsortentryin(A,B,C,D,E):[92]...: inf with precondition: [A>=2] evalrealshellsortentryin(A,B,C,D,E):[93]...: inf with precondition: [A>=3] evalrealshellsortentryin(A,B,C,D,E):[94]...: inf with precondition: [A>=2] evalrealshellsortentryin(A,B,C,D,E):[95]...: inf with precondition: [A>=3] evalrealshellsortentryin(A,B,C,D,E):[96]...: inf with precondition: [A>=2] evalrealshellsortentryin(A,B,C,D,E):[97]...: inf with precondition: [A>=3] evalrealshellsortentryin(A,B,C,D,E):[98]...: inf with precondition: [A>=3] evalrealshellsortentryin(A,B,C,D,E):[99]...: inf with precondition: [A>=2] evalrealshellsortentryin(A,B,C,D,E):[100]...: inf with precondition: [A>=2] evalrealshellsortentryin(A,B,C,D,E):[101]...: inf with precondition: [A>=4] evalrealshellsortentryin(A,B,C,D,E):[102]...: inf with precondition: [A>=4] evalrealshellsortentryin(A,B,C,D,E):[103]...: inf with precondition: [A>=4] evalrealshellsortentryin(A,B,C,D,E):[104]...: inf with precondition: [A>=4] evalrealshellsortentryin(A,B,C,D,E):[105]...: inf with precondition: [A>=4] evalrealshellsortentryin(A,B,C,D,E):[106]...: inf with precondition: [A>=4] evalrealshellsortentryin(A,B,C,D,E):[107]...: inf with precondition: [A>=4] evalrealshellsortentryin(A,B,C,D,E):[108]...: inf with precondition: [A>=4] evalrealshellsortentryin(A,B,C,D,E):[109]...: inf with precondition: [A>=4] evalrealshellsortentryin(A,B,C,D,E):[110]...: inf with precondition: [A>=4] Inferred cost of evalrealshellsortstart(A,B,C,D,E): evalrealshellsortstart(A,B,C,D,E):[112]: 4 with precondition: [A=0] evalrealshellsortstart(A,B,C,D,E):[113]: 4 with precondition: [A=1] evalrealshellsortstart(A,B,C,D,E):[114]: 4+it1*(3+it2*(5)+it3*(inf)+it4*(4)) Such that:it1=<1*A,it1=<1*A+ -1,it1=<1*A+1,it1=<2*A+ -3,it1=<2*A+ -2 it4=<1/2*A+3/2,it4=<1/2*A+1/2,it4=<1/2*A+1,it4=<1*A+ -1,it4=<1/2*A,it4=<1*A,it2+it3=<1*A+ -1,it2+it3=<1*A with precondition: [A>=2] evalrealshellsortstart(A,B,C,D,E):[115]: 6+it1*(5)+it2*(inf)+it3*(4) Such that:it1+it2=<1/2*A,it1+it2=<1*A+ -2,it1+it2=<1*A+ -1,it1+it2=<1/2*A+1,it1+it2=<1/2*A+ -1/2,it1+it2=<1/2*A+1/2,it3=<1*A,it3=<1/2*A,it3=<1*A+ -2,it3=<1*A+ -1,it3=<1*A+1,it3=<2*A+ -5,it3=<2*A+ -3,it3=<1/2*A+1/2 with precondition: [A>=3] evalrealshellsortstart(A,B,C,D,E):[116]: inf with precondition: [A>=3] evalrealshellsortstart(A,B,C,D,E):[117]: 6+it1*(4) Such that:it1=<1*A,it1=<1/2*A,it1=<1*A+ -1,it1=<1*A+1,it1=<1/2*A+1/2 with precondition: [A>=2] evalrealshellsortstart(A,B,C,D,E):[118]: inf with precondition: [A>=2] evalrealshellsortstart(A,B,C,D,E):[119]: 6+it1*(5)+it2*(inf)+it3*(4)+it4*(3+it5*(5)+it6*(inf)+it7*(4)) Such that:it1+it2=<1*A+ -2,it1+it2=<1*A+ -1,it3=<1*A,it3=<1*A+ -2,it3=<1/4*A+1/4,it3+it4=<1*A,it3+it4=<1*A+ -1,it4=<1*A,it4=<1*A+ -1 it7=<1/2*A+3/2,it7=<1/2*A+1/2,it7=<1/2*A+1,it7=<1*A+ -1,it7=<1/2*A,it7=<1*A,it5+it6=<1*A+ -1,it5+it6=<1*A with precondition: [A>=4] evalrealshellsortstart(A,B,C,D,E):[120]: inf with precondition: [A>=4] evalrealshellsortstart(A,B,C,D,E):[121]: 6+it1*(4)+it2*(3+it3*(5)+it4*(inf)+it5*(4)) Such that:it1=<1*A,it1=<1*A+ -1,it1=<1/2*A+1/2,it1+it2=<1*A,it1+it2=<1*A+ -1,it2=<1*A,it2=<1*A+ -1 it5=<1/2*A+3/2,it5=<1/2*A+1/2,it5=<1/2*A+1,it5=<1*A+ -1,it5=<1/2*A,it5=<1*A,it3+it4=<1*A+ -1,it3+it4=<1*A with precondition: [A>=4] evalrealshellsortstart(A,B,C,D,E):[122]: inf with precondition: [A>=4] evalrealshellsortstart(A,B,C,D,E):[123]: 4 with precondition: [0>=A+1] evalrealshellsortstart(A,B,C,D,E):[124]...: inf with precondition: [A>=3] evalrealshellsortstart(A,B,C,D,E):[125]...: inf with precondition: [A>=2] evalrealshellsortstart(A,B,C,D,E):[126]...: inf with precondition: [A>=3] evalrealshellsortstart(A,B,C,D,E):[127]...: inf with precondition: [A>=2] evalrealshellsortstart(A,B,C,D,E):[128]...: inf with precondition: [A>=3] evalrealshellsortstart(A,B,C,D,E):[129]...: inf with precondition: [A>=2] evalrealshellsortstart(A,B,C,D,E):[130]...: inf with precondition: [A>=4] evalrealshellsortstart(A,B,C,D,E):[131]...: inf with precondition: [A>=4] evalrealshellsortstart(A,B,C,D,E):[132]...: inf with precondition: [A>=4] evalrealshellsortstart(A,B,C,D,E):[133]...: inf with precondition: [A>=4] evalrealshellsortstart(A,B,C,D,E):[134]...: inf with precondition: [A>=4] evalrealshellsortstart(A,B,C,D,E):[135]...: inf with precondition: [A>=4] evalrealshellsortstart(A,B,C,D,E):[136]...: inf with precondition: [A>=3] evalrealshellsortstart(A,B,C,D,E):[137]...: inf with precondition: [A>=2] evalrealshellsortstart(A,B,C,D,E):[138]...: inf with precondition: [A>=3] evalrealshellsortstart(A,B,C,D,E):[139]...: inf with precondition: [A>=2] evalrealshellsortstart(A,B,C,D,E):[140]...: inf with precondition: [A>=3] evalrealshellsortstart(A,B,C,D,E):[141]...: inf with precondition: [A>=2] evalrealshellsortstart(A,B,C,D,E):[142]...: inf with precondition: [A>=3] evalrealshellsortstart(A,B,C,D,E):[143]...: inf with precondition: [A>=3] evalrealshellsortstart(A,B,C,D,E):[144]...: inf with precondition: [A>=2] evalrealshellsortstart(A,B,C,D,E):[145]...: inf with precondition: [A>=2] evalrealshellsortstart(A,B,C,D,E):[146]...: inf with precondition: [A>=4] evalrealshellsortstart(A,B,C,D,E):[147]...: inf with precondition: [A>=4] evalrealshellsortstart(A,B,C,D,E):[148]...: inf with precondition: [A>=4] evalrealshellsortstart(A,B,C,D,E):[149]...: inf with precondition: [A>=4] evalrealshellsortstart(A,B,C,D,E):[150]...: inf with precondition: [A>=4] evalrealshellsortstart(A,B,C,D,E):[151]...: inf with precondition: [A>=4] evalrealshellsortstart(A,B,C,D,E):[152]...: inf with precondition: [A>=4] evalrealshellsortstart(A,B,C,D,E):[153]...: inf with precondition: [A>=4] evalrealshellsortstart(A,B,C,D,E):[154]...: inf with precondition: [A>=4] evalrealshellsortstart(A,B,C,D,E):[155]...: inf with precondition: [A>=4] Solved cost expressions of evalrealshellsortstart(A,B,C,D,E): evalrealshellsortstart(A,B,C,D,E):[112]: 4 with precondition: [A=0] evalrealshellsortstart(A,B,C,D,E):[113]: 4 with precondition: [A=1] evalrealshellsortstart(A,B,C,D,E):[114]: inf with precondition: [A>=2] evalrealshellsortstart(A,B,C,D,E):[115]: inf with precondition: [A>=3] evalrealshellsortstart(A,B,C,D,E):[116]: inf with precondition: [A>=3] evalrealshellsortstart(A,B,C,D,E):[117]: 2*A+6 with precondition: [A>=2] evalrealshellsortstart(A,B,C,D,E):[118]: inf with precondition: [A>=2] evalrealshellsortstart(A,B,C,D,E):[119]: inf with precondition: [A>=4] evalrealshellsortstart(A,B,C,D,E):[120]: inf with precondition: [A>=4] evalrealshellsortstart(A,B,C,D,E):[121]: inf with precondition: [A>=4] evalrealshellsortstart(A,B,C,D,E):[122]: inf with precondition: [A>=4] evalrealshellsortstart(A,B,C,D,E):[123]: 4 with precondition: [0>=A+1] evalrealshellsortstart(A,B,C,D,E):[124]...: inf with precondition: [A>=3] evalrealshellsortstart(A,B,C,D,E):[125]...: inf with precondition: [A>=2] evalrealshellsortstart(A,B,C,D,E):[126]...: inf with precondition: [A>=3] evalrealshellsortstart(A,B,C,D,E):[127]...: inf with precondition: [A>=2] evalrealshellsortstart(A,B,C,D,E):[128]...: inf with precondition: [A>=3] evalrealshellsortstart(A,B,C,D,E):[129]...: inf with precondition: [A>=2] evalrealshellsortstart(A,B,C,D,E):[130]...: inf with precondition: [A>=4] evalrealshellsortstart(A,B,C,D,E):[131]...: inf with precondition: [A>=4] evalrealshellsortstart(A,B,C,D,E):[132]...: inf with precondition: [A>=4] evalrealshellsortstart(A,B,C,D,E):[133]...: inf with precondition: [A>=4] evalrealshellsortstart(A,B,C,D,E):[134]...: inf with precondition: [A>=4] evalrealshellsortstart(A,B,C,D,E):[135]...: inf with precondition: [A>=4] evalrealshellsortstart(A,B,C,D,E):[136]...: inf with precondition: [A>=3] evalrealshellsortstart(A,B,C,D,E):[137]...: inf with precondition: [A>=2] evalrealshellsortstart(A,B,C,D,E):[138]...: inf with precondition: [A>=3] evalrealshellsortstart(A,B,C,D,E):[139]...: inf with precondition: [A>=2] evalrealshellsortstart(A,B,C,D,E):[140]...: inf with precondition: [A>=3] evalrealshellsortstart(A,B,C,D,E):[141]...: inf with precondition: [A>=2] evalrealshellsortstart(A,B,C,D,E):[142]...: inf with precondition: [A>=3] evalrealshellsortstart(A,B,C,D,E):[143]...: inf with precondition: [A>=3] evalrealshellsortstart(A,B,C,D,E):[144]...: inf with precondition: [A>=2] evalrealshellsortstart(A,B,C,D,E):[145]...: inf with precondition: [A>=2] evalrealshellsortstart(A,B,C,D,E):[146]...: inf with precondition: [A>=4] evalrealshellsortstart(A,B,C,D,E):[147]...: inf with precondition: [A>=4] evalrealshellsortstart(A,B,C,D,E):[148]...: inf with precondition: [A>=4] evalrealshellsortstart(A,B,C,D,E):[149]...: inf with precondition: [A>=4] evalrealshellsortstart(A,B,C,D,E):[150]...: inf with precondition: [A>=4] evalrealshellsortstart(A,B,C,D,E):[151]...: inf with precondition: [A>=4] evalrealshellsortstart(A,B,C,D,E):[152]...: inf with precondition: [A>=4] evalrealshellsortstart(A,B,C,D,E):[153]...: inf with precondition: [A>=4] evalrealshellsortstart(A,B,C,D,E):[154]...: inf with precondition: [A>=4] evalrealshellsortstart(A,B,C,D,E):[155]...: inf with precondition: [A>=4] Maximum cost of evalrealshellsortstart(A,B,C,D,E): inf Asymptotic class: infinity Time statistics: Partial evaluation computed in 39 ms. Invariants computed in 293 ms. ----Backward Invariants 201 ms. ----Transitive Invariants 15 ms. Refinement performed in 196 ms. Termination proved in 29 ms. Upper bounds computed in 585 ms. ----Phase cost structures 170 ms. --------Equation cost structures 147 ms. --------Inductive compression(1) 1 ms. --------Inductive compression(2) 0 ms. --------Black Cost 0 ms. ----Chain cost structures 392 ms. ----Solving cost expressions 8 ms. Compressed phase information: 31 Compressed Chains: 0 Compressed invariants: 0 Total analysis performed in 1197 ms.