PUBS: A Practical Upper Bounds Solver
Please follow these steps (more details in the help section):

Step 1: Provide a Cost Equation System.
Step 2: Provide an Entry or leave it empty and the solver will take the first equation as an entry. Also select the type of Computation.
Step 3: Click on the Solve button.

 CES eq('Inverse_invert([[D)[[D'(A),16,['2'(A,A,A,A,A,0,B,C)],[D=0, E=0, F=0, G=0, H=0, B=0, C=0, A>=0, A>=0, A>=0, A>=0]). eq('2'(A,B,C,D,E,F,G,H),0,['2_loop'(B,D,F), '75_normal'(A,B,C,D,E,I,G,H,J)],[-1*B+1*I>=0, -1*F+1*I>=0]). eq('2_loop'(A,B,C),3,['76'(A,B,C,C,A)],[]). eq('75_normal'(A,B,C,D,E,F,G,H,I),3,['Inverse_gaussian([[D[I)V'(A,E), '62_normal'(A,B,C,D,E,F,G,H,J)],[1*E>=0]). eq('76'(A,B,C,C,A),0,['4'(A,B,C)],[C+1==A]). eq('Inverse_gaussian([[D[I)V'(A,B),8,['27'(A,B,B,B,0,C,D,E,F,G,H,I,J)],[K=0, L=0, M=0, C=0, D=0, E=0, F=0, G=0, H=0, I=0, J=0, B>=0, B>=0]). eq('62_normal'(A,B,C,D,E,F,G,H,I),0,['5'(A,B,C,D,E,F,G,H)],[]). eq('4'(A,B,C),8,['2_loop'(A,B,D)],[D=C+1]). eq('2_loop_nexit'(A,B,C),0,[],[]). eq('27'(A,B,C,D,E,F,G,H,I,J,K,L,M),0,['27_loop'(B,C,E), '93_normal'(A,B,C,D,N,F,G,H,I,J,K,L,M,O)],[-1*C+1*N>=0, -1*E+1*N>=0]). eq('5'(A,B,C,D,E,F,G,H),2,['7_loop'(A,B,D,E,0,G,H), '73_normal'(A,B,C,D,E,I,J,K,L)],[-1*0+1*I>=0]). eq('27_loop'(A,B,C),3,['94'(A,B,C,C,B)],[]). eq('93_normal'(A,B,C,D,E,F,G,H,I,J,K,L,M,N),2,['30'(A,B,C,D,0,F,G,H,I,J,K,L,M)],[]). eq('7_loop'(A,B,C,D,E,F,G),5,['74'(A,B,C,D,E,F,G,E,H)],[H=B-1]). eq('73_normal'(A,B,C,D,E,F,G,H,I),2,['10'(A,B,C,D,E,0,G,H)],[]). eq('94'(A,B,C,C,B),0,['29'(A,B,C)],[C+1==B]). eq('30'(A,B,C,D,E,F,G,H,I,J,K,L,M),0,['30_loop'(A,C,D,E,F,G,H,I,J), '91_normal'(A,B,C,D,N,O,P,Q,R,S,K,L,M,T)],[-1*C+1*N>=0, -1*E+1*N>=0]). eq('74'(A,B,C,D,E,F,G,E,H),0,['9'(A,B,C,D,E,F,G)],[E+1==H]). eq('10'(A,B,C,D,E,F,G,H),0,['10_loop'(A,B,C,D,E,F,G,H), '67_normal'(A,B,C,D,E,I,J,K,L)],[-1*B+1*I>=0, -1*F+1*I>=0]). eq('29'(A,B,C),6,['27_loop'(A,B,D)],[D=C+1]). eq('27_loop_nexit'(A,B,C),0,[],[]). eq('30_loop'(A,B,C,D,E,F,G,H,I),3,['92'(A,B,C,D,E,F,G,H,I,D,B)],[]). eq('91_normal'(A,B,C,D,E,F,G,H,I,J,K,L,M,N),0,['31'(A,B,C,D,E,F,G,H,I,J,K,L,M)],[]). eq('9'(A,B,C,D,E,F,G),4,['11_loop'(A,B,C,D,E,H,G), '71_normal'(A,B,C,D,E,I,J)],[H=E+1, -1*B+1*I>=0, -1*H+1*I>=0]). eq('7_loop_nexit'(A,B,C,D,E,F,G),0,[],[]). eq('10_loop'(A,B,C,D,E,F,G,H),3,['68'(A,B,C,D,E,F,G,H,F,B)],[]). eq('67_normal'(A,B,C,D,E,F,G,H,I),2,['16'(A,B,C,D,E,F,G,H,C)],[]). eq('92'(A,B,C,D,E,F,G,H,I,D,B),0,['32'(A,B,C,D,E,F,G,H,I)],[D+1==B]). eq('31'(A,B,C,D,E,F,G,H,I,J,K,L,M),4,['33_loop'(A,B,C,D,0,0,G,H,I,J,K,L,M), '87_normal'(A,B,C,D,N,O,P,Q,R,S,T,U,V,W)],[-1*0+1*O>=0]). eq('11_loop'(A,B,C,D,E,F,G),3,['72'(A,B,C,D,E,F,G,F,B)],[]). eq('71_normal'(A,B,C,D,E,F,G),2,['7_loop'(A,B,C,D,H,F,G)],[H=E+1]). eq('68'(A,B,C,D,E,F,G,H,F,B),0,['13'(A,B,C,D,E,F,G,H)],[F+1==B]). eq('16'(A,B,C,D,E,F,G,H,I),0,[],[]). eq('32'(A,B,C,D,E,F,G,H,I),4,['34_loop'(A,B,D,J,K,0,H,I), '89_normal'(A,B,C,D,L,M,N,O,P)],[-1*B+1*N>=0, -1*0+1*N>=0]). eq('30_loop_nexit'(A,B,C,D,E,F,G,H,I),0,[],[]). eq('33_loop'(A,B,C,D,E,F,G,H,I,J,K,L,M),5,['88'(A,B,C,D,E,F,G,H,I,J,K,L,M,F,N)],[N=C-1]). eq('87_normal'(A,B,C,D,E,F,G,H,I,J,K,L,M,N),0,['35'(A,B,C,D,E,F,G,H,I,J,K,L,M)],[]). eq('72'(A,B,C,D,E,F,G,F,B),0,['15'(A,B,C,D,E,F,G)],[F+1==B]). eq('13'(A,B,C,D,E,F,G,H),32,['17_loop'(A,B,C,D,E,F,I,H), '65_normal'(A,B,C,D,E,F,J,K)],[L=B-1, M=B-1, N=B-1, O=B-1, I=B-2, -1*J>=1, 1*I+ -1*J>=0]). eq('10_loop_nexit'(A,B,C,D,E,F,G,H),0,[],[]). eq('34_loop'(A,B,C,D,E,F,G,H),3,['90'(A,B,C,D,E,F,G,H,F,B)],[]). eq('89_normal'(A,B,C,D,E,F,G,H,I),0,['37'(A,B,C,D,E,F,G,H,I)],[]). eq('88'(A,B,C,D,E,F,G,H,I,J,K,L,M,F,N),0,['36'(A,B,C,D,E,F,G,H,I,J,K,L,M)],[F+1==N]). eq('35'(A,B,C,D,E,F,G,H,I,J,K,L,M),1,[],[]). eq('15'(A,B,C,D,E,F,G),2,['18_loop'(A,B,C,D,E,F,0), '69_normal'(A,B,C,D,E,F,H)],[-1*B+1*H>=0, -1*0+1*H>=0]). eq('11_loop_nexit'(A,B,C,D,E,F,G),0,[],[]). eq('17_loop'(A,B,C,D,E,F,G,H),2,['66'(A,B,C,D,E,F,G,H,G)],[]). eq('65_normal'(A,B,C,D,E,F,G,H),2,['10_loop'(A,B,C,D,E,I,G,H)],[I=F+1]). eq('90'(A,B,C,D,E,F,G,H,F,B),0,['38'(A,B,C,D,E,F,G,H)],[F+1==B]). eq('37'(A,B,C,D,E,F,G,H,I),6,['30_loop'(A,B,C,J,E,F,G,H,I)],[J=D+1]). eq('36'(A,B,C,D,E,F,G,H,I,J,K,L,M),4,['40_loop'(A,B,C,D,F,N,O,F,J,K), '85_normal'(A,B,C,D,P,F,Q,R,S,T,U,L,M)],[-1*C+1*S>=0, -1*F+1*S>=0]). eq('33_loop_nexit'(A,B,C,D,E,F,G,H,I,J,K,L,M),0,[],[]). eq('18_loop'(A,B,C,D,E,F,G),3,['70'(A,B,C,D,E,F,G,G,B)],[]). eq('69_normal'(A,B,C,D,E,F,G),2,['11_loop'(A,B,C,D,E,H,G)],[H=F+1]). eq('66'(A,B,C,D,E,F,G,H,G),0,['20'(A,B,C,D,E,F,G,H)],[G>=0]). eq('66'(A,B,C,D,E,F,G,H,G),0,['17_loop_nexit'(A,B,C,D,E,F,G,H)],[G=< -1]). eq('38'(A,B,C,D,E,F,G,H),6,['java/lang/Math_abs(D)D'(I,J), '77_normal'(A,B,C,D,E,F,G,H,K,L)],[]). eq('34_loop_nexit'(A,B,C,D,E,F,G,H),0,[],[]). eq('40_loop'(A,B,C,D,E,F,G,H,I,J),3,['86'(A,B,C,D,E,F,G,H,I,J,H,C)],[]). eq('85_normal'(A,B,C,D,E,F,G,H,I,J,K,L,M),0,['43'(A,B,C,D,E,F,G,H,I,J,K,L,M)],[]). eq('70'(A,B,C,D,E,F,G,G,B),0,['22'(A,B,C,D,E,F,G)],[G+1==B]). eq('20'(A,B,C,D,E,F,G,H),16,['23_loop'(A,B,C,E,F,G,I), '63_normal'(A,B,C,D,E,F,G,J)],[I=G+1, -1*B+1*J>=0, -1*I+1*J>=0]). eq('17_loop_nexit'(A,B,C,D,E,F,G,H),0,[],[]). eq('java/lang/Math_abs(D)D'(A,B),4,['95'(A,B,C)],[]). eq('77_normal'(A,B,C,D,E,F,G,H,I,J),0,['41'(A,B,C,D,E,F,G,H,I,J)],[]). eq('86'(A,B,C,D,E,F,G,H,I,J,H,C),0,['44'(A,B,C,D,E,F,G,H,I,J)],[H+1==C]). eq('43'(A,B,C,D,E,F,G,H,I,J,K,L,M),18,['47_loop'(A,B,C,F,N,K,L,M), '83_normal'(A,B,C,D,E,F,G,H,O,P,Q,R,S)],[N=F+1, -1*C+1*P>=0, -1*N+1*P>=0]). eq('22'(A,B,C,D,E,F,G),27,['18_loop'(A,B,C,D,E,F,H)],[H=G+1]). eq('18_loop_nexit'(A,B,C,D,E,F,G),0,[],[]). eq('23_loop'(A,B,C,D,E,F,G),3,['64'(A,B,C,D,E,F,G,G,B)],[]). eq('63_normal'(A,B,C,D,E,F,G,H),17,['17_loop'(A,B,C,D,E,F,I,H)],[I=G+ -1]). eq('95'(A,B,C),0,['57'(A,B)],[C>=1]). eq('95'(A,B,C),0,['58'(A,B)],[C=<0]). eq('41'(A,B,C,D,E,F,G,H,I,J),5,['78'(A,B,C,D,E,F,I,J,K)],[]). eq('44'(A,B,C,D,E,F,G,H,I,J),8,['java/lang/Math_abs(D)D'(K,L), '79_normal'(A,B,C,D,E,F,G,H,I,J,M,N)],[]). eq('40_loop_nexit'(A,B,C,D,E,F,G,H,I,J),0,[],[]). eq('47_loop'(A,B,C,D,E,F,G,H),3,['84'(A,B,C,D,E,F,G,H,E,C)],[]). eq('83_normal'(A,B,C,D,E,F,G,H,I,J,K,L,M),2,['33_loop'(A,B,C,D,E,N,G,H,I,J,K,L,M)],[N=F+1]). eq('64'(A,B,C,D,E,F,G,G,B),0,['25'(A,B,C,D,E,F,G)],[G+1==B]). eq('57'(A,B),1,['59'(A,B,A,B)],[]). eq('58'(A,B),4,['59'(A,B,C,D)],[]). eq('78'(A,B,C,D,E,F,G,H,I),0,['45'(A,B,C,D,E,F,G,H)],[I=<0]). eq('78'(A,B,C,D,E,F,G,H,I),0,['46'(A,B,C,D,E,F,G,H)],[I>=1]). eq('79_normal'(A,B,C,D,E,F,G,H,I,J,K,L),0,['48'(A,B,C,D,E,F,G,H,I,J,K,L)],[]). eq('84'(A,B,C,D,E,F,G,H,E,C),0,['50'(A,B,C,D,E,F,G,H)],[E+1==C]). eq('25'(A,B,C,D,E,F,G),23,['23_loop'(A,B,C,D,E,F,H)],[H=G+1]). eq('23_loop_nexit'(A,B,C,D,E,F,G),0,[],[]). eq('59'(A,B,C,D),1,[],[]). eq('45'(A,B,C,D,E,F,G,H),2,['34_loop'(A,B,C,D,E,I,G,H)],[I=F+1]). eq('46'(A,B,C,D,E,F,G,H),2,['45'(A,B,C,G,H,F,G,H)],[]). eq('48'(A,B,C,D,E,F,G,H,I,J,K,L),13,['80'(A,B,C,D,E,F,G,H,M,N,O)],[]). eq('50'(A,B,C,D,E,F,G,H),28,['53_loop'(A,B,C,D,E,I,J,K), '81_normal'(A,B,C,D,E,I,J,L)],[K=D+1, -1*C+1*L>=0, -1*K+1*L>=0]). eq('47_loop_nexit'(A,B,C,D,E,F,G,H),0,[],[]). eq('80'(A,B,C,D,E,F,G,H,I,J,K),0,['51'(A,B,C,D,E,F,G,H,I,J)],[K=<0]). eq('80'(A,B,C,D,E,F,G,H,I,J,K),0,['52'(A,B,C,D,E,F,G,H,I,J)],[K>=1]). eq('53_loop'(A,B,C,D,E,F,G,H),3,['82'(A,B,C,D,E,F,G,H,H,C)],[]). eq('81_normal'(A,B,C,D,E,F,G,H),2,['47_loop'(A,B,C,D,I,F,G,H)],[I=E+1]). eq('51'(A,B,C,D,E,F,G,H,I,J),2,['40_loop'(A,B,C,D,E,F,G,K,I,J)],[K=H+1]). eq('52'(A,B,C,D,E,F,G,H,I,J),4,['51'(A,B,C,D,E,I,J,H,I,J)],[]). eq('82'(A,B,C,D,E,F,G,H,H,C),0,['55'(A,B,C,D,E,F,G,H)],[H+1==C]). eq('55'(A,B,C,D,E,F,G,H),21,['53_loop'(A,B,C,D,E,F,G,I)],[I=H+1]). eq('53_loop_nexit'(A,B,C,D,E,F,G,H),0,[],[]). File Entry IEntry # Compute Upper Bound (Normal) Upper Bound (Normal with level-count enabled) Upper Bound (series) Lower Bound (series)