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

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


	 int a21 = 7;
	 int a15 = 8;
	 int a12 = -49;
	 int a24 = 1;

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

	    if((((a24==1) && (  ((11 < a12) && (80 >= a12))  && ((input == 5) && (a15==8)))) && (a21==9))){
	    	a12 = ((((a12 + 555500) * -1)/ 10) * 5);
	    		a15 = 5; 
	    		a21 = 6; 

	    	 return -1;
	    } else if((((a15==9) && ((((a21==9) || ((a21==7) || (a21==8))) && (input == 5)) &&  a12 <=  -43 )) && (a24==1))){

	    		a15 = 5; 
	    		a21 = 6; 

	    	 return -1;
	    } else if(((a15==9) && ((  ((-43 < a12) && (11 >= a12))  && ((a24==1) && (input == 2))) && (a21==8)))){
	    	a12 = (((a12 - -571629) / 5) + -404132);
	    		a15 = 5; 
	    		a21 = 6; 

	    	 return -1;
	    } else if(((a24==1) && ((a15==8) && (  ((11 < a12) && (80 >= a12))  && ((input == 1) && ((a21==7) || (a21==8))))))){
	    	a12 = (((a12 - 268644) + -323718) + -3883);
	    		a15 = 5; 
	    		a21 = 6; 

	    	 return -1;
	    } else if((((((a21==10) && ( 80 < a12  && (a15==8))) || (((a15==9) &&  a12 <=  -43 ) && (a21==6))) && (input == 2)) && (a24==1))){
	    	a12 = (((a12 / 5) + -345781) / 5);
	    		a15 = 5; 
	    		a21 = 6; 

	    	 return -1;
	    } else if(((a24==1) && ((a15==9) && ((((a21==6) &&  80 < a12 ) || (((a21==9) &&   ((11 < a12) && (80 >= a12)) ) || (  ((11 < a12) && (80 >= a12))  && (a21==10)))) && (input == 5))))){
	    	a12 = (((((a12 % 34)+ 23) - -139662) - 547970) - -408298);
	    		a15 = 6; 
	    		a21 = 6; 

	    	 return -1;
	    } else if((( a12 <=  -43  && ((((a21==9) || ((a21==7) || (a21==8))) && (input == 4)) && (a24==1))) && (a15==9))){

	    		a15 = 5; 
	    		a21 = 6; 

	    	 return -1;
	    } else if((((((input == 2) && (a24==1)) &&   ((11 < a12) && (80 >= a12)) ) && (a21==9)) && (a15==8))){
	    	a12 = (((a12 - -334333) + 32000) / 5);
	    		a21 = 8; 

	    	 return 22;
	    } else if((((((  ((-43 < a12) && (11 >= a12))  && (a21==10)) || (  ((11 < a12) && (80 >= a12))  && (a21==6))) && (input == 2)) && (a24==1)) && (a15==8))){
	    	a12 = ((((a12 - 438298) * 1) + 564710) - 684902);
	    		a15 = 5; 
	    		a21 = 6; 

	    	 return -1;
	    } else if(((a15==9) && (((input == 1) && ((( a12 <=  -43  && (a21==10)) || ((a21==6) &&   ((-43 < a12) && (11 >= a12)) )) || (  ((-43 < a12) && (11 >= a12))  && (a21==7)))) && (a24==1)))){
	    	a12 = ((((a12 % 299978)+ -300020) * 1) - 3);
	    		a15 = 5; 
	    		a21 = 6; 

	    	 return -1;
	    } else if((((a24==1) && (((input == 6) && ((a21==7) || (a21==8))) &&  80 < a12 )) && (a15==9))){

	    		a21 = 9; 

	    	 return 26;
	    } else if((  ((-43 < a12) && (11 >= a12))  && ((a15==9) && ((a24==1) && (((a21==9) || (a21==10)) && (input == 2)))))){

	    		a15 = 6; 
	    		a21 = 9; 

	    	 return -1;
	    } else if((((((input == 5) && (a15==8)) &&   ((-43 < a12) && (11 >= a12)) ) && (a21==9)) && (a24==1))){

	    		a21 = 10; 

	    	 return 24;
	    } else if((( 80 < a12  && ((a15==8) && (((a21==8) || (a21==9)) && (input == 3)))) && (a24==1))){
	    	a12 = ((((a12 * -6)/ 10) - 40423) + -165586);
	    		a15 = 5; 
	    		a21 = 6; 

	    	 return -1;
	    } else if(((input == 4) && ((((a15==9) && ((a24==1) &&  80 < a12 )) && (a21==10)) || ((a21==6) && ((a15==5) && ((a24==2) &&  a12 <=  -43 )))))){
	    	a12 = ((((a12 / 5) % 26)+ -16) + 1);
	    		a24 = 1; 
	    		a15 = 6; 
	    		a21 = 10; 

	    	 return -1;
	    } else if(((((a24==1) && ((input == 3) &&  a12 <=  -43 )) && (a21==7)) && (a15==8))){

	    		a15 = 5; 
	    		a21 = 6; 

	    	 return -1;
	    } else if(((a24==1) && (((( 80 < a12  && (a15==8)) && (a21==10)) || (((a15==9) &&  a12 <=  -43 ) && (a21==6))) && (input == 3)))){
	    	a12 = ((((a12 - 0) - 0) / 5) + -200550);
	    		a15 = 5; 
	    		a21 = 6; 

	    	 return -1;
	    } else if((((a24==1) && ((a15==9) && (((a21==7) || (a21==8)) && (input == 3)))) &&  80 < a12 )){
	    	a12 = ((((a12 * 9)/ 10) / 5) + -505559);
	    		a15 = 7; 
	    		a21 = 10; 

	    	 return -1;
	    } else if((((((((a21==8) || (a21==9)) || (a21==10)) && (input == 5)) &&  a12 <=  -43 ) && (a15==8)) && (a24==1))){

	    		a15 = 5; 
	    		a21 = 6; 

	    	 return -1;
	    } else if(((((a15==9) && ((input == 1) && (a21==8))) && (a24==1)) &&   ((-43 < a12) && (11 >= a12)) )){
	    	a12 = (((a12 + -386239) - 148442) - -217864);
	    		a15 = 5; 
	    		a21 = 6; 

	    	 return -1;
	    } else if((((((((a21==8) || (a21==9)) || (a21==10)) && (input == 3)) && (a15==8)) &&  a12 <=  -43 ) && (a24==1))){

	    		a15 = 5; 
	    		a21 = 6; 

	    	 return -1;
	    } else if(((a24==1) && (((a15==8) && ((input == 1) && (a21==9))) &&   ((11 < a12) && (80 >= a12)) ))){
	    	a12 = (((a12 / 5) + -16723) / 5);
	    		a15 = 5; 
	    		a21 = 6; 

	    	 return -1;
	    } else if(((a15==9) && ( 80 < a12  && ((a24==1) && (((a21==7) || (a21==8)) && (input == 4)))))){

	    		a15 = 7; 
	    		a21 = 10; 

	    	 return -1;
	    } else if(( 80 < a12  && ((a15==9) && (((input == 2) && ((a21==7) || (a21==8))) && (a24==1))))){
	    	a12 = (((((a12 * 9)/ 10) / 5) * 10)/ -3);
	    		a15 = 6; 
	    		a21 = 9; 

	    	 return -1;
	    } else if((((((input == 6) &&   ((11 < a12) && (80 >= a12)) ) && (a21==9)) && (a15==8)) && (a24==1))){
	    	a12 = (((a12 + -285349) + -46510) + -209836);
	    		a15 = 5; 
	    		a21 = 6; 

	    	 return -1;
	    } else if(((((a24==1) && ((input == 1) && ((a21==8) || ((a21==6) || (a21==7))))) && (a15==9)) &&   ((11 < a12) && (80 >= a12)) )){

	    		a15 = 6; 
	    		a21 = 8; 

	    	 return -1;
	    } else if(((((a21==10) && (( 80 < a12  && (a24==1)) && (a15==9))) || (((a15==5) && ((a24==2) &&  a12 <=  -43 )) && (a21==6))) && (input == 3))){
	    	a12 = ((((a12 % 26)- 15) + 426288) + -426288);
	    		a24 = 1; 
	    		a15 = 7; 
	    		a21 = 6; 

	    	 return -1;
	    } else if(((((((a21==7) &&   ((-43 < a12) && (11 >= a12)) ) || (((a21==10) &&  a12 <=  -43 ) || (  ((-43 < a12) && (11 >= a12))  && (a21==6)))) && (input == 5)) && (a24==1)) && (a15==9))){
	    	a12 = ((((a12 % 299978)- 300020) + -1) + -1);
	    		a15 = 5; 
	    		a21 = 6; 

	    	 return -1;
	    } else if((((((input == 1) && (((a21==7) || (a21==8)) || (a21==9))) && (a15==9)) &&  a12 <=  -43 ) && (a24==1))){

	    		a15 = 5; 
	    		a21 = 6; 

	    	 return -1;
	    } else if(((a15==9) && ((a24==1) && (((input == 6) &&   ((-43 < a12) && (11 >= a12)) ) && (a21==8))))){
	    	a12 = (((a12 * 5) / 5) + -316852);
	    		a15 = 5; 
	    		a21 = 6; 

	    	 return -1;
	    } else if((((a24==1) && ((a15==9) && ((input == 5) && ((a21==8) || ((a21==6) || (a21==7)))))) &&   ((11 < a12) && (80 >= a12)) )){

	    		a15 = 5; 
	    		a21 = 8; 

	    	 return -1;
	    } else if(((((a15==8) && ((((a21==6) || (a21==7)) || (a21==8)) && (input == 5))) &&   ((-43 < a12) && (11 >= a12)) ) && (a24==1))){
	    	a12 = (((a12 - 529036) / 5) * 5);
	    		a15 = 5; 
	    		a21 = 6; 

	    	 return -1;
	    } else if(((a15==9) && ((((input == 3) && (((a21==6) || (a21==7)) || (a21==8))) && (a24==1)) &&   ((11 < a12) && (80 >= a12)) ))){
	    	a12 = ((((((a12 * 10)/ -2) * 5) - -29976) * -1)/ 10);
	    		a15 = 7; 
	    		a21 = 6; 

	    	 return -1;
	    } else if(((  ((-43 < a12) && (11 >= a12))  && ((a15==8) && (((a21==8) || ((a21==6) || (a21==7))) && (input == 3)))) && (a24==1))){
	    	a12 = (((a12 - 239513) * 2) - 118149);
	    		a15 = 5; 
	    		a21 = 6; 

	    	 return -1;
	    } else if(((a15==9) && ((a24==1) && ((((a21==9) || (a21==10)) && (input == 5)) &&   ((-43 < a12) && (11 >= a12)) )))){
	    	a12 = (((a12 + -382503) - -833715) - -74843);
	    		a15 = 5; 
	    		a21 = 6; 

	    	 return -1;
	    } else if((  ((11 < a12) && (80 >= a12))  && (((a24==1) && ((((a21==6) || (a21==7)) || (a21==8)) && (input == 4))) && (a15==9)))){

	    		a15 = 5; 
	    		a21 = 10; 

	    	 return -1;
	    } else if(((a15==9) && ((a24==1) && (((input == 6) &&  80 < a12 ) && (a21==9))))){
	    	a12 = (((((a12 - 600066) * 1) / 5) * 34)/ 10);
	    		a15 = 7; 
	    		a21 = 8; 

	    	 return -1;
	    } else if((((a24==1) && (((input == 2) && ((a21==10) || ((a21==8) || (a21==9)))) &&  a12 <=  -43 )) && (a15==8))){

	    		a15 = 5; 
	    		a21 = 6; 

	    	 return -1;
	    } else if(((a24==1) && (((input == 4) && ((  ((-43 < a12) && (11 >= a12))  && (a21==7)) || (( a12 <=  -43  && (a21==10)) || (  ((-43 < a12) && (11 >= a12))  && (a21==6))))) && (a15==9)))){
	    	a12 = (((((a12 % 299978)+ -300020) - 3) - -109194) + -109193);
	    		a15 = 5; 
	    		a21 = 6; 

	    	 return -1;
	    } else if((((((input == 6) && ((a21==9) || ((a21==7) || (a21==8)))) && (a24==1)) && (a15==9)) &&  a12 <=  -43 )){

	    		a15 = 5; 
	    		a21 = 6; 

	    	 return -1;
	    } else if(((( a12 <=  -43  && ((input == 6) && ((a21==10) || ((a21==8) || (a21==9))))) && (a24==1)) && (a15==8))){
	    	a12 = ((((a12 % 26)+ -1) / 5) / 5);
	    		a21 = 7; 

	    	 return 25;
	    } else if((((((a21==7) && (input == 5)) &&  a12 <=  -43 ) && (a24==1)) && (a15==8))){

	    		a21 = 10; 

	    	 return 22;
	    } else if((((a15==9) && ((((a21==9) || (a21==10)) && (input == 4)) &&   ((-43 < a12) && (11 >= a12)) )) && (a24==1))){
	    	a12 = (((a12 / 5) + 176111) * 3);
	    		a15 = 7; 
	    		a21 = 9; 

	    	 return -1;
	    } else if(((((( 80 < a12  && (a24==1)) && (a15==9)) && (a21==10)) || ((( a12 <=  -43  && (a24==2)) && (a15==5)) && (a21==6))) && (input == 2))){
	    	a12 = (((((a12 % 299959)- -300039) / 5) / 5) + 204292);
	    		a24 = 1; 
	    		a15 = 9; 
	    		a21 = 9; 

	    	 return -1;
	    } else if((((  ((-43 < a12) && (11 >= a12))  && (((a21==9) || (a21==10)) && (input == 3))) && (a15==9)) && (a24==1))){
	    	a12 = (((a12 + 66) - 3) + -2);
	    		a21 = 8; 

	    	 return 21;
	    } else if((((a15==8) && ( 80 < a12  && (((a21==8) || (a21==9)) && (input == 6)))) && (a24==1))){
	    	a12 = ((((a12 + 0) * 9)/ 10) - 558346);
	    		a15 = 5; 
	    		a21 = 6; 

	    	 return -1;
	    } else if((((((( a12 <=  -43  && (a21==10)) || (  ((-43 < a12) && (11 >= a12))  && (a21==6))) || ((a21==7) &&   ((-43 < a12) && (11 >= a12)) )) && (input == 3)) && (a24==1)) && (a15==9))){
	    	a12 = (((a12 + 101173) / 5) - 185122);
	    		a15 = 5; 
	    		a21 = 6; 

	    	 return -1;
	    } else if(((a24==1) && ((input == 1) && (((a21==10) && ((a15==8) &&  80 < a12 )) || (( a12 <=  -43  && (a15==9)) && (a21==6)))))){
	    	a12 = ((((a12 % 299978)+ -300020) * 1) - 2);
	    		a15 = 5; 
	    		a21 = 6; 

	    	 return -1;
	    } else if(((  ((-43 < a12) && (11 >= a12))  && ((a24==1) && (((a21==8) || ((a21==6) || (a21==7))) && (input == 1)))) && (a15==8))){

	    		a21 = 9; 

	    	 return 21;
	    } else if((((a24==1) && ( a12 <=  -43  && ((((a21==7) || (a21==8)) || (a21==9)) && (input == 3)))) && (a15==9))){

	    		a21 = 10; 

	    	 return 22;
	    } else if((((a24==1) && ((input == 4) && ((((a21==9) &&   ((11 < a12) && (80 >= a12)) ) || ((a21==10) &&   ((11 < a12) && (80 >= a12)) )) || ((a21==6) &&  80 < a12 )))) && (a15==9))){
	    	a12 = (((((a12 * 9)/ 10) - 589907) - -649897) + -606113);
	    		a15 = 7; 
	    		a21 = 7; 

	    	 return -1;
	    } else if(((a15==8) && (((a21==7) && ((input == 2) && (a24==1))) &&  a12 <=  -43 ))){

	    		a15 = 5; 
	    		a21 = 6; 

	    	 return -1;
	    } else if(((a15==8) && (((input == 4) && ((  ((-43 < a12) && (11 >= a12))  && (a21==10)) || ((a21==6) &&   ((11 < a12) && (80 >= a12)) ))) && (a24==1)))){
	    	a12 = ((((a12 - 357209) * 1) - -928336) - 1022569);
	    		a15 = 5; 
	    		a21 = 6; 

	    	 return -1;
	    } else if(((a15==9) && (( a12 <=  -43  && (((a21==9) || ((a21==7) || (a21==8))) && (input == 2))) && (a24==1)))){

	    		a15 = 5; 
	    		a21 = 6; 

	    	 return -1;
	    } else if(((a24==1) && ((a15==8) && ((((a21==10) &&   ((-43 < a12) && (11 >= a12)) ) || (  ((11 < a12) && (80 >= a12))  && (a21==6))) && (input == 3))))){
	    	a12 = (((a12 + 60189) + -305530) + -244668);
	    		a15 = 5; 
	    		a21 = 6; 

	    	 return -1;
	    } else if((((a15==8) && (((a24==1) && (input == 4)) &&   ((11 < a12) && (80 >= a12)) )) && (a21==9))){
	    	a12 = (((a12 - 310903) + -128009) + -1314);
	    		a15 = 5; 
	    		a21 = 6; 

	    	 return -1;
	    } else if(((((input == 6) && (((  ((11 < a12) && (80 >= a12))  && (a21==9)) || (  ((11 < a12) && (80 >= a12))  && (a21==10))) || ( 80 < a12  && (a21==6)))) && (a24==1)) && (a15==9))){
	    	a12 = ((((a12 % 299959)- -81) - -194202) - -92066);
	    		a21 = 7; 

	    	 return 26;
	    } else if((((a15==8) && ((((a21==10) &&   ((-43 < a12) && (11 >= a12)) ) || (  ((11 < a12) && (80 >= a12))  && (a21==6))) && (input == 6))) && (a24==1))){
	    	a12 = (((a12 / 5) - 557506) - 18416);
	    		a15 = 5; 
	    		a21 = 6; 

	    	 return -1;
	    } else if(((((a24==1) && (((a21==8) || ((a21==6) || (a21==7))) && (input == 2))) && (a15==9)) &&   ((11 < a12) && (80 >= a12)) )){
	    	a12 = ((((a12 - -582271) - 436382) - 442400) - -391873);
	    		a21 = 6; 

	    	 return 22;
	    } else if((((a21==9) && (((input == 3) && (a24==1)) &&  80 < a12 )) && (a15==9))){

	    	 return -1;
	    } else if(((((((a21==7) || (a21==8)) && (input == 1)) && (a15==9)) &&  80 < a12 ) && (a24==1))){
	    	a12 = ((((a12 / 5) % 26)+ -33) / 5);
	    		a15 = 5; 
	    		a21 = 10; 

	    	 return -1;
	    } else if((((((a15==9) && ( 80 < a12  && (a24==1))) && (a21==10)) || ((a21==6) && (((a24==2) &&  a12 <=  -43 ) && (a15==5)))) && (input == 6))){
	    	a12 = (((((a12 % 299959)- -300039) + -252537) * 1) - -252539);
	    		a24 = 1; 
	    		a15 = 9; 
	    		a21 = 7; 

	    	 return -1;
	    } else if(((a15==9) && ((a21==9) && ( 80 < a12  && ((input == 2) && (a24==1)))))){

	    		a21 = 8; 

	    	 return -1;
	    } else if(((((a15==8) && (((a21==7) || (a21==8)) && (input == 3))) && (a24==1)) &&   ((11 < a12) && (80 >= a12)) )){
	    	a12 = ((((a12 / 5) + -439847) * 10)/ 9);
	    		a15 = 5; 
	    		a21 = 6; 

	    	 return -1;
	    } else if(((a24==1) && ((input == 5) && ((((a15==8) &&  80 < a12 ) && (a21==10)) || ((a21==6) && ( a12 <=  -43  && (a15==9))))))){
	    	a12 = ((((a12 % 299959)- -300039) * 1) * 1);
	    		a15 = 8; 
	    		a21 = 10; 

	    	 return 26;
	    } else if(((a24==1) && (((( 80 < a12  && (a21==6)) || (((a21==9) &&   ((11 < a12) && (80 >= a12)) ) || ((a21==10) &&   ((11 < a12) && (80 >= a12)) ))) && (input == 1)) && (a15==9)))){
	    	a12 = (((((a12 * 9)/ 10) * 1) + -581502) + 599190);
	    		a15 = 7; 
	    		a21 = 8; 

	    	 return -1;
	    } else if((((a24==1) && ( a12 <=  -43  && ((((a21==8) || (a21==9)) || (a21==10)) && (input == 1)))) && (a15==8))){

	    		a15 = 5; 
	    		a21 = 6; 

	    	 return -1;
	    } else if(((a24==1) && (((((a21==7) &&   ((-43 < a12) && (11 >= a12)) ) || (((a21==10) &&  a12 <=  -43 ) || ((a21==6) &&   ((-43 < a12) && (11 >= a12)) ))) && (input == 6)) && (a15==9)))){
	    	a12 = ((((a12 % 299978)+ -300020) / 5) + -174067);
	    		a15 = 5; 
	    		a21 = 6; 

	    	 return -1;
	    } else if(((a15==8) && (((a24==1) && ((((a21==6) || (a21==7)) || (a21==8)) && (input == 2))) &&   ((-43 < a12) && (11 >= a12)) ))){
	    	a12 = (((((a12 - 185217) - 149574) - -494599) * -1)/ 10);
	    		a15 = 5; 
	    		a21 = 6; 

	    	 return -1;
	    } else if((((((input == 6) && (((a21==6) || (a21==7)) || (a21==8))) && (a15==8)) && (a24==1)) &&   ((-43 < a12) && (11 >= a12)) )){
	    	a12 = (((a12 * 5) - 432359) / 5);
	    		a15 = 5; 
	    		a21 = 6; 

	    	 return -1;
	    } else if(((a24==1) && (((((a21==7) || (a21==8)) && (input == 6)) && (a15==8)) &&   ((11 < a12) && (80 >= a12)) ))){
	    	a12 = ((((a12 / 5) - 526582) * 10)/ 9);
	    		a15 = 5; 
	    		a21 = 6; 

	    	 return -1;
	    } else if((((((  ((-43 < a12) && (11 >= a12))  && (a21==7)) || (((a21==10) &&  a12 <=  -43 ) || (  ((-43 < a12) && (11 >= a12))  && (a21==6)))) && (input == 2)) && (a15==9)) && (a24==1))){
	    	a12 = (((((a12 % 26)- 16) + 343661) - 46416) - 297244);
	    		a21 = 8; 

	    	 return 25;
	    } else if(((  ((-43 < a12) && (11 >= a12))  && (((input == 1) && (a15==8)) && (a24==1))) && (a21==9))){
	    	a12 = (((a12 * 5) * 5) + -84619);
	    		a15 = 5; 
	    		a21 = 6; 

	    	 return -1;
	    } else if(((a24==1) && ((a15==9) && ((input == 2) && (( 80 < a12  && (a21==6)) || ((  ((11 < a12) && (80 >= a12))  && (a21==9)) || (  ((11 < a12) && (80 >= a12))  && (a21==10)))))))){
	    	a12 = ((((a12 % 299959)- -81) * 1) * 1);
	    		a15 = 6; 
	    		a21 = 9; 

	    	 return -1;
	    } else if(((a24==1) && ((a15==8) && (((input == 2) && ((a21==7) || (a21==8))) &&   ((11 < a12) && (80 >= a12)) )))){
	    	a12 = ((((a12 + -453921) * 10)/ 9) - 34620);
	    		a15 = 5; 
	    		a21 = 6; 

	    	 return -1;
	    } else if(((a24==1) && ((a21==9) && (((input == 5) && (a15==9)) &&  80 < a12 )))){

	    		a15 = 7; 
	    		a21 = 6; 

	    	 return -1;
	    } else if((( a12 <=  -43  && (((input == 1) && (a21==7)) && (a24==1))) && (a15==8))){

	    		a15 = 5; 
	    		a21 = 6; 

	    	 return -1;
	    } else if((((a21==9) && ((  ((11 < a12) && (80 >= a12))  && (input == 3)) && (a24==1))) && (a15==8))){
	    	a12 = (((a12 - -195021) - 451510) / 5);
	    		a15 = 5; 
	    		a21 = 6; 

	    	 return -1;
	    } else if((((a15==8) && ((((a21==8) || (a21==9)) && (input == 2)) && (a24==1))) &&  80 < a12 )){
	    	a12 = ((((a12 * 9)/ 10) + -545656) * 1);
	    		a15 = 5; 
	    		a21 = 6; 

	    	 return -1;
	    } else if((( 80 < a12  && ((a24==1) && (((a21==8) || (a21==9)) && (input == 4)))) && (a15==8))){
	    	a12 = ((((a12 * 9)/ 10) + -562768) / 5);
	    		a15 = 5; 
	    		a21 = 6; 

	    	 return -1;
	    } else if(((a21==9) && ((a15==9) && ((a24==1) && ( 80 < a12  && (input == 1)))))){

	    	 return 26;
	    } else if(((a15==8) && (((input == 3) && ((((a21==10) &&   ((11 < a12) && (80 >= a12)) ) || ((a21==6) &&  80 < a12 )) || ( 80 < a12  && (a21==7)))) && (a24==1)))){
	    	a12 = ((((a12 % 299978)+ -300020) + -247081) * 1);
	    		a15 = 5; 
	    		a21 = 6; 

	    	 return -1;
	    } else if(((a24==1) && ( 80 < a12  && ((a21==9) && ((a15==9) && (input == 4)))))){
	    	a12 = ((((a12 + 0) + -318749) % 34)+ 45);
	    		a15 = 5; 

	    	 return -1;
	    } else if(((a15==8) && (((input == 6) && (( 80 < a12  && (a21==7)) || (((a21==10) &&   ((11 < a12) && (80 >= a12)) ) || ( 80 < a12  && (a21==6))))) && (a24==1)))){
	    	a12 = ((((a12 % 299978)- 300020) - 166783) * 1);
	    		a15 = 5; 
	    		a21 = 6; 

	    	 return -1;
	    } else if(((a15==9) && ((a24==1) && (  ((-43 < a12) && (11 >= a12))  && ((input == 1) && ((a21==9) || (a21==10))))))){
	    	a12 = (((((a12 - -56) * 9)/ 10) / 5) + 56);
	    		a15 = 5; 
	    		a21 = 7; 

	    	 return -1;
	    } else if(((((( 80 < a12  && (a15==8)) && (a21==10)) || ((a21==6) && ((a15==9) &&  a12 <=  -43 ))) && (input == 6)) && (a24==1))){
	    	a12 = ((((a12 % 299978)- 300020) * 1) + -2);
	    		a15 = 5; 
	    		a21 = 6; 

	    	 return -1;
	    } else if(((((a15==8) && (((a21==8) || (a21==9)) && (input == 1))) && (a24==1)) &&  80 < a12 )){
	    	a12 = ((((a12 - 94512) / 5) / 5) + -533466);
	    		a15 = 5; 
	    		a21 = 6; 

	    	 return -1;
	    } else if((((a24==1) && ((((a21==7) &&  80 < a12 ) || ((  ((11 < a12) && (80 >= a12))  && (a21==10)) || ((a21==6) &&  80 < a12 ))) && (input == 2))) && (a15==8))){
	    	a12 = ((((a12 % 299978)- 300020) + 525887) + -618409);
	    		a15 = 5; 
	    		a21 = 6; 

	    	 return -1;
	    } else if(((a24==1) && (  ((-43 < a12) && (11 >= a12))  && (((((a21==6) || (a21==7)) || (a21==8)) && (input == 4)) && (a15==8))))){
	    	a12 = ((((a12 - 87828) * 10)/ 9) - 284434);
	    		a15 = 5; 
	    		a21 = 6; 

	    	 return -1;
	    } else if((((a15==8) && (((a21==7) && (input == 4)) && (a24==1))) &&  a12 <=  -43 )){

	    		a15 = 5; 
	    		a21 = 6; 

	    	 return -1;
	    } else if(((a21==9) && (((a24==1) && ((input == 2) &&   ((-43 < a12) && (11 >= a12)) )) && (a15==8)))){
	    	a12 = (((a12 - -61) - -3) - -1);
	    		a21 = 8; 

	    	 return 26;
	    } else if(((a15==8) && ((  ((-43 < a12) && (11 >= a12))  && ((a21==9) && (input == 4))) && (a24==1)))){
	    	a12 = (((a12 + -564241) - 3500) * 1);
	    		a15 = 5; 
	    		a21 = 6; 

	    	 return -1;
	    } else if((( a12 <=  -43  && ((((a21==10) || ((a21==8) || (a21==9))) && (input == 4)) && (a15==8))) && (a24==1))){

	    		a15 = 5; 
	    		a21 = 6; 

	    	 return -1;
	    } else if(((a24==1) && ((a15==8) && ((input == 4) && (( 80 < a12  && (a21==7)) || ((  ((11 < a12) && (80 >= a12))  && (a21==10)) || ( 80 < a12  && (a21==6)))))))){
	    	a12 = (((((a12 % 299959)- -81) * 1) / 5) + 165863);
	    		a21 = 10; 

	    	 return 22;
	    } else if((  ((11 < a12) && (80 >= a12))  && ((a15==8) && ((a24==1) && (((a21==7) || (a21==8)) && (input == 4)))))){
	    	a12 = (((a12 + -256944) - 53297) - 113637);
	    		a15 = 5; 
	    		a21 = 6; 

	    	 return -1;
	    } else if(((((((a15==8) &&  80 < a12 ) && (a21==10)) || ((a21==6) && ( a12 <=  -43  && (a15==9)))) && (input == 4)) && (a24==1))){
	    	a12 = (((a12 / 5) + -409994) + 99019);
	    		a15 = 5; 
	    		a21 = 6; 

	    	 return -1;
	    } else if(((((( 80 < a12  && (a24==1)) && (a15==9)) && (a21==10)) || ((( a12 <=  -43  && (a24==2)) && (a15==5)) && (a21==6))) && (input == 1))){
	    	a12 = ((((((a12 % 299978)- 300020) / 5) + 194993) * -1)/ 10);
	    		a24 = 1; 
	    		a15 = 5; 
	    		a21 = 9; 

	    	 return -1;
	    } else if((((a15==8) && ((((  ((11 < a12) && (80 >= a12))  && (a21==10)) || ( 80 < a12  && (a21==6))) || ( 80 < a12  && (a21==7))) && (input == 5))) && (a24==1))){
	    	a12 = (((((a12 + -334090) % 299978)+ -300020) / 5) + -383582);
	    		a15 = 5; 
	    		a21 = 6; 

	    	 return -1;
	    } else if(((a21==9) && ((((input == 6) && (a15==8)) &&   ((-43 < a12) && (11 >= a12)) ) && (a24==1)))){
	    	a12 = (((((a12 + 423400) * 1) * 1) * -1)/ 10);
	    		a15 = 5; 
	    		a21 = 6; 

	    	 return -1;
	    } else if(((a24==1) && ((a21==9) && (  ((-43 < a12) && (11 >= a12))  && ((a15==8) && (input == 3)))))){
	    	a12 = (((a12 + -295946) + -243936) * 1);
	    		a15 = 5; 
	    		a21 = 6; 

	    	 return -1;
	    } else if(((a15==9) && (((input == 3) && (((a21==6) &&  80 < a12 ) || (((a21==9) &&   ((11 < a12) && (80 >= a12)) ) || ((a21==10) &&   ((11 < a12) && (80 >= a12)) )))) && (a24==1)))){
	    	a12 = ((((((a12 % 299959)+ 81) - 332928) / 5) * -1)/ 10);
	    		a15 = 5; 
	    		a21 = 10; 

	    	 return -1;
	    } else if(( a12 <=  -43  && ((a21==7) && ((a24==1) && ((a15==8) && (input == 6)))))){

	    		a15 = 5; 
	    		a21 = 6; 

	    	 return -1;
	    } else if((  ((-43 < a12) && (11 >= a12))  && ((((input == 3) && (a24==1)) && (a21==8)) && (a15==9)))){
	    	a12 = (((a12 * 5) - 497532) - 56570);
	    		a15 = 5; 
	    		a21 = 6; 

	    	 return -1;
	    } else if((((((a15==9) && ((a24==1) &&  80 < a12 )) && (a21==10)) || ((((a24==2) &&  a12 <=  -43 ) && (a15==5)) && (a21==6))) && (input == 5))){
	    	a12 = (((((a12 + 0) % 299978)+ -300020) / 5) + -262569);
	    		a24 = 2; 
	    		a15 = 5; 
	    		a21 = 6; 

	    	 return 25;
	    } else if((((a24==1) && (  ((11 < a12) && (80 >= a12))  && (((a21==7) || (a21==8)) && (input == 5)))) && (a15==8))){
	    	a12 = (((((a12 * 68)/ 10) * 5) + -454858) + 972700);
	    		a21 = 6; 

	    	 return 25;
	    } else if(((((((a21==10) &&   ((-43 < a12) && (11 >= a12)) ) || (  ((11 < a12) && (80 >= a12))  && (a21==6))) && (input == 1)) && (a15==8)) && (a24==1))){
	    	a12 = (((a12 + -298811) + -140133) + -153332);
	    		a15 = 5; 
	    		a21 = 6; 

	    	 return -1;
	    } else if(((a24==1) && (  ((11 < a12) && (80 >= a12))  && (((((a21==6) || (a21==7)) || (a21==8)) && (input == 6)) && (a15==9))))){

	    		a15 = 7; 
	    		a21 = 9; 

	    	 return -1;
	    } else if(((a24==1) && (((((a21==7) &&  80 < a12 ) || ((  ((11 < a12) && (80 >= a12))  && (a21==10)) || ( 80 < a12  && (a21==6)))) && (input == 1)) && (a15==8)))){
	    	a12 = ((((a12 + 0) % 299978)+ -300020) * 1);
	    		a15 = 5; 
	    		a21 = 6; 

	    	 return -1;
	    } else if((((a15==8) && ((((a21==10) &&   ((-43 < a12) && (11 >= a12)) ) || (  ((11 < a12) && (80 >= a12))  && (a21==6))) && (input == 5))) && (a24==1))){
	    	a12 = (((((a12 - -338613) - -126296) * 1) % 34)- -42);
	    		a21 = 9; 

	    	 return 25;
	    } else if(((  ((-43 < a12) && (11 >= a12))  && (((input == 6) && ((a21==9) || (a21==10))) && (a24==1))) && (a15==9))){
	    	a12 = ((((((a12 - -277912) * 10)/ 9) - 437300) * -1)/ 10);
	    		a15 = 6; 
	    		a21 = 6; 

	    	 return -1;
	    } else if(((a15==8) && ( 80 < a12  && ((a24==1) && (((a21==8) || (a21==9)) && (input == 5)))))){
	    	a12 = (((a12 + -600079) - -316691) - 316661);
	    		a15 = 9; 
	    		a21 = 8; 

	    	 return 26;
	    } else if((((a24==1) && ((a15==9) && (((a21==7) || (a21==8)) && (input == 5)))) &&  80 < a12 )){

	    		a21 = 10; 

	    	 return 25;
	    } else if((((((input == 5) &&   ((-43 < a12) && (11 >= a12)) ) && (a21==8)) && (a24==1)) && (a15==9))){
	    	a12 = (((a12 / 5) - 440689) * 1);
	    		a15 = 5; 
	    		a21 = 6; 

	    	 return -1;
	    } else if(((a15==9) && ((((input == 4) && (a24==1)) && (a21==8)) &&   ((-43 < a12) && (11 >= a12)) ))){

	    		a21 = 10; 

	    	 return 22;
	    } 
	    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 != 1) && (input != 2) && (input != 3) && (input != 4) && (input != 5) && (input != 6)) return -2;

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