int calculate_output(int); int calculate_output2(int); extern void __VERIFIER_error(void); extern int __VERIFIER_nondet_int(void); extern void exit(int); // inputs int inputB = 2; int inputE = 5; int inputD = 4; int inputF = 6; int inputC = 3; int inputA = 1; int a15 = 3; int a18 = -87; int a16 = 11; int a12 = 5; int calculate_output2(int input); int calculate_output(int input) { if(((((a16==8) && (a15==3)) && a18 <= -156 ) && (a12==6))){ error_3: exit(0); } if(((((a16==8) && (a15==3)) && 134 < a18 ) && (a12==9))){ error_18: exit(0); } if(((((a16==9) && (a15==3)) && a18 <= -156 ) && (a12==8))){ error_31: exit(0); } if(((((a16==10) && (a15==3)) && a18 <= -156 ) && (a12==6))){ error_43: exit(0); } if(((((a16==8) && (a15==3)) && 134 < a18 ) && (a12==6))){ error_6: exit(0); } if(((((a16==9) && (a15==3)) && 134 < a18 ) && (a12==9))){ error_38: exit(0); } if(((((a16==9) && (a15==3)) && a18 <= -156 ) && (a12==7))){ error_27: exit(0); } if(((((a16==9) && (a15==3)) && 134 < a18 ) && (a12==5))){ error_22: exit(0); } if(((((a16==10) && (a15==3)) && a18 <= -156 ) && (a12==8))){ error_51: exit(0); } if(((((a16==9) && (a15==3)) && 134 < a18 ) && (a12==7))){ error_30: exit(0); } if(((((a16==10) && (a15==3)) && 134 < a18 ) && (a12==6))){ error_46: exit(0); } if(((((a16==8) && (a15==3)) && ((-156 < a18) && (-79 >= a18)) ) && (a12==7))){ error_8: exit(0); } if(((((a16==8) && (a15==3)) && 134 < a18 ) && (a12==8))){ error_14: exit(0); } if(((((a16==8) && (a15==3)) && ((-79 < a18) && (134 >= a18)) ) && (a12==6))){ error_5: exit(0); } if(((((a16==9) && (a15==3)) && ((-79 < a18) && (134 >= a18)) ) && (a12==9))){ error_37: exit(0); } if(((((a16==8) && (a15==3)) && ((-156 < a18) && (-79 >= a18)) ) && (a12==5))){ error_0: exit(0); } if(((((a16==8) && (a15==3)) && a18 <= -156 ) && (a12==9))){ error_15: exit(0); } if(((((a16==10) && (a15==3)) && ((-79 < a18) && (134 >= a18)) ) && (a12==5))){ error_41: exit(0); } if(((((a16==9) && (a15==3)) && ((-156 < a18) && (-79 >= a18)) ) && (a12==5))){ error_20: exit(0); } if(((((a16==10) && (a15==3)) && 134 < a18 ) && (a12==8))){ error_54: exit(0); } if(((((a16==8) && (a15==3)) && ((-79 < a18) && (134 >= a18)) ) && (a12==5))){ error_1: exit(0); } if(((((a16==9) && (a15==3)) && ((-79 < a18) && (134 >= a18)) ) && (a12==8))){ error_33: exit(0); } if(((((a16==8) && (a15==3)) && ((-156 < a18) && (-79 >= a18)) ) && (a12==6))){ error_4: exit(0); } if(((((a16==10) && (a15==3)) && ((-156 < a18) && (-79 >= a18)) ) && (a12==8))){ error_52: exit(0); } if(((((a16==10) && (a15==3)) && ((-156 < a18) && (-79 >= a18)) ) && (a12==6))){ error_44: exit(0); } if(((((a16==9) && (a15==3)) && a18 <= -156 ) && (a12==6))){ error_23: exit(0); } if(((((a16==8) && (a15==3)) && 134 < a18 ) && (a12==7))){ error_10: exit(0); } if(((((a16==10) && (a15==3)) && ((-156 < a18) && (-79 >= a18)) ) && (a12==9))){ error_56: exit(0); } if(((((a16==9) && (a15==3)) && 134 < a18 ) && (a12==8))){ error_34: __VERIFIER_error(); } if(((((a16==9) && (a15==3)) && 134 < a18 ) && (a12==6))){ error_26: exit(0); } if(((((a16==9) && (a15==3)) && ((-156 < a18) && (-79 >= a18)) ) && (a12==9))){ error_36: exit(0); } if(((((a16==10) && (a15==3)) && ((-79 < a18) && (134 >= a18)) ) && (a12==8))){ error_53: exit(0); } if(((((a16==9) && (a15==3)) && ((-79 < a18) && (134 >= a18)) ) && (a12==5))){ error_21: exit(0); } if(((((a16==8) && (a15==3)) && ((-156 < a18) && (-79 >= a18)) ) && (a12==8))){ error_12: exit(0); } if(((((a16==10) && (a15==3)) && ((-79 < a18) && (134 >= a18)) ) && (a12==9))){ error_57: exit(0); } if(((((a16==9) && (a15==3)) && a18 <= -156 ) && (a12==9))){ error_35: exit(0); } if(((((a16==8) && (a15==3)) && ((-156 < a18) && (-79 >= a18)) ) && (a12==9))){ error_16: exit(0); } if(((((a16==9) && (a15==3)) && a18 <= -156 ) && (a12==5))){ error_19: exit(0); } if(((((a16==11) && (a15==3)) && a18 <= -156 ) && (a12==5))){ error_59: exit(0); } if(((((a16==10) && (a15==3)) && 134 < a18 ) && (a12==7))){ error_50: exit(0); } if(((((a16==9) && (a15==3)) && ((-79 < a18) && (134 >= a18)) ) && (a12==7))){ error_29: exit(0); } if(((((a16==8) && (a15==3)) && ((-79 < a18) && (134 >= a18)) ) && (a12==7))){ error_9: exit(0); } if(((((a16==9) && (a15==3)) && ((-156 < a18) && (-79 >= a18)) ) && (a12==8))){ error_32: exit(0); } if(((((a16==10) && (a15==3)) && a18 <= -156 ) && (a12==5))){ error_39: exit(0); } if(((((a16==9) && (a15==3)) && ((-79 < a18) && (134 >= a18)) ) && (a12==6))){ error_25: exit(0); } if(((((a16==10) && (a15==3)) && 134 < a18 ) && (a12==9))){ error_58: exit(0); } if(((((a16==9) && (a15==3)) && ((-156 < a18) && (-79 >= a18)) ) && (a12==6))){ error_24: exit(0); } if(((((a16==10) && (a15==3)) && ((-79 < a18) && (134 >= a18)) ) && (a12==6))){ error_45: exit(0); } if(((((a16==8) && (a15==3)) && a18 <= -156 ) && (a12==7))){ error_7: exit(0); } if(((((a16==8) && (a15==3)) && a18 <= -156 ) && (a12==8))){ error_11: exit(0); } if(((((a16==8) && (a15==3)) && ((-79 < a18) && (134 >= a18)) ) && (a12==8))){ error_13: exit(0); } if(((((a16==10) && (a15==3)) && a18 <= -156 ) && (a12==9))){ error_55: exit(0); } if(((((a16==8) && (a15==3)) && ((-79 < a18) && (134 >= a18)) ) && (a12==9))){ error_17: exit(0); } if(((((a16==8) && (a15==3)) && a18 <= -156 ) && (a12==5))){ globalError: exit(0); } if(((((a16==10) && (a15==3)) && ((-79 < a18) && (134 >= a18)) ) && (a12==7))){ error_49: exit(0); } if(((((a16==8) && (a15==3)) && 134 < a18 ) && (a12==5))){ error_2: exit(0); } if(((((a16==10) && (a15==3)) && 134 < a18 ) && (a12==5))){ error_42: exit(0); } if(((((a16==10) && (a15==3)) && ((-156 < a18) && (-79 >= a18)) ) && (a12==5))){ error_40: exit(0); } if(((((a16==10) && (a15==3)) && ((-156 < a18) && (-79 >= a18)) ) && (a12==7))){ error_48: exit(0); } if(((((a16==10) && (a15==3)) && a18 <= -156 ) && (a12==7))){ error_47: exit(0); } if(((((a16==9) && (a15==3)) && ((-156 < a18) && (-79 >= a18)) ) && (a12==7))){ error_28: exit(0); } if(((a15==3) && ((a16==12) && ((input == 6) && ((((a12==7) && 134 < a18 ) || ( a18 <= -156 && (a12==8))) || ((a12==8) && ((-156 < a18) && (-79 >= a18)) )))))){ a18 = (((((a18 - 0) + 0) - 0) % 299922)- 300077); a12 = 8; return 22; } else if(((((a15==3) && ((a12==7) && (input == 3))) && (a16==12)) && ((-156 < a18) && (-79 >= a18)) )){ a18 = ((((a18 * 10)/ -5) * 5) / 5); a12 = 9; return 22; } else if(((((input == 2) && (((a12==7) && ((-156 < a18) && (-79 >= a18)) ) || (((a12==6) && 134 < a18 ) || ((a12==7) && a18 <= -156 )))) && (a16==9)) && (a15==4))){ a18 = ((((a18 / 5) % 106)+ 27) + 1); a12 = 7; return 21; } else if(((a15==4) && ((((input == 1) && ( ((-79 < a18) && (134 >= a18)) || 134 < a18 )) && (a16==10)) && (a12==5)))){ a18 = ((((a18 * 9)/ 10) * 1) - 557770); a15 = 3; a12 = 6; return -1; } else if(((a16==8) && ((a15==4) && ((a12==8) && ((input == 4) && ((-79 < a18) && (134 >= a18)) ))))){ a18 = (((a18 - 465312) / 5) + -95319); a15 = 3; a12 = 5; return -1; } else if((((a12==8) && ((a15==4) && ( ((-79 < a18) && (134 >= a18)) && (input == 1)))) && (a16==8))){ a18 = (((a18 + 534994) - 153945) - 311877); a12 = 9; return 25; } else if((( ((-79 < a18) && (134 >= a18)) && ((a16==12) && ((a15==3) && (input == 6)))) && (a12==7))){ a18 = (((((a18 / 5) - -329526) * 1) * -1)/ 10); a16 = 8; a12 = 5; return -1; } else if((((a12==7) && ((( ((-79 < a18) && (134 >= a18)) || 134 < a18 ) && (input == 6)) && (a16==11))) && (a15==3))){ a18 = (((((a18 - 0) % 299922)- 300077) / 5) - 269658); a16 = 8; a12 = 5; return -1; } else if((((a12==5) && (((( ((-156 < a18) && (-79 >= a18)) || ((-79 < a18) && (134 >= a18)) ) || 134 < a18 ) && (input == 5)) && (a15==4))) && (a16==8))){ a18 = ((((a18 + 0) - 386666) % 299922)+ -300077); a15 = 3; return -1; } else if(((a12==5) && ((((input == 1) && (a16==8)) && a18 <= -156 ) && (a15==4)))){ a15 = 3; return -1; } else if((( ((-156 < a18) && (-79 >= a18)) && (((a15==3) && (input == 5)) && (a12==7))) && (a16==12))){ a18 = (((a18 - 359568) + -143924) + -3048); a16 = 8; a12 = 5; return -1; } else if((((((input == 3) && (a16==8)) && (a12==7)) && ((-79 < a18) && (134 >= a18)) ) && (a15==4))){ a18 = (((a18 * 5) + -585061) + -4999); a15 = 3; a12 = 5; return -1; } else if(((a16==10) && ((a12==5) && (((input == 3) && ((-156 < a18) && (-79 >= a18)) ) && (a15==4))))){ a18 = (((((((a18 * 10)/ 5) * 10)/ 9) / 5) * 45)/ 10); a16 = 8; return -1; } else if(((((a16==8) && ((a12==6) && (input == 2))) && a18 <= -156 ) && (a15==4))){ a15 = 3; a12 = 5; return -1; } else if((((a15==4) && ((a12==5) && (( 134 < a18 || ( ((-156 < a18) && (-79 >= a18)) || ((-79 < a18) && (134 >= a18)) )) && (input == 4)))) && (a16==8))){ a18 = ((((a18 % 106)- -28) + 468168) - 468167); a12 = 7; return 21; } else if((((a12==8) && ((a15==4) && ((input == 3) && (( ((-156 < a18) && (-79 >= a18)) || ((-79 < a18) && (134 >= a18)) ) || 134 < a18 )))) && (a16==9))){ a18 = ((((a18 % 299922)- 300077) + 363758) - 363759); a16 = 8; a15 = 3; a12 = 5; return -1; } else if((((((a16==12) && (input == 1)) && (a12==9)) && 134 < a18 ) && (a15==3))){ a18 = ((((((a18 - 0) % 299922)+ -300077) / 5) * 51)/ 10); a16 = 8; a12 = 5; return -1; } else if(((((a15==4) && ((input == 1) && ( ((-156 < a18) && (-79 >= a18)) || ((-79 < a18) && (134 >= a18)) ))) && (a16==9)) && (a12==5))){ a18 = (((a18 + -456144) * 1) + -99954); a16 = 8; a15 = 3; return -1; } else if(( 134 < a18 && ((a12==6) && ((a16==10) && ((input == 1) && (a15==4)))))){ a18 = ((((a18 % 299922)- 300077) + -183065) / 5); a16 = 8; a15 = 3; return -1; } else if((((a12==6) && ( a18 <= -156 && ((a16==8) && (input == 1)))) && (a15==4))){ a15 = 3; a12 = 5; return -1; } else if(((a15==3) && ((a16==12) && ((((a12==8) && 134 < a18 ) || ( a18 <= -156 && (a12==9))) && (input == 1))))){ a18 = ((((a18 % 299922)- 300077) + 389885) - 389885); a16 = 8; a12 = 5; return -1; } else if(((a16==12) && ((a12==9) && ((a15==3) && ((input == 2) && ( ((-156 < a18) && (-79 >= a18)) || ((-79 < a18) && (134 >= a18)) )))))){ a18 = (((a18 - -464480) - 792268) * 1); a16 = 8; a12 = 5; return -1; } else if(((((a16==11) && ((input == 5) && ((-156 < a18) && (-79 >= a18)) )) && (a15==3)) && (a12==5))){ a18 = ((((a18 - -528844) - -67556) * -1)/ 10); a16 = 8; return -1; } else if(((a16==9) && ((((input == 3) && (a15==4)) && ((-156 < a18) && (-79 >= a18)) ) && (a12==9)))){ a18 = ((((a18 + 207) * 5) % 106)+ 7); a16 = 10; a15 = 3; a12 = 5; return -1; } else if(((((( ((-156 < a18) && (-79 >= a18)) && (a12==8)) || (( 134 < a18 && (a12==7)) || ( a18 <= -156 && (a12==8)))) && (input == 3)) && (a15==3)) && (a16==12))){ a18 = ((((a18 / 5) + -261188) % 38)- 91); a12 = 5; return 21; } else if(((a16==11) && (((a12==8) && ((input == 1) && (a15==3))) && a18 <= -156 ))){ a16 = 8; a12 = 5; return -1; } else if((((((((a12==7) && 134 < a18 ) || ((a12==8) && a18 <= -156 )) || ( ((-156 < a18) && (-79 >= a18)) && (a12==8))) && (input == 4)) && (a15==3)) && (a16==12))){ a18 = ((((((a18 - 0) % 38)- 117) / 5) * 51)/ 10); a12 = 8; return -1; } else if((((a15==4) && (((input == 3) && ( a18 <= -156 || ((-156 < a18) && (-79 >= a18)) )) && (a12==7))) && (a16==8))){ a18 = (((a18 / 5) - 102582) * 2); a15 = 3; a12 = 5; return -1; } else if(((a16==8) && ((( ((-79 < a18) && (134 >= a18)) && (input == 3)) && (a12==9)) && (a15==4)))){ a18 = (((((a18 - 534921) + 840780) + -285366) * -1)/ 10); a15 = 3; a12 = 5; return -1; } else if(((a16==8) && ((a12==6) && ((a15==4) && ((input == 2) && (( ((-156 < a18) && (-79 >= a18)) || ((-79 < a18) && (134 >= a18)) ) || 134 < a18 )))))){ a18 = (((((a18 % 299932)+ 300066) - -1) / 5) - -438117); a16 = 12; a15 = 3; a12 = 8; return 25; } else if((((a16==12) && (((( 134 < a18 && (a12==7)) || ( a18 <= -156 && (a12==8))) || ((a12==8) && ((-156 < a18) && (-79 >= a18)) )) && (input == 1))) && (a15==3))){ a18 = ((((a18 + 0) % 299922)+ -300077) + -1); a16 = 8; a12 = 5; return -1; } else if(((a15==3) && (((( ((-79 < a18) && (134 >= a18)) || 134 < a18 ) && (input == 6)) && (a16==11)) && (a12==5)))){ a18 = ((((a18 % 38)- 116) - 2) - -1); a12 = 7; return 22; } else if(((a15==4) && ((a12==8) && ((a16==9) && ((input == 5) && (( ((-156 < a18) && (-79 >= a18)) || ((-79 < a18) && (134 >= a18)) ) || 134 < a18 )))))){ a18 = ((((((a18 % 38)- 116) + -1) * 5) % 38)- 106); a16 = 10; a15 = 3; a12 = 6; return -1; } else if(( ((-79 < a18) && (134 >= a18)) && (((a16==8) && ((a15==4) && (input == 1))) && (a12==9)))){ a18 = (((a18 + -26889) - 308042) - -53173); a15 = 3; a12 = 5; return -1; } else if(((a16==9) && (((input == 3) && ((((a12==6) && 134 < a18 ) || ((a12==7) && a18 <= -156 )) || ( ((-156 < a18) && (-79 >= a18)) && (a12==7)))) && (a15==4)))){ a18 = (((((a18 % 299922)- 300077) - 1) - -524582) - 524581); a16 = 8; a15 = 3; a12 = 5; return -1; } else if((((input == 1) && (((( ((-79 < a18) && (134 >= a18)) && (a16==11)) && (a12==9)) || (( 134 < a18 && (a16==11)) && (a12==9))) || (( a18 <= -156 && (a16==12)) && (a12==5)))) && (a15==3))){ a18 = (((((a18 % 299922)+ -300077) * 1) / 5) + -390754); a16 = 8; a12 = 5; return -1; } else if(((a15==4) && ((a12==6) && ((a16==8) && ((input == 3) && (( ((-156 < a18) && (-79 >= a18)) || ((-79 < a18) && (134 >= a18)) ) || 134 < a18 )))))){ a18 = ((((a18 + 0) % 299922)+ -300077) - 2); a16 = 12; a15 = 3; a12 = 9; return 25; } else if(((a15==3) && ((a16==12) && ((a12==5) && ((input == 1) && ( ((-156 < a18) && (-79 >= a18)) || ((-79 < a18) && (134 >= a18)) )))))){ a18 = (((((a18 % 38)+ -117) / 5) - -1641) + -1708); return 21; } else if((((a16==10) && (((input == 2) && ( ((-79 < a18) && (134 >= a18)) || 134 < a18 )) && (a15==4))) && (a12==5))){ a18 = ((((a18 - 176885) - 48192) % 299922)+ -300077); a16 = 9; a15 = 3; a12 = 7; return -1; } else if(((a16==11) && ((a15==3) && (((a12==8) && (input == 5)) && a18 <= -156 )))){ a16 = 8; a12 = 5; return -1; } else if((((a16==8) && (((input == 4) && (a15==4)) && (a12==5))) && a18 <= -156 )){ return -1; } else if(((a16==8) && (((((a12==9) && ((-156 < a18) && (-79 >= a18)) ) || (( 134 < a18 && (a12==8)) || ( a18 <= -156 && (a12==9)))) && (input == 3)) && (a15==4)))){ a18 = ((((((a18 * 9)/ 10) % 38)- 117) + -30963) + 30963); a16 = 9; a12 = 5; return 22; } else if((((((a12==5) && (input == 6)) && (a16==12)) && 134 < a18 ) && (a15==3))){ a18 = ((((a18 - 133708) / 5) / 5) - 473751); a16 = 8; return -1; } else if(((a15==4) && ((a16==9) && ((a12==6) && ((input == 5) && ( ((-156 < a18) && (-79 >= a18)) || ((-79 < a18) && (134 >= a18)) )))))){ a18 = ((((a18 / 5) + -18) + 538676) - 538696); return -1; } else if((((a15==3) && ((a16==11) && ((input == 3) && (a12==8)))) && a18 <= -156 )){ a16 = 8; a12 = 5; return -1; } else if(((a15==3) && (( ((-79 < a18) && (134 >= a18)) && ((a16==12) && (input == 2))) && (a12==7)))){ a18 = (((a18 + -122114) / 5) - 319126); a16 = 8; a12 = 5; return -1; } else if(((((( ((-156 < a18) && (-79 >= a18)) || ((-79 < a18) && (134 >= a18)) ) && (input == 6)) && (a16==12)) && (a15==3)) && (a12==9))){ a18 = (((a18 - 568671) / 5) - -21092); a16 = 8; a15 = 4; a12 = 7; return 26; } else if(((a12==9) && ((((input == 6) && a18 <= -156 ) && (a16==9)) && (a15==4)))){ a18 = (((a18 + 600140) - -5) + 6); a16 = 10; a15 = 3; a12 = 8; return -1; } else if(((a12==6) && ((a15==4) && (( 134 < a18 && (input == 3)) && (a16==10))))){ a18 = ((((a18 - 0) / 5) * 4) - 482286); a16 = 8; a12 = 5; return 26; } else if(((((( ((-79 < a18) && (134 >= a18)) || ( a18 <= -156 || ((-156 < a18) && (-79 >= a18)) )) && (input == 2)) && (a12==6)) && (a16==12)) && (a15==3))){ a18 = ((((a18 / 5) / 5) - -69371) + -434278); a16 = 8; a12 = 5; return -1; } else if(((a12==8) && ((((input == 2) && ( ((-156 < a18) && (-79 >= a18)) || ((-79 < a18) && (134 >= a18)) )) && (a16==11)) && (a15==3)))){ a18 = (((a18 + -260389) / 5) - 210583); a16 = 8; a12 = 5; return -1; } else if(((a16==10) && ((a15==4) && ((a12==5) && ((input == 3) && ( ((-79 < a18) && (134 >= a18)) || 134 < a18 )))))){ a18 = ((((a18 % 299932)- -300066) - 71339) + 71340); a16 = 12; a15 = 3; a12 = 9; return 22; } else if(((a15==4) && ((a16==9) && ((input == 2) && (((a12==5) && 134 < a18 ) || ( a18 <= -156 && (a12==6))))))){ a18 = (((((a18 * 9)/ 10) % 299922)+ -300077) - 1); a16 = 8; a15 = 3; a12 = 5; return -1; } else if(((((( 134 < a18 && (a12==8)) || ( a18 <= -156 && (a12==9))) && (input == 5)) && (a15==3)) && (a16==12))){ a18 = ((((a18 % 299922)+ -300077) / 5) - 30273); a16 = 8; a12 = 5; return -1; } else if(((a16==11) && ((a15==3) && ((( ((-156 < a18) && (-79 >= a18)) && (a12==7)) || (( 134 < a18 && (a12==6)) || ( a18 <= -156 && (a12==7)))) && (input == 3))))){ a18 = ((((a18 % 299922)+ -300077) + -1) + -1); a16 = 8; a12 = 5; return -1; } else if(((a15==4) && ((((input == 4) && a18 <= -156 ) && (a12==9)) && (a16==9)))){ a18 = ((((a18 - -89780) % 38)+ -117) + 1); a15 = 3; a12 = 5; return -1; } else if(((a15==4) && (((a12==5) && ((input == 5) && a18 <= -156 )) && (a16==8)))){ a15 = 3; return -1; } else if((((((input == 2) && (a12==5)) && ((-156 < a18) && (-79 >= a18)) ) && (a15==4)) && (a16==10))){ a18 = ((((a18 + -131462) * 10)/ 9) * 4); a16 = 8; return -1; } else if((((a15==3) && ((a12==5) && ((input == 6) && (a16==11)))) && ((-156 < a18) && (-79 >= a18)) )){ a18 = ((((a18 * 10)/ 5) + -596729) * 1); a16 = 8; return -1; } else if((((a15==4) && ((a16==9) && ((input == 6) && (( ((-156 < a18) && (-79 >= a18)) || ((-79 < a18) && (134 >= a18)) ) || 134 < a18 )))) && (a12==8))){ a18 = (((((a18 - 211013) % 38)- 116) / 5) - 104); a16 = 10; a15 = 3; return -1; } else if(((a16==11) && ((a15==3) && ((input == 3) && (((a12==9) && ((-156 < a18) && (-79 >= a18)) ) || (( 134 < a18 && (a12==8)) || ((a12==9) && a18 <= -156 ))))))){ a18 = (((((a18 % 38)- 117) * 5) % 38)- 97); a16 = 12; a12 = 7; return 26; } else if(((((a12==6) && ((( a18 <= -156 || ((-156 < a18) && (-79 >= a18)) ) || ((-79 < a18) && (134 >= a18)) ) && (input == 1))) && (a15==4)) && (a16==10))){ a18 = (((((a18 % 106)- -28) + -1) + -96017) - -96017); a16 = 12; a15 = 3; a12 = 5; return 21; } else if(((a15==4) && (((( a18 <= -156 || ((-156 < a18) && (-79 >= a18)) ) && (input == 6)) && (a12==7)) && (a16==8)))){ a18 = ((((a18 % 299922)+ -156) + -148030) - 5822); a15 = 3; a12 = 5; return -1; } else if(((a12==6) && ((a15==3) && (((input == 6) && (( a18 <= -156 || ((-156 < a18) && (-79 >= a18)) ) || ((-79 < a18) && (134 >= a18)) )) && (a16==12))))){ a18 = ((((a18 / 5) - 77572) * 10)/ 9); a12 = 9; return 25; } else if((((a15==4) && ( ((-79 < a18) && (134 >= a18)) && ((input == 5) && (a12==9)))) && (a16==8))){ a18 = (((a18 - 337989) * 1) + -240309); a15 = 3; a12 = 5; return -1; } else if(((a16==8) && ((((( ((-156 < a18) && (-79 >= a18)) || ((-79 < a18) && (134 >= a18)) ) || 134 < a18 ) && (input == 3)) && (a12==5)) && (a15==4)))){ a18 = (((((a18 + 0) * 9)/ 10) / 5) - 594461); a15 = 3; return -1; } else if(((a16==12) && ((a12==5) && ((a15==3) && ((input == 6) && ( ((-156 < a18) && (-79 >= a18)) || ((-79 < a18) && (134 >= a18)) )))))){ a18 = (((((a18 + -597667) * 1) - -30563) % 38)- 112); a12 = 8; return 22; } else if((((a12==7) && ((a15==4) && ((input == 4) && ( a18 <= -156 || ((-156 < a18) && (-79 >= a18)) )))) && (a16==8))){ a18 = ((((a18 - -336694) * 1) % 299922)+ -300077); a15 = 3; a12 = 5; return -1; } else if(((((input == 4) && (((a12==9) && ((-156 < a18) && (-79 >= a18)) ) || (( 134 < a18 && (a12==8)) || ( a18 <= -156 && (a12==9))))) && (a16==8)) && (a15==4))){ a18 = (((((a18 * 9)/ 10) % 299922)- 300077) + -2); a15 = 3; a12 = 5; return -1; } else if((((a12==5) && ( ((-156 < a18) && (-79 >= a18)) && ((a15==4) && (input == 6)))) && (a16==10))){ a18 = ((((a18 - 233839) - 136301) / 5) - -671859); a16 = 9; a12 = 7; return 21; } else if(((a15==4) && ( ((-79 < a18) && (134 >= a18)) && (((input == 3) && (a12==8)) && (a16==8))))){ a18 = (((a18 - -28581) + -601110) - 10494); a15 = 3; a12 = 5; return -1; } else if((((a15==4) && ((input == 3) && (((a12==8) && ((-156 < a18) && (-79 >= a18)) ) || (( 134 < a18 && (a12==7)) || ((a12==8) && a18 <= -156 ))))) && (a16==8))){ a18 = ((((((a18 % 299922)+ -300077) + -2) * 9)/ 10) - 52098); a15 = 3; a12 = 5; return -1; } else if(((a15==4) && ((a16==9) && ((( ((-156 < a18) && (-79 >= a18)) && (a12==7)) || (((a12==6) && 134 < a18 ) || ((a12==7) && a18 <= -156 ))) && (input == 4))))){ a18 = (((((((a18 % 299922)+ -300077) - 2) * 9)/ 10) * 11)/ 10); a16 = 8; a15 = 3; a12 = 5; return -1; } else if(((a16==8) && (( a18 <= -156 && ((input == 5) && (a15==4))) && (a12==6)))){ a12 = 8; return 22; } else if(((a16==8) && (((( 134 < a18 || ( ((-156 < a18) && (-79 >= a18)) || ((-79 < a18) && (134 >= a18)) )) && (input == 6)) && (a15==4)) && (a12==5)))){ a18 = (((((a18 * 9)/ 10) + 11822) * 1) - 601534); a15 = 3; return -1; } else if(((( ((-79 < a18) && (134 >= a18)) && ((input == 4) && (a15==3))) && (a16==12)) && (a12==8))){ a18 = (((a18 - -58548) - 365272) - 81969); a16 = 8; a15 = 4; a12 = 6; return 21; } else if(((((((a12==9) && ((a16==9) && ((-79 < a18) && (134 >= a18)) )) || ((a12==9) && ((a16==9) && 134 < a18 ))) || ((a12==5) && ((a16==10) && a18 <= -156 ))) && (input == 6)) && (a15==4))){ a18 = (((((a18 % 299932)+ 300066) - -1) / 5) - -173797); a16 = 12; a15 = 3; a12 = 9; return 22; } else if(((a12==9) && ((a15==4) && (((input == 4) && (a16==8)) && ((-79 < a18) && (134 >= a18)) )))){ a18 = ((((a18 - -387386) * -1)/ 10) - 350531); a15 = 3; a12 = 5; return -1; } else if(((((a16==12) && ((a15==3) && (input == 6))) && (a12==9)) && 134 < a18 )){ return 22; } else if(((a12==7) && ((a15==4) && (( ((-79 < a18) && (134 >= a18)) && (input == 1)) && (a16==8))))){ a18 = (((a18 / 5) / 5) - 438923); a15 = 3; a12 = 5; return -1; } else if(((a15==4) && ((((input == 5) && 134 < a18 ) && (a16==10)) && (a12==6)))){ a16 = 8; a15 = 3; a12 = 9; return -1; } else if((((a15==3) && (((input == 2) && (a12==9)) && 134 < a18 )) && (a16==12))){ return -1; } else if(((((( 134 < a18 && (a12==8)) || ((a12==9) && a18 <= -156 )) && (input == 3)) && (a15==3)) && (a16==12))){ a18 = (((((a18 - 0) + 0) + 0) % 299922)- 300077); a16 = 8; a12 = 5; return -1; } else if((((((a16==11) && (input == 2)) && (a15==3)) && (a12==5)) && ((-156 < a18) && (-79 >= a18)) )){ a18 = ((((a18 - 388142) - 114659) * 10)/ 9); a16 = 8; return -1; } else if(((a12==5) && ((a16==12) && (((input == 3) && (a15==3)) && 134 < a18 )))){ a18 = ((((((a18 % 106)- -23) + 2) * 5) % 106)+ -70); a12 = 8; return 24; } else if((((a15==4) && ((a12==6) && ((input == 5) && (( ((-156 < a18) && (-79 >= a18)) || ((-79 < a18) && (134 >= a18)) ) || 134 < a18 )))) && (a16==8))){ a18 = (((((a18 % 299922)- 300077) + -2) / 5) - 29645); a16 = 12; a15 = 3; a12 = 9; return 25; } else if(((((( ((-156 < a18) && (-79 >= a18)) || ((-79 < a18) && (134 >= a18)) ) && (input == 5)) && (a15==3)) && (a12==5)) && (a16==12))){ a18 = ((((a18 % 106)- -28) + 1) - 1); return 24; } else if((((a12==9) && (((a15==3) && (input == 4)) && 134 < a18 )) && (a16==12))){ a18 = (((((a18 - 229749) % 299922)+ -300077) / 5) - 241926); a16 = 8; a12 = 5; return -1; } else if(((a15==3) && ((a16==11) && ((a12==5) && (( ((-79 < a18) && (134 >= a18)) || 134 < a18 ) && (input == 1)))))){ a18 = (((((a18 * 9)/ 10) % 106)- -28) + 1); a12 = 7; return 26; } else if(((a15==4) && ((((a12==9) && (input == 3)) && a18 <= -156 ) && (a16==9)))){ a16 = 10; a12 = 5; return 21; } else if(((a12==5) && ((a15==4) && (((input == 1) && (a16==10)) && ((-156 < a18) && (-79 >= a18)) )))){ a18 = (((a18 + -288461) + -195317) * 1); a16 = 8; return 26; } else if(((((a16==9) && ((input == 2) && (a15==4))) && ((-156 < a18) && (-79 >= a18)) ) && (a12==9))){ a18 = (((((a18 * 10)/ 5) * 10)/ 9) + -493699); a16 = 8; a15 = 3; return -1; } else if((((a12==5) && ((( ((-156 < a18) && (-79 >= a18)) || ((-79 < a18) && (134 >= a18)) ) && (input == 2)) && (a16==9))) && (a15==4))){ a18 = (((a18 / 5) - -417716) + 79833); a16 = 12; a15 = 3; a12 = 9; return 26; } else if(((a15==3) && ((a16==11) && (((((a12==6) && 134 < a18 ) || ( a18 <= -156 && (a12==7))) || ( ((-156 < a18) && (-79 >= a18)) && (a12==7))) && (input == 6))))){ a18 = ((((a18 % 299922)+ -300077) + -1) + -1); a12 = 9; return 24; } else if((((a12==8) && ((a16==11) && (( ((-156 < a18) && (-79 >= a18)) || ((-79 < a18) && (134 >= a18)) ) && (input == 3)))) && (a15==3))){ a18 = (((a18 - -441612) - -144586) + 8176); a16 = 12; a12 = 6; return 22; } else if(((a16==12) && (( 134 < a18 && ((a12==9) && (input == 3))) && (a15==3)))){ a18 = ((((a18 % 299922)- 300077) - 272337) - 27219); a16 = 8; a12 = 5; return -1; } else if(((((a12==8) && (( 134 < a18 || ( ((-156 < a18) && (-79 >= a18)) || ((-79 < a18) && (134 >= a18)) )) && (input == 4))) && (a15==4)) && (a16==9))){ a18 = ((((((a18 * 9)/ 10) % 38)+ -117) - 511801) - -511801); a12 = 9; return 21; } else if(((((((a16==12) && a18 <= -156 ) && (a12==5)) || (((a12==9) && ((a16==11) && ((-79 < a18) && (134 >= a18)) )) || ((a12==9) && ((a16==11) && 134 < a18 )))) && (input == 5)) && (a15==3))){ a18 = ((((a18 % 299922)+ -300077) * 1) + 0); a16 = 8; a12 = 5; return -1; } else if(((a16==12) && (((a15==3) && ((input == 3) && ( ((-156 < a18) && (-79 >= a18)) || ((-79 < a18) && (134 >= a18)) ))) && (a12==9)))){ a18 = (((a18 - -438851) + -1005658) + 501717); a16 = 8; a12 = 5; return -1; } else if((((((input == 4) && ( ((-156 < a18) && (-79 >= a18)) || ((-79 < a18) && (134 >= a18)) )) && (a16==12)) && (a12==5)) && (a15==3))){ a18 = (((((a18 % 38)+ -116) - -324773) * 1) - 324773); return 21; } else if(((a15==3) && (((( a18 <= -156 && (a16==12)) && (a12==5)) || ((( ((-79 < a18) && (134 >= a18)) && (a16==11)) && (a12==9)) || (( 134 < a18 && (a16==11)) && (a12==9)))) && (input == 2)))){ a18 = (((((a18 * 9)/ 10) % 299922)+ -300077) + -2); a16 = 8; a12 = 5; return -1; } else if((((a12==6) && ((a15==4) && (( ((-79 < a18) && (134 >= a18)) || ( a18 <= -156 || ((-156 < a18) && (-79 >= a18)) )) && (input == 5)))) && (a16==10))){ a18 = ((((a18 - -34662) % 299932)- -300066) * 1); a15 = 3; return -1; } else if(((a15==4) && ((a16==9) && (((input == 5) && a18 <= -156 ) && (a12==9))))){ a18 = ((((a18 - 0) + 0) % 106)+ 100); a16 = 8; a15 = 3; a12 = 5; return -1; } else if(((a15==3) && ((a12==9) && ((a16==12) && (( ((-156 < a18) && (-79 >= a18)) || ((-79 < a18) && (134 >= a18)) ) && (input == 4)))))){ a18 = (((a18 - 311285) / 5) - 169375); a16 = 8; a12 = 5; return -1; } else if((((((input == 2) && a18 <= -156 ) && (a16==9)) && (a15==4)) && (a12==9))){ a18 = ((((((a18 * 9)/ 10) * 1) * 1) % 106)- -133); a15 = 3; a12 = 8; return -1; } else if((((((a12==9) && ((a16==8) && 134 < a18 )) || (( a18 <= -156 && (a16==9)) && (a12==5))) && (input == 4)) && (a15==4))){ a18 = (((((a18 + 0) / 5) * 4) % 299922)- 300077); a16 = 8; a15 = 3; a12 = 5; return -1; } else if(((a12==5) && ((a16==10) && (((input == 6) && ( ((-79 < a18) && (134 >= a18)) || 134 < a18 )) && (a15==4))))){ a18 = ((((a18 * 9)/ 10) + 39879) + 10187); a16 = 9; a15 = 3; a12 = 9; return -1; } else if(((((input == 6) && (((a12==9) && ((-156 < a18) && (-79 >= a18)) ) || (((a12==8) && 134 < a18 ) || ( a18 <= -156 && (a12==9))))) && (a16==8)) && (a15==4))){ a18 = (((((a18 * 9)/ 10) + -45334) % 299922)+ -300077); a15 = 3; a12 = 5; return -1; } else if(((a15==3) && (((a12==8) && ((input == 5) && ( ((-156 < a18) && (-79 >= a18)) || ((-79 < a18) && (134 >= a18)) ))) && (a16==11)))){ a18 = (((a18 - 574900) * 1) * 1); a16 = 8; a12 = 5; return -1; } else if(((a16==12) && ((a15==3) && (((((a12==7) && 134 < a18 ) || ((a12==8) && a18 <= -156 )) || ( ((-156 < a18) && (-79 >= a18)) && (a12==8))) && (input == 2))))){ a18 = ((((a18 % 299922)- 300077) + -1) * 1); a16 = 8; a12 = 5; return -1; } else if(((a15==3) && ((((((a12==8) && 134 < a18 ) || ((a12==9) && a18 <= -156 )) || ((a12==9) && ((-156 < a18) && (-79 >= a18)) )) && (input == 6)) && (a16==11)))){ a18 = ((((a18 % 299922)+ -300077) - 2) + 0); a16 = 8; a12 = 5; return -1; } else if(((((a16==8) && ((( ((-156 < a18) && (-79 >= a18)) || ((-79 < a18) && (134 >= a18)) ) || 134 < a18 ) && (input == 1))) && (a15==4)) && (a12==5))){ a18 = ((((a18 % 299922)+ -300077) - 1) - 1); a15 = 3; return -1; } else if(((a12==8) && ((a16==11) && ((a15==3) && ((input == 1) && ( ((-156 < a18) && (-79 >= a18)) || ((-79 < a18) && (134 >= a18)) )))))){ a18 = (((a18 / 5) + -194631) + -403246); a16 = 8; a12 = 5; return -1; } else if(((((input == 1) && (((a12==9) && ((-156 < a18) && (-79 >= a18)) ) || (( 134 < a18 && (a12==8)) || ((a12==9) && a18 <= -156 )))) && (a15==3)) && (a16==11))){ a18 = ((((((a18 * 9)/ 10) % 299922)- 300077) / 5) + -194205); a16 = 8; a12 = 5; return -1; } else if((((((( a18 <= -156 || ((-156 < a18) && (-79 >= a18)) ) || ((-79 < a18) && (134 >= a18)) ) && (input == 1)) && (a12==6)) && (a15==3)) && (a16==11))){ a18 = ((((a18 / 5) + 361665) * 10)/ -9); a16 = 8; a12 = 5; return -1; } else if(((((a12==8) && ((input == 2) && (a16==8))) && ((-79 < a18) && (134 >= a18)) ) && (a15==4))){ a18 = (((a18 + -445261) / 5) + -398719); a15 = 3; a12 = 5; return -1; } else if(((a15==4) && ((((((a12==6) && 134 < a18 ) || ((a12==7) && a18 <= -156 )) || ( ((-156 < a18) && (-79 >= a18)) && (a12==7))) && (input == 5)) && (a16==9)))){ a18 = ((((((a18 % 299922)+ -300077) / 5) + 368648) * -1)/ 10); a16 = 8; a15 = 3; a12 = 5; return -1; } else if((((((input == 4) && (a15==3)) && a18 <= -156 ) && (a12==8)) && (a16==11))){ a16 = 8; a12 = 5; return -1; } else if((((a16==11) && (((a15==3) && (input == 2)) && a18 <= -156 )) && (a12==8))){ a18 = (((((a18 * 9)/ 10) % 106)- -27) - 0); a16 = 12; a12 = 6; return 26; } else if(( ((-79 < a18) && (134 >= a18)) && ((a15==4) && (((a16==8) && (input == 4)) && (a12==7))))){ a18 = (((((a18 - 14625) % 38)- 90) + 504647) - 504666); a12 = 9; return 21; } else if(((a16==12) && ((((input == 1) && ((-79 < a18) && (134 >= a18)) ) && (a15==3)) && (a12==8)))){ a18 = ((((a18 - 505930) * 10)/ 9) + -6324); a16 = 8; a12 = 5; return -1; } else if((((a15==4) && ((((a12==5) && 134 < a18 ) || ((a12==6) && a18 <= -156 )) && (input == 3))) && (a16==9))){ a18 = ((((((a18 * 9)/ 10) * 1) * 1) % 299922)+ -300077); a16 = 8; a15 = 3; a12 = 5; return -1; } else if(((((a16==12) && ( 134 < a18 && (input == 4))) && (a15==3)) && (a12==5))){ a18 = (((((a18 - 0) % 299922)+ -300077) * 10)/ 9); a16 = 8; return -1; } else if(( ((-156 < a18) && (-79 >= a18)) && ((a15==3) && ((a12==5) && ((a16==11) && (input == 3)))))){ a18 = (((a18 - 346761) - -815404) + -976893); a16 = 8; return -1; } else if((((a15==4) && ((((a12==5) && 134 < a18 ) || ((a12==6) && a18 <= -156 )) && (input == 1))) && (a16==9))){ a18 = (((((a18 % 299922)- 300077) + -2) + 166911) + -166909); a16 = 8; a15 = 3; a12 = 5; return -1; } else if(((a15==3) && ((a16==12) && ((input == 4) && (((a12==8) && 134 < a18 ) || ((a12==9) && a18 <= -156 )))))){ a18 = (((((a18 + 0) % 299922)+ -300077) - -216724) + -216725); a16 = 8; a12 = 5; return -1; } else if(((a16==12) && ( ((-156 < a18) && (-79 >= a18)) && (((a12==7) && (input == 1)) && (a15==3))))){ a18 = ((((a18 - -321471) / 5) * -1)/ 10); a16 = 8; a15 = 4; a12 = 5; return 22; } else if(((( ((-79 < a18) && (134 >= a18)) && ((a12==7) && (input == 2))) && (a16==8)) && (a15==4))){ a18 = (((a18 + -10249) - 154667) - 274224); a15 = 3; a12 = 5; return -1; } else if((((a12==7) && ( ((-79 < a18) && (134 >= a18)) && ((a15==4) && (input == 6)))) && (a16==8))){ a18 = ((((a18 + -530804) * 1) * 10)/ 9); a15 = 3; a12 = 5; return -1; } else if(((a16==10) && ((((input == 4) && (a12==5)) && (a15==4)) && ((-156 < a18) && (-79 >= a18)) ))){ a18 = ((((a18 / 5) - 345528) - 47726) + 960891); a16 = 8; a15 = 3; a12 = 8; return -1; } else if((((a16==12) && ((( 134 < a18 && (a12==6)) || ((a12==7) && a18 <= -156 )) && (input == 1))) && (a15==3))){ a18 = (((a18 / 5) - -286090) - 697375); a16 = 8; a12 = 5; return -1; } else if(((a12==5) && (((a16==10) && (( ((-79 < a18) && (134 >= a18)) || 134 < a18 ) && (input == 4))) && (a15==4)))){ a18 = ((((a18 / 5) * 4) / 5) - -92063); a16 = 8; a15 = 3; a12 = 6; return -1; } else if(((a16==12) && (((((a12==6) && 134 < a18 ) || ( a18 <= -156 && (a12==7))) && (input == 5)) && (a15==3)))){ a18 = (((((a18 * 9)/ 10) / 5) % 106)- -27); a12 = 9; return 26; } else if((((a16==9) && ((( ((-156 < a18) && (-79 >= a18)) || ((-79 < a18) && (134 >= a18)) ) && (input == 3)) && (a12==6))) && (a15==4))){ a18 = ((((a18 - 434752) * 10)/ 9) * 1); a16 = 8; a15 = 3; a12 = 5; return -1; } else if(((a16==9) && ((a15==4) && ((input == 3) && (( a18 <= -156 && (a12==8)) || (( ((-79 < a18) && (134 >= a18)) && (a12==7)) || ( 134 < a18 && (a12==7)))))))){ a18 = (((((a18 % 299922)- 300077) + 492107) / 5) - 171690); a16 = 8; a15 = 3; a12 = 5; return -1; } else if(((a15==4) && (((input == 5) && ((((a12==7) && 134 < a18 ) || ( a18 <= -156 && (a12==8))) || ((a12==8) && ((-156 < a18) && (-79 >= a18)) ))) && (a16==8)))){ a18 = (((((a18 * 9)/ 10) * 1) % 299922)- 300077); a15 = 3; a12 = 5; return -1; } else if(((a16==9) && (((a15==4) && ((input == 1) && a18 <= -156 )) && (a12==9)))){ a18 = ((((a18 - 0) + 432253) % 38)+ -117); a16 = 10; a12 = 5; return 22; } else if(((a12==6) && ((a16==9) && ((a15==4) && (( ((-156 < a18) && (-79 >= a18)) || ((-79 < a18) && (134 >= a18)) ) && (input == 6)))))){ a18 = ((((((a18 - 391987) * 10)/ 9) - -1010678) * -1)/ 10); a16 = 8; a12 = 7; return -1; } else if(((a15==4) && ((a16==10) && (((input == 4) && (( a18 <= -156 || ((-156 < a18) && (-79 >= a18)) ) || ((-79 < a18) && (134 >= a18)) )) && (a12==6))))){ a18 = ((((((a18 * 9)/ 10) % 106)- -28) + -527048) + 527047); a16 = 12; a15 = 3; a12 = 5; return 21; } else if(((((input == 5) && (((a12==8) && a18 <= -156 ) || (( ((-79 < a18) && (134 >= a18)) && (a12==7)) || ( 134 < a18 && (a12==7))))) && (a15==4)) && (a16==9))){ a18 = (((((a18 * 9)/ 10) % 299922)+ -300077) - 1); a16 = 8; a15 = 3; a12 = 5; return -1; } else if(((a16==12) && ( ((-79 < a18) && (134 >= a18)) && (((input == 2) && (a15==3)) && (a12==8))))){ a18 = (((a18 + -78407) * 5) * 1); a16 = 8; a12 = 5; return -1; } else if(((a15==3) && (((a12==5) && (( ((-156 < a18) && (-79 >= a18)) || ((-79 < a18) && (134 >= a18)) ) && (input == 2))) && (a16==12)))){ a18 = (((a18 + -461068) + -81241) / 5); a16 = 8; return -1; } else if((((a12==7) && ((a15==3) && (( ((-79 < a18) && (134 >= a18)) || 134 < a18 ) && (input == 2)))) && (a16==11))){ a18 = ((((a18 - 0) % 299922)+ -300077) * 1); a16 = 8; a12 = 5; return -1; } else if(((a12==6) && ((a15==3) && ((a16==12) && (( ((-79 < a18) && (134 >= a18)) || ( a18 <= -156 || ((-156 < a18) && (-79 >= a18)) )) && (input == 1)))))){ a18 = ((((a18 + 570150) + 12375) / 5) - 311619); a16 = 8; a12 = 5; return -1; } else if((((a15==4) && ((input == 6) && (((a12==7) && ((-156 < a18) && (-79 >= a18)) ) || (( 134 < a18 && (a12==6)) || ((a12==7) && a18 <= -156 ))))) && (a16==9))){ a18 = ((((a18 % 299922)+ -300077) + -1) - 1); a16 = 8; a15 = 3; a12 = 5; return -1; } else if((((a15==3) && ((a16==12) && ((input == 5) && ( ((-156 < a18) && (-79 >= a18)) || ((-79 < a18) && (134 >= a18)) )))) && (a12==9))){ a18 = ((((a18 + -342736) - 10111) * 10)/ 9); a16 = 8; a12 = 5; return -1; } else if(((a15==4) && (((( a18 <= -156 && (a16==10)) && (a12==5)) || ((((a16==9) && ((-79 < a18) && (134 >= a18)) ) && (a12==9)) || (( 134 < a18 && (a16==9)) && (a12==9)))) && (input == 4)))){ a18 = (((((a18 + 0) * 9)/ 10) % 299932)- -300066); a16 = 10; a12 = 6; return 22; } else if(((a15==3) && ((((a16==12) && (input == 1)) && (a12==7)) && ((-79 < a18) && (134 >= a18)) ))){ a18 = (((a18 + -550746) - 39665) - 1952); a16 = 8; a12 = 5; return -1; } else if(((a15==4) && (((a16==9) && ((input == 4) && ( ((-156 < a18) && (-79 >= a18)) || ((-79 < a18) && (134 >= a18)) ))) && (a12==5)))){ a18 = (((a18 * 5) - -337473) - 438171); a16 = 8; a15 = 3; return -1; } else if(((a15==4) && ((input == 3) && ((((a16==10) && a18 <= -156 ) && (a12==5)) || (((a12==9) && ( ((-79 < a18) && (134 >= a18)) && (a16==9))) || ((a12==9) && ((a16==9) && 134 < a18 ))))))){ a18 = ((((a18 - 0) % 299932)+ 300066) - -2); a16 = 9; a15 = 3; a12 = 7; return -1; } else if((((a15==3) && ((( ((-79 < a18) && (134 >= a18)) || 134 < a18 ) && (input == 1)) && (a12==7))) && (a16==11))){ a18 = ((((a18 % 299932)- -300066) / 5) * 5); a16 = 12; a12 = 5; return 24; } else if((((a12==5) && ( 134 < a18 && ((a16==12) && (input == 2)))) && (a15==3))){ a18 = ((((a18 % 299922)- 300077) + -264640) * 1); a16 = 8; return -1; } else if((((input == 1) && ((((a16==8) && 134 < a18 ) && (a12==9)) || (((a16==9) && a18 <= -156 ) && (a12==5)))) && (a15==4))){ a18 = ((((a18 % 299932)- -300066) / 5) - -391507); a16 = 8; a12 = 6; return 22; } else if(((a12==6) && (((a15==3) && ((input == 5) && (( a18 <= -156 || ((-156 < a18) && (-79 >= a18)) ) || ((-79 < a18) && (134 >= a18)) ))) && (a16==12)))){ a18 = ((((a18 / 5) + -85998) * 10)/ 9); a16 = 8; a12 = 5; return -1; } else if((((a12==6) && ((( ((-79 < a18) && (134 >= a18)) || ( a18 <= -156 || ((-156 < a18) && (-79 >= a18)) )) && (input == 5)) && (a16==11))) && (a15==3))){ a18 = ((((a18 * 9)/ 10) + -36694) - 20345); a12 = 8; return 21; } else if(((a16==12) && ((a15==3) && (( ((-79 < a18) && (134 >= a18)) && (input == 5)) && (a12==8))))){ a18 = (((((a18 / 5) - 448485) + 1026663) * -1)/ 10); a16 = 8; a12 = 5; return -1; } else if(((a12==6) && ((a16==11) && ((( ((-79 < a18) && (134 >= a18)) || ( a18 <= -156 || ((-156 < a18) && (-79 >= a18)) )) && (input == 6)) && (a15==3))))){ a18 = ((((a18 % 106)+ 27) - 0) - 0); a12 = 8; return 21; } else if(((a12==8) && ((a15==3) && ( ((-79 < a18) && (134 >= a18)) && ((input == 3) && (a16==12)))))){ a18 = ((((a18 + -545737) + -23113) + 1070233) + -885976); a16 = 8; a12 = 5; return -1; } else if((((a15==4) && (((input == 6) && (a16==8)) && (a12==9))) && ((-79 < a18) && (134 >= a18)) )){ a18 = (((a18 + -53755) - 464770) + -16467); a15 = 3; a12 = 5; return -1; } else if((((a16==9) && ((a12==5) && (( ((-156 < a18) && (-79 >= a18)) || ((-79 < a18) && (134 >= a18)) ) && (input == 3)))) && (a15==4))){ a18 = (((a18 * 5) - 10445) - 493515); a16 = 8; a15 = 3; return -1; } else if(((a15==4) && (((a12==6) && ((input == 3) && (a16==8))) && a18 <= -156 ))){ a15 = 3; a12 = 5; return -1; } else if(((a16==8) && ((a15==4) && ((a12==6) && ((input == 6) && (( ((-156 < a18) && (-79 >= a18)) || ((-79 < a18) && (134 >= a18)) ) || 134 < a18 )))))){ a18 = (((((a18 % 299922)+ -300077) - 1) / 5) + -169688); a15 = 3; a12 = 5; return -1; } else if((((a16==9) && (((( ((-156 < a18) && (-79 >= a18)) || ((-79 < a18) && (134 >= a18)) ) || 134 < a18 ) && (input == 2)) && (a15==4))) && (a12==8))){ a18 = ((((a18 % 299922)+ -300077) - 2) - 0); a12 = 9; return 21; } else if(((a12==5) && (((a16==9) && (( ((-156 < a18) && (-79 >= a18)) || ((-79 < a18) && (134 >= a18)) ) && (input == 6))) && (a15==4)))){ a18 = (((a18 + -119540) + -156143) + 89026); a16 = 8; a15 = 3; return -1; } else if((((( a18 <= -156 && (input == 4)) && (a15==4)) && (a12==6)) && (a16==8))){ a15 = 3; a12 = 5; return -1; } else if(((a12==6) && (((a16==10) && ((input == 4) && 134 < a18 )) && (a15==4)))){ a18 = (((a18 / 5) + -58871) - 215176); return 24; } else if((((a15==3) && ((input == 6) && (( 134 < a18 && (a12==6)) || ((a12==7) && a18 <= -156 )))) && (a16==12))){ a18 = (((((a18 % 299922)- 300077) * 1) / 5) + -32545); a16 = 8; a12 = 5; return -1; } else if(((((a15==4) && ((input == 1) && ( a18 <= -156 || ((-156 < a18) && (-79 >= a18)) ))) && (a12==7)) && (a16==8))){ a18 = ((((a18 * 9)/ 10) - 44611) - 2793); a15 = 3; a12 = 5; return -1; } else if(((a15==3) && ((a16==11) && ((( ((-156 < a18) && (-79 >= a18)) && (a12==7)) || (((a12==6) && 134 < a18 ) || ( a18 <= -156 && (a12==7)))) && (input == 4))))){ a18 = ((((a18 / 5) * 4) % 299922)- 300077); a16 = 8; a12 = 5; return -1; } else if((((input == 5) && ((((a12==9) && ( ((-79 < a18) && (134 >= a18)) && (a16==9))) || (((a16==9) && 134 < a18 ) && (a12==9))) || (( a18 <= -156 && (a16==10)) && (a12==5)))) && (a15==4))){ a18 = ((((a18 % 299932)- -300066) - -1) - 0); a16 = 12; a15 = 3; a12 = 9; return 22; } else if(((a12==5) && ((a16==11) && (((input == 1) && (a15==3)) && ((-156 < a18) && (-79 >= a18)) )))){ a12 = 6; return 22; } else if(((a16==8) && (((input == 1) && ((( 134 < a18 && (a12==7)) || ((a12==8) && a18 <= -156 )) || ( ((-156 < a18) && (-79 >= a18)) && (a12==8)))) && (a15==4)))){ a18 = (((((a18 - 0) / 5) * 4) % 299922)- 300077); a15 = 3; a12 = 5; return -1; } else if(((a16==9) && ((((input == 2) && ( ((-156 < a18) && (-79 >= a18)) || ((-79 < a18) && (134 >= a18)) )) && (a15==4)) && (a12==6)))){ a18 = ((((a18 % 106)+ 27) - 0) - -1); return -1; } else if(((a16==11) && ((a15==3) && (((input == 3) && (( a18 <= -156 || ((-156 < a18) && (-79 >= a18)) ) || ((-79 < a18) && (134 >= a18)) )) && (a12==6))))){ a18 = ((((a18 % 299922)- 300077) + -1) - 1); a16 = 8; a12 = 5; return -1; } else if(((a15==4) && ((input == 5) && (((a12==9) && ((a16==8) && 134 < a18 )) || (((a16==9) && a18 <= -156 ) && (a12==5)))))){ a18 = ((((a18 % 299922)+ -300077) * 1) * 1); a16 = 8; a15 = 3; a12 = 5; return -1; } else if(((a15==4) && ((input == 2) && ((( 134 < a18 && (a16==8)) && (a12==9)) || ((a12==5) && ((a16==9) && a18 <= -156 )))))){ a18 = ((((a18 % 299922)- 300077) - 2) - 0); a16 = 8; a15 = 3; a12 = 5; return -1; } else if(((((a12==6) && (( ((-156 < a18) && (-79 >= a18)) || ((-79 < a18) && (134 >= a18)) ) && (input == 1))) && (a16==9)) && (a15==4))){ a18 = (((a18 + -381867) * 1) * 1); a16 = 8; a15 = 3; a12 = 5; return -1; } else if(((a15==3) && (((input == 4) && (( 134 < a18 && (a12==6)) || ( a18 <= -156 && (a12==7)))) && (a16==12)))){ a18 = ((((a18 % 299922)+ -300077) + 179128) + -179128); a16 = 8; a12 = 5; return -1; } else if(( ((-156 < a18) && (-79 >= a18)) && (((a12==5) && ((input == 4) && (a15==3))) && (a16==11)))){ a18 = ((((a18 - -196) - -3) - 306144) + 306115); return 21; } else if(((( ((-79 < a18) && (134 >= a18)) && ((input == 5) && (a15==4))) && (a12==8)) && (a16==8))){ a18 = ((((a18 - -325901) - 596158) * 10)/ 9); a15 = 3; a12 = 5; return -1; } else if((((input == 4) && ((((a12==9) && ( ((-79 < a18) && (134 >= a18)) && (a16==11))) || ((a12==9) && ( 134 < a18 && (a16==11)))) || (( a18 <= -156 && (a16==12)) && (a12==5)))) && (a15==3))){ a18 = ((((a18 % 106)+ 28) - 1) - 0); a16 = 12; a12 = 7; return 21; } else if(((a15==4) && ((((((a12==7) && 134 < a18 ) || ((a12==8) && a18 <= -156 )) || ((a12==8) && ((-156 < a18) && (-79 >= a18)) )) && (input == 2)) && (a16==8)))){ a18 = ((((a18 / 5) % 106)+ 28) - -1); a12 = 9; return 24; } else if((((a16==9) && ((( a18 <= -156 && (a12==8)) || (((a12==7) && ((-79 < a18) && (134 >= a18)) ) || ( 134 < a18 && (a12==7)))) && (input == 6))) && (a15==4))){ a18 = (((a18 / 5) - 311597) * 1); a16 = 8; a15 = 3; a12 = 5; return -1; } else if(((a16==10) && ( 134 < a18 && ((a12==6) && ((a15==4) && (input == 6)))))){ a18 = ((((a18 % 106)- 22) - -310427) - 310465); a16 = 9; a12 = 8; return 24; } else if(( a18 <= -156 && ((((input == 6) && (a15==3)) && (a16==11)) && (a12==8)))){ a16 = 8; a12 = 5; return -1; } else if(((((input == 1) && (( a18 <= -156 && (a12==8)) || (( ((-79 < a18) && (134 >= a18)) && (a12==7)) || ( 134 < a18 && (a12==7))))) && (a15==4)) && (a16==9))){ a18 = ((((a18 % 38)+ -116) - 1) - 1); a12 = 8; return 24; } else if(((a15==4) && (((a12==6) && ((input == 4) && ( 134 < a18 || ( ((-156 < a18) && (-79 >= a18)) || ((-79 < a18) && (134 >= a18)) )))) && (a16==8)))){ a18 = ((((a18 + -471665) % 299922)+ -300077) + -1); a15 = 3; a12 = 5; return -1; } else if(((a15==4) && ((a16==8) && ((((a12==9) && ((-156 < a18) && (-79 >= a18)) ) || (( 134 < a18 && (a12==8)) || ((a12==9) && a18 <= -156 ))) && (input == 1))))){ a18 = (((((a18 * 9)/ 10) + 30175) / 5) - 488605); a15 = 3; a12 = 5; return -1; } else if((((((a12==5) && ( a18 <= -156 && (a16==12))) || ((( ((-79 < a18) && (134 >= a18)) && (a16==11)) && (a12==9)) || (((a16==11) && 134 < a18 ) && (a12==9)))) && (input == 3)) && (a15==3))){ a18 = ((((a18 % 299922)- 300077) - 1) * 1); a16 = 8; a12 = 5; return -1; } else if((((((a15==3) && (input == 1)) && (a16==12)) && 134 < a18 ) && (a12==5))){ a18 = (((((a18 % 299922)+ -300077) * 10)/ 9) - 83144); a16 = 8; return -1; } else if(((( ((-156 < a18) && (-79 >= a18)) && ((input == 5) && (a16==10))) && (a12==5)) && (a15==4))){ a18 = (((a18 - -463156) - 463043) + 25); a16 = 8; a15 = 3; a12 = 6; return -1; } else if(((a16==11) && ((a12==7) && ((a15==3) && ((input == 5) && ( ((-79 < a18) && (134 >= a18)) || 134 < a18 )))))){ a18 = ((((a18 % 299922)- 300077) + -2) - 0); a16 = 8; a12 = 5; return -1; } else if(((a15==4) && ((a16==9) && (((((a12==7) && ((-79 < a18) && (134 >= a18)) ) || ( 134 < a18 && (a12==7))) || ((a12==8) && a18 <= -156 )) && (input == 2))))){ a18 = (((((a18 % 299922)+ -300077) / 5) * 5) + -2); a16 = 8; a15 = 3; a12 = 5; return -1; } else if((((a16==12) && ((input == 6) && (((a12==8) && 134 < a18 ) || ( a18 <= -156 && (a12==9))))) && (a15==3))){ a18 = (((((a18 * 9)/ 10) * 1) % 106)- -27); a16 = 8; a15 = 4; a12 = 6; return 22; } else if(((a15==4) && (((a16==9) && ((input == 5) && ( ((-156 < a18) && (-79 >= a18)) || ((-79 < a18) && (134 >= a18)) ))) && (a12==5)))){ a18 = ((((a18 - 312650) * 10)/ 9) - 121120); a16 = 8; a15 = 3; return -1; } else if(((a15==3) && ((input == 6) && (((((a16==11) && ((-79 < a18) && (134 >= a18)) ) && (a12==9)) || ((a12==9) && ( 134 < a18 && (a16==11)))) || (((a16==12) && a18 <= -156 ) && (a12==5)))))){ a18 = (((a18 / 5) + -368911) - 86460); a16 = 8; a12 = 5; return -1; } else if(((a16==9) && ((a12==6) && ((a15==4) && ((input == 4) && ( ((-156 < a18) && (-79 >= a18)) || ((-79 < a18) && (134 >= a18)) )))))){ a18 = (((a18 + -541849) / 5) * 5); a12 = 5; return -1; } else if((((a15==4) && (((input == 2) && (a16==8)) && (a12==5))) && a18 <= -156 )){ a18 = ((((((a18 * 9)/ 10) / 5) * 5) % 38)+ -106); a16 = 12; a15 = 3; return 21; } else if(((((a15==3) && ((input == 1) && ( ((-156 < a18) && (-79 >= a18)) || ((-79 < a18) && (134 >= a18)) ))) && (a16==12)) && (a12==9))){ a18 = (((a18 / 5) / 5) + -202401); a16 = 8; a12 = 5; return -1; } else if(((a15==3) && ((a12==5) && ((a16==12) && ((input == 5) && 134 < a18 ))))){ a18 = ((((a18 % 299922)- 300077) + -103268) - 179093); a16 = 8; return -1; } else if((((a15==3) && ((a16==12) && ((input == 3) && ( ((-79 < a18) && (134 >= a18)) || ( a18 <= -156 || ((-156 < a18) && (-79 >= a18)) ))))) && (a12==6))){ a18 = ((((a18 % 299922)+ -300077) + -1) + -1); a16 = 8; a12 = 5; return -1; } else if(((a12==9) && ((((input == 5) && (a15==3)) && (a16==12)) && 134 < a18 ))){ a18 = (((((a18 + 0) - 0) + 0) % 38)- 138); a12 = 8; return -1; } else if(((((input == 2) && (((a12==7) && ((-156 < a18) && (-79 >= a18)) ) || (((a12==6) && 134 < a18 ) || ( a18 <= -156 && (a12==7))))) && (a15==3)) && (a16==11))){ a18 = (((((a18 % 299922)+ -300077) - -251504) - 125524) + -125980); a16 = 8; a12 = 5; return -1; } else if(((a16==11) && ((((input == 3) && ( ((-79 < a18) && (134 >= a18)) || 134 < a18 )) && (a12==5)) && (a15==3)))){ a18 = ((((a18 + 0) * 9)/ 10) + -591177); a16 = 8; return -1; } else if(((a15==4) && ((((a12==9) && ( 134 < a18 && (a16==8))) || ((a12==5) && ((a16==9) && a18 <= -156 ))) && (input == 3)))){ a18 = ((((((a18 - 0) % 38)+ -117) / 5) * 51)/ 10); a16 = 9; a12 = 6; return 22; } else if(((a12==8) && ((((input == 6) && (a15==3)) && ((-79 < a18) && (134 >= a18)) ) && (a16==12)))){ a18 = (((a18 * 5) - 592842) / 5); a16 = 8; a12 = 5; return -1; } else if(((a15==3) && ((a16==12) && ((((a12==6) && 134 < a18 ) || ( a18 <= -156 && (a12==7))) && (input == 3))))){ a18 = ((((a18 % 299922)- 300077) - 2) - 0); a16 = 8; a12 = 5; return -1; } else if((((a16==12) && ((a15==3) && ((a12==7) && (input == 4)))) && ((-79 < a18) && (134 >= a18)) )){ a18 = ((((a18 + -58296) - -119457) * 10)/ 9); a16 = 8; a15 = 4; a12 = 5; return 22; } else if(((((( ((-79 < a18) && (134 >= a18)) || 134 < a18 ) && (input == 3)) && (a15==3)) && (a16==11)) && (a12==7))){ a18 = (((a18 / 5) + -363987) / 5); a16 = 8; a12 = 5; return -1; } else if((((a12==6) && ( a18 <= -156 && ((a16==8) && (input == 6)))) && (a15==4))){ a15 = 3; a12 = 5; return -1; } else if(((((( ((-156 < a18) && (-79 >= a18)) && (a12==9)) || (((a12==8) && 134 < a18 ) || ( a18 <= -156 && (a12==9)))) && (input == 5)) && (a16==11)) && (a15==3))){ a18 = ((((a18 % 299922)+ -300077) - 1) - 1); a16 = 8; a12 = 5; return -1; } else if(( ((-156 < a18) && (-79 >= a18)) && ((((input == 2) && (a16==12)) && (a12==7)) && (a15==3)))){ a18 = ((((a18 - 288903) + -104387) * 10)/ 9); a16 = 8; a12 = 5; return -1; } else if(((a15==4) && ((((input == 5) && ( ((-79 < a18) && (134 >= a18)) || 134 < a18 )) && (a12==5)) && (a16==10)))){ a18 = ((((((a18 % 38)- 117) * 1) * 5) % 38)- 96); return 22; } else if(((a15==4) && ( a18 <= -156 && ((a12==5) && ((a16==8) && (input == 6)))))){ a18 = (((((a18 % 38)- 103) - -12) * 9)/ 10); a16 = 12; a15 = 3; a12 = 7; return -1; } else if((((a16==12) && ((input == 5) && ((((a12==7) && 134 < a18 ) || ( a18 <= -156 && (a12==8))) || ( ((-156 < a18) && (-79 >= a18)) && (a12==8))))) && (a15==3))){ a18 = ((((((a18 + 0) * 9)/ 10) / 5) % 106)- -27); a12 = 5; return 21; } else if(((a16==9) && ((a15==4) && ((input == 6) && (( 134 < a18 && (a12==5)) || ((a12==6) && a18 <= -156 )))))){ a18 = ((((a18 % 299922)- 300077) - 1) * 1); a12 = 7; return 26; } else if((((a12==6) && ((a16==11) && (( ((-79 < a18) && (134 >= a18)) || ( a18 <= -156 || ((-156 < a18) && (-79 >= a18)) )) && (input == 2)))) && (a15==3))){ a18 = (((((a18 % 299922)- 300077) * 1) / 5) - 145687); a16 = 8; a12 = 5; return -1; } else if(((a15==4) && ((a12==9) && ((a16==9) && ((input == 1) && ((-156 < a18) && (-79 >= a18)) ))))){ a18 = (((a18 - -186) - -589325) - 589400); a15 = 3; return -1; } else if(((a15==4) && ((input == 6) && ((((a16==8) && 134 < a18 ) && (a12==9)) || (((a16==9) && a18 <= -156 ) && (a12==5)))))){ a18 = ((((a18 * 9)/ 10) / 5) + -312636); a16 = 8; a15 = 3; a12 = 5; return -1; } else if(((((( ((-156 < a18) && (-79 >= a18)) && (a12==9)) || (( 134 < a18 && (a12==8)) || ( a18 <= -156 && (a12==9)))) && (input == 2)) && (a15==4)) && (a16==8))){ a18 = ((((a18 + 0) % 299922)- 300077) * 1); a15 = 3; a12 = 5; return -1; } return calculate_output2(input); } int calculate_output2(int input) { if(((a16==11) && (((a15==3) && ((input == 4) && ( ((-79 < a18) && (134 >= a18)) || ( a18 <= -156 || ((-156 < a18) && (-79 >= a18)) )))) && (a12==6)))){ a18 = ((((a18 % 299922)+ -300077) * 1) * 1); a16 = 8; a12 = 5; return -1; } else if(((a15==4) && ((input == 2) && ((((a12==9) && ( ((-79 < a18) && (134 >= a18)) && (a16==9))) || (((a16==9) && 134 < a18 ) && (a12==9))) || (((a16==10) && a18 <= -156 ) && (a12==5)))))){ a18 = (((a18 / 5) + -396744) + -23110); a16 = 10; a15 = 3; a12 = 8; return -1; } else if(((a16==11) && (((input == 5) && ((( 134 < a18 && (a12==6)) || ((a12==7) && a18 <= -156 )) || ((a12==7) && ((-156 < a18) && (-79 >= a18)) ))) && (a15==3)))){ a18 = (((((a18 % 106)- -28) - -1) + -190496) - -190494); a12 = 9; return 24; } else if(((a12==7) && ( ((-79 < a18) && (134 >= a18)) && (((input == 5) && (a15==3)) && (a16==12))))){ a18 = ((((a18 / 5) + 4454) / 5) - 411113); a16 = 8; a12 = 5; return -1; } else if((((a15==3) && ((a12==8) && (( ((-156 < a18) && (-79 >= a18)) || ((-79 < a18) && (134 >= a18)) ) && (input == 4)))) && (a16==11))){ a18 = ((((a18 + -273331) * 10)/ 9) / 5); a16 = 8; a12 = 5; return -1; } else if(((a16==10) && ((a15==4) && (( 134 < a18 && (input == 2)) && (a12==6))))){ a18 = ((((a18 - 490505) + -86259) % 299922)+ -300077); a16 = 9; a15 = 3; a12 = 8; return -1; } else if((((a15==4) && ((( ((-156 < a18) && (-79 >= a18)) && (a12==8)) || (( 134 < a18 && (a12==7)) || ((a12==8) && a18 <= -156 ))) && (input == 6))) && (a16==8))){ a18 = (((a18 / 5) + -571) + -337865); a15 = 3; a12 = 5; return -1; } else if(((a16==8) && ((a15==4) && (((input == 2) && (a12==9)) && ((-79 < a18) && (134 >= a18)) )))){ a18 = (((a18 - 193312) - 117004) + -81027); a16 = 9; a12 = 6; return 21; } else if((((((input == 4) && ((-156 < a18) && (-79 >= a18)) ) && (a12==9)) && (a16==9)) && (a15==4))){ a16 = 8; a15 = 3; a12 = 5; return -1; } else if(((a12==7) && ((a15==3) && ((a16==12) && ((input == 4) && ((-156 < a18) && (-79 >= a18)) ))))){ a18 = ((((a18 * 10)/ 5) * 5) * 5); a16 = 8; a12 = 5; return -1; } else if((((a16==9) && ((((a12==5) && 134 < a18 ) || ((a12==6) && a18 <= -156 )) && (input == 5))) && (a15==4))){ a18 = (((a18 - 0) / 5) + -211951); a16 = 8; a15 = 3; a12 = 5; return -1; } else if(((a12==6) && ((a15==4) && ((( ((-79 < a18) && (134 >= a18)) || ( a18 <= -156 || ((-156 < a18) && (-79 >= a18)) )) && (input == 3)) && (a16==10))))){ a18 = ((((((a18 + 101692) % 38)+ -117) * 5) % 38)+ -113); a16 = 8; a15 = 3; a12 = 7; return -1; } else if((((a16==11) && ((a15==3) && (( ((-79 < a18) && (134 >= a18)) || 134 < a18 ) && (input == 4)))) && (a12==7))){ a18 = ((((a18 + -488724) % 299922)- 300077) - 2); a16 = 8; a12 = 5; return -1; } else if((((((input == 6) && (( a18 <= -156 || ((-156 < a18) && (-79 >= a18)) ) || ((-79 < a18) && (134 >= a18)) )) && (a16==10)) && (a15==4)) && (a12==6))){ a18 = (((((a18 * 9)/ 10) + -30078) % 38)+ -89); a16 = 9; a12 = 8; return -1; } else if((((a16==12) && ((input == 2) && (((a12==6) && 134 < a18 ) || ( a18 <= -156 && (a12==7))))) && (a15==3))){ a18 = ((((a18 % 299922)+ -300077) - -391248) - 391248); a16 = 8; a12 = 5; return -1; } else if(((a15==4) && (((a12==6) && ((input == 1) && ( 134 < a18 || ( ((-156 < a18) && (-79 >= a18)) || ((-79 < a18) && (134 >= a18)) )))) && (a16==8)))){ a18 = (((a18 / 5) - 162524) / 5); a15 = 3; a12 = 5; return -1; } else if(((a16==12) && (( ((-79 < a18) && (134 >= a18)) && ((input == 3) && (a12==7))) && (a15==3)))){ a18 = ((((a18 / 5) + -75398) * 10)/ 9); a16 = 8; a12 = 5; return -1; } else if(((((input == 4) && ((((a12==7) && 134 < a18 ) || ((a12==8) && a18 <= -156 )) || ( ((-156 < a18) && (-79 >= a18)) && (a12==8)))) && (a15==4)) && (a16==8))){ a18 = (((((a18 % 299922)- 300077) * 1) - -561980) - 561981); a15 = 3; a12 = 5; return -1; } else if(((a16==9) && ((((((a12==6) && 134 < a18 ) || ( a18 <= -156 && (a12==7))) || ( ((-156 < a18) && (-79 >= a18)) && (a12==7))) && (input == 1)) && (a15==4)))){ a18 = ((((a18 - 0) % 299922)- 300077) * 1); a16 = 8; a15 = 3; a12 = 5; return -1; } else if(((a16==8) && (((input == 5) && (((a12==9) && ((-156 < a18) && (-79 >= a18)) ) || (( 134 < a18 && (a12==8)) || ( a18 <= -156 && (a12==9))))) && (a15==4)))){ a18 = ((((a18 / 5) + -149887) * 10)/ 9); a15 = 3; a12 = 5; return -1; } else if((((((a15==4) && (input == 6)) && (a16==8)) && (a12==8)) && ((-79 < a18) && (134 >= a18)) )){ a18 = (((a18 * 5) + -275350) * 2); a15 = 3; a12 = 5; return -1; } else if(((((a12==5) && (( ((-79 < a18) && (134 >= a18)) || 134 < a18 ) && (input == 2))) && (a16==11)) && (a15==3))){ a18 = ((((a18 - 0) - 0) % 299922)+ -300077); a16 = 8; return -1; } else if((((a12==5) && ((a15==3) && ((input == 4) && ( ((-79 < a18) && (134 >= a18)) || 134 < a18 )))) && (a16==11))){ a18 = (((((a18 % 299922)+ -300077) - 1) / 5) - 308492); a16 = 8; return -1; } else if((((a16==9) && ((input == 4) && (((a12==8) && a18 <= -156 ) || (( ((-79 < a18) && (134 >= a18)) && (a12==7)) || ( 134 < a18 && (a12==7)))))) && (a15==4))){ a18 = (((((a18 - 0) + 0) + 0) % 299922)+ -300077); a16 = 8; a15 = 3; a12 = 5; return -1; } else if(((((input == 2) && ((( 134 < a18 && (a12==8)) || ( a18 <= -156 && (a12==9))) || ( ((-156 < a18) && (-79 >= a18)) && (a12==9)))) && (a15==3)) && (a16==11))){ a18 = ((((a18 % 299922)- 300077) - 2) - 0); a16 = 8; a12 = 5; return -1; } else if(((a15==3) && ((((input == 3) && ( ((-156 < a18) && (-79 >= a18)) || ((-79 < a18) && (134 >= a18)) )) && (a12==5)) && (a16==12)))){ a18 = (((a18 + 91995) + 337235) - 1021683); a16 = 8; return -1; } else if(((a15==4) && (((input == 4) && (( 134 < a18 && (a12==5)) || ( a18 <= -156 && (a12==6)))) && (a16==9)))){ a18 = ((((((a18 + 0) + 0) * 9)/ 10) % 299922)- 300077); a16 = 8; a15 = 3; a12 = 5; return -1; } else if(((a15==4) && ((((input == 3) && (a12==5)) && (a16==8)) && a18 <= -156 ))){ a18 = ((((a18 / 5) / 5) % 38)+ -101); a16 = 12; a15 = 3; return 21; } else if(( ((-156 < a18) && (-79 >= a18)) && (((a15==4) && ((a12==9) && (input == 5))) && (a16==9)))){ a18 = (((a18 + -461124) - -660849) * 3); a16 = 10; a12 = 5; return 26; } else if((((a16==9) && ((a12==8) && ((input == 1) && (( ((-156 < a18) && (-79 >= a18)) || ((-79 < a18) && (134 >= a18)) ) || 134 < a18 )))) && (a15==4))){ a18 = ((((a18 % 38)+ -116) - 2) + 2); a16 = 8; a15 = 3; a12 = 6; return -1; } else if(((a15==4) && ((a16==8) && ((( 134 < a18 || ( ((-156 < a18) && (-79 >= a18)) || ((-79 < a18) && (134 >= a18)) )) && (input == 2)) && (a12==5))))){ a18 = (((((a18 % 299922)+ -300077) + -1) / 5) + -166490); a15 = 3; return -1; } else if(((((a12==8) && ((input == 6) && ( ((-156 < a18) && (-79 >= a18)) || ((-79 < a18) && (134 >= a18)) ))) && (a16==11)) && (a15==3))){ a18 = (((a18 + -89557) * 5) * 1); a16 = 8; a12 = 5; return -1; } else if(((a15==3) && ((a12==6) && ((( ((-79 < a18) && (134 >= a18)) || ( a18 <= -156 || ((-156 < a18) && (-79 >= a18)) )) && (input == 4)) && (a16==12))))){ a18 = ((((a18 % 299922)- 300077) / 5) + -268951); a16 = 8; a12 = 5; return -1; } else if((((a16==8) && ((a15==4) && ((input == 2) && ( a18 <= -156 || ((-156 < a18) && (-79 >= a18)) )))) && (a12==7))){ a18 = ((((a18 - 0) / 5) % 106)+ 112); a12 = 8; return 26; } else if(((a12==5) && (((a15==3) && (( ((-79 < a18) && (134 >= a18)) || 134 < a18 ) && (input == 5))) && (a16==11)))){ a18 = ((((a18 - 263413) % 299922)- 300077) + -2); a16 = 8; return -1; } else if(((a16==8) && ((a12==7) && (((input == 5) && ( a18 <= -156 || ((-156 < a18) && (-79 >= a18)) )) && (a15==4))))){ a18 = ((((((a18 % 299922)- 156) * 1) / 5) * 51)/ 10); a15 = 3; a12 = 5; return -1; } else if(((a16==11) && (((input == 1) && (((a12==7) && ((-156 < a18) && (-79 >= a18)) ) || (((a12==6) && 134 < a18 ) || ( a18 <= -156 && (a12==7))))) && (a15==3)))){ a18 = ((((a18 / 5) * 4) % 38)- 117); a16 = 12; a12 = 5; return 26; } else if(( ((-156 < a18) && (-79 >= a18)) && ((((a16==9) && (input == 6)) && (a15==4)) && (a12==9)))){ a18 = (((a18 * 5) - 354899) * 1); a16 = 10; a12 = 6; return 22; } else if(((((input == 2) && (((a12==8) && 134 < a18 ) || ((a12==9) && a18 <= -156 ))) && (a16==12)) && (a15==3))){ a18 = ((((a18 + 0) % 299922)- 300077) + -2); a16 = 8; a12 = 5; return -1; } else if(((a15==3) && (((( ((-156 < a18) && (-79 >= a18)) && (a12==9)) || (( 134 < a18 && (a12==8)) || ((a12==9) && a18 <= -156 ))) && (input == 4)) && (a16==11)))){ a18 = ((((a18 % 299922)+ -300077) * 1) * 1); a16 = 8; a12 = 5; return -1; } else if((((input == 1) && ((((a12==9) && ((a16==9) && ((-79 < a18) && (134 >= a18)) )) || (( 134 < a18 && (a16==9)) && (a12==9))) || (( a18 <= -156 && (a16==10)) && (a12==5)))) && (a15==4))){ a18 = ((((a18 - 0) % 299932)- -300066) * 1); a16 = 9; a15 = 3; a12 = 5; return -1; } else if(((( ((-79 < a18) && (134 >= a18)) && ((a15==4) && (input == 5))) && (a16==8)) && (a12==7))){ a18 = (((a18 + -501510) * 1) * 1); a15 = 3; a12 = 5; return -1; } else if((((a15==4) && (((( a18 <= -156 || ((-156 < a18) && (-79 >= a18)) ) || ((-79 < a18) && (134 >= a18)) ) && (input == 2)) && (a16==10))) && (a12==6))){ a18 = ((((a18 + 62616) - -362435) % 38)- 116); a12 = 5; return -1; } else if(((((a16==12) && ((a12==7) && (input == 6))) && ((-156 < a18) && (-79 >= a18)) ) && (a15==3))){ a18 = (((a18 + -550912) * 1) + -3494); a16 = 8; a12 = 5; return -1; } 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); } }