int calculate_output(int); int calculate_output2(int); int calculate_output3(int); int calculate_output4(int); extern void __VERIFIER_error(void); extern int __VERIFIER_nondet_int(void); extern void exit(int); // inputs int f= 6; int e= 5; int d= 4; int b= 2; int a= 1; int c= 3; // outputs int u = 21; int v = 22; int w = 23; int x = 24; int y = 25; int z = 26; int a3 = 1; int a4 = 17; int a25 = 1; int a1 = 1; int a26 = 18; int a28 = 15; int a7 = 1; int a14 = 19; int calculate_output2(int input); int calculate_output3(int input); int calculate_output4(int input); int calculate_output(int input) { if((((a25==1)&&((a1==1)&&((input==5)&&((((((a4==17)&&(a26==19))&&(a28==17))&&!(a7==1))&&(a14==20))||(((a7==1)&&(((a26==17)&&(a4==18))&&(a28==15)))&&(a14==18))))))&&(a3==1))){ a28 = 15; a26 = 17; a4 = 16; a14 = 18; a7 = 1; return -1; } else if((((a25==1)&&(((a28==16)&&((a4==17)&&((a1==1)&&(((((a7==1)&&(a26==18))||((a26==19)&&(a7==1)))||(!(a7==1)&&(a26==17)))&&(input==4)))))&&!(a3==1)))&&(a14==20))){ a26 = 19; a28 = 15; a7 = 0; return -1; } else if(((a28==17)&&((a1==1)&&((a25==1)&&((a7==1)&&((a4==17)&&(((a14==18)&&((input==4)&&((a26==17)||(a26==18))))&&!(a3==1)))))))){ a28 = 15; a4 = 16; a26 = 17; a3 = 1; return -1; } else if((!(a7==1)&&(!(a3==1)&&(((a28==16)&&((a25==1)&&((a4==17)&&((((a26==17)||(a26==18))&&(input==6))&&(a1==1)))))&&(a14==19))))){ a7 = 1; a26 = 17; a28 = 15; a4 = 16; a3 = 1; a14 = 18; return -1; } else if(((a28==16)&&((((a14==18)&&((!(a7==1)&&((a26==18)&&((a3==1)&&(input==1))))&&(a1==1)))&&(a25==1))&&(a4==18)))){ a7 = 1; a28 = 15; a4 = 16; a26 = 17; return -1; } else if((!(a3==1)&&((a28==17)&&((a25==1)&&((((input==5)&&((((a14==18)&&((a26==19)&&!(a7==1)))||((a14==19)&&((a7==1)&&(a26==17))))||((a14==19)&&((a26==18)&&(a7==1)))))&&(a4==17))&&(a1==1)))))){ a28 = 15; a4 = 16; a7 = 1; a14 = 18; a26 = 17; a3 = 1; return -1; } else if(((a1==1)&&((a26==17)&&((a4==18)&&(!(a7==1)&&((((a25==1)&&((input==3)&&(a28==15)))&&(a3==1))&&(a14==20))))))){ a14 = 18; a4 = 16; a7 = 1; return -1; } else if(((((((a1==1)&&(((a14==20)&&((input==2)&&(a26==17)))&&!(a7==1)))&&(a28==15))&&(a25==1))&&(a4==17))&&!(a3==1))){ a7 = 1; a28 = 17; a4 = 16; a14 = 19; a26 = 18; return -1; } else if(((a28==17)&&((a4==17)&&((a25==1)&&((a3==1)&&((a14==20)&&((a1==1)&&((input==6)&&((((a7==1)&&(a26==19))||((a26==17)&&!(a7==1)))||(!(a7==1)&&(a26==18))))))))))){ a28 = 15; a14 = 18; a4 = 16; a7 = 1; a26 = 17; return -1; } else if(((((a4==17)&&((((((!(a7==1)&&(a26==19))&&(a14==19))||((a14==20)&&((a7==1)&&(a26==17))))&&(input==3))&&(a28==15))&&(a25==1)))&&(a3==1))&&(a1==1))){ a14 = 18; a26 = 17; a7 = 1; a4 = 16; return -1; } else if((((a28==16)&&((!(a7==1)&&((a1==1)&&((a4==17)&&((((a26==18)||(a26==19))&&(input==5))&&!(a3==1)))))&&(a14==18)))&&(a25==1))){ a4 = 16; a28 = 15; a7 = 1; a3 = 1; a26 = 17; return -1; } else if(((a25==1)&&(((a1==1)&&(((a7==1)&&((((input==2)&&(a4==17))&&(a28==15))&&(a3==1)))&&(a26==18)))&&(a14==19)))){ a26 = 17; a14 = 20; return 24; } else if((((a26==18)&&((a7==1)&&((a28==16)&&(((((a25==1)&&(input==2))&&(a4==18))&&(a14==19))&&(a1==1)))))&&!(a3==1))){ a7 = 0; a4 = 16; a3 = 1; return -1; } else if(((a4==18)&&((a7==1)&&(!(a3==1)&&((a14==19)&&(((a1==1)&&((a28==16)&&((input==1)&&(a26==18))))&&(a25==1))))))){ a28 = 15; a3 = 1; a7 = 0; a4 = 16; a14 = 20; return -1; } else if(((a25==1)&&(!(a3==1)&&((a28==16)&&(((((input==3)&&((!(a7==1)&&(a26==17))||(((a7==1)&&(a26==18))||((a7==1)&&(a26==19)))))&&(a14==20))&&(a1==1))&&(a4==17)))))){ a7 = 1; a14 = 18; a28 = 15; a4 = 16; a26 = 17; a3 = 1; return -1; } else if(((a4==17)&&((a25==1)&&((a14==20)&&(((!(a3==1)&&((input==5)&&((((a7==1)&&(a26==18))||((a26==19)&&(a7==1)))||((a26==17)&&!(a7==1)))))&&(a1==1))&&(a28==16)))))){ a26 = 18; a28 = 15; a7 = 0; return 26; } else if(((((((((a7==1)&&(((a26==19)||((a26==17)||(a26==18)))&&(input==5)))&&(a1==1))&&!(a3==1))&&(a25==1))&&(a14==20))&&(a4==18))&&(a28==15))){ a4 = 16; a26 = 17; a3 = 1; a14 = 18; return -1; } else if((((a26==19)&&((a7==1)&&(((((a14==18)&&((input==4)&&(a1==1)))&&!(a3==1))&&(a25==1))&&(a28==15))))&&(a4==16))){ a3 = 1; a26 = 17; return -1; } else if(((a26==18)&&(((a28==15)&&((a7==1)&&((a25==1)&&(((a4==17)&&((a14==19)&&(input==6)))&&(a3==1)))))&&(a1==1)))){ a7 = 0; a26 = 17; return 21; } else if((((a14==20)&&(((a28==15)&&((((a4==17)&&((input==5)&&(a3==1)))&&(a26==19))&&(a25==1)))&&(a1==1)))&&(a7==1))){ a4 = 16; a14 = 18; a26 = 17; return -1; } else if((((a1==1)&&(((((a14==19)&&((input==4)&&(((a26==18)&&!(a7==1))||(((a7==1)&&(a26==19))||((a26==17)&&!(a7==1))))))&&(a28==16))&&(a4==16))&&(a25==1)))&&!(a3==1))){ a26 = 18; a14 = 20; a7 = 0; a28 = 17; return -1; } else if(((a28==17)&&(((a3==1)&&((a25==1)&&((a4==18)&&((input==1)&&((((a26==19)&&!(a7==1))&&(a14==19))||(((a26==17)&&(a7==1))&&(a14==20)))))))&&(a1==1)))){ a26 = 17; a4 = 16; a7 = 1; a14 = 18; a28 = 15; return -1; } else if(((!(a7==1)&&(((!(a3==1)&&(((((a26==18)||(a26==19))&&(input==2))&&(a1==1))&&(a14==18)))&&(a25==1))&&(a4==16)))&&(a28==16))){ a26 = 17; a7 = 1; a3 = 1; a28 = 15; return -1; } else if((((a1==1)&&(((a14==20)&&(((a28==17)&&(((((a7==1)&&(a26==19))||((a26==17)&&!(a7==1)))||((a26==18)&&!(a7==1)))&&(input==3)))&&(a4==17)))&&(a3==1)))&&(a25==1))){ a26 = 17; a14 = 18; a4 = 18; a7 = 1; return 22; } else if((((a25==1)&&((a28==16)&&(((a1==1)&&((((((a26==18)&&!(a7==1))&&(a14==19))||(((a26==19)&&!(a7==1))&&(a14==19)))||((a14==20)&&((a7==1)&&(a26==17))))&&(input==5)))&&(a3==1))))&&(a4==17))){ a4 = 16; a7 = 1; a28 = 15; a14 = 18; a26 = 17; return -1; } else if(((a1==1)&&((a4==16)&&((((((((a26==17)||(a26==18))&&(input==3))&&(a28==16))&&(a7==1))&&(a25==1))&&!(a3==1))&&(a14==19))))){ a3 = 1; a28 = 15; a14 = 18; a26 = 17; return -1; } else if(((a4==16)&&((a25==1)&&((a28==17)&&((((a14==19)&&(((input==1)&&((a26==18)||(a26==19)))&&(a7==1)))&&!(a3==1))&&(a1==1)))))){ a3 = 1; a28 = 15; a14 = 18; a26 = 17; return -1; } else if(((a25==1)&&(((((a3==1)&&((((((a26==19)&&!(a7==1))&&(a14==19))||((a14==20)&&((a7==1)&&(a26==17))))||(((a7==1)&&(a26==18))&&(a14==20)))&&(input==3)))&&(a28==15))&&(a1==1))&&(a4==18)))){ a14 = 18; a7 = 1; a26 = 17; a4 = 16; return -1; } else if(((a28==16)&&((a3==1)&&((a14==19)&&((((a4==18)&&(!(a7==1)&&((input==5)&&((a26==18)||(a26==19)))))&&(a25==1))&&(a1==1)))))){ a26 = 17; a14 = 18; a7 = 1; a4 = 16; a28 = 15; return -1; } else if(((!(a3==1)&&((((((((a7==1)&&(a26==19))||(!(a7==1)&&(a26==17)))&&(input==2))&&(a4==17))&&(a25==1))&&(a28==15))&&(a14==19)))&&(a1==1))){ a26 = 17; a7 = 1; a3 = 1; a4 = 16; a14 = 18; return -1; } else if(((((a28==17)&&(((((input==2)&&((((a26==18)&&(a7==1))||((a26==19)&&(a7==1)))||(!(a7==1)&&(a26==17))))&&(a14==18))&&(a25==1))&&(a4==18)))&&(a3==1))&&(a1==1))){ a28 = 15; a26 = 17; a4 = 16; a7 = 1; return -1; } else if((((((a3==1)&&(((a25==1)&&(((input==4)&&(a7==1))&&(a14==20)))&&(a1==1)))&&(a4==17))&&(a28==17))&&(a26==18))){ a14 = 18; a4 = 16; a28 = 15; a26 = 17; return -1; } else if(((a1==1)&&((a4==18)&&(((!(a7==1)&&((a14==19)&&(((input==5)&&((a26==17)||(a26==18)))&&(a25==1))))&&(a28==15))&&(a3==1))))){ a7 = 1; a14 = 18; a26 = 17; a4 = 16; return -1; } else if(((a25==1)&&((a4==18)&&((a1==1)&&((a28==16)&&((((input==2)&&((!(a7==1)&&(a26==18))||(((a7==1)&&(a26==19))||((a26==17)&&!(a7==1)))))&&(a14==18))&&!(a3==1))))))){ a26 = 17; a4 = 16; a28 = 15; a7 = 1; a3 = 1; return -1; } else if((((a4==18)&&(((a28==16)&&((a3==1)&&((a14==18)&&(((!(a7==1)&&(a26==17))||(((a26==18)&&(a7==1))||((a7==1)&&(a26==19))))&&(input==2)))))&&(a1==1)))&&(a25==1))){ a26 = 17; a28 = 15; a4 = 16; a7 = 1; return -1; } else if(((!(a7==1)&&((a28==16)&&((a25==1)&&((a1==1)&&(!(a3==1)&&(((input==5)&&(a14==19))&&(a26==18)))))))&&(a4==18))){ a26 = 19; a7 = 1; a14 = 20; return 23; } else if(((((((a28==15)&&(((a1==1)&&((input==2)&&((a26==17)||(a26==18))))&&!(a3==1)))&&(a25==1))&&(a14==19))&&(a7==1))&&(a4==16))){ a3 = 1; a14 = 18; a26 = 17; return -1; } else if(((((((!(a7==1)&&((a14==20)&&(((a26==17)||(a26==18))&&(input==6))))&&(a25==1))&&(a4==16))&&(a1==1))&&!(a3==1))&&(a28==15))){ a26 = 17; return -1; } else if(((a14==19)&&((a26==19)&&((a28==15)&&(((a4==16)&&(!(a3==1)&&(((a25==1)&&(input==2))&&!(a7==1))))&&(a1==1)))))){ a14 = 18; a26 = 17; a7 = 1; a3 = 1; return -1; } else if((((((a25==1)&&((a4==18)&&((((((a7==1)&&(a26==18))||((a26==19)&&(a7==1)))||((a26==17)&&!(a7==1)))&&(input==4))&&(a14==18))))&&(a28==17))&&(a3==1))&&(a1==1))){ a28 = 15; a7 = 1; a26 = 17; a4 = 16; return -1; } else if((((a28==16)&&((((a14==19)&&((((((a7==1)&&(a26==18))||((a7==1)&&(a26==19)))||(!(a7==1)&&(a26==17)))&&(input==1))&&(a3==1)))&&(a25==1))&&(a1==1)))&&(a4==17))){ a26 = 17; a4 = 18; a28 = 15; a7 = 1; a14 = 20; return 22; } else if(((a25==1)&&((((((a28==15)&&(((input==6)&&(a14==19))&&(a26==18)))&&!(a7==1))&&(a4==17))&&(a1==1))&&!(a3==1)))){ a4 = 16; a26 = 17; a7 = 1; a3 = 1; a14 = 18; return -1; } else if(((a3==1)&&(((((input==4)&&(((a14==18)&&((a7==1)&&((a26==17)&&(a28==16))))||(((a14==20)&&(((a26==18)&&(a28==15))&&!(a7==1)))||((!(a7==1)&&((a26==19)&&(a28==15)))&&(a14==20)))))&&(a1==1))&&(a25==1))&&(a4==18)))){ a28 = 15; a7 = 1; a4 = 16; a3 = 0; a26 = 17; a14 = 19; return 22; } else if(((a14==20)&&((a25==1)&&(((a7==1)&&((((a4==16)&&((input==5)&&((a26==17)||(a26==18))))&&(a1==1))&&!(a3==1)))&&(a28==15))))){ a3 = 1; a14 = 18; a26 = 17; return -1; } else if((!(a3==1)&&(((a25==1)&&((a28==17)&&(((input==5)&&(((a14==20)&&((a26==18)&&(a7==1)))||(((!(a7==1)&&(a26==19))&&(a14==19))||((a14==20)&&((a26==17)&&(a7==1))))))&&(a4==16))))&&(a1==1)))){ a26 = 17; a7 = 1; a28 = 15; a14 = 18; a3 = 1; return -1; } else if(((a14==18)&&((a28==16)&&(((((!(a7==1)&&((input==6)&&((a26==18)||(a26==19))))&&(a4==16))&&!(a3==1))&&(a1==1))&&(a25==1))))){ a26 = 18; a28 = 15; a14 = 20; return 26; } else if(((a4==18)&&((a26==17)&&((a25==1)&&((a1==1)&&((((a7==1)&&((a28==16)&&(input==6)))&&(a14==20))&&(a3==1))))))){ a4 = 17; a28 = 17; return -1; } else if((((a25==1)&&((a28==16)&&(!(a3==1)&&((a4==16)&&(((input==1)&&(((a7==1)&&(a26==19))||((a26==17)&&!(a7==1))))&&(a1==1))))))&&(a14==20))){ a7 = 1; a28 = 15; a4 = 17; a14 = 19; a26 = 19; return 24; } else if(((a1==1)&&((a3==1)&&(((a14==20)&&((a28==16)&&(((input==3)&&((((a7==1)&&(a26==18))||((a26==19)&&(a7==1)))||((a26==17)&&!(a7==1))))&&(a25==1))))&&(a4==18))))){ a26 = 17; a14 = 18; a4 = 16; a7 = 1; a28 = 15; return -1; } else if(((((a4==18)&&((((input==6)&&(((a14==18)&&(!(a7==1)&&(a26==19)))||((a14==19)&&((a26==17)&&(a7==1)))))&&(a1==1))&&!(a3==1)))&&(a25==1))&&(a28==16))){ a28 = 15; a14 = 18; a7 = 1; a4 = 16; a26 = 17; a3 = 1; return -1; } else if(((a7==1)&&((a25==1)&&((((a1==1)&&(((a28==17)&&((input==2)&&((a26==17)||(a26==18))))&&(a14==18)))&&(a4==18))&&!(a3==1))))){ a4 = 16; a3 = 1; a26 = 19; a28 = 16; a14 = 20; return -1; } else if(((((((a28==16)&&((a25==1)&&((input==6)&&(((a26==17)&&!(a7==1))||(((a26==18)&&(a7==1))||((a7==1)&&(a26==19)))))))&&(a1==1))&&(a3==1))&&(a14==19))&&(a4==18))){ a26 = 17; a14 = 18; a4 = 16; a7 = 1; a28 = 15; return -1; } else if((((a14==19)&&((a25==1)&&((!(a7==1)&&((a28==16)&&((a4==17)&&((input==3)&&!(a3==1)))))&&(a26==19))))&&(a1==1))){ a28 = 15; a14 = 18; a7 = 1; a26 = 17; a3 = 1; a4 = 16; return -1; } else if(((((a1==1)&&((((a3==1)&&((a14==19)&&((input==2)&&(a4==18))))&&(a7==1))&&(a28==15)))&&(a26==18))&&(a25==1))){ a26 = 17; a4 = 16; a14 = 18; return -1; } else if(((a4==16)&&((!(a3==1)&&((a14==19)&&((a1==1)&&(((((a26==17)||(a26==18))&&(input==4))&&(a28==15))&&!(a7==1)))))&&(a25==1)))){ a28 = 17; a26 = 17; a14 = 18; return 24; } else if(((((((a14==18)&&((((input==1)&&(a3==1))&&(a28==17))&&(a4==18)))&&!(a7==1))&&(a26==18))&&(a1==1))&&(a25==1))){ a26 = 17; a28 = 15; a7 = 1; a4 = 16; return -1; } else if(((a7==1)&&((a26==19)&&((a1==1)&&((a14==19)&&((a25==1)&&((a28==15)&&((a4==16)&&(!(a3==1)&&(input==5)))))))))){ a3 = 1; a14 = 18; a26 = 17; return -1; } else if((!(a7==1)&&(((a1==1)&&(((!(a3==1)&&((a14==18)&&((input==6)&&((a26==19)||((a26==17)||(a26==18))))))&&(a4==16))&&(a25==1)))&&(a28==15)))){ a3 = 1; a26 = 17; a7 = 1; return -1; } else if(((a4==16)&&((!(a3==1)&&((a14==20)&&((((((a26==17)||(a26==18))&&(input==4))&&(a28==15))&&(a25==1))&&(a1==1))))&&!(a7==1)))){ a7 = 1; a14 = 19; a3 = 1; a26 = 19; a28 = 17; a4 = 18; return 22; } else if((((a4==16)&&((((a14==19)&&((a7==1)&&(((input==1)&&((a26==17)||(a26==18)))&&!(a3==1))))&&(a25==1))&&(a1==1)))&&(a28==15))){ a3 = 1; a26 = 17; a14 = 18; return -1; } else if((((((a26==19)&&((a4==18)&&((!(a7==1)&&((a28==16)&&(input==2)))&&(a1==1))))&&(a14==18))&&(a25==1))&&(a3==1))){ a3 = 0; a14 = 19; a28 = 15; a4 = 16; return 26; } else if(((((a1==1)&&((a28==17)&&((a14==20)&&((a3==1)&&(((((a26==19)&&(a7==1))||(!(a7==1)&&(a26==17)))||((a26==18)&&!(a7==1)))&&(input==5))))))&&(a4==17))&&(a25==1))){ a28 = 15; a4 = 16; a14 = 18; a26 = 17; a7 = 1; return -1; } else if((((a25==1)&&((a4==18)&&((((a7==1)&&(((input==6)&&(a3==1))&&(a1==1)))&&(a14==19))&&(a26==17))))&&(a28==16))){ a28 = 15; a4 = 16; a14 = 18; return -1; } else if(((((a1==1)&&(((((((a26==18)||(a26==19))&&(input==4))&&(a25==1))&&!(a3==1))&&(a14==18))&&(a28==16)))&&!(a7==1))&&(a4==16))){ a28 = 15; a26 = 17; a7 = 1; a3 = 1; return -1; } else if(((a1==1)&&(((a14==19)&&((((a7==1)&&(((input==6)&&((a26==18)||(a26==19)))&&(a28==17)))&&!(a3==1))&&(a25==1)))&&(a4==16)))){ a14 = 18; a3 = 1; a28 = 15; a26 = 17; return -1; } else if(((((a25==1)&&((((a7==1)&&(((input==2)&&(a14==20))&&(a4==17)))&&(a28==15))&&(a26==18)))&&(a1==1))&&(a3==1))){ a14 = 18; a28 = 17; return 24; } else if(((((a1==1)&&((a14==20)&&((!(a7==1)&&(((a28==15)&&(input==5))&&(a26==17)))&&(a25==1))))&&(a3==1))&&(a4==17))){ a26 = 18; a28 = 17; return 22; } else if(((a1==1)&&((a4==17)&&((a25==1)&&((a28==16)&&(!(a7==1)&&((!(a3==1)&&(((a26==18)||(a26==19))&&(input==5)))&&(a14==20)))))))){ a26 = 19; return 24; } else if((((a14==19)&&((a3==1)&&((a1==1)&&(((a25==1)&&(((!(a7==1)&&(a26==17))||(((a26==18)&&(a7==1))||((a26==19)&&(a7==1))))&&(input==1)))&&(a4==18)))))&&(a28==17))){ a28 = 15; a26 = 17; a14 = 18; a7 = 1; a4 = 16; return -1; } else if(((a28==16)&&(((a1==1)&&((a4==17)&&((a3==1)&&((a25==1)&&((input==6)&&(((a26==17)&&!(a7==1))||(((a7==1)&&(a26==18))||((a26==19)&&(a7==1)))))))))&&(a14==20)))){ a28 = 15; a4 = 16; a7 = 1; a26 = 17; a14 = 18; return -1; } else if((((a25==1)&&((((a1==1)&&((((input==6)&&((a26==18)||(a26==19)))&&(a4==18))&&(a14==20)))&&!(a7==1))&&(a28==15)))&&!(a3==1))){ a14 = 18; a7 = 1; a26 = 19; a28 = 16; return 22; } else if(((a28==16)&&(((((a4==16)&&((a7==1)&&(((input==6)&&(a14==18))&&!(a3==1))))&&(a25==1))&&(a1==1))&&(a26==18)))){ a26 = 17; a3 = 1; a28 = 15; return -1; } else if((((a28==15)&&((a1==1)&&((a4==16)&&(!(a3==1)&&(((((a26==17)||(a26==18))&&(input==1))&&(a25==1))&&(a14==20))))))&&(a7==1))){ a28 = 17; a26 = 19; a14 = 18; a7 = 0; return 21; } else if(((a1==1)&&((a28==15)&&(((a4==17)&&(((a26==19)&&(((a14==19)&&(input==4))&&(a25==1)))&&!(a3==1)))&&!(a7==1))))){ a3 = 1; a14 = 18; a4 = 16; a26 = 17; a7 = 1; return -1; } else if(((a14==19)&&(((a7==1)&&((((((a4==18)&&(input==4))&&(a26==18))&&(a28==15))&&(a25==1))&&(a1==1)))&&(a3==1)))){ a4 = 16; a14 = 18; a26 = 17; return -1; } else if(((((a1==1)&&((a28==16)&&((a7==1)&&((a4==18)&&(!(a3==1)&&(((a26==17)||(a26==18))&&(input==6)))))))&&(a25==1))&&(a14==18))){ a26 = 17; a28 = 15; a3 = 1; a4 = 16; return -1; } else if((((a4==16)&&(((a1==1)&&((a26==18)&&((!(a3==1)&&((a25==1)&&(input==3)))&&(a14==18))))&&(a7==1)))&&(a28==16))){ a26 = 17; a28 = 15; a3 = 1; return -1; } else if(((a28==17)&&((a14==19)&&((a26==18)&&(!(a7==1)&&((a25==1)&&((((input==3)&&(a3==1))&&(a4==18))&&(a1==1)))))))){ a7 = 1; return 26; } else if(((((a1==1)&&(((((input==3)&&(((a26==17)&&!(a7==1))||(((a26==18)&&(a7==1))||((a7==1)&&(a26==19)))))&&(a28==17))&&(a4==18))&&(a3==1)))&&(a25==1))&&(a14==20))){ a7 = 1; a26 = 17; a4 = 16; a28 = 15; a14 = 18; return -1; } else if((((a4==18)&&((((input==6)&&((((((a28==16)&&(a26==18))&&!(a7==1))&&(a14==20))||((!(a7==1)&&((a28==16)&&(a26==19)))&&(a14==20)))||(((a7==1)&&((a28==17)&&(a26==17)))&&(a14==18))))&&(a3==1))&&(a1==1)))&&(a25==1))){ a14 = 18; a26 = 17; a7 = 1; a28 = 15; a4 = 16; return -1; } else if(((((a1==1)&&(((a25==1)&&(((((!(a7==1)&&(a26==19))&&(a14==19))||(((a26==17)&&(a7==1))&&(a14==20)))||((a14==20)&&((a7==1)&&(a26==18))))&&(input==6)))&&(a28==17)))&&(a4==16))&&!(a3==1))){ a3 = 1; a28 = 15; a26 = 17; a14 = 18; a7 = 1; return -1; } else if(((((((a1==1)&&((a4==17)&&(!(a7==1)&&((input==6)&&((a26==18)||(a26==19))))))&&(a25==1))&&!(a3==1))&&(a14==20))&&(a28==16))){ a26 = 17; a28 = 15; return -1; } else if(((((a14==20)&&(((a4==18)&&(((input==2)&&((((a26==18)&&(a7==1))||((a26==19)&&(a7==1)))||((a26==17)&&!(a7==1))))&&(a25==1)))&&(a28==16)))&&(a1==1))&&(a3==1))){ a7 = 1; a26 = 17; a4 = 16; a28 = 15; a14 = 18; return -1; } else if(((a14==20)&&((a4==17)&&((a28==16)&&(!(a3==1)&&((a1==1)&&((a25==1)&&((((a26==18)||(a26==19))&&(input==2))&&!(a7==1))))))))){ a26 = 19; return -1; } else if(((a4==16)&&(!(a3==1)&&(((((a28==17)&&(((a1==1)&&(input==6))&&(a26==18)))&&(a14==19))&&!(a7==1))&&(a25==1))))){ a28 = 15; a7 = 1; a14 = 18; a26 = 17; a3 = 1; return -1; } else if(((((((((((a7==1)&&(a26==18))&&(a14==19))||(((a14==18)&&(!(a7==1)&&(a26==19)))||((a14==19)&&((a26==17)&&(a7==1)))))&&(input==2))&&(a4==17))&&(a1==1))&&(a28==17))&&!(a3==1))&&(a25==1))){ a28 = 15; a26 = 17; a7 = 1; a14 = 18; a3 = 1; a4 = 16; return -1; } else if(((a4==16)&&(!(a7==1)&&((a25==1)&&(((a14==19)&&(!(a3==1)&&((a1==1)&&((a26==19)&&(input==3)))))&&(a28==15)))))){ a7 = 1; a26 = 17; a3 = 1; a14 = 18; return -1; } else if(((a7==1)&&(((a28==15)&&((((((input==6)&&(a1==1))&&(a14==19))&&(a4==18))&&(a25==1))&&(a3==1)))&&(a26==17)))){ a4 = 16; a14 = 18; return -1; } else if((((a1==1)&&((((a4==17)&&(!(a7==1)&&(((input==1)&&((a26==17)||(a26==18)))&&!(a3==1))))&&(a25==1))&&(a14==19)))&&(a28==16))){ a26 = 17; a14 = 18; a7 = 1; a3 = 1; a4 = 16; a28 = 15; return -1; } else if((((a1==1)&&(((!(a3==1)&&((a28==17)&&(!(a7==1)&&((a14==19)&&(input==4)))))&&(a25==1))&&(a4==16)))&&(a26==18))){ a26 = 17; a14 = 18; a28 = 15; a7 = 1; a3 = 1; return -1; } else if(((!(a3==1)&&((!(a7==1)&&((a1==1)&&((a25==1)&&(((input==5)&&((a26==18)||(a26==19)))&&(a4==16)))))&&(a28==16)))&&(a14==18))){ a3 = 1; a26 = 17; a28 = 15; a7 = 1; return -1; } else if((((((a28==17)&&((((((a26==18)&&(a7==1))&&(a14==19))||(((!(a7==1)&&(a26==19))&&(a14==18))||((a14==19)&&((a26==17)&&(a7==1)))))&&(input==4))&&(a1==1)))&&(a25==1))&&(a4==17))&&!(a3==1))){ a4 = 16; a14 = 18; a28 = 15; a26 = 17; a3 = 1; a7 = 1; return -1; } else if((((a4==17)&&(((a28==17)&&((((((a14==19)&&((a26==18)&&!(a7==1)))||((!(a7==1)&&(a26==19))&&(a14==19)))||(((a26==17)&&(a7==1))&&(a14==20)))&&(input==1))&&(a3==1)))&&(a1==1)))&&(a25==1))){ a28 = 15; a4 = 16; a7 = 1; a26 = 17; a14 = 18; return -1; } else if(((((a25==1)&&(((((!(a7==1)&&((a28==15)&&(a26==19)))&&(a14==20))||(((a7==1)&&((a28==16)&&(a26==17)))&&(a14==18)))&&(input==1))&&(a4==16)))&&!(a3==1))&&(a1==1))){ a14 = 18; a28 = 15; a7 = 1; a3 = 1; a26 = 17; return -1; } else if((((a25==1)&&((((a3==1)&&((input==2)&&(((((a26==18)&&!(a7==1))&&(a14==19))||((!(a7==1)&&(a26==19))&&(a14==19)))||(((a7==1)&&(a26==17))&&(a14==20)))))&&(a4==17))&&(a1==1)))&&(a28==16))){ a4 = 16; a14 = 18; a7 = 1; a28 = 15; a26 = 17; return -1; } else if((((((a25==1)&&(((a28==15)&&((a1==1)&&((input==3)&&(a4==18))))&&!(a3==1)))&&!(a7==1))&&(a26==17))&&(a14==20))){ a3 = 1; a14 = 18; a4 = 16; a7 = 1; return -1; } else if((((a25==1)&&((((a28==15)&&(((a1==1)&&((a3==1)&&(input==3)))&&(a4==18)))&&(a14==19))&&(a7==1)))&&(a26==19))){ a4 = 16; a14 = 18; a26 = 17; return -1; } else if(((a4==18)&&((a14==18)&&((a1==1)&&((a26==18)&&(!(a3==1)&&(((a25==1)&&((input==4)&&(a28==15)))&&!(a7==1)))))))){ a3 = 1; a7 = 1; a4 = 16; a26 = 17; return -1; } else if(((((a1==1)&&(((((input==1)&&((((a26==19)&&(a7==1))||((a26==17)&&!(a7==1)))||((a26==18)&&!(a7==1))))&&(a28==17))&&!(a3==1))&&(a4==18)))&&(a14==18))&&(a25==1))){ a26 = 18; a7 = 0; return -1; } else if(((((a4==18)&&(!(a3==1)&&((a25==1)&&((((input==1)&&((a26==18)||(a26==19)))&&(a1==1))&&(a14==19)))))&&!(a7==1))&&(a28==15))){ a14 = 20; a26 = 17; return 24; } else if(((a14==19)&&((((a28==17)&&((a1==1)&&((a4==17)&&((input==1)&&((!(a7==1)&&(a26==17))||(((a26==18)&&(a7==1))||((a7==1)&&(a26==19))))))))&&(a25==1))&&(a3==1)))){ a7 = 1; a28 = 16; a4 = 18; a26 = 18; return 26; } else if((((a25==1)&&(((a28==17)&&((((input==4)&&((((a26==18)&&(a7==1))||((a26==19)&&(a7==1)))||((a26==17)&&!(a7==1))))&&(a4==17))&&(a14==19)))&&(a1==1)))&&(a3==1))){ a7 = 1; a26 = 17; a14 = 18; a28 = 15; a4 = 16; return -1; } else if(((a1==1)&&((a28==17)&&((a14==19)&&((a4==17)&&(((((input==6)&&(a25==1))&&!(a3==1))&&(a26==18))&&!(a7==1))))))){ a26 = 17; a7 = 1; a14 = 18; a28 = 15; a4 = 16; a3 = 1; return -1; } else if(((((((((a25==1)&&((input==6)&&(a28==15)))&&(a1==1))&&(a26==18))&&!(a3==1))&&(a4==18))&&(a7==1))&&(a14==19))){ a26 = 17; a14 = 20; a4 = 16; a7 = 0; return 26; } else if(((a26==19)&&((a28==16)&&((a3==1)&&((a1==1)&&((a14==18)&&(((a25==1)&&((input==3)&&(a4==18)))&&!(a7==1)))))))){ a4 = 16; a7 = 1; a26 = 17; a28 = 15; return -1; } else if((((a28==16)&&((a14==18)&&((a4==17)&&((a3==1)&&((((((a26==18)&&(a7==1))||((a26==19)&&(a7==1)))||(!(a7==1)&&(a26==17)))&&(input==3))&&(a25==1))))))&&(a1==1))){ a28 = 15; a14 = 19; a4 = 18; a26 = 17; a7 = 1; return 24; } else if((!(a3==1)&&(((a14==19)&&((a1==1)&&((a28==16)&&(((((a26==17)||(a26==18))&&(input==4))&&(a25==1))&&(a4==16)))))&&(a7==1)))){ a14 = 20; a26 = 19; a28 = 17; return 23; } else if((((a14==20)&&((a1==1)&&((a28==17)&&((!(a3==1)&&((a4==17)&&((input==5)&&(((a26==17)||(a26==18))||(a26==19)))))&&(a7==1)))))&&(a25==1))){ a26 = 17; a14 = 18; a3 = 1; a28 = 15; a4 = 16; return -1; } else if(((a1==1)&&((a14==19)&&(((a25==1)&&((a3==1)&&((a26==18)&&(((input==5)&&(a28==17))&&!(a7==1)))))&&(a4==18))))){ a26 = 17; a4 = 16; a28 = 15; a7 = 1; a14 = 18; return -1; } else if((((a4==17)&&(!(a3==1)&&(((((((a26==18)&&!(a7==1))||(((a26==19)&&(a7==1))||(!(a7==1)&&(a26==17))))&&(input==2))&&(a25==1))&&(a1==1))&&(a14==18))))&&(a28==17))){ a26 = 19; a14 = 20; a7 = 1; a28 = 16; return 24; } else if((((a4==18)&&((a14==20)&&((a25==1)&&((a1==1)&&((a28==16)&&((((a26==19)&&(a7==1))||(!(a7==1)&&(a26==17)))&&(input==5)))))))&&!(a3==1))){ a28 = 17; a7 = 0; a26 = 18; a14 = 19; a4 = 16; a3 = 1; return -1; } else if((!(a3==1)&&((a14==19)&&((a25==1)&&(((a1==1)&&(((((a26==18)&&!(a7==1))||(((a26==19)&&(a7==1))||(!(a7==1)&&(a26==17))))&&(input==1))&&(a4==16)))&&(a28==16)))))){ a28 = 15; a4 = 17; a7 = 1; a26 = 18; a14 = 18; return 23; } else if(((a4==16)&&((a28==15)&&(!(a3==1)&&(((!(a7==1)&&((((a26==19)||((a26==17)||(a26==18)))&&(input==3))&&(a25==1)))&&(a14==18))&&(a1==1)))))){ a7 = 1; a26 = 17; a3 = 1; return -1; } else if((((a1==1)&&((a3==1)&&(((a7==1)&&(((a14==18)&&(((a26==18)||(a26==19))&&(input==4)))&&(a25==1)))&&(a28==15))))&&(a4==18))){ a4 = 16; a26 = 17; return -1; } else if(((a28==16)&&((a4==17)&&((((a1==1)&&((((((a26==18)&&(a7==1))||((a7==1)&&(a26==19)))||((a26==17)&&!(a7==1)))&&(input==4))&&(a25==1)))&&(a14==18))&&(a3==1))))){ a26 = 18; a28 = 15; a7 = 0; a4 = 18; return 24; } else if((!(a3==1)&&((((a1==1)&&((a25==1)&&((input==5)&&((((a7==1)&&(a26==18))&&(a14==20))||((((a26==19)&&!(a7==1))&&(a14==19))||(((a7==1)&&(a26==17))&&(a14==20)))))))&&(a28==16))&&(a4==18)))){ a14 = 19; a4 = 17; a26 = 17; a7 = 0; return -1; } else if(((a7==1)&&(((((a25==1)&&(!(a3==1)&&((a28==16)&&((a4==17)&&(input==5)))))&&(a1==1))&&(a26==17))&&(a14==20)))){ a28 = 15; a14 = 18; a3 = 1; a4 = 16; return -1; } else if((((((((((a14==19)&&(!(a7==1)&&(a26==19)))||(((a7==1)&&(a26==17))&&(a14==20)))&&(input==4))&&(a4==17))&&(a1==1))&&(a28==15))&&(a3==1))&&(a25==1))){ a7 = 0; a26 = 18; a28 = 16; a14 = 18; return 23; } else if((!(a3==1)&&((((a28==17)&&((a14==18)&&((((((a7==1)&&(a26==19))||((a26==17)&&!(a7==1)))||((a26==18)&&!(a7==1)))&&(input==5))&&(a1==1))))&&(a4==18))&&(a25==1)))){ a14 = 20; a7 = 0; a4 = 17; a28 = 16; a26 = 17; return 23; } else if(((a14==19)&&(((a4==17)&&(((a3==1)&&((((a7==1)&&(input==4))&&(a28==15))&&(a25==1)))&&(a26==18)))&&(a1==1)))){ a26 = 17; a14 = 18; a4 = 16; return -1; } else if((((a14==20)&&((((a4==17)&&(((((a26==18)&&!(a7==1))||(((a7==1)&&(a26==19))||((a26==17)&&!(a7==1))))&&(input==2))&&(a25==1)))&&(a3==1))&&(a1==1)))&&(a28==17))){ a7 = 1; a14 = 18; a4 = 16; a26 = 17; a28 = 15; return -1; } else if((((a28==15)&&((a7==1)&&(!(a3==1)&&((a25==1)&&(((a26==19)&&((a14==20)&&(input==6)))&&(a1==1))))))&&(a4==16))){ a3 = 1; a26 = 17; a14 = 18; return -1; } else if((((a26==18)&&(((((a28==17)&&((a4==16)&&((a7==1)&&(input==6))))&&(a1==1))&&(a14==18))&&!(a3==1)))&&(a25==1))){ return -1; } else if((((a7==1)&&(((a28==15)&&((a4==17)&&((a1==1)&&((a14==19)&&((input==3)&&(a26==18))))))&&(a25==1)))&&(a3==1))){ a14 = 18; a26 = 17; a4 = 16; return -1; } else if(((a28==17)&&((a4==18)&&((a25==1)&&(((a3==1)&&((input==3)&&(((!(a7==1)&&(a26==19))&&(a14==18))||(((a26==17)&&(a7==1))&&(a14==19)))))&&(a1==1)))))){ a14 = 18; a7 = 0; a26 = 19; return 26; } else if((((a14==20)&&(((((a4==18)&&((input==1)&&(((a26==17)&&!(a7==1))||(((a26==18)&&(a7==1))||((a26==19)&&(a7==1))))))&&(a3==1))&&(a28==16))&&(a1==1)))&&(a25==1))){ a7 = 1; a26 = 17; return -1; } else if((((((a28==16)&&(((input==3)&&((((a7==1)&&(a26==17))&&(a14==19))||(((a14==18)&&((a26==18)&&!(a7==1)))||((a14==18)&&(!(a7==1)&&(a26==19))))))&&(a1==1)))&&(a25==1))&&(a4==17))&&(a3==1))){ a4 = 16; a28 = 15; a7 = 1; a14 = 18; a26 = 17; return -1; } else if((((a14==19)&&(((((a1==1)&&((((a7==1)&&(a26==19))||(!(a7==1)&&(a26==17)))&&(input==5)))&&(a4==17))&&!(a3==1))&&(a25==1)))&&(a28==17))){ a3 = 1; a14 = 18; a7 = 1; a28 = 15; a4 = 16; a26 = 17; return -1; } else if((!(a7==1)&&((a1==1)&&(((a3==1)&&((a25==1)&&(((((a26==18)||(a26==19))&&(input==2))&&(a28==16))&&(a14==20))))&&(a4==17))))){ a7 = 1; a28 = 15; a26 = 17; a4 = 16; a14 = 18; return -1; } else if(((!(a3==1)&&((((((((a26==19)&&(a7==1))||((a26==17)&&!(a7==1)))&&(input==2))&&(a4==17))&&(a28==17))&&(a25==1))&&(a1==1)))&&(a14==19))){ a28 = 15; a14 = 18; a4 = 16; a3 = 1; a7 = 1; a26 = 17; return -1; } else if((!(a3==1)&&((a28==16)&&(((a1==1)&&((((input==2)&&(((a26==18)&&!(a7==1))||(((a26==19)&&(a7==1))||(!(a7==1)&&(a26==17)))))&&(a14==19))&&(a25==1)))&&(a4==16))))){ a7 = 1; a26 = 17; a3 = 1; a14 = 18; a28 = 15; return -1; } else if(((!(a3==1)&&((a28==16)&&((((a14==19)&&((a1==1)&&((input==1)&&((a26==17)||(a26==18)))))&&(a25==1))&&(a4==16))))&&(a7==1))){ a3 = 1; a28 = 15; a14 = 18; a26 = 17; return -1; } else if((((a1==1)&&(((a25==1)&&(((a7==1)&&(((a4==16)&&(input==2))&&!(a3==1)))&&(a14==18)))&&(a26==19)))&&(a28==15))){ a26 = 18; a28 = 16; a14 = 20; return 24; } else if(((a14==18)&&(!(a3==1)&&((((((a1==1)&&(((a26==17)||(a26==18))&&(input==5)))&&(a25==1))&&(a7==1))&&(a28==15))&&(a4==18))))){ a3 = 1; a26 = 17; a4 = 16; return -1; } else if(((!(a3==1)&&((a28==17)&&(((a1==1)&&((a25==1)&&((!(a7==1)&&(input==4))&&(a14==18))))&&(a4==16))))&&(a26==18))){ a7 = 1; a28 = 15; a3 = 1; a26 = 17; return -1; } else if(((a4==17)&&((((a26==19)&&(((((input==4)&&(a25==1))&&(a28==17))&&(a14==19))&&!(a7==1)))&&(a1==1))&&!(a3==1)))){ a3 = 1; a7 = 1; a28 = 15; a26 = 17; a14 = 18; a4 = 16; return -1; } else if((((a25==1)&&((a7==1)&&((a14==19)&&((((((a26==18)||(a26==19))&&(input==5))&&(a4==16))&&(a28==17))&&!(a3==1)))))&&(a1==1))){ a26 = 18; return 26; } else if((!(a3==1)&&((a25==1)&&((a4==17)&&(((input==5)&&(((a14==18)&&(((a26==17)&&(a28==16))&&(a7==1)))||(((a14==20)&&(((a28==15)&&(a26==18))&&!(a7==1)))||((!(a7==1)&&((a26==19)&&(a28==15)))&&(a14==20)))))&&(a1==1)))))){ a7 = 1; a14 = 20; a28 = 16; a26 = 19; return 22; } else if((((a25==1)&&((((a14==19)&&(((input==3)&&(((a7==1)&&(a26==19))||(!(a7==1)&&(a26==17))))&&(a1==1)))&&(a28==17))&&(a4==17)))&&!(a3==1))){ a14 = 18; a7 = 1; a3 = 1; a26 = 17; a4 = 16; a28 = 15; return -1; } else if(((a4==17)&&(((a25==1)&&(((!(a7==1)&&(((input==5)&&(((a26==17)||(a26==18))||(a26==19)))&&(a14==20)))&&(a1==1))&&!(a3==1)))&&(a28==17)))){ a7 = 1; a14 = 18; a26 = 17; a28 = 15; a4 = 16; a3 = 1; return -1; } else if(((a1==1)&&(((a25==1)&&((a28==17)&&((a3==1)&&((((!(a7==1)&&(a26==18))||(((a26==19)&&(a7==1))||(!(a7==1)&&(a26==17))))&&(input==1))&&(a14==20)))))&&(a4==17)))){ a14 = 18; a7 = 1; a26 = 17; a4 = 16; a28 = 15; return -1; } else if(((a4==18)&&((a25==1)&&((a1==1)&&((a28==15)&&((((((a7==1)&&(a26==19))||(!(a7==1)&&(a26==17)))&&(input==1))&&(a14==18))&&!(a3==1))))))){ a4 = 16; a3 = 1; a7 = 1; a26 = 17; return -1; } else if(((a1==1)&&((a25==1)&&(((((((!(a7==1)&&((a28==15)&&(a26==18)))&&(a14==20))||((((a26==19)&&(a28==15))&&!(a7==1))&&(a14==20)))||((((a26==17)&&(a28==16))&&(a7==1))&&(a14==18)))&&(input==5))&&(a4==17))&&(a3==1))))){ a4 = 18; a7 = 1; a26 = 17; a14 = 18; a28 = 15; return 26; } else if((((a28==15)&&((((a25==1)&&((a4==16)&&(((((a26==17)||(a26==18))||(a26==19))&&(input==2))&&!(a3==1))))&&!(a7==1))&&(a14==18)))&&(a1==1))){ a3 = 1; a26 = 17; a7 = 1; return -1; } else if(((((((a4==17)&&((input==4)&&(((((a26==19)&&!(a7==1))&&(a14==18))||(((a26==17)&&(a7==1))&&(a14==19)))||(((a26==18)&&(a7==1))&&(a14==19)))))&&(a28==15))&&(a1==1))&&!(a3==1))&&(a25==1))){ a7 = 1; a26 = 17; a4 = 16; a14 = 18; a3 = 1; return -1; } else if(((a14==19)&&((a25==1)&&(((!(a7==1)&&((a4==17)&&(((input==2)&&(a28==17))&&!(a3==1))))&&(a26==19))&&(a1==1))))){ a7 = 1; a28 = 15; a4 = 16; a26 = 17; a3 = 1; a14 = 18; return -1; } else if((((a14==20)&&((a1==1)&&(((a25==1)&&((a4==18)&&((input==6)&&(((a7==1)&&(a26==19))||((a26==17)&&!(a7==1))))))&&(a28==16))))&&!(a3==1))){ a26 = 17; a4 = 16; a7 = 1; a28 = 15; a3 = 1; return -1; } else if((!(a7==1)&&((((!(a3==1)&&((a28==15)&&(((a4==16)&&(input==1))&&(a26==19))))&&(a1==1))&&(a14==19))&&(a25==1)))){ a14 = 18; a26 = 18; a28 = 17; return 21; } else if(((!(a3==1)&&((a1==1)&&((a7==1)&&((a25==1)&&((((input==3)&&((a26==19)||((a26==17)||(a26==18))))&&(a14==20))&&(a28==15))))))&&(a4==17))){ a26 = 17; a28 = 16; a7 = 0; a14 = 19; return -1; } else if((!(a3==1)&&((((a14==19)&&((((a25==1)&&(((a26==17)||(a26==18))&&(input==5)))&&(a28==16))&&(a4==17)))&&(a1==1))&&!(a7==1)))){ a28 = 15; a4 = 16; a26 = 17; a7 = 1; a3 = 1; a14 = 18; return -1; } else if((((a25==1)&&((!(a3==1)&&((a7==1)&&((a4==17)&&((a1==1)&&(((a26==17)||(a26==18))&&(input==5))))))&&(a14==18)))&&(a28==17))){ a26 = 17; a28 = 15; a4 = 16; a3 = 1; return -1; } else if(((a1==1)&&((((a25==1)&&(((!(a3==1)&&(((a26==18)||(a26==19))&&(input==3)))&&(a14==18))&&(a28==16)))&&!(a7==1))&&(a4==17)))){ a7 = 1; a28 = 15; a4 = 16; a3 = 1; a26 = 17; return -1; } else if((((a14==20)&&(((!(a7==1)&&((a1==1)&&((a4==17)&&(((a26==18)||(a26==19))&&(input==4)))))&&(a25==1))&&(a3==1)))&&(a28==16))){ a26 = 19; a4 = 18; a28 = 15; return 26; } else if((((((a28==16)&&(((a4==18)&&((input==3)&&((((a26==18)&&(a7==1))||((a7==1)&&(a26==19)))||((a26==17)&&!(a7==1)))))&&(a3==1)))&&(a25==1))&&(a14==18))&&(a1==1))){ a4 = 16; a3 = 0; a26 = 19; a14 = 19; a7 = 1; a28 = 15; return 26; } else if(((a25==1)&&((a4==18)&&((a26==19)&&(((a3==1)&&((a28==16)&&(((input==1)&&(a1==1))&&(a14==18))))&&!(a7==1)))))){ a26 = 17; a28 = 15; a4 = 16; a7 = 1; return -1; } else if((((((a3==1)&&((a1==1)&&((!(a7==1)&&((input==4)&&((a26==17)||(a26==18))))&&(a28==15))))&&(a14==19))&&(a25==1))&&(a4==18))){ a4 = 16; a14 = 18; a7 = 1; a26 = 17; return -1; } else if(((((((((input==6)&&(((a7==1)&&(a26==19))||((a26==17)&&!(a7==1))))&&(a25==1))&&!(a3==1))&&(a14==19))&&(a4==18))&&(a1==1))&&(a28==16))){ a14 = 18; a3 = 1; a4 = 16; a7 = 1; a26 = 17; return -1; } else if((((a28==15)&&((a25==1)&&((a4==17)&&(((input==1)&&(((!(a7==1)&&(a26==19))&&(a14==19))||(((a7==1)&&(a26==17))&&(a14==20))))&&(a1==1)))))&&(a3==1))){ a7 = 1; a26 = 17; a14 = 18; a4 = 16; return -1; } else if((!(a3==1)&&(((!(a7==1)&&((((a1==1)&&((input==5)&&((a26==18)||(a26==19))))&&(a14==19))&&(a28==15)))&&(a4==18))&&(a25==1)))){ a3 = 1; a7 = 1; a26 = 17; a4 = 16; a14 = 18; return -1; } else if(((a28==17)&&(((!(a3==1)&&((a4==18)&&((((((a7==1)&&(a26==19))||((a26==17)&&!(a7==1)))||(!(a7==1)&&(a26==18)))&&(input==4))&&(a25==1))))&&(a1==1))&&(a14==18)))){ a4 = 16; a26 = 18; a7 = 1; return 24; } else if(((a1==1)&&(((a26==17)&&((a28==16)&&((a3==1)&&((a4==18)&&((a7==1)&&((a14==19)&&(input==3)))))))&&(a25==1)))){ a3 = 0; a4 = 16; a14 = 20; a28 = 15; return 24; } else if((((((a25==1)&&((((a1==1)&&((input==6)&&((a26==18)||(a26==19))))&&(a14==18))&&(a4==17)))&&(a7==1))&&(a28==15))&&!(a3==1))){ a26 = 18; return 23; } else if((((a4==18)&&(!(a7==1)&&((a26==18)&&((a25==1)&&(((a14==18)&&((a28==15)&&(input==2)))&&(a1==1))))))&&!(a3==1))){ a7 = 1; a26 = 17; a3 = 1; a4 = 16; return -1; } else if((((a1==1)&&((a25==1)&&(((a28==15)&&(((((a26==19)&&(a7==1))||(!(a7==1)&&(a26==17)))&&(input==2))&&(a4==18)))&&!(a3==1))))&&(a14==19))){ a7 = 1; a4 = 16; a14 = 18; a26 = 17; a3 = 1; return -1; } else if((((((a25==1)&&((!(a3==1)&&((a4==18)&&((input==4)&&((a26==18)||(a26==19)))))&&(a14==20)))&&(a1==1))&&!(a7==1))&&(a28==16))){ a26 = 19; return 23; } else if(((((((a28==16)&&(((input==5)&&((!(a7==1)&&(a26==17))||(((a7==1)&&(a26==18))||((a26==19)&&(a7==1)))))&&(a3==1)))&&(a25==1))&&(a4==18))&&(a14==19))&&(a1==1))){ a7 = 1; a4 = 16; a28 = 15; a14 = 18; a26 = 17; return -1; } else if((!(a7==1)&&(((((a1==1)&&(!(a3==1)&&((a25==1)&&((input==6)&&(a4==17)))))&&(a14==19))&&(a28==15))&&(a26==19)))){ a4 = 16; a26 = 17; a14 = 18; a7 = 1; a3 = 1; return -1; } else if(((a1==1)&&((!(a3==1)&&((((((a14==20)&&((a7==1)&&(a26==18)))||(((a14==19)&&((a26==19)&&!(a7==1)))||(((a7==1)&&(a26==17))&&(a14==20))))&&(input==6))&&(a28==16))&&(a25==1)))&&(a4==16)))){ a3 = 1; a14 = 18; a26 = 17; a28 = 15; a7 = 1; return -1; } else if(((a4==18)&&((a3==1)&&(((a14==18)&&(((a1==1)&&((((a26==17)&&!(a7==1))||(((a26==18)&&(a7==1))||((a26==19)&&(a7==1))))&&(input==6)))&&(a28==17)))&&(a25==1))))){ a4 = 16; a28 = 16; a3 = 0; a26 = 18; a7 = 1; return 23; } else if(((a1==1)&&((a14==18)&&(((((a4==17)&&((input==6)&&(((a26==19)&&(a7==1))||((a26==17)&&!(a7==1)))))&&(a28==17))&&(a3==1))&&(a25==1))))){ a26 = 17; a7 = 1; a4 = 16; a28 = 15; return -1; } else if(((a1==1)&&((a7==1)&&(!(a3==1)&&((a28==15)&&((a25==1)&&(((((a26==17)||(a26==18))&&(input==4))&&(a4==16))&&(a14==20)))))))){ a3 = 1; a26 = 17; a14 = 18; return -1; } else if((((a28==16)&&((a4==17)&&((a25==1)&&((a3==1)&&(((input==1)&&((((a26==18)&&(a7==1))||((a7==1)&&(a26==19)))||(!(a7==1)&&(a26==17))))&&(a14==20))))))&&(a1==1))){ a28 = 15; a14 = 18; a26 = 17; a4 = 16; a7 = 1; return -1; } else if((((((a4==17)&&((a1==1)&&(((((a26==19)&&(a7==1))||((a26==17)&&!(a7==1)))&&(input==4))&&(a14==18))))&&(a3==1))&&(a28==17))&&(a25==1))){ a4 = 16; a28 = 15; a7 = 1; a26 = 17; return -1; } else if(((a28==17)&&(((a25==1)&&((a3==1)&&((a1==1)&&((input==3)&&((((a26==19)&&!(a7==1))&&(a14==19))||(((a26==17)&&(a7==1))&&(a14==20)))))))&&(a4==18)))){ a4 = 16; a26 = 17; a28 = 15; a7 = 1; a14 = 18; return -1; } else if((((((((a28==15)&&(((input==1)&&(((a26==17)||(a26==18))||(a26==19)))&&(a4==18)))&&(a1==1))&&(a25==1))&&(a7==1))&&!(a3==1))&&(a14==20))){ a14 = 18; a26 = 17; a4 = 16; a3 = 1; return -1; } else if(((a3==1)&&((a1==1)&&((a25==1)&&((((a26==17)&&((a14==20)&&((a4==18)&&(input==5))))&&!(a7==1))&&(a28==15)))))){ a4 = 16; a14 = 18; a7 = 1; return -1; } else if((((a3==1)&&((a28==16)&&((a26==18)&&((a1==1)&&(!(a7==1)&&((a25==1)&&((a14==18)&&(input==3))))))))&&(a4==18))){ a3 = 0; a28 = 15; a4 = 16; a14 = 19; return 24; } else if(((a25==1)&&(((a4==16)&&(((input==6)&&(((((a26==17)&&(a28==17))&&(a7==1))&&(a14==18))||(((!(a7==1)&&((a26==18)&&(a28==16)))&&(a14==20))||((((a26==19)&&(a28==16))&&!(a7==1))&&(a14==20)))))&&(a1==1)))&&!(a3==1)))){ a3 = 1; a28 = 15; a26 = 17; a14 = 18; a7 = 1; return -1; } else if(((a25==1)&&(!(a3==1)&&((a1==1)&&((a4==16)&&((input==2)&&((((((a26==18)&&(a28==16))&&!(a7==1))&&(a14==20))||((!(a7==1)&&((a26==19)&&(a28==16)))&&(a14==20)))||((((a26==17)&&(a28==17))&&(a7==1))&&(a14==18))))))))){ a7 = 0; a4 = 17; a14 = 19; a26 = 18; a28 = 15; return 26; } else if(((a4==16)&&(((a25==1)&&((((a1==1)&&(((a26==18)&&(input==5))&&(a28==16)))&&(a7==1))&&(a14==18)))&&!(a3==1)))){ a28 = 17; a7 = 0; a14 = 19; return 24; } else if(((a14==20)&&((((a4==18)&&(((a26==18)&&(((input==6)&&(a28==17))&&(a1==1)))&&!(a7==1)))&&(a25==1))&&(a3==1)))){ a26 = 17; a7 = 1; a14 = 18; a28 = 15; a4 = 16; return -1; } else if(((((a3==1)&&((((a1==1)&&((a28==16)&&((a25==1)&&(input==4))))&&(a4==18))&&(a14==19)))&&(a26==17))&&(a7==1))){ a14 = 18; a28 = 15; a4 = 16; return -1; } else if(((((a4==17)&&((((((input==5)&&(a28==16))&&(a25==1))&&(a26==19))&&!(a7==1))&&(a1==1)))&&!(a3==1))&&(a14==19))){ a4 = 16; a26 = 17; a14 = 18; a7 = 1; a28 = 15; a3 = 1; return -1; } else if(((a1==1)&&((a25==1)&&((!(a3==1)&&((a4==16)&&(((((a14==19)&&(!(a7==1)&&(a26==19)))||((a14==20)&&((a7==1)&&(a26==17))))||(((a26==18)&&(a7==1))&&(a14==20)))&&(input==3))))&&(a28==16))))){ a14 = 18; a26 = 19; a7 = 0; a4 = 17; a28 = 15; return 26; } else if((((((((a26==18)&&(((input==5)&&(a25==1))&&(a3==1)))&&(a7==1))&&(a28==17))&&(a4==17))&&(a1==1))&&(a14==20))){ a28 = 15; a4 = 16; a14 = 18; a26 = 17; return -1; } else if(((a25==1)&&((((a4==18)&&((a28==16)&&((input==4)&&(((!(a7==1)&&(a26==19))&&(a14==18))||(((a26==17)&&(a7==1))&&(a14==19))))))&&(a1==1))&&!(a3==1)))){ a4 = 16; a7 = 1; a28 = 15; a26 = 17; a3 = 1; a14 = 18; return -1; } else if(((((((a14==18)&&((a4==18)&&(((((a26==19)&&(a7==1))||(!(a7==1)&&(a26==17)))||(!(a7==1)&&(a26==18)))&&(input==5))))&&(a1==1))&&(a25==1))&&!(a3==1))&&(a28==16))){ a3 = 1; a4 = 16; a26 = 17; a7 = 1; a28 = 15; return -1; } else if((((a25==1)&&((((((((a26==18)||(a26==19))&&(input==2))&&(a14==18))&&(a1==1))&&(a4==18))&&(a7==1))&&(a3==1)))&&(a28==15))){ a7 = 0; a26 = 19; a28 = 17; return 26; } else if(((((a25==1)&&((a1==1)&&((a4==18)&&((((!(a7==1)&&(a26==19))&&(a14==18))||((a14==19)&&((a7==1)&&(a26==17))))&&(input==5)))))&&(a28==17))&&(a3==1))){ a26 = 17; a7 = 1; a14 = 19; return -1; } else if((((((((a14==19)&&(((((a7==1)&&(a26==19))||(!(a7==1)&&(a26==17)))||((a26==18)&&!(a7==1)))&&(input==2)))&&(a4==17))&&(a25==1))&&(a28==15))&&(a3==1))&&(a1==1))){ a26 = 17; a4 = 16; a14 = 18; a7 = 1; return -1; } else if((((((((a14==18)&&((((a7==1)&&(a26==19))||(!(a7==1)&&(a26==17)))&&(input==5)))&&(a4==16))&&!(a3==1))&&(a25==1))&&(a1==1))&&(a28==16))){ a7 = 1; a28 = 15; a3 = 1; a26 = 17; return -1; } else if((!(a7==1)&&(((a4==17)&&((((a28==15)&&((a1==1)&&((a26==17)&&(input==2))))&&(a3==1))&&(a14==20)))&&(a25==1)))){ a26 = 18; a28 = 17; a7 = 1; return 24; } else if(((((a1==1)&&(!(a3==1)&&((a14==19)&&((a4==16)&&((a26==19)&&((input==6)&&!(a7==1)))))))&&(a25==1))&&(a28==15))){ a7 = 1; a3 = 1; a26 = 17; a14 = 18; return -1; } else if(((a14==19)&&(((a4==17)&&(((a25==1)&&((a1==1)&&(((input==5)&&(((a26==17)||(a26==18))||(a26==19)))&&(a7==1))))&&(a28==16)))&&!(a3==1)))){ a4 = 16; a3 = 1; a26 = 17; a14 = 18; a28 = 15; return -1; } else if((((((a25==1)&&(((a4==18)&&(((((a26==17)||(a26==18))||(a26==19))&&(input==6))&&(a28==15)))&&(a1==1)))&&(a7==1))&&!(a3==1))&&(a14==20))){ a26 = 17; a4 = 16; a3 = 1; a14 = 18; return -1; } else if(((a4==16)&&((!(a3==1)&&((((((input==3)&&((a26==17)||(a26==18)))&&(a25==1))&&(a14==20))&&(a1==1))&&(a7==1)))&&(a28==15)))){ a26 = 17; a14 = 18; a3 = 1; return -1; } else if(((!(a3==1)&&((((((((a26==17)||(a26==18))&&(input==1))&&(a1==1))&&(a14==18))&&(a4==18))&&(a25==1))&&(a28==15)))&&(a7==1))){ a14 = 19; a26 = 17; return 24; } else if(((a14==20)&&(((((a26==17)&&((a1==1)&&((a7==1)&&((input==2)&&!(a3==1)))))&&(a28==16))&&(a25==1))&&(a4==17)))){ a3 = 1; a14 = 18; a4 = 16; a28 = 15; return -1; } else if((((a4==17)&&(((a3==1)&&(((input==2)&&(((((a26==18)&&!(a7==1))&&(a14==18))||((a14==18)&&((a26==19)&&!(a7==1))))||((a14==19)&&((a26==17)&&(a7==1)))))&&(a28==16)))&&(a25==1)))&&(a1==1))){ a26 = 17; a4 = 16; a28 = 15; a7 = 1; a14 = 18; return -1; } else if(((a28==17)&&((a25==1)&&((a3==1)&&((a14==19)&&((a1==1)&&((a4==18)&&(((((a26==18)&&(a7==1))||((a26==19)&&(a7==1)))||((a26==17)&&!(a7==1)))&&(input==3))))))))){ a28 = 15; a14 = 18; a26 = 17; a7 = 0; return -1; } else if(((a1==1)&&((a4==16)&&(((((!(a7==1)&&((input==5)&&((a26==17)||(a26==18))))&&(a14==20))&&(a28==15))&&!(a3==1))&&(a25==1))))){ a14 = 18; a3 = 1; a7 = 1; a26 = 17; return -1; } else if((((a4==18)&&(((a28==15)&&((a1==1)&&((a7==1)&&((a3==1)&&((a25==1)&&(input==5))))))&&(a26==18)))&&(a14==19))){ a26 = 19; a7 = 0; a28 = 17; return 24; } else if(((((a25==1)&&(((a28==15)&&(((a26==18)&&((input==4)&&!(a3==1)))&&(a1==1)))&&(a4==18)))&&(a14==19))&&(a7==1))){ a14 = 18; a3 = 1; a4 = 16; a26 = 17; return -1; } else if(((a3==1)&&((a1==1)&&(((a4==18)&&((a28==17)&&((((a14==19)&&(!(a7==1)&&(a26==19)))||(((a26==17)&&(a7==1))&&(a14==20)))&&(input==5))))&&(a25==1))))){ a7 = 1; a26 = 17; a14 = 19; return 26; } else if(((((a4==16)&&((a26==19)&&(((a14==20)&&(!(a3==1)&&((a7==1)&&(input==5))))&&(a25==1))))&&(a1==1))&&(a28==15))){ a14 = 18; a3 = 1; a26 = 17; return -1; } else if(((a25==1)&&((a1==1)&&(((a4==17)&&((a3==1)&&((input==2)&&((((a26==19)&&!(a7==1))&&(a14==19))||(((a7==1)&&(a26==17))&&(a14==20))))))&&(a28==15))))){ a14 = 18; a4 = 16; a26 = 17; a7 = 1; return -1; } else if((((a4==18)&&((a28==16)&&((a25==1)&&(((input==5)&&(((a14==18)&&(!(a7==1)&&(a26==19)))||((a14==19)&&((a7==1)&&(a26==17)))))&&!(a3==1)))))&&(a1==1))){ a7 = 1; a14 = 19; a26 = 19; return 22; } else if(((a25==1)&&((a28==15)&&(((a14==18)&&((a4==17)&&((((input==5)&&((a26==17)||(a26==18)))&&(a1==1))&&!(a3==1))))&&!(a7==1))))){ a26 = 17; a14 = 19; a28 = 16; return -1; } else if(((((a4==18)&&(((a28==17)&&(((((!(a7==1)&&(a26==19))&&(a14==18))||(((a26==17)&&(a7==1))&&(a14==19)))||((a14==19)&&((a26==18)&&(a7==1))))&&(input==1)))&&(a1==1)))&&!(a3==1))&&(a25==1))){ a26 = 17; a14 = 18; a7 = 0; return 26; } else if(((a25==1)&&((a1==1)&&((((((((a14==18)&&((a26==19)&&!(a7==1)))||((a14==19)&&((a26==17)&&(a7==1))))||(((a7==1)&&(a26==18))&&(a14==19)))&&(input==6))&&(a4==17))&&(a28==17))&&!(a3==1))))){ a14 = 20; a7 = 1; a26 = 19; return 22; } else if(((((a28==17)&&((a1==1)&&((a4==17)&&((input==1)&&(((a14==19)&&((a26==18)&&(a7==1)))||(((a14==18)&&(!(a7==1)&&(a26==19)))||((a14==19)&&((a7==1)&&(a26==17)))))))))&&(a25==1))&&!(a3==1))){ a26 = 17; a3 = 1; a4 = 16; a14 = 18; a7 = 1; a28 = 15; return -1; } else if(((a28==15)&&((a25==1)&&((a3==1)&&(!(a7==1)&&(((((a1==1)&&(input==4))&&(a14==20))&&(a26==17))&&(a4==17))))))){ a28 = 17; a7 = 1; a26 = 19; a14 = 19; return 22; } else if((((a25==1)&&((((a28==15)&&((a1==1)&&(!(a3==1)&&((input==1)&&((a26==17)||(a26==18))))))&&(a4==17))&&!(a7==1)))&&(a14==18))){ a28 = 17; a7 = 1; a4 = 16; a26 = 18; return -1; } else if(((a25==1)&&((a1==1)&&((input==6)&&((((((a28==17)&&((a26==19)&&((a4==18)&&(a3==1))))&&!(a7==1))&&(a14==20))||((((a28==15)&&((!(a3==1)&&(a4==16))&&(a26==17)))&&(a7==1))&&(a14==18)))||((a14==18)&&((a7==1)&&((a28==15)&&((a26==18)&&(!(a3==1)&&(a4==16))))))))))){ a28 = 15; a26 = 17; a7 = 1; a14 = 18; a3 = 1; a4 = 16; return -1; } else if(((a1==1)&&((((((a14==19)&&((a28==15)&&((a7==1)&&(input==6))))&&(a4==16))&&(a26==19))&&!(a3==1))&&(a25==1)))){ a3 = 1; a26 = 17; a14 = 18; return -1; } else if((((a25==1)&&((((((a4==17)&&((((a26==17)||(a26==18))||(a26==19))&&(input==6)))&&(a28==17))&&(a14==20))&&(a1==1))&&(a7==1)))&&!(a3==1))){ a14 = 18; a4 = 16; a3 = 1; a26 = 17; a28 = 15; return -1; } else if(((!(a3==1)&&((((a25==1)&&(((((a26==18)||(a26==19))&&(input==4))&&(a14==18))&&(a7==1)))&&(a4==17))&&(a28==15)))&&(a1==1))){ a26 = 19; return 23; } else if(((a25==1)&&(((((!(a3==1)&&(!(a7==1)&&((input==6)&&((a26==18)||(a26==19)))))&&(a28==15))&&(a4==18))&&(a1==1))&&(a14==19)))){ a14 = 18; a7 = 1; a26 = 17; a3 = 1; a4 = 16; return -1; } else if(((a28==15)&&(!(a3==1)&&((a4==18)&&(((a1==1)&&((((!(a7==1)&&(a26==19))&&(a14==18))||(((a7==1)&&(a26==17))&&(a14==19)))&&(input==3)))&&(a25==1)))))){ a4 = 16; a3 = 1; a14 = 18; a26 = 17; a7 = 1; return -1; } else if(((a4==16)&&((a1==1)&&((a14==20)&&((!(a3==1)&&((a28==16)&&((input==3)&&(((a7==1)&&(a26==19))||((a26==17)&&!(a7==1))))))&&(a25==1)))))){ a28 = 15; a3 = 1; a14 = 18; a26 = 17; a7 = 1; return -1; } return calculate_output2(input); } int calculate_output2(int input) { if((((a28==16)&&((((a25==1)&&(((a1==1)&&((a4==18)&&(input==4)))&&(a14==18)))&&(a26==18))&&!(a7==1)))&&(a3==1))){ a28 = 15; a7 = 1; a4 = 16; a26 = 17; return -1; } else if(((a25==1)&&((a4==17)&&((a28==15)&&((((((((a7==1)&&(a26==19))||((a26==17)&&!(a7==1)))||(!(a7==1)&&(a26==18)))&&(input==1))&&(a3==1))&&(a14==19))&&(a1==1)))))){ a14 = 20; a26 = 17; a7 = 0; return 22; } else if(((a4==16)&&((!(a3==1)&&(((a14==19)&&((((input==3)&&(a28==15))&&(a26==19))&&(a25==1)))&&(a1==1)))&&(a7==1)))){ a26 = 17; a3 = 1; a14 = 18; return -1; } else if(((!(a3==1)&&((((((a26==18)&&((input==1)&&(a4==16)))&&(a1==1))&&(a28==17))&&(a14==18))&&(a7==1)))&&(a25==1))){ return -1; } else if((((!(a7==1)&&((a14==18)&&(((!(a3==1)&&((input==3)&&(a1==1)))&&(a25==1))&&(a28==17))))&&(a4==16))&&(a26==18))){ a7 = 1; return 24; } else if(((a28==16)&&(((((a14==20)&&((((input==4)&&((a26==18)||(a26==19)))&&!(a7==1))&&!(a3==1)))&&(a1==1))&&(a4==17))&&(a25==1)))){ a26 = 18; a28 = 15; a7 = 1; return -1; } else if(((!(a3==1)&&((a25==1)&&((a28==17)&&((a14==18)&&((a4==17)&&(((input==3)&&((a26==17)||(a26==18)))&&(a7==1)))))))&&(a1==1))){ a26 = 17; a4 = 16; a28 = 15; a3 = 1; return -1; } else if((((a3==1)&&(((((((a14==19)&&(!(a7==1)&&(a26==19)))||(((a7==1)&&(a26==17))&&(a14==20)))&&(input==2))&&(a1==1))&&(a25==1))&&(a4==18)))&&(a28==17))){ a14 = 18; a26 = 17; a28 = 15; a4 = 16; a7 = 1; return -1; } else if(((a14==20)&&((((!(a3==1)&&((a4==17)&&(((input==1)&&((a26==19)||((a26==17)||(a26==18))))&&(a28==17))))&&!(a7==1))&&(a25==1))&&(a1==1)))){ a26 = 18; a14 = 18; a28 = 15; a4 = 18; return 22; } else if((((a3==1)&&((((((input==5)&&((((a7==1)&&(a26==18))||((a7==1)&&(a26==19)))||((a26==17)&&!(a7==1))))&&(a25==1))&&(a28==16))&&(a14==20))&&(a1==1)))&&(a4==17))){ a14 = 18; a28 = 15; a26 = 17; a4 = 16; a7 = 1; return -1; } else if((((((((a25==1)&&((((a26==17)||(a26==18))&&(input==6))&&(a1==1)))&&(a4==17))&&!(a3==1))&&(a14==18))&&!(a7==1))&&(a28==15))){ a26 = 18; a4 = 16; a7 = 1; a28 = 17; return -1; } else if(((a4==17)&&(((((a25==1)&&(((((a26==18)&&!(a7==1))||(((a26==19)&&(a7==1))||(!(a7==1)&&(a26==17))))&&(input==3))&&(a1==1)))&&(a3==1))&&(a28==15))&&(a14==19)))){ a4 = 16; a7 = 1; a26 = 17; a14 = 18; return -1; } else if((((a25==1)&&((a26==19)&&((a14==20)&&((a3==1)&&(((a1==1)&&((input==2)&&(a4==18)))&&(a7==1))))))&&(a28==15))){ a14 = 18; a4 = 16; a26 = 17; return -1; } else if(((a26==19)&&((a28==15)&&((a25==1)&&(((a1==1)&&((!(a3==1)&&((a4==16)&&(input==3)))&&(a14==20)))&&(a7==1)))))){ a3 = 1; a26 = 17; a14 = 18; return -1; } else if((((((a1==1)&&((a26==17)&&((a25==1)&&(((input==2)&&(a7==1))&&(a14==19)))))&&(a28==16))&&(a3==1))&&(a4==18))){ a4 = 16; a14 = 18; a28 = 15; return -1; } else if((!(a7==1)&&((a25==1)&&(((a1==1)&&(((((a14==20)&&(input==4))&&!(a3==1))&&(a4==18))&&(a26==17)))&&(a28==15))))){ a14 = 18; a4 = 16; a3 = 1; a7 = 1; return -1; } else if(((a28==15)&&((a1==1)&&((a4==18)&&(!(a3==1)&&((((((a7==1)&&(a26==19))||(!(a7==1)&&(a26==17)))&&(input==5))&&(a25==1))&&(a14==18))))))){ a7 = 1; a4 = 16; a26 = 17; a3 = 1; return -1; } else if((((a14==19)&&((a4==18)&&((a28==16)&&((a25==1)&&(!(a7==1)&&((a1==1)&&((input==2)&&((a26==18)||(a26==19)))))))))&&(a3==1))){ a28 = 17; a26 = 17; return 26; } else if((((((a28==16)&&((((((a26==17)||(a26==18))&&(input==3))&&(a1==1))&&(a4==17))&&!(a7==1)))&&(a14==19))&&!(a3==1))&&(a25==1))){ a26 = 18; return -1; } else if((((((a25==1)&&((a4==17)&&((((((a26==18)&&!(a7==1))&&(a14==19))||((!(a7==1)&&(a26==19))&&(a14==19)))||((a14==20)&&((a7==1)&&(a26==17))))&&(input==2))))&&(a3==1))&&(a28==17))&&(a1==1))){ a14 = 18; a28 = 15; a4 = 16; a26 = 17; a7 = 1; return -1; } else if((((a25==1)&&(((((a4==18)&&(((input==1)&&(a26==19))&&(a28==15)))&&(a7==1))&&(a14==20))&&(a1==1)))&&(a3==1))){ a4 = 16; a26 = 17; a14 = 18; return -1; } else if(((a28==15)&&((a26==19)&&((a4==17)&&((!(a7==1)&&(!(a3==1)&&(((a1==1)&&(input==5))&&(a14==19))))&&(a25==1)))))){ a14 = 18; a7 = 1; a4 = 16; a3 = 1; a26 = 17; return -1; } else if(((a1==1)&&((a25==1)&&(((a3==1)&&(((a4==17)&&(((!(a7==1)&&(a26==17))||(((a26==18)&&(a7==1))||((a26==19)&&(a7==1))))&&(input==3)))&&(a28==16)))&&(a14==20))))){ a28 = 15; a7 = 1; a14 = 18; a4 = 16; a26 = 17; return -1; } else if(((a25==1)&&(((a14==19)&&(((((a3==1)&&((a4==18)&&(input==2)))&&(a26==19))&&(a28==15))&&(a1==1)))&&(a7==1)))){ a28 = 17; a26 = 17; a7 = 0; a14 = 20; return 22; } else if((((a25==1)&&((a4==17)&&((a1==1)&&(((((a7==1)&&((a28==16)&&(a26==17)))&&(a14==18))||(((a14==20)&&(!(a7==1)&&((a28==15)&&(a26==18))))||((a14==20)&&(!(a7==1)&&((a26==19)&&(a28==15))))))&&(input==6)))))&&!(a3==1))){ a7 = 0; a28 = 15; a26 = 17; a14 = 20; return 23; } else if(((a25==1)&&((((!(a3==1)&&((a4==18)&&((a28==15)&&((a26==17)&&(input==1)))))&&(a1==1))&&(a14==20))&&!(a7==1)))){ a28 = 16; a7 = 1; a14 = 18; return 22; } else if((((a28==17)&&(((a4==18)&&((a26==18)&&((a3==1)&&((a1==1)&&((a14==19)&&(input==6))))))&&!(a7==1)))&&(a25==1))){ a7 = 1; a28 = 15; a14 = 18; a26 = 17; a4 = 16; return -1; } else if(((((a3==1)&&((((a26==18)&&(((a25==1)&&(input==5))&&(a28==16)))&&!(a7==1))&&(a1==1)))&&(a4==18))&&(a14==18))){ a7 = 1; a28 = 15; a26 = 17; a4 = 16; return -1; } else if(((a3==1)&&((a4==18)&&(((!(a7==1)&&((a14==19)&&((a1==1)&&((input==3)&&((a26==17)||(a26==18))))))&&(a25==1))&&(a28==15))))){ a4 = 16; a26 = 17; a14 = 18; a7 = 1; return -1; } else if((((a28==15)&&((a25==1)&&((a7==1)&&((((a3==1)&&((input==1)&&(a1==1)))&&(a26==19))&&(a4==18)))))&&(a14==19))){ a4 = 16; a14 = 18; a26 = 17; return -1; } else if(((!(a3==1)&&((((((a4==16)&&((a25==1)&&(input==5)))&&(a26==19))&&(a7==1))&&(a1==1))&&(a14==18)))&&(a28==15))){ a26 = 17; a3 = 1; return -1; } else if((((((a28==16)&&(((a14==20)&&(((!(a7==1)&&(a26==17))||(((a26==18)&&(a7==1))||((a26==19)&&(a7==1))))&&(input==2)))&&!(a3==1)))&&(a4==17))&&(a25==1))&&(a1==1))){ a7 = 0; a26 = 17; a28 = 15; return -1; } else if(((a3==1)&&((((((a1==1)&&((input==2)&&((((a26==18)&&(a7==1))||((a7==1)&&(a26==19)))||((a26==17)&&!(a7==1)))))&&(a25==1))&&(a28==16))&&(a4==17))&&(a14==18)))){ a4 = 16; a7 = 1; a28 = 15; a26 = 17; return -1; } else if(((a28==17)&&((!(a7==1)&&((a25==1)&&((a1==1)&&((a26==18)&&(((a14==18)&&(input==6))&&(a4==16))))))&&!(a3==1)))){ a3 = 1; a28 = 15; a7 = 1; a26 = 17; return -1; } else if(((a1==1)&&((a25==1)&&((((((a26==18)&&((input==5)&&(a28==17)))&&(a14==19))&&!(a7==1))&&!(a3==1))&&(a4==16))))){ a4 = 17; a14 = 18; a28 = 16; a7 = 1; return 23; } else if(((a1==1)&&((a25==1)&&(((a3==1)&&((a28==15)&&((((a14==19)&&((a26==19)&&!(a7==1)))||((a14==20)&&((a26==17)&&(a7==1))))&&(input==5))))&&(a4==17))))){ a7 = 0; a26 = 17; a14 = 19; a28 = 16; return 24; } else if(((a28==17)&&(((a25==1)&&(((((((a14==18)&&(!(a7==1)&&(a26==19)))||((a14==19)&&((a7==1)&&(a26==17))))||((a14==19)&&((a7==1)&&(a26==18))))&&(input==2))&&(a4==18))&&(a1==1)))&&!(a3==1)))){ a7 = 1; a26 = 19; a14 = 18; return -1; } else if(((a1==1)&&(((a7==1)&&((a28==15)&&((a14==20)&&((((a26==19)&&(input==2))&&(a3==1))&&(a4==17)))))&&(a25==1)))){ a26 = 17; a14 = 18; a4 = 16; return -1; } else if(((!(a3==1)&&((a4==17)&&(!(a7==1)&&(((((input==5)&&(a14==19))&&(a26==19))&&(a25==1))&&(a1==1)))))&&(a28==17))){ a28 = 15; a4 = 16; a7 = 1; a26 = 17; a14 = 18; a3 = 1; return -1; } else if(((((a1==1)&&((((((input==2)&&(a28==17))&&!(a7==1))&&(a26==18))&&(a25==1))&&!(a3==1)))&&(a4==16))&&(a14==19))){ a3 = 1; a7 = 1; a28 = 15; a26 = 17; a14 = 18; return -1; } else if((((a4==18)&&(((a14==18)&&((a1==1)&&(!(a7==1)&&((a25==1)&&((a26==18)&&(input==2))))))&&(a3==1)))&&(a28==16))){ a28 = 15; a7 = 1; a4 = 16; a26 = 17; return -1; } else if(((((a25==1)&&((((a14==20)&&((input==4)&&(((a7==1)&&(a26==19))||((a26==17)&&!(a7==1)))))&&(a28==16))&&!(a3==1)))&&(a1==1))&&(a4==16))){ a14 = 18; a26 = 17; a28 = 15; a7 = 1; a3 = 1; return -1; } else if(((a4==17)&&((!(a3==1)&&((a25==1)&&((a28==16)&&((((((a26==18)&&(a7==1))||((a7==1)&&(a26==19)))||(!(a7==1)&&(a26==17)))&&(input==5))&&(a14==18)))))&&(a1==1)))){ a26 = 17; a28 = 15; a4 = 16; a3 = 1; a7 = 1; return -1; } else if(((a1==1)&&((a14==20)&&((a25==1)&&((!(a3==1)&&((a4==16)&&((((a7==1)&&(a26==19))||(!(a7==1)&&(a26==17)))&&(input==4))))&&(a28==17)))))){ a26 = 18; a4 = 17; a28 = 16; a14 = 19; a7 = 1; return 24; } else if(((((((input==3)&&(((((a26==17)&&(a28==17))&&(a7==1))&&(a14==18))||(((a14==20)&&(!(a7==1)&&((a26==18)&&(a28==16))))||((((a28==16)&&(a26==19))&&!(a7==1))&&(a14==20)))))&&!(a3==1))&&(a4==16))&&(a25==1))&&(a1==1))){ a3 = 1; a7 = 1; a14 = 18; a28 = 15; a26 = 17; return -1; } else if((((((a25==1)&&((a1==1)&&((((((a7==1)&&(a26==18))||((a26==19)&&(a7==1)))||(!(a7==1)&&(a26==17)))&&(input==4))&&(a14==19))))&&(a28==16))&&(a4==18))&&(a3==1))){ a28 = 15; a7 = 1; a4 = 16; a26 = 17; a14 = 18; return -1; } else if((((a28==15)&&((a26==18)&&((((((input==1)&&(a4==17))&&(a1==1))&&(a7==1))&&(a14==19))&&(a25==1))))&&(a3==1))){ a14 = 20; return 26; } else if((!(a3==1)&&((((((((((a26==19)&&!(a7==1))&&(a14==19))||(((a7==1)&&(a26==17))&&(a14==20)))||(((a26==18)&&(a7==1))&&(a14==20)))&&(input==4))&&(a28==16))&&(a25==1))&&(a4==18))&&(a1==1)))){ a26 = 19; a14 = 20; a7 = 0; return 26; } else if(((a25==1)&&((a14==18)&&(((((a4==18)&&(((((a26==18)&&(a7==1))||((a7==1)&&(a26==19)))||(!(a7==1)&&(a26==17)))&&(input==6)))&&(a28==16))&&(a3==1))&&(a1==1))))){ a7 = 1; a4 = 16; a28 = 15; a26 = 17; return -1; } else if(((a25==1)&&((a4==16)&&(!(a3==1)&&(((((a14==20)&&(!(a7==1)&&((a26==19)&&(a28==15))))||((a14==18)&&(((a28==16)&&(a26==17))&&(a7==1))))&&(input==5))&&(a1==1)))))){ a26 = 17; a14 = 18; a28 = 15; a7 = 1; a3 = 1; return -1; } else if(((a28==15)&&((a4==17)&&((!(a3==1)&&((a14==18)&&((a1==1)&&(((input==3)&&((a26==18)||(a26==19)))&&(a7==1)))))&&(a25==1))))){ a4 = 16; a26 = 18; a28 = 17; return -1; } else if(((a14==18)&&((((((a4==16)&&((!(a3==1)&&(input==1))&&(a25==1)))&&(a28==17))&&(a1==1))&&!(a7==1))&&(a26==18)))){ a26 = 17; a7 = 1; a3 = 1; a28 = 15; return -1; } else if((((((((a25==1)&&((a7==1)&&((input==6)&&(((a26==17)||(a26==18))||(a26==19)))))&&(a1==1))&&(a4==17))&&(a28==15))&&!(a3==1))&&(a14==20))){ a26 = 18; a4 = 16; a14 = 19; a28 = 17; return -1; } else if((((a3==1)&&((a28==17)&&((a4==18)&&(((a25==1)&&((input==6)&&((!(a7==1)&&(a26==17))||(((a26==18)&&(a7==1))||((a7==1)&&(a26==19))))))&&(a14==20)))))&&(a1==1))){ a14 = 18; a26 = 18; a28 = 16; a3 = 0; a7 = 0; a4 = 16; return 24; } else if(((a26==18)&&((a14==19)&&(((a4==17)&&((!(a3==1)&&((a1==1)&&((input==2)&&!(a7==1))))&&(a28==17)))&&(a25==1))))){ a3 = 1; a4 = 16; a14 = 18; a26 = 17; a7 = 1; a28 = 15; return -1; } else if((((((a4==17)&&(((((!(a7==1)&&(a26==18))||(((a7==1)&&(a26==19))||(!(a7==1)&&(a26==17))))&&(input==4))&&(a1==1))&&(a25==1)))&&(a3==1))&&(a28==15))&&(a14==19))){ a26 = 17; a28 = 16; a7 = 1; a14 = 18; return 22; } else if(((((((a25==1)&&((a26==18)&&((a7==1)&&((input==1)&&(a14==20)))))&&(a3==1))&&(a1==1))&&(a4==17))&&(a28==15))){ a4 = 16; a26 = 17; a14 = 18; return -1; } else if(((a14==19)&&((a26==19)&&((a7==1)&&((((a3==1)&&(((a25==1)&&(input==6))&&(a4==18)))&&(a1==1))&&(a28==15)))))){ a14 = 18; a26 = 17; a4 = 16; return -1; } else if((((a4==17)&&(((a1==1)&&((((((!(a7==1)&&(a26==18))&&(a14==19))||(((a26==19)&&!(a7==1))&&(a14==19)))||((a14==20)&&((a26==17)&&(a7==1))))&&(input==4))&&(a3==1)))&&(a25==1)))&&(a28==16))){ a28 = 15; a14 = 20; a7 = 1; a4 = 18; a26 = 19; return 26; } else if(((a14==19)&&((a4==18)&&(!(a7==1)&&((a25==1)&&(((((a1==1)&&(input==2))&&(a28==16))&&(a26==18))&&!(a3==1))))))){ a14 = 18; a7 = 1; a4 = 16; a28 = 17; a3 = 1; return -1; } else if(((!(a3==1)&&(((a4==18)&&(((input==1)&&((((a26==19)&&!(a7==1))&&(a14==18))||(((a26==17)&&(a7==1))&&(a14==19))))&&(a28==16)))&&(a25==1)))&&(a1==1))){ a14 = 18; a3 = 1; a28 = 15; a7 = 1; a26 = 17; a4 = 16; return -1; } else if(((a28==15)&&(((a25==1)&&(((((((a26==18)&&(a7==1))&&(a14==20))||((((a26==19)&&!(a7==1))&&(a14==19))||(((a7==1)&&(a26==17))&&(a14==20))))&&(input==6))&&(a4==18))&&(a1==1)))&&(a3==1)))){ a26 = 17; a4 = 16; a14 = 18; a7 = 1; return -1; } else if(((!(a7==1)&&((a4==18)&&((a1==1)&&(((a26==18)&&(((input==1)&&(a14==19))&&(a28==17)))&&(a3==1)))))&&(a25==1))){ a14 = 18; a7 = 1; a4 = 16; a28 = 15; a26 = 17; return -1; } else if((((a4==18)&&(((((a1==1)&&((a25==1)&&((a14==18)&&(input==5))))&&(a3==1))&&!(a7==1))&&(a26==19)))&&(a28==16))){ a7 = 1; a4 = 16; a26 = 17; a28 = 15; return -1; } else if(((a28==16)&&(((a25==1)&&(((a4==18)&&((((a14==20)&&((a7==1)&&(a26==18)))||((((a26==19)&&!(a7==1))&&(a14==19))||(((a7==1)&&(a26==17))&&(a14==20))))&&(input==2)))&&(a1==1)))&&!(a3==1)))){ a28 = 17; a4 = 16; a26 = 19; a7 = 0; a3 = 1; a14 = 18; return -1; } else if(((a4==18)&&(!(a3==1)&&((((a25==1)&&((a28==16)&&((input==6)&&(((a26==18)&&!(a7==1))||(((a7==1)&&(a26==19))||(!(a7==1)&&(a26==17)))))))&&(a1==1))&&(a14==18))))){ a3 = 1; a4 = 16; a26 = 17; a28 = 15; a7 = 1; return -1; } else if((!(a7==1)&&((a28==15)&&((((a25==1)&&(((a14==18)&&((((a26==17)||(a26==18))||(a26==19))&&(input==4)))&&(a1==1)))&&(a3==1))&&(a4==18))))){ a7 = 1; a26 = 17; a4 = 16; return -1; } else if(((a3==1)&&((a25==1)&&((a26==18)&&((a4==18)&&(((a7==1)&&(((a28==15)&&(input==3))&&(a14==19)))&&(a1==1))))))){ a14 = 18; a4 = 16; a26 = 17; return -1; } else if(((a1==1)&&(((((a28==16)&&((input==1)&&(((a14==20)&&((a26==17)&&(a7==1)))||(((!(a7==1)&&(a26==18))&&(a14==19))||(((a26==19)&&!(a7==1))&&(a14==19))))))&&(a4==17))&&(a25==1))&&(a3==1)))){ a14 = 18; a28 = 15; a26 = 17; a7 = 1; a4 = 16; return -1; } else if(((((a28==15)&&((a1==1)&&((a4==17)&&(((((a7==1)&&(a26==19))||((a26==17)&&!(a7==1)))&&(input==1))&&(a14==19)))))&&!(a3==1))&&(a25==1))){ a7 = 1; a26 = 17; a3 = 1; a4 = 16; a14 = 18; return -1; } else if((((a14==19)&&(((((a1==1)&&((input==3)&&(((a26==17)&&!(a7==1))||(((a26==18)&&(a7==1))||((a26==19)&&(a7==1))))))&&(a3==1))&&(a28==17))&&(a4==17)))&&(a25==1))){ a7 = 1; a28 = 15; a14 = 18; a4 = 16; a26 = 17; return -1; } else if(((a28==17)&&(((a3==1)&&((a25==1)&&((a1==1)&&((input==6)&&(((a14==18)&&((a26==19)&&!(a7==1)))||((a14==19)&&((a26==17)&&(a7==1))))))))&&(a4==18)))){ a26 = 19; a14 = 18; a7 = 0; return -1; } else if((((a25==1)&&((a4==18)&&((a1==1)&&((input==4)&&((((a7==1)&&((a26==17)&&(a28==17)))&&(a14==18))||(((a14==20)&&(!(a7==1)&&((a28==16)&&(a26==18))))||((a14==20)&&(!(a7==1)&&((a26==19)&&(a28==16))))))))))&&(a3==1))){ a7 = 1; a28 = 15; a26 = 17; a4 = 16; a14 = 18; return -1; } else if(((a28==15)&&(((((((a4==16)&&((a14==18)&&(input==3)))&&(a25==1))&&(a7==1))&&!(a3==1))&&(a1==1))&&(a26==19)))){ a26 = 17; a3 = 1; return -1; } else if((((((((a28==15)&&(((input==6)&&(a4==17))&&(a14==20)))&&(a7==1))&&(a26==19))&&(a3==1))&&(a25==1))&&(a1==1))){ a28 = 17; a14 = 18; return 23; } else if(((a14==19)&&(((a1==1)&&(((!(a7==1)&&((a4==18)&&((input==1)&&(a28==16))))&&(a26==18))&&!(a3==1)))&&(a25==1)))){ a7 = 1; a26 = 19; a4 = 17; a3 = 1; a28 = 15; a14 = 18; return -1; } else if(((a28==17)&&((((!(a3==1)&&((input==3)&&((((a14==18)&&(!(a7==1)&&(a26==19)))||((a14==19)&&((a7==1)&&(a26==17))))||((a14==19)&&((a26==18)&&(a7==1))))))&&(a25==1))&&(a4==17))&&(a1==1)))){ a14 = 18; a28 = 15; a7 = 1; a26 = 17; a4 = 16; a3 = 1; return -1; } else if(((a28==16)&&(((a7==1)&&((a25==1)&&((a14==19)&&((a1==1)&&((((a26==17)||(a26==18))&&(input==5))&&(a4==16))))))&&!(a3==1)))){ a28 = 15; a14 = 18; a26 = 17; a3 = 1; return -1; } else if(((a4==16)&&(((((a7==1)&&((a25==1)&&(((input==4)&&(a1==1))&&!(a3==1))))&&(a14==19))&&(a28==15))&&(a26==19)))){ a14 = 18; a26 = 17; a3 = 1; return -1; } else if(((a28==17)&&((a3==1)&&(((a4==17)&&((((((!(a7==1)&&(a26==18))&&(a14==18))||((a14==18)&&(!(a7==1)&&(a26==19))))||(((a7==1)&&(a26==17))&&(a14==19)))&&(input==2))&&(a25==1)))&&(a1==1))))){ a28 = 15; a7 = 1; a26 = 17; a4 = 16; a14 = 18; return -1; } else if((((a3==1)&&(((((((((a26==18)&&(a28==16))&&!(a7==1))&&(a14==20))||((!(a7==1)&&((a28==16)&&(a26==19)))&&(a14==20)))||((a14==18)&&((a7==1)&&((a26==17)&&(a28==17)))))&&(input==3))&&(a25==1))&&(a1==1)))&&(a4==18))){ a26 = 19; a4 = 16; a3 = 0; a28 = 15; a7 = 0; a14 = 20; return 22; } else if(((a1==1)&&((a3==1)&&(((a28==16)&&((a25==1)&&((a14==20)&&((a4==17)&&(((a26==18)||(a26==19))&&(input==5))))))&&!(a7==1))))){ a4 = 16; a26 = 17; a14 = 18; a7 = 1; a28 = 15; return -1; } else if(((a4==18)&&(((a14==18)&&((a28==15)&&(!(a7==1)&&(((a25==1)&&((((a26==17)||(a26==18))||(a26==19))&&(input==2)))&&(a1==1)))))&&(a3==1)))){ a26 = 17; a7 = 1; a4 = 16; return -1; } else if((((a4==17)&&((a28==16)&&(((a3==1)&&(((((a26==17)&&(a7==1))&&(a14==20))||((((a26==18)&&!(a7==1))&&(a14==19))||(((a26==19)&&!(a7==1))&&(a14==19))))&&(input==3)))&&(a1==1))))&&(a25==1))){ a26 = 17; a28 = 15; a4 = 16; a7 = 1; a14 = 18; return -1; } else if(((a14==19)&&((!(a3==1)&&((((a1==1)&&((a7==1)&&((input==4)&&((a26==18)||(a26==19)))))&&(a28==17))&&(a25==1)))&&(a4==16)))){ a14 = 20; a28 = 15; a26 = 18; a4 = 17; return 23; } else if(((((a1==1)&&(((a3==1)&&((a14==19)&&((a4==18)&&((a7==1)&&(input==4)))))&&(a28==15)))&&(a26==19))&&(a25==1))){ a26 = 17; a4 = 16; a14 = 18; return -1; } else if((((a1==1)&&(!(a3==1)&&((((a4==17)&&((((a7==1)&&(a26==19))||(!(a7==1)&&(a26==17)))&&(input==4)))&&(a14==19))&&(a28==15))))&&(a25==1))){ a7 = 1; a26 = 17; a28 = 16; a14 = 20; return 24; } else if((((a28==15)&&(((((a25==1)&&((((a26==18)||(a26==19))&&(input==5))&&(a4==18)))&&(a7==1))&&(a14==18))&&(a3==1)))&&(a1==1))){ a4 = 16; a26 = 17; return -1; } else if(((a25==1)&&(((a28==15)&&(((a7==1)&&(!(a3==1)&&((((a26==18)||(a26==19))&&(input==2))&&(a4==17))))&&(a14==18)))&&(a1==1)))){ a26 = 19; return 23; } else if((((a14==19)&&(((!(a3==1)&&((((input==5)&&((a26==17)||(a26==18)))&&(a7==1))&&(a28==15)))&&(a4==16))&&(a25==1)))&&(a1==1))){ a28 = 17; a14 = 18; a26 = 17; return 22; } else if(((a25==1)&&(((a1==1)&&(!(a3==1)&&(((a4==17)&&((a28==16)&&(((a26==18)||(a26==19))&&(input==2))))&&(a14==18))))&&!(a7==1)))){ a4 = 16; a28 = 15; a3 = 1; a7 = 1; a26 = 17; return -1; } else if(((a14==20)&&((((a3==1)&&(((((input==1)&&(a25==1))&&(a28==16))&&(a1==1))&&(a7==1)))&&(a26==17))&&(a4==18)))){ a14 = 18; a4 = 16; a28 = 15; return -1; } else if(((a25==1)&&(((a14==18)&&(!(a3==1)&&((a4==17)&&((a28==16)&&(((((a7==1)&&(a26==18))||((a7==1)&&(a26==19)))||((a26==17)&&!(a7==1)))&&(input==3))))))&&(a1==1)))){ a4 = 16; a3 = 1; a7 = 1; a28 = 15; a26 = 17; return -1; } else if((((a1==1)&&((((!(a7==1)&&((a25==1)&&((input==4)&&(a14==19))))&&(a4==17))&&!(a3==1))&&(a26==18)))&&(a28==15))){ a4 = 16; a26 = 17; a14 = 18; a7 = 1; a3 = 1; return -1; } else if(((((((a1==1)&&(((((a26==18)||(a26==19))&&(input==5))&&(a14==20))&&!(a3==1)))&&!(a7==1))&&(a28==15))&&(a25==1))&&(a4==18))){ a14 = 18; a4 = 16; a26 = 17; a7 = 1; a3 = 1; return -1; } else if((!(a7==1)&&(((a14==19)&&((a4==17)&&(((!(a3==1)&&((input==4)&&(a25==1)))&&(a28==17))&&(a26==18))))&&(a1==1)))){ a4 = 16; a7 = 1; a3 = 1; a28 = 15; a26 = 17; a14 = 18; return -1; } else if(((a28==17)&&((a25==1)&&((((((input==3)&&((!(a7==1)&&(a26==18))||(((a7==1)&&(a26==19))||((a26==17)&&!(a7==1)))))&&!(a3==1))&&(a1==1))&&(a4==17))&&(a14==18))))){ a7 = 1; a4 = 16; a26 = 17; a3 = 1; a28 = 15; return -1; } else if((((!(a7==1)&&((a28==16)&&((a14==18)&&(((a1==1)&&((input==1)&&((a26==18)||(a26==19))))&&!(a3==1)))))&&(a25==1))&&(a4==16))){ a7 = 1; a26 = 17; a28 = 15; a3 = 1; return -1; } else if(((a25==1)&&((a1==1)&&(((((a7==1)&&((a28==15)&&(((a4==16)&&!(a3==1))&&(a26==18))))&&(a14==18))||(((a14==20)&&(!(a7==1)&&((((a3==1)&&(a4==18))&&(a26==19))&&(a28==17))))||(((a7==1)&&((((a4==16)&&!(a3==1))&&(a26==17))&&(a28==15)))&&(a14==18))))&&(input==3))))){ a28 = 15; a7 = 1; a14 = 18; a3 = 1; a26 = 17; a4 = 16; return -1; } else if(((a25==1)&&((((a28==15)&&((a26==17)&&((a4==18)&&((a14==19)&&((a3==1)&&(input==1))))))&&(a1==1))&&(a7==1)))){ a4 = 16; a14 = 18; return -1; } else if(((a1==1)&&((!(a7==1)&&(((a14==19)&&(((a3==1)&&((input==6)&&((a26==18)||(a26==19))))&&(a4==18)))&&(a28==16)))&&(a25==1)))){ a7 = 1; a26 = 17; a28 = 15; a14 = 18; a4 = 16; return -1; } else if(((((a1==1)&&((input==2)&&(((a14==20)&&(!(a7==1)&&((a28==17)&&((a4==17)&&(a26==19)))))||(((a7==1)&&(((a26==17)&&(a4==18))&&(a28==15)))&&(a14==18)))))&&(a3==1))&&(a25==1))){ a4 = 18; a26 = 18; a14 = 18; a7 = 0; a28 = 17; return 22; } else if(((a4==17)&&(!(a3==1)&&((((((((a26==19)&&(a7==1))||(!(a7==1)&&(a26==17)))&&(input==6))&&(a28==15))&&(a1==1))&&(a25==1))&&(a14==19))))){ a14 = 18; a3 = 1; a26 = 17; a7 = 1; a4 = 16; return -1; } else if(((((a4==16)&&((a25==1)&&((((a7==1)&&((a14==18)&&(input==4)))&&(a26==18))&&(a28==17))))&&(a1==1))&&!(a3==1))){ a3 = 1; a28 = 15; a26 = 17; return -1; } else if(((((a28==17)&&((a1==1)&&(((input==4)&&((((a26==17)&&(a7==1))&&(a14==19))||(((a14==18)&&(!(a7==1)&&(a26==18)))||((a14==18)&&((a26==19)&&!(a7==1))))))&&(a25==1))))&&(a3==1))&&(a4==17))){ a28 = 15; a7 = 1; a26 = 17; a4 = 16; a14 = 18; return -1; } else if((((a25==1)&&((a1==1)&&((a4==17)&&((input==2)&&((((!(a7==1)&&((a28==15)&&(a26==18)))&&(a14==20))||((((a28==15)&&(a26==19))&&!(a7==1))&&(a14==20)))||(((a7==1)&&((a26==17)&&(a28==16)))&&(a14==18)))))))&&!(a3==1))){ a26 = 19; a14 = 20; a28 = 16; a7 = 0; return 24; } else if(((a1==1)&&((((a25==1)&&((((((a7==1)&&(a26==17))&&(a14==19))||(((!(a7==1)&&(a26==18))&&(a14==18))||(((a26==19)&&!(a7==1))&&(a14==18))))&&(input==6))&&(a3==1)))&&(a28==16))&&(a4==17)))){ a26 = 17; a28 = 15; a4 = 16; a14 = 18; a7 = 1; return -1; } else if(((((!(a3==1)&&((a25==1)&&((a14==18)&&((input==3)&&((((a26==19)&&(a7==1))||(!(a7==1)&&(a26==17)))||((a26==18)&&!(a7==1)))))))&&(a28==17))&&(a1==1))&&(a4==18))){ a7 = 0; a26 = 19; return 24; } else if((!(a3==1)&&((((a1==1)&&(((a7==1)&&((a28==16)&&((a14==20)&&(input==6))))&&(a4==17)))&&(a26==17))&&(a25==1)))){ a14 = 19; a7 = 0; a26 = 19; a28 = 17; return 24; } else if(((((a25==1)&&(((((((a26==17)||(a26==18))&&(input==5))&&!(a3==1))&&(a4==18))&&(a14==18))&&(a28==17)))&&(a7==1))&&(a1==1))){ a26 = 18; a3 = 1; a7 = 0; a4 = 16; return -1; } else if(((a28==16)&&(((!(a3==1)&&((a4==18)&&((((input==1)&&((a26==17)||(a26==18)))&&(a25==1))&&(a7==1))))&&(a14==18))&&(a1==1)))){ a28 = 15; a3 = 1; a26 = 17; a4 = 16; return -1; } else if(((((((a3==1)&&((((((a26==19)&&!(a7==1))&&(a14==19))||((a14==20)&&((a26==17)&&(a7==1))))||(((a26==18)&&(a7==1))&&(a14==20)))&&(input==1)))&&(a25==1))&&(a1==1))&&(a28==15))&&(a4==18))){ a7 = 0; a28 = 17; a26 = 19; a14 = 20; return 21; } else if((((a28==16)&&(!(a3==1)&&((a14==19)&&((a4==17)&&(!(a7==1)&&(((a26==19)&&(input==1))&&(a1==1)))))))&&(a25==1))){ a28 = 15; a3 = 1; a4 = 16; a7 = 1; a26 = 17; a14 = 18; return -1; } else if(((a1==1)&&((a3==1)&&((a25==1)&&((a4==18)&&((((a14==18)&&((a7==1)&&((a28==16)&&(a26==17))))||(((a14==20)&&(((a28==15)&&(a26==18))&&!(a7==1)))||((!(a7==1)&&((a28==15)&&(a26==19)))&&(a14==20))))&&(input==2))))))){ a7 = 1; a4 = 16; a14 = 18; a28 = 15; a26 = 17; return -1; } else if((((a3==1)&&(((a4==18)&&(((a1==1)&&((a14==18)&&((input==6)&&!(a7==1))))&&(a28==16)))&&(a26==19)))&&(a25==1))){ a4 = 16; a28 = 15; a7 = 1; a26 = 17; return -1; } else if(((((((a25==1)&&((a26==18)&&(((a4==18)&&(input==4))&&(a28==16))))&&(a1==1))&&!(a7==1))&&(a14==19))&&!(a3==1))){ a4 = 16; a14 = 18; a3 = 1; a7 = 1; return -1; } else if((((a1==1)&&((((((((a14==18)&&((a26==18)&&!(a7==1)))||((!(a7==1)&&(a26==19))&&(a14==18)))||((a14==19)&&((a26==17)&&(a7==1))))&&(input==1))&&(a4==17))&&(a28==17))&&(a25==1)))&&(a3==1))){ a4 = 16; a7 = 1; a28 = 15; a26 = 17; a14 = 18; return -1; } else if(((a4==16)&&((!(a3==1)&&(((((a1==1)&&((input==5)&&(a25==1)))&&!(a7==1))&&(a28==17))&&(a14==19)))&&(a26==17)))){ a14 = 18; a7 = 1; a3 = 1; a28 = 15; return -1; } else if(((a4==16)&&((a25==1)&&(((a1==1)&&(((((input==3)&&((a26==17)||(a26==18)))&&!(a3==1))&&(a28==15))&&!(a7==1)))&&(a14==20))))){ a26 = 17; a3 = 1; a7 = 1; a14 = 18; return -1; } else if((!(a3==1)&&((a1==1)&&((a25==1)&&(((((input==6)&&((((a7==1)&&(a26==19))||((a26==17)&&!(a7==1)))||(!(a7==1)&&(a26==18))))&&(a4==17))&&(a28==17))&&(a14==18)))))){ a7 = 1; a26 = 17; a28 = 15; a3 = 1; a4 = 16; return -1; } else if(((a1==1)&&((a4==16)&&(!(a7==1)&&(((((a26==17)&&((a25==1)&&(input==1)))&&!(a3==1))&&(a14==18))&&(a28==17)))))){ a26 = 18; a7 = 1; return 21; } else if(((((((a28==15)&&(((((a26==17)||(a26==18))&&(input==6))&&!(a3==1))&&!(a7==1)))&&(a1==1))&&(a14==19))&&(a25==1))&&(a4==16))){ a7 = 1; a14 = 18; a3 = 1; a26 = 17; return -1; } else if(((a28==16)&&((a14==19)&&(((a7==1)&&(((((input==1)&&(a26==17))&&(a1==1))&&(a4==18))&&(a3==1)))&&(a25==1))))){ a4 = 16; a28 = 15; a14 = 18; return -1; } else if((((((a4==17)&&((a28==16)&&(((input==2)&&(((a26==17)&&!(a7==1))||(((a26==18)&&(a7==1))||((a26==19)&&(a7==1)))))&&(a25==1))))&&(a1==1))&&(a14==20))&&(a3==1))){ a7 = 0; a26 = 17; a4 = 18; a28 = 15; return 22; } else if(((((a4==18)&&((a25==1)&&((a1==1)&&((((a14==18)&&((a26==19)&&!(a7==1)))||((a14==19)&&((a7==1)&&(a26==17))))&&(input==1)))))&&(a3==1))&&(a28==17))){ a14 = 20; a28 = 16; a7 = 1; a26 = 17; return -1; } else if(((a25==1)&&((((a14==18)&&((!(a3==1)&&((input==6)&&((((a7==1)&&(a26==19))||((a26==17)&&!(a7==1)))||((a26==18)&&!(a7==1)))))&&(a1==1)))&&(a4==18))&&(a28==17)))){ a4 = 16; a26 = 18; a7 = 1; return 24; } else if((((a4==17)&&(((a28==15)&&(((a1==1)&&((((a26==17)||(a26==18))&&(input==4))&&(a14==18)))&&(a25==1)))&&!(a7==1)))&&!(a3==1))){ a26 = 18; return -1; } else if(((a25==1)&&(((a1==1)&&((((((input==3)&&((a26==17)||(a26==18)))&&!(a7==1))&&(a28==15))&&!(a3==1))&&(a4==16)))&&(a14==19)))){ a14 = 18; a26 = 17; a7 = 1; a3 = 1; return -1; } else if((((a4==16)&&((a1==1)&&(((((((!(a7==1)&&(a26==19))&&(a14==19))||(((a7==1)&&(a26==17))&&(a14==20)))||(((a7==1)&&(a26==18))&&(a14==20)))&&(input==4))&&(a28==17))&&!(a3==1))))&&(a25==1))){ a26 = 17; a14 = 18; a3 = 1; a7 = 1; a28 = 15; return -1; } else if(((a28==15)&&((a4==17)&&((a14==20)&&((a1==1)&&(((((((a26==17)||(a26==18))||(a26==19))&&(input==1))&&!(a3==1))&&(a7==1))&&(a25==1))))))){ a4 = 16; a26 = 17; a14 = 18; a3 = 1; return -1; } else if(((!(a7==1)&&(((((a4==18)&&((a1==1)&&((a3==1)&&(input==6))))&&(a14==18))&&(a26==18))&&(a28==16)))&&(a25==1))){ a26 = 17; a4 = 16; a7 = 1; a28 = 15; return -1; } else if((!(a7==1)&&(((!(a3==1)&&((((a14==18)&&((input==6)&&(a4==18)))&&(a25==1))&&(a28==15)))&&(a1==1))&&(a26==18)))){ a7 = 1; a26 = 17; a3 = 1; a4 = 16; return -1; } else if(((((a14==19)&&(((((a1==1)&&((input==3)&&((a26==18)||(a26==19))))&&(a25==1))&&(a4==18))&&(a28==15)))&&!(a3==1))&&!(a7==1))){ a4 = 16; a3 = 1; a26 = 17; a14 = 18; a7 = 1; return -1; } else if(((((((a7==1)&&((a4==17)&&((a25==1)&&(((a26==19)||((a26==17)||(a26==18)))&&(input==2)))))&&!(a3==1))&&(a1==1))&&(a28==17))&&(a14==20))){ a4 = 16; a26 = 17; a14 = 18; a28 = 15; a3 = 1; return -1; } else if(((a4==16)&&((a28==15)&&(((a1==1)&&(((((input==2)&&((a26==17)||(a26==18)))&&!(a7==1))&&(a14==20))&&!(a3==1)))&&(a25==1))))){ a26 = 17; a14 = 18; a7 = 1; a3 = 1; return -1; } else if((((((a1==1)&&((((((a26==19)&&!(a7==1))&&(a14==18))||(((a7==1)&&(a26==17))&&(a14==19)))&&(input==2))&&(a28==17)))&&(a25==1))&&(a4==16))&&!(a3==1))){ a7 = 1; a14 = 18; a28 = 15; a26 = 17; a3 = 1; return -1; } else if((((((a3==1)&&((input==1)&&((((a7==1)&&((a28==17)&&(a26==17)))&&(a14==18))||(((((a28==16)&&(a26==18))&&!(a7==1))&&(a14==20))||((!(a7==1)&&((a28==16)&&(a26==19)))&&(a14==20))))))&&(a25==1))&&(a1==1))&&(a4==18))){ a28 = 15; a4 = 16; a14 = 18; a7 = 1; a26 = 17; return -1; } else if(((a1==1)&&((a26==17)&&(!(a7==1)&&(((((a3==1)&&((a25==1)&&(input==2)))&&(a4==18))&&(a28==15))&&(a14==20)))))){ a14 = 18; a7 = 1; a4 = 16; return -1; } else if(((a26==18)&&(!(a3==1)&&((a14==19)&&(((a25==1)&&((a7==1)&&(((input==6)&&(a28==16))&&(a4==18))))&&(a1==1)))))){ a3 = 1; a26 = 17; a4 = 16; a28 = 15; a14 = 18; return -1; } else if(((((a4==16)&&(((!(a3==1)&&((input==5)&&(((a7==1)&&(a26==19))||(!(a7==1)&&(a26==17)))))&&(a28==16))&&(a1==1)))&&(a25==1))&&(a14==20))){ a28 = 15; a3 = 1; a7 = 1; a14 = 18; a26 = 17; return -1; } else if((((((a25==1)&&(((a1==1)&&((input==5)&&(((a26==17)&&!(a7==1))||(((a7==1)&&(a26==18))||((a26==19)&&(a7==1))))))&&(a4==18)))&&(a3==1))&&(a14==18))&&(a28==16))){ a4 = 16; a26 = 17; a28 = 15; a7 = 1; return -1; } else if((((a4==18)&&((((a25==1)&&((a26==17)&&(((input==3)&&(a28==16))&&(a14==20))))&&(a7==1))&&(a1==1)))&&(a3==1))){ a4 = 16; a28 = 15; a14 = 18; return -1; } else if((((a25==1)&&(((a14==18)&&(!(a3==1)&&(((input==4)&&(((a7==1)&&(a26==19))||((a26==17)&&!(a7==1))))&&(a28==15))))&&(a1==1)))&&(a4==18))){ a26 = 18; a7 = 1; a14 = 19; return 22; } else if((((((a1==1)&&((a4==18)&&((a14==19)&&((a3==1)&&((a26==17)&&(input==4))))))&&(a28==15))&&(a25==1))&&(a7==1))){ a14 = 18; a4 = 16; return -1; } else if(((a25==1)&&((((a28==17)&&(((a1==1)&&((input==5)&&((((a7==1)&&(a26==18))||((a26==19)&&(a7==1)))||((a26==17)&&!(a7==1)))))&&(a4==17)))&&(a14==19))&&(a3==1)))){ a14 = 18; a28 = 15; a26 = 17; a7 = 1; a4 = 16; return -1; } else if(((a1==1)&&((a25==1)&&((a4==16)&&((a28==17)&&((!(a7==1)&&((a14==19)&&(!(a3==1)&&(input==1))))&&(a26==17))))))){ a26 = 19; a28 = 15; a14 = 20; a4 = 17; return 24; } else if(((a25==1)&&((((a1==1)&&((((a14==18)&&(((a28==16)&&(a26==17))&&(a7==1)))||(((((a26==18)&&(a28==15))&&!(a7==1))&&(a14==20))||((!(a7==1)&&((a26==19)&&(a28==15)))&&(a14==20))))&&(input==5)))&&(a3==1))&&(a4==18)))){ a4 = 16; a14 = 18; a28 = 15; a26 = 17; a7 = 1; return -1; } else if(((a26==18)&&((a7==1)&&((((((a28==17)&&((a3==1)&&(input==3)))&&(a25==1))&&(a1==1))&&(a4==17))&&(a14==20))))){ a4 = 18; a28 = 16; return 26; } else if(((a26==17)&&((a1==1)&&(((a28==15)&&((a3==1)&&((a14==20)&&(((input==4)&&(a25==1))&&(a4==18)))))&&!(a7==1))))){ a3 = 0; a14 = 18; a4 = 16; return 26; } else if((!(a3==1)&&((a4==18)&&(((a28==17)&&((a25==1)&&(((((a7==1)&&(a26==18))&&(a14==19))||(((a14==18)&&((a26==19)&&!(a7==1)))||(((a26==17)&&(a7==1))&&(a14==19))))&&(input==5))))&&(a1==1))))){ a3 = 1; a4 = 16; a7 = 1; a14 = 20; a26 = 18; a28 = 15; return -1; } else if(((a26==19)&&(((a25==1)&&(!(a3==1)&&((a28==15)&&((a1==1)&&(((input==1)&&(a7==1))&&(a4==16))))))&&(a14==20)))){ a14 = 19; a28 = 17; a26 = 18; return 24; } else if(((((((((a14==20)&&(((a28==15)&&(a26==19))&&!(a7==1)))||((((a28==16)&&(a26==17))&&(a7==1))&&(a14==18)))&&(input==6))&&(a4==16))&&(a25==1))&&(a1==1))&&!(a3==1))){ a7 = 1; a3 = 1; a26 = 17; a28 = 15; a14 = 18; return -1; } else if((((a7==1)&&(((a25==1)&&(((a28==15)&&((a4==16)&&(((a26==17)||(a26==18))&&(input==2))))&&(a1==1)))&&!(a3==1)))&&(a14==20))){ a26 = 17; a3 = 1; a14 = 18; return -1; } else if((!(a3==1)&&((((a28==16)&&((a4==16)&&(((((a7==1)&&(a26==19))||(!(a7==1)&&(a26==17)))&&(input==2))&&(a1==1))))&&(a25==1))&&(a14==18)))){ a28 = 15; a3 = 1; a26 = 17; a7 = 1; return -1; } else if(((((a4==17)&&((a25==1)&&((a26==18)&&(((a14==20)&&((input==3)&&(a1==1)))&&(a7==1)))))&&(a3==1))&&(a28==15))){ a4 = 16; a26 = 17; a14 = 18; return -1; } else if((!(a3==1)&&((!(a7==1)&&((a1==1)&&(((a25==1)&&(((input==2)&&((a26==17)||(a26==18)))&&(a4==17)))&&(a14==18))))&&(a28==15)))){ a7 = 1; a28 = 17; a4 = 16; a26 = 18; return -1; } else if(((a25==1)&&((((a28==15)&&(((a4==18)&&(!(a3==1)&&((input==1)&&((a26==18)||(a26==19)))))&&(a1==1)))&&(a14==20))&&!(a7==1)))){ a26 = 17; a3 = 1; a14 = 18; a7 = 1; a4 = 16; return -1; } else if(((a4==17)&&(((a3==1)&&((a1==1)&&((a25==1)&&((input==1)&&((((a7==1)&&(a26==17))&&(a14==19))||((((a26==18)&&!(a7==1))&&(a14==18))||(((a26==19)&&!(a7==1))&&(a14==18))))))))&&(a28==16)))){ a28 = 15; a26 = 17; a4 = 16; a7 = 1; a14 = 18; return -1; } else if(((!(a3==1)&&((a14==18)&&(((a1==1)&&(((((a7==1)&&(a26==19))||(!(a7==1)&&(a26==17)))&&(input==2))&&(a28==15)))&&(a25==1))))&&(a4==18))){ a4 = 16; a7 = 1; a3 = 1; a26 = 17; return -1; } else if(((a4==17)&&((a14==19)&&(((a1==1)&&(((a28==16)&&(!(a3==1)&&((input==2)&&((a26==17)||(a26==18)))))&&(a25==1)))&&!(a7==1))))){ a26 = 18; a28 = 17; a4 = 16; a7 = 1; return 26; } else if(((a14==20)&&((a1==1)&&((a25==1)&&(((((a4==17)&&((a28==15)&&(input==3)))&&(a26==19))&&(a3==1))&&(a7==1)))))){ a7 = 0; a28 = 17; a26 = 18; a14 = 18; return 24; } else if((((a25==1)&&(((a1==1)&&((a4==16)&&(((input==4)&&(((a7==1)&&(a26==19))||((a26==17)&&!(a7==1))))&&(a28==16))))&&!(a3==1)))&&(a14==18))){ a7 = 1; a3 = 1; a28 = 15; a26 = 17; return -1; } else if(((a25==1)&&((a28==17)&&((a1==1)&&((a7==1)&&((a14==18)&&((((input==1)&&!(a3==1))&&(a26==19))&&(a4==16)))))))){ a26 = 18; return -1; } else if(((a3==1)&&(((a25==1)&&(((((((a4==17)&&(a26==19))&&(a28==17))&&!(a7==1))&&(a14==20))||((a14==18)&&(((a28==15)&&((a4==18)&&(a26==17)))&&(a7==1))))&&(input==1)))&&(a1==1)))){ a7 = 1; a26 = 17; a14 = 18; a28 = 15; a4 = 16; return -1; } else if((((a1==1)&&(((((((!(a7==1)&&(a26==19))&&(a14==18))||((a14==19)&&((a7==1)&&(a26==17))))&&(input==6))&&(a4==16))&&(a25==1))&&(a28==17)))&&!(a3==1))){ a14 = 18; a3 = 1; a7 = 1; a28 = 15; a26 = 17; return -1; } else if((((a28==16)&&(!(a3==1)&&((a4==18)&&((((input==1)&&(((a26==19)&&(a7==1))||((a26==17)&&!(a7==1))))&&(a14==19))&&(a25==1)))))&&(a1==1))){ a7 = 0; a28 = 15; a14 = 18; a4 = 17; a26 = 18; return 21; } else if((((a28==15)&&((((!(a3==1)&&((a25==1)&&(((a26==18)||(a26==19))&&(input==2))))&&(a1==1))&&!(a7==1))&&(a14==20)))&&(a4==18))){ a7 = 1; a4 = 16; a3 = 1; a14 = 18; a26 = 17; return -1; } else if((((a7==1)&&(((a1==1)&&(!(a3==1)&&((((input==1)&&(a26==18))&&(a25==1))&&(a28==15))))&&(a4==18)))&&(a14==19))){ a14 = 20; a7 = 0; a4 = 16; return 26; } else if((((a14==19)&&(((!(a7==1)&&(((a1==1)&&(((a26==18)||(a26==19))&&(input==1)))&&(a3==1)))&&(a28==16))&&(a4==18)))&&(a25==1))){ a14 = 18; a4 = 16; a7 = 1; a28 = 15; a26 = 17; return -1; } else if((((a4==17)&&((a28==17)&&(!(a3==1)&&((((((a7==1)&&(a26==19))||(!(a7==1)&&(a26==17)))&&(input==6))&&(a14==19))&&(a1==1)))))&&(a25==1))){ a14 = 18; a7 = 1; a3 = 1; a26 = 17; a28 = 15; a4 = 16; return -1; } else if(((a28==16)&&(((a4==17)&&((((((((a26==18)&&(a7==1))||((a26==19)&&(a7==1)))||(!(a7==1)&&(a26==17)))&&(input==6))&&(a14==20))&&(a1==1))&&!(a3==1)))&&(a25==1)))){ a14 = 19; a26 = 18; a7 = 0; return 26; } else if((((((a25==1)&&(((((input==3)&&(a1==1))&&(a7==1))&&(a4==16))&&(a14==18)))&&(a28==17))&&(a26==19))&&!(a3==1))){ a28 = 15; a3 = 1; a26 = 17; return -1; } else if((((a1==1)&&(((((a28==15)&&((a14==20)&&((((a26==17)||(a26==18))||(a26==19))&&(input==3))))&&!(a3==1))&&(a4==18))&&(a25==1)))&&(a7==1))){ a26 = 18; a7 = 0; return 26; } else if((((a28==16)&&(!(a7==1)&&(((a14==20)&&((a1==1)&&((a4==17)&&(((a26==18)||(a26==19))&&(input==3)))))&&!(a3==1))))&&(a25==1))){ a26 = 17; a28 = 15; return -1; } else if(((a28==17)&&((a7==1)&&(((a25==1)&&(!(a3==1)&&(((a14==20)&&((input==3)&&(((a26==17)||(a26==18))||(a26==19))))&&(a1==1))))&&(a4==17))))){ a14 = 18; a3 = 1; a26 = 17; a4 = 16; a28 = 15; return -1; } else if((((a4==18)&&((a14==20)&&((a3==1)&&((a1==1)&&((a28==17)&&(((input==2)&&(a26==18))&&!(a7==1)))))))&&(a25==1))){ a14 = 18; a7 = 1; a28 = 15; a4 = 16; a26 = 17; return -1; } else if(((a26==19)&&(((a7==1)&&(!(a3==1)&&((a4==16)&&(((a1==1)&&((a25==1)&&(input==1)))&&(a14==19)))))&&(a28==15)))){ a14 = 18; a26 = 18; a28 = 17; return 22; } else if((((a25==1)&&(((((a14==20)&&(((a28==17)&&((a26==19)&&((a4==18)&&(a3==1))))&&!(a7==1)))||((a14==18)&&((a7==1)&&((a28==15)&&((a26==17)&&((a4==16)&&!(a3==1)))))))||((a14==18)&&(((a28==15)&&((a26==18)&&(!(a3==1)&&(a4==16))))&&(a7==1))))&&(input==5)))&&(a1==1))){ a4 = 16; a28 = 15; a14 = 18; a3 = 1; a7 = 1; a26 = 17; return -1; } else if(((((a7==1)&&((a4==17)&&(((a28==17)&&((a25==1)&&(((a26==17)||(a26==18))&&(input==2))))&&(a3==1))))&&(a1==1))&&(a14==18))){ a4 = 16; a28 = 15; a26 = 17; return -1; } else if(((a28==16)&&((((a25==1)&&(((a7==1)&&(((a26==18)&&(input==4))&&!(a3==1)))&&(a14==19)))&&(a1==1))&&(a4==18)))){ a28 = 15; a4 = 16; a14 = 18; a26 = 17; a3 = 1; return -1; } else if((((a4==18)&&((((((a26==17)&&((input==2)&&(a3==1)))&&(a28==15))&&(a14==19))&&(a7==1))&&(a25==1)))&&(a1==1))){ a4 = 16; a14 = 18; return -1; } else if((((a1==1)&&((a25==1)&&((input==1)&&((((a14==20)&&(!(a7==1)&&((a28==17)&&((a4==16)&&(a26==18)))))||((a14==20)&&(((a28==17)&&((a26==19)&&(a4==16)))&&!(a7==1))))||((a14==18)&&((a7==1)&&((a28==15)&&((a26==17)&&(a4==17)))))))))&&!(a3==1))){ a7 = 1; a14 = 18; a4 = 16; a26 = 18; a28 = 17; return -1; } else if(((a1==1)&&((a3==1)&&(((a26==18)&&((a4==18)&&(((a25==1)&&((input==4)&&(a28==17)))&&!(a7==1))))&&(a14==18))))){ a28 = 15; a26 = 17; a4 = 16; a7 = 1; return -1; } else if(((a26==18)&&((a25==1)&&((((a1==1)&&(!(a3==1)&&(((input==1)&&(a14==19))&&(a28==15))))&&!(a7==1))&&(a4==17))))){ a14 = 18; return 21; } else if(((a4==17)&&(((((!(a3==1)&&((a1==1)&&(((a26==17)||(a26==18))&&(input==3))))&&(a28==15))&&(a14==18))&&!(a7==1))&&(a25==1)))){ a7 = 1; a26 = 18; a28 = 17; a4 = 16; return 26; } else if(((a4==17)&&(((a14==20)&&(((a28==15)&&((a7==1)&&((a25==1)&&((input==2)&&((a26==19)||((a26==17)||(a26==18)))))))&&!(a3==1)))&&(a1==1)))){ a26 = 18; a14 = 19; a4 = 16; a28 = 17; return -1; } else if(((a26==18)&&((((a14==18)&&(((((a4==16)&&(input==4))&&(a7==1))&&!(a3==1))&&(a25==1)))&&(a1==1))&&(a28==16)))){ a28 = 15; a3 = 1; a26 = 17; return -1; } else if(((!(a3==1)&&((a25==1)&&((a14==19)&&((a4==16)&&(((a28==17)&&((input==1)&&(a26==18)))&&(a1==1))))))&&!(a7==1))){ a14 = 18; a26 = 17; a28 = 15; a3 = 1; a7 = 1; return -1; } else if((((a25==1)&&((a4==18)&&(((((((a26==17)&&!(a7==1))||(((a26==18)&&(a7==1))||((a7==1)&&(a26==19))))&&(input==2))&&(a28==16))&&(a1==1))&&(a14==19))))&&(a3==1))){ a4 = 16; a14 = 18; a26 = 17; a7 = 1; a28 = 15; return -1; } else if(((((((a14==19)&&(!(a3==1)&&((((a7==1)&&(a26==19))||((a26==17)&&!(a7==1)))&&(input==3))))&&(a25==1))&&(a28==16))&&(a1==1))&&(a4==18))){ a26 = 17; a7 = 1; a4 = 16; a28 = 17; a3 = 1; a14 = 18; return -1; } else if(((a14==19)&&(((a3==1)&&((a25==1)&&(((a28==17)&&((input==2)&&((!(a7==1)&&(a26==17))||(((a26==18)&&(a7==1))||((a7==1)&&(a26==19))))))&&(a4==18))))&&(a1==1)))){ a14 = 20; a28 = 16; a7 = 1; a26 = 17; return -1; } else if((((a28==16)&&((!(a3==1)&&(((((a26==18)&&(input==3))&&(a4==18))&&(a14==19))&&!(a7==1)))&&(a1==1)))&&(a25==1))){ a3 = 1; a28 = 15; a14 = 20; a7 = 1; a26 = 19; a4 = 16; return -1; } else if(((!(a7==1)&&((((a25==1)&&((a1==1)&&((((a26==18)||(a26==19))&&(input==1))&&(a4==18))))&&(a28==16))&&!(a3==1)))&&(a14==20))){ a26 = 18; a14 = 18; a28 = 15; a4 = 17; return 23; } else if(((a25==1)&&((a4==16)&&((a26==19)&&((a1==1)&&((((a28==15)&&((input==5)&&!(a3==1)))&&(a14==19))&&!(a7==1))))))){ a14 = 18; a7 = 1; a3 = 1; a26 = 17; return -1; } else if((((a1==1)&&(!(a3==1)&&((((input==3)&&(((((a26==19)&&!(a7==1))&&(a14==18))||((a14==19)&&((a26==17)&&(a7==1))))||((a14==19)&&((a26==18)&&(a7==1)))))&&(a28==15))&&(a4==17))))&&(a25==1))){ a26 = 17; a3 = 1; a4 = 16; a14 = 18; a7 = 1; return -1; } else if(((a4==18)&&((a14==20)&&(((((a1==1)&&(!(a7==1)&&((a28==15)&&(input==5))))&&(a26==17))&&(a25==1))&&!(a3==1))))){ a14 = 18; a7 = 1; a4 = 16; a3 = 1; return -1; } else if((((a25==1)&&(!(a3==1)&&((input==5)&&(((a14==18)&&((a7==1)&&((a28==15)&&((a4==17)&&(a26==17)))))||(((!(a7==1)&&(((a4==16)&&(a26==18))&&(a28==17)))&&(a14==20))||((!(a7==1)&&((a28==17)&&((a4==16)&&(a26==19))))&&(a14==20)))))))&&(a1==1))){ a7 = 1; a4 = 16; a26 = 17; a3 = 1; a28 = 15; a14 = 18; return -1; } else if(((a7==1)&&((a4==18)&&((((a25==1)&&((a28==16)&&((a14==20)&&((input==4)&&(a3==1)))))&&(a26==17))&&(a1==1))))){ return -1; } else if(((((a25==1)&&((a4==16)&&(((((a14==20)&&(((a26==18)&&(a28==16))&&!(a7==1)))||((((a26==19)&&(a28==16))&&!(a7==1))&&(a14==20)))||((a14==18)&&((a7==1)&&((a28==17)&&(a26==17)))))&&(input==4))))&&(a1==1))&&!(a3==1))){ a7 = 1; a28 = 15; a14 = 18; a26 = 17; a3 = 1; return -1; } else if((((a4==17)&&((((input==3)&&((((a14==20)&&(((a26==18)&&(a28==15))&&!(a7==1)))||((!(a7==1)&&((a26==19)&&(a28==15)))&&(a14==20)))||((a14==18)&&((a7==1)&&((a26==17)&&(a28==16))))))&&(a3==1))&&(a25==1)))&&(a1==1))){ a14 = 18; a28 = 15; a26 = 17; a4 = 16; a7 = 1; return -1; } else if(((((((a14==18)&&((a7==1)&&((a26==18)&&((input==5)&&(a1==1)))))&&!(a3==1))&&(a28==17))&&(a25==1))&&(a4==16))){ a26 = 17; a3 = 1; a28 = 15; return -1; } else if(((a4==18)&&(((a25==1)&&((((a3==1)&&(!(a7==1)&&(((a26==17)||(a26==18))&&(input==6))))&&(a1==1))&&(a28==15)))&&(a14==19)))){ a7 = 1; a26 = 17; a14 = 18; a4 = 16; return -1; } else if((((a25==1)&&(!(a3==1)&&(((a1==1)&&((a28==17)&&((((a7==1)&&(a26==19))||((a26==17)&&!(a7==1)))&&(input==1))))&&(a4==17))))&&(a14==19))){ a28 = 15; a4 = 16; a3 = 1; a7 = 1; a14 = 18; a26 = 17; return -1; } else if(((((((a28==15)&&((((input==2)&&!(a3==1))&&(a4==18))&&(a1==1)))&&!(a7==1))&&(a14==20))&&(a26==17))&&(a25==1))){ a7 = 1; a4 = 16; a14 = 18; a3 = 1; return -1; } else if((((((a1==1)&&((a4==17)&&(!(a7==1)&&(((input==3)&&(a14==19))&&(a25==1)))))&&(a26==19))&&!(a3==1))&&(a28==17))){ a7 = 1; a26 = 17; a28 = 15; a14 = 18; a4 = 16; a3 = 1; return -1; } else if(((a25==1)&&(((a3==1)&&((a7==1)&&(((a14==18)&&((((a26==18)||(a26==19))&&(input==3))&&(a28==15)))&&(a4==18))))&&(a1==1)))){ a26 = 17; a4 = 16; return -1; } else if(((a1==1)&&((a4==18)&&((a28==16)&&((a14==20)&&(((a25==1)&&(((((a26==18)&&(a7==1))||((a26==19)&&(a7==1)))||((a26==17)&&!(a7==1)))&&(input==5)))&&(a3==1))))))){ a4 = 16; a26 = 17; a28 = 15; a14 = 18; a7 = 1; return -1; } else if(((((a1==1)&&((a3==1)&&((((input==4)&&((!(a7==1)&&(a26==17))||(((a7==1)&&(a26==18))||((a26==19)&&(a7==1)))))&&(a4==18))&&(a25==1))))&&(a28==16))&&(a14==20))){ a4 = 16; a28 = 15; a14 = 18; a26 = 17; a7 = 1; return -1; } else if(((a25==1)&&((a1==1)&&((((a3==1)&&((a14==18)&&((((a26==17)&&!(a7==1))||(((a26==18)&&(a7==1))||((a26==19)&&(a7==1))))&&(input==1))))&&(a28==17))&&(a4==18))))){ a4 = 16; a7 = 1; a26 = 17; a28 = 15; return -1; } else if((((a4==17)&&(((a14==19)&&((a3==1)&&((a1==1)&&((input==5)&&((!(a7==1)&&(a26==18))||(((a7==1)&&(a26==19))||(!(a7==1)&&(a26==17))))))))&&(a25==1)))&&(a28==15))){ a7 = 0; a28 = 16; a14 = 18; a26 = 17; return 23; } else if((((((((!(a7==1)&&(((a26==19)||((a26==17)||(a26==18)))&&(input==3)))&&(a25==1))&&(a14==20))&&(a4==17))&&(a28==17))&&!(a3==1))&&(a1==1))){ a3 = 1; a14 = 18; a26 = 17; a4 = 16; a7 = 1; a28 = 15; return -1; } else if(((a26==17)&&((a3==1)&&((((a14==20)&&((a1==1)&&(((input==6)&&!(a7==1))&&(a28==15))))&&(a25==1))&&(a4==17))))){ a14 = 18; a4 = 16; a7 = 1; return -1; } else if(((a4==17)&&(((((a1==1)&&((a14==20)&&(((input==3)&&((a26==18)||(a26==19)))&&(a25==1))))&&!(a7==1))&&(a28==16))&&(a3==1)))){ a7 = 1; a14 = 18; a26 = 17; a4 = 16; a28 = 15; return -1; } else if(((a14==19)&&((!(a3==1)&&(((((input==6)&&((((a26==19)&&(a7==1))||(!(a7==1)&&(a26==17)))||((a26==18)&&!(a7==1))))&&(a25==1))&&(a28==16))&&(a4==16)))&&(a1==1)))){ a3 = 1; a28 = 15; a7 = 1; a14 = 18; a26 = 17; return -1; } else if(((!(a3==1)&&((a1==1)&&((a4==16)&&((((((a7==1)&&(a26==18))&&(a14==20))||(((!(a7==1)&&(a26==19))&&(a14==19))||(((a26==17)&&(a7==1))&&(a14==20))))&&(input==1))&&(a28==17)))))&&(a25==1))){ a14 = 18; a26 = 17; a7 = 1; a28 = 15; a3 = 1; return -1; } else if(((((a25==1)&&((((a14==20)&&((a7==1)&&((input==5)&&(((a26==17)||(a26==18))||(a26==19)))))&&(a1==1))&&(a28==15)))&&!(a3==1))&&(a4==17))){ a3 = 1; a14 = 18; a26 = 17; a4 = 16; return -1; } else if((((a4==17)&&((a1==1)&&(((input==2)&&((((!(a7==1)&&((a28==15)&&(a26==18)))&&(a14==20))||((a14==20)&&(!(a7==1)&&((a26==19)&&(a28==15)))))||((((a26==17)&&(a28==16))&&(a7==1))&&(a14==18))))&&(a25==1))))&&(a3==1))){ a4 = 18; a14 = 18; a28 = 15; a26 = 19; a7 = 1; return 24; } else if((((((((!(a7==1)&&((a28==17)&&(((a4==18)&&(a3==1))&&(a26==19))))&&(a14==20))||((a14==18)&&((a7==1)&&((a28==15)&&((a26==17)&&(!(a3==1)&&(a4==16)))))))||((((a28==15)&&(((a4==16)&&!(a3==1))&&(a26==18)))&&(a7==1))&&(a14==18)))&&(input==4))&&(a1==1))&&(a25==1))){ a14 = 18; a4 = 16; a26 = 17; a3 = 1; a7 = 1; a28 = 15; return -1; } else if((((((a3==1)&&((((((a26==17)||(a26==18))&&(input==4))&&(a28==17))&&(a25==1))&&(a1==1)))&&(a4==17))&&(a14==18))&&(a7==1))){ a4 = 18; a28 = 16; a7 = 0; a26 = 18; return 22; } else if((((a28==15)&&((a25==1)&&((((input==5)&&(((a14==18)&&((a26==19)&&!(a7==1)))||((a14==19)&&((a26==17)&&(a7==1)))))&&!(a3==1))&&(a1==1))))&&(a4==18))){ a3 = 1; a14 = 18; a7 = 1; a26 = 17; a4 = 16; return -1; } return calculate_output3(input); } int calculate_output3(int input) { if((!(a3==1)&&((((a14==18)&&((a7==1)&&(((a4==17)&&(((a26==17)||(a26==18))&&(input==1)))&&(a28==17))))&&(a1==1))&&(a25==1)))){ a28 = 15; a26 = 17; a3 = 1; a4 = 16; return -1; } else if(((a7==1)&&((a1==1)&&(((a14==20)&&((((a28==17)&&(((a26==19)||((a26==17)||(a26==18)))&&(input==1)))&&!(a3==1))&&(a25==1)))&&(a4==17))))){ a7 = 0; a26 = 17; a28 = 15; a4 = 18; a14 = 18; return 21; } else if((((((((a14==20)&&((a4==18)&&((a25==1)&&(input==3))))&&(a3==1))&&(a7==1))&&(a1==1))&&(a28==15))&&(a26==19))){ a4 = 16; a26 = 17; a14 = 18; return -1; } else if(((((a25==1)&&((a14==20)&&(((a1==1)&&((input==2)&&((!(a7==1)&&(a26==17))||(((a7==1)&&(a26==18))||((a26==19)&&(a7==1))))))&&(a3==1))))&&(a4==18))&&(a28==17))){ a4 = 16; a7 = 1; a14 = 18; a26 = 17; a28 = 15; return -1; } else if(((((((((a28==15)&&((input==6)&&((a26==17)||(a26==18))))&&!(a3==1))&&(a4==18))&&(a25==1))&&(a1==1))&&(a7==1))&&(a14==18))){ a4 = 16; a26 = 17; a3 = 1; return -1; } else if((((a25==1)&&(!(a3==1)&&((a4==16)&&(((input==1)&&(((a14==18)&&(!(a7==1)&&(a26==19)))||(((a26==17)&&(a7==1))&&(a14==19))))&&(a1==1)))))&&(a28==17))){ a4 = 17; a14 = 19; a7 = 0; a28 = 15; a26 = 19; return 21; } else if((!(a7==1)&&(((a14==18)&&((a3==1)&&((((a25==1)&&((input==2)&&(a1==1)))&&(a4==18))&&(a26==18))))&&(a28==17)))){ a26 = 17; a4 = 16; a28 = 15; a7 = 1; return -1; } else if(((((a4==17)&&((a14==20)&&((a1==1)&&((((((a7==1)&&(a26==18))||((a7==1)&&(a26==19)))||(!(a7==1)&&(a26==17)))&&(input==1))&&(a28==16)))))&&!(a3==1))&&(a25==1))){ a26 = 19; a7 = 1; return -1; } else if(((((a7==1)&&((((((input==1)&&!(a3==1))&&(a4==16))&&(a28==16))&&(a14==18))&&(a1==1)))&&(a26==18))&&(a25==1))){ a26 = 17; a3 = 1; a28 = 15; return -1; } else if((!(a7==1)&&(((a1==1)&&(((a3==1)&&(((a25==1)&&(((a26==18)||(a26==19))&&(input==3)))&&(a14==19)))&&(a28==16)))&&(a4==18)))){ a26 = 17; a4 = 16; a7 = 1; a14 = 18; a28 = 15; return -1; } else if((((a3==1)&&((((input==6)&&(((a14==18)&&(((a28==16)&&(a26==17))&&(a7==1)))||(((a14==20)&&(!(a7==1)&&((a26==18)&&(a28==15))))||((!(a7==1)&&((a26==19)&&(a28==15)))&&(a14==20)))))&&(a4==18))&&(a25==1)))&&(a1==1))){ a26 = 17; a14 = 18; a4 = 16; a7 = 1; a28 = 15; return -1; } else if(((a4==18)&&(((a28==15)&&((a25==1)&&(((((a14==19)&&(input==5))&&(a7==1))&&(a3==1))&&(a26==19))))&&(a1==1)))){ a4 = 16; a14 = 18; a26 = 17; return -1; } else if(((a1==1)&&((a4==17)&&((((((((a26==17)&&(a7==1))&&(a14==19))||(((a14==18)&&((a26==18)&&!(a7==1)))||((a14==18)&&(!(a7==1)&&(a26==19)))))&&(input==5))&&(a25==1))&&(a3==1))&&(a28==16))))){ a4 = 16; a14 = 18; a7 = 1; a26 = 17; a28 = 15; return -1; } else if(((!(a7==1)&&(!(a3==1)&&(((a14==18)&&(((a4==16)&&((a25==1)&&(input==4)))&&(a28==17)))&&(a26==17))))&&(a1==1))){ a28 = 15; a7 = 1; a3 = 1; return -1; } else if(((((a14==20)&&(((((a4==17)&&((input==3)&&(a26==17)))&&(a3==1))&&(a25==1))&&(a1==1)))&&!(a7==1))&&(a28==15))){ a7 = 1; a14 = 18; a4 = 16; return -1; } else if((((((a1==1)&&(!(a3==1)&&((input==3)&&(((a14==19)&&((a7==1)&&(a26==18)))||(((!(a7==1)&&(a26==19))&&(a14==18))||(((a7==1)&&(a26==17))&&(a14==19)))))))&&(a28==17))&&(a25==1))&&(a4==18))){ a4 = 17; a28 = 15; a7 = 0; a26 = 18; a14 = 18; return 24; } else if(((a4==17)&&(((((input==6)&&((((((a28==15)&&(a26==18))&&!(a7==1))&&(a14==20))||((((a26==19)&&(a28==15))&&!(a7==1))&&(a14==20)))||(((a7==1)&&((a28==16)&&(a26==17)))&&(a14==18))))&&(a25==1))&&(a3==1))&&(a1==1)))){ a4 = 16; a28 = 15; a14 = 18; a26 = 17; a7 = 1; return -1; } else if(((a14==19)&&(((a1==1)&&(((!(a3==1)&&((((a7==1)&&(a26==19))||((a26==17)&&!(a7==1)))&&(input==5)))&&(a25==1))&&(a28==16)))&&(a4==18)))){ a4 = 16; a3 = 1; a7 = 0; a26 = 18; a28 = 15; return -1; } else if(((((a3==1)&&((((((((a26==18)&&(a7==1))||((a7==1)&&(a26==19)))||(!(a7==1)&&(a26==17)))&&(input==5))&&(a25==1))&&(a4==17))&&(a1==1)))&&(a28==16))&&(a14==18))){ a26 = 18; a28 = 15; a4 = 18; a7 = 1; a14 = 19; return 22; } else if(((((a14==18)&&(((((a3==1)&&((input==5)&&((a26==19)||((a26==17)||(a26==18)))))&&(a4==18))&&(a28==15))&&(a25==1)))&&!(a7==1))&&(a1==1))){ a7 = 1; a4 = 16; a26 = 17; return -1; } else if(((a14==20)&&((((a4==17)&&(((a28==17)&&(((a1==1)&&(input==2))&&(a26==18)))&&(a3==1)))&&(a25==1))&&(a7==1)))){ a4 = 16; a14 = 18; a28 = 15; a26 = 17; return -1; } else if(((((((a28==15)&&((((a14==20)&&((a7==1)&&(a26==18)))||(((a14==19)&&(!(a7==1)&&(a26==19)))||(((a26==17)&&(a7==1))&&(a14==20))))&&(input==4)))&&(a1==1))&&(a4==18))&&(a25==1))&&(a3==1))){ a26 = 17; a7 = 1; a14 = 18; a4 = 16; return -1; } else if(((((a28==16)&&((a3==1)&&((a1==1)&&((a4==18)&&(((((a26==18)&&(a7==1))||((a26==19)&&(a7==1)))||(!(a7==1)&&(a26==17)))&&(input==4))))))&&(a14==18))&&(a25==1))){ a4 = 16; a7 = 1; a26 = 17; a28 = 15; return -1; } else if(((a1==1)&&((a28==16)&&(((a25==1)&&(!(a3==1)&&((a14==18)&&(((input==2)&&((a26==17)||(a26==18)))&&(a7==1)))))&&(a4==18))))){ a4 = 16; a26 = 17; a28 = 15; a3 = 1; return -1; } else if(((a4==18)&&((a1==1)&&(((a25==1)&&((input==2)&&((((a7==1)&&((a28==17)&&(a26==17)))&&(a14==18))||(((a14==20)&&(((a28==16)&&(a26==18))&&!(a7==1)))||((((a28==16)&&(a26==19))&&!(a7==1))&&(a14==20))))))&&(a3==1))))){ a4 = 16; a14 = 18; a7 = 1; a28 = 15; a26 = 17; return -1; } else if(((a28==17)&&((((a25==1)&&((a14==19)&&((((input==2)&&!(a3==1))&&!(a7==1))&&(a26==17))))&&(a1==1))&&(a4==16)))){ a14 = 18; a7 = 1; a3 = 1; a28 = 15; return -1; } else if(((a3==1)&&(((((a1==1)&&((((a25==1)&&(input==2))&&(a4==18))&&(a14==20)))&&(a7==1))&&(a28==16))&&(a26==17)))){ return -1; } else if((((a4==18)&&(((a28==15)&&(!(a3==1)&&((input==6)&&(((a14==18)&&(!(a7==1)&&(a26==19)))||(((a26==17)&&(a7==1))&&(a14==19))))))&&(a25==1)))&&(a1==1))){ a14 = 18; a3 = 1; a26 = 17; a4 = 16; a7 = 1; return -1; } else if(((a1==1)&&((a25==1)&&(((a4==18)&&((((input==5)&&(((a7==1)&&(a26==19))||(!(a7==1)&&(a26==17))))&&!(a3==1))&&(a14==19)))&&(a28==15))))){ a3 = 1; a4 = 16; a26 = 17; a7 = 1; a14 = 18; return -1; } else if((((a4==18)&&(((!(a3==1)&&(((a1==1)&&((input==3)&&((a26==17)||(a26==18))))&&(a25==1)))&&(a7==1))&&(a28==17)))&&(a14==18))){ a28 = 15; a4 = 17; a3 = 1; a26 = 19; a7 = 0; return -1; } else if((!(a3==1)&&((((a28==15)&&((a1==1)&&((((a26==19)&&(input==1))&&(a7==1))&&(a25==1))))&&(a14==18))&&(a4==16)))){ a26 = 17; a3 = 1; return -1; } else if(((a25==1)&&((((((a28==16)&&(((input==5)&&(a26==18))&&(a14==19)))&&(a1==1))&&(a7==1))&&(a4==18))&&!(a3==1)))){ a14 = 18; a26 = 17; a28 = 15; a3 = 1; a4 = 16; return -1; } else if((!(a3==1)&&((a25==1)&&((a1==1)&&((input==4)&&((((((a28==17)&&((a26==18)&&(a4==16)))&&!(a7==1))&&(a14==20))||((a14==20)&&((((a26==19)&&(a4==16))&&(a28==17))&&!(a7==1))))||((((a28==15)&&((a26==17)&&(a4==17)))&&(a7==1))&&(a14==18)))))))){ a28 = 15; a14 = 18; a26 = 17; a7 = 1; a4 = 16; a3 = 1; return -1; } else if(((a14==19)&&(((a1==1)&&((((a25==1)&&((input==2)&&((!(a7==1)&&(a26==17))||(((a26==18)&&(a7==1))||((a26==19)&&(a7==1))))))&&(a4==17))&&(a3==1)))&&(a28==17)))){ a28 = 15; a26 = 17; a4 = 16; a14 = 18; a7 = 1; return -1; } else if(((a4==17)&&((a1==1)&&(((((((a14==20)&&(((a28==15)&&(a26==18))&&!(a7==1)))||((a14==20)&&(((a26==19)&&(a28==15))&&!(a7==1))))||(((a7==1)&&((a28==16)&&(a26==17)))&&(a14==18)))&&(input==1))&&(a25==1))&&(a3==1))))){ a4 = 16; a7 = 1; a26 = 17; a28 = 15; a14 = 18; return -1; } else if((((a1==1)&&(!(a3==1)&&(((a14==20)&&(((input==6)&&(((a26==19)&&(a7==1))||(!(a7==1)&&(a26==17))))&&(a25==1)))&&(a28==16))))&&(a4==16))){ a28 = 15; a7 = 1; a26 = 17; a14 = 18; a3 = 1; return -1; } else if(((((((a25==1)&&(((a28==15)&&((input==6)&&(a14==20)))&&(a4==18)))&&!(a7==1))&&(a1==1))&&!(a3==1))&&(a26==17))){ a7 = 1; a14 = 18; a4 = 16; a3 = 1; return -1; } else if((((((((a4==16)&&(!(a3==1)&&((input==4)&&((a26==17)||(a26==18)))))&&(a25==1))&&(a14==19))&&(a1==1))&&(a28==15))&&(a7==1))){ a14 = 18; a26 = 17; a3 = 1; return -1; } else if(((a25==1)&&((!(a7==1)&&((((a4==17)&&((a14==18)&&(((a26==18)||(a26==19))&&(input==4))))&&(a28==16))&&(a1==1)))&&!(a3==1)))){ a26 = 19; a28 = 17; a7 = 1; return 26; } else if((((((a1==1)&&((input==1)&&(((a14==18)&&(((a26==17)&&(a28==16))&&(a7==1)))||(((((a26==18)&&(a28==15))&&!(a7==1))&&(a14==20))||((((a26==19)&&(a28==15))&&!(a7==1))&&(a14==20))))))&&(a25==1))&&!(a3==1))&&(a4==17))){ a26 = 17; a28 = 16; a14 = 19; a7 = 0; return 22; } else if(((a4==17)&&((a3==1)&&((a14==18)&&((a25==1)&&((((a28==17)&&((input==3)&&((a26==17)||(a26==18))))&&(a7==1))&&(a1==1))))))){ a4 = 16; a26 = 17; a28 = 15; return -1; } else if((((a14==18)&&(!(a3==1)&&((a1==1)&&(((a4==17)&&((input==6)&&((!(a7==1)&&(a26==17))||(((a26==18)&&(a7==1))||((a26==19)&&(a7==1))))))&&(a28==16)))))&&(a25==1))){ a28 = 17; a7 = 1; a26 = 18; return 24; } else if((((a25==1)&&((((((((a26==17)||(a26==18))&&(input==6))&&(a3==1))&&(a1==1))&&(a4==17))&&(a28==17))&&(a7==1)))&&(a14==18))){ a28 = 15; a26 = 17; a4 = 16; return -1; } else if(((a1==1)&&((a4==16)&&(!(a3==1)&&(((((((a26==19)&&(a28==15))&&!(a7==1))&&(a14==20))||((a14==18)&&(((a26==17)&&(a28==16))&&(a7==1))))&&(input==3))&&(a25==1)))))){ a14 = 18; a26 = 17; a28 = 15; a7 = 1; a3 = 1; return -1; } else if(((((a26==19)&&((((((a14==19)&&(input==2))&&(a7==1))&&(a1==1))&&(a28==15))&&(a25==1)))&&(a4==16))&&!(a3==1))){ a28 = 17; a14 = 18; return 24; } else if(((((a1==1)&&((a14==19)&&((a28==15)&&(((((a26==19)&&(a7==1))||(!(a7==1)&&(a26==17)))&&(input==3))&&(a4==17)))))&&(a25==1))&&!(a3==1))){ a7 = 1; a3 = 1; a14 = 18; a4 = 16; a26 = 17; return -1; } else if(((((a25==1)&&((((((((a26==19)&&!(a7==1))&&(a14==18))||(((a7==1)&&(a26==17))&&(a14==19)))||((a14==19)&&((a26==18)&&(a7==1))))&&(input==5))&&!(a3==1))&&(a1==1)))&&(a28==15))&&(a4==17))){ a7 = 1; a3 = 1; a26 = 17; a14 = 18; a4 = 16; return -1; } else if(((a4==18)&&((a14==20)&&(((((a1==1)&&((((a26==19)&&(a7==1))||((a26==17)&&!(a7==1)))&&(input==1)))&&(a25==1))&&(a28==16))&&!(a3==1))))){ a26 = 19; a3 = 1; a7 = 0; a28 = 15; a4 = 16; a14 = 18; return -1; } else if(((a28==17)&&((a25==1)&&((a1==1)&&((a7==1)&&((!(a3==1)&&((a26==18)&&((input==3)&&(a14==18))))&&(a4==16))))))){ a3 = 1; a28 = 16; a26 = 19; a4 = 18; return -1; } else if((((a4==17)&&((a25==1)&&(((a28==16)&&((((((a26==18)&&(a7==1))||((a7==1)&&(a26==19)))||(!(a7==1)&&(a26==17)))&&(input==5))&&(a3==1)))&&(a1==1))))&&(a14==19))){ a4 = 16; a14 = 18; a7 = 1; a26 = 17; a28 = 15; return -1; } else if((((a28==17)&&((a4==18)&&(!(a3==1)&&((a7==1)&&((((input==1)&&((a26==17)||(a26==18)))&&(a1==1))&&(a25==1))))))&&(a14==18))){ a26 = 17; a7 = 0; return 21; } else if((((a14==19)&&(((a25==1)&&(((((((a26==17)||(a26==18))||(a26==19))&&(input==1))&&(a4==17))&&!(a3==1))&&(a28==16)))&&(a7==1)))&&(a1==1))){ a26 = 17; a4 = 16; a3 = 1; a14 = 18; a28 = 15; return -1; } else if((((a25==1)&&((((a3==1)&&((a1==1)&&((input==4)&&((!(a7==1)&&(a26==17))||(((a7==1)&&(a26==18))||((a7==1)&&(a26==19)))))))&&(a28==17))&&(a4==18)))&&(a14==20))){ a26 = 17; a28 = 15; a7 = 1; a4 = 16; a14 = 18; return -1; } else if(((a3==1)&&((a4==17)&&(((a1==1)&&((a26==17)&&(((a25==1)&&((a28==15)&&(input==1)))&&!(a7==1))))&&(a14==20))))){ a28 = 17; a14 = 19; a26 = 19; return 24; } else if(((a4==17)&&(((a1==1)&&((a14==20)&&((!(a7==1)&&(((a28==15)&&(input==6))&&!(a3==1)))&&(a26==17))))&&(a25==1)))){ a26 = 18; a7 = 1; a28 = 17; a4 = 16; a14 = 19; return -1; } else if(((a25==1)&&(((a28==15)&&((((a14==18)&&(!(a7==1)&&((input==4)&&((a26==19)||((a26==17)||(a26==18))))))&&!(a3==1))&&(a1==1)))&&(a4==16)))){ a14 = 20; a28 = 16; a26 = 17; return 24; } else if(((((a14==20)&&((((a1==1)&&((a26==17)&&((input==4)&&!(a7==1))))&&(a4==17))&&!(a3==1)))&&(a25==1))&&(a28==15))){ a4 = 16; a7 = 1; a14 = 18; a3 = 1; return -1; } else if((((((a3==1)&&((input==5)&&(((a14==18)&&(((a28==17)&&(a26==17))&&(a7==1)))||(((((a28==16)&&(a26==18))&&!(a7==1))&&(a14==20))||((((a26==19)&&(a28==16))&&!(a7==1))&&(a14==20))))))&&(a25==1))&&(a4==18))&&(a1==1))){ a26 = 17; a7 = 1; a4 = 16; a14 = 18; a28 = 15; return -1; } else if((((a14==19)&&(((a28==15)&&((a25==1)&&((a3==1)&&(((!(a7==1)&&(a26==18))||(((a26==19)&&(a7==1))||(!(a7==1)&&(a26==17))))&&(input==6)))))&&(a1==1)))&&(a4==17))){ a4 = 16; a14 = 18; a26 = 17; a7 = 1; return -1; } else if((((a14==18)&&((a25==1)&&((((a4==18)&&((a3==1)&&(((a26==18)||(a26==19))&&(input==1))))&&(a7==1))&&(a1==1))))&&(a28==15))){ a26 = 17; a4 = 16; return -1; } else if(((((((a1==1)&&((((input==6)&&(a25==1))&&(a26==17))&&!(a3==1)))&&!(a7==1))&&(a4==16))&&(a28==17))&&(a14==19))){ a14 = 18; a7 = 1; a3 = 1; a28 = 15; return -1; } else if(((((a14==18)&&((a4==18)&&((((((a26==18)&&!(a7==1))||(((a26==19)&&(a7==1))||(!(a7==1)&&(a26==17))))&&(input==2))&&!(a3==1))&&(a25==1))))&&(a28==17))&&(a1==1))){ a28 = 15; a26 = 17; a7 = 0; a4 = 17; return 23; } else if(((((((!(a3==1)&&((((a26==17)||(a26==18))&&(input==3))&&(a1==1)))&&(a14==19))&&(a7==1))&&(a25==1))&&(a4==16))&&(a28==15))){ a26 = 17; a3 = 1; a14 = 18; return -1; } else if(((a25==1)&&((((input==2)&&((((!(a7==1)&&((a28==17)&&((a26==18)&&(a4==16))))&&(a14==20))||((a14==20)&&(!(a7==1)&&((a28==17)&&((a26==19)&&(a4==16))))))||(((a7==1)&&(((a4==17)&&(a26==17))&&(a28==15)))&&(a14==18))))&&!(a3==1))&&(a1==1)))){ a28 = 15; a14 = 18; a26 = 17; a4 = 16; a3 = 1; a7 = 1; return -1; } else if((((a25==1)&&((((((input==6)&&((((a26==18)&&(a7==1))||((a7==1)&&(a26==19)))||((a26==17)&&!(a7==1))))&&(a14==20))&&(a3==1))&&(a4==18))&&(a1==1)))&&(a28==16))){ a28 = 15; a3 = 0; a7 = 0; a4 = 16; a26 = 18; return 23; } else if(((a28==16)&&(((!(a3==1)&&((((a25==1)&&(((a26==18)||(a26==19))&&(input==1)))&&(a4==17))&&!(a7==1)))&&(a1==1))&&(a14==18)))){ a3 = 1; a26 = 17; a4 = 16; a7 = 1; a28 = 15; return -1; } else if((((a25==1)&&(!(a7==1)&&(((a14==18)&&((((((a26==17)||(a26==18))||(a26==19))&&(input==1))&&!(a3==1))&&(a4==16)))&&(a1==1))))&&(a28==15))){ a26 = 17; a7 = 1; a3 = 1; return -1; } else if(((((((a1==1)&&((a25==1)&&((input==3)&&(((a7==1)&&(a26==19))||((a26==17)&&!(a7==1))))))&&(a4==17))&&(a28==17))&&(a14==18))&&(a3==1))){ a28 = 15; a4 = 16; a7 = 1; a26 = 17; return -1; } else if((((a1==1)&&((!(a3==1)&&((a28==15)&&((a4==18)&&((input==6)&&(((a7==1)&&(a26==19))||(!(a7==1)&&(a26==17)))))))&&(a14==18)))&&(a25==1))){ a26 = 17; a7 = 1; a3 = 1; a4 = 16; return -1; } else if(((((a7==1)&&((((!(a3==1)&&((a26==17)&&(input==4)))&&(a14==20))&&(a25==1))&&(a28==16)))&&(a4==17))&&(a1==1))){ a3 = 1; a28 = 15; a14 = 18; a4 = 16; return -1; } else if((((a28==17)&&(((a4==17)&&((a3==1)&&((input==6)&&((((a7==1)&&(a26==17))&&(a14==20))||(((a14==19)&&(!(a7==1)&&(a26==18)))||((!(a7==1)&&(a26==19))&&(a14==19)))))))&&(a25==1)))&&(a1==1))){ a14 = 20; a4 = 18; a26 = 17; a7 = 1; a28 = 16; return 26; } else if(((a4==17)&&(((((a28==15)&&(!(a7==1)&&(!(a3==1)&&((a1==1)&&(input==3)))))&&(a25==1))&&(a26==18))&&(a14==19)))){ a26 = 17; a14 = 18; a4 = 16; a7 = 1; a3 = 1; return -1; } else if(((a28==17)&&((a25==1)&&((a3==1)&&(((a4==17)&&(((((a14==19)&&(!(a7==1)&&(a26==18)))||(((a26==19)&&!(a7==1))&&(a14==19)))||((a14==20)&&((a7==1)&&(a26==17))))&&(input==5)))&&(a1==1)))))){ a28 = 15; a14 = 18; a4 = 16; a26 = 17; a7 = 1; return -1; } else if(((a4==18)&&(((((((a3==1)&&((a14==19)&&(input==5)))&&(a7==1))&&(a1==1))&&(a26==17))&&(a28==16))&&(a25==1)))){ a4 = 16; a14 = 18; a28 = 15; return -1; } else if(((a25==1)&&(((a1==1)&&((a4==17)&&(((a7==1)&&(((input==5)&&((a26==17)||(a26==18)))&&(a14==18)))&&(a3==1))))&&(a28==17)))){ a4 = 16; a28 = 15; a26 = 17; return -1; } else if((((((a25==1)&&(((a4==17)&&(((a26==19)&&(input==6))&&(a14==19)))&&!(a7==1)))&&!(a3==1))&&(a28==17))&&(a1==1))){ a4 = 16; a14 = 18; a7 = 1; a3 = 1; a28 = 15; a26 = 17; return -1; } else if((((a28==15)&&(((((a25==1)&&(!(a7==1)&&((input==3)&&((a26==19)||((a26==17)||(a26==18))))))&&(a14==18))&&(a1==1))&&(a3==1)))&&(a4==18))){ a4 = 16; a26 = 17; a7 = 1; return -1; } else if(((a26==18)&&(((a14==20)&&((((a3==1)&&((a1==1)&&((a4==18)&&(input==5))))&&!(a7==1))&&(a28==17)))&&(a25==1)))){ a4 = 16; a7 = 1; a26 = 17; a28 = 15; a14 = 18; return -1; } else if((((a1==1)&&((a4==18)&&((a25==1)&&((a7==1)&&((a14==20)&&(((input==2)&&(((a26==17)||(a26==18))||(a26==19)))&&!(a3==1)))))))&&(a28==15))){ a4 = 16; a14 = 18; a3 = 1; a26 = 17; return -1; } else if((((a14==18)&&(((a28==15)&&((a3==1)&&((a4==18)&&(((((a26==17)||(a26==18))||(a26==19))&&(input==1))&&(a1==1)))))&&(a25==1)))&&!(a7==1))){ a7 = 1; a4 = 16; a26 = 17; return -1; } else if(((((a28==16)&&((a1==1)&&(((input==2)&&(((a14==18)&&((a26==19)&&!(a7==1)))||(((a7==1)&&(a26==17))&&(a14==19))))&&!(a3==1))))&&(a25==1))&&(a4==18))){ a14 = 19; a26 = 18; a7 = 0; return 24; } else if((((a25==1)&&(!(a3==1)&&(((((((a14==19)&&((a26==19)&&!(a7==1)))||((a14==20)&&((a7==1)&&(a26==17))))||((a14==20)&&((a7==1)&&(a26==18))))&&(input==3))&&(a4==18))&&(a28==16))))&&(a1==1))){ a7 = 1; a26 = 18; a14 = 20; return -1; } else if(((a4==18)&&((((a25==1)&&((a28==16)&&(((input==2)&&(((a7==1)&&(a26==19))||((a26==17)&&!(a7==1))))&&!(a3==1))))&&(a1==1))&&(a14==20)))){ a28 = 17; a7 = 0; a3 = 1; a14 = 18; a26 = 17; a4 = 16; return -1; } else if((((((a3==1)&&((a28==16)&&((a1==1)&&(!(a7==1)&&(((a26==18)||(a26==19))&&(input==1))))))&&(a4==17))&&(a25==1))&&(a14==20))){ a26 = 18; a14 = 18; a4 = 18; a7 = 1; return 21; } else if(((((((((a25==1)&&((input==6)&&((a26==17)||(a26==18))))&&(a28==16))&&(a4==16))&&(a7==1))&&(a1==1))&&!(a3==1))&&(a14==19))){ a3 = 1; a14 = 18; a26 = 17; a28 = 15; return -1; } else if((((a28==16)&&(!(a3==1)&&((a25==1)&&(((input==4)&&(((((a26==19)&&!(a7==1))&&(a14==19))||(((a7==1)&&(a26==17))&&(a14==20)))||(((a7==1)&&(a26==18))&&(a14==20))))&&(a1==1)))))&&(a4==16))){ a14 = 18; a28 = 15; a3 = 1; a26 = 17; a7 = 1; return -1; } else if((((a7==1)&&((((a25==1)&&((a14==20)&&((a1==1)&&((((a26==17)||(a26==18))||(a26==19))&&(input==4)))))&&(a28==15))&&(a4==18)))&&!(a3==1))){ a4 = 16; a3 = 1; a14 = 18; a26 = 17; return -1; } else if((!(a3==1)&&(((((a4==18)&&((input==3)&&((((a26==19)&&!(a7==1))&&(a14==18))||((a14==19)&&((a26==17)&&(a7==1))))))&&(a1==1))&&(a25==1))&&(a28==16)))){ a3 = 1; a14 = 18; a26 = 17; a28 = 15; a7 = 1; a4 = 16; return -1; } else if((((a28==15)&&(((a3==1)&&((((a14==18)&&((input==6)&&((a26==19)||((a26==17)||(a26==18)))))&&!(a7==1))&&(a4==18)))&&(a1==1)))&&(a25==1))){ a7 = 1; a26 = 19; a28 = 17; a14 = 19; return 26; } else if((((a25==1)&&(((((((a26==18)&&(input==1))&&(a4==18))&&(a14==20))&&(a1==1))&&(a3==1))&&(a28==17)))&&!(a7==1))){ a14 = 18; a7 = 1; a28 = 15; a26 = 17; a4 = 16; return -1; } else if(((a4==18)&&((((((a7==1)&&(!(a3==1)&&((input==3)&&(a14==19))))&&(a25==1))&&(a28==16))&&(a1==1))&&(a26==18)))){ a14 = 20; return 21; } else if(((!(a7==1)&&(((a14==18)&&((a28==15)&&((((input==5)&&(a26==18))&&(a25==1))&&!(a3==1))))&&(a4==18)))&&(a1==1))){ a7 = 1; a14 = 19; a26 = 19; return 24; } else if(((a26==19)&&((a28==15)&&(((a4==16)&&((a1==1)&&((a25==1)&&(((input==6)&&(a14==18))&&!(a3==1)))))&&(a7==1))))){ a26 = 17; a3 = 1; return -1; } else if((((a4==16)&&((!(a3==1)&&(((((input==3)&&(a26==17))&&(a14==19))&&(a25==1))&&(a28==17)))&&(a1==1)))&&!(a7==1))){ a14 = 18; a28 = 15; a3 = 1; a7 = 1; return -1; } else if(((a4==17)&&((a1==1)&&(((a14==19)&&((((a28==16)&&((((a26==17)||(a26==18))||(a26==19))&&(input==3)))&&(a25==1))&&!(a3==1)))&&(a7==1))))){ a4 = 16; a26 = 17; a14 = 18; a3 = 1; a28 = 15; return -1; } else if((((a3==1)&&(((a4==17)&&((a1==1)&&(((((a26==19)&&(a7==1))||(!(a7==1)&&(a26==17)))&&(input==2))&&(a28==17))))&&(a25==1)))&&(a14==18))){ a26 = 17; a28 = 15; a4 = 16; a7 = 1; return -1; } else if((((a7==1)&&((a14==19)&&((((a28==15)&&(!(a3==1)&&((input==6)&&((a26==17)||(a26==18)))))&&(a4==16))&&(a1==1))))&&(a25==1))){ a3 = 1; a26 = 17; a14 = 18; return -1; } else if((((a28==15)&&((((!(a3==1)&&((((a26==19)&&(a7==1))||(!(a7==1)&&(a26==17)))&&(input==3)))&&(a25==1))&&(a1==1))&&(a14==18)))&&(a4==18))){ a26 = 17; a3 = 1; a4 = 16; a7 = 1; return -1; } else if(((((a28==16)&&(((a1==1)&&(((((a14==19)&&(!(a7==1)&&(a26==19)))||((a14==20)&&((a7==1)&&(a26==17))))||((a14==20)&&((a7==1)&&(a26==18))))&&(input==1)))&&(a4==18)))&&(a25==1))&&!(a3==1))){ a26 = 17; a14 = 20; a7 = 1; return -1; } else if((!(a7==1)&&(((((!(a3==1)&&((a14==19)&&(((a26==18)||(a26==19))&&(input==2))))&&(a1==1))&&(a28==15))&&(a4==18))&&(a25==1)))){ a26 = 17; a7 = 1; a3 = 1; a4 = 16; a14 = 18; return -1; } else if(((((((input==1)&&((((((a26==18)&&(a28==15))&&!(a7==1))&&(a14==20))||((((a28==15)&&(a26==19))&&!(a7==1))&&(a14==20)))||((a14==18)&&((a7==1)&&((a28==16)&&(a26==17))))))&&(a25==1))&&(a3==1))&&(a4==18))&&(a1==1))){ a4 = 16; a14 = 18; a7 = 1; a28 = 15; a26 = 17; return -1; } else if((((((a14==18)&&(((a25==1)&&((((a26==17)||(a26==18))&&(input==2))&&(a1==1)))&&(a28==17)))&&(a7==1))&&!(a3==1))&&(a4==17))){ a14 = 19; a4 = 18; a26 = 19; a3 = 1; return 26; } else if((((a25==1)&&(((a1==1)&&((input==1)&&((((!(a7==1)&&((a26==18)&&(a28==16)))&&(a14==20))||((!(a7==1)&&((a26==19)&&(a28==16)))&&(a14==20)))||((a14==18)&&((a7==1)&&((a26==17)&&(a28==17)))))))&&(a4==16)))&&!(a3==1))){ a7 = 1; a14 = 18; a28 = 15; a3 = 1; a26 = 17; return -1; } else if(((a1==1)&&(((((a4==17)&&((a28==16)&&((((a26==17)&&!(a7==1))||(((a26==18)&&(a7==1))||((a7==1)&&(a26==19))))&&(input==4))))&&(a14==18))&&(a25==1))&&!(a3==1)))){ a26 = 17; a7 = 1; a3 = 1; a28 = 15; a4 = 16; return -1; } else if((((((a14==19)&&(((((input==5)&&(a26==18))&&(a1==1))&&(a25==1))&&(a28==15)))&&!(a3==1))&&(a7==1))&&(a4==18))){ a28 = 17; a3 = 1; a26 = 17; return 26; } else if(((a25==1)&&((a14==18)&&((a1==1)&&((a7==1)&&(((a28==16)&&((a4==18)&&(((a26==17)||(a26==18))&&(input==4))))&&!(a3==1))))))){ a4 = 16; a26 = 17; a3 = 1; a28 = 15; return -1; } else if(((((a7==1)&&((a4==18)&&(((!(a3==1)&&(((a26==17)||(a26==18))&&(input==2)))&&(a28==15))&&(a14==18))))&&(a25==1))&&(a1==1))){ a3 = 1; a4 = 16; a26 = 17; return -1; } else if(((((a3==1)&&((a14==18)&&((a26==18)&&((a4==18)&&((a28==17)&&((input==5)&&(a1==1)))))))&&(a25==1))&&!(a7==1))){ a7 = 1; a28 = 16; a4 = 16; a26 = 19; a3 = 0; return 22; } else if((((a25==1)&&((a1==1)&&((a28==15)&&(!(a3==1)&&((a4==18)&&((a14==19)&&((input==4)&&((a26==18)||(a26==19)))))))))&&!(a7==1))){ a26 = 17; a4 = 16; a7 = 1; a3 = 1; a14 = 18; return -1; } else if(((!(a7==1)&&((a25==1)&&((a4==16)&&((a14==20)&&((a28==15)&&(!(a3==1)&&((input==1)&&((a26==17)||(a26==18)))))))))&&(a1==1))){ a4 = 18; a28 = 17; a26 = 19; a3 = 1; a14 = 18; return -1; } else if(((a25==1)&&((a4==17)&&((a7==1)&&((((a28==15)&&(((a26==19)&&(input==4))&&(a3==1)))&&(a1==1))&&(a14==20)))))){ a4 = 16; a26 = 17; a14 = 18; return -1; } else if(((a28==16)&&((a3==1)&&((a1==1)&&((a25==1)&&(((((!(a7==1)&&(a26==17))||(((a7==1)&&(a26==18))||((a7==1)&&(a26==19))))&&(input==4))&&(a4==17))&&(a14==20))))))){ a14 = 18; a7 = 1; a4 = 16; a28 = 15; a26 = 17; return -1; } else if(((a14==19)&&(((((a28==16)&&((a25==1)&&((((a26==17)&&!(a7==1))||(((a7==1)&&(a26==18))||((a7==1)&&(a26==19))))&&(input==1))))&&(a1==1))&&(a3==1))&&(a4==18)))){ a14 = 20; a28 = 15; a26 = 19; a7 = 1; a4 = 16; a3 = 0; return 26; } else if(((a14==18)&&(!(a3==1)&&((a1==1)&&(((a28==17)&&((a4==17)&&(((!(a7==1)&&(a26==18))||(((a26==19)&&(a7==1))||(!(a7==1)&&(a26==17))))&&(input==4))))&&(a25==1)))))){ a4 = 16; a7 = 1; a3 = 1; a28 = 15; a26 = 17; return -1; } else if(((a28==15)&&(((((a25==1)&&((a14==18)&&((a4==18)&&((input==3)&&((a26==17)||(a26==18))))))&&!(a3==1))&&(a7==1))&&(a1==1)))){ a26 = 17; a4 = 16; a3 = 1; return -1; } else if((((a1==1)&&(((((a4==17)&&((input==1)&&((((a26==18)&&(a7==1))||((a26==19)&&(a7==1)))||((a26==17)&&!(a7==1)))))&&!(a3==1))&&(a14==18))&&(a25==1)))&&(a28==16))){ a3 = 1; a4 = 16; a7 = 1; a26 = 17; a28 = 15; return -1; } else if(((a28==15)&&(!(a7==1)&&((a25==1)&&(!(a3==1)&&((a1==1)&&((a26==17)&&(((input==5)&&(a4==17))&&(a14==20))))))))){ return -1; } else if(((a25==1)&&((a4==18)&&(((a28==15)&&(!(a3==1)&&((((a14==18)&&(!(a7==1)&&(a26==19)))||(((a7==1)&&(a26==17))&&(a14==19)))&&(input==1))))&&(a1==1))))){ a4 = 16; a26 = 17; a7 = 1; a14 = 18; a3 = 1; return -1; } else if(((((a26==18)&&(((a4==17)&&((!(a7==1)&&((input==2)&&(a28==15)))&&(a25==1)))&&(a1==1)))&&!(a3==1))&&(a14==19))){ a4 = 16; a3 = 1; a14 = 18; a7 = 1; a26 = 17; return -1; } else if(((((!(a3==1)&&((a14==20)&&((a4==16)&&((((a26==19)&&(a7==1))||(!(a7==1)&&(a26==17)))&&(input==2)))))&&(a25==1))&&(a1==1))&&(a28==16))){ a14 = 18; a3 = 1; a7 = 1; a28 = 15; a26 = 17; return -1; } else if(((((((a4==16)&&((((input==2)&&((a26==17)||(a26==18)))&&(a25==1))&&!(a7==1)))&&(a14==19))&&(a28==15))&&(a1==1))&&!(a3==1))){ a14 = 18; a7 = 1; a26 = 17; a3 = 1; return -1; } else if(((a28==15)&&((a25==1)&&(!(a3==1)&&((a4==17)&&(((input==2)&&(((a14==19)&&((a26==18)&&(a7==1)))||((((a26==19)&&!(a7==1))&&(a14==18))||(((a7==1)&&(a26==17))&&(a14==19)))))&&(a1==1))))))){ a3 = 1; a14 = 18; a26 = 17; a4 = 16; a7 = 1; return -1; } else if((((a25==1)&&((a14==18)&&(((a28==17)&&((a1==1)&&((((a26==19)&&(a7==1))||(!(a7==1)&&(a26==17)))&&(input==5))))&&(a3==1))))&&(a4==17))){ a26 = 19; a28 = 16; a4 = 18; a7 = 0; return 22; } else if((((a4==17)&&(((a28==17)&&(((a1==1)&&((a25==1)&&((input==5)&&!(a7==1))))&&(a14==19)))&&!(a3==1)))&&(a26==18))){ a14 = 18; a7 = 1; a28 = 15; a4 = 16; a3 = 1; a26 = 17; return -1; } else if(((a14==19)&&(((a7==1)&&((((a26==18)&&((a1==1)&&((input==2)&&(a28==15))))&&(a25==1))&&(a4==18)))&&!(a3==1)))){ a14 = 20; a28 = 16; a3 = 1; a26 = 17; return 26; } else if((((a14==19)&&(!(a3==1)&&((((a1==1)&&((input==1)&&(((a26==19)&&(a7==1))||((a26==17)&&!(a7==1)))))&&(a25==1))&&(a4==18))))&&(a28==15))){ a7 = 1; a4 = 16; a26 = 17; a3 = 1; a14 = 18; return -1; } else if(((a4==17)&&(!(a3==1)&&((((a25==1)&&((((!(a7==1)&&(a26==17))||(((a7==1)&&(a26==18))||((a7==1)&&(a26==19))))&&(input==2))&&(a28==16)))&&(a1==1))&&(a14==18))))){ a26 = 17; a4 = 16; a28 = 15; a7 = 1; a3 = 1; return -1; } else if(((a7==1)&&((!(a3==1)&&((((((a14==18)&&(input==2))&&(a25==1))&&(a1==1))&&(a4==16))&&(a26==19)))&&(a28==17)))){ a26 = 17; a3 = 1; a28 = 15; return -1; } else if((((((a1==1)&&(((a28==16)&&((((a26==19)&&(a7==1))||((a26==17)&&!(a7==1)))&&(input==3)))&&(a4==18)))&&(a14==20))&&!(a3==1))&&(a25==1))){ a4 = 16; a3 = 1; a7 = 0; a26 = 17; a14 = 19; return -1; } else if(((a28==16)&&(((a4==17)&&(!(a3==1)&&((((a25==1)&&((input==4)&&((a26==19)||((a26==17)||(a26==18)))))&&(a1==1))&&(a14==19))))&&(a7==1)))){ a4 = 16; a3 = 1; a26 = 17; a28 = 15; a14 = 18; return -1; } else if((((a4==17)&&((a14==19)&&((a25==1)&&((((a1==1)&&((input==3)&&(a28==17)))&&!(a3==1))&&(a26==18)))))&&!(a7==1))){ a14 = 18; a7 = 1; a26 = 17; a3 = 1; a4 = 16; a28 = 15; return -1; } else if(((a4==18)&&((a25==1)&&(((a1==1)&&((input==3)&&((((!(a7==1)&&((a26==18)&&(a28==15)))&&(a14==20))||((a14==20)&&(!(a7==1)&&((a26==19)&&(a28==15)))))||((((a26==17)&&(a28==16))&&(a7==1))&&(a14==18)))))&&(a3==1))))){ a7 = 1; a26 = 17; a28 = 15; a4 = 16; a14 = 18; return -1; } else if(((a3==1)&&((a25==1)&&(((a1==1)&&((a28==17)&&((((a14==19)&&((a26==19)&&!(a7==1)))||((a14==20)&&((a7==1)&&(a26==17))))&&(input==4))))&&(a4==18))))){ a14 = 18; a4 = 16; a28 = 15; a26 = 17; a7 = 1; return -1; } else if(((a3==1)&&((a25==1)&&(((input==3)&&(((a14==20)&&((((a4==17)&&(a26==19))&&(a28==17))&&!(a7==1)))||(((((a26==17)&&(a4==18))&&(a28==15))&&(a7==1))&&(a14==18))))&&(a1==1))))){ a28 = 15; a26 = 17; a7 = 1; a14 = 18; a4 = 16; return -1; } else if((((a25==1)&&(((a1==1)&&((a4==17)&&((((((a26==19)&&(a7==1))||((a26==17)&&!(a7==1)))||(!(a7==1)&&(a26==18)))&&(input==4))&&(a14==20))))&&(a3==1)))&&(a28==17))){ a7 = 0; a14 = 18; a26 = 17; a4 = 18; return 26; } else if(((((((a1==1)&&((input==6)&&(((a14==19)&&((a7==1)&&(a26==18)))||(((!(a7==1)&&(a26==19))&&(a14==18))||((a14==19)&&((a26==17)&&(a7==1)))))))&&!(a3==1))&&(a25==1))&&(a28==17))&&(a4==18))){ a7 = 0; a14 = 18; a26 = 17; a4 = 17; a28 = 15; return 24; } else if(((a4==16)&&((!(a3==1)&&((a1==1)&&(!(a7==1)&&((((a26==17)&&(input==6))&&(a28==17))&&(a14==18)))))&&(a25==1)))){ a28 = 15; a3 = 1; a7 = 1; return -1; } else if((((((a1==1)&&((a28==17)&&((a25==1)&&(((input==3)&&(a14==20))&&(a26==18)))))&&(a3==1))&&!(a7==1))&&(a4==18))){ a28 = 16; a7 = 1; a4 = 16; a3 = 0; a14 = 19; return 22; } else if(((a1==1)&&((a4==18)&&((a14==20)&&((a28==16)&&((!(a7==1)&&(!(a3==1)&&(((a26==18)||(a26==19))&&(input==6))))&&(a25==1))))))){ a3 = 1; a26 = 19; a4 = 16; a14 = 18; a7 = 1; return -1; } else if(((!(a3==1)&&(((a1==1)&&(((((input==3)&&((a26==17)||(a26==18)))&&(a7==1))&&(a14==18))&&(a28==16)))&&(a25==1)))&&(a4==18))){ a14 = 19; a26 = 17; return 24; } else if((((a1==1)&&((a28==15)&&(((a3==1)&&(((((a14==19)&&((a26==19)&&!(a7==1)))||(((a26==17)&&(a7==1))&&(a14==20)))||((a14==20)&&((a7==1)&&(a26==18))))&&(input==2)))&&(a25==1))))&&(a4==18))){ a26 = 17; a14 = 18; a7 = 1; a4 = 16; return -1; } else if(((a1==1)&&(((a4==17)&&((a25==1)&&((input==3)&&(((a14==18)&&(((a28==16)&&(a26==17))&&(a7==1)))||(((a14==20)&&(((a26==18)&&(a28==15))&&!(a7==1)))||((((a28==15)&&(a26==19))&&!(a7==1))&&(a14==20)))))))&&!(a3==1)))){ a14 = 18; a4 = 16; a7 = 1; a26 = 17; a3 = 1; a28 = 15; return -1; } else if((!(a7==1)&&((a25==1)&&(!(a3==1)&&(((a14==18)&&(((a1==1)&&(((a26==18)||(a26==19))&&(input==3)))&&(a28==16)))&&(a4==16)))))){ a28 = 15; a26 = 18; a14 = 20; return 26; } else if((!(a3==1)&&(((a1==1)&&((a25==1)&&(((((a14==18)&&((a26==19)&&!(a7==1)))||(((a7==1)&&(a26==17))&&(a14==19)))&&(input==4))&&(a28==17))))&&(a4==16)))){ a7 = 1; a14 = 18; a3 = 1; a26 = 17; a28 = 15; return -1; } else if((((a1==1)&&((a28==15)&&((a14==19)&&((a4==18)&&(((input==6)&&(((a26==19)&&(a7==1))||(!(a7==1)&&(a26==17))))&&!(a3==1))))))&&(a25==1))){ a14 = 18; a3 = 1; a7 = 1; a26 = 17; a4 = 16; return -1; } else if(((a28==15)&&((a14==19)&&(((((a26==18)&&((a1==1)&&((a25==1)&&(input==1))))&&(a3==1))&&(a7==1))&&(a4==18))))){ a14 = 18; a4 = 16; a26 = 17; return -1; } else if((((a3==1)&&((((a1==1)&&((input==6)&&((((a7==1)&&(a26==17))&&(a14==19))||(((!(a7==1)&&(a26==18))&&(a14==18))||((!(a7==1)&&(a26==19))&&(a14==18))))))&&(a25==1))&&(a28==17)))&&(a4==17))){ a14 = 19; a28 = 16; a4 = 18; a26 = 17; a7 = 1; return 26; } else if((((a1==1)&&((a25==1)&&((a4==18)&&(((input==6)&&(((a14==20)&&((a26==18)&&(a7==1)))||((((a26==19)&&!(a7==1))&&(a14==19))||(((a26==17)&&(a7==1))&&(a14==20)))))&&(a28==16)))))&&!(a3==1))){ a26 = 17; a4 = 17; a7 = 0; a14 = 18; a28 = 15; return 21; } else if(((((a25==1)&&((a7==1)&&((((a1==1)&&((a4==18)&&(input==4)))&&(a3==1))&&(a26==19))))&&(a14==20))&&(a28==15))){ a14 = 18; a4 = 16; a26 = 17; return -1; } else if(((a28==15)&&((a14==20)&&((((a7==1)&&((((input==4)&&(a1==1))&&(a25==1))&&!(a3==1)))&&(a26==19))&&(a4==16))))){ a3 = 1; a26 = 17; a14 = 18; return -1; } else if((((a3==1)&&((a4==17)&&((((((input==1)&&(a7==1))&&(a1==1))&&(a26==19))&&(a25==1))&&(a14==20))))&&(a28==15))){ a4 = 16; a14 = 18; a26 = 17; return -1; } else if((((a25==1)&&(!(a3==1)&&((a1==1)&&(((((a14==18)&&(!(a7==1)&&(a26==19)))||(((a7==1)&&(a26==17))&&(a14==19)))&&(input==2))&&(a4==18)))))&&(a28==15))){ a3 = 1; a14 = 18; a26 = 17; a7 = 1; a4 = 16; return -1; } else if((((a4==16)&&((a25==1)&&(((a1==1)&&((((a14==18)&&(!(a7==1)&&(a26==19)))||(((a26==17)&&(a7==1))&&(a14==19)))&&(input==3)))&&!(a3==1))))&&(a28==17))){ a26 = 17; a14 = 18; a3 = 1; a7 = 1; a28 = 15; return -1; } else if(((a25==1)&&((a1==1)&&((a14==20)&&(!(a3==1)&&((a4==17)&&((a7==1)&&(((a28==16)&&(input==3))&&(a26==17))))))))){ a28 = 15; a3 = 1; a4 = 16; a14 = 18; return -1; } else if(((a4==18)&&(((a28==15)&&(((a7==1)&&((((input==4)&&((a26==17)||(a26==18)))&&(a14==18))&&(a1==1)))&&(a25==1)))&&!(a3==1)))){ a4 = 16; a26 = 17; a3 = 1; return -1; } else if(((a14==20)&&(((((a7==1)&&((((input==6)&&((a26==17)||(a26==18)))&&(a28==15))&&(a25==1)))&&!(a3==1))&&(a1==1))&&(a4==16)))){ a3 = 1; a14 = 18; a26 = 17; return -1; } else if(((a14==19)&&(!(a3==1)&&(((((a1==1)&&((((a26==19)&&(a7==1))||(!(a7==1)&&(a26==17)))&&(input==5)))&&(a28==15))&&(a25==1))&&(a4==17))))){ a7 = 1; a14 = 18; a4 = 16; a3 = 1; a26 = 17; return -1; } else if(((a25==1)&&(!(a3==1)&&(((((a14==20)&&((((a26==19)||((a26==17)||(a26==18)))&&(input==4))&&(a1==1)))&&(a7==1))&&(a28==15))&&(a4==17))))){ a14 = 18; a3 = 1; a4 = 16; a26 = 17; return -1; } else if(((a1==1)&&(((a3==1)&&(((a4==18)&&(((((a26==17)&&!(a7==1))||(((a26==18)&&(a7==1))||((a26==19)&&(a7==1))))&&(input==5))&&(a25==1)))&&(a28==17)))&&(a14==18)))){ a7 = 1; a4 = 16; a28 = 15; a26 = 17; return -1; } else if(((a28==17)&&(((((a4==17)&&((a3==1)&&(((input==1)&&(a1==1))&&(a25==1))))&&(a7==1))&&(a14==20))&&(a26==18)))){ a28 = 15; a4 = 16; a14 = 18; a26 = 17; return -1; } else if(((a28==17)&&(((a1==1)&&((a3==1)&&(((a25==1)&&(((!(a7==1)&&(a26==17))||(((a26==18)&&(a7==1))||((a7==1)&&(a26==19))))&&(input==5)))&&(a4==18))))&&(a14==19)))){ a14 = 18; a26 = 19; a7 = 0; return 24; } else if(((((a1==1)&&((a25==1)&&((((input==3)&&(((a26==19)&&(a7==1))||(!(a7==1)&&(a26==17))))&&(a14==18))&&(a28==16))))&&(a4==16))&&!(a3==1))){ a26 = 17; a7 = 1; a3 = 1; a28 = 15; return -1; } else if(((a28==15)&&((((a3==1)&&((((((!(a7==1)&&(a26==19))&&(a14==19))||((a14==20)&&((a7==1)&&(a26==17))))||(((a7==1)&&(a26==18))&&(a14==20)))&&(input==5))&&(a25==1)))&&(a4==18))&&(a1==1)))){ a7 = 1; a14 = 18; a4 = 16; a26 = 17; return -1; } else if(((((a25==1)&&(((input==4)&&(((a14==18)&&((a7==1)&&((a28==16)&&(a26==17))))||(((!(a7==1)&&((a26==18)&&(a28==15)))&&(a14==20))||((!(a7==1)&&((a28==15)&&(a26==19)))&&(a14==20)))))&&(a3==1)))&&(a4==17))&&(a1==1))){ a14 = 18; a26 = 17; a7 = 1; a4 = 16; a28 = 15; return -1; } else if((((a4==18)&&((((a26==18)&&((!(a7==1)&&((input==3)&&(a28==15)))&&!(a3==1)))&&(a14==18))&&(a25==1)))&&(a1==1))){ a26 = 17; a3 = 1; a4 = 16; a7 = 1; return -1; } else if((((((a4==17)&&((a14==19)&&(((((a26==19)&&(a7==1))||((a26==17)&&!(a7==1)))&&(input==4))&&!(a3==1))))&&(a1==1))&&(a25==1))&&(a28==17))){ a14 = 20; a7 = 0; a26 = 17; return 24; } else if((!(a3==1)&&((((a28==16)&&((((a1==1)&&((input==3)&&((a26==18)||(a26==19))))&&!(a7==1))&&(a14==20)))&&(a4==18))&&(a25==1)))){ a7 = 1; a4 = 16; a28 = 17; a26 = 18; a14 = 18; return 24; } else if(((a25==1)&&(((a1==1)&&((a3==1)&&((a28==17)&&((input==6)&&(((a14==19)&&((a26==19)&&!(a7==1)))||(((a7==1)&&(a26==17))&&(a14==20)))))))&&(a4==18)))){ a26 = 18; a14 = 19; a7 = 1; return 26; } else if((((((((!(a7==1)&&((a28==17)&&(((a4==18)&&(a3==1))&&(a26==19))))&&(a14==20))||((a14==18)&&((a7==1)&&(((!(a3==1)&&(a4==16))&&(a26==17))&&(a28==15)))))||(((a7==1)&&((a28==15)&&(((a4==16)&&!(a3==1))&&(a26==18))))&&(a14==18)))&&(input==1))&&(a25==1))&&(a1==1))){ a4 = 16; a14 = 19; a26 = 19; a3 = 0; a7 = 1; a28 = 16; return 26; } else if(((a1==1)&&((a25==1)&&(((a4==17)&&((a28==16)&&(((input==2)&&((((a7==1)&&(a26==18))||((a7==1)&&(a26==19)))||(!(a7==1)&&(a26==17))))&&(a3==1))))&&(a14==19))))){ a14 = 18; a26 = 17; a7 = 1; a28 = 15; a4 = 16; return -1; } else if(((a28==16)&&(((a14==20)&&((!(a3==1)&&(((a1==1)&&((a7==1)&&(input==1)))&&(a26==17)))&&(a4==17)))&&(a25==1)))){ a14 = 18; a4 = 16; a3 = 1; a28 = 15; return -1; } else if((!(a7==1)&&((((((a14==20)&&((a28==15)&&((input==1)&&(a3==1))))&&(a26==17))&&(a25==1))&&(a1==1))&&(a4==18)))){ a7 = 1; a4 = 16; a14 = 18; return -1; } else if((!(a3==1)&&((a14==19)&&(((a4==16)&&(((a25==1)&&(((input==2)&&((a26==17)||(a26==18)))&&(a28==16)))&&(a7==1)))&&(a1==1))))){ a26 = 17; a3 = 1; a14 = 18; a28 = 15; return -1; } else if(((((a4==18)&&((((((((a26==18)&&(a7==1))||((a7==1)&&(a26==19)))||((a26==17)&&!(a7==1)))&&(input==5))&&(a28==17))&&(a1==1))&&(a25==1)))&&(a3==1))&&(a14==20))){ a26 = 17; a14 = 18; a7 = 1; a4 = 16; a28 = 15; return -1; } else if((((a14==20)&&((a1==1)&&((a4==16)&&(((a28==17)&&((input==2)&&(((a7==1)&&(a26==19))||(!(a7==1)&&(a26==17)))))&&!(a3==1)))))&&(a25==1))){ a7 = 1; a26 = 17; a14 = 18; a28 = 15; a3 = 1; return -1; } else if(((((a28==15)&&(((a4==18)&&(((a26==19)&&((input==5)&&(a14==20)))&&(a1==1)))&&(a3==1)))&&(a25==1))&&(a7==1))){ a3 = 0; a14 = 18; a4 = 16; return 26; } else if(((((a28==15)&&(((a4==18)&&(((((a26==19)&&(a7==1))||(!(a7==1)&&(a26==17)))&&(input==3))&&(a25==1)))&&(a1==1)))&&!(a3==1))&&(a14==19))){ a3 = 1; a14 = 18; a4 = 16; a7 = 1; a26 = 17; return -1; } else if(((a1==1)&&((a25==1)&&(((((a7==1)&&(((a14==20)&&(input==2))&&(a26==19)))&&(a4==16))&&!(a3==1))&&(a28==15))))){ a14 = 18; a26 = 17; a3 = 1; return -1; } else if(((a4==16)&&((!(a3==1)&&(((input==2)&&(((!(a7==1)&&((a26==19)&&(a28==15)))&&(a14==20))||(((a7==1)&&((a28==16)&&(a26==17)))&&(a14==18))))&&(a1==1)))&&(a25==1)))){ a14 = 19; a7 = 0; a28 = 17; a26 = 17; return 26; } else if((((a1==1)&&((!(a3==1)&&((a14==19)&&((a28==16)&&((a26==19)&&((input==2)&&!(a7==1))))))&&(a25==1)))&&(a4==17))){ a26 = 17; a28 = 15; a4 = 16; a7 = 1; a3 = 1; a14 = 18; return -1; } else if((((a1==1)&&(((input==4)&&((((((a4==17)&&(a26==19))&&(a28==17))&&!(a7==1))&&(a14==20))||(((a7==1)&&((a28==15)&&((a26==17)&&(a4==18))))&&(a14==18))))&&(a3==1)))&&(a25==1))){ a14 = 18; a28 = 15; a4 = 16; a7 = 1; a26 = 17; return -1; } else if(((a14==19)&&((a1==1)&&((a3==1)&&((a4==17)&&(((a25==1)&&((((a26==17)&&!(a7==1))||(((a26==18)&&(a7==1))||((a26==19)&&(a7==1))))&&(input==4)))&&(a28==16))))))){ a4 = 16; a26 = 17; a7 = 1; a28 = 15; a14 = 18; return -1; } else if(((!(a3==1)&&(((((!(a7==1)&&((input==1)&&(a4==17)))&&(a25==1))&&(a26==18))&&(a1==1))&&(a14==19)))&&(a28==17))){ a7 = 1; a4 = 18; a14 = 18; a28 = 15; return 24; } else if(((((((((((a26==17)&&!(a7==1))||(((a7==1)&&(a26==18))||((a7==1)&&(a26==19))))&&(input==1))&&(a4==17))&&(a14==18))&&(a25==1))&&(a1==1))&&(a3==1))&&(a28==16))){ a26 = 17; a28 = 15; a7 = 1; a4 = 16; return -1; } else if(((((((a14==18)&&((a28==16)&&((((a26==19)&&(a7==1))||((a26==17)&&!(a7==1)))&&(input==6))))&&(a25==1))&&(a1==1))&&(a4==16))&&!(a3==1))){ a28 = 15; a7 = 1; a3 = 1; a26 = 17; return -1; } else if(((a4==16)&&(((a7==1)&&((!(a3==1)&&(((a14==18)&&((a26==19)&&(input==4)))&&(a28==17)))&&(a25==1)))&&(a1==1)))){ a3 = 1; a26 = 17; a28 = 15; return -1; } else if(((a28==16)&&(((a4==17)&&((((input==6)&&((((a7==1)&&(a26==17))&&(a14==20))||((((a26==18)&&!(a7==1))&&(a14==19))||((!(a7==1)&&(a26==19))&&(a14==19)))))&&(a25==1))&&(a3==1)))&&(a1==1)))){ a7 = 1; a14 = 18; a28 = 15; a4 = 16; a26 = 17; return -1; } else if(((a1==1)&&((!(a7==1)&&(((((((a26==18)||(a26==19))&&(input==5))&&(a25==1))&&!(a3==1))&&(a28==16))&&(a14==20)))&&(a4==18)))){ a26 = 17; a28 = 15; a4 = 17; return 24; } else if((((!(a3==1)&&((a28==15)&&(((input==1)&&(((a14==19)&&((a26==18)&&(a7==1)))||(((a14==18)&&(!(a7==1)&&(a26==19)))||(((a7==1)&&(a26==17))&&(a14==19)))))&&(a4==17))))&&(a1==1))&&(a25==1))){ a4 = 16; a14 = 18; a3 = 1; a7 = 1; a26 = 17; return -1; } else if(((a25==1)&&((a1==1)&&(!(a3==1)&&(((input==4)&&(((!(a7==1)&&((a26==19)&&(a28==15)))&&(a14==20))||(((a7==1)&&((a28==16)&&(a26==17)))&&(a14==18))))&&(a4==16)))))){ a3 = 1; a26 = 17; a7 = 1; a28 = 15; a14 = 18; return -1; } else if(((((((!(a3==1)&&(((input==1)&&(a25==1))&&(a28==15)))&&(a14==20))&&(a1==1))&&(a4==17))&&(a26==17))&&!(a7==1))){ a7 = 1; a26 = 19; return -1; } else if((((!(a3==1)&&((a14==20)&&((a4==17)&&(((a1==1)&&(((a26==18)||(a26==19))&&(input==1)))&&(a28==16)))))&&!(a7==1))&&(a25==1))){ a26 = 17; return -1; } else if((((a4==16)&&(((((a28==15)&&((a14==19)&&(((a26==17)||(a26==18))&&(input==1))))&&!(a3==1))&&!(a7==1))&&(a1==1)))&&(a25==1))){ a3 = 1; a26 = 17; a7 = 1; a14 = 18; return -1; } else if(((!(a7==1)&&((a25==1)&&((a1==1)&&((a3==1)&&((a4==18)&&(((input==4)&&((a26==18)||(a26==19)))&&(a28==16)))))))&&(a14==19))){ a7 = 1; a28 = 15; a26 = 17; a14 = 18; a4 = 16; return -1; } else if(((a28==15)&&((((a7==1)&&((a4==17)&&(((a25==1)&&(((a26==18)||(a26==19))&&(input==1)))&&(a1==1))))&&!(a3==1))&&(a14==18)))){ a26 = 18; return 23; } else if(((a26==19)&&((a28==16)&&((!(a7==1)&&((a3==1)&&(((a25==1)&&((input==4)&&(a4==18)))&&(a1==1))))&&(a14==18))))){ a7 = 1; a4 = 16; a26 = 17; a28 = 15; return -1; } else if(((((a25==1)&&((a28==17)&&(!(a3==1)&&(((((a14==19)&&((a26==19)&&!(a7==1)))||((a14==20)&&((a26==17)&&(a7==1))))||((a14==20)&&((a7==1)&&(a26==18))))&&(input==3)))))&&(a1==1))&&(a4==16))){ a7 = 1; a26 = 17; a3 = 1; a14 = 18; a28 = 15; return -1; } else if(((((((a25==1)&&((!(a7==1)&&((input==1)&&(a28==15)))&&(a1==1)))&&(a4==17))&&!(a3==1))&&(a14==19))&&(a26==19))){ a3 = 1; a7 = 1; a4 = 16; a14 = 18; a26 = 17; return -1; } else if(((((a1==1)&&((a28==15)&&((a4==17)&&((input==6)&&(((((a26==19)&&!(a7==1))&&(a14==18))||((a14==19)&&((a7==1)&&(a26==17))))||(((a7==1)&&(a26==18))&&(a14==19)))))))&&(a25==1))&&!(a3==1))){ a7 = 0; a28 = 16; a26 = 19; a14 = 19; return 22; } else if(((a14==18)&&((a28==17)&&((((a25==1)&&(!(a3==1)&&((a1==1)&&(((a26==17)||(a26==18))&&(input==4)))))&&(a4==18))&&(a7==1))))){ a14 = 19; a26 = 18; a28 = 15; a3 = 1; a4 = 16; return -1; } else if((!(a7==1)&&((a28==17)&&((a14==18)&&(((a1==1)&&((a26==18)&&(!(a3==1)&&((input==2)&&(a25==1)))))&&(a4==16)))))){ a28 = 15; a3 = 1; a26 = 17; a7 = 1; return -1; } else if(((!(a3==1)&&(((((((((a26==17)||(a26==18))||(a26==19))&&(input==4))&&!(a7==1))&&(a25==1))&&(a1==1))&&(a28==17))&&(a14==20)))&&(a4==17))){ a3 = 1; a4 = 16; a14 = 18; a28 = 15; a26 = 17; a7 = 1; return -1; } else if((((((((a4==17)&&(((input==5)&&(a25==1))&&(a1==1)))&&(a14==20))&&(a3==1))&&(a26==18))&&(a7==1))&&(a28==15))){ a4 = 16; a26 = 17; a14 = 18; return -1; } else if(((a4==16)&&(((a25==1)&&((a1==1)&&((input==5)&&(((a14==18)&&((a7==1)&&((a28==17)&&(a26==17))))||(((((a26==18)&&(a28==16))&&!(a7==1))&&(a14==20))||((a14==20)&&(((a26==19)&&(a28==16))&&!(a7==1))))))))&&!(a3==1)))){ a14 = 18; a26 = 17; a3 = 1; a28 = 15; a7 = 1; return -1; } else if(((a25==1)&&((a3==1)&&((((a4==17)&&(((((a26==17)&&!(a7==1))||(((a26==18)&&(a7==1))||((a26==19)&&(a7==1))))&&(input==6))&&(a28==16)))&&(a14==19))&&(a1==1))))){ a28 = 15; a7 = 1; a26 = 17; a4 = 16; a14 = 18; return -1; } else if(((((((a4==16)&&(!(a7==1)&&((a14==18)&&((input==5)&&(a1==1)))))&&!(a3==1))&&(a28==17))&&(a25==1))&&(a26==18))){ a28 = 15; a7 = 1; a3 = 1; a26 = 17; return -1; } else if((((((((a28==15)&&(((input==3)&&((a26==18)||(a26==19)))&&(a25==1)))&&!(a3==1))&&!(a7==1))&&(a4==18))&&(a1==1))&&(a14==20))){ a7 = 1; a3 = 1; a4 = 16; a14 = 18; a26 = 17; return -1; } else if(((a14==19)&&(((a1==1)&&((((a4==18)&&((input==6)&&(((a26==17)&&!(a7==1))||(((a26==18)&&(a7==1))||((a7==1)&&(a26==19))))))&&(a3==1))&&(a28==17)))&&(a25==1)))){ a26 = 17; a7 = 0; return 22; } else if(((a4==18)&&(((((((((a26==19)&&(a7==1))||(!(a7==1)&&(a26==17)))&&(input==2))&&(a28==16))&&(a14==19))&&(a25==1))&&!(a3==1))&&(a1==1)))){ a26 = 17; a4 = 16; a7 = 1; a14 = 18; a28 = 15; a3 = 1; return -1; } else if(((a25==1)&&((((a1==1)&&((a14==18)&&(((input==5)&&((((a26==19)&&(a7==1))||(!(a7==1)&&(a26==17)))||((a26==18)&&!(a7==1))))&&(a4==17))))&&!(a3==1))&&(a28==17)))){ a3 = 1; a4 = 16; a7 = 1; a28 = 15; a26 = 17; return -1; } else if((((a25==1)&&((a7==1)&&(((((a14==18)&&(((a26==17)||(a26==18))&&(input==6)))&&(a4==17))&&!(a3==1))&&(a1==1))))&&(a28==17))){ a26 = 17; a4 = 18; a28 = 16; a14 = 20; a3 = 1; return 26; } else if(((a4==16)&&((!(a3==1)&&((a28==17)&&((a1==1)&&((input==5)&&(((a14==18)&&(!(a7==1)&&(a26==19)))||(((a26==17)&&(a7==1))&&(a14==19)))))))&&(a25==1)))){ a7 = 1; a28 = 15; a3 = 1; a26 = 17; a14 = 18; return -1; } else if(((a28==17)&&(((a26==18)&&(!(a7==1)&&((a4==18)&&((((a3==1)&&(input==4))&&(a25==1))&&(a1==1)))))&&(a14==19)))){ a7 = 1; a28 = 16; a26 = 17; a14 = 20; return 26; } else if(((a25==1)&&(((a28==16)&&((a3==1)&&(((a4==17)&&((input==3)&&((!(a7==1)&&(a26==17))||(((a7==1)&&(a26==18))||((a26==19)&&(a7==1))))))&&(a1==1))))&&(a14==19)))){ a4 = 16; a14 = 18; a26 = 17; a7 = 1; a28 = 15; return -1; } else if((((a25==1)&&(((a14==20)&&(((a28==15)&&(((input==4)&&((a26==18)||(a26==19)))&&(a4==18)))&&(a1==1)))&&!(a3==1)))&&!(a7==1))){ a14 = 18; a7 = 1; a3 = 1; a4 = 16; a26 = 17; return -1; } else if((!(a3==1)&&(((a14==19)&&((a4==17)&&(((a1==1)&&(!(a7==1)&&((a25==1)&&(input==2))))&&(a28==15))))&&(a26==19)))){ a7 = 1; a14 = 18; a3 = 1; a26 = 17; a4 = 16; return -1; } else if(((a1==1)&&(((((((a14==19)&&((a4==18)&&(input==6)))&&(a25==1))&&(a28==16))&&(a26==18))&&!(a3==1))&&!(a7==1)))){ a26 = 17; a28 = 15; a14 = 20; a3 = 1; a4 = 16; return -1; } else if(((a4==18)&&((a1==1)&&(((a14==20)&&(((((!(a7==1)&&(a26==17))||(((a26==18)&&(a7==1))||((a26==19)&&(a7==1))))&&(input==1))&&(a25==1))&&(a3==1)))&&(a28==17))))){ a14 = 18; a7 = 1; a26 = 17; a28 = 15; a4 = 16; return -1; } else if(((a26==19)&&(!(a7==1)&&((a4==17)&&((a1==1)&&((((a28==17)&&((input==1)&&!(a3==1)))&&(a25==1))&&(a14==19))))))){ a14 = 18; a26 = 17; a28 = 15; return 21; } else if(((a28==17)&&((((a25==1)&&(((input==2)&&((((a7==1)&&(a26==18))&&(a14==20))||(((a14==19)&&(!(a7==1)&&(a26==19)))||(((a7==1)&&(a26==17))&&(a14==20)))))&&(a4==16)))&&!(a3==1))&&(a1==1)))){ a4 = 17; a7 = 0; a14 = 18; a26 = 18; a28 = 16; return 22; } return calculate_output4(input); } int calculate_output4(int input) { if(((a25==1)&&((a28==17)&&((a14==18)&&(((((a26==17)&&((a4==16)&&(input==5)))&&!(a3==1))&&!(a7==1))&&(a1==1)))))){ a3 = 1; a7 = 1; a28 = 15; return -1; } else if(((a3==1)&&(((a1==1)&&((a28==16)&&(((a4==18)&&((input==1)&&((((a26==18)&&(a7==1))||((a26==19)&&(a7==1)))||(!(a7==1)&&(a26==17)))))&&(a14==18))))&&(a25==1)))){ a4 = 16; a26 = 17; a7 = 1; a28 = 15; return -1; } else if(((!(a7==1)&&(((a25==1)&&(((((input==2)&&(((a26==17)||(a26==18))||(a26==19)))&&(a1==1))&&!(a3==1))&&(a28==17)))&&(a4==17)))&&(a14==20))){ a26 = 17; a3 = 1; a4 = 16; a14 = 18; a28 = 15; a7 = 1; return -1; } else if(((a4==17)&&((a28==17)&&((a25==1)&&((a3==1)&&(((input==3)&&((((a14==19)&&(!(a7==1)&&(a26==18)))||(((a26==19)&&!(a7==1))&&(a14==19)))||(((a7==1)&&(a26==17))&&(a14==20))))&&(a1==1))))))){ a4 = 16; a7 = 1; a26 = 17; a28 = 15; a14 = 18; return -1; } else if(((a28==15)&&((a1==1)&&(((a25==1)&&(((a4==16)&&(((((a26==17)||(a26==18))||(a26==19))&&(input==5))&&!(a7==1)))&&!(a3==1)))&&(a14==18))))){ a26 = 17; a3 = 1; a7 = 1; return -1; } else if((((!(a7==1)&&((a4==17)&&((a14==19)&&((a1==1)&&((((a26==17)||(a26==18))&&(input==4))&&!(a3==1))))))&&(a28==16))&&(a25==1))){ a4 = 16; a26 = 18; a7 = 1; a28 = 17; return 26; } else if((!(a3==1)&&(((a14==20)&&((a25==1)&&((a1==1)&&(((input==4)&&(((a7==1)&&(a26==19))||(!(a7==1)&&(a26==17))))&&(a4==18)))))&&(a28==16)))){ a28 = 17; a26 = 18; a14 = 18; a7 = 1; return 24; } else if(((((a1==1)&&((((a14==19)&&((input==3)&&((((a7==1)&&(a26==19))||((a26==17)&&!(a7==1)))||((a26==18)&&!(a7==1)))))&&(a28==16))&&!(a3==1)))&&(a25==1))&&(a4==16))){ a28 = 15; a3 = 1; a26 = 17; a7 = 1; a14 = 18; return -1; } else if(((a3==1)&&((((a28==17)&&(((a14==18)&&((input==3)&&(((a26==17)&&!(a7==1))||(((a26==18)&&(a7==1))||((a7==1)&&(a26==19))))))&&(a1==1)))&&(a25==1))&&(a4==18)))){ a4 = 16; a28 = 15; a26 = 17; a7 = 1; return -1; } else if(((a28==16)&&(((a4==16)&&(((a25==1)&&((input==5)&&((((a7==1)&&(a26==18))&&(a14==20))||(((a14==19)&&(!(a7==1)&&(a26==19)))||((a14==20)&&((a26==17)&&(a7==1)))))))&&(a1==1)))&&!(a3==1)))){ a3 = 1; a14 = 18; a7 = 1; a28 = 15; a26 = 17; return -1; } else if(((a4==16)&&((((a14==20)&&(!(a3==1)&&((a28==17)&&((((a26==19)&&(a7==1))||((a26==17)&&!(a7==1)))&&(input==6)))))&&(a25==1))&&(a1==1)))){ a26 = 17; a3 = 1; a14 = 18; a7 = 1; a28 = 15; return -1; } else if(((((a14==19)&&((a1==1)&&((a28==16)&&(((((a7==1)&&(a26==19))||(!(a7==1)&&(a26==17)))&&(input==4))&&(a4==18)))))&&!(a3==1))&&(a25==1))){ a4 = 16; a26 = 17; a7 = 0; a3 = 1; a14 = 20; return -1; } else if(((a25==1)&&(((!(a3==1)&&((((a28==16)&&((input==6)&&(((a26==17)||(a26==18))||(a26==19))))&&(a1==1))&&(a4==17)))&&(a14==19))&&(a7==1)))){ a14 = 18; a7 = 0; a28 = 17; a26 = 19; return 26; } else if((((a7==1)&&((a25==1)&&(!(a3==1)&&((((((a26==17)||(a26==18))&&(input==5))&&(a28==16))&&(a14==18))&&(a1==1)))))&&(a4==18))){ a4 = 16; a28 = 15; a26 = 17; a3 = 1; return -1; } else if((((a4==17)&&(((((((((a26==19)&&(a7==1))||((a26==17)&&!(a7==1)))||(!(a7==1)&&(a26==18)))&&(input==1))&&(a25==1))&&(a1==1))&&(a14==18))&&!(a3==1)))&&(a28==17))){ a14 = 19; a7 = 0; a28 = 16; a26 = 18; return 24; } else if(((a28==16)&&(!(a7==1)&&((a26==19)&&((a25==1)&&(!(a3==1)&&((a14==19)&&(((input==4)&&(a1==1))&&(a4==17))))))))){ a26 = 18; a28 = 17; return 23; } else if((((a4==18)&&(((a28==16)&&((a25==1)&&((a14==18)&&((input==4)&&((((a7==1)&&(a26==19))||(!(a7==1)&&(a26==17)))||((a26==18)&&!(a7==1)))))))&&!(a3==1)))&&(a1==1))){ a7 = 1; a3 = 1; a26 = 17; a4 = 16; a28 = 15; return -1; } else if(((a28==15)&&(!(a3==1)&&((a1==1)&&((a4==18)&&(((((!(a7==1)&&(a26==19))&&(a14==18))||(((a7==1)&&(a26==17))&&(a14==19)))&&(input==4))&&(a25==1))))))){ a26 = 19; a14 = 19; a7 = 0; return 22; } else if((((a25==1)&&((a28==16)&&((a4==16)&&((a1==1)&&((input==2)&&(((a14==20)&&((a26==18)&&(a7==1)))||((((a26==19)&&!(a7==1))&&(a14==19))||((a14==20)&&((a26==17)&&(a7==1))))))))))&&!(a3==1))){ a14 = 18; a7 = 1; a28 = 15; a26 = 17; a3 = 1; return -1; } else if(((a4==18)&&(!(a7==1)&&(((a26==18)&&(((((a3==1)&&(input==2))&&(a28==17))&&(a1==1))&&(a14==19)))&&(a25==1))))){ a26 = 17; a4 = 16; a28 = 15; a14 = 18; a7 = 1; return -1; } else if((((a14==20)&&(((a3==1)&&(!(a7==1)&&((a25==1)&&(((input==6)&&((a26==18)||(a26==19)))&&(a28==16)))))&&(a4==17)))&&(a1==1))){ a28 = 15; a14 = 18; a26 = 17; a4 = 16; a7 = 1; return -1; } else if((((a1==1)&&((((a7==1)&&((a14==18)&&((a28==17)&&(((a26==17)||(a26==18))&&(input==6)))))&&(a4==18))&&(a25==1)))&&!(a3==1))){ a7 = 0; a4 = 16; a26 = 19; a14 = 20; a3 = 1; return -1; } else if((((((a1==1)&&((a4==17)&&((input==6)&&(((!(a7==1)&&(a26==19))&&(a14==19))||(((a26==17)&&(a7==1))&&(a14==20))))))&&(a25==1))&&(a28==15))&&(a3==1))){ a14 = 19; a7 = 0; a26 = 18; a28 = 16; return 23; } else if((((a28==17)&&((((a3==1)&&((input==4)&&(((!(a7==1)&&(a26==19))&&(a14==18))||((a14==19)&&((a26==17)&&(a7==1))))))&&(a4==18))&&(a1==1)))&&(a25==1))){ a7 = 0; a14 = 20; a28 = 16; a26 = 17; return -1; } else if(((a28==17)&&((a1==1)&&((a4==18)&&((a3==1)&&(((a25==1)&&(((input==6)&&!(a7==1))&&(a26==18)))&&(a14==18))))))){ a4 = 16; a7 = 1; a26 = 17; a28 = 15; return -1; } else if(((((a3==1)&&((a14==19)&&((a28==15)&&(((a1==1)&&((input==1)&&((a26==17)||(a26==18))))&&!(a7==1)))))&&(a25==1))&&(a4==18))){ a14 = 18; a4 = 16; a7 = 1; a26 = 17; return -1; } else if(((a1==1)&&(((a25==1)&&(((!(a3==1)&&((input==5)&&((!(a7==1)&&(a26==18))||(((a7==1)&&(a26==19))||(!(a7==1)&&(a26==17))))))&&(a28==16))&&(a4==16)))&&(a14==19)))){ a14 = 18; a7 = 1; a28 = 15; a26 = 17; a3 = 1; return -1; } else if((((((a25==1)&&(((a26==18)&&((a4==18)&&((input==1)&&(a1==1))))&&(a28==15)))&&!(a3==1))&&!(a7==1))&&(a14==18))){ a7 = 1; a26 = 17; a3 = 1; a4 = 16; return -1; } else if(((a4==17)&&((a28==16)&&(((a14==18)&&((!(a7==1)&&((a25==1)&&(((a26==18)||(a26==19))&&(input==6))))&&!(a3==1)))&&(a1==1))))){ a28 = 15; a3 = 1; a26 = 17; a4 = 16; a7 = 1; return -1; } else if((((a3==1)&&((a28==16)&&(((a1==1)&&((a14==18)&&(((((a26==18)&&(a7==1))||((a26==19)&&(a7==1)))||(!(a7==1)&&(a26==17)))&&(input==6))))&&(a4==17))))&&(a25==1))){ a26 = 19; a4 = 18; a28 = 15; a14 = 19; a7 = 1; return 23; } else if((((a25==1)&&((a1==1)&&((a4==17)&&((a3==1)&&((input==4)&&((((!(a7==1)&&(a26==18))&&(a14==18))||((a14==18)&&(!(a7==1)&&(a26==19))))||((a14==19)&&((a7==1)&&(a26==17)))))))))&&(a28==16))){ a14 = 19; a28 = 15; a26 = 17; a4 = 18; a7 = 0; return 23; } else if(((a14==19)&&((a25==1)&&(((a1==1)&&((((a28==15)&&((input==5)&&((a26==17)||(a26==18))))&&!(a3==1))&&!(a7==1)))&&(a4==16))))){ a3 = 1; a14 = 18; a7 = 1; a26 = 17; return -1; } else if(((a28==16)&&((a14==18)&&((a4==16)&&((!(a3==1)&&((a25==1)&&((input==1)&&(((a7==1)&&(a26==19))||((a26==17)&&!(a7==1))))))&&(a1==1)))))){ a14 = 20; a7 = 1; a28 = 17; a26 = 17; return 26; } else if(((((a26==19)&&((a7==1)&&((a3==1)&&((a25==1)&&((a28==15)&&((a1==1)&&(input==6)))))))&&(a14==20))&&(a4==18))){ a26 = 17; a14 = 18; a4 = 16; return -1; } else if(((((a4==17)&&((a14==19)&&((a7==1)&&(!(a3==1)&&((((a26==19)||((a26==17)||(a26==18)))&&(input==2))&&(a1==1))))))&&(a25==1))&&(a28==16))){ a28 = 17; a7 = 0; a26 = 17; return 22; } else if(((a4==17)&&(!(a3==1)&&(((a1==1)&&((input==4)&&((((!(a7==1)&&((a26==18)&&(a28==15)))&&(a14==20))||((!(a7==1)&&((a26==19)&&(a28==15)))&&(a14==20)))||(((a7==1)&&((a26==17)&&(a28==16)))&&(a14==18)))))&&(a25==1))))){ a26 = 17; a14 = 19; a28 = 16; a7 = 0; return 26; } else if((((((((((input==3)&&(a26==17))&&(a25==1))&&(a1==1))&&(a14==20))&&!(a7==1))&&(a4==17))&&!(a3==1))&&(a28==15))){ a7 = 1; a4 = 16; a3 = 1; a14 = 18; return -1; } else if(((((a3==1)&&((a28==17)&&((a14==19)&&((a4==17)&&((((a26==17)&&!(a7==1))||(((a26==18)&&(a7==1))||((a26==19)&&(a7==1))))&&(input==6))))))&&(a1==1))&&(a25==1))){ a28 = 15; a26 = 17; a7 = 1; a4 = 16; a14 = 18; return -1; } else if(((a7==1)&&((a1==1)&&((a28==17)&&((((a4==16)&&(((input==2)&&((a26==18)||(a26==19)))&&(a25==1)))&&!(a3==1))&&(a14==19)))))){ a7 = 0; a4 = 17; a28 = 15; a26 = 17; a14 = 20; return 26; } else if(((((a7==1)&&((a14==19)&&((a1==1)&&(!(a3==1)&&(((a4==18)&&(input==3))&&(a28==15))))))&&(a25==1))&&(a26==18))){ a26 = 17; a28 = 16; a14 = 20; a3 = 1; return 26; } else if((((a4==17)&&((a28==17)&&((a14==20)&&((!(a7==1)&&((a1==1)&&((((a26==17)||(a26==18))||(a26==19))&&(input==6))))&&!(a3==1)))))&&(a25==1))){ a14 = 18; a3 = 1; a28 = 15; a4 = 16; a7 = 1; a26 = 17; return -1; } else if(((((((a1==1)&&(((((a14==18)&&((a26==18)&&!(a7==1)))||((a14==18)&&(!(a7==1)&&(a26==19))))||(((a7==1)&&(a26==17))&&(a14==19)))&&(input==3)))&&(a3==1))&&(a4==17))&&(a28==17))&&(a25==1))){ a26 = 17; a4 = 16; a14 = 18; a7 = 1; a28 = 15; return -1; } else if((((a3==1)&&((a25==1)&&((a1==1)&&(((a14==18)&&((a4==18)&&((a26==18)&&(input==3))))&&(a28==17)))))&&!(a7==1))){ a28 = 15; a4 = 16; a7 = 1; a26 = 17; return -1; } else if((((a14==19)&&((a4==17)&&((((!(a3==1)&&((input==3)&&!(a7==1)))&&(a1==1))&&(a26==19))&&(a25==1))))&&(a28==15))){ a26 = 18; a7 = 1; a14 = 18; return 26; } else if(((a4==17)&&(((a7==1)&&((((a3==1)&&((a25==1)&&((input==4)&&(a14==20))))&&(a28==15))&&(a26==18)))&&(a1==1)))){ a28 = 16; a7 = 0; return 24; } else if(((a4==18)&&((a3==1)&&(((((input==2)&&((((a26==19)&&!(a7==1))&&(a14==18))||((a14==19)&&((a26==17)&&(a7==1)))))&&(a28==17))&&(a25==1))&&(a1==1))))){ a7 = 1; a28 = 16; a14 = 20; a26 = 19; return -1; } else if(((a25==1)&&((a1==1)&&((((a26==18)&&((((a14==20)&&(input==6))&&(a3==1))&&(a4==17)))&&(a28==17))&&(a7==1))))){ a4 = 16; a28 = 15; a14 = 18; a26 = 17; return -1; } else if(((((a26==19)&&(((((a1==1)&&((input==4)&&(a28==15)))&&!(a7==1))&&(a4==16))&&(a25==1)))&&!(a3==1))&&(a14==19))){ a26 = 17; a3 = 1; a14 = 18; a7 = 1; return -1; } else if(((((input==2)&&((((!(a7==1)&&((a28==17)&&((a26==19)&&((a3==1)&&(a4==18)))))&&(a14==20))||((a14==18)&&((a7==1)&&((a28==15)&&((!(a3==1)&&(a4==16))&&(a26==17))))))||(((a7==1)&&((a28==15)&&((a26==18)&&((a4==16)&&!(a3==1)))))&&(a14==18))))&&(a1==1))&&(a25==1))){ a28 = 15; a14 = 18; a3 = 1; a7 = 1; a4 = 16; a26 = 17; return -1; } else if(((a4==18)&&(((a1==1)&&((!(a7==1)&&((a14==19)&&((a25==1)&&((input==2)&&((a26==17)||(a26==18))))))&&(a28==15)))&&(a3==1)))){ a26 = 18; a14 = 20; a28 = 17; return 24; } else if(((((a25==1)&&((a4==16)&&(((a14==20)&&((((a7==1)&&(a26==19))||(!(a7==1)&&(a26==17)))&&(input==1)))&&!(a3==1))))&&(a28==17))&&(a1==1))){ a7 = 1; a28 = 15; a14 = 18; a26 = 17; a3 = 1; return -1; } else if((((a4==18)&&((((a14==18)&&(((((a26==18)||(a26==19))&&(input==6))&&(a28==15))&&(a1==1)))&&(a25==1))&&(a7==1)))&&(a3==1))){ a4 = 16; a26 = 17; return -1; } else if(((a3==1)&&((a25==1)&&((a28==17)&&((((input==4)&&((((a14==19)&&((a26==18)&&!(a7==1)))||((a14==19)&&(!(a7==1)&&(a26==19))))||(((a7==1)&&(a26==17))&&(a14==20))))&&(a1==1))&&(a4==17)))))){ a4 = 18; a28 = 16; a26 = 19; a7 = 0; a14 = 19; return 23; } else if(((((((a26==19)&&((a14==19)&&((a4==17)&&((input==6)&&(a25==1)))))&&!(a7==1))&&(a1==1))&&(a28==16))&&!(a3==1))){ a4 = 16; a7 = 1; a28 = 15; a14 = 18; a3 = 1; a26 = 17; return -1; } else if(((a26==17)&&((a1==1)&&((((((!(a3==1)&&(input==3))&&(a14==18))&&(a28==17))&&!(a7==1))&&(a25==1))&&(a4==16))))){ a7 = 1; a3 = 1; a28 = 15; return -1; } else if(((a4==16)&&(((a26==17)&&((a14==19)&&(((a28==17)&&((!(a7==1)&&(input==4))&&(a1==1)))&&!(a3==1))))&&(a25==1)))){ a14 = 18; a7 = 1; a28 = 15; a3 = 1; return -1; } else if(((a4==17)&&(((((((a1==1)&&((a3==1)&&(input==5)))&&(a14==19))&&(a7==1))&&(a26==18))&&(a25==1))&&(a28==15)))){ a14 = 20; a26 = 19; return 22; } else if((!(a3==1)&&((a4==18)&&((((a14==18)&&((a28==16)&&((input==1)&&((((a7==1)&&(a26==19))||(!(a7==1)&&(a26==17)))||(!(a7==1)&&(a26==18))))))&&(a25==1))&&(a1==1))))){ a14 = 19; a26 = 18; a7 = 1; return 22; } else if((((a7==1)&&((a3==1)&&((a14==20)&&((a25==1)&&((a4==17)&&(((input==6)&&(a26==18))&&(a28==15)))))))&&(a1==1))){ a26 = 17; a7 = 0; a28 = 16; return 24; } else if(((a25==1)&&(((a1==1)&&((a28==15)&&((a26==17)&&((a4==18)&&(((a14==20)&&(input==6))&&(a3==1))))))&&!(a7==1)))){ a4 = 16; a7 = 1; a14 = 18; return -1; } else if((((a4==18)&&((a3==1)&&((a28==15)&&((((a25==1)&&((a1==1)&&(input==5)))&&(a7==1))&&(a26==17)))))&&(a14==19))){ a28 = 17; a7 = 0; a26 = 18; return 22; } else if((((a26==19)&&((a1==1)&&((a14==18)&&(((((input==5)&&(a25==1))&&!(a3==1))&&(a4==16))&&(a7==1)))))&&(a28==17))){ a3 = 1; a26 = 17; a28 = 15; return -1; } else if((((a1==1)&&((a4==17)&&((a28==17)&&((a14==20)&&((!(a3==1)&&((((a26==17)||(a26==18))||(a26==19))&&(input==4)))&&(a7==1))))))&&(a25==1))){ a3 = 1; a28 = 15; a14 = 18; a26 = 17; a4 = 16; return -1; } else if((!(a7==1)&&((!(a3==1)&&((((a28==17)&&((a14==19)&&((a26==18)&&(input==3))))&&(a25==1))&&(a1==1)))&&(a4==16)))){ a3 = 1; a7 = 1; a14 = 18; a28 = 15; a26 = 17; return -1; } else if((((a4==18)&&((a14==20)&&((a26==18)&&(((a1==1)&&((a25==1)&&((a3==1)&&(input==4))))&&!(a7==1)))))&&(a28==17))){ a4 = 16; a14 = 18; a28 = 15; a7 = 1; a26 = 17; return -1; } else if((!(a3==1)&&((a4==18)&&(!(a7==1)&&((a25==1)&&((a28==16)&&(((a1==1)&&((input==2)&&((a26==18)||(a26==19))))&&(a14==20)))))))){ a14 = 18; a28 = 15; a4 = 17; a26 = 18; return 23; } else if(((a4==18)&&((a26==17)&&(((a14==19)&&(((a25==1)&&(((a7==1)&&(input==3))&&(a3==1)))&&(a28==15)))&&(a1==1))))){ a4 = 16; a14 = 18; return -1; } else if(((a25==1)&&(((a4==18)&&((((a3==1)&&((((a26==17)&&!(a7==1))||(((a26==18)&&(a7==1))||((a26==19)&&(a7==1))))&&(input==3)))&&(a28==16))&&(a1==1)))&&(a14==19)))){ a26 = 17; a28 = 15; a14 = 18; a4 = 16; a7 = 1; return -1; } else if((!(a3==1)&&(!(a7==1)&&((a25==1)&&((a1==1)&&((a28==17)&&((a14==18)&&(((input==2)&&(a26==17))&&(a4==16))))))))){ a3 = 1; a28 = 15; a7 = 1; return -1; } else if((((a14==18)&&((((a1==1)&&((a4==17)&&((((a26==19)&&(a7==1))||((a26==17)&&!(a7==1)))&&(input==1))))&&(a28==17))&&(a25==1)))&&(a3==1))){ a28 = 15; a7 = 1; a4 = 16; a26 = 17; return -1; } else if((((a1==1)&&((((((((!(a7==1)&&(a26==19))&&(a14==18))||(((a7==1)&&(a26==17))&&(a14==19)))||((a14==19)&&((a26==18)&&(a7==1))))&&(input==4))&&(a28==17))&&(a25==1))&&(a4==18)))&&!(a3==1))){ a26 = 18; a14 = 19; a7 = 1; return 24; } else if(((a1==1)&&(!(a3==1)&&((a4==16)&&(((a14==19)&&(((a28==17)&&(((a26==18)||(a26==19))&&(input==3)))&&(a7==1)))&&(a25==1)))))){ a14 = 18; a28 = 15; a3 = 1; a26 = 17; return -1; } else if(((a25==1)&&((a1==1)&&((((a28==17)&&((input==5)&&((((!(a7==1)&&(a26==18))&&(a14==18))||((a14==18)&&((a26==19)&&!(a7==1))))||(((a7==1)&&(a26==17))&&(a14==19)))))&&(a3==1))&&(a4==17))))){ a14 = 18; a28 = 15; a7 = 1; a4 = 16; a26 = 17; return -1; } else if(((a25==1)&&((a26==18)&&(((a4==16)&&(((((input==2)&&(a28==16))&&(a1==1))&&(a7==1))&&!(a3==1)))&&(a14==18))))){ a26 = 17; a28 = 15; a3 = 1; return -1; } else if(((!(a3==1)&&((((a7==1)&&((((a14==18)&&(input==6))&&(a1==1))&&(a4==16)))&&(a26==19))&&(a28==17)))&&(a25==1))){ a28 = 15; a26 = 17; a3 = 1; return -1; } else if(((a25==1)&&(((a4==18)&&((a28==15)&&((a1==1)&&(((a26==18)&&((a3==1)&&(input==6)))&&(a7==1)))))&&(a14==19)))){ a26 = 17; a4 = 16; a14 = 18; return -1; } else if(((a14==18)&&((a25==1)&&((a28==16)&&(((((input==3)&&(((a26==18)&&!(a7==1))||(((a7==1)&&(a26==19))||(!(a7==1)&&(a26==17)))))&&(a1==1))&&(a4==18))&&!(a3==1)))))){ a28 = 15; a3 = 1; a26 = 17; a7 = 1; a4 = 16; return -1; } else if((((a3==1)&&((((((((a26==19)&&(a4==17))&&(a28==17))&&!(a7==1))&&(a14==20))||((a14==18)&&((((a26==17)&&(a4==18))&&(a28==15))&&(a7==1))))&&(input==6))&&(a1==1)))&&(a25==1))){ a28 = 15; a14 = 18; a26 = 17; a7 = 1; a4 = 16; return -1; } else if(((a14==20)&&((a1==1)&&((((a25==1)&&(((((a7==1)&&(a26==19))||((a26==17)&&!(a7==1)))&&(input==5))&&(a28==17)))&&(a4==16))&&!(a3==1))))){ a7 = 1; a14 = 18; a26 = 17; a28 = 15; a3 = 1; return -1; } else if(((!(a3==1)&&((a7==1)&&(((((((a26==18)||(a26==19))&&(input==5))&&(a4==17))&&(a14==18))&&(a25==1))&&(a1==1))))&&(a28==15))){ a28 = 16; a14 = 20; a4 = 18; a3 = 1; a26 = 17; return -1; } else if((((a4==16)&&((!(a3==1)&&((a25==1)&&((((a14==20)&&((a26==18)&&(a7==1)))||((((a26==19)&&!(a7==1))&&(a14==19))||((a14==20)&&((a7==1)&&(a26==17)))))&&(input==1))))&&(a1==1)))&&(a28==16))){ a26 = 18; a14 = 18; a4 = 17; a7 = 0; a28 = 15; return 21; } else if(((a1==1)&&((((((a28==15)&&((((a7==1)&&(a26==19))||((a26==17)&&!(a7==1)))&&(input==4)))&&(a14==19))&&!(a3==1))&&(a25==1))&&(a4==18)))){ a7 = 1; a26 = 18; a14 = 20; return 24; } else if((((!(a3==1)&&((((((((a4==16)&&(a26==18))&&(a28==17))&&!(a7==1))&&(a14==20))||((a14==20)&&((((a26==19)&&(a4==16))&&(a28==17))&&!(a7==1))))||((a14==18)&&((((a26==17)&&(a4==17))&&(a28==15))&&(a7==1))))&&(input==6)))&&(a1==1))&&(a25==1))){ a26 = 17; a14 = 18; a4 = 16; a7 = 1; a28 = 15; a3 = 1; return -1; } else if((((a26==18)&&((((a14==19)&&((a25==1)&&((a1==1)&&((a4==17)&&(input==5)))))&&(a28==15))&&!(a3==1)))&&!(a7==1))){ a3 = 1; a14 = 18; a7 = 1; a26 = 17; a4 = 16; return -1; } else if(((a1==1)&&((a25==1)&&(((a28==17)&&(((a14==18)&&((a7==1)&&((input==2)&&(a26==18))))&&(a4==16)))&&!(a3==1))))){ return 22; } else if((((a25==1)&&((a3==1)&&((a4==18)&&((a14==20)&&((((input==5)&&(a1==1))&&(a26==17))&&(a7==1))))))&&(a28==16))){ a4 = 16; a14 = 18; a28 = 15; return -1; } else if((((a3==1)&&((a25==1)&&((a7==1)&&((a14==18)&&((a28==17)&&((a4==17)&&((input==1)&&((a26==17)||(a26==18)))))))))&&(a1==1))){ a28 = 15; a4 = 16; a26 = 17; return -1; } else if(((a1==1)&&((a25==1)&&(!(a3==1)&&((((a14==18)&&((((a4==17)&&(a26==17))&&(a28==15))&&(a7==1)))||(((!(a7==1)&&(((a26==18)&&(a4==16))&&(a28==17)))&&(a14==20))||((a14==20)&&(!(a7==1)&&(((a4==16)&&(a26==19))&&(a28==17))))))&&(input==3)))))){ a3 = 1; a14 = 18; a7 = 1; a28 = 15; a26 = 17; a4 = 16; return -1; } else if(((a28==17)&&((a14==20)&&((a4==16)&&((((a25==1)&&((((a7==1)&&(a26==19))||((a26==17)&&!(a7==1)))&&(input==3)))&&(a1==1))&&!(a3==1)))))){ a26 = 17; a7 = 1; a28 = 15; a14 = 18; a3 = 1; return -1; } else if((((a4==18)&&((a14==19)&&((a28==17)&&((a25==1)&&(((input==4)&&((((a26==18)&&(a7==1))||((a7==1)&&(a26==19)))||(!(a7==1)&&(a26==17))))&&(a3==1))))))&&(a1==1))){ a7 = 1; a14 = 20; a28 = 16; a26 = 18; return -1; } if(((((((((a3==1)&&(a4==16))&&(a25==1))&&(a1==1))&&(a26==18))&&(a28==15))&&(a7==1))&&(a14==20))){ error_12: exit(0); } if(((((((((a3==1)&&(a4==16))&&(a25==1))&&(a1==1))&&(a26==19))&&(a28==16))&&(a7==1))&&(a14==18))){ error_19: exit(0); } if(((((((((a3==1)&&(a4==16))&&(a25==1))&&(a1==1))&&(a26==19))&&(a28==16))&&(a7==1))&&(a14==20))){ error_31: exit(0); } if(((((((((a3==1)&&(a4==16))&&(a25==1))&&(a1==1))&&(a26==18))&&(a28==17))&&!(a7==1))&&(a14==18))){ error_39: exit(0); } if(((((((((a3==1)&&(a4==16))&&(a25==1))&&(a1==1))&&(a26==19))&&(a28==17))&&!(a7==1))&&(a14==20))){ error_52: exit(0); } if(((((((((a3==1)&&(a4==16))&&(a25==1))&&(a1==1))&&(a26==18))&&(a28==15))&&(a7==1))&&(a14==19))){ error_6: exit(0); } if(((((((((a3==1)&&(a4==17))&&(a25==1))&&(a1==1))&&(a26==19))&&(a28==15))&&!(a7==1))&&(a14==18))){ error_58: exit(0); } if(((((((((a3==1)&&(a4==16))&&(a25==1))&&(a1==1))&&(a26==19))&&(a28==17))&&!(a7==1))&&(a14==18))){ error_40: exit(0); } if(((((((((a3==1)&&(a4==16))&&(a25==1))&&(a1==1))&&(a26==19))&&(a28==15))&&!(a7==1))&&(a14==18))){ error_4: exit(0); } if(((((((((a3==1)&&(a4==16))&&(a25==1))&&(a1==1))&&(a26==17))&&(a28==17))&&!(a7==1))&&(a14==18))){ error_38: __VERIFIER_error(); } if(((((((((a3==1)&&(a4==16))&&(a25==1))&&(a1==1))&&(a26==18))&&(a28==17))&&!(a7==1))&&(a14==19))){ error_45: exit(0); } if(((((((((a3==1)&&(a4==16))&&(a25==1))&&(a1==1))&&(a26==17))&&(a28==15))&&(a7==1))&&(a14==20))){ error_11: exit(0); } if(((((((((a3==1)&&(a4==16))&&(a25==1))&&(a1==1))&&(a26==17))&&(a28==16))&&!(a7==1))&&(a14==19))){ error_26: exit(0); } if(((((((((a3==1)&&(a4==16))&&(a25==1))&&(a1==1))&&(a26==17))&&(a28==15))&&(a7==1))&&(a14==18))){ globalError: exit(0); } if(((((((((a3==1)&&(a4==16))&&(a25==1))&&(a1==1))&&(a26==18))&&(a28==15))&&!(a7==1))&&(a14==19))){ error_9: exit(0); } if(((((((((a3==1)&&(a4==16))&&(a25==1))&&(a1==1))&&(a26==17))&&(a28==16))&&(a7==1))&&(a14==18))){ error_17: exit(0); } if(((((((((a3==1)&&(a4==16))&&(a25==1))&&(a1==1))&&(a26==17))&&(a28==16))&&!(a7==1))&&(a14==20))){ error_32: exit(0); } if(((((((((a3==1)&&(a4==16))&&(a25==1))&&(a1==1))&&(a26==17))&&(a28==17))&&(a7==1))&&(a14==18))){ error_35: exit(0); } if(((((((((a3==1)&&(a4==17))&&(a25==1))&&(a1==1))&&(a26==19))&&(a28==15))&&(a7==1))&&(a14==18))){ error_55: exit(0); } if(((((((((a3==1)&&(a4==16))&&(a25==1))&&(a1==1))&&(a26==18))&&(a28==17))&&(a7==1))&&(a14==18))){ error_36: exit(0); } if(((((((((a3==1)&&(a4==16))&&(a25==1))&&(a1==1))&&(a26==17))&&(a28==15))&&!(a7==1))&&(a14==20))){ error_14: exit(0); } if(((((((((a3==1)&&(a4==16))&&(a25==1))&&(a1==1))&&(a26==18))&&(a28==16))&&(a7==1))&&(a14==18))){ error_18: exit(0); } if(((((((((a3==1)&&(a4==16))&&(a25==1))&&(a1==1))&&(a26==19))&&(a28==15))&&(a7==1))&&(a14==20))){ error_13: exit(0); } if(((((((((a3==1)&&(a4==16))&&(a25==1))&&(a1==1))&&(a26==18))&&(a28==15))&&!(a7==1))&&(a14==20))){ error_15: exit(0); } if(((((((((a3==1)&&(a4==16))&&(a25==1))&&(a1==1))&&(a26==18))&&(a28==16))&&!(a7==1))&&(a14==19))){ error_27: exit(0); } if(((((((((a3==1)&&(a4==16))&&(a25==1))&&(a1==1))&&(a26==18))&&(a28==16))&&(a7==1))&&(a14==20))){ error_30: exit(0); } if(((((((((a3==1)&&(a4==16))&&(a25==1))&&(a1==1))&&(a26==17))&&(a28==17))&&!(a7==1))&&(a14==19))){ error_44: exit(0); } if(((((((((a3==1)&&(a4==16))&&(a25==1))&&(a1==1))&&(a26==17))&&(a28==15))&&(a7==1))&&(a14==19))){ error_5: exit(0); } if(((((((((a3==1)&&(a4==16))&&(a25==1))&&(a1==1))&&(a26==17))&&(a28==16))&&(a7==1))&&(a14==20))){ error_29: exit(0); } if(((((((((a3==1)&&(a4==16))&&(a25==1))&&(a1==1))&&(a26==18))&&(a28==15))&&!(a7==1))&&(a14==18))){ error_3: exit(0); } if(((((((((a3==1)&&(a4==16))&&(a25==1))&&(a1==1))&&(a26==17))&&(a28==17))&&(a7==1))&&(a14==20))){ error_47: exit(0); } if(((((((((a3==1)&&(a4==16))&&(a25==1))&&(a1==1))&&(a26==18))&&(a28==17))&&!(a7==1))&&(a14==20))){ error_51: exit(0); } if(((((((((a3==1)&&(a4==16))&&(a25==1))&&(a1==1))&&(a26==19))&&(a28==16))&&!(a7==1))&&(a14==20))){ error_34: exit(0); } if(((((((((a3==1)&&(a4==16))&&(a25==1))&&(a1==1))&&(a26==19))&&(a28==15))&&(a7==1))&&(a14==19))){ error_7: exit(0); } if(((((((((a3==1)&&(a4==17))&&(a25==1))&&(a1==1))&&(a26==17))&&(a28==15))&&(a7==1))&&(a14==19))){ error_59: exit(0); } if(((((((((a3==1)&&(a4==16))&&(a25==1))&&(a1==1))&&(a26==19))&&(a28==17))&&(a7==1))&&(a14==20))){ error_49: exit(0); } if(((((((((a3==1)&&(a4==16))&&(a25==1))&&(a1==1))&&(a26==19))&&(a28==17))&&!(a7==1))&&(a14==19))){ error_46: exit(0); } if(((((((((a3==1)&&(a4==16))&&(a25==1))&&(a1==1))&&(a26==17))&&(a28==16))&&!(a7==1))&&(a14==18))){ error_20: exit(0); } if(((((((((a3==1)&&(a4==17))&&(a25==1))&&(a1==1))&&(a26==18))&&(a28==15))&&!(a7==1))&&(a14==18))){ error_57: exit(0); } if(((((((((a3==1)&&(a4==17))&&(a25==1))&&(a1==1))&&(a26==17))&&(a28==15))&&(a7==1))&&(a14==18))){ error_53: exit(0); } if(((((((((a3==1)&&(a4==16))&&(a25==1))&&(a1==1))&&(a26==18))&&(a28==16))&&!(a7==1))&&(a14==18))){ error_21: exit(0); } if(((((((((a3==1)&&(a4==16))&&(a25==1))&&(a1==1))&&(a26==19))&&(a28==16))&&(a7==1))&&(a14==19))){ error_25: exit(0); } if(((((((((a3==1)&&(a4==16))&&(a25==1))&&(a1==1))&&(a26==19))&&(a28==17))&&(a7==1))&&(a14==19))){ error_43: exit(0); } if(((((((((a3==1)&&(a4==16))&&(a25==1))&&(a1==1))&&(a26==19))&&(a28==15))&&!(a7==1))&&(a14==20))){ error_16: exit(0); } if(((((((((a3==1)&&(a4==17))&&(a25==1))&&(a1==1))&&(a26==17))&&(a28==15))&&!(a7==1))&&(a14==18))){ error_56: exit(0); } if(((((((((a3==1)&&(a4==16))&&(a25==1))&&(a1==1))&&(a26==18))&&(a28==15))&&(a7==1))&&(a14==18))){ error_0: exit(0); } if(((((((((a3==1)&&(a4==16))&&(a25==1))&&(a1==1))&&(a26==17))&&(a28==15))&&!(a7==1))&&(a14==18))){ error_2: exit(0); } if(((((((((a3==1)&&(a4==16))&&(a25==1))&&(a1==1))&&(a26==18))&&(a28==16))&&(a7==1))&&(a14==19))){ error_24: exit(0); } if(((((((((a3==1)&&(a4==17))&&(a25==1))&&(a1==1))&&(a26==18))&&(a28==15))&&(a7==1))&&(a14==18))){ error_54: exit(0); } if(((((((((a3==1)&&(a4==16))&&(a25==1))&&(a1==1))&&(a26==17))&&(a28==16))&&(a7==1))&&(a14==19))){ error_23: exit(0); } if(((((((((a3==1)&&(a4==16))&&(a25==1))&&(a1==1))&&(a26==18))&&(a28==17))&&(a7==1))&&(a14==20))){ error_48: exit(0); } if(((((((((a3==1)&&(a4==16))&&(a25==1))&&(a1==1))&&(a26==17))&&(a28==15))&&!(a7==1))&&(a14==19))){ error_8: exit(0); } if(((((((((a3==1)&&(a4==16))&&(a25==1))&&(a1==1))&&(a26==19))&&(a28==16))&&!(a7==1))&&(a14==19))){ error_28: exit(0); } if(((((((((a3==1)&&(a4==16))&&(a25==1))&&(a1==1))&&(a26==19))&&(a28==15))&&(a7==1))&&(a14==18))){ error_1: exit(0); } if(((((((((a3==1)&&(a4==16))&&(a25==1))&&(a1==1))&&(a26==19))&&(a28==15))&&!(a7==1))&&(a14==19))){ error_10: exit(0); } if(((((((((a3==1)&&(a4==16))&&(a25==1))&&(a1==1))&&(a26==17))&&(a28==17))&&(a7==1))&&(a14==19))){ error_41: exit(0); } if(((((((((a3==1)&&(a4==16))&&(a25==1))&&(a1==1))&&(a26==18))&&(a28==16))&&!(a7==1))&&(a14==20))){ error_33: exit(0); } if(((((((((a3==1)&&(a4==16))&&(a25==1))&&(a1==1))&&(a26==19))&&(a28==16))&&!(a7==1))&&(a14==18))){ error_22: exit(0); } if(((((((((a3==1)&&(a4==16))&&(a25==1))&&(a1==1))&&(a26==18))&&(a28==17))&&(a7==1))&&(a14==19))){ error_42: exit(0); } if(((((((((a3==1)&&(a4==16))&&(a25==1))&&(a1==1))&&(a26==19))&&(a28==17))&&(a7==1))&&(a14==18))){ error_37: exit(0); } if(((((((((a3==1)&&(a4==16))&&(a25==1))&&(a1==1))&&(a26==17))&&(a28==17))&&!(a7==1))&&(a14==20))){ error_50: 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); } }