supcontext(_ctx_stack_1); assume((n>1000)); assume((n>1000)); declare(n, integer); supcontext(_ctx_stack_2); fullratsimp(expand((i+1))); fullratsimp(expand((i+1))); solve([(_r1_x=i)], i); subst(_r1_x, i,i); subst(_r1_x, i,(i+1)); subst(_r1_x, i,i); subst(_r1_x, i,(i+1)); diff((_r1_x+1),_r1_x); is(1<0); solve([(0=_r1_x)], _r1_x); solve([(n=(_r1_x+1))], _r1_x); fullratsimp(expand(((n-1)+(1/1)))); diff((_r1_x+1),_r1_x); is(1<0); solve([(0=_r1_x)], _r1_x); solve([(n=(_r1_x+1))], _r1_x); _tmp:fullratsimp(((n-1)+(1/1)))$ fullratsimp( (num(_tmp)+denom(_tmp)-1) / denom(_tmp) ); is(0>=0); is(n<=n); assume((_r1_x>=0)); assume((_r1_x<=n)); assume(equal(i,_r1_x)); is(_r1_x<(_r1_x+1)); is(_r1_x>=_r1_x); diff((_r1_x+1),_r1_x); fullratsimp(expand((n-1))); is(1<0); subst(0, _r1_x,_r1_x); subst((n-1), _r1_x,(_r1_x+1)); is(1<0); is(_r1_x<(_r1_x+1)); is(_r1_x>=_r1_x); diff((_r1_x+1),_r1_x); fullratsimp(expand((n-1))); is(1<0); subst(0, _r1_x,_r1_x); subst((n-1), _r1_x,(_r1_x+1)); is(1<0); killcontext(_ctx_stack_2); is(equal(n,0)); killcontext(_ctx_stack_1); supcontext(_ctx_stack_1); assume((w>1000)); assume((h>1000)); assume((d>1000)); assume((w>1000)); assume((h>1000)); assume((d>1000)); declare(d, integer); declare(h, integer); declare(w, integer); supcontext(_ctx_stack_2); fullratsimp(expand((i+1))); fullratsimp(expand((j+1))); fullratsimp(expand((k+1))); fullratsimp(expand((i+1))); fullratsimp(expand((j+1))); fullratsimp(expand((k+1))); solve([(_r2_x=i)], i); solve([(_r2_y=j)], j); solve([(_r2_z=k)], k); subst(_r2_x, i,i); subst(_r2_y, j,j); subst(_r2_z, k,k); subst(_r2_x, i,(i+1)); subst(_r2_y, j,(j+1)); subst(_r2_z, k,(k+1)); subst(_r2_x, i,i); subst(_r2_y, j,j); subst(_r2_z, k,k); subst(_r2_x, i,(i+1)); subst(_r2_y, j,(j+1)); subst(_r2_z, k,(k+1)); diff((_r2_x+1),_r2_x); diff((_r2_y+1),_r2_y); diff((_r2_z+1),_r2_z); is(1<0); is(1<0); is(1<0); solve([(0=_r2_x)], _r2_x); solve([(0=_r2_y)], _r2_y); solve([(0=_r2_z)], _r2_z); solve([(w=(_r2_x+1))], _r2_x); fullratsimp(expand(((w-1)+(1/1)))); solve([(h=(_r2_y+1))], _r2_y); fullratsimp(expand(((h-1)+(1/1)))); solve([(d=(_r2_z+1))], _r2_z); fullratsimp(expand(((d-1)+(1/1)))); diff((_r2_x+1),_r2_x); diff((_r2_y+1),_r2_y); diff((_r2_z+1),_r2_z); is(1<0); is(1<0); is(1<0); solve([(0=_r2_x)], _r2_x); solve([(0=_r2_y)], _r2_y); solve([(0=_r2_z)], _r2_z); solve([(w=(_r2_x+1))], _r2_x); _tmp:fullratsimp(((w-1)+(1/1)))$ fullratsimp( (num(_tmp)+denom(_tmp)-1) / denom(_tmp) ); solve([(h=(_r2_y+1))], _r2_y); _tmp:fullratsimp(((h-1)+(1/1)))$ fullratsimp( (num(_tmp)+denom(_tmp)-1) / denom(_tmp) ); solve([(d=(_r2_z+1))], _r2_z); _tmp:fullratsimp(((d-1)+(1/1)))$ fullratsimp( (num(_tmp)+denom(_tmp)-1) / denom(_tmp) ); is(0>=0); is(w<=w); is(0>=0); is(h<=h); is(0>=0); is(d<=d); assume((_r2_x>=0)); assume((_r2_x<=w)); assume((_r2_y>=0)); assume((_r2_y<=h)); assume((_r2_z>=0)); assume((_r2_z<=d)); assume(equal(i,_r2_x)); assume(equal(j,_r2_y)); assume(equal(k,_r2_z)); is(_r2_x<(_r2_x+1)); is(_r2_x>=_r2_x); is(_r2_y<(_r2_y+1)); is(_r2_y>=_r2_y); is(_r2_z<(_r2_z+1)); is(_r2_z>=_r2_z); diff((_r2_x+1),_r2_x); diff((_r2_y+1),_r2_y); diff((_r2_z+1),_r2_z); fullratsimp(expand((w-1))); fullratsimp(expand((h-1))); fullratsimp(expand((d-1))); is(1<0); is(1<0); is(1<0); subst(0, _r2_x,_r2_x); subst(0, _r2_y,_r2_y); subst(0, _r2_z,_r2_z); subst((w-1), _r2_x,(_r2_x+1)); subst((h-1), _r2_y,(_r2_y+1)); subst((d-1), _r2_z,(_r2_z+1)); is(1<0); is(1<0); is(1<0); is(_r2_x<(_r2_x+1)); is(_r2_x>=_r2_x); is(_r2_y<(_r2_y+1)); is(_r2_y>=_r2_y); is(_r2_z<(_r2_z+1)); is(_r2_z>=_r2_z); diff((_r2_x+1),_r2_x); diff((_r2_y+1),_r2_y); diff((_r2_z+1),_r2_z); fullratsimp(expand((w-1))); fullratsimp(expand((h-1))); fullratsimp(expand((d-1))); is(1<0); is(1<0); is(1<0); subst(0, _r2_x,_r2_x); subst(0, _r2_y,_r2_y); subst(0, _r2_z,_r2_z); subst((w-1), _r2_x,(_r2_x+1)); subst((h-1), _r2_y,(_r2_y+1)); subst((d-1), _r2_z,(_r2_z+1)); is(1<0); is(1<0); is(1<0); killcontext(_ctx_stack_2); is(equal(w,0)); is(equal(h,0)); is(equal(d,0)); killcontext(_ctx_stack_1); supcontext(_ctx_stack_1); assume((w>1000)); assume((h>1000)); assume((w>1000)); assume((h>1000)); declare(h, integer); declare(w, integer); supcontext(_ctx_stack_2); fullratsimp(expand((i+1))); fullratsimp(expand((j+1))); fullratsimp(expand((i+1))); fullratsimp(expand((j+1))); solve([(_r3_x=i)], i); solve([(_r3_y=j)], j); subst(_r3_x, i,i); subst(_r3_y, j,j); subst(_r3_x, i,(i+1)); subst(_r3_y, j,(j+1)); subst(_r3_x, i,i); subst(_r3_y, j,j); subst(_r3_x, i,(i+1)); subst(_r3_y, j,(j+1)); diff((_r3_x+1),_r3_x); diff((_r3_y+1),_r3_y); is(1<0); is(1<0); solve([(0=_r3_x)], _r3_x); solve([(0=_r3_y)], _r3_y); solve([(w=(_r3_x+1))], _r3_x); fullratsimp(expand(((w-1)+(1/1)))); solve([(h=(_r3_y+1))], _r3_y); fullratsimp(expand(((h-1)+(1/1)))); diff((_r3_x+1),_r3_x); diff((_r3_y+1),_r3_y); is(1<0); is(1<0); solve([(0=_r3_x)], _r3_x); solve([(0=_r3_y)], _r3_y); solve([(w=(_r3_x+1))], _r3_x); _tmp:fullratsimp(((w-1)+(1/1)))$ fullratsimp( (num(_tmp)+denom(_tmp)-1) / denom(_tmp) ); solve([(h=(_r3_y+1))], _r3_y); _tmp:fullratsimp(((h-1)+(1/1)))$ fullratsimp( (num(_tmp)+denom(_tmp)-1) / denom(_tmp) ); is(0>=0); is(w<=w); is(0>=0); is(h<=h); assume((_r3_x>=0)); assume((_r3_x<=w)); assume((_r3_y>=0)); assume((_r3_y<=h)); assume(equal(i,_r3_x)); assume(equal(j,_r3_y)); is(_r3_x<(_r3_x+1)); is(_r3_x>=_r3_x); is(_r3_y<(_r3_y+1)); is(_r3_y>=_r3_y); diff((_r3_x+1),_r3_x); diff((_r3_y+1),_r3_y); fullratsimp(expand((w-1))); fullratsimp(expand((h-1))); is(1<0); is(1<0); subst(0, _r3_x,_r3_x); subst(0, _r3_y,_r3_y); subst((w-1), _r3_x,(_r3_x+1)); subst((h-1), _r3_y,(_r3_y+1)); is(1<0); is(1<0); is(_r3_x<(_r3_x+1)); is(_r3_x>=_r3_x); is(_r3_y<(_r3_y+1)); is(_r3_y>=_r3_y); diff((_r3_x+1),_r3_x); diff((_r3_y+1),_r3_y); fullratsimp(expand((w-1))); fullratsimp(expand((h-1))); is(1<0); is(1<0); subst(0, _r3_x,_r3_x); subst(0, _r3_y,_r3_y); subst((w-1), _r3_x,(_r3_x+1)); subst((h-1), _r3_y,(_r3_y+1)); is(1<0); is(1<0); killcontext(_ctx_stack_2); is(equal(w,0)); is(equal(h,0)); killcontext(_ctx_stack_1); supcontext(_ctx_stack_1); assume((n>1000)); assume((n>1000)); assume((n>1000)); declare(n, integer); supcontext(_ctx_stack_2); is(0<0); is(0<0); is(0>=0); is(n<=n); is(0<0); is(0>=0); is(n<=inf); assume((_r4_x>=0)); assume((_r4_x<=n)); is(_r4_x=0); fullratsimp(expand((n-1))); is(0<0); is(0<0); fullratsimp(expand((n-1))); fullratsimp(expand((n-1))); is(_r4_x=0); fullratsimp(expand((n-1))); is(0<0); is(0<0); is(_r4_x=0); fullratsimp(expand((n-1))); is(0<0); is(0<0); killcontext(_ctx_stack_2); is(equal(n,0)); is(equal(n,0)); killcontext(_ctx_stack_1); supcontext(_ctx_stack_1); assume((n>1000)); assume((n>1000)); declare(n, integer); supcontext(_ctx_stack_2); is(0<0); is(0<0); is(0>=0); is(n<=inf); assume((_r5_x>=0)); assume((_r5_x<=n)); is(_r5_x=0); fullratsimp(expand((n-1))); is(0<0); is(0<0); is(_r5_x=0); fullratsimp(expand((n-1))); is(0<0); is(0<0); killcontext(_ctx_stack_2); is(equal(n,0)); killcontext(_ctx_stack_1); supcontext(_ctx_stack_1); assume((n>1000)); assume((n>1000)); declare(n, integer); supcontext(_ctx_stack_2); is(0<0); is(0<0); is(0>=0); is(n<=inf); assume((_r6_x>=0)); assume((_r6_x<=n)); is(_r6_x=0); fullratsimp(expand((n-1))); is(0<0); is(0<0); is(_r6_x=0); fullratsimp(expand((n-1))); is(0<0); is(0<0); killcontext(_ctx_stack_2); is(equal(n,0)); killcontext(_ctx_stack_1); supcontext(_ctx_stack_1); assume((n>1000)); assume((n>1000)); declare(n, integer); supcontext(_ctx_stack_2); is(0<0); is(0<0); is(0>=0); is(n<=inf); assume((_r7_x>=0)); assume((_r7_x<=n)); is(_r7_x=0); fullratsimp(expand((n-1))); is(0<0); is(0<0); is(_r7_x=0); fullratsimp(expand((n-1))); is(0<0); is(0<0); killcontext(_ctx_stack_2); is(equal(n,0)); killcontext(_ctx_stack_1); supcontext(_ctx_stack_1); assume((n>1000)); assume((n>1000)); assume((n>1000)); declare(n, integer); supcontext(_ctx_stack_2); is(0<0); is(0<0); is(0>=0); is(n<=n); is(0<0); is(0>=0); is(n<=inf); assume((_r8_x>=0)); assume((_r8_x<=n)); is(_r8_x=0); fullratsimp(expand((n-1))); is(0<0); is(0<0); fullratsimp(expand((n-1))); fullratsimp(expand((n-1))); is(_r8_x=0); fullratsimp(expand((n-1))); is(0<0); is(0<0); is(_r8_x=0); fullratsimp(expand((n-1))); is(0<0); is(0<0); killcontext(_ctx_stack_2); is(equal(n,0)); is(equal(n,0)); killcontext(_ctx_stack_1); supcontext(_ctx_stack_1); assume((n>1000)); assume((n>1000)); declare(n, integer); supcontext(_ctx_stack_2); is(0<0); is(0<0); is(0>=0); is(n<=inf); assume((_r9_x>=0)); assume((_r9_x<=n)); is(_r9_x=0); fullratsimp(expand((n-1))); is(0<0); is(0<0); is(_r9_x=0); fullratsimp(expand((n-1))); is(0<0); is(0<0); killcontext(_ctx_stack_2); is(equal(n,0)); killcontext(_ctx_stack_1); supcontext(_ctx_stack_1); assume((n1>1000)); assume((n2>1000)); assume(((n1+n2)>1000)); declare(Cutoff, integer); declare(n1, integer); declare(n2, integer); supcontext(_ctx_stack_2); is(0<0); is(0<0); is(0>=0); is((n1+n2)<=inf); is(0<0); is(0>=0); is((n1+n2)<=inf); assume((_r10_x>=0)); assume((_r10_x<=(n1+n2))); is(_r10_x=0); fullratsimp(expand(((n1+n2)-1))); is(0<0); is(0<0); is(_r10_x=0); fullratsimp(expand(((n1+n2)-1))); is(0<0); is(0<0); is(_r10_x<(n1+n2)); is(_r10_x>=0); fullratsimp(expand(((n1+n2)-1))); is(0<0); is(0<0); killcontext(_ctx_stack_2); fullratsimp(expand((n1+n2))); is(equal((n2+n1),0)); killcontext(_ctx_stack_1); supcontext(_ctx_stack_1); assume((n>1000)); assume((n>1000)); assume((n>1000)); declare(n, integer); supcontext(_ctx_stack_2); is(0<0); is(0<0); is(0>=0); is(n<=n); is(0<0); is(0>=0); is(n<=inf); assume((_r11_x>=0)); assume((_r11_x<=n)); is(_r11_x=0); fullratsimp(expand((n-1))); is(0<0); is(0<0); fullratsimp(expand((n-1))); fullratsimp(expand((n-1))); is(_r11_x=0); fullratsimp(expand((n-1))); is(0<0); is(0<0); is(_r11_x=0); fullratsimp(expand((n-1))); is(0<0); is(0<0); killcontext(_ctx_stack_2); is(equal(n,0)); is(equal(n,0)); killcontext(_ctx_stack_1); supcontext(_ctx_stack_1); assume((n>1000)); assume((n>1000)); declare(n, integer); supcontext(_ctx_stack_2); is(0<0); is(0<0); is(0>=0); is(n<=inf); assume((_r12_x>=0)); assume((_r12_x<=n)); is(_r12_x=0); fullratsimp(expand((n-1))); is(0<0); is(0<0); is(_r12_x=0); fullratsimp(expand((n-1))); is(0<0); is(0<0); killcontext(_ctx_stack_2); is(equal(n,0)); killcontext(_ctx_stack_1); supcontext(_ctx_stack_1); assume((n>1000)); assume((n>1000)); declare(n, integer); supcontext(_ctx_stack_2); is(0<0); is(0<0); is(0>=0); is(n<=inf); assume((_r13_x>=0)); assume((_r13_x<=n)); is(_r13_x=0); fullratsimp(expand((n-1))); is(0<0); is(0<0); is(_r13_x=0); fullratsimp(expand((n-1))); is(0<0); is(0<0); killcontext(_ctx_stack_2); is(equal(n,0)); killcontext(_ctx_stack_1); supcontext(_ctx_stack_1); assume((n>1000)); assume((n>1000)); assume((n>1000)); declare(n, integer); supcontext(_ctx_stack_2); is(0<0); is(0<0); is(0>=0); is(n<=n); is(0<0); is(0>=0); is(n<=inf); assume((_r14_x>=0)); assume((_r14_x<=n)); is(_r14_x=0); fullratsimp(expand((n-1))); is(0<0); is(0<0); fullratsimp(expand((n-1))); fullratsimp(expand((n-1))); is(_r14_x=0); fullratsimp(expand((n-1))); is(0<0); is(0<0); is(_r14_x=0); fullratsimp(expand((n-1))); is(0<0); is(0<0); killcontext(_ctx_stack_2); is(equal(n,0)); is(equal(n,0)); killcontext(_ctx_stack_1); supcontext(_ctx_stack_1); assume((n>1000)); assume((n>1000)); declare(n, integer); supcontext(_ctx_stack_2); is(0<0); is(0<0); is(0>=0); is(n<=inf); assume((_r15_x>=0)); assume((_r15_x<=n)); is(_r15_x=0); fullratsimp(expand((n-1))); is(0<0); is(0<0); is(_r15_x=0); fullratsimp(expand((n-1))); is(0<0); is(0<0); killcontext(_ctx_stack_2); is(equal(n,0)); killcontext(_ctx_stack_1); supcontext(_ctx_stack_1); assume((n>1000)); assume((n>1000)); assume((n>1000)); declare(n, integer); supcontext(_ctx_stack_2); is(0<0); is(0<0); is(0>=0); is(n<=n); is(0<0); is(0>=0); is(n<=inf); assume((_r16_x>=0)); assume((_r16_x<=n)); is(_r16_x=0); fullratsimp(expand((n-1))); is(0<0); is(0<0); fullratsimp(expand((n-1))); fullratsimp(expand((n-1))); is(_r16_x=0); fullratsimp(expand((n-1))); is(0<0); is(0<0); is(_r16_x=0); fullratsimp(expand((n-1))); is(0<0); is(0<0); killcontext(_ctx_stack_2); supcontext(_ctx_stack_2); is(0<0); is(0<0); is(0>=0); is(n<=n); is(0<0); is(0>=0); is(n<=inf); assume((_r17_x>=0)); assume((_r17_x<=n)); is(_r17_x=0); fullratsimp(expand((n-1))); is(0<0); is(0<0); fullratsimp(expand((n-1))); fullratsimp(expand((n-1))); is(_r17_x=0); fullratsimp(expand((n-1))); is(0<0); is(0<0); is(_r17_x=0); fullratsimp(expand((n-1))); is(0<0); is(0<0); killcontext(_ctx_stack_2); supcontext(_ctx_stack_2); is(0<0); is(0<0); is(0>=0); is(n<=n); is(0<0); is(0>=0); is(n<=inf); assume((_r18_x>=0)); assume((_r18_x<=n)); is(_r18_x=0); fullratsimp(expand((n-1))); is(0<0); is(0<0); fullratsimp(expand((n-1))); fullratsimp(expand((n-1))); is(_r18_x=0); fullratsimp(expand((n-1))); is(0<0); is(0<0); is(_r18_x=0); fullratsimp(expand((n-1))); is(0<0); is(0<0); killcontext(_ctx_stack_2); supcontext(_ctx_stack_2); is(0<0); is(0<0); is(0>=0); is(n<=n); is(0<0); is(0>=0); is(n<=inf); assume((_r19_x>=0)); assume((_r19_x<=n)); is(_r19_x=0); fullratsimp(expand((n-1))); is(0<0); is(0<0); fullratsimp(expand((n-1))); fullratsimp(expand((n-1))); is(_r19_x=0); fullratsimp(expand((n-1))); is(0<0); is(0<0); is(_r19_x=0); fullratsimp(expand((n-1))); is(0<0); is(0<0); killcontext(_ctx_stack_2); supcontext(_ctx_stack_2); is(0<0); is(0<0); is(0>=0); is(n<=n); is(0<0); is(0>=0); is(n<=inf); assume((_r20_x>=0)); assume((_r20_x<=n)); is(_r20_x=0); fullratsimp(expand((n-1))); is(0<0); is(0<0); fullratsimp(expand((n-1))); fullratsimp(expand((n-1))); is(_r20_x=0); fullratsimp(expand((n-1))); is(0<0); is(0<0); is(_r20_x=0); fullratsimp(expand((n-1))); is(0<0); is(0<0); killcontext(_ctx_stack_2); supcontext(_ctx_stack_2); is(0<0); is(0<0); is(0>=0); is(n<=n); is(0<0); is(0>=0); is(n<=inf); assume((_r21_x>=0)); assume((_r21_x<=n)); is(_r21_x=0); fullratsimp(expand((n-1))); is(0<0); is(0<0); fullratsimp(expand((n-1))); fullratsimp(expand((n-1))); is(_r21_x=0); fullratsimp(expand((n-1))); is(0<0); is(0<0); is(_r21_x=0); fullratsimp(expand((n-1))); is(0<0); is(0<0); killcontext(_ctx_stack_2); supcontext(_ctx_stack_2); is(0<0); is(0<0); is(0>=0); is(n<=n); is(0<0); is(0>=0); is(n<=inf); assume((_r22_x>=0)); assume((_r22_x<=n)); is(_r22_x=0); fullratsimp(expand((n-1))); is(0<0); is(0<0); fullratsimp(expand((n-1))); fullratsimp(expand((n-1))); is(_r22_x=0); fullratsimp(expand((n-1))); is(0<0); is(0<0); is(_r22_x=0); fullratsimp(expand((n-1))); is(0<0); is(0<0); killcontext(_ctx_stack_2); supcontext(_ctx_stack_2); is(0<0); is(0<0); is(0>=0); is(n<=n); is(0<0); is(0>=0); is(n<=inf); assume((_r23_x>=0)); assume((_r23_x<=n)); is(_r23_x=0); fullratsimp(expand((n-1))); is(0<0); is(0<0); fullratsimp(expand((n-1))); is(_r23_x=0); fullratsimp(expand((n-1))); is(0<0); is(0<0); is(_r23_x=0); fullratsimp(expand((n-1))); is(0<0); is(0<0); killcontext(_ctx_stack_2); is(equal(n,0)); is(equal(n,0)); killcontext(_ctx_stack_1); supcontext(_ctx_stack_1); assume((n>1000)); assume((n>1000)); declare(n, integer); supcontext(_ctx_stack_2); is(0<0); is(0<0); is(0>=0); is(n<=inf); assume((_r24_x>=0)); assume((_r24_x<=n)); is(_r24_x=0); fullratsimp(expand((n-1))); is(0<0); is(0<0); is(_r24_x=0); fullratsimp(expand((n-1))); is(0<0); is(0<0); killcontext(_ctx_stack_2); is(equal(n,0)); killcontext(_ctx_stack_1); supcontext(_ctx_stack_1); assume((n>1000)); assume((n>1000)); killcontext(_ctx_stack_1); supcontext(_ctx_stack_1); assume((w>1000)); assume((h>1000)); assume((d>1000)); assume((w>1000)); assume((h>1000)); assume((d>1000)); killcontext(_ctx_stack_1); supcontext(_ctx_stack_1); assume((w>1000)); assume((h>1000)); assume((w>1000)); assume((h>1000)); killcontext(_ctx_stack_1); supcontext(_ctx_stack_1); assume((n>1000)); assume((n>1000)); assume((n>1000)); killcontext(_ctx_stack_1); supcontext(_ctx_stack_1); assume((n>1000)); assume((n>1000)); killcontext(_ctx_stack_1); supcontext(_ctx_stack_1); assume((n>1000)); assume((n>1000)); killcontext(_ctx_stack_1); supcontext(_ctx_stack_1); assume((n>1000)); assume((n>1000)); killcontext(_ctx_stack_1); supcontext(_ctx_stack_1); assume((n>1000)); assume((n>1000)); assume((n>1000)); killcontext(_ctx_stack_1); supcontext(_ctx_stack_1); assume((n>1000)); assume((n>1000)); killcontext(_ctx_stack_1); supcontext(_ctx_stack_1); assume((n1>1000)); assume((n2>1000)); assume(((n1+n2)>1000)); is((n2+n1)<=0); is(0>=(n1+n2)); killcontext(_ctx_stack_1); supcontext(_ctx_stack_1); assume((n>1000)); assume((n>1000)); assume((n>1000)); killcontext(_ctx_stack_1); supcontext(_ctx_stack_1); assume((n>1000)); assume((n>1000)); killcontext(_ctx_stack_1); supcontext(_ctx_stack_1); assume((n>1000)); assume((n>1000)); killcontext(_ctx_stack_1); supcontext(_ctx_stack_1); assume((n>1000)); assume((n>1000)); assume((n>1000)); killcontext(_ctx_stack_1); supcontext(_ctx_stack_1); assume((n>1000)); assume((n>1000)); killcontext(_ctx_stack_1); supcontext(_ctx_stack_1); assume((n>1000)); assume((n>1000)); assume((n>1000)); killcontext(_ctx_stack_1); supcontext(_ctx_stack_1); assume((n>1000)); assume((n>1000)); killcontext(_ctx_stack_1); solve([(_tmp1=n)], n); fullratsimp(expand(((_r1_x+1)-_r1_x))); fullratsimp(expand(((_r1_x+1)-_r1_x))); solve([(_tmp3=n)], n); solve([(_tmp7=w)], w); solve([(_tmp8=h)], h); solve([(_tmp9=d)], d); fullratsimp(expand(((_r2_x+1)-_r2_x))); fullratsimp(expand(((_r2_y+1)-_r2_y))); fullratsimp(expand(((_r2_z+1)-_r2_z))); fullratsimp(expand(((_r2_x+1)-_r2_x))); fullratsimp(expand(((_r2_y+1)-_r2_y))); fullratsimp(expand(((_r2_z+1)-_r2_z))); solve([(_tmp13=w)], w); solve([(_tmp14=h)], h); solve([(_tmp15=d)], d); solve([(_tmp25=w)], w); solve([(_tmp26=h)], h); fullratsimp(expand(((_r3_x+1)-_r3_x))); fullratsimp(expand(((_r3_y+1)-_r3_y))); fullratsimp(expand(((_r3_x+1)-_r3_x))); fullratsimp(expand(((_r3_y+1)-_r3_y))); solve([(_tmp29=w)], w); solve([(_tmp30=h)], h); solve([(_tmp37=n)], n); fullratsimp(expand((n-0))); fullratsimp(expand((n-0))); solve([(_tmp40=n)], n); solve([(_tmp46=n)], n); fullratsimp(expand((n-0))); fullratsimp(expand((n-0))); solve([(_tmp48=n)], n); solve([(_tmp52=n)], n); fullratsimp(expand((n-0))); fullratsimp(expand((n-0))); solve([(_tmp54=n)], n); solve([(_tmp58=n)], n); fullratsimp(expand((n-0))); fullratsimp(expand((n-0))); solve([(_tmp60=n)], n); solve([(_tmp64=n)], n); fullratsimp(expand((n-0))); fullratsimp(expand((n-0))); solve([(_tmp67=n)], n); solve([(_tmp73=n)], n); fullratsimp(expand((n-0))); fullratsimp(expand((n-0))); solve([(_tmp75=n)], n); solve([(_tmp79=n1)], n1); solve([(_tmp80=n2)], n2); fullratsimp(expand(((n1+n2)-0))); fullratsimp(expand(((n1+n2)-0))); solve([(_tmp81=n1)], n1); solve([(_tmp82=n2)], n2); solve([(_tmp85=n)], n); fullratsimp(expand((n-0))); fullratsimp(expand((n-0))); solve([(_tmp88=n)], n); solve([(_tmp94=n)], n); fullratsimp(expand((n-0))); fullratsimp(expand((n-0))); solve([(_tmp96=n)], n); solve([(_tmp100=n)], n); fullratsimp(expand((n-0))); fullratsimp(expand((n-0))); solve([(_tmp102=n)], n); solve([(_tmp106=n)], n); fullratsimp(expand((n-0))); fullratsimp(expand((n-0))); solve([(_tmp108=n)], n); solve([(_tmp112=n)], n); fullratsimp(expand((n-0))); fullratsimp(expand((n-0))); solve([(_tmp114=n)], n); solve([(_tmp118=n)], n); fullratsimp(expand((n-0))); fullratsimp(expand((n-0))); solve([(_tmp120=n)], n); solve([(_tmp124=n)], n); fullratsimp(expand((n-0))); fullratsimp(expand((n-0))); solve([(_tmp126=n)], n); solve([(_tmp130=n)], n); fullratsimp(expand((n-0))); fullratsimp(expand((n-0))); solve([(_tmp133=n)], n); solve([(_tmp139=n)], n); fullratsimp(expand((n-0))); fullratsimp(expand((n-0))); solve([(_tmp142=n)], n); solve([(_tmp148=n)], n); fullratsimp(expand((n-0))); fullratsimp(expand((n-0))); solve([(_tmp151=n)], n); solve([(_tmp157=n)], n); fullratsimp(expand((n-0))); fullratsimp(expand((n-0))); solve([(_tmp160=n)], n); solve([(_tmp166=n)], n); fullratsimp(expand((n-0))); fullratsimp(expand((n-0))); solve([(_tmp169=n)], n); solve([(_tmp175=n)], n); fullratsimp(expand((n-0))); fullratsimp(expand((n-0))); solve([(_tmp177=n)], n); solve([(_tmp181=n)], n); fullratsimp(expand((n-0))); fullratsimp(expand((n-0))); solve([(_tmp183=n)], n); solve([(_tmp187=n)], n); fullratsimp(expand((n-0))); fullratsimp(expand((n-0))); solve([(_tmp189=n)], n); solve([(_tmp193=n)], n); fullratsimp(expand((n-0))); fullratsimp(expand((n-0))); solve([(_tmp195=n)], n); solve([(_tmp199=n)], n); fullratsimp(expand((n-0))); fullratsimp(expand((n-0))); solve([(_tmp201=n)], n); solve([(_tmp205=n)], n); fullratsimp(expand((n-0))); fullratsimp(expand((n-0))); fullratsimp(expand((n-0))); fullratsimp(expand((n-0))); fullratsimp(expand((n-0))); fullratsimp(expand((n-0))); fullratsimp(expand((n-0))); fullratsimp(expand((n-0))); fullratsimp(expand((n-0))); fullratsimp(expand((n-0))); fullratsimp(expand((n-0))); fullratsimp(expand((n-0))); fullratsimp(expand((n-0))); fullratsimp(expand((n-0))); fullratsimp(expand((n-0))); fullratsimp(expand((n-0))); solve([(_tmp208=n)], n); solve([(_tmp214=n)], n); fullratsimp(expand((n-0))); fullratsimp(expand((n-0))); solve([(_tmp216=n)], n);