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

	// inputs
	int d= 4;
	int f= 6;
	int a= 1;
	int e= 5;
	int c= 3;
	int b= 2;

	// outputs
	int u = 21;
	int v = 22;
	int w = 23;
	int x = 24;
	int y = 25;
	int z = 26;


	int a1 = 1;
	int a4 = 1;
	int a0 = 1;
	int a15 = 1;
	int a29 = 1;
	int a10 = 1;
	int a16 = 1;
	int a22 = 1;
	int a2 = 0;
	int a17 = 0;
	int a25 = 0;
	int a7 = 0;
	int a14 = 0;
	int a19 = 0;
	int a20 = 0;
	int a8 = 0;
	int a23 = 0;
	int a21 = 1;
	int a24 = 1;
	int a13 = 1;
	int a9 = 1;
	int a28 = 1;
	int a26 = 0;
	int a6 = 0;
	int a27 = 1;
	int a12 = 0;
	int a3 = 1;
	int a11 = 0;
	int a5 = 1;
	int a18 = 1;

	int calculate_output(int input) {
	    if((((((a18==1)&&((((a22==1)&&(a4==1))||(a2==1))&&(a0==1)))&&(a11==1))&&(a3==2))&&(!(a8==1)&&(((a5==1)&&((a6==1)&&(((((!(a27==1)&&!(a26==1))&&(a12==1))||(((a26==1)&&(a27==1))&&!(a12==1)))&&(input==5))&&!(a2==1))))&&!(a25==1))))){
	    	if((a18==1)){
	    		a2 = 0;
	    		a27 = 1;
	    		a25 = 0;
	    		a19 = 0;
	    		a26 = 1;
	    		a11 = 0;
	    		a12 = 0;
	    	}else{
	    		a12 = 0;
	    		a29 = 1;
	    		a26 = 1;
	    		a27 = 1;
	    		a6 = 0;
	    		a1 = 1;
	    	}  
	    	return 23;
	    } else if(((((a5==1)&&((a20==1)&&(((!(a26==1)&&(a27==1))||(!(a27==1)&&(a26==1)))&&(input==6))))&&!(a15==1))&&(((a3==2)&&(!(a1==1)&&((a18==1)&&((a19==1)&&(((((a0==1)&&!(a16==1))&&(a12==1))&&(a14==1))&&(a6==1))))))&&!(a11==1)))){
	    	a26 = 1;
	    	a3 = 0;
	    	a27 = 0;
	    	a17 = 1;
	    	a25 = 1;
	    	a19 = 1;
	    	a11 = 1;
	    	return -1;
	    } else if(((!(a1==1)||((a10==1)&&((a4==1)&&!(a8==1))))&&((!(a11==1)&&(!(a14==1)&&(((a18==1)&&(!(a12==1)&&((((a3==2)&&(((((a26==1)&&(a27==1))||(!(a26==1)&&(a27==1)))||((a26==1)&&!(a27==1)))&&(input==5)))&&!(a8==1))&&(a16==1))))&&(a6==1))))&&(a5==1)))){
	    	a4 = 1;
	    	a26 = 0;
	    	a25 = 0;
	    	a2 = 0;
	    	a27 = 1;
	    	return -1;
	    } else if(((((a3==1)&&(!(a6==1)&&((!(a14==1)&&(((input==5)&&!(a26==1))&&(a1==1)))&&!(a8==1))))&&(a27==1))&&(((!(a16==1)||((!(a12==1)&&((a5==1)&&((a29==1)&&!(a25==1))))&&(a18==1)))&&(a10==1))&&!(a11==1)))){
	    	a17 = 0;
	    	a1 = 1;
	    	a25 = 0;
	    	a27 = 0;
	    	return 26;
	    } else if(((!(a26==1)&&((a5==1)&&((a18==1)&&(((a4==1)&&!(a11==1))&&!(a6==1)))))&&(((a29==1)&&(!(a23==1)&&(!(a7==1)&&((!(a25==1)&&(((!(a27==1)&&(input==1))&&(a3==1))&&(a10==1)))&&!(a14==1)))))&&!(a12==1)))){
	    	a26 = 1;
	    	a11 = 1;
	    	a3 = 0;
	    	a27 = 1;
	    	a6 = 1;
	    	a12 = 1;
	    	a15 = 1;
	    	a4 = 1;
	    	return -1;
	    } else if(((((a16==1)&&((a3==2)&&((a11==1)&&((a20==1)||((a16==1)&&(a18==1))))))&&(a22==1))&&((a15==1)&&((a22==1)&&(((a5==1)&&(((((!(a26==1)&&!(a27==1))||(((a27==1)&&!(a26==1))||(!(a27==1)&&(a26==1))))&&(input==2))&&!(a17==1))&&!(a12==1)))&&(a6==1)))))){
	    	a7 = 0;
	    	a1 = 1;
	    	a3 = 0;
	    	a12 = 1;
	    	a26 = 1;
	    	a27 = 1;
	    	a14 = 0;
	    	return -1;
	    } else if((((((a18==1)&&((((((!(a12==1)&&((!(a26==1)&&!(a6==1))&&!(a27==1)))&&(a3==2))&&!(a11==1))&&(a5==1))||(!(a5==1)&&(((a3==0)&&((a12==1)&&((a27==1)&&((a26==1)&&(a6==1)))))&&(a11==1))))&&(input==3)))&&!(a20==1))&&!(a23==1))&&(!(a29==1)||(!(a1==1)||(!(a15==1)||(!(a17==1)&&(a4==1))))))){
	    	a19 = 1;
	    	a12 = 1;
	    	a24 = 1;
	    	a5 = 1;
	    	a26 = 1;
	    	a11 = 0;
	    	a6 = 0;
	    	a28 = 0;
	    	a27 = 1;
	    	a3 = 0;
	    	return 25;
	    } else if(((((((!(a20==1)&&((((a15==1)&&((input==1)&&(((a12==1)&&(!(a27==1)&&!(a26==1)))||(((a27==1)&&(a26==1))&&!(a12==1)))))&&!(a8==1))&&(a5==1)))&&(a11==1))&&!(a17==1))&&(a4==1))&&(a6==1))&&(!(a19==1)&&((a18==1)&&((a3==2)&&(a0==1)))))){
	    	a16 = 1;
	    	a22 = 1;
	    	a8 = 0;
	    	a3 = 0;
	    	a26 = 1;
	    	a12 = 1;
	    	a27 = 1;
	    	return -1;
	    } else if((((((a18==1)&&((!(a2==1)&&(((input==5)&&(((a12==1)&&(!(a26==1)&&!(a27==1)))||(!(a12==1)&&((a26==1)&&(a27==1)))))&&!(a7==1)))&&(a29==1)))&&(a0==1))&&(a11==1))&&((a6==1)&&((a7==1)||(!(a10==1)||(!(a5==1)&&((a3==0)&&(a0==1)))))))){
	    	a14 = 1;
	    	a10 = 0;
	    	a6 = 0;
	    	a5 = 1;
	    	a11 = 0;
	    	a12 = 1;
	    	a26 = 1;
	    	a24 = 0;
	    	a27 = 1;
	    	return 21;
	    } else if(((((a7==1)||((!(a8==1)&&((!(a12==1)&&((a0==1)&&(a3==0)))&&!(a19==1)))&&(a11==1)))&&!(a5==1))&&((a18==1)&&((((a6==1)&&((a10==1)&&(((((a27==1)&&!(a26==1))||((a26==1)&&!(a27==1)))||(!(a27==1)&&!(a26==1)))&&(input==4))))&&(a1==1))&&(a22==1))))){
	    	a26 = 0;
	    	a15 = 0;
	    	a29 = 0;
	    	a27 = 0;
	    	a5 = 1;
	    	a6 = 0;
	    	a12 = 1;
	    	return 25;
	    } else if(((!(a22==1)&&(((a5==1)&&((a3==2)&&((!(a22==1)&&((a17==1)&&(a10==1)))&&(a12==1))))&&!(a11==1)))&&((!(a15==1)&&(((a18==1)&&(((input==4)&&((!(a26==1)&&(a27==1))||((a26==1)&&!(a27==1))))&&(a20==1)))&&(a6==1)))&&!(a4==1)))){
	    	a26 = 1;
	    	a29 = 0;
	    	a28 = 1;
	    	a11 = 1;
	    	a6 = 0;
	    	a27 = 0;
	    	a25 = 1;
	    	return -1;
	    } else if(((((a3==2)&&(((a6==1)&&((!(a23==1)&&(!(a25==1)&&(((((a26==1)&&(a27==1))||(!(a26==1)&&(a27==1)))||((a26==1)&&!(a27==1)))&&(input==2))))&&!(a11==1)))&&(a16==1)))&&(a18==1))&&((a5==1)&&((((a25==1)||((a4==1)&&(a22==1)))&&!(a25==1))&&!(a12==1))))){
	    	a6 = 0;
	    	a29 = 1;
	    	a11 = 1;
	    	a26 = 1;
	    	a7 = 0;
	    	a27 = 1;
	    	return 23;
	    } else if((((a11==1)&&((a18==1)&&((a22==1)&&((!(a23==1)&&(((!(a26==1)&&!(a27==1))||((!(a26==1)&&(a27==1))||((a26==1)&&!(a27==1))))&&(input==6)))&&!(a12==1)))))&&(!(a22==1)||((a6==1)&&(((a22==1)&&(((a5==1)&&((a4==1)||!(a10==1)))&&(a3==2)))||!(a22==1)))))){
	    	a27 = 1;
	    	a17 = 0;
	    	a10 = 1;
	    	a3 = 0;
	    	a8 = 0;
	    	a26 = 1;
	    	a12 = 1;
	    	return -1;
	    } else if(((!(a26==1)&&((!(a22==1)||(!(a1==1)||((!(a8==1)&&(a29==1))||(a7==1))))&&(a29==1)))&&((a3==1)&&((a27==1)&&((!(a12==1)&&(!(a11==1)&&((a18==1)&&(((input==6)&&(a5==1))&&!(a6==1)))))&&!(a19==1)))))){
	    	a3 = 0;
	    	a11 = 1;
	    	a12 = 1;
	    	a8 = 0;
	    	a20 = 0;
	    	a26 = 1;
	    	a6 = 1;
	    	a29 = 1;
	    	return -1;
	    } else if((((a11==1)&&(!(a8==1)&&((((a12==1)&&(!(a26==1)&&!(a27==1)))||(!(a12==1)&&((a27==1)&&(a26==1))))&&(input==6))))&&(!(a5==1)&&((a3==0)&&((a18==1)&&((((!(a4==1)||(((a1==1)&&!(a8==1))&&(a6==1)))||(a14==1))||!(a0==1))&&(a4==1))))))){
	    	if((a29==1)){
	    		a12 = 1;
	    		a26 = 1;
	    		a5 = 1;
	    		a0 = 0;
	    		a27 = 1;
	    		a3 = 2;
	    		a21 = 1;
	    		a6 = 0;
	    		a29 = 0;
	    	}else{
	    		a29 = 0;
	    		a9 = 0;
	    		a3 = 2;
	    		a26 = 0;
	    		a4 = 0;
	    		a12 = 0;
	    		a5 = 1;
	    		a27 = 0;
	    	}  
	    	return -1;
	    } else if(((!(a17==1)&&(!(a8==1)&&((a4==1)&&((a18==1)&&((a3==2)&&(!(a6==1)&&(((!(a17==1)&&((((!(a26==1)&&!(a27==1))&&(a12==1))||(!(a12==1)&&((a27==1)&&(a26==1))))&&(input==2)))&&(a5==1))&&!(a11==1))))))))&&(((a4==1)||(a2==1))||!(a10==1)))){
	    	a3 = 1;
	    	a24 = 0;
	    	a28 = 0;
	    	a0 = 0;
	    	a27 = 0;
	    	a12 = 0;
	    	a26 = 1;
	    	return -1;
	    } else if((((a15==1)&&((a3==2)&&((a5==1)&&((((input==1)&&((!(a12==1)&&(((a6==1)&&!(a26==1))&&!(a27==1)))||(((a27==1)&&((a26==1)&&!(a6==1)))&&(a12==1))))&&!(a11==1))&&(a29==1)))))&&((a8==1)||((((a18==1)&&(!(a7==1)&&(a15==1)))&&!(a19==1))&&(a22==1))))){
	    	a12 = 1;
	    	a27 = 1;
	    	a26 = 1;
	    	a25 = 0;
	    	a6 = 1;
	    	a3 = 0;
	    	a16 = 1;
	    	a10 = 1;
	    	a11 = 1;
	    	return -1;
	    } else if(((((((((!(a25==1)&&(a1==1))&&(a0==1))||(a7==1))&&!(a6==1))&&(a29==1))&&(a3==2))&&(a11==1))&&((a18==1)&&((((a27==1)&&(((!(a12==1)&&(input==2))&&(a29==1))&&!(a26==1)))&&!(a25==1))&&(a5==1))))){
	    	a1 = 1;
	    	a19 = 0;
	    	a0 = 1;
	    	return 24;
	    } else if((((a0==1)&&((!(a6==1)&&(((a3==1)&&(!(a12==1)&&((a8==1)||((a22==1)&&!(a23==1)))))||!(a10==1)))&&!(a11==1)))&&(!(a27==1)&&((a26==1)&&((!(a14==1)&&(((input==1)&&(a5==1))&&(a29==1)))&&(a18==1)))))){
	    	a1 = 1;
	    	a11 = 1;
	    	a12 = 1;
	    	a3 = 0;
	    	a27 = 1;
	    	a19 = 0;
	    	a6 = 1;
	    	a2 = 0;
	    	return -1;
	    } else if(((((((a20==1)||((a4==1)&&((a20==1)||((a29==1)&&(a5==1)))))||!(a22==1))&&(a3==2))&&(a27==1))&&((!(a14==1)&&(!(a26==1)&&(((a1==1)&&((a18==1)&&(!(a12==1)&&(input==1))))&&(a11==1))))&&!(a6==1)))){
	    	a27 = 0;
	    	a1 = 1;
	    	a25 = 0;
	    	a6 = 1;
	    	a26 = 1;
	    	a3 = 1;
	    	a15 = 1;
	    	return -1;
	    } else if(((((((((a11==1)&&((a6==1)&&(!(a7==1)&&(a22==1))))&&(a18==1))&&(a5==1))||(a14==1))&&(a16==1))&&(a29==1))&&((a10==1)&&(!(a2==1)&&((((((a26==1)&&!(a27==1))||(((a26==1)&&(a27==1))||((a27==1)&&!(a26==1))))&&(input==1))&&(a3==2))&&(a12==1)))))){
	    	a26 = 1;
	    	a3 = 0;
	    	a27 = 1;
	    	a25 = 0;
	    	a23 = 0;
	    	a4 = 1;
	    	return -1;
	    } else if((((a3==2)&&((!(a17==1)&&((a18==1)&&((a17==1)||(a16==1))))&&(a5==1)))&&(!(a25==1)&&(((!(a11==1)&&((((!(a12==1)&&((!(a26==1)&&(a6==1))&&!(a27==1)))||((a12==1)&&((!(a6==1)&&(a26==1))&&(a27==1))))&&(input==5))&&!(a7==1)))&&!(a19==1))&&!(a7==1))))){
	    	a3 = 0;
	    	a12 = 1;
	    	a26 = 1;
	    	a11 = 1;
	    	a15 = 1;
	    	a6 = 1;
	    	a27 = 1;
	    	a2 = 0;
	    	a23 = 0;
	    	return -1;
	    } else if((((a1==1)&&(((!(a23==1)&&((a27==1)&&(!(a12==1)&&((a18==1)&&(!(a20==1)&&((input==1)&&(a11==1)))))))&&!(a23==1))&&!(a19==1)))&&(!(a20==1)&&((a3==2)&&((a5==1)&&(!(a6==1)&&((a16==1)&&(a26==1)))))))){
	    	a11 = 0;
	    	a6 = 1;
	    	a14 = 0;
	    	a10 = 1;
	    	a27 = 0;
	    	a23 = 0;
	    	return -1;
	    } else if(((((a18==1)&&(((!(a14==1)&&((a4==1)&&((a16==1)&&(((input==3)&&((a26==1)||!(a26==1)))&&(a22==1)))))&&(a11==1))&&(a5==1)))&&!(a6==1))&&((a27==1)&&((a12==1)&&(((a22==1)&&((a10==1)&&(a0==1)))&&(a3==2)))))){
	    	a11 = 0;
	    	a17 = 0;
	    	a7 = 0;
	    	a26 = 1;
	    	a6 = 1;
	    	a20 = 0;
	    	return 21;
	    } else if(((!(a25==1)&&((((((a11==1)&&(((!(a14==1)&&(!(a27==1)&&(a15==1)))&&(a12==1))&&(a5==1)))&&(a3==2))&&!(a2==1))||!(a15==1))&&!(a6==1)))&&((a22==1)&&(((a29==1)&&(((a26==1)||!(a26==1))&&(input==4)))&&(a18==1))))){
	    	a27 = 1;
	    	a16 = 1;
	    	a6 = 1;
	    	a3 = 0;
	    	a26 = 1;
	    	a0 = 1;
	    	a10 = 1;
	    	return -1;
	    } else if((((a1==1)&&((a5==1)&&((!(a26==1)&&(a0==1))&&!(a6==1))))&&((((!(a23==1)&&((((!(a11==1)&&(((a3==1)&&(input==2))&&!(a27==1)))&&!(a12==1))&&(a0==1))&&!(a19==1)))&&!(a17==1))&&(a18==1))&&(a16==1)))){
	    	a3 = 0;
	    	a12 = 1;
	    	a11 = 1;
	    	a6 = 1;
	    	a14 = 0;
	    	a27 = 1;
	    	a0 = 1;
	    	a7 = 0;
	    	a26 = 1;
	    	return -1;
	    } else if(((!(a6==1)&&((!(a8==1)&&((!(a7==1)&&((input==4)&&(a11==1)))&&(a5==1)))&&!(a8==1)))&&((a18==1)&&((!(a12==1)&&((((((a3==2)&&(a0==1))||!(a0==1))||!(a1==1))&&(a26==1))&&(a27==1)))||!(a16==1))))){
	    	a11 = 0;
	    	a6 = 1;
	    	a1 = 1;
	    	a2 = 0;
	    	a19 = 0;
	    	return 23;
	    } else if((((!(a26==1)&&((((a27==1)&&((a10==1)&&(!(a25==1)&&(a22==1))))||!(a16==1))&&!(a2==1)))&&!(a7==1))&&(((a5==1)&&(((a18==1)&&((a0==1)&&(!(a11==1)&&((input==2)&&(a3==1)))))&&!(a6==1)))&&!(a12==1)))){
	    	a11 = 1;
	    	a14 = 0;
	    	a6 = 1;
	    	a15 = 1;
	    	a23 = 0;
	    	a26 = 1;
	    	a3 = 0;
	    	a12 = 1;
	    	return -1;
	    } else if(((!(a23==1)&&((a1==1)&&(!(a27==1)&&(((input==2)&&(a18==1))&&(a0==1)))))&&(((a12==1)&&((a3==2)&&((!(a11==1)&&((a5==1)&&((a2==1)||((a10==1)&&((a15==1)||(a7==1))))))&&!(a26==1))))&&(a6==1)))){
	    	a29 = 1;
	    	a4 = 1;
	    	a27 = 1;
	    	a17 = 0;
	    	a6 = 0;
	    	a3 = 1;
	    	a26 = 1;
	    	a11 = 1;
	    	return -1;
	    } else if(((!(a2==1)&&(((a3==2)&&((a5==1)&&((a12==1)&&((!(a11==1)&&((a6==1)&&((input==5)&&((!(a26==1)&&(a27==1))||((a26==1)&&!(a27==1))))))&&(a15==1)))))&&(a10==1)))&&(!(a0==1)||((!(a7==1)&&((a4==1)&&(a22==1)))&&(a18==1))))){
	    	a12 = 0;
	    	a25 = 0;
	    	a3 = 0;
	    	a15 = 1;
	    	a26 = 1;
	    	a6 = 0;
	    	a27 = 1;
	    	return -1;
	    } else if(((((a0==1)&&(!(a17==1)&&((a0==1)&&((((input==5)&&((!(a26==1)&&!(a27==1))||((!(a26==1)&&(a27==1))||(!(a27==1)&&(a26==1)))))&&!(a2==1))&&!(a12==1)))))&&(a1==1))&&((((a18==1)&&((a11==1)&&(((a22==1)&&(a6==1))&&(a5==1))))&&(a3==2))||!(a29==1)))){
	    	a20 = 0;
	    	a27 = 1;
	    	a2 = 0;
	    	a26 = 0;
	    	a6 = 0;
	    	a22 = 1;
	    	return 24;
	    } else if(((((a3==1)&&(((((((a23==1)||(a15==1))||!(a15==1))&&(a26==1))&&!(a14==1))&&!(a19==1))&&!(a12==1)))&&!(a27==1))&&(!(a6==1)&&(((a5==1)&&((a0==1)&&((a10==1)&&((input==4)&&(a18==1)))))&&!(a11==1))))){
	    	a3 = 0;
	    	a29 = 1;
	    	a12 = 1;
	    	a11 = 1;
	    	a15 = 1;
	    	a6 = 1;
	    	a0 = 1;
	    	a27 = 1;
	    	return -1;
	    } else if((((a6==1)&&(((!(a19==1)&&((a0==1)&&(!(a5==1)&&(((input==3)&&(((!(a27==1)&&!(a26==1))&&(a12==1))||(((a26==1)&&(a27==1))&&!(a12==1))))&&(a10==1)))))&&!(a25==1))&&(a3==0)))&&((a11==1)&&((a18==1)&&((a4==1)&&(!(a4==1)||(a15==1))))))){
	    	a20 = 1;
	    	a6 = 0;
	    	a5 = 1;
	    	a12 = 0;
	    	a3 = 2;
	    	a19 = 1;
	    	a27 = 1;
	    	a26 = 1;
	    	a21 = 1;
	    	return -1;
	    } else if(((((a6==1)&&(((a19==1)||((!(a19==1)&&(a29==1))||(a20==1)))&&!(a5==1)))&&(a18==1))&&((a11==1)&&((!(a23==1)&&((((a10==1)&&(((((a27==1)&&!(a26==1))||((a26==1)&&!(a27==1)))||(!(a27==1)&&!(a26==1)))&&(input==3)))&&!(a12==1))&&(a3==0)))&&!(a20==1))))){
	    	if((a15==1)){
	    		a11 = 0;
	    		a24 = 0;
	    		a0 = 0;
	    		a26 = 1;
	    		a6 = 0;
	    		a27 = 1;
	    		a5 = 1;
	    		a9 = 1;
	    		a3 = 2;
	    	}else{
	    		a20 = 1;
	    		a5 = 1;
	    		a12 = 1;
	    		a16 = 0;
	    		a27 = 1;
	    		a26 = 0;
	    	}  
	    	return -1;
	    } else if((((a18==1)&&((((((a6==1)&&((input==2)&&(((!(a26==1)&&!(a27==1))&&(a12==1))||(!(a12==1)&&((a27==1)&&(a26==1))))))&&!(a23==1))&&(a11==1))&&(a0==1))&&!(a8==1)))&&((!(a7==1)&&((a3==2)&&(((a15==1)||(a14==1))&&(a5==1))))||!(a0==1)))){
	    	a3 = 0;
	    	a23 = 0;
	    	a12 = 1;
	    	a27 = 1;
	    	a1 = 1;
	    	a26 = 1;
	    	return -1;
	    } else if(((((((a3==2)&&((a5==1)&&(((a7==1)||(a22==1))&&!(a6==1))))&&!(a27==1))||!(a4==1))&&(a12==1))&&((a11==1)&&(((a18==1)&&((((((a26==1)||!(a26==1))&&(input==6))&&!(a19==1))&&!(a7==1))&&(a16==1)))&&(a0==1))))){
	    	a27 = 1;
	    	a16 = 1;
	    	a3 = 0;
	    	a7 = 0;
	    	a6 = 1;
	    	a10 = 1;
	    	a26 = 1;
	    	return -1;
	    } else if(((((((((a4==1)&&((a18==1)&&((a11==1)&&((((a26==1)&&!(a27==1))||(((a27==1)&&(a26==1))||((a27==1)&&!(a26==1))))&&(input==6)))))&&(a10==1))&&(a22==1))&&!(a25==1))&&(a3==2))&&(a6==1))&&((((a5==1)&&((a12==1)&&(a15==1)))&&(a1==1))&&!(a7==1)))){
	    	a3 = 0;
	    	a10 = 1;
	    	a27 = 1;
	    	a26 = 1;
	    	a1 = 1;
	    	a8 = 0;
	    	return -1;
	    } else if(((((((a16==1)||!(a16==1))||(a25==1))&&(a18==1))&&!(a2==1))&&((a22==1)&&((((input==5)&&(((a5==1)&&(((((!(a26==1)&&!(a6==1))&&!(a27==1))&&!(a12==1))&&(a3==2))&&!(a11==1)))||(!(a5==1)&&(((((a27==1)&&((a6==1)&&(a26==1)))&&(a12==1))&&(a3==0))&&(a11==1)))))&&(a16==1))&&!(a7==1))))){
	    	a13 = 1;
	    	a25 = 1;
	    	a12 = 1;
	    	a26 = 0;
	    	a3 = 1;
	    	a27 = 0;
	    	a20 = 1;
	    	a11 = 1;
	    	a6 = 1;
	    	a5 = 1;
	    	return -1;
	    } else if(((((a18==1)&&((a5==1)&&(!(a12==1)&&(!(a20==1)&&(((input==5)&&((!(a26==1)&&(a27==1))||(!(a27==1)&&(a26==1))))&&(a0==1))))))&&(a3==2))&&(!(a11==1)&&(((a22==1)&&((a14==1)||(!(a6==1)&&((a10==1)||(a14==1)))))||(a2==1))))){
	    	a21 = 0;
	    	a27 = 1;
	    	a26 = 1;
	    	a24 = 1;
	    	a3 = 1;
	    	return -1;
	    } else if(((((!(a27==1)&&((a3==2)&&(((!(a16==1)||(a29==1))&&(a22==1))||!(a22==1))))&&(a10==1))&&!(a8==1))&&(((!(a25==1)&&(!(a26==1)&&((((input==1)&&(a6==1))&&!(a11==1))&&(a5==1))))&&(a12==1))&&(a18==1)))){
	    	a26 = 1;
	    	a2 = 0;
	    	a29 = 1;
	    	a6 = 0;
	    	a11 = 1;
	    	a23 = 0;
	    	a3 = 0;
	    	return -1;
	    } else if((((((!(a14==1)&&(((a0==1)&&((a15==1)&&(!(a8==1)&&((input==5)&&((!(a26==1)&&(a27==1))||(!(a27==1)&&(a26==1)))))))&&!(a25==1)))&&(a5==1))&&!(a6==1))&&(a18==1))&&(!(a11==1)&&((a3==2)&&((a12==1)&&((a10==1)&&!(a23==1))))))){
	    	a11 = 1;
	    	a26 = 1;
	    	a23 = 0;
	    	a27 = 1;
	    	a19 = 0;
	    	a12 = 0;
	    	return 23;
	    } else if(((((((a6==1)&&((a12==1)&&((a2==1)&&(a22==1))))&&(a23==1))&&(a8==1))&&(a7==1))&&((!(a11==1)&&(((a3==2)&&((a19==1)&&(((input==3)&&((!(a26==1)&&(a27==1))||((a26==1)&&!(a27==1))))&&(a5==1))))&&(a18==1)))&&(a17==1)))){
	    	a28 = 0;
	    	a27 = 0;
	    	a8 = 1;
	    	a12 = 0;
	    	a13 = 1;
	    	a11 = 1;
	    	a26 = 1;
	    	return 23;
	    } else if(((((a3==2)&&(((a4==1)&&(!(a17==1)&&((!(a19==1)&&(((a26==1)&&((a27==1)&&((input==3)&&(a18==1))))&&(a0==1)))&&(a4==1))))&&!(a17==1)))&&(a5==1))&&(((!(a6==1)&&(a15==1))&&!(a12==1))&&(a11==1)))){
	    	if((a20==1)){
	    		a14 = 0;
	    		a26 = 0;
	    		a11 = 0;
	    		a6 = 1;
	    		a15 = 1;
	    	}else{
	    		a10 = 1;
	    		a17 = 0;
	    		a14 = 0;
	    	}  
	    	return 23;
	    } else if((((a22==1)&&(((((a29==1)||!(a4==1))||(a17==1))&&(a18==1))&&(a11==1)))&&(!(a6==1)&&((a12==1)&&((((a3==2)&&((a4==1)&&((a5==1)&&((a27==1)&&(((a26==1)||!(a26==1))&&(input==2))))))&&!(a8==1))&&(a15==1)))))){
	    	a25 = 0;
	    	a1 = 1;
	    	a3 = 0;
	    	a7 = 0;
	    	a26 = 1;
	    	a6 = 1;
	    	return -1;
	    } else if((((a6==1)&&((a19==1)||(((a8==1)||(!(a12==1)&&(((a5==1)&&(a10==1))||!(a4==1))))&&(a11==1))))&&((a18==1)&&(!(a19==1)&&(((a1==1)&&(((input==1)&&(((!(a26==1)&&(a27==1))||((a26==1)&&!(a27==1)))||(!(a27==1)&&!(a26==1))))&&(a3==2)))&&!(a20==1)))))){
	    	a0 = 1;
	    	a12 = 1;
	    	a26 = 1;
	    	a2 = 0;
	    	a27 = 1;
	    	a1 = 1;
	    	a3 = 0;
	    	return -1;
	    } else if(((((a3==2)&&((a29==1)&&((a10==1)&&((a17==1)||((((a15==1)&&(a22==1))&&!(a12==1))&&(a29==1))))))&&(a6==1))&&((!(a11==1)&&((((((a26==1)&&!(a27==1))||(((a27==1)&&(a26==1))||((a27==1)&&!(a26==1))))&&(input==4))&&(a29==1))&&(a5==1)))&&(a18==1)))){
	    	if((a23==1)){
	    		a14 = 0;
	    		a29 = 1;
	    		a26 = 0;
	    		a27 = 1;
	    		a23 = 0;
	    	}else{
	    		a27 = 1;
	    		a26 = 1;
	    		a25 = 0;
	    		a11 = 1;
	    		a4 = 1;
	    		a6 = 0;
	    	}  
	    	return 23;
	    } else if(((((a8==1)||((a14==1)||(((a22==1)&&(a11==1))&&!(a6==1))))&&!(a27==1))&&((a12==1)&&((a16==1)&&(!(a17==1)&&((a5==1)&&((a4==1)&&((a3==2)&&(((a0==1)&&(((a26==1)||!(a26==1))&&(input==2)))&&(a18==1)))))))))){
	    	a26 = 1;
	    	a6 = 1;
	    	a27 = 1;
	    	a3 = 0;
	    	a29 = 1;
	    	a0 = 1;
	    	a15 = 1;
	    	return -1;
	    } else if((((((((((a26==1)||!(a26==1))&&(input==4))&&(a5==1))&&(a27==1))&&!(a19==1))&&(a18==1))&&(a16==1))&&(((!(a16==1)||((((a11==1)&&(((a15==1)&&(a3==2))&&!(a6==1)))||!(a22==1))&&(a12==1)))&&!(a25==1))&&(a16==1)))){
	    	a16 = 1;
	    	a6 = 1;
	    	a3 = 0;
	    	a10 = 1;
	    	a26 = 1;
	    	return -1;
	    } else if(((((a5==1)&&((((a18==1)&&((a0==1)&&(((a16==1)&&((input==2)&&((((!(a26==1)&&(a6==1))&&!(a27==1))&&!(a12==1))||((a12==1)&&((a27==1)&&(!(a6==1)&&(a26==1)))))))&&!(a25==1))))&&!(a2==1))&&(a3==2)))&&(a22==1))&&(!(a11==1)&&((a29==1)||!(a1==1))))){
	    	a12 = 1;
	    	a6 = 1;
	    	a26 = 1;
	    	a27 = 1;
	    	a2 = 0;
	    	a22 = 1;
	    	a3 = 0;
	    	a11 = 1;
	    	return -1;
	    } else if((((a12==1)&&(!(a6==1)&&(((a11==1)&&((((a26==1)||!(a26==1))&&(input==5))&&(a3==2)))&&!(a14==1))))&&(!(a15==1)||(((a15==1)&&(!(a0==1)||((((a18==1)&&((a5==1)&&(a1==1)))||(a19==1))&&(a27==1))))||(a2==1))))){
	    	a26 = 1;
	    	a16 = 1;
	    	a15 = 1;
	    	a6 = 1;
	    	a3 = 0;
	    	return -1;
	    } else if((((((((a5==1)&&((a3==2)&&(a1==1)))&&(a18==1))&&(a22==1))&&!(a11==1))||!(a0==1))&&((((a12==1)&&(((a6==1)&&((((!(a26==1)&&(a27==1))||((a26==1)&&!(a27==1)))&&(input==4))&&!(a8==1)))&&(a4==1)))&&!(a23==1))&&(a29==1)))){
	    	a12 = 0;
	    	a10 = 1;
	    	a27 = 1;
	    	a6 = 0;
	    	a23 = 0;
	    	a26 = 0;
	    	a8 = 0;
	    	a3 = 0;
	    	return -1;
	    } else if(((!(a19==1)&&((a16==1)&&(!(a7==1)&&(!(a20==1)&&(((input==2)&&((!(a11==1)&&((a12==1)&&((a27==1)&&((a6==1)&&(a26==1)))))||(((a11==1)&&((!(a27==1)&&(!(a6==1)&&(a26==1)))&&!(a12==1)))||((a11==1)&&(!(a12==1)&&(!(a27==1)&&(!(a26==1)&&!(a6==1))))))))&&!(a17==1))))))&&((a18==1)&&((a17==1)||(((a15==1)&&(a3==2))&&(a5==1)))))){
	    	a12 = 0;
	    	a11 = 1;
	    	a27 = 0;
	    	a6 = 0;
	    	a26 = 0;
	    	a25 = 0;
	    	a16 = 1;
	    	a20 = 0;
	    	return -1;
	    } else if((((a12==1)&&((a3==2)&&((!(a1==1)||(!(a22==1)||((a11==1)&&((a4==1)&&((a6==1)&&((a4==1)||!(a15==1)))))))||(a2==1))))&&((a29==1)&&((a18==1)&&((a5==1)&&(((((a26==1)&&(a27==1))||((a27==1)&&!(a26==1)))||(!(a27==1)&&(a26==1)))&&(input==4))))))){
	    	a23 = 0;
	    	a10 = 1;
	    	a3 = 0;
	    	a27 = 1;
	    	a4 = 1;
	    	a26 = 1;
	    	return -1;
	    } else if(((!(a11==1)&&((a5==1)&&((((input==5)&&(((a27==1)&&!(a26==1))||(!(a27==1)&&(a26==1))))&&(a23==1))&&(a3==2))))&&((a23==1)&&(!(a4==1)&&((((a18==1)&&((((a12==1)&&(a29==1))&&!(a22==1))&&!(a0==1)))&&(a19==1))&&(a6==1)))))){
	    	a27 = 1;
	    	a0 = 0;
	    	a12 = 0;
	    	a11 = 1;
	    	a29 = 0;
	    	a26 = 0;
	    	a28 = 1;
	    	return -1;
	    } else if((((((a1==1)&&(((input==6)&&(((a12==1)&&(!(a26==1)&&!(a27==1)))||(((a27==1)&&(a26==1))&&!(a12==1))))&&(a1==1)))&&(a5==1))&&(a16==1))&&(((a3==2)&&(!(a11==1)&&((!(a1==1)||((!(a6==1)&&(a0==1))&&!(a20==1)))&&(a18==1))))&&!(a17==1)))){
	    	a3 = 0;
	    	a12 = 1;
	    	a24 = 0;
	    	a28 = 1;
	    	a26 = 1;
	    	a4 = 0;
	    	a27 = 0;
	    	return -1;
	    } else if((((a18==1)&&(((!(a20==1)&&(a0==1))||(a20==1))&&(a1==1)))&&((a3==2)&&((a1==1)&&((a5==1)&&((((((((a27==1)&&((a26==1)&&(a6==1)))&&(a12==1))&&!(a11==1))||((((!(a27==1)&&(!(a6==1)&&(a26==1)))&&!(a12==1))&&(a11==1))||((!(a12==1)&&(!(a27==1)&&(!(a6==1)&&!(a26==1))))&&(a11==1))))&&(input==1))&&!(a7==1))&&(a15==1))))))){
	    	a6 = 0;
	    	a26 = 1;
	    	a1 = 1;
	    	a23 = 0;
	    	a27 = 1;
	    	a12 = 0;
	    	a11 = 1;
	    	a14 = 0;
	    	a3 = 1;
	    	return -1;
	    } else if(((((((a18==1)&&((a25==1)||(!(a11==1)&&((a4==1)&&(a3==2)))))&&(a0==1))&&(a5==1))||(a7==1))&&((a10==1)&&((!(a14==1)&&((input==6)&&((((!(a26==1)&&(a6==1))&&!(a27==1))&&!(a12==1))||((a12==1)&&((a27==1)&&(!(a6==1)&&(a26==1)))))))&&(a4==1))))){
	    	a11 = 1;
	    	a26 = 1;
	    	a12 = 1;
	    	a3 = 0;
	    	a7 = 0;
	    	a27 = 1;
	    	a4 = 1;
	    	a0 = 1;
	    	a6 = 1;
	    	return -1;
	    } else if((((!(a11==1)&&(((((a12==1)&&((((a27==1)&&!(a26==1))||((a26==1)&&!(a27==1)))&&(input==3)))&&!(a8==1))&&!(a19==1))&&!(a14==1)))&&(a0==1))&&(((a3==2)&&((((a5==1)&&(!(a6==1)&&(a29==1)))||(a17==1))&&(a16==1)))&&(a18==1)))){
	    	a7 = 0;
	    	a22 = 1;
	    	a16 = 1;
	    	a3 = 0;
	    	a26 = 0;
	    	a27 = 0;
	    	return -1;
	    } else if((((!(a19==1)&&(((((a4==1)&&!(a26==1))||!(a4==1))&&!(a11==1))&&!(a6==1)))||(a23==1))&&(!(a27==1)&&((a5==1)&&((((a22==1)&&((((a3==1)&&(input==5))&&!(a12==1))&&!(a25==1)))&&(a1==1))&&(a18==1)))))){
	    	a11 = 1;
	    	a12 = 1;
	    	a6 = 1;
	    	a1 = 1;
	    	a15 = 1;
	    	a10 = 1;
	    	a27 = 1;
	    	a3 = 0;
	    	a26 = 1;
	    	return -1;
	    } else if((((a4==1)&&((((((((!(a12==1)&&(((a26==1)&&!(a6==1))&&!(a27==1)))&&(a11==1))||((!(a12==1)&&(!(a27==1)&&(!(a6==1)&&!(a26==1))))&&(a11==1)))||(!(a11==1)&&((((a6==1)&&(a26==1))&&(a27==1))&&(a12==1))))&&(input==4))&&(a5==1))&&(a18==1))&&!(a19==1)))&&(((a17==1)||((!(a25==1)&&((a3==2)&&(a29==1)))||(a23==1)))&&(a1==1)))){
	    	a6 = 1;
	    	a12 = 1;
	    	a26 = 1;
	    	a11 = 0;
	    	a8 = 0;
	    	a27 = 1;
	    	a22 = 1;
	    	a15 = 1;
	    	return -1;
	    } else if((((a3==2)&&(((a18==1)&&(((input==2)&&((!(a26==1)&&(a27==1))||((a26==1)&&!(a27==1))))&&(a10==1)))&&(a15==1)))&&((((a23==1)||((a20==1)||((!(a25==1)&&(((a5==1)&&(a4==1))&&!(a8==1)))&&(a12==1))))&&!(a11==1))&&!(a6==1)))){
	    	a26 = 1;
	    	a10 = 1;
	    	a27 = 1;
	    	a3 = 0;
	    	a6 = 1;
	    	a11 = 1;
	    	a19 = 0;
	    	a23 = 0;
	    	return -1;
	    } else if(((!(a23==1)&&((!(a2==1)&&((((a5==1)&&(a29==1))||!(a1==1))||!(a22==1)))||(a8==1)))&&((a0==1)&&((a18==1)&&(!(a12==1)&&(!(a26==1)&&((((a3==2)&&((a27==1)&&(input==6)))&&(a11==1))&&!(a6==1)))))))){
	    	a0 = 1;
	    	a7 = 0;
	    	a22 = 1;
	    	return -1;
	    } else if((((a1==1)&&(((((a15==1)&&((!(a11==1)&&(!(a23==1)&&(!(a14==1)&&((input==3)&&(((a27==1)&&!(a26==1))||((a26==1)&&!(a27==1)))))))&&(a10==1)))&&!(a6==1))&&(a5==1))&&(a1==1)))&&((a3==2)&&((!(a12==1)&&(a10==1))&&(a18==1))))){
	    	a26 = 1;
	    	a0 = 0;
	    	a27 = 1;
	    	a9 = 1;
	    	a21 = 0;
	    	return -1;
	    } else if(((!(a11==1)&&((a18==1)&&((!(a23==1)&&(((((a5==1)&&((input==1)&&(((a12==1)&&(!(a27==1)&&!(a26==1)))||(((a26==1)&&(a27==1))&&!(a12==1)))))&&!(a6==1))&&!(a14==1))&&(a16==1)))&&(a3==2))))&&(!(a10==1)||((a19==1)||(!(a7==1)&&(a0==1)))))){
	    	a12 = 0;
	    	a26 = 1;
	    	a11 = 1;
	    	a3 = 0;
	    	a22 = 0;
	    	a24 = 1;
	    	a27 = 1;
	    	a7 = 1;
	    	return -1;
	    } else if((((((!(a25==1)&&((((a22==1)||(a8==1))&&(a18==1))||!(a15==1)))&&!(a12==1))&&(a6==1))&&(a5==1))&&((a11==1)&&(((((a3==2)&&((input==4)&&((!(a27==1)&&!(a26==1))||((!(a26==1)&&(a27==1))||(!(a27==1)&&(a26==1))))))&&!(a14==1))&&(a16==1))&&!(a20==1))))){
	    	a27 = 1;
	    	a12 = 1;
	    	a3 = 0;
	    	a10 = 1;
	    	a26 = 1;
	    	a25 = 0;
	    	a16 = 1;
	    	return -1;
	    } else if(((!(a17==1)&&((((!(a11==1)&&(a1==1))&&(a18==1))&&(a6==1))&&(a3==2)))&&((a4==1)&&((a16==1)&&(!(a20==1)&&((a15==1)&&((((((((a27==1)&&(a26==1))||((a27==1)&&!(a26==1)))||((a26==1)&&!(a27==1)))&&(input==1))&&!(a14==1))&&(a5==1))&&!(a12==1)))))))){
	    	if((a10==1)){
	    		a26 = 0;
	    		a27 = 1;
	    		a1 = 1;
	    		a2 = 0;
	    		a14 = 0;
	    	}else{
	    		a23 = 0;
	    		a0 = 1;
	    		a6 = 0;
	    		a25 = 0;
	    		a11 = 1;
	    		a26 = 1;
	    		a27 = 1;
	    	}  
	    	return -1;
	    } else if((((a1==1)&&(((a18==1)&&((!(a27==1)&&(a29==1))&&(a10==1)))||(a7==1)))&&(((!(a19==1)&&(((a5==1)&&((((a11==1)&&((input==3)&&((a26==1)||!(a26==1))))&&!(a6==1))&&(a12==1)))&&(a3==2)))&&(a16==1))&&(a0==1)))){
	    	a26 = 1;
	    	a6 = 1;
	    	a11 = 0;
	    	a22 = 1;
	    	a15 = 1;
	    	a8 = 0;
	    	return 25;
	    } else if((((((a16==1)&&((a18==1)&&((input==2)&&(((a5==1)&&(((!(a12==1)&&(!(a27==1)&&(!(a26==1)&&!(a6==1))))&&(a3==2))&&!(a11==1)))||(!(a5==1)&&((a11==1)&&(((a12==1)&&(((a6==1)&&(a26==1))&&(a27==1)))&&(a3==0))))))))&&(a10==1))&&(a29==1))&&((a0==1)&&(((a15==1)&&!(a14==1))&&!(a2==1))))){
	    	if((a11==1)){
	    		a26 = 1;
	    		a12 = 0;
	    		a27 = 0;
	    		a14 = 1;
	    		a5 = 1;
	    		a11 = 1;
	    		a3 = 0;
	    		a24 = 0;
	    		a6 = 0;
	    	}else{
	    		a3 = 2;
	    		a11 = 1;
	    		a6 = 1;
	    		a12 = 0;
	    		a5 = 1;
	    		a27 = 1;
	    		a13 = 0;
	    		a26 = 1;
	    		a25 = 1;
	    		a21 = 1;
	    	}  
	    	return 23;
	    } else if(((((a3==2)&&((a18==1)&&(a1==1)))&&!(a19==1))&&(((((a15==1)&&((((input==3)&&((((a12==1)&&((a27==1)&&((a6==1)&&(a26==1))))&&!(a11==1))||(((!(a12==1)&&(!(a27==1)&&((a26==1)&&!(a6==1))))&&(a11==1))||((a11==1)&&((!(a27==1)&&(!(a26==1)&&!(a6==1)))&&!(a12==1))))))&&(a5==1))&&!(a17==1)))&&(a10==1))&&(a16==1))&&(a0==1)))){
	    	a26 = 0;
	    	a27 = 1;
	    	a20 = 0;
	    	a29 = 1;
	    	a10 = 1;
	    	a11 = 1;
	    	a6 = 0;
	    	a12 = 0;
	    	return -1;
	    } else if((((!(a11==1)&&((a1==1)&&(a29==1)))&&(a12==1))&&((!(a2==1)&&(!(a6==1)&&((!(a17==1)&&(((a3==2)&&((a18==1)&&(((input==6)&&(((a27==1)&&!(a26==1))||((a26==1)&&!(a27==1))))&&(a0==1))))&&(a15==1)))&&(a22==1))))&&(a5==1)))){
	    	a10 = 1;
	    	a19 = 0;
	    	a27 = 1;
	    	a2 = 0;
	    	a6 = 1;
	    	a26 = 1;
	    	a3 = 0;
	    	a11 = 1;
	    	return -1;
	    } else if(((((((a2==1)||((a5==1)&&((a3==2)&&(a10==1))))&&(a18==1))||!(a1==1))&&!(a12==1))&&(!(a7==1)&&(!(a14==1)&&(!(a11==1)&&((((((!(a26==1)&&(a27==1))||(!(a27==1)&&(a26==1)))&&(input==4))&&(a4==1))&&!(a6==1))&&(a10==1))))))){
	    	a21 = 0;
	    	a26 = 1;
	    	a13 = 0;
	    	a4 = 0;
	    	a6 = 1;
	    	a27 = 0;
	    	return -1;
	    } else if((((!(a10==1)||(!(a12==1)&&(!(a27==1)&&(!(a7==1)&&(a22==1)))))&&!(a6==1))&&((a3==1)&&(!(a11==1)&&((!(a20==1)&&((a0==1)&&((!(a2==1)&&((a18==1)&&((a5==1)&&(input==5))))&&!(a19==1))))&&(a26==1)))))){
	    	a16 = 1;
	    	a22 = 1;
	    	a11 = 1;
	    	a3 = 2;
	    	a27 = 1;
	    	a6 = 1;
	    	return 21;
	    } else if(((((((!(a7==1)&&(a16==1))||!(a10==1))||!(a15==1))&&!(a6==1))||!(a22==1))&&(((!(a12==1)&&((a3==2)&&((a18==1)&&((!(a11==1)&&((((a27==1)&&!(a26==1))||(!(a27==1)&&(a26==1)))&&(input==6)))&&(a5==1)))))&&(a29==1))&&(a0==1)))){
	    	a27 = 1;
	    	a15 = 0;
	    	a14 = 1;
	    	a3 = 1;
	    	a26 = 0;
	    	a6 = 1;
	    	return -1;
	    } else if(((!(a12==1)&&(!(a11==1)&&((a6==1)&&((!(a17==1)&&((a5==1)&&(!(a2==1)&&(((input==6)&&((((a27==1)&&(a26==1))||((a27==1)&&!(a26==1)))||((a26==1)&&!(a27==1))))&&!(a7==1)))))&&(a29==1)))))&&((((!(a16==1)||(a1==1))&&(a3==2))||(a2==1))&&(a18==1)))){
	    	a26 = 1;
	    	a10 = 1;
	    	a29 = 1;
	    	a27 = 0;
	    	a1 = 1;
	    	return 23;
	    } else if(((((((a1==1)&&((input==3)&&(((a12==1)&&(!(a26==1)&&!(a27==1)))||(((a26==1)&&(a27==1))&&!(a12==1)))))&&!(a7==1))&&(a18==1))&&(a4==1))&&((a6==1)&&((a5==1)&&((a20==1)||(!(a1==1)||(((a3==2)&&((a10==1)||!(a10==1)))&&(a11==1)))))))){
	    	a26 = 0;
	    	a3 = 0;
	    	a6 = 0;
	    	a12 = 1;
	    	a27 = 0;
	    	a2 = 0;
	    	a14 = 0;
	    	a11 = 0;
	    	a8 = 0;
	    	return -1;
	    } else if(((((a18==1)&&((a1==1)&&((((a0==1)&&(!(a6==1)&&((((a12==1)&&(!(a26==1)&&!(a27==1)))||(((a27==1)&&(a26==1))&&!(a12==1)))&&(input==3))))&&!(a11==1))&&(a0==1))))&&(a16==1))&&(((a3==2)&&(((a5==1)&&(a0==1))&&(a1==1)))&&(a16==1)))){
	    	a12 = 0;
	    	a26 = 1;
	    	a4 = 0;
	    	a13 = 0;
	    	a25 = 1;
	    	a27 = 1;
	    	a11 = 1;
	    	return 23;
	    } else if(((!(a16==1)||(!(a8==1)&&(!(a0==1)||(((a16==1)&&(a6==1))&&(a11==1)))))&&((a16==1)&&((((a18==1)&&((a3==2)&&((a4==1)&&((((a12==1)&&(!(a26==1)&&!(a27==1)))||(!(a12==1)&&((a27==1)&&(a26==1))))&&(input==6)))))&&(a22==1))&&(a5==1))))){
	    	a16 = 1;
	    	a3 = 0;
	    	a26 = 1;
	    	a22 = 1;
	    	a7 = 0;
	    	a27 = 1;
	    	a12 = 1;
	    	return -1;
	    } else if(((((a6==1)&&(!(a7==1)&&(((a11==1)&&(((((input==5)&&((!(a26==1)&&!(a27==1))||((!(a26==1)&&(a27==1))||((a26==1)&&!(a27==1)))))&&(a18==1))&&!(a2==1))&&!(a19==1)))&&(a10==1))))&&!(a12==1))&&(((a3==0)&&(!(a0==1)||((a22==1)&&!(a8==1))))&&!(a5==1)))){
	    	a9 = 0;
	    	a3 = 1;
	    	a1 = 0;
	    	a5 = 1;
	    	a12 = 1;
	    	a11 = 0;
	    	a26 = 1;
	    	a27 = 0;
	    	a29 = 0;
	    	a6 = 0;
	    	return 23;
	    } else if((((!(a20==1)&&(((((a5==1)&&((((!(a26==1)&&!(a27==1))&&(a12==1))||(!(a12==1)&&((a26==1)&&(a27==1))))&&(input==5)))&&!(a17==1))&&(a22==1))&&(a3==2)))&&!(a11==1))&&(((a25==1)||((a18==1)&&(((a0==1)&&!(a14==1))&&!(a6==1))))&&(a22==1)))){
	    	a4 = 0;
	    	a12 = 0;
	    	a6 = 1;
	    	a26 = 0;
	    	a9 = 0;
	    	a0 = 0;
	    	a27 = 1;
	    	a3 = 0;
	    	a11 = 1;
	    	return -1;
	    } else if(((!(a2==1)&&((((((((((a26==1)||!(a26==1))&&(input==1))&&!(a14==1))&&(a11==1))&&!(a17==1))&&(a18==1))&&(a4==1))&&!(a6==1))&&!(a8==1)))&&((((a27==1)&&((a5==1)&&((a22==1)||(a23==1))))&&(a12==1))&&(a3==2)))){
	    	a16 = 1;
	    	a26 = 1;
	    	a3 = 0;
	    	a4 = 1;
	    	a6 = 1;
	    	a2 = 0;
	    	return -1;
	    } else if(((((!(a7==1)&&(!(a20==1)&&(((a6==1)&&(((a3==2)&&((input==3)&&((((a27==1)&&!(a26==1))||((a26==1)&&!(a27==1)))||(!(a27==1)&&!(a26==1)))))&&!(a12==1)))&&(a4==1))))&&(a11==1))&&(a18==1))&&((!(a10==1)||(((a15==1)||(a25==1))&&(a5==1)))&&!(a2==1)))){
	    	a10 = 1;
	    	a12 = 1;
	    	a27 = 1;
	    	a29 = 1;
	    	a14 = 0;
	    	a3 = 0;
	    	a26 = 1;
	    	return -1;
	    } else if(((((a11==1)&&((((a16==1)&&((a6==1)&&((input==4)&&(((!(a27==1)&&!(a26==1))&&(a12==1))||(!(a12==1)&&((a27==1)&&(a26==1)))))))&&(a18==1))&&(a3==0)))&&(a10==1))&&((((!(a5==1)&&((a15==1)||(a25==1)))||(a7==1))&&!(a2==1))&&!(a25==1)))){
	    	a26 = 1;
	    	a29 = 0;
	    	a0 = 0;
	    	a27 = 0;
	    	a12 = 1;
	    	a6 = 0;
	    	a5 = 1;
	    	a8 = 1;
	    	return -1;
	    } else if((((a11==1)&&(!(a6==1)&&(((a27==1)&&((a0==1)&&((!(a23==1)&&(!(a12==1)&&(input==5)))&&!(a26==1))))&&(a5==1))))&&((a3==2)&&((a23==1)||(((((a4==1)&&(a18==1))&&(a15==1))||!(a0==1))||!(a29==1)))))){
	    	a14 = 0;
	    	a29 = 1;
	    	a10 = 1;
	    	return -1;
	    } else if((((a3==0)&&((!(a5==1)&&(!(a14==1)&&(((((a0==1)||(a23==1))&&!(a25==1))||!(a1==1))||!(a29==1))))&&(a6==1)))&&((a11==1)&&((((((((a27==1)&&!(a26==1))||(!(a27==1)&&(a26==1)))||(!(a26==1)&&!(a27==1)))&&(input==2))&&(a18==1))&&!(a20==1))&&!(a12==1))))){
	    	if((a5==1)){
	    		a3 = 1;
	    		a26 = 1;
	    		a22 = 0;
	    		a15 = 0;
	    		a5 = 1;
	    		a21 = 1;
	    		a27 = 0;
	    	}else{
	    		a3 = 1;
	    		a6 = 0;
	    		a5 = 1;
	    		a13 = 0;
	    		a26 = 1;
	    		a2 = 1;
	    		a22 = 0;
	    		a27 = 0;
	    		a11 = 0;
	    	}  
	    	return -1;
	    } else if(((!(a27==1)&&(!(a23==1)&&(!(a11==1)&&(((a12==1)&&(!(a26==1)&&((a3==2)&&(input==4))))&&(a4==1)))))&&(((a15==1)&&((a23==1)||((a6==1)&&(!(a8==1)&&((a23==1)||((a18==1)&&(a22==1)))))))&&(a5==1)))){
	    	a11 = 1;
	    	a4 = 1;
	    	a26 = 1;
	    	a23 = 0;
	    	a12 = 0;
	    	a19 = 0;
	    	a27 = 1;
	    	a3 = 1;
	    	return -1;
	    } else if(((((!(a16==1)&&((((a3==2)&&(!(a22==1)&&(!(a10==1)&&(((!(a26==1)&&(a27==1))||((a26==1)&&!(a27==1)))&&(input==1)))))&&(a12==1))&&(a25==1)))&&(a20==1))&&!(a11==1))&&((((a5==1)&&((a18==1)&&(a1==1)))&&!(a15==1))&&(a6==1)))){
	    	a12 = 0;
	    	a14 = 1;
	    	a28 = 1;
	    	a9 = 1;
	    	a27 = 0;
	    	a26 = 0;
	    	return 24;
	    } else if(((((a18==1)&&(((!(a22==1)||((a15==1)&&(a4==1)))||(a25==1))&&(a5==1)))&&!(a11==1))&&(((a3==2)&&((!(a7==1)&&((input==3)&&((!(a12==1)&&(((a6==1)&&!(a26==1))&&!(a27==1)))||((((a26==1)&&!(a6==1))&&(a27==1))&&(a12==1)))))&&(a22==1)))&&(a0==1)))){
	    	a26 = 0;
	    	a1 = 1;
	    	a11 = 1;
	    	a27 = 0;
	    	a6 = 0;
	    	a22 = 1;
	    	a12 = 0;
	    	a14 = 0;
	    	return 21;
	    } else if((((a16==1)&&(!(a5==1)&&((a3==0)&&(((input==2)&&(((!(a26==1)&&!(a27==1))&&(a12==1))||(((a27==1)&&(a26==1))&&!(a12==1))))&&(a6==1)))))&&(!(a29==1)||((a17==1)||(((((a17==1)||((a15==1)&&(a11==1)))||!(a10==1))&&(a18==1))||(a7==1)))))){
	    	if((a0==1)){
	    		a6 = 0;
	    		a13 = 0;
	    		a5 = 1;
	    		a7 = 1;
	    		a12 = 0;
	    		a2 = 1;
	    		a26 = 0;
	    		a27 = 1;
	    	}else{
	    		a5 = 1;
	    		a12 = 1;
	    		a9 = 0;
	    		a27 = 0;
	    		a16 = 0;
	    		a2 = 1;
	    		a26 = 1;
	    	}  
	    	return -1;
	    } else if((((!(a14==1)&&((a0==1)&&(a18==1)))&&(a16==1))&&((!(a19==1)&&((!(a23==1)&&((a5==1)&&((a3==2)&&((input==6)&&((((a11==1)&&((((a26==1)&&!(a6==1))&&!(a27==1))&&!(a12==1)))||((a11==1)&&((!(a27==1)&&(!(a6==1)&&!(a26==1)))&&!(a12==1))))||(((a12==1)&&(((a6==1)&&(a26==1))&&(a27==1)))&&!(a11==1)))))))&&!(a19==1)))&&(a16==1)))){
	    	a11 = 1;
	    	a6 = 0;
	    	a12 = 0;
	    	a26 = 0;
	    	a1 = 1;
	    	a19 = 0;
	    	a20 = 0;
	    	a27 = 0;
	    	return -1;
	    } else if(((!(a10==1)||((!(a1==1)||((((a23==1)||(((a11==1)&&((a29==1)&&!(a12==1)))&&!(a8==1)))&&(a6==1))&&(a3==0)))&&(a18==1)))&&(((((input==6)&&((!(a26==1)&&!(a27==1))||(((a27==1)&&!(a26==1))||((a26==1)&&!(a27==1)))))&&!(a7==1))&&!(a5==1))&&!(a2==1)))){
	    	a5 = 1;
	    	a25 = 1;
	    	a12 = 1;
	    	a9 = 0;
	    	a27 = 1;
	    	a26 = 0;
	    	return -1;
	    } else if((((!(a14==1)&&(((a18==1)&&((input==4)&&(((!(a11==1)&&(((!(a27==1)&&(!(a26==1)&&!(a6==1)))&&!(a12==1))&&(a3==2)))&&(a5==1))||(!(a5==1)&&(((a3==0)&&((a12==1)&&(((a26==1)&&(a6==1))&&(a27==1))))&&(a11==1))))))&&!(a25==1)))&&!(a2==1))&&((a10==1)&&(!(a7==1)&&((a10==1)&&!(a19==1)))))){
	    	a5 = 1;
	    	a19 = 1;
	    	a27 = 1;
	    	a12 = 0;
	    	a26 = 0;
	    	a21 = 0;
	    	a3 = 2;
	    	a6 = 1;
	    	a11 = 0;
	    	return -1;
	    } else if((((a5==1)&&(((!(a12==1)&&((((a16==1)||(a14==1))||(a19==1))&&!(a17==1)))&&!(a25==1))&&!(a11==1)))&&((((a18==1)&&((a3==2)&&((((((a26==1)&&(a27==1))||(!(a26==1)&&(a27==1)))||((a26==1)&&!(a27==1)))&&(input==3))&&!(a2==1))))&&(a6==1))&&(a29==1)))){
	    	a27 = 1;
	    	a26 = 1;
	    	a11 = 1;
	    	a6 = 0;
	    	a22 = 1;
	    	a23 = 0;
	    	a20 = 0;
	    	return 23;
	    } else if((((!(a12==1)&&((((a19==1)||((a22==1)&&!(a6==1)))&&(a5==1))||!(a16==1)))&&!(a26==1))&&((a4==1)&&((((a16==1)&&(((((input==3)&&!(a11==1))&&!(a25==1))&&(a27==1))&&(a18==1)))&&(a10==1))&&(a3==1))))){
	    	a6 = 1;
	    	a11 = 1;
	    	a3 = 2;
	    	a7 = 0;
	    	a12 = 1;
	    	a17 = 0;
	    	return 22;
	    } else if(((!(a17==1)&&((a1==1)&&(((a15==1)&&((!(a11==1)&&((((a27==1)&&!(a26==1))||((a26==1)&&!(a27==1)))&&(input==1)))&&(a15==1)))&&(a12==1))))&&(((a18==1)&&((a16==1)&&(((a3==2)&&((a22==1)&&(a5==1)))&&(a6==1))))&&!(a8==1)))){
	    	a11 = 1;
	    	a0 = 1;
	    	a27 = 0;
	    	a12 = 0;
	    	a6 = 0;
	    	a23 = 0;
	    	a16 = 1;
	    	a3 = 0;
	    	a26 = 1;
	    	return -1;
	    } else if(((((a3==2)&&(((((a29==1)||(a14==1))&&!(a6==1))||(a23==1))||!(a4==1)))&&(a5==1))&&(!(a27==1)&&(((a12==1)&&(((!(a2==1)&&((a22==1)&&((input==1)&&((a26==1)||!(a26==1)))))&&(a18==1))&&(a11==1)))&&!(a14==1))))){
	    	a27 = 1;
	    	a14 = 0;
	    	a15 = 1;
	    	a3 = 0;
	    	a6 = 1;
	    	a10 = 1;
	    	a26 = 1;
	    	return -1;
	    } else if((((!(a2==1)&&(((((input==3)&&(((a26==1)&&!(a27==1))||(((a26==1)&&(a27==1))||((a27==1)&&!(a26==1)))))&&(a6==1))&&(a18==1))&&(a3==2)))&&!(a23==1))&&((((a5==1)&&(((((a17==1)||(a22==1))&&!(a25==1))||(a20==1))&&(a4==1)))&&(a12==1))&&(a11==1)))){
	    	a3 = 0;
	    	a22 = 1;
	    	a26 = 1;
	    	a14 = 0;
	    	a29 = 1;
	    	a27 = 1;
	    	return -1;
	    } else if(((!(a6==1)&&(((!(a25==1)&&((a3==1)&&((a16==1)&&(a26==1))))&&!(a19==1))&&!(a20==1)))&&((((((a1==1)&&((a18==1)&&((!(a12==1)&&(input==3))&&(a5==1))))&&!(a27==1))&&!(a8==1))&&!(a7==1))&&!(a11==1)))){
	    	a6 = 1;
	    	a3 = 0;
	    	a11 = 1;
	    	a20 = 0;
	    	a14 = 0;
	    	a27 = 1;
	    	a12 = 1;
	    	a7 = 0;
	    	return -1;
	    } else if((((a15==1)&&(!(a25==1)&&(((a3==2)&&((((((a5==1)&&(((!(a26==1)&&(a27==1))||((a26==1)&&!(a27==1)))&&(input==1)))&&!(a2==1))&&!(a11==1))&&(a12==1))&&(a18==1)))&&!(a17==1))))&&((!(a16==1)||((a1==1)&&!(a6==1)))&&(a4==1)))){
	    	a4 = 1;
	    	a11 = 1;
	    	a25 = 0;
	    	a26 = 1;
	    	a27 = 1;
	    	a3 = 0;
	    	a23 = 0;
	    	a6 = 1;
	    	return -1;
	    } else if((((((a18==1)&&(((a27==1)&&(!(a11==1)&&(input==4)))&&!(a2==1)))&&!(a6==1))&&!(a12==1))&&((!(a26==1)&&(((a25==1)||(((!(a8==1)&&((a19==1)||(a16==1)))&&!(a17==1))&&!(a8==1)))&&(a3==1)))&&(a5==1)))){
	    	a27 = 0;
	    	a17 = 0;
	    	a22 = 1;
	    	a26 = 1;
	    	a0 = 1;
	    	return 25;
	    } else if(((((!(a19==1)&&((a11==1)&&(((((!(a5==1)&&((input==1)&&((!(a26==1)&&!(a27==1))||((!(a26==1)&&(a27==1))||((a26==1)&&!(a27==1))))))&&!(a12==1))&&(a22==1))&&(a6==1))&&(a18==1))))&&(a10==1))&&(a3==0))&&(((!(a16==1)||(a22==1))||!(a10==1))||!(a29==1)))){
	    	if((a2==1)){
	    		a12 = 1;
	    		a15 = 0;
	    		a2 = 1;
	    		a27 = 1;
	    		a6 = 0;
	    		a26 = 1;
	    		a24 = 0;
	    		a3 = 2;
	    		a5 = 1;
	    	}else{
	    		a6 = 0;
	    		a21 = 0;
	    		a29 = 0;
	    		a26 = 1;
	    		a8 = 1;
	    		a11 = 0;
	    		a27 = 1;
	    		a5 = 1;
	    		a12 = 1;
	    	}  
	    	return -1;
	    } else if(((((a4==1)&&((a22==1)&&((a11==1)&&((a0==1)&&((((input==6)&&(a18==1))&&(a29==1))&&!(a6==1))))))&&(a3==2))&&((a27==1)&&(((a5==1)&&(!(a12==1)&&((a26==1)&&((a22==1)&&(a1==1)))))||!(a22==1))))){
	    	a20 = 0;
	    	a14 = 0;
	    	a25 = 0;
	    	return 23;
	    } else if(((((((a1==1)&&(!(a27==1)&&((a18==1)&&(a16==1))))||(a8==1))||(a20==1))&&(a3==2))&&(((!(a19==1)&&((!(a11==1)&&((((input==6)&&(a5==1))&&(a16==1))&&(a12==1)))&&!(a26==1)))&&!(a19==1))&&(a6==1)))){
	    	a27 = 1;
	    	a12 = 0;
	    	a0 = 1;
	    	a23 = 0;
	    	a29 = 1;
	    	a3 = 1;
	    	return -1;
	    } else if(((((((a29==1)&&(a15==1))||(a14==1))&&(a4==1))&&!(a5==1))&&(((((a18==1)&&((a12==1)&&(!(a2==1)&&(!(a23==1)&&(((((a27==1)&&!(a26==1))||(!(a27==1)&&(a26==1)))&&(input==4))&&!(a17==1))))))&&(a3==0))&&(a6==1))&&(a11==1)))){
	    	a27 = 1;
	    	a3 = 1;
	    	a7 = 1;
	    	a22 = 0;
	    	a11 = 0;
	    	a6 = 0;
	    	a26 = 1;
	    	a12 = 0;
	    	a5 = 1;
	    	a19 = 1;
	    	return -1;
	    } else if((((a17==1)&&((a20==1)&&((!(a11==1)&&((a6==1)&&((a18==1)&&(((input==2)&&((!(a26==1)&&(a27==1))||(!(a27==1)&&(a26==1))))&&!(a0==1)))))&&(a12==1))))&&((!(a16==1)&&(((a5==1)&&((a15==1)&&(a3==2)))&&!(a22==1)))&&(a23==1)))){
	    	a3 = 0;
	    	a6 = 0;
	    	a4 = 0;
	    	a26 = 0;
	    	a27 = 0;
	    	a8 = 1;
	    	a22 = 0;
	    	return -1;
	    } else if(((((a18==1)&&((!(a8==1)&&(((a6==1)&&(input==5))&&!(a23==1)))&&(a12==1)))&&(a5==1))&&((a16==1)&&(!(a27==1)&&(!(a2==1)&&((a20==1)||(!(a26==1)&&(!(a11==1)&&(!(a15==1)||((a10==1)&&(a3==2))))))))))){
	    	a6 = 0;
	    	a22 = 1;
	    	a11 = 1;
	    	a27 = 1;
	    	a12 = 0;
	    	a19 = 0;
	    	a16 = 1;
	    	return 21;
	    } else if((((a4==1)&&((a12==1)&&((a6==1)&&(((a18==1)&&((a10==1)&&(((a16==1)&&(a0==1))&&(a5==1))))&&!(a11==1)))))&&((!(a17==1)&&((((input==3)&&((!(a26==1)&&(a27==1))||((a26==1)&&!(a27==1))))&&!(a20==1))&&(a3==2)))&&(a16==1)))){
	    	a27 = 1;
	    	a26 = 1;
	    	a8 = 0;
	    	a11 = 1;
	    	a3 = 1;
	    	a15 = 1;
	    	return -1;
	    } else if((((!(a7==1)&&(((a6==1)&&((a5==1)&&(((input==2)&&((!(a26==1)&&(a27==1))||((a26==1)&&!(a27==1))))&&(a18==1))))&&(a12==1)))&&!(a8==1))&&((((a4==1)&&((a0==1)&&((a3==2)&&((a10==1)&&!(a11==1)))))&&(a0==1))||(a8==1)))){
	    	a10 = 1;
	    	a27 = 0;
	    	a2 = 0;
	    	a23 = 0;
	    	a26 = 0;
	    	a3 = 1;
	    	return -1;
	    } else if((((a3==2)&&(!(a11==1)&&(!(a17==1)&&((a19==1)||((a4==1)&&((a1==1)&&!(a12==1)))))))&&((((!(a7==1)&&((a5==1)&&((a18==1)&&((((a27==1)&&!(a26==1))||((a26==1)&&!(a27==1)))&&(input==1)))))&&!(a23==1))&&!(a6==1))&&!(a2==1)))){
	    	a12 = 1;
	    	a27 = 0;
	    	a28 = 1;
	    	a26 = 1;
	    	a21 = 1;
	    	return -1;
	    } else if(((!(a29==1)||((a4==1)&&(((a5==1)&&((a17==1)||(a22==1)))&&(a1==1))))&&(!(a12==1)&&(((a26==1)&&((a27==1)&&((a3==2)&&((a11==1)&&(!(a8==1)&&(!(a25==1)&&((input==5)&&(a18==1))))))))&&!(a6==1))))){
	    	a4 = 1;
	    	a22 = 1;
	    	a7 = 0;
	    	return -1;
	    } else if((((((a4==1)&&((!(a20==1)&&(!(a19==1)&&(((((((a6==1)&&(a26==1))&&(a27==1))&&(a12==1))&&!(a11==1))||(((a11==1)&&(!(a12==1)&&(!(a27==1)&&((a26==1)&&!(a6==1)))))||(((!(a27==1)&&(!(a26==1)&&!(a6==1)))&&!(a12==1))&&(a11==1))))&&(input==5))))&&(a5==1)))&&!(a7==1))&&(a3==2))&&((a18==1)&&((a15==1)&&((a1==1)&&(a4==1)))))){
	    	a0 = 1;
	    	a6 = 0;
	    	a26 = 0;
	    	a12 = 0;
	    	a25 = 0;
	    	a27 = 1;
	    	a11 = 1;
	    	a20 = 0;
	    	return -1;
	    } else if(((((((((a27==1)&&(a22==1))&&!(a17==1))&&!(a20==1))&&(a3==1))&&!(a11==1))&&!(a23==1))&&((((a5==1)&&((a29==1)&&((a18==1)&&((((input==1)&&!(a26==1))&&!(a12==1))&&!(a6==1)))))&&(a10==1))&&(a4==1)))){
	    	a7 = 0;
	    	a26 = 1;
	    	a6 = 1;
	    	a11 = 1;
	    	a4 = 1;
	    	a12 = 1;
	    	a3 = 0;
	    	a8 = 0;
	    	return -1;
	    } else if((((((!(a11==1)&&((a5==1)&&(input==2)))&&(a15==1))&&(a1==1))&&(a3==1))&&(!(a12==1)&&(!(a6==1)&&((a0==1)&&((!(a19==1)&&(!(a16==1)||(((a26==1)&&((a15==1)&&(a18==1)))&&!(a27==1))))&&!(a17==1))))))){
	    	a6 = 1;
	    	a25 = 0;
	    	a17 = 0;
	    	a23 = 0;
	    	a3 = 0;
	    	a27 = 1;
	    	a11 = 1;
	    	a12 = 1;
	    	return -1;
	    } else if((((((a22==1)&&((!(a27==1)&&(!(a6==1)&&(((a22==1)&&(a3==1))&&!(a12==1))))&&(a0==1)))&&!(a20==1))||!(a16==1))&&(!(a26==1)&&((a29==1)&&(!(a14==1)&&(!(a11==1)&&((a5==1)&&((input==4)&&(a18==1))))))))){
	    	a11 = 1;
	    	a10 = 1;
	    	a12 = 1;
	    	a26 = 1;
	    	a15 = 1;
	    	a6 = 1;
	    	a3 = 0;
	    	a27 = 1;
	    	a29 = 1;
	    	return -1;
	    } else if(((((a5==1)&&((!(a11==1)&&(!(a23==1)&&((a29==1)&&(((((a27==1)&&!(a26==1))||((a26==1)&&!(a27==1)))&&(input==2))&&!(a19==1)))))&&!(a23==1)))&&!(a6==1))&&(!(a20==1)&&(!(a12==1)&&(((a29==1)&&((a22==1)&&(a3==2)))&&(a18==1)))))){
	    	a6 = 1;
	    	a11 = 1;
	    	a29 = 0;
	    	a26 = 1;
	    	a27 = 0;
	    	a13 = 1;
	    	a2 = 1;
	    	return -1;
	    } else if(((((a29==1)&&((((a22==1)&&(((((((a27==1)&&(a26==1))||((a27==1)&&!(a26==1)))||(!(a27==1)&&(a26==1)))&&(input==5))&&(a6==1))&&(a5==1)))&&(a3==2))&&!(a20==1)))&&!(a2==1))&&((a11==1)&&((((!(a16==1)||(a1==1))&&!(a25==1))&&(a18==1))&&(a12==1))))){
	    	a15 = 1;
	    	a27 = 1;
	    	a3 = 0;
	    	a16 = 1;
	    	a22 = 1;
	    	a26 = 1;
	    	return -1;
	    } else if(((!(a15==1)||(((!(a23==1)&&(((((a0==1)&&!(a11==1))||(a20==1))&&(a5==1))&&(a6==1)))&&(a1==1))||(a8==1)))&&((((a0==1)&&(((a3==2)&&((input==3)&&(a12==1)))&&!(a27==1)))&&(a18==1))&&!(a26==1)))){
	    	a26 = 1;
	    	a11 = 1;
	    	a23 = 0;
	    	a10 = 1;
	    	a6 = 0;
	    	a12 = 0;
	    	a3 = 1;
	    	a4 = 1;
	    	return -1;
	    } else if(((!(a6==1)&&((!(a8==1)&&((a16==1)&&((a22==1)&&((a26==1)&&(!(a11==1)&&(input==6))))))&&(a18==1)))&&(!(a27==1)&&((((!(a1==1)||(((a22==1)&&!(a12==1))&&(a0==1)))&&(a3==1))&&(a10==1))&&(a5==1))))){
	    	a27 = 1;
	    	a3 = 0;
	    	a6 = 1;
	    	a12 = 1;
	    	a29 = 1;
	    	a19 = 0;
	    	a4 = 1;
	    	a11 = 1;
	    	return -1;
	    } else if(((!(a26==1)&&(((a3==1)&&((a1==1)&&((!(a6==1)&&((a5==1)&&(input==6)))&&(a18==1))))&&!(a11==1)))&&(!(a12==1)&&((((a0==1)&&((((a0==1)&&(a10==1))||!(a10==1))&&(a22==1)))&&(a29==1))&&!(a27==1))))){
	    	if((a7==1)){
	    		a23 = 0;
	    		a3 = 2;
	    		a6 = 1;
	    		a1 = 1;
	    	}else{
	    		a19 = 0;
	    		a26 = 1;
	    		a0 = 1;
	    		a12 = 1;
	    		a3 = 2;
	    		a11 = 1;
	    		a27 = 1;
	    	}  
	    	return 25;
	    } else if(((!(a29==1)||((!(a11==1)&&((a22==1)&&(a16==1)))&&(a5==1)))&&((a10==1)&&((((!(a7==1)&&((a29==1)&&(((!(a12==1)&&(!(a27==1)&&(!(a26==1)&&(a6==1))))||((a12==1)&&((!(a6==1)&&(a26==1))&&(a27==1))))&&(input==4))))&&(a18==1))&&(a3==2))&&(a29==1))))){
	    	a22 = 1;
	    	a6 = 1;
	    	a4 = 1;
	    	a3 = 0;
	    	a0 = 1;
	    	a11 = 1;
	    	a12 = 1;
	    	a26 = 1;
	    	a27 = 1;
	    	return -1;
	    } else if(((!(a25==1)&&((a15==1)&&((((a5==1)&&(((a3==2)&&(((!(a26==1)&&!(a6==1))&&!(a27==1))&&!(a12==1)))&&!(a11==1)))||(((a11==1)&&(((((a6==1)&&(a26==1))&&(a27==1))&&(a12==1))&&(a3==0)))&&!(a5==1)))&&(input==6))))&&((a14==1)||(!(a2==1)&&((((a4==1)&&(a0==1))&&(a18==1))&&!(a19==1)))))){
	    	a10 = 0;
	    	a8 = 1;
	    	a5 = 1;
	    	a12 = 1;
	    	a3 = 0;
	    	a9 = 0;
	    	a11 = 0;
	    	a26 = 1;
	    	a27 = 1;
	    	a6 = 0;
	    	return -1;
	    } else if((((a10==1)||!(a16==1))&&((a0==1)&&(!(a25==1)&&(!(a17==1)&&((a18==1)&&((!(a19==1)&&((input==1)&&(((a5==1)&&(!(a11==1)&&(((!(a27==1)&&(!(a6==1)&&!(a26==1)))&&!(a12==1))&&(a3==2))))||(((a11==1)&&((a3==0)&&((a12==1)&&((a27==1)&&((a6==1)&&(a26==1))))))&&!(a5==1)))))&&!(a25==1)))))))){
	    	if((a13==1)){
	    		a4 = 0;
	    		a5 = 1;
	    		a26 = 1;
	    		a11 = 1;
	    		a12 = 0;
	    		a28 = 0;
	    		a2 = 1;
	    		a3 = 0;
	    		a27 = 0;
	    		a6 = 1;
	    	}else{
	    		a8 = 1;
	    		a3 = 2;
	    		a27 = 1;
	    		a29 = 0;
	    		a5 = 1;
	    		a6 = 0;
	    		a11 = 0;
	    		a12 = 1;
	    		a26 = 0;
	    		a24 = 1;
	    	}  
	    	return -1;
	    } else if(((!(a22==1)||((a19==1)||(!(a10==1)||((a12==1)&&(!(a27==1)&&(((a0==1)&&(a18==1))&&(a11==1)))))))&&(!(a20==1)&&((a10==1)&&(((a5==1)&&(!(a6==1)&&((a0==1)&&((input==5)&&((a26==1)||!(a26==1))))))&&(a3==2)))))){
	    	a6 = 1;
	    	a23 = 0;
	    	a7 = 0;
	    	a15 = 1;
	    	a3 = 0;
	    	a26 = 1;
	    	a27 = 1;
	    	return -1;
	    } else if((((a12==1)&&(((a2==1)||(a10==1))&&!(a25==1)))&&(((a3==0)&&(((a18==1)&&(!(a23==1)&&((((a15==1)&&((a29==1)&&(((!(a26==1)&&(a27==1))||(!(a27==1)&&(a26==1)))&&(input==1))))&&!(a5==1))&&(a11==1))))&&(a1==1)))&&(a6==1)))){
	    	if((a29==1)){
	    		a5 = 1;
	    		a21 = 0;
	    		a12 = 0;
	    		a11 = 0;
	    		a26 = 0;
	    		a22 = 0;
	    		a3 = 1;
	    		a13 = 0;
	    		a27 = 0;
	    	}else{
	    		a5 = 1;
	    		a9 = 0;
	    		a11 = 0;
	    		a16 = 0;
	    		a26 = 0;
	    		a20 = 1;
	    		a6 = 0;
	    		a27 = 1;
	    	}  
	    	return 25;
	    } else if((((a3==2)&&((((a29==1)&&(((input==6)&&((a26==1)||!(a26==1)))&&(a4==1)))&&(a29==1))&&!(a20==1)))&&(!(a4==1)||(((a11==1)&&((a5==1)&&(((a18==1)&&((a12==1)&&((a27==1)&&(a29==1))))&&(a10==1))))&&!(a6==1))))){
	    	a8 = 0;
	    	a4 = 1;
	    	a6 = 1;
	    	a3 = 0;
	    	a26 = 1;
	    	a15 = 1;
	    	return -1;
	    } else if(((!(a16==1)||(!(a26==1)&&(((a15==1)&&(a3==2))&&!(a17==1))))&&((a29==1)&&((a5==1)&&(((!(a23==1)&&((!(a23==1)&&((a27==1)&&(!(a12==1)&&(!(a6==1)&&(input==4)))))&&(a18==1)))&&(a11==1))&&(a16==1)))))){
	    	a6 = 1;
	    	a27 = 0;
	    	a16 = 1;
	    	a23 = 0;
	    	a26 = 1;
	    	a20 = 0;
	    	return -1;
	    } else if((((a15==1)&&(((a11==1)&&(((a5==1)&&((!(a10==1)||(a1==1))&&(a3==2)))||(a7==1)))||!(a22==1)))&&((((a18==1)&&((!(a6==1)&&((!(a12==1)&&(input==3))&&(a1==1)))&&(a29==1)))&&(a27==1))&&!(a26==1)))){
	    	a2 = 0;
	    	a0 = 1;
	    	a10 = 1;
	    	return -1;
	    } else if(((!(a14==1)&&(((a5==1)&&(!(a6==1)&&((input==4)&&(((!(a26==1)&&!(a27==1))&&(a12==1))||(!(a12==1)&&((a27==1)&&(a26==1)))))))&&!(a23==1)))&&((a2==1)||((!(a1==1)||(((((a18==1)&&(a1==1))&&!(a11==1))&&(a29==1))&&(a3==2)))&&!(a8==1))))){
	    	a27 = 1;
	    	a16 = 0;
	    	a26 = 1;
	    	a12 = 0;
	    	a8 = 1;
	    	a6 = 1;
	    	a3 = 1;
	    	a23 = 1;
	    	return -1;
	    } else if((((a18==1)&&((a7==1)||(!(a2==1)&&(((((a16==1)&&(a11==1))&&(a6==1))&&!(a23==1))||(a23==1)))))&&((a5==1)&&((a3==2)&&((!(a14==1)&&((a12==1)&&((input==2)&&((((a26==1)&&(a27==1))||((a27==1)&&!(a26==1)))||((a26==1)&&!(a27==1))))))&&(a22==1)))))){
	    	a17 = 0;
	    	a19 = 0;
	    	a6 = 0;
	    	a26 = 1;
	    	a27 = 0;
	    	a1 = 1;
	    	return 25;
	    } else if((((a4==1)&&(((a6==1)&&((a10==1)&&!(a11==1)))&&(a12==1)))&&(!(a7==1)&&(((a5==1)&&(((((((((a27==1)&&!(a26==1))||((a26==1)&&!(a27==1)))&&(input==6))&&(a3==2))&&(a16==1))&&!(a23==1))&&(a18==1))&&(a0==1)))&&!(a19==1))))){
	    	a19 = 0;
	    	a27 = 0;
	    	a26 = 0;
	    	a8 = 0;
	    	return 26;
	    } else if(((((!(a16==1)||((((a5==1)&&(((a22==1)&&!(a23==1))||!(a22==1)))&&(a6==1))&&(a16==1)))&&(a18==1))||(a2==1))&&((((a3==2)&&((input==4)&&(((!(a27==1)&&!(a26==1))&&(a12==1))||(!(a12==1)&&((a27==1)&&(a26==1))))))&&(a16==1))&&(a11==1)))){
	    	a3 = 0;
	    	a27 = 1;
	    	a16 = 1;
	    	a12 = 1;
	    	a19 = 0;
	    	a26 = 1;
	    	a22 = 1;
	    	return -1;
	    } else if((((a18==1)&&((a4==1)&&((a14==1)||((!(a5==1)&&(a16==1))||!(a1==1)))))&&((((((a11==1)&&((a12==1)&&((a6==1)&&((((a27==1)&&!(a26==1))||((a26==1)&&!(a27==1)))&&(input==5)))))&&!(a8==1))&&!(a14==1))&&(a3==0))&&!(a2==1)))){
	    	if((a0==1)){
	    		a17 = 1;
	    		a3 = 2;
	    		a20 = 1;
	    		a27 = 0;
	    		a26 = 0;
	    		a12 = 0;
	    		a11 = 0;
	    		a5 = 1;
	    		a1 = 0;
	    	}else{
	    		a27 = 0;
	    		a1 = 0;
	    		a3 = 1;
	    		a6 = 0;
	    		a9 = 1;
	    		a15 = 0;
	    		a5 = 1;
	    		a26 = 1;
	    	}  
	    	return -1;
	    } else if(((!(a20==1)&&((((!(a10==1)||((a6==1)&&((!(a0==1)||(a10==1))&&!(a2==1))))||!(a1==1))&&!(a14==1))&&(a11==1)))&&((a18==1)&&(((a12==1)&&(((input==3)&&((!(a26==1)&&(a27==1))||(!(a27==1)&&(a26==1))))&&!(a5==1)))&&(a3==0))))){
	    	if((a22==1)){
	    		a16 = 0;
	    		a3 = 2;
	    		a23 = 1;
	    		a27 = 0;
	    		a11 = 0;
	    		a5 = 1;
	    		a26 = 1;
	    		a1 = 0;
	    	}else{
	    		a27 = 1;
	    		a3 = 2;
	    		a2 = 1;
	    		a11 = 0;
	    		a10 = 0;
	    		a16 = 0;
	    		a26 = 0;
	    		a5 = 1;
	    	}  
	    	return -1;
	    } else if((((((a18==1)&&(!(a20==1)&&(a0==1)))&&(a12==1))||!(a1==1))&&(((((a11==1)&&(!(a23==1)&&(!(a5==1)&&((((input==6)&&(((a27==1)&&!(a26==1))||(!(a27==1)&&(a26==1))))&&!(a14==1))&&!(a20==1)))))&&(a6==1))&&(a3==0))&&(a1==1)))){
	    	if((a21==1)){
	    		a22 = 0;
	    		a12 = 0;
	    		a24 = 1;
	    		a27 = 1;
	    		a26 = 1;
	    		a5 = 1;
	    		a9 = 0;
	    	}else{
	    		a28 = 1;
	    		a5 = 1;
	    		a11 = 0;
	    		a7 = 1;
	    		a3 = 2;
	    		a4 = 0;
	    		a27 = 1;
	    		a12 = 0;
	    		a26 = 0;
	    	}  
	    	return -1;
	    } else if(((!(a19==1)&&((a4==1)&&((((a18==1)&&(a0==1))&&(a11==1))&&!(a5==1))))&&((a10==1)&&((a15==1)&&((!(a14==1)&&((a6==1)&&((a3==0)&&((((!(a26==1)&&!(a27==1))&&(a12==1))||(!(a12==1)&&((a27==1)&&(a26==1))))&&(input==1)))))&&(a16==1)))))){
	    	a27 = 0;
	    	a25 = 1;
	    	a2 = 1;
	    	a23 = 1;
	    	a26 = 1;
	    	a12 = 1;
	    	a5 = 1;
	    	return -1;
	    } else if((((a0==1)&&((((a6==1)&&(!(a5==1)&&((((a27==1)&&!(a26==1))||(!(a27==1)&&(a26==1)))&&(input==2))))&&!(a2==1))&&(a3==0)))&&((a22==1)&&((a12==1)&&(((a18==1)&&((((a22==1)&&(a11==1))&&!(a23==1))||!(a4==1)))&&!(a7==1)))))){
	    	a27 = 0;
	    	a3 = 2;
	    	a26 = 0;
	    	a5 = 1;
	    	a7 = 1;
	    	a11 = 0;
	    	a28 = 0;
	    	a2 = 1;
	    	return -1;
	    } else if(((((!(a11==1)&&(!(a6==1)&&((((input==4)&&((!(a26==1)&&(a27==1))||((a26==1)&&!(a27==1))))&&!(a8==1))&&(a18==1))))&&(a16==1))&&!(a17==1))&&((a1==1)&&((a20==1)||((((a5==1)&&((a3==2)&&(a1==1)))&&(a12==1))||!(a4==1)))))){
	    	a11 = 1;
	    	a27 = 1;
	    	a25 = 0;
	    	a17 = 0;
	    	a6 = 1;
	    	a3 = 0;
	    	a7 = 0;
	    	a26 = 1;
	    	return -1;
	    } else if((((((!(a7==1)&&(((input==3)&&(a5==1))&&(a16==1)))&&(a18==1))&&!(a27==1))&&!(a26==1))&&((!(a11==1)&&((!(a17==1)&&((a3==1)&&(!(a23==1)&&(!(a16==1)||((a10==1)||(a14==1))))))&&!(a12==1)))&&!(a6==1)))){
	    	a6 = 1;
	    	a10 = 1;
	    	a3 = 2;
	    	a0 = 1;
	    	a11 = 1;
	    	a26 = 1;
	    	return 21;
	    } else if((((a27==1)&&(!(a12==1)&&((a11==1)&&((!(a2==1)&&((a18==1)&&(((!(a25==1)&&(((a3==2)&&(input==2))&&(a15==1)))&&(a29==1))&&(a15==1))))&&!(a25==1)))))&&((a5==1)&&(((a10==1)&&(a26==1))&&!(a6==1))))){
	    	a17 = 0;
	    	a15 = 1;
	    	a2 = 0;
	    	return 23;
	    } 
	    if(((((((((a26==1)&&!(a6==1))&&!(a27==1))&&!(a12==1))&&(a3==1))&&(a11==1))&&(a5==1))&&(a18==1))){
	    	error_45: exit(0);
	    } 
	    if(((((((((a26==1)&&(a6==1))&&(a27==1))&&!(a12==1))&&(a3==1))&&(a11==1))&&(a5==1))&&(a18==1))){
	    	error_35: exit(0);
	    } 
	    if((((((((!(a26==1)&&(a6==1))&&(a27==1))&&!(a12==1))&&(a3==1))&&!(a11==1))&&(a5==1))&&(a18==1))){
	    	error_52: exit(0);
	    } 
	    if(((((((((a26==1)&&!(a6==1))&&(a27==1))&&(a12==1))&&(a3==1))&&(a11==1))&&(a5==1))&&(a18==1))){
	    	error_39: exit(0);
	    } 
	    if(((((((((a26==1)&&!(a6==1))&&!(a27==1))&&(a12==1))&&(a3==0))&&(a11==1))&&(a5==1))&&(a18==1))){
	    	error_9: exit(0);
	    } 
	    if(((((((((a26==1)&&(a6==1))&&!(a27==1))&&!(a12==1))&&(a3==1))&&(a11==1))&&(a5==1))&&(a18==1))){
	    	error_37: exit(0);
	    } 
	    if(((((((((a26==1)&&!(a6==1))&&(a27==1))&&!(a12==1))&&(a3==1))&&(a11==1))&&(a5==1))&&(a18==1))){
	    	error_43: exit(0);
	    } 
	    if(((((((((a26==1)&&(a6==1))&&(a27==1))&&(a12==1))&&(a3==1))&&(a11==1))&&(a5==1))&&(a18==1))){
	    	error_31: exit(0);
	    } 
	    if((((((((!(a26==1)&&!(a6==1))&&(a27==1))&&!(a12==1))&&(a3==0))&&!(a11==1))&&(a5==1))&&(a18==1))){
	    	error_28: exit(0);
	    } 
	    if(((((((((a26==1)&&!(a6==1))&&(a27==1))&&!(a12==1))&&(a3==0))&&!(a11==1))&&(a5==1))&&(a18==1))){
	    	error_27: exit(0);
	    } 
	    if((((((((!(a26==1)&&(a6==1))&&!(a27==1))&&(a12==1))&&(a3==1))&&!(a11==1))&&(a5==1))&&(a18==1))){
	    	error_50: exit(0);
	    } 
	    if(((((((((a26==1)&&!(a6==1))&&!(a27==1))&&!(a12==1))&&(a3==0))&&(a11==1))&&(a5==1))&&(a18==1))){
	    	error_13: exit(0);
	    } 
	    if((((((((!(a26==1)&&!(a6==1))&&!(a27==1))&&(a12==1))&&(a3==0))&&!(a11==1))&&(a5==1))&&(a18==1))){
	    	error_26: exit(0);
	    } 
	    if((((((((!(a26==1)&&!(a6==1))&&(a27==1))&&(a12==1))&&(a3==0))&&(a11==1))&&(a5==1))&&(a18==1))){
	    	error_8: exit(0);
	    } 
	    if(((((((((a26==1)&&(a6==1))&&!(a27==1))&&!(a12==1))&&(a3==0))&&(a11==1))&&(a5==1))&&(a18==1))){
	    	error_5: exit(0);
	    } 
	    if(((((((((a26==1)&&(a6==1))&&!(a27==1))&&(a12==1))&&(a3==1))&&(a11==1))&&(a5==1))&&(a18==1))){
	    	error_33: exit(0);
	    } 
	    if((((((((!(a26==1)&&!(a6==1))&&!(a27==1))&&(a12==1))&&(a3==1))&&!(a11==1))&&(a5==1))&&(a18==1))){
	    	error_58: exit(0);
	    } 
	    if(((((((((a26==1)&&!(a6==1))&&!(a27==1))&&(a12==1))&&(a3==1))&&!(a11==1))&&(a5==1))&&(a18==1))){
	    	error_57: exit(0);
	    } 
	    if(((((((((a26==1)&&!(a6==1))&&(a27==1))&&(a12==1))&&(a3==1))&&!(a11==1))&&(a5==1))&&(a18==1))){
	    	error_55: exit(0);
	    } 
	    if((((((((!(a26==1)&&!(a6==1))&&(a27==1))&&!(a12==1))&&(a3==0))&&(a11==1))&&(a5==1))&&(a18==1))){
	    	error_12: exit(0);
	    } 
	    if(((((((((a26==1)&&(a6==1))&&(a27==1))&&!(a12==1))&&(a3==0))&&(a11==1))&&(a5==1))&&(a18==1))){
	    	error_3: exit(0);
	    } 
	    if((((((((!(a26==1)&&(a6==1))&&(a27==1))&&(a12==1))&&(a3==0))&&!(a11==1))&&(a5==1))&&(a18==1))){
	    	error_16: exit(0);
	    } 
	    if((((((((!(a26==1)&&(a6==1))&&!(a27==1))&&!(a12==1))&&(a3==1))&&!(a11==1))&&(a5==1))&&(a18==1))){
	    	error_54: exit(0);
	    } 
	    if((((((((!(a26==1)&&(a6==1))&&!(a27==1))&&!(a12==1))&&(a3==0))&&!(a11==1))&&(a5==1))&&(a18==1))){
	    	error_22: exit(0);
	    } 
	    if(((((((((a26==1)&&(a6==1))&&!(a27==1))&&(a12==1))&&(a3==1))&&!(a11==1))&&(a5==1))&&(a18==1))){
	    	error_49: exit(0);
	    } 
	    if((((((((!(a26==1)&&(a6==1))&&!(a27==1))&&!(a12==1))&&(a3==0))&&(a11==1))&&(a5==1))&&(a18==1))){
	    	error_6: exit(0);
	    } 
	    if((((((((!(a26==1)&&!(a6==1))&&!(a27==1))&&!(a12==1))&&(a3==0))&&(a11==1))&&(a5==1))&&(a18==1))){
	    	error_14: exit(0);
	    } 
	    if(((((((((a26==1)&&!(a6==1))&&(a27==1))&&(a12==1))&&(a3==0))&&!(a11==1))&&(a5==1))&&(a18==1))){
	    	error_23: exit(0);
	    } 
	    if(((((((((a26==1)&&!(a6==1))&&(a27==1))&&(a12==1))&&(a3==0))&&(a11==1))&&(a5==1))&&(a18==1))){
	    	error_7: __VERIFIER_error();
	    } 
	    if((((((((!(a26==1)&&!(a6==1))&&(a27==1))&&(a12==1))&&(a3==1))&&!(a11==1))&&(a5==1))&&(a18==1))){
	    	error_56: exit(0);
	    } 
	    if(((((((((a26==1)&&!(a6==1))&&(a27==1))&&!(a12==1))&&(a3==1))&&!(a11==1))&&(a5==1))&&(a18==1))){
	    	error_59: exit(0);
	    } 
	    if((((((((!(a26==1)&&!(a6==1))&&!(a27==1))&&!(a12==1))&&(a3==0))&&!(a11==1))&&(a5==1))&&(a18==1))){
	    	error_30: exit(0);
	    } 
	    if(((((((((a26==1)&&(a6==1))&&(a27==1))&&(a12==1))&&(a3==0))&&(a11==1))&&(a5==1))&&(a18==1))){
	    	globalError: exit(0);
	    } 
	    if((((((((!(a26==1)&&!(a6==1))&&(a27==1))&&!(a12==1))&&(a3==1))&&(a11==1))&&(a5==1))&&(a18==1))){
	    	error_44: exit(0);
	    } 
	    if(((((((((a26==1)&&!(a6==1))&&!(a27==1))&&!(a12==1))&&(a3==0))&&!(a11==1))&&(a5==1))&&(a18==1))){
	    	error_29: exit(0);
	    } 
	    if((((((((!(a26==1)&&(a6==1))&&(a27==1))&&!(a12==1))&&(a3==1))&&(a11==1))&&(a5==1))&&(a18==1))){
	    	error_36: exit(0);
	    } 
	    if(((((((((a26==1)&&!(a6==1))&&!(a27==1))&&(a12==1))&&(a3==0))&&!(a11==1))&&(a5==1))&&(a18==1))){
	    	error_25: exit(0);
	    } 
	    if((((((((!(a26==1)&&!(a6==1))&&!(a27==1))&&(a12==1))&&(a3==0))&&(a11==1))&&(a5==1))&&(a18==1))){
	    	error_10: exit(0);
	    } 
	    if(((((((((a26==1)&&!(a6==1))&&!(a27==1))&&(a12==1))&&(a3==1))&&(a11==1))&&(a5==1))&&(a18==1))){
	    	error_41: exit(0);
	    } 
	    if((((((((!(a26==1)&&(a6==1))&&(a27==1))&&(a12==1))&&(a3==1))&&!(a11==1))&&(a5==1))&&(a18==1))){
	    	error_48: exit(0);
	    } 
	    if((((((((!(a26==1)&&!(a6==1))&&(a27==1))&&(a12==1))&&(a3==1))&&(a11==1))&&(a5==1))&&(a18==1))){
	    	error_40: exit(0);
	    } 
	    if((((((((!(a26==1)&&!(a6==1))&&!(a27==1))&&!(a12==1))&&(a3==1))&&(a11==1))&&(a5==1))&&(a18==1))){
	    	error_46: exit(0);
	    } 
	    if(((((((((a26==1)&&(a6==1))&&!(a27==1))&&(a12==1))&&(a3==0))&&(a11==1))&&(a5==1))&&(a18==1))){
	    	error_1: exit(0);
	    } 
	    if(((((((((a26==1)&&(a6==1))&&(a27==1))&&!(a12==1))&&(a3==0))&&!(a11==1))&&(a5==1))&&(a18==1))){
	    	error_19: exit(0);
	    } 
	    if(((((((((a26==1)&&(a6==1))&&(a27==1))&&!(a12==1))&&(a3==1))&&!(a11==1))&&(a5==1))&&(a18==1))){
	    	error_51: exit(0);
	    } 
	    if((((((((!(a26==1)&&(a6==1))&&(a27==1))&&(a12==1))&&(a3==1))&&(a11==1))&&(a5==1))&&(a18==1))){
	    	error_32: exit(0);
	    } 
	    if((((((((!(a26==1)&&(a6==1))&&!(a27==1))&&(a12==1))&&(a3==1))&&(a11==1))&&(a5==1))&&(a18==1))){
	    	error_34: exit(0);
	    } 
	    if((((((((!(a26==1)&&!(a6==1))&&(a27==1))&&(a12==1))&&(a3==0))&&!(a11==1))&&(a5==1))&&(a18==1))){
	    	error_24: exit(0);
	    } 
	    if((((((((!(a26==1)&&(a6==1))&&(a27==1))&&(a12==1))&&(a3==0))&&(a11==1))&&(a5==1))&&(a18==1))){
	    	error_0: exit(0);
	    } 
	    if(((((((((a26==1)&&!(a6==1))&&(a27==1))&&!(a12==1))&&(a3==0))&&(a11==1))&&(a5==1))&&(a18==1))){
	    	error_11: exit(0);
	    } 
	    if(((((((((a26==1)&&(a6==1))&&!(a27==1))&&!(a12==1))&&(a3==1))&&!(a11==1))&&(a5==1))&&(a18==1))){
	    	error_53: exit(0);
	    } 
	    if((((((((!(a26==1)&&(a6==1))&&(a27==1))&&!(a12==1))&&(a3==0))&&!(a11==1))&&(a5==1))&&(a18==1))){
	    	error_20: exit(0);
	    } 
	    if((((((((!(a26==1)&&!(a6==1))&&!(a27==1))&&(a12==1))&&(a3==1))&&(a11==1))&&(a5==1))&&(a18==1))){
	    	error_42: exit(0);
	    } 
	    if(((((((((a26==1)&&(a6==1))&&(a27==1))&&(a12==1))&&(a3==1))&&!(a11==1))&&(a5==1))&&(a18==1))){
	    	error_47: exit(0);
	    } 
	    if((((((((!(a26==1)&&(a6==1))&&(a27==1))&&!(a12==1))&&(a3==0))&&(a11==1))&&(a5==1))&&(a18==1))){
	    	error_4: exit(0);
	    } 
	    if(((((((((a26==1)&&(a6==1))&&!(a27==1))&&(a12==1))&&(a3==0))&&!(a11==1))&&(a5==1))&&(a18==1))){
	    	error_17: exit(0);
	    } 
	    if(((((((((a26==1)&&(a6==1))&&(a27==1))&&(a12==1))&&(a3==0))&&!(a11==1))&&(a5==1))&&(a18==1))){
	    	error_15: exit(0);
	    } 
	    if((((((((!(a26==1)&&(a6==1))&&!(a27==1))&&!(a12==1))&&(a3==1))&&(a11==1))&&(a5==1))&&(a18==1))){
	    	error_38: exit(0);
	    } 
	    if(((((((((a26==1)&&(a6==1))&&!(a27==1))&&!(a12==1))&&(a3==0))&&!(a11==1))&&(a5==1))&&(a18==1))){
	    	error_21: exit(0);
	    } 
	    if((((((((!(a26==1)&&(a6==1))&&!(a27==1))&&(a12==1))&&(a3==0))&&!(a11==1))&&(a5==1))&&(a18==1))){
	    	error_18: exit(0);
	    } 
	    if((((((((!(a26==1)&&(a6==1))&&!(a27==1))&&(a12==1))&&(a3==0))&&(a11==1))&&(a5==1))&&(a18==1))){
	    	error_2: exit(0);
	    } 
	    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);

    }
}