int calculate_output(int);
extern void __VERIFIER_error(void);
extern int __VERIFIER_nondet_int(void);
extern void exit(int);

	// inputs
	int inputC = 3;
	int inputD = 4;
	int inputE = 5;
	int inputF = 6;
	int inputB = 2;


	 int a1 = 23;
	 int a19 = 9;
	 int a10 = 0;
	 int a12 = 0;
	 int a4 = 14;

	int calculate_output(int input) {
		if((((((a10==4) && (a12==0)) &&   ((38 < a1) && (218 >= a1)) ) && (a4==14)) && (a19==8))){
		error_57: exit(0);
		}
		if((((((a10==2) && (a12==0)) &&   ((-13 < a1) && (38 >= a1)) ) && (a4==14)) && (a19==8))){
		error_48: exit(0);
		}
		if((((((a10==0) && (a12==0)) &&  a1 <=  -13 ) && (a4==14)) && (a19==6))){
		globalError: exit(0);
		}
		if((((((a10==2) && (a12==0)) &&  218 < a1 ) && (a4==14)) && (a19==8))){
		error_50: exit(0);
		}
		if((((((a10==4) && (a12==0)) &&  a1 <=  -13 ) && (a4==14)) && (a19==6))){
		error_15: exit(0);
		}
		if((((((a10==2) && (a12==0)) &&   ((-13 < a1) && (38 >= a1)) ) && (a4==14)) && (a19==7))){
		error_28: exit(0);
		}
		if((((((a10==3) && (a12==0)) &&   ((-13 < a1) && (38 >= a1)) ) && (a4==14)) && (a19==6))){
		error_12: exit(0);
		}
		if((((((a10==4) && (a12==0)) &&  218 < a1 ) && (a4==14)) && (a19==8))){
		error_58: exit(0);
		}
		if((((((a10==1) && (a12==0)) &&   ((-13 < a1) && (38 >= a1)) ) && (a4==14)) && (a19==7))){
		error_24: exit(0);
		}
		if((((((a10==2) && (a12==0)) &&   ((38 < a1) && (218 >= a1)) ) && (a4==14)) && (a19==7))){
		error_29: exit(0);
		}
		if((((((a10==1) && (a12==0)) &&  218 < a1 ) && (a4==14)) && (a19==7))){
		error_26: exit(0);
		}
		if((((((a10==0) && (a12==0)) &&  218 < a1 ) && (a4==14)) && (a19==8))){
		error_42: exit(0);
		}
		if((((((a10==4) && (a12==0)) &&  a1 <=  -13 ) && (a4==14)) && (a19==8))){
		error_55: exit(0);
		}
		if((((((a10==2) && (a12==0)) &&  a1 <=  -13 ) && (a4==14)) && (a19==8))){
		error_47: exit(0);
		}
		if((((((a10==0) && (a12==0)) &&   ((38 < a1) && (218 >= a1)) ) && (a4==14)) && (a19==8))){
		error_41: exit(0);
		}
		if((((((a10==1) && (a12==0)) &&  218 < a1 ) && (a4==14)) && (a19==8))){
		error_46: exit(0);
		}
		if((((((a10==2) && (a12==0)) &&   ((38 < a1) && (218 >= a1)) ) && (a4==14)) && (a19==8))){
		error_49: exit(0);
		}
		if((((((a10==4) && (a12==0)) &&   ((-13 < a1) && (38 >= a1)) ) && (a4==14)) && (a19==8))){
		error_56: exit(0);
		}
		if((((((a10==1) && (a12==0)) &&  218 < a1 ) && (a4==14)) && (a19==6))){
		error_6: exit(0);
		}
		if((((((a10==3) && (a12==0)) &&   ((-13 < a1) && (38 >= a1)) ) && (a4==14)) && (a19==7))){
		error_32: exit(0);
		}
		if((((((a10==0) && (a12==0)) &&  a1 <=  -13 ) && (a4==14)) && (a19==8))){
		error_39: exit(0);
		}
		if((((((a10==0) && (a12==0)) &&   ((38 < a1) && (218 >= a1)) ) && (a4==14)) && (a19==7))){
		error_21: exit(0);
		}
		if((((((a10==0) && (a12==0)) &&   ((-13 < a1) && (38 >= a1)) ) && (a4==14)) && (a19==7))){
		error_20: exit(0);
		}
		if((((((a10==0) && (a12==0)) &&  a1 <=  -13 ) && (a4==14)) && (a19==7))){
		error_19: exit(0);
		}
		if((((((a10==4) && (a12==0)) &&   ((38 < a1) && (218 >= a1)) ) && (a4==14)) && (a19==6))){
		error_17: exit(0);
		}
		if((((((a10==3) && (a12==0)) &&  218 < a1 ) && (a4==14)) && (a19==6))){
		error_14: exit(0);
		}
		if((((((a10==4) && (a12==0)) &&  218 < a1 ) && (a4==14)) && (a19==7))){
		error_38: exit(0);
		}
		if((((((a10==4) && (a12==0)) &&   ((-13 < a1) && (38 >= a1)) ) && (a4==14)) && (a19==6))){
		error_16: exit(0);
		}
		if((((((a10==2) && (a12==0)) &&  218 < a1 ) && (a4==14)) && (a19==7))){
		error_30: exit(0);
		}
		if((((((a10==1) && (a12==0)) &&  a1 <=  -13 ) && (a4==14)) && (a19==8))){
		error_43: exit(0);
		}
		if((((((a10==1) && (a12==0)) &&  a1 <=  -13 ) && (a4==14)) && (a19==6))){
		error_3: exit(0);
		}
		if((((((a10==0) && (a12==0)) &&  218 < a1 ) && (a4==14)) && (a19==7))){
		error_22: exit(0);
		}
		if((((((a10==1) && (a12==0)) &&   ((38 < a1) && (218 >= a1)) ) && (a4==14)) && (a19==8))){
		error_45: exit(0);
		}
		if((((((a10==4) && (a12==0)) &&   ((-13 < a1) && (38 >= a1)) ) && (a4==14)) && (a19==7))){
		error_36: exit(0);
		}
		if((((((a10==2) && (a12==0)) &&   ((-13 < a1) && (38 >= a1)) ) && (a4==14)) && (a19==6))){
		error_8: exit(0);
		}
		if((((((a10==3) && (a12==0)) &&   ((-13 < a1) && (38 >= a1)) ) && (a4==14)) && (a19==8))){
		error_52: exit(0);
		}
		if((((((a10==3) && (a12==0)) &&   ((38 < a1) && (218 >= a1)) ) && (a4==14)) && (a19==8))){
		error_53: exit(0);
		}
		if((((((a10==3) && (a12==0)) &&  a1 <=  -13 ) && (a4==14)) && (a19==7))){
		error_31: exit(0);
		}
		if((((((a10==3) && (a12==0)) &&   ((38 < a1) && (218 >= a1)) ) && (a4==14)) && (a19==7))){
		error_33: exit(0);
		}
		if((((((a10==2) && (a12==0)) &&  a1 <=  -13 ) && (a4==14)) && (a19==6))){
		error_7: exit(0);
		}
		if((((((a10==1) && (a12==0)) &&  a1 <=  -13 ) && (a4==14)) && (a19==7))){
		error_23: __VERIFIER_error();
		}
		if((((((a10==0) && (a12==0)) &&   ((-13 < a1) && (38 >= a1)) ) && (a4==14)) && (a19==6))){
		error_0: exit(0);
		}
		if((((((a10==2) && (a12==0)) &&  218 < a1 ) && (a4==14)) && (a19==6))){
		error_10: exit(0);
		}
		if((((((a10==0) && (a12==0)) &&   ((-13 < a1) && (38 >= a1)) ) && (a4==14)) && (a19==8))){
		error_40: exit(0);
		}
		if((((((a10==3) && (a12==0)) &&  a1 <=  -13 ) && (a4==14)) && (a19==8))){
		error_51: exit(0);
		}
		if((((((a10==4) && (a12==0)) &&  a1 <=  -13 ) && (a4==14)) && (a19==7))){
		error_35: exit(0);
		}
		if((((((a10==1) && (a12==0)) &&   ((38 < a1) && (218 >= a1)) ) && (a4==14)) && (a19==6))){
		error_5: exit(0);
		}
		if((((((a10==0) && (a12==0)) &&   ((38 < a1) && (218 >= a1)) ) && (a4==14)) && (a19==6))){
		error_1: exit(0);
		}
		if((((((a10==4) && (a12==0)) &&   ((38 < a1) && (218 >= a1)) ) && (a4==14)) && (a19==7))){
		error_37: exit(0);
		}
		if((((((a10==3) && (a12==0)) &&   ((38 < a1) && (218 >= a1)) ) && (a4==14)) && (a19==6))){
		error_13: exit(0);
		}
		if((((((a10==2) && (a12==0)) &&   ((38 < a1) && (218 >= a1)) ) && (a4==14)) && (a19==6))){
		error_9: exit(0);
		}
		if((((((a10==1) && (a12==0)) &&   ((-13 < a1) && (38 >= a1)) ) && (a4==14)) && (a19==8))){
		error_44: exit(0);
		}
		if((((((a10==4) && (a12==0)) &&  218 < a1 ) && (a4==14)) && (a19==6))){
		error_18: exit(0);
		}
		if((((((a10==0) && (a12==0)) &&  218 < a1 ) && (a4==14)) && (a19==6))){
		error_2: exit(0);
		}
		if((((((a10==2) && (a12==0)) &&  a1 <=  -13 ) && (a4==14)) && (a19==7))){
		error_27: exit(0);
		}
		if((((((a10==3) && (a12==0)) &&  a1 <=  -13 ) && (a4==14)) && (a19==6))){
		error_11: exit(0);
		}
		if((((((a10==3) && (a12==0)) &&  218 < a1 ) && (a4==14)) && (a19==8))){
		error_54: exit(0);
		}
		if((((((a10==3) && (a12==0)) &&  218 < a1 ) && (a4==14)) && (a19==7))){
		error_34: exit(0);
		}
		if((((((a10==1) && (a12==0)) &&   ((38 < a1) && (218 >= a1)) ) && (a4==14)) && (a19==7))){
		error_25: exit(0);
		}
		if((((((a10==0) && (a12==0)) &&  a1 <=  -13 ) && (a4==14)) && (a19==9))){
		error_59: exit(0);
		}
		if((((((a10==1) && (a12==0)) &&   ((-13 < a1) && (38 >= a1)) ) && (a4==14)) && (a19==6))){
		error_4: exit(0);
		}

	    if((((a10==4) && ( 218 < a1  && (((input == 4) && (a12==0)) && (a4==14)))) && (a19==9))){

	    		a10 = 1; 

	    	 return 24;
	    } else if(((a4==14) && (((a12==0) && (((  ((-13 < a1) && (38 >= a1))  ||   ((38 < a1) && (218 >= a1)) ) && (input == 4)) && (a19==9))) && (a10==0)))){
	    	a1 = (((a1 + -15535) - 211896) / 5);
	    		a10 = 2; 

	    	 return 22;
	    } else if(((((a4==14) && ((a19==10) && ((a10==1) && (input == 2)))) && (a12==0)) &&  218 < a1 )){

	    		a19 = 9; 

	    	 return 22;
	    } else if(((a12==0) && ((a19==9) && ((a10==1) && (( 218 < a1  && (input == 3)) && (a4==14)))))){

	    		a19 = 10; 

	    	 return 25;
	    } else if(((a19==10) && (((a4==14) && (((((a10==0) &&   ((38 < a1) && (218 >= a1)) ) || ((a10==0) &&  218 < a1 )) || ((a10==1) &&  a1 <=  -13 )) && (input == 5))) && (a12==0)))){
	    	a1 = (((((a1 - 0) * 9)/ 10) % 25)- -12);
	    		a10 = 2; 
	    		a19 = 8; 

	    	 return -1;
	    } else if(((a12==0) && ((a19==9) && (((a4==14) && ((input == 2) && (  ((-13 < a1) && (38 >= a1))  ||   ((38 < a1) && (218 >= a1)) ))) && (a10==3))))){
	    	a1 = (((a1 + 513169) / 5) - -374179);
	    		a10 = 0; 

	    	 return 26;
	    } else if(((a12==0) && ((((a4==14) && ((input == 3) && ( a1 <=  -13  ||   ((-13 < a1) && (38 >= a1)) ))) && (a10==2)) && (a19==9)))){
	    	a1 = (((((a1 % 299993)+ -300005) * 1) + 533674) - 533676);
	    	 return 22;
	    } else if((((a12==0) && (  ((-13 < a1) && (38 >= a1))  && (((input == 3) && (a19==10)) && (a4==14)))) && (a10==1))){
	    	a1 = ((((a1 - -221565) * 10)/ 9) / 5);
	    		a19 = 9; 

	    	 return 22;
	    } else if((((a19==9) && (((input == 6) && (( 218 < a1  && (a10==0)) || ( a1 <=  -13  && (a10==1)))) && (a4==14))) && (a12==0))){
	    	a1 = (((((a1 % 25)- -13) - 42605) / 5) - -8517);
	    		a10 = 3; 

	    	 return 26;
	    } else if((  ((38 < a1) && (218 >= a1))  && (((a4==14) && ((a19==10) && ((a10==1) && (input == 4)))) && (a12==0)))){
	    	a1 = ((((a1 * 57)/ 10) * 5) * 5);
	    		a19 = 9; 

	    	 return 24;
	    } else if((((a4==14) && ((((  ((-13 < a1) && (38 >= a1))  ||   ((38 < a1) && (218 >= a1)) ) && (input == 5)) && (a19==9)) && (a12==0))) && (a10==0))){
	    	a1 = (((a1 / 5) + 110755) + 220746);
	    		a10 = 1; 
	    		a19 = 8; 

	    	 return -1;
	    } else if((((a4==14) && ((((((a10==2) &&   ((38 < a1) && (218 >= a1)) ) || ((a10==2) &&  218 < a1 )) || ( a1 <=  -13  && (a10==3))) && (input == 2)) && (a19==9))) && (a12==0))){
	    	a1 = (((((a1 % 299890)- -300108) + 0) + -140588) + 140590);
	    		a10 = 0; 

	    	 return 26;
	    } else if((((a10==1) && (((a12==0) && ((input == 6) && (  ((-13 < a1) && (38 >= a1))  ||   ((38 < a1) && (218 >= a1)) ))) && (a4==14))) && (a19==9))){
	    	a1 = ((((a1 / 5) - -367248) * 1) - 890938);
	    		a10 = 0; 
	    		a19 = 10; 

	    	 return 26;
	    } else if(((((((input == 5) && (a4==14)) &&  218 < a1 ) && (a10==4)) && (a19==9)) && (a12==0))){
	    	a1 = (((((a1 % 25)+ -8) * 5) % 25)+ 13);
	    		a10 = 1; 
	    		a19 = 7; 

	    	 return -1;
	    } else if(((a19==10) && ((a4==14) && ((a12==0) && ((input == 4) && ((((a10==0) &&   ((38 < a1) && (218 >= a1)) ) || ( 218 < a1  && (a10==0))) || ((a10==1) &&  a1 <=  -13 ))))))){
	    	a1 = ((((a1 % 299993)- 300005) * 1) + -3);
	    		a10 = 2; 
	    		a19 = 9; 

	    	 return 24;
	    } else if((((a12==0) && ((((a19==9) && (input == 4)) &&  218 < a1 ) && (a10==1))) && (a4==14))){

	    	 return 22;
	    } else if(((a10==1) && ((a4==14) && ((((a12==0) && (input == 2)) && (a19==9)) &&  218 < a1 )))){
	    	a1 = ((((((a1 % 89)+ 74) - -21) * 5) % 89)- -118);
	    		a19 = 10; 

	    	 return 25;
	    } else if((((a4==14) && (((input == 4) && (((  ((38 < a1) && (218 >= a1))  && (a10==2)) || ((a10==2) &&  218 < a1 )) || ( a1 <=  -13  && (a10==3)))) && (a19==9))) && (a12==0))){
	    	a1 = (((a1 / 5) - -435872) + 13710);
	    		a10 = 0; 

	    	 return -1;
	    } else if(((((a12==0) && ((((a10==0) &&  218 < a1 ) || ((a10==1) &&  a1 <=  -13 )) && (input == 2))) && (a19==9)) && (a4==14))){
	    	a1 = ((((((a1 * 9)/ 10) % 299993)+ -300005) / 5) + -75819);
	    		a10 = 4; 

	    	 return 26;
	    } else if((((a4==14) && ((a12==0) && ((input == 3) && (((a10==3) &&  218 < a1 ) || ( a1 <=  -13  && (a10==4)))))) && (a19==9))){
	    	a1 = ((((a1 - 0) - 0) / 5) - 247106);
	    		a10 = 4; 

	    	 return -1;
	    } else if((((((a10==1) && ((a12==0) && (input == 6))) && (a19==10)) &&   ((-13 < a1) && (38 >= a1)) ) && (a4==14))){
	    	a1 = (((a1 / 5) - 367764) - -191971);
	    		a10 = 2; 
	    		a19 = 9; 

	    	 return 24;
	    } else if(((a19==9) && (((a10==4) && ( 218 < a1  && ((a4==14) && (input == 6)))) && (a12==0)))){

	    		a19 = 8; 

	    	 return -1;
	    } else if((((a10==0) && ((a12==0) && (((input == 4) && ( a1 <=  -13  ||   ((-13 < a1) && (38 >= a1)) )) && (a19==10)))) && (a4==14))){
	    	a1 = ((((a1 % 25)+ 13) / 5) - -2);
	    	 return 26;
	    } else if(((a19==9) && ((((a4==14) && ((input == 2) && ( a1 <=  -13  ||   ((-13 < a1) && (38 >= a1)) ))) && (a12==0)) && (a10==2)))){
	    	a1 = ((((a1 % 299993)+ -300005) * 1) + -1);
	    	 return 25;
	    } else if((((((a12==0) && ((input == 4) && (  ((-13 < a1) && (38 >= a1))  ||   ((38 < a1) && (218 >= a1)) ))) && (a19==9)) && (a4==14)) && (a10==3))){
	    	a1 = (((a1 * 5) - 196556) + 94277);
	    	 return -1;
	    } else if((((a4==14) && (((a12==0) && ( 218 < a1  && (input == 6))) && (a19==10))) && (a10==1))){
	    	a1 = (((a1 - 600149) - 12) + -58);
	    	 return -1;
	    } else if(((((((input == 2) && ( a1 <=  -13  ||   ((-13 < a1) && (38 >= a1)) )) && (a19==10)) && (a10==0)) && (a4==14)) && (a12==0))){
	    	a1 = ((((a1 % 299890)+ 300108) - -1) + 0);
	    		a10 = 4; 
	    		a19 = 9; 

	    	 return -1;
	    } else if((((((( 218 < a1  && (a10==0)) || ((a10==1) &&  a1 <=  -13 )) && (input == 3)) && (a4==14)) && (a12==0)) && (a19==9))){
	    	a1 = ((((((a1 / 5) % 25)+ 13) * 5) % 25)- -12);
	    		a10 = 4; 

	    	 return 22;
	    } else if(((a12==0) && ((a19==9) && (((input == 6) && (((a10==3) &&  218 < a1 ) || ( a1 <=  -13  && (a10==4)))) && (a4==14))))){
	    	a1 = ((((a1 + 0) % 299890)+ 300108) + 0);
	    		a10 = 2; 

	    	 return -1;
	    } else if((((a10==3) && (((a19==9) && ((  ((-13 < a1) && (38 >= a1))  ||   ((38 < a1) && (218 >= a1)) ) && (input == 5))) && (a12==0))) && (a4==14))){
	    	a1 = ((((a1 - 287698) - 189392) % 89)+ 206);
	    		a10 = 2; 
	    		a19 = 7; 

	    	 return -1;
	    } else if((((a12==0) && ((a10==1) && ( 218 < a1  && ((a19==9) && (input == 6))))) && (a4==14))){

	    	 return 24;
	    } else if(((a10==0) && ((a12==0) && (((( a1 <=  -13  ||   ((-13 < a1) && (38 >= a1)) ) && (input == 3)) && (a19==10)) && (a4==14))))){
	    	a1 = (((((a1 % 25)+ 13) - 1) + -16025) - -16025);
	    	 return -1;
	    } else if((((a10==4) && ((((  ((-13 < a1) && (38 >= a1))  ||   ((38 < a1) && (218 >= a1)) ) && (input == 4)) && (a4==14)) && (a19==9))) && (a12==0))){
	    	a1 = (((((a1 - -249982) + 317100) * 1) % 89)- -62);
	    	 return -1;
	    } else if(((a4==14) && ((a10==1) && ((a19==9) && ((a12==0) && ((  ((-13 < a1) && (38 >= a1))  ||   ((38 < a1) && (218 >= a1)) ) && (input == 4))))))){
	    	a1 = ((((a1 - 46038) + -455425) * 10)/ 9);
	    		a19 = 10; 

	    	 return 24;
	    } else if(((a4==14) && ((a19==9) && (((( a1 <=  -13  && (a10==3)) || ((  ((38 < a1) && (218 >= a1))  && (a10==2)) || ((a10==2) &&  218 < a1 ))) && (input == 3)) && (a12==0))))){
	    	a1 = ((((a1 % 299890)- -300108) + 1) * 1);
	    		a10 = 0; 

	    	 return -1;
	    } else if((((((a4==14) && ((input == 6) && (a10==1))) && (a12==0)) &&   ((38 < a1) && (218 >= a1)) ) && (a19==10))){
	    	a1 = (((a1 - -320095) * 1) - -173480);
	    		a19 = 9; 

	    	 return -1;
	    } else if(((a4==14) && (((a12==0) && ( 218 < a1  && ((a19==9) && (input == 3)))) && (a10==4)))){

	    	 return 24;
	    } else if((((a4==14) && ((a12==0) && ((((a10==3) &&  218 < a1 ) || ((a10==4) &&  a1 <=  -13 )) && (input == 4)))) && (a19==9))){
	    	a1 = ((((a1 % 89)+ 128) + -1) - 0);
	    		a10 = 3; 

	    	 return -1;
	    } else if((((a12==0) && (((a10==4) && ((  ((-13 < a1) && (38 >= a1))  ||   ((38 < a1) && (218 >= a1)) ) && (input == 3))) && (a4==14))) && (a19==9))){
	    	a1 = ((((a1 + -121822) * 4) * 10)/ -9);
	    		a10 = 3; 

	    	 return -1;
	    } else if(((a19==9) && ((a4==14) && (((input == 5) && (((  ((38 < a1) && (218 >= a1))  && (a10==2)) || ((a10==2) &&  218 < a1 )) || ((a10==3) &&  a1 <=  -13 ))) && (a12==0))))){
	    	a1 = ((((a1 % 299890)- -300108) + 2) + 0);
	    		a10 = 2; 

	    	 return 21;
	    } else if(((a12==0) && (((a19==9) && ((((a10==0) &&  218 < a1 ) || ( a1 <=  -13  && (a10==1))) && (input == 5))) && (a4==14)))){
	    	a1 = ((((a1 % 299993)- 300005) + -1) - 1);
	    		a10 = 3; 

	    	 return 21;
	    } else if(( 218 < a1  && ((((a12==0) && ((a19==9) && (input == 2))) && (a10==4)) && (a4==14)))){

	    		a10 = 1; 

	    	 return 22;
	    } else if((((a12==0) && ((a19==9) && ((((a10==3) &&  a1 <=  -13 ) || (((a10==2) &&   ((38 < a1) && (218 >= a1)) ) || ( 218 < a1  && (a10==2)))) && (input == 6)))) && (a4==14))){
	    	a1 = ((((a1 - 0) % 299890)- -300108) - -1);
	    		a10 = 2; 

	    	 return -1;
	    } else if(((a19==9) && ((a12==0) && (((( a1 <=  -13  ||   ((-13 < a1) && (38 >= a1)) ) && (input == 5)) && (a4==14)) && (a10==2))))){
	    	a1 = ((((a1 % 299890)+ 300108) * 1) * 1);
	    		a10 = 0; 
	    		a19 = 8; 

	    	 return -1;
	    } else if((((a10==1) && (((a12==0) && ((a19==10) && (input == 4))) &&   ((-13 < a1) && (38 >= a1)) )) && (a4==14))){
	    	a1 = (((a1 - -575828) - -5011) + 9014);
	    		a19 = 9; 

	    	 return 24;
	    } else if(((a12==0) && ((a4==14) && ( 218 < a1  && (((a10==1) && (input == 4)) && (a19==10)))))){
	    	a1 = (((((a1 * 9)/ 10) * -1)/ 10) * 5);
	    		a10 = 2; 
	    		a19 = 9; 

	    	 return 24;
	    } else if(((((((input == 3) && (  ((-13 < a1) && (38 >= a1))  ||   ((38 < a1) && (218 >= a1)) )) && (a10==0)) && (a19==9)) && (a4==14)) && (a12==0))){
	    	a1 = ((((a1 / 5) * 5) / 5) + 505228);
	    		a10 = 1; 

	    	 return 25;
	    } else if((((a4==14) && (((( a1 <=  -13  && (a10==1)) || (((a10==0) &&   ((38 < a1) && (218 >= a1)) ) || ( 218 < a1  && (a10==0)))) && (input == 6)) && (a19==10))) && (a12==0))){
	    	a1 = (((((a1 * 9)/ 10) % 299993)+ -300005) - 1);
	    		a10 = 2; 
	    		a19 = 9; 

	    	 return 24;
	    } else if(((a19==9) && ((((input == 4) && (( 218 < a1  && (a10==0)) || ((a10==1) &&  a1 <=  -13 ))) && (a12==0)) && (a4==14)))){
	    	a1 = (((((a1 / 5) % 89)- -128) / 5) + 34);
	    		a10 = 0; 
	    		a19 = 8; 

	    	 return -1;
	    } else if((((a19==10) && ((a12==0) && ((((a10==1) &&  a1 <=  -13 ) || ((  ((38 < a1) && (218 >= a1))  && (a10==0)) || ((a10==0) &&  218 < a1 ))) && (input == 3)))) && (a4==14))){
	    	a1 = ((((a1 % 299993)- 300005) - 0) - 2);
	    		a10 = 2; 
	    		a19 = 9; 

	    	 return 22;
	    } else if(((a19==9) && (((a4==14) && ((((a10==3) &&  218 < a1 ) || ( a1 <=  -13  && (a10==4))) && (input == 5))) && (a12==0)))){
	    	a1 = ((((((a1 % 25)- -12) - 0) * 5) % 25)- -13);
	    		a10 = 3; 
	    		a19 = 6; 

	    	 return -1;
	    } else if((((a12==0) && ((((input == 5) && (a19==10)) &&   ((38 < a1) && (218 >= a1)) ) && (a4==14))) && (a10==1))){
	    	a1 = ((((a1 + 381077) % 25)- -1) / 5);
	    		a10 = 2; 
	    		a19 = 7; 

	    	 return -1;
	    } else if(((a19==9) && ((a4==14) && ((((  ((-13 < a1) && (38 >= a1))  ||   ((38 < a1) && (218 >= a1)) ) && (input == 3)) && (a10==1)) && (a12==0))))){
	    	a1 = (((a1 / 5) + 105416) + 61704);
	    		a10 = 4; 

	    	 return 24;
	    } else if(((a10==0) && ((a12==0) && ((((input == 5) && ( a1 <=  -13  ||   ((-13 < a1) && (38 >= a1)) )) && (a19==10)) && (a4==14))))){
	    	a1 = (((((a1 % 299890)+ 300108) - -1) + -309315) - -309317);
	    		a10 = 1; 
	    		a19 = 7; 

	    	 return -1;
	    } else if(( 218 < a1  && (((((input == 3) && (a10==1)) && (a12==0)) && (a4==14)) && (a19==10)))){
	    	a1 = ((((a1 % 25)- 10) - 1) / 5);
	    		a10 = 0; 

	    	 return -1;
	    } else if((((a12==0) && ((a19==9) && (((input == 3) && (  ((-13 < a1) && (38 >= a1))  ||   ((38 < a1) && (218 >= a1)) )) && (a4==14)))) && (a10==3))){
	    	a1 = ((((a1 - -133866) + -357620) / 5) + 265622);
	    		a10 = 0; 

	    	 return -1;
	    } else if((((((a4==14) && (  ((38 < a1) && (218 >= a1))  && (input == 2))) && (a12==0)) && (a10==1)) && (a19==10))){
	    	a1 = ((((a1 * 10)/ -9) * 5) - 333686);
	    		a10 = 4; 
	    		a19 = 6; 

	    	 return -1;
	    } else if((((a19==10) && ((a10==1) && ((a12==0) && (  ((-13 < a1) && (38 >= a1))  && (input == 5))))) && (a4==14))){
	    	a1 = (((a1 + -283353) / 5) + -495232);
	    		a10 = 0; 
	    		a19 = 6; 

	    	 return -1;
	    } else if(((((a10==1) && (((input == 5) &&  218 < a1 ) && (a4==14))) && (a19==10)) && (a12==0))){
	    	a1 = (((((a1 % 89)- -93) * 5) % 89)- -56);
	    		a10 = 4; 
	    		a19 = 8; 

	    	 return -1;
	    } else if((((a4==14) && ((a19==9) && ((input == 2) && (((a10==3) &&  218 < a1 ) || ((a10==4) &&  a1 <=  -13 ))))) && (a12==0))){
	    	a1 = ((((a1 % 299993)+ -300005) - 1) - 1);
	    		a10 = 1; 

	    	 return -1;
	    } else if((((a4==14) && (((a19==9) && ((  ((-13 < a1) && (38 >= a1))  ||   ((38 < a1) && (218 >= a1)) ) && (input == 2))) && (a12==0))) && (a10==4))){
	    	a1 = (((((a1 % 89)+ 129) - 1134) * -1)/ 10);
	    		a10 = 3; 

	    	 return -1;
	    } else if(((a4==14) && (((a19==9) && (((  ((-13 < a1) && (38 >= a1))  ||   ((38 < a1) && (218 >= a1)) ) && (input == 6)) && (a10==3))) && (a12==0)))){
	    	a1 = (((a1 - 559222) + -11915) - 28339);
	    		a10 = 1; 

	    	 return -1;
	    } else if((((a4==14) && ((((input == 6) && ( a1 <=  -13  ||   ((-13 < a1) && (38 >= a1)) )) && (a19==10)) && (a12==0))) && (a10==0))){
	    	a1 = (((((a1 + 0) % 299993)- 300005) / 5) - 292229);
	    	 return -1;
	    } else if(((a12==0) && ((a4==14) && (((( a1 <=  -13  && (a10==1)) || (((a10==0) &&   ((38 < a1) && (218 >= a1)) ) || ( 218 < a1  && (a10==0)))) && (input == 2)) && (a19==10))))){
	    	a1 = ((((a1 % 25)+ 12) - -2) / 5);
	    		a10 = 2; 
	    		a19 = 9; 

	    	 return 22;
	    } else if((((a12==0) && ((a19==9) && ((a10==2) && ((input == 6) && ( a1 <=  -13  ||   ((-13 < a1) && (38 >= a1)) ))))) && (a4==14))){
	    	a1 = ((((a1 / 5) % 25)+ 13) / 5);
	    	 return 25;
	    } else if(((a4==14) && ((a19==9) && ((a12==0) && (((input == 2) && (  ((-13 < a1) && (38 >= a1))  ||   ((38 < a1) && (218 >= a1)) )) && (a10==0)))))){
	    	a1 = (((a1 * 5) + 278443) - -239546);
	    	 return 26;
	    } else if(((a19==9) && (((a10==1) && ((a12==0) && ((input == 2) && (  ((-13 < a1) && (38 >= a1))  ||   ((38 < a1) && (218 >= a1)) )))) && (a4==14)))){
	    	a1 = (((((a1 * 5) + 59655) * 5) % 25)+ 12);
	    		a19 = 10; 

	    	 return 26;
	    } else if(((a19==9) && ((a4==14) && ((a10==1) && (((input == 5) && (  ((-13 < a1) && (38 >= a1))  ||   ((38 < a1) && (218 >= a1)) )) && (a12==0)))))){
	    	a1 = (((a1 + -438195) * 1) * 1);
	    		a10 = 2; 
	    		a19 = 8; 

	    	 return -1;
	    } else if(((a12==0) && (((((input == 6) && (  ((-13 < a1) && (38 >= a1))  ||   ((38 < a1) && (218 >= a1)) )) && (a19==9)) && (a4==14)) && (a10==0)))){
	    	a1 = (((((a1 + -272193) - -47605) - -570122) % 89)+ 110);
	    		a10 = 1; 

	    	 return 25;
	    } else if(((a4==14) && (((a12==0) && ((a19==9) && ((input == 6) && (  ((-13 < a1) && (38 >= a1))  ||   ((38 < a1) && (218 >= a1)) )))) && (a10==4)))){
	    	a1 = (((((a1 - 44798) + -168742) * 2) % 89)+ 207);
	    	 return -1;
	    } else if((((((  ((38 < a1) && (218 >= a1))  && (input == 3)) && (a10==1)) && (a12==0)) && (a4==14)) && (a19==10))){
	    	a1 = ((((a1 * 5) - -287099) - 723016) + 616783);
	    		a10 = 4; 
	    		a19 = 9; 

	    	 return -1;
	    } else if((((a4==14) && (((( a1 <=  -13  ||   ((-13 < a1) && (38 >= a1)) ) && (input == 4)) && (a12==0)) && (a19==9))) && (a10==2))){
	    	a1 = ((((a1 % 299993)- 300005) * 1) - 3);
	    	 return 24;
	    } else if(((a12==0) && ((( 218 < a1  && ((a19==9) && (input == 5))) && (a10==1)) && (a4==14)))){
	    	a1 = ((((a1 * 9)/ 10) + 58620) - 603783);
	    		a10 = 4; 
	    		a19 = 8; 

	    	 return -1;
	    } else if(((a4==14) && (((((  ((-13 < a1) && (38 >= a1))  ||   ((38 < a1) && (218 >= a1)) ) && (input == 5)) && (a12==0)) && (a19==9)) && (a10==4)))){
	    	a1 = (((a1 + 566454) + 1842) + 23814);
	    		a10 = 2; 
	    		a19 = 8; 

	    	 return -1;
	    } else if(((a12==0) && ((((a10==1) && (  ((-13 < a1) && (38 >= a1))  && (input == 2))) && (a4==14)) && (a19==10)))){

	    	 return 26;
	    } 
	    return -2;
	}

int main()
{
    // default output
    int output = -1;

    // main i/o-loop
    while(1)
    {
        // read input
        int input;
        input = __VERIFIER_nondet_int();
        if ((input != 2) && (input != 3) && (input != 4) && (input != 5) && (input != 6)) return -2;

        // operate eca engine
        output = calculate_output(input);
    }
}